[GOAL]
R : Type u
inst✝⁵ : Semiring R
ι : Type v
dec_ι : DecidableEq ι
M : ι → Type w
inst✝⁴ : (i : ι) → AddCommMonoid (M i)
inst✝³ : (i : ι) → Module R (M i)
N : Type u₁
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
φ : (i : ι) → M i →ₗ[R] N
ψ ψ' : (⨁ (i : ι), M i) →ₗ[R] N
inst✝ : Fintype ι
src✝ : (Π₀ (i : ι), M i) ≃ ((i : ι) → M i) := DFinsupp.equivFunOnFintype
f g : ⨁ (i : ι), M i
⊢ ↑(f + g) = ↑f + ↑g
[PROOFSTEP]
ext
[GOAL]
case h
R : Type u
inst✝⁵ : Semiring R
ι : Type v
dec_ι : DecidableEq ι
M : ι → Type w
inst✝⁴ : (i : ι) → AddCommMonoid (M i)
inst✝³ : (i : ι) → Module R (M i)
N : Type u₁
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
φ : (i : ι) → M i →ₗ[R] N
ψ ψ' : (⨁ (i : ι), M i) →ₗ[R] N
inst✝ : Fintype ι
src✝ : (Π₀ (i : ι), M i) ≃ ((i : ι) → M i) := DFinsupp.equivFunOnFintype
f g : ⨁ (i : ι), M i
x✝ : ι
⊢ ↑(f + g) x✝ = (↑f + ↑g) x✝
[PROOFSTEP]
rw [add_apply, Pi.add_apply]
[GOAL]
R : Type u
inst✝⁵ : Semiring R
ι : Type v
dec_ι : DecidableEq ι
M : ι → Type w
inst✝⁴ : (i : ι) → AddCommMonoid (M i)
inst✝³ : (i : ι) → Module R (M i)
N : Type u₁
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
φ : (i : ι) → M i →ₗ[R] N
ψ ψ' : (⨁ (i : ι), M i) →ₗ[R] N
inst✝ : Fintype ι
src✝ : (Π₀ (i : ι), M i) ≃ ((i : ι) → M i) := DFinsupp.equivFunOnFintype
c : R
f : ⨁ (i : ι), M i
⊢ AddHom.toFun { toFun := FunLike.coe, map_add' := (_ : ∀ (f g : ⨁ (i : ι), M i), ↑(f + g) = ↑f + ↑g) } (c • f) =
    ↑(RingHom.id R) c •
      AddHom.toFun { toFun := FunLike.coe, map_add' := (_ : ∀ (f g : ⨁ (i : ι), M i), ↑(f + g) = ↑f + ↑g) } f
[PROOFSTEP]
simp_rw [RingHom.id_apply]
[GOAL]
R : Type u
inst✝⁵ : Semiring R
ι : Type v
dec_ι : DecidableEq ι
M : ι → Type w
inst✝⁴ : (i : ι) → AddCommMonoid (M i)
inst✝³ : (i : ι) → Module R (M i)
N : Type u₁
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
φ : (i : ι) → M i →ₗ[R] N
ψ ψ' : (⨁ (i : ι), M i) →ₗ[R] N
inst✝ : Fintype ι
src✝ : (Π₀ (i : ι), M i) ≃ ((i : ι) → M i) := DFinsupp.equivFunOnFintype
c : R
f : ⨁ (i : ι), M i
⊢ ↑(c • f) = c • ↑f
[PROOFSTEP]
rw [DFinsupp.coe_smul]
[GOAL]
R : Type u
inst✝⁶ : Semiring R
ι : Type v
dec_ι : DecidableEq ι
M : ι → Type w
inst✝⁵ : (i : ι) → AddCommMonoid (M i)
inst✝⁴ : (i : ι) → Module R (M i)
N : Type u₁
inst✝³ : AddCommMonoid N
inst✝² : Module R N
φ : (i : ι) → M i →ₗ[R] N
ψ ψ' : (⨁ (i : ι), M i) →ₗ[R] N
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
i : ι
m : M i
⊢ ↑(linearEquivFunOnFintype R ι M) (↑(lof R ι M i) m) = Pi.single i m
[PROOFSTEP]
ext a
[GOAL]
case h
R : Type u
inst✝⁶ : Semiring R
ι : Type v
dec_ι : DecidableEq ι
M : ι → Type w
inst✝⁵ : (i : ι) → AddCommMonoid (M i)
inst✝⁴ : (i : ι) → Module R (M i)
N : Type u₁
inst✝³ : AddCommMonoid N
inst✝² : Module R N
φ : (i : ι) → M i →ₗ[R] N
ψ ψ' : (⨁ (i : ι), M i) →ₗ[R] N
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
i : ι
m : M i
a : ι
⊢ ↑(linearEquivFunOnFintype R ι M) (↑(lof R ι M i) m) a = Pi.single i m a
[PROOFSTEP]
change (DFinsupp.equivFunOnFintype (lof R ι M i m)) a = _
[GOAL]
case h
R : Type u
inst✝⁶ : Semiring R
ι : Type v
dec_ι : DecidableEq ι
M : ι → Type w
inst✝⁵ : (i : ι) → AddCommMonoid (M i)
inst✝⁴ : (i : ι) → Module R (M i)
N : Type u₁
inst✝³ : AddCommMonoid N
inst✝² : Module R N
φ : (i : ι) → M i →ₗ[R] N
ψ ψ' : (⨁ (i : ι), M i) →ₗ[R] N
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
i : ι
m : M i
a : ι
⊢ ↑DFinsupp.equivFunOnFintype (↑(lof R ι M i) m) a = Pi.single i m a
[PROOFSTEP]
convert _root_.congr_fun (DFinsupp.equivFunOnFintype_single i m) a
[GOAL]
R : Type u
inst✝⁶ : Semiring R
ι : Type v
dec_ι : DecidableEq ι
M : ι → Type w
inst✝⁵ : (i : ι) → AddCommMonoid (M i)
inst✝⁴ : (i : ι) → Module R (M i)
N : Type u₁
inst✝³ : AddCommMonoid N
inst✝² : Module R N
φ : (i : ι) → M i →ₗ[R] N
ψ ψ' : (⨁ (i : ι), M i) →ₗ[R] N
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
i : ι
m : M i
⊢ ↑(LinearEquiv.symm (linearEquivFunOnFintype R ι M)) (Pi.single i m) = ↑(lof R ι M i) m
[PROOFSTEP]
change (DFinsupp.equivFunOnFintype.symm (Pi.single i m)) = _
[GOAL]
R : Type u
inst✝⁶ : Semiring R
ι : Type v
dec_ι : DecidableEq ι
M : ι → Type w
inst✝⁵ : (i : ι) → AddCommMonoid (M i)
inst✝⁴ : (i : ι) → Module R (M i)
N : Type u₁
inst✝³ : AddCommMonoid N
inst✝² : Module R N
φ : (i : ι) → M i →ₗ[R] N
ψ ψ' : (⨁ (i : ι), M i) →ₗ[R] N
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
i : ι
m : M i
⊢ ↑DFinsupp.equivFunOnFintype.symm (Pi.single i m) = ↑(lof R ι M i) m
[PROOFSTEP]
rw [DFinsupp.equivFunOnFintype_symm_single i m]
[GOAL]
R : Type u
inst✝⁶ : Semiring R
ι : Type v
dec_ι : DecidableEq ι
M : ι → Type w
inst✝⁵ : (i : ι) → AddCommMonoid (M i)
inst✝⁴ : (i : ι) → Module R (M i)
N : Type u₁
inst✝³ : AddCommMonoid N
inst✝² : Module R N
φ : (i : ι) → M i →ₗ[R] N
ψ ψ' : (⨁ (i : ι), M i) →ₗ[R] N
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
i : ι
m : M i
⊢ DFinsupp.single i m = ↑(lof R ι M i) m
[PROOFSTEP]
rfl
[GOAL]
R : Type u
inst✝⁵ : Semiring R
ι : Type v
dec_ι : DecidableEq ι
M : ι → Type w
inst✝⁴ : (i : ι) → AddCommMonoid (M i)
inst✝³ : (i : ι) → Module R (M i)
N : Type u₁
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
φ : (i : ι) → M i →ₗ[R] N
ψ ψ' : (⨁ (i : ι), M i) →ₗ[R] N
inst✝ : Fintype ι
f : ⨁ (i : ι), M i
⊢ ↑(LinearEquiv.symm (linearEquivFunOnFintype R ι M)) ↑f = f
[PROOFSTEP]
simp [linearEquivFunOnFintype]
[GOAL]
R : Type u
inst✝⁴ : Semiring R
ι : Type v
dec_ι : DecidableEq ι
M : ι → Type w
inst✝³ : (i : ι) → AddCommMonoid (M i)
inst✝² : (i : ι) → Module R (M i)
N : Type u₁
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
φ : (i : ι) → M i →ₗ[R] N
ψ ψ' : (⨁ (i : ι), M i) →ₗ[R] N
f g : ⨁ (i : ι), M i
h : f = g
x✝ : ι
⊢ ↑(component R ι M x✝) f = ↑(component R ι M x✝) g
[PROOFSTEP]
rw [h]
[GOAL]
R : Type u
inst✝⁶ : Semiring R
ι : Type v
dec_ι : DecidableEq ι
M : ι → Type w
inst✝⁵ : (i : ι) → AddCommMonoid (M i)
inst✝⁴ : (i : ι) → Module R (M i)
N : Type u₁
inst✝³ : AddCommMonoid N
inst✝² : Module R N
φ : (i : ι) → M i →ₗ[R] N
ψ ψ' : (⨁ (i : ι), M i) →ₗ[R] N
α : ι → Type u_1
δ : (i : ι) → α i → Type w
inst✝¹ : (i : ι) → (j : α i) → AddCommMonoid (δ i j)
inst✝ : (i : ι) → (j : α i) → Module R (δ i j)
src✝ : (⨁ (i : (_i : ι) × α _i), δ i.fst i.snd) →+ ⨁ (i : ι) (j : α i), δ i j := sigmaCurry
r : R
⊢ ∀ (x : ⨁ (i : (i : ι) × α i), δ i.fst i.snd),
    AddHom.toFun
        { toFun := src✝.toFun,
          map_add' :=
            (_ :
              ∀ (x y : ⨁ (i : (_i : ι) × α _i), δ i.fst i.snd),
                ZeroHom.toFun (↑src✝) (x + y) = ZeroHom.toFun (↑src✝) x + ZeroHom.toFun (↑src✝) y) }
        (r • x) =
      ↑(RingHom.id R) r •
        AddHom.toFun
          { toFun := src✝.toFun,
            map_add' :=
              (_ :
                ∀ (x y : ⨁ (i : (_i : ι) × α _i), δ i.fst i.snd),
                  ZeroHom.toFun (↑src✝) (x + y) = ZeroHom.toFun (↑src✝) x + ZeroHom.toFun (↑src✝) y) }
          x
[PROOFSTEP]
convert DFinsupp.sigmaCurry_smul (δ := δ) r
[GOAL]
R : Type u
inst✝² : Semiring R
ι : Type v
dec_ι : DecidableEq ι
M : Type u_1
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
A : ι → Submodule R M
h : IsInternal A
⊢ iSup A = ⊤
[PROOFSTEP]
rw [Submodule.iSup_eq_range_dfinsupp_lsum, LinearMap.range_eq_top]
[GOAL]
R : Type u
inst✝² : Semiring R
ι : Type v
dec_ι : DecidableEq ι
M : Type u_1
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
A : ι → Submodule R M
h : IsInternal A
⊢ Function.Surjective ↑(↑(DFinsupp.lsum ℕ) fun i => Submodule.subtype (A i))
[PROOFSTEP]
exact Function.Bijective.surjective h
[GOAL]
R : Type u
inst✝² : Semiring R
ι : Type v
dec_ι : DecidableEq ι
M : Type u_1
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
A : ι → Submodule R M
h : IsInternal A
α : ι → Type u_2
v : (i : ι) → Basis (α i) R { x // x ∈ A i }
⊢ ↑(collectedBasis h v) = fun a => ↑(↑(v a.fst) a.snd)
[PROOFSTEP]
funext a
[GOAL]
case h
R : Type u
inst✝² : Semiring R
ι : Type v
dec_ι : DecidableEq ι
M : Type u_1
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
A : ι → Submodule R M
h : IsInternal A
α : ι → Type u_2
v : (i : ι) → Basis (α i) R { x // x ∈ A i }
a : (i : ι) × α i
⊢ ↑(collectedBasis h v) a = ↑(↑(v a.fst) a.snd)
[PROOFSTEP]
simp only [IsInternal.collectedBasis, coeLinearMap, Basis.coe_ofRepr, LinearEquiv.trans_symm, LinearEquiv.symm_symm,
  LinearEquiv.trans_apply, sigmaFinsuppLequivDFinsupp_apply, sigmaFinsuppEquivDFinsupp_single,
  LinearEquiv.ofBijective_apply, sigmaFinsuppAddEquivDFinsupp_apply]
[GOAL]
case h
R : Type u
inst✝² : Semiring R
ι : Type v
dec_ι : DecidableEq ι
M : Type u_1
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
A : ι → Submodule R M
h : IsInternal A
α : ι → Type u_2
v : (i : ι) → Basis (α i) R { x // x ∈ A i }
a : (i : ι) × α i
⊢ ↑(toModule R ι M fun i => Submodule.subtype (A i))
      (↑(LinearEquiv.symm (DFinsupp.mapRange.linearEquiv fun i => (v i).repr))
        (DFinsupp.single a.fst (Finsupp.single a.snd 1))) =
    ↑(↑(v a.fst) a.snd)
[PROOFSTEP]
rw [DFinsupp.mapRange.linearEquiv_symm]
[GOAL]
case h
R : Type u
inst✝² : Semiring R
ι : Type v
dec_ι : DecidableEq ι
M : Type u_1
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
A : ι → Submodule R M
h : IsInternal A
α : ι → Type u_2
v : (i : ι) → Basis (α i) R { x // x ∈ A i }
a : (i : ι) × α i
⊢ ↑(toModule R ι M fun i => Submodule.subtype (A i))
      (↑(DFinsupp.mapRange.linearEquiv fun i => LinearEquiv.symm (v i).repr)
        (DFinsupp.single a.fst (Finsupp.single a.snd 1))) =
    ↑(↑(v a.fst) a.snd)
[PROOFSTEP]
erw [DFinsupp.mapRange.linearEquiv_apply]
[GOAL]
case h
R : Type u
inst✝² : Semiring R
ι : Type v
dec_ι : DecidableEq ι
M : Type u_1
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
A : ι → Submodule R M
h : IsInternal A
α : ι → Type u_2
v : (i : ι) → Basis (α i) R { x // x ∈ A i }
a : (i : ι) × α i
⊢ ↑(toModule R ι M fun i => Submodule.subtype (A i))
      (DFinsupp.mapRange (fun i x => ↑(LinearEquiv.symm (v i).repr) x)
        (_ : ∀ (i : ι), ↑(LinearEquiv.symm (v i).repr) 0 = 0) (DFinsupp.single a.fst (Finsupp.single a.snd 1))) =
    ↑(↑(v a.fst) a.snd)
[PROOFSTEP]
simp only [DFinsupp.mapRange_single, Basis.repr_symm_apply, Finsupp.total_single, one_smul, toModule]
[GOAL]
case h
R : Type u
inst✝² : Semiring R
ι : Type v
dec_ι : DecidableEq ι
M : Type u_1
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
A : ι → Submodule R M
h : IsInternal A
α : ι → Type u_2
v : (i : ι) → Basis (α i) R { x // x ∈ A i }
a : (i : ι) × α i
⊢ ↑(↑(DFinsupp.lsum ℕ) fun i => Submodule.subtype (A i)) (DFinsupp.single a.fst (↑(v a.fst) a.snd)) =
    ↑(↑(v a.fst) a.snd)
[PROOFSTEP]
erw [DFinsupp.lsum_single]
[GOAL]
case h
R : Type u
inst✝² : Semiring R
ι : Type v
dec_ι : DecidableEq ι
M : Type u_1
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
A : ι → Submodule R M
h : IsInternal A
α : ι → Type u_2
v : (i : ι) → Basis (α i) R { x // x ∈ A i }
a : (i : ι) × α i
⊢ ↑(Submodule.subtype (A a.fst)) (↑(v a.fst) a.snd) = ↑(↑(v a.fst) a.snd)
[PROOFSTEP]
simp only [Submodule.coeSubtype]
[GOAL]
R : Type u
inst✝² : Semiring R
ι : Type v
dec_ι : DecidableEq ι
M : Type u_1
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
A : ι → Submodule R M
h : IsInternal A
α : ι → Type u_2
v : (i : ι) → Basis (α i) R { x // x ∈ A i }
a : (i : ι) × α i
⊢ ↑(collectedBasis h v) a ∈ A a.fst
[PROOFSTEP]
simp
[GOAL]
R : Type u
inst✝² : Semiring R
ι : Type v
dec_ι : DecidableEq ι
M : Type u_1
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
A✝ A : ι → Submodule R M
i j : ι
hij : i ≠ j
h : Set.univ = {i, j}
hi : IsInternal A
⊢ iSup A = A i ⊔ A j
[PROOFSTEP]
rw [← sSup_pair, iSup, ← Set.image_univ, h, Set.image_insert_eq, Set.image_singleton]
[GOAL]
R : Type u
inst✝² : Ring R
ι : Type v
dec_ι : DecidableEq ι
M : Type u_1
inst✝¹ : AddCommGroup M
inst✝ : Module R M
A : ι → Submodule R M
i j : ι
hij : i ≠ j
h : Set.univ = {i, j}
⊢ IsInternal A ↔ IsCompl (A i) (A j)
[PROOFSTEP]
have : ∀ k, k = i ∨ k = j := fun k ↦ by simpa using Set.ext_iff.mp h k
[GOAL]
R : Type u
inst✝² : Ring R
ι : Type v
dec_ι : DecidableEq ι
M : Type u_1
inst✝¹ : AddCommGroup M
inst✝ : Module R M
A : ι → Submodule R M
i j : ι
hij : i ≠ j
h : Set.univ = {i, j}
k : ι
⊢ k = i ∨ k = j
[PROOFSTEP]
simpa using Set.ext_iff.mp h k
[GOAL]
R : Type u
inst✝² : Ring R
ι : Type v
dec_ι : DecidableEq ι
M : Type u_1
inst✝¹ : AddCommGroup M
inst✝ : Module R M
A : ι → Submodule R M
i j : ι
hij : i ≠ j
h : Set.univ = {i, j}
this : ∀ (k : ι), k = i ∨ k = j
⊢ IsInternal A ↔ IsCompl (A i) (A j)
[PROOFSTEP]
rw [isInternal_submodule_iff_independent_and_iSup_eq_top, iSup, ← Set.image_univ, h, Set.image_insert_eq,
  Set.image_singleton, sSup_pair, CompleteLattice.independent_pair hij this]
[GOAL]
R : Type u
inst✝² : Ring R
ι : Type v
dec_ι : DecidableEq ι
M : Type u_1
inst✝¹ : AddCommGroup M
inst✝ : Module R M
A : ι → Submodule R M
i j : ι
hij : i ≠ j
h : Set.univ = {i, j}
this : ∀ (k : ι), k = i ∨ k = j
⊢ Disjoint (A i) (A j) ∧ A i ⊔ A j = ⊤ ↔ IsCompl (A i) (A j)
[PROOFSTEP]
exact ⟨fun ⟨hd, ht⟩ ↦ ⟨hd, codisjoint_iff.mpr ht⟩, fun ⟨hd, ht⟩ ↦ ⟨hd, ht.eq_top⟩⟩
