mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: case refine_1.refine_1
α : Type u
R : Computation α → Computation α → Prop
bisim : IsBisimulation R
s₁ s₂ : Computation α
r : R s₁ s₂
t₁ t₂ : Stream' (Option α)
e : ∃ s s', s.val = t₁ ∧ s'.val = t₂ ∧ R s s'
s s' : Computation α
r' a' : α
⊢ R (pure r') (pure a') →
    BisimO R (pure r').destruct (pure a').destruct → (pure r').head = (pure a').head ∧ R (pure r').tail (pure a').tail

Tactic:
r

Goal state after:
case refine_1.refine_1
α : Type u
R : Computation α → Computation α → Prop
bisim : IsBisimulation R
s₁ s₂ : Computation α
r✝ : R s₁ s₂
t₁ t₂ : Stream' (Option α)
e : ∃ s s', s.val = t₁ ∧ s'.val = t₂ ∧ R s s'
s s' : Computation α
r' a' : α
r : R (pure r') (pure a')
⊢ BisimO R (pure r').destruct (pure a').destruct → (pure r').head = (pure a').head ∧ R (pure r').tail (pure a').tail
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: case refine_1.refine_2
α : Type u
R : Computation α → Computation α → Prop
bisim : IsBisimulation R
s₁ s₂ : Computation α
r : R s₁ s₂
t₁ t₂ : Stream' (Option α)
e : ∃ s s', s.val = t₁ ∧ s'.val = t₂ ∧ R s s'
s s' : Computation α
r' : α
a' : Computation α
⊢ R (pure r') a'.think →
    BisimO R (pure r').destruct a'.think.destruct → (pure r').head = a'.think.head ∧ R (pure r').tail a'.think.tail

Tactic:
r

Goal state after:
case refine_1.refine_2
α : Type u
R : Computation α → Computation α → Prop
bisim : IsBisimulation R
s₁ s₂ : Computation α
r✝ : R s₁ s₂
t₁ t₂ : Stream' (Option α)
e : ∃ s s', s.val = t₁ ∧ s'.val = t₂ ∧ R s s'
s s' : Computation α
r' : α
a' : Computation α
r : R (pure r') a'.think
⊢ BisimO R (pure r').destruct a'.think.destruct → (pure r').head = a'.think.head ∧ R (pure r').tail a'.think.tail
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: case refine_2.refine_1
α : Type u
R : Computation α → Computation α → Prop
bisim : IsBisimulation R
s₁ s₂ : Computation α
r : R s₁ s₂
t₁ t₂ : Stream' (Option α)
e : ∃ s s', s.val = t₁ ∧ s'.val = t₂ ∧ R s s'
s s' r' : Computation α
a' : α
⊢ R r'.think (pure a') →
    BisimO R r'.think.destruct (pure a').destruct → r'.think.head = (pure a').head ∧ R r'.think.tail (pure a').tail

Tactic:
r

Goal state after:
case refine_2.refine_1
α : Type u
R : Computation α → Computation α → Prop
bisim : IsBisimulation R
s₁ s₂ : Computation α
r✝ : R s₁ s₂
t₁ t₂ : Stream' (Option α)
e : ∃ s s', s.val = t₁ ∧ s'.val = t₂ ∧ R s s'
s s' r' : Computation α
a' : α
r : R r'.think (pure a')
⊢ BisimO R r'.think.destruct (pure a').destruct → r'.think.head = (pure a').head ∧ R r'.think.tail (pure a').tail
Module: Mathlib.Data.Seq.Computation

Goal state before:
pp: case refine_2.refine_2
α : Type u
R : Computation α → Computation α → Prop
bisim : IsBisimulation R
s₁ s₂ : Computation α
r : R s₁ s₂
t₁ t₂ : Stream' (Option α)
e : ∃ s s', s.val = t₁ ∧ s'.val = t₂ ∧ R s s'
s s' r' a' : Computation α
⊢ R r'.think a'.think →
    BisimO R r'.think.destruct a'.think.destruct → r'.think.head = a'.think.head ∧ R r'.think.tail a'.think.tail

Tactic:
r

Goal state after:
case refine_2.refine_2
α : Type u
R : Computation α → Computation α → Prop
bisim : IsBisimulation R
s₁ s₂ : Computation α
r✝ : R s₁ s₂
t₁ t₂ : Stream' (Option α)
e : ∃ s s', s.val = t₁ ∧ s'.val = t₂ ∧ R s s'
s s' r' a' : Computation α
r : R r'.think a'.think
⊢ BisimO R r'.think.destruct a'.think.destruct → r'.think.head = a'.think.head ∧ R r'.think.tail a'.think.tail
Module: Mathlib.Data.Stream.Init

Goal state before:
pp: α : Type u
x y : List α
a b : Stream' α
h : x ++ₛ a = y ++ₛ b
hl : x.length = y.length
⊢ x = y

Tactic:
by
  apply List.ext_getElem hl
  intros
  rw [← get_append_left, ← get_append_left, h]

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

Goal state before:
pp: α : Type u
m n : ℕ
a : Stream' α
h : m < (take n a).length
⊢ (take n a)[m] = a.get m

Tactic:
nth_rw 2 [← append_take_drop n a]; rw [get_append_left]

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

Goal state before:
pp: α : Type u
s : Seq α
n : ℕ
h : s.Terminates
⊢ n < s.length h ↔ ∃ a, a ∈ s.get? n

Tactic:
← lt_length_iff'

Goal state after:
α : Type u
s : Seq α
n : ℕ
h : s.Terminates
⊢ n < s.length h ↔ ∀ (h : s.Terminates), n < s.length h
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: α : Type u
s : Seq α
h : s.Terminates
⊢ ↑(s.toList h) = s

Tactic:
ext n; simp [ofList]

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

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

Tactic:
change s.get? n = none at terminatedAt_n

Goal state after:
K : Type u_1
n : ℕ
inst✝ : DivisionRing K
s : Stream'.Seq (Pair K)
terminatedAt_n : s.get? n = none
⊢ convs'Aux s (n + 1) = convs'Aux s n
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: case bisim.nil.nil.cons
α : Type u
s t u✝ : Seq α
x✝ : α
u : Seq α
⊢ BisimO (fun s1 s2 ↦ ∃ s t u, s1 = (s.append t).append u ∧ s2 = s.append (t.append u))
    ((nil.append nil).append (cons x✝ u)).destruct (nil.append (nil.append (cons x✝ u))).destruct

Tactic:
simpa using ⟨nil, nil, u, by simp, by simp⟩

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

Goal state before:
pp: case refine_2
α : Type u
β : Type v
R : α → β → Prop
C : Computation α → Computation β → Prop
H : ∀ {ca : Computation α} {cb : Computation β}, C ca cb → LiftRelAux R C ca.destruct cb.destruct
ca : Computation α
a : α
ha : a ∈ ca
ca' : Computation α
IH : ∀ (cb : Computation β), C ca' cb → LiftRel R ca' cb
cb : Computation β
Hc : C ca'.think cb
h : LiftRelAux R C ca'.think.destruct cb.destruct
⊢ LiftRel R ca'.think cb

Tactic:
simp only [liftRel_think_left]
    induction cb using recOn with
    | pure b => simpa using h
    | think cb => simpa [h] using IH _ h

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

Goal state before:
pp: case inr.inr
K : Type u_1
inst✝³ : DivisionRing K
inst✝² : LinearOrder K
inst✝¹ : FloorRing K
v : K
inst✝ : IsStrictOrderedRing K
n : ℕ
h : fract v ≠ 0
h₁ : (of (fract v)⁻¹).s.get? n ≠ none
p : Pair K
hp : (of (fract v)⁻¹).s.get? n = some p
⊢ (of v).s.get? (n + 1) = (of (fract v)⁻¹).s.get? n

Tactic:
obtain ⟨p', hp'₁, _⟩ := exists_succ_get?_stream_of_gcf_of_get?_eq_some hp

Goal state after:
case inr.inr
K : Type u_1
inst✝³ : DivisionRing K
inst✝² : LinearOrder K
inst✝¹ : FloorRing K
v : K
inst✝ : IsStrictOrderedRing K
n : ℕ
h : fract v ≠ 0
h₁ : (of (fract v)⁻¹).s.get? n ≠ none
p : Pair K
hp : (of (fract v)⁻¹).s.get? n = some p
p' : IntFractPair K
hp'₁ : IntFractPair.stream (fract v)⁻¹ (n + 1) = some p'
right✝ : ↑p'.b = p.b
⊢ (of v).s.get? (n + 1) = (of (fract v)⁻¹).s.get? n
Module: Mathlib.Algebra.ContinuedFractions.Computation.CorrectnessTerminating

Goal state before:
pp: case succ
K : Type u_1
inst✝² : Field K
inst✝¹ : LinearOrder K
v : K
n✝ : ℕ
inst✝ : FloorRing K
g : GenContFract K := of v
n : ℕ
ifp_succ_n : IntFractPair K
succ_nth_stream_eq : IntFractPair.stream v (n + 1) = some ifp_succ_n
ifp_n : IntFractPair K
nth_stream_eq : IntFractPair.stream v n = some ifp_n
nth_fract_ne_zero : ifp_n.fr ≠ 0
conts : Pair K := g.contsAux (n + 2)
pconts : Pair K := g.contsAux (n + 1)
IH :
  ∀ {ifp_n : IntFractPair K},
    IntFractPair.stream v n = some ifp_n → v = compExactValue ((of v).contsAux n) pconts ifp_n.fr
pconts_eq : pconts = g.contsAux (n + 1)
⊢ v = compExactValue pconts ((of v).contsAux (n + 1 + 1)) ifp_succ_n.fr

Tactic:
set ppconts := g.contsAux n with ppconts_eq

Goal state after:
case succ
K : Type u_1
inst✝² : Field K
inst✝¹ : LinearOrder K
v : K
n✝ : ℕ
inst✝ : FloorRing K
g : GenContFract K := of v
n : ℕ
ifp_succ_n : IntFractPair K
succ_nth_stream_eq : IntFractPair.stream v (n + 1) = some ifp_succ_n
ifp_n : IntFractPair K
nth_stream_eq : IntFractPair.stream v n = some ifp_n
nth_fract_ne_zero : ifp_n.fr ≠ 0
conts : Pair K := g.contsAux (n + 2)
pconts : Pair K := g.contsAux (n + 1)
pconts_eq : pconts = g.contsAux (n + 1)
ppconts : Pair K := g.contsAux n
IH : ∀ {ifp_n : IntFractPair K}, IntFractPair.stream v n = some ifp_n → v = compExactValue ppconts pconts ifp_n.fr
ppconts_eq : ppconts = g.contsAux n
⊢ v = compExactValue pconts ((of v).contsAux (n + 1 + 1)) ifp_succ_n.fr
Module: Mathlib.Data.Nat.Fib.Basic

Goal state before:
pp: x✝ : ℕ
⊢ fib x✝ = x✝.fastFib

Tactic:
fastFib_eq

Goal state after:
x✝ : ℕ
⊢ fib x✝ = fib x✝
Module: Mathlib.Data.Seq.Basic

Goal state before:
pp: case bisim
α : Type u
SS : Seq (Seq1 (Seq1 α))
⊢ Seq.IsBisimulation fun s1 s2 ↦ ∃ s SS, s1 = s.append SS.join.join ∧ s2 = s.append (Seq.map join SS).join

Tactic:
rintro s1 s2 ⟨s, SS, rfl, rfl⟩

Goal state after:
case bisim
α : Type u
SS✝ : Seq (Seq1 (Seq1 α))
s : Seq α
SS : Seq (Seq1 (Seq1 α))
⊢ BisimO (fun s1 s2 ↦ ∃ s SS, s1 = s.append SS.join.join ∧ s2 = s.append (Seq.map join SS).join)
    (s.append SS.join.join).destruct (s.append (Seq.map join SS).join).destruct
Module: Mathlib.Data.Nat.Fib.Basic

Goal state before:

Tactic:
fib (n + 2) = fib n + fib (n + 1) := fib_add_two
      _ = (fib n + ∑ k ∈ Finset.range n, fib k) + 1 := by rw [ih, add_assoc]
      _ = (∑ k ∈ Finset.range (n + 1), fib k) + 1 := by simp [Finset.range_add_one]

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

Goal state before:
pp: K : Type u_1
v : K
inst✝⁴ : Field K
inst✝³ : LinearOrder K
inst✝² : IsStrictOrderedRing K
inst✝¹ : FloorRing K
inst✝ : Archimedean K
ε : K
ε_pos : ε > 0
N' : ℕ
one_div_ε_lt_N' : 1 / ε < ↑N'
N : ℕ := max N' 5
⊢ ∀ n ≥ N, |v - (of v).convs n| < ε

Tactic:
intro n n_ge_N

Goal state after:
K : Type u_1
v : K
inst✝⁴ : Field K
inst✝³ : LinearOrder K
inst✝² : IsStrictOrderedRing K
inst✝¹ : FloorRing K
inst✝ : Archimedean K
ε : K
ε_pos : ε > 0
N' : ℕ
one_div_ε_lt_N' : 1 / ε < ↑N'
N : ℕ := max N' 5
n : ℕ
n_ge_N : n ≥ N
⊢ |v - (of v).convs n| < ε
Module: Mathlib.Algebra.ContinuedFractions.Computation.TerminatesIffRat

Goal state before:
pp: q : ℚ
⊢ ∃ n, IntFractPair.stream q n = none

Tactic:
let fract_q_num := (Int.fract q).num

Goal state after:
q : ℚ
fract_q_num : ℤ := (Int.fract q).num
⊢ ∃ n, IntFractPair.stream q n = none
Module: Mathlib.Algebra.ContinuedFractions.Computation.Approximations

Goal state before:
pp: K : Type u_1
v : K
n : ℕ
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : FloorRing K
gp : Pair K
nth_s_eq : (of v).s.get? n = some gp
ifp : IntFractPair K
stream_succ_nth_eq : IntFractPair.stream v (n + 1) = some ifp
this : (of v).s.get? n = some { a := 1, b := ↑ifp.b }
⊢ gp = { a := 1, b := ↑ifp.b }

Tactic:
have : some gp = some ⟨1, ifp.b⟩ := by rwa [nth_s_eq] at this

Goal state after:
K : Type u_1
v : K
n : ℕ
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : FloorRing K
gp : Pair K
nth_s_eq : (of v).s.get? n = some gp
ifp : IntFractPair K
stream_succ_nth_eq : IntFractPair.stream v (n + 1) = some ifp
this✝ : (of v).s.get? n = some { a := 1, b := ↑ifp.b }
this : some gp = some { a := 1, b := ↑ifp.b }
⊢ gp = { a := 1, b := ↑ifp.b }
Module: Mathlib.Algebra.ContinuedFractions.Computation.Approximations

Goal state before:
pp: case succ.succ
K : Type u_1
v : K
n✝ : ℕ
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : FloorRing K
n : ℕ
IH : ∀ m < n + 1 + 1, m ≤ 1 ∨ ¬(of v).TerminatedAt (m - 2) → ↑(fib m) ≤ ((of v).contsAux m).b
hyp : n + 1 + 1 ≤ 1 ∨ ¬(of v).TerminatedAt (n + 1 + 1 - 2)
g : GenContFract K := of v
this : ¬n + 2 ≤ 1
not_terminatedAt_n : ¬g.TerminatedAt n
gp : Pair K
s_ppred_nth_eq : g.s.get? n = some gp
pconts : Pair K := g.contsAux (n + 1)
pconts_eq : pconts = g.contsAux (n + 1)
⊢ ↑(fib (n + 1 + 1)) ≤ ((of v).contsAux (n + 1 + 1)).b

Tactic:
set ppconts := g.contsAux n with ppconts_eq

Goal state after:
case succ.succ
K : Type u_1
v : K
n✝ : ℕ
inst✝³ : Field K
inst✝² : LinearOrder K
inst✝¹ : IsStrictOrderedRing K
inst✝ : FloorRing K
n : ℕ
IH : ∀ m < n + 1 + 1, m ≤ 1 ∨ ¬(of v).TerminatedAt (m - 2) → ↑(fib m) ≤ ((of v).contsAux m).b
hyp : n + 1 + 1 ≤ 1 ∨ ¬(of v).TerminatedAt (n + 1 + 1 - 2)
g : GenContFract K := of v
this : ¬n + 2 ≤ 1
not_terminatedAt_n : ¬g.TerminatedAt n
gp : Pair K
s_ppred_nth_eq : g.s.get? n = some gp
pconts : Pair K := g.contsAux (n + 1)
pconts_eq : pconts = g.contsAux (n + 1)
ppconts : Pair K := g.contsAux n
ppconts_eq : ppconts = g.contsAux n
⊢ ↑(fib (n + 1 + 1)) ≤ ((of v).contsAux (n + 1 + 1)).b
Module: Mathlib.Algebra.CubicDiscriminant

Goal state before:
pp: R : Type u_1
P : Cubic R
inst✝ : Semiring R
h0 : P.a ≠ 0 ∨ P.b ≠ 0 ∨ P.c ≠ 0 ∨ P.d ≠ 0
⊢ P.toPoly ≠ 0

Tactic:
contrapose! h0

Goal state after:
R : Type u_1
P : Cubic R
inst✝ : Semiring R
h0 : P.toPoly = 0
⊢ P.a = 0 ∧ P.b = 0 ∧ P.c = 0 ∧ P.d = 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 : ℕ∞
⊢ Directed (fun x1 x2 ↦ x1 ≤ x2) fun l ↦ (f.genEigenspace μ) ↑↑l

Tactic:
by
  have aux : Monotone ((↑) : {l : ℕ // l ≤ k} → ℕ∞) := fun x y h ↦ by simpa using h
  exact ((genEigenspace f μ).monotone.comp aux).directed_le

Goal state after:
Module: Mathlib.RingTheory.Idempotents

Goal state before:
pp: case cons
R : Type u_1
inst✝ : CommRing R
I : Type u_3
e : I → R
he : OrthogonalIdempotents e
a : I
s : Finset I
has : a ∉ s
ih : ∏ i ∈ s, (1 - e i) = 1 - ∑ i ∈ s, e i
⊢ ∏ i ∈ Finset.cons a s has, (1 - e i) = 1 - ∑ i ∈ Finset.cons a s has, e i

Tactic:
| cons a s has ih =>

Goal state after:
Module: Mathlib.RingTheory.Idempotents

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
e f : R
he : IsIdempotentElem e
hf : IsIdempotentElem f
hef₁ : e + f = 1
hef₂ : e * f = 0
o : Fin 2 → R :=
  fun i ↦
    match i with
    | 0 => e
    | 1 => f
⊢ Function.Bijective ⇑(RingHom.pi fun i ↦ Ideal.Quotient.mk (Ideal.span {o i}))

Tactic:
apply pi_bijective_of_isIdempotentElem

Goal state after:
case he
R : Type u_1
inst✝ : CommRing R
e f : R
he : IsIdempotentElem e
hf : IsIdempotentElem f
hef₁ : e + f = 1
hef₂ : e * f = 0
o : Fin 2 → R := ⋯
⊢ ∀ (i : Fin 2), IsIdempotentElem (o i)

case he₁
R : Type u_1
inst✝ : CommRing R
e f : R
he : IsIdempotentElem e
hf : IsIdempotentElem f
hef₁ : e + f = 1
hef₂ : e * f = 0
o : Fin 2 → R := ⋯
⊢ ∀ (i j : Fin 2), i ≠ j → (1 - o i) * (1 - o j) = 0

case he₂
R : Type u_1
inst✝ : CommRing R
e f : R
he : IsIdempotentElem e
hf : IsIdempotentElem f
hef₁ : e + f = 1
hef₂ : e * f = 0
o : Fin 2 → R := ⋯
⊢ ∏ i, o i = 0
Module: Mathlib.LinearAlgebra.Matrix.Ideal

Goal state before:
pp: case mp
R : Type u_1
n : Type u_2
inst✝³ : NonAssocRing R
inst✝² : Fintype n
inst✝¹ : Nonempty n
inst✝ : DecidableEq n
I J : TwoSidedIdeal R
⊢ matrix n I ≤ matrix n J → I ≤ J

Tactic:
intro le x xI

Goal state after:
case mp
R : Type u_1
n : Type u_2
inst✝³ : NonAssocRing R
inst✝² : Fintype n
inst✝¹ : Nonempty n
inst✝ : DecidableEq n
I J : TwoSidedIdeal R
le : matrix n I ≤ matrix n J
x : R
xI : x ∈ I
⊢ x ∈ J
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 m : ℕ∞
hm : 0 < m
hk : f.HasUnifEigenvalue μ k
⊢ f.HasUnifEigenvalue μ m

Tactic:
apply HasUnifEigenvalue.le (k := 1) (Order.one_le_iff_pos.mpr hm)

Goal state after:
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ : R
k m : ℕ∞
hm : 0 < m
hk : f.HasUnifEigenvalue μ k
⊢ f.HasUnifEigenvalue μ 1
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 g : End R M
h : Commute f g
μ : R
k : ℕ∞
⊢ MapsTo ⇑g ↑((f.genEigenspace μ) k) ↑((f.genEigenspace μ) k)

Tactic:
by
  intro x hx
  simp only [SetLike.mem_coe, mem_genEigenspace, LinearMap.mem_ker] at hx ⊢
  rcases hx with ⟨l, hl, hx⟩
  replace h : Commute ((f - μ • (1 : End R M)) ^ l) g :=
    (h.sub_left <| Algebra.commute_algebraMap_left μ g).pow_left l
  use l, hl
  rw [← LinearMap.comp_apply, ← Module.End.mul_eq_comp, h.eq, Module.End.mul_eq_comp,
    LinearMap.comp_apply, hx, map_zero]

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

Goal state before:
pp: R : Type u_2
M : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : IsDomain R
inst✝² : IsPrincipalIdealRing R
inst✝¹ : Free R M
inst✝ : Module.Finite R M
f g : End R M
h_comm✝ : Commute f g
hf : ⨆ μ, f.maxGenEigenspace μ = ⊤
hg : ∀ (μ : R), (trace R ↥(f.maxGenEigenspace μ)) (restrict g ⋯) = 0
hfg : ∀ (μ : R), MapsTo ⇑(g ∘ₗ f) ↑(f.maxGenEigenspace μ) ↑(f.maxGenEigenspace μ)
μ : R
hf' : MapsTo ⇑f ↑(f.maxGenEigenspace μ) ↑(f.maxGenEigenspace μ)
hg' : MapsTo ⇑g ↑(f.maxGenEigenspace μ) ↑(f.maxGenEigenspace μ)
h_comm : Commute (restrict g ⋯) (restrict f ⋯)
this : IsNilpotent (restrict (f - (algebraMap R (End R M)) μ) ⋯)
⊢ μ * (trace R ↥(f.maxGenEigenspace μ)) (restrict g ⋯) = 0

Tactic:
hg,

Goal state after:
R : Type u_2
M : Type u_3
inst✝⁶ : CommRing R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : IsDomain R
inst✝² : IsPrincipalIdealRing R
inst✝¹ : Free R M
inst✝ : Module.Finite R M
f g : End R M
h_comm✝ : Commute f g
hf : ⨆ μ, f.maxGenEigenspace μ = ⊤
hg : ∀ (μ : R), (trace R ↥(f.maxGenEigenspace μ)) (restrict g ⋯) = 0
hfg : ∀ (μ : R), MapsTo ⇑(g ∘ₗ f) ↑(f.maxGenEigenspace μ) ↑(f.maxGenEigenspace μ)
μ : R
hf' : MapsTo ⇑f ↑(f.maxGenEigenspace μ) ↑(f.maxGenEigenspace μ)
hg' : MapsTo ⇑g ↑(f.maxGenEigenspace μ) ↑(f.maxGenEigenspace μ)
h_comm : Commute (restrict g ⋯) (restrict f ⋯)
this : IsNilpotent (restrict (f - (algebraMap R (End R M)) μ) ⋯)
⊢ μ * 0 = 0
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
N : Type u_3
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : M →ₗ[R] M
e : M ≃ₗ[R] N
⊢ (trace R N) (e.conj f) = (trace R M) f

Tactic:
by
  classical
  by_cases hM : ∃ s : Finset M, Nonempty (Basis s R M)
  · obtain ⟨s, ⟨b⟩⟩ := hM
    have := Module.Finite.of_basis b
    have := (Module.free_def R M).mpr ⟨_, ⟨b⟩⟩
    have := Module.Finite.of_basis (b.map e)
    have := (Module.free_def R N).mpr ⟨_, ⟨(b.map e).reindex (e.toEquiv.image _)⟩⟩
    rw [e.conj_apply, trace_comp_comm', ← comp_assoc, LinearEquiv.comp_coe,
      LinearEquiv.self_trans_symm, LinearEquiv.refl_toLinearMap, id_comp]
  · rw [trace, trace, dif_neg hM, dif_neg ?_, zero_apply, zero_apply]
    rintro ⟨s, ⟨b⟩⟩
    exact hM ⟨s.image e.symm, ⟨(b.map e.symm).reindex
      ((e.symm.toEquiv.image s).trans (Equiv.setCongr Finset.coe_image.symm))⟩⟩

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✝ : IsReduced R
f g : End R M
μ : R
h_comm : Commute f g
n : End R M := g - (algebraMap R (End R M)) μ
hg : (trace R M) (f ∘ₗ n) = 0
hμ : g = (algebraMap R (End R M)) μ + n
this : f ∘ₗ (algebraMap R (M →ₗ[R] M)) μ = μ • f
⊢ (trace R M) (f ∘ₗ (algebraMap R (End R M)) μ) + (trace R M) (f ∘ₗ n) = μ * (trace R M) f

Tactic:
hg,

Goal state after:
R : Type u_1
inst✝³ : CommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsReduced R
f g : End R M
μ : R
h_comm : Commute f g
n : End R M := g - (algebraMap R (End R M)) μ
hg : (trace R M) (f ∘ₗ n) = 0
hμ : g = (algebraMap R (End R M)) μ + n
this : f ∘ₗ (algebraMap R (M →ₗ[R] M)) μ = μ • f
⊢ (trace R M) (f ∘ₗ (algebraMap R (End R M)) μ) + 0 = μ * (trace R M) f
Module: Mathlib.GroupTheory.FreeGroup.Reduce

Goal state before:
pp: α : Type u_1
L : List (α × Bool)
inst✝ : DecidableEq α
h : reduce L = L
⊢ IsChain (fun a b ↦ a.1 = b.1 → a.2 = b.2) L

Tactic:
List.isChain_iff_forall_rel_of_append_cons_cons

Goal state after:
α : Type u_1
L : List (α × Bool)
inst✝ : DecidableEq α
h : reduce L = L
⊢ ∀ ⦃a b : α × Bool⦄ ⦃l₁ l₂ : List (α × Bool)⦄, L = l₁ ++ a :: b :: l₂ → a.1 = b.1 → a.2 = b.2
Module: Mathlib.Algebra.FreeMonoid.FreeSemigroup

Goal state before:
pp: α : Type u_1
x : α
xs : List α
⊢ ∀ (x : FreeMonoid α), List.foldl (fun x1 x2 ↦ x1 * x2) x (List.map FreeMonoid.of xs) = x * ofList xs

Tactic:
induction xs with

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

Goal state before:
pp: case right
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra R K
q f g : R[X]
p : ℕ
hq_irr : Irreducible (map (algebraMap R K) q)
hq_monic : q.Monic
hf_lC : (algebraMap R K) f.leadingCoeff ≠ 0
hf_prim : ∀ (r : R), C r ∣ f → IsUnit r
hfmodP : map (algebraMap R K) f = C ((algebraMap R K) f.leadingCoeff) * map (algebraMap R K) q ^ p
hg_div : g ∣ f
P : Ideal R := ⋯
hP : P.IsPrime
hgP : g.leadingCoeff ∉ P
map_dvd_pow_q : map (algebraMap R K) g ∣ map (algebraMap R K) q ^ p
m : ℕ
hm✝ : m ≤ p
hf : Associated (map (algebraMap R K) g) (map (algebraMap R K) q ^ m)
r : R[X] := ⋯
hg : g = C g.leadingCoeff + r
hr : map (algebraMap R K) r = 0
hm : m = 0
hg' : ¬g.natDegree = 0
⊢ g.leadingCoeff ∈ P

Tactic:
hg,

Goal state after:
case right
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
K : Type u_2
inst✝¹ : Field K
inst✝ : Algebra R K
q f g : R[X]
p : ℕ
hq_irr : Irreducible (map (algebraMap R K) q)
hq_monic : q.Monic
hf_lC : (algebraMap R K) f.leadingCoeff ≠ 0
hf_prim : ∀ (r : R), C r ∣ f → IsUnit r
hfmodP : map (algebraMap R K) f = C ((algebraMap R K) f.leadingCoeff) * map (algebraMap R K) q ^ p
hg_div : g ∣ f
P : Ideal R := ker (algebraMap R K)
hP : P.IsPrime
hgP : g.leadingCoeff ∉ P
map_dvd_pow_q : map (algebraMap R K) g ∣ map (algebraMap R K) q ^ p
m : ℕ
hm✝ : m ≤ p
hf : Associated (map (algebraMap R K) g) (map (algebraMap R K) q ^ m)
r : R[X] := g - C g.leadingCoeff * q ^ m
hg : g = C g.leadingCoeff + r
hr : map (algebraMap R K) r = 0
hm : m = 0
hg' : ¬g.natDegree = 0
⊢ (C g.leadingCoeff + r).leadingCoeff ∈ P
Module: Mathlib.RingTheory.IntegralClosure.IntegrallyClosed

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f✝ : R ≃+* S
h : IsIntegrallyClosed R
x✝ : Algebra S R := f✝.symm.toRingHom.toAlgebra
f : S ≃ₐ[S] R := AlgEquiv.ofRingEquiv ⋯
g : FractionRing S ≃ₐ[S] FractionRing R := IsFractionRing.algEquivOfAlgEquiv f
⊢ IsIntegrallyClosed S

Tactic:
refine (isIntegrallyClosed_iff (FractionRing S)).mpr (fun hx ↦ ?_)

Goal state after:
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f✝ : R ≃+* S
h : IsIntegrallyClosed R
x✝¹ : Algebra S R := f✝.symm.toRingHom.toAlgebra
f : S ≃ₐ[S] R := AlgEquiv.ofRingEquiv ⋯
g : FractionRing S ≃ₐ[S] FractionRing R := IsFractionRing.algEquivOfAlgEquiv f
x✝ : FractionRing S
hx : IsIntegral S x✝
⊢ ∃ y, (algebraMap S (FractionRing S)) y = x✝
Module: Mathlib.Algebra.Group.Action.Equidecomp

Goal state before:
pp: X : Type u_1
G : Type u_2
inst✝ : SMul G X
⊢ Injective toPartialEquiv

Tactic:
intro ⟨_, _, _⟩ _ _
  congr

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
⊢ g * h %ₘ q = r * s %ₘ q

Tactic:
hg,

Goal state after:
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
⊢ (C g.leadingCoeff * q ^ m + r) * h %ₘ q = r * s %ₘ q