mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Combinatorics.Enumerative.Catalan.Basic

Goal state before:
pp: d : ℕ
hd : ∀ m ≤ d, ↑(catalan m) = ↑m.centralBinom / (↑m + 1)
⊢ gosperCatalan (d + 1) (d + 1) - gosperCatalan (d + 1) 0 = ↑(d + 1).centralBinom / (↑(d + 1) + 1)

Tactic:
gosper_catalan_sub_eq_central_binom_div d

Goal state after:
d : ℕ
hd : ∀ m ≤ d, ↑(catalan m) = ↑m.centralBinom / (↑m + 1)
⊢ ↑(d + 1).centralBinom / (↑d + 2) = ↑(d + 1).centralBinom / (↑(d + 1) + 1)
Module: Mathlib.Combinatorics.Enumerative.Bell

Goal state before:
pp: case e'_2.e'_5.e'_6
m n : ℕ
hn : n ≠ 0
⊢ n ! ^ m = (map (fun j ↦ j !) (replicate m n)).prod

Tactic:
simp only [map_replicate, prod_replicate]

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
⊢ ∏ a ∈ p.parts.toFinset, f a ((Multiset.toFinsupp p.parts) a) =
    ∏ i ∈ s, (coeff (p.toFinsuppAntidiag i)) (1 + ∑' (j : ℕ), f i (j + 1) • X ^ (i * (j + 1)))

Tactic:
Multiset.toFinsupp_apply

Goal state after:
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
⊢ ∏ a ∈ p.parts.toFinset, f a (Multiset.count a p.parts) =
    ∏ i ∈ s, (coeff (p.toFinsuppAntidiag i)) (1 + ∑' (j : ℕ), f i (j + 1) • X ^ (i * (j + 1)))
Module: Mathlib.Combinatorics.Additive.VerySmallDoubling

Goal state before:
pp: G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
K : ℝ
A : Finset G
hK₁ : 1 < K
hKφ : K < φ
hA₁ : ↑(#(A⁻¹ * A)) ≤ K * ↑(#A)
hA₂ : ↑(#(A * A⁻¹)) ≤ K * ↑(#A)
K_pos hK₀ : 0 < K
hKφ' : 0 < φ - K
hKψ' : 0 < K - ψ
hK₂' : 0 < 2 - K
const_pos : 0 < K * (2 - K) / ((φ - K) * (K - ψ))
A_nonempty : A.Nonempty
S : Finset G := A * A⁻¹
H : Subgroup G := stabilizer G S
S_nonempty : S.Nonempty
this✝ : Finite ↥H
val✝ : Fintype ↥H
H_mul_S : ↑H * ↑S = ↑S
Z : Finset G
hZ : Z ⊆ S ∧ ↑H * ↑Z = ↑H * ↑S ∧ Set.InjOn (fun x ↦ ↑H <• x) ↑Z
H_mul_Z : ↑H * ↑Z = ↑S
H_toFinset_mul_Z : (↑H).toFinset * Z = S
card_H_mul_card_Z : Fintype.card ↥H * #Z = #S
r : G → ℕ := fun z ↦ A.convolution A⁻¹ z
r_inv : ∀ (z : G), r z⁻¹ = r z
z : G
hz : z ∈ S
w : G
hw : w ∈ S
hrz : (K - 1) * ↑(#A) < ↑(#(A ∩ z⁻¹ •> A))
hrw : (2 - K) * ↑(#A) ≤ ↑(#(A ∩ w •> A))
this : ↑(#(A ∩ z⁻¹ •> A ∩ (A ∩ w •> A))) ≤ ↑(#(z⁻¹ •> A ∩ w •> A))
⊢ 0 < ↑(#(z⁻¹ •> A ∩ w •> A))

Tactic:
have : (#((A ∩ z⁻¹ •> A) ∪ (A ∩ w •> A)) : ℝ) ≤ #A := by
        gcongr; exact union_subset inter_subset_left inter_subset_left

Goal state after:
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
K : ℝ
A : Finset G
hK₁ : 1 < K
hKφ : K < φ
hA₁ : ↑(#(A⁻¹ * A)) ≤ K * ↑(#A)
hA₂ : ↑(#(A * A⁻¹)) ≤ K * ↑(#A)
K_pos hK₀ : 0 < K
hKφ' : 0 < φ - K
hKψ' : 0 < K - ψ
hK₂' : 0 < 2 - K
const_pos : 0 < K * (2 - K) / ((φ - K) * (K - ψ))
A_nonempty : A.Nonempty
S : Finset G := A * A⁻¹
H : Subgroup G := stabilizer G S
S_nonempty : S.Nonempty
this✝¹ : Finite ↥H
val✝ : Fintype ↥H
H_mul_S : ↑H * ↑S = ↑S
Z : Finset G
hZ : Z ⊆ S ∧ ↑H * ↑Z = ↑H * ↑S ∧ Set.InjOn (fun x ↦ ↑H <• x) ↑Z
H_mul_Z : ↑H * ↑Z = ↑S
H_toFinset_mul_Z : (↑H).toFinset * Z = S
card_H_mul_card_Z : Fintype.card ↥H * #Z = #S
r : G → ℕ := fun z ↦ A.convolution A⁻¹ z
r_inv : ∀ (z : G), r z⁻¹ = r z
z : G
hz : z ∈ S
w : G
hw : w ∈ S
hrz : (K - 1) * ↑(#A) < ↑(#(A ∩ z⁻¹ •> A))
hrw : (2 - K) * ↑(#A) ≤ ↑(#(A ∩ w •> A))
this✝ : ↑(#(A ∩ z⁻¹ •> A ∩ (A ∩ w •> A))) ≤ ↑(#(z⁻¹ •> A ∩ w •> A))
this : ↑(#(A ∩ z⁻¹ •> A ∪ A ∩ w •> A)) ≤ ↑(#A)
⊢ 0 < ↑(#(z⁻¹ •> A ∩ w •> A))
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 : (A ∩ B).Nonempty
⊢ A = B

Tactic:
by
  replace hAB := hA.isFragment.inter hK hS hB.isFragment hAB
  replace hA := hA.2 hAB <| by grw [inter_subset_left]
  replace hB := hB.2 hAB <| by grw [inter_subset_right]
  replace hA := eq_of_subset_of_card_le inter_subset_left hA
  replace hB := eq_of_subset_of_card_le inter_subset_right hB
  exact hA.symm.trans hB

Goal state after:
Module: Mathlib.Combinatorics.HalesJewett

Goal state before:
pp: case pos
κ : Type (max v u)
inst✝ : Finite κ
h : Nonempty κ
⊢ ∃ ι x, ∀ (C : (ι → PEmpty.{u + 1}) → κ), ∃ l, IsMono C l

pp: case neg
κ : Type (max v u)
inst✝ : Finite κ
h : ¬Nonempty κ
⊢ ∃ ι x, ∀ (C : (ι → PEmpty.{u + 1}) → κ), ∃ l, IsMono C l

Tactic:
· refine ⟨Unit, inferInstance, fun C => ⟨default, Classical.arbitrary _, PEmpty.rec⟩⟩

Goal state after:
case neg
κ : Type (max v u)
inst✝ : Finite κ
h : ¬Nonempty κ
⊢ ∃ ι x, ∀ (C : (ι → PEmpty.{u + 1}) → κ), ∃ l, IsMono C l
Module: Mathlib.Combinatorics.Matroid.Minor.Delete

Goal state before:
pp: α : Type u_1
M N : Matroid α
X : Set α
h : N ≤r M
hX : Disjoint X N.E
⊢ N ≤r M ＼ X

Tactic:
obtain ⟨D, hD, rfl⟩ := isRestriction_iff_exists_eq_delete.1 h

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

Goal state before:
pp: case zero
M : Type u_1
inst✝ : Semigroup M
a : Stream' M
⊢ a.get 0 ∈ FP a

Tactic:
exact FP.head _

Goal state after:
Module: Mathlib.Combinatorics.Hindman

Goal state before:
pp: case H.inl
M : Type u_1
inst✝ : CommMonoid M
a : Stream' M
s : Finset ℕ
ih :
  ∀ s_1 ∈ s, ∀ (hs : (s.erase s_1).Nonempty), ∏ i ∈ s.erase s_1, a.get i ∈ FP (Stream'.drop ((s.erase s_1).min' hs) a)
hs : s.Nonempty
h : s.erase (s.min' hs) = ∅
⊢ (Stream'.drop (s.min' hs) a).head ∈ FP (Stream'.drop (s.min' hs) a)

Tactic:
exact FP.head _

Goal state after:
Module: Mathlib.Combinatorics.KatonaCircle

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

Tactic:
simp +contextual [Prod.ext_iff, DFunLike.ext_iff]

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
⊢ (Multiset.map AlmostMono.color
      ({ line := vertical s.focus (map some l'), color := C' s.focus, has_color := ⋯ } ::ₘ
        Multiset.map (fun p ↦ { line := p.line.prod (map some l'), color := p.color, has_color := ⋯ }) s.lines)).Nodup

Tactic:
rw [Multiset.map_cons, Multiset.map_map, Multiset.nodup_cons, Multiset.mem_map]

Goal state after:
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
Module: Mathlib.RingTheory.MvPolynomial.Groebner

Goal state before:
pp: case hnc
σ : 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
⊢ ¬↑hb.unit⁻¹ * m.leadingCoeff f = 0

Tactic:
simp only [Units.mul_right_eq_zero, leadingCoeff_eq_zero_iff]
      intro hf0
      apply hf
      simp [hf0]

Goal state after:
Module: Mathlib.Combinatorics.HalesJewett

Goal state before:
pp: case neg.refine_5
α : 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
⊢ {
          lines :=
            { line := vertical s.focus (map some l'), color := C' s.focus, has_color := ⋯ } ::ₘ
              Multiset.map (fun p ↦ { line := p.line.prod (map some l'), color := p.color, has_color := ⋯ }) s.lines,
          focus := Sum.elim s.focus (↑(map some l') none), is_focused := ⋯, distinct_colors := ⋯ }.lines.card =
    r + 1

Tactic:
Multiset.card_cons,

Goal state after:
case neg.refine_5
α : 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
⊢ (Multiset.map (fun p ↦ { line := p.line.prod (map some l'), color := p.color, has_color := ⋯ }) s.lines).card + 1 =
    r + 1
Module: Mathlib.Combinatorics.HalesJewett

Goal state before:
pp: case refine_3
M : Type u_5
κ : Type u_6
inst✝¹ : AddCommMonoid M
S : Finset M
inst✝ : Finite κ
C : M → κ
ι : Type
_inst : Fintype ι
l : Line (↥S) ι
c : κ
s : Finset ι := {i | l.idxFun i = none}
hs : s = {i | l.idxFun i = none}
x : M
xs : x ∈ S
⊢ #s • x + ∑ i ∈ sᶜ, (Option.map (fun m ↦ ↑m) (l.idxFun i)).getD 0 =
    ∑ i ∈ s, ↑(↑l ⟨x, xs⟩ i) + ∑ i ∈ sᶜ, ↑(↑l ⟨x, xs⟩ i)

Tactic:
congr 1

Goal state after:
case refine_3.e_a
M : Type u_5
κ : Type u_6
inst✝¹ : AddCommMonoid M
S : Finset M
inst✝ : Finite κ
C : M → κ
ι : Type
_inst : Fintype ι
l : Line (↥S) ι
c : κ
s : Finset ι := {i | l.idxFun i = none}
hs : s = {i | l.idxFun i = none}
x : M
xs : x ∈ S
⊢ #s • x = ∑ i ∈ s, ↑(↑l ⟨x, xs⟩ i)

case refine_3.e_a
M : Type u_5
κ : Type u_6
inst✝¹ : AddCommMonoid M
S : Finset M
inst✝ : Finite κ
C : M → κ
ι : Type
_inst : Fintype ι
l : Line (↥S) ι
c : κ
s : Finset ι := {i | l.idxFun i = none}
hs : s = {i | l.idxFun i = none}
x : M
xs : x ∈ S
⊢ ∑ i ∈ sᶜ, (Option.map (fun m ↦ ↑m) (l.idxFun i)).getD 0 = ∑ i ∈ sᶜ, ↑(↑l ⟨x, xs⟩ i)
Module: Mathlib.Combinatorics.Nullstellensatz

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
σ✝ : Type u_2
inst✝² : Finite σ✝
inst✝¹ : IsDomain R
σ : Type u_2
inst✝ : Fintype σ
h :
  ∀ (P : MvPolynomial σ R) (S : σ → Finset R),
    (∀ (i : σ), degreeOf i P < #(S i)) → (∀ (x : σ → R), (∀ (i : σ), x i ∈ S i) → (eval x) P = 0) → P = 0
P : MvPolynomial (Option σ) R
S : Option σ → Finset R
Hdeg : ∀ (i : Option σ), degreeOf i P < #(S i)
Heval : ∀ (x : Option σ → R), (∀ (i : Option σ), x i ∈ S i) → (eval x) P = 0
Q : Polynomial (MvPolynomial σ R) := (optionEquivLeft R σ) P
hQ : Q = (optionEquivLeft R σ) P
x : σ → R
hx : ∀ (i : σ), x i ∈ S (Option.some i)
d : ℕ
hd : degreeOf none P < d
⊢ (eval x) (((optionEquivLeft R σ) P).coeff d) = 0

Tactic:
convert! map_zero (MvPolynomial.eval x)

Goal state after:
R : Type u_1
inst✝³ : CommRing R
σ✝ : Type u_2
inst✝² : Finite σ✝
inst✝¹ : IsDomain R
σ : Type u_2
inst✝ : Fintype σ
h :
  ∀ (P : MvPolynomial σ R) (S : σ → Finset R),
    (∀ (i : σ), degreeOf i P < #(S i)) → (∀ (x : σ → R), (∀ (i : σ), x i ∈ S i) → (eval x) P = 0) → P = 0
P : MvPolynomial (Option σ) R
S : Option σ → Finset R
Hdeg : ∀ (i : Option σ), degreeOf i P < #(S i)
Heval : ∀ (x : Option σ → R), (∀ (i : Option σ), x i ∈ S i) → (eval x) P = 0
Q : Polynomial (MvPolynomial σ R) := (optionEquivLeft R σ) P
hQ : Q = (optionEquivLeft R σ) P
x : σ → R
hx : ∀ (i : σ), x i ∈ S (Option.some i)
d : ℕ
hd : degreeOf none P < d
⊢ ((optionEquivLeft R σ) P).coeff d = 0
Module: Mathlib.Combinatorics.Matroid.Minor.Contract

Goal state before:
pp: α : Type u_1
R C : Set α
M : Matroid α
h : Disjoint C R
⊢ M ／ C ↾ R = (M ↾ (R ∪ C)) ／ C

Tactic:
refine ext_indep (by simp [h.sdiff_eq_right]) fun I (hI : I ⊆ R) ↦ ?_
  obtain ⟨J, hJ⟩ := (M ↾ (R ∪ C)).exists_isBasis' C
  have hJ' : M.IsBasis' J C := by
    simpa [inter_eq_self_of_subset_left subset_union_right] using (isBasis'_restrict_iff.1 hJ).1
  rw [restrict_indep_iff, hJ.contract_indep_iff, hJ'.contract_indep_iff, restrict_indep_iff]
  have hJC := hJ'.subset
  tauto_set

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

Goal state before:
pp: α : Type u_1
M : Matroid α
D C : Set α
⊢ M ＼ D ／ C = M ／ (C \ D) ＼ D

Tactic:
rw [delete_contract_eq_sdiff, ← contract_delete_comm _ disjoint_sdiff_left]

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
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 + 0
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
this : r = 0
⊢ (∀ (i : σ), ((∏ s ∈ S i, (X i - C s)) * h i).totalDegree ≤ f.totalDegree) ∧
    f = (linearCombination (MvPolynomial σ R) fun i ↦ ∏ r ∈ S i, (X i - C r)) h

Tactic:
add_zero

Goal state after:
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
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
this : r = 0
⊢ (∀ (i : σ), ((∏ s ∈ S i, (X i - C s)) * h i).totalDegree ≤ f.totalDegree) ∧
    f = (linearCombination (MvPolynomial σ R) fun i ↦ ∏ r ∈ S i, (X i - C r)) h
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) r = 0

Tactic:
← hf,

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 - (linearCombination (MvPolynomial σ R) fun i ↦ Alon.P (S i) i) h) = 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
inst✝² : HasInvolutiveReverse U
inst✝¹ : HasInvolutiveReverse V
inst✝ : φ.MapReverse
u : U
⊢ φ.costar u = ⇑(starEquivCostar (φ.obj u)) ∘ φ.star u ∘ ⇑(starEquivCostar u).symm

Tactic:
ext ⟨v, f⟩ <;> simp

Goal state after:
Module: Mathlib.Combinatorics.Schnirelmann

Goal state before:
pp: case inr
A : Finset ℕ
ε : ℝ
hε : 0 < ε
this : ∀ (ε : ℝ), 0 < ε → ε ≤ 1 → ∃ n, 0 < n ∧ ↑(#({a ∈ Ioc 0 n | a ∈ ↑A})) / ↑n < ε
hε₁ : ¬ε ≤ 1
⊢ ∃ n, 0 < n ∧ ↑(#({a ∈ Ioc 0 n | a ∈ ↑A})) / ↑n < ε

Tactic:
obtain ⟨n, hn, hn'⟩ := this 1 zero_lt_one le_rfl
    exact ⟨n, hn, hn'.trans_le (le_of_not_ge hε₁)⟩

Goal state after:
Module: Mathlib.Combinatorics.Schnirelmann

Goal state before:
pp: m : ℕ
hm : m ≠ 1
hm' : m > 0
⊢ ↑(#({a ∈ Ioc 0 m | a ∈ {n | n % m = 1}})) / ↑m ≤ 1 / ↑m

Tactic:
← @Nat.cast_one ℝ

Goal state after:
m : ℕ
hm : m ≠ 1
hm' : m > 0
⊢ ↑(#({a ∈ Ioc 0 m | a ∈ {n | n % m = 1}})) / ↑m ≤ ↑1 / ↑m
Module: Mathlib.Combinatorics.Schnirelmann

Goal state before:
pp: A B : Set ℕ
inst✝¹ : DecidablePred fun x ↦ x ∈ A
inst✝ : DecidablePred fun x ↦ x ∈ B
hA : 0 ∈ A
hB : 0 ∈ B
h : 1 ≤ schnirelmannDensity A + schnirelmannDensity B
m : ℕ
n : ℕ := m + 1
hnA : n ∉ A
hnB : n ∉ B
f : ℕ ⊕ ℕ → ℕ :=
  fun x ↦
    match x with
    | Sum.inl x => x
    | Sum.inr y => n - y
sA : Finset ℕ := {a ∈ Ioc 0 n | a ∈ A}
sB : Finset ℕ := {b ∈ Ioc 0 n | b ∈ B}
⊢ n ≤ #(sA.disjSum sB)

Tactic:
rw [card_disjSum]
      rify
      nlinarith [@schnirelmannDensity_mul_le_card_filter A _ n,
        @schnirelmannDensity_mul_le_card_filter B _ n]

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

Goal state before:
pp: α : Type u_2
inst✝³ : DecidableEq α
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : DecidableRel Disjoint
t : Finset α
⊢ ∅ ○ t = ∅

Tactic:
by simp [disjSups]

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

Goal state before:
pp: α : Type u_2
inst✝³ : DecidableEq α
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : DecidableRel Disjoint
s : Finset α
⊢ s ○ ∅ = ∅

Tactic:
by simp [disjSups]

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
t✝ t : Finset α
x✝ : t ∈ 𝒜
hst : t✝ ⊆ t
⊢ #(t \ t✝) = 1 ↔ #t = #t✝ + 1

Tactic:
rw [card_sdiff_of_subset hst, tsub_eq_iff_eq_add_of_le, add_comm]

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
t✝ t : Finset α
x✝ : t ∈ 𝒜
hst : t✝ ⊆ t
⊢ #t✝ ≤ #t
Module: Mathlib.Combinatorics.SetFamily.Shadow

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
t✝ : Finset α
k : ℕ
t : Finset α
x✝ : t ∈ 𝒜
hst : t✝ ⊆ t
⊢ #(t \ t✝) = k ↔ #t = #t✝ + k

Tactic:
rw [card_sdiff_of_subset hst, tsub_eq_iff_eq_add_of_le, add_comm]

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
t✝ : Finset α
k : ℕ
t : Finset α
x✝ : t ∈ 𝒜
hst : t✝ ⊆ t
⊢ #t✝ ≤ #t
Module: Mathlib.Order.Irreducible

Goal state before:
pp: α : Type u_2
inst✝² : SemilatticeSup α
inst✝¹ : OrderBot α
inst✝ : WellFoundedLT α
a : α
⊢ ∃ s, s.sup id = a ∧ ∀ ⦃b : α⦄, b ∈ s → SupIrred b

Tactic:
by
  classical
  apply WellFoundedLT.induction a _
  clear a
  rintro a ih
  by_cases ha : SupIrred a
  · exact ⟨{a}, by simp [ha]⟩
  rw [not_supIrred] at ha
  obtain ha | ⟨b, c, rfl, hb, hc⟩ := ha
  · exact ⟨∅, by simp [ha.eq_bot]⟩
  obtain ⟨s, rfl, hs⟩ := ih _ hb
  obtain ⟨t, rfl, ht⟩ := ih _ hc
  exact ⟨s ∪ t, sup_union, forall_mem_union.2 ⟨hs, ht⟩⟩

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

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
t✝ t : Finset α
x✝ : t ∈ 𝒜
hst : t ⊆ t✝
⊢ #(t✝ \ t) = 1 ↔ #t✝ = #t + 1

Tactic:
rw [card_sdiff_of_subset hst, tsub_eq_iff_eq_add_of_le, add_comm]

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
t✝ t : Finset α
x✝ : t ∈ 𝒜
hst : t ⊆ t✝
⊢ #t ≤ #t✝
Module: Mathlib.Combinatorics.SetFamily.AhlswedeZhang

Goal state before:
pp: case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 ℬ : Finset (Finset α)
s : Finset α
h𝒜 : s ∈ upperClosure ↑𝒜
hℬ : s ∉ upperClosure ↑ℬ
⊢ #(𝒜.truncatedInf s) + #((𝒜 ⊻ ℬ).truncatedInf s) = #(𝒜.truncatedInf s) + #⊥

Tactic:
truncatedInf_sups_of_notMem fun h ↦ hℬ h.2

Goal state after:
case neg
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 ℬ : Finset (Finset α)
s : Finset α
h𝒜 : s ∈ upperClosure ↑𝒜
hℬ : s ∉ upperClosure ↑ℬ
⊢ #(𝒜.truncatedInf s) + #⊥ = #(𝒜.truncatedInf s) + #⊥
Module: Mathlib.Combinatorics.SetFamily.Shadow

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
t✝ : Finset α
k : ℕ
t : Finset α
x✝ : t ∈ 𝒜
hst : t ⊆ t✝
⊢ #(t✝ \ t) = k ↔ #t✝ = #t + k

Tactic:
rw [card_sdiff_of_subset hst, tsub_eq_iff_eq_add_of_le, add_comm]

Goal state after:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
t✝ : Finset α
k : ℕ
t : Finset α
x✝ : t ∈ 𝒜
hst : t ⊆ t✝
⊢ #t ≤ #t✝
Module: Mathlib.Combinatorics.SetFamily.Compression.UV

Goal state before:
pp: case pos
α : Type u_1
inst✝ : DecidableEq α
u v : Finset α
huv : #u = #v
a : Finset α
h : Disjoint u a ∧ v ⊆ a
⊢ #a + #v - #v = #a

Tactic:
add_tsub_cancel_right

Goal state after:
case pos
α : Type u_1
inst✝ : DecidableEq α
u v : Finset α
huv : #u = #v
a : Finset α
h : Disjoint u a ∧ v ⊆ a
⊢ #a = #a