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

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Mul α
s t u : Finset α
⊢ #u * ∑ c ∈ s * t, #({xy ∈ s ×ˢ t | xy.1 * xy.2 = c}) ^ 2 = #u * Eₘ[s, t]

Tactic:
by rw [mulEnergy_eq_sum_sq']

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

Goal state before:
pp: case refine_3
α : 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
hUVne : U ≠ V
hUV : ¬G.IsUniform ε U V
t : (star hP G ε hU V).product (star hP G ε hV U) ⊆ (chunk hP G ε hU).parts.product (chunk hP G ε hV).parts
hε : 0 ≤ ε
sp : ∀ (a b : Finset (Finset α)), a.product b = a ×ˢ b
this :
  ↑(G.edgeDensity U V) ^ 2 - ε ^ 5 / 25 +
      ↑(#((star hP G ε hU V).product (star hP G ε hV U))) /
          ↑(#((chunk hP G ε hU).parts.product (chunk hP G ε hV).parts)) *
        (3 / 4 * ε) ^ 2 ≤
    (∑ i ∈ (chunk hP G ε hU).parts.product (chunk hP G ε hV).parts, ↑(G.edgeDensity i.1 i.2) ^ 2) /
      ↑(#((chunk hP G ε hU).parts.product (chunk hP G ε hV).parts))
⊢ ↑(G.edgeDensity U V) ^ 2 - ε ^ 5 / 25 +
      ↑(#(star hP G ε hU V)) * ↑(#(star hP G ε hV U)) / 16 ^ #P.parts * (9 / 16) * ε ^ 2 ≤
    (∑ ab ∈ (chunk hP G ε hU).parts.product (chunk hP G ε hV).parts, ↑(G.edgeDensity ab.1 ab.2) ^ 2) / 16 ^ #P.parts

Tactic:
simp_rw [sp, card_product, card_chunk (m_pos hPα).ne', ← mul_pow, cast_pow, mul_pow,
          div_pow, ← mul_assoc] at this

Goal state after:
case refine_3
α : 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
hUVne : U ≠ V
hUV : ¬G.IsUniform ε U V
t : (star hP G ε hU V).product (star hP G ε hV U) ⊆ (chunk hP G ε hU).parts.product (chunk hP G ε hV).parts
hε : 0 ≤ ε
sp : ∀ (a b : Finset (Finset α)), a.product b = a ×ˢ b
this :
  ↑(G.edgeDensity U V) ^ 2 - ε ^ 5 / 25 +
      ↑(#(star hP G ε hU V) * #(star hP G ε hV U)) / ↑(4 * 4) ^ #P.parts * (3 ^ 2 / 4 ^ 2) * ε ^ 2 ≤
    (∑ x ∈ (chunk hP G ε hU).parts ×ˢ (chunk hP G ε hV).parts, ↑(G.edgeDensity x.1 x.2) ^ 2) / ↑(4 * 4) ^ #P.parts
⊢ ↑(G.edgeDensity U V) ^ 2 - ε ^ 5 / 25 +
      ↑(#(star hP G ε hU V)) * ↑(#(star hP G ε hV U)) / 16 ^ #P.parts * (9 / 16) * ε ^ 2 ≤
    (∑ ab ∈ (chunk hP G ε hU).parts.product (chunk hP G ε hV).parts, ↑(G.edgeDensity ab.1 ab.2) ^ 2) / 16 ^ #P.parts
Module: Mathlib.Combinatorics.Additive.Randomisation

Goal state before:
pp: G : Type u_1
inst✝¹ : Fintype G
inst✝ : AddCommGroup G
c : AddChar G ℂ → ℝ
d : AddChar G ℂ → ℂ
hcd : AddDissociated {ψ | d ψ ≠ 0}
t : Finset (AddChar G ℂ)
ht : t ≠ ∅
u : Finset (AddChar G ℂ)
x✝ : u ∈ t.powerset
⊢ ((∏ ψ ∈ u, d ψ) * ∏ ψ ∈ t \ u, (starRingEnd ℂ) (d ψ)) * 𝔼 a, (∑ ψ ∈ u, ψ - ∑ ψ ∈ t \ u, ψ) a = 0

Tactic:
mul_eq_zero,

Goal state after:
G : Type u_1
inst✝¹ : Fintype G
inst✝ : AddCommGroup G
c : AddChar G ℂ → ℝ
d : AddChar G ℂ → ℂ
hcd : AddDissociated {ψ | d ψ ≠ 0}
t : Finset (AddChar G ℂ)
ht : t ≠ ∅
u : Finset (AddChar G ℂ)
x✝ : u ∈ t.powerset
⊢ (∏ ψ ∈ u, d ψ) * ∏ ψ ∈ t \ u, (starRingEnd ℂ) (d ψ) = 0 ∨ 𝔼 a, (∑ ψ ∈ u, ψ - ∑ ψ ∈ t \ u, ψ) a = 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}

pp: case refine_2.refine_3
ι : 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
⊢ #univ < 2 * p

Tactic:
· rw [← CharP.cast_eq_zero_iff (ZMod p), ← Finset.sum_boole]
      simpa only [f₁, map_sum, ZMod.pow_card_sub_one, map_pow, eval_X] using x.2.1

Goal state after:
case refine_2.refine_3
ι : 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
⊢ #univ < 2 * p
Module: Mathlib.Data.Nat.BitIndices

Goal state before:
pp: case cons
a : ℕ
L₀ : List ℕ
hL₀ : L₀.SortedLT
hL✝ : (a :: map (fun x ↦ x + a + 1) L₀).SortedLT
hL : List.Pairwise (fun x1 x2 ↦ x1 < x2) (map (fun x ↦ x + a + 1) L₀)
haL : ∀ (a' : ℕ), a' ∈ map (fun x ↦ x + a + 1) L₀ → a + 1 ≤ a'
hrw : ((fun x ↦ 2 ^ x) ∘ fun x ↦ x + a + 1) = fun i ↦ 2 ^ a * (2 * 2 ^ i)
⊢ map (fun x ↦ x + a) (0 :: map (fun x ↦ x + 1) L₀) = a :: map (fun x ↦ x + a + 1) L₀

Tactic:
simp [add_comm (a := 1), add_assoc]

Goal state after:
Module: Mathlib.Combinatorics.Colex

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

Tactic:
rw [lt_iff_le_and_ne, toColex_le_singleton, ne_eq, toColex_inj]

Goal state after:
α : Type u_1
inst✝ : PartialOrder α
s : Finset α
a : α
⊢ (∀ b ∈ s, b ≤ a ∧ (a ∈ s → b = a)) ∧ ¬s = {a} ↔ ∀ b ∈ s, b < a
Module: Mathlib.Combinatorics.Digraph.Basic

Goal state before:
pp: V : Type u_1
adj adj' : V → V → Bool
⊢ (fun x ↦ { Adj := fun v w ↦ x v w = true }) adj = (fun x ↦ { Adj := fun v w ↦ x v w = true }) adj' → adj = adj'

Tactic:
simp_rw [mk.injEq]
    intro h
    funext v w
    simpa only [eq_iff_iff, Bool.coe_iff_coe] using congr($h v w)

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

Goal state before:
pp: V : Type u_1
inst✝¹ : DecidableEq V
inst✝ : Fintype V
⊢ Bijective ⇑Digraph.mk'

Tactic:
refine ⟨Embedding.injective _, ?_⟩

Goal state after:
V : Type u_1
inst✝¹ : DecidableEq V
inst✝ : Fintype V
⊢ Surjective ⇑Digraph.mk'
Module: Mathlib.Combinatorics.Enumerative.Bell

Goal state before:
pp: x : ℕ
hx : x ≠ 0
c : ℕ
⊢ (c + 1) * (c * x + x - 1).choose (x - 1) * (x * c)! * x ! = (x * (c + 1))!

Tactic:
by
        rw [← Nat.choose_mul_add hx, mul_comm c x, Nat.add_choose_mul_factorial_mul_factorial]
        ring_nf

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

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

Tactic:
rw [invMulSubgroup_eq_inv_mul]

Goal state after:
case refine_2
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A : Finset G
h : ↑(#(A * A)) < 3 / 2 * ↑(#A)
H : Subgroup G := A.invMulSubgroup h
a : G
ha : a ∈ A
⊢ ↑A ⊆ a •> (↑A⁻¹ * ↑A)
Module: Mathlib.Combinatorics.Enumerative.DyckWord

Goal state before:
pp: p : DyckWord
h : p ≠ 0
lp : 0 < (↑p).length
⊢ count U (List.take ((↑p).length - 1 + 1) ↑p) = count D (List.take ((↑p).length - 1 + 1) ↑p)

Tactic:
rw [Nat.sub_add_cancel lp, take_of_length_le (le_refl _),
    p.count_U_eq_count_D]

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

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

Tactic:
rw [succ_eq_add_one, mul_eq_mul_right_iff]

Goal state after:
n : ℕ
p : (n + 1).Partition
⊢ n + 1 = ∑ a ∈ p.parts.toFinset, count a p.parts * a ∨ p.parts.bell = 0
Module: Mathlib.Combinatorics.Enumerative.Bell

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

Tactic:
by grind [Finset.sum_mul]

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

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

Tactic:
have := semilength_outsidePart_lt h

Goal state after:
case neg
p q : DyckWord
h : ¬p = 0
this : p.outsidePart.semilength < p.semilength
⊢ q ≤ p + q
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
hgne0 : ∀ (i : ℕ), g i ≠ 0 ↔ i ≠ 0 ∧ i ≤ g i
⊢ ∀ (a : ℕ), a ∈ g.support ↔ g a / a ≠ 0

Tactic:
simpa using hgne0

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

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
K : ℝ
A S : Finset G
a : G
⊢ IsFragment K S (a •> A) ↔ IsFragment K S A

Tactic:
simp [IsFragment]

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
hK : K ≤ 1
hS : S.Nonempty
hA : IsAtom K S A
hB : IsAtom K S B
hAB : IsFragment K S (A ∩ B)
⊢ A = B

Tactic:
replace hA := hA.2 hAB <| by grw [inter_subset_left]

Goal state after:
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
K : ℝ
A B S : Finset G
hK : K ≤ 1
hS : S.Nonempty
hB : IsAtom K S B
hAB : IsFragment K S (A ∩ B)
hA : #A ≤ #(A ∩ B)
⊢ A = B
Module: Mathlib.Combinatorics.Enumerative.Stirling

Goal state before:
pp: n k : ℕ
hk : k ≠ 0
⊢ (n + 1).stirlingFirst k = n * n.stirlingFirst k + n.stirlingFirst (k - 1)

Tactic:
by
  obtain ⟨l, rfl⟩ := Nat.exists_eq_add_of_le' (Nat.pos_of_ne_zero hk)
  rfl

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

Goal state before:
pp: n k : ℕ
hk : k ≠ 0
⊢ (n + 1).stirlingSecond k = k * n.stirlingSecond k + n.stirlingSecond (k - 1)

Tactic:
by
  obtain ⟨l, rfl⟩ := Nat.exists_eq_add_of_le' (Nat.pos_of_ne_zero hk)
  rfl

Goal state after:
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)
K : ℝ := 1 - ε / 2
⊢ K < 1

Tactic:
unfold K

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
⊢ 1 - ε / 2 < 1
Module: Mathlib.Combinatorics.Extremal.RuzsaSzemeredi

Goal state before:
pp: n : ℕ
α : Type := Fin (2 * n + 1)
this✝ : Coprime 2 (2 * n + 1)
this : Fact (IsUnit 2)
⊢ ruzsaSzemerediNumber (α ⊕ α ⊕ α) = ruzsaSzemerediNumberNat (6 * n + 3)

Tactic:
by
      simp_rw [← ruzsaSzemerediNumberNat_card, Fintype.card_sum, α, Fintype.card_fin]
      ring_nf

Goal state after:
Module: Mathlib.Combinatorics.HalesJewett

Goal state before:
pp: α : Type u_2
ι : Type u_3
l : Line α ι
a : Unit → α
i : ι
⊢ ↑l.toSubspaceUnit a i = ↑l (a ()) i

Tactic:
cases h : l.idxFun i

Goal state after:
case none
α : Type u_2
ι : Type u_3
l : Line α ι
a : Unit → α
i : ι
h : l.idxFun i = none
⊢ ↑l.toSubspaceUnit a i = ↑l (a ()) i

case some
α : Type u_2
ι : Type u_3
l : Line α ι
a : Unit → α
i : ι
val✝ : α
h : l.idxFun i = some val✝
⊢ ↑l.toSubspaceUnit a i = ↑l (a ()) i
Module: Mathlib.Combinatorics.Hindman

Goal state before:
pp: case h.cons'.refine_2
M : Type u_1
inst✝ : Semigroup M
U : Ultrafilter M
U_idem : U * U = U
exists_elem : ∀ {s : Set M}, s ∈ U → (s ∩ {m | ∀ᶠ (m' : M) in ↑U, m * m' ∈ s}).Nonempty
elem : { s // s ∈ U } → M := fun p ↦ ⋯.some
succ : { s // s ∈ U } → { s // s ∈ U } := fun p ↦ ⟨↑p ∩ {m | elem p * m ∈ ↑p}, ⋯⟩
a : Stream' M
m n : M
p : { s // s ∈ U }
h : FP (Stream'.corec elem succ p).tail n
ih : ∀ (p_1 : { s // s ∈ U }), (Stream'.corec elem succ p).tail = Stream'.corec elem succ p_1 → n ∈ ↑p_1
this : n ∈ {m | elem p * m ∈ ↑p}
⊢ (Stream'.corec elem succ p).head * n ∈ ↑p

pp: case h.cons'.refine_1
M : Type u_1
inst✝ : Semigroup M
U : Ultrafilter M
U_idem : U * U = U
exists_elem : ∀ {s : Set M}, s ∈ U → (s ∩ {m | ∀ᶠ (m' : M) in ↑U, m * m' ∈ s}).Nonempty
elem : { s // s ∈ U } → M := fun p ↦ ⋯.some
succ : { s // s ∈ U } → { s // s ∈ U } := fun p ↦ ⟨↑p ∩ {m | elem p * m ∈ ↑p}, ⋯⟩
a : Stream' M
m n : M
p : { s // s ∈ U }
h : FP (Stream'.corec elem succ p).tail n
ih : ∀ (p_1 : { s // s ∈ U }), (Stream'.corec elem succ p).tail = Stream'.corec elem succ p_1 → n ∈ ↑p_1
⊢ (Stream'.corec elem succ p).tail = Stream'.corec elem succ (succ p)

Tactic:
· simpa only using! this

Goal state after:
case h.cons'.refine_1
M : Type u_1
inst✝ : Semigroup M
U : Ultrafilter M
U_idem : U * U = U
exists_elem : ∀ {s : Set M}, s ∈ U → (s ∩ {m | ∀ᶠ (m' : M) in ↑U, m * m' ∈ s}).Nonempty
elem : { s // s ∈ U } → M := fun p ↦ ⋯.some
succ : { s // s ∈ U } → { s // s ∈ U } := fun p ↦ ⟨↑p ∩ {m | elem p * m ∈ ↑p}, ⋯⟩
a : Stream' M
m n : M
p : { s // s ∈ U }
h : FP (Stream'.corec elem succ p).tail n
ih : ∀ (p_1 : { s // s ∈ U }), (Stream'.corec elem succ p).tail = Stream'.corec elem succ p_1 → n ∈ ↑p_1
⊢ (Stream'.corec elem succ p).tail = Stream'.corec elem succ (succ p)
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 1 (Stream'.drop n a)) ⊆ FP a

Tactic:
exact _root_.trans (FP.tail _) ih

Goal state after:
Module: Mathlib.Combinatorics.KatonaCircle

Goal state before:
pp: case pos
X : Type u_1
inst✝¹ : Fintype X
f : Numbering X
s✝ t : Finset X
inst✝ : DecidableEq X
s : Finset X
x✝ : Numbering ↥s × Numbering ↥sᶜ
g : Numbering ↥s
g' : Numbering ↥sᶜ
x : X
hx : x ∈ s
⊢ (fun n ↦ if hn : ↑n < #s then ↑((Equiv.symm g) ⟨↑n, ⋯⟩) else ↑((Equiv.symm g') ⟨↑n - #s, ⋯⟩))
      ((fun x ↦ if hx : x ∈ s then Fin.castLE ⋯ (g ⟨x, hx⟩) else Fin.cast ⋯ ((g' ⟨x, ⋯⟩).addNat #s)) x) =
    x

Tactic:
have : g ⟨x, hx⟩ < #s := by simpa using (g ⟨x, hx⟩).2

Goal state after:
case pos
X : Type u_1
inst✝¹ : Fintype X
f : Numbering X
s✝ t : Finset X
inst✝ : DecidableEq X
s : Finset X
x✝ : Numbering ↥s × Numbering ↥sᶜ
g : Numbering ↥s
g' : Numbering ↥sᶜ
x : X
hx : x ∈ s
this : ↑(g ⟨x, hx⟩) < #s
⊢ (fun n ↦ if hn : ↑n < #s then ↑((Equiv.symm g) ⟨↑n, ⋯⟩) else ↑((Equiv.symm g') ⟨↑n - #s, ⋯⟩))
      ((fun x ↦ if hx : x ∈ s then Fin.castLE ⋯ (g ⟨x, hx⟩) else Fin.cast ⋯ ((g' ⟨x, ⋯⟩).addNat #s)) x) =
    x
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
hb' : ∀ (i : ι), m.degree (b i) ≠ 0
hf0 : ¬f = 0
i : ι
hf : m.degree (b i) ≤ m.degree f
deg_reduce : m.toSyn (m.degree (m.reduce ⋯ f)) < m.toSyn (m.degree f)
g' : ι →₀ MvPolynomial σ R
r' : MvPolynomial σ R
H' :
  m.reduce ⋯ f = (Finsupp.linearCombination (MvPolynomial σ R) b) g' + r' ∧
    (∀ (i_1 : ι), m.toSyn (m.degree (b i_1 * g' i_1)) ≤ m.toSyn (m.degree (m.reduce ⋯ f))) ∧
      ∀ c ∈ r'.support, ∀ (i : ι), ¬m.degree (b i) ≤ c
⊢ f =
    (Finsupp.linearCombination (MvPolynomial σ R) b) g' +
      (r' +
        (Finsupp.linearCombination (MvPolynomial σ R) b)
          (Finsupp.single i ((monomial (m.degree f - m.degree (b i))) (↑⋯.unit⁻¹ * m.leadingCoeff f))))

Tactic:
← add_assoc,

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
hb' : ∀ (i : ι), m.degree (b i) ≠ 0
hf0 : ¬f = 0
i : ι
hf : m.degree (b i) ≤ m.degree f
deg_reduce : m.toSyn (m.degree (m.reduce ⋯ f)) < m.toSyn (m.degree f)
g' : ι →₀ MvPolynomial σ R
r' : MvPolynomial σ R
H' :
  m.reduce ⋯ f = (Finsupp.linearCombination (MvPolynomial σ R) b) g' + r' ∧
    (∀ (i_1 : ι), m.toSyn (m.degree (b i_1 * g' i_1)) ≤ m.toSyn (m.degree (m.reduce ⋯ f))) ∧
      ∀ c ∈ r'.support, ∀ (i : ι), ¬m.degree (b i) ≤ c
⊢ f =
    (Finsupp.linearCombination (MvPolynomial σ R) b) g' + r' +
      (Finsupp.linearCombination (MvPolynomial σ R) b)
        (Finsupp.single i ((monomial (m.degree f - m.degree (b i))) (↑⋯.unit⁻¹ * m.leadingCoeff f)))
Module: Mathlib.Combinatorics.Matroid.Minor.Contract

Goal state before:
pp: α : Type u_1
D C✝ : Set α
M : Matroid α
C : Set α
hCD : Disjoint C D
hCE : C ⊆ M.E
⊢ C ⊆ M.E \ D

Tactic:
simpa [hCE, subset_sdiff]

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
⊢ b ∈ p.vertices

Tactic:
have h₁ : p.vertices.getLast (vertices_ne_nil p) = b :=
    vertices_getLast p (vertices_ne_nil p)

Goal state after:
V : Type u_1
inst✝ : Quiver V
a b : V
p : Path a b
h₁ : p.vertices.getLast ⋯ = b
⊢ b ∈ p.vertices
Module: Mathlib.Combinatorics.Quiver.Path.Vertices

Goal state before:
pp: V : Type u_1
inst✝ : Quiver V
a b : V
p : Path a b
b✝ c : V
p' : Path a b✝
e : b✝ ⟶ c
ih : ∀ {n : ℕ}, n ≤ p'.length → ∃ v p₁ p₂, p' = p₁.comp p₂ ∧ p₁.length = n
n : ℕ
hn : n ≤ p'.length + 1
h : n ≤ p'.length
d : V
p₁ : Path a d
p₂ : Path d b✝
hp : p' = p₁.comp p₂
hl : p₁.length = n
⊢ p'.cons e = p₁.comp (p₂.cons e)

Tactic:
by simp [hp]

Goal state after:
Module: Mathlib.Combinatorics.Schnirelmann

Goal state before:
pp: case hab
A : Set ℕ
inst✝ : DecidablePred fun x ↦ x ∈ A
k : ℕ
hk : k ∉ A
hk' : k > 0
⊢ ↑(#({a ∈ Ioc 0 k | a ∈ A})) ≤ ↑k - 1

Tactic:
rw [← Nat.cast_pred hk', Nat.cast_le]

Goal state after:
case hab
A : Set ℕ
inst✝ : DecidablePred fun x ↦ x ∈ A
k : ℕ
hk : k ∉ A
hk' : k > 0
⊢ #({a ∈ Ioc 0 k | a ∈ A}) ≤ k - 1
Module: Mathlib.Combinatorics.SetFamily.Compression.Down

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
s : Finset α
a : α
hs : s ∈ 𝒜
⊢ s.erase a ∈ 𝒜 ∧ s.erase a ∈ 𝒜 ∨ s.erase a ∉ 𝒜 ∧ insert a (s.erase a) ∈ 𝒜

Tactic:
and_self_iff

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
s : Finset α
a : α
hs : s ∈ 𝒜
⊢ s.erase a ∈ 𝒜 ∨ s.erase a ∉ 𝒜 ∧ insert a (s.erase a) ∈ 𝒜
Module: Mathlib.Combinatorics.SetFamily.AhlswedeZhang

Goal state before:
pp: α : Type u_1
inst✝³ : DistribLattice α
inst✝² : DecidableEq α
s t : Finset α
a : α
inst✝¹ : DecidableLE α
inst✝ : BoundedOrder α
hs : a ∈ lowerClosure ↑s
ht : a ∈ lowerClosure ↑t
⊢ ((image (Function.uncurry fun x1 x2 ↦ x1 ⊓ x2) ({b ∈ s | a ≤ b} ×ˢ {b ∈ t | a ≤ b})).sup' ⋯ fun x ↦ id x) =
    ({b ∈ s | a ≤ b} ×ˢ {b ∈ t | a ≤ b}).sup' ⋯ fun i ↦ id i.1 ⊓ id i.2

Tactic:
rw [sup'_image]

Goal state after:
α : Type u_1
inst✝³ : DistribLattice α
inst✝² : DecidableEq α
s t : Finset α
a : α
inst✝¹ : DecidableLE α
inst✝ : BoundedOrder α
hs : a ∈ lowerClosure ↑s
ht : a ∈ lowerClosure ↑t
⊢ ({b ∈ s | a ≤ b} ×ˢ {b ∈ t | a ≤ b}).sup' ⋯ ((fun x ↦ id x) ∘ Function.uncurry fun x1 x2 ↦ x1 ⊓ x2) =
    ({b ∈ s | a ≤ b} ×ˢ {b ∈ t | a ≤ b}).sup' ⋯ fun i ↦ id i.1 ⊓ id i.2
Module: Mathlib.Combinatorics.SetFamily.Compression.UV

Goal state before:
pp: α : Type u_1
inst✝³ : GeneralizedBooleanAlgebra α
inst✝² : DecidableRel Disjoint
inst✝¹ : DecidableLE α
s : Finset α
u v : α
inst✝ : DecidableEq α
b : α
hb : b ∈ s
left✝ : compress u v b ∉ s
⊢ compress u v (compress u v b) ∉ s

Tactic:
by rwa [compress_idem]

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
t : Finset α
⊢ t ∈ ∂⁺ 𝒜 ↔ ∃ s ∈ 𝒜, s ⊆ t ∧ #t = #s + 1

Tactic:
by
  refine mem_upShadow_iff_exists_sdiff.trans <| exists_congr fun t ↦ and_congr_right fun _ ↦
    and_congr_right fun hst ↦ ?_
  rw [card_sdiff_of_subset hst, tsub_eq_iff_eq_add_of_le, add_comm]
  exact card_mono hst

Goal state after:
Module: Mathlib.Combinatorics.SetFamily.Compression.UV

Goal state before:
pp: case inl
α : Type u_1
inst✝³ : GeneralizedBooleanAlgebra α
inst✝² : DecidableRel Disjoint
inst✝¹ : DecidableLE α
s : Finset α
u v a : α
inst✝ : DecidableEq α
hva : v ≤ a
hvu : v = ⊥ → u = ⊥
ha : a ∈ s ∧ compress u v a ∈ s
⊢ a ∈ s

pp: case inr
α : Type u_1
inst✝³ : GeneralizedBooleanAlgebra α
inst✝² : DecidableRel Disjoint
inst✝¹ : DecidableLE α
s : Finset α
u v a : α
inst✝ : DecidableEq α
hva : v ≤ a
hvu : v = ⊥ → u = ⊥
left✝ : a ∉ s
b : α
hb : b ∈ s
h : compress u v b = a
⊢ a ∈ s

Tactic:
· exact ha.1

Goal state after:
case inr
α : Type u_1
inst✝³ : GeneralizedBooleanAlgebra α
inst✝² : DecidableRel Disjoint
inst✝¹ : DecidableLE α
s : Finset α
u v a : α
inst✝ : DecidableEq α
hva : v ≤ a
hvu : v = ⊥ → u = ⊥
left✝ : a ∉ s
b : α
hb : b ∈ s
h : compress u v b = a
⊢ a ∈ s
Module: Mathlib.Combinatorics.SetFamily.FourFunctions

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : DecidableEq α
inst✝ : CommSemiring β
𝒜 : Finset (Finset α)
a : α
f : Finset α → β
t : Finset α
ht : t ∈ 𝒜
ha : a ∉ t
hu : insert a t ∈ 𝒜
⊢ (f t + if insert a t ∈ 𝒜 then f (insert a t) else 0) = f t + f (insert a t)

Tactic:
if_pos hu

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

Goal state before:
pp: case mpr
α : Type u_1
inst✝¹ : LinearOrder α
s : Finset α
inst✝ : Fintype α
hs : s.Nonempty
t : Finset α
⊢ #(s.erase (s.min' hs)) = #t ∧ toColex t ≤ toColex (s.erase (s.min' hs)) →
    ∃ a ∉ t, #s = #(insert a t) ∧ toColex (insert a t) ≤ toColex s

Tactic:
simp_rw [le_iff_eq_or_lt, lt_iff_exists_filter_lt, mem_sdiff, filter_inj, and_assoc]

Goal state after:
case mpr
α : Type u_1
inst✝¹ : LinearOrder α
s : Finset α
inst✝ : Fintype α
hs : s.Nonempty
t : Finset α
⊢ #(s.erase (s.min' hs)) = #t ∧
      (toColex t = toColex (s.erase (s.min' hs)) ∨
        ∃ w ∈ s.erase (s.min' hs), w ∉ t ∧ ∀ ⦃a : α⦄, w < a → (a ∈ t ↔ a ∈ s.erase (s.min' hs))) →
    ∃ a ∉ t,
      #s = #(insert a t) ∧
        (toColex (insert a t) = toColex s ∨
          ∃ w ∈ s, w ∉ insert a t ∧ ∀ ⦃a_1 : α⦄, w < a_1 → (a_1 ∈ insert a t ↔ a_1 ∈ s))
Module: Mathlib.Combinatorics.SetFamily.LYM

Goal state before:
pp: α : Type u_2
inst✝ : Fintype α
𝒜 : Finset (Finset α)
h𝒜 : IsAntichain (fun x1 x2 ↦ x1 ⊆ x2) ↑𝒜
⊢ #𝒜 ≤ (Fintype.card α).choose (Fintype.card α / 2)

Tactic:
have : 0 < ((Fintype.card α).choose (Fintype.card α / 2) : ℚ≥0) :=
    Nat.cast_pos.2 <| choose_pos (Nat.div_le_self _ _)

Goal state after:
α : Type u_2
inst✝ : Fintype α
𝒜 : Finset (Finset α)
h𝒜 : IsAntichain (fun x1 x2 ↦ x1 ⊆ x2) ↑𝒜
this : 0 < ↑((Fintype.card α).choose (Fintype.card α / 2))
⊢ #𝒜 ≤ (Fintype.card α).choose (Fintype.card α / 2)
Module: Mathlib.Combinatorics.SetFamily.KruskalKatona

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
ℬ : Finset (Finset α)
r : ℕ
h₁ : Set.Sized r ↑ℬ
h₂ : ∀ (U V : Finset α), UsefulCompression U V → IsCompressed U V ℬ
A B : Finset α
hA : A ∈ ℬ
hBA : toColex B < toColex A
sizeA : #B = r
hB : B ∉ ℬ
hAB : A ≠ B
hAB' : #A = #B
hU : (A \ B).Nonempty
hV : (B \ A).Nonempty
disj : Disjoint (B \ A) (A \ B)
⊢ False

Tactic:
have smaller : max' _ hV < max' _ hU := by
    obtain hlt | heq | hgt := lt_trichotomy (max' _ hU) (max' _ hV)
    · rw [← compress_sdiff_sdiff A B] at hAB hBA
      cases hBA.not_gt <| toColex_compress_lt_toColex hlt hAB
    · exact (disjoint_right.1 disj (max'_mem _ hU) <| heq.symm ▸ max'_mem _ _).elim
    · assumption

Goal state after:
α : Type u_1
inst✝ : LinearOrder α
ℬ : Finset (Finset α)
r : ℕ
h₁ : Set.Sized r ↑ℬ
h₂ : ∀ (U V : Finset α), UsefulCompression U V → IsCompressed U V ℬ
A B : Finset α
hA : A ∈ ℬ
hBA : toColex B < toColex A
sizeA : #B = r
hB : B ∉ ℬ
hAB : A ≠ B
hAB' : #A = #B
hU : (A \ B).Nonempty
hV : (B \ A).Nonempty
disj : Disjoint (B \ A) (A \ B)
smaller : (B \ A).max' hV < (A \ B).max' hU
⊢ False