mathlib-initiative/mathlib-tactics huggingface dataset:
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✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : NonUnitalNonAssocSemiring 𝕜
f g h : IncidenceAlgebra 𝕜 α
a✝¹ b✝ : α
a✝ : a✝¹ ≤ b✝
⊢ ((f + g) * h) a✝¹ b✝ = (f * h + g * h) a✝¹ b✝

Tactic:
exact Eq.trans (sum_congr rfl fun x _ ↦ right_distrib _ _ _) sum_add_distrib

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

Goal state before:
pp: 𝕜 : Type u_2
α : Type u_5
inst✝³ : NonAssocSemiring 𝕜
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableLE α
a b : α
⊢ (zeta 𝕜 * zeta 𝕜) a b = ↑(#(Icc a b))

Tactic:
mul_apply,

Goal state after:
𝕜 : Type u_2
α : Type u_5
inst✝³ : NonAssocSemiring 𝕜
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableLE α
a b : α
⊢ ∑ x ∈ Icc a b, (zeta 𝕜) a x * (zeta 𝕜) x b = ↑(#(Icc a b))
Module: Mathlib.Combinatorics.Enumerative.Partition.GenFun

Goal state before:
pp: R : Type u_1
inst✝ : CommSemiring R
f : ℕ → ℕ → R
i n m : ℕ
⊢ n ≤ m → ↑n < (f (i + 1) (m + 1) • X ^ ((i + 1) * (m + 1))).order

Tactic:
hm

Goal state after:
R : Type u_1
inst✝ : CommSemiring R
f : ℕ → ℕ → R
i n m : ℕ
hm : n ≤ m
⊢ ↑n < (f (i + 1) (m + 1) • X ^ ((i + 1) * (m + 1))).order
Module: Mathlib.Combinatorics.Enumerative.IncidenceAlgebra

Goal state before:
pp: 𝕜 : Type u_2
α : Type u_5
inst✝⁴ : Ring 𝕜
inst✝³ : PartialOrder α
inst✝² : OrderTop α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
f g : α → 𝕜
h : ∀ (x : α), g x = ∑ y ≥ x, f y
x : α
this : DecidableLE α := Classical.decRel LE.le
⊢ ∑ z ≥ x, ∑ y ∈ Icc x z, (mu 𝕜) x y * (zeta 𝕜) y z * f z = ∑ z ≥ x, (mu 𝕜 * zeta 𝕜) x z * f z

Tactic:
mul_apply,

Goal state after:
𝕜 : Type u_2
α : Type u_5
inst✝⁴ : Ring 𝕜
inst✝³ : PartialOrder α
inst✝² : OrderTop α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
f g : α → 𝕜
h : ∀ (x : α), g x = ∑ y ≥ x, f y
x : α
this : DecidableLE α := Classical.decRel LE.le
⊢ ∑ z ≥ x, ∑ y ∈ Icc x z, (mu 𝕜) x y * (zeta 𝕜) y z * f z =
    ∑ x_1 ≥ x, (∑ x_2 ∈ Icc x x_1, (mu 𝕜) x x_2 * (zeta 𝕜) x_2 x_1) * f x_1
Module: Mathlib.Combinatorics.Enumerative.Partition.Glaisher

Goal state before:
pp: case inr
R : Type u_1
inst✝² : TopologicalSpace R
inst✝¹ : T2Space R
inst✝ : CommSemiring R
m : ℕ
hm : m > 0
⊢ Multipliable fun i ↦ ∑ j ∈ range m, X ^ ((i + 1) * j)

Tactic:
· exact (hasProd_powerSeriesMk_card_countRestricted R hm).multipliable

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
⊢ ∀ (b' : ℕ),
    b' ≠ Multiset.count i p.parts - 1 → (if Multiset.count i p.parts * i = i * (b' + 1) then f i (b' + 1) else 0) = 0

Tactic:
intro b

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
i : ℕ
hi : i ∈ p.parts
hi0 : i ≠ 0
b : ℕ
⊢ b ≠ Multiset.count i p.parts - 1 → (if Multiset.count i p.parts * i = i * (b + 1) then f i (b + 1) else 0) = 0
Module: Mathlib.Combinatorics.Enumerative.Partition.Glaisher

Goal state before:
pp: case refine_1
R : Type u_1
inst✝⁴ : TopologicalSpace R
inst✝³ : T2Space R
inst✝² : CommRing R
inst✝¹ : NoZeroDivisors R
inst✝ : IsTopologicalRing R
m : ℕ
hm : 0 < m
a✝ : Nontrivial R
a b : ↑(Function.mulSupport fun i ↦ 1 - (X ^ (i + 1)) ^ m)
h : ↑a = ↑b
⊢ a = b

Tactic:
exact SetCoe.ext h

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

Goal state before:
pp: case refine_2
R : Type u_1
inst✝⁴ : TopologicalSpace R
inst✝³ : T2Space R
inst✝² : CommRing R
inst✝¹ : NoZeroDivisors R
inst✝ : IsTopologicalRing R
m : ℕ
hm : 0 < m
a✝ : Nontrivial R
⊢ (Function.mulSupport fun b ↦ if m ∣ b + 1 then 1 * (1 - X ^ (b + 1)) else 1) ⊆ Set.range fun i ↦ (↑i + 1) * m - 1

Tactic:
suffices ∀ (i : ℕ), m ∣ i + 1 → ∃ j ≠ 0, j * m - 1 = i by simpa

Goal state after:
case refine_2
R : Type u_1
inst✝⁴ : TopologicalSpace R
inst✝³ : T2Space R
inst✝² : CommRing R
inst✝¹ : NoZeroDivisors R
inst✝ : IsTopologicalRing R
m : ℕ
hm : 0 < m
a✝ : Nontrivial R
⊢ ∀ (i : ℕ), m ∣ i + 1 → ∃ j, j ≠ 0 ∧ j * m - 1 = i
Module: Mathlib.Combinatorics.Enumerative.Pentagonal.Ring

Goal state before:
pp: case succ
R : Type u_1
inst✝³ : CommRing R
inst✝² : TopologicalSpace R
inst✝¹ : IsTopologicalRing R
inst✝ : T2Space R
x : R
hx : IsTopologicallyNilpotent x
hsum : ∀ (k : ℕ), Summable fun x_1 ↦ powMulProdOneSubPow k x_1 x
h : ∀ (k : ℕ), Multipliable fun n ↦ 1 - x ^ (n + k + 1)
n : ℕ
ih :
  ∏' (n : ℕ), (1 - x ^ (n + 1)) =
    ∑ k ∈ Finset.range (n + 1), (-1) ^ k * (x ^ (k * (3 * k + 1) / 2) - x ^ ((k + 1) * (3 * k + 2) / 2)) +
      (-1) ^ (n + 1) * x ^ ((n + 1) * (3 * n + 4) / 2) * ∑' (n_1 : ℕ), powMulProdOneSubPow n n_1 x
⊢ ∏' (n : ℕ), (1 - x ^ (n + 1)) =
    ∑ k ∈ Finset.range (n + 1 + 1), (-1) ^ k * (x ^ (k * (3 * k + 1) / 2) - x ^ ((k + 1) * (3 * k + 2) / 2)) +
      (-1) ^ (n + 1 + 1) * x ^ ((n + 1 + 1) * (3 * (n + 1) + 4) / 2) * ∑' (n_1 : ℕ), powMulProdOneSubPow (n + 1) n_1 x

Tactic:
rw [ih, tsum_powMulProdOneSubPow _ hx hsum h, Finset.sum_range_succ _ (n + 1)]

Goal state after:
case succ
R : Type u_1
inst✝³ : CommRing R
inst✝² : TopologicalSpace R
inst✝¹ : IsTopologicalRing R
inst✝ : T2Space R
x : R
hx : IsTopologicallyNilpotent x
hsum : ∀ (k : ℕ), Summable fun x_1 ↦ powMulProdOneSubPow k x_1 x
h : ∀ (k : ℕ), Multipliable fun n ↦ 1 - x ^ (n + k + 1)
n : ℕ
ih :
  ∏' (n : ℕ), (1 - x ^ (n + 1)) =
    ∑ k ∈ Finset.range (n + 1), (-1) ^ k * (x ^ (k * (3 * k + 1) / 2) - x ^ ((k + 1) * (3 * k + 2) / 2)) +
      (-1) ^ (n + 1) * x ^ ((n + 1) * (3 * n + 4) / 2) * ∑' (n_1 : ℕ), powMulProdOneSubPow n n_1 x
⊢ ∑ k ∈ Finset.range (n + 1), (-1) ^ k * (x ^ (k * (3 * k + 1) / 2) - x ^ ((k + 1) * (3 * k + 2) / 2)) +
      (-1) ^ (n + 1) * x ^ ((n + 1) * (3 * n + 4) / 2) *
        (1 - x ^ (2 * n + 3) - x ^ (3 * n + 5) * ∑' (n_1 : ℕ), powMulProdOneSubPow (n + 1) n_1 x) =
    ∑ x_1 ∈ Finset.range (n + 1), (-1) ^ x_1 * (x ^ (x_1 * (3 * x_1 + 1) / 2) - x ^ ((x_1 + 1) * (3 * x_1 + 2) / 2)) +
        (-1) ^ (n + 1) * (x ^ ((n + 1) * (3 * (n + 1) + 1) / 2) - x ^ ((n + 1 + 1) * (3 * (n + 1) + 2) / 2)) +
      (-1) ^ (n + 1 + 1) * x ^ ((n + 1 + 1) * (3 * (n + 1) + 4) / 2) * ∑' (n_1 : ℕ), powMulProdOneSubPow (n + 1) n_1 x
Module: Mathlib.Combinatorics.Enumerative.Schroder

Goal state before:
pp: n : ℕ
hn : 1 < n + 1 + 1
⊢ (n + 1).largeSchroder +
      (∑ x ∈ Ioc ⊥ (n + 1), x.largeSchroder * (n + 1 - x).largeSchroder + ⊥.largeSchroder * (n + 1 - ⊥).largeSchroder) =
    3 * (n + 1).largeSchroder + ∑ i ∈ Ioo 0 (n + 1), i.largeSchroder * (n + 1 - i).largeSchroder

pp: n : ℕ
hn : 1 < n + 1 + 1
⊢ ⊥ ≤ n + 1

pp: n : ℕ
hn : 1 < n + 1 + 1
⊢ n + 2 ≠ 0

Tactic:
← sum_Ioo_add_eq_sum_Ioc

Goal state after:
n : ℕ
hn : 1 < n + 1 + 1
⊢ (n + 1).largeSchroder +
      (∑ x ∈ Ioo ⊥ (n + 1), x.largeSchroder * (n + 1 - x).largeSchroder +
          (n + 1).largeSchroder * (n + 1 - (n + 1)).largeSchroder +
        ⊥.largeSchroder * (n + 1 - ⊥).largeSchroder) =
    3 * (n + 1).largeSchroder + ∑ i ∈ Ioo 0 (n + 1), i.largeSchroder * (n + 1 - i).largeSchroder

n : ℕ
hn : 1 < n + 1 + 1
⊢ ⊥ < n + 1

n : ℕ
hn : 1 < n + 1 + 1
⊢ ⊥ ≤ n + 1

n : ℕ
hn : 1 < n + 1 + 1
⊢ n + 2 ≠ 0
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 b : G
ha : a ∈ ↑(n⁻¹ •> N)
hb : b ∈ ↑(n⁻¹ •> N)
⊢ a * b ∈ ↑(n⁻¹ •> N)

Tactic:
mem_coe

Goal state after:
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 b : G
ha : a ∈ n⁻¹ •> N
hb : b ∈ n⁻¹ •> N
⊢ a * b ∈ n⁻¹ •> N
Module: Mathlib.Combinatorics.Enumerative.Pentagonal.PowerSeries

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
k : ℕ
a✝ : Nontrivial R
n m : ℕ
⊢ n + 1 ≤ m → ↑n < (X ^ ((k + 1) * m) * ∏ i ∈ Finset.range (m + 1), (1 - X ^ (k + i + 1))).order

Tactic:
hm

Goal state after:
R : Type u_1
inst✝ : CommRing R
k : ℕ
a✝ : Nontrivial R
n m : ℕ
hm : n + 1 ≤ m
⊢ ↑n < (X ^ ((k + 1) * m) * ∏ i ∈ Finset.range (m + 1), (1 - X ^ (k + i + 1))).order
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 b : G
ha : a ∈ n⁻¹ •> N
hb✝ : b ∈ n⁻¹ •> N
hb : a * b ∈ a •> n⁻¹ •> N
⊢ a * b ∈ n⁻¹ •> N

Tactic:
have : (n⁻¹ •> N ∩ a •> n⁻¹ •> N).Nonempty := ⟨a, by
        simpa only [mem_inter] using! ⟨ha, self_mem_smul_carrier a⟩⟩

Goal state after:
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 b : G
ha : a ∈ n⁻¹ •> N
hb✝ : b ∈ n⁻¹ •> N
hb : a * b ∈ a •> n⁻¹ •> N
this : (n⁻¹ •> N ∩ a •> n⁻¹ •> N).Nonempty
⊢ a * b ∈ n⁻¹ •> N
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)
⊢ a⁻¹ ∈ ↑(n⁻¹ •> N)

Tactic:
mem_coe

Goal state after:
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
⊢ a⁻¹ ∈ n⁻¹ •> N
Module: Mathlib.Combinatorics.Graph.Basic

Goal state before:
pp: case inr
α : Type u_1
β : Type u_2
y z : α
e : β
G : Graph α β
h : G.IsLink e y y
h' : G.IsLink e y z
⊢ y = z

Tactic:
obtain rfl | rfl := h'.right_eq_or_eq h.symm

Goal state after:
case inr.inl
α : Type u_1
β : Type u_2
z : α
e : β
G : Graph α β
h h' : G.IsLink e z z
⊢ z = z

case inr.inr
α : Type u_1
β : Type u_2
z : α
e : β
G : Graph α β
h h' : G.IsLink e z z
⊢ z = z
Module: Mathlib.Combinatorics.Graph.Delete

Goal state before:
pp: α : Type u_1
β : Type u_2
G : Graph α β
F₁ F₂ : Set β
⊢ (G.restrict F₁).restrict F₂ = G.restrict (F₁ ∩ F₂)

Tactic:
refine (Compatible.of_le_le (G := G) (restrict_le.trans (by simp)) (by simp)).ext (by simp) ?_

Goal state after:
α : Type u_1
β : Type u_2
G : Graph α β
F₁ F₂ : Set β
⊢ E((G.restrict F₁).restrict F₂) = E(G.restrict (F₁ ∩ F₂))
Module: Mathlib.Combinatorics.Hindman

Goal state before:
pp: M : Type u_1
inst✝ : Semigroup M
a : Stream' M
S : Set (Ultrafilter M) := ⋂ n, {U | ∀ᶠ (m : M) in ↑U, m ∈ FP (Stream'.drop n a)}
U : Ultrafilter M
hU : ∀ (i : ℕ), U ∈ {U | ∀ᶠ (m : M) in ↑U, m ∈ FP (Stream'.drop i a)}
V : Ultrafilter M
hV : ∀ (i : ℕ), V ∈ {U | ∀ᶠ (m : M) in ↑U, m ∈ FP (Stream'.drop i a)}
n : ℕ
m : M
⊢ m ∈ FP (Stream'.drop n a) → ∀ᶠ (m' : M) in ↑V, m * m' ∈ FP (Stream'.drop n a)

Tactic:
hm

Goal state after:
M : Type u_1
inst✝ : Semigroup M
a : Stream' M
S : Set (Ultrafilter M) := ⋂ n, {U | ∀ᶠ (m : M) in ↑U, m ∈ FP (Stream'.drop n a)}
U : Ultrafilter M
hU : ∀ (i : ℕ), U ∈ {U | ∀ᶠ (m : M) in ↑U, m ∈ FP (Stream'.drop i a)}
V : Ultrafilter M
hV : ∀ (i : ℕ), V ∈ {U | ∀ᶠ (m : M) in ↑U, m ∈ FP (Stream'.drop i a)}
n : ℕ
m : M
hm : m ∈ FP (Stream'.drop n a)
⊢ ∀ᶠ (m' : M) in ↑V, m * m' ∈ FP (Stream'.drop n a)
Module: Mathlib.Combinatorics.Hindman

Goal state before:
pp: M : Type u_1
inst✝ : Semigroup M
U : Ultrafilter M
U_idem : U * U = U
s₀ : Set M
sU : s₀ ∈ 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}, ⋯⟩
this : ∀ (a : Stream' M), ∀ m ∈ FP a, ∀ (p : { s // s ∈ U }), a = Stream'.corec elem succ p → m ∈ ↑p
m : M
⊢ m ∈ FP (Stream'.corec elem succ ⟨s₀, sU⟩) → m ∈ s₀

Tactic:
hm

Goal state after:
M : Type u_1
inst✝ : Semigroup M
U : Ultrafilter M
U_idem : U * U = U
s₀ : Set M
sU : s₀ ∈ 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}, ⋯⟩
this : ∀ (a : Stream' M), ∀ m ∈ FP a, ∀ (p : { s // s ∈ U }), a = Stream'.corec elem succ p → m ∈ ↑p
m : M
hm : m ∈ FP (Stream'.corec elem succ ⟨s₀, sU⟩)
⊢ m ∈ s₀
Module: Mathlib.Combinatorics.Matroid.Minor.Delete

Goal state before:
pp: α : Type u_1
M : Matroid α
D X : Set α
⊢ (M ＼ D).closure X = M.closure (X \ D) \ D

Tactic:
rw [← restrict_compl, restrict_closure_eq', sdiff_sdiff_self, bot_eq_empty, union_empty,
    sdiff_eq, inter_comm M.E, ← inter_assoc X, ← sdiff_eq, closure_inter_ground,
    ← inter_assoc, ← sdiff_eq, inter_eq_left]

Goal state after:
α : Type u_1
M : Matroid α
D X : Set α
⊢ M.closure (X \ D) \ D ⊆ M.E
Module: Mathlib.Combinatorics.HalesJewett

Goal state before:
pp: case refine_2
M : Type u_5
κ : Type u_6
inst✝¹ : AddCommMonoid M
S : Finset M
inst✝ : Finite κ
C : M → κ
ι : Type
_inst : Fintype ι
l : Line (↥S) ι
c : κ
hl : ∀ (x : ↥S), (fun v ↦ C (∑ i, ↑(v i))) (↑l x) = c
s : Finset ι := {i | l.idxFun i = none}
hs : s = {i | l.idxFun i = none}
i : ι
⊢ ↥S → M

Tactic:
exact fun m => m

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

Goal state before:
pp: case pos
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
ι : Type u_3
b : ι → MvPolynomial σ R
hb : ∀ (i : ι), IsUnit (m.leadingCoeff (b i))
f : MvPolynomial σ R
hb' : ∀ (i : ι), m.degree (b i) ≠ 0
hf0 : f = 0
⊢ ∀ (i : ι), m.toSyn (m.degree (b i * 0 i)) ≤ m.toSyn (m.degree f)

Tactic:
intro b

Goal state after:
case pos
σ : 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
b : ι
⊢ m.toSyn (m.degree (b✝ b * 0 b)) ≤ m.toSyn (m.degree f)
Module: Mathlib.Combinatorics.Matroid.Minor.Contract

Goal state before:
pp: α✝ α : Type u_1
M : Matroid α
C : Set α
hCE : C ⊆ M.E
I : Set α
hI : M.IsBasis I C
⊢ M ／ M.closure C = M ／ C ＼ (M.closure C \ C)

Tactic:
hI.isBasis_closure_right.contract_eq_contract_delete,

Goal state after:
α✝ α : Type u_1
M : Matroid α
C : Set α
hCE : C ⊆ M.E
I : Set α
hI : M.IsBasis I C
⊢ M ／ I ＼ (M.closure C \ I) = M ／ C ＼ (M.closure C \ C)
Module: Mathlib.Combinatorics.Matroid.Minor.Contract

Goal state before:
pp: α : Type u_1
M : Matroid α
K✝ C K : Set α
hC : (M ／ K).IsCircuit C
hKi : M.Indep K
⊢ ∃ C', M.IsCircuit C' ∧ C ⊆ C' ∧ C' ⊆ C ∪ K

Tactic:
obtain ⟨hCE : C ⊆ M.E, hCK : Disjoint C K⟩ := subset_sdiff.1 hC.subset_ground

Goal state after:
α : Type u_1
M : Matroid α
K✝ C K : Set α
hC : (M ／ K).IsCircuit C
hKi : M.Indep K
hCE : C ⊆ M.E
hCK : Disjoint C K
⊢ ∃ C', M.IsCircuit C' ∧ C ⊆ C' ∧ C' ⊆ C ∪ K
Module: Mathlib.Combinatorics.Matroid.Sum

Goal state before:
pp: case refine_4
ι : 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✝¹ :
  (∀ (x : ι), Sigma.mk x ⁻¹' I ⊆ Sigma.mk x ⁻¹' X) ∧
    (∀ (x : ι) ⦃t : Set (α x)⦄, (M x).Indep t → t ⊆ Sigma.mk x ⁻¹' X → Sigma.mk x ⁻¹' I ⊆ t → Sigma.mk x ⁻¹' I = t) ∧
      ∀ (x : ι), Sigma.mk x ⁻¹' X ⊆ (M x).E
hIX : ∀ (x : ι), Sigma.mk x ⁻¹' I ⊆ Sigma.mk x ⁻¹' X
h' : ∀ (x : ι) ⦃t : Set (α x)⦄, (M x).Indep t → t ⊆ Sigma.mk x ⁻¹' X → Sigma.mk x ⁻¹' I ⊆ t → Sigma.mk x ⁻¹' I = t
h'' : ∀ (x : ι), Sigma.mk x ⁻¹' X ⊆ (M x).E
J : Set ((i : ι) × α i)
hJ : ∀ (i : ι), (M i).Indep (Sigma.mk i ⁻¹' J)
hJX : J ⊆ X
hIJ : I ⊆ J
x✝ : (i : ι) × α i
i : ι
x : α i
hx : ⟨i, x⟩ ∈ J
⊢ ⟨i, x⟩ ∈ I

Tactic:
simpa using (h' i (hJ i) (preimage_mono hJX) (preimage_mono hIJ)).symm.subset hx

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

Goal state before:
pp: case pos
σ : 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
hf'0 : m.subLTerm f = 0
⊢ ∀ (i : ι), m.toSyn (m.degree (b i * 0 i)) ≤ m.toSyn (m.degree (m.subLTerm f))

Tactic:
intro b

Goal state after:
case pos
σ : 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
hf'0 : m.subLTerm f = 0
b : ι
⊢ m.toSyn (m.degree (b✝ b * 0 b)) ≤ m.toSyn (m.degree (m.subLTerm f))
Module: Mathlib.Combinatorics.Quiver.Arborescence

Goal state before:
pp: V : Type u
inst✝¹ : Quiver V
r : V
inst✝ : RootedConnected r
⊢ ∀ (b : WideSubquiver.toType V (geodesicSubtree r)), b = r ∨ ∃ a, Nonempty (a ⟶ b)

Tactic:
intro b

Goal state after:
V : Type u
inst✝¹ : Quiver V
r : V
inst✝ : RootedConnected r
b : WideSubquiver.toType V (geodesicSubtree r)
⊢ b = r ∨ ∃ a, Nonempty (a ⟶ b)
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 : σ
⊢ ∀ i_1 ∈ S, IsRegular (m.leadingCoeff (X i - C i_1))

Tactic:
· intro r _
    rw [m.monic_X_sub_C]
    exact isRegular_one

Goal state after:
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φ : φ.IsCovering
⊢ φ.symmetrify.IsCovering

Tactic:
refine ⟨fun u => ?_, fun u => ?_⟩

Goal state after:
case refine_1
U : Type u_1
inst✝¹ : Quiver U
V : Type u_2
inst✝ : Quiver V
φ : U ⥤q V
hφ : φ.IsCovering
u : Symmetrify U
⊢ Bijective (φ.symmetrify.star u)

case refine_2
U : Type u_1
inst✝¹ : Quiver U
V : Type u_2
inst✝ : Quiver V
φ : U ⥤q V
hφ : φ.IsCovering
u : Symmetrify U
⊢ Bijective (φ.symmetrify.costar u)
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
this : Finsupp.degree (degLex.degree (h i * Alon.P (S i) i)) ≤ f.totalDegree
⊢ IsRegular (degLex.leadingCoeff (Alon.P (S i) i))

Tactic:
simp only [(Alon.monic_P ..).leadingCoeff_eq_one,
      isRegular_one]

Goal state after:
Module: Mathlib.Combinatorics.Schnirelmann

Goal state before:
pp: A : Set ℕ
inst✝ : DecidablePred fun x ↦ x ∈ A
⊢ ↑(#({a ∈ Ioc 0 1 | a ∈ A})) / ↑1 ≤ 1

Tactic:
rw [Nat.cast_one, div_one, Nat.cast_le_one]; exact card_filter_le _ _

Goal state after:
Module: Mathlib.Combinatorics.Schnirelmann

Goal state before:
pp: A : Set ℕ
inst✝ : DecidablePred fun x ↦ x ∈ A
k : ℕ
hk : k ∉ A
⊢ schnirelmannDensity A ≤ 1 - (↑k)⁻¹

Tactic:
rcases k.eq_zero_or_pos with rfl | hk'
  · simpa using schnirelmannDensity_le_one
  apply schnirelmannDensity_le_of_le k hk'.ne'
  rw [← one_div, one_sub_div (Nat.cast_pos.2 hk').ne']
  gcongr
  rw [← Nat.cast_pred hk', Nat.cast_le]
  suffices {a ∈ Ioc 0 k | a ∈ A} ⊆ Ioo 0 k from (card_le_card this).trans_eq (by simp)
  rw [← Ioo_insert_right hk', filter_insert, if_neg hk]
  exact filter_subset _ _

Goal state after:
Module: Mathlib.Combinatorics.Schnirelmann

Goal state before:
pp: A : Set ℕ
inst✝ : DecidablePred fun x ↦ x ∈ A
x : ℝ
⊢ schnirelmannDensity A < x ↔ ∃ n, 0 < n ∧ ↑(#({a ∈ Ioc 0 n | a ∈ A})) / ↑n < x

Tactic:
rw [← not_le, le_schnirelmannDensity_iff]; simp

Goal state after:
Module: Mathlib.Combinatorics.Schnirelmann

Goal state before:
pp: A : Set ℕ
inst✝¹ : DecidablePred fun x ↦ x ∈ A
B : Set ℕ
inst✝ : DecidablePred fun x ↦ x ∈ B
h : ∀ n > 0, n ∈ A ↔ n ∈ B
⊢ ⨅ n, ↑(#({a ∈ Ioc 0 ↑n | a ∈ A})) / ↑↑n = schnirelmannDensity B

Tactic:
schnirelmannDensity

Goal state after:
A : Set ℕ
inst✝¹ : DecidablePred fun x ↦ x ∈ A
B : Set ℕ
inst✝ : DecidablePred fun x ↦ x ∈ B
h : ∀ n > 0, n ∈ A ↔ n ∈ B
⊢ ⨅ n, ↑(#({a ∈ Ioc 0 ↑n | a ∈ A})) / ↑↑n = ⨅ n, ↑(#({a ∈ Ioc 0 ↑n | a ∈ B})) / ↑↑n
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 ≤ (↑m)⁻¹

pp: m : ℕ
hm : m ≠ 1
hm' : m > 0
⊢ (↑m)⁻¹ ≤ schnirelmannDensity {n | n % m = 1}

Tactic:
· rw [← one_div, ← @Nat.cast_one ℝ]
    gcongr
    simp only [Set.mem_ofPred_eq, card_le_one_iff_subset_singleton, subset_iff,
      mem_filter, mem_Ioc, mem_singleton, and_imp]
    use 1
    intro x _ hxm h
    rcases eq_or_lt_of_le hxm with rfl | hxm'
    · simp at h
    rwa [Nat.mod_eq_of_lt hxm'] at h

Goal state after:
m : ℕ
hm : m ≠ 1
hm' : m > 0
⊢ (↑m)⁻¹ ≤ schnirelmannDensity {n | n % m = 1}
Module: Mathlib.Combinatorics.Schnirelmann

Goal state before:
pp: case neg
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
⊢ n ∈ A + B

Tactic:
let f : ℕ ⊕ ℕ → ℕ
    | .inl x => x
    | .inr y => n - y

Goal state after:
case neg
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
⊢ n ∈ A + B
Module: Mathlib.Combinatorics.SetFamily.AhlswedeZhang

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁵ : SemilatticeSup α
inst✝⁴ : SemilatticeSup β
inst✝³ : BoundedOrder β
inst✝² : DecidableLE α
inst✝¹ : OrderTop α
inst✝ : DecidableLE β
e : α ≃o β
s : Finset α
a : α
this : e a ∈ lowerClosure ↑(map e.toEmbedding s) ↔ a ∈ lowerClosure ↑s
⊢ (if h : a ∈ lowerClosure ↑s then {b ∈ s | a ≤ b}.sup' ⋯ (⇑e ∘ id) else ⊤) =
    if h : a ∈ lowerClosure ↑s then {b ∈ map e.toEmbedding s | e a ≤ b}.sup' ⋯ id else ⊤

Tactic:
congr with h

Goal state after:
case e_t
α : Type u_1
β : Type u_2
inst✝⁵ : SemilatticeSup α
inst✝⁴ : SemilatticeSup β
inst✝³ : BoundedOrder β
inst✝² : DecidableLE α
inst✝¹ : OrderTop α
inst✝ : DecidableLE β
e : α ≃o β
s : Finset α
a : α
this : e a ∈ lowerClosure ↑(map e.toEmbedding s) ↔ a ∈ lowerClosure ↑s
h : a ∈ lowerClosure ↑s
⊢ {b ∈ s | a ≤ b}.sup' ⋯ (⇑e ∘ id) = {b ∈ map e.toEmbedding s | e a ≤ b}.sup' ⋯ id
Module: Mathlib.Combinatorics.Schnirelmann

Goal state before:
pp: case neg
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}
hc : #(image f (sA.disjSum sB)) < #(sA.disjSum sB)
⊢ n ∈ A + B

Tactic:
obtain ⟨a | b, ha, a | b, hb, _, hxy⟩ := exists_ne_map_eq_of_card_image_lt hc <;>
  simp only [sA, sB, inl_mem_disjSum, mem_filter, mem_Ioc, inr_mem_disjSum] at ha hb <;>
  first | grind [inr_mem_disjSum] | exact ⟨a, by simp [*], b, by simp [*], by grind⟩

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₁ s₂ t : Finset α
⊢ (s₁ ∩ s₂) ○ t ⊆ s₁ ○ t ∩ s₂ ○ t

Tactic:
simpa only [disjSups, inter_product, filter_inter_distrib] using image_inter_subset _ _ _

Goal state after: