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

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

Tactic:
simp only [mem_mul, mem_inv'] at ha hc

Goal state after:
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
K : ℝ
A✝ B S : Finset G
a✝ b c✝ d x y : G
A : Finset G
h : ↑(#(A * A)) < 3 / 2 * ↑(#A)
h₁ : ∀ x ∈ A, ∀ y ∈ A, 1 / 2 * ↑(#A) < ↑(#(x •> A ∩ y •> A))
a c : G
ha : ∃ y, y⁻¹ ∈ A ∧ ∃ z ∈ A, y * z = a
hc : ∃ y, y⁻¹ ∈ A ∧ ∃ z ∈ A, y * z = c
⊢ a * c ∈ A⁻¹ * A
Module: Mathlib.Combinatorics.Enumerative.Catalan.Tree

Goal state before:
pp: case hi
n : ℕ
ih : ∀ m ≤ n, #(treesOfNumNodesEq m) = catalan m
i j : ℕ
H : (i, j) ∈ antidiagonal n
⊢ #(pairwiseNode (treesOfNumNodesEq (i, j).1) (treesOfNumNodesEq (i, j).2)) = catalan (i, j).1 * catalan (i, j).2

Tactic:
rw [card_map, card_product, ih _ (fst_le H), ih _ (snd_le H)]

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✝⁵ : PartialOrder α
inst✝⁴ : LocallyFiniteOrder α
inst✝³ : DecidableEq α
inst✝² : CommSemiring 𝕜
inst✝¹ : CommSemiring 𝕝
inst✝ : Algebra 𝕜 𝕝
⊢ (algebraMap 𝕜 𝕝) 0 • 1 = 0

Tactic:
by rw [map_zero, zero_smul]

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

Goal state before:
pp: 𝕜 : Type u_2
α : Type u_5
inst✝⁴ : AddCommGroup 𝕜
inst✝³ : One 𝕜
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b : α
hab : a ≠ b
⊢ (mu 𝕜) a b = -∑ x ∈ Ico a b, (mu 𝕜) a x

Tactic:
rw [mu_apply, if_neg hab]

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

Goal state before:
pp: case a
n✝ n : ℕ
ih : ∀ m < n + 1, m.bell = ∑ p, p.parts.bell
i : ℕ
hi : i ∈ Finset.Iic n
this : i ≤ n
h1 : 1 ≤ i + 1
h2 : i + 1 ≤ n + 1
⊢ ∑ q, n.choose i * q.parts.bell = ∑ p, n.choose i * ((↑p).parts.erase (i + 1)).bell

Tactic:
have hsub : n + 1 - (i + 1 : ℕ) = n - i := by lia

Goal state after:
case a
n✝ n : ℕ
ih : ∀ m < n + 1, m.bell = ∑ p, p.parts.bell
i : ℕ
hi : i ∈ Finset.Iic n
this : i ≤ n
h1 : 1 ≤ i + 1
h2 : i + 1 ≤ n + 1
hsub : n + 1 - (i + 1) = n - i
⊢ ∑ q, n.choose i * q.parts.bell = ∑ p, n.choose i * ((↑p).parts.erase (i + 1)).bell
Module: Mathlib.Combinatorics.Enumerative.DyckWord

Goal state before:
pp: p q : DyckWord
r' : List DyckStep
h : r' ++ ↑p = ↑q
hq : count U r' + count D ↑p = count D r' + count D ↑p
⊢ count U (List.take ((r' ++ ↑p).length - (↑p).length) (r' ++ ↑p)) =
    count D (List.take ((r' ++ ↑p).length - (↑p).length) (r' ++ ↑p))

Tactic:
Nat.add_right_cancel_iff

Goal state after:
p q : DyckWord
r' : List DyckStep
h : r' ++ ↑p = ↑q
hq : count U r' = count D r'
⊢ count U (List.take ((r' ++ ↑p).length - (↑p).length) (r' ++ ↑p)) =
    count D (List.take ((r' ++ ↑p).length - (↑p).length) (r' ++ ↑p))
Module: Mathlib.Combinatorics.Enumerative.Partition.GenFun

Goal state before:
pp: case hg
R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : TopologicalSpace R
inst✝ : T2Space R
f : ℕ → ℕ → R
n : ℕ
p : n.Partition
s : Finset ℕ
hs : Icc 1 n ⊆ s
hs0 : 0 ∉ s
x : ℕ
hx : x ∈ s ∧ x ∉ p.parts
⊢ (coeff (p.toFinsuppAntidiag x)) (1 + ∑' (j : ℕ), f x (j + 1) • X ^ (x * (j + 1))) = 1

Tactic:
have hx0 : x ≠ 0 := fun h ↦ hs0 (h ▸ hx.1)

Goal state after:
case hg
R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : TopologicalSpace R
inst✝ : T2Space R
f : ℕ → ℕ → R
n : ℕ
p : n.Partition
s : Finset ℕ
hs : Icc 1 n ⊆ s
hs0 : 0 ∉ s
x : ℕ
hx : x ∈ s ∧ x ∉ p.parts
hx0 : x ≠ 0
⊢ (coeff (p.toFinsuppAntidiag x)) (1 + ∑' (j : ℕ), f x (j + 1) • X ^ (x * (j + 1))) = 1
Module: Mathlib.Combinatorics.Enumerative.Partition.GenFun

Goal state before:
pp: case hg
R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : TopologicalSpace R
inst✝ : T2Space R
f : ℕ → ℕ → R
n : ℕ
p : n.Partition
s : Finset ℕ
hs : Icc 1 n ⊆ s
hs0 : 0 ∉ s
⊢ ∀ x ∈ s \ p.parts.toFinset, (coeff (p.toFinsuppAntidiag x)) (1 + ∑' (j : ℕ), f x (j + 1) • X ^ (x * (j + 1))) = 1

Tactic:
intro x hx
    rw [mem_sdiff, Multiset.mem_toFinset] at hx
    have hx0 : x ≠ 0 := fun h ↦ hs0 (h ▸ hx.1)
    have hsum := (summable_genFun_term' f hx0).map_tsum _
      (WithPiTopology.continuous_constantCoeff R)
    simp [toFinsuppAntidiag, hsum, hx.2, hx0]

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

Goal state before:
pp: R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : TopologicalSpace R
inst✝ : T2Space R
f : ℕ → ℕ → R
n : ℕ
p : n.Partition
s : Finset ℕ
hs : Icc 1 n ⊆ s
hs0 : 0 ∉ s
i : ℕ
hi : i ∈ p.parts
hi0 : i ≠ 0
this :
  f i (Multiset.count i p.parts) = ∑' (j : ℕ), if Multiset.count i p.parts * i = i * (j + 1) then f i (j + 1) else 0
⊢ f i (Multiset.count i p.parts) =
    (coeff (p.toFinsuppAntidiag i)) 1 +
      ∑' (i_1 : ℕ), (coeff (p.toFinsuppAntidiag i)) (f i (i_1 + 1) • X ^ (i * (i_1 + 1)))

Tactic:
by
      simpa [toFinsuppAntidiag, hi, hi0, coeff_X_pow]

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
m : ℕ
hm : 0 < m
a✝ : Nontrivial R
x✝¹ : TopologicalSpace R := ⋯
x✝ : DiscreteTopology R
⊢ (∏' (i : ℕ), if ¬m ∣ i + 1 then ∑' (j : ℕ), X ^ ((i + 1) * j) else 1) * ∏' (i : ℕ), (1 - X ^ (i + 1)) =
    (∏' (i : ℕ), ∑ j ∈ range m, X ^ ((i + 1) * j)) * ∏' (i : ℕ), (1 - X ^ (i + 1))

Tactic:
rw [aux_mul_one_sub_X_pow R hm]

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NoZeroDivisors R
m : ℕ
hm : 0 < m
a✝ : Nontrivial R
x✝¹ : TopologicalSpace R := ⊥
x✝ : DiscreteTopology R
⊢ ∏' (i : ℕ), (1 - X ^ ((i + 1) * m)) = (∏' (i : ℕ), ∑ j ∈ range m, X ^ ((i + 1) * j)) * ∏' (i : ℕ), (1 - X ^ (i + 1))
Module: Mathlib.Combinatorics.Enumerative.Partition.Glaisher

Goal state before:
pp: n m : ℕ
hm : 0 < m
⊢ #(restricted n fun x ↦ ¬m ∣ x) = #(countRestricted n m)

Tactic:
by
  simpa using PowerSeries.ext_iff.mp
    (powerSeriesMk_card_restricted_eq_powerSeriesMk_card_countRestricted ℤ hm) n

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

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
K : ℝ
S : Finset G
hK : K < 1
hS : S.Nonempty
N : Finset G
hN : IsAtom K S N
n : G
hn : n ∈ N
one_mem_carrier : 1 ∈ n⁻¹ •> N
self_mem_smul_carrier : ∀ (x : G), x ∈ x •> n⁻¹ •> N
a : G
ha✝ : a ∈ n⁻¹ •> N
ha : 1 ∈ a⁻¹ •> n⁻¹ •> N
this : (n⁻¹ •> N ∩ a⁻¹ •> n⁻¹ •> N).Nonempty
⊢ a⁻¹ ∈ n⁻¹ •> N

Tactic:
simpa only [← (hN.smul_finset n⁻¹).eq_of_inter_nonempty hK.le hS
        ((hN.smul_finset n⁻¹).smul_finset a⁻¹) this] using! self_mem_smul_carrier a⁻¹

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

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
inst✝² : TopologicalSpace R
inst✝¹ : IsTopologicalRing R
inst✝ : T2Space R
a✝ : Nontrivial R
⊢ ∏' (n : ℕ), (1 - X ^ (n + 1)) = pentagonalSeries R

Tactic:
pentagonalSeries_eq_tsum_pow_pentagonal_sub

Goal state after:
R : Type u_1
inst✝³ : CommRing R
inst✝² : TopologicalSpace R
inst✝¹ : IsTopologicalRing R
inst✝ : T2Space R
a✝ : Nontrivial R
⊢ ∏' (n : ℕ), (1 - X ^ (n + 1)) = ∑' (k : ℕ), (-1) ^ k * (X ^ pentagonal (-↑k) - X ^ pentagonal (↑k + 1))
Module: Mathlib.Combinatorics.Enumerative.Pentagonal.PowerSeries

Goal state before:
pp: case refine_5
R : Type u_1
inst✝³ : CommRing R
inst✝² : TopologicalSpace R
inst✝¹ : IsTopologicalRing R
inst✝ : T2Space R
a✝ : Nontrivial R
n k : ℕ
hk : k ≥ n
⊢ ↑n < (X ^ ((k + 1) * (3 * k + 4) / 2)).order

Tactic:
rw [order_X_pow, Nat.cast_lt, ← Nat.add_one_le_iff, Nat.le_div_iff_mul_le (by simp)]

Goal state after:
case refine_5
R : Type u_1
inst✝³ : CommRing R
inst✝² : TopologicalSpace R
inst✝¹ : IsTopologicalRing R
inst✝ : T2Space R
a✝ : Nontrivial R
n k : ℕ
hk : k ≥ n
⊢ (n + 1) * 2 ≤ (k + 1) * (3 * k + 4)
Module: Mathlib.Combinatorics.Extremal.RuzsaSzemeredi

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

Tactic:
by
  let α := Fin (2 * n + 1)
  have : Nat.Coprime 2 (2 * n + 1) := by simp
  have : Fact (IsUnit (2 : Fin (2 * n + 1))) := ⟨by simpa
    using! (ZMod.unitOfCoprime 2 this).isUnit⟩
  open scoped Fin.CommRing in
  calc
    (2 * n + 1) * rothNumberNat n
    _ = Fintype.card α * addRothNumber (Iio (⟨n, by lia⟩ : α)) := by
      rw [Fin.addRothNumber_eq_rothNumberNat (by simp), Fintype.card_fin]
    _ ≤ Fintype.card α * addRothNumber (univ : Finset α) := by
      gcongr; exact subset_univ _
    _ ≤ ruzsaSzemerediNumber (Sum α (Sum α α)) := addRothNumber_le_ruzsaSzemerediNumber _
    _ = ruzsaSzemerediNumberNat (6 * n + 3) := 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_5
α : Type u_6
ι : Type u_7
κ : Type u_8
l : Subspace η α ι
η' : Type u_9
α' : Type u_10
ι' : Type u_11
eη : η ≃ η'
eα : α ≃ α'
eι : ι ≃ ι'
C : (ι → α) → κ
hl : IsMono C l
⊢ IsMono (fun x ↦ C (⇑eα.symm ∘ ⇑eα ∘ x)) l

Tactic:
simpa [← Function.comp_assoc]

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

Goal state before:
pp: α : Type u_1
M : Matroid α
D₁ D₂ : Set α
h : D₁ ∩ M.E = D₂ ∩ M.E
⊢ M ＼ (D₁ ∩ M.E) = M ＼ (D₂ ∩ M.E)

Tactic:
rw [h]

Goal state after:
Module: Mathlib.Combinatorics.Hindman

Goal state before:
pp: case h.head'
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 : M
b : Stream' M
⊢ ∀ (p : { s // s ∈ U }), b = Stream'.corec elem succ p → b.head ∈ ↑p

Tactic:
rintro p rfl

Goal state after:
case h.head'
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 : M
p : { s // s ∈ U }
⊢ (Stream'.corec elem succ p).head ∈ ↑p
Module: Mathlib.Combinatorics.Hindman

Goal state before:
pp: case h.tail'
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 : M
b : Stream' M
n : M
h : FP b.tail n
ih : ∀ (p : { s // s ∈ U }), b.tail = Stream'.corec elem succ p → n ∈ ↑p
⊢ ∀ (p : { s // s ∈ U }), b = Stream'.corec elem succ p → n ∈ ↑p

Tactic:
rintro p rfl

Goal state after:
case h.tail'
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
⊢ n ∈ ↑p
Module: Mathlib.Combinatorics.Hindman

Goal state before:
pp: case h.cons'
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 : M
b : Stream' M
n : M
h : FP b.tail n
ih : ∀ (p : { s // s ∈ U }), b.tail = Stream'.corec elem succ p → n ∈ ↑p
⊢ ∀ (p : { s // s ∈ U }), b = Stream'.corec elem succ p → b.head * n ∈ ↑p

Tactic:
rintro p rfl

Goal state after:
case h.cons'
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).head * n ∈ ↑p
Module: Mathlib.Combinatorics.Matroid.Minor.Delete

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

Tactic:
by
  rw [← indep_singleton, delete_indep_iff, disjoint_singleton_left, indep_singleton]

Goal state after:
Module: Mathlib.Combinatorics.HalesJewett

Goal state before:
pp: case neg.refine_4
α : 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
h : ¬∃ p ∈ s.lines, p.color = C' s.focus
⊢ (¬∃ a ∈ s.lines,
        (AlmostMono.color ∘ fun p ↦ { line := p.line.prod (map some l'), color := p.color, has_color := ⋯ }) a =
          { line := vertical s.focus (map some l'), color := C' s.focus, has_color := ⋯ }.color) ∧
    (Multiset.map (AlmostMono.color ∘ fun p ↦ { line := p.line.prod (map some l'), color := p.color, has_color := ⋯ })
        s.lines).Nodup

Tactic:
exact ⟨h, s.distinct_colors⟩

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

Goal state before:
pp: α : Type u_1
M : Matroid α
I X : Set α
hI : M.IsBasis I X
J : Set α
hJ : J ⊆ (M✶ ＼ I ＼ (X \ I)).E
hss : X \ I ⊆ (M✶ ＼ I).coloops
⊢ (M✶ ＼ I).Indep J ∧ Disjoint J (X \ I) ↔ Disjoint J (X \ I) ∧ (M✶ ＼ I).Indep J

Tactic:
and_comm

Goal state after:
α : Type u_1
M : Matroid α
I X : Set α
hI : M.IsBasis I X
J : Set α
hJ : J ⊆ (M✶ ＼ I ＼ (X \ I)).E
hss : X \ I ⊆ (M✶ ＼ I).coloops
⊢ Disjoint J (X \ I) ∧ (M✶ ＼ I).Indep J ↔ Disjoint J (X \ I) ∧ (M✶ ＼ I).Indep J
Module: Mathlib.Combinatorics.HalesJewett

Goal state before:
pp: case pos.succ
α : Type u
inst✝¹ : Fintype α
ihα : ∀ (κ : Type (max v u)) [Finite κ], ∃ ι x, ∀ (C : (ι → α) → κ), ∃ l, IsMono C l
κ : Type (max v u)
inst✝ : Finite κ
val✝ : Fintype κ
h : Nonempty α
r : ℕ
ihr : ∃ ι x, ∀ (C : (ι → Option α) → κ), (∃ s, s.lines.card = r) ∨ ∃ l, IsMono C l
⊢ ∃ ι x, ∀ (C : (ι → Option α) → κ), (∃ s, s.lines.card = r + 1) ∨ ∃ l, IsMono C l

Tactic:
| succ r ihr =>

Goal state after:
Module: Mathlib.RingTheory.MvPolynomial.Groebner

Goal state before:
pp: case left
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
f b : MvPolynomial σ R
hb : IsUnit (m.leadingCoeff b)
hbf : m.degree b ≤ m.degree f
hf : m.degree f ≠ 0
H : m.degree f = m.degree ((monomial (m.degree f - m.degree b)) (↑hb.unit⁻¹ * m.leadingCoeff f)) + m.degree b
H' : coeff (m.degree f) (m.reduce hb f) = 0
⊢ m.degree ((monomial (m.degree f - m.degree b)) (↑hb.unit⁻¹ * m.leadingCoeff f)) + m.degree b = m.degree f

Tactic:
exact H.symm

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

Goal state before:
pp: α : Type u_1
M : Matroid α
I X : Set α
hI : M.IsBasis' I X
D : Set α
⊢ Disjoint X D ∧ M.Dep (D ∪ I) ↔ M.Dep (D ∪ I) ∧ Disjoint X D

Tactic:
and_comm

Goal state after:
α : Type u_1
M : Matroid α
I X : Set α
hI : M.IsBasis' I X
D : Set α
⊢ M.Dep (D ∪ I) ∧ Disjoint X D ↔ M.Dep (D ∪ I) ∧ Disjoint X D
Module: Mathlib.Combinatorics.Matroid.Sum

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
M : (i : ι) → Matroid (α i)
I X : Set ((i : ι) × α i)
hI : ∀ (i : ι), (M i).Indep (Sigma.mk i ⁻¹' I)
x✝ :
  I ⊆ X ∧
    (∀ ⦃t : Set ((i : ι) × α i)⦄, (∀ (i : ι), (M i).Indep (Sigma.mk i ⁻¹' t)) → t ⊆ X → I ⊆ t → I = t) ∧
      X ⊆ univ.sigma fun i ↦ (M i).E
hIX : I ⊆ X
h : ∀ ⦃t : Set ((i : ι) × α i)⦄, (∀ (i : ι), (M i).Indep (Sigma.mk i ⁻¹' t)) → t ⊆ X → I ⊆ t → I = t
h' : X ⊆ univ.sigma fun i ↦ (M i).E
i : ι
⊢ Sigma.mk i ⁻¹' X ⊆ (M i).E

Tactic:
simpa using preimage_mono (f := Sigma.mk i) h'

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

Goal state before:
pp: case inr
α : Type u_1
M : Matroid α
K C : Set α
aux : ∀ {K : Set α}, (M ／ K).IsCircuit C → M.Indep K → ∃ C', M.IsCircuit C' ∧ C ⊆ C' ∧ C' ⊆ C ∪ K
hKi : ¬M.Indep K
I : Set α
hC : (M ／ I).IsCircuit C ∧ Disjoint C (K \ I)
hI : M.IsBasis' I K
⊢ ∃ C', M.IsCircuit C' ∧ C ⊆ C' ∧ C' ⊆ C ∪ K

Tactic:
obtain ⟨C', hC', hCC', hC'ss⟩ := aux hC.1 hI.indep

Goal state after:
case inr
α : Type u_1
M : Matroid α
K C : Set α
aux : ∀ {K : Set α}, (M ／ K).IsCircuit C → M.Indep K → ∃ C', M.IsCircuit C' ∧ C ⊆ C' ∧ C' ⊆ C ∪ K
hKi : ¬M.Indep K
I : Set α
hC : (M ／ I).IsCircuit C ∧ Disjoint C (K \ I)
hI : M.IsBasis' I K
C' : Set α
hC' : M.IsCircuit C'
hCC' : C ⊆ C'
hC'ss : C' ⊆ C ∪ I
⊢ ∃ C', M.IsCircuit C' ∧ C ⊆ C' ∧ C' ⊆ C ∪ K
Module: Mathlib.Combinatorics.Nullstellensatz

Goal state before:
pp: 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
⊢ lex.toSyn e ≤ lex.toSyn (single () #S)

Tactic:
← Alon.degree_P

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
⊢ lex.toSyn e ≤ lex.toSyn (MonomialOrder.degree ?refine_1.m (P S ()))

case refine_1.m
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
⊢ MonomialOrder Unit
Module: Mathlib.Combinatorics.SetFamily.Compression.Down

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
𝒜 ℬ : Finset (Finset α)
⊢ memberSubfamily a (𝒜 ∩ ℬ) = memberSubfamily a 𝒜 ∩ memberSubfamily a ℬ

Tactic:
by
  unfold memberSubfamily
  rw [filter_inter_distrib, image_inter_of_injOn _ _ ((erase_injOn' _).mono _)]
  simp

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

Goal state before:
pp: case refine_1
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
a : α
s : Finset α
hs : insert a s ∈ 𝒜
⊢ insert a s ∈ 𝒜 ∧ a ∈ insert a s

Tactic:
exact ⟨hs, mem_insert_self _ _⟩

Goal state after:
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 ∈ 𝓓 a 𝒜

Tactic:
simp_rw [mem_compression, erase_idem, and_self_iff]
  refine (em _).imp_right fun h => ⟨h, ?_⟩
  rwa [insert_erase (erase_ne_self.1 (ne_of_mem_of_not_mem hs h).symm)]

Goal state after:
Module: Mathlib.Data.Finset.Sups

Goal state before:
pp: α : Type u_2
inst✝ : DecidableEq α
s : Finset α
⊢ s.powerset ⊻ s.powerset = s.powerset

Tactic:
by simp [← powerset_union]

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

Goal state before:
pp: α : Type u_1
inst✝² : SemilatticeInf α
s : Finset α
a : α
inst✝¹ : DecidableLE α
inst✝ : BoundedOrder α
hs : IsAntichain (fun x1 x2 ↦ x1 ≤ x2) ↑s
ha : a ∈ s
⊢ a ≤ s.truncatedInf a

Tactic:
truncatedInf_of_mem (subset_upperClosure ha),

Goal state after:
α : Type u_1
inst✝² : SemilatticeInf α
s : Finset α
a : α
inst✝¹ : DecidableLE α
inst✝ : BoundedOrder α
hs : IsAntichain (fun x1 x2 ↦ x1 ≤ x2) ↑s
ha : a ∈ s
⊢ a ≤ {b ∈ s | b ≤ a}.inf' ⋯ id
Module: Mathlib.Combinatorics.SetFamily.AhlswedeZhang

Goal state before:
pp: α : Type u_1
inst✝² : SemilatticeInf α
s : Finset α
a : α
inst✝¹ : DecidableLE α
inst✝ : BoundedOrder α
hs : IsAntichain (fun x1 x2 ↦ x1 ≤ x2) ↑s
ha : a ∈ s
⊢ s.truncatedInf a = a

Tactic:
refine le_antisymm truncatedInf_le ?_
  simp_rw [truncatedInf_of_mem (subset_upperClosure ha), le_inf'_iff, mem_filter]
  rintro b ⟨hb, hba⟩
  exact (hs.eq hb ha hba).ge

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

Goal state before:
pp: α : Type u_1
inst✝³ : GeneralizedBooleanAlgebra α
inst✝² : DecidableRel Disjoint
inst✝¹ : DecidableLE α
s : Finset α
u v a : α
inst✝ : DecidableEq α
⊢ a ∈ s ∧ compress u v a ∈ s ∨ (∃ a_1 ∈ s, compress u v a_1 = a) ∧ a ∉ s ↔
    a ∈ s ∧ compress u v a ∈ s ∨ a ∉ s ∧ ∃ a_1 ∈ s, compress u v a_1 = a

Tactic:
and_comm

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
𝒜 ℬ : Finset (Finset α)
s : Finset α
h𝒜 : IsLowerSet ↑𝒜
hℬ : IsLowerSet ↑ℬ
h𝒜s : ∀ t ∈ 𝒜, t ⊆ s
hℬs : ∀ t ∈ ℬ, t ⊆ s
⊢ #𝒜 * #ℬ ≤ 2 ^ #s * #(𝒜 ∩ ℬ)

Tactic:
induction s using Finset.induction generalizing 𝒜 ℬ with
  | empty =>
    simp_rw [subset_empty, ← subset_singleton_iff', subset_singleton_iff] at h𝒜s hℬs
    obtain rfl | rfl := h𝒜s
    · simp only [card_empty, zero_mul, empty_inter, mul_zero, le_refl]
    obtain rfl | rfl := hℬs
    · simp
    · simp only [card_empty, pow_zero, inter_singleton_of_mem, mem_singleton, card_singleton,
        le_refl]
  | insert a s hs ih =>
  rw [card_insert_of_notMem hs, ← card_memberSubfamily_add_card_nonMemberSubfamily a 𝒜, ←
    card_memberSubfamily_add_card_nonMemberSubfamily a ℬ, add_mul, mul_add, mul_add,
    add_comm (_ * _), add_add_add_comm]
  grw [mul_add_mul_le_mul_add_mul
    (card_le_card h𝒜.memberSubfamily_subset_nonMemberSubfamily) <|
      card_le_card hℬ.memberSubfamily_subset_nonMemberSubfamily, ← two_mul, pow_succ', mul_assoc]
  have h₀ : ∀ 𝒞 : Finset (Finset α), (∀ t ∈ 𝒞, t ⊆ insert a s) →
      ∀ t ∈ 𝒞.nonMemberSubfamily a, t ⊆ s := by
    rintro 𝒞 h𝒞 t ht
    rw [mem_nonMemberSubfamily] at ht
    exact (subset_insert_iff_of_notMem ht.2).1 (h𝒞 _ ht.1)
  have h₁ : ∀ 𝒞 : Finset (Finset α), (∀ t ∈ 𝒞, t ⊆ insert a s) →
      ∀ t ∈ 𝒞.memberSubfamily a, t ⊆ s := by
    rintro 𝒞 h𝒞 t ht
    rw [mem_memberSubfamily] at ht
    exact (subset_insert_iff_of_notMem ht.2).1 ((subset_insert _ _).trans <| h𝒞 _ ht.1)
  gcongr
  refine (add_le_add (ih h𝒜.memberSubfamily hℬ.memberSubfamily (h₁ _ h𝒜s) <| h₁ _ hℬs) <|
    ih h𝒜.nonMemberSubfamily hℬ.nonMemberSubfamily (h₀ _ h𝒜s) <| h₀ _ hℬs).trans_eq ?_
  rw [← mul_add, ← memberSubfamily_inter, ← nonMemberSubfamily_inter,
    card_memberSubfamily_add_card_nonMemberSubfamily]

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
H : G.Subgraph
hr : G.Reachable u v
h : ∀ v ∈ H.verts, ∀ (w : V), G.Adj v w → H.Adj v w
hu : u ∈ H.verts
⊢ v ∈ H.verts

Tactic:
exact aux hu hr.some

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected

Goal state before:
pp: V : Type u
x y : V
h : x = y
⊢ ⊤.Reachable x y

Tactic:
rw [h]

Goal state after:
Module: Mathlib.Data.Setoid.Partition

Goal state before:
pp: ι : Type u_1
α : Type u_2
s : ι → Set α
hs : IndexedPartition s
β : Type u_3
f : ι → α → β
h_injOn : ∀ (i : ι), InjOn (f i) (s i)
h_disjoint : univ.PairwiseDisjoint fun i ↦ f i '' s i
x y : α
h : hs.piecewise f x = hs.piecewise f y
this : hs.index x = hs.index y
⊢ x = y

Tactic:
apply h_injOn (hs.index x) (hs.mem_index x) (this ▸ hs.mem_index y)

Goal state after:
ι : Type u_1
α : Type u_2
s : ι → Set α
hs : IndexedPartition s
β : Type u_3
f : ι → α → β
h_injOn : ∀ (i : ι), InjOn (f i) (s i)
h_disjoint : univ.PairwiseDisjoint fun i ↦ f i '' s i
x y : α
h : hs.piecewise f x = hs.piecewise f y
this : hs.index x = hs.index y
⊢ f (hs.index x) x = f (hs.index x) y
Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex

Goal state before:
pp: V : Type u_4
W : Type u_5
inst✝¹ : Nonempty V
inst✝ : Nonempty W
⊢ (completeBipartiteGraph V W).Colorable 2

Tactic:
by simpa using (CompleteBipartiteGraph.bicoloring V W).colorable

Goal state after: