mathlib-initiative/mathlib-tactics huggingface dataset:
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}
hS : ∀ (x : σ → K), x ∈ S ↔ ∀ i ∈ s, (eval x) (f i) = 0
F : MvPolynomial σ K := ∏ i ∈ s, (1 - f i ^ (q - 1))
x : σ → K
⊢ ∏ i ∈ s, (eval x) (1 - f i ^ (q - 1)) = if x ∈ S then 1 else 0

Tactic:
simp only [(eval x).map_sub, (eval x).map_pow, (eval x).map_one]

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
F : MvPolynomial σ K := ∏ i ∈ s, (1 - f i ^ (q - 1))
x : σ → K
⊢ ∏ x_1 ∈ s, (1 - (eval x) (f x_1) ^ (q - 1)) = if x ∈ S then 1 else 0
Module: Mathlib.Combinatorics.Colex

Goal state before:
pp: α : Type u_1
inst✝ : PartialOrder α
s : Finset α
a b : α
ha : a ∉ s
hb : b ∉ s
⊢ toColex (cons a s ha) ≤ toColex (cons b s hb) ↔ a ≤ b

Tactic:
obtain rfl | hab := eq_or_ne a b

Goal state after:
case inl
α : Type u_1
inst✝ : PartialOrder α
s : Finset α
a : α
ha hb : a ∉ s
⊢ toColex (cons a s ha) ≤ toColex (cons a s hb) ↔ a ≤ a

case inr
α : Type u_1
inst✝ : PartialOrder α
s : Finset α
a b : α
ha : a ∉ s
hb : b ∉ s
hab : a ≠ b
⊢ toColex (cons a s ha) ≤ toColex (cons b s hb) ↔ a ≤ b
Module: Mathlib.Combinatorics.Colex

Goal state before:
pp: α : Type u_1
inst✝¹ : PartialOrder α
s : Finset α
a b : α
inst✝ : DecidableEq α
ha : a ∈ s
hb : b ∈ s
⊢ toColex (s.erase a) ≤ toColex (s.erase b) ↔ b ≤ a

Tactic:
obtain rfl | hab := eq_or_ne a b

Goal state after:
case inl
α : Type u_1
inst✝¹ : PartialOrder α
s : Finset α
a : α
inst✝ : DecidableEq α
ha hb : a ∈ s
⊢ toColex (s.erase a) ≤ toColex (s.erase a) ↔ a ≤ a

case inr
α : Type u_1
inst✝¹ : PartialOrder α
s : Finset α
a b : α
inst✝ : DecidableEq α
ha : a ∈ s
hb : b ∈ s
hab : a ≠ b
⊢ toColex (s.erase a) ≤ toColex (s.erase b) ↔ b ≤ a
Module: Mathlib.Combinatorics.Colex

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
s t : Finset α
⊢ toColex s ≤ toColex t ↔ ∀ (hst : s ≠ t), (s ∆ t).max' ⋯ ∈ t

Tactic:
refine ⟨fun h hst ↦ ?_, fun h a has hat ↦ ?_⟩

Goal state after:
case refine_1
α : Type u_1
inst✝ : LinearOrder α
s t : Finset α
h : toColex s ≤ toColex t
hst : s ≠ t
⊢ (s ∆ t).max' ⋯ ∈ t

case refine_2
α : Type u_1
inst✝ : LinearOrder α
s t : Finset α
h : ∀ (hst : s ≠ t), (s ∆ t).max' ⋯ ∈ t
a : α
has : a ∈ ofColex (toColex s)
hat : a ∉ ofColex (toColex t)
⊢ ∃ b ∈ ofColex (toColex t), b ∉ ofColex (toColex s) ∧ a ≤ b
Module: Mathlib.Combinatorics.Derangements.Basic

Goal state before:
pp: case mpr
α : Type u_1
inst✝ : DecidableEq α
a : α
f : Perm α
h_opfp : f ∈ {f | fixedPoints ⇑f ⊆ {a}}
⊢ f ∈ fiber (some a)

Tactic:
use Equiv.Perm.decomposeOption.symm (some a, f)

Goal state after:
case h
α : Type u_1
inst✝ : DecidableEq α
a : α
f : Perm α
h_opfp : f ∈ {f | fixedPoints ⇑f ⊆ {a}}
⊢ Perm.decomposeOption.symm (some a, f) ∈ derangements (Option α) ∧
    Perm.decomposeOption (Perm.decomposeOption.symm (some a, f)) = (some a, f)
Module: Mathlib.Combinatorics.Configuration

Goal state before:
pp: P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : ProjectivePlane P L
inst✝¹ : Finite P
inst✝ : Finite L
⊢ 1 < order P L

Tactic:
obtain ⟨p₁, p₂, p₃, l₁, l₂, l₃, -, -, h₂₁, h₂₂, h₂₃, h₃₁, h₃₂, h₃₃⟩ := @exists_config P L _ _
  cases nonempty_fintype { p : P // p ∈ l₂ }
  rw [← add_lt_add_iff_right 1, ← pointCount_eq _ l₂, pointCount, Nat.card_eq_fintype_card,
    Fintype.two_lt_card_iff]
  simp_rw [Ne, Subtype.ext_iff]
  have h := mkPoint_ax (P := P) (L := L) fun h => h₂₁ ((congr_arg (p₂ ∈ ·) h).mpr h₂₂)
  exact
    ⟨⟨mkPoint _, h.2⟩, ⟨p₂, h₂₂⟩, ⟨p₃, h₃₂⟩, ne_of_mem_of_not_mem h.1 h₂₁,
      ne_of_mem_of_not_mem h.1 h₃₁, ne_of_mem_of_not_mem h₂₃ h₃₃⟩

Goal state after:
Module: Mathlib.Combinatorics.Enumerative.Catalan.Basic

Goal state before:
pp: n : ℕ
⊢ catalan (n + 1) = ∑ ij ∈ antidiagonal n, catalan ij.1 * catalan ij.2

Tactic:
catalan_succ,

Goal state after:
n : ℕ
⊢ ∑ i, catalan ↑i * catalan (n - ↑i) = ∑ ij ∈ antidiagonal n, catalan ij.1 * catalan ij.2
Module: Mathlib.Combinatorics.Additive.VerySmallDoubling

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A : Finset G
h : ↑(#(A * A)) < 3 / 2 * ↑(#A)
h₀ : A.Nonempty
h₁ : ∀ a ∈ A⁻¹ * A, 1 / 2 * ↑(#A) < ↑(#({xy ∈ A ×ˢ A | xy.1 * xy.2⁻¹ = a}))
a b : G
ha : a ∈ A
hb : b ∈ A
⊢ ∃ y ∈ A, y⁻¹ = b⁻¹

Tactic:
by simp [hb]

Goal state after:
Module: Mathlib.Combinatorics.Enumerative.Catalan.Basic

Goal state before:
pp: case ind
d : ℕ
hd : ∀ m ≤ d, ↑(catalan m) = ↑m.centralBinom / (↑m + 1)
⊢ ↑(catalan d.succ) = ↑d.succ.centralBinom / (↑d.succ + 1)

Tactic:
catalan_succ,

Goal state after:
case ind
d : ℕ
hd : ∀ m ≤ d, ↑(catalan m) = ↑m.centralBinom / (↑m + 1)
⊢ ↑(∑ i, catalan ↑i * catalan (d - ↑i)) = ↑d.succ.centralBinom / (↑d.succ + 1)
Module: Mathlib.Combinatorics.Enumerative.DyckWord

Goal state before:
pp: p q r : DyckWord
⊢ p + q + r = p + (q + r)

Tactic:
ext1; apply append_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
h : ↑(#(A * A)) < 3 / 2 * ↑(#A)
a : G
ha : a ∈ A
⊢ a •> ((A⁻¹ * A) <• a) ⊆ A * A

Tactic:
by
  intro z hz
  simp only [mem_smul_finset, smul_eq_mul_unop, unop_op, smul_eq_mul, mem_mul, mem_inv,
    exists_exists_and_eq_and] at hz
  obtain ⟨d, ⟨b, hb, c, hc, rfl⟩, hz⟩ := hz
  let l : Finset G := A ∩ ((z * a⁻¹) • (A⁻¹ * A))
    -- ^ set of x ∈ A st ∃ y ∈ H a with x y = z
  let r : Finset G := (a • (A⁻¹ * A)) ∩ (z • A⁻¹)
    -- ^ set of x ∈ a H st ∃ y ∈ A with x y = z
  have : (A⁻¹ * A) * (A⁻¹ * A) = A⁻¹ * A := by
    rw [← coe_inj, coe_mul, coe_mul, ← invMulSubgroup_eq_inv_mul _ h, coe_mul_coe]
  have hl : l = A := by
    rw [inter_eq_left, ← this, subset_smul_finset_iff]
    simp only [← hz, mul_inv_rev, inv_inv, ← mul_assoc]
    refine smul_finset_subset_mul ?_
    simp [mul_mem_mul, ha, hb, hc]
  have hr : r = z • A⁻¹ := by
    rw [inter_eq_right, ← this, mul_assoc _ A,
      ← mul_inv_eq_inv_mul_of_doubling_lt_two (weaken_doubling h), subset_smul_finset_iff]
    simp only [← mul_assoc, smul_smul]
    refine smul_finset_subset_mul ?_
    simp [← hz, mul_mem_mul, ha, hb, hc]
  have lr : l ∪ r ⊆ a • (A⁻¹ * A) := by
    rw [union_subset_iff, hl]
    exact ⟨A_subset_aH a ha, inter_subset_left⟩
  have : #l = #A := by rw [hl]
  have : #r = #A := by rw [hr, card_smul_finset, card_inv]
  have : #(l ∪ r) < 2 * #A := by
    refine (card_le_card lr).trans_lt ?_
    rw [card_smul_finset]
    exact weak_invMulSubgroup_bound h
  have ⟨t, ht⟩ : (l ∩ r).Nonempty := by
    rw [← card_pos]
    linarith [card_inter_add_card_union l r]
  simp only [hl, hr, mem_inter, ← inv_smul_mem_iff, smul_eq_mul, mem_inv', mul_inv_rev,
    inv_inv] at ht
  rw [mem_mul]
  exact ⟨t, ht.1, t⁻¹ * z, ht.2, by simp⟩

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

Goal state before:
pp: F : Type u_1
𝕜 : Type u_2
𝕝 : Type u_3
𝕞 : Type u_4
α : Type u_5
β : Type u_6
inst✝⁵ : Preorder α
inst✝⁴ : LocallyFiniteOrder α
inst✝³ : DecidableEq α
inst✝² : Semiring 𝕜
inst✝¹ : Semiring 𝕝
inst✝ : Module 𝕜 𝕝
f : IncidenceAlgebra 𝕝 α
a b : α
hab : a ≤ b
⊢ (1 • f) a b = f a b

Tactic:
simp [ite_smul, hab]

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

Goal state before:
pp: case pos
p q : DyckWord
h : p = 0
⊢ (p + q).firstReturn = q.firstReturn

pp: case neg
p q : DyckWord
h : ¬p = 0
⊢ (p + q).firstReturn = p.firstReturn

Tactic:
· simp [h]

Goal state after:
case neg
p q : DyckWord
h : ¬p = 0
⊢ (p + q).firstReturn = p.firstReturn
Module: Mathlib.Combinatorics.Enumerative.IncidenceAlgebra

Goal state before:
pp: 𝕜 : Type u_2
α : Type u_5
inst✝³ : Ring 𝕜
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b : α
this✝ : DecidableLE α := Classical.decRel LE.le
mud : IncidenceAlgebra 𝕜 αᵒᵈ := { toFun := fun a b ↦ (mu 𝕜) (ofDual b) (ofDual a), eq_zero_of_not_le' := ⋯ }
this : mud * zeta 𝕜 = mu 𝕜 * zeta 𝕜
⊢ mu 𝕜 = mud

Tactic:
apply_fun (· * mu 𝕜) at this

Goal state after:
𝕜 : Type u_2
α : Type u_5
inst✝³ : Ring 𝕜
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b : α
this✝ : DecidableLE α := Classical.decRel LE.le
mud : IncidenceAlgebra 𝕜 αᵒᵈ := { toFun := fun a b ↦ (mu 𝕜) (ofDual b) (ofDual a), eq_zero_of_not_le' := ⋯ }
this : mud * zeta 𝕜 * mu 𝕜 = mu 𝕜 * zeta 𝕜 * mu 𝕜
⊢ mu 𝕜 = mud
Module: Mathlib.Combinatorics.Enumerative.DyckWord

Goal state before:
pp: case pos
p q : DyckWord
h : p = 0
⊢ q ≤ p + q

pp: case neg
p q : DyckWord
h : ¬p = 0
⊢ q ≤ p + q

Tactic:
· simp [h]

Goal state after:
case neg
p q : DyckWord
h : ¬p = 0
⊢ q ≤ p + q
Module: Mathlib.Combinatorics.Additive.VerySmallDoubling

Goal state before:
pp: case inr.intro.calc_1
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
r : G → ℕ := fun z ↦ A.convolution A⁻¹ z
r_inv : ∀ (z : G), r z⁻¹ = r z
⊢ (φ - K) * (K - ψ) / ((2 - K) * K) * ↑(#S) ≤ ↑(#({z ∈ S | (K - 1) * ↑(#A) < ↑(r z)}))

Tactic:
set l : ℕ := #{z ∈ S | (K - 1) * #A < r z} with hk
    -- By upper-bounding `r(z)` by `(K - 1)|A|` for the `z` with few representations,
    -- and by `|A|` for the `z` with many representations,
    -- we get `|A|² ≤ l|A| + (|S| - l)(K - 1)|A| = ((2 - K)l + (K - 1)|S|)|A|`.
    have ineq : #A * #A ≤ ((2 - K) * l + (K - 1) * #S) * #A := by
      calc
            (#A : ℝ) * #A
        _ = #A * #A⁻¹ := by simp
        _ = #(A ×ˢ A⁻¹) := by simp
        _ = ∑ z ∈ S, ↑(r z) := by
          norm_cast
          exact card_eq_sum_card_fiberwise fun xy hxy ↦
            mul_mem_mul (mem_product.mp hxy).1 (mem_product.mp hxy).2
        _ = ∑ z ∈ S with (K - 1) * #A < r z, ↑(r z) + ∑ z ∈ S with r z ≤ (K - 1) * #A, ↑(r z) := by
          norm_cast; simp_rw [← not_lt, sum_filter_add_sum_filter_not]
        _ ≤ ∑ z ∈ S with (K - 1) * #A < r z, ↑(#A)
          + ∑ z ∈ S with r z ≤ (K - 1) * #A, (K - 1) * #A := by
          gcongr with z hz z hz
          · exact convolution_le_card_left
          · simp_all
        _ = l * #A + (#S - l) * (K - 1) * #A := by
          simp [hk, ← not_lt, mul_assoc,
            ← S.card_filter_add_card_filter_not fun z ↦ (K - 1) * #A < r z]
        _ = ((2 - K) * l + (K - 1) * #S) * #A := by ring
    -- By cancelling `|A|` on both sides, we get `|A| ≤ (2 - K)l + (K - 1)|S|`.
    -- By composing with `|S| ≤ K|A|`, we get `|S| ≤ (2 - K)Kl + (K - 1)K|S|`.
    have : 0 < #A := by positivity
    replace ineq := calc
          (#S : ℝ)
      _ ≤ K * #A := ‹_›
      _ ≤ K * ((2 - K) * l + (K - 1) * #S) := by
        gcongr; exact le_of_mul_le_mul_right ineq <| by positivity
      _ = (2 - K) * K * l + (K - 1) * K * #S := by ring
    -- Now, we are done.
    calc
          (φ - K) * (K - ψ) / ((2 - K) * K) * #S
      _ = (φ - K) * (K - ψ) * #S / ((2 - K) * K) := div_mul_eq_mul_div ..
      _ ≤ (2 - K) * K * l / ((2 - K) * K) := by
        have := Real.goldenRatio_mul_goldenConj
        have := Real.goldenRatio_add_goldenConj
        rw [show (φ - K) * (K - ψ) = 1 - (K - 1) * K by grind]
        gcongr ?_ / _
        linarith [ineq]
      _ = l := by field

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

Goal state before:
pp: case inl
R : Type u_1
inst✝² : TopologicalSpace R
inst✝¹ : T2Space R
inst✝ : CommSemiring R
⊢ Multipliable fun i ↦ ∑ j ∈ range 0, X ^ ((i + 1) * j)

pp: case inr
R : Type u_1
inst✝² : TopologicalSpace R
inst✝¹ : T2Space R
inst✝ : CommSemiring R
m : ℕ
hm : m > 0
⊢ Multipliable fun i ↦ ∑ j ∈ range m, X ^ ((i + 1) * j)

Tactic:
· simpa using multipliable_of_exists_eq_zero ⟨0, rfl⟩

Goal state after:
case inr
R : Type u_1
inst✝² : TopologicalSpace R
inst✝¹ : T2Space R
inst✝ : CommSemiring R
m : ℕ
hm : m > 0
⊢ Multipliable fun i ↦ ∑ j ∈ range m, X ^ ((i + 1) * j)
Module: Mathlib.Combinatorics.Enumerative.Partition.Glaisher

Goal state before:
pp: case refine_1
R : Type u_1
inst✝⁴ : TopologicalSpace R
inst✝³ : T2Space R
inst✝² : CommRing R
inst✝¹ : NoZeroDivisors R
inst✝ : IsTopologicalRing R
m : ℕ
hm : 0 < m
a✝ : Nontrivial R
a b : ↑(Function.mulSupport fun i ↦ 1 - (X ^ (i + 1)) ^ m)
h : (fun i ↦ (↑i + 1) * m - 1) a = (fun i ↦ (↑i + 1) * m - 1) b
⊢ a = b

Tactic:
tsub_left_inj (by nlinarith) (by nlinarith),

Goal state after:
case refine_1
R : Type u_1
inst✝⁴ : TopologicalSpace R
inst✝³ : T2Space R
inst✝² : CommRing R
inst✝¹ : NoZeroDivisors R
inst✝ : IsTopologicalRing R
m : ℕ
hm : 0 < m
a✝ : Nontrivial R
a b : ↑(Function.mulSupport fun i ↦ 1 - (X ^ (i + 1)) ^ m)
h : (↑a + 1) * m = (↑b + 1) * m
⊢ a = b
Module: Mathlib.Combinatorics.Additive.VerySmallDoubling

Goal state before:
pp: case refine_1
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
K : ℝ
S : Finset G
hK : K < 1
hS : S.Nonempty
H : ∀ (A : Finset G), A.Nonempty → ¬IsFragment K S A
ex : Finset G → ℝ := expansion K S
κ : ℝ := connectivity K S
κ_add_one_pos : 0 < κ + 1
one_sub_K_pos : 0 < 1 - K
t : ℕ := ⌊(κ + 1) / (1 - K)⌋₊
largeA : ∀ {A : Finset G}, t < #A → κ + 1 < ex A
M : Finset ℝ := {x ∈ map Nat.castEmbedding (Icc (#S) (t * #S)) - K •> map Nat.castEmbedding (Icc 1 t) | κ < x}
A : Finset G
hA : A.Nonempty
hAt : #A ≤ t
⊢ ↑(#(A * S)) ∈ map Nat.castEmbedding (Icc (#S) (t * #S))

pp: case refine_2
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
K : ℝ
S : Finset G
hK : K < 1
hS : S.Nonempty
H : ∀ (A : Finset G), A.Nonempty → ¬IsFragment K S A
ex : Finset G → ℝ := expansion K S
κ : ℝ := connectivity K S
κ_add_one_pos : 0 < κ + 1
one_sub_K_pos : 0 < 1 - K
t : ℕ := ⌊(κ + 1) / (1 - K)⌋₊
largeA : ∀ {A : Finset G}, t < #A → κ + 1 < ex A
M : Finset ℝ := {x ∈ map Nat.castEmbedding (Icc (#S) (t * #S)) - K •> map Nat.castEmbedding (Icc 1 t) | κ < x}
A : Finset G
hA : A.Nonempty
hAt : #A ≤ t
⊢ K * ↑(#A) ∈ K •> map Nat.castEmbedding (Icc 1 t)

Tactic:
· apply mem_map_of_mem
      exact mem_Icc.2 ⟨card_le_card_mul_left hA, by grw [card_mul_le, hAt]⟩

Goal state after:
case refine_2
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
K : ℝ
S : Finset G
hK : K < 1
hS : S.Nonempty
H : ∀ (A : Finset G), A.Nonempty → ¬IsFragment K S A
ex : Finset G → ℝ := expansion K S
κ : ℝ := connectivity K S
κ_add_one_pos : 0 < κ + 1
one_sub_K_pos : 0 < 1 - K
t : ℕ := ⌊(κ + 1) / (1 - K)⌋₊
largeA : ∀ {A : Finset G}, t < #A → κ + 1 < ex A
M : Finset ℝ := {x ∈ map Nat.castEmbedding (Icc (#S) (t * #S)) - K •> map Nat.castEmbedding (Icc 1 t) | κ < x}
A : Finset G
hA : A.Nonempty
hAt : #A ≤ t
⊢ K * ↑(#A) ∈ K •> map Nat.castEmbedding (Icc 1 t)
Module: Mathlib.Combinatorics.Enumerative.Stirling

Goal state before:
pp: n : ℕ
⊢ (n + 1).stirlingSecond 1 = 1

Tactic:
by
  induction n with
  | zero => rfl
  | succ n ih => rw [stirlingSecond, stirlingSecond_succ_zero, ih]

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

Goal state before:
pp: α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
hG : G.LocallyLinear
⊢ #(G.cliqueFinset 3) ≤ ruzsaSzemerediNumber α

Tactic:
classical
  exact le_findGreatest card_cliqueFinset_le ⟨G, inferInstance, by congr, hG⟩

Goal state after:
Module: Mathlib.Combinatorics.HalesJewett

Goal state before:
pp: case pos
α : Type u
inst✝¹ : Fintype α
κ : Type (max v u)
inst✝ : Finite κ
val✝ : Fintype κ
h : Nonempty α
r : ℕ
ι : Type
_inst✝ : Fintype ι
ι' : Type
_inst : Fintype ι'
C : (ι ⊕ ι' → Option α) → κ
l' : Line α ι'
C' : (ι → Option α) → κ
hl' : ∀ (x : α), (fun v' v ↦ C (Sum.elim v (some ∘ v'))) (↑l' x) = C'
mono_of_mono : (∃ l, IsMono C' l) → ∃ l, IsMono C l
s : ColorFocused C'
sr : s.lines.card = r
p : AlmostMono C'
p_mem : p ∈ s.lines
hp : p.color = C' s.focus
⊢ ∀ (x : Option α), C' (↑p.line x) = p.color

Tactic:
rintro (_ | _)

Goal state after:
case pos.none
α : Type u
inst✝¹ : Fintype α
κ : Type (max v u)
inst✝ : Finite κ
val✝ : Fintype κ
h : Nonempty α
r : ℕ
ι : Type
_inst✝ : Fintype ι
ι' : Type
_inst : Fintype ι'
C : (ι ⊕ ι' → Option α) → κ
l' : Line α ι'
C' : (ι → Option α) → κ
hl' : ∀ (x : α), (fun v' v ↦ C (Sum.elim v (some ∘ v'))) (↑l' x) = C'
mono_of_mono : (∃ l, IsMono C' l) → ∃ l, IsMono C l
s : ColorFocused C'
sr : s.lines.card = r
p : AlmostMono C'
p_mem : p ∈ s.lines
hp : p.color = C' s.focus
⊢ C' (↑p.line none) = p.color

case pos.some
α : Type u
inst✝¹ : Fintype α
κ : Type (max v u)
inst✝ : Finite κ
val✝¹ : Fintype κ
h : Nonempty α
r : ℕ
ι : Type
_inst✝ : Fintype ι
ι' : Type
_inst : Fintype ι'
C : (ι ⊕ ι' → Option α) → κ
l' : Line α ι'
C' : (ι → Option α) → κ
hl' : ∀ (x : α), (fun v' v ↦ C (Sum.elim v (some ∘ v'))) (↑l' x) = C'
mono_of_mono : (∃ l, IsMono C' l) → ∃ l, IsMono C l
s : ColorFocused C'
sr : s.lines.card = r
p : AlmostMono C'
p_mem : p ∈ s.lines
hp : p.color = C' s.focus
val✝ : α
⊢ C' (↑p.line (some val✝)) = p.color
Module: Mathlib.Combinatorics.Matroid.Minor.Order

Goal state before:
pp: α : Type u_1
M N : Matroid α
h : N ≤m M
hE : M.E ⊆ N.E
⊢ M = N

Tactic:
by
  obtain ⟨C, D, rfl⟩ := h
  rw [delete_ground, contract_ground, subset_sdiff, subset_sdiff] at hE
  rw [← contract_inter_ground_eq, hE.1.2.symm.inter_eq, contract_empty, ← delete_inter_ground_eq,
    hE.2.symm.inter_eq, delete_empty]

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

Goal state before:
pp: α : Type u_1
M : Matroid α
C₁ C₂ : Set α
⊢ M ／ C₁ ／ C₂ = M ／ (C₁ ∪ C₂)

Tactic:
by
  simp [← dual_inj]

Goal state after:
Module: Mathlib.Combinatorics.HalesJewett

Goal state before:
pp: case refine_3
M : Type u_5
κ : Type u_6
inst✝¹ : AddCommMonoid M
S : Finset M
inst✝ : Finite κ
C : M → κ
ι : Type
_inst : Fintype ι
l : Line (↥S) ι
c : κ
hl : ∀ (x : ↥S), (fun v ↦ C (∑ i, ↑(v i))) (↑l x) = c
s : Finset ι := {i | l.idxFun i = none}
hs : s = {i | l.idxFun i = none}
x : M
xs : x ∈ S
⊢ C (#s • x + ∑ i ∈ sᶜ, (Option.map (fun m ↦ ↑m) (l.idxFun i)).getD 0) = c

Tactic:
← hl ⟨x, xs⟩

Goal state after:
case refine_3
M : Type u_5
κ : Type u_6
inst✝¹ : AddCommMonoid M
S : Finset M
inst✝ : Finite κ
C : M → κ
ι : Type
_inst : Fintype ι
l : Line (↥S) ι
c : κ
hl : ∀ (x : ↥S), (fun v ↦ C (∑ i, ↑(v i))) (↑l x) = c
s : Finset ι := {i | l.idxFun i = none}
hs : s = {i | l.idxFun i = none}
x : M
xs : x ∈ S
⊢ C (#s • x + ∑ i ∈ sᶜ, (Option.map (fun m ↦ ↑m) (l.idxFun i)).getD 0) = (fun v ↦ C (∑ i, ↑(v i))) (↑l ⟨x, xs⟩)
Module: Mathlib.Combinatorics.Matroid.Minor.Contract

Goal state before:
pp: α : Type u_1
M : Matroid α
K C : Set α
hK : M.IsCircuit K
hC : C ⊂ K
⊢ (M ／ C).IsCircuit (K \ C)

Tactic:
suffices ∀ e ∈ K, e ∉ C → M.Indep (K \ {e} ∪ C) by
    simpa [isCircuit_iff_dep_forall_sdiff_singleton_indep, sdiff_sdiff_comm (s := K) (t := C),
    dep_iff, (hK.ssubset_indep hC).contract_indep_iff, sdiff_subset_sdiff_left hK.subset_ground,
    disjoint_sdiff_left, sdiff_union_of_subset hC.subset, hK.not_indep]

Goal state after:
α : Type u_1
M : Matroid α
K C : Set α
hK : M.IsCircuit K
hC : C ⊂ K
⊢ ∀ e ∈ K, e ∉ C → M.Indep (K \ {e} ∪ C)
Module: Mathlib.Combinatorics.Quiver.Arborescence

Goal state before:
pp: V : Type u
inst✝ : Quiver V
r : V
height : V → ℕ
height_lt : ∀ ⦃a b : V⦄ (a_1 : a ⟶ b), height a < height b
unique_arrow : ∀ ⦃a b c : V⦄ (e : a ⟶ c) (f : b ⟶ c), a = b ∧ e ≍ f
root_or_arrow : ∀ (b : V), b = r ∨ ∃ a, Nonempty (a ⟶ b)
b✝ a b : V
p : Path a b
⊢ height a ≤ height b

Tactic:
induction p with

Goal state after:
Module: Mathlib.Combinatorics.Quiver.Arborescence

Goal state before:
pp: V : Type u
inst✝ : Quiver V
r : V
height : V → ℕ
height_lt : ∀ ⦃a b : V⦄ (a_1 : a ⟶ b), height a < height b
unique_arrow : ∀ ⦃a b c : V⦄ (e : a ⟶ c) (f : b ⟶ c), a = b ∧ e ≍ f
root_or_arrow : ∀ (b : V), b = r ∨ ∃ a, Nonempty (a ⟶ b)
b : V
height_le : ∀ {a b : V} (a_1 : Path a b), height a ≤ height b
p q : Path r b
⊢ p = q

Tactic:
induction p with

Goal state after:
Module: Mathlib.Combinatorics.Optimization.ValuedCSP

Goal state before:
pp: case hle
D : Type u_1
C : Type u_3
inst✝² : AddCommMonoid C
inst✝¹ : PartialOrder C
inst✝ : IsOrderedCancelAddMonoid C
f : (Fin 2 → D) → C
ω : FractionalOperation D 2
valid : ω.IsValid
symmega : ω.IsSymmetric
a b : D
contr : 2 • (Multiset.map f (ω.tt ![![a, b], ![b, a]])).sum ≤ ω.size • 2 • f ![a, b]
hab : a ≠ b
mcfab : HasMaxCutPropertyAt f a b
⊢ ∀ i ∈ ω.tt ![![a, b], ![b, a]], f ![a, b] ≤ f i

Tactic:
intro r rin

Goal state after:
case hle
D : Type u_1
C : Type u_3
inst✝² : AddCommMonoid C
inst✝¹ : PartialOrder C
inst✝ : IsOrderedCancelAddMonoid C
f : (Fin 2 → D) → C
ω : FractionalOperation D 2
valid : ω.IsValid
symmega : ω.IsSymmetric
a b : D
contr : 2 • (Multiset.map f (ω.tt ![![a, b], ![b, a]])).sum ≤ ω.size • 2 • f ![a, b]
hab : a ≠ b
mcfab : HasMaxCutPropertyAt f a b
r : Fin (Nat.succ 0).succ → D
rin : r ∈ ω.tt ![![a, b], ![b, a]]
⊢ f ![a, b] ≤ f r
Module: Mathlib.Combinatorics.Quiver.ConnectedComponent

Goal state before:
pp: V : Type u_2
inst✝ : Quiver V
h : IsStronglyConnected V
a b : Symmetrify V
p : Path a b
⊢ Nonempty (Path a b)

Tactic:
induction p with

Goal state after:
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
⊢ ∀ b_1 ∈ {b}, IsUnit (m.leadingCoeff b_1)

Tactic:
by simp [hb]

Goal state after:
Module: Mathlib.Combinatorics.Nullstellensatz

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
ι : Type u_3
i : ι
S : Finset R
m : ι →₀ ℕ
hP : P S i = (rename fun x ↦ i) (P S ())
e : Unit →₀ ℕ
he : ¬coeff e (P S ()) = 0
hm : mapDomain (fun x ↦ i) e = m
this : Nontrivial R
⊢ ∃ e ≤ #S, m = single i e

Tactic:
refine ⟨e (), ?_, ?_⟩

Goal state after:
case refine_1
R : Type u_1
inst✝ : CommRing R
ι : Type u_3
i : ι
S : Finset R
m : ι →₀ ℕ
hP : P S i = (rename fun x ↦ i) (P S ())
e : Unit →₀ ℕ
he : ¬coeff e (P S ()) = 0
hm : mapDomain (fun x ↦ i) e = m
this : Nontrivial R
⊢ e () ≤ #S

case refine_2
R : Type u_1
inst✝ : CommRing R
ι : Type u_3
i : ι
S : Finset R
m : ι →₀ ℕ
hP : P S i = (rename fun x ↦ i) (P S ())
e : Unit →₀ ℕ
he : ¬coeff e (P S ()) = 0
hm : mapDomain (fun x ↦ i) e = m
this : Nontrivial R
⊢ m = single i (e ())
Module: Mathlib.Combinatorics.Quiver.Path.Vertices

Goal state before:
pp: V : Type u_2
inst✝ : Quiver V
a b : V
p : Path a b
⊢ p.vertices.length = p.length + 1

Tactic:
induction p with

Goal state after:
Module: Mathlib.Combinatorics.Quiver.Path.Vertices

Goal state before:
pp: V : Type u_1
inst✝ : Quiver V
a b : V
p : Path a b
⊢ a ∈ p.vertices

Tactic:
induction p with

Goal state after:
Module: Mathlib.Combinatorics.Quiver.Path.Vertices

Goal state before:
pp: V : Type u_1
inst✝ : Quiver V
a b : V
p : Path a b
⊢ p.vertices.head? = some a

Tactic:
induction p with

Goal state after:
Module: Mathlib.Combinatorics.Quiver.Covering

Goal state before:
pp: U : Type u_1
inst✝¹ : Quiver U
V : Type u_2
inst✝ : Quiver V
φ : U ⥤q V
u : U
⊢ φ.symmetrify.star u =
    ⇑(Quiver.symmetrifyStar (φ.obj u)).symm ∘ Sum.map (φ.star u) (φ.costar u) ∘ ⇑(Quiver.symmetrifyStar u)

Tactic:
rw [Equiv.eq_symm_comp (e := Quiver.symmetrifyStar (φ.obj u))]

Goal state after:
U : Type u_1
inst✝¹ : Quiver U
V : Type u_2
inst✝ : Quiver V
φ : U ⥤q V
u : U
⊢ ⇑(Quiver.symmetrifyStar (φ.obj u)) ∘ φ.symmetrify.star u =
    Sum.map (φ.star u) (φ.costar u) ∘ ⇑(Quiver.symmetrifyStar u)
Module: Mathlib.Combinatorics.Quiver.Path.Vertices

Goal state before:
pp: V : Type u_1
inst✝ : Quiver V
a b : V
p : Path a b
h : p.vertices ≠ []
⊢ p.vertices.head h = a

Tactic:
induction p with

Goal state after: