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

Goal state before:
pp: case neg
V : Type u
G : SimpleGraph V
s : ℕ
ih :
  ∀ m < s,
    ∀ {u v : V} {p q : G.Walk u v},
      p.IsPath →
        q.IsPath →
          p ≠ q → p.length = m → ∃ u' v' p' q', p'.IsSubwalk p ∧ q'.IsSubwalk q ∧ (p'.append q'.reverse).IsCycle
u v : V
p q : G.Walk u v
hp : p.IsPath
hq : q.IsPath
h : p ≠ q
hs : p.length = s
hw : ∀ w ∈ p.support, w ∈ q.support → w ≠ u → w = v
⊢ ∃ u' v' p' q', p'.IsSubwalk p ∧ q'.IsSubwalk q ∧ (p'.append q'.reverse).IsCycle

Tactic:
refine ⟨u, v, p, q, p.isSubwalk_rfl, q.isSubwalk_rfl, ?_⟩

Goal state after:
case neg
V : Type u
G : SimpleGraph V
s : ℕ
ih :
  ∀ m < s,
    ∀ {u v : V} {p q : G.Walk u v},
      p.IsPath →
        q.IsPath →
          p ≠ q → p.length = m → ∃ u' v' p' q', p'.IsSubwalk p ∧ q'.IsSubwalk q ∧ (p'.append q'.reverse).IsCycle
u v : V
p q : G.Walk u v
hp : p.IsPath
hq : q.IsPath
h : p ≠ q
hs : p.length = s
hw : ∀ w ∈ p.support, w ∈ q.support → w ≠ u → w = v
⊢ (p.append q.reverse).IsCycle
Module: Mathlib.Combinatorics.SimpleGraph.Triangle.Removal

Goal state before:
pp: α : Type u_1
inst✝² : DecidableEq α
inst✝¹ : Fintype α
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε : ℝ
hG : G.FarFromTriangleFree ε
h✝ : Nonempty α
hε : 0 < ε
l : ℕ := ⌈4 / ε⌉₊
hl : 4 / ε ≤ ↑l
hl' : Fintype.card α ≤ l
⊢ 1 ≤ ↑(#(G.cliqueFinset 3))

Tactic:
by simpa [one_le_iff_ne_zero] using (hG.cliqueFinset_nonempty hε).card_pos.ne'

Goal state after:
Module: Mathlib.Combinatorics.Configuration

Goal state before:
pp: case neg
P : Type u_1
L : Type u_2
inst✝² : Membership P L
inst✝¹ : HasLines P L
p : P
l : L
h : p ∉ l
inst✝ : Finite { l // p ∈ l }
hf : ¬Infinite { p // p ∈ l }
this : Fintype { p // p ∈ l }
⊢ pointCount P l ≤ lineCount L p

Tactic:
cases nonempty_fintype { l : L // p ∈ l }

Goal state after:
case neg.intro
P : Type u_1
L : Type u_2
inst✝² : Membership P L
inst✝¹ : HasLines P L
p : P
l : L
h : p ∉ l
inst✝ : Finite { l // p ∈ l }
hf : ¬Infinite { p // p ∈ l }
this : Fintype { p // p ∈ l }
val✝ : Fintype { l // p ∈ l }
⊢ pointCount P l ≤ lineCount L p
Module: Mathlib.Combinatorics.Derangements.Basic

Goal state before:
pp: case neg
α : Type u_1
inst✝ : DecidableEq α
a : α
f : Perm α
h_opfp : f ∈ {f | fixedPoints ⇑f ⊆ {a}}
x : α
x_vs_a : ¬x = a
ne_1 : some x ≠ none
⊢ some (f x) ≠ (Equiv.swap none (some a)) (some x)

Tactic:
have ne_2 : some x ≠ some a := (Option.some_injective α).ne_iff.mpr x_vs_a

Goal state after:
case neg
α : Type u_1
inst✝ : DecidableEq α
a : α
f : Perm α
h_opfp : f ∈ {f | fixedPoints ⇑f ⊆ {a}}
x : α
x_vs_a : ¬x = a
ne_1 : some x ≠ none
ne_2 : some x ≠ some a
⊢ some (f x) ≠ (Equiv.swap none (some a)) (some x)
Module: Mathlib.Combinatorics.Configuration

Goal state before:
pp: P : Type u_1
L : Type u_2
inst✝³ : Membership P L
inst✝² : HasLines P L
inst✝¹ : Fintype P
inst✝ : Fintype L
hc₂ : ¬Fintype.card P ≤ Fintype.card L
f : L → P
hf₁ : Function.Injective f
hf₂ : ∀ (l : L), f l ∉ l
⊢ ∑ p ∈ map { toFun := f, inj' := hf₁ } univ, lineCount L p < ∑ p, lineCount L p

Tactic:
by
        obtain ⟨p, hp⟩ := not_forall.mp (mt (Fintype.card_le_of_surjective f) hc₂)
        refine sum_lt_sum_of_subset (subset_univ _) (mem_univ p) ?_ ?_ fun p _ _ ↦ zero_le
        · simpa only [Finset.mem_map, exists_prop, Finset.mem_univ, true_and]
        · rw [lineCount, Nat.card_eq_fintype_card, Fintype.card_pos_iff]
          obtain ⟨l, _⟩ := @exists_line P L _ _ p
          exact
            let := not_exists.mp hp l
            ⟨⟨mkLine this, (mkLine_ax this).2⟩⟩

Goal state after:
Module: Mathlib.Combinatorics.Configuration

Goal state before:
pp: K : Type u_3
inst✝ : Field K
a b c d : Fin 3 → K
hac : a ⬝ᵥ c = 0
hbc : b ⬝ᵥ c = 0
had : a ⬝ᵥ d = 0
hbd : b ⬝ᵥ d = 0
⊢ (crossProduct a) b = 0 ∨ (crossProduct c) d = 0

Tactic:
by
  by_contra h
  simp_rw [not_or, ← ne_eq, crossProduct_ne_zero_iff_linearIndependent] at h
  rw [← Matrix.of_row (![a, b]), ← Matrix.of_row (![c, d])] at h
  let A : Matrix (Fin 2) (Fin 3) K := .of ![a, b]
  let B : Matrix (Fin 2) (Fin 3) K := .of ![c, d]
  have hAB : A * B.transpose = 0 := by
    ext i j
    fin_cases i <;> fin_cases j <;> assumption
  replace hAB := rank_add_rank_le_card_of_mul_eq_zero hAB
  rw [rank_transpose, h.1.rank_matrix, h.2.rank_matrix, Fintype.card_fin, Fintype.card_fin] at hAB
  contradiction

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

Goal state before:
pp: p : DyckWord
⊢ ↑p = [] ↔ p = 0

Tactic:
by rw [DyckWord.ext_iff]; rfl

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

Goal state before:
pp: case neg
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
hmem : a ∉ m.toFinset.erase 0
⊢ (count a m)! * rest = ∏ j ∈ m.toFinset.erase 0, (count j m)!

Tactic:
have hcount : m.count a = 0 := by grind [Multiset.count_eq_zero_of_notMem]
        simp [rest, Finset.erase_eq_of_notMem hmem, hcount]

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

Goal state before:
pp: case neg
m n : ℕ
hm : ¬m = 0
hn : ¬n = 0
⊢ (multinomial {n} fun k ↦ k * count k (replicate m n)) *
      ∏ x ∈ {n}.erase 0, ∏ j ∈ Finset.range (count x (replicate m n)), (j * x + x - 1).choose (x - 1) =
    ∏ p ∈ Finset.range m, (p * n + n - 1).choose (n - 1)

Tactic:
show ({n} : Finset ℕ).erase 0 = {n} by simp [Ne.symm hn]

Goal state after:
case neg
m n : ℕ
hm : ¬m = 0
hn : ¬n = 0
⊢ (multinomial {n} fun k ↦ k * count k (replicate m n)) *
      ∏ x ∈ {n}, ∏ j ∈ Finset.range (count x (replicate m n)), (j * x + x - 1).choose (x - 1) =
    ∏ p ∈ Finset.range m, (p * n + n - 1).choose (n - 1)
Module: Mathlib.Combinatorics.Enumerative.Bell

Goal state before:
pp: case neg
m n : ℕ
hn : n ≠ 0
hm : ¬m = 0
⊢ m ! = ∏ x ∈ {n}.erase 0, (count x (replicate m n))!

Tactic:
show ({n} : Finset ℕ).erase 0 = {n} by simp [Ne.symm hn]

Goal state after:
case neg
m n : ℕ
hn : n ≠ 0
hm : ¬m = 0
⊢ m ! = ∏ x ∈ {n}, (count x (replicate m n))!
Module: Mathlib.Combinatorics.Enumerative.IncidenceAlgebra

Goal state before:
pp: case a
𝕜 : Type u_2
α : Type u_5
inst✝⁵ : AddCommGroup 𝕜
inst✝⁴ : MulOneClass 𝕜
inst✝³ : PartialOrder α
inst✝² : LocallyFiniteOrder α
inst✝¹ : DecidableEq α
inst✝ : DecidableLE α
a b : α
a✝ : a ≤ b
x : α
hx : x ∈ Icc a b
⊢ (mu 𝕜) a x * (zeta 𝕜) x b = (mu 𝕜) a x

Tactic:
simp [(mem_Icc.1 hx).2]

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

Goal state before:
pp: 𝕜 : Type u_2
α : Type u_5
inst✝⁵ : AddCommGroup 𝕜
inst✝⁴ : MulOneClass 𝕜
inst✝³ : PartialOrder α
inst✝² : LocallyFiniteOrder α
inst✝¹ : DecidableEq α
inst✝ : DecidableLE α
a b : α
a✝ : a ≤ b
⊢ (zeta 𝕜 * mu' 𝕜) a b = ∑ x ∈ Icc a b, (mu' 𝕜) x b

Tactic:
by rw [mul_apply]; congr! with x hx; simp [(mem_Icc.1 hx).1]

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

Goal state before:
pp: case pos.refine_2
R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : TopologicalSpace R
inst✝ : T2Space R
f : ℕ → ℕ → R
d : ℕ
s : Finset ℕ
hs0 : 0 ∉ s
g : ℕ →₀ ℕ
hg : g ∈ s.finsuppAntidiag d
x : ℕ
hx : x ∈ s
hprod : ¬x ∣ g x
hx0 : x ≠ 0
i : ℕ
⊢ (coeff (g x)) (f x (i + 1) • X ^ (x * (i + 1))) = 0

Tactic:
rw [map_smul, coeff_X_pow]

Goal state after:
case pos.refine_2
R : Type u_1
inst✝² : CommSemiring R
inst✝¹ : TopologicalSpace R
inst✝ : T2Space R
f : ℕ → ℕ → R
d : ℕ
s : Finset ℕ
hs0 : 0 ∉ s
g : ℕ →₀ ℕ
hg : g ∈ s.finsuppAntidiag d
x : ℕ
hx : x ∈ s
hprod : ¬x ∣ g x
hx0 : x ≠ 0
i : ℕ
⊢ (f x (i + 1) • if g x = x * (i + 1) then 1 else 0) = 0
Module: Mathlib.Combinatorics.Enumerative.IncidenceAlgebra

Goal state before:
pp: 𝕜 : Type u_2
α : Type u_5
β : Type u_6
inst✝⁸ : Ring 𝕜
inst✝⁷ : PartialOrder α
inst✝⁶ : PartialOrder β
inst✝⁵ : LocallyFiniteOrder α
inst✝⁴ : LocallyFiniteOrder β
inst✝³ : DecidableEq α
inst✝² : DecidableEq β
inst✝¹ : DecidableLE α
inst✝ : DecidableLE β
⊢ (mu 𝕜).prod (mu 𝕜) * (zeta 𝕜).prod (zeta 𝕜) = 1

Tactic:
prod_mul_prod',

Goal state after:
𝕜 : Type u_2
α : Type u_5
β : Type u_6
inst✝⁸ : Ring 𝕜
inst✝⁷ : PartialOrder α
inst✝⁶ : PartialOrder β
inst✝⁵ : LocallyFiniteOrder α
inst✝⁴ : LocallyFiniteOrder β
inst✝³ : DecidableEq α
inst✝² : DecidableEq β
inst✝¹ : DecidableLE α
inst✝ : DecidableLE β
⊢ (mu 𝕜 * zeta 𝕜).prod (mu 𝕜 * zeta 𝕜) = 1

case h
𝕜 : Type u_2
α : Type u_5
β : Type u_6
inst✝⁸ : Ring 𝕜
inst✝⁷ : PartialOrder α
inst✝⁶ : PartialOrder β
inst✝⁵ : LocallyFiniteOrder α
inst✝⁴ : LocallyFiniteOrder β
inst✝³ : DecidableEq α
inst✝² : DecidableEq β
inst✝¹ : DecidableLE α
inst✝ : DecidableLE β
⊢ ∀ (a₁ a₂ a₃ : α) (b₁ b₂ b₃ : β),
    (mu 𝕜) a₁ a₂ * (mu 𝕜) b₁ b₂ * ((zeta 𝕜) a₂ a₃ * (zeta 𝕜) b₂ b₃) =
      (mu 𝕜) a₁ a₂ * (zeta 𝕜) a₂ a₃ * ((mu 𝕜) b₁ b₂ * (zeta 𝕜) b₂ b₃)
Module: Mathlib.Combinatorics.Enumerative.Partition.Glaisher

Goal state before:
pp: case e'_5
R : Type u_1
inst✝² : TopologicalSpace R
inst✝¹ : T2Space R
inst✝ : CommSemiring R
m : ℕ
hm : 0 < m
a✝ : Nontrivial R
i : ℕ
⊢ ∑ j ∈ range m, X ^ ((i + 1) * j) = 1 + ∑' (j : ℕ), (if j + 1 < m then 1 else 0) • X ^ ((i + 1) * (j + 1))

Tactic:
rw [sum_range_eq_add_Ico _ hm, sum_Ico_eq_sum_range]

Goal state after:
case e'_5
R : Type u_1
inst✝² : TopologicalSpace R
inst✝¹ : T2Space R
inst✝ : CommSemiring R
m : ℕ
hm : 0 < m
a✝ : Nontrivial R
i : ℕ
⊢ X ^ ((i + 1) * 0) + ∑ k ∈ range (m - 1), X ^ ((i + 1) * (1 + k)) =
    1 + ∑' (j : ℕ), (if j + 1 < m then 1 else 0) • X ^ ((i + 1) * (j + 1))
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 : ℕ
⊢ ∑ k ∈ range (m - 1), X ^ ((i + 1) * (1 + k)) =
    ∑ k ∈ range (m - 1), (if k + 1 < m then 1 else 0) • X ^ ((i + 1) * (k + 1))

pp: R : Type u_1
inst✝² : TopologicalSpace R
inst✝¹ : T2Space R
inst✝ : CommSemiring R
m : ℕ
hm : 0 < m
a✝ : Nontrivial R
i : ℕ
⊢ ∑ k ∈ range (m - 1), (if k + 1 < m then 1 else 0) • X ^ ((i + 1) * (k + 1)) =
    ∑' (j : ℕ), (if j + 1 < m then 1 else 0) • X ^ ((i + 1) * (j + 1))

Tactic:
· refine sum_congr rfl fun b hn ↦ ?_
      rw [add_comm 1 b]
      have : b + 1 < m := by grind
      simp [this]

Goal state after:
R : Type u_1
inst✝² : TopologicalSpace R
inst✝¹ : T2Space R
inst✝ : CommSemiring R
m : ℕ
hm : 0 < m
a✝ : Nontrivial R
i : ℕ
⊢ ∑ k ∈ range (m - 1), (if k + 1 < m then 1 else 0) • X ^ ((i + 1) * (k + 1)) =
    ∑' (j : ℕ), (if j + 1 < m then 1 else 0) • X ^ ((i + 1) * (j + 1))
Module: Mathlib.Combinatorics.Enumerative.Pentagonal.Ring

Goal state before:
pp: 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 : ℕ), powMulProdOneSubPow n✝ n x
n : ℕ
⊢ (n + 1 + 1) * (3 * (n + 1) + 2) / 2 = (n + 1) * (3 * n + 4) / 2 + (2 * n + 3)

Tactic:
rw [← Nat.add_mul_div_left _ _ (by simp)]

Goal state after:
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 : ℕ), powMulProdOneSubPow n✝ n x
n : ℕ
⊢ (n + 1 + 1) * (3 * (n + 1) + 2) / 2 = ((n + 1) * (3 * n + 4) + 2 * (2 * n + 3)) / 2
Module: Mathlib.Combinatorics.Enumerative.Pentagonal.Ring

Goal state before:
pp: 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 : ℕ), powMulProdOneSubPow n✝ n x
h : ∀ (n : ℕ), (n + 1 + 1) * (3 * (n + 1) + 2) / 2 = (n + 1) * (3 * n + 4) / 2 + (2 * n + 3)
n : ℕ
⊢ (n + 1 + 1) * (3 * (n + 1) + 4) / 2 = (n + 1) * (3 * n + 4) / 2 + (3 * n + 5)

Tactic:
rw [← Nat.add_mul_div_left _ _ (by simp)]

Goal state after:
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 : ℕ), powMulProdOneSubPow n✝ n x
h : ∀ (n : ℕ), (n + 1 + 1) * (3 * (n + 1) + 2) / 2 = (n + 1) * (3 * n + 4) / 2 + (2 * n + 3)
n : ℕ
⊢ (n + 1 + 1) * (3 * (n + 1) + 4) / 2 = ((n + 1) * (3 * n + 4) + 2 * (3 * n + 5)) / 2
Module: Mathlib.Combinatorics.HalesJewett

Goal state before:
pp: η : Type u_5
α : Type u_6
ι : Type u_7
l : Subspace η α ι
x : η → α
i : ι
a : α
h : l.idxFun i = Sum.inl a
⊢ ↑l x i = a

Tactic:
simp [apply_def, h]

Goal state after:
Module: Mathlib.Combinatorics.HalesJewett

Goal state before:
pp: η : Type u_5
α : Type u_6
ι : Type u_7
l : Subspace η α ι
x : η → α
i : ι
e : η
h : l.idxFun i = Sum.inr e
⊢ ↑l x i = x e

Tactic:
simp [apply_def, h]

Goal state after:
Module: Mathlib.Combinatorics.Hindman

Goal state before:
pp: case head'
M : Type u_1
inst✝ : Semigroup M
a✝ : Stream' M
m : M
a : Stream' M
⊢ ∃ n, ∀ m' ∈ FP (Stream'.drop n a), a.head * m' ∈ FP a

Tactic:
| head' a =>

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

Goal state before:
pp: α : Type u_1
M : Matroid α
e : α
D : Set α
⊢ (M ＼ D).IsNonloop e ↔ M.IsNonloop e ∧ e ∉ D

Tactic:
rw [← indep_singleton, delete_indep_iff, disjoint_singleton_left, indep_singleton]

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

Goal state before:
pp: α : Type u_1
e : α
M : Matroid α
D : Set α
⊢ (M ＼ D).IsColoop e ↔ e ∉ M.closure ((M.E \ D) \ {e}) ∧ e ∈ M.E ∧ e ∉ D

Tactic:
rw [delete_eq_restrict, restrict_isColoop_iff sdiff_subset, mem_sdiff, and_congr_left_iff]
  simp

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
⊢ (Multiset.map (fun p ↦ { line := p.line.prod (map some l'), color := p.color, has_color := ⋯ }) s.lines).card + 1 =
    r + 1

Tactic:
Multiset.card_map,

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
⊢ s.lines.card + 1 = r + 1
Module: Mathlib.Combinatorics.Matroid.Minor.Contract

Goal state before:
pp: α : Type u_1
M : Matroid α
I J X : Set α
h : M.IsBasis' (J ∪ I) (X ∪ I)
hJI : Disjoint J I
hXI : Disjoint X I
⊢ (M ／ I).IsBasis' J X

Tactic:
simpa [hJI.sdiff_eq_left, hXI.sdiff_eq_left] using
    h.contract_isBasis'_sdiff_sdiff_of_subset subset_union_right

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

Goal state before:
pp: α : Type u_1
M : Matroid α
I X : Set α
hI : M.IsBasis' I X
D : Set α
⊢ (M ／ X).Dep D ↔ M.Dep (D ∪ I) ∧ Disjoint X D

Tactic:
rw [hI.contract_eq_contract_delete, delete_dep_iff, hI.indep.contract_dep_iff, and_comm,
    ← and_assoc, ← disjoint_union_right, sdiff_union_of_subset hI.subset, disjoint_comm, and_comm]

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

Goal state before:
pp: ι : 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
⊢ ∃ J, I ⊆ J ∧ Maximal (fun K ↦ (fun I ↦ ∀ (i : ι), (M i).Indep (Sigma.mk i ⁻¹' I)) K ∧ K ⊆ X) J

Tactic:
by
    choose Js hJs using
      fun i ↦ (hI i).subset_isBasis'_of_subset (preimage_mono (f := Sigma.mk i) hIX)
    use univ.sigma Js
    simp only [maximal_subset_iff', mem_univ, mk_preimage_sigma, and_imp]
    refine ⟨?_, ⟨fun i ↦ (hJs i).1.indep, ?_⟩, fun S hS hSX hJS ↦ ?_⟩
    · rw [← univ_sigma_preimage_mk I]
      exact sigma_mono rfl.subset fun i ↦ (hJs i).2
    · rw [← univ_sigma_preimage_mk X]
      exact sigma_mono rfl.subset fun i ↦ (hJs i).1.subset
    rw [← univ_sigma_preimage_mk S]
    refine sigma_mono rfl.subset fun i ↦ ?_
    rw [sigma_subset_iff] at hJS
    rw [(hJs i).1.eq_of_subset_indep (hS i) (hJS <| mem_univ i)]
    exact preimage_mono hSX

Goal state after:
Module: Mathlib.Combinatorics.Quiver.Arborescence

Goal state before:
pp: V : Type u
inst✝ : Quiver V
r : V
height : V → ℕ
height_lt : ∀ ⦃a b : V⦄ (a_1 : a ⟶ b), height a < height b
unique_arrow : ∀ ⦃a b c : V⦄ (e : a ⟶ c) (f : b ⟶ c), a = b ∧ e ≍ f
root_or_arrow : ∀ (b : V), b = r ∨ ∃ a, Nonempty (a ⟶ b)
b : V
⊢ ∀ (a : Path r b), a = default

Tactic:
by
      have height_le : ∀ {a b}, Path a b → height a ≤ height b := by
        intro a b p
        induction p with
        | nil => rfl
        | cons _ e ih => exact le_of_lt (lt_of_le_of_lt ih (height_lt e))
      suffices ∀ p q : Path r b, p = q by
        intro p
        apply this
      intro p q
      induction p with
      | nil =>
        rcases q with _ | ⟨q, f⟩
        · rfl
        · exact False.elim (lt_irrefl _ (lt_of_le_of_lt (height_le q) (height_lt f)))
      | cons p e ih =>
        rcases q with _ | ⟨q, f⟩
        · exact False.elim (lt_irrefl _ (lt_of_le_of_lt (height_le p) (height_lt e)))
        · rcases unique_arrow e f with ⟨⟨⟩, ⟨⟩⟩
          rw [ih]

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 + 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
i : σ
⊢ ⊥ < #(S i)

Tactic:
by simp [Sne i]

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
u : U
⊢ ⇑(Quiver.symmetrifyStar (φ.obj u)) ∘ φ.symmetrify.star u =
    Sum.map (φ.star u) (φ.costar u) ∘ ⇑(Quiver.symmetrifyStar u)

Tactic:
ext ⟨v, f | g⟩ <;>
    -- Porting note (https://github.com/leanprover-community/mathlib4/issues/10745): was `simp [Quiver.symmetrifyStar]`
    simp only [Quiver.symmetrifyStar, Function.comp_apply] <;>
    erw [Equiv.sigmaSumDistrib_apply, Equiv.sigmaSumDistrib_apply]

Goal state after:
case inl
U : Type u_1
inst✝¹ : Quiver U
V : Type u_2
inst✝ : Quiver V
φ : U ⥤q V
u : U
v : Symmetrify U
f : u ⟶ v
⊢ Sum.map (Sigma.mk (φ.symmetrify.star u ⟨v, Sum.inl f⟩).fst) (Sigma.mk (φ.symmetrify.star u ⟨v, Sum.inl f⟩).fst)
      (φ.symmetrify.star u ⟨v, Sum.inl f⟩).snd =
    Sum.map (φ.star u) (φ.costar u)
      (Sum.map (Sigma.mk ⟨v, Sum.inl f⟩.fst) (Sigma.mk ⟨v, Sum.inl f⟩.fst) ⟨v, Sum.inl f⟩.snd)

case inr
U : Type u_1
inst✝¹ : Quiver U
V : Type u_2
inst✝ : Quiver V
φ : U ⥤q V
u : U
v : Symmetrify U
g : v ⟶ u
⊢ Sum.map (Sigma.mk (φ.symmetrify.star u ⟨v, Sum.inr g⟩).fst) (Sigma.mk (φ.symmetrify.star u ⟨v, Sum.inr g⟩).fst)
      (φ.symmetrify.star u ⟨v, Sum.inr g⟩).snd =
    Sum.map (φ.star u) (φ.costar u)
      (Sum.map (Sigma.mk ⟨v, Sum.inr g⟩.fst) (Sigma.mk ⟨v, Sum.inr g⟩.fst) ⟨v, Sum.inr g⟩.snd)
Module: Mathlib.Combinatorics.SetFamily.Shadow

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
𝒜 : Finset (Finset α)
t s : Finset α
hs : s ∈ 𝒜
hst : s ⊆ t
⊢ t \ (t \ s) ∈ 𝒜

Tactic:
by rwa [sdiff_sdiff_eq_self hst]

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

Goal state before:
pp: α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
s : Finset α
inst✝ : Nonempty α
hs : s ≠ univ
this :
  ∀ (t : Finset α),
    (↑(card α) - ↑(#({s}.truncatedSup t))) / ((↑(card α) - ↑(#t)) * ↑((card α).choose #t)) =
      if t ⊆ s then (↑(card α) - ↑(#s)) / ((↑(card α) - ↑(#t)) * ↑((card α).choose #t)) else 0
⊢ 1 = ∑ t, if t ⊆ s then (↑(card α) - ↑(#s)) / ((↑(card α) - ↑(#t)) * ↑((card α).choose #t)) else 0

Tactic:
sum_ite,

Goal state after:
α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
s : Finset α
inst✝ : Nonempty α
hs : s ≠ univ
this :
  ∀ (t : Finset α),
    (↑(card α) - ↑(#({s}.truncatedSup t))) / ((↑(card α) - ↑(#t)) * ↑((card α).choose #t)) =
      if t ⊆ s then (↑(card α) - ↑(#s)) / ((↑(card α) - ↑(#t)) * ↑((card α).choose #t)) else 0
⊢ 1 = ∑ x with x ⊆ s, (↑(card α) - ↑(#s)) / ((↑(card α) - ↑(#x)) * ↑((card α).choose #x)) + ∑ x with ¬x ⊆ s, 0
Module: Mathlib.Combinatorics.SetFamily.AhlswedeZhang

Goal state before:
pp: α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
s : Finset α
inst✝ : Nonempty α
hs : s ≠ univ
this :
  ∀ (t : Finset α),
    (↑(card α) - ↑(#({s}.truncatedSup t))) / ((↑(card α) - ↑(#t)) * ↑((card α).choose #t)) =
      if t ⊆ s then (↑(card α) - ↑(#s)) / ((↑(card α) - ↑(#t)) * ↑((card α).choose #t)) else 0
⊢ 1 = ∑ x with x ⊆ s, (↑(card α) - ↑(#s)) / ((↑(card α) - ↑(#x)) * ↑((card α).choose #x)) + ∑ x with ¬x ⊆ s, 0

Tactic:
sum_const_zero,

Goal state after:
α : Type u_1
inst✝² : Fintype α
inst✝¹ : DecidableEq α
s : Finset α
inst✝ : Nonempty α
hs : s ≠ univ
this :
  ∀ (t : Finset α),
    (↑(card α) - ↑(#({s}.truncatedSup t))) / ((↑(card α) - ↑(#t)) * ↑((card α).choose #t)) =
      if t ⊆ s then (↑(card α) - ↑(#s)) / ((↑(card α) - ↑(#t)) * ↑((card α).choose #t)) else 0
⊢ 1 = ∑ x with x ⊆ s, (↑(card α) - ↑(#s)) / ((↑(card α) - ↑(#x)) * ↑((card α).choose #x)) + 0
Module: Mathlib.Combinatorics.SetFamily.Compression.UV

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
u v : Finset α
huv : ∀ x ∈ u, ∃ y ∈ v, IsCompressed (u.erase x) (v.erase y) 𝒜
⊢ ∂ (𝓒 u v 𝒜) ⊆ 𝓒 u v (∂ 𝒜)

Tactic:
set 𝒜' := 𝓒 u v 𝒜

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
𝒜 : Finset (Finset α)
u v : Finset α
huv : ∀ x ∈ u, ∃ y ∈ v, IsCompressed (u.erase x) (v.erase y) 𝒜
𝒜' : Finset (Finset α) := 𝓒 u v 𝒜
⊢ ∂ 𝒜' ⊆ 𝓒 u v (∂ 𝒜)