mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend

Goal state before:
pp: N : ℕ
hN₃ : 8 ≤ N
hN₀ : 0 < ↑N
⊢ log 2 * ↑(nValue N) ≤ log ↑N

Tactic:
have : (nValue N : ℝ) ≤ 2 * √(log N) := by
      apply (ceil_lt_add_one <| sqrt_nonneg _).le.trans
      rw [two_mul, add_le_add_iff_left]
      apply le_sqrt_of_sq_le
      rw [one_pow, le_log_iff_exp_le hN₀]
      exact (exp_one_lt_d9.le.trans <| by norm_num).trans (cast_le.2 hN₃)

Goal state after:
N : ℕ
hN₃ : 8 ≤ N
hN₀ : 0 < ↑N
this : ↑(nValue N) ≤ 2 * √(log ↑N)
⊢ log 2 * ↑(nValue N) ≤ log ↑N
Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend

Goal state before:
pp: case hx
N : ℕ
hN : 4096 ≤ N
this : ↑12 * log 2 ≤ log ↑N
⊢ (50 / 19) ^ 2 ≤ ↑12 * log 2

Tactic:
← div_le_iff₀'

Goal state after:
case hx
N : ℕ
hN : 4096 ≤ N
this : ↑12 * log 2 ≤ log ↑N
⊢ (50 / 19) ^ 2 / ↑12 ≤ log 2

case hx
N : ℕ
hN : 4096 ≤ N
this : ↑12 * log 2 ≤ log ↑N
⊢ 0 < ↑12
Module: Mathlib.Combinatorics.Additive.AP.Three.Behrend

Goal state before:
pp: N : ℕ
hN : 2 ≤ N
hN' : N ≤ 4096
⊢ ↑N * rexp (-4 * √(log ↑N)) ≤ 1

Tactic:
by
  rw [← log_le_log_iff (mul_pos (cast_pos.2 (zero_lt_two.trans_le hN)) (exp_pos _)) zero_lt_one,
    log_one, log_mul (cast_pos.2 (zero_lt_two.trans_le hN)).ne' (exp_pos _).ne', log_exp, neg_mul, ←
    sub_eq_add_neg, sub_nonpos, ←
    div_le_iff₀ (Real.sqrt_pos.2 <| log_pos <| one_lt_cast.2 <| one_lt_two.trans_le hN), div_sqrt,
    sqrt_le_left zero_le_four, log_le_iff_le_exp (cast_pos.2 (zero_lt_two.trans_le hN))]
  norm_num1
  apply le_trans _ four_zero_nine_six_lt_exp_sixteen.le
  exact mod_cast hN'

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

Goal state before:
pp: G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : Group G
A B : Finset G
hA : ∀ A' ⊆ A, #(A * B) * #A' ≤ #(A' * B) * #A
x : G
C : Finset G
a✝ : x ∉ C
ih : #(C * A * B) * #A ≤ #(A * B) * #(C * A)
A' : Finset G := A ∩ ({x}⁻¹ * C * A)
hA' : A' = A ∩ ({x}⁻¹ * C * A)
C' : Finset G := insert x C
hC' : C' = insert x C
h₀ : {x} * A' = {x} * A ∩ (C * A)
h₁ : C' * A * B = C * A * B ∪ ({x} * A * B) \ ({x} * A' * B)
h₂ : {x} * A' * B ⊆ {x} * A * B
⊢ #(A * B) * (#(C * A) + #A - #A') = #(A * B) * #({x} * A ∪ C * A)

Tactic:
← card_singleton_mul x A,

Goal state after:
G : Type u_1
inst✝¹ : DecidableEq G
inst✝ : Group G
A B : Finset G
hA : ∀ A' ⊆ A, #(A * B) * #A' ≤ #(A' * B) * #A
x : G
C : Finset G
a✝ : x ∉ C
ih : #(C * A * B) * #A ≤ #(A * B) * #(C * A)
A' : Finset G := A ∩ ({x}⁻¹ * C * A)
hA' : A' = A ∩ ({x}⁻¹ * C * A)
C' : Finset G := insert x C
hC' : C' = insert x C
h₀ : {x} * A' = {x} * A ∩ (C * A)
h₁ : C' * A * B = C * A * B ∪ ({x} * A * B) \ ({x} * A' * B)
h₂ : {x} * A' * B ⊆ {x} * A * B
⊢ #(A * B) * (#(C * A) + #({x} * A) - #A') = #(A * B) * #({x} * A ∪ C * A)
Module: Mathlib.Combinatorics.Additive.ETransform

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

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_inter, smul_inv_smul, inter_comm, union_eq_left]
    exact inter_subset_union

Goal state after:
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
Module: Mathlib.Combinatorics.SimpleGraph.Dart

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
⊢ ∀ {d : G.Dart} {u v : V}, d.edge = s(u, v) ↔ d.toProd = (u, v) ∨ d.toProd = (v, u)

Tactic:
rintro ⟨p, h⟩ _ _
  simp

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

Goal state before:
pp: case succ
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
ih :
  ∀ (ε : Fin m → ℤ),
    (∀ (i : Fin m), |ε i| = 1) → ↑(#(List.map (fun i ↦ A ^ ε i) (finRange m)).prod) ≤ k ^ (m - 2) * ↑(#A)
ε : Fin (m + 1) → ℤ
hε : ∀ (i : Fin (m + 1)), |ε i| = 1
⊢ ↑(#(List.map (fun i ↦ A ^ ε i) (finRange (m + 1))).prod) ≤ k ^ (m + 1 - 2) * ↑(#A)

Tactic:
| succ m hm ih =>

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
inst✝ : DecidableEq V
v : V
⊢ {d | d.toProd.1 = v} = image (G.dartOfNeighborSet v) univ

Tactic:
by
  ext d
  simp only [mem_image, true_and, mem_filter, SetCoe.exists, mem_univ]
  constructor
  · rintro rfl
    exact ⟨_, d.adj, by ext <;> rfl⟩
  · rintro ⟨e, he, rfl⟩
    rfl

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

Goal state before:
pp: case e'_3
V : Type u
G : SimpleGraph V
inst✝² : Fintype V
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableEq V
e : Sym2 V
v w : V
h : Quot.mk (Sym2.Rel V) (v, w) ∈ G.edgeSet
d : G.Dart := { fst := v, snd := w, adj := h }
⊢ 2 = #{d, d.symm}

Tactic:
rw [card_insert_of_notMem, card_singleton]

Goal state after:
case e'_3
V : Type u
G : SimpleGraph V
inst✝² : Fintype V
inst✝¹ : DecidableRel G.Adj
inst✝ : DecidableEq V
e : Sym2 V
v w : V
h : Quot.mk (Sym2.Rel V) (v, w) ∈ G.edgeSet
d : G.Dart := { fst := v, snd := w, adj := h }
⊢ d ∉ {d.symm}
Module: Mathlib.Combinatorics.SimpleGraph.DegreeSum

Goal state before:
pp: V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
⊢ ∑ b ∈ G.edgeFinset, #{a | a.edge = b} = 2 * #G.edgeFinset

Tactic:
rw [← mul_comm, sum_const_nat]

Goal state after:
V : Type u
G : SimpleGraph V
inst✝¹ : Fintype V
inst✝ : DecidableRel G.Adj
⊢ ∀ x ∈ G.edgeFinset, #{a | a.edge = x} = 2
Module: Mathlib.Combinatorics.SimpleGraph.Maps

Goal state before:
pp: V : Type u_1
W : Type u_2
G : SimpleGraph V
e : V ≃ W
⊢ SimpleGraph.comap (⇑e.symm.toEmbedding) G = SimpleGraph.map (⇑e.toEmbedding) G

Tactic:
by
  ext; simp only [← Equiv.eq_symm_apply, comap_adj, map_adj, Equiv.toEmbedding_apply,
    exists_eq_right_right, exists_eq_right]

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

Goal state before:
pp: V : Type u_1
W : Type u_2
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
hinj : Injective ⇑f
e₁ : Sym2 V
h₁ : e₁ ∈ G.edgeSet
e₂ : Sym2 V
h₂ : e₂ ∈ G.edgeSet
⊢ ⟨Sym2.map (⇑f) e₁, ⋯⟩ = ⟨Sym2.map (⇑f) e₂, ⋯⟩ → ⟨e₁, h₁⟩ = ⟨e₂, h₂⟩

Tactic:
rw [Subtype.mk_eq_mk]

Goal state after:
V : Type u_1
W : Type u_2
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
hinj : Injective ⇑f
e₁ : Sym2 V
h₁ : e₁ ∈ G.edgeSet
e₂ : Sym2 V
h₂ : e₂ ∈ G.edgeSet
⊢ Sym2.map (⇑f) e₁ = Sym2.map (⇑f) e₂ → ⟨e₁, h₁⟩ = ⟨e₂, h₂⟩
Module: Mathlib.Combinatorics.SimpleGraph.Maps

Goal state before:
pp: V : Type u_1
W : Type u_2
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
hinj : Injective ⇑f
e₁ : Sym2 V
h₁ : e₁ ∈ G.edgeSet
e₂ : Sym2 V
h₂ : e₂ ∈ G.edgeSet
⊢ Sym2.map (⇑f) e₁ = Sym2.map (⇑f) e₂ → ⟨e₁, h₁⟩ = ⟨e₂, h₂⟩

Tactic:
rw [Subtype.mk_eq_mk]

Goal state after:
V : Type u_1
W : Type u_2
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
hinj : Injective ⇑f
e₁ : Sym2 V
h₁ : e₁ ∈ G.edgeSet
e₂ : Sym2 V
h₂ : e₂ ∈ G.edgeSet
⊢ Sym2.map (⇑f) e₁ = Sym2.map (⇑f) e₂ → e₁ = e₂
Module: Mathlib.Combinatorics.SimpleGraph.Maps

Goal state before:
pp: V : Type u_1
W : Type u_2
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
hinj : Injective ⇑f
e₁ : Sym2 V
h₁ : e₁ ∈ G.edgeSet
e₂ : Sym2 V
h₂ : e₂ ∈ G.edgeSet
⊢ Sym2.map (⇑f) e₁ = Sym2.map (⇑f) e₂ → e₁ = e₂

Tactic:
rw [Subtype.mk_eq_mk]

Goal state after:
V : Type u_1
W : Type u_2
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
hinj : Injective ⇑f
e₁ : Sym2 V
h₁ : e₁ ∈ G.edgeSet
e₂ : Sym2 V
h₂ : e₂ ∈ G.edgeSet
⊢ Sym2.map (⇑f) e₁ = Sym2.map (⇑f) e₂ → e₁ = e₂
Module: Mathlib.Combinatorics.SimpleGraph.Finite

Goal state before:
pp: V : Type u_1
G : SimpleGraph V
v : V
inst✝¹ : Fintype ↑(G.neighborSet v)
inst✝ : DecidableEq V
⊢ #(G.incidenceFinset v) = G.degree v

Tactic:
by
  rw [← G.card_incidenceSet_eq_degree]
  apply Set.toFinset_card

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

Goal state before:
pp: V : Type u_1
G H : SimpleGraph V
v : V
inst✝² : Fintype ↑(G.neighborSet v)
inst✝¹ : DecidableEq V
inst✝ : Fintype ↑(H.neighborSet v)
h : Disjoint G H
⊢ Disjoint (G.incidenceFinset v) (H.incidenceFinset v)

Tactic:
simp [← Finset.disjoint_coe, disjoint_incidenceSet.mpr h 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:
rw [← 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:
rw [← 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: α : Type u_1
inst✝² : DistribLattice α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
a b c : α
P : Finpartition a
hb : b ≤ a
⊢ ((image (fun x ↦ x ⊓ b) P.parts).erase ⊥).sup id = b

Tactic:
simp only [sup_erase_bot, sup_image, Function.id_comp, (sup_inf_distrib_right ..).symm]

Goal state after:
α : Type u_1
inst✝² : DistribLattice α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
a b c : α
P : Finpartition a
hb : b ≤ a
⊢ (P.parts.sup fun i ↦ i) ⊓ b = b
Module: Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : Preadditive C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝ : Pretriangulated C
t : TStructure C
i j : EInt
f : i ⟶ j
X : C
⊢ (t.eTruncLT.obj i).map ((t.eTruncLTι j).app X) ≫ (t.eTruncLT.map f).app X =
    (t.eTruncLTι i).app ((t.eTruncLT.obj j).obj X)

Tactic:
by
  dsimp [eTruncLTι]
  rw [show homOfLE le_top = f ≫ homOfLE le_top by rfl]
  induction j using WithBotTop.rec with simp [truncLT_map_truncLTι_app]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : GeneralizedBooleanAlgebra α
inst✝ : DecidableEq α
a b : α
P : Finpartition a
hab : a = b
⊢ (P.extendOfLE ⋯).parts = P.parts

Tactic:
subst hab

Goal state after:
α : Type u_1
inst✝¹ : GeneralizedBooleanAlgebra α
inst✝ : DecidableEq α
a : α
P : Finpartition a
⊢ (P.extendOfLE ⋯).parts = P.parts
Module: Mathlib.Order.Partition.Finpartition

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
s✝ t u : Finset α
P : Finpartition s✝
a✝ : α
s : Setoid α
x : Finset α
inst✝ : DecidableRel ⇑s
a : α
⊢ (a ∈ x.sup fun a ↦ {b ∈ x | s a b}) ↔ a ∈ x

Tactic:
mem_sup,

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
s✝ t u : Finset α
P : Finpartition s✝
a✝ : α
s : Setoid α
x : Finset α
inst✝ : DecidableRel ⇑s
a : α
⊢ (∃ i ∈ x, a ∈ {b ∈ x | s i b}) ↔ a ∈ x
Module: Mathlib.Order.Partition.Finpartition

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
s✝ t u : Finset α
P : Finpartition s✝
a : α
s : Finset α
F : Finset (Finset α)
z : α
Q : Finset (Finset α)
hQ : Q ∈ F.powerset
hz1 : z ∈ s ∧ ∀ t ∈ F, t ∈ Q ↔ z ∈ t
R : Finset (Finset α)
hR : R ∈ F.powerset
hz2 : z ∈ s ∧ ∀ t ∈ F, t ∈ R ↔ z ∈ t
h : {i ∈ s | ∀ t ∈ F, t ∈ Q ↔ i ∈ t} ≠ {i ∈ s | ∀ t ∈ F, t ∈ R ↔ i ∈ t}
⊢ Q = R

Tactic:
rw [mem_powerset] at hQ hR

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
s✝ t u : Finset α
P : Finpartition s✝
a : α
s : Finset α
F : Finset (Finset α)
z : α
Q : Finset (Finset α)
hQ : Q ⊆ F
hz1 : z ∈ s ∧ ∀ t ∈ F, t ∈ Q ↔ z ∈ t
R : Finset (Finset α)
hR : R ⊆ F
hz2 : z ∈ s ∧ ∀ t ∈ F, t ∈ R ↔ z ∈ t
h : {i ∈ s | ∀ t ∈ F, t ∈ Q ↔ i ∈ t} ≠ {i ∈ s | ∀ t ∈ F, t ∈ R ↔ i ∈ t}
⊢ Q = R
Module: Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc

Goal state before:
pp: C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Preadditive C
inst✝⁴ : HasZeroObject C
inst✝³ : HasShift C ℤ
inst✝² : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝¹ : Pretriangulated C
t : TStructure C
inst✝ : IsTriangulated C
a : EInt
X : C
⊢ a ≤ a

Tactic:
by rfl

Goal state after:
Module: Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc

Goal state before:
pp: case coe.top.left
C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Preadditive C
inst✝⁴ : HasZeroObject C
inst✝³ : HasShift C ℤ
inst✝² : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝¹ : Pretriangulated C
t : TStructure C
inst✝ : IsTriangulated C
a b✝ : EInt
X : C
b : ℤ
⊢ IsZero ((t.truncLT b).obj (Functor.obj 0 ((t.truncLT b).obj X)))

pp: case coe.top.right
C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Preadditive C
inst✝⁴ : HasZeroObject C
inst✝³ : HasShift C ℤ
inst✝² : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝¹ : Pretriangulated C
t : TStructure C
inst✝ : IsTriangulated C
a b✝ : EInt
X : C
b : ℤ
⊢ IsZero ((t.truncLT b).obj (Functor.obj 0 X))

Tactic:
all_goals exact Functor.map_isZero _ (Functor.zero_obj _)

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

Goal state before:
pp: α : Type u_1
𝕜 : Type u_2
inst✝³ : Field 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
s t s' : Finset α
hs' : s' ⊆ s
t' : Finset α
ht' : t' ⊆ t
hs : ↑(#s) ≤ ↑(#s')
ht : ↑(#t) ≤ ↑(#t')
⊢ |↑(G.edgeDensity s t') - ↑(G.edgeDensity s t)| < 1

Tactic:
eq_of_subset_of_card_le ht' (Nat.cast_le.1 ht),

Goal state after:
α : Type u_1
𝕜 : Type u_2
inst✝³ : Field 𝕜
inst✝² : LinearOrder 𝕜
inst✝¹ : IsStrictOrderedRing 𝕜
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
s t s' : Finset α
hs' : s' ⊆ s
t' : Finset α
ht' : t' ⊆ t
hs : ↑(#s) ≤ ↑(#s')
ht : ↑(#t) ≤ ↑(#t')
⊢ |↑(G.edgeDensity s t) - ↑(G.edgeDensity s t)| < 1
Module: Mathlib.Combinatorics.SimpleGraph.Subgraph

Goal state before:
pp: V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
U : Type u_2
G'' : SimpleGraph U
H : G.Subgraph
f : G →g G'
g : G' →g G''
⊢ Subgraph.map (g.comp f) H = Subgraph.map g (Subgraph.map f H)

Tactic:
by ext <;> simp [Subgraph.map]

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

Goal state before:
pp: case refine_2
V : Type u
W : Type v
G : SimpleGraph V
G' : SimpleGraph W
f : G →g G'
H : G.Subgraph
H' : G'.Subgraph
h : Subgraph.map f H ≤ H'
v w : V
hvw : H.Adj v w
⊢ H'.Adj (f v) (f w)

Tactic:
exact h.2 ⟨v, w, hvw, rfl, rfl⟩

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v✝¹ v v✝ : V
h : G.Adj u v✝
p : G.Walk v✝ v
⊢ { fst := u, snd := v✝, adj := h }.toProd.2 = v✝

Tactic:
by rfl

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v w : V
motive : {u w : V} → (p : G.Walk u w) → ¬p.Nil → Sort u_1
cons : {u v w : V} → (h : G.Adj u v) → (q : G.Walk v w) → motive (Walk.cons h q) ⋯
h' : G.Adj u v
q' : G.Walk v w
⊢ notNilRec (fun {u v w} ↦ cons) (Walk.cons h' q') ⋯ = cons h' q'

Tactic:
by rfl

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

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

Tactic:
have : (m : ℝ) / (m + 1) = 1 - 1 / (m + 1) := by
    rw [one_sub_div coe_m_add_one_pos.ne', add_sub_cancel_right]
  rw [this, sub_sq, one_pow, mul_one]
  refine le_trans ?_ (le_add_of_nonneg_right <| sq_nonneg _)
  rw [sub_le_sub_iff_left, ← le_div_iff₀' (show (0 : ℝ) < 2 by simp), div_div,
    one_div_le coe_m_add_one_pos, one_div_div]
  · refine le_trans ?_ (le_add_of_nonneg_right zero_le_one)
    norm_num
    apply hundred_div_ε_pow_five_le_m hPα hPε
  sz_positivity

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
inst✝ : DecidableEq V
u v w : V
p : G.Walk v w
h : u ∈ p.support
huw : u ≠ w
hl : (p.takeUntil u h).length = p.length
⊢ (p.takeUntil u h).length ≤ (p.takeUntil u h).length

Tactic:
by rfl

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v w : V
h : G.Adj u v
p : G.Walk v w
⊢ (cons h p).IsPath ↔ p.IsPath ∧ u ∉ p.support

Tactic:
by
  constructor <;> simp +contextual [isPath_def]

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

Goal state before:
pp: case nil.zero
V : Type u
G : SimpleGraph V
u v : V
m : ℕ
u✝ : V
⊢ nil.take (m + 0) ≍ (nil.take 0).append ((nil.drop 0).take m)

Tactic:
simp [take, drop]

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

Goal state before:
pp: case nil.succ
V : Type u
G : SimpleGraph V
u v : V
m : ℕ
u✝ : V
n✝ : ℕ
⊢ nil.take (m + (n✝ + 1)) ≍ (nil.take (n✝ + 1)).append ((nil.drop (n✝ + 1)).take m)

Tactic:
simp [take, drop]

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

Goal state before:
pp: case cons.zero
V : Type u
G : SimpleGraph V
u v : V
m : ℕ
u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ : ∀ (n : ℕ), p✝.take (m + n) ≍ (p✝.take n).append ((p✝.drop n).take m)
⊢ (cons h✝ p✝).take (m + 0) ≍ ((cons h✝ p✝).take 0).append (((cons h✝ p✝).drop 0).take m)

Tactic:
simp [take, drop]

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

Goal state before:
pp: case cons.succ
V : Type u
G : SimpleGraph V
u v : V
m : ℕ
u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ : ∀ (n : ℕ), p✝.take (m + n) ≍ (p✝.take n).append ((p✝.drop n).take m)
n✝ : ℕ
⊢ (cons h✝ p✝).take (m + (n✝ + 1)) ≍ ((cons h✝ p✝).take (n✝ + 1)).append (((cons h✝ p✝).drop (n✝ + 1)).take m)

Tactic:
simp [take, drop]

Goal state after:
case cons.succ
V : Type u
G : SimpleGraph V
u v : V
m : ℕ
u✝ v✝ w✝ : V
h✝ : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
p_ih✝ : ∀ (n : ℕ), p✝.take (m + n) ≍ (p✝.take n).append ((p✝.drop n).take m)
n✝ : ℕ
⊢ cons h✝ (p✝.take (m + n✝)) ≍ cons h✝ ((p✝.take n✝).append ((p✝.drop n✝).take m))
Module: Mathlib.Combinatorics.SimpleGraph.Paths

Goal state before:
pp: V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
u✝ u' v✝ w : V
p✝ : G.Walk u✝ v✝
f : G →g G'
inst✝ : DecidableEq V
u v : V
p : G.Walk u v
⊢ Decidable p.IsPath

Tactic:
by
  rw [isPath_def]
  infer_instance

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Basic

Goal state before:
pp: case refine_2
α : Type u_1
G : SimpleGraph α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : DecidableRel G.Adj
hG : G.LocallyLinear
a b c : α
hab : G.Adj a b
hac : G.Adj a c
hbc : G.Adj b c
⊢ #(bipartiteBelow (fun e s ↦ e ∈ s.sym2) G.edgeFinset {a, b, c}) ≤ 3

Tactic:
calc
    _ ≤ #{s(a, b), s(a, c), s(b, c)} := card_le_card ?_
    _ ≤ 3 := (card_insert_le _ _).trans (succ_le_succ <| (card_insert_le _ _).trans_eq <| by
      rw [card_singleton])

Goal state after:
case refine_2
α : Type u_1
G : SimpleGraph α
inst✝² : DecidableEq α
inst✝¹ : Fintype α
inst✝ : DecidableRel G.Adj
hG : G.LocallyLinear
a b c : α
hab : G.Adj a b
hac : G.Adj a c
hbc : G.Adj b c
⊢ bipartiteBelow (fun e s ↦ e ∈ s.sym2) G.edgeFinset {a, b, c} ⊆ {s(a, b), s(a, c), s(b, c)}
Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Counting

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
s t : Finset α
dst : 2 * ε ≤ ↑(G.edgeDensity s t)
hst : G.IsUniform ε s t
⊢ ↑(#(G.badVertices ε s t)) ≤ ↑(#s) * ε

Tactic:
by
  have hε : ε ≤ 1 := (le_mul_of_one_le_left hst.pos.le (by simp)).trans
    (dst.trans <| mod_cast edgeDensity_le_one _ _ _)
  by_contra! h
  have : |(G.edgeDensity (badVertices G ε s t) t - G.edgeDensity s t : ℝ)| < ε :=
    hst (filter_subset _ _) Subset.rfl h.le (mul_le_of_le_one_right (Nat.cast_nonneg _) hε)
  rw [abs_sub_lt_iff] at this
  linarith [G.edgeDensity_badVertices_le hst.pos.le dst]

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

Goal state before:
pp: case hba
α : 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
hε₁ : ε ≤ 1
hU : U ∈ P.parts
hV : V ∈ P.parts
hUV : U ≠ V
hunif : ¬G.IsUniform ε U V
hm : 0 ≤ 1 - (↑m)⁻¹
hε : 0 ≤ 1 - ε / 10
hε₀ : 0 < ε
⊢ 9 ≤ ↑m

pp: case h₂
α : 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
hε₁ : ε ≤ 1
hU : U ∈ P.parts
hV : V ∈ P.parts
hUV : U ≠ V
hunif : ¬G.IsUniform ε U V
hm : 0 ≤ 1 - (↑m)⁻¹
hε : 0 ≤ 1 - ε / 10
hε₀ : 0 < ε
⊢ ε ≤ ↑(#(G.nonuniformWitness ε U V)) / ↑(#U)

Tactic:
exacts [mod_cast (show 9 ≤ 100 by simp).trans (hundred_le_m hPα hPε hε₁),
          (le_div_iff₀' <| cast_pos.2 (P.nonempty_of_mem_parts hU).card_pos).2 <|
           G.le_card_nonuniformWitness hunif]

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite

Goal state before:
pp: case refine_3
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
inst✝³ : DecidableEq α
inst✝² : DecidableEq β
inst✝¹ : DecidableEq γ
inst✝ : ExplicitDisjoint t
a : α
b : β
c : γ
habc : (a, b, c) ∈ t
x : α
hxyz : (x, b, c) ∈ t
h' : ¬toTriangle (a, b, c) = toTriangle (x, b, c)
this : a = x → b = b → ¬c = c
⊢ False

Tactic:
exact this (ExplicitDisjoint.inj₀ habc hxyz) rfl rfl

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

Goal state before:
pp: case pos
α : Type u_1
inst✝² : CommGroup α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Finset α
d : ℕ
hs : ∀ s' ⊆ s, MulDissociated ↑s' → #s' ≤ d
s' : Finset α
hs' : Maximal (fun x ↦ x ⊆ s ∧ MulDissociated ↑x) s'
a : α
ha : a ∈ s
ha' : a ∉ s'
t u : Finset α
ht : t ⊆ s'
hu : ↑u ⊆ ↑(insert a s')
htu : Disjoint t u ∧ t ≠ u ∧ ∏ a ∈ t, a = ∏ a ∈ u, a
hat : a ∉ t
hau : a ∈ u
⊢ a ∈ s'.mulSpan

Tactic:
have : a = (∏ b ∈ t, b) / ∏ b ∈ u.erase a, b := by
      rw [prod_erase_eq_div hau, htu.2.2, div_div_self']

Goal state after:
case pos
α : Type u_1
inst✝² : CommGroup α
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Finset α
d : ℕ
hs : ∀ s' ⊆ s, MulDissociated ↑s' → #s' ≤ d
s' : Finset α
hs' : Maximal (fun x ↦ x ⊆ s ∧ MulDissociated ↑x) s'
a : α
ha : a ∈ s
ha' : a ∉ s'
t u : Finset α
ht : t ⊆ s'
hu : ↑u ⊆ ↑(insert a s')
htu : Disjoint t u ∧ t ≠ u ∧ ∏ a ∈ t, a = ∏ a ∈ u, a
hat : a ∉ t
hau : a ∈ u
this : a = (∏ b ∈ t, b) / ∏ b ∈ u.erase a, b
⊢ a ∈ s'.mulSpan
Module: Mathlib.Combinatorics.Additive.DoublingConst

Goal state before:
pp: G : Type u_1
inst✝³ : Group G
inst✝² : DecidableEq G
𝕜 : Type u_3
inst✝¹ : Semifield 𝕜
inst✝ : CharZero 𝕜
A B : Finset G
⊢ ↑σₘ[A, B] * ↑(#A) = ↑(#(A * B))

Tactic:
by
  norm_cast; exact mulConst_mul_card _ _

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

Goal state before:
pp: G : Type u_1
inst✝¹ : CommGroup G
inst✝ : DecidableEq G
A : Finset G
hA' : A.Nonempty
⊢ ↑(#(A * A)) * ↑(#A) ≤ ↑(#(A / A)) * ↑(#(A / A))

Tactic:
by norm_cast; exact ruzsa_triangle_inequality_mul_div_div ..

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

Goal state before:
pp: case prime
p : ℕ
hp : Nat.Prime p
ι : Type u_1
s : Finset ι
a : ι → ℤ
hs : 2 * p - 1 ≤ #s
⊢ ∃ t ⊆ s, #t = p ∧ ↑p ∣ ∑ i ∈ t, a i

Tactic:
have := Fact.mk hp
    obtain ⟨t, hts, ht⟩ := exists_subset_card_eq hs
    obtain ⟨u, hut, hu⟩ := Int.erdos_ginzburg_ziv_prime a ht
    exact ⟨u, hut.trans hts, hu⟩

Goal state after:
Module: Mathlib.Combinatorics.Colex

Goal state before:
pp: α : Type u_1
inst✝ : PartialOrder α
s : Finset α
a : α
⊢ toColex s ≤ toColex {a} ∧ toColex s ≠ toColex {a} ↔ ∀ b ∈ s, b < a

Tactic:
toColex_le_singleton,

Goal state after:
α : Type u_1
inst✝ : PartialOrder α
s : Finset α
a : α
⊢ (∀ b ∈ s, b ≤ a ∧ (a ∈ s → b = a)) ∧ toColex s ≠ toColex {a} ↔ ∀ b ∈ s, b < a