[GOAL]
R : Type u1
inst✝⁴ : CommRing R
M : Type u2
inst✝³ : AddCommGroup M
inst✝² : Module R M
A : Type u_1
inst✝¹ : Semiring A
inst✝ : Algebra R A
g : ExteriorAlgebra R M →ₐ[R] A
m : M
⊢ ↑g (↑(ι R) m) * ↑g (↑(ι R) m) = 0
[PROOFSTEP]
rw [← AlgHom.map_mul, ι_sq_zero, AlgHom.map_zero]
[GOAL]
R : Type u1
inst✝⁴ : CommRing R
M : Type u2
inst✝³ : AddCommGroup M
inst✝² : Module R M
A : Type u_1
inst✝¹ : Semiring A
inst✝ : Algebra R A
⊢ ∀ (a : M →ₗ[R] A),
    (∀ (m : M), ↑a m * ↑a m = 0) ↔
      ∀ (m : M), ↑(↑(Equiv.refl (M →ₗ[R] A)) a) m * ↑(↑(Equiv.refl (M →ₗ[R] A)) a) m = ↑(algebraMap R A) (↑0 m)
[PROOFSTEP]
simp
[GOAL]
R : Type u1
inst✝⁴ : CommRing R
M : Type u2
inst✝³ : AddCommGroup M
inst✝² : Module R M
A : Type u_1
inst✝¹ : Semiring A
inst✝ : Algebra R A
m : M
⊢ ↑0 m * ↑0 m = 0
[PROOFSTEP]
simp
[GOAL]
R : Type u1
inst✝⁴ : CommRing R
M : Type u2
inst✝³ : AddCommGroup M
inst✝² : Module R M
A : Type u_1
inst✝¹ : Semiring A
inst✝ : Algebra R A
x : R
⊢ ↑algebraMapInv (↑(algebraMap R (ExteriorAlgebra R M)) x) = x
[PROOFSTEP]
simp [algebraMapInv]
[GOAL]
R : Type u1
inst✝⁴ : CommRing R
M : Type u2
inst✝³ : AddCommGroup M
inst✝² : Module R M
A : Type u_1
inst✝¹ : Semiring A
inst✝ : Algebra R A
⊢ ExteriorAlgebra R M →ₗ[R] M
[PROOFSTEP]
letI : Module Rᵐᵒᵖ M := Module.compHom _ ((RingHom.id R).fromOpposite mul_comm)
[GOAL]
R : Type u1
inst✝⁴ : CommRing R
M : Type u2
inst✝³ : AddCommGroup M
inst✝² : Module R M
A : Type u_1
inst✝¹ : Semiring A
inst✝ : Algebra R A
this : Module Rᵐᵒᵖ M := Module.compHom M (RingHom.fromOpposite (RingHom.id R) (_ : ∀ (a b : R), a * b = b * a))
⊢ ExteriorAlgebra R M →ₗ[R] M
[PROOFSTEP]
haveI : IsCentralScalar R M := ⟨fun r m => rfl⟩
[GOAL]
R : Type u1
inst✝⁴ : CommRing R
M : Type u2
inst✝³ : AddCommGroup M
inst✝² : Module R M
A : Type u_1
inst✝¹ : Semiring A
inst✝ : Algebra R A
this✝ : Module Rᵐᵒᵖ M := Module.compHom M (RingHom.fromOpposite (RingHom.id R) (_ : ∀ (a b : R), a * b = b * a))
this : IsCentralScalar R M
⊢ ExteriorAlgebra R M →ₗ[R] M
[PROOFSTEP]
exact (TrivSqZeroExt.sndHom R M).comp toTrivSqZeroExt.toLinearMap
[GOAL]
R : Type u1
inst✝⁴ : CommRing R
M : Type u2
inst✝³ : AddCommGroup M
inst✝² : Module R M
A : Type u_1
inst✝¹ : Semiring A
inst✝ : Algebra R A
x : M
⊢ ↑ιInv.toAddHom (↑(ι R) x) = x
[PROOFSTEP]
letI : Module Rᵐᵒᵖ M := Module.compHom _ ((RingHom.id R).fromOpposite mul_comm)
[GOAL]
R : Type u1
inst✝⁴ : CommRing R
M : Type u2
inst✝³ : AddCommGroup M
inst✝² : Module R M
A : Type u_1
inst✝¹ : Semiring A
inst✝ : Algebra R A
x : M
this : Module Rᵐᵒᵖ M := Module.compHom M (RingHom.fromOpposite (RingHom.id R) (_ : ∀ (a b : R), a * b = b * a))
⊢ ↑ιInv.toAddHom (↑(ι R) x) = x
[PROOFSTEP]
haveI : IsCentralScalar R M := ⟨fun r m => rfl⟩
[GOAL]
R : Type u1
inst✝⁴ : CommRing R
M : Type u2
inst✝³ : AddCommGroup M
inst✝² : Module R M
A : Type u_1
inst✝¹ : Semiring A
inst✝ : Algebra R A
x : M
this✝ : Module Rᵐᵒᵖ M := Module.compHom M (RingHom.fromOpposite (RingHom.id R) (_ : ∀ (a b : R), a * b = b * a))
this : IsCentralScalar R M
⊢ ↑ιInv.toAddHom (↑(ι R) x) = x
[PROOFSTEP]
simp [ιInv]
[GOAL]
R : Type u1
inst✝⁴ : CommRing R
M : Type u2
inst✝³ : AddCommGroup M
inst✝² : Module R M
A : Type u_1
inst✝¹ : Semiring A
inst✝ : Algebra R A
x : M
⊢ ↑(ι R) x = 0 ↔ x = 0
[PROOFSTEP]
rw [← ι_inj R x 0, LinearMap.map_zero]
[GOAL]
R : Type u1
inst✝⁴ : CommRing R
M : Type u2
inst✝³ : AddCommGroup M
inst✝² : Module R M
A : Type u_1
inst✝¹ : Semiring A
inst✝ : Algebra R A
x : M
r : R
⊢ ↑(ι R) x = ↑(algebraMap R (ExteriorAlgebra R M)) r ↔ x = 0 ∧ r = 0
[PROOFSTEP]
refine' ⟨fun h => _, _⟩
[GOAL]
case refine'_1
R : Type u1
inst✝⁴ : CommRing R
M : Type u2
inst✝³ : AddCommGroup M
inst✝² : Module R M
A : Type u_1
inst✝¹ : Semiring A
inst✝ : Algebra R A
x : M
r : R
h : ↑(ι R) x = ↑(algebraMap R (ExteriorAlgebra R M)) r
⊢ x = 0 ∧ r = 0
[PROOFSTEP]
letI : Module Rᵐᵒᵖ M := Module.compHom _ ((RingHom.id R).fromOpposite mul_comm)
[GOAL]
case refine'_1
R : Type u1
inst✝⁴ : CommRing R
M : Type u2
inst✝³ : AddCommGroup M
inst✝² : Module R M
A : Type u_1
inst✝¹ : Semiring A
inst✝ : Algebra R A
x : M
r : R
h : ↑(ι R) x = ↑(algebraMap R (ExteriorAlgebra R M)) r
this : Module Rᵐᵒᵖ M := Module.compHom M (RingHom.fromOpposite (RingHom.id R) (_ : ∀ (a b : R), a * b = b * a))
⊢ x = 0 ∧ r = 0
[PROOFSTEP]
haveI : IsCentralScalar R M := ⟨fun r m => rfl⟩
[GOAL]
case refine'_1
R : Type u1
inst✝⁴ : CommRing R
M : Type u2
inst✝³ : AddCommGroup M
inst✝² : Module R M
A : Type u_1
inst✝¹ : Semiring A
inst✝ : Algebra R A
x : M
r : R
h : ↑(ι R) x = ↑(algebraMap R (ExteriorAlgebra R M)) r
this✝ : Module Rᵐᵒᵖ M := Module.compHom M (RingHom.fromOpposite (RingHom.id R) (_ : ∀ (a b : R), a * b = b * a))
this : IsCentralScalar R M
⊢ x = 0 ∧ r = 0
[PROOFSTEP]
have hf0 : toTrivSqZeroExt (ι R x) = (0, x) := toTrivSqZeroExt_ι _
[GOAL]
case refine'_1
R : Type u1
inst✝⁴ : CommRing R
M : Type u2
inst✝³ : AddCommGroup M
inst✝² : Module R M
A : Type u_1
inst✝¹ : Semiring A
inst✝ : Algebra R A
x : M
r : R
h : ↑(ι R) x = ↑(algebraMap R (ExteriorAlgebra R M)) r
this✝ : Module Rᵐᵒᵖ M := Module.compHom M (RingHom.fromOpposite (RingHom.id R) (_ : ∀ (a b : R), a * b = b * a))
this : IsCentralScalar R M
hf0 : ↑toTrivSqZeroExt (↑(ι R) x) = (0, x)
⊢ x = 0 ∧ r = 0
[PROOFSTEP]
rw [h, AlgHom.commutes] at hf0
[GOAL]
case refine'_1
R : Type u1
inst✝⁴ : CommRing R
M : Type u2
inst✝³ : AddCommGroup M
inst✝² : Module R M
A : Type u_1
inst✝¹ : Semiring A
inst✝ : Algebra R A
x : M
r : R
h : ↑(ι R) x = ↑(algebraMap R (ExteriorAlgebra R M)) r
this✝ : Module Rᵐᵒᵖ M := Module.compHom M (RingHom.fromOpposite (RingHom.id R) (_ : ∀ (a b : R), a * b = b * a))
this : IsCentralScalar R M
hf0 : ↑(algebraMap R (TrivSqZeroExt R M)) r = (0, x)
⊢ x = 0 ∧ r = 0
[PROOFSTEP]
have : r = 0 ∧ 0 = x := Prod.ext_iff.1 hf0
[GOAL]
case refine'_1
R : Type u1
inst✝⁴ : CommRing R
M : Type u2
inst✝³ : AddCommGroup M
inst✝² : Module R M
A : Type u_1
inst✝¹ : Semiring A
inst✝ : Algebra R A
x : M
r : R
h : ↑(ι R) x = ↑(algebraMap R (ExteriorAlgebra R M)) r
this✝¹ : Module Rᵐᵒᵖ M := Module.compHom M (RingHom.fromOpposite (RingHom.id R) (_ : ∀ (a b : R), a * b = b * a))
this✝ : IsCentralScalar R M
hf0 : ↑(algebraMap R (TrivSqZeroExt R M)) r = (0, x)
this : r = 0 ∧ 0 = x
⊢ x = 0 ∧ r = 0
[PROOFSTEP]
exact this.symm.imp_left Eq.symm
[GOAL]
case refine'_2
R : Type u1
inst✝⁴ : CommRing R
M : Type u2
inst✝³ : AddCommGroup M
inst✝² : Module R M
A : Type u_1
inst✝¹ : Semiring A
inst✝ : Algebra R A
x : M
r : R
⊢ x = 0 ∧ r = 0 → ↑(ι R) x = ↑(algebraMap R (ExteriorAlgebra R M)) r
[PROOFSTEP]
rintro ⟨rfl, rfl⟩
[GOAL]
case refine'_2.intro
R : Type u1
inst✝⁴ : CommRing R
M : Type u2
inst✝³ : AddCommGroup M
inst✝² : Module R M
A : Type u_1
inst✝¹ : Semiring A
inst✝ : Algebra R A
⊢ ↑(ι R) 0 = ↑(algebraMap R (ExteriorAlgebra R M)) 0
[PROOFSTEP]
rw [LinearMap.map_zero, RingHom.map_zero]
[GOAL]
R : Type u1
inst✝⁵ : CommRing R
M : Type u2
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
A : Type u_1
inst✝² : Semiring A
inst✝¹ : Algebra R A
inst✝ : Nontrivial R
x : M
⊢ ↑(ι R) x ≠ 1
[PROOFSTEP]
rw [← (algebraMap R (ExteriorAlgebra R M)).map_one, Ne.def, ι_eq_algebraMap_iff]
[GOAL]
R : Type u1
inst✝⁵ : CommRing R
M : Type u2
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
A : Type u_1
inst✝² : Semiring A
inst✝¹ : Algebra R A
inst✝ : Nontrivial R
x : M
⊢ ¬(x = 0 ∧ 1 = 0)
[PROOFSTEP]
exact one_ne_zero ∘ And.right
[GOAL]
R : Type u1
inst✝⁴ : CommRing R
M : Type u2
inst✝³ : AddCommGroup M
inst✝² : Module R M
A : Type u_1
inst✝¹ : Semiring A
inst✝ : Algebra R A
⊢ Disjoint (LinearMap.range (ι R)) 1
[PROOFSTEP]
rw [Submodule.disjoint_def]
[GOAL]
R : Type u1
inst✝⁴ : CommRing R
M : Type u2
inst✝³ : AddCommGroup M
inst✝² : Module R M
A : Type u_1
inst✝¹ : Semiring A
inst✝ : Algebra R A
⊢ ∀ (x : ExteriorAlgebra R M), x ∈ LinearMap.range (ι R) → x ∈ 1 → x = 0
[PROOFSTEP]
rintro _ ⟨x, hx⟩ ⟨r, rfl : algebraMap R (ExteriorAlgebra R M) r = _⟩
[GOAL]
case intro.intro
R : Type u1
inst✝⁴ : CommRing R
M : Type u2
inst✝³ : AddCommGroup M
inst✝² : Module R M
A : Type u_1
inst✝¹ : Semiring A
inst✝ : Algebra R A
x : M
r : R
hx : ↑(ι R) x = ↑(algebraMap R (ExteriorAlgebra R M)) r
⊢ ↑(algebraMap R (ExteriorAlgebra R M)) r = 0
[PROOFSTEP]
rw [ι_eq_algebraMap_iff x] at hx
[GOAL]
case intro.intro
R : Type u1
inst✝⁴ : CommRing R
M : Type u2
inst✝³ : AddCommGroup M
inst✝² : Module R M
A : Type u_1
inst✝¹ : Semiring A
inst✝ : Algebra R A
x : M
r : R
hx : x = 0 ∧ r = 0
⊢ ↑(algebraMap R (ExteriorAlgebra R M)) r = 0
[PROOFSTEP]
rw [hx.2, RingHom.map_zero]
[GOAL]
R : Type u1
inst✝⁴ : CommRing R
M : Type u2
inst✝³ : AddCommGroup M
inst✝² : Module R M
A : Type u_1
inst✝¹ : Semiring A
inst✝ : Algebra R A
x y : M
⊢ ↑(ι R) x * ↑(ι R) y + ↑(ι R) y * ↑(ι R) x = ↑(ι R) (y + x) * ↑(ι R) (y + x)
[PROOFSTEP]
simp [mul_add, add_mul]
[GOAL]
R : Type u1
inst✝⁴ : CommRing R
M : Type u2
inst✝³ : AddCommGroup M
inst✝² : Module R M
A : Type u_1
inst✝¹ : Semiring A
inst✝ : Algebra R A
n : ℕ
f : Fin n → M
i : Fin n
⊢ ↑(ι R) (f i) * List.prod (List.ofFn fun i => ↑(ι R) (f i)) = 0
[PROOFSTEP]
induction' n with n hn
[GOAL]
case zero
R : Type u1
inst✝⁴ : CommRing R
M : Type u2
inst✝³ : AddCommGroup M
inst✝² : Module R M
A : Type u_1
inst✝¹ : Semiring A
inst✝ : Algebra R A
n : ℕ
f✝ : Fin n → M
i✝ : Fin n
f : Fin Nat.zero → M
i : Fin Nat.zero
⊢ ↑(ι R) (f i) * List.prod (List.ofFn fun i => ↑(ι R) (f i)) = 0
[PROOFSTEP]
exact i.elim0
[GOAL]
case succ
R : Type u1
inst✝⁴ : CommRing R
M : Type u2
inst✝³ : AddCommGroup M
inst✝² : Module R M
A : Type u_1
inst✝¹ : Semiring A
inst✝ : Algebra R A
n✝ : ℕ
f✝ : Fin n✝ → M
i✝ : Fin n✝
n : ℕ
hn : ∀ (f : Fin n → M) (i : Fin n), ↑(ι R) (f i) * List.prod (List.ofFn fun i => ↑(ι R) (f i)) = 0
f : Fin (Nat.succ n) → M
i : Fin (Nat.succ n)
⊢ ↑(ι R) (f i) * List.prod (List.ofFn fun i => ↑(ι R) (f i)) = 0
[PROOFSTEP]
rw [List.ofFn_succ, List.prod_cons, ← mul_assoc]
[GOAL]
case succ
R : Type u1
inst✝⁴ : CommRing R
M : Type u2
inst✝³ : AddCommGroup M
inst✝² : Module R M
A : Type u_1
inst✝¹ : Semiring A
inst✝ : Algebra R A
n✝ : ℕ
f✝ : Fin n✝ → M
i✝ : Fin n✝
n : ℕ
hn : ∀ (f : Fin n → M) (i : Fin n), ↑(ι R) (f i) * List.prod (List.ofFn fun i => ↑(ι R) (f i)) = 0
f : Fin (Nat.succ n) → M
i : Fin (Nat.succ n)
⊢ ↑(ι R) (f i) * ↑(ι R) (f 0) * List.prod (List.ofFn fun i => ↑(ι R) (f (Fin.succ i))) = 0
[PROOFSTEP]
by_cases h : i = 0
[GOAL]
case pos
R : Type u1
inst✝⁴ : CommRing R
M : Type u2
inst✝³ : AddCommGroup M
inst✝² : Module R M
A : Type u_1
inst✝¹ : Semiring A
inst✝ : Algebra R A
n✝ : ℕ
f✝ : Fin n✝ → M
i✝ : Fin n✝
n : ℕ
hn : ∀ (f : Fin n → M) (i : Fin n), ↑(ι R) (f i) * List.prod (List.ofFn fun i => ↑(ι R) (f i)) = 0
f : Fin (Nat.succ n) → M
i : Fin (Nat.succ n)
h : i = 0
⊢ ↑(ι R) (f i) * ↑(ι R) (f 0) * List.prod (List.ofFn fun i => ↑(ι R) (f (Fin.succ i))) = 0
[PROOFSTEP]
rw [h, ι_sq_zero, zero_mul]
[GOAL]
case neg
R : Type u1
inst✝⁴ : CommRing R
M : Type u2
inst✝³ : AddCommGroup M
inst✝² : Module R M
A : Type u_1
inst✝¹ : Semiring A
inst✝ : Algebra R A
n✝ : ℕ
f✝ : Fin n✝ → M
i✝ : Fin n✝
n : ℕ
hn : ∀ (f : Fin n → M) (i : Fin n), ↑(ι R) (f i) * List.prod (List.ofFn fun i => ↑(ι R) (f i)) = 0
f : Fin (Nat.succ n) → M
i : Fin (Nat.succ n)
h : ¬i = 0
⊢ ↑(ι R) (f i) * ↑(ι R) (f 0) * List.prod (List.ofFn fun i => ↑(ι R) (f (Fin.succ i))) = 0
[PROOFSTEP]
replace hn := congr_arg ((· * ·) <| ι R <| f 0) (hn (fun i => f <| Fin.succ i) (i.pred h))
[GOAL]
case neg
R : Type u1
inst✝⁴ : CommRing R
M : Type u2
inst✝³ : AddCommGroup M
inst✝² : Module R M
A : Type u_1
inst✝¹ : Semiring A
inst✝ : Algebra R A
n✝ : ℕ
f✝ : Fin n✝ → M
i✝ : Fin n✝
n : ℕ
f : Fin (Nat.succ n) → M
i : Fin (Nat.succ n)
h : ¬i = 0
hn :
  (fun x x_1 => x * x_1) (↑(ι R) (f 0))
      (↑(ι R) (f (Fin.succ (Fin.pred i h))) * List.prod (List.ofFn fun i => ↑(ι R) (f (Fin.succ i)))) =
    (fun x x_1 => x * x_1) (↑(ι R) (f 0)) 0
⊢ ↑(ι R) (f i) * ↑(ι R) (f 0) * List.prod (List.ofFn fun i => ↑(ι R) (f (Fin.succ i))) = 0
[PROOFSTEP]
simp only at hn
[GOAL]
case neg
R : Type u1
inst✝⁴ : CommRing R
M : Type u2
inst✝³ : AddCommGroup M
inst✝² : Module R M
A : Type u_1
inst✝¹ : Semiring A
inst✝ : Algebra R A
n✝ : ℕ
f✝ : Fin n✝ → M
i✝ : Fin n✝
n : ℕ
f : Fin (Nat.succ n) → M
i : Fin (Nat.succ n)
h : ¬i = 0
hn :
  ↑(ι R) (f 0) * (↑(ι R) (f (Fin.succ (Fin.pred i h))) * List.prod (List.ofFn fun i => ↑(ι R) (f (Fin.succ i)))) =
    ↑(ι R) (f 0) * 0
⊢ ↑(ι R) (f i) * ↑(ι R) (f 0) * List.prod (List.ofFn fun i => ↑(ι R) (f (Fin.succ i))) = 0
[PROOFSTEP]
rw [Fin.succ_pred, ← mul_assoc, mul_zero] at hn
[GOAL]
case neg
R : Type u1
inst✝⁴ : CommRing R
M : Type u2
inst✝³ : AddCommGroup M
inst✝² : Module R M
A : Type u_1
inst✝¹ : Semiring A
inst✝ : Algebra R A
n✝ : ℕ
f✝ : Fin n✝ → M
i✝ : Fin n✝
n : ℕ
f : Fin (Nat.succ n) → M
i : Fin (Nat.succ n)
h : ¬i = 0
hn : ↑(ι R) (f 0) * ↑(ι R) (f i) * List.prod (List.ofFn fun i => ↑(ι R) (f (Fin.succ i))) = 0
⊢ ↑(ι R) (f i) * ↑(ι R) (f 0) * List.prod (List.ofFn fun i => ↑(ι R) (f (Fin.succ i))) = 0
[PROOFSTEP]
refine' (eq_zero_iff_eq_zero_of_add_eq_zero _).mp hn
[GOAL]
case neg
R : Type u1
inst✝⁴ : CommRing R
M : Type u2
inst✝³ : AddCommGroup M
inst✝² : Module R M
A : Type u_1
inst✝¹ : Semiring A
inst✝ : Algebra R A
n✝ : ℕ
f✝ : Fin n✝ → M
i✝ : Fin n✝
n : ℕ
f : Fin (Nat.succ n) → M
i : Fin (Nat.succ n)
h : ¬i = 0
hn : ↑(ι R) (f 0) * ↑(ι R) (f i) * List.prod (List.ofFn fun i => ↑(ι R) (f (Fin.succ i))) = 0
⊢ ↑(ι R) (f 0) * ↑(ι R) (f i) * List.prod (List.ofFn fun i => ↑(ι R) (f (Fin.succ i))) +
      ↑(ι R) (f i) * ↑(ι R) (f 0) * List.prod (List.ofFn fun i => ↑(ι R) (f (Fin.succ i))) =
    0
[PROOFSTEP]
rw [← add_mul, ι_add_mul_swap, zero_mul]
[GOAL]
R : Type u1
inst✝⁴ : CommRing R
M : Type u2
inst✝³ : AddCommGroup M
inst✝² : Module R M
A : Type u_1
inst✝¹ : Semiring A
inst✝ : Algebra R A
n : ℕ
F : MultilinearMap R (fun x => M) (ExteriorAlgebra R M) :=
  MultilinearMap.compLinearMap (MultilinearMap.mkPiAlgebraFin R n (ExteriorAlgebra R M)) fun x => ι R
f : Fin n → M
x y : Fin n
hfxy : f x = f y
hxy : x ≠ y
⊢ MultilinearMap.toFun
      { toFun := ↑F,
        map_add' :=
          (_ :
            ∀ [inst : DecidableEq (Fin n)] (m : Fin n → M) (i : Fin n) (x y : M),
              MultilinearMap.toFun F (Function.update m i (x + y)) =
                MultilinearMap.toFun F (Function.update m i x) + MultilinearMap.toFun F (Function.update m i y)),
        map_smul' :=
          (_ :
            ∀ [inst : DecidableEq (Fin n)] (m : Fin n → M) (i : Fin n) (c : R) (x : M),
              MultilinearMap.toFun F (Function.update m i (c • x)) =
                c • MultilinearMap.toFun F (Function.update m i x)) }
      f =
    0
[PROOFSTEP]
dsimp
[GOAL]
R : Type u1
inst✝⁴ : CommRing R
M : Type u2
inst✝³ : AddCommGroup M
inst✝² : Module R M
A : Type u_1
inst✝¹ : Semiring A
inst✝ : Algebra R A
n : ℕ
F : MultilinearMap R (fun x => M) (ExteriorAlgebra R M) :=
  MultilinearMap.compLinearMap (MultilinearMap.mkPiAlgebraFin R n (ExteriorAlgebra R M)) fun x => ι R
f : Fin n → M
x y : Fin n
hfxy : f x = f y
hxy : x ≠ y
⊢ List.prod (List.ofFn fun i => ↑(ι R) (f i)) = 0
[PROOFSTEP]
clear F
[GOAL]
R : Type u1
inst✝⁴ : CommRing R
M : Type u2
inst✝³ : AddCommGroup M
inst✝² : Module R M
A : Type u_1
inst✝¹ : Semiring A
inst✝ : Algebra R A
n : ℕ
f : Fin n → M
x y : Fin n
hfxy : f x = f y
hxy : x ≠ y
⊢ List.prod (List.ofFn fun i => ↑(ι R) (f i)) = 0
[PROOFSTEP]
wlog h : x < y
[GOAL]
case inr
R : Type u1
inst✝⁴ : CommRing R
M : Type u2
inst✝³ : AddCommGroup M
inst✝² : Module R M
A : Type u_1
inst✝¹ : Semiring A
inst✝ : Algebra R A
n : ℕ
f : Fin n → M
x y : Fin n
hfxy : f x = f y
hxy : x ≠ y
this :
  ∀ (R : Type u1) [inst : CommRing R] {M : Type u2} [inst_1 : AddCommGroup M] [inst_2 : Module R M] {A : Type u_1}
    [inst_3 : Semiring A] [inst_4 : Algebra R A] (n : ℕ) (f : Fin n → M) (x y : Fin n),
    f x = f y → x ≠ y → x < y → List.prod (List.ofFn fun i => ↑(ι R) (f i)) = 0
h : ¬x < y
⊢ List.prod (List.ofFn fun i => ↑(ι R) (f i)) = 0
[PROOFSTEP]
exact this R (A := A) n f y x hfxy.symm hxy.symm (hxy.lt_or_lt.resolve_left h)
[GOAL]
R✝ : Type u1
inst✝⁷ : CommRing R✝
M✝ : Type u2
inst✝⁶ : AddCommGroup M✝
inst✝⁵ : Module R✝ M✝
R : Type u1
inst✝⁴ : CommRing R
M : Type u2
inst✝³ : AddCommGroup M
inst✝² : Module R M
A : Type u_1
inst✝¹ : Semiring A
inst✝ : Algebra R A
n : ℕ
f : Fin n → M
x y : Fin n
hfxy : f x = f y
hxy : x ≠ y
h : x < y
⊢ List.prod (List.ofFn fun i => ↑(ι R) (f i)) = 0
[PROOFSTEP]
clear hxy
[GOAL]
R✝ : Type u1
inst✝⁷ : CommRing R✝
M✝ : Type u2
inst✝⁶ : AddCommGroup M✝
inst✝⁵ : Module R✝ M✝
R : Type u1
inst✝⁴ : CommRing R
M : Type u2
inst✝³ : AddCommGroup M
inst✝² : Module R M
A : Type u_1
inst✝¹ : Semiring A
inst✝ : Algebra R A
n : ℕ
f : Fin n → M
x y : Fin n
hfxy : f x = f y
h : x < y
⊢ List.prod (List.ofFn fun i => ↑(ι R) (f i)) = 0
[PROOFSTEP]
induction' n with n hn
[GOAL]
case zero
R✝ : Type u1
inst✝⁷ : CommRing R✝
M✝ : Type u2
inst✝⁶ : AddCommGroup M✝
inst✝⁵ : Module R✝ M✝
R : Type u1
inst✝⁴ : CommRing R
M : Type u2
inst✝³ : AddCommGroup M
inst✝² : Module R M
A : Type u_1
inst✝¹ : Semiring A
inst✝ : Algebra R A
n : ℕ
f✝ : Fin n → M
x✝ y✝ : Fin n
hfxy✝ : f✝ x✝ = f✝ y✝
h✝ : x✝ < y✝
f : Fin Nat.zero → M
x y : Fin Nat.zero
hfxy : f x = f y
h : x < y
⊢ List.prod (List.ofFn fun i => ↑(ι R) (f i)) = 0
[PROOFSTEP]
exact x.elim0
[GOAL]
case succ
R✝ : Type u1
inst✝⁷ : CommRing R✝
M✝ : Type u2
inst✝⁶ : AddCommGroup M✝
inst✝⁵ : Module R✝ M✝
R : Type u1
inst✝⁴ : CommRing R
M : Type u2
inst✝³ : AddCommGroup M
inst✝² : Module R M
A : Type u_1
inst✝¹ : Semiring A
inst✝ : Algebra R A
n✝ : ℕ
f✝ : Fin n✝ → M
x✝ y✝ : Fin n✝
hfxy✝ : f✝ x✝ = f✝ y✝
h✝ : x✝ < y✝
n : ℕ
hn : ∀ (f : Fin n → M) (x y : Fin n), f x = f y → x < y → List.prod (List.ofFn fun i => ↑(ι R) (f i)) = 0
f : Fin (Nat.succ n) → M
x y : Fin (Nat.succ n)
hfxy : f x = f y
h : x < y
⊢ List.prod (List.ofFn fun i => ↑(ι R) (f i)) = 0
[PROOFSTEP]
rw [List.ofFn_succ, List.prod_cons]
[GOAL]
case succ
R✝ : Type u1
inst✝⁷ : CommRing R✝
M✝ : Type u2
inst✝⁶ : AddCommGroup M✝
inst✝⁵ : Module R✝ M✝
R : Type u1
inst✝⁴ : CommRing R
M : Type u2
inst✝³ : AddCommGroup M
inst✝² : Module R M
A : Type u_1
inst✝¹ : Semiring A
inst✝ : Algebra R A
n✝ : ℕ
f✝ : Fin n✝ → M
x✝ y✝ : Fin n✝
hfxy✝ : f✝ x✝ = f✝ y✝
h✝ : x✝ < y✝
n : ℕ
hn : ∀ (f : Fin n → M) (x y : Fin n), f x = f y → x < y → List.prod (List.ofFn fun i => ↑(ι R) (f i)) = 0
f : Fin (Nat.succ n) → M
x y : Fin (Nat.succ n)
hfxy : f x = f y
h : x < y
⊢ ↑(ι R) (f 0) * List.prod (List.ofFn fun i => ↑(ι R) (f (Fin.succ i))) = 0
[PROOFSTEP]
by_cases hx :
  x =
    0
      -- one of the repeated terms is on the left
[GOAL]
case pos
R✝ : Type u1
inst✝⁷ : CommRing R✝
M✝ : Type u2
inst✝⁶ : AddCommGroup M✝
inst✝⁵ : Module R✝ M✝
R : Type u1
inst✝⁴ : CommRing R
M : Type u2
inst✝³ : AddCommGroup M
inst✝² : Module R M
A : Type u_1
inst✝¹ : Semiring A
inst✝ : Algebra R A
n✝ : ℕ
f✝ : Fin n✝ → M
x✝ y✝ : Fin n✝
hfxy✝ : f✝ x✝ = f✝ y✝
h✝ : x✝ < y✝
n : ℕ
hn : ∀ (f : Fin n → M) (x y : Fin n), f x = f y → x < y → List.prod (List.ofFn fun i => ↑(ι R) (f i)) = 0
f : Fin (Nat.succ n) → M
x y : Fin (Nat.succ n)
hfxy : f x = f y
h : x < y
hx : x = 0
⊢ ↑(ι R) (f 0) * List.prod (List.ofFn fun i => ↑(ι R) (f (Fin.succ i))) = 0
[PROOFSTEP]
rw [hx] at hfxy h
[GOAL]
case pos
R✝ : Type u1
inst✝⁷ : CommRing R✝
M✝ : Type u2
inst✝⁶ : AddCommGroup M✝
inst✝⁵ : Module R✝ M✝
R : Type u1
inst✝⁴ : CommRing R
M : Type u2
inst✝³ : AddCommGroup M
inst✝² : Module R M
A : Type u_1
inst✝¹ : Semiring A
inst✝ : Algebra R A
n✝ : ℕ
f✝ : Fin n✝ → M
x✝ y✝ : Fin n✝
hfxy✝ : f✝ x✝ = f✝ y✝
h✝ : x✝ < y✝
n : ℕ
hn : ∀ (f : Fin n → M) (x y : Fin n), f x = f y → x < y → List.prod (List.ofFn fun i => ↑(ι R) (f i)) = 0
f : Fin (Nat.succ n) → M
x y : Fin (Nat.succ n)
hfxy : f 0 = f y
h : 0 < y
hx : x = 0
⊢ ↑(ι R) (f 0) * List.prod (List.ofFn fun i => ↑(ι R) (f (Fin.succ i))) = 0
[PROOFSTEP]
rw [hfxy, ← Fin.succ_pred y (ne_of_lt h).symm]
[GOAL]
case pos
R✝ : Type u1
inst✝⁷ : CommRing R✝
M✝ : Type u2
inst✝⁶ : AddCommGroup M✝
inst✝⁵ : Module R✝ M✝
R : Type u1
inst✝⁴ : CommRing R
M : Type u2
inst✝³ : AddCommGroup M
inst✝² : Module R M
A : Type u_1
inst✝¹ : Semiring A
inst✝ : Algebra R A
n✝ : ℕ
f✝ : Fin n✝ → M
x✝ y✝ : Fin n✝
hfxy✝ : f✝ x✝ = f✝ y✝
h✝ : x✝ < y✝
n : ℕ
hn : ∀ (f : Fin n → M) (x y : Fin n), f x = f y → x < y → List.prod (List.ofFn fun i => ↑(ι R) (f i)) = 0
f : Fin (Nat.succ n) → M
x y : Fin (Nat.succ n)
hfxy : f 0 = f y
h : 0 < y
hx : x = 0
⊢ ↑(ι R) (f (Fin.succ (Fin.pred y (_ : y ≠ 0)))) * List.prod (List.ofFn fun i => ↑(ι R) (f (Fin.succ i))) = 0
[PROOFSTEP]
exact
  ι_mul_prod_list (f ∘ Fin.succ)
    _
      -- ignore the left-most term and induct on the remaining ones, decrementing indices
[GOAL]
case neg
R✝ : Type u1
inst✝⁷ : CommRing R✝
M✝ : Type u2
inst✝⁶ : AddCommGroup M✝
inst✝⁵ : Module R✝ M✝
R : Type u1
inst✝⁴ : CommRing R
M : Type u2
inst✝³ : AddCommGroup M
inst✝² : Module R M
A : Type u_1
inst✝¹ : Semiring A
inst✝ : Algebra R A
n✝ : ℕ
f✝ : Fin n✝ → M
x✝ y✝ : Fin n✝
hfxy✝ : f✝ x✝ = f✝ y✝
h✝ : x✝ < y✝
n : ℕ
hn : ∀ (f : Fin n → M) (x y : Fin n), f x = f y → x < y → List.prod (List.ofFn fun i => ↑(ι R) (f i)) = 0
f : Fin (Nat.succ n) → M
x y : Fin (Nat.succ n)
hfxy : f x = f y
h : x < y
hx : ¬x = 0
⊢ ↑(ι R) (f 0) * List.prod (List.ofFn fun i => ↑(ι R) (f (Fin.succ i))) = 0
[PROOFSTEP]
convert mul_zero (ι R (f 0))
[GOAL]
case h.e'_2.h.e'_6
R✝ : Type u1
inst✝⁷ : CommRing R✝
M✝ : Type u2
inst✝⁶ : AddCommGroup M✝
inst✝⁵ : Module R✝ M✝
R : Type u1
inst✝⁴ : CommRing R
M : Type u2
inst✝³ : AddCommGroup M
inst✝² : Module R M
A : Type u_1
inst✝¹ : Semiring A
inst✝ : Algebra R A
n✝ : ℕ
f✝ : Fin n✝ → M
x✝ y✝ : Fin n✝
hfxy✝ : f✝ x✝ = f✝ y✝
h✝ : x✝ < y✝
n : ℕ
hn : ∀ (f : Fin n → M) (x y : Fin n), f x = f y → x < y → List.prod (List.ofFn fun i => ↑(ι R) (f i)) = 0
f : Fin (Nat.succ n) → M
x y : Fin (Nat.succ n)
hfxy : f x = f y
h : x < y
hx : ¬x = 0
⊢ List.prod (List.ofFn fun i => ↑(ι R) (f (Fin.succ i))) = 0
[PROOFSTEP]
refine'
  hn (fun i => f <| Fin.succ i) (x.pred hx) (y.pred (ne_of_lt <| lt_of_le_of_lt x.zero_le h).symm) _
    (Fin.pred_lt_pred_iff.mpr h)
[GOAL]
case h.e'_2.h.e'_6
R✝ : Type u1
inst✝⁷ : CommRing R✝
M✝ : Type u2
inst✝⁶ : AddCommGroup M✝
inst✝⁵ : Module R✝ M✝
R : Type u1
inst✝⁴ : CommRing R
M : Type u2
inst✝³ : AddCommGroup M
inst✝² : Module R M
A : Type u_1
inst✝¹ : Semiring A
inst✝ : Algebra R A
n✝ : ℕ
f✝ : Fin n✝ → M
x✝ y✝ : Fin n✝
hfxy✝ : f✝ x✝ = f✝ y✝
h✝ : x✝ < y✝
n : ℕ
hn : ∀ (f : Fin n → M) (x y : Fin n), f x = f y → x < y → List.prod (List.ofFn fun i => ↑(ι R) (f i)) = 0
f : Fin (Nat.succ n) → M
x y : Fin (Nat.succ n)
hfxy : f x = f y
h : x < y
hx : ¬x = 0
⊢ (fun i => f (Fin.succ i)) (Fin.pred x hx) = (fun i => f (Fin.succ i)) (Fin.pred y (_ : y ≠ 0))
[PROOFSTEP]
simp only [Fin.succ_pred]
[GOAL]
case h.e'_2.h.e'_6
R✝ : Type u1
inst✝⁷ : CommRing R✝
M✝ : Type u2
inst✝⁶ : AddCommGroup M✝
inst✝⁵ : Module R✝ M✝
R : Type u1
inst✝⁴ : CommRing R
M : Type u2
inst✝³ : AddCommGroup M
inst✝² : Module R M
A : Type u_1
inst✝¹ : Semiring A
inst✝ : Algebra R A
n✝ : ℕ
f✝ : Fin n✝ → M
x✝ y✝ : Fin n✝
hfxy✝ : f✝ x✝ = f✝ y✝
h✝ : x✝ < y✝
n : ℕ
hn : ∀ (f : Fin n → M) (x y : Fin n), f x = f y → x < y → List.prod (List.ofFn fun i => ↑(ι R) (f i)) = 0
f : Fin (Nat.succ n) → M
x y : Fin (Nat.succ n)
hfxy : f x = f y
h : x < y
hx : ¬x = 0
⊢ f x = f y
[PROOFSTEP]
exact hfxy
[GOAL]
R : Type u1
inst✝⁴ : CommRing R
M : Type u2
inst✝³ : AddCommGroup M
inst✝² : Module R M
A : Type u_1
inst✝¹ : Semiring A
inst✝ : Algebra R A
n : ℕ
m : M
v : Fin n → M
⊢ ↑(ι R) (Matrix.vecCons m v 0) * ↑(ιMulti R n) (Matrix.vecTail (Matrix.vecCons m v)) =
    ↑(↑(LinearMap.compAlternatingMap (LinearMap.mulLeft R (↑(ι R) m))) (ιMulti R n)) v
[PROOFSTEP]
simp_rw [Matrix.tail_cons]
[GOAL]
R : Type u1
inst✝⁴ : CommRing R
M : Type u2
inst✝³ : AddCommGroup M
inst✝² : Module R M
A : Type u_1
inst✝¹ : Semiring A
inst✝ : Algebra R A
n : ℕ
m : M
v : Fin n → M
⊢ ↑(ι R) (Matrix.vecCons m v 0) * ↑(ιMulti R n) v =
    ↑(↑(LinearMap.compAlternatingMap (LinearMap.mulLeft R (↑(ι R) m))) (ιMulti R n)) v
[PROOFSTEP]
rfl
[GOAL]
R : Type u1
inst✝² : CommRing R
M : Type u2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
m : M
⊢ ↑toExterior (↑(ι R) m) = ↑(ExteriorAlgebra.ι R) m
[PROOFSTEP]
simp [toExterior]


[GOAL]
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
x : CliffordAlgebra Q
⊢ star (star x) = x
[PROOFSTEP]
simp only [reverse_involute_commute.eq, reverse_reverse, involute_involute]
[GOAL]
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
x y : CliffordAlgebra Q
⊢ star (x * y) = star y * star x
[PROOFSTEP]
simp only [map_mul, reverse.map_mul]
[GOAL]
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
x y : CliffordAlgebra Q
⊢ star (x + y) = star x + star y
[PROOFSTEP]
simp only [map_add]
  -- porting note: cannot infer `Q`
[GOAL]
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
m : M
⊢ star (↑(ι Q) m) = -↑(ι Q) m
[PROOFSTEP]
rw [star_def, involute_ι, map_neg, reverse_ι]
[GOAL]
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
r : R
x : CliffordAlgebra Q
⊢ star (r • x) = r • star x
[PROOFSTEP]
rw [star_def, star_def, map_smul, map_smul]
[GOAL]
R : Type u_1
inst✝² : CommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
Q : QuadraticForm R M
r : R
⊢ star (↑(algebraMap R (CliffordAlgebra Q)) r) = ↑(algebraMap R (CliffordAlgebra Q)) r
[PROOFSTEP]
rw [star_def, involute.commutes, reverse.commutes]


[GOAL]
ι : Type u_1
K : Type u_2
V : Type u_3
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : ι → ℙ K V
⊢ Independent f ↔ LinearIndependent K (Projectivization.rep ∘ f)
[PROOFSTEP]
refine' ⟨_, fun h => _⟩
[GOAL]
case refine'_1
ι : Type u_1
K : Type u_2
V : Type u_3
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : ι → ℙ K V
⊢ Independent f → LinearIndependent K (Projectivization.rep ∘ f)
[PROOFSTEP]
rintro ⟨ff, hff, hh⟩
[GOAL]
case refine'_1.mk
ι : Type u_1
K : Type u_2
V : Type u_3
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
ff : ι → V
hff : ∀ (i : ι), ff i ≠ 0
hh : LinearIndependent K ff
⊢ LinearIndependent K (Projectivization.rep ∘ fun i => mk K (ff i) (_ : ff i ≠ 0))
[PROOFSTEP]
choose a ha using fun i : ι => exists_smul_eq_mk_rep K (ff i) (hff i)
[GOAL]
case refine'_1.mk
ι : Type u_1
K : Type u_2
V : Type u_3
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
ff : ι → V
hff : ∀ (i : ι), ff i ≠ 0
hh : LinearIndependent K ff
a : ι → Kˣ
ha : ∀ (i : ι), a i • ff i = Projectivization.rep (mk K (ff i) (_ : ff i ≠ 0))
⊢ LinearIndependent K (Projectivization.rep ∘ fun i => mk K (ff i) (_ : ff i ≠ 0))
[PROOFSTEP]
convert hh.units_smul a
[GOAL]
case h.e'_4
ι : Type u_1
K : Type u_2
V : Type u_3
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
ff : ι → V
hff : ∀ (i : ι), ff i ≠ 0
hh : LinearIndependent K ff
a : ι → Kˣ
ha : ∀ (i : ι), a i • ff i = Projectivization.rep (mk K (ff i) (_ : ff i ≠ 0))
⊢ (Projectivization.rep ∘ fun i => mk K (ff i) (_ : ff i ≠ 0)) = a • ff
[PROOFSTEP]
ext i
[GOAL]
case h.e'_4.h
ι : Type u_1
K : Type u_2
V : Type u_3
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
ff : ι → V
hff : ∀ (i : ι), ff i ≠ 0
hh : LinearIndependent K ff
a : ι → Kˣ
ha : ∀ (i : ι), a i • ff i = Projectivization.rep (mk K (ff i) (_ : ff i ≠ 0))
i : ι
⊢ (Projectivization.rep ∘ fun i => mk K (ff i) (_ : ff i ≠ 0)) i = (a • ff) i
[PROOFSTEP]
exact (ha i).symm
[GOAL]
case refine'_2
ι : Type u_1
K : Type u_2
V : Type u_3
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : ι → ℙ K V
h : LinearIndependent K (Projectivization.rep ∘ f)
⊢ Independent f
[PROOFSTEP]
convert Independent.mk _ _ h
[GOAL]
case h.e'_7.h
ι : Type u_1
K : Type u_2
V : Type u_3
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : ι → ℙ K V
h : LinearIndependent K (Projectivization.rep ∘ f)
x✝ : ι
⊢ f x✝ = mk K ((Projectivization.rep ∘ f) x✝) (_ : ?m.12147 x✝ ≠ 0)
[PROOFSTEP]
simp only [mk_rep, Function.comp_apply]
[GOAL]
case refine'_2
ι : Type u_1
K : Type u_2
V : Type u_3
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : ι → ℙ K V
h : LinearIndependent K (Projectivization.rep ∘ f)
⊢ ∀ (i : ι), (Projectivization.rep ∘ f) i ≠ 0
[PROOFSTEP]
intro i
[GOAL]
case refine'_2
ι : Type u_1
K : Type u_2
V : Type u_3
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : ι → ℙ K V
h : LinearIndependent K (Projectivization.rep ∘ f)
i : ι
⊢ (Projectivization.rep ∘ f) i ≠ 0
[PROOFSTEP]
apply rep_nonzero
[GOAL]
ι : Type u_1
K : Type u_2
V : Type u_3
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : ι → ℙ K V
⊢ Independent f ↔ CompleteLattice.Independent fun i => Projectivization.submodule (f i)
[PROOFSTEP]
refine' ⟨_, fun h => _⟩
[GOAL]
case refine'_1
ι : Type u_1
K : Type u_2
V : Type u_3
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : ι → ℙ K V
⊢ Independent f → CompleteLattice.Independent fun i => Projectivization.submodule (f i)
[PROOFSTEP]
rintro ⟨f, hf, hi⟩
[GOAL]
case refine'_1.mk
ι : Type u_1
K : Type u_2
V : Type u_3
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : ι → V
hf : ∀ (i : ι), f i ≠ 0
hi : LinearIndependent K f
⊢ CompleteLattice.Independent fun i => Projectivization.submodule ((fun i => mk K (f i) (_ : f i ≠ 0)) i)
[PROOFSTEP]
simp only [submodule_mk]
[GOAL]
case refine'_1.mk
ι : Type u_1
K : Type u_2
V : Type u_3
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : ι → V
hf : ∀ (i : ι), f i ≠ 0
hi : LinearIndependent K f
⊢ CompleteLattice.Independent fun i => Submodule.span K {f i}
[PROOFSTEP]
exact (CompleteLattice.independent_iff_linearIndependent_of_ne_zero (R := K) hf).mpr hi
[GOAL]
case refine'_2
ι : Type u_1
K : Type u_2
V : Type u_3
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : ι → ℙ K V
h : CompleteLattice.Independent fun i => Projectivization.submodule (f i)
⊢ Independent f
[PROOFSTEP]
rw [independent_iff]
[GOAL]
case refine'_2
ι : Type u_1
K : Type u_2
V : Type u_3
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : ι → ℙ K V
h : CompleteLattice.Independent fun i => Projectivization.submodule (f i)
⊢ LinearIndependent K (Projectivization.rep ∘ f)
[PROOFSTEP]
refine' h.linearIndependent (Projectivization.submodule ∘ f) (fun i => _) fun i => _
[GOAL]
case refine'_2.refine'_1
ι : Type u_1
K : Type u_2
V : Type u_3
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : ι → ℙ K V
h : CompleteLattice.Independent fun i => Projectivization.submodule (f i)
i : ι
⊢ (Projectivization.rep ∘ f) i ∈ (Projectivization.submodule ∘ f) i
[PROOFSTEP]
simpa only [Function.comp_apply, submodule_eq] using Submodule.mem_span_singleton_self _
[GOAL]
case refine'_2.refine'_2
ι : Type u_1
K : Type u_2
V : Type u_3
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : ι → ℙ K V
h : CompleteLattice.Independent fun i => Projectivization.submodule (f i)
i : ι
⊢ (Projectivization.rep ∘ f) i ≠ 0
[PROOFSTEP]
exact rep_nonzero (f i)
[GOAL]
ι : Type u_1
K : Type u_2
V : Type u_3
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : ι → ℙ K V
⊢ Dependent f ↔ ¬LinearIndependent K (Projectivization.rep ∘ f)
[PROOFSTEP]
refine' ⟨_, fun h => _⟩
[GOAL]
case refine'_1
ι : Type u_1
K : Type u_2
V : Type u_3
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : ι → ℙ K V
⊢ Dependent f → ¬LinearIndependent K (Projectivization.rep ∘ f)
[PROOFSTEP]
rintro ⟨ff, hff, hh1⟩
[GOAL]
case refine'_1.mk
ι : Type u_1
K : Type u_2
V : Type u_3
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
ff : ι → V
hff : ∀ (i : ι), ff i ≠ 0
hh1 : ¬LinearIndependent K ff
⊢ ¬LinearIndependent K (Projectivization.rep ∘ fun i => mk K (ff i) (_ : ff i ≠ 0))
[PROOFSTEP]
contrapose! hh1
[GOAL]
case refine'_1.mk
ι : Type u_1
K : Type u_2
V : Type u_3
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
ff : ι → V
hff : ∀ (i : ι), ff i ≠ 0
hh1 : LinearIndependent K (Projectivization.rep ∘ fun i => mk K (ff i) (_ : ff i ≠ 0))
⊢ LinearIndependent K ff
[PROOFSTEP]
choose a ha using fun i : ι => exists_smul_eq_mk_rep K (ff i) (hff i)
[GOAL]
case refine'_1.mk
ι : Type u_1
K : Type u_2
V : Type u_3
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
ff : ι → V
hff : ∀ (i : ι), ff i ≠ 0
hh1 : LinearIndependent K (Projectivization.rep ∘ fun i => mk K (ff i) (_ : ff i ≠ 0))
a : ι → Kˣ
ha : ∀ (i : ι), a i • ff i = Projectivization.rep (mk K (ff i) (_ : ff i ≠ 0))
⊢ LinearIndependent K ff
[PROOFSTEP]
convert hh1.units_smul a⁻¹
[GOAL]
case h.e'_4
ι : Type u_1
K : Type u_2
V : Type u_3
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
ff : ι → V
hff : ∀ (i : ι), ff i ≠ 0
hh1 : LinearIndependent K (Projectivization.rep ∘ fun i => mk K (ff i) (_ : ff i ≠ 0))
a : ι → Kˣ
ha : ∀ (i : ι), a i • ff i = Projectivization.rep (mk K (ff i) (_ : ff i ≠ 0))
⊢ ff = a⁻¹ • Projectivization.rep ∘ fun i => mk K (ff i) (_ : ff i ≠ 0)
[PROOFSTEP]
ext i
[GOAL]
case h.e'_4.h
ι : Type u_1
K : Type u_2
V : Type u_3
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
ff : ι → V
hff : ∀ (i : ι), ff i ≠ 0
hh1 : LinearIndependent K (Projectivization.rep ∘ fun i => mk K (ff i) (_ : ff i ≠ 0))
a : ι → Kˣ
ha : ∀ (i : ι), a i • ff i = Projectivization.rep (mk K (ff i) (_ : ff i ≠ 0))
i : ι
⊢ ff i = (a⁻¹ • Projectivization.rep ∘ fun i => mk K (ff i) (_ : ff i ≠ 0)) i
[PROOFSTEP]
simp only [← ha, inv_smul_smul, Pi.smul_apply', Pi.inv_apply, Function.comp_apply]
[GOAL]
case refine'_2
ι : Type u_1
K : Type u_2
V : Type u_3
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : ι → ℙ K V
h : ¬LinearIndependent K (Projectivization.rep ∘ f)
⊢ Dependent f
[PROOFSTEP]
convert Dependent.mk _ _ h
[GOAL]
case h.e'_7.h
ι : Type u_1
K : Type u_2
V : Type u_3
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : ι → ℙ K V
h : ¬LinearIndependent K (Projectivization.rep ∘ f)
x✝ : ι
⊢ f x✝ = mk K ((Projectivization.rep ∘ f) x✝) (_ : ?m.30442 x✝ ≠ 0)
[PROOFSTEP]
simp only [mk_rep, Function.comp_apply]
[GOAL]
case refine'_2
ι : Type u_1
K : Type u_2
V : Type u_3
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : ι → ℙ K V
h : ¬LinearIndependent K (Projectivization.rep ∘ f)
⊢ ∀ (i : ι), (Projectivization.rep ∘ f) i ≠ 0
[PROOFSTEP]
exact fun i => rep_nonzero (f i)
[GOAL]
ι : Type u_1
K : Type u_2
V : Type u_3
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : ι → ℙ K V
⊢ Dependent f ↔ ¬Independent f
[PROOFSTEP]
rw [dependent_iff, independent_iff]
[GOAL]
ι : Type u_1
K : Type u_2
V : Type u_3
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : ι → ℙ K V
⊢ Independent f ↔ ¬Dependent f
[PROOFSTEP]
rw [dependent_iff_not_independent, Classical.not_not]
[GOAL]
ι : Type u_1
K : Type u_2
V : Type u_3
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : ι → ℙ K V
u v : ℙ K V
⊢ Dependent ![u, v] ↔ u = v
[PROOFSTEP]
rw [dependent_iff_not_independent, independent_iff, linearIndependent_fin2, Function.comp_apply, Matrix.cons_val_one,
  Matrix.head_cons, Ne.def]
[GOAL]
ι : Type u_1
K : Type u_2
V : Type u_3
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : ι → ℙ K V
u v : ℙ K V
⊢ ¬(¬Projectivization.rep v = 0 ∧ ∀ (a : K), a • Projectivization.rep v ≠ (Projectivization.rep ∘ ![u, v]) 0) ↔ u = v
[PROOFSTEP]
simp only [Matrix.cons_val_zero, not_and, not_forall, Classical.not_not, Function.comp_apply, ←
  mk_eq_mk_iff' K _ _ (rep_nonzero u) (rep_nonzero v), mk_rep, imp_iff_right_iff]
[GOAL]
ι : Type u_1
K : Type u_2
V : Type u_3
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : ι → ℙ K V
u v : ℙ K V
⊢ ¬Projectivization.rep v = 0 ∨ u = v
[PROOFSTEP]
exact Or.inl (rep_nonzero v)
[GOAL]
ι : Type u_1
K : Type u_2
V : Type u_3
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : ι → ℙ K V
u v : ℙ K V
⊢ Independent ![u, v] ↔ u ≠ v
[PROOFSTEP]
rw [independent_iff_not_dependent, dependent_pair_iff_eq u v]


[GOAL]
R : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : DivisionRing R
inst✝³ : CharZero R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
a b : P
⊢ ↑(lineMap a b) (1 / 2) = midpoint R a b
[PROOFSTEP]
rw [one_div, lineMap_inv_two]
[GOAL]
k : Type u_1
V : Type u_2
P : Type u_3
inst✝⁴ : Field k
inst✝³ : CharZero k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AddTorsor V P
a b : P
⊢ ↑(homothety a (1 / 2)) b = midpoint k a b
[PROOFSTEP]
rw [one_div, homothety_inv_two]


[GOAL]
K : Type u_1
V : Type u_2
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
A B : Subspace K V
⊢ A.carrier = B.carrier → A = B
[PROOFSTEP]
cases A
[GOAL]
case mk
K : Type u_1
V : Type u_2
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
B : Subspace K V
carrier✝ : Set (ℙ K V)
mem_add'✝ :
  ∀ (v w : V) (hv : v ≠ 0) (hw : w ≠ 0) (hvw : v + w ≠ 0),
    Projectivization.mk K v hv ∈ carrier✝ →
      Projectivization.mk K w hw ∈ carrier✝ → Projectivization.mk K (v + w) hvw ∈ carrier✝
⊢ { carrier := carrier✝, mem_add' := mem_add'✝ }.carrier = B.carrier →
    { carrier := carrier✝, mem_add' := mem_add'✝ } = B
[PROOFSTEP]
cases B
[GOAL]
case mk.mk
K : Type u_1
V : Type u_2
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
carrier✝¹ : Set (ℙ K V)
mem_add'✝¹ :
  ∀ (v w : V) (hv : v ≠ 0) (hw : w ≠ 0) (hvw : v + w ≠ 0),
    Projectivization.mk K v hv ∈ carrier✝¹ →
      Projectivization.mk K w hw ∈ carrier✝¹ → Projectivization.mk K (v + w) hvw ∈ carrier✝¹
carrier✝ : Set (ℙ K V)
mem_add'✝ :
  ∀ (v w : V) (hv : v ≠ 0) (hw : w ≠ 0) (hvw : v + w ≠ 0),
    Projectivization.mk K v hv ∈ carrier✝ →
      Projectivization.mk K w hw ∈ carrier✝ → Projectivization.mk K (v + w) hvw ∈ carrier✝
⊢ { carrier := carrier✝¹, mem_add' := mem_add'✝¹ }.carrier = { carrier := carrier✝, mem_add' := mem_add'✝ }.carrier →
    { carrier := carrier✝¹, mem_add' := mem_add'✝¹ } = { carrier := carrier✝, mem_add' := mem_add'✝ }
[PROOFSTEP]
simp
[GOAL]
K : Type u_1
V : Type u_2
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
A : Set (ℙ K V)
B : Subspace K V
⊢ A ≤ ↑B → span A ≤ B
[PROOFSTEP]
intro h x hx
[GOAL]
K : Type u_1
V : Type u_2
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
A : Set (ℙ K V)
B : Subspace K V
h : A ≤ ↑B
x : ℙ K V
hx : x ∈ span A
⊢ x ∈ B
[PROOFSTEP]
induction' hx with y hy
[GOAL]
case of
K : Type u_1
V : Type u_2
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
A : Set (ℙ K V)
B : Subspace K V
h : A ≤ ↑B
x y : ℙ K V
hy : y ∈ A
⊢ y ∈ B
[PROOFSTEP]
apply h
[GOAL]
case of.a
K : Type u_1
V : Type u_2
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
A : Set (ℙ K V)
B : Subspace K V
h : A ≤ ↑B
x y : ℙ K V
hy : y ∈ A
⊢ y ∈ A
[PROOFSTEP]
assumption
[GOAL]
case mem_add
K : Type u_1
V : Type u_2
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
A : Set (ℙ K V)
B : Subspace K V
h : A ≤ ↑B
x : ℙ K V
v✝ w✝ : V
hv✝ : v✝ ≠ 0
hw✝ : w✝ ≠ 0
hvw✝ : v✝ + w✝ ≠ 0
a✝¹ : spanCarrier A (Projectivization.mk K v✝ hv✝)
a✝ : spanCarrier A (Projectivization.mk K w✝ hw✝)
a_ih✝¹ : Projectivization.mk K v✝ hv✝ ∈ B
a_ih✝ : Projectivization.mk K w✝ hw✝ ∈ B
⊢ Projectivization.mk K (v✝ + w✝) hvw✝ ∈ B
[PROOFSTEP]
apply B.mem_add
[GOAL]
case mem_add.a
K : Type u_1
V : Type u_2
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
A : Set (ℙ K V)
B : Subspace K V
h : A ≤ ↑B
x : ℙ K V
v✝ w✝ : V
hv✝ : v✝ ≠ 0
hw✝ : w✝ ≠ 0
hvw✝ : v✝ + w✝ ≠ 0
a✝¹ : spanCarrier A (Projectivization.mk K v✝ hv✝)
a✝ : spanCarrier A (Projectivization.mk K w✝ hw✝)
a_ih✝¹ : Projectivization.mk K v✝ hv✝ ∈ B
a_ih✝ : Projectivization.mk K w✝ hw✝ ∈ B
⊢ Projectivization.mk K v✝ ?mem_add.hv ∈ B
case mem_add.a
K : Type u_1
V : Type u_2
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
A : Set (ℙ K V)
B : Subspace K V
h : A ≤ ↑B
x : ℙ K V
v✝ w✝ : V
hv✝ : v✝ ≠ 0
hw✝ : w✝ ≠ 0
hvw✝ : v✝ + w✝ ≠ 0
a✝¹ : spanCarrier A (Projectivization.mk K v✝ hv✝)
a✝ : spanCarrier A (Projectivization.mk K w✝ hw✝)
a_ih✝¹ : Projectivization.mk K v✝ hv✝ ∈ B
a_ih✝ : Projectivization.mk K w✝ hw✝ ∈ B
⊢ Projectivization.mk K w✝ ?mem_add.hw ∈ B
case mem_add.hv
K : Type u_1
V : Type u_2
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
A : Set (ℙ K V)
B : Subspace K V
h : A ≤ ↑B
x : ℙ K V
v✝ w✝ : V
hv✝ : v✝ ≠ 0
hw✝ : w✝ ≠ 0
hvw✝ : v✝ + w✝ ≠ 0
a✝¹ : spanCarrier A (Projectivization.mk K v✝ hv✝)
a✝ : spanCarrier A (Projectivization.mk K w✝ hw✝)
a_ih✝¹ : Projectivization.mk K v✝ hv✝ ∈ B
a_ih✝ : Projectivization.mk K w✝ hw✝ ∈ B
⊢ v✝ ≠ 0
case mem_add.hw
K : Type u_1
V : Type u_2
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
A : Set (ℙ K V)
B : Subspace K V
h : A ≤ ↑B
x : ℙ K V
v✝ w✝ : V
hv✝ : v✝ ≠ 0
hw✝ : w✝ ≠ 0
hvw✝ : v✝ + w✝ ≠ 0
a✝¹ : spanCarrier A (Projectivization.mk K v✝ hv✝)
a✝ : spanCarrier A (Projectivization.mk K w✝ hw✝)
a_ih✝¹ : Projectivization.mk K v✝ hv✝ ∈ B
a_ih✝ : Projectivization.mk K w✝ hw✝ ∈ B
⊢ w✝ ≠ 0
[PROOFSTEP]
assumption'
[GOAL]
K : Type u_1
V : Type u_2
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
A : Set (Subspace K V)
v w : V
hv : v ≠ 0
hw : w ≠ 0
hvw : v + w ≠ 0
h1 : Projectivization.mk K v hv ∈ sInf (SetLike.coe '' A)
h2 : Projectivization.mk K w hw ∈ sInf (SetLike.coe '' A)
t : Set (ℙ K V)
⊢ t ∈ SetLike.coe '' A → Projectivization.mk K (v + w) hvw ∈ t
[PROOFSTEP]
rintro ⟨s, hs, rfl⟩
[GOAL]
case intro.intro
K : Type u_1
V : Type u_2
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
A : Set (Subspace K V)
v w : V
hv : v ≠ 0
hw : w ≠ 0
hvw : v + w ≠ 0
h1 : Projectivization.mk K v hv ∈ sInf (SetLike.coe '' A)
h2 : Projectivization.mk K w hw ∈ sInf (SetLike.coe '' A)
s : Subspace K V
hs : s ∈ A
⊢ Projectivization.mk K (v + w) hvw ∈ ↑s
[PROOFSTEP]
exact s.mem_add v w hv hw _ (h1 s ⟨s, hs, rfl⟩) (h2 s ⟨s, hs, rfl⟩)
[GOAL]
K : Type u_1
V : Type u_2
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
src✝ : Inf (Subspace K V) := inferInstance
⊢ ∀ (s : Set (Subspace K V)), IsGLB s (sInf s)
[PROOFSTEP]
refine fun s => ⟨fun a ha x hx => hx _ ⟨a, ha, rfl⟩, fun a ha x hx E => ?_⟩
[GOAL]
K : Type u_1
V : Type u_2
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
src✝ : Inf (Subspace K V) := inferInstance
s : Set (Subspace K V)
a : Subspace K V
ha : a ∈ lowerBounds s
x : ℙ K V
hx : x ∈ a
E : Set (ℙ K V)
⊢ E ∈ SetLike.coe '' s → x ∈ E
[PROOFSTEP]
rintro ⟨E, hE, rfl⟩
[GOAL]
case intro.intro
K : Type u_1
V : Type u_2
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
src✝ : Inf (Subspace K V) := inferInstance
s : Set (Subspace K V)
a : Subspace K V
ha : a ∈ lowerBounds s
x : ℙ K V
hx : x ∈ a
E : Subspace K V
hE : E ∈ s
⊢ x ∈ ↑E
[PROOFSTEP]
exact ha hE hx
[GOAL]
K : Type u_1
V : Type u_2
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
⊢ span Set.univ = ⊤
[PROOFSTEP]
rw [eq_top_iff, SetLike.le_def]
[GOAL]
K : Type u_1
V : Type u_2
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
⊢ ∀ ⦃x : ℙ K V⦄, x ∈ ⊤ → x ∈ span Set.univ
[PROOFSTEP]
intro x _hx
[GOAL]
K : Type u_1
V : Type u_2
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
x : ℙ K V
_hx : x ∈ ⊤
⊢ x ∈ span Set.univ
[PROOFSTEP]
exact subset_span _ (Set.mem_univ x)
[GOAL]
K : Type u_1
V : Type u_2
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
S : Set (ℙ K V)
W : Subspace K V
⊢ W ⊔ span S = span (↑W ∪ S)
[PROOFSTEP]
rw [span_union, span_coe]
[GOAL]
K : Type u_1
V : Type u_2
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
S : Set (ℙ K V)
W : Subspace K V
⊢ span S ⊔ W = span (S ∪ ↑W)
[PROOFSTEP]
rw [span_union, span_coe]
[GOAL]
K : Type u_1
V : Type u_2
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
S : Set (ℙ K V)
u : ℙ K V
⊢ u ∈ span S ↔ ∀ (W : Subspace K V), S ⊆ ↑W → u ∈ W
[PROOFSTEP]
simp_rw [← span_le_subspace_iff]
[GOAL]
K : Type u_1
V : Type u_2
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
S : Set (ℙ K V)
u : ℙ K V
⊢ u ∈ span S ↔ ∀ (W : Subspace K V), span S ≤ W → u ∈ W
[PROOFSTEP]
exact ⟨fun hu W hW => hW hu, fun W => W (span S) (le_refl _)⟩
[GOAL]
K : Type u_1
V : Type u_2
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
S : Set (ℙ K V)
⊢ span S = sInf {W | S ⊆ ↑W}
[PROOFSTEP]
ext x
[GOAL]
case carrier.h
K : Type u_1
V : Type u_2
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
S : Set (ℙ K V)
x : ℙ K V
⊢ x ∈ (span S).carrier ↔ x ∈ (sInf {W | S ⊆ ↑W}).carrier
[PROOFSTEP]
simp_rw [mem_carrier_iff, mem_span x]
[GOAL]
case carrier.h
K : Type u_1
V : Type u_2
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
S : Set (ℙ K V)
x : ℙ K V
⊢ (∀ (W : Subspace K V), S ⊆ ↑W → x ∈ W) ↔ x ∈ sInf {W | S ⊆ ↑W}
[PROOFSTEP]
refine ⟨fun hx => ?_, fun hx W hW => ?_⟩
[GOAL]
case carrier.h.refine_1
K : Type u_1
V : Type u_2
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
S : Set (ℙ K V)
x : ℙ K V
hx : ∀ (W : Subspace K V), S ⊆ ↑W → x ∈ W
⊢ x ∈ sInf {W | S ⊆ ↑W}
[PROOFSTEP]
rintro W ⟨T, hT, rfl⟩
[GOAL]
case carrier.h.refine_1.intro.intro
K : Type u_1
V : Type u_2
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
S : Set (ℙ K V)
x : ℙ K V
hx : ∀ (W : Subspace K V), S ⊆ ↑W → x ∈ W
T : Subspace K V
hT : T ∈ {W | S ⊆ ↑W}
⊢ x ∈ ↑T
[PROOFSTEP]
exact hx T hT
[GOAL]
case carrier.h.refine_2
K : Type u_1
V : Type u_2
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
S : Set (ℙ K V)
x : ℙ K V
hx : x ∈ sInf {W | S ⊆ ↑W}
W : Subspace K V
hW : S ⊆ ↑W
⊢ x ∈ W
[PROOFSTEP]
exact (@sInf_le _ _ {W : Subspace K V | S ⊆ ↑W} W hW) hx


[GOAL]
K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v : ℙ K V
⊢ ∀ (a b : { v // v ≠ 0 }), Setoid.r a b → Submodule.span K {↑a} = Submodule.span K {↑b}
[PROOFSTEP]
rintro ⟨a, ha⟩ ⟨b, hb⟩ ⟨x, rfl : x • b = a⟩
[GOAL]
case mk.mk.intro
K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v : ℙ K V
b : V
hb : b ≠ 0
x : Kˣ
ha : x • b ≠ 0
⊢ Submodule.span K {↑{ val := x • b, property := ha }} = Submodule.span K {↑{ val := b, property := hb }}
[PROOFSTEP]
exact Submodule.span_singleton_group_smul_eq _ x _
[GOAL]
K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v w : V
hv : v ≠ 0
hw : w ≠ 0
⊢ mk K v hv = mk K w hw ↔ ∃ a, a • w = v
[PROOFSTEP]
rw [mk_eq_mk_iff K v w hv hw]
[GOAL]
K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v w : V
hv : v ≠ 0
hw : w ≠ 0
⊢ (∃ a, a • w = v) ↔ ∃ a, a • w = v
[PROOFSTEP]
constructor
[GOAL]
case mp
K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v w : V
hv : v ≠ 0
hw : w ≠ 0
⊢ (∃ a, a • w = v) → ∃ a, a • w = v
[PROOFSTEP]
rintro ⟨a, ha⟩
[GOAL]
case mp.intro
K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v w : V
hv : v ≠ 0
hw : w ≠ 0
a : Kˣ
ha : a • w = v
⊢ ∃ a, a • w = v
[PROOFSTEP]
exact ⟨a, ha⟩
[GOAL]
case mpr
K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v w : V
hv : v ≠ 0
hw : w ≠ 0
⊢ (∃ a, a • w = v) → ∃ a, a • w = v
[PROOFSTEP]
rintro ⟨a, ha⟩
[GOAL]
case mpr.intro
K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v w : V
hv : v ≠ 0
hw : w ≠ 0
a : K
ha : a • w = v
⊢ ∃ a, a • w = v
[PROOFSTEP]
refine' ⟨Units.mk0 a fun c => hv.symm _, ha⟩
[GOAL]
case mpr.intro
K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v w : V
hv : v ≠ 0
hw : w ≠ 0
a : K
ha : a • w = v
c : a = 0
⊢ 0 = v
[PROOFSTEP]
rwa [c, zero_smul] at ha
[GOAL]
K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v : ℙ K V
⊢ Projectivization.submodule v = Submodule.span K {Projectivization.rep v}
[PROOFSTEP]
conv_lhs => rw [← v.mk_rep]
[GOAL]
K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v : ℙ K V
| Projectivization.submodule v
[PROOFSTEP]
rw [← v.mk_rep]
[GOAL]
K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v : ℙ K V
| Projectivization.submodule v
[PROOFSTEP]
rw [← v.mk_rep]
[GOAL]
K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v : ℙ K V
| Projectivization.submodule v
[PROOFSTEP]
rw [← v.mk_rep]
[GOAL]
K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v : ℙ K V
⊢ finrank K { x // x ∈ Projectivization.submodule v } = 1
[PROOFSTEP]
rw [submodule_eq]
[GOAL]
K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v : ℙ K V
⊢ finrank K { x // x ∈ Submodule.span K {Projectivization.rep v} } = 1
[PROOFSTEP]
exact finrank_span_singleton v.rep_nonzero
[GOAL]
K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v : ℙ K V
⊢ FiniteDimensional K { x // x ∈ Projectivization.submodule v }
[PROOFSTEP]
rw [← v.mk_rep]
[GOAL]
K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v : ℙ K V
⊢ FiniteDimensional K
    { x // x ∈ Projectivization.submodule (mk K (Projectivization.rep v) (_ : Projectivization.rep v ≠ 0)) }
[PROOFSTEP]
change FiniteDimensional K (K ∙ v.rep)
[GOAL]
K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
v : ℙ K V
⊢ FiniteDimensional K { x // x ∈ Submodule.span K {Projectivization.rep v} }
[PROOFSTEP]
infer_instance
[GOAL]
K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
u v : ℙ K V
h : Projectivization.submodule u = Projectivization.submodule v
⊢ u = v
[PROOFSTEP]
induction' u using ind with u hu
[GOAL]
case h
K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
u✝ v : ℙ K V
h✝ : Projectivization.submodule u✝ = Projectivization.submodule v
u : V
hu : u ≠ 0
h : Projectivization.submodule (mk K u hu) = Projectivization.submodule v
⊢ mk K u hu = v
[PROOFSTEP]
induction' v using ind with v hv
[GOAL]
case h.h
K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
u✝ v✝ : ℙ K V
h✝² : Projectivization.submodule u✝ = Projectivization.submodule v✝
u : V
hu : u ≠ 0
h✝¹ : Projectivization.submodule (mk K u hu) = Projectivization.submodule v✝
v : V
hv : v ≠ 0
h✝ : Projectivization.submodule u✝ = Projectivization.submodule (mk K v hv)
h : Projectivization.submodule (mk K u hu) = Projectivization.submodule (mk K v hv)
⊢ mk K u hu = mk K v hv
[PROOFSTEP]
rw [submodule_mk, submodule_mk, Submodule.span_singleton_eq_span_singleton] at h
[GOAL]
case h.h
K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
u✝ v✝ : ℙ K V
h✝² : Projectivization.submodule u✝ = Projectivization.submodule v✝
u : V
hu : u ≠ 0
h✝¹ : Projectivization.submodule (mk K u hu) = Projectivization.submodule v✝
v : V
hv : v ≠ 0
h✝ : Projectivization.submodule u✝ = Projectivization.submodule (mk K v hv)
h : ∃ z, z • u = v
⊢ mk K u hu = mk K v hv
[PROOFSTEP]
exact ((mk_eq_mk_iff K v u hv hu).2 h).symm
[GOAL]
K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
H : Submodule K V
⊢ H ∈ Set.range Projectivization.submodule ↔ finrank K { x // x ∈ ↑(Equiv.refl (Submodule K V)) H } = 1
[PROOFSTEP]
refine ⟨fun ⟨v, hv⟩ ↦ hv ▸ v.finrank_submodule, fun h ↦ ?_⟩
[GOAL]
K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
H : Submodule K V
h : finrank K { x // x ∈ ↑(Equiv.refl (Submodule K V)) H } = 1
⊢ H ∈ Set.range Projectivization.submodule
[PROOFSTEP]
rcases finrank_eq_one_iff'.1 h with ⟨v : H, hv₀, hv : ∀ w : H, _⟩
[GOAL]
case intro.intro
K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
H : Submodule K V
h : finrank K { x // x ∈ ↑(Equiv.refl (Submodule K V)) H } = 1
v : { x // x ∈ H }
hv₀ : v ≠ 0
hv : ∀ (w : { x // x ∈ H }), ∃ c, c • v = w
⊢ H ∈ Set.range Projectivization.submodule
[PROOFSTEP]
use mk K (v : V) (Subtype.coe_injective.ne hv₀)
[GOAL]
case h
K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
H : Submodule K V
h : finrank K { x // x ∈ ↑(Equiv.refl (Submodule K V)) H } = 1
v : { x // x ∈ H }
hv₀ : v ≠ 0
hv : ∀ (w : { x // x ∈ H }), ∃ c, c • v = w
⊢ Projectivization.submodule (mk K ↑v (_ : ↑v ≠ ↑0)) = H
[PROOFSTEP]
rw [submodule_mk, SetLike.ext'_iff, Submodule.span_singleton_eq_range]
[GOAL]
case h
K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
H : Submodule K V
h : finrank K { x // x ∈ ↑(Equiv.refl (Submodule K V)) H } = 1
v : { x // x ∈ H }
hv₀ : v ≠ 0
hv : ∀ (w : { x // x ∈ H }), ∃ c, c • v = w
⊢ (Set.range fun x => x • ↑v) = ↑H
[PROOFSTEP]
refine (Set.range_subset_iff.2 fun _ ↦ H.smul_mem _ v.2).antisymm fun x hx ↦ ?_
[GOAL]
case h
K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
H : Submodule K V
h : finrank K { x // x ∈ ↑(Equiv.refl (Submodule K V)) H } = 1
v : { x // x ∈ H }
hv₀ : v ≠ 0
hv : ∀ (w : { x // x ∈ H }), ∃ c, c • v = w
x : V
hx : x ∈ ↑H
⊢ x ∈ Set.range fun x => x • ↑v
[PROOFSTEP]
rcases hv ⟨x, hx⟩ with ⟨c, hc⟩
[GOAL]
case h.intro
K : Type u_1
V : Type u_2
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
H : Submodule K V
h : finrank K { x // x ∈ ↑(Equiv.refl (Submodule K V)) H } = 1
v : { x // x ∈ H }
hv₀ : v ≠ 0
hv : ∀ (w : { x // x ∈ H }), ∃ c, c • v = w
x : V
hx : x ∈ ↑H
c : K
hc : c • v = { val := x, property := hx }
⊢ x ∈ Set.range fun x => x • ↑v
[PROOFSTEP]
exact ⟨c, congr_arg Subtype.val hc⟩
[GOAL]
K : Type u_1
V : Type u_2
inst✝⁵ : DivisionRing K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
L : Type u_3
W : Type u_4
inst✝² : DivisionRing L
inst✝¹ : AddCommGroup W
inst✝ : Module L W
σ : K →+* L
f : V →ₛₗ[σ] W
hf : Function.Injective ↑f
v : { v // v ≠ 0 }
c : ↑f ↑v = 0
⊢ ↑f ↑v = ↑f 0
[PROOFSTEP]
simp [c]
[GOAL]
K : Type u_1
V : Type u_2
inst✝⁵ : DivisionRing K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
L : Type u_3
W : Type u_4
inst✝² : DivisionRing L
inst✝¹ : AddCommGroup W
inst✝ : Module L W
σ : K →+* L
f : V →ₛₗ[σ] W
hf : Function.Injective ↑f
⊢ (Setoid.r ⇒ Setoid.r) (fun v => { val := ↑f ↑v, property := (_ : ↑f ↑v = 0 → False) }) fun v =>
    { val := ↑f ↑v, property := (_ : ↑f ↑v = 0 → False) }
[PROOFSTEP]
rintro ⟨u, hu⟩ ⟨v, hv⟩ ⟨a, ha⟩
[GOAL]
case mk.mk.intro
K : Type u_1
V : Type u_2
inst✝⁵ : DivisionRing K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
L : Type u_3
W : Type u_4
inst✝² : DivisionRing L
inst✝¹ : AddCommGroup W
inst✝ : Module L W
σ : K →+* L
f : V →ₛₗ[σ] W
hf : Function.Injective ↑f
u : V
hu : u ≠ 0
v : V
hv : v ≠ 0
a : Kˣ
ha : (fun m => m • ↑{ val := v, property := hv }) a = ↑{ val := u, property := hu }
⊢ Setoid.r ((fun v => { val := ↑f ↑v, property := (_ : ↑f ↑v = 0 → False) }) { val := u, property := hu })
    ((fun v => { val := ↑f ↑v, property := (_ : ↑f ↑v = 0 → False) }) { val := v, property := hv })
[PROOFSTEP]
use Units.map σ.toMonoidHom a
[GOAL]
case h
K : Type u_1
V : Type u_2
inst✝⁵ : DivisionRing K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
L : Type u_3
W : Type u_4
inst✝² : DivisionRing L
inst✝¹ : AddCommGroup W
inst✝ : Module L W
σ : K →+* L
f : V →ₛₗ[σ] W
hf : Function.Injective ↑f
u : V
hu : u ≠ 0
v : V
hv : v ≠ 0
a : Kˣ
ha : (fun m => m • ↑{ val := v, property := hv }) a = ↑{ val := u, property := hu }
⊢ (fun m => m • ↑((fun v => { val := ↑f ↑v, property := (_ : ↑f ↑v = 0 → False) }) { val := v, property := hv }))
      (↑(Units.map ↑σ) a) =
    ↑((fun v => { val := ↑f ↑v, property := (_ : ↑f ↑v = 0 → False) }) { val := u, property := hu })
[PROOFSTEP]
dsimp at ha ⊢
[GOAL]
case h
K : Type u_1
V : Type u_2
inst✝⁵ : DivisionRing K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
L : Type u_3
W : Type u_4
inst✝² : DivisionRing L
inst✝¹ : AddCommGroup W
inst✝ : Module L W
σ : K →+* L
f : V →ₛₗ[σ] W
hf : Function.Injective ↑f
u : V
hu : u ≠ 0
v : V
hv : v ≠ 0
a : Kˣ
ha : a • v = u
⊢ ↑(Units.map ↑σ) a • ↑f v = ↑f u
[PROOFSTEP]
erw [← f.map_smulₛₗ, ha]
[GOAL]
K : Type u_1
V : Type u_2
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
L : Type u_3
W : Type u_4
inst✝³ : DivisionRing L
inst✝² : AddCommGroup W
inst✝¹ : Module L W
σ : K →+* L
τ : L →+* K
inst✝ : RingHomInvPair σ τ
f : V →ₛₗ[σ] W
hf : Function.Injective ↑f
u v : ℙ K V
h : map f hf u = map f hf v
⊢ u = v
[PROOFSTEP]
induction' u using ind with u hu
[GOAL]
case h
K : Type u_1
V : Type u_2
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
L : Type u_3
W : Type u_4
inst✝³ : DivisionRing L
inst✝² : AddCommGroup W
inst✝¹ : Module L W
σ : K →+* L
τ : L →+* K
inst✝ : RingHomInvPair σ τ
f : V →ₛₗ[σ] W
hf : Function.Injective ↑f
u✝ v : ℙ K V
h✝ : map f hf u✝ = map f hf v
u : V
hu : u ≠ 0
h : map f hf (mk K u hu) = map f hf v
⊢ mk K u hu = v
[PROOFSTEP]
induction' v using ind with v hv
[GOAL]
case h.h
K : Type u_1
V : Type u_2
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
L : Type u_3
W : Type u_4
inst✝³ : DivisionRing L
inst✝² : AddCommGroup W
inst✝¹ : Module L W
σ : K →+* L
τ : L →+* K
inst✝ : RingHomInvPair σ τ
f : V →ₛₗ[σ] W
hf : Function.Injective ↑f
u✝ v✝ : ℙ K V
h✝² : map f hf u✝ = map f hf v✝
u : V
hu : u ≠ 0
h✝¹ : map f hf (mk K u hu) = map f hf v✝
v : V
hv : v ≠ 0
h✝ : map f hf u✝ = map f hf (mk K v hv)
h : map f hf (mk K u hu) = map f hf (mk K v hv)
⊢ mk K u hu = mk K v hv
[PROOFSTEP]
simp only [map_mk, mk_eq_mk_iff'] at h ⊢
[GOAL]
case h.h
K : Type u_1
V : Type u_2
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
L : Type u_3
W : Type u_4
inst✝³ : DivisionRing L
inst✝² : AddCommGroup W
inst✝¹ : Module L W
σ : K →+* L
τ : L →+* K
inst✝ : RingHomInvPair σ τ
f : V →ₛₗ[σ] W
hf : Function.Injective ↑f
u✝ v✝ : ℙ K V
h✝² : map f hf u✝ = map f hf v✝
u : V
hu : u ≠ 0
h✝¹ : map f hf (mk K u hu) = map f hf v✝
v : V
hv : v ≠ 0
h✝ : map f hf u✝ = map f hf (mk K v hv)
h : ∃ a, a • ↑f v = ↑f u
⊢ ∃ a, a • v = u
[PROOFSTEP]
rcases h with ⟨a, ha⟩
[GOAL]
case h.h.intro
K : Type u_1
V : Type u_2
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
L : Type u_3
W : Type u_4
inst✝³ : DivisionRing L
inst✝² : AddCommGroup W
inst✝¹ : Module L W
σ : K →+* L
τ : L →+* K
inst✝ : RingHomInvPair σ τ
f : V →ₛₗ[σ] W
hf : Function.Injective ↑f
u✝ v✝ : ℙ K V
h✝¹ : map f hf u✝ = map f hf v✝
u : V
hu : u ≠ 0
h✝ : map f hf (mk K u hu) = map f hf v✝
v : V
hv : v ≠ 0
h : map f hf u✝ = map f hf (mk K v hv)
a : L
ha : a • ↑f v = ↑f u
⊢ ∃ a, a • v = u
[PROOFSTEP]
refine ⟨τ a, hf ?_⟩
[GOAL]
case h.h.intro
K : Type u_1
V : Type u_2
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
L : Type u_3
W : Type u_4
inst✝³ : DivisionRing L
inst✝² : AddCommGroup W
inst✝¹ : Module L W
σ : K →+* L
τ : L →+* K
inst✝ : RingHomInvPair σ τ
f : V →ₛₗ[σ] W
hf : Function.Injective ↑f
u✝ v✝ : ℙ K V
h✝¹ : map f hf u✝ = map f hf v✝
u : V
hu : u ≠ 0
h✝ : map f hf (mk K u hu) = map f hf v✝
v : V
hv : v ≠ 0
h : map f hf u✝ = map f hf (mk K v hv)
a : L
ha : a • ↑f v = ↑f u
⊢ ↑f (↑τ a • v) = ↑f u
[PROOFSTEP]
rwa [f.map_smulₛₗ, RingHomInvPair.comp_apply_eq₂]
[GOAL]
K : Type u_1
V : Type u_2
inst✝⁵ : DivisionRing K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
L : Type u_3
W : Type u_4
inst✝² : DivisionRing L
inst✝¹ : AddCommGroup W
inst✝ : Module L W
⊢ map LinearMap.id (_ : Function.Injective ↑(LinearEquiv.refl K V)) = id
[PROOFSTEP]
ext ⟨v⟩
[GOAL]
case h.mk
K : Type u_1
V : Type u_2
inst✝⁵ : DivisionRing K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
L : Type u_3
W : Type u_4
inst✝² : DivisionRing L
inst✝¹ : AddCommGroup W
inst✝ : Module L W
x✝ : ℙ K V
v : { v // v ≠ 0 }
⊢ map LinearMap.id (_ : Function.Injective ↑(LinearEquiv.refl K V)) (Quot.mk Setoid.r v) = id (Quot.mk Setoid.r v)
[PROOFSTEP]
rfl
[GOAL]
K : Type u_1
V : Type u_2
inst✝⁹ : DivisionRing K
inst✝⁸ : AddCommGroup V
inst✝⁷ : Module K V
L : Type u_3
W : Type u_4
inst✝⁶ : DivisionRing L
inst✝⁵ : AddCommGroup W
inst✝⁴ : Module L W
F : Type u_5
U : Type u_6
inst✝³ : Field F
inst✝² : AddCommGroup U
inst✝¹ : Module F U
σ : K →+* L
τ : L →+* F
γ : K →+* F
inst✝ : RingHomCompTriple σ τ γ
f : V →ₛₗ[σ] W
hf : Function.Injective ↑f
g : W →ₛₗ[τ] U
hg : Function.Injective ↑g
⊢ map (LinearMap.comp g f) (_ : Function.Injective (↑g ∘ fun x => ↑f x)) = map g hg ∘ map f hf
[PROOFSTEP]
ext ⟨v⟩
[GOAL]
case h.mk
K : Type u_1
V : Type u_2
inst✝⁹ : DivisionRing K
inst✝⁸ : AddCommGroup V
inst✝⁷ : Module K V
L : Type u_3
W : Type u_4
inst✝⁶ : DivisionRing L
inst✝⁵ : AddCommGroup W
inst✝⁴ : Module L W
F : Type u_5
U : Type u_6
inst✝³ : Field F
inst✝² : AddCommGroup U
inst✝¹ : Module F U
σ : K →+* L
τ : L →+* F
γ : K →+* F
inst✝ : RingHomCompTriple σ τ γ
f : V →ₛₗ[σ] W
hf : Function.Injective ↑f
g : W →ₛₗ[τ] U
hg : Function.Injective ↑g
x✝ : ℙ K V
v : { v // v ≠ 0 }
⊢ map (LinearMap.comp g f) (_ : Function.Injective (↑g ∘ fun x => ↑f x)) (Quot.mk Setoid.r v) =
    (map g hg ∘ map f hf) (Quot.mk Setoid.r v)
[PROOFSTEP]
rfl