mathlib-initiative/mathlib-tactics huggingface dataset:
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 α
x y z : α
⊢ ∀ x_1 ∈ s,
    ¬(x_1 ∈ G.badVertices ε s t ∨ x_1 ∈ G.badVertices ε s u) →
      ∀ (x_2 x_3 : α),
        x_2 ∈ t →
          G.Adj x_1 x_2 →
            x_3 ∈ u →
              G.Adj x_1 x_3 →
                G.Adj x_2 x_3 → x_1 = x → x_2 = y → x_3 = z → x ∈ s ∧ y ∈ t ∧ z ∈ u ∧ G.Adj x y ∧ G.Adj x z ∧ G.Adj y z

Tactic:
rintro x hx - y z hy xy hz xz yz rfl rfl rfl

Goal state after:
α : Type u_1
G : SimpleGraph α
inst✝¹ : DecidableRel G.Adj
ε : ℝ
s t u : Finset α
inst✝ : DecidableEq α
x : α
hx : x ∈ s
y z : α
hy : y ∈ t
xy : G.Adj x y
hz : z ∈ u
xz : G.Adj x z
yz : G.Adj y z
⊢ x ∈ s ∧ y ∈ t ∧ z ∈ u ∧ G.Adj x y ∧ G.Adj x z ∧ G.Adj y z
Module: Mathlib.Combinatorics.Additive.Corner.Roth

Goal state before:
pp: G : Type u_1
inst✝¹ : AddCommGroup G
inst✝ : Fintype G
ε : ℝ
hε : 0 < ε
hG : cornersTheoremBound ε ≤ Fintype.card G
A : Finset G
hAε : ε * ↑(Fintype.card G) ≤ ↑(#A)
hA : ThreeAPFree ↑A
B : Finset (G × G) :=
  {x |
    match x with
    | (x, y) => y - x ∈ A}
this : ε * ↑(Fintype.card G) ^ 2 ≤ ↑(#B)
x₁ y₁ x₂ y₂ : G
hx₁y₁ : y₁ - x₁ ∈ A
hx₁y₂ : y₂ - x₁ ∈ A
hx₂y₁ : y₁ - x₂ ∈ A
hxy : x₁ + y₂ = x₂ + y₁
hx₁x₂ : x₁ ≠ x₂
⊢ False

Tactic:
have := hA hx₂y₁ hx₁y₁ hx₁y₂ <| by -- TODO: This really ought to just be `by linear_combination h`
    rw [sub_add_sub_comm, add_comm, add_sub_add_comm, add_right_cancel_iff,
      sub_eq_sub_iff_add_eq_add, add_comm, hxy, add_comm]

Goal state after:
G : Type u_1
inst✝¹ : AddCommGroup G
inst✝ : Fintype G
ε : ℝ
hε : 0 < ε
hG : cornersTheoremBound ε ≤ Fintype.card G
A : Finset G
hAε : ε * ↑(Fintype.card G) ≤ ↑(#A)
hA : ThreeAPFree ↑A
B : Finset (G × G) :=
  {x |
    match x with
    | (x, y) => y - x ∈ A}
this✝ : ε * ↑(Fintype.card G) ^ 2 ≤ ↑(#B)
x₁ y₁ x₂ y₂ : G
hx₁y₁ : y₁ - x₁ ∈ A
hx₁y₂ : y₂ - x₁ ∈ A
hx₂y₁ : y₁ - x₂ ∈ A
hxy : x₁ + y₂ = x₂ + y₁
hx₁x₂ : x₁ ≠ x₂
this : y₁ - x₂ = y₁ - x₁
⊢ False
Module: Mathlib.FieldTheory.ChevalleyWarning

Goal state before:
pp: K : Type u_1
σ : Type u_2
inst✝⁵ : Fintype K
inst✝⁴ : Field K
inst✝³ : Fintype σ
inst✝² : DecidableEq σ
inst✝¹ : DecidableEq K
p : ℕ
inst✝ : CharP K p
f : MvPolynomial σ K
h : f.totalDegree < Fintype.card σ
F : Unit → MvPolynomial σ K := fun x ↦ f
this : ∑ i, (F i).totalDegree < Fintype.card σ
⊢ p ∣ Fintype.card { x // (eval x) f = 0 }

Tactic:
convert! char_dvd_card_solutions_of_sum_lt p this

Goal state after:
K : Type u_1
σ : Type u_2
inst✝⁵ : Fintype K
inst✝⁴ : Field K
inst✝³ : Fintype σ
inst✝² : DecidableEq σ
inst✝¹ : DecidableEq K
p : ℕ
inst✝ : CharP K p
f : MvPolynomial σ K
h : f.totalDegree < Fintype.card σ
F : Unit → MvPolynomial σ K := ⋯
this : ∑ i, (F i).totalDegree < Fintype.card σ
x✝ : σ → K
⊢ (eval x✝) f = 0 ↔ ∀ i ∈ univ, (eval x✝) (F i) = 0
Module: Mathlib.Data.Nat.BitIndices

Goal state before:
pp: b : Bool
n : ℕ
hs : n.bitIndices.SortedLT
this : List.Pairwise (fun a b ↦ a < b) n.bitIndices
⊢ (bit b n).bitIndices.SortedLT

Tactic:
cases b

Goal state after:
case false
n : ℕ
hs : n.bitIndices.SortedLT
this : List.Pairwise (fun a b ↦ a < b) n.bitIndices
⊢ (bit false n).bitIndices.SortedLT

case true
n : ℕ
hs : n.bitIndices.SortedLT
this : List.Pairwise (fun a b ↦ a < b) n.bitIndices
⊢ (bit true n).bitIndices.SortedLT
Module: Mathlib.Data.Nat.BitIndices

Goal state before:
pp: case succ
n k : ℕ
ih : (2 ^ k * n).bitIndices = map (fun x ↦ x + k) n.bitIndices
⊢ map (fun x ↦ x + 1) (2 ^ k * n).bitIndices = map (fun x ↦ x + (1 + k)) n.bitIndices

Tactic:
ih,

Goal state after:
case succ
n k : ℕ
ih : (2 ^ k * n).bitIndices = map (fun x ↦ x + k) n.bitIndices
⊢ map (fun x ↦ x + 1) (map (fun x ↦ x + k) n.bitIndices) = map (fun x ↦ x + (1 + k)) n.bitIndices
Module: Mathlib.Data.Nat.BitIndices

Goal state before:
pp: case bit
b : Bool
n : ℕ
hs : (map (fun i ↦ 2 ^ i) n.bitIndices).sum = n
hrw : ((fun i ↦ 2 ^ i) ∘ fun x ↦ x + 1) = fun i ↦ 2 * 2 ^ i
⊢ (map (fun i ↦ 2 ^ i) (bit b n).bitIndices).sum = bit b n

Tactic:
cases b

Goal state after:
case bit.false
n : ℕ
hs : (map (fun i ↦ 2 ^ i) n.bitIndices).sum = n
hrw : ((fun i ↦ 2 ^ i) ∘ fun x ↦ x + 1) = fun i ↦ 2 * 2 ^ i
⊢ (map (fun i ↦ 2 ^ i) (bit false n).bitIndices).sum = bit false n

case bit.true
n : ℕ
hs : (map (fun i ↦ 2 ^ i) n.bitIndices).sum = n
hrw : ((fun i ↦ 2 ^ i) ∘ fun x ↦ x + 1) = fun i ↦ 2 * 2 ^ i
⊢ (map (fun i ↦ 2 ^ i) (bit true n).bitIndices).sum = bit true n
Module: Mathlib.Data.Nat.BitIndices

Goal state before:
pp: case bit
b : Bool
n : ℕ
ih : ∀ {i : ℕ}, i ∈ n.bitIndices ↔ n.testBit i = true
i : ℕ
⊢ i ∈ (bit b n).bitIndices ↔ (bit b n).testBit i = true

Tactic:
cases b

Goal state after:
case bit.false
n : ℕ
ih : ∀ {i : ℕ}, i ∈ n.bitIndices ↔ n.testBit i = true
i : ℕ
⊢ i ∈ (bit false n).bitIndices ↔ (bit false n).testBit i = true

case bit.true
n : ℕ
ih : ∀ {i : ℕ}, i ∈ n.bitIndices ↔ n.testBit i = true
i : ℕ
⊢ i ∈ (bit true n).bitIndices ↔ (bit true n).testBit i = true
Module: Mathlib.Combinatorics.Colex

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
s t : Finset α
⊢ (∃ x, ¬(x ∈ t → x ∉ s → ∃ b ∈ s, b ∉ t ∧ x ≤ b)) ↔ ∃ a ∈ t, a ∉ s ∧ ∀ b ∈ s, b ∉ t → b < a

Tactic:
simp only [not_forall, not_exists, not_and, not_le, exists_prop]

Goal state after:
Module: Mathlib.Combinatorics.Colex

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
𝒜₁ 𝒜₂ : Finset (Finset α)
r : ℕ
h₁ : IsInitSeg 𝒜₁ r
h₂ : IsInitSeg 𝒜₂ r
h : (𝒜₁ \ 𝒜₂).Nonempty ∧ (𝒜₂ \ 𝒜₁).Nonempty
s : Finset α
hs : s ∈ 𝒜₁ \ 𝒜₂
t : Finset α
ht : t ∈ 𝒜₂ \ 𝒜₁
⊢ False

Tactic:
mem_sdiff

Goal state after:
α : Type u_1
inst✝ : LinearOrder α
𝒜₁ 𝒜₂ : Finset (Finset α)
r : ℕ
h₁ : IsInitSeg 𝒜₁ r
h₂ : IsInitSeg 𝒜₂ r
h : (𝒜₁ \ 𝒜₂).Nonempty ∧ (𝒜₂ \ 𝒜₁).Nonempty
s : Finset α
hs : s ∈ 𝒜₁ ∧ s ∉ 𝒜₂
t : Finset α
ht : t ∈ 𝒜₂ ∧ t ∉ 𝒜₁
⊢ False
Module: Mathlib.Combinatorics.Derangements.Basic

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
a : α
⊢ { f // a ∉ fixedPoints ⇑↑f } ≃ { f // fixedPoints ⇑f ⊆ {a} ∧ a ∉ fixedPoints ⇑f }

Tactic:
· exact subtypeSubtypeEquivSubtypeInter
          (fun x : Perm α => fixedPoints x ⊆ {a})
          (a ∉ fixedPoints ·)

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

Goal state before:
pp: n : ℕ
⊢ ↑(numDerangements (n + 1)) = (↑n + 1) * ↑(numDerangements n) - (-1) ^ n

Tactic:
induction n with
  | zero => rfl
  | succ n hn =>
    simp only [numDerangements_add_two, hn, pow_succ, Int.natCast_mul, Int.natCast_add]
    ring

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

Goal state before:
pp: case pos
α : Type u_1
inst✝ : DecidableEq α
a : α
f : Perm α
h_opfp : f ∈ {f | fixedPoints ⇑f ⊆ {a}}
x : α
x_vs_a : x = a
⊢ some (f a) ≠ (Equiv.swap none (some a)) (some a)

Tactic:
swap_apply_right

Goal state after:
case pos
α : Type u_1
inst✝ : DecidableEq α
a : α
f : Perm α
h_opfp : f ∈ {f | fixedPoints ⇑f ⊆ {a}}
x : α
x_vs_a : x = a
⊢ some (f a) ≠ none
Module: Mathlib.Combinatorics.Additive.VerySmallDoubling

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
c : Set G
x : G
hc : c ∈ orbit Gᵐᵒᵖ ↑H
⊢ x ∈ c ↔ ↑H <• x = c

Tactic:
by
  refine ⟨fun hx => ?_, fun hx =>
    by simp only [← hx, mem_rightCoset_iff, mul_inv_cancel, SetLike.mem_coe, one_mem]⟩
  obtain ⟨⟨a⟩, rfl⟩ := hc
  change _ = _ <• _
  rw [eq_comm, smul_eq_iff_eq_inv_smul, ← op_inv, op_smul_op_smul, rightCoset_mem_rightCoset]
  rwa [← op_smul_eq_mul, op_inv, ← SetLike.mem_coe, ← Set.mem_smul_set_iff_inv_smul_mem]

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

Goal state before:
pp: 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
this✝ : Finite ↥H
val✝ : Fintype ↥H
H_mul_S : ↑H * ↑S = ↑S
Z : Finset G
hZ : Z ⊆ S ∧ ↑H * ↑Z = ↑H * ↑S ∧ Set.InjOn (fun x ↦ ↑H <• x) ↑Z
H_mul_Z : ↑H * ↑Z = ↑S
H_toFinset_mul_Z : (↑H).toFinset * Z = S
card_H_mul_card_Z : Fintype.card ↥H * #Z = #S
this : (φ - K) * (K - ψ) / ((2 - K) * K) * ↑(#S) ≤ ↑(Fintype.card ↥H)
⊢ ((φ - K) * (K - ψ) / ((2 - K) * K) * ↑(#S) / ↑(#S))⁻¹ = (2 - K) * K / ((φ - K) * (K - ψ))

Tactic:
have : (#S : ℝ) ≠ 0 := by positivity

Goal state after:
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
this✝¹ : Finite ↥H
val✝ : Fintype ↥H
H_mul_S : ↑H * ↑S = ↑S
Z : Finset G
hZ : Z ⊆ S ∧ ↑H * ↑Z = ↑H * ↑S ∧ Set.InjOn (fun x ↦ ↑H <• x) ↑Z
H_mul_Z : ↑H * ↑Z = ↑S
H_toFinset_mul_Z : (↑H).toFinset * Z = S
card_H_mul_card_Z : Fintype.card ↥H * #Z = #S
this✝ : (φ - K) * (K - ψ) / ((2 - K) * K) * ↑(#S) ≤ ↑(Fintype.card ↥H)
this : ↑(#S) ≠ 0
⊢ ((φ - K) * (K - ψ) / ((2 - K) * K) * ↑(#S) / ↑(#S))⁻¹ = (2 - K) * K / ((φ - K) * (K - ψ))
Module: Mathlib.Combinatorics.Enumerative.DyckWord

Goal state before:
pp: p : DyckWord
⊢ p.semilength = count D ↑p

Tactic:
rw [← count_U_eq_count_D]; rfl

Goal state after:
Module: Mathlib.Combinatorics.Enumerative.IncidenceAlgebra

Goal state before:
pp: case neg
𝕜 : Type u_2
α : Type u_5
inst✝⁴ : AddCommGroup 𝕜
inst✝³ : One 𝕜
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b : α
hab✝ : ¬a = b
hab : ¬a ≤ b
⊢ ∑ x ∈ Icc a b, (mu' 𝕜) x b = 0

Tactic:
· exact sum_eq_zero fun x hx ↦ apply_eq_zero_of_not_le
      (fun hxb ↦ hab <| (mem_Icc.1 hx).1.trans hxb) _

Goal state after:
Module: Mathlib.Combinatorics.Enumerative.DyckWord

Goal state before:
pp: p q : DyckWord
h : p ≠ 0
⊢ (if h : p + q = 0 then 0 else ((p + q).take ((if p = 0 then q.firstReturn else p.firstReturn) + 1) ⋯).denest ⋯) =
    if h : p = 0 then 0 else (p.take (p.firstReturn + 1) ⋯).denest ⋯

Tactic:
add_eq_zero',

Goal state after:
p q : DyckWord
h : p ≠ 0
⊢ (if h : p = 0 ∧ q = 0 then 0 else ((p + q).take ((if p = 0 then q.firstReturn else p.firstReturn) + 1) ⋯).denest ⋯) =
    if h : p = 0 then 0 else (p.take (p.firstReturn + 1) ⋯).denest ⋯
Module: Mathlib.Combinatorics.Enumerative.DyckWord

Goal state before:
pp: p q : DyckWord
h : p ≠ 0
⊢ (if h : p + q = 0 then 0 else (p + q).drop ((if p = 0 then q.firstReturn else p.firstReturn) + 1) ⋯) =
    (if h : p = 0 then 0 else p.drop (p.firstReturn + 1) ⋯) + q

Tactic:
add_eq_zero',

Goal state after:
p q : DyckWord
h : p ≠ 0
⊢ (if h : p = 0 ∧ q = 0 then 0 else (p + q).drop ((if p = 0 then q.firstReturn else p.firstReturn) + 1) ⋯) =
    (if h : p = 0 then 0 else p.drop (p.firstReturn + 1) ⋯) + q
Module: Mathlib.Combinatorics.Enumerative.Partition.GenFun

Goal state before:
pp: case refine_2
R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : TopologicalSpace R
inst✝ : T2Space R
f : ℕ → ℕ → R
d : ℕ
s : Finset ℕ
hs0 : 0 ∉ s
g : ℕ →₀ ℕ
hg : g ∈ s.finsuppAntidiag d
hprod : ∀ i ∈ s, (coeff (g i)) (1 + ∑' (j : ℕ), f i (j + 1) • X ^ (i * (j + 1))) ≠ 0
hgne0 : ∀ (i : ℕ), g i ≠ 0 ↔ i ≠ 0 ∧ i ≤ g i
⊢ ∀ {i : ℕ}, i ∈ Finsupp.toMultiset { support := g.support, toFun := fun i ↦ g i / i, mem_support_toFun := ⋯ } → 0 < i

Tactic:
suffices ∀ i, g i ≠ 0 → i ≠ 0 by simpa [Nat.pos_iff_ne_zero]

Goal state after:
case refine_2
R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : TopologicalSpace R
inst✝ : T2Space R
f : ℕ → ℕ → R
d : ℕ
s : Finset ℕ
hs0 : 0 ∉ s
g : ℕ →₀ ℕ
hg : g ∈ s.finsuppAntidiag d
hprod : ∀ i ∈ s, (coeff (g i)) (1 + ∑' (j : ℕ), f i (j + 1) • X ^ (i * (j + 1))) ≠ 0
hgne0 : ∀ (i : ℕ), g i ≠ 0 ↔ i ≠ 0 ∧ i ≤ g i
⊢ ∀ (i : ℕ), g i ≠ 0 → i ≠ 0
Module: Mathlib.Combinatorics.Enumerative.Pentagonal.Ring

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
inst✝² : TopologicalSpace R
inst✝¹ : IsTopologicalRing R
inst✝ : T2Space R
k : ℕ
x : R
hx : IsTopologicallyNilpotent x
hsum : ∀ (k : ℕ), Summable fun x_1 ↦ powMulProdOneSubPow k x_1 x
h : ∀ (k : ℕ), Multipliable fun n ↦ 1 - x ^ (n + k + 1)
⊢ 1 - x ^ (2 * k + 3) = 0 - aux k 0 x

Tactic:
simp [aux]

Goal state after:
Module: Mathlib.Combinatorics.Enumerative.Pentagonal.Ring

Goal state before:
pp: case succ
R : Type u_1
inst✝³ : CommRing R
inst✝² : TopologicalSpace R
inst✝¹ : IsTopologicalRing R
inst✝ : T2Space R
x : R
hx : IsTopologicallyNilpotent x
hsum : ∀ (k : ℕ), Summable fun x_1 ↦ powMulProdOneSubPow k x_1 x
h : ∀ (k : ℕ), Multipliable fun n ↦ 1 - x ^ (n + k + 1)
n : ℕ
ih :
  ∏' (n : ℕ), (1 - x ^ (n + 1)) =
    ∑ k ∈ Finset.range (n + 1), (-1) ^ k * (x ^ (k * (3 * k + 1) / 2) - x ^ ((k + 1) * (3 * k + 2) / 2)) +
      (-1) ^ (n + 1) * x ^ ((n + 1) * (3 * n + 4) / 2) * ∑' (n_1 : ℕ), powMulProdOneSubPow n n_1 x
⊢ ∏' (n : ℕ), (1 - x ^ (n + 1)) =
    ∑ k ∈ Finset.range (n + 1 + 1), (-1) ^ k * (x ^ (k * (3 * k + 1) / 2) - x ^ ((k + 1) * (3 * k + 2) / 2)) +
      (-1) ^ (n + 1 + 1) * x ^ ((n + 1 + 1) * (3 * (n + 1) + 4) / 2) * ∑' (n_1 : ℕ), powMulProdOneSubPow (n + 1) n_1 x

Tactic:
ih,

Goal state after:
case succ
R : Type u_1
inst✝³ : CommRing R
inst✝² : TopologicalSpace R
inst✝¹ : IsTopologicalRing R
inst✝ : T2Space R
x : R
hx : IsTopologicallyNilpotent x
hsum : ∀ (k : ℕ), Summable fun x_1 ↦ powMulProdOneSubPow k x_1 x
h : ∀ (k : ℕ), Multipliable fun n ↦ 1 - x ^ (n + k + 1)
n : ℕ
ih :
  ∏' (n : ℕ), (1 - x ^ (n + 1)) =
    ∑ k ∈ Finset.range (n + 1), (-1) ^ k * (x ^ (k * (3 * k + 1) / 2) - x ^ ((k + 1) * (3 * k + 2) / 2)) +
      (-1) ^ (n + 1) * x ^ ((n + 1) * (3 * n + 4) / 2) * ∑' (n_1 : ℕ), powMulProdOneSubPow n n_1 x
⊢ ∑ k ∈ Finset.range (n + 1), (-1) ^ k * (x ^ (k * (3 * k + 1) / 2) - x ^ ((k + 1) * (3 * k + 2) / 2)) +
      (-1) ^ (n + 1) * x ^ ((n + 1) * (3 * n + 4) / 2) * ∑' (n_1 : ℕ), powMulProdOneSubPow n n_1 x =
    ∑ k ∈ Finset.range (n + 1 + 1), (-1) ^ k * (x ^ (k * (3 * k + 1) / 2) - x ^ ((k + 1) * (3 * k + 2) / 2)) +
      (-1) ^ (n + 1 + 1) * x ^ ((n + 1 + 1) * (3 * (n + 1) + 4) / 2) * ∑' (n_1 : ℕ), powMulProdOneSubPow (n + 1) n_1 x
Module: Mathlib.Combinatorics.Enumerative.Stirling

Goal state before:
pp: case succ
n : ℕ
ih : (n + 1).stirlingFirst n = (n + 1).choose 2
⊢ (n + 1) * (n + 1).stirlingFirst (n + 1) + (n + 1).stirlingFirst n = (n + 1 + 1).choose 2

Tactic:
ih,

Goal state after:
case succ
n : ℕ
ih : (n + 1).stirlingFirst n = (n + 1).choose 2
⊢ (n + 1) * (n + 1).stirlingFirst (n + 1) + (n + 1).choose 2 = (n + 1 + 1).choose 2
Module: Mathlib.Combinatorics.Enumerative.Stirling

Goal state before:
pp: case succ
n : ℕ
ih : (n + 1).stirlingSecond n = (n + 1).choose 2
⊢ (n + 1) * (n + 1).stirlingSecond (n + 1) + (n + 1).stirlingSecond n = (n + 1 + 1).choose 2

Tactic:
ih,

Goal state after:
case succ
n : ℕ
ih : (n + 1).stirlingSecond n = (n + 1).choose 2
⊢ (n + 1) * (n + 1).stirlingSecond (n + 1) + (n + 1).choose 2 = (n + 1 + 1).choose 2
Module: Mathlib.Combinatorics.Additive.VerySmallDoubling

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
S : Finset G
ε : ℝ
hε₀ : 0 < ε
hε₁ : ε ≤ 1
hS : S.Nonempty
hA : ∃ A, #S ≤ #A ∧ ↑(#(A * S)) ≤ (2 - ε) * ↑(#S)
⊢ ∃ H x Z, ↑(Fintype.card ↥H) ≤ (2 / ε - 1) * ↑(#S) ∧ ↑(#Z) ≤ 2 / ε - 1 ∧ ↑S ⊆ ↑H * ↑Z

Tactic:
let K := 1 - ε / 2

Goal state after:
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
S : Finset G
ε : ℝ
hε₀ : 0 < ε
hε₁ : ε ≤ 1
hS : S.Nonempty
hA : ∃ A, #S ≤ #A ∧ ↑(#(A * S)) ≤ (2 - ε) * ↑(#S)
K : ℝ := 1 - ε / 2
⊢ ∃ H x Z, ↑(Fintype.card ↥H) ≤ (2 / ε - 1) * ↑(#S) ∧ ↑(#Z) ≤ 2 / ε - 1 ∧ ↑S ⊆ ↑H * ↑Z
Module: Mathlib.Combinatorics.Extremal.RuzsaSzemeredi

Goal state before:
pp: α : Type u_1
inst✝¹ : Fintype α
inst✝ : CommRing α
s : Finset α
hs : ThreeAPFree ↑s
d a : α
ha : a ∈ s
b : α
hb : b ∈ s
d' c : α
hc : c ∈ s
h₁ : d' + 2 * b = d + 2 * a
h₂ : d' + c = d + a
⊢ d' = d ∨ d + a = d' + b ∨ d + 2 * a = d' + 2 * c

Tactic:
have : a + c = b + b := by linear_combination h₁.symm - h₂.symm

Goal state after:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : CommRing α
s : Finset α
hs : ThreeAPFree ↑s
d a : α
ha : a ∈ s
b : α
hb : b ∈ s
d' c : α
hc : c ∈ s
h₁ : d' + 2 * b = d + 2 * a
h₂ : d' + c = d + a
this : a + c = b + b
⊢ d' = d ∨ d + a = d' + b ∨ d + 2 * a = d' + 2 * c
Module: Mathlib.Combinatorics.Graph.Maps

Goal state before:
pp: α : Type u_1
α' : Type u_2
β : Type u_4
G : Graph α β
e : β
x : α'
f : α → α'
⊢ (map f G).Inc e x ↔ ∃ v, G.Inc e v ∧ x = f v

Tactic:
simp only [Inc, map_isLink, map_apply]
  tauto

Goal state after:
Module: Mathlib.Combinatorics.Hindman

Goal state before:
pp: M : Type u_1
inst✝ : Semigroup M
a : Stream' M
i j : ℕ
ij : i < j
d : ℕ
hd : j = i.succ + d
this : (Stream'.drop 1 (Stream'.drop i a)).get d ∈ FP (Stream'.drop 1 (Stream'.drop i a))
⊢ FP (Stream'.drop i a).tail (a.get j)

Tactic:
Stream'.get_drop,

Goal state after:
M : Type u_1
inst✝ : Semigroup M
a : Stream' M
i j : ℕ
ij : i < j
d : ℕ
hd : j = i.succ + d
this : (Stream'.drop i a).get (1 + d) ∈ FP (Stream'.drop 1 (Stream'.drop i a))
⊢ FP (Stream'.drop i a).tail (a.get j)
Module: Mathlib.Combinatorics.Hindman

Goal state before:
pp: case H.inl
M : Type u_1
inst✝ : CommMonoid M
a : Stream' M
s : Finset ℕ
ih :
  ∀ s_1 ∈ s, ∀ (hs : (s.erase s_1).Nonempty), ∏ i ∈ s.erase s_1, a.get i ∈ FP (Stream'.drop ((s.erase s_1).min' hs) a)
hs : s.Nonempty
h : s.erase (s.min' hs) = ∅
⊢ (Stream'.drop (s.min' hs) a).head * ∏ x ∈ ∅, a.get x ∈ FP (Stream'.drop (s.min' hs) a)

Tactic:
Finset.prod_empty,

Goal state after:
case H.inl
M : Type u_1
inst✝ : CommMonoid M
a : Stream' M
s : Finset ℕ
ih :
  ∀ s_1 ∈ s, ∀ (hs : (s.erase s_1).Nonempty), ∏ i ∈ s.erase s_1, a.get i ∈ FP (Stream'.drop ((s.erase s_1).min' hs) a)
hs : s.Nonempty
h : s.erase (s.min' hs) = ∅
⊢ (Stream'.drop (s.min' hs) a).head * 1 ∈ FP (Stream'.drop (s.min' hs) a)
Module: Mathlib.RingTheory.MvPolynomial.Groebner

Goal state before:
pp: σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
f : MvPolynomial σ R
hf : m.degree f ≠ 0
hf' : m.degree (m.subLTerm f) = m.degree f
this : coeff (m.degree f) (m.subLTerm f) ≠ 0
⊢ coeff (m.degree f) (m.subLTerm f) = 0

Tactic:
simp [subLTerm, coeff_monomial, leadingCoeff]

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

Goal state before:
pp: α : Type u_1
M : Matroid α
I J X : Set α
h : M.IsBasis (J ∪ I) (X ∪ I)
hJI : Disjoint J I
hXI : Disjoint X I
⊢ (M ／ I).IsBasis J X

Tactic:
by
  refine (isBasis'_iff_isBasis ?_).1 <| h.isBasis'.contract_isBasis_union_union hJI hXI
  rw [contract_ground, subset_sdiff, and_iff_left hXI]
  exact subset_union_left.trans h.subset_ground

Goal state after:
Module: Mathlib.Combinatorics.Nullstellensatz

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
σ : Type u_2
inst✝¹ : Finite σ
inst✝ : IsDomain R
P : MvPolynomial PEmpty.{u_2 + 1} R
S : PEmpty.{u_2 + 1} → Finset R
Hdeg : ∀ (i : PEmpty.{u_2 + 1}), degreeOf i P < #(S i)
Heval : constantCoeff P = 0
this : P = C (constantCoeff P)
⊢ C (constantCoeff P) = 0

Tactic:
Heval,

Goal state after:
R : Type u_1
inst✝² : CommRing R
σ : Type u_2
inst✝¹ : Finite σ
inst✝ : IsDomain R
P : MvPolynomial PEmpty.{u_2 + 1} R
S : PEmpty.{u_2 + 1} → Finset R
Hdeg : ∀ (i : PEmpty.{u_2 + 1}), degreeOf i P < #(S i)
Heval : constantCoeff P = 0
this : P = C (constantCoeff P)
⊢ C 0 = 0
Module: Mathlib.Combinatorics.Matroid.Minor.Contract

Goal state before:
pp: α : Type u_1
M : Matroid α
K D : Set α
hK : M.IsCocircuit K
hD : D ⊂ K
⊢ (M ＼ D)✶.IsCircuit (K \ D)

Tactic:
dual_delete

Goal state after:
α : Type u_1
M : Matroid α
K D : Set α
hK : M.IsCocircuit K
hD : D ⊂ K
⊢ (M✶ ／ D).IsCircuit (K \ D)
Module: Mathlib.Combinatorics.Matroid.Minor.Contract

Goal state before:
pp: α : Type u_1
M : Matroid α
K X : Set α
hK : M.IsCocircuit K
hXK : X ⊆ K
hX : X.Nonempty
⊢ (M ＼ (K \ X))✶.IsCircuit X

Tactic:
dual_delete

Goal state after:
α : Type u_1
M : Matroid α
K X : Set α
hK : M.IsCocircuit K
hXK : X ⊆ K
hX : X.Nonempty
⊢ (M✶ ／ (K \ X)).IsCircuit X
Module: Mathlib.RingTheory.MvPolynomial.Groebner

Goal state before:
pp: σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
b : MvPolynomial σ R
hb : IsUnit (m.leadingCoeff b)
f : MvPolynomial σ R
⊢ ∃ g r, f = g * b + r ∧ m.toSyn (m.degree (b * g)) ≤ m.toSyn (m.degree f) ∧ ∀ c ∈ r.support, ¬m.degree b ≤ c

Tactic:
obtain ⟨g, r, hgr, h1, h2⟩ := div_set (B := {b}) (m := m) (by simp [hb]) f
  specialize h1 ⟨b, by simp⟩
  set q := g ⟨b, by simp⟩
  simp only [Set.mem_singleton_iff, forall_eq] at h2
  simp only at h1
  refine ⟨q, r, ?_, h1, h2⟩
  rw [hgr]
  simp only [Finsupp.linearCombination, Finsupp.coe_lsum, LinearMap.coe_smulRight, LinearMap.id_coe,
    id_eq, smul_eq_mul, add_left_inj]
  rw [Finsupp.sum_eq_single ⟨b, by simp⟩ _ (by simp)]
  simp +contextual

Goal state after:
Module: Mathlib.Combinatorics.Nullstellensatz

Goal state before:
pp: case h.Heval
R : Type u_1
inst✝² : CommRing R
σ : Type u_2
inst✝¹ : Finite σ
inst✝ : IsDomain R
S : σ → Finset R
Sne : ∀ (i : σ), (S i).Nonempty
f : MvPolynomial σ R
Heval : ∀ (x : σ → R), (∀ (i : σ), x i ∈ S i) → (eval x) f = 0
this : LinearOrder σ := IsWellOrder.linearOrder WellOrderingRel
h : σ →₀ MvPolynomial σ R
r : MvPolynomial σ R
hf : f = (linearCombination (MvPolynomial σ R) fun i ↦ Alon.P (S i) i) h + r
hh : ∀ (i : σ), degLex.toSyn (degLex.degree (Alon.P (S i) i * h i)) ≤ degLex.toSyn (degLex.degree f)
hr : ∀ c ∈ r.support, ∀ (i : σ), ¬degLex.degree (Alon.P (S i) i) ≤ c
x : σ → R
hx : ∀ (i : σ), x i ∈ S i
⊢ (eval x) r = 0

Tactic:
Iff.symm sub_eq_iff_eq_add'

Goal state after:
case h.Heval
R : Type u_1
inst✝² : CommRing R
σ : Type u_2
inst✝¹ : Finite σ
inst✝ : IsDomain R
S : σ → Finset R
Sne : ∀ (i : σ), (S i).Nonempty
f : MvPolynomial σ R
Heval : ∀ (x : σ → R), (∀ (i : σ), x i ∈ S i) → (eval x) f = 0
this : LinearOrder σ := IsWellOrder.linearOrder WellOrderingRel
h : σ →₀ MvPolynomial σ R
r : MvPolynomial σ R
hf : f - (linearCombination (MvPolynomial σ R) fun i ↦ Alon.P (S i) i) h = r
hh : ∀ (i : σ), degLex.toSyn (degLex.degree (Alon.P (S i) i * h i)) ≤ degLex.toSyn (degLex.degree f)
hr : ∀ c ∈ r.support, ∀ (i : σ), ¬degLex.degree (Alon.P (S i) i) ≤ c
x : σ → R
hx : ∀ (i : σ), x i ∈ S i
⊢ (eval x) r = 0
Module: Mathlib.Combinatorics.Nullstellensatz

Goal state before:
pp: case neg
R : Type u_1
inst✝² : CommRing R
σ : Type u_2
inst✝¹ : Finite σ
inst✝ : IsDomain R
f : MvPolynomial σ R
t : σ →₀ ℕ
ht : coeff t f ≠ 0
ht' : f.totalDegree = Finsupp.degree t
S : σ → Finset R
htS : ∀ (i : σ), t i < #(S i)
x✝ : LinearOrder σ := ⋯
Heval : ∀ (s : σ → R), (∀ (i : σ), s i ∈ S i) → (eval s) f = 0
h : σ →₀ MvPolynomial σ R
hh : ∀ (i : σ), ((∏ s ∈ S i, (X i - C s)) * h i).totalDegree ≤ f.totalDegree
hf : f = (linearCombination (MvPolynomial σ R) fun i ↦ ∏ r ∈ S i, (X i - C r)) h
i : σ
a✝ : i ∈ h.support
g : MvPolynomial σ R := ⋯
hg : g = h i * Alon.P (S i) i
hi : ¬h i = 0
this : (h i).totalDegree + #(S i) ≤ Finsupp.degree t
p q : σ →₀ ℕ
hpq : p + q = t
hq✝ : q ∈ (∏ r ∈ S i, (X i - C r)).support
e : ℕ
hq' : e ≤ #(S i)
hq : q = single i e
⊢ (h i).totalDegree < ∑ i ∈ p.support, p i

Tactic:
rw [← Finsupp.degree_apply]

Goal state after:
case neg
R : Type u_1
inst✝² : CommRing R
σ : Type u_2
inst✝¹ : Finite σ
inst✝ : IsDomain R
f : MvPolynomial σ R
t : σ →₀ ℕ
ht : coeff t f ≠ 0
ht' : f.totalDegree = Finsupp.degree t
S : σ → Finset R
htS : ∀ (i : σ), t i < #(S i)
x✝ : LinearOrder σ := IsWellOrder.linearOrder WellOrderingRel
Heval : ∀ (s : σ → R), (∀ (i : σ), s i ∈ S i) → (eval s) f = 0
h : σ →₀ MvPolynomial σ R
hh : ∀ (i : σ), ((∏ s ∈ S i, (X i - C s)) * h i).totalDegree ≤ f.totalDegree
hf : f = (linearCombination (MvPolynomial σ R) fun i ↦ ∏ r ∈ S i, (X i - C r)) h
i : σ
a✝ : i ∈ h.support
g : MvPolynomial σ R := h i * Alon.P (S i) i
hg : g = h i * Alon.P (S i) i
hi : ¬h i = 0
this : (h i).totalDegree + #(S i) ≤ Finsupp.degree t
p q : σ →₀ ℕ
hpq : p + q = t
hq✝ : q ∈ (∏ r ∈ S i, (X i - C r)).support
e : ℕ
hq' : e ≤ #(S i)
hq : q = single i e
⊢ (h i).totalDegree < Finsupp.degree p
Module: Mathlib.Combinatorics.Schnirelmann

Goal state before:
pp: case mpr
A : Set ℕ
inst✝ : DecidablePred fun x ↦ x ∈ A
h : {0}ᶜ ⊆ A
x✝ : { n // 0 < n }
n : ℕ
hn : 0 < n
x : ℕ
hx : x ∈ Ioc 0 ↑⟨n, hn⟩
⊢ x ∈ A

Tactic:
exact h (mem_Ioc.1 hx).1.ne'

Goal state after: