mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Combinatorics.SimpleGraph.Paths

Goal state before:
pp: case refine_3
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
q : G.Walk v u
hp : p.IsPath
hq : q.IsPath
h : p.support.tail.Disjoint q.support.tail
hn : 1 < p.length ∨ 1 < q.length
⊢ (p.append q).support.tail.Nodup

Tactic:
rw [tail_support_append, List.nodup_append']

Goal state after:
case refine_3
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
q : G.Walk v u
hp : p.IsPath
hq : q.IsPath
h : p.support.tail.Disjoint q.support.tail
hn : 1 < p.length ∨ 1 < q.length
⊢ p.support.tail.Nodup ∧ q.support.tail.Nodup ∧ p.support.tail.Disjoint q.support.tail
Module: Mathlib.Combinatorics.SimpleGraph.Clique

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
n : ℕ
inst✝ : DecidableEq α
h : Maximal (fun H ↦ H.CliqueFree (n + 1)) G
x y : α
hne : x ≠ y
hn : ¬G.Adj x y
⊢ ∃ s, x ∉ s ∧ y ∉ s ∧ G.IsNClique n (insert x s) ∧ G.IsNClique n (insert y s)

Tactic:
obtain ⟨t, hc⟩ := not_forall_not.1 <| h.not_prop_of_gt <| G.lt_sup_edge _ _ hne hn

Goal state after:
α : Type u_1
G : SimpleGraph α
n : ℕ
inst✝ : DecidableEq α
h : Maximal (fun H ↦ H.CliqueFree (n + 1)) G
x y : α
hne : x ≠ y
hn : ¬G.Adj x y
t : Finset α
hc : (G ⊔ edge x y).IsNClique (n + 1) t
⊢ ∃ s, x ∉ s ∧ y ∉ s ∧ G.IsNClique n (insert x s) ∧ G.IsNClique n (insert y s)
Module: Mathlib.Combinatorics.SimpleGraph.Paths

Goal state before:
pp: V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
f : G →g G'
u v : V
p : G.Walk u v
hp : (Walk.map f p).support.Nodup
⊢ p.support.Nodup

Tactic:
support_map

Goal state after:
V : Type u
V' : Type v
G : SimpleGraph V
G' : SimpleGraph V'
f : G →g G'
u v : V
p : G.Walk u v
hp : (List.map (⇑f) p.support).Nodup
⊢ p.support.Nodup
Module: Mathlib.Combinatorics.SimpleGraph.Clique

Goal state before:
pp: α : Type u_3
G : SimpleGraph α
inst✝ : Finite α
s : Finset α
M : G.IsMaximumIndepSet s
⊢ Maximal G.IsIndepSet ↑s

Tactic:
by
  rw [← isMaximalClique_compl]
  rw [← isMaximumClique_compl] at M
  exact IsMaximumClique.isMaximalClique s M

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

Goal state before:
pp: α : Type u_1
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
ε : ℝ
s t u : Finset α
inst✝ : DecidableEq α
dst : 2 * ε ≤ ↑(G.edgeDensity s t)
dsu : 2 * ε ≤ ↑(G.edgeDensity s u)
dtu : 2 * ε ≤ ↑(G.edgeDensity t u)
utu : G.IsUniform ε t u
x : α
hx : x ∈ s \ (G.badVertices ε s t ∪ G.badVertices ε s u)
⊢ ε ^ 3 * ↑(#t) * ↑(#u) ≤
    ↑(#(image (fun x_1 ↦ (x, x_1))
          ({x ∈ {y ∈ t | G.Adj x y} ×ˢ {y ∈ u | G.Adj x y} |
            match x with
            | (y, z) => G.Adj y z})))

Tactic:
simp only [mem_sdiff, badVertices, mem_union, not_or, mem_filter, not_and_or, not_lt] at hx

Goal state after:
α : Type u_1
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
ε : ℝ
s t u : Finset α
inst✝ : DecidableEq α
dst : 2 * ε ≤ ↑(G.edgeDensity s t)
dsu : 2 * ε ≤ ↑(G.edgeDensity s u)
dtu : 2 * ε ≤ ↑(G.edgeDensity t u)
utu : G.IsUniform ε t u
x : α
hx :
  x ∈ s ∧
    (x ∉ s ∨ (↑(G.edgeDensity s t) - ε) * ↑(#t) ≤ ↑(#({y ∈ t | G.Adj x y}))) ∧
      (x ∉ s ∨ (↑(G.edgeDensity s u) - ε) * ↑(#u) ≤ ↑(#({y ∈ u | G.Adj x y})))
⊢ ε ^ 3 * ↑(#t) * ↑(#u) ≤
    ↑(#(image (fun x_1 ↦ (x, x_1))
          ({x ∈ {y ∈ t | G.Adj x y} ×ˢ {y ∈ u | G.Adj x y} |
            match x with
            | (y, z) => G.Adj y z})))
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
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 < ε
⊢ (1 - ε / 10) * ↑(#(G.nonuniformWitness ε U V)) * ((1 - (↑m)⁻¹) / ↑(#U)) ≤
    ↑(#((star hP G ε hU V).biUnion id)) * ((1 - (↑m)⁻¹) / ↑(#U))

Tactic:
by
      gcongr
      exact one_sub_eps_mul_card_nonuniformWitness_le_card_star hV hUV hunif hPε hε₁

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
𝕜 : Type u_4
inst✝⁹ : Field 𝕜
inst✝⁸ : LinearOrder 𝕜
inst✝⁷ : IsStrictOrderedRing 𝕜
t : Finset (α × β × γ)
inst✝⁶ : DecidableEq α
inst✝⁵ : DecidableEq β
inst✝⁴ : DecidableEq γ
inst✝³ : Fintype α
inst✝² : Fintype β
inst✝¹ : Fintype γ
inst✝ : ExplicitDisjoint t
ε : 𝕜
ht : ε * ↑((Fintype.card α + Fintype.card β + Fintype.card γ) ^ 2) ≤ ↑(#t)
⊢ ε * ↑(Fintype.card (α ⊕ β ⊕ γ) ^ 2) ≤ ↑(#(map toTriangle t))

Tactic:
simpa [add_assoc] using ht

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

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A B : Finset G
⊢ δₘ[A, B] ≤ ↑(#B)

Tactic:
obtain rfl | hA' := A.eq_empty_or_nonempty
  · simp
  rw [divConst, div_le_iff₀' (by positivity)]
  exact mod_cast card_div_le

Goal state after:
Module: Mathlib.Combinatorics.Additive.Corner.Roth

Goal state before:
pp: n : ℕ
ε : ℝ
hε : 0 < ε
hG : cornersTheoremBound (ε / 3) ≤ n
A : Finset ℕ
hAn : ↑A ⊆ Set.Iio n
hAε : ε * ↑n ≤ ↑(#A)
hA : ThreeAPFree (Fin.val '' Nat.cast '' ↑A)
this✝¹ : ↑A = Fin.val '' Nat.cast '' ↑A
this✝ : IsAddFreimanIso 2 (Set.Iio ↑n) (Set.Iio n) Fin.val
this : ThreeAPFree ↑(image (fun x ↦ ↑x) A)
⊢ ε / 3 * (2 * ↑n + 1) ≤ ε / 3 * (2 * ↑n + ↑n)

Tactic:
by gcongr; simp; unfold cornersTheoremBound at hG; lia

Goal state after:
Module: Mathlib.FieldTheory.ChevalleyWarning

Goal state before:
pp: K : Type u_1
σ : Type u_2
ι : Type u_3
inst✝⁵ : Fintype K
inst✝⁴ : Field K
inst✝³ : Fintype σ
inst✝² : DecidableEq σ
inst✝¹ : DecidableEq K
p : ℕ
inst✝ : CharP K p
s : Finset ι
f : ι → MvPolynomial σ K
h : ∑ i ∈ s, (f i).totalDegree < Fintype.card σ
hq : 0 < q - 1
S : Finset (σ → K) := {x | ∀ i ∈ s, (eval x) (f i) = 0}
⊢ p ∣ Fintype.card { x // ∀ i ∈ s, (eval x) (f i) = 0 }

Tactic:
have hS (x : σ → K) : x ∈ S ↔ ∀ i ∈ s, eval x (f i) = 0 := by simp [S]

Goal state after:
K : Type u_1
σ : Type u_2
ι : Type u_3
inst✝⁵ : Fintype K
inst✝⁴ : Field K
inst✝³ : Fintype σ
inst✝² : DecidableEq σ
inst✝¹ : DecidableEq K
p : ℕ
inst✝ : CharP K p
s : Finset ι
f : ι → MvPolynomial σ K
h : ∑ i ∈ s, (f i).totalDegree < Fintype.card σ
hq : 0 < q - 1
S : Finset (σ → K) := {x | ∀ i ∈ s, (eval x) (f i) = 0}
hS : ∀ (x : σ → K), x ∈ S ↔ ∀ i ∈ s, (eval x) (f i) = 0
⊢ p ∣ Fintype.card { x // ∀ i ∈ s, (eval x) (f i) = 0 }
Module: Mathlib.Combinatorics.Additive.ErdosGinzburgZiv

Goal state before:
pp: case refine_2.refine_2
ι : Type u_1
p : ℕ
inst✝ : Fact (Nat.Prime p)
s : Finset ι
a : ι → ZMod p
hs : #s = 2 * p - 1
this : NeZero p
N : ℕ := Fintype.card { x // (eval x) (f₁ s a) = 0 ∧ (eval x) (f₂ s a) = 0 }
zero_sol : { x // (eval x) (f₁ s a) = 0 ∧ (eval x) (f₂ s a) = 0 } := ⟨0, ⋯⟩
hN₀ : 0 < N
hs' : 2 * p - 1 = Fintype.card ↥s
hpN : p ∣ N
x : { x // (eval x) (f₁ s a) = 0 ∧ (eval x) (f₂ s a) = 0 }
hx : x ≠ zero_sol
⊢ p ∣ #{a_1 | ↑x a_1 ≠ 0}

Tactic:
rw [← CharP.cast_eq_zero_iff (ZMod p), ← Finset.sum_boole]

Goal state after:
case refine_2.refine_2
ι : Type u_1
p : ℕ
inst✝ : Fact (Nat.Prime p)
s : Finset ι
a : ι → ZMod p
hs : #s = 2 * p - 1
this : NeZero p
N : ℕ := Fintype.card { x // (eval x) (f₁ s a) = 0 ∧ (eval x) (f₂ s a) = 0 }
zero_sol : { x // (eval x) (f₁ s a) = 0 ∧ (eval x) (f₂ s a) = 0 } := ⟨0, ⋯⟩
hN₀ : 0 < N
hs' : 2 * p - 1 = Fintype.card ↥s
hpN : p ∣ N
x : { x // (eval x) (f₁ s a) = 0 ∧ (eval x) (f₂ s a) = 0 }
hx : x ≠ zero_sol
⊢ (∑ x_1, if ↑x x_1 ≠ 0 then 1 else 0) = 0
Module: Mathlib.LinearAlgebra.CrossProduct

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
u v w : Fin 3 → R
⊢ u ⬝ᵥ (crossProduct v) w = det ![u, v, w]

Tactic:
rw [vec3_dotProduct, cross_apply, det_fin_three]

Goal state after:
R : Type u_1
inst✝ : CommRing R
u v w : Fin 3 → R
⊢ u 0 * ![v 1 * w 2 - v 2 * w 1, v 2 * w 0 - v 0 * w 2, v 0 * w 1 - v 1 * w 0] 0 +
        u 1 * ![v 1 * w 2 - v 2 * w 1, v 2 * w 0 - v 0 * w 2, v 0 * w 1 - v 1 * w 0] 1 +
      u 2 * ![v 1 * w 2 - v 2 * w 1, v 2 * w 0 - v 0 * w 2, v 0 * w 1 - v 1 * w 0] 2 =
    ![u, v, w] 0 0 * ![u, v, w] 1 1 * ![u, v, w] 2 2 - ![u, v, w] 0 0 * ![u, v, w] 1 2 * ![u, v, w] 2 1 -
            ![u, v, w] 0 1 * ![u, v, w] 1 0 * ![u, v, w] 2 2 +
          ![u, v, w] 0 1 * ![u, v, w] 1 2 * ![u, v, w] 2 0 +
        ![u, v, w] 0 2 * ![u, v, w] 1 0 * ![u, v, w] 2 1 -
      ![u, v, w] 0 2 * ![u, v, w] 1 1 * ![u, v, w] 2 0
Module: Mathlib.LinearAlgebra.CrossProduct

Goal state before:
pp: case neg.mp
F : Type u_2
inst✝ : Field F
v w : Fin 3 → F
hv : ¬v = 0
⊢ ¬LinearIndependent F ![v, w] → (crossProduct v) w = 0

Tactic:
LinearIndependent.pair_iff' hv,

Goal state after:
case neg.mp
F : Type u_2
inst✝ : Field F
v w : Fin 3 → F
hv : ¬v = 0
⊢ (¬∀ (a : F), a • v ≠ w) → (crossProduct v) w = 0
Module: Mathlib.Combinatorics.Additive.VerySmallDoubling

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
K : ℝ
A B : Finset G
x : G
hA : ↑(#(B * A)) ≤ K * ↑(#A)
hx : x ∈ B⁻¹ * B
⊢ (2 - K) * ↑(#A) ≤ ↑(#({ab ∈ A ×ˢ A | ab.1 * ab.2⁻¹ = x}))

Tactic:
simp only [mem_mul, mem_inv, exists_exists_and_eq_and] at hx
  obtain ⟨a, ha, b, hb, rfl⟩ := hx
  rw [card_mul_inv_eq_convolution_inv]
  simpa [card_smul_inter_smul] using le_card_smul_inter_smul hA ha hb

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

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
K : ℝ
A✝ B S : Finset G
a✝ b✝ c✝ d✝ x y : G
A : Finset G
h : ↑(#(A * A)) < 3 / 2 * ↑(#A)
h₁ : ∀ x ∈ A, ∀ y ∈ A, 1 / 2 * ↑(#A) < ↑(#(x •> A ∩ y •> A))
a : G
ha : a⁻¹ ∈ A
b : G
hb : b ∈ A
c : G
hc : c⁻¹ ∈ A
d : G
hd : d ∈ A
h₂ : 1 / 2 * ↑(#A) < ↑(#(A ∩ (a * b)⁻¹ •> A))
⊢ a * b * (c * d) ∈ A⁻¹ * A

Tactic:
have h₃ : (1 / 2 : ℚ) * #A < #(A ∩ (c * d) • A) := by
      refine (h₁ _ hc d hd).trans_le ?_
      rw [← card_smul_finset c]
      simp [smul_smul, smul_finset_inter]

Goal state after:
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
K : ℝ
A✝ B S : Finset G
a✝ b✝ c✝ d✝ x y : G
A : Finset G
h : ↑(#(A * A)) < 3 / 2 * ↑(#A)
h₁ : ∀ x ∈ A, ∀ y ∈ A, 1 / 2 * ↑(#A) < ↑(#(x •> A ∩ y •> A))
a : G
ha : a⁻¹ ∈ A
b : G
hb : b ∈ A
c : G
hc : c⁻¹ ∈ A
d : G
hd : d ∈ A
h₂ : 1 / 2 * ↑(#A) < ↑(#(A ∩ (a * b)⁻¹ •> A))
h₃ : 1 / 2 * ↑(#A) < ↑(#(A ∩ (c * d) •> A))
⊢ a * b * (c * d) ∈ A⁻¹ * A
Module: Mathlib.Combinatorics.Additive.VerySmallDoubling

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
K : ℝ
A✝ B S : Finset G
a b c d x y : G
A : Finset G
h : ↑(#(A * A)) < 3 / 2 * ↑(#A)
⊢ ∀ {a b : G}, a ∈ ↑A⁻¹ * ↑A → b ∈ ↑A⁻¹ * ↑A → a * b ∈ ↑A⁻¹ * ↑A

Tactic:
by
    norm_cast
    have h₁ x (hx : x ∈ A) y (hy : y ∈ A) : (1 / 2 : ℚ) * #A < #(x • A ∩ y • A) := by
      convert! lt_card_smul_inter_smul (by simpa using Rat.cast_strictMono (K := ℝ) h) hx hy
      norm_num
      simp [← Rat.cast_lt (K := ℝ)]
    intro a c ha hc
    simp only [mem_mul, mem_inv'] at ha hc
    obtain ⟨a, ha, b, hb, rfl⟩ := ha
    obtain ⟨c, hc, d, hd, rfl⟩ := hc
    have h₂ : (1 / 2 : ℚ) * #A < #(A ∩ (a * b)⁻¹ • A) := by
      refine (h₁ b hb _ ha).trans_le ?_
      rw [← card_smul_finset b⁻¹]
      simp [smul_smul, smul_finset_inter]
    have h₃ : (1 / 2 : ℚ) * #A < #(A ∩ (c * d) • A) := by
      refine (h₁ _ hc d hd).trans_le ?_
      rw [← card_smul_finset c]
      simp [smul_smul, smul_finset_inter]
    have ⟨t, ht⟩ : ((A ∩ (c * d) • A) ∩ (A ∩ (a * b)⁻¹ • A)).Nonempty := by
      rw [← card_pos, ← Nat.cast_pos (α := ℚ)]
      have := card_inter_add_card_union (A ∩ (c * d) • A) (A ∩ (a * b)⁻¹ • A)
      rw [← Nat.cast_inj (R := ℚ), Nat.cast_add, Nat.cast_add] at this
      have : (#((A ∩ (c * d) • A) ∪ (A ∩ (a * b)⁻¹ • A)) : ℚ) ≤ #A := by
        rw [Nat.cast_le, ← inter_union_distrib_left]
        exact card_le_card inter_subset_left
      linarith
    simp only [inter_inter_inter_comm, inter_self, mem_inter, ← inv_smul_mem_iff, inv_inv,
      smul_eq_mul, mul_assoc, mul_inv_rev] at ht
    rw [← mul_inv_eq_inv_mul_of_doubling_lt_two (weaken_doubling h), mem_mul]
    exact ⟨a * b * t, by simp [ht, mul_assoc], ((c * d)⁻¹ * t)⁻¹, by simp [ht, mul_assoc]⟩

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

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A : Finset G
a : G
ha : a ∈ A
⊢ A ⊆ a •> (A⁻¹ * A)

Tactic:
← smul_mul_assoc

Goal state after:
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A : Finset G
a : G
ha : a ∈ A
⊢ A ⊆ a •> A⁻¹ * A
Module: Mathlib.Combinatorics.Additive.VerySmallDoubling

Goal state before:
pp: case inr
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
K : ℝ
A : Finset G
hK₁ : 1 < K
hKφ : K < φ
hA₁ : ↑(#(A⁻¹ * A)) ≤ K * ↑(#A)
hA₂ : ↑(#(A * A⁻¹)) ≤ K * ↑(#A)
K_pos hK₀ : 0 < K
hKφ' : 0 < φ - K
hKψ' : 0 < K - ψ
hK₂' : 0 < 2 - K
const_pos : 0 < K * (2 - K) / ((φ - K) * (K - ψ))
A_nonempty : A.Nonempty
S : Finset G := A * A⁻¹
H : Subgroup G := stabilizer G S
⊢ ∃ H x Z, ↑(#Z) ≤ (2 - K) * K / ((φ - K) * (K - ψ)) ∧ ↑H * ↑Z = ↑A * ↑A⁻¹

Tactic:
have S_nonempty : S.Nonempty := by simpa [S]

Goal state after:
case inr
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
K : ℝ
A : Finset G
hK₁ : 1 < K
hKφ : K < φ
hA₁ : ↑(#(A⁻¹ * A)) ≤ K * ↑(#A)
hA₂ : ↑(#(A * A⁻¹)) ≤ K * ↑(#A)
K_pos hK₀ : 0 < K
hKφ' : 0 < φ - K
hKψ' : 0 < K - ψ
hK₂' : 0 < 2 - K
const_pos : 0 < K * (2 - K) / ((φ - K) * (K - ψ))
A_nonempty : A.Nonempty
S : Finset G := A * A⁻¹
H : Subgroup G := stabilizer G S
S_nonempty : S.Nonempty
⊢ ∃ H x Z, ↑(#Z) ≤ (2 - K) * K / ((φ - K) * (K - ψ)) ∧ ↑H * ↑Z = ↑A * ↑A⁻¹
Module: Mathlib.Combinatorics.Enumerative.Bell

Goal state before:
pp: n : ℕ
p : (n + 1).Partition
⊢ ∑ a ∈ p.parts.toFinset, a * (count a p.parts * p.parts.bell) =
    ∑ a ∈ p.parts.toFinset, (n + 1) * (n.choose (a - 1) * (p.parts.erase a).bell)

Tactic:
congr! 1 with a ha

Goal state after:
case a
n : ℕ
p : (n + 1).Partition
a : ℕ
ha : a ∈ p.parts.toFinset
⊢ a * (count a p.parts * p.parts.bell) = (n + 1) * (n.choose (a - 1) * (p.parts.erase a).bell)
Module: Mathlib.Combinatorics.Enumerative.Partition.Glaisher

Goal state before:
pp: R : Type u_1
inst✝⁴ : TopologicalSpace R
inst✝³ : T2Space R
inst✝² : CommRing R
inst✝¹ : NoZeroDivisors R
inst✝ : IsTopologicalRing R
m : ℕ
hm : 0 < m
⊢ (∏' (i : ℕ), if ¬m ∣ i + 1 then ∑' (j : ℕ), X ^ ((i + 1) * j) else 1) * ∏' (i : ℕ), (1 - X ^ (i + 1)) =
    ∏' (i : ℕ), (1 - X ^ ((i + 1) * m))

Tactic:
nontriviality R
  rw [← (multipliable_powerSeriesMk_card_restricted R (¬ m ∣ ·)).tprod_mul
    (multipliable_one_sub_X_pow _)]
  simp_rw [ite_not, ite_mul, pow_mul]
  conv in fun b ↦ _ =>
    ext b
    rw [tsum_pow_mul_one_sub_of_constantCoeff_eq_zero (by simp)]
  refine tprod_eq_tprod_of_ne_one_bij (fun i ↦ (i.val + 1) * m - 1) ?_ ?_ ?_
  · intro a b h
    rw [tsub_left_inj (by nlinarith) (by nlinarith), mul_left_inj' (hm.ne.symm), add_left_inj] at h
    exact SetCoe.ext h
  · suffices ∀ (i : ℕ), m ∣ i + 1 → ∃ j ≠ 0, j * m - 1 = i by simpa
    intro i hi
    obtain ⟨j, hj⟩ := dvd_def.mp hi
    refine ⟨j, by grind, Nat.sub_eq_of_eq_add ?_⟩
    rw [hj, mul_comm m j]
  · intro i
    have : (i + 1) * m - 1 + 1 = (i + 1) * m := by grind
    simp [this, pow_mul]

Goal state after:
Module: Mathlib.Combinatorics.Enumerative.Partition.Glaisher

Goal state before:
pp: n : ℕ
⊢ #(restricted n fun x ↦ ¬Even x) = #(countRestricted n 2)

Tactic:
even_iff_two_dvd

Goal state after:
n : ℕ
⊢ #(restricted n fun x ↦ ¬2 ∣ x) = #(countRestricted n 2)
Module: Mathlib.Combinatorics.Enumerative.Stirling

Goal state before:
pp: case zero
⊢ (0 + 1).stirlingSecond 0 = (0 + 1).choose 2

Tactic:
simp only [zero_add, stirlingSecond_succ_zero, choose_succ_self]

Goal state after:
Module: Mathlib.Combinatorics.Extremal.RuzsaSzemeredi

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : DecidableEq α
inst✝² : DecidableEq β
inst✝¹ : Fintype α
inst✝ : Fintype β
f : α ↪ β
G : SimpleGraph α
w✝ : DecidableRel G.Adj
hG : G.LocallyLinear
⊢ ∃ G_1 x, #(G_1.cliqueFinset 3) = #(G.cliqueFinset 3) ∧ G_1.LocallyLinear

Tactic:
refine ⟨G.map f, inferInstance, ?_, hG.map _⟩

Goal state after:
α : Type u_1
β : Type u_2
inst✝³ : DecidableEq α
inst✝² : DecidableEq β
inst✝¹ : Fintype α
inst✝ : Fintype β
f : α ↪ β
G : SimpleGraph α
w✝ : DecidableRel G.Adj
hG : G.LocallyLinear
⊢ #((SimpleGraph.map (⇑f) G).cliqueFinset 3) = #(G.cliqueFinset 3)
Module: Mathlib.Combinatorics.Extremal.RuzsaSzemeredi

Goal state before:
pp: n : ℕ
⊢ (↑(n + 3) / 3 - 2) * ↑(rothNumberNat ((n + 3 - 3) / 6)) ≤ ↑(ruzsaSzemerediNumberNat (n + 3))

Tactic:
by
    calc
      _ ≤ (↑(2 * (n / 6) + 1) : ℝ) * rothNumberNat (n / 6) :=
        mul_le_mul_of_nonneg_right ?_ (Nat.cast_nonneg _)
      _ ≤ (ruzsaSzemerediNumberNat (6 * (n / 6) + 3) : ℝ) := ?_
      _ ≤ _ := by grw [Nat.mul_div_le]
    · simp only [cast_add, cast_ofNat, cast_mul, cast_one, tsub_le_iff_right]
      rw [← div_add_one (three_ne_zero' ℝ), ← le_sub_iff_add_le, div_le_iff₀ (zero_lt_three' ℝ),
        add_assoc, add_sub_assoc, add_mul, mul_right_comm, add_sub_cancel_left]
      norm_cast
      rw [← mul_add_one]
      exact (Nat.lt_mul_div_succ _ <| by simp).le
    · norm_cast
      exact rothNumberNat_le_ruzsaSzemerediNumberNat _

Goal state after:
Module: Mathlib.Combinatorics.Graph.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
x y : α
e : β
G : Graph α β
h : G.IsLink e x y
x' y' : α
⊢ G.IsLink e x' y' ↔ x = x' ∧ y = y' ∨ x = y' ∧ y = x'

Tactic:
refine ⟨h.eq_and_eq_or_eq_and_eq, ?_⟩
  rintro (⟨rfl, rfl⟩ | ⟨rfl, rfl⟩)
  · assumption
  exact h.symm

Goal state after:
Module: Mathlib.Combinatorics.Graph.Delete

Goal state before:
pp: α : Type u_1
β : Type u_2
x✝ y✝ : α
e✝ : β
G✝ H : Graph α β
F✝ F₀ : Set β
X : Set α
G : Graph α β
F : Set β
e : β
x y : α
⊢ (G.restrict (E(G) \ F)).IsLink e x y ↔ G.IsLink e x y ∧ e ∉ F

Tactic:
by
    simp only [restrict_isLink, mem_sdiff, and_comm, and_congr_left_iff, and_iff_left_iff_imp]
    exact fun h _ ↦ h.edge_mem

Goal state after:
Module: Mathlib.Combinatorics.Graph.Lattice

Goal state before:
pp: α : Type u_1
β : Type u_2
x y : α
e✝ : β
G✝ H✝ G H : Graph α β
e : β
⊢ e ∈ {e | e ∈ E(G) ∩ E(H) ∧ ∀ (x y : α), G.IsLink e x y ↔ H.IsLink e x y} ↔ ∃ x y, G.IsLink e x y ∧ H.IsLink e x y

Tactic:
by
      simp only [edgeSet_eq_setOfPred_exists_isLink, mem_inter_iff, mem_ofPred_eq]
      exact ⟨fun ⟨⟨⟨x, y, hexy⟩, ⟨z, w, hezw⟩⟩, h⟩ ↦ ⟨x, y, hexy, by rwa [← h]⟩,
        fun ⟨x, y, hfG, hfH⟩ ↦ ⟨⟨⟨_, _, hfG⟩, ⟨_, _, hfH⟩⟩,
        fun z w ↦ by rw [hfG.isLink_iff_sym2_eq, hfH.isLink_iff_sym2_eq]⟩⟩

Goal state after:
Module: Mathlib.Combinatorics.Graph.Simple

Goal state before:
pp: α : Type u_1
β : Type u_2
G✝ H : Graph α β
u v : α
e f : β
X Y : Set α
G : SimpleGraph α
⊢ (ofSimpleGraph G).toSimpleGraph ≃g G

Tactic:
by
  use Equiv.Set.univ α
  refine ⟨fun h ↦ ⟨fun h' ↦ h.ne (congrArg Subtype.val h'), ?_⟩, fun ⟨_, h⟩ ↦ ?_⟩ <;>
    revert h <;> rw [ofSimpleGraph_adj_iff] <;> exact id

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Minor.Delete

Goal state before:
pp: α : Type u_1
M : Matroid α
e : α
D : Set α
⊢ (M ＼ D).IsLoop e ↔ M.IsLoop e ∧ e ∉ D

Tactic:
by
  rw [← singleton_dep, delete_dep_iff, disjoint_singleton_left, singleton_dep]

Goal state after:
Module: Mathlib.Combinatorics.Hindman

Goal state before:
pp: case succ
M : Type u_1
inst✝ : Semigroup M
a : Stream' M
n : ℕ
ih : FP (Stream'.drop n a) ⊆ FP a
⊢ FP (Stream'.drop (n + 1) a) ⊆ FP a

Tactic:
← Stream'.drop_drop

Goal state after:
case succ
M : Type u_1
inst✝ : Semigroup M
a : Stream' M
n : ℕ
ih : FP (Stream'.drop n a) ⊆ FP a
⊢ FP (Stream'.drop 1 (Stream'.drop n a)) ⊆ FP a
Module: Mathlib.Combinatorics.Matroid.Minor.Contract

Goal state before:
pp: α : Type u_1
M : Matroid α
⊢ M ／ ∅ = M

Tactic:
rw [← dual_delete_dual, delete_empty, dual_dual]

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Minor.Contract

Goal state before:
pp: α : Type u_1
M : Matroid α
I J : Set α
hI : M.Indep I
x✝ : Disjoint J I ∧ ∃ B, M.IsBase B ∧ J ⊆ B ∧ I ⊆ B
hdj : Disjoint J I
B : Set α
hB : M.IsBase B
hJB : J ⊆ B
hIB : I ⊆ B
⊢ M.IsBase (B \ I ∪ I)

Tactic:
simpa [union_eq_self_of_subset_right hIB]

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Sum

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
M✝ M : (i : ι) → Matroid (α i)
B : Set ((i : ι) × α i)
hB : ∀ (i : ι), (M i).IsBase (Sigma.mk i ⁻¹' B)
⊢ B ⊆ univ.sigma fun i ↦ (M i).E

Tactic:
← univ_sigma_preimage_mk B

Goal state after:
ι : Type u_1
α : ι → Type u_2
M✝ M : (i : ι) → Matroid (α i)
B : Set ((i : ι) × α i)
hB : ∀ (i : ι), (M i).IsBase (Sigma.mk i ⁻¹' B)
⊢ (univ.sigma fun i ↦ Sigma.mk i ⁻¹' B) ⊆ univ.sigma fun i ↦ (M i).E
Module: Mathlib.Combinatorics.Nullstellensatz

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
σ✝ : Type u_2
inst✝² : Finite σ✝
inst✝¹ : IsDomain R
σ : Type u_2
inst✝ : Fintype σ
h :
  ∀ (P : MvPolynomial σ R) (S : σ → Finset R),
    (∀ (i : σ), degreeOf i P < #(S i)) → (∀ (x : σ → R), (∀ (i : σ), x i ∈ S i) → (eval x) P = 0) → P = 0
P : MvPolynomial (Option σ) R
S : Option σ → Finset R
Hdeg : ∀ (i : Option σ), degreeOf i P < #(S i)
Heval : ∀ (x : Option σ → R), (∀ (i : Option σ), x i ∈ S i) → (eval x) P = 0
Q : Polynomial (MvPolynomial σ R) := (optionEquivLeft R σ) P
hQ : Q = (optionEquivLeft R σ) P
x : σ → R
hx : ∀ (i : σ), x i ∈ S (Option.some i)
d : ℕ
hd : degreeOf none P < d
⊢ (Polynomial.map (eval x) Q).coeff d = 0

Tactic:
simp only [hQ]

Goal state after:
R : Type u_1
inst✝³ : CommRing R
σ✝ : Type u_2
inst✝² : Finite σ✝
inst✝¹ : IsDomain R
σ : Type u_2
inst✝ : Fintype σ
h :
  ∀ (P : MvPolynomial σ R) (S : σ → Finset R),
    (∀ (i : σ), degreeOf i P < #(S i)) → (∀ (x : σ → R), (∀ (i : σ), x i ∈ S i) → (eval x) P = 0) → P = 0
P : MvPolynomial (Option σ) R
S : Option σ → Finset R
Hdeg : ∀ (i : Option σ), degreeOf i P < #(S i)
Heval : ∀ (x : Option σ → R), (∀ (i : Option σ), x i ∈ S i) → (eval x) P = 0
Q : Polynomial (MvPolynomial σ R) := (optionEquivLeft R σ) P
hQ : Q = (optionEquivLeft R σ) P
x : σ → R
hx : ∀ (i : σ), x i ∈ S (Option.some i)
d : ℕ
hd : degreeOf none P < d
⊢ (Polynomial.map (eval x) ((optionEquivLeft R σ) P)).coeff d = 0
Module: Mathlib.Combinatorics.Quiver.Covering

Goal state before:
pp: case inl
U : Type u_1
inst✝¹ : Quiver U
V : Type u_2
inst✝ : Quiver V
φ : U ⥤q V
u : U
v : Symmetrify U
f : u ⟶ v
⊢ (⇑(Quiver.symmetrifyStar (φ.obj u)) ∘ φ.symmetrify.star u) ⟨v, Sum.inl f⟩ =
    (Sum.map (φ.star u) (φ.costar u) ∘ ⇑(Quiver.symmetrifyStar u)) ⟨v, Sum.inl f⟩

Tactic:
simp only [Quiver.symmetrifyStar, Function.comp_apply]

Goal state after:
case inl
U : Type u_1
inst✝¹ : Quiver U
V : Type u_2
inst✝ : Quiver V
φ : U ⥤q V
u : U
v : Symmetrify U
f : u ⟶ v
⊢ (Equiv.sigmaSumDistrib (Hom (Symmetrify.of.obj (φ.obj u))) fun v ↦ v ⟶ Symmetrify.of.obj (φ.obj u))
      (φ.symmetrify.star u ⟨v, Sum.inl f⟩) =
    Sum.map (φ.star u) (φ.costar u)
      ((Equiv.sigmaSumDistrib (Hom (Symmetrify.of.obj u)) fun v ↦ v ⟶ Symmetrify.of.obj u) ⟨v, Sum.inl f⟩)
Module: Mathlib.Combinatorics.Quiver.Covering

Goal state before:
pp: case inr
U : Type u_1
inst✝¹ : Quiver U
V : Type u_2
inst✝ : Quiver V
φ : U ⥤q V
u : U
v : Symmetrify U
g : v ⟶ u
⊢ (⇑(Quiver.symmetrifyStar (φ.obj u)) ∘ φ.symmetrify.star u) ⟨v, Sum.inr g⟩ =
    (Sum.map (φ.star u) (φ.costar u) ∘ ⇑(Quiver.symmetrifyStar u)) ⟨v, Sum.inr g⟩

Tactic:
simp only [Quiver.symmetrifyStar, Function.comp_apply]

Goal state after:
case inr
U : Type u_1
inst✝¹ : Quiver U
V : Type u_2
inst✝ : Quiver V
φ : U ⥤q V
u : U
v : Symmetrify U
g : v ⟶ u
⊢ (Equiv.sigmaSumDistrib (Hom (Symmetrify.of.obj (φ.obj u))) fun v ↦ v ⟶ Symmetrify.of.obj (φ.obj u))
      (φ.symmetrify.star u ⟨v, Sum.inr g⟩) =
    Sum.map (φ.star u) (φ.costar u)
      ((Equiv.sigmaSumDistrib (Hom (Symmetrify.of.obj u)) fun v ↦ v ⟶ Symmetrify.of.obj u) ⟨v, Sum.inr g⟩)