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

Goal state before:
pp: G : Type u_1
inst✝ : Group G
A : Set G
hA : IsApproximateSubgroup 1 A
x : G
hx : A * A ⊆ x • A
hx' : x⁻¹ • (A * A) ⊆ A
⊢ x⁻¹ ∈ A

Tactic:
simpa using hx' (smul_mem_smul_set (mul_mem_mul hA.one_mem hA.one_mem))

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

Goal state before:
pp: case snd
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : CommGroup α
e : α
x : Finset α × Finset α
⊢ x.2 ∩ e⁻¹ • x.1 ∩ e⁻¹ • (x.1 ∪ e • x.2) = x.2 ∩ e⁻¹ • x.1

Tactic:
· rw [smul_finset_union, inv_smul_smul, union_comm, inter_eq_left]
    exact inter_subset_union

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✝ : ℕ
h : ∀ (ε : Fin 3 → ℤ), (∀ (i : Fin 3), |ε i| = 1) → ↑(#(List.map (fun i ↦ A ^ ε i) (finRange 3)).prod) ≤ k * ↑(#A)
m : ℕ
hm : 3 ≤ m + 1
ih :
  ∀ (ε : Fin (m + 1) → ℤ),
    (∀ (i : Fin (m + 1)), |ε i| = 1) →
      ↑(#(List.map (fun i ↦ A ^ ε i) (finRange (m + 1))).prod) ≤ k ^ (m + 1 - 2) * ↑(#A)
ε : Fin (m + 1 + 1) → ℤ
hε : ∀ (i : Fin (m + 1 + 1)), |ε i| = 1
hm₀ : m ≠ 0
hε₀ : ∀ (i : Fin (m + 1 + 1)), ε i ≠ 0
hA : A.Nonempty
hk : 0 ≤ k
π : {n : ℕ} → (Fin n → ℤ) → Finset G := fun {n} δ ↦ (List.map (fun i ↦ A ^ δ i) (finRange n)).prod
V : Finset G := π ![-ε 1, -ε 0]
W : Finset G := π (tail (tail ε))
⊢ ↑(#A) * ↑(#(V⁻¹ * W)) ≤ ↑(#(A * V)) * ↑(#(A * W))

Tactic:
norm_cast

Goal state after:
G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : Group G
A : Finset G
k : ℝ
m✝ : ℕ
h : ∀ (ε : Fin 3 → ℤ), (∀ (i : Fin 3), |ε i| = 1) → ↑(#(List.map (fun i ↦ A ^ ε i) (finRange 3)).prod) ≤ k * ↑(#A)
m : ℕ
hm : 3 ≤ m + 1
ih :
  ∀ (ε : Fin (m + 1) → ℤ),
    (∀ (i : Fin (m + 1)), |ε i| = 1) →
      ↑(#(List.map (fun i ↦ A ^ ε i) (finRange (m + 1))).prod) ≤ k ^ (m + 1 - 2) * ↑(#A)
ε : Fin (m + 1 + 1) → ℤ
hε : ∀ (i : Fin (m + 1 + 1)), |ε i| = 1
hm₀ : m ≠ 0
hε₀ : ∀ (i : Fin (m + 1 + 1)), ε i ≠ 0
hA : A.Nonempty
hk : 0 ≤ k
π : {n : ℕ} → (Fin n → ℤ) → Finset G := fun {n} δ ↦ (List.map (fun i ↦ A ^ δ i) (finRange n)).prod
V : Finset G := π ![-ε 1, -ε 0]
W : Finset G := π (tail (tail ε))
⊢ #A * #(V⁻¹ * W) ≤ #(A * V) * #(A * W)
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 * A)))

Tactic:
norm_cast

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 * 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
⊢ ↑(#A) * ↑(#(A * A⁻¹ * A)) ≤ ↑(#(A * (A * A⁻¹))) * ↑(#(A * A))

Tactic:
norm_cast

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
⊢ #A * #(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 : ℝ
m : ℕ
hm : 3 ≤ m
hA : ↑(#(A ^ 3)) ≤ K * ↑(#A)
ε : Fin m → ℤ
hε : ∀ (i : Fin m), |ε i| = 1
hm₀ : m ≠ 0
hε₀ : ∀ (i : Fin m), ε i ≠ 0
hA₀ : A.Nonempty
⊢ ↑(#A) ≤ ↑(#(A ^ 3))

Tactic:
norm_cast

Goal state after:
G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : Group G
A : Finset G
K : ℝ
m : ℕ
hm : 3 ≤ m
hA : ↑(#(A ^ 3)) ≤ K * ↑(#A)
ε : Fin m → ℤ
hε : ∀ (i : Fin m), |ε i| = 1
hm₀ : m ≠ 0
hε₀ : ∀ (i : Fin m), ε i ≠ 0
hA₀ : A.Nonempty
⊢ #A ≤ #(A ^ 3)
Module: Mathlib.Combinatorics.SimpleGraph.DegreeSum

Goal state before:
pp: V : Type u
G : SimpleGraph V
inst✝² : Fintype V
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableEq V
e : Sym2 V
h : e ∈ G.edgeSet
⊢ #{d | d.edge = e} = 2

Tactic:
obtain ⟨v, w⟩ := e
  let d : G.Dart := ⟨(v, w), h⟩
  convert! congr_arg card d.edge_fiber
  rw [card_insert_of_notMem, card_singleton]
  rw [mem_singleton]
  exact d.symm_ne.symm

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
h : ↑(∑ v, G.degree v) = ↑(2 * #G.edgeFinset)
⊢ Even #{v | Odd (G.degree v)}

Tactic:
simp only [ZMod.natCast_self, zero_mul, Nat.cast_mul] at h

Goal state after:
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
h : ↑(∑ v, G.degree v) = 0
⊢ Even #{v | Odd (G.degree v)}
Module: Mathlib.Combinatorics.SimpleGraph.DegreeSum

Goal state before:
pp: V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
h : ∑ x with ↑(G.degree x) ≠ 0, ↑(G.degree x) = 0
v : V
⊢ ¬↑(G.degree v) = 0 → ↑(G.degree v) = 1

Tactic:
ZMod.natCast_eq_zero_iff_even,

Goal state after:
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
h : ∑ x with ↑(G.degree x) ≠ 0, ↑(G.degree x) = 0
v : V
⊢ ¬Even (G.degree v) → ↑(G.degree v) = 1
Module: Mathlib.Combinatorics.SimpleGraph.Finite

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
inst✝² : Fintype V
inst✝¹ : DecidableRel G.Adj
inst✝ : Nonempty V
⊢ G.maxDegree < Fintype.card V

Tactic:
obtain ⟨v, hv⟩ := G.exists_maximal_degree_vertex
  rw [hv]
  apply G.degree_lt_card_verts v

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
P : Finpartition s
hP : P.IsEquipartition
ht : t ∈ P.parts
⊢ #s / #P.parts ≤ #t

Tactic:
← P.sum_card_parts

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
P : Finpartition s
hP : P.IsEquipartition
ht : t ∈ P.parts
⊢ (∑ i ∈ P.parts, #i) / #P.parts ≤ #t
Module: Mathlib.Order.Partition.Equipartition

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
P : Finpartition s
hP : P.IsEquipartition
ht : t ∈ P.parts
⊢ #t ≤ #s / #P.parts + 1

Tactic:
← P.sum_card_parts

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
P : Finpartition s
hP : P.IsEquipartition
ht : t ∈ P.parts
⊢ #t ≤ (∑ i ∈ P.parts, #i) / #P.parts + 1
Module: Mathlib.Order.Partition.Finpartition

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

Tactic:
hbc.antisymm

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

case refine_1
α : Type u_1
inst✝¹ : Lattice α
inst✝ : OrderBot α
a : α
P✝ P Q : Finpartition a
hPQ : P ≤ Q
hQP : Q ≤ P
b : α
hb : b ∈ P.parts
c : α
hc : c ∈ Q.parts
hbc : b ≤ c
d : α
hd : d ∈ P.parts
hcd : c ≤ d
⊢ c ≤ b
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
⊢ b ∈ P.parts

Tactic:
hbc.antisymm

Goal state after:
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 ∈ P.parts

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
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Bound

Goal state before:
pp: α : Type u_1
inst✝ : Semiring α
n : ℕ
⊢ ↑(n * 4 ^ n) = ↑n * 4 ^ n

Tactic:
norm_cast

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Bound

Goal state before:
pp: α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
P : Finpartition univ
ε : ℝ
inst✝ : Nonempty α
hPα : #P.parts * 16 ^ #P.parts ≤ Fintype.card α
hPε : 100 ≤ 4 ^ #P.parts * ε ^ 5
⊢ 4 ^ #P.parts ≤ ↑m

Tactic:
norm_cast

Goal state after:
α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
P : Finpartition univ
ε : ℝ
inst✝ : Nonempty α
hPα : #P.parts * 16 ^ #P.parts ≤ Fintype.card α
hPε : 100 ≤ 4 ^ #P.parts * ε ^ 5
⊢ 4 ^ #P.parts ≤ m
Module: Mathlib.Order.Partition.Finpartition

Goal state before:
pp: case neg
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
P : Finpartition s
a : α
ha : a ∉ s
⊢ a ∈ P.part a ↔ a ∈ s

Tactic:
simp [P.part_eq_empty.2, ha]

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Bound

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
P : Finpartition univ
u : Finset α
hP : P.IsEquipartition
hu : u ∈ P.parts
⊢ 4 ^ #P.parts * ↑m ≤ ↑(#u)

Tactic:
norm_cast

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
P : Finpartition univ
u : Finset α
hP : P.IsEquipartition
hu : u ∈ P.parts
⊢ 4 ^ #P.parts * m ≤ #u
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Bound

Goal state before:
pp: ι : Type u_2
𝕜 : Type u_3
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
s t : Finset ι
x : 𝕜
hst : s ⊆ t
f : ι → 𝕜
hs : x ^ 2 ≤ ((∑ i ∈ s, f i) / ↑(#s)) ^ 2
hs' : ↑(#s) ≠ 0
⊢ ↑(#s) * x ^ 2 ≤ ↑(#s) * ((∑ i ∈ s, f i ^ 2) / ↑(#s))

Tactic:
by
    gcongr
    exact hs.trans sum_div_card_sq_le_sum_sq_div_card

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

Goal state before:
pp: α : Type u_4
β : Type u_5
r : α → β → Prop
inst✝ : (a : α) → DecidablePred (r a)
s : Finset α
t : Finset β
hs : s.Nonempty
ht : t.Nonempty
⊢ ↑(#s) * ↑(#t) ≠ 0

Tactic:
· exact mod_cast (mul_pos hs.card_pos ht.card_pos).ne'

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

Goal state before:
pp: case inr.inr
𝕜 : Type u_1
α : Type u_4
β : Type u_5
inst✝³ : Field 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
r : α → β → Prop
inst✝ : (a : α) → DecidablePred (r a)
s₁ s₂ : Finset α
t₁ t₂ : Finset β
δ : 𝕜
hs : s₂ ⊆ s₁
ht : t₂ ⊆ t₁
hδ₀ : 0 ≤ δ
hδ₁ : 0 < 1 - δ
hs₂ : (1 - δ) * ↑(#s₁) ≤ ↑(#s₂)
ht₂ : (1 - δ) * ↑(#t₁) ≤ ↑(#t₂)
hδ' : 0 ≤ 2 * δ - δ ^ 2
hs₂' : s₂.Nonempty
ht₂' : t₂.Nonempty
hr : 2 * δ - δ ^ 2 = 1 - (1 - δ) * (1 - δ)
⊢ |↑(edgeDensity r s₂ t₂) - ↑(edgeDensity r s₁ t₁)| ≤ 1 - (1 - δ) * (1 - δ)

Tactic:
norm_cast

Goal state after:
case inr.inr
𝕜 : Type u_1
α : Type u_4
β : Type u_5
inst✝³ : Field 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
r : α → β → Prop
inst✝ : (a : α) → DecidablePred (r a)
s₁ s₂ : Finset α
t₁ t₂ : Finset β
δ : 𝕜
hs : s₂ ⊆ s₁
ht : t₂ ⊆ t₁
hδ₀ : 0 ≤ δ
hδ₁ : 0 < 1 - δ
hs₂ : (1 - δ) * ↑(#s₁) ≤ ↑(#s₂)
ht₂ : (1 - δ) * ↑(#t₁) ≤ ↑(#t₂)
hδ' : 0 ≤ 2 * δ - δ ^ 2
hs₂' : s₂.Nonempty
ht₂' : t₂.Nonempty
hr : 2 * δ - δ ^ 2 = 1 - (1 - δ) * (1 - δ)
⊢ ↑|edgeDensity r s₂ t₂ - edgeDensity r s₁ t₁| ≤ 1 - (1 - δ) * (1 - δ)
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 α
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
hε : 0 < ε
u v : Finset α
⊢ (u, v) ∉ ⊥.nonUniforms G ε

Tactic:
simp only [mk_mem_nonUniforms, parts_bot, mem_map, not_and,
    Classical.not_not, exists_imp]

Goal state after:
α : Type u_1
𝕜 : Type u_2
inst✝⁴ : Field 𝕜
inst✝³ : LinearOrder 𝕜
inst✝² : IsStrictOrderedRing 𝕜
inst✝¹ : DecidableEq α
A : Finset α
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
hε : 0 < ε
u v : Finset α
⊢ ∀ (x : α),
    x ∈ A ∧ { toFun := singleton, inj' := ⋯ } x = u →
      ∀ (x : α), x ∈ A ∧ { toFun := singleton, inj' := ⋯ } x = v → u ≠ v → G.IsUniform ε u v
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
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
⊢ P.IsUniform G 1

Tactic:
IsUniform,

Goal state after:
α : 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
⊢ ↑(#(P.nonUniforms G 1)) ≤ ↑(#P.parts * (#P.parts - 1)) * 1
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform

Goal state before:
pp: case 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 ≤ ε
⊢ ε * ∑ UV ∈ P.parts.offDiag, ↑(#UV.1) * ↑(#UV.2) ≤ ε * (↑(#A) + ↑(#P.parts)) ^ 2

Tactic:
norm_cast

Goal state after:
case 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 ≤ ε
⊢ ε * ↑(∑ x ∈ P.parts.offDiag, #x.1 * #x.2) ≤ ε * ↑((#A + #P.parts) ^ 2)
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Energy

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
s : Finset α
P : Finpartition s
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
⊢ ↑(#P.parts * #P.parts - #P.parts) ≤ ↑(#P.parts) ^ 2

Tactic:
norm_cast

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
s : Finset α
P : Finpartition s
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
⊢ #P.parts * #P.parts - #P.parts ≤ #P.parts ^ 2
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Energy

Goal state before:
pp: α : Type u_1
inst✝⁴ : DecidableEq α
s : Finset α
P : Finpartition s
G : SimpleGraph α
inst✝³ : DecidableRel G.Adj
𝕜 : Type u_2
inst✝² : Field 𝕜
inst✝¹ : LinearOrder 𝕜
inst✝ : IsStrictOrderedRing 𝕜
⊢ ↑((∑ uv ∈ P.parts.offDiag, G.edgeDensity uv.1 uv.2 ^ 2) / ↑(#P.parts) ^ 2) =
    (∑ uv ∈ P.parts.offDiag, ↑(G.edgeDensity uv.1 uv.2) ^ 2) / ↑(#P.parts) ^ 2

Tactic:
norm_cast

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform

Goal state before:
pp: case inr
α : Type u_1
𝕜 : Type u_2
inst✝³ : Field 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
inst✝ : DecidableEq α
A : Finset α
P : Finpartition A
ε : 𝕜
hε : 0 < ε
hP : P.IsEquipartition
hP' : 4 / ε ≤ ↑(#P.parts)
hA : A.Nonempty
⊢ ↑(#A) * (↑(#A) + ↑(#P.parts)) / ↑(#P.parts) ≤ ε / 2 * ↑(#A) ^ 2

Tactic:
rw [div_le_iff₀ (Nat.cast_pos.2 (P.parts_nonempty hA.ne_empty).card_pos)]

Goal state after:
case inr
α : Type u_1
𝕜 : Type u_2
inst✝³ : Field 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
inst✝ : DecidableEq α
A : Finset α
P : Finpartition A
ε : 𝕜
hε : 0 < ε
hP : P.IsEquipartition
hP' : 4 / ε ≤ ↑(#P.parts)
hA : A.Nonempty
⊢ ↑(#A) * (↑(#A) + ↑(#P.parts)) ≤ ε / 2 * ↑(#A) ^ 2 * ↑(#P.parts)
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform

Goal state before:
pp: case hbc
α : 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
ε : 𝕜
hA : A.Nonempty
hε : 0 < ε
hP : P.IsEquipartition
hG : P.IsUniform G ε
⊢ ↑(#P.parts * (#P.parts - 1)) * ↑(#A / #P.parts + 1) ^ 2 < (↑(#A) + ↑(#P.parts)) ^ 2

Tactic:
norm_cast

Goal state after:
case hbc
α : 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
ε : 𝕜
hA : A.Nonempty
hε : 0 < ε
hP : P.IsEquipartition
hG : P.IsUniform G ε
⊢ #P.parts * (#P.parts - 1) * (#A / #P.parts + 1) ^ 2 < (#A + #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
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : 𝕜
hA : A.Nonempty
hε : 0 < ε
hP : P.IsEquipartition
hG : P.IsUniform G ε
⊢ ↑(#((P.nonUniforms G ε).biUnion fun x ↦
          match x with
          | (U, V) => U ×ˢ V)) ≤
    ∑ i ∈ P.nonUniforms G ε, ↑(#i.1) * ↑(#i.2)

Tactic:
norm_cast

Goal state after:
α : 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
ε : 𝕜
hA : A.Nonempty
hε : 0 < ε
hP : P.IsEquipartition
hG : P.IsUniform G ε
⊢ #((P.nonUniforms G ε).biUnion fun x ↦
        match x with
        | (U, V) => U ×ˢ V) ≤
    ∑ x ∈ P.nonUniforms G ε, #x.1 * #x.2
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Lemma

Goal state before:
pp: 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
this : Nonempty α
⊢ ∀ (i : ℕ),
    ∃ P,
      P.IsEquipartition ∧ t ≤ #P.parts ∧ #P.parts ≤ stepBound^[i] t ∧ (P.IsUniform G ε ∨ ε ^ 5 / 4 * ↑i ≤ ↑(P.energy G))

Tactic:
intro i

Goal state after:
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
this : Nonempty α
i : ℕ
⊢ ∃ P,
    P.IsEquipartition ∧ t ≤ #P.parts ∧ #P.parts ≤ stepBound^[i] t ∧ (P.IsUniform G ε ∨ ε ^ 5 / 4 * ↑i ≤ ↑(P.energy G))
Module: Mathlib.Combinatorics.SimpleGraph.DeleteEdges

Goal state before:
pp: V : Type u_1
inst✝² : Fintype V
inst✝¹ : DecidableEq V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
x : V
hx : {x} ⊆ G.support
⊢ Fintype.card ↑(G.deleteIncidenceSet x).support ≤ Fintype.card ↑G.support - 1

Tactic:
← Set.toFinset_subset_toFinset

Goal state after:
V : Type u_1
inst✝² : Fintype V
inst✝¹ : DecidableEq V
G : SimpleGraph V
inst✝ : DecidableRel G.Adj
x : V
hx : {x}.toFinset ⊆ G.support.toFinset
⊢ Fintype.card ↑(G.deleteIncidenceSet x).support ≤ Fintype.card ↑G.support - 1
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Increment

Goal state before:
pp: case hbc
α : Type u_1
inst✝³ : Fintype α
inst✝² : DecidableEq α
P : Finpartition univ
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
ε : ℝ
inst✝ : Nonempty α
hP : P.IsEquipartition
hP₇ : 7 ≤ #P.parts
hPε : 100 ≤ 4 ^ #P.parts * ε ^ 5
hPα : #P.parts * 16 ^ #P.parts ≤ Fintype.card α
hPG : ↑(#P.parts.offDiag) * ε < ↑(#(P.nonUniforms G ε))
hε₀ : 0 ≤ ε
hε₁ : ε ≤ 1
⊢ 6 * ↑(#P.parts) ^ 2 ≤ ↑(#P.parts * #P.parts - #P.parts) * 7

Tactic:
norm_cast

Goal state after:
case hbc
α : Type u_1
inst✝³ : Fintype α
inst✝² : DecidableEq α
P : Finpartition univ
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
ε : ℝ
inst✝ : Nonempty α
hP : P.IsEquipartition
hP₇ : 7 ≤ #P.parts
hPε : 100 ≤ 4 ^ #P.parts * ε ^ 5
hPα : #P.parts * 16 ^ #P.parts ≤ Fintype.card α
hPG : ↑(#P.parts.offDiag) * ε < ↑(#(P.nonUniforms G ε))
hε₀ : 0 ≤ ε
hε₁ : ε ≤ 1
⊢ 6 * #P.parts ^ 2 ≤ (#P.parts * #P.parts - #P.parts) * 7
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Increment

Goal state before:
pp: case hbc
α : Type u_1
inst✝³ : Fintype α
inst✝² : DecidableEq α
P : Finpartition univ
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
ε : ℝ
inst✝ : Nonempty α
hP : P.IsEquipartition
hP₇ : 7 ≤ #P.parts
hPε : 100 ≤ 4 ^ #P.parts * ε ^ 5
hPα : #P.parts * 16 ^ #P.parts ≤ Fintype.card α
hPG : ↑(#P.parts.offDiag) * ε < ↑(#(P.nonUniforms G ε))
hε₀ : 0 ≤ ε
hε₁ : ε ≤ 1
⊢ 6 * #P.parts ^ 2 ≤ #P.parts * #P.parts * 7 - #P.parts * 7

Tactic:
refine le_tsub_of_add_le_left ?_

Goal state after:
case hbc
α : Type u_1
inst✝³ : Fintype α
inst✝² : DecidableEq α
P : Finpartition univ
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
ε : ℝ
inst✝ : Nonempty α
hP : P.IsEquipartition
hP₇ : 7 ≤ #P.parts
hPε : 100 ≤ 4 ^ #P.parts * ε ^ 5
hPα : #P.parts * 16 ^ #P.parts ≤ Fintype.card α
hPG : ↑(#P.parts.offDiag) * ε < ↑(#(P.nonUniforms G ε))
hε₀ : 0 ≤ ε
hε₁ : ε ≤ 1
⊢ #P.parts * 7 + 6 * #P.parts ^ 2 ≤ #P.parts * #P.parts * 7
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
hHG : H.Free G
hH : H ≠ ⊥
⊢ G.killCopies H = G

Tactic:
· exact (killCopies_eq_left hH).2 hHG

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

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

Tactic:
rw [subgraphOfAdj_symm hvw.symm]

Goal state after:
V : Type u
G : SimpleGraph V
v w : V
hvw : G.Adj v w
⊢ (G.subgraphOfAdj ⋯).neighborSet w = {v}
Module: Mathlib.Combinatorics.SimpleGraph.Subgraph

Goal state before:
pp: V : Type u
G : SimpleGraph V
G' : G.Subgraph
s s' : Set V
⊢ (G'.deleteVerts s).deleteVerts s' = G'.deleteVerts (s ∪ s')

Tactic:
ext <;> simp +contextual [not_or, and_assoc]

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk

Goal state before:
pp: case h₁
α : 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
𝒜 : Finset (Finset α)
s : Finset α
m_pos : 0 < ↑m
h𝒜 : 𝒜 ⊆ (chunk hP G ε hU).parts
hs : s ∈ 𝒜
⊢ ↑(#(𝒜.biUnion id)) ≤ ↑(#𝒜) * (↑m + 1)

Tactic:
norm_cast

Goal state after:
case h₁
α : 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
𝒜 : Finset (Finset α)
s : Finset α
m_pos : 0 < ↑m
h𝒜 : 𝒜 ⊆ (chunk hP G ε hU).parts
hs : s ∈ 𝒜
⊢ #(𝒜.biUnion id) ≤ #𝒜 * (m + 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✝¹
u✝ v✝ : V
p✝ : G.Walk u✝ v✝
H : SimpleGraph V
u w v : V
h✝ : G.Adj u v
p : G.Walk v w
h : ∀ e ∈ (cons' u v w h✝ p).edges, e ∈ H.edgeSet
e : Sym2 V
he : e ∈ p.edges
⊢ e ∈ (cons' u v w h✝ p).edges

Tactic:
simp [he]

Goal state after:
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
w : V
q : G.Walk v w
hpq : ∀ e ∈ (p.append q).edges, e ∈ H.edgeSet
e : Sym2 V
he : e ∈ p.edges
⊢ e ∈ (p.append q).edges

Tactic:
simp [he]

Goal state after:
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
w : V
q : G.Walk v w
hpq : ∀ e ∈ (p.append q).edges, e ∈ H.edgeSet
e : Sym2 V
he : e ∈ q.edges
⊢ e ∈ (p.append q).edges

Tactic:
simp [he]

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

Goal state before:
pp: case head
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
hx : ¬v = v
⊢ v ∈ p.support

Tactic:
exact (hx rfl).elim

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

Goal state before:
pp: case cons.nil
V : Type u
G : SimpleGraph V
u v v' w : V
h' : G.Adj v' w
v✝ w✝ : V
p✝ : G.Walk v✝ w✝
ih : ∀ {h : G.Adj w✝ w} {p' : G.Walk v✝ v'}, p✝.concat h = p'.concat h' → ∃ (hv : w✝ = v'), p✝.copy ⋯ hv = p'
h : G.Adj w✝ w
h✝ : G.Adj v' v✝
he : cons h✝ (p✝.concat h) = nil.concat h'
⊢ ∃ (hv : w✝ = v'), (cons h✝ p✝).copy ⋯ hv = nil

Tactic:
simp only [concat_nil, cons.injEq] at he
      obtain ⟨rfl, he⟩ := he
      exact (concat_ne_nil _ _ (heq_iff_eq.mp he)).elim

Goal state after: