mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.ContinuedFractions.ConvergentsEquiv

Goal state before:
pp: case inr
K : Type u_1
n : ℕ
g : GenContFract K
inst✝ : Field K
nth_partDen_ne_zero : ∀ {b : K}, g.partDens.get? n = some b → b ≠ 0
not_terminatedAt_n : ¬g.TerminatedAt n
a b : K
s_nth_eq : g.s.get? n = some { a := a, b := b }
b_ne_zero : b ≠ 0
⊢ g.convs (n + 1) = (g.squashGCF n).convs n

Tactic:
cases n with

Goal state after:
Module: Mathlib.Algebra.ContinuedFractions.ConvergentsEquiv

Goal state before:
pp: case refl
K : Type u_1
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
g : GenContFract K
gp' : Pair K
m : ℕ
IH :
  ∀ {g : GenContFract K},
    (∀ {gp : Pair K} {m_1 : ℕ}, m_1 < m.succ → g.s.get? m_1 = some gp → 0 < gp.a ∧ 0 < gp.b) →
      g.convs m.succ = g.convs' m.succ
s_pos : ∀ {gp : Pair K} {m_1 : ℕ}, m_1 < m.succ + 1 → g.s.get? m_1 = some gp → 0 < gp.a ∧ 0 < gp.b
g' : GenContFract K := g.squashGCF m.succ
not_terminatedAt_n : ¬g.TerminatedAt m.succ
this : g.convs (m.succ + 1) = g'.convs m.succ
s_mth_eq' : g'.s.get? m = some gp'
gp_succ_m : Pair K
s_succ_mth_eq : g.s.get? (m + 1) = some gp_succ_m
gp_m : Pair K
mth_s_eq : g.s.get? m = some gp_m
m_lt_n : m < m.succ
⊢ 0 < gp_m.b + gp_succ_m.a / gp_succ_m.b

Tactic:
refine add_pos (s_pos (Nat.lt_succ_of_lt m_lt_n) mth_s_eq).right ?_

Goal state after:
case refl
K : Type u_1
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
g : GenContFract K
gp' : Pair K
m : ℕ
IH :
  ∀ {g : GenContFract K},
    (∀ {gp : Pair K} {m_1 : ℕ}, m_1 < m.succ → g.s.get? m_1 = some gp → 0 < gp.a ∧ 0 < gp.b) →
      g.convs m.succ = g.convs' m.succ
s_pos : ∀ {gp : Pair K} {m_1 : ℕ}, m_1 < m.succ + 1 → g.s.get? m_1 = some gp → 0 < gp.a ∧ 0 < gp.b
g' : GenContFract K := g.squashGCF m.succ
not_terminatedAt_n : ¬g.TerminatedAt m.succ
this : g.convs (m.succ + 1) = g'.convs m.succ
s_mth_eq' : g'.s.get? m = some gp'
gp_succ_m : Pair K
s_succ_mth_eq : g.s.get? (m + 1) = some gp_succ_m
gp_m : Pair K
mth_s_eq : g.s.get? m = some gp_m
m_lt_n : m < m.succ
⊢ 0 < gp_succ_m.a / gp_succ_m.b
Module: Mathlib.Algebra.ContinuedFractions.Computation.Approximations

Goal state before:
pp: K : Type u_1
v : K
n : ℕ
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : FloorRing K
hyp : n = 0 ∨ ¬(of v).TerminatedAt (n - 1)
⊢ n + 1 ≤ 1 ∨ ¬(of v).TerminatedAt (n - 1)

Tactic:
cases n with

Goal state after:
Module: Mathlib.Algebra.CubicDiscriminant

Goal state before:
pp: case a
R : Type u_1
S : Type u_2
F : Type u_3
K : Type u_4
P✝ Q : Cubic R
a b c d a' b' c' d' : R
inst✝ : Semiring R
P : Cubic R
⊢ ((fun f ↦ { a := (↑f).coeff 3, b := (↑f).coeff 2, c := (↑f).coeff 1, d := (↑f).coeff 0 })
        ((fun P ↦ ⟨P.toPoly, ⋯⟩) P)).a =
    P.a

Tactic:
simp only [coeffs]

Goal state after:
Module: Mathlib.Algebra.CubicDiscriminant

Goal state before:
pp: case b
R : Type u_1
S : Type u_2
F : Type u_3
K : Type u_4
P✝ Q : Cubic R
a b c d a' b' c' d' : R
inst✝ : Semiring R
P : Cubic R
⊢ ((fun f ↦ { a := (↑f).coeff 3, b := (↑f).coeff 2, c := (↑f).coeff 1, d := (↑f).coeff 0 })
        ((fun P ↦ ⟨P.toPoly, ⋯⟩) P)).b =
    P.b

Tactic:
simp only [coeffs]

Goal state after:
Module: Mathlib.Algebra.CubicDiscriminant

Goal state before:
pp: case c
R : Type u_1
S : Type u_2
F : Type u_3
K : Type u_4
P✝ Q : Cubic R
a b c d a' b' c' d' : R
inst✝ : Semiring R
P : Cubic R
⊢ ((fun f ↦ { a := (↑f).coeff 3, b := (↑f).coeff 2, c := (↑f).coeff 1, d := (↑f).coeff 0 })
        ((fun P ↦ ⟨P.toPoly, ⋯⟩) P)).c =
    P.c

Tactic:
simp only [coeffs]

Goal state after:
Module: Mathlib.Algebra.CubicDiscriminant

Goal state before:
pp: case d
R : Type u_1
S : Type u_2
F : Type u_3
K : Type u_4
P✝ Q : Cubic R
a b c d a' b' c' d' : R
inst✝ : Semiring R
P : Cubic R
⊢ ((fun f ↦ { a := (↑f).coeff 3, b := (↑f).coeff 2, c := (↑f).coeff 1, d := (↑f).coeff 0 })
        ((fun P ↦ ⟨P.toPoly, ⋯⟩) P)).d =
    P.d

Tactic:
simp only [coeffs]

Goal state after:
Module: Mathlib.Algebra.CubicDiscriminant

Goal state before:
pp: case inl.«0»
R : Type u_1
S : Type u_2
F : Type u_3
K : Type u_4
P Q : Cubic R
a b c d a' b' c' d' : R
inst✝ : Semiring R
f : { p // p.degree ≤ 3 }
n : ℕ
hn : 0 ≤ 3
⊢ { a := (↑f).coeff 3, b := (↑f).coeff 2, c := (↑f).coeff 1, d := (↑f).coeff 0 }.toPoly.coeff 0 = (↑f).coeff 0

Tactic:
simp only [coeffs]

Goal state after:
Module: Mathlib.Algebra.CubicDiscriminant

Goal state before:
pp: case inl.«1»
R : Type u_1
S : Type u_2
F : Type u_3
K : Type u_4
P Q : Cubic R
a b c d a' b' c' d' : R
inst✝ : Semiring R
f : { p // p.degree ≤ 3 }
n : ℕ
hn : 1 ≤ 3
⊢ { a := (↑f).coeff 3, b := (↑f).coeff 2, c := (↑f).coeff 1, d := (↑f).coeff 0 }.toPoly.coeff 1 = (↑f).coeff 1

Tactic:
simp only [coeffs]

Goal state after:
Module: Mathlib.Algebra.CubicDiscriminant

Goal state before:
pp: case inl.«2»
R : Type u_1
S : Type u_2
F : Type u_3
K : Type u_4
P Q : Cubic R
a b c d a' b' c' d' : R
inst✝ : Semiring R
f : { p // p.degree ≤ 3 }
n : ℕ
hn : 2 ≤ 3
⊢ { a := (↑f).coeff 3, b := (↑f).coeff 2, c := (↑f).coeff 1, d := (↑f).coeff 0 }.toPoly.coeff 2 = (↑f).coeff 2

Tactic:
simp only [coeffs]

Goal state after:
Module: Mathlib.Algebra.CubicDiscriminant

Goal state before:
pp: case inl.«3»
R : Type u_1
S : Type u_2
F : Type u_3
K : Type u_4
P Q : Cubic R
a b c d a' b' c' d' : R
inst✝ : Semiring R
f : { p // p.degree ≤ 3 }
n : ℕ
hn : 3 ≤ 3
⊢ { a := (↑f).coeff 3, b := (↑f).coeff 2, c := (↑f).coeff 1, d := (↑f).coeff 0 }.toPoly.coeff 3 = (↑f).coeff 3

Tactic:
simp only [coeffs]

Goal state after:
Module: Mathlib.Algebra.ContinuedFractions.Computation.Approximations

Goal state before:
pp: K : Type u_1
v : K
n : ℕ
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : FloorRing K
not_terminatedAt_n : ¬(of v).TerminatedAt n
g : GenContFract K := of v
nextConts : Pair K := g.contsAux (n + 2)
conts : Pair K := g.contsAux (n + 1)
conts_eq : conts = g.contsAux (n + 1)
pred_conts : Pair K := g.contsAux n
pred_conts_eq : pred_conts = g.contsAux n
gp : Pair K
s_nth_eq : g.s.get? n = some gp
gp_a_eq_one : gp.a = 1
⊢ |v - g.convs n| ≤ 1 / (conts.b * nextConts.b)

Tactic:
have nextConts_b_eq : nextConts.b = pred_conts.b + gp.b * conts.b := by
    simp [nextConts, contsAux_recurrence s_nth_eq pred_conts_eq conts_eq, gp_a_eq_one,
      pred_conts_eq.symm, conts_eq.symm, add_comm]

Goal state after:
K : Type u_1
v : K
n : ℕ
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : FloorRing K
not_terminatedAt_n : ¬(of v).TerminatedAt n
g : GenContFract K := of v
nextConts : Pair K := g.contsAux (n + 2)
conts : Pair K := g.contsAux (n + 1)
conts_eq : conts = g.contsAux (n + 1)
pred_conts : Pair K := g.contsAux n
pred_conts_eq : pred_conts = g.contsAux n
gp : Pair K
s_nth_eq : g.s.get? n = some gp
gp_a_eq_one : gp.a = 1
nextConts_b_eq : nextConts.b = pred_conts.b + gp.b * conts.b
⊢ |v - g.convs n| ≤ 1 / (conts.b * nextConts.b)
Module: Mathlib.LinearAlgebra.GeneralLinearGroup.AlgEquiv

Goal state before:
pp: K : Type u_1
V : Type u_2
W : Type u_3
inst✝⁶ : Semifield K
inst✝⁵ : AddCommMonoid V
inst✝⁴ : Module K V
inst✝³ : Projective K V
inst✝² : AddCommMonoid W
inst✝¹ : Module K W
inst✝ : Projective K W
f : End K V ≃ₐ[K] End K W
hV : Nontrivial V
u : V
hu : u ≠ 0
v : Dual K V
huv : v u ≠ 0
⊢ ¬∀ (x : W), (f (smulRight v u)) x = 0 x

Tactic:
← LinearMap.ext_iff,

Goal state after:
K : Type u_1
V : Type u_2
W : Type u_3
inst✝⁶ : Semifield K
inst✝⁵ : AddCommMonoid V
inst✝⁴ : Module K V
inst✝³ : Projective K V
inst✝² : AddCommMonoid W
inst✝¹ : Module K W
inst✝ : Projective K W
f : End K V ≃ₐ[K] End K W
hV : Nontrivial V
u : V
hu : u ≠ 0
v : Dual K V
huv : v u ≠ 0
⊢ ¬f (smulRight v u) = 0
Module: Mathlib.LinearAlgebra.Eigenspace.Basic

Goal state before:
pp: R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
⊢ (f.genEigenspace μ) 0 = ⊥

Tactic:
by
  ext; apply mem_genEigenspace_zero

Goal state after:
Module: Mathlib.LinearAlgebra.Eigenspace.Basic

Goal state before:
pp: R : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
f : End R M
μ₁ μ₂ : R
hμ : μ₁ ≠ μ₂
k✝ l✝ : ℕ∞
k : ℕ
property✝¹ : ↑k ≤ k✝
l : ℕ
property✝ : ↑l ≤ l✝
a✝ : Nontrivial M
p : Submodule R M := (f.genEigenspace μ₁) ↑k ⊓ (f.genEigenspace μ₂) ↑l
hp : ¬p = ⊥
⊢ False

Tactic:
replace hp : Nontrivial p := Submodule.nontrivial_iff_ne_bot.mpr hp

Goal state after:
R : Type v
M : Type w
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R M
f : End R M
μ₁ μ₂ : R
hμ : μ₁ ≠ μ₂
k✝ l✝ : ℕ∞
k : ℕ
property✝¹ : ↑k ≤ k✝
l : ℕ
property✝ : ↑l ≤ l✝
a✝ : Nontrivial M
p : Submodule R M := (f.genEigenspace μ₁) ↑k ⊓ (f.genEigenspace μ₂) ↑l
hp : Nontrivial ↥p
⊢ False
Module: Mathlib.Algebra.Divisibility.Prod

Goal state before:
pp: ι : Type u_1
G : ι → Type u_4
inst✝ : (i : ι) → Semigroup (G i)
x y : (i : ι) → G i
⊢ x ∣ y ↔ ∀ (i : ι), x i ∣ y i

Tactic:
simp_rw [dvd_def, funext_iff, Classical.skolem]; rfl

Goal state after:
Module: Mathlib.LinearAlgebra.Trace

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Free R M
inst✝ : Module.Finite R M
⊢ (trace R M) id = ↑(finrank R M)

Tactic:
← Module.End.one_eq_id,

Goal state after:
R : Type u_1
inst✝⁴ : CommRing R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Free R M
inst✝ : Module.Finite R M
⊢ (trace R M) 1 = ↑(finrank R M)
Module: Mathlib.LinearAlgebra.Eigenspace.Basic

Goal state before:
pp: K : Type v
V : Type w
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : End K V
μ : K
n : ℕ
⊢ (f * (f - (algebraMap K (End K V)) μ) ^ n).range = ((f - (algebraMap K (End K V)) μ) ^ n * f).range

Tactic:
by
        rw [Algebra.mul_sub_algebraMap_pow_commutes]

Goal state after:
Module: Mathlib.LinearAlgebra.Eigenspace.Basic

Goal state before:
pp: case h.right.inl
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f₁ f₂ : End R M
μ₁ μ₂ : R
k₁ k₂ : ℕ∞
m : M
l₁ : ℕ
hlk₁ : ↑l₁ ≤ k₁
hl₁ : ((f₁ - μ₁ • 1) ^ l₁) m = 0
l₂ : ℕ
hlk₂ : ↑l₂ ≤ k₂
hl₂ : ((f₂ - μ₂ • 1) ^ l₂) m = 0
this : f₁ + f₂ - (μ₁ + μ₂) • 1 = f₁ - μ₁ • 1 + (f₂ - μ₂ • 1)
h : Commute (f₁ - μ₁ • 1) (f₂ - μ₂ • 1)
x✝ : ℕ × ℕ
i j : ℕ
hij : (i, j).1 + (i, j).2 = l₁ + l₂
hi : l₁ ≤ i
⊢ ((f₁ - μ₁ • 1) ^ i * (f₂ - μ₂ • 1) ^ j) m = 0

Tactic:
(h.pow_pow i j).eq,

Goal state after:
case h.right.inl
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f₁ f₂ : End R M
μ₁ μ₂ : R
k₁ k₂ : ℕ∞
m : M
l₁ : ℕ
hlk₁ : ↑l₁ ≤ k₁
hl₁ : ((f₁ - μ₁ • 1) ^ l₁) m = 0
l₂ : ℕ
hlk₂ : ↑l₂ ≤ k₂
hl₂ : ((f₂ - μ₂ • 1) ^ l₂) m = 0
this : f₁ + f₂ - (μ₁ + μ₂) • 1 = f₁ - μ₁ • 1 + (f₂ - μ₂ • 1)
h : Commute (f₁ - μ₁ • 1) (f₂ - μ₂ • 1)
x✝ : ℕ × ℕ
i j : ℕ
hij : (i, j).1 + (i, j).2 = l₁ + l₂
hi : l₁ ≤ i
⊢ ((f₂ - μ₂ • 1) ^ j * (f₁ - μ₁ • 1) ^ i) m = 0
Module: Mathlib.LinearAlgebra.Eigenspace.Basic

Goal state before:
pp: R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ ρ : R
⊢ (ρ • LinearMap.id + f).HasEigenvalue μ ↔ f.HasEigenvalue (μ - ρ)

Tactic:
by
  have aux : ρ • .id + f - μ • 1 = f - (μ - ρ) • 1 := by module
  simp only [hasEigenvalue_iff, eigenspace_def, aux]

Goal state after:
Module: Mathlib.GroupTheory.FreeGroup.Reduce

Goal state before:
pp: case succ
α : Type u_1
inst✝ : DecidableEq α
x : α × Bool
n : ℕ
ih : reduce (List.replicate n x) = List.replicate n x
⊢ (List.casesOn (List.replicate n x) [x] fun hd tl ↦ if x.1 = hd.1 ∧ x.2 = !hd.2 then tl else x :: hd :: tl) =
    x :: List.replicate n x

Tactic:
cases n with

Goal state after:
Module: Mathlib.Algebra.FiveLemma

Goal state before:
pp: M₁ : Type u_1
M₂ : Type u_2
M₃ : Type u_3
M₄ : Type u_4
N₁ : Type u_6
N₂ : Type u_7
N₃ : Type u_8
N₄ : Type u_9
inst✝⁷ : Group M₁
inst✝⁶ : Group M₂
inst✝⁵ : Group M₃
inst✝⁴ : Group M₄
inst✝³ : Group N₁
inst✝² : Group N₂
inst✝¹ : Group N₃
inst✝ : Group N₄
f₁ : M₁ →* M₂
f₂ : M₂ →* M₃
f₃ : M₃ →* M₄
g₁ : N₁ →* N₂
g₂ : N₂ →* N₃
g₃ : N₃ →* N₄
i₁ : M₁ →* N₁
i₂ : M₂ →* N₂
i₃ : M₃ →* N₃
i₄ : M₄ →* N₄
hc₁ : g₁.comp i₁ = i₂.comp f₁
hc₂ : g₂.comp i₂ = i₃.comp f₂
hc₃ : g₃.comp i₃ = i₄.comp f₃
hf₂ : Function.MulExact ⇑f₂ ⇑f₃
hg₁ : Function.MulExact ⇑g₁ ⇑g₂
hg₂ : Function.MulExact ⇑g₂ ⇑g₃
hi₁ : Function.Surjective ⇑i₁
hi₃ : Function.Surjective ⇑i₃
hi₄ : Function.Injective ⇑i₄
x : N₂
y : M₃
hy : i₃ y = g₂ x
⊢ ∃ a, i₂ a = x

Tactic:
obtain ⟨a, rfl⟩ : y ∈ Set.range f₂ := (hf₂ _).mp <| by
    simpa [hy, hg₂.apply_apply_eq_one, map_eq_one_iff _ hi₄] using (DFunLike.congr_fun hc₃ y).symm

Goal state after:
M₁ : Type u_1
M₂ : Type u_2
M₃ : Type u_3
M₄ : Type u_4
N₁ : Type u_6
N₂ : Type u_7
N₃ : Type u_8
N₄ : Type u_9
inst✝⁷ : Group M₁
inst✝⁶ : Group M₂
inst✝⁵ : Group M₃
inst✝⁴ : Group M₄
inst✝³ : Group N₁
inst✝² : Group N₂
inst✝¹ : Group N₃
inst✝ : Group N₄
f₁ : M₁ →* M₂
f₂ : M₂ →* M₃
f₃ : M₃ →* M₄
g₁ : N₁ →* N₂
g₂ : N₂ →* N₃
g₃ : N₃ →* N₄
i₁ : M₁ →* N₁
i₂ : M₂ →* N₂
i₃ : M₃ →* N₃
i₄ : M₄ →* N₄
hc₁ : g₁.comp i₁ = i₂.comp f₁
hc₂ : g₂.comp i₂ = i₃.comp f₂
hc₃ : g₃.comp i₃ = i₄.comp f₃
hf₂ : Function.MulExact ⇑f₂ ⇑f₃
hg₁ : Function.MulExact ⇑g₁ ⇑g₂
hg₂ : Function.MulExact ⇑g₂ ⇑g₃
hi₁ : Function.Surjective ⇑i₁
hi₃ : Function.Surjective ⇑i₃
hi₄ : Function.Injective ⇑i₄
x : N₂
a : M₂
hy : i₃ (f₂ a) = g₂ x
⊢ ∃ a, i₂ a = x
Module: Mathlib.Algebra.FreeMonoid.Count

Goal state before:
pp: α : Type u_1
p : α → Prop
inst✝ : DecidablePred p
l₁ l₂ : FreeMonoid α
⊢ List.countP (fun b ↦ decide (p b)) (toList l₁ ++ toList l₂) =
    List.countP (fun b ↦ decide (p b)) (toList l₁) + List.countP (fun b ↦ decide (p b)) (toList l₂)

Tactic:
simp only [List.countP_append]

Goal state after:
Module: Mathlib.Algebra.FreeMonoid.FreeSemigroup

Goal state before:
pp: case coe
α : Type u_1
a : FreeSemigroup α
⊢ (lift fun x ↦ ↑(FreeSemigroup.of x)) ((WithOne.lift toFreeMonoid) ↑a) = ↑a

Tactic:
| coe a =>

Goal state after:
Module: Mathlib.Algebra.Group.Action.Pointwise.Finset

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝⁵ : DecidableEq γ
inst✝⁴ : DecidableEq β
inst✝³ : SMul α β
inst✝² : SMul α γ
inst✝¹ : SMul β γ
inst✝ : IsScalarTower α β γ
a : α
s : Finset β
t : Finset γ
⊢ ↑((a • s) • t) = ↑(a • s • t)

Tactic:
simp only [coe_smul_finset, coe_smul, smul_assoc]

Goal state after:
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: R : Type u_1
inst✝² : Field R
a✝¹ b✝ : ℍ[R]
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
a✝ b a : ℍ[R]
ha : a ≠ 0
⊢ a * (normSq a)⁻¹ • star a = 1

Tactic:
Algebra.mul_smul_comm (normSq a)⁻¹ a (star a),

Goal state after:
R : Type u_1
inst✝² : Field R
a✝¹ b✝ : ℍ[R]
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
a✝ b a : ℍ[R]
ha : a ≠ 0
⊢ (normSq a)⁻¹ • (a * star a) = 1
Module: Mathlib.Algebra.Group.Action.Pointwise.Finset

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝² : DecidableEq β
inst✝¹ : Group α
inst✝ : MulAction α β
s t : Finset β
a : α
⊢ a • s ⊆ t ↔ s ⊆ a⁻¹ • t

Tactic:
simp_rw [← coe_subset]
  push_cast
  exact Set.smul_set_subset_iff_subset_inv_smul_set

Goal state after:
Module: Mathlib.Algebra.Group.Ideal

Goal state before:
pp: M : Type u_1
inst✝ : Monoid M
s : Set M
⊢ ↑(closure s) = univ * s

Tactic:
coe_closure,

Goal state after:
M : Type u_1
inst✝ : Monoid M
s : Set M
⊢ s ∪ univ * s = univ * s
Module: Mathlib.Algebra.Group.PNatPowAssoc

Goal state before:
pp: case one
M : Type u_1
inst✝² : Monoid M
inst✝¹ : Pow M ℕ+
inst✝ : PNatPowAssoc M
x : M
⊢ x ^ 1 = x ^ ↑1

Tactic:
rw [ppow_one, PNat.one_coe, pow_one]

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Range

Goal state before:
pp: case refine_1.mul
A : Type u_1
B : Type u_2
inst✝¹ : MonoidWithZero A
inst✝ : CommGroupWithZero B
f : A →*₀ B
y c d : Bˣ
hc : c ∈ Subgroup.closure ↑{ carrier := Units.val ⁻¹' range ⇑f, mul_mem' := ⋯, one_mem' := ⋯ }
hd : d ∈ Subgroup.closure ↑{ carrier := Units.val ⁻¹' range ⇑f, mul_mem' := ⋯, one_mem' := ⋯ }
u : A
hu : f u ≠ 0
a : A
ha : f u * ↑c = f a
v : A
hv : f v ≠ 0
b : A
hb : f v * ↑d = f b
⊢ ∃ a, f a ≠ 0 ∧ ∃ x, f a * ↑(c * d) = f x

Tactic:
refine ⟨u * v, by simp [hu, hv], a * b, ?_⟩

Goal state after:
case refine_1.mul
A : Type u_1
B : Type u_2
inst✝¹ : MonoidWithZero A
inst✝ : CommGroupWithZero B
f : A →*₀ B
y c d : Bˣ
hc : c ∈ Subgroup.closure ↑{ carrier := Units.val ⁻¹' range ⇑f, mul_mem' := ⋯, one_mem' := ⋯ }
hd : d ∈ Subgroup.closure ↑{ carrier := Units.val ⁻¹' range ⇑f, mul_mem' := ⋯, one_mem' := ⋯ }
u : A
hu : f u ≠ 0
a : A
ha : f u * ↑c = f a
v : A
hv : f v ≠ 0
b : A
hb : f v * ↑d = f b
⊢ f (u * v) * ↑(c * d) = f (a * b)
Module: Mathlib.AlgebraicTopology.MooreComplex

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Abelian C
X Y : SimplicialObject C
f✝ f : X ⟶ Y
n : ℕ
⊢ (objX Y n).Factors ((objX X n).arrow ≫ f.app (op ⦋n⦌))

Tactic:
cases n <;> dsimp
      · apply top_factors
      · refine (finset_inf_factors _).mpr fun i _ => kernelSubobject_factors _ _ ?_
        rw [Category.assoc, SimplicialObject.δ, ← f.naturality,
          ← factorThru_arrow _ _ (finset_inf_arrow_factors Finset.univ _ i (by simp)),
          Category.assoc]
        rw [← SimplicialObject.δ_def, kernelSubobject_arrow_comp_assoc, zero_comp, comp_zero]

Goal state after:
Module: Mathlib.CategoryTheory.Idempotents.FunctorCategories

Goal state before:
pp: J : Type u_1
C : Type u_2
inst✝¹ : Category.{v_1, u_1} J
inst✝ : Category.{v_2, u_2} C
P✝ Q : Karoubi (J ⥤ C)
f : P✝ ⟶ Q
X : J
P : Karoubi (J ⥤ C)
j j' : J
φ : j ⟶ j'
h : (P.p ≫ P.p).app j = P.p.app j
⊢ P.p.app j ≫ P.p.app j ≫ P.p.app j ≫ P.X.map φ = P.p.app j ≫ P.X.map φ

Tactic:
NatTrans.comp_app

Goal state after:
J : Type u_1
C : Type u_2
inst✝¹ : Category.{v_1, u_1} J
inst✝ : Category.{v_2, u_2} C
P✝ Q : Karoubi (J ⥤ C)
f : P✝ ⟶ Q
X : J
P : Karoubi (J ⥤ C)
j j' : J
φ : j ⟶ j'
h : P.p.app j ≫ P.p.app j = P.p.app j
⊢ P.p.app j ≫ P.p.app j ≫ P.p.app j ≫ P.X.map φ = P.p.app j ≫ P.X.map φ
Module: Mathlib.CategoryTheory.Idempotents.FunctorCategories

Goal state before:
pp: J : Type u_1
C : Type u_2
inst✝¹ : Category.{v_1, u_1} J
inst✝ : Category.{v_2, u_2} C
P Q : Karoubi (J ⥤ C)
f : P ⟶ Q
X : J
X✝ Y✝ : Karoubi (J ⥤ C)
a₁✝ a₂✝ : X✝ ⟶ Y✝
h : (karoubiFunctorCategoryEmbedding J C).map a₁✝ = (karoubiFunctorCategoryEmbedding J C).map a₂✝
⊢ a₁✝ = a₂✝

Tactic:
by
    ext j
    exact hom_ext_iff.mp (congr_app h j)

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: case «1»
n : ℕ
i : Fin n
j : Fin (n + 2)
h : i.succ.castSucc < j
⊢ ↑((Hom.toOrderHom (mkOfSucc i ≫ δ j)) ((fun i ↦ i) ⟨1, ⋯⟩)) =
    ↑((Hom.toOrderHom (mkOfSucc i.castSucc)) ((fun i ↦ i) ⟨1, ⋯⟩))

Tactic:
simp [δ, Fin.succAbove_of_castSucc_lt _ _ h]

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialObject.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X : CosimplicialObject C
n : ℕ
i j : Fin (n + 2)
H : i ≤ j
⊢ X.map (SimplexCategory.δ i) ≫ X.map (SimplexCategory.δ j.succ) =
    X.map (SimplexCategory.δ j) ≫ X.map (SimplexCategory.δ i.castSucc)

Tactic:
simp only [← X.map_comp, SimplexCategory.δ_comp_δ H]

Goal state after:
Module: Mathlib.AlgebraicTopology.AlternatingFaceMapComplex

Goal state before:
pp: C : Type u_1
inst✝³ : Category.{v_1, u_1} C
inst✝² : Preadditive C
A : Type u_2
inst✝¹ : Category.{v_2, u_2} A
inst✝ : Abelian A
X : SimplicialObject A
i : ℕ
⊢ (NormalizedMooreComplex.objX X (i + 1)).arrow ≫ ((alternatingFaceMapComplex A).obj X).d (i + 1) i =
    ((normalizedMooreComplex A).obj X).d (i + 1) i ≫ (NormalizedMooreComplex.objX X i).arrow

Tactic:
simp only [normalizedMooreComplex, NormalizedMooreComplex.obj, alternatingFaceMapComplex,
    AlternatingFaceMapComplex.obj, ChainComplex.of_d, AlternatingFaceMapComplex.objD, comp_sum]
  rw [Fin.sum_univ_succ, Fintype.sum_eq_zero]
  swap
  · intro j
    rw [NormalizedMooreComplex.objX_add_one, comp_zsmul,
      ← factorThru_arrow _ _ (finset_inf_arrow_factors Finset.univ _ _ (Finset.mem_univ j)),
      Category.assoc, kernelSubobject_arrow_comp, comp_zero, smul_zero]
  -- finally, we study the remaining term which is induced by X.δ 0
  rw [add_zero, Fin.val_zero, pow_zero, one_zsmul]
  dsimp [NormalizedMooreComplex.objD, NormalizedMooreComplex.objX]
  cases i <;> simp

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter

Goal state before:
pp: case inl
n m : ℕ
j : Fin (m + 1)
hi : n + ↑j = m
hj : ↑j ≤ ↑j
⊢ ↑j - ↑j = 0

Tactic:
tsub_self

Goal state after:
case inl
n m : ℕ
j : Fin (m + 1)
hi : n + ↑j = m
hj : ↑j ≤ ↑j
⊢ 0 = 0
Module: Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter

Goal state before:
pp: n : ℕ
⊢ σ₀Iter 0 ⋯ = 𝟙 ⦋n⦌

Tactic:
by
  ext
  simp [σ₀Iter]

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter

Goal state before:
pp: case neg
n : ℕ
i : Fin (n + 2)
m : ℕ
k : Fin (⦋n⦌.len + 1)
hk' : k.castSucc < i
h : m + (↑k + 1) = n + 1
hi' : ↑i ≤ ↑k + 1
hk : ↑k ≤ ↑k
⊢ 0 = ↑k - ↑k

Tactic:
tsub_self

Goal state after:
case neg
n : ℕ
i : Fin (n + 2)
m : ℕ
k : Fin (⦋n⦌.len + 1)
hk' : k.castSucc < i
h : m + (↑k + 1) = n + 1
hi' : ↑i ≤ ↑k + 1
hk : ↑k ≤ ↑k
⊢ 0 = 0
Module: Mathlib.AlgebraicTopology.SimplicialSet.Degenerate

Goal state before:
pp: case neg
X : SSet
n✝ n : ℕ
hn : ∀ (x : X _⦋n⦌), ∃ m f, ∃ (_ : Epi f), ∃ y, x = (ConcreteCategory.hom (X.map f.op)) ↑y
x : X _⦋n + 1⦌
hx : x ∉ X.nonDegenerate (n + 1)
⊢ ∃ m f, ∃ (_ : Epi f), ∃ y, x = (ConcreteCategory.hom (X.map f.op)) ↑y

Tactic:
· simp only [← mem_degenerate_iff_notMem_nonDegenerate,
          degenerate_eq_iUnion_range_σ, Set.mem_iUnion, Set.mem_range] at hx
        obtain ⟨i, y, rfl⟩ := hx
        obtain ⟨m, f, hf, z, rfl⟩ := hn y
        exact ⟨_, SimplexCategory.σ i ≫ f, inferInstance, z, by simp; rfl⟩

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.Finite

Goal state before:
pp: X Y : SSet
inst✝ : Y.Finite
f : X ⟶ Y
hf : Mono f
d : ℕ
h✝ : Y.HasDimensionLT d
⊢ X.Finite

Tactic:
have := hasDimensionLT_of_mono f d

Goal state after:
X Y : SSet
inst✝ : Y.Finite
f : X ⟶ Y
hf : Mono f
d : ℕ
h✝ : Y.HasDimensionLT d
this : X.HasDimensionLT d
⊢ X.Finite
Module: Mathlib.Algebra.Homology.AlternatingConst

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroMorphisms C
A : C
φ ψ : A ⟶ A
hOdd : φ ≫ ψ = 0
hEven : ψ ≫ φ = 0
c : ComplexShape ℕ
inst✝ : DecidableRel c.Rel
hc : ∀ (i j : ℕ), c.Rel i j → Odd (i + j)
i j k : ℕ
hij : c.Rel i j
hjk : c.Rel j k
h : Even j
⊢ (Iso.refl ((alternatingConst A hOdd hEven hc).sc' i j k).X₁).hom ≫
      { X₁ := A, X₂ := A, X₃ := A, f := ψ, g := φ, zero := hEven }.f =
    ((alternatingConst A hOdd hEven hc).sc' i j k).f ≫ (Iso.refl ((alternatingConst A hOdd hEven hc).sc' i j k).X₂).hom

Tactic:
simp_all only [alternatingConst, dite_eq_ite, Iso.refl_hom, Category.id_comp,
        shortComplexFunctor'_obj_f, ↓reduceIte, Category.comp_id, right_eq_ite_iff]
      intro hi
      have := hc i j hij
      exact False.elim <| Nat.not_odd_iff_even.2 hi <| by simp_all [Nat.odd_add]

Goal state after:
Module: Mathlib.AlgebraicTopology.ExtraDegeneracy

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : Augmented C
ed : X.ExtraDegeneracy
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
hij : j.castSucc < i
k : Fin (n + 1)
hk : j.rev = k
l : ℕ
hl : ↑i = ↑j + 1 + l
this :
  ed.s (↑k + 1) ≫ X.left.δ ⟨l + 1 + 1, ⋯⟩ =
    X.left.δ ⟨l + 1, CategoryTheory.SimplicialObject.Augmented.ExtraDegeneracy.homotopy._proof_24 n i j k hk l hl⟩ ≫
      ed.s ↑k
⊢ X.left.δ₀Iter ↑j.castSucc ⋯ ≫
      ed.s (↑k + 1) ≫
        X.left.δ ⟨l + 2, CategoryTheory.SimplicialObject.Augmented.ExtraDegeneracy.homotopy._proof_28 n i j k hk l hl⟩ ≫
          X.left.σ₀Iter ↑j.castSucc ⋯ =
    X.left.δ i ≫ X.left.δ₀Iter ↑j ⋯ ≫ ed.s ↑k ≫ X.left.σ₀Iter ↑j ⋯

Tactic:
reassoc_of% this,

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : Augmented C
ed : X.ExtraDegeneracy
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
hij : j.castSucc < i
k : Fin (n + 1)
hk : j.rev = k
l : ℕ
hl : ↑i = ↑j + 1 + l
this :
  ed.s (↑k + 1) ≫ X.left.δ ⟨l + 1 + 1, ⋯⟩ =
    X.left.δ ⟨l + 1, CategoryTheory.SimplicialObject.Augmented.ExtraDegeneracy.homotopy._proof_24 n i j k hk l hl⟩ ≫
      ed.s ↑k
⊢ X.left.δ₀Iter ↑j.castSucc ⋯ ≫
      X.left.δ ⟨l + 1, CategoryTheory.SimplicialObject.Augmented.ExtraDegeneracy.homotopy._proof_24 n i j k hk l hl⟩ ≫
        ed.s ↑k ≫ X.left.σ₀Iter ↑j.castSucc ⋯ =
    X.left.δ i ≫ X.left.δ₀Iter ↑j ⋯ ≫ ed.s ↑k ≫ X.left.σ₀Iter ↑j ⋯