case intro
R : Type u_3
ι : Type u_1
inst✝⁴ : Semiring R
φ : ι → Type u_2
inst✝³ : (i : ι) → AddCommMonoid (φ i)
inst✝² : (i : ι) → Module R (φ i)
inst✝¹ : DecidableEq ι
inst✝ : Finite ι
val✝ : Fintype ι
⊢ (⨆ (i : ι), range (stdBasis R φ i)) = ⊤
R : Type u_3
ι : Type u_1
inst✝⁴ : Semiring R
φ : ι → Type u_2
inst✝³ : (i : ι) → AddCommMonoid (φ i)
inst✝² : (i : ι) → Module R (φ i)
inst✝¹ : DecidableEq ι
inst✝ : Finite ι
⊢ (⨆ (i : ι), range (stdBasis R φ i)) = ⊤
cases nonempty_fintype ι
case h.e'_2.h.e'_4.h
R : Type u_3
ι : Type u_1
inst✝⁴ : Semiring R
φ : ι → Type u_2
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✝)

case intro.convert_1
R : Type u_3
ι : Type u_1
inst✝⁴ : Semiring R
φ : ι → Type u_2
inst✝³ : (i : ι) → AddCommMonoid (φ i)
inst✝² : (i : ι) → Module R (φ i)
inst✝¹ : DecidableEq ι
inst✝ : Finite ι
val✝ : Fintype ι
⊢ Finset ι

case intro.convert_2
R : Type u_3
ι : Type u_1
inst✝⁴ : Semiring R
φ : ι → Type u_2
inst✝³ : (i : ι) → AddCommMonoid (φ i)
inst✝² : (i : ι) → Module R (φ i)
inst✝¹ : DecidableEq ι
inst✝ : Finite ι
val✝ : Fintype ι
⊢ Set.univ ⊆ ↑?intro.convert_1 ∪ ∅
case intro
R : Type u_3
ι : Type u_1
inst✝⁴ : Semiring R
φ : ι → Type u_2
inst✝³ : (i : ι) → AddCommMonoid (φ i)
inst✝² : (i : ι) → Module R (φ i)
inst✝¹ : DecidableEq ι
inst✝ : Finite ι
val✝ : Fintype ι
⊢ (⨆ (i : ι), range (stdBasis R φ i)) = ⊤
convert top_unique (iInf_emptyset.ge.trans <| iInf_ker_proj_le_iSup_range_stdBasis R φ _)
case h.e'_2.h.e'_4.h
R : Type u_3
ι : Type u_1
inst✝⁴ : Semiring R
φ : ι → Type u_2
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)
case h.e'_2.h.e'_4.h
R : Type u_3
ι : Type u_1
inst✝⁴ : Semiring R
φ : ι → Type u_2
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✝)
rename_i i
no goals
case h.e'_2.h.e'_4.h
R : Type u_3
ι : Type u_1
inst✝⁴ : Semiring R
φ : ι → Type u_2
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)
exact ((@iSup_pos _ _ _ fun _ => range <| stdBasis R φ i) <| Finset.mem_univ i).symm
no goals
case intro.convert_2
R : Type u_3
ι : Type u_1
inst✝⁴ : Semiring R
φ : ι → Type u_2
inst✝³ : (i : ι) → AddCommMonoid (φ i)
inst✝² : (i : ι) → Module R (φ i)
inst✝¹ : DecidableEq ι
inst✝ : Finite ι
val✝ : Fintype ι
⊢ Set.univ ⊆ ↑Finset.univ ∪ ∅
rw [Finset.coe_univ, Set.union_empty]