[GOAL]
R : Type u_1
M : Type u_2
ι : Type u_3
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
φ : ι → Type u_4
f : (ι : ι) → φ ι → M
hf : ∀ (i : ι), LinearIndependent R (f i)
⊢ LinearIndependent R fun ix => single ix.fst (f ix.fst ix.snd)
[PROOFSTEP]
apply @linearIndependent_iUnion_finite R _ _ _ _ ι φ fun i x => single i (f i x)
[GOAL]
case hindep
R : Type u_1
M : Type u_2
ι : Type u_3
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
φ : ι → Type u_4
f : (ι : ι) → φ ι → M
hf : ∀ (i : ι), LinearIndependent R (f i)
⊢ ∀ (j : ι), LinearIndependent R fun x => single j (f j x)
[PROOFSTEP]
intro i
[GOAL]
case hindep
R : Type u_1
M : Type u_2
ι : Type u_3
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
φ : ι → Type u_4
f : (ι : ι) → φ ι → M
hf : ∀ (i : ι), LinearIndependent R (f i)
i : ι
⊢ LinearIndependent R fun x => single i (f i x)
[PROOFSTEP]
have h_disjoint : Disjoint (span R (range (f i))) (ker (lsingle i)) :=
  by
  rw [ker_lsingle]
  exact disjoint_bot_right
[GOAL]
R : Type u_1
M : Type u_2
ι : Type u_3
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
φ : ι → Type u_4
f : (ι : ι) → φ ι → M
hf : ∀ (i : ι), LinearIndependent R (f i)
i : ι
⊢ Disjoint (span R (Set.range (f i))) (ker (lsingle i))
[PROOFSTEP]
rw [ker_lsingle]
[GOAL]
R : Type u_1
M : Type u_2
ι : Type u_3
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
φ : ι → Type u_4
f : (ι : ι) → φ ι → M
hf : ∀ (i : ι), LinearIndependent R (f i)
i : ι
⊢ Disjoint (span R (Set.range (f i))) ⊥
[PROOFSTEP]
exact disjoint_bot_right
[GOAL]
case hindep
R : Type u_1
M : Type u_2
ι : Type u_3
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
φ : ι → Type u_4
f : (ι : ι) → φ ι → M
hf : ∀ (i : ι), LinearIndependent R (f i)
i : ι
h_disjoint : Disjoint (span R (Set.range (f i))) (ker (lsingle i))
⊢ LinearIndependent R fun x => single i (f i x)
[PROOFSTEP]
apply (hf i).map h_disjoint
[GOAL]
case hd
R : Type u_1
M : Type u_2
ι : Type u_3
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
φ : ι → Type u_4
f : (ι : ι) → φ ι → M
hf : ∀ (i : ι), LinearIndependent R (f i)
⊢ ∀ (i : ι) (t : Set ι),
    Set.Finite t →
      ¬i ∈ t →
        Disjoint (span R (Set.range fun x => single i (f i x)))
          (⨆ (i : ι) (_ : i ∈ t), span R (Set.range fun x => single i (f i x)))
[PROOFSTEP]
intro i t _ hit
[GOAL]
case hd
R : Type u_1
M : Type u_2
ι : Type u_3
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
φ : ι → Type u_4
f : (ι : ι) → φ ι → M
hf : ∀ (i : ι), LinearIndependent R (f i)
i : ι
t : Set ι
a✝ : Set.Finite t
hit : ¬i ∈ t
⊢ Disjoint (span R (Set.range fun x => single i (f i x)))
    (⨆ (i : ι) (_ : i ∈ t), span R (Set.range fun x => single i (f i x)))
[PROOFSTEP]
refine' (disjoint_lsingle_lsingle { i } t (disjoint_singleton_left.2 hit)).mono _ _
[GOAL]
case hd.refine'_1
R : Type u_1
M : Type u_2
ι : Type u_3
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
φ : ι → Type u_4
f : (ι : ι) → φ ι → M
hf : ∀ (i : ι), LinearIndependent R (f i)
i : ι
t : Set ι
a✝ : Set.Finite t
hit : ¬i ∈ t
⊢ span R (Set.range fun x => single i (f i x)) ≤ ⨆ (a : ι) (_ : a ∈ {i}), LinearMap.range (lsingle a)
[PROOFSTEP]
rw [span_le]
[GOAL]
case hd.refine'_1
R : Type u_1
M : Type u_2
ι : Type u_3
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
φ : ι → Type u_4
f : (ι : ι) → φ ι → M
hf : ∀ (i : ι), LinearIndependent R (f i)
i : ι
t : Set ι
a✝ : Set.Finite t
hit : ¬i ∈ t
⊢ (Set.range fun x => single i (f i x)) ⊆ ↑(⨆ (a : ι) (_ : a ∈ {i}), LinearMap.range (lsingle a))
[PROOFSTEP]
simp only [iSup_singleton]
[GOAL]
case hd.refine'_1
R : Type u_1
M : Type u_2
ι : Type u_3
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
φ : ι → Type u_4
f : (ι : ι) → φ ι → M
hf : ∀ (i : ι), LinearIndependent R (f i)
i : ι
t : Set ι
a✝ : Set.Finite t
hit : ¬i ∈ t
⊢ (Set.range fun x => single i (f i x)) ⊆ ↑(LinearMap.range (lsingle i))
[PROOFSTEP]
rw [range_coe]
[GOAL]
case hd.refine'_1
R : Type u_1
M : Type u_2
ι : Type u_3
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
φ : ι → Type u_4
f : (ι : ι) → φ ι → M
hf : ∀ (i : ι), LinearIndependent R (f i)
i : ι
t : Set ι
a✝ : Set.Finite t
hit : ¬i ∈ t
⊢ (Set.range fun x => single i (f i x)) ⊆ Set.range ↑(lsingle i)
[PROOFSTEP]
apply range_comp_subset_range _ (lsingle i)
[GOAL]
case hd.refine'_2
R : Type u_1
M : Type u_2
ι : Type u_3
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
φ : ι → Type u_4
f : (ι : ι) → φ ι → M
hf : ∀ (i : ι), LinearIndependent R (f i)
i : ι
t : Set ι
a✝ : Set.Finite t
hit : ¬i ∈ t
⊢ ⨆ (i : ι) (_ : i ∈ t), span R (Set.range fun x => single i (f i x)) ≤
    ⨆ (a : ι) (_ : a ∈ t), LinearMap.range (lsingle a)
[PROOFSTEP]
refine' iSup₂_mono fun i hi => _
[GOAL]
case hd.refine'_2
R : Type u_1
M : Type u_2
ι : Type u_3
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
φ : ι → Type u_4
f : (ι : ι) → φ ι → M
hf : ∀ (i : ι), LinearIndependent R (f i)
i✝ : ι
t : Set ι
a✝ : Set.Finite t
hit : ¬i✝ ∈ t
i : ι
hi : i ∈ t
⊢ span R (Set.range fun x => single i (f i x)) ≤ LinearMap.range (lsingle i)
[PROOFSTEP]
rw [span_le, range_coe]
[GOAL]
case hd.refine'_2
R : Type u_1
M : Type u_2
ι : Type u_3
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
φ : ι → Type u_4
f : (ι : ι) → φ ι → M
hf : ∀ (i : ι), LinearIndependent R (f i)
i✝ : ι
t : Set ι
a✝ : Set.Finite t
hit : ¬i✝ ∈ t
i : ι
hi : i ∈ t
⊢ (Set.range fun x => single i (f i x)) ⊆ Set.range ↑(lsingle i)
[PROOFSTEP]
apply range_comp_subset_range _ (lsingle i)
[GOAL]
R : Type u_1
M : Type u_2
ι : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
φ : ι → Type u_4
b : (i : ι) → Basis (φ i) R M
g : ι →₀ M
ix : (i : ι) × φ i
⊢ (ix ∈ Finset.sigma g.support fun i => (↑(b i).repr (↑g i)).support) ↔
    (fun ix => ↑(↑(b ix.fst).repr (↑g ix.fst)) ix.snd) ix ≠ 0
[PROOFSTEP]
simp only [Finset.mem_sigma, mem_support_iff, and_iff_right_iff_imp, Ne.def]
[GOAL]
R : Type u_1
M : Type u_2
ι : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
φ : ι → Type u_4
b : (i : ι) → Basis (φ i) R M
g : ι →₀ M
ix : (i : ι) × φ i
⊢ ¬↑(↑(b ix.fst).repr (↑g ix.fst)) ix.snd = 0 → ¬↑g ix.fst = 0
[PROOFSTEP]
intro b hg
[GOAL]
R : Type u_1
M : Type u_2
ι : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
φ : ι → Type u_4
b✝ : (i : ι) → Basis (φ i) R M
g : ι →₀ M
ix : (i : ι) × φ i
b : ¬↑(↑(b✝ ix.fst).repr (↑g ix.fst)) ix.snd = 0
hg : ↑g ix.fst = 0
⊢ False
[PROOFSTEP]
simp [hg] at b 
[GOAL]
R : Type u_1
M : Type u_2
ι : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
φ : ι → Type u_4
b : (i : ι) → Basis (φ i) R M
g h : ι →₀ M
⊢ (fun g =>
        { support := Finset.sigma g.support fun i => (↑(b i).repr (↑g i)).support,
          toFun := fun ix => ↑(↑(b ix.fst).repr (↑g ix.fst)) ix.snd,
          mem_support_toFun :=
            (_ :
              ∀ (ix : (i : ι) × φ i),
                (ix ∈ Finset.sigma g.support fun i => (↑(b i).repr (↑g i)).support) ↔
                  (fun ix => ↑(↑(b ix.fst).repr (↑g ix.fst)) ix.snd) ix ≠ 0) })
      (g + h) =
    (fun g =>
          { support := Finset.sigma g.support fun i => (↑(b i).repr (↑g i)).support,
            toFun := fun ix => ↑(↑(b ix.fst).repr (↑g ix.fst)) ix.snd,
            mem_support_toFun :=
              (_ :
                ∀ (ix : (i : ι) × φ i),
                  (ix ∈ Finset.sigma g.support fun i => (↑(b i).repr (↑g i)).support) ↔
                    (fun ix => ↑(↑(b ix.fst).repr (↑g ix.fst)) ix.snd) ix ≠ 0) })
        g +
      (fun g =>
          { support := Finset.sigma g.support fun i => (↑(b i).repr (↑g i)).support,
            toFun := fun ix => ↑(↑(b ix.fst).repr (↑g ix.fst)) ix.snd,
            mem_support_toFun :=
              (_ :
                ∀ (ix : (i : ι) × φ i),
                  (ix ∈ Finset.sigma g.support fun i => (↑(b i).repr (↑g i)).support) ↔
                    (fun ix => ↑(↑(b ix.fst).repr (↑g ix.fst)) ix.snd) ix ≠ 0) })
        h
[PROOFSTEP]
ext ⟨i, x⟩
[GOAL]
case h.mk
R : Type u_1
M : Type u_2
ι : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
φ : ι → Type u_4
b : (i : ι) → Basis (φ i) R M
g h : ι →₀ M
i : ι
x : φ i
⊢ ↑((fun g =>
            { support := Finset.sigma g.support fun i => (↑(b i).repr (↑g i)).support,
              toFun := fun ix => ↑(↑(b ix.fst).repr (↑g ix.fst)) ix.snd,
              mem_support_toFun :=
                (_ :
                  ∀ (ix : (i : ι) × φ i),
                    (ix ∈ Finset.sigma g.support fun i => (↑(b i).repr (↑g i)).support) ↔
                      (fun ix => ↑(↑(b ix.fst).repr (↑g ix.fst)) ix.snd) ix ≠ 0) })
          (g + h))
      { fst := i, snd := x } =
    ↑((fun g =>
              { support := Finset.sigma g.support fun i => (↑(b i).repr (↑g i)).support,
                toFun := fun ix => ↑(↑(b ix.fst).repr (↑g ix.fst)) ix.snd,
                mem_support_toFun :=
                  (_ :
                    ∀ (ix : (i : ι) × φ i),
                      (ix ∈ Finset.sigma g.support fun i => (↑(b i).repr (↑g i)).support) ↔
                        (fun ix => ↑(↑(b ix.fst).repr (↑g ix.fst)) ix.snd) ix ≠ 0) })
            g +
          (fun g =>
              { support := Finset.sigma g.support fun i => (↑(b i).repr (↑g i)).support,
                toFun := fun ix => ↑(↑(b ix.fst).repr (↑g ix.fst)) ix.snd,
                mem_support_toFun :=
                  (_ :
                    ∀ (ix : (i : ι) × φ i),
                      (ix ∈ Finset.sigma g.support fun i => (↑(b i).repr (↑g i)).support) ↔
                        (fun ix => ↑(↑(b ix.fst).repr (↑g ix.fst)) ix.snd) ix ≠ 0) })
            h)
      { fst := i, snd := x }
[PROOFSTEP]
simp only [coe_mk, add_apply, LinearEquiv.map_add]
[GOAL]
R : Type u_1
M : Type u_2
ι : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
φ : ι → Type u_4
b : (i : ι) → Basis (φ i) R M
c : R
h : ι →₀ M
⊢ AddHom.toFun
      {
        toFun := fun g =>
          { support := Finset.sigma g.support fun i => (↑(b i).repr (↑g i)).support,
            toFun := fun ix => ↑(↑(b ix.fst).repr (↑g ix.fst)) ix.snd,
            mem_support_toFun :=
              (_ :
                ∀ (ix : (i : ι) × φ i),
                  (ix ∈ Finset.sigma g.support fun i => (↑(b i).repr (↑g i)).support) ↔
                    (fun ix => ↑(↑(b ix.fst).repr (↑g ix.fst)) ix.snd) ix ≠ 0) },
        map_add' :=
          (_ :
            ∀ (g h : ι →₀ M),
              (fun g =>
                    { support := Finset.sigma g.support fun i => (↑(b i).repr (↑g i)).support,
                      toFun := fun ix => ↑(↑(b ix.fst).repr (↑g ix.fst)) ix.snd,
                      mem_support_toFun :=
                        (_ :
                          ∀ (ix : (i : ι) × φ i),
                            (ix ∈ Finset.sigma g.support fun i => (↑(b i).repr (↑g i)).support) ↔
                              (fun ix => ↑(↑(b ix.fst).repr (↑g ix.fst)) ix.snd) ix ≠ 0) })
                  (g + h) =
                (fun g =>
                      { support := Finset.sigma g.support fun i => (↑(b i).repr (↑g i)).support,
                        toFun := fun ix => ↑(↑(b ix.fst).repr (↑g ix.fst)) ix.snd,
                        mem_support_toFun :=
                          (_ :
                            ∀ (ix : (i : ι) × φ i),
                              (ix ∈ Finset.sigma g.support fun i => (↑(b i).repr (↑g i)).support) ↔
                                (fun ix => ↑(↑(b ix.fst).repr (↑g ix.fst)) ix.snd) ix ≠ 0) })
                    g +
                  (fun g =>
                      { support := Finset.sigma g.support fun i => (↑(b i).repr (↑g i)).support,
                        toFun := fun ix => ↑(↑(b ix.fst).repr (↑g ix.fst)) ix.snd,
                        mem_support_toFun :=
                          (_ :
                            ∀ (ix : (i : ι) × φ i),
                              (ix ∈ Finset.sigma g.support fun i => (↑(b i).repr (↑g i)).support) ↔
                                (fun ix => ↑(↑(b ix.fst).repr (↑g ix.fst)) ix.snd) ix ≠ 0) })
                    h) }
      (c • h) =
    ↑(RingHom.id R) c •
      AddHom.toFun
        {
          toFun := fun g =>
            { support := Finset.sigma g.support fun i => (↑(b i).repr (↑g i)).support,
              toFun := fun ix => ↑(↑(b ix.fst).repr (↑g ix.fst)) ix.snd,
              mem_support_toFun :=
                (_ :
                  ∀ (ix : (i : ι) × φ i),
                    (ix ∈ Finset.sigma g.support fun i => (↑(b i).repr (↑g i)).support) ↔
                      (fun ix => ↑(↑(b ix.fst).repr (↑g ix.fst)) ix.snd) ix ≠ 0) },
          map_add' :=
            (_ :
              ∀ (g h : ι →₀ M),
                (fun g =>
                      { support := Finset.sigma g.support fun i => (↑(b i).repr (↑g i)).support,
                        toFun := fun ix => ↑(↑(b ix.fst).repr (↑g ix.fst)) ix.snd,
                        mem_support_toFun :=
                          (_ :
                            ∀ (ix : (i : ι) × φ i),
                              (ix ∈ Finset.sigma g.support fun i => (↑(b i).repr (↑g i)).support) ↔
                                (fun ix => ↑(↑(b ix.fst).repr (↑g ix.fst)) ix.snd) ix ≠ 0) })
                    (g + h) =
                  (fun g =>
                        { support := Finset.sigma g.support fun i => (↑(b i).repr (↑g i)).support,
                          toFun := fun ix => ↑(↑(b ix.fst).repr (↑g ix.fst)) ix.snd,
                          mem_support_toFun :=
                            (_ :
                              ∀ (ix : (i : ι) × φ i),
                                (ix ∈ Finset.sigma g.support fun i => (↑(b i).repr (↑g i)).support) ↔
                                  (fun ix => ↑(↑(b ix.fst).repr (↑g ix.fst)) ix.snd) ix ≠ 0) })
                      g +
                    (fun g =>
                        { support := Finset.sigma g.support fun i => (↑(b i).repr (↑g i)).support,
                          toFun := fun ix => ↑(↑(b ix.fst).repr (↑g ix.fst)) ix.snd,
                          mem_support_toFun :=
                            (_ :
                              ∀ (ix : (i : ι) × φ i),
                                (ix ∈ Finset.sigma g.support fun i => (↑(b i).repr (↑g i)).support) ↔
                                  (fun ix => ↑(↑(b ix.fst).repr (↑g ix.fst)) ix.snd) ix ≠ 0) })
                      h) }
        h
[PROOFSTEP]
ext ⟨i, x⟩
[GOAL]
case h.mk
R : Type u_1
M : Type u_2
ι : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
φ : ι → Type u_4
b : (i : ι) → Basis (φ i) R M
c : R
h : ι →₀ M
i : ι
x : φ i
⊢ ↑(AddHom.toFun
          {
            toFun := fun g =>
              { support := Finset.sigma g.support fun i => (↑(b i).repr (↑g i)).support,
                toFun := fun ix => ↑(↑(b ix.fst).repr (↑g ix.fst)) ix.snd,
                mem_support_toFun :=
                  (_ :
                    ∀ (ix : (i : ι) × φ i),
                      (ix ∈ Finset.sigma g.support fun i => (↑(b i).repr (↑g i)).support) ↔
                        (fun ix => ↑(↑(b ix.fst).repr (↑g ix.fst)) ix.snd) ix ≠ 0) },
            map_add' :=
              (_ :
                ∀ (g h : ι →₀ M),
                  (fun g =>
                        { support := Finset.sigma g.support fun i => (↑(b i).repr (↑g i)).support,
                          toFun := fun ix => ↑(↑(b ix.fst).repr (↑g ix.fst)) ix.snd,
                          mem_support_toFun :=
                            (_ :
                              ∀ (ix : (i : ι) × φ i),
                                (ix ∈ Finset.sigma g.support fun i => (↑(b i).repr (↑g i)).support) ↔
                                  (fun ix => ↑(↑(b ix.fst).repr (↑g ix.fst)) ix.snd) ix ≠ 0) })
                      (g + h) =
                    (fun g =>
                          { support := Finset.sigma g.support fun i => (↑(b i).repr (↑g i)).support,
                            toFun := fun ix => ↑(↑(b ix.fst).repr (↑g ix.fst)) ix.snd,
                            mem_support_toFun :=
                              (_ :
                                ∀ (ix : (i : ι) × φ i),
                                  (ix ∈ Finset.sigma g.support fun i => (↑(b i).repr (↑g i)).support) ↔
                                    (fun ix => ↑(↑(b ix.fst).repr (↑g ix.fst)) ix.snd) ix ≠ 0) })
                        g +
                      (fun g =>
                          { support := Finset.sigma g.support fun i => (↑(b i).repr (↑g i)).support,
                            toFun := fun ix => ↑(↑(b ix.fst).repr (↑g ix.fst)) ix.snd,
                            mem_support_toFun :=
                              (_ :
                                ∀ (ix : (i : ι) × φ i),
                                  (ix ∈ Finset.sigma g.support fun i => (↑(b i).repr (↑g i)).support) ↔
                                    (fun ix => ↑(↑(b ix.fst).repr (↑g ix.fst)) ix.snd) ix ≠ 0) })
                        h) }
          (c • h))
      { fst := i, snd := x } =
    ↑(↑(RingHom.id R) c •
          AddHom.toFun
            {
              toFun := fun g =>
                { support := Finset.sigma g.support fun i => (↑(b i).repr (↑g i)).support,
                  toFun := fun ix => ↑(↑(b ix.fst).repr (↑g ix.fst)) ix.snd,
                  mem_support_toFun :=
                    (_ :
                      ∀ (ix : (i : ι) × φ i),
                        (ix ∈ Finset.sigma g.support fun i => (↑(b i).repr (↑g i)).support) ↔
                          (fun ix => ↑(↑(b ix.fst).repr (↑g ix.fst)) ix.snd) ix ≠ 0) },
              map_add' :=
                (_ :
                  ∀ (g h : ι →₀ M),
                    (fun g =>
                          { support := Finset.sigma g.support fun i => (↑(b i).repr (↑g i)).support,
                            toFun := fun ix => ↑(↑(b ix.fst).repr (↑g ix.fst)) ix.snd,
                            mem_support_toFun :=
                              (_ :
                                ∀ (ix : (i : ι) × φ i),
                                  (ix ∈ Finset.sigma g.support fun i => (↑(b i).repr (↑g i)).support) ↔
                                    (fun ix => ↑(↑(b ix.fst).repr (↑g ix.fst)) ix.snd) ix ≠ 0) })
                        (g + h) =
                      (fun g =>
                            { support := Finset.sigma g.support fun i => (↑(b i).repr (↑g i)).support,
                              toFun := fun ix => ↑(↑(b ix.fst).repr (↑g ix.fst)) ix.snd,
                              mem_support_toFun :=
                                (_ :
                                  ∀ (ix : (i : ι) × φ i),
                                    (ix ∈ Finset.sigma g.support fun i => (↑(b i).repr (↑g i)).support) ↔
                                      (fun ix => ↑(↑(b ix.fst).repr (↑g ix.fst)) ix.snd) ix ≠ 0) })
                          g +
                        (fun g =>
                            { support := Finset.sigma g.support fun i => (↑(b i).repr (↑g i)).support,
                              toFun := fun ix => ↑(↑(b ix.fst).repr (↑g ix.fst)) ix.snd,
                              mem_support_toFun :=
                                (_ :
                                  ∀ (ix : (i : ι) × φ i),
                                    (ix ∈ Finset.sigma g.support fun i => (↑(b i).repr (↑g i)).support) ↔
                                      (fun ix => ↑(↑(b ix.fst).repr (↑g ix.fst)) ix.snd) ix ≠ 0) })
                          h) }
            h)
      { fst := i, snd := x }
[PROOFSTEP]
simp only [coe_mk, smul_apply, LinearEquiv.map_smul, RingHom.id_apply]
[GOAL]
R : Type u_1
M : Type u_2
ι : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
φ : ι → Type u_4
b : (i : ι) → Basis (φ i) R M
g : (i : ι) × φ i →₀ R
i : ι
⊢ i ∈ Finset.image Sigma.fst g.support ↔
    (fun i =>
          ↑(LinearEquiv.symm (b i).repr)
            (comapDomain (Sigma.mk i) g (_ : InjOn (Sigma.mk i) (Sigma.mk i ⁻¹' ↑g.support))))
        i ≠
      0
[PROOFSTEP]
rw [Ne.def, ← (b i).repr.injective.eq_iff, (b i).repr.apply_symm_apply, FunLike.ext_iff]
[GOAL]
R : Type u_1
M : Type u_2
ι : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
φ : ι → Type u_4
b : (i : ι) → Basis (φ i) R M
g : (i : ι) × φ i →₀ R
i : ι
⊢ i ∈ Finset.image Sigma.fst g.support ↔
    ¬∀ (x : φ i),
        ↑(comapDomain (Sigma.mk i) g (_ : InjOn (Sigma.mk i) (Sigma.mk i ⁻¹' ↑g.support))) x = ↑(↑(b i).repr 0) x
[PROOFSTEP]
simp only [exists_prop, LinearEquiv.map_zero, comapDomain_apply, zero_apply, exists_and_right, mem_support_iff,
  exists_eq_right, Sigma.exists, Finset.mem_image, not_forall]
[GOAL]
R : Type u_1
M : Type u_2
ι : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
φ : ι → Type u_4
b : (i : ι) → Basis (φ i) R M
g : ι →₀ M
⊢ (fun g =>
        { support := Finset.image Sigma.fst g.support,
          toFun := fun i =>
            ↑(LinearEquiv.symm (b i).repr)
              (comapDomain (Sigma.mk i) g (_ : InjOn (Sigma.mk i) (Sigma.mk i ⁻¹' ↑g.support))),
          mem_support_toFun :=
            (_ :
              ∀ (i : ι),
                i ∈ Finset.image Sigma.fst g.support ↔
                  (fun i =>
                        ↑(LinearEquiv.symm (b i).repr)
                          (comapDomain (Sigma.mk i) g (_ : InjOn (Sigma.mk i) (Sigma.mk i ⁻¹' ↑g.support))))
                      i ≠
                    0) })
      (AddHom.toFun
        {
            toAddHom :=
              {
                toFun := fun g =>
                  { support := Finset.sigma g.support fun i => (↑(b i).repr (↑g i)).support,
                    toFun := fun ix => ↑(↑(b ix.fst).repr (↑g ix.fst)) ix.snd,
                    mem_support_toFun :=
                      (_ :
                        ∀ (ix : (i : ι) × φ i),
                          (ix ∈ Finset.sigma g.support fun i => (↑(b i).repr (↑g i)).support) ↔
                            (fun ix => ↑(↑(b ix.fst).repr (↑g ix.fst)) ix.snd) ix ≠ 0) },
                map_add' :=
                  (_ :
                    ∀ (g h : ι →₀ M),
                      (fun g =>
                            { support := Finset.sigma g.support fun i => (↑(b i).repr (↑g i)).support,
                              toFun := fun ix => ↑(↑(b ix.fst).repr (↑g ix.fst)) ix.snd,
                              mem_support_toFun :=
                                (_ :
                                  ∀ (ix : (i : ι) × φ i),
                                    (ix ∈ Finset.sigma g.support fun i => (↑(b i).repr (↑g i)).support) ↔
                                      (fun ix => ↑(↑(b ix.fst).repr (↑g ix.fst)) ix.snd) ix ≠ 0) })
                          (g + h) =
                        (fun g =>
                              { support := Finset.sigma g.support fun i => (↑(b i).repr (↑g i)).support,
                                toFun := fun ix => ↑(↑(b ix.fst).repr (↑g ix.fst)) ix.snd,
                                mem_support_toFun :=
                                  (_ :
                                    ∀ (ix : (i : ι) × φ i),
                                      (ix ∈ Finset.sigma g.support fun i => (↑(b i).repr (↑g i)).support) ↔
                                        (fun ix => ↑(↑(b ix.fst).repr (↑g ix.fst)) ix.snd) ix ≠ 0) })
                            g +
                          (fun g =>
                              { support := Finset.sigma g.support fun i => (↑(b i).repr (↑g i)).support,
                                toFun := fun ix => ↑(↑(b ix.fst).repr (↑g ix.fst)) ix.snd,
                                mem_support_toFun :=
                                  (_ :
                                    ∀ (ix : (i : ι) × φ i),
                                      (ix ∈ Finset.sigma g.support fun i => (↑(b i).repr (↑g i)).support) ↔
                                        (fun ix => ↑(↑(b ix.fst).repr (↑g ix.fst)) ix.snd) ix ≠ 0) })
                            h) },
            map_smul' :=
              (_ :
                ∀ (c : R) (h : ι →₀ M),
                  AddHom.toFun
                      {
                        toFun := fun g =>
                          { support := Finset.sigma g.support fun i => (↑(b i).repr (↑g i)).support,
                            toFun := fun ix => ↑(↑(b ix.fst).repr (↑g ix.fst)) ix.snd,
                            mem_support_toFun :=
                              (_ :
                                ∀ (ix : (i : ι) × φ i),
                                  (ix ∈ Finset.sigma g.support fun i => (↑(b i).repr (↑g i)).support) ↔
                                    (fun ix => ↑(↑(b ix.fst).repr (↑g ix.fst)) ix.snd) ix ≠ 0) },
                        map_add' :=
                          (_ :
                            ∀ (g h : ι →₀ M),
                              (fun g =>
                                    { support := Finset.sigma g.support fun i => (↑(b i).repr (↑g i)).support,
                                      toFun := fun ix => ↑(↑(b ix.fst).repr (↑g ix.fst)) ix.snd,
                                      mem_support_toFun :=
                                        (_ :
                                          ∀ (ix : (i : ι) × φ i),
                                            (ix ∈ Finset.sigma g.support fun i => (↑(b i).repr (↑g i)).support) ↔
                                              (fun ix => ↑(↑(b ix.fst).repr (↑g ix.fst)) ix.snd) ix ≠ 0) })
                                  (g + h) =
                                (fun g =>
                                      { support := Finset.sigma g.support fun i => (↑(b i).repr (↑g i)).support,
                                        toFun := fun ix => ↑(↑(b ix.fst).repr (↑g ix.fst)) ix.snd,
                                        mem_support_toFun :=
                                          (_ :
                                            ∀ (ix : (i : ι) × φ i),
                                              (ix ∈ Finset.sigma g.support fun i => (↑(b i).repr (↑g i)).support) ↔
                                                (fun ix => ↑(↑(b ix.fst).repr (↑g ix.fst)) ix.snd) ix ≠ 0) })
                                    g +
                                  (fun g =>
                                      { support := Finset.sigma g.support fun i => (↑(b i).repr (↑g i)).support,
                                        toFun := fun ix => ↑(↑(b ix.fst).repr (↑g ix.fst)) ix.snd,
                                        mem_support_toFun :=
                                          (_ :
                                            ∀ (ix : (i : ι) × φ i),
                                              (ix ∈ Finset.sigma g.support fun i => (↑(b i).repr (↑g i)).support) ↔
                                                (fun ix => ↑(↑(b ix.fst).repr (↑g ix.fst)) ix.snd) ix ≠ 0) })
                                    h) }
                      (c • h) =
                    ↑(RingHom.id R) c •
                      AddHom.toFun
                        {
                          toFun := fun g =>
                            { support := Finset.sigma g.support fun i => (↑(b i).repr (↑g i)).support,
                              toFun := fun ix => ↑(↑(b ix.fst).repr (↑g ix.fst)) ix.snd,
                              mem_support_toFun :=
                                (_ :
                                  ∀ (ix : (i : ι) × φ i),
                                    (ix ∈ Finset.sigma g.support fun i => (↑(b i).repr (↑g i)).support) ↔
                                      (fun ix => ↑(↑(b ix.fst).repr (↑g ix.fst)) ix.snd) ix ≠ 0) },
                          map_add' :=
                            (_ :
                              ∀ (g h : ι →₀ M),
                                (fun g =>
                                      { support := Finset.sigma g.support fun i => (↑(b i).repr (↑g i)).support,
                                        toFun := fun ix => ↑(↑(b ix.fst).repr (↑g ix.fst)) ix.snd,
                                        mem_support_toFun :=
                                          (_ :
                                            ∀ (ix : (i : ι) × φ i),
                                              (ix ∈ Finset.sigma g.support fun i => (↑(b i).repr (↑g i)).support) ↔
                                                (fun ix => ↑(↑(b ix.fst).repr (↑g ix.fst)) ix.snd) ix ≠ 0) })
                                    (g + h) =
                                  (fun g =>
                                        { support := Finset.sigma g.support fun i => (↑(b i).repr (↑g i)).support,
                                          toFun := fun ix => ↑(↑(b ix.fst).repr (↑g ix.fst)) ix.snd,
                                          mem_support_toFun :=
                                            (_ :
                                              ∀ (ix : (i : ι) × φ i),
                                                (ix ∈ Finset.sigma g.support fun i => (↑(b i).repr (↑g i)).support) ↔
                                                  (fun ix => ↑(↑(b ix.fst).repr (↑g ix.fst)) ix.snd) ix ≠ 0) })
                                      g +
                                    (fun g =>
                                        { support := Finset.sigma g.support fun i => (↑(b i).repr (↑g i)).support,
                                          toFun := fun ix => ↑(↑(b ix.fst).repr (↑g ix.fst)) ix.snd,
                                          mem_support_toFun :=
                                            (_ :
                                              ∀ (ix : (i : ι) × φ i),
                                                (ix ∈ Finset.sigma g.support fun i => (↑(b i).repr (↑g i)).support) ↔
                                                  (fun ix => ↑(↑(b ix.fst).repr (↑g ix.fst)) ix.snd) ix ≠ 0) })
                                      h) }
                        h) }.toAddHom
        g) =
    g
[PROOFSTEP]
ext i
[GOAL]
case h
R : Type u_1
M : Type u_2
ι : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
φ : ι → Type u_4
b : (i : ι) → Basis (φ i) R M
g : ι →₀ M
i : ι
⊢ ↑((fun g =>
            { support := Finset.image Sigma.fst g.support,
              toFun := fun i =>
                ↑(LinearEquiv.symm (b i).repr)
                  (comapDomain (Sigma.mk i) g (_ : InjOn (Sigma.mk i) (Sigma.mk i ⁻¹' ↑g.support))),
              mem_support_toFun :=
                (_ :
                  ∀ (i : ι),
                    i ∈ Finset.image Sigma.fst g.support ↔
                      (fun i =>
                            ↑(LinearEquiv.symm (b i).repr)
                              (comapDomain (Sigma.mk i) g (_ : InjOn (Sigma.mk i) (Sigma.mk i ⁻¹' ↑g.support))))
                          i ≠
                        0) })
          (AddHom.toFun
            {
                toAddHom :=
                  {
                    toFun := fun g =>
                      { support := Finset.sigma g.support fun i => (↑(b i).repr (↑g i)).support,
                        toFun := fun ix => ↑(↑(b ix.fst).repr (↑g ix.fst)) ix.snd,
                        mem_support_toFun :=
                          (_ :
                            ∀ (ix : (i : ι) × φ i),
                              (ix ∈ Finset.sigma g.support fun i => (↑(b i).repr (↑g i)).support) ↔
                                (fun ix => ↑(↑(b ix.fst).repr (↑g ix.fst)) ix.snd) ix ≠ 0) },
                    map_add' :=
                      (_ :
                        ∀ (g h : ι →₀ M),
                          (fun g =>
                                { support := Finset.sigma g.support fun i => (↑(b i).repr (↑g i)).support,
                                  toFun := fun ix => ↑(↑(b ix.fst).repr (↑g ix.fst)) ix.snd,
                                  mem_support_toFun :=
                                    (_ :
                                      ∀ (ix : (i : ι) × φ i),
                                        (ix ∈ Finset.sigma g.support fun i => (↑(b i).repr (↑g i)).support) ↔
                                          (fun ix => ↑(↑(b ix.fst).repr (↑g ix.fst)) ix.snd) ix ≠ 0) })
                              (g + h) =
                            (fun g =>
                                  { support := Finset.sigma g.support fun i => (↑(b i).repr (↑g i)).support,
                                    toFun := fun ix => ↑(↑(b ix.fst).repr (↑g ix.fst)) ix.snd,
                                    mem_support_toFun :=
                                      (_ :
                                        ∀ (ix : (i : ι) × φ i),
                                          (ix ∈ Finset.sigma g.support fun i => (↑(b i).repr (↑g i)).support) ↔
                                            (fun ix => ↑(↑(b ix.fst).repr (↑g ix.fst)) ix.snd) ix ≠ 0) })
                                g +
                              (fun g =>
                                  { support := Finset.sigma g.support fun i => (↑(b i).repr (↑g i)).support,
                                    toFun := fun ix => ↑(↑(b ix.fst).repr (↑g ix.fst)) ix.snd,
                                    mem_support_toFun :=
                                      (_ :
                                        ∀ (ix : (i : ι) × φ i),
                                          (ix ∈ Finset.sigma g.support fun i => (↑(b i).repr (↑g i)).support) ↔
                                            (fun ix => ↑(↑(b ix.fst).repr (↑g ix.fst)) ix.snd) ix ≠ 0) })
                                h) },
                map_smul' :=
                  (_ :
                    ∀ (c : R) (h : ι →₀ M),
                      AddHom.toFun
                          {
                            toFun := fun g =>
                              { support := Finset.sigma g.support fun i => (↑(b i).repr (↑g i)).support,
                                toFun := fun ix => ↑(↑(b ix.fst).repr (↑g ix.fst)) ix.snd,
                                mem_support_toFun :=
                                  (_ :
                                    ∀ (ix : (i : ι) × φ i),
                                      (ix ∈ Finset.sigma g.support fun i => (↑(b i).repr (↑g i)).support) ↔
                                        (fun ix => ↑(↑(b ix.fst).repr (↑g ix.fst)) ix.snd) ix ≠ 0) },
                            map_add' :=
                              (_ :
                                ∀ (g h : ι →₀ M),
                                  (fun g =>
                                        { support := Finset.sigma g.support fun i => (↑(b i).repr (↑g i)).support,
                                          toFun := fun ix => ↑(↑(b ix.fst).repr (↑g ix.fst)) ix.snd,
                                          mem_support_toFun :=
                                            (_ :
                                              ∀ (ix : (i : ι) × φ i),
                                                (ix ∈ Finset.sigma g.support fun i => (↑(b i).repr (↑g i)).support) ↔
                                                  (fun ix => ↑(↑(b ix.fst).repr (↑g ix.fst)) ix.snd) ix ≠ 0) })
                                      (g + h) =
                                    (fun g =>
                                          { support := Finset.sigma g.support fun i => (↑(b i).repr (↑g i)).support,
                                            toFun := fun ix => ↑(↑(b ix.fst).repr (↑g ix.fst)) ix.snd,
                                            mem_support_toFun :=
                                              (_ :
                                                ∀ (ix : (i : ι) × φ i),
                                                  (ix ∈ Finset.sigma g.support fun i => (↑(b i).repr (↑g i)).support) ↔
                                                    (fun ix => ↑(↑(b ix.fst).repr (↑g ix.fst)) ix.snd) ix ≠ 0) })
                                        g +
                                      (fun g =>
                                          { support := Finset.sigma g.support fun i => (↑(b i).repr (↑g i)).support,
                                            toFun := fun ix => ↑(↑(b ix.fst).repr (↑g ix.fst)) ix.snd,
                                            mem_support_toFun :=
                                              (_ :
                                                ∀ (ix : (i : ι) × φ i),
                                                  (ix ∈ Finset.sigma g.support fun i => (↑(b i).repr (↑g i)).support) ↔
                                                    (fun ix => ↑(↑(b ix.fst).repr (↑g ix.fst)) ix.snd) ix ≠ 0) })
                                        h) }
                          (c • h) =
                        ↑(RingHom.id R) c •
                          AddHom.toFun
                            {
                              toFun := fun g =>
                                { support := Finset.sigma g.support fun i => (↑(b i).repr (↑g i)).support,
                                  toFun := fun ix => ↑(↑(b ix.fst).repr (↑g ix.fst)) ix.snd,
                                  mem_support_toFun :=
                                    (_ :
                                      ∀ (ix : (i : ι) × φ i),
                                        (ix ∈ Finset.sigma g.support fun i => (↑(b i).repr (↑g i)).support) ↔
                                          (fun ix => ↑(↑(b ix.fst).repr (↑g ix.fst)) ix.snd) ix ≠ 0) },
                              map_add' :=
                                (_ :
                                  ∀ (g h : ι →₀ M),
                                    (fun g =>
                                          { support := Finset.sigma g.support fun i => (↑(b i).repr (↑g i)).support,
                                            toFun := fun ix => ↑(↑(b ix.fst).repr (↑g ix.fst)) ix.snd,
                                            mem_support_toFun :=
                                              (_ :
                                                ∀ (ix : (i : ι) × φ i),
                                                  (ix ∈ Finset.sigma g.support fun i => (↑(b i).repr (↑g i)).support) ↔
                                                    (fun ix => ↑(↑(b ix.fst).repr (↑g ix.fst)) ix.snd) ix ≠ 0) })
                                        (g + h) =
                                      (fun g =>
                                            { support := Finset.sigma g.support fun i => (↑(b i).repr (↑g i)).support,
                                              toFun := fun ix => ↑(↑(b ix.fst).repr (↑g ix.fst)) ix.snd,
                                              mem_support_toFun :=
                                                (_ :
                                                  ∀ (ix : (i : ι) × φ i),
                                                    (ix ∈
                                                        Finset.sigma g.support fun i => (↑(b i).repr (↑g i)).support) ↔
                                                      (fun ix => ↑(↑(b ix.fst).repr (↑g ix.fst)) ix.snd) ix ≠ 0) })
                                          g +
                                        (fun g =>
                                            { support := Finset.sigma g.support fun i => (↑(b i).repr (↑g i)).support,
                                              toFun := fun ix => ↑(↑(b ix.fst).repr (↑g ix.fst)) ix.snd,
                                              mem_support_toFun :=
                                                (_ :
                                                  ∀ (ix : (i : ι) × φ i),
                                                    (ix ∈
                                                        Finset.sigma g.support fun i => (↑(b i).repr (↑g i)).support) ↔
                                                      (fun ix => ↑(↑(b ix.fst).repr (↑g ix.fst)) ix.snd) ix ≠ 0) })
                                          h) }
                            h) }.toAddHom
            g))
      i =
    ↑g i
[PROOFSTEP]
rw [← (b i).repr.injective.eq_iff]
[GOAL]
case h
R : Type u_1
M : Type u_2
ι : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
φ : ι → Type u_4
b : (i : ι) → Basis (φ i) R M
g : ι →₀ M
i : ι
⊢ ↑(b i).repr
      (↑((fun g =>
              { support := Finset.image Sigma.fst g.support,
                toFun := fun i =>
                  ↑(LinearEquiv.symm (b i).repr)
                    (comapDomain (Sigma.mk i) g (_ : InjOn (Sigma.mk i) (Sigma.mk i ⁻¹' ↑g.support))),
                mem_support_toFun :=
                  (_ :
                    ∀ (i : ι),
                      i ∈ Finset.image Sigma.fst g.support ↔
                        (fun i =>
                              ↑(LinearEquiv.symm (b i).repr)
                                (comapDomain (Sigma.mk i) g (_ : InjOn (Sigma.mk i) (Sigma.mk i ⁻¹' ↑g.support))))
                            i ≠
                          0) })
            (AddHom.toFun
              {
                  toAddHom :=
                    {
                      toFun := fun g =>
                        { support := Finset.sigma g.support fun i => (↑(b i).repr (↑g i)).support,
                          toFun := fun ix => ↑(↑(b ix.fst).repr (↑g ix.fst)) ix.snd,
                          mem_support_toFun :=
                            (_ :
                              ∀ (ix : (i : ι) × φ i),
                                (ix ∈ Finset.sigma g.support fun i => (↑(b i).repr (↑g i)).support) ↔
                                  (fun ix => ↑(↑(b ix.fst).repr (↑g ix.fst)) ix.snd) ix ≠ 0) },
                      map_add' :=
                        (_ :
                          ∀ (g h : ι →₀ M),
                            (fun g =>
                                  { support := Finset.sigma g.support fun i => (↑(b i).repr (↑g i)).support,
                                    toFun := fun ix => ↑(↑(b ix.fst).repr (↑g ix.fst)) ix.snd,
                                    mem_support_toFun :=
                                      (_ :
                                        ∀ (ix : (i : ι) × φ i),
                                          (ix ∈ Finset.sigma g.support fun i => (↑(b i).repr (↑g i)).support) ↔
                                            (fun ix => ↑(↑(b ix.fst).repr (↑g ix.fst)) ix.snd) ix ≠ 0) })
                                (g + h) =
                              (fun g =>
                                    { support := Finset.sigma g.support fun i => (↑(b i).repr (↑g i)).support,
                                      toFun := fun ix => ↑(↑(b ix.fst).repr (↑g ix.fst)) ix.snd,
                                      mem_support_toFun :=
                                        (_ :
                                          ∀ (ix : (i : ι) × φ i),
                                            (ix ∈ Finset.sigma g.support fun i => (↑(b i).repr (↑g i)).support) ↔
                                              (fun ix => ↑(↑(b ix.fst).repr (↑g ix.fst)) ix.snd) ix ≠ 0) })
                                  g +
                                (fun g =>
                                    { support := Finset.sigma g.support fun i => (↑(b i).repr (↑g i)).support,
                                      toFun := fun ix => ↑(↑(b ix.fst).repr (↑g ix.fst)) ix.snd,
                                      mem_support_toFun :=
                                        (_ :
                                          ∀ (ix : (i : ι) × φ i),
                                            (ix ∈ Finset.sigma g.support fun i => (↑(b i).repr (↑g i)).support) ↔
                                              (fun ix => ↑(↑(b ix.fst).repr (↑g ix.fst)) ix.snd) ix ≠ 0) })
                                  h) },
                  map_smul' :=
                    (_ :
                      ∀ (c : R) (h : ι →₀ M),
                        AddHom.toFun
                            {
                              toFun := fun g =>
                                { support := Finset.sigma g.support fun i => (↑(b i).repr (↑g i)).support,
                                  toFun := fun ix => ↑(↑(b ix.fst).repr (↑g ix.fst)) ix.snd,
                                  mem_support_toFun :=
                                    (_ :
                                      ∀ (ix : (i : ι) × φ i),
                                        (ix ∈ Finset.sigma g.support fun i => (↑(b i).repr (↑g i)).support) ↔
                                          (fun ix => ↑(↑(b ix.fst).repr (↑g ix.fst)) ix.snd) ix ≠ 0) },
                              map_add' :=
                                (_ :
                                  ∀ (g h : ι →₀ M),
                                    (fun g =>
                                          { support := Finset.sigma g.support fun i => (↑(b i).repr (↑g i)).support,
                                            toFun := fun ix => ↑(↑(b ix.fst).repr (↑g ix.fst)) ix.snd,
                                            mem_support_toFun :=
                                              (_ :
                                                ∀ (ix : (i : ι) × φ i),
                                                  (ix ∈ Finset.sigma g.support fun i => (↑(b i).repr (↑g i)).support) ↔
                                                    (fun ix => ↑(↑(b ix.fst).repr (↑g ix.fst)) ix.snd) ix ≠ 0) })
                                        (g + h) =
                                      (fun g =>
                                            { support := Finset.sigma g.support fun i => (↑(b i).repr (↑g i)).support,
                                              toFun := fun ix => ↑(↑(b ix.fst).repr (↑g ix.fst)) ix.snd,
                                              mem_support_toFun :=
                                                (_ :
                                                  ∀ (ix : (i : ι) × φ i),
                                                    (ix ∈
                                                        Finset.sigma g.support fun i => (↑(b i).repr (↑g i)).support) ↔
                                                      (fun ix => ↑(↑(b ix.fst).repr (↑g ix.fst)) ix.snd) ix ≠ 0) })
                                          g +
                                        (fun g =>
                                            { support := Finset.sigma g.support fun i => (↑(b i).repr (↑g i)).support,
                                              toFun := fun ix => ↑(↑(b ix.fst).repr (↑g ix.fst)) ix.snd,
                                              mem_support_toFun :=
                                                (_ :
                                                  ∀ (ix : (i : ι) × φ i),
                                                    (ix ∈
                                                        Finset.sigma g.support fun i => (↑(b i).repr (↑g i)).support) ↔
                                                      (fun ix => ↑(↑(b ix.fst).repr (↑g ix.fst)) ix.snd) ix ≠ 0) })
                                          h) }
                            (c • h) =
                          ↑(RingHom.id R) c •
                            AddHom.toFun
                              {
                                toFun := fun g =>
                                  { support := Finset.sigma g.support fun i => (↑(b i).repr (↑g i)).support,
                                    toFun := fun ix => ↑(↑(b ix.fst).repr (↑g ix.fst)) ix.snd,
                                    mem_support_toFun :=
                                      (_ :
                                        ∀ (ix : (i : ι) × φ i),
                                          (ix ∈ Finset.sigma g.support fun i => (↑(b i).repr (↑g i)).support) ↔
                                            (fun ix => ↑(↑(b ix.fst).repr (↑g ix.fst)) ix.snd) ix ≠ 0) },
                                map_add' :=
                                  (_ :
                                    ∀ (g h : ι →₀ M),
                                      (fun g =>
                                            { support := Finset.sigma g.support fun i => (↑(b i).repr (↑g i)).support,
                                              toFun := fun ix => ↑(↑(b ix.fst).repr (↑g ix.fst)) ix.snd,
                                              mem_support_toFun :=
                                                (_ :
                                                  ∀ (ix : (i : ι) × φ i),
                                                    (ix ∈
                                                        Finset.sigma g.support fun i => (↑(b i).repr (↑g i)).support) ↔
                                                      (fun ix => ↑(↑(b ix.fst).repr (↑g ix.fst)) ix.snd) ix ≠ 0) })
                                          (g + h) =
                                        (fun g =>
                                              { support := Finset.sigma g.support fun i => (↑(b i).repr (↑g i)).support,
                                                toFun := fun ix => ↑(↑(b ix.fst).repr (↑g ix.fst)) ix.snd,
                                                mem_support_toFun :=
                                                  (_ :
                                                    ∀ (ix : (i : ι) × φ i),
                                                      (ix ∈
                                                          Finset.sigma g.support fun i =>
                                                            (↑(b i).repr (↑g i)).support) ↔
                                                        (fun ix => ↑(↑(b ix.fst).repr (↑g ix.fst)) ix.snd) ix ≠ 0) })
                                            g +
                                          (fun g =>
                                              { support := Finset.sigma g.support fun i => (↑(b i).repr (↑g i)).support,
                                                toFun := fun ix => ↑(↑(b ix.fst).repr (↑g ix.fst)) ix.snd,
                                                mem_support_toFun :=
                                                  (_ :
                                                    ∀ (ix : (i : ι) × φ i),
                                                      (ix ∈
                                                          Finset.sigma g.support fun i =>
                                                            (↑(b i).repr (↑g i)).support) ↔
                                                        (fun ix => ↑(↑(b ix.fst).repr (↑g ix.fst)) ix.snd) ix ≠ 0) })
                                            h) }
                              h) }.toAddHom
              g))
        i) =
    ↑(b i).repr (↑g i)
[PROOFSTEP]
ext x
[GOAL]
case h.h
R : Type u_1
M : Type u_2
ι : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
φ : ι → Type u_4
b : (i : ι) → Basis (φ i) R M
g : ι →₀ M
i : ι
x : φ i
⊢ ↑(↑(b i).repr
          (↑((fun g =>
                  { support := Finset.image Sigma.fst g.support,
                    toFun := fun i =>
                      ↑(LinearEquiv.symm (b i).repr)
                        (comapDomain (Sigma.mk i) g (_ : InjOn (Sigma.mk i) (Sigma.mk i ⁻¹' ↑g.support))),
                    mem_support_toFun :=
                      (_ :
                        ∀ (i : ι),
                          i ∈ Finset.image Sigma.fst g.support ↔
                            (fun i =>
                                  ↑(LinearEquiv.symm (b i).repr)
                                    (comapDomain (Sigma.mk i) g (_ : InjOn (Sigma.mk i) (Sigma.mk i ⁻¹' ↑g.support))))
                                i ≠
                              0) })
                (AddHom.toFun
                  {
                      toAddHom :=
                        {
                          toFun := fun g =>
                            { support := Finset.sigma g.support fun i => (↑(b i).repr (↑g i)).support,
                              toFun := fun ix => ↑(↑(b ix.fst).repr (↑g ix.fst)) ix.snd,
                              mem_support_toFun :=
                                (_ :
                                  ∀ (ix : (i : ι) × φ i),
                                    (ix ∈ Finset.sigma g.support fun i => (↑(b i).repr (↑g i)).support) ↔
                                      (fun ix => ↑(↑(b ix.fst).repr (↑g ix.fst)) ix.snd) ix ≠ 0) },
                          map_add' :=
                            (_ :
                              ∀ (g h : ι →₀ M),
                                (fun g =>
                                      { support := Finset.sigma g.support fun i => (↑(b i).repr (↑g i)).support,
                                        toFun := fun ix => ↑(↑(b ix.fst).repr (↑g ix.fst)) ix.snd,
                                        mem_support_toFun :=
                                          (_ :
                                            ∀ (ix : (i : ι) × φ i),
                                              (ix ∈ Finset.sigma g.support fun i => (↑(b i).repr (↑g i)).support) ↔
                                                (fun ix => ↑(↑(b ix.fst).repr (↑g ix.fst)) ix.snd) ix ≠ 0) })
                                    (g + h) =
                                  (fun g =>
                                        { support := Finset.sigma g.support fun i => (↑(b i).repr (↑g i)).support,
                                          toFun := fun ix => ↑(↑(b ix.fst).repr (↑g ix.fst)) ix.snd,
                                          mem_support_toFun :=
                                            (_ :
                                              ∀ (ix : (i : ι) × φ i),
                                                (ix ∈ Finset.sigma g.support fun i => (↑(b i).repr (↑g i)).support) ↔
                                                  (fun ix => ↑(↑(b ix.fst).repr (↑g ix.fst)) ix.snd) ix ≠ 0) })
                                      g +
                                    (fun g =>
                                        { support := Finset.sigma g.support fun i => (↑(b i).repr (↑g i)).support,
                                          toFun := fun ix => ↑(↑(b ix.fst).repr (↑g ix.fst)) ix.snd,
                                          mem_support_toFun :=
                                            (_ :
                                              ∀ (ix : (i : ι) × φ i),
                                                (ix ∈ Finset.sigma g.support fun i => (↑(b i).repr (↑g i)).support) ↔
                                                  (fun ix => ↑(↑(b ix.fst).repr (↑g ix.fst)) ix.snd) ix ≠ 0) })
                                      h) },
                      map_smul' :=
                        (_ :
                          ∀ (c : R) (h : ι →₀ M),
                            AddHom.toFun
                                {
                                  toFun := fun g =>
                                    { support := Finset.sigma g.support fun i => (↑(b i).repr (↑g i)).support,
                                      toFun := fun ix => ↑(↑(b ix.fst).repr (↑g ix.fst)) ix.snd,
                                      mem_support_toFun :=
                                        (_ :
                                          ∀ (ix : (i : ι) × φ i),
                                            (ix ∈ Finset.sigma g.support fun i => (↑(b i).repr (↑g i)).support) ↔
                                              (fun ix => ↑(↑(b ix.fst).repr (↑g ix.fst)) ix.snd) ix ≠ 0) },
                                  map_add' :=
                                    (_ :
                                      ∀ (g h : ι →₀ M),
                                        (fun g =>
                                              { support := Finset.sigma g.support fun i => (↑(b i).repr (↑g i)).support,
                                                toFun := fun ix => ↑(↑(b ix.fst).repr (↑g ix.fst)) ix.snd,
                                                mem_support_toFun :=
                                                  (_ :
                                                    ∀ (ix : (i : ι) × φ i),
                                                      (ix ∈
                                                          Finset.sigma g.support fun i =>
                                                            (↑(b i).repr (↑g i)).support) ↔
                                                        (fun ix => ↑(↑(b ix.fst).repr (↑g ix.fst)) ix.snd) ix ≠ 0) })
                                            (g + h) =
                                          (fun g =>
                                                {
                                                  support :=
                                                    Finset.sigma g.support fun i => (↑(b i).repr (↑g i)).support,
                                                  toFun := fun ix => ↑(↑(b ix.fst).repr (↑g ix.fst)) ix.snd,
                                                  mem_support_toFun :=
                                                    (_ :
                                                      ∀ (ix : (i : ι) × φ i),
                                                        (ix ∈
                                                            Finset.sigma g.support fun i =>
                                                              (↑(b i).repr (↑g i)).support) ↔
                                                          (fun ix => ↑(↑(b ix.fst).repr (↑g ix.fst)) ix.snd) ix ≠ 0) })
                                              g +
                                            (fun g =>
                                                {
                                                  support :=
                                                    Finset.sigma g.support fun i => (↑(b i).repr (↑g i)).support,
                                                  toFun := fun ix => ↑(↑(b ix.fst).repr (↑g ix.fst)) ix.snd,
                                                  mem_support_toFun :=
                                                    (_ :
                                                      ∀ (ix : (i : ι) × φ i),
                                                        (ix ∈
                                                            Finset.sigma g.support fun i =>
                                                              (↑(b i).repr (↑g i)).support) ↔
                                                          (fun ix => ↑(↑(b ix.fst).repr (↑g ix.fst)) ix.snd) ix ≠ 0) })
                                              h) }
                                (c • h) =
                              ↑(RingHom.id R) c •
                                AddHom.toFun
                                  {
                                    toFun := fun g =>
                                      { support := Finset.sigma g.support fun i => (↑(b i).repr (↑g i)).support,
                                        toFun := fun ix => ↑(↑(b ix.fst).repr (↑g ix.fst)) ix.snd,
                                        mem_support_toFun :=
                                          (_ :
                                            ∀ (ix : (i : ι) × φ i),
                                              (ix ∈ Finset.sigma g.support fun i => (↑(b i).repr (↑g i)).support) ↔
                                                (fun ix => ↑(↑(b ix.fst).repr (↑g ix.fst)) ix.snd) ix ≠ 0) },
                                    map_add' :=
                                      (_ :
                                        ∀ (g h : ι →₀ M),
                                          (fun g =>
                                                {
                                                  support :=
                                                    Finset.sigma g.support fun i => (↑(b i).repr (↑g i)).support,
                                                  toFun := fun ix => ↑(↑(b ix.fst).repr (↑g ix.fst)) ix.snd,
                                                  mem_support_toFun :=
                                                    (_ :
                                                      ∀ (ix : (i : ι) × φ i),
                                                        (ix ∈
                                                            Finset.sigma g.support fun i =>
                                                              (↑(b i).repr (↑g i)).support) ↔
                                                          (fun ix => ↑(↑(b ix.fst).repr (↑g ix.fst)) ix.snd) ix ≠ 0) })
                                              (g + h) =
                                            (fun g =>
                                                  {
                                                    support :=
                                                      Finset.sigma g.support fun i => (↑(b i).repr (↑g i)).support,
                                                    toFun := fun ix => ↑(↑(b ix.fst).repr (↑g ix.fst)) ix.snd,
                                                    mem_support_toFun :=
                                                      (_ :
                                                        ∀ (ix : (i : ι) × φ i),
                                                          (ix ∈
                                                              Finset.sigma g.support fun i =>
                                                                (↑(b i).repr (↑g i)).support) ↔
                                                            (fun ix => ↑(↑(b ix.fst).repr (↑g ix.fst)) ix.snd) ix ≠
                                                              0) })
                                                g +
                                              (fun g =>
                                                  {
                                                    support :=
                                                      Finset.sigma g.support fun i => (↑(b i).repr (↑g i)).support,
                                                    toFun := fun ix => ↑(↑(b ix.fst).repr (↑g ix.fst)) ix.snd,
                                                    mem_support_toFun :=
                                                      (_ :
                                                        ∀ (ix : (i : ι) × φ i),
                                                          (ix ∈
                                                              Finset.sigma g.support fun i =>
                                                                (↑(b i).repr (↑g i)).support) ↔
                                                            (fun ix => ↑(↑(b ix.fst).repr (↑g ix.fst)) ix.snd) ix ≠
                                                              0) })
                                                h) }
                                  h) }.toAddHom
                  g))
            i))
      x =
    ↑(↑(b i).repr (↑g i)) x
[PROOFSTEP]
simp only [coe_mk, LinearEquiv.apply_symm_apply, comapDomain_apply]
[GOAL]
R : Type u_1
M : Type u_2
ι : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
φ : ι → Type u_4
b : (i : ι) → Basis (φ i) R M
g : (i : ι) × φ i →₀ R
⊢ AddHom.toFun
      {
          toAddHom :=
            {
              toFun := fun g =>
                { support := Finset.sigma g.support fun i => (↑(b i).repr (↑g i)).support,
                  toFun := fun ix => ↑(↑(b ix.fst).repr (↑g ix.fst)) ix.snd,
                  mem_support_toFun :=
                    (_ :
                      ∀ (ix : (i : ι) × φ i),
                        (ix ∈ Finset.sigma g.support fun i => (↑(b i).repr (↑g i)).support) ↔
                          (fun ix => ↑(↑(b ix.fst).repr (↑g ix.fst)) ix.snd) ix ≠ 0) },
              map_add' :=
                (_ :
                  ∀ (g h : ι →₀ M),
                    (fun g =>
                          { support := Finset.sigma g.support fun i => (↑(b i).repr (↑g i)).support,
                            toFun := fun ix => ↑(↑(b ix.fst).repr (↑g ix.fst)) ix.snd,
                            mem_support_toFun :=
                              (_ :
                                ∀ (ix : (i : ι) × φ i),
                                  (ix ∈ Finset.sigma g.support fun i => (↑(b i).repr (↑g i)).support) ↔
                                    (fun ix => ↑(↑(b ix.fst).repr (↑g ix.fst)) ix.snd) ix ≠ 0) })
                        (g + h) =
                      (fun g =>
                            { support := Finset.sigma g.support fun i => (↑(b i).repr (↑g i)).support,
                              toFun := fun ix => ↑(↑(b ix.fst).repr (↑g ix.fst)) ix.snd,
                              mem_support_toFun :=
                                (_ :
                                  ∀ (ix : (i : ι) × φ i),
                                    (ix ∈ Finset.sigma g.support fun i => (↑(b i).repr (↑g i)).support) ↔
                                      (fun ix => ↑(↑(b ix.fst).repr (↑g ix.fst)) ix.snd) ix ≠ 0) })
                          g +
                        (fun g =>
                            { support := Finset.sigma g.support fun i => (↑(b i).repr (↑g i)).support,
                              toFun := fun ix => ↑(↑(b ix.fst).repr (↑g ix.fst)) ix.snd,
                              mem_support_toFun :=
                                (_ :
                                  ∀ (ix : (i : ι) × φ i),
                                    (ix ∈ Finset.sigma g.support fun i => (↑(b i).repr (↑g i)).support) ↔
                                      (fun ix => ↑(↑(b ix.fst).repr (↑g ix.fst)) ix.snd) ix ≠ 0) })
                          h) },
          map_smul' :=
            (_ :
              ∀ (c : R) (h : ι →₀ M),
                AddHom.toFun
                    {
                      toFun := fun g =>
                        { support := Finset.sigma g.support fun i => (↑(b i).repr (↑g i)).support,
                          toFun := fun ix => ↑(↑(b ix.fst).repr (↑g ix.fst)) ix.snd,
                          mem_support_toFun :=
                            (_ :
                              ∀ (ix : (i : ι) × φ i),
                                (ix ∈ Finset.sigma g.support fun i => (↑(b i).repr (↑g i)).support) ↔
                                  (fun ix => ↑(↑(b ix.fst).repr (↑g ix.fst)) ix.snd) ix ≠ 0) },
                      map_add' :=
                        (_ :
                          ∀ (g h : ι →₀ M),
                            (fun g =>
                                  { support := Finset.sigma g.support fun i => (↑(b i).repr (↑g i)).support,
                                    toFun := fun ix => ↑(↑(b ix.fst).repr (↑g ix.fst)) ix.snd,
                                    mem_support_toFun :=
                                      (_ :
                                        ∀ (ix : (i : ι) × φ i),
                                          (ix ∈ Finset.sigma g.support fun i => (↑(b i).repr (↑g i)).support) ↔
                                            (fun ix => ↑(↑(b ix.fst).repr (↑g ix.fst)) ix.snd) ix ≠ 0) })
                                (g + h) =
                              (fun g =>
                                    { support := Finset.sigma g.support fun i => (↑(b i).repr (↑g i)).support,
                                      toFun := fun ix => ↑(↑(b ix.fst).repr (↑g ix.fst)) ix.snd,
                                      mem_support_toFun :=
                                        (_ :
                                          ∀ (ix : (i : ι) × φ i),
                                            (ix ∈ Finset.sigma g.support fun i => (↑(b i).repr (↑g i)).support) ↔
                                              (fun ix => ↑(↑(b ix.fst).repr (↑g ix.fst)) ix.snd) ix ≠ 0) })
                                  g +
                                (fun g =>
                                    { support := Finset.sigma g.support fun i => (↑(b i).repr (↑g i)).support,
                                      toFun := fun ix => ↑(↑(b ix.fst).repr (↑g ix.fst)) ix.snd,
                                      mem_support_toFun :=
                                        (_ :
                                          ∀ (ix : (i : ι) × φ i),
                                            (ix ∈ Finset.sigma g.support fun i => (↑(b i).repr (↑g i)).support) ↔
                                              (fun ix => ↑(↑(b ix.fst).repr (↑g ix.fst)) ix.snd) ix ≠ 0) })
                                  h) }
                    (c • h) =
                  ↑(RingHom.id R) c •
                    AddHom.toFun
                      {
                        toFun := fun g =>
                          { support := Finset.sigma g.support fun i => (↑(b i).repr (↑g i)).support,
                            toFun := fun ix => ↑(↑(b ix.fst).repr (↑g ix.fst)) ix.snd,
                            mem_support_toFun :=
                              (_ :
                                ∀ (ix : (i : ι) × φ i),
                                  (ix ∈ Finset.sigma g.support fun i => (↑(b i).repr (↑g i)).support) ↔
                                    (fun ix => ↑(↑(b ix.fst).repr (↑g ix.fst)) ix.snd) ix ≠ 0) },
                        map_add' :=
                          (_ :
                            ∀ (g h : ι →₀ M),
                              (fun g =>
                                    { support := Finset.sigma g.support fun i => (↑(b i).repr (↑g i)).support,
                                      toFun := fun ix => ↑(↑(b ix.fst).repr (↑g ix.fst)) ix.snd,
                                      mem_support_toFun :=
                                        (_ :
                                          ∀ (ix : (i : ι) × φ i),
                                            (ix ∈ Finset.sigma g.support fun i => (↑(b i).repr (↑g i)).support) ↔
                                              (fun ix => ↑(↑(b ix.fst).repr (↑g ix.fst)) ix.snd) ix ≠ 0) })
                                  (g + h) =
                                (fun g =>
                                      { support := Finset.sigma g.support fun i => (↑(b i).repr (↑g i)).support,
                                        toFun := fun ix => ↑(↑(b ix.fst).repr (↑g ix.fst)) ix.snd,
                                        mem_support_toFun :=
                                          (_ :
                                            ∀ (ix : (i : ι) × φ i),
                                              (ix ∈ Finset.sigma g.support fun i => (↑(b i).repr (↑g i)).support) ↔
                                                (fun ix => ↑(↑(b ix.fst).repr (↑g ix.fst)) ix.snd) ix ≠ 0) })
                                    g +
                                  (fun g =>
                                      { support := Finset.sigma g.support fun i => (↑(b i).repr (↑g i)).support,
                                        toFun := fun ix => ↑(↑(b ix.fst).repr (↑g ix.fst)) ix.snd,
                                        mem_support_toFun :=
                                          (_ :
                                            ∀ (ix : (i : ι) × φ i),
                                              (ix ∈ Finset.sigma g.support fun i => (↑(b i).repr (↑g i)).support) ↔
                                                (fun ix => ↑(↑(b ix.fst).repr (↑g ix.fst)) ix.snd) ix ≠ 0) })
                                    h) }
                      h) }.toAddHom
      ((fun g =>
          { support := Finset.image Sigma.fst g.support,
            toFun := fun i =>
              ↑(LinearEquiv.symm (b i).repr)
                (comapDomain (Sigma.mk i) g (_ : InjOn (Sigma.mk i) (Sigma.mk i ⁻¹' ↑g.support))),
            mem_support_toFun :=
              (_ :
                ∀ (i : ι),
                  i ∈ Finset.image Sigma.fst g.support ↔
                    (fun i =>
                          ↑(LinearEquiv.symm (b i).repr)
                            (comapDomain (Sigma.mk i) g (_ : InjOn (Sigma.mk i) (Sigma.mk i ⁻¹' ↑g.support))))
                        i ≠
                      0) })
        g) =
    g
[PROOFSTEP]
ext ⟨i, x⟩
[GOAL]
case h.mk
R : Type u_1
M : Type u_2
ι : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
φ : ι → Type u_4
b : (i : ι) → Basis (φ i) R M
g : (i : ι) × φ i →₀ R
i : ι
x : φ i
⊢ ↑(AddHom.toFun
          {
              toAddHom :=
                {
                  toFun := fun g =>
                    { support := Finset.sigma g.support fun i => (↑(b i).repr (↑g i)).support,
                      toFun := fun ix => ↑(↑(b ix.fst).repr (↑g ix.fst)) ix.snd,
                      mem_support_toFun :=
                        (_ :
                          ∀ (ix : (i : ι) × φ i),
                            (ix ∈ Finset.sigma g.support fun i => (↑(b i).repr (↑g i)).support) ↔
                              (fun ix => ↑(↑(b ix.fst).repr (↑g ix.fst)) ix.snd) ix ≠ 0) },
                  map_add' :=
                    (_ :
                      ∀ (g h : ι →₀ M),
                        (fun g =>
                              { support := Finset.sigma g.support fun i => (↑(b i).repr (↑g i)).support,
                                toFun := fun ix => ↑(↑(b ix.fst).repr (↑g ix.fst)) ix.snd,
                                mem_support_toFun :=
                                  (_ :
                                    ∀ (ix : (i : ι) × φ i),
                                      (ix ∈ Finset.sigma g.support fun i => (↑(b i).repr (↑g i)).support) ↔
                                        (fun ix => ↑(↑(b ix.fst).repr (↑g ix.fst)) ix.snd) ix ≠ 0) })
                            (g + h) =
                          (fun g =>
                                { support := Finset.sigma g.support fun i => (↑(b i).repr (↑g i)).support,
                                  toFun := fun ix => ↑(↑(b ix.fst).repr (↑g ix.fst)) ix.snd,
                                  mem_support_toFun :=
                                    (_ :
                                      ∀ (ix : (i : ι) × φ i),
                                        (ix ∈ Finset.sigma g.support fun i => (↑(b i).repr (↑g i)).support) ↔
                                          (fun ix => ↑(↑(b ix.fst).repr (↑g ix.fst)) ix.snd) ix ≠ 0) })
                              g +
                            (fun g =>
                                { support := Finset.sigma g.support fun i => (↑(b i).repr (↑g i)).support,
                                  toFun := fun ix => ↑(↑(b ix.fst).repr (↑g ix.fst)) ix.snd,
                                  mem_support_toFun :=
                                    (_ :
                                      ∀ (ix : (i : ι) × φ i),
                                        (ix ∈ Finset.sigma g.support fun i => (↑(b i).repr (↑g i)).support) ↔
                                          (fun ix => ↑(↑(b ix.fst).repr (↑g ix.fst)) ix.snd) ix ≠ 0) })
                              h) },
              map_smul' :=
                (_ :
                  ∀ (c : R) (h : ι →₀ M),
                    AddHom.toFun
                        {
                          toFun := fun g =>
                            { support := Finset.sigma g.support fun i => (↑(b i).repr (↑g i)).support,
                              toFun := fun ix => ↑(↑(b ix.fst).repr (↑g ix.fst)) ix.snd,
                              mem_support_toFun :=
                                (_ :
                                  ∀ (ix : (i : ι) × φ i),
                                    (ix ∈ Finset.sigma g.support fun i => (↑(b i).repr (↑g i)).support) ↔
                                      (fun ix => ↑(↑(b ix.fst).repr (↑g ix.fst)) ix.snd) ix ≠ 0) },
                          map_add' :=
                            (_ :
                              ∀ (g h : ι →₀ M),
                                (fun g =>
                                      { support := Finset.sigma g.support fun i => (↑(b i).repr (↑g i)).support,
                                        toFun := fun ix => ↑(↑(b ix.fst).repr (↑g ix.fst)) ix.snd,
                                        mem_support_toFun :=
                                          (_ :
                                            ∀ (ix : (i : ι) × φ i),
                                              (ix ∈ Finset.sigma g.support fun i => (↑(b i).repr (↑g i)).support) ↔
                                                (fun ix => ↑(↑(b ix.fst).repr (↑g ix.fst)) ix.snd) ix ≠ 0) })
                                    (g + h) =
                                  (fun g =>
                                        { support := Finset.sigma g.support fun i => (↑(b i).repr (↑g i)).support,
                                          toFun := fun ix => ↑(↑(b ix.fst).repr (↑g ix.fst)) ix.snd,
                                          mem_support_toFun :=
                                            (_ :
                                              ∀ (ix : (i : ι) × φ i),
                                                (ix ∈ Finset.sigma g.support fun i => (↑(b i).repr (↑g i)).support) ↔
                                                  (fun ix => ↑(↑(b ix.fst).repr (↑g ix.fst)) ix.snd) ix ≠ 0) })
                                      g +
                                    (fun g =>
                                        { support := Finset.sigma g.support fun i => (↑(b i).repr (↑g i)).support,
                                          toFun := fun ix => ↑(↑(b ix.fst).repr (↑g ix.fst)) ix.snd,
                                          mem_support_toFun :=
                                            (_ :
                                              ∀ (ix : (i : ι) × φ i),
                                                (ix ∈ Finset.sigma g.support fun i => (↑(b i).repr (↑g i)).support) ↔
                                                  (fun ix => ↑(↑(b ix.fst).repr (↑g ix.fst)) ix.snd) ix ≠ 0) })
                                      h) }
                        (c • h) =
                      ↑(RingHom.id R) c •
                        AddHom.toFun
                          {
                            toFun := fun g =>
                              { support := Finset.sigma g.support fun i => (↑(b i).repr (↑g i)).support,
                                toFun := fun ix => ↑(↑(b ix.fst).repr (↑g ix.fst)) ix.snd,
                                mem_support_toFun :=
                                  (_ :
                                    ∀ (ix : (i : ι) × φ i),
                                      (ix ∈ Finset.sigma g.support fun i => (↑(b i).repr (↑g i)).support) ↔
                                        (fun ix => ↑(↑(b ix.fst).repr (↑g ix.fst)) ix.snd) ix ≠ 0) },
                            map_add' :=
                              (_ :
                                ∀ (g h : ι →₀ M),
                                  (fun g =>
                                        { support := Finset.sigma g.support fun i => (↑(b i).repr (↑g i)).support,
                                          toFun := fun ix => ↑(↑(b ix.fst).repr (↑g ix.fst)) ix.snd,
                                          mem_support_toFun :=
                                            (_ :
                                              ∀ (ix : (i : ι) × φ i),
                                                (ix ∈ Finset.sigma g.support fun i => (↑(b i).repr (↑g i)).support) ↔
                                                  (fun ix => ↑(↑(b ix.fst).repr (↑g ix.fst)) ix.snd) ix ≠ 0) })
                                      (g + h) =
                                    (fun g =>
                                          { support := Finset.sigma g.support fun i => (↑(b i).repr (↑g i)).support,
                                            toFun := fun ix => ↑(↑(b ix.fst).repr (↑g ix.fst)) ix.snd,
                                            mem_support_toFun :=
                                              (_ :
                                                ∀ (ix : (i : ι) × φ i),
                                                  (ix ∈ Finset.sigma g.support fun i => (↑(b i).repr (↑g i)).support) ↔
                                                    (fun ix => ↑(↑(b ix.fst).repr (↑g ix.fst)) ix.snd) ix ≠ 0) })
                                        g +
                                      (fun g =>
                                          { support := Finset.sigma g.support fun i => (↑(b i).repr (↑g i)).support,
                                            toFun := fun ix => ↑(↑(b ix.fst).repr (↑g ix.fst)) ix.snd,
                                            mem_support_toFun :=
                                              (_ :
                                                ∀ (ix : (i : ι) × φ i),
                                                  (ix ∈ Finset.sigma g.support fun i => (↑(b i).repr (↑g i)).support) ↔
                                                    (fun ix => ↑(↑(b ix.fst).repr (↑g ix.fst)) ix.snd) ix ≠ 0) })
                                        h) }
                          h) }.toAddHom
          ((fun g =>
              { support := Finset.image Sigma.fst g.support,
                toFun := fun i =>
                  ↑(LinearEquiv.symm (b i).repr)
                    (comapDomain (Sigma.mk i) g (_ : InjOn (Sigma.mk i) (Sigma.mk i ⁻¹' ↑g.support))),
                mem_support_toFun :=
                  (_ :
                    ∀ (i : ι),
                      i ∈ Finset.image Sigma.fst g.support ↔
                        (fun i =>
                              ↑(LinearEquiv.symm (b i).repr)
                                (comapDomain (Sigma.mk i) g (_ : InjOn (Sigma.mk i) (Sigma.mk i ⁻¹' ↑g.support))))
                            i ≠
                          0) })
            g))
      { fst := i, snd := x } =
    ↑g { fst := i, snd := x }
[PROOFSTEP]
simp only [coe_mk, LinearEquiv.apply_symm_apply, comapDomain_apply]
[GOAL]
R : Type u_1
M : Type u_2
ι : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
φ : ι → Type u_4
b : (i : ι) → Basis (φ i) R M
x✝ : (i : ι) × φ i
i : ι
x : φ i
⊢ ↑(Finsupp.basis b).repr
      (single { fst := i, snd := x }.fst (↑(b { fst := i, snd := x }.fst) { fst := i, snd := x }.snd)) =
    single { fst := i, snd := x } 1
[PROOFSTEP]
classical
ext ⟨j, y⟩
by_cases h : i = j
· cases h
  simp only [basis_repr, single_eq_same, Basis.repr_self, Finsupp.single_apply_left sigma_mk_injective]
· have : Sigma.mk i x ≠ Sigma.mk j y := fun h' => h <| congrArg (fun s => s.fst) h'
  simp only [basis_repr, single_apply, h, this, false_and_iff, if_false, LinearEquiv.map_zero, zero_apply]
[GOAL]
R : Type u_1
M : Type u_2
ι : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
φ : ι → Type u_4
b : (i : ι) → Basis (φ i) R M
x✝ : (i : ι) × φ i
i : ι
x : φ i
⊢ ↑(Finsupp.basis b).repr
      (single { fst := i, snd := x }.fst (↑(b { fst := i, snd := x }.fst) { fst := i, snd := x }.snd)) =
    single { fst := i, snd := x } 1
[PROOFSTEP]
ext ⟨j, y⟩
[GOAL]
case h.mk
R : Type u_1
M : Type u_2
ι : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
φ : ι → Type u_4
b : (i : ι) → Basis (φ i) R M
x✝ : (i : ι) × φ i
i : ι
x : φ i
j : ι
y : φ j
⊢ ↑(↑(Finsupp.basis b).repr
          (single { fst := i, snd := x }.fst (↑(b { fst := i, snd := x }.fst) { fst := i, snd := x }.snd)))
      { fst := j, snd := y } =
    ↑(single { fst := i, snd := x } 1) { fst := j, snd := y }
[PROOFSTEP]
by_cases h : i = j
[GOAL]
case pos
R : Type u_1
M : Type u_2
ι : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
φ : ι → Type u_4
b : (i : ι) → Basis (φ i) R M
x✝ : (i : ι) × φ i
i : ι
x : φ i
j : ι
y : φ j
h : i = j
⊢ ↑(↑(Finsupp.basis b).repr
          (single { fst := i, snd := x }.fst (↑(b { fst := i, snd := x }.fst) { fst := i, snd := x }.snd)))
      { fst := j, snd := y } =
    ↑(single { fst := i, snd := x } 1) { fst := j, snd := y }
[PROOFSTEP]
cases h
[GOAL]
case pos.refl
R : Type u_1
M : Type u_2
ι : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
φ : ι → Type u_4
b : (i : ι) → Basis (φ i) R M
x✝ : (i : ι) × φ i
i : ι
x y : φ i
⊢ ↑(↑(Finsupp.basis b).repr
          (single { fst := i, snd := x }.fst (↑(b { fst := i, snd := x }.fst) { fst := i, snd := x }.snd)))
      { fst := i, snd := y } =
    ↑(single { fst := i, snd := x } 1) { fst := i, snd := y }
[PROOFSTEP]
simp only [basis_repr, single_eq_same, Basis.repr_self, Finsupp.single_apply_left sigma_mk_injective]
[GOAL]
case neg
R : Type u_1
M : Type u_2
ι : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
φ : ι → Type u_4
b : (i : ι) → Basis (φ i) R M
x✝ : (i : ι) × φ i
i : ι
x : φ i
j : ι
y : φ j
h : ¬i = j
⊢ ↑(↑(Finsupp.basis b).repr
          (single { fst := i, snd := x }.fst (↑(b { fst := i, snd := x }.fst) { fst := i, snd := x }.snd)))
      { fst := j, snd := y } =
    ↑(single { fst := i, snd := x } 1) { fst := j, snd := y }
[PROOFSTEP]
have : Sigma.mk i x ≠ Sigma.mk j y := fun h' => h <| congrArg (fun s => s.fst) h'
[GOAL]
case neg
R : Type u_1
M : Type u_2
ι : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
φ : ι → Type u_4
b : (i : ι) → Basis (φ i) R M
x✝ : (i : ι) × φ i
i : ι
x : φ i
j : ι
y : φ j
h : ¬i = j
this : { fst := i, snd := x } ≠ { fst := j, snd := y }
⊢ ↑(↑(Finsupp.basis b).repr
          (single { fst := i, snd := x }.fst (↑(b { fst := i, snd := x }.fst) { fst := i, snd := x }.snd)))
      { fst := j, snd := y } =
    ↑(single { fst := i, snd := x } 1) { fst := j, snd := y }
[PROOFSTEP]
simp only [basis_repr, single_apply, h, this, false_and_iff, if_false, LinearEquiv.map_zero, zero_apply]
[GOAL]
R : Type u_1
M : Type u_2
n : Type u_3
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
a : R
i : n
⊢ (Finset.sum Finset.univ fun x => Finsupp.single x (if i = x then a else 0)) = Finsupp.single i a
[PROOFSTEP]
rw [Finset.sum_congr_set { i } (fun x : n => Finsupp.single x (ite (i = x) a 0)) fun _ => Finsupp.single i a]
[GOAL]
R : Type u_1
M : Type u_2
n : Type u_3
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
a : R
i : n
⊢ (Finset.sum Finset.univ fun x => Finsupp.single i a) = Finsupp.single i a
[PROOFSTEP]
simp
[GOAL]
case w
R : Type u_1
M : Type u_2
n : Type u_3
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
a : R
i : n
⊢ ∀ (x : n), x ∈ {i} → Finsupp.single x (if i = x then a else 0) = Finsupp.single i a
[PROOFSTEP]
intro x hx
[GOAL]
case w
R : Type u_1
M : Type u_2
n : Type u_3
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
a : R
i x : n
hx : x ∈ {i}
⊢ Finsupp.single x (if i = x then a else 0) = Finsupp.single i a
[PROOFSTEP]
rw [Set.mem_singleton_iff] at hx 
[GOAL]
case w
R : Type u_1
M : Type u_2
n : Type u_3
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
a : R
i x : n
hx : x = i
⊢ Finsupp.single x (if i = x then a else 0) = Finsupp.single i a
[PROOFSTEP]
simp [hx]
[GOAL]
case w'
R : Type u_1
M : Type u_2
n : Type u_3
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
a : R
i : n
⊢ ∀ (x : n), ¬x ∈ {i} → Finsupp.single x (if i = x then a else 0) = 0
[PROOFSTEP]
intro x hx
[GOAL]
case w'
R : Type u_1
M : Type u_2
n : Type u_3
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
a : R
i x : n
hx : ¬x ∈ {i}
⊢ Finsupp.single x (if i = x then a else 0) = 0
[PROOFSTEP]
have hx' : ¬i = x := by
  refine' ne_comm.mp _
  rwa [mem_singleton_iff] at hx 
[GOAL]
R : Type u_1
M : Type u_2
n : Type u_3
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
a : R
i x : n
hx : ¬x ∈ {i}
⊢ ¬i = x
[PROOFSTEP]
refine' ne_comm.mp _
[GOAL]
R : Type u_1
M : Type u_2
n : Type u_3
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
a : R
i x : n
hx : ¬x ∈ {i}
⊢ x ≠ i
[PROOFSTEP]
rwa [mem_singleton_iff] at hx 
[GOAL]
case w'
R : Type u_1
M : Type u_2
n : Type u_3
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
a : R
i x : n
hx : ¬x ∈ {i}
hx' : ¬i = x
⊢ Finsupp.single x (if i = x then a else 0) = 0
[PROOFSTEP]
simp [hx']
[GOAL]
R : Type u_1
M : Type u_2
n : Type u_3
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : n → M
i : n
⊢ (Finset.sum Finset.univ fun x => (if i = x then 1 else 0) • b x) = b i
[PROOFSTEP]
simp only [ite_smul, zero_smul, one_smul, Finset.sum_ite_eq, Finset.mem_univ, ite_true]
[GOAL]
R : Type u_1
M : Type u_2
n : Type u_3
inst✝⁴ : DecidableEq n
inst✝³ : Fintype n
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : Basis n R M
i : n
⊢ ↑(LinearEquiv.symm (equivFun b)) (↑(stdBasis R (fun x => R) i) 1) = ↑b i
[PROOFSTEP]
simp
