[GOAL]
R : Type u
inst✝⁴ : CommSemiring R
M₁ : Type v
M₂ : Type v'
inst✝³ : AddCommMonoid M₁
inst✝² : Module R M₁
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
⊢ dualMap id = id
[PROOFSTEP]
ext
[GOAL]
case h.h
R : Type u
inst✝⁴ : CommSemiring R
M₁ : Type v
M₂ : Type v'
inst✝³ : AddCommMonoid M₁
inst✝² : Module R M₁
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
x✝¹ : Dual R M₁
x✝ : M₁
⊢ ↑(↑(dualMap id) x✝¹) x✝ = ↑(↑id x✝¹) x✝
[PROOFSTEP]
rfl
[GOAL]
R : Type u
inst✝⁴ : CommSemiring R
M₁ : Type v
M₂ : Type v'
inst✝³ : AddCommMonoid M₁
inst✝² : Module R M₁
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
f : M₁ →ₗ[R] M₂
hf : Function.Surjective ↑f
⊢ Function.Injective ↑(dualMap f)
[PROOFSTEP]
intro φ ψ h
[GOAL]
R : Type u
inst✝⁴ : CommSemiring R
M₁ : Type v
M₂ : Type v'
inst✝³ : AddCommMonoid M₁
inst✝² : Module R M₁
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
f : M₁ →ₗ[R] M₂
hf : Function.Surjective ↑f
φ ψ : Dual R M₂
h : ↑(dualMap f) φ = ↑(dualMap f) ψ
⊢ φ = ψ
[PROOFSTEP]
ext x
[GOAL]
case h
R : Type u
inst✝⁴ : CommSemiring R
M₁ : Type v
M₂ : Type v'
inst✝³ : AddCommMonoid M₁
inst✝² : Module R M₁
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
f : M₁ →ₗ[R] M₂
hf : Function.Surjective ↑f
φ ψ : Dual R M₂
h : ↑(dualMap f) φ = ↑(dualMap f) ψ
x : M₂
⊢ ↑φ x = ↑ψ x
[PROOFSTEP]
obtain ⟨y, rfl⟩ := hf x
[GOAL]
case h.intro
R : Type u
inst✝⁴ : CommSemiring R
M₁ : Type v
M₂ : Type v'
inst✝³ : AddCommMonoid M₁
inst✝² : Module R M₁
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
f : M₁ →ₗ[R] M₂
hf : Function.Surjective ↑f
φ ψ : Dual R M₂
h : ↑(dualMap f) φ = ↑(dualMap f) ψ
y : M₁
⊢ ↑φ (↑f y) = ↑ψ (↑f y)
[PROOFSTEP]
exact congr_arg (fun g : Module.Dual R M₁ => g y) h
[GOAL]
R : Type u
inst✝⁴ : CommSemiring R
M₁ : Type v
M₂ : Type v'
inst✝³ : AddCommMonoid M₁
inst✝² : Module R M₁
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
f : M₁ ≃ₗ[R] M₂
src✝ : Dual R M₂ →ₗ[R] Dual R M₁ := LinearMap.dualMap ↑f
⊢ Function.LeftInverse ↑(LinearMap.dualMap ↑(symm f))
    { toAddHom := src✝.toAddHom,
          map_smul' :=
            (_ :
              ∀ (r : R) (x : Dual R M₂),
                AddHom.toFun src✝.toAddHom (r • x) = ↑(RingHom.id R) r • AddHom.toFun src✝.toAddHom x) }.toAddHom.toFun
[PROOFSTEP]
intro φ
[GOAL]
R : Type u
inst✝⁴ : CommSemiring R
M₁ : Type v
M₂ : Type v'
inst✝³ : AddCommMonoid M₁
inst✝² : Module R M₁
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
f : M₁ ≃ₗ[R] M₂
src✝ : Dual R M₂ →ₗ[R] Dual R M₁ := LinearMap.dualMap ↑f
φ : Dual R M₂
⊢ ↑(LinearMap.dualMap ↑(symm f))
      (AddHom.toFun
        { toAddHom := src✝.toAddHom,
            map_smul' :=
              (_ :
                ∀ (r : R) (x : Dual R M₂),
                  AddHom.toFun src✝.toAddHom (r • x) = ↑(RingHom.id R) r • AddHom.toFun src✝.toAddHom x) }.toAddHom
        φ) =
    φ
[PROOFSTEP]
ext x
[GOAL]
case h
R : Type u
inst✝⁴ : CommSemiring R
M₁ : Type v
M₂ : Type v'
inst✝³ : AddCommMonoid M₁
inst✝² : Module R M₁
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
f : M₁ ≃ₗ[R] M₂
src✝ : Dual R M₂ →ₗ[R] Dual R M₁ := LinearMap.dualMap ↑f
φ : Dual R M₂
x : M₂
⊢ ↑(↑(LinearMap.dualMap ↑(symm f))
          (AddHom.toFun
            { toAddHom := src✝.toAddHom,
                map_smul' :=
                  (_ :
                    ∀ (r : R) (x : Dual R M₂),
                      AddHom.toFun src✝.toAddHom (r • x) = ↑(RingHom.id R) r • AddHom.toFun src✝.toAddHom x) }.toAddHom
            φ))
      x =
    ↑φ x
[PROOFSTEP]
simp only [LinearMap.dualMap_apply, LinearEquiv.coe_toLinearMap, LinearMap.toFun_eq_coe, LinearEquiv.apply_symm_apply]
[GOAL]
R : Type u
inst✝⁴ : CommSemiring R
M₁ : Type v
M₂ : Type v'
inst✝³ : AddCommMonoid M₁
inst✝² : Module R M₁
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
f : M₁ ≃ₗ[R] M₂
src✝ : Dual R M₂ →ₗ[R] Dual R M₁ := LinearMap.dualMap ↑f
⊢ Function.RightInverse ↑(LinearMap.dualMap ↑(symm f))
    { toAddHom := src✝.toAddHom,
          map_smul' :=
            (_ :
              ∀ (r : R) (x : Dual R M₂),
                AddHom.toFun src✝.toAddHom (r • x) = ↑(RingHom.id R) r • AddHom.toFun src✝.toAddHom x) }.toAddHom.toFun
[PROOFSTEP]
intro φ
[GOAL]
R : Type u
inst✝⁴ : CommSemiring R
M₁ : Type v
M₂ : Type v'
inst✝³ : AddCommMonoid M₁
inst✝² : Module R M₁
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
f : M₁ ≃ₗ[R] M₂
src✝ : Dual R M₂ →ₗ[R] Dual R M₁ := LinearMap.dualMap ↑f
φ : Dual R M₁
⊢ AddHom.toFun
      { toAddHom := src✝.toAddHom,
          map_smul' :=
            (_ :
              ∀ (r : R) (x : Dual R M₂),
                AddHom.toFun src✝.toAddHom (r • x) = ↑(RingHom.id R) r • AddHom.toFun src✝.toAddHom x) }.toAddHom
      (↑(LinearMap.dualMap ↑(symm f)) φ) =
    φ
[PROOFSTEP]
ext x
[GOAL]
case h
R : Type u
inst✝⁴ : CommSemiring R
M₁ : Type v
M₂ : Type v'
inst✝³ : AddCommMonoid M₁
inst✝² : Module R M₁
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
f : M₁ ≃ₗ[R] M₂
src✝ : Dual R M₂ →ₗ[R] Dual R M₁ := LinearMap.dualMap ↑f
φ : Dual R M₁
x : M₁
⊢ ↑(AddHom.toFun
          { toAddHom := src✝.toAddHom,
              map_smul' :=
                (_ :
                  ∀ (r : R) (x : Dual R M₂),
                    AddHom.toFun src✝.toAddHom (r • x) = ↑(RingHom.id R) r • AddHom.toFun src✝.toAddHom x) }.toAddHom
          (↑(LinearMap.dualMap ↑(symm f)) φ))
      x =
    ↑φ x
[PROOFSTEP]
simp only [LinearMap.dualMap_apply, LinearEquiv.coe_toLinearMap, LinearMap.toFun_eq_coe, LinearEquiv.symm_apply_apply]
[GOAL]
R : Type u
inst✝⁴ : CommSemiring R
M₁ : Type v
M₂ : Type v'
inst✝³ : AddCommMonoid M₁
inst✝² : Module R M₁
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
⊢ dualMap (refl R M₁) = refl R (Dual R M₁)
[PROOFSTEP]
ext
[GOAL]
case h.h
R : Type u
inst✝⁴ : CommSemiring R
M₁ : Type v
M₂ : Type v'
inst✝³ : AddCommMonoid M₁
inst✝² : Module R M₁
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
x✝¹ : Dual R M₁
x✝ : M₁
⊢ ↑(↑(dualMap (refl R M₁)) x✝¹) x✝ = ↑(↑(refl R (Dual R M₁)) x✝¹) x✝
[PROOFSTEP]
rfl
[GOAL]
R : Type u
M : Type v
K : Type u₁
V : Type u₂
ι : Type w
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : DecidableEq ι
b : Basis ι R M
i j : ι
⊢ ↑(↑(toDual b) (↑b i)) (↑b j) = if i = j then 1 else 0
[PROOFSTEP]
erw [constr_basis b, constr_basis b]
[GOAL]
R : Type u
M : Type v
K : Type u₁
V : Type u₂
ι : Type w
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : DecidableEq ι
b : Basis ι R M
i j : ι
⊢ (if j = i then 1 else 0) = if i = j then 1 else 0
[PROOFSTEP]
simp only [eq_comm]
[GOAL]
R : Type u
M : Type v
K : Type u₁
V : Type u₂
ι : Type w
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : DecidableEq ι
b : Basis ι R M
f : ι →₀ R
i : ι
⊢ ↑(↑(toDual b) (↑(Finsupp.total ι M R ↑b) f)) (↑b i) = ↑f i
[PROOFSTEP]
rw [Finsupp.total_apply, Finsupp.sum, LinearMap.map_sum, LinearMap.sum_apply]
[GOAL]
R : Type u
M : Type v
K : Type u₁
V : Type u₂
ι : Type w
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : DecidableEq ι
b : Basis ι R M
f : ι →₀ R
i : ι
⊢ ∑ d in f.support, ↑(↑(toDual b) (↑f d • ↑b d)) (↑b i) = ↑f i
[PROOFSTEP]
simp_rw [LinearMap.map_smul, LinearMap.smul_apply, toDual_apply, smul_eq_mul, mul_boole, Finset.sum_ite_eq']
[GOAL]
R : Type u
M : Type v
K : Type u₁
V : Type u₂
ι : Type w
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : DecidableEq ι
b : Basis ι R M
f : ι →₀ R
i : ι
⊢ (if i ∈ f.support then ↑f i else 0) = ↑f i
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
R : Type u
M : Type v
K : Type u₁
V : Type u₂
ι : Type w
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : DecidableEq ι
b : Basis ι R M
f : ι →₀ R
i : ι
h : i ∈ f.support
⊢ ↑f i = ↑f i
[PROOFSTEP]
rfl
[GOAL]
case neg
R : Type u
M : Type v
K : Type u₁
V : Type u₂
ι : Type w
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : DecidableEq ι
b : Basis ι R M
f : ι →₀ R
i : ι
h : ¬i ∈ f.support
⊢ 0 = ↑f i
[PROOFSTEP]
rw [Finsupp.not_mem_support_iff.mp h]
[GOAL]
R : Type u
M : Type v
K : Type u₁
V : Type u₂
ι : Type w
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : DecidableEq ι
b : Basis ι R M
f : ι →₀ R
i : ι
⊢ ↑(↑(toDual b) (↑b i)) (↑(Finsupp.total ι M R ↑b) f) = ↑f i
[PROOFSTEP]
rw [Finsupp.total_apply, Finsupp.sum, LinearMap.map_sum]
[GOAL]
R : Type u
M : Type v
K : Type u₁
V : Type u₂
ι : Type w
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : DecidableEq ι
b : Basis ι R M
f : ι →₀ R
i : ι
⊢ ∑ i_1 in f.support, ↑(↑(toDual b) (↑b i)) (↑f i_1 • ↑b i_1) = ↑f i
[PROOFSTEP]
simp_rw [LinearMap.map_smul, toDual_apply, smul_eq_mul, mul_boole, Finset.sum_ite_eq]
[GOAL]
R : Type u
M : Type v
K : Type u₁
V : Type u₂
ι : Type w
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : DecidableEq ι
b : Basis ι R M
f : ι →₀ R
i : ι
⊢ (if i ∈ f.support then ↑f i else 0) = ↑f i
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
R : Type u
M : Type v
K : Type u₁
V : Type u₂
ι : Type w
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : DecidableEq ι
b : Basis ι R M
f : ι →₀ R
i : ι
h : i ∈ f.support
⊢ ↑f i = ↑f i
[PROOFSTEP]
rfl
[GOAL]
case neg
R : Type u
M : Type v
K : Type u₁
V : Type u₂
ι : Type w
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : DecidableEq ι
b : Basis ι R M
f : ι →₀ R
i : ι
h : ¬i ∈ f.support
⊢ 0 = ↑f i
[PROOFSTEP]
rw [Finsupp.not_mem_support_iff.mp h]
[GOAL]
R : Type u
M : Type v
K : Type u₁
V : Type u₂
ι : Type w
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : DecidableEq ι
b : Basis ι R M
m : M
i : ι
⊢ ↑(↑(toDual b) m) (↑b i) = ↑(↑b.repr m) i
[PROOFSTEP]
rw [← b.toDual_total_left, b.total_repr]
[GOAL]
R : Type u
M : Type v
K : Type u₁
V : Type u₂
ι : Type w
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : DecidableEq ι
b : Basis ι R M
i : ι
m : M
⊢ ↑(↑(toDual b) (↑b i)) m = ↑(↑b.repr m) i
[PROOFSTEP]
rw [← b.toDual_total_right, b.total_repr]
[GOAL]
R : Type u
M : Type v
K : Type u₁
V : Type u₂
ι : Type w
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : DecidableEq ι
b : Basis ι R M
i : ι
⊢ ↑(toDual b) (↑b i) = coord b i
[PROOFSTEP]
ext
[GOAL]
case h
R : Type u
M : Type v
K : Type u₁
V : Type u₂
ι : Type w
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : DecidableEq ι
b : Basis ι R M
i : ι
x✝ : M
⊢ ↑(↑(toDual b) (↑b i)) x✝ = ↑(coord b i) x✝
[PROOFSTEP]
apply toDual_apply_right
[GOAL]
R : Type u
M : Type v
K : Type u₁
V : Type u₂
ι : Type w
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq ι
b : Basis ι R M
inst✝ : Fintype ι
m : M
i : ι
⊢ ↑(↑(toDual b) m) (↑b i) = ↑(equivFun b) m i
[PROOFSTEP]
rw [b.equivFun_apply, toDual_eq_repr]
[GOAL]
R : Type u
M : Type v
K : Type u₁
V : Type u₂
ι : Type w
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : DecidableEq ι
b : Basis ι R M
m : M
a : ↑(toDual b) m = 0
⊢ m = 0
[PROOFSTEP]
rw [← mem_bot R, ← b.repr.ker, mem_ker, LinearEquiv.coe_coe]
[GOAL]
R : Type u
M : Type v
K : Type u₁
V : Type u₂
ι : Type w
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : DecidableEq ι
b : Basis ι R M
m : M
a : ↑(toDual b) m = 0
⊢ ↑b.repr m = 0
[PROOFSTEP]
apply Finsupp.ext
[GOAL]
case h
R : Type u
M : Type v
K : Type u₁
V : Type u₂
ι : Type w
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : DecidableEq ι
b : Basis ι R M
m : M
a : ↑(toDual b) m = 0
⊢ ∀ (a : ι), ↑(↑b.repr m) a = ↑0 a
[PROOFSTEP]
intro b
[GOAL]
case h
R : Type u
M : Type v
K : Type u₁
V : Type u₂
ι : Type w
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : DecidableEq ι
b✝ : Basis ι R M
m : M
a : ↑(toDual b✝) m = 0
b : ι
⊢ ↑(↑b✝.repr m) b = ↑0 b
[PROOFSTEP]
rw [← toDual_eq_repr, a]
[GOAL]
case h
R : Type u
M : Type v
K : Type u₁
V : Type u₂
ι : Type w
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : DecidableEq ι
b✝ : Basis ι R M
m : M
a : ↑(toDual b✝) m = 0
b : ι
⊢ ↑0 (↑b✝ b) = ↑0 b
[PROOFSTEP]
rfl
[GOAL]
R : Type u
M : Type v
K : Type u₁
V : Type u₂
ι : Type w
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq ι
b : Basis ι R M
inst✝ : _root_.Finite ι
⊢ range (toDual b) = ⊤
[PROOFSTEP]
cases nonempty_fintype ι
[GOAL]
case intro
R : Type u
M : Type v
K : Type u₁
V : Type u₂
ι : Type w
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq ι
b : Basis ι R M
inst✝ : _root_.Finite ι
val✝ : Fintype ι
⊢ range (toDual b) = ⊤
[PROOFSTEP]
refine' eq_top_iff'.2 fun f => _
[GOAL]
case intro
R : Type u
M : Type v
K : Type u₁
V : Type u₂
ι : Type w
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq ι
b : Basis ι R M
inst✝ : _root_.Finite ι
val✝ : Fintype ι
f : Dual R M
⊢ f ∈ range (toDual b)
[PROOFSTEP]
rw [LinearMap.mem_range]
[GOAL]
case intro
R : Type u
M : Type v
K : Type u₁
V : Type u₂
ι : Type w
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq ι
b : Basis ι R M
inst✝ : _root_.Finite ι
val✝ : Fintype ι
f : Dual R M
⊢ ∃ y, ↑(toDual b) y = f
[PROOFSTEP]
let lin_comb : ι →₀ R := Finsupp.equivFunOnFinite.symm fun i => f.toFun (b i)
[GOAL]
case intro
R : Type u
M : Type v
K : Type u₁
V : Type u₂
ι : Type w
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq ι
b : Basis ι R M
inst✝ : _root_.Finite ι
val✝ : Fintype ι
f : Dual R M
lin_comb : ι →₀ R := ↑Finsupp.equivFunOnFinite.symm fun i => AddHom.toFun f.toAddHom (↑b i)
⊢ ∃ y, ↑(toDual b) y = f
[PROOFSTEP]
refine' ⟨Finsupp.total ι M R b lin_comb, b.ext fun i => _⟩
[GOAL]
case intro
R : Type u
M : Type v
K : Type u₁
V : Type u₂
ι : Type w
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq ι
b : Basis ι R M
inst✝ : _root_.Finite ι
val✝ : Fintype ι
f : Dual R M
lin_comb : ι →₀ R := ↑Finsupp.equivFunOnFinite.symm fun i => AddHom.toFun f.toAddHom (↑b i)
i : ι
⊢ ↑(↑(toDual b) (↑(Finsupp.total ι M R ↑b) lin_comb)) (↑b i) = ↑f (↑b i)
[PROOFSTEP]
rw [b.toDual_eq_repr _ i, repr_total b]
[GOAL]
case intro
R : Type u
M : Type v
K : Type u₁
V : Type u₂
ι : Type w
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : DecidableEq ι
b : Basis ι R M
inst✝ : _root_.Finite ι
val✝ : Fintype ι
f : Dual R M
lin_comb : ι →₀ R := ↑Finsupp.equivFunOnFinite.symm fun i => AddHom.toFun f.toAddHom (↑b i)
i : ι
⊢ ↑lin_comb i = ↑f (↑b i)
[PROOFSTEP]
rfl
[GOAL]
R : Type u
M : Type v
K : Type u₁
V : Type u₂
ι : Type w
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Fintype ι
b : Basis ι R M
f : Dual R M
⊢ ∑ x : ι, ↑f (↑b x) • coord b x = f
[PROOFSTEP]
ext m
[GOAL]
case h
R : Type u
M : Type v
K : Type u₁
V : Type u₂
ι : Type w
inst✝³ : CommSemiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Fintype ι
b : Basis ι R M
f : Dual R M
m : M
⊢ ↑(∑ x : ι, ↑f (↑b x) • coord b x) m = ↑f m
[PROOFSTEP]
simp_rw [LinearMap.sum_apply, LinearMap.smul_apply, smul_eq_mul, mul_comm (f _), ← smul_eq_mul, ← f.map_smul, ←
  f.map_sum, Basis.coord_apply, Basis.sum_repr]
[GOAL]
R : Type u
M : Type v
K : Type u₁
V : Type u₂
ι : Type w
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : DecidableEq ι
b : Basis ι R M
inst✝ : _root_.Finite ι
i j : ι
⊢ ↑(↑(dualBasis b) i) (↑b j) = if j = i then 1 else 0
[PROOFSTEP]
convert b.toDual_apply i j using 2
[GOAL]
case h.e'_3.h₁.a
R : Type u
M : Type v
K : Type u₁
V : Type u₂
ι : Type w
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : DecidableEq ι
b : Basis ι R M
inst✝ : _root_.Finite ι
i j : ι
⊢ j = i ↔ i = j
[PROOFSTEP]
rw [@eq_comm _ j i]
[GOAL]
R : Type u
M : Type v
K : Type u₁
V : Type u₂
ι : Type w
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : DecidableEq ι
b : Basis ι R M
inst✝ : _root_.Finite ι
f : ι →₀ R
i : ι
⊢ ↑(↑(Finsupp.total ι (Dual R M) R ↑(dualBasis b)) f) (↑b i) = ↑f i
[PROOFSTEP]
cases nonempty_fintype ι
[GOAL]
case intro
R : Type u
M : Type v
K : Type u₁
V : Type u₂
ι : Type w
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : DecidableEq ι
b : Basis ι R M
inst✝ : _root_.Finite ι
f : ι →₀ R
i : ι
val✝ : Fintype ι
⊢ ↑(↑(Finsupp.total ι (Dual R M) R ↑(dualBasis b)) f) (↑b i) = ↑f i
[PROOFSTEP]
rw [Finsupp.total_apply, Finsupp.sum_fintype, LinearMap.sum_apply]
[GOAL]
case intro
R : Type u
M : Type v
K : Type u₁
V : Type u₂
ι : Type w
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : DecidableEq ι
b : Basis ι R M
inst✝ : _root_.Finite ι
f : ι →₀ R
i : ι
val✝ : Fintype ι
⊢ ∑ d : ι, ↑(↑f d • ↑(dualBasis b) d) (↑b i) = ↑f i
[PROOFSTEP]
simp_rw [LinearMap.smul_apply, smul_eq_mul, dualBasis_apply_self, mul_boole, Finset.sum_ite_eq,
  if_pos (Finset.mem_univ i)]
[GOAL]
case intro.h
R : Type u
M : Type v
K : Type u₁
V : Type u₂
ι : Type w
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : DecidableEq ι
b : Basis ι R M
inst✝ : _root_.Finite ι
f : ι →₀ R
i : ι
val✝ : Fintype ι
⊢ ∀ (i : ι), 0 • ↑(dualBasis b) i = 0
[PROOFSTEP]
intro
[GOAL]
case intro.h
R : Type u
M : Type v
K : Type u₁
V : Type u₂
ι : Type w
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : DecidableEq ι
b : Basis ι R M
inst✝ : _root_.Finite ι
f : ι →₀ R
i : ι
val✝ : Fintype ι
i✝ : ι
⊢ 0 • ↑(dualBasis b) i✝ = 0
[PROOFSTEP]
rw [zero_smul]
[GOAL]
R : Type u
M : Type v
K : Type u₁
V : Type u₂
ι : Type w
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : DecidableEq ι
b : Basis ι R M
inst✝ : _root_.Finite ι
l : Dual R M
i : ι
⊢ ↑(↑(dualBasis b).repr l) i = ↑l (↑b i)
[PROOFSTEP]
rw [← total_dualBasis b, Basis.total_repr b.dualBasis l]
[GOAL]
R : Type u
M : Type v
K : Type u₁
V : Type u₂
ι : Type w
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : DecidableEq ι
b : Basis ι R M
inst✝ : _root_.Finite ι
⊢ ↑(dualBasis b) = coord b
[PROOFSTEP]
ext i x
[GOAL]
case h.h
R : Type u
M : Type v
K : Type u₁
V : Type u₂
ι : Type w
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : DecidableEq ι
b : Basis ι R M
inst✝ : _root_.Finite ι
i : ι
x : M
⊢ ↑(↑(dualBasis b) i) x = ↑(coord b i) x
[PROOFSTEP]
apply dualBasis_apply
[GOAL]
R : Type u
M : Type v
K : Type u₁
V : Type u₂
ι : Type w
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : DecidableEq ι
b : Basis ι R M
inst✝ : _root_.Finite ι
⊢ LinearMap.comp (toDual (dualBasis b)) (toDual b) = Dual.eval R M
[PROOFSTEP]
refine' b.ext fun i => b.dualBasis.ext fun j => _
[GOAL]
R : Type u
M : Type v
K : Type u₁
V : Type u₂
ι : Type w
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : DecidableEq ι
b : Basis ι R M
inst✝ : _root_.Finite ι
i j : ι
⊢ ↑(↑(LinearMap.comp (toDual (dualBasis b)) (toDual b)) (↑b i)) (↑(dualBasis b) j) =
    ↑(↑(Dual.eval R M) (↑b i)) (↑(dualBasis b) j)
[PROOFSTEP]
rw [LinearMap.comp_apply, toDual_apply_left, coe_toDual_self, ← coe_dualBasis, Dual.eval_apply, Basis.repr_self,
  Finsupp.single_apply, dualBasis_apply_self]
[GOAL]
R : Type u
M : Type v
K : Type u₁
V : Type u₂
ι : Type w
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : DecidableEq ι
b : Basis ι R M
inst✝ : Fintype ι
l : Dual R M
i : ι
⊢ ↑(equivFun (dualBasis b)) l i = ↑l (↑b i)
[PROOFSTEP]
rw [Basis.equivFun_apply, dualBasis_repr]
[GOAL]
R : Type u
M : Type v
K : Type u₁
V : Type u₂
ι✝ : Type w
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : DecidableEq ι✝
b✝ : Basis ι✝ R M
ι : Type u_1
b : Basis ι R M
⊢ ker (Dual.eval R M) = ⊥
[PROOFSTEP]
rw [ker_eq_bot']
[GOAL]
R : Type u
M : Type v
K : Type u₁
V : Type u₂
ι✝ : Type w
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : DecidableEq ι✝
b✝ : Basis ι✝ R M
ι : Type u_1
b : Basis ι R M
⊢ ∀ (m : M), ↑(Dual.eval R M) m = 0 → m = 0
[PROOFSTEP]
intro m hm
[GOAL]
R : Type u
M : Type v
K : Type u₁
V : Type u₂
ι✝ : Type w
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : DecidableEq ι✝
b✝ : Basis ι✝ R M
ι : Type u_1
b : Basis ι R M
m : M
hm : ↑(Dual.eval R M) m = 0
⊢ m = 0
[PROOFSTEP]
simp_rw [LinearMap.ext_iff, Dual.eval_apply, zero_apply] at hm 
[GOAL]
R : Type u
M : Type v
K : Type u₁
V : Type u₂
ι✝ : Type w
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : DecidableEq ι✝
b✝ : Basis ι✝ R M
ι : Type u_1
b : Basis ι R M
m : M
hm : ∀ (x : Dual R M), ↑x m = 0
⊢ m = 0
[PROOFSTEP]
exact (Basis.forall_coord_eq_zero_iff _).mp fun i => hm (b.coord i)
[GOAL]
R : Type u
M : Type v
K : Type u₁
V : Type u₂
ι✝ : Type w
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : DecidableEq ι✝
b✝ : Basis ι✝ R M
ι : Type u_1
inst✝ : _root_.Finite ι
b : Basis ι R M
⊢ range (Dual.eval R M) = ⊤
[PROOFSTEP]
classical
cases nonempty_fintype ι
rw [← b.toDual_toDual, range_comp, b.toDual_range, Submodule.map_top, toDual_range _]
[GOAL]
R : Type u
M : Type v
K : Type u₁
V : Type u₂
ι✝ : Type w
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : DecidableEq ι✝
b✝ : Basis ι✝ R M
ι : Type u_1
inst✝ : _root_.Finite ι
b : Basis ι R M
⊢ range (Dual.eval R M) = ⊤
[PROOFSTEP]
cases nonempty_fintype ι
[GOAL]
case intro
R : Type u
M : Type v
K : Type u₁
V : Type u₂
ι✝ : Type w
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : DecidableEq ι✝
b✝ : Basis ι✝ R M
ι : Type u_1
inst✝ : _root_.Finite ι
b : Basis ι R M
val✝ : Fintype ι
⊢ range (Dual.eval R M) = ⊤
[PROOFSTEP]
rw [← b.toDual_toDual, range_comp, b.toDual_range, Submodule.map_top, toDual_range _]
[GOAL]
R : Type u
M : Type v
K : Type u₁
V : Type u₂
ι : Type w
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : _root_.Finite ι
b : Basis ι R M
f : ι →₀ R
i : ι
⊢ ↑(↑(Finsupp.total ι (Dual R M) R (coord b)) f) (↑b i) = ↑f i
[PROOFSTEP]
haveI := Classical.decEq ι
[GOAL]
R : Type u
M : Type v
K : Type u₁
V : Type u₂
ι : Type w
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : _root_.Finite ι
b : Basis ι R M
f : ι →₀ R
i : ι
this : DecidableEq ι
⊢ ↑(↑(Finsupp.total ι (Dual R M) R (coord b)) f) (↑b i) = ↑f i
[PROOFSTEP]
rw [← coe_dualBasis, total_dualBasis]
[GOAL]
R : Type u
M : Type v
K : Type u₁
V : Type u₂
ι : Type w
inst✝³ : CommRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : _root_.Finite ι
b : Basis ι K V
⊢ lift (Module.rank K V) = Module.rank K (Dual K V)
[PROOFSTEP]
classical
cases nonempty_fintype ι
have := LinearEquiv.lift_rank_eq b.toDualEquiv
rw [Cardinal.lift_umax.{u₂, u₁}] at this 
rw [this, ← Cardinal.lift_umax]
apply Cardinal.lift_id
[GOAL]
R : Type u
M : Type v
K : Type u₁
V : Type u₂
ι : Type w
inst✝³ : CommRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : _root_.Finite ι
b : Basis ι K V
⊢ lift (Module.rank K V) = Module.rank K (Dual K V)
[PROOFSTEP]
cases nonempty_fintype ι
[GOAL]
case intro
R : Type u
M : Type v
K : Type u₁
V : Type u₂
ι : Type w
inst✝³ : CommRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : _root_.Finite ι
b : Basis ι K V
val✝ : Fintype ι
⊢ lift (Module.rank K V) = Module.rank K (Dual K V)
[PROOFSTEP]
have := LinearEquiv.lift_rank_eq b.toDualEquiv
[GOAL]
case intro
R : Type u
M : Type v
K : Type u₁
V : Type u₂
ι : Type w
inst✝³ : CommRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : _root_.Finite ι
b : Basis ι K V
val✝ : Fintype ι
this : lift (Module.rank K V) = lift (Module.rank K (Dual K V))
⊢ lift (Module.rank K V) = Module.rank K (Dual K V)
[PROOFSTEP]
rw [Cardinal.lift_umax.{u₂, u₁}] at this 
[GOAL]
case intro
R : Type u
M : Type v
K : Type u₁
V : Type u₂
ι : Type w
inst✝³ : CommRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : _root_.Finite ι
b : Basis ι K V
val✝ : Fintype ι
this : lift (Module.rank K V) = lift (Module.rank K (Dual K V))
⊢ lift (Module.rank K V) = Module.rank K (Dual K V)
[PROOFSTEP]
rw [this, ← Cardinal.lift_umax]
[GOAL]
case intro
R : Type u
M : Type v
K : Type u₁
V : Type u₂
ι : Type w
inst✝³ : CommRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : _root_.Finite ι
b : Basis ι K V
val✝ : Fintype ι
this : lift (Module.rank K V) = lift (Module.rank K (Dual K V))
⊢ lift (Module.rank K (Dual K V)) = Module.rank K (Dual K V)
[PROOFSTEP]
apply Cardinal.lift_id
[GOAL]
K : Type u₁
V : Type u₂
inst✝³ : CommRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : Free K V
⊢ ker (eval K V) = ⊥
[PROOFSTEP]
classical exact (Module.Free.chooseBasis K V).eval_ker
[GOAL]
K : Type u₁
V : Type u₂
inst✝³ : CommRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : Free K V
⊢ ker (eval K V) = ⊥
[PROOFSTEP]
exact (Module.Free.chooseBasis K V).eval_ker
[GOAL]
K : Type u₁
V : Type u₂
inst✝³ : CommRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : Free K V
⊢ Function.Injective (Submodule.map (eval K V))
[PROOFSTEP]
apply Submodule.map_injective_of_injective
[GOAL]
case hf
K : Type u₁
V : Type u₂
inst✝³ : CommRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : Free K V
⊢ Function.Injective ↑(eval K V)
[PROOFSTEP]
rw [← LinearMap.ker_eq_bot]
[GOAL]
case hf
K : Type u₁
V : Type u₂
inst✝³ : CommRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : Free K V
⊢ ker (eval K V) = ⊥
[PROOFSTEP]
apply eval_ker K V
[GOAL]
K : Type u₁
V : Type u₂
inst✝³ : CommRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : Free K V
⊢ Function.Surjective (Submodule.comap (eval K V))
[PROOFSTEP]
apply Submodule.comap_surjective_of_injective
[GOAL]
case hf
K : Type u₁
V : Type u₂
inst✝³ : CommRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : Free K V
⊢ Function.Injective ↑(eval K V)
[PROOFSTEP]
rw [← LinearMap.ker_eq_bot]
[GOAL]
case hf
K : Type u₁
V : Type u₂
inst✝³ : CommRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : Free K V
⊢ ker (eval K V) = ⊥
[PROOFSTEP]
apply eval_ker K V
[GOAL]
K : Type u₁
V : Type u₂
inst✝³ : CommRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : Free K V
v : V
⊢ ↑(eval K V) v = 0 ↔ v = 0
[PROOFSTEP]
simpa only using SetLike.ext_iff.mp (eval_ker K V) v
[GOAL]
K : Type u₁
V : Type u₂
inst✝³ : CommRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : Free K V
v : V
⊢ (∀ (φ : Dual K V), ↑φ v = 0) ↔ v = 0
[PROOFSTEP]
rw [← eval_apply_eq_zero_iff K v, LinearMap.ext_iff]
[GOAL]
K : Type u₁
V : Type u₂
inst✝³ : CommRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : Free K V
v : V
⊢ (∀ (φ : Dual K V), ↑φ v = 0) ↔ ∀ (x : Dual K V), ↑(↑(eval K V) v) x = ↑0 x
[PROOFSTEP]
rfl
[GOAL]
K : Type u₁
V : Type u₂
inst✝⁹ : CommRing K
inst✝⁸ : AddCommGroup V
inst✝⁷ : Module K V
inst✝⁶ : Free K V
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
inst✝ : IsReflexive R M
f : Dual R M
g : Dual R (Dual R M)
⊢ ↑f (↑(LinearEquiv.symm (evalEquiv R M)) g) = ↑g f
[PROOFSTEP]
set m := (evalEquiv R M).symm g
[GOAL]
K : Type u₁
V : Type u₂
inst✝⁹ : CommRing K
inst✝⁸ : AddCommGroup V
inst✝⁷ : Module K V
inst✝⁶ : Free K V
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
inst✝ : IsReflexive R M
f : Dual R M
g : Dual R (Dual R M)
m : M := ↑(LinearEquiv.symm (evalEquiv R M)) g
⊢ ↑f m = ↑g f
[PROOFSTEP]
rw [← (evalEquiv R M).apply_symm_apply g, evalEquiv_apply, Dual.eval_apply]
[GOAL]
K : Type u₁
V : Type u₂
inst✝⁹ : CommRing K
inst✝⁸ : AddCommGroup V
inst✝⁷ : Module K V
inst✝⁶ : Free K V
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
inst✝ : IsReflexive R M
⊢ ↑(LinearEquiv.dualMap (LinearEquiv.symm (evalEquiv R M))) = Dual.eval R (Dual R M)
[PROOFSTEP]
ext
[GOAL]
case h.h
K : Type u₁
V : Type u₂
inst✝⁹ : CommRing K
inst✝⁸ : AddCommGroup V
inst✝⁷ : Module K V
inst✝⁶ : Free K V
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
inst✝ : IsReflexive R M
x✝¹ : Dual R M
x✝ : Dual R (Dual R M)
⊢ ↑(↑↑(LinearEquiv.dualMap (LinearEquiv.symm (evalEquiv R M))) x✝¹) x✝ = ↑(↑(Dual.eval R (Dual R M)) x✝¹) x✝
[PROOFSTEP]
simp
[GOAL]
K : Type u₁
V : Type u₂
inst✝⁹ : CommRing K
inst✝⁸ : AddCommGroup V
inst✝⁷ : Module K V
inst✝⁶ : Free K V
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
inst✝ : IsReflexive R M
⊢ Bijective ↑(eval R (Dual R M))
[PROOFSTEP]
simpa only [← symm_dualMap_evalEquiv] using (evalEquiv R M).dualMap.symm.bijective
[GOAL]
K : Type u₁
V : Type u₂
inst✝¹⁰ : CommRing K
inst✝⁹ : AddCommGroup V
inst✝⁸ : Module K V
inst✝⁷ : Free K V
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
inst✝¹ : IsReflexive R M
inst✝ : IsReflexive R N
⊢ Bijective ↑(Dual.eval R (M × N))
[PROOFSTEP]
let e : Dual R (Dual R (M × N)) ≃ₗ[R] Dual R (Dual R M) × Dual R (Dual R N) :=
  (dualProdDualEquivDual R M N).dualMap.trans (dualProdDualEquivDual R (Dual R M) (Dual R N)).symm
[GOAL]
K : Type u₁
V : Type u₂
inst✝¹⁰ : CommRing K
inst✝⁹ : AddCommGroup V
inst✝⁸ : Module K V
inst✝⁷ : Free K V
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
inst✝¹ : IsReflexive R M
inst✝ : IsReflexive R N
e : Dual R (Dual R (M × N)) ≃ₗ[R] Dual R (Dual R M) × Dual R (Dual R N) :=
  LinearEquiv.trans (LinearEquiv.dualMap (dualProdDualEquivDual R M N))
    (LinearEquiv.symm (dualProdDualEquivDual R (Dual R M) (Dual R N)))
⊢ Bijective ↑(Dual.eval R (M × N))
[PROOFSTEP]
have : Dual.eval R (M × N) = e.symm.comp ((Dual.eval R M).prodMap (Dual.eval R N)) := by ext m f <;> simp
[GOAL]
K : Type u₁
V : Type u₂
inst✝¹⁰ : CommRing K
inst✝⁹ : AddCommGroup V
inst✝⁸ : Module K V
inst✝⁷ : Free K V
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
inst✝¹ : IsReflexive R M
inst✝ : IsReflexive R N
e : Dual R (Dual R (M × N)) ≃ₗ[R] Dual R (Dual R M) × Dual R (Dual R N) :=
  LinearEquiv.trans (LinearEquiv.dualMap (dualProdDualEquivDual R M N))
    (LinearEquiv.symm (dualProdDualEquivDual R (Dual R M) (Dual R N)))
⊢ Dual.eval R (M × N) = LinearMap.comp (↑(LinearEquiv.symm e)) (prodMap (Dual.eval R M) (Dual.eval R N))
[PROOFSTEP]
ext m f
[GOAL]
case hl.h.h
K : Type u₁
V : Type u₂
inst✝¹⁰ : CommRing K
inst✝⁹ : AddCommGroup V
inst✝⁸ : Module K V
inst✝⁷ : Free K V
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
inst✝¹ : IsReflexive R M
inst✝ : IsReflexive R N
e : Dual R (Dual R (M × N)) ≃ₗ[R] Dual R (Dual R M) × Dual R (Dual R N) :=
  LinearEquiv.trans (LinearEquiv.dualMap (dualProdDualEquivDual R M N))
    (LinearEquiv.symm (dualProdDualEquivDual R (Dual R M) (Dual R N)))
m : M
f : Dual R (M × N)
⊢ ↑(↑(LinearMap.comp (Dual.eval R (M × N)) (inl R M N)) m) f =
    ↑(↑(LinearMap.comp (LinearMap.comp (↑(LinearEquiv.symm e)) (prodMap (Dual.eval R M) (Dual.eval R N))) (inl R M N))
          m)
      f
[PROOFSTEP]
simp
[GOAL]
case hr.h.h
K : Type u₁
V : Type u₂
inst✝¹⁰ : CommRing K
inst✝⁹ : AddCommGroup V
inst✝⁸ : Module K V
inst✝⁷ : Free K V
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
inst✝¹ : IsReflexive R M
inst✝ : IsReflexive R N
e : Dual R (Dual R (M × N)) ≃ₗ[R] Dual R (Dual R M) × Dual R (Dual R N) :=
  LinearEquiv.trans (LinearEquiv.dualMap (dualProdDualEquivDual R M N))
    (LinearEquiv.symm (dualProdDualEquivDual R (Dual R M) (Dual R N)))
m : N
f : Dual R (M × N)
⊢ ↑(↑(LinearMap.comp (Dual.eval R (M × N)) (inr R M N)) m) f =
    ↑(↑(LinearMap.comp (LinearMap.comp (↑(LinearEquiv.symm e)) (prodMap (Dual.eval R M) (Dual.eval R N))) (inr R M N))
          m)
      f
[PROOFSTEP]
simp
[GOAL]
K : Type u₁
V : Type u₂
inst✝¹⁰ : CommRing K
inst✝⁹ : AddCommGroup V
inst✝⁸ : Module K V
inst✝⁷ : Free K V
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
inst✝¹ : IsReflexive R M
inst✝ : IsReflexive R N
e : Dual R (Dual R (M × N)) ≃ₗ[R] Dual R (Dual R M) × Dual R (Dual R N) :=
  LinearEquiv.trans (LinearEquiv.dualMap (dualProdDualEquivDual R M N))
    (LinearEquiv.symm (dualProdDualEquivDual R (Dual R M) (Dual R N)))
this : Dual.eval R (M × N) = LinearMap.comp (↑(LinearEquiv.symm e)) (prodMap (Dual.eval R M) (Dual.eval R N))
⊢ Bijective ↑(Dual.eval R (M × N))
[PROOFSTEP]
simp only [this, LinearEquiv.trans_symm, LinearEquiv.symm_symm, LinearEquiv.dualMap_symm, coe_comp, LinearEquiv.coe_coe,
  EquivLike.comp_bijective]
[GOAL]
K : Type u₁
V : Type u₂
inst✝¹⁰ : CommRing K
inst✝⁹ : AddCommGroup V
inst✝⁸ : Module K V
inst✝⁷ : Free K V
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
inst✝¹ : IsReflexive R M
inst✝ : IsReflexive R N
e : Dual R (Dual R (M × N)) ≃ₗ[R] Dual R (Dual R M) × Dual R (Dual R N) :=
  LinearEquiv.trans (LinearEquiv.dualMap (dualProdDualEquivDual R M N))
    (LinearEquiv.symm (dualProdDualEquivDual R (Dual R M) (Dual R N)))
this : Dual.eval R (M × N) = LinearMap.comp (↑(LinearEquiv.symm e)) (prodMap (Dual.eval R M) (Dual.eval R N))
⊢ Bijective ↑(prodMap (Dual.eval R M) (Dual.eval R N))
[PROOFSTEP]
exact Bijective.Prod_map (bijective_dual_eval R M) (bijective_dual_eval R N)
[GOAL]
K : Type u₁
V : Type u₂
inst✝¹⁰ : CommRing K
inst✝⁹ : AddCommGroup V
inst✝⁸ : Module K V
inst✝⁷ : Free K V
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
inst✝¹ inst✝ : IsReflexive R M
e : M ≃ₗ[R] N
⊢ Bijective ↑(Dual.eval R N)
[PROOFSTEP]
let ed : Dual R (Dual R N) ≃ₗ[R] Dual R (Dual R M) := e.symm.dualMap.dualMap
[GOAL]
K : Type u₁
V : Type u₂
inst✝¹⁰ : CommRing K
inst✝⁹ : AddCommGroup V
inst✝⁸ : Module K V
inst✝⁷ : Free K V
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
inst✝¹ inst✝ : IsReflexive R M
e : M ≃ₗ[R] N
ed : Dual R (Dual R N) ≃ₗ[R] Dual R (Dual R M) := LinearEquiv.dualMap (LinearEquiv.dualMap (LinearEquiv.symm e))
⊢ Bijective ↑(Dual.eval R N)
[PROOFSTEP]
have : Dual.eval R N = ed.symm.comp ((Dual.eval R M).comp e.symm.toLinearMap) :=
  by
  ext m f
  exact FunLike.congr_arg f (e.apply_symm_apply m).symm
[GOAL]
K : Type u₁
V : Type u₂
inst✝¹⁰ : CommRing K
inst✝⁹ : AddCommGroup V
inst✝⁸ : Module K V
inst✝⁷ : Free K V
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
inst✝¹ inst✝ : IsReflexive R M
e : M ≃ₗ[R] N
ed : Dual R (Dual R N) ≃ₗ[R] Dual R (Dual R M) := LinearEquiv.dualMap (LinearEquiv.dualMap (LinearEquiv.symm e))
⊢ Dual.eval R N = LinearMap.comp (↑(LinearEquiv.symm ed)) (LinearMap.comp (Dual.eval R M) ↑(LinearEquiv.symm e))
[PROOFSTEP]
ext m f
[GOAL]
case h.h
K : Type u₁
V : Type u₂
inst✝¹⁰ : CommRing K
inst✝⁹ : AddCommGroup V
inst✝⁸ : Module K V
inst✝⁷ : Free K V
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
inst✝¹ inst✝ : IsReflexive R M
e : M ≃ₗ[R] N
ed : Dual R (Dual R N) ≃ₗ[R] Dual R (Dual R M) := LinearEquiv.dualMap (LinearEquiv.dualMap (LinearEquiv.symm e))
m : N
f : Dual R N
⊢ ↑(↑(Dual.eval R N) m) f =
    ↑(↑(LinearMap.comp (↑(LinearEquiv.symm ed)) (LinearMap.comp (Dual.eval R M) ↑(LinearEquiv.symm e))) m) f
[PROOFSTEP]
exact FunLike.congr_arg f (e.apply_symm_apply m).symm
[GOAL]
K : Type u₁
V : Type u₂
inst✝¹⁰ : CommRing K
inst✝⁹ : AddCommGroup V
inst✝⁸ : Module K V
inst✝⁷ : Free K V
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
inst✝¹ inst✝ : IsReflexive R M
e : M ≃ₗ[R] N
ed : Dual R (Dual R N) ≃ₗ[R] Dual R (Dual R M) := LinearEquiv.dualMap (LinearEquiv.dualMap (LinearEquiv.symm e))
this : Dual.eval R N = LinearMap.comp (↑(LinearEquiv.symm ed)) (LinearMap.comp (Dual.eval R M) ↑(LinearEquiv.symm e))
⊢ Bijective ↑(Dual.eval R N)
[PROOFSTEP]
simp only [this, LinearEquiv.trans_symm, LinearEquiv.symm_symm, LinearEquiv.dualMap_symm, coe_comp, LinearEquiv.coe_coe,
  EquivLike.comp_bijective]
[GOAL]
K : Type u₁
V : Type u₂
inst✝¹⁰ : CommRing K
inst✝⁹ : AddCommGroup V
inst✝⁸ : Module K V
inst✝⁷ : Free K V
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
inst✝¹ inst✝ : IsReflexive R M
e : M ≃ₗ[R] N
ed : Dual R (Dual R N) ≃ₗ[R] Dual R (Dual R M) := LinearEquiv.dualMap (LinearEquiv.dualMap (LinearEquiv.symm e))
this : Dual.eval R N = LinearMap.comp (↑(LinearEquiv.symm ed)) (LinearMap.comp (Dual.eval R M) ↑(LinearEquiv.symm e))
⊢ Bijective (↑(Dual.eval R M) ∘ ↑(LinearEquiv.symm e))
[PROOFSTEP]
refine Bijective.comp (bijective_dual_eval R M) (LinearEquiv.bijective _)
[GOAL]
R : Type u_1
M : Type u_2
ι : Type u_3
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
e : ι → M
ε : ι → Dual R M
inst✝ : DecidableEq ι
h : DualBases e ε
m : M
⊢ ∀ (a : ι), a ∈ Set.Finite.toFinset (_ : Set.Finite {i | ↑(ε i) m ≠ 0}) ↔ (fun i => ↑(ε i) m) a ≠ 0
[PROOFSTEP]
intro i
[GOAL]
R : Type u_1
M : Type u_2
ι : Type u_3
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
e : ι → M
ε : ι → Dual R M
inst✝ : DecidableEq ι
h : DualBases e ε
m : M
i : ι
⊢ i ∈ Set.Finite.toFinset (_ : Set.Finite {i | ↑(ε i) m ≠ 0}) ↔ (fun i => ↑(ε i) m) i ≠ 0
[PROOFSTEP]
rw [Set.Finite.mem_toFinset, Set.mem_setOf_eq]
[GOAL]
R : Type u_1
M : Type u_2
ι : Type u_3
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
e : ι → M
ε : ι → Dual R M
inst✝ : DecidableEq ι
h : DualBases e ε
l : ι →₀ R
i : ι
⊢ ↑(ε i) (lc e l) = ↑l i
[PROOFSTEP]
erw [LinearMap.map_sum]
  -- Porting note: cannot get at •
    -- simp only [h.eval, map_smul, smul_eq_mul]
[GOAL]
R : Type u_1
M : Type u_2
ι : Type u_3
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
e : ι → M
ε : ι → Dual R M
inst✝ : DecidableEq ι
h : DualBases e ε
l : ι →₀ R
i : ι
⊢ (Finset.sum l.support fun i_1 => ↑(ε i) ((fun i a => a • e i) i_1 (↑l i_1))) = ↑l i
[PROOFSTEP]
rw [Finset.sum_eq_single i]
[GOAL]
R : Type u_1
M : Type u_2
ι : Type u_3
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
e : ι → M
ε : ι → Dual R M
inst✝ : DecidableEq ι
h : DualBases e ε
l : ι →₀ R
i : ι
⊢ ↑(ε i) ((fun i a => a • e i) i (↑l i)) = ↑l i
[PROOFSTEP]
simp [h.eval, smul_eq_mul]
[GOAL]
case h₀
R : Type u_1
M : Type u_2
ι : Type u_3
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
e : ι → M
ε : ι → Dual R M
inst✝ : DecidableEq ι
h : DualBases e ε
l : ι →₀ R
i : ι
⊢ ∀ (b : ι), b ∈ l.support → b ≠ i → ↑(ε i) ((fun i a => a • e i) b (↑l b)) = 0
[PROOFSTEP]
intro q _ q_ne
[GOAL]
case h₀
R : Type u_1
M : Type u_2
ι : Type u_3
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
e : ι → M
ε : ι → Dual R M
inst✝ : DecidableEq ι
h : DualBases e ε
l : ι →₀ R
i q : ι
a✝ : q ∈ l.support
q_ne : q ≠ i
⊢ ↑(ε i) ((fun i a => a • e i) q (↑l q)) = 0
[PROOFSTEP]
simp [q_ne.symm, h.eval, smul_eq_mul]
[GOAL]
case h₁
R : Type u_1
M : Type u_2
ι : Type u_3
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
e : ι → M
ε : ι → Dual R M
inst✝ : DecidableEq ι
h : DualBases e ε
l : ι →₀ R
i : ι
⊢ ¬i ∈ l.support → ↑(ε i) ((fun i a => a • e i) i (↑l i)) = 0
[PROOFSTEP]
intro p_not_in
[GOAL]
case h₁
R : Type u_1
M : Type u_2
ι : Type u_3
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
e : ι → M
ε : ι → Dual R M
inst✝ : DecidableEq ι
h : DualBases e ε
l : ι →₀ R
i : ι
p_not_in : ¬i ∈ l.support
⊢ ↑(ε i) ((fun i a => a • e i) i (↑l i)) = 0
[PROOFSTEP]
simp [Finsupp.not_mem_support_iff.1 p_not_in]
[GOAL]
R : Type u_1
M : Type u_2
ι : Type u_3
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
e : ι → M
ε : ι → Dual R M
inst✝ : DecidableEq ι
h : DualBases e ε
l : ι →₀ R
⊢ coeffs h (lc e l) = l
[PROOFSTEP]
ext i
[GOAL]
case h
R : Type u_1
M : Type u_2
ι : Type u_3
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
e : ι → M
ε : ι → Dual R M
inst✝ : DecidableEq ι
h : DualBases e ε
l : ι →₀ R
i : ι
⊢ ↑(coeffs h (lc e l)) i = ↑l i
[PROOFSTEP]
rw [h.coeffs_apply, h.dual_lc]
[GOAL]
R : Type u_1
M : Type u_2
ι : Type u_3
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
e : ι → M
ε : ι → Dual R M
inst✝ : DecidableEq ι
h : DualBases e ε
m : M
⊢ lc e (coeffs h m) = m
[PROOFSTEP]
refine' eq_of_sub_eq_zero (h.Total _)
[GOAL]
R : Type u_1
M : Type u_2
ι : Type u_3
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
e : ι → M
ε : ι → Dual R M
inst✝ : DecidableEq ι
h : DualBases e ε
m : M
⊢ ∀ (i : ι), ↑(ε i) (lc e (coeffs h m) - m) = 0
[PROOFSTEP]
intro i
[GOAL]
R : Type u_1
M : Type u_2
ι : Type u_3
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
e : ι → M
ε : ι → Dual R M
inst✝ : DecidableEq ι
h : DualBases e ε
m : M
i : ι
⊢ ↑(ε i) (lc e (coeffs h m) - m) = 0
[PROOFSTEP]
simp [LinearMap.map_sub, h.dual_lc, sub_eq_zero]
[GOAL]
R : Type u_1
M : Type u_2
ι : Type u_3
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
e : ι → M
ε : ι → Dual R M
inst✝ : DecidableEq ι
h : DualBases e ε
v w : M
⊢ coeffs h (v + w) = coeffs h v + coeffs h w
[PROOFSTEP]
ext i
[GOAL]
case h
R : Type u_1
M : Type u_2
ι : Type u_3
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
e : ι → M
ε : ι → Dual R M
inst✝ : DecidableEq ι
h : DualBases e ε
v w : M
i : ι
⊢ ↑(coeffs h (v + w)) i = ↑(coeffs h v + coeffs h w) i
[PROOFSTEP]
exact (ε i).map_add v w
[GOAL]
R : Type u_1
M : Type u_2
ι : Type u_3
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
e : ι → M
ε : ι → Dual R M
inst✝ : DecidableEq ι
h : DualBases e ε
c : R
v : M
⊢ AddHom.toFun { toFun := coeffs h, map_add' := (_ : ∀ (v w : M), coeffs h (v + w) = coeffs h v + coeffs h w) }
      (c • v) =
    ↑(RingHom.id R) c •
      AddHom.toFun { toFun := coeffs h, map_add' := (_ : ∀ (v w : M), coeffs h (v + w) = coeffs h v + coeffs h w) } v
[PROOFSTEP]
ext i
[GOAL]
case h
R : Type u_1
M : Type u_2
ι : Type u_3
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
e : ι → M
ε : ι → Dual R M
inst✝ : DecidableEq ι
h : DualBases e ε
c : R
v : M
i : ι
⊢ ↑(AddHom.toFun { toFun := coeffs h, map_add' := (_ : ∀ (v w : M), coeffs h (v + w) = coeffs h v + coeffs h w) }
          (c • v))
      i =
    ↑(↑(RingHom.id R) c •
          AddHom.toFun { toFun := coeffs h, map_add' := (_ : ∀ (v w : M), coeffs h (v + w) = coeffs h v + coeffs h w) }
            v)
      i
[PROOFSTEP]
exact (ε i).map_smul c v
[GOAL]
R : Type u_1
M : Type u_2
ι : Type u_3
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
e : ι → M
ε : ι → Dual R M
inst✝ : DecidableEq ι
h : DualBases e ε
⊢ ↑(basis h) = e
[PROOFSTEP]
ext i
[GOAL]
case h
R : Type u_1
M : Type u_2
ι : Type u_3
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
e : ι → M
ε : ι → Dual R M
inst✝ : DecidableEq ι
h : DualBases e ε
i : ι
⊢ ↑(basis h) i = e i
[PROOFSTEP]
rw [Basis.apply_eq_iff]
[GOAL]
case h
R : Type u_1
M : Type u_2
ι : Type u_3
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
e : ι → M
ε : ι → Dual R M
inst✝ : DecidableEq ι
h : DualBases e ε
i : ι
⊢ ↑(basis h).repr (e i) = Finsupp.single i 1
[PROOFSTEP]
ext j
[GOAL]
case h.h
R : Type u_1
M : Type u_2
ι : Type u_3
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
e : ι → M
ε : ι → Dual R M
inst✝ : DecidableEq ι
h : DualBases e ε
i j : ι
⊢ ↑(↑(basis h).repr (e i)) j = ↑(Finsupp.single i 1) j
[PROOFSTEP]
rw [h.basis_repr_apply, coeffs_apply, h.eval, Finsupp.single_apply]
[GOAL]
case h.h
R : Type u_1
M : Type u_2
ι : Type u_3
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
e : ι → M
ε : ι → Dual R M
inst✝ : DecidableEq ι
h : DualBases e ε
i j : ι
⊢ (if j = i then 1 else 0) = if i = j then 1 else 0
[PROOFSTEP]
convert if_congr (eq_comm (a := j) (b := i)) rfl rfl
[GOAL]
R : Type u_1
M : Type u_2
ι : Type u_3
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
e : ι → M
ε : ι → Dual R M
inst✝ : DecidableEq ι
h : DualBases e ε
H : Set ι
x : M
hmem : x ∈ Submodule.span R (e '' H)
⊢ ∀ (i : ι), ↑(ε i) x ≠ 0 → i ∈ H
[PROOFSTEP]
intro i hi
[GOAL]
R : Type u_1
M : Type u_2
ι : Type u_3
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
e : ι → M
ε : ι → Dual R M
inst✝ : DecidableEq ι
h : DualBases e ε
H : Set ι
x : M
hmem : x ∈ Submodule.span R (e '' H)
i : ι
hi : ↑(ε i) x ≠ 0
⊢ i ∈ H
[PROOFSTEP]
rcases(Finsupp.mem_span_image_iff_total _).mp hmem with ⟨l, supp_l, rfl⟩
[GOAL]
case intro.intro
R : Type u_1
M : Type u_2
ι : Type u_3
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
e : ι → M
ε : ι → Dual R M
inst✝ : DecidableEq ι
h : DualBases e ε
H : Set ι
i : ι
l : ι →₀ R
supp_l : l ∈ Finsupp.supported R R H
hmem : ↑(Finsupp.total ι M R e) l ∈ Submodule.span R (e '' H)
hi : ↑(ε i) (↑(Finsupp.total ι M R e) l) ≠ 0
⊢ i ∈ H
[PROOFSTEP]
apply not_imp_comm.mp ((Finsupp.mem_supported' _ _).mp supp_l i)
[GOAL]
case intro.intro
R : Type u_1
M : Type u_2
ι : Type u_3
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
e : ι → M
ε : ι → Dual R M
inst✝ : DecidableEq ι
h : DualBases e ε
H : Set ι
i : ι
l : ι →₀ R
supp_l : l ∈ Finsupp.supported R R H
hmem : ↑(Finsupp.total ι M R e) l ∈ Submodule.span R (e '' H)
hi : ↑(ε i) (↑(Finsupp.total ι M R e) l) ≠ 0
⊢ ¬↑l i = 0
[PROOFSTEP]
rwa [← lc_def, h.dual_lc] at hi 
[GOAL]
R : Type u_1
M : Type u_2
ι : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
e : ι → M
ε : ι → Dual R M
inst✝¹ : DecidableEq ι
h : DualBases e ε
inst✝ : Fintype ι
i j : ι
⊢ ↑(↑(Basis.dualBasis (basis h)) i) (↑(basis h) j) = ↑(ε i) (↑(basis h) j)
[PROOFSTEP]
rw [h.basis.dualBasis_apply_self, h.coe_basis, h.eval, if_congr eq_comm rfl rfl]
[GOAL]
R : Type u
M : Type v
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
W : Submodule R M
φ : Module.Dual R M
⊢ φ ∈ dualAnnihilator W ↔ ∀ (w : M), w ∈ W → ↑φ w = 0
[PROOFSTEP]
refine' LinearMap.mem_ker.trans _
[GOAL]
R : Type u
M : Type v
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
W : Submodule R M
φ : Module.Dual R M
⊢ ↑(dualRestrict W) φ = 0 ↔ ∀ (w : M), w ∈ W → ↑φ w = 0
[PROOFSTEP]
simp_rw [LinearMap.ext_iff, dualRestrict_apply]
[GOAL]
R : Type u
M : Type v
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
W : Submodule R M
φ : Module.Dual R M
⊢ (∀ (x : { x // x ∈ W }), ↑φ ↑x = ↑0 x) ↔ ∀ (w : M), w ∈ W → ↑φ w = 0
[PROOFSTEP]
exact ⟨fun h w hw => h ⟨w, hw⟩, fun h w => h w.1 w.2⟩
[GOAL]
R : Type u
M : Type v
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
W : Submodule R M
Φ : Submodule R (Module.Dual R M)
x : M
⊢ x ∈ dualCoannihilator Φ ↔ ∀ (φ : Module.Dual R M), φ ∈ Φ → ↑φ x = 0
[PROOFSTEP]
simp_rw [dualCoannihilator, mem_comap, mem_dualAnnihilator, Module.Dual.eval_apply]
[GOAL]
R✝ : Type u
M✝ : Type v
inst✝⁵ : CommSemiring R✝
inst✝⁴ : AddCommMonoid M✝
inst✝³ : Module R✝ M✝
W : Submodule R✝ M✝
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
⊢ GaloisConnection (↑OrderDual.toDual ∘ dualAnnihilator) (dualCoannihilator ∘ ↑OrderDual.ofDual)
[PROOFSTEP]
intro a b
[GOAL]
R✝ : Type u
M✝ : Type v
inst✝⁵ : CommSemiring R✝
inst✝⁴ : AddCommMonoid M✝
inst✝³ : Module R✝ M✝
W : Submodule R✝ M✝
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
a : Submodule R M
b : (Submodule R (Module.Dual R M))ᵒᵈ
⊢ (↑OrderDual.toDual ∘ dualAnnihilator) a ≤ b ↔ a ≤ (dualCoannihilator ∘ ↑OrderDual.ofDual) b
[PROOFSTEP]
induction b using OrderDual.rec
[GOAL]
case h₂
R✝ : Type u
M✝ : Type v
inst✝⁵ : CommSemiring R✝
inst✝⁴ : AddCommMonoid M✝
inst✝³ : Module R✝ M✝
W : Submodule R✝ M✝
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
a : Submodule R M
a✝ : Submodule R (Module.Dual R M)
⊢ (↑OrderDual.toDual ∘ dualAnnihilator) a ≤ ↑OrderDual.toDual a✝ ↔
    a ≤ (dualCoannihilator ∘ ↑OrderDual.ofDual) (↑OrderDual.toDual a✝)
[PROOFSTEP]
simp only [Function.comp_apply, OrderDual.toDual_le_toDual, OrderDual.ofDual_toDual]
[GOAL]
case h₂
R✝ : Type u
M✝ : Type v
inst✝⁵ : CommSemiring R✝
inst✝⁴ : AddCommMonoid M✝
inst✝³ : Module R✝ M✝
W : Submodule R✝ M✝
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
a : Submodule R M
a✝ : Submodule R (Module.Dual R M)
⊢ a✝ ≤ dualAnnihilator a ↔ a ≤ dualCoannihilator a✝
[PROOFSTEP]
constructor
[GOAL]
case h₂.mp
R✝ : Type u
M✝ : Type v
inst✝⁵ : CommSemiring R✝
inst✝⁴ : AddCommMonoid M✝
inst✝³ : Module R✝ M✝
W : Submodule R✝ M✝
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
a : Submodule R M
a✝ : Submodule R (Module.Dual R M)
⊢ a✝ ≤ dualAnnihilator a → a ≤ dualCoannihilator a✝
[PROOFSTEP]
intro h x hx
[GOAL]
case h₂.mp
R✝ : Type u
M✝ : Type v
inst✝⁵ : CommSemiring R✝
inst✝⁴ : AddCommMonoid M✝
inst✝³ : Module R✝ M✝
W : Submodule R✝ M✝
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
a : Submodule R M
a✝ : Submodule R (Module.Dual R M)
h : a✝ ≤ dualAnnihilator a
x : M
hx : x ∈ a
⊢ x ∈ dualCoannihilator a✝
[PROOFSTEP]
simp only [mem_dualAnnihilator, mem_dualCoannihilator]
[GOAL]
case h₂.mp
R✝ : Type u
M✝ : Type v
inst✝⁵ : CommSemiring R✝
inst✝⁴ : AddCommMonoid M✝
inst✝³ : Module R✝ M✝
W : Submodule R✝ M✝
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
a : Submodule R M
a✝ : Submodule R (Module.Dual R M)
h : a✝ ≤ dualAnnihilator a
x : M
hx : x ∈ a
⊢ ∀ (φ : Module.Dual R M), φ ∈ a✝ → ↑φ x = 0
[PROOFSTEP]
intro y hy
[GOAL]
case h₂.mp
R✝ : Type u
M✝ : Type v
inst✝⁵ : CommSemiring R✝
inst✝⁴ : AddCommMonoid M✝
inst✝³ : Module R✝ M✝
W : Submodule R✝ M✝
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
a : Submodule R M
a✝ : Submodule R (Module.Dual R M)
h : a✝ ≤ dualAnnihilator a
x : M
hx : x ∈ a
y : Module.Dual R M
hy : y ∈ a✝
⊢ ↑y x = 0
[PROOFSTEP]
have := h hy
[GOAL]
case h₂.mp
R✝ : Type u
M✝ : Type v
inst✝⁵ : CommSemiring R✝
inst✝⁴ : AddCommMonoid M✝
inst✝³ : Module R✝ M✝
W : Submodule R✝ M✝
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
a : Submodule R M
a✝ : Submodule R (Module.Dual R M)
h : a✝ ≤ dualAnnihilator a
x : M
hx : x ∈ a
y : Module.Dual R M
hy : y ∈ a✝
this : y ∈ dualAnnihilator a
⊢ ↑y x = 0
[PROOFSTEP]
simp only [mem_dualAnnihilator, mem_dualCoannihilator] at this 
[GOAL]
case h₂.mp
R✝ : Type u
M✝ : Type v
inst✝⁵ : CommSemiring R✝
inst✝⁴ : AddCommMonoid M✝
inst✝³ : Module R✝ M✝
W : Submodule R✝ M✝
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
a : Submodule R M
a✝ : Submodule R (Module.Dual R M)
h : a✝ ≤ dualAnnihilator a
x : M
hx : x ∈ a
y : Module.Dual R M
hy : y ∈ a✝
this : ∀ (w : M), w ∈ a → ↑y w = 0
⊢ ↑y x = 0
[PROOFSTEP]
exact this x hx
[GOAL]
case h₂.mpr
R✝ : Type u
M✝ : Type v
inst✝⁵ : CommSemiring R✝
inst✝⁴ : AddCommMonoid M✝
inst✝³ : Module R✝ M✝
W : Submodule R✝ M✝
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
a : Submodule R M
a✝ : Submodule R (Module.Dual R M)
⊢ a ≤ dualCoannihilator a✝ → a✝ ≤ dualAnnihilator a
[PROOFSTEP]
intro h x hx
[GOAL]
case h₂.mpr
R✝ : Type u
M✝ : Type v
inst✝⁵ : CommSemiring R✝
inst✝⁴ : AddCommMonoid M✝
inst✝³ : Module R✝ M✝
W : Submodule R✝ M✝
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
a : Submodule R M
a✝ : Submodule R (Module.Dual R M)
h : a ≤ dualCoannihilator a✝
x : Module.Dual R M
hx : x ∈ a✝
⊢ x ∈ dualAnnihilator a
[PROOFSTEP]
simp only [mem_dualAnnihilator, mem_dualCoannihilator]
[GOAL]
case h₂.mpr
R✝ : Type u
M✝ : Type v
inst✝⁵ : CommSemiring R✝
inst✝⁴ : AddCommMonoid M✝
inst✝³ : Module R✝ M✝
W : Submodule R✝ M✝
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
a : Submodule R M
a✝ : Submodule R (Module.Dual R M)
h : a ≤ dualCoannihilator a✝
x : Module.Dual R M
hx : x ∈ a✝
⊢ ∀ (w : M), w ∈ a → ↑x w = 0
[PROOFSTEP]
intro y hy
[GOAL]
case h₂.mpr
R✝ : Type u
M✝ : Type v
inst✝⁵ : CommSemiring R✝
inst✝⁴ : AddCommMonoid M✝
inst✝³ : Module R✝ M✝
W : Submodule R✝ M✝
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
a : Submodule R M
a✝ : Submodule R (Module.Dual R M)
h : a ≤ dualCoannihilator a✝
x : Module.Dual R M
hx : x ∈ a✝
y : M
hy : y ∈ a
⊢ ↑x y = 0
[PROOFSTEP]
have := h hy
[GOAL]
case h₂.mpr
R✝ : Type u
M✝ : Type v
inst✝⁵ : CommSemiring R✝
inst✝⁴ : AddCommMonoid M✝
inst✝³ : Module R✝ M✝
W : Submodule R✝ M✝
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
a : Submodule R M
a✝ : Submodule R (Module.Dual R M)
h : a ≤ dualCoannihilator a✝
x : Module.Dual R M
hx : x ∈ a✝
y : M
hy : y ∈ a
this : y ∈ dualCoannihilator a✝
⊢ ↑x y = 0
[PROOFSTEP]
simp only [mem_dualAnnihilator, mem_dualCoannihilator] at this 
[GOAL]
case h₂.mpr
R✝ : Type u
M✝ : Type v
inst✝⁵ : CommSemiring R✝
inst✝⁴ : AddCommMonoid M✝
inst✝³ : Module R✝ M✝
W : Submodule R✝ M✝
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
a : Submodule R M
a✝ : Submodule R (Module.Dual R M)
h : a ≤ dualCoannihilator a✝
x : Module.Dual R M
hx : x ∈ a✝
y : M
hy : y ∈ a
this : ∀ (φ : Module.Dual R M), φ ∈ a✝ → ↑φ y = 0
⊢ ↑x y = 0
[PROOFSTEP]
exact this x hx
[GOAL]
R : Type u
M : Type v
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
W : Submodule R M
⊢ dualAnnihilator ⊤ = ⊥
[PROOFSTEP]
rw [eq_bot_iff]
[GOAL]
R : Type u
M : Type v
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
W : Submodule R M
⊢ dualAnnihilator ⊤ ≤ ⊥
[PROOFSTEP]
intro v
[GOAL]
R : Type u
M : Type v
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
W : Submodule R M
v : Module.Dual R M
⊢ v ∈ dualAnnihilator ⊤ → v ∈ ⊥
[PROOFSTEP]
simp_rw [mem_dualAnnihilator, mem_bot, mem_top, forall_true_left]
[GOAL]
R : Type u
M : Type v
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
W : Submodule R M
v : Module.Dual R M
⊢ (∀ (w : M), ↑v w = 0) → v = 0
[PROOFSTEP]
exact fun h => LinearMap.ext h
[GOAL]
R : Type u
M : Type v
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
W U V : Submodule R M
⊢ dualAnnihilator U ⊔ dualAnnihilator V ≤ dualAnnihilator (U ⊓ V)
[PROOFSTEP]
rw [le_dualAnnihilator_iff_le_dualCoannihilator, dualCoannihilator_sup_eq]
[GOAL]
R : Type u
M : Type v
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
W U V : Submodule R M
⊢ U ⊓ V ≤ dualCoannihilator (dualAnnihilator U) ⊓ dualCoannihilator (dualAnnihilator V)
[PROOFSTEP]
apply inf_le_inf
[GOAL]
case h₁
R : Type u
M : Type v
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
W U V : Submodule R M
⊢ U ≤ dualCoannihilator (dualAnnihilator U)
[PROOFSTEP]
exact le_dualAnnihilator_dualCoannihilator _
[GOAL]
case h₂
R : Type u
M : Type v
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
W U V : Submodule R M
⊢ V ≤ dualCoannihilator (dualAnnihilator V)
[PROOFSTEP]
exact le_dualAnnihilator_dualCoannihilator _
[GOAL]
R : Type u
M : Type v
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
W : Submodule R M
ι : Type u_1
U : ι → Submodule R M
⊢ ⨆ (i : ι), dualAnnihilator (U i) ≤ dualAnnihilator (⨅ (i : ι), U i)
[PROOFSTEP]
rw [le_dualAnnihilator_iff_le_dualCoannihilator, dualCoannihilator_iSup_eq]
[GOAL]
R : Type u
M : Type v
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
W : Submodule R M
ι : Type u_1
U : ι → Submodule R M
⊢ ⨅ (i : ι), U i ≤ ⨅ (i : ι), dualCoannihilator (dualAnnihilator (U i))
[PROOFSTEP]
apply iInf_mono
[GOAL]
case h
R : Type u
M : Type v
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
W : Submodule R M
ι : Type u_1
U : ι → Submodule R M
⊢ ∀ (i : ι), U i ≤ dualCoannihilator (dualAnnihilator (U i))
[PROOFSTEP]
exact fun i : ι => le_dualAnnihilator_dualCoannihilator (U i)
[GOAL]
K : Type u
V : Type v
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
W : Subspace K V
⊢ dualCoannihilator ⊤ = ⊥
[PROOFSTEP]
rw [dualCoannihilator, dualAnnihilator_top, comap_bot, Module.eval_ker]
[GOAL]
K : Type u
V : Type v
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
W : Subspace K V
⊢ dualCoannihilator (dualAnnihilator W) = W
[PROOFSTEP]
refine' le_antisymm _ (le_dualAnnihilator_dualCoannihilator _)
[GOAL]
K : Type u
V : Type v
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
W : Subspace K V
⊢ dualCoannihilator (dualAnnihilator W) ≤ W
[PROOFSTEP]
intro v
[GOAL]
K : Type u
V : Type v
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
W : Subspace K V
v : V
⊢ v ∈ dualCoannihilator (dualAnnihilator W) → v ∈ W
[PROOFSTEP]
simp only [mem_dualAnnihilator, mem_dualCoannihilator]
[GOAL]
K : Type u
V : Type v
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
W : Subspace K V
v : V
⊢ (∀ (φ : Module.Dual K V), (∀ (w : V), w ∈ W → ↑φ w = 0) → ↑φ v = 0) → v ∈ W
[PROOFSTEP]
contrapose!
[GOAL]
K : Type u
V : Type v
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
W : Subspace K V
v : V
⊢ ¬v ∈ W → ∃ φ, (∀ (w : V), w ∈ W → ↑φ w = 0) ∧ ↑φ v ≠ 0
[PROOFSTEP]
intro hv
[GOAL]
K : Type u
V : Type v
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
W : Subspace K V
v : V
hv : ¬v ∈ W
⊢ ∃ φ, (∀ (w : V), w ∈ W → ↑φ w = 0) ∧ ↑φ v ≠ 0
[PROOFSTEP]
obtain ⟨W', hW⟩ := Submodule.exists_isCompl W
[GOAL]
case intro
K : Type u
V : Type v
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
W : Subspace K V
v : V
hv : ¬v ∈ W
W' : Submodule K V
hW : IsCompl W W'
⊢ ∃ φ, (∀ (w : V), w ∈ W → ↑φ w = 0) ∧ ↑φ v ≠ 0
[PROOFSTEP]
obtain ⟨⟨w, w'⟩, rfl, -⟩ := existsUnique_add_of_isCompl_prod hW v
[GOAL]
case intro.intro.mk.intro
K : Type u
V : Type v
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
W : Subspace K V
W' : Submodule K V
hW : IsCompl W W'
w : { x // x ∈ W }
w' : { x // x ∈ W' }
hv : ¬↑(w, w').fst + ↑(w, w').snd ∈ W
⊢ ∃ φ, (∀ (w : V), w ∈ W → ↑φ w = 0) ∧ ↑φ (↑(w, w').fst + ↑(w, w').snd) ≠ 0
[PROOFSTEP]
have hw'n : (w' : V) ∉ W := by
  contrapose! hv
  exact Submodule.add_mem W w.2 hv
[GOAL]
K : Type u
V : Type v
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
W : Subspace K V
W' : Submodule K V
hW : IsCompl W W'
w : { x // x ∈ W }
w' : { x // x ∈ W' }
hv : ¬↑(w, w').fst + ↑(w, w').snd ∈ W
⊢ ¬↑w' ∈ W
[PROOFSTEP]
contrapose! hv
[GOAL]
K : Type u
V : Type v
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
W : Subspace K V
W' : Submodule K V
hW : IsCompl W W'
w : { x // x ∈ W }
w' : { x // x ∈ W' }
hv : ↑w' ∈ W
⊢ ↑w + ↑w' ∈ W
[PROOFSTEP]
exact Submodule.add_mem W w.2 hv
[GOAL]
case intro.intro.mk.intro
K : Type u
V : Type v
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
W : Subspace K V
W' : Submodule K V
hW : IsCompl W W'
w : { x // x ∈ W }
w' : { x // x ∈ W' }
hv : ¬↑(w, w').fst + ↑(w, w').snd ∈ W
hw'n : ¬↑w' ∈ W
⊢ ∃ φ, (∀ (w : V), w ∈ W → ↑φ w = 0) ∧ ↑φ (↑(w, w').fst + ↑(w, w').snd) ≠ 0
[PROOFSTEP]
have hw'nz : w' ≠ 0 := by
  rintro rfl
  exact hw'n (Submodule.zero_mem W)
[GOAL]
K : Type u
V : Type v
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
W : Subspace K V
W' : Submodule K V
hW : IsCompl W W'
w : { x // x ∈ W }
w' : { x // x ∈ W' }
hv : ¬↑(w, w').fst + ↑(w, w').snd ∈ W
hw'n : ¬↑w' ∈ W
⊢ w' ≠ 0
[PROOFSTEP]
rintro rfl
[GOAL]
K : Type u
V : Type v
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
W : Subspace K V
W' : Submodule K V
hW : IsCompl W W'
w : { x // x ∈ W }
hv : ¬↑(w, 0).fst + ↑(w, 0).snd ∈ W
hw'n : ¬↑0 ∈ W
⊢ False
[PROOFSTEP]
exact hw'n (Submodule.zero_mem W)
[GOAL]
case intro.intro.mk.intro
K : Type u
V : Type v
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
W : Subspace K V
W' : Submodule K V
hW : IsCompl W W'
w : { x // x ∈ W }
w' : { x // x ∈ W' }
hv : ¬↑(w, w').fst + ↑(w, w').snd ∈ W
hw'n : ¬↑w' ∈ W
hw'nz : w' ≠ 0
⊢ ∃ φ, (∀ (w : V), w ∈ W → ↑φ w = 0) ∧ ↑φ (↑(w, w').fst + ↑(w, w').snd) ≠ 0
[PROOFSTEP]
rw [Ne.def, ← Module.forall_dual_apply_eq_zero_iff K w'] at hw'nz 
[GOAL]
case intro.intro.mk.intro
K : Type u
V : Type v
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
W : Subspace K V
W' : Submodule K V
hW : IsCompl W W'
w : { x // x ∈ W }
w' : { x // x ∈ W' }
hv : ¬↑(w, w').fst + ↑(w, w').snd ∈ W
hw'n : ¬↑w' ∈ W
hw'nz : ¬∀ (φ : Module.Dual K { x // x ∈ W' }), ↑φ w' = 0
⊢ ∃ φ, (∀ (w : V), w ∈ W → ↑φ w = 0) ∧ ↑φ (↑(w, w').fst + ↑(w, w').snd) ≠ 0
[PROOFSTEP]
push_neg at hw'nz 
[GOAL]
case intro.intro.mk.intro
K : Type u
V : Type v
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
W : Subspace K V
W' : Submodule K V
hW : IsCompl W W'
w : { x // x ∈ W }
w' : { x // x ∈ W' }
hv : ¬↑(w, w').fst + ↑(w, w').snd ∈ W
hw'n : ¬↑w' ∈ W
hw'nz : ∃ φ, ↑φ w' ≠ 0
⊢ ∃ φ, (∀ (w : V), w ∈ W → ↑φ w = 0) ∧ ↑φ (↑(w, w').fst + ↑(w, w').snd) ≠ 0
[PROOFSTEP]
obtain ⟨φ, hφ⟩ := hw'nz
[GOAL]
case intro.intro.mk.intro.intro
K : Type u
V : Type v
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
W : Subspace K V
W' : Submodule K V
hW : IsCompl W W'
w : { x // x ∈ W }
w' : { x // x ∈ W' }
hv : ¬↑(w, w').fst + ↑(w, w').snd ∈ W
hw'n : ¬↑w' ∈ W
φ : Module.Dual K { x // x ∈ W' }
hφ : ↑φ w' ≠ 0
⊢ ∃ φ, (∀ (w : V), w ∈ W → ↑φ w = 0) ∧ ↑φ (↑(w, w').fst + ↑(w, w').snd) ≠ 0
[PROOFSTEP]
exists ((LinearMap.ofIsComplProd hW).comp (LinearMap.inr _ _ _)) φ
[GOAL]
case intro.intro.mk.intro.intro
K : Type u
V : Type v
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
W : Subspace K V
W' : Submodule K V
hW : IsCompl W W'
w : { x // x ∈ W }
w' : { x // x ∈ W' }
hv : ¬↑(w, w').fst + ↑(w, w').snd ∈ W
hw'n : ¬↑w' ∈ W
φ : Module.Dual K { x // x ∈ W' }
hφ : ↑φ w' ≠ 0
⊢ (∀ (w : V),
      w ∈ W → ↑(↑(comp (ofIsComplProd hW) (inr K ({ x // x ∈ W } →ₗ[K] K) ({ x // x ∈ W' } →ₗ[K] K))) φ) w = 0) ∧
    ↑(↑(comp (ofIsComplProd hW) (inr K ({ x // x ∈ W } →ₗ[K] K) ({ x // x ∈ W' } →ₗ[K] K))) φ)
        (↑(w, w').fst + ↑(w, w').snd) ≠
      0
[PROOFSTEP]
simp only [coe_comp, coe_inr, Function.comp_apply, ofIsComplProd_apply, map_add, ofIsCompl_left_apply, zero_apply,
  ofIsCompl_right_apply, zero_add, Ne.def]
[GOAL]
case intro.intro.mk.intro.intro
K : Type u
V : Type v
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
W : Subspace K V
W' : Submodule K V
hW : IsCompl W W'
w : { x // x ∈ W }
w' : { x // x ∈ W' }
hv : ¬↑(w, w').fst + ↑(w, w').snd ∈ W
hw'n : ¬↑w' ∈ W
φ : Module.Dual K { x // x ∈ W' }
hφ : ↑φ w' ≠ 0
⊢ (∀ (w : V), w ∈ W → ↑(ofIsCompl hW 0 φ) w = 0) ∧ ¬↑φ w' = 0
[PROOFSTEP]
refine' ⟨_, hφ⟩
[GOAL]
case intro.intro.mk.intro.intro
K : Type u
V : Type v
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
W : Subspace K V
W' : Submodule K V
hW : IsCompl W W'
w : { x // x ∈ W }
w' : { x // x ∈ W' }
hv : ¬↑(w, w').fst + ↑(w, w').snd ∈ W
hw'n : ¬↑w' ∈ W
φ : Module.Dual K { x // x ∈ W' }
hφ : ↑φ w' ≠ 0
⊢ ∀ (w : V), w ∈ W → ↑(ofIsCompl hW 0 φ) w = 0
[PROOFSTEP]
intro v hv
[GOAL]
case intro.intro.mk.intro.intro
K : Type u
V : Type v
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
W : Subspace K V
W' : Submodule K V
hW : IsCompl W W'
w : { x // x ∈ W }
w' : { x // x ∈ W' }
hv✝ : ¬↑(w, w').fst + ↑(w, w').snd ∈ W
hw'n : ¬↑w' ∈ W
φ : Module.Dual K { x // x ∈ W' }
hφ : ↑φ w' ≠ 0
v : V
hv : v ∈ W
⊢ ↑(ofIsCompl hW 0 φ) v = 0
[PROOFSTEP]
apply LinearMap.ofIsCompl_left_apply hW ⟨v, hv⟩
[GOAL]
K : Type u
V : Type v
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
W : Subspace K V
v : V
⊢ (∀ (φ : Module.Dual K V), φ ∈ dualAnnihilator W → ↑φ v = 0) ↔ v ∈ W
[PROOFSTEP]
rw [← SetLike.ext_iff.mp dualAnnihilator_dualCoannihilator_eq v, mem_dualCoannihilator]
[GOAL]
K : Type u
V : Type v
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
W W' : Subspace K V
⊢ dualAnnihilator W = dualAnnihilator W' ↔ W = W'
[PROOFSTEP]
constructor
[GOAL]
case mp
K : Type u
V : Type v
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
W W' : Subspace K V
⊢ dualAnnihilator W = dualAnnihilator W' → W = W'
[PROOFSTEP]
apply (dualAnnihilatorGci K V).l_injective
[GOAL]
case mpr
K : Type u
V : Type v
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
W W' : Subspace K V
⊢ W = W' → dualAnnihilator W = dualAnnihilator W'
[PROOFSTEP]
rintro rfl
[GOAL]
case mpr
K : Type u
V : Type v
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
W : Subspace K V
⊢ dualAnnihilator W = dualAnnihilator W
[PROOFSTEP]
rfl
[GOAL]
K : Type u
V : Type v
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
W : Subspace K V
φ : Module.Dual K { x // x ∈ W }
w : { x // x ∈ W }
⊢ ↑(↑(dualLift W) φ) ↑w = ↑φ w
[PROOFSTEP]
erw [ofIsCompl_left_apply _ w]
[GOAL]
K : Type u
V : Type v
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
W : Subspace K V
φ : Module.Dual K { x // x ∈ W }
w : { x // x ∈ W }
⊢ ↑(↑(inl K (Module.Dual K { x // x ∈ W })
                ({ x // x ∈ ↑(Classical.indefiniteDescription (fun x => IsCompl W x) (_ : ∃ q, IsCompl W q)) } →ₗ[K] K))
            φ).fst
      w =
    ↑φ w
[PROOFSTEP]
rfl
[GOAL]
K : Type u
V : Type v
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
W : Subspace K V
φ : Module.Dual K { x // x ∈ W }
w : V
hw : w ∈ W
⊢ ↑(↑(dualLift W) φ) w = ↑φ { val := w, property := hw }
[PROOFSTEP]
convert dualLift_of_subtype ⟨w, hw⟩
[GOAL]
K : Type u
V : Type v
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
W✝ W : Subspace K V
⊢ comp (dualRestrict W) (dualLift W) = 1
[PROOFSTEP]
ext φ x
[GOAL]
case h.h
K : Type u
V : Type v
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
W✝ W : Subspace K V
φ : Module.Dual K { x // x ∈ W }
x : { x // x ∈ W }
⊢ ↑(↑(comp (dualRestrict W) (dualLift W)) φ) x = ↑(↑1 φ) x
[PROOFSTEP]
simp
[GOAL]
K : Type u
V : Type v
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
W✝ W : Subspace K V
x : Module.Dual K { x // x ∈ W }
⊢ ↑(comp (dualRestrict W) (dualLift W)) x = x
[PROOFSTEP]
rw [dualRestrict_comp_dualLift]
[GOAL]
K : Type u
V : Type v
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
W✝ W : Subspace K V
x : Module.Dual K { x // x ∈ W }
⊢ ↑1 x = x
[PROOFSTEP]
rfl
[GOAL]
K : Type u
V : Type v
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
W✝ W : Subspace K V
φ : Module.Dual K V
⊢ ↑(quotAnnihilatorEquiv W) (Submodule.Quotient.mk φ) = ↑(dualRestrict W) φ
[PROOFSTEP]
ext
[GOAL]
case h
K : Type u
V : Type v
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
W✝ W : Subspace K V
φ : Module.Dual K V
x✝ : { x // x ∈ W }
⊢ ↑(↑(quotAnnihilatorEquiv W) (Submodule.Quotient.mk φ)) x✝ = ↑(↑(dualRestrict W) φ) x✝
[PROOFSTEP]
rfl
[GOAL]
K : Type u
V : Type v
inst✝⁴ : Field K
inst✝³ : AddCommGroup V
inst✝² : Module K V
W : Subspace K V
V₁ : Type u_1
inst✝¹ : AddCommGroup V₁
inst✝ : Module K V₁
H : FiniteDimensional K V
⊢ FiniteDimensional K (Module.Dual K V)
[PROOFSTEP]
infer_instance
[GOAL]
K : Type u
V : Type v
inst✝⁶ : Field K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
W✝ : Subspace K V
V₁ : Type u_1
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : FiniteDimensional K V
inst✝ : FiniteDimensional K V₁
W : Subspace K V
⊢ dualAnnihilator (dualAnnihilator W) = ↑(Module.mapEvalEquiv K V) W
[PROOFSTEP]
have : _ = W := Subspace.dualAnnihilator_dualCoannihilator_eq
[GOAL]
K : Type u
V : Type v
inst✝⁶ : Field K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
W✝ : Subspace K V
V₁ : Type u_1
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : FiniteDimensional K V
inst✝ : FiniteDimensional K V₁
W : Subspace K V
this : dualCoannihilator (dualAnnihilator W) = W
⊢ dualAnnihilator (dualAnnihilator W) = ↑(Module.mapEvalEquiv K V) W
[PROOFSTEP]
rw [dualCoannihilator, ← Module.mapEvalEquiv_symm_apply] at this 
[GOAL]
K : Type u
V : Type v
inst✝⁶ : Field K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
W✝ : Subspace K V
V₁ : Type u_1
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : FiniteDimensional K V
inst✝ : FiniteDimensional K V₁
W : Subspace K V
this : ↑(OrderIso.symm (Module.mapEvalEquiv K V)) (dualAnnihilator (dualAnnihilator W)) = W
⊢ dualAnnihilator (dualAnnihilator W) = ↑(Module.mapEvalEquiv K V) W
[PROOFSTEP]
rwa [← OrderIso.symm_apply_eq]
[GOAL]
K : Type u
V : Type v
inst✝⁶ : Field K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
W : Subspace K V
V₁ : Type u_1
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : FiniteDimensional K V
inst✝ : FiniteDimensional K V₁
⊢ finrank K (Module.Dual K V) = finrank K V
[PROOFSTEP]
classical exact LinearEquiv.finrank_eq (Basis.ofVectorSpace K V).toDualEquiv.symm
[GOAL]
K : Type u
V : Type v
inst✝⁶ : Field K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
W : Subspace K V
V₁ : Type u_1
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : FiniteDimensional K V
inst✝ : FiniteDimensional K V₁
⊢ finrank K (Module.Dual K V) = finrank K V
[PROOFSTEP]
exact LinearEquiv.finrank_eq (Basis.ofVectorSpace K V).toDualEquiv.symm
[GOAL]
K : Type u
V : Type v
inst✝⁶ : Field K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
W : Subspace K V
V₁ : Type u_1
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : FiniteDimensional K V
inst✝ : FiniteDimensional K V₁
Φ : Subspace K (Module.Dual K V)
⊢ finrank K { x // x ∈ dualCoannihilator Φ } = finrank K { x // x ∈ dualAnnihilator Φ }
[PROOFSTEP]
rw [Submodule.dualCoannihilator, ← Module.evalEquiv_toLinearMap]
[GOAL]
K : Type u
V : Type v
inst✝⁶ : Field K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
W : Subspace K V
V₁ : Type u_1
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : FiniteDimensional K V
inst✝ : FiniteDimensional K V₁
Φ : Subspace K (Module.Dual K V)
⊢ finrank K { x // x ∈ comap (↑(Module.evalEquiv K V)) (dualAnnihilator Φ) } = finrank K { x // x ∈ dualAnnihilator Φ }
[PROOFSTEP]
exact LinearEquiv.finrank_eq (LinearEquiv.ofSubmodule' _ _)
[GOAL]
K : Type u
V : Type v
inst✝⁶ : Field K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
W✝ : Subspace K V
V₁ : Type u_1
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : FiniteDimensional K V
inst✝ : FiniteDimensional K V₁
W : Subspace K (Module.Dual K V)
⊢ finrank K { x // x ∈ W } + finrank K { x // x ∈ dualCoannihilator W } = finrank K V
[PROOFSTEP]
rw [finrank_dualCoannihilator_eq]
  -- Porting note: LinearEquiv.finrank_eq needs help
[GOAL]
K : Type u
V : Type v
inst✝⁶ : Field K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
W✝ : Subspace K V
V₁ : Type u_1
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : FiniteDimensional K V
inst✝ : FiniteDimensional K V₁
W : Subspace K (Module.Dual K V)
⊢ finrank K { x // x ∈ W } + finrank K { x // x ∈ dualAnnihilator W } = finrank K V
[PROOFSTEP]
let equiv := W.quotEquivAnnihilator
[GOAL]
K : Type u
V : Type v
inst✝⁶ : Field K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
W✝ : Subspace K V
V₁ : Type u_1
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : FiniteDimensional K V
inst✝ : FiniteDimensional K V₁
W : Subspace K (Module.Dual K V)
equiv : (Module.Dual K V ⧸ W) ≃ₗ[K] { x // x ∈ dualAnnihilator W } := quotEquivAnnihilator W
⊢ finrank K { x // x ∈ W } + finrank K { x // x ∈ dualAnnihilator W } = finrank K V
[PROOFSTEP]
have eq := LinearEquiv.finrank_eq (R := K) (M := (Module.Dual K V) ⧸ W) (M₂ := { x // x ∈ dualAnnihilator W }) equiv
[GOAL]
K : Type u
V : Type v
inst✝⁶ : Field K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
W✝ : Subspace K V
V₁ : Type u_1
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : FiniteDimensional K V
inst✝ : FiniteDimensional K V₁
W : Subspace K (Module.Dual K V)
equiv : (Module.Dual K V ⧸ W) ≃ₗ[K] { x // x ∈ dualAnnihilator W } := quotEquivAnnihilator W
eq : finrank K (Module.Dual K V ⧸ W) = finrank K { x // x ∈ dualAnnihilator W }
⊢ finrank K { x // x ∈ W } + finrank K { x // x ∈ dualAnnihilator W } = finrank K V
[PROOFSTEP]
rw [eq.symm, add_comm, Submodule.finrank_quotient_add_finrank, Subspace.dual_finrank_eq]
[GOAL]
R : Type u
inst✝⁴ : CommSemiring R
M₁ : Type v
M₂ : Type v'
inst✝³ : AddCommMonoid M₁
inst✝² : Module R M₁
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
f : M₁ →ₗ[R] M₂
⊢ ker (dualMap f) = Submodule.dualAnnihilator (range f)
[PROOFSTEP]
ext φ
[GOAL]
case h
R : Type u
inst✝⁴ : CommSemiring R
M₁ : Type v
M₂ : Type v'
inst✝³ : AddCommMonoid M₁
inst✝² : Module R M₁
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
f : M₁ →ₗ[R] M₂
φ : Dual R M₂
⊢ φ ∈ ker (dualMap f) ↔ φ ∈ Submodule.dualAnnihilator (range f)
[PROOFSTEP]
constructor
[GOAL]
case h.mp
R : Type u
inst✝⁴ : CommSemiring R
M₁ : Type v
M₂ : Type v'
inst✝³ : AddCommMonoid M₁
inst✝² : Module R M₁
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
f : M₁ →ₗ[R] M₂
φ : Dual R M₂
⊢ φ ∈ ker (dualMap f) → φ ∈ Submodule.dualAnnihilator (range f)
[PROOFSTEP]
intro hφ
[GOAL]
case h.mpr
R : Type u
inst✝⁴ : CommSemiring R
M₁ : Type v
M₂ : Type v'
inst✝³ : AddCommMonoid M₁
inst✝² : Module R M₁
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
f : M₁ →ₗ[R] M₂
φ : Dual R M₂
⊢ φ ∈ Submodule.dualAnnihilator (range f) → φ ∈ ker (dualMap f)
[PROOFSTEP]
intro hφ
[GOAL]
case h.mp
R : Type u
inst✝⁴ : CommSemiring R
M₁ : Type v
M₂ : Type v'
inst✝³ : AddCommMonoid M₁
inst✝² : Module R M₁
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
f : M₁ →ₗ[R] M₂
φ : Dual R M₂
hφ : φ ∈ ker (dualMap f)
⊢ φ ∈ Submodule.dualAnnihilator (range f)
[PROOFSTEP]
rw [mem_ker] at hφ 
[GOAL]
case h.mp
R : Type u
inst✝⁴ : CommSemiring R
M₁ : Type v
M₂ : Type v'
inst✝³ : AddCommMonoid M₁
inst✝² : Module R M₁
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
f : M₁ →ₗ[R] M₂
φ : Dual R M₂
hφ : ↑(dualMap f) φ = 0
⊢ φ ∈ Submodule.dualAnnihilator (range f)
[PROOFSTEP]
rw [Submodule.mem_dualAnnihilator]
[GOAL]
case h.mp
R : Type u
inst✝⁴ : CommSemiring R
M₁ : Type v
M₂ : Type v'
inst✝³ : AddCommMonoid M₁
inst✝² : Module R M₁
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
f : M₁ →ₗ[R] M₂
φ : Dual R M₂
hφ : ↑(dualMap f) φ = 0
⊢ ∀ (w : M₂), w ∈ range f → ↑φ w = 0
[PROOFSTEP]
rintro y ⟨x, rfl⟩
[GOAL]
case h.mp.intro
R : Type u
inst✝⁴ : CommSemiring R
M₁ : Type v
M₂ : Type v'
inst✝³ : AddCommMonoid M₁
inst✝² : Module R M₁
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
f : M₁ →ₗ[R] M₂
φ : Dual R M₂
hφ : ↑(dualMap f) φ = 0
x : M₁
⊢ ↑φ (↑f x) = 0
[PROOFSTEP]
rw [← dualMap_apply, hφ, zero_apply]
[GOAL]
case h.mpr
R : Type u
inst✝⁴ : CommSemiring R
M₁ : Type v
M₂ : Type v'
inst✝³ : AddCommMonoid M₁
inst✝² : Module R M₁
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
f : M₁ →ₗ[R] M₂
φ : Dual R M₂
hφ : φ ∈ Submodule.dualAnnihilator (range f)
⊢ φ ∈ ker (dualMap f)
[PROOFSTEP]
ext x
[GOAL]
case h.mpr.h
R : Type u
inst✝⁴ : CommSemiring R
M₁ : Type v
M₂ : Type v'
inst✝³ : AddCommMonoid M₁
inst✝² : Module R M₁
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
f : M₁ →ₗ[R] M₂
φ : Dual R M₂
hφ : φ ∈ Submodule.dualAnnihilator (range f)
x : M₁
⊢ ↑(↑(dualMap f) φ) x = ↑0 x
[PROOFSTEP]
rw [dualMap_apply]
[GOAL]
case h.mpr.h
R : Type u
inst✝⁴ : CommSemiring R
M₁ : Type v
M₂ : Type v'
inst✝³ : AddCommMonoid M₁
inst✝² : Module R M₁
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
f : M₁ →ₗ[R] M₂
φ : Dual R M₂
hφ : φ ∈ Submodule.dualAnnihilator (range f)
x : M₁
⊢ ↑φ (↑f x) = ↑0 x
[PROOFSTEP]
rw [Submodule.mem_dualAnnihilator] at hφ 
[GOAL]
case h.mpr.h
R : Type u
inst✝⁴ : CommSemiring R
M₁ : Type v
M₂ : Type v'
inst✝³ : AddCommMonoid M₁
inst✝² : Module R M₁
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
f : M₁ →ₗ[R] M₂
φ : Dual R M₂
hφ : ∀ (w : M₂), w ∈ range f → ↑φ w = 0
x : M₁
⊢ ↑φ (↑f x) = ↑0 x
[PROOFSTEP]
exact hφ (f x) ⟨x, rfl⟩
[GOAL]
R : Type u
inst✝⁴ : CommSemiring R
M₁ : Type v
M₂ : Type v'
inst✝³ : AddCommMonoid M₁
inst✝² : Module R M₁
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
f : M₁ →ₗ[R] M₂
⊢ range (dualMap f) ≤ Submodule.dualAnnihilator (ker f)
[PROOFSTEP]
rintro _ ⟨ψ, rfl⟩
[GOAL]
case intro
R : Type u
inst✝⁴ : CommSemiring R
M₁ : Type v
M₂ : Type v'
inst✝³ : AddCommMonoid M₁
inst✝² : Module R M₁
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
f : M₁ →ₗ[R] M₂
ψ : Dual R M₂
⊢ ↑(dualMap f) ψ ∈ Submodule.dualAnnihilator (ker f)
[PROOFSTEP]
simp_rw [Submodule.mem_dualAnnihilator, mem_ker]
[GOAL]
case intro
R : Type u
inst✝⁴ : CommSemiring R
M₁ : Type v
M₂ : Type v'
inst✝³ : AddCommMonoid M₁
inst✝² : Module R M₁
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
f : M₁ →ₗ[R] M₂
ψ : Dual R M₂
⊢ ∀ (w : M₁), ↑f w = 0 → ↑(↑(dualMap f) ψ) w = 0
[PROOFSTEP]
rintro x hx
[GOAL]
case intro
R : Type u
inst✝⁴ : CommSemiring R
M₁ : Type v
M₂ : Type v'
inst✝³ : AddCommMonoid M₁
inst✝² : Module R M₁
inst✝¹ : AddCommMonoid M₂
inst✝ : Module R M₂
f : M₁ →ₗ[R] M₂
ψ : Dual R M₂
x : M₁
hx : ↑f x = 0
⊢ ↑(↑(dualMap f) ψ) x = 0
[PROOFSTEP]
rw [dualMap_apply, hx, map_zero]
[GOAL]
R : Type u_1
M : Type u_2
M' : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup M'
inst✝ : Module R M'
W : Submodule R M
⊢ W ≤ LinearMap.ker (LinearMap.flip (LinearMap.domRestrict (dualPairing R M) (dualAnnihilator W)))
[PROOFSTEP]
intro w hw
[GOAL]
R : Type u_1
M : Type u_2
M' : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup M'
inst✝ : Module R M'
W : Submodule R M
w : M
hw : w ∈ W
⊢ w ∈ LinearMap.ker (LinearMap.flip (LinearMap.domRestrict (dualPairing R M) (dualAnnihilator W)))
[PROOFSTEP]
ext ⟨φ, hφ⟩
[GOAL]
case h.mk
R : Type u_1
M : Type u_2
M' : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup M'
inst✝ : Module R M'
W : Submodule R M
w : M
hw : w ∈ W
φ : Dual R M
hφ : φ ∈ dualAnnihilator W
⊢ ↑(↑(LinearMap.flip (LinearMap.domRestrict (dualPairing R M) (dualAnnihilator W))) w) { val := φ, property := hφ } =
    ↑0 { val := φ, property := hφ }
[PROOFSTEP]
exact (mem_dualAnnihilator φ).mp hφ w hw
[GOAL]
R : Type u_1
M : Type u_2
M' : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup M'
inst✝ : Module R M'
W : Submodule R M
φ ψ : { x // x ∈ dualAnnihilator W }
h : (fun φ => ↑↑φ) φ = (fun φ => ↑↑φ) ψ
⊢ φ = ψ
[PROOFSTEP]
ext
[GOAL]
case a.h
R : Type u_1
M : Type u_2
M' : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup M'
inst✝ : Module R M'
W : Submodule R M
φ ψ : { x // x ∈ dualAnnihilator W }
h : (fun φ => ↑↑φ) φ = (fun φ => ↑↑φ) ψ
x✝ : M
⊢ ↑↑φ x✝ = ↑↑ψ x✝
[PROOFSTEP]
simp only [Function.funext_iff] at h 
[GOAL]
case a.h
R : Type u_1
M : Type u_2
M' : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup M'
inst✝ : Module R M'
W : Submodule R M
φ ψ : { x // x ∈ dualAnnihilator W }
x✝ : M
h : ∀ (a : M), ↑↑φ a = ↑↑ψ a
⊢ ↑↑φ x✝ = ↑↑ψ x✝
[PROOFSTEP]
exact h _
[GOAL]
R : Type u_1
M : Type u_2
M' : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup M'
inst✝ : Module R M'
W : Submodule R M
⊢ LinearMap.range (LinearMap.dualMap (mkQ W)) = dualAnnihilator W
[PROOFSTEP]
ext φ
[GOAL]
case h
R : Type u_1
M : Type u_2
M' : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup M'
inst✝ : Module R M'
W : Submodule R M
φ : Dual R M
⊢ φ ∈ LinearMap.range (LinearMap.dualMap (mkQ W)) ↔ φ ∈ dualAnnihilator W
[PROOFSTEP]
rw [LinearMap.mem_range]
[GOAL]
case h
R : Type u_1
M : Type u_2
M' : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup M'
inst✝ : Module R M'
W : Submodule R M
φ : Dual R M
⊢ (∃ y, ↑(LinearMap.dualMap (mkQ W)) y = φ) ↔ φ ∈ dualAnnihilator W
[PROOFSTEP]
constructor
[GOAL]
case h.mp
R : Type u_1
M : Type u_2
M' : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup M'
inst✝ : Module R M'
W : Submodule R M
φ : Dual R M
⊢ (∃ y, ↑(LinearMap.dualMap (mkQ W)) y = φ) → φ ∈ dualAnnihilator W
[PROOFSTEP]
rintro ⟨ψ, rfl⟩
[GOAL]
case h.mp.intro
R : Type u_1
M : Type u_2
M' : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup M'
inst✝ : Module R M'
W : Submodule R M
ψ : Dual R (M ⧸ W)
⊢ ↑(LinearMap.dualMap (mkQ W)) ψ ∈ dualAnnihilator W
[PROOFSTEP]
have := LinearMap.mem_range_self W.mkQ.dualMap ψ
[GOAL]
case h.mp.intro
R : Type u_1
M : Type u_2
M' : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup M'
inst✝ : Module R M'
W : Submodule R M
ψ : Dual R (M ⧸ W)
this : ↑(LinearMap.dualMap (mkQ W)) ψ ∈ LinearMap.range (LinearMap.dualMap (mkQ W))
⊢ ↑(LinearMap.dualMap (mkQ W)) ψ ∈ dualAnnihilator W
[PROOFSTEP]
simpa only [ker_mkQ] using LinearMap.range_dualMap_le_dualAnnihilator_ker W.mkQ this
[GOAL]
case h.mpr
R : Type u_1
M : Type u_2
M' : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup M'
inst✝ : Module R M'
W : Submodule R M
φ : Dual R M
⊢ φ ∈ dualAnnihilator W → ∃ y, ↑(LinearMap.dualMap (mkQ W)) y = φ
[PROOFSTEP]
intro hφ
[GOAL]
case h.mpr
R : Type u_1
M : Type u_2
M' : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup M'
inst✝ : Module R M'
W : Submodule R M
φ : Dual R M
hφ : φ ∈ dualAnnihilator W
⊢ ∃ y, ↑(LinearMap.dualMap (mkQ W)) y = φ
[PROOFSTEP]
exists W.dualCopairing ⟨φ, hφ⟩
[GOAL]
R : Type u_1
M : Type u_2
M' : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup M'
inst✝ : Module R M'
W : Submodule R M
⊢ LinearMap.comp
      (LinearMap.codRestrict (dualAnnihilator W) (LinearMap.dualMap (mkQ W))
        (_ : ∀ (φ : Dual R (M ⧸ W)), ↑(LinearMap.dualMap (mkQ W)) φ ∈ dualAnnihilator W))
      (dualCopairing W) =
    LinearMap.id
[PROOFSTEP]
ext
[GOAL]
case h.a.h
R : Type u_1
M : Type u_2
M' : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup M'
inst✝ : Module R M'
W : Submodule R M
x✝¹ : { x // x ∈ dualAnnihilator W }
x✝ : M
⊢ ↑↑(↑(LinearMap.comp
                (LinearMap.codRestrict (dualAnnihilator W) (LinearMap.dualMap (mkQ W))
                  (_ : ∀ (φ : Dual R (M ⧸ W)), ↑(LinearMap.dualMap (mkQ W)) φ ∈ dualAnnihilator W))
                (dualCopairing W))
            x✝¹)
      x✝ =
    ↑↑(↑LinearMap.id x✝¹) x✝
[PROOFSTEP]
rfl
[GOAL]
R : Type u_1
M : Type u_2
M' : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup M'
inst✝ : Module R M'
W : Submodule R M
⊢ LinearMap.comp (dualCopairing W)
      (LinearMap.codRestrict (dualAnnihilator W) (LinearMap.dualMap (mkQ W))
        (_ : ∀ (φ : Dual R (M ⧸ W)), ↑(LinearMap.dualMap (mkQ W)) φ ∈ dualAnnihilator W)) =
    LinearMap.id
[PROOFSTEP]
ext
[GOAL]
case h.h.h
R : Type u_1
M : Type u_2
M' : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup M'
inst✝ : Module R M'
W : Submodule R M
x✝¹ : Dual R (M ⧸ W)
x✝ : M
⊢ ↑(LinearMap.comp
          (↑(LinearMap.comp (dualCopairing W)
                (LinearMap.codRestrict (dualAnnihilator W) (LinearMap.dualMap (mkQ W))
                  (_ : ∀ (φ : Dual R (M ⧸ W)), ↑(LinearMap.dualMap (mkQ W)) φ ∈ dualAnnihilator W)))
            x✝¹)
          (mkQ W))
      x✝ =
    ↑(LinearMap.comp (↑LinearMap.id x✝¹) (mkQ W)) x✝
[PROOFSTEP]
rfl
[GOAL]
R : Type u_1
M : Type u_2
M' : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup M'
inst✝ : Module R M'
f : M →ₗ[R] M'
hf : Function.Surjective ↑f
⊢ range (dualMap f) = dualAnnihilator (ker f)
[PROOFSTEP]
rw [← f.ker.range_dualMap_mkQ_eq]
[GOAL]
R : Type u_1
M : Type u_2
M' : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup M'
inst✝ : Module R M'
f : M →ₗ[R] M'
hf : Function.Surjective ↑f
⊢ range (dualMap f) = range (dualMap (mkQ (ker f)))
[PROOFSTEP]
let f' := LinearMap.quotKerEquivOfSurjective f hf
[GOAL]
R : Type u_1
M : Type u_2
M' : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup M'
inst✝ : Module R M'
f : M →ₗ[R] M'
hf : Function.Surjective ↑f
f' : (M ⧸ ker f) ≃ₗ[R] M' := quotKerEquivOfSurjective f hf
⊢ range (dualMap f) = range (dualMap (mkQ (ker f)))
[PROOFSTEP]
trans LinearMap.range (f.dualMap.comp f'.symm.dualMap.toLinearMap)
[GOAL]
R : Type u_1
M : Type u_2
M' : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup M'
inst✝ : Module R M'
f : M →ₗ[R] M'
hf : Function.Surjective ↑f
f' : (M ⧸ ker f) ≃ₗ[R] M' := quotKerEquivOfSurjective f hf
⊢ range (dualMap f) = range (comp (dualMap f) ↑(LinearEquiv.dualMap (LinearEquiv.symm f')))
[PROOFSTEP]
rw [LinearMap.range_comp_of_range_eq_top]
[GOAL]
case hf
R : Type u_1
M : Type u_2
M' : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup M'
inst✝ : Module R M'
f : M →ₗ[R] M'
hf : Function.Surjective ↑f
f' : (M ⧸ ker f) ≃ₗ[R] M' := quotKerEquivOfSurjective f hf
⊢ range ↑(LinearEquiv.dualMap (LinearEquiv.symm f')) = ⊤
[PROOFSTEP]
apply LinearEquiv.range
[GOAL]
R : Type u_1
M : Type u_2
M' : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup M'
inst✝ : Module R M'
f : M →ₗ[R] M'
hf : Function.Surjective ↑f
f' : (M ⧸ ker f) ≃ₗ[R] M' := quotKerEquivOfSurjective f hf
⊢ range (comp (dualMap f) ↑(LinearEquiv.dualMap (LinearEquiv.symm f'))) = range (dualMap (mkQ (ker f)))
[PROOFSTEP]
apply congr_arg
[GOAL]
case h
R : Type u_1
M : Type u_2
M' : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup M'
inst✝ : Module R M'
f : M →ₗ[R] M'
hf : Function.Surjective ↑f
f' : (M ⧸ ker f) ≃ₗ[R] M' := quotKerEquivOfSurjective f hf
⊢ comp (dualMap f) ↑(LinearEquiv.dualMap (LinearEquiv.symm f')) = dualMap (mkQ (ker f))
[PROOFSTEP]
ext φ x
[GOAL]
case h.h.h
R : Type u_1
M : Type u_2
M' : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup M'
inst✝ : Module R M'
f : M →ₗ[R] M'
hf : Function.Surjective ↑f
f' : (M ⧸ ker f) ≃ₗ[R] M' := quotKerEquivOfSurjective f hf
φ : Dual R (M ⧸ ker f)
x : M
⊢ ↑(↑(comp (dualMap f) ↑(LinearEquiv.dualMap (LinearEquiv.symm f'))) φ) x = ↑(↑(dualMap (mkQ (ker f))) φ) x
[PROOFSTEP]
simp only [LinearMap.coe_comp, LinearEquiv.coe_toLinearMap, LinearMap.dualMap_apply, LinearEquiv.dualMap_apply,
  mkQ_apply, LinearMap.quotKerEquivOfSurjective, LinearEquiv.trans_symm, LinearEquiv.trans_apply,
  LinearEquiv.ofTop_symm_apply, LinearMap.quotKerEquivRange_symm_apply_image, mkQ_apply, Function.comp]
[GOAL]
R : Type u_1
M : Type u_2
M' : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup M'
inst✝ : Module R M'
f : M →ₗ[R] M'
hf : Function.Surjective ↑(dualMap (Submodule.subtype (range f)))
⊢ range (dualMap f) = dualAnnihilator (ker f)
[PROOFSTEP]
have rr_surj : Function.Surjective f.rangeRestrict := by rw [← LinearMap.range_eq_top, LinearMap.range_rangeRestrict]
[GOAL]
R : Type u_1
M : Type u_2
M' : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup M'
inst✝ : Module R M'
f : M →ₗ[R] M'
hf : Function.Surjective ↑(dualMap (Submodule.subtype (range f)))
⊢ Function.Surjective ↑(rangeRestrict f)
[PROOFSTEP]
rw [← LinearMap.range_eq_top, LinearMap.range_rangeRestrict]
[GOAL]
R : Type u_1
M : Type u_2
M' : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup M'
inst✝ : Module R M'
f : M →ₗ[R] M'
hf : Function.Surjective ↑(dualMap (Submodule.subtype (range f)))
rr_surj : Function.Surjective ↑(rangeRestrict f)
⊢ range (dualMap f) = dualAnnihilator (ker f)
[PROOFSTEP]
have := range_dualMap_eq_dualAnnihilator_ker_of_surjective f.rangeRestrict rr_surj
[GOAL]
R : Type u_1
M : Type u_2
M' : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup M'
inst✝ : Module R M'
f : M →ₗ[R] M'
hf : Function.Surjective ↑(dualMap (Submodule.subtype (range f)))
rr_surj : Function.Surjective ↑(rangeRestrict f)
this : range (dualMap (rangeRestrict f)) = dualAnnihilator (ker (rangeRestrict f))
⊢ range (dualMap f) = dualAnnihilator (ker f)
[PROOFSTEP]
convert this using 1
  -- Porting note: broken dot notation lean4#1910
[GOAL]
case h.e'_2
R : Type u_1
M : Type u_2
M' : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup M'
inst✝ : Module R M'
f : M →ₗ[R] M'
hf : Function.Surjective ↑(dualMap (Submodule.subtype (range f)))
rr_surj : Function.Surjective ↑(rangeRestrict f)
this : range (dualMap (rangeRestrict f)) = dualAnnihilator (ker (rangeRestrict f))
⊢ range (dualMap f) = range (dualMap (rangeRestrict f))
[PROOFSTEP]
change LinearMap.range ((Submodule.subtype <| LinearMap.range f).comp f.rangeRestrict).dualMap = _
[GOAL]
case h.e'_2
R : Type u_1
M : Type u_2
M' : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup M'
inst✝ : Module R M'
f : M →ₗ[R] M'
hf : Function.Surjective ↑(dualMap (Submodule.subtype (range f)))
rr_surj : Function.Surjective ↑(rangeRestrict f)
this : range (dualMap (rangeRestrict f)) = dualAnnihilator (ker (rangeRestrict f))
⊢ range (dualMap (comp (Submodule.subtype (range f)) (rangeRestrict f))) = range (dualMap (rangeRestrict f))
[PROOFSTEP]
rw [← LinearMap.dualMap_comp_dualMap, LinearMap.range_comp_of_range_eq_top]
[GOAL]
case h.e'_2.hf
R : Type u_1
M : Type u_2
M' : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup M'
inst✝ : Module R M'
f : M →ₗ[R] M'
hf : Function.Surjective ↑(dualMap (Submodule.subtype (range f)))
rr_surj : Function.Surjective ↑(rangeRestrict f)
this : range (dualMap (rangeRestrict f)) = dualAnnihilator (ker (rangeRestrict f))
⊢ range (dualMap (Submodule.subtype (range f))) = ⊤
[PROOFSTEP]
rwa [LinearMap.range_eq_top]
[GOAL]
case h.e'_3
R : Type u_1
M : Type u_2
M' : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup M'
inst✝ : Module R M'
f : M →ₗ[R] M'
hf : Function.Surjective ↑(dualMap (Submodule.subtype (range f)))
rr_surj : Function.Surjective ↑(rangeRestrict f)
this : range (dualMap (rangeRestrict f)) = dualAnnihilator (ker (rangeRestrict f))
⊢ dualAnnihilator (ker f) = dualAnnihilator (ker (rangeRestrict f))
[PROOFSTEP]
apply congr_arg
[GOAL]
case h.e'_3.h
R : Type u_1
M : Type u_2
M' : Type u_3
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup M'
inst✝ : Module R M'
f : M →ₗ[R] M'
hf : Function.Surjective ↑(dualMap (Submodule.subtype (range f)))
rr_surj : Function.Surjective ↑(rangeRestrict f)
this : range (dualMap (rangeRestrict f)) = dualAnnihilator (ker (rangeRestrict f))
⊢ ker f = ker (rangeRestrict f)
[PROOFSTEP]
exact (LinearMap.ker_rangeRestrict f).symm
[GOAL]
K : Type u
inst✝⁴ : Field K
V₁ : Type v'
V₂ : Type v''
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : AddCommGroup V₂
inst✝ : Module K V₂
f : V₁ →ₗ[K] V₂
hf : Function.Injective ↑f
⊢ Function.Surjective ↑(dualMap f)
[PROOFSTEP]
intro φ
[GOAL]
K : Type u
inst✝⁴ : Field K
V₁ : Type v'
V₂ : Type v''
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : AddCommGroup V₂
inst✝ : Module K V₂
f : V₁ →ₗ[K] V₂
hf : Function.Injective ↑f
φ : Dual K V₁
⊢ ∃ a, ↑(dualMap f) a = φ
[PROOFSTEP]
let f' := LinearEquiv.ofInjective f hf
[GOAL]
K : Type u
inst✝⁴ : Field K
V₁ : Type v'
V₂ : Type v''
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : AddCommGroup V₂
inst✝ : Module K V₂
f : V₁ →ₗ[K] V₂
hf : Function.Injective ↑f
φ : Dual K V₁
f' : V₁ ≃ₗ[K] { x // x ∈ range f } := LinearEquiv.ofInjective f hf
⊢ ∃ a, ↑(dualMap f) a = φ
[PROOFSTEP]
use Subspace.dualLift (range f) (f'.symm.dualMap φ)
[GOAL]
case h
K : Type u
inst✝⁴ : Field K
V₁ : Type v'
V₂ : Type v''
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : AddCommGroup V₂
inst✝ : Module K V₂
f : V₁ →ₗ[K] V₂
hf : Function.Injective ↑f
φ : Dual K V₁
f' : V₁ ≃ₗ[K] { x // x ∈ range f } := LinearEquiv.ofInjective f hf
⊢ ↑(dualMap f) (↑(Subspace.dualLift (range f)) (↑(LinearEquiv.dualMap (LinearEquiv.symm f')) φ)) = φ
[PROOFSTEP]
ext x
[GOAL]
case h.h
K : Type u
inst✝⁴ : Field K
V₁ : Type v'
V₂ : Type v''
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : AddCommGroup V₂
inst✝ : Module K V₂
f : V₁ →ₗ[K] V₂
hf : Function.Injective ↑f
φ : Dual K V₁
f' : V₁ ≃ₗ[K] { x // x ∈ range f } := LinearEquiv.ofInjective f hf
x : V₁
⊢ ↑(↑(dualMap f) (↑(Subspace.dualLift (range f)) (↑(LinearEquiv.dualMap (LinearEquiv.symm f')) φ))) x = ↑φ x
[PROOFSTEP]
rw [LinearMap.dualMap_apply, Subspace.dualLift_of_mem (mem_range_self f x), LinearEquiv.dualMap_apply]
[GOAL]
case h.h
K : Type u
inst✝⁴ : Field K
V₁ : Type v'
V₂ : Type v''
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : AddCommGroup V₂
inst✝ : Module K V₂
f : V₁ →ₗ[K] V₂
hf : Function.Injective ↑f
φ : Dual K V₁
f' : V₁ ≃ₗ[K] { x // x ∈ range f } := LinearEquiv.ofInjective f hf
x : V₁
⊢ ↑φ (↑(LinearEquiv.symm f') { val := ↑f x, property := (_ : ↑f x ∈ range f) }) = ↑φ x
[PROOFSTEP]
congr 1
[GOAL]
case h.h.h.e_6.h
K : Type u
inst✝⁴ : Field K
V₁ : Type v'
V₂ : Type v''
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : AddCommGroup V₂
inst✝ : Module K V₂
f : V₁ →ₗ[K] V₂
hf : Function.Injective ↑f
φ : Dual K V₁
f' : V₁ ≃ₗ[K] { x // x ∈ range f } := LinearEquiv.ofInjective f hf
x : V₁
⊢ ↑(LinearEquiv.symm f') { val := ↑f x, property := (_ : ↑f x ∈ range f) } = x
[PROOFSTEP]
exact LinearEquiv.symm_apply_apply f' x
[GOAL]
K : Type u
inst✝⁴ : Field K
V₁ : Type v'
V₂ : Type v''
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : AddCommGroup V₂
inst✝ : Module K V₂
f : V₁ →ₗ[K] V₂
⊢ Function.Surjective ↑(dualMap f) ↔ Function.Injective ↑f
[PROOFSTEP]
rw [← LinearMap.range_eq_top, range_dualMap_eq_dualAnnihilator_ker, ← Submodule.dualAnnihilator_bot,
  Subspace.dualAnnihilator_inj, LinearMap.ker_eq_bot]
[GOAL]
K : Type u
inst✝⁴ : Field K
V₁ : Type v'
V₂ : Type v''
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : AddCommGroup V₂
inst✝ : Module K V₂
W : Subspace K V₁
⊢ Submodule.dualPairing W = ↑(quotAnnihilatorEquiv W)
[PROOFSTEP]
ext
[GOAL]
case h.h.h
K : Type u
inst✝⁴ : Field K
V₁ : Type v'
V₂ : Type v''
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : AddCommGroup V₂
inst✝ : Module K V₂
W : Subspace K V₁
x✝¹ : Dual K V₁
x✝ : { x // x ∈ W }
⊢ ↑(↑(LinearMap.comp (Submodule.dualPairing W) (mkQ (dualAnnihilator W))) x✝¹) x✝ =
    ↑(↑(LinearMap.comp (↑(quotAnnihilatorEquiv W)) (mkQ (dualAnnihilator W))) x✝¹) x✝
[PROOFSTEP]
rfl
[GOAL]
K : Type u
inst✝⁴ : Field K
V₁ : Type v'
V₂ : Type v''
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : AddCommGroup V₂
inst✝ : Module K V₂
W : Subspace K V₁
⊢ LinearMap.Nondegenerate (Submodule.dualPairing W)
[PROOFSTEP]
constructor
[GOAL]
case left
K : Type u
inst✝⁴ : Field K
V₁ : Type v'
V₂ : Type v''
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : AddCommGroup V₂
inst✝ : Module K V₂
W : Subspace K V₁
⊢ LinearMap.SeparatingLeft (Submodule.dualPairing W)
[PROOFSTEP]
rw [LinearMap.separatingLeft_iff_ker_eq_bot, dualPairing_eq]
[GOAL]
case left
K : Type u
inst✝⁴ : Field K
V₁ : Type v'
V₂ : Type v''
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : AddCommGroup V₂
inst✝ : Module K V₂
W : Subspace K V₁
⊢ LinearMap.ker ↑(quotAnnihilatorEquiv W) = ⊥
[PROOFSTEP]
apply LinearEquiv.ker
[GOAL]
case right
K : Type u
inst✝⁴ : Field K
V₁ : Type v'
V₂ : Type v''
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : AddCommGroup V₂
inst✝ : Module K V₂
W : Subspace K V₁
⊢ LinearMap.SeparatingRight (Submodule.dualPairing W)
[PROOFSTEP]
intro x h
[GOAL]
case right
K : Type u
inst✝⁴ : Field K
V₁ : Type v'
V₂ : Type v''
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : AddCommGroup V₂
inst✝ : Module K V₂
W : Subspace K V₁
x : { x // x ∈ W }
h : ∀ (x_1 : Dual K V₁ ⧸ dualAnnihilator W), ↑(↑(Submodule.dualPairing W) x_1) x = 0
⊢ x = 0
[PROOFSTEP]
rw [← forall_dual_apply_eq_zero_iff K x]
[GOAL]
case right
K : Type u
inst✝⁴ : Field K
V₁ : Type v'
V₂ : Type v''
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : AddCommGroup V₂
inst✝ : Module K V₂
W : Subspace K V₁
x : { x // x ∈ W }
h : ∀ (x_1 : Dual K V₁ ⧸ dualAnnihilator W), ↑(↑(Submodule.dualPairing W) x_1) x = 0
⊢ ∀ (φ : Dual K { x // x ∈ W }), ↑φ x = 0
[PROOFSTEP]
intro φ
[GOAL]
case right
K : Type u
inst✝⁴ : Field K
V₁ : Type v'
V₂ : Type v''
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : AddCommGroup V₂
inst✝ : Module K V₂
W : Subspace K V₁
x : { x // x ∈ W }
h : ∀ (x_1 : Dual K V₁ ⧸ dualAnnihilator W), ↑(↑(Submodule.dualPairing W) x_1) x = 0
φ : Dual K { x // x ∈ W }
⊢ ↑φ x = 0
[PROOFSTEP]
simpa only [Submodule.dualPairing_apply, dualLift_of_subtype] using h (Submodule.Quotient.mk (W.dualLift φ))
[GOAL]
K : Type u
inst✝⁴ : Field K
V₁ : Type v'
V₂ : Type v''
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : AddCommGroup V₂
inst✝ : Module K V₂
W : Subspace K V₁
⊢ LinearMap.Nondegenerate (dualCopairing W)
[PROOFSTEP]
constructor
[GOAL]
case left
K : Type u
inst✝⁴ : Field K
V₁ : Type v'
V₂ : Type v''
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : AddCommGroup V₂
inst✝ : Module K V₂
W : Subspace K V₁
⊢ LinearMap.SeparatingLeft (dualCopairing W)
[PROOFSTEP]
rw [LinearMap.separatingLeft_iff_ker_eq_bot, dualCopairing_eq]
[GOAL]
case left
K : Type u
inst✝⁴ : Field K
V₁ : Type v'
V₂ : Type v''
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : AddCommGroup V₂
inst✝ : Module K V₂
W : Subspace K V₁
⊢ LinearMap.ker ↑(LinearEquiv.symm (dualQuotEquivDualAnnihilator W)) = ⊥
[PROOFSTEP]
apply LinearEquiv.ker
[GOAL]
case right
K : Type u
inst✝⁴ : Field K
V₁ : Type v'
V₂ : Type v''
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : AddCommGroup V₂
inst✝ : Module K V₂
W : Subspace K V₁
⊢ LinearMap.SeparatingRight (dualCopairing W)
[PROOFSTEP]
rintro ⟨x⟩
[GOAL]
case right.mk
K : Type u
inst✝⁴ : Field K
V₁ : Type v'
V₂ : Type v''
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : AddCommGroup V₂
inst✝ : Module K V₂
W : Subspace K V₁
y✝ : V₁ ⧸ W
x : V₁
⊢ (∀ (x_1 : { x // x ∈ dualAnnihilator W }), ↑(↑(dualCopairing W) x_1) (Quot.mk Setoid.r x) = 0) →
    Quot.mk Setoid.r x = 0
[PROOFSTEP]
simp only [Quotient.quot_mk_eq_mk, dualCopairing_apply, Quotient.mk_eq_zero]
[GOAL]
case right.mk
K : Type u
inst✝⁴ : Field K
V₁ : Type v'
V₂ : Type v''
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : AddCommGroup V₂
inst✝ : Module K V₂
W : Subspace K V₁
y✝ : V₁ ⧸ W
x : V₁
⊢ (∀ (x_1 : { x // x ∈ dualAnnihilator W }), ↑x_1 x = 0) → x ∈ W
[PROOFSTEP]
rw [← forall_mem_dualAnnihilator_apply_eq_zero_iff, SetLike.forall]
[GOAL]
case right.mk
K : Type u
inst✝⁴ : Field K
V₁ : Type v'
V₂ : Type v''
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : AddCommGroup V₂
inst✝ : Module K V₂
W : Subspace K V₁
y✝ : V₁ ⧸ W
x : V₁
⊢ (∀ (x_1 : Dual K V₁) (h : x_1 ∈ dualAnnihilator W), ↑{ val := x_1, property := h } x = 0) →
    ∀ (φ : Dual K V₁), φ ∈ dualAnnihilator W → ↑φ x = 0
[PROOFSTEP]
exact id
[GOAL]
K : Type u
inst✝⁴ : Field K
V₁ : Type v'
V₂ : Type v''
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : AddCommGroup V₂
inst✝ : Module K V₂
W W' : Subspace K V₁
⊢ dualAnnihilator (W ⊓ W') = dualAnnihilator W ⊔ dualAnnihilator W'
[PROOFSTEP]
refine' le_antisymm _ (sup_dualAnnihilator_le_inf W W')
[GOAL]
K : Type u
inst✝⁴ : Field K
V₁ : Type v'
V₂ : Type v''
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : AddCommGroup V₂
inst✝ : Module K V₂
W W' : Subspace K V₁
⊢ dualAnnihilator (W ⊓ W') ≤ dualAnnihilator W ⊔ dualAnnihilator W'
[PROOFSTEP]
let F : V₁ →ₗ[K] (V₁ ⧸ W) × V₁ ⧸ W' :=
  (Submodule.mkQ W).prod
    (Submodule.mkQ W')
      -- Porting note: broken dot notation lean4#1910 LinearMap.ker
[GOAL]
K : Type u
inst✝⁴ : Field K
V₁ : Type v'
V₂ : Type v''
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : AddCommGroup V₂
inst✝ : Module K V₂
W W' : Subspace K V₁
F : V₁ →ₗ[K] (V₁ ⧸ W) × V₁ ⧸ W' := LinearMap.prod (mkQ W) (mkQ W')
⊢ dualAnnihilator (W ⊓ W') ≤ dualAnnihilator W ⊔ dualAnnihilator W'
[PROOFSTEP]
have : LinearMap.ker F = W ⊓ W' := by simp only [LinearMap.ker_prod, ker_mkQ]
[GOAL]
K : Type u
inst✝⁴ : Field K
V₁ : Type v'
V₂ : Type v''
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : AddCommGroup V₂
inst✝ : Module K V₂
W W' : Subspace K V₁
F : V₁ →ₗ[K] (V₁ ⧸ W) × V₁ ⧸ W' := LinearMap.prod (mkQ W) (mkQ W')
⊢ LinearMap.ker F = W ⊓ W'
[PROOFSTEP]
simp only [LinearMap.ker_prod, ker_mkQ]
[GOAL]
K : Type u
inst✝⁴ : Field K
V₁ : Type v'
V₂ : Type v''
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : AddCommGroup V₂
inst✝ : Module K V₂
W W' : Subspace K V₁
F : V₁ →ₗ[K] (V₁ ⧸ W) × V₁ ⧸ W' := LinearMap.prod (mkQ W) (mkQ W')
this : LinearMap.ker F = W ⊓ W'
⊢ dualAnnihilator (W ⊓ W') ≤ dualAnnihilator W ⊔ dualAnnihilator W'
[PROOFSTEP]
rw [← this, ← LinearMap.range_dualMap_eq_dualAnnihilator_ker]
[GOAL]
K : Type u
inst✝⁴ : Field K
V₁ : Type v'
V₂ : Type v''
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : AddCommGroup V₂
inst✝ : Module K V₂
W W' : Subspace K V₁
F : V₁ →ₗ[K] (V₁ ⧸ W) × V₁ ⧸ W' := LinearMap.prod (mkQ W) (mkQ W')
this : LinearMap.ker F = W ⊓ W'
⊢ LinearMap.range (LinearMap.dualMap F) ≤ dualAnnihilator W ⊔ dualAnnihilator W'
[PROOFSTEP]
intro φ
[GOAL]
K : Type u
inst✝⁴ : Field K
V₁ : Type v'
V₂ : Type v''
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : AddCommGroup V₂
inst✝ : Module K V₂
W W' : Subspace K V₁
F : V₁ →ₗ[K] (V₁ ⧸ W) × V₁ ⧸ W' := LinearMap.prod (mkQ W) (mkQ W')
this : LinearMap.ker F = W ⊓ W'
φ : Dual K V₁
⊢ φ ∈ LinearMap.range (LinearMap.dualMap F) → φ ∈ dualAnnihilator W ⊔ dualAnnihilator W'
[PROOFSTEP]
rw [LinearMap.mem_range]
[GOAL]
K : Type u
inst✝⁴ : Field K
V₁ : Type v'
V₂ : Type v''
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : AddCommGroup V₂
inst✝ : Module K V₂
W W' : Subspace K V₁
F : V₁ →ₗ[K] (V₁ ⧸ W) × V₁ ⧸ W' := LinearMap.prod (mkQ W) (mkQ W')
this : LinearMap.ker F = W ⊓ W'
φ : Dual K V₁
⊢ (∃ y, ↑(LinearMap.dualMap F) y = φ) → φ ∈ dualAnnihilator W ⊔ dualAnnihilator W'
[PROOFSTEP]
rintro ⟨x, rfl⟩
[GOAL]
case intro
K : Type u
inst✝⁴ : Field K
V₁ : Type v'
V₂ : Type v''
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : AddCommGroup V₂
inst✝ : Module K V₂
W W' : Subspace K V₁
F : V₁ →ₗ[K] (V₁ ⧸ W) × V₁ ⧸ W' := LinearMap.prod (mkQ W) (mkQ W')
this : LinearMap.ker F = W ⊓ W'
x : Dual K ((V₁ ⧸ W) × V₁ ⧸ W')
⊢ ↑(LinearMap.dualMap F) x ∈ dualAnnihilator W ⊔ dualAnnihilator W'
[PROOFSTEP]
rw [Submodule.mem_sup]
[GOAL]
case intro
K : Type u
inst✝⁴ : Field K
V₁ : Type v'
V₂ : Type v''
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : AddCommGroup V₂
inst✝ : Module K V₂
W W' : Subspace K V₁
F : V₁ →ₗ[K] (V₁ ⧸ W) × V₁ ⧸ W' := LinearMap.prod (mkQ W) (mkQ W')
this : LinearMap.ker F = W ⊓ W'
x : Dual K ((V₁ ⧸ W) × V₁ ⧸ W')
⊢ ∃ y, y ∈ dualAnnihilator W ∧ ∃ z, z ∈ dualAnnihilator W' ∧ y + z = ↑(LinearMap.dualMap F) x
[PROOFSTEP]
obtain ⟨⟨a, b⟩, rfl⟩ := (dualProdDualEquivDual K (V₁ ⧸ W) (V₁ ⧸ W')).surjective x
[GOAL]
case intro.intro.mk
K : Type u
inst✝⁴ : Field K
V₁ : Type v'
V₂ : Type v''
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : AddCommGroup V₂
inst✝ : Module K V₂
W W' : Subspace K V₁
F : V₁ →ₗ[K] (V₁ ⧸ W) × V₁ ⧸ W' := LinearMap.prod (mkQ W) (mkQ W')
this : LinearMap.ker F = W ⊓ W'
a : Dual K (V₁ ⧸ W)
b : Dual K (V₁ ⧸ W')
⊢ ∃ y,
    y ∈ dualAnnihilator W ∧
      ∃ z,
        z ∈ dualAnnihilator W' ∧ y + z = ↑(LinearMap.dualMap F) (↑(dualProdDualEquivDual K (V₁ ⧸ W) (V₁ ⧸ W')) (a, b))
[PROOFSTEP]
obtain ⟨a', rfl⟩ := (dualQuotEquivDualAnnihilator W).symm.surjective a
[GOAL]
case intro.intro.mk.intro
K : Type u
inst✝⁴ : Field K
V₁ : Type v'
V₂ : Type v''
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : AddCommGroup V₂
inst✝ : Module K V₂
W W' : Subspace K V₁
F : V₁ →ₗ[K] (V₁ ⧸ W) × V₁ ⧸ W' := LinearMap.prod (mkQ W) (mkQ W')
this : LinearMap.ker F = W ⊓ W'
b : Dual K (V₁ ⧸ W')
a' : { x // x ∈ dualAnnihilator W }
⊢ ∃ y,
    y ∈ dualAnnihilator W ∧
      ∃ z,
        z ∈ dualAnnihilator W' ∧
          y + z =
            ↑(LinearMap.dualMap F)
              (↑(dualProdDualEquivDual K (V₁ ⧸ W) (V₁ ⧸ W'))
                (↑(LinearEquiv.symm (dualQuotEquivDualAnnihilator W)) a', b))
[PROOFSTEP]
obtain ⟨b', rfl⟩ := (dualQuotEquivDualAnnihilator W').symm.surjective b
[GOAL]
case intro.intro.mk.intro.intro
K : Type u
inst✝⁴ : Field K
V₁ : Type v'
V₂ : Type v''
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : AddCommGroup V₂
inst✝ : Module K V₂
W W' : Subspace K V₁
F : V₁ →ₗ[K] (V₁ ⧸ W) × V₁ ⧸ W' := LinearMap.prod (mkQ W) (mkQ W')
this : LinearMap.ker F = W ⊓ W'
a' : { x // x ∈ dualAnnihilator W }
b' : { x // x ∈ dualAnnihilator W' }
⊢ ∃ y,
    y ∈ dualAnnihilator W ∧
      ∃ z,
        z ∈ dualAnnihilator W' ∧
          y + z =
            ↑(LinearMap.dualMap F)
              (↑(dualProdDualEquivDual K (V₁ ⧸ W) (V₁ ⧸ W'))
                (↑(LinearEquiv.symm (dualQuotEquivDualAnnihilator W)) a',
                  ↑(LinearEquiv.symm (dualQuotEquivDualAnnihilator W')) b'))
[PROOFSTEP]
use a', a'.property, b', b'.property
[GOAL]
case right
K : Type u
inst✝⁴ : Field K
V₁ : Type v'
V₂ : Type v''
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : AddCommGroup V₂
inst✝ : Module K V₂
W W' : Subspace K V₁
F : V₁ →ₗ[K] (V₁ ⧸ W) × V₁ ⧸ W' := LinearMap.prod (mkQ W) (mkQ W')
this : LinearMap.ker F = W ⊓ W'
a' : { x // x ∈ dualAnnihilator W }
b' : { x // x ∈ dualAnnihilator W' }
⊢ ↑a' + ↑b' =
    ↑(LinearMap.dualMap F)
      (↑(dualProdDualEquivDual K (V₁ ⧸ W) (V₁ ⧸ W'))
        (↑(LinearEquiv.symm (dualQuotEquivDualAnnihilator W)) a',
          ↑(LinearEquiv.symm (dualQuotEquivDualAnnihilator W')) b'))
[PROOFSTEP]
rfl
[GOAL]
K : Type u
inst✝⁵ : Field K
V₁ : Type v'
V₂ : Type v''
inst✝⁴ : AddCommGroup V₁
inst✝³ : Module K V₁
inst✝² : AddCommGroup V₂
inst✝¹ : Module K V₂
ι : Type u_1
inst✝ : _root_.Finite ι
W : ι → Subspace K V₁
⊢ dualAnnihilator (⨅ (i : ι), W i) = ⨆ (i : ι), dualAnnihilator (W i)
[PROOFSTEP]
revert ι
[GOAL]
K : Type u
inst✝⁴ : Field K
V₁ : Type v'
V₂ : Type v''
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : AddCommGroup V₂
inst✝ : Module K V₂
⊢ ∀ {ι : Type u_1} [inst : _root_.Finite ι] (W : ι → Subspace K V₁),
    dualAnnihilator (⨅ (i : ι), W i) = ⨆ (i : ι), dualAnnihilator (W i)
[PROOFSTEP]
refine' @Finite.induction_empty_option _ _ _ _
[GOAL]
case refine'_1
K : Type u
inst✝⁴ : Field K
V₁ : Type v'
V₂ : Type v''
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : AddCommGroup V₂
inst✝ : Module K V₂
⊢ ∀ {α β : Type u_1},
    α ≃ β →
      (∀ (W : α → Subspace K V₁), dualAnnihilator (⨅ (i : α), W i) = ⨆ (i : α), dualAnnihilator (W i)) →
        ∀ (W : β → Subspace K V₁), dualAnnihilator (⨅ (i : β), W i) = ⨆ (i : β), dualAnnihilator (W i)
[PROOFSTEP]
intro α β h hyp W
[GOAL]
case refine'_1
K : Type u
inst✝⁴ : Field K
V₁ : Type v'
V₂ : Type v''
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : AddCommGroup V₂
inst✝ : Module K V₂
α β : Type u_1
h : α ≃ β
hyp : ∀ (W : α → Subspace K V₁), dualAnnihilator (⨅ (i : α), W i) = ⨆ (i : α), dualAnnihilator (W i)
W : β → Subspace K V₁
⊢ dualAnnihilator (⨅ (i : β), W i) = ⨆ (i : β), dualAnnihilator (W i)
[PROOFSTEP]
rw [← h.iInf_comp, hyp _, ← h.iSup_comp]
[GOAL]
case refine'_2
K : Type u
inst✝⁴ : Field K
V₁ : Type v'
V₂ : Type v''
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : AddCommGroup V₂
inst✝ : Module K V₂
⊢ ∀ (W : PEmpty → Subspace K V₁), dualAnnihilator (⨅ (i : PEmpty), W i) = ⨆ (i : PEmpty), dualAnnihilator (W i)
[PROOFSTEP]
intro W
[GOAL]
case refine'_2
K : Type u
inst✝⁴ : Field K
V₁ : Type v'
V₂ : Type v''
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : AddCommGroup V₂
inst✝ : Module K V₂
W : PEmpty → Subspace K V₁
⊢ dualAnnihilator (⨅ (i : PEmpty), W i) = ⨆ (i : PEmpty), dualAnnihilator (W i)
[PROOFSTEP]
rw [iSup_of_empty', iInf_of_empty', sInf_empty, sSup_empty, dualAnnihilator_top]
[GOAL]
case refine'_3
K : Type u
inst✝⁴ : Field K
V₁ : Type v'
V₂ : Type v''
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : AddCommGroup V₂
inst✝ : Module K V₂
⊢ ∀ {α : Type u_1} [inst : Fintype α],
    (∀ (W : α → Subspace K V₁), dualAnnihilator (⨅ (i : α), W i) = ⨆ (i : α), dualAnnihilator (W i)) →
      ∀ (W : Option α → Subspace K V₁),
        dualAnnihilator (⨅ (i : Option α), W i) = ⨆ (i : Option α), dualAnnihilator (W i)
[PROOFSTEP]
intro α _ h W
[GOAL]
case refine'_3
K : Type u
inst✝⁵ : Field K
V₁ : Type v'
V₂ : Type v''
inst✝⁴ : AddCommGroup V₁
inst✝³ : Module K V₁
inst✝² : AddCommGroup V₂
inst✝¹ : Module K V₂
α : Type u_1
inst✝ : Fintype α
h : ∀ (W : α → Subspace K V₁), dualAnnihilator (⨅ (i : α), W i) = ⨆ (i : α), dualAnnihilator (W i)
W : Option α → Subspace K V₁
⊢ dualAnnihilator (⨅ (i : Option α), W i) = ⨆ (i : Option α), dualAnnihilator (W i)
[PROOFSTEP]
rw [iInf_option, iSup_option, dualAnnihilator_inf_eq, h]
[GOAL]
K : Type u
inst✝⁴ : Field K
V₁ : Type v'
V₂ : Type v''
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : AddCommGroup V₂
inst✝ : Module K V₂
W W' : Subspace K V₁
h : IsCompl W W'
⊢ IsCompl (dualAnnihilator W) (dualAnnihilator W')
[PROOFSTEP]
rw [isCompl_iff, disjoint_iff, codisjoint_iff] at h ⊢
[GOAL]
K : Type u
inst✝⁴ : Field K
V₁ : Type v'
V₂ : Type v''
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : AddCommGroup V₂
inst✝ : Module K V₂
W W' : Subspace K V₁
h : W ⊓ W' = ⊥ ∧ W ⊔ W' = ⊤
⊢ dualAnnihilator W ⊓ dualAnnihilator W' = ⊥ ∧ dualAnnihilator W ⊔ dualAnnihilator W' = ⊤
[PROOFSTEP]
rw [← dualAnnihilator_inf_eq, ← dualAnnihilator_sup_eq, h.1, h.2, dualAnnihilator_top, dualAnnihilator_bot]
[GOAL]
K : Type u
inst✝⁴ : Field K
V₁ : Type v'
V₂ : Type v''
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : AddCommGroup V₂
inst✝ : Module K V₂
W W' : Subspace K V₁
h : W ⊓ W' = ⊥ ∧ W ⊔ W' = ⊤
⊢ ⊥ = ⊥ ∧ ⊤ = ⊤
[PROOFSTEP]
exact ⟨rfl, rfl⟩
[GOAL]
K : Type u
inst✝⁵ : Field K
V₁ : Type v'
V₂ : Type v''
inst✝⁴ : AddCommGroup V₁
inst✝³ : Module K V₁
inst✝² : AddCommGroup V₂
inst✝¹ : Module K V₂
inst✝ : FiniteDimensional K V₂
f : V₁ →ₗ[K] V₂
⊢ finrank K { x // x ∈ range (dualMap f) } = finrank K { x // x ∈ range f }
[PROOFSTEP]
have that :=
  Submodule.finrank_quotient_add_finrank
    (LinearMap.range f)
      -- Porting note: Again LinearEquiv.finrank_eq needs help
[GOAL]
K : Type u
inst✝⁵ : Field K
V₁ : Type v'
V₂ : Type v''
inst✝⁴ : AddCommGroup V₁
inst✝³ : Module K V₁
inst✝² : AddCommGroup V₂
inst✝¹ : Module K V₂
inst✝ : FiniteDimensional K V₂
f : V₁ →ₗ[K] V₂
that : finrank K (V₂ ⧸ range f) + finrank K { x // x ∈ range f } = finrank K V₂
⊢ finrank K { x // x ∈ range (dualMap f) } = finrank K { x // x ∈ range f }
[PROOFSTEP]
let equiv := (Subspace.quotEquivAnnihilator <| LinearMap.range f)
[GOAL]
K : Type u
inst✝⁵ : Field K
V₁ : Type v'
V₂ : Type v''
inst✝⁴ : AddCommGroup V₁
inst✝³ : Module K V₁
inst✝² : AddCommGroup V₂
inst✝¹ : Module K V₂
inst✝ : FiniteDimensional K V₂
f : V₁ →ₗ[K] V₂
that : finrank K (V₂ ⧸ range f) + finrank K { x // x ∈ range f } = finrank K V₂
equiv : (V₂ ⧸ range f) ≃ₗ[K] { x // x ∈ Submodule.dualAnnihilator (range f) } := Subspace.quotEquivAnnihilator (range f)
⊢ finrank K { x // x ∈ range (dualMap f) } = finrank K { x // x ∈ range f }
[PROOFSTEP]
have eq :=
  LinearEquiv.finrank_eq (R := K) (M := (V₂ ⧸ range f)) (M₂ := { x // x ∈ Submodule.dualAnnihilator (range f) }) equiv
[GOAL]
K : Type u
inst✝⁵ : Field K
V₁ : Type v'
V₂ : Type v''
inst✝⁴ : AddCommGroup V₁
inst✝³ : Module K V₁
inst✝² : AddCommGroup V₂
inst✝¹ : Module K V₂
inst✝ : FiniteDimensional K V₂
f : V₁ →ₗ[K] V₂
that : finrank K (V₂ ⧸ range f) + finrank K { x // x ∈ range f } = finrank K V₂
equiv : (V₂ ⧸ range f) ≃ₗ[K] { x // x ∈ Submodule.dualAnnihilator (range f) } := Subspace.quotEquivAnnihilator (range f)
eq : finrank K (V₂ ⧸ range f) = finrank K { x // x ∈ Submodule.dualAnnihilator (range f) }
⊢ finrank K { x // x ∈ range (dualMap f) } = finrank K { x // x ∈ range f }
[PROOFSTEP]
rw [eq, ← ker_dualMap_eq_dualAnnihilator_range] at that 
[GOAL]
K : Type u
inst✝⁵ : Field K
V₁ : Type v'
V₂ : Type v''
inst✝⁴ : AddCommGroup V₁
inst✝³ : Module K V₁
inst✝² : AddCommGroup V₂
inst✝¹ : Module K V₂
inst✝ : FiniteDimensional K V₂
f : V₁ →ₗ[K] V₂
that : finrank K { x // x ∈ ker (dualMap f) } + finrank K { x // x ∈ range f } = finrank K V₂
equiv : (V₂ ⧸ range f) ≃ₗ[K] { x // x ∈ Submodule.dualAnnihilator (range f) } := Subspace.quotEquivAnnihilator (range f)
eq : finrank K (V₂ ⧸ range f) = finrank K { x // x ∈ Submodule.dualAnnihilator (range f) }
⊢ finrank K { x // x ∈ range (dualMap f) } = finrank K { x // x ∈ range f }
[PROOFSTEP]
conv_rhs at that => rw [← Subspace.dual_finrank_eq]
[GOAL]
K : Type u
inst✝⁵ : Field K
V₁ : Type v'
V₂ : Type v''
inst✝⁴ : AddCommGroup V₁
inst✝³ : Module K V₁
inst✝² : AddCommGroup V₂
inst✝¹ : Module K V₂
inst✝ : FiniteDimensional K V₂
f : V₁ →ₗ[K] V₂
that : finrank K { x // x ∈ ker (dualMap f) } + finrank K { x // x ∈ range f } = finrank K V₂
equiv : (V₂ ⧸ range f) ≃ₗ[K] { x // x ∈ Submodule.dualAnnihilator (range f) } := Subspace.quotEquivAnnihilator (range f)
eq : finrank K (V₂ ⧸ range f) = finrank K { x // x ∈ Submodule.dualAnnihilator (range f) }
| finrank K V₂
[PROOFSTEP]
rw [← Subspace.dual_finrank_eq]
[GOAL]
K : Type u
inst✝⁵ : Field K
V₁ : Type v'
V₂ : Type v''
inst✝⁴ : AddCommGroup V₁
inst✝³ : Module K V₁
inst✝² : AddCommGroup V₂
inst✝¹ : Module K V₂
inst✝ : FiniteDimensional K V₂
f : V₁ →ₗ[K] V₂
that : finrank K { x // x ∈ ker (dualMap f) } + finrank K { x // x ∈ range f } = finrank K V₂
equiv : (V₂ ⧸ range f) ≃ₗ[K] { x // x ∈ Submodule.dualAnnihilator (range f) } := Subspace.quotEquivAnnihilator (range f)
eq : finrank K (V₂ ⧸ range f) = finrank K { x // x ∈ Submodule.dualAnnihilator (range f) }
| finrank K V₂
[PROOFSTEP]
rw [← Subspace.dual_finrank_eq]
[GOAL]
K : Type u
inst✝⁵ : Field K
V₁ : Type v'
V₂ : Type v''
inst✝⁴ : AddCommGroup V₁
inst✝³ : Module K V₁
inst✝² : AddCommGroup V₂
inst✝¹ : Module K V₂
inst✝ : FiniteDimensional K V₂
f : V₁ →ₗ[K] V₂
that : finrank K { x // x ∈ ker (dualMap f) } + finrank K { x // x ∈ range f } = finrank K V₂
equiv : (V₂ ⧸ range f) ≃ₗ[K] { x // x ∈ Submodule.dualAnnihilator (range f) } := Subspace.quotEquivAnnihilator (range f)
eq : finrank K (V₂ ⧸ range f) = finrank K { x // x ∈ Submodule.dualAnnihilator (range f) }
| finrank K V₂
[PROOFSTEP]
rw [← Subspace.dual_finrank_eq]
[GOAL]
K : Type u
inst✝⁵ : Field K
V₁ : Type v'
V₂ : Type v''
inst✝⁴ : AddCommGroup V₁
inst✝³ : Module K V₁
inst✝² : AddCommGroup V₂
inst✝¹ : Module K V₂
inst✝ : FiniteDimensional K V₂
f : V₁ →ₗ[K] V₂
that : finrank K { x // x ∈ ker (dualMap f) } + finrank K { x // x ∈ range f } = finrank K (Dual K V₂)
equiv : (V₂ ⧸ range f) ≃ₗ[K] { x // x ∈ Submodule.dualAnnihilator (range f) } := Subspace.quotEquivAnnihilator (range f)
eq : finrank K (V₂ ⧸ range f) = finrank K { x // x ∈ Submodule.dualAnnihilator (range f) }
⊢ finrank K { x // x ∈ range (dualMap f) } = finrank K { x // x ∈ range f }
[PROOFSTEP]
refine' add_left_injective (finrank K <| LinearMap.ker f.dualMap) _
[GOAL]
K : Type u
inst✝⁵ : Field K
V₁ : Type v'
V₂ : Type v''
inst✝⁴ : AddCommGroup V₁
inst✝³ : Module K V₁
inst✝² : AddCommGroup V₂
inst✝¹ : Module K V₂
inst✝ : FiniteDimensional K V₂
f : V₁ →ₗ[K] V₂
that : finrank K { x // x ∈ ker (dualMap f) } + finrank K { x // x ∈ range f } = finrank K (Dual K V₂)
equiv : (V₂ ⧸ range f) ≃ₗ[K] { x // x ∈ Submodule.dualAnnihilator (range f) } := Subspace.quotEquivAnnihilator (range f)
eq : finrank K (V₂ ⧸ range f) = finrank K { x // x ∈ Submodule.dualAnnihilator (range f) }
⊢ (fun x => x + finrank K { x // x ∈ ker (dualMap f) }) (finrank K { x // x ∈ range (dualMap f) }) =
    (fun x => x + finrank K { x // x ∈ ker (dualMap f) }) (finrank K { x // x ∈ range f })
[PROOFSTEP]
change _ + _ = _ + _
[GOAL]
K : Type u
inst✝⁵ : Field K
V₁ : Type v'
V₂ : Type v''
inst✝⁴ : AddCommGroup V₁
inst✝³ : Module K V₁
inst✝² : AddCommGroup V₂
inst✝¹ : Module K V₂
inst✝ : FiniteDimensional K V₂
f : V₁ →ₗ[K] V₂
that : finrank K { x // x ∈ ker (dualMap f) } + finrank K { x // x ∈ range f } = finrank K (Dual K V₂)
equiv : (V₂ ⧸ range f) ≃ₗ[K] { x // x ∈ Submodule.dualAnnihilator (range f) } := Subspace.quotEquivAnnihilator (range f)
eq : finrank K (V₂ ⧸ range f) = finrank K { x // x ∈ Submodule.dualAnnihilator (range f) }
⊢ finrank K { x // x ∈ range (dualMap f) } + finrank K { x // x ∈ ker (dualMap f) } =
    finrank K { x // x ∈ range f } + finrank K { x // x ∈ ker (dualMap f) }
[PROOFSTEP]
rw [finrank_range_add_finrank_ker f.dualMap, add_comm, that]
[GOAL]
K : Type u
inst✝⁵ : Field K
V₁ : Type v'
V₂ : Type v''
inst✝⁴ : AddCommGroup V₁
inst✝³ : Module K V₁
inst✝² : AddCommGroup V₂
inst✝¹ : Module K V₂
inst✝ : FiniteDimensional K V₂
f : V₁ →ₗ[K] V₂
⊢ Function.Injective ↑(dualMap f) ↔ Function.Surjective ↑f
[PROOFSTEP]
refine' ⟨_, fun h => dualMap_injective_of_surjective h⟩
[GOAL]
K : Type u
inst✝⁵ : Field K
V₁ : Type v'
V₂ : Type v''
inst✝⁴ : AddCommGroup V₁
inst✝³ : Module K V₁
inst✝² : AddCommGroup V₂
inst✝¹ : Module K V₂
inst✝ : FiniteDimensional K V₂
f : V₁ →ₗ[K] V₂
⊢ Function.Injective ↑(dualMap f) → Function.Surjective ↑f
[PROOFSTEP]
rw [← range_eq_top, ← ker_eq_bot]
[GOAL]
K : Type u
inst✝⁵ : Field K
V₁ : Type v'
V₂ : Type v''
inst✝⁴ : AddCommGroup V₁
inst✝³ : Module K V₁
inst✝² : AddCommGroup V₂
inst✝¹ : Module K V₂
inst✝ : FiniteDimensional K V₂
f : V₁ →ₗ[K] V₂
⊢ ker (dualMap f) = ⊥ → range f = ⊤
[PROOFSTEP]
intro h
[GOAL]
K : Type u
inst✝⁵ : Field K
V₁ : Type v'
V₂ : Type v''
inst✝⁴ : AddCommGroup V₁
inst✝³ : Module K V₁
inst✝² : AddCommGroup V₂
inst✝¹ : Module K V₂
inst✝ : FiniteDimensional K V₂
f : V₁ →ₗ[K] V₂
h : ker (dualMap f) = ⊥
⊢ range f = ⊤
[PROOFSTEP]
apply Submodule.eq_top_of_finrank_eq
[GOAL]
case h
K : Type u
inst✝⁵ : Field K
V₁ : Type v'
V₂ : Type v''
inst✝⁴ : AddCommGroup V₁
inst✝³ : Module K V₁
inst✝² : AddCommGroup V₂
inst✝¹ : Module K V₂
inst✝ : FiniteDimensional K V₂
f : V₁ →ₗ[K] V₂
h : ker (dualMap f) = ⊥
⊢ finrank K { x // x ∈ range f } = finrank K V₂
[PROOFSTEP]
rw [← finrank_eq_zero] at h 
[GOAL]
case h
K : Type u
inst✝⁵ : Field K
V₁ : Type v'
V₂ : Type v''
inst✝⁴ : AddCommGroup V₁
inst✝³ : Module K V₁
inst✝² : AddCommGroup V₂
inst✝¹ : Module K V₂
inst✝ : FiniteDimensional K V₂
f : V₁ →ₗ[K] V₂
h : finrank K { x // x ∈ ker (dualMap f) } = 0
⊢ finrank K { x // x ∈ range f } = finrank K V₂
[PROOFSTEP]
rw [← add_zero (FiniteDimensional.finrank K <| LinearMap.range f), ← h, ←
  LinearMap.finrank_range_dualMap_eq_finrank_range, LinearMap.finrank_range_add_finrank_ker, Subspace.dual_finrank_eq]
[GOAL]
K : Type u
inst✝⁵ : Field K
V₁ : Type v'
V₂ : Type v''
inst✝⁴ : AddCommGroup V₁
inst✝³ : Module K V₁
inst✝² : AddCommGroup V₂
inst✝¹ : Module K V₂
inst✝ : FiniteDimensional K V₂
f : V₁ →ₗ[K] V₂
⊢ Function.Bijective ↑(dualMap f) ↔ Function.Bijective ↑f
[PROOFSTEP]
simp_rw [Function.Bijective, dualMap_surjective_iff, dualMap_injective_iff, and_comm]
[GOAL]
R : Type u_1
A : Type u_2
M : Type u_3
N : Type u_4
ι : Type u_5
κ : Type u_6
inst✝⁸ : DecidableEq ι
inst✝⁷ : DecidableEq κ
inst✝⁶ : Fintype ι
inst✝⁵ : Fintype κ
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
b : Basis ι R M
c : Basis κ R N
f : Dual R (M ⊗[R] N)
⊢ ↑(dualDistribInvOfBasis b c) f =
    ∑ i : ι, ∑ j : κ, ↑f (↑b i ⊗ₜ[R] ↑c j) • ↑(Basis.dualBasis b) i ⊗ₜ[R] ↑(Basis.dualBasis c) j
[PROOFSTEP]
simp [dualDistribInvOfBasis]
[GOAL]
R : Type u_1
A : Type u_2
M : Type u_3
N : Type u_4
ι : Type u_5
κ : Type u_6
inst✝⁸ : DecidableEq ι
inst✝⁷ : DecidableEq κ
inst✝⁶ : Fintype ι
inst✝⁵ : Fintype κ
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
b : Basis ι R M
c : Basis κ R N
⊢ comp (dualDistrib R M N) (dualDistribInvOfBasis b c) = LinearMap.id
[PROOFSTEP]
apply (b.tensorProduct c).dualBasis.ext
[GOAL]
R : Type u_1
A : Type u_2
M : Type u_3
N : Type u_4
ι : Type u_5
κ : Type u_6
inst✝⁸ : DecidableEq ι
inst✝⁷ : DecidableEq κ
inst✝⁶ : Fintype ι
inst✝⁵ : Fintype κ
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
b : Basis ι R M
c : Basis κ R N
⊢ ∀ (i : ι × κ),
    ↑(comp (dualDistrib R M N) (dualDistribInvOfBasis b c)) (↑(Basis.dualBasis (Basis.tensorProduct b c)) i) =
      ↑LinearMap.id (↑(Basis.dualBasis (Basis.tensorProduct b c)) i)
[PROOFSTEP]
rintro ⟨i, j⟩
[GOAL]
case mk
R : Type u_1
A : Type u_2
M : Type u_3
N : Type u_4
ι : Type u_5
κ : Type u_6
inst✝⁸ : DecidableEq ι
inst✝⁷ : DecidableEq κ
inst✝⁶ : Fintype ι
inst✝⁵ : Fintype κ
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
b : Basis ι R M
c : Basis κ R N
i : ι
j : κ
⊢ ↑(comp (dualDistrib R M N) (dualDistribInvOfBasis b c)) (↑(Basis.dualBasis (Basis.tensorProduct b c)) (i, j)) =
    ↑LinearMap.id (↑(Basis.dualBasis (Basis.tensorProduct b c)) (i, j))
[PROOFSTEP]
apply (b.tensorProduct c).ext
[GOAL]
case mk
R : Type u_1
A : Type u_2
M : Type u_3
N : Type u_4
ι : Type u_5
κ : Type u_6
inst✝⁸ : DecidableEq ι
inst✝⁷ : DecidableEq κ
inst✝⁶ : Fintype ι
inst✝⁵ : Fintype κ
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
b : Basis ι R M
c : Basis κ R N
i : ι
j : κ
⊢ ∀ (i_1 : ι × κ),
    ↑(↑(comp (dualDistrib R M N) (dualDistribInvOfBasis b c)) (↑(Basis.dualBasis (Basis.tensorProduct b c)) (i, j)))
        (↑(Basis.tensorProduct b c) i_1) =
      ↑(↑LinearMap.id (↑(Basis.dualBasis (Basis.tensorProduct b c)) (i, j))) (↑(Basis.tensorProduct b c) i_1)
[PROOFSTEP]
rintro ⟨i', j'⟩
[GOAL]
case mk.mk
R : Type u_1
A : Type u_2
M : Type u_3
N : Type u_4
ι : Type u_5
κ : Type u_6
inst✝⁸ : DecidableEq ι
inst✝⁷ : DecidableEq κ
inst✝⁶ : Fintype ι
inst✝⁵ : Fintype κ
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
b : Basis ι R M
c : Basis κ R N
i : ι
j : κ
i' : ι
j' : κ
⊢ ↑(↑(comp (dualDistrib R M N) (dualDistribInvOfBasis b c)) (↑(Basis.dualBasis (Basis.tensorProduct b c)) (i, j)))
      (↑(Basis.tensorProduct b c) (i', j')) =
    ↑(↑LinearMap.id (↑(Basis.dualBasis (Basis.tensorProduct b c)) (i, j))) (↑(Basis.tensorProduct b c) (i', j'))
[PROOFSTEP]
simp only [dualDistrib, Basis.coe_dualBasis, coe_comp, Function.comp_apply, dualDistribInvOfBasis_apply,
  Basis.coord_apply, Basis.tensorProduct_repr_tmul_apply, Basis.repr_self, ne_eq, LinearMap.map_sum, map_smul,
  homTensorHomMap_apply, compRight_apply, Basis.tensorProduct_apply, coeFn_sum, Finset.sum_apply, smul_apply,
  LinearEquiv.coe_coe, map_tmul, lid_tmul, smul_eq_mul, id_coe, id_eq]
[GOAL]
case mk.mk
R : Type u_1
A : Type u_2
M : Type u_3
N : Type u_4
ι : Type u_5
κ : Type u_6
inst✝⁸ : DecidableEq ι
inst✝⁷ : DecidableEq κ
inst✝⁶ : Fintype ι
inst✝⁵ : Fintype κ
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
b : Basis ι R M
c : Basis κ R N
i : ι
j : κ
i' : ι
j' : κ
⊢ ∑ x : ι,
      ∑ x_1 : κ,
        ↑(Finsupp.single x 1) i * ↑(Finsupp.single x_1 1) j * (↑(Finsupp.single i' 1) x * ↑(Finsupp.single j' 1) x_1) =
    ↑(Finsupp.single i' 1) i * ↑(Finsupp.single j' 1) j
[PROOFSTEP]
rw [Finset.sum_eq_single i, Finset.sum_eq_single j]
[GOAL]
case mk.mk
R : Type u_1
A : Type u_2
M : Type u_3
N : Type u_4
ι : Type u_5
κ : Type u_6
inst✝⁸ : DecidableEq ι
inst✝⁷ : DecidableEq κ
inst✝⁶ : Fintype ι
inst✝⁵ : Fintype κ
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
b : Basis ι R M
c : Basis κ R N
i : ι
j : κ
i' : ι
j' : κ
⊢ ↑(Finsupp.single i 1) i * ↑(Finsupp.single j 1) j * (↑(Finsupp.single i' 1) i * ↑(Finsupp.single j' 1) j) =
    ↑(Finsupp.single i' 1) i * ↑(Finsupp.single j' 1) j
case mk.mk.h₀
R : Type u_1
A : Type u_2
M : Type u_3
N : Type u_4
ι : Type u_5
κ : Type u_6
inst✝⁸ : DecidableEq ι
inst✝⁷ : DecidableEq κ
inst✝⁶ : Fintype ι
inst✝⁵ : Fintype κ
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
b : Basis ι R M
c : Basis κ R N
i : ι
j : κ
i' : ι
j' : κ
⊢ ∀ (b : κ),
    b ∈ Finset.univ →
      b ≠ j →
        ↑(Finsupp.single i 1) i * ↑(Finsupp.single b 1) j * (↑(Finsupp.single i' 1) i * ↑(Finsupp.single j' 1) b) = 0
case mk.mk.h₁
R : Type u_1
A : Type u_2
M : Type u_3
N : Type u_4
ι : Type u_5
κ : Type u_6
inst✝⁸ : DecidableEq ι
inst✝⁷ : DecidableEq κ
inst✝⁶ : Fintype ι
inst✝⁵ : Fintype κ
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
b : Basis ι R M
c : Basis κ R N
i : ι
j : κ
i' : ι
j' : κ
⊢ ¬j ∈ Finset.univ →
    ↑(Finsupp.single i 1) i * ↑(Finsupp.single j 1) j * (↑(Finsupp.single i' 1) i * ↑(Finsupp.single j' 1) j) = 0
case mk.mk.h₀
R : Type u_1
A : Type u_2
M : Type u_3
N : Type u_4
ι : Type u_5
κ : Type u_6
inst✝⁸ : DecidableEq ι
inst✝⁷ : DecidableEq κ
inst✝⁶ : Fintype ι
inst✝⁵ : Fintype κ
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
b : Basis ι R M
c : Basis κ R N
i : ι
j : κ
i' : ι
j' : κ
⊢ ∀ (b : ι),
    b ∈ Finset.univ →
      b ≠ i →
        ∑ x : κ,
            ↑(Finsupp.single b 1) i * ↑(Finsupp.single x 1) j * (↑(Finsupp.single i' 1) b * ↑(Finsupp.single j' 1) x) =
          0
case mk.mk.h₁
R : Type u_1
A : Type u_2
M : Type u_3
N : Type u_4
ι : Type u_5
κ : Type u_6
inst✝⁸ : DecidableEq ι
inst✝⁷ : DecidableEq κ
inst✝⁶ : Fintype ι
inst✝⁵ : Fintype κ
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
b : Basis ι R M
c : Basis κ R N
i : ι
j : κ
i' : ι
j' : κ
⊢ ¬i ∈ Finset.univ →
    ∑ x : κ, ↑(Finsupp.single i 1) i * ↑(Finsupp.single x 1) j * (↑(Finsupp.single i' 1) i * ↑(Finsupp.single j' 1) x) =
      0
[PROOFSTEP]
simp
[GOAL]
case mk.mk.h₀
R : Type u_1
A : Type u_2
M : Type u_3
N : Type u_4
ι : Type u_5
κ : Type u_6
inst✝⁸ : DecidableEq ι
inst✝⁷ : DecidableEq κ
inst✝⁶ : Fintype ι
inst✝⁵ : Fintype κ
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
b : Basis ι R M
c : Basis κ R N
i : ι
j : κ
i' : ι
j' : κ
⊢ ∀ (b : κ),
    b ∈ Finset.univ →
      b ≠ j →
        ↑(Finsupp.single i 1) i * ↑(Finsupp.single b 1) j * (↑(Finsupp.single i' 1) i * ↑(Finsupp.single j' 1) b) = 0
case mk.mk.h₁
R : Type u_1
A : Type u_2
M : Type u_3
N : Type u_4
ι : Type u_5
κ : Type u_6
inst✝⁸ : DecidableEq ι
inst✝⁷ : DecidableEq κ
inst✝⁶ : Fintype ι
inst✝⁵ : Fintype κ
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
b : Basis ι R M
c : Basis κ R N
i : ι
j : κ
i' : ι
j' : κ
⊢ ¬j ∈ Finset.univ →
    ↑(Finsupp.single i 1) i * ↑(Finsupp.single j 1) j * (↑(Finsupp.single i' 1) i * ↑(Finsupp.single j' 1) j) = 0
case mk.mk.h₀
R : Type u_1
A : Type u_2
M : Type u_3
N : Type u_4
ι : Type u_5
κ : Type u_6
inst✝⁸ : DecidableEq ι
inst✝⁷ : DecidableEq κ
inst✝⁶ : Fintype ι
inst✝⁵ : Fintype κ
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
b : Basis ι R M
c : Basis κ R N
i : ι
j : κ
i' : ι
j' : κ
⊢ ∀ (b : ι),
    b ∈ Finset.univ →
      b ≠ i →
        ∑ x : κ,
            ↑(Finsupp.single b 1) i * ↑(Finsupp.single x 1) j * (↑(Finsupp.single i' 1) b * ↑(Finsupp.single j' 1) x) =
          0
case mk.mk.h₁
R : Type u_1
A : Type u_2
M : Type u_3
N : Type u_4
ι : Type u_5
κ : Type u_6
inst✝⁸ : DecidableEq ι
inst✝⁷ : DecidableEq κ
inst✝⁶ : Fintype ι
inst✝⁵ : Fintype κ
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
b : Basis ι R M
c : Basis κ R N
i : ι
j : κ
i' : ι
j' : κ
⊢ ¬i ∈ Finset.univ →
    ∑ x : κ, ↑(Finsupp.single i 1) i * ↑(Finsupp.single x 1) j * (↑(Finsupp.single i' 1) i * ↑(Finsupp.single j' 1) x) =
      0
[PROOFSTEP]
all_goals {intros; simp [*] at *
}
-- Porting note: introduced to help with timeout in dualDistribEquivOfBasis
[GOAL]
case mk.mk.h₀
R : Type u_1
A : Type u_2
M : Type u_3
N : Type u_4
ι : Type u_5
κ : Type u_6
inst✝⁸ : DecidableEq ι
inst✝⁷ : DecidableEq κ
inst✝⁶ : Fintype ι
inst✝⁵ : Fintype κ
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
b : Basis ι R M
c : Basis κ R N
i : ι
j : κ
i' : ι
j' : κ
⊢ ∀ (b : κ),
    b ∈ Finset.univ →
      b ≠ j →
        ↑(Finsupp.single i 1) i * ↑(Finsupp.single b 1) j * (↑(Finsupp.single i' 1) i * ↑(Finsupp.single j' 1) b) = 0
[PROOFSTEP]
{intros; simp [*] at *
}
-- Porting note: introduced to help with timeout in dualDistribEquivOfBasis
[GOAL]
case mk.mk.h₀
R : Type u_1
A : Type u_2
M : Type u_3
N : Type u_4
ι : Type u_5
κ : Type u_6
inst✝⁸ : DecidableEq ι
inst✝⁷ : DecidableEq κ
inst✝⁶ : Fintype ι
inst✝⁵ : Fintype κ
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
b : Basis ι R M
c : Basis κ R N
i : ι
j : κ
i' : ι
j' : κ
⊢ ∀ (b : κ),
    b ∈ Finset.univ →
      b ≠ j →
        ↑(Finsupp.single i 1) i * ↑(Finsupp.single b 1) j * (↑(Finsupp.single i' 1) i * ↑(Finsupp.single j' 1) b) = 0
[PROOFSTEP]
intros
[GOAL]
case mk.mk.h₀
R : Type u_1
A : Type u_2
M : Type u_3
N : Type u_4
ι : Type u_5
κ : Type u_6
inst✝⁸ : DecidableEq ι
inst✝⁷ : DecidableEq κ
inst✝⁶ : Fintype ι
inst✝⁵ : Fintype κ
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
b : Basis ι R M
c : Basis κ R N
i : ι
j : κ
i' : ι
j' b✝ : κ
a✝¹ : b✝ ∈ Finset.univ
a✝ : b✝ ≠ j
⊢ ↑(Finsupp.single i 1) i * ↑(Finsupp.single b✝ 1) j * (↑(Finsupp.single i' 1) i * ↑(Finsupp.single j' 1) b✝) = 0
[PROOFSTEP]
simp [*] at *
[GOAL]
case mk.mk.h₁
R : Type u_1
A : Type u_2
M : Type u_3
N : Type u_4
ι : Type u_5
κ : Type u_6
inst✝⁸ : DecidableEq ι
inst✝⁷ : DecidableEq κ
inst✝⁶ : Fintype ι
inst✝⁵ : Fintype κ
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
b : Basis ι R M
c : Basis κ R N
i : ι
j : κ
i' : ι
j' : κ
⊢ ¬j ∈ Finset.univ →
    ↑(Finsupp.single i 1) i * ↑(Finsupp.single j 1) j * (↑(Finsupp.single i' 1) i * ↑(Finsupp.single j' 1) j) = 0
[PROOFSTEP]
{intros; simp [*] at *
}
-- Porting note: introduced to help with timeout in dualDistribEquivOfBasis
[GOAL]
case mk.mk.h₁
R : Type u_1
A : Type u_2
M : Type u_3
N : Type u_4
ι : Type u_5
κ : Type u_6
inst✝⁸ : DecidableEq ι
inst✝⁷ : DecidableEq κ
inst✝⁶ : Fintype ι
inst✝⁵ : Fintype κ
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
b : Basis ι R M
c : Basis κ R N
i : ι
j : κ
i' : ι
j' : κ
⊢ ¬j ∈ Finset.univ →
    ↑(Finsupp.single i 1) i * ↑(Finsupp.single j 1) j * (↑(Finsupp.single i' 1) i * ↑(Finsupp.single j' 1) j) = 0
[PROOFSTEP]
intros
[GOAL]
case mk.mk.h₁
R : Type u_1
A : Type u_2
M : Type u_3
N : Type u_4
ι : Type u_5
κ : Type u_6
inst✝⁸ : DecidableEq ι
inst✝⁷ : DecidableEq κ
inst✝⁶ : Fintype ι
inst✝⁵ : Fintype κ
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
b : Basis ι R M
c : Basis κ R N
i : ι
j : κ
i' : ι
j' : κ
a✝ : ¬j ∈ Finset.univ
⊢ ↑(Finsupp.single i 1) i * ↑(Finsupp.single j 1) j * (↑(Finsupp.single i' 1) i * ↑(Finsupp.single j' 1) j) = 0
[PROOFSTEP]
simp [*] at *
[GOAL]
case mk.mk.h₀
R : Type u_1
A : Type u_2
M : Type u_3
N : Type u_4
ι : Type u_5
κ : Type u_6
inst✝⁸ : DecidableEq ι
inst✝⁷ : DecidableEq κ
inst✝⁶ : Fintype ι
inst✝⁵ : Fintype κ
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
b : Basis ι R M
c : Basis κ R N
i : ι
j : κ
i' : ι
j' : κ
⊢ ∀ (b : ι),
    b ∈ Finset.univ →
      b ≠ i →
        ∑ x : κ,
            ↑(Finsupp.single b 1) i * ↑(Finsupp.single x 1) j * (↑(Finsupp.single i' 1) b * ↑(Finsupp.single j' 1) x) =
          0
[PROOFSTEP]
{intros; simp [*] at *
}
-- Porting note: introduced to help with timeout in dualDistribEquivOfBasis
[GOAL]
case mk.mk.h₀
R : Type u_1
A : Type u_2
M : Type u_3
N : Type u_4
ι : Type u_5
κ : Type u_6
inst✝⁸ : DecidableEq ι
inst✝⁷ : DecidableEq κ
inst✝⁶ : Fintype ι
inst✝⁵ : Fintype κ
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
b : Basis ι R M
c : Basis κ R N
i : ι
j : κ
i' : ι
j' : κ
⊢ ∀ (b : ι),
    b ∈ Finset.univ →
      b ≠ i →
        ∑ x : κ,
            ↑(Finsupp.single b 1) i * ↑(Finsupp.single x 1) j * (↑(Finsupp.single i' 1) b * ↑(Finsupp.single j' 1) x) =
          0
[PROOFSTEP]
intros
[GOAL]
case mk.mk.h₀
R : Type u_1
A : Type u_2
M : Type u_3
N : Type u_4
ι : Type u_5
κ : Type u_6
inst✝⁸ : DecidableEq ι
inst✝⁷ : DecidableEq κ
inst✝⁶ : Fintype ι
inst✝⁵ : Fintype κ
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
b : Basis ι R M
c : Basis κ R N
i : ι
j : κ
i' : ι
j' : κ
b✝ : ι
a✝¹ : b✝ ∈ Finset.univ
a✝ : b✝ ≠ i
⊢ ∑ x : κ, ↑(Finsupp.single b✝ 1) i * ↑(Finsupp.single x 1) j * (↑(Finsupp.single i' 1) b✝ * ↑(Finsupp.single j' 1) x) =
    0
[PROOFSTEP]
simp [*] at *
[GOAL]
case mk.mk.h₁
R : Type u_1
A : Type u_2
M : Type u_3
N : Type u_4
ι : Type u_5
κ : Type u_6
inst✝⁸ : DecidableEq ι
inst✝⁷ : DecidableEq κ
inst✝⁶ : Fintype ι
inst✝⁵ : Fintype κ
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
b : Basis ι R M
c : Basis κ R N
i : ι
j : κ
i' : ι
j' : κ
⊢ ¬i ∈ Finset.univ →
    ∑ x : κ, ↑(Finsupp.single i 1) i * ↑(Finsupp.single x 1) j * (↑(Finsupp.single i' 1) i * ↑(Finsupp.single j' 1) x) =
      0
[PROOFSTEP]
{intros; simp [*] at *
}
-- Porting note: introduced to help with timeout in dualDistribEquivOfBasis
[GOAL]
case mk.mk.h₁
R : Type u_1
A : Type u_2
M : Type u_3
N : Type u_4
ι : Type u_5
κ : Type u_6
inst✝⁸ : DecidableEq ι
inst✝⁷ : DecidableEq κ
inst✝⁶ : Fintype ι
inst✝⁵ : Fintype κ
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
b : Basis ι R M
c : Basis κ R N
i : ι
j : κ
i' : ι
j' : κ
⊢ ¬i ∈ Finset.univ →
    ∑ x : κ, ↑(Finsupp.single i 1) i * ↑(Finsupp.single x 1) j * (↑(Finsupp.single i' 1) i * ↑(Finsupp.single j' 1) x) =
      0
[PROOFSTEP]
intros
[GOAL]
case mk.mk.h₁
R : Type u_1
A : Type u_2
M : Type u_3
N : Type u_4
ι : Type u_5
κ : Type u_6
inst✝⁸ : DecidableEq ι
inst✝⁷ : DecidableEq κ
inst✝⁶ : Fintype ι
inst✝⁵ : Fintype κ
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
b : Basis ι R M
c : Basis κ R N
i : ι
j : κ
i' : ι
j' : κ
a✝ : ¬i ∈ Finset.univ
⊢ ∑ x : κ, ↑(Finsupp.single i 1) i * ↑(Finsupp.single x 1) j * (↑(Finsupp.single i' 1) i * ↑(Finsupp.single j' 1) x) = 0
[PROOFSTEP]
simp [*] at *
[GOAL]
R : Type u_1
A : Type u_2
M : Type u_3
N : Type u_4
ι : Type u_5
κ : Type u_6
inst✝⁸ : DecidableEq ι
inst✝⁷ : DecidableEq κ
inst✝⁶ : Fintype ι
inst✝⁵ : Fintype κ
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
b : Basis ι R M
c : Basis κ R N
⊢ comp (dualDistribInvOfBasis b c) (dualDistrib R M N) = LinearMap.id
[PROOFSTEP]
apply (b.dualBasis.tensorProduct c.dualBasis).ext
[GOAL]
R : Type u_1
A : Type u_2
M : Type u_3
N : Type u_4
ι : Type u_5
κ : Type u_6
inst✝⁸ : DecidableEq ι
inst✝⁷ : DecidableEq κ
inst✝⁶ : Fintype ι
inst✝⁵ : Fintype κ
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
b : Basis ι R M
c : Basis κ R N
⊢ ∀ (i : ι × κ),
    ↑(comp (dualDistribInvOfBasis b c) (dualDistrib R M N))
        (↑(Basis.tensorProduct (Basis.dualBasis b) (Basis.dualBasis c)) i) =
      ↑LinearMap.id (↑(Basis.tensorProduct (Basis.dualBasis b) (Basis.dualBasis c)) i)
[PROOFSTEP]
rintro ⟨i, j⟩
[GOAL]
case mk
R : Type u_1
A : Type u_2
M : Type u_3
N : Type u_4
ι : Type u_5
κ : Type u_6
inst✝⁸ : DecidableEq ι
inst✝⁷ : DecidableEq κ
inst✝⁶ : Fintype ι
inst✝⁵ : Fintype κ
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
b : Basis ι R M
c : Basis κ R N
i : ι
j : κ
⊢ ↑(comp (dualDistribInvOfBasis b c) (dualDistrib R M N))
      (↑(Basis.tensorProduct (Basis.dualBasis b) (Basis.dualBasis c)) (i, j)) =
    ↑LinearMap.id (↑(Basis.tensorProduct (Basis.dualBasis b) (Basis.dualBasis c)) (i, j))
[PROOFSTEP]
simp only [Basis.tensorProduct_apply, Basis.coe_dualBasis, coe_comp, Function.comp_apply, dualDistribInvOfBasis_apply,
  dualDistrib_apply, Basis.coord_apply, Basis.repr_self, ne_eq, id_coe, id_eq]
[GOAL]
case mk
R : Type u_1
A : Type u_2
M : Type u_3
N : Type u_4
ι : Type u_5
κ : Type u_6
inst✝⁸ : DecidableEq ι
inst✝⁷ : DecidableEq κ
inst✝⁶ : Fintype ι
inst✝⁵ : Fintype κ
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
b : Basis ι R M
c : Basis κ R N
i : ι
j : κ
⊢ ∑ x : ι, ∑ x_1 : κ, (↑(Finsupp.single x 1) i * ↑(Finsupp.single x_1 1) j) • Basis.coord b x ⊗ₜ[R] Basis.coord c x_1 =
    Basis.coord b i ⊗ₜ[R] Basis.coord c j
[PROOFSTEP]
rw [Finset.sum_eq_single i, Finset.sum_eq_single j]
[GOAL]
case mk
R : Type u_1
A : Type u_2
M : Type u_3
N : Type u_4
ι : Type u_5
κ : Type u_6
inst✝⁸ : DecidableEq ι
inst✝⁷ : DecidableEq κ
inst✝⁶ : Fintype ι
inst✝⁵ : Fintype κ
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
b : Basis ι R M
c : Basis κ R N
i : ι
j : κ
⊢ (↑(Finsupp.single i 1) i * ↑(Finsupp.single j 1) j) • Basis.coord b i ⊗ₜ[R] Basis.coord c j =
    Basis.coord b i ⊗ₜ[R] Basis.coord c j
case mk.h₀
R : Type u_1
A : Type u_2
M : Type u_3
N : Type u_4
ι : Type u_5
κ : Type u_6
inst✝⁸ : DecidableEq ι
inst✝⁷ : DecidableEq κ
inst✝⁶ : Fintype ι
inst✝⁵ : Fintype κ
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
b : Basis ι R M
c : Basis κ R N
i : ι
j : κ
⊢ ∀ (b_1 : κ),
    b_1 ∈ Finset.univ →
      b_1 ≠ j → (↑(Finsupp.single i 1) i * ↑(Finsupp.single b_1 1) j) • Basis.coord b i ⊗ₜ[R] Basis.coord c b_1 = 0
case mk.h₁
R : Type u_1
A : Type u_2
M : Type u_3
N : Type u_4
ι : Type u_5
κ : Type u_6
inst✝⁸ : DecidableEq ι
inst✝⁷ : DecidableEq κ
inst✝⁶ : Fintype ι
inst✝⁵ : Fintype κ
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
b : Basis ι R M
c : Basis κ R N
i : ι
j : κ
⊢ ¬j ∈ Finset.univ → (↑(Finsupp.single i 1) i * ↑(Finsupp.single j 1) j) • Basis.coord b i ⊗ₜ[R] Basis.coord c j = 0
case mk.h₀
R : Type u_1
A : Type u_2
M : Type u_3
N : Type u_4
ι : Type u_5
κ : Type u_6
inst✝⁸ : DecidableEq ι
inst✝⁷ : DecidableEq κ
inst✝⁶ : Fintype ι
inst✝⁵ : Fintype κ
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
b : Basis ι R M
c : Basis κ R N
i : ι
j : κ
⊢ ∀ (b_1 : ι),
    b_1 ∈ Finset.univ →
      b_1 ≠ i →
        ∑ x : κ, (↑(Finsupp.single b_1 1) i * ↑(Finsupp.single x 1) j) • Basis.coord b b_1 ⊗ₜ[R] Basis.coord c x = 0
case mk.h₁
R : Type u_1
A : Type u_2
M : Type u_3
N : Type u_4
ι : Type u_5
κ : Type u_6
inst✝⁸ : DecidableEq ι
inst✝⁷ : DecidableEq κ
inst✝⁶ : Fintype ι
inst✝⁵ : Fintype κ
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
b : Basis ι R M
c : Basis κ R N
i : ι
j : κ
⊢ ¬i ∈ Finset.univ →
    ∑ x : κ, (↑(Finsupp.single i 1) i * ↑(Finsupp.single x 1) j) • Basis.coord b i ⊗ₜ[R] Basis.coord c x = 0
[PROOFSTEP]
simp
[GOAL]
case mk.h₀
R : Type u_1
A : Type u_2
M : Type u_3
N : Type u_4
ι : Type u_5
κ : Type u_6
inst✝⁸ : DecidableEq ι
inst✝⁷ : DecidableEq κ
inst✝⁶ : Fintype ι
inst✝⁵ : Fintype κ
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
b : Basis ι R M
c : Basis κ R N
i : ι
j : κ
⊢ ∀ (b_1 : κ),
    b_1 ∈ Finset.univ →
      b_1 ≠ j → (↑(Finsupp.single i 1) i * ↑(Finsupp.single b_1 1) j) • Basis.coord b i ⊗ₜ[R] Basis.coord c b_1 = 0
case mk.h₁
R : Type u_1
A : Type u_2
M : Type u_3
N : Type u_4
ι : Type u_5
κ : Type u_6
inst✝⁸ : DecidableEq ι
inst✝⁷ : DecidableEq κ
inst✝⁶ : Fintype ι
inst✝⁵ : Fintype κ
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
b : Basis ι R M
c : Basis κ R N
i : ι
j : κ
⊢ ¬j ∈ Finset.univ → (↑(Finsupp.single i 1) i * ↑(Finsupp.single j 1) j) • Basis.coord b i ⊗ₜ[R] Basis.coord c j = 0
case mk.h₀
R : Type u_1
A : Type u_2
M : Type u_3
N : Type u_4
ι : Type u_5
κ : Type u_6
inst✝⁸ : DecidableEq ι
inst✝⁷ : DecidableEq κ
inst✝⁶ : Fintype ι
inst✝⁵ : Fintype κ
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
b : Basis ι R M
c : Basis κ R N
i : ι
j : κ
⊢ ∀ (b_1 : ι),
    b_1 ∈ Finset.univ →
      b_1 ≠ i →
        ∑ x : κ, (↑(Finsupp.single b_1 1) i * ↑(Finsupp.single x 1) j) • Basis.coord b b_1 ⊗ₜ[R] Basis.coord c x = 0
case mk.h₁
R : Type u_1
A : Type u_2
M : Type u_3
N : Type u_4
ι : Type u_5
κ : Type u_6
inst✝⁸ : DecidableEq ι
inst✝⁷ : DecidableEq κ
inst✝⁶ : Fintype ι
inst✝⁵ : Fintype κ
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
b : Basis ι R M
c : Basis κ R N
i : ι
j : κ
⊢ ¬i ∈ Finset.univ →
    ∑ x : κ, (↑(Finsupp.single i 1) i * ↑(Finsupp.single x 1) j) • Basis.coord b i ⊗ₜ[R] Basis.coord c x = 0
[PROOFSTEP]
all_goals {intros; simp [*] at *
}
[GOAL]
case mk.h₀
R : Type u_1
A : Type u_2
M : Type u_3
N : Type u_4
ι : Type u_5
κ : Type u_6
inst✝⁸ : DecidableEq ι
inst✝⁷ : DecidableEq κ
inst✝⁶ : Fintype ι
inst✝⁵ : Fintype κ
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
b : Basis ι R M
c : Basis κ R N
i : ι
j : κ
⊢ ∀ (b_1 : κ),
    b_1 ∈ Finset.univ →
      b_1 ≠ j → (↑(Finsupp.single i 1) i * ↑(Finsupp.single b_1 1) j) • Basis.coord b i ⊗ₜ[R] Basis.coord c b_1 = 0
[PROOFSTEP]
{intros; simp [*] at *
}
[GOAL]
case mk.h₀
R : Type u_1
A : Type u_2
M : Type u_3
N : Type u_4
ι : Type u_5
κ : Type u_6
inst✝⁸ : DecidableEq ι
inst✝⁷ : DecidableEq κ
inst✝⁶ : Fintype ι
inst✝⁵ : Fintype κ
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
b : Basis ι R M
c : Basis κ R N
i : ι
j : κ
⊢ ∀ (b_1 : κ),
    b_1 ∈ Finset.univ →
      b_1 ≠ j → (↑(Finsupp.single i 1) i * ↑(Finsupp.single b_1 1) j) • Basis.coord b i ⊗ₜ[R] Basis.coord c b_1 = 0
[PROOFSTEP]
intros
[GOAL]
case mk.h₀
R : Type u_1
A : Type u_2
M : Type u_3
N : Type u_4
ι : Type u_5
κ : Type u_6
inst✝⁸ : DecidableEq ι
inst✝⁷ : DecidableEq κ
inst✝⁶ : Fintype ι
inst✝⁵ : Fintype κ
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
b : Basis ι R M
c : Basis κ R N
i : ι
j b✝ : κ
a✝¹ : b✝ ∈ Finset.univ
a✝ : b✝ ≠ j
⊢ (↑(Finsupp.single i 1) i * ↑(Finsupp.single b✝ 1) j) • Basis.coord b i ⊗ₜ[R] Basis.coord c b✝ = 0
[PROOFSTEP]
simp [*] at *
[GOAL]
case mk.h₁
R : Type u_1
A : Type u_2
M : Type u_3
N : Type u_4
ι : Type u_5
κ : Type u_6
inst✝⁸ : DecidableEq ι
inst✝⁷ : DecidableEq κ
inst✝⁶ : Fintype ι
inst✝⁵ : Fintype κ
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
b : Basis ι R M
c : Basis κ R N
i : ι
j : κ
⊢ ¬j ∈ Finset.univ → (↑(Finsupp.single i 1) i * ↑(Finsupp.single j 1) j) • Basis.coord b i ⊗ₜ[R] Basis.coord c j = 0
[PROOFSTEP]
{intros; simp [*] at *
}
[GOAL]
case mk.h₁
R : Type u_1
A : Type u_2
M : Type u_3
N : Type u_4
ι : Type u_5
κ : Type u_6
inst✝⁸ : DecidableEq ι
inst✝⁷ : DecidableEq κ
inst✝⁶ : Fintype ι
inst✝⁵ : Fintype κ
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
b : Basis ι R M
c : Basis κ R N
i : ι
j : κ
⊢ ¬j ∈ Finset.univ → (↑(Finsupp.single i 1) i * ↑(Finsupp.single j 1) j) • Basis.coord b i ⊗ₜ[R] Basis.coord c j = 0
[PROOFSTEP]
intros
[GOAL]
case mk.h₁
R : Type u_1
A : Type u_2
M : Type u_3
N : Type u_4
ι : Type u_5
κ : Type u_6
inst✝⁸ : DecidableEq ι
inst✝⁷ : DecidableEq κ
inst✝⁶ : Fintype ι
inst✝⁵ : Fintype κ
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
b : Basis ι R M
c : Basis κ R N
i : ι
j : κ
a✝ : ¬j ∈ Finset.univ
⊢ (↑(Finsupp.single i 1) i * ↑(Finsupp.single j 1) j) • Basis.coord b i ⊗ₜ[R] Basis.coord c j = 0
[PROOFSTEP]
simp [*] at *
[GOAL]
case mk.h₀
R : Type u_1
A : Type u_2
M : Type u_3
N : Type u_4
ι : Type u_5
κ : Type u_6
inst✝⁸ : DecidableEq ι
inst✝⁷ : DecidableEq κ
inst✝⁶ : Fintype ι
inst✝⁵ : Fintype κ
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
b : Basis ι R M
c : Basis κ R N
i : ι
j : κ
⊢ ∀ (b_1 : ι),
    b_1 ∈ Finset.univ →
      b_1 ≠ i →
        ∑ x : κ, (↑(Finsupp.single b_1 1) i * ↑(Finsupp.single x 1) j) • Basis.coord b b_1 ⊗ₜ[R] Basis.coord c x = 0
[PROOFSTEP]
{intros; simp [*] at *
}
[GOAL]
case mk.h₀
R : Type u_1
A : Type u_2
M : Type u_3
N : Type u_4
ι : Type u_5
κ : Type u_6
inst✝⁸ : DecidableEq ι
inst✝⁷ : DecidableEq κ
inst✝⁶ : Fintype ι
inst✝⁵ : Fintype κ
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
b : Basis ι R M
c : Basis κ R N
i : ι
j : κ
⊢ ∀ (b_1 : ι),
    b_1 ∈ Finset.univ →
      b_1 ≠ i →
        ∑ x : κ, (↑(Finsupp.single b_1 1) i * ↑(Finsupp.single x 1) j) • Basis.coord b b_1 ⊗ₜ[R] Basis.coord c x = 0
[PROOFSTEP]
intros
[GOAL]
case mk.h₀
R : Type u_1
A : Type u_2
M : Type u_3
N : Type u_4
ι : Type u_5
κ : Type u_6
inst✝⁸ : DecidableEq ι
inst✝⁷ : DecidableEq κ
inst✝⁶ : Fintype ι
inst✝⁵ : Fintype κ
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
b : Basis ι R M
c : Basis κ R N
i : ι
j : κ
b✝ : ι
a✝¹ : b✝ ∈ Finset.univ
a✝ : b✝ ≠ i
⊢ ∑ x : κ, (↑(Finsupp.single b✝ 1) i * ↑(Finsupp.single x 1) j) • Basis.coord b b✝ ⊗ₜ[R] Basis.coord c x = 0
[PROOFSTEP]
simp [*] at *
[GOAL]
case mk.h₁
R : Type u_1
A : Type u_2
M : Type u_3
N : Type u_4
ι : Type u_5
κ : Type u_6
inst✝⁸ : DecidableEq ι
inst✝⁷ : DecidableEq κ
inst✝⁶ : Fintype ι
inst✝⁵ : Fintype κ
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
b : Basis ι R M
c : Basis κ R N
i : ι
j : κ
⊢ ¬i ∈ Finset.univ →
    ∑ x : κ, (↑(Finsupp.single i 1) i * ↑(Finsupp.single x 1) j) • Basis.coord b i ⊗ₜ[R] Basis.coord c x = 0
[PROOFSTEP]
{intros; simp [*] at *
}
[GOAL]
case mk.h₁
R : Type u_1
A : Type u_2
M : Type u_3
N : Type u_4
ι : Type u_5
κ : Type u_6
inst✝⁸ : DecidableEq ι
inst✝⁷ : DecidableEq κ
inst✝⁶ : Fintype ι
inst✝⁵ : Fintype κ
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
b : Basis ι R M
c : Basis κ R N
i : ι
j : κ
⊢ ¬i ∈ Finset.univ →
    ∑ x : κ, (↑(Finsupp.single i 1) i * ↑(Finsupp.single x 1) j) • Basis.coord b i ⊗ₜ[R] Basis.coord c x = 0
[PROOFSTEP]
intros
[GOAL]
case mk.h₁
R : Type u_1
A : Type u_2
M : Type u_3
N : Type u_4
ι : Type u_5
κ : Type u_6
inst✝⁸ : DecidableEq ι
inst✝⁷ : DecidableEq κ
inst✝⁶ : Fintype ι
inst✝⁵ : Fintype κ
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
b : Basis ι R M
c : Basis κ R N
i : ι
j : κ
a✝ : ¬i ∈ Finset.univ
⊢ ∑ x : κ, (↑(Finsupp.single i 1) i * ↑(Finsupp.single x 1) j) • Basis.coord b i ⊗ₜ[R] Basis.coord c x = 0
[PROOFSTEP]
simp [*] at *
[GOAL]
R : Type u_1
A : Type u_2
M : Type u_3
N : Type u_4
ι : Type u_5
κ : Type u_6
inst✝⁸ : DecidableEq ι
inst✝⁷ : DecidableEq κ
inst✝⁶ : Fintype ι
inst✝⁵ : Fintype κ
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
b : Basis ι R M
c : Basis κ R N
⊢ Dual R M ⊗[R] Dual R N ≃ₗ[R] Dual R (M ⊗[R] N)
[PROOFSTEP]
refine' LinearEquiv.ofLinear (dualDistrib R M N) (dualDistribInvOfBasis b c) _ _
[GOAL]
case refine'_1
R : Type u_1
A : Type u_2
M : Type u_3
N : Type u_4
ι : Type u_5
κ : Type u_6
inst✝⁸ : DecidableEq ι
inst✝⁷ : DecidableEq κ
inst✝⁶ : Fintype ι
inst✝⁵ : Fintype κ
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
b : Basis ι R M
c : Basis κ R N
⊢ comp (dualDistrib R M N) (dualDistribInvOfBasis b c) = LinearMap.id
[PROOFSTEP]
exact dualDistrib_dualDistribInvOfBasis_left_inverse _ _
[GOAL]
case refine'_2
R : Type u_1
A : Type u_2
M : Type u_3
N : Type u_4
ι : Type u_5
κ : Type u_6
inst✝⁸ : DecidableEq ι
inst✝⁷ : DecidableEq κ
inst✝⁶ : Fintype ι
inst✝⁵ : Fintype κ
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
b : Basis ι R M
c : Basis κ R N
⊢ comp (dualDistribInvOfBasis b c) (dualDistrib R M N) = LinearMap.id
[PROOFSTEP]
exact dualDistrib_dualDistribInvOfBasis_right_inverse _ _
