internlm/Lean-Github huggingface dataset:
Theorem: titi
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
𝕜 : Type u_1
ι : Type u_2
α : Type u_3
s K : Set α
inst✝ : NormedField 𝕜
F G : ι → α → 𝕜
f g : α → 𝕜
x✝ y : 𝕜
η✝ η'✝ : ℝ
p✝ : Filter ι
mf mg : ℝ
p q : Filter 𝕜
hp : p ⊓ 𝓝 0 = ⊥
hq : q ⊓ 𝓝 0 = ⊥
U : Set 𝕜
hU : U ∈ p
V : Set 𝕜
hV✝ : V ∈ 𝓝 0
hUV : U ∩ V = ∅
U' : Set 𝕜
hU' : U' ∈ q
V' : Set 𝕜
hV'✝ : V' ∈ 𝓝 0
hUV' : U' ∩ V' = ∅
η : ℝ
hη : η > 0
hV : ball 0 η ⊆ V
η' : ℝ
hη' : η' > 0
hV' : ball 0 η' ⊆ V'
hηη' : 0 < η * η'
u : Set (𝕜 × 𝕜)
hu✝ : u ∈ 𝓤 𝕜
ε : ℝ
hε : ε > 0
hu : ∀ {a b : 𝕜}, dist a b < ε → (a, b) ∈ u
x : 𝕜 × 𝕜
hx1 : x ∈ {p | dist p.1 p.2 < ε * (η * η')}
hx2 : x ∈ U ×ˢ U'
⊢ (fun x => (x.1⁻¹, x.2⁻¹)) x ∈ u
Tactic:
have hx'1 : x.1 ∉ ball (0 : 𝕜) η :=
  λ h => (Set.nonempty_of_mem (mem_inter hx2.1 (hV h))).ne_empty hUV
Proof state after:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
𝕜 : Type u_1
ι : Type u_2
α : Type u_3
s K : Set α
inst✝ : NormedField 𝕜
F G : ι → α → 𝕜
f g : α → 𝕜
x✝ y : 𝕜
η✝ η'✝ : ℝ
p✝ : Filter ι
mf mg : ℝ
p q : Filter 𝕜
hp : p ⊓ 𝓝 0 = ⊥
hq : q ⊓ 𝓝 0 = ⊥
U : Set 𝕜
hU : U ∈ p
V : Set 𝕜
hV✝ : V ∈ 𝓝 0
hUV : U ∩ V = ∅
U' : Set 𝕜
hU' : U' ∈ q
V' : Set 𝕜
hV'✝ : V' ∈ 𝓝 0
hUV' : U' ∩ V' = ∅
η : ℝ
hη : η > 0
hV : ball 0 η ⊆ V
η' : ℝ
hη' : η' > 0
hV' : ball 0 η' ⊆ V'
hηη' : 0 < η * η'
u : Set (𝕜 × 𝕜)
hu✝ : u ∈ 𝓤 𝕜
ε : ℝ
hε : ε > 0
hu : ∀ {a b : 𝕜}, dist a b < ε → (a, b) ∈ u
x : 𝕜 × 𝕜
hx1 : x ∈ {p | dist p.1 p.2 < ε * (η * η')}
hx2 : x ∈ U ×ˢ U'
hx'1 : x.1 ∉ ball 0 η
⊢ (fun x => (x.1⁻¹, x.2⁻¹)) x ∈ u
Theorem: titi
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
𝕜 : Type u_1
ι : Type u_2
α : Type u_3
s K : Set α
inst✝ : NormedField 𝕜
F G : ι → α → 𝕜
f g : α → 𝕜
x✝ y : 𝕜
η✝ η'✝ : ℝ
p✝ : Filter ι
mf mg : ℝ
p q : Filter 𝕜
hp : p ⊓ 𝓝 0 = ⊥
hq : q ⊓ 𝓝 0 = ⊥
U : Set 𝕜
hU : U ∈ p
V : Set 𝕜
hV✝ : V ∈ 𝓝 0
hUV : U ∩ V = ∅
U' : Set 𝕜
hU' : U' ∈ q
V' : Set 𝕜
hV'✝ : V' ∈ 𝓝 0
hUV' : U' ∩ V' = ∅
η : ℝ
hη : η > 0
hV : ball 0 η ⊆ V
η' : ℝ
hη' : η' > 0
hV' : ball 0 η' ⊆ V'
hηη' : 0 < η * η'
u : Set (𝕜 × 𝕜)
hu✝ : u ∈ 𝓤 𝕜
ε : ℝ
hε : ε > 0
hu : ∀ {a b : 𝕜}, dist a b < ε → (a, b) ∈ u
x : 𝕜 × 𝕜
hx1 : x ∈ {p | dist p.1 p.2 < ε * (η * η')}
hx2 : x ∈ U ×ˢ U'
hx'1 : x.1 ∉ ball 0 η
⊢ (fun x => (x.1⁻¹, x.2⁻¹)) x ∈ u
Tactic:
have hx'2 : x.2 ∉ ball (0 : 𝕜) η' :=
  λ h => (Set.nonempty_of_mem (mem_inter hx2.2 (hV' h))).ne_empty hUV'
Proof state after:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
𝕜 : Type u_1
ι : Type u_2
α : Type u_3
s K : Set α
inst✝ : NormedField 𝕜
F G : ι → α → 𝕜
f g : α → 𝕜
x✝ y : 𝕜
η✝ η'✝ : ℝ
p✝ : Filter ι
mf mg : ℝ
p q : Filter 𝕜
hp : p ⊓ 𝓝 0 = ⊥
hq : q ⊓ 𝓝 0 = ⊥
U : Set 𝕜
hU : U ∈ p
V : Set 𝕜
hV✝ : V ∈ 𝓝 0
hUV : U ∩ V = ∅
U' : Set 𝕜
hU' : U' ∈ q
V' : Set 𝕜
hV'✝ : V' ∈ 𝓝 0
hUV' : U' ∩ V' = ∅
η : ℝ
hη : η > 0
hV : ball 0 η ⊆ V
η' : ℝ
hη' : η' > 0
hV' : ball 0 η' ⊆ V'
hηη' : 0 < η * η'
u : Set (𝕜 × 𝕜)
hu✝ : u ∈ 𝓤 𝕜
ε : ℝ
hε : ε > 0
hu : ∀ {a b : 𝕜}, dist a b < ε → (a, b) ∈ u
x : 𝕜 × 𝕜
hx1 : x ∈ {p | dist p.1 p.2 < ε * (η * η')}
hx2 : x ∈ U ×ˢ U'
hx'1 : x.1 ∉ ball 0 η
hx'2 : x.2 ∉ ball 0 η'
⊢ (fun x => (x.1⁻¹, x.2⁻¹)) x ∈ u
Theorem: titi
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
𝕜 : Type u_1
ι : Type u_2
α : Type u_3
s K : Set α
inst✝ : NormedField 𝕜
F G : ι → α → 𝕜
f g : α → 𝕜
x✝ y : 𝕜
η✝ η'✝ : ℝ
p✝ : Filter ι
mf mg : ℝ
p q : Filter 𝕜
hp : p ⊓ 𝓝 0 = ⊥
hq : q ⊓ 𝓝 0 = ⊥
U : Set 𝕜
hU : U ∈ p
V : Set 𝕜
hV✝ : V ∈ 𝓝 0
hUV : U ∩ V = ∅
U' : Set 𝕜
hU' : U' ∈ q
V' : Set 𝕜
hV'✝ : V' ∈ 𝓝 0
hUV' : U' ∩ V' = ∅
η : ℝ
hη : η > 0
hV : ball 0 η ⊆ V
η' : ℝ
hη' : η' > 0
hV' : ball 0 η' ⊆ V'
hηη' : 0 < η * η'
u : Set (𝕜 × 𝕜)
hu✝ : u ∈ 𝓤 𝕜
ε : ℝ
hε : ε > 0
hu : ∀ {a b : 𝕜}, dist a b < ε → (a, b) ∈ u
x : 𝕜 × 𝕜
hx1 : x ∈ {p | dist p.1 p.2 < ε * (η * η')}
hx2 : x ∈ U ×ˢ U'
hx'1 : x.1 ∉ ball 0 η
hx'2 : x.2 ∉ ball 0 η'
⊢ (fun x => (x.1⁻¹, x.2⁻¹)) x ∈ u
Tactic:
refine hu ((dist_inv_le_dist_div hη hη' hx'1 hx'2).trans_lt ?_)
Proof state after:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
𝕜 : Type u_1
ι : Type u_2
α : Type u_3
s K : Set α
inst✝ : NormedField 𝕜
F G : ι → α → 𝕜
f g : α → 𝕜
x✝ y : 𝕜
η✝ η'✝ : ℝ
p✝ : Filter ι
mf mg : ℝ
p q : Filter 𝕜
hp : p ⊓ 𝓝 0 = ⊥
hq : q ⊓ 𝓝 0 = ⊥
U : Set 𝕜
hU : U ∈ p
V : Set 𝕜
hV✝ : V ∈ 𝓝 0
hUV : U ∩ V = ∅
U' : Set 𝕜
hU' : U' ∈ q
V' : Set 𝕜
hV'✝ : V' ∈ 𝓝 0
hUV' : U' ∩ V' = ∅
η : ℝ
hη : η > 0
hV : ball 0 η ⊆ V
η' : ℝ
hη' : η' > 0
hV' : ball 0 η' ⊆ V'
hηη' : 0 < η * η'
u : Set (𝕜 × 𝕜)
hu✝ : u ∈ 𝓤 𝕜
ε : ℝ
hε : ε > 0
hu : ∀ {a b : 𝕜}, dist a b < ε → (a, b) ∈ u
x : 𝕜 × 𝕜
hx1 : x ∈ {p | dist p.1 p.2 < ε * (η * η')}
hx2 : x ∈ U ×ˢ U'
hx'1 : x.1 ∉ ball 0 η
hx'2 : x.2 ∉ ball 0 η'
⊢ dist x.1 x.2 / (η * η') < ε
Theorem: titi
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
𝕜 : Type u_1
ι : Type u_2
α : Type u_3
s K : Set α
inst✝ : NormedField 𝕜
F G : ι → α → 𝕜
f g : α → 𝕜
x✝ y : 𝕜
η✝ η'✝ : ℝ
p✝ : Filter ι
mf mg : ℝ
p q : Filter 𝕜
hp : p ⊓ 𝓝 0 = ⊥
hq : q ⊓ 𝓝 0 = ⊥
U : Set 𝕜
hU : U ∈ p
V : Set 𝕜
hV✝ : V ∈ 𝓝 0
hUV : U ∩ V = ∅
U' : Set 𝕜
hU' : U' ∈ q
V' : Set 𝕜
hV'✝ : V' ∈ 𝓝 0
hUV' : U' ∩ V' = ∅
η : ℝ
hη : η > 0
hV : ball 0 η ⊆ V
η' : ℝ
hη' : η' > 0
hV' : ball 0 η' ⊆ V'
hηη' : 0 < η * η'
u : Set (𝕜 × 𝕜)
hu✝ : u ∈ 𝓤 𝕜
ε : ℝ
hε : ε > 0
hu : ∀ {a b : 𝕜}, dist a b < ε → (a, b) ∈ u
x : 𝕜 × 𝕜
hx1 : x ∈ {p | dist p.1 p.2 < ε * (η * η')}
hx2 : x ∈ U ×ˢ U'
hx'1 : x.1 ∉ ball 0 η
hx'2 : x.2 ∉ ball 0 η'
⊢ dist x.1 x.2 / (η * η') < ε
Tactic:
convert (div_lt_div_right hηη').mpr hx1
Proof state after:
case h.e'_4
𝕜 : Type u_1
ι : Type u_2
α : Type u_3
s K : Set α
inst✝ : NormedField 𝕜
F G : ι → α → 𝕜
f g : α → 𝕜
x✝ y : 𝕜
η✝ η'✝ : ℝ
p✝ : Filter ι
mf mg : ℝ
p q : Filter 𝕜
hp : p ⊓ 𝓝 0 = ⊥
hq : q ⊓ 𝓝 0 = ⊥
U : Set 𝕜
hU : U ∈ p
V : Set 𝕜
hV✝ : V ∈ 𝓝 0
hUV : U ∩ V = ∅
U' : Set 𝕜
hU' : U' ∈ q
V' : Set 𝕜
hV'✝ : V' ∈ 𝓝 0
hUV' : U' ∩ V' = ∅
η : ℝ
hη : η > 0
hV : ball 0 η ⊆ V
η' : ℝ
hη' : η' > 0
hV' : ball 0 η' ⊆ V'
hηη' : 0 < η * η'
u : Set (𝕜 × 𝕜)
hu✝ : u ∈ 𝓤 𝕜
ε : ℝ
hε : ε > 0
hu : ∀ {a b : 𝕜}, dist a b < ε → (a, b) ∈ u
x : 𝕜 × 𝕜
hx1 : x ∈ {p | dist p.1 p.2 < ε * (η * η')}
hx2 : x ∈ U ×ˢ U'
hx'1 : x.1 ∉ ball 0 η
hx'2 : x.2 ∉ ball 0 η'
⊢ ε = ε * (η * η') / (η * η')
Theorem: titi
Proof state before:
case h.e'_4
𝕜 : Type u_1
ι : Type u_2
α : Type u_3
s K : Set α
inst✝ : NormedField 𝕜
F G : ι → α → 𝕜
f g : α → 𝕜
x✝ y : 𝕜
η✝ η'✝ : ℝ
p✝ : Filter ι
mf mg : ℝ
p q : Filter 𝕜
hp : p ⊓ 𝓝 0 = ⊥
hq : q ⊓ 𝓝 0 = ⊥
U : Set 𝕜
hU : U ∈ p
V : Set 𝕜
hV✝ : V ∈ 𝓝 0
hUV : U ∩ V = ∅
U' : Set 𝕜
hU' : U' ∈ q
V' : Set 𝕜
hV'✝ : V' ∈ 𝓝 0
hUV' : U' ∩ V' = ∅
η : ℝ
hη : η > 0
hV : ball 0 η ⊆ V
η' : ℝ
hη' : η' > 0
hV' : ball 0 η' ⊆ V'
hηη' : 0 < η * η'
u : Set (𝕜 × 𝕜)
hu✝ : u ∈ 𝓤 𝕜
ε : ℝ
hε : ε > 0
hu : ∀ {a b : 𝕜}, dist a b < ε → (a, b) ∈ u
x : 𝕜 × 𝕜
hx1 : x ∈ {p | dist p.1 p.2 < ε * (η * η')}
hx2 : x ∈ U ×ˢ U'
hx'1 : x.1 ∉ ball 0 η
hx'2 : x.2 ∉ ball 0 η'
⊢ ε = ε * (η * η') / (η * η')
Tactic:
field_simp [hη.lt.ne.symm, hη'.lt.ne.symm]
Proof state after:
no goals
Theorem: uniform_ContinuousOn_inv
Proof state before:
𝕜 : Type u_1
ι : Type u_2
α : Type u_3
s✝ K : Set α
inst✝ : NormedField 𝕜
F G : ι → α → 𝕜
f g : α → 𝕜
x y : 𝕜
η η' : ℝ
p : Filter ι
mf mg : ℝ
s : Set 𝕜
hs : 𝓟 s ⊓ 𝓝 0 = ⊥
⊢ UniformContinuousOn Inv.inv s
Tactic:
simpa only [UniformContinuousOn, Tendsto, ← prod_principal_principal] using titi hs hs
Proof state after:
no goals
Theorem: TendstoUniformlyOn.inv
Proof state before:
𝕜 : Type u_1
ι : Type u_2
α : Type u_3
s K : Set α
inst✝ : NormedField 𝕜
F G : ι → α → 𝕜
f g : α → 𝕜
x y : 𝕜
η η' : ℝ
p : Filter ι
mf mg : ℝ
hF : TendstoUniformlyOn F f p s
hf : 𝓟 (f '' s) ⊓ 𝓝 0 = ⊥
⊢ TendstoUniformlyOn F⁻¹ f⁻¹ p s
Tactic:
have : 𝓝ᵘ (f '' s) ⊓ 𝓝 0 = ⊥ := by
  rw [inf_comm] at hf ⊢
  exact UniformSpace.nhds_inf_uniform_nhds_eq_bot hf
Proof state after:
𝕜 : Type u_1
ι : Type u_2
α : Type u_3
s K : Set α
inst✝ : NormedField 𝕜
F G : ι → α → 𝕜
f g : α → 𝕜
x y : 𝕜
η η' : ℝ
p : Filter ι
mf mg : ℝ
hF : TendstoUniformlyOn F f p s
hf : 𝓟 (f '' s) ⊓ 𝓝 0 = ⊥
this : 𝓝ᵘ (f '' s) ⊓ 𝓝 0 = ⊥
⊢ TendstoUniformlyOn F⁻¹ f⁻¹ p s
Theorem: TendstoUniformlyOn.inv
Proof state before:
𝕜 : Type u_1
ι : Type u_2
α : Type u_3
s K : Set α
inst✝ : NormedField 𝕜
F G : ι → α → 𝕜
f g : α → 𝕜
x y : 𝕜
η η' : ℝ
p : Filter ι
mf mg : ℝ
hF : TendstoUniformlyOn F f p s
hf : 𝓟 (f '' s) ⊓ 𝓝 0 = ⊥
this : 𝓝ᵘ (f '' s) ⊓ 𝓝 0 = ⊥
⊢ TendstoUniformlyOn F⁻¹ f⁻¹ p s
Tactic:
have h1 := lemma1 hF
Proof state after:
𝕜 : Type u_1
ι : Type u_2
α : Type u_3
s K : Set α
inst✝ : NormedField 𝕜
F G : ι → α → 𝕜
f g : α → 𝕜
x y : 𝕜
η η' : ℝ
p : Filter ι
mf mg : ℝ
hF : TendstoUniformlyOn F f p s
hf : 𝓟 (f '' s) ⊓ 𝓝 0 = ⊥
this : 𝓝ᵘ (f '' s) ⊓ 𝓝 0 = ⊥
h1 : Tendsto (fun q => (f q.2, F q.1 q.2)) (p ×ˢ 𝓟 s) (𝓟 (f '' s) ×ˢ 𝓝ᵘ (f '' s))
⊢ TendstoUniformlyOn F⁻¹ f⁻¹ p s
Theorem: TendstoUniformlyOn.inv
Proof state before:
𝕜 : Type u_1
ι : Type u_2
α : Type u_3
s K : Set α
inst✝ : NormedField 𝕜
F G : ι → α → 𝕜
f g : α → 𝕜
x y : 𝕜
η η' : ℝ
p : Filter ι
mf mg : ℝ
hF : TendstoUniformlyOn F f p s
hf : 𝓟 (f '' s) ⊓ 𝓝 0 = ⊥
this : 𝓝ᵘ (f '' s) ⊓ 𝓝 0 = ⊥
h1 : Tendsto (fun q => (f q.2, F q.1 q.2)) (p ×ˢ 𝓟 s) (𝓟 (f '' s) ×ˢ 𝓝ᵘ (f '' s))
⊢ TendstoUniformlyOn F⁻¹ f⁻¹ p s
Tactic:
rw [tendstoUniformlyOn_iff_tendsto] at hF ⊢
Proof state after:
𝕜 : Type u_1
ι : Type u_2
α : Type u_3
s K : Set α
inst✝ : NormedField 𝕜
F G : ι → α → 𝕜
f g : α → 𝕜
x y : 𝕜
η η' : ℝ
p : Filter ι
mf mg : ℝ
hF : Tendsto (fun q => (f q.2, F q.1 q.2)) (p ×ˢ 𝓟 s) (𝓤 𝕜)
hf : 𝓟 (f '' s) ⊓ 𝓝 0 = ⊥
this : 𝓝ᵘ (f '' s) ⊓ 𝓝 0 = ⊥
h1 : Tendsto (fun q => (f q.2, F q.1 q.2)) (p ×ˢ 𝓟 s) (𝓟 (f '' s) ×ˢ 𝓝ᵘ (f '' s))
⊢ Tendsto (fun q => (f⁻¹ q.2, F⁻¹ q.1 q.2)) (p ×ˢ 𝓟 s) (𝓤 𝕜)
Theorem: TendstoUniformlyOn.inv
Proof state before:
𝕜 : Type u_1
ι : Type u_2
α : Type u_3
s K : Set α
inst✝ : NormedField 𝕜
F G : ι → α → 𝕜
f g : α → 𝕜
x y : 𝕜
η η' : ℝ
p : Filter ι
mf mg : ℝ
hF : Tendsto (fun q => (f q.2, F q.1 q.2)) (p ×ˢ 𝓟 s) (𝓤 𝕜)
hf : 𝓟 (f '' s) ⊓ 𝓝 0 = ⊥
this : 𝓝ᵘ (f '' s) ⊓ 𝓝 0 = ⊥
h1 : Tendsto (fun q => (f q.2, F q.1 q.2)) (p ×ˢ 𝓟 s) (𝓟 (f '' s) ×ˢ 𝓝ᵘ (f '' s))
⊢ Tendsto (fun q => (f⁻¹ q.2, F⁻¹ q.1 q.2)) (p ×ˢ 𝓟 s) (𝓤 𝕜)
Tactic:
refine (Filter.map_mono (le_inf hF h1)).trans (titi hf this)
Proof state after:
no goals
Theorem: TendstoUniformlyOn.inv
Proof state before:
𝕜 : Type u_1
ι : Type u_2
α : Type u_3
s K : Set α
inst✝ : NormedField 𝕜
F G : ι → α → 𝕜
f g : α → 𝕜
x y : 𝕜
η η' : ℝ
p : Filter ι
mf mg : ℝ
hF : TendstoUniformlyOn F f p s
hf : 𝓟 (f '' s) ⊓ 𝓝 0 = ⊥
⊢ 𝓝ᵘ (f '' s) ⊓ 𝓝 0 = ⊥
Tactic:
rw [inf_comm] at hf ⊢
Proof state after:
𝕜 : Type u_1
ι : Type u_2
α : Type u_3
s K : Set α
inst✝ : NormedField 𝕜
F G : ι → α → 𝕜
f g : α → 𝕜
x y : 𝕜
η η' : ℝ
p : Filter ι
mf mg : ℝ
hF : TendstoUniformlyOn F f p s
hf : 𝓝 0 ⊓ 𝓟 (f '' s) = ⊥
⊢ 𝓝 0 ⊓ 𝓝ᵘ (f '' s) = ⊥
Theorem: TendstoUniformlyOn.inv
Proof state before:
𝕜 : Type u_1
ι : Type u_2
α : Type u_3
s K : Set α
inst✝ : NormedField 𝕜
F G : ι → α → 𝕜
f g : α → 𝕜
x y : 𝕜
η η' : ℝ
p : Filter ι
mf mg : ℝ
hF : TendstoUniformlyOn F f p s
hf : 𝓝 0 ⊓ 𝓟 (f '' s) = ⊥
⊢ 𝓝 0 ⊓ 𝓝ᵘ (f '' s) = ⊥
Tactic:
exact UniformSpace.nhds_inf_uniform_nhds_eq_bot hf
Proof state after:
no goals
Theorem: lxyab
Proof state before:
𝕜 : Type u_1
ι : Type u_2
α : Type u_3
s K : Set α
inst✝ : NormedField 𝕜
F G : ι → α → 𝕜
f g : α → 𝕜
x✝ y✝ : 𝕜
η η' : ℝ
p : Filter ι
mf mg : ℝ
x y a b : 𝕜
⊢ x * a - y * b = (x - y) * a + y * (a - b)
Tactic:
ring
Proof state after:
no goals
Theorem: TendstoUniformlyOn.mul_of_le
Proof state before:
𝕜 : Type u_1
ι : Type u_2
α : Type u_3
s K : Set α
inst✝ : NormedField 𝕜
F G : ι → α → 𝕜
f g : α → 𝕜
x y : 𝕜
η η' : ℝ
p : Filter ι
mf mg : ℝ
hF : TendstoUniformlyOn F f p s
hG : TendstoUniformlyOn G g p s
hf : ∀ᶠ (i : ι) in p, ∀ x ∈ s, ‖F i x‖ ≤ mf
hg : ∀ᶠ (i : ι) in p, ∀ x ∈ s, ‖G i x‖ ≤ mg
⊢ TendstoUniformlyOn (F * G) (f * g) p s
Tactic:
by_cases h : NeBot p
Proof state after:
case pos
𝕜 : Type u_1
ι : Type u_2
α : Type u_3
s K : Set α
inst✝ : NormedField 𝕜
F G : ι → α → 𝕜
f g : α → 𝕜
x y : 𝕜
η η' : ℝ
p : Filter ι
mf mg : ℝ
hF : TendstoUniformlyOn F f p s
hG : TendstoUniformlyOn G g p s
hf : ∀ᶠ (i : ι) in p, ∀ x ∈ s, ‖F i x‖ ≤ mf
hg : ∀ᶠ (i : ι) in p, ∀ x ∈ s, ‖G i x‖ ≤ mg
h : NeBot p
⊢ TendstoUniformlyOn (F * G) (f * g) p s

case neg
𝕜 : Type u_1
ι : Type u_2
α : Type u_3
s K : Set α
inst✝ : NormedField 𝕜
F G : ι → α → 𝕜
f g : α → 𝕜
x y : 𝕜
η η' : ℝ
p : Filter ι
mf mg : ℝ
hF : TendstoUniformlyOn F f p s
hG : TendstoUniformlyOn G g p s
hf : ∀ᶠ (i : ι) in p, ∀ x ∈ s, ‖F i x‖ ≤ mf
hg : ∀ᶠ (i : ι) in p, ∀ x ∈ s, ‖G i x‖ ≤ mg
h : ¬NeBot p
⊢ TendstoUniformlyOn (F * G) (f * g) p s
Theorem: TendstoUniformlyOn.mul_of_le
Proof state before:
𝕜 : Type u_1
ι : Type u_2
α : Type u_3
s K : Set α
inst✝ : NormedField 𝕜
F G : ι → α → 𝕜
f g : α → 𝕜
x y : 𝕜
η η' : ℝ
p : Filter ι
mf mg : ℝ
hF : TendstoUniformlyOn F f p s
hG : TendstoUniformlyOn G g p s
hf : ∀ᶠ (i : ι) in p, ∀ x ∈ s, ‖F i x‖ ≤ mf
hg : ∀ᶠ (i : ι) in p, ∀ x ∈ s, ‖G i x‖ ≤ mg
h : ¬NeBot p
⊢ TendstoUniformlyOn (F * G) (f * g) p s
Tactic:
case neg => simp at h; simp [h, TendstoUniformlyOn]
Proof state after:
no goals
Theorem: TendstoUniformlyOn.mul_of_le
Proof state before:
𝕜 : Type u_1
ι : Type u_2
α : Type u_3
s K : Set α
inst✝ : NormedField 𝕜
F G : ι → α → 𝕜
f g : α → 𝕜
x y : 𝕜
η η' : ℝ
p : Filter ι
mf mg : ℝ
hF : TendstoUniformlyOn F f p s
hG : TendstoUniformlyOn G g p s
hf : ∀ᶠ (i : ι) in p, ∀ x ∈ s, ‖F i x‖ ≤ mf
hg : ∀ᶠ (i : ι) in p, ∀ x ∈ s, ‖G i x‖ ≤ mg
h : NeBot p
⊢ TendstoUniformlyOn (F * G) (f * g) p s
Tactic:
case pos =>
  set Mf := |mf| + 1
  set Mg := |mg| + 1
  have hMf : 0 < Mf := by positivity
  have hMg : 0 < Mg := by positivity
  replace hf : ∀ᶠ i in p, ∀ x ∈ s, ‖F i x‖ ≤ Mf := by
    filter_upwards [hf] with i hF x hx using (hF x hx).trans ((le_abs_self mf).trans (lt_add_one _).le)
  replace hg : ∀ᶠ i in p, ∀ x ∈ s, ‖G i x‖ ≤ Mg := by
    filter_upwards [hg] with i hG x hx using (hG x hx).trans ((le_abs_self mg).trans (lt_add_one _).le)
  have h1 : ∀ x ∈ s, ‖g x‖ ≤ Mg := by
    intro x hx
    refine le_of_tendsto ((continuous_norm.tendsto (g x)).comp (hG.tendsto_at hx)) ?_
    filter_upwards [hg] with i hg using hg x hx
  simp_rw [Metric.tendstoUniformlyOn_iff, dist_eq_norm] at hF hG ⊢
  intro ε hε
  filter_upwards [hf, hF (ε / (2 * Mg)) (by positivity), hG (ε / (2 * Mf)) (by positivity)] with i hf hF hG x hx
  have h2 : ‖(f x - F i x) * g x‖ < ε / 2 := by
    rw [norm_mul]
    by_cases h : g x = 0
    case pos => simp [h, half_pos hε]
    case neg =>
      convert mul_lt_mul (hF x hx) (h1 x hx) (norm_pos_iff.mpr h) (by positivity) using 1
      simp only [div_mul, mul_div_cancel, hMg.ne.symm, Ne.def, not_false_iff]
  have h3 : ‖F i x * (g x - G i x)‖ < ε / 2 := by
    rw [norm_mul]
    by_cases h : F i x = 0
    case pos => simp [h, half_pos hε]
    case neg =>
      convert mul_lt_mul' (hf x hx) (hG x hx) (norm_nonneg _) hMf using 1
      field_simp [hMf.ne.symm]; ring
  simp_rw [Pi.mul_apply, lxyab]
  exact (norm_add_le _ _).trans_lt (add_halves' ε ▸ add_lt_add h2 h3)
Proof state after:
no goals
Theorem: TendstoUniformlyOn.mul_of_le
Proof state before:
𝕜 : Type u_1
ι : Type u_2
α : Type u_3
s K : Set α
inst✝ : NormedField 𝕜
F G : ι → α → 𝕜
f g : α → 𝕜
x y : 𝕜
η η' : ℝ
p : Filter ι
mf mg : ℝ
hF : TendstoUniformlyOn F f p s
hG : TendstoUniformlyOn G g p s
hf : ∀ᶠ (i : ι) in p, ∀ x ∈ s, ‖F i x‖ ≤ mf
hg : ∀ᶠ (i : ι) in p, ∀ x ∈ s, ‖G i x‖ ≤ mg
h : ¬NeBot p
⊢ TendstoUniformlyOn (F * G) (f * g) p s
Tactic:
simp at h
Proof state after:
𝕜 : Type u_1
ι : Type u_2
α : Type u_3
s K : Set α
inst✝ : NormedField 𝕜
F G : ι → α → 𝕜
f g : α → 𝕜
x y : 𝕜
η η' : ℝ
p : Filter ι
mf mg : ℝ
hF : TendstoUniformlyOn F f p s
hG : TendstoUniformlyOn G g p s
hf : ∀ᶠ (i : ι) in p, ∀ x ∈ s, ‖F i x‖ ≤ mf
hg : ∀ᶠ (i : ι) in p, ∀ x ∈ s, ‖G i x‖ ≤ mg
h : p = ⊥
⊢ TendstoUniformlyOn (F * G) (f * g) p s
Theorem: TendstoUniformlyOn.mul_of_le
Proof state before:
𝕜 : Type u_1
ι : Type u_2
α : Type u_3
s K : Set α
inst✝ : NormedField 𝕜
F G : ι → α → 𝕜
f g : α → 𝕜
x y : 𝕜
η η' : ℝ
p : Filter ι
mf mg : ℝ
hF : TendstoUniformlyOn F f p s
hG : TendstoUniformlyOn G g p s
hf : ∀ᶠ (i : ι) in p, ∀ x ∈ s, ‖F i x‖ ≤ mf
hg : ∀ᶠ (i : ι) in p, ∀ x ∈ s, ‖G i x‖ ≤ mg
h : p = ⊥
⊢ TendstoUniformlyOn (F * G) (f * g) p s
Tactic:
simp [h, TendstoUniformlyOn]
Proof state after:
no goals
Theorem: TendstoUniformlyOn.mul_of_le
Proof state before:
𝕜 : Type u_1
ι : Type u_2
α : Type u_3
s K : Set α
inst✝ : NormedField 𝕜
F G : ι → α → 𝕜
f g : α → 𝕜
x y : 𝕜
η η' : ℝ
p : Filter ι
mf mg : ℝ
hF : TendstoUniformlyOn F f p s
hG : TendstoUniformlyOn G g p s
hf : ∀ᶠ (i : ι) in p, ∀ x ∈ s, ‖F i x‖ ≤ mf
hg : ∀ᶠ (i : ι) in p, ∀ x ∈ s, ‖G i x‖ ≤ mg
h : NeBot p
⊢ TendstoUniformlyOn (F * G) (f * g) p s
Tactic:
set Mf := |mf| + 1
Proof state after:
𝕜 : Type u_1
ι : Type u_2
α : Type u_3
s K : Set α
inst✝ : NormedField 𝕜
F G : ι → α → 𝕜
f g : α → 𝕜
x y : 𝕜
η η' : ℝ
p : Filter ι
mf mg : ℝ
hF : TendstoUniformlyOn F f p s
hG : TendstoUniformlyOn G g p s
hf : ∀ᶠ (i : ι) in p, ∀ x ∈ s, ‖F i x‖ ≤ mf
hg : ∀ᶠ (i : ι) in p, ∀ x ∈ s, ‖G i x‖ ≤ mg
h : NeBot p
Mf : ℝ := |mf| + 1
⊢ TendstoUniformlyOn (F * G) (f * g) p s
Theorem: TendstoUniformlyOn.mul_of_le
Proof state before:
𝕜 : Type u_1
ι : Type u_2
α : Type u_3
s K : Set α
inst✝ : NormedField 𝕜
F G : ι → α → 𝕜
f g : α → 𝕜
x y : 𝕜
η η' : ℝ
p : Filter ι
mf mg : ℝ
hF : TendstoUniformlyOn F f p s
hG : TendstoUniformlyOn G g p s
hf : ∀ᶠ (i : ι) in p, ∀ x ∈ s, ‖F i x‖ ≤ mf
hg : ∀ᶠ (i : ι) in p, ∀ x ∈ s, ‖G i x‖ ≤ mg
h : NeBot p
Mf : ℝ := |mf| + 1
⊢ TendstoUniformlyOn (F * G) (f * g) p s
Tactic:
set Mg := |mg| + 1
Proof state after:
𝕜 : Type u_1
ι : Type u_2
α : Type u_3
s K : Set α
inst✝ : NormedField 𝕜
F G : ι → α → 𝕜
f g : α → 𝕜
x y : 𝕜
η η' : ℝ
p : Filter ι
mf mg : ℝ
hF : TendstoUniformlyOn F f p s
hG : TendstoUniformlyOn G g p s
hf : ∀ᶠ (i : ι) in p, ∀ x ∈ s, ‖F i x‖ ≤ mf
hg : ∀ᶠ (i : ι) in p, ∀ x ∈ s, ‖G i x‖ ≤ mg
h : NeBot p
Mf : ℝ := |mf| + 1
Mg : ℝ := |mg| + 1
⊢ TendstoUniformlyOn (F * G) (f * g) p s
Theorem: TendstoUniformlyOn.mul_of_le
Proof state before:
𝕜 : Type u_1
ι : Type u_2
α : Type u_3
s K : Set α
inst✝ : NormedField 𝕜
F G : ι → α → 𝕜
f g : α → 𝕜
x y : 𝕜
η η' : ℝ
p : Filter ι
mf mg : ℝ
hF : TendstoUniformlyOn F f p s
hG : TendstoUniformlyOn G g p s
hf : ∀ᶠ (i : ι) in p, ∀ x ∈ s, ‖F i x‖ ≤ mf
hg : ∀ᶠ (i : ι) in p, ∀ x ∈ s, ‖G i x‖ ≤ mg
h : NeBot p
Mf : ℝ := |mf| + 1
Mg : ℝ := |mg| + 1
⊢ TendstoUniformlyOn (F * G) (f * g) p s
Tactic:
have hMf : 0 < Mf := by positivity
Proof state after:
𝕜 : Type u_1
ι : Type u_2
α : Type u_3
s K : Set α
inst✝ : NormedField 𝕜
F G : ι → α → 𝕜
f g : α → 𝕜
x y : 𝕜
η η' : ℝ
p : Filter ι
mf mg : ℝ
hF : TendstoUniformlyOn F f p s
hG : TendstoUniformlyOn G g p s
hf : ∀ᶠ (i : ι) in p, ∀ x ∈ s, ‖F i x‖ ≤ mf
hg : ∀ᶠ (i : ι) in p, ∀ x ∈ s, ‖G i x‖ ≤ mg
h : NeBot p
Mf : ℝ := |mf| + 1
Mg : ℝ := |mg| + 1
hMf : 0 < Mf
⊢ TendstoUniformlyOn (F * G) (f * g) p s
Theorem: TendstoUniformlyOn.mul_of_le
Proof state before:
𝕜 : Type u_1
ι : Type u_2
α : Type u_3
s K : Set α
inst✝ : NormedField 𝕜
F G : ι → α → 𝕜
f g : α → 𝕜
x y : 𝕜
η η' : ℝ
p : Filter ι
mf mg : ℝ
hF : TendstoUniformlyOn F f p s
hG : TendstoUniformlyOn G g p s
hf : ∀ᶠ (i : ι) in p, ∀ x ∈ s, ‖F i x‖ ≤ mf
hg : ∀ᶠ (i : ι) in p, ∀ x ∈ s, ‖G i x‖ ≤ mg
h : NeBot p
Mf : ℝ := |mf| + 1
Mg : ℝ := |mg| + 1
hMf : 0 < Mf
⊢ TendstoUniformlyOn (F * G) (f * g) p s
Tactic:
have hMg : 0 < Mg := by positivity
Proof state after:
𝕜 : Type u_1
ι : Type u_2
α : Type u_3
s K : Set α
inst✝ : NormedField 𝕜
F G : ι → α → 𝕜
f g : α → 𝕜
x y : 𝕜
η η' : ℝ
p : Filter ι
mf mg : ℝ
hF : TendstoUniformlyOn F f p s
hG : TendstoUniformlyOn G g p s
hf : ∀ᶠ (i : ι) in p, ∀ x ∈ s, ‖F i x‖ ≤ mf
hg : ∀ᶠ (i : ι) in p, ∀ x ∈ s, ‖G i x‖ ≤ mg
h : NeBot p
Mf : ℝ := |mf| + 1
Mg : ℝ := |mg| + 1
hMf : 0 < Mf
hMg : 0 < Mg
⊢ TendstoUniformlyOn (F * G) (f * g) p s
Theorem: TendstoUniformlyOn.mul_of_le
Proof state before:
𝕜 : Type u_1
ι : Type u_2
α : Type u_3
s K : Set α
inst✝ : NormedField 𝕜
F G : ι → α → 𝕜
f g : α → 𝕜
x y : 𝕜
η η' : ℝ
p : Filter ι
mf mg : ℝ
hF : TendstoUniformlyOn F f p s
hG : TendstoUniformlyOn G g p s
hf : ∀ᶠ (i : ι) in p, ∀ x ∈ s, ‖F i x‖ ≤ mf
hg : ∀ᶠ (i : ι) in p, ∀ x ∈ s, ‖G i x‖ ≤ mg
h : NeBot p
Mf : ℝ := |mf| + 1
Mg : ℝ := |mg| + 1
hMf : 0 < Mf
hMg : 0 < Mg
⊢ TendstoUniformlyOn (F * G) (f * g) p s
Tactic:
replace hf : ∀ᶠ i in p, ∀ x ∈ s, ‖F i x‖ ≤ Mf := by
  filter_upwards [hf] with i hF x hx using (hF x hx).trans ((le_abs_self mf).trans (lt_add_one _).le)
Proof state after:
𝕜 : Type u_1
ι : Type u_2
α : Type u_3
s K : Set α
inst✝ : NormedField 𝕜
F G : ι → α → 𝕜
f g : α → 𝕜
x y : 𝕜
η η' : ℝ
p : Filter ι
mf mg : ℝ
hF : TendstoUniformlyOn F f p s
hG : TendstoUniformlyOn G g p s
hg : ∀ᶠ (i : ι) in p, ∀ x ∈ s, ‖G i x‖ ≤ mg
h : NeBot p
Mf : ℝ := |mf| + 1
Mg : ℝ := |mg| + 1
hMf : 0 < Mf
hMg : 0 < Mg
hf : ∀ᶠ (i : ι) in p, ∀ x ∈ s, ‖F i x‖ ≤ Mf
⊢ TendstoUniformlyOn (F * G) (f * g) p s
Theorem: TendstoUniformlyOn.mul_of_le
Proof state before:
𝕜 : Type u_1
ι : Type u_2
α : Type u_3
s K : Set α
inst✝ : NormedField 𝕜
F G : ι → α → 𝕜
f g : α → 𝕜
x y : 𝕜
η η' : ℝ
p : Filter ι
mf mg : ℝ
hF : TendstoUniformlyOn F f p s
hG : TendstoUniformlyOn G g p s
hg : ∀ᶠ (i : ι) in p, ∀ x ∈ s, ‖G i x‖ ≤ mg
h : NeBot p
Mf : ℝ := |mf| + 1
Mg : ℝ := |mg| + 1
hMf : 0 < Mf
hMg : 0 < Mg
hf : ∀ᶠ (i : ι) in p, ∀ x ∈ s, ‖F i x‖ ≤ Mf
⊢ TendstoUniformlyOn (F * G) (f * g) p s
Tactic:
replace hg : ∀ᶠ i in p, ∀ x ∈ s, ‖G i x‖ ≤ Mg := by
  filter_upwards [hg] with i hG x hx using (hG x hx).trans ((le_abs_self mg).trans (lt_add_one _).le)
Proof state after:
𝕜 : Type u_1
ι : Type u_2
α : Type u_3
s K : Set α
inst✝ : NormedField 𝕜
F G : ι → α → 𝕜
f g : α → 𝕜
x y : 𝕜
η η' : ℝ
p : Filter ι
mf mg : ℝ
hF : TendstoUniformlyOn F f p s
hG : TendstoUniformlyOn G g p s
h : NeBot p
Mf : ℝ := |mf| + 1
Mg : ℝ := |mg| + 1
hMf : 0 < Mf
hMg : 0 < Mg
hf : ∀ᶠ (i : ι) in p, ∀ x ∈ s, ‖F i x‖ ≤ Mf
hg : ∀ᶠ (i : ι) in p, ∀ x ∈ s, ‖G i x‖ ≤ Mg
⊢ TendstoUniformlyOn (F * G) (f * g) p s
Theorem: TendstoUniformlyOn.mul_of_le
Proof state before:
𝕜 : Type u_1
ι : Type u_2
α : Type u_3
s K : Set α
inst✝ : NormedField 𝕜
F G : ι → α → 𝕜
f g : α → 𝕜
x y : 𝕜
η η' : ℝ
p : Filter ι
mf mg : ℝ
hF : TendstoUniformlyOn F f p s
hG : TendstoUniformlyOn G g p s
h : NeBot p
Mf : ℝ := |mf| + 1
Mg : ℝ := |mg| + 1
hMf : 0 < Mf
hMg : 0 < Mg
hf : ∀ᶠ (i : ι) in p, ∀ x ∈ s, ‖F i x‖ ≤ Mf
hg : ∀ᶠ (i : ι) in p, ∀ x ∈ s, ‖G i x‖ ≤ Mg
⊢ TendstoUniformlyOn (F * G) (f * g) p s
Tactic:
have h1 : ∀ x ∈ s, ‖g x‖ ≤ Mg := by
  intro x hx
  refine le_of_tendsto ((continuous_norm.tendsto (g x)).comp (hG.tendsto_at hx)) ?_
  filter_upwards [hg] with i hg using hg x hx
Proof state after:
𝕜 : Type u_1
ι : Type u_2
α : Type u_3
s K : Set α
inst✝ : NormedField 𝕜
F G : ι → α → 𝕜
f g : α → 𝕜
x y : 𝕜
η η' : ℝ
p : Filter ι
mf mg : ℝ
hF : TendstoUniformlyOn F f p s
hG : TendstoUniformlyOn G g p s
h : NeBot p
Mf : ℝ := |mf| + 1
Mg : ℝ := |mg| + 1
hMf : 0 < Mf
hMg : 0 < Mg
hf : ∀ᶠ (i : ι) in p, ∀ x ∈ s, ‖F i x‖ ≤ Mf
hg : ∀ᶠ (i : ι) in p, ∀ x ∈ s, ‖G i x‖ ≤ Mg
h1 : ∀ x ∈ s, ‖g x‖ ≤ Mg
⊢ TendstoUniformlyOn (F * G) (f * g) p s
Theorem: TendstoUniformlyOn.mul_of_le
Proof state before:
𝕜 : Type u_1
ι : Type u_2
α : Type u_3
s K : Set α
inst✝ : NormedField 𝕜
F G : ι → α → 𝕜
f g : α → 𝕜
x y : 𝕜
η η' : ℝ
p : Filter ι
mf mg : ℝ
hF : TendstoUniformlyOn F f p s
hG : TendstoUniformlyOn G g p s
h : NeBot p
Mf : ℝ := |mf| + 1
Mg : ℝ := |mg| + 1
hMf : 0 < Mf
hMg : 0 < Mg
hf : ∀ᶠ (i : ι) in p, ∀ x ∈ s, ‖F i x‖ ≤ Mf
hg : ∀ᶠ (i : ι) in p, ∀ x ∈ s, ‖G i x‖ ≤ Mg
h1 : ∀ x ∈ s, ‖g x‖ ≤ Mg
⊢ TendstoUniformlyOn (F * G) (f * g) p s
Tactic:
simp_rw [Metric.tendstoUniformlyOn_iff, dist_eq_norm] at hF hG ⊢
Proof state after:
𝕜 : Type u_1
ι : Type u_2
α : Type u_3
s K : Set α
inst✝ : NormedField 𝕜
F G : ι → α → 𝕜
f g : α → 𝕜
x y : 𝕜
η η' : ℝ
p : Filter ι
mf mg : ℝ
h : NeBot p
Mf : ℝ := |mf| + 1
Mg : ℝ := |mg| + 1
hMf : 0 < Mf
hMg : 0 < Mg
hf : ∀ᶠ (i : ι) in p, ∀ x ∈ s, ‖F i x‖ ≤ Mf
hg : ∀ᶠ (i : ι) in p, ∀ x ∈ s, ‖G i x‖ ≤ Mg
h1 : ∀ x ∈ s, ‖g x‖ ≤ Mg
hF : ∀ ε > 0, ∀ᶠ (n : ι) in p, ∀ x ∈ s, ‖f x - F n x‖ < ε
hG : ∀ ε > 0, ∀ᶠ (n : ι) in p, ∀ x ∈ s, ‖g x - G n x‖ < ε
⊢ ∀ ε > 0, ∀ᶠ (n : ι) in p, ∀ x ∈ s, ‖(f * g) x - (F * G) n x‖ < ε