[GOAL]
α : Type u_1
β : Type u_2
r r₁ r₂ : α → α → Prop
r' : β → β → Prop
s t : Set α
a b : α
inst✝ : IsTrichotomous α r
h : IsAntichain r s
⊢ Set.Subsingleton s
[PROOFSTEP]
rintro a ha b hb
[GOAL]
α : Type u_1
β : Type u_2
r r₁ r₂ : α → α → Prop
r' : β → β → Prop
s t : Set α
a✝ b✝ : α
inst✝ : IsTrichotomous α r
h : IsAntichain r s
a : α
ha : a ∈ s
b : α
hb : b ∈ s
⊢ a = b
[PROOFSTEP]
obtain hab | hab | hab := trichotomous_of r a b
[GOAL]
case inl
α : Type u_1
β : Type u_2
r r₁ r₂ : α → α → Prop
r' : β → β → Prop
s t : Set α
a✝ b✝ : α
inst✝ : IsTrichotomous α r
h : IsAntichain r s
a : α
ha : a ∈ s
b : α
hb : b ∈ s
hab : r a b
⊢ a = b
[PROOFSTEP]
exact h.eq ha hb hab
[GOAL]
case inr.inl
α : Type u_1
β : Type u_2
r r₁ r₂ : α → α → Prop
r' : β → β → Prop
s t : Set α
a✝ b✝ : α
inst✝ : IsTrichotomous α r
h : IsAntichain r s
a : α
ha : a ∈ s
b : α
hb : b ∈ s
hab : a = b
⊢ a = b
[PROOFSTEP]
exact hab
[GOAL]
case inr.inr
α : Type u_1
β : Type u_2
r r₁ r₂ : α → α → Prop
r' : β → β → Prop
s t : Set α
a✝ b✝ : α
inst✝ : IsTrichotomous α r
h : IsAntichain r s
a : α
ha : a ∈ s
b : α
hb : b ∈ s
hab : r b a
⊢ a = b
[PROOFSTEP]
exact h.eq' ha hb hab
[GOAL]
α : Type u_1
β : Type u_2
r r₁ r₂ : α → α → Prop
r' : β → β → Prop
s t : Set α
a b : α
hs : IsAntichain r s
f : α → β
h : ∀ ⦃a b : α⦄, r' (f a) (f b) → r a b
⊢ IsAntichain r' (f '' s)
[PROOFSTEP]
rintro _ ⟨b, hb, rfl⟩ _ ⟨c, hc, rfl⟩ hbc hr
[GOAL]
case intro.intro.intro.intro
α : Type u_1
β : Type u_2
r r₁ r₂ : α → α → Prop
r' : β → β → Prop
s t : Set α
a b✝ : α
hs : IsAntichain r s
f : α → β
h : ∀ ⦃a b : α⦄, r' (f a) (f b) → r a b
b : α
hb : b ∈ s
c : α
hc : c ∈ s
hbc : f b ≠ f c
hr : r' (f b) (f c)
⊢ False
[PROOFSTEP]
exact hs hb hc (ne_of_apply_ne _ hbc) (h hr)
[GOAL]
α : Type u_1
β : Type u_2
r r₁ r₂ : α → α → Prop
r' : β → β → Prop
s t : Set α
a b : α
hs : IsAntichain r s
φ : r ↪r r'
⊢ IsAntichain r' (↑φ '' s)
[PROOFSTEP]
intro b hb b' hb' h₁ h₂
[GOAL]
α : Type u_1
β : Type u_2
r r₁ r₂ : α → α → Prop
r' : β → β → Prop
s t : Set α
a b✝ : α
hs : IsAntichain r s
φ : r ↪r r'
b : β
hb : b ∈ ↑φ '' s
b' : β
hb' : b' ∈ ↑φ '' s
h₁ : b ≠ b'
h₂ : r' b b'
⊢ False
[PROOFSTEP]
rw [Set.mem_image] at hb hb'
[GOAL]
α : Type u_1
β : Type u_2
r r₁ r₂ : α → α → Prop
r' : β → β → Prop
s t : Set α
a b✝ : α
hs : IsAntichain r s
φ : r ↪r r'
b : β
hb : ∃ x, x ∈ s ∧ ↑φ x = b
b' : β
hb' : ∃ x, x ∈ s ∧ ↑φ x = b'
h₁ : b ≠ b'
h₂ : r' b b'
⊢ False
[PROOFSTEP]
obtain ⟨⟨a, has, rfl⟩, ⟨a', has', rfl⟩⟩ := hb, hb'
[GOAL]
case intro.intro.intro.intro
α : Type u_1
β : Type u_2
r r₁ r₂ : α → α → Prop
r' : β → β → Prop
s t : Set α
a✝ b : α
hs : IsAntichain r s
φ : r ↪r r'
a : α
has : a ∈ s
a' : α
has' : a' ∈ s
h₁ : ↑φ a ≠ ↑φ a'
h₂ : r' (↑φ a) (↑φ a')
⊢ False
[PROOFSTEP]
exact hs has has' (fun haa' => h₁ (by rw [haa'])) (φ.map_rel_iff.mp h₂)
[GOAL]
α : Type u_1
β : Type u_2
r r₁ r₂ : α → α → Prop
r' : β → β → Prop
s t : Set α
a✝ b : α
hs : IsAntichain r s
φ : r ↪r r'
a : α
has : a ∈ s
a' : α
has' : a' ∈ s
h₁ : ↑φ a ≠ ↑φ a'
h₂ : r' (↑φ a) (↑φ a')
haa' : a = a'
⊢ ↑φ a = ↑φ a'
[PROOFSTEP]
rw [haa']
[GOAL]
α : Type u_1
β : Type u_2
r r₁ r₂ : α → α → Prop
r' : β → β → Prop
s t : Set α
a b : α
inst✝ : Preorder α
⊢ s = {a} → IsAntichain (fun x x_1 => x ≤ x_1) s ∧ IsLeast s a
[PROOFSTEP]
rintro rfl
[GOAL]
α : Type u_1
β : Type u_2
r r₁ r₂ : α → α → Prop
r' : β → β → Prop
t : Set α
a b : α
inst✝ : Preorder α
⊢ IsAntichain (fun x x_1 => x ≤ x_1) {a} ∧ IsLeast {a} a
[PROOFSTEP]
exact ⟨isAntichain_singleton _ _, isLeast_singleton⟩
[GOAL]
α : Type u_1
β : Type u_2
r r₁ r₂ : α → α → Prop
r' : β → β → Prop
s t : Set α
a b : α
inst✝ : Preorder α
⊢ s = {a} → IsAntichain (fun x x_1 => x ≤ x_1) s ∧ IsGreatest s a
[PROOFSTEP]
rintro rfl
[GOAL]
α : Type u_1
β : Type u_2
r r₁ r₂ : α → α → Prop
r' : β → β → Prop
t : Set α
a b : α
inst✝ : Preorder α
⊢ IsAntichain (fun x x_1 => x ≤ x_1) {a} ∧ IsGreatest {a} a
[PROOFSTEP]
exact ⟨isAntichain_singleton _ _, isGreatest_singleton⟩
[GOAL]
α : Type u_1
β : Type u_2
r r₁ r₂ : α → α → Prop
r' : β → β → Prop
s t : Set α
a b : α
hs : IsStrongAntichain r s
f : α → β
hf : Surjective f
h : ∀ (a b : α), r' (f a) (f b) → r a b
⊢ IsStrongAntichain r' (f '' s)
[PROOFSTEP]
rintro _ ⟨a, ha, rfl⟩ _ ⟨b, hb, rfl⟩ hab c
[GOAL]
case intro.intro.intro.intro
α : Type u_1
β : Type u_2
r r₁ r₂ : α → α → Prop
r' : β → β → Prop
s t : Set α
a✝ b✝ : α
hs : IsStrongAntichain r s
f : α → β
hf : Surjective f
h : ∀ (a b : α), r' (f a) (f b) → r a b
a : α
ha : a ∈ s
b : α
hb : b ∈ s
hab : f a ≠ f b
c : β
⊢ ¬r' (f a) c ∨ ¬r' (f b) c
[PROOFSTEP]
obtain ⟨c, rfl⟩ := hf c
[GOAL]
case intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
r r₁ r₂ : α → α → Prop
r' : β → β → Prop
s t : Set α
a✝ b✝ : α
hs : IsStrongAntichain r s
f : α → β
hf : Surjective f
h : ∀ (a b : α), r' (f a) (f b) → r a b
a : α
ha : a ∈ s
b : α
hb : b ∈ s
hab : f a ≠ f b
c : α
⊢ ¬r' (f a) (f c) ∨ ¬r' (f b) (f c)
[PROOFSTEP]
exact (hs ha hb (ne_of_apply_ne _ hab) _).imp (mt <| h _ _) (mt <| h _ _)


[GOAL]
α : Type u_1
β : Type u_2
ι : Sort u_3
l l' la : Filter α
lb : Filter β
f : Filter α
⊢ smallSets f = generate (powerset '' f.sets)
[PROOFSTEP]
simp_rw [generate_eq_biInf, smallSets, iInf_image]
[GOAL]
α : Type u_1
β : Type u_2
ι : Sort u_3
l l' la : Filter α
lb : Filter β
f : Filter α
⊢ Filter.lift' f powerset = ⨅ (b : Set α) (_ : b ∈ f.sets), 𝓟 (𝒫 b)
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
ι : Sort u_3
l l' la : Filter α
lb : Filter β
p : Set α → Prop
⊢ (∀ᶠ (s : Set α) in smallSets l, p s) ↔ ∃ s, s ∈ l ∧ ∀ (t : Set α), t ⊆ s → p t
[PROOFSTEP]
rw [smallSets, eventually_lift'_iff]
[GOAL]
α : Type u_1
β : Type u_2
ι : Sort u_3
l l' la : Filter α
lb : Filter β
p : Set α → Prop
⊢ (∃ t, t ∈ l ∧ ∀ (y : Set α), y ∈ 𝒫 t → p y) ↔ ∃ s, s ∈ l ∧ ∀ (t : Set α), t ⊆ s → p t
case hh α : Type u_1 β : Type u_2 ι : Sort u_3 l l' la : Filter α lb : Filter β p : Set α → Prop ⊢ Monotone powerset
[PROOFSTEP]
rfl
[GOAL]
case hh
α : Type u_1
β : Type u_2
ι : Sort u_3
l l' la : Filter α
lb : Filter β
p : Set α → Prop
⊢ Monotone powerset
[PROOFSTEP]
exact monotone_powerset
[GOAL]
α : Type u_1
β : Type u_2
ι : Sort u_3
l l' la : Filter α
lb : Filter β
⊢ smallSets ⊥ = pure ∅
[PROOFSTEP]
rw [smallSets, lift'_bot, powerset_empty, principal_singleton]
[GOAL]
α : Type u_1
β : Type u_2
ι : Sort u_3
l l' la : Filter α
lb : Filter β
⊢ Monotone powerset
[PROOFSTEP]
exact monotone_powerset
[GOAL]
α : Type u_1
β : Type u_2
ι : Sort u_3
l l' la : Filter α
lb : Filter β
⊢ smallSets ⊤ = ⊤
[PROOFSTEP]
rw [smallSets, lift'_top, powerset_univ, principal_univ]
[GOAL]
α : Type u_1
β : Type u_2
ι : Sort u_3
l✝ l' la : Filter α
lb : Filter β
l : Filter α
⊢ NeBot (smallSets l)
[PROOFSTEP]
refine' (lift'_neBot_iff _).2 fun _ _ => powerset_nonempty
[GOAL]
α : Type u_1
β : Type u_2
ι : Sort u_3
l✝ l' la : Filter α
lb : Filter β
l : Filter α
⊢ Monotone powerset
[PROOFSTEP]
exact monotone_powerset
[GOAL]
α : Type u_1
β : Type u_2
ι : Sort u_3
l l' la : Filter α
lb : Filter β
s t : α → Set β
ht : Tendsto t la (smallSets lb)
hst : ∀ᶠ (x : α) in la, s x ⊆ t x
⊢ Tendsto s la (smallSets lb)
[PROOFSTEP]
rw [tendsto_smallSets_iff] at ht ⊢
[GOAL]
α : Type u_1
β : Type u_2
ι : Sort u_3
l l' la : Filter α
lb : Filter β
s t : α → Set β
ht : ∀ (t_1 : Set β), t_1 ∈ lb → ∀ᶠ (x : α) in la, t x ⊆ t_1
hst : ∀ᶠ (x : α) in la, s x ⊆ t x
⊢ ∀ (t : Set β), t ∈ lb → ∀ᶠ (x : α) in la, s x ⊆ t
[PROOFSTEP]
exact fun u hu => (ht u hu).mp (hst.mono fun _ hst ht => hst.trans ht)
[GOAL]
α : Type u_1
β : Type u_2
ι : Sort u_3
l l' la : Filter α
lb : Filter β
p : α → Prop
⊢ (∃ s, s ∈ l ∧ ∀ᶠ (x : α) in l', x ∈ s → p x) ↔ ∃ s, s ∈ l ∧ ∃ t, t ∈ l' ∧ ∀ (x : α), x ∈ t → x ∈ s → p x
[PROOFSTEP]
simp only [eventually_iff_exists_mem]
[GOAL]
α : Type u_1
β : Type u_2
ι : Sort u_3
l l' la : Filter α
lb : Filter β
p : α → Prop
⊢ (∃ s, s ∈ l ∧ ∃ t, t ∈ l' ∧ ∀ (x : α), x ∈ t → x ∈ s → p x) ↔ ∀ᶠ (x : α) in l ⊓ l', p x
[PROOFSTEP]
simp only [eventually_inf, and_comm, mem_inter_iff, ← and_imp]
[GOAL]
α : Type u_1
β : Type u_2
ι : Sort u_3
l l' la : Filter α
lb : Filter β
p : α → Prop
⊢ (∀ᶠ (s : Set α) in smallSets l, ∀ (x : α), x ∈ s → p x) ↔ ∀ᶠ (x : α) in l, p x
[PROOFSTEP]
simpa only [inf_top_eq, eventually_top] using @eventually_smallSets_eventually α l ⊤ p


[GOAL]
R : Type u
M : Type v
N : Type w
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Free R M
inst✝ : Finite R M
⊢ Fintype (ChooseBasisIndex R M)
[PROOFSTEP]
refine @Fintype.ofFinite _ ?_
[GOAL]
R : Type u
M : Type v
N : Type w
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Free R M
inst✝ : Finite R M
⊢ _root_.Finite (ChooseBasisIndex R M)
[PROOFSTEP]
cases subsingleton_or_nontrivial R
[GOAL]
case inl
R : Type u
M : Type v
N : Type w
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Free R M
inst✝ : Finite R M
h✝ : Subsingleton R
⊢ _root_.Finite (ChooseBasisIndex R M)
[PROOFSTEP]
have := Module.subsingleton R M
[GOAL]
case inl
R : Type u
M : Type v
N : Type w
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Free R M
inst✝ : Finite R M
h✝ : Subsingleton R
this : Subsingleton M
⊢ _root_.Finite (ChooseBasisIndex R M)
[PROOFSTEP]
rw [ChooseBasisIndex]
[GOAL]
case inl
R : Type u
M : Type v
N : Type w
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Free R M
inst✝ : Finite R M
h✝ : Subsingleton R
this : Subsingleton M
⊢ _root_.Finite ↑(Exists.choose (_ : ∃ S, Nonempty (Basis (↑S) R M)))
[PROOFSTEP]
infer_instance
[GOAL]
case inr
R : Type u
M : Type v
N : Type w
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Free R M
inst✝ : Finite R M
h✝ : Nontrivial R
⊢ _root_.Finite (ChooseBasisIndex R M)
[PROOFSTEP]
obtain ⟨s, hs⟩ := id ‹Module.Finite R M›
[GOAL]
case inr.mk.intro
R : Type u
M : Type v
N : Type w
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : Free R M
inst✝ : Finite R M
h✝ : Nontrivial R
s : Finset M
hs : Submodule.span R ↑s = ⊤
⊢ _root_.Finite (ChooseBasisIndex R M)
[PROOFSTEP]
exact basis_finite_of_finite_spans (↑s) s.finite_toSet hs (chooseBasis _ _)
[GOAL]
R✝ : Type u
M✝ : Type v
N : Type w
inst✝¹⁰ : CommRing R✝
inst✝⁹ : AddCommGroup M✝
inst✝⁸ : Module R✝ M✝
inst✝⁷ : Free R✝ M✝
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R✝ N
inst✝⁴ : Free R✝ N
R : Type u_1
M : Type u_2
ι : Type u_3
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : _root_.Finite ι
b : Basis ι R M
⊢ Finite R M
[PROOFSTEP]
cases nonempty_fintype ι
[GOAL]
case intro
R✝ : Type u
M✝ : Type v
N : Type w
inst✝¹⁰ : CommRing R✝
inst✝⁹ : AddCommGroup M✝
inst✝⁸ : Module R✝ M✝
inst✝⁷ : Free R✝ M✝
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R✝ N
inst✝⁴ : Free R✝ N
R : Type u_1
M : Type u_2
ι : Type u_3
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : _root_.Finite ι
b : Basis ι R M
val✝ : Fintype ι
⊢ Finite R M
[PROOFSTEP]
classical
refine' ⟨⟨Finset.univ.image b, _⟩⟩
simp only [Set.image_univ, Finset.coe_univ, Finset.coe_image, Basis.span_eq]
[GOAL]
case intro
R✝ : Type u
M✝ : Type v
N : Type w
inst✝¹⁰ : CommRing R✝
inst✝⁹ : AddCommGroup M✝
inst✝⁸ : Module R✝ M✝
inst✝⁷ : Free R✝ M✝
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R✝ N
inst✝⁴ : Free R✝ N
R : Type u_1
M : Type u_2
ι : Type u_3
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : _root_.Finite ι
b : Basis ι R M
val✝ : Fintype ι
⊢ Finite R M
[PROOFSTEP]
refine' ⟨⟨Finset.univ.image b, _⟩⟩
[GOAL]
case intro
R✝ : Type u
M✝ : Type v
N : Type w
inst✝¹⁰ : CommRing R✝
inst✝⁹ : AddCommGroup M✝
inst✝⁸ : Module R✝ M✝
inst✝⁷ : Free R✝ M✝
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R✝ N
inst✝⁴ : Free R✝ N
R : Type u_1
M : Type u_2
ι : Type u_3
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : _root_.Finite ι
b : Basis ι R M
val✝ : Fintype ι
⊢ Submodule.span R ↑(Finset.image (↑b) Finset.univ) = ⊤
[PROOFSTEP]
simp only [Set.image_univ, Finset.coe_univ, Finset.coe_image, Basis.span_eq]
[GOAL]
R : Type u
M : Type v
N : Type w
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : Free R M
inst✝⁴ : AddCommGroup N
inst✝³ : Module R N
inst✝² : Free R N
ι₁ : Type u_1
ι₂ : Type u_2
inst✝¹ : _root_.Finite ι₁
inst✝ : _root_.Finite ι₂
⊢ Finite R (Matrix ι₁ ι₂ R)
[PROOFSTEP]
cases nonempty_fintype ι₁
[GOAL]
case intro
R : Type u
M : Type v
N : Type w
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : Free R M
inst✝⁴ : AddCommGroup N
inst✝³ : Module R N
inst✝² : Free R N
ι₁ : Type u_1
ι₂ : Type u_2
inst✝¹ : _root_.Finite ι₁
inst✝ : _root_.Finite ι₂
val✝ : Fintype ι₁
⊢ Finite R (Matrix ι₁ ι₂ R)
[PROOFSTEP]
cases nonempty_fintype ι₂
[GOAL]
case intro.intro
R : Type u
M : Type v
N : Type w
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : Free R M
inst✝⁴ : AddCommGroup N
inst✝³ : Module R N
inst✝² : Free R N
ι₁ : Type u_1
ι₂ : Type u_2
inst✝¹ : _root_.Finite ι₁
inst✝ : _root_.Finite ι₂
val✝¹ : Fintype ι₁
val✝ : Fintype ι₂
⊢ Finite R (Matrix ι₁ ι₂ R)
[PROOFSTEP]
exact Module.Finite.of_basis (Pi.basis fun _ => Pi.basisFun R _)


[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝⁴ : PartialOrder α
inst✝³ : OrderTop α
inst✝² : Preorder β
inst✝¹ : OrderTop β
inst✝ : PseudoEpimorphismClass F α β
f : F
⊢ ↑f ⊤ = ⊤
[PROOFSTEP]
let ⟨b, h⟩ := exists_map_eq_of_map_le f (@le_top _ _ _ <| f ⊤)
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝⁴ : PartialOrder α
inst✝³ : OrderTop α
inst✝² : Preorder β
inst✝¹ : OrderTop β
inst✝ : PseudoEpimorphismClass F α β
f : F
b : α
h : ⊤ ≤ b ∧ ↑f b = ⊤
⊢ ↑f ⊤ = ⊤
[PROOFSTEP]
rw [← top_le_iff.1 h.1, h.2]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : Preorder γ
inst✝ : Preorder δ
f g : PseudoEpimorphism α β
h : (fun f => f.toFun) f = (fun f => f.toFun) g
⊢ f = g
[PROOFSTEP]
obtain ⟨⟨_, _⟩, _⟩ := f
[GOAL]
case mk.mk
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : Preorder γ
inst✝ : Preorder δ
g : PseudoEpimorphism α β
toFun✝ : α → β
monotone'✝ : Monotone toFun✝
exists_map_eq_of_map_le'✝ :
  ∀ ⦃a : α⦄ ⦃b : β⦄,
    OrderHom.toFun { toFun := toFun✝, monotone' := monotone'✝ } a ≤ b →
      ∃ c, a ≤ c ∧ OrderHom.toFun { toFun := toFun✝, monotone' := monotone'✝ } c = b
h :
  (fun f => f.toFun)
      { toOrderHom := { toFun := toFun✝, monotone' := monotone'✝ },
        exists_map_eq_of_map_le' := exists_map_eq_of_map_le'✝ } =
    (fun f => f.toFun) g
⊢ { toOrderHom := { toFun := toFun✝, monotone' := monotone'✝ },
      exists_map_eq_of_map_le' := exists_map_eq_of_map_le'✝ } =
    g
[PROOFSTEP]
obtain ⟨⟨_, _⟩, _⟩ := g
[GOAL]
case mk.mk.mk.mk
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : Preorder γ
inst✝ : Preorder δ
toFun✝¹ : α → β
monotone'✝¹ : Monotone toFun✝¹
exists_map_eq_of_map_le'✝¹ :
  ∀ ⦃a : α⦄ ⦃b : β⦄,
    OrderHom.toFun { toFun := toFun✝¹, monotone' := monotone'✝¹ } a ≤ b →
      ∃ c, a ≤ c ∧ OrderHom.toFun { toFun := toFun✝¹, monotone' := monotone'✝¹ } c = b
toFun✝ : α → β
monotone'✝ : Monotone toFun✝
exists_map_eq_of_map_le'✝ :
  ∀ ⦃a : α⦄ ⦃b : β⦄,
    OrderHom.toFun { toFun := toFun✝, monotone' := monotone'✝ } a ≤ b →
      ∃ c, a ≤ c ∧ OrderHom.toFun { toFun := toFun✝, monotone' := monotone'✝ } c = b
h :
  (fun f => f.toFun)
      { toOrderHom := { toFun := toFun✝¹, monotone' := monotone'✝¹ },
        exists_map_eq_of_map_le' := exists_map_eq_of_map_le'✝¹ } =
    (fun f => f.toFun)
      { toOrderHom := { toFun := toFun✝, monotone' := monotone'✝ },
        exists_map_eq_of_map_le' := exists_map_eq_of_map_le'✝ }
⊢ { toOrderHom := { toFun := toFun✝¹, monotone' := monotone'✝¹ },
      exists_map_eq_of_map_le' := exists_map_eq_of_map_le'✝¹ } =
    { toOrderHom := { toFun := toFun✝, monotone' := monotone'✝ },
      exists_map_eq_of_map_le' := exists_map_eq_of_map_le'✝ }
[PROOFSTEP]
congr
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : Preorder γ
inst✝ : Preorder δ
f : PseudoEpimorphism α β
f' : α → β
h : f' = ↑f
⊢ ∀ ⦃a : α⦄ ⦃b : β⦄,
    OrderHom.toFun (OrderHom.copy f.toOrderHom f' h) a ≤ b →
      ∃ c, a ≤ c ∧ OrderHom.toFun (OrderHom.copy f.toOrderHom f' h) c = b
[PROOFSTEP]
simpa only [h.symm, toFun_eq_coe] using f.exists_map_eq_of_map_le'
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : Preorder γ
inst✝ : Preorder δ
g : PseudoEpimorphism β γ
f : PseudoEpimorphism α β
a : α
b : γ
h₀ : OrderHom.toFun (OrderHom.comp g.toOrderHom f.toOrderHom) a ≤ b
⊢ ∃ c, a ≤ c ∧ OrderHom.toFun (OrderHom.comp g.toOrderHom f.toOrderHom) c = b
[PROOFSTEP]
obtain ⟨b, h₁, rfl⟩ := g.exists_map_eq_of_map_le' h₀
[GOAL]
case intro.intro
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : Preorder γ
inst✝ : Preorder δ
g : PseudoEpimorphism β γ
f : PseudoEpimorphism α β
a : α
b : β
h₁ : ↑f.toOrderHom a ≤ b
h₀ : OrderHom.toFun (OrderHom.comp g.toOrderHom f.toOrderHom) a ≤ OrderHom.toFun g.toOrderHom b
⊢ ∃ c, a ≤ c ∧ OrderHom.toFun (OrderHom.comp g.toOrderHom f.toOrderHom) c = OrderHom.toFun g.toOrderHom b
[PROOFSTEP]
obtain ⟨b, h₂, rfl⟩ := f.exists_map_eq_of_map_le' h₁
[GOAL]
case intro.intro.intro.intro
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : Preorder γ
inst✝ : Preorder δ
g : PseudoEpimorphism β γ
f : PseudoEpimorphism α β
a b : α
h₂ : a ≤ b
h₁ : ↑f.toOrderHom a ≤ OrderHom.toFun f.toOrderHom b
h₀ :
  OrderHom.toFun (OrderHom.comp g.toOrderHom f.toOrderHom) a ≤
    OrderHom.toFun g.toOrderHom (OrderHom.toFun f.toOrderHom b)
⊢ ∃ c,
    a ≤ c ∧
      OrderHom.toFun (OrderHom.comp g.toOrderHom f.toOrderHom) c =
        OrderHom.toFun g.toOrderHom (OrderHom.toFun f.toOrderHom b)
[PROOFSTEP]
exact ⟨b, h₂, rfl⟩
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : Preorder γ
inst✝ : Preorder δ
g : PseudoEpimorphism β γ
f₁ f₂ : PseudoEpimorphism α β
hg : Injective ↑g
h : comp g f₁ = comp g f₂
a : α
⊢ ↑g (↑f₁ a) = ↑g (↑f₂ a)
[PROOFSTEP]
rw [← comp_apply, h, comp_apply]
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝⁷ : TopologicalSpace α
inst✝⁶ : Preorder α
inst✝⁵ : TopologicalSpace β
inst✝⁴ : Preorder β
inst✝³ : TopologicalSpace γ
inst✝² : Preorder γ
inst✝¹ : TopologicalSpace δ
inst✝ : Preorder δ
f g : EsakiaHom α β
h : (fun f => f.toFun) f = (fun f => f.toFun) g
⊢ f = g
[PROOFSTEP]
obtain ⟨⟨⟨_, _⟩, _⟩, _⟩ := f
[GOAL]
case mk.mk.mk
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝⁷ : TopologicalSpace α
inst✝⁶ : Preorder α
inst✝⁵ : TopologicalSpace β
inst✝⁴ : Preorder β
inst✝³ : TopologicalSpace γ
inst✝² : Preorder γ
inst✝¹ : TopologicalSpace δ
inst✝ : Preorder δ
g : EsakiaHom α β
toFun✝ : α → β
monotone'✝ : Monotone toFun✝
continuous_toFun✝ : Continuous { toFun := toFun✝, monotone' := monotone'✝ }.toFun
exists_map_eq_of_map_le'✝ :
  ∀ ⦃a : α⦄ ⦃b : β⦄,
    OrderHom.toFun
          { toOrderHom := { toFun := toFun✝, monotone' := monotone'✝ },
              continuous_toFun := continuous_toFun✝ }.toOrderHom
          a ≤
        b →
      ∃ c,
        a ≤ c ∧
          OrderHom.toFun
              { toOrderHom := { toFun := toFun✝, monotone' := monotone'✝ },
                  continuous_toFun := continuous_toFun✝ }.toOrderHom
              c =
            b
h :
  (fun f => f.toFun)
      {
        toContinuousOrderHom :=
          { toOrderHom := { toFun := toFun✝, monotone' := monotone'✝ }, continuous_toFun := continuous_toFun✝ },
        exists_map_eq_of_map_le' := exists_map_eq_of_map_le'✝ } =
    (fun f => f.toFun) g
⊢ {
      toContinuousOrderHom :=
        { toOrderHom := { toFun := toFun✝, monotone' := monotone'✝ }, continuous_toFun := continuous_toFun✝ },
      exists_map_eq_of_map_le' := exists_map_eq_of_map_le'✝ } =
    g
[PROOFSTEP]
obtain ⟨⟨⟨_, _⟩, _⟩, _⟩ := g
[GOAL]
case mk.mk.mk.mk.mk.mk
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝⁷ : TopologicalSpace α
inst✝⁶ : Preorder α
inst✝⁵ : TopologicalSpace β
inst✝⁴ : Preorder β
inst✝³ : TopologicalSpace γ
inst✝² : Preorder γ
inst✝¹ : TopologicalSpace δ
inst✝ : Preorder δ
toFun✝¹ : α → β
monotone'✝¹ : Monotone toFun✝¹
continuous_toFun✝¹ : Continuous { toFun := toFun✝¹, monotone' := monotone'✝¹ }.toFun
exists_map_eq_of_map_le'✝¹ :
  ∀ ⦃a : α⦄ ⦃b : β⦄,
    OrderHom.toFun
          { toOrderHom := { toFun := toFun✝¹, monotone' := monotone'✝¹ },
              continuous_toFun := continuous_toFun✝¹ }.toOrderHom
          a ≤
        b →
      ∃ c,
        a ≤ c ∧
          OrderHom.toFun
              { toOrderHom := { toFun := toFun✝¹, monotone' := monotone'✝¹ },
                  continuous_toFun := continuous_toFun✝¹ }.toOrderHom
              c =
            b
toFun✝ : α → β
monotone'✝ : Monotone toFun✝
continuous_toFun✝ : Continuous { toFun := toFun✝, monotone' := monotone'✝ }.toFun
exists_map_eq_of_map_le'✝ :
  ∀ ⦃a : α⦄ ⦃b : β⦄,
    OrderHom.toFun
          { toOrderHom := { toFun := toFun✝, monotone' := monotone'✝ },
              continuous_toFun := continuous_toFun✝ }.toOrderHom
          a ≤
        b →
      ∃ c,
        a ≤ c ∧
          OrderHom.toFun
              { toOrderHom := { toFun := toFun✝, monotone' := monotone'✝ },
                  continuous_toFun := continuous_toFun✝ }.toOrderHom
              c =
            b
h :
  (fun f => f.toFun)
      {
        toContinuousOrderHom :=
          { toOrderHom := { toFun := toFun✝¹, monotone' := monotone'✝¹ }, continuous_toFun := continuous_toFun✝¹ },
        exists_map_eq_of_map_le' := exists_map_eq_of_map_le'✝¹ } =
    (fun f => f.toFun)
      {
        toContinuousOrderHom :=
          { toOrderHom := { toFun := toFun✝, monotone' := monotone'✝ }, continuous_toFun := continuous_toFun✝ },
        exists_map_eq_of_map_le' := exists_map_eq_of_map_le'✝ }
⊢ {
      toContinuousOrderHom :=
        { toOrderHom := { toFun := toFun✝¹, monotone' := monotone'✝¹ }, continuous_toFun := continuous_toFun✝¹ },
      exists_map_eq_of_map_le' := exists_map_eq_of_map_le'✝¹ } =
    {
      toContinuousOrderHom :=
        { toOrderHom := { toFun := toFun✝, monotone' := monotone'✝ }, continuous_toFun := continuous_toFun✝ },
      exists_map_eq_of_map_le' := exists_map_eq_of_map_le'✝ }
[PROOFSTEP]
congr
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝⁷ : TopologicalSpace α
inst✝⁶ : Preorder α
inst✝⁵ : TopologicalSpace β
inst✝⁴ : Preorder β
inst✝³ : TopologicalSpace γ
inst✝² : Preorder γ
inst✝¹ : TopologicalSpace δ
inst✝ : Preorder δ
f : EsakiaHom α β
f' : α → β
h : f' = ↑f
⊢ ∀ ⦃a : α⦄ ⦃b : β⦄,
    OrderHom.toFun (ContinuousOrderHom.copy f.toContinuousOrderHom f' h).toOrderHom a ≤ b →
      ∃ c, a ≤ c ∧ OrderHom.toFun (ContinuousOrderHom.copy f.toContinuousOrderHom f' h).toOrderHom c = b
[PROOFSTEP]
simpa only [h.symm, toFun_eq_coe] using f.exists_map_eq_of_map_le'
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝⁷ : TopologicalSpace α
inst✝⁶ : Preorder α
inst✝⁵ : TopologicalSpace β
inst✝⁴ : Preorder β
inst✝³ : TopologicalSpace γ
inst✝² : Preorder γ
inst✝¹ : TopologicalSpace δ
inst✝ : Preorder δ
g : EsakiaHom β γ
f : EsakiaHom α β
a : α
b : γ
h₀ : OrderHom.toFun (ContinuousOrderHom.comp g.toContinuousOrderHom f.toContinuousOrderHom).toOrderHom a ≤ b
⊢ ∃ c, a ≤ c ∧ OrderHom.toFun (ContinuousOrderHom.comp g.toContinuousOrderHom f.toContinuousOrderHom).toOrderHom c = b
[PROOFSTEP]
obtain ⟨b, h₁, rfl⟩ := g.exists_map_eq_of_map_le' h₀
[GOAL]
case intro.intro
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝⁷ : TopologicalSpace α
inst✝⁶ : Preorder α
inst✝⁵ : TopologicalSpace β
inst✝⁴ : Preorder β
inst✝³ : TopologicalSpace γ
inst✝² : Preorder γ
inst✝¹ : TopologicalSpace δ
inst✝ : Preorder δ
g : EsakiaHom β γ
f : EsakiaHom α β
a : α
b : β
h₁ : ↑f.toOrderHom a ≤ b
h₀ :
  OrderHom.toFun (ContinuousOrderHom.comp g.toContinuousOrderHom f.toContinuousOrderHom).toOrderHom a ≤
    OrderHom.toFun g.toOrderHom b
⊢ ∃ c,
    a ≤ c ∧
      OrderHom.toFun (ContinuousOrderHom.comp g.toContinuousOrderHom f.toContinuousOrderHom).toOrderHom c =
        OrderHom.toFun g.toOrderHom b
[PROOFSTEP]
obtain ⟨b, h₂, rfl⟩ := f.exists_map_eq_of_map_le' h₁
[GOAL]
case intro.intro.intro.intro
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝⁷ : TopologicalSpace α
inst✝⁶ : Preorder α
inst✝⁵ : TopologicalSpace β
inst✝⁴ : Preorder β
inst✝³ : TopologicalSpace γ
inst✝² : Preorder γ
inst✝¹ : TopologicalSpace δ
inst✝ : Preorder δ
g : EsakiaHom β γ
f : EsakiaHom α β
a b : α
h₂ : a ≤ b
h₁ : ↑f.toOrderHom a ≤ OrderHom.toFun f.toOrderHom b
h₀ :
  OrderHom.toFun (ContinuousOrderHom.comp g.toContinuousOrderHom f.toContinuousOrderHom).toOrderHom a ≤
    OrderHom.toFun g.toOrderHom (OrderHom.toFun f.toOrderHom b)
⊢ ∃ c,
    a ≤ c ∧
      OrderHom.toFun (ContinuousOrderHom.comp g.toContinuousOrderHom f.toContinuousOrderHom).toOrderHom c =
        OrderHom.toFun g.toOrderHom (OrderHom.toFun f.toOrderHom b)
[PROOFSTEP]
exact ⟨b, h₂, rfl⟩
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝⁷ : TopologicalSpace α
inst✝⁶ : Preorder α
inst✝⁵ : TopologicalSpace β
inst✝⁴ : Preorder β
inst✝³ : TopologicalSpace γ
inst✝² : Preorder γ
inst✝¹ : TopologicalSpace δ
inst✝ : Preorder δ
g : EsakiaHom β γ
f₁ f₂ : EsakiaHom α β
hg : Injective ↑g
h : comp g f₁ = comp g f₂
a : α
⊢ ↑g (↑f₁ a) = ↑g (↑f₂ a)
[PROOFSTEP]
rw [← comp_apply, h, comp_apply]


[GOAL]
ι : Type u_1
X : Type u_2
inst✝ : EMetricSpace X
K U : ι → Set X
hK : ∀ (i : ι), IsClosed (K i)
hU : ∀ (i : ι), IsOpen (U i)
hKU : ∀ (i : ι), K i ⊆ U i
hfin : LocallyFinite K
x : X
⊢ ∀ᶠ (p : ℝ≥0∞ × X) in 𝓝 0 ×ˢ 𝓝 x, ∀ (i : ι), p.snd ∈ K i → closedBall p.snd p.fst ⊆ U i
[PROOFSTEP]
suffices ∀ i, x ∈ K i → ∀ᶠ p : ℝ≥0∞ × X in 𝓝 0 ×ˢ 𝓝 x, closedBall p.2 p.1 ⊆ U i
  by
  apply
    mp_mem ((eventually_all_finite (hfin.point_finite x)).2 this)
      (mp_mem (@tendsto_snd ℝ≥0∞ _ (𝓝 0) _ _ (hfin.iInter_compl_mem_nhds hK x)) _)
  apply univ_mem'
  rintro ⟨r, y⟩ hxy hyU i hi
  simp only [mem_iInter, mem_compl_iff, not_imp_not, mem_preimage] at hxy
  exact hyU _ (hxy _ hi)
[GOAL]
ι : Type u_1
X : Type u_2
inst✝ : EMetricSpace X
K U : ι → Set X
hK : ∀ (i : ι), IsClosed (K i)
hU : ∀ (i : ι), IsOpen (U i)
hKU : ∀ (i : ι), K i ⊆ U i
hfin : LocallyFinite K
x : X
this : ∀ (i : ι), x ∈ K i → ∀ᶠ (p : ℝ≥0∞ × X) in 𝓝 0 ×ˢ 𝓝 x, closedBall p.snd p.fst ⊆ U i
⊢ ∀ᶠ (p : ℝ≥0∞ × X) in 𝓝 0 ×ˢ 𝓝 x, ∀ (i : ι), p.snd ∈ K i → closedBall p.snd p.fst ⊆ U i
[PROOFSTEP]
apply
  mp_mem ((eventually_all_finite (hfin.point_finite x)).2 this)
    (mp_mem (@tendsto_snd ℝ≥0∞ _ (𝓝 0) _ _ (hfin.iInter_compl_mem_nhds hK x)) _)
[GOAL]
ι : Type u_1
X : Type u_2
inst✝ : EMetricSpace X
K U : ι → Set X
hK : ∀ (i : ι), IsClosed (K i)
hU : ∀ (i : ι), IsOpen (U i)
hKU : ∀ (i : ι), K i ⊆ U i
hfin : LocallyFinite K
x : X
this : ∀ (i : ι), x ∈ K i → ∀ᶠ (p : ℝ≥0∞ × X) in 𝓝 0 ×ˢ 𝓝 x, closedBall p.snd p.fst ⊆ U i
⊢ {x_1 |
      x_1 ∈ Prod.snd ⁻¹' ⋂ (i : ι) (_ : ¬x ∈ K i), (K i)ᶜ →
        x_1 ∈
          {x_2 |
            x_2 ∈ {x_3 | (fun x_4 => ∀ (i : ι), i ∈ {b | x ∈ K b} → closedBall x_4.snd x_4.fst ⊆ U i) x_3} →
              x_2 ∈ {x | (fun p => ∀ (i : ι), p.snd ∈ K i → closedBall p.snd p.fst ⊆ U i) x}}} ∈
    𝓝 0 ×ˢ 𝓝 x
[PROOFSTEP]
apply univ_mem'
[GOAL]
case h
ι : Type u_1
X : Type u_2
inst✝ : EMetricSpace X
K U : ι → Set X
hK : ∀ (i : ι), IsClosed (K i)
hU : ∀ (i : ι), IsOpen (U i)
hKU : ∀ (i : ι), K i ⊆ U i
hfin : LocallyFinite K
x : X
this : ∀ (i : ι), x ∈ K i → ∀ᶠ (p : ℝ≥0∞ × X) in 𝓝 0 ×ˢ 𝓝 x, closedBall p.snd p.fst ⊆ U i
⊢ ∀ (a : ℝ≥0∞ × X),
    a ∈
      {x_1 |
        x_1 ∈ Prod.snd ⁻¹' ⋂ (i : ι) (_ : ¬x ∈ K i), (K i)ᶜ →
          x_1 ∈
            {x_2 |
              x_2 ∈ {x_3 | (fun x_4 => ∀ (i : ι), i ∈ {b | x ∈ K b} → closedBall x_4.snd x_4.fst ⊆ U i) x_3} →
                x_2 ∈ {x | (fun p => ∀ (i : ι), p.snd ∈ K i → closedBall p.snd p.fst ⊆ U i) x}}}
[PROOFSTEP]
rintro ⟨r, y⟩ hxy hyU i hi
[GOAL]
case h.mk
ι : Type u_1
X : Type u_2
inst✝ : EMetricSpace X
K U : ι → Set X
hK : ∀ (i : ι), IsClosed (K i)
hU : ∀ (i : ι), IsOpen (U i)
hKU : ∀ (i : ι), K i ⊆ U i
hfin : LocallyFinite K
x : X
this : ∀ (i : ι), x ∈ K i → ∀ᶠ (p : ℝ≥0∞ × X) in 𝓝 0 ×ˢ 𝓝 x, closedBall p.snd p.fst ⊆ U i
r : ℝ≥0∞
y : X
hxy : (r, y) ∈ Prod.snd ⁻¹' ⋂ (i : ι) (_ : ¬x ∈ K i), (K i)ᶜ
hyU : (r, y) ∈ {x_1 | (fun x_2 => ∀ (i : ι), i ∈ {b | x ∈ K b} → closedBall x_2.snd x_2.fst ⊆ U i) x_1}
i : ι
hi : (r, y).snd ∈ K i
⊢ closedBall (r, y).snd (r, y).fst ⊆ U i
[PROOFSTEP]
simp only [mem_iInter, mem_compl_iff, not_imp_not, mem_preimage] at hxy
[GOAL]
case h.mk
ι : Type u_1
X : Type u_2
inst✝ : EMetricSpace X
K U : ι → Set X
hK : ∀ (i : ι), IsClosed (K i)
hU : ∀ (i : ι), IsOpen (U i)
hKU : ∀ (i : ι), K i ⊆ U i
hfin : LocallyFinite K
x : X
this : ∀ (i : ι), x ∈ K i → ∀ᶠ (p : ℝ≥0∞ × X) in 𝓝 0 ×ˢ 𝓝 x, closedBall p.snd p.fst ⊆ U i
r : ℝ≥0∞
y : X
hyU : (r, y) ∈ {x_1 | (fun x_2 => ∀ (i : ι), i ∈ {b | x ∈ K b} → closedBall x_2.snd x_2.fst ⊆ U i) x_1}
i : ι
hi : (r, y).snd ∈ K i
hxy : ∀ (i : ι), y ∈ K i → x ∈ K i
⊢ closedBall (r, y).snd (r, y).fst ⊆ U i
[PROOFSTEP]
exact hyU _ (hxy _ hi)
[GOAL]
ι : Type u_1
X : Type u_2
inst✝ : EMetricSpace X
K U : ι → Set X
hK : ∀ (i : ι), IsClosed (K i)
hU : ∀ (i : ι), IsOpen (U i)
hKU : ∀ (i : ι), K i ⊆ U i
hfin : LocallyFinite K
x : X
⊢ ∀ (i : ι), x ∈ K i → ∀ᶠ (p : ℝ≥0∞ × X) in 𝓝 0 ×ˢ 𝓝 x, closedBall p.snd p.fst ⊆ U i
[PROOFSTEP]
intro i hi
[GOAL]
ι : Type u_1
X : Type u_2
inst✝ : EMetricSpace X
K U : ι → Set X
hK : ∀ (i : ι), IsClosed (K i)
hU : ∀ (i : ι), IsOpen (U i)
hKU : ∀ (i : ι), K i ⊆ U i
hfin : LocallyFinite K
x : X
i : ι
hi : x ∈ K i
⊢ ∀ᶠ (p : ℝ≥0∞ × X) in 𝓝 0 ×ˢ 𝓝 x, closedBall p.snd p.fst ⊆ U i
[PROOFSTEP]
rcases nhds_basis_closed_eball.mem_iff.1 ((hU i).mem_nhds <| hKU i hi) with ⟨R, hR₀, hR⟩
[GOAL]
case intro.intro
ι : Type u_1
X : Type u_2
inst✝ : EMetricSpace X
K U : ι → Set X
hK : ∀ (i : ι), IsClosed (K i)
hU : ∀ (i : ι), IsOpen (U i)
hKU : ∀ (i : ι), K i ⊆ U i
hfin : LocallyFinite K
x : X
i : ι
hi : x ∈ K i
R : ℝ≥0∞
hR₀ : 0 < R
hR : closedBall x R ⊆ U i
⊢ ∀ᶠ (p : ℝ≥0∞ × X) in 𝓝 0 ×ˢ 𝓝 x, closedBall p.snd p.fst ⊆ U i
[PROOFSTEP]
rcases ENNReal.lt_iff_exists_nnreal_btwn.mp hR₀ with ⟨r, hr₀, hrR⟩
[GOAL]
case intro.intro.intro.intro
ι : Type u_1
X : Type u_2
inst✝ : EMetricSpace X
K U : ι → Set X
hK : ∀ (i : ι), IsClosed (K i)
hU : ∀ (i : ι), IsOpen (U i)
hKU : ∀ (i : ι), K i ⊆ U i
hfin : LocallyFinite K
x : X
i : ι
hi : x ∈ K i
R : ℝ≥0∞
hR₀ : 0 < R
hR : closedBall x R ⊆ U i
r : ℝ≥0
hr₀ : 0 < ↑r
hrR : ↑r < R
⊢ ∀ᶠ (p : ℝ≥0∞ × X) in 𝓝 0 ×ˢ 𝓝 x, closedBall p.snd p.fst ⊆ U i
[PROOFSTEP]
filter_upwards [prod_mem_prod (eventually_lt_nhds hr₀) (closedBall_mem_nhds x (tsub_pos_iff_lt.2 hrR))] with p hp z hz
[GOAL]
case h
ι : Type u_1
X : Type u_2
inst✝ : EMetricSpace X
K U : ι → Set X
hK : ∀ (i : ι), IsClosed (K i)
hU : ∀ (i : ι), IsOpen (U i)
hKU : ∀ (i : ι), K i ⊆ U i
hfin : LocallyFinite K
x : X
i : ι
hi : x ∈ K i
R : ℝ≥0∞
hR₀ : 0 < R
hR : closedBall x R ⊆ U i
r : ℝ≥0
hr₀ : 0 < ↑r
hrR : ↑r < R
p : ℝ≥0∞ × X
hp : p ∈ {x | x < ↑r} ×ˢ closedBall x (R - ↑r)
z : X
hz : z ∈ closedBall p.snd p.fst
⊢ z ∈ U i
[PROOFSTEP]
apply hR
[GOAL]
case h.a
ι : Type u_1
X : Type u_2
inst✝ : EMetricSpace X
K U : ι → Set X
hK : ∀ (i : ι), IsClosed (K i)
hU : ∀ (i : ι), IsOpen (U i)
hKU : ∀ (i : ι), K i ⊆ U i
hfin : LocallyFinite K
x : X
i : ι
hi : x ∈ K i
R : ℝ≥0∞
hR₀ : 0 < R
hR : closedBall x R ⊆ U i
r : ℝ≥0
hr₀ : 0 < ↑r
hrR : ↑r < R
p : ℝ≥0∞ × X
hp : p ∈ {x | x < ↑r} ×ˢ closedBall x (R - ↑r)
z : X
hz : z ∈ closedBall p.snd p.fst
⊢ z ∈ closedBall x R
[PROOFSTEP]
calc
  edist z x ≤ edist z p.2 + edist p.2 x := edist_triangle _ _ _
  _ ≤ p.1 + (R - p.1) := (add_le_add hz <| le_trans hp.2 <| tsub_le_tsub_left hp.1.out.le _)
  _ = R := add_tsub_cancel_of_le (lt_trans (by exact hp.1) hrR).le
[GOAL]
ι : Type u_1
X : Type u_2
inst✝ : EMetricSpace X
K U : ι → Set X
hK : ∀ (i : ι), IsClosed (K i)
hU : ∀ (i : ι), IsOpen (U i)
hKU : ∀ (i : ι), K i ⊆ U i
hfin : LocallyFinite K
x : X
i : ι
hi : x ∈ K i
R : ℝ≥0∞
hR₀ : 0 < R
hR : closedBall x R ⊆ U i
r : ℝ≥0
hr₀ : 0 < ↑r
hrR : ↑r < R
p : ℝ≥0∞ × X
hp : p ∈ {x | x < ↑r} ×ˢ closedBall x (R - ↑r)
z : X
hz : z ∈ closedBall p.snd p.fst
⊢ p.fst < ↑r
[PROOFSTEP]
exact hp.1
[GOAL]
ι : Type u_1
X : Type u_2
inst✝ : EMetricSpace X
K U : ι → Set X
hK : ∀ (i : ι), IsClosed (K i)
hU : ∀ (i : ι), IsOpen (U i)
hKU : ∀ (i : ι), K i ⊆ U i
hfin : LocallyFinite K
x : X
⊢ ∃ r, ∀ᶠ (y : X) in 𝓝 x, r ∈ Ioi 0 ∩ ENNReal.ofReal ⁻¹' ⋂ (i : ι) (_ : y ∈ K i), {r | closedBall y r ⊆ U i}
[PROOFSTEP]
have :=
  (ENNReal.continuous_ofReal.tendsto' 0 0 ENNReal.ofReal_zero).eventually
    (eventually_nhds_zero_forall_closedBall_subset hK hU hKU hfin x).curry
[GOAL]
ι : Type u_1
X : Type u_2
inst✝ : EMetricSpace X
K U : ι → Set X
hK : ∀ (i : ι), IsClosed (K i)
hU : ∀ (i : ι), IsOpen (U i)
hKU : ∀ (i : ι), K i ⊆ U i
hfin : LocallyFinite K
x : X
this :
  ∀ᶠ (x_1 : ℝ) in 𝓝 0,
    ∀ᶠ (y : X) in 𝓝 x,
      ∀ (i : ι),
        (ENNReal.ofReal x_1, y).snd ∈ K i → closedBall (ENNReal.ofReal x_1, y).snd (ENNReal.ofReal x_1, y).fst ⊆ U i
⊢ ∃ r, ∀ᶠ (y : X) in 𝓝 x, r ∈ Ioi 0 ∩ ENNReal.ofReal ⁻¹' ⋂ (i : ι) (_ : y ∈ K i), {r | closedBall y r ⊆ U i}
[PROOFSTEP]
rcases this.exists_gt with ⟨r, hr0, hr⟩
[GOAL]
case intro.intro
ι : Type u_1
X : Type u_2
inst✝ : EMetricSpace X
K U : ι → Set X
hK : ∀ (i : ι), IsClosed (K i)
hU : ∀ (i : ι), IsOpen (U i)
hKU : ∀ (i : ι), K i ⊆ U i
hfin : LocallyFinite K
x : X
this :
  ∀ᶠ (x_1 : ℝ) in 𝓝 0,
    ∀ᶠ (y : X) in 𝓝 x,
      ∀ (i : ι),
        (ENNReal.ofReal x_1, y).snd ∈ K i → closedBall (ENNReal.ofReal x_1, y).snd (ENNReal.ofReal x_1, y).fst ⊆ U i
r : ℝ
hr0 : r > 0
hr :
  ∀ᶠ (y : X) in 𝓝 x,
    ∀ (i : ι), (ENNReal.ofReal r, y).snd ∈ K i → closedBall (ENNReal.ofReal r, y).snd (ENNReal.ofReal r, y).fst ⊆ U i
⊢ ∃ r, ∀ᶠ (y : X) in 𝓝 x, r ∈ Ioi 0 ∩ ENNReal.ofReal ⁻¹' ⋂ (i : ι) (_ : y ∈ K i), {r | closedBall y r ⊆ U i}
[PROOFSTEP]
refine' ⟨r, hr.mono fun y hy => ⟨hr0, _⟩⟩
[GOAL]
case intro.intro
ι : Type u_1
X : Type u_2
inst✝ : EMetricSpace X
K U : ι → Set X
hK : ∀ (i : ι), IsClosed (K i)
hU : ∀ (i : ι), IsOpen (U i)
hKU : ∀ (i : ι), K i ⊆ U i
hfin : LocallyFinite K
x : X
this :
  ∀ᶠ (x_1 : ℝ) in 𝓝 0,
    ∀ᶠ (y : X) in 𝓝 x,
      ∀ (i : ι),
        (ENNReal.ofReal x_1, y).snd ∈ K i → closedBall (ENNReal.ofReal x_1, y).snd (ENNReal.ofReal x_1, y).fst ⊆ U i
r : ℝ
hr0 : r > 0
hr :
  ∀ᶠ (y : X) in 𝓝 x,
    ∀ (i : ι), (ENNReal.ofReal r, y).snd ∈ K i → closedBall (ENNReal.ofReal r, y).snd (ENNReal.ofReal r, y).fst ⊆ U i
y : X
hy : ∀ (i : ι), (ENNReal.ofReal r, y).snd ∈ K i → closedBall (ENNReal.ofReal r, y).snd (ENNReal.ofReal r, y).fst ⊆ U i
⊢ r ∈ ENNReal.ofReal ⁻¹' ⋂ (i : ι) (_ : y ∈ K i), {r | closedBall y r ⊆ U i}
[PROOFSTEP]
rwa [mem_preimage, mem_iInter₂]
[GOAL]
ι : Type u_1
X : Type u_2
inst✝ : EMetricSpace X
K U : ι → Set X
hK : ∀ (i : ι), IsClosed (K i)
hU : ∀ (i : ι), IsOpen (U i)
hKU : ∀ (i : ι), K i ⊆ U i
hfin : LocallyFinite K
⊢ ∃ δ, (∀ (x : X), 0 < ↑δ x) ∧ ∀ (i : ι) (x : X), x ∈ K i → closedBall x (ENNReal.ofReal (↑δ x)) ⊆ U i
[PROOFSTEP]
simpa only [mem_inter_iff, forall_and, mem_preimage, mem_iInter, @forall_swap ι X] using
  exists_continuous_forall_mem_convex_of_local_const exists_forall_closedBall_subset_aux₂
    (exists_forall_closedBall_subset_aux₁ hK hU hKU hfin)
[GOAL]
ι : Type u_1
X : Type u_2
inst✝ : EMetricSpace X
K U : ι → Set X
hK : ∀ (i : ι), IsClosed (K i)
hU : ∀ (i : ι), IsOpen (U i)
hKU : ∀ (i : ι), K i ⊆ U i
hfin : LocallyFinite K
⊢ ∃ δ, (∀ (x : X), 0 < ↑δ x) ∧ ∀ (i : ι) (x : X), x ∈ K i → closedBall x ↑(↑δ x) ⊆ U i
[PROOFSTEP]
rcases exists_continuous_real_forall_closedBall_subset hK hU hKU hfin with ⟨δ, hδ₀, hδ⟩
[GOAL]
case intro.intro
ι : Type u_1
X : Type u_2
inst✝ : EMetricSpace X
K U : ι → Set X
hK : ∀ (i : ι), IsClosed (K i)
hU : ∀ (i : ι), IsOpen (U i)
hKU : ∀ (i : ι), K i ⊆ U i
hfin : LocallyFinite K
δ : C(X, ℝ)
hδ₀ : ∀ (x : X), 0 < ↑δ x
hδ : ∀ (i : ι) (x : X), x ∈ K i → closedBall x (ENNReal.ofReal (↑δ x)) ⊆ U i
⊢ ∃ δ, (∀ (x : X), 0 < ↑δ x) ∧ ∀ (i : ι) (x : X), x ∈ K i → closedBall x ↑(↑δ x) ⊆ U i
[PROOFSTEP]
lift δ to C(X, ℝ≥0) using fun x => (hδ₀ x).le
[GOAL]
case intro.intro.intro
ι : Type u_1
X : Type u_2
inst✝ : EMetricSpace X
K U : ι → Set X
hK : ∀ (i : ι), IsClosed (K i)
hU : ∀ (i : ι), IsOpen (U i)
hKU : ∀ (i : ι), K i ⊆ U i
hfin : LocallyFinite K
δ : C(X, ℝ≥0)
hδ₀ : ∀ (x : X), 0 < ↑(ContinuousMap.comp ContinuousMap.coeNNRealReal δ) x
hδ :
  ∀ (i : ι) (x : X),
    x ∈ K i → closedBall x (ENNReal.ofReal (↑(ContinuousMap.comp ContinuousMap.coeNNRealReal δ) x)) ⊆ U i
⊢ ∃ δ, (∀ (x : X), 0 < ↑δ x) ∧ ∀ (i : ι) (x : X), x ∈ K i → closedBall x ↑(↑δ x) ⊆ U i
[PROOFSTEP]
refine' ⟨δ, hδ₀, fun i x hi => _⟩
[GOAL]
case intro.intro.intro
ι : Type u_1
X : Type u_2
inst✝ : EMetricSpace X
K U : ι → Set X
hK : ∀ (i : ι), IsClosed (K i)
hU : ∀ (i : ι), IsOpen (U i)
hKU : ∀ (i : ι), K i ⊆ U i
hfin : LocallyFinite K
δ : C(X, ℝ≥0)
hδ₀ : ∀ (x : X), 0 < ↑(ContinuousMap.comp ContinuousMap.coeNNRealReal δ) x
hδ :
  ∀ (i : ι) (x : X),
    x ∈ K i → closedBall x (ENNReal.ofReal (↑(ContinuousMap.comp ContinuousMap.coeNNRealReal δ) x)) ⊆ U i
i : ι
x : X
hi : x ∈ K i
⊢ closedBall x ↑(↑δ x) ⊆ U i
[PROOFSTEP]
simpa only [← ENNReal.ofReal_coe_nnreal] using hδ i x hi
[GOAL]
ι : Type u_1
X : Type u_2
inst✝ : MetricSpace X
K U : ι → Set X
hK : ∀ (i : ι), IsClosed (K i)
hU : ∀ (i : ι), IsOpen (U i)
hKU : ∀ (i : ι), K i ⊆ U i
hfin : LocallyFinite K
⊢ ∃ δ, (∀ (x : X), 0 < ↑δ x) ∧ ∀ (i : ι) (x : X), x ∈ K i → closedBall x ↑(↑δ x) ⊆ U i
[PROOFSTEP]
rcases EMetric.exists_continuous_nNReal_forall_closedBall_subset hK hU hKU hfin with ⟨δ, hδ0, hδ⟩
[GOAL]
case intro.intro
ι : Type u_1
X : Type u_2
inst✝ : MetricSpace X
K U : ι → Set X
hK : ∀ (i : ι), IsClosed (K i)
hU : ∀ (i : ι), IsOpen (U i)
hKU : ∀ (i : ι), K i ⊆ U i
hfin : LocallyFinite K
δ : C(X, ℝ≥0)
hδ0 : ∀ (x : X), 0 < ↑δ x
hδ : ∀ (i : ι) (x : X), x ∈ K i → EMetric.closedBall x ↑(↑δ x) ⊆ U i
⊢ ∃ δ, (∀ (x : X), 0 < ↑δ x) ∧ ∀ (i : ι) (x : X), x ∈ K i → closedBall x ↑(↑δ x) ⊆ U i
[PROOFSTEP]
refine' ⟨δ, hδ0, fun i x hx => _⟩
[GOAL]
case intro.intro
ι : Type u_1
X : Type u_2
inst✝ : MetricSpace X
K U : ι → Set X
hK : ∀ (i : ι), IsClosed (K i)
hU : ∀ (i : ι), IsOpen (U i)
hKU : ∀ (i : ι), K i ⊆ U i
hfin : LocallyFinite K
δ : C(X, ℝ≥0)
hδ0 : ∀ (x : X), 0 < ↑δ x
hδ : ∀ (i : ι) (x : X), x ∈ K i → EMetric.closedBall x ↑(↑δ x) ⊆ U i
i : ι
x : X
hx : x ∈ K i
⊢ closedBall x ↑(↑δ x) ⊆ U i
[PROOFSTEP]
rw [← emetric_closedBall_nnreal]
[GOAL]
case intro.intro
ι : Type u_1
X : Type u_2
inst✝ : MetricSpace X
K U : ι → Set X
hK : ∀ (i : ι), IsClosed (K i)
hU : ∀ (i : ι), IsOpen (U i)
hKU : ∀ (i : ι), K i ⊆ U i
hfin : LocallyFinite K
δ : C(X, ℝ≥0)
hδ0 : ∀ (x : X), 0 < ↑δ x
hδ : ∀ (i : ι) (x : X), x ∈ K i → EMetric.closedBall x ↑(↑δ x) ⊆ U i
i : ι
x : X
hx : x ∈ K i
⊢ EMetric.closedBall x ↑(↑δ x) ⊆ U i
[PROOFSTEP]
exact hδ i x hx


[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝³ : Bornology α
inst✝² : Bornology β
inst✝¹ : Bornology γ
inst✝ : Bornology δ
f g : LocallyBoundedMap α β
h : (fun f => f.toFun) f = (fun f => f.toFun) g
⊢ f = g
[PROOFSTEP]
cases f
[GOAL]
case mk
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝³ : Bornology α
inst✝² : Bornology β
inst✝¹ : Bornology γ
inst✝ : Bornology δ
g : LocallyBoundedMap α β
toFun✝ : α → β
comap_cobounded_le'✝ : comap toFun✝ (cobounded β) ≤ cobounded α
h : (fun f => f.toFun) { toFun := toFun✝, comap_cobounded_le' := comap_cobounded_le'✝ } = (fun f => f.toFun) g
⊢ { toFun := toFun✝, comap_cobounded_le' := comap_cobounded_le'✝ } = g
[PROOFSTEP]
cases g
[GOAL]
case mk.mk
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝³ : Bornology α
inst✝² : Bornology β
inst✝¹ : Bornology γ
inst✝ : Bornology δ
toFun✝¹ : α → β
comap_cobounded_le'✝¹ : comap toFun✝¹ (cobounded β) ≤ cobounded α
toFun✝ : α → β
comap_cobounded_le'✝ : comap toFun✝ (cobounded β) ≤ cobounded α
h :
  (fun f => f.toFun) { toFun := toFun✝¹, comap_cobounded_le' := comap_cobounded_le'✝¹ } =
    (fun f => f.toFun) { toFun := toFun✝, comap_cobounded_le' := comap_cobounded_le'✝ }
⊢ { toFun := toFun✝¹, comap_cobounded_le' := comap_cobounded_le'✝¹ } =
    { toFun := toFun✝, comap_cobounded_le' := comap_cobounded_le'✝ }
[PROOFSTEP]
congr
[GOAL]
F : Type u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝³ : Bornology α
inst✝² : Bornology β
inst✝¹ : Bornology γ
inst✝ : Bornology δ
g : LocallyBoundedMap β γ
f₁ f₂ : LocallyBoundedMap α β
hg : Injective ↑g
h : comp g f₁ = comp g f₂
a : α
⊢ ↑g (↑f₁ a) = ↑g (↑f₂ a)
[PROOFSTEP]
rw [← comp_apply, h, comp_apply]


[GOAL]
R : Type uR
A : Type uA
B : Type uB
M : Type uM
N : Type uN
P : Type uP
Q : Type uQ
inst✝²² : CommSemiring R
inst✝²¹ : Semiring A
inst✝²⁰ : Semiring B
inst✝¹⁹ : Algebra R A
inst✝¹⁸ : Algebra R B
inst✝¹⁷ : AddCommMonoid M
inst✝¹⁶ : Module R M
inst✝¹⁵ : Module A M
inst✝¹⁴ : Module B M
inst✝¹³ : IsScalarTower R A M
inst✝¹² : IsScalarTower R B M
inst✝¹¹ : SMulCommClass A B M
inst✝¹⁰ : AddCommMonoid N
inst✝⁹ : Module R N
inst✝⁸ : AddCommMonoid P
inst✝⁷ : Module R P
inst✝⁶ : Module A P
inst✝⁵ : Module B P
inst✝⁴ : IsScalarTower R A P
inst✝³ : IsScalarTower R B P
inst✝² : SMulCommClass A B P
inst✝¹ : AddCommMonoid Q
inst✝ : Module R Q
f : M →ₗ[A] N →ₗ[R] P
src✝ : M ⊗[R] N →ₗ[R] P := TensorProduct.lift (↑R f)
c : A
x : M
y : N
⊢ ↑(comp (TensorProduct.lift (↑R f)) (↑(Algebra.lsmul R R (M ⊗[R] N)) c)) (x ⊗ₜ[R] y) =
    ↑(comp (↑(Algebra.lsmul R R P) c) (TensorProduct.lift (↑R f))) (x ⊗ₜ[R] y)
[PROOFSTEP]
simp only [comp_apply, Algebra.lsmul_coe, smul_tmul', lift.tmul, coe_restrictScalars, f.map_smul, smul_apply]
[GOAL]
R : Type uR
A : Type uA
B : Type uB
M : Type uM
N : Type uN
P : Type uP
Q : Type uQ
inst✝²² : CommSemiring R
inst✝²¹ : Semiring A
inst✝²⁰ : Semiring B
inst✝¹⁹ : Algebra R A
inst✝¹⁸ : Algebra R B
inst✝¹⁷ : AddCommMonoid M
inst✝¹⁶ : Module R M
inst✝¹⁵ : Module A M
inst✝¹⁴ : Module B M
inst✝¹³ : IsScalarTower R A M
inst✝¹² : IsScalarTower R B M
inst✝¹¹ : SMulCommClass A B M
inst✝¹⁰ : AddCommMonoid N
inst✝⁹ : Module R N
inst✝⁸ : AddCommMonoid P
inst✝⁷ : Module R P
inst✝⁶ : Module A P
inst✝⁵ : Module B P
inst✝⁴ : IsScalarTower R A P
inst✝³ : IsScalarTower R B P
inst✝² : SMulCommClass A B P
inst✝¹ : AddCommMonoid Q
inst✝ : Module R Q
x✝¹ x✝ : M →ₗ[A] N →ₗ[R] P
x : M
y : N
⊢ ↑(lift (x✝¹ + x✝)) (x ⊗ₜ[R] y) = ↑(lift x✝¹ + lift x✝) (x ⊗ₜ[R] y)
[PROOFSTEP]
simp only [lift_tmul, add_apply]
[GOAL]
R : Type uR
A : Type uA
B : Type uB
M : Type uM
N : Type uN
P : Type uP
Q : Type uQ
inst✝²² : CommSemiring R
inst✝²¹ : Semiring A
inst✝²⁰ : Semiring B
inst✝¹⁹ : Algebra R A
inst✝¹⁸ : Algebra R B
inst✝¹⁷ : AddCommMonoid M
inst✝¹⁶ : Module R M
inst✝¹⁵ : Module A M
inst✝¹⁴ : Module B M
inst✝¹³ : IsScalarTower R A M
inst✝¹² : IsScalarTower R B M
inst✝¹¹ : SMulCommClass A B M
inst✝¹⁰ : AddCommMonoid N
inst✝⁹ : Module R N
inst✝⁸ : AddCommMonoid P
inst✝⁷ : Module R P
inst✝⁶ : Module A P
inst✝⁵ : Module B P
inst✝⁴ : IsScalarTower R A P
inst✝³ : IsScalarTower R B P
inst✝² : SMulCommClass A B P
inst✝¹ : AddCommMonoid Q
inst✝ : Module R Q
x✝¹ : B
x✝ : M →ₗ[A] N →ₗ[R] P
x : M
y : N
⊢ ↑(AddHom.toFun { toFun := lift, map_add' := (_ : ∀ (x x_1 : M →ₗ[A] N →ₗ[R] P), lift (x + x_1) = lift x + lift x_1) }
          (x✝¹ • x✝))
      (x ⊗ₜ[R] y) =
    ↑(↑(RingHom.id B) x✝¹ •
          AddHom.toFun
            { toFun := lift, map_add' := (_ : ∀ (x x_1 : M →ₗ[A] N →ₗ[R] P), lift (x + x_1) = lift x + lift x_1) } x✝)
      (x ⊗ₜ[R] y)
[PROOFSTEP]
simp only [lift_tmul, smul_apply, RingHom.id_apply]
  -- porting note: new `B` argument
[GOAL]
R : Type uR
A : Type uA
B : Type uB
M : Type uM
N : Type uN
P : Type uP
Q : Type uQ
inst✝²² : CommSemiring R
inst✝²¹ : Semiring A
inst✝²⁰ : Semiring B
inst✝¹⁹ : Algebra R A
inst✝¹⁸ : Algebra R B
inst✝¹⁷ : AddCommMonoid M
inst✝¹⁶ : Module R M
inst✝¹⁵ : Module A M
inst✝¹⁴ : Module B M
inst✝¹³ : IsScalarTower R A M
inst✝¹² : IsScalarTower R B M
inst✝¹¹ : SMulCommClass A B M
inst✝¹⁰ : AddCommMonoid N
inst✝⁹ : Module R N
inst✝⁸ : AddCommMonoid P
inst✝⁷ : Module R P
inst✝⁶ : Module A P
inst✝⁵ : Module B P
inst✝⁴ : IsScalarTower R A P
inst✝³ : IsScalarTower R B P
inst✝² : SMulCommClass A B P
inst✝¹ : AddCommMonoid Q
inst✝ : Module R Q
f₁ f₂ : M →ₗ[A] P
g : N →ₗ[R] Q
⊢ map (f₁ + f₂) g = map f₁ g + map f₂ g
[PROOFSTEP]
ext
[GOAL]
case a.h.h
R : Type uR
A : Type uA
B : Type uB
M : Type uM
N : Type uN
P : Type uP
Q : Type uQ
inst✝²² : CommSemiring R
inst✝²¹ : Semiring A
inst✝²⁰ : Semiring B
inst✝¹⁹ : Algebra R A
inst✝¹⁸ : Algebra R B
inst✝¹⁷ : AddCommMonoid M
inst✝¹⁶ : Module R M
inst✝¹⁵ : Module A M
inst✝¹⁴ : Module B M
inst✝¹³ : IsScalarTower R A M
inst✝¹² : IsScalarTower R B M
inst✝¹¹ : SMulCommClass A B M
inst✝¹⁰ : AddCommMonoid N
inst✝⁹ : Module R N
inst✝⁸ : AddCommMonoid P
inst✝⁷ : Module R P
inst✝⁶ : Module A P
inst✝⁵ : Module B P
inst✝⁴ : IsScalarTower R A P
inst✝³ : IsScalarTower R B P
inst✝² : SMulCommClass A B P
inst✝¹ : AddCommMonoid Q
inst✝ : Module R Q
f₁ f₂ : M →ₗ[A] P
g : N →ₗ[R] Q
x✝¹ : M
x✝ : N
⊢ ↑(↑(curry (map (f₁ + f₂) g)) x✝¹) x✝ = ↑(↑(curry (map f₁ g + map f₂ g)) x✝¹) x✝
[PROOFSTEP]
simp_rw [curry_apply, TensorProduct.curry_apply, restrictScalars_apply, add_apply, map_tmul, add_apply, add_tmul]
[GOAL]
R : Type uR
A : Type uA
B : Type uB
M : Type uM
N : Type uN
P : Type uP
Q : Type uQ
inst✝²² : CommSemiring R
inst✝²¹ : Semiring A
inst✝²⁰ : Semiring B
inst✝¹⁹ : Algebra R A
inst✝¹⁸ : Algebra R B
inst✝¹⁷ : AddCommMonoid M
inst✝¹⁶ : Module R M
inst✝¹⁵ : Module A M
inst✝¹⁴ : Module B M
inst✝¹³ : IsScalarTower R A M
inst✝¹² : IsScalarTower R B M
inst✝¹¹ : SMulCommClass A B M
inst✝¹⁰ : AddCommMonoid N
inst✝⁹ : Module R N
inst✝⁸ : AddCommMonoid P
inst✝⁷ : Module R P
inst✝⁶ : Module A P
inst✝⁵ : Module B P
inst✝⁴ : IsScalarTower R A P
inst✝³ : IsScalarTower R B P
inst✝² : SMulCommClass A B P
inst✝¹ : AddCommMonoid Q
inst✝ : Module R Q
f : M →ₗ[A] P
g₁ g₂ : N →ₗ[R] Q
⊢ map f (g₁ + g₂) = map f g₁ + map f g₂
[PROOFSTEP]
ext
[GOAL]
case a.h.h
R : Type uR
A : Type uA
B : Type uB
M : Type uM
N : Type uN
P : Type uP
Q : Type uQ
inst✝²² : CommSemiring R
inst✝²¹ : Semiring A
inst✝²⁰ : Semiring B
inst✝¹⁹ : Algebra R A
inst✝¹⁸ : Algebra R B
inst✝¹⁷ : AddCommMonoid M
inst✝¹⁶ : Module R M
inst✝¹⁵ : Module A M
inst✝¹⁴ : Module B M
inst✝¹³ : IsScalarTower R A M
inst✝¹² : IsScalarTower R B M
inst✝¹¹ : SMulCommClass A B M
inst✝¹⁰ : AddCommMonoid N
inst✝⁹ : Module R N
inst✝⁸ : AddCommMonoid P
inst✝⁷ : Module R P
inst✝⁶ : Module A P
inst✝⁵ : Module B P
inst✝⁴ : IsScalarTower R A P
inst✝³ : IsScalarTower R B P
inst✝² : SMulCommClass A B P
inst✝¹ : AddCommMonoid Q
inst✝ : Module R Q
f : M →ₗ[A] P
g₁ g₂ : N →ₗ[R] Q
x✝¹ : M
x✝ : N
⊢ ↑(↑(curry (map f (g₁ + g₂))) x✝¹) x✝ = ↑(↑(curry (map f g₁ + map f g₂)) x✝¹) x✝
[PROOFSTEP]
simp_rw [curry_apply, TensorProduct.curry_apply, restrictScalars_apply, add_apply, map_tmul, add_apply, tmul_add]
[GOAL]
R : Type uR
A : Type uA
B : Type uB
M : Type uM
N : Type uN
P : Type uP
Q : Type uQ
inst✝²² : CommSemiring R
inst✝²¹ : Semiring A
inst✝²⁰ : Semiring B
inst✝¹⁹ : Algebra R A
inst✝¹⁸ : Algebra R B
inst✝¹⁷ : AddCommMonoid M
inst✝¹⁶ : Module R M
inst✝¹⁵ : Module A M
inst✝¹⁴ : Module B M
inst✝¹³ : IsScalarTower R A M
inst✝¹² : IsScalarTower R B M
inst✝¹¹ : SMulCommClass A B M
inst✝¹⁰ : AddCommMonoid N
inst✝⁹ : Module R N
inst✝⁸ : AddCommMonoid P
inst✝⁷ : Module R P
inst✝⁶ : Module A P
inst✝⁵ : Module B P
inst✝⁴ : IsScalarTower R A P
inst✝³ : IsScalarTower R B P
inst✝² : SMulCommClass A B P
inst✝¹ : AddCommMonoid Q
inst✝ : Module R Q
r : R
f : M →ₗ[A] P
g : N →ₗ[R] Q
⊢ map f (r • g) = r • map f g
[PROOFSTEP]
ext
[GOAL]
case a.h.h
R : Type uR
A : Type uA
B : Type uB
M : Type uM
N : Type uN
P : Type uP
Q : Type uQ
inst✝²² : CommSemiring R
inst✝²¹ : Semiring A
inst✝²⁰ : Semiring B
inst✝¹⁹ : Algebra R A
inst✝¹⁸ : Algebra R B
inst✝¹⁷ : AddCommMonoid M
inst✝¹⁶ : Module R M
inst✝¹⁵ : Module A M
inst✝¹⁴ : Module B M
inst✝¹³ : IsScalarTower R A M
inst✝¹² : IsScalarTower R B M
inst✝¹¹ : SMulCommClass A B M
inst✝¹⁰ : AddCommMonoid N
inst✝⁹ : Module R N
inst✝⁸ : AddCommMonoid P
inst✝⁷ : Module R P
inst✝⁶ : Module A P
inst✝⁵ : Module B P
inst✝⁴ : IsScalarTower R A P
inst✝³ : IsScalarTower R B P
inst✝² : SMulCommClass A B P
inst✝¹ : AddCommMonoid Q
inst✝ : Module R Q
r : R
f : M →ₗ[A] P
g : N →ₗ[R] Q
x✝¹ : M
x✝ : N
⊢ ↑(↑(curry (map f (r • g))) x✝¹) x✝ = ↑(↑(curry (r • map f g)) x✝¹) x✝
[PROOFSTEP]
simp_rw [curry_apply, TensorProduct.curry_apply, restrictScalars_apply, smul_apply, map_tmul, smul_apply, tmul_smul]
[GOAL]
R : Type uR
A : Type uA
B : Type uB
M : Type uM
N : Type uN
P : Type uP
Q : Type uQ
inst✝²² : CommSemiring R
inst✝²¹ : Semiring A
inst✝²⁰ : Semiring B
inst✝¹⁹ : Algebra R A
inst✝¹⁸ : Algebra R B
inst✝¹⁷ : AddCommMonoid M
inst✝¹⁶ : Module R M
inst✝¹⁵ : Module A M
inst✝¹⁴ : Module B M
inst✝¹³ : IsScalarTower R A M
inst✝¹² : IsScalarTower R B M
inst✝¹¹ : SMulCommClass A B M
inst✝¹⁰ : AddCommMonoid N
inst✝⁹ : Module R N
inst✝⁸ : AddCommMonoid P
inst✝⁷ : Module R P
inst✝⁶ : Module A P
inst✝⁵ : Module B P
inst✝⁴ : IsScalarTower R A P
inst✝³ : IsScalarTower R B P
inst✝² : SMulCommClass A B P
inst✝¹ : AddCommMonoid Q
inst✝ : Module R Q
b : B
f : M →ₗ[A] P
g : N →ₗ[R] Q
⊢ map (b • f) g = b • map f g
[PROOFSTEP]
ext
[GOAL]
case a.h.h
R : Type uR
A : Type uA
B : Type uB
M : Type uM
N : Type uN
P : Type uP
Q : Type uQ
inst✝²² : CommSemiring R
inst✝²¹ : Semiring A
inst✝²⁰ : Semiring B
inst✝¹⁹ : Algebra R A
inst✝¹⁸ : Algebra R B
inst✝¹⁷ : AddCommMonoid M
inst✝¹⁶ : Module R M
inst✝¹⁵ : Module A M
inst✝¹⁴ : Module B M
inst✝¹³ : IsScalarTower R A M
inst✝¹² : IsScalarTower R B M
inst✝¹¹ : SMulCommClass A B M
inst✝¹⁰ : AddCommMonoid N
inst✝⁹ : Module R N
inst✝⁸ : AddCommMonoid P
inst✝⁷ : Module R P
inst✝⁶ : Module A P
inst✝⁵ : Module B P
inst✝⁴ : IsScalarTower R A P
inst✝³ : IsScalarTower R B P
inst✝² : SMulCommClass A B P
inst✝¹ : AddCommMonoid Q
inst✝ : Module R Q
b : B
f : M →ₗ[A] P
g : N →ₗ[R] Q
x✝¹ : M
x✝ : N
⊢ ↑(↑(curry (map (b • f) g)) x✝¹) x✝ = ↑(↑(curry (b • map f g)) x✝¹) x✝
[PROOFSTEP]
simp_rw [curry_apply, TensorProduct.curry_apply, restrictScalars_apply, smul_apply, map_tmul, smul_apply, smul_tmul']
[GOAL]
R : Type uR
A : Type uA
B : Type uB
M : Type uM
N : Type uN
P : Type uP
Q : Type uQ
inst✝²⁴ : CommSemiring R
inst✝²³ : CommSemiring A
inst✝²² : Semiring B
inst✝²¹ : Algebra R A
inst✝²⁰ : Algebra R B
inst✝¹⁹ : AddCommMonoid M
inst✝¹⁸ : Module R M
inst✝¹⁷ : Module A M
inst✝¹⁶ : Module B M
inst✝¹⁵ : IsScalarTower R A M
inst✝¹⁴ : IsScalarTower R B M
inst✝¹³ : SMulCommClass A B M
inst✝¹² : AddCommMonoid N
inst✝¹¹ : Module R N
inst✝¹⁰ : AddCommMonoid P
inst✝⁹ : Module R P
inst✝⁸ : Module A P
inst✝⁷ : Module B P
inst✝⁶ : IsScalarTower R A P
inst✝⁵ : IsScalarTower R B P
inst✝⁴ : SMulCommClass A B P
inst✝³ : AddCommMonoid Q
inst✝² : Module R Q
inst✝¹ : Algebra A B
inst✝ : IsScalarTower A B M
⊢ comp (lift (lift (comp (lcurry R A B P Q (M ⊗[A] P ⊗[R] Q)) (mk A B M (P ⊗[R] Q)))))
      (lift (comp (uncurry R A B P Q ((M ⊗[A] P) ⊗[R] Q)) (curry (mk R B (M ⊗[A] P) Q)))) =
    LinearMap.id
[PROOFSTEP]
ext
[GOAL]
case a.h.a.h.h
R : Type uR
A : Type uA
B : Type uB
M : Type uM
N : Type uN
P : Type uP
Q : Type uQ
inst✝²⁴ : CommSemiring R
inst✝²³ : CommSemiring A
inst✝²² : Semiring B
inst✝²¹ : Algebra R A
inst✝²⁰ : Algebra R B
inst✝¹⁹ : AddCommMonoid M
inst✝¹⁸ : Module R M
inst✝¹⁷ : Module A M
inst✝¹⁶ : Module B M
inst✝¹⁵ : IsScalarTower R A M
inst✝¹⁴ : IsScalarTower R B M
inst✝¹³ : SMulCommClass A B M
inst✝¹² : AddCommMonoid N
inst✝¹¹ : Module R N
inst✝¹⁰ : AddCommMonoid P
inst✝⁹ : Module R P
inst✝⁸ : Module A P
inst✝⁷ : Module B P
inst✝⁶ : IsScalarTower R A P
inst✝⁵ : IsScalarTower R B P
inst✝⁴ : SMulCommClass A B P
inst✝³ : AddCommMonoid Q
inst✝² : Module R Q
inst✝¹ : Algebra A B
inst✝ : IsScalarTower A B M
x✝² : M
x✝¹ : P
x✝ : Q
⊢ ↑(↑(curry
              (↑(curry
                    (comp (lift (lift (comp (lcurry R A B P Q (M ⊗[A] P ⊗[R] Q)) (mk A B M (P ⊗[R] Q)))))
                      (lift (comp (uncurry R A B P Q ((M ⊗[A] P) ⊗[R] Q)) (curry (mk R B (M ⊗[A] P) Q))))))
                x✝²))
          x✝¹)
      x✝ =
    ↑(↑(curry (↑(curry LinearMap.id) x✝²)) x✝¹) x✝
[PROOFSTEP]
rfl
[GOAL]
R : Type uR
A : Type uA
B : Type uB
M : Type uM
N : Type uN
P : Type uP
Q : Type uQ
inst✝²⁴ : CommSemiring R
inst✝²³ : CommSemiring A
inst✝²² : Semiring B
inst✝²¹ : Algebra R A
inst✝²⁰ : Algebra R B
inst✝¹⁹ : AddCommMonoid M
inst✝¹⁸ : Module R M
inst✝¹⁷ : Module A M
inst✝¹⁶ : Module B M
inst✝¹⁵ : IsScalarTower R A M
inst✝¹⁴ : IsScalarTower R B M
inst✝¹³ : SMulCommClass A B M
inst✝¹² : AddCommMonoid N
inst✝¹¹ : Module R N
inst✝¹⁰ : AddCommMonoid P
inst✝⁹ : Module R P
inst✝⁸ : Module A P
inst✝⁷ : Module B P
inst✝⁶ : IsScalarTower R A P
inst✝⁵ : IsScalarTower R B P
inst✝⁴ : SMulCommClass A B P
inst✝³ : AddCommMonoid Q
inst✝² : Module R Q
inst✝¹ : Algebra A B
inst✝ : IsScalarTower A B M
⊢ comp (lift (comp (uncurry R A B P Q ((M ⊗[A] P) ⊗[R] Q)) (curry (mk R B (M ⊗[A] P) Q))))
      (lift (lift (comp (lcurry R A B P Q (M ⊗[A] P ⊗[R] Q)) (mk A B M (P ⊗[R] Q))))) =
    LinearMap.id
[PROOFSTEP]
ext
[GOAL]
case a.a.h.h.h
R : Type uR
A : Type uA
B : Type uB
M : Type uM
N : Type uN
P : Type uP
Q : Type uQ
inst✝²⁴ : CommSemiring R
inst✝²³ : CommSemiring A
inst✝²² : Semiring B
inst✝²¹ : Algebra R A
inst✝²⁰ : Algebra R B
inst✝¹⁹ : AddCommMonoid M
inst✝¹⁸ : Module R M
inst✝¹⁷ : Module A M
inst✝¹⁶ : Module B M
inst✝¹⁵ : IsScalarTower R A M
inst✝¹⁴ : IsScalarTower R B M
inst✝¹³ : SMulCommClass A B M
inst✝¹² : AddCommMonoid N
inst✝¹¹ : Module R N
inst✝¹⁰ : AddCommMonoid P
inst✝⁹ : Module R P
inst✝⁸ : Module A P
inst✝⁷ : Module B P
inst✝⁶ : IsScalarTower R A P
inst✝⁵ : IsScalarTower R B P
inst✝⁴ : SMulCommClass A B P
inst✝³ : AddCommMonoid Q
inst✝² : Module R Q
inst✝¹ : Algebra A B
inst✝ : IsScalarTower A B M
x✝² : M
x✝¹ : P
x✝ : Q
⊢ ↑(↑(↑(curry
                  (curry
                    (comp (lift (comp (uncurry R A B P Q ((M ⊗[A] P) ⊗[R] Q)) (curry (mk R B (M ⊗[A] P) Q))))
                      (lift (lift (comp (lcurry R A B P Q (M ⊗[A] P ⊗[R] Q)) (mk A B M (P ⊗[R] Q))))))))
              x✝²)
          x✝¹)
      x✝ =
    ↑(↑(↑(curry (curry LinearMap.id)) x✝²) x✝¹) x✝
[PROOFSTEP]
rfl


[GOAL]
α : Type u_1
𝕜 : Type u_2
𝕝 : Type u_3
R : Type u_4
E : Type u_5
F : Type u_6
M : Type u_7
inst✝⁵ : TopologicalSpace 𝕜
inst✝⁴ : CommSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : Module 𝕜 E
inst✝¹ : AddCommMonoid F
inst✝ : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
l : Filter α
f : α → WeakBilin B
x : WeakBilin B
hB : Function.Injective ↑B
⊢ Tendsto f l (𝓝 x) ↔ ∀ (y : F), Tendsto (fun i => ↑(↑B (f i)) y) l (𝓝 (↑(↑B x) y))
[PROOFSTEP]
rw [← tendsto_pi_nhds, Embedding.tendsto_nhds_iff (embedding hB)]
[GOAL]
α : Type u_1
𝕜 : Type u_2
𝕝 : Type u_3
R : Type u_4
E : Type u_5
F : Type u_6
M : Type u_7
inst✝⁵ : TopologicalSpace 𝕜
inst✝⁴ : CommSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : Module 𝕜 E
inst✝¹ : AddCommMonoid F
inst✝ : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
l : Filter α
f : α → WeakBilin B
x : WeakBilin B
hB : Function.Injective ↑B
⊢ Tendsto ((fun x y => ↑(↑B x) y) ∘ f) l (𝓝 fun y => ↑(↑B x) y) ↔
    Tendsto (fun i y => ↑(↑B (f i)) y) l (𝓝 fun y => ↑(↑B x) y)
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
𝕜 : Type u_2
𝕝 : Type u_3
R : Type u_4
E : Type u_5
F : Type u_6
M : Type u_7
inst✝⁶ : TopologicalSpace 𝕜
inst✝⁵ : CommSemiring 𝕜
inst✝⁴ : AddCommMonoid E
inst✝³ : Module 𝕜 E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
inst✝ : ContinuousAdd 𝕜
⊢ ContinuousAdd (WeakBilin B)
[PROOFSTEP]
refine' ⟨continuous_induced_rng.2 _⟩
[GOAL]
α : Type u_1
𝕜 : Type u_2
𝕝 : Type u_3
R : Type u_4
E : Type u_5
F : Type u_6
M : Type u_7
inst✝⁶ : TopologicalSpace 𝕜
inst✝⁵ : CommSemiring 𝕜
inst✝⁴ : AddCommMonoid E
inst✝³ : Module 𝕜 E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
inst✝ : ContinuousAdd 𝕜
⊢ Continuous ((fun x y => ↑(↑B x) y) ∘ fun p => p.fst + p.snd)
[PROOFSTEP]
refine' cast (congr_arg _ _) (((coeFn_continuous B).comp continuous_fst).add ((coeFn_continuous B).comp continuous_snd))
[GOAL]
α : Type u_1
𝕜 : Type u_2
𝕝 : Type u_3
R : Type u_4
E : Type u_5
F : Type u_6
M : Type u_7
inst✝⁶ : TopologicalSpace 𝕜
inst✝⁵ : CommSemiring 𝕜
inst✝⁴ : AddCommMonoid E
inst✝³ : Module 𝕜 E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
inst✝ : ContinuousAdd 𝕜
⊢ (fun x => ((fun x y => ↑(↑B x) y) ∘ Prod.fst) x + ((fun x y => ↑(↑B x) y) ∘ Prod.snd) x) =
    (fun x y => ↑(↑B x) y) ∘ fun p => p.fst + p.snd
[PROOFSTEP]
ext
[GOAL]
case h.h
α : Type u_1
𝕜 : Type u_2
𝕝 : Type u_3
R : Type u_4
E : Type u_5
F : Type u_6
M : Type u_7
inst✝⁶ : TopologicalSpace 𝕜
inst✝⁵ : CommSemiring 𝕜
inst✝⁴ : AddCommMonoid E
inst✝³ : Module 𝕜 E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
inst✝ : ContinuousAdd 𝕜
x✝¹ : WeakBilin B × WeakBilin B
x✝ : F
⊢ (((fun x y => ↑(↑B x) y) ∘ Prod.fst) x✝¹ + ((fun x y => ↑(↑B x) y) ∘ Prod.snd) x✝¹) x✝ =
    ((fun x y => ↑(↑B x) y) ∘ fun p => p.fst + p.snd) x✝¹ x✝
[PROOFSTEP]
simp only [Function.comp_apply, Pi.add_apply, map_add, LinearMap.add_apply]
[GOAL]
α : Type u_1
𝕜 : Type u_2
𝕝 : Type u_3
R : Type u_4
E : Type u_5
F : Type u_6
M : Type u_7
inst✝⁶ : TopologicalSpace 𝕜
inst✝⁵ : CommSemiring 𝕜
inst✝⁴ : AddCommMonoid E
inst✝³ : Module 𝕜 E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
inst✝ : ContinuousSMul 𝕜 𝕜
⊢ ContinuousSMul 𝕜 (WeakBilin B)
[PROOFSTEP]
refine' ⟨continuous_induced_rng.2 _⟩
[GOAL]
α : Type u_1
𝕜 : Type u_2
𝕝 : Type u_3
R : Type u_4
E : Type u_5
F : Type u_6
M : Type u_7
inst✝⁶ : TopologicalSpace 𝕜
inst✝⁵ : CommSemiring 𝕜
inst✝⁴ : AddCommMonoid E
inst✝³ : Module 𝕜 E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
inst✝ : ContinuousSMul 𝕜 𝕜
⊢ Continuous ((fun x y => ↑(↑B x) y) ∘ fun p => p.fst • p.snd)
[PROOFSTEP]
refine' cast (congr_arg _ _) (continuous_fst.smul ((coeFn_continuous B).comp continuous_snd))
[GOAL]
α : Type u_1
𝕜 : Type u_2
𝕝 : Type u_3
R : Type u_4
E : Type u_5
F : Type u_6
M : Type u_7
inst✝⁶ : TopologicalSpace 𝕜
inst✝⁵ : CommSemiring 𝕜
inst✝⁴ : AddCommMonoid E
inst✝³ : Module 𝕜 E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
inst✝ : ContinuousSMul 𝕜 𝕜
⊢ (fun x => x.fst • ((fun x y => ↑(↑B x) y) ∘ Prod.snd) x) = (fun x y => ↑(↑B x) y) ∘ fun p => p.fst • p.snd
[PROOFSTEP]
ext
[GOAL]
case h.h
α : Type u_1
𝕜 : Type u_2
𝕝 : Type u_3
R : Type u_4
E : Type u_5
F : Type u_6
M : Type u_7
inst✝⁶ : TopologicalSpace 𝕜
inst✝⁵ : CommSemiring 𝕜
inst✝⁴ : AddCommMonoid E
inst✝³ : Module 𝕜 E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
inst✝ : ContinuousSMul 𝕜 𝕜
x✝¹ : 𝕜 × WeakBilin B
x✝ : F
⊢ (x✝¹.fst • ((fun x y => ↑(↑B x) y) ∘ Prod.snd) x✝¹) x✝ = ((fun x y => ↑(↑B x) y) ∘ fun p => p.fst • p.snd) x✝¹ x✝
[PROOFSTEP]
simp only [Function.comp_apply, Pi.smul_apply, LinearMap.map_smulₛₗ, RingHom.id_apply, LinearMap.smul_apply]
[GOAL]
α : Type u_1
𝕜 : Type u_2
𝕝 : Type u_3
R : Type u_4
E : Type u_5
F : Type u_6
M : Type u_7
inst✝⁶ : TopologicalSpace 𝕜
inst✝⁵ : CommRing 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
inst✝ : ContinuousAdd 𝕜
⊢ ContinuousAdd (WeakBilin B)
[PROOFSTEP]
infer_instance
[GOAL]
α : Type u_1
𝕜 : Type u_2
𝕝 : Type u_3
R : Type u_4
E : Type u_5
F : Type u_6
M : Type u_7
inst✝⁶ : TopologicalSpace 𝕜
inst✝⁵ : CommRing 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
inst✝ : ContinuousAdd 𝕜
⊢ Continuous fun a => -a
[PROOFSTEP]
refine' continuous_induced_rng.2 (continuous_pi_iff.mpr fun y => _)
[GOAL]
α : Type u_1
𝕜 : Type u_2
𝕝 : Type u_3
R : Type u_4
E : Type u_5
F : Type u_6
M : Type u_7
inst✝⁶ : TopologicalSpace 𝕜
inst✝⁵ : CommRing 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
inst✝ : ContinuousAdd 𝕜
y : F
⊢ Continuous fun a => ((fun x y => ↑(↑B x) y) ∘ fun a => -a) a y
[PROOFSTEP]
refine' cast (congr_arg _ _) (eval_continuous B (-y))
[GOAL]
α : Type u_1
𝕜 : Type u_2
𝕝 : Type u_3
R : Type u_4
E : Type u_5
F : Type u_6
M : Type u_7
inst✝⁶ : TopologicalSpace 𝕜
inst✝⁵ : CommRing 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
inst✝ : ContinuousAdd 𝕜
y : F
⊢ (fun x => ↑(↑B x) (-y)) = fun a => ((fun x y => ↑(↑B x) y) ∘ fun a => -a) a y
[PROOFSTEP]
ext x
[GOAL]
case h
α : Type u_1
𝕜 : Type u_2
𝕝 : Type u_3
R : Type u_4
E : Type u_5
F : Type u_6
M : Type u_7
inst✝⁶ : TopologicalSpace 𝕜
inst✝⁵ : CommRing 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
inst✝ : ContinuousAdd 𝕜
y : F
x : WeakBilin B
⊢ ↑(↑B x) (-y) = ((fun x y => ↑(↑B x) y) ∘ fun a => -a) x y
[PROOFSTEP]
simp only [map_neg, Function.comp_apply, LinearMap.neg_apply]
  -- Porting note: mathlib3 proof was done here
[GOAL]
case h
α : Type u_1
𝕜 : Type u_2
𝕝 : Type u_3
R : Type u_4
E : Type u_5
F : Type u_6
M : Type u_7
inst✝⁶ : TopologicalSpace 𝕜
inst✝⁵ : CommRing 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
inst✝ : ContinuousAdd 𝕜
y : F
x : WeakBilin B
⊢ -↑(↑B x) y = ↑(↑B (-x)) y
[PROOFSTEP]
rw [← (B x).neg_apply]
[GOAL]
case h
α : Type u_1
𝕜 : Type u_2
𝕝 : Type u_3
R : Type u_4
E : Type u_5
F : Type u_6
M : Type u_7
inst✝⁶ : TopologicalSpace 𝕜
inst✝⁵ : CommRing 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
inst✝ : ContinuousAdd 𝕜
y : F
x : WeakBilin B
⊢ ↑(-↑B x) y = ↑(↑B (-x)) y
[PROOFSTEP]
congr
[GOAL]
case h.e_a
α : Type u_1
𝕜 : Type u_2
𝕝 : Type u_3
R : Type u_4
E : Type u_5
F : Type u_6
M : Type u_7
inst✝⁶ : TopologicalSpace 𝕜
inst✝⁵ : CommRing 𝕜
inst✝⁴ : AddCommGroup E
inst✝³ : Module 𝕜 E
inst✝² : AddCommGroup F
inst✝¹ : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
inst✝ : ContinuousAdd 𝕜
y : F
x : WeakBilin B
⊢ -↑B x = ↑B (-x)
[PROOFSTEP]
exact (map_neg B x).symm