[GOAL]
k : Type u_1
V₁ : Type u_2
P₁ : Type u_3
V₂ : Type u_4
P₂ : Type u_5
inst✝⁶ : Ring k
inst✝⁵ : AddCommGroup V₁
inst✝⁴ : AddCommGroup V₂
inst✝³ : Module k V₁
inst✝² : Module k V₂
inst✝¹ : AddTorsor V₁ P₁
inst✝ : AddTorsor V₂ P₂
E : AffineSubspace k P₁
Ene : Nonempty { x // x ∈ E }
φ : P₁ →ᵃ[k] P₂
⊢ Nonempty { x // x ∈ map φ E }
[PROOFSTEP]
obtain ⟨x, hx⟩ := id Ene
[GOAL]
case intro.mk
k : Type u_1
V₁ : Type u_2
P₁ : Type u_3
V₂ : Type u_4
P₂ : Type u_5
inst✝⁶ : Ring k
inst✝⁵ : AddCommGroup V₁
inst✝⁴ : AddCommGroup V₂
inst✝³ : Module k V₁
inst✝² : Module k V₂
inst✝¹ : AddTorsor V₁ P₁
inst✝ : AddTorsor V₂ P₂
E : AffineSubspace k P₁
Ene : Nonempty { x // x ∈ E }
φ : P₁ →ᵃ[k] P₂
x : P₁
hx : x ∈ E
⊢ Nonempty { x // x ∈ map φ E }
[PROOFSTEP]
refine' ⟨⟨φ x, AffineSubspace.mem_map.mpr ⟨x, hx, rfl⟩⟩⟩
[GOAL]
k : Type u_1
V₁ : Type u_2
P₁ : Type u_3
V₂ : Type u_4
P₂ : Type u_5
inst✝⁸ : Ring k
inst✝⁷ : AddCommGroup V₁
inst✝⁶ : AddCommGroup V₂
inst✝⁵ : Module k V₁
inst✝⁴ : Module k V₂
inst✝³ : AddTorsor V₁ P₁
inst✝² : AddTorsor V₂ P₂
φ : P₁ →ᵃ[k] P₂
E : AffineSubspace k P₁
F : AffineSubspace k P₂
inst✝¹ : Nonempty { x // x ∈ E }
inst✝ : Nonempty { x // x ∈ F }
hEF : AffineSubspace.map φ E ≤ F
⊢ { x // x ∈ E } →ᵃ[k] { x // x ∈ F }
[PROOFSTEP]
refine' ⟨_, _, _⟩
[GOAL]
case refine'_1
k : Type u_1
V₁ : Type u_2
P₁ : Type u_3
V₂ : Type u_4
P₂ : Type u_5
inst✝⁸ : Ring k
inst✝⁷ : AddCommGroup V₁
inst✝⁶ : AddCommGroup V₂
inst✝⁵ : Module k V₁
inst✝⁴ : Module k V₂
inst✝³ : AddTorsor V₁ P₁
inst✝² : AddTorsor V₂ P₂
φ : P₁ →ᵃ[k] P₂
E : AffineSubspace k P₁
F : AffineSubspace k P₂
inst✝¹ : Nonempty { x // x ∈ E }
inst✝ : Nonempty { x // x ∈ F }
hEF : AffineSubspace.map φ E ≤ F
⊢ { x // x ∈ E } → { x // x ∈ F }
[PROOFSTEP]
exact fun x => ⟨φ x, hEF <| AffineSubspace.mem_map.mpr ⟨x, x.property, rfl⟩⟩
[GOAL]
case refine'_2
k : Type u_1
V₁ : Type u_2
P₁ : Type u_3
V₂ : Type u_4
P₂ : Type u_5
inst✝⁸ : Ring k
inst✝⁷ : AddCommGroup V₁
inst✝⁶ : AddCommGroup V₂
inst✝⁵ : Module k V₁
inst✝⁴ : Module k V₂
inst✝³ : AddTorsor V₁ P₁
inst✝² : AddTorsor V₂ P₂
φ : P₁ →ᵃ[k] P₂
E : AffineSubspace k P₁
F : AffineSubspace k P₂
inst✝¹ : Nonempty { x // x ∈ E }
inst✝ : Nonempty { x // x ∈ F }
hEF : AffineSubspace.map φ E ≤ F
⊢ { x // x ∈ AffineSubspace.direction E } →ₗ[k] { x // x ∈ AffineSubspace.direction F }
[PROOFSTEP]
refine' φ.linear.restrict (_ : E.direction ≤ F.direction.comap φ.linear)
[GOAL]
case refine'_2
k : Type u_1
V₁ : Type u_2
P₁ : Type u_3
V₂ : Type u_4
P₂ : Type u_5
inst✝⁸ : Ring k
inst✝⁷ : AddCommGroup V₁
inst✝⁶ : AddCommGroup V₂
inst✝⁵ : Module k V₁
inst✝⁴ : Module k V₂
inst✝³ : AddTorsor V₁ P₁
inst✝² : AddTorsor V₂ P₂
φ : P₁ →ᵃ[k] P₂
E : AffineSubspace k P₁
F : AffineSubspace k P₂
inst✝¹ : Nonempty { x // x ∈ E }
inst✝ : Nonempty { x // x ∈ F }
hEF : AffineSubspace.map φ E ≤ F
⊢ AffineSubspace.direction E ≤ Submodule.comap φ.linear (AffineSubspace.direction F)
[PROOFSTEP]
rw [← Submodule.map_le_iff_le_comap, ← AffineSubspace.map_direction]
[GOAL]
case refine'_2
k : Type u_1
V₁ : Type u_2
P₁ : Type u_3
V₂ : Type u_4
P₂ : Type u_5
inst✝⁸ : Ring k
inst✝⁷ : AddCommGroup V₁
inst✝⁶ : AddCommGroup V₂
inst✝⁵ : Module k V₁
inst✝⁴ : Module k V₂
inst✝³ : AddTorsor V₁ P₁
inst✝² : AddTorsor V₂ P₂
φ : P₁ →ᵃ[k] P₂
E : AffineSubspace k P₁
F : AffineSubspace k P₂
inst✝¹ : Nonempty { x // x ∈ E }
inst✝ : Nonempty { x // x ∈ F }
hEF : AffineSubspace.map φ E ≤ F
⊢ AffineSubspace.direction (AffineSubspace.map φ E) ≤ AffineSubspace.direction F
[PROOFSTEP]
exact AffineSubspace.direction_le hEF
[GOAL]
case refine'_3
k : Type u_1
V₁ : Type u_2
P₁ : Type u_3
V₂ : Type u_4
P₂ : Type u_5
inst✝⁸ : Ring k
inst✝⁷ : AddCommGroup V₁
inst✝⁶ : AddCommGroup V₂
inst✝⁵ : Module k V₁
inst✝⁴ : Module k V₂
inst✝³ : AddTorsor V₁ P₁
inst✝² : AddTorsor V₂ P₂
φ : P₁ →ᵃ[k] P₂
E : AffineSubspace k P₁
F : AffineSubspace k P₂
inst✝¹ : Nonempty { x // x ∈ E }
inst✝ : Nonempty { x // x ∈ F }
hEF : AffineSubspace.map φ E ≤ F
⊢ ∀ (p : { x // x ∈ E }) (v : { x // x ∈ AffineSubspace.direction E }),
    { val := ↑φ ↑(v +ᵥ p), property := (_ : ↑φ ↑(v +ᵥ p) ∈ ↑F) } =
      ↑(LinearMap.restrict φ.linear
              (_ : AffineSubspace.direction E ≤ Submodule.comap φ.linear (AffineSubspace.direction F)))
          v +ᵥ
        { val := ↑φ ↑p, property := (_ : ↑φ ↑p ∈ ↑F) }
[PROOFSTEP]
intro p v
[GOAL]
case refine'_3
k : Type u_1
V₁ : Type u_2
P₁ : Type u_3
V₂ : Type u_4
P₂ : Type u_5
inst✝⁸ : Ring k
inst✝⁷ : AddCommGroup V₁
inst✝⁶ : AddCommGroup V₂
inst✝⁵ : Module k V₁
inst✝⁴ : Module k V₂
inst✝³ : AddTorsor V₁ P₁
inst✝² : AddTorsor V₂ P₂
φ : P₁ →ᵃ[k] P₂
E : AffineSubspace k P₁
F : AffineSubspace k P₂
inst✝¹ : Nonempty { x // x ∈ E }
inst✝ : Nonempty { x // x ∈ F }
hEF : AffineSubspace.map φ E ≤ F
p : { x // x ∈ E }
v : { x // x ∈ AffineSubspace.direction E }
⊢ { val := ↑φ ↑(v +ᵥ p), property := (_ : ↑φ ↑(v +ᵥ p) ∈ ↑F) } =
    ↑(LinearMap.restrict φ.linear
            (_ : AffineSubspace.direction E ≤ Submodule.comap φ.linear (AffineSubspace.direction F)))
        v +ᵥ
      { val := ↑φ ↑p, property := (_ : ↑φ ↑p ∈ ↑F) }
[PROOFSTEP]
simp only [Subtype.ext_iff, Subtype.coe_mk, AffineSubspace.coe_vadd]
[GOAL]
case refine'_3
k : Type u_1
V₁ : Type u_2
P₁ : Type u_3
V₂ : Type u_4
P₂ : Type u_5
inst✝⁸ : Ring k
inst✝⁷ : AddCommGroup V₁
inst✝⁶ : AddCommGroup V₂
inst✝⁵ : Module k V₁
inst✝⁴ : Module k V₂
inst✝³ : AddTorsor V₁ P₁
inst✝² : AddTorsor V₂ P₂
φ : P₁ →ᵃ[k] P₂
E : AffineSubspace k P₁
F : AffineSubspace k P₂
inst✝¹ : Nonempty { x // x ∈ E }
inst✝ : Nonempty { x // x ∈ F }
hEF : AffineSubspace.map φ E ≤ F
p : { x // x ∈ E }
v : { x // x ∈ AffineSubspace.direction E }
⊢ ↑φ (↑v +ᵥ ↑p) =
    ↑(↑(LinearMap.restrict φ.linear
              (_ : AffineSubspace.direction E ≤ Submodule.comap φ.linear (AffineSubspace.direction F)))
          v) +ᵥ
      ↑φ ↑p
[PROOFSTEP]
apply AffineMap.map_vadd
[GOAL]
k : Type u_1
V₁ : Type u_2
P₁ : Type u_3
V₂ : Type u_4
P₂ : Type u_5
inst✝⁶ : Ring k
inst✝⁵ : AddCommGroup V₁
inst✝⁴ : AddCommGroup V₂
inst✝³ : Module k V₁
inst✝² : Module k V₂
inst✝¹ : AddTorsor V₁ P₁
inst✝ : AddTorsor V₂ P₂
φ : P₁ →ᵃ[k] P₂
E : AffineSubspace k P₁
F : AffineSubspace k P₂
hEF : AffineSubspace.map φ E ≤ F
⊢ AffineSubspace.direction E ≤ Submodule.comap φ.linear (AffineSubspace.direction F)
[PROOFSTEP]
rw [← Submodule.map_le_iff_le_comap, ← AffineSubspace.map_direction]
[GOAL]
k : Type u_1
V₁ : Type u_2
P₁ : Type u_3
V₂ : Type u_4
P₂ : Type u_5
inst✝⁶ : Ring k
inst✝⁵ : AddCommGroup V₁
inst✝⁴ : AddCommGroup V₂
inst✝³ : Module k V₁
inst✝² : Module k V₂
inst✝¹ : AddTorsor V₁ P₁
inst✝ : AddTorsor V₂ P₂
φ : P₁ →ᵃ[k] P₂
E : AffineSubspace k P₁
F : AffineSubspace k P₂
hEF : AffineSubspace.map φ E ≤ F
⊢ AffineSubspace.direction (AffineSubspace.map φ E) ≤ AffineSubspace.direction F
[PROOFSTEP]
exact AffineSubspace.direction_le hEF
[GOAL]
k : Type u_1
V₁ : Type u_2
P₁ : Type u_3
V₂ : Type u_4
P₂ : Type u_5
inst✝⁸ : Ring k
inst✝⁷ : AddCommGroup V₁
inst✝⁶ : AddCommGroup V₂
inst✝⁵ : Module k V₁
inst✝⁴ : Module k V₂
inst✝³ : AddTorsor V₁ P₁
inst✝² : AddTorsor V₂ P₂
φ : P₁ →ᵃ[k] P₂
hφ : Function.Injective ↑φ
E : AffineSubspace k P₁
F : AffineSubspace k P₂
inst✝¹ : Nonempty { x // x ∈ E }
inst✝ : Nonempty { x // x ∈ F }
hEF : AffineSubspace.map φ E ≤ F
⊢ Function.Injective ↑(restrict φ hEF)
[PROOFSTEP]
intro x y h
[GOAL]
k : Type u_1
V₁ : Type u_2
P₁ : Type u_3
V₂ : Type u_4
P₂ : Type u_5
inst✝⁸ : Ring k
inst✝⁷ : AddCommGroup V₁
inst✝⁶ : AddCommGroup V₂
inst✝⁵ : Module k V₁
inst✝⁴ : Module k V₂
inst✝³ : AddTorsor V₁ P₁
inst✝² : AddTorsor V₂ P₂
φ : P₁ →ᵃ[k] P₂
hφ : Function.Injective ↑φ
E : AffineSubspace k P₁
F : AffineSubspace k P₂
inst✝¹ : Nonempty { x // x ∈ E }
inst✝ : Nonempty { x // x ∈ F }
hEF : AffineSubspace.map φ E ≤ F
x y : { x // x ∈ E }
h : ↑(restrict φ hEF) x = ↑(restrict φ hEF) y
⊢ x = y
[PROOFSTEP]
simp only [Subtype.ext_iff, Subtype.coe_mk, AffineMap.restrict.coe_apply] at h ⊢
[GOAL]
k : Type u_1
V₁ : Type u_2
P₁ : Type u_3
V₂ : Type u_4
P₂ : Type u_5
inst✝⁸ : Ring k
inst✝⁷ : AddCommGroup V₁
inst✝⁶ : AddCommGroup V₂
inst✝⁵ : Module k V₁
inst✝⁴ : Module k V₂
inst✝³ : AddTorsor V₁ P₁
inst✝² : AddTorsor V₂ P₂
φ : P₁ →ᵃ[k] P₂
hφ : Function.Injective ↑φ
E : AffineSubspace k P₁
F : AffineSubspace k P₂
inst✝¹ : Nonempty { x // x ∈ E }
inst✝ : Nonempty { x // x ∈ F }
hEF : AffineSubspace.map φ E ≤ F
x y : { x // x ∈ E }
h : ↑φ ↑x = ↑φ ↑y
⊢ ↑x = ↑y
[PROOFSTEP]
exact hφ h
[GOAL]
k : Type u_1
V₁ : Type u_2
P₁ : Type u_3
V₂ : Type u_4
P₂ : Type u_5
inst✝⁸ : Ring k
inst✝⁷ : AddCommGroup V₁
inst✝⁶ : AddCommGroup V₂
inst✝⁵ : Module k V₁
inst✝⁴ : Module k V₂
inst✝³ : AddTorsor V₁ P₁
inst✝² : AddTorsor V₂ P₂
φ : P₁ →ᵃ[k] P₂
E : AffineSubspace k P₁
F : AffineSubspace k P₂
inst✝¹ : Nonempty { x // x ∈ E }
inst✝ : Nonempty { x // x ∈ F }
h : AffineSubspace.map φ E = F
⊢ Function.Surjective ↑(restrict φ (_ : AffineSubspace.map φ E ≤ F))
[PROOFSTEP]
rintro ⟨x, hx : x ∈ F⟩
[GOAL]
case mk
k : Type u_1
V₁ : Type u_2
P₁ : Type u_3
V₂ : Type u_4
P₂ : Type u_5
inst✝⁸ : Ring k
inst✝⁷ : AddCommGroup V₁
inst✝⁶ : AddCommGroup V₂
inst✝⁵ : Module k V₁
inst✝⁴ : Module k V₂
inst✝³ : AddTorsor V₁ P₁
inst✝² : AddTorsor V₂ P₂
φ : P₁ →ᵃ[k] P₂
E : AffineSubspace k P₁
F : AffineSubspace k P₂
inst✝¹ : Nonempty { x // x ∈ E }
inst✝ : Nonempty { x // x ∈ F }
h : AffineSubspace.map φ E = F
x : P₂
hx : x ∈ F
⊢ ∃ a, ↑(restrict φ (_ : AffineSubspace.map φ E ≤ F)) a = { val := x, property := hx }
[PROOFSTEP]
rw [← h, AffineSubspace.mem_map] at hx
[GOAL]
case mk
k : Type u_1
V₁ : Type u_2
P₁ : Type u_3
V₂ : Type u_4
P₂ : Type u_5
inst✝⁸ : Ring k
inst✝⁷ : AddCommGroup V₁
inst✝⁶ : AddCommGroup V₂
inst✝⁵ : Module k V₁
inst✝⁴ : Module k V₂
inst✝³ : AddTorsor V₁ P₁
inst✝² : AddTorsor V₂ P₂
φ : P₁ →ᵃ[k] P₂
E : AffineSubspace k P₁
F : AffineSubspace k P₂
inst✝¹ : Nonempty { x // x ∈ E }
inst✝ : Nonempty { x // x ∈ F }
h : AffineSubspace.map φ E = F
x : P₂
hx✝ : x ∈ F
hx : ∃ y, y ∈ E ∧ ↑φ y = x
⊢ ∃ a, ↑(restrict φ (_ : AffineSubspace.map φ E ≤ F)) a = { val := x, property := hx✝ }
[PROOFSTEP]
obtain ⟨y, hy, rfl⟩ := hx
[GOAL]
case mk.intro.intro
k : Type u_1
V₁ : Type u_2
P₁ : Type u_3
V₂ : Type u_4
P₂ : Type u_5
inst✝⁸ : Ring k
inst✝⁷ : AddCommGroup V₁
inst✝⁶ : AddCommGroup V₂
inst✝⁵ : Module k V₁
inst✝⁴ : Module k V₂
inst✝³ : AddTorsor V₁ P₁
inst✝² : AddTorsor V₂ P₂
φ : P₁ →ᵃ[k] P₂
E : AffineSubspace k P₁
F : AffineSubspace k P₂
inst✝¹ : Nonempty { x // x ∈ E }
inst✝ : Nonempty { x // x ∈ F }
h : AffineSubspace.map φ E = F
y : P₁
hy : y ∈ E
hx : ↑φ y ∈ F
⊢ ∃ a, ↑(restrict φ (_ : AffineSubspace.map φ E ≤ F)) a = { val := ↑φ y, property := hx }
[PROOFSTEP]
exact ⟨⟨y, hy⟩, rfl⟩


[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