[GOAL]
R : Type u_1
𝕜 : Type u_2
inst✝³ : NonUnitalNonAssocRing R
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace R
inst✝ : TopologicalAddGroup R
norm : R → 𝕜
norm_nonneg : ∀ (x : R), 0 ≤ norm x
norm_mul_le : ∀ (x y : R), norm (x * y) ≤ norm x * norm y
nhds_basis : HasBasis (𝓝 0) (fun x => 0 < x) fun ε => {x | norm x < ε}
⊢ TopologicalRing R
[PROOFSTEP]
have h0 : ∀ f : R → R, ∀ c ≥ (0 : 𝕜), (∀ x, norm (f x) ≤ c * norm x) → Tendsto f (𝓝 0) (𝓝 0)
[GOAL]
case h0
R : Type u_1
𝕜 : Type u_2
inst✝³ : NonUnitalNonAssocRing R
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace R
inst✝ : TopologicalAddGroup R
norm : R → 𝕜
norm_nonneg : ∀ (x : R), 0 ≤ norm x
norm_mul_le : ∀ (x y : R), norm (x * y) ≤ norm x * norm y
nhds_basis : HasBasis (𝓝 0) (fun x => 0 < x) fun ε => {x | norm x < ε}
⊢ ∀ (f : R → R) (c : 𝕜), c ≥ 0 → (∀ (x : R), norm (f x) ≤ c * norm x) → Tendsto f (𝓝 0) (𝓝 0)
[PROOFSTEP]
refine fun f c c0 hf ↦ (nhds_basis.tendsto_iff nhds_basis).2 fun ε ε0 ↦ ?_
[GOAL]
case h0
R : Type u_1
𝕜 : Type u_2
inst✝³ : NonUnitalNonAssocRing R
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace R
inst✝ : TopologicalAddGroup R
norm : R → 𝕜
norm_nonneg : ∀ (x : R), 0 ≤ norm x
norm_mul_le : ∀ (x y : R), norm (x * y) ≤ norm x * norm y
nhds_basis : HasBasis (𝓝 0) (fun x => 0 < x) fun ε => {x | norm x < ε}
f : R → R
c : 𝕜
c0 : c ≥ 0
hf : ∀ (x : R), norm (f x) ≤ c * norm x
ε : 𝕜
ε0 : 0 < ε
⊢ ∃ ia, 0 < ia ∧ ∀ (x : R), x ∈ {x | norm x < ia} → f x ∈ {x | norm x < ε}
[PROOFSTEP]
rcases exists_pos_mul_lt ε0 c with ⟨δ, δ0, hδ⟩
[GOAL]
case h0.intro.intro
R : Type u_1
𝕜 : Type u_2
inst✝³ : NonUnitalNonAssocRing R
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace R
inst✝ : TopologicalAddGroup R
norm : R → 𝕜
norm_nonneg : ∀ (x : R), 0 ≤ norm x
norm_mul_le : ∀ (x y : R), norm (x * y) ≤ norm x * norm y
nhds_basis : HasBasis (𝓝 0) (fun x => 0 < x) fun ε => {x | norm x < ε}
f : R → R
c : 𝕜
c0 : c ≥ 0
hf : ∀ (x : R), norm (f x) ≤ c * norm x
ε : 𝕜
ε0 : 0 < ε
δ : 𝕜
δ0 : 0 < δ
hδ : c * δ < ε
⊢ ∃ ia, 0 < ia ∧ ∀ (x : R), x ∈ {x | norm x < ia} → f x ∈ {x | norm x < ε}
[PROOFSTEP]
refine ⟨δ, δ0, fun x hx ↦ (hf _).trans_lt ?_⟩
[GOAL]
case h0.intro.intro
R : Type u_1
𝕜 : Type u_2
inst✝³ : NonUnitalNonAssocRing R
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace R
inst✝ : TopologicalAddGroup R
norm : R → 𝕜
norm_nonneg : ∀ (x : R), 0 ≤ norm x
norm_mul_le : ∀ (x y : R), norm (x * y) ≤ norm x * norm y
nhds_basis : HasBasis (𝓝 0) (fun x => 0 < x) fun ε => {x | norm x < ε}
f : R → R
c : 𝕜
c0 : c ≥ 0
hf : ∀ (x : R), norm (f x) ≤ c * norm x
ε : 𝕜
ε0 : 0 < ε
δ : 𝕜
δ0 : 0 < δ
hδ : c * δ < ε
x : R
hx : x ∈ {x | norm x < δ}
⊢ c * norm x < ε
[PROOFSTEP]
exact (mul_le_mul_of_nonneg_left (le_of_lt hx) c0).trans_lt hδ
[GOAL]
R : Type u_1
𝕜 : Type u_2
inst✝³ : NonUnitalNonAssocRing R
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace R
inst✝ : TopologicalAddGroup R
norm : R → 𝕜
norm_nonneg : ∀ (x : R), 0 ≤ norm x
norm_mul_le : ∀ (x y : R), norm (x * y) ≤ norm x * norm y
nhds_basis : HasBasis (𝓝 0) (fun x => 0 < x) fun ε => {x | norm x < ε}
h0 : ∀ (f : R → R) (c : 𝕜), c ≥ 0 → (∀ (x : R), norm (f x) ≤ c * norm x) → Tendsto f (𝓝 0) (𝓝 0)
⊢ TopologicalRing R
[PROOFSTEP]
apply TopologicalRing.of_addGroup_of_nhds_zero
[GOAL]
case hmul
R : Type u_1
𝕜 : Type u_2
inst✝³ : NonUnitalNonAssocRing R
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace R
inst✝ : TopologicalAddGroup R
norm : R → 𝕜
norm_nonneg : ∀ (x : R), 0 ≤ norm x
norm_mul_le : ∀ (x y : R), norm (x * y) ≤ norm x * norm y
nhds_basis : HasBasis (𝓝 0) (fun x => 0 < x) fun ε => {x | norm x < ε}
h0 : ∀ (f : R → R) (c : 𝕜), c ≥ 0 → (∀ (x : R), norm (f x) ≤ c * norm x) → Tendsto f (𝓝 0) (𝓝 0)
⊢ Tendsto (uncurry fun x x_1 => x * x_1) (𝓝 0 ×ˢ 𝓝 0) (𝓝 0)
case hmul_left
R : Type u_1
𝕜 : Type u_2
inst✝³ : NonUnitalNonAssocRing R
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace R
inst✝ : TopologicalAddGroup R
norm : R → 𝕜
norm_nonneg : ∀ (x : R), 0 ≤ norm x
norm_mul_le : ∀ (x y : R), norm (x * y) ≤ norm x * norm y
nhds_basis : HasBasis (𝓝 0) (fun x => 0 < x) fun ε => {x | norm x < ε}
h0 : ∀ (f : R → R) (c : 𝕜), c ≥ 0 → (∀ (x : R), norm (f x) ≤ c * norm x) → Tendsto f (𝓝 0) (𝓝 0)
⊢ ∀ (x₀ : R), Tendsto (fun x => x₀ * x) (𝓝 0) (𝓝 0)
case hmul_right
R : Type u_1
𝕜 : Type u_2
inst✝³ : NonUnitalNonAssocRing R
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace R
inst✝ : TopologicalAddGroup R
norm : R → 𝕜
norm_nonneg : ∀ (x : R), 0 ≤ norm x
norm_mul_le : ∀ (x y : R), norm (x * y) ≤ norm x * norm y
nhds_basis : HasBasis (𝓝 0) (fun x => 0 < x) fun ε => {x | norm x < ε}
h0 : ∀ (f : R → R) (c : 𝕜), c ≥ 0 → (∀ (x : R), norm (f x) ≤ c * norm x) → Tendsto f (𝓝 0) (𝓝 0)
⊢ ∀ (x₀ : R), Tendsto (fun x => x * x₀) (𝓝 0) (𝓝 0)
[PROOFSTEP]
case hmul =>
  refine ((nhds_basis.prod nhds_basis).tendsto_iff nhds_basis).2 fun ε ε0 ↦ ?_
  refine ⟨(1, ε), ⟨one_pos, ε0⟩, fun (x, y) ⟨hx, hy⟩ => ?_⟩
  simp only [sub_zero] at *
  calc
    norm (x * y) ≤ norm x * norm y := norm_mul_le _ _
    _ < ε := mul_lt_of_le_one_of_lt_of_nonneg hx.le hy (norm_nonneg _)
[GOAL]
R : Type u_1
𝕜 : Type u_2
inst✝³ : NonUnitalNonAssocRing R
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace R
inst✝ : TopologicalAddGroup R
norm : R → 𝕜
norm_nonneg : ∀ (x : R), 0 ≤ norm x
norm_mul_le : ∀ (x y : R), norm (x * y) ≤ norm x * norm y
nhds_basis : HasBasis (𝓝 0) (fun x => 0 < x) fun ε => {x | norm x < ε}
h0 : ∀ (f : R → R) (c : 𝕜), c ≥ 0 → (∀ (x : R), norm (f x) ≤ c * norm x) → Tendsto f (𝓝 0) (𝓝 0)
⊢ Tendsto (uncurry fun x x_1 => x * x_1) (𝓝 0 ×ˢ 𝓝 0) (𝓝 0)
[PROOFSTEP]
case hmul =>
  refine ((nhds_basis.prod nhds_basis).tendsto_iff nhds_basis).2 fun ε ε0 ↦ ?_
  refine ⟨(1, ε), ⟨one_pos, ε0⟩, fun (x, y) ⟨hx, hy⟩ => ?_⟩
  simp only [sub_zero] at *
  calc
    norm (x * y) ≤ norm x * norm y := norm_mul_le _ _
    _ < ε := mul_lt_of_le_one_of_lt_of_nonneg hx.le hy (norm_nonneg _)
[GOAL]
R : Type u_1
𝕜 : Type u_2
inst✝³ : NonUnitalNonAssocRing R
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace R
inst✝ : TopologicalAddGroup R
norm : R → 𝕜
norm_nonneg : ∀ (x : R), 0 ≤ norm x
norm_mul_le : ∀ (x y : R), norm (x * y) ≤ norm x * norm y
nhds_basis : HasBasis (𝓝 0) (fun x => 0 < x) fun ε => {x | norm x < ε}
h0 : ∀ (f : R → R) (c : 𝕜), c ≥ 0 → (∀ (x : R), norm (f x) ≤ c * norm x) → Tendsto f (𝓝 0) (𝓝 0)
⊢ Tendsto (uncurry fun x x_1 => x * x_1) (𝓝 0 ×ˢ 𝓝 0) (𝓝 0)
[PROOFSTEP]
refine ((nhds_basis.prod nhds_basis).tendsto_iff nhds_basis).2 fun ε ε0 ↦ ?_
[GOAL]
R : Type u_1
𝕜 : Type u_2
inst✝³ : NonUnitalNonAssocRing R
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace R
inst✝ : TopologicalAddGroup R
norm : R → 𝕜
norm_nonneg : ∀ (x : R), 0 ≤ norm x
norm_mul_le : ∀ (x y : R), norm (x * y) ≤ norm x * norm y
nhds_basis : HasBasis (𝓝 0) (fun x => 0 < x) fun ε => {x | norm x < ε}
h0 : ∀ (f : R → R) (c : 𝕜), c ≥ 0 → (∀ (x : R), norm (f x) ≤ c * norm x) → Tendsto f (𝓝 0) (𝓝 0)
ε : 𝕜
ε0 : 0 < ε
⊢ ∃ ia,
    (0 < ia.fst ∧ 0 < ia.snd) ∧
      ∀ (x : R × R),
        x ∈ {x | norm x < ia.fst} ×ˢ {x | norm x < ia.snd} → uncurry (fun x x_1 => x * x_1) x ∈ {x | norm x < ε}
[PROOFSTEP]
refine ⟨(1, ε), ⟨one_pos, ε0⟩, fun (x, y) ⟨hx, hy⟩ => ?_⟩
[GOAL]
R : Type u_1
𝕜 : Type u_2
inst✝³ : NonUnitalNonAssocRing R
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace R
inst✝ : TopologicalAddGroup R
norm : R → 𝕜
norm_nonneg : ∀ (x : R), 0 ≤ norm x
norm_mul_le : ∀ (x y : R), norm (x * y) ≤ norm x * norm y
nhds_basis : HasBasis (𝓝 0) (fun x => 0 < x) fun ε => {x | norm x < ε}
h0 : ∀ (f : R → R) (c : 𝕜), c ≥ 0 → (∀ (x : R), norm (f x) ≤ c * norm x) → Tendsto f (𝓝 0) (𝓝 0)
ε : 𝕜
ε0 : 0 < ε
x✝¹ : R × R
x y : R
x✝ : (x, y) ∈ {x | norm x < (1, ε).fst} ×ˢ {x | norm x < (1, ε).snd}
hx : (x, y).fst ∈ {x | norm x < (1, ε).fst}
hy : (x, y).snd ∈ {x | norm x < (1, ε).snd}
⊢ uncurry (fun x x_1 => x * x_1) (x, y) ∈ {x | norm x < ε}
[PROOFSTEP]
simp only [sub_zero] at *
[GOAL]
R : Type u_1
𝕜 : Type u_2
inst✝³ : NonUnitalNonAssocRing R
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace R
inst✝ : TopologicalAddGroup R
norm : R → 𝕜
norm_nonneg : ∀ (x : R), 0 ≤ norm x
norm_mul_le : ∀ (x y : R), norm (x * y) ≤ norm x * norm y
nhds_basis : HasBasis (𝓝 0) (fun x => 0 < x) fun ε => {x | norm x < ε}
h0 : ∀ (f : R → R) (c : 𝕜), c ≥ 0 → (∀ (x : R), norm (f x) ≤ c * norm x) → Tendsto f (𝓝 0) (𝓝 0)
ε : 𝕜
ε0 : 0 < ε
x✝¹ : R × R
x y : R
x✝ : (x, y) ∈ {x | norm x < 1} ×ˢ {x | norm x < ε}
hx : x ∈ {x | norm x < 1}
hy : y ∈ {x | norm x < ε}
⊢ uncurry (fun x x_1 => x * x_1) (x, y) ∈ {x | norm x < ε}
[PROOFSTEP]
calc
  norm (x * y) ≤ norm x * norm y := norm_mul_le _ _
  _ < ε := mul_lt_of_le_one_of_lt_of_nonneg hx.le hy (norm_nonneg _)
[GOAL]
case hmul_left
R : Type u_1
𝕜 : Type u_2
inst✝³ : NonUnitalNonAssocRing R
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace R
inst✝ : TopologicalAddGroup R
norm : R → 𝕜
norm_nonneg : ∀ (x : R), 0 ≤ norm x
norm_mul_le : ∀ (x y : R), norm (x * y) ≤ norm x * norm y
nhds_basis : HasBasis (𝓝 0) (fun x => 0 < x) fun ε => {x | norm x < ε}
h0 : ∀ (f : R → R) (c : 𝕜), c ≥ 0 → (∀ (x : R), norm (f x) ≤ c * norm x) → Tendsto f (𝓝 0) (𝓝 0)
⊢ ∀ (x₀ : R), Tendsto (fun x => x₀ * x) (𝓝 0) (𝓝 0)
case hmul_right
R : Type u_1
𝕜 : Type u_2
inst✝³ : NonUnitalNonAssocRing R
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace R
inst✝ : TopologicalAddGroup R
norm : R → 𝕜
norm_nonneg : ∀ (x : R), 0 ≤ norm x
norm_mul_le : ∀ (x y : R), norm (x * y) ≤ norm x * norm y
nhds_basis : HasBasis (𝓝 0) (fun x => 0 < x) fun ε => {x | norm x < ε}
h0 : ∀ (f : R → R) (c : 𝕜), c ≥ 0 → (∀ (x : R), norm (f x) ≤ c * norm x) → Tendsto f (𝓝 0) (𝓝 0)
⊢ ∀ (x₀ : R), Tendsto (fun x => x * x₀) (𝓝 0) (𝓝 0)
[PROOFSTEP]
case hmul_left => exact fun x => h0 _ (norm x) (norm_nonneg _) (norm_mul_le x)
[GOAL]
R : Type u_1
𝕜 : Type u_2
inst✝³ : NonUnitalNonAssocRing R
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace R
inst✝ : TopologicalAddGroup R
norm : R → 𝕜
norm_nonneg : ∀ (x : R), 0 ≤ norm x
norm_mul_le : ∀ (x y : R), norm (x * y) ≤ norm x * norm y
nhds_basis : HasBasis (𝓝 0) (fun x => 0 < x) fun ε => {x | norm x < ε}
h0 : ∀ (f : R → R) (c : 𝕜), c ≥ 0 → (∀ (x : R), norm (f x) ≤ c * norm x) → Tendsto f (𝓝 0) (𝓝 0)
⊢ ∀ (x₀ : R), Tendsto (fun x => x₀ * x) (𝓝 0) (𝓝 0)
[PROOFSTEP]
case hmul_left => exact fun x => h0 _ (norm x) (norm_nonneg _) (norm_mul_le x)
[GOAL]
R : Type u_1
𝕜 : Type u_2
inst✝³ : NonUnitalNonAssocRing R
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace R
inst✝ : TopologicalAddGroup R
norm : R → 𝕜
norm_nonneg : ∀ (x : R), 0 ≤ norm x
norm_mul_le : ∀ (x y : R), norm (x * y) ≤ norm x * norm y
nhds_basis : HasBasis (𝓝 0) (fun x => 0 < x) fun ε => {x | norm x < ε}
h0 : ∀ (f : R → R) (c : 𝕜), c ≥ 0 → (∀ (x : R), norm (f x) ≤ c * norm x) → Tendsto f (𝓝 0) (𝓝 0)
⊢ ∀ (x₀ : R), Tendsto (fun x => x₀ * x) (𝓝 0) (𝓝 0)
[PROOFSTEP]
exact fun x => h0 _ (norm x) (norm_nonneg _) (norm_mul_le x)
[GOAL]
case hmul_right
R : Type u_1
𝕜 : Type u_2
inst✝³ : NonUnitalNonAssocRing R
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace R
inst✝ : TopologicalAddGroup R
norm : R → 𝕜
norm_nonneg : ∀ (x : R), 0 ≤ norm x
norm_mul_le : ∀ (x y : R), norm (x * y) ≤ norm x * norm y
nhds_basis : HasBasis (𝓝 0) (fun x => 0 < x) fun ε => {x | norm x < ε}
h0 : ∀ (f : R → R) (c : 𝕜), c ≥ 0 → (∀ (x : R), norm (f x) ≤ c * norm x) → Tendsto f (𝓝 0) (𝓝 0)
⊢ ∀ (x₀ : R), Tendsto (fun x => x * x₀) (𝓝 0) (𝓝 0)
[PROOFSTEP]
case hmul_right => exact fun y => h0 (· * y) (norm y) (norm_nonneg y) fun x => (norm_mul_le x y).trans_eq (mul_comm _ _)
[GOAL]
R : Type u_1
𝕜 : Type u_2
inst✝³ : NonUnitalNonAssocRing R
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace R
inst✝ : TopologicalAddGroup R
norm : R → 𝕜
norm_nonneg : ∀ (x : R), 0 ≤ norm x
norm_mul_le : ∀ (x y : R), norm (x * y) ≤ norm x * norm y
nhds_basis : HasBasis (𝓝 0) (fun x => 0 < x) fun ε => {x | norm x < ε}
h0 : ∀ (f : R → R) (c : 𝕜), c ≥ 0 → (∀ (x : R), norm (f x) ≤ c * norm x) → Tendsto f (𝓝 0) (𝓝 0)
⊢ ∀ (x₀ : R), Tendsto (fun x => x * x₀) (𝓝 0) (𝓝 0)
[PROOFSTEP]
case hmul_right => exact fun y => h0 (· * y) (norm y) (norm_nonneg y) fun x => (norm_mul_le x y).trans_eq (mul_comm _ _)
[GOAL]
R : Type u_1
𝕜 : Type u_2
inst✝³ : NonUnitalNonAssocRing R
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace R
inst✝ : TopologicalAddGroup R
norm : R → 𝕜
norm_nonneg : ∀ (x : R), 0 ≤ norm x
norm_mul_le : ∀ (x y : R), norm (x * y) ≤ norm x * norm y
nhds_basis : HasBasis (𝓝 0) (fun x => 0 < x) fun ε => {x | norm x < ε}
h0 : ∀ (f : R → R) (c : 𝕜), c ≥ 0 → (∀ (x : R), norm (f x) ≤ c * norm x) → Tendsto f (𝓝 0) (𝓝 0)
⊢ ∀ (x₀ : R), Tendsto (fun x => x * x₀) (𝓝 0) (𝓝 0)
[PROOFSTEP]
exact fun y => h0 (· * y) (norm y) (norm_nonneg y) fun x => (norm_mul_le x y).trans_eq (mul_comm _ _)
[GOAL]
𝕜 : Type u_1
α : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
⊢ HasBasis (𝓝 0) (fun x => 0 < x) fun ε => {x | |x| < ε}
[PROOFSTEP]
simpa using nhds_basis_abs_sub_lt (0 : 𝕜)
[GOAL]
𝕜 : Type u_1
α : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
C : 𝕜
hC : 0 < C
hf : Tendsto f l atTop
hg : Tendsto g l (𝓝 C)
⊢ Tendsto (fun x => f x * g x) l atTop
[PROOFSTEP]
refine' tendsto_atTop_mono' _ _ (hf.atTop_mul_const (half_pos hC))
[GOAL]
𝕜 : Type u_1
α : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
C : 𝕜
hC : 0 < C
hf : Tendsto f l atTop
hg : Tendsto g l (𝓝 C)
⊢ (fun x => f x * (C / 2)) ≤ᶠ[l] fun x => f x * g x
[PROOFSTEP]
filter_upwards [hg.eventually (lt_mem_nhds (half_lt_self hC)), hf.eventually_ge_atTop 0] with x hg hf using
  mul_le_mul_of_nonneg_left hg.le hf
[GOAL]
𝕜 : Type u_1
α : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
C : 𝕜
hC : 0 < C
hf : Tendsto f l (𝓝 C)
hg : Tendsto g l atTop
⊢ Tendsto (fun x => f x * g x) l atTop
[PROOFSTEP]
simpa only [mul_comm] using hg.atTop_mul hC hf
[GOAL]
𝕜 : Type u_1
α : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
C : 𝕜
hC : C < 0
hf : Tendsto f l atTop
hg : Tendsto g l (𝓝 C)
⊢ Tendsto (fun x => f x * g x) l atBot
[PROOFSTEP]
have := hf.atTop_mul (neg_pos.2 hC) hg.neg
[GOAL]
𝕜 : Type u_1
α : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
C : 𝕜
hC : C < 0
hf : Tendsto f l atTop
hg : Tendsto g l (𝓝 C)
this : Tendsto (fun x => f x * -g x) l atTop
⊢ Tendsto (fun x => f x * g x) l atBot
[PROOFSTEP]
simpa only [(· ∘ ·), neg_mul_eq_mul_neg, neg_neg] using tendsto_neg_atTop_atBot.comp this
[GOAL]
𝕜 : Type u_1
α : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
C : 𝕜
hC : C < 0
hf : Tendsto f l (𝓝 C)
hg : Tendsto g l atTop
⊢ Tendsto (fun x => f x * g x) l atBot
[PROOFSTEP]
simpa only [mul_comm] using hg.atTop_mul_neg hC hf
[GOAL]
𝕜 : Type u_1
α : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
C : 𝕜
hC : 0 < C
hf : Tendsto f l atBot
hg : Tendsto g l (𝓝 C)
⊢ Tendsto (fun x => f x * g x) l atBot
[PROOFSTEP]
have := (tendsto_neg_atBot_atTop.comp hf).atTop_mul hC hg
[GOAL]
𝕜 : Type u_1
α : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
C : 𝕜
hC : 0 < C
hf : Tendsto f l atBot
hg : Tendsto g l (𝓝 C)
this : Tendsto (fun x => (Neg.neg ∘ f) x * g x) l atTop
⊢ Tendsto (fun x => f x * g x) l atBot
[PROOFSTEP]
simpa [(· ∘ ·)] using tendsto_neg_atTop_atBot.comp this
[GOAL]
𝕜 : Type u_1
α : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
C : 𝕜
hC : C < 0
hf : Tendsto f l atBot
hg : Tendsto g l (𝓝 C)
⊢ Tendsto (fun x => f x * g x) l atTop
[PROOFSTEP]
have := (tendsto_neg_atBot_atTop.comp hf).atTop_mul_neg hC hg
[GOAL]
𝕜 : Type u_1
α : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
C : 𝕜
hC : C < 0
hf : Tendsto f l atBot
hg : Tendsto g l (𝓝 C)
this : Tendsto (fun x => (Neg.neg ∘ f) x * g x) l atBot
⊢ Tendsto (fun x => f x * g x) l atTop
[PROOFSTEP]
simpa [(· ∘ ·)] using tendsto_neg_atBot_atTop.comp this
[GOAL]
𝕜 : Type u_1
α : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
C : 𝕜
hC : 0 < C
hf : Tendsto f l (𝓝 C)
hg : Tendsto g l atBot
⊢ Tendsto (fun x => f x * g x) l atBot
[PROOFSTEP]
simpa only [mul_comm] using hg.atBot_mul hC hf
[GOAL]
𝕜 : Type u_1
α : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
C : 𝕜
hC : C < 0
hf : Tendsto f l (𝓝 C)
hg : Tendsto g l atBot
⊢ Tendsto (fun x => f x * g x) l atTop
[PROOFSTEP]
simpa only [mul_comm] using hg.atBot_mul_neg hC hf
[GOAL]
𝕜 : Type u_1
α : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
⊢ Tendsto (fun x => x⁻¹) (𝓝[Ioi 0] 0) atTop
[PROOFSTEP]
refine' (atTop_basis' 1).tendsto_right_iff.2 fun b hb => _
[GOAL]
𝕜 : Type u_1
α : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
b : 𝕜
hb : 1 ≤ b
⊢ ∀ᶠ (x : 𝕜) in 𝓝[Ioi 0] 0, x⁻¹ ∈ Ici b
[PROOFSTEP]
have hb' : 0 < b := by positivity
[GOAL]
𝕜 : Type u_1
α : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
b : 𝕜
hb : 1 ≤ b
⊢ 0 < b
[PROOFSTEP]
positivity
[GOAL]
𝕜 : Type u_1
α : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
b : 𝕜
hb : 1 ≤ b
hb' : 0 < b
⊢ ∀ᶠ (x : 𝕜) in 𝓝[Ioi 0] 0, x⁻¹ ∈ Ici b
[PROOFSTEP]
filter_upwards [Ioc_mem_nhdsWithin_Ioi ⟨le_rfl, inv_pos.2 hb'⟩] with x hx using (le_inv hx.1 hb').1 hx.2
[GOAL]
𝕜 : Type u_1
α : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
⊢ Tendsto (fun r => r⁻¹) atTop (𝓝[Ioi 0] 0)
[PROOFSTEP]
refine (atTop_basis.tendsto_iff ⟨fun s => mem_nhdsWithin_Ioi_iff_exists_Ioc_subset⟩).2 ?_
[GOAL]
𝕜 : Type u_1
α : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
⊢ ∀ (ib : 𝕜), ib ∈ Ioi 0 → ∃ ia, True ∧ ∀ (x : 𝕜), x ∈ Ici ia → x⁻¹ ∈ Ioc 0 ib
[PROOFSTEP]
refine fun b hb => ⟨b⁻¹, trivial, fun x hx => ?_⟩
[GOAL]
𝕜 : Type u_1
α : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
b : 𝕜
hb : b ∈ Ioi 0
x : 𝕜
hx : x ∈ Ici b⁻¹
⊢ x⁻¹ ∈ Ioc 0 b
[PROOFSTEP]
have : 0 < x := lt_of_lt_of_le (inv_pos.2 hb) hx
[GOAL]
𝕜 : Type u_1
α : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
b : 𝕜
hb : b ∈ Ioi 0
x : 𝕜
hx : x ∈ Ici b⁻¹
this : 0 < x
⊢ x⁻¹ ∈ Ioc 0 b
[PROOFSTEP]
exact ⟨inv_pos.2 this, (inv_le this hb).2 hx⟩
[GOAL]
𝕜 : Type u_1
α : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
a : 𝕜
h : Tendsto f l (𝓝 a)
hg : Tendsto g l atTop
⊢ Tendsto (fun x => f x / g x) l (𝓝 0)
[PROOFSTEP]
simp only [div_eq_mul_inv]
[GOAL]
𝕜 : Type u_1
α : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
a : 𝕜
h : Tendsto f l (𝓝 a)
hg : Tendsto g l atTop
⊢ Tendsto (fun x => f x * (g x)⁻¹) l (𝓝 0)
[PROOFSTEP]
exact mul_zero a ▸ h.mul (tendsto_inv_atTop_zero.comp hg)
[GOAL]
𝕜 : Type u_1
α : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
n : ℕ
hn : n ≠ 0
⊢ Tendsto (fun x => x ^ (-↑n)) atTop (𝓝 0)
[PROOFSTEP]
simpa only [zpow_neg, zpow_ofNat] using (@tendsto_pow_atTop 𝕜 _ _ hn).inv_tendsto_atTop
[GOAL]
𝕜 : Type u_1
α : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
n : ℤ
hn : n < 0
⊢ Tendsto (fun x => x ^ n) atTop (𝓝 0)
[PROOFSTEP]
lift -n to ℕ using le_of_lt (neg_pos.mpr hn) with N h
[GOAL]
case intro
𝕜 : Type u_1
α : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
n : ℤ
hn : n < 0
N : ℕ
h : ↑N = -n
⊢ Tendsto (fun x => x ^ n) atTop (𝓝 0)
[PROOFSTEP]
rw [← neg_pos, ← h, Nat.cast_pos] at hn
[GOAL]
case intro
𝕜 : Type u_1
α : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
n : ℤ
N : ℕ
hn : 0 < N
h : ↑N = -n
⊢ Tendsto (fun x => x ^ n) atTop (𝓝 0)
[PROOFSTEP]
simpa only [h, neg_neg] using tendsto_pow_neg_atTop hn.ne'
[GOAL]
𝕜 : Type u_1
α : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
n : ℕ
c d : 𝕜
⊢ Tendsto (fun x => c * x ^ n) atTop (𝓝 d) ↔ (c = 0 ∨ n = 0) ∧ c = d
[PROOFSTEP]
rcases eq_or_ne n 0 with (rfl | hn)
[GOAL]
case inl
𝕜 : Type u_1
α : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
c d : 𝕜
⊢ Tendsto (fun x => c * x ^ 0) atTop (𝓝 d) ↔ (c = 0 ∨ 0 = 0) ∧ c = d
[PROOFSTEP]
simp [tendsto_const_nhds_iff]
[GOAL]
case inr
𝕜 : Type u_1
α : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
n : ℕ
c d : 𝕜
hn : n ≠ 0
⊢ Tendsto (fun x => c * x ^ n) atTop (𝓝 d) ↔ (c = 0 ∨ n = 0) ∧ c = d
[PROOFSTEP]
rcases lt_trichotomy c 0 with (hc | rfl | hc)
[GOAL]
case inr.inl
𝕜 : Type u_1
α : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
n : ℕ
c d : 𝕜
hn : n ≠ 0
hc : c < 0
⊢ Tendsto (fun x => c * x ^ n) atTop (𝓝 d) ↔ (c = 0 ∨ n = 0) ∧ c = d
[PROOFSTEP]
have := tendsto_const_mul_pow_atBot_iff.2 ⟨hn, hc⟩
[GOAL]
case inr.inl
𝕜 : Type u_1
α : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
n : ℕ
c d : 𝕜
hn : n ≠ 0
hc : c < 0
this : Tendsto (fun x => c * x ^ n) atTop atBot
⊢ Tendsto (fun x => c * x ^ n) atTop (𝓝 d) ↔ (c = 0 ∨ n = 0) ∧ c = d
[PROOFSTEP]
simp [not_tendsto_nhds_of_tendsto_atBot this, hc.ne, hn]
[GOAL]
case inr.inr.inl
𝕜 : Type u_1
α : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
n : ℕ
d : 𝕜
hn : n ≠ 0
⊢ Tendsto (fun x => 0 * x ^ n) atTop (𝓝 d) ↔ (0 = 0 ∨ n = 0) ∧ 0 = d
[PROOFSTEP]
simp [tendsto_const_nhds_iff]
[GOAL]
case inr.inr.inr
𝕜 : Type u_1
α : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
n : ℕ
c d : 𝕜
hn : n ≠ 0
hc : 0 < c
⊢ Tendsto (fun x => c * x ^ n) atTop (𝓝 d) ↔ (c = 0 ∨ n = 0) ∧ c = d
[PROOFSTEP]
have := tendsto_const_mul_pow_atTop_iff.2 ⟨hn, hc⟩
[GOAL]
case inr.inr.inr
𝕜 : Type u_1
α : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
n : ℕ
c d : 𝕜
hn : n ≠ 0
hc : 0 < c
this : Tendsto (fun x => c * x ^ n) atTop atTop
⊢ Tendsto (fun x => c * x ^ n) atTop (𝓝 d) ↔ (c = 0 ∨ n = 0) ∧ c = d
[PROOFSTEP]
simp [not_tendsto_nhds_of_tendsto_atTop this, hc.ne', hn]
[GOAL]
𝕜 : Type u_1
α : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
n : ℕ
c d : 𝕜
hc : c ≠ 0
⊢ Tendsto (fun x => c * x ^ n) atTop (𝓝 d) ↔ n = 0 ∧ c = d
[PROOFSTEP]
simp [tendsto_const_mul_pow_nhds_iff', hc]
[GOAL]
𝕜 : Type u_1
α : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
n : ℤ
c d : 𝕜
hc : c ≠ 0
⊢ Tendsto (fun x => c * x ^ n) atTop (𝓝 d) ↔ n = 0 ∧ c = d ∨ n < 0 ∧ d = 0
[PROOFSTEP]
refine' ⟨fun h => _, fun h => _⟩
[GOAL]
case refine'_1
𝕜 : Type u_1
α : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
n : ℤ
c d : 𝕜
hc : c ≠ 0
h : Tendsto (fun x => c * x ^ n) atTop (𝓝 d)
⊢ n = 0 ∧ c = d ∨ n < 0 ∧ d = 0
[PROOFSTEP]
cases n with
  -- porting note: Lean 3 proof used `by_cases`, then `lift` but `lift` failed
| ofNat n =>
  left
  simpa [tendsto_const_mul_pow_nhds_iff hc] using h
| negSucc n =>
  have hn := Int.negSucc_lt_zero n
  exact Or.inr ⟨hn, tendsto_nhds_unique h (tendsto_const_mul_zpow_atTop_zero hn)⟩
[GOAL]
case refine'_1
𝕜 : Type u_1
α : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
n : ℤ
c d : 𝕜
hc : c ≠ 0
h : Tendsto (fun x => c * x ^ n) atTop (𝓝 d)
⊢ n = 0 ∧ c = d ∨ n < 0 ∧ d = 0
[PROOFSTEP]
cases n with
  -- porting note: Lean 3 proof used `by_cases`, then `lift` but `lift` failed
| ofNat n =>
  left
  simpa [tendsto_const_mul_pow_nhds_iff hc] using h
| negSucc n =>
  have hn := Int.negSucc_lt_zero n
  exact Or.inr ⟨hn, tendsto_nhds_unique h (tendsto_const_mul_zpow_atTop_zero hn)⟩
[GOAL]
case refine'_1.ofNat
𝕜 : Type u_1
α : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
c d : 𝕜
hc : c ≠ 0
n : ℕ
h : Tendsto (fun x => c * x ^ Int.ofNat n) atTop (𝓝 d)
⊢ Int.ofNat n = 0 ∧ c = d ∨ Int.ofNat n < 0 ∧ d = 0
[PROOFSTEP]

| ofNat n =>
  left
  simpa [tendsto_const_mul_pow_nhds_iff hc] using h
[GOAL]
case refine'_1.ofNat
𝕜 : Type u_1
α : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
c d : 𝕜
hc : c ≠ 0
n : ℕ
h : Tendsto (fun x => c * x ^ Int.ofNat n) atTop (𝓝 d)
⊢ Int.ofNat n = 0 ∧ c = d ∨ Int.ofNat n < 0 ∧ d = 0
[PROOFSTEP]
left
[GOAL]
case refine'_1.ofNat.h
𝕜 : Type u_1
α : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
c d : 𝕜
hc : c ≠ 0
n : ℕ
h : Tendsto (fun x => c * x ^ Int.ofNat n) atTop (𝓝 d)
⊢ Int.ofNat n = 0 ∧ c = d
[PROOFSTEP]
simpa [tendsto_const_mul_pow_nhds_iff hc] using h
[GOAL]
case refine'_1.negSucc
𝕜 : Type u_1
α : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
c d : 𝕜
hc : c ≠ 0
n : ℕ
h : Tendsto (fun x => c * x ^ Int.negSucc n) atTop (𝓝 d)
⊢ Int.negSucc n = 0 ∧ c = d ∨ Int.negSucc n < 0 ∧ d = 0
[PROOFSTEP]

| negSucc n =>
  have hn := Int.negSucc_lt_zero n
  exact Or.inr ⟨hn, tendsto_nhds_unique h (tendsto_const_mul_zpow_atTop_zero hn)⟩
[GOAL]
case refine'_1.negSucc
𝕜 : Type u_1
α : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
c d : 𝕜
hc : c ≠ 0
n : ℕ
h : Tendsto (fun x => c * x ^ Int.negSucc n) atTop (𝓝 d)
⊢ Int.negSucc n = 0 ∧ c = d ∨ Int.negSucc n < 0 ∧ d = 0
[PROOFSTEP]
have hn := Int.negSucc_lt_zero n
[GOAL]
case refine'_1.negSucc
𝕜 : Type u_1
α : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
c d : 𝕜
hc : c ≠ 0
n : ℕ
h : Tendsto (fun x => c * x ^ Int.negSucc n) atTop (𝓝 d)
hn : Int.negSucc n < 0
⊢ Int.negSucc n = 0 ∧ c = d ∨ Int.negSucc n < 0 ∧ d = 0
[PROOFSTEP]
exact Or.inr ⟨hn, tendsto_nhds_unique h (tendsto_const_mul_zpow_atTop_zero hn)⟩
[GOAL]
case refine'_2
𝕜 : Type u_1
α : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
n : ℤ
c d : 𝕜
hc : c ≠ 0
h : n = 0 ∧ c = d ∨ n < 0 ∧ d = 0
⊢ Tendsto (fun x => c * x ^ n) atTop (𝓝 d)
[PROOFSTEP]
cases' h with h h
[GOAL]
case refine'_2.inl
𝕜 : Type u_1
α : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
n : ℤ
c d : 𝕜
hc : c ≠ 0
h : n = 0 ∧ c = d
⊢ Tendsto (fun x => c * x ^ n) atTop (𝓝 d)
[PROOFSTEP]
simp only [h.left, h.right, zpow_zero, mul_one]
[GOAL]
case refine'_2.inl
𝕜 : Type u_1
α : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
n : ℤ
c d : 𝕜
hc : c ≠ 0
h : n = 0 ∧ c = d
⊢ Tendsto (fun x => d) atTop (𝓝 d)
[PROOFSTEP]
exact tendsto_const_nhds
[GOAL]
case refine'_2.inr
𝕜 : Type u_1
α : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
n : ℤ
c d : 𝕜
hc : c ≠ 0
h : n < 0 ∧ d = 0
⊢ Tendsto (fun x => c * x ^ n) atTop (𝓝 d)
[PROOFSTEP]
exact h.2.symm ▸ tendsto_const_mul_zpow_atTop_zero h.1
[GOAL]
𝕜✝ : Type u_1
α : Type u_2
inst✝⁶ : LinearOrderedField 𝕜✝
inst✝⁵ : TopologicalSpace 𝕜✝
inst✝⁴ : OrderTopology 𝕜✝
l : Filter α
f g : α → 𝕜✝
𝕜 : Type ?u.49426
inst✝³ : LinearOrderedSemifield 𝕜
inst✝² : TopologicalSpace 𝕜
inst✝¹ : OrderTopology 𝕜
inst✝ : ContinuousMul 𝕜
⊢ (∀ (a' : 𝕜), a' < 1 → ∀ᶠ (b : 𝕜) in 𝓝 1, a' < b⁻¹) ∧ ∀ (a' : 𝕜), a' > 1 → ∀ᶠ (b : 𝕜) in 𝓝 1, b⁻¹ < a'
[PROOFSTEP]
refine ⟨fun x hx => ?_, fun x hx => ?_⟩
[GOAL]
case refine_1
𝕜✝ : Type u_1
α : Type u_2
inst✝⁶ : LinearOrderedField 𝕜✝
inst✝⁵ : TopologicalSpace 𝕜✝
inst✝⁴ : OrderTopology 𝕜✝
l : Filter α
f g : α → 𝕜✝
𝕜 : Type ?u.49426
inst✝³ : LinearOrderedSemifield 𝕜
inst✝² : TopologicalSpace 𝕜
inst✝¹ : OrderTopology 𝕜
inst✝ : ContinuousMul 𝕜
x : 𝕜
hx : x < 1
⊢ ∀ᶠ (b : 𝕜) in 𝓝 1, x < b⁻¹
[PROOFSTEP]
obtain ⟨x', h₀, hxx', h₁⟩ : ∃ x', 0 < x' ∧ x ≤ x' ∧ x' < 1 :=
  ⟨max x (1 / 2), one_half_pos.trans_le (le_max_right _ _), le_max_left _ _, max_lt hx one_half_lt_one⟩
[GOAL]
case refine_1.intro.intro.intro
𝕜✝ : Type u_1
α : Type u_2
inst✝⁶ : LinearOrderedField 𝕜✝
inst✝⁵ : TopologicalSpace 𝕜✝
inst✝⁴ : OrderTopology 𝕜✝
l : Filter α
f g : α → 𝕜✝
𝕜 : Type ?u.49426
inst✝³ : LinearOrderedSemifield 𝕜
inst✝² : TopologicalSpace 𝕜
inst✝¹ : OrderTopology 𝕜
inst✝ : ContinuousMul 𝕜
x : 𝕜
hx : x < 1
x' : 𝕜
h₀ : 0 < x'
hxx' : x ≤ x'
h₁ : x' < 1
⊢ ∀ᶠ (b : 𝕜) in 𝓝 1, x < b⁻¹
[PROOFSTEP]
filter_upwards [Ioo_mem_nhds one_pos (one_lt_inv h₀ h₁)] with y hy
[GOAL]
case h
𝕜✝ : Type u_1
α : Type u_2
inst✝⁶ : LinearOrderedField 𝕜✝
inst✝⁵ : TopologicalSpace 𝕜✝
inst✝⁴ : OrderTopology 𝕜✝
l : Filter α
f g : α → 𝕜✝
𝕜 : Type ?u.49426
inst✝³ : LinearOrderedSemifield 𝕜
inst✝² : TopologicalSpace 𝕜
inst✝¹ : OrderTopology 𝕜
inst✝ : ContinuousMul 𝕜
x : 𝕜
hx : x < 1
x' : 𝕜
h₀ : 0 < x'
hxx' : x ≤ x'
h₁ : x' < 1
y : 𝕜
hy : y ∈ Ioo 0 x'⁻¹
⊢ x < y⁻¹
[PROOFSTEP]
exact hxx'.trans_lt <| inv_inv x' ▸ inv_lt_inv_of_lt hy.1 hy.2
[GOAL]
case refine_2
𝕜✝ : Type u_1
α : Type u_2
inst✝⁶ : LinearOrderedField 𝕜✝
inst✝⁵ : TopologicalSpace 𝕜✝
inst✝⁴ : OrderTopology 𝕜✝
l : Filter α
f g : α → 𝕜✝
𝕜 : Type ?u.49426
inst✝³ : LinearOrderedSemifield 𝕜
inst✝² : TopologicalSpace 𝕜
inst✝¹ : OrderTopology 𝕜
inst✝ : ContinuousMul 𝕜
x : 𝕜
hx : x > 1
⊢ ∀ᶠ (b : 𝕜) in 𝓝 1, b⁻¹ < x
[PROOFSTEP]
filter_upwards [Ioi_mem_nhds (inv_lt_one hx)] with y hy
[GOAL]
case h
𝕜✝ : Type u_1
α : Type u_2
inst✝⁶ : LinearOrderedField 𝕜✝
inst✝⁵ : TopologicalSpace 𝕜✝
inst✝⁴ : OrderTopology 𝕜✝
l : Filter α
f g : α → 𝕜✝
𝕜 : Type ?u.49426
inst✝³ : LinearOrderedSemifield 𝕜
inst✝² : TopologicalSpace 𝕜
inst✝¹ : OrderTopology 𝕜
inst✝ : ContinuousMul 𝕜
x : 𝕜
hx : x > 1
y : 𝕜
hy : y ∈ Ioi x⁻¹
⊢ y⁻¹ < x
[PROOFSTEP]
simpa only [inv_inv] using inv_lt_inv_of_lt (inv_pos.2 <| one_pos.trans hx) hy
[GOAL]
𝕜 : Type u_1
α : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
x : 𝕜
hx : 0 < x
⊢ comap (fun x_1 => x * x_1) (𝓝[Ioi 0] 0) = 𝓝[Ioi 0] 0
[PROOFSTEP]
rw [nhdsWithin, comap_inf, comap_principal, preimage_const_mul_Ioi _ hx, zero_div]
[GOAL]
𝕜 : Type u_1
α : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
x : 𝕜
hx : 0 < x
⊢ comap (fun x_1 => x * x_1) (𝓝 0) ⊓ 𝓟 (Ioi 0) = 𝓝 0 ⊓ 𝓟 (Ioi 0)
[PROOFSTEP]
congr 1
[GOAL]
case e_a
𝕜 : Type u_1
α : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
x : 𝕜
hx : 0 < x
⊢ comap (fun x_1 => x * x_1) (𝓝 0) = 𝓝 0
[PROOFSTEP]
refine ((Homeomorph.mulLeft₀ x hx.ne').comap_nhds_eq _).trans ?_
[GOAL]
case e_a
𝕜 : Type u_1
α : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
x : 𝕜
hx : 0 < x
⊢ 𝓝 (↑(Homeomorph.symm (Homeomorph.mulLeft₀ x (_ : x ≠ 0))) 0) = 𝓝 0
[PROOFSTEP]
simp
[GOAL]
𝕜 : Type u_1
α : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
x : 𝕜
hx : 0 < x
p : 𝕜 → Prop
h : ∀ᶠ (ε : 𝕜) in 𝓝[Ioi 0] 0, p ε
⊢ ∀ᶠ (ε : 𝕜) in 𝓝[Ioi 0] 0, p (x * ε)
[PROOFSTEP]
rw [← nhdsWithin_pos_comap_mul_left hx]
[GOAL]
𝕜 : Type u_1
α : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
l : Filter α
f g : α → 𝕜
x : 𝕜
hx : 0 < x
p : 𝕜 → Prop
h : ∀ᶠ (ε : 𝕜) in 𝓝[Ioi 0] 0, p ε
⊢ ∀ᶠ (ε : 𝕜) in comap (fun x_1 => x * x_1) (𝓝[Ioi 0] 0), p (x * ε)
[PROOFSTEP]
exact h.comap fun ε => x * ε


[GOAL]
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : TopologicalSpace α
inst✝³ : OrderTopology α
inst✝² : LinearOrder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
s : Set α
a : α
h_mono : StrictMonoOn f s
hs : s ∈ 𝓝[Ici a] a
hfs : ∀ (b : β), b > f a → ∃ c, c ∈ s ∧ f c ∈ Ioc (f a) b
⊢ ContinuousWithinAt f (Ici a) a
[PROOFSTEP]
have ha : a ∈ Ici a := left_mem_Ici
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : TopologicalSpace α
inst✝³ : OrderTopology α
inst✝² : LinearOrder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
s : Set α
a : α
h_mono : StrictMonoOn f s
hs : s ∈ 𝓝[Ici a] a
hfs : ∀ (b : β), b > f a → ∃ c, c ∈ s ∧ f c ∈ Ioc (f a) b
ha : a ∈ Ici a
⊢ ContinuousWithinAt f (Ici a) a
[PROOFSTEP]
have has : a ∈ s := mem_of_mem_nhdsWithin ha hs
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : TopologicalSpace α
inst✝³ : OrderTopology α
inst✝² : LinearOrder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
s : Set α
a : α
h_mono : StrictMonoOn f s
hs : s ∈ 𝓝[Ici a] a
hfs : ∀ (b : β), b > f a → ∃ c, c ∈ s ∧ f c ∈ Ioc (f a) b
ha : a ∈ Ici a
has : a ∈ s
⊢ ContinuousWithinAt f (Ici a) a
[PROOFSTEP]
refine' tendsto_order.2 ⟨fun b hb => _, fun b hb => _⟩
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : TopologicalSpace α
inst✝³ : OrderTopology α
inst✝² : LinearOrder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
s : Set α
a : α
h_mono : StrictMonoOn f s
hs : s ∈ 𝓝[Ici a] a
hfs : ∀ (b : β), b > f a → ∃ c, c ∈ s ∧ f c ∈ Ioc (f a) b
ha : a ∈ Ici a
has : a ∈ s
b : β
hb : b < f a
⊢ ∀ᶠ (b_1 : α) in 𝓝[Ici a] a, b < f b_1
[PROOFSTEP]
filter_upwards [hs, @self_mem_nhdsWithin _ _ a (Ici a)] with _ hxs hxa using
  hb.trans_le ((h_mono.le_iff_le has hxs).2 hxa)
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : TopologicalSpace α
inst✝³ : OrderTopology α
inst✝² : LinearOrder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
s : Set α
a : α
h_mono : StrictMonoOn f s
hs : s ∈ 𝓝[Ici a] a
hfs : ∀ (b : β), b > f a → ∃ c, c ∈ s ∧ f c ∈ Ioc (f a) b
ha : a ∈ Ici a
has : a ∈ s
b : β
hb : b > f a
⊢ ∀ᶠ (b_1 : α) in 𝓝[Ici a] a, f b_1 < b
[PROOFSTEP]
rcases hfs b hb with ⟨c, hcs, hac, hcb⟩
[GOAL]
case refine'_2.intro.intro.intro
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : TopologicalSpace α
inst✝³ : OrderTopology α
inst✝² : LinearOrder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
s : Set α
a : α
h_mono : StrictMonoOn f s
hs : s ∈ 𝓝[Ici a] a
hfs : ∀ (b : β), b > f a → ∃ c, c ∈ s ∧ f c ∈ Ioc (f a) b
ha : a ∈ Ici a
has : a ∈ s
b : β
hb : b > f a
c : α
hcs : c ∈ s
hac : f a < f c
hcb : f c ≤ b
⊢ ∀ᶠ (b_1 : α) in 𝓝[Ici a] a, f b_1 < b
[PROOFSTEP]
rw [h_mono.lt_iff_lt has hcs] at hac
[GOAL]
case refine'_2.intro.intro.intro
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : TopologicalSpace α
inst✝³ : OrderTopology α
inst✝² : LinearOrder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
s : Set α
a : α
h_mono : StrictMonoOn f s
hs : s ∈ 𝓝[Ici a] a
hfs : ∀ (b : β), b > f a → ∃ c, c ∈ s ∧ f c ∈ Ioc (f a) b
ha : a ∈ Ici a
has : a ∈ s
b : β
hb : b > f a
c : α
hcs : c ∈ s
hac : a < c
hcb : f c ≤ b
⊢ ∀ᶠ (b_1 : α) in 𝓝[Ici a] a, f b_1 < b
[PROOFSTEP]
filter_upwards [hs, Ico_mem_nhdsWithin_Ici (left_mem_Ico.2 hac)]
[GOAL]
case h
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : TopologicalSpace α
inst✝³ : OrderTopology α
inst✝² : LinearOrder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
s : Set α
a : α
h_mono : StrictMonoOn f s
hs : s ∈ 𝓝[Ici a] a
hfs : ∀ (b : β), b > f a → ∃ c, c ∈ s ∧ f c ∈ Ioc (f a) b
ha : a ∈ Ici a
has : a ∈ s
b : β
hb : b > f a
c : α
hcs : c ∈ s
hac : a < c
hcb : f c ≤ b
⊢ ∀ (a_1 : α), a_1 ∈ s → a_1 ∈ Ico a c → f a_1 < b
[PROOFSTEP]
rintro x hx ⟨_, hxc⟩
[GOAL]
case h.intro
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : TopologicalSpace α
inst✝³ : OrderTopology α
inst✝² : LinearOrder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
s : Set α
a : α
h_mono : StrictMonoOn f s
hs : s ∈ 𝓝[Ici a] a
hfs : ∀ (b : β), b > f a → ∃ c, c ∈ s ∧ f c ∈ Ioc (f a) b
ha : a ∈ Ici a
has : a ∈ s
b : β
hb : b > f a
c : α
hcs : c ∈ s
hac : a < c
hcb : f c ≤ b
x : α
hx : x ∈ s
left✝ : a ≤ x
hxc : x < c
⊢ f x < b
[PROOFSTEP]
exact ((h_mono.lt_iff_lt hx hcs).2 hxc).trans_le hcb
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : TopologicalSpace α
inst✝³ : OrderTopology α
inst✝² : LinearOrder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
s : Set α
a : α
h_mono : MonotoneOn f s
hs : s ∈ 𝓝[Ici a] a
hfs : ∀ (b : β), b > f a → ∃ c, c ∈ s ∧ f c ∈ Ioo (f a) b
⊢ ContinuousWithinAt f (Ici a) a
[PROOFSTEP]
have ha : a ∈ Ici a := left_mem_Ici
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : TopologicalSpace α
inst✝³ : OrderTopology α
inst✝² : LinearOrder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
s : Set α
a : α
h_mono : MonotoneOn f s
hs : s ∈ 𝓝[Ici a] a
hfs : ∀ (b : β), b > f a → ∃ c, c ∈ s ∧ f c ∈ Ioo (f a) b
ha : a ∈ Ici a
⊢ ContinuousWithinAt f (Ici a) a
[PROOFSTEP]
have has : a ∈ s := mem_of_mem_nhdsWithin ha hs
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : TopologicalSpace α
inst✝³ : OrderTopology α
inst✝² : LinearOrder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
s : Set α
a : α
h_mono : MonotoneOn f s
hs : s ∈ 𝓝[Ici a] a
hfs : ∀ (b : β), b > f a → ∃ c, c ∈ s ∧ f c ∈ Ioo (f a) b
ha : a ∈ Ici a
has : a ∈ s
⊢ ContinuousWithinAt f (Ici a) a
[PROOFSTEP]
refine' tendsto_order.2 ⟨fun b hb => _, fun b hb => _⟩
[GOAL]
case refine'_1
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : TopologicalSpace α
inst✝³ : OrderTopology α
inst✝² : LinearOrder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
s : Set α
a : α
h_mono : MonotoneOn f s
hs : s ∈ 𝓝[Ici a] a
hfs : ∀ (b : β), b > f a → ∃ c, c ∈ s ∧ f c ∈ Ioo (f a) b
ha : a ∈ Ici a
has : a ∈ s
b : β
hb : b < f a
⊢ ∀ᶠ (b_1 : α) in 𝓝[Ici a] a, b < f b_1
[PROOFSTEP]
filter_upwards [hs, @self_mem_nhdsWithin _ _ a (Ici a)] with _ hxs hxa using hb.trans_le (h_mono has hxs hxa)
[GOAL]
case refine'_2
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : TopologicalSpace α
inst✝³ : OrderTopology α
inst✝² : LinearOrder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
s : Set α
a : α
h_mono : MonotoneOn f s
hs : s ∈ 𝓝[Ici a] a
hfs : ∀ (b : β), b > f a → ∃ c, c ∈ s ∧ f c ∈ Ioo (f a) b
ha : a ∈ Ici a
has : a ∈ s
b : β
hb : b > f a
⊢ ∀ᶠ (b_1 : α) in 𝓝[Ici a] a, f b_1 < b
[PROOFSTEP]
rcases hfs b hb with ⟨c, hcs, hac, hcb⟩
[GOAL]
case refine'_2.intro.intro.intro
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : TopologicalSpace α
inst✝³ : OrderTopology α
inst✝² : LinearOrder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
s : Set α
a : α
h_mono : MonotoneOn f s
hs : s ∈ 𝓝[Ici a] a
hfs : ∀ (b : β), b > f a → ∃ c, c ∈ s ∧ f c ∈ Ioo (f a) b
ha : a ∈ Ici a
has : a ∈ s
b : β
hb : b > f a
c : α
hcs : c ∈ s
hac : f a < f c
hcb : f c < b
⊢ ∀ᶠ (b_1 : α) in 𝓝[Ici a] a, f b_1 < b
[PROOFSTEP]
have : a < c := not_le.1 fun h => hac.not_le <| h_mono hcs has h
[GOAL]
case refine'_2.intro.intro.intro
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : TopologicalSpace α
inst✝³ : OrderTopology α
inst✝² : LinearOrder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
s : Set α
a : α
h_mono : MonotoneOn f s
hs : s ∈ 𝓝[Ici a] a
hfs : ∀ (b : β), b > f a → ∃ c, c ∈ s ∧ f c ∈ Ioo (f a) b
ha : a ∈ Ici a
has : a ∈ s
b : β
hb : b > f a
c : α
hcs : c ∈ s
hac : f a < f c
hcb : f c < b
this : a < c
⊢ ∀ᶠ (b_1 : α) in 𝓝[Ici a] a, f b_1 < b
[PROOFSTEP]
filter_upwards [hs, Ico_mem_nhdsWithin_Ici (left_mem_Ico.2 this)]
[GOAL]
case h
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : TopologicalSpace α
inst✝³ : OrderTopology α
inst✝² : LinearOrder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
s : Set α
a : α
h_mono : MonotoneOn f s
hs : s ∈ 𝓝[Ici a] a
hfs : ∀ (b : β), b > f a → ∃ c, c ∈ s ∧ f c ∈ Ioo (f a) b
ha : a ∈ Ici a
has : a ∈ s
b : β
hb : b > f a
c : α
hcs : c ∈ s
hac : f a < f c
hcb : f c < b
this : a < c
⊢ ∀ (a_1 : α), a_1 ∈ s → a_1 ∈ Ico a c → f a_1 < b
[PROOFSTEP]
rintro x hx ⟨_, hxc⟩
[GOAL]
case h.intro
α : Type u_1
β : Type u_2
inst✝⁵ : LinearOrder α
inst✝⁴ : TopologicalSpace α
inst✝³ : OrderTopology α
inst✝² : LinearOrder β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
s : Set α
a : α
h_mono : MonotoneOn f s
hs : s ∈ 𝓝[Ici a] a
hfs : ∀ (b : β), b > f a → ∃ c, c ∈ s ∧ f c ∈ Ioo (f a) b
ha : a ∈ Ici a
has : a ∈ s
b : β
hb : b > f a
c : α
hcs : c ∈ s
hac : f a < f c
hcb : f c < b
this : a < c
x : α
hx : x ∈ s
left✝ : a ≤ x
hxc : x < c
⊢ f x < b
[PROOFSTEP]
exact (h_mono hx hcs hxc.le).trans_lt hcb
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁶ : LinearOrder α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : LinearOrder β
inst✝² : TopologicalSpace β
inst✝¹ : OrderTopology β
inst✝ : DenselyOrdered β
f : α → β
s : Set α
a : α
h_mono : MonotoneOn f s
hs : s ∈ 𝓝[Ici a] a
hfs : closure (f '' s) ∈ 𝓝[Ici (f a)] f a
⊢ ContinuousWithinAt f (Ici a) a
[PROOFSTEP]
refine' continuousWithinAt_right_of_monotoneOn_of_exists_between h_mono hs fun b hb => _
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁶ : LinearOrder α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : LinearOrder β
inst✝² : TopologicalSpace β
inst✝¹ : OrderTopology β
inst✝ : DenselyOrdered β
f : α → β
s : Set α
a : α
h_mono : MonotoneOn f s
hs : s ∈ 𝓝[Ici a] a
hfs : closure (f '' s) ∈ 𝓝[Ici (f a)] f a
b : β
hb : b > f a
⊢ ∃ c, c ∈ s ∧ f c ∈ Ioo (f a) b
[PROOFSTEP]
rcases(mem_nhdsWithin_Ici_iff_exists_mem_Ioc_Ico_subset hb).1 hfs with ⟨b', ⟨hab', hbb'⟩, hb'⟩
[GOAL]
case intro.intro.intro
α : Type u_1
β : Type u_2
inst✝⁶ : LinearOrder α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : LinearOrder β
inst✝² : TopologicalSpace β
inst✝¹ : OrderTopology β
inst✝ : DenselyOrdered β
f : α → β
s : Set α
a : α
h_mono : MonotoneOn f s
hs : s ∈ 𝓝[Ici a] a
hfs : closure (f '' s) ∈ 𝓝[Ici (f a)] f a
b : β
hb : b > f a
b' : β
hb' : Ico (f a) b' ⊆ closure (f '' s)
hab' : f a < b'
hbb' : b' ≤ b
⊢ ∃ c, c ∈ s ∧ f c ∈ Ioo (f a) b
[PROOFSTEP]
rcases exists_between hab' with ⟨c', hc'⟩
[GOAL]
case intro.intro.intro.intro
α : Type u_1
β : Type u_2
inst✝⁶ : LinearOrder α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : LinearOrder β
inst✝² : TopologicalSpace β
inst✝¹ : OrderTopology β
inst✝ : DenselyOrdered β
f : α → β
s : Set α
a : α
h_mono : MonotoneOn f s
hs : s ∈ 𝓝[Ici a] a
hfs : closure (f '' s) ∈ 𝓝[Ici (f a)] f a
b : β
hb : b > f a
b' : β
hb' : Ico (f a) b' ⊆ closure (f '' s)
hab' : f a < b'
hbb' : b' ≤ b
c' : β
hc' : f a < c' ∧ c' < b'
⊢ ∃ c, c ∈ s ∧ f c ∈ Ioo (f a) b
[PROOFSTEP]
rcases mem_closure_iff.1 (hb' ⟨hc'.1.le, hc'.2⟩) (Ioo (f a) b') isOpen_Ioo hc' with ⟨_, hc, ⟨c, hcs, rfl⟩⟩
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
β : Type u_2
inst✝⁶ : LinearOrder α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : LinearOrder β
inst✝² : TopologicalSpace β
inst✝¹ : OrderTopology β
inst✝ : DenselyOrdered β
f : α → β
s : Set α
a : α
h_mono : MonotoneOn f s
hs : s ∈ 𝓝[Ici a] a
hfs : closure (f '' s) ∈ 𝓝[Ici (f a)] f a
b : β
hb : b > f a
b' : β
hb' : Ico (f a) b' ⊆ closure (f '' s)
hab' : f a < b'
hbb' : b' ≤ b
c' : β
hc' : f a < c' ∧ c' < b'
c : α
hcs : c ∈ s
hc : f c ∈ Ioo (f a) b'
⊢ ∃ c, c ∈ s ∧ f c ∈ Ioo (f a) b
[PROOFSTEP]
exact ⟨c, hcs, hc.1, hc.2.trans_le hbb'⟩
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁶ : LinearOrder α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : LinearOrder β
inst✝² : TopologicalSpace β
inst✝¹ : OrderTopology β
inst✝ : DenselyOrdered β
f : α → β
h_mono : Monotone f
h_dense : DenseRange f
a : α
⊢ closure (f '' univ) ∈ 𝓝 (f a)
[PROOFSTEP]
simp only [image_univ, h_dense.closure_eq, univ_mem]
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁵ : PartialOrder α
inst✝⁴ : PartialOrder β
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : OrderTopology α
inst✝ : OrderTopology β
e : α ≃o β
⊢ Continuous ↑e
[PROOFSTEP]
rw [‹OrderTopology β›.topology_eq_generate_intervals]
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁵ : PartialOrder α
inst✝⁴ : PartialOrder β
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : OrderTopology α
inst✝ : OrderTopology β
e : α ≃o β
⊢ Continuous ↑e
[PROOFSTEP]
refine' continuous_generateFrom fun s hs => _
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁵ : PartialOrder α
inst✝⁴ : PartialOrder β
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : OrderTopology α
inst✝ : OrderTopology β
e : α ≃o β
s : Set β
hs : s ∈ {s | ∃ a, s = Ioi a ∨ s = Iio a}
⊢ IsOpen (↑e ⁻¹' s)
[PROOFSTEP]
rcases hs with ⟨a, rfl | rfl⟩
[GOAL]
case intro.inl
α : Type u_1
β : Type u_2
inst✝⁵ : PartialOrder α
inst✝⁴ : PartialOrder β
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : OrderTopology α
inst✝ : OrderTopology β
e : α ≃o β
a : β
⊢ IsOpen (↑e ⁻¹' Ioi a)
[PROOFSTEP]
rw [e.preimage_Ioi]
[GOAL]
case intro.inl
α : Type u_1
β : Type u_2
inst✝⁵ : PartialOrder α
inst✝⁴ : PartialOrder β
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : OrderTopology α
inst✝ : OrderTopology β
e : α ≃o β
a : β
⊢ IsOpen (Ioi (↑(symm e) a))
[PROOFSTEP]
apply isOpen_lt'
[GOAL]
case intro.inr
α : Type u_1
β : Type u_2
inst✝⁵ : PartialOrder α
inst✝⁴ : PartialOrder β
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : OrderTopology α
inst✝ : OrderTopology β
e : α ≃o β
a : β
⊢ IsOpen (↑e ⁻¹' Iio a)
[PROOFSTEP]
rw [e.preimage_Iio]
[GOAL]
case intro.inr
α : Type u_1
β : Type u_2
inst✝⁵ : PartialOrder α
inst✝⁴ : PartialOrder β
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : OrderTopology α
inst✝ : OrderTopology β
e : α ≃o β
a : β
⊢ IsOpen (Iio (↑(symm e) a))
[PROOFSTEP]
apply isOpen_gt'


[GOAL]
α : Type u_1
inst✝³ : Ring α
inst✝² : UniformSpace α
inst✝¹ : TopologicalRing α
inst✝ : UniformAddGroup α
⊢ Continuous fun p => p.fst * p.snd
[PROOFSTEP]
let m := (AddMonoidHom.mul : α →+ α →+ α).compr₂ toCompl
[GOAL]
α : Type u_1
inst✝³ : Ring α
inst✝² : UniformSpace α
inst✝¹ : TopologicalRing α
inst✝ : UniformAddGroup α
m : α →+ α →+ Completion α := AddMonoidHom.compr₂ AddMonoidHom.mul toCompl
⊢ Continuous fun p => p.fst * p.snd
[PROOFSTEP]
have : Continuous fun p : α × α => m p.1 p.2 :=
  by
  apply (continuous_coe α).comp _
  simp only [AddMonoidHom.coe_mul, AddMonoidHom.coe_mulLeft]
  exact _root_.continuous_mul
[GOAL]
α : Type u_1
inst✝³ : Ring α
inst✝² : UniformSpace α
inst✝¹ : TopologicalRing α
inst✝ : UniformAddGroup α
m : α →+ α →+ Completion α := AddMonoidHom.compr₂ AddMonoidHom.mul toCompl
⊢ Continuous fun p => ↑(↑m p.fst) p.snd
[PROOFSTEP]
apply (continuous_coe α).comp _
[GOAL]
α : Type u_1
inst✝³ : Ring α
inst✝² : UniformSpace α
inst✝¹ : TopologicalRing α
inst✝ : UniformAddGroup α
m : α →+ α →+ Completion α := AddMonoidHom.compr₂ AddMonoidHom.mul toCompl
⊢ Continuous fun p => ↑(↑AddMonoidHom.mul p.fst) p.snd
[PROOFSTEP]
simp only [AddMonoidHom.coe_mul, AddMonoidHom.coe_mulLeft]
[GOAL]
α : Type u_1
inst✝³ : Ring α
inst✝² : UniformSpace α
inst✝¹ : TopologicalRing α
inst✝ : UniformAddGroup α
m : α →+ α →+ Completion α := AddMonoidHom.compr₂ AddMonoidHom.mul toCompl
⊢ Continuous fun p => p.fst * p.snd
[PROOFSTEP]
exact _root_.continuous_mul
[GOAL]
α : Type u_1
inst✝³ : Ring α
inst✝² : UniformSpace α
inst✝¹ : TopologicalRing α
inst✝ : UniformAddGroup α
m : α →+ α →+ Completion α := AddMonoidHom.compr₂ AddMonoidHom.mul toCompl
this : Continuous fun p => ↑(↑m p.fst) p.snd
⊢ Continuous fun p => p.fst * p.snd
[PROOFSTEP]
have di : DenseInducing (toCompl : α → Completion α) := denseInducing_coe
[GOAL]
α : Type u_1
inst✝³ : Ring α
inst✝² : UniformSpace α
inst✝¹ : TopologicalRing α
inst✝ : UniformAddGroup α
m : α →+ α →+ Completion α := AddMonoidHom.compr₂ AddMonoidHom.mul toCompl
this : Continuous fun p => ↑(↑m p.fst) p.snd
di : DenseInducing ↑toCompl
⊢ Continuous fun p => p.fst * p.snd
[PROOFSTEP]
convert di.extend_Z_bilin di this
[GOAL]
α : Type u_1
inst✝³ : Ring α
inst✝² : UniformSpace α
inst✝¹ : TopologicalRing α
inst✝ : UniformAddGroup α
src✝³ : AddMonoidWithOne (Completion α) := AddMonoidWithOne.unary
src✝² : AddCommGroup (Completion α) := inferInstanceAs (AddCommGroup (Completion α))
src✝¹ : Mul (Completion α) := inferInstanceAs (Mul (Completion α))
src✝ : One (Completion α) := inferInstanceAs (One (Completion α))
a✝ b✝ c✝ : Completion α
a b c : α
⊢ ↑α a * (↑α b + ↑α c) = ↑α a * ↑α b + ↑α a * ↑α c
[PROOFSTEP]
rw [← coe_add, ← coe_mul, ← coe_mul, ← coe_mul, ← coe_add, mul_add]
[GOAL]
α : Type u_1
inst✝³ : Ring α
inst✝² : UniformSpace α
inst✝¹ : TopologicalRing α
inst✝ : UniformAddGroup α
src✝³ : AddMonoidWithOne (Completion α) := AddMonoidWithOne.unary
src✝² : AddCommGroup (Completion α) := inferInstanceAs (AddCommGroup (Completion α))
src✝¹ : Mul (Completion α) := inferInstanceAs (Mul (Completion α))
src✝ : One (Completion α) := inferInstanceAs (One (Completion α))
a✝ b✝ c✝ : Completion α
a b c : α
⊢ (↑α a + ↑α b) * ↑α c = ↑α a * ↑α c + ↑α b * ↑α c
[PROOFSTEP]
rw [← coe_add, ← coe_mul, ← coe_mul, ← coe_mul, ← coe_add, add_mul]
[GOAL]
α : Type u_1
inst✝³ : Ring α
inst✝² : UniformSpace α
inst✝¹ : TopologicalRing α
inst✝ : UniformAddGroup α
src✝³ : AddMonoidWithOne (Completion α) := AddMonoidWithOne.unary
src✝² : AddCommGroup (Completion α) := inferInstanceAs (AddCommGroup (Completion α))
src✝¹ : Mul (Completion α) := inferInstanceAs (Mul (Completion α))
src✝ : One (Completion α) := inferInstanceAs (One (Completion α))
a✝ : Completion α
a : α
⊢ 0 * ↑α a = 0
[PROOFSTEP]
rw [← coe_zero, ← coe_mul, zero_mul]
[GOAL]
α : Type u_1
inst✝³ : Ring α
inst✝² : UniformSpace α
inst✝¹ : TopologicalRing α
inst✝ : UniformAddGroup α
src✝³ : AddMonoidWithOne (Completion α) := AddMonoidWithOne.unary
src✝² : AddCommGroup (Completion α) := inferInstanceAs (AddCommGroup (Completion α))
src✝¹ : Mul (Completion α) := inferInstanceAs (Mul (Completion α))
src✝ : One (Completion α) := inferInstanceAs (One (Completion α))
a✝ : Completion α
a : α
⊢ ↑α a * 0 = 0
[PROOFSTEP]
rw [← coe_zero, ← coe_mul, mul_zero]
[GOAL]
α : Type u_1
inst✝³ : Ring α
inst✝² : UniformSpace α
inst✝¹ : TopologicalRing α
inst✝ : UniformAddGroup α
src✝³ : AddMonoidWithOne (Completion α) := AddMonoidWithOne.unary
src✝² : AddCommGroup (Completion α) := inferInstanceAs (AddCommGroup (Completion α))
src✝¹ : Mul (Completion α) := inferInstanceAs (Mul (Completion α))
src✝ : One (Completion α) := inferInstanceAs (One (Completion α))
a✝ b✝ c✝ : Completion α
a b c : α
⊢ ↑α a * ↑α b * ↑α c = ↑α a * (↑α b * ↑α c)
[PROOFSTEP]
rw [← coe_mul, ← coe_mul, ← coe_mul, ← coe_mul, mul_assoc]
[GOAL]
α : Type u_1
inst✝³ : Ring α
inst✝² : UniformSpace α
inst✝¹ : TopologicalRing α
inst✝ : UniformAddGroup α
src✝³ : AddMonoidWithOne (Completion α) := AddMonoidWithOne.unary
src✝² : AddCommGroup (Completion α) := inferInstanceAs (AddCommGroup (Completion α))
src✝¹ : Mul (Completion α) := inferInstanceAs (Mul (Completion α))
src✝ : One (Completion α) := inferInstanceAs (One (Completion α))
a✝ : Completion α
a : α
⊢ 1 * ↑α a = ↑α a
[PROOFSTEP]
rw [← coe_one, ← coe_mul, one_mul]
[GOAL]
α : Type u_1
inst✝³ : Ring α
inst✝² : UniformSpace α
inst✝¹ : TopologicalRing α
inst✝ : UniformAddGroup α
src✝³ : AddMonoidWithOne (Completion α) := AddMonoidWithOne.unary
src✝² : AddCommGroup (Completion α) := inferInstanceAs (AddCommGroup (Completion α))
src✝¹ : Mul (Completion α) := inferInstanceAs (Mul (Completion α))
src✝ : One (Completion α) := inferInstanceAs (One (Completion α))
a✝ : Completion α
a : α
⊢ ↑α a * 1 = ↑α a
[PROOFSTEP]
rw [← coe_one, ← coe_mul, mul_one]
[GOAL]
α : Type u_1
inst✝⁹ : Ring α
inst✝⁸ : UniformSpace α
inst✝⁷ : TopologicalRing α
inst✝⁶ : UniformAddGroup α
β : Type u
inst✝⁵ : UniformSpace β
inst✝⁴ : Ring β
inst✝³ : UniformAddGroup β
inst✝² : TopologicalRing β
f : α →+* β
hf✝ : Continuous ↑f
inst✝¹ : CompleteSpace β
inst✝ : SeparatedSpace β
hf' : Continuous ↑↑f
hf : UniformContinuous ↑f
⊢ Completion.extension (↑f) 1 = 1
[PROOFSTEP]
rw [← coe_one, extension_coe hf, f.map_one]
[GOAL]
α : Type u_1
inst✝⁹ : Ring α
inst✝⁸ : UniformSpace α
inst✝⁷ : TopologicalRing α
inst✝⁶ : UniformAddGroup α
β : Type u
inst✝⁵ : UniformSpace β
inst✝⁴ : Ring β
inst✝³ : UniformAddGroup β
inst✝² : TopologicalRing β
f : α →+* β
hf✝ : Continuous ↑f
inst✝¹ : CompleteSpace β
inst✝ : SeparatedSpace β
hf' : Continuous ↑↑f
hf : UniformContinuous ↑f
a✝ b✝ : Completion α
a b : α
⊢ OneHom.toFun { toFun := Completion.extension ↑f, map_one' := (_ : Completion.extension (↑f) 1 = 1) } (↑α a * ↑α b) =
    OneHom.toFun { toFun := Completion.extension ↑f, map_one' := (_ : Completion.extension (↑f) 1 = 1) } (↑α a) *
      OneHom.toFun { toFun := Completion.extension ↑f, map_one' := (_ : Completion.extension (↑f) 1 = 1) } (↑α b)
[PROOFSTEP]
simp_rw [← coe_mul, extension_coe hf, f.map_mul]
[GOAL]
α : Type u_1
inst✝⁹ : Ring α
inst✝⁸ : UniformSpace α
inst✝⁷ : TopologicalRing α
inst✝⁶ : UniformAddGroup α
β : Type u
inst✝⁵ : UniformSpace β
inst✝⁴ : Ring β
inst✝³ : UniformAddGroup β
inst✝² : TopologicalRing β
f : α →+* β
hf✝ : Continuous ↑f
inst✝¹ : CompleteSpace β
inst✝ : SeparatedSpace β
hf' : Continuous ↑↑f
hf : UniformContinuous ↑f
⊢ OneHom.toFun
      (↑{ toOneHom := { toFun := Completion.extension ↑f, map_one' := (_ : Completion.extension (↑f) 1 = 1) },
          map_mul' :=
            (_ :
              ∀ (a b : Completion α),
                OneHom.toFun { toFun := Completion.extension ↑f, map_one' := (_ : Completion.extension (↑f) 1 = 1) }
                    (a * b) =
                  OneHom.toFun { toFun := Completion.extension ↑f, map_one' := (_ : Completion.extension (↑f) 1 = 1) }
                      a *
                    OneHom.toFun { toFun := Completion.extension ↑f, map_one' := (_ : Completion.extension (↑f) 1 = 1) }
                      b) })
      0 =
    0
[PROOFSTEP]
simp_rw [← coe_zero, extension_coe hf, f.map_zero]
[GOAL]
α : Type u_1
inst✝⁹ : Ring α
inst✝⁸ : UniformSpace α
inst✝⁷ : TopologicalRing α
inst✝⁶ : UniformAddGroup α
β : Type u
inst✝⁵ : UniformSpace β
inst✝⁴ : Ring β
inst✝³ : UniformAddGroup β
inst✝² : TopologicalRing β
f : α →+* β
hf✝ : Continuous ↑f
inst✝¹ : CompleteSpace β
inst✝ : SeparatedSpace β
hf' : Continuous ↑↑f
hf : UniformContinuous ↑f
a✝ b✝ : Completion α
a b : α
⊢ OneHom.toFun
      (↑{ toOneHom := { toFun := Completion.extension ↑f, map_one' := (_ : Completion.extension (↑f) 1 = 1) },
          map_mul' :=
            (_ :
              ∀ (a b : Completion α),
                OneHom.toFun { toFun := Completion.extension ↑f, map_one' := (_ : Completion.extension (↑f) 1 = 1) }
                    (a * b) =
                  OneHom.toFun { toFun := Completion.extension ↑f, map_one' := (_ : Completion.extension (↑f) 1 = 1) }
                      a *
                    OneHom.toFun { toFun := Completion.extension ↑f, map_one' := (_ : Completion.extension (↑f) 1 = 1) }
                      b) })
      (↑α a + ↑α b) =
    OneHom.toFun
        (↑{ toOneHom := { toFun := Completion.extension ↑f, map_one' := (_ : Completion.extension (↑f) 1 = 1) },
            map_mul' :=
              (_ :
                ∀ (a b : Completion α),
                  OneHom.toFun { toFun := Completion.extension ↑f, map_one' := (_ : Completion.extension (↑f) 1 = 1) }
                      (a * b) =
                    OneHom.toFun { toFun := Completion.extension ↑f, map_one' := (_ : Completion.extension (↑f) 1 = 1) }
                        a *
                      OneHom.toFun
                        { toFun := Completion.extension ↑f, map_one' := (_ : Completion.extension (↑f) 1 = 1) } b) })
        (↑α a) +
      OneHom.toFun
        (↑{ toOneHom := { toFun := Completion.extension ↑f, map_one' := (_ : Completion.extension (↑f) 1 = 1) },
            map_mul' :=
              (_ :
                ∀ (a b : Completion α),
                  OneHom.toFun { toFun := Completion.extension ↑f, map_one' := (_ : Completion.extension (↑f) 1 = 1) }
                      (a * b) =
                    OneHom.toFun { toFun := Completion.extension ↑f, map_one' := (_ : Completion.extension (↑f) 1 = 1) }
                        a *
                      OneHom.toFun
                        { toFun := Completion.extension ↑f, map_one' := (_ : Completion.extension (↑f) 1 = 1) } b) })
        (↑α b)
[PROOFSTEP]
simp_rw [← coe_add, extension_coe hf, f.map_add]
[GOAL]
α : Type u_1
inst✝¹⁴ : Ring α
inst✝¹³ : UniformSpace α
inst✝¹² : TopologicalRing α
inst✝¹¹ : UniformAddGroup α
β : Type u
inst✝¹⁰ : UniformSpace β
inst✝⁹ : Ring β
inst✝⁸ : UniformAddGroup β
inst✝⁷ : TopologicalRing β
f : α →+* β
hf : Continuous ↑f
A : Type u_2
inst✝⁶ : Ring A
inst✝⁵ : UniformSpace A
inst✝⁴ : UniformAddGroup A
inst✝³ : TopologicalRing A
R : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Algebra R A
inst✝ : UniformContinuousConstSMul R A
r : R
⊢ Completion.map ((fun x x_1 => x • x_1) r) = (fun x x_1 => x * x_1) (↑((fun x => A) r) (↑(algebraMap R A) r))
[PROOFSTEP]
ext x
[GOAL]
case h
α : Type u_1
inst✝¹⁴ : Ring α
inst✝¹³ : UniformSpace α
inst✝¹² : TopologicalRing α
inst✝¹¹ : UniformAddGroup α
β : Type u
inst✝¹⁰ : UniformSpace β
inst✝⁹ : Ring β
inst✝⁸ : UniformAddGroup β
inst✝⁷ : TopologicalRing β
f : α →+* β
hf : Continuous ↑f
A : Type u_2
inst✝⁶ : Ring A
inst✝⁵ : UniformSpace A
inst✝⁴ : UniformAddGroup A
inst✝³ : TopologicalRing A
R : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Algebra R A
inst✝ : UniformContinuousConstSMul R A
r : R
x : Completion ((fun x => A) r)
⊢ Completion.map ((fun x x_1 => x • x_1) r) x = (fun x x_1 => x * x_1) (↑((fun x => A) r) (↑(algebraMap R A) r)) x
[PROOFSTEP]
refine' Completion.induction_on x _ fun a => _
[GOAL]
case h.refine'_1
α : Type u_1
inst✝¹⁴ : Ring α
inst✝¹³ : UniformSpace α
inst✝¹² : TopologicalRing α
inst✝¹¹ : UniformAddGroup α
β : Type u
inst✝¹⁰ : UniformSpace β
inst✝⁹ : Ring β
inst✝⁸ : UniformAddGroup β
inst✝⁷ : TopologicalRing β
f : α →+* β
hf : Continuous ↑f
A : Type u_2
inst✝⁶ : Ring A
inst✝⁵ : UniformSpace A
inst✝⁴ : UniformAddGroup A
inst✝³ : TopologicalRing A
R : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Algebra R A
inst✝ : UniformContinuousConstSMul R A
r : R
x : Completion ((fun x => A) r)
⊢ IsClosed
    {a |
      Completion.map ((fun x x_1 => x • x_1) r) a = (fun x x_1 => x * x_1) (↑((fun x => A) r) (↑(algebraMap R A) r)) a}
[PROOFSTEP]
exact isClosed_eq Completion.continuous_map (continuous_mul_left _)
[GOAL]
case h.refine'_2
α : Type u_1
inst✝¹⁴ : Ring α
inst✝¹³ : UniformSpace α
inst✝¹² : TopologicalRing α
inst✝¹¹ : UniformAddGroup α
β : Type u
inst✝¹⁰ : UniformSpace β
inst✝⁹ : Ring β
inst✝⁸ : UniformAddGroup β
inst✝⁷ : TopologicalRing β
f : α →+* β
hf : Continuous ↑f
A : Type u_2
inst✝⁶ : Ring A
inst✝⁵ : UniformSpace A
inst✝⁴ : UniformAddGroup A
inst✝³ : TopologicalRing A
R : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Algebra R A
inst✝ : UniformContinuousConstSMul R A
r : R
x : Completion ((fun x => A) r)
a : (fun x => A) r
⊢ Completion.map ((fun x x_1 => x • x_1) r) (↑((fun x => A) r) a) =
    (fun x x_1 => x * x_1) (↑((fun x => A) r) (↑(algebraMap R A) r)) (↑((fun x => A) r) a)
[PROOFSTEP]
simp_rw [map_coe (uniformContinuous_const_smul r) a, Algebra.smul_def, coe_mul]
[GOAL]
α : Type u_1
inst✝¹⁴ : Ring α
inst✝¹³ : UniformSpace α
inst✝¹² : TopologicalRing α
inst✝¹¹ : UniformAddGroup α
β : Type u
inst✝¹⁰ : UniformSpace β
inst✝⁹ : Ring β
inst✝⁸ : UniformAddGroup β
inst✝⁷ : TopologicalRing β
f : α →+* β
hf : Continuous ↑f
A : Type u_2
inst✝⁶ : Ring A
inst✝⁵ : UniformSpace A
inst✝⁴ : UniformAddGroup A
inst✝³ : TopologicalRing A
R : Type u_3
inst✝² : CommSemiring R
inst✝¹ : Algebra R A
inst✝ : UniformContinuousConstSMul R A
src✝ : R →+* Completion A := RingHom.comp coeRingHom (algebraMap R A)
r : R
x : (fun x => Completion A) r
a : A
⊢ ↑{ toMonoidHom := ↑src✝, map_zero' := (_ : OneHom.toFun (↑↑src✝) 0 = 0),
            map_add' :=
              (_ : ∀ (x y : R), OneHom.toFun (↑↑src✝) (x + y) = OneHom.toFun (↑↑src✝) x + OneHom.toFun (↑↑src✝) y) }
        r *
      ↑A a =
    ↑A a *
      ↑{ toMonoidHom := ↑src✝, map_zero' := (_ : OneHom.toFun (↑↑src✝) 0 = 0),
            map_add' :=
              (_ : ∀ (x y : R), OneHom.toFun (↑↑src✝) (x + y) = OneHom.toFun (↑↑src✝) x + OneHom.toFun (↑↑src✝) y) }
        r
[PROOFSTEP]
simpa only [coe_mul] using congr_arg ((↑) : A → Completion A) (Algebra.commutes r a)
[GOAL]
α : Type u_1
inst✝¹¹ : Ring α
inst✝¹⁰ : UniformSpace α
inst✝⁹ : TopologicalRing α
inst✝⁸ : UniformAddGroup α
β : Type u
inst✝⁷ : UniformSpace β
inst✝⁶ : Ring β
inst✝⁵ : UniformAddGroup β
inst✝⁴ : TopologicalRing β
f : α →+* β
hf : Continuous ↑f
R : Type u_2
inst✝³ : CommRing R
inst✝² : UniformSpace R
inst✝¹ : UniformAddGroup R
inst✝ : TopologicalRing R
src✝ : Ring (Completion R) := ring
a✝ b✝ : Completion R
a b : R
⊢ ↑R a * ↑R b = ↑R b * ↑R a
[PROOFSTEP]
rw [← coe_mul, ← coe_mul, mul_comm]
[GOAL]
α : Type u_1
inst✝¹¹ : Ring α
inst✝¹⁰ : UniformSpace α
inst✝⁹ : TopologicalRing α
inst✝⁸ : UniformAddGroup α
β : Type u
inst✝⁷ : UniformSpace β
inst✝⁶ : Ring β
inst✝⁵ : UniformAddGroup β
inst✝⁴ : TopologicalRing β
f : α →+* β
hf : Continuous ↑f
R : Type u_2
inst✝³ : CommRing R
inst✝² : UniformSpace R
inst✝¹ : UniformAddGroup R
inst✝ : TopologicalRing R
⊢ Algebra R (Completion R)
[PROOFSTEP]
infer_instance
[GOAL]
α✝ : Type u_1
α : Type u_2
inst✝³ : CommRing α
inst✝² : UniformSpace α
inst✝¹ : UniformAddGroup α
inst✝ : TopologicalRing α
x y : α
⊢ x - y ∈ closure {0} ↔ x - y ∈ Ideal.closure ⊥
[PROOFSTEP]
rfl
[GOAL]
α✝ : Type u_1
α : Type u
r : CommRing α
inst✝² : UniformSpace α
inst✝¹ : UniformAddGroup α
inst✝ : TopologicalRing α
⊢ Quotient (separationSetoid α) = (α ⧸ Ideal.closure ⊥)
[PROOFSTEP]
rw [@ring_sep_rel α r]
[GOAL]
α✝ : Type u_1
α : Type u
r : CommRing α
inst✝² : UniformSpace α
inst✝¹ : UniformAddGroup α
inst✝ : TopologicalRing α
⊢ Quotient (Submodule.quotientRel (Ideal.closure ⊥)) = (α ⧸ Ideal.closure ⊥)
[PROOFSTEP]
rfl
[GOAL]
α✝ : Type u_1
α : Type ?u.345143
r : CommRing α
inst✝² : UniformSpace α
inst✝¹ : UniformAddGroup α
inst✝ : TopologicalRing α
x y : α
⊢ x - y ∈ closure {0} ↔ x - y ∈ Ideal.closure ⊥
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
inst✝³ : CommRing α
inst✝² : UniformSpace α
inst✝¹ : UniformAddGroup α
inst✝ : TopologicalRing α
⊢ CommRing (Quotient (separationSetoid α))
[PROOFSTEP]
rw [ring_sep_quot α]
[GOAL]
α : Type u_1
inst✝³ : CommRing α
inst✝² : UniformSpace α
inst✝¹ : UniformAddGroup α
inst✝ : TopologicalRing α
⊢ CommRing (α ⧸ Ideal.closure ⊥)
[PROOFSTEP]
infer_instance
[GOAL]
α : Type u_1
inst✝³ : CommRing α
inst✝² : UniformSpace α
inst✝¹ : UniformAddGroup α
inst✝ : TopologicalRing α
⊢ TopologicalRing (Quotient (separationSetoid α))
[PROOFSTEP]
convert topologicalRing_quotient (⊥ : Ideal α).closure
[GOAL]
case h.e'_1
α : Type u_1
inst✝³ : CommRing α
inst✝² : UniformSpace α
inst✝¹ : UniformAddGroup α
inst✝ : TopologicalRing α
⊢ Quotient (separationSetoid α) = (α ⧸ Ideal.closure ⊥)
[PROOFSTEP]
try congr; apply ring_sep_rel
[GOAL]
case h.e'_1
α : Type u_1
inst✝³ : CommRing α
inst✝² : UniformSpace α
inst✝¹ : UniformAddGroup α
inst✝ : TopologicalRing α
⊢ Quotient (separationSetoid α) = (α ⧸ Ideal.closure ⊥)
[PROOFSTEP]
congr
[GOAL]
case h.e'_1.e_s
α : Type u_1
inst✝³ : CommRing α
inst✝² : UniformSpace α
inst✝¹ : UniformAddGroup α
inst✝ : TopologicalRing α
⊢ separationSetoid α = Submodule.quotientRel (Ideal.closure ⊥)
[PROOFSTEP]
apply ring_sep_rel
[GOAL]
case h.e'_2
α : Type u_1
inst✝³ : CommRing α
inst✝² : UniformSpace α
inst✝¹ : UniformAddGroup α
inst✝ : TopologicalRing α
e_1✝ : Quotient (separationSetoid α) = (α ⧸ Ideal.closure ⊥)
⊢ HEq instTopologicalSpaceQuotient (topologicalRingQuotientTopology (Ideal.closure ⊥))
[PROOFSTEP]
try congr; apply ring_sep_rel
[GOAL]
case h.e'_2
α : Type u_1
inst✝³ : CommRing α
inst✝² : UniformSpace α
inst✝¹ : UniformAddGroup α
inst✝ : TopologicalRing α
e_1✝ : Quotient (separationSetoid α) = (α ⧸ Ideal.closure ⊥)
⊢ HEq instTopologicalSpaceQuotient (topologicalRingQuotientTopology (Ideal.closure ⊥))
[PROOFSTEP]
congr
[GOAL]
case h.e'_2.e_2.h
α : Type u_1
inst✝³ : CommRing α
inst✝² : UniformSpace α
inst✝¹ : UniformAddGroup α
inst✝ : TopologicalRing α
e_1✝ : Quotient (separationSetoid α) = (α ⧸ Ideal.closure ⊥)
⊢ separationSetoid α = Submodule.quotientRel (Ideal.closure ⊥)
[PROOFSTEP]
apply ring_sep_rel
[GOAL]
case h.e'_3.e'_2.e'_2.e'_2
α : Type u_1
inst✝³ : CommRing α
inst✝² : UniformSpace α
inst✝¹ : UniformAddGroup α
inst✝ : TopologicalRing α
e_1✝ : Quotient (separationSetoid α) = (α ⧸ Ideal.closure ⊥)
⊢ HEq commRing (Ideal.Quotient.commRing (Ideal.closure ⊥))
[PROOFSTEP]
try congr; apply ring_sep_rel
[GOAL]
case h.e'_3.e'_2.e'_2.e'_2
α : Type u_1
inst✝³ : CommRing α
inst✝² : UniformSpace α
inst✝¹ : UniformAddGroup α
inst✝ : TopologicalRing α
e_1✝ : Quotient (separationSetoid α) = (α ⧸ Ideal.closure ⊥)
⊢ HEq commRing (Ideal.Quotient.commRing (Ideal.closure ⊥))
[PROOFSTEP]
congr
[GOAL]
case h.e'_3.e'_2.e'_2.e'_2
α : Type u_1
inst✝³ : CommRing α
inst✝² : UniformSpace α
inst✝¹ : UniformAddGroup α
inst✝ : TopologicalRing α
e_1✝ : Quotient (separationSetoid α) = (α ⧸ Ideal.closure ⊥)
⊢ HEq commRing (Ideal.Quotient.commRing (Ideal.closure ⊥))
[PROOFSTEP]
apply ring_sep_rel
[GOAL]
case h.e'_3.e'_2.e'_2.e'_2
α : Type u_1
inst✝³ : CommRing α
inst✝² : UniformSpace α
inst✝¹ : UniformAddGroup α
inst✝ : TopologicalRing α
e_1✝ : Quotient (separationSetoid α) = (α ⧸ Ideal.closure ⊥)
⊢ HEq commRing (Ideal.Quotient.commRing (Ideal.closure ⊥))
[PROOFSTEP]
simp [commRing]
[GOAL]
α : Type u_1
inst✝⁹ : UniformSpace α
inst✝⁸ : Semiring α
β : Type u_2
inst✝⁷ : UniformSpace β
inst✝⁶ : Semiring β
inst✝⁵ : TopologicalSemiring β
γ : Type u_3
inst✝⁴ : UniformSpace γ
inst✝³ : Semiring γ
inst✝² : TopologicalSemiring γ
inst✝¹ : T2Space γ
inst✝ : CompleteSpace γ
i : α →+* β
f : α →+* γ
ue : UniformInducing ↑i
dr : DenseRange ↑i
hf : UniformContinuous ↑f
⊢ extend (_ : DenseInducing ↑i) (↑f) 1 = 1
[PROOFSTEP]
convert DenseInducing.extend_eq (ue.denseInducing dr) hf.continuous 1
[GOAL]
case h.e'_2.h.e'_10
α : Type u_1
inst✝⁹ : UniformSpace α
inst✝⁸ : Semiring α
β : Type u_2
inst✝⁷ : UniformSpace β
inst✝⁶ : Semiring β
inst✝⁵ : TopologicalSemiring β
γ : Type u_3
inst✝⁴ : UniformSpace γ
inst✝³ : Semiring γ
inst✝² : TopologicalSemiring γ
inst✝¹ : T2Space γ
inst✝ : CompleteSpace γ
i : α →+* β
f : α →+* γ
ue : UniformInducing ↑i
dr : DenseRange ↑i
hf : UniformContinuous ↑f
⊢ 1 = ↑i 1
case h.e'_3
α : Type u_1
inst✝⁹ : UniformSpace α
inst✝⁸ : Semiring α
β : Type u_2
inst✝⁷ : UniformSpace β
inst✝⁶ : Semiring β
inst✝⁵ : TopologicalSemiring β
γ : Type u_3
inst✝⁴ : UniformSpace γ
inst✝³ : Semiring γ
inst✝² : TopologicalSemiring γ
inst✝¹ : T2Space γ
inst✝ : CompleteSpace γ
i : α →+* β
f : α →+* γ
ue : UniformInducing ↑i
dr : DenseRange ↑i
hf : UniformContinuous ↑f
⊢ 1 = ↑f 1
[PROOFSTEP]
exacts [i.map_one.symm, f.map_one.symm]
[GOAL]
α : Type u_1
inst✝⁹ : UniformSpace α
inst✝⁸ : Semiring α
β : Type u_2
inst✝⁷ : UniformSpace β
inst✝⁶ : Semiring β
inst✝⁵ : TopologicalSemiring β
γ : Type u_3
inst✝⁴ : UniformSpace γ
inst✝³ : Semiring γ
inst✝² : TopologicalSemiring γ
inst✝¹ : T2Space γ
inst✝ : CompleteSpace γ
i : α →+* β
f : α →+* γ
ue : UniformInducing ↑i
dr : DenseRange ↑i
hf : UniformContinuous ↑f
⊢ ∀ (x y : β),
    OneHom.toFun
        { toFun := extend (_ : DenseInducing ↑i) ↑f, map_one' := (_ : extend (_ : DenseInducing ↑i) (↑f) 1 = 1) }
        (x * y) =
      OneHom.toFun
          { toFun := extend (_ : DenseInducing ↑i) ↑f, map_one' := (_ : extend (_ : DenseInducing ↑i) (↑f) 1 = 1) } x *
        OneHom.toFun
          { toFun := extend (_ : DenseInducing ↑i) ↑f, map_one' := (_ : extend (_ : DenseInducing ↑i) (↑f) 1 = 1) } y
[PROOFSTEP]
have h := (uniformContinuous_uniformly_extend ue dr hf).continuous
[GOAL]
α : Type u_1
inst✝⁹ : UniformSpace α
inst✝⁸ : Semiring α
β : Type u_2
inst✝⁷ : UniformSpace β
inst✝⁶ : Semiring β
inst✝⁵ : TopologicalSemiring β
γ : Type u_3
inst✝⁴ : UniformSpace γ
inst✝³ : Semiring γ
inst✝² : TopologicalSemiring γ
inst✝¹ : T2Space γ
inst✝ : CompleteSpace γ
i : α →+* β
f : α →+* γ
ue : UniformInducing ↑i
dr : DenseRange ↑i
hf : UniformContinuous ↑f
h : Continuous (extend (_ : DenseInducing ↑i) ↑f)
⊢ ∀ (x y : β),
    OneHom.toFun
        { toFun := extend (_ : DenseInducing ↑i) ↑f, map_one' := (_ : extend (_ : DenseInducing ↑i) (↑f) 1 = 1) }
        (x * y) =
      OneHom.toFun
          { toFun := extend (_ : DenseInducing ↑i) ↑f, map_one' := (_ : extend (_ : DenseInducing ↑i) (↑f) 1 = 1) } x *
        OneHom.toFun
          { toFun := extend (_ : DenseInducing ↑i) ↑f, map_one' := (_ : extend (_ : DenseInducing ↑i) (↑f) 1 = 1) } y
[PROOFSTEP]
refine' fun x y => DenseRange.induction_on₂ dr _ (fun a b => _) x y
[GOAL]
case refine'_1
α : Type u_1
inst✝⁹ : UniformSpace α
inst✝⁸ : Semiring α
β : Type u_2
inst✝⁷ : UniformSpace β
inst✝⁶ : Semiring β
inst✝⁵ : TopologicalSemiring β
γ : Type u_3
inst✝⁴ : UniformSpace γ
inst✝³ : Semiring γ
inst✝² : TopologicalSemiring γ
inst✝¹ : T2Space γ
inst✝ : CompleteSpace γ
i : α →+* β
f : α →+* γ
ue : UniformInducing ↑i
dr : DenseRange ↑i
hf : UniformContinuous ↑f
h : Continuous (extend (_ : DenseInducing ↑i) ↑f)
x y : β
⊢ IsClosed
    {q |
      OneHom.toFun
          { toFun := extend (_ : DenseInducing ↑i) ↑f, map_one' := (_ : extend (_ : DenseInducing ↑i) (↑f) 1 = 1) }
          (q.fst * q.snd) =
        OneHom.toFun
            { toFun := extend (_ : DenseInducing ↑i) ↑f, map_one' := (_ : extend (_ : DenseInducing ↑i) (↑f) 1 = 1) }
            q.fst *
          OneHom.toFun
            { toFun := extend (_ : DenseInducing ↑i) ↑f, map_one' := (_ : extend (_ : DenseInducing ↑i) (↑f) 1 = 1) }
            q.snd}
[PROOFSTEP]
exact isClosed_eq (Continuous.comp h continuous_mul) ((h.comp continuous_fst).mul (h.comp continuous_snd))
[GOAL]
case refine'_2
α : Type u_1
inst✝⁹ : UniformSpace α
inst✝⁸ : Semiring α
β : Type u_2
inst✝⁷ : UniformSpace β
inst✝⁶ : Semiring β
inst✝⁵ : TopologicalSemiring β
γ : Type u_3
inst✝⁴ : UniformSpace γ
inst✝³ : Semiring γ
inst✝² : TopologicalSemiring γ
inst✝¹ : T2Space γ
inst✝ : CompleteSpace γ
i : α →+* β
f : α →+* γ
ue : UniformInducing ↑i
dr : DenseRange ↑i
hf : UniformContinuous ↑f
h : Continuous (extend (_ : DenseInducing ↑i) ↑f)
x y : β
a b : α
⊢ OneHom.toFun { toFun := extend (_ : DenseInducing ↑i) ↑f, map_one' := (_ : extend (_ : DenseInducing ↑i) (↑f) 1 = 1) }
      (↑i a * ↑i b) =
    OneHom.toFun
        { toFun := extend (_ : DenseInducing ↑i) ↑f, map_one' := (_ : extend (_ : DenseInducing ↑i) (↑f) 1 = 1) }
        (↑i a) *
      OneHom.toFun
        { toFun := extend (_ : DenseInducing ↑i) ↑f, map_one' := (_ : extend (_ : DenseInducing ↑i) (↑f) 1 = 1) } (↑i b)
[PROOFSTEP]
simp_rw [← i.map_mul, DenseInducing.extend_eq (ue.denseInducing dr) hf.continuous _, ← f.map_mul]
[GOAL]
α : Type u_1
inst✝⁹ : UniformSpace α
inst✝⁸ : Semiring α
β : Type u_2
inst✝⁷ : UniformSpace β
inst✝⁶ : Semiring β
inst✝⁵ : TopologicalSemiring β
γ : Type u_3
inst✝⁴ : UniformSpace γ
inst✝³ : Semiring γ
inst✝² : TopologicalSemiring γ
inst✝¹ : T2Space γ
inst✝ : CompleteSpace γ
i : α →+* β
f : α →+* γ
ue : UniformInducing ↑i
dr : DenseRange ↑i
hf : UniformContinuous ↑f
⊢ OneHom.toFun
      (↑{
          toOneHom :=
            { toFun := extend (_ : DenseInducing ↑i) ↑f, map_one' := (_ : extend (_ : DenseInducing ↑i) (↑f) 1 = 1) },
          map_mul' :=
            (_ :
              ∀ (x y : β),
                OneHom.toFun
                    { toFun := extend (_ : DenseInducing ↑i) ↑f,
                      map_one' := (_ : extend (_ : DenseInducing ↑i) (↑f) 1 = 1) }
                    (x * y) =
                  OneHom.toFun
                      { toFun := extend (_ : DenseInducing ↑i) ↑f,
                        map_one' := (_ : extend (_ : DenseInducing ↑i) (↑f) 1 = 1) }
                      x *
                    OneHom.toFun
                      { toFun := extend (_ : DenseInducing ↑i) ↑f,
                        map_one' := (_ : extend (_ : DenseInducing ↑i) (↑f) 1 = 1) }
                      y) })
      0 =
    0
[PROOFSTEP]
convert DenseInducing.extend_eq (ue.denseInducing dr) hf.continuous 0
[GOAL]
case h.e'_2.h.e'_1
α : Type u_1
inst✝⁹ : UniformSpace α
inst✝⁸ : Semiring α
β : Type u_2
inst✝⁷ : UniformSpace β
inst✝⁶ : Semiring β
inst✝⁵ : TopologicalSemiring β
γ : Type u_3
inst✝⁴ : UniformSpace γ
inst✝³ : Semiring γ
inst✝² : TopologicalSemiring γ
inst✝¹ : T2Space γ
inst✝ : CompleteSpace γ
i : α →+* β
f : α →+* γ
ue : UniformInducing ↑i
dr : DenseRange ↑i
hf : UniformContinuous ↑f
⊢ 0 = ↑i 0
[PROOFSTEP]
simp only [map_zero]
[GOAL]
case h.e'_3
α : Type u_1
inst✝⁹ : UniformSpace α
inst✝⁸ : Semiring α
β : Type u_2
inst✝⁷ : UniformSpace β
inst✝⁶ : Semiring β
inst✝⁵ : TopologicalSemiring β
γ : Type u_3
inst✝⁴ : UniformSpace γ
inst✝³ : Semiring γ
inst✝² : TopologicalSemiring γ
inst✝¹ : T2Space γ
inst✝ : CompleteSpace γ
i : α →+* β
f : α →+* γ
ue : UniformInducing ↑i
dr : DenseRange ↑i
hf : UniformContinuous ↑f
⊢ 0 = ↑f 0
[PROOFSTEP]
simp only [map_zero]
[GOAL]
α : Type u_1
inst✝⁹ : UniformSpace α
inst✝⁸ : Semiring α
β : Type u_2
inst✝⁷ : UniformSpace β
inst✝⁶ : Semiring β
inst✝⁵ : TopologicalSemiring β
γ : Type u_3
inst✝⁴ : UniformSpace γ
inst✝³ : Semiring γ
inst✝² : TopologicalSemiring γ
inst✝¹ : T2Space γ
inst✝ : CompleteSpace γ
i : α →+* β
f : α →+* γ
ue : UniformInducing ↑i
dr : DenseRange ↑i
hf : UniformContinuous ↑f
⊢ ∀ (x y : β),
    OneHom.toFun
        (↑{
            toOneHom :=
              { toFun := extend (_ : DenseInducing ↑i) ↑f, map_one' := (_ : extend (_ : DenseInducing ↑i) (↑f) 1 = 1) },
            map_mul' :=
              (_ :
                ∀ (x y : β),
                  OneHom.toFun
                      { toFun := extend (_ : DenseInducing ↑i) ↑f,
                        map_one' := (_ : extend (_ : DenseInducing ↑i) (↑f) 1 = 1) }
                      (x * y) =
                    OneHom.toFun
                        { toFun := extend (_ : DenseInducing ↑i) ↑f,
                          map_one' := (_ : extend (_ : DenseInducing ↑i) (↑f) 1 = 1) }
                        x *
                      OneHom.toFun
                        { toFun := extend (_ : DenseInducing ↑i) ↑f,
                          map_one' := (_ : extend (_ : DenseInducing ↑i) (↑f) 1 = 1) }
                        y) })
        (x + y) =
      OneHom.toFun
          (↑{
              toOneHom :=
                { toFun := extend (_ : DenseInducing ↑i) ↑f,
                  map_one' := (_ : extend (_ : DenseInducing ↑i) (↑f) 1 = 1) },
              map_mul' :=
                (_ :
                  ∀ (x y : β),
                    OneHom.toFun
                        { toFun := extend (_ : DenseInducing ↑i) ↑f,
                          map_one' := (_ : extend (_ : DenseInducing ↑i) (↑f) 1 = 1) }
                        (x * y) =
                      OneHom.toFun
                          { toFun := extend (_ : DenseInducing ↑i) ↑f,
                            map_one' := (_ : extend (_ : DenseInducing ↑i) (↑f) 1 = 1) }
                          x *
                        OneHom.toFun
                          { toFun := extend (_ : DenseInducing ↑i) ↑f,
                            map_one' := (_ : extend (_ : DenseInducing ↑i) (↑f) 1 = 1) }
                          y) })
          x +
        OneHom.toFun
          (↑{
              toOneHom :=
                { toFun := extend (_ : DenseInducing ↑i) ↑f,
                  map_one' := (_ : extend (_ : DenseInducing ↑i) (↑f) 1 = 1) },
              map_mul' :=
                (_ :
                  ∀ (x y : β),
                    OneHom.toFun
                        { toFun := extend (_ : DenseInducing ↑i) ↑f,
                          map_one' := (_ : extend (_ : DenseInducing ↑i) (↑f) 1 = 1) }
                        (x * y) =
                      OneHom.toFun
                          { toFun := extend (_ : DenseInducing ↑i) ↑f,
                            map_one' := (_ : extend (_ : DenseInducing ↑i) (↑f) 1 = 1) }
                          x *
                        OneHom.toFun
                          { toFun := extend (_ : DenseInducing ↑i) ↑f,
                            map_one' := (_ : extend (_ : DenseInducing ↑i) (↑f) 1 = 1) }
                          y) })
          y
[PROOFSTEP]
have h := (uniformContinuous_uniformly_extend ue dr hf).continuous
[GOAL]
α : Type u_1
inst✝⁹ : UniformSpace α
inst✝⁸ : Semiring α
β : Type u_2
inst✝⁷ : UniformSpace β
inst✝⁶ : Semiring β
inst✝⁵ : TopologicalSemiring β
γ : Type u_3
inst✝⁴ : UniformSpace γ
inst✝³ : Semiring γ
inst✝² : TopologicalSemiring γ
inst✝¹ : T2Space γ
inst✝ : CompleteSpace γ
i : α →+* β
f : α →+* γ
ue : UniformInducing ↑i
dr : DenseRange ↑i
hf : UniformContinuous ↑f
h : Continuous (extend (_ : DenseInducing ↑i) ↑f)
⊢ ∀ (x y : β),
    OneHom.toFun
        (↑{
            toOneHom :=
              { toFun := extend (_ : DenseInducing ↑i) ↑f, map_one' := (_ : extend (_ : DenseInducing ↑i) (↑f) 1 = 1) },
            map_mul' :=
              (_ :
                ∀ (x y : β),
                  OneHom.toFun
                      { toFun := extend (_ : DenseInducing ↑i) ↑f,
                        map_one' := (_ : extend (_ : DenseInducing ↑i) (↑f) 1 = 1) }
                      (x * y) =
                    OneHom.toFun
                        { toFun := extend (_ : DenseInducing ↑i) ↑f,
                          map_one' := (_ : extend (_ : DenseInducing ↑i) (↑f) 1 = 1) }
                        x *
                      OneHom.toFun
                        { toFun := extend (_ : DenseInducing ↑i) ↑f,
                          map_one' := (_ : extend (_ : DenseInducing ↑i) (↑f) 1 = 1) }
                        y) })
        (x + y) =
      OneHom.toFun
          (↑{
              toOneHom :=
                { toFun := extend (_ : DenseInducing ↑i) ↑f,
                  map_one' := (_ : extend (_ : DenseInducing ↑i) (↑f) 1 = 1) },
              map_mul' :=
                (_ :
                  ∀ (x y : β),
                    OneHom.toFun
                        { toFun := extend (_ : DenseInducing ↑i) ↑f,
                          map_one' := (_ : extend (_ : DenseInducing ↑i) (↑f) 1 = 1) }
                        (x * y) =
                      OneHom.toFun
                          { toFun := extend (_ : DenseInducing ↑i) ↑f,
                            map_one' := (_ : extend (_ : DenseInducing ↑i) (↑f) 1 = 1) }
                          x *
                        OneHom.toFun
                          { toFun := extend (_ : DenseInducing ↑i) ↑f,
                            map_one' := (_ : extend (_ : DenseInducing ↑i) (↑f) 1 = 1) }
                          y) })
          x +
        OneHom.toFun
          (↑{
              toOneHom :=
                { toFun := extend (_ : DenseInducing ↑i) ↑f,
                  map_one' := (_ : extend (_ : DenseInducing ↑i) (↑f) 1 = 1) },
              map_mul' :=
                (_ :
                  ∀ (x y : β),
                    OneHom.toFun
                        { toFun := extend (_ : DenseInducing ↑i) ↑f,
                          map_one' := (_ : extend (_ : DenseInducing ↑i) (↑f) 1 = 1) }
                        (x * y) =
                      OneHom.toFun
                          { toFun := extend (_ : DenseInducing ↑i) ↑f,
                            map_one' := (_ : extend (_ : DenseInducing ↑i) (↑f) 1 = 1) }
                          x *
                        OneHom.toFun
                          { toFun := extend (_ : DenseInducing ↑i) ↑f,
                            map_one' := (_ : extend (_ : DenseInducing ↑i) (↑f) 1 = 1) }
                          y) })
          y
[PROOFSTEP]
refine' fun x y => DenseRange.induction_on₂ dr _ (fun a b => _) x y
[GOAL]
case refine'_1
α : Type u_1
inst✝⁹ : UniformSpace α
inst✝⁸ : Semiring α
β : Type u_2
inst✝⁷ : UniformSpace β
inst✝⁶ : Semiring β
inst✝⁵ : TopologicalSemiring β
γ : Type u_3
inst✝⁴ : UniformSpace γ
inst✝³ : Semiring γ
inst✝² : TopologicalSemiring γ
inst✝¹ : T2Space γ
inst✝ : CompleteSpace γ
i : α →+* β
f : α →+* γ
ue : UniformInducing ↑i
dr : DenseRange ↑i
hf : UniformContinuous ↑f
h : Continuous (extend (_ : DenseInducing ↑i) ↑f)
x y : β
⊢ IsClosed
    {q |
      OneHom.toFun
          (↑{
              toOneHom :=
                { toFun := extend (_ : DenseInducing ↑i) ↑f,
                  map_one' := (_ : extend (_ : DenseInducing ↑i) (↑f) 1 = 1) },
              map_mul' :=
                (_ :
                  ∀ (x y : β),
                    OneHom.toFun
                        { toFun := extend (_ : DenseInducing ↑i) ↑f,
                          map_one' := (_ : extend (_ : DenseInducing ↑i) (↑f) 1 = 1) }
                        (x * y) =
                      OneHom.toFun
                          { toFun := extend (_ : DenseInducing ↑i) ↑f,
                            map_one' := (_ : extend (_ : DenseInducing ↑i) (↑f) 1 = 1) }
                          x *
                        OneHom.toFun
                          { toFun := extend (_ : DenseInducing ↑i) ↑f,
                            map_one' := (_ : extend (_ : DenseInducing ↑i) (↑f) 1 = 1) }
                          y) })
          (q.fst + q.snd) =
        OneHom.toFun
            (↑{
                toOneHom :=
                  { toFun := extend (_ : DenseInducing ↑i) ↑f,
                    map_one' := (_ : extend (_ : DenseInducing ↑i) (↑f) 1 = 1) },
                map_mul' :=
                  (_ :
                    ∀ (x y : β),
                      OneHom.toFun
                          { toFun := extend (_ : DenseInducing ↑i) ↑f,
                            map_one' := (_ : extend (_ : DenseInducing ↑i) (↑f) 1 = 1) }
                          (x * y) =
                        OneHom.toFun
                            { toFun := extend (_ : DenseInducing ↑i) ↑f,
                              map_one' := (_ : extend (_ : DenseInducing ↑i) (↑f) 1 = 1) }
                            x *
                          OneHom.toFun
                            { toFun := extend (_ : DenseInducing ↑i) ↑f,
                              map_one' := (_ : extend (_ : DenseInducing ↑i) (↑f) 1 = 1) }
                            y) })
            q.fst +
          OneHom.toFun
            (↑{
                toOneHom :=
                  { toFun := extend (_ : DenseInducing ↑i) ↑f,
                    map_one' := (_ : extend (_ : DenseInducing ↑i) (↑f) 1 = 1) },
                map_mul' :=
                  (_ :
                    ∀ (x y : β),
                      OneHom.toFun
                          { toFun := extend (_ : DenseInducing ↑i) ↑f,
                            map_one' := (_ : extend (_ : DenseInducing ↑i) (↑f) 1 = 1) }
                          (x * y) =
                        OneHom.toFun
                            { toFun := extend (_ : DenseInducing ↑i) ↑f,
                              map_one' := (_ : extend (_ : DenseInducing ↑i) (↑f) 1 = 1) }
                            x *
                          OneHom.toFun
                            { toFun := extend (_ : DenseInducing ↑i) ↑f,
                              map_one' := (_ : extend (_ : DenseInducing ↑i) (↑f) 1 = 1) }
                            y) })
            q.snd}
[PROOFSTEP]
exact isClosed_eq (Continuous.comp h continuous_add) ((h.comp continuous_fst).add (h.comp continuous_snd))
[GOAL]
case refine'_2
α : Type u_1
inst✝⁹ : UniformSpace α
inst✝⁸ : Semiring α
β : Type u_2
inst✝⁷ : UniformSpace β
inst✝⁶ : Semiring β
inst✝⁵ : TopologicalSemiring β
γ : Type u_3
inst✝⁴ : UniformSpace γ
inst✝³ : Semiring γ
inst✝² : TopologicalSemiring γ
inst✝¹ : T2Space γ
inst✝ : CompleteSpace γ
i : α →+* β
f : α →+* γ
ue : UniformInducing ↑i
dr : DenseRange ↑i
hf : UniformContinuous ↑f
h : Continuous (extend (_ : DenseInducing ↑i) ↑f)
x y : β
a b : α
⊢ OneHom.toFun
      (↑{
          toOneHom :=
            { toFun := extend (_ : DenseInducing ↑i) ↑f, map_one' := (_ : extend (_ : DenseInducing ↑i) (↑f) 1 = 1) },
          map_mul' :=
            (_ :
              ∀ (x y : β),
                OneHom.toFun
                    { toFun := extend (_ : DenseInducing ↑i) ↑f,
                      map_one' := (_ : extend (_ : DenseInducing ↑i) (↑f) 1 = 1) }
                    (x * y) =
                  OneHom.toFun
                      { toFun := extend (_ : DenseInducing ↑i) ↑f,
                        map_one' := (_ : extend (_ : DenseInducing ↑i) (↑f) 1 = 1) }
                      x *
                    OneHom.toFun
                      { toFun := extend (_ : DenseInducing ↑i) ↑f,
                        map_one' := (_ : extend (_ : DenseInducing ↑i) (↑f) 1 = 1) }
                      y) })
      (↑i a + ↑i b) =
    OneHom.toFun
        (↑{
            toOneHom :=
              { toFun := extend (_ : DenseInducing ↑i) ↑f, map_one' := (_ : extend (_ : DenseInducing ↑i) (↑f) 1 = 1) },
            map_mul' :=
              (_ :
                ∀ (x y : β),
                  OneHom.toFun
                      { toFun := extend (_ : DenseInducing ↑i) ↑f,
                        map_one' := (_ : extend (_ : DenseInducing ↑i) (↑f) 1 = 1) }
                      (x * y) =
                    OneHom.toFun
                        { toFun := extend (_ : DenseInducing ↑i) ↑f,
                          map_one' := (_ : extend (_ : DenseInducing ↑i) (↑f) 1 = 1) }
                        x *
                      OneHom.toFun
                        { toFun := extend (_ : DenseInducing ↑i) ↑f,
                          map_one' := (_ : extend (_ : DenseInducing ↑i) (↑f) 1 = 1) }
                        y) })
        (↑i a) +
      OneHom.toFun
        (↑{
            toOneHom :=
              { toFun := extend (_ : DenseInducing ↑i) ↑f, map_one' := (_ : extend (_ : DenseInducing ↑i) (↑f) 1 = 1) },
            map_mul' :=
              (_ :
                ∀ (x y : β),
                  OneHom.toFun
                      { toFun := extend (_ : DenseInducing ↑i) ↑f,
                        map_one' := (_ : extend (_ : DenseInducing ↑i) (↑f) 1 = 1) }
                      (x * y) =
                    OneHom.toFun
                        { toFun := extend (_ : DenseInducing ↑i) ↑f,
                          map_one' := (_ : extend (_ : DenseInducing ↑i) (↑f) 1 = 1) }
                        x *
                      OneHom.toFun
                        { toFun := extend (_ : DenseInducing ↑i) ↑f,
                          map_one' := (_ : extend (_ : DenseInducing ↑i) (↑f) 1 = 1) }
                        y) })
        (↑i b)
[PROOFSTEP]
simp_rw [← i.map_add, DenseInducing.extend_eq (ue.denseInducing dr) hf.continuous _, ← f.map_add]