mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Combinatorics.Additive.SmallTripling

Goal state before:
pp: G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : Group G
A : Finset G
K : ℝ
hA : ↑(#(A ^ 3)) ≤ K * ↑(#A)
hA₀ : A.Nonempty
this : 0 ≤ K
⊢ ↑(#A) * ↑(#(A⁻¹ * A * A)) = ↑(#A) * ↑(#(A⁻¹ * (A * A)))

Tactic:
mul_assoc

Goal state after:
G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : Group G
A : Finset G
K : ℝ
hA : ↑(#(A ^ 3)) ≤ K * ↑(#A)
hA₀ : A.Nonempty
this : 0 ≤ K
⊢ ↑(#A) * ↑(#(A⁻¹ * (A * A))) = ↑(#A) * ↑(#(A⁻¹ * (A * A)))
Module: Mathlib.Combinatorics.Additive.SmallTripling

Goal state before:
pp: G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : Group G
A : Finset G
K : ℝ
hA : ↑(#(A ^ 3)) ≤ K * ↑(#A)
hA₀ : A.Nonempty
this : 0 ≤ K
⊢ ↑(#(A ^ 2)) * ↑(#(A ^ 3)) ≤ K * ↑(#A) * (K * ↑(#A))

Tactic:
by
      gcongr
      calc
        (#(A ^ 2) : ℝ) ≤ #(A ^ 3) := mod_cast hA₀.card_pow_mono (by simp)
        _ ≤ K * #A := hA

Goal state after:
Module: Mathlib.Combinatorics.Additive.SmallTripling

Goal state before:
pp: G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : Group G
A : Finset G
K : ℝ
m : ℕ
hm : 3 ≤ m
hA : ↑(#(A ^ 3)) ≤ K * ↑(#A)
hAsymm : A⁻¹ = A
this : ∀ (ε : ℤ), |ε| = 1 → A ^ ε = A
⊢ ↑(#(A ^ m)) ≤ K ^ (m - 2) * ↑(#A)

Tactic:
calc
    (#(A ^ m) : ℝ) = #((finRange m).map fun i ↦ A ^ 1).prod := by simp
    _ ≤ K ^ (m - 2) * #A :=
      inductive_claim_mul hm (fun δ hδ ↦ by simpa [this _ (hδ _), pow_succ'] using hA) _ (by simp)

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.DegreeSum

Goal state before:
pp: case mpr
V : Type u
G : SimpleGraph V
inst✝² : Fintype V
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableEq V
v : V
d : G.Dart
⊢ (∃ x, ∃ (h : x ∈ G.neighborSet v), G.dartOfNeighborSet v ⟨x, h⟩ = d) → d.toProd.1 = v

Tactic:
· rintro ⟨e, he, rfl⟩
    rfl

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Finite

Goal state before:
pp: V : Type u_1
G₁ G₂ : SimpleGraph V
inst✝¹ : Fintype ↑G₁.edgeSet
inst✝ : Fintype ↑G₂.edgeSet
⊢ Disjoint G₁.edgeFinset G₂.edgeFinset ↔ Disjoint G₁ G₂

Tactic:
simp_rw [← Finset.disjoint_coe, coe_edgeFinset, disjoint_edgeSet]

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Finite

Goal state before:
pp: V : Type u_1
v : V
inst✝¹ : Fintype V
inst✝ : DecidableEq V
⊢ ⊤.neighborFinset v = {v}ᶜ

Tactic:
by
  simp [← Finset.coe_inj]

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Finite

Goal state before:
pp: V : Type u_1
v : V
inst✝³ : DecidableEq V
G₁ G₂ : SimpleGraph V
inst✝² : Fintype ↑((G₁ ⊔ G₂).neighborSet v)
inst✝¹ : Fintype ↑(G₁.neighborSet v)
inst✝ : Fintype ↑(G₂.neighborSet v)
⊢ (G₁ ⊔ G₂).neighborFinset v = G₁.neighborFinset v ∪ G₂.neighborFinset v

Tactic:
by
  simp [← Finset.coe_inj]

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Finite

Goal state before:
pp: V : Type u_1
v : V
inst✝³ : DecidableEq V
G₁ G₂ : SimpleGraph V
inst✝² : Fintype ↑((G₁ ⊓ G₂).neighborSet v)
inst✝¹ : Fintype ↑(G₁.neighborSet v)
inst✝ : Fintype ↑(G₂.neighborSet v)
⊢ (G₁ ⊓ G₂).neighborFinset v = G₁.neighborFinset v ∩ G₂.neighborFinset v

Tactic:
by
  simp [← Finset.coe_inj]

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Finite

Goal state before:
pp: V : Type u_1
v : V
inst✝³ : DecidableEq V
G₁ G₂ : SimpleGraph V
inst✝² : Fintype ↑((G₁ \ G₂).neighborSet v)
inst✝¹ : Fintype ↑(G₁.neighborSet v)
inst✝ : Fintype ↑(G₂.neighborSet v)
⊢ (G₁ \ G₂).neighborFinset v = G₁.neighborFinset v \ G₂.neighborFinset v

Tactic:
by
  simp [← Finset.coe_inj]

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Finite

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
v : V
inst✝ : Fintype ↑(G.neighborSet v)
⊢ (∃! a, a ∈ G.neighborFinset v) ↔ ∃! w, G.Adj v w

Tactic:
simp only [mem_neighborFinset]

Goal state after:
Module: Mathlib.Order.Partition.Finpartition

Goal state before:
pp: case pos
α : Type u_1
inst✝¹ : Lattice α
inst✝ : OrderBot α
a : α
P : Finpartition a
h : a = ⊥
⊢ Nonempty (Finpartition a)

pp: case neg
α : Type u_1
inst✝¹ : Lattice α
inst✝ : OrderBot α
a : α
P : Finpartition a
h : ¬a = ⊥
⊢ Nonempty (Finpartition a)

Tactic:
· rw [h]; exact ⟨Finpartition.empty α⟩

Goal state after:
case neg
α : Type u_1
inst✝¹ : Lattice α
inst✝ : OrderBot α
a : α
P : Finpartition a
h : ¬a = ⊥
⊢ Nonempty (Finpartition a)
Module: Mathlib.Order.Partition.Finpartition

Goal state before:
pp: case refine_2
α : Type u_1
inst✝¹ : Lattice α
inst✝ : OrderBot α
a : α
P✝ P Q : Finpartition a
hPQ : P ≤ Q
hQP : Q ≤ P
b : α
hb : b ∈ Q.parts
c : α
hc : c ∈ P.parts
hbc : b ≤ c
d : α
hd : d ∈ Q.parts
hcd : c ≤ d
⊢ c ≤ b

Tactic:
rwa [Q.disjoint.eq_of_le hb hd (Q.ne_bot hb) (hbc.trans hcd)]

Goal state after:
Module: Mathlib.Order.Partition.Finpartition

Goal state before:
pp: α : Type u_1
inst✝¹ : Lattice α
inst✝ : OrderBot α
a : α
P Q : Finpartition a
h : P ≤ Q
f : (b : α) → b ∈ Q.parts → α
hP : ∀ (b : α) (a_1 : b ∈ Q.parts), f b a_1 ∈ P.parts
hf : ∀ (b : α) (a : b ∈ Q.parts), f b a ≤ b
⊢ #Q.parts.attach ≤ #P.parts

Tactic:
refine card_le_card_of_injOn (fun b ↦ f _ b.2) (fun b _ ↦ hP _ b.2) fun b _ c _ h ↦ ?_

Goal state after:
α : Type u_1
inst✝¹ : Lattice α
inst✝ : OrderBot α
a : α
P Q : Finpartition a
h✝ : P ≤ Q
f : (b : α) → b ∈ Q.parts → α
hP : ∀ (b : α) (a_1 : b ∈ Q.parts), f b a_1 ∈ P.parts
hf : ∀ (b : α) (a : b ∈ Q.parts), f b a ≤ b
b : ↥Q.parts
x✝¹ : b ∈ ↑Q.parts.attach
c : ↥Q.parts
x✝ : c ∈ ↑Q.parts.attach
h : (fun b ↦ f ↑b ⋯) b = (fun b ↦ f ↑b ⋯) c
⊢ b = c
Module: Mathlib.Order.Partition.Finpartition

Goal state before:
pp: α : Type u_1
inst✝⁴ : Lattice α
inst✝³ : OrderBot α
inst✝² : IsModularLattice α
inst✝¹ : DecidableEq α
ι : Type u_2
I : Finset ι
s : ι → α
P : (i : ι) → Finpartition (s i)
ha : I.SupIndep s
M : Type u_3
inst✝ : AddCommMonoid M
f : α → M
i : ι
hi : i ∈ ↑I
j : ι
hj : j ∈ ↑I
hij : i ≠ j
⊢ (Disjoint on fun i ↦ (P i).parts) i j

Tactic:
rw [Function.onFun, Finset.disjoint_left]

Goal state after:
α : Type u_1
inst✝⁴ : Lattice α
inst✝³ : OrderBot α
inst✝² : IsModularLattice α
inst✝¹ : DecidableEq α
ι : Type u_2
I : Finset ι
s : ι → α
P : (i : ι) → Finpartition (s i)
ha : I.SupIndep s
M : Type u_3
inst✝ : AddCommMonoid M
f : α → M
i : ι
hi : i ∈ ↑I
j : ι
hj : j ∈ ↑I
hij : i ≠ j
⊢ ∀ ⦃a : α⦄, a ∈ (P i).parts → a ∉ (P j).parts
Module: Mathlib.Order.Partition.Finpartition

Goal state before:
pp: α : Type u_1
inst✝³ : Lattice α
inst✝² : OrderBot α
inst✝¹ : IsModularLattice α
inst✝ : DecidableEq α
a : α
P : Finpartition a
Q : (i : α) → i ∈ P.parts → Finpartition i
b : α
hb : b ∈ P.parts
c : α
hc : c ∈ P.parts
hbc : ⟨b, hb⟩ ≠ ⟨c, hc⟩
⊢ (Disjoint on fun i ↦ ((fun i ↦ Q ↑i ⋯) i).parts) ⟨b, hb⟩ ⟨c, hc⟩

Tactic:
rw [Function.onFun, Finset.disjoint_left]

Goal state after:
α : Type u_1
inst✝³ : Lattice α
inst✝² : OrderBot α
inst✝¹ : IsModularLattice α
inst✝ : DecidableEq α
a : α
P : Finpartition a
Q : (i : α) → i ∈ P.parts → Finpartition i
b : α
hb : b ∈ P.parts
c : α
hc : c ∈ P.parts
hbc : ⟨b, hb⟩ ≠ ⟨c, hc⟩
⊢ ∀ ⦃a_1 : α⦄, a_1 ∈ ((fun i ↦ Q ↑i ⋯) ⟨b, hb⟩).parts → a_1 ∉ ((fun i ↦ Q ↑i ⋯) ⟨c, hc⟩).parts
Module: Mathlib.Order.Partition.Finpartition

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t u : Finset α
P : Finpartition s
a✝ : α
parts : Finset (Finset α)
h : ∀ p ∈ parts, p ⊆ s
h' : ∀ a ∈ s, ∃! t, t ∈ parts ∧ a ∈ t
h'' : ∅ ∉ parts
a : Finset α
ha : a ∈ ↑parts
b : Finset α
hb : b ∈ ↑parts
hab : a ≠ b
⊢ (Disjoint on id) a b

Tactic:
rw [Function.onFun, Finset.disjoint_left]

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s t u : Finset α
P : Finpartition s
a✝ : α
parts : Finset (Finset α)
h : ∀ p ∈ parts, p ⊆ s
h' : ∀ a ∈ s, ∃! t, t ∈ parts ∧ a ∈ t
h'' : ∅ ∉ parts
a : Finset α
ha : a ∈ ↑parts
b : Finset α
hb : b ∈ ↑parts
hab : a ≠ b
⊢ ∀ ⦃a_1 : α⦄, a_1 ∈ id a → a_1 ∉ id b
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Bound

Goal state before:
pp: case inr
ι : Type u_2
𝕜 : Type u_3
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
s t : Finset ι
x : 𝕜
hst : s ⊆ t
f : ι → 𝕜
d : 𝕜
hx : 0 ≤ x
hs : x ≤ |(∑ i ∈ s, f i) / ↑(#s) - (∑ i ∈ t, f i) / ↑(#t)|
ht : d ≤ ((∑ i ∈ t, f i) / ↑(#t)) ^ 2
hscard : 0 < ↑(#s)
htcard : 0 < ↑(#t)
h₁ : x ^ 2 ≤ ((∑ i ∈ s, f i) / ↑(#s) - (∑ i ∈ t, f i) / ↑(#t)) ^ 2
h₂ : x ^ 2 ≤ ((∑ i ∈ s, (f i - (∑ j ∈ t, f j) / ↑(#t))) / ↑(#s)) ^ 2
⊢ ((∑ i ∈ t, f i) / ↑(#t)) ^ 2 + ↑(#s) / ↑(#t) * x ^ 2 ≤ (∑ i ∈ t, f i ^ 2) / ↑(#t)

Tactic:
rw [← mul_div_right_comm, le_div_iff₀ htcard, add_mul, div_mul_cancel₀ _ htcard.ne']

Goal state after:
case inr
ι : Type u_2
𝕜 : Type u_3
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
s t : Finset ι
x : 𝕜
hst : s ⊆ t
f : ι → 𝕜
d : 𝕜
hx : 0 ≤ x
hs : x ≤ |(∑ i ∈ s, f i) / ↑(#s) - (∑ i ∈ t, f i) / ↑(#t)|
ht : d ≤ ((∑ i ∈ t, f i) / ↑(#t)) ^ 2
hscard : 0 < ↑(#s)
htcard : 0 < ↑(#t)
h₁ : x ^ 2 ≤ ((∑ i ∈ s, f i) / ↑(#s) - (∑ i ∈ t, f i) / ↑(#t)) ^ 2
h₂ : x ^ 2 ≤ ((∑ i ∈ s, (f i - (∑ j ∈ t, f j) / ↑(#t))) / ↑(#s)) ^ 2
⊢ ((∑ i ∈ t, f i) / ↑(#t)) ^ 2 * ↑(#t) + ↑(#s) * x ^ 2 ≤ ∑ i ∈ t, f i ^ 2
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform

Goal state before:
pp: case inl
α : Type u_1
𝕜 : Type u_2
inst✝³ : Field 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
s t : Finset α
h₁ : s ≠ t
h₂ : ¬G.IsUniform ε s t
lt : WellOrderingRel s t
⊢ ε ≤
    ↑|G.edgeDensity (G.nonuniformWitnesses ε s t).1
            (if WellOrderingRel t s then (G.nonuniformWitnesses ε t s).1 else (G.nonuniformWitnesses ε s t).2) -
          G.edgeDensity s t|

Tactic:
if_neg (asymm lt)

Goal state after:
case inl
α : Type u_1
𝕜 : Type u_2
inst✝³ : Field 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
s t : Finset α
h₁ : s ≠ t
h₂ : ¬G.IsUniform ε s t
lt : WellOrderingRel s t
⊢ ε ≤ ↑|G.edgeDensity (G.nonuniformWitnesses ε s t).1 (G.nonuniformWitnesses ε s t).2 - G.edgeDensity s t|
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform

Goal state before:
pp: case a.calc_2
α : Type u_1
𝕜 : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : DecidableEq α
A : Finset α
P : Finpartition A
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
hP : P.IsEquipartition
hε : 0 ≤ ε
⊢ (#P.parts * (#A / #P.parts + 1)) ^ 2 - #P.parts * (#A / #P.parts + 1) ^ 2 ≤
    (#P.parts * (#A / #P.parts) + #P.parts) ^ 2

Tactic:
mul_add_one (α := ℕ)

Goal state after:
case a.calc_2
α : Type u_1
𝕜 : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : DecidableEq α
A : Finset α
P : Finpartition A
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
hP : P.IsEquipartition
hε : 0 ≤ ε
⊢ (#P.parts * (#A / #P.parts) + #P.parts) ^ 2 - #P.parts * (#A / #P.parts + 1) ^ 2 ≤
    (#P.parts * (#A / #P.parts) + #P.parts) ^ 2
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform

Goal state before:
pp: α : Type u_1
𝕜 : Type u_2
inst✝³ : Field 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
inst✝ : DecidableEq α
A : Finset α
P : Finpartition A
hP : P.IsEquipartition
h : P.parts.Nonempty
⊢ ↑(#P.parts) * (↑(#A / #P.parts) * ↑(#A / #P.parts + 1)) = ↑(#P.parts) * ↑(#A / #P.parts) * ↑(#A / #P.parts + 1)

Tactic:
mul_assoc

Goal state after:
α : Type u_1
𝕜 : Type u_2
inst✝³ : Field 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
inst✝ : DecidableEq α
A : Finset α
P : Finpartition A
hP : P.IsEquipartition
h : P.parts.Nonempty
⊢ ↑(#P.parts) * (↑(#A / #P.parts) * ↑(#A / #P.parts + 1)) = ↑(#P.parts) * (↑(#A / #P.parts) * ↑(#A / #P.parts + 1))
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Lemma

Goal state before:
pp: case inr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
l : ℕ
hε : 0 < ε
hl : l ≤ Fintype.card α
hα : bound ε l ≤ Fintype.card α
t : ℕ := initialBound ε l
htα : t ≤ #univ
dum : Finpartition univ
hdum₁ : dum.IsEquipartition
hdum₂ : #dum.parts = initialBound ε l
⊢ ∃ P, P.IsEquipartition ∧ l ≤ #P.parts ∧ #P.parts ≤ bound ε l ∧ P.IsUniform G ε

Tactic:
obtain hε₁ | hε₁ := le_total 1 ε

Goal state after:
case inr.inl
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
l : ℕ
hε : 0 < ε
hl : l ≤ Fintype.card α
hα : bound ε l ≤ Fintype.card α
t : ℕ := initialBound ε l
htα : t ≤ #univ
dum : Finpartition univ
hdum₁ : dum.IsEquipartition
hdum₂ : #dum.parts = initialBound ε l
hε₁ : 1 ≤ ε
⊢ ∃ P, P.IsEquipartition ∧ l ≤ #P.parts ∧ #P.parts ≤ bound ε l ∧ P.IsUniform G ε

case inr.inr
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
l : ℕ
hε : 0 < ε
hl : l ≤ Fintype.card α
hα : bound ε l ≤ Fintype.card α
t : ℕ := initialBound ε l
htα : t ≤ #univ
dum : Finpartition univ
hdum₁ : dum.IsEquipartition
hdum₂ : #dum.parts = initialBound ε l
hε₁ : ε ≤ 1
⊢ ∃ P, P.IsEquipartition ∧ l ≤ #P.parts ∧ #P.parts ≤ bound ε l ∧ P.IsUniform G ε
Module: Mathlib.Combinatorics.SimpleGraph.Subgraph

Goal state before:
pp: V : Type u
G : SimpleGraph V
H : G.Subgraph
u v w x : V
h2 : s(u, v) = s(w, x)
⊢ H.Adj u v ↔ H.Adj w x

Tactic:
simp only [Sym2.eq, Sym2.rel_iff', Prod.mk.injEq, Prod.swap_prod_mk] at h2

Goal state after:
V : Type u
G : SimpleGraph V
H : G.Subgraph
u v w x : V
h2 : u = w ∧ v = x ∨ u = x ∧ v = w
⊢ H.Adj u v ↔ H.Adj w x
Module: Mathlib.Combinatorics.SimpleGraph.Copy

Goal state before:
pp: V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
inst✝¹ : Fintype V
inst✝ : Fintype W
⊢ G.copyCount H ≤ G.labelledCopyCount H

Tactic:
copyCount_eq_card_image_copyToSubgraph

Goal state after:
V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
inst✝¹ : Fintype V
inst✝ : Fintype W
⊢ #(image Copy.toSubgraph univ) ≤ G.labelledCopyCount H
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk

Goal state before:
pp: α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
P : Finpartition univ
hP : P.IsEquipartition
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
U : Finset α
hU : U ∈ P.parts
V : Finset α
hV : V ∈ P.parts
hUV : U ≠ V
hunif : ¬G.IsUniform ε U V
hPε : 100 ≤ 4 ^ #P.parts * ε ^ 5
hε₁ : ε ≤ 1
hP₁ : 0 < #P.parts
⊢ 2 ^ #P.parts * (2 ^ #P.parts * ↑m) / ↑(#U) = 2 ^ #P.parts * 2 ^ #P.parts * ↑m / ↑(#U)

Tactic:
mul_assoc

Goal state after:
α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
P : Finpartition univ
hP : P.IsEquipartition
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
U : Finset α
hU : U ∈ P.parts
V : Finset α
hV : V ∈ P.parts
hUV : U ≠ V
hunif : ¬G.IsUniform ε U V
hPε : 100 ≤ 4 ^ #P.parts * ε ^ 5
hε₁ : ε ≤ 1
hP₁ : 0 < #P.parts
⊢ 2 ^ #P.parts * (2 ^ #P.parts * ↑m) / ↑(#U) = 2 ^ #P.parts * (2 ^ #P.parts * ↑m) / ↑(#U)
Module: Mathlib.Combinatorics.SimpleGraph.Copy

Goal state before:
pp: case inr
V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
inst✝¹ : Fintype ↑G.edgeSet
inst✝ : Fintype V
hH : H ≠ ⊥
f : { G' // Nonempty (H ≃g G'.coe) } → Sym2 V := fun G' ↦ ⋯.some
⊢ #G.edgeFinset - G.copyCount H ≤ #(G.killCopies H).edgeFinset

Tactic:
calc
    _ = #G.edgeFinset - card {G' : G.Subgraph // Nonempty (H ≃g G'.coe)} := ?_
    _ ≤ #G.edgeFinset - #(univ.image f) := Nat.sub_le_sub_left card_image_le _
    _ = #G.edgeFinset - #(Set.range f).toFinset := by rw [Set.toFinset_range]
    _ ≤ #(G.edgeFinset \ (Set.range f).toFinset) := le_card_sdiff ..
    _ = #(G.killCopies H).edgeFinset := ?_

Goal state after:
case inr.calc_1
V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
inst✝¹ : Fintype ↑G.edgeSet
inst✝ : Fintype V
hH : H ≠ ⊥
f : { G' // Nonempty (H ≃g G'.coe) } → Sym2 V := fun G' ↦ ⋯.some
⊢ #G.edgeFinset - G.copyCount H = #G.edgeFinset - Fintype.card { G' // Nonempty (H ≃g G'.coe) }

case inr.calc_2
V : Type u_1
W : Type u_2
G : SimpleGraph V
H : SimpleGraph W
inst✝¹ : Fintype ↑G.edgeSet
inst✝ : Fintype V
hH : H ≠ ⊥
f : { G' // Nonempty (H ≃g G'.coe) } → Sym2 V := fun G' ↦ ⋯.some
⊢ #(G.edgeFinset \ (Set.range f).toFinset) = #(G.killCopies H).edgeFinset
Module: Mathlib.Combinatorics.SimpleGraph.Subgraph

Goal state before:
pp: V : Type u
G H : SimpleGraph V
h : H ≤ G
v : V
inst✝¹ : Fintype ↑((toSubgraph H h).neighborSet v)
inst✝ : Fintype ↑(H.neighborSet v)
⊢ ↥(H.neighborFinset v) ≃ ↑((toSubgraph H h).neighborSet v)

Tactic:
simp only [mem_neighborFinset]

Goal state after:
V : Type u
G H : SimpleGraph V
h : H ≤ G
v : V
inst✝¹ : Fintype ↑((toSubgraph H h).neighborSet v)
inst✝ : Fintype ↑(H.neighborSet v)
⊢ { x // H.Adj v x } ≃ ↑((toSubgraph H h).neighborSet v)
Module: Mathlib.Combinatorics.SimpleGraph.Subgraph

Goal state before:
pp: V : Type u
G : SimpleGraph V
v w : V
hvw : G.Adj v w
u : V
this : w = u ↔ u = w
⊢ u ∈ (G.subgraphOfAdj hvw).neighborSet v ↔ u ∈ {w}

Tactic:
by simpa [hvw.ne.symm] using this

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Traversal

Goal state before:
pp: case cons.succ
V : Type u
G : SimpleGraph V
u v v✝ : V
h✝ : G.Adj u v✝
p✝ : G.Walk v✝ v
n : ℕ
h : n + 1 ≤ (cons h✝ p✝).length
⊢ (cons h✝ p✝).getVert (n + 1) = (cons h✝ p✝).support[n + 1]

Tactic:
simp_rw [support_cons, getVert_cons _ _ n.zero_ne_add_one.symm, List.getElem_cons]

Goal state after:
case cons.succ
V : Type u
G : SimpleGraph V
u v v✝ : V
h✝ : G.Adj u v✝
p✝ : G.Walk v✝ v
n : ℕ
h : n + 1 ≤ (cons h✝ p✝).length
⊢ p✝.getVert (n + 1 - 1) = if h : n + 1 = 0 then u else p✝.support[n + 1 - 1]
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Maps

Goal state before:
pp: V : Type u
V' : Type v
V'' : Type w
G : SimpleGraph V
G' : SimpleGraph V'
G'' : SimpleGraph V''
f : G →g G'
f' : G' →g G''
u v u' v' w : V
p✝ : G.Walk u v
H : SimpleGraph V
s s' : Set V
e : Sym2 V
p : G.Walk v w
hp : e ∉ p.edges
x✝ : Sym2 V
⊢ x✝ ∈ p.edges → x✝ ∉ {e}

Tactic:
contrapose; simp +contextual [hp]

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Decomp

Goal state before:
pp: V : Type u
G : SimpleGraph V
v✝¹ w✝¹ u✝ : V
inst✝ : DecidableEq V
v w✝ w v✝ : V
r : G.Adj v v✝
p : G.Walk v✝ w
u : V
h : u ∈ (cons r p).support
hx : v = u
⊢ G.Walk u w

Tactic:
by
      subst u
      exact cons r p

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
⊢ p.support.dropLast ++ [v] = p.support

Tactic:
cases p with | nil => rfl | cons h p
   =>  _ 

Goal state after:
case cons
V : Type u
G : SimpleGraph V
u v v✝ : V
h : G.Adj u v✝
p : G.Walk v✝ v
⊢ (cons h p).support.dropLast ++ [v] = (cons h p).support
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk

Goal state before:
pp: α : Type u_1
inst✝³ : Fintype α
inst✝² : DecidableEq α
P : Finpartition univ
hP : P.IsEquipartition
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
ε : ℝ
U V : Finset α
inst✝ : Nonempty α
hPα : #P.parts * 16 ^ #P.parts ≤ Fintype.card α
hPε : 100 ≤ 4 ^ #P.parts * ε ^ 5
hU : U ∈ P.parts
hV : V ∈ P.parts
A B : Finset (Finset α)
hA : A ⊆ (chunk hP G ε hU).parts
hB : B ⊆ (chunk hP G ε hV).parts
this :
  ↑(G.edgeDensity (A.biUnion id) (B.biUnion id)) - ε ^ 5 / 50 ≤
    (1 - ε ^ 5 / 50) * ↑(G.edgeDensity (A.biUnion id) (B.biUnion id))
| (1 - ε ^ 5 / 50) * ↑(G.edgeDensity (A.biUnion id) (B.biUnion id))

Tactic:
rw [SimpleGraph.edgeDensity_def, SimpleGraph.interedges, ← sup_eq_biUnion, ← sup_eq_biUnion,
      Rel.card_interedges_finpartition _ (ofSubset _ hA rfl) (ofSubset _ hB rfl), ofSubset_parts,
      ofSubset_parts]

Goal state after:
α : Type u_1
inst✝³ : Fintype α
inst✝² : DecidableEq α
P : Finpartition univ
hP : P.IsEquipartition
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
ε : ℝ
U V : Finset α
inst✝ : Nonempty α
hPα : #P.parts * 16 ^ #P.parts ≤ Fintype.card α
hPε : 100 ≤ 4 ^ #P.parts * ε ^ 5
hU : U ∈ P.parts
hV : V ∈ P.parts
A B : Finset (Finset α)
hA : A ⊆ (chunk hP G ε hU).parts
hB : B ⊆ (chunk hP G ε hV).parts
this :
  ↑(G.edgeDensity (A.biUnion id) (B.biUnion id)) - ε ^ 5 / 50 ≤
    (1 - ε ^ 5 / 50) * ↑(G.edgeDensity (A.biUnion id) (B.biUnion id))
| (1 - ε ^ 5 / 50) * ↑(↑(∑ ab ∈ A ×ˢ B, #(interedges G.Adj ab.1 ab.2)) / (↑(#(A.sup id)) * ↑(#(B.sup id))))
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk

Goal state before:
pp: α : Type u_1
inst✝³ : Fintype α
inst✝² : DecidableEq α
P : Finpartition univ
hP : P.IsEquipartition
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
ε : ℝ
U V : Finset α
inst✝ : Nonempty α
hPα : #P.parts * 16 ^ #P.parts ≤ Fintype.card α
hPε : 100 ≤ 4 ^ #P.parts * ε ^ 5
hU : U ∈ P.parts
hV : V ∈ P.parts
A B : Finset (Finset α)
hA : A ⊆ (chunk hP G ε hU).parts
hB : B ⊆ (chunk hP G ε hV).parts
this :
  ↑(G.edgeDensity (A.biUnion id) (B.biUnion id)) - ε ^ 5 / 50 ≤
    (1 - ε ^ 5 / 50) * ↑(G.edgeDensity (A.biUnion id) (B.biUnion id))
x y : Finset α
hx : x ∈ A
hy : y ∈ B
⊢ ↑(#(interedges G.Adj x y)) * ((1 - ε ^ 5 / 50) / (↑(#(A.sup id)) * ↑(#(B.sup id)))) *
      (↑(#A) * ↑(#x) * (↑(#B) * ↑(#y))) ≤
    ↑(#(G.interedges x y))

pp: α : Type u_1
inst✝³ : Fintype α
inst✝² : DecidableEq α
P : Finpartition univ
hP : P.IsEquipartition
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
ε : ℝ
U V : Finset α
inst✝ : Nonempty α
hPα : #P.parts * 16 ^ #P.parts ≤ Fintype.card α
hPε : 100 ≤ 4 ^ #P.parts * ε ^ 5
hU : U ∈ P.parts
hV : V ∈ P.parts
A B : Finset (Finset α)
hA : A ⊆ (chunk hP G ε hU).parts
hB : B ⊆ (chunk hP G ε hV).parts
this :
  ↑(G.edgeDensity (A.biUnion id) (B.biUnion id)) - ε ^ 5 / 50 ≤
    (1 - ε ^ 5 / 50) * ↑(G.edgeDensity (A.biUnion id) (B.biUnion id))
x y : Finset α
hx : x ∈ A
hy : y ∈ B
⊢ 0 < ↑(#A) * ↑(#x) * (↑(#B) * ↑(#y))

Tactic:
mul_assoc

Goal state after:
α : Type u_1
inst✝³ : Fintype α
inst✝² : DecidableEq α
P : Finpartition univ
hP : P.IsEquipartition
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
ε : ℝ
U V : Finset α
inst✝ : Nonempty α
hPα : #P.parts * 16 ^ #P.parts ≤ Fintype.card α
hPε : 100 ≤ 4 ^ #P.parts * ε ^ 5
hU : U ∈ P.parts
hV : V ∈ P.parts
A B : Finset (Finset α)
hA : A ⊆ (chunk hP G ε hU).parts
hB : B ⊆ (chunk hP G ε hV).parts
this :
  ↑(G.edgeDensity (A.biUnion id) (B.biUnion id)) - ε ^ 5 / 50 ≤
    (1 - ε ^ 5 / 50) * ↑(G.edgeDensity (A.biUnion id) (B.biUnion id))
x y : Finset α
hx : x ∈ A
hy : y ∈ B
⊢ ↑(#(interedges G.Adj x y)) *
      ((1 - ε ^ 5 / 50) / (↑(#(A.sup id)) * ↑(#(B.sup id))) * (↑(#A) * ↑(#x) * (↑(#B) * ↑(#y)))) ≤
    ↑(#(G.interedges x y))

α : Type u_1
inst✝³ : Fintype α
inst✝² : DecidableEq α
P : Finpartition univ
hP : P.IsEquipartition
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
ε : ℝ
U V : Finset α
inst✝ : Nonempty α
hPα : #P.parts * 16 ^ #P.parts ≤ Fintype.card α
hPε : 100 ≤ 4 ^ #P.parts * ε ^ 5
hU : U ∈ P.parts
hV : V ∈ P.parts
A B : Finset (Finset α)
hA : A ⊆ (chunk hP G ε hU).parts
hB : B ⊆ (chunk hP G ε hV).parts
this :
  ↑(G.edgeDensity (A.biUnion id) (B.biUnion id)) - ε ^ 5 / 50 ≤
    (1 - ε ^ 5 / 50) * ↑(G.edgeDensity (A.biUnion id) (B.biUnion id))
x y : Finset α
hx : x ∈ A
hy : y ∈ B
⊢ 0 < ↑(#A) * ↑(#x) * (↑(#B) * ↑(#y))
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk

Goal state before:
pp: α : Type u_1
inst✝³ : Fintype α
inst✝² : DecidableEq α
P : Finpartition univ
hP : P.IsEquipartition
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
ε : ℝ
U V : Finset α
inst✝ : Nonempty α
hPα : #P.parts * 16 ^ #P.parts ≤ Fintype.card α
hPε : 100 ≤ 4 ^ #P.parts * ε ^ 5
hU : U ∈ P.parts
hV : V ∈ P.parts
A B : Finset (Finset α)
hA : A ⊆ (chunk hP G ε hU).parts
hB : B ⊆ (chunk hP G ε hV).parts
this :
  ↑(G.edgeDensity (A.biUnion id) (B.biUnion id)) - ε ^ 5 / 50 ≤
    (1 - ε ^ 5 / 50) * ↑(G.edgeDensity (A.biUnion id) (B.biUnion id))
x y : Finset α
hx : x ∈ A
hy : y ∈ B
⊢ (1 - ε ^ 5 / 50) * (↑(#A) * ↑(#x)) * (↑(#B) * ↑(#y)) / (↑(#(A.sup id)) * ↑(#(B.sup id))) ≤ 1

Tactic:
mul_assoc

Goal state after:
α : Type u_1
inst✝³ : Fintype α
inst✝² : DecidableEq α
P : Finpartition univ
hP : P.IsEquipartition
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
ε : ℝ
U V : Finset α
inst✝ : Nonempty α
hPα : #P.parts * 16 ^ #P.parts ≤ Fintype.card α
hPε : 100 ≤ 4 ^ #P.parts * ε ^ 5
hU : U ∈ P.parts
hV : V ∈ P.parts
A B : Finset (Finset α)
hA : A ⊆ (chunk hP G ε hU).parts
hB : B ⊆ (chunk hP G ε hV).parts
this :
  ↑(G.edgeDensity (A.biUnion id) (B.biUnion id)) - ε ^ 5 / 50 ≤
    (1 - ε ^ 5 / 50) * ↑(G.edgeDensity (A.biUnion id) (B.biUnion id))
x y : Finset α
hx : x ∈ A
hy : y ∈ B
⊢ (1 - ε ^ 5 / 50) * (↑(#A) * ↑(#x) * (↑(#B) * ↑(#y))) / (↑(#(A.sup id)) * ↑(#(B.sup id))) ≤ 1
Module: Mathlib.Combinatorics.SimpleGraph.Walk.Operations

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
⊢ p.drop 0 = p.copy ⋯ ⋯

Tactic:
cases p <;> simp [Walk.drop]

Goal state after: