mathlib-initiative/mathlib-tactics huggingface dataset:
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)
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 *
        { a := gp.b * (g.contsAux (n + 1)).a + gp.a * (g.contsAux n).a,
            b := gp.b * (g.contsAux (n + 1)).b + gp.a * (g.contsAux n).b }.b -
      pB *
        { a := gp.b * (g.contsAux (n + 1)).a + gp.a * (g.contsAux n).a,
            b := gp.b * (g.contsAux (n + 1)).b + gp.a * (g.contsAux n).b }.a =
    (ppA * pB - ppB * pA) * -gp.a

Tactic:
ring

Goal state after:
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 : ℕ
⊢ (of v).TerminatedAt n ↔ IntFractPair.stream v (n + 1) = none

Tactic:
by
  rw [of_terminatedAt_iff_intFractPair_seq1_terminatedAt, Stream'.Seq.TerminatedAt,
    IntFractPair.get?_seq1_eq_succ_get?_stream]

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

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
α' : Type u'
β' : Type v'
s₁ : Seq α
s₂ : Seq β
f₁ : α → α'
f₂ : β → β'
g : α' → β' → γ
⊢ zipWith g (map f₁ s₁) (map f₂ s₂) = zipWith (fun a b ↦ g (f₁ a) (f₂ b)) s₁ s₂

Tactic:
by
  ext1 n
  simp only [get?_zipWith, map_get?]
  cases s₁.get? n <;> cases s₂.get? n <;> simp

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

Goal state before:
pp: K : Type u_1
inst✝² : Field K
inst✝¹ : LinearOrder K
inst✝ : FloorRing K
a b c : K
fract_a_ne_zero : Int.fract a ≠ 0
⊢ ↑⌊a⌋ * b + c + b * (a - ↑⌊a⌋) = b * a + c

Tactic:
ring

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

Goal state before:
pp: α : Type u
p : α → Prop
s : Seq α
h : ∀ (n : ℕ) (x : α), s.get? n = some x → p x
⊢ ∀ x ∈ s, p x

Tactic:
by
  simp only [mem_iff_exists_get?]
  grind

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

Goal state before:
pp: case refine_2
α β : Type u
f : α → β
p : β → Prop
s : Seq α
x✝¹ : ∀ x ∈ s, (p ∘ f) x
x✝ : β
hx : x✝ ∈ map f s
w✝ : α
left✝ : w✝ ∈ s
hx' : f w✝ = x✝
⊢ p x✝

Tactic:
← hx'

Goal state after:
case refine_2
α β : Type u
f : α → β
p : β → Prop
s : Seq α
x✝¹ : ∀ x ∈ s, (p ∘ f) x
x✝ : β
hx : x✝ ∈ map f s
w✝ : α
left✝ : w✝ ∈ s
hx' : f w✝ = x✝
⊢ p (f w✝)
Module: Mathlib.Data.Nat.Fib.Basic

Goal state before:
pp: case succ
n m : ℕ
ih : fib (m + (n + 1) + 1) = fib (m + 1) * fib n + fib (m + 1 + 1) * fib (n + 1)
⊢ fib (m + 1) * fib n + (fib m + fib (m + 1)) * fib (n + 1) = fib m * fib (n + 1) + fib (m + 1) * (fib n + fib (n + 1))

Tactic:
ring

Goal state after:
Module: Mathlib.Data.Nat.Fib.Basic

Goal state before:
pp: case succ
n✝ : ℕ
⊢ fib (n✝ + 1) * fib n✝ + (fib n✝ + fib (n✝ + 1)) * fib (n✝ + 1) = fib (n✝ + 1) * (fib n✝ + fib (n✝ + 1) + fib n✝)

Tactic:
ring

Goal state after:
Module: Mathlib.Data.Nat.Fib.Basic

Goal state before:
pp: n : ℕ
⊢ fib n * fib n + fib (n + 1) * fib (n + 1) = fib (n + 1) ^ 2 + fib n ^ 2

Tactic:
ring

Goal state after:
Module: Mathlib.Data.Nat.Fib.Basic

Goal state before:
pp: n : ℕ
this : fib n ≤ 2 * fib (n + 1)
⊢ ↑(fib n) * (2 * ↑(fib (n + 1)) - ↑(fib n)) + (↑(fib (n + 1)) ^ 2 + ↑(fib n) ^ 2) =
    ↑(fib (n + 1)) * (2 * ↑(fib n) + ↑(fib (n + 1)))

Tactic:
ring

Goal state after:
Module: Mathlib.Data.Nat.Fib.Basic

Goal state before:
pp: n : ℕ
⊢ (bit false n).fastFibAux =
    let p := n.fastFibAux;
    (p.1 * (2 * p.2 - p.1), p.2 ^ 2 + p.1 ^ 2)

Tactic:
fastFibAux,

Goal state after:
n : ℕ
⊢ binaryRec (fib 0, fib 1)
      (fun b x p ↦
        if b = true then (p.2 ^ 2 + p.1 ^ 2, p.2 * (2 * p.1 + p.2)) else (p.1 * (2 * p.2 - p.1), p.2 ^ 2 + p.1 ^ 2))
      (bit false n) =
    let p := n.fastFibAux;
    (p.1 * (2 * p.2 - p.1), p.2 ^ 2 + p.1 ^ 2)
Module: Mathlib.Data.Nat.Fib.Basic

Goal state before:
pp: n : ℕ
⊢ (bit true n).fastFibAux =
    let p := n.fastFibAux;
    (p.2 ^ 2 + p.1 ^ 2, p.2 * (2 * p.1 + p.2))

Tactic:
fastFibAux,

Goal state after:
n : ℕ
⊢ binaryRec (fib 0, fib 1)
      (fun b x p ↦
        if b = true then (p.2 ^ 2 + p.1 ^ 2, p.2 * (2 * p.1 + p.2)) else (p.1 * (2 * p.2 - p.1), p.2 ^ 2 + p.1 ^ 2))
      (bit true n) =
    let p := n.fastFibAux;
    (p.2 ^ 2 + p.1 ^ 2, p.2 * (2 * p.1 + p.2))
Module: Mathlib.Data.Nat.Fib.Basic

Goal state before:
pp: case H1
m n : ℕ
a✝ : 0 < m
h' : fib ((n % m).gcd m) = (fib (n % m)).gcd (fib m)
⊢ fib (m.gcd n) = (fib m).gcd (fib n)

Tactic:
rw [← gcd_rec m n] at h'

Goal state after:
case H1
m n : ℕ
a✝ : 0 < m
h' : fib (m.gcd n) = (fib (n % m)).gcd (fib m)
⊢ fib (m.gcd n) = (fib m).gcd (fib n)
Module: Mathlib.Algebra.ContinuedFractions.ConvergentsEquiv

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

Tactic:
| some gp_succ_n =>

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

Goal state before:
pp: case inr
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
g : GenContFract K := of v
not_terminatedAt_n : ¬g.TerminatedAt n
B : K := g.dens n
nB : K := g.dens (n + 1)
abs_v_sub_conv_le : |v - g.convs n| ≤ 1 / (B * nB)
⊢ 1 / (B * nB) < ε

Tactic:
have nB_ineq : (fib (n + 2) : K) ≤ nB :=
      succ_nth_fib_le_of_nth_den (Or.inr not_terminatedAt_n)

Goal state after:
case inr
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
g : GenContFract K := of v
not_terminatedAt_n : ¬g.TerminatedAt n
B : K := g.dens n
nB : K := g.dens (n + 1)
abs_v_sub_conv_le : |v - g.convs n| ≤ 1 / (B * nB)
nB_ineq : ↑(fib (n + 2)) ≤ nB
⊢ 1 / (B * nB) < ε
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
ifp_succ_n : IntFractPair K
succ_nth_stream_eq : IntFractPair.stream v (n + 1) = some ifp_succ_n
⊢ 1 ≤ ifp_succ_n.b

Tactic:
obtain ⟨ifp_n, nth_stream_eq, stream_nth_fr_ne_zero, ⟨-⟩⟩ :
      ∃ ifp_n, IntFractPair.stream v n = some ifp_n ∧ ifp_n.fr ≠ 0
        ∧ IntFractPair.of ifp_n.fr⁻¹ = ifp_succ_n :=
    succ_nth_stream_eq_some_iff.1 succ_nth_stream_eq
  rw [IntFractPair.of, le_floor, cast_one, one_le_inv₀
    ((nth_stream_fr_nonneg nth_stream_eq).lt_of_ne' stream_nth_fr_ne_zero)]
  exact (nth_stream_fr_lt_one nth_stream_eq).le

Goal state after:
Module: Mathlib.RingTheory.Idempotents

Goal state before:
pp: case refine_3
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
h₁ : IsIdempotentElem e'
h₂ : e' * e₂ = 0
he : f e' ∈ f.range
he₁ : IsIdempotentElem (f e')
he₁e₂ : f e' * f e₂ = 0
he₂e₁ : f e₂ * f e' = 0
⊢ (1 - e₂) * e' * e₂ = 0

pp: case refine_4
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
h₁ : IsIdempotentElem e'
h₂ : e' * e₂ = 0
he : f e' ∈ f.range
he₁ : IsIdempotentElem (f e')
he₁e₂ : f e' * f e₂ = 0
he₂e₁ : f e₂ * f e' = 0
⊢ e₂ * ((1 - e₂) * e') = 0

Tactic:
· rw [mul_assoc, h₂, mul_zero]

Goal state after:
case refine_4
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
h₁ : IsIdempotentElem e'
h₂ : e' * e₂ = 0
he : f e' ∈ f.range
he₁ : IsIdempotentElem (f e')
he₁e₂ : f e' * f e₂ = 0
he₂e₁ : f e₂ * f e' = 0
⊢ e₂ * ((1 - 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
this✝ : Nonempty { l // ↑l ≤ k }
this : Directed (fun x1 x2 ↦ x1 ≤ x2) fun i ↦ ((f - μ • 1) ^ ↑i).ker
⊢ (∃ i, ((f - μ • 1) ^ ↑i) x = 0) ↔ ∃ l, ↑l ≤ k ∧ ((f - μ • 1) ^ l) x = 0

Tactic:
Subtype.exists,

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 : ℕ∞
x : M
this✝ : Nonempty { l // ↑l ≤ k }
this : Directed (fun x1 x2 ↦ x1 ≤ x2) fun i ↦ ((f - μ • 1) ^ ↑i).ker
⊢ (∃ a, ∃ (_ : ↑a ≤ k), ((f - μ • 1) ^ a) x = 0) ↔ ∃ l, ↑l ≤ k ∧ ((f - μ • 1) ^ l) x = 0
Module: Mathlib.LinearAlgebra.Matrix.Ideal

Goal state before:
pp: R : Type u_1
inst✝² : Ring R
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
I : TwoSidedIdeal R
M : Matrix n n R
p q : n
Mmem : ∀ (y : Matrix n n R), ∃ z, z * y * (M * single q p 1) + z - 1 ∈ matrix n I
y : R
⊢ ∃ z, z * y * M p q + z - 1 ∈ I

Tactic:
specialize Mmem (y • single p p 1)

Goal state after:
R : Type u_1
inst✝² : Ring R
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
I : TwoSidedIdeal R
M : Matrix n n R
p q : n
y : R
Mmem : ∃ z, z * y • single p p 1 * (M * single q p 1) + z - 1 ∈ matrix n I
⊢ ∃ z, z * y * M p q + z - 1 ∈ I
Module: Mathlib.LinearAlgebra.Matrix.Ideal

Goal state before:
pp: case h
R : Type u_1
inst✝² : Ring R
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
I : TwoSidedIdeal R
M : Matrix n n R
p q : n
y : R
Mmem : ∃ z, z * y • single p p 1 * (M * single q p 1) + z - 1 ∈ matrix n I
N : Matrix n n R
NxMI : N * y • single p p 1 * (M * single q p 1) + N - 1 ∈ matrix n I
⊢ N p p * y * M p q + N p p - 1 ∈ I

Tactic:
simpa [mul_apply, single, ite_and] using! NxMI p p

Goal state after:
Module: Mathlib.LinearAlgebra.Trace

Goal state before:
pp: R : Type u
inst✝⁶ : CommSemiring R
M : Type v
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
ι : Type w
inst✝³ : DecidableEq ι
inst✝² : Fintype ι
κ : Type u_1
inst✝¹ : DecidableEq κ
inst✝ : Fintype κ
b : Basis ι R M
c : Basis κ R M
f : M →ₗ[R] M
⊢ ((toMatrix c c) f * (toMatrix b c) id * (toMatrix c b) id).trace = ((toMatrix c c) ((f ∘ₗ id) ∘ₗ id)).trace

Tactic:
by
        rw [LinearMap.toMatrix_comp _ b, LinearMap.toMatrix_comp _ c]

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

Goal state before:
pp: case insert
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
y : M
hy : y ∈ (f.genEigenspace μ₂) k
z : M
hz : z ∈ s.sup fun μ ↦ (f.genEigenspace μ) k
hx : y + z ∈ (f.genEigenspace μ₁) k
g : End R M := f - μ₂ • 1
⊢ y + z ∈ (f.genEigenspace μ₂) k

Tactic:
mem_genEigenspace,

Goal state after:
case insert
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
y z : M
hz : z ∈ s.sup fun μ ↦ (f.genEigenspace μ) k
hx : y + z ∈ (f.genEigenspace μ₁) k
g : End R M := f - μ₂ • 1
hy : ∃ l, ↑l ≤ k ∧ y ∈ ((f - μ₂ • 1) ^ l).ker
⊢ ∃ l, ↑l ≤ k ∧ y + z ∈ ((f - μ₂ • 1) ^ l).ker
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
inst✝³ : Free R M
inst✝² : Module.Finite R M
inst✝¹ : Free R N
inst✝ : Module.Finite R N
⊢ (llcomp R M N M).compr₂ (trace R M) = (llcomp R N M N).flip.compr₂ (trace R N)

Tactic:
by
  apply
    (compl₁₂_inj (show Surjective (dualTensorHom R N M) from (dualTensorHomEquiv R N M).surjective)
        (show Surjective (dualTensorHom R M N) from (dualTensorHomEquiv R M N).surjective)).1
  ext g m f n
  simp only [AlgebraTensorModule.curry_apply, TensorProduct.curry_apply,
    coe_restrictScalars, compl₁₂_apply, compr₂_apply, flip_apply, llcomp_apply',
    comp_dualTensorHom, LinearMapClass.map_smul, trace_eq_contract_apply,
    contractLeft_apply, smul_eq_mul, mul_comm]

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
f : End R M
p : Submodule R M
k : ℕ∞
μ : R
hfp : ∀ x ∈ p, f x ∈ p
x : ↥p
this : ∀ (l : ℕ), (genEigenspace (LinearMap.restrict f hfp) μ) ↑l = Submodule.comap p.subtype ((f.genEigenspace μ) ↑l)
⊢ x ∈ (genEigenspace (LinearMap.restrict f hfp) μ) k ↔ x ∈ Submodule.comap p.subtype ((f.genEigenspace μ) k)

Tactic:
mem_genEigenspace,

Goal state after:
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
p : Submodule R M
k : ℕ∞
μ : R
hfp : ∀ x ∈ p, f x ∈ p
x : ↥p
this : ∀ (l : ℕ), (genEigenspace (LinearMap.restrict f hfp) μ) ↑l = Submodule.comap p.subtype ((f.genEigenspace μ) ↑l)
⊢ (∃ l, ↑l ≤ k ∧ x ∈ ((LinearMap.restrict f hfp - μ • 1) ^ l).ker) ↔
    x ∈ Submodule.comap p.subtype ((f.genEigenspace μ) k)
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
μ t : R
k : ℕ∞
m : M
hm : m ∈ (f.genEigenspace μ) k
⊢ m ∈ ((t • f).genEigenspace (t * μ)) k

Tactic:
mem_genEigenspace,

Goal state after:
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ t : R
k : ℕ∞
m : M
hm : ∃ l, ↑l ≤ k ∧ m ∈ ((f - μ • 1) ^ l).ker
⊢ ∃ l, ↑l ≤ k ∧ m ∈ ((t • f - (t * μ) • 1) ^ l).ker
Module: Mathlib.LinearAlgebra.Eigenspace.Basic

Goal state before:
pp: case h.h
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ t : R
k : ℕ∞
m : M
hm : ∃ l, ∃ (_ : ↑l ≤ k), ((f - μ • 1) ^ l) m = 0
l : ℕ
hlk : ↑l ≤ k
hl : ((f - μ • 1) ^ l) m = 0
⊢ t ^ l • 0 = 0

Tactic:
smul_zero

Goal state after:
case h.h
R : Type v
M : Type w
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : End R M
μ t : R
k : ℕ∞
m : M
hm : ∃ l, ∃ (_ : ↑l ≤ k), ((f - μ • 1) ^ l) m = 0
l : ℕ
hlk : ↑l ≤ k
hl : ((f - μ • 1) ^ l) m = 0
⊢ 0 = 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₁ 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) ∈ Finset.antidiagonal (l₁ + l₂)
this : ((f₁ - μ₁ • 1) ^ i * (f₂ - μ₂ • 1) ^ j) m = 0
⊢ (l₁ + l₂).choose (i, j).1 • 0 = 0

Tactic:
smul_zero

Goal state after:
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) ∈ Finset.antidiagonal (l₁ + l₂)
this : ((f₁ - μ₁ • 1) ^ i * (f₂ - μ₂ • 1) ^ j) m = 0
⊢ 0 = 0
Module: Mathlib.LinearAlgebra.Trace

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : Ring S
inst✝² : Algebra R S
inst✝¹ : Nontrivial R
inst✝ : Free R S
h : finrank R S = 1
⊢ Function.Bijective ⇑(algebraMap R S)

Tactic:
have : Module.Finite R S := finite_of_finrank_pos (by grind)
  have : Free R (Module.End R S) := .of_equiv (dualTensorHomEquiv R S S)
  let f : S →ₐ[R] (S →ₗ[R] S) := Algebra.lmul R S
  have h1 : LinearMap.trace R S ∘ₗ f ∘ₗ Algebra.linearMap R S = LinearMap.id := by ext; simp [h]
  let b : Basis (Unit × Unit) R (End R S) :=
    .map (.tensorProduct (.dualBasis <| basisUnique Unit h) (basisUnique Unit h))
      (dualTensorHomEquiv R S S)
  have h2 : (f ∘ₗ Algebra.linearMap R S) ∘ₗ LinearMap.trace R S = LinearMap.id :=
    b.ext fun i ↦
      (basisUnique Unit h).ext fun j ↦ (by simp [f, b, Basis.tensorProduct])
  let eq : R ≃ₗ[R] End R S := .ofLinearMap (f ∘ₗ Algebra.linearMap R S) (.trace R S) h2 h1
  have hf : Function.Bijective f := ⟨Algebra.lmul_injective, .of_comp eq.surjective⟩
  exact (Function.Bijective.of_comp_iff' hf _).mp eq.bijective

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
L : Type u_1
F : Type u_2
inst✝² : Add L
inst✝¹ : FunLike F L (End R M)
inst✝ : AddHomClass F L (End R M)
f : F
μ : L → R
k : ℕ∞
h_ne : ⨅ x, ((f x).genEigenspace (μ x)) k ≠ ⊥
h : ∀ (x y : L), Commute (f x) (f y)
x y : L
⊢ μ (x + y) = μ x + μ y

Tactic:
by
  by_contra contra
  let g : L → Submodule R M := fun x ↦ (f x).genEigenspace (μ x) k
  have : ⨅ x, g x ≤ (g x ⊓ g y) ⊓ g (x + y) :=
    le_inf_iff.mpr ⟨le_inf_iff.mpr ⟨iInf_le g x, iInf_le g y⟩, iInf_le g (x + y)⟩
  refine h_ne <| eq_bot_iff.mpr (le_trans this (disjoint_iff_inf_le.mp ?_))
  apply Disjoint.mono_left (genEigenspace_inf_le_add (f x) (f y) (μ x) (μ y) k k (h x y))
  simp only [g, map_add]
  exact disjoint_genEigenspace (f x + f y) (Ne.symm contra) _ k

Goal state after:
Module: Mathlib.Algebra.DualQuaternion

Goal state before:
pp: case h2.e_re
R : Type u_1
inst✝ : CommRing R
x✝ y✝ : ℍ[DualNumber R]
⊢ TrivSqZeroExt.fst x✝.re * TrivSqZeroExt.snd y✝.re + TrivSqZeroExt.snd x✝.re * TrivSqZeroExt.fst y✝.re -
          (TrivSqZeroExt.fst x✝.imI * TrivSqZeroExt.snd y✝.imI + TrivSqZeroExt.snd x✝.imI * TrivSqZeroExt.fst y✝.imI) -
        (TrivSqZeroExt.fst x✝.imJ * TrivSqZeroExt.snd y✝.imJ + TrivSqZeroExt.snd x✝.imJ * TrivSqZeroExt.fst y✝.imJ) -
      (TrivSqZeroExt.fst x✝.imK * TrivSqZeroExt.snd y✝.imK + TrivSqZeroExt.snd x✝.imK * TrivSqZeroExt.fst y✝.imK) =
    TrivSqZeroExt.fst x✝.re * TrivSqZeroExt.snd y✝.re - TrivSqZeroExt.fst x✝.imI * TrivSqZeroExt.snd y✝.imI -
          TrivSqZeroExt.fst x✝.imJ * TrivSqZeroExt.snd y✝.imJ -
        TrivSqZeroExt.fst x✝.imK * TrivSqZeroExt.snd y✝.imK +
      (TrivSqZeroExt.snd x✝.re * TrivSqZeroExt.fst y✝.re - TrivSqZeroExt.snd x✝.imI * TrivSqZeroExt.fst y✝.imI -
          TrivSqZeroExt.snd x✝.imJ * TrivSqZeroExt.fst y✝.imJ -
        TrivSqZeroExt.snd x✝.imK * TrivSqZeroExt.fst y✝.imK)

Tactic:
ring

Goal state after:
Module: Mathlib.Algebra.DualQuaternion

Goal state before:
pp: case h2.e_imI
R : Type u_1
inst✝ : CommRing R
x✝ y✝ : ℍ[DualNumber R]
⊢ TrivSqZeroExt.fst x✝.re * TrivSqZeroExt.snd y✝.imI + TrivSqZeroExt.snd x✝.re * TrivSqZeroExt.fst y✝.imI +
          (TrivSqZeroExt.fst x✝.imI * TrivSqZeroExt.snd y✝.re + TrivSqZeroExt.snd x✝.imI * TrivSqZeroExt.fst y✝.re) +
        (TrivSqZeroExt.fst x✝.imJ * TrivSqZeroExt.snd y✝.imK + TrivSqZeroExt.snd x✝.imJ * TrivSqZeroExt.fst y✝.imK) -
      (TrivSqZeroExt.fst x✝.imK * TrivSqZeroExt.snd y✝.imJ + TrivSqZeroExt.snd x✝.imK * TrivSqZeroExt.fst y✝.imJ) =
    TrivSqZeroExt.fst x✝.re * TrivSqZeroExt.snd y✝.imI + TrivSqZeroExt.fst x✝.imI * TrivSqZeroExt.snd y✝.re +
          TrivSqZeroExt.fst x✝.imJ * TrivSqZeroExt.snd y✝.imK -
        TrivSqZeroExt.fst x✝.imK * TrivSqZeroExt.snd y✝.imJ +
      (TrivSqZeroExt.snd x✝.re * TrivSqZeroExt.fst y✝.imI + TrivSqZeroExt.snd x✝.imI * TrivSqZeroExt.fst y✝.re +
          TrivSqZeroExt.snd x✝.imJ * TrivSqZeroExt.fst y✝.imK -
        TrivSqZeroExt.snd x✝.imK * TrivSqZeroExt.fst y✝.imJ)

Tactic:
ring

Goal state after:
Module: Mathlib.Algebra.DualQuaternion

Goal state before:
pp: case h2.e_imJ
R : Type u_1
inst✝ : CommRing R
x✝ y✝ : ℍ[DualNumber R]
⊢ TrivSqZeroExt.fst x✝.re * TrivSqZeroExt.snd y✝.imJ + TrivSqZeroExt.snd x✝.re * TrivSqZeroExt.fst y✝.imJ -
          (TrivSqZeroExt.fst x✝.imI * TrivSqZeroExt.snd y✝.imK + TrivSqZeroExt.snd x✝.imI * TrivSqZeroExt.fst y✝.imK) +
        (TrivSqZeroExt.fst x✝.imJ * TrivSqZeroExt.snd y✝.re + TrivSqZeroExt.snd x✝.imJ * TrivSqZeroExt.fst y✝.re) +
      (TrivSqZeroExt.fst x✝.imK * TrivSqZeroExt.snd y✝.imI + TrivSqZeroExt.snd x✝.imK * TrivSqZeroExt.fst y✝.imI) =
    TrivSqZeroExt.fst x✝.re * TrivSqZeroExt.snd y✝.imJ - TrivSqZeroExt.fst x✝.imI * TrivSqZeroExt.snd y✝.imK +
          TrivSqZeroExt.fst x✝.imJ * TrivSqZeroExt.snd y✝.re +
        TrivSqZeroExt.fst x✝.imK * TrivSqZeroExt.snd y✝.imI +
      (TrivSqZeroExt.snd x✝.re * TrivSqZeroExt.fst y✝.imJ - TrivSqZeroExt.snd x✝.imI * TrivSqZeroExt.fst y✝.imK +
          TrivSqZeroExt.snd x✝.imJ * TrivSqZeroExt.fst y✝.re +
        TrivSqZeroExt.snd x✝.imK * TrivSqZeroExt.fst y✝.imI)

Tactic:
ring

Goal state after:
Module: Mathlib.Algebra.DualQuaternion

Goal state before:
pp: case h2.e_imK
R : Type u_1
inst✝ : CommRing R
x✝ y✝ : ℍ[DualNumber R]
⊢ TrivSqZeroExt.fst x✝.re * TrivSqZeroExt.snd y✝.imK + TrivSqZeroExt.snd x✝.re * TrivSqZeroExt.fst y✝.imK +
          (TrivSqZeroExt.fst x✝.imI * TrivSqZeroExt.snd y✝.imJ + TrivSqZeroExt.snd x✝.imI * TrivSqZeroExt.fst y✝.imJ) -
        (TrivSqZeroExt.fst x✝.imJ * TrivSqZeroExt.snd y✝.imI + TrivSqZeroExt.snd x✝.imJ * TrivSqZeroExt.fst y✝.imI) +
      (TrivSqZeroExt.fst x✝.imK * TrivSqZeroExt.snd y✝.re + TrivSqZeroExt.snd x✝.imK * TrivSqZeroExt.fst y✝.re) =
    TrivSqZeroExt.fst x✝.re * TrivSqZeroExt.snd y✝.imK + TrivSqZeroExt.fst x✝.imI * TrivSqZeroExt.snd y✝.imJ -
          TrivSqZeroExt.fst x✝.imJ * TrivSqZeroExt.snd y✝.imI +
        TrivSqZeroExt.fst x✝.imK * TrivSqZeroExt.snd y✝.re +
      (TrivSqZeroExt.snd x✝.re * TrivSqZeroExt.fst y✝.imK + TrivSqZeroExt.snd x✝.imI * TrivSqZeroExt.fst y✝.imJ -
          TrivSqZeroExt.snd x✝.imJ * TrivSqZeroExt.fst y✝.imI +
        TrivSqZeroExt.snd x✝.imK * TrivSqZeroExt.fst y✝.re)

Tactic:
ring

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

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
w : List (α × Bool)
⊢ Red (invRev (reduce (invRev w))) (invRev (invRev (reduce w)))

Tactic:
invRev_invRev

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
w : List (α × Bool)
⊢ Red (invRev (reduce (invRev w))) (reduce w)
Module: Mathlib.GroupTheory.FreeGroup.Reduce

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
w : List (α × Bool)
this : Red (invRev (invRev w)) (invRev (reduce (invRev w)))
⊢ Red w (invRev (reduce (invRev w)))

Tactic:
invRev_invRev

Goal state after:
α : Type u_1
inst✝ : DecidableEq α
w : List (α × Bool)
this : Red w (invRev (reduce (invRev w)))
⊢ Red w (invRev (reduce (invRev w)))
Module: Mathlib.RingTheory.Polynomial.Eisenstein.Criterion

Goal state before:
pp: 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 : f.IsPrimitive
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
⊢ g = C g.leadingCoeff * q ^ m + r

Tactic:
ring

Goal state after: