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

Goal state before:
pp: case composite.succ
m : ℕ
hm : 2 ≤ m
ihm : ∀ {ι : Type u_1} {s : Finset ι} (a : ι → ℤ), 2 * m - 1 ≤ #s → ∃ t ⊆ s, #t = m ∧ ↑m ∣ ∑ i ∈ t, a i
n : ℕ
hn : 2 ≤ n
ihn : ∀ {ι : Type u_1} {s : Finset ι} (a : ι → ℤ), 2 * n - 1 ≤ #s → ∃ t ⊆ s, #t = n ∧ ↑n ∣ ∑ i ∈ t, a i
ι : Type u_1
s : Finset ι
a : ι → ℤ
hs : 2 * (m * n) - 1 ≤ #s
k : ℕ
ih : k ≤ 2 * m - 1 → ∃ 𝒜, #𝒜 = k ∧ (↑𝒜).Pairwise Disjoint ∧ ∀ ⦃t : Finset ι⦄, t ∈ 𝒜 → t ⊆ s ∧ #t = n ∧ ↑n ∣ ∑ i ∈ t, a i
hk : k + 1 ≤ 2 * m - 1
⊢ ∃ 𝒜, #𝒜 = k + 1 ∧ (↑𝒜).Pairwise Disjoint ∧ ∀ ⦃t : Finset ι⦄, t ∈ 𝒜 → t ⊆ s ∧ #t = n ∧ ↑n ∣ ∑ i ∈ t, a i

Tactic:
obtain ⟨𝒜, h𝒜card, h𝒜disj, h𝒜⟩ := ih (Nat.le_of_succ_le hk)

Goal state after:
case composite.succ
m : ℕ
hm : 2 ≤ m
ihm : ∀ {ι : Type u_1} {s : Finset ι} (a : ι → ℤ), 2 * m - 1 ≤ #s → ∃ t ⊆ s, #t = m ∧ ↑m ∣ ∑ i ∈ t, a i
n : ℕ
hn : 2 ≤ n
ihn : ∀ {ι : Type u_1} {s : Finset ι} (a : ι → ℤ), 2 * n - 1 ≤ #s → ∃ t ⊆ s, #t = n ∧ ↑n ∣ ∑ i ∈ t, a i
ι : Type u_1
s : Finset ι
a : ι → ℤ
hs : 2 * (m * n) - 1 ≤ #s
k : ℕ
ih : k ≤ 2 * m - 1 → ∃ 𝒜, #𝒜 = k ∧ (↑𝒜).Pairwise Disjoint ∧ ∀ ⦃t : Finset ι⦄, t ∈ 𝒜 → t ⊆ s ∧ #t = n ∧ ↑n ∣ ∑ i ∈ t, a i
hk : k + 1 ≤ 2 * m - 1
𝒜 : Finset (Finset ι)
h𝒜card : #𝒜 = k
h𝒜disj : (↑𝒜).Pairwise Disjoint
h𝒜 : ∀ ⦃t : Finset ι⦄, t ∈ 𝒜 → t ⊆ s ∧ #t = n ∧ ↑n ∣ ∑ i ∈ t, a i
⊢ ∃ 𝒜, #𝒜 = k + 1 ∧ (↑𝒜).Pairwise Disjoint ∧ ∀ ⦃t : Finset ι⦄, t ∈ 𝒜 → t ⊆ s ∧ #t = n ∧ ↑n ∣ ∑ i ∈ t, a i
Module: Mathlib.LinearAlgebra.CrossProduct

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
u v w : Fin 3 → R
i : Fin (Nat.succ 0).succ.succ
⊢ ![![u 1 * v 2 - u 2 * v 1, u 2 * v 0 - u 0 * v 2, u 0 * v 1 - u 1 * v 0] 1 * w 2 -
          ![u 1 * v 2 - u 2 * v 1, u 2 * v 0 - u 0 * v 2, u 0 * v 1 - u 1 * v 0] 2 * w 1,
        ![u 1 * v 2 - u 2 * v 1, u 2 * v 0 - u 0 * v 2, u 0 * v 1 - u 1 * v 0] 2 * w 0 -
          ![u 1 * v 2 - u 2 * v 1, u 2 * v 0 - u 0 * v 2, u 0 * v 1 - u 1 * v 0] 0 * w 2,
        ![u 1 * v 2 - u 2 * v 1, u 2 * v 0 - u 0 * v 2, u 0 * v 1 - u 1 * v 0] 0 * w 1 -
          ![u 1 * v 2 - u 2 * v 1, u 2 * v 0 - u 0 * v 2, u 0 * v 1 - u 1 * v 0] 1 * w 0]
      i =
    ((u 0 * w 0 + u 1 * w 1 + u 2 * w 2) • v - (v 0 * w 0 + v 1 * w 1 + v 2 * w 2) • u) i

Tactic:
fin_cases i <;>
  · simp only [Fin.isValue, Nat.succ_eq_add_one, Nat.reduceAdd, Fin.reduceFinMk, cons_val,
      Pi.sub_apply, Pi.smul_apply, smul_eq_mul]
    ring

Goal state after:
Module: Mathlib.Combinatorics.Configuration

Goal state before:
pp: P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : HasLines P L
inst✝¹ : Fintype P
inst✝ : Fintype L
hPL : Fintype.card P = Fintype.card L
p : P
l : L
hpl : p ∉ l
⊢ lineCount L p = pointCount P l

Tactic:
obtain ⟨f, hf1, hf2⟩ := HasLines.exists_bijective_of_card_eq hPL

Goal state after:
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : HasLines P L
inst✝¹ : Fintype P
inst✝ : Fintype L
hPL : Fintype.card P = Fintype.card L
p : P
l : L
hpl : p ∉ l
f : L → P
hf1 : Function.Bijective f
hf2 : ∀ (l : L), pointCount P l = lineCount L (f l)
⊢ lineCount L p = pointCount P l
Module: Mathlib.Combinatorics.Derangements.Exponential

Goal state before:
pp: s : ℕ → ℝ := fun n ↦ ∑ k ∈ Finset.range n, (-1) ^ k / ↑k.factorial
n k : ℕ
hk : k ∈ Finset.range (n + 1)
h_le : k ≤ n
⊢ (-1) ^ k * ↑(n.factorial / k.factorial) / ↑n.factorial = (-1) ^ k / ↑k.factorial

Tactic:
push_cast [Nat.factorial_dvd_factorial h_le]

Goal state after:
s : ℕ → ℝ := fun n ↦ ∑ k ∈ Finset.range n, (-1) ^ k / ↑k.factorial
n k : ℕ
hk : k ∈ Finset.range (n + 1)
h_le : k ≤ n
⊢ (-1) ^ k * (↑n.factorial / ↑k.factorial) / ↑n.factorial = (-1) ^ k / ↑k.factorial
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 * A) < 2 * #A

Tactic:
← Nat.cast_lt (α := ℚ),

Goal state after:
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A : Finset G
h : ↑(#(A * A)) < 3 / 2 * ↑(#A)
⊢ ↑(#(A * A)) < ↑(2 * #A)
Module: Mathlib.Combinatorics.Enumerative.Catalan.Basic

Goal state before:
pp: n : ℕ
⊢ ∑ i, catalan ↑i * catalan (n - ↑i) = ∑ k ∈ range n.succ, catalan k * catalan (n - k)

Tactic:
sum_range

Goal state after:
n : ℕ
⊢ ∑ i, catalan ↑i * catalan (n - ↑i) = ∑ i, catalan ↑i * catalan (n - ↑i)
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}))
h₂ :
  ∀ x ∈ A ×ˢ A,
    (fun x ↦
          match x with
          | (x, y) => x * y⁻¹)
        x ∈
      A⁻¹ * A
⊢ 1 / 2 * ↑(#A) * ↑(#(A⁻¹ * A)) <
    ∑ x ∈ A⁻¹ * A,
      ↑(#({a ∈ A ×ˢ A |
            (match a with
              | (x, y) => x * y⁻¹) =
              x}))

Tactic:
refine (sum_lt_sum_of_nonempty (by simp [h₀]) h₁).trans_eq' ?_

Goal state after:
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}))
h₂ :
  ∀ x ∈ A ×ˢ A,
    (fun x ↦
          match x with
          | (x, y) => x * y⁻¹)
        x ∈
      A⁻¹ * A
⊢ ∑ i ∈ A⁻¹ * A, 1 / 2 * ↑(#A) = 1 / 2 * ↑(#A) * ↑(#(A⁻¹ * A))
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}))
h₂ :
  ∀ x ∈ A ×ˢ A,
    (fun x ↦
          match x with
          | (x, y) => x * y⁻¹)
        x ∈
      A⁻¹ * A
this : 1 / 2 * ↑(#A) * ↑(#(A⁻¹ * A)) < ↑(#A) ^ 2
⊢ #(A⁻¹ * A) < 2 * #A

Tactic:
← Nat.cast_lt (α := ℚ),

Goal state after:
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}))
h₂ :
  ∀ x ∈ A ×ˢ A,
    (fun x ↦
          match x with
          | (x, y) => x * y⁻¹)
        x ∈
      A⁻¹ * A
this : 1 / 2 * ↑(#A) * ↑(#(A⁻¹ * A)) < ↑(#A) ^ 2
⊢ ↑(#(A⁻¹ * A)) < ↑(2 * #A)
Module: Mathlib.Combinatorics.Enumerative.DyckWord

Goal state before:
pp: p q : DyckWord
⊢ ∀ (i : ℕ), count D (take i (↑p ++ ↑q)) ≤ count U (take i (↑p ++ ↑q))

Tactic:
simp only [take_append, count_append]

Goal state after:
p q : DyckWord
⊢ ∀ (i : ℕ),
    count D (take i ↑p) + count D (take (i - (↑p).length) ↑q) ≤
      count U (take i ↑p) + count U (take (i - (↑p).length) ↑q)
Module: Mathlib.Combinatorics.Additive.VerySmallDoubling

Goal state before:
pp: case refine_1
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A : Finset G
a : G
h : ↑(#(A * A)) < 3 / 2 * ↑(#A)
ha : a ∈ A
⊢ a •> (A⁻¹ * A) ⊆ (A⁻¹ * A) <• a

Tactic:
rw [subset_smul_finset_iff, ← op_inv]
    calc
      a •> (A⁻¹ * A) <• a⁻¹ ⊆ a •> (A⁻¹ * A) * A⁻¹ := op_smul_finset_subset_mul (by simpa)
      _ ⊆ A * (A⁻¹ * A) * A⁻¹ := by grw [smul_finset_subset_mul (by simpa)]
      _ = A⁻¹ * A := by
        simp_rw [← coe_inj, coe_mul]
        rw [← mul_assoc, ← invMulSubgroup_eq_mul_inv _ h, mul_assoc,
          ← invMulSubgroup_eq_mul_inv _ h, coe_mul_coe, invMulSubgroup_eq_inv_mul]

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

Goal state before:
pp: p q : DyckWord
h : p ≠ 0
i : ℕ
⊢ count D (List.take i ([U] ++ ↑p ++ [D])) ≤ count U (List.take i ([U] ++ ↑p ++ [D]))

Tactic:
simp only [take_append, count_append]

Goal state after:
p q : DyckWord
h : p ≠ 0
i : ℕ
⊢ count D (List.take i [U]) + count D (List.take (i - [U].length) ↑p) +
      count D (List.take (i - ([U] ++ ↑p).length) [D]) ≤
    count U (List.take i [U]) + count U (List.take (i - [U].length) ↑p) +
      count U (List.take (i - ([U] ++ ↑p).length) [D])
Module: Mathlib.Combinatorics.Enumerative.Bell

Goal state before:
pp: ⊢ Nat.bell 2 = 2

Tactic:
have : Finset.Iic 1 = {0, 1} := Finset.eq_of_veq rfl

Goal state after:
this : Finset.Iic 1 = {0, 1}
⊢ Nat.bell 2 = 2
Module: Mathlib.Combinatorics.Enumerative.Partition.GenFun

Goal state before:
pp: case pos
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
x : ℕ
hx : x ∈ s
hprod : ¬x ∣ g x
hx0 : x ≠ 0
⊢ (coeff (g x)) 1 + (coeff (g x)) (∑' (j : ℕ), f x (j + 1) • X ^ (x * (j + 1))) = 0

Tactic:
(summable_genFun_term' f hx0).map_tsum _ (WithPiTopology.continuous_coeff _ _)

Goal state after:
case pos
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
x : ℕ
hx : x ∈ s
hprod : ¬x ∣ g x
hx0 : x ≠ 0
⊢ (coeff (g x)) 1 + ∑' (i : ℕ), (coeff (g x)) (f x (i + 1) • X ^ (x * (i + 1))) = 0
Module: Mathlib.Combinatorics.Enumerative.IncidenceAlgebra

Goal state before:
pp: 𝕜 : Type u_2
α : Type u_5
inst✝⁴ : Ring 𝕜
inst✝³ : PartialOrder α
inst✝² : OrderTop α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
f g : α → 𝕜
h : ∀ (x : α), g x = ∑ y ≥ x, f y
x : α
this : DecidableLE α := Classical.decRel LE.le
⊢ ∑ y ≥ x, (mu 𝕜) x y * ∑ z ≥ y, f z = ∑ y ≥ x, (mu 𝕜) x y * ∑ z ≥ y, (zeta 𝕜) y z * f z

Tactic:
congr with y

Goal state after:
case e_f
𝕜 : Type u_2
α : Type u_5
inst✝⁴ : Ring 𝕜
inst✝³ : PartialOrder α
inst✝² : OrderTop α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
f g : α → 𝕜
h : ∀ (x : α), g x = ∑ y ≥ x, f y
x : α
this : DecidableLE α := Classical.decRel LE.le
y : α
⊢ (mu 𝕜) x y * ∑ z ≥ y, f z = (mu 𝕜) x y * ∑ z ≥ y, (zeta 𝕜) y z * f z
Module: Mathlib.Combinatorics.Enumerative.Partition.GenFun

Goal state before:
pp: case refine_1
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
i : ℕ
h : g i ≠ 0
⊢ i ≠ 0

Tactic:
contrapose hs0 with rfl

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

Goal state before:
pp: 𝕜 : Type u_2
α : Type u_5
inst✝⁴ : Ring 𝕜
inst✝³ : PartialOrder α
inst✝² : OrderTop α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
f g : α → 𝕜
h : ∀ (x : α), g x = ∑ y ≥ x, f y
x : α
this : DecidableLE α := ⋯
⊢ ∑ y ≥ x, (mu 𝕜) x y * g y = f x

Tactic:
calc
    ∑ y ∈ Ici x, mu 𝕜 x y * g y = ∑ y ∈ Ici x, mu 𝕜 x y * ∑ z ∈ Ici y, f z := by simp_rw [h]
    _ = ∑ y ∈ Ici x, mu 𝕜 x y * ∑ z ∈ Ici y, zeta 𝕜 y z * f z := by
      congr with y
      rw [sum_congr rfl fun z hz ↦ ?_]
      rw [zeta_apply, if_pos (mem_Ici.mp ‹_›), one_mul]
    _ = ∑ y ∈ Ici x, ∑ z ∈ Ici y, mu 𝕜 x y * zeta 𝕜 y z * f z := by simp [mul_sum]
    _ = ∑ z ∈ Ici x, ∑ y ∈ Icc x z, mu 𝕜 x y * zeta 𝕜 y z * f z := by
      rw [sum_sigma' (Ici x) fun y ↦ Ici y]
      rw [sum_sigma' (Ici x) fun z ↦ Icc x z]
      simp only [mul_boole, zero_mul, ite_mul, zeta_apply]
      apply sum_nbij' (fun ⟨a, b⟩ ↦ ⟨b, a⟩) (fun ⟨a, b⟩ ↦ ⟨b, a⟩) <;>
        aesop (add simp mul_assoc) (add unsafe le_trans)
    _ = ∑ z ∈ Ici x, (mu 𝕜 * zeta 𝕜 : IncidenceAlgebra 𝕜 α) x z * f z := by
      simp_rw [mul_apply, sum_mul]
    _ = ∑ y ∈ Ici x, ∑ z ∈ Ici y, (1 : IncidenceAlgebra 𝕜 α) x z * f z := by
      simp only [mu_mul_zeta 𝕜, one_apply, ite_mul, one_mul, zero_mul, sum_ite_eq, mem_Ici, le_refl,
        ↓reduceIte, ← add_sum_Ioi_eq_sum_Ici, left_eq_add]
      exact sum_eq_zero fun y hy ↦ if_neg (mem_Ioi.mp hy).not_ge
    _ = f x := by
      simp only [one_apply, ite_mul, one_mul, zero_mul, sum_ite_eq, mem_Ici,
        ← add_sum_Ioi_eq_sum_Ici, le_refl, ↓reduceIte, add_eq_left]
      exact sum_eq_zero fun y hy ↦ if_neg (mem_Ioi.mp hy).not_ge

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✝² : Ring 𝕜
inst✝¹ : Preorder α
inst✝ : Preorder β
f f₁ f₂ : IncidenceAlgebra 𝕜 α
g g₁ g₂ : IncidenceAlgebra 𝕜 β
x y : α × β
hxy : ¬x ≤ y
⊢ f x.1 y.1 * g x.2 y.2 = 0

Tactic:
rw [Prod.le_def, not_and_or] at hxy

Goal state after:
F : Type u_1
𝕜 : Type u_2
𝕝 : Type u_3
𝕞 : Type u_4
α : Type u_5
β : Type u_6
inst✝² : Ring 𝕜
inst✝¹ : Preorder α
inst✝ : Preorder β
f f₁ f₂ : IncidenceAlgebra 𝕜 α
g g₁ g₂ : IncidenceAlgebra 𝕜 β
x y : α × β
hxy : ¬x.1 ≤ y.1 ∨ ¬x.2 ≤ y.2
⊢ f x.1 y.1 * g x.2 y.2 = 0
Module: Mathlib.Combinatorics.Enumerative.Partition.Glaisher

Goal state before:
pp: R : Type u_1
inst✝² : TopologicalSpace R
inst✝¹ : T2Space R
inst✝ : CommSemiring R
m : ℕ
hm : 0 < m
a✝ : Nontrivial R
i : ℕ
⊢ ∑ k ∈ range (m - 1), (if k + 1 < m then 1 else 0) • X ^ ((i + 1) * (k + 1)) =
    ∑' (j : ℕ), (if j + 1 < m then 1 else 0) • X ^ ((i + 1) * (j + 1))

Tactic:
· exact (tsum_eq_sum (fun b hb ↦ smul_eq_zero_of_left (by simpa using hb) _)).symm

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

Goal state before:
pp: case refine_3
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)
⊢ Tendsto (fun x_1 ↦ ∏ i ∈ Finset.range x_1, (1 - x ^ (k + i + 2))) atTop (𝓝 (∏' (i : ℕ), (1 - x ^ (k + i + 2))))

Tactic:
apply Multipliable.tendsto_prod_tprod_nat

Goal state after:
case refine_3
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)
⊢ Multipliable fun i ↦ 1 - x ^ (k + i + 2)
Module: Mathlib.Combinatorics.Extremal.RuzsaSzemeredi

Goal state before:

Tactic:
_ ≤ (↑(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]

Goal state after:
case calc_1
n : ℕ
⊢ ↑(n + 3) / 3 - 2 ≤ ↑(2 * (n / 6) + 1)

case calc_2
n : ℕ
⊢ ↑(2 * (n / 6) + 1) * ↑(rothNumberNat (n / 6)) ≤ ↑(ruzsaSzemerediNumberNat (6 * (n / 6) + 3))
Module: Mathlib.Combinatorics.Graph.Subgraph

Goal state before:
pp: α : Type u_1
β : Type u_2
G H K : Graph α β
h' : K ≤ G
hsu : V(K) ⊆ V(H)
h : H ≤i G
e : β
he : e ∈ E(K)
u v : α
huv : K.IsLink e u v
⊢ e ∈ E(H)

Tactic:
exact h.2 (huv.mono h') (hsu huv.left_mem) (hsu huv.right_mem) |>.edge_mem

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

Goal state before:
pp: α : Type u_1
β : Type u_2
x y z : α
e : β
G : Graph α β
hy : G.Inc e y
hz : G.Inc e z
hxy : x ≠ y
hxz : x ≠ z
hyz : y ≠ z
hx' : G.IsLink e x y
⊢ False

Tactic:
obtain rfl := hz.eq_of_isLink_of_ne_left hx' hxz.symm

Goal state after:
α : Type u_1
β : Type u_2
x z : α
e : β
G : Graph α β
hz : G.Inc e z
hxz : x ≠ z
hy : G.Inc e z
hxy : x ≠ z
hyz : z ≠ z
hx' : G.IsLink e x z
⊢ False
Module: Mathlib.Combinatorics.Graph.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
x y z u v w : α
e f : β
G✝ H G : Graph α β
E : Set β
hE : ∀ (e : β), e ∈ E ↔ ∃ x y, G.IsLink e x y
⊢ E = E(G)

Tactic:
simp [Set.ext_iff, hE, G.edge_mem_iff_exists_isLink]

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

Goal state before:
pp: α : Type u_1
β : Type u_2
G : Graph α β
E : Set β
hE : ∀ (e : β), e ∈ E ↔ ∃ x y, G.IsLink e x y
⊢ E = E(G)

Tactic:
simp [Set.ext_iff, hE, G.edge_mem_iff_exists_isLink]

Goal state after:
Module: Mathlib.Combinatorics.HalesJewett

Goal state before:
pp: case refine_1.none
α : Type u_2
ι : Type u_3
inst✝ : Nontrivial α
l m : Line α ι
i : ι
a b : α
hba : b ≠ a
hlm : ∀ (x : α) (x_1 : ι), ↑l x x_1 = ↑m x x_1
h : l.idxFun i = some a
hi : m.idxFun i = none
⊢ none = some a

Tactic:
simpa [@eq_comm _ a, hi, h, hba] using hlm b i

Goal state after:
Module: Mathlib.Combinatorics.HalesJewett

Goal state before:
pp: case refine_1.some
α : Type u_2
ι : Type u_3
inst✝ : Nontrivial α
l m : Line α ι
i : ι
a b : α
hba : b ≠ a
hlm : ∀ (x : α) (x_1 : ι), ↑l x x_1 = ↑m x x_1
h : l.idxFun i = some a
val✝ : α
hi : m.idxFun i = some val✝
⊢ some val✝ = some a

Tactic:
simpa [@eq_comm _ a, hi, h, hba] using hlm b i

Goal state after:
Module: Mathlib.Combinatorics.HalesJewett

Goal state before:
pp: case refine_2.none
α : Type u_2
ι : Type u_3
inst✝ : Nontrivial α
l m : Line α ι
i : ι
a b : α
hba : b ≠ a
hlm : ∀ (x : α) (x_1 : ι), ↑l x x_1 = ↑m x x_1
h : m.idxFun i = some a
hi : l.idxFun i = none
⊢ none = some a

Tactic:
simpa [@eq_comm _ a, hi, h, hba] using hlm b i

Goal state after:
Module: Mathlib.Combinatorics.HalesJewett

Goal state before:
pp: case refine_2.some
α : Type u_2
ι : Type u_3
inst✝ : Nontrivial α
l m : Line α ι
i : ι
a b : α
hba : b ≠ a
hlm : ∀ (x : α) (x_1 : ι), ↑l x x_1 = ↑m x x_1
h : m.idxFun i = some a
val✝ : α
hi : l.idxFun i = some val✝
⊢ some val✝ = some a

Tactic:
simpa [@eq_comm _ a, hi, h, hba] using hlm b i

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

Goal state before:
pp: α : Type u_1
M : Matroid α
X D : Set α
hD : D ⊆ M.E
h : M ＼ D ≤r M
hX : Disjoint X (M ＼ D).E
⊢ M ＼ D = M ＼ (D ∪ X)

Tactic:
← delete_delete,

Goal state after:
α : Type u_1
M : Matroid α
X D : Set α
hD : D ⊆ M.E
h : M ＼ D ≤r M
hX : Disjoint X (M ＼ D).E
⊢ M ＼ D = M ＼ D ＼ X
Module: Mathlib.Combinatorics.Matroid.Minor.Contract

Goal state before:
pp: α : Type u_1
M : Matroid α
I X : Set α
hI : M.IsBasis I X
⊢ M✶ ＼ (I ∪ X \ I) = M✶ ＼ I ／ (X \ I)

Tactic:
← delete_delete,

Goal state after:
α : Type u_1
M : Matroid α
I X : Set α
hI : M.IsBasis I X
⊢ M✶ ＼ I ＼ (X \ I) = M✶ ＼ I ／ (X \ I)
Module: Mathlib.RingTheory.MvPolynomial.Groebner

Goal state before:
pp: case h.left
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
ι : Type u_3
b : ι → MvPolynomial σ R
hb : ∀ (i : ι), IsUnit (m.leadingCoeff (b i))
f : MvPolynomial σ R
i : ι
hb0 : m.degree (b i) = 0
⊢ m.leadingCoeff (b i) • f = f * b i

Tactic:
eq_C_of_degree_eq_zero hb0

Goal state after:
case h.left
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
ι : Type u_3
b : ι → MvPolynomial σ R
hb : ∀ (i : ι), IsUnit (m.leadingCoeff (b i))
f : MvPolynomial σ R
i : ι
hb0 : m.degree (b i) = 0
⊢ m.leadingCoeff (b i) • f = f * C (m.leadingCoeff (b i))
Module: Mathlib.Combinatorics.Matroid.Minor.Contract

Goal state before:
pp: α : Type u_1
M : Matroid α
X C : Set α
hC : C ⊆ M.E
⊢ (M ／ C).Spanning X ↔ M.Spanning (X ∪ C) ∧ Disjoint X C

Tactic:
rw [spanning_iff, contract_closure_eq, contract_ground, spanning_iff, union_subset_iff,
    subset_sdiff, ← and_assoc, and_congr_left_iff, and_comm (a := X ⊆ _), ← and_assoc,
    and_congr_left_iff]

Goal state after:
α : Type u_1
M : Matroid α
X C : Set α
hC : C ⊆ M.E
⊢ Disjoint X C → X ⊆ M.E → (M.closure (X ∪ C) \ C = M.E \ C ↔ M.closure (X ∪ C) = M.E ∧ C ⊆ M.E)
Module: Mathlib.Combinatorics.Matroid.Minor.Contract

Goal state before:
pp: α : Type u_1
M : Matroid α
K C : Set α
hK : M.IsCircuit K
hCK : Disjoint C K
I : Set α
hI : M.IsBasis I (C ∩ M.E)
⊢ ¬M.Indep (K ∪ I) ∧ K ⊆ M.E

Tactic:
and_iff_left hK.subset_ground

Goal state after:
α : Type u_1
M : Matroid α
K C : Set α
hK : M.IsCircuit K
hCK : Disjoint C K
I : Set α
hI : M.IsBasis I (C ∩ M.E)
⊢ ¬M.Indep (K ∪ I)
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
⊢ ∀ {a b : V} (a_1 : Path a b), height a ≤ height b

Tactic:
intro a b p

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

Goal state before:
pp: case mpr
V : Type u_2
inst✝ : Quiver V
v : V
h_no_bidir : ∀ (w : V), w ≠ v → ¬(Nonempty (Path v w) ∧ Nonempty (Path w v))
w : V
h_same_scc : StronglyConnectedComponent.mk w = StronglyConnectedComponent.mk v
hw_ne : ¬w = v
⊢ False

Tactic:
obtain ⟨hab, hba⟩ :=
      exists_path_of_stronglyConnectedComponent_eq (a := w) (b := v) h_same_scc

Goal state after:
case mpr
V : Type u_2
inst✝ : Quiver V
v : V
h_no_bidir : ∀ (w : V), w ≠ v → ¬(Nonempty (Path v w) ∧ Nonempty (Path w v))
w : V
h_same_scc : StronglyConnectedComponent.mk w = StronglyConnectedComponent.mk v
hw_ne : ¬w = v
hab : Nonempty (Path w v)
hba : Nonempty (Path v w)
⊢ False
Module: Mathlib.Combinatorics.Quiver.Path.Vertices

Goal state before:
pp: case neg
V : Type u_1
inst✝ : Quiver V
a b : V
p : Path a b
v b✝ c✝ : V
pPrev : Path a b✝
e : b✝ ⟶ c✝
ih : v ∈ pPrev.vertices → ∃ p₁ p₂, pPrev = p₁.comp p₂ ∧ ¬v ∈ p₂.vertices.tail
hv : v ∈ (pPrev.cons e).vertices
h_case₁ : v = (pPrev.cons e).end → ∃ p₁ p₂, pPrev.cons e = p₁.comp p₂ ∧ ¬v ∈ p₂.vertices.tail
h_case₂ : v ∈ pPrev.vertices → v ≠ (pPrev.cons e).end → ∃ p₁ p₂, pPrev.cons e = p₁.comp p₂ ∧ ¬v ∈ p₂.vertices.tail
h_in_prefix : v ∈ pPrev.vertices
h_eq_end : ¬v = (pPrev.cons e).end
⊢ ∃ p₁ p₂, pPrev.cons e = p₁.comp p₂ ∧ ¬v ∈ p₂.vertices.tail

Tactic:
exact h_case₂ h_in_prefix h_eq_end

Goal state after:
Module: Mathlib.Combinatorics.Schnirelmann

Goal state before:
pp: m : ℕ
hm : m ≠ 1
hm' : m > 0
n : ℕ
hn : 0 < n
this : image (fun x ↦ x * m + 1) (Icc 0 ((n - 1) / m)) ⊆ {x ∈ Ioc 0 n | x % m = 1}
⊢ ↑n / ↑m ≤ ↑(#(image (fun x ↦ x * m + 1) (Icc 0 ((n - 1) / m))))

Tactic:
card_image_of_injective,

Goal state after:
m : ℕ
hm : m ≠ 1
hm' : m > 0
n : ℕ
hn : 0 < n
this : image (fun x ↦ x * m + 1) (Icc 0 ((n - 1) / m)) ⊆ {x ∈ Ioc 0 n | x % m = 1}
⊢ ↑n / ↑m ≤ ↑(#(Icc 0 ((n - 1) / m)))

case H
m : ℕ
hm : m ≠ 1
hm' : m > 0
n : ℕ
hn : 0 < n
this : image (fun x ↦ x * m + 1) (Icc 0 ((n - 1) / m)) ⊆ {x ∈ Ioc 0 n | x % m = 1}
⊢ Function.Injective fun x ↦ x * m + 1
Module: Mathlib.Combinatorics.SetFamily.Shadow

Goal state before:
pp: case succ.mp
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
k : ℕ
ih : ∀ {t : Finset α}, t ∈ ∂⁺ ^[k] 𝒜 ↔ ∃ u, #u = k ∧ u ⊆ t ∧ t \ u ∈ 𝒜
t : Finset α
⊢ (∃ a ∈ t, ∃ u, #u = k ∧ (u ⊆ t ∧ a ∉ u) ∧ t \ insert a u ∈ 𝒜) →
    ∃ u, (∃ a t, a ∉ t ∧ insert a t = u ∧ #t = k) ∧ u ⊆ t ∧ t \ u ∈ 𝒜

Tactic:
rintro ⟨a, hat, u, rfl, ⟨hut, hau⟩, htu⟩
      exact ⟨_, ⟨_, _, hau, rfl, rfl⟩, insert_subset hat hut, htu⟩

Goal state after:
Module: Mathlib.Combinatorics.SetFamily.Shadow

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
t u : Finset α
hut : u ⊆ t
htu : t \ u ∈ 𝒜
⊢ #(t \ (t \ u)) = #u

Tactic:
sdiff_sdiff_eq_self hut

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
t u : Finset α
hut : u ⊆ t
htu : t \ u ∈ 𝒜
⊢ #u = #u