[GOAL]
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
Q : QuadraticForm R M
l : List M
f : M →ₗ[R] N →ₗ[R] N
hf : ∀ (m : M) (x : N), ↑(↑f m) (↑(↑f m) x) = ↑Q m • x
n : N
⊢ ↑(↑(foldr Q f hf) n) (List.prod (List.map (↑(ι Q)) l)) = List.foldr (fun m n => ↑(↑f m) n) n l
[PROOFSTEP]
induction' l with hd tl ih
[GOAL]
case nil
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
Q : QuadraticForm R M
f : M →ₗ[R] N →ₗ[R] N
hf : ∀ (m : M) (x : N), ↑(↑f m) (↑(↑f m) x) = ↑Q m • x
n : N
⊢ ↑(↑(foldr Q f hf) n) (List.prod (List.map ↑(ι Q) [])) = List.foldr (fun m n => ↑(↑f m) n) n []
[PROOFSTEP]
rw [List.map_nil, List.prod_nil, List.foldr_nil, foldr_one]
[GOAL]
case cons
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
Q : QuadraticForm R M
f : M →ₗ[R] N →ₗ[R] N
hf : ∀ (m : M) (x : N), ↑(↑f m) (↑(↑f m) x) = ↑Q m • x
n : N
hd : M
tl : List M
ih : ↑(↑(foldr Q f hf) n) (List.prod (List.map (↑(ι Q)) tl)) = List.foldr (fun m n => ↑(↑f m) n) n tl
⊢ ↑(↑(foldr Q f hf) n) (List.prod (List.map (↑(ι Q)) (hd :: tl))) = List.foldr (fun m n => ↑(↑f m) n) n (hd :: tl)
[PROOFSTEP]
rw [List.map_cons, List.prod_cons, List.foldr_cons, foldr_mul, foldr_ι, ih]
[GOAL]
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
Q : QuadraticForm R M
f : M →ₗ[R] N →ₗ[R] N
hf : ∀ (m : M) (x : N), ↑(↑f m) (↑(↑f m) x) = ↑Q m • x
n : N
m : M
⊢ ↑(↑(foldl Q f hf) n) (↑(ι Q) m) = ↑(↑f m) n
[PROOFSTEP]
rw [← foldr_reverse, reverse_ι, foldr_ι]
[GOAL]
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
Q : QuadraticForm R M
f : M →ₗ[R] N →ₗ[R] N
hf : ∀ (m : M) (x : N), ↑(↑f m) (↑(↑f m) x) = ↑Q m • x
n : N
r : R
⊢ ↑(↑(foldl Q f hf) n) (↑(algebraMap R (CliffordAlgebra Q)) r) = r • n
[PROOFSTEP]
rw [← foldr_reverse, reverse.commutes, foldr_algebraMap]
[GOAL]
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
Q : QuadraticForm R M
f : M →ₗ[R] N →ₗ[R] N
hf : ∀ (m : M) (x : N), ↑(↑f m) (↑(↑f m) x) = ↑Q m • x
n : N
⊢ ↑(↑(foldl Q f hf) n) 1 = n
[PROOFSTEP]
rw [← foldr_reverse, reverse.map_one, foldr_one]
[GOAL]
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
Q : QuadraticForm R M
f : M →ₗ[R] N →ₗ[R] N
hf : ∀ (m : M) (x : N), ↑(↑f m) (↑(↑f m) x) = ↑Q m • x
n : N
a b : CliffordAlgebra Q
⊢ ↑(↑(foldl Q f hf) n) (a * b) = ↑(↑(foldl Q f hf) (↑(↑(foldl Q f hf) n) a)) b
[PROOFSTEP]
rw [← foldr_reverse, ← foldr_reverse, ← foldr_reverse, reverse.map_mul, foldr_mul]
[GOAL]
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
Q : QuadraticForm R M
l : List M
f : M →ₗ[R] N →ₗ[R] N
hf : ∀ (m : M) (x : N), ↑(↑f m) (↑(↑f m) x) = ↑Q m • x
n : N
⊢ ↑(↑(foldl Q f hf) n) (List.prod (List.map (↑(ι Q)) l)) = List.foldl (fun m n => ↑(↑f n) m) n l
[PROOFSTEP]
rw [← foldr_reverse, reverse_prod_map_ι, ← List.map_reverse, foldr_prod_map_ι, List.foldr_reverse]
[GOAL]
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
Q : QuadraticForm R M
P : CliffordAlgebra Q → Prop
hr : ∀ (r : R), P (↑(algebraMap R (CliffordAlgebra Q)) r)
h_add : ∀ (x y : CliffordAlgebra Q), P x → P y → P (x + y)
h_ι_mul : ∀ (m : M) (x : CliffordAlgebra Q), P x → P (x * ↑(ι Q) m)
⊢ ∀ (x : CliffordAlgebra Q), P x
[PROOFSTEP]
intro x
[GOAL]
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
Q : QuadraticForm R M
P : CliffordAlgebra Q → Prop
hr : ∀ (r : R), P (↑(algebraMap R (CliffordAlgebra Q)) r)
h_add : ∀ (x y : CliffordAlgebra Q), P x → P y → P (x + y)
h_ι_mul : ∀ (m : M) (x : CliffordAlgebra Q), P x → P (x * ↑(ι Q) m)
x : CliffordAlgebra Q
⊢ P x
[PROOFSTEP]
have : x ∈ ⊤ := Submodule.mem_top (R := R)
[GOAL]
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
Q : QuadraticForm R M
P : CliffordAlgebra Q → Prop
hr : ∀ (r : R), P (↑(algebraMap R (CliffordAlgebra Q)) r)
h_add : ∀ (x y : CliffordAlgebra Q), P x → P y → P (x + y)
h_ι_mul : ∀ (m : M) (x : CliffordAlgebra Q), P x → P (x * ↑(ι Q) m)
x : CliffordAlgebra Q
this : x ∈ ⊤
⊢ P x
[PROOFSTEP]
rw [← iSup_ι_range_eq_top] at this
[GOAL]
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
Q : QuadraticForm R M
P : CliffordAlgebra Q → Prop
hr : ∀ (r : R), P (↑(algebraMap R (CliffordAlgebra Q)) r)
h_add : ∀ (x y : CliffordAlgebra Q), P x → P y → P (x + y)
h_ι_mul : ∀ (m : M) (x : CliffordAlgebra Q), P x → P (x * ↑(ι Q) m)
x : CliffordAlgebra Q
this : x ∈ ⨆ (i : ℕ), LinearMap.range (ι Q) ^ i
⊢ P x
[PROOFSTEP]
induction this using Submodule.iSup_induction' with
  -- _ this (fun i x hx => ?_) _ h_add
| hp i x hx =>
  induction hx using Submodule.pow_induction_on_right' with
  | hr r => exact hr r
  | hadd _x _y _i _ _ ihx ihy => exact h_add _ _ ihx ihy
  | hmul _i x _hx px m hm =>
    obtain ⟨m, rfl⟩ := hm
    exact h_ι_mul _ _ px
| h0 => simpa only [map_zero] using hr 0
| hadd _x _y _ _ ihx ihy => exact h_add _ _ ihx ihy
[GOAL]
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
Q : QuadraticForm R M
P : CliffordAlgebra Q → Prop
hr : ∀ (r : R), P (↑(algebraMap R (CliffordAlgebra Q)) r)
h_add : ∀ (x y : CliffordAlgebra Q), P x → P y → P (x + y)
h_ι_mul : ∀ (m : M) (x : CliffordAlgebra Q), P x → P (x * ↑(ι Q) m)
x : CliffordAlgebra Q
this : x ∈ ⨆ (i : ℕ), LinearMap.range (ι Q) ^ i
⊢ P x
[PROOFSTEP]
induction this using Submodule.iSup_induction' with
  -- _ this (fun i x hx => ?_) _ h_add
| hp i x hx =>
  induction hx using Submodule.pow_induction_on_right' with
  | hr r => exact hr r
  | hadd _x _y _i _ _ ihx ihy => exact h_add _ _ ihx ihy
  | hmul _i x _hx px m hm =>
    obtain ⟨m, rfl⟩ := hm
    exact h_ι_mul _ _ px
| h0 => simpa only [map_zero] using hr 0
| hadd _x _y _ _ ihx ihy => exact h_add _ _ ihx ihy
[GOAL]
case hp
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
Q : QuadraticForm R M
P : CliffordAlgebra Q → Prop
hr : ∀ (r : R), P (↑(algebraMap R (CliffordAlgebra Q)) r)
h_add : ∀ (x y : CliffordAlgebra Q), P x → P y → P (x + y)
h_ι_mul : ∀ (m : M) (x : CliffordAlgebra Q), P x → P (x * ↑(ι Q) m)
x✝ : CliffordAlgebra Q
i : ℕ
x : CliffordAlgebra Q
hx : x ∈ LinearMap.range (ι Q) ^ i
⊢ P x
[PROOFSTEP]

| hp i x hx =>
  induction hx using Submodule.pow_induction_on_right' with
  | hr r => exact hr r
  | hadd _x _y _i _ _ ihx ihy => exact h_add _ _ ihx ihy
  | hmul _i x _hx px m hm =>
    obtain ⟨m, rfl⟩ := hm
    exact h_ι_mul _ _ px
[GOAL]
case hp
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
Q : QuadraticForm R M
P : CliffordAlgebra Q → Prop
hr : ∀ (r : R), P (↑(algebraMap R (CliffordAlgebra Q)) r)
h_add : ∀ (x y : CliffordAlgebra Q), P x → P y → P (x + y)
h_ι_mul : ∀ (m : M) (x : CliffordAlgebra Q), P x → P (x * ↑(ι Q) m)
x✝ : CliffordAlgebra Q
i : ℕ
x : CliffordAlgebra Q
hx : x ∈ LinearMap.range (ι Q) ^ i
⊢ P x
[PROOFSTEP]
induction hx using Submodule.pow_induction_on_right' with
| hr r => exact hr r
| hadd _x _y _i _ _ ihx ihy => exact h_add _ _ ihx ihy
| hmul _i x _hx px m hm =>
  obtain ⟨m, rfl⟩ := hm
  exact h_ι_mul _ _ px
[GOAL]
case hp
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
Q : QuadraticForm R M
P : CliffordAlgebra Q → Prop
hr : ∀ (r : R), P (↑(algebraMap R (CliffordAlgebra Q)) r)
h_add : ∀ (x y : CliffordAlgebra Q), P x → P y → P (x + y)
h_ι_mul : ∀ (m : M) (x : CliffordAlgebra Q), P x → P (x * ↑(ι Q) m)
x✝ : CliffordAlgebra Q
i : ℕ
x : CliffordAlgebra Q
hx : x ∈ LinearMap.range (ι Q) ^ i
⊢ P x
[PROOFSTEP]
induction hx using Submodule.pow_induction_on_right' with
| hr r => exact hr r
| hadd _x _y _i _ _ ihx ihy => exact h_add _ _ ihx ihy
| hmul _i x _hx px m hm =>
  obtain ⟨m, rfl⟩ := hm
  exact h_ι_mul _ _ px
[GOAL]
case hp.hr
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
Q : QuadraticForm R M
P : CliffordAlgebra Q → Prop
hr : ∀ (r : R), P (↑(algebraMap R (CliffordAlgebra Q)) r)
h_add : ∀ (x y : CliffordAlgebra Q), P x → P y → P (x + y)
h_ι_mul : ∀ (m : M) (x : CliffordAlgebra Q), P x → P (x * ↑(ι Q) m)
x✝ : CliffordAlgebra Q
i : ℕ
x : CliffordAlgebra Q
r : R
⊢ P (↑(algebraMap R (CliffordAlgebra Q)) r)
[PROOFSTEP]

| hr r => exact hr r
[GOAL]
case hp.hr
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
Q : QuadraticForm R M
P : CliffordAlgebra Q → Prop
hr : ∀ (r : R), P (↑(algebraMap R (CliffordAlgebra Q)) r)
h_add : ∀ (x y : CliffordAlgebra Q), P x → P y → P (x + y)
h_ι_mul : ∀ (m : M) (x : CliffordAlgebra Q), P x → P (x * ↑(ι Q) m)
x✝ : CliffordAlgebra Q
i : ℕ
x : CliffordAlgebra Q
r : R
⊢ P (↑(algebraMap R (CliffordAlgebra Q)) r)
[PROOFSTEP]
exact hr r
[GOAL]
case hp.hadd
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
Q : QuadraticForm R M
P : CliffordAlgebra Q → Prop
hr : ∀ (r : R), P (↑(algebraMap R (CliffordAlgebra Q)) r)
h_add : ∀ (x y : CliffordAlgebra Q), P x → P y → P (x + y)
h_ι_mul : ∀ (m : M) (x : CliffordAlgebra Q), P x → P (x * ↑(ι Q) m)
x✝ : CliffordAlgebra Q
i : ℕ
x _x _y : CliffordAlgebra Q
_i : ℕ
hx✝ : _x ∈ LinearMap.range (ι Q) ^ _i
hy✝ : _y ∈ LinearMap.range (ι Q) ^ _i
ihx : P _x
ihy : P _y
⊢ P (_x + _y)
[PROOFSTEP]

| hadd _x _y _i _ _ ihx ihy => exact h_add _ _ ihx ihy
[GOAL]
case hp.hadd
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
Q : QuadraticForm R M
P : CliffordAlgebra Q → Prop
hr : ∀ (r : R), P (↑(algebraMap R (CliffordAlgebra Q)) r)
h_add : ∀ (x y : CliffordAlgebra Q), P x → P y → P (x + y)
h_ι_mul : ∀ (m : M) (x : CliffordAlgebra Q), P x → P (x * ↑(ι Q) m)
x✝ : CliffordAlgebra Q
i : ℕ
x _x _y : CliffordAlgebra Q
_i : ℕ
hx✝ : _x ∈ LinearMap.range (ι Q) ^ _i
hy✝ : _y ∈ LinearMap.range (ι Q) ^ _i
ihx : P _x
ihy : P _y
⊢ P (_x + _y)
[PROOFSTEP]
exact h_add _ _ ihx ihy
[GOAL]
case hp.hmul
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
Q : QuadraticForm R M
P : CliffordAlgebra Q → Prop
hr : ∀ (r : R), P (↑(algebraMap R (CliffordAlgebra Q)) r)
h_add : ∀ (x y : CliffordAlgebra Q), P x → P y → P (x + y)
h_ι_mul : ∀ (m : M) (x : CliffordAlgebra Q), P x → P (x * ↑(ι Q) m)
x✝¹ : CliffordAlgebra Q
i : ℕ
x✝ : CliffordAlgebra Q
_i : ℕ
x : CliffordAlgebra Q
_hx : x ∈ LinearMap.range (ι Q) ^ _i
px : P x
m : CliffordAlgebra Q
hm : m ∈ LinearMap.range (ι Q)
⊢ P (x * m)
[PROOFSTEP]

| hmul _i x _hx px m hm =>
  obtain ⟨m, rfl⟩ := hm
  exact h_ι_mul _ _ px
[GOAL]
case hp.hmul
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
Q : QuadraticForm R M
P : CliffordAlgebra Q → Prop
hr : ∀ (r : R), P (↑(algebraMap R (CliffordAlgebra Q)) r)
h_add : ∀ (x y : CliffordAlgebra Q), P x → P y → P (x + y)
h_ι_mul : ∀ (m : M) (x : CliffordAlgebra Q), P x → P (x * ↑(ι Q) m)
x✝¹ : CliffordAlgebra Q
i : ℕ
x✝ : CliffordAlgebra Q
_i : ℕ
x : CliffordAlgebra Q
_hx : x ∈ LinearMap.range (ι Q) ^ _i
px : P x
m : CliffordAlgebra Q
hm : m ∈ LinearMap.range (ι Q)
⊢ P (x * m)
[PROOFSTEP]
obtain ⟨m, rfl⟩ := hm
[GOAL]
case hp.hmul.intro
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
Q : QuadraticForm R M
P : CliffordAlgebra Q → Prop
hr : ∀ (r : R), P (↑(algebraMap R (CliffordAlgebra Q)) r)
h_add : ∀ (x y : CliffordAlgebra Q), P x → P y → P (x + y)
h_ι_mul : ∀ (m : M) (x : CliffordAlgebra Q), P x → P (x * ↑(ι Q) m)
x✝¹ : CliffordAlgebra Q
i : ℕ
x✝ : CliffordAlgebra Q
_i : ℕ
x : CliffordAlgebra Q
_hx : x ∈ LinearMap.range (ι Q) ^ _i
px : P x
m : M
⊢ P (x * ↑(ι Q) m)
[PROOFSTEP]
exact h_ι_mul _ _ px
[GOAL]
case h0
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
Q : QuadraticForm R M
P : CliffordAlgebra Q → Prop
hr : ∀ (r : R), P (↑(algebraMap R (CliffordAlgebra Q)) r)
h_add : ∀ (x y : CliffordAlgebra Q), P x → P y → P (x + y)
h_ι_mul : ∀ (m : M) (x : CliffordAlgebra Q), P x → P (x * ↑(ι Q) m)
x : CliffordAlgebra Q
⊢ P 0
[PROOFSTEP]

| h0 => simpa only [map_zero] using hr 0
[GOAL]
case h0
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
Q : QuadraticForm R M
P : CliffordAlgebra Q → Prop
hr : ∀ (r : R), P (↑(algebraMap R (CliffordAlgebra Q)) r)
h_add : ∀ (x y : CliffordAlgebra Q), P x → P y → P (x + y)
h_ι_mul : ∀ (m : M) (x : CliffordAlgebra Q), P x → P (x * ↑(ι Q) m)
x : CliffordAlgebra Q
⊢ P 0
[PROOFSTEP]
simpa only [map_zero] using hr 0
[GOAL]
case hadd
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
Q : QuadraticForm R M
P : CliffordAlgebra Q → Prop
hr : ∀ (r : R), P (↑(algebraMap R (CliffordAlgebra Q)) r)
h_add : ∀ (x y : CliffordAlgebra Q), P x → P y → P (x + y)
h_ι_mul : ∀ (m : M) (x : CliffordAlgebra Q), P x → P (x * ↑(ι Q) m)
x _x _y : CliffordAlgebra Q
hx✝ : _x ∈ ⨆ (i : ℕ), LinearMap.range (ι Q) ^ i
hy✝ : _y ∈ ⨆ (i : ℕ), LinearMap.range (ι Q) ^ i
ihx : P _x
ihy : P _y
⊢ P (_x + _y)
[PROOFSTEP]

| hadd _x _y _ _ ihx ihy => exact h_add _ _ ihx ihy
[GOAL]
case hadd
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
Q : QuadraticForm R M
P : CliffordAlgebra Q → Prop
hr : ∀ (r : R), P (↑(algebraMap R (CliffordAlgebra Q)) r)
h_add : ∀ (x y : CliffordAlgebra Q), P x → P y → P (x + y)
h_ι_mul : ∀ (m : M) (x : CliffordAlgebra Q), P x → P (x * ↑(ι Q) m)
x _x _y : CliffordAlgebra Q
hx✝ : _x ∈ ⨆ (i : ℕ), LinearMap.range (ι Q) ^ i
hy✝ : _y ∈ ⨆ (i : ℕ), LinearMap.range (ι Q) ^ i
ihx : P _x
ihy : P _y
⊢ P (_x + _y)
[PROOFSTEP]
exact h_add _ _ ihx ihy
[GOAL]
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
Q : QuadraticForm R M
P : CliffordAlgebra Q → Prop
hr : ∀ (r : R), P (↑(algebraMap R (CliffordAlgebra Q)) r)
h_add : ∀ (x y : CliffordAlgebra Q), P x → P y → P (x + y)
h_mul_ι : ∀ (x : CliffordAlgebra Q) (m : M), P x → P (↑(ι Q) m * x)
⊢ ∀ (x : CliffordAlgebra Q), P x
[PROOFSTEP]
refine' reverse_involutive.surjective.forall.2 _
[GOAL]
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
Q : QuadraticForm R M
P : CliffordAlgebra Q → Prop
hr : ∀ (r : R), P (↑(algebraMap R (CliffordAlgebra Q)) r)
h_add : ∀ (x y : CliffordAlgebra Q), P x → P y → P (x + y)
h_mul_ι : ∀ (x : CliffordAlgebra Q) (m : M), P x → P (↑(ι Q) m * x)
⊢ ∀ (x : CliffordAlgebra Q), P (↑reverse x)
[PROOFSTEP]
intro x
[GOAL]
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
Q : QuadraticForm R M
P : CliffordAlgebra Q → Prop
hr : ∀ (r : R), P (↑(algebraMap R (CliffordAlgebra Q)) r)
h_add : ∀ (x y : CliffordAlgebra Q), P x → P y → P (x + y)
h_mul_ι : ∀ (x : CliffordAlgebra Q) (m : M), P x → P (↑(ι Q) m * x)
x : CliffordAlgebra Q
⊢ P (↑reverse x)
[PROOFSTEP]
induction' x using CliffordAlgebra.right_induction with r x y hx hy m x hx
[GOAL]
case hr
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
Q : QuadraticForm R M
P : CliffordAlgebra Q → Prop
hr : ∀ (r : R), P (↑(algebraMap R (CliffordAlgebra Q)) r)
h_add : ∀ (x y : CliffordAlgebra Q), P x → P y → P (x + y)
h_mul_ι : ∀ (x : CliffordAlgebra Q) (m : M), P x → P (↑(ι Q) m * x)
r : R
⊢ P (↑reverse (↑(algebraMap R (CliffordAlgebra Q)) r))
[PROOFSTEP]
simpa only [reverse.commutes] using hr r
[GOAL]
case h_add
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
Q : QuadraticForm R M
P : CliffordAlgebra Q → Prop
hr : ∀ (r : R), P (↑(algebraMap R (CliffordAlgebra Q)) r)
h_add : ∀ (x y : CliffordAlgebra Q), P x → P y → P (x + y)
h_mul_ι : ∀ (x : CliffordAlgebra Q) (m : M), P x → P (↑(ι Q) m * x)
x y : CliffordAlgebra Q
hx : P (↑reverse x)
hy : P (↑reverse y)
⊢ P (↑reverse (x + y))
[PROOFSTEP]
simpa only [map_add] using h_add _ _ hx hy
[GOAL]
case h_ι_mul
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
Q : QuadraticForm R M
P : CliffordAlgebra Q → Prop
hr : ∀ (r : R), P (↑(algebraMap R (CliffordAlgebra Q)) r)
h_add : ∀ (x y : CliffordAlgebra Q), P x → P y → P (x + y)
h_mul_ι : ∀ (x : CliffordAlgebra Q) (m : M), P x → P (↑(ι Q) m * x)
m : M
x : CliffordAlgebra Q
hx : P (↑reverse x)
⊢ P (↑reverse (x * ↑(ι Q) m))
[PROOFSTEP]
simpa only [reverse.map_mul, reverse_ι] using h_mul_ι _ _ hx
[GOAL]
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
Q : QuadraticForm R M
f : M →ₗ[R] CliffordAlgebra Q × N →ₗ[R] N
⊢ M →ₗ[R] Module.End R (CliffordAlgebra Q × N)
[PROOFSTEP]
have v_mul := (Algebra.lmul R (CliffordAlgebra Q)).toLinearMap ∘ₗ ι Q
[GOAL]
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
Q : QuadraticForm R M
f : M →ₗ[R] CliffordAlgebra Q × N →ₗ[R] N
v_mul : M →ₗ[R] Module.End R (CliffordAlgebra Q)
⊢ M →ₗ[R] Module.End R (CliffordAlgebra Q × N)
[PROOFSTEP]
have l := v_mul.compl₂ (LinearMap.fst _ _ N)
[GOAL]
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
Q : QuadraticForm R M
f : M →ₗ[R] CliffordAlgebra Q × N →ₗ[R] N
v_mul : M →ₗ[R] Module.End R (CliffordAlgebra Q)
l : M →ₗ[R] CliffordAlgebra Q × N →ₗ[R] CliffordAlgebra Q
⊢ M →ₗ[R] Module.End R (CliffordAlgebra Q × N)
[PROOFSTEP]
exact
  { toFun := fun m => (l m).prod (f m)
    map_add' := fun v₂ v₂ =>
      LinearMap.ext fun x => Prod.ext (LinearMap.congr_fun (l.map_add _ _) x) (LinearMap.congr_fun (f.map_add _ _) x)
    map_smul' := fun c v =>
      LinearMap.ext fun x =>
        Prod.ext (LinearMap.congr_fun (l.map_smul _ _) x) (LinearMap.congr_fun (f.map_smul _ _) x) }
[GOAL]
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
Q : QuadraticForm R M
f : M →ₗ[R] CliffordAlgebra Q × N →ₗ[R] N
hf : ∀ (m : M) (x : CliffordAlgebra Q) (fx : N), ↑(↑f m) (↑(ι Q) m * x, ↑(↑f m) (x, fx)) = ↑Q m • fx
v : M
x_fx : CliffordAlgebra Q × N
⊢ ↑(↑(foldr'Aux Q f) v) (↑(↑(foldr'Aux Q f) v) x_fx) = ↑Q v • x_fx
[PROOFSTEP]
cases' x_fx with x fx
[GOAL]
case mk
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
Q : QuadraticForm R M
f : M →ₗ[R] CliffordAlgebra Q × N →ₗ[R] N
hf : ∀ (m : M) (x : CliffordAlgebra Q) (fx : N), ↑(↑f m) (↑(ι Q) m * x, ↑(↑f m) (x, fx)) = ↑Q m • fx
v : M
x : CliffordAlgebra Q
fx : N
⊢ ↑(↑(foldr'Aux Q f) v) (↑(↑(foldr'Aux Q f) v) (x, fx)) = ↑Q v • (x, fx)
[PROOFSTEP]
simp only [foldr'Aux_apply_apply]
[GOAL]
case mk
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
Q : QuadraticForm R M
f : M →ₗ[R] CliffordAlgebra Q × N →ₗ[R] N
hf : ∀ (m : M) (x : CliffordAlgebra Q) (fx : N), ↑(↑f m) (↑(ι Q) m * x, ↑(↑f m) (x, fx)) = ↑Q m • fx
v : M
x : CliffordAlgebra Q
fx : N
⊢ (↑(ι Q) v * (↑(ι Q) v * x), ↑(↑f v) (↑(ι Q) v * x, ↑(↑f v) (x, fx))) = ↑Q v • (x, fx)
[PROOFSTEP]
rw [← mul_assoc, ι_sq_scalar, ← Algebra.smul_def, hf, Prod.smul_mk]
[GOAL]
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
Q : QuadraticForm R M
f : M →ₗ[R] CliffordAlgebra Q × N →ₗ[R] N
hf : ∀ (m : M) (x : CliffordAlgebra Q) (fx : N), ↑(↑f m) (↑(ι Q) m * x, ↑(↑f m) (x, fx)) = ↑Q m • fx
n : N
m : M
x : CliffordAlgebra Q
⊢ ↑(foldr' Q f hf n) (↑(ι Q) m * x) = ↑(↑f m) (x, ↑(foldr' Q f hf n) x)
[PROOFSTEP]
dsimp [foldr']
[GOAL]
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
Q : QuadraticForm R M
f : M →ₗ[R] CliffordAlgebra Q × N →ₗ[R] N
hf : ∀ (m : M) (x : CliffordAlgebra Q) (fx : N), ↑(↑f m) (↑(ι Q) m * x, ↑(↑f m) (x, fx)) = ↑Q m • fx
n : N
m : M
x : CliffordAlgebra Q
⊢ (↑(↑(foldr Q (foldr'Aux Q f)
                (_ :
                  ∀ (v : M) (x_fx : CliffordAlgebra Q × N),
                    ↑(↑(foldr'Aux Q f) v) (↑(↑(foldr'Aux Q f) v) x_fx) = ↑Q v • x_fx))
            (1, n))
        (↑(ι Q) m * x)).snd =
    ↑(↑f m)
      (x,
        (↑(↑(foldr Q (foldr'Aux Q f)
                    (_ :
                      ∀ (v : M) (x_fx : CliffordAlgebra Q × N),
                        ↑(↑(foldr'Aux Q f) v) (↑(↑(foldr'Aux Q f) v) x_fx) = ↑Q v • x_fx))
                (1, n))
            x).snd)
[PROOFSTEP]
rw [foldr_mul, foldr_ι, foldr'Aux_apply_apply]
[GOAL]
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
Q : QuadraticForm R M
f : M →ₗ[R] CliffordAlgebra Q × N →ₗ[R] N
hf : ∀ (m : M) (x : CliffordAlgebra Q) (fx : N), ↑(↑f m) (↑(ι Q) m * x, ↑(↑f m) (x, fx)) = ↑Q m • fx
n : N
m : M
x : CliffordAlgebra Q
⊢ (↑(ι Q) m *
          (↑(↑(foldr Q (foldr'Aux Q f)
                      (_ :
                        ∀ (v : M) (x_fx : CliffordAlgebra Q × N),
                          ↑(↑(foldr'Aux Q f) v) (↑(↑(foldr'Aux Q f) v) x_fx) = ↑Q v • x_fx))
                  (1, n))
              x).fst,
        ↑(↑f m)
          (↑(↑(foldr Q (foldr'Aux Q f)
                    (_ :
                      ∀ (v : M) (x_fx : CliffordAlgebra Q × N),
                        ↑(↑(foldr'Aux Q f) v) (↑(↑(foldr'Aux Q f) v) x_fx) = ↑Q v • x_fx))
                (1, n))
            x)).snd =
    ↑(↑f m)
      (x,
        (↑(↑(foldr Q (foldr'Aux Q f)
                    (_ :
                      ∀ (v : M) (x_fx : CliffordAlgebra Q × N),
                        ↑(↑(foldr'Aux Q f) v) (↑(↑(foldr'Aux Q f) v) x_fx) = ↑Q v • x_fx))
                (1, n))
            x).snd)
[PROOFSTEP]
refine' congr_arg (f m) (Prod.mk.eta.symm.trans _)
[GOAL]
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
Q : QuadraticForm R M
f : M →ₗ[R] CliffordAlgebra Q × N →ₗ[R] N
hf : ∀ (m : M) (x : CliffordAlgebra Q) (fx : N), ↑(↑f m) (↑(ι Q) m * x, ↑(↑f m) (x, fx)) = ↑Q m • fx
n : N
m : M
x : CliffordAlgebra Q
⊢ ((↑(↑(foldr Q (foldr'Aux Q f)
                  (_ :
                    ∀ (v : M) (x_fx : CliffordAlgebra Q × N),
                      ↑(↑(foldr'Aux Q f) v) (↑(↑(foldr'Aux Q f) v) x_fx) = ↑Q v • x_fx))
              (1, n))
          x).fst,
      (↑(↑(foldr Q (foldr'Aux Q f)
                  (_ :
                    ∀ (v : M) (x_fx : CliffordAlgebra Q × N),
                      ↑(↑(foldr'Aux Q f) v) (↑(↑(foldr'Aux Q f) v) x_fx) = ↑Q v • x_fx))
              (1, n))
          x).snd) =
    (x,
      (↑(↑(foldr Q (foldr'Aux Q f)
                  (_ :
                    ∀ (v : M) (x_fx : CliffordAlgebra Q × N),
                      ↑(↑(foldr'Aux Q f) v) (↑(↑(foldr'Aux Q f) v) x_fx) = ↑Q v • x_fx))
              (1, n))
          x).snd)
[PROOFSTEP]
congr 1
[GOAL]
case e_fst
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
Q : QuadraticForm R M
f : M →ₗ[R] CliffordAlgebra Q × N →ₗ[R] N
hf : ∀ (m : M) (x : CliffordAlgebra Q) (fx : N), ↑(↑f m) (↑(ι Q) m * x, ↑(↑f m) (x, fx)) = ↑Q m • fx
n : N
m : M
x : CliffordAlgebra Q
⊢ (↑(↑(foldr Q (foldr'Aux Q f)
                (_ :
                  ∀ (v : M) (x_fx : CliffordAlgebra Q × N),
                    ↑(↑(foldr'Aux Q f) v) (↑(↑(foldr'Aux Q f) v) x_fx) = ↑Q v • x_fx))
            (1, n))
        x).fst =
    x
[PROOFSTEP]
induction' x using CliffordAlgebra.left_induction with r x y hx hy m x hx
[GOAL]
case e_fst.hr
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
Q : QuadraticForm R M
f : M →ₗ[R] CliffordAlgebra Q × N →ₗ[R] N
hf : ∀ (m : M) (x : CliffordAlgebra Q) (fx : N), ↑(↑f m) (↑(ι Q) m * x, ↑(↑f m) (x, fx)) = ↑Q m • fx
n : N
m : M
r : R
⊢ (↑(↑(foldr Q (foldr'Aux Q f)
                (_ :
                  ∀ (v : M) (x_fx : CliffordAlgebra Q × N),
                    ↑(↑(foldr'Aux Q f) v) (↑(↑(foldr'Aux Q f) v) x_fx) = ↑Q v • x_fx))
            (1, n))
        (↑(algebraMap R (CliffordAlgebra Q)) r)).fst =
    ↑(algebraMap R (CliffordAlgebra Q)) r
[PROOFSTEP]
simp_rw [foldr_algebraMap, Prod.smul_mk, Algebra.algebraMap_eq_smul_one]
[GOAL]
case e_fst.h_add
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
Q : QuadraticForm R M
f : M →ₗ[R] CliffordAlgebra Q × N →ₗ[R] N
hf : ∀ (m : M) (x : CliffordAlgebra Q) (fx : N), ↑(↑f m) (↑(ι Q) m * x, ↑(↑f m) (x, fx)) = ↑Q m • fx
n : N
m : M
x y : CliffordAlgebra Q
hx :
  (↑(↑(foldr Q (foldr'Aux Q f)
                (_ :
                  ∀ (v : M) (x_fx : CliffordAlgebra Q × N),
                    ↑(↑(foldr'Aux Q f) v) (↑(↑(foldr'Aux Q f) v) x_fx) = ↑Q v • x_fx))
            (1, n))
        x).fst =
    x
hy :
  (↑(↑(foldr Q (foldr'Aux Q f)
                (_ :
                  ∀ (v : M) (x_fx : CliffordAlgebra Q × N),
                    ↑(↑(foldr'Aux Q f) v) (↑(↑(foldr'Aux Q f) v) x_fx) = ↑Q v • x_fx))
            (1, n))
        y).fst =
    y
⊢ (↑(↑(foldr Q (foldr'Aux Q f)
                (_ :
                  ∀ (v : M) (x_fx : CliffordAlgebra Q × N),
                    ↑(↑(foldr'Aux Q f) v) (↑(↑(foldr'Aux Q f) v) x_fx) = ↑Q v • x_fx))
            (1, n))
        (x + y)).fst =
    x + y
[PROOFSTEP]
rw [map_add, Prod.fst_add, hx, hy]
[GOAL]
case e_fst.h_mul_ι
R : Type u_1
M : Type u_2
N : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
Q : QuadraticForm R M
f : M →ₗ[R] CliffordAlgebra Q × N →ₗ[R] N
hf : ∀ (m : M) (x : CliffordAlgebra Q) (fx : N), ↑(↑f m) (↑(ι Q) m * x, ↑(↑f m) (x, fx)) = ↑Q m • fx
n : N
m✝ : M
m : CliffordAlgebra Q
x : M
hx :
  (↑(↑(foldr Q (foldr'Aux Q f)
                (_ :
                  ∀ (v : M) (x_fx : CliffordAlgebra Q × N),
                    ↑(↑(foldr'Aux Q f) v) (↑(↑(foldr'Aux Q f) v) x_fx) = ↑Q v • x_fx))
            (1, n))
        m).fst =
    m
⊢ (↑(↑(foldr Q (foldr'Aux Q f)
                (_ :
                  ∀ (v : M) (x_fx : CliffordAlgebra Q × N),
                    ↑(↑(foldr'Aux Q f) v) (↑(↑(foldr'Aux Q f) v) x_fx) = ↑Q v • x_fx))
            (1, n))
        (↑(ι Q) x * m)).fst =
    ↑(ι Q) x * m
[PROOFSTEP]
rw [foldr_mul, foldr_ι, foldr'Aux_apply_apply, hx]


[GOAL]
k : Type u_1
E : Type u_2
PE : Type u_3
inst✝³ : OrderedRing k
inst✝² : OrderedAddCommGroup E
inst✝¹ : Module k E
inst✝ : OrderedSMul k E
a a' b b' : E
r r' : k
ha : a ≤ a'
hr : r ≤ 1
⊢ ↑(lineMap a b) r ≤ ↑(lineMap a' b) r
[PROOFSTEP]
simp only [lineMap_apply_module]
[GOAL]
k : Type u_1
E : Type u_2
PE : Type u_3
inst✝³ : OrderedRing k
inst✝² : OrderedAddCommGroup E
inst✝¹ : Module k E
inst✝ : OrderedSMul k E
a a' b b' : E
r r' : k
ha : a ≤ a'
hr : r ≤ 1
⊢ (1 - r) • a + r • b ≤ (1 - r) • a' + r • b
[PROOFSTEP]
exact add_le_add_right (smul_le_smul_of_nonneg ha (sub_nonneg.2 hr)) _
[GOAL]
k : Type u_1
E : Type u_2
PE : Type u_3
inst✝³ : OrderedRing k
inst✝² : OrderedAddCommGroup E
inst✝¹ : Module k E
inst✝ : OrderedSMul k E
a a' b b' : E
r r' : k
ha : a < a'
hr : r < 1
⊢ ↑(lineMap a b) r < ↑(lineMap a' b) r
[PROOFSTEP]
simp only [lineMap_apply_module]
[GOAL]
k : Type u_1
E : Type u_2
PE : Type u_3
inst✝³ : OrderedRing k
inst✝² : OrderedAddCommGroup E
inst✝¹ : Module k E
inst✝ : OrderedSMul k E
a a' b b' : E
r r' : k
ha : a < a'
hr : r < 1
⊢ (1 - r) • a + r • b < (1 - r) • a' + r • b
[PROOFSTEP]
exact add_lt_add_right (smul_lt_smul_of_pos ha (sub_pos.2 hr)) _
[GOAL]
k : Type u_1
E : Type u_2
PE : Type u_3
inst✝³ : OrderedRing k
inst✝² : OrderedAddCommGroup E
inst✝¹ : Module k E
inst✝ : OrderedSMul k E
a a' b b' : E
r r' : k
hb : b ≤ b'
hr : 0 ≤ r
⊢ ↑(lineMap a b) r ≤ ↑(lineMap a b') r
[PROOFSTEP]
simp only [lineMap_apply_module]
[GOAL]
k : Type u_1
E : Type u_2
PE : Type u_3
inst✝³ : OrderedRing k
inst✝² : OrderedAddCommGroup E
inst✝¹ : Module k E
inst✝ : OrderedSMul k E
a a' b b' : E
r r' : k
hb : b ≤ b'
hr : 0 ≤ r
⊢ (1 - r) • a + r • b ≤ (1 - r) • a + r • b'
[PROOFSTEP]
exact add_le_add_left (smul_le_smul_of_nonneg hb hr) _
[GOAL]
k : Type u_1
E : Type u_2
PE : Type u_3
inst✝³ : OrderedRing k
inst✝² : OrderedAddCommGroup E
inst✝¹ : Module k E
inst✝ : OrderedSMul k E
a a' b b' : E
r r' : k
hb : b < b'
hr : 0 < r
⊢ ↑(lineMap a b) r < ↑(lineMap a b') r
[PROOFSTEP]
simp only [lineMap_apply_module]
[GOAL]
k : Type u_1
E : Type u_2
PE : Type u_3
inst✝³ : OrderedRing k
inst✝² : OrderedAddCommGroup E
inst✝¹ : Module k E
inst✝ : OrderedSMul k E
a a' b b' : E
r r' : k
hb : b < b'
hr : 0 < r
⊢ (1 - r) • a + r • b < (1 - r) • a + r • b'
[PROOFSTEP]
exact add_lt_add_left (smul_lt_smul_of_pos hb hr) _
[GOAL]
k : Type u_1
E : Type u_2
PE : Type u_3
inst✝³ : OrderedRing k
inst✝² : OrderedAddCommGroup E
inst✝¹ : Module k E
inst✝ : OrderedSMul k E
a a' b b' : E
r r' : k
ha : a < a'
hb : b < b'
h₀ : 0 ≤ r
h₁ : r ≤ 1
⊢ ↑(lineMap a b) r < ↑(lineMap a' b') r
[PROOFSTEP]
rcases h₀.eq_or_lt with (rfl | h₀)
[GOAL]
case inl
k : Type u_1
E : Type u_2
PE : Type u_3
inst✝³ : OrderedRing k
inst✝² : OrderedAddCommGroup E
inst✝¹ : Module k E
inst✝ : OrderedSMul k E
a a' b b' : E
r' : k
ha : a < a'
hb : b < b'
h₀ : 0 ≤ 0
h₁ : 0 ≤ 1
⊢ ↑(lineMap a b) 0 < ↑(lineMap a' b') 0
[PROOFSTEP]
simpa
[GOAL]
case inr
k : Type u_1
E : Type u_2
PE : Type u_3
inst✝³ : OrderedRing k
inst✝² : OrderedAddCommGroup E
inst✝¹ : Module k E
inst✝ : OrderedSMul k E
a a' b b' : E
r r' : k
ha : a < a'
hb : b < b'
h₀✝ : 0 ≤ r
h₁ : r ≤ 1
h₀ : 0 < r
⊢ ↑(lineMap a b) r < ↑(lineMap a' b') r
[PROOFSTEP]
exact (lineMap_mono_left ha.le h₁).trans_lt (lineMap_strict_mono_right hb h₀)
[GOAL]
k : Type u_1
E : Type u_2
PE : Type u_3
inst✝³ : OrderedRing k
inst✝² : OrderedAddCommGroup E
inst✝¹ : Module k E
inst✝ : OrderedSMul k E
a a' b b' : E
r r' : k
h : r < r'
⊢ ↑(lineMap a b) r < ↑(lineMap a b) r' ↔ a < b
[PROOFSTEP]
simp only [lineMap_apply_module]
[GOAL]
k : Type u_1
E : Type u_2
PE : Type u_3
inst✝³ : OrderedRing k
inst✝² : OrderedAddCommGroup E
inst✝¹ : Module k E
inst✝ : OrderedSMul k E
a a' b b' : E
r r' : k
h : r < r'
⊢ (1 - r) • a + r • b < (1 - r') • a + r' • b ↔ a < b
[PROOFSTEP]
rw [← lt_sub_iff_add_lt, add_sub_assoc, ← sub_lt_iff_lt_add', ← sub_smul, ← sub_smul, sub_sub_sub_cancel_left,
  smul_lt_smul_iff_of_pos (sub_pos.2 h)]
[GOAL]
k : Type u_1
E : Type u_2
PE : Type u_3
inst✝³ : OrderedRing k
inst✝² : OrderedAddCommGroup E
inst✝¹ : Module k E
inst✝ : OrderedSMul k E
a a' b b' : E
r r' : k
h : 0 < r
⊢ a < ↑(lineMap a b) r ↔ ↑(lineMap a b) 0 < ↑(lineMap a b) r
[PROOFSTEP]
rw [lineMap_apply_zero]
[GOAL]
k : Type u_1
E : Type u_2
PE : Type u_3
inst✝³ : OrderedRing k
inst✝² : OrderedAddCommGroup E
inst✝¹ : Module k E
inst✝ : OrderedSMul k E
a a' b b' : E
r r' : k
h : r < 1
⊢ ↑(lineMap a b) r < b ↔ ↑(lineMap a b) r < ↑(lineMap a b) 1
[PROOFSTEP]
rw [lineMap_apply_one]
[GOAL]
k : Type u_1
E : Type u_2
PE : Type u_3
inst✝³ : LinearOrderedField k
inst✝² : OrderedAddCommGroup E
inst✝¹ : Module k E
inst✝ : OrderedSMul k E
a b : E
r r' : k
h : r < r'
⊢ ↑(lineMap a b) r ≤ ↑(lineMap a b) r' ↔ a ≤ b
[PROOFSTEP]
simp only [lineMap_apply_module]
[GOAL]
k : Type u_1
E : Type u_2
PE : Type u_3
inst✝³ : LinearOrderedField k
inst✝² : OrderedAddCommGroup E
inst✝¹ : Module k E
inst✝ : OrderedSMul k E
a b : E
r r' : k
h : r < r'
⊢ (1 - r) • a + r • b ≤ (1 - r') • a + r' • b ↔ a ≤ b
[PROOFSTEP]
rw [← le_sub_iff_add_le, add_sub_assoc, ← sub_le_iff_le_add', ← sub_smul, ← sub_smul, sub_sub_sub_cancel_left,
  smul_le_smul_iff_of_pos (sub_pos.2 h)]
[GOAL]
k : Type u_1
E : Type u_2
PE : Type u_3
inst✝³ : LinearOrderedField k
inst✝² : OrderedAddCommGroup E
inst✝¹ : Module k E
inst✝ : OrderedSMul k E
a b : E
r r' : k
h : 0 < r
⊢ a ≤ ↑(lineMap a b) r ↔ ↑(lineMap a b) 0 ≤ ↑(lineMap a b) r
[PROOFSTEP]
rw [lineMap_apply_zero]
[GOAL]
k : Type u_1
E : Type u_2
PE : Type u_3
inst✝³ : LinearOrderedField k
inst✝² : OrderedAddCommGroup E
inst✝¹ : Module k E
inst✝ : OrderedSMul k E
a b : E
r r' : k
h : r < 1
⊢ ↑(lineMap a b) r ≤ b ↔ ↑(lineMap a b) r ≤ ↑(lineMap a b) 1
[PROOFSTEP]
rw [lineMap_apply_one]
[GOAL]
k : Type u_1
E : Type u_2
PE : Type u_3
inst✝³ : LinearOrderedField k
inst✝² : OrderedAddCommGroup E
inst✝¹ : Module k E
inst✝ : OrderedSMul k E
f : k → E
a b r : k
h : 0 < r * (b - a)
⊢ f (↑(lineMap a b) r) ≤ ↑(lineMap (f a) (f b)) r ↔ slope f a (↑(lineMap a b) r) ≤ slope f a b
[PROOFSTEP]
rw [lineMap_apply, lineMap_apply, slope, slope, vsub_eq_sub, vsub_eq_sub, vsub_eq_sub, vadd_eq_add, vadd_eq_add,
  smul_eq_mul, add_sub_cancel, smul_sub, smul_sub, smul_sub, sub_le_iff_le_add, mul_inv_rev, mul_smul, mul_smul, ←
  smul_sub, ← smul_sub, ← smul_add, smul_smul, ← mul_inv_rev, inv_smul_le_iff h, smul_smul,
  mul_inv_cancel_right₀ (right_ne_zero_of_mul h.ne'), smul_add, smul_inv_smul₀ (left_ne_zero_of_mul h.ne')]
[GOAL]
k : Type u_1
E : Type u_2
PE : Type u_3
inst✝³ : LinearOrderedField k
inst✝² : OrderedAddCommGroup E
inst✝¹ : Module k E
inst✝ : OrderedSMul k E
f : k → E
a b r : k
h : 0 < (1 - r) * (b - a)
⊢ f (↑(lineMap a b) r) ≤ ↑(lineMap (f a) (f b)) r ↔ slope f a b ≤ slope f (↑(lineMap a b) r) b
[PROOFSTEP]
rw [← lineMap_apply_one_sub, ← lineMap_apply_one_sub _ _ r]
[GOAL]
k : Type u_1
E : Type u_2
PE : Type u_3
inst✝³ : LinearOrderedField k
inst✝² : OrderedAddCommGroup E
inst✝¹ : Module k E
inst✝ : OrderedSMul k E
f : k → E
a b r : k
h : 0 < (1 - r) * (b - a)
⊢ f (↑(lineMap b a) (1 - r)) ≤ ↑(lineMap (f b) (f a)) (1 - r) ↔ slope f a b ≤ slope f (↑(lineMap b a) (1 - r)) b
[PROOFSTEP]
revert h
[GOAL]
k : Type u_1
E : Type u_2
PE : Type u_3
inst✝³ : LinearOrderedField k
inst✝² : OrderedAddCommGroup E
inst✝¹ : Module k E
inst✝ : OrderedSMul k E
f : k → E
a b r : k
⊢ 0 < (1 - r) * (b - a) →
    (f (↑(lineMap b a) (1 - r)) ≤ ↑(lineMap (f b) (f a)) (1 - r) ↔ slope f a b ≤ slope f (↑(lineMap b a) (1 - r)) b)
[PROOFSTEP]
generalize 1 - r = r'
[GOAL]
k : Type u_1
E : Type u_2
PE : Type u_3
inst✝³ : LinearOrderedField k
inst✝² : OrderedAddCommGroup E
inst✝¹ : Module k E
inst✝ : OrderedSMul k E
f : k → E
a b r r' : k
⊢ 0 < r' * (b - a) → (f (↑(lineMap b a) r') ≤ ↑(lineMap (f b) (f a)) r' ↔ slope f a b ≤ slope f (↑(lineMap b a) r') b)
[PROOFSTEP]
clear! r
[GOAL]
k : Type u_1
E : Type u_2
PE : Type u_3
inst✝³ : LinearOrderedField k
inst✝² : OrderedAddCommGroup E
inst✝¹ : Module k E
inst✝ : OrderedSMul k E
f : k → E
a b r' : k
⊢ 0 < r' * (b - a) → (f (↑(lineMap b a) r') ≤ ↑(lineMap (f b) (f a)) r' ↔ slope f a b ≤ slope f (↑(lineMap b a) r') b)
[PROOFSTEP]
intro h
[GOAL]
k : Type u_1
E : Type u_2
PE : Type u_3
inst✝³ : LinearOrderedField k
inst✝² : OrderedAddCommGroup E
inst✝¹ : Module k E
inst✝ : OrderedSMul k E
f : k → E
a b r' : k
h : 0 < r' * (b - a)
⊢ f (↑(lineMap b a) r') ≤ ↑(lineMap (f b) (f a)) r' ↔ slope f a b ≤ slope f (↑(lineMap b a) r') b
[PROOFSTEP]
simp_rw [lineMap_apply, slope, vsub_eq_sub, vadd_eq_add, smul_eq_mul]
[GOAL]
k : Type u_1
E : Type u_2
PE : Type u_3
inst✝³ : LinearOrderedField k
inst✝² : OrderedAddCommGroup E
inst✝¹ : Module k E
inst✝ : OrderedSMul k E
f : k → E
a b r' : k
h : 0 < r' * (b - a)
⊢ f (r' * (a - b) + b) ≤ r' • (f a - f b) + f b ↔
    (b - a)⁻¹ • (f b - f a) ≤ (b - (r' * (a - b) + b))⁻¹ • (f b - f (r' * (a - b) + b))
[PROOFSTEP]
rw [sub_add_eq_sub_sub_swap, sub_self, zero_sub, neg_mul_eq_mul_neg, neg_sub, le_inv_smul_iff h, smul_smul,
  mul_inv_cancel_right₀, le_sub_comm, ← neg_sub (f b), smul_neg, neg_add_eq_sub]
[GOAL]
case h
k : Type u_1
E : Type u_2
PE : Type u_3
inst✝³ : LinearOrderedField k
inst✝² : OrderedAddCommGroup E
inst✝¹ : Module k E
inst✝ : OrderedSMul k E
f : k → E
a b r' : k
h : 0 < r' * (b - a)
⊢ b - a ≠ 0
[PROOFSTEP]
exact right_ne_zero_of_mul h.ne'
[GOAL]
k : Type u_1
E : Type u_2
PE : Type u_3
inst✝³ : LinearOrderedField k
inst✝² : OrderedAddCommGroup E
inst✝¹ : Module k E
inst✝ : OrderedSMul k E
f : k → E
a b r : k
hab : a < b
h₀ : 0 < r
h₁ : r < 1
⊢ f (↑(lineMap a b) r) ≤ ↑(lineMap (f a) (f b)) r ↔ slope f a (↑(lineMap a b) r) ≤ slope f (↑(lineMap a b) r) b
[PROOFSTEP]
rw [map_le_lineMap_iff_slope_le_slope_left (mul_pos h₀ (sub_pos.2 hab)), ← lineMap_slope_lineMap_slope_lineMap f a b r,
  right_le_lineMap_iff_le h₁]


[GOAL]
K : Type v
V : Type w
inst✝⁵ : Field K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
inst✝² : IsAlgClosed K
inst✝¹ : FiniteDimensional K V
inst✝ : Nontrivial V
f : End K V
⊢ ∃ c, HasEigenvalue f c
[PROOFSTEP]
simp_rw [hasEigenvalue_iff_mem_spectrum]
[GOAL]
K : Type v
V : Type w
inst✝⁵ : Field K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
inst✝² : IsAlgClosed K
inst✝¹ : FiniteDimensional K V
inst✝ : Nontrivial V
f : End K V
⊢ ∃ c, c ∈ spectrum K f
[PROOFSTEP]
exact spectrum.nonempty_of_isAlgClosed_of_finiteDimensional K f
[GOAL]
K : Type v
V : Type w
inst✝⁴ : Field K
inst✝³ : AddCommGroup V
inst✝² : Module K V
inst✝¹ : IsAlgClosed K
inst✝ : FiniteDimensional K V
f : End K V
⊢ ⨆ (μ : K) (k : ℕ), ↑(generalizedEigenspace f μ) k = ⊤
[PROOFSTEP]
induction' h_dim : finrank K V using Nat.strong_induction_on with n ih generalizing V
[GOAL]
case h
K : Type v
V✝ : Type w
inst✝⁷ : Field K
inst✝⁶ : AddCommGroup V✝
inst✝⁵ : Module K V✝
inst✝⁴ : IsAlgClosed K
inst✝³ : FiniteDimensional K V✝
f✝ : End K V✝
x✝ : ℕ
h_dim✝ : finrank K V✝ = x✝
n : ℕ
ih :
  ∀ (m : ℕ),
    m < n →
      ∀ {V : Type w} [inst : AddCommGroup V] [inst_1 : Module K V] [inst_2 : FiniteDimensional K V] (f : End K V),
        finrank K V = m → ⨆ (μ : K) (k : ℕ), ↑(generalizedEigenspace f μ) k = ⊤
V : Type w
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
h_dim : finrank K V = n
⊢ ⨆ (μ : K) (k : ℕ), ↑(generalizedEigenspace f μ) k = ⊤
[PROOFSTEP]
cases' n with n
[GOAL]
case h.zero
K : Type v
V✝ : Type w
inst✝⁷ : Field K
inst✝⁶ : AddCommGroup V✝
inst✝⁵ : Module K V✝
inst✝⁴ : IsAlgClosed K
inst✝³ : FiniteDimensional K V✝
f✝ : End K V✝
x✝ : ℕ
h_dim✝ : finrank K V✝ = x✝
V : Type w
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
ih :
  ∀ (m : ℕ),
    m < Nat.zero →
      ∀ {V : Type w} [inst : AddCommGroup V] [inst_1 : Module K V] [inst_2 : FiniteDimensional K V] (f : End K V),
        finrank K V = m → ⨆ (μ : K) (k : ℕ), ↑(generalizedEigenspace f μ) k = ⊤
h_dim : finrank K V = Nat.zero
⊢ ⨆ (μ : K) (k : ℕ), ↑(generalizedEigenspace f μ) k = ⊤
[PROOFSTEP]
rw [← top_le_iff]
[GOAL]
case h.zero
K : Type v
V✝ : Type w
inst✝⁷ : Field K
inst✝⁶ : AddCommGroup V✝
inst✝⁵ : Module K V✝
inst✝⁴ : IsAlgClosed K
inst✝³ : FiniteDimensional K V✝
f✝ : End K V✝
x✝ : ℕ
h_dim✝ : finrank K V✝ = x✝
V : Type w
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
ih :
  ∀ (m : ℕ),
    m < Nat.zero →
      ∀ {V : Type w} [inst : AddCommGroup V] [inst_1 : Module K V] [inst_2 : FiniteDimensional K V] (f : End K V),
        finrank K V = m → ⨆ (μ : K) (k : ℕ), ↑(generalizedEigenspace f μ) k = ⊤
h_dim : finrank K V = Nat.zero
⊢ ⊤ ≤ ⨆ (μ : K) (k : ℕ), ↑(generalizedEigenspace f μ) k
[PROOFSTEP]
simp only [finrank_eq_zero.1 (Eq.trans (finrank_top _ _) h_dim), bot_le]
  -- Otherwise the vector space is nontrivial.
[GOAL]
case h.succ
K : Type v
V✝ : Type w
inst✝⁷ : Field K
inst✝⁶ : AddCommGroup V✝
inst✝⁵ : Module K V✝
inst✝⁴ : IsAlgClosed K
inst✝³ : FiniteDimensional K V✝
f✝ : End K V✝
x✝ : ℕ
h_dim✝ : finrank K V✝ = x✝
V : Type w
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
n : ℕ
ih :
  ∀ (m : ℕ),
    m < Nat.succ n →
      ∀ {V : Type w} [inst : AddCommGroup V] [inst_1 : Module K V] [inst_2 : FiniteDimensional K V] (f : End K V),
        finrank K V = m → ⨆ (μ : K) (k : ℕ), ↑(generalizedEigenspace f μ) k = ⊤
h_dim : finrank K V = Nat.succ n
⊢ ⨆ (μ : K) (k : ℕ), ↑(generalizedEigenspace f μ) k = ⊤
[PROOFSTEP]
haveI : Nontrivial V :=
  finrank_pos_iff.1
    (by rw [h_dim]; apply Nat.zero_lt_succ)
      -- Hence, `f` has an eigenvalue `μ₀`.
[GOAL]
K : Type v
V✝ : Type w
inst✝⁷ : Field K
inst✝⁶ : AddCommGroup V✝
inst✝⁵ : Module K V✝
inst✝⁴ : IsAlgClosed K
inst✝³ : FiniteDimensional K V✝
f✝ : End K V✝
x✝ : ℕ
h_dim✝ : finrank K V✝ = x✝
V : Type w
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
n : ℕ
ih :
  ∀ (m : ℕ),
    m < Nat.succ n →
      ∀ {V : Type w} [inst : AddCommGroup V] [inst_1 : Module K V] [inst_2 : FiniteDimensional K V] (f : End K V),
        finrank K V = m → ⨆ (μ : K) (k : ℕ), ↑(generalizedEigenspace f μ) k = ⊤
h_dim : finrank K V = Nat.succ n
⊢ 0 < finrank ?m.10065 V
[PROOFSTEP]
rw [h_dim]
[GOAL]
K : Type v
V✝ : Type w
inst✝⁷ : Field K
inst✝⁶ : AddCommGroup V✝
inst✝⁵ : Module K V✝
inst✝⁴ : IsAlgClosed K
inst✝³ : FiniteDimensional K V✝
f✝ : End K V✝
x✝ : ℕ
h_dim✝ : finrank K V✝ = x✝
V : Type w
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
n : ℕ
ih :
  ∀ (m : ℕ),
    m < Nat.succ n →
      ∀ {V : Type w} [inst : AddCommGroup V] [inst_1 : Module K V] [inst_2 : FiniteDimensional K V] (f : End K V),
        finrank K V = m → ⨆ (μ : K) (k : ℕ), ↑(generalizedEigenspace f μ) k = ⊤
h_dim : finrank K V = Nat.succ n
⊢ 0 < Nat.succ n
[PROOFSTEP]
apply Nat.zero_lt_succ
[GOAL]
case h.succ
K : Type v
V✝ : Type w
inst✝⁷ : Field K
inst✝⁶ : AddCommGroup V✝
inst✝⁵ : Module K V✝
inst✝⁴ : IsAlgClosed K
inst✝³ : FiniteDimensional K V✝
f✝ : End K V✝
x✝ : ℕ
h_dim✝ : finrank K V✝ = x✝
V : Type w
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
n : ℕ
ih :
  ∀ (m : ℕ),
    m < Nat.succ n →
      ∀ {V : Type w} [inst : AddCommGroup V] [inst_1 : Module K V] [inst_2 : FiniteDimensional K V] (f : End K V),
        finrank K V = m → ⨆ (μ : K) (k : ℕ), ↑(generalizedEigenspace f μ) k = ⊤
h_dim : finrank K V = Nat.succ n
this : Nontrivial V
⊢ ⨆ (μ : K) (k : ℕ), ↑(generalizedEigenspace f μ) k = ⊤
[PROOFSTEP]
obtain ⟨μ₀, hμ₀⟩ : ∃ μ₀, f.HasEigenvalue μ₀ := exists_eigenvalue f
[GOAL]
case h.succ.intro
K : Type v
V✝ : Type w
inst✝⁷ : Field K
inst✝⁶ : AddCommGroup V✝
inst✝⁵ : Module K V✝
inst✝⁴ : IsAlgClosed K
inst✝³ : FiniteDimensional K V✝
f✝ : End K V✝
x✝ : ℕ
h_dim✝ : finrank K V✝ = x✝
V : Type w
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
n : ℕ
ih :
  ∀ (m : ℕ),
    m < Nat.succ n →
      ∀ {V : Type w} [inst : AddCommGroup V] [inst_1 : Module K V] [inst_2 : FiniteDimensional K V] (f : End K V),
        finrank K V = m → ⨆ (μ : K) (k : ℕ), ↑(generalizedEigenspace f μ) k = ⊤
h_dim : finrank K V = Nat.succ n
this : Nontrivial V
μ₀ : K
hμ₀ : HasEigenvalue f μ₀
⊢ ⨆ (μ : K) (k : ℕ), ↑(generalizedEigenspace f μ) k = ⊤
[PROOFSTEP]
let ES :=
  f.generalizedEigenspace μ₀
    (finrank K V)
      -- and `ER` to be the generalized eigenrange.
[GOAL]
case h.succ.intro
K : Type v
V✝ : Type w
inst✝⁷ : Field K
inst✝⁶ : AddCommGroup V✝
inst✝⁵ : Module K V✝
inst✝⁴ : IsAlgClosed K
inst✝³ : FiniteDimensional K V✝
f✝ : End K V✝
x✝ : ℕ
h_dim✝ : finrank K V✝ = x✝
V : Type w
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
n : ℕ
ih :
  ∀ (m : ℕ),
    m < Nat.succ n →
      ∀ {V : Type w} [inst : AddCommGroup V] [inst_1 : Module K V] [inst_2 : FiniteDimensional K V] (f : End K V),
        finrank K V = m → ⨆ (μ : K) (k : ℕ), ↑(generalizedEigenspace f μ) k = ⊤
h_dim : finrank K V = Nat.succ n
this : Nontrivial V
μ₀ : K
hμ₀ : HasEigenvalue f μ₀
ES : Submodule K V := ↑(generalizedEigenspace f μ₀) (finrank K V)
⊢ ⨆ (μ : K) (k : ℕ), ↑(generalizedEigenspace f μ) k = ⊤
[PROOFSTEP]
let ER :=
  f.generalizedEigenrange μ₀
    (finrank K V)
      -- `f` maps `ER` into itself.
[GOAL]
case h.succ.intro
K : Type v
V✝ : Type w
inst✝⁷ : Field K
inst✝⁶ : AddCommGroup V✝
inst✝⁵ : Module K V✝
inst✝⁴ : IsAlgClosed K
inst✝³ : FiniteDimensional K V✝
f✝ : End K V✝
x✝ : ℕ
h_dim✝ : finrank K V✝ = x✝
V : Type w
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
n : ℕ
ih :
  ∀ (m : ℕ),
    m < Nat.succ n →
      ∀ {V : Type w} [inst : AddCommGroup V] [inst_1 : Module K V] [inst_2 : FiniteDimensional K V] (f : End K V),
        finrank K V = m → ⨆ (μ : K) (k : ℕ), ↑(generalizedEigenspace f μ) k = ⊤
h_dim : finrank K V = Nat.succ n
this : Nontrivial V
μ₀ : K
hμ₀ : HasEigenvalue f μ₀
ES : Submodule K V := ↑(generalizedEigenspace f μ₀) (finrank K V)
ER : Submodule K V := generalizedEigenrange f μ₀ (finrank K V)
⊢ ⨆ (μ : K) (k : ℕ), ↑(generalizedEigenspace f μ) k = ⊤
[PROOFSTEP]
have h_f_ER : ∀ x : V, x ∈ ER → f x ∈ ER := fun x hx =>
  map_generalizedEigenrange_le
    (Submodule.mem_map_of_mem hx)
      -- Therefore, we can define the restriction `f'` of `f` to `ER`.
[GOAL]
case h.succ.intro
K : Type v
V✝ : Type w
inst✝⁷ : Field K
inst✝⁶ : AddCommGroup V✝
inst✝⁵ : Module K V✝
inst✝⁴ : IsAlgClosed K
inst✝³ : FiniteDimensional K V✝
f✝ : End K V✝
x✝ : ℕ
h_dim✝ : finrank K V✝ = x✝
V : Type w
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
n : ℕ
ih :
  ∀ (m : ℕ),
    m < Nat.succ n →
      ∀ {V : Type w} [inst : AddCommGroup V] [inst_1 : Module K V] [inst_2 : FiniteDimensional K V] (f : End K V),
        finrank K V = m → ⨆ (μ : K) (k : ℕ), ↑(generalizedEigenspace f μ) k = ⊤
h_dim : finrank K V = Nat.succ n
this : Nontrivial V
μ₀ : K
hμ₀ : HasEigenvalue f μ₀
ES : Submodule K V := ↑(generalizedEigenspace f μ₀) (finrank K V)
ER : Submodule K V := generalizedEigenrange f μ₀ (finrank K V)
h_f_ER : ∀ (x : V), x ∈ ER → ↑f x ∈ ER
⊢ ⨆ (μ : K) (k : ℕ), ↑(generalizedEigenspace f μ) k = ⊤
[PROOFSTEP]
let f' : End K ER := f.restrict h_f_ER
[GOAL]
case h.succ.intro
K : Type v
V✝ : Type w
inst✝⁷ : Field K
inst✝⁶ : AddCommGroup V✝
inst✝⁵ : Module K V✝
inst✝⁴ : IsAlgClosed K
inst✝³ : FiniteDimensional K V✝
f✝ : End K V✝
x✝ : ℕ
h_dim✝ : finrank K V✝ = x✝
V : Type w
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
n : ℕ
ih :
  ∀ (m : ℕ),
    m < Nat.succ n →
      ∀ {V : Type w} [inst : AddCommGroup V] [inst_1 : Module K V] [inst_2 : FiniteDimensional K V] (f : End K V),
        finrank K V = m → ⨆ (μ : K) (k : ℕ), ↑(generalizedEigenspace f μ) k = ⊤
h_dim : finrank K V = Nat.succ n
this : Nontrivial V
μ₀ : K
hμ₀ : HasEigenvalue f μ₀
ES : Submodule K V := ↑(generalizedEigenspace f μ₀) (finrank K V)
ER : Submodule K V := generalizedEigenrange f μ₀ (finrank K V)
h_f_ER : ∀ (x : V), x ∈ ER → ↑f x ∈ ER
f' : End K { x // x ∈ ER } := LinearMap.restrict f h_f_ER
⊢ ⨆ (μ : K) (k : ℕ), ↑(generalizedEigenspace f μ) k = ⊤
[PROOFSTEP]
have h_dim_ES_pos : 0 < finrank K ES := by
  dsimp only
  rw [h_dim]
  apply
    pos_finrank_generalizedEigenspace_of_hasEigenvalue hμ₀
      (Nat.zero_lt_succ n)
        -- and the dimensions of `ES` and `ER` add up to `finrank K V`.
[GOAL]
K : Type v
V✝ : Type w
inst✝⁷ : Field K
inst✝⁶ : AddCommGroup V✝
inst✝⁵ : Module K V✝
inst✝⁴ : IsAlgClosed K
inst✝³ : FiniteDimensional K V✝
f✝ : End K V✝
x✝ : ℕ
h_dim✝ : finrank K V✝ = x✝
V : Type w
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
n : ℕ
ih :
  ∀ (m : ℕ),
    m < Nat.succ n →
      ∀ {V : Type w} [inst : AddCommGroup V] [inst_1 : Module K V] [inst_2 : FiniteDimensional K V] (f : End K V),
        finrank K V = m → ⨆ (μ : K) (k : ℕ), ↑(generalizedEigenspace f μ) k = ⊤
h_dim : finrank K V = Nat.succ n
this : Nontrivial V
μ₀ : K
hμ₀ : HasEigenvalue f μ₀
ES : Submodule K V := ↑(generalizedEigenspace f μ₀) (finrank K V)
ER : Submodule K V := generalizedEigenrange f μ₀ (finrank K V)
h_f_ER : ∀ (x : V), x ∈ ER → ↑f x ∈ ER
f' : End K { x // x ∈ ER } := LinearMap.restrict f h_f_ER
⊢ 0 < finrank K { x // x ∈ ES }
[PROOFSTEP]
dsimp only
[GOAL]
K : Type v
V✝ : Type w
inst✝⁷ : Field K
inst✝⁶ : AddCommGroup V✝
inst✝⁵ : Module K V✝
inst✝⁴ : IsAlgClosed K
inst✝³ : FiniteDimensional K V✝
f✝ : End K V✝
x✝ : ℕ
h_dim✝ : finrank K V✝ = x✝
V : Type w
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
n : ℕ
ih :
  ∀ (m : ℕ),
    m < Nat.succ n →
      ∀ {V : Type w} [inst : AddCommGroup V] [inst_1 : Module K V] [inst_2 : FiniteDimensional K V] (f : End K V),
        finrank K V = m → ⨆ (μ : K) (k : ℕ), ↑(generalizedEigenspace f μ) k = ⊤
h_dim : finrank K V = Nat.succ n
this : Nontrivial V
μ₀ : K
hμ₀ : HasEigenvalue f μ₀
ES : Submodule K V := ↑(generalizedEigenspace f μ₀) (finrank K V)
ER : Submodule K V := generalizedEigenrange f μ₀ (finrank K V)
h_f_ER : ∀ (x : V), x ∈ ER → ↑f x ∈ ER
f' : End K { x // x ∈ ER } := LinearMap.restrict f h_f_ER
⊢ 0 < finrank K { x // x ∈ ↑(generalizedEigenspace f μ₀) (finrank K V) }
[PROOFSTEP]
rw [h_dim]
[GOAL]
K : Type v
V✝ : Type w
inst✝⁷ : Field K
inst✝⁶ : AddCommGroup V✝
inst✝⁵ : Module K V✝
inst✝⁴ : IsAlgClosed K
inst✝³ : FiniteDimensional K V✝
f✝ : End K V✝
x✝ : ℕ
h_dim✝ : finrank K V✝ = x✝
V : Type w
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
n : ℕ
ih :
  ∀ (m : ℕ),
    m < Nat.succ n →
      ∀ {V : Type w} [inst : AddCommGroup V] [inst_1 : Module K V] [inst_2 : FiniteDimensional K V] (f : End K V),
        finrank K V = m → ⨆ (μ : K) (k : ℕ), ↑(generalizedEigenspace f μ) k = ⊤
h_dim : finrank K V = Nat.succ n
this : Nontrivial V
μ₀ : K
hμ₀ : HasEigenvalue f μ₀
ES : Submodule K V := ↑(generalizedEigenspace f μ₀) (finrank K V)
ER : Submodule K V := generalizedEigenrange f μ₀ (finrank K V)
h_f_ER : ∀ (x : V), x ∈ ER → ↑f x ∈ ER
f' : End K { x // x ∈ ER } := LinearMap.restrict f h_f_ER
⊢ 0 < finrank K { x // x ∈ ↑(generalizedEigenspace f μ₀) (Nat.succ n) }
[PROOFSTEP]
apply
  pos_finrank_generalizedEigenspace_of_hasEigenvalue hμ₀
    (Nat.zero_lt_succ n)
      -- and the dimensions of `ES` and `ER` add up to `finrank K V`.
[GOAL]
case h.succ.intro
K : Type v
V✝ : Type w
inst✝⁷ : Field K
inst✝⁶ : AddCommGroup V✝
inst✝⁵ : Module K V✝
inst✝⁴ : IsAlgClosed K
inst✝³ : FiniteDimensional K V✝
f✝ : End K V✝
x✝ : ℕ
h_dim✝ : finrank K V✝ = x✝
V : Type w
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
n : ℕ
ih :
  ∀ (m : ℕ),
    m < Nat.succ n →
      ∀ {V : Type w} [inst : AddCommGroup V] [inst_1 : Module K V] [inst_2 : FiniteDimensional K V] (f : End K V),
        finrank K V = m → ⨆ (μ : K) (k : ℕ), ↑(generalizedEigenspace f μ) k = ⊤
h_dim : finrank K V = Nat.succ n
this : Nontrivial V
μ₀ : K
hμ₀ : HasEigenvalue f μ₀
ES : Submodule K V := ↑(generalizedEigenspace f μ₀) (finrank K V)
ER : Submodule K V := generalizedEigenrange f μ₀ (finrank K V)
h_f_ER : ∀ (x : V), x ∈ ER → ↑f x ∈ ER
f' : End K { x // x ∈ ER } := LinearMap.restrict f h_f_ER
h_dim_ES_pos : 0 < finrank K { x // x ∈ ES }
⊢ ⨆ (μ : K) (k : ℕ), ↑(generalizedEigenspace f μ) k = ⊤
[PROOFSTEP]
have h_dim_add : finrank K ER + finrank K ES = finrank K V := by apply LinearMap.finrank_range_add_finrank_ker
[GOAL]
K : Type v
V✝ : Type w
inst✝⁷ : Field K
inst✝⁶ : AddCommGroup V✝
inst✝⁵ : Module K V✝
inst✝⁴ : IsAlgClosed K
inst✝³ : FiniteDimensional K V✝
f✝ : End K V✝
x✝ : ℕ
h_dim✝ : finrank K V✝ = x✝
V : Type w
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
n : ℕ
ih :
  ∀ (m : ℕ),
    m < Nat.succ n →
      ∀ {V : Type w} [inst : AddCommGroup V] [inst_1 : Module K V] [inst_2 : FiniteDimensional K V] (f : End K V),
        finrank K V = m → ⨆ (μ : K) (k : ℕ), ↑(generalizedEigenspace f μ) k = ⊤
h_dim : finrank K V = Nat.succ n
this : Nontrivial V
μ₀ : K
hμ₀ : HasEigenvalue f μ₀
ES : Submodule K V := ↑(generalizedEigenspace f μ₀) (finrank K V)
ER : Submodule K V := generalizedEigenrange f μ₀ (finrank K V)
h_f_ER : ∀ (x : V), x ∈ ER → ↑f x ∈ ER
f' : End K { x // x ∈ ER } := LinearMap.restrict f h_f_ER
h_dim_ES_pos : 0 < finrank K { x // x ∈ ES }
⊢ finrank K { x // x ∈ ER } + finrank K { x // x ∈ ES } = finrank K V
[PROOFSTEP]
apply LinearMap.finrank_range_add_finrank_ker
[GOAL]
case h.succ.intro
K : Type v
V✝ : Type w
inst✝⁷ : Field K
inst✝⁶ : AddCommGroup V✝
inst✝⁵ : Module K V✝
inst✝⁴ : IsAlgClosed K
inst✝³ : FiniteDimensional K V✝
f✝ : End K V✝
x✝ : ℕ
h_dim✝ : finrank K V✝ = x✝
V : Type w
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
n : ℕ
ih :
  ∀ (m : ℕ),
    m < Nat.succ n →
      ∀ {V : Type w} [inst : AddCommGroup V] [inst_1 : Module K V] [inst_2 : FiniteDimensional K V] (f : End K V),
        finrank K V = m → ⨆ (μ : K) (k : ℕ), ↑(generalizedEigenspace f μ) k = ⊤
h_dim : finrank K V = Nat.succ n
this : Nontrivial V
μ₀ : K
hμ₀ : HasEigenvalue f μ₀
ES : Submodule K V := ↑(generalizedEigenspace f μ₀) (finrank K V)
ER : Submodule K V := generalizedEigenrange f μ₀ (finrank K V)
h_f_ER : ∀ (x : V), x ∈ ER → ↑f x ∈ ER
f' : End K { x // x ∈ ER } := LinearMap.restrict f h_f_ER
h_dim_ES_pos : 0 < finrank K { x // x ∈ ES }
h_dim_add : finrank K { x // x ∈ ER } + finrank K { x // x ∈ ES } = finrank K V
⊢ ⨆ (μ : K) (k : ℕ), ↑(generalizedEigenspace f μ) k = ⊤
[PROOFSTEP]
have h_dim_ER : finrank K ER < n.succ := by
  linarith
    -- This allows us to apply the induction hypothesis on `ER`:
[GOAL]
K : Type v
V✝ : Type w
inst✝⁷ : Field K
inst✝⁶ : AddCommGroup V✝
inst✝⁵ : Module K V✝
inst✝⁴ : IsAlgClosed K
inst✝³ : FiniteDimensional K V✝
f✝ : End K V✝
x✝ : ℕ
h_dim✝ : finrank K V✝ = x✝
V : Type w
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
n : ℕ
ih :
  ∀ (m : ℕ),
    m < Nat.succ n →
      ∀ {V : Type w} [inst : AddCommGroup V] [inst_1 : Module K V] [inst_2 : FiniteDimensional K V] (f : End K V),
        finrank K V = m → ⨆ (μ : K) (k : ℕ), ↑(generalizedEigenspace f μ) k = ⊤
h_dim : finrank K V = Nat.succ n
this : Nontrivial V
μ₀ : K
hμ₀ : HasEigenvalue f μ₀
ES : Submodule K V := ↑(generalizedEigenspace f μ₀) (finrank K V)
ER : Submodule K V := generalizedEigenrange f μ₀ (finrank K V)
h_f_ER : ∀ (x : V), x ∈ ER → ↑f x ∈ ER
f' : End K { x // x ∈ ER } := LinearMap.restrict f h_f_ER
h_dim_ES_pos : 0 < finrank K { x // x ∈ ES }
h_dim_add : finrank K { x // x ∈ ER } + finrank K { x // x ∈ ES } = finrank K V
⊢ finrank K { x // x ∈ ER } < Nat.succ n
[PROOFSTEP]
linarith
  -- This allows us to apply the induction hypothesis on `ER`:
[GOAL]
case h.succ.intro
K : Type v
V✝ : Type w
inst✝⁷ : Field K
inst✝⁶ : AddCommGroup V✝
inst✝⁵ : Module K V✝
inst✝⁴ : IsAlgClosed K
inst✝³ : FiniteDimensional K V✝
f✝ : End K V✝
x✝ : ℕ
h_dim✝ : finrank K V✝ = x✝
V : Type w
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
n : ℕ
ih :
  ∀ (m : ℕ),
    m < Nat.succ n →
      ∀ {V : Type w} [inst : AddCommGroup V] [inst_1 : Module K V] [inst_2 : FiniteDimensional K V] (f : End K V),
        finrank K V = m → ⨆ (μ : K) (k : ℕ), ↑(generalizedEigenspace f μ) k = ⊤
h_dim : finrank K V = Nat.succ n
this : Nontrivial V
μ₀ : K
hμ₀ : HasEigenvalue f μ₀
ES : Submodule K V := ↑(generalizedEigenspace f μ₀) (finrank K V)
ER : Submodule K V := generalizedEigenrange f μ₀ (finrank K V)
h_f_ER : ∀ (x : V), x ∈ ER → ↑f x ∈ ER
f' : End K { x // x ∈ ER } := LinearMap.restrict f h_f_ER
h_dim_ES_pos : 0 < finrank K { x // x ∈ ES }
h_dim_add : finrank K { x // x ∈ ER } + finrank K { x // x ∈ ES } = finrank K V
h_dim_ER : finrank K { x // x ∈ ER } < Nat.succ n
⊢ ⨆ (μ : K) (k : ℕ), ↑(generalizedEigenspace f μ) k = ⊤
[PROOFSTEP]
have ih_ER : ⨆ (μ : K) (k : ℕ), f'.generalizedEigenspace μ k = ⊤ := ih (finrank K ER) h_dim_ER f' rfl
[GOAL]
case h.succ.intro
K : Type v
V✝ : Type w
inst✝⁷ : Field K
inst✝⁶ : AddCommGroup V✝
inst✝⁵ : Module K V✝
inst✝⁴ : IsAlgClosed K
inst✝³ : FiniteDimensional K V✝
f✝ : End K V✝
x✝ : ℕ
h_dim✝ : finrank K V✝ = x✝
V : Type w
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
n : ℕ
ih :
  ∀ (m : ℕ),
    m < Nat.succ n →
      ∀ {V : Type w} [inst : AddCommGroup V] [inst_1 : Module K V] [inst_2 : FiniteDimensional K V] (f : End K V),
        finrank K V = m → ⨆ (μ : K) (k : ℕ), ↑(generalizedEigenspace f μ) k = ⊤
h_dim : finrank K V = Nat.succ n
this : Nontrivial V
μ₀ : K
hμ₀ : HasEigenvalue f μ₀
ES : Submodule K V := ↑(generalizedEigenspace f μ₀) (finrank K V)
ER : Submodule K V := generalizedEigenrange f μ₀ (finrank K V)
h_f_ER : ∀ (x : V), x ∈ ER → ↑f x ∈ ER
f' : End K { x // x ∈ ER } := LinearMap.restrict f h_f_ER
h_dim_ES_pos : 0 < finrank K { x // x ∈ ES }
h_dim_add : finrank K { x // x ∈ ER } + finrank K { x // x ∈ ES } = finrank K V
h_dim_ER : finrank K { x // x ∈ ER } < Nat.succ n
ih_ER : ⨆ (μ : K) (k : ℕ), ↑(generalizedEigenspace f' μ) k = ⊤
⊢ ⨆ (μ : K) (k : ℕ), ↑(generalizedEigenspace f μ) k = ⊤
[PROOFSTEP]
have ih_ER' : ⨆ (μ : K) (k : ℕ), (f'.generalizedEigenspace μ k).map ER.subtype = ER := by
  simp only [(Submodule.map_iSup _ _).symm, ih_ER, Submodule.map_subtype_top ER]
    -- Moreover, every generalized eigenspace of `f'` is contained in the corresponding generalized
        -- eigenspace of `f`.
[GOAL]
K : Type v
V✝ : Type w
inst✝⁷ : Field K
inst✝⁶ : AddCommGroup V✝
inst✝⁵ : Module K V✝
inst✝⁴ : IsAlgClosed K
inst✝³ : FiniteDimensional K V✝
f✝ : End K V✝
x✝ : ℕ
h_dim✝ : finrank K V✝ = x✝
V : Type w
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
n : ℕ
ih :
  ∀ (m : ℕ),
    m < Nat.succ n →
      ∀ {V : Type w} [inst : AddCommGroup V] [inst_1 : Module K V] [inst_2 : FiniteDimensional K V] (f : End K V),
        finrank K V = m → ⨆ (μ : K) (k : ℕ), ↑(generalizedEigenspace f μ) k = ⊤
h_dim : finrank K V = Nat.succ n
this : Nontrivial V
μ₀ : K
hμ₀ : HasEigenvalue f μ₀
ES : Submodule K V := ↑(generalizedEigenspace f μ₀) (finrank K V)
ER : Submodule K V := generalizedEigenrange f μ₀ (finrank K V)
h_f_ER : ∀ (x : V), x ∈ ER → ↑f x ∈ ER
f' : End K { x // x ∈ ER } := LinearMap.restrict f h_f_ER
h_dim_ES_pos : 0 < finrank K { x // x ∈ ES }
h_dim_add : finrank K { x // x ∈ ER } + finrank K { x // x ∈ ES } = finrank K V
h_dim_ER : finrank K { x // x ∈ ER } < Nat.succ n
ih_ER : ⨆ (μ : K) (k : ℕ), ↑(generalizedEigenspace f' μ) k = ⊤
⊢ ⨆ (μ : K) (k : ℕ), Submodule.map (Submodule.subtype ER) (↑(generalizedEigenspace f' μ) k) = ER
[PROOFSTEP]
simp only [(Submodule.map_iSup _ _).symm, ih_ER, Submodule.map_subtype_top ER]
  -- Moreover, every generalized eigenspace of `f'` is contained in the corresponding generalized
      -- eigenspace of `f`.
[GOAL]
case h.succ.intro
K : Type v
V✝ : Type w
inst✝⁷ : Field K
inst✝⁶ : AddCommGroup V✝
inst✝⁵ : Module K V✝
inst✝⁴ : IsAlgClosed K
inst✝³ : FiniteDimensional K V✝
f✝ : End K V✝
x✝ : ℕ
h_dim✝ : finrank K V✝ = x✝
V : Type w
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
n : ℕ
ih :
  ∀ (m : ℕ),
    m < Nat.succ n →
      ∀ {V : Type w} [inst : AddCommGroup V] [inst_1 : Module K V] [inst_2 : FiniteDimensional K V] (f : End K V),
        finrank K V = m → ⨆ (μ : K) (k : ℕ), ↑(generalizedEigenspace f μ) k = ⊤
h_dim : finrank K V = Nat.succ n
this : Nontrivial V
μ₀ : K
hμ₀ : HasEigenvalue f μ₀
ES : Submodule K V := ↑(generalizedEigenspace f μ₀) (finrank K V)
ER : Submodule K V := generalizedEigenrange f μ₀ (finrank K V)
h_f_ER : ∀ (x : V), x ∈ ER → ↑f x ∈ ER
f' : End K { x // x ∈ ER } := LinearMap.restrict f h_f_ER
h_dim_ES_pos : 0 < finrank K { x // x ∈ ES }
h_dim_add : finrank K { x // x ∈ ER } + finrank K { x // x ∈ ES } = finrank K V
h_dim_ER : finrank K { x // x ∈ ER } < Nat.succ n
ih_ER : ⨆ (μ : K) (k : ℕ), ↑(generalizedEigenspace f' μ) k = ⊤
ih_ER' : ⨆ (μ : K) (k : ℕ), Submodule.map (Submodule.subtype ER) (↑(generalizedEigenspace f' μ) k) = ER
⊢ ⨆ (μ : K) (k : ℕ), ↑(generalizedEigenspace f μ) k = ⊤
[PROOFSTEP]
have hff' : ∀ μ k, (f'.generalizedEigenspace μ k).map ER.subtype ≤ f.generalizedEigenspace μ k :=
  by
  intros
  rw [generalizedEigenspace_restrict]
  apply Submodule.map_comap_le
[GOAL]
K : Type v
V✝ : Type w
inst✝⁷ : Field K
inst✝⁶ : AddCommGroup V✝
inst✝⁵ : Module K V✝
inst✝⁴ : IsAlgClosed K
inst✝³ : FiniteDimensional K V✝
f✝ : End K V✝
x✝ : ℕ
h_dim✝ : finrank K V✝ = x✝
V : Type w
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
n : ℕ
ih :
  ∀ (m : ℕ),
    m < Nat.succ n →
      ∀ {V : Type w} [inst : AddCommGroup V] [inst_1 : Module K V] [inst_2 : FiniteDimensional K V] (f : End K V),
        finrank K V = m → ⨆ (μ : K) (k : ℕ), ↑(generalizedEigenspace f μ) k = ⊤
h_dim : finrank K V = Nat.succ n
this : Nontrivial V
μ₀ : K
hμ₀ : HasEigenvalue f μ₀
ES : Submodule K V := ↑(generalizedEigenspace f μ₀) (finrank K V)
ER : Submodule K V := generalizedEigenrange f μ₀ (finrank K V)
h_f_ER : ∀ (x : V), x ∈ ER → ↑f x ∈ ER
f' : End K { x // x ∈ ER } := LinearMap.restrict f h_f_ER
h_dim_ES_pos : 0 < finrank K { x // x ∈ ES }
h_dim_add : finrank K { x // x ∈ ER } + finrank K { x // x ∈ ES } = finrank K V
h_dim_ER : finrank K { x // x ∈ ER } < Nat.succ n
ih_ER : ⨆ (μ : K) (k : ℕ), ↑(generalizedEigenspace f' μ) k = ⊤
ih_ER' : ⨆ (μ : K) (k : ℕ), Submodule.map (Submodule.subtype ER) (↑(generalizedEigenspace f' μ) k) = ER
⊢ ∀ (μ : K) (k : ℕ),
    Submodule.map (Submodule.subtype ER) (↑(generalizedEigenspace f' μ) k) ≤ ↑(generalizedEigenspace f μ) k
[PROOFSTEP]
intros
[GOAL]
K : Type v
V✝ : Type w
inst✝⁷ : Field K
inst✝⁶ : AddCommGroup V✝
inst✝⁵ : Module K V✝
inst✝⁴ : IsAlgClosed K
inst✝³ : FiniteDimensional K V✝
f✝ : End K V✝
x✝ : ℕ
h_dim✝ : finrank K V✝ = x✝
V : Type w
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
n : ℕ
ih :
  ∀ (m : ℕ),
    m < Nat.succ n →
      ∀ {V : Type w} [inst : AddCommGroup V] [inst_1 : Module K V] [inst_2 : FiniteDimensional K V] (f : End K V),
        finrank K V = m → ⨆ (μ : K) (k : ℕ), ↑(generalizedEigenspace f μ) k = ⊤
h_dim : finrank K V = Nat.succ n
this : Nontrivial V
μ₀ : K
hμ₀ : HasEigenvalue f μ₀
ES : Submodule K V := ↑(generalizedEigenspace f μ₀) (finrank K V)
ER : Submodule K V := generalizedEigenrange f μ₀ (finrank K V)
h_f_ER : ∀ (x : V), x ∈ ER → ↑f x ∈ ER
f' : End K { x // x ∈ ER } := LinearMap.restrict f h_f_ER
h_dim_ES_pos : 0 < finrank K { x // x ∈ ES }
h_dim_add : finrank K { x // x ∈ ER } + finrank K { x // x ∈ ES } = finrank K V
h_dim_ER : finrank K { x // x ∈ ER } < Nat.succ n
ih_ER : ⨆ (μ : K) (k : ℕ), ↑(generalizedEigenspace f' μ) k = ⊤
ih_ER' : ⨆ (μ : K) (k : ℕ), Submodule.map (Submodule.subtype ER) (↑(generalizedEigenspace f' μ) k) = ER
μ✝ : K
k✝ : ℕ
⊢ Submodule.map (Submodule.subtype ER) (↑(generalizedEigenspace f' μ✝) k✝) ≤ ↑(generalizedEigenspace f μ✝) k✝
[PROOFSTEP]
rw [generalizedEigenspace_restrict]
[GOAL]
K : Type v
V✝ : Type w
inst✝⁷ : Field K
inst✝⁶ : AddCommGroup V✝
inst✝⁵ : Module K V✝
inst✝⁴ : IsAlgClosed K
inst✝³ : FiniteDimensional K V✝
f✝ : End K V✝
x✝ : ℕ
h_dim✝ : finrank K V✝ = x✝
V : Type w
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
n : ℕ
ih :
  ∀ (m : ℕ),
    m < Nat.succ n →
      ∀ {V : Type w} [inst : AddCommGroup V] [inst_1 : Module K V] [inst_2 : FiniteDimensional K V] (f : End K V),
        finrank K V = m → ⨆ (μ : K) (k : ℕ), ↑(generalizedEigenspace f μ) k = ⊤
h_dim : finrank K V = Nat.succ n
this : Nontrivial V
μ₀ : K
hμ₀ : HasEigenvalue f μ₀
ES : Submodule K V := ↑(generalizedEigenspace f μ₀) (finrank K V)
ER : Submodule K V := generalizedEigenrange f μ₀ (finrank K V)
h_f_ER : ∀ (x : V), x ∈ ER → ↑f x ∈ ER
f' : End K { x // x ∈ ER } := LinearMap.restrict f h_f_ER
h_dim_ES_pos : 0 < finrank K { x // x ∈ ES }
h_dim_add : finrank K { x // x ∈ ER } + finrank K { x // x ∈ ES } = finrank K V
h_dim_ER : finrank K { x // x ∈ ER } < Nat.succ n
ih_ER : ⨆ (μ : K) (k : ℕ), ↑(generalizedEigenspace f' μ) k = ⊤
ih_ER' : ⨆ (μ : K) (k : ℕ), Submodule.map (Submodule.subtype ER) (↑(generalizedEigenspace f' μ) k) = ER
μ✝ : K
k✝ : ℕ
⊢ Submodule.map (Submodule.subtype ER) (Submodule.comap (Submodule.subtype ER) (↑(generalizedEigenspace f μ✝) k✝)) ≤
    ↑(generalizedEigenspace f μ✝) k✝
[PROOFSTEP]
apply Submodule.map_comap_le
[GOAL]
case h.succ.intro
K : Type v
V✝ : Type w
inst✝⁷ : Field K
inst✝⁶ : AddCommGroup V✝
inst✝⁵ : Module K V✝
inst✝⁴ : IsAlgClosed K
inst✝³ : FiniteDimensional K V✝
f✝ : End K V✝
x✝ : ℕ
h_dim✝ : finrank K V✝ = x✝
V : Type w
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
n : ℕ
ih :
  ∀ (m : ℕ),
    m < Nat.succ n →
      ∀ {V : Type w} [inst : AddCommGroup V] [inst_1 : Module K V] [inst_2 : FiniteDimensional K V] (f : End K V),
        finrank K V = m → ⨆ (μ : K) (k : ℕ), ↑(generalizedEigenspace f μ) k = ⊤
h_dim : finrank K V = Nat.succ n
this : Nontrivial V
μ₀ : K
hμ₀ : HasEigenvalue f μ₀
ES : Submodule K V := ↑(generalizedEigenspace f μ₀) (finrank K V)
ER : Submodule K V := generalizedEigenrange f μ₀ (finrank K V)
h_f_ER : ∀ (x : V), x ∈ ER → ↑f x ∈ ER
f' : End K { x // x ∈ ER } := LinearMap.restrict f h_f_ER
h_dim_ES_pos : 0 < finrank K { x // x ∈ ES }
h_dim_add : finrank K { x // x ∈ ER } + finrank K { x // x ∈ ES } = finrank K V
h_dim_ER : finrank K { x // x ∈ ER } < Nat.succ n
ih_ER : ⨆ (μ : K) (k : ℕ), ↑(generalizedEigenspace f' μ) k = ⊤
ih_ER' : ⨆ (μ : K) (k : ℕ), Submodule.map (Submodule.subtype ER) (↑(generalizedEigenspace f' μ) k) = ER
hff' :
  ∀ (μ : K) (k : ℕ),
    Submodule.map (Submodule.subtype ER) (↑(generalizedEigenspace f' μ) k) ≤ ↑(generalizedEigenspace f μ) k
⊢ ⨆ (μ : K) (k : ℕ), ↑(generalizedEigenspace f μ) k = ⊤
[PROOFSTEP]
have hER : ER ≤ ⨆ (μ : K) (k : ℕ), f.generalizedEigenspace μ k :=
  by
  rw [← ih_ER']
  exact iSup₂_mono hff'
[GOAL]
K : Type v
V✝ : Type w
inst✝⁷ : Field K
inst✝⁶ : AddCommGroup V✝
inst✝⁵ : Module K V✝
inst✝⁴ : IsAlgClosed K
inst✝³ : FiniteDimensional K V✝
f✝ : End K V✝
x✝ : ℕ
h_dim✝ : finrank K V✝ = x✝
V : Type w
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
n : ℕ
ih :
  ∀ (m : ℕ),
    m < Nat.succ n →
      ∀ {V : Type w} [inst : AddCommGroup V] [inst_1 : Module K V] [inst_2 : FiniteDimensional K V] (f : End K V),
        finrank K V = m → ⨆ (μ : K) (k : ℕ), ↑(generalizedEigenspace f μ) k = ⊤
h_dim : finrank K V = Nat.succ n
this : Nontrivial V
μ₀ : K
hμ₀ : HasEigenvalue f μ₀
ES : Submodule K V := ↑(generalizedEigenspace f μ₀) (finrank K V)
ER : Submodule K V := generalizedEigenrange f μ₀ (finrank K V)
h_f_ER : ∀ (x : V), x ∈ ER → ↑f x ∈ ER
f' : End K { x // x ∈ ER } := LinearMap.restrict f h_f_ER
h_dim_ES_pos : 0 < finrank K { x // x ∈ ES }
h_dim_add : finrank K { x // x ∈ ER } + finrank K { x // x ∈ ES } = finrank K V
h_dim_ER : finrank K { x // x ∈ ER } < Nat.succ n
ih_ER : ⨆ (μ : K) (k : ℕ), ↑(generalizedEigenspace f' μ) k = ⊤
ih_ER' : ⨆ (μ : K) (k : ℕ), Submodule.map (Submodule.subtype ER) (↑(generalizedEigenspace f' μ) k) = ER
hff' :
  ∀ (μ : K) (k : ℕ),
    Submodule.map (Submodule.subtype ER) (↑(generalizedEigenspace f' μ) k) ≤ ↑(generalizedEigenspace f μ) k
⊢ ER ≤ ⨆ (μ : K) (k : ℕ), ↑(generalizedEigenspace f μ) k
[PROOFSTEP]
rw [← ih_ER']
[GOAL]
K : Type v
V✝ : Type w
inst✝⁷ : Field K
inst✝⁶ : AddCommGroup V✝
inst✝⁵ : Module K V✝
inst✝⁴ : IsAlgClosed K
inst✝³ : FiniteDimensional K V✝
f✝ : End K V✝
x✝ : ℕ
h_dim✝ : finrank K V✝ = x✝
V : Type w
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
n : ℕ
ih :
  ∀ (m : ℕ),
    m < Nat.succ n →
      ∀ {V : Type w} [inst : AddCommGroup V] [inst_1 : Module K V] [inst_2 : FiniteDimensional K V] (f : End K V),
        finrank K V = m → ⨆ (μ : K) (k : ℕ), ↑(generalizedEigenspace f μ) k = ⊤
h_dim : finrank K V = Nat.succ n
this : Nontrivial V
μ₀ : K
hμ₀ : HasEigenvalue f μ₀
ES : Submodule K V := ↑(generalizedEigenspace f μ₀) (finrank K V)
ER : Submodule K V := generalizedEigenrange f μ₀ (finrank K V)
h_f_ER : ∀ (x : V), x ∈ ER → ↑f x ∈ ER
f' : End K { x // x ∈ ER } := LinearMap.restrict f h_f_ER
h_dim_ES_pos : 0 < finrank K { x // x ∈ ES }
h_dim_add : finrank K { x // x ∈ ER } + finrank K { x // x ∈ ES } = finrank K V
h_dim_ER : finrank K { x // x ∈ ER } < Nat.succ n
ih_ER : ⨆ (μ : K) (k : ℕ), ↑(generalizedEigenspace f' μ) k = ⊤
ih_ER' : ⨆ (μ : K) (k : ℕ), Submodule.map (Submodule.subtype ER) (↑(generalizedEigenspace f' μ) k) = ER
hff' :
  ∀ (μ : K) (k : ℕ),
    Submodule.map (Submodule.subtype ER) (↑(generalizedEigenspace f' μ) k) ≤ ↑(generalizedEigenspace f μ) k
⊢ ⨆ (μ : K) (k : ℕ), Submodule.map (Submodule.subtype ER) (↑(generalizedEigenspace f' μ) k) ≤
    ⨆ (μ : K) (k : ℕ), ↑(generalizedEigenspace f μ) k
[PROOFSTEP]
exact iSup₂_mono hff'
[GOAL]
case h.succ.intro
K : Type v
V✝ : Type w
inst✝⁷ : Field K
inst✝⁶ : AddCommGroup V✝
inst✝⁵ : Module K V✝
inst✝⁴ : IsAlgClosed K
inst✝³ : FiniteDimensional K V✝
f✝ : End K V✝
x✝ : ℕ
h_dim✝ : finrank K V✝ = x✝
V : Type w
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
n : ℕ
ih :
  ∀ (m : ℕ),
    m < Nat.succ n →
      ∀ {V : Type w} [inst : AddCommGroup V] [inst_1 : Module K V] [inst_2 : FiniteDimensional K V] (f : End K V),
        finrank K V = m → ⨆ (μ : K) (k : ℕ), ↑(generalizedEigenspace f μ) k = ⊤
h_dim : finrank K V = Nat.succ n
this : Nontrivial V
μ₀ : K
hμ₀ : HasEigenvalue f μ₀
ES : Submodule K V := ↑(generalizedEigenspace f μ₀) (finrank K V)
ER : Submodule K V := generalizedEigenrange f μ₀ (finrank K V)
h_f_ER : ∀ (x : V), x ∈ ER → ↑f x ∈ ER
f' : End K { x // x ∈ ER } := LinearMap.restrict f h_f_ER
h_dim_ES_pos : 0 < finrank K { x // x ∈ ES }
h_dim_add : finrank K { x // x ∈ ER } + finrank K { x // x ∈ ES } = finrank K V
h_dim_ER : finrank K { x // x ∈ ER } < Nat.succ n
ih_ER : ⨆ (μ : K) (k : ℕ), ↑(generalizedEigenspace f' μ) k = ⊤
ih_ER' : ⨆ (μ : K) (k : ℕ), Submodule.map (Submodule.subtype ER) (↑(generalizedEigenspace f' μ) k) = ER
hff' :
  ∀ (μ : K) (k : ℕ),
    Submodule.map (Submodule.subtype ER) (↑(generalizedEigenspace f' μ) k) ≤ ↑(generalizedEigenspace f μ) k
hER : ER ≤ ⨆ (μ : K) (k : ℕ), ↑(generalizedEigenspace f μ) k
⊢ ⨆ (μ : K) (k : ℕ), ↑(generalizedEigenspace f μ) k = ⊤
[PROOFSTEP]
have hES : ES ≤ ⨆ (μ : K) (k : ℕ), f.generalizedEigenspace μ k :=
  le_trans (le_iSup (fun k => f.generalizedEigenspace μ₀ k) (finrank K V))
    (le_iSup (fun μ : K => ⨆ k : ℕ, f.generalizedEigenspace μ k) μ₀)
      -- Moreover, we know that `ER` and `ES` are disjoint.
[GOAL]
case h.succ.intro
K : Type v
V✝ : Type w
inst✝⁷ : Field K
inst✝⁶ : AddCommGroup V✝
inst✝⁵ : Module K V✝
inst✝⁴ : IsAlgClosed K
inst✝³ : FiniteDimensional K V✝
f✝ : End K V✝
x✝ : ℕ
h_dim✝ : finrank K V✝ = x✝
V : Type w
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
n : ℕ
ih :
  ∀ (m : ℕ),
    m < Nat.succ n →
      ∀ {V : Type w} [inst : AddCommGroup V] [inst_1 : Module K V] [inst_2 : FiniteDimensional K V] (f : End K V),
        finrank K V = m → ⨆ (μ : K) (k : ℕ), ↑(generalizedEigenspace f μ) k = ⊤
h_dim : finrank K V = Nat.succ n
this : Nontrivial V
μ₀ : K
hμ₀ : HasEigenvalue f μ₀
ES : Submodule K V := ↑(generalizedEigenspace f μ₀) (finrank K V)
ER : Submodule K V := generalizedEigenrange f μ₀ (finrank K V)
h_f_ER : ∀ (x : V), x ∈ ER → ↑f x ∈ ER
f' : End K { x // x ∈ ER } := LinearMap.restrict f h_f_ER
h_dim_ES_pos : 0 < finrank K { x // x ∈ ES }
h_dim_add : finrank K { x // x ∈ ER } + finrank K { x // x ∈ ES } = finrank K V
h_dim_ER : finrank K { x // x ∈ ER } < Nat.succ n
ih_ER : ⨆ (μ : K) (k : ℕ), ↑(generalizedEigenspace f' μ) k = ⊤
ih_ER' : ⨆ (μ : K) (k : ℕ), Submodule.map (Submodule.subtype ER) (↑(generalizedEigenspace f' μ) k) = ER
hff' :
  ∀ (μ : K) (k : ℕ),
    Submodule.map (Submodule.subtype ER) (↑(generalizedEigenspace f' μ) k) ≤ ↑(generalizedEigenspace f μ) k
hER : ER ≤ ⨆ (μ : K) (k : ℕ), ↑(generalizedEigenspace f μ) k
hES : ES ≤ ⨆ (μ : K) (k : ℕ), ↑(generalizedEigenspace f μ) k
⊢ ⨆ (μ : K) (k : ℕ), ↑(generalizedEigenspace f μ) k = ⊤
[PROOFSTEP]
have h_disjoint : Disjoint ER ES := generalized_eigenvec_disjoint_range_ker f μ₀
[GOAL]
case h.succ.intro
K : Type v
V✝ : Type w
inst✝⁷ : Field K
inst✝⁶ : AddCommGroup V✝
inst✝⁵ : Module K V✝
inst✝⁴ : IsAlgClosed K
inst✝³ : FiniteDimensional K V✝
f✝ : End K V✝
x✝ : ℕ
h_dim✝ : finrank K V✝ = x✝
V : Type w
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
n : ℕ
ih :
  ∀ (m : ℕ),
    m < Nat.succ n →
      ∀ {V : Type w} [inst : AddCommGroup V] [inst_1 : Module K V] [inst_2 : FiniteDimensional K V] (f : End K V),
        finrank K V = m → ⨆ (μ : K) (k : ℕ), ↑(generalizedEigenspace f μ) k = ⊤
h_dim : finrank K V = Nat.succ n
this : Nontrivial V
μ₀ : K
hμ₀ : HasEigenvalue f μ₀
ES : Submodule K V := ↑(generalizedEigenspace f μ₀) (finrank K V)
ER : Submodule K V := generalizedEigenrange f μ₀ (finrank K V)
h_f_ER : ∀ (x : V), x ∈ ER → ↑f x ∈ ER
f' : End K { x // x ∈ ER } := LinearMap.restrict f h_f_ER
h_dim_ES_pos : 0 < finrank K { x // x ∈ ES }
h_dim_add : finrank K { x // x ∈ ER } + finrank K { x // x ∈ ES } = finrank K V
h_dim_ER : finrank K { x // x ∈ ER } < Nat.succ n
ih_ER : ⨆ (μ : K) (k : ℕ), ↑(generalizedEigenspace f' μ) k = ⊤
ih_ER' : ⨆ (μ : K) (k : ℕ), Submodule.map (Submodule.subtype ER) (↑(generalizedEigenspace f' μ) k) = ER
hff' :
  ∀ (μ : K) (k : ℕ),
    Submodule.map (Submodule.subtype ER) (↑(generalizedEigenspace f' μ) k) ≤ ↑(generalizedEigenspace f μ) k
hER : ER ≤ ⨆ (μ : K) (k : ℕ), ↑(generalizedEigenspace f μ) k
hES : ES ≤ ⨆ (μ : K) (k : ℕ), ↑(generalizedEigenspace f μ) k
h_disjoint : Disjoint ER ES
⊢ ⨆ (μ : K) (k : ℕ), ↑(generalizedEigenspace f μ) k = ⊤
[PROOFSTEP]
show ⨆ (μ : K) (k : ℕ), f.generalizedEigenspace μ k = ⊤
[GOAL]
case h.succ.intro
K : Type v
V✝ : Type w
inst✝⁷ : Field K
inst✝⁶ : AddCommGroup V✝
inst✝⁵ : Module K V✝
inst✝⁴ : IsAlgClosed K
inst✝³ : FiniteDimensional K V✝
f✝ : End K V✝
x✝ : ℕ
h_dim✝ : finrank K V✝ = x✝
V : Type w
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
n : ℕ
ih :
  ∀ (m : ℕ),
    m < Nat.succ n →
      ∀ {V : Type w} [inst : AddCommGroup V] [inst_1 : Module K V] [inst_2 : FiniteDimensional K V] (f : End K V),
        finrank K V = m → ⨆ (μ : K) (k : ℕ), ↑(generalizedEigenspace f μ) k = ⊤
h_dim : finrank K V = Nat.succ n
this : Nontrivial V
μ₀ : K
hμ₀ : HasEigenvalue f μ₀
ES : Submodule K V := ↑(generalizedEigenspace f μ₀) (finrank K V)
ER : Submodule K V := generalizedEigenrange f μ₀ (finrank K V)
h_f_ER : ∀ (x : V), x ∈ ER → ↑f x ∈ ER
f' : End K { x // x ∈ ER } := LinearMap.restrict f h_f_ER
h_dim_ES_pos : 0 < finrank K { x // x ∈ ES }
h_dim_add : finrank K { x // x ∈ ER } + finrank K { x // x ∈ ES } = finrank K V
h_dim_ER : finrank K { x // x ∈ ER } < Nat.succ n
ih_ER : ⨆ (μ : K) (k : ℕ), ↑(generalizedEigenspace f' μ) k = ⊤
ih_ER' : ⨆ (μ : K) (k : ℕ), Submodule.map (Submodule.subtype ER) (↑(generalizedEigenspace f' μ) k) = ER
hff' :
  ∀ (μ : K) (k : ℕ),
    Submodule.map (Submodule.subtype ER) (↑(generalizedEigenspace f' μ) k) ≤ ↑(generalizedEigenspace f μ) k
hER : ER ≤ ⨆ (μ : K) (k : ℕ), ↑(generalizedEigenspace f μ) k
hES : ES ≤ ⨆ (μ : K) (k : ℕ), ↑(generalizedEigenspace f μ) k
h_disjoint : Disjoint ER ES
⊢ ⨆ (μ : K) (k : ℕ), ↑(generalizedEigenspace f μ) k = ⊤
[PROOFSTEP]
rw [← top_le_iff, ← Submodule.eq_top_of_disjoint ER ES h_dim_add h_disjoint]
[GOAL]
case h.succ.intro
K : Type v
V✝ : Type w
inst✝⁷ : Field K
inst✝⁶ : AddCommGroup V✝
inst✝⁵ : Module K V✝
inst✝⁴ : IsAlgClosed K
inst✝³ : FiniteDimensional K V✝
f✝ : End K V✝
x✝ : ℕ
h_dim✝ : finrank K V✝ = x✝
V : Type w
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
f : End K V
n : ℕ
ih :
  ∀ (m : ℕ),
    m < Nat.succ n →
      ∀ {V : Type w} [inst : AddCommGroup V] [inst_1 : Module K V] [inst_2 : FiniteDimensional K V] (f : End K V),
        finrank K V = m → ⨆ (μ : K) (k : ℕ), ↑(generalizedEigenspace f μ) k = ⊤
h_dim : finrank K V = Nat.succ n
this : Nontrivial V
μ₀ : K
hμ₀ : HasEigenvalue f μ₀
ES : Submodule K V := ↑(generalizedEigenspace f μ₀) (finrank K V)
ER : Submodule K V := generalizedEigenrange f μ₀ (finrank K V)
h_f_ER : ∀ (x : V), x ∈ ER → ↑f x ∈ ER
f' : End K { x // x ∈ ER } := LinearMap.restrict f h_f_ER
h_dim_ES_pos : 0 < finrank K { x // x ∈ ES }
h_dim_add : finrank K { x // x ∈ ER } + finrank K { x // x ∈ ES } = finrank K V
h_dim_ER : finrank K { x // x ∈ ER } < Nat.succ n
ih_ER : ⨆ (μ : K) (k : ℕ), ↑(generalizedEigenspace f' μ) k = ⊤
ih_ER' : ⨆ (μ : K) (k : ℕ), Submodule.map (Submodule.subtype ER) (↑(generalizedEigenspace f' μ) k) = ER
hff' :
  ∀ (μ : K) (k : ℕ),
    Submodule.map (Submodule.subtype ER) (↑(generalizedEigenspace f' μ) k) ≤ ↑(generalizedEigenspace f μ) k
hER : ER ≤ ⨆ (μ : K) (k : ℕ), ↑(generalizedEigenspace f μ) k
hES : ES ≤ ⨆ (μ : K) (k : ℕ), ↑(generalizedEigenspace f μ) k
h_disjoint : Disjoint ER ES
⊢ ER ⊔ ES ≤ ⨆ (μ : K) (k : ℕ), ↑(generalizedEigenspace f μ) k
[PROOFSTEP]
apply sup_le hER hES


[GOAL]
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
m : M
⊢ ↑(ι R) m ∈ LinearMap.range (ι R) ^ 1
[PROOFSTEP]
simpa only [pow_one] using LinearMap.mem_range_self _ m
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
m : M
⊢ ↑(ι R) m ∈ LinearMap.range (ι R) ^ 1
[PROOFSTEP]
simpa only [pow_one] using LinearMap.mem_range_self _ m
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
m : M
⊢ ↑(GradedAlgebra.ι R M) m * ↑(GradedAlgebra.ι R M) m = 0
[PROOFSTEP]
rw [GradedAlgebra.ι_apply, DirectSum.of_mul_of]
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
m : M
⊢ ↑(DirectSum.of (fun i => { x // x ∈ LinearMap.range (ι R) ^ i }) (1 + 1))
      (GradedMonoid.GMul.mul { val := ↑(ι R) m, property := (_ : ↑(ι R) m ∈ LinearMap.range (ι R) ^ 1) }
        { val := ↑(ι R) m, property := (_ : ↑(ι R) m ∈ LinearMap.range (ι R) ^ 1) }) =
    0
[PROOFSTEP]
refine DFinsupp.single_eq_zero.mpr (Subtype.ext <| ExteriorAlgebra.ι_sq_zero _)
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
⊢ M →ₗ[R] ⨁ (i : ℕ), { x // x ∈ LinearMap.range (ι R) ^ i }
[PROOFSTEP]
apply GradedAlgebra.ι R M
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
i : ℕ
x : { x // x ∈ LinearMap.range (ι R) ^ i }
⊢ ↑(liftι R M) ↑x = ↑(DirectSum.of (fun i => { x // x ∈ LinearMap.range (ι R) ^ i }) i) x
[PROOFSTEP]
cases' x with x hx
[GOAL]
case mk
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
i : ℕ
x : ExteriorAlgebra R M
hx : x ∈ LinearMap.range (ι R) ^ i
⊢ ↑(liftι R M) ↑{ val := x, property := hx } =
    ↑(DirectSum.of (fun i => { x // x ∈ LinearMap.range (ι R) ^ i }) i) { val := x, property := hx }
[PROOFSTEP]
dsimp only [Subtype.coe_mk, DirectSum.lof_eq_of]
  -- Porting note: original statement was
    --  refine Submodule.pow_induction_on_left' _ (fun r => ?_) (fun x y i hx hy ihx ihy => ?_)
    --    (fun m hm i x hx ih => ?_) hx
    -- but it created invalid goals
[GOAL]
case mk
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
i : ℕ
x : ExteriorAlgebra R M
hx : x ∈ LinearMap.range (ι R) ^ i
⊢ ↑(liftι R M) x = ↑(DirectSum.of (fun i => { x // x ∈ LinearMap.range (ι R) ^ i }) i) { val := x, property := hx }
[PROOFSTEP]
induction hx using Submodule.pow_induction_on_left' with
| hr => simp_rw [AlgHom.commutes, DirectSum.algebraMap_apply]; rfl
| hadd _ _ _ _ _ ihx ihy => simp_rw [AlgHom.map_add, ihx, ihy, ← map_add]; rfl
| hmul _ hm _ _ _ ih =>
  obtain ⟨_, rfl⟩ := hm
  simp_rw [AlgHom.map_mul, ih, GradedAlgebra.liftι, lift_ι_apply, GradedAlgebra.ι_apply R M, DirectSum.of_mul_of]
  exact DirectSum.of_eq_of_gradedMonoid_eq (Sigma.subtype_ext (add_comm _ _) rfl)
[GOAL]
case mk
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
i : ℕ
x : ExteriorAlgebra R M
hx : x ∈ LinearMap.range (ι R) ^ i
⊢ ↑(liftι R M) x = ↑(DirectSum.of (fun i => { x // x ∈ LinearMap.range (ι R) ^ i }) i) { val := x, property := hx }
[PROOFSTEP]
induction hx using Submodule.pow_induction_on_left' with
| hr => simp_rw [AlgHom.commutes, DirectSum.algebraMap_apply]; rfl
| hadd _ _ _ _ _ ihx ihy => simp_rw [AlgHom.map_add, ihx, ihy, ← map_add]; rfl
| hmul _ hm _ _ _ ih =>
  obtain ⟨_, rfl⟩ := hm
  simp_rw [AlgHom.map_mul, ih, GradedAlgebra.liftι, lift_ι_apply, GradedAlgebra.ι_apply R M, DirectSum.of_mul_of]
  exact DirectSum.of_eq_of_gradedMonoid_eq (Sigma.subtype_ext (add_comm _ _) rfl)
[GOAL]
case mk.hr
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
i : ℕ
x : ExteriorAlgebra R M
r✝ : R
⊢ ↑(liftι R M) (↑(algebraMap R (ExteriorAlgebra R M)) r✝) =
    ↑(DirectSum.of (fun i => { x // x ∈ LinearMap.range (ι R) ^ i }) 0)
      { val := ↑(algebraMap R (ExteriorAlgebra R M)) r✝,
        property := (_ : ↑(algebraMap R (ExteriorAlgebra R M)) r✝ ∈ 1) }
[PROOFSTEP]

| hr => simp_rw [AlgHom.commutes, DirectSum.algebraMap_apply]; rfl
[GOAL]
case mk.hr
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
i : ℕ
x : ExteriorAlgebra R M
r✝ : R
⊢ ↑(liftι R M) (↑(algebraMap R (ExteriorAlgebra R M)) r✝) =
    ↑(DirectSum.of (fun i => { x // x ∈ LinearMap.range (ι R) ^ i }) 0)
      { val := ↑(algebraMap R (ExteriorAlgebra R M)) r✝,
        property := (_ : ↑(algebraMap R (ExteriorAlgebra R M)) r✝ ∈ 1) }
[PROOFSTEP]
simp_rw [AlgHom.commutes, DirectSum.algebraMap_apply]
[GOAL]
case mk.hr
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
i : ℕ
x : ExteriorAlgebra R M
r✝ : R
⊢ ↑(DirectSum.of (fun i => { x // x ∈ LinearMap.range (ι R) ^ i }) 0) (↑DirectSum.GAlgebra.toFun r✝) =
    ↑(DirectSum.of (fun i => { x // x ∈ LinearMap.range (ι R) ^ i }) 0)
      { val := ↑(algebraMap R (ExteriorAlgebra R M)) r✝,
        property := (_ : ↑(algebraMap R (ExteriorAlgebra R M)) r✝ ∈ 1) }
[PROOFSTEP]
rfl
[GOAL]
case mk.hadd
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
i : ℕ
x x✝ y✝ : ExteriorAlgebra R M
i✝ : ℕ
hx✝ : x✝ ∈ LinearMap.range (ι R) ^ i✝
hy✝ : y✝ ∈ LinearMap.range (ι R) ^ i✝
ihx :
  ↑(liftι R M) x✝ = ↑(DirectSum.of (fun i => { x // x ∈ LinearMap.range (ι R) ^ i }) i✝) { val := x✝, property := hx✝ }
ihy :
  ↑(liftι R M) y✝ = ↑(DirectSum.of (fun i => { x // x ∈ LinearMap.range (ι R) ^ i }) i✝) { val := y✝, property := hy✝ }
⊢ ↑(liftι R M) (x✝ + y✝) =
    ↑(DirectSum.of (fun i => { x // x ∈ LinearMap.range (ι R) ^ i }) i✝)
      { val := x✝ + y✝, property := (_ : x✝ + y✝ ∈ LinearMap.range (ι R) ^ i✝) }
[PROOFSTEP]

| hadd _ _ _ _ _ ihx ihy => simp_rw [AlgHom.map_add, ihx, ihy, ← map_add]; rfl
[GOAL]
case mk.hadd
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
i : ℕ
x x✝ y✝ : ExteriorAlgebra R M
i✝ : ℕ
hx✝ : x✝ ∈ LinearMap.range (ι R) ^ i✝
hy✝ : y✝ ∈ LinearMap.range (ι R) ^ i✝
ihx :
  ↑(liftι R M) x✝ = ↑(DirectSum.of (fun i => { x // x ∈ LinearMap.range (ι R) ^ i }) i✝) { val := x✝, property := hx✝ }
ihy :
  ↑(liftι R M) y✝ = ↑(DirectSum.of (fun i => { x // x ∈ LinearMap.range (ι R) ^ i }) i✝) { val := y✝, property := hy✝ }
⊢ ↑(liftι R M) (x✝ + y✝) =
    ↑(DirectSum.of (fun i => { x // x ∈ LinearMap.range (ι R) ^ i }) i✝)
      { val := x✝ + y✝, property := (_ : x✝ + y✝ ∈ LinearMap.range (ι R) ^ i✝) }
[PROOFSTEP]
simp_rw [AlgHom.map_add, ihx, ihy, ← map_add]
[GOAL]
case mk.hadd
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
i : ℕ
x x✝ y✝ : ExteriorAlgebra R M
i✝ : ℕ
hx✝ : x✝ ∈ LinearMap.range (ι R) ^ i✝
hy✝ : y✝ ∈ LinearMap.range (ι R) ^ i✝
ihx :
  ↑(liftι R M) x✝ = ↑(DirectSum.of (fun i => { x // x ∈ LinearMap.range (ι R) ^ i }) i✝) { val := x✝, property := hx✝ }
ihy :
  ↑(liftι R M) y✝ = ↑(DirectSum.of (fun i => { x // x ∈ LinearMap.range (ι R) ^ i }) i✝) { val := y✝, property := hy✝ }
⊢ ↑(DirectSum.of (fun i => { x // x ∈ LinearMap.range (ι R) ^ i }) i✝)
      ({ val := x✝, property := hx✝ } + { val := y✝, property := hy✝ }) =
    ↑(DirectSum.of (fun i => { x // x ∈ LinearMap.range (ι R) ^ i }) i✝)
      { val := x✝ + y✝, property := (_ : x✝ + y✝ ∈ LinearMap.range (ι R) ^ i✝) }
[PROOFSTEP]
rfl
[GOAL]
case mk.hmul
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
i : ℕ
x m✝ : ExteriorAlgebra R M
hm : m✝ ∈ LinearMap.range (ι R)
i✝ : ℕ
x✝ : ExteriorAlgebra R M
hx✝ : x✝ ∈ LinearMap.range (ι R) ^ i✝
ih :
  ↑(liftι R M) x✝ = ↑(DirectSum.of (fun i => { x // x ∈ LinearMap.range (ι R) ^ i }) i✝) { val := x✝, property := hx✝ }
⊢ ↑(liftι R M) (m✝ * x✝) =
    ↑(DirectSum.of (fun i => { x // x ∈ LinearMap.range (ι R) ^ i }) (Nat.succ i✝))
      { val := m✝ * x✝, property := (_ : m✝ * x✝ ∈ LinearMap.range (ι R) * npowRec i✝ (LinearMap.range (ι R))) }
[PROOFSTEP]

| hmul _ hm _ _ _ ih =>
  obtain ⟨_, rfl⟩ := hm
  simp_rw [AlgHom.map_mul, ih, GradedAlgebra.liftι, lift_ι_apply, GradedAlgebra.ι_apply R M, DirectSum.of_mul_of]
  exact DirectSum.of_eq_of_gradedMonoid_eq (Sigma.subtype_ext (add_comm _ _) rfl)
[GOAL]
case mk.hmul
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
i : ℕ
x m✝ : ExteriorAlgebra R M
hm : m✝ ∈ LinearMap.range (ι R)
i✝ : ℕ
x✝ : ExteriorAlgebra R M
hx✝ : x✝ ∈ LinearMap.range (ι R) ^ i✝
ih :
  ↑(liftι R M) x✝ = ↑(DirectSum.of (fun i => { x // x ∈ LinearMap.range (ι R) ^ i }) i✝) { val := x✝, property := hx✝ }
⊢ ↑(liftι R M) (m✝ * x✝) =
    ↑(DirectSum.of (fun i => { x // x ∈ LinearMap.range (ι R) ^ i }) (Nat.succ i✝))
      { val := m✝ * x✝, property := (_ : m✝ * x✝ ∈ LinearMap.range (ι R) * npowRec i✝ (LinearMap.range (ι R))) }
[PROOFSTEP]
obtain ⟨_, rfl⟩ := hm
[GOAL]
case mk.hmul.intro
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
i : ℕ
x : ExteriorAlgebra R M
i✝ : ℕ
x✝ : ExteriorAlgebra R M
hx✝ : x✝ ∈ LinearMap.range (ι R) ^ i✝
ih :
  ↑(liftι R M) x✝ = ↑(DirectSum.of (fun i => { x // x ∈ LinearMap.range (ι R) ^ i }) i✝) { val := x✝, property := hx✝ }
w✝ : M
⊢ ↑(liftι R M) (↑(ι R) w✝ * x✝) =
    ↑(DirectSum.of (fun i => { x // x ∈ LinearMap.range (ι R) ^ i }) (Nat.succ i✝))
      { val := ↑(ι R) w✝ * x✝,
        property := (_ : ↑(ι R) w✝ * x✝ ∈ LinearMap.range (ι R) * npowRec i✝ (LinearMap.range (ι R))) }
[PROOFSTEP]
simp_rw [AlgHom.map_mul, ih, GradedAlgebra.liftι, lift_ι_apply, GradedAlgebra.ι_apply R M, DirectSum.of_mul_of]
[GOAL]
case mk.hmul.intro
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
i : ℕ
x : ExteriorAlgebra R M
i✝ : ℕ
x✝ : ExteriorAlgebra R M
hx✝ : x✝ ∈ LinearMap.range (ι R) ^ i✝
ih :
  ↑(liftι R M) x✝ = ↑(DirectSum.of (fun i => { x // x ∈ LinearMap.range (ι R) ^ i }) i✝) { val := x✝, property := hx✝ }
w✝ : M
⊢ ↑(DirectSum.of (fun i => { x // x ∈ LinearMap.range (ι R) ^ i }) (1 + i✝))
      (GradedMonoid.GMul.mul { val := ↑(ι R) w✝, property := (_ : ↑(ι R) w✝ ∈ LinearMap.range (ι R) ^ 1) }
        { val := x✝, property := hx✝ }) =
    ↑(DirectSum.of (fun i => { x // x ∈ LinearMap.range (ι R) ^ i }) (Nat.succ i✝))
      { val := ↑(ι R) w✝ * x✝,
        property := (_ : ↑(ι R) w✝ * x✝ ∈ LinearMap.range (ι R) * npowRec i✝ (LinearMap.range (ι R))) }
[PROOFSTEP]
exact DirectSum.of_eq_of_gradedMonoid_eq (Sigma.subtype_ext (add_comm _ _) rfl)
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
⊢ ExteriorAlgebra R M →ₐ[R] ⨁ (i : ℕ), { x // x ∈ LinearMap.range (ι R) ^ i }
[PROOFSTEP]
apply GradedAlgebra.liftι R M
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
⊢ AlgHom.comp (DirectSum.coeAlgHom fun x => LinearMap.range (ι R) ^ x) (GradedAlgebra.liftι R M) =
    AlgHom.id R (ExteriorAlgebra R M)
[PROOFSTEP]
ext m
[GOAL]
case a.h
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
m : M
⊢ ↑(LinearMap.comp
          (AlgHom.toLinearMap
            (AlgHom.comp (DirectSum.coeAlgHom fun x => LinearMap.range (ι R) ^ x) (GradedAlgebra.liftι R M)))
          (CliffordAlgebra.ι 0))
      m =
    ↑(LinearMap.comp (AlgHom.toLinearMap (AlgHom.id R (ExteriorAlgebra R M))) (CliffordAlgebra.ι 0)) m
[PROOFSTEP]
dsimp only [LinearMap.comp_apply, AlgHom.toLinearMap_apply, AlgHom.comp_apply, AlgHom.id_apply, GradedAlgebra.liftι]
[GOAL]
case a.h
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
m : M
⊢ ↑(DirectSum.coeAlgHom fun x => LinearMap.range (ι R) ^ x)
      (↑(↑(lift R)
            { val := GradedAlgebra.ι R M,
              property := (_ : ∀ (m : M), ↑(GradedAlgebra.ι R M) m * ↑(GradedAlgebra.ι R M) m = 0) })
        (↑(CliffordAlgebra.ι 0) m)) =
    ↑(CliffordAlgebra.ι 0) m
[PROOFSTEP]
rw [lift_ι_apply, GradedAlgebra.ι_apply R M, DirectSum.coeAlgHom_of, Subtype.coe_mk]
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
⊢ ∀ (i : ℕ) (x : { x // x ∈ LinearMap.range (ι R) ^ i }),
    ↑(GradedAlgebra.liftι R M) ↑x = ↑(DirectSum.of (fun i => { x // x ∈ LinearMap.range (ι R) ^ i }) i) x
[PROOFSTEP]
apply GradedAlgebra.liftι_eq R M