-- Mathlib/RingTheory/NormTrace.lean
lemma Algebra.norm_one_add_smul {A B} [CommRing A] [CommRing B] [Algebra A B]
    [Module.Free A B] [Module.Finite A B] (a : A) (x : B) :
    ∃ r : A, Algebra.norm A (1 + a • x) = 1 + Algebra.trace A B x * a + r * a ^ 2

Proof state:
A : Type u_1
B : Type u_2
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Algebra A B
inst✝¹ : Module.Free A B
inst✝ : Module.Finite A B
a : A
x : B
ι : Type u_2 := Module.Free.ChooseBasisIndex A B
b : Basis ι A B := Module.Free.chooseBasis A B
this : Fintype ι
⊢ ∃ r, (norm A) (1 + a • x) = 1 + (trace A B) x * a + r * a ^ 2

Tactic:
clear_value ι b

Result:
A : Type u_1
B : Type u_2
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Algebra A B
inst✝¹ : Module.Free A B
inst✝ : Module.Finite A B
a : A
x : B
ι : Type u_2
this : Fintype ι
b : Basis ι A B
⊢ ∃ r, (norm A) (1 + a • x) = 1 + (trace A B) x * a + r * a ^ 2

Proof state:
A : Type u_1
B : Type u_2
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Algebra A B
inst✝¹ : Module.Free A B
inst✝ : Module.Finite A B
a : A
x : B
ι : Type u_2 := Module.Free.ChooseBasisIndex A B
⊢ ∃ r, (norm A) (1 + a • x) = 1 + (trace A B) x * a + r * a ^ 2

Tactic:
let b : Basis ι A B := Module.Free.chooseBasis _ _

Result:
A : Type u_1
B : Type u_2
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Algebra A B
inst✝¹ : Module.Free A B
inst✝ : Module.Finite A B
a : A
x : B
ι : Type u_2 := Module.Free.ChooseBasisIndex A B
b : Basis ι A B := Module.Free.chooseBasis A B
⊢ ∃ r, (norm A) (1 + a • x) = 1 + (trace A B) x * a + r * a ^ 2

Proof state:
A : Type u_1
B : Type u_2
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Algebra A B
inst✝¹ : Module.Free A B
inst✝ : Module.Finite A B
a : A
x : B
ι : Type u_2 := Module.Free.ChooseBasisIndex A B
b : Basis ι A B := Module.Free.chooseBasis A B
⊢ ∃ r, (norm A) (1 + a • x) = 1 + (trace A B) x * a + r * a ^ 2

Tactic:
haveI : Fintype ι := inferInstance

Result:
A : Type u_1
B : Type u_2
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Algebra A B
inst✝¹ : Module.Free A B
inst✝ : Module.Finite A B
a : A
x : B
ι : Type u_2 := Module.Free.ChooseBasisIndex A B
b : Basis ι A B := Module.Free.chooseBasis A B
this : Fintype ι
⊢ ∃ r, (norm A) (1 + a • x) = 1 + (trace A B) x * a + r * a ^ 2

Proof state:
A : Type u_1
B : Type u_2
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Algebra A B
inst✝¹ : Module.Free A B
inst✝ : Module.Finite A B
a : A
x : B
ι : Type u_2
this : Fintype ι
b : Basis ι A B
⊢ ∃ r, ((leftMulMatrix b) (1 + a • x)).det = 1 + ((leftMulMatrix b) x).trace * a + r * a ^ 2

Tactic:
simp only [map_add, map_one, map_smul, Matrix.det_one_add_smul a]

Result:
A : Type u_1
B : Type u_2
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Algebra A B
inst✝¹ : Module.Free A B
inst✝ : Module.Finite A B
a : A
x : B
ι : Type u_2
this : Fintype ι
b : Basis ι A B
⊢ ∃ r,
    1 + ((leftMulMatrix b) x).trace * a +
        Polynomial.eval a (1 + Polynomial.X • ((leftMulMatrix b) x).map ⇑Polynomial.C).det.divX.divX * a ^ 2 =
      1 + ((leftMulMatrix b) x).trace * a + r * a ^ 2

Proof state:
A : Type u_1
B : Type u_2
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Algebra A B
inst✝¹ : Module.Free A B
inst✝ : Module.Finite A B
a : A
x : B
⊢ ∃ r, (norm A) (1 + a • x) = 1 + (trace A B) x * a + r * a ^ 2

Tactic:
let ι := Module.Free.ChooseBasisIndex A B

Result:
A : Type u_1
B : Type u_2
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Algebra A B
inst✝¹ : Module.Free A B
inst✝ : Module.Finite A B
a : A
x : B
ι : Type u_2 := Module.Free.ChooseBasisIndex A B
⊢ ∃ r, (norm A) (1 + a • x) = 1 + (trace A B) x * a + r * a ^ 2

Proof state:
A : Type u_1
B : Type u_2
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Algebra A B
inst✝¹ : Module.Free A B
inst✝ : Module.Finite A B
a : A
x : B
ι : Type u_2
this : Fintype ι
b : Basis ι A B
⊢ ∃ r, (norm A) (1 + a • x) = 1 + (trace A B) x * a + r * a ^ 2

Tactic:
simp_rw [Algebra.norm_eq_matrix_det b, Algebra.trace_eq_matrix_trace b]

Result:
A : Type u_1
B : Type u_2
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Algebra A B
inst✝¹ : Module.Free A B
inst✝ : Module.Finite A B
a : A
x : B
ι : Type u_2
this : Fintype ι
b : Basis ι A B
⊢ ∃ r, ((leftMulMatrix b) (1 + a • x)).det = 1 + ((leftMulMatrix b) x).trace * a + r * a ^ 2

Proof state:
A : Type u_1
B : Type u_2
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Algebra A B
inst✝¹ : Module.Free A B
inst✝ : Module.Finite A B
a : A
x : B
ι : Type u_2
this : Fintype ι
b : Basis ι A B
⊢ ∃ r,
    1 + ((leftMulMatrix b) x).trace * a +
        Polynomial.eval a (1 + Polynomial.X • ((leftMulMatrix b) x).map ⇑Polynomial.C).det.divX.divX * a ^ 2 =
      1 + ((leftMulMatrix b) x).trace * a + r * a ^ 2

Tactic:
exact ⟨_, rfl⟩

Result:
no goals

Proof state:
A : Type u_1
B : Type u_2
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Algebra A B
inst✝¹ : Module.Free A B
inst✝ : Module.Finite A B
a : A
x : B
⊢ ∃ r, (norm A) (1 + a • x) = 1 + (trace A B) x * a + r * a ^ 2

Tactic:
classical
let ι := Module.Free.ChooseBasisIndex A B
let b : Basis ι A B := Module.Free.chooseBasis _ _
haveI : Fintype ι := inferInstance
clear_value ι b
simp_rw [Algebra.norm_eq_matrix_det b, Algebra.trace_eq_matrix_trace b]
simp only [map_add, map_one, map_smul, Matrix.det_one_add_smul a]
exact ⟨_, rfl⟩

Result:
no goals