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

Goal state before:
pp: 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
⊢ 2 * n - 1 ≤ (2 * m - k) * n - 1

Tactic:
by gcongr; lia

Goal state after:
Module: Mathlib.Combinatorics.Colex

Goal state before:
pp: α : Type u_1
inst✝ : PartialOrder α
s : Finset α
a : α
⊢ toColex {a} ≤ toColex s ↔ ∃ x ∈ s, a ≤ x

Tactic:
by
  simp [toColex_le_toColex]; by_cases a ∈ s <;> aesop

Goal state after:
Module: Mathlib.LinearAlgebra.Projectivization.Basic

Goal state before:
pp: case mpr
K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v w : V
hv : v ≠ 0
hw : w ≠ 0
a : K
ha : 0 • w = v
c : a = 0
⊢ 0 = v

Tactic:
zero_smul

Goal state after:
case mpr
K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v w : V
hv : v ≠ 0
hw : w ≠ 0
a : K
ha : 0 = v
c : a = 0
⊢ 0 = v
Module: Mathlib.LinearAlgebra.Projectivization.Basic

Goal state before:
pp: K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v w : V
hv : v ≠ 0
hw : w ≠ 0
⊢ mk K v hv = mk K w hw ↔ ∃ a, a • w = v

Tactic:
rw [mk_eq_mk_iff K v w hv hw]
  constructor
  · rintro ⟨a, ha⟩
    exact ⟨a, ha⟩
  · rintro ⟨a, ha⟩
    refine ⟨Units.mk0 a fun c => hv.symm ?_, ha⟩
    rwa [c, zero_smul] at ha

Goal state after:
Module: Mathlib.LinearAlgebra.CrossProduct

Goal state before:
pp: case neg.mp
F : Type u_2
inst✝ : Field F
v w : Fin 3 → F
hv : ¬v = 0
⊢ ¬LinearIndependent F ![v, w] → (crossProduct v) w = 0

Tactic:
rw [LinearIndependent.pair_iff' hv, not_forall_not]

Goal state after:
case neg.mp
F : Type u_2
inst✝ : Field F
v w : Fin 3 → F
hv : ¬v = 0
⊢ (∃ x, x • v = w) → (crossProduct v) w = 0
Module: Mathlib.LinearAlgebra.Projectivization.Basic

Goal state before:
pp: K : Type u_1
V : Type u_2
inst✝⁵ : DivisionRing K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
L : Type u_3
W : Type u_4
inst✝² : DivisionRing L
inst✝¹ : AddCommGroup W
inst✝ : Module L W
σ : K →+* L
f : V →ₛₗ[σ] W
hf : Function.Injective ⇑f
⊢ ∀ (a b : { v // v ≠ 0 }), (projectivizationSetoid K V) a b → (projectivizationSetoid L W) ⟨f ↑a, ⋯⟩ ⟨f ↑b, ⋯⟩

Tactic:
rintro ⟨u, hu⟩ ⟨v, hv⟩ ⟨a, ha⟩

Goal state after:
K : Type u_1
V : Type u_2
inst✝⁵ : DivisionRing K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
L : Type u_3
W : Type u_4
inst✝² : DivisionRing L
inst✝¹ : AddCommGroup W
inst✝ : Module L W
σ : K →+* L
f : V →ₛₗ[σ] W
hf : Function.Injective ⇑f
u : V
hu : u ≠ 0
v : V
hv : v ≠ 0
a : Kˣ
ha : (fun m ↦ m • ↑⟨v, hv⟩) a = ↑⟨u, hu⟩
⊢ (projectivizationSetoid L W) ⟨f ↑⟨u, hu⟩, ⋯⟩ ⟨f ↑⟨v, hv⟩, ⋯⟩
Module: Mathlib.Combinatorics.Colex

Goal state before:
pp: case refine_1
α : Type u_1
inst✝¹ : LinearOrder α
𝒜 : Finset (Finset α)
r : ℕ
inst✝ : Fintype α
h𝒜 : IsInitSeg 𝒜 r
h𝒜₀ : 𝒜.Nonempty
hs : 𝒜.sup' h𝒜₀ ⇑toColex ∈ ⇑ofColex ⁻¹' ↑𝒜
t : Finset α
p : t ∈ 𝒜
⊢ #(𝒜.sup' h𝒜₀ ⇑toColex) = #t ∧ toColex t ≤ toColex (𝒜.sup' h𝒜₀ ⇑toColex)

Tactic:
h𝒜.1 p,

Goal state after:
case refine_1
α : Type u_1
inst✝¹ : LinearOrder α
𝒜 : Finset (Finset α)
r : ℕ
inst✝ : Fintype α
h𝒜 : IsInitSeg 𝒜 r
h𝒜₀ : 𝒜.Nonempty
hs : 𝒜.sup' h𝒜₀ ⇑toColex ∈ ⇑ofColex ⁻¹' ↑𝒜
t : Finset α
p : t ∈ 𝒜
⊢ #(𝒜.sup' h𝒜₀ ⇑toColex) = r ∧ toColex t ≤ toColex (𝒜.sup' h𝒜₀ ⇑toColex)
Module: Mathlib.Combinatorics.Derangements.Finite

Goal state before:
pp: case ind.succ.succ
n : ℕ
hyp : ∀ m < n + 1 + 1, card ↑(derangements (Fin m)) = numDerangements m
⊢ card ↑(derangements (Fin (n + 1 + 1))) = (n + 1) * (numDerangements n + numDerangements (n + 1))

Tactic:
card_derangements_fin_add_two,

Goal state after:
case ind.succ.succ
n : ℕ
hyp : ∀ m < n + 1 + 1, card ↑(derangements (Fin m)) = numDerangements m
⊢ (n + 1) * card ↑(derangements (Fin n)) + (n + 1) * card ↑(derangements (Fin (n + 1))) =
    (n + 1) * (numDerangements n + numDerangements (n + 1))
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⁻¹ = A⁻¹ * A

Tactic:
exact mul_inv_eq_inv_mul_of_doubling_lt_two (by qify at h ⊢; linarith)

Goal state after:
Module: Mathlib.Combinatorics.Configuration

Goal state before:
pp: P : Type u_1
L : Type u_2
inst✝² : Membership P L
K : Type u_3
inst✝¹ : Field K
inst✝ : DecidableEq K
v w : ℙ K (Fin 3 → K)
a✝ : v ≠ w
⊢ ℙ K (Fin 3 → K)

Tactic:
exact cross v w

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

Goal state before:
pp: n : ℕ
⊢ catalan n = n.centralBinom / (n + 1)

Tactic:
suffices (catalan n : ℚ) = Nat.centralBinom n / (n + 1) by
    have h := Nat.succ_dvd_centralBinom n
    exact mod_cast this
  induction n using Nat.caseStrongRecOn with
  | zero => simp
  | ind d hd =>
    simp_rw [catalan_succ, Nat.cast_sum, Nat.cast_mul]
    trans (∑ i : Fin d.succ, Nat.centralBinom i / (i + 1) *
                            (Nat.centralBinom (d - i) / (d - i + 1)) : ℚ)
    · congr
      ext1 x
      have m_le_d : x.val ≤ d := by lia
      have d_minus_x_le_d : (d - x.val) ≤ d := tsub_le_self
      rw [hd _ m_le_d, hd _ d_minus_x_le_d]
      norm_cast
    · trans (∑ i : Fin d.succ, (gosperCatalan (d + 1) (i + 1) - gosperCatalan (d + 1) i))
      · refine sum_congr rfl fun i _ => ?_
        rw [gosper_trick i.is_le, mul_div]
      · rw [← sum_range fun i => gosperCatalan (d + 1) (i + 1) - gosperCatalan (d + 1) i,
            sum_range_sub, Nat.succ_eq_add_one]
        rw [gosper_catalan_sub_eq_central_binom_div d]
        norm_cast

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

Goal state before:
pp: x : ℕ
hx : x ≠ 0
c : ℕ
⊢ (x ! ^ c * c ! * ∏ j ∈ Finset.range c, (j * x + x - 1).choose (x - 1)) * (c * x + x - 1).choose (x - 1) * x ! *
      (c + 1) =
    (c + 1) * (c * x + x - 1).choose (x - 1) * (x * c)! * x !

Tactic:
rw [bell_mul_eq_lemma hx]; ring

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

Goal state before:
pp: case h
m : Multiset ℕ
a : ℕ
ha : a ≠ 0
rest : ℕ := ∏ j ∈ (m.toFinset.erase 0).erase a, (count j m)!
⊢ (m.toFinset.erase 0).erase a = ((a ::ₘ m).toFinset.erase 0).erase a

pp: case a
m : Multiset ℕ
a : ℕ
ha : a ≠ 0
rest : ℕ := ∏ j ∈ (m.toFinset.erase 0).erase a, (count j m)!
j : ℕ
hj : j ∈ ((a ::ₘ m).toFinset.erase 0).erase a
⊢ (count j m)! = (count j (a ::ₘ m))!

Tactic:
· grind [Multiset.toFinset_cons]

Goal state after:
case a
m : Multiset ℕ
a : ℕ
ha : a ≠ 0
rest : ℕ := ∏ j ∈ (m.toFinset.erase 0).erase a, (count j m)!
j : ℕ
hj : j ∈ ((a ::ₘ m).toFinset.erase 0).erase a
⊢ (count j m)! = (count j (a ::ₘ m))!
Module: Mathlib.Combinatorics.Enumerative.Bell

Goal state before:
pp: m : Multiset ℕ
a : ℕ
ha : a ≠ 0
rest : ℕ := ∏ j ∈ (m.toFinset.erase 0).erase a, (count j m)!
⊢ (a ::ₘ m).bell * count a (a ::ₘ m) = (m.sum + a).choose a * m.bell

Tactic:
have hrest : rest = ∏ j ∈ ((a ::ₘ m).toFinset.erase 0).erase a, ((a ::ₘ m).count j)! := by
    unfold rest
    congr! 1 with j hj
    · grind [Multiset.toFinset_cons]
    · simp [Finset.mem_erase.mp hj]

Goal state after:
m : Multiset ℕ
a : ℕ
ha : a ≠ 0
rest : ℕ := ∏ j ∈ (m.toFinset.erase 0).erase a, (count j m)!
hrest : rest = ∏ j ∈ ((a ::ₘ m).toFinset.erase 0).erase a, (count j (a ::ₘ m))!
⊢ (a ::ₘ m).bell * count a (a ::ₘ m) = (m.sum + a).choose a * m.bell
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 𝕜 𝕝
⊢ 0 • 1 = 0

Tactic:
zero_smul

Goal state after:
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 𝕜 𝕝
⊢ 0 = 0
Module: Mathlib.Combinatorics.Enumerative.IncidenceAlgebra

Goal state before:
pp: 𝕜 : Type u_2
α : Type u_5
inst✝⁴ : AddCommGroup 𝕜
inst✝³ : One 𝕜
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b : α
⊢ ∑ x ∈ Icc a b, (mu' 𝕜) x b = if a = b then 1 else 0

Tactic:
by
  split_ifs with hab
  · simp [hab]
  by_cases hab : a ≤ b
  · simp [Icc_eq_cons_Ioc hab, mu'_eq_sum_Ioc_of_ne ‹_›]
  · exact sum_eq_zero fun x hx ↦ apply_eq_zero_of_not_le
      (fun hxb ↦ hab <| (mem_Icc.1 hx).1.trans hxb) _

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

Goal state before:
pp: p q : DyckWord
h✝ : p ≠ 0
h : ¬p = 0
i : ℕ
lb : 0 < i
ub : i < (↑(p.take (p.firstReturn + 1) ⋯)).length
⊢ count D (List.take i ↑(p.take (p.firstReturn + 1) ⋯)) < count U (List.take i ↑(p.take (p.firstReturn + 1) ⋯))

Tactic:
simp only [take, length_take, lt_min_iff] at ub ⊢
      replace ub := ub.1
      rw [take_take, min_eq_left ub.le]
      rw [show i = i - 1 + 1 by lia] at ub ⊢
      rw [Nat.add_lt_add_iff_right] at ub
      exact count_D_lt_count_U_of_lt_firstReturn ub

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

Goal state before:
pp: p✝ q✝ : DyckWord
h : p✝ ≠ 0
p q : DyckWord
pq : p ≤ q
qp : q ≤ p
⊢ p = q

Tactic:
have h₁ := infix_of_le pq
    have h₂ := infix_of_le qp
    exact DyckWord.ext <| h₁.eq_of_length <| h₁.length_le.antisymm h₂.length_le

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

Goal state before:
pp: case e'_6
R : Type u_1
inst✝⁴ : TopologicalSpace R
inst✝³ : T2Space R
inst✝² : CommSemiring R
inst✝¹ : IsTopologicalSemiring R
p : ℕ → Prop
inst✝ : DecidablePred p
⊢ (PowerSeries.mk fun n ↦ ↑(#(restricted n p))) = genFun fun i c ↦ if p i then 1 else 0

Tactic:
simp_rw [genFun, restricted, card_filter, Finsupp.prod, prod_boole]
    simp

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
⊢ HasProd (fun i ↦ 1 + ∑' (j : ℕ), f (i + 1) (j + 1) • X ^ ((i + 1) * (j + 1))) (genFun f)

Tactic:
rw [HasProd, WithPiTopology.tendsto_iff_coeff_tendsto]
  refine fun d ↦ tendsto_atTop_of_eventually_const (fun s (hs : s ≥ range d) ↦ ?_)
  have : ∏ i ∈ s, ((1 : R⟦X⟧) + ∑' j, f (i + 1) (j + 1) • X ^ ((i + 1) * (j + 1)))
      = ∏ i ∈ s.map (addRightEmbedding 1), (1 + ∑' j, f i (j + 1) • X ^ (i * (j + 1))) := by simp
  rw [this]
  have hs : Icc 1 d ⊆ s.map (addRightEmbedding 1) := by
    intro i
    suffices 1 ≤ i → i ≤ d → ∃ a ∈ s, a + 1 = i by simpa
    intro h1 h2
    refine ⟨i - 1, mem_of_subset hs ?_, ?_⟩ <;> grind
  rw [coeff_genFun, coeff_prod]
  refine (sum_of_injOn toFinsuppAntidiag (toFinsuppAntidiag_injective d).injOn ?_ ?_ ?_).symm
  · intro p _
    exact mem_of_subset (finsuppAntidiag_mono hs _) p.toFinsuppAntidiag_mem_finsuppAntidiag
  · exact fun g hg hg' ↦ aux_prod_coeff_eq_zero_of_notMem_range f (by simp) hg (by simpa using hg')
  · exact fun p _ ↦ aux_prod_f_eq_prod_coeff f p hs (by simp)

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
⊢ ∃ H x, IsAtom K S (↑H).toFinset

Tactic:
obtain ⟨N, hN⟩ := exists_isAtom hK hS
  obtain ⟨n, hn⟩ := IsAtom.nonempty hK hS hN
  have one_mem_carrier : 1 ∈ n⁻¹ •> N := by simpa [mem_inv_smul_finset_iff]
  have self_mem_smul_carrier (x : G) : x ∈ x • n⁻¹ • N := by
    apply smul_mem_smul_finset (a := x) at one_mem_carrier
    simpa only [smul_eq_mul, mul_one] using! one_mem_carrier
  let H : Subgroup G := {
    carrier := n⁻¹ •> N
    one_mem' := mod_cast one_mem_carrier
    mul_mem' {a b} ha hb := by
      rw [← coe_smul_finset, mem_coe] at *
      apply smul_mem_smul_finset (a := a) at hb
      rw [smul_eq_mul] at hb
      have : (n⁻¹ •> N ∩ a •> n⁻¹ •> N).Nonempty := ⟨a, by
        simpa only [mem_inter] using! ⟨ha, self_mem_smul_carrier a⟩⟩
      simpa only [← (hN.smul_finset n⁻¹).eq_of_inter_nonempty hK.le hS
        ((hN.smul_finset n⁻¹).smul_finset a) this] using! hb
    inv_mem' {a} ha := by
      rw [← coe_smul_finset, mem_coe] at *
      apply smul_mem_smul_finset (a := a⁻¹) at ha
      rw [smul_eq_mul, inv_mul_cancel] at ha
      have : (n⁻¹ •> N ∩ a⁻¹ •> n⁻¹ •> N).Nonempty := ⟨1, by simpa using! ⟨one_mem_carrier, ha⟩⟩
      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⁻¹
  }
  refine ⟨H, Fintype.ofFinset (n⁻¹ •> N) fun a => ?_, ?_⟩
  · simpa only [← mem_coe, coe_smul_finset] using! H.mem_carrier
  · simpa [Set.toFinset_smul_set, toFinset_coe, H] using! IsAtom.smul_finset n⁻¹ hN

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
K : ℝ := 1 - ε / 2
hK : K < 1
ex : Finset G → ℝ := expansion K S
κ : ℝ := connectivity K S
H : Subgroup G
w✝ : Fintype ↥H
hH : IsAtom K S (↑H).toFinset
Z : Finset G
hZS : Z ⊆ S
hHZS : ↑H * ↑Z = ↑H * ↑S
hZinj : Set.InjOn (fun x ↦ ↑H <• x) ↑Z
A : Finset G
hA₁ : #S ≤ #A
hA₂ : ↑(#(A * S)) ≤ (2 - ε) * ↑(#S)
calc₁ : ex (↑H).toFinset ≤ (1 - ε / 2) * ↑(#S)
⊢ ↑(#(↑H).toFinset) * ↑(#Z) / ↑(#(↑H).toFinset) = ↑(#((↑H).toFinset * Z)) / ↑(#(↑H).toFinset)

Tactic:
by
        simp [← card_mul_eq_mul_card_of_injOn_opSMul hZinj, Nat.cast_mul]

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

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
G H : Graph α β
h : H ≤ G
F : Set β
⊢ V(H.restrict F) ⊆ V(G.restrict F)

Tactic:
simpa using h.vertexSet_mono

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

Goal state before:
pp: α : Type u_1
β : Type u_4
G : Graph α β
⊢ map id G = G

Tactic:
ext a b c

Goal state after:
case hV
α : Type u_1
β : Type u_4
G : Graph α β
a : α
⊢ a ∈ V(map id G) ↔ a ∈ V(G)

case h
α : Type u_1
β : Type u_4
G : Graph α β
a : β
b c : α
⊢ (map id G).IsLink a b c ↔ G.IsLink a b c
Module: Mathlib.Combinatorics.Graph.Maps

Goal state before:
pp: α : Type u_1
α' : Type u_2
α'' : Type u_3
β : Type u_4
G : Graph α β
f : α → α'
f' : α' → α''
⊢ map f' (map f G) = map (f' ∘ f) G

Tactic:
ext a b c

Goal state after:
case hV
α : Type u_1
α' : Type u_2
α'' : Type u_3
β : Type u_4
G : Graph α β
f : α → α'
f' : α' → α''
a : α''
⊢ a ∈ V(map f' (map f G)) ↔ a ∈ V(map (f' ∘ f) G)

case h
α : Type u_1
α' : Type u_2
α'' : Type u_3
β : Type u_4
G : Graph α β
f : α → α'
f' : α' → α''
a : β
b c : α''
⊢ (map f' (map f G)).IsLink a b c ↔ (map (f' ∘ f) G).IsLink a b c
Module: Mathlib.RingTheory.MvPolynomial.Groebner

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

Tactic:
rw [← coeff_degree_ne_zero_iff (m := m), hf'] at this

Goal state after:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
f : MvPolynomial σ R
hf : m.degree f ≠ 0
hf' : m.degree (m.subLTerm f) = m.degree f
this : coeff (m.degree f) (m.subLTerm f) ≠ 0
⊢ False
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
e : α
he : e ∈ X \ I
⊢ M.Dep (insert e I)

Tactic:
hI.indep.insert_dep_iff,

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
e : α
he : e ∈ X \ I
⊢ e ∈ M.closure I \ I
Module: Mathlib.Combinatorics.Matroid.Minor.Contract

Goal state before:
pp: α : Type u_1
M : Matroid α
e : α
C I : Set α
hI : M.IsBasis' I C
⊢ (Disjoint {e} I ∧ M.Dep (insert e I)) ∧ e ∉ C \ I ↔ e ∈ M.closure C ∧ e ∉ C

Tactic:
hI.indep.insert_dep_iff,

Goal state after:
α : Type u_1
M : Matroid α
e : α
C I : Set α
hI : M.IsBasis' I C
⊢ (Disjoint {e} I ∧ e ∈ M.closure I \ I) ∧ e ∉ C \ I ↔ e ∈ M.closure C ∧ e ∉ C
Module: Mathlib.Combinatorics.Nullstellensatz

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
σ : Type u_2
inst✝ : Nontrivial R
m : MonomialOrder σ
S : Finset R
i : σ
r : R
a✝ : r ∈ S
⊢ IsRegular (m.leadingCoeff (X i - C r))

Tactic:
rw [m.monic_X_sub_C]

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
σ : Type u_2
inst✝ : Nontrivial R
m : MonomialOrder σ
S : Finset R
i : σ
r : R
a✝ : r ∈ S
⊢ IsRegular 1
Module: Mathlib.Combinatorics.Quiver.Path.Decomposition

Goal state before:
pp: case zero
V : Type u_1
inst✝ : Quiver V
a b : V
p : Path a b
S : Set V
ha_not_in_S : ¬a ∈ S
hb_in_S : b ∈ S
h_len : p.length = 0
⊢ ∃ u, ¬u ∈ S ∧ ∃ v, v ∈ S ∧ ∃ e p₁ p₂, p = p₁.comp (e.toPath.comp p₂)

Tactic:
obtain rfl := eq_of_length_zero p h_len
    exact (ha_not_in_S hb_in_S).elim

Goal state after:
Module: Mathlib.Combinatorics.Nullstellensatz

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

Tactic:
neg_eq_zero,

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

Goal state before:
pp: V : Type u_1
M : Type u_2
inst✝¹ : Monoid M
inst✝ : MulAction M V
S : Type u_3
ι : S → M
x : SchreierGraph V ι
⊢ (1 • x).toVertex = x.toVertex

Tactic:
exact one_smul M x.toVertex

Goal state after:
Module: Mathlib.Combinatorics.Nullstellensatz

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

Tactic:
rw [hg, mul_comm]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : α
𝒜 : Finset (Finset α)
⊢ Set.InjOn (fun s ↦ s.erase a) ↑({s ∈ 𝒜 | a ∈ s})

Tactic:
· apply (erase_injOn' _).mono
    simp

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

Goal state before:
pp: α : Type u_1
inst✝ : GeneralizedBooleanAlgebra α
u v a : α
ha : a ∈ {x | Disjoint u x ∧ v ≤ x}
b : α
hb : b ∈ {x | Disjoint u x ∧ v ≤ x}
hab : (fun x ↦ (x ⊔ u) \ v) a = (fun x ↦ (x ⊔ u) \ v) b
⊢ ((a ⊔ u) \ v) \ u ⊔ v = ((b ⊔ u) \ v) \ u ⊔ v

Tactic:
dsimp at hab

Goal state after:
α : Type u_1
inst✝ : GeneralizedBooleanAlgebra α
u v a : α
ha : a ∈ {x | Disjoint u x ∧ v ≤ x}
b : α
hb : b ∈ {x | Disjoint u x ∧ v ≤ x}
hab : (a ⊔ u) \ v = (b ⊔ u) \ v
⊢ ((a ⊔ u) \ v) \ u ⊔ v = ((b ⊔ u) \ v) \ u ⊔ v
Module: Mathlib.Combinatorics.SetFamily.Intersecting

Goal state before:
pp: α : Type u_1
inst✝¹ : BooleanAlgebra α
inst✝ : Fintype α
s : Finset α
hs : (↑s).Intersecting
⊢ #(s.disjUnion (map { toFun := compl, inj' := ⋯ } s) ⋯) = 2 * #s

Tactic:
rw [Nat.two_mul, card_disjUnion, card_map]

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

Goal state before:
pp: case mp.cons
V : Type u
G : SimpleGraph V
u v u✝ v✝ w✝ : V
h' : G.Adj u✝ v✝
p✝ : G.Walk v✝ w✝
ih : Relation.ReflTransGen G.Adj v✝ w✝
⊢ Relation.ReflTransGen G.Adj u✝ w✝

Tactic:
exact (Relation.ReflTransGen.single h').trans ih

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

Goal state before:
pp: V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
hp : ¬p.Nil
w : V
hw : w ∈ p.support
⊢ w ∈ G.support

Tactic:
by
  obtain ⟨y, hy⟩ := adj_of_mem_walk_support p hp hw
  exact (mem_support G).mpr ⟨y, hy.right⟩

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

Goal state before:
pp: case mp
α : Type u_1
c : Set (Set α)
hc : IsPartition c
y : α
b : Set α
right✝ : ∀ (y_1 : Set α), (fun b ↦ b ∈ c ∧ y ∈ b) y_1 → y_1 = b
hb : b ∈ c
hy : y ∈ b
⊢ {x | (mkClasses c ⋯) x y} ∈ c

Tactic:
rwa [← eq_eqv_class_of_mem _ hb hy]

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex

Goal state before:
pp: V : Type u
G : SimpleGraph V
n : ℕ
⊢ G.chromaticNumber ≤ ↑n + 1 ∧ ¬G.Colorable n ↔ G.Colorable (n + 1) ∧ ¬G.Colorable n

Tactic:
← Nat.cast_add_one,

Goal state after:
V : Type u
G : SimpleGraph V
n : ℕ
⊢ G.chromaticNumber ≤ ↑(n + 1) ∧ ¬G.Colorable n ↔ G.Colorable (n + 1) ∧ ¬G.Colorable n
Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex

Goal state before:
pp: V : Type u
G : SimpleGraph V
m : ℕ
hc : G.Colorable m
⊢ G.Colorable G.chromaticNumber.toNat

Tactic:
rw [hc.chromaticNumber_eq_sInf, Nat.sInf_def]

Goal state after:
V : Type u
G : SimpleGraph V
m : ℕ
hc : G.Colorable m
⊢ G.Colorable (↑(Nat.find ?m.12)).toNat

V : Type u
G : SimpleGraph V
m : ℕ
hc : G.Colorable m
⊢ {n' | G.Colorable n'}.Nonempty
Module: Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected

Goal state before:
pp: case mpr
V : Type u
G : SimpleGraph V
v w u : V
c : G.Walk u u
hc : c.IsCycle
he : s(v, w) ∈ c.edges
hb : ∀ (p : G.Walk v w), s(v, w) ∈ p.edges
hb' : ∀ (p : G.Walk w v), s(w, v) ∈ p.edges
⊢ False

Tactic:
have hvc : v ∈ c.support := Walk.fst_mem_support_of_mem_edges c he

Goal state after:
case mpr
V : Type u
G : SimpleGraph V
v w u : V
c : G.Walk u u
hc : c.IsCycle
he : s(v, w) ∈ c.edges
hb : ∀ (p : G.Walk v w), s(v, w) ∈ p.edges
hb' : ∀ (p : G.Walk w v), s(w, v) ∈ p.edges
hvc : v ∈ c.support
⊢ False
Module: Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex

Goal state before:
pp: V : Type u
G : SimpleGraph V
α : Type u_2
inst✝ : Fintype α
i : ℕ
C : G.Coloring (Fin i)
h : i < card α
⊢ card (Fin i) ≤ card α

Tactic:
by simpa using h.le

Goal state after: