[GOAL]
R : Type u_1
ι : Type u_2
inst✝³ : Semiring R
φ : ι → Type u_3
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
inst✝ : DecidableEq ι
i i' : ι
⊢ ↑(stdBasis R (fun _x => R) i) 1 i' = if i = i' then 1 else 0
[PROOFSTEP]
rw [LinearMap.stdBasis_apply, Function.update_apply, Pi.zero_apply]
[GOAL]
R : Type u_1
ι : Type u_2
inst✝³ : Semiring R
φ : ι → Type u_3
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
inst✝ : DecidableEq ι
i i' : ι
⊢ (if i' = i then 1 else 0) = if i = i' then 1 else 0
[PROOFSTEP]
congr 1
[GOAL]
case e_c
R : Type u_1
ι : Type u_2
inst✝³ : Semiring R
φ : ι → Type u_3
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
inst✝ : DecidableEq ι
i i' : ι
⊢ (i' = i) = (i = i')
[PROOFSTEP]
rw [eq_iff_iff, eq_comm]
[GOAL]
R : Type u_1
ι : Type u_2
inst✝³ : Semiring R
φ : ι → Type u_3
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
inst✝ : DecidableEq ι
i : ι
⊢ stdBasis R φ i = pi (diag i)
[PROOFSTEP]
ext x j
[GOAL]
case h.h
R : Type u_1
ι : Type u_2
inst✝³ : Semiring R
φ : ι → Type u_3
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
inst✝ : DecidableEq ι
i : ι
x : φ i
j : ι
⊢ ↑(stdBasis R φ i) x j = ↑(pi (diag i)) x j
[PROOFSTEP]
convert (update_apply (R := R) (φ := φ) (ι := ι) 0 x i j _).symm
[GOAL]
case h.e'_2.h.e'_1
R : Type u_1
ι : Type u_2
inst✝³ : Semiring R
φ : ι → Type u_3
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
inst✝ : DecidableEq ι
i : ι
x : φ i
j : ι
⊢ x = ↑id x
[PROOFSTEP]
rfl
[GOAL]
R : Type u_1
ι : Type u_2
inst✝³ : Semiring R
φ : ι → Type u_3
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
inst✝ : DecidableEq ι
i j : ι
⊢ comp (proj i) (stdBasis R φ j) = diag j i
[PROOFSTEP]
rw [stdBasis_eq_pi_diag, proj_pi]
[GOAL]
R : Type u_1
ι : Type u_2
inst✝³ : Semiring R
φ : ι → Type u_3
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
inst✝ : DecidableEq ι
I J : Set ι
h : Disjoint I J
⊢ ⨆ (i : ι) (_ : i ∈ I), range (stdBasis R φ i) ≤ ⨅ (i : ι) (_ : i ∈ J), ker (proj i)
[PROOFSTEP]
refine' iSup_le fun i => iSup_le fun hi => range_le_iff_comap.2 _
[GOAL]
R : Type u_1
ι : Type u_2
inst✝³ : Semiring R
φ : ι → Type u_3
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
inst✝ : DecidableEq ι
I J : Set ι
h : Disjoint I J
i : ι
hi : i ∈ I
⊢ comap (stdBasis R φ i) (⨅ (i : ι) (_ : i ∈ J), ker (proj i)) = ⊤
[PROOFSTEP]
simp only [← ker_comp, eq_top_iff, SetLike.le_def, mem_ker, comap_iInf, mem_iInf]
[GOAL]
R : Type u_1
ι : Type u_2
inst✝³ : Semiring R
φ : ι → Type u_3
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
inst✝ : DecidableEq ι
I J : Set ι
h : Disjoint I J
i : ι
hi : i ∈ I
⊢ ∀ ⦃x : φ i⦄, x ∈ ⊤ → ∀ (i_1 : ι), i_1 ∈ J → ↑(comp (proj i_1) (stdBasis R φ i)) x = 0
[PROOFSTEP]
rintro b - j hj
[GOAL]
R : Type u_1
ι : Type u_2
inst✝³ : Semiring R
φ : ι → Type u_3
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
inst✝ : DecidableEq ι
I J : Set ι
h : Disjoint I J
i : ι
hi : i ∈ I
b : φ i
j : ι
hj : j ∈ J
⊢ ↑(comp (proj j) (stdBasis R φ i)) b = 0
[PROOFSTEP]
rw [proj_stdBasis_ne R φ j i, zero_apply]
[GOAL]
R : Type u_1
ι : Type u_2
inst✝³ : Semiring R
φ : ι → Type u_3
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
inst✝ : DecidableEq ι
I J : Set ι
h : Disjoint I J
i : ι
hi : i ∈ I
b : φ i
j : ι
hj : j ∈ J
⊢ j ≠ i
[PROOFSTEP]
rintro rfl
[GOAL]
R : Type u_1
ι : Type u_2
inst✝³ : Semiring R
φ : ι → Type u_3
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
inst✝ : DecidableEq ι
I J : Set ι
h : Disjoint I J
j : ι
hj : j ∈ J
hi : j ∈ I
b : φ j
⊢ False
[PROOFSTEP]
exact h.le_bot ⟨hi, hj⟩
[GOAL]
R : Type u_1
ι : Type u_2
inst✝³ : Semiring R
φ : ι → Type u_3
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
inst✝ : DecidableEq ι
I : Finset ι
J : Set ι
hu : Set.univ ⊆ ↑I ∪ J
⊢ ∀ ⦃x : (i : ι) → φ i⦄, x ∈ ⨅ (i : ι) (_ : i ∈ J), ker (proj i) → x ∈ ⨆ (i : ι) (_ : i ∈ I), range (stdBasis R φ i)
[PROOFSTEP]
intro b hb
[GOAL]
R : Type u_1
ι : Type u_2
inst✝³ : Semiring R
φ : ι → Type u_3
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
inst✝ : DecidableEq ι
I : Finset ι
J : Set ι
hu : Set.univ ⊆ ↑I ∪ J
b : (i : ι) → φ i
hb : b ∈ ⨅ (i : ι) (_ : i ∈ J), ker (proj i)
⊢ b ∈ ⨆ (i : ι) (_ : i ∈ I), range (stdBasis R φ i)
[PROOFSTEP]
simp only [mem_iInf, mem_ker, proj_apply] at hb 
[GOAL]
R : Type u_1
ι : Type u_2
inst✝³ : Semiring R
φ : ι → Type u_3
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
inst✝ : DecidableEq ι
I : Finset ι
J : Set ι
hu : Set.univ ⊆ ↑I ∪ J
b : (i : ι) → φ i
hb : ∀ (i : ι), i ∈ J → b i = 0
⊢ b ∈ ⨆ (i : ι) (_ : i ∈ I), range (stdBasis R φ i)
[PROOFSTEP]
rw [←
  show (∑ i in I, stdBasis R φ i (b i)) = b by
    ext i
    rw [Finset.sum_apply, ← stdBasis_same R φ i (b i)]
    refine Finset.sum_eq_single i (fun j _ ne => stdBasis_ne _ _ _ _ ne.symm _) ?_
    intro hiI
    rw [stdBasis_same]
    exact hb _ ((hu trivial).resolve_left hiI)]
[GOAL]
R : Type u_1
ι : Type u_2
inst✝³ : Semiring R
φ : ι → Type u_3
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
inst✝ : DecidableEq ι
I : Finset ι
J : Set ι
hu : Set.univ ⊆ ↑I ∪ J
b : (i : ι) → φ i
hb : ∀ (i : ι), i ∈ J → b i = 0
⊢ ∑ i in I, ↑(stdBasis R φ i) (b i) = b
[PROOFSTEP]
ext i
[GOAL]
case h
R : Type u_1
ι : Type u_2
inst✝³ : Semiring R
φ : ι → Type u_3
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
inst✝ : DecidableEq ι
I : Finset ι
J : Set ι
hu : Set.univ ⊆ ↑I ∪ J
b : (i : ι) → φ i
hb : ∀ (i : ι), i ∈ J → b i = 0
i : ι
⊢ Finset.sum I (fun i => ↑(stdBasis R φ i) (b i)) i = b i
[PROOFSTEP]
rw [Finset.sum_apply, ← stdBasis_same R φ i (b i)]
[GOAL]
case h
R : Type u_1
ι : Type u_2
inst✝³ : Semiring R
φ : ι → Type u_3
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
inst✝ : DecidableEq ι
I : Finset ι
J : Set ι
hu : Set.univ ⊆ ↑I ∪ J
b : (i : ι) → φ i
hb : ∀ (i : ι), i ∈ J → b i = 0
i : ι
⊢ ∑ c in I, ↑(stdBasis R φ c) (b c) i = ↑(stdBasis R φ i) (b i) i
[PROOFSTEP]
refine Finset.sum_eq_single i (fun j _ ne => stdBasis_ne _ _ _ _ ne.symm _) ?_
[GOAL]
case h
R : Type u_1
ι : Type u_2
inst✝³ : Semiring R
φ : ι → Type u_3
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
inst✝ : DecidableEq ι
I : Finset ι
J : Set ι
hu : Set.univ ⊆ ↑I ∪ J
b : (i : ι) → φ i
hb : ∀ (i : ι), i ∈ J → b i = 0
i : ι
⊢ ¬i ∈ I → ↑(stdBasis R φ i) (b i) i = 0
[PROOFSTEP]
intro hiI
[GOAL]
case h
R : Type u_1
ι : Type u_2
inst✝³ : Semiring R
φ : ι → Type u_3
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
inst✝ : DecidableEq ι
I : Finset ι
J : Set ι
hu : Set.univ ⊆ ↑I ∪ J
b : (i : ι) → φ i
hb : ∀ (i : ι), i ∈ J → b i = 0
i : ι
hiI : ¬i ∈ I
⊢ ↑(stdBasis R φ i) (b i) i = 0
[PROOFSTEP]
rw [stdBasis_same]
[GOAL]
case h
R : Type u_1
ι : Type u_2
inst✝³ : Semiring R
φ : ι → Type u_3
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
inst✝ : DecidableEq ι
I : Finset ι
J : Set ι
hu : Set.univ ⊆ ↑I ∪ J
b : (i : ι) → φ i
hb : ∀ (i : ι), i ∈ J → b i = 0
i : ι
hiI : ¬i ∈ I
⊢ b i = 0
[PROOFSTEP]
exact hb _ ((hu trivial).resolve_left hiI)
[GOAL]
R : Type u_1
ι : Type u_2
inst✝³ : Semiring R
φ : ι → Type u_3
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
inst✝ : DecidableEq ι
I : Finset ι
J : Set ι
hu : Set.univ ⊆ ↑I ∪ J
b : (i : ι) → φ i
hb : ∀ (i : ι), i ∈ J → b i = 0
⊢ ∑ i in I, ↑(stdBasis R φ i) (b i) ∈ ⨆ (i : ι) (_ : i ∈ I), range (stdBasis R φ i)
[PROOFSTEP]
exact sum_mem_biSup fun i _ => mem_range_self (stdBasis R φ i) (b i)
[GOAL]
R : Type u_1
ι : Type u_2
inst✝³ : Semiring R
φ : ι → Type u_3
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
inst✝ : DecidableEq ι
I J : Set ι
hd : Disjoint I J
hu : Set.univ ⊆ I ∪ J
hI : Set.Finite I
⊢ ⨆ (i : ι) (_ : i ∈ I), range (stdBasis R φ i) = ⨅ (i : ι) (_ : i ∈ J), ker (proj i)
[PROOFSTEP]
refine' le_antisymm (iSup_range_stdBasis_le_iInf_ker_proj _ _ _ _ hd) _
[GOAL]
R : Type u_1
ι : Type u_2
inst✝³ : Semiring R
φ : ι → Type u_3
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
inst✝ : DecidableEq ι
I J : Set ι
hd : Disjoint I J
hu : Set.univ ⊆ I ∪ J
hI : Set.Finite I
⊢ ⨅ (i : ι) (_ : i ∈ J), ker (proj i) ≤ ⨆ (i : ι) (_ : i ∈ I), range (stdBasis R φ i)
[PROOFSTEP]
have : Set.univ ⊆ ↑hI.toFinset ∪ J := by rwa [hI.coe_toFinset]
[GOAL]
R : Type u_1
ι : Type u_2
inst✝³ : Semiring R
φ : ι → Type u_3
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
inst✝ : DecidableEq ι
I J : Set ι
hd : Disjoint I J
hu : Set.univ ⊆ I ∪ J
hI : Set.Finite I
⊢ Set.univ ⊆ ↑(Set.Finite.toFinset hI) ∪ J
[PROOFSTEP]
rwa [hI.coe_toFinset]
[GOAL]
R : Type u_1
ι : Type u_2
inst✝³ : Semiring R
φ : ι → Type u_3
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
inst✝ : DecidableEq ι
I J : Set ι
hd : Disjoint I J
hu : Set.univ ⊆ I ∪ J
hI : Set.Finite I
this : Set.univ ⊆ ↑(Set.Finite.toFinset hI) ∪ J
⊢ ⨅ (i : ι) (_ : i ∈ J), ker (proj i) ≤ ⨆ (i : ι) (_ : i ∈ I), range (stdBasis R φ i)
[PROOFSTEP]
refine' le_trans (iInf_ker_proj_le_iSup_range_stdBasis R φ this) (iSup_mono fun i => _)
[GOAL]
R : Type u_1
ι : Type u_2
inst✝³ : Semiring R
φ : ι → Type u_3
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
inst✝ : DecidableEq ι
I J : Set ι
hd : Disjoint I J
hu : Set.univ ⊆ I ∪ J
hI : Set.Finite I
this : Set.univ ⊆ ↑(Set.Finite.toFinset hI) ∪ J
i : ι
⊢ ⨆ (_ : i ∈ Set.Finite.toFinset hI), range (stdBasis R φ i) ≤ ⨆ (_ : i ∈ I), range (stdBasis R φ i)
[PROOFSTEP]
rw [Set.Finite.mem_toFinset]
[GOAL]
R : Type u_1
ι : Type u_2
inst✝⁴ : Semiring R
φ : ι → Type u_3
inst✝³ : (i : ι) → AddCommMonoid (φ i)
inst✝² : (i : ι) → Module R (φ i)
inst✝¹ : DecidableEq ι
inst✝ : Finite ι
⊢ ⨆ (i : ι), range (stdBasis R φ i) = ⊤
[PROOFSTEP]
cases nonempty_fintype ι
[GOAL]
case intro
R : Type u_1
ι : Type u_2
inst✝⁴ : Semiring R
φ : ι → Type u_3
inst✝³ : (i : ι) → AddCommMonoid (φ i)
inst✝² : (i : ι) → Module R (φ i)
inst✝¹ : DecidableEq ι
inst✝ : Finite ι
val✝ : Fintype ι
⊢ ⨆ (i : ι), range (stdBasis R φ i) = ⊤
[PROOFSTEP]
convert top_unique (iInf_emptyset.ge.trans <| iInf_ker_proj_le_iSup_range_stdBasis R φ _)
[GOAL]
case h.e'_2.h.e'_4.h
R : Type u_1
ι : Type u_2
inst✝⁴ : Semiring R
φ : ι → Type u_3
inst✝³ : (i : ι) → AddCommMonoid (φ i)
inst✝² : (i : ι) → Module R (φ i)
inst✝¹ : DecidableEq ι
inst✝ : Finite ι
val✝ : Fintype ι
x✝ : ι
⊢ range (stdBasis R φ x✝) = ⨆ (_ : x✝ ∈ ?intro.convert_1), range (stdBasis R φ x✝)
[PROOFSTEP]
rename_i i
[GOAL]
case h.e'_2.h.e'_4.h
R : Type u_1
ι : Type u_2
inst✝⁴ : Semiring R
φ : ι → Type u_3
inst✝³ : (i : ι) → AddCommMonoid (φ i)
inst✝² : (i : ι) → Module R (φ i)
inst✝¹ : DecidableEq ι
inst✝ : Finite ι
val✝ : Fintype ι
i : ι
⊢ range (stdBasis R φ i) = ⨆ (_ : i ∈ ?intro.convert_1), range (stdBasis R φ i)
[PROOFSTEP]
exact ((@iSup_pos _ _ _ fun _ => range <| stdBasis R φ i) <| Finset.mem_univ i).symm
[GOAL]
case intro.convert_2
R : Type u_1
ι : Type u_2
inst✝⁴ : Semiring R
φ : ι → Type u_3
inst✝³ : (i : ι) → AddCommMonoid (φ i)
inst✝² : (i : ι) → Module R (φ i)
inst✝¹ : DecidableEq ι
inst✝ : Finite ι
val✝ : Fintype ι
⊢ Set.univ ⊆ ↑Finset.univ ∪ ∅
[PROOFSTEP]
rw [Finset.coe_univ, Set.union_empty]
[GOAL]
R : Type u_1
ι : Type u_2
inst✝³ : Semiring R
φ : ι → Type u_3
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
inst✝ : DecidableEq ι
I J : Set ι
h : Disjoint I J
⊢ Disjoint (⨆ (i : ι) (_ : i ∈ I), range (stdBasis R φ i)) (⨆ (i : ι) (_ : i ∈ J), range (stdBasis R φ i))
[PROOFSTEP]
refine'
  Disjoint.mono (iSup_range_stdBasis_le_iInf_ker_proj _ _ _ _ <| disjoint_compl_right)
    (iSup_range_stdBasis_le_iInf_ker_proj _ _ _ _ <| disjoint_compl_right) _
[GOAL]
R : Type u_1
ι : Type u_2
inst✝³ : Semiring R
φ : ι → Type u_3
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
inst✝ : DecidableEq ι
I J : Set ι
h : Disjoint I J
⊢ Disjoint (⨅ (i : ι) (_ : i ∈ Iᶜ), ker (proj i)) (⨅ (i : ι) (_ : i ∈ Jᶜ), ker (proj i))
[PROOFSTEP]
simp only [disjoint_iff_inf_le, SetLike.le_def, mem_iInf, mem_inf, mem_ker, mem_bot, proj_apply, funext_iff]
[GOAL]
R : Type u_1
ι : Type u_2
inst✝³ : Semiring R
φ : ι → Type u_3
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
inst✝ : DecidableEq ι
I J : Set ι
h : Disjoint I J
⊢ ∀ ⦃x : (i : ι) → φ i⦄,
    ((∀ (i : ι), i ∈ Iᶜ → x i = 0) ∧ ∀ (i : ι), i ∈ Jᶜ → x i = 0) → ∀ (a : ι), x a = OfNat.ofNat 0 a
[PROOFSTEP]
rintro b ⟨hI, hJ⟩ i
[GOAL]
case intro
R : Type u_1
ι : Type u_2
inst✝³ : Semiring R
φ : ι → Type u_3
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
inst✝ : DecidableEq ι
I J : Set ι
h : Disjoint I J
b : (i : ι) → φ i
hI : ∀ (i : ι), i ∈ Iᶜ → b i = 0
hJ : ∀ (i : ι), i ∈ Jᶜ → b i = 0
i : ι
⊢ b i = OfNat.ofNat 0 i
[PROOFSTEP]
classical
by_cases hiI : i ∈ I
· by_cases hiJ : i ∈ J
  · exact (h.le_bot ⟨hiI, hiJ⟩).elim
  · exact hJ i hiJ
· exact hI i hiI
[GOAL]
case intro
R : Type u_1
ι : Type u_2
inst✝³ : Semiring R
φ : ι → Type u_3
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
inst✝ : DecidableEq ι
I J : Set ι
h : Disjoint I J
b : (i : ι) → φ i
hI : ∀ (i : ι), i ∈ Iᶜ → b i = 0
hJ : ∀ (i : ι), i ∈ Jᶜ → b i = 0
i : ι
⊢ b i = OfNat.ofNat 0 i
[PROOFSTEP]
by_cases hiI : i ∈ I
[GOAL]
case pos
R : Type u_1
ι : Type u_2
inst✝³ : Semiring R
φ : ι → Type u_3
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
inst✝ : DecidableEq ι
I J : Set ι
h : Disjoint I J
b : (i : ι) → φ i
hI : ∀ (i : ι), i ∈ Iᶜ → b i = 0
hJ : ∀ (i : ι), i ∈ Jᶜ → b i = 0
i : ι
hiI : i ∈ I
⊢ b i = OfNat.ofNat 0 i
[PROOFSTEP]
by_cases hiJ : i ∈ J
[GOAL]
case pos
R : Type u_1
ι : Type u_2
inst✝³ : Semiring R
φ : ι → Type u_3
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
inst✝ : DecidableEq ι
I J : Set ι
h : Disjoint I J
b : (i : ι) → φ i
hI : ∀ (i : ι), i ∈ Iᶜ → b i = 0
hJ : ∀ (i : ι), i ∈ Jᶜ → b i = 0
i : ι
hiI : i ∈ I
hiJ : i ∈ J
⊢ b i = OfNat.ofNat 0 i
[PROOFSTEP]
exact (h.le_bot ⟨hiI, hiJ⟩).elim
[GOAL]
case neg
R : Type u_1
ι : Type u_2
inst✝³ : Semiring R
φ : ι → Type u_3
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
inst✝ : DecidableEq ι
I J : Set ι
h : Disjoint I J
b : (i : ι) → φ i
hI : ∀ (i : ι), i ∈ Iᶜ → b i = 0
hJ : ∀ (i : ι), i ∈ Jᶜ → b i = 0
i : ι
hiI : i ∈ I
hiJ : ¬i ∈ J
⊢ b i = OfNat.ofNat 0 i
[PROOFSTEP]
exact hJ i hiJ
[GOAL]
case neg
R : Type u_1
ι : Type u_2
inst✝³ : Semiring R
φ : ι → Type u_3
inst✝² : (i : ι) → AddCommMonoid (φ i)
inst✝¹ : (i : ι) → Module R (φ i)
inst✝ : DecidableEq ι
I J : Set ι
h : Disjoint I J
b : (i : ι) → φ i
hI : ∀ (i : ι), i ∈ Iᶜ → b i = 0
hJ : ∀ (i : ι), i ∈ Jᶜ → b i = 0
i : ι
hiI : ¬i ∈ I
⊢ b i = OfNat.ofNat 0 i
[PROOFSTEP]
exact hI i hiI
[GOAL]
R : Type u_1
η : Type u_2
ιs : η → Type u_3
Ms : η → Type u_4
inst✝³ : Ring R
inst✝² : (i : η) → AddCommGroup (Ms i)
inst✝¹ : (i : η) → Module R (Ms i)
inst✝ : DecidableEq η
v : (j : η) → ιs j → Ms j
hs : ∀ (i : η), LinearIndependent R (v i)
⊢ LinearIndependent R fun ji => ↑(stdBasis R Ms ji.fst) (v ji.fst ji.snd)
[PROOFSTEP]
have hs' : ∀ j : η, LinearIndependent R fun i : ιs j => stdBasis R Ms j (v j i) :=
  by
  intro j
  exact (hs j).map' _ (ker_stdBasis _ _ _)
[GOAL]
R : Type u_1
η : Type u_2
ιs : η → Type u_3
Ms : η → Type u_4
inst✝³ : Ring R
inst✝² : (i : η) → AddCommGroup (Ms i)
inst✝¹ : (i : η) → Module R (Ms i)
inst✝ : DecidableEq η
v : (j : η) → ιs j → Ms j
hs : ∀ (i : η), LinearIndependent R (v i)
⊢ ∀ (j : η), LinearIndependent R fun i => ↑(stdBasis R Ms j) (v j i)
[PROOFSTEP]
intro j
[GOAL]
R : Type u_1
η : Type u_2
ιs : η → Type u_3
Ms : η → Type u_4
inst✝³ : Ring R
inst✝² : (i : η) → AddCommGroup (Ms i)
inst✝¹ : (i : η) → Module R (Ms i)
inst✝ : DecidableEq η
v : (j : η) → ιs j → Ms j
hs : ∀ (i : η), LinearIndependent R (v i)
j : η
⊢ LinearIndependent R fun i => ↑(stdBasis R Ms j) (v j i)
[PROOFSTEP]
exact (hs j).map' _ (ker_stdBasis _ _ _)
[GOAL]
R : Type u_1
η : Type u_2
ιs : η → Type u_3
Ms : η → Type u_4
inst✝³ : Ring R
inst✝² : (i : η) → AddCommGroup (Ms i)
inst✝¹ : (i : η) → Module R (Ms i)
inst✝ : DecidableEq η
v : (j : η) → ιs j → Ms j
hs : ∀ (i : η), LinearIndependent R (v i)
hs' : ∀ (j : η), LinearIndependent R fun i => ↑(stdBasis R Ms j) (v j i)
⊢ LinearIndependent R fun ji => ↑(stdBasis R Ms ji.fst) (v ji.fst ji.snd)
[PROOFSTEP]
apply linearIndependent_iUnion_finite hs'
[GOAL]
R : Type u_1
η : Type u_2
ιs : η → Type u_3
Ms : η → Type u_4
inst✝³ : Ring R
inst✝² : (i : η) → AddCommGroup (Ms i)
inst✝¹ : (i : η) → Module R (Ms i)
inst✝ : DecidableEq η
v : (j : η) → ιs j → Ms j
hs : ∀ (i : η), LinearIndependent R (v i)
hs' : ∀ (j : η), LinearIndependent R fun i => ↑(stdBasis R Ms j) (v j i)
⊢ ∀ (i : η) (t : Set η),
    Set.Finite t →
      ¬i ∈ t →
        Disjoint (span R (Set.range fun i_1 => ↑(stdBasis R Ms i) (v i i_1)))
          (⨆ (i : η) (_ : i ∈ t), span R (Set.range fun i_1 => ↑(stdBasis R Ms i) (v i i_1)))
[PROOFSTEP]
intro j J _ hiJ
[GOAL]
R : Type u_1
η : Type u_2
ιs : η → Type u_3
Ms : η → Type u_4
inst✝³ : Ring R
inst✝² : (i : η) → AddCommGroup (Ms i)
inst✝¹ : (i : η) → Module R (Ms i)
inst✝ : DecidableEq η
v : (j : η) → ιs j → Ms j
hs : ∀ (i : η), LinearIndependent R (v i)
hs' : ∀ (j : η), LinearIndependent R fun i => ↑(stdBasis R Ms j) (v j i)
j : η
J : Set η
a✝ : Set.Finite J
hiJ : ¬j ∈ J
⊢ Disjoint (span R (Set.range fun i => ↑(stdBasis R Ms j) (v j i)))
    (⨆ (i : η) (_ : i ∈ J), span R (Set.range fun i_1 => ↑(stdBasis R Ms i) (v i i_1)))
[PROOFSTEP]
simp only
[GOAL]
R : Type u_1
η : Type u_2
ιs : η → Type u_3
Ms : η → Type u_4
inst✝³ : Ring R
inst✝² : (i : η) → AddCommGroup (Ms i)
inst✝¹ : (i : η) → Module R (Ms i)
inst✝ : DecidableEq η
v : (j : η) → ιs j → Ms j
hs : ∀ (i : η), LinearIndependent R (v i)
hs' : ∀ (j : η), LinearIndependent R fun i => ↑(stdBasis R Ms j) (v j i)
j : η
J : Set η
a✝ : Set.Finite J
hiJ : ¬j ∈ J
⊢ Disjoint (span R (Set.range fun i => ↑(stdBasis R Ms j) (v j i)))
    (⨆ (i : η) (_ : i ∈ J), span R (Set.range fun i_1 => ↑(stdBasis R Ms i) (v i i_1)))
[PROOFSTEP]
have h₀ : ∀ j, span R (range fun i : ιs j => stdBasis R Ms j (v j i)) ≤ LinearMap.range (stdBasis R Ms j) :=
  by
  intro j
  rw [span_le, LinearMap.range_coe]
  apply range_comp_subset_range
[GOAL]
R : Type u_1
η : Type u_2
ιs : η → Type u_3
Ms : η → Type u_4
inst✝³ : Ring R
inst✝² : (i : η) → AddCommGroup (Ms i)
inst✝¹ : (i : η) → Module R (Ms i)
inst✝ : DecidableEq η
v : (j : η) → ιs j → Ms j
hs : ∀ (i : η), LinearIndependent R (v i)
hs' : ∀ (j : η), LinearIndependent R fun i => ↑(stdBasis R Ms j) (v j i)
j : η
J : Set η
a✝ : Set.Finite J
hiJ : ¬j ∈ J
⊢ ∀ (j : η), span R (Set.range fun i => ↑(stdBasis R Ms j) (v j i)) ≤ LinearMap.range (stdBasis R Ms j)
[PROOFSTEP]
intro j
[GOAL]
R : Type u_1
η : Type u_2
ιs : η → Type u_3
Ms : η → Type u_4
inst✝³ : Ring R
inst✝² : (i : η) → AddCommGroup (Ms i)
inst✝¹ : (i : η) → Module R (Ms i)
inst✝ : DecidableEq η
v : (j : η) → ιs j → Ms j
hs : ∀ (i : η), LinearIndependent R (v i)
hs' : ∀ (j : η), LinearIndependent R fun i => ↑(stdBasis R Ms j) (v j i)
j✝ : η
J : Set η
a✝ : Set.Finite J
hiJ : ¬j✝ ∈ J
j : η
⊢ span R (Set.range fun i => ↑(stdBasis R Ms j) (v j i)) ≤ LinearMap.range (stdBasis R Ms j)
[PROOFSTEP]
rw [span_le, LinearMap.range_coe]
[GOAL]
R : Type u_1
η : Type u_2
ιs : η → Type u_3
Ms : η → Type u_4
inst✝³ : Ring R
inst✝² : (i : η) → AddCommGroup (Ms i)
inst✝¹ : (i : η) → Module R (Ms i)
inst✝ : DecidableEq η
v : (j : η) → ιs j → Ms j
hs : ∀ (i : η), LinearIndependent R (v i)
hs' : ∀ (j : η), LinearIndependent R fun i => ↑(stdBasis R Ms j) (v j i)
j✝ : η
J : Set η
a✝ : Set.Finite J
hiJ : ¬j✝ ∈ J
j : η
⊢ (Set.range fun i => ↑(stdBasis R Ms j) (v j i)) ⊆ Set.range ↑(stdBasis R Ms j)
[PROOFSTEP]
apply range_comp_subset_range
[GOAL]
R : Type u_1
η : Type u_2
ιs : η → Type u_3
Ms : η → Type u_4
inst✝³ : Ring R
inst✝² : (i : η) → AddCommGroup (Ms i)
inst✝¹ : (i : η) → Module R (Ms i)
inst✝ : DecidableEq η
v : (j : η) → ιs j → Ms j
hs : ∀ (i : η), LinearIndependent R (v i)
hs' : ∀ (j : η), LinearIndependent R fun i => ↑(stdBasis R Ms j) (v j i)
j : η
J : Set η
a✝ : Set.Finite J
hiJ : ¬j ∈ J
h₀ : ∀ (j : η), span R (Set.range fun i => ↑(stdBasis R Ms j) (v j i)) ≤ LinearMap.range (stdBasis R Ms j)
⊢ Disjoint (span R (Set.range fun i => ↑(stdBasis R Ms j) (v j i)))
    (⨆ (i : η) (_ : i ∈ J), span R (Set.range fun i_1 => ↑(stdBasis R Ms i) (v i i_1)))
[PROOFSTEP]
have h₁ :
  span R (range fun i : ιs j => stdBasis R Ms j (v j i)) ≤ ⨆ i ∈ ({ j } : Set _), LinearMap.range (stdBasis R Ms i) :=
  by
  rw [@iSup_singleton _ _ _ fun i => LinearMap.range (stdBasis R (Ms) i)]
  apply h₀
[GOAL]
R : Type u_1
η : Type u_2
ιs : η → Type u_3
Ms : η → Type u_4
inst✝³ : Ring R
inst✝² : (i : η) → AddCommGroup (Ms i)
inst✝¹ : (i : η) → Module R (Ms i)
inst✝ : DecidableEq η
v : (j : η) → ιs j → Ms j
hs : ∀ (i : η), LinearIndependent R (v i)
hs' : ∀ (j : η), LinearIndependent R fun i => ↑(stdBasis R Ms j) (v j i)
j : η
J : Set η
a✝ : Set.Finite J
hiJ : ¬j ∈ J
h₀ : ∀ (j : η), span R (Set.range fun i => ↑(stdBasis R Ms j) (v j i)) ≤ LinearMap.range (stdBasis R Ms j)
⊢ span R (Set.range fun i => ↑(stdBasis R Ms j) (v j i)) ≤ ⨆ (i : η) (_ : i ∈ {j}), LinearMap.range (stdBasis R Ms i)
[PROOFSTEP]
rw [@iSup_singleton _ _ _ fun i => LinearMap.range (stdBasis R (Ms) i)]
[GOAL]
R : Type u_1
η : Type u_2
ιs : η → Type u_3
Ms : η → Type u_4
inst✝³ : Ring R
inst✝² : (i : η) → AddCommGroup (Ms i)
inst✝¹ : (i : η) → Module R (Ms i)
inst✝ : DecidableEq η
v : (j : η) → ιs j → Ms j
hs : ∀ (i : η), LinearIndependent R (v i)
hs' : ∀ (j : η), LinearIndependent R fun i => ↑(stdBasis R Ms j) (v j i)
j : η
J : Set η
a✝ : Set.Finite J
hiJ : ¬j ∈ J
h₀ : ∀ (j : η), span R (Set.range fun i => ↑(stdBasis R Ms j) (v j i)) ≤ LinearMap.range (stdBasis R Ms j)
⊢ span R (Set.range fun i => ↑(stdBasis R Ms j) (v j i)) ≤ LinearMap.range (stdBasis R Ms j)
[PROOFSTEP]
apply h₀
[GOAL]
R : Type u_1
η : Type u_2
ιs : η → Type u_3
Ms : η → Type u_4
inst✝³ : Ring R
inst✝² : (i : η) → AddCommGroup (Ms i)
inst✝¹ : (i : η) → Module R (Ms i)
inst✝ : DecidableEq η
v : (j : η) → ιs j → Ms j
hs : ∀ (i : η), LinearIndependent R (v i)
hs' : ∀ (j : η), LinearIndependent R fun i => ↑(stdBasis R Ms j) (v j i)
j : η
J : Set η
a✝ : Set.Finite J
hiJ : ¬j ∈ J
h₀ : ∀ (j : η), span R (Set.range fun i => ↑(stdBasis R Ms j) (v j i)) ≤ LinearMap.range (stdBasis R Ms j)
h₁ : span R (Set.range fun i => ↑(stdBasis R Ms j) (v j i)) ≤ ⨆ (i : η) (_ : i ∈ {j}), LinearMap.range (stdBasis R Ms i)
⊢ Disjoint (span R (Set.range fun i => ↑(stdBasis R Ms j) (v j i)))
    (⨆ (i : η) (_ : i ∈ J), span R (Set.range fun i_1 => ↑(stdBasis R Ms i) (v i i_1)))
[PROOFSTEP]
have h₂ :
  ⨆ j ∈ J, span R (range fun i : ιs j => stdBasis R Ms j (v j i)) ≤
    ⨆ j ∈ J, LinearMap.range (stdBasis R (fun j : η => Ms j) j) :=
  iSup₂_mono fun i _ => h₀ i
[GOAL]
R : Type u_1
η : Type u_2
ιs : η → Type u_3
Ms : η → Type u_4
inst✝³ : Ring R
inst✝² : (i : η) → AddCommGroup (Ms i)
inst✝¹ : (i : η) → Module R (Ms i)
inst✝ : DecidableEq η
v : (j : η) → ιs j → Ms j
hs : ∀ (i : η), LinearIndependent R (v i)
hs' : ∀ (j : η), LinearIndependent R fun i => ↑(stdBasis R Ms j) (v j i)
j : η
J : Set η
a✝ : Set.Finite J
hiJ : ¬j ∈ J
h₀ : ∀ (j : η), span R (Set.range fun i => ↑(stdBasis R Ms j) (v j i)) ≤ LinearMap.range (stdBasis R Ms j)
h₁ : span R (Set.range fun i => ↑(stdBasis R Ms j) (v j i)) ≤ ⨆ (i : η) (_ : i ∈ {j}), LinearMap.range (stdBasis R Ms i)
h₂ :
  ⨆ (j : η) (_ : j ∈ J), span R (Set.range fun i => ↑(stdBasis R Ms j) (v j i)) ≤
    ⨆ (j : η) (_ : j ∈ J), LinearMap.range (stdBasis R (fun j => Ms j) j)
⊢ Disjoint (span R (Set.range fun i => ↑(stdBasis R Ms j) (v j i)))
    (⨆ (i : η) (_ : i ∈ J), span R (Set.range fun i_1 => ↑(stdBasis R Ms i) (v i i_1)))
[PROOFSTEP]
have h₃ : Disjoint (fun i : η => i ∈ ({ j } : Set _)) J := by convert Set.disjoint_singleton_left.2 hiJ using 0
[GOAL]
R : Type u_1
η : Type u_2
ιs : η → Type u_3
Ms : η → Type u_4
inst✝³ : Ring R
inst✝² : (i : η) → AddCommGroup (Ms i)
inst✝¹ : (i : η) → Module R (Ms i)
inst✝ : DecidableEq η
v : (j : η) → ιs j → Ms j
hs : ∀ (i : η), LinearIndependent R (v i)
hs' : ∀ (j : η), LinearIndependent R fun i => ↑(stdBasis R Ms j) (v j i)
j : η
J : Set η
a✝ : Set.Finite J
hiJ : ¬j ∈ J
h₀ : ∀ (j : η), span R (Set.range fun i => ↑(stdBasis R Ms j) (v j i)) ≤ LinearMap.range (stdBasis R Ms j)
h₁ : span R (Set.range fun i => ↑(stdBasis R Ms j) (v j i)) ≤ ⨆ (i : η) (_ : i ∈ {j}), LinearMap.range (stdBasis R Ms i)
h₂ :
  ⨆ (j : η) (_ : j ∈ J), span R (Set.range fun i => ↑(stdBasis R Ms j) (v j i)) ≤
    ⨆ (j : η) (_ : j ∈ J), LinearMap.range (stdBasis R (fun j => Ms j) j)
⊢ Disjoint (fun i => i ∈ {j}) J
[PROOFSTEP]
convert Set.disjoint_singleton_left.2 hiJ using 0
[GOAL]
R : Type u_1
η : Type u_2
ιs : η → Type u_3
Ms : η → Type u_4
inst✝³ : Ring R
inst✝² : (i : η) → AddCommGroup (Ms i)
inst✝¹ : (i : η) → Module R (Ms i)
inst✝ : DecidableEq η
v : (j : η) → ιs j → Ms j
hs : ∀ (i : η), LinearIndependent R (v i)
hs' : ∀ (j : η), LinearIndependent R fun i => ↑(stdBasis R Ms j) (v j i)
j : η
J : Set η
a✝ : Set.Finite J
hiJ : ¬j ∈ J
h₀ : ∀ (j : η), span R (Set.range fun i => ↑(stdBasis R Ms j) (v j i)) ≤ LinearMap.range (stdBasis R Ms j)
h₁ : span R (Set.range fun i => ↑(stdBasis R Ms j) (v j i)) ≤ ⨆ (i : η) (_ : i ∈ {j}), LinearMap.range (stdBasis R Ms i)
h₂ :
  ⨆ (j : η) (_ : j ∈ J), span R (Set.range fun i => ↑(stdBasis R Ms j) (v j i)) ≤
    ⨆ (j : η) (_ : j ∈ J), LinearMap.range (stdBasis R (fun j => Ms j) j)
h₃ : Disjoint (fun i => i ∈ {j}) J
⊢ Disjoint (span R (Set.range fun i => ↑(stdBasis R Ms j) (v j i)))
    (⨆ (i : η) (_ : i ∈ J), span R (Set.range fun i_1 => ↑(stdBasis R Ms i) (v i i_1)))
[PROOFSTEP]
exact (disjoint_stdBasis_stdBasis _ _ _ _ h₃).mono h₁ h₂
[GOAL]
R : Type u_1
η : Type u_2
ιs : η → Type u_3
Ms : η → Type u_4
inst✝⁴ : Semiring R
inst✝³ : (i : η) → AddCommMonoid (Ms i)
inst✝² : (i : η) → Module R (Ms i)
inst✝¹ : Fintype η
inst✝ : DecidableEq η
s : (j : η) → Basis (ιs j) R (Ms j)
j : η
i : ιs j
⊢ ↑(Pi.basis s).repr (↑(stdBasis R Ms j) (↑(s j) i)) = Finsupp.single { fst := j, snd := i } 1
[PROOFSTEP]
ext ⟨j', i'⟩
[GOAL]
case h.mk
R : Type u_1
η : Type u_2
ιs : η → Type u_3
Ms : η → Type u_4
inst✝⁴ : Semiring R
inst✝³ : (i : η) → AddCommMonoid (Ms i)
inst✝² : (i : η) → Module R (Ms i)
inst✝¹ : Fintype η
inst✝ : DecidableEq η
s : (j : η) → Basis (ιs j) R (Ms j)
j : η
i : ιs j
j' : η
i' : ιs j'
⊢ ↑(↑(Pi.basis s).repr (↑(stdBasis R Ms j) (↑(s j) i))) { fst := j', snd := i' } =
    ↑(Finsupp.single { fst := j, snd := i } 1) { fst := j', snd := i' }
[PROOFSTEP]
by_cases hj : j = j'
[GOAL]
case pos
R : Type u_1
η : Type u_2
ιs : η → Type u_3
Ms : η → Type u_4
inst✝⁴ : Semiring R
inst✝³ : (i : η) → AddCommMonoid (Ms i)
inst✝² : (i : η) → Module R (Ms i)
inst✝¹ : Fintype η
inst✝ : DecidableEq η
s : (j : η) → Basis (ιs j) R (Ms j)
j : η
i : ιs j
j' : η
i' : ιs j'
hj : j = j'
⊢ ↑(↑(Pi.basis s).repr (↑(stdBasis R Ms j) (↑(s j) i))) { fst := j', snd := i' } =
    ↑(Finsupp.single { fst := j, snd := i } 1) { fst := j', snd := i' }
[PROOFSTEP]
subst hj
[GOAL]
case pos
R : Type u_1
η : Type u_2
ιs : η → Type u_3
Ms : η → Type u_4
inst✝⁴ : Semiring R
inst✝³ : (i : η) → AddCommMonoid (Ms i)
inst✝² : (i : η) → Module R (Ms i)
inst✝¹ : Fintype η
inst✝ : DecidableEq η
s : (j : η) → Basis (ιs j) R (Ms j)
j : η
i i' : ιs j
⊢ ↑(↑(Pi.basis s).repr (↑(stdBasis R Ms j) (↑(s j) i))) { fst := j, snd := i' } =
    ↑(Finsupp.single { fst := j, snd := i } 1) { fst := j, snd := i' }
[PROOFSTEP]
simp only [Pi.basis, LinearEquiv.trans_apply, Basis.repr_self, stdBasis_same, LinearEquiv.piCongrRight,
  Finsupp.sigmaFinsuppLEquivPiFinsupp_symm_apply, Basis.repr_symm_apply, LinearEquiv.coe_mk, ne_eq, Sigma.mk.inj_iff,
  heq_eq_eq, true_and]
[GOAL]
case pos
R : Type u_1
η : Type u_2
ιs : η → Type u_3
Ms : η → Type u_4
inst✝⁴ : Semiring R
inst✝³ : (i : η) → AddCommMonoid (Ms i)
inst✝² : (i : η) → Module R (Ms i)
inst✝¹ : Fintype η
inst✝ : DecidableEq η
s : (j : η) → Basis (ιs j) R (Ms j)
j : η
i i' : ιs j
⊢ ↑(Finsupp.single i 1) i' = ↑(Finsupp.single { fst := j, snd := i } 1) { fst := j, snd := i' }
[PROOFSTEP]
symm
  -- Porting note: `Sigma.mk.inj` not found in the following, replaced by `Sigma.mk.inj_iff.mp`
[GOAL]
case pos
R : Type u_1
η : Type u_2
ιs : η → Type u_3
Ms : η → Type u_4
inst✝⁴ : Semiring R
inst✝³ : (i : η) → AddCommMonoid (Ms i)
inst✝² : (i : η) → Module R (Ms i)
inst✝¹ : Fintype η
inst✝ : DecidableEq η
s : (j : η) → Basis (ιs j) R (Ms j)
j : η
i i' : ιs j
⊢ ↑(Finsupp.single { fst := j, snd := i } 1) { fst := j, snd := i' } = ↑(Finsupp.single i 1) i'
[PROOFSTEP]
exact
  Finsupp.single_apply_left (fun i i' (h : (⟨j, i⟩ : Σ j, ιs j) = ⟨j, i'⟩) => eq_of_heq (Sigma.mk.inj_iff.mp h).2) _ _ _
[GOAL]
case neg
R : Type u_1
η : Type u_2
ιs : η → Type u_3
Ms : η → Type u_4
inst✝⁴ : Semiring R
inst✝³ : (i : η) → AddCommMonoid (Ms i)
inst✝² : (i : η) → Module R (Ms i)
inst✝¹ : Fintype η
inst✝ : DecidableEq η
s : (j : η) → Basis (ιs j) R (Ms j)
j : η
i : ιs j
j' : η
i' : ιs j'
hj : ¬j = j'
⊢ ↑(↑(Pi.basis s).repr (↑(stdBasis R Ms j) (↑(s j) i))) { fst := j', snd := i' } =
    ↑(Finsupp.single { fst := j, snd := i } 1) { fst := j', snd := i' }
[PROOFSTEP]
simp only [Pi.basis, LinearEquiv.trans_apply, Finsupp.sigmaFinsuppLEquivPiFinsupp_symm_apply, LinearEquiv.piCongrRight]
[GOAL]
case neg
R : Type u_1
η : Type u_2
ιs : η → Type u_3
Ms : η → Type u_4
inst✝⁴ : Semiring R
inst✝³ : (i : η) → AddCommMonoid (Ms i)
inst✝² : (i : η) → Module R (Ms i)
inst✝¹ : Fintype η
inst✝ : DecidableEq η
s : (j : η) → Basis (ιs j) R (Ms j)
j : η
i : ιs j
j' : η
i' : ιs j'
hj : ¬j = j'
⊢ ↑(↑{
              toLinearMap :=
                {
                  toAddHom :=
                    { toFun := fun f i => ↑(s i).repr (f i),
                      map_add' :=
                        (_ :
                          ∀ (x y : (j : η) → (fun j => Ms j) j),
                            Equiv.toFun (AddEquiv.piCongrRight fun j => toAddEquiv (s j).repr).toEquiv (x + y) =
                              Equiv.toFun (AddEquiv.piCongrRight fun j => toAddEquiv (s j).repr).toEquiv x +
                                Equiv.toFun (AddEquiv.piCongrRight fun j => toAddEquiv (s j).repr).toEquiv y) },
                  map_smul' :=
                    (_ :
                      ∀ (c : R) (f : (i : η) → (fun j => Ms j) i),
                        AddHom.toFun
                            { toFun := fun f i => ↑(s i).repr (f i),
                              map_add' :=
                                (_ :
                                  ∀ (x y : (j : η) → (fun j => Ms j) j),
                                    Equiv.toFun (AddEquiv.piCongrRight fun j => toAddEquiv (s j).repr).toEquiv (x + y) =
                                      Equiv.toFun (AddEquiv.piCongrRight fun j => toAddEquiv (s j).repr).toEquiv x +
                                        Equiv.toFun (AddEquiv.piCongrRight fun j => toAddEquiv (s j).repr).toEquiv y) }
                            (c • f) =
                          ↑(RingHom.id R) c •
                            AddHom.toFun
                              { toFun := fun f i => ↑(s i).repr (f i),
                                map_add' :=
                                  (_ :
                                    ∀ (x y : (j : η) → (fun j => Ms j) j),
                                      Equiv.toFun (AddEquiv.piCongrRight fun j => toAddEquiv (s j).repr).toEquiv
                                          (x + y) =
                                        Equiv.toFun (AddEquiv.piCongrRight fun j => toAddEquiv (s j).repr).toEquiv x +
                                          Equiv.toFun (AddEquiv.piCongrRight fun j => toAddEquiv (s j).repr).toEquiv
                                            y) }
                              f) },
              invFun := fun f i => ↑(LinearEquiv.symm (s i).repr) (f i),
              left_inv :=
                (_ :
                  LeftInverse (AddEquiv.piCongrRight fun j => toAddEquiv (s j).repr).toEquiv.invFun
                    (AddEquiv.piCongrRight fun j => toAddEquiv (s j).repr).toEquiv.toFun),
              right_inv :=
                (_ :
                  Function.RightInverse (AddEquiv.piCongrRight fun j => toAddEquiv (s j).repr).toEquiv.invFun
                    (AddEquiv.piCongrRight fun j => toAddEquiv (s j).repr).toEquiv.toFun) }
          (↑(stdBasis R Ms j) (↑(s j) i)) j')
      i' =
    ↑(Finsupp.single { fst := j, snd := i } 1) { fst := j', snd := i' }
[PROOFSTEP]
dsimp
[GOAL]
case neg
R : Type u_1
η : Type u_2
ιs : η → Type u_3
Ms : η → Type u_4
inst✝⁴ : Semiring R
inst✝³ : (i : η) → AddCommMonoid (Ms i)
inst✝² : (i : η) → Module R (Ms i)
inst✝¹ : Fintype η
inst✝ : DecidableEq η
s : (j : η) → Basis (ιs j) R (Ms j)
j : η
i : ιs j
j' : η
i' : ιs j'
hj : ¬j = j'
⊢ ↑(↑(s j').repr (↑(stdBasis R Ms j) (↑(s j) i) j')) i' =
    ↑(Finsupp.single { fst := j, snd := i } 1) { fst := j', snd := i' }
[PROOFSTEP]
rw [stdBasis_ne _ _ _ _ (Ne.symm hj), LinearEquiv.map_zero, Finsupp.zero_apply, Finsupp.single_eq_of_ne]
[GOAL]
case neg
R : Type u_1
η : Type u_2
ιs : η → Type u_3
Ms : η → Type u_4
inst✝⁴ : Semiring R
inst✝³ : (i : η) → AddCommMonoid (Ms i)
inst✝² : (i : η) → Module R (Ms i)
inst✝¹ : Fintype η
inst✝ : DecidableEq η
s : (j : η) → Basis (ιs j) R (Ms j)
j : η
i : ιs j
j' : η
i' : ιs j'
hj : ¬j = j'
⊢ { fst := j, snd := i } ≠ { fst := j', snd := i' }
[PROOFSTEP]
rintro ⟨⟩
[GOAL]
case neg.refl
R : Type u_1
η : Type u_2
ιs : η → Type u_3
Ms : η → Type u_4
inst✝⁴ : Semiring R
inst✝³ : (i : η) → AddCommMonoid (Ms i)
inst✝² : (i : η) → Module R (Ms i)
inst✝¹ : Fintype η
inst✝ : DecidableEq η
s : (j : η) → Basis (ιs j) R (Ms j)
j : η
i : ιs j
hj : ¬j = j
⊢ False
[PROOFSTEP]
contradiction
[GOAL]
R : Type u_1
η : Type u_2
ιs : η → Type u_3
Ms : η → Type u_4
inst✝⁴ : Semiring R
inst✝³ : (i : η) → AddCommMonoid (Ms i)
inst✝² : (i : η) → Module R (Ms i)
inst✝¹ : Fintype η
inst✝ : DecidableEq η
s : (j : η) → Basis (ιs j) R (Ms j)
ji : (j : η) × ιs j
⊢ ↑(Pi.basis s).repr (↑(stdBasis R Ms ji.fst) (↑(s ji.fst) ji.snd)) = Finsupp.single ji 1
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
η : Type u_2
ιs : η → Type u_3
Ms : η → Type u_4
inst✝⁴ : Semiring R
inst✝³ : (i : η) → AddCommMonoid (Ms i)
inst✝² : (i : η) → Module R (Ms i)
inst✝¹ : Fintype η
inst✝ : DecidableEq η
i : η
⊢ ↑(basisFun R η) i = ↑(stdBasis R (fun x => R) i) 1
[PROOFSTEP]
simp only [basisFun, Basis.coe_ofEquivFun, LinearEquiv.refl_symm, LinearEquiv.refl_apply, stdBasis_apply]
[GOAL]
R : Type u_1
η : Type u_2
ιs : η → Type u_3
Ms : η → Type u_4
inst✝³ : Semiring R
inst✝² : (i : η) → AddCommMonoid (Ms i)
inst✝¹ : (i : η) → Module R (Ms i)
inst✝ : Fintype η
x : η → R
i : η
⊢ ↑(↑(basisFun R η).repr x) i = x i
[PROOFSTEP]
simp [basisFun]
[GOAL]
R : Type u_1
m : Type u_2
n : Type u_3
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : Semiring R
i : n
j : m
inst✝¹ : DecidableEq n
inst✝ : DecidableEq m
⊢ ↑(stdBasis R n m) (i, j) = stdBasisMatrix i j 1
[PROOFSTEP]
ext a b
[GOAL]
case a.h
R : Type u_1
m : Type u_2
n : Type u_3
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : Semiring R
i : n
j : m
inst✝¹ : DecidableEq n
inst✝ : DecidableEq m
a : n
b : m
⊢ ↑(stdBasis R n m) (i, j) a b = stdBasisMatrix i j 1 a b
[PROOFSTEP]
by_cases hi : i = a
[GOAL]
case pos
R : Type u_1
m : Type u_2
n : Type u_3
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : Semiring R
i : n
j : m
inst✝¹ : DecidableEq n
inst✝ : DecidableEq m
a : n
b : m
hi : i = a
⊢ ↑(stdBasis R n m) (i, j) a b = stdBasisMatrix i j 1 a b
[PROOFSTEP]
by_cases hj : j = b
[GOAL]
case neg
R : Type u_1
m : Type u_2
n : Type u_3
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : Semiring R
i : n
j : m
inst✝¹ : DecidableEq n
inst✝ : DecidableEq m
a : n
b : m
hi : ¬i = a
⊢ ↑(stdBasis R n m) (i, j) a b = stdBasisMatrix i j 1 a b
[PROOFSTEP]
by_cases hj : j = b
[GOAL]
case pos
R : Type u_1
m : Type u_2
n : Type u_3
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : Semiring R
i : n
j : m
inst✝¹ : DecidableEq n
inst✝ : DecidableEq m
a : n
b : m
hi : i = a
hj : j = b
⊢ ↑(stdBasis R n m) (i, j) a b = stdBasisMatrix i j 1 a b
[PROOFSTEP]
simp [stdBasis, hi, hj, Basis.coe_reindex, comp_apply, Equiv.sigmaEquivProd_symm_apply, StdBasisMatrix.apply_same]
[GOAL]
case pos
R : Type u_1
m : Type u_2
n : Type u_3
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : Semiring R
i : n
j : m
inst✝¹ : DecidableEq n
inst✝ : DecidableEq m
a : n
b : m
hi : i = a
hj : j = b
⊢ ↑(Pi.basis fun x => Pi.basisFun R m) { fst := a, snd := b } a b = 1
[PROOFSTEP]
erw [Pi.basis_apply]
[GOAL]
case pos
R : Type u_1
m : Type u_2
n : Type u_3
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : Semiring R
i : n
j : m
inst✝¹ : DecidableEq n
inst✝ : DecidableEq m
a : n
b : m
hi : i = a
hj : j = b
⊢ ↑(LinearMap.stdBasis R (fun a => m → R) { fst := a, snd := b }.fst) (↑(Pi.basisFun R m) { fst := a, snd := b }.snd) a
      b =
    1
[PROOFSTEP]
simp
[GOAL]
case neg
R : Type u_1
m : Type u_2
n : Type u_3
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : Semiring R
i : n
j : m
inst✝¹ : DecidableEq n
inst✝ : DecidableEq m
a : n
b : m
hi : i = a
hj : ¬j = b
⊢ ↑(stdBasis R n m) (i, j) a b = stdBasisMatrix i j 1 a b
[PROOFSTEP]
simp only [stdBasis, hi, Basis.coe_reindex, comp_apply, Equiv.sigmaEquivProd_symm_apply, hj, and_false, not_false_iff,
  StdBasisMatrix.apply_of_ne]
[GOAL]
case neg
R : Type u_1
m : Type u_2
n : Type u_3
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : Semiring R
i : n
j : m
inst✝¹ : DecidableEq n
inst✝ : DecidableEq m
a : n
b : m
hi : i = a
hj : ¬j = b
⊢ ↑(Pi.basis fun x => Pi.basisFun R m) { fst := a, snd := j } a b = 0
[PROOFSTEP]
erw [Pi.basis_apply]
[GOAL]
case neg
R : Type u_1
m : Type u_2
n : Type u_3
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : Semiring R
i : n
j : m
inst✝¹ : DecidableEq n
inst✝ : DecidableEq m
a : n
b : m
hi : i = a
hj : ¬j = b
⊢ ↑(LinearMap.stdBasis R (fun a => m → R) { fst := a, snd := j }.fst) (↑(Pi.basisFun R m) { fst := a, snd := j }.snd) a
      b =
    0
[PROOFSTEP]
simp [hj]
[GOAL]
case pos
R : Type u_1
m : Type u_2
n : Type u_3
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : Semiring R
i : n
j : m
inst✝¹ : DecidableEq n
inst✝ : DecidableEq m
a : n
b : m
hi : ¬i = a
hj : j = b
⊢ ↑(stdBasis R n m) (i, j) a b = stdBasisMatrix i j 1 a b
[PROOFSTEP]
simp only [stdBasis, hj, Basis.coe_reindex, comp_apply, Equiv.sigmaEquivProd_symm_apply, hi, and_true, not_false_iff,
  StdBasisMatrix.apply_of_ne]
[GOAL]
case pos
R : Type u_1
m : Type u_2
n : Type u_3
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : Semiring R
i : n
j : m
inst✝¹ : DecidableEq n
inst✝ : DecidableEq m
a : n
b : m
hi : ¬i = a
hj : j = b
⊢ ↑(Pi.basis fun x => Pi.basisFun R m) { fst := i, snd := b } a b = 0
[PROOFSTEP]
erw [Pi.basis_apply]
[GOAL]
case pos
R : Type u_1
m : Type u_2
n : Type u_3
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : Semiring R
i : n
j : m
inst✝¹ : DecidableEq n
inst✝ : DecidableEq m
a : n
b : m
hi : ¬i = a
hj : j = b
⊢ ↑(LinearMap.stdBasis R (fun a => m → R) { fst := i, snd := b }.fst) (↑(Pi.basisFun R m) { fst := i, snd := b }.snd) a
      b =
    0
[PROOFSTEP]
simp [hi, hj, Ne.symm hi, LinearMap.stdBasis_ne]
[GOAL]
case neg
R : Type u_1
m : Type u_2
n : Type u_3
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : Semiring R
i : n
j : m
inst✝¹ : DecidableEq n
inst✝ : DecidableEq m
a : n
b : m
hi : ¬i = a
hj : ¬j = b
⊢ ↑(stdBasis R n m) (i, j) a b = stdBasisMatrix i j 1 a b
[PROOFSTEP]
simp only [stdBasis, Basis.coe_reindex, comp_apply, Equiv.sigmaEquivProd_symm_apply, hi, hj, and_self, not_false_iff,
  StdBasisMatrix.apply_of_ne]
[GOAL]
case neg
R : Type u_1
m : Type u_2
n : Type u_3
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : Semiring R
i : n
j : m
inst✝¹ : DecidableEq n
inst✝ : DecidableEq m
a : n
b : m
hi : ¬i = a
hj : ¬j = b
⊢ ↑(Pi.basis fun x => Pi.basisFun R m) { fst := i, snd := j } a b = 0
[PROOFSTEP]
erw [Pi.basis_apply]
[GOAL]
case neg
R : Type u_1
m : Type u_2
n : Type u_3
inst✝⁴ : Fintype m
inst✝³ : Fintype n
inst✝² : Semiring R
i : n
j : m
inst✝¹ : DecidableEq n
inst✝ : DecidableEq m
a : n
b : m
hi : ¬i = a
hj : ¬j = b
⊢ ↑(LinearMap.stdBasis R (fun a => m → R) { fst := i, snd := j }.fst) (↑(Pi.basisFun R m) { fst := i, snd := j }.snd) a
      b =
    0
[PROOFSTEP]
simp [hi, hj, Ne.symm hj, Ne.symm hi, LinearMap.stdBasis_ne]
