mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: α : Type u
l : List α
s : Stream' α
⊢ corec
      (fun x ↦
        match x with
        | (a, snd) => a)
      (fun p ↦
        match p with
        | (l', s') => (l' ++ [s'.head], s'.tail))
      (l, s) =
    l ::
      corec
        (fun x ↦
          match x with
          | (a, snd) => a)
        (fun p ↦
          match p with
          | (l', s') => (l' ++ [s'.head], s'.tail))
        (l ++ [s.head], s.tail)

Tactic:
rw [corec_eq]

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

Goal state before:
pp: case succ.some
α : Type u
m : ℕ
ih : ∀ {s : Seq α}, (take m s).length ≤ m
s : Seq α
v : Seq1 α
⊢ (match some v with
      | none => []
      | some (x, r) => x :: take m r).length ≤
    m + 1

Tactic:
obtain ⟨x, r⟩ := v
      simpa using ih

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

Goal state before:
pp: α : Type u
s : Seq α
h : s.Terminates
⊢ (s.toList h).getLast? = s.get? (s.length h - 1)

Tactic:
List.getLast?_eq_getElem?,

Goal state after:
α : Type u
s : Seq α
h : s.Terminates
⊢ (s.toList h)[(s.toList h).length - 1]? = s.get? (s.length h - 1)
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: α : Type u
a : α
s t : Seq α
⊢ (corec
        (fun x ↦
          match x.1.destruct with
          | none =>
            match x.2.destruct with
            | none => none
            | some (a, b) => some (a, nil, b)
          | some (a, s₁') => some (a, s₁', x.2))
        (cons a s, t)).destruct =
    some
      (a,
        corec
          (fun x ↦
            match x.1.destruct with
            | none =>
              match x.2.destruct with
              | none => none
              | some (a, b) => some (a, nil, b)
            | some (a, s₁') => some (a, s₁', x.2))
          (s, t))

Tactic:
rw [corec_eq]

Goal state after:
α : Type u
a : α
s t : Seq α
⊢ omap
      (corec fun x ↦
        match x.1.destruct with
        | none =>
          match x.2.destruct with
          | none => none
          | some (a, b) => some (a, nil, b)
        | some (a, s₁') => some (a, s₁', x.2))
      (match (cons a s, t).1.destruct with
      | none =>
        match (cons a s, t).2.destruct with
        | none => none
        | some (a, b) => some (a, nil, b)
      | some (a_1, s₁') => some (a_1, s₁', (cons a s, t).2)) =
    some
      (a,
        corec
          (fun x ↦
            match x.1.destruct with
            | none =>
              match x.2.destruct with
              | none => none
              | some (a, b) => some (a, nil, b)
            | some (a, s₁') => some (a, s₁', x.2))
          (s, t))
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: α : Type u
s✝ s : Seq α
⊢ match
    (corec
        (fun x ↦
          match x.1.destruct with
          | none =>
            match x.2.destruct with
            | none => none
            | some (a, b) => some (a, nil, b)
          | some (a, s₁') => some (a, s₁', x.2))
        (nil, s)).destruct,
    s.destruct with
  | none, none => True
  | some (a, s), some (a', s') =>
    a = a' ∧
      ∃ s_1,
        s =
            corec
              (fun x ↦
                match x.1.destruct with
                | none =>
                  match x.2.destruct with
                  | none => none
                  | some (a, b) => some (a, nil, b)
                | some (a, s₁') => some (a, s₁', x.2))
              (nil, s_1) ∧
          s' = s_1
  | x, x_1 => False

Tactic:
rw [corec_eq]

Goal state after:
α : Type u
s✝ s : Seq α
⊢ match
    omap
      (corec fun x ↦
        match x.1.destruct with
        | none =>
          match x.2.destruct with
          | none => none
          | some (a, b) => some (a, nil, b)
        | some (a, s₁') => some (a, s₁', x.2))
      (match (nil, s).1.destruct with
      | none =>
        match (nil, s).2.destruct with
        | none => none
        | some (a, b) => some (a, nil, b)
      | some (a, s₁') => some (a, s₁', (nil, s).2)),
    s.destruct with
  | none, none => True
  | some (a, s), some (a', s') =>
    a = a' ∧
      ∃ s_1,
        s =
            corec
              (fun x ↦
                match x.1.destruct with
                | none =>
                  match x.2.destruct with
                  | none => none
                  | some (a, b) => some (a, nil, b)
                | some (a, s₁') => some (a, s₁', x.2))
              (nil, s_1) ∧
          s' = s_1
  | x, x_1 => False
Module: Mathlib.Algebra.ContinuedFractions.Determinant

Goal state before:
pp: K : Type u_1
inst✝ : Field K
g : GenContFract K
n✝ n : ℕ
hyp : n + 1 = 0 ∨ ¬g.TerminatedAt (n + 1 - 1)
conts : Pair K := g.contsAux (n + 2)
pred_conts : Pair K := g.contsAux (n + 1)
pred_conts_eq : pred_conts = g.contsAux (n + 1)
ppred_conts : Pair K := g.contsAux n
IH :
  n = 0 ∨ ¬g.TerminatedAt (n - 1) →
    ppred_conts.a * pred_conts.b - ppred_conts.b * pred_conts.a = ∏ i ∈ Finset.range n, -(g.partNums.get? i).getD 0
ppred_conts_eq : ppred_conts = g.contsAux n
pA : K := pred_conts.a
pB : K := pred_conts.b
ppA : K := ppred_conts.a
ppB : K := ppred_conts.b
not_terminated_at_n : ¬g.TerminatedAt n
gp : Pair K
s_nth_eq : g.s.get? n = some gp
this : ppA * pB - ppB * pA = ∏ i ∈ Finset.range n, -(g.partNums.get? i).getD 0
⊢ pA * conts.b - pB * conts.a = ∏ i ∈ Finset.range (n + 1), -(g.partNums.get? i).getD 0

Tactic:
rw [Finset.prod_range_succ, ← this, partNum_eq_s_a s_nth_eq, Option.getD_some]

Goal state after:
K : Type u_1
inst✝ : Field K
g : GenContFract K
n✝ n : ℕ
hyp : n + 1 = 0 ∨ ¬g.TerminatedAt (n + 1 - 1)
conts : Pair K := g.contsAux (n + 2)
pred_conts : Pair K := g.contsAux (n + 1)
pred_conts_eq : pred_conts = g.contsAux (n + 1)
ppred_conts : Pair K := g.contsAux n
IH :
  n = 0 ∨ ¬g.TerminatedAt (n - 1) →
    ppred_conts.a * pred_conts.b - ppred_conts.b * pred_conts.a = ∏ i ∈ Finset.range n, -(g.partNums.get? i).getD 0
ppred_conts_eq : ppred_conts = g.contsAux n
pA : K := pred_conts.a
pB : K := pred_conts.b
ppA : K := ppred_conts.a
ppB : K := ppred_conts.b
not_terminated_at_n : ¬g.TerminatedAt n
gp : Pair K
s_nth_eq : g.s.get? n = some gp
this : ppA * pB - ppB * pA = ∏ i ∈ Finset.range n, -(g.partNums.get? i).getD 0
⊢ pA * conts.b - pB * conts.a = (ppA * pB - ppB * pA) * -gp.a
Module: Mathlib.Algebra.ContinuedFractions.Computation.Basic

Goal state before:
pp: K : Type u_1
inst✝² : DivisionRing K
inst✝¹ : LinearOrder K
inst✝ : FloorRing K
v : K
n✝ : ℕ
⊢ IntFractPair.stream v n✝ = none → IntFractPair.stream v (n✝ + 1) = none

Tactic:
hyp

Goal state after:
K : Type u_1
inst✝² : DivisionRing K
inst✝¹ : LinearOrder K
inst✝ : FloorRing K
v : K
n✝ : ℕ
hyp : IntFractPair.stream v n✝ = none
⊢ IntFractPair.stream v (n✝ + 1) = none
Module: Mathlib.Algebra.ContinuedFractions.Computation.Translations

Goal state before:
pp: K : Type u_1
inst✝² : DivisionRing K
inst✝¹ : LinearOrder K
inst✝ : FloorRing K
v : K
n : ℕ
ifp_succ_n : IntFractPair K
stream_succ_nth_eq : IntFractPair.stream v (n + 1) = some ifp_succ_n
⊢ (match (IntFractPair.of v, Stream'.Seq.tail ⟨IntFractPair.stream v, ⋯⟩) with
          | (h, s) => { h := ↑h.b, s := Stream'.Seq.map (fun p ↦ { a := 1, b := ↑p.b }) s }).s.get?
      n =
    some { a := 1, b := ↑ifp_succ_n.b }

Tactic:
simp [stream_succ_nth_eq]

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

Goal state before:
pp: α : Type u
p : α → Prop
s : Seq α
h_all : ∀ x ∈ s, p x
n : ℕ
x : α
hx : p x
⊢ ∀ y ∈ s.set n x, p y

Tactic:
intro y hy

Goal state after:
α : Type u
p : α → Prop
s : Seq α
h_all : ∀ x ∈ s, p x
n : ℕ
x : α
hx : p x
y : α
hy : y ∈ s.set n x
⊢ p y
Module: Mathlib.Algebra.ContinuedFractions.Computation.CorrectnessTerminating

Goal state before:
pp: case h
K : Type u_1
inst✝² : Field K
inst✝¹ : LinearOrder K
v : K
inst✝ : FloorRing K
n : ℕ
terminatedAt_n : (of v).TerminatedAt n
m : ℕ
m_geq_n : n ≤ m
⊢ v = (of v).convs m

Tactic:
convs_stable_of_terminated m_geq_n terminatedAt_n

Goal state after:
case h
K : Type u_1
inst✝² : Field K
inst✝¹ : LinearOrder K
v : K
inst✝ : FloorRing K
n : ℕ
terminatedAt_n : (of v).TerminatedAt n
m : ℕ
m_geq_n : n ≤ m
⊢ v = (of v).convs n
Module: Mathlib.Algebra.CubicDiscriminant

Goal state before:
pp: S : Type u_2
inst✝ : CommRing S
w x y z : S
⊢ C w * (X - C x) * (X - C y) * (X - C z) =
    C w * X ^ 3 + C w * -(C x + C y + C z) * X ^ 2 + C w * (C x * C y + C x * C z + C y * C z) * X +
      C w * -(C x * C y * C z)

Tactic:
ring1

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 : ℕ
IH : ∀ 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:
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: F : Type u_3
K : Type u_4
P : Cubic F
inst✝¹ : Field F
inst✝ : Field K
φ : F →+* K
ha : P.a ≠ 0
⊢ (Polynomial.map φ P.toPoly).Splits ↔ (map φ P).roots.card = 3

Tactic:
replace ha : (map φ P).a ≠ 0 := (map_ne_zero φ).mpr ha
  rw [roots, ← map_toPoly, Polynomial.splits_iff_card_roots,
    ← ((degree_eq_iff_natDegree_eq <| ne_zero_of_a_ne_zero ha).1 <| degree_of_a_ne_zero ha : _ = 3)]

Goal state after:
Module: Mathlib.Algebra.CubicDiscriminant

Goal state before:
pp: F : Type u_3
K : Type u_4
P : Cubic F
inst✝¹ : Field F
inst✝ : Field K
φ : F →+* K
x y z : K
ha : P.a ≠ 0
h3 : (map φ P).roots = {x, y, z}
⊢ (φ P.a * -(x + y + z)) ^ 2 * (φ P.a * (x * y + x * z + y * z)) ^ 2 -
            4 * φ P.a * (φ P.a * (x * y + x * z + y * z)) ^ 3 -
          4 * (φ P.a * -(x + y + z)) ^ 3 * (φ P.a * -(x * y * z)) -
        27 * φ P.a ^ 2 * (φ P.a * -(x * y * z)) ^ 2 +
      18 * φ P.a * (φ P.a * -(x + y + z)) * (φ P.a * (x * y + x * z + y * z)) * (φ P.a * -(x * y * z)) =
    (φ P.a * φ P.a * (x - y) * (x - z) * (y - z)) ^ 2

Tactic:
ring1

Goal state after:
Module: Mathlib.RingTheory.Idempotents

Goal state before:
pp: R : Type u_1
inst✝² : Semiring R
I : Type u_3
e : I → R
inst✝¹ : Fintype I
inst✝ : Unique I
⊢ CompleteOrthogonalIdempotents e ↔ e default = 1

Tactic:
rw [completeOrthogonalIdempotents_iff, OrthogonalIdempotents.unique, Fintype.sum_unique,
    and_iff_right_iff_imp]

Goal state after:
R : Type u_1
inst✝² : Semiring R
I : Type u_3
e : I → R
inst✝¹ : Fintype I
inst✝ : Unique I
⊢ e default = 1 → IsIdempotentElem (e default)
Module: Mathlib.Algebra.ContinuedFractions.Computation.Approximations

Goal state before:
pp: case inr.ha
K : Type u_1
v : K
n : ℕ
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : FloorRing K
b : K
nth_partDen_eq : (of v).partDens.get? n = some b
not_terminatedAt_n : ¬(of v).TerminatedAt n
hB : 0 < (of v).dens n
⊢ 0 < b * (of v).dens n * (of v).dens n

Tactic:
have : 0 < b := zero_lt_one.trans_le (of_one_le_get?_partDen nth_partDen_eq)
      apply_rules [mul_pos]

Goal state after:
Module: Mathlib.RingTheory.Idempotents

Goal state before:
pp: case inr
R : Type u_1
S : Type u_2
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
h : ∀ x ∈ RingHom.ker f, IsNilpotent x
e₂ : R
he₂ : IsIdempotentElem e₂
e₁ : R
he₁ : IsIdempotentElem (f e₁)
he₁e₂ : f e₁ * f e₂ = 0
h✝ : Nontrivial R
a : R := e₁ - e₁ * e₂
ha : f a = f e₁
ha' : a * e₂ = 0
⊢ ∃ e', IsIdempotentElem e' ∧ f e' = f e₁ ∧ e' * e₂ = 0

Tactic:
have hx' : a - a ^ 2 ∈ RingHom.ker f := by
    simp [RingHom.mem_ker, pow_two, ha, he₁.eq]

Goal state after:
case inr
R : Type u_1
S : Type u_2
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
h : ∀ x ∈ RingHom.ker f, IsNilpotent x
e₂ : R
he₂ : IsIdempotentElem e₂
e₁ : R
he₁ : IsIdempotentElem (f e₁)
he₁e₂ : f e₁ * f e₂ = 0
h✝ : Nontrivial R
a : R := e₁ - e₁ * e₂
ha : f a = f e₁
ha' : a * e₂ = 0
hx' : a - a ^ 2 ∈ RingHom.ker f
⊢ ∃ e', IsIdempotentElem e' ∧ f e' = f e₁ ∧ e' * e₂ = 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
k : ℕ∞
x : M
⊢ x ∈ (f.genEigenspace μ) k ↔ ∃ l, ↑l ≤ k ∧ x ∈ ((f - μ • 1) ^ l).ker

Tactic:
have : Nonempty {l : ℕ // l ≤ k} := ⟨⟨0, zero_le⟩⟩
  have : Directed (ι := { i : ℕ // i ≤ k }) (· ≤ ·) fun i ↦ LinearMap.ker ((f - μ • 1) ^ (i : ℕ)) :=
    Monotone.directed_le fun m n h ↦ by simpa using (f - μ • 1).iterateKer.monotone h
  simp_rw [genEigenspace, OrderHom.coe_mk, LinearMap.mem_ker, iSup_subtype',
    Submodule.mem_iSup_of_directed _ this, LinearMap.mem_ker, Subtype.exists, exists_prop]

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
hfn : IsNilpotent f
μ : R
hf : f.HasUnifEigenvalue μ 1
⊢ IsNilpotent μ

Tactic:
obtain ⟨m : M, hm⟩ := hf.exists_hasUnifEigenvector
  obtain ⟨n : ℕ, hn : f ^ n = 0⟩ := hfn
  exact ⟨n, by simpa [hn, hm.2, eq_comm (a := (0 : M))] using hm.pow_apply n⟩

Goal state after:
Module: Mathlib.RingTheory.Idempotents

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
I : Type u_3
inst✝ : Fintype I
e : I → R
he : CompleteOrthogonalIdempotents e
⊢ Function.Bijective ⇑(RingHom.pi fun i ↦ Ideal.Quotient.mk (Ideal.span {1 - e i}))

Tactic:
refine ⟨?_, he.1.surjective_pi⟩
  rw [injective_iff_map_eq_zero]
  intro x hx
  simp only [funext_iff, RingHom.pi_apply, Pi.zero_apply, Ideal.Quotient.eq_zero_iff_mem,
    Ideal.mem_span_singleton] at hx
  suffices ∀ s : Finset I, (∏ i ∈ s, (1 - e i)) * x = x by
    rw [← this Finset.univ, he.prod_one_sub, zero_mul]
  refine fun s ↦ Finset.induction_on s (by simp) ?_
  intro a s has e'
  suffices (1 - e a) * x = x by simp [has, mul_assoc, e', this]
  obtain ⟨c, rfl⟩ := hx a
  rw [← mul_assoc, (he.idem a).one_sub.eq]

Goal state after:
Module: Mathlib.Algebra.DirectSum.LinearMap

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
N : ι → Submodule R M
inst✝³ : DecidableEq ι
inst✝² : ∀ (i : ι), Module.Finite R ↥(N i)
inst✝¹ : ∀ (i : ι), Free R ↥(N i)
h : IsInternal N
inst✝ : Fintype ι
f : M →ₗ[R] M
hf : ∀ (i : ι), MapsTo ⇑f ↑(N i) ↑(N i)
b : (i : ι) → Basis (Free.ChooseBasisIndex R ↥(N i)) R ↥(N i) := fun i ↦ Free.chooseBasis R ↥(N i)
⊢ (trace R M) f = ∑ i, (trace R ↥(N i)) (f.restrict ⋯)

Tactic:
trace_eq_matrix_trace R (h.collectedBasis b),

Goal state after:
ι : Type u_1
R : Type u_2
M : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
N : ι → Submodule R M
inst✝³ : DecidableEq ι
inst✝² : ∀ (i : ι), Module.Finite R ↥(N i)
inst✝¹ : ∀ (i : ι), Free R ↥(N i)
h : IsInternal N
inst✝ : Fintype ι
f : M →ₗ[R] M
hf : ∀ (i : ι), MapsTo ⇑f ↑(N i) ↑(N i)
b : (i : ι) → Basis (Free.ChooseBasisIndex R ↥(N i)) R ↥(N i) := fun i ↦ Free.chooseBasis R ↥(N i)
⊢ ((toMatrix (h.collectedBasis b) (h.collectedBasis b)) f).trace = ∑ i, (trace R ↥(N i)) (f.restrict ⋯)
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
k : ℕ
h : MapsTo ⇑(f - μ • 1) ↑((f.genEigenspace μ) ↑k) ↑((f.genEigenspace μ) ↑k)
⊢ IsNilpotent (LinearMap.restrict (f - μ • 1) h)

Tactic:
by
  use k
  ext ⟨x, hx⟩
  rw [mem_genEigenspace_nat] at hx
  rw [LinearMap.zero_apply, ZeroMemClass.coe_zero, ZeroMemClass.coe_eq_zero,
    Module.End.pow_restrict, LinearMap.restrict_apply]
  ext
  simpa

Goal state after:
Module: Mathlib.Algebra.DirectSum.LinearMap

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
N : ι → Submodule R M
inst✝³ : DecidableEq ι
inst✝² : ∀ (i : ι), Module.Finite R ↥(N i)
inst✝¹ : ∀ (i : ι), Free R ↥(N i)
inst✝ : IsNoetherian R M
σ : ι → ι
hσ : ∀ (i : ι), σ i ≠ i
f : End R M
hf : ∀ (i : ι), MapsTo ⇑f ↑(N i) ↑(N (σ i))
hN : {i | N i ≠ ⊥}.Finite
s : Finset ι := hN.toFinset
κ : ι → Type u_3 := fun i ↦ Free.ChooseBasisIndex R ↥(N i)
b : (i : ↥s) → Basis (κ ↑i) R ↥(N ↑i) := fun i ↦ Free.chooseBasis R ↥(N ↑i)
h : IsInternal fun i ↦ N ↑i
⊢ (trace R M) f = 0

Tactic:
trace_eq_matrix_trace R (h.collectedBasis b),

Goal state after:
ι : Type u_1
R : Type u_2
M : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
N : ι → Submodule R M
inst✝³ : DecidableEq ι
inst✝² : ∀ (i : ι), Module.Finite R ↥(N i)
inst✝¹ : ∀ (i : ι), Free R ↥(N i)
inst✝ : IsNoetherian R M
σ : ι → ι
hσ : ∀ (i : ι), σ i ≠ i
f : End R M
hf : ∀ (i : ι), MapsTo ⇑f ↑(N i) ↑(N (σ i))
hN : {i | N i ≠ ⊥}.Finite
s : Finset ι := hN.toFinset
κ : ι → Type u_3 := fun i ↦ Free.ChooseBasisIndex R ↥(N i)
b : (i : ↥s) → Basis (κ ↑i) R ↥(N ↑i) := fun i ↦ Free.chooseBasis R ↥(N ↑i)
h : IsInternal fun i ↦ N ↑i
⊢ ((toMatrix (h.collectedBasis b) (h.collectedBasis b)) f).trace = 0
Module: Mathlib.Algebra.DualNumber

Goal state before:
pp: R : Type u_1
inst✝¹ : CommSemiring R
R' : Type u_5
inst✝ : CommSemiring R'
f g : R[ε] →+* R'
h₀ : f.comp (algebraMap R R[ε]) = g.comp (algebraMap R R[ε])
hε : f ε = g ε
⊢ Algebra R R'

Tactic:
letI := f.toAlgebra

Goal state after:
R : Type u_1
inst✝¹ : CommSemiring R
R' : Type u_5
inst✝ : CommSemiring R'
f g : R[ε] →+* R'
h₀ : f.comp (algebraMap R R[ε]) = g.comp (algebraMap R R[ε])
hε : f ε = g ε
this : Algebra R[ε] R' := f.toAlgebra
⊢ Algebra R R'
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
k : ℕ∞
μ₁ μ₂ : R
s : Finset R
a✝ : μ₂ ∉ s
ih : Disjoint ((f.genEigenspace μ₁) k) (s.sup fun μ ↦ (f.genEigenspace μ) k)
hμ₁₂✝ : μ₁ ∉ insert μ₂ s
hμ₁₂ : μ₁ ≠ μ₂
hμ₁ : μ₁ ∉ s
x : M
hx : x ∈ (f.genEigenspace μ₁) k
hx' : x ∈ (f.genEigenspace μ₂) k ⊔ s.sup fun μ ↦ (f.genEigenspace μ) k
this : x ∈ (f.genEigenspace μ₂) k
⊢ x = 0

Tactic:
by
    rw [← Submodule.mem_bot (R := R), ← (f.disjoint_genEigenspace hμ₁₂ k k).eq_bot]
    exact ⟨hx, this⟩

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

Goal state before:
pp: α : Type u_1
L₁ L₂ : List (α × Bool)
inst✝ : DecidableEq α
⊢ reduce (reduce L₁ ++ reduce L₂) = (mk (L₁ ++ L₂)).toWord

Tactic:
← mul_mk,

Goal state after:
α : Type u_1
L₁ L₂ : List (α × Bool)
inst✝ : DecidableEq α
⊢ reduce (reduce L₁ ++ reduce L₂) = (mk L₁ * mk L₂).toWord
Module: Mathlib.GroupTheory.FreeGroup.Reduce

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
x y : FreeGroup α
⊢ (x * y).norm = (mk (x.toWord ++ y.toWord)).norm

Tactic:
← mul_mk,

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
x y : FreeGroup α
⊢ (x * y).norm = (mk x.toWord * mk y.toWord).norm
Module: Mathlib.Algebra.GCDMonoid.FinsetLemmas

Goal state before:
pp: case insert
ι : Type u_3
f : ι → ℚ
a✝ : ι
s✝ : Finset ι
has : a✝ ∉ s✝
ih : (∑ i ∈ s✝, f i).den ∣ s✝.lcm fun i ↦ (f i).den
⊢ (∑ i ∈ insert a✝ s✝, f i).den ∣ (insert a✝ s✝).lcm fun i ↦ (f i).den

Tactic:
| insert _ _ has ih =>

Goal state after:
Module: Mathlib.Algebra.GCDMonoid.FinsetLemmas

Goal state before:
pp: case insert
ι : Type u_3
f : ι → ℚ
a✝ : ι
s✝ : Finset ι
has : a✝ ∉ s✝
ih : (∏ i ∈ s✝, f i).den ∣ ∏ i ∈ s✝, (f i).den
⊢ (∏ i ∈ insert a✝ s✝, f i).den ∣ ∏ i ∈ insert a✝ s✝, (f i).den

Tactic:
| insert _ _ has ih =>

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

Goal state before:
pp: R : Type u
inst✝ : CommRing R
𝓟 : Ideal R
f : R[X]
hf : f.IsWeaklyEisensteinAt 𝓟
x : R
hroot : f.IsRoot x
hmo : f.Monic
i : ℕ
hi : f.natDegree ≤ i
k : ℕ
hk : i = f.natDegree + k
⊢ x ^ f.natDegree ∈ 𝓟

Tactic:
IsRoot.def,

Goal state after:
R : Type u
inst✝ : CommRing R
𝓟 : Ideal R
f : R[X]
hf : f.IsWeaklyEisensteinAt 𝓟
x : R
hroot : eval x f = 0
hmo : f.Monic
i : ℕ
hi : f.natDegree ≤ i
k : ℕ
hk : i = f.natDegree + k
⊢ x ^ f.natDegree ∈ 𝓟
Module: Mathlib.Algebra.Quaternion

Goal state before:
pp: R : Type u_3
c₁ c₂ c₃ : R
a : ℍ[R,c₁,c₂,c₃]
inst✝ : CommRing R
⊢ star a + a = 2 * ↑a.re + ↑c₂ * ↑a.imI

Tactic:
rw [add_comm, self_add_star]

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

Goal state before:
pp: case neg
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra R K
q f : R[X]
p : ℕ
hq_irr : Irreducible (map (algebraMap R K) q)
hq_monic : q.Monic
hf_prim : f.IsPrimitive
hfd0 : 0 < f.natDegree
hfP : (algebraMap R K) f.leadingCoeff ≠ 0
hfmodP : map (algebraMap R K) f = C ((algebraMap R K) f.leadingCoeff) * map (algebraMap R K) q ^ p
g h : R[X]
h_eq : f = g * h
P : Ideal R := ker (algebraMap R K)
hfmodP2 : map (Ideal.Quotient.mk (P ^ 2)) (f %ₘ q) ≠ 0
m : ℕ
r : R[X]
hg : g = C g.leadingCoeff * q ^ m + r
hr : map (algebraMap R K) r = 0
hm0 : m = 0 → IsUnit g
n : ℕ
s : R[X]
hh : h = C h.leadingCoeff * q ^ n + s
hs : map (algebraMap R K) s = 0
hn0 : n = 0 → IsUnit h
hm : ¬m = 0
hn : ¬n = 0
⊢ q ∣ r * (C h.leadingCoeff * q ^ n)

Tactic:
simp only [← mul_assoc]
      exact (dvd_pow_self q hn).mul_left _

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

Goal state before:
pp: case inr
M : Type u_1
inst✝ : Semigroup M
s : Set M
x y z : M
hz : z ∈ s
⊢ x • (fun x1 x2 ↦ x1 * x2) y z ∈ s ∪ univ * s

Tactic:
simpa [← mul_assoc] using .inr <| mul_mem_mul (mem_univ _) hz

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Pointwise.Finset

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
s : Finset α
⊢ s * 0 ⊆ 0

Tactic:
simp [subset_iff, mem_mul]

Goal state after:
Module: Mathlib.Algebra.GroupWithZero.Pointwise.Finset

Goal state before:
pp: α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : MulZeroClass α
s : Finset α
⊢ 0 * s ⊆ 0

Tactic:
simp [subset_iff, mem_mul]

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

Goal state before:
pp: ι : Type u_1
M : Type u_2
S : Type u_4
inst✝⁴ : Monoid M
inst✝³ : LinearOrder S
inst✝² : Finite ι
inst✝¹ : CommMonoid S
inst✝ : IsOrderedCancelMonoid S
v : ι → M
f : M →* S
t : Set ι := {i | IsMulIndecomposable v {j | 1 < f (v j)} i}
s : Set ι := {j | 1 < f (v j) ∧ v j ∉ closure (v '' t)}
hne : s.Nonempty
i : ι
hi : MinimalFor (fun x ↦ x ∈ s) (⇑f ∘ v) i
hi₀ : 1 < f (v i)
hi₁ : v i ∉ closure (v '' t)
k : ι
hk₀ : 1 < f (v k)
hk₁ : f (v k) < f (v i)
hk₂ : v k ∉ closure (v '' t)
⊢ False

Tactic:
exact not_le.mpr hk₁ <| hi.le_of_le ⟨hk₀, hk₂⟩ hk₁.le

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

Goal state before:
pp: case inr
α : Type u_1
inst✝¹ : GroupWithZero α
inst✝ : DecidableEq α
a : α
s : Finset α
ha : a ≠ 0
⊢ (a •> s)⁻¹ = s⁻¹ <• a⁻¹

Tactic:
ext; simp only [mem_inv', ne_eq, not_false_eq_true, ← inv_smul_mem_iff₀, smul_eq_mul,
      MulOpposite.op_inv, inv_eq_zero, MulOpposite.op_eq_zero_iff, inv_inv,
      MulOpposite.smul_eq_mul_unop, MulOpposite.unop_op, mul_inv_rev, ha]

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

Goal state before:
pp: M : Type u_1
inst✝³ : CommMonoidWithZero M
inst✝² : UniqueFactorizationMonoid M
inst✝¹ : NormalizationMonoid M
inst✝ : IsMulTorsionFree Mˣ
x : M
hx : x ≠ 0
y : M
hy : y ≠ 0
n : ℕ
hn : n ≠ 0
hxy : x ^ n = y ^ n
this : normalizedFactors x = normalizedFactors y
⊢ Associated x y

Tactic:
← associated_iff_normalizedFactors_eq_normalizedFactors hx hy

Goal state after:
M : Type u_1
inst✝³ : CommMonoidWithZero M
inst✝² : UniqueFactorizationMonoid M
inst✝¹ : NormalizationMonoid M
inst✝ : IsMulTorsionFree Mˣ
x : M
hx : x ≠ 0
y : M
hy : y ≠ 0
n : ℕ
hn : n ≠ 0
hxy : x ^ n = y ^ n
this : Associated x y
⊢ Associated x y