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

Goal state before:
pp: G : Type u_1
inst✝ : AddCommGroup G
A : Finset (G × G)
a b c : G
h₁ : (a, b) ∈ A
h₂ : c = ({ toFun := fun x ↦ (x.1, x.2, x.1 + x.2), inj' := ⋯ } (a, b)).2.2
⊢ (a, b) ∈ A ∧ c = a + b

Tactic:
exact ⟨h₁, h₂⟩

Goal state after:
Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
inst✝³ : DecidableEq α
inst✝² : DecidableEq β
inst✝¹ : DecidableEq γ
inst✝ : NoAccidental t
⊢ (graph t).cliqueSet 3 = ⇑toTriangle '' ↑t

Tactic:
ext; exact is3Clique_iff

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

Goal state before:
pp: M : Type u_1
inst✝³ : DecidableEq M
inst✝² : AddCommMonoid M
A : Finset M
inst✝¹ : LinearOrder M
inst✝ : IsOrderedCancelAddMonoid M
A_pos : ∀ x ∈ A, 0 ≤ x
⊢ #(A.erase 0).subsetSum = #A.subsetSum

Tactic:
rw [subsetSum_erase_zero]

Goal state after:
Module: Mathlib.Data.Nat.BitIndices

Goal state before:
pp: case succ
n k : ℕ
ih : (2 ^ k * n).bitIndices = map (fun x ↦ x + k) n.bitIndices
⊢ (2 ^ (k + 1) * n).bitIndices = map (fun x ↦ x + (k + 1)) n.bitIndices

Tactic:
rw [add_comm, pow_add, pow_one, mul_assoc, bitIndices_two_mul, ih, List.map_map, comp_add_right]
    simp [add_comm (a := 1)]

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

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
a : α
f : Perm α
⊢ fixedPoints ⇑f ⊆ {a} ∧ a ∉ fixedPoints ⇑f ↔ fixedPoints ⇑f = ∅

Tactic:
rw [Set.eq_empty_iff_forall_notMem]

Goal state after:
case refine_2
α : Type u_1
β : Type u_2
inst✝ : DecidableEq α
a : α
f : Perm α
⊢ fixedPoints ⇑f ⊆ {a} ∧ a ∉ fixedPoints ⇑f ↔ ∀ (x : α), x ∉ fixedPoints ⇑f
Module: Mathlib.Combinatorics.Derangements.Basic

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
⊢ fiber none = ∅

Tactic:
rw [Set.eq_empty_iff_forall_notMem]

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
⊢ ∀ (x : Perm α), x ∉ fiber none
Module: Mathlib.Combinatorics.Configuration

Goal state before:
pp: P : Type u_1
L : Type u_2
inst✝² : Membership P L
inst✝¹ : Fintype P
inst✝ : Fintype L
⊢ (i : P) × { l // i ∈ l } ≃ (i : L) × { p // p ∈ i }

Tactic:
calc
      (Σ p, { l : L // p ∈ l }) ≃ { x : P × L // x.1 ∈ x.2 } :=
        (Equiv.subtypeProdEquivSigmaSubtype (· ∈ ·)).symm
      _ ≃ { x : L × P // x.2 ∈ x.1 } := (Equiv.prodComm P L).subtypeEquiv fun x => Iff.rfl
      _ ≃ Σ l, { p // p ∈ l } := Equiv.subtypeProdEquivSigmaSubtype fun (l : L) (p : P) => p ∈ l

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

Goal state before:
pp: x : ℕ
hx : x ≠ 0
c : ℕ
⊢ (c + 1) * (c * x + x - 1).choose (x - 1) * (x * c)! * x ! = (x * (c + 1))!

Tactic:
← Nat.choose_mul_add hx,

Goal state after:
x : ℕ
hx : x ≠ 0
c : ℕ
⊢ (c * x + x).choose x * (x * c)! * x ! = (x * (c + 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 : G
ha : a ∈ A
z b : G
hb : b ∈ A
c : G
hc : c ∈ A
hz : a * (b⁻¹ * c * a) = z
l : Finset G := A ∩ (z * a⁻¹) •> (A⁻¹ * A)
r : Finset G := a •> (A⁻¹ * A) ∩ z •> A⁻¹
this✝² : A⁻¹ * A * (A⁻¹ * A) = A⁻¹ * A
hl : l = A
hr : r = z •> A⁻¹
lr : l ∪ r ⊆ a •> (A⁻¹ * A)
this✝¹ : #l = #A
this✝ : #r = #A
this : #(l ∪ r) < 2 * #A
⊢ (l ∩ r).Nonempty

Tactic:
← card_pos

Goal state after:
G : Type u_1
inst✝¹ : Group G
inst✝ : DecidableEq G
A : Finset G
h : ↑(#(A * A)) < 3 / 2 * ↑(#A)
a : G
ha : a ∈ A
z b : G
hb : b ∈ A
c : G
hc : c ∈ A
hz : a * (b⁻¹ * c * a) = z
l : Finset G := A ∩ (z * a⁻¹) •> (A⁻¹ * A)
r : Finset G := a •> (A⁻¹ * A) ∩ z •> A⁻¹
this✝² : A⁻¹ * A * (A⁻¹ * A) = A⁻¹ * A
hl : l = A
hr : r = z •> A⁻¹
lr : l ∪ r ⊆ a •> (A⁻¹ * A)
this✝¹ : #l = #A
this✝ : #r = #A
this : #(l ∪ r) < 2 * #A
⊢ 0 < #(l ∩ r)
Module: Mathlib.Combinatorics.Additive.VerySmallDoubling

Goal state before:
pp: G : Type u_1
inst✝ : Group G
H : Subgroup G
x a : G
hx : x ∈ (fun m ↦ m •> ↑H) { unop' := a }
⊢ ↑H = ↑H <• (x * a⁻¹)

Tactic:
rightCoset_mem_rightCoset

Goal state after:
G : Type u_1
inst✝ : Group G
H : Subgroup G
x a : G
hx : x ∈ (fun m ↦ m •> ↑H) { unop' := a }
⊢ ↑H = ↑H

case ha
G : Type u_1
inst✝ : Group G
H : Subgroup G
x a : G
hx : x ∈ (fun m ↦ m •> ↑H) { unop' := a }
⊢ x * a⁻¹ ∈ H
Module: Mathlib.Combinatorics.Enumerative.DyckWord

Goal state before:
pp: p : DyckWord
i : ℕ
lb : 0 < i
ub : i < 1 + (↑p).length + 1
⊢ count D (List.take (i - 1) ↑p) < count U (U :: List.take (i - 1) ↑p)

Tactic:
count_cons_self,

Goal state after:
p : DyckWord
i : ℕ
lb : 0 < i
ub : i < 1 + (↑p).length + 1
⊢ count D (List.take (i - 1) ↑p) < count U (List.take (i - 1) ↑p) + 1
Module: Mathlib.Combinatorics.Enumerative.DyckWord

Goal state before:
pp: p : DyckWord
i : ℕ
lb : 0 < i
ub : i < 1 + (↑p).length + 1
⊢ count D (List.take i ([U] ++ ↑p ++ [D])) < count U (List.take i ([U] ++ ↑p ++ [D]))

Tactic:
rw [take_append_of_le_length (by rw [singleton_append, length_cons]; lia),
    take_append, take_of_length_le (by rw [length_singleton]; lia),
    length_singleton, singleton_append, count_cons_of_ne (by simp), count_cons_self,
    Nat.lt_add_one_iff]

Goal state after:
p : DyckWord
i : ℕ
lb : 0 < i
ub : i < 1 + (↑p).length + 1
⊢ count D (List.take (i - 1) ↑p) ≤ count U (List.take (i - 1) ↑p)
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)!
hrest : rest = ∏ j ∈ ((a ::ₘ m).toFinset.erase 0).erase a, (count j (a ::ₘ m))!
c : ℕ := (map (fun x ↦ x !) m).prod * (count a m)! * rest
hm0 : m.bell * c = m.sum !
hm : m.sum ! * a ! = m.bell * a ! * c
hc : 0 < a ! * c
hq :
  (a ::ₘ m).bell * (map (fun j ↦ j !) (a ::ₘ m)).prod * ∏ j ∈ (a ::ₘ m).toFinset.erase 0, (count j (a ::ₘ m))! =
    (a ::ₘ m).sum !
⊢ a ∈ (a ::ₘ m).toFinset.erase 0

Tactic:
by simp [*]

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

Goal state before:
pp: F : Type u_1
𝕜 : Type u_2
𝕝 : Type u_3
𝕞 : Type u_4
α : Type u_5
β : Type u_6
inst✝⁵ : PartialOrder α
inst✝⁴ : LocallyFiniteOrder α
inst✝³ : DecidableEq α
inst✝² : CommSemiring 𝕜
inst✝¹ : CommSemiring 𝕝
inst✝ : Algebra 𝕜 𝕝
c : 𝕜
f : IncidenceAlgebra 𝕝 α
⊢ { toFun := fun c ↦ (algebraMap 𝕜 𝕝) c • 1, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ } c * f =
    f * { toFun := fun c ↦ (algebraMap 𝕜 𝕝) c • 1, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ } c

Tactic:
classical ext a b hab; simp [if_pos hab, constSMul_apply, mul_comm]

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

Goal state before:
pp: case pos
𝕜 : Type u_2
α : Type u_5
inst✝⁴ : AddCommGroup 𝕜
inst✝³ : One 𝕜
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b : α
hab✝ : ¬a = b
hab : a ≤ b
⊢ ∑ x ∈ Icc a b, (mu 𝕜) a x = 0

pp: case neg
𝕜 : Type u_2
α : Type u_5
inst✝⁴ : AddCommGroup 𝕜
inst✝³ : One 𝕜
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b : α
hab✝ : ¬a = b
hab : ¬a ≤ b
⊢ ∑ x ∈ Icc a b, (mu 𝕜) a x = 0

Tactic:
· simp [Icc_eq_cons_Ico hab, mu_eq_neg_sum_Ico_of_ne ‹_›]

Goal state after:
case neg
𝕜 : Type u_2
α : Type u_5
inst✝⁴ : AddCommGroup 𝕜
inst✝³ : One 𝕜
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
a b : α
hab✝ : ¬a = b
hab : ¬a ≤ b
⊢ ∑ x ∈ Icc a b, (mu 𝕜) a x = 0
Module: Mathlib.Combinatorics.Enumerative.IncidenceAlgebra

Goal state before:
pp: 𝕜 : Type u_2
α : Type u_5
inst✝³ : Ring 𝕜
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : DecidableEq α
this : DecidableLE α := Classical.decRel LE.le
mud : IncidenceAlgebra 𝕜 αᵒᵈ := { toFun := fun a b ↦ (mu 𝕜) (ofDual b) (ofDual a), eq_zero_of_not_le' := ⋯ }
a b : αᵒᵈ
a✝ : a ≤ b
⊢ (if ofDual b = ofDual a then 1 else 0) = if a = b then 1 else 0

Tactic:
simp [eq_comm]

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
⊢ 0 ≤ connectivity K S

Tactic:
by simp [*]

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : TopologicalSpace R
this : HasSum ((fun n ↦ C ((coeff n) (pentagonalSeries R)) * X ^ n) ∘ pentagonal) (pentagonalSeries R)
⊢ HasSum (fun k ↦ ↑↑k.negOnePow * X ^ pentagonal k) (pentagonalSeries R)

Tactic:
convert this

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : TopologicalSpace R
this : HasSum ((fun n ↦ C ((coeff n) (pentagonalSeries R)) * X ^ n) ∘ pentagonal) (pentagonalSeries R)
x✝ : ℤ
⊢ ↑↑x✝.negOnePow * X ^ pentagonal x✝ = ((fun n ↦ C ((coeff n) (pentagonalSeries R)) * X ^ n) ∘ pentagonal) x✝
Module: Mathlib.Combinatorics.Enumerative.Pentagonal.PowerSeries

Goal state before:
pp: case refine_1
R : Type u_1
inst✝³ : CommRing R
inst✝² : TopologicalSpace R
inst✝¹ : IsTopologicalRing R
inst✝ : T2Space R
a✝ : Nontrivial R
⊢ IsTopologicallyNilpotent X

pp: case refine_2
R : Type u_1
inst✝³ : CommRing R
inst✝² : TopologicalSpace R
inst✝¹ : IsTopologicalRing R
inst✝ : T2Space R
a✝ : Nontrivial R
⊢ ∀ (k : ℕ), Summable fun n ↦ X ^ ((k + 1) * n) * ∏ i ∈ Finset.range (n + 1), (1 - X ^ (k + i + 1))

pp: case refine_3
R : Type u_1
inst✝³ : CommRing R
inst✝² : TopologicalSpace R
inst✝¹ : IsTopologicalRing R
inst✝ : T2Space R
a✝ : Nontrivial R
⊢ ∀ (k : ℕ), Multipliable fun n ↦ 1 - X ^ (n + k + 1)

pp: case refine_4
R : Type u_1
inst✝³ : CommRing R
inst✝² : TopologicalSpace R
inst✝¹ : IsTopologicalRing R
inst✝ : T2Space R
a✝ : Nontrivial R
⊢ Summable fun k ↦ (-1) ^ k * (X ^ pentagonal (-↑k) - X ^ pentagonal (↑k + 1))

pp: case refine_5
R : Type u_1
inst✝³ : CommRing R
inst✝² : TopologicalSpace R
inst✝¹ : IsTopologicalRing R
inst✝ : T2Space R
a✝ : Nontrivial R
⊢ Tendsto
    (fun k ↦
      (-1) ^ (k + 1) * X ^ ((k + 1) * (3 * k + 4) / 2) *
        ∑' (n : ℕ), X ^ ((k + 1) * n) * ∏ i ∈ Finset.range (n + 1), (1 - X ^ (k + i + 1)))
    atTop (𝓝 0)

Tactic:
· rw [IsTopologicallyNilpotent, tendsto_iff_coeff_tendsto]
    refine fun d ↦ tendsto_atTop_of_eventually_const fun i (hi : i ≥ d + 1) ↦ ?_
    grind

Goal state after:
case refine_2
R : Type u_1
inst✝³ : CommRing R
inst✝² : TopologicalSpace R
inst✝¹ : IsTopologicalRing R
inst✝ : T2Space R
a✝ : Nontrivial R
⊢ ∀ (k : ℕ), Summable fun n ↦ X ^ ((k + 1) * n) * ∏ i ∈ Finset.range (n + 1), (1 - X ^ (k + i + 1))

case refine_3
R : Type u_1
inst✝³ : CommRing R
inst✝² : TopologicalSpace R
inst✝¹ : IsTopologicalRing R
inst✝ : T2Space R
a✝ : Nontrivial R
⊢ ∀ (k : ℕ), Multipliable fun n ↦ 1 - X ^ (n + k + 1)

case refine_4
R : Type u_1
inst✝³ : CommRing R
inst✝² : TopologicalSpace R
inst✝¹ : IsTopologicalRing R
inst✝ : T2Space R
a✝ : Nontrivial R
⊢ Summable fun k ↦ (-1) ^ k * (X ^ pentagonal (-↑k) - X ^ pentagonal (↑k + 1))

case refine_5
R : Type u_1
inst✝³ : CommRing R
inst✝² : TopologicalSpace R
inst✝¹ : IsTopologicalRing R
inst✝ : T2Space R
a✝ : Nontrivial R
⊢ Tendsto
    (fun k ↦
      (-1) ^ (k + 1) * X ^ ((k + 1) * (3 * k + 4) / 2) *
        ∑' (n : ℕ), X ^ ((k + 1) * n) * ∏ i ∈ Finset.range (n + 1), (1 - X ^ (k + i + 1)))
    atTop (𝓝 0)
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)
⊢ ↑(Fintype.card ↥H) ≤ (2 / ε - 1) * ↑(#S)

Tactic:
case =>

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

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

Tactic:
isBigO_exp_comp_exp_comp

Goal state after:
case refine_3
⊢ IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) atTop ((fun n ↦ -4 * √(Real.log ↑n)) - fun n ↦ -4 * √(Real.log ↑((n - 3) / 6)))
Module: Mathlib.Combinatorics.Graph.Basic

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

Tactic:
simp [h'.symm.right_unique h]

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)
⊢ ↑(#Z) ≤ 2 / ε - 1

Tactic:
case =>

Goal state after:
Module: Mathlib.Combinatorics.HalesJewett

Goal state before:
pp: η : Type u_1
α✝ : Type u_2
ι✝ : Type u_3
κ✝ : Type u_4
l : Line α✝ ι✝
i : ι✝
a x : α✝
α : Type ?u.18
ι : Type ?u.23
κ : Type ?u.22
C : (ι → Option α) → κ
⊢ Inhabited (ColorFocused C)

Tactic:
refine ⟨⟨0, fun _ => none, fun h => ?_, Multiset.nodup_zero⟩⟩

Goal state after:
η : Type u_1
α✝ : Type u_2
ι✝ : Type u_3
κ✝ : Type u_4
l : Line α✝ ι✝
i : ι✝
a x : α✝
α : Type ?u.18
ι : Type ?u.23
κ : Type ?u.22
C : (ι → Option α) → κ
h : AlmostMono C
⊢ h ∈ 0 → ↑h.line none = fun x ↦ none
Module: Mathlib.Combinatorics.HalesJewett

Goal state before:
pp: α : Type u
inst✝¹ : Fintype α
ihα : ∀ (κ : Type (max v u)) [Finite κ], ∃ ι x, ∀ (C : (ι → α) → κ), ∃ l, IsMono C l
κ : Type (max v u)
inst✝ : Finite κ
val✝ : Fintype κ
h : ¬Nonempty α
⊢ ∃ ι x, ∀ (C : (ι → Option α) → κ), ∃ l, IsMono C l

Tactic:
case =>

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]
      exact ⟨h, s.distinct_colors⟩

Goal state after:
Module: Mathlib.Combinatorics.Matroid.Sum

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

Tactic:
exact sigma_mono rfl.subset fun i ↦ (hJs i).2

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

Goal state before:
pp: α : Type u_1
M : Matroid α
I J X : Set α
h : M.IsBasis I X
hdj : Disjoint J X
h_ind : M.Indep (I ∪ J)
⊢ (M ／ J).IsBasis I X

Tactic:
rw [← hdj.sdiff_eq_right, ← (hdj.mono_right h.subset).sdiff_eq_right]
  exact h.contract_isBasis_of_indep h_ind

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

Goal state before:
pp: α : Type u_1
M : Matroid α
e : α
C : Set α
⊢ e ∈ (M.E \ C) \ (M.closure C \ C) ↔ e ∈ M.E \ M.closure C

Tactic:
refine ⟨fun ⟨he,heC⟩ ↦ ⟨he.1, fun h ↦ heC ⟨h, he.2⟩⟩,
    fun h ↦ ⟨⟨h.1, fun heC ↦ h.2 ?_⟩, fun h' ↦ h.2 h'.1⟩⟩

Goal state after:
α : Type u_1
M : Matroid α
e : α
C : Set α
h : e ∈ M.E \ M.closure C
heC : e ∈ C
⊢ e ∈ M.closure C
Module: Mathlib.Combinatorics.Matroid.Minor.Contract

Goal state before:
pp: α : Type u_1
M : Matroid α
X C : Set α
hC : C ⊆ M.E
⊢ Disjoint X C → X ⊆ M.E → (M.closure (X ∪ C) \ C = M.E \ C ↔ M.closure (X ∪ C) = M.E ∧ C ⊆ M.E)

Tactic:
refine fun hdj hX ↦ ⟨fun h ↦ ⟨?_, hC⟩, fun h ↦ by simp [h]⟩

Goal state after:
α : Type u_1
M : Matroid α
X C : Set α
hC : C ⊆ M.E
hdj : Disjoint X C
hX : X ⊆ M.E
h : M.closure (X ∪ C) \ C = M.E \ C
⊢ M.closure (X ∪ C) = M.E
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) := ⋯
hQ : Q = (optionEquivLeft R σ) P
x : σ → R
hx : ∀ (i : σ), x i ∈ S (Option.some i)
⊢ (Polynomial.map (eval x) Q).natDegree ≤ degreeOf none P

Tactic:
rw [Polynomial.natDegree_le_iff_coeff_eq_zero]

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)
⊢ ∀ (N : ℕ), degreeOf none P < N → (Polynomial.map (eval x) Q).coeff N = 0
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
m : σ →₀ ℕ
n : Option σ →₀ ℕ := (embDomain Embedding.some m).update none d
hn : n none = d ∧ n.some = m
⊢ coeff m (((optionEquivLeft R σ) P).coeff d) = 0

Tactic:
rw [← hn.1, ← hn.2, optionEquivLeft_coeff_some_coeff_none]

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
m : σ →₀ ℕ
n : Option σ →₀ ℕ := (embDomain Embedding.some m).update none d
hn : n none = d ∧ n.some = m
⊢ coeff n P = 0
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:
(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:
(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))
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}
hc : #(image f (sA.disjSum sB)) < #(sA.disjSum sB)
a b : ℕ
left✝ : Sum.inl a ≠ Sum.inr b
hxy : f (Sum.inl a) = f (Sum.inr b)
ha : (0 < a ∧ a ≤ n) ∧ a ∈ A
hb : (0 < b ∧ b ≤ n) ∧ b ∈ B
⊢ a ∈ A

Tactic:
by simp [*]

Goal state after:
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}
hc : #(image f (sA.disjSum sB)) < #(sA.disjSum sB)
a b : ℕ
left✝ : Sum.inl a ≠ Sum.inr b
hxy : f (Sum.inl a) = f (Sum.inr b)
ha : (0 < a ∧ a ≤ n) ∧ a ∈ A
hb : (0 < b ∧ b ≤ n) ∧ b ∈ B
⊢ b ∈ B

Tactic:
by simp [*]

Goal state after:
Module: Mathlib.Combinatorics.Schnirelmann

Goal state before:
pp: case neg.inl.inr
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)
a b : ℕ
left✝ : Sum.inl a ≠ Sum.inr b
hxy : f (Sum.inl a) = f (Sum.inr b)
ha : (0 < a ∧ a ≤ n) ∧ a ∈ A
hb : (0 < b ∧ b ≤ n) ∧ b ∈ B
⊢ n ∈ A + B

Tactic:
exact ⟨a, by simp [*], b, by simp [*], by grind⟩

Goal state after: