[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : TopologicalSpace E
inst✝³ : AddCommGroup E
inst✝² : TopologicalAddGroup E
inst✝¹ : Module ℝ E
inst✝ : ContinuousSMul ℝ E
s : Set E
hs₀ : 0 ∈ s
hs₁ : Convex ℝ s
hs₂ : IsOpen s
x₀ : E
hx₀ : ¬x₀ ∈ s
⊢ ∃ f, ↑f x₀ = 1 ∧ ∀ (x : E), x ∈ s → ↑f x < 1
[PROOFSTEP]
let f : E →ₗ.[ℝ] ℝ := LinearPMap.mkSpanSingleton x₀ 1 (ne_of_mem_of_not_mem hs₀ hx₀).symm
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : TopologicalSpace E
inst✝³ : AddCommGroup E
inst✝² : TopologicalAddGroup E
inst✝¹ : Module ℝ E
inst✝ : ContinuousSMul ℝ E
s : Set E
hs₀ : 0 ∈ s
hs₁ : Convex ℝ s
hs₂ : IsOpen s
x₀ : E
hx₀ : ¬x₀ ∈ s
f : E →ₗ.[ℝ] ℝ := LinearPMap.mkSpanSingleton x₀ 1 (_ : x₀ ≠ 0)
⊢ ∃ f, ↑f x₀ = 1 ∧ ∀ (x : E), x ∈ s → ↑f x < 1
[PROOFSTEP]
have :=
  exists_extension_of_le_sublinear f (gauge s) (fun c hc => gauge_smul_of_nonneg hc.le)
    (gauge_add_le hs₁ <| absorbent_nhds_zero <| hs₂.mem_nhds hs₀) ?_
[GOAL]
case refine_2
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : TopologicalSpace E
inst✝³ : AddCommGroup E
inst✝² : TopologicalAddGroup E
inst✝¹ : Module ℝ E
inst✝ : ContinuousSMul ℝ E
s : Set E
hs₀ : 0 ∈ s
hs₁ : Convex ℝ s
hs₂ : IsOpen s
x₀ : E
hx₀ : ¬x₀ ∈ s
f : E →ₗ.[ℝ] ℝ := LinearPMap.mkSpanSingleton x₀ 1 (_ : x₀ ≠ 0)
this : ∃ g, (∀ (x : { x // x ∈ f.domain }), ↑g ↑x = ↑f x) ∧ ∀ (x : E), ↑g x ≤ gauge s x
⊢ ∃ f, ↑f x₀ = 1 ∧ ∀ (x : E), x ∈ s → ↑f x < 1
case refine_1
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : TopologicalSpace E
inst✝³ : AddCommGroup E
inst✝² : TopologicalAddGroup E
inst✝¹ : Module ℝ E
inst✝ : ContinuousSMul ℝ E
s : Set E
hs₀ : 0 ∈ s
hs₁ : Convex ℝ s
hs₂ : IsOpen s
x₀ : E
hx₀ : ¬x₀ ∈ s
f : E →ₗ.[ℝ] ℝ := LinearPMap.mkSpanSingleton x₀ 1 (_ : x₀ ≠ 0)
⊢ ∀ (x : { x // x ∈ f.domain }), ↑f x ≤ gauge s ↑x
[PROOFSTEP]
obtain ⟨φ, hφ₁, hφ₂⟩ := this
[GOAL]
case refine_2.intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : TopologicalSpace E
inst✝³ : AddCommGroup E
inst✝² : TopologicalAddGroup E
inst✝¹ : Module ℝ E
inst✝ : ContinuousSMul ℝ E
s : Set E
hs₀ : 0 ∈ s
hs₁ : Convex ℝ s
hs₂ : IsOpen s
x₀ : E
hx₀ : ¬x₀ ∈ s
f : E →ₗ.[ℝ] ℝ := LinearPMap.mkSpanSingleton x₀ 1 (_ : x₀ ≠ 0)
φ : E →ₗ[ℝ] ℝ
hφ₁ : ∀ (x : { x // x ∈ f.domain }), ↑φ ↑x = ↑f x
hφ₂ : ∀ (x : E), ↑φ x ≤ gauge s x
⊢ ∃ f, ↑f x₀ = 1 ∧ ∀ (x : E), x ∈ s → ↑f x < 1
case refine_1
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : TopologicalSpace E
inst✝³ : AddCommGroup E
inst✝² : TopologicalAddGroup E
inst✝¹ : Module ℝ E
inst✝ : ContinuousSMul ℝ E
s : Set E
hs₀ : 0 ∈ s
hs₁ : Convex ℝ s
hs₂ : IsOpen s
x₀ : E
hx₀ : ¬x₀ ∈ s
f : E →ₗ.[ℝ] ℝ := LinearPMap.mkSpanSingleton x₀ 1 (_ : x₀ ≠ 0)
⊢ ∀ (x : { x // x ∈ f.domain }), ↑f x ≤ gauge s ↑x
[PROOFSTEP]
have hφ₃ : φ x₀ = 1 := by
  rw [← f.domain.coe_mk x₀ (Submodule.mem_span_singleton_self _), hφ₁, LinearPMap.mkSpanSingleton'_apply_self]
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : TopologicalSpace E
inst✝³ : AddCommGroup E
inst✝² : TopologicalAddGroup E
inst✝¹ : Module ℝ E
inst✝ : ContinuousSMul ℝ E
s : Set E
hs₀ : 0 ∈ s
hs₁ : Convex ℝ s
hs₂ : IsOpen s
x₀ : E
hx₀ : ¬x₀ ∈ s
f : E →ₗ.[ℝ] ℝ := LinearPMap.mkSpanSingleton x₀ 1 (_ : x₀ ≠ 0)
φ : E →ₗ[ℝ] ℝ
hφ₁ : ∀ (x : { x // x ∈ f.domain }), ↑φ ↑x = ↑f x
hφ₂ : ∀ (x : E), ↑φ x ≤ gauge s x
⊢ ↑φ x₀ = 1
[PROOFSTEP]
rw [← f.domain.coe_mk x₀ (Submodule.mem_span_singleton_self _), hφ₁, LinearPMap.mkSpanSingleton'_apply_self]
[GOAL]
case refine_2.intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : TopologicalSpace E
inst✝³ : AddCommGroup E
inst✝² : TopologicalAddGroup E
inst✝¹ : Module ℝ E
inst✝ : ContinuousSMul ℝ E
s : Set E
hs₀ : 0 ∈ s
hs₁ : Convex ℝ s
hs₂ : IsOpen s
x₀ : E
hx₀ : ¬x₀ ∈ s
f : E →ₗ.[ℝ] ℝ := LinearPMap.mkSpanSingleton x₀ 1 (_ : x₀ ≠ 0)
φ : E →ₗ[ℝ] ℝ
hφ₁ : ∀ (x : { x // x ∈ f.domain }), ↑φ ↑x = ↑f x
hφ₂ : ∀ (x : E), ↑φ x ≤ gauge s x
hφ₃ : ↑φ x₀ = 1
⊢ ∃ f, ↑f x₀ = 1 ∧ ∀ (x : E), x ∈ s → ↑f x < 1
case refine_1
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : TopologicalSpace E
inst✝³ : AddCommGroup E
inst✝² : TopologicalAddGroup E
inst✝¹ : Module ℝ E
inst✝ : ContinuousSMul ℝ E
s : Set E
hs₀ : 0 ∈ s
hs₁ : Convex ℝ s
hs₂ : IsOpen s
x₀ : E
hx₀ : ¬x₀ ∈ s
f : E →ₗ.[ℝ] ℝ := LinearPMap.mkSpanSingleton x₀ 1 (_ : x₀ ≠ 0)
⊢ ∀ (x : { x // x ∈ f.domain }), ↑f x ≤ gauge s ↑x
[PROOFSTEP]
have hφ₄ : ∀ x ∈ s, φ x < 1 := fun x hx => (hφ₂ x).trans_lt (gauge_lt_one_of_mem_of_open hs₂ hx)
[GOAL]
case refine_2.intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : TopologicalSpace E
inst✝³ : AddCommGroup E
inst✝² : TopologicalAddGroup E
inst✝¹ : Module ℝ E
inst✝ : ContinuousSMul ℝ E
s : Set E
hs₀ : 0 ∈ s
hs₁ : Convex ℝ s
hs₂ : IsOpen s
x₀ : E
hx₀ : ¬x₀ ∈ s
f : E →ₗ.[ℝ] ℝ := LinearPMap.mkSpanSingleton x₀ 1 (_ : x₀ ≠ 0)
φ : E →ₗ[ℝ] ℝ
hφ₁ : ∀ (x : { x // x ∈ f.domain }), ↑φ ↑x = ↑f x
hφ₂ : ∀ (x : E), ↑φ x ≤ gauge s x
hφ₃ : ↑φ x₀ = 1
hφ₄ : ∀ (x : E), x ∈ s → ↑φ x < 1
⊢ ∃ f, ↑f x₀ = 1 ∧ ∀ (x : E), x ∈ s → ↑f x < 1
[PROOFSTEP]
refine' ⟨⟨φ, _⟩, hφ₃, hφ₄⟩
[GOAL]
case refine_2.intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : TopologicalSpace E
inst✝³ : AddCommGroup E
inst✝² : TopologicalAddGroup E
inst✝¹ : Module ℝ E
inst✝ : ContinuousSMul ℝ E
s : Set E
hs₀ : 0 ∈ s
hs₁ : Convex ℝ s
hs₂ : IsOpen s
x₀ : E
hx₀ : ¬x₀ ∈ s
f : E →ₗ.[ℝ] ℝ := LinearPMap.mkSpanSingleton x₀ 1 (_ : x₀ ≠ 0)
φ : E →ₗ[ℝ] ℝ
hφ₁ : ∀ (x : { x // x ∈ f.domain }), ↑φ ↑x = ↑f x
hφ₂ : ∀ (x : E), ↑φ x ≤ gauge s x
hφ₃ : ↑φ x₀ = 1
hφ₄ : ∀ (x : E), x ∈ s → ↑φ x < 1
⊢ Continuous φ.toFun
[PROOFSTEP]
refine'
  φ.continuous_of_nonzero_on_open _ (hs₂.vadd (-x₀)) (Nonempty.vadd_set ⟨0, hs₀⟩)
    (vadd_set_subset_iff.mpr fun x hx => _)
[GOAL]
case refine_2.intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : TopologicalSpace E
inst✝³ : AddCommGroup E
inst✝² : TopologicalAddGroup E
inst✝¹ : Module ℝ E
inst✝ : ContinuousSMul ℝ E
s : Set E
hs₀ : 0 ∈ s
hs₁ : Convex ℝ s
hs₂ : IsOpen s
x₀ : E
hx₀ : ¬x₀ ∈ s
f : E →ₗ.[ℝ] ℝ := LinearPMap.mkSpanSingleton x₀ 1 (_ : x₀ ≠ 0)
φ : E →ₗ[ℝ] ℝ
hφ₁ : ∀ (x : { x // x ∈ f.domain }), ↑φ ↑x = ↑f x
hφ₂ : ∀ (x : E), ↑φ x ≤ gauge s x
hφ₃ : ↑φ x₀ = 1
hφ₄ : ∀ (x : E), x ∈ s → ↑φ x < 1
x : E
hx : x ∈ s
⊢ -x₀ +ᵥ x ∈ fun x => ↑φ x = 0 → False
[PROOFSTEP]
change φ (-x₀ + x) ≠ 0
[GOAL]
case refine_2.intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : TopologicalSpace E
inst✝³ : AddCommGroup E
inst✝² : TopologicalAddGroup E
inst✝¹ : Module ℝ E
inst✝ : ContinuousSMul ℝ E
s : Set E
hs₀ : 0 ∈ s
hs₁ : Convex ℝ s
hs₂ : IsOpen s
x₀ : E
hx₀ : ¬x₀ ∈ s
f : E →ₗ.[ℝ] ℝ := LinearPMap.mkSpanSingleton x₀ 1 (_ : x₀ ≠ 0)
φ : E →ₗ[ℝ] ℝ
hφ₁ : ∀ (x : { x // x ∈ f.domain }), ↑φ ↑x = ↑f x
hφ₂ : ∀ (x : E), ↑φ x ≤ gauge s x
hφ₃ : ↑φ x₀ = 1
hφ₄ : ∀ (x : E), x ∈ s → ↑φ x < 1
x : E
hx : x ∈ s
⊢ ↑φ (-x₀ + x) ≠ 0
[PROOFSTEP]
rw [map_add, map_neg]
[GOAL]
case refine_2.intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : TopologicalSpace E
inst✝³ : AddCommGroup E
inst✝² : TopologicalAddGroup E
inst✝¹ : Module ℝ E
inst✝ : ContinuousSMul ℝ E
s : Set E
hs₀ : 0 ∈ s
hs₁ : Convex ℝ s
hs₂ : IsOpen s
x₀ : E
hx₀ : ¬x₀ ∈ s
f : E →ₗ.[ℝ] ℝ := LinearPMap.mkSpanSingleton x₀ 1 (_ : x₀ ≠ 0)
φ : E →ₗ[ℝ] ℝ
hφ₁ : ∀ (x : { x // x ∈ f.domain }), ↑φ ↑x = ↑f x
hφ₂ : ∀ (x : E), ↑φ x ≤ gauge s x
hφ₃ : ↑φ x₀ = 1
hφ₄ : ∀ (x : E), x ∈ s → ↑φ x < 1
x : E
hx : x ∈ s
⊢ -↑φ x₀ + ↑φ x ≠ 0
[PROOFSTEP]
specialize hφ₄ x hx
[GOAL]
case refine_2.intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : TopologicalSpace E
inst✝³ : AddCommGroup E
inst✝² : TopologicalAddGroup E
inst✝¹ : Module ℝ E
inst✝ : ContinuousSMul ℝ E
s : Set E
hs₀ : 0 ∈ s
hs₁ : Convex ℝ s
hs₂ : IsOpen s
x₀ : E
hx₀ : ¬x₀ ∈ s
f : E →ₗ.[ℝ] ℝ := LinearPMap.mkSpanSingleton x₀ 1 (_ : x₀ ≠ 0)
φ : E →ₗ[ℝ] ℝ
hφ₁ : ∀ (x : { x // x ∈ f.domain }), ↑φ ↑x = ↑f x
hφ₂ : ∀ (x : E), ↑φ x ≤ gauge s x
hφ₃ : ↑φ x₀ = 1
x : E
hx : x ∈ s
hφ₄ : ↑φ x < 1
⊢ -↑φ x₀ + ↑φ x ≠ 0
[PROOFSTEP]
linarith
[GOAL]
case refine_1
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : TopologicalSpace E
inst✝³ : AddCommGroup E
inst✝² : TopologicalAddGroup E
inst✝¹ : Module ℝ E
inst✝ : ContinuousSMul ℝ E
s : Set E
hs₀ : 0 ∈ s
hs₁ : Convex ℝ s
hs₂ : IsOpen s
x₀ : E
hx₀ : ¬x₀ ∈ s
f : E →ₗ.[ℝ] ℝ := LinearPMap.mkSpanSingleton x₀ 1 (_ : x₀ ≠ 0)
⊢ ∀ (x : { x // x ∈ f.domain }), ↑f x ≤ gauge s ↑x
[PROOFSTEP]
rintro ⟨x, hx⟩
[GOAL]
case refine_1.mk
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : TopologicalSpace E
inst✝³ : AddCommGroup E
inst✝² : TopologicalAddGroup E
inst✝¹ : Module ℝ E
inst✝ : ContinuousSMul ℝ E
s : Set E
hs₀ : 0 ∈ s
hs₁ : Convex ℝ s
hs₂ : IsOpen s
x₀ : E
hx₀ : ¬x₀ ∈ s
f : E →ₗ.[ℝ] ℝ := LinearPMap.mkSpanSingleton x₀ 1 (_ : x₀ ≠ 0)
x : E
hx : x ∈ f.domain
⊢ ↑f { val := x, property := hx } ≤ gauge s ↑{ val := x, property := hx }
[PROOFSTEP]
obtain ⟨y, rfl⟩ := Submodule.mem_span_singleton.1 hx
[GOAL]
case refine_1.mk.intro
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : TopologicalSpace E
inst✝³ : AddCommGroup E
inst✝² : TopologicalAddGroup E
inst✝¹ : Module ℝ E
inst✝ : ContinuousSMul ℝ E
s : Set E
hs₀ : 0 ∈ s
hs₁ : Convex ℝ s
hs₂ : IsOpen s
x₀ : E
hx₀ : ¬x₀ ∈ s
f : E →ₗ.[ℝ] ℝ := LinearPMap.mkSpanSingleton x₀ 1 (_ : x₀ ≠ 0)
y : ℝ
hx : y • x₀ ∈ f.domain
⊢ ↑f { val := y • x₀, property := hx } ≤ gauge s ↑{ val := y • x₀, property := hx }
[PROOFSTEP]
rw [LinearPMap.mkSpanSingleton'_apply]
[GOAL]
case refine_1.mk.intro
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : TopologicalSpace E
inst✝³ : AddCommGroup E
inst✝² : TopologicalAddGroup E
inst✝¹ : Module ℝ E
inst✝ : ContinuousSMul ℝ E
s : Set E
hs₀ : 0 ∈ s
hs₁ : Convex ℝ s
hs₂ : IsOpen s
x₀ : E
hx₀ : ¬x₀ ∈ s
f : E →ₗ.[ℝ] ℝ := LinearPMap.mkSpanSingleton x₀ 1 (_ : x₀ ≠ 0)
y : ℝ
hx : y • x₀ ∈ f.domain
⊢ y • 1 ≤ gauge s ↑{ val := y • x₀, property := hx }
[PROOFSTEP]
simp only [mul_one, Algebra.id.smul_eq_mul, Submodule.coe_mk]
[GOAL]
case refine_1.mk.intro
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : TopologicalSpace E
inst✝³ : AddCommGroup E
inst✝² : TopologicalAddGroup E
inst✝¹ : Module ℝ E
inst✝ : ContinuousSMul ℝ E
s : Set E
hs₀ : 0 ∈ s
hs₁ : Convex ℝ s
hs₂ : IsOpen s
x₀ : E
hx₀ : ¬x₀ ∈ s
f : E →ₗ.[ℝ] ℝ := LinearPMap.mkSpanSingleton x₀ 1 (_ : x₀ ≠ 0)
y : ℝ
hx : y • x₀ ∈ f.domain
⊢ y ≤ gauge s (y • x₀)
[PROOFSTEP]
obtain h | h := le_or_lt y 0
[GOAL]
case refine_1.mk.intro.inl
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : TopologicalSpace E
inst✝³ : AddCommGroup E
inst✝² : TopologicalAddGroup E
inst✝¹ : Module ℝ E
inst✝ : ContinuousSMul ℝ E
s : Set E
hs₀ : 0 ∈ s
hs₁ : Convex ℝ s
hs₂ : IsOpen s
x₀ : E
hx₀ : ¬x₀ ∈ s
f : E →ₗ.[ℝ] ℝ := LinearPMap.mkSpanSingleton x₀ 1 (_ : x₀ ≠ 0)
y : ℝ
hx : y • x₀ ∈ f.domain
h : y ≤ 0
⊢ y ≤ gauge s (y • x₀)
[PROOFSTEP]
exact h.trans (gauge_nonneg _)
[GOAL]
case refine_1.mk.intro.inr
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : TopologicalSpace E
inst✝³ : AddCommGroup E
inst✝² : TopologicalAddGroup E
inst✝¹ : Module ℝ E
inst✝ : ContinuousSMul ℝ E
s : Set E
hs₀ : 0 ∈ s
hs₁ : Convex ℝ s
hs₂ : IsOpen s
x₀ : E
hx₀ : ¬x₀ ∈ s
f : E →ₗ.[ℝ] ℝ := LinearPMap.mkSpanSingleton x₀ 1 (_ : x₀ ≠ 0)
y : ℝ
hx : y • x₀ ∈ f.domain
h : 0 < y
⊢ y ≤ gauge s (y • x₀)
[PROOFSTEP]
rw [gauge_smul_of_nonneg h.le, smul_eq_mul, le_mul_iff_one_le_right h]
[GOAL]
case refine_1.mk.intro.inr
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : TopologicalSpace E
inst✝³ : AddCommGroup E
inst✝² : TopologicalAddGroup E
inst✝¹ : Module ℝ E
inst✝ : ContinuousSMul ℝ E
s : Set E
hs₀ : 0 ∈ s
hs₁ : Convex ℝ s
hs₂ : IsOpen s
x₀ : E
hx₀ : ¬x₀ ∈ s
f : E →ₗ.[ℝ] ℝ := LinearPMap.mkSpanSingleton x₀ 1 (_ : x₀ ≠ 0)
y : ℝ
hx : y • x₀ ∈ f.domain
h : 0 < y
⊢ 1 ≤ gauge s x₀
[PROOFSTEP]
exact one_le_gauge_of_not_mem (hs₁.starConvex hs₀) (absorbent_nhds_zero <| hs₂.mem_nhds hs₀).absorbs hx₀
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : TopologicalSpace E
inst✝³ : AddCommGroup E
inst✝² : TopologicalAddGroup E
inst✝¹ : Module ℝ E
inst✝ : ContinuousSMul ℝ E
s t : Set E
x y : E
hs₁ : Convex ℝ s
hs₂ : IsOpen s
ht : Convex ℝ t
disj : Disjoint s t
⊢ ∃ f u, (∀ (a : E), a ∈ s → ↑f a < u) ∧ ∀ (b : E), b ∈ t → u ≤ ↑f b
[PROOFSTEP]
obtain rfl | ⟨a₀, ha₀⟩ := s.eq_empty_or_nonempty
[GOAL]
case inl
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : TopologicalSpace E
inst✝³ : AddCommGroup E
inst✝² : TopologicalAddGroup E
inst✝¹ : Module ℝ E
inst✝ : ContinuousSMul ℝ E
t : Set E
x y : E
ht : Convex ℝ t
hs₁ : Convex ℝ ∅
hs₂ : IsOpen ∅
disj : Disjoint ∅ t
⊢ ∃ f u, (∀ (a : E), a ∈ ∅ → ↑f a < u) ∧ ∀ (b : E), b ∈ t → u ≤ ↑f b
[PROOFSTEP]
exact ⟨0, 0, by simp, fun b _hb => le_rfl⟩
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : TopologicalSpace E
inst✝³ : AddCommGroup E
inst✝² : TopologicalAddGroup E
inst✝¹ : Module ℝ E
inst✝ : ContinuousSMul ℝ E
t : Set E
x y : E
ht : Convex ℝ t
hs₁ : Convex ℝ ∅
hs₂ : IsOpen ∅
disj : Disjoint ∅ t
⊢ ∀ (a : E), a ∈ ∅ → ↑0 a < 0
[PROOFSTEP]
simp
[GOAL]
case inr.intro
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : TopologicalSpace E
inst✝³ : AddCommGroup E
inst✝² : TopologicalAddGroup E
inst✝¹ : Module ℝ E
inst✝ : ContinuousSMul ℝ E
s t : Set E
x y : E
hs₁ : Convex ℝ s
hs₂ : IsOpen s
ht : Convex ℝ t
disj : Disjoint s t
a₀ : E
ha₀ : a₀ ∈ s
⊢ ∃ f u, (∀ (a : E), a ∈ s → ↑f a < u) ∧ ∀ (b : E), b ∈ t → u ≤ ↑f b
[PROOFSTEP]
obtain rfl | ⟨b₀, hb₀⟩ := t.eq_empty_or_nonempty
[GOAL]
case inr.intro.inl
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : TopologicalSpace E
inst✝³ : AddCommGroup E
inst✝² : TopologicalAddGroup E
inst✝¹ : Module ℝ E
inst✝ : ContinuousSMul ℝ E
s : Set E
x y : E
hs₁ : Convex ℝ s
hs₂ : IsOpen s
a₀ : E
ha₀ : a₀ ∈ s
ht : Convex ℝ ∅
disj : Disjoint s ∅
⊢ ∃ f u, (∀ (a : E), a ∈ s → ↑f a < u) ∧ ∀ (b : E), b ∈ ∅ → u ≤ ↑f b
[PROOFSTEP]
exact ⟨0, 1, fun a _ha => zero_lt_one, by simp⟩
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : TopologicalSpace E
inst✝³ : AddCommGroup E
inst✝² : TopologicalAddGroup E
inst✝¹ : Module ℝ E
inst✝ : ContinuousSMul ℝ E
s : Set E
x y : E
hs₁ : Convex ℝ s
hs₂ : IsOpen s
a₀ : E
ha₀ : a₀ ∈ s
ht : Convex ℝ ∅
disj : Disjoint s ∅
⊢ ∀ (b : E), b ∈ ∅ → 1 ≤ ↑0 b
[PROOFSTEP]
simp
[GOAL]
case inr.intro.inr.intro
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : TopologicalSpace E
inst✝³ : AddCommGroup E
inst✝² : TopologicalAddGroup E
inst✝¹ : Module ℝ E
inst✝ : ContinuousSMul ℝ E
s t : Set E
x y : E
hs₁ : Convex ℝ s
hs₂ : IsOpen s
ht : Convex ℝ t
disj : Disjoint s t
a₀ : E
ha₀ : a₀ ∈ s
b₀ : E
hb₀ : b₀ ∈ t
⊢ ∃ f u, (∀ (a : E), a ∈ s → ↑f a < u) ∧ ∀ (b : E), b ∈ t → u ≤ ↑f b
[PROOFSTEP]
let x₀ := b₀ - a₀
[GOAL]
case inr.intro.inr.intro
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : TopologicalSpace E
inst✝³ : AddCommGroup E
inst✝² : TopologicalAddGroup E
inst✝¹ : Module ℝ E
inst✝ : ContinuousSMul ℝ E
s t : Set E
x y : E
hs₁ : Convex ℝ s
hs₂ : IsOpen s
ht : Convex ℝ t
disj : Disjoint s t
a₀ : E
ha₀ : a₀ ∈ s
b₀ : E
hb₀ : b₀ ∈ t
x₀ : E := b₀ - a₀
⊢ ∃ f u, (∀ (a : E), a ∈ s → ↑f a < u) ∧ ∀ (b : E), b ∈ t → u ≤ ↑f b
[PROOFSTEP]
let C := x₀ +ᵥ (s - t)
[GOAL]
case inr.intro.inr.intro
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : TopologicalSpace E
inst✝³ : AddCommGroup E
inst✝² : TopologicalAddGroup E
inst✝¹ : Module ℝ E
inst✝ : ContinuousSMul ℝ E
s t : Set E
x y : E
hs₁ : Convex ℝ s
hs₂ : IsOpen s
ht : Convex ℝ t
disj : Disjoint s t
a₀ : E
ha₀ : a₀ ∈ s
b₀ : E
hb₀ : b₀ ∈ t
x₀ : E := b₀ - a₀
C : Set E := x₀ +ᵥ (s - t)
⊢ ∃ f u, (∀ (a : E), a ∈ s → ↑f a < u) ∧ ∀ (b : E), b ∈ t → u ≤ ↑f b
[PROOFSTEP]
have : (0 : E) ∈ C := ⟨a₀ - b₀, sub_mem_sub ha₀ hb₀, by simp_rw [vadd_eq_add, sub_add_sub_cancel', sub_self]⟩
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : TopologicalSpace E
inst✝³ : AddCommGroup E
inst✝² : TopologicalAddGroup E
inst✝¹ : Module ℝ E
inst✝ : ContinuousSMul ℝ E
s t : Set E
x y : E
hs₁ : Convex ℝ s
hs₂ : IsOpen s
ht : Convex ℝ t
disj : Disjoint s t
a₀ : E
ha₀ : a₀ ∈ s
b₀ : E
hb₀ : b₀ ∈ t
x₀ : E := b₀ - a₀
C : Set E := x₀ +ᵥ (s - t)
⊢ (fun x => x₀ +ᵥ x) (a₀ - b₀) = 0
[PROOFSTEP]
simp_rw [vadd_eq_add, sub_add_sub_cancel', sub_self]
[GOAL]
case inr.intro.inr.intro
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : TopologicalSpace E
inst✝³ : AddCommGroup E
inst✝² : TopologicalAddGroup E
inst✝¹ : Module ℝ E
inst✝ : ContinuousSMul ℝ E
s t : Set E
x y : E
hs₁ : Convex ℝ s
hs₂ : IsOpen s
ht : Convex ℝ t
disj : Disjoint s t
a₀ : E
ha₀ : a₀ ∈ s
b₀ : E
hb₀ : b₀ ∈ t
x₀ : E := b₀ - a₀
C : Set E := x₀ +ᵥ (s - t)
this : 0 ∈ C
⊢ ∃ f u, (∀ (a : E), a ∈ s → ↑f a < u) ∧ ∀ (b : E), b ∈ t → u ≤ ↑f b
[PROOFSTEP]
have : Convex ℝ C := (hs₁.sub ht).vadd _
[GOAL]
case inr.intro.inr.intro
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : TopologicalSpace E
inst✝³ : AddCommGroup E
inst✝² : TopologicalAddGroup E
inst✝¹ : Module ℝ E
inst✝ : ContinuousSMul ℝ E
s t : Set E
x y : E
hs₁ : Convex ℝ s
hs₂ : IsOpen s
ht : Convex ℝ t
disj : Disjoint s t
a₀ : E
ha₀ : a₀ ∈ s
b₀ : E
hb₀ : b₀ ∈ t
x₀ : E := b₀ - a₀
C : Set E := x₀ +ᵥ (s - t)
this✝ : 0 ∈ C
this : Convex ℝ C
⊢ ∃ f u, (∀ (a : E), a ∈ s → ↑f a < u) ∧ ∀ (b : E), b ∈ t → u ≤ ↑f b
[PROOFSTEP]
have : x₀ ∉ C := by
  intro hx₀
  rw [← add_zero x₀] at hx₀
  exact disj.zero_not_mem_sub_set (vadd_mem_vadd_set_iff.1 hx₀)
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : TopologicalSpace E
inst✝³ : AddCommGroup E
inst✝² : TopologicalAddGroup E
inst✝¹ : Module ℝ E
inst✝ : ContinuousSMul ℝ E
s t : Set E
x y : E
hs₁ : Convex ℝ s
hs₂ : IsOpen s
ht : Convex ℝ t
disj : Disjoint s t
a₀ : E
ha₀ : a₀ ∈ s
b₀ : E
hb₀ : b₀ ∈ t
x₀ : E := b₀ - a₀
C : Set E := x₀ +ᵥ (s - t)
this✝ : 0 ∈ C
this : Convex ℝ C
⊢ ¬x₀ ∈ C
[PROOFSTEP]
intro hx₀
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : TopologicalSpace E
inst✝³ : AddCommGroup E
inst✝² : TopologicalAddGroup E
inst✝¹ : Module ℝ E
inst✝ : ContinuousSMul ℝ E
s t : Set E
x y : E
hs₁ : Convex ℝ s
hs₂ : IsOpen s
ht : Convex ℝ t
disj : Disjoint s t
a₀ : E
ha₀ : a₀ ∈ s
b₀ : E
hb₀ : b₀ ∈ t
x₀ : E := b₀ - a₀
C : Set E := x₀ +ᵥ (s - t)
this✝ : 0 ∈ C
this : Convex ℝ C
hx₀ : x₀ ∈ C
⊢ False
[PROOFSTEP]
rw [← add_zero x₀] at hx₀
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : TopologicalSpace E
inst✝³ : AddCommGroup E
inst✝² : TopologicalAddGroup E
inst✝¹ : Module ℝ E
inst✝ : ContinuousSMul ℝ E
s t : Set E
x y : E
hs₁ : Convex ℝ s
hs₂ : IsOpen s
ht : Convex ℝ t
disj : Disjoint s t
a₀ : E
ha₀ : a₀ ∈ s
b₀ : E
hb₀ : b₀ ∈ t
x₀ : E := b₀ - a₀
C : Set E := x₀ +ᵥ (s - t)
this✝ : 0 ∈ C
this : Convex ℝ C
hx₀ : x₀ + 0 ∈ C
⊢ False
[PROOFSTEP]
exact disj.zero_not_mem_sub_set (vadd_mem_vadd_set_iff.1 hx₀)
[GOAL]
case inr.intro.inr.intro
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : TopologicalSpace E
inst✝³ : AddCommGroup E
inst✝² : TopologicalAddGroup E
inst✝¹ : Module ℝ E
inst✝ : ContinuousSMul ℝ E
s t : Set E
x y : E
hs₁ : Convex ℝ s
hs₂ : IsOpen s
ht : Convex ℝ t
disj : Disjoint s t
a₀ : E
ha₀ : a₀ ∈ s
b₀ : E
hb₀ : b₀ ∈ t
x₀ : E := b₀ - a₀
C : Set E := x₀ +ᵥ (s - t)
this✝¹ : 0 ∈ C
this✝ : Convex ℝ C
this : ¬x₀ ∈ C
⊢ ∃ f u, (∀ (a : E), a ∈ s → ↑f a < u) ∧ ∀ (b : E), b ∈ t → u ≤ ↑f b
[PROOFSTEP]
obtain ⟨f, hf₁, hf₂⟩ := separate_convex_open_set ‹0 ∈ C› ‹_› (hs₂.sub_right.vadd _) ‹x₀ ∉ C›
[GOAL]
case inr.intro.inr.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : TopologicalSpace E
inst✝³ : AddCommGroup E
inst✝² : TopologicalAddGroup E
inst✝¹ : Module ℝ E
inst✝ : ContinuousSMul ℝ E
s t : Set E
x y : E
hs₁ : Convex ℝ s
hs₂ : IsOpen s
ht : Convex ℝ t
disj : Disjoint s t
a₀ : E
ha₀ : a₀ ∈ s
b₀ : E
hb₀ : b₀ ∈ t
x₀ : E := b₀ - a₀
C : Set E := x₀ +ᵥ (s - t)
this✝¹ : 0 ∈ C
this✝ : Convex ℝ C
this : ¬x₀ ∈ C
f : E →L[ℝ] ℝ
hf₁ : ↑f x₀ = 1
hf₂ : ∀ (x : E), x ∈ C → ↑f x < 1
⊢ ∃ f u, (∀ (a : E), a ∈ s → ↑f a < u) ∧ ∀ (b : E), b ∈ t → u ≤ ↑f b
[PROOFSTEP]
have : f b₀ = f a₀ + 1 := by simp [← hf₁]
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : TopologicalSpace E
inst✝³ : AddCommGroup E
inst✝² : TopologicalAddGroup E
inst✝¹ : Module ℝ E
inst✝ : ContinuousSMul ℝ E
s t : Set E
x y : E
hs₁ : Convex ℝ s
hs₂ : IsOpen s
ht : Convex ℝ t
disj : Disjoint s t
a₀ : E
ha₀ : a₀ ∈ s
b₀ : E
hb₀ : b₀ ∈ t
x₀ : E := b₀ - a₀
C : Set E := x₀ +ᵥ (s - t)
this✝¹ : 0 ∈ C
this✝ : Convex ℝ C
this : ¬x₀ ∈ C
f : E →L[ℝ] ℝ
hf₁ : ↑f x₀ = 1
hf₂ : ∀ (x : E), x ∈ C → ↑f x < 1
⊢ ↑f b₀ = ↑f a₀ + 1
[PROOFSTEP]
simp [← hf₁]
[GOAL]
case inr.intro.inr.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : TopologicalSpace E
inst✝³ : AddCommGroup E
inst✝² : TopologicalAddGroup E
inst✝¹ : Module ℝ E
inst✝ : ContinuousSMul ℝ E
s t : Set E
x y : E
hs₁ : Convex ℝ s
hs₂ : IsOpen s
ht : Convex ℝ t
disj : Disjoint s t
a₀ : E
ha₀ : a₀ ∈ s
b₀ : E
hb₀ : b₀ ∈ t
x₀ : E := b₀ - a₀
C : Set E := x₀ +ᵥ (s - t)
this✝² : 0 ∈ C
this✝¹ : Convex ℝ C
this✝ : ¬x₀ ∈ C
f : E →L[ℝ] ℝ
hf₁ : ↑f x₀ = 1
hf₂ : ∀ (x : E), x ∈ C → ↑f x < 1
this : ↑f b₀ = ↑f a₀ + 1
⊢ ∃ f u, (∀ (a : E), a ∈ s → ↑f a < u) ∧ ∀ (b : E), b ∈ t → u ≤ ↑f b
[PROOFSTEP]
have forall_le : ∀ a ∈ s, ∀ b ∈ t, f a ≤ f b := by
  intro a ha b hb
  have := hf₂ (x₀ + (a - b)) (vadd_mem_vadd_set <| sub_mem_sub ha hb)
  simp only [f.map_add, f.map_sub, hf₁] at this
  linarith
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : TopologicalSpace E
inst✝³ : AddCommGroup E
inst✝² : TopologicalAddGroup E
inst✝¹ : Module ℝ E
inst✝ : ContinuousSMul ℝ E
s t : Set E
x y : E
hs₁ : Convex ℝ s
hs₂ : IsOpen s
ht : Convex ℝ t
disj : Disjoint s t
a₀ : E
ha₀ : a₀ ∈ s
b₀ : E
hb₀ : b₀ ∈ t
x₀ : E := b₀ - a₀
C : Set E := x₀ +ᵥ (s - t)
this✝² : 0 ∈ C
this✝¹ : Convex ℝ C
this✝ : ¬x₀ ∈ C
f : E →L[ℝ] ℝ
hf₁ : ↑f x₀ = 1
hf₂ : ∀ (x : E), x ∈ C → ↑f x < 1
this : ↑f b₀ = ↑f a₀ + 1
⊢ ∀ (a : E), a ∈ s → ∀ (b : E), b ∈ t → ↑f a ≤ ↑f b
[PROOFSTEP]
intro a ha b hb
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : TopologicalSpace E
inst✝³ : AddCommGroup E
inst✝² : TopologicalAddGroup E
inst✝¹ : Module ℝ E
inst✝ : ContinuousSMul ℝ E
s t : Set E
x y : E
hs₁ : Convex ℝ s
hs₂ : IsOpen s
ht : Convex ℝ t
disj : Disjoint s t
a₀ : E
ha₀ : a₀ ∈ s
b₀ : E
hb₀ : b₀ ∈ t
x₀ : E := b₀ - a₀
C : Set E := x₀ +ᵥ (s - t)
this✝² : 0 ∈ C
this✝¹ : Convex ℝ C
this✝ : ¬x₀ ∈ C
f : E →L[ℝ] ℝ
hf₁ : ↑f x₀ = 1
hf₂ : ∀ (x : E), x ∈ C → ↑f x < 1
this : ↑f b₀ = ↑f a₀ + 1
a : E
ha : a ∈ s
b : E
hb : b ∈ t
⊢ ↑f a ≤ ↑f b
[PROOFSTEP]
have := hf₂ (x₀ + (a - b)) (vadd_mem_vadd_set <| sub_mem_sub ha hb)
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : TopologicalSpace E
inst✝³ : AddCommGroup E
inst✝² : TopologicalAddGroup E
inst✝¹ : Module ℝ E
inst✝ : ContinuousSMul ℝ E
s t : Set E
x y : E
hs₁ : Convex ℝ s
hs₂ : IsOpen s
ht : Convex ℝ t
disj : Disjoint s t
a₀ : E
ha₀ : a₀ ∈ s
b₀ : E
hb₀ : b₀ ∈ t
x₀ : E := b₀ - a₀
C : Set E := x₀ +ᵥ (s - t)
this✝³ : 0 ∈ C
this✝² : Convex ℝ C
this✝¹ : ¬x₀ ∈ C
f : E →L[ℝ] ℝ
hf₁ : ↑f x₀ = 1
hf₂ : ∀ (x : E), x ∈ C → ↑f x < 1
this✝ : ↑f b₀ = ↑f a₀ + 1
a : E
ha : a ∈ s
b : E
hb : b ∈ t
this : ↑f (x₀ + (a - b)) < 1
⊢ ↑f a ≤ ↑f b
[PROOFSTEP]
simp only [f.map_add, f.map_sub, hf₁] at this
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : TopologicalSpace E
inst✝³ : AddCommGroup E
inst✝² : TopologicalAddGroup E
inst✝¹ : Module ℝ E
inst✝ : ContinuousSMul ℝ E
s t : Set E
x y : E
hs₁ : Convex ℝ s
hs₂ : IsOpen s
ht : Convex ℝ t
disj : Disjoint s t
a₀ : E
ha₀ : a₀ ∈ s
b₀ : E
hb₀ : b₀ ∈ t
x₀ : E := b₀ - a₀
C : Set E := x₀ +ᵥ (s - t)
this✝³ : 0 ∈ C
this✝² : Convex ℝ C
this✝¹ : ¬x₀ ∈ C
f : E →L[ℝ] ℝ
hf₁ : ↑f x₀ = 1
hf₂ : ∀ (x : E), x ∈ C → ↑f x < 1
this✝ : ↑f b₀ = ↑f a₀ + 1
a : E
ha : a ∈ s
b : E
hb : b ∈ t
this : ↑f b₀ - ↑f a₀ + (↑f a - ↑f b) < 1
⊢ ↑f a ≤ ↑f b
[PROOFSTEP]
linarith
[GOAL]
case inr.intro.inr.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : TopologicalSpace E
inst✝³ : AddCommGroup E
inst✝² : TopologicalAddGroup E
inst✝¹ : Module ℝ E
inst✝ : ContinuousSMul ℝ E
s t : Set E
x y : E
hs₁ : Convex ℝ s
hs₂ : IsOpen s
ht : Convex ℝ t
disj : Disjoint s t
a₀ : E
ha₀ : a₀ ∈ s
b₀ : E
hb₀ : b₀ ∈ t
x₀ : E := b₀ - a₀
C : Set E := x₀ +ᵥ (s - t)
this✝² : 0 ∈ C
this✝¹ : Convex ℝ C
this✝ : ¬x₀ ∈ C
f : E →L[ℝ] ℝ
hf₁ : ↑f x₀ = 1
hf₂ : ∀ (x : E), x ∈ C → ↑f x < 1
this : ↑f b₀ = ↑f a₀ + 1
forall_le : ∀ (a : E), a ∈ s → ∀ (b : E), b ∈ t → ↑f a ≤ ↑f b
⊢ ∃ f u, (∀ (a : E), a ∈ s → ↑f a < u) ∧ ∀ (b : E), b ∈ t → u ≤ ↑f b
[PROOFSTEP]
refine' ⟨f, sInf (f '' t), image_subset_iff.1 (_ : f '' s ⊆ Iio (sInf (f '' t))), fun b hb => _⟩
[GOAL]
case inr.intro.inr.intro.intro.intro.refine'_1
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : TopologicalSpace E
inst✝³ : AddCommGroup E
inst✝² : TopologicalAddGroup E
inst✝¹ : Module ℝ E
inst✝ : ContinuousSMul ℝ E
s t : Set E
x y : E
hs₁ : Convex ℝ s
hs₂ : IsOpen s
ht : Convex ℝ t
disj : Disjoint s t
a₀ : E
ha₀ : a₀ ∈ s
b₀ : E
hb₀ : b₀ ∈ t
x₀ : E := b₀ - a₀
C : Set E := x₀ +ᵥ (s - t)
this✝² : 0 ∈ C
this✝¹ : Convex ℝ C
this✝ : ¬x₀ ∈ C
f : E →L[ℝ] ℝ
hf₁ : ↑f x₀ = 1
hf₂ : ∀ (x : E), x ∈ C → ↑f x < 1
this : ↑f b₀ = ↑f a₀ + 1
forall_le : ∀ (a : E), a ∈ s → ∀ (b : E), b ∈ t → ↑f a ≤ ↑f b
⊢ ↑f '' s ⊆ Iio (sInf (↑f '' t))
[PROOFSTEP]
rw [← interior_Iic]
[GOAL]
case inr.intro.inr.intro.intro.intro.refine'_1
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : TopologicalSpace E
inst✝³ : AddCommGroup E
inst✝² : TopologicalAddGroup E
inst✝¹ : Module ℝ E
inst✝ : ContinuousSMul ℝ E
s t : Set E
x y : E
hs₁ : Convex ℝ s
hs₂ : IsOpen s
ht : Convex ℝ t
disj : Disjoint s t
a₀ : E
ha₀ : a₀ ∈ s
b₀ : E
hb₀ : b₀ ∈ t
x₀ : E := b₀ - a₀
C : Set E := x₀ +ᵥ (s - t)
this✝² : 0 ∈ C
this✝¹ : Convex ℝ C
this✝ : ¬x₀ ∈ C
f : E →L[ℝ] ℝ
hf₁ : ↑f x₀ = 1
hf₂ : ∀ (x : E), x ∈ C → ↑f x < 1
this : ↑f b₀ = ↑f a₀ + 1
forall_le : ∀ (a : E), a ∈ s → ∀ (b : E), b ∈ t → ↑f a ≤ ↑f b
⊢ ↑f '' s ⊆ interior (Iic (sInf (↑f '' t)))
[PROOFSTEP]
refine' interior_maximal (image_subset_iff.2 fun a ha => _) (f.isOpenMap_of_ne_zero _ _ hs₂)
[GOAL]
case inr.intro.inr.intro.intro.intro.refine'_1.refine'_1
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : TopologicalSpace E
inst✝³ : AddCommGroup E
inst✝² : TopologicalAddGroup E
inst✝¹ : Module ℝ E
inst✝ : ContinuousSMul ℝ E
s t : Set E
x y : E
hs₁ : Convex ℝ s
hs₂ : IsOpen s
ht : Convex ℝ t
disj : Disjoint s t
a₀ : E
ha₀ : a₀ ∈ s
b₀ : E
hb₀ : b₀ ∈ t
x₀ : E := b₀ - a₀
C : Set E := x₀ +ᵥ (s - t)
this✝² : 0 ∈ C
this✝¹ : Convex ℝ C
this✝ : ¬x₀ ∈ C
f : E →L[ℝ] ℝ
hf₁ : ↑f x₀ = 1
hf₂ : ∀ (x : E), x ∈ C → ↑f x < 1
this : ↑f b₀ = ↑f a₀ + 1
forall_le : ∀ (a : E), a ∈ s → ∀ (b : E), b ∈ t → ↑f a ≤ ↑f b
a : E
ha : a ∈ s
⊢ a ∈ ↑f ⁻¹' Iic (sInf (↑f '' t))
[PROOFSTEP]
exact le_csInf (Nonempty.image _ ⟨_, hb₀⟩) (ball_image_of_ball <| forall_le _ ha)
[GOAL]
case inr.intro.inr.intro.intro.intro.refine'_1.refine'_2
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : TopologicalSpace E
inst✝³ : AddCommGroup E
inst✝² : TopologicalAddGroup E
inst✝¹ : Module ℝ E
inst✝ : ContinuousSMul ℝ E
s t : Set E
x y : E
hs₁ : Convex ℝ s
hs₂ : IsOpen s
ht : Convex ℝ t
disj : Disjoint s t
a₀ : E
ha₀ : a₀ ∈ s
b₀ : E
hb₀ : b₀ ∈ t
x₀ : E := b₀ - a₀
C : Set E := x₀ +ᵥ (s - t)
this✝² : 0 ∈ C
this✝¹ : Convex ℝ C
this✝ : ¬x₀ ∈ C
f : E →L[ℝ] ℝ
hf₁ : ↑f x₀ = 1
hf₂ : ∀ (x : E), x ∈ C → ↑f x < 1
this : ↑f b₀ = ↑f a₀ + 1
forall_le : ∀ (a : E), a ∈ s → ∀ (b : E), b ∈ t → ↑f a ≤ ↑f b
⊢ f ≠ 0
[PROOFSTEP]
rintro rfl
[GOAL]
case inr.intro.inr.intro.intro.intro.refine'_1.refine'_2
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : TopologicalSpace E
inst✝³ : AddCommGroup E
inst✝² : TopologicalAddGroup E
inst✝¹ : Module ℝ E
inst✝ : ContinuousSMul ℝ E
s t : Set E
x y : E
hs₁ : Convex ℝ s
hs₂ : IsOpen s
ht : Convex ℝ t
disj : Disjoint s t
a₀ : E
ha₀ : a₀ ∈ s
b₀ : E
hb₀ : b₀ ∈ t
x₀ : E := b₀ - a₀
C : Set E := x₀ +ᵥ (s - t)
this✝² : 0 ∈ C
this✝¹ : Convex ℝ C
this✝ : ¬x₀ ∈ C
hf₁ : ↑0 x₀ = 1
hf₂ : ∀ (x : E), x ∈ C → ↑0 x < 1
this : ↑0 b₀ = ↑0 a₀ + 1
forall_le : ∀ (a : E), a ∈ s → ∀ (b : E), b ∈ t → ↑0 a ≤ ↑0 b
⊢ False
[PROOFSTEP]
simp at hf₁
[GOAL]
case inr.intro.inr.intro.intro.intro.refine'_2
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : TopologicalSpace E
inst✝³ : AddCommGroup E
inst✝² : TopologicalAddGroup E
inst✝¹ : Module ℝ E
inst✝ : ContinuousSMul ℝ E
s t : Set E
x y : E
hs₁ : Convex ℝ s
hs₂ : IsOpen s
ht : Convex ℝ t
disj : Disjoint s t
a₀ : E
ha₀ : a₀ ∈ s
b₀ : E
hb₀ : b₀ ∈ t
x₀ : E := b₀ - a₀
C : Set E := x₀ +ᵥ (s - t)
this✝² : 0 ∈ C
this✝¹ : Convex ℝ C
this✝ : ¬x₀ ∈ C
f : E →L[ℝ] ℝ
hf₁ : ↑f x₀ = 1
hf₂ : ∀ (x : E), x ∈ C → ↑f x < 1
this : ↑f b₀ = ↑f a₀ + 1
forall_le : ∀ (a : E), a ∈ s → ∀ (b : E), b ∈ t → ↑f a ≤ ↑f b
b : E
hb : b ∈ t
⊢ sInf (↑f '' t) ≤ ↑f b
[PROOFSTEP]
exact csInf_le ⟨f a₀, ball_image_of_ball <| forall_le _ ha₀⟩ (mem_image_of_mem _ hb)
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : TopologicalSpace E
inst✝³ : AddCommGroup E
inst✝² : TopologicalAddGroup E
inst✝¹ : Module ℝ E
inst✝ : ContinuousSMul ℝ E
s t : Set E
x y : E
ht₁ : Convex ℝ t
ht₂ : IsOpen t
disj : ¬x ∈ t
f : E →L[ℝ] ℝ
hf : ∀ (a : E), a ∈ t → ↑f a < ↑f x
⊢ ∀ (b : E), b ∈ t → ↑(-f) x < ↑(-f) b
[PROOFSTEP]
simpa
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : TopologicalSpace E
inst✝³ : AddCommGroup E
inst✝² : TopologicalAddGroup E
inst✝¹ : Module ℝ E
inst✝ : ContinuousSMul ℝ E
s t : Set E
x y : E
hs₁ : Convex ℝ s
hs₂ : IsOpen s
ht₁ : Convex ℝ t
ht₃ : IsOpen t
disj : Disjoint s t
⊢ ∃ f u, (∀ (a : E), a ∈ s → ↑f a < u) ∧ ∀ (b : E), b ∈ t → u < ↑f b
[PROOFSTEP]
obtain rfl | ⟨a₀, ha₀⟩ := s.eq_empty_or_nonempty
[GOAL]
case inl
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : TopologicalSpace E
inst✝³ : AddCommGroup E
inst✝² : TopologicalAddGroup E
inst✝¹ : Module ℝ E
inst✝ : ContinuousSMul ℝ E
t : Set E
x y : E
ht₁ : Convex ℝ t
ht₃ : IsOpen t
hs₁ : Convex ℝ ∅
hs₂ : IsOpen ∅
disj : Disjoint ∅ t
⊢ ∃ f u, (∀ (a : E), a ∈ ∅ → ↑f a < u) ∧ ∀ (b : E), b ∈ t → u < ↑f b
[PROOFSTEP]
exact ⟨0, -1, by simp, fun b _hb => by norm_num⟩
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : TopologicalSpace E
inst✝³ : AddCommGroup E
inst✝² : TopologicalAddGroup E
inst✝¹ : Module ℝ E
inst✝ : ContinuousSMul ℝ E
t : Set E
x y : E
ht₁ : Convex ℝ t
ht₃ : IsOpen t
hs₁ : Convex ℝ ∅
hs₂ : IsOpen ∅
disj : Disjoint ∅ t
⊢ ∀ (a : E), a ∈ ∅ → ↑0 a < -1
[PROOFSTEP]
simp
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : TopologicalSpace E
inst✝³ : AddCommGroup E
inst✝² : TopologicalAddGroup E
inst✝¹ : Module ℝ E
inst✝ : ContinuousSMul ℝ E
t : Set E
x y : E
ht₁ : Convex ℝ t
ht₃ : IsOpen t
hs₁ : Convex ℝ ∅
hs₂ : IsOpen ∅
disj : Disjoint ∅ t
b : E
_hb : b ∈ t
⊢ -1 < ↑0 b
[PROOFSTEP]
norm_num
[GOAL]
case inr.intro
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : TopologicalSpace E
inst✝³ : AddCommGroup E
inst✝² : TopologicalAddGroup E
inst✝¹ : Module ℝ E
inst✝ : ContinuousSMul ℝ E
s t : Set E
x y : E
hs₁ : Convex ℝ s
hs₂ : IsOpen s
ht₁ : Convex ℝ t
ht₃ : IsOpen t
disj : Disjoint s t
a₀ : E
ha₀ : a₀ ∈ s
⊢ ∃ f u, (∀ (a : E), a ∈ s → ↑f a < u) ∧ ∀ (b : E), b ∈ t → u < ↑f b
[PROOFSTEP]
obtain rfl | ⟨b₀, hb₀⟩ := t.eq_empty_or_nonempty
[GOAL]
case inr.intro.inl
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : TopologicalSpace E
inst✝³ : AddCommGroup E
inst✝² : TopologicalAddGroup E
inst✝¹ : Module ℝ E
inst✝ : ContinuousSMul ℝ E
s : Set E
x y : E
hs₁ : Convex ℝ s
hs₂ : IsOpen s
a₀ : E
ha₀ : a₀ ∈ s
ht₁ : Convex ℝ ∅
ht₃ : IsOpen ∅
disj : Disjoint s ∅
⊢ ∃ f u, (∀ (a : E), a ∈ s → ↑f a < u) ∧ ∀ (b : E), b ∈ ∅ → u < ↑f b
[PROOFSTEP]
exact ⟨0, 1, fun a _ha => by norm_num, by simp⟩
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : TopologicalSpace E
inst✝³ : AddCommGroup E
inst✝² : TopologicalAddGroup E
inst✝¹ : Module ℝ E
inst✝ : ContinuousSMul ℝ E
s : Set E
x y : E
hs₁ : Convex ℝ s
hs₂ : IsOpen s
a₀ : E
ha₀ : a₀ ∈ s
ht₁ : Convex ℝ ∅
ht₃ : IsOpen ∅
disj : Disjoint s ∅
a : E
_ha : a ∈ s
⊢ ↑0 a < 1
[PROOFSTEP]
norm_num
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : TopologicalSpace E
inst✝³ : AddCommGroup E
inst✝² : TopologicalAddGroup E
inst✝¹ : Module ℝ E
inst✝ : ContinuousSMul ℝ E
s : Set E
x y : E
hs₁ : Convex ℝ s
hs₂ : IsOpen s
a₀ : E
ha₀ : a₀ ∈ s
ht₁ : Convex ℝ ∅
ht₃ : IsOpen ∅
disj : Disjoint s ∅
⊢ ∀ (b : E), b ∈ ∅ → 1 < ↑0 b
[PROOFSTEP]
simp
[GOAL]
case inr.intro.inr.intro
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : TopologicalSpace E
inst✝³ : AddCommGroup E
inst✝² : TopologicalAddGroup E
inst✝¹ : Module ℝ E
inst✝ : ContinuousSMul ℝ E
s t : Set E
x y : E
hs₁ : Convex ℝ s
hs₂ : IsOpen s
ht₁ : Convex ℝ t
ht₃ : IsOpen t
disj : Disjoint s t
a₀ : E
ha₀ : a₀ ∈ s
b₀ : E
hb₀ : b₀ ∈ t
⊢ ∃ f u, (∀ (a : E), a ∈ s → ↑f a < u) ∧ ∀ (b : E), b ∈ t → u < ↑f b
[PROOFSTEP]
obtain ⟨f, s, hf₁, hf₂⟩ := geometric_hahn_banach_open hs₁ hs₂ ht₁ disj
[GOAL]
case inr.intro.inr.intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : TopologicalSpace E
inst✝³ : AddCommGroup E
inst✝² : TopologicalAddGroup E
inst✝¹ : Module ℝ E
inst✝ : ContinuousSMul ℝ E
s✝ t : Set E
x y : E
hs₁ : Convex ℝ s✝
hs₂ : IsOpen s✝
ht₁ : Convex ℝ t
ht₃ : IsOpen t
disj : Disjoint s✝ t
a₀ : E
ha₀ : a₀ ∈ s✝
b₀ : E
hb₀ : b₀ ∈ t
f : E →L[ℝ] ℝ
s : ℝ
hf₁ : ∀ (a : E), a ∈ s✝ → ↑f a < s
hf₂ : ∀ (b : E), b ∈ t → s ≤ ↑f b
⊢ ∃ f u, (∀ (a : E), a ∈ s✝ → ↑f a < u) ∧ ∀ (b : E), b ∈ t → u < ↑f b
[PROOFSTEP]
have hf : IsOpenMap f := by
  refine' f.isOpenMap_of_ne_zero _
  rintro rfl
  simp_rw [ContinuousLinearMap.zero_apply] at hf₁ hf₂
  exact (hf₁ _ ha₀).not_le (hf₂ _ hb₀)
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : TopologicalSpace E
inst✝³ : AddCommGroup E
inst✝² : TopologicalAddGroup E
inst✝¹ : Module ℝ E
inst✝ : ContinuousSMul ℝ E
s✝ t : Set E
x y : E
hs₁ : Convex ℝ s✝
hs₂ : IsOpen s✝
ht₁ : Convex ℝ t
ht₃ : IsOpen t
disj : Disjoint s✝ t
a₀ : E
ha₀ : a₀ ∈ s✝
b₀ : E
hb₀ : b₀ ∈ t
f : E →L[ℝ] ℝ
s : ℝ
hf₁ : ∀ (a : E), a ∈ s✝ → ↑f a < s
hf₂ : ∀ (b : E), b ∈ t → s ≤ ↑f b
⊢ IsOpenMap ↑f
[PROOFSTEP]
refine' f.isOpenMap_of_ne_zero _
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : TopologicalSpace E
inst✝³ : AddCommGroup E
inst✝² : TopologicalAddGroup E
inst✝¹ : Module ℝ E
inst✝ : ContinuousSMul ℝ E
s✝ t : Set E
x y : E
hs₁ : Convex ℝ s✝
hs₂ : IsOpen s✝
ht₁ : Convex ℝ t
ht₃ : IsOpen t
disj : Disjoint s✝ t
a₀ : E
ha₀ : a₀ ∈ s✝
b₀ : E
hb₀ : b₀ ∈ t
f : E →L[ℝ] ℝ
s : ℝ
hf₁ : ∀ (a : E), a ∈ s✝ → ↑f a < s
hf₂ : ∀ (b : E), b ∈ t → s ≤ ↑f b
⊢ f ≠ 0
[PROOFSTEP]
rintro rfl
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : TopologicalSpace E
inst✝³ : AddCommGroup E
inst✝² : TopologicalAddGroup E
inst✝¹ : Module ℝ E
inst✝ : ContinuousSMul ℝ E
s✝ t : Set E
x y : E
hs₁ : Convex ℝ s✝
hs₂ : IsOpen s✝
ht₁ : Convex ℝ t
ht₃ : IsOpen t
disj : Disjoint s✝ t
a₀ : E
ha₀ : a₀ ∈ s✝
b₀ : E
hb₀ : b₀ ∈ t
s : ℝ
hf₁ : ∀ (a : E), a ∈ s✝ → ↑0 a < s
hf₂ : ∀ (b : E), b ∈ t → s ≤ ↑0 b
⊢ False
[PROOFSTEP]
simp_rw [ContinuousLinearMap.zero_apply] at hf₁ hf₂
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : TopologicalSpace E
inst✝³ : AddCommGroup E
inst✝² : TopologicalAddGroup E
inst✝¹ : Module ℝ E
inst✝ : ContinuousSMul ℝ E
s✝ t : Set E
x y : E
hs₁ : Convex ℝ s✝
hs₂ : IsOpen s✝
ht₁ : Convex ℝ t
ht₃ : IsOpen t
disj : Disjoint s✝ t
a₀ : E
ha₀ : a₀ ∈ s✝
b₀ : E
hb₀ : b₀ ∈ t
s : ℝ
hf₁ : ∀ (a : E), a ∈ s✝ → 0 < s
hf₂ : ∀ (b : E), b ∈ t → s ≤ 0
⊢ False
[PROOFSTEP]
exact (hf₁ _ ha₀).not_le (hf₂ _ hb₀)
[GOAL]
case inr.intro.inr.intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : TopologicalSpace E
inst✝³ : AddCommGroup E
inst✝² : TopologicalAddGroup E
inst✝¹ : Module ℝ E
inst✝ : ContinuousSMul ℝ E
s✝ t : Set E
x y : E
hs₁ : Convex ℝ s✝
hs₂ : IsOpen s✝
ht₁ : Convex ℝ t
ht₃ : IsOpen t
disj : Disjoint s✝ t
a₀ : E
ha₀ : a₀ ∈ s✝
b₀ : E
hb₀ : b₀ ∈ t
f : E →L[ℝ] ℝ
s : ℝ
hf₁ : ∀ (a : E), a ∈ s✝ → ↑f a < s
hf₂ : ∀ (b : E), b ∈ t → s ≤ ↑f b
hf : IsOpenMap ↑f
⊢ ∃ f u, (∀ (a : E), a ∈ s✝ → ↑f a < u) ∧ ∀ (b : E), b ∈ t → u < ↑f b
[PROOFSTEP]
refine' ⟨f, s, hf₁, image_subset_iff.1 (_ : f '' t ⊆ Ioi s)⟩
[GOAL]
case inr.intro.inr.intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : TopologicalSpace E
inst✝³ : AddCommGroup E
inst✝² : TopologicalAddGroup E
inst✝¹ : Module ℝ E
inst✝ : ContinuousSMul ℝ E
s✝ t : Set E
x y : E
hs₁ : Convex ℝ s✝
hs₂ : IsOpen s✝
ht₁ : Convex ℝ t
ht₃ : IsOpen t
disj : Disjoint s✝ t
a₀ : E
ha₀ : a₀ ∈ s✝
b₀ : E
hb₀ : b₀ ∈ t
f : E →L[ℝ] ℝ
s : ℝ
hf₁ : ∀ (a : E), a ∈ s✝ → ↑f a < s
hf₂ : ∀ (b : E), b ∈ t → s ≤ ↑f b
hf : IsOpenMap ↑f
⊢ ↑f '' t ⊆ Ioi s
[PROOFSTEP]
rw [← interior_Ici]
[GOAL]
case inr.intro.inr.intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : TopologicalSpace E
inst✝³ : AddCommGroup E
inst✝² : TopologicalAddGroup E
inst✝¹ : Module ℝ E
inst✝ : ContinuousSMul ℝ E
s✝ t : Set E
x y : E
hs₁ : Convex ℝ s✝
hs₂ : IsOpen s✝
ht₁ : Convex ℝ t
ht₃ : IsOpen t
disj : Disjoint s✝ t
a₀ : E
ha₀ : a₀ ∈ s✝
b₀ : E
hb₀ : b₀ ∈ t
f : E →L[ℝ] ℝ
s : ℝ
hf₁ : ∀ (a : E), a ∈ s✝ → ↑f a < s
hf₂ : ∀ (b : E), b ∈ t → s ≤ ↑f b
hf : IsOpenMap ↑f
⊢ ↑f '' t ⊆ interior (Ici s)
[PROOFSTEP]
refine' interior_maximal (image_subset_iff.2 hf₂) (f.isOpenMap_of_ne_zero _ _ ht₃)
[GOAL]
case inr.intro.inr.intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : TopologicalSpace E
inst✝³ : AddCommGroup E
inst✝² : TopologicalAddGroup E
inst✝¹ : Module ℝ E
inst✝ : ContinuousSMul ℝ E
s✝ t : Set E
x y : E
hs₁ : Convex ℝ s✝
hs₂ : IsOpen s✝
ht₁ : Convex ℝ t
ht₃ : IsOpen t
disj : Disjoint s✝ t
a₀ : E
ha₀ : a₀ ∈ s✝
b₀ : E
hb₀ : b₀ ∈ t
f : E →L[ℝ] ℝ
s : ℝ
hf₁ : ∀ (a : E), a ∈ s✝ → ↑f a < s
hf₂ : ∀ (b : E), b ∈ t → s ≤ ↑f b
hf : IsOpenMap ↑f
⊢ f ≠ 0
[PROOFSTEP]
rintro rfl
[GOAL]
case inr.intro.inr.intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : TopologicalSpace E
inst✝³ : AddCommGroup E
inst✝² : TopologicalAddGroup E
inst✝¹ : Module ℝ E
inst✝ : ContinuousSMul ℝ E
s✝ t : Set E
x y : E
hs₁ : Convex ℝ s✝
hs₂ : IsOpen s✝
ht₁ : Convex ℝ t
ht₃ : IsOpen t
disj : Disjoint s✝ t
a₀ : E
ha₀ : a₀ ∈ s✝
b₀ : E
hb₀ : b₀ ∈ t
s : ℝ
hf₁ : ∀ (a : E), a ∈ s✝ → ↑0 a < s
hf₂ : ∀ (b : E), b ∈ t → s ≤ ↑0 b
hf : IsOpenMap ↑0
⊢ False
[PROOFSTEP]
simp_rw [ContinuousLinearMap.zero_apply] at hf₁ hf₂
[GOAL]
case inr.intro.inr.intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : TopologicalSpace E
inst✝³ : AddCommGroup E
inst✝² : TopologicalAddGroup E
inst✝¹ : Module ℝ E
inst✝ : ContinuousSMul ℝ E
s✝ t : Set E
x y : E
hs₁ : Convex ℝ s✝
hs₂ : IsOpen s✝
ht₁ : Convex ℝ t
ht₃ : IsOpen t
disj : Disjoint s✝ t
a₀ : E
ha₀ : a₀ ∈ s✝
b₀ : E
hb₀ : b₀ ∈ t
s : ℝ
hf₁ : ∀ (a : E), a ∈ s✝ → 0 < s
hf₂ : ∀ (b : E), b ∈ t → s ≤ 0
hf : IsOpenMap ↑0
⊢ False
[PROOFSTEP]
exact (hf₁ _ ha₀).not_le (hf₂ _ hb₀)
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : TopologicalSpace E
inst✝⁴ : AddCommGroup E
inst✝³ : TopologicalAddGroup E
inst✝² : Module ℝ E
inst✝¹ : ContinuousSMul ℝ E
s t : Set E
x y : E
inst✝ : LocallyConvexSpace ℝ E
hs₁ : Convex ℝ s
hs₂ : IsCompact s
ht₁ : Convex ℝ t
ht₂ : IsClosed t
disj : Disjoint s t
⊢ ∃ f u v, (∀ (a : E), a ∈ s → ↑f a < u) ∧ u < v ∧ ∀ (b : E), b ∈ t → v < ↑f b
[PROOFSTEP]
obtain rfl | hs := s.eq_empty_or_nonempty
[GOAL]
case inl
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : TopologicalSpace E
inst✝⁴ : AddCommGroup E
inst✝³ : TopologicalAddGroup E
inst✝² : Module ℝ E
inst✝¹ : ContinuousSMul ℝ E
t : Set E
x y : E
inst✝ : LocallyConvexSpace ℝ E
ht₁ : Convex ℝ t
ht₂ : IsClosed t
hs₁ : Convex ℝ ∅
hs₂ : IsCompact ∅
disj : Disjoint ∅ t
⊢ ∃ f u v, (∀ (a : E), a ∈ ∅ → ↑f a < u) ∧ u < v ∧ ∀ (b : E), b ∈ t → v < ↑f b
[PROOFSTEP]
exact ⟨0, -2, -1, by simp, by norm_num, fun b _hb => by norm_num⟩
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : TopologicalSpace E
inst✝⁴ : AddCommGroup E
inst✝³ : TopologicalAddGroup E
inst✝² : Module ℝ E
inst✝¹ : ContinuousSMul ℝ E
t : Set E
x y : E
inst✝ : LocallyConvexSpace ℝ E
ht₁ : Convex ℝ t
ht₂ : IsClosed t
hs₁ : Convex ℝ ∅
hs₂ : IsCompact ∅
disj : Disjoint ∅ t
⊢ ∀ (a : E), a ∈ ∅ → ↑0 a < -2
[PROOFSTEP]
simp
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : TopologicalSpace E
inst✝⁴ : AddCommGroup E
inst✝³ : TopologicalAddGroup E
inst✝² : Module ℝ E
inst✝¹ : ContinuousSMul ℝ E
t : Set E
x y : E
inst✝ : LocallyConvexSpace ℝ E
ht₁ : Convex ℝ t
ht₂ : IsClosed t
hs₁ : Convex ℝ ∅
hs₂ : IsCompact ∅
disj : Disjoint ∅ t
⊢ -2 < -1
[PROOFSTEP]
norm_num
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : TopologicalSpace E
inst✝⁴ : AddCommGroup E
inst✝³ : TopologicalAddGroup E
inst✝² : Module ℝ E
inst✝¹ : ContinuousSMul ℝ E
t : Set E
x y : E
inst✝ : LocallyConvexSpace ℝ E
ht₁ : Convex ℝ t
ht₂ : IsClosed t
hs₁ : Convex ℝ ∅
hs₂ : IsCompact ∅
disj : Disjoint ∅ t
b : E
_hb : b ∈ t
⊢ -1 < ↑0 b
[PROOFSTEP]
norm_num
[GOAL]
case inr
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : TopologicalSpace E
inst✝⁴ : AddCommGroup E
inst✝³ : TopologicalAddGroup E
inst✝² : Module ℝ E
inst✝¹ : ContinuousSMul ℝ E
s t : Set E
x y : E
inst✝ : LocallyConvexSpace ℝ E
hs₁ : Convex ℝ s
hs₂ : IsCompact s
ht₁ : Convex ℝ t
ht₂ : IsClosed t
disj : Disjoint s t
hs : Set.Nonempty s
⊢ ∃ f u v, (∀ (a : E), a ∈ s → ↑f a < u) ∧ u < v ∧ ∀ (b : E), b ∈ t → v < ↑f b
[PROOFSTEP]
obtain rfl | _ht := t.eq_empty_or_nonempty
[GOAL]
case inr.inl
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : TopologicalSpace E
inst✝⁴ : AddCommGroup E
inst✝³ : TopologicalAddGroup E
inst✝² : Module ℝ E
inst✝¹ : ContinuousSMul ℝ E
s : Set E
x y : E
inst✝ : LocallyConvexSpace ℝ E
hs₁ : Convex ℝ s
hs₂ : IsCompact s
hs : Set.Nonempty s
ht₁ : Convex ℝ ∅
ht₂ : IsClosed ∅
disj : Disjoint s ∅
⊢ ∃ f u v, (∀ (a : E), a ∈ s → ↑f a < u) ∧ u < v ∧ ∀ (b : E), b ∈ ∅ → v < ↑f b
[PROOFSTEP]
exact ⟨0, 1, 2, fun a _ha => by norm_num, by norm_num, by simp⟩
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : TopologicalSpace E
inst✝⁴ : AddCommGroup E
inst✝³ : TopologicalAddGroup E
inst✝² : Module ℝ E
inst✝¹ : ContinuousSMul ℝ E
s : Set E
x y : E
inst✝ : LocallyConvexSpace ℝ E
hs₁ : Convex ℝ s
hs₂ : IsCompact s
hs : Set.Nonempty s
ht₁ : Convex ℝ ∅
ht₂ : IsClosed ∅
disj : Disjoint s ∅
a : E
_ha : a ∈ s
⊢ ↑0 a < 1
[PROOFSTEP]
norm_num
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : TopologicalSpace E
inst✝⁴ : AddCommGroup E
inst✝³ : TopologicalAddGroup E
inst✝² : Module ℝ E
inst✝¹ : ContinuousSMul ℝ E
s : Set E
x y : E
inst✝ : LocallyConvexSpace ℝ E
hs₁ : Convex ℝ s
hs₂ : IsCompact s
hs : Set.Nonempty s
ht₁ : Convex ℝ ∅
ht₂ : IsClosed ∅
disj : Disjoint s ∅
⊢ 1 < 2
[PROOFSTEP]
norm_num
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : TopologicalSpace E
inst✝⁴ : AddCommGroup E
inst✝³ : TopologicalAddGroup E
inst✝² : Module ℝ E
inst✝¹ : ContinuousSMul ℝ E
s : Set E
x y : E
inst✝ : LocallyConvexSpace ℝ E
hs₁ : Convex ℝ s
hs₂ : IsCompact s
hs : Set.Nonempty s
ht₁ : Convex ℝ ∅
ht₂ : IsClosed ∅
disj : Disjoint s ∅
⊢ ∀ (b : E), b ∈ ∅ → 2 < ↑0 b
[PROOFSTEP]
simp
[GOAL]
case inr.inr
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : TopologicalSpace E
inst✝⁴ : AddCommGroup E
inst✝³ : TopologicalAddGroup E
inst✝² : Module ℝ E
inst✝¹ : ContinuousSMul ℝ E
s t : Set E
x y : E
inst✝ : LocallyConvexSpace ℝ E
hs₁ : Convex ℝ s
hs₂ : IsCompact s
ht₁ : Convex ℝ t
ht₂ : IsClosed t
disj : Disjoint s t
hs : Set.Nonempty s
_ht : Set.Nonempty t
⊢ ∃ f u v, (∀ (a : E), a ∈ s → ↑f a < u) ∧ u < v ∧ ∀ (b : E), b ∈ t → v < ↑f b
[PROOFSTEP]
obtain ⟨U, V, hU, hV, hU₁, hV₁, sU, tV, disj'⟩ := disj.exists_open_convexes hs₁ hs₂ ht₁ ht₂
[GOAL]
case inr.inr.intro.intro.intro.intro.intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : TopologicalSpace E
inst✝⁴ : AddCommGroup E
inst✝³ : TopologicalAddGroup E
inst✝² : Module ℝ E
inst✝¹ : ContinuousSMul ℝ E
s t : Set E
x y : E
inst✝ : LocallyConvexSpace ℝ E
hs₁ : Convex ℝ s
hs₂ : IsCompact s
ht₁ : Convex ℝ t
ht₂ : IsClosed t
disj : Disjoint s t
hs : Set.Nonempty s
_ht : Set.Nonempty t
U V : Set E
hU : IsOpen U
hV : IsOpen V
hU₁ : Convex ℝ U
hV₁ : Convex ℝ V
sU : s ⊆ U
tV : t ⊆ V
disj' : Disjoint U V
⊢ ∃ f u v, (∀ (a : E), a ∈ s → ↑f a < u) ∧ u < v ∧ ∀ (b : E), b ∈ t → v < ↑f b
[PROOFSTEP]
obtain ⟨f, u, hf₁, hf₂⟩ := geometric_hahn_banach_open_open hU₁ hU hV₁ hV disj'
[GOAL]
case inr.inr.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : TopologicalSpace E
inst✝⁴ : AddCommGroup E
inst✝³ : TopologicalAddGroup E
inst✝² : Module ℝ E
inst✝¹ : ContinuousSMul ℝ E
s t : Set E
x y : E
inst✝ : LocallyConvexSpace ℝ E
hs₁ : Convex ℝ s
hs₂ : IsCompact s
ht₁ : Convex ℝ t
ht₂ : IsClosed t
disj : Disjoint s t
hs : Set.Nonempty s
_ht : Set.Nonempty t
U V : Set E
hU : IsOpen U
hV : IsOpen V
hU₁ : Convex ℝ U
hV₁ : Convex ℝ V
sU : s ⊆ U
tV : t ⊆ V
disj' : Disjoint U V
f : E →L[ℝ] ℝ
u : ℝ
hf₁ : ∀ (a : E), a ∈ U → ↑f a < u
hf₂ : ∀ (b : E), b ∈ V → u < ↑f b
⊢ ∃ f u v, (∀ (a : E), a ∈ s → ↑f a < u) ∧ u < v ∧ ∀ (b : E), b ∈ t → v < ↑f b
[PROOFSTEP]
obtain ⟨x, hx₁, hx₂⟩ := hs₂.exists_forall_ge hs f.continuous.continuousOn
[GOAL]
case inr.inr.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : TopologicalSpace E
inst✝⁴ : AddCommGroup E
inst✝³ : TopologicalAddGroup E
inst✝² : Module ℝ E
inst✝¹ : ContinuousSMul ℝ E
s t : Set E
x✝ y : E
inst✝ : LocallyConvexSpace ℝ E
hs₁ : Convex ℝ s
hs₂ : IsCompact s
ht₁ : Convex ℝ t
ht₂ : IsClosed t
disj : Disjoint s t
hs : Set.Nonempty s
_ht : Set.Nonempty t
U V : Set E
hU : IsOpen U
hV : IsOpen V
hU₁ : Convex ℝ U
hV₁ : Convex ℝ V
sU : s ⊆ U
tV : t ⊆ V
disj' : Disjoint U V
f : E →L[ℝ] ℝ
u : ℝ
hf₁ : ∀ (a : E), a ∈ U → ↑f a < u
hf₂ : ∀ (b : E), b ∈ V → u < ↑f b
x : E
hx₁ : x ∈ s
hx₂ : ∀ (y : E), y ∈ s → ↑f y ≤ ↑f x
⊢ ∃ f u v, (∀ (a : E), a ∈ s → ↑f a < u) ∧ u < v ∧ ∀ (b : E), b ∈ t → v < ↑f b
[PROOFSTEP]
have : f x < u := hf₁ x (sU hx₁)
[GOAL]
case inr.inr.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : TopologicalSpace E
inst✝⁴ : AddCommGroup E
inst✝³ : TopologicalAddGroup E
inst✝² : Module ℝ E
inst✝¹ : ContinuousSMul ℝ E
s t : Set E
x✝ y : E
inst✝ : LocallyConvexSpace ℝ E
hs₁ : Convex ℝ s
hs₂ : IsCompact s
ht₁ : Convex ℝ t
ht₂ : IsClosed t
disj : Disjoint s t
hs : Set.Nonempty s
_ht : Set.Nonempty t
U V : Set E
hU : IsOpen U
hV : IsOpen V
hU₁ : Convex ℝ U
hV₁ : Convex ℝ V
sU : s ⊆ U
tV : t ⊆ V
disj' : Disjoint U V
f : E →L[ℝ] ℝ
u : ℝ
hf₁ : ∀ (a : E), a ∈ U → ↑f a < u
hf₂ : ∀ (b : E), b ∈ V → u < ↑f b
x : E
hx₁ : x ∈ s
hx₂ : ∀ (y : E), y ∈ s → ↑f y ≤ ↑f x
this : ↑f x < u
⊢ ∃ f u v, (∀ (a : E), a ∈ s → ↑f a < u) ∧ u < v ∧ ∀ (b : E), b ∈ t → v < ↑f b
[PROOFSTEP]
exact ⟨f, (f x + u) / 2, u, fun a ha => by linarith [hx₂ a ha], by linarith, fun b hb => hf₂ b (tV hb)⟩
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : TopologicalSpace E
inst✝⁴ : AddCommGroup E
inst✝³ : TopologicalAddGroup E
inst✝² : Module ℝ E
inst✝¹ : ContinuousSMul ℝ E
s t : Set E
x✝ y : E
inst✝ : LocallyConvexSpace ℝ E
hs₁ : Convex ℝ s
hs₂ : IsCompact s
ht₁ : Convex ℝ t
ht₂ : IsClosed t
disj : Disjoint s t
hs : Set.Nonempty s
_ht : Set.Nonempty t
U V : Set E
hU : IsOpen U
hV : IsOpen V
hU₁ : Convex ℝ U
hV₁ : Convex ℝ V
sU : s ⊆ U
tV : t ⊆ V
disj' : Disjoint U V
f : E →L[ℝ] ℝ
u : ℝ
hf₁ : ∀ (a : E), a ∈ U → ↑f a < u
hf₂ : ∀ (b : E), b ∈ V → u < ↑f b
x : E
hx₁ : x ∈ s
hx₂ : ∀ (y : E), y ∈ s → ↑f y ≤ ↑f x
this : ↑f x < u
a : E
ha : a ∈ s
⊢ ↑f a < (↑f x + u) / 2
[PROOFSTEP]
linarith [hx₂ a ha]
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : TopologicalSpace E
inst✝⁴ : AddCommGroup E
inst✝³ : TopologicalAddGroup E
inst✝² : Module ℝ E
inst✝¹ : ContinuousSMul ℝ E
s t : Set E
x✝ y : E
inst✝ : LocallyConvexSpace ℝ E
hs₁ : Convex ℝ s
hs₂ : IsCompact s
ht₁ : Convex ℝ t
ht₂ : IsClosed t
disj : Disjoint s t
hs : Set.Nonempty s
_ht : Set.Nonempty t
U V : Set E
hU : IsOpen U
hV : IsOpen V
hU₁ : Convex ℝ U
hV₁ : Convex ℝ V
sU : s ⊆ U
tV : t ⊆ V
disj' : Disjoint U V
f : E →L[ℝ] ℝ
u : ℝ
hf₁ : ∀ (a : E), a ∈ U → ↑f a < u
hf₂ : ∀ (b : E), b ∈ V → u < ↑f b
x : E
hx₁ : x ∈ s
hx₂ : ∀ (y : E), y ∈ s → ↑f y ≤ ↑f x
this : ↑f x < u
⊢ (↑f x + u) / 2 < u
[PROOFSTEP]
linarith
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : TopologicalSpace E
inst✝⁴ : AddCommGroup E
inst✝³ : TopologicalAddGroup E
inst✝² : Module ℝ E
inst✝¹ : ContinuousSMul ℝ E
s✝ t✝ : Set E
x y : E
inst✝ : LocallyConvexSpace ℝ E
hs₁ : Convex ℝ s✝
hs₂ : IsClosed s✝
ht₁ : Convex ℝ t✝
ht₂ : IsCompact t✝
disj : Disjoint s✝ t✝
f : E →L[ℝ] ℝ
s t : ℝ
hs : ∀ (a : E), a ∈ t✝ → ↑f a < s
st : s < t
ht : ∀ (b : E), b ∈ s✝ → t < ↑f b
⊢ ∀ (a : E), a ∈ s✝ → ↑(-f) a < -t
[PROOFSTEP]
simpa using ht
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : TopologicalSpace E
inst✝⁴ : AddCommGroup E
inst✝³ : TopologicalAddGroup E
inst✝² : Module ℝ E
inst✝¹ : ContinuousSMul ℝ E
s✝ t✝ : Set E
x y : E
inst✝ : LocallyConvexSpace ℝ E
hs₁ : Convex ℝ s✝
hs₂ : IsClosed s✝
ht₁ : Convex ℝ t✝
ht₂ : IsCompact t✝
disj : Disjoint s✝ t✝
f : E →L[ℝ] ℝ
s t : ℝ
hs : ∀ (a : E), a ∈ t✝ → ↑f a < s
st : s < t
ht : ∀ (b : E), b ∈ s✝ → t < ↑f b
⊢ -t < -s
[PROOFSTEP]
simpa using st
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : TopologicalSpace E
inst✝⁴ : AddCommGroup E
inst✝³ : TopologicalAddGroup E
inst✝² : Module ℝ E
inst✝¹ : ContinuousSMul ℝ E
s✝ t✝ : Set E
x y : E
inst✝ : LocallyConvexSpace ℝ E
hs₁ : Convex ℝ s✝
hs₂ : IsClosed s✝
ht₁ : Convex ℝ t✝
ht₂ : IsCompact t✝
disj : Disjoint s✝ t✝
f : E →L[ℝ] ℝ
s t : ℝ
hs : ∀ (a : E), a ∈ t✝ → ↑f a < s
st : s < t
ht : ∀ (b : E), b ∈ s✝ → t < ↑f b
⊢ ∀ (b : E), b ∈ t✝ → -s < ↑(-f) b
[PROOFSTEP]
simpa using hs
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝⁶ : TopologicalSpace E
inst✝⁵ : AddCommGroup E
inst✝⁴ : TopologicalAddGroup E
inst✝³ : Module ℝ E
inst✝² : ContinuousSMul ℝ E
s t : Set E
x y : E
inst✝¹ : LocallyConvexSpace ℝ E
inst✝ : T1Space E
hxy : x ≠ y
⊢ ∃ f, ↑f x < ↑f y
[PROOFSTEP]
obtain ⟨f, s, t, hs, st, ht⟩ :=
  geometric_hahn_banach_compact_closed (convex_singleton x) isCompact_singleton (convex_singleton y) isClosed_singleton
    (disjoint_singleton.2 hxy)
[GOAL]
case intro.intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝⁶ : TopologicalSpace E
inst✝⁵ : AddCommGroup E
inst✝⁴ : TopologicalAddGroup E
inst✝³ : Module ℝ E
inst✝² : ContinuousSMul ℝ E
s✝ t✝ : Set E
x y : E
inst✝¹ : LocallyConvexSpace ℝ E
inst✝ : T1Space E
hxy : x ≠ y
f : E →L[ℝ] ℝ
s t : ℝ
hs : ∀ (a : E), a ∈ {x} → ↑f a < s
st : s < t
ht : ∀ (b : E), b ∈ {y} → t < ↑f b
⊢ ∃ f, ↑f x < ↑f y
[PROOFSTEP]
exact ⟨f, by linarith [hs x rfl, ht y rfl]⟩
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝⁶ : TopologicalSpace E
inst✝⁵ : AddCommGroup E
inst✝⁴ : TopologicalAddGroup E
inst✝³ : Module ℝ E
inst✝² : ContinuousSMul ℝ E
s✝ t✝ : Set E
x y : E
inst✝¹ : LocallyConvexSpace ℝ E
inst✝ : T1Space E
hxy : x ≠ y
f : E →L[ℝ] ℝ
s t : ℝ
hs : ∀ (a : E), a ∈ {x} → ↑f a < s
st : s < t
ht : ∀ (b : E), b ∈ {y} → t < ↑f b
⊢ ↑f x < ↑f y
[PROOFSTEP]
linarith [hs x rfl, ht y rfl]
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : TopologicalSpace E
inst✝⁴ : AddCommGroup E
inst✝³ : TopologicalAddGroup E
inst✝² : Module ℝ E
inst✝¹ : ContinuousSMul ℝ E
s t : Set E
x y : E
inst✝ : LocallyConvexSpace ℝ E
hs₁ : Convex ℝ s
hs₂ : IsClosed s
⊢ ⋂ (l : E →L[ℝ] ℝ), {x | ∃ y, y ∈ s ∧ ↑l x ≤ ↑l y} = s
[PROOFSTEP]
rw [Set.iInter_setOf]
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : TopologicalSpace E
inst✝⁴ : AddCommGroup E
inst✝³ : TopologicalAddGroup E
inst✝² : Module ℝ E
inst✝¹ : ContinuousSMul ℝ E
s t : Set E
x y : E
inst✝ : LocallyConvexSpace ℝ E
hs₁ : Convex ℝ s
hs₂ : IsClosed s
⊢ {x | ∀ (i : E →L[ℝ] ℝ), ∃ y, y ∈ s ∧ ↑i x ≤ ↑i y} = s
[PROOFSTEP]
refine' Set.Subset.antisymm (fun x hx => _) fun x hx l => ⟨x, hx, le_rfl⟩
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : TopologicalSpace E
inst✝⁴ : AddCommGroup E
inst✝³ : TopologicalAddGroup E
inst✝² : Module ℝ E
inst✝¹ : ContinuousSMul ℝ E
s t : Set E
x✝ y : E
inst✝ : LocallyConvexSpace ℝ E
hs₁ : Convex ℝ s
hs₂ : IsClosed s
x : E
hx : x ∈ {x | ∀ (i : E →L[ℝ] ℝ), ∃ y, y ∈ s ∧ ↑i x ≤ ↑i y}
⊢ x ∈ s
[PROOFSTEP]
by_contra h
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : TopologicalSpace E
inst✝⁴ : AddCommGroup E
inst✝³ : TopologicalAddGroup E
inst✝² : Module ℝ E
inst✝¹ : ContinuousSMul ℝ E
s t : Set E
x✝ y : E
inst✝ : LocallyConvexSpace ℝ E
hs₁ : Convex ℝ s
hs₂ : IsClosed s
x : E
hx : x ∈ {x | ∀ (i : E →L[ℝ] ℝ), ∃ y, y ∈ s ∧ ↑i x ≤ ↑i y}
h : ¬x ∈ s
⊢ False
[PROOFSTEP]
obtain ⟨l, s, hlA, hl⟩ := geometric_hahn_banach_closed_point hs₁ hs₂ h
[GOAL]
case intro.intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : TopologicalSpace E
inst✝⁴ : AddCommGroup E
inst✝³ : TopologicalAddGroup E
inst✝² : Module ℝ E
inst✝¹ : ContinuousSMul ℝ E
s✝ t : Set E
x✝ y : E
inst✝ : LocallyConvexSpace ℝ E
hs₁ : Convex ℝ s✝
hs₂ : IsClosed s✝
x : E
hx : x ∈ {x | ∀ (i : E →L[ℝ] ℝ), ∃ y, y ∈ s✝ ∧ ↑i x ≤ ↑i y}
h : ¬x ∈ s✝
l : E →L[ℝ] ℝ
s : ℝ
hlA : ∀ (a : E), a ∈ s✝ → ↑l a < s
hl : s < ↑l x
⊢ False
[PROOFSTEP]
obtain ⟨y, hy, hxy⟩ := hx l
[GOAL]
case intro.intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : TopologicalSpace E
inst✝⁴ : AddCommGroup E
inst✝³ : TopologicalAddGroup E
inst✝² : Module ℝ E
inst✝¹ : ContinuousSMul ℝ E
s✝ t : Set E
x✝ y✝ : E
inst✝ : LocallyConvexSpace ℝ E
hs₁ : Convex ℝ s✝
hs₂ : IsClosed s✝
x : E
hx : x ∈ {x | ∀ (i : E →L[ℝ] ℝ), ∃ y, y ∈ s✝ ∧ ↑i x ≤ ↑i y}
h : ¬x ∈ s✝
l : E →L[ℝ] ℝ
s : ℝ
hlA : ∀ (a : E), a ∈ s✝ → ↑l a < s
hl : s < ↑l x
y : E
hy : y ∈ s✝
hxy : ↑l x ≤ ↑l y
⊢ False
[PROOFSTEP]
exact ((hxy.trans_lt (hlA y hy)).trans hl).not_le le_rfl


[GOAL]
α : Type u_1
β : Type u_2
inst✝³ : SeminormedAddGroup α
inst✝² : SeminormedAddGroup β
inst✝¹ : SMulZeroClass α β
inst✝ : BoundedSMul α β
r : α
x : β
⊢ ‖r • x‖ ≤ ‖r‖ * ‖x‖
[PROOFSTEP]
simpa [smul_zero] using dist_smul_pair r 0 x
[GOAL]
α : Type u_1
β : Type u_2
inst✝³ : SeminormedAddGroup α
inst✝² : SeminormedAddGroup β
inst✝¹ : SMulZeroClass α β
inst✝ : BoundedSMul α β
s : α
x y : β
⊢ dist (s • x) (s • y) ≤ ‖s‖ * dist x y
[PROOFSTEP]
simpa only [dist_eq_norm, sub_zero] using dist_smul_pair s x y
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : NonUnitalSeminormedRing α
x y₁ y₂ : α
⊢ dist (x • y₁) (x • y₂) ≤ dist x 0 * dist y₁ y₂
[PROOFSTEP]
simpa [mul_sub, dist_eq_norm] using norm_mul_le x (y₁ - y₂)
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : NonUnitalSeminormedRing α
x₁ x₂ y : α
⊢ dist (x₁ • y) (x₂ • y) ≤ dist x₁ x₂ * dist y 0
[PROOFSTEP]
simpa [sub_mul, dist_eq_norm] using norm_mul_le (x₁ - x₂) y
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : NonUnitalSeminormedRing α
x : αᵐᵒᵖ
y₁ y₂ : α
⊢ dist (x • y₁) (x • y₂) ≤ dist x 0 * dist y₁ y₂
[PROOFSTEP]
simpa [sub_mul, dist_eq_norm, mul_comm] using norm_mul_le (y₁ - y₂) x.unop
[GOAL]
α : Type u_1
β : Type u_2
inst✝ : NonUnitalSeminormedRing α
x₁ x₂ : αᵐᵒᵖ
y : α
⊢ dist (x₁ • y) (x₂ • y) ≤ dist x₁ x₂ * dist y 0
[PROOFSTEP]
simpa [mul_sub, dist_eq_norm, mul_comm] using norm_mul_le y (x₁ - x₂).unop
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : SeminormedRing α
inst✝¹ : SeminormedAddCommGroup β
inst✝ : Module α β
h : ∀ (r : α) (x : β), ‖r • x‖ ≤ ‖r‖ * ‖x‖
a : α
b₁ b₂ : β
⊢ dist (a • b₁) (a • b₂) ≤ dist a 0 * dist b₁ b₂
[PROOFSTEP]
simpa [smul_sub, dist_eq_norm] using h a (b₁ - b₂)
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : SeminormedRing α
inst✝¹ : SeminormedAddCommGroup β
inst✝ : Module α β
h : ∀ (r : α) (x : β), ‖r • x‖ ≤ ‖r‖ * ‖x‖
a₁ a₂ : α
b : β
⊢ dist (a₁ • b) (a₂ • b) ≤ dist a₁ a₂ * dist b 0
[PROOFSTEP]
simpa [sub_smul, dist_eq_norm] using h (a₁ - a₂) b
[GOAL]
α : Type u_1
β : Type u_2
inst✝³ : NormedDivisionRing α
inst✝² : SeminormedAddGroup β
inst✝¹ : MulActionWithZero α β
inst✝ : BoundedSMul α β
r : α
x : β
⊢ ‖r • x‖ = ‖r‖ * ‖x‖
[PROOFSTEP]
by_cases h : r = 0
[GOAL]
case pos
α : Type u_1
β : Type u_2
inst✝³ : NormedDivisionRing α
inst✝² : SeminormedAddGroup β
inst✝¹ : MulActionWithZero α β
inst✝ : BoundedSMul α β
r : α
x : β
h : r = 0
⊢ ‖r • x‖ = ‖r‖ * ‖x‖
[PROOFSTEP]
simp [h, zero_smul α x]
[GOAL]
case neg
α : Type u_1
β : Type u_2
inst✝³ : NormedDivisionRing α
inst✝² : SeminormedAddGroup β
inst✝¹ : MulActionWithZero α β
inst✝ : BoundedSMul α β
r : α
x : β
h : ¬r = 0
⊢ ‖r • x‖ = ‖r‖ * ‖x‖
[PROOFSTEP]
refine' le_antisymm (norm_smul_le r x) _
[GOAL]
case neg
α : Type u_1
β : Type u_2
inst✝³ : NormedDivisionRing α
inst✝² : SeminormedAddGroup β
inst✝¹ : MulActionWithZero α β
inst✝ : BoundedSMul α β
r : α
x : β
h : ¬r = 0
⊢ ‖r‖ * ‖x‖ ≤ ‖r • x‖
[PROOFSTEP]
calc
  ‖r‖ * ‖x‖ = ‖r‖ * ‖r⁻¹ • r • x‖ := by rw [inv_smul_smul₀ h]
  _ ≤ ‖r‖ * (‖r⁻¹‖ * ‖r • x‖) := by gcongr; apply norm_smul_le
  _ = ‖r • x‖ := by rw [norm_inv, ← mul_assoc, mul_inv_cancel (mt norm_eq_zero.1 h), one_mul]
[GOAL]
α : Type u_1
β : Type u_2
inst✝³ : NormedDivisionRing α
inst✝² : SeminormedAddGroup β
inst✝¹ : MulActionWithZero α β
inst✝ : BoundedSMul α β
r : α
x : β
h : ¬r = 0
⊢ ‖r‖ * ‖x‖ = ‖r‖ * ‖r⁻¹ • r • x‖
[PROOFSTEP]
rw [inv_smul_smul₀ h]
[GOAL]
α : Type u_1
β : Type u_2
inst✝³ : NormedDivisionRing α
inst✝² : SeminormedAddGroup β
inst✝¹ : MulActionWithZero α β
inst✝ : BoundedSMul α β
r : α
x : β
h : ¬r = 0
⊢ ‖r‖ * ‖r⁻¹ • r • x‖ ≤ ‖r‖ * (‖r⁻¹‖ * ‖r • x‖)
[PROOFSTEP]
gcongr
[GOAL]
case h
α : Type u_1
β : Type u_2
inst✝³ : NormedDivisionRing α
inst✝² : SeminormedAddGroup β
inst✝¹ : MulActionWithZero α β
inst✝ : BoundedSMul α β
r : α
x : β
h : ¬r = 0
⊢ ‖r⁻¹ • r • x‖ ≤ ‖r⁻¹‖ * ‖r • x‖
[PROOFSTEP]
apply norm_smul_le
[GOAL]
α : Type u_1
β : Type u_2
inst✝³ : NormedDivisionRing α
inst✝² : SeminormedAddGroup β
inst✝¹ : MulActionWithZero α β
inst✝ : BoundedSMul α β
r : α
x : β
h : ¬r = 0
⊢ ‖r‖ * (‖r⁻¹‖ * ‖r • x‖) = ‖r • x‖
[PROOFSTEP]
rw [norm_inv, ← mul_assoc, mul_inv_cancel (mt norm_eq_zero.1 h), one_mul]
[GOAL]
α : Type u_1
β : Type u_2
inst✝³ : NormedDivisionRing α
inst✝² : SeminormedAddCommGroup β
inst✝¹ : Module α β
inst✝ : BoundedSMul α β
s : α
x y : β
⊢ dist (s • x) (s • y) = ‖s‖ * dist x y
[PROOFSTEP]
simp_rw [dist_eq_norm, (norm_smul s (x - y)).symm, smul_sub]
[GOAL]
α : Type u_1
β : Type u_2
inst✝³ : NormedDivisionRing α
inst✝² : SeminormedAddCommGroup β
inst✝¹ : Module α β
inst✝ : BoundedSMul α β
s : α
x y : β
⊢ edist (s • x) (s • y) = ‖s‖₊ • edist x y
[PROOFSTEP]
simp only [edist_nndist, nndist_smul₀, ENNReal.coe_mul, ENNReal.smul_def, smul_eq_mul]


[GOAL]
α : Type u_1
β : Type u_2
l✝ : Filter α
k✝ f g g' : α → β
inst✝¹ : TopologicalSpace β
inst✝ : CommSemiring β
l : Filter α
k : α → β
z : ℕ
⊢ Tendsto (fun a => k a ^ z * OfNat.ofNat 0 a) l (𝓝 0)
[PROOFSTEP]
simpa only [Pi.zero_apply, mul_zero] using tendsto_const_nhds
[GOAL]
α : Type u_1
β : Type u_2
l : Filter α
k f g g' : α → β
inst✝² : TopologicalSpace β
inst✝¹ : CommSemiring β
inst✝ : ContinuousAdd β
hf : SuperpolynomialDecay l k f
hg : SuperpolynomialDecay l k g
z : ℕ
⊢ Tendsto (fun a => k a ^ z * (f + g) a) l (𝓝 0)
[PROOFSTEP]
simpa only [mul_add, add_zero, Pi.add_apply] using (hf z).add (hg z)
[GOAL]
α : Type u_1
β : Type u_2
l : Filter α
k f g g' : α → β
inst✝² : TopologicalSpace β
inst✝¹ : CommSemiring β
inst✝ : ContinuousMul β
hf : SuperpolynomialDecay l k f
hg : SuperpolynomialDecay l k g
z : ℕ
⊢ Tendsto (fun a => k a ^ z * (f * g) a) l (𝓝 0)
[PROOFSTEP]
simpa only [mul_assoc, one_mul, mul_zero, pow_zero] using (hf z).mul (hg 0)
[GOAL]
α : Type u_1
β : Type u_2
l : Filter α
k f g g' : α → β
inst✝² : TopologicalSpace β
inst✝¹ : CommSemiring β
inst✝ : ContinuousMul β
hf : SuperpolynomialDecay l k f
c : β
z : ℕ
⊢ Tendsto (fun a => k a ^ z * (fun n => f n * c) a) l (𝓝 0)
[PROOFSTEP]
simpa only [← mul_assoc, zero_mul] using Tendsto.mul_const c (hf z)
[GOAL]
α : Type u_1
β : Type u_2
l : Filter α
k f g g' : α → β
inst✝¹ : TopologicalSpace β
inst✝ : CommSemiring β
hf : SuperpolynomialDecay l k f
z : ℕ
s : Set β
hs : IsOpen s
hs0 : 0 ∈ s
x : α
hx : x ∈ (fun a => k a ^ (z + 1) * f a) ⁻¹' s
⊢ x ∈ (fun a => k a ^ z * (k * f) a) ⁻¹' s
[PROOFSTEP]
simpa only [Set.mem_preimage, Pi.mul_apply, ← mul_assoc, ← pow_succ'] using hx
[GOAL]
α : Type u_1
β : Type u_2
l : Filter α
k f g g' : α → β
inst✝¹ : TopologicalSpace β
inst✝ : CommSemiring β
hf : SuperpolynomialDecay l k f
n : ℕ
⊢ SuperpolynomialDecay l k (k ^ n * f)
[PROOFSTEP]
induction' n with n hn
[GOAL]
case zero
α : Type u_1
β : Type u_2
l : Filter α
k f g g' : α → β
inst✝¹ : TopologicalSpace β
inst✝ : CommSemiring β
hf : SuperpolynomialDecay l k f
⊢ SuperpolynomialDecay l k (k ^ Nat.zero * f)
[PROOFSTEP]
simpa only [Nat.zero_eq, one_mul, pow_zero] using hf
[GOAL]
case succ
α : Type u_1
β : Type u_2
l : Filter α
k f g g' : α → β
inst✝¹ : TopologicalSpace β
inst✝ : CommSemiring β
hf : SuperpolynomialDecay l k f
n : ℕ
hn : SuperpolynomialDecay l k (k ^ n * f)
⊢ SuperpolynomialDecay l k (k ^ Nat.succ n * f)
[PROOFSTEP]
simpa only [pow_succ, mul_assoc] using hn.param_mul
[GOAL]
α : Type u_1
β : Type u_2
l : Filter α
k f g g' : α → β
inst✝³ : TopologicalSpace β
inst✝² : CommSemiring β
inst✝¹ : ContinuousAdd β
inst✝ : ContinuousMul β
hf : SuperpolynomialDecay l k f
p✝ p q : β[X]
hp : SuperpolynomialDecay l k fun x => eval (k x) p * f x
hq : SuperpolynomialDecay l k fun x => eval (k x) q * f x
⊢ SuperpolynomialDecay l k fun x => eval (k x) (p + q) * f x
[PROOFSTEP]
simpa [add_mul] using hp.add hq
[GOAL]
α : Type u_1
β : Type u_2
l : Filter α
k f g g' : α → β
inst✝³ : TopologicalSpace β
inst✝² : CommSemiring β
inst✝¹ : ContinuousAdd β
inst✝ : ContinuousMul β
hf : SuperpolynomialDecay l k f
p : β[X]
n : ℕ
c : β
⊢ SuperpolynomialDecay l k fun x => eval (k x) (↑(monomial n) c) * f x
[PROOFSTEP]
simpa [mul_assoc] using (hf.param_pow_mul n).const_mul c
[GOAL]
α : Type u_1
β : Type u_2
l : Filter α
k f g g' : α → β
inst✝² : TopologicalSpace β
inst✝¹ : LinearOrderedCommRing β
inst✝ : OrderTopology β
⊢ (∀ (n : ℕ), Tendsto (fun a => |k a ^ n * f a|) l (𝓝 0)) ↔ SuperpolynomialDecay l (fun a => |k a|) fun a => |f a|
[PROOFSTEP]
simp_rw [SuperpolynomialDecay, abs_mul, abs_pow]
[GOAL]
α : Type u_1
β : Type u_2
l : Filter α
k f g g' : α → β
inst✝² : TopologicalSpace β
inst✝¹ : LinearOrderedCommRing β
inst✝ : OrderTopology β
hf : SuperpolynomialDecay l k f
hfg : abs ∘ g ≤ᶠ[l] abs ∘ f
⊢ SuperpolynomialDecay l k g
[PROOFSTEP]
rw [superpolynomialDecay_iff_abs_tendsto_zero] at hf ⊢
[GOAL]
α : Type u_1
β : Type u_2
l : Filter α
k f g g' : α → β
inst✝² : TopologicalSpace β
inst✝¹ : LinearOrderedCommRing β
inst✝ : OrderTopology β
hf : ∀ (n : ℕ), Tendsto (fun a => |k a ^ n * f a|) l (𝓝 0)
hfg : abs ∘ g ≤ᶠ[l] abs ∘ f
⊢ ∀ (n : ℕ), Tendsto (fun a => |k a ^ n * g a|) l (𝓝 0)
[PROOFSTEP]
refine' fun z =>
  tendsto_of_tendsto_of_tendsto_of_le_of_le' tendsto_const_nhds (hf z) (eventually_of_forall fun x => abs_nonneg _)
    (hfg.mono fun x hx => _)
[GOAL]
α : Type u_1
β : Type u_2
l : Filter α
k f g g' : α → β
inst✝² : TopologicalSpace β
inst✝¹ : LinearOrderedCommRing β
inst✝ : OrderTopology β
hf : ∀ (n : ℕ), Tendsto (fun a => |k a ^ n * f a|) l (𝓝 0)
hfg : abs ∘ g ≤ᶠ[l] abs ∘ f
z : ℕ
x : α
hx : (abs ∘ g) x ≤ (abs ∘ f) x
⊢ |k x ^ z * g x| ≤ |k x ^ z * f x|
[PROOFSTEP]
calc
  |k x ^ z * g x| = |k x ^ z| * |g x| := abs_mul (k x ^ z) (g x)
  _ ≤ |k x ^ z| * |f x| := by gcongr; exact hx
  _ = |k x ^ z * f x| := (abs_mul (k x ^ z) (f x)).symm
[GOAL]
α : Type u_1
β : Type u_2
l : Filter α
k f g g' : α → β
inst✝² : TopologicalSpace β
inst✝¹ : LinearOrderedCommRing β
inst✝ : OrderTopology β
hf : ∀ (n : ℕ), Tendsto (fun a => |k a ^ n * f a|) l (𝓝 0)
hfg : abs ∘ g ≤ᶠ[l] abs ∘ f
z : ℕ
x : α
hx : (abs ∘ g) x ≤ (abs ∘ f) x
⊢ |k x ^ z| * |g x| ≤ |k x ^ z| * |f x|
[PROOFSTEP]
gcongr
[GOAL]
case h
α : Type u_1
β : Type u_2
l : Filter α
k f g g' : α → β
inst✝² : TopologicalSpace β
inst✝¹ : LinearOrderedCommRing β
inst✝ : OrderTopology β
hf : ∀ (n : ℕ), Tendsto (fun a => |k a ^ n * f a|) l (𝓝 0)
hfg : abs ∘ g ≤ᶠ[l] abs ∘ f
z : ℕ
x : α
hx : (abs ∘ g) x ≤ (abs ∘ f) x
⊢ |g x| ≤ |f x|
[PROOFSTEP]
exact hx
[GOAL]
α : Type u_1
β : Type u_2
l : Filter α
k f g g' : α → β
inst✝² : TopologicalSpace β
inst✝¹ : Field β
inst✝ : ContinuousMul β
c : β
hc0 : c ≠ 0
h : SuperpolynomialDecay l k fun n => f n * c
x : α
⊢ f x * c * c⁻¹ = f x
[PROOFSTEP]
simp [mul_assoc, mul_inv_cancel hc0]
[GOAL]
α : Type u_1
β : Type u_2
l : Filter α
k f g g' : α → β
inst✝² : TopologicalSpace β
inst✝¹ : Field β
inst✝ : ContinuousMul β
c : β
hc0 : c ≠ 0
h : SuperpolynomialDecay l k fun n => c * f n
x : α
⊢ c⁻¹ * (c * f x) = f x
[PROOFSTEP]
simp [← mul_assoc, inv_mul_cancel hc0]
[GOAL]
α : Type u_1
β : Type u_2
l : Filter α
k f g g' : α → β
inst✝² : TopologicalSpace β
inst✝¹ : LinearOrderedField β
inst✝ : OrderTopology β
hk : Tendsto k l atTop
⊢ SuperpolynomialDecay l k f ↔ ∀ (z : ℕ), IsBoundedUnder (fun x x_1 => x ≤ x_1) l fun a => |k a ^ z * f a|
[PROOFSTEP]
refine'
  ⟨fun h z => Tendsto.isBoundedUnder_le (Tendsto.abs (h z)), fun h =>
    (superpolynomialDecay_iff_abs_tendsto_zero l k f).2 fun z => _⟩
[GOAL]
α : Type u_1
β : Type u_2
l : Filter α
k f g g' : α → β
inst✝² : TopologicalSpace β
inst✝¹ : LinearOrderedField β
inst✝ : OrderTopology β
hk : Tendsto k l atTop
h : ∀ (z : ℕ), IsBoundedUnder (fun x x_1 => x ≤ x_1) l fun a => |k a ^ z * f a|
z : ℕ
⊢ Tendsto (fun a => |k a ^ z * f a|) l (𝓝 0)
[PROOFSTEP]
obtain ⟨m, hm⟩ := h (z + 1)
[GOAL]
case intro
α : Type u_1
β : Type u_2
l : Filter α
k f g g' : α → β
inst✝² : TopologicalSpace β
inst✝¹ : LinearOrderedField β
inst✝ : OrderTopology β
hk : Tendsto k l atTop
h : ∀ (z : ℕ), IsBoundedUnder (fun x x_1 => x ≤ x_1) l fun a => |k a ^ z * f a|
z : ℕ
m : β
hm : ∀ᶠ (x : β) in Filter.map (fun a => |k a ^ (z + 1) * f a|) l, (fun x x_1 => x ≤ x_1) x m
⊢ Tendsto (fun a => |k a ^ z * f a|) l (𝓝 0)
[PROOFSTEP]
have h1 : Tendsto (fun _ : α => (0 : β)) l (𝓝 0) := tendsto_const_nhds
[GOAL]
case intro
α : Type u_1
β : Type u_2
l : Filter α
k f g g' : α → β
inst✝² : TopologicalSpace β
inst✝¹ : LinearOrderedField β
inst✝ : OrderTopology β
hk : Tendsto k l atTop
h : ∀ (z : ℕ), IsBoundedUnder (fun x x_1 => x ≤ x_1) l fun a => |k a ^ z * f a|
z : ℕ
m : β
hm : ∀ᶠ (x : β) in Filter.map (fun a => |k a ^ (z + 1) * f a|) l, (fun x x_1 => x ≤ x_1) x m
h1 : Tendsto (fun x => 0) l (𝓝 0)
⊢ Tendsto (fun a => |k a ^ z * f a|) l (𝓝 0)
[PROOFSTEP]
have h2 : Tendsto (fun a : α => |(k a)⁻¹| * m) l (𝓝 0) :=
  zero_mul m ▸ Tendsto.mul_const m ((tendsto_zero_iff_abs_tendsto_zero _).1 hk.inv_tendsto_atTop)
[GOAL]
case intro
α : Type u_1
β : Type u_2
l : Filter α
k f g g' : α → β
inst✝² : TopologicalSpace β
inst✝¹ : LinearOrderedField β
inst✝ : OrderTopology β
hk : Tendsto k l atTop
h : ∀ (z : ℕ), IsBoundedUnder (fun x x_1 => x ≤ x_1) l fun a => |k a ^ z * f a|
z : ℕ
m : β
hm : ∀ᶠ (x : β) in Filter.map (fun a => |k a ^ (z + 1) * f a|) l, (fun x x_1 => x ≤ x_1) x m
h1 : Tendsto (fun x => 0) l (𝓝 0)
h2 : Tendsto (fun a => |(k a)⁻¹| * m) l (𝓝 0)
⊢ Tendsto (fun a => |k a ^ z * f a|) l (𝓝 0)
[PROOFSTEP]
refine'
  tendsto_of_tendsto_of_tendsto_of_le_of_le' h1 h2 (eventually_of_forall fun x => abs_nonneg _)
    ((eventually_map.1 hm).mp _)
[GOAL]
case intro
α : Type u_1
β : Type u_2
l : Filter α
k f g g' : α → β
inst✝² : TopologicalSpace β
inst✝¹ : LinearOrderedField β
inst✝ : OrderTopology β
hk : Tendsto k l atTop
h : ∀ (z : ℕ), IsBoundedUnder (fun x x_1 => x ≤ x_1) l fun a => |k a ^ z * f a|
z : ℕ
m : β
hm : ∀ᶠ (x : β) in Filter.map (fun a => |k a ^ (z + 1) * f a|) l, (fun x x_1 => x ≤ x_1) x m
h1 : Tendsto (fun x => 0) l (𝓝 0)
h2 : Tendsto (fun a => |(k a)⁻¹| * m) l (𝓝 0)
⊢ ∀ᶠ (x : α) in l, (fun x x_1 => x ≤ x_1) |k x ^ (z + 1) * f x| m → |k x ^ z * f x| ≤ |(k x)⁻¹| * m
[PROOFSTEP]
refine' (hk.eventually_ne_atTop 0).mono fun x hk0 hx => _
[GOAL]
case intro
α : Type u_1
β : Type u_2
l : Filter α
k f g g' : α → β
inst✝² : TopologicalSpace β
inst✝¹ : LinearOrderedField β
inst✝ : OrderTopology β
hk : Tendsto k l atTop
h : ∀ (z : ℕ), IsBoundedUnder (fun x x_1 => x ≤ x_1) l fun a => |k a ^ z * f a|
z : ℕ
m : β
hm : ∀ᶠ (x : β) in Filter.map (fun a => |k a ^ (z + 1) * f a|) l, (fun x x_1 => x ≤ x_1) x m
h1 : Tendsto (fun x => 0) l (𝓝 0)
h2 : Tendsto (fun a => |(k a)⁻¹| * m) l (𝓝 0)
x : α
hk0 : k x ≠ 0
hx : (fun x x_1 => x ≤ x_1) |k x ^ (z + 1) * f x| m
⊢ |k x ^ z * f x| ≤ |(k x)⁻¹| * m
[PROOFSTEP]
refine' Eq.trans_le _ (mul_le_mul_of_nonneg_left hx <| abs_nonneg (k x)⁻¹)
[GOAL]
case intro
α : Type u_1
β : Type u_2
l : Filter α
k f g g' : α → β
inst✝² : TopologicalSpace β
inst✝¹ : LinearOrderedField β
inst✝ : OrderTopology β
hk : Tendsto k l atTop
h : ∀ (z : ℕ), IsBoundedUnder (fun x x_1 => x ≤ x_1) l fun a => |k a ^ z * f a|
z : ℕ
m : β
hm : ∀ᶠ (x : β) in Filter.map (fun a => |k a ^ (z + 1) * f a|) l, (fun x x_1 => x ≤ x_1) x m
h1 : Tendsto (fun x => 0) l (𝓝 0)
h2 : Tendsto (fun a => |(k a)⁻¹| * m) l (𝓝 0)
x : α
hk0 : k x ≠ 0
hx : (fun x x_1 => x ≤ x_1) |k x ^ (z + 1) * f x| m
⊢ |k x ^ z * f x| = |(k x)⁻¹| * |k x ^ (z + 1) * f x|
[PROOFSTEP]
rw [← abs_mul, ← mul_assoc, pow_succ, ← mul_assoc, inv_mul_cancel hk0, one_mul]
[GOAL]
α : Type u_1
β : Type u_2
l : Filter α
k f g g' : α → β
inst✝² : TopologicalSpace β
inst✝¹ : LinearOrderedField β
inst✝ : OrderTopology β
hk : Tendsto k l atTop
⊢ SuperpolynomialDecay l k f ↔ ∀ (z : ℤ), Tendsto (fun a => k a ^ z * f a) l (𝓝 0)
[PROOFSTEP]
refine' ⟨fun h z => _, fun h n => by simpa only [zpow_ofNat] using h (n : ℤ)⟩
[GOAL]
α : Type u_1
β : Type u_2
l : Filter α
k f g g' : α → β
inst✝² : TopologicalSpace β
inst✝¹ : LinearOrderedField β
inst✝ : OrderTopology β
hk : Tendsto k l atTop
h : ∀ (z : ℤ), Tendsto (fun a => k a ^ z * f a) l (𝓝 0)
n : ℕ
⊢ Tendsto (fun a => k a ^ n * f a) l (𝓝 0)
[PROOFSTEP]
simpa only [zpow_ofNat] using h (n : ℤ)
[GOAL]
α : Type u_1
β : Type u_2
l : Filter α
k f g g' : α → β
inst✝² : TopologicalSpace β
inst✝¹ : LinearOrderedField β
inst✝ : OrderTopology β
hk : Tendsto k l atTop
h : SuperpolynomialDecay l k f
z : ℤ
⊢ Tendsto (fun a => k a ^ z * f a) l (𝓝 0)
[PROOFSTEP]
by_cases hz : 0 ≤ z
[GOAL]
case pos
α : Type u_1
β : Type u_2
l : Filter α
k f g g' : α → β
inst✝² : TopologicalSpace β
inst✝¹ : LinearOrderedField β
inst✝ : OrderTopology β
hk : Tendsto k l atTop
h : SuperpolynomialDecay l k f
z : ℤ
hz : 0 ≤ z
⊢ Tendsto (fun a => k a ^ z * f a) l (𝓝 0)
[PROOFSTEP]
unfold Tendsto
[GOAL]
case pos
α : Type u_1
β : Type u_2
l : Filter α
k f g g' : α → β
inst✝² : TopologicalSpace β
inst✝¹ : LinearOrderedField β
inst✝ : OrderTopology β
hk : Tendsto k l atTop
h : SuperpolynomialDecay l k f
z : ℤ
hz : 0 ≤ z
⊢ Filter.map (fun a => k a ^ z * f a) l ≤ 𝓝 0
[PROOFSTEP]
lift z to ℕ using hz
[GOAL]
case pos.intro
α : Type u_1
β : Type u_2
l : Filter α
k f g g' : α → β
inst✝² : TopologicalSpace β
inst✝¹ : LinearOrderedField β
inst✝ : OrderTopology β
hk : Tendsto k l atTop
h : SuperpolynomialDecay l k f
z : ℕ
⊢ Filter.map (fun a => k a ^ ↑z * f a) l ≤ 𝓝 0
[PROOFSTEP]
simpa using h z
[GOAL]
case neg
α : Type u_1
β : Type u_2
l : Filter α
k f g g' : α → β
inst✝² : TopologicalSpace β
inst✝¹ : LinearOrderedField β
inst✝ : OrderTopology β
hk : Tendsto k l atTop
h : SuperpolynomialDecay l k f
z : ℤ
hz : ¬0 ≤ z
⊢ Tendsto (fun a => k a ^ z * f a) l (𝓝 0)
[PROOFSTEP]
have : Tendsto (fun a => k a ^ z) l (𝓝 0) := Tendsto.comp (tendsto_zpow_atTop_zero (not_le.1 hz)) hk
[GOAL]
case neg
α : Type u_1
β : Type u_2
l : Filter α
k f g g' : α → β
inst✝² : TopologicalSpace β
inst✝¹ : LinearOrderedField β
inst✝ : OrderTopology β
hk : Tendsto k l atTop
h : SuperpolynomialDecay l k f
z : ℤ
hz : ¬0 ≤ z
this : Tendsto (fun a => k a ^ z) l (𝓝 0)
⊢ Tendsto (fun a => k a ^ z * f a) l (𝓝 0)
[PROOFSTEP]
have h : Tendsto f l (𝓝 0) := by simpa using h 0
[GOAL]
α : Type u_1
β : Type u_2
l : Filter α
k f g g' : α → β
inst✝² : TopologicalSpace β
inst✝¹ : LinearOrderedField β
inst✝ : OrderTopology β
hk : Tendsto k l atTop
h : SuperpolynomialDecay l k f
z : ℤ
hz : ¬0 ≤ z
this : Tendsto (fun a => k a ^ z) l (𝓝 0)
⊢ Tendsto f l (𝓝 0)
[PROOFSTEP]
simpa using h 0
[GOAL]
case neg
α : Type u_1
β : Type u_2
l : Filter α
k f g g' : α → β
inst✝² : TopologicalSpace β
inst✝¹ : LinearOrderedField β
inst✝ : OrderTopology β
hk : Tendsto k l atTop
h✝ : SuperpolynomialDecay l k f
z : ℤ
hz : ¬0 ≤ z
this : Tendsto (fun a => k a ^ z) l (𝓝 0)
h : Tendsto f l (𝓝 0)
⊢ Tendsto (fun a => k a ^ z * f a) l (𝓝 0)
[PROOFSTEP]
exact zero_mul (0 : β) ▸ this.mul h
[GOAL]
α : Type u_1
β : Type u_2
l : Filter α
k f g g' : α → β
inst✝² : TopologicalSpace β
inst✝¹ : LinearOrderedField β
inst✝ : OrderTopology β
hk : Tendsto k l atTop
hf : SuperpolynomialDecay l k f
z : ℤ
⊢ SuperpolynomialDecay l k fun a => k a ^ z * f a
[PROOFSTEP]
rw [superpolynomialDecay_iff_zpow_tendsto_zero _ hk] at hf ⊢
[GOAL]
α : Type u_1
β : Type u_2
l : Filter α
k f g g' : α → β
inst✝² : TopologicalSpace β
inst✝¹ : LinearOrderedField β
inst✝ : OrderTopology β
hk : Tendsto k l atTop
hf : ∀ (z : ℤ), Tendsto (fun a => k a ^ z * f a) l (𝓝 0)
z : ℤ
⊢ ∀ (z_1 : ℤ), Tendsto (fun a => k a ^ z_1 * (k a ^ z * f a)) l (𝓝 0)
[PROOFSTEP]
refine' fun z' => (hf <| z' + z).congr' ((hk.eventually_ne_atTop 0).mono fun x hx => _)
[GOAL]
α : Type u_1
β : Type u_2
l : Filter α
k f g g' : α → β
inst✝² : TopologicalSpace β
inst✝¹ : LinearOrderedField β
inst✝ : OrderTopology β
hk : Tendsto k l atTop
hf : ∀ (z : ℤ), Tendsto (fun a => k a ^ z * f a) l (𝓝 0)
z z' : ℤ
x : α
hx : k x ≠ 0
⊢ k x ^ (z' + z) * f x = (fun a => k a ^ z' * (k a ^ z * f a)) x
[PROOFSTEP]
simp [zpow_add₀ hx, mul_assoc, Pi.mul_apply]
[GOAL]
α : Type u_1
β : Type u_2
l : Filter α
k f g g' : α → β
inst✝² : TopologicalSpace β
inst✝¹ : LinearOrderedField β
inst✝ : OrderTopology β
hk : Tendsto k l atTop
hf : SuperpolynomialDecay l k f
⊢ SuperpolynomialDecay l k (k⁻¹ * f)
[PROOFSTEP]
simpa using hf.param_zpow_mul hk (-1)
[GOAL]
α : Type u_1
β : Type u_2
l : Filter α
k f g g' : α → β
inst✝² : TopologicalSpace β
inst✝¹ : LinearOrderedField β
inst✝ : OrderTopology β
hk : Tendsto k l atTop
h : SuperpolynomialDecay l k (k * f)
x : α
hx : k x ≠ 0
⊢ (k⁻¹ * (k * f)) x = f x
[PROOFSTEP]
simp [← mul_assoc, inv_mul_cancel hx]
[GOAL]
α : Type u_1
β : Type u_2
l : Filter α
k f g g' : α → β
inst✝² : TopologicalSpace β
inst✝¹ : LinearOrderedField β
inst✝ : OrderTopology β
hk : Tendsto k l atTop
⊢ SuperpolynomialDecay l k (f * k) ↔ SuperpolynomialDecay l k f
[PROOFSTEP]
simpa [mul_comm k] using superpolynomialDecay_param_mul_iff f hk
[GOAL]
α : Type u_1
β : Type u_2
l : Filter α
k f g g' : α → β
inst✝² : TopologicalSpace β
inst✝¹ : LinearOrderedField β
inst✝ : OrderTopology β
hk : Tendsto k l atTop
n : ℕ
⊢ SuperpolynomialDecay l k (k ^ n * f) ↔ SuperpolynomialDecay l k f
[PROOFSTEP]
induction' n with n hn
[GOAL]
case zero
α : Type u_1
β : Type u_2
l : Filter α
k f g g' : α → β
inst✝² : TopologicalSpace β
inst✝¹ : LinearOrderedField β
inst✝ : OrderTopology β
hk : Tendsto k l atTop
⊢ SuperpolynomialDecay l k (k ^ Nat.zero * f) ↔ SuperpolynomialDecay l k f
[PROOFSTEP]
simp
[GOAL]
case succ
α : Type u_1
β : Type u_2
l : Filter α
k f g g' : α → β
inst✝² : TopologicalSpace β
inst✝¹ : LinearOrderedField β
inst✝ : OrderTopology β
hk : Tendsto k l atTop
n : ℕ
hn : SuperpolynomialDecay l k (k ^ n * f) ↔ SuperpolynomialDecay l k f
⊢ SuperpolynomialDecay l k (k ^ Nat.succ n * f) ↔ SuperpolynomialDecay l k f
[PROOFSTEP]
simpa [pow_succ, ← mul_comm k, mul_assoc, superpolynomialDecay_param_mul_iff (k ^ n * f) hk] using hn
[GOAL]
α : Type u_1
β : Type u_2
l : Filter α
k f g g' : α → β
inst✝² : TopologicalSpace β
inst✝¹ : LinearOrderedField β
inst✝ : OrderTopology β
hk : Tendsto k l atTop
n : ℕ
⊢ SuperpolynomialDecay l k (f * k ^ n) ↔ SuperpolynomialDecay l k f
[PROOFSTEP]
simpa [mul_comm f] using superpolynomialDecay_param_pow_mul_iff f hk n
[GOAL]
α : Type u_1
β : Type u_2
l : Filter α
k f g g' : α → β
inst✝ : NormedLinearOrderedField β
⊢ (∀ (n : ℕ), Tendsto (fun a => ‖k a ^ n * f a‖) l (𝓝 0)) ↔ SuperpolynomialDecay l (fun a => ‖k a‖) fun a => ‖f a‖
[PROOFSTEP]
simp [SuperpolynomialDecay]
[GOAL]
α : Type u_1
β : Type u_2
l : Filter α
k f g g' : α → β
inst✝¹ : NormedLinearOrderedField β
inst✝ : OrderTopology β
hk : Tendsto k l atTop
⊢ SuperpolynomialDecay l k f ↔ ∀ (z : ℤ), f =O[l] fun a => k a ^ z
[PROOFSTEP]
refine' (superpolynomialDecay_iff_zpow_tendsto_zero f hk).trans _
[GOAL]
α : Type u_1
β : Type u_2
l : Filter α
k f g g' : α → β
inst✝¹ : NormedLinearOrderedField β
inst✝ : OrderTopology β
hk : Tendsto k l atTop
⊢ (∀ (z : ℤ), Tendsto (fun a => k a ^ z * f a) l (𝓝 0)) ↔ ∀ (z : ℤ), f =O[l] fun a => k a ^ z
[PROOFSTEP]
have hk0 : ∀ᶠ x in l, k x ≠ 0 := hk.eventually_ne_atTop 0
[GOAL]
α : Type u_1
β : Type u_2
l : Filter α
k f g g' : α → β
inst✝¹ : NormedLinearOrderedField β
inst✝ : OrderTopology β
hk : Tendsto k l atTop
hk0 : ∀ᶠ (x : α) in l, k x ≠ 0
⊢ (∀ (z : ℤ), Tendsto (fun a => k a ^ z * f a) l (𝓝 0)) ↔ ∀ (z : ℤ), f =O[l] fun a => k a ^ z
[PROOFSTEP]
refine' ⟨fun h z => _, fun h z => _⟩
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
l : Filter α
k f g g' : α → β
inst✝¹ : NormedLinearOrderedField β
inst✝ : OrderTopology β
hk : Tendsto k l atTop
hk0 : ∀ᶠ (x : α) in l, k x ≠ 0
h : ∀ (z : ℤ), Tendsto (fun a => k a ^ z * f a) l (𝓝 0)
z : ℤ
⊢ f =O[l] fun a => k a ^ z
[PROOFSTEP]
refine' isBigO_of_div_tendsto_nhds (hk0.mono fun x hx hxz => absurd (zpow_eq_zero hxz) hx) 0 _
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
l : Filter α
k f g g' : α → β
inst✝¹ : NormedLinearOrderedField β
inst✝ : OrderTopology β
hk : Tendsto k l atTop
hk0 : ∀ᶠ (x : α) in l, k x ≠ 0
h : ∀ (z : ℤ), Tendsto (fun a => k a ^ z * f a) l (𝓝 0)
z : ℤ
⊢ Tendsto (f / fun a => k a ^ z) l (𝓝 0)
[PROOFSTEP]
have : (fun a : α => k a ^ z)⁻¹ = fun a : α => k a ^ (-z) := funext fun x => by simp
[GOAL]
α : Type u_1
β : Type u_2
l : Filter α
k f g g' : α → β
inst✝¹ : NormedLinearOrderedField β
inst✝ : OrderTopology β
hk : Tendsto k l atTop
hk0 : ∀ᶠ (x : α) in l, k x ≠ 0
h : ∀ (z : ℤ), Tendsto (fun a => k a ^ z * f a) l (𝓝 0)
z : ℤ
x : α
⊢ (fun a => k a ^ z)⁻¹ x = k x ^ (-z)
[PROOFSTEP]
simp
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
l : Filter α
k f g g' : α → β
inst✝¹ : NormedLinearOrderedField β
inst✝ : OrderTopology β
hk : Tendsto k l atTop
hk0 : ∀ᶠ (x : α) in l, k x ≠ 0
h : ∀ (z : ℤ), Tendsto (fun a => k a ^ z * f a) l (𝓝 0)
z : ℤ
this : (fun a => k a ^ z)⁻¹ = fun a => k a ^ (-z)
⊢ Tendsto (f / fun a => k a ^ z) l (𝓝 0)
[PROOFSTEP]
rw [div_eq_mul_inv, mul_comm f, this]
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
l : Filter α
k f g g' : α → β
inst✝¹ : NormedLinearOrderedField β
inst✝ : OrderTopology β
hk : Tendsto k l atTop
hk0 : ∀ᶠ (x : α) in l, k x ≠ 0
h : ∀ (z : ℤ), Tendsto (fun a => k a ^ z * f a) l (𝓝 0)
z : ℤ
this : (fun a => k a ^ z)⁻¹ = fun a => k a ^ (-z)
⊢ Tendsto ((fun a => k a ^ (-z)) * f) l (𝓝 0)
[PROOFSTEP]
exact h (-z)
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
l : Filter α
k f g g' : α → β
inst✝¹ : NormedLinearOrderedField β
inst✝ : OrderTopology β
hk : Tendsto k l atTop
hk0 : ∀ᶠ (x : α) in l, k x ≠ 0
h : ∀ (z : ℤ), f =O[l] fun a => k a ^ z
z : ℤ
⊢ Tendsto (fun a => k a ^ z * f a) l (𝓝 0)
[PROOFSTEP]
suffices : (fun a : α => k a ^ z * f a) =O[l] fun a : α => (k a)⁻¹
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
l : Filter α
k f g g' : α → β
inst✝¹ : NormedLinearOrderedField β
inst✝ : OrderTopology β
hk : Tendsto k l atTop
hk0 : ∀ᶠ (x : α) in l, k x ≠ 0
h : ∀ (z : ℤ), f =O[l] fun a => k a ^ z
z : ℤ
this : (fun a => k a ^ z * f a) =O[l] fun a => (k a)⁻¹
⊢ Tendsto (fun a => k a ^ z * f a) l (𝓝 0)
case this
α : Type u_1
β : Type u_2
l : Filter α
k f g g' : α → β
inst✝¹ : NormedLinearOrderedField β
inst✝ : OrderTopology β
hk : Tendsto k l atTop
hk0 : ∀ᶠ (x : α) in l, k x ≠ 0
h : ∀ (z : ℤ), f =O[l] fun a => k a ^ z
z : ℤ
⊢ (fun a => k a ^ z * f a) =O[l] fun a => (k a)⁻¹
[PROOFSTEP]
exact IsBigO.trans_tendsto this hk.inv_tendsto_atTop
[GOAL]
case this
α : Type u_1
β : Type u_2
l : Filter α
k f g g' : α → β
inst✝¹ : NormedLinearOrderedField β
inst✝ : OrderTopology β
hk : Tendsto k l atTop
hk0 : ∀ᶠ (x : α) in l, k x ≠ 0
h : ∀ (z : ℤ), f =O[l] fun a => k a ^ z
z : ℤ
⊢ (fun a => k a ^ z * f a) =O[l] fun a => (k a)⁻¹
[PROOFSTEP]
refine' ((isBigO_refl (fun a => k a ^ z) l).mul (h (-(z + 1)))).trans (IsBigO.of_bound 1 <| hk0.mono fun a ha0 => _)
[GOAL]
case this
α : Type u_1
β : Type u_2
l : Filter α
k f g g' : α → β
inst✝¹ : NormedLinearOrderedField β
inst✝ : OrderTopology β
hk : Tendsto k l atTop
hk0 : ∀ᶠ (x : α) in l, k x ≠ 0
h : ∀ (z : ℤ), f =O[l] fun a => k a ^ z
z : ℤ
a : α
ha0 : k a ≠ 0
⊢ ‖k a ^ z * k a ^ (-(z + 1))‖ ≤ 1 * ‖(k a)⁻¹‖
[PROOFSTEP]
simp only [one_mul, neg_add z 1, zpow_add₀ ha0, ← mul_assoc, zpow_neg, mul_inv_cancel (zpow_ne_zero z ha0), zpow_one]
[GOAL]
case this
α : Type u_1
β : Type u_2
l : Filter α
k f g g' : α → β
inst✝¹ : NormedLinearOrderedField β
inst✝ : OrderTopology β
hk : Tendsto k l atTop
hk0 : ∀ᶠ (x : α) in l, k x ≠ 0
h : ∀ (z : ℤ), f =O[l] fun a => k a ^ z
z : ℤ
a : α
ha0 : k a ≠ 0
⊢ ‖(k a)⁻¹‖ ≤ ‖(k a)⁻¹‖
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
l : Filter α
k f g g' : α → β
inst✝¹ : NormedLinearOrderedField β
inst✝ : OrderTopology β
hk : Tendsto k l atTop
⊢ SuperpolynomialDecay l k f ↔ ∀ (z : ℤ), f =o[l] fun a => k a ^ z
[PROOFSTEP]
refine' ⟨fun h z => _, fun h => (superpolynomialDecay_iff_isBigO f hk).2 fun z => (h z).isBigO⟩
[GOAL]
α : Type u_1
β : Type u_2
l : Filter α
k f g g' : α → β
inst✝¹ : NormedLinearOrderedField β
inst✝ : OrderTopology β
hk : Tendsto k l atTop
h : SuperpolynomialDecay l k f
z : ℤ
⊢ f =o[l] fun a => k a ^ z
[PROOFSTEP]
have hk0 : ∀ᶠ x in l, k x ≠ 0 := hk.eventually_ne_atTop 0
[GOAL]
α : Type u_1
β : Type u_2
l : Filter α
k f g g' : α → β
inst✝¹ : NormedLinearOrderedField β
inst✝ : OrderTopology β
hk : Tendsto k l atTop
h : SuperpolynomialDecay l k f
z : ℤ
hk0 : ∀ᶠ (x : α) in l, k x ≠ 0
⊢ f =o[l] fun a => k a ^ z
[PROOFSTEP]
have : (fun _ : α => (1 : β)) =o[l] k :=
  isLittleO_of_tendsto' (hk0.mono fun x hkx hkx' => absurd hkx' hkx) (by simpa using hk.inv_tendsto_atTop)
[GOAL]
α : Type u_1
β : Type u_2
l : Filter α
k f g g' : α → β
inst✝¹ : NormedLinearOrderedField β
inst✝ : OrderTopology β
hk : Tendsto k l atTop
h : SuperpolynomialDecay l k f
z : ℤ
hk0 : ∀ᶠ (x : α) in l, k x ≠ 0
⊢ Tendsto (fun x => 1 / k x) l (𝓝 0)
[PROOFSTEP]
simpa using hk.inv_tendsto_atTop
[GOAL]
α : Type u_1
β : Type u_2
l : Filter α
k f g g' : α → β
inst✝¹ : NormedLinearOrderedField β
inst✝ : OrderTopology β
hk : Tendsto k l atTop
h : SuperpolynomialDecay l k f
z : ℤ
hk0 : ∀ᶠ (x : α) in l, k x ≠ 0
this : (fun x => 1) =o[l] k
⊢ f =o[l] fun a => k a ^ z
[PROOFSTEP]
have : f =o[l] fun x : α => k x * k x ^ (z - 1) := by
  simpa using this.mul_isBigO ((superpolynomialDecay_iff_isBigO f hk).1 h <| z - 1)
[GOAL]
α : Type u_1
β : Type u_2
l : Filter α
k f g g' : α → β
inst✝¹ : NormedLinearOrderedField β
inst✝ : OrderTopology β
hk : Tendsto k l atTop
h : SuperpolynomialDecay l k f
z : ℤ
hk0 : ∀ᶠ (x : α) in l, k x ≠ 0
this : (fun x => 1) =o[l] k
⊢ f =o[l] fun x => k x * k x ^ (z - 1)
[PROOFSTEP]
simpa using this.mul_isBigO ((superpolynomialDecay_iff_isBigO f hk).1 h <| z - 1)
[GOAL]
α : Type u_1
β : Type u_2
l : Filter α
k f g g' : α → β
inst✝¹ : NormedLinearOrderedField β
inst✝ : OrderTopology β
hk : Tendsto k l atTop
h : SuperpolynomialDecay l k f
z : ℤ
hk0 : ∀ᶠ (x : α) in l, k x ≠ 0
this✝ : (fun x => 1) =o[l] k
this : f =o[l] fun x => k x * k x ^ (z - 1)
⊢ f =o[l] fun a => k a ^ z
[PROOFSTEP]
refine' this.trans_isBigO (IsBigO.of_bound 1 (hk0.mono fun x hkx => le_of_eq _))
[GOAL]
α : Type u_1
β : Type u_2
l : Filter α
k f g g' : α → β
inst✝¹ : NormedLinearOrderedField β
inst✝ : OrderTopology β
hk : Tendsto k l atTop
h : SuperpolynomialDecay l k f
z : ℤ
hk0 : ∀ᶠ (x : α) in l, k x ≠ 0
this✝ : (fun x => 1) =o[l] k
this : f =o[l] fun x => k x * k x ^ (z - 1)
x : α
hkx : k x ≠ 0
⊢ ‖k x * k x ^ (z - 1)‖ = 1 * ‖k x ^ z‖
[PROOFSTEP]
rw [one_mul, zpow_sub_one₀ hkx, mul_comm (k x), mul_assoc, inv_mul_cancel hkx, mul_one]