mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk

Goal state before:
pp: α : 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
⊢ ↑(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:
have t : (star hP G ε hU V).product (star hP G ε hV U) ⊆
          (chunk hP G ε hU).parts.product (chunk hP G ε hV).parts :=
        product_subset_product star_subset_chunk star_subset_chunk
      have hε : 0 ≤ ε := by sz_positivity
      have sp : ∀ (a b : Finset (Finset α)), a.product b = a ×ˢ b := fun a b => rfl
      have := add_div_le_sum_sq_div_card t (fun x => (G.edgeDensity x.1 x.2 : ℝ))
        ((G.edgeDensity U V : ℝ) ^ 2 - ε ^ 5 / ↑25) (show 0 ≤ 3 / 4 * ε by linarith) ?_ ?_
      · simp_rw [sp, card_product, card_chunk (m_pos hPα).ne', ← mul_pow, cast_pow, mul_pow,
          div_pow, ← mul_assoc] at this
        norm_num at this
        exact this
      · simp_rw [sp, card_product, card_chunk (m_pos hPα).ne', ← mul_pow]
        simpa using edgeDensity_star_not_uniform hPα hPε hε₁ hUVne hUV
      · rw [sp, card_product]
        apply (edgeDensity_chunk_aux hP hPα hPε hU hV).trans
        · rw [card_chunk (m_pos hPα).ne', card_chunk (m_pos hPα).ne', ← mul_pow]
          simp

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

Goal state before:
pp: α : 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
hU : U ∈ P.parts
hV : V ∈ P.parts
⊢ 16 ^ #P.parts = ↑(#((chunk hP G ε hU).parts ×ˢ (chunk hP G ε hV).parts))

Tactic:
card_product,

Goal state after:
α : 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
hU : U ∈ P.parts
hV : V ∈ P.parts
⊢ 16 ^ #P.parts = ↑(#(chunk hP G ε hU).parts * #(chunk hP G ε hV).parts)
Module: Mathlib.Combinatorics.Colex

Goal state before:
pp: α : Type u_1
inst✝ : PartialOrder α
s t : Colex (Finset α)
⊢ s ≤ t ↔ ↑(ofColex s) \ ↑(ofColex t) ⊆ ↑(lowerClosure (↑(ofColex t) \ ↑(ofColex s)))

Tactic:
by
  simp [le_def, Set.subset_def, and_assoc]

Goal state after:
Module: Mathlib.Combinatorics.Colex

Goal state before:
pp: case refine_1
α : Type u_1
inst✝ : LinearOrder α
s t : Finset α
h : toColex s ≤ toColex t
hst : s ≠ t
m : α := (s ∆ t).max' ⋯
hmt : m ∉ t
hms : m ∈ s
⊢ False

Tactic:
have ⟨b, hbt, hbs, hmb⟩ := h hms hmt

Goal state after:
case refine_1
α : Type u_1
inst✝ : LinearOrder α
s t : Finset α
h : toColex s ≤ toColex t
hst : s ≠ t
m : α := (s ∆ t).max' ⋯
hmt : m ∉ t
hms : m ∈ s
b : α
hbt : b ∈ ofColex (toColex t)
hbs : b ∉ ofColex (toColex s)
hmb : m ≤ b
⊢ False
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
τ : L →+* K
inst✝ : RingHomInvPair σ τ
f : V →ₛₗ[σ] W
hf : Function.Injective ⇑f
u v : ℙ K V
h : map f hf u = map f hf v
⊢ u = v

Tactic:
induction u using ind with | h u hu => induction v using ind with | h v hv =>
  simp only [map_mk, mk_eq_mk_iff'] at h ⊢
  rcases h with ⟨a, ha⟩
  refine ⟨τ a, hf ?_⟩
  rwa [f.map_smulₛₗ, RingHomInvPair.comp_apply_eq₂]

Goal state after:
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
D D' : ℙ K V
⊢ LinearIndependent K ![D.rep, D'.rep] ↔ D ≠ D'

Tactic:
rw [LinearIndependent.pair_iff' (rep_nonzero _)]
    refine ⟨fun h hD ↦ h 1 (by simp [hD]), fun h a hD ↦ h ?_⟩
    rw [eq_comm, ← mk_rep D, ← mk_rep D', mk_eq_mk_iff]
    suffices a ≠ 0 by refine ⟨(Ne.isUnit this).unit, by simp [← hD]⟩
    exact fun ha ↦ D'.rep_nonzero (by simp [← hD, ha])

Goal state after:
Module: Mathlib.Combinatorics.Colex

Goal state before:
pp: case inr.inr.inr
α : Type u_1
inst✝ : LinearOrder α
s t : Finset α
a : α
hcard : #s ≤ #t
ha : a ∈ s
ht : t.Nonempty
m : α := t.min' ht
h' : s ≠ t
w : α
hwt : w ∈ t
hws : w ∉ s
hw : ∀ ⦃a : α⦄, w < a → (a ∈ s ↔ a ∈ t)
haw : a < w
hmw : m < w
⊢ toColex (s.erase a) ≤ toColex (t.erase m)

Tactic:
refine (lt_iff_exists_forall_lt.2 ⟨w, mem_erase.2 ⟨hmw.ne', hwt⟩, mt mem_of_mem_erase hws,
      fun b hbs hbt ↦ ?_⟩).le
    change b ∉ t.erase m at hbt
    rw [mem_erase, not_and_or, not_ne_iff] at hbt
    obtain rfl | hbt := hbt
    · assumption
    · by_contra! hwb
      exact hbt <| (hw <| hwb.lt_of_ne <| ne_of_mem_of_not_mem hwt hbt).1 <| mem_of_mem_erase hbs

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

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
p : α → Prop
inst✝ : DecidablePred p
f : Perm (Subtype p)
hf : f ∈ derangements (Subtype p)
a : α
hfa : a ∈ fixedPoints ⇑↑((Perm.subtypeEquivSubtypePerm p) f)
ha : p a
⊢ False

Tactic:
refine hf ⟨a, ha⟩ (Subtype.ext ?_)
        simp_rw [mem_fixedPoints, IsFixedPt, Perm.subtypeEquivSubtypePerm,
        Equiv.coe_fn_mk, Perm.ofSubtype_apply_of_mem _ ha] at hfa
        assumption

Goal state after:
Module: Mathlib.Combinatorics.Configuration

Goal state before:
pp: case pos
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : Nondegenerate P L
inst✝¹ : Fintype P
inst✝ : Fintype L
h : Fintype.card L ≤ Fintype.card P
t : L → Finset P := fun l ↦ {p | p ∉ l}.toFinset
s : Finset L
hs₀ : ¬#s = 0
hs₁ : ¬#s = 1
hs₂ : #(s.biUnion t)ᶜ ≤ 1
hs₃ : #sᶜ = 0
⊢ #(s.biUnion t)ᶜ ≤ #sᶜ

Tactic:
rw [hs₃, Nat.le_zero]

Goal state after:
case pos
P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : Nondegenerate P L
inst✝¹ : Fintype P
inst✝ : Fintype L
h : Fintype.card L ≤ Fintype.card P
t : L → Finset P := fun l ↦ {p | p ∉ l}.toFinset
s : Finset L
hs₀ : ¬#s = 0
hs₁ : ¬#s = 1
hs₂ : #(s.biUnion t)ᶜ ≤ 1
hs₃ : #sᶜ = 0
⊢ #(s.biUnion t)ᶜ = 0
Module: Mathlib.Combinatorics.Derangements.Exponential

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

Tactic:
refine Finset.sum_congr (refl _) ?_

Goal state after:
s : ℕ → ℝ := fun n ↦ ∑ k ∈ Finset.range n, (-1) ^ k / ↑k.factorial
n : ℕ
⊢ ∀ x ∈ Finset.range (n + 1), (-1) ^ x * ↑((x + 1).ascFactorial (n - x)) / ↑n.factorial = (-1) ^ x / ↑x.factorial
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
⊢ #(treesOfNumNodesEq (i, j).1 ×ˢ treesOfNumNodesEq (i, j).2) = catalan (i, j).1 * catalan (i, j).2

Tactic:
card_product,

Goal state after:
case hi
n : ℕ
ih : ∀ m ≤ n, #(treesOfNumNodesEq m) = catalan m
i j : ℕ
H : (i, j) ∈ antidiagonal n
⊢ #(treesOfNumNodesEq (i, j).1) * #(treesOfNumNodesEq (i, j).2) = catalan (i, j).1 * catalan (i, j).2
Module: Mathlib.Combinatorics.Enumerative.DyckWord

Goal state before:
pp: p : DyckWord
h : ↑p ≠ []
f : ¬(↑p).getLast h = D
s : count U (take ((↑p).length - 1) ↑p) + 1 = count D (take ((↑p).length - 1) ↑p) + 0
⊢ False

Tactic:
have := p.count_D_le_count_U (p.toList.length - 1)

Goal state after:
p : DyckWord
h : ↑p ≠ []
f : ¬(↑p).getLast h = D
s : count U (take ((↑p).length - 1) ↑p) + 1 = count D (take ((↑p).length - 1) ↑p) + 0
this : count D (take ((↑p).length - 1) ↑p) ≤ count U (take ((↑p).length - 1) ↑p)
⊢ False
Module: Mathlib.Combinatorics.Enumerative.Bell

Goal state before:
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:
simp [Finset.mem_erase.mp hj]

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

Goal state before:
pp: p : DyckWord
h : p ≠ 0
⊢ 0 < (range (↑p).length).length

Tactic:
rw [length_range, length_pos_iff]
    exact toList_ne_nil.mpr h

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

Goal state before:
pp: p q : DyckWord
h : p ≠ 0
⊢ (if h : p + q = 0 then 0 else ((p + q).take ((p + q).firstReturn + 1) ⋯).denest ⋯) =
    if h : p = 0 then 0 else (p.take (p.firstReturn + 1) ⋯).denest ⋯

Tactic:
firstReturn_add,

Goal state after:
p q : DyckWord
h : p ≠ 0
⊢ (if h : p + q = 0 then 0 else ((p + q).take ((if p = 0 then q.firstReturn else p.firstReturn) + 1) ⋯).denest ⋯) =
    if h : p = 0 then 0 else (p.take (p.firstReturn + 1) ⋯).denest ⋯
Module: Mathlib.Combinatorics.Enumerative.DyckWord

Goal state before:
pp: p q : DyckWord
h : p ≠ 0
⊢ (if h : p + q = 0 then 0 else (p + q).drop ((p + q).firstReturn + 1) ⋯) =
    (if h : p = 0 then 0 else p.drop (p.firstReturn + 1) ⋯) + q

Tactic:
firstReturn_add,

Goal state after:
p q : DyckWord
h : p ≠ 0
⊢ (if h : p + q = 0 then 0 else (p + q).drop ((if p = 0 then q.firstReturn else p.firstReturn) + 1) ⋯) =
    (if h : p = 0 then 0 else p.drop (p.firstReturn + 1) ⋯) + q
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 b : ℕ
hn : b ∈ range (m - 1)
⊢ X ^ ((i + 1) * (1 + b)) = (if b + 1 < m then 1 else 0) • X ^ ((i + 1) * (b + 1))

Tactic:
add_comm 1 b

Goal state after:
R : Type u_1
inst✝² : TopologicalSpace R
inst✝¹ : T2Space R
inst✝ : CommSemiring R
m : ℕ
hm : 0 < m
a✝ : Nontrivial R
i b : ℕ
hn : b ∈ range (m - 1)
⊢ X ^ ((i + 1) * (b + 1)) = (if b + 1 < m then 1 else 0) • X ^ ((i + 1) * (b + 1))
Module: Mathlib.Combinatorics.Additive.VerySmallDoubling

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
K : ℝ
A S : Finset G
hK : K < 1
hS : S.Nonempty
hA : A.Nonempty
⊢ 0 < expansion K S A

Tactic:
by
  have : (0 : ℝ) < #A := by simp [hA]
  nlinarith [mul_card_le_expansion (K := K) hS (A := A)]

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

Goal state before:
pp: n k : ℕ
hk : n + 1 < k + 1
⊢ n * 0 + 0 = 0

Tactic:
mul_zero

Goal state after:
n k : ℕ
hk : n + 1 < k + 1
⊢ 0 + 0 = 0
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)
⊢ (2 * n + 1) * rothNumberNat n = Fintype.card α * addRothNumber (Iio ⟨n, ⋯⟩)

Tactic:
rw [Fin.addRothNumber_eq_rothNumberNat (by simp), Fintype.card_fin]

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

Goal state before:
pp: ⊢ (fun n ↦ ↑n ^ 2 * rexp (-4 * √(Real.log ↑n))) =O[atTop] fun n ↦
    (↑n / 3 - 2) * ↑((n - 3) / 6) * rexp (-4 * √(Real.log ↑((n - 3) / 6)))

Tactic:
simp_rw [sq]
    refine (IsBigO.mul ?_ ?_).mul ?_
    · trans fun n ↦ n / 3
      · simp_rw [div_eq_inv_mul]
        exact (isBigO_refl ..).const_mul_right (by simp)
      refine IsLittleO.right_isBigO_sub ?_
      simpa [div_eq_inv_mul, Function.comp_def] using
        .atTop_of_const_mul₀ zero_lt_three (by simp [tendsto_natCast_atTop_atTop])
    · rw [IsBigO_def]
      refine ⟨12, ?_⟩
      simp only [IsBigOWith, norm_natCast, eventually_atTop]
      exact ⟨15, fun x hx ↦ by norm_cast; lia⟩
    · rw [isBigO_exp_comp_exp_comp]
      refine ⟨0, ?_⟩
      simp only [neg_mul, eventually_map, Pi.sub_apply, sub_neg_eq_add, neg_add_le_iff_le_add,
        add_zero, eventually_atTop]
      refine ⟨9, fun x hx ↦ ?_⟩
      gcongr
      · simp
        lia
      · lia

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

Goal state before:
pp: α : Type u_1
M : Matroid α
C D : Set α
hE : (M.E ⊆ M.E ∧ Disjoint M.E C) ∧ Disjoint M.E D
⊢ M = M ／ C ＼ D

Tactic:
rw [← contract_inter_ground_eq, hE.1.2.symm.inter_eq, contract_empty, ← delete_inter_ground_eq,
    hE.2.symm.inter_eq, delete_empty]

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

Goal state before:
pp: case neg
σ : 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
j : ι
hj : ¬j = i
⊢ m.toSyn (m.degree (b j * (Finsupp.single i (⋯.unit⁻¹ • f)) j)) ≤ m.toSyn (m.degree f)

Tactic:
simp only [Finsupp.single_eq_of_ne hj, mul_zero, degree_zero, map_zero]

Goal state after:
case neg
σ : 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
j : ι
hj : ¬j = i
⊢ 0 ≤ m.toSyn (m.degree f)
Module: Mathlib.RingTheory.MvPolynomial.Groebner

Goal state before:
pp: case h.right.right
σ : 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
hf : ∀ (i : ι), ¬m.degree (b i) ≤ m.degree f
g' : ι →₀ MvPolynomial σ R
r' : MvPolynomial σ R
H' :
  m.subLTerm f = (Finsupp.linearCombination (MvPolynomial σ R) b) g' + r' ∧
    (∀ (i : ι), m.toSyn (m.degree (b i * g' i)) ≤ m.toSyn (m.degree (m.subLTerm f))) ∧
      ∀ c ∈ r'.support, ∀ (i : ι), ¬m.degree (b i) ≤ c
⊢ ∀ c ∈ (r' + (monomial (m.degree f)) (m.leadingCoeff f)).support, ∀ (i : ι), ¬m.degree (b i) ≤ c

Tactic:
intro c

Goal state after:
case h.right.right
σ : 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
hf : ∀ (i : ι), ¬m.degree (b i) ≤ m.degree f
g' : ι →₀ MvPolynomial σ R
r' : MvPolynomial σ R
H' :
  m.subLTerm f = (Finsupp.linearCombination (MvPolynomial σ R) b) g' + r' ∧
    (∀ (i : ι), m.toSyn (m.degree (b i * g' i)) ≤ m.toSyn (m.degree (m.subLTerm f))) ∧
      ∀ c ∈ r'.support, ∀ (i : ι), ¬m.degree (b i) ≤ c
c : σ →₀ ℕ
⊢ c ∈ (r' + (monomial (m.degree f)) (m.leadingCoeff f)).support → ∀ (i : ι), ¬m.degree (b i) ≤ c
Module: Mathlib.Combinatorics.Quiver.ConnectedComponent

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

Tactic:
by
  constructor
  · intro h_singleton w hw_ne h_bidir
    obtain ⟨hab, hba⟩ := h_bidir
    have h_same_scc : (w : StronglyConnectedComponent V) = v :=
      stronglyConnectedComponent_eq_of_path (a := w) (b := v) hba hab
    obtain ⟨rfl⟩ := h_singleton w h_same_scc
    contradiction
  · intro h_no_bidir w h_same_scc
    by_contra hw_ne
    obtain ⟨hab, hba⟩ :=
      exists_path_of_stronglyConnectedComponent_eq (a := w) (b := v) h_same_scc
    exact (h_no_bidir w hw_ne) ⟨hba, hab⟩

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) (f - (linearCombination (MvPolynomial σ R) fun i ↦ Alon.P (S i) i) h) = 0

Tactic:
map_sub,

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) f - (eval x) ((linearCombination (MvPolynomial σ R) fun i ↦ Alon.P (S i) i) h) = 0
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
i : σ
a✝ : i ∈ h.support
⊢ (eval x) (h i * Alon.P (S i) i) = 0

Tactic:
map_mul

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
i : σ
a✝ : i ∈ h.support
⊢ (eval x) (h i) * (eval x) (Alon.P (S i) i) = 0
Module: Mathlib.Combinatorics.Quiver.Covering

Goal state before:
pp: U : Type u_1
inst✝¹ : Quiver U
V : Type u_2
inst✝ : Quiver V
φ : U ⥤q V
hφ : ∀ (u : U), Injective (φ.star u)
u v₁ x₁ y₁ : U
p₁ : Path u x₁
e₁ : x₁ ⟶ y₁
ih :
  ∀ ⦃a₂ : PathStar u⦄,
    (fun p ↦ ⟨φ.obj p.fst, φ.mapPath p.snd⟩) ⟨x₁, p₁⟩ = (fun p ↦ ⟨φ.obj p.fst, φ.mapPath p.snd⟩) a₂ → ⟨x₁, p₁⟩ = a₂
y₂ : U
hφy : φ.obj y₁ = φ.obj y₂
e₂ : x₁ ⟶ y₂
hφx : φ.obj x₁ = φ.obj x₁
hφe : φ.map e₁ ≍ φ.map e₂
h' : (φ.mapPath p₁).cons (Hom.cast ⋯ hφy (φ.map e₁)) = (φ.mapPath p₁).cons (φ.map e₂)
hφp : φ.mapPath p₁ ≍ φ.mapPath p₁
h_path_star : φ.pathStar u ⟨x₁, p₁⟩ = φ.pathStar u ⟨x₁, p₁⟩
⊢ φ.star x₁ ⟨y₁, e₁⟩ = φ.star x₁ ⟨y₂, e₂⟩

Tactic:
simp only [Prefunctor.star_apply, Sigma.mk.inj_iff]

Goal state after:
U : Type u_1
inst✝¹ : Quiver U
V : Type u_2
inst✝ : Quiver V
φ : U ⥤q V
hφ : ∀ (u : U), Injective (φ.star u)
u v₁ x₁ y₁ : U
p₁ : Path u x₁
e₁ : x₁ ⟶ y₁
ih :
  ∀ ⦃a₂ : PathStar u⦄,
    (fun p ↦ ⟨φ.obj p.fst, φ.mapPath p.snd⟩) ⟨x₁, p₁⟩ = (fun p ↦ ⟨φ.obj p.fst, φ.mapPath p.snd⟩) a₂ → ⟨x₁, p₁⟩ = a₂
y₂ : U
hφy : φ.obj y₁ = φ.obj y₂
e₂ : x₁ ⟶ y₂
hφx : φ.obj x₁ = φ.obj x₁
hφe : φ.map e₁ ≍ φ.map e₂
h' : (φ.mapPath p₁).cons (Hom.cast ⋯ hφy (φ.map e₁)) = (φ.mapPath p₁).cons (φ.map e₂)
hφp : φ.mapPath p₁ ≍ φ.mapPath p₁
h_path_star : φ.pathStar u ⟨x₁, p₁⟩ = φ.pathStar u ⟨x₁, p₁⟩
⊢ φ.obj y₁ = φ.obj y₂ ∧ φ.map e₁ ≍ φ.map e₂
Module: Mathlib.Combinatorics.Nullstellensatz

Goal state before:
pp: case neg
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 σ := ⋯
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 := ⋯
hg : g = h i * Alon.P (S i) i
hi : ¬h i = 0
this : (h i).totalDegree + #(S i) ≤ Finsupp.degree t
p q : σ →₀ ℕ
hpq : p + q = t
hq✝ : q ∈ (∏ r ∈ S i, (X i - C r)).support
e : ℕ
hq' : e ≤ #(S i)
hq : q = single i e
⊢ (h i).totalDegree < ∑ i ∈ p.support, p i

Tactic:
← Finsupp.degree_apply

Goal state after:
case neg
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
this : (h i).totalDegree + #(S i) ≤ Finsupp.degree t
p q : σ →₀ ℕ
hpq : p + q = t
hq✝ : q ∈ (∏ r ∈ S i, (X i - C r)).support
e : ℕ
hq' : e ≤ #(S i)
hq : q = single i e
⊢ (h i).totalDegree < Finsupp.degree p
Module: Mathlib.Combinatorics.SetFamily.AhlswedeZhang

Goal state before:
pp: m n : ℕ
h : n < m
f : ℕ → ℚ := fun i ↦ ↑(n.choose i) * (↑(m.choose i))⁻¹
hf : f = fun i ↦ ↑(n.choose i) * (↑(m.choose i))⁻¹
i : ℕ
h₁✝ : i < n + 1
h₁ : i ≤ n
h₂ : i < m
h₃ : i ≤ m
hi₄ : ↑i + 1 ≠ 0
this : ↑(m.choose (i + 1)) * (↑i + 1) = ↑(m.choose i) * ↑(m - i)
⊢ ↑(n.choose i) * (↑(m.choose i))⁻¹ - ↑(n.choose (i + 1)) * (↑(m.choose (i + 1)))⁻¹ =
    ↑(n.choose i) * (↑m - ↑n) / ((↑m - ↑i) * ↑(m.choose i))

Tactic:
rw [(eq_mul_inv_iff_mul_eq₀ hi₄).mpr this]

Goal state after:
m n : ℕ
h : n < m
f : ℕ → ℚ := fun i ↦ ↑(n.choose i) * (↑(m.choose i))⁻¹
hf : f = fun i ↦ ↑(n.choose i) * (↑(m.choose i))⁻¹
i : ℕ
h₁✝ : i < n + 1
h₁ : i ≤ n
h₂ : i < m
h₃ : i ≤ m
hi₄ : ↑i + 1 ≠ 0
this : ↑(m.choose (i + 1)) * (↑i + 1) = ↑(m.choose i) * ↑(m - i)
⊢ ↑(n.choose i) * (↑(m.choose i))⁻¹ - ↑(n.choose (i + 1)) * (↑(m.choose i) * ↑(m - i) * (↑i + 1)⁻¹)⁻¹ =
    ↑(n.choose i) * (↑m - ↑n) / ((↑m - ↑i) * ↑(m.choose i))
Module: Mathlib.Combinatorics.SetFamily.AhlswedeZhang

Goal state before:
pp: m n : ℕ
h : n < m
f : ℕ → ℚ := fun i ↦ ↑(n.choose i) * (↑(m.choose i))⁻¹
hf : f = fun i ↦ ↑(n.choose i) * (↑(m.choose i))⁻¹
i : ℕ
h₁✝ : i < n + 1
h₁ : i ≤ n
h₂ : i < m
h₃ : i ≤ m
hi₄ : ↑i + 1 ≠ 0
this✝ : ↑(m.choose (i + 1)) * (↑i + 1) = ↑(m.choose i) * ↑(m - i)
this : ↑(n.choose (i + 1)) * (↑i + 1) = ↑(n.choose i) * ↑(n - i)
⊢ ↑(n.choose i) * (↑(m.choose i))⁻¹ - ↑(n.choose (i + 1)) * (↑(m.choose i) * ↑(m - i) * (↑i + 1)⁻¹)⁻¹ =
    ↑(n.choose i) * (↑m - ↑n) / ((↑m - ↑i) * ↑(m.choose i))

Tactic:
rw [(eq_mul_inv_iff_mul_eq₀ hi₄).mpr this]

Goal state after:
m n : ℕ
h : n < m
f : ℕ → ℚ := fun i ↦ ↑(n.choose i) * (↑(m.choose i))⁻¹
hf : f = fun i ↦ ↑(n.choose i) * (↑(m.choose i))⁻¹
i : ℕ
h₁✝ : i < n + 1
h₁ : i ≤ n
h₂ : i < m
h₃ : i ≤ m
hi₄ : ↑i + 1 ≠ 0
this✝ : ↑(m.choose (i + 1)) * (↑i + 1) = ↑(m.choose i) * ↑(m - i)
this : ↑(n.choose (i + 1)) * (↑i + 1) = ↑(n.choose i) * ↑(n - i)
⊢ ↑(n.choose i) * (↑(m.choose i))⁻¹ -
      ↑(n.choose i) * ↑(n - i) * (↑i + 1)⁻¹ * (↑(m.choose i) * ↑(m - i) * (↑i + 1)⁻¹)⁻¹ =
    ↑(n.choose i) * (↑m - ↑n) / ((↑m - ↑i) * ↑(m.choose i))