[GOAL]
α : Type u
inst✝ : Preorder α
c : Chain α
x : α
⊢ IsωSup c x ↔ IsLUB (range ↑c) x
[PROOFSTEP]
simp [IsωSup, IsLUB, IsLeast, upperBounds, lowerBounds]
[GOAL]
α : Type u
inst✝ : OmegaCompletePartialOrder α
s : Set (Set α)
hs : ∀ (t : Set α), t ∈ s → IsOpen α t
⊢ IsOpen α (⋃₀ s)
[PROOFSTEP]
simp only [IsOpen] at hs ⊢
[GOAL]
α : Type u
inst✝ : OmegaCompletePartialOrder α
s : Set (Set α)
hs : ∀ (t : Set α), t ∈ s → Continuous' fun x => x ∈ t
⊢ Continuous' fun x => x ∈ ⋃₀ s
[PROOFSTEP]
convert CompleteLattice.sSup_continuous' (setOf ⁻¹' s) hs
[GOAL]
case h.e'_5.h.a
α : Type u
inst✝ : OmegaCompletePartialOrder α
s : Set (Set α)
hs : ∀ (t : Set α), t ∈ s → Continuous' fun x => x ∈ t
x✝ : α
⊢ x✝ ∈ ⋃₀ s ↔ sSup (setOf ⁻¹' s) x✝
[PROOFSTEP]
simp only [sSup_apply, setOf_bijective.surjective.exists, exists_prop, mem_preimage, SetCoe.exists, iSup_Prop_eq,
  mem_setOf_eq, mem_sUnion]
[GOAL]
α : Type u_1
inst✝ : OmegaCompletePartialOrder α
y : Scott α
⊢ IsOpen (notBelow y)
[PROOFSTEP]
have h : Monotone (notBelow y) := fun x z hle ↦ mt hle.trans
[GOAL]
α : Type u_1
inst✝ : OmegaCompletePartialOrder α
y : Scott α
h : Monotone (notBelow y)
⊢ IsOpen (notBelow y)
[PROOFSTEP]
refine ⟨h, fun c ↦ eq_of_forall_ge_iff fun z ↦ ?_⟩
[GOAL]
α : Type u_1
inst✝ : OmegaCompletePartialOrder α
y : Scott α
h : Monotone (notBelow y)
c : Chain α
z : Prop
⊢ ↑{ toFun := fun x => x ∈ notBelow y, monotone' := h } (ωSup c) ≤ z ↔
    ωSup (Chain.map c { toFun := fun x => x ∈ notBelow y, monotone' := h }) ≤ z
[PROOFSTEP]
simp only [ωSup_le_iff, notBelow, mem_setOf_eq, le_Prop_eq, OrderHom.coe_mk, Chain.map_coe, Function.comp_apply,
  exists_imp, not_forall]
[GOAL]
α : Type u_1
inst✝ : OmegaCompletePartialOrder α
c : Chain α
⊢ IsωSup c (ωSup c)
[PROOFSTEP]
constructor
[GOAL]
case left
α : Type u_1
inst✝ : OmegaCompletePartialOrder α
c : Chain α
⊢ ∀ (i : ℕ), ↑c i ≤ ωSup c
[PROOFSTEP]
apply le_ωSup
[GOAL]
case right
α : Type u_1
inst✝ : OmegaCompletePartialOrder α
c : Chain α
⊢ ∀ (y : α), (∀ (i : ℕ), ↑c i ≤ y) → ωSup c ≤ y
[PROOFSTEP]
apply ωSup_le
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : OmegaCompletePartialOrder β
f : Scott α → Scott β
hf : _root_.Continuous f
⊢ Continuous' f
[PROOFSTEP]
have h : Monotone f := fun x y h ↦
  by
  have hf : IsUpperSet {x | ¬f x ≤ f y} := ((notBelow_isOpen (f y)).preimage hf).isUpperSet
  simpa only [mem_setOf_eq, le_refl, not_true, imp_false, not_not] using hf h
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : OmegaCompletePartialOrder β
f : Scott α → Scott β
hf : _root_.Continuous f
x y : Scott α
h : x ≤ y
⊢ f x ≤ f y
[PROOFSTEP]
have hf : IsUpperSet {x | ¬f x ≤ f y} := ((notBelow_isOpen (f y)).preimage hf).isUpperSet
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : OmegaCompletePartialOrder β
f : Scott α → Scott β
hf✝ : _root_.Continuous f
x y : Scott α
h : x ≤ y
hf : IsUpperSet {x | ¬f x ≤ f y}
⊢ f x ≤ f y
[PROOFSTEP]
simpa only [mem_setOf_eq, le_refl, not_true, imp_false, not_not] using hf h
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : OmegaCompletePartialOrder β
f : Scott α → Scott β
hf : _root_.Continuous f
h : Monotone f
⊢ Continuous' f
[PROOFSTEP]
refine ⟨h, fun c ↦ eq_of_forall_ge_iff fun z ↦ ?_⟩
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : OmegaCompletePartialOrder β
f : Scott α → Scott β
hf : _root_.Continuous f
h : Monotone f
c : Chain (Scott α)
z : Scott β
⊢ ↑{ toFun := f, monotone' := h } (ωSup c) ≤ z ↔ ωSup (Chain.map c { toFun := f, monotone' := h }) ≤ z
[PROOFSTEP]
rcases(notBelow_isOpen z).preimage hf with ⟨hf, hf'⟩
[GOAL]
case intro
α : Type u_1
β : Type u_2
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : OmegaCompletePartialOrder β
f : Scott α → Scott β
hf✝ : _root_.Continuous f
h : Monotone f
c : Chain (Scott α)
z : Scott β
hf : Monotone fun x => x ∈ f ⁻¹' notBelow z
hf' : OmegaCompletePartialOrder.Continuous { toFun := fun x => x ∈ f ⁻¹' notBelow z, monotone' := hf }
⊢ ↑{ toFun := f, monotone' := h } (ωSup c) ≤ z ↔ ωSup (Chain.map c { toFun := f, monotone' := h }) ≤ z
[PROOFSTEP]
specialize hf' c
[GOAL]
case intro
α : Type u_1
β : Type u_2
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : OmegaCompletePartialOrder β
f : Scott α → Scott β
hf✝ : _root_.Continuous f
h : Monotone f
c : Chain (Scott α)
z : Scott β
hf : Monotone fun x => x ∈ f ⁻¹' notBelow z
hf' :
  ↑{ toFun := fun x => x ∈ f ⁻¹' notBelow z, monotone' := hf } (ωSup c) =
    ωSup (Chain.map c { toFun := fun x => x ∈ f ⁻¹' notBelow z, monotone' := hf })
⊢ ↑{ toFun := f, monotone' := h } (ωSup c) ≤ z ↔ ωSup (Chain.map c { toFun := f, monotone' := h }) ≤ z
[PROOFSTEP]
simp only [OrderHom.coe_mk, mem_preimage, notBelow, mem_setOf_eq] at hf'
[GOAL]
case intro
α : Type u_1
β : Type u_2
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : OmegaCompletePartialOrder β
f : Scott α → Scott β
hf✝ : _root_.Continuous f
h : Monotone f
c : Chain (Scott α)
z : Scott β
hf : Monotone fun x => x ∈ f ⁻¹' notBelow z
hf' :
  (¬f (ωSup c) ≤ z) = ωSup (Chain.map c { toFun := fun x => ¬f x ≤ z, monotone' := (_ : Monotone fun x => ¬f x ≤ z) })
⊢ ↑{ toFun := f, monotone' := h } (ωSup c) ≤ z ↔ ωSup (Chain.map c { toFun := f, monotone' := h }) ≤ z
[PROOFSTEP]
rw [← not_iff_not]
[GOAL]
case intro
α : Type u_1
β : Type u_2
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : OmegaCompletePartialOrder β
f : Scott α → Scott β
hf✝ : _root_.Continuous f
h : Monotone f
c : Chain (Scott α)
z : Scott β
hf : Monotone fun x => x ∈ f ⁻¹' notBelow z
hf' :
  (¬f (ωSup c) ≤ z) = ωSup (Chain.map c { toFun := fun x => ¬f x ≤ z, monotone' := (_ : Monotone fun x => ¬f x ≤ z) })
⊢ ¬↑{ toFun := f, monotone' := h } (ωSup c) ≤ z ↔ ¬ωSup (Chain.map c { toFun := f, monotone' := h }) ≤ z
[PROOFSTEP]
simp only [ωSup_le_iff, hf', ωSup, iSup, sSup, mem_range, Chain.map_coe, Function.comp_apply, eq_iff_iff, not_forall,
  OrderHom.coe_mk]
[GOAL]
case intro
α : Type u_1
β : Type u_2
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : OmegaCompletePartialOrder β
f : Scott α → Scott β
hf✝ : _root_.Continuous f
h : Monotone f
c : Chain (Scott α)
z : Scott β
hf : Monotone fun x => x ∈ f ⁻¹' notBelow z
hf' :
  (¬f (ωSup c) ≤ z) = ωSup (Chain.map c { toFun := fun x => ¬f x ≤ z, monotone' := (_ : Monotone fun x => ¬f x ≤ z) })
⊢ (∃ a, (∃ y, ¬f (↑c y) ≤ z ↔ a) ∧ a) ↔ ∃ x, ¬f (↑c x) ≤ z
[PROOFSTEP]
tauto
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : OmegaCompletePartialOrder β
f : Scott α → Scott β
hf : Continuous' f
⊢ _root_.Continuous f
[PROOFSTEP]
rw [continuous_def]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : OmegaCompletePartialOrder β
f : Scott α → Scott β
hf : Continuous' f
⊢ ∀ (s : Set (Scott β)), IsOpen s → IsOpen (f ⁻¹' s)
[PROOFSTEP]
intro s hs
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : OmegaCompletePartialOrder β
f : Scott α → Scott β
hf : Continuous' f
s : Set (Scott β)
hs : IsOpen s
⊢ IsOpen (f ⁻¹' s)
[PROOFSTEP]
change Continuous' (s ∘ f)
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : OmegaCompletePartialOrder β
f : Scott α → Scott β
hf : Continuous' f
s : Set (Scott β)
hs : IsOpen s
⊢ Continuous' (s ∘ f)
[PROOFSTEP]
cases' hs with hs hs'
[GOAL]
case intro
α : Type u_1
β : Type u_2
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : OmegaCompletePartialOrder β
f : Scott α → Scott β
hf : Continuous' f
s : Set (Scott β)
hs : Monotone fun x => x ∈ s
hs' : OmegaCompletePartialOrder.Continuous { toFun := fun x => x ∈ s, monotone' := hs }
⊢ Continuous' (s ∘ f)
[PROOFSTEP]
cases' hf with hf hf'
[GOAL]
case intro.intro
α : Type u_1
β : Type u_2
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : OmegaCompletePartialOrder β
f : Scott α → Scott β
s : Set (Scott β)
hs : Monotone fun x => x ∈ s
hs' : OmegaCompletePartialOrder.Continuous { toFun := fun x => x ∈ s, monotone' := hs }
hf : Monotone f
hf' : OmegaCompletePartialOrder.Continuous { toFun := f, monotone' := hf }
⊢ Continuous' (s ∘ f)
[PROOFSTEP]
apply Continuous.of_bundled
[GOAL]
case intro.intro.hf'
α : Type u_1
β : Type u_2
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : OmegaCompletePartialOrder β
f : Scott α → Scott β
s : Set (Scott β)
hs : Monotone fun x => x ∈ s
hs' : OmegaCompletePartialOrder.Continuous { toFun := fun x => x ∈ s, monotone' := hs }
hf : Monotone f
hf' : OmegaCompletePartialOrder.Continuous { toFun := f, monotone' := hf }
⊢ OmegaCompletePartialOrder.Continuous { toFun := s ∘ f, monotone' := ?intro.intro.hf }
case intro.intro.hf
α : Type u_1
β : Type u_2
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : OmegaCompletePartialOrder β
f : Scott α → Scott β
s : Set (Scott β)
hs : Monotone fun x => x ∈ s
hs' : OmegaCompletePartialOrder.Continuous { toFun := fun x => x ∈ s, monotone' := hs }
hf : Monotone f
hf' : OmegaCompletePartialOrder.Continuous { toFun := f, monotone' := hf }
⊢ Monotone (s ∘ f)
[PROOFSTEP]
apply continuous_comp _ _ hf' hs'


[GOAL]
ι : Type u_1
ι' : Type u_2
K : Type u_3
V : Type u_4
V' : Type u_5
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup V'
inst✝¹ : Module K V
inst✝ : Module K V'
v : ι → V
s t : Set V
x y z : V
hs : LinearIndependent K Subtype.val
⊢ ↑⊤ ⊆ ↑(span K (range (restrict (LinearIndependent.extend hs (_ : s ⊆ univ)) id)))
[PROOFSTEP]
simpa using hs.subset_span_extend (subset_univ s)
[GOAL]
ι : Type u_1
ι' : Type u_2
K : Type u_3
V : Type u_4
V' : Type u_5
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup V'
inst✝¹ : Module K V
inst✝ : Module K V'
v : ι → V
s t : Set V
x y z : V
hs : LinearIndependent K Subtype.val
⊢ range ↑(extend hs) = LinearIndependent.extend hs (_ : s ⊆ univ)
[PROOFSTEP]
rw [coe_extend, Subtype.range_coe_subtype, setOf_mem_eq]
[GOAL]
ι : Type u_1
ι' : Type u_2
K : Type u_3
V : Type u_4
V' : Type u_5
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup V'
inst✝¹ : Module K V
inst✝ : Module K V'
v : ι → V
s t : Set V
x✝ y z : V
x : ↑(ofVectorSpaceIndex K V)
⊢ ↑(ofVectorSpace K V) x = ↑x
[PROOFSTEP]
unfold ofVectorSpace
[GOAL]
ι : Type u_1
ι' : Type u_2
K : Type u_3
V : Type u_4
V' : Type u_5
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup V'
inst✝¹ : Module K V
inst✝ : Module K V'
v : ι → V
s t : Set V
x✝ y z : V
x : ↑(ofVectorSpaceIndex K V)
⊢ ↑(extend (_ : LinearIndependent K fun x => ↑x)) x = ↑x
[PROOFSTEP]
exact Basis.mk_apply _ _ _
[GOAL]
ι : Type u_1
ι' : Type u_2
K : Type u_3
V : Type u_4
V' : Type u_5
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup V'
inst✝¹ : Module K V
inst✝ : Module K V'
v : ι → V
s t : Set V
x y z : V
⊢ LinearIndependent K Subtype.val
[PROOFSTEP]
convert (ofVectorSpace K V).linearIndependent
[GOAL]
case h.e'_4
ι : Type u_1
ι' : Type u_2
K : Type u_3
V : Type u_4
V' : Type u_5
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup V'
inst✝¹ : Module K V
inst✝ : Module K V'
v : ι → V
s t : Set V
x y z : V
⊢ Subtype.val = ↑(ofVectorSpace K V)
[PROOFSTEP]
ext x
[GOAL]
case h.e'_4.h
ι : Type u_1
ι' : Type u_2
K : Type u_3
V : Type u_4
V' : Type u_5
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup V'
inst✝¹ : Module K V
inst✝ : Module K V'
v : ι → V
s t : Set V
x✝ y z : V
x : { x // x ∈ ofVectorSpaceIndex K V }
⊢ ↑x = ↑(ofVectorSpace K V) x
[PROOFSTEP]
rw [ofVectorSpace_apply_self]
[GOAL]
ι : Type u_1
ι' : Type u_2
K : Type u_3
V : Type u_4
V' : Type u_5
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup V
inst✝⁴ : AddCommGroup V'
inst✝³ : Module K V
inst✝² : Module K V'
v : ι → V
s t : Set V
x y z : V
inst✝¹ : Fintype K
inst✝ : Fintype V
⊢ ∃ n, card V = card K ^ n
[PROOFSTEP]
classical exact ⟨card (Basis.ofVectorSpaceIndex K V), Module.card_fintype (Basis.ofVectorSpace K V)⟩
[GOAL]
ι : Type u_1
ι' : Type u_2
K : Type u_3
V : Type u_4
V' : Type u_5
inst✝⁶ : DivisionRing K
inst✝⁵ : AddCommGroup V
inst✝⁴ : AddCommGroup V'
inst✝³ : Module K V
inst✝² : Module K V'
v : ι → V
s t : Set V
x y z : V
inst✝¹ : Fintype K
inst✝ : Fintype V
⊢ ∃ n, card V = card K ^ n
[PROOFSTEP]
exact ⟨card (Basis.ofVectorSpaceIndex K V), Module.card_fintype (Basis.ofVectorSpace K V)⟩
[GOAL]
ι : Type u_1
ι' : Type u_2
K : Type u_3
V : Type u_4
V' : Type u_5
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup V'
inst✝¹ : Module K V
inst✝ : Module K V'
v✝ : ι → V
s t : Set V
x y z v : V
hv : v ≠ 0
⊢ IsAtom (span K {v})
[PROOFSTEP]
constructor
[GOAL]
case left
ι : Type u_1
ι' : Type u_2
K : Type u_3
V : Type u_4
V' : Type u_5
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup V'
inst✝¹ : Module K V
inst✝ : Module K V'
v✝ : ι → V
s t : Set V
x y z v : V
hv : v ≠ 0
⊢ span K {v} ≠ ⊥
[PROOFSTEP]
rw [Submodule.ne_bot_iff]
[GOAL]
case left
ι : Type u_1
ι' : Type u_2
K : Type u_3
V : Type u_4
V' : Type u_5
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup V'
inst✝¹ : Module K V
inst✝ : Module K V'
v✝ : ι → V
s t : Set V
x y z v : V
hv : v ≠ 0
⊢ ∃ x, x ∈ span K {v} ∧ x ≠ 0
[PROOFSTEP]
exact ⟨v, ⟨mem_span_singleton_self v, hv⟩⟩
[GOAL]
case right
ι : Type u_1
ι' : Type u_2
K : Type u_3
V : Type u_4
V' : Type u_5
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup V'
inst✝¹ : Module K V
inst✝ : Module K V'
v✝ : ι → V
s t : Set V
x y z v : V
hv : v ≠ 0
⊢ ∀ (b : Submodule K V), b < span K {v} → b = ⊥
[PROOFSTEP]
intro T hT
[GOAL]
case right
ι : Type u_1
ι' : Type u_2
K : Type u_3
V : Type u_4
V' : Type u_5
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup V'
inst✝¹ : Module K V
inst✝ : Module K V'
v✝ : ι → V
s t : Set V
x y z v : V
hv : v ≠ 0
T : Submodule K V
hT : T < span K {v}
⊢ T = ⊥
[PROOFSTEP]
by_contra h
[GOAL]
case right
ι : Type u_1
ι' : Type u_2
K : Type u_3
V : Type u_4
V' : Type u_5
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup V'
inst✝¹ : Module K V
inst✝ : Module K V'
v✝ : ι → V
s t : Set V
x y z v : V
hv : v ≠ 0
T : Submodule K V
hT : T < span K {v}
h : ¬T = ⊥
⊢ False
[PROOFSTEP]
apply hT.2
[GOAL]
case right
ι : Type u_1
ι' : Type u_2
K : Type u_3
V : Type u_4
V' : Type u_5
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup V'
inst✝¹ : Module K V
inst✝ : Module K V'
v✝ : ι → V
s t : Set V
x y z v : V
hv : v ≠ 0
T : Submodule K V
hT : T < span K {v}
h : ¬T = ⊥
⊢ ↑(span K {v}) ⊆ ↑T
[PROOFSTEP]
change span K { v } ≤ T
[GOAL]
case right
ι : Type u_1
ι' : Type u_2
K : Type u_3
V : Type u_4
V' : Type u_5
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup V'
inst✝¹ : Module K V
inst✝ : Module K V'
v✝ : ι → V
s t : Set V
x y z v : V
hv : v ≠ 0
T : Submodule K V
hT : T < span K {v}
h : ¬T = ⊥
⊢ span K {v} ≤ T
[PROOFSTEP]
simp_rw [span_singleton_le_iff_mem, ← Ne.def, Submodule.ne_bot_iff] at *
[GOAL]
case right
ι : Type u_1
ι' : Type u_2
K : Type u_3
V : Type u_4
V' : Type u_5
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup V'
inst✝¹ : Module K V
inst✝ : Module K V'
v✝ : ι → V
s t : Set V
x y z v : V
hv : v ≠ 0
T : Submodule K V
hT : T < span K {v}
h : ∃ x, x ∈ T ∧ x ≠ 0
⊢ v ∈ T
[PROOFSTEP]
rcases h with ⟨s, ⟨hs, hz⟩⟩
[GOAL]
case right.intro.intro
ι : Type u_1
ι' : Type u_2
K : Type u_3
V : Type u_4
V' : Type u_5
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup V'
inst✝¹ : Module K V
inst✝ : Module K V'
v✝ : ι → V
s✝ t : Set V
x y z v : V
hv : v ≠ 0
T : Submodule K V
hT : T < span K {v}
s : V
hs : s ∈ T
hz : s ≠ 0
⊢ v ∈ T
[PROOFSTEP]
rcases mem_span_singleton.1 (hT.1 hs) with ⟨a, rfl⟩
[GOAL]
case right.intro.intro.intro
ι : Type u_1
ι' : Type u_2
K : Type u_3
V : Type u_4
V' : Type u_5
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup V'
inst✝¹ : Module K V
inst✝ : Module K V'
v✝ : ι → V
s t : Set V
x y z v : V
hv : v ≠ 0
T : Submodule K V
hT : T < span K {v}
a : K
hs : a • v ∈ T
hz : a • v ≠ 0
⊢ v ∈ T
[PROOFSTEP]
rcases eq_or_ne a 0 with rfl | h
[GOAL]
case right.intro.intro.intro.inl
ι : Type u_1
ι' : Type u_2
K : Type u_3
V : Type u_4
V' : Type u_5
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup V'
inst✝¹ : Module K V
inst✝ : Module K V'
v✝ : ι → V
s t : Set V
x y z v : V
hv : v ≠ 0
T : Submodule K V
hT : T < span K {v}
hs : 0 • v ∈ T
hz : 0 • v ≠ 0
⊢ v ∈ T
[PROOFSTEP]
simp only [zero_smul, ne_eq, not_true] at hz
[GOAL]
case right.intro.intro.intro.inr
ι : Type u_1
ι' : Type u_2
K : Type u_3
V : Type u_4
V' : Type u_5
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup V'
inst✝¹ : Module K V
inst✝ : Module K V'
v✝ : ι → V
s t : Set V
x y z v : V
hv : v ≠ 0
T : Submodule K V
hT : T < span K {v}
a : K
hs : a • v ∈ T
hz : a • v ≠ 0
h : a ≠ 0
⊢ v ∈ T
[PROOFSTEP]
rwa [T.smul_mem_iff h] at hs
[GOAL]
ι : Type u_1
ι' : Type u_2
K : Type u_3
V : Type u_4
V' : Type u_5
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup V'
inst✝¹ : Module K V
inst✝ : Module K V'
v : ι → V
s t : Set V
x y z : V
W : Submodule K V
⊢ IsAtom W ↔ ∃ v x, W = span K {v}
[PROOFSTEP]
refine' ⟨fun h => _, fun h => _⟩
[GOAL]
case refine'_1
ι : Type u_1
ι' : Type u_2
K : Type u_3
V : Type u_4
V' : Type u_5
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup V'
inst✝¹ : Module K V
inst✝ : Module K V'
v : ι → V
s t : Set V
x y z : V
W : Submodule K V
h : IsAtom W
⊢ ∃ v x, W = span K {v}
[PROOFSTEP]
cases' h with hbot h
[GOAL]
case refine'_1.intro
ι : Type u_1
ι' : Type u_2
K : Type u_3
V : Type u_4
V' : Type u_5
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup V'
inst✝¹ : Module K V
inst✝ : Module K V'
v : ι → V
s t : Set V
x y z : V
W : Submodule K V
hbot : W ≠ ⊥
h : ∀ (b : Submodule K V), b < W → b = ⊥
⊢ ∃ v x, W = span K {v}
[PROOFSTEP]
rcases(Submodule.ne_bot_iff W).1 hbot with ⟨v, ⟨hW, hv⟩⟩
[GOAL]
case refine'_1.intro.intro.intro
ι : Type u_1
ι' : Type u_2
K : Type u_3
V : Type u_4
V' : Type u_5
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup V'
inst✝¹ : Module K V
inst✝ : Module K V'
v✝ : ι → V
s t : Set V
x y z : V
W : Submodule K V
hbot : W ≠ ⊥
h : ∀ (b : Submodule K V), b < W → b = ⊥
v : V
hW : v ∈ W
hv : v ≠ 0
⊢ ∃ v x, W = span K {v}
[PROOFSTEP]
refine' ⟨v, ⟨hv, _⟩⟩
[GOAL]
case refine'_1.intro.intro.intro
ι : Type u_1
ι' : Type u_2
K : Type u_3
V : Type u_4
V' : Type u_5
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup V'
inst✝¹ : Module K V
inst✝ : Module K V'
v✝ : ι → V
s t : Set V
x y z : V
W : Submodule K V
hbot : W ≠ ⊥
h : ∀ (b : Submodule K V), b < W → b = ⊥
v : V
hW : v ∈ W
hv : v ≠ 0
⊢ W = span K {v}
[PROOFSTEP]
by_contra heq
[GOAL]
case refine'_1.intro.intro.intro
ι : Type u_1
ι' : Type u_2
K : Type u_3
V : Type u_4
V' : Type u_5
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup V'
inst✝¹ : Module K V
inst✝ : Module K V'
v✝ : ι → V
s t : Set V
x y z : V
W : Submodule K V
hbot : W ≠ ⊥
h : ∀ (b : Submodule K V), b < W → b = ⊥
v : V
hW : v ∈ W
hv : v ≠ 0
heq : ¬W = span K {v}
⊢ False
[PROOFSTEP]
specialize h (span K { v })
[GOAL]
case refine'_1.intro.intro.intro
ι : Type u_1
ι' : Type u_2
K : Type u_3
V : Type u_4
V' : Type u_5
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup V'
inst✝¹ : Module K V
inst✝ : Module K V'
v✝ : ι → V
s t : Set V
x y z : V
W : Submodule K V
hbot : W ≠ ⊥
v : V
hW : v ∈ W
hv : v ≠ 0
heq : ¬W = span K {v}
h : span K {v} < W → span K {v} = ⊥
⊢ False
[PROOFSTEP]
rw [span_singleton_eq_bot, lt_iff_le_and_ne] at h
[GOAL]
case refine'_1.intro.intro.intro
ι : Type u_1
ι' : Type u_2
K : Type u_3
V : Type u_4
V' : Type u_5
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup V'
inst✝¹ : Module K V
inst✝ : Module K V'
v✝ : ι → V
s t : Set V
x y z : V
W : Submodule K V
hbot : W ≠ ⊥
v : V
hW : v ∈ W
hv : v ≠ 0
heq : ¬W = span K {v}
h : span K {v} ≤ W ∧ span K {v} ≠ W → v = 0
⊢ False
[PROOFSTEP]
exact hv (h ⟨(span_singleton_le_iff_mem v W).2 hW, Ne.symm heq⟩)
[GOAL]
case refine'_2
ι : Type u_1
ι' : Type u_2
K : Type u_3
V : Type u_4
V' : Type u_5
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup V'
inst✝¹ : Module K V
inst✝ : Module K V'
v : ι → V
s t : Set V
x y z : V
W : Submodule K V
h : ∃ v x, W = span K {v}
⊢ IsAtom W
[PROOFSTEP]
rcases h with ⟨v, ⟨hv, rfl⟩⟩
[GOAL]
case refine'_2.intro.intro
ι : Type u_1
ι' : Type u_2
K : Type u_3
V : Type u_4
V' : Type u_5
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup V'
inst✝¹ : Module K V
inst✝ : Module K V'
v✝ : ι → V
s t : Set V
x y z v : V
hv : v ≠ 0
⊢ IsAtom (span K {v})
[PROOFSTEP]
exact nonzero_span_atom v hv
[GOAL]
ι : Type u_1
ι' : Type u_2
K : Type u_3
V : Type u_4
V' : Type u_5
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup V'
inst✝¹ : Module K V
inst✝ : Module K V'
v : ι → V
s t : Set V
x y z : V
W : Submodule K V
⊢ ∃ s, W = sSup s ∧ ∀ (a : Submodule K V), a ∈ s → IsAtom a
[PROOFSTEP]
refine ⟨_, submodule_eq_sSup_le_nonzero_spans W, ?_⟩
[GOAL]
ι : Type u_1
ι' : Type u_2
K : Type u_3
V : Type u_4
V' : Type u_5
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup V'
inst✝¹ : Module K V
inst✝ : Module K V'
v : ι → V
s t : Set V
x y z : V
W : Submodule K V
⊢ ∀ (a : Submodule K V), a ∈ {T | ∃ m x x, T = span K {m}} → IsAtom a
[PROOFSTEP]
rintro _ ⟨w, ⟨_, ⟨hw, rfl⟩⟩⟩
[GOAL]
case intro.intro.intro
ι : Type u_1
ι' : Type u_2
K : Type u_3
V : Type u_4
V' : Type u_5
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup V'
inst✝¹ : Module K V
inst✝ : Module K V'
v : ι → V
s t : Set V
x y z : V
W : Submodule K V
w : V
w✝ : w ∈ W
hw : w ≠ 0
⊢ IsAtom (span K {w})
[PROOFSTEP]
exact nonzero_span_atom w hw
[GOAL]
ι : Type u_1
ι' : Type u_2
K : Type u_3
V : Type u_4
V' : Type u_5
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup V'
inst✝¹ : Module K V
inst✝ : Module K V'
v : ι → V
s t : Set V
x y z : V
f : V →ₗ[K] V'
hf_inj : ker f = ⊥
⊢ ∃ g, comp g f = id
[PROOFSTEP]
let B := Basis.ofVectorSpaceIndex K V
[GOAL]
ι : Type u_1
ι' : Type u_2
K : Type u_3
V : Type u_4
V' : Type u_5
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup V'
inst✝¹ : Module K V
inst✝ : Module K V'
v : ι → V
s t : Set V
x y z : V
f : V →ₗ[K] V'
hf_inj : ker f = ⊥
B : Set V := Basis.ofVectorSpaceIndex K V
⊢ ∃ g, comp g f = id
[PROOFSTEP]
let hB := Basis.ofVectorSpace K V
[GOAL]
ι : Type u_1
ι' : Type u_2
K : Type u_3
V : Type u_4
V' : Type u_5
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup V'
inst✝¹ : Module K V
inst✝ : Module K V'
v : ι → V
s t : Set V
x y z : V
f : V →ₗ[K] V'
hf_inj : ker f = ⊥
B : Set V := Basis.ofVectorSpaceIndex K V
hB : Basis (↑(Basis.ofVectorSpaceIndex K V)) K V := Basis.ofVectorSpace K V
⊢ ∃ g, comp g f = id
[PROOFSTEP]
have hB₀ : _ := hB.linearIndependent.to_subtype_range
[GOAL]
ι : Type u_1
ι' : Type u_2
K : Type u_3
V : Type u_4
V' : Type u_5
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup V'
inst✝¹ : Module K V
inst✝ : Module K V'
v : ι → V
s t : Set V
x y z : V
f : V →ₗ[K] V'
hf_inj : ker f = ⊥
B : Set V := Basis.ofVectorSpaceIndex K V
hB : Basis (↑(Basis.ofVectorSpaceIndex K V)) K V := Basis.ofVectorSpace K V
hB₀ : LinearIndependent K Subtype.val
⊢ ∃ g, comp g f = id
[PROOFSTEP]
have : LinearIndependent K (fun x => x : f '' B → V') :=
  by
  have h₁ : LinearIndependent K ((↑) : ↥(f '' Set.range (Basis.ofVectorSpace K V)) → V') :=
    @LinearIndependent.image_subtype _ _ _ _ _ _ _ _ _ f hB₀ (show Disjoint _ _ by simp [hf_inj])
  rwa [Basis.range_ofVectorSpace K V] at h₁
[GOAL]
ι : Type u_1
ι' : Type u_2
K : Type u_3
V : Type u_4
V' : Type u_5
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup V'
inst✝¹ : Module K V
inst✝ : Module K V'
v : ι → V
s t : Set V
x y z : V
f : V →ₗ[K] V'
hf_inj : ker f = ⊥
B : Set V := Basis.ofVectorSpaceIndex K V
hB : Basis (↑(Basis.ofVectorSpaceIndex K V)) K V := Basis.ofVectorSpace K V
hB₀ : LinearIndependent K Subtype.val
⊢ LinearIndependent K fun x => ↑x
[PROOFSTEP]
have h₁ : LinearIndependent K ((↑) : ↥(f '' Set.range (Basis.ofVectorSpace K V)) → V') :=
  @LinearIndependent.image_subtype _ _ _ _ _ _ _ _ _ f hB₀ (show Disjoint _ _ by simp [hf_inj])
[GOAL]
ι : Type u_1
ι' : Type u_2
K : Type u_3
V : Type u_4
V' : Type u_5
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup V'
inst✝¹ : Module K V
inst✝ : Module K V'
v : ι → V
s t : Set V
x y z : V
f : V →ₗ[K] V'
hf_inj : ker f = ⊥
B : Set V := Basis.ofVectorSpaceIndex K V
hB : Basis (↑(Basis.ofVectorSpaceIndex K V)) K V := Basis.ofVectorSpace K V
hB₀ : LinearIndependent K Subtype.val
⊢ Disjoint (span K (Set.range ↑(Basis.ofVectorSpace K V))) (ker f)
[PROOFSTEP]
simp [hf_inj]
[GOAL]
ι : Type u_1
ι' : Type u_2
K : Type u_3
V : Type u_4
V' : Type u_5
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup V'
inst✝¹ : Module K V
inst✝ : Module K V'
v : ι → V
s t : Set V
x y z : V
f : V →ₗ[K] V'
hf_inj : ker f = ⊥
B : Set V := Basis.ofVectorSpaceIndex K V
hB : Basis (↑(Basis.ofVectorSpaceIndex K V)) K V := Basis.ofVectorSpace K V
hB₀ : LinearIndependent K Subtype.val
h₁ : LinearIndependent K Subtype.val
⊢ LinearIndependent K fun x => ↑x
[PROOFSTEP]
rwa [Basis.range_ofVectorSpace K V] at h₁
[GOAL]
ι : Type u_1
ι' : Type u_2
K : Type u_3
V : Type u_4
V' : Type u_5
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup V'
inst✝¹ : Module K V
inst✝ : Module K V'
v : ι → V
s t : Set V
x y z : V
f : V →ₗ[K] V'
hf_inj : ker f = ⊥
B : Set V := Basis.ofVectorSpaceIndex K V
hB : Basis (↑(Basis.ofVectorSpaceIndex K V)) K V := Basis.ofVectorSpace K V
hB₀ : LinearIndependent K Subtype.val
this : LinearIndependent K fun x => ↑x
⊢ ∃ g, comp g f = id
[PROOFSTEP]
let C := this.extend (subset_univ _)
[GOAL]
ι : Type u_1
ι' : Type u_2
K : Type u_3
V : Type u_4
V' : Type u_5
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup V'
inst✝¹ : Module K V
inst✝ : Module K V'
v : ι → V
s t : Set V
x y z : V
f : V →ₗ[K] V'
hf_inj : ker f = ⊥
B : Set V := Basis.ofVectorSpaceIndex K V
hB : Basis (↑(Basis.ofVectorSpaceIndex K V)) K V := Basis.ofVectorSpace K V
hB₀ : LinearIndependent K Subtype.val
this : LinearIndependent K fun x => ↑x
C : Set V' := LinearIndependent.extend this (_ : ↑f '' B ⊆ univ)
⊢ ∃ g, comp g f = id
[PROOFSTEP]
have BC := this.subset_extend (subset_univ _)
[GOAL]
ι : Type u_1
ι' : Type u_2
K : Type u_3
V : Type u_4
V' : Type u_5
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup V'
inst✝¹ : Module K V
inst✝ : Module K V'
v : ι → V
s t : Set V
x y z : V
f : V →ₗ[K] V'
hf_inj : ker f = ⊥
B : Set V := Basis.ofVectorSpaceIndex K V
hB : Basis (↑(Basis.ofVectorSpaceIndex K V)) K V := Basis.ofVectorSpace K V
hB₀ : LinearIndependent K Subtype.val
this : LinearIndependent K fun x => ↑x
C : Set V' := LinearIndependent.extend this (_ : ↑f '' B ⊆ univ)
BC : ↑f '' B ⊆ LinearIndependent.extend this (_ : ↑f '' B ⊆ univ)
⊢ ∃ g, comp g f = id
[PROOFSTEP]
let hC := Basis.extend this
[GOAL]
ι : Type u_1
ι' : Type u_2
K : Type u_3
V : Type u_4
V' : Type u_5
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup V'
inst✝¹ : Module K V
inst✝ : Module K V'
v : ι → V
s t : Set V
x y z : V
f : V →ₗ[K] V'
hf_inj : ker f = ⊥
B : Set V := Basis.ofVectorSpaceIndex K V
hB : Basis (↑(Basis.ofVectorSpaceIndex K V)) K V := Basis.ofVectorSpace K V
hB₀ : LinearIndependent K Subtype.val
this : LinearIndependent K fun x => ↑x
C : Set V' := LinearIndependent.extend this (_ : ↑f '' B ⊆ univ)
BC : ↑f '' B ⊆ LinearIndependent.extend this (_ : ↑f '' B ⊆ univ)
hC : Basis (↑(LinearIndependent.extend this (_ : ↑f '' B ⊆ univ))) K V' := Basis.extend this
⊢ ∃ g, comp g f = id
[PROOFSTEP]
haveI Vinh : Inhabited V := ⟨0⟩
[GOAL]
ι : Type u_1
ι' : Type u_2
K : Type u_3
V : Type u_4
V' : Type u_5
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup V'
inst✝¹ : Module K V
inst✝ : Module K V'
v : ι → V
s t : Set V
x y z : V
f : V →ₗ[K] V'
hf_inj : ker f = ⊥
B : Set V := Basis.ofVectorSpaceIndex K V
hB : Basis (↑(Basis.ofVectorSpaceIndex K V)) K V := Basis.ofVectorSpace K V
hB₀ : LinearIndependent K Subtype.val
this : LinearIndependent K fun x => ↑x
C : Set V' := LinearIndependent.extend this (_ : ↑f '' B ⊆ univ)
BC : ↑f '' B ⊆ LinearIndependent.extend this (_ : ↑f '' B ⊆ univ)
hC : Basis (↑(LinearIndependent.extend this (_ : ↑f '' B ⊆ univ))) K V' := Basis.extend this
Vinh : Inhabited V
⊢ ∃ g, comp g f = id
[PROOFSTEP]
refine' ⟨(hC.constr ℕ : _ → _) (C.restrict (invFun f)), hB.ext fun b => _⟩
[GOAL]
ι : Type u_1
ι' : Type u_2
K : Type u_3
V : Type u_4
V' : Type u_5
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup V'
inst✝¹ : Module K V
inst✝ : Module K V'
v : ι → V
s t : Set V
x y z : V
f : V →ₗ[K] V'
hf_inj : ker f = ⊥
B : Set V := Basis.ofVectorSpaceIndex K V
hB : Basis (↑(Basis.ofVectorSpaceIndex K V)) K V := Basis.ofVectorSpace K V
hB₀ : LinearIndependent K Subtype.val
this : LinearIndependent K fun x => ↑x
C : Set V' := LinearIndependent.extend this (_ : ↑f '' B ⊆ univ)
BC : ↑f '' B ⊆ LinearIndependent.extend this (_ : ↑f '' B ⊆ univ)
hC : Basis (↑(LinearIndependent.extend this (_ : ↑f '' B ⊆ univ))) K V' := Basis.extend this
Vinh : Inhabited V
b : ↑(Basis.ofVectorSpaceIndex K V)
⊢ ↑(comp (↑(Basis.constr hC ℕ) (Set.restrict C (invFun ↑f))) f) (↑hB b) = ↑id (↑hB b)
[PROOFSTEP]
rw [image_subset_iff] at BC
[GOAL]
ι : Type u_1
ι' : Type u_2
K : Type u_3
V : Type u_4
V' : Type u_5
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup V'
inst✝¹ : Module K V
inst✝ : Module K V'
v : ι → V
s t : Set V
x y z : V
f : V →ₗ[K] V'
hf_inj : ker f = ⊥
B : Set V := Basis.ofVectorSpaceIndex K V
hB : Basis (↑(Basis.ofVectorSpaceIndex K V)) K V := Basis.ofVectorSpace K V
hB₀ : LinearIndependent K Subtype.val
this : LinearIndependent K fun x => ↑x
C : Set V' := LinearIndependent.extend this (_ : ↑f '' B ⊆ univ)
BC : B ⊆ ↑f ⁻¹' LinearIndependent.extend this (_ : ↑f '' B ⊆ univ)
hC : Basis (↑(LinearIndependent.extend this (_ : ↑f '' B ⊆ univ))) K V' := Basis.extend this
Vinh : Inhabited V
b : ↑(Basis.ofVectorSpaceIndex K V)
⊢ ↑(comp (↑(Basis.constr hC ℕ) (Set.restrict C (invFun ↑f))) f) (↑hB b) = ↑id (↑hB b)
[PROOFSTEP]
have fb_eq : f b = hC ⟨f b, BC b.2⟩ := by
  change f b = Basis.extend this _
  simp_rw [Basis.extend_apply_self]
[GOAL]
ι : Type u_1
ι' : Type u_2
K : Type u_3
V : Type u_4
V' : Type u_5
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup V'
inst✝¹ : Module K V
inst✝ : Module K V'
v : ι → V
s t : Set V
x y z : V
f : V →ₗ[K] V'
hf_inj : ker f = ⊥
B : Set V := Basis.ofVectorSpaceIndex K V
hB : Basis (↑(Basis.ofVectorSpaceIndex K V)) K V := Basis.ofVectorSpace K V
hB₀ : LinearIndependent K Subtype.val
this : LinearIndependent K fun x => ↑x
C : Set V' := LinearIndependent.extend this (_ : ↑f '' B ⊆ univ)
BC : B ⊆ ↑f ⁻¹' LinearIndependent.extend this (_ : ↑f '' B ⊆ univ)
hC : Basis (↑(LinearIndependent.extend this (_ : ↑f '' B ⊆ univ))) K V' := Basis.extend this
Vinh : Inhabited V
b : ↑(Basis.ofVectorSpaceIndex K V)
⊢ ↑f ↑b = ↑hC { val := ↑f ↑b, property := (_ : ↑b ∈ ↑f ⁻¹' LinearIndependent.extend this (_ : ↑f '' B ⊆ univ)) }
[PROOFSTEP]
change f b = Basis.extend this _
[GOAL]
ι : Type u_1
ι' : Type u_2
K : Type u_3
V : Type u_4
V' : Type u_5
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup V'
inst✝¹ : Module K V
inst✝ : Module K V'
v : ι → V
s t : Set V
x y z : V
f : V →ₗ[K] V'
hf_inj : ker f = ⊥
B : Set V := Basis.ofVectorSpaceIndex K V
hB : Basis (↑(Basis.ofVectorSpaceIndex K V)) K V := Basis.ofVectorSpace K V
hB₀ : LinearIndependent K Subtype.val
this : LinearIndependent K fun x => ↑x
C : Set V' := LinearIndependent.extend this (_ : ↑f '' B ⊆ univ)
BC : B ⊆ ↑f ⁻¹' LinearIndependent.extend this (_ : ↑f '' B ⊆ univ)
hC : Basis (↑(LinearIndependent.extend this (_ : ↑f '' B ⊆ univ))) K V' := Basis.extend this
Vinh : Inhabited V
b : ↑(Basis.ofVectorSpaceIndex K V)
⊢ ↑f ↑b =
    ↑(Basis.extend this)
      { val := ↑f ↑b, property := (_ : ↑b ∈ ↑f ⁻¹' LinearIndependent.extend this (_ : ↑f '' B ⊆ univ)) }
[PROOFSTEP]
simp_rw [Basis.extend_apply_self]
[GOAL]
ι : Type u_1
ι' : Type u_2
K : Type u_3
V : Type u_4
V' : Type u_5
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup V'
inst✝¹ : Module K V
inst✝ : Module K V'
v : ι → V
s t : Set V
x y z : V
f : V →ₗ[K] V'
hf_inj : ker f = ⊥
B : Set V := Basis.ofVectorSpaceIndex K V
hB : Basis (↑(Basis.ofVectorSpaceIndex K V)) K V := Basis.ofVectorSpace K V
hB₀ : LinearIndependent K Subtype.val
this : LinearIndependent K fun x => ↑x
C : Set V' := LinearIndependent.extend this (_ : ↑f '' B ⊆ univ)
BC : B ⊆ ↑f ⁻¹' LinearIndependent.extend this (_ : ↑f '' B ⊆ univ)
hC : Basis (↑(LinearIndependent.extend this (_ : ↑f '' B ⊆ univ))) K V' := Basis.extend this
Vinh : Inhabited V
b : ↑(Basis.ofVectorSpaceIndex K V)
fb_eq : ↑f ↑b = ↑hC { val := ↑f ↑b, property := (_ : ↑b ∈ ↑f ⁻¹' LinearIndependent.extend this (_ : ↑f '' B ⊆ univ)) }
⊢ ↑(comp (↑(Basis.constr hC ℕ) (Set.restrict C (invFun ↑f))) f) (↑hB b) = ↑id (↑hB b)
[PROOFSTEP]
dsimp []
[GOAL]
ι : Type u_1
ι' : Type u_2
K : Type u_3
V : Type u_4
V' : Type u_5
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup V'
inst✝¹ : Module K V
inst✝ : Module K V'
v : ι → V
s t : Set V
x y z : V
f : V →ₗ[K] V'
hf_inj : ker f = ⊥
B : Set V := Basis.ofVectorSpaceIndex K V
hB : Basis (↑(Basis.ofVectorSpaceIndex K V)) K V := Basis.ofVectorSpace K V
hB₀ : LinearIndependent K Subtype.val
this : LinearIndependent K fun x => ↑x
C : Set V' := LinearIndependent.extend this (_ : ↑f '' B ⊆ univ)
BC : B ⊆ ↑f ⁻¹' LinearIndependent.extend this (_ : ↑f '' B ⊆ univ)
hC : Basis (↑(LinearIndependent.extend this (_ : ↑f '' B ⊆ univ))) K V' := Basis.extend this
Vinh : Inhabited V
b : ↑(Basis.ofVectorSpaceIndex K V)
fb_eq : ↑f ↑b = ↑hC { val := ↑f ↑b, property := (_ : ↑b ∈ ↑f ⁻¹' LinearIndependent.extend this (_ : ↑f '' B ⊆ univ)) }
⊢ ↑(↑(Basis.constr (Basis.extend this) ℕ)
          (Set.restrict (LinearIndependent.extend this (_ : ↑f '' Basis.ofVectorSpaceIndex K V ⊆ univ)) (invFun ↑f)))
      (↑f (↑(Basis.ofVectorSpace K V) b)) =
    ↑(Basis.ofVectorSpace K V) b
[PROOFSTEP]
rw [Basis.ofVectorSpace_apply_self, fb_eq, hC.constr_basis]
[GOAL]
ι : Type u_1
ι' : Type u_2
K : Type u_3
V : Type u_4
V' : Type u_5
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup V'
inst✝¹ : Module K V
inst✝ : Module K V'
v : ι → V
s t : Set V
x y z : V
f : V →ₗ[K] V'
hf_inj : ker f = ⊥
B : Set V := Basis.ofVectorSpaceIndex K V
hB : Basis (↑(Basis.ofVectorSpaceIndex K V)) K V := Basis.ofVectorSpace K V
hB₀ : LinearIndependent K Subtype.val
this : LinearIndependent K fun x => ↑x
C : Set V' := LinearIndependent.extend this (_ : ↑f '' B ⊆ univ)
BC : B ⊆ ↑f ⁻¹' LinearIndependent.extend this (_ : ↑f '' B ⊆ univ)
hC : Basis (↑(LinearIndependent.extend this (_ : ↑f '' B ⊆ univ))) K V' := Basis.extend this
Vinh : Inhabited V
b : ↑(Basis.ofVectorSpaceIndex K V)
fb_eq : ↑f ↑b = ↑hC { val := ↑f ↑b, property := (_ : ↑b ∈ ↑f ⁻¹' LinearIndependent.extend this (_ : ↑f '' B ⊆ univ)) }
⊢ Set.restrict (LinearIndependent.extend this (_ : ↑f '' Basis.ofVectorSpaceIndex K V ⊆ univ)) (invFun ↑f)
      { val := ↑f ↑b, property := (_ : ↑b ∈ ↑f ⁻¹' LinearIndependent.extend this (_ : ↑f '' B ⊆ univ)) } =
    ↑b
[PROOFSTEP]
exact leftInverse_invFun (LinearMap.ker_eq_bot.1 hf_inj) _
[GOAL]
ι : Type u_1
ι' : Type u_2
K : Type u_3
V : Type u_4
V' : Type u_5
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup V'
inst✝¹ : Module K V
inst✝ : Module K V'
v : ι → V
s t : Set V
x y z : V
f : V →ₗ[K] V'
hf_surj : range f = ⊤
⊢ ∃ g, comp f g = id
[PROOFSTEP]
let C := Basis.ofVectorSpaceIndex K V'
[GOAL]
ι : Type u_1
ι' : Type u_2
K : Type u_3
V : Type u_4
V' : Type u_5
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup V'
inst✝¹ : Module K V
inst✝ : Module K V'
v : ι → V
s t : Set V
x y z : V
f : V →ₗ[K] V'
hf_surj : range f = ⊤
C : Set V' := Basis.ofVectorSpaceIndex K V'
⊢ ∃ g, comp f g = id
[PROOFSTEP]
let hC := Basis.ofVectorSpace K V'
[GOAL]
ι : Type u_1
ι' : Type u_2
K : Type u_3
V : Type u_4
V' : Type u_5
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup V'
inst✝¹ : Module K V
inst✝ : Module K V'
v : ι → V
s t : Set V
x y z : V
f : V →ₗ[K] V'
hf_surj : range f = ⊤
C : Set V' := Basis.ofVectorSpaceIndex K V'
hC : Basis (↑(Basis.ofVectorSpaceIndex K V')) K V' := Basis.ofVectorSpace K V'
⊢ ∃ g, comp f g = id
[PROOFSTEP]
haveI : Inhabited V := ⟨0⟩
[GOAL]
ι : Type u_1
ι' : Type u_2
K : Type u_3
V : Type u_4
V' : Type u_5
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup V'
inst✝¹ : Module K V
inst✝ : Module K V'
v : ι → V
s t : Set V
x y z : V
f : V →ₗ[K] V'
hf_surj : range f = ⊤
C : Set V' := Basis.ofVectorSpaceIndex K V'
hC : Basis (↑(Basis.ofVectorSpaceIndex K V')) K V' := Basis.ofVectorSpace K V'
this : Inhabited V
⊢ ∃ g, comp f g = id
[PROOFSTEP]
refine' ⟨(hC.constr ℕ : _ → _) (C.restrict (invFun f)), hC.ext fun c => _⟩
[GOAL]
ι : Type u_1
ι' : Type u_2
K : Type u_3
V : Type u_4
V' : Type u_5
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup V'
inst✝¹ : Module K V
inst✝ : Module K V'
v : ι → V
s t : Set V
x y z : V
f : V →ₗ[K] V'
hf_surj : range f = ⊤
C : Set V' := Basis.ofVectorSpaceIndex K V'
hC : Basis (↑(Basis.ofVectorSpaceIndex K V')) K V' := Basis.ofVectorSpace K V'
this : Inhabited V
c : ↑(Basis.ofVectorSpaceIndex K V')
⊢ ↑(comp f (↑(Basis.constr hC ℕ) (Set.restrict C (invFun ↑f)))) (↑hC c) = ↑id (↑hC c)
[PROOFSTEP]
rw [LinearMap.comp_apply, hC.constr_basis]
[GOAL]
ι : Type u_1
ι' : Type u_2
K : Type u_3
V : Type u_4
V' : Type u_5
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup V'
inst✝¹ : Module K V
inst✝ : Module K V'
v : ι → V
s t : Set V
x y z : V
f : V →ₗ[K] V'
hf_surj : range f = ⊤
C : Set V' := Basis.ofVectorSpaceIndex K V'
hC : Basis (↑(Basis.ofVectorSpaceIndex K V')) K V' := Basis.ofVectorSpace K V'
this : Inhabited V
c : ↑(Basis.ofVectorSpaceIndex K V')
⊢ ↑f (Set.restrict C (invFun ↑f) c) = ↑id (↑hC c)
[PROOFSTEP]
simp [rightInverse_invFun (LinearMap.range_eq_top.1 hf_surj) c]
[GOAL]
ι : Type u_1
ι' : Type u_2
K : Type u_3
V : Type u_4
V' : Type u_5
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup V'
inst✝¹ : Module K V
inst✝ : Module K V'
v : ι → V
s t : Set V
x y z : V
p : Submodule K V
f : { x // x ∈ p } →ₗ[K] V'
g : V →ₗ[K] { x // x ∈ p }
hg : comp g (Submodule.subtype p) = id
⊢ comp (comp f g) (Submodule.subtype p) = f
[PROOFSTEP]
rw [LinearMap.comp_assoc, hg, f.comp_id]
[GOAL]
ι : Type u_1
ι' : Type u_2
K : Type u_3
V : Type u_4
V' : Type u_5
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup V'
inst✝¹ : Module K V
inst✝ : Module K V'
v : ι → V
s t : Set V
x y z : V
p : Submodule K V
hp : p < ⊤
⊢ ∃ f, f ≠ 0 ∧ p ≤ ker f
[PROOFSTEP]
rcases SetLike.exists_of_lt hp with ⟨v, -, hpv⟩
[GOAL]
case intro.intro
ι : Type u_1
ι' : Type u_2
K : Type u_3
V : Type u_4
V' : Type u_5
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup V'
inst✝¹ : Module K V
inst✝ : Module K V'
v✝ : ι → V
s t : Set V
x y z : V
p : Submodule K V
hp : p < ⊤
v : V
hpv : ¬v ∈ p
⊢ ∃ f, f ≠ 0 ∧ p ≤ ker f
[PROOFSTEP]
clear hp
[GOAL]
case intro.intro
ι : Type u_1
ι' : Type u_2
K : Type u_3
V : Type u_4
V' : Type u_5
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup V'
inst✝¹ : Module K V
inst✝ : Module K V'
v✝ : ι → V
s t : Set V
x y z : V
p : Submodule K V
v : V
hpv : ¬v ∈ p
⊢ ∃ f, f ≠ 0 ∧ p ≤ ker f
[PROOFSTEP]
rcases(LinearPMap.supSpanSingleton ⟨p, 0⟩ v (1 : K) hpv).toFun.exists_extend with ⟨f, hf⟩
[GOAL]
case intro.intro.intro
ι : Type u_1
ι' : Type u_2
K : Type u_3
V : Type u_4
V' : Type u_5
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup V'
inst✝¹ : Module K V
inst✝ : Module K V'
v✝ : ι → V
s t : Set V
x y z : V
p : Submodule K V
v : V
hpv : ¬v ∈ p
f : V →ₗ[K] K
hf :
  LinearMap.comp f (Submodule.subtype (LinearPMap.supSpanSingleton { domain := p, toFun := 0 } v 1 hpv).domain) =
    (LinearPMap.supSpanSingleton { domain := p, toFun := 0 } v 1 hpv).toFun
⊢ ∃ f, f ≠ 0 ∧ p ≤ ker f
[PROOFSTEP]
refine' ⟨f, _, _⟩
[GOAL]
case intro.intro.intro.refine'_1
ι : Type u_1
ι' : Type u_2
K : Type u_3
V : Type u_4
V' : Type u_5
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup V'
inst✝¹ : Module K V
inst✝ : Module K V'
v✝ : ι → V
s t : Set V
x y z : V
p : Submodule K V
v : V
hpv : ¬v ∈ p
f : V →ₗ[K] K
hf :
  LinearMap.comp f (Submodule.subtype (LinearPMap.supSpanSingleton { domain := p, toFun := 0 } v 1 hpv).domain) =
    (LinearPMap.supSpanSingleton { domain := p, toFun := 0 } v 1 hpv).toFun
⊢ f ≠ 0
[PROOFSTEP]
rintro rfl
[GOAL]
case intro.intro.intro.refine'_1
ι : Type u_1
ι' : Type u_2
K : Type u_3
V : Type u_4
V' : Type u_5
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup V'
inst✝¹ : Module K V
inst✝ : Module K V'
v✝ : ι → V
s t : Set V
x y z : V
p : Submodule K V
v : V
hpv : ¬v ∈ p
hf :
  LinearMap.comp 0 (Submodule.subtype (LinearPMap.supSpanSingleton { domain := p, toFun := 0 } v 1 hpv).domain) =
    (LinearPMap.supSpanSingleton { domain := p, toFun := 0 } v 1 hpv).toFun
⊢ False
[PROOFSTEP]
rw [LinearMap.zero_comp] at hf
[GOAL]
case intro.intro.intro.refine'_1
ι : Type u_1
ι' : Type u_2
K : Type u_3
V : Type u_4
V' : Type u_5
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup V'
inst✝¹ : Module K V
inst✝ : Module K V'
v✝ : ι → V
s t : Set V
x y z : V
p : Submodule K V
v : V
hpv : ¬v ∈ p
hf : 0 = (LinearPMap.supSpanSingleton { domain := p, toFun := 0 } v 1 hpv).toFun
⊢ False
[PROOFSTEP]
have := LinearPMap.supSpanSingleton_apply_mk ⟨p, 0⟩ v (1 : K) hpv 0 p.zero_mem 1
[GOAL]
case intro.intro.intro.refine'_1
ι : Type u_1
ι' : Type u_2
K : Type u_3
V : Type u_4
V' : Type u_5
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup V'
inst✝¹ : Module K V
inst✝ : Module K V'
v✝ : ι → V
s t : Set V
x y z : V
p : Submodule K V
v : V
hpv : ¬v ∈ p
hf : 0 = (LinearPMap.supSpanSingleton { domain := p, toFun := 0 } v 1 hpv).toFun
this :
  ↑(LinearPMap.supSpanSingleton { domain := p, toFun := 0 } v 1 hpv)
      { val := 0 + 1 • v,
        property :=
          (_ :
            0 + 1 • v ∈
              { domain := p, toFun := 0 }.domain ⊔ (LinearPMap.mkSpanSingleton v 1 (_ : v = 0 → False)).domain) } =
    ↑{ domain := p, toFun := 0 } { val := 0, property := (_ : 0 ∈ p) } + 1 • 1
⊢ False
[PROOFSTEP]
simpa using (LinearMap.congr_fun hf _).trans this
[GOAL]
case intro.intro.intro.refine'_2
ι : Type u_1
ι' : Type u_2
K : Type u_3
V : Type u_4
V' : Type u_5
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup V'
inst✝¹ : Module K V
inst✝ : Module K V'
v✝ : ι → V
s t : Set V
x y z : V
p : Submodule K V
v : V
hpv : ¬v ∈ p
f : V →ₗ[K] K
hf :
  LinearMap.comp f (Submodule.subtype (LinearPMap.supSpanSingleton { domain := p, toFun := 0 } v 1 hpv).domain) =
    (LinearPMap.supSpanSingleton { domain := p, toFun := 0 } v 1 hpv).toFun
⊢ p ≤ ker f
[PROOFSTEP]
refine' fun x hx => mem_ker.2 _
[GOAL]
case intro.intro.intro.refine'_2
ι : Type u_1
ι' : Type u_2
K : Type u_3
V : Type u_4
V' : Type u_5
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup V'
inst✝¹ : Module K V
inst✝ : Module K V'
v✝ : ι → V
s t : Set V
x✝ y z : V
p : Submodule K V
v : V
hpv : ¬v ∈ p
f : V →ₗ[K] K
hf :
  LinearMap.comp f (Submodule.subtype (LinearPMap.supSpanSingleton { domain := p, toFun := 0 } v 1 hpv).domain) =
    (LinearPMap.supSpanSingleton { domain := p, toFun := 0 } v 1 hpv).toFun
x : V
hx : x ∈ p
⊢ ↑f x = 0
[PROOFSTEP]
have := LinearPMap.supSpanSingleton_apply_mk ⟨p, 0⟩ v (1 : K) hpv x hx 0
[GOAL]
case intro.intro.intro.refine'_2
ι : Type u_1
ι' : Type u_2
K : Type u_3
V : Type u_4
V' : Type u_5
inst✝⁴ : DivisionRing K
inst✝³ : AddCommGroup V
inst✝² : AddCommGroup V'
inst✝¹ : Module K V
inst✝ : Module K V'
v✝ : ι → V
s t : Set V
x✝ y z : V
p : Submodule K V
v : V
hpv : ¬v ∈ p
f : V →ₗ[K] K
hf :
  LinearMap.comp f (Submodule.subtype (LinearPMap.supSpanSingleton { domain := p, toFun := 0 } v 1 hpv).domain) =
    (LinearPMap.supSpanSingleton { domain := p, toFun := 0 } v 1 hpv).toFun
x : V
hx : x ∈ p
this :
  ↑(LinearPMap.supSpanSingleton { domain := p, toFun := 0 } v 1 hpv)
      { val := x + 0 • v,
        property :=
          (_ :
            x + 0 • v ∈
              { domain := p, toFun := 0 }.domain ⊔ (LinearPMap.mkSpanSingleton v 1 (_ : v = 0 → False)).domain) } =
    ↑{ domain := p, toFun := 0 } { val := x, property := hx } + 0 • 1
⊢ ↑f x = 0
[PROOFSTEP]
simpa using (LinearMap.congr_fun hf _).trans this


[GOAL]
ι : Type u_1
inst✝⁴ : Fintype ι
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_3
inst✝² : CommRing R
inst✝¹ : Module R M
I : Ideal R
b : ι → M
hb : Submodule.span R (Set.range b) = ⊤
inst✝ : DecidableEq ι
A : Matrix ι ι R
j : ι
⊢ ↑(↑(fromMatrix R b) A) (Pi.single j 1) = ∑ i : ι, A i j • b i
[PROOFSTEP]
rw [PiToModule.fromMatrix_apply, Fintype.total_apply, Matrix.mulVec_single]
[GOAL]
ι : Type u_1
inst✝⁴ : Fintype ι
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_3
inst✝² : CommRing R
inst✝¹ : Module R M
I : Ideal R
b : ι → M
hb : Submodule.span R (Set.range b) = ⊤
inst✝ : DecidableEq ι
A : Matrix ι ι R
j : ι
⊢ ∑ i : ι, (fun i => A i j * 1) i • b i = ∑ i : ι, A i j • b i
[PROOFSTEP]
simp_rw [mul_one]
[GOAL]
ι : Type u_1
inst✝⁴ : Fintype ι
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_3
inst✝² : CommRing R
inst✝¹ : Module R M
I : Ideal R
b : ι → M
hb : Submodule.span R (Set.range b) = ⊤
inst✝ : DecidableEq ι
f : Module.End R M
i : ι
⊢ ↑(↑(fromEnd R b) f) (Pi.single i 1) = ↑f (b i)
[PROOFSTEP]
rw [PiToModule.fromEnd_apply]
[GOAL]
ι : Type u_1
inst✝⁴ : Fintype ι
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_3
inst✝² : CommRing R
inst✝¹ : Module R M
I : Ideal R
b : ι → M
hb : Submodule.span R (Set.range b) = ⊤
inst✝ : DecidableEq ι
f : Module.End R M
i : ι
⊢ ↑f (↑(↑(Fintype.total R R) b) (Pi.single i 1)) = ↑f (b i)
[PROOFSTEP]
congr
[GOAL]
case h.e_6.h
ι : Type u_1
inst✝⁴ : Fintype ι
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_3
inst✝² : CommRing R
inst✝¹ : Module R M
I : Ideal R
b : ι → M
hb : Submodule.span R (Set.range b) = ⊤
inst✝ : DecidableEq ι
f : Module.End R M
i : ι
⊢ ↑(↑(Fintype.total R R) b) (Pi.single i 1) = b i
[PROOFSTEP]
convert Fintype.total_apply_single (S := R) R b i (1 : R)
[GOAL]
case h.e'_3
ι : Type u_1
inst✝⁴ : Fintype ι
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_3
inst✝² : CommRing R
inst✝¹ : Module R M
I : Ideal R
b : ι → M
hb : Submodule.span R (Set.range b) = ⊤
inst✝ : DecidableEq ι
f : Module.End R M
i : ι
⊢ b i = 1 • b i
[PROOFSTEP]
rw [one_smul]
[GOAL]
ι : Type u_1
inst✝³ : Fintype ι
M : Type u_2
inst✝² : AddCommGroup M
R : Type u_3
inst✝¹ : CommRing R
inst✝ : Module R M
I : Ideal R
b : ι → M
hb✝ hb : Submodule.span R (Set.range b) = ⊤
⊢ Function.Injective ↑(fromEnd R b)
[PROOFSTEP]
intro x y e
[GOAL]
ι : Type u_1
inst✝³ : Fintype ι
M : Type u_2
inst✝² : AddCommGroup M
R : Type u_3
inst✝¹ : CommRing R
inst✝ : Module R M
I : Ideal R
b : ι → M
hb✝ hb : Submodule.span R (Set.range b) = ⊤
x y : Module.End R M
e : ↑(fromEnd R b) x = ↑(fromEnd R b) y
⊢ x = y
[PROOFSTEP]
ext m
[GOAL]
case h
ι : Type u_1
inst✝³ : Fintype ι
M : Type u_2
inst✝² : AddCommGroup M
R : Type u_3
inst✝¹ : CommRing R
inst✝ : Module R M
I : Ideal R
b : ι → M
hb✝ hb : Submodule.span R (Set.range b) = ⊤
x y : Module.End R M
e : ↑(fromEnd R b) x = ↑(fromEnd R b) y
m : M
⊢ ↑x m = ↑y m
[PROOFSTEP]
obtain ⟨m, rfl⟩ : m ∈ LinearMap.range (Fintype.total R R b) :=
  by
  rw [(Fintype.range_total R b).trans hb]
  exact Submodule.mem_top
[GOAL]
ι : Type u_1
inst✝³ : Fintype ι
M : Type u_2
inst✝² : AddCommGroup M
R : Type u_3
inst✝¹ : CommRing R
inst✝ : Module R M
I : Ideal R
b : ι → M
hb✝ hb : Submodule.span R (Set.range b) = ⊤
x y : Module.End R M
e : ↑(fromEnd R b) x = ↑(fromEnd R b) y
m : M
⊢ m ∈ LinearMap.range (↑(Fintype.total R R) b)
[PROOFSTEP]
rw [(Fintype.range_total R b).trans hb]
[GOAL]
ι : Type u_1
inst✝³ : Fintype ι
M : Type u_2
inst✝² : AddCommGroup M
R : Type u_3
inst✝¹ : CommRing R
inst✝ : Module R M
I : Ideal R
b : ι → M
hb✝ hb : Submodule.span R (Set.range b) = ⊤
x y : Module.End R M
e : ↑(fromEnd R b) x = ↑(fromEnd R b) y
m : M
⊢ m ∈ ⊤
[PROOFSTEP]
exact Submodule.mem_top
[GOAL]
case h.intro
ι : Type u_1
inst✝³ : Fintype ι
M : Type u_2
inst✝² : AddCommGroup M
R : Type u_3
inst✝¹ : CommRing R
inst✝ : Module R M
I : Ideal R
b : ι → M
hb✝ hb : Submodule.span R (Set.range b) = ⊤
x y : Module.End R M
e : ↑(fromEnd R b) x = ↑(fromEnd R b) y
m : ι → R
⊢ ↑x (↑(↑(Fintype.total R R) b) m) = ↑y (↑(↑(Fintype.total R R) b) m)
[PROOFSTEP]
exact (LinearMap.congr_fun e m : _)
[GOAL]
ι : Type u_1
inst✝⁴ : Fintype ι
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_3
inst✝² : CommRing R
inst✝¹ : Module R M
I : Ideal R
b : ι → M
hb : Submodule.span R (Set.range b) = ⊤
inst✝ : DecidableEq ι
A : Matrix ι ι R
f : Module.End R M
⊢ Represents b A f ↔ ∀ (j : ι), ∑ i : ι, A i j • b i = ↑f (b j)
[PROOFSTEP]
constructor
[GOAL]
case mp
ι : Type u_1
inst✝⁴ : Fintype ι
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_3
inst✝² : CommRing R
inst✝¹ : Module R M
I : Ideal R
b : ι → M
hb : Submodule.span R (Set.range b) = ⊤
inst✝ : DecidableEq ι
A : Matrix ι ι R
f : Module.End R M
⊢ Represents b A f → ∀ (j : ι), ∑ i : ι, A i j • b i = ↑f (b j)
[PROOFSTEP]
intro h i
[GOAL]
case mp
ι : Type u_1
inst✝⁴ : Fintype ι
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_3
inst✝² : CommRing R
inst✝¹ : Module R M
I : Ideal R
b : ι → M
hb : Submodule.span R (Set.range b) = ⊤
inst✝ : DecidableEq ι
A : Matrix ι ι R
f : Module.End R M
h : Represents b A f
i : ι
⊢ ∑ i_1 : ι, A i_1 i • b i_1 = ↑f (b i)
[PROOFSTEP]
have := LinearMap.congr_fun h (Pi.single i 1)
[GOAL]
case mp
ι : Type u_1
inst✝⁴ : Fintype ι
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_3
inst✝² : CommRing R
inst✝¹ : Module R M
I : Ideal R
b : ι → M
hb : Submodule.span R (Set.range b) = ⊤
inst✝ : DecidableEq ι
A : Matrix ι ι R
f : Module.End R M
h : Represents b A f
i : ι
this : ↑(↑(PiToModule.fromMatrix R b) A) (Pi.single i 1) = ↑(↑(PiToModule.fromEnd R b) f) (Pi.single i 1)
⊢ ∑ i_1 : ι, A i_1 i • b i_1 = ↑f (b i)
[PROOFSTEP]
rwa [PiToModule.fromEnd_apply_single_one, PiToModule.fromMatrix_apply_single_one] at this
[GOAL]
case mpr
ι : Type u_1
inst✝⁴ : Fintype ι
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_3
inst✝² : CommRing R
inst✝¹ : Module R M
I : Ideal R
b : ι → M
hb : Submodule.span R (Set.range b) = ⊤
inst✝ : DecidableEq ι
A : Matrix ι ι R
f : Module.End R M
⊢ (∀ (j : ι), ∑ i : ι, A i j • b i = ↑f (b j)) → Represents b A f
[PROOFSTEP]
intro h
[GOAL]
case mpr
ι : Type u_1
inst✝⁴ : Fintype ι
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_3
inst✝² : CommRing R
inst✝¹ : Module R M
I : Ideal R
b : ι → M
hb : Submodule.span R (Set.range b) = ⊤
inst✝ : DecidableEq ι
A : Matrix ι ι R
f : Module.End R M
h : ∀ (j : ι), ∑ i : ι, A i j • b i = ↑f (b j)
⊢ Represents b A f
[PROOFSTEP]
refine LinearMap.pi_ext' (fun i => LinearMap.ext_ring ?_)
[GOAL]
case mpr
ι : Type u_1
inst✝⁴ : Fintype ι
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_3
inst✝² : CommRing R
inst✝¹ : Module R M
I : Ideal R
b : ι → M
hb : Submodule.span R (Set.range b) = ⊤
inst✝ : DecidableEq ι
A : Matrix ι ι R
f : Module.End R M
h : ∀ (j : ι), ∑ i : ι, A i j • b i = ↑f (b j)
i : ι
⊢ ↑(LinearMap.comp (↑(PiToModule.fromMatrix R b) A) (LinearMap.single i)) 1 =
    ↑(LinearMap.comp (↑(PiToModule.fromEnd R b) f) (LinearMap.single i)) 1
[PROOFSTEP]
simp_rw [LinearMap.comp_apply, LinearMap.coe_single, PiToModule.fromEnd_apply_single_one,
  PiToModule.fromMatrix_apply_single_one]
[GOAL]
case mpr
ι : Type u_1
inst✝⁴ : Fintype ι
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_3
inst✝² : CommRing R
inst✝¹ : Module R M
I : Ideal R
b : ι → M
hb : Submodule.span R (Set.range b) = ⊤
inst✝ : DecidableEq ι
A : Matrix ι ι R
f : Module.End R M
h : ∀ (j : ι), ∑ i : ι, A i j • b i = ↑f (b j)
i : ι
⊢ ∑ i_1 : ι, A i_1 i • b i_1 = ↑f (b i)
[PROOFSTEP]
apply h
[GOAL]
ι : Type u_1
inst✝⁴ : Fintype ι
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_3
inst✝² : CommRing R
inst✝¹ : Module R M
I : Ideal R
b : ι → M
hb : Submodule.span R (Set.range b) = ⊤
inst✝ : DecidableEq ι
A A' : Matrix ι ι R
f f' : Module.End R M
h : Represents b A f
h' : Represents b A' f'
⊢ Represents b (A * A') (f * f')
[PROOFSTEP]
delta Matrix.Represents PiToModule.fromMatrix
[GOAL]
ι : Type u_1
inst✝⁴ : Fintype ι
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_3
inst✝² : CommRing R
inst✝¹ : Module R M
I : Ideal R
b : ι → M
hb : Submodule.span R (Set.range b) = ⊤
inst✝ : DecidableEq ι
A A' : Matrix ι ι R
f f' : Module.End R M
h : Represents b A f
h' : Represents b A' f'
⊢ ↑(LinearMap.comp (↑(LinearMap.llcomp R (ι → R) (ι → R) M) (↑(Fintype.total R R) b))
          (AlgEquiv.toLinearMap (AlgEquiv.symm algEquivMatrix')))
      (A * A') =
    ↑(PiToModule.fromEnd R b) (f * f')
[PROOFSTEP]
rw [LinearMap.comp_apply, AlgEquiv.toLinearMap_apply, _root_.map_mul]
[GOAL]
ι : Type u_1
inst✝⁴ : Fintype ι
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_3
inst✝² : CommRing R
inst✝¹ : Module R M
I : Ideal R
b : ι → M
hb : Submodule.span R (Set.range b) = ⊤
inst✝ : DecidableEq ι
A A' : Matrix ι ι R
f f' : Module.End R M
h : Represents b A f
h' : Represents b A' f'
⊢ ↑(↑(LinearMap.llcomp R (ι → R) (ι → R) M) (↑(Fintype.total R R) b))
      (↑(AlgEquiv.symm algEquivMatrix') A * ↑(AlgEquiv.symm algEquivMatrix') A') =
    ↑(PiToModule.fromEnd R b) (f * f')
[PROOFSTEP]
ext
[GOAL]
case h.h
ι : Type u_1
inst✝⁴ : Fintype ι
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_3
inst✝² : CommRing R
inst✝¹ : Module R M
I : Ideal R
b : ι → M
hb : Submodule.span R (Set.range b) = ⊤
inst✝ : DecidableEq ι
A A' : Matrix ι ι R
f f' : Module.End R M
h : Represents b A f
h' : Represents b A' f'
i✝ : ι
⊢ ↑(LinearMap.comp
          (↑(↑(LinearMap.llcomp R (ι → R) (ι → R) M) (↑(Fintype.total R R) b))
            (↑(AlgEquiv.symm algEquivMatrix') A * ↑(AlgEquiv.symm algEquivMatrix') A'))
          (LinearMap.single i✝))
      1 =
    ↑(LinearMap.comp (↑(PiToModule.fromEnd R b) (f * f')) (LinearMap.single i✝)) 1
[PROOFSTEP]
dsimp [PiToModule.fromEnd]
[GOAL]
case h.h
ι : Type u_1
inst✝⁴ : Fintype ι
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_3
inst✝² : CommRing R
inst✝¹ : Module R M
I : Ideal R
b : ι → M
hb : Submodule.span R (Set.range b) = ⊤
inst✝ : DecidableEq ι
A A' : Matrix ι ι R
f f' : Module.End R M
h : Represents b A f
h' : Represents b A' f'
i✝ : ι
⊢ ↑(↑(Fintype.total R R) b)
      (↑(↑(AlgEquiv.symm algEquivMatrix') A) (↑(↑(AlgEquiv.symm algEquivMatrix') A') (Pi.single i✝ 1))) =
    ↑f (↑f' (↑(↑(Fintype.total R R) b) (Pi.single i✝ 1)))
[PROOFSTEP]
rw [← h'.congr_fun, ← h.congr_fun]
[GOAL]
case h.h
ι : Type u_1
inst✝⁴ : Fintype ι
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_3
inst✝² : CommRing R
inst✝¹ : Module R M
I : Ideal R
b : ι → M
hb : Submodule.span R (Set.range b) = ⊤
inst✝ : DecidableEq ι
A A' : Matrix ι ι R
f f' : Module.End R M
h : Represents b A f
h' : Represents b A' f'
i✝ : ι
⊢ ↑(↑(Fintype.total R R) b)
      (↑(↑(AlgEquiv.symm algEquivMatrix') A) (↑(↑(AlgEquiv.symm algEquivMatrix') A') (Pi.single i✝ 1))) =
    ↑(↑(Fintype.total R R) b) (mulVec A (mulVec A' (Pi.single i✝ 1)))
[PROOFSTEP]
rfl
[GOAL]
ι : Type u_1
inst✝⁴ : Fintype ι
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_3
inst✝² : CommRing R
inst✝¹ : Module R M
I : Ideal R
b : ι → M
hb : Submodule.span R (Set.range b) = ⊤
inst✝ : DecidableEq ι
⊢ Represents b 1 1
[PROOFSTEP]
delta Matrix.Represents PiToModule.fromMatrix
[GOAL]
ι : Type u_1
inst✝⁴ : Fintype ι
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_3
inst✝² : CommRing R
inst✝¹ : Module R M
I : Ideal R
b : ι → M
hb : Submodule.span R (Set.range b) = ⊤
inst✝ : DecidableEq ι
⊢ ↑(LinearMap.comp (↑(LinearMap.llcomp R (ι → R) (ι → R) M) (↑(Fintype.total R R) b))
          (AlgEquiv.toLinearMap (AlgEquiv.symm algEquivMatrix')))
      1 =
    ↑(PiToModule.fromEnd R b) 1
[PROOFSTEP]
rw [LinearMap.comp_apply, AlgEquiv.toLinearMap_apply, _root_.map_one]
[GOAL]
ι : Type u_1
inst✝⁴ : Fintype ι
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_3
inst✝² : CommRing R
inst✝¹ : Module R M
I : Ideal R
b : ι → M
hb : Submodule.span R (Set.range b) = ⊤
inst✝ : DecidableEq ι
⊢ ↑(↑(LinearMap.llcomp R (ι → R) (ι → R) M) (↑(Fintype.total R R) b)) 1 = ↑(PiToModule.fromEnd R b) 1
[PROOFSTEP]
ext
[GOAL]
case h.h
ι : Type u_1
inst✝⁴ : Fintype ι
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_3
inst✝² : CommRing R
inst✝¹ : Module R M
I : Ideal R
b : ι → M
hb : Submodule.span R (Set.range b) = ⊤
inst✝ : DecidableEq ι
i✝ : ι
⊢ ↑(LinearMap.comp (↑(↑(LinearMap.llcomp R (ι → R) (ι → R) M) (↑(Fintype.total R R) b)) 1) (LinearMap.single i✝)) 1 =
    ↑(LinearMap.comp (↑(PiToModule.fromEnd R b) 1) (LinearMap.single i✝)) 1
[PROOFSTEP]
rfl
[GOAL]
ι : Type u_1
inst✝⁴ : Fintype ι
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_3
inst✝² : CommRing R
inst✝¹ : Module R M
I : Ideal R
b : ι → M
hb : Submodule.span R (Set.range b) = ⊤
inst✝ : DecidableEq ι
A A' : Matrix ι ι R
f f' : Module.End R M
h : Represents b A f
h' : Represents b A' f'
⊢ Represents b (A + A') (f + f')
[PROOFSTEP]
delta Matrix.Represents at h h' ⊢
[GOAL]
ι : Type u_1
inst✝⁴ : Fintype ι
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_3
inst✝² : CommRing R
inst✝¹ : Module R M
I : Ideal R
b : ι → M
hb : Submodule.span R (Set.range b) = ⊤
inst✝ : DecidableEq ι
A A' : Matrix ι ι R
f f' : Module.End R M
h : ↑(PiToModule.fromMatrix R b) A = ↑(PiToModule.fromEnd R b) f
h' : ↑(PiToModule.fromMatrix R b) A' = ↑(PiToModule.fromEnd R b) f'
⊢ ↑(PiToModule.fromMatrix R b) (A + A') = ↑(PiToModule.fromEnd R b) (f + f')
[PROOFSTEP]
rw [map_add, map_add, h, h']
[GOAL]
ι : Type u_1
inst✝⁴ : Fintype ι
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_3
inst✝² : CommRing R
inst✝¹ : Module R M
I : Ideal R
b : ι → M
hb : Submodule.span R (Set.range b) = ⊤
inst✝ : DecidableEq ι
⊢ Represents b 0 0
[PROOFSTEP]
delta Matrix.Represents
[GOAL]
ι : Type u_1
inst✝⁴ : Fintype ι
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_3
inst✝² : CommRing R
inst✝¹ : Module R M
I : Ideal R
b : ι → M
hb : Submodule.span R (Set.range b) = ⊤
inst✝ : DecidableEq ι
⊢ ↑(PiToModule.fromMatrix R b) 0 = ↑(PiToModule.fromEnd R b) 0
[PROOFSTEP]
rw [map_zero, map_zero]
[GOAL]
ι : Type u_1
inst✝⁴ : Fintype ι
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_3
inst✝² : CommRing R
inst✝¹ : Module R M
I : Ideal R
b : ι → M
hb : Submodule.span R (Set.range b) = ⊤
inst✝ : DecidableEq ι
A : Matrix ι ι R
f : Module.End R M
h : Represents b A f
r : R
⊢ Represents b (r • A) (r • f)
[PROOFSTEP]
delta Matrix.Represents at h ⊢
[GOAL]
ι : Type u_1
inst✝⁴ : Fintype ι
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_3
inst✝² : CommRing R
inst✝¹ : Module R M
I : Ideal R
b : ι → M
hb : Submodule.span R (Set.range b) = ⊤
inst✝ : DecidableEq ι
A : Matrix ι ι R
f : Module.End R M
h : ↑(PiToModule.fromMatrix R b) A = ↑(PiToModule.fromEnd R b) f
r : R
⊢ ↑(PiToModule.fromMatrix R b) (r • A) = ↑(PiToModule.fromEnd R b) (r • f)
[PROOFSTEP]
rw [SMulHomClass.map_smul, SMulHomClass.map_smul, h]
[GOAL]
ι : Type u_1
inst✝⁴ : Fintype ι
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_3
inst✝² : CommRing R
inst✝¹ : Module R M
I✝ : Ideal R
b : ι → M
hb : Submodule.span R (Set.range b) = ⊤
inst✝ : DecidableEq ι
f : Module.End R M
I : Ideal R
hI : LinearMap.range f ≤ I • ⊤
⊢ ∃ M_1, ↑(toEnd R b hb) M_1 = f ∧ ∀ (i j : ι), ↑M_1 i j ∈ I
[PROOFSTEP]
have : ∀ x, f x ∈ LinearMap.range (Ideal.finsuppTotal ι M I b) :=
  by
  rw [Ideal.range_finsuppTotal, hb]
  exact fun x => hI (LinearMap.mem_range_self f x)
[GOAL]
ι : Type u_1
inst✝⁴ : Fintype ι
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_3
inst✝² : CommRing R
inst✝¹ : Module R M
I✝ : Ideal R
b : ι → M
hb : Submodule.span R (Set.range b) = ⊤
inst✝ : DecidableEq ι
f : Module.End R M
I : Ideal R
hI : LinearMap.range f ≤ I • ⊤
⊢ ∀ (x : M), ↑f x ∈ LinearMap.range (Ideal.finsuppTotal ι M I b)
[PROOFSTEP]
rw [Ideal.range_finsuppTotal, hb]
[GOAL]
ι : Type u_1
inst✝⁴ : Fintype ι
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_3
inst✝² : CommRing R
inst✝¹ : Module R M
I✝ : Ideal R
b : ι → M
hb : Submodule.span R (Set.range b) = ⊤
inst✝ : DecidableEq ι
f : Module.End R M
I : Ideal R
hI : LinearMap.range f ≤ I • ⊤
⊢ ∀ (x : M), ↑f x ∈ I • ⊤
[PROOFSTEP]
exact fun x => hI (LinearMap.mem_range_self f x)
[GOAL]
ι : Type u_1
inst✝⁴ : Fintype ι
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_3
inst✝² : CommRing R
inst✝¹ : Module R M
I✝ : Ideal R
b : ι → M
hb : Submodule.span R (Set.range b) = ⊤
inst✝ : DecidableEq ι
f : Module.End R M
I : Ideal R
hI : LinearMap.range f ≤ I • ⊤
this : ∀ (x : M), ↑f x ∈ LinearMap.range (Ideal.finsuppTotal ι M I b)
⊢ ∃ M_1, ↑(toEnd R b hb) M_1 = f ∧ ∀ (i j : ι), ↑M_1 i j ∈ I
[PROOFSTEP]
choose bM' hbM' using this
[GOAL]
ι : Type u_1
inst✝⁴ : Fintype ι
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_3
inst✝² : CommRing R
inst✝¹ : Module R M
I✝ : Ideal R
b : ι → M
hb : Submodule.span R (Set.range b) = ⊤
inst✝ : DecidableEq ι
f : Module.End R M
I : Ideal R
hI : LinearMap.range f ≤ I • ⊤
bM' : M → ι →₀ { x // x ∈ I }
hbM' : ∀ (x : M), ↑(Ideal.finsuppTotal ι M I b) (bM' x) = ↑f x
⊢ ∃ M_1, ↑(toEnd R b hb) M_1 = f ∧ ∀ (i j : ι), ↑M_1 i j ∈ I
[PROOFSTEP]
let A : Matrix ι ι R := fun i j => bM' (b j) i
[GOAL]
ι : Type u_1
inst✝⁴ : Fintype ι
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_3
inst✝² : CommRing R
inst✝¹ : Module R M
I✝ : Ideal R
b : ι → M
hb : Submodule.span R (Set.range b) = ⊤
inst✝ : DecidableEq ι
f : Module.End R M
I : Ideal R
hI : LinearMap.range f ≤ I • ⊤
bM' : M → ι →₀ { x // x ∈ I }
hbM' : ∀ (x : M), ↑(Ideal.finsuppTotal ι M I b) (bM' x) = ↑f x
A : Matrix ι ι R := fun i j => ↑(↑(bM' (b j)) i)
⊢ ∃ M_1, ↑(toEnd R b hb) M_1 = f ∧ ∀ (i j : ι), ↑M_1 i j ∈ I
[PROOFSTEP]
have : A.Represents b f := by
  rw [Matrix.represents_iff']
  dsimp
  intro j
  specialize hbM' (b j)
  rwa [Ideal.finsuppTotal_apply_eq_of_fintype] at hbM'
[GOAL]
ι : Type u_1
inst✝⁴ : Fintype ι
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_3
inst✝² : CommRing R
inst✝¹ : Module R M
I✝ : Ideal R
b : ι → M
hb : Submodule.span R (Set.range b) = ⊤
inst✝ : DecidableEq ι
f : Module.End R M
I : Ideal R
hI : LinearMap.range f ≤ I • ⊤
bM' : M → ι →₀ { x // x ∈ I }
hbM' : ∀ (x : M), ↑(Ideal.finsuppTotal ι M I b) (bM' x) = ↑f x
A : Matrix ι ι R := fun i j => ↑(↑(bM' (b j)) i)
⊢ Represents b A f
[PROOFSTEP]
rw [Matrix.represents_iff']
[GOAL]
ι : Type u_1
inst✝⁴ : Fintype ι
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_3
inst✝² : CommRing R
inst✝¹ : Module R M
I✝ : Ideal R
b : ι → M
hb : Submodule.span R (Set.range b) = ⊤
inst✝ : DecidableEq ι
f : Module.End R M
I : Ideal R
hI : LinearMap.range f ≤ I • ⊤
bM' : M → ι →₀ { x // x ∈ I }
hbM' : ∀ (x : M), ↑(Ideal.finsuppTotal ι M I b) (bM' x) = ↑f x
A : Matrix ι ι R := fun i j => ↑(↑(bM' (b j)) i)
⊢ ∀ (j : ι), ∑ i : ι, A i j • b i = ↑f (b j)
[PROOFSTEP]
dsimp
[GOAL]
ι : Type u_1
inst✝⁴ : Fintype ι
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_3
inst✝² : CommRing R
inst✝¹ : Module R M
I✝ : Ideal R
b : ι → M
hb : Submodule.span R (Set.range b) = ⊤
inst✝ : DecidableEq ι
f : Module.End R M
I : Ideal R
hI : LinearMap.range f ≤ I • ⊤
bM' : M → ι →₀ { x // x ∈ I }
hbM' : ∀ (x : M), ↑(Ideal.finsuppTotal ι M I b) (bM' x) = ↑f x
A : Matrix ι ι R := fun i j => ↑(↑(bM' (b j)) i)
⊢ ∀ (j : ι), ∑ i : ι, ↑(↑(bM' (b j)) i) • b i = ↑f (b j)
[PROOFSTEP]
intro j
[GOAL]
ι : Type u_1
inst✝⁴ : Fintype ι
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_3
inst✝² : CommRing R
inst✝¹ : Module R M
I✝ : Ideal R
b : ι → M
hb : Submodule.span R (Set.range b) = ⊤
inst✝ : DecidableEq ι
f : Module.End R M
I : Ideal R
hI : LinearMap.range f ≤ I • ⊤
bM' : M → ι →₀ { x // x ∈ I }
hbM' : ∀ (x : M), ↑(Ideal.finsuppTotal ι M I b) (bM' x) = ↑f x
A : Matrix ι ι R := fun i j => ↑(↑(bM' (b j)) i)
j : ι
⊢ ∑ i : ι, ↑(↑(bM' (b j)) i) • b i = ↑f (b j)
[PROOFSTEP]
specialize hbM' (b j)
[GOAL]
ι : Type u_1
inst✝⁴ : Fintype ι
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_3
inst✝² : CommRing R
inst✝¹ : Module R M
I✝ : Ideal R
b : ι → M
hb : Submodule.span R (Set.range b) = ⊤
inst✝ : DecidableEq ι
f : Module.End R M
I : Ideal R
hI : LinearMap.range f ≤ I • ⊤
bM' : M → ι →₀ { x // x ∈ I }
A : Matrix ι ι R := fun i j => ↑(↑(bM' (b j)) i)
j : ι
hbM' : ↑(Ideal.finsuppTotal ι M I b) (bM' (b j)) = ↑f (b j)
⊢ ∑ i : ι, ↑(↑(bM' (b j)) i) • b i = ↑f (b j)
[PROOFSTEP]
rwa [Ideal.finsuppTotal_apply_eq_of_fintype] at hbM'
[GOAL]
ι : Type u_1
inst✝⁴ : Fintype ι
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_3
inst✝² : CommRing R
inst✝¹ : Module R M
I✝ : Ideal R
b : ι → M
hb : Submodule.span R (Set.range b) = ⊤
inst✝ : DecidableEq ι
f : Module.End R M
I : Ideal R
hI : LinearMap.range f ≤ I • ⊤
bM' : M → ι →₀ { x // x ∈ I }
hbM' : ∀ (x : M), ↑(Ideal.finsuppTotal ι M I b) (bM' x) = ↑f x
A : Matrix ι ι R := fun i j => ↑(↑(bM' (b j)) i)
this : Represents b A f
⊢ ∃ M_1, ↑(toEnd R b hb) M_1 = f ∧ ∀ (i j : ι), ↑M_1 i j ∈ I
[PROOFSTEP]
exact
  ⟨⟨A, f, this⟩, Matrix.isRepresentation.eq_toEnd_of_represents R b hb ⟨A, f, this⟩ this, fun i j => (bM' (b j) i).prop⟩
[GOAL]
ι : Type u_1
inst✝⁴ : Fintype ι
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_3
inst✝² : CommRing R
inst✝¹ : Module R M
I : Ideal R
b : ι → M
hb : Submodule.span R (Set.range b) = ⊤
inst✝ : DecidableEq ι
⊢ Function.Surjective ↑(toEnd R b hb)
[PROOFSTEP]
intro f
[GOAL]
ι : Type u_1
inst✝⁴ : Fintype ι
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_3
inst✝² : CommRing R
inst✝¹ : Module R M
I : Ideal R
b : ι → M
hb : Submodule.span R (Set.range b) = ⊤
inst✝ : DecidableEq ι
f : Module.End R M
⊢ ∃ a, ↑(toEnd R b hb) a = f
[PROOFSTEP]
obtain ⟨M, e, -⟩ := Matrix.isRepresentation.toEnd_exists_mem_ideal R b hb f ⊤ (by simp)
[GOAL]
ι : Type u_1
inst✝⁴ : Fintype ι
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_3
inst✝² : CommRing R
inst✝¹ : Module R M
I : Ideal R
b : ι → M
hb : Submodule.span R (Set.range b) = ⊤
inst✝ : DecidableEq ι
f : Module.End R M
⊢ LinearMap.range f ≤ ⊤ • ⊤
[PROOFSTEP]
simp
[GOAL]
case intro.intro
ι : Type u_1
inst✝⁴ : Fintype ι
M✝ : Type u_2
inst✝³ : AddCommGroup M✝
R : Type u_3
inst✝² : CommRing R
inst✝¹ : Module R M✝
I : Ideal R
b : ι → M✝
hb : Submodule.span R (Set.range b) = ⊤
inst✝ : DecidableEq ι
f : Module.End R M✝
M : { x // x ∈ isRepresentation R b }
e : ↑(toEnd R b hb) M = f
⊢ ∃ a, ↑(toEnd R b hb) a = f
[PROOFSTEP]
exact ⟨M, e⟩
[GOAL]
ι : Type u_1
inst✝⁴ : Fintype ι
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_3
inst✝² : CommRing R
inst✝¹ : Module R M
I✝ : Ideal R
b : ι → M
hb : Submodule.span R (Set.range b) = ⊤
inst✝ : Module.Finite R M
f : Module.End R M
I : Ideal R
hI : range f ≤ I • ⊤
⊢ ∃ p, Monic p ∧ (∀ (k : ℕ), coeff p k ∈ I ^ (natDegree p - k)) ∧ ↑(aeval f) p = 0
[PROOFSTEP]
classical
cases subsingleton_or_nontrivial R
· exact ⟨0, Polynomial.monic_of_subsingleton _, by simp⟩
obtain ⟨s : Finset M, hs : Submodule.span R (s : Set M) = ⊤⟩ :=
  Module.Finite.out (R := R) (M := M)
    -- Porting note: `H` was `rfl`
obtain ⟨A, H, h⟩ :=
  Matrix.isRepresentation.toEnd_exists_mem_ideal R ((↑) : s → M)
    (by rw [Subtype.range_coe_subtype, Finset.setOf_mem, hs]) f I hI
rw [← H]
refine' ⟨A.1.charpoly, A.1.charpoly_monic, _, _⟩
· rw [A.1.charpoly_natDegree_eq_dim]
  exact coeff_charpoly_mem_ideal_pow h
· rw [Polynomial.aeval_algHom_apply, ← map_zero (Matrix.isRepresentation.toEnd R ((↑) : s → M) _)]
  congr 1
  ext1
  rw [Polynomial.aeval_subalgebra_coe, Matrix.aeval_self_charpoly, Subalgebra.coe_zero]
[GOAL]
ι : Type u_1
inst✝⁴ : Fintype ι
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_3
inst✝² : CommRing R
inst✝¹ : Module R M
I✝ : Ideal R
b : ι → M
hb : Submodule.span R (Set.range b) = ⊤
inst✝ : Module.Finite R M
f : Module.End R M
I : Ideal R
hI : range f ≤ I • ⊤
⊢ ∃ p, Monic p ∧ (∀ (k : ℕ), coeff p k ∈ I ^ (natDegree p - k)) ∧ ↑(aeval f) p = 0
[PROOFSTEP]
cases subsingleton_or_nontrivial R
[GOAL]
case inl
ι : Type u_1
inst✝⁴ : Fintype ι
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_3
inst✝² : CommRing R
inst✝¹ : Module R M
I✝ : Ideal R
b : ι → M
hb : Submodule.span R (Set.range b) = ⊤
inst✝ : Module.Finite R M
f : Module.End R M
I : Ideal R
hI : range f ≤ I • ⊤
h✝ : Subsingleton R
⊢ ∃ p, Monic p ∧ (∀ (k : ℕ), coeff p k ∈ I ^ (natDegree p - k)) ∧ ↑(aeval f) p = 0
[PROOFSTEP]
exact ⟨0, Polynomial.monic_of_subsingleton _, by simp⟩
[GOAL]
ι : Type u_1
inst✝⁴ : Fintype ι
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_3
inst✝² : CommRing R
inst✝¹ : Module R M
I✝ : Ideal R
b : ι → M
hb : Submodule.span R (Set.range b) = ⊤
inst✝ : Module.Finite R M
f : Module.End R M
I : Ideal R
hI : range f ≤ I • ⊤
h✝ : Subsingleton R
⊢ (∀ (k : ℕ), coeff 0 k ∈ I ^ (natDegree 0 - k)) ∧ ↑(aeval f) 0 = 0
[PROOFSTEP]
simp
[GOAL]
case inr
ι : Type u_1
inst✝⁴ : Fintype ι
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_3
inst✝² : CommRing R
inst✝¹ : Module R M
I✝ : Ideal R
b : ι → M
hb : Submodule.span R (Set.range b) = ⊤
inst✝ : Module.Finite R M
f : Module.End R M
I : Ideal R
hI : range f ≤ I • ⊤
h✝ : Nontrivial R
⊢ ∃ p, Monic p ∧ (∀ (k : ℕ), coeff p k ∈ I ^ (natDegree p - k)) ∧ ↑(aeval f) p = 0
[PROOFSTEP]
obtain ⟨s : Finset M, hs : Submodule.span R (s : Set M) = ⊤⟩ :=
  Module.Finite.out (R := R) (M := M)
    -- Porting note: `H` was `rfl`
[GOAL]
case inr.intro
ι : Type u_1
inst✝⁴ : Fintype ι
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_3
inst✝² : CommRing R
inst✝¹ : Module R M
I✝ : Ideal R
b : ι → M
hb : Submodule.span R (Set.range b) = ⊤
inst✝ : Module.Finite R M
f : Module.End R M
I : Ideal R
hI : range f ≤ I • ⊤
h✝ : Nontrivial R
s : Finset M
hs : Submodule.span R ↑s = ⊤
⊢ ∃ p, Monic p ∧ (∀ (k : ℕ), coeff p k ∈ I ^ (natDegree p - k)) ∧ ↑(aeval f) p = 0
[PROOFSTEP]
obtain ⟨A, H, h⟩ :=
  Matrix.isRepresentation.toEnd_exists_mem_ideal R ((↑) : s → M)
    (by rw [Subtype.range_coe_subtype, Finset.setOf_mem, hs]) f I hI
[GOAL]
ι : Type u_1
inst✝⁴ : Fintype ι
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_3
inst✝² : CommRing R
inst✝¹ : Module R M
I✝ : Ideal R
b : ι → M
hb : Submodule.span R (Set.range b) = ⊤
inst✝ : Module.Finite R M
f : Module.End R M
I : Ideal R
hI : range f ≤ I • ⊤
h✝ : Nontrivial R
s : Finset M
hs : Submodule.span R ↑s = ⊤
⊢ Submodule.span R (Set.range Subtype.val) = ⊤
[PROOFSTEP]
rw [Subtype.range_coe_subtype, Finset.setOf_mem, hs]
[GOAL]
case inr.intro.intro.intro
ι : Type u_1
inst✝⁴ : Fintype ι
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_3
inst✝² : CommRing R
inst✝¹ : Module R M
I✝ : Ideal R
b : ι → M
hb : Submodule.span R (Set.range b) = ⊤
inst✝ : Module.Finite R M
f : Module.End R M
I : Ideal R
hI : range f ≤ I • ⊤
h✝ : Nontrivial R
s : Finset M
hs : Submodule.span R ↑s = ⊤
A : { x // x ∈ Matrix.isRepresentation R Subtype.val }
H : ↑(Matrix.isRepresentation.toEnd R Subtype.val (_ : Submodule.span R (Set.range Subtype.val) = ⊤)) A = f
h : ∀ (i j : { x // x ∈ s }), ↑A i j ∈ I
⊢ ∃ p, Monic p ∧ (∀ (k : ℕ), coeff p k ∈ I ^ (natDegree p - k)) ∧ ↑(aeval f) p = 0
[PROOFSTEP]
rw [← H]
[GOAL]
case inr.intro.intro.intro
ι : Type u_1
inst✝⁴ : Fintype ι
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_3
inst✝² : CommRing R
inst✝¹ : Module R M
I✝ : Ideal R
b : ι → M
hb : Submodule.span R (Set.range b) = ⊤
inst✝ : Module.Finite R M
f : Module.End R M
I : Ideal R
hI : range f ≤ I • ⊤
h✝ : Nontrivial R
s : Finset M
hs : Submodule.span R ↑s = ⊤
A : { x // x ∈ Matrix.isRepresentation R Subtype.val }
H : ↑(Matrix.isRepresentation.toEnd R Subtype.val (_ : Submodule.span R (Set.range Subtype.val) = ⊤)) A = f
h : ∀ (i j : { x // x ∈ s }), ↑A i j ∈ I
⊢ ∃ p,
    Monic p ∧
      (∀ (k : ℕ), coeff p k ∈ I ^ (natDegree p - k)) ∧
        ↑(aeval (↑(Matrix.isRepresentation.toEnd R Subtype.val (_ : Submodule.span R (Set.range Subtype.val) = ⊤)) A))
            p =
          0
[PROOFSTEP]
refine' ⟨A.1.charpoly, A.1.charpoly_monic, _, _⟩
[GOAL]
case inr.intro.intro.intro.refine'_1
ι : Type u_1
inst✝⁴ : Fintype ι
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_3
inst✝² : CommRing R
inst✝¹ : Module R M
I✝ : Ideal R
b : ι → M
hb : Submodule.span R (Set.range b) = ⊤
inst✝ : Module.Finite R M
f : Module.End R M
I : Ideal R
hI : range f ≤ I • ⊤
h✝ : Nontrivial R
s : Finset M
hs : Submodule.span R ↑s = ⊤
A : { x // x ∈ Matrix.isRepresentation R Subtype.val }
H : ↑(Matrix.isRepresentation.toEnd R Subtype.val (_ : Submodule.span R (Set.range Subtype.val) = ⊤)) A = f
h : ∀ (i j : { x // x ∈ s }), ↑A i j ∈ I
⊢ ∀ (k : ℕ), coeff (Matrix.charpoly ↑A) k ∈ I ^ (natDegree (Matrix.charpoly ↑A) - k)
[PROOFSTEP]
rw [A.1.charpoly_natDegree_eq_dim]
[GOAL]
case inr.intro.intro.intro.refine'_1
ι : Type u_1
inst✝⁴ : Fintype ι
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_3
inst✝² : CommRing R
inst✝¹ : Module R M
I✝ : Ideal R
b : ι → M
hb : Submodule.span R (Set.range b) = ⊤
inst✝ : Module.Finite R M
f : Module.End R M
I : Ideal R
hI : range f ≤ I • ⊤
h✝ : Nontrivial R
s : Finset M
hs : Submodule.span R ↑s = ⊤
A : { x // x ∈ Matrix.isRepresentation R Subtype.val }
H : ↑(Matrix.isRepresentation.toEnd R Subtype.val (_ : Submodule.span R (Set.range Subtype.val) = ⊤)) A = f
h : ∀ (i j : { x // x ∈ s }), ↑A i j ∈ I
⊢ ∀ (k : ℕ), coeff (Matrix.charpoly ↑A) k ∈ I ^ (Fintype.card { x // x ∈ s } - k)
[PROOFSTEP]
exact coeff_charpoly_mem_ideal_pow h
[GOAL]
case inr.intro.intro.intro.refine'_2
ι : Type u_1
inst✝⁴ : Fintype ι
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_3
inst✝² : CommRing R
inst✝¹ : Module R M
I✝ : Ideal R
b : ι → M
hb : Submodule.span R (Set.range b) = ⊤
inst✝ : Module.Finite R M
f : Module.End R M
I : Ideal R
hI : range f ≤ I • ⊤
h✝ : Nontrivial R
s : Finset M
hs : Submodule.span R ↑s = ⊤
A : { x // x ∈ Matrix.isRepresentation R Subtype.val }
H : ↑(Matrix.isRepresentation.toEnd R Subtype.val (_ : Submodule.span R (Set.range Subtype.val) = ⊤)) A = f
h : ∀ (i j : { x // x ∈ s }), ↑A i j ∈ I
⊢ ↑(aeval (↑(Matrix.isRepresentation.toEnd R Subtype.val (_ : Submodule.span R (Set.range Subtype.val) = ⊤)) A))
      (Matrix.charpoly ↑A) =
    0
[PROOFSTEP]
rw [Polynomial.aeval_algHom_apply, ← map_zero (Matrix.isRepresentation.toEnd R ((↑) : s → M) _)]
[GOAL]
case inr.intro.intro.intro.refine'_2
ι : Type u_1
inst✝⁴ : Fintype ι
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_3
inst✝² : CommRing R
inst✝¹ : Module R M
I✝ : Ideal R
b : ι → M
hb : Submodule.span R (Set.range b) = ⊤
inst✝ : Module.Finite R M
f : Module.End R M
I : Ideal R
hI : range f ≤ I • ⊤
h✝ : Nontrivial R
s : Finset M
hs : Submodule.span R ↑s = ⊤
A : { x // x ∈ Matrix.isRepresentation R Subtype.val }
H : ↑(Matrix.isRepresentation.toEnd R Subtype.val (_ : Submodule.span R (Set.range Subtype.val) = ⊤)) A = f
h : ∀ (i j : { x // x ∈ s }), ↑A i j ∈ I
⊢ ↑(Matrix.isRepresentation.toEnd R Subtype.val (_ : Submodule.span R (Set.range Subtype.val) = ⊤))
      (↑(aeval A) (Matrix.charpoly ↑A)) =
    ↑(Matrix.isRepresentation.toEnd R Subtype.val ?m.193133) 0
ι : Type u_1
inst✝⁴ : Fintype ι
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_3
inst✝² : CommRing R
inst✝¹ : Module R M
I✝ : Ideal R
b : ι → M
hb : Submodule.span R (Set.range b) = ⊤
inst✝ : Module.Finite R M
f : Module.End R M
I : Ideal R
hI : range f ≤ I • ⊤
h✝ : Nontrivial R
s : Finset M
hs : Submodule.span R ↑s = ⊤
A : { x // x ∈ Matrix.isRepresentation R Subtype.val }
H : ↑(Matrix.isRepresentation.toEnd R Subtype.val (_ : Submodule.span R (Set.range Subtype.val) = ⊤)) A = f
h : ∀ (i j : { x // x ∈ s }), ↑A i j ∈ I
⊢ Submodule.span R (Set.range Subtype.val) = ⊤
[PROOFSTEP]
congr 1
[GOAL]
case inr.intro.intro.intro.refine'_2.h.e_6.h
ι : Type u_1
inst✝⁴ : Fintype ι
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_3
inst✝² : CommRing R
inst✝¹ : Module R M
I✝ : Ideal R
b : ι → M
hb : Submodule.span R (Set.range b) = ⊤
inst✝ : Module.Finite R M
f : Module.End R M
I : Ideal R
hI : range f ≤ I • ⊤
h✝ : Nontrivial R
s : Finset M
hs : Submodule.span R ↑s = ⊤
A : { x // x ∈ Matrix.isRepresentation R Subtype.val }
H : ↑(Matrix.isRepresentation.toEnd R Subtype.val (_ : Submodule.span R (Set.range Subtype.val) = ⊤)) A = f
h : ∀ (i j : { x // x ∈ s }), ↑A i j ∈ I
⊢ ↑(aeval A) (Matrix.charpoly ↑A) = 0
[PROOFSTEP]
ext1
[GOAL]
case inr.intro.intro.intro.refine'_2.h.e_6.h.a
ι : Type u_1
inst✝⁴ : Fintype ι
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_3
inst✝² : CommRing R
inst✝¹ : Module R M
I✝ : Ideal R
b : ι → M
hb : Submodule.span R (Set.range b) = ⊤
inst✝ : Module.Finite R M
f : Module.End R M
I : Ideal R
hI : range f ≤ I • ⊤
h✝ : Nontrivial R
s : Finset M
hs : Submodule.span R ↑s = ⊤
A : { x // x ∈ Matrix.isRepresentation R Subtype.val }
H : ↑(Matrix.isRepresentation.toEnd R Subtype.val (_ : Submodule.span R (Set.range Subtype.val) = ⊤)) A = f
h : ∀ (i j : { x // x ∈ s }), ↑A i j ∈ I
⊢ ↑(↑(aeval A) (Matrix.charpoly ↑A)) = ↑0
[PROOFSTEP]
rw [Polynomial.aeval_subalgebra_coe, Matrix.aeval_self_charpoly, Subalgebra.coe_zero]
[GOAL]
ι : Type u_1
inst✝⁴ : Fintype ι
M : Type u_2
inst✝³ : AddCommGroup M
R : Type u_3
inst✝² : CommRing R
inst✝¹ : Module R M
I : Ideal R
b : ι → M
hb : Submodule.span R (Set.range b) = ⊤
inst✝ : Module.Finite R M
f : Module.End R M
⊢ range f ≤ ⊤ • ⊤
[PROOFSTEP]
simp


[GOAL]
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : RegularSpace Y
f : X → Y
A B : Set X
hB : B ⊆ closure A
hf : ∀ (x : X), x ∈ B → ∃ y, Tendsto f (𝓝[A] x) (𝓝 y)
⊢ ContinuousOn (extendFrom A f) B
[PROOFSTEP]
set φ := extendFrom A f
[GOAL]
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : RegularSpace Y
f : X → Y
A B : Set X
hB : B ⊆ closure A
hf : ∀ (x : X), x ∈ B → ∃ y, Tendsto f (𝓝[A] x) (𝓝 y)
φ : X → Y := extendFrom A f
⊢ ContinuousOn φ B
[PROOFSTEP]
intro x x_in
[GOAL]
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : RegularSpace Y
f : X → Y
A B : Set X
hB : B ⊆ closure A
hf : ∀ (x : X), x ∈ B → ∃ y, Tendsto f (𝓝[A] x) (𝓝 y)
φ : X → Y := extendFrom A f
x : X
x_in : x ∈ B
⊢ ContinuousWithinAt φ B x
[PROOFSTEP]
suffices ∀ V' ∈ 𝓝 (φ x), IsClosed V' → φ ⁻¹' V' ∈ 𝓝[B] x by
  simpa [ContinuousWithinAt, (closed_nhds_basis (φ x)).tendsto_right_iff]
[GOAL]
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : RegularSpace Y
f : X → Y
A B : Set X
hB : B ⊆ closure A
hf : ∀ (x : X), x ∈ B → ∃ y, Tendsto f (𝓝[A] x) (𝓝 y)
φ : X → Y := extendFrom A f
x : X
x_in : x ∈ B
this : ∀ (V' : Set Y), V' ∈ 𝓝 (φ x) → IsClosed V' → φ ⁻¹' V' ∈ 𝓝[B] x
⊢ ContinuousWithinAt φ B x
[PROOFSTEP]
simpa [ContinuousWithinAt, (closed_nhds_basis (φ x)).tendsto_right_iff]
[GOAL]
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : RegularSpace Y
f : X → Y
A B : Set X
hB : B ⊆ closure A
hf : ∀ (x : X), x ∈ B → ∃ y, Tendsto f (𝓝[A] x) (𝓝 y)
φ : X → Y := extendFrom A f
x : X
x_in : x ∈ B
⊢ ∀ (V' : Set Y), V' ∈ 𝓝 (φ x) → IsClosed V' → φ ⁻¹' V' ∈ 𝓝[B] x
[PROOFSTEP]
intro V' V'_in V'_closed
[GOAL]
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : RegularSpace Y
f : X → Y
A B : Set X
hB : B ⊆ closure A
hf : ∀ (x : X), x ∈ B → ∃ y, Tendsto f (𝓝[A] x) (𝓝 y)
φ : X → Y := extendFrom A f
x : X
x_in : x ∈ B
V' : Set Y
V'_in : V' ∈ 𝓝 (φ x)
V'_closed : IsClosed V'
⊢ φ ⁻¹' V' ∈ 𝓝[B] x
[PROOFSTEP]
obtain ⟨V, V_in, V_op, hV⟩ : ∃ V ∈ 𝓝 x, IsOpen V ∧ V ∩ A ⊆ f ⁻¹' V' :=
  by
  have := tendsto_extendFrom (hf x x_in)
  rcases(nhdsWithin_basis_open x A).tendsto_left_iff.mp this V' V'_in with ⟨V, ⟨hxV, V_op⟩, hV⟩
  exact ⟨V, IsOpen.mem_nhds V_op hxV, V_op, hV⟩
[GOAL]
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : RegularSpace Y
f : X → Y
A B : Set X
hB : B ⊆ closure A
hf : ∀ (x : X), x ∈ B → ∃ y, Tendsto f (𝓝[A] x) (𝓝 y)
φ : X → Y := extendFrom A f
x : X
x_in : x ∈ B
V' : Set Y
V'_in : V' ∈ 𝓝 (φ x)
V'_closed : IsClosed V'
⊢ ∃ V, V ∈ 𝓝 x ∧ IsOpen V ∧ V ∩ A ⊆ f ⁻¹' V'
[PROOFSTEP]
have := tendsto_extendFrom (hf x x_in)
[GOAL]
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : RegularSpace Y
f : X → Y
A B : Set X
hB : B ⊆ closure A
hf : ∀ (x : X), x ∈ B → ∃ y, Tendsto f (𝓝[A] x) (𝓝 y)
φ : X → Y := extendFrom A f
x : X
x_in : x ∈ B
V' : Set Y
V'_in : V' ∈ 𝓝 (φ x)
V'_closed : IsClosed V'
this : Tendsto f (𝓝[A] x) (𝓝 (extendFrom A f x))
⊢ ∃ V, V ∈ 𝓝 x ∧ IsOpen V ∧ V ∩ A ⊆ f ⁻¹' V'
[PROOFSTEP]
rcases(nhdsWithin_basis_open x A).tendsto_left_iff.mp this V' V'_in with ⟨V, ⟨hxV, V_op⟩, hV⟩
[GOAL]
case intro.intro.intro
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : RegularSpace Y
f : X → Y
A B : Set X
hB : B ⊆ closure A
hf : ∀ (x : X), x ∈ B → ∃ y, Tendsto f (𝓝[A] x) (𝓝 y)
φ : X → Y := extendFrom A f
x : X
x_in : x ∈ B
V' : Set Y
V'_in : V' ∈ 𝓝 (φ x)
V'_closed : IsClosed V'
this : Tendsto f (𝓝[A] x) (𝓝 (extendFrom A f x))
V : Set X
hV : MapsTo f (V ∩ A) V'
hxV : x ∈ V
V_op : IsOpen V
⊢ ∃ V, V ∈ 𝓝 x ∧ IsOpen V ∧ V ∩ A ⊆ f ⁻¹' V'
[PROOFSTEP]
exact ⟨V, IsOpen.mem_nhds V_op hxV, V_op, hV⟩
[GOAL]
case intro.intro.intro
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : RegularSpace Y
f : X → Y
A B : Set X
hB : B ⊆ closure A
hf : ∀ (x : X), x ∈ B → ∃ y, Tendsto f (𝓝[A] x) (𝓝 y)
φ : X → Y := extendFrom A f
x : X
x_in : x ∈ B
V' : Set Y
V'_in : V' ∈ 𝓝 (φ x)
V'_closed : IsClosed V'
V : Set X
V_in : V ∈ 𝓝 x
V_op : IsOpen V
hV : V ∩ A ⊆ f ⁻¹' V'
⊢ φ ⁻¹' V' ∈ 𝓝[B] x
[PROOFSTEP]
suffices : ∀ y ∈ V ∩ B, φ y ∈ V'
[GOAL]
case intro.intro.intro
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : RegularSpace Y
f : X → Y
A B : Set X
hB : B ⊆ closure A
hf : ∀ (x : X), x ∈ B → ∃ y, Tendsto f (𝓝[A] x) (𝓝 y)
φ : X → Y := extendFrom A f
x : X
x_in : x ∈ B
V' : Set Y
V'_in : V' ∈ 𝓝 (φ x)
V'_closed : IsClosed V'
V : Set X
V_in : V ∈ 𝓝 x
V_op : IsOpen V
hV : V ∩ A ⊆ f ⁻¹' V'
this : ∀ (y : X), y ∈ V ∩ B → φ y ∈ V'
⊢ φ ⁻¹' V' ∈ 𝓝[B] x
case this
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : RegularSpace Y
f : X → Y
A B : Set X
hB : B ⊆ closure A
hf : ∀ (x : X), x ∈ B → ∃ y, Tendsto f (𝓝[A] x) (𝓝 y)
φ : X → Y := extendFrom A f
x : X
x_in : x ∈ B
V' : Set Y
V'_in : V' ∈ 𝓝 (φ x)
V'_closed : IsClosed V'
V : Set X
V_in : V ∈ 𝓝 x
V_op : IsOpen V
hV : V ∩ A ⊆ f ⁻¹' V'
⊢ ∀ (y : X), y ∈ V ∩ B → φ y ∈ V'
[PROOFSTEP]
exact mem_of_superset (inter_mem_inf V_in <| mem_principal_self B) this
[GOAL]
case this
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : RegularSpace Y
f : X → Y
A B : Set X
hB : B ⊆ closure A
hf : ∀ (x : X), x ∈ B → ∃ y, Tendsto f (𝓝[A] x) (𝓝 y)
φ : X → Y := extendFrom A f
x : X
x_in : x ∈ B
V' : Set Y
V'_in : V' ∈ 𝓝 (φ x)
V'_closed : IsClosed V'
V : Set X
V_in : V ∈ 𝓝 x
V_op : IsOpen V
hV : V ∩ A ⊆ f ⁻¹' V'
⊢ ∀ (y : X), y ∈ V ∩ B → φ y ∈ V'
[PROOFSTEP]
rintro y ⟨hyV, hyB⟩
[GOAL]
case this.intro
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : RegularSpace Y
f : X → Y
A B : Set X
hB : B ⊆ closure A
hf : ∀ (x : X), x ∈ B → ∃ y, Tendsto f (𝓝[A] x) (𝓝 y)
φ : X → Y := extendFrom A f
x : X
x_in : x ∈ B
V' : Set Y
V'_in : V' ∈ 𝓝 (φ x)
V'_closed : IsClosed V'
V : Set X
V_in : V ∈ 𝓝 x
V_op : IsOpen V
hV : V ∩ A ⊆ f ⁻¹' V'
y : X
hyV : y ∈ V
hyB : y ∈ B
⊢ φ y ∈ V'
[PROOFSTEP]
haveI := mem_closure_iff_nhdsWithin_neBot.mp (hB hyB)
[GOAL]
case this.intro
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : RegularSpace Y
f : X → Y
A B : Set X
hB : B ⊆ closure A
hf : ∀ (x : X), x ∈ B → ∃ y, Tendsto f (𝓝[A] x) (𝓝 y)
φ : X → Y := extendFrom A f
x : X
x_in : x ∈ B
V' : Set Y
V'_in : V' ∈ 𝓝 (φ x)
V'_closed : IsClosed V'
V : Set X
V_in : V ∈ 𝓝 x
V_op : IsOpen V
hV : V ∩ A ⊆ f ⁻¹' V'
y : X
hyV : y ∈ V
hyB : y ∈ B
this : NeBot (𝓝[A] y)
⊢ φ y ∈ V'
[PROOFSTEP]
have limy : Tendsto f (𝓝[A] y) (𝓝 <| φ y) := tendsto_extendFrom (hf y hyB)
[GOAL]
case this.intro
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : RegularSpace Y
f : X → Y
A B : Set X
hB : B ⊆ closure A
hf : ∀ (x : X), x ∈ B → ∃ y, Tendsto f (𝓝[A] x) (𝓝 y)
φ : X → Y := extendFrom A f
x : X
x_in : x ∈ B
V' : Set Y
V'_in : V' ∈ 𝓝 (φ x)
V'_closed : IsClosed V'
V : Set X
V_in : V ∈ 𝓝 x
V_op : IsOpen V
hV : V ∩ A ⊆ f ⁻¹' V'
y : X
hyV : y ∈ V
hyB : y ∈ B
this : NeBot (𝓝[A] y)
limy : Tendsto f (𝓝[A] y) (𝓝 (φ y))
⊢ φ y ∈ V'
[PROOFSTEP]
have hVy : V ∈ 𝓝 y := IsOpen.mem_nhds V_op hyV
[GOAL]
case this.intro
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : RegularSpace Y
f : X → Y
A B : Set X
hB : B ⊆ closure A
hf : ∀ (x : X), x ∈ B → ∃ y, Tendsto f (𝓝[A] x) (𝓝 y)
φ : X → Y := extendFrom A f
x : X
x_in : x ∈ B
V' : Set Y
V'_in : V' ∈ 𝓝 (φ x)
V'_closed : IsClosed V'
V : Set X
V_in : V ∈ 𝓝 x
V_op : IsOpen V
hV : V ∩ A ⊆ f ⁻¹' V'
y : X
hyV : y ∈ V
hyB : y ∈ B
this : NeBot (𝓝[A] y)
limy : Tendsto f (𝓝[A] y) (𝓝 (φ y))
hVy : V ∈ 𝓝 y
⊢ φ y ∈ V'
[PROOFSTEP]
have : V ∩ A ∈ 𝓝[A] y := by simpa only [inter_comm] using inter_mem_nhdsWithin A hVy
[GOAL]
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : RegularSpace Y
f : X → Y
A B : Set X
hB : B ⊆ closure A
hf : ∀ (x : X), x ∈ B → ∃ y, Tendsto f (𝓝[A] x) (𝓝 y)
φ : X → Y := extendFrom A f
x : X
x_in : x ∈ B
V' : Set Y
V'_in : V' ∈ 𝓝 (φ x)
V'_closed : IsClosed V'
V : Set X
V_in : V ∈ 𝓝 x
V_op : IsOpen V
hV : V ∩ A ⊆ f ⁻¹' V'
y : X
hyV : y ∈ V
hyB : y ∈ B
this : NeBot (𝓝[A] y)
limy : Tendsto f (𝓝[A] y) (𝓝 (φ y))
hVy : V ∈ 𝓝 y
⊢ V ∩ A ∈ 𝓝[A] y
[PROOFSTEP]
simpa only [inter_comm] using inter_mem_nhdsWithin A hVy
[GOAL]
case this.intro
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : RegularSpace Y
f : X → Y
A B : Set X
hB : B ⊆ closure A
hf : ∀ (x : X), x ∈ B → ∃ y, Tendsto f (𝓝[A] x) (𝓝 y)
φ : X → Y := extendFrom A f
x : X
x_in : x ∈ B
V' : Set Y
V'_in : V' ∈ 𝓝 (φ x)
V'_closed : IsClosed V'
V : Set X
V_in : V ∈ 𝓝 x
V_op : IsOpen V
hV : V ∩ A ⊆ f ⁻¹' V'
y : X
hyV : y ∈ V
hyB : y ∈ B
this✝ : NeBot (𝓝[A] y)
limy : Tendsto f (𝓝[A] y) (𝓝 (φ y))
hVy : V ∈ 𝓝 y
this : V ∩ A ∈ 𝓝[A] y
⊢ φ y ∈ V'
[PROOFSTEP]
exact V'_closed.mem_of_tendsto limy (mem_of_superset this hV)
[GOAL]
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : RegularSpace Y
f : X → Y
A : Set X
hA : Dense A
hf : ∀ (x : X), ∃ y, Tendsto f (𝓝[A] x) (𝓝 y)
⊢ Continuous (extendFrom A f)
[PROOFSTEP]
rw [continuous_iff_continuousOn_univ]
[GOAL]
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : RegularSpace Y
f : X → Y
A : Set X
hA : Dense A
hf : ∀ (x : X), ∃ y, Tendsto f (𝓝[A] x) (𝓝 y)
⊢ ContinuousOn (extendFrom A f) univ
[PROOFSTEP]
exact continuousOn_extendFrom (fun x _ ↦ hA x) (by simpa using hf)
[GOAL]
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : RegularSpace Y
f : X → Y
A : Set X
hA : Dense A
hf : ∀ (x : X), ∃ y, Tendsto f (𝓝[A] x) (𝓝 y)
⊢ ∀ (x : X), x ∈ univ → ∃ y, Tendsto f (𝓝[A] x) (𝓝 y)
[PROOFSTEP]
simpa using hf


[GOAL]
α✝ : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α✝
inst✝¹ : TopologicalSpace β
s t s₁ s₂ t₁ t₂ : Set α✝
x : α✝
α : Type u_3
inst✝ : TopologicalSpace (α × α)
⊢ 𝓝ˢ (diagonal α) = ⨆ (x : α), 𝓝 (x, x)
[PROOFSTEP]
rw [nhdsSet, ← range_diag, ← range_comp]
[GOAL]
α✝ : Type u_1
β : Type u_2
inst✝² : TopologicalSpace α✝
inst✝¹ : TopologicalSpace β
s t s₁ s₂ t₁ t₂ : Set α✝
x : α✝
α : Type u_3
inst✝ : TopologicalSpace (α × α)
⊢ sSup (range (𝓝 ∘ fun x => (x, x))) = ⨆ (x : α), 𝓝 (x, x)
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t s₁ s₂ t₁ t₂ : Set α
x : α
⊢ s ∈ 𝓝ˢ t ↔ ∀ (x : α), x ∈ t → s ∈ 𝓝 x
[PROOFSTEP]
simp_rw [nhdsSet, Filter.mem_sSup, ball_image_iff]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t s₁ s₂ t₁ t₂ : Set α
x : α
⊢ s ⊆ interior t ↔ t ∈ 𝓝ˢ s
[PROOFSTEP]
simp_rw [mem_nhdsSet_iff_forall, subset_interior_iff_nhds]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t s₁ s₂ t₁ t₂ : Set α
x : α
⊢ Disjoint (𝓟 s) (𝓝ˢ t) ↔ Disjoint (closure s) t
[PROOFSTEP]
rw [disjoint_principal_left, ← subset_interior_iff_mem_nhdsSet, interior_compl, subset_compl_iff_disjoint_left]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t s₁ s₂ t₁ t₂ : Set α
x : α
⊢ Disjoint (𝓝ˢ s) (𝓟 t) ↔ Disjoint s (closure t)
[PROOFSTEP]
rw [disjoint_comm, disjoint_principal_nhdsSet, disjoint_comm]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t s₁ s₂ t₁ t₂ : Set α
x : α
⊢ s ∈ 𝓝ˢ t ↔ ∃ U, IsOpen U ∧ t ⊆ U ∧ U ⊆ s
[PROOFSTEP]
rw [← subset_interior_iff_mem_nhdsSet, subset_interior_iff]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s✝ t✝ s₁ s₂ t₁ t₂ : Set α
x : α
s t : Set α
⊢ t ∈ 𝓝ˢ s ↔ ∃ i, (IsOpen i ∧ s ⊆ i) ∧ i ⊆ t
[PROOFSTEP]
simp [mem_nhdsSet_iff_exists, and_assoc]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t s₁ s₂ t₁ t₂ : Set α
x : α
hU : IsOpen s
⊢ s ∈ 𝓝ˢ t ↔ t ⊆ s
[PROOFSTEP]
rw [← subset_interior_iff_mem_nhdsSet, hU.interior_eq]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t s₁ s₂ t₁ t₂ : Set α
x : α
⊢ 𝓝ˢ s = 𝓟 s ↔ IsOpen s
[PROOFSTEP]
rw [← principal_le_nhdsSet.le_iff_eq, le_principal_iff, mem_nhdsSet_iff_forall, isOpen_iff_mem_nhds]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t s₁ s₂ t₁ t₂ : Set α
x : α
⊢ 𝓝ˢ {x} = 𝓝 x
[PROOFSTEP]
simp [nhdsSet]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t s₁ s₂ t₁ t₂ : Set α
x : α
⊢ 𝓝ˢ ∅ = ⊥
[PROOFSTEP]
rw [isOpen_empty.nhdsSet_eq, principal_empty]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t s₁ s₂ t₁ t₂ : Set α
x : α
⊢ s ∈ 𝓝ˢ ∅
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t s₁ s₂ t₁ t₂ : Set α
x : α
⊢ 𝓝ˢ univ = ⊤
[PROOFSTEP]
rw [isOpen_univ.nhdsSet_eq, principal_univ]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s✝ t✝ s₁ s₂ t₁ t₂ : Set α
x : α
s t : Set α
⊢ 𝓝ˢ (s ∪ t) = 𝓝ˢ s ⊔ 𝓝ˢ t
[PROOFSTEP]
simp only [nhdsSet, image_union, sSup_union]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t s₁ s₂ t₁ t₂ : Set α
x : α
h₁ : s₁ ∈ 𝓝ˢ t₁
h₂ : s₂ ∈ 𝓝ˢ t₂
⊢ s₁ ∪ s₂ ∈ 𝓝ˢ (t₁ ∪ t₂)
[PROOFSTEP]
rw [nhdsSet_union]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s t s₁ s₂ t₁ t₂ : Set α
x : α
h₁ : s₁ ∈ 𝓝ˢ t₁
h₂ : s₂ ∈ 𝓝ˢ t₂
⊢ s₁ ∪ s₂ ∈ 𝓝ˢ t₁ ⊔ 𝓝ˢ t₂
[PROOFSTEP]
exact union_mem_sup h₁ h₂
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
s✝ t s₁ s₂ t₁ t₂ : Set α
x✝ x : α
s : Set α
⊢ 𝓝ˢ (insert x s) = 𝓝 x ⊔ 𝓝ˢ s
[PROOFSTEP]
rw [insert_eq, nhdsSet_union, nhdsSet_singleton]


[GOAL]
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
s t : Set X
hs : IsClosed s
ht : IsClosed t
hd : Disjoint s t
a b : ℝ
hle : a ≤ b
f : X →ᵇ ℝ
hfs : EqOn (↑f) 0 s
hft : EqOn (↑f) 1 t
hf01 : ∀ (x : X), ↑f x ∈ Icc 0 1
x : X
hx : x ∈ s
⊢ ↑(BoundedContinuousFunction.const X a + (b - a) • f) x = Function.const X a x
[PROOFSTEP]
simp [hfs hx]
[GOAL]
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
s t : Set X
hs : IsClosed s
ht : IsClosed t
hd : Disjoint s t
a b : ℝ
hle : a ≤ b
f : X →ᵇ ℝ
hfs : EqOn (↑f) 0 s
hft : EqOn (↑f) 1 t
hf01 : ∀ (x : X), ↑f x ∈ Icc 0 1
x : X
hx : x ∈ t
⊢ ↑(BoundedContinuousFunction.const X a + (b - a) • f) x = Function.const X b x
[PROOFSTEP]
simp [hft hx]
[GOAL]
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
s t : Set X
hs : IsClosed s
ht : IsClosed t
hd : Disjoint s t
a b : ℝ
hle : a ≤ b
f : X →ᵇ ℝ
hfs : EqOn (↑f) 0 s
hft : EqOn (↑f) 1 t
hf01 : ∀ (x : X), ↑f x ∈ Icc 0 1
x : X
⊢ a ≤ ↑(BoundedContinuousFunction.const X a + (b - a) • f) x
[PROOFSTEP]
dsimp
[GOAL]
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
s t : Set X
hs : IsClosed s
ht : IsClosed t
hd : Disjoint s t
a b : ℝ
hle : a ≤ b
f : X →ᵇ ℝ
hfs : EqOn (↑f) 0 s
hft : EqOn (↑f) 1 t
hf01 : ∀ (x : X), ↑f x ∈ Icc 0 1
x : X
⊢ a ≤ a + (b - a) * ↑f x
[PROOFSTEP]
nlinarith [(hf01 x).1]
[GOAL]
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
s t : Set X
hs : IsClosed s
ht : IsClosed t
hd : Disjoint s t
a b : ℝ
hle : a ≤ b
f : X →ᵇ ℝ
hfs : EqOn (↑f) 0 s
hft : EqOn (↑f) 1 t
hf01 : ∀ (x : X), ↑f x ∈ Icc 0 1
x : X
⊢ ↑(BoundedContinuousFunction.const X a + (b - a) • f) x ≤ b
[PROOFSTEP]
dsimp
[GOAL]
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
s t : Set X
hs : IsClosed s
ht : IsClosed t
hd : Disjoint s t
a b : ℝ
hle : a ≤ b
f : X →ᵇ ℝ
hfs : EqOn (↑f) 0 s
hft : EqOn (↑f) 1 t
hf01 : ∀ (x : X), ↑f x ∈ Icc 0 1
x : X
⊢ a + (b - a) * ↑f x ≤ b
[PROOFSTEP]
nlinarith [(hf01 x).2]