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

Goal state before:
pp: case mp
R : Type u_1
inst✝¹⁸ : CommRing R
M₁ : Type u_2
M₂ : Type u_3
M₃ : Type u_4
N₁ : Type u_5
N₂ : Type u_6
N₃ : Type u_7
inst✝¹⁷ : AddCommGroup M₁
inst✝¹⁶ : Module R M₁
inst✝¹⁵ : AddCommGroup M₂
inst✝¹⁴ : Module R M₂
inst✝¹³ : AddCommGroup M₃
inst✝¹² : Module R M₃
inst✝¹¹ : AddCommGroup N₁
inst✝¹⁰ : Module R N₁
inst✝⁹ : AddCommGroup N₂
inst✝⁸ : Module R N₂
inst✝⁷ : AddCommGroup N₃
inst✝⁶ : Module R N₃
i₁ : M₁ →ₗ[R] N₁
i₂ : M₂ →ₗ[R] N₂
i₃ : M₃ →ₗ[R] N₃
f₁ : M₁ →ₗ[R] M₂
f₂ : M₂ →ₗ[R] M₃
hf : Exact ⇑f₁ ⇑f₂
g₁ : N₁ →ₗ[R] N₂
g₂ : N₂ →ₗ[R] N₃
hg : Exact ⇑g₁ ⇑g₂
h₁ : g₁ ∘ₗ i₁ = i₂ ∘ₗ f₁
h₂ : g₂ ∘ₗ i₂ = i₃ ∘ₗ f₂
σ : M₃ → M₂
hσ : ⇑f₂ ∘ σ = id
ρ : N₂ → N₁
hρ : ρ ∘ ⇑g₁ = id
K₃ : Type u_9
C₁ : Type u_10
C₂ : Type u_11
inst✝⁵ : AddCommGroup K₃
inst✝⁴ : Module R K₃
inst✝³ : AddCommGroup C₁
inst✝² : Module R C₁
inst✝¹ : AddCommGroup C₂
inst✝ : Module R C₂
ι₃ : K₃ →ₗ[R] M₃
hι₃ : Exact ⇑ι₃ ⇑i₃
π₁ : N₁ →ₗ[R] C₁
hπ₁ : Exact ⇑i₁ ⇑π₁
π₂ : N₂ →ₗ[R] C₂
hπ₂ : Exact ⇑i₂ ⇑π₂
G : C₁ →ₗ[R] C₂
hF : G ∘ₗ π₁ = π₂ ∘ₗ g₁
h : Surjective ⇑π₁
H₂ : ∀ (x : K₃), g₁ (ρ (i₂ (σ (ι₃ x)))) = i₂ (σ (ι₃ x))
x : C₁
⊢ G x = 0 → x ∈ Set.range ⇑(δ i₁ i₂ i₃ f₁ f₂ hf g₁ g₂ hg h₁ h₂ σ hσ ρ hρ ι₃ hι₃ π₁ hπ₁)

Tactic:
intro H
    obtain ⟨x, rfl⟩ := h x
    obtain ⟨y, hy⟩ := (hπ₂ (g₁ x)).mp (by simpa only [← LinearMap.comp_apply, hF] using H)
    obtain ⟨z, hz⟩ : f₂ y ∈ range ι₃ := (hι₃ (f₂ y)).mp (by rw [← i₃.comp_apply, ← h₂,
      g₂.comp_apply, hy, hg.apply_apply_eq_zero])
    exact ⟨z, δ_eq i₁ i₂ i₃ f₁ f₂ hf g₁ g₂ hg h₁ h₂ σ hσ ρ hρ ι₃ hι₃ π₁ hπ₁ _ _ hz.symm _ hy.symm⟩

Goal state after:
Module: Mathlib.Algebra.CharP.Algebra

Goal state before:
pp: case zero
R : Type u_1
A : Type u_2
inst✝² : NonAssocSemiring R
inst✝¹ : NonAssocSemiring A
f : R →+* A
h : Function.Injective ⇑f
inst✝ : CharZero R
this : CharZero A
⊢ ExpChar A 1

Tactic:
exact .zero

Goal state after:
Module: Mathlib.Algebra.CharP.Algebra

Goal state before:
pp: case zero
R : Type u_1
A : Type u_2
inst✝² : NonAssocSemiring R
inst✝¹ : NonAssocSemiring A
f : R →+* A
H : Function.Injective ⇑f
inst✝ : CharZero A
this : CharZero R
⊢ ExpChar R 1

Tactic:
exact .zero

Goal state after:
Module: Mathlib.Algebra.CharP.MixedCharZero

Goal state before:
pp: case mpr
R : Type u_1
inst✝ : CommRing R
P : Prop
⊢ (∀ (p : ℕ), Nat.Prime p → MixedCharZero R p → P) → ∀ p > 0, MixedCharZero R p → P

Tactic:
intro h q q_pos q_mixedChar

Goal state after:
case mpr
R : Type u_1
inst✝ : CommRing R
P : Prop
h : ∀ (p : ℕ), Nat.Prime p → MixedCharZero R p → P
q : ℕ
q_pos : q > 0
q_mixedChar : MixedCharZero R q
⊢ P
Module: Mathlib.Data.Seq.Defs

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
s : Seq α
n : ℕ
f : α → α
⊢ IsSeq (Function.update (↑s) n (Option.map f (↑s n)))

Tactic:
have (i : ℕ) : Function.update s.val n ((s.get? n).map f) i = none ↔ s.get? i = none := by
      by_cases hi : i = n <;> simp [Function.update, hi]
    simp only [IsSeq, val_eq_get, this]
    exact @s.prop

Goal state after:
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: α : Type u
β : Type v
n : ℕ
a : Stream' α
f : α → β
⊢ List.map f (take n a) = take n (map f a)

Tactic:
apply List.ext_getElem

Goal state after:
case hl
α : Type u
β : Type v
n : ℕ
a : Stream' α
f : α → β
⊢ (List.map f (take n a)).length = (take n (map f a)).length

case h
α : Type u
β : Type v
n : ℕ
a : Stream' α
f : α → β
⊢ ∀ (i : ℕ) (h₁ : i < (List.map f (take n a)).length) (h₂ : i < (take n (map f a)).length),
    (List.map f (take n a))[i] = (take n (map f a))[i]
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: α : Type u
m n : ℕ
a : Stream' α
⊢ take n (drop m a) = List.drop m (take (m + n) a)

Tactic:
apply List.ext_getElem

Goal state after:
case hl
α : Type u
m n : ℕ
a : Stream' α
⊢ (take n (drop m a)).length = (List.drop m (take (m + n) a)).length

case h
α : Type u
m n : ℕ
a : Stream' α
⊢ ∀ (i : ℕ) (h₁ : i < (take n (drop m a)).length) (h₂ : i < (List.drop m (take (m + n) a)).length),
    (take n (drop m a))[i] = (List.drop m (take (m + n) a))[i]
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
C : Computation α → Sort v
a : α
s : Computation α
M : a ∈ s
h1 : C (pure a)
h2 : (s : Computation α) → C s → C s.think
T : s.Terminates
⊢ C s

Tactic:
rw [eq_thinkN' s, get_eq_of_mem s M]

Goal state after:
α : Type u
β : Type v
γ : Type w
C : Computation α → Sort v
a : α
s : Computation α
M : a ∈ s
h1 : C (pure a)
h2 : (s : Computation α) → C s → C s.think
T : s.Terminates
⊢ C ((pure a).thinkN s.length)
Module: Mathlib.Algebra.ContinuedFractions.TerminatedStable

Goal state before:
pp: K : Type u_1
n m : ℕ
inst✝ : DivisionRing K
s : Stream'.Seq (Pair K)
n_le_m : n ≤ m
terminatedAt_n : s.TerminatedAt n
⊢ convs'Aux s m = convs'Aux s n

Tactic:
by
  induction n_le_m with
  | refl => rfl
  | step n_le_m IH =>
    refine (convs'Aux_stable_step_of_terminated (?_)).trans IH
    exact s.terminated_stable n_le_m terminatedAt_n

Goal state after:
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: case zero
α : Type u
β : Type v
f : α → Computation β
b : β
s : Computation α
⊢ (s.bind f).Results b 0 → ∃ a m n, s.Results a m ∧ (f a).Results b n ∧ 0 = n + m

Tactic:
induction s using recOn with intro h | pure a  =>  _ | think s'
   =>  _ 

Goal state after:
case zero.pure
α : Type u
β : Type v
f : α → Computation β
b : β
a : α
h : ((pure a).bind f).Results b 0
⊢ ∃ a_1 m n, (pure a).Results a_1 m ∧ (f a_1).Results b n ∧ 0 = n + m

case zero.think
α : Type u
β : Type v
f : α → Computation β
b : β
s' : Computation α
h : (s'.think.bind f).Results b 0
⊢ ∃ a m n, s'.think.Results a m ∧ (f a).Results b n ∧ 0 = n + m
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: case succ
α : Type u
β : Type v
f : α → Computation β
b : β
n : ℕ
IH : ∀ {s : Computation α}, (s.bind f).Results b n → ∃ a m n_1, s.Results a m ∧ (f a).Results b n_1 ∧ n = n_1 + m
s : Computation α
⊢ (s.bind f).Results b (n + 1) → ∃ a m n_1, s.Results a m ∧ (f a).Results b n_1 ∧ n + 1 = n_1 + m

Tactic:
induction s using recOn with intro h | pure a  =>  _ | think s'
   =>  _ 

Goal state after:
case succ.pure
α : Type u
β : Type v
f : α → Computation β
b : β
n : ℕ
IH : ∀ {s : Computation α}, (s.bind f).Results b n → ∃ a m n_1, s.Results a m ∧ (f a).Results b n_1 ∧ n = n_1 + m
a : α
h : ((pure a).bind f).Results b (n + 1)
⊢ ∃ a_1 m n_1, (pure a).Results a_1 m ∧ (f a_1).Results b n_1 ∧ n + 1 = n_1 + m

case succ.think
α : Type u
β : Type v
f : α → Computation β
b : β
n : ℕ
IH : ∀ {s : Computation α}, (s.bind f).Results b n → ∃ a m n_1, s.Results a m ∧ (f a).Results b n_1 ∧ n = n_1 + m
s' : Computation α
h : (s'.think.bind f).Results b (n + 1)
⊢ ∃ a m n_1, s'.think.Results a m ∧ (f a).Results b n_1 ∧ n + 1 = n_1 + m
Module: Mathlib.Algebra.Colimit.Ring

Goal state before:
pp: ι : Type u_1
inst✝² : Preorder ι
G : ι → Type u_2
inst✝¹ : (i : ι) → CommRing (G i)
f : (i j : ι) → i ≤ j → G i → G j
P : Type u_3
inst✝ : CommRing P
g : (i : ι) → G i →+* P
Hg : ∀ (i j : ι) (hij : i ≤ j) (x : G i), (g j) (f i j hij x) = (g i) x
⊢ Ideal.span
      {a |
        (∃ i j, ∃ (H : i ≤ j), ∃ x, FreeCommRing.of ⟨j, f i j H x⟩ - FreeCommRing.of ⟨i, x⟩ = a) ∨
          (∃ i, FreeCommRing.of ⟨i, 1⟩ - 1 = a) ∨
            (∃ i x y, FreeCommRing.of ⟨i, x + y⟩ - (FreeCommRing.of ⟨i, x⟩ + FreeCommRing.of ⟨i, y⟩) = a) ∨
              ∃ i x y, FreeCommRing.of ⟨i, x * y⟩ - FreeCommRing.of ⟨i, x⟩ * FreeCommRing.of ⟨i, y⟩ = a} ≤
    Ideal.comap (FreeCommRing.lift fun x ↦ (g x.fst) x.snd) ⊥

Tactic:
rw [Ideal.span_le]

Goal state after:
ι : Type u_1
inst✝² : Preorder ι
G : ι → Type u_2
inst✝¹ : (i : ι) → CommRing (G i)
f : (i j : ι) → i ≤ j → G i → G j
P : Type u_3
inst✝ : CommRing P
g : (i : ι) → G i →+* P
Hg : ∀ (i j : ι) (hij : i ≤ j) (x : G i), (g j) (f i j hij x) = (g i) x
⊢ {a |
      (∃ i j, ∃ (H : i ≤ j), ∃ x, FreeCommRing.of ⟨j, f i j H x⟩ - FreeCommRing.of ⟨i, x⟩ = a) ∨
        (∃ i, FreeCommRing.of ⟨i, 1⟩ - 1 = a) ∨
          (∃ i x y, FreeCommRing.of ⟨i, x + y⟩ - (FreeCommRing.of ⟨i, x⟩ + FreeCommRing.of ⟨i, y⟩) = a) ∨
            ∃ i x y, FreeCommRing.of ⟨i, x * y⟩ - FreeCommRing.of ⟨i, x⟩ * FreeCommRing.of ⟨i, y⟩ = a} ⊆
    ↑(Ideal.comap (FreeCommRing.lift fun x ↦ (g x.fst) x.snd) ⊥)
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: α : Type u
hd : α
tl : Seq α
f : α → α
n : ℕ
⊢ ((cons hd tl).update 0 f).get? n = (cons (f hd) tl).get? n

Tactic:
cases n <;> simp [get?_update]

Goal state after:
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: α : Type u
hd : α
tl : Seq α
f : α → α
n✝ n : ℕ
⊢ ((cons hd tl).update (n✝ + 1) f).get? n = (cons hd (tl.update n✝ f)).get? n

Tactic:
cases n <;> simp [get?_update]

Goal state after:
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: α : Type u
R : α → α → Prop
hd : α
tl : Seq α
h : Pairwise R (Seq.cons hd tl)
⊢ (∀ x ∈ tl, R hd x) ∧ Pairwise R tl

Tactic:
simp only [Pairwise] at *
  refine ⟨?_, fun i j h_ij ↦ h (i + 1) (j + 1) (by lia)⟩
  intro x hx
  rw [mem_iff_exists_get?] at hx
  obtain ⟨n, hx⟩ := hx
  simpa [← hx] using h 0 (n + 1) (by lia)

Goal state after:
Module: Mathlib.Algebra.Colimit.Ring

Goal state before:
pp: ι : Type u_1
inst✝³ : Preorder ι
G : ι → Type u_2
inst✝² : Nonempty ι
inst✝¹ : IsDirectedOrder ι
inst✝ : (i : ι) → Field (G i)
f : (i j : ι) → i ≤ j → G i → G j
p : Ring.DirectLimit G f
hp : p ≠ 0
⊢ inv G f p * p = 1

Tactic:
_root_.mul_comm,

Goal state after:
ι : Type u_1
inst✝³ : Preorder ι
G : ι → Type u_2
inst✝² : Nonempty ι
inst✝¹ : IsDirectedOrder ι
inst✝ : (i : ι) → Field (G i)
f : (i j : ι) → i ≤ j → G i → G j
p : Ring.DirectLimit G f
hp : p ≠ 0
⊢ p * inv G f p = 1
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: α : Type u
β : Type v
a : α
f : α → Seq1 β
⊢ (ret a).bind f = f a

Tactic:
simp only [bind, map, ret.eq_1, map_nil]
  obtain ⟨a, s⟩ := f a
  cases s <;> simp

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

Goal state before:
pp: case none
K : Type u_1
n : ℕ
s : Stream'.Seq (Pair K)
inst✝ : DivisionRing K
s_succ_nth_eq : s.get? (n + 1) = none
⊢ convs'Aux s (n + 2) = convs'Aux s (n + 1)

Tactic:
convs'Aux_stable_step_of_terminated s_succ_nth_eq

Goal state after:
case none
K : Type u_1
n : ℕ
s : Stream'.Seq (Pair K)
inst✝ : DivisionRing K
s_succ_nth_eq : s.get? (n + 1) = none
⊢ convs'Aux s (n + 1) = convs'Aux s (n + 1)
Module: Mathlib.Algebra.ContinuedFractions.ConvergentsEquiv

Goal state before:
pp: K : Type u_1
inst✝ : DivisionRing K
m : ℕ
IH :
  ∀ {s : Stream'.Seq (Pair K)} (gp_succ_n : Pair K),
    s.get? (m + 1) = some gp_succ_n → convs'Aux s (m + 2) = convs'Aux (squashSeq s m) (m + 1)
s : Stream'.Seq (Pair K)
gp_succ_n : Pair K
s_succ_nth_eq : s.get? (m + 1 + 1) = some gp_succ_n
gp_head : Pair K
s_head_eq : s.head = some gp_head
this : gp_head.a / (gp_head.b + convs'Aux s.tail (m + 2)) = convs'Aux (squashSeq s (m + 1)) (m + 2)
⊢ convs'Aux s (m + 1 + 2) = convs'Aux (squashSeq s (m + 1)) (m + 1 + 1)

Tactic:
by simpa only [convs'Aux, s_head_eq]

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
⊢ ∀ (n : ℕ),
    (∀ m < n, m ≤ 1 ∨ ¬(of v).TerminatedAt (m - 2) → ↑(fib m) ≤ ((of v).contsAux m).b) →
      n ≤ 1 ∨ ¬(of v).TerminatedAt (n - 2) → ↑(fib n) ≤ ((of v).contsAux n).b

Tactic:
intro n IH hyp

Goal state after:
K : Type u_1
v : K
n✝ : ℕ
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : FloorRing K
n : ℕ
IH : ∀ m < n, m ≤ 1 ∨ ¬(of v).TerminatedAt (m - 2) → ↑(fib m) ≤ ((of v).contsAux m).b
hyp : n ≤ 1 ∨ ¬(of v).TerminatedAt (n - 2)
⊢ ↑(fib n) ≤ ((of v).contsAux n).b
Module: Mathlib.Algebra.CubicDiscriminant

Goal state before:
pp: R : Type u_1
P : Cubic R
inst✝ : Semiring R
ha : P.a = 0
⊢ P.toPoly = C P.b * X ^ 2 + C P.c * X + C P.d

Tactic:
rw [toPoly, ha, C_0, zero_mul, zero_add]

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

Goal state before:
pp: case succ
K : Type u_1
v : K
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : FloorRing K
ifp : IntFractPair K
g : GenContFract K := of v
ifp_fr_ne_zero : ifp.fr ≠ 0
n' : ℕ
stream_nth_eq : IntFractPair.stream v (n' + 1) = some ifp
conts : Pair K := g.contsAux (n' + 1 + 1)
pred_conts : Pair K := g.contsAux (n' + 1)
A : K := conts.a
B : K := conts.b
pA : K := pred_conts.a
pB : K := pred_conts.b
g_finite_correctness : v = (pA + ifp.fr⁻¹ * A) / (pB + ifp.fr⁻¹ * B)
⊢ n' + 1 = 0 ∨ ¬g.TerminatedAt (n' + 1 - 1)

Tactic:
have : IntFractPair.stream v (n' + 1) ≠ none := by simp [stream_nth_eq]
        have : ¬g.TerminatedAt n' :=
          (not_congr of_terminatedAt_n_iff_succ_nth_intFractPair_stream_eq_none).2 this
        exact Or.inr this

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

Goal state before:
pp: case mp
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
k : ℕ
x : M
⊢ (∀ i ≤ k, ∃ y, ((f - μ • 1) ^ i) y = x) → ∃ y, ((f - μ • 1) ^ k) y = x

pp: case mpr
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
k : ℕ
x : M
⊢ (∃ y, ((f - μ • 1) ^ k) y = x) → ∀ i ≤ k, ∃ y, ((f - μ • 1) ^ i) y = x

Tactic:
· intro h
    exact h _ le_rfl

Goal state after:
case mpr
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
k : ℕ
x : M
⊢ (∃ y, ((f - μ • 1) ^ k) y = x) → ∀ i ≤ k, ∃ y, ((f - μ • 1) ^ i) y = x
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✝ : IsNoetherian R M
f : End R M
μ : R
⊢ (f.genEigenspace μ) ⊤ = (f.genEigenspace μ) ↑(f.maxUnifEigenspaceIndex μ)

Tactic:
have := WellFoundedGT.iSup_eq_monotonicSequenceLimit <|
    (f.genEigenspace μ).comp <| WithTop.coeOrderHom.toOrderHom

Goal state after:
R : Type v
M : Type w
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsNoetherian R M
f : End R M
μ : R
this :
  iSup ⇑((f.genEigenspace μ).comp WithTop.coeOrderHom.toOrderHom) =
    monotonicSequenceLimit ((f.genEigenspace μ).comp WithTop.coeOrderHom.toOrderHom)
⊢ (f.genEigenspace μ) ⊤ = (f.genEigenspace μ) ↑(f.maxUnifEigenspaceIndex μ)
Module: Mathlib.Algebra.GroupWithZero.Action.ConjAct

Goal state before:
pp: α : Type u_1
G₀ : Type u_2
inst✝ : GroupWithZero G₀
⊢ ∀ (b : G₀), 1 • b = b

Tactic:
by simp [smul_def]

Goal state after:
Module: Mathlib.Algebra.Field.Action.ConjAct

Goal state before:
pp: K : Type u_1
inst✝ : DivisionRing K
⊢ ∀ (a : ConjAct K), a • 0 = 0

Tactic:
by simp [smul_def]

Goal state after:
Module: Mathlib.Algebra.Field.ZMod

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
⊢ IsDomain (ZMod p)

Tactic:
by constructor

Goal state after:
Module: Mathlib.Algebra.FreeAlgebra.Cardinality

Goal state before:
pp: R : Type u
inst✝² : CommSemiring R
X : Type v
inst✝¹ : Nonempty X
inst✝ : Nontrivial R
hX : #(FreeMonoid X) = max #X ℵ₀
⊢ #(FreeAlgebra R X) = max (max (Cardinal.lift.{v, u} #R) (Cardinal.lift.{u, v} #X)) ℵ₀

Tactic:
equivMonoidAlgebraFreeMonoid.toEquiv.cardinal_eq,

Goal state after:
R : Type u
inst✝² : CommSemiring R
X : Type v
inst✝¹ : Nonempty X
inst✝ : Nontrivial R
hX : #(FreeMonoid X) = max #X ℵ₀
⊢ #(MonoidAlgebra R (FreeMonoid X)) = max (max (Cardinal.lift.{v, u} #R) (Cardinal.lift.{u, v} #X)) ℵ₀
Module: Mathlib.Algebra.FreeAlgebra.Cardinality

Goal state before:
pp: R : Type u
inst✝¹ : CommSemiring R
X : Type v
inst✝ : Subsingleton R
⊢ #(FreeAlgebra R X) = 1

Tactic:
equivMonoidAlgebraFreeMonoid.toEquiv.cardinal_eq,

Goal state after:
R : Type u
inst✝¹ : CommSemiring R
X : Type v
inst✝ : Subsingleton R
⊢ #(MonoidAlgebra R (FreeMonoid X)) = 1
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: S : Type u_1
T : Type u_2
R : Type u_3
c₁ c₂ c₃ r x y : R
a b : ℍ[R,c₁,c₂,c₃]
inst✝ : AddCommGroupWithOne R
n : ℕ
⊢ ↑↑(Int.negSucc n) = -↑↑(n + 1)

Tactic:
rw [Int.cast_negSucc, coe_neg]

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Eisenstein.Basic

Goal state before:
pp: R : Type u
inst✝² : CommRing R
𝓟 : Ideal R
f : R[X]
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
hf : f.IsWeaklyEisensteinAt 𝓟
x : S
hx : (aeval x) f = 0
hmo : f.Monic
⊢ x ^ (Polynomial.map (algebraMap R S) f).natDegree ∈ Ideal.map (algebraMap R S) 𝓟

Tactic:
rw [aeval_def, eval₂_eq_eval_map, ← IsRoot.def] at hx

Goal state after:
R : Type u
inst✝² : CommRing R
𝓟 : Ideal R
f : R[X]
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
hf : f.IsWeaklyEisensteinAt 𝓟
x : S
hx : (Polynomial.map (algebraMap R S) f).IsRoot x
hmo : f.Monic
⊢ x ^ (Polynomial.map (algebraMap R S) f).natDegree ∈ Ideal.map (algebraMap R S) 𝓟
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: R : Type u_3
inst✝ : CommRing R
a : ℍ[R]
⊢ normSq (star a) = normSq a

Tactic:
by simp [normSq_def']

Goal state after:
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : LinearOrder R
inst✝ : IsStrictOrderedRing R
a : ℍ[R]
⊢ a ^ 2 = -↑(normSq a) ↔ a.re = 0

Tactic:
simp_rw [← star_eq_neg]
  obtain rfl | hq0 := eq_or_ne a 0
  · simp
  · rw [← star_mul_self, ← mul_neg, ← neg_sq, sq, mul_left_inj' (neg_ne_zero.mpr hq0), eq_comm]

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

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝⁵ : MulOneClass M
inst✝⁴ : Pow M ℕ
inst✝³ : NatPowAssoc M
inst✝² : MulOneClass N
inst✝¹ : Pow N ℕ
inst✝ : NatPowAssoc N
x✝² x✝¹ : ℕ
x✝ : M × N
⊢ x✝ ^ (x✝² + x✝¹) = x✝ ^ x✝² * x✝ ^ x✝¹

Tactic:
by ext <;> simp [npow_add]

Goal state after:
Module: Mathlib.Algebra.Group.Irreducible.Indecomposable

Goal state before:
pp: ι : Type u_1
G : Type u_3
S : Type u_4
inst✝⁴ : CommGroup G
inst✝³ : LinearOrder S
inst✝² : InvolutiveInv ι
inst✝¹ : CommGroup S
inst✝ : IsOrderedMonoid S
v : ι → G
f : G →* S
s : Set ι
hf : ∀ i ∈ s, 1 < f (v i)
i : ι
hv_one : v i ≠ 1
hv_inv : v i⁻¹ = (v i)⁻¹
hsp : v i ∈ closure (v '' s) ∨ (v i)⁻¹ ∈ closure (v '' s)
⊢ f (v i) ≠ 1

Tactic:
wlog hi : v i ∈ closure (v '' s)
  · rcases hsp with hi' | hi'; · contradiction
    simpa [hv_inv] using this v f s hf i⁻¹ (by simpa [hv_inv]) (by simp [hv_inv])
      (by left; simpa [hv_inv]) (by simpa [hv_inv])
  suffices v i ≠ 1 → 1 < f (v i) from (this hv_one).ne'
  refine closure_induction (by simp_all) (by simp) (fun x y _ _ hx hy _ ↦ ?_) hi
  rcases eq_or_ne x 1 with rfl | hx'; · grind
  rcases eq_or_ne y 1 with rfl | hy'; · grind
  simpa using lt_mul_of_lt_of_one_lt (hx hx') (hy hy')

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X : SimplicialObject C
n : ℕ
i : Fin (n + 2)
j : Fin (n + 3)
H : i.castSucc < j
⊢ X.δ j ≫ X.δ i = X.δ i.castSucc ≫ X.δ (j.pred ⋯)

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

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

Goal state before:
pp: case succ
j : ℕ
hj :
  ∀ {n : ℕ} (i : Fin (n + 2)) {m : ℕ} (i' : Fin (m + 2)) (h : n + j = m),
    ↑i' = ↑i + j → δ₀Iter j h ≫ δ i' = δ i ≫ δ₀Iter j ⋯
n : ℕ
i : Fin (n + 2)
m : ℕ
i' : Fin (m + 2)
h : n + (j + 1) = m
hi'' : ↑i' = ↑i + (j + 1)
⊢ δ 0 ≫ δ₀Iter j ⋯ ≫ δ i' = δ i ≫ δ 0 ≫ δ₀Iter j ⋯

Tactic:
← reassoc_of% dsimp% δ_comp_δ (i := 0) (j := i) (by simp),

Goal state after:
case succ
j : ℕ
hj :
  ∀ {n : ℕ} (i : Fin (n + 2)) {m : ℕ} (i' : Fin (m + 2)) (h : n + j = m),
    ↑i' = ↑i + j → δ₀Iter j h ≫ δ i' = δ i ≫ δ₀Iter j ⋯
n : ℕ
i : Fin (n + 2)
m : ℕ
i' : Fin (m + 2)
h : n + (j + 1) = m
hi'' : ↑i' = ↑i + (j + 1)
⊢ δ 0 ≫ δ₀Iter j ⋯ ≫ δ i' = δ 0 ≫ δ i.succ ≫ δ₀Iter j ⋯
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: x : SimplexCategory
e : x ≅ x
h : Finset.univ.card = x.len + 1
eq₁ : RelIso.toRelEmbedding (orderIsoOfIso e) = Finset.univ.orderEmbOfFin h
eq₂ : RelIso.toRelEmbedding (orderIsoOfIso (Iso.refl x)) = Finset.univ.orderEmbOfFin h
x✝ : Fin (x.len + 1)
⊢ (Hom.toOrderHom e.hom) x✝ = (Hom.toOrderHom (Iso.refl x).hom) x✝

Tactic:
exact DFunLike.congr_fun (eq₁.trans eq₂.symm) _

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

Goal state before:
pp: case neg
n : ℕ
Δ' : SimplexCategory
θ : ⦋n + 1⦌ ⟶ Δ'
i : Fin (n + 1)
hi : (Hom.toOrderHom θ) i.castSucc = (Hom.toOrderHom θ) i.succ
x : Fin (⦋n + 1⦌.len + 1)
h' : i.castSucc < x
y : Fin ⦋n + 1⦌.len := x.pred ⋯
hy : x = y.succ
⊢ (Hom.toOrderHom θ) x = (Hom.toOrderHom θ) ((Hom.toOrderHom (δ i.succ)) (i.predAbove x))

Tactic:
rw [hy] at h' ⊢

Goal state after:
case neg
n : ℕ
Δ' : SimplexCategory
θ : ⦋n + 1⦌ ⟶ Δ'
i : Fin (n + 1)
hi : (Hom.toOrderHom θ) i.castSucc = (Hom.toOrderHom θ) i.succ
x : Fin (⦋n + 1⦌.len + 1)
h'✝ : i.castSucc < x
y : Fin ⦋n + 1⦌.len := x.pred ⋯
h' : i.castSucc < y.succ
hy : x = y.succ
⊢ (Hom.toOrderHom θ) y.succ = (Hom.toOrderHom θ) ((Hom.toOrderHom (δ i.succ)) (i.predAbove y.succ))
Module: Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter

Goal state before:
pp: case neg
n : ℕ
i : Fin (n + 2)
j m : ℕ
h : m + (j + 1) = n + 1
hi' : ↑i ≤ j + 1
k : Fin (⦋n⦌.len + 1)
hk : ↑k < j
hk' : k.castSucc < i
⊢ ↑((ConcreteCategory.hom (σ₀Iter (j + 1) ⋯)) (i.succAbove k)) = 0

Tactic:
rw [Fin.succAbove_of_castSucc_lt _ _ (by lia), σ₀Iter_coe_eq_of_lt ..]

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

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
this✝ : 0 < n
Δ : SimplexCategory
this : Nonempty (CostructuredArrow (inclusion n) Δ)
Δ₁ : SimplexCategory
hΔ₁ : Δ₁.len ≤ n
f : (inclusion n).obj { obj := Δ₁, property := hΔ₁ } ⟶ (Functor.fromPUnit Δ).obj { as := PUnit.unit }
Δ₂ : SimplexCategory
hΔ₂ : Δ₂.len ≤ n
f' : (inclusion n).obj { obj := Δ₂, property := hΔ₂ } ⟶ (Functor.fromPUnit Δ).obj { as := PUnit.unit }
hff' : ¬(ConcreteCategory.hom f) 0 ≤ (ConcreteCategory.hom f') 0
⊢ Zigzag
    { left := { obj := ⦋1⦌, property := this✝ }, right := { as := PUnit.unit },
      hom := mkOfLe ((ConcreteCategory.hom f') 0) ((ConcreteCategory.hom f) 0) ⋯ }
    { left := { obj := Δ₂, property := hΔ₂ }, right := { as := PUnit.unit }, hom := f' }

Tactic:
trans ⟨⦋0⦌ₙ, ⟨⟨⟩⟩, ⦋0⦌.const _ (f' 0)⟩
      · apply Zigzag.of_inv <| CostructuredArrow.homMk <| Hom.tr <| ⦋0⦌.const _ 0
      · apply Zigzag.of_hom <| CostructuredArrow.homMk <| Hom.tr <| ⦋0⦌.const _ 0

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

Goal state before:
pp: X : SSet
n : ℕ
Y : SSet
f : X ⟶ Y
inst✝ : Mono f
x : X _⦋n⦌
⊢ (ConcreteCategory.hom (f.app (op ⦋n⦌))) x ∈ Y.degenerate n ↔
    (ConcreteCategory.hom ((Subcomplex.toRange f).app (op ⦋n⦌))) x ∈ (Subcomplex.range f).toSSet.degenerate n

Tactic:
Subcomplex.mem_degenerate_iff

Goal state after:
X : SSet
n : ℕ
Y : SSet
f : X ⟶ Y
inst✝ : Mono f
x : X _⦋n⦌
⊢ (ConcreteCategory.hom (f.app (op ⦋n⦌))) x ∈ Y.degenerate n ↔
    ↑((ConcreteCategory.hom ((Subcomplex.toRange f).app (op ⦋n⦌))) x) ∈ Y.degenerate n
Module: Mathlib.AlgebraicTopology.SimplicialSet.NerveNondegenerate

Goal state before:
pp: X : Type u_1
inst✝ : PartialOrder X
n : ℕ
s : nerve X _⦋n + 1⦌
i : Fin (n + 1)
hi : s.obj i.castSucc = s.obj i.succ
⊢ s ∈ (nerve X).degenerate (n + 1)

Tactic:
by
  simp only [SSet.degenerate_eq_iUnion_range_σ, Set.mem_iUnion]
  exact ⟨i, by rwa [← mem_range_nerve_σ_iff] at hi⟩

Goal state after: