[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Mul α
s s₁ s₂ t t₁ t₂ : Finset α
⊢ card s * card t ≤ multiplicativeEnergy s t
[PROOFSTEP]
rw [← card_product]
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Mul α
s s₁ s₂ t t₁ t₂ : Finset α
⊢ card (s ×ˢ t) ≤ multiplicativeEnergy s t
[PROOFSTEP]
refine'
  card_le_card_of_inj_on (@fun x => ((x.1, x.1), x.2, x.2))
    (by
      -- porting note: changed this from a `simp` proof without `only` because of a timeoutsimp only [← and_imp,
        mem_product, and_imp, Prod.forall, mem_filter, and_self, and_true, imp_self, implies_true])
    fun a _ b _ => _
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Mul α
s s₁ s₂ t t₁ t₂ : Finset α
⊢ ∀ (a : α × α),
    a ∈ s ×ˢ t →
      (fun x => ((x.fst, x.fst), x.snd, x.snd)) a ∈
        filter (fun x => x.fst.fst * x.snd.fst = x.fst.snd * x.snd.snd) ((s ×ˢ s) ×ˢ t ×ˢ t)
[PROOFSTEP]
simp only [← and_imp, mem_product, and_imp, Prod.forall, mem_filter, and_self, and_true, imp_self, implies_true]
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Mul α
s s₁ s₂ t t₁ t₂ : Finset α
a : α × α
x✝¹ : a ∈ s ×ˢ t
b : α × α
x✝ : b ∈ s ×ˢ t
⊢ (fun x => ((x.fst, x.fst), x.snd, x.snd)) a = (fun x => ((x.fst, x.fst), x.snd, x.snd)) b → a = b
[PROOFSTEP]
simp only [Prod.mk.inj_iff, and_self_iff, and_imp]
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Mul α
s s₁ s₂ t t₁ t₂ : Finset α
a : α × α
x✝¹ : a ∈ s ×ˢ t
b : α × α
x✝ : b ∈ s ×ˢ t
⊢ a.fst = b.fst → a.snd = b.snd → a = b
[PROOFSTEP]
exact Prod.ext
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Mul α
s s₁ s₂ t t₁ t₂ : Finset α
⊢ multiplicativeEnergy ∅ t = 0
[PROOFSTEP]
simp [multiplicativeEnergy]
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Mul α
s s₁ s₂ t t₁ t₂ : Finset α
⊢ multiplicativeEnergy s ∅ = 0
[PROOFSTEP]
simp [multiplicativeEnergy]
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Mul α
s s₁ s₂ t t₁ t₂ : Finset α
h : 0 < multiplicativeEnergy s t
H : ¬(Finset.Nonempty s ∧ Finset.Nonempty t)
⊢ False
[PROOFSTEP]
simp_rw [not_and_or, not_nonempty_iff_eq_empty] at H
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Mul α
s s₁ s₂ t t₁ t₂ : Finset α
h : 0 < multiplicativeEnergy s t
H : s = ∅ ∨ t = ∅
⊢ False
[PROOFSTEP]
obtain rfl | rfl := H
[GOAL]
case inl
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Mul α
s₁ s₂ t t₁ t₂ : Finset α
h : 0 < multiplicativeEnergy ∅ t
⊢ False
[PROOFSTEP]
simp [Nat.not_lt_zero] at h
[GOAL]
case inr
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Mul α
s s₁ s₂ t₁ t₂ : Finset α
h : 0 < multiplicativeEnergy s ∅
⊢ False
[PROOFSTEP]
simp [Nat.not_lt_zero] at h
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Mul α
s s₁ s₂ t t₁ t₂ : Finset α
⊢ multiplicativeEnergy s t = 0 ↔ s = ∅ ∨ t = ∅
[PROOFSTEP]
simp [← (Nat.zero_le _).not_gt_iff_eq, not_and_or, imp_iff_or_not, or_comm]
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : CommMonoid α
s t : Finset α
⊢ multiplicativeEnergy s t = multiplicativeEnergy t s
[PROOFSTEP]
rw [multiplicativeEnergy, ← Finset.card_map (Equiv.prodComm _ _).toEmbedding, map_filter]
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : CommMonoid α
s t : Finset α
⊢ card
      (filter ((fun x => x.fst.fst * x.snd.fst = x.fst.snd * x.snd.snd) ∘ ↑(Equiv.prodComm (α × α) (α × α)).symm)
        (map (Equiv.toEmbedding (Equiv.prodComm (α × α) (α × α))) ((s ×ˢ s) ×ˢ t ×ˢ t))) =
    multiplicativeEnergy t s
[PROOFSTEP]
simp [-Finset.card_map, eq_comm, multiplicativeEnergy, mul_comm, map_eq_image, Function.comp]
[GOAL]
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : CommGroup α
inst✝ : Fintype α
s t : Finset α
⊢ multiplicativeEnergy univ t = Fintype.card α * card t ^ 2
[PROOFSTEP]
simp only [multiplicativeEnergy, univ_product_univ, Fintype.card, sq, ← card_product]
[GOAL]
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : CommGroup α
inst✝ : Fintype α
s t : Finset α
⊢ card (filter (fun x => x.fst.fst * x.snd.fst = x.fst.snd * x.snd.snd) (univ ×ˢ t ×ˢ t)) = card (univ ×ˢ t ×ˢ t)
[PROOFSTEP]
let f : α × α × α → (α × α) × α × α := fun x => ((x.1 * x.2.2, x.1 * x.2.1), x.2)
[GOAL]
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : CommGroup α
inst✝ : Fintype α
s t : Finset α
f : α × α × α → (α × α) × α × α := fun x => ((x.fst * x.snd.snd, x.fst * x.snd.fst), x.snd)
⊢ card (filter (fun x => x.fst.fst * x.snd.fst = x.fst.snd * x.snd.snd) (univ ×ˢ t ×ˢ t)) = card (univ ×ˢ t ×ˢ t)
[PROOFSTEP]
have : (↑((univ : Finset α) ×ˢ t ×ˢ t) : Set (α × α × α)).InjOn f :=
  by
  rintro ⟨a₁, b₁, c₁⟩ _ ⟨a₂, b₂, c₂⟩ h₂ h
  simp_rw [Prod.ext_iff] at h
  obtain ⟨h, rfl, rfl⟩ := h
  rw [mul_right_cancel h.1]
[GOAL]
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : CommGroup α
inst✝ : Fintype α
s t : Finset α
f : α × α × α → (α × α) × α × α := fun x => ((x.fst * x.snd.snd, x.fst * x.snd.fst), x.snd)
⊢ Set.InjOn f ↑(univ ×ˢ t ×ˢ t)
[PROOFSTEP]
rintro ⟨a₁, b₁, c₁⟩ _ ⟨a₂, b₂, c₂⟩ h₂ h
[GOAL]
case mk.mk.mk.mk
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : CommGroup α
inst✝ : Fintype α
s t : Finset α
f : α × α × α → (α × α) × α × α := fun x => ((x.fst * x.snd.snd, x.fst * x.snd.fst), x.snd)
a₁ b₁ c₁ : α
a✝ : (a₁, b₁, c₁) ∈ ↑(univ ×ˢ t ×ˢ t)
a₂ b₂ c₂ : α
h₂ : (a₂, b₂, c₂) ∈ ↑(univ ×ˢ t ×ˢ t)
h : f (a₁, b₁, c₁) = f (a₂, b₂, c₂)
⊢ (a₁, b₁, c₁) = (a₂, b₂, c₂)
[PROOFSTEP]
simp_rw [Prod.ext_iff] at h
[GOAL]
case mk.mk.mk.mk
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : CommGroup α
inst✝ : Fintype α
s t : Finset α
f : α × α × α → (α × α) × α × α := fun x => ((x.fst * x.snd.snd, x.fst * x.snd.fst), x.snd)
a₁ b₁ c₁ : α
a✝ : (a₁, b₁, c₁) ∈ ↑(univ ×ˢ t ×ˢ t)
a₂ b₂ c₂ : α
h₂ : (a₂, b₂, c₂) ∈ ↑(univ ×ˢ t ×ˢ t)
h : (a₁ * c₁ = a₂ * c₂ ∧ a₁ * b₁ = a₂ * b₂) ∧ b₁ = b₂ ∧ c₁ = c₂
⊢ (a₁, b₁, c₁) = (a₂, b₂, c₂)
[PROOFSTEP]
obtain ⟨h, rfl, rfl⟩ := h
[GOAL]
case mk.mk.mk.mk.intro.intro
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : CommGroup α
inst✝ : Fintype α
s t : Finset α
f : α × α × α → (α × α) × α × α := fun x => ((x.fst * x.snd.snd, x.fst * x.snd.fst), x.snd)
a₁ b₁ c₁ : α
a✝ : (a₁, b₁, c₁) ∈ ↑(univ ×ˢ t ×ˢ t)
a₂ : α
h₂ : (a₂, b₁, c₁) ∈ ↑(univ ×ˢ t ×ˢ t)
h : a₁ * c₁ = a₂ * c₁ ∧ a₁ * b₁ = a₂ * b₁
⊢ (a₁, b₁, c₁) = (a₂, b₁, c₁)
[PROOFSTEP]
rw [mul_right_cancel h.1]
[GOAL]
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : CommGroup α
inst✝ : Fintype α
s t : Finset α
f : α × α × α → (α × α) × α × α := fun x => ((x.fst * x.snd.snd, x.fst * x.snd.fst), x.snd)
this : Set.InjOn f ↑(univ ×ˢ t ×ˢ t)
⊢ card (filter (fun x => x.fst.fst * x.snd.fst = x.fst.snd * x.snd.snd) (univ ×ˢ t ×ˢ t)) = card (univ ×ˢ t ×ˢ t)
[PROOFSTEP]
rw [← card_image_of_injOn this]
[GOAL]
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : CommGroup α
inst✝ : Fintype α
s t : Finset α
f : α × α × α → (α × α) × α × α := fun x => ((x.fst * x.snd.snd, x.fst * x.snd.fst), x.snd)
this : Set.InjOn f ↑(univ ×ˢ t ×ˢ t)
⊢ card (filter (fun x => x.fst.fst * x.snd.fst = x.fst.snd * x.snd.snd) (univ ×ˢ t ×ˢ t)) =
    card (image f (univ ×ˢ t ×ˢ t))
[PROOFSTEP]
congr with a
[GOAL]
case e_s.a
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : CommGroup α
inst✝ : Fintype α
s t : Finset α
f : α × α × α → (α × α) × α × α := fun x => ((x.fst * x.snd.snd, x.fst * x.snd.fst), x.snd)
this : Set.InjOn f ↑(univ ×ˢ t ×ˢ t)
a : (α × α) × α × α
⊢ a ∈ filter (fun x => x.fst.fst * x.snd.fst = x.fst.snd * x.snd.snd) (univ ×ˢ t ×ˢ t) ↔ a ∈ image f (univ ×ˢ t ×ˢ t)
[PROOFSTEP]
simp only [mem_filter, mem_product, mem_univ, true_and_iff, mem_image, exists_prop, Prod.exists]
[GOAL]
case e_s.a
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : CommGroup α
inst✝ : Fintype α
s t : Finset α
f : α × α × α → (α × α) × α × α := fun x => ((x.fst * x.snd.snd, x.fst * x.snd.fst), x.snd)
this : Set.InjOn f ↑(univ ×ˢ t ×ˢ t)
a : (α × α) × α × α
⊢ (a.snd.fst ∈ t ∧ a.snd.snd ∈ t) ∧ a.fst.fst * a.snd.fst = a.fst.snd * a.snd.snd ↔
    ∃ a_1 a_2 b, (a_2 ∈ t ∧ b ∈ t) ∧ ((a_1 * b, a_1 * a_2), a_2, b) = a
[PROOFSTEP]
refine' ⟨fun h => ⟨a.1.1 * a.2.2⁻¹, _, _, h.1, by simp [mul_right_comm, h.2]⟩, _⟩
[GOAL]
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : CommGroup α
inst✝ : Fintype α
s t : Finset α
f : α × α × α → (α × α) × α × α := fun x => ((x.fst * x.snd.snd, x.fst * x.snd.fst), x.snd)
this : Set.InjOn f ↑(univ ×ˢ t ×ˢ t)
a : (α × α) × α × α
h : (a.snd.fst ∈ t ∧ a.snd.snd ∈ t) ∧ a.fst.fst * a.snd.fst = a.fst.snd * a.snd.snd
⊢ ((a.fst.fst * a.snd.snd⁻¹ * a.snd.snd, a.fst.fst * a.snd.snd⁻¹ * a.snd.fst), a.snd.fst, a.snd.snd) = a
[PROOFSTEP]
simp [mul_right_comm, h.2]
[GOAL]
case e_s.a
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : CommGroup α
inst✝ : Fintype α
s t : Finset α
f : α × α × α → (α × α) × α × α := fun x => ((x.fst * x.snd.snd, x.fst * x.snd.fst), x.snd)
this : Set.InjOn f ↑(univ ×ˢ t ×ˢ t)
a : (α × α) × α × α
⊢ (∃ a_1 a_2 b, (a_2 ∈ t ∧ b ∈ t) ∧ ((a_1 * b, a_1 * a_2), a_2, b) = a) →
    (a.snd.fst ∈ t ∧ a.snd.snd ∈ t) ∧ a.fst.fst * a.snd.fst = a.fst.snd * a.snd.snd
[PROOFSTEP]
rintro ⟨b, c, d, hcd, rfl⟩
[GOAL]
case e_s.a.intro.intro.intro.intro
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : CommGroup α
inst✝ : Fintype α
s t : Finset α
f : α × α × α → (α × α) × α × α := fun x => ((x.fst * x.snd.snd, x.fst * x.snd.fst), x.snd)
this : Set.InjOn f ↑(univ ×ˢ t ×ˢ t)
b c d : α
hcd : c ∈ t ∧ d ∈ t
⊢ (((b * d, b * c), c, d).snd.fst ∈ t ∧ ((b * d, b * c), c, d).snd.snd ∈ t) ∧
    ((b * d, b * c), c, d).fst.fst * ((b * d, b * c), c, d).snd.fst =
      ((b * d, b * c), c, d).fst.snd * ((b * d, b * c), c, d).snd.snd
[PROOFSTEP]
simpa [mul_right_comm]
[GOAL]
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : CommGroup α
inst✝ : Fintype α
s t : Finset α
⊢ multiplicativeEnergy s univ = Fintype.card α * card s ^ 2
[PROOFSTEP]
rw [multiplicativeEnergy_comm, multiplicativeEnergy_univ_left]


[GOAL]
M : Type u_1
inst✝³ : MeasurableSpace M
α : Type u_2
m : MeasurableSpace α
μ : Measure α
f✝ g : α → M
δ : Type u_3
inst✝² : MeasurableSpace δ
inst✝¹ : SemilatticeSup α
inst✝ : MeasurableSup₂ α
f : ℕ → δ → α
n : ℕ
hf : ∀ (k : ℕ), k ≤ n → Measurable (f k)
⊢ Measurable (sup' (range (n + 1)) (_ : Finset.Nonempty (range (n + 1))) f)
[PROOFSTEP]
simp_rw [← Nat.lt_succ_iff] at hf
[GOAL]
M : Type u_1
inst✝³ : MeasurableSpace M
α : Type u_2
m : MeasurableSpace α
μ : Measure α
f✝ g : α → M
δ : Type u_3
inst✝² : MeasurableSpace δ
inst✝¹ : SemilatticeSup α
inst✝ : MeasurableSup₂ α
f : ℕ → δ → α
n : ℕ
hf : ∀ (k : ℕ), k < Nat.succ n → Measurable (f k)
⊢ Measurable (sup' (range (n + 1)) (_ : Finset.Nonempty (range (n + 1))) f)
[PROOFSTEP]
refine' Finset.measurable_sup' _ _
[GOAL]
M : Type u_1
inst✝³ : MeasurableSpace M
α : Type u_2
m : MeasurableSpace α
μ : Measure α
f✝ g : α → M
δ : Type u_3
inst✝² : MeasurableSpace δ
inst✝¹ : SemilatticeSup α
inst✝ : MeasurableSup₂ α
f : ℕ → δ → α
n : ℕ
hf : ∀ (k : ℕ), k < Nat.succ n → Measurable (f k)
⊢ ∀ (n_1 : ℕ), n_1 ∈ range (n + 1) → Measurable (f n_1)
[PROOFSTEP]
simpa [Finset.mem_range]
[GOAL]
M : Type u_1
inst✝³ : MeasurableSpace M
α : Type u_2
m : MeasurableSpace α
μ : Measure α
f✝ g : α → M
δ : Type u_3
inst✝² : MeasurableSpace δ
inst✝¹ : SemilatticeSup α
inst✝ : MeasurableSup₂ α
f : ℕ → δ → α
n : ℕ
hf : ∀ (k : ℕ), k ≤ n → Measurable (f k)
⊢ Measurable fun x => sup' (range (n + 1)) (_ : Finset.Nonempty (range (n + 1))) fun k => f k x
[PROOFSTEP]
convert Finset.measurable_range_sup' hf using 1
[GOAL]
case h.e'_5
M : Type u_1
inst✝³ : MeasurableSpace M
α : Type u_2
m : MeasurableSpace α
μ : Measure α
f✝ g : α → M
δ : Type u_3
inst✝² : MeasurableSpace δ
inst✝¹ : SemilatticeSup α
inst✝ : MeasurableSup₂ α
f : ℕ → δ → α
n : ℕ
hf : ∀ (k : ℕ), k ≤ n → Measurable (f k)
⊢ (fun x => sup' (range (n + 1)) (_ : Finset.Nonempty (range (n + 1))) fun k => f k x) =
    sup' (range (n + 1)) (_ : Finset.Nonempty (range (n + 1))) fun k => f k
[PROOFSTEP]
ext x
[GOAL]
case h.e'_5.h
M : Type u_1
inst✝³ : MeasurableSpace M
α : Type u_2
m : MeasurableSpace α
μ : Measure α
f✝ g : α → M
δ : Type u_3
inst✝² : MeasurableSpace δ
inst✝¹ : SemilatticeSup α
inst✝ : MeasurableSup₂ α
f : ℕ → δ → α
n : ℕ
hf : ∀ (k : ℕ), k ≤ n → Measurable (f k)
x : δ
⊢ (sup' (range (n + 1)) (_ : Finset.Nonempty (range (n + 1))) fun k => f k x) =
    sup' (range (n + 1)) (_ : Finset.Nonempty (range (n + 1))) (fun k => f k) x
[PROOFSTEP]
simp


[GOAL]
V : Type u
G : SimpleGraph V
K L L' M : Set V
⊢ Function.Injective supp
[PROOFSTEP]
refine' ConnectedComponent.ind₂ _
[GOAL]
V : Type u
G : SimpleGraph V
K L L' M : Set V
⊢ ∀ (v w : ↑Kᶜ),
    supp (connectedComponentMk (induce Kᶜ G) v) = supp (connectedComponentMk (induce Kᶜ G) w) →
      connectedComponentMk (induce Kᶜ G) v = connectedComponentMk (induce Kᶜ G) w
[PROOFSTEP]
rintro ⟨v, hv⟩ ⟨w, hw⟩ h
[GOAL]
case mk.mk
V : Type u
G : SimpleGraph V
K L L' M : Set V
v : V
hv : v ∈ Kᶜ
w : V
hw : w ∈ Kᶜ
h :
  supp (connectedComponentMk (induce Kᶜ G) { val := v, property := hv }) =
    supp (connectedComponentMk (induce Kᶜ G) { val := w, property := hw })
⊢ connectedComponentMk (induce Kᶜ G) { val := v, property := hv } =
    connectedComponentMk (induce Kᶜ G) { val := w, property := hw }
[PROOFSTEP]
simp only [Set.ext_iff, ConnectedComponent.eq, Set.mem_setOf_eq, ComponentCompl.supp] at h ⊢
[GOAL]
case mk.mk
V : Type u
G : SimpleGraph V
K L L' M : Set V
v : V
hv : v ∈ Kᶜ
w : V
hw : w ∈ Kᶜ
h :
  ∀ (x : V),
    (∃ h, Reachable (induce Kᶜ G) { val := x, property := (_ : ¬x ∈ K) } { val := v, property := hv }) ↔
      ∃ h, Reachable (induce Kᶜ G) { val := x, property := (_ : ¬x ∈ K) } { val := w, property := hw }
⊢ Reachable (induce Kᶜ G) { val := v, property := hv } { val := w, property := hw }
[PROOFSTEP]
exact ((h v).mp ⟨hv, Reachable.refl _⟩).choose_spec
[GOAL]
V : Type u
G✝ : SimpleGraph V
K L L' M : Set V
G : SimpleGraph V
v w : V
vK : ¬v ∈ K
wK : ¬w ∈ K
a : Adj G v w
⊢ componentComplMk G vK = componentComplMk G wK
[PROOFSTEP]
rw [ConnectedComponent.eq]
[GOAL]
V : Type u
G✝ : SimpleGraph V
K L L' M : Set V
G : SimpleGraph V
v w : V
vK : ¬v ∈ K
wK : ¬w ∈ K
a : Adj G v w
⊢ Reachable (induce Kᶜ G) { val := v, property := vK } { val := w, property := wK }
[PROOFSTEP]
apply Adj.reachable
[GOAL]
case h
V : Type u
G✝ : SimpleGraph V
K L L' M : Set V
G : SimpleGraph V
v w : V
vK : ¬v ∈ K
wK : ¬w ∈ K
a : Adj G v w
⊢ Adj (induce Kᶜ G) { val := v, property := vK } { val := w, property := wK }
[PROOFSTEP]
exact a
[GOAL]
V : Type u
G : SimpleGraph V
K L L' M : Set V
β : Sort u_1
f : ⦃v : V⦄ → ¬v ∈ K → β
h : ∀ ⦃v w : V⦄ (hv : ¬v ∈ K) (hw : ¬w ∈ K), Adj G v w → f hv = f hw
v w : ↑Kᶜ
p : Walk (induce Kᶜ G) v w
⊢ Walk.IsPath p → (fun vv => f (_ : ↑vv ∈ Kᶜ)) v = (fun vv => f (_ : ↑vv ∈ Kᶜ)) w
[PROOFSTEP]
induction' p with _ u v w a q ih
[GOAL]
case nil
V : Type u
G : SimpleGraph V
K L L' M : Set V
β : Sort u_1
f : ⦃v : V⦄ → ¬v ∈ K → β
h : ∀ ⦃v w : V⦄ (hv : ¬v ∈ K) (hw : ¬w ∈ K), Adj G v w → f hv = f hw
v w u✝ : ↑Kᶜ
⊢ Walk.IsPath Walk.nil → (fun vv => f (_ : ↑vv ∈ Kᶜ)) u✝ = (fun vv => f (_ : ↑vv ∈ Kᶜ)) u✝
[PROOFSTEP]
rintro _
[GOAL]
case nil
V : Type u
G : SimpleGraph V
K L L' M : Set V
β : Sort u_1
f : ⦃v : V⦄ → ¬v ∈ K → β
h : ∀ ⦃v w : V⦄ (hv : ¬v ∈ K) (hw : ¬w ∈ K), Adj G v w → f hv = f hw
v w u✝ : ↑Kᶜ
a✝ : Walk.IsPath Walk.nil
⊢ (fun vv => f (_ : ↑vv ∈ Kᶜ)) u✝ = (fun vv => f (_ : ↑vv ∈ Kᶜ)) u✝
[PROOFSTEP]
rfl
[GOAL]
case cons
V : Type u
G : SimpleGraph V
K L L' M : Set V
β : Sort u_1
f : ⦃v : V⦄ → ¬v ∈ K → β
h : ∀ ⦃v w : V⦄ (hv : ¬v ∈ K) (hw : ¬w ∈ K), Adj G v w → f hv = f hw
v✝ w✝ u v w : ↑Kᶜ
a : Adj (induce Kᶜ G) u v
q : Walk (induce Kᶜ G) v w
ih : Walk.IsPath q → (fun vv => f (_ : ↑vv ∈ Kᶜ)) v = (fun vv => f (_ : ↑vv ∈ Kᶜ)) w
⊢ Walk.IsPath (Walk.cons a q) → (fun vv => f (_ : ↑vv ∈ Kᶜ)) u = (fun vv => f (_ : ↑vv ∈ Kᶜ)) w
[PROOFSTEP]
rintro h'
[GOAL]
case cons
V : Type u
G : SimpleGraph V
K L L' M : Set V
β : Sort u_1
f : ⦃v : V⦄ → ¬v ∈ K → β
h : ∀ ⦃v w : V⦄ (hv : ¬v ∈ K) (hw : ¬w ∈ K), Adj G v w → f hv = f hw
v✝ w✝ u v w : ↑Kᶜ
a : Adj (induce Kᶜ G) u v
q : Walk (induce Kᶜ G) v w
ih : Walk.IsPath q → (fun vv => f (_ : ↑vv ∈ Kᶜ)) v = (fun vv => f (_ : ↑vv ∈ Kᶜ)) w
h' : Walk.IsPath (Walk.cons a q)
⊢ (fun vv => f (_ : ↑vv ∈ Kᶜ)) u = (fun vv => f (_ : ↑vv ∈ Kᶜ)) w
[PROOFSTEP]
exact (h u.prop v.prop a).trans (ih h'.of_cons)
[GOAL]
V : Type u
G : SimpleGraph V
K L L' M : Set V
β : ComponentCompl G K → Prop
f : ∀ ⦃v : V⦄ (hv : ¬v ∈ K), β (componentComplMk G hv)
⊢ ∀ (C : ComponentCompl G K), β C
[PROOFSTEP]
apply ConnectedComponent.ind
[GOAL]
case h
V : Type u
G : SimpleGraph V
K L L' M : Set V
β : ComponentCompl G K → Prop
f : ∀ ⦃v : V⦄ (hv : ¬v ∈ K), β (componentComplMk G hv)
⊢ ∀ (v : ↑Kᶜ), β (connectedComponentMk (induce Kᶜ G) v)
[PROOFSTEP]
exact fun ⟨v, vnK⟩ => f vnK
[GOAL]
V : Type u
G : SimpleGraph V
K L L' M : Set V
C : ComponentCompl G K
⊢ Disjoint K ↑C
[PROOFSTEP]
rw [Set.disjoint_iff]
[GOAL]
V : Type u
G : SimpleGraph V
K L L' M : Set V
C : ComponentCompl G K
⊢ K ∩ ↑C ⊆ ∅
[PROOFSTEP]
exact fun v ⟨vK, vC⟩ => vC.choose vK
[GOAL]
V : Type u
G : SimpleGraph V
K L L' M : Set V
⊢ Pairwise fun C D => Disjoint ↑C ↑D
[PROOFSTEP]
rintro C D ne
[GOAL]
V : Type u
G : SimpleGraph V
K L L' M : Set V
C D : ComponentCompl G K
ne : C ≠ D
⊢ Disjoint ↑C ↑D
[PROOFSTEP]
rw [Set.disjoint_iff]
[GOAL]
V : Type u
G : SimpleGraph V
K L L' M : Set V
C D : ComponentCompl G K
ne : C ≠ D
⊢ ↑C ∩ ↑D ⊆ ∅
[PROOFSTEP]
exact fun u ⟨uC, uD⟩ => ne (uC.choose_spec.symm.trans uD.choose_spec)
[GOAL]
V : Type u
G : SimpleGraph V
K L L' M : Set V
C : ComponentCompl G K
c d : V
x✝ : c ∈ C
dnK : ¬d ∈ K
cd : Adj G c d
cnK : ¬c ∈ K
h : componentComplMk G cnK = C
⊢ componentComplMk G dnK = C
[PROOFSTEP]
rw [← h, ConnectedComponent.eq]
[GOAL]
V : Type u
G : SimpleGraph V
K L L' M : Set V
C : ComponentCompl G K
c d : V
x✝ : c ∈ C
dnK : ¬d ∈ K
cd : Adj G c d
cnK : ¬c ∈ K
h : componentComplMk G cnK = C
⊢ Reachable (induce Kᶜ G) { val := d, property := dnK } { val := c, property := cnK }
[PROOFSTEP]
exact Adj.reachable cd.symm
[GOAL]
V : Type u
G : SimpleGraph V
K L L' M : Set V
Gc : Preconnected G
hK : Set.Nonempty K
⊢ ∀ (C : ComponentCompl G K), ∃ ck, ck.fst ∈ C ∧ ck.snd ∈ K ∧ Adj G ck.fst ck.snd
[PROOFSTEP]
refine' ComponentCompl.ind fun v vnK => _
[GOAL]
V : Type u
G : SimpleGraph V
K L L' M : Set V
Gc : Preconnected G
hK : Set.Nonempty K
v : V
vnK : ¬v ∈ K
⊢ ∃ ck, ck.fst ∈ componentComplMk G vnK ∧ ck.snd ∈ K ∧ Adj G ck.fst ck.snd
[PROOFSTEP]
let C : G.ComponentCompl K := G.componentComplMk vnK
[GOAL]
V : Type u
G : SimpleGraph V
K L L' M : Set V
Gc : Preconnected G
hK : Set.Nonempty K
v : V
vnK : ¬v ∈ K
C : ComponentCompl G K := componentComplMk G vnK
⊢ ∃ ck, ck.fst ∈ componentComplMk G vnK ∧ ck.snd ∈ K ∧ Adj G ck.fst ck.snd
[PROOFSTEP]
let dis := Set.disjoint_iff.mp C.disjoint_right
[GOAL]
V : Type u
G : SimpleGraph V
K L L' M : Set V
Gc : Preconnected G
hK : Set.Nonempty K
v : V
vnK : ¬v ∈ K
C : ComponentCompl G K := componentComplMk G vnK
dis : K ∩ ↑C ⊆ ∅ := Iff.mp Set.disjoint_iff (ComponentCompl.disjoint_right C)
⊢ ∃ ck, ck.fst ∈ componentComplMk G vnK ∧ ck.snd ∈ K ∧ Adj G ck.fst ck.snd
[PROOFSTEP]
by_contra' h
[GOAL]
V : Type u
G : SimpleGraph V
K L L' M : Set V
Gc : Preconnected G
hK : Set.Nonempty K
v : V
vnK : ¬v ∈ K
C : ComponentCompl G K := componentComplMk G vnK
dis : K ∩ ↑C ⊆ ∅ := Iff.mp Set.disjoint_iff (ComponentCompl.disjoint_right C)
h : ∀ (ck : V × V), ck.fst ∈ componentComplMk G vnK → ck.snd ∈ K → ¬Adj G ck.fst ck.snd
⊢ False
[PROOFSTEP]
suffices Set.univ = (C : Set V) by exact dis ⟨hK.choose_spec, this ▸ Set.mem_univ hK.some⟩
[GOAL]
V : Type u
G : SimpleGraph V
K L L' M : Set V
Gc : Preconnected G
hK : Set.Nonempty K
v : V
vnK : ¬v ∈ K
C : ComponentCompl G K := componentComplMk G vnK
dis : K ∩ ↑C ⊆ ∅ := Iff.mp Set.disjoint_iff (ComponentCompl.disjoint_right C)
h : ∀ (ck : V × V), ck.fst ∈ componentComplMk G vnK → ck.snd ∈ K → ¬Adj G ck.fst ck.snd
this : Set.univ = ↑C
⊢ False
[PROOFSTEP]
exact dis ⟨hK.choose_spec, this ▸ Set.mem_univ hK.some⟩
[GOAL]
V : Type u
G : SimpleGraph V
K L L' M : Set V
Gc : Preconnected G
hK : Set.Nonempty K
v : V
vnK : ¬v ∈ K
C : ComponentCompl G K := componentComplMk G vnK
dis : K ∩ ↑C ⊆ ∅ := Iff.mp Set.disjoint_iff (ComponentCompl.disjoint_right C)
h : ∀ (ck : V × V), ck.fst ∈ componentComplMk G vnK → ck.snd ∈ K → ¬Adj G ck.fst ck.snd
⊢ Set.univ = ↑C
[PROOFSTEP]
symm
[GOAL]
V : Type u
G : SimpleGraph V
K L L' M : Set V
Gc : Preconnected G
hK : Set.Nonempty K
v : V
vnK : ¬v ∈ K
C : ComponentCompl G K := componentComplMk G vnK
dis : K ∩ ↑C ⊆ ∅ := Iff.mp Set.disjoint_iff (ComponentCompl.disjoint_right C)
h : ∀ (ck : V × V), ck.fst ∈ componentComplMk G vnK → ck.snd ∈ K → ¬Adj G ck.fst ck.snd
⊢ ↑C = Set.univ
[PROOFSTEP]
rw [Set.eq_univ_iff_forall]
[GOAL]
V : Type u
G : SimpleGraph V
K L L' M : Set V
Gc : Preconnected G
hK : Set.Nonempty K
v : V
vnK : ¬v ∈ K
C : ComponentCompl G K := componentComplMk G vnK
dis : K ∩ ↑C ⊆ ∅ := Iff.mp Set.disjoint_iff (ComponentCompl.disjoint_right C)
h : ∀ (ck : V × V), ck.fst ∈ componentComplMk G vnK → ck.snd ∈ K → ¬Adj G ck.fst ck.snd
⊢ ∀ (x : V), x ∈ ↑C
[PROOFSTEP]
rintro u
[GOAL]
V : Type u
G : SimpleGraph V
K L L' M : Set V
Gc : Preconnected G
hK : Set.Nonempty K
v : V
vnK : ¬v ∈ K
C : ComponentCompl G K := componentComplMk G vnK
dis : K ∩ ↑C ⊆ ∅ := Iff.mp Set.disjoint_iff (ComponentCompl.disjoint_right C)
h : ∀ (ck : V × V), ck.fst ∈ componentComplMk G vnK → ck.snd ∈ K → ¬Adj G ck.fst ck.snd
u : V
⊢ u ∈ ↑C
[PROOFSTEP]
by_contra unC
[GOAL]
V : Type u
G : SimpleGraph V
K L L' M : Set V
Gc : Preconnected G
hK : Set.Nonempty K
v : V
vnK : ¬v ∈ K
C : ComponentCompl G K := componentComplMk G vnK
dis : K ∩ ↑C ⊆ ∅ := Iff.mp Set.disjoint_iff (ComponentCompl.disjoint_right C)
h : ∀ (ck : V × V), ck.fst ∈ componentComplMk G vnK → ck.snd ∈ K → ¬Adj G ck.fst ck.snd
u : V
unC : ¬u ∈ ↑C
⊢ False
[PROOFSTEP]
obtain ⟨p⟩ := Gc v u
[GOAL]
case intro
V : Type u
G : SimpleGraph V
K L L' M : Set V
Gc : Preconnected G
hK : Set.Nonempty K
v : V
vnK : ¬v ∈ K
C : ComponentCompl G K := componentComplMk G vnK
dis : K ∩ ↑C ⊆ ∅ := Iff.mp Set.disjoint_iff (ComponentCompl.disjoint_right C)
h : ∀ (ck : V × V), ck.fst ∈ componentComplMk G vnK → ck.snd ∈ K → ¬Adj G ck.fst ck.snd
u : V
unC : ¬u ∈ ↑C
p : Walk G v u
⊢ False
[PROOFSTEP]
obtain ⟨⟨⟨x, y⟩, xy⟩, -, xC, ynC⟩ := p.exists_boundary_dart (C : Set V) (G.componentComplMk_mem vnK) unC
[GOAL]
case intro.intro.mk.mk.intro.intro
V : Type u
G : SimpleGraph V
K L L' M : Set V
Gc : Preconnected G
hK : Set.Nonempty K
v : V
vnK : ¬v ∈ K
C : ComponentCompl G K := componentComplMk G vnK
dis : K ∩ ↑C ⊆ ∅ := Iff.mp Set.disjoint_iff (ComponentCompl.disjoint_right C)
h : ∀ (ck : V × V), ck.fst ∈ componentComplMk G vnK → ck.snd ∈ K → ¬Adj G ck.fst ck.snd
u : V
unC : ¬u ∈ ↑C
p : Walk G v u
x y : V
xy : Adj G (x, y).fst (x, y).snd
xC : { toProd := (x, y), is_adj := xy }.toProd.fst ∈ ↑C
ynC : ¬{ toProd := (x, y), is_adj := xy }.toProd.snd ∈ ↑C
⊢ False
[PROOFSTEP]
exact ynC (mem_of_adj x y xC (fun yK : y ∈ K => h ⟨x, y⟩ xC yK xy) xy)
[GOAL]
V : Type u
G : SimpleGraph V
K L L' M : Set V
C : ComponentCompl G L
h : K ⊆ L
⊢ ↑C ⊆ ↑(hom h C)
[PROOFSTEP]
rintro c ⟨cL, rfl⟩
[GOAL]
case intro
V : Type u
G : SimpleGraph V
K L L' M : Set V
h : K ⊆ L
c : V
cL : ¬c ∈ L
⊢ c ∈ ↑(hom h (componentComplMk G cL))
[PROOFSTEP]
exact ⟨fun h' => cL (h h'), rfl⟩
[GOAL]
V : Type u
G : SimpleGraph V
K L L' M : Set V
C : ComponentCompl G L
h : K ⊆ L
D : ComponentCompl G K
⊢ hom h C = D ↔ ¬Disjoint ↑C ↑D
[PROOFSTEP]
rw [Set.not_disjoint_iff]
[GOAL]
V : Type u
G : SimpleGraph V
K L L' M : Set V
C : ComponentCompl G L
h : K ⊆ L
D : ComponentCompl G K
⊢ hom h C = D ↔ ∃ x, x ∈ ↑C ∧ x ∈ ↑D
[PROOFSTEP]
constructor
[GOAL]
case mp
V : Type u
G : SimpleGraph V
K L L' M : Set V
C : ComponentCompl G L
h : K ⊆ L
D : ComponentCompl G K
⊢ hom h C = D → ∃ x, x ∈ ↑C ∧ x ∈ ↑D
[PROOFSTEP]
rintro rfl
[GOAL]
case mp
V : Type u
G : SimpleGraph V
K L L' M : Set V
C : ComponentCompl G L
h : K ⊆ L
⊢ ∃ x, x ∈ ↑C ∧ x ∈ ↑(hom h C)
[PROOFSTEP]
refine C.ind fun x xnL => ?_
[GOAL]
case mp
V : Type u
G : SimpleGraph V
K L L' M : Set V
C : ComponentCompl G L
h : K ⊆ L
x : V
xnL : ¬x ∈ L
⊢ ∃ x_1, x_1 ∈ ↑(componentComplMk G xnL) ∧ x_1 ∈ ↑(hom h (componentComplMk G xnL))
[PROOFSTEP]
exact ⟨x, ⟨xnL, rfl⟩, ⟨fun xK => xnL (h xK), rfl⟩⟩
[GOAL]
case mpr
V : Type u
G : SimpleGraph V
K L L' M : Set V
C : ComponentCompl G L
h : K ⊆ L
D : ComponentCompl G K
⊢ (∃ x, x ∈ ↑C ∧ x ∈ ↑D) → hom h C = D
[PROOFSTEP]
refine C.ind fun x xnL => ?_
[GOAL]
case mpr
V : Type u
G : SimpleGraph V
K L L' M : Set V
C : ComponentCompl G L
h : K ⊆ L
D : ComponentCompl G K
x : V
xnL : ¬x ∈ L
⊢ (∃ x_1, x_1 ∈ ↑(componentComplMk G xnL) ∧ x_1 ∈ ↑D) → hom h (componentComplMk G xnL) = D
[PROOFSTEP]
rintro ⟨x, ⟨_, e₁⟩, _, rfl⟩
[GOAL]
case mpr.intro.intro.intro.intro
V : Type u
G : SimpleGraph V
K L L' M : Set V
C : ComponentCompl G L
h : K ⊆ L
x✝ : V
xnL : ¬x✝ ∈ L
x : V
w✝¹ : ¬x ∈ L
e₁ : componentComplMk G w✝¹ = componentComplMk G xnL
w✝ : ¬x ∈ K
⊢ hom h (componentComplMk G xnL) = componentComplMk G w✝
[PROOFSTEP]
rw [← e₁]
[GOAL]
case mpr.intro.intro.intro.intro
V : Type u
G : SimpleGraph V
K L L' M : Set V
C : ComponentCompl G L
h : K ⊆ L
x✝ : V
xnL : ¬x✝ ∈ L
x : V
w✝¹ : ¬x ∈ L
e₁ : componentComplMk G w✝¹ = componentComplMk G xnL
w✝ : ¬x ∈ K
⊢ hom h (componentComplMk G w✝¹) = componentComplMk G w✝
[PROOFSTEP]
rfl
[GOAL]
V : Type u
G : SimpleGraph V
K L L' M : Set V
C : ComponentCompl G L
⊢ hom (_ : L ⊆ L) C = C
[PROOFSTEP]
change C.map _ = C
[GOAL]
V : Type u
G : SimpleGraph V
K L L' M : Set V
C : ComponentCompl G L
⊢ ConnectedComponent.map (induceHom Hom.id (_ : Lᶜ ⊆ Lᶜ)) C = C
[PROOFSTEP]
erw [induceHom_id G Lᶜ, ConnectedComponent.map_id]
[GOAL]
V : Type u
G : SimpleGraph V
K L L' M : Set V
C : ComponentCompl G L
h : K ⊆ L
h' : M ⊆ K
⊢ hom (_ : M ⊆ L) C = hom h' (hom h C)
[PROOFSTEP]
change C.map _ = (C.map _).map _
[GOAL]
V : Type u
G : SimpleGraph V
K L L' M : Set V
C : ComponentCompl G L
h : K ⊆ L
h' : M ⊆ K
⊢ ConnectedComponent.map (induceHom Hom.id (_ : Lᶜ ⊆ Mᶜ)) C =
    ConnectedComponent.map (induceHom Hom.id (_ : Kᶜ ⊆ Mᶜ)) (ConnectedComponent.map (induceHom Hom.id (_ : Lᶜ ⊆ Kᶜ)) C)
[PROOFSTEP]
erw [ConnectedComponent.map_comp, induceHom_comp]
[GOAL]
V : Type u
G : SimpleGraph V
K L L' M : Set V
C : ComponentCompl G L
h : K ⊆ L
h' : M ⊆ K
⊢ ConnectedComponent.map (induceHom Hom.id (_ : Lᶜ ⊆ Mᶜ)) C =
    ConnectedComponent.map (induceHom (Hom.comp Hom.id Hom.id) (_ : Set.MapsTo (↑Hom.id ∘ fun x => ↑Hom.id x) Lᶜ Mᶜ)) C
[PROOFSTEP]
rfl
[GOAL]
V : Type u
G : SimpleGraph V
K✝ L L' M : Set V
K : Finset V
C : ComponentCompl G ↑K
⊢ Set.Infinite (supp C) ↔ ∀ (L : Finset V) (h : K ⊆ L), ∃ D, hom h D = C
[PROOFSTEP]
classical
constructor
· rintro Cinf L h
  obtain ⟨v, ⟨vK, rfl⟩, vL⟩ := Set.Infinite.nonempty (Set.Infinite.diff Cinf L.finite_toSet)
  exact ⟨componentComplMk _ vL, rfl⟩
· rintro h Cfin
  obtain ⟨D, e⟩ := h (K ∪ Cfin.toFinset) (Finset.subset_union_left K Cfin.toFinset)
  obtain ⟨v, vD⟩ := D.nonempty
  let Ddis := D.disjoint_right
  simp_rw [Finset.coe_union, Set.Finite.coe_toFinset, Set.disjoint_union_left, Set.disjoint_iff] at Ddis
  exact Ddis.right ⟨(ComponentCompl.hom_eq_iff_le _ _ _).mp e vD, vD⟩
[GOAL]
V : Type u
G : SimpleGraph V
K✝ L L' M : Set V
K : Finset V
C : ComponentCompl G ↑K
⊢ Set.Infinite (supp C) ↔ ∀ (L : Finset V) (h : K ⊆ L), ∃ D, hom h D = C
[PROOFSTEP]
constructor
[GOAL]
case mp
V : Type u
G : SimpleGraph V
K✝ L L' M : Set V
K : Finset V
C : ComponentCompl G ↑K
⊢ Set.Infinite (supp C) → ∀ (L : Finset V) (h : K ⊆ L), ∃ D, hom h D = C
[PROOFSTEP]
rintro Cinf L h
[GOAL]
case mp
V : Type u
G : SimpleGraph V
K✝ L✝ L' M : Set V
K : Finset V
C : ComponentCompl G ↑K
Cinf : Set.Infinite (supp C)
L : Finset V
h : K ⊆ L
⊢ ∃ D, hom h D = C
[PROOFSTEP]
obtain ⟨v, ⟨vK, rfl⟩, vL⟩ := Set.Infinite.nonempty (Set.Infinite.diff Cinf L.finite_toSet)
[GOAL]
case mp.intro.intro.intro
V : Type u
G : SimpleGraph V
K✝ L✝ L' M : Set V
K L : Finset V
h : K ⊆ L
v : V
vL : ¬v ∈ ↑L
vK : ¬v ∈ ↑K
Cinf : Set.Infinite (supp (componentComplMk G vK))
⊢ ∃ D, hom h D = componentComplMk G vK
[PROOFSTEP]
exact ⟨componentComplMk _ vL, rfl⟩
[GOAL]
case mpr
V : Type u
G : SimpleGraph V
K✝ L L' M : Set V
K : Finset V
C : ComponentCompl G ↑K
⊢ (∀ (L : Finset V) (h : K ⊆ L), ∃ D, hom h D = C) → Set.Infinite (supp C)
[PROOFSTEP]
rintro h Cfin
[GOAL]
case mpr
V : Type u
G : SimpleGraph V
K✝ L L' M : Set V
K : Finset V
C : ComponentCompl G ↑K
h : ∀ (L : Finset V) (h : K ⊆ L), ∃ D, hom h D = C
Cfin : Set.Finite (supp C)
⊢ False
[PROOFSTEP]
obtain ⟨D, e⟩ := h (K ∪ Cfin.toFinset) (Finset.subset_union_left K Cfin.toFinset)
[GOAL]
case mpr.intro
V : Type u
G : SimpleGraph V
K✝ L L' M : Set V
K : Finset V
C : ComponentCompl G ↑K
h : ∀ (L : Finset V) (h : K ⊆ L), ∃ D, hom h D = C
Cfin : Set.Finite (supp C)
D : ComponentCompl G ↑(K ∪ Set.Finite.toFinset Cfin)
e : hom (_ : K ⊆ K ∪ Set.Finite.toFinset Cfin) D = C
⊢ False
[PROOFSTEP]
obtain ⟨v, vD⟩ := D.nonempty
[GOAL]
case mpr.intro.intro
V : Type u
G : SimpleGraph V
K✝ L L' M : Set V
K : Finset V
C : ComponentCompl G ↑K
h : ∀ (L : Finset V) (h : K ⊆ L), ∃ D, hom h D = C
Cfin : Set.Finite (supp C)
D : ComponentCompl G ↑(K ∪ Set.Finite.toFinset Cfin)
e : hom (_ : K ⊆ K ∪ Set.Finite.toFinset Cfin) D = C
v : V
vD : v ∈ ↑D
⊢ False
[PROOFSTEP]
let Ddis := D.disjoint_right
[GOAL]
case mpr.intro.intro
V : Type u
G : SimpleGraph V
K✝ L L' M : Set V
K : Finset V
C : ComponentCompl G ↑K
h : ∀ (L : Finset V) (h : K ⊆ L), ∃ D, hom h D = C
Cfin : Set.Finite (supp C)
D : ComponentCompl G ↑(K ∪ Set.Finite.toFinset Cfin)
e : hom (_ : K ⊆ K ∪ Set.Finite.toFinset Cfin) D = C
v : V
vD : v ∈ ↑D
Ddis : Disjoint ↑(K ∪ Set.Finite.toFinset Cfin) ↑D := ComponentCompl.disjoint_right D
⊢ False
[PROOFSTEP]
simp_rw [Finset.coe_union, Set.Finite.coe_toFinset, Set.disjoint_union_left, Set.disjoint_iff] at Ddis
[GOAL]
case mpr.intro.intro
V : Type u
G : SimpleGraph V
K✝ L L' M : Set V
K : Finset V
C : ComponentCompl G ↑K
h : ∀ (L : Finset V) (h : K ⊆ L), ∃ D, hom h D = C
Cfin : Set.Finite (supp C)
D : ComponentCompl G ↑(K ∪ Set.Finite.toFinset Cfin)
e : hom (_ : K ⊆ K ∪ Set.Finite.toFinset Cfin) D = C
v : V
vD : v ∈ ↑D
Ddis : ↑K ∩ ↑D ⊆ ∅ ∧ supp C ∩ ↑D ⊆ ∅
⊢ False
[PROOFSTEP]
exact Ddis.right ⟨(ComponentCompl.hom_eq_iff_le _ _ _).mp e vD, vD⟩
[GOAL]
V : Type u
G : SimpleGraph V
K✝ L L' M : Set V
inst✝ : LocallyFinite G
Gpc : Fact (Preconnected G)
K : Finset V
⊢ Finite (ComponentCompl G ↑K)
[PROOFSTEP]
classical
rcases K.eq_empty_or_nonempty with rfl | h
· dsimp [ComponentCompl]
  rw [Finset.coe_empty, Set.compl_empty]
  have := Gpc.out.subsingleton_connectedComponent
  exact Finite.of_equiv _ (induceUnivIso G).connectedComponentEquiv.symm
· let touch (C : G.ComponentCompl K) : {v : V | ∃ k : V, k ∈ K ∧ G.Adj k v} :=
    let p := C.exists_adj_boundary_pair Gpc.out h
    ⟨p.choose.1, p.choose.2, p.choose_spec.2.1, p.choose_spec.2.2.symm⟩
      -- `touch` is injective
  have touch_inj : touch.Injective := fun C D h' =>
    ComponentCompl.pairwise_disjoint.eq
      (Set.not_disjoint_iff.mpr
        ⟨touch C, (C.exists_adj_boundary_pair Gpc.out h).choose_spec.1,
          h'.symm ▸ (D.exists_adj_boundary_pair Gpc.out h).choose_spec.1⟩)
        -- `touch` has finite range
  have : Finite (Set.range touch) :=
    by
    refine @Subtype.finite _ (Set.Finite.to_subtype ?_) _
    apply Set.Finite.ofFinset (K.biUnion (fun v => G.neighborFinset v))
    simp only [Finset.mem_biUnion, mem_neighborFinset, Set.mem_setOf_eq, implies_true]
      -- hence `touch` has a finite domain
  apply Finite.of_injective_finite_range touch_inj
[GOAL]
V : Type u
G : SimpleGraph V
K✝ L L' M : Set V
inst✝ : LocallyFinite G
Gpc : Fact (Preconnected G)
K : Finset V
⊢ Finite (ComponentCompl G ↑K)
[PROOFSTEP]
rcases K.eq_empty_or_nonempty with rfl | h
[GOAL]
case inl
V : Type u
G : SimpleGraph V
K L L' M : Set V
inst✝ : LocallyFinite G
Gpc : Fact (Preconnected G)
⊢ Finite (ComponentCompl G ↑∅)
[PROOFSTEP]
dsimp [ComponentCompl]
[GOAL]
case inl
V : Type u
G : SimpleGraph V
K L L' M : Set V
inst✝ : LocallyFinite G
Gpc : Fact (Preconnected G)
⊢ Finite (ConnectedComponent (induce (↑∅)ᶜ G))
[PROOFSTEP]
rw [Finset.coe_empty, Set.compl_empty]
[GOAL]
case inl
V : Type u
G : SimpleGraph V
K L L' M : Set V
inst✝ : LocallyFinite G
Gpc : Fact (Preconnected G)
⊢ Finite (ConnectedComponent (induce Set.univ G))
[PROOFSTEP]
have := Gpc.out.subsingleton_connectedComponent
[GOAL]
case inl
V : Type u
G : SimpleGraph V
K L L' M : Set V
inst✝ : LocallyFinite G
Gpc : Fact (Preconnected G)
this : Subsingleton (ConnectedComponent G)
⊢ Finite (ConnectedComponent (induce Set.univ G))
[PROOFSTEP]
exact Finite.of_equiv _ (induceUnivIso G).connectedComponentEquiv.symm
[GOAL]
case inr
V : Type u
G : SimpleGraph V
K✝ L L' M : Set V
inst✝ : LocallyFinite G
Gpc : Fact (Preconnected G)
K : Finset V
h : Finset.Nonempty K
⊢ Finite (ComponentCompl G ↑K)
[PROOFSTEP]
let touch (C : G.ComponentCompl K) : {v : V | ∃ k : V, k ∈ K ∧ G.Adj k v} :=
  let p := C.exists_adj_boundary_pair Gpc.out h
  ⟨p.choose.1, p.choose.2, p.choose_spec.2.1, p.choose_spec.2.2.symm⟩
    -- `touch` is injective
[GOAL]
case inr
V : Type u
G : SimpleGraph V
K✝ L L' M : Set V
inst✝ : LocallyFinite G
Gpc : Fact (Preconnected G)
K : Finset V
h : Finset.Nonempty K
touch : ComponentCompl G ↑K → ↑{v | ∃ k, k ∈ K ∧ Adj G k v} :=
  fun C =>
    let p := (_ : ∃ ck, ck.fst ∈ C ∧ (ck.snd ∈ fun x => x ∈ K.val) ∧ Adj G ck.fst ck.snd);
    { val := (Exists.choose p).fst, property := (_ : ∃ k, k ∈ K ∧ Adj G k (Exists.choose p).fst) }
⊢ Finite (ComponentCompl G ↑K)
[PROOFSTEP]
have touch_inj : touch.Injective := fun C D h' =>
  ComponentCompl.pairwise_disjoint.eq
    (Set.not_disjoint_iff.mpr
      ⟨touch C, (C.exists_adj_boundary_pair Gpc.out h).choose_spec.1,
        h'.symm ▸ (D.exists_adj_boundary_pair Gpc.out h).choose_spec.1⟩)
      -- `touch` has finite range
[GOAL]
case inr
V : Type u
G : SimpleGraph V
K✝ L L' M : Set V
inst✝ : LocallyFinite G
Gpc : Fact (Preconnected G)
K : Finset V
h : Finset.Nonempty K
touch : ComponentCompl G ↑K → ↑{v | ∃ k, k ∈ K ∧ Adj G k v} :=
  fun C =>
    let p := (_ : ∃ ck, ck.fst ∈ C ∧ (ck.snd ∈ fun x => x ∈ K.val) ∧ Adj G ck.fst ck.snd);
    { val := (Exists.choose p).fst, property := (_ : ∃ k, k ∈ K ∧ Adj G k (Exists.choose p).fst) }
touch_inj : Function.Injective touch
⊢ Finite (ComponentCompl G ↑K)
[PROOFSTEP]
have : Finite (Set.range touch) :=
  by
  refine @Subtype.finite _ (Set.Finite.to_subtype ?_) _
  apply Set.Finite.ofFinset (K.biUnion (fun v => G.neighborFinset v))
  simp only [Finset.mem_biUnion, mem_neighborFinset, Set.mem_setOf_eq, implies_true]
    -- hence `touch` has a finite domain
[GOAL]
V : Type u
G : SimpleGraph V
K✝ L L' M : Set V
inst✝ : LocallyFinite G
Gpc : Fact (Preconnected G)
K : Finset V
h : Finset.Nonempty K
touch : ComponentCompl G ↑K → ↑{v | ∃ k, k ∈ K ∧ Adj G k v} :=
  fun C =>
    let p := (_ : ∃ ck, ck.fst ∈ C ∧ (ck.snd ∈ fun x => x ∈ K.val) ∧ Adj G ck.fst ck.snd);
    { val := (Exists.choose p).fst, property := (_ : ∃ k, k ∈ K ∧ Adj G k (Exists.choose p).fst) }
touch_inj : Function.Injective touch
⊢ Finite ↑(Set.range touch)
[PROOFSTEP]
refine @Subtype.finite _ (Set.Finite.to_subtype ?_) _
[GOAL]
V : Type u
G : SimpleGraph V
K✝ L L' M : Set V
inst✝ : LocallyFinite G
Gpc : Fact (Preconnected G)
K : Finset V
h : Finset.Nonempty K
touch : ComponentCompl G ↑K → ↑{v | ∃ k, k ∈ K ∧ Adj G k v} :=
  fun C =>
    let p := (_ : ∃ ck, ck.fst ∈ C ∧ (ck.snd ∈ fun x => x ∈ K.val) ∧ Adj G ck.fst ck.snd);
    { val := (Exists.choose p).fst, property := (_ : ∃ k, k ∈ K ∧ Adj G k (Exists.choose p).fst) }
touch_inj : Function.Injective touch
⊢ Set.Finite {v | ∃ k, k ∈ K ∧ Adj G k v}
[PROOFSTEP]
apply Set.Finite.ofFinset (K.biUnion (fun v => G.neighborFinset v))
[GOAL]
V : Type u
G : SimpleGraph V
K✝ L L' M : Set V
inst✝ : LocallyFinite G
Gpc : Fact (Preconnected G)
K : Finset V
h : Finset.Nonempty K
touch : ComponentCompl G ↑K → ↑{v | ∃ k, k ∈ K ∧ Adj G k v} :=
  fun C =>
    let p := (_ : ∃ ck, ck.fst ∈ C ∧ (ck.snd ∈ fun x => x ∈ K.val) ∧ Adj G ck.fst ck.snd);
    { val := (Exists.choose p).fst, property := (_ : ∃ k, k ∈ K ∧ Adj G k (Exists.choose p).fst) }
touch_inj : Function.Injective touch
⊢ ∀ (x : V), (x ∈ Finset.biUnion K fun v => neighborFinset G v) ↔ x ∈ {v | ∃ k, k ∈ K ∧ Adj G k v}
[PROOFSTEP]
simp only [Finset.mem_biUnion, mem_neighborFinset, Set.mem_setOf_eq, implies_true]
  -- hence `touch` has a finite domain
[GOAL]
case inr
V : Type u
G : SimpleGraph V
K✝ L L' M : Set V
inst✝ : LocallyFinite G
Gpc : Fact (Preconnected G)
K : Finset V
h : Finset.Nonempty K
touch : ComponentCompl G ↑K → ↑{v | ∃ k, k ∈ K ∧ Adj G k v} :=
  fun C =>
    let p := (_ : ∃ ck, ck.fst ∈ C ∧ (ck.snd ∈ fun x => x ∈ K.val) ∧ Adj G ck.fst ck.snd);
    { val := (Exists.choose p).fst, property := (_ : ∃ k, k ∈ K ∧ Adj G k (Exists.choose p).fst) }
touch_inj : Function.Injective touch
this : Finite ↑(Set.range touch)
⊢ Finite (ComponentCompl G ↑K)
[PROOFSTEP]
apply Finite.of_injective_finite_range touch_inj
[GOAL]
V : Type u
G : SimpleGraph V
K✝ L✝ L' M : Set V
s : (j : (Finset V)ᵒᵖ) → (componentComplFunctor G).obj j
sec : s ∈ SimpleGraph.end G
K L : (Finset V)ᵒᵖ
h : L ⟶ K
v : V
vnL : ¬v ∈ L.unop
hs : s L = componentComplMk G vnL
⊢ s K = componentComplMk G (_ : ¬v ∈ fun a => a ∈ K.unop.val)
[PROOFSTEP]
rw [← sec h, hs]
[GOAL]
V : Type u
G : SimpleGraph V
K✝ L✝ L' M : Set V
s : (j : (Finset V)ᵒᵖ) → (componentComplFunctor G).obj j
sec : s ∈ SimpleGraph.end G
K L : (Finset V)ᵒᵖ
h : L ⟶ K
v : V
vnL : ¬v ∈ L.unop
hs : s L = componentComplMk G vnL
⊢ (componentComplFunctor G).map h (componentComplMk G vnL) = componentComplMk G (_ : ¬v ∈ fun a => a ∈ K.unop.val)
[PROOFSTEP]
apply ComponentCompl.hom_mk _ (le_of_op_hom h : _ ⊆ _)
[GOAL]
V : Type u
G : SimpleGraph V
K✝ L L' M : Set V
K : (Finset V)ᵒᵖ
C : (componentComplFunctor G).obj K
⊢ Set.Infinite (ComponentCompl.supp C) ↔ C ∈ Functor.eventualRange (componentComplFunctor G) K
[PROOFSTEP]
simp only [C.infinite_iff_in_all_ranges, CategoryTheory.Functor.eventualRange, Set.mem_iInter, Set.mem_range,
  componentComplFunctor_map]
[GOAL]
V : Type u
G : SimpleGraph V
K✝ L L' M : Set V
K : (Finset V)ᵒᵖ
C : (componentComplFunctor G).obj K
⊢ (∀ (L : Finset V) (h : K.unop ⊆ L), ∃ D, ComponentCompl.hom h D = C) ↔
    ∀ (i : (Finset V)ᵒᵖ) (i_1 : i ⟶ K), ∃ y, ComponentCompl.hom (_ : K.unop ≤ i.unop) y = C
[PROOFSTEP]
exact ⟨fun h Lop KL => h Lop.unop (le_of_op_hom KL), fun h L KL => h (Opposite.op L) (opHomOfLE KL)⟩


[GOAL]
⊢ Tendsto (fun n => ↑(numDerangements n) / ↑(Nat.factorial n)) atTop (𝓝 (Real.exp (-1)))
[PROOFSTEP]
let s : ℕ → ℝ := fun n => ∑ k in Finset.range n, (-1 : ℝ) ^ k / k.factorial
[GOAL]
s : ℕ → ℝ := fun n => ∑ k in Finset.range n, (-1) ^ k / ↑(Nat.factorial k)
⊢ Tendsto (fun n => ↑(numDerangements n) / ↑(Nat.factorial n)) atTop (𝓝 (Real.exp (-1)))
[PROOFSTEP]
suffices ∀ n : ℕ, (numDerangements n : ℝ) / n.factorial = s (n + 1)
  by
  simp_rw [this]
    -- shift the function by 1, and then use the fact that the partial sums
        -- converge to the infinite sum
  rw [tendsto_add_atTop_iff_nat (f := fun n => ∑ k in Finset.range n, (-1 : ℝ) ^ k / k.factorial) 1]
  apply HasSum.tendsto_sum_nat
  rw [Real.exp_eq_exp_ℝ]
  exact expSeries_div_hasSum_exp ℝ (-1 : ℝ)
[GOAL]
s : ℕ → ℝ := fun n => ∑ k in Finset.range n, (-1) ^ k / ↑(Nat.factorial k)
this : ∀ (n : ℕ), ↑(numDerangements n) / ↑(Nat.factorial n) = s (n + 1)
⊢ Tendsto (fun n => ↑(numDerangements n) / ↑(Nat.factorial n)) atTop (𝓝 (Real.exp (-1)))
[PROOFSTEP]
simp_rw [this]
  -- shift the function by 1, and then use the fact that the partial sums
      -- converge to the infinite sum
[GOAL]
s : ℕ → ℝ := fun n => ∑ k in Finset.range n, (-1) ^ k / ↑(Nat.factorial k)
this : ∀ (n : ℕ), ↑(numDerangements n) / ↑(Nat.factorial n) = s (n + 1)
⊢ Tendsto (fun n => ∑ k in Finset.range (n + 1), (-1) ^ k / ↑(Nat.factorial k)) atTop (𝓝 (Real.exp (-1)))
[PROOFSTEP]
rw [tendsto_add_atTop_iff_nat (f := fun n => ∑ k in Finset.range n, (-1 : ℝ) ^ k / k.factorial) 1]
[GOAL]
s : ℕ → ℝ := fun n => ∑ k in Finset.range n, (-1) ^ k / ↑(Nat.factorial k)
this : ∀ (n : ℕ), ↑(numDerangements n) / ↑(Nat.factorial n) = s (n + 1)
⊢ Tendsto (fun n => ∑ k in Finset.range n, (-1) ^ k / ↑(Nat.factorial k)) atTop (𝓝 (Real.exp (-1)))
[PROOFSTEP]
apply HasSum.tendsto_sum_nat
[GOAL]
case h
s : ℕ → ℝ := fun n => ∑ k in Finset.range n, (-1) ^ k / ↑(Nat.factorial k)
this : ∀ (n : ℕ), ↑(numDerangements n) / ↑(Nat.factorial n) = s (n + 1)
⊢ HasSum (fun i => (-1) ^ i / ↑(Nat.factorial i)) (Real.exp (-1))
[PROOFSTEP]
rw [Real.exp_eq_exp_ℝ]
[GOAL]
case h
s : ℕ → ℝ := fun n => ∑ k in Finset.range n, (-1) ^ k / ↑(Nat.factorial k)
this : ∀ (n : ℕ), ↑(numDerangements n) / ↑(Nat.factorial n) = s (n + 1)
⊢ HasSum (fun i => (-1) ^ i / ↑(Nat.factorial i)) (exp ℝ (-1))
[PROOFSTEP]
exact expSeries_div_hasSum_exp ℝ (-1 : ℝ)
[GOAL]
s : ℕ → ℝ := fun n => ∑ k in Finset.range n, (-1) ^ k / ↑(Nat.factorial k)
⊢ ∀ (n : ℕ), ↑(numDerangements n) / ↑(Nat.factorial n) = s (n + 1)
[PROOFSTEP]
intro n
[GOAL]
s : ℕ → ℝ := fun n => ∑ k in Finset.range n, (-1) ^ k / ↑(Nat.factorial k)
n : ℕ
⊢ ↑(numDerangements n) / ↑(Nat.factorial n) = s (n + 1)
[PROOFSTEP]
rw [← Int.cast_ofNat, numDerangements_sum]
[GOAL]
s : ℕ → ℝ := fun n => ∑ k in Finset.range n, (-1) ^ k / ↑(Nat.factorial k)
n : ℕ
⊢ ↑(∑ k in Finset.range (n + 1), (-1) ^ k * ↑(Nat.ascFactorial k (n - k))) / ↑(Nat.factorial n) = s (n + 1)
[PROOFSTEP]
push_cast
[GOAL]
s : ℕ → ℝ := fun n => ∑ k in Finset.range n, (-1) ^ k / ↑(Nat.factorial k)
n : ℕ
⊢ (∑ x in Finset.range (n + 1), (-1) ^ x * ↑(Nat.ascFactorial x (n - x))) / ↑(Nat.factorial n) =
    ∑ k in Finset.range (n + 1), (-1) ^ k / ↑(Nat.factorial k)
[PROOFSTEP]
rw [Finset.sum_div]
  -- get down to individual terms
[GOAL]
s : ℕ → ℝ := fun n => ∑ k in Finset.range n, (-1) ^ k / ↑(Nat.factorial k)
n : ℕ
⊢ ∑ x in Finset.range (n + 1), (-1) ^ x * ↑(Nat.ascFactorial x (n - x)) / ↑(Nat.factorial n) =
    ∑ k in Finset.range (n + 1), (-1) ^ k / ↑(Nat.factorial k)
[PROOFSTEP]
refine' Finset.sum_congr (refl _) _
[GOAL]
s : ℕ → ℝ := fun n => ∑ k in Finset.range n, (-1) ^ k / ↑(Nat.factorial k)
n : ℕ
⊢ ∀ (x : ℕ),
    x ∈ Finset.range (n + 1) →
      (-1) ^ x * ↑(Nat.ascFactorial x (n - x)) / ↑(Nat.factorial n) = (-1) ^ x / ↑(Nat.factorial x)
[PROOFSTEP]
intro k hk
[GOAL]
s : ℕ → ℝ := fun n => ∑ k in Finset.range n, (-1) ^ k / ↑(Nat.factorial k)
n k : ℕ
hk : k ∈ Finset.range (n + 1)
⊢ (-1) ^ k * ↑(Nat.ascFactorial k (n - k)) / ↑(Nat.factorial n) = (-1) ^ k / ↑(Nat.factorial k)
[PROOFSTEP]
have h_le : k ≤ n := Finset.mem_range_succ_iff.mp hk
[GOAL]
s : ℕ → ℝ := fun n => ∑ k in Finset.range n, (-1) ^ k / ↑(Nat.factorial k)
n k : ℕ
hk : k ∈ Finset.range (n + 1)
h_le : k ≤ n
⊢ (-1) ^ k * ↑(Nat.ascFactorial k (n - k)) / ↑(Nat.factorial n) = (-1) ^ k / ↑(Nat.factorial k)
[PROOFSTEP]
rw [Nat.ascFactorial_eq_div, add_tsub_cancel_of_le h_le]
[GOAL]
s : ℕ → ℝ := fun n => ∑ k in Finset.range n, (-1) ^ k / ↑(Nat.factorial k)
n k : ℕ
hk : k ∈ Finset.range (n + 1)
h_le : k ≤ n
⊢ (-1) ^ k * ↑(Nat.factorial n / Nat.factorial k) / ↑(Nat.factorial n) = (-1) ^ k / ↑(Nat.factorial k)
[PROOFSTEP]
push_cast [Nat.factorial_dvd_factorial h_le]
[GOAL]
s : ℕ → ℝ := fun n => ∑ k in Finset.range n, (-1) ^ k / ↑(Nat.factorial k)
n k : ℕ
hk : k ∈ Finset.range (n + 1)
h_le : k ≤ n
⊢ (-1) ^ k * (↑(Nat.factorial n) / ↑(Nat.factorial k)) / ↑(Nat.factorial n) = (-1) ^ k / ↑(Nat.factorial k)
[PROOFSTEP]
field_simp [Nat.factorial_ne_zero]
[GOAL]
s : ℕ → ℝ := fun n => ∑ k in Finset.range n, (-1) ^ k / ↑(Nat.factorial k)
n k : ℕ
hk : k ∈ Finset.range (n + 1)
h_le : k ≤ n
⊢ (-1) ^ k * ↑(Nat.factorial n) * ↑(Nat.factorial k) = (-1) ^ k * (↑(Nat.factorial k) * ↑(Nat.factorial n))
[PROOFSTEP]
ring


[GOAL]
α : Type u_1
inst✝ : Fintype α
G : SimpleGraph α
ε : ℝ
l : ℕ
hε : 0 < ε
hl : l ≤ Fintype.card α
⊢ ∃ P, IsEquipartition P ∧ l ≤ Finset.card P.parts ∧ Finset.card P.parts ≤ bound ε l ∧ IsUniform P G ε
[PROOFSTEP]
obtain hα | hα :=
  le_total (card α)
    (bound ε l)
      -- If `card α ≤ bound ε l`, then the partition into singletons is acceptable.
[GOAL]
case inl
α : Type u_1
inst✝ : Fintype α
G : SimpleGraph α
ε : ℝ
l : ℕ
hε : 0 < ε
hl : l ≤ Fintype.card α
hα : Fintype.card α ≤ bound ε l
⊢ ∃ P, IsEquipartition P ∧ l ≤ Finset.card P.parts ∧ Finset.card P.parts ≤ bound ε l ∧ IsUniform P G ε
[PROOFSTEP]
refine' ⟨⊥, bot_isEquipartition _, _⟩
[GOAL]
case inl
α : Type u_1
inst✝ : Fintype α
G : SimpleGraph α
ε : ℝ
l : ℕ
hε : 0 < ε
hl : l ≤ Fintype.card α
hα : Fintype.card α ≤ bound ε l
⊢ l ≤ Finset.card ⊥.parts ∧ Finset.card ⊥.parts ≤ bound ε l ∧ IsUniform ⊥ G ε
[PROOFSTEP]
rw [card_bot, card_univ]
[GOAL]
case inl
α : Type u_1
inst✝ : Fintype α
G : SimpleGraph α
ε : ℝ
l : ℕ
hε : 0 < ε
hl : l ≤ Fintype.card α
hα : Fintype.card α ≤ bound ε l
⊢ l ≤ Fintype.card α ∧ Fintype.card α ≤ bound ε l ∧ IsUniform ⊥ G ε
[PROOFSTEP]
exact
  ⟨hl, hα, botIsUniform _ hε⟩
    -- Else, let's start from a dummy equipartition of size `initialBound ε l`.
[GOAL]
case inr
α : Type u_1
inst✝ : Fintype α
G : SimpleGraph α
ε : ℝ
l : ℕ
hε : 0 < ε
hl : l ≤ Fintype.card α
hα : bound ε l ≤ Fintype.card α
⊢ ∃ P, IsEquipartition P ∧ l ≤ Finset.card P.parts ∧ Finset.card P.parts ≤ bound ε l ∧ IsUniform P G ε
[PROOFSTEP]
let t := initialBound ε l
[GOAL]
case inr
α : Type u_1
inst✝ : Fintype α
G : SimpleGraph α
ε : ℝ
l : ℕ
hε : 0 < ε
hl : l ≤ Fintype.card α
hα : bound ε l ≤ Fintype.card α
t : ℕ := initialBound ε l
⊢ ∃ P, IsEquipartition P ∧ l ≤ Finset.card P.parts ∧ Finset.card P.parts ≤ bound ε l ∧ IsUniform P G ε
[PROOFSTEP]
have htα : t ≤ (univ : Finset α).card := (initialBound_le_bound _ _).trans (by rwa [Finset.card_univ])
[GOAL]
α : Type u_1
inst✝ : Fintype α
G : SimpleGraph α
ε : ℝ
l : ℕ
hε : 0 < ε
hl : l ≤ Fintype.card α
hα : bound ε l ≤ Fintype.card α
t : ℕ := initialBound ε l
⊢ bound ε l ≤ Finset.card univ
[PROOFSTEP]
rwa [Finset.card_univ]
[GOAL]
case inr
α : Type u_1
inst✝ : Fintype α
G : SimpleGraph α
ε : ℝ
l : ℕ
hε : 0 < ε
hl : l ≤ Fintype.card α
hα : bound ε l ≤ Fintype.card α
t : ℕ := initialBound ε l
htα : t ≤ Finset.card univ
⊢ ∃ P, IsEquipartition P ∧ l ≤ Finset.card P.parts ∧ Finset.card P.parts ≤ bound ε l ∧ IsUniform P G ε
[PROOFSTEP]
obtain ⟨dum, hdum₁, hdum₂⟩ := exists_equipartition_card_eq (univ : Finset α) (initialBound_pos _ _).ne' htα
[GOAL]
case inr.intro.intro
α : Type u_1
inst✝ : Fintype α
G : SimpleGraph α
ε : ℝ
l : ℕ
hε : 0 < ε
hl : l ≤ Fintype.card α
hα : bound ε l ≤ Fintype.card α
t : ℕ := initialBound ε l
htα : t ≤ Finset.card univ
dum : Finpartition univ
hdum₁ : IsEquipartition dum
hdum₂ : Finset.card dum.parts = initialBound ε l
⊢ ∃ P, IsEquipartition P ∧ l ≤ Finset.card P.parts ∧ Finset.card P.parts ≤ bound ε l ∧ IsUniform P G ε
[PROOFSTEP]
obtain hε₁ | hε₁ := le_total 1 ε
[GOAL]
case inr.intro.intro.inl
α : Type u_1
inst✝ : Fintype α
G : SimpleGraph α
ε : ℝ
l : ℕ
hε : 0 < ε
hl : l ≤ Fintype.card α
hα : bound ε l ≤ Fintype.card α
t : ℕ := initialBound ε l
htα : t ≤ Finset.card univ
dum : Finpartition univ
hdum₁ : IsEquipartition dum
hdum₂ : Finset.card dum.parts = initialBound ε l
hε₁ : 1 ≤ ε
⊢ ∃ P, IsEquipartition P ∧ l ≤ Finset.card P.parts ∧ Finset.card P.parts ≤ bound ε l ∧ IsUniform P G ε
[PROOFSTEP]
exact
  ⟨dum, hdum₁, (le_initialBound ε l).trans hdum₂.ge, hdum₂.le.trans (initialBound_le_bound ε l),
    (dum.isUniformOne G).mono hε₁⟩
    -- Else, set up the induction on energy. We phrase it through the existence for each `i` of an
      -- equipartition of size bounded by `stepBound^[i] (initialBound ε l)` and which is either
      -- `ε`-uniform or has energy at least `ε ^ 5 / 4 * i`.
[GOAL]
case inr.intro.intro.inr
α : Type u_1
inst✝ : Fintype α
G : SimpleGraph α
ε : ℝ
l : ℕ
hε : 0 < ε
hl : l ≤ Fintype.card α
hα : bound ε l ≤ Fintype.card α
t : ℕ := initialBound ε l
htα : t ≤ Finset.card univ
dum : Finpartition univ
hdum₁ : IsEquipartition dum
hdum₂ : Finset.card dum.parts = initialBound ε l
hε₁ : ε ≤ 1
⊢ ∃ P, IsEquipartition P ∧ l ≤ Finset.card P.parts ∧ Finset.card P.parts ≤ bound ε l ∧ IsUniform P G ε
[PROOFSTEP]
have : Nonempty α := by
  rw [← Fintype.card_pos_iff]
  exact (bound_pos _ _).trans_le hα
[GOAL]
α : Type u_1
inst✝ : Fintype α
G : SimpleGraph α
ε : ℝ
l : ℕ
hε : 0 < ε
hl : l ≤ Fintype.card α
hα : bound ε l ≤ Fintype.card α
t : ℕ := initialBound ε l
htα : t ≤ Finset.card univ
dum : Finpartition univ
hdum₁ : IsEquipartition dum
hdum₂ : Finset.card dum.parts = initialBound ε l
hε₁ : ε ≤ 1
⊢ Nonempty α
[PROOFSTEP]
rw [← Fintype.card_pos_iff]
[GOAL]
α : Type u_1
inst✝ : Fintype α
G : SimpleGraph α
ε : ℝ
l : ℕ
hε : 0 < ε
hl : l ≤ Fintype.card α
hα : bound ε l ≤ Fintype.card α
t : ℕ := initialBound ε l
htα : t ≤ Finset.card univ
dum : Finpartition univ
hdum₁ : IsEquipartition dum
hdum₂ : Finset.card dum.parts = initialBound ε l
hε₁ : ε ≤ 1
⊢ 0 < Fintype.card α
[PROOFSTEP]
exact (bound_pos _ _).trans_le hα
[GOAL]
case inr.intro.intro.inr
α : Type u_1
inst✝ : Fintype α
G : SimpleGraph α
ε : ℝ
l : ℕ
hε : 0 < ε
hl : l ≤ Fintype.card α
hα : bound ε l ≤ Fintype.card α
t : ℕ := initialBound ε l
htα : t ≤ Finset.card univ
dum : Finpartition univ
hdum₁ : IsEquipartition dum
hdum₂ : Finset.card dum.parts = initialBound ε l
hε₁ : ε ≤ 1
this : Nonempty α
⊢ ∃ P, IsEquipartition P ∧ l ≤ Finset.card P.parts ∧ Finset.card P.parts ≤ bound ε l ∧ IsUniform P G ε
[PROOFSTEP]
suffices h :
  ∀ i,
    ∃ P : Finpartition (univ : Finset α),
      P.IsEquipartition ∧
        t ≤ P.parts.card ∧
          P.parts.card ≤ stepBound^[i] t ∧
            (P.IsUniform G ε ∨ ε ^ 5 / 4 * i ≤ P.energy G)
              -- For `i > 4 / ε ^ 5` we know that the partition we get can't have energy `≥ ε ^ 5 / 4 * i > 1`,
                -- so it must instead be `ε`-uniform and we won.
[GOAL]
case inr.intro.intro.inr
α : Type u_1
inst✝ : Fintype α
G : SimpleGraph α
ε : ℝ
l : ℕ
hε : 0 < ε
hl : l ≤ Fintype.card α
hα : bound ε l ≤ Fintype.card α
t : ℕ := initialBound ε l
htα : t ≤ Finset.card univ
dum : Finpartition univ
hdum₁ : IsEquipartition dum
hdum₂ : Finset.card dum.parts = initialBound ε l
hε₁ : ε ≤ 1
this : Nonempty α
h :
  ∀ (i : ℕ),
    ∃ P,
      IsEquipartition P ∧
        t ≤ Finset.card P.parts ∧
          Finset.card P.parts ≤ stepBound^[i] t ∧ (IsUniform P G ε ∨ ε ^ 5 / 4 * ↑i ≤ ↑(energy P G))
⊢ ∃ P, IsEquipartition P ∧ l ≤ Finset.card P.parts ∧ Finset.card P.parts ≤ bound ε l ∧ IsUniform P G ε
[PROOFSTEP]
obtain ⟨P, hP₁, hP₂, hP₃, hP₄⟩ := h (⌊4 / ε ^ 5⌋₊ + 1)
[GOAL]
case inr.intro.intro.inr.intro.intro.intro.intro
α : Type u_1
inst✝ : Fintype α
G : SimpleGraph α
ε : ℝ
l : ℕ
hε : 0 < ε
hl : l ≤ Fintype.card α
hα : bound ε l ≤ Fintype.card α
t : ℕ := initialBound ε l
htα : t ≤ Finset.card univ
dum : Finpartition univ
hdum₁ : IsEquipartition dum
hdum₂ : Finset.card dum.parts = initialBound ε l
hε₁ : ε ≤ 1
this : Nonempty α
h :
  ∀ (i : ℕ),
    ∃ P,
      IsEquipartition P ∧
        t ≤ Finset.card P.parts ∧
          Finset.card P.parts ≤ stepBound^[i] t ∧ (IsUniform P G ε ∨ ε ^ 5 / 4 * ↑i ≤ ↑(energy P G))
P : Finpartition univ
hP₁ : IsEquipartition P
hP₂ : t ≤ Finset.card P.parts
hP₃ : Finset.card P.parts ≤ stepBound^[⌊↑4 / ε ^ 5⌋₊ + 1] t
hP₄ : IsUniform P G ε ∨ ε ^ 5 / 4 * ↑(⌊↑4 / ε ^ 5⌋₊ + 1) ≤ ↑(energy P G)
⊢ ∃ P, IsEquipartition P ∧ l ≤ Finset.card P.parts ∧ Finset.card P.parts ≤ bound ε l ∧ IsUniform P G ε
[PROOFSTEP]
refine' ⟨P, hP₁, (le_initialBound _ _).trans hP₂, hP₃.trans _, hP₄.resolve_right fun hPenergy => lt_irrefl (1 : ℝ) _⟩
[GOAL]
case inr.intro.intro.inr.intro.intro.intro.intro.refine'_1
α : Type u_1
inst✝ : Fintype α
G : SimpleGraph α
ε : ℝ
l : ℕ
hε : 0 < ε
hl : l ≤ Fintype.card α
hα : bound ε l ≤ Fintype.card α
t : ℕ := initialBound ε l
htα : t ≤ Finset.card univ
dum : Finpartition univ
hdum₁ : IsEquipartition dum
hdum₂ : Finset.card dum.parts = initialBound ε l
hε₁ : ε ≤ 1
this : Nonempty α
h :
  ∀ (i : ℕ),
    ∃ P,
      IsEquipartition P ∧
        t ≤ Finset.card P.parts ∧
          Finset.card P.parts ≤ stepBound^[i] t ∧ (IsUniform P G ε ∨ ε ^ 5 / 4 * ↑i ≤ ↑(energy P G))
P : Finpartition univ
hP₁ : IsEquipartition P
hP₂ : t ≤ Finset.card P.parts
hP₃ : Finset.card P.parts ≤ stepBound^[⌊↑4 / ε ^ 5⌋₊ + 1] t
hP₄ : IsUniform P G ε ∨ ε ^ 5 / 4 * ↑(⌊↑4 / ε ^ 5⌋₊ + 1) ≤ ↑(energy P G)
⊢ stepBound^[⌊↑4 / ε ^ 5⌋₊ + 1] t ≤ bound ε l
[PROOFSTEP]
rw [iterate_succ_apply']
[GOAL]
case inr.intro.intro.inr.intro.intro.intro.intro.refine'_1
α : Type u_1
inst✝ : Fintype α
G : SimpleGraph α
ε : ℝ
l : ℕ
hε : 0 < ε
hl : l ≤ Fintype.card α
hα : bound ε l ≤ Fintype.card α
t : ℕ := initialBound ε l
htα : t ≤ Finset.card univ
dum : Finpartition univ
hdum₁ : IsEquipartition dum
hdum₂ : Finset.card dum.parts = initialBound ε l
hε₁ : ε ≤ 1
this : Nonempty α
h :
  ∀ (i : ℕ),
    ∃ P,
      IsEquipartition P ∧
        t ≤ Finset.card P.parts ∧
          Finset.card P.parts ≤ stepBound^[i] t ∧ (IsUniform P G ε ∨ ε ^ 5 / 4 * ↑i ≤ ↑(energy P G))
P : Finpartition univ
hP₁ : IsEquipartition P
hP₂ : t ≤ Finset.card P.parts
hP₃ : Finset.card P.parts ≤ stepBound^[⌊↑4 / ε ^ 5⌋₊ + 1] t
hP₄ : IsUniform P G ε ∨ ε ^ 5 / 4 * ↑(⌊↑4 / ε ^ 5⌋₊ + 1) ≤ ↑(energy P G)
⊢ stepBound (stepBound^[⌊↑4 / ε ^ 5⌋₊] t) ≤ bound ε l
[PROOFSTEP]
exact mul_le_mul_left' (pow_le_pow_of_le_left (by norm_num) (by norm_num) _) _
[GOAL]
α : Type u_1
inst✝ : Fintype α
G : SimpleGraph α
ε : ℝ
l : ℕ
hε : 0 < ε
hl : l ≤ Fintype.card α
hα : bound ε l ≤ Fintype.card α
t : ℕ := initialBound ε l
htα : t ≤ Finset.card univ
dum : Finpartition univ
hdum₁ : IsEquipartition dum
hdum₂ : Finset.card dum.parts = initialBound ε l
hε₁ : ε ≤ 1
this : Nonempty α
h :
  ∀ (i : ℕ),
    ∃ P,
      IsEquipartition P ∧
        t ≤ Finset.card P.parts ∧
          Finset.card P.parts ≤ stepBound^[i] t ∧ (IsUniform P G ε ∨ ε ^ 5 / 4 * ↑i ≤ ↑(energy P G))
P : Finpartition univ
hP₁ : IsEquipartition P
hP₂ : t ≤ Finset.card P.parts
hP₃ : Finset.card P.parts ≤ stepBound^[⌊↑4 / ε ^ 5⌋₊ + 1] t
hP₄ : IsUniform P G ε ∨ ε ^ 5 / 4 * ↑(⌊↑4 / ε ^ 5⌋₊ + 1) ≤ ↑(energy P G)
⊢ 0 ≤ 4
[PROOFSTEP]
norm_num
[GOAL]
α : Type u_1
inst✝ : Fintype α
G : SimpleGraph α
ε : ℝ
l : ℕ
hε : 0 < ε
hl : l ≤ Fintype.card α
hα : bound ε l ≤ Fintype.card α
t : ℕ := initialBound ε l
htα : t ≤ Finset.card univ
dum : Finpartition univ
hdum₁ : IsEquipartition dum
hdum₂ : Finset.card dum.parts = initialBound ε l
hε₁ : ε ≤ 1
this : Nonempty α
h :
  ∀ (i : ℕ),
    ∃ P,
      IsEquipartition P ∧
        t ≤ Finset.card P.parts ∧
          Finset.card P.parts ≤ stepBound^[i] t ∧ (IsUniform P G ε ∨ ε ^ 5 / 4 * ↑i ≤ ↑(energy P G))
P : Finpartition univ
hP₁ : IsEquipartition P
hP₂ : t ≤ Finset.card P.parts
hP₃ : Finset.card P.parts ≤ stepBound^[⌊↑4 / ε ^ 5⌋₊ + 1] t
hP₄ : IsUniform P G ε ∨ ε ^ 5 / 4 * ↑(⌊↑4 / ε ^ 5⌋₊ + 1) ≤ ↑(energy P G)
⊢ 4 ≤ 16
[PROOFSTEP]
norm_num
[GOAL]
case inr.intro.intro.inr.intro.intro.intro.intro.refine'_2
α : Type u_1
inst✝ : Fintype α
G : SimpleGraph α
ε : ℝ
l : ℕ
hε : 0 < ε
hl : l ≤ Fintype.card α
hα : bound ε l ≤ Fintype.card α
t : ℕ := initialBound ε l
htα : t ≤ Finset.card univ
dum : Finpartition univ
hdum₁ : IsEquipartition dum
hdum₂ : Finset.card dum.parts = initialBound ε l
hε₁ : ε ≤ 1
this : Nonempty α
h :
  ∀ (i : ℕ),
    ∃ P,
      IsEquipartition P ∧
        t ≤ Finset.card P.parts ∧
          Finset.card P.parts ≤ stepBound^[i] t ∧ (IsUniform P G ε ∨ ε ^ 5 / 4 * ↑i ≤ ↑(energy P G))
P : Finpartition univ
hP₁ : IsEquipartition P
hP₂ : t ≤ Finset.card P.parts
hP₃ : Finset.card P.parts ≤ stepBound^[⌊↑4 / ε ^ 5⌋₊ + 1] t
hP₄ : IsUniform P G ε ∨ ε ^ 5 / 4 * ↑(⌊↑4 / ε ^ 5⌋₊ + 1) ≤ ↑(energy P G)
hPenergy : ε ^ 5 / 4 * ↑(⌊↑4 / ε ^ 5⌋₊ + 1) ≤ ↑(energy P G)
⊢ 1 < 1
[PROOFSTEP]
calc
  (1 : ℝ) = ε ^ 5 / ↑4 * (↑4 / ε ^ 5) := by rw [mul_comm, div_mul_div_cancel 4 (pow_pos hε 5).ne']; norm_num
  _ < ε ^ 5 / 4 * (⌊4 / ε ^ 5⌋₊ + 1) := ((mul_lt_mul_left <| by positivity).2 (Nat.lt_floor_add_one _))
  _ ≤ (P.energy G : ℝ) := by rwa [← Nat.cast_add_one]
  _ ≤ 1 := by exact_mod_cast P.energy_le_one G
[GOAL]
α : Type u_1
inst✝ : Fintype α
G : SimpleGraph α
ε : ℝ
l : ℕ
hε : 0 < ε
hl : l ≤ Fintype.card α
hα : bound ε l ≤ Fintype.card α
t : ℕ := initialBound ε l
htα : t ≤ Finset.card univ
dum : Finpartition univ
hdum₁ : IsEquipartition dum
hdum₂ : Finset.card dum.parts = initialBound ε l
hε₁ : ε ≤ 1
this : Nonempty α
h :
  ∀ (i : ℕ),
    ∃ P,
      IsEquipartition P ∧
        t ≤ Finset.card P.parts ∧
          Finset.card P.parts ≤ stepBound^[i] t ∧ (IsUniform P G ε ∨ ε ^ 5 / 4 * ↑i ≤ ↑(energy P G))
P : Finpartition univ
hP₁ : IsEquipartition P
hP₂ : t ≤ Finset.card P.parts
hP₃ : Finset.card P.parts ≤ stepBound^[⌊↑4 / ε ^ 5⌋₊ + 1] t
hP₄ : IsUniform P G ε ∨ ε ^ 5 / 4 * ↑(⌊↑4 / ε ^ 5⌋₊ + 1) ≤ ↑(energy P G)
hPenergy : ε ^ 5 / 4 * ↑(⌊↑4 / ε ^ 5⌋₊ + 1) ≤ ↑(energy P G)
⊢ 1 = ε ^ 5 / 4 * (4 / ε ^ 5)
[PROOFSTEP]
rw [mul_comm, div_mul_div_cancel 4 (pow_pos hε 5).ne']
[GOAL]
α : Type u_1
inst✝ : Fintype α
G : SimpleGraph α
ε : ℝ
l : ℕ
hε : 0 < ε
hl : l ≤ Fintype.card α
hα : bound ε l ≤ Fintype.card α
t : ℕ := initialBound ε l
htα : t ≤ Finset.card univ
dum : Finpartition univ
hdum₁ : IsEquipartition dum
hdum₂ : Finset.card dum.parts = initialBound ε l
hε₁ : ε ≤ 1
this : Nonempty α
h :
  ∀ (i : ℕ),
    ∃ P,
      IsEquipartition P ∧
        t ≤ Finset.card P.parts ∧
          Finset.card P.parts ≤ stepBound^[i] t ∧ (IsUniform P G ε ∨ ε ^ 5 / 4 * ↑i ≤ ↑(energy P G))
P : Finpartition univ
hP₁ : IsEquipartition P
hP₂ : t ≤ Finset.card P.parts
hP₃ : Finset.card P.parts ≤ stepBound^[⌊↑4 / ε ^ 5⌋₊ + 1] t
hP₄ : IsUniform P G ε ∨ ε ^ 5 / 4 * ↑(⌊↑4 / ε ^ 5⌋₊ + 1) ≤ ↑(energy P G)
hPenergy : ε ^ 5 / 4 * ↑(⌊↑4 / ε ^ 5⌋₊ + 1) ≤ ↑(energy P G)
⊢ 1 = 4 / 4
[PROOFSTEP]
norm_num
[GOAL]
α : Type u_1
inst✝ : Fintype α
G : SimpleGraph α
ε : ℝ
l : ℕ
hε : 0 < ε
hl : l ≤ Fintype.card α
hα : bound ε l ≤ Fintype.card α
t : ℕ := initialBound ε l
htα : t ≤ Finset.card univ
dum : Finpartition univ
hdum₁ : IsEquipartition dum
hdum₂ : Finset.card dum.parts = initialBound ε l
hε₁ : ε ≤ 1
this : Nonempty α
h :
  ∀ (i : ℕ),
    ∃ P,
      IsEquipartition P ∧
        t ≤ Finset.card P.parts ∧
          Finset.card P.parts ≤ stepBound^[i] t ∧ (IsUniform P G ε ∨ ε ^ 5 / 4 * ↑i ≤ ↑(energy P G))
P : Finpartition univ
hP₁ : IsEquipartition P
hP₂ : t ≤ Finset.card P.parts
hP₃ : Finset.card P.parts ≤ stepBound^[⌊↑4 / ε ^ 5⌋₊ + 1] t
hP₄ : IsUniform P G ε ∨ ε ^ 5 / 4 * ↑(⌊↑4 / ε ^ 5⌋₊ + 1) ≤ ↑(energy P G)
hPenergy : ε ^ 5 / 4 * ↑(⌊↑4 / ε ^ 5⌋₊ + 1) ≤ ↑(energy P G)
⊢ 0 < ε ^ 5 / 4
[PROOFSTEP]
positivity
[GOAL]
α : Type u_1
inst✝ : Fintype α
G : SimpleGraph α
ε : ℝ
l : ℕ
hε : 0 < ε
hl : l ≤ Fintype.card α
hα : bound ε l ≤ Fintype.card α
t : ℕ := initialBound ε l
htα : t ≤ Finset.card univ
dum : Finpartition univ
hdum₁ : IsEquipartition dum
hdum₂ : Finset.card dum.parts = initialBound ε l
hε₁ : ε ≤ 1
this : Nonempty α
h :
  ∀ (i : ℕ),
    ∃ P,
      IsEquipartition P ∧
        t ≤ Finset.card P.parts ∧
          Finset.card P.parts ≤ stepBound^[i] t ∧ (IsUniform P G ε ∨ ε ^ 5 / 4 * ↑i ≤ ↑(energy P G))
P : Finpartition univ
hP₁ : IsEquipartition P
hP₂ : t ≤ Finset.card P.parts
hP₃ : Finset.card P.parts ≤ stepBound^[⌊↑4 / ε ^ 5⌋₊ + 1] t
hP₄ : IsUniform P G ε ∨ ε ^ 5 / 4 * ↑(⌊↑4 / ε ^ 5⌋₊ + 1) ≤ ↑(energy P G)
hPenergy : ε ^ 5 / 4 * ↑(⌊↑4 / ε ^ 5⌋₊ + 1) ≤ ↑(energy P G)
⊢ ε ^ 5 / ↑4 * (↑⌊↑4 / ε ^ 5⌋₊ + 1) ≤ ↑(energy P G)
[PROOFSTEP]
rwa [← Nat.cast_add_one]
[GOAL]
α : Type u_1
inst✝ : Fintype α
G : SimpleGraph α
ε : ℝ
l : ℕ
hε : 0 < ε
hl : l ≤ Fintype.card α
hα : bound ε l ≤ Fintype.card α
t : ℕ := initialBound ε l
htα : t ≤ Finset.card univ
dum : Finpartition univ
hdum₁ : IsEquipartition dum
hdum₂ : Finset.card dum.parts = initialBound ε l
hε₁ : ε ≤ 1
this : Nonempty α
h :
  ∀ (i : ℕ),
    ∃ P,
      IsEquipartition P ∧
        t ≤ Finset.card P.parts ∧
          Finset.card P.parts ≤ stepBound^[i] t ∧ (IsUniform P G ε ∨ ε ^ 5 / 4 * ↑i ≤ ↑(energy P G))
P : Finpartition univ
hP₁ : IsEquipartition P
hP₂ : t ≤ Finset.card P.parts
hP₃ : Finset.card P.parts ≤ stepBound^[⌊↑4 / ε ^ 5⌋₊ + 1] t
hP₄ : IsUniform P G ε ∨ ε ^ 5 / 4 * ↑(⌊↑4 / ε ^ 5⌋₊ + 1) ≤ ↑(energy P G)
hPenergy : ε ^ 5 / 4 * ↑(⌊↑4 / ε ^ 5⌋₊ + 1) ≤ ↑(energy P G)
⊢ ↑(energy P G) ≤ 1
[PROOFSTEP]
exact_mod_cast P.energy_le_one G
[GOAL]
case h
α : Type u_1
inst✝ : Fintype α
G : SimpleGraph α
ε : ℝ
l : ℕ
hε : 0 < ε
hl : l ≤ Fintype.card α
hα : bound ε l ≤ Fintype.card α
t : ℕ := initialBound ε l
htα : t ≤ Finset.card univ
dum : Finpartition univ
hdum₁ : IsEquipartition dum
hdum₂ : Finset.card dum.parts = initialBound ε l
hε₁ : ε ≤ 1
this : Nonempty α
⊢ ∀ (i : ℕ),
    ∃ P,
      IsEquipartition P ∧
        t ≤ Finset.card P.parts ∧
          Finset.card P.parts ≤ stepBound^[i] t ∧ (IsUniform P G ε ∨ ε ^ 5 / 4 * ↑i ≤ ↑(energy P G))
[PROOFSTEP]
intro i
[GOAL]
case h
α : Type u_1
inst✝ : Fintype α
G : SimpleGraph α
ε : ℝ
l : ℕ
hε : 0 < ε
hl : l ≤ Fintype.card α
hα : bound ε l ≤ Fintype.card α
t : ℕ := initialBound ε l
htα : t ≤ Finset.card univ
dum : Finpartition univ
hdum₁ : IsEquipartition dum
hdum₂ : Finset.card dum.parts = initialBound ε l
hε₁ : ε ≤ 1
this : Nonempty α
i : ℕ
⊢ ∃ P,
    IsEquipartition P ∧
      t ≤ Finset.card P.parts ∧
        Finset.card P.parts ≤ stepBound^[i] t ∧ (IsUniform P G ε ∨ ε ^ 5 / 4 * ↑i ≤ ↑(energy P G))
[PROOFSTEP]
induction' i with i ih
[GOAL]
case h.zero
α : Type u_1
inst✝ : Fintype α
G : SimpleGraph α
ε : ℝ
l : ℕ
hε : 0 < ε
hl : l ≤ Fintype.card α
hα : bound ε l ≤ Fintype.card α
t : ℕ := initialBound ε l
htα : t ≤ Finset.card univ
dum : Finpartition univ
hdum₁ : IsEquipartition dum
hdum₂ : Finset.card dum.parts = initialBound ε l
hε₁ : ε ≤ 1
this : Nonempty α
⊢ ∃ P,
    IsEquipartition P ∧
      t ≤ Finset.card P.parts ∧
        Finset.card P.parts ≤ stepBound^[Nat.zero] t ∧ (IsUniform P G ε ∨ ε ^ 5 / 4 * ↑Nat.zero ≤ ↑(energy P G))
[PROOFSTEP]
refine' ⟨dum, hdum₁, hdum₂.ge, hdum₂.le, Or.inr _⟩
[GOAL]
case h.zero
α : Type u_1
inst✝ : Fintype α
G : SimpleGraph α
ε : ℝ
l : ℕ
hε : 0 < ε
hl : l ≤ Fintype.card α
hα : bound ε l ≤ Fintype.card α
t : ℕ := initialBound ε l
htα : t ≤ Finset.card univ
dum : Finpartition univ
hdum₁ : IsEquipartition dum
hdum₂ : Finset.card dum.parts = initialBound ε l
hε₁ : ε ≤ 1
this : Nonempty α
⊢ ε ^ 5 / 4 * ↑Nat.zero ≤ ↑(energy dum G)
[PROOFSTEP]
rw [Nat.cast_zero, mul_zero]
[GOAL]
case h.zero
α : Type u_1
inst✝ : Fintype α
G : SimpleGraph α
ε : ℝ
l : ℕ
hε : 0 < ε
hl : l ≤ Fintype.card α
hα : bound ε l ≤ Fintype.card α
t : ℕ := initialBound ε l
htα : t ≤ Finset.card univ
dum : Finpartition univ
hdum₁ : IsEquipartition dum
hdum₂ : Finset.card dum.parts = initialBound ε l
hε₁ : ε ≤ 1
this : Nonempty α
⊢ 0 ≤ ↑(energy dum G)
[PROOFSTEP]
exact_mod_cast dum.energy_nonneg G
[GOAL]
case h.succ
α : Type u_1
inst✝ : Fintype α
G : SimpleGraph α
ε : ℝ
l : ℕ
hε : 0 < ε
hl : l ≤ Fintype.card α
hα : bound ε l ≤ Fintype.card α
t : ℕ := initialBound ε l
htα : t ≤ Finset.card univ
dum : Finpartition univ
hdum₁ : IsEquipartition dum
hdum₂ : Finset.card dum.parts = initialBound ε l
hε₁ : ε ≤ 1
this : Nonempty α
i : ℕ
ih :
  ∃ P,
    IsEquipartition P ∧
      t ≤ Finset.card P.parts ∧
        Finset.card P.parts ≤ stepBound^[i] t ∧ (IsUniform P G ε ∨ ε ^ 5 / 4 * ↑i ≤ ↑(energy P G))
⊢ ∃ P,
    IsEquipartition P ∧
      t ≤ Finset.card P.parts ∧
        Finset.card P.parts ≤ stepBound^[Nat.succ i] t ∧ (IsUniform P G ε ∨ ε ^ 5 / 4 * ↑(Nat.succ i) ≤ ↑(energy P G))
[PROOFSTEP]
obtain ⟨P, hP₁, hP₂, hP₃, hP₄⟩ := ih
[GOAL]
case h.succ.intro.intro.intro.intro
α : Type u_1
inst✝ : Fintype α
G : SimpleGraph α
ε : ℝ
l : ℕ
hε : 0 < ε
hl : l ≤ Fintype.card α
hα : bound ε l ≤ Fintype.card α
t : ℕ := initialBound ε l
htα : t ≤ Finset.card univ
dum : Finpartition univ
hdum₁ : IsEquipartition dum
hdum₂ : Finset.card dum.parts = initialBound ε l
hε₁ : ε ≤ 1
this : Nonempty α
i : ℕ
P : Finpartition univ
hP₁ : IsEquipartition P
hP₂ : t ≤ Finset.card P.parts
hP₃ : Finset.card P.parts ≤ stepBound^[i] t
hP₄ : IsUniform P G ε ∨ ε ^ 5 / 4 * ↑i ≤ ↑(energy P G)
⊢ ∃ P,
    IsEquipartition P ∧
      t ≤ Finset.card P.parts ∧
        Finset.card P.parts ≤ stepBound^[Nat.succ i] t ∧ (IsUniform P G ε ∨ ε ^ 5 / 4 * ↑(Nat.succ i) ≤ ↑(energy P G))
[PROOFSTEP]
by_cases huniform : P.IsUniform G ε
[GOAL]
case pos
α : Type u_1
inst✝ : Fintype α
G : SimpleGraph α
ε : ℝ
l : ℕ
hε : 0 < ε
hl : l ≤ Fintype.card α
hα : bound ε l ≤ Fintype.card α
t : ℕ := initialBound ε l
htα : t ≤ Finset.card univ
dum : Finpartition univ
hdum₁ : IsEquipartition dum
hdum₂ : Finset.card dum.parts = initialBound ε l
hε₁ : ε ≤ 1
this : Nonempty α
i : ℕ
P : Finpartition univ
hP₁ : IsEquipartition P
hP₂ : t ≤ Finset.card P.parts
hP₃ : Finset.card P.parts ≤ stepBound^[i] t
hP₄ : IsUniform P G ε ∨ ε ^ 5 / 4 * ↑i ≤ ↑(energy P G)
huniform : IsUniform P G ε
⊢ ∃ P,
    IsEquipartition P ∧
      t ≤ Finset.card P.parts ∧
        Finset.card P.parts ≤ stepBound^[Nat.succ i] t ∧ (IsUniform P G ε ∨ ε ^ 5 / 4 * ↑(Nat.succ i) ≤ ↑(energy P G))
[PROOFSTEP]
refine' ⟨P, hP₁, hP₂, _, Or.inl huniform⟩
[GOAL]
case pos
α : Type u_1
inst✝ : Fintype α
G : SimpleGraph α
ε : ℝ
l : ℕ
hε : 0 < ε
hl : l ≤ Fintype.card α
hα : bound ε l ≤ Fintype.card α
t : ℕ := initialBound ε l
htα : t ≤ Finset.card univ
dum : Finpartition univ
hdum₁ : IsEquipartition dum
hdum₂ : Finset.card dum.parts = initialBound ε l
hε₁ : ε ≤ 1
this : Nonempty α
i : ℕ
P : Finpartition univ
hP₁ : IsEquipartition P
hP₂ : t ≤ Finset.card P.parts
hP₃ : Finset.card P.parts ≤ stepBound^[i] t
hP₄ : IsUniform P G ε ∨ ε ^ 5 / 4 * ↑i ≤ ↑(energy P G)
huniform : IsUniform P G ε
⊢ Finset.card P.parts ≤ stepBound^[Nat.succ i] t
[PROOFSTEP]
rw [iterate_succ_apply']
[GOAL]
case pos
α : Type u_1
inst✝ : Fintype α
G : SimpleGraph α
ε : ℝ
l : ℕ
hε : 0 < ε
hl : l ≤ Fintype.card α
hα : bound ε l ≤ Fintype.card α
t : ℕ := initialBound ε l
htα : t ≤ Finset.card univ
dum : Finpartition univ
hdum₁ : IsEquipartition dum
hdum₂ : Finset.card dum.parts = initialBound ε l
hε₁ : ε ≤ 1
this : Nonempty α
i : ℕ
P : Finpartition univ
hP₁ : IsEquipartition P
hP₂ : t ≤ Finset.card P.parts
hP₃ : Finset.card P.parts ≤ stepBound^[i] t
hP₄ : IsUniform P G ε ∨ ε ^ 5 / 4 * ↑i ≤ ↑(energy P G)
huniform : IsUniform P G ε
⊢ Finset.card P.parts ≤ stepBound (stepBound^[i] t)
[PROOFSTEP]
exact
  hP₃.trans
    (le_stepBound _)
      -- Else, `P` must instead have energy at least `ε ^ 5 / 4 * i`.
[GOAL]
case neg
α : Type u_1
inst✝ : Fintype α
G : SimpleGraph α
ε : ℝ
l : ℕ
hε : 0 < ε
hl : l ≤ Fintype.card α
hα : bound ε l ≤ Fintype.card α
t : ℕ := initialBound ε l
htα : t ≤ Finset.card univ
dum : Finpartition univ
hdum₁ : IsEquipartition dum
hdum₂ : Finset.card dum.parts = initialBound ε l
hε₁ : ε ≤ 1
this : Nonempty α
i : ℕ
P : Finpartition univ
hP₁ : IsEquipartition P
hP₂ : t ≤ Finset.card P.parts
hP₃ : Finset.card P.parts ≤ stepBound^[i] t
hP₄ : IsUniform P G ε ∨ ε ^ 5 / 4 * ↑i ≤ ↑(energy P G)
huniform : ¬IsUniform P G ε
⊢ ∃ P,
    IsEquipartition P ∧
      t ≤ Finset.card P.parts ∧
        Finset.card P.parts ≤ stepBound^[Nat.succ i] t ∧ (IsUniform P G ε ∨ ε ^ 5 / 4 * ↑(Nat.succ i) ≤ ↑(energy P G))
[PROOFSTEP]
replace hP₄ := hP₄.resolve_left huniform
[GOAL]
case neg
α : Type u_1
inst✝ : Fintype α
G : SimpleGraph α
ε : ℝ
l : ℕ
hε : 0 < ε
hl : l ≤ Fintype.card α
hα : bound ε l ≤ Fintype.card α
t : ℕ := initialBound ε l
htα : t ≤ Finset.card univ
dum : Finpartition univ
hdum₁ : IsEquipartition dum
hdum₂ : Finset.card dum.parts = initialBound ε l
hε₁ : ε ≤ 1
this : Nonempty α
i : ℕ
P : Finpartition univ
hP₁ : IsEquipartition P
hP₂ : t ≤ Finset.card P.parts
hP₃ : Finset.card P.parts ≤ stepBound^[i] t
huniform : ¬IsUniform P G ε
hP₄ : ε ^ 5 / 4 * ↑i ≤ ↑(energy P G)
⊢ ∃ P,
    IsEquipartition P ∧
      t ≤ Finset.card P.parts ∧
        Finset.card P.parts ≤ stepBound^[Nat.succ i] t ∧ (IsUniform P G ε ∨ ε ^ 5 / 4 * ↑(Nat.succ i) ≤ ↑(energy P G))
[PROOFSTEP]
have hεl' : ↑100 < ↑4 ^ P.parts.card * ε ^ 5 :=
  (hundred_lt_pow_initialBound_mul hε l).trans_le
    (mul_le_mul_of_nonneg_right (pow_le_pow (by norm_num) hP₂) <| by positivity)
[GOAL]
α : Type u_1
inst✝ : Fintype α
G : SimpleGraph α
ε : ℝ
l : ℕ
hε : 0 < ε
hl : l ≤ Fintype.card α
hα : bound ε l ≤ Fintype.card α
t : ℕ := initialBound ε l
htα : t ≤ Finset.card univ
dum : Finpartition univ
hdum₁ : IsEquipartition dum
hdum₂ : Finset.card dum.parts = initialBound ε l
hε₁ : ε ≤ 1
this : Nonempty α
i : ℕ
P : Finpartition univ
hP₁ : IsEquipartition P
hP₂ : t ≤ Finset.card P.parts
hP₃ : Finset.card P.parts ≤ stepBound^[i] t
huniform : ¬IsUniform P G ε
hP₄ : ε ^ 5 / 4 * ↑i ≤ ↑(energy P G)
⊢ 1 ≤ 4
[PROOFSTEP]
norm_num
[GOAL]
α : Type u_1
inst✝ : Fintype α
G : SimpleGraph α
ε : ℝ
l : ℕ
hε : 0 < ε
hl : l ≤ Fintype.card α
hα : bound ε l ≤ Fintype.card α
t : ℕ := initialBound ε l
htα : t ≤ Finset.card univ
dum : Finpartition univ
hdum₁ : IsEquipartition dum
hdum₂ : Finset.card dum.parts = initialBound ε l
hε₁ : ε ≤ 1
this : Nonempty α
i : ℕ
P : Finpartition univ
hP₁ : IsEquipartition P
hP₂ : t ≤ Finset.card P.parts
hP₃ : Finset.card P.parts ≤ stepBound^[i] t
huniform : ¬IsUniform P G ε
hP₄ : ε ^ 5 / 4 * ↑i ≤ ↑(energy P G)
⊢ 0 ≤ ε ^ 5
[PROOFSTEP]
positivity
[GOAL]
case neg
α : Type u_1
inst✝ : Fintype α
G : SimpleGraph α
ε : ℝ
l : ℕ
hε : 0 < ε
hl : l ≤ Fintype.card α
hα : bound ε l ≤ Fintype.card α
t : ℕ := initialBound ε l
htα : t ≤ Finset.card univ
dum : Finpartition univ
hdum₁ : IsEquipartition dum
hdum₂ : Finset.card dum.parts = initialBound ε l
hε₁ : ε ≤ 1
this : Nonempty α
i : ℕ
P : Finpartition univ
hP₁ : IsEquipartition P
hP₂ : t ≤ Finset.card P.parts
hP₃ : Finset.card P.parts ≤ stepBound^[i] t
huniform : ¬IsUniform P G ε
hP₄ : ε ^ 5 / 4 * ↑i ≤ ↑(energy P G)
hεl' : 100 < 4 ^ Finset.card P.parts * ε ^ 5
⊢ ∃ P,
    IsEquipartition P ∧
      t ≤ Finset.card P.parts ∧
        Finset.card P.parts ≤ stepBound^[Nat.succ i] t ∧ (IsUniform P G ε ∨ ε ^ 5 / 4 * ↑(Nat.succ i) ≤ ↑(energy P G))
[PROOFSTEP]
have hi : (i : ℝ) ≤ 4 / ε ^ 5 :=
  by
  have hi : ε ^ 5 / 4 * ↑i ≤ 1 := hP₄.trans (by exact_mod_cast P.energy_le_one G)
  rw [div_mul_eq_mul_div, div_le_iff (show (0 : ℝ) < 4 by norm_num)] at hi
  norm_num at hi
  rwa [le_div_iff' (pow_pos hε _)]
[GOAL]
α : Type u_1
inst✝ : Fintype α
G : SimpleGraph α
ε : ℝ
l : ℕ
hε : 0 < ε
hl : l ≤ Fintype.card α
hα : bound ε l ≤ Fintype.card α
t : ℕ := initialBound ε l
htα : t ≤ Finset.card univ
dum : Finpartition univ
hdum₁ : IsEquipartition dum
hdum₂ : Finset.card dum.parts = initialBound ε l
hε₁ : ε ≤ 1
this : Nonempty α
i : ℕ
P : Finpartition univ
hP₁ : IsEquipartition P
hP₂ : t ≤ Finset.card P.parts
hP₃ : Finset.card P.parts ≤ stepBound^[i] t
huniform : ¬IsUniform P G ε
hP₄ : ε ^ 5 / 4 * ↑i ≤ ↑(energy P G)
hεl' : 100 < 4 ^ Finset.card P.parts * ε ^ 5
⊢ ↑i ≤ ↑4 / ε ^ 5
[PROOFSTEP]
have hi : ε ^ 5 / 4 * ↑i ≤ 1 := hP₄.trans (by exact_mod_cast P.energy_le_one G)
[GOAL]
α : Type u_1
inst✝ : Fintype α
G : SimpleGraph α
ε : ℝ
l : ℕ
hε : 0 < ε
hl : l ≤ Fintype.card α
hα : bound ε l ≤ Fintype.card α
t : ℕ := initialBound ε l
htα : t ≤ Finset.card univ
dum : Finpartition univ
hdum₁ : IsEquipartition dum
hdum₂ : Finset.card dum.parts = initialBound ε l
hε₁ : ε ≤ 1
this : Nonempty α
i : ℕ
P : Finpartition univ
hP₁ : IsEquipartition P
hP₂ : t ≤ Finset.card P.parts
hP₃ : Finset.card P.parts ≤ stepBound^[i] t
huniform : ¬IsUniform P G ε
hP₄ : ε ^ 5 / 4 * ↑i ≤ ↑(energy P G)
hεl' : 100 < 4 ^ Finset.card P.parts * ε ^ 5
⊢ ↑(energy P G) ≤ 1
[PROOFSTEP]
exact_mod_cast P.energy_le_one G
[GOAL]
α : Type u_1
inst✝ : Fintype α
G : SimpleGraph α
ε : ℝ
l : ℕ
hε : 0 < ε
hl : l ≤ Fintype.card α
hα : bound ε l ≤ Fintype.card α
t : ℕ := initialBound ε l
htα : t ≤ Finset.card univ
dum : Finpartition univ
hdum₁ : IsEquipartition dum
hdum₂ : Finset.card dum.parts = initialBound ε l
hε₁ : ε ≤ 1
this : Nonempty α
i : ℕ
P : Finpartition univ
hP₁ : IsEquipartition P
hP₂ : t ≤ Finset.card P.parts
hP₃ : Finset.card P.parts ≤ stepBound^[i] t
huniform : ¬IsUniform P G ε
hP₄ : ε ^ 5 / 4 * ↑i ≤ ↑(energy P G)
hεl' : 100 < 4 ^ Finset.card P.parts * ε ^ 5
hi : ε ^ 5 / 4 * ↑i ≤ 1
⊢ ↑i ≤ ↑4 / ε ^ 5
[PROOFSTEP]
rw [div_mul_eq_mul_div, div_le_iff (show (0 : ℝ) < 4 by norm_num)] at hi
[GOAL]
α : Type u_1
inst✝ : Fintype α
G : SimpleGraph α
ε : ℝ
l : ℕ
hε : 0 < ε
hl : l ≤ Fintype.card α
hα : bound ε l ≤ Fintype.card α
t : ℕ := initialBound ε l
htα : t ≤ Finset.card univ
dum : Finpartition univ
hdum₁ : IsEquipartition dum
hdum₂ : Finset.card dum.parts = initialBound ε l
hε₁ : ε ≤ 1
this : Nonempty α
i : ℕ
P : Finpartition univ
hP₁ : IsEquipartition P
hP₂ : t ≤ Finset.card P.parts
hP₃ : Finset.card P.parts ≤ stepBound^[i] t
huniform : ¬IsUniform P G ε
hP₄ : ε ^ 5 / 4 * ↑i ≤ ↑(energy P G)
hεl' : 100 < 4 ^ Finset.card P.parts * ε ^ 5
hi : ε ^ 5 * ↑i / 4 ≤ 1
⊢ 0 < 4
[PROOFSTEP]
norm_num
[GOAL]
α : Type u_1
inst✝ : Fintype α
G : SimpleGraph α
ε : ℝ
l : ℕ
hε : 0 < ε
hl : l ≤ Fintype.card α
hα : bound ε l ≤ Fintype.card α
t : ℕ := initialBound ε l
htα : t ≤ Finset.card univ
dum : Finpartition univ
hdum₁ : IsEquipartition dum
hdum₂ : Finset.card dum.parts = initialBound ε l
hε₁ : ε ≤ 1
this : Nonempty α
i : ℕ
P : Finpartition univ
hP₁ : IsEquipartition P
hP₂ : t ≤ Finset.card P.parts
hP₃ : Finset.card P.parts ≤ stepBound^[i] t
huniform : ¬IsUniform P G ε
hP₄ : ε ^ 5 / 4 * ↑i ≤ ↑(energy P G)
hεl' : 100 < 4 ^ Finset.card P.parts * ε ^ 5
hi : ε ^ 5 * ↑i ≤ 1 * 4
⊢ ↑i ≤ ↑4 / ε ^ 5
[PROOFSTEP]
norm_num at hi
[GOAL]
α : Type u_1
inst✝ : Fintype α
G : SimpleGraph α
ε : ℝ
l : ℕ
hε : 0 < ε
hl : l ≤ Fintype.card α
hα : bound ε l ≤ Fintype.card α
t : ℕ := initialBound ε l
htα : t ≤ Finset.card univ
dum : Finpartition univ
hdum₁ : IsEquipartition dum
hdum₂ : Finset.card dum.parts = initialBound ε l
hε₁ : ε ≤ 1
this : Nonempty α
i : ℕ
P : Finpartition univ
hP₁ : IsEquipartition P
hP₂ : t ≤ Finset.card P.parts
hP₃ : Finset.card P.parts ≤ stepBound^[i] t
huniform : ¬IsUniform P G ε
hP₄ : ε ^ 5 / 4 * ↑i ≤ ↑(energy P G)
hεl' : 100 < 4 ^ Finset.card P.parts * ε ^ 5
hi : ε ^ 5 * ↑i ≤ 4
⊢ ↑i ≤ ↑4 / ε ^ 5
[PROOFSTEP]
rwa [le_div_iff' (pow_pos hε _)]
[GOAL]
case neg
α : Type u_1
inst✝ : Fintype α
G : SimpleGraph α
ε : ℝ
l : ℕ
hε : 0 < ε
hl : l ≤ Fintype.card α
hα : bound ε l ≤ Fintype.card α
t : ℕ := initialBound ε l
htα : t ≤ Finset.card univ
dum : Finpartition univ
hdum₁ : IsEquipartition dum
hdum₂ : Finset.card dum.parts = initialBound ε l
hε₁ : ε ≤ 1
this : Nonempty α
i : ℕ
P : Finpartition univ
hP₁ : IsEquipartition P
hP₂ : t ≤ Finset.card P.parts
hP₃ : Finset.card P.parts ≤ stepBound^[i] t
huniform : ¬IsUniform P G ε
hP₄ : ε ^ 5 / 4 * ↑i ≤ ↑(energy P G)
hεl' : 100 < 4 ^ Finset.card P.parts * ε ^ 5
hi : ↑i ≤ ↑4 / ε ^ 5
⊢ ∃ P,
    IsEquipartition P ∧
      t ≤ Finset.card P.parts ∧
        Finset.card P.parts ≤ stepBound^[Nat.succ i] t ∧ (IsUniform P G ε ∨ ε ^ 5 / 4 * ↑(Nat.succ i) ≤ ↑(energy P G))
[PROOFSTEP]
have hsize : P.parts.card ≤ stepBound^[⌊4 / ε ^ 5⌋₊] t :=
  hP₃.trans (monotone_iterate_of_id_le le_stepBound (Nat.le_floor hi) _)
[GOAL]
case neg
α : Type u_1
inst✝ : Fintype α
G : SimpleGraph α
ε : ℝ
l : ℕ
hε : 0 < ε
hl : l ≤ Fintype.card α
hα : bound ε l ≤ Fintype.card α
t : ℕ := initialBound ε l
htα : t ≤ Finset.card univ
dum : Finpartition univ
hdum₁ : IsEquipartition dum
hdum₂ : Finset.card dum.parts = initialBound ε l
hε₁ : ε ≤ 1
this : Nonempty α
i : ℕ
P : Finpartition univ
hP₁ : IsEquipartition P
hP₂ : t ≤ Finset.card P.parts
hP₃ : Finset.card P.parts ≤ stepBound^[i] t
huniform : ¬IsUniform P G ε
hP₄ : ε ^ 5 / 4 * ↑i ≤ ↑(energy P G)
hεl' : 100 < 4 ^ Finset.card P.parts * ε ^ 5
hi : ↑i ≤ ↑4 / ε ^ 5
hsize : Finset.card P.parts ≤ stepBound^[⌊↑4 / ε ^ 5⌋₊] t
⊢ ∃ P,
    IsEquipartition P ∧
      t ≤ Finset.card P.parts ∧
        Finset.card P.parts ≤ stepBound^[Nat.succ i] t ∧ (IsUniform P G ε ∨ ε ^ 5 / 4 * ↑(Nat.succ i) ≤ ↑(energy P G))
[PROOFSTEP]
have hPα : P.parts.card * 16 ^ P.parts.card ≤ card α :=
  (Nat.mul_le_mul hsize (Nat.pow_le_pow_of_le_right (by norm_num) hsize)).trans hα
[GOAL]
α : Type u_1
inst✝ : Fintype α
G : SimpleGraph α
ε : ℝ
l : ℕ
hε : 0 < ε
hl : l ≤ Fintype.card α
hα : bound ε l ≤ Fintype.card α
t : ℕ := initialBound ε l
htα : t ≤ Finset.card univ
dum : Finpartition univ
hdum₁ : IsEquipartition dum
hdum₂ : Finset.card dum.parts = initialBound ε l
hε₁ : ε ≤ 1
this : Nonempty α
i : ℕ
P : Finpartition univ
hP₁ : IsEquipartition P
hP₂ : t ≤ Finset.card P.parts
hP₃ : Finset.card P.parts ≤ stepBound^[i] t
huniform : ¬IsUniform P G ε
hP₄ : ε ^ 5 / 4 * ↑i ≤ ↑(energy P G)
hεl' : 100 < 4 ^ Finset.card P.parts * ε ^ 5
hi : ↑i ≤ ↑4 / ε ^ 5
hsize : Finset.card P.parts ≤ stepBound^[⌊↑4 / ε ^ 5⌋₊] t
⊢ 16 > 0
[PROOFSTEP]
norm_num
[GOAL]
case neg
α : Type u_1
inst✝ : Fintype α
G : SimpleGraph α
ε : ℝ
l : ℕ
hε : 0 < ε
hl : l ≤ Fintype.card α
hα : bound ε l ≤ Fintype.card α
t : ℕ := initialBound ε l
htα : t ≤ Finset.card univ
dum : Finpartition univ
hdum₁ : IsEquipartition dum
hdum₂ : Finset.card dum.parts = initialBound ε l
hε₁ : ε ≤ 1
this : Nonempty α
i : ℕ
P : Finpartition univ
hP₁ : IsEquipartition P
hP₂ : t ≤ Finset.card P.parts
hP₃ : Finset.card P.parts ≤ stepBound^[i] t
huniform : ¬IsUniform P G ε
hP₄ : ε ^ 5 / 4 * ↑i ≤ ↑(energy P G)
hεl' : 100 < 4 ^ Finset.card P.parts * ε ^ 5
hi : ↑i ≤ ↑4 / ε ^ 5
hsize : Finset.card P.parts ≤ stepBound^[⌊↑4 / ε ^ 5⌋₊] t
hPα : Finset.card P.parts * 16 ^ Finset.card P.parts ≤ Fintype.card α
⊢ ∃ P,
    IsEquipartition P ∧
      t ≤ Finset.card P.parts ∧
        Finset.card P.parts ≤ stepBound^[Nat.succ i] t ∧ (IsUniform P G ε ∨ ε ^ 5 / 4 * ↑(Nat.succ i) ≤ ↑(energy P G))
[PROOFSTEP]
refine'
  ⟨increment hP₁ G ε, increment_isEquipartition hP₁ G ε, _, _,
    Or.inr <| le_trans _ <| energy_increment hP₁ ((seven_le_initialBound ε l).trans hP₂) hεl' hPα huniform hε₁⟩
[GOAL]
case neg.refine'_1
α : Type u_1
inst✝ : Fintype α
G : SimpleGraph α
ε : ℝ
l : ℕ
hε : 0 < ε
hl : l ≤ Fintype.card α
hα : bound ε l ≤ Fintype.card α
t : ℕ := initialBound ε l
htα : t ≤ Finset.card univ
dum : Finpartition univ
hdum₁ : IsEquipartition dum
hdum₂ : Finset.card dum.parts = initialBound ε l
hε₁ : ε ≤ 1
this : Nonempty α
i : ℕ
P : Finpartition univ
hP₁ : IsEquipartition P
hP₂ : t ≤ Finset.card P.parts
hP₃ : Finset.card P.parts ≤ stepBound^[i] t
huniform : ¬IsUniform P G ε
hP₄ : ε ^ 5 / 4 * ↑i ≤ ↑(energy P G)
hεl' : 100 < 4 ^ Finset.card P.parts * ε ^ 5
hi : ↑i ≤ ↑4 / ε ^ 5
hsize : Finset.card P.parts ≤ stepBound^[⌊↑4 / ε ^ 5⌋₊] t
hPα : Finset.card P.parts * 16 ^ Finset.card P.parts ≤ Fintype.card α
⊢ t ≤ Finset.card (increment hP₁ G ε).parts
[PROOFSTEP]
rw [card_increment hPα huniform]
[GOAL]
case neg.refine'_1
α : Type u_1
inst✝ : Fintype α
G : SimpleGraph α
ε : ℝ
l : ℕ
hε : 0 < ε
hl : l ≤ Fintype.card α
hα : bound ε l ≤ Fintype.card α
t : ℕ := initialBound ε l
htα : t ≤ Finset.card univ
dum : Finpartition univ
hdum₁ : IsEquipartition dum
hdum₂ : Finset.card dum.parts = initialBound ε l
hε₁ : ε ≤ 1
this : Nonempty α
i : ℕ
P : Finpartition univ
hP₁ : IsEquipartition P
hP₂ : t ≤ Finset.card P.parts
hP₃ : Finset.card P.parts ≤ stepBound^[i] t
huniform : ¬IsUniform P G ε
hP₄ : ε ^ 5 / 4 * ↑i ≤ ↑(energy P G)
hεl' : 100 < 4 ^ Finset.card P.parts * ε ^ 5
hi : ↑i ≤ ↑4 / ε ^ 5
hsize : Finset.card P.parts ≤ stepBound^[⌊↑4 / ε ^ 5⌋₊] t
hPα : Finset.card P.parts * 16 ^ Finset.card P.parts ≤ Fintype.card α
⊢ t ≤ stepBound (Finset.card P.parts)
[PROOFSTEP]
exact hP₂.trans (le_stepBound _)
[GOAL]
case neg.refine'_2
α : Type u_1
inst✝ : Fintype α
G : SimpleGraph α
ε : ℝ
l : ℕ
hε : 0 < ε
hl : l ≤ Fintype.card α
hα : bound ε l ≤ Fintype.card α
t : ℕ := initialBound ε l
htα : t ≤ Finset.card univ
dum : Finpartition univ
hdum₁ : IsEquipartition dum
hdum₂ : Finset.card dum.parts = initialBound ε l
hε₁ : ε ≤ 1
this : Nonempty α
i : ℕ
P : Finpartition univ
hP₁ : IsEquipartition P
hP₂ : t ≤ Finset.card P.parts
hP₃ : Finset.card P.parts ≤ stepBound^[i] t
huniform : ¬IsUniform P G ε
hP₄ : ε ^ 5 / 4 * ↑i ≤ ↑(energy P G)
hεl' : 100 < 4 ^ Finset.card P.parts * ε ^ 5
hi : ↑i ≤ ↑4 / ε ^ 5
hsize : Finset.card P.parts ≤ stepBound^[⌊↑4 / ε ^ 5⌋₊] t
hPα : Finset.card P.parts * 16 ^ Finset.card P.parts ≤ Fintype.card α
⊢ Finset.card (increment hP₁ G ε).parts ≤ stepBound^[Nat.succ i] t
[PROOFSTEP]
rw [card_increment hPα huniform, iterate_succ_apply']
[GOAL]
case neg.refine'_2
α : Type u_1
inst✝ : Fintype α
G : SimpleGraph α
ε : ℝ
l : ℕ
hε : 0 < ε
hl : l ≤ Fintype.card α
hα : bound ε l ≤ Fintype.card α
t : ℕ := initialBound ε l
htα : t ≤ Finset.card univ
dum : Finpartition univ
hdum₁ : IsEquipartition dum
hdum₂ : Finset.card dum.parts = initialBound ε l
hε₁ : ε ≤ 1
this : Nonempty α
i : ℕ
P : Finpartition univ
hP₁ : IsEquipartition P
hP₂ : t ≤ Finset.card P.parts
hP₃ : Finset.card P.parts ≤ stepBound^[i] t
huniform : ¬IsUniform P G ε
hP₄ : ε ^ 5 / 4 * ↑i ≤ ↑(energy P G)
hεl' : 100 < 4 ^ Finset.card P.parts * ε ^ 5
hi : ↑i ≤ ↑4 / ε ^ 5
hsize : Finset.card P.parts ≤ stepBound^[⌊↑4 / ε ^ 5⌋₊] t
hPα : Finset.card P.parts * 16 ^ Finset.card P.parts ≤ Fintype.card α
⊢ stepBound (Finset.card P.parts) ≤ stepBound (stepBound^[i] t)
[PROOFSTEP]
exact stepBound_mono hP₃
[GOAL]
case neg.refine'_3
α : Type u_1
inst✝ : Fintype α
G : SimpleGraph α
ε : ℝ
l : ℕ
hε : 0 < ε
hl : l ≤ Fintype.card α
hα : bound ε l ≤ Fintype.card α
t : ℕ := initialBound ε l
htα : t ≤ Finset.card univ
dum : Finpartition univ
hdum₁ : IsEquipartition dum
hdum₂ : Finset.card dum.parts = initialBound ε l
hε₁ : ε ≤ 1
this : Nonempty α
i : ℕ
P : Finpartition univ
hP₁ : IsEquipartition P
hP₂ : t ≤ Finset.card P.parts
hP₃ : Finset.card P.parts ≤ stepBound^[i] t
huniform : ¬IsUniform P G ε
hP₄ : ε ^ 5 / 4 * ↑i ≤ ↑(energy P G)
hεl' : 100 < 4 ^ Finset.card P.parts * ε ^ 5
hi : ↑i ≤ ↑4 / ε ^ 5
hsize : Finset.card P.parts ≤ stepBound^[⌊↑4 / ε ^ 5⌋₊] t
hPα : Finset.card P.parts * 16 ^ Finset.card P.parts ≤ Fintype.card α
⊢ ε ^ 5 / 4 * ↑(Nat.succ i) ≤ ↑(energy P G) + ε ^ 5 / 4
[PROOFSTEP]
rw [Nat.cast_succ, mul_add, mul_one]
[GOAL]
case neg.refine'_3
α : Type u_1
inst✝ : Fintype α
G : SimpleGraph α
ε : ℝ
l : ℕ
hε : 0 < ε
hl : l ≤ Fintype.card α
hα : bound ε l ≤ Fintype.card α
t : ℕ := initialBound ε l
htα : t ≤ Finset.card univ
dum : Finpartition univ
hdum₁ : IsEquipartition dum
hdum₂ : Finset.card dum.parts = initialBound ε l
hε₁ : ε ≤ 1
this : Nonempty α
i : ℕ
P : Finpartition univ
hP₁ : IsEquipartition P
hP₂ : t ≤ Finset.card P.parts
hP₃ : Finset.card P.parts ≤ stepBound^[i] t
huniform : ¬IsUniform P G ε
hP₄ : ε ^ 5 / 4 * ↑i ≤ ↑(energy P G)
hεl' : 100 < 4 ^ Finset.card P.parts * ε ^ 5
hi : ↑i ≤ ↑4 / ε ^ 5
hsize : Finset.card P.parts ≤ stepBound^[⌊↑4 / ε ^ 5⌋₊] t
hPα : Finset.card P.parts * 16 ^ Finset.card P.parts ≤ Fintype.card α
⊢ ε ^ 5 / 4 * ↑i + ε ^ 5 / 4 ≤ ↑(energy P G) + ε ^ 5 / 4
[PROOFSTEP]
exact add_le_add_right hP₄ _


[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
n : ℕ
⊢ card ↑(derangements (Fin (n + 2))) =
    (n + 1) * card ↑(derangements (Fin n)) + (n + 1) * card ↑(derangements (Fin (n + 1)))
[PROOFSTEP]
have h1 : ∀ a : Fin (n + 1), card ({ a }ᶜ : Set (Fin (n + 1))) = card (Fin n) :=
  by
  intro a
  simp only [Fintype.card_fin, Finset.card_fin, Fintype.card_ofFinset, Finset.filter_ne' _ a,
    Set.mem_compl_singleton_iff, Finset.card_erase_of_mem (Finset.mem_univ a), add_tsub_cancel_right]
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
n : ℕ
⊢ ∀ (a : Fin (n + 1)), card ↑{a}ᶜ = card (Fin n)
[PROOFSTEP]
intro a
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
n : ℕ
a : Fin (n + 1)
⊢ card ↑{a}ᶜ = card (Fin n)
[PROOFSTEP]
simp only [Fintype.card_fin, Finset.card_fin, Fintype.card_ofFinset, Finset.filter_ne' _ a, Set.mem_compl_singleton_iff,
  Finset.card_erase_of_mem (Finset.mem_univ a), add_tsub_cancel_right]
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
n : ℕ
h1 : ∀ (a : Fin (n + 1)), card ↑{a}ᶜ = card (Fin n)
⊢ card ↑(derangements (Fin (n + 2))) =
    (n + 1) * card ↑(derangements (Fin n)) + (n + 1) * card ↑(derangements (Fin (n + 1)))
[PROOFSTEP]
have h2 : card (Fin (n + 2)) = card (Option (Fin (n + 1))) := by
  simp only [card_fin, card_option]
    -- rewrite the LHS and substitute in our fintype-level equivalence
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
n : ℕ
h1 : ∀ (a : Fin (n + 1)), card ↑{a}ᶜ = card (Fin n)
⊢ card (Fin (n + 2)) = card (Option (Fin (n + 1)))
[PROOFSTEP]
simp only [card_fin, card_option]
  -- rewrite the LHS and substitute in our fintype-level equivalence
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
n : ℕ
h1 : ∀ (a : Fin (n + 1)), card ↑{a}ᶜ = card (Fin n)
h2 : card (Fin (n + 2)) = card (Option (Fin (n + 1)))
⊢ card ↑(derangements (Fin (n + 2))) =
    (n + 1) * card ↑(derangements (Fin n)) + (n + 1) * card ↑(derangements (Fin (n + 1)))
[PROOFSTEP]
simp only [card_derangements_invariant h2, card_congr (@derangementsRecursionEquiv (Fin (n + 1)) _),
  -- push the cardinality through the Σ and ⊕ so that we can use `card_n`card_sigma, card_sum,
  card_derangements_invariant (h1 _), Finset.sum_const, nsmul_eq_mul, Finset.card_fin, mul_add, Nat.cast_id]
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
n : ℕ
⊢ ↑(numDerangements (n + 1)) = (↑n + 1) * ↑(numDerangements n) - (-1) ^ n
[PROOFSTEP]
induction' n with n hn
[GOAL]
case zero
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
⊢ ↑(numDerangements (Nat.zero + 1)) = (↑Nat.zero + 1) * ↑(numDerangements Nat.zero) - (-1) ^ Nat.zero
[PROOFSTEP]
rfl
[GOAL]
case succ
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
n : ℕ
hn : ↑(numDerangements (n + 1)) = (↑n + 1) * ↑(numDerangements n) - (-1) ^ n
⊢ ↑(numDerangements (Nat.succ n + 1)) = (↑(Nat.succ n) + 1) * ↑(numDerangements (Nat.succ n)) - (-1) ^ Nat.succ n
[PROOFSTEP]
simp only [numDerangements_add_two, hn, pow_succ, Int.ofNat_mul, Int.ofNat_add, Int.ofNat_succ]
[GOAL]
case succ
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
n : ℕ
hn : ↑(numDerangements (n + 1)) = (↑n + 1) * ↑(numDerangements n) - (-1) ^ n
⊢ (↑n + 1) * (↑(numDerangements n) + ((↑n + 1) * ↑(numDerangements n) - (-1) ^ n)) =
    (↑n + 1 + 1) * ((↑n + 1) * ↑(numDerangements n) - (-1) ^ n) - -1 * (-1) ^ n
[PROOFSTEP]
ring
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
n : ℕ
⊢ card ↑(derangements (Fin n)) = numDerangements n
[PROOFSTEP]
induction' n using Nat.strong_induction_on with n hyp
[GOAL]
case h
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
n : ℕ
hyp : ∀ (m : ℕ), m < n → card ↑(derangements (Fin m)) = numDerangements m
⊢ card ↑(derangements (Fin n)) = numDerangements n
[PROOFSTEP]
rcases n with _ | _ | n
[GOAL]
case h.zero
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hyp : ∀ (m : ℕ), m < Nat.zero → card ↑(derangements (Fin m)) = numDerangements m
⊢ card ↑(derangements (Fin Nat.zero)) = numDerangements Nat.zero
[PROOFSTEP]
convert_to card ↑{f : Perm (Fin 0) | ∀ (x : Fin 0), f x ≠ x} = _ using 2
[GOAL]
case h.zero.convert_2
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hyp : ∀ (m : ℕ), m < Nat.zero → card ↑(derangements (Fin m)) = numDerangements m
⊢ card ↑{f | ∀ (x : Fin 0), ↑f x ≠ x} = numDerangements Nat.zero
[PROOFSTEP]
rfl
[GOAL]
case h.succ.zero
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hyp : ∀ (m : ℕ), m < Nat.succ Nat.zero → card ↑(derangements (Fin m)) = numDerangements m
⊢ card ↑(derangements (Fin (Nat.succ Nat.zero))) = numDerangements (Nat.succ Nat.zero)
[PROOFSTEP]
convert_to card ↑{f : Perm (Fin 1) | ∀ (x : Fin 1), f x ≠ x} = _ using 2
[GOAL]
case h.succ.zero.convert_2
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hyp : ∀ (m : ℕ), m < Nat.succ Nat.zero → card ↑(derangements (Fin m)) = numDerangements m
⊢ card ↑{f | ∀ (x : Fin 1), ↑f x ≠ x} = numDerangements (Nat.succ Nat.zero)
[PROOFSTEP]
rfl
  -- knock out cases 0 and 1
    -- now we have n ≥ 2. rewrite everything in terms of card_derangements, so that we can use
    -- `card_derangements_fin_add_two`
[GOAL]
case h.succ.succ
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
n : ℕ
hyp : ∀ (m : ℕ), m < Nat.succ (Nat.succ n) → card ↑(derangements (Fin m)) = numDerangements m
⊢ card ↑(derangements (Fin (Nat.succ (Nat.succ n)))) = numDerangements (Nat.succ (Nat.succ n))
[PROOFSTEP]
rw [numDerangements_add_two, card_derangements_fin_add_two, mul_add, hyp _ (Nat.lt_add_of_pos_right zero_lt_two),
  hyp _ (lt_add_one _)]
[GOAL]
α✝ : Type u_1
inst✝³ : DecidableEq α✝
inst✝² : Fintype α✝
α : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq α
⊢ card ↑(derangements α) = numDerangements (card α)
[PROOFSTEP]
rw [← card_derangements_invariant (card_fin _)]
[GOAL]
α✝ : Type u_1
inst✝³ : DecidableEq α✝
inst✝² : Fintype α✝
α : Type u_2
inst✝¹ : Fintype α
inst✝ : DecidableEq α
⊢ card ↑(derangements (Fin (card α))) = numDerangements (card α)
[PROOFSTEP]
exact card_derangements_fin_eq_numDerangements
[GOAL]
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
n : ℕ
⊢ ↑(numDerangements n) = ∑ k in Finset.range (n + 1), (-1) ^ k * ↑(Nat.ascFactorial k (n - k))
[PROOFSTEP]
induction' n with n hn
[GOAL]
case zero
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
⊢ ↑(numDerangements Nat.zero) = ∑ k in Finset.range (Nat.zero + 1), (-1) ^ k * ↑(Nat.ascFactorial k (Nat.zero - k))
[PROOFSTEP]
rfl
[GOAL]
case succ
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
n : ℕ
hn : ↑(numDerangements n) = ∑ k in Finset.range (n + 1), (-1) ^ k * ↑(Nat.ascFactorial k (n - k))
⊢ ↑(numDerangements (Nat.succ n)) =
    ∑ k in Finset.range (Nat.succ n + 1), (-1) ^ k * ↑(Nat.ascFactorial k (Nat.succ n - k))
[PROOFSTEP]
rw [Finset.sum_range_succ, numDerangements_succ, hn, Finset.mul_sum, tsub_self, Nat.ascFactorial_zero, Int.ofNat_one,
  mul_one, pow_succ, neg_one_mul, sub_eq_add_neg, add_left_inj, Finset.sum_congr rfl]
  -- show that (n + 1) * (-1)^x * asc_fac x (n - x) = (-1)^x * asc_fac x (n.succ - x)
[GOAL]
case succ
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
n : ℕ
hn : ↑(numDerangements n) = ∑ k in Finset.range (n + 1), (-1) ^ k * ↑(Nat.ascFactorial k (n - k))
⊢ ∀ (x : ℕ),
    x ∈ Finset.range (n + 1) →
      (↑n + 1) * ((-1) ^ x * ↑(Nat.ascFactorial x (n - x))) = (-1) ^ x * ↑(Nat.ascFactorial x (Nat.succ n - x))
[PROOFSTEP]
intro x hx
[GOAL]
case succ
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
n : ℕ
hn : ↑(numDerangements n) = ∑ k in Finset.range (n + 1), (-1) ^ k * ↑(Nat.ascFactorial k (n - k))
x : ℕ
hx : x ∈ Finset.range (n + 1)
⊢ (↑n + 1) * ((-1) ^ x * ↑(Nat.ascFactorial x (n - x))) = (-1) ^ x * ↑(Nat.ascFactorial x (Nat.succ n - x))
[PROOFSTEP]
have h_le : x ≤ n := Finset.mem_range_succ_iff.mp hx
[GOAL]
case succ
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
n : ℕ
hn : ↑(numDerangements n) = ∑ k in Finset.range (n + 1), (-1) ^ k * ↑(Nat.ascFactorial k (n - k))
x : ℕ
hx : x ∈ Finset.range (n + 1)
h_le : x ≤ n
⊢ (↑n + 1) * ((-1) ^ x * ↑(Nat.ascFactorial x (n - x))) = (-1) ^ x * ↑(Nat.ascFactorial x (Nat.succ n - x))
[PROOFSTEP]
rw [Nat.succ_sub h_le, Nat.ascFactorial_succ, add_tsub_cancel_of_le h_le, Int.ofNat_mul, Int.ofNat_succ, mul_left_comm]


[GOAL]
α : Type u_1
E : Type u_2
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
inst✝ : NormedLatticeAddCommGroup E
f g : { x // x ∈ Lp E p }
⊢ ↑↑f ≤ᵐ[μ] ↑↑g ↔ f ≤ g
[PROOFSTEP]
rw [← Subtype.coe_le_coe, ← AEEqFun.coeFn_le]
[GOAL]
α : Type u_1
E : Type u_2
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
inst✝ : NormedLatticeAddCommGroup E
f : { x // x ∈ Lp E p }
⊢ 0 ≤ᵐ[μ] ↑↑f ↔ 0 ≤ f
[PROOFSTEP]
rw [← coeFn_le]
[GOAL]
α : Type u_1
E : Type u_2
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
inst✝ : NormedLatticeAddCommGroup E
f : { x // x ∈ Lp E p }
⊢ 0 ≤ᵐ[μ] ↑↑f ↔ ↑↑0 ≤ᵐ[μ] ↑↑f
[PROOFSTEP]
have h0 := Lp.coeFn_zero E p μ
[GOAL]
α : Type u_1
E : Type u_2
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
inst✝ : NormedLatticeAddCommGroup E
f : { x // x ∈ Lp E p }
h0 : ↑↑0 =ᵐ[μ] 0
⊢ 0 ≤ᵐ[μ] ↑↑f ↔ ↑↑0 ≤ᵐ[μ] ↑↑f
[PROOFSTEP]
constructor
[GOAL]
case mp
α : Type u_1
E : Type u_2
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
inst✝ : NormedLatticeAddCommGroup E
f : { x // x ∈ Lp E p }
h0 : ↑↑0 =ᵐ[μ] 0
⊢ 0 ≤ᵐ[μ] ↑↑f → ↑↑0 ≤ᵐ[μ] ↑↑f
[PROOFSTEP]
intro h
[GOAL]
case mpr
α : Type u_1
E : Type u_2
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
inst✝ : NormedLatticeAddCommGroup E
f : { x // x ∈ Lp E p }
h0 : ↑↑0 =ᵐ[μ] 0
⊢ ↑↑0 ≤ᵐ[μ] ↑↑f → 0 ≤ᵐ[μ] ↑↑f
[PROOFSTEP]
intro h
[GOAL]
case mp
α : Type u_1
E : Type u_2
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
inst✝ : NormedLatticeAddCommGroup E
f : { x // x ∈ Lp E p }
h0 : ↑↑0 =ᵐ[μ] 0
h : 0 ≤ᵐ[μ] ↑↑f
⊢ ↑↑0 ≤ᵐ[μ] ↑↑f
[PROOFSTEP]
filter_upwards [h, h0] with _ _ h2
[GOAL]
case mpr
α : Type u_1
E : Type u_2
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
inst✝ : NormedLatticeAddCommGroup E
f : { x // x ∈ Lp E p }
h0 : ↑↑0 =ᵐ[μ] 0
h : ↑↑0 ≤ᵐ[μ] ↑↑f
⊢ 0 ≤ᵐ[μ] ↑↑f
[PROOFSTEP]
filter_upwards [h, h0] with _ _ h2
[GOAL]
case h
α : Type u_1
E : Type u_2
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
inst✝ : NormedLatticeAddCommGroup E
f : { x // x ∈ Lp E p }
h0 : ↑↑0 =ᵐ[μ] 0
h : 0 ≤ᵐ[μ] ↑↑f
a✝¹ : α
a✝ : OfNat.ofNat 0 a✝¹ ≤ ↑↑f a✝¹
h2 : ↑↑0 a✝¹ = OfNat.ofNat 0 a✝¹
⊢ ↑↑0 a✝¹ ≤ ↑↑f a✝¹
[PROOFSTEP]
rwa [h2]
[GOAL]
case h
α : Type u_1
E : Type u_2
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
inst✝ : NormedLatticeAddCommGroup E
f : { x // x ∈ Lp E p }
h0 : ↑↑0 =ᵐ[μ] 0
h : ↑↑0 ≤ᵐ[μ] ↑↑f
a✝¹ : α
a✝ : ↑↑0 a✝¹ ≤ ↑↑f a✝¹
h2 : ↑↑0 a✝¹ = OfNat.ofNat 0 a✝¹
⊢ OfNat.ofNat 0 a✝¹ ≤ ↑↑f a✝¹
[PROOFSTEP]
rwa [← h2]
[GOAL]
α : Type u_1
E : Type u_2
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
inst✝ : NormedLatticeAddCommGroup E
⊢ CovariantClass { x // x ∈ Lp E p } { x // x ∈ Lp E p } (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
[PROOFSTEP]
refine' ⟨fun f g₁ g₂ hg₁₂ => _⟩
[GOAL]
α : Type u_1
E : Type u_2
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
inst✝ : NormedLatticeAddCommGroup E
f g₁ g₂ : { x // x ∈ Lp E p }
hg₁₂ : g₁ ≤ g₂
⊢ f + g₁ ≤ f + g₂
[PROOFSTEP]
rw [← coeFn_le] at hg₁₂ ⊢
[GOAL]
α : Type u_1
E : Type u_2
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
inst✝ : NormedLatticeAddCommGroup E
f g₁ g₂ : { x // x ∈ Lp E p }
hg₁₂ : ↑↑g₁ ≤ᵐ[μ] ↑↑g₂
⊢ ↑↑(f + g₁) ≤ᵐ[μ] ↑↑(f + g₂)
[PROOFSTEP]
filter_upwards [coeFn_add f g₁, coeFn_add f g₂, hg₁₂] with _ h1 h2 h3
[GOAL]
case h
α : Type u_1
E : Type u_2
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
inst✝ : NormedLatticeAddCommGroup E
f g₁ g₂ : { x // x ∈ Lp E p }
hg₁₂ : ↑↑g₁ ≤ᵐ[μ] ↑↑g₂
a✝ : α
h1 : ↑↑(f + g₁) a✝ = (↑↑f + ↑↑g₁) a✝
h2 : ↑↑(f + g₂) a✝ = (↑↑f + ↑↑g₂) a✝
h3 : ↑↑g₁ a✝ ≤ ↑↑g₂ a✝
⊢ ↑↑(f + g₁) a✝ ≤ ↑↑(f + g₂) a✝
[PROOFSTEP]
rw [h1, h2, Pi.add_apply, Pi.add_apply]
[GOAL]
case h
α : Type u_1
E : Type u_2
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
inst✝ : NormedLatticeAddCommGroup E
f g₁ g₂ : { x // x ∈ Lp E p }
hg₁₂ : ↑↑g₁ ≤ᵐ[μ] ↑↑g₂
a✝ : α
h1 : ↑↑(f + g₁) a✝ = (↑↑f + ↑↑g₁) a✝
h2 : ↑↑(f + g₂) a✝ = (↑↑f + ↑↑g₂) a✝
h3 : ↑↑g₁ a✝ ≤ ↑↑g₂ a✝
⊢ ↑↑f a✝ + ↑↑g₁ a✝ ≤ ↑↑f a✝ + ↑↑g₂ a✝
[PROOFSTEP]
exact add_le_add le_rfl h3
[GOAL]
α : Type u_1
E : Type u_2
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
inst✝ : NormedLatticeAddCommGroup E
f g : α →ₘ[μ] E
hf : f ∈ Lp E p
hg : g ∈ Lp E p
⊢ f ⊔ g ∈ Lp E p
[PROOFSTEP]
rw [mem_Lp_iff_memℒp] at *
[GOAL]
α : Type u_1
E : Type u_2
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
inst✝ : NormedLatticeAddCommGroup E
f g : α →ₘ[μ] E
hf : Memℒp (↑f) p
hg : Memℒp (↑g) p
⊢ Memℒp (↑(f ⊔ g)) p
[PROOFSTEP]
exact (memℒp_congr_ae (AEEqFun.coeFn_sup _ _)).mpr (hf.sup hg)
[GOAL]
α : Type u_1
E : Type u_2
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
inst✝ : NormedLatticeAddCommGroup E
f g : α →ₘ[μ] E
hf : f ∈ Lp E p
hg : g ∈ Lp E p
⊢ f ⊓ g ∈ Lp E p
[PROOFSTEP]
rw [mem_Lp_iff_memℒp] at *
[GOAL]
α : Type u_1
E : Type u_2
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
inst✝ : NormedLatticeAddCommGroup E
f g : α →ₘ[μ] E
hf : Memℒp (↑f) p
hg : Memℒp (↑g) p
⊢ Memℒp (↑(f ⊓ g)) p
[PROOFSTEP]
exact (memℒp_congr_ae (AEEqFun.coeFn_inf _ _)).mpr (hf.inf hg)
[GOAL]
α : Type u_1
E : Type u_2
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
inst✝¹ : NormedLatticeAddCommGroup E
inst✝ : Fact (1 ≤ p)
src✝¹ : Lattice { x // x ∈ Lp E p } := instLattice
src✝ : NormedAddCommGroup { x // x ∈ Lp E p } := instNormedAddCommGroup
f g : { x // x ∈ Lp E p }
hfg : |f| ≤ |g|
⊢ ‖f‖ ≤ ‖g‖
[PROOFSTEP]
rw [← coeFn_le] at hfg
[GOAL]
α : Type u_1
E : Type u_2
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
inst✝¹ : NormedLatticeAddCommGroup E
inst✝ : Fact (1 ≤ p)
src✝¹ : Lattice { x // x ∈ Lp E p } := instLattice
src✝ : NormedAddCommGroup { x // x ∈ Lp E p } := instNormedAddCommGroup
f g : { x // x ∈ Lp E p }
hfg : ↑↑|f| ≤ᵐ[μ] ↑↑|g|
⊢ ‖f‖ ≤ ‖g‖
[PROOFSTEP]
simp_rw [Lp.norm_def, ENNReal.toReal_le_toReal (Lp.snorm_ne_top f) (Lp.snorm_ne_top g)]
[GOAL]
α : Type u_1
E : Type u_2
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
inst✝¹ : NormedLatticeAddCommGroup E
inst✝ : Fact (1 ≤ p)
src✝¹ : Lattice { x // x ∈ Lp E p } := instLattice
src✝ : NormedAddCommGroup { x // x ∈ Lp E p } := instNormedAddCommGroup
f g : { x // x ∈ Lp E p }
hfg : ↑↑|f| ≤ᵐ[μ] ↑↑|g|
⊢ snorm (↑↑f) p μ ≤ snorm (↑↑g) p μ
[PROOFSTEP]
refine' snorm_mono_ae _
[GOAL]
α : Type u_1
E : Type u_2
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
inst✝¹ : NormedLatticeAddCommGroup E
inst✝ : Fact (1 ≤ p)
src✝¹ : Lattice { x // x ∈ Lp E p } := instLattice
src✝ : NormedAddCommGroup { x // x ∈ Lp E p } := instNormedAddCommGroup
f g : { x // x ∈ Lp E p }
hfg : ↑↑|f| ≤ᵐ[μ] ↑↑|g|
⊢ ∀ᵐ (x : α) ∂μ, ‖↑↑f x‖ ≤ ‖↑↑g x‖
[PROOFSTEP]
filter_upwards [hfg, Lp.coeFn_abs f, Lp.coeFn_abs g] with x hx hxf hxg
[GOAL]
case h
α : Type u_1
E : Type u_2
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
inst✝¹ : NormedLatticeAddCommGroup E
inst✝ : Fact (1 ≤ p)
src✝¹ : Lattice { x // x ∈ Lp E p } := instLattice
src✝ : NormedAddCommGroup { x // x ∈ Lp E p } := instNormedAddCommGroup
f g : { x // x ∈ Lp E p }
hfg : ↑↑|f| ≤ᵐ[μ] ↑↑|g|
x : α
hx : ↑↑|f| x ≤ ↑↑|g| x
hxf : ↑↑|f| x = |↑↑f x|
hxg : ↑↑|g| x = |↑↑g x|
⊢ ‖↑↑f x‖ ≤ ‖↑↑g x‖
[PROOFSTEP]
rw [hxf, hxg] at hx
[GOAL]
case h
α : Type u_1
E : Type u_2
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
inst✝¹ : NormedLatticeAddCommGroup E
inst✝ : Fact (1 ≤ p)
src✝¹ : Lattice { x // x ∈ Lp E p } := instLattice
src✝ : NormedAddCommGroup { x // x ∈ Lp E p } := instNormedAddCommGroup
f g : { x // x ∈ Lp E p }
hfg : ↑↑|f| ≤ᵐ[μ] ↑↑|g|
x : α
hx : |↑↑f x| ≤ |↑↑g x|
hxf : ↑↑|f| x = |↑↑f x|
hxg : ↑↑|g| x = |↑↑g x|
⊢ ‖↑↑f x‖ ≤ ‖↑↑g x‖
[PROOFSTEP]
exact HasSolidNorm.solid hx