internlm/Lean-Github huggingface dataset:
Theorem: 𝓘_nonempty
Proof state before:
U : Set ℂ
Q : Set ℂ → Set ℂ
ι : Type u_1
l : Filter ι
inst✝ : good_domain U
u : ℂ
hu : u ∈ Uᶜ
f : ℂ → ℂ := fun z => z - u
f_inj : Injective f
f_hol : DifferentiableOn ℂ f U
f_noz : ∀ ⦃z : ℂ⦄, z ∈ U → f z ≠ 0
g : ℂ → ℂ
g_hol : DifferentiableOn ℂ g U
g_sqf : EqOn f (g ^ 2) U
z₀ : ℂ
hz₀ : z₀ ∈ U
gU_nhd : g '' U ∈ 𝓝 (g z₀)
r : ℝ
r_pos : r > 0
hr : ball (g z₀) r ⊆ g '' U
z : ℂ
hz : z ∈ U
hgz : g z ∈ closedBall (-g z₀) (r / 2)
⊢ f z = 0
Tactic:
rw [mem_closed_ball_neg_iff_mem_neg_closed_ball] at hgz
Proof state after:
U : Set ℂ
Q : Set ℂ → Set ℂ
ι : Type u_1
l : Filter ι
inst✝ : good_domain U
u : ℂ
hu : u ∈ Uᶜ
f : ℂ → ℂ := fun z => z - u
f_inj : Injective f
f_hol : DifferentiableOn ℂ f U
f_noz : ∀ ⦃z : ℂ⦄, z ∈ U → f z ≠ 0
g : ℂ → ℂ
g_hol : DifferentiableOn ℂ g U
g_sqf : EqOn f (g ^ 2) U
z₀ : ℂ
hz₀ : z₀ ∈ U
gU_nhd : g '' U ∈ 𝓝 (g z₀)
r : ℝ
r_pos : r > 0
hr : ball (g z₀) r ⊆ g '' U
z : ℂ
hz : z ∈ U
hgz : -g z ∈ closedBall (g z₀) (r / 2)
⊢ f z = 0
Theorem: 𝓘_nonempty
Proof state before:
U : Set ℂ
Q : Set ℂ → Set ℂ
ι : Type u_1
l : Filter ι
inst✝ : good_domain U
u : ℂ
hu : u ∈ Uᶜ
f : ℂ → ℂ := fun z => z - u
f_inj : Injective f
f_hol : DifferentiableOn ℂ f U
f_noz : ∀ ⦃z : ℂ⦄, z ∈ U → f z ≠ 0
g : ℂ → ℂ
g_hol : DifferentiableOn ℂ g U
g_sqf : EqOn f (g ^ 2) U
z₀ : ℂ
hz₀ : z₀ ∈ U
gU_nhd : g '' U ∈ 𝓝 (g z₀)
r : ℝ
r_pos : r > 0
hr : ball (g z₀) r ⊆ g '' U
z : ℂ
hz : z ∈ U
hgz : -g z ∈ closedBall (g z₀) (r / 2)
⊢ f z = 0
Tactic:
obtain ⟨z', hz', hgz'⟩ := (closedBall_subset_ball (by linarith)).trans hr hgz
Proof state after:
case intro.intro
U : Set ℂ
Q : Set ℂ → Set ℂ
ι : Type u_1
l : Filter ι
inst✝ : good_domain U
u : ℂ
hu : u ∈ Uᶜ
f : ℂ → ℂ := fun z => z - u
f_inj : Injective f
f_hol : DifferentiableOn ℂ f U
f_noz : ∀ ⦃z : ℂ⦄, z ∈ U → f z ≠ 0
g : ℂ → ℂ
g_hol : DifferentiableOn ℂ g U
g_sqf : EqOn f (g ^ 2) U
z₀ : ℂ
hz₀ : z₀ ∈ U
gU_nhd : g '' U ∈ 𝓝 (g z₀)
r : ℝ
r_pos : r > 0
hr : ball (g z₀) r ⊆ g '' U
z : ℂ
hz : z ∈ U
hgz : -g z ∈ closedBall (g z₀) (r / 2)
z' : ℂ
hz' : z' ∈ U
hgz' : g z' = -g z
⊢ f z = 0
Theorem: 𝓘_nonempty
Proof state before:
case intro.intro
U : Set ℂ
Q : Set ℂ → Set ℂ
ι : Type u_1
l : Filter ι
inst✝ : good_domain U
u : ℂ
hu : u ∈ Uᶜ
f : ℂ → ℂ := fun z => z - u
f_inj : Injective f
f_hol : DifferentiableOn ℂ f U
f_noz : ∀ ⦃z : ℂ⦄, z ∈ U → f z ≠ 0
g : ℂ → ℂ
g_hol : DifferentiableOn ℂ g U
g_sqf : EqOn f (g ^ 2) U
z₀ : ℂ
hz₀ : z₀ ∈ U
gU_nhd : g '' U ∈ 𝓝 (g z₀)
r : ℝ
r_pos : r > 0
hr : ball (g z₀) r ⊆ g '' U
z : ℂ
hz : z ∈ U
hgz : -g z ∈ closedBall (g z₀) (r / 2)
z' : ℂ
hz' : z' ∈ U
hgz' : g z' = -g z
⊢ f z = 0
Tactic:
have hzz' : z = z' := f_inj (by simp [g_sqf hz, g_sqf hz', hgz'])
Proof state after:
case intro.intro
U : Set ℂ
Q : Set ℂ → Set ℂ
ι : Type u_1
l : Filter ι
inst✝ : good_domain U
u : ℂ
hu : u ∈ Uᶜ
f : ℂ → ℂ := fun z => z - u
f_inj : Injective f
f_hol : DifferentiableOn ℂ f U
f_noz : ∀ ⦃z : ℂ⦄, z ∈ U → f z ≠ 0
g : ℂ → ℂ
g_hol : DifferentiableOn ℂ g U
g_sqf : EqOn f (g ^ 2) U
z₀ : ℂ
hz₀ : z₀ ∈ U
gU_nhd : g '' U ∈ 𝓝 (g z₀)
r : ℝ
r_pos : r > 0
hr : ball (g z₀) r ⊆ g '' U
z : ℂ
hz : z ∈ U
hgz : -g z ∈ closedBall (g z₀) (r / 2)
z' : ℂ
hz' : z' ∈ U
hgz' : g z' = -g z
hzz' : z = z'
⊢ f z = 0
Theorem: 𝓘_nonempty
Proof state before:
case intro.intro
U : Set ℂ
Q : Set ℂ → Set ℂ
ι : Type u_1
l : Filter ι
inst✝ : good_domain U
u : ℂ
hu : u ∈ Uᶜ
f : ℂ → ℂ := fun z => z - u
f_inj : Injective f
f_hol : DifferentiableOn ℂ f U
f_noz : ∀ ⦃z : ℂ⦄, z ∈ U → f z ≠ 0
g : ℂ → ℂ
g_hol : DifferentiableOn ℂ g U
g_sqf : EqOn f (g ^ 2) U
z₀ : ℂ
hz₀ : z₀ ∈ U
gU_nhd : g '' U ∈ 𝓝 (g z₀)
r : ℝ
r_pos : r > 0
hr : ball (g z₀) r ⊆ g '' U
z : ℂ
hz : z ∈ U
hgz : -g z ∈ closedBall (g z₀) (r / 2)
z' : ℂ
hz' : z' ∈ U
hgz' : g z' = -g z
hzz' : z = z'
⊢ f z = 0
Tactic:
simpa [hzz', neg_eq_self_iff, g_sqf hz'] using hgz'.symm
Proof state after:
no goals
Theorem: 𝓘_nonempty
Proof state before:
U : Set ℂ
Q : Set ℂ → Set ℂ
ι : Type u_1
l : Filter ι
inst✝ : good_domain U
u : ℂ
hu : u ∈ Uᶜ
f : ℂ → ℂ := fun z => z - u
f_inj : Injective f
f_hol : DifferentiableOn ℂ f U
f_noz : ∀ ⦃z : ℂ⦄, z ∈ U → f z ≠ 0
g : ℂ → ℂ
g_hol : DifferentiableOn ℂ g U
g_sqf : EqOn f (g ^ 2) U
z₀ : ℂ
hz₀ : z₀ ∈ U
gU_nhd : g '' U ∈ 𝓝 (g z₀)
r : ℝ
r_pos : r > 0
hr : ball (g z₀) r ⊆ g '' U
z : ℂ
hz : z ∈ U
hgz : -g z ∈ closedBall (g z₀) (r / 2)
⊢ r / 2 < r
Tactic:
linarith
Proof state after:
no goals
Theorem: 𝓘_nonempty
Proof state before:
U : Set ℂ
Q : Set ℂ → Set ℂ
ι : Type u_1
l : Filter ι
inst✝ : good_domain U
u : ℂ
hu : u ∈ Uᶜ
f : ℂ → ℂ := fun z => z - u
f_inj : Injective f
f_hol : DifferentiableOn ℂ f U
f_noz : ∀ ⦃z : ℂ⦄, z ∈ U → f z ≠ 0
g : ℂ → ℂ
g_hol : DifferentiableOn ℂ g U
g_sqf : EqOn f (g ^ 2) U
z₀ : ℂ
hz₀ : z₀ ∈ U
gU_nhd : g '' U ∈ 𝓝 (g z₀)
r : ℝ
r_pos : r > 0
hr : ball (g z₀) r ⊆ g '' U
z : ℂ
hz : z ∈ U
hgz : -g z ∈ closedBall (g z₀) (r / 2)
z' : ℂ
hz' : z' ∈ U
hgz' : g z' = -g z
⊢ f z = f z'
Tactic:
simp [g_sqf hz, g_sqf hz', hgz']
Proof state after:
no goals
Theorem: 𝓘_nonempty
Proof state before:
U : Set ℂ
Q : Set ℂ → Set ℂ
ι : Type u_1
l : Filter ι
inst✝ : good_domain U
u : ℂ
hu : u ∈ Uᶜ
f : ℂ → ℂ := fun z => z - u
f_inj : Injective f
f_hol : DifferentiableOn ℂ f U
f_noz : ∀ ⦃z : ℂ⦄, z ∈ U → f z ≠ 0
g : ℂ → ℂ
g_hol : DifferentiableOn ℂ g U
g_sqf : EqOn f (g ^ 2) U
z₀ : ℂ
hz₀ : z₀ ∈ U
gU_nhd : g '' U ∈ 𝓝 (g z₀)
r : ℝ
r_pos : r > 0
hr : ball (g z₀) r ⊆ g '' U
gg : embedding U (closedBall (-g z₀) (r / 2))ᶜ := { to_fun := g, is_diff := g_hol, is_inj := ⋯, maps_to := ⋯ }
⊢ 0 < r / 2
Tactic:
linarith
Proof state after:
no goals
Theorem: mem_iff_eventually_subset
Proof state before:
α : Type u_1
𝕜 : Type u_2
s : Set α
z₀ : α
P : α → Prop
p : Filter α
φ : ℝ → Set α
hp : HasBasis p (fun t => 0 < t) φ
hφ : Monotone φ
⊢ s ∈ p ↔ ∀ᶠ (t : ℝ) in 𝓝[>] 0, φ t ⊆ s
Tactic:
rw [(nhdsWithin_hasBasis nhds_basis_closedBall (Ioi (0 : ℝ))).eventually_iff]
Proof state after:
α : Type u_1
𝕜 : Type u_2
s : Set α
z₀ : α
P : α → Prop
p : Filter α
φ : ℝ → Set α
hp : HasBasis p (fun t => 0 < t) φ
hφ : Monotone φ
⊢ s ∈ p ↔ ∃ i, 0 < i ∧ ∀ ⦃x : ℝ⦄, x ∈ closedBall 0 i ∩ Ioi 0 → φ x ⊆ s
Theorem: mem_iff_eventually_subset
Proof state before:
α : Type u_1
𝕜 : Type u_2
s : Set α
z₀ : α
P : α → Prop
p : Filter α
φ : ℝ → Set α
hp : HasBasis p (fun t => 0 < t) φ
hφ : Monotone φ
⊢ s ∈ p ↔ ∃ i, 0 < i ∧ ∀ ⦃x : ℝ⦄, x ∈ closedBall 0 i ∩ Ioi 0 → φ x ⊆ s
Tactic:
simp_rw [hp.mem_iff, ← exists_prop, mem_inter_iff, mem_closedBall_zero_iff]
Proof state after:
α : Type u_1
𝕜 : Type u_2
s : Set α
z₀ : α
P : α → Prop
p : Filter α
φ : ℝ → Set α
hp : HasBasis p (fun t => 0 < t) φ
hφ : Monotone φ
⊢ (∃ i, ∃ (_ : 0 < i), φ i ⊆ s) ↔ ∃ i, ∃ (_ : 0 < i), ∀ ⦃x : ℝ⦄, ‖x‖ ≤ i ∧ x ∈ Ioi 0 → φ x ⊆ s
Theorem: mem_iff_eventually_subset
Proof state before:
α : Type u_1
𝕜 : Type u_2
s : Set α
z₀ : α
P : α → Prop
p : Filter α
φ : ℝ → Set α
hp : HasBasis p (fun t => 0 < t) φ
hφ : Monotone φ
⊢ (∃ i, ∃ (_ : 0 < i), φ i ⊆ s) ↔ ∃ i, ∃ (_ : 0 < i), ∀ ⦃x : ℝ⦄, ‖x‖ ≤ i ∧ x ∈ Ioi 0 → φ x ⊆ s
Tactic:
refine exists₂_congr (λ ε hε => ⟨λ h r h' => (hφ (le_of_abs_le h'.1)).trans h,
  λ h => h ⟨Eq.le (abs_eq_self.mpr hε.le), hε⟩⟩)
Proof state after:
no goals
Theorem: dist_inv_le_dist_div
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 : ℝ
hη : 0 < η
hη' : 0 < η'
hx : x ∉ ball 0 η
hy : y ∉ ball 0 η'
⊢ dist x⁻¹ y⁻¹ ≤ dist x y / (η * η')
Tactic:
have h1 : x ≠ 0 := by contrapose! hx; simp only [hx, mem_ball_self, 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 : ℝ
hη : 0 < η
hη' : 0 < η'
hx : x ∉ ball 0 η
hy : y ∉ ball 0 η'
h1 : x ≠ 0
⊢ dist x⁻¹ y⁻¹ ≤ dist x y / (η * η')
Theorem: dist_inv_le_dist_div
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 : ℝ
hη : 0 < η
hη' : 0 < η'
hx : x ∉ ball 0 η
hy : y ∉ ball 0 η'
h1 : x ≠ 0
⊢ dist x⁻¹ y⁻¹ ≤ dist x y / (η * η')
Tactic:
have h2 : y ≠ 0 := by contrapose! hy; simp only [hy, mem_ball_self, 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 : ℝ
hη : 0 < η
hη' : 0 < η'
hx : x ∉ ball 0 η
hy : y ∉ ball 0 η'
h1 : x ≠ 0
h2 : y ≠ 0
⊢ dist x⁻¹ y⁻¹ ≤ dist x y / (η * η')
Theorem: dist_inv_le_dist_div
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 : ℝ
hη : 0 < η
hη' : 0 < η'
hx : x ∉ ball 0 η
hy : y ∉ ball 0 η'
h1 : x ≠ 0
h2 : y ≠ 0
⊢ dist x⁻¹ y⁻¹ ≤ dist x y / (η * η')
Tactic:
simp only [mem_ball, dist_eq_norm, sub_zero, not_lt] at hx hy
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η : 0 < η
hη' : 0 < η'
h1 : x ≠ 0
h2 : y ≠ 0
hx : η ≤ ‖x‖
hy : η' ≤ ‖y‖
⊢ dist x⁻¹ y⁻¹ ≤ dist x y / (η * η')
Theorem: dist_inv_le_dist_div
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 : ℝ
hη : 0 < η
hη' : 0 < η'
h1 : x ≠ 0
h2 : y ≠ 0
hx : η ≤ ‖x‖
hy : η' ≤ ‖y‖
⊢ dist x⁻¹ y⁻¹ ≤ dist x y / (η * η')
Tactic:
rw [dist_inv_inv₀ h1 h2]
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η : 0 < η
hη' : 0 < η'
h1 : x ≠ 0
h2 : y ≠ 0
hx : η ≤ ‖x‖
hy : η' ≤ ‖y‖
⊢ dist x y / (‖x‖ * ‖y‖) ≤ dist x y / (η * η')
Theorem: dist_inv_le_dist_div
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 : ℝ
hη : 0 < η
hη' : 0 < η'
h1 : x ≠ 0
h2 : y ≠ 0
hx : η ≤ ‖x‖
hy : η' ≤ ‖y‖
⊢ dist x y / (‖x‖ * ‖y‖) ≤ dist x y / (η * η')
Tactic:
gcongr
Proof state after:
no goals
Theorem: dist_inv_le_dist_div
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 : ℝ
hη : 0 < η
hη' : 0 < η'
hx : x ∉ ball 0 η
hy : y ∉ ball 0 η'
⊢ x ≠ 0
Tactic:
contrapose! 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 : ℝ
hη : 0 < η
hη' : 0 < η'
hy : y ∉ ball 0 η'
hx : x = 0
⊢ x ∈ ball 0 η
Theorem: dist_inv_le_dist_div
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 : ℝ
hη : 0 < η
hη' : 0 < η'
hy : y ∉ ball 0 η'
hx : x = 0
⊢ x ∈ ball 0 η
Tactic:
simp only [hx, mem_ball_self, hη]
Proof state after:
no goals
Theorem: dist_inv_le_dist_div
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 : ℝ
hη : 0 < η
hη' : 0 < η'
hx : x ∉ ball 0 η
hy : y ∉ ball 0 η'
h1 : x ≠ 0
⊢ y ≠ 0
Tactic:
contrapose! hy
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η : 0 < η
hη' : 0 < η'
hx : x ∉ ball 0 η
h1 : x ≠ 0
hy : y = 0
⊢ y ∈ ball 0 η'
Theorem: dist_inv_le_dist_div
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 : ℝ
hη : 0 < η
hη' : 0 < η'
hx : x ∉ ball 0 η
h1 : x ≠ 0
hy : y = 0
⊢ y ∈ ball 0 η'
Tactic:
simp only [hy, mem_ball_self, hη']
Proof state after:
no goals
Theorem: titi
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 : ℝ
p q : Filter 𝕜
hp : p ⊓ 𝓝 0 = ⊥
hq : q ⊓ 𝓝 0 = ⊥
⊢ map (fun x => (x.1⁻¹, x.2⁻¹)) (𝓤 𝕜 ⊓ p ×ˢ q) ≤ 𝓤 𝕜
Tactic:
obtain ⟨U, hU, V, hV, hUV⟩ := inf_eq_bot_iff.mp hp
Proof state after:
case 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 = ∅
⊢ map (fun x => (x.1⁻¹, x.2⁻¹)) (𝓤 𝕜 ⊓ p ×ˢ q) ≤ 𝓤 𝕜
Theorem: titi
Proof state before:
case 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 = ∅
⊢ map (fun x => (x.1⁻¹, x.2⁻¹)) (𝓤 𝕜 ⊓ p ×ˢ q) ≤ 𝓤 𝕜
Tactic:
obtain ⟨U', hU', V', hV', hUV'⟩ := inf_eq_bot_iff.mp hq
Proof state after:
case 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' = ∅
⊢ map (fun x => (x.1⁻¹, x.2⁻¹)) (𝓤 𝕜 ⊓ p ×ˢ q) ≤ 𝓤 𝕜
Theorem: titi
Proof state before:
case 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' = ∅
⊢ map (fun x => (x.1⁻¹, x.2⁻¹)) (𝓤 𝕜 ⊓ p ×ˢ q) ≤ 𝓤 𝕜
Tactic:
obtain ⟨η, hη, hV⟩ := Metric.mem_nhds_iff.mp hV
Proof state after:
case 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
⊢ map (fun x => (x.1⁻¹, x.2⁻¹)) (𝓤 𝕜 ⊓ p ×ˢ q) ≤ 𝓤 𝕜
Theorem: titi
Proof state before:
case 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
⊢ map (fun x => (x.1⁻¹, x.2⁻¹)) (𝓤 𝕜 ⊓ p ×ˢ q) ≤ 𝓤 𝕜
Tactic:
obtain ⟨η', hη', hV'⟩ := Metric.mem_nhds_iff.mp hV'
Proof state after:
case 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'
⊢ map (fun x => (x.1⁻¹, x.2⁻¹)) (𝓤 𝕜 ⊓ p ×ˢ q) ≤ 𝓤 𝕜
Theorem: titi
Proof state before:
case 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'
⊢ map (fun x => (x.1⁻¹, x.2⁻¹)) (𝓤 𝕜 ⊓ p ×ˢ q) ≤ 𝓤 𝕜
Tactic:
have hηη' : 0 < η * η' := mul_pos hη hη'
Proof state after:
case 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 < η * η'
⊢ map (fun x => (x.1⁻¹, x.2⁻¹)) (𝓤 𝕜 ⊓ p ×ˢ q) ≤ 𝓤 𝕜
Theorem: titi
Proof state before:
case 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 < η * η'
⊢ map (fun x => (x.1⁻¹, x.2⁻¹)) (𝓤 𝕜 ⊓ p ×ˢ q) ≤ 𝓤 𝕜
Tactic:
intro u hu
Proof state after:
case 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 ∈ 𝓤 𝕜
⊢ u ∈ map (fun x => (x.1⁻¹, x.2⁻¹)) (𝓤 𝕜 ⊓ p ×ˢ q)
Theorem: titi
Proof state before:
case 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 ∈ 𝓤 𝕜
⊢ u ∈ map (fun x => (x.1⁻¹, x.2⁻¹)) (𝓤 𝕜 ⊓ p ×ˢ q)
Tactic:
obtain ⟨ε, hε, hu⟩ := mem_uniformity_dist.mp hu
Proof state after:
case 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
⊢ u ∈ map (fun x => (x.1⁻¹, x.2⁻¹)) (𝓤 𝕜 ⊓ p ×ˢ q)
Theorem: titi
Proof state before:
case 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
⊢ u ∈ map (fun x => (x.1⁻¹, x.2⁻¹)) (𝓤 𝕜 ⊓ p ×ˢ q)
Tactic:
rw [mem_map_iff_exists_image]
Proof state after:
case 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
⊢ ∃ s ∈ 𝓤 𝕜 ⊓ p ×ˢ q, (fun x => (x.1⁻¹, x.2⁻¹)) '' s ⊆ u
Theorem: titi
Proof state before:
case 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
⊢ ∃ s ∈ 𝓤 𝕜 ⊓ p ×ˢ q, (fun x => (x.1⁻¹, x.2⁻¹)) '' s ⊆ u
Tactic:
refine ⟨_, inter_mem_inf (dist_mem_uniformity (mul_pos hε hηη')) (prod_mem_prod hU hU'), ?_⟩
Proof state after:
case 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
⊢ (fun x => (x.1⁻¹, x.2⁻¹)) '' ({p | dist p.1 p.2 < ε * (η * η')} ∩ U ×ˢ U') ⊆ u
Theorem: titi
Proof state before:
case 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
⊢ (fun x => (x.1⁻¹, x.2⁻¹)) '' ({p | dist p.1 p.2 < ε * (η * η')} ∩ U ×ˢ U') ⊆ u
Tactic:
rintro z ⟨x, ⟨hx1, hx2⟩, rfl⟩
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'
⊢ (fun x => (x.1⁻¹, x.2⁻¹)) x ∈ u