[GOAL]
R : Type u_1
S : Type u_2
inst✝³ : Semiring R
inst✝² : TopologicalSpace R
inst✝¹ : TopologicalSemiring R
p✝ : R[X]
inst✝ : Semiring S
p : S[X]
f : S →+* R
⊢ Continuous fun x => eval₂ f x p
[PROOFSTEP]
simp only [eval₂_eq_sum, Finsupp.sum]
[GOAL]
R : Type u_1
S : Type u_2
inst✝³ : Semiring R
inst✝² : TopologicalSpace R
inst✝¹ : TopologicalSemiring R
p✝ : R[X]
inst✝ : Semiring S
p : S[X]
f : S →+* R
⊢ Continuous fun x => sum p fun e a => ↑f a * x ^ e
[PROOFSTEP]
exact continuous_finset_sum _ fun c _ => continuous_const.mul (continuous_pow _)
[GOAL]
R : Type u_1
S : Type u_2
k : Type u_3
α : Type u_4
inst✝³ : Semiring R
inst✝² : Ring S
inst✝¹ : LinearOrderedField k
f : R →+* S
abv : S → k
inst✝ : IsAbsoluteValue abv
p : R[X]
hd : 0 < degree p
hf : ↑f (leadingCoeff p) ≠ 0
l : Filter α
z : α → S
hz : Tendsto (abv ∘ z) l atTop
⊢ Tendsto (fun x => abv (eval₂ f (z x) p)) l atTop
[PROOFSTEP]
revert hf
[GOAL]
R : Type u_1
S : Type u_2
k : Type u_3
α : Type u_4
inst✝³ : Semiring R
inst✝² : Ring S
inst✝¹ : LinearOrderedField k
f : R →+* S
abv : S → k
inst✝ : IsAbsoluteValue abv
p : R[X]
hd : 0 < degree p
l : Filter α
z : α → S
hz : Tendsto (abv ∘ z) l atTop
⊢ ↑f (leadingCoeff p) ≠ 0 → Tendsto (fun x => abv (eval₂ f (z x) p)) l atTop
[PROOFSTEP]
refine' degree_pos_induction_on p hd _ _ _
[GOAL]
case refine'_1
R : Type u_1
S : Type u_2
k : Type u_3
α : Type u_4
inst✝³ : Semiring R
inst✝² : Ring S
inst✝¹ : LinearOrderedField k
f : R →+* S
abv : S → k
inst✝ : IsAbsoluteValue abv
p : R[X]
hd : 0 < degree p
l : Filter α
z : α → S
hz : Tendsto (abv ∘ z) l atTop
⊢ ∀ {a : R}, a ≠ 0 → ↑f (leadingCoeff (↑C a * X)) ≠ 0 → Tendsto (fun x => abv (eval₂ f (z x) (↑C a * X))) l atTop
[PROOFSTEP]
clear hd p
[GOAL]
case refine'_2
R : Type u_1
S : Type u_2
k : Type u_3
α : Type u_4
inst✝³ : Semiring R
inst✝² : Ring S
inst✝¹ : LinearOrderedField k
f : R →+* S
abv : S → k
inst✝ : IsAbsoluteValue abv
p : R[X]
hd : 0 < degree p
l : Filter α
z : α → S
hz : Tendsto (abv ∘ z) l atTop
⊢ ∀ {p : R[X]},
    0 < degree p →
      (↑f (leadingCoeff p) ≠ 0 → Tendsto (fun x => abv (eval₂ f (z x) p)) l atTop) →
        ↑f (leadingCoeff (p * X)) ≠ 0 → Tendsto (fun x => abv (eval₂ f (z x) (p * X))) l atTop
[PROOFSTEP]
clear hd p
[GOAL]
case refine'_3
R : Type u_1
S : Type u_2
k : Type u_3
α : Type u_4
inst✝³ : Semiring R
inst✝² : Ring S
inst✝¹ : LinearOrderedField k
f : R →+* S
abv : S → k
inst✝ : IsAbsoluteValue abv
p : R[X]
hd : 0 < degree p
l : Filter α
z : α → S
hz : Tendsto (abv ∘ z) l atTop
⊢ ∀ {p : R[X]} {a : R},
    0 < degree p →
      (↑f (leadingCoeff p) ≠ 0 → Tendsto (fun x => abv (eval₂ f (z x) p)) l atTop) →
        ↑f (leadingCoeff (p + ↑C a)) ≠ 0 → Tendsto (fun x => abv (eval₂ f (z x) (p + ↑C a))) l atTop
[PROOFSTEP]
clear hd p
[GOAL]
case refine'_1
R : Type u_1
S : Type u_2
k : Type u_3
α : Type u_4
inst✝³ : Semiring R
inst✝² : Ring S
inst✝¹ : LinearOrderedField k
f : R →+* S
abv : S → k
inst✝ : IsAbsoluteValue abv
l : Filter α
z : α → S
hz : Tendsto (abv ∘ z) l atTop
⊢ ∀ {a : R}, a ≠ 0 → ↑f (leadingCoeff (↑C a * X)) ≠ 0 → Tendsto (fun x => abv (eval₂ f (z x) (↑C a * X))) l atTop
[PROOFSTEP]
rintro _ - hc
[GOAL]
case refine'_1
R : Type u_1
S : Type u_2
k : Type u_3
α : Type u_4
inst✝³ : Semiring R
inst✝² : Ring S
inst✝¹ : LinearOrderedField k
f : R →+* S
abv : S → k
inst✝ : IsAbsoluteValue abv
l : Filter α
z : α → S
hz : Tendsto (abv ∘ z) l atTop
a✝ : R
hc : ↑f (leadingCoeff (↑C a✝ * X)) ≠ 0
⊢ Tendsto (fun x => abv (eval₂ f (z x) (↑C a✝ * X))) l atTop
[PROOFSTEP]
rw [leadingCoeff_mul_X, leadingCoeff_C] at hc
[GOAL]
case refine'_1
R : Type u_1
S : Type u_2
k : Type u_3
α : Type u_4
inst✝³ : Semiring R
inst✝² : Ring S
inst✝¹ : LinearOrderedField k
f : R →+* S
abv : S → k
inst✝ : IsAbsoluteValue abv
l : Filter α
z : α → S
hz : Tendsto (abv ∘ z) l atTop
a✝ : R
hc : ↑f a✝ ≠ 0
⊢ Tendsto (fun x => abv (eval₂ f (z x) (↑C a✝ * X))) l atTop
[PROOFSTEP]
simpa [abv_mul abv] using hz.const_mul_atTop ((abv_pos abv).2 hc)
[GOAL]
case refine'_2
R : Type u_1
S : Type u_2
k : Type u_3
α : Type u_4
inst✝³ : Semiring R
inst✝² : Ring S
inst✝¹ : LinearOrderedField k
f : R →+* S
abv : S → k
inst✝ : IsAbsoluteValue abv
l : Filter α
z : α → S
hz : Tendsto (abv ∘ z) l atTop
⊢ ∀ {p : R[X]},
    0 < degree p →
      (↑f (leadingCoeff p) ≠ 0 → Tendsto (fun x => abv (eval₂ f (z x) p)) l atTop) →
        ↑f (leadingCoeff (p * X)) ≠ 0 → Tendsto (fun x => abv (eval₂ f (z x) (p * X))) l atTop
[PROOFSTEP]
intro _ _ ihp hf
[GOAL]
case refine'_2
R : Type u_1
S : Type u_2
k : Type u_3
α : Type u_4
inst✝³ : Semiring R
inst✝² : Ring S
inst✝¹ : LinearOrderedField k
f : R →+* S
abv : S → k
inst✝ : IsAbsoluteValue abv
l : Filter α
z : α → S
hz : Tendsto (abv ∘ z) l atTop
p✝ : R[X]
a✝ : 0 < degree p✝
ihp : ↑f (leadingCoeff p✝) ≠ 0 → Tendsto (fun x => abv (eval₂ f (z x) p✝)) l atTop
hf : ↑f (leadingCoeff (p✝ * X)) ≠ 0
⊢ Tendsto (fun x => abv (eval₂ f (z x) (p✝ * X))) l atTop
[PROOFSTEP]
rw [leadingCoeff_mul_X] at hf
[GOAL]
case refine'_2
R : Type u_1
S : Type u_2
k : Type u_3
α : Type u_4
inst✝³ : Semiring R
inst✝² : Ring S
inst✝¹ : LinearOrderedField k
f : R →+* S
abv : S → k
inst✝ : IsAbsoluteValue abv
l : Filter α
z : α → S
hz : Tendsto (abv ∘ z) l atTop
p✝ : R[X]
a✝ : 0 < degree p✝
ihp : ↑f (leadingCoeff p✝) ≠ 0 → Tendsto (fun x => abv (eval₂ f (z x) p✝)) l atTop
hf : ↑f (leadingCoeff p✝) ≠ 0
⊢ Tendsto (fun x => abv (eval₂ f (z x) (p✝ * X))) l atTop
[PROOFSTEP]
simpa [abv_mul abv] using (ihp hf).atTop_mul_atTop hz
[GOAL]
case refine'_3
R : Type u_1
S : Type u_2
k : Type u_3
α : Type u_4
inst✝³ : Semiring R
inst✝² : Ring S
inst✝¹ : LinearOrderedField k
f : R →+* S
abv : S → k
inst✝ : IsAbsoluteValue abv
l : Filter α
z : α → S
hz : Tendsto (abv ∘ z) l atTop
⊢ ∀ {p : R[X]} {a : R},
    0 < degree p →
      (↑f (leadingCoeff p) ≠ 0 → Tendsto (fun x => abv (eval₂ f (z x) p)) l atTop) →
        ↑f (leadingCoeff (p + ↑C a)) ≠ 0 → Tendsto (fun x => abv (eval₂ f (z x) (p + ↑C a))) l atTop
[PROOFSTEP]
intro _ a hd ihp hf
[GOAL]
case refine'_3
R : Type u_1
S : Type u_2
k : Type u_3
α : Type u_4
inst✝³ : Semiring R
inst✝² : Ring S
inst✝¹ : LinearOrderedField k
f : R →+* S
abv : S → k
inst✝ : IsAbsoluteValue abv
l : Filter α
z : α → S
hz : Tendsto (abv ∘ z) l atTop
p✝ : R[X]
a : R
hd : 0 < degree p✝
ihp : ↑f (leadingCoeff p✝) ≠ 0 → Tendsto (fun x => abv (eval₂ f (z x) p✝)) l atTop
hf : ↑f (leadingCoeff (p✝ + ↑C a)) ≠ 0
⊢ Tendsto (fun x => abv (eval₂ f (z x) (p✝ + ↑C a))) l atTop
[PROOFSTEP]
rw [add_comm, leadingCoeff_add_of_degree_lt (degree_C_le.trans_lt hd)] at hf
[GOAL]
case refine'_3
R : Type u_1
S : Type u_2
k : Type u_3
α : Type u_4
inst✝³ : Semiring R
inst✝² : Ring S
inst✝¹ : LinearOrderedField k
f : R →+* S
abv : S → k
inst✝ : IsAbsoluteValue abv
l : Filter α
z : α → S
hz : Tendsto (abv ∘ z) l atTop
p✝ : R[X]
a : R
hd : 0 < degree p✝
ihp : ↑f (leadingCoeff p✝) ≠ 0 → Tendsto (fun x => abv (eval₂ f (z x) p✝)) l atTop
hf : ↑f (leadingCoeff p✝) ≠ 0
⊢ Tendsto (fun x => abv (eval₂ f (z x) (p✝ + ↑C a))) l atTop
[PROOFSTEP]
refine' tendsto_atTop_of_add_const_right (abv (-f a)) _
[GOAL]
case refine'_3
R : Type u_1
S : Type u_2
k : Type u_3
α : Type u_4
inst✝³ : Semiring R
inst✝² : Ring S
inst✝¹ : LinearOrderedField k
f : R →+* S
abv : S → k
inst✝ : IsAbsoluteValue abv
l : Filter α
z : α → S
hz : Tendsto (abv ∘ z) l atTop
p✝ : R[X]
a : R
hd : 0 < degree p✝
ihp : ↑f (leadingCoeff p✝) ≠ 0 → Tendsto (fun x => abv (eval₂ f (z x) p✝)) l atTop
hf : ↑f (leadingCoeff p✝) ≠ 0
⊢ Tendsto (fun x => abv (eval₂ f (z x) (p✝ + ↑C a)) + abv (-↑f a)) l atTop
[PROOFSTEP]
refine' tendsto_atTop_mono (fun _ => abv_add abv _ _) _
[GOAL]
case refine'_3
R : Type u_1
S : Type u_2
k : Type u_3
α : Type u_4
inst✝³ : Semiring R
inst✝² : Ring S
inst✝¹ : LinearOrderedField k
f : R →+* S
abv : S → k
inst✝ : IsAbsoluteValue abv
l : Filter α
z : α → S
hz : Tendsto (abv ∘ z) l atTop
p✝ : R[X]
a : R
hd : 0 < degree p✝
ihp : ↑f (leadingCoeff p✝) ≠ 0 → Tendsto (fun x => abv (eval₂ f (z x) p✝)) l atTop
hf : ↑f (leadingCoeff p✝) ≠ 0
⊢ Tendsto (fun x => abv (eval₂ f (z x) (p✝ + ↑C a) + -↑f a)) l atTop
[PROOFSTEP]
simpa using ihp hf
[GOAL]
R : Type u_1
k : Type u_2
α : Type u_3
inst✝² : Ring R
inst✝¹ : LinearOrderedField k
abv : R → k
inst✝ : IsAbsoluteValue abv
p : R[X]
h : 0 < degree p
l : Filter α
z : α → R
hz : Tendsto (abv ∘ z) l atTop
⊢ Tendsto (fun x => abv (eval (z x) p)) l atTop
[PROOFSTEP]
apply tendsto_abv_eval₂_atTop _ _ _ h _ hz
[GOAL]
R : Type u_1
k : Type u_2
α : Type u_3
inst✝² : Ring R
inst✝¹ : LinearOrderedField k
abv : R → k
inst✝ : IsAbsoluteValue abv
p : R[X]
h : 0 < degree p
l : Filter α
z : α → R
hz : Tendsto (abv ∘ z) l atTop
⊢ ↑(RingHom.id R) (leadingCoeff p) ≠ 0
[PROOFSTEP]
exact (mt leadingCoeff_eq_zero.1 (ne_zero_of_degree_gt h))
[GOAL]
α : Type u_1
R : Type u_2
inst✝² : NormedRing R
inst✝¹ : IsAbsoluteValue norm
inst✝ : ProperSpace R
p : R[X]
hp0 : ¬0 < degree p
⊢ ∀ (y : R), ‖eval (coeff p 0) p‖ ≤ ‖eval y p‖
[PROOFSTEP]
rw [eq_C_of_degree_le_zero (le_of_not_gt hp0)]
[GOAL]
α : Type u_1
R : Type u_2
inst✝² : NormedRing R
inst✝¹ : IsAbsoluteValue norm
inst✝ : ProperSpace R
p : R[X]
hp0 : ¬0 < degree p
⊢ ∀ (y : R), ‖eval (coeff (↑C (coeff p 0)) 0) (↑C (coeff p 0))‖ ≤ ‖eval y (↑C (coeff p 0))‖
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
R : Type u_2
inst✝³ : NormedRing R
inst✝² : IsAbsoluteValue norm
F : Type u_3
K : Type u_4
inst✝¹ : CommRing F
inst✝ : NormedField K
p : F[X]
f : F →+* K
B : ℝ
hB : B < 0
h1 : Monic p
h2 : Splits f p
h3 : ∀ (z : K), z ∈ roots (map f p) → ‖z‖ ≤ B
⊢ natDegree p = 0
[PROOFSTEP]
contrapose! hB
[GOAL]
α : Type u_1
R : Type u_2
inst✝³ : NormedRing R
inst✝² : IsAbsoluteValue norm
F : Type u_3
K : Type u_4
inst✝¹ : CommRing F
inst✝ : NormedField K
p : F[X]
f : F →+* K
B : ℝ
h1 : Monic p
h2 : Splits f p
h3 : ∀ (z : K), z ∈ roots (map f p) → ‖z‖ ≤ B
hB : natDegree p ≠ 0
⊢ 0 ≤ B
[PROOFSTEP]
rw [← h1.natDegree_map f, natDegree_eq_card_roots' h2] at hB
[GOAL]
α : Type u_1
R : Type u_2
inst✝³ : NormedRing R
inst✝² : IsAbsoluteValue norm
F : Type u_3
K : Type u_4
inst✝¹ : CommRing F
inst✝ : NormedField K
p : F[X]
f : F →+* K
B : ℝ
h1 : Monic p
h2 : Splits f p
h3 : ∀ (z : K), z ∈ roots (map f p) → ‖z‖ ≤ B
hB : ↑card (roots (map f p)) ≠ 0
⊢ 0 ≤ B
[PROOFSTEP]
obtain ⟨z, hz⟩ := card_pos_iff_exists_mem.mp (zero_lt_iff.mpr hB)
[GOAL]
case intro
α : Type u_1
R : Type u_2
inst✝³ : NormedRing R
inst✝² : IsAbsoluteValue norm
F : Type u_3
K : Type u_4
inst✝¹ : CommRing F
inst✝ : NormedField K
p : F[X]
f : F →+* K
B : ℝ
h1 : Monic p
h2 : Splits f p
h3 : ∀ (z : K), z ∈ roots (map f p) → ‖z‖ ≤ B
hB : ↑card (roots (map f p)) ≠ 0
z : K
hz : z ∈ roots (map f p)
⊢ 0 ≤ B
[PROOFSTEP]
exact le_trans (norm_nonneg _) (h3 z hz)
[GOAL]
α : Type u_1
R : Type u_2
inst✝³ : NormedRing R
inst✝² : IsAbsoluteValue norm
F : Type u_3
K : Type u_4
inst✝¹ : CommRing F
inst✝ : NormedField K
p : F[X]
f : F →+* K
B : ℝ
i : ℕ
h1 : Monic p
h2 : Splits f p
h3 : ∀ (z : K), z ∈ roots (map f p) → ‖z‖ ≤ B
⊢ ‖coeff (map f p) i‖ ≤ B ^ (natDegree p - i) * ↑(Nat.choose (natDegree p) i)
[PROOFSTEP]
obtain hB | hB := lt_or_le B 0
[GOAL]
case inl
α : Type u_1
R : Type u_2
inst✝³ : NormedRing R
inst✝² : IsAbsoluteValue norm
F : Type u_3
K : Type u_4
inst✝¹ : CommRing F
inst✝ : NormedField K
p : F[X]
f : F →+* K
B : ℝ
i : ℕ
h1 : Monic p
h2 : Splits f p
h3 : ∀ (z : K), z ∈ roots (map f p) → ‖z‖ ≤ B
hB : B < 0
⊢ ‖coeff (map f p) i‖ ≤ B ^ (natDegree p - i) * ↑(Nat.choose (natDegree p) i)
[PROOFSTEP]
rw [eq_one_of_roots_le hB h1 h2 h3, Polynomial.map_one, natDegree_one, zero_tsub, pow_zero, one_mul, coeff_one]
[GOAL]
case inl
α : Type u_1
R : Type u_2
inst✝³ : NormedRing R
inst✝² : IsAbsoluteValue norm
F : Type u_3
K : Type u_4
inst✝¹ : CommRing F
inst✝ : NormedField K
p : F[X]
f : F →+* K
B : ℝ
i : ℕ
h1 : Monic p
h2 : Splits f p
h3 : ∀ (z : K), z ∈ roots (map f p) → ‖z‖ ≤ B
hB : B < 0
⊢ ‖if 0 = i then 1 else 0‖ ≤ ↑(Nat.choose 0 i)
[PROOFSTEP]
split_ifs
[GOAL]
case pos
α : Type u_1
R : Type u_2
inst✝³ : NormedRing R
inst✝² : IsAbsoluteValue norm
F : Type u_3
K : Type u_4
inst✝¹ : CommRing F
inst✝ : NormedField K
p : F[X]
f : F →+* K
B : ℝ
i : ℕ
h1 : Monic p
h2 : Splits f p
h3 : ∀ (z : K), z ∈ roots (map f p) → ‖z‖ ≤ B
hB : B < 0
h✝ : 0 = i
⊢ ‖1‖ ≤ ↑(Nat.choose 0 i)
[PROOFSTEP]
norm_num [h]
[GOAL]
case neg
α : Type u_1
R : Type u_2
inst✝³ : NormedRing R
inst✝² : IsAbsoluteValue norm
F : Type u_3
K : Type u_4
inst✝¹ : CommRing F
inst✝ : NormedField K
p : F[X]
f : F →+* K
B : ℝ
i : ℕ
h1 : Monic p
h2 : Splits f p
h3 : ∀ (z : K), z ∈ roots (map f p) → ‖z‖ ≤ B
hB : B < 0
h✝ : ¬0 = i
⊢ ‖0‖ ≤ ↑(Nat.choose 0 i)
[PROOFSTEP]
norm_num [h]
[GOAL]
case pos
α : Type u_1
R : Type u_2
inst✝³ : NormedRing R
inst✝² : IsAbsoluteValue norm
F : Type u_3
K : Type u_4
inst✝¹ : CommRing F
inst✝ : NormedField K
p : F[X]
f : F →+* K
B : ℝ
i : ℕ
h1 : Monic p
h2 : Splits f p
h3 : ∀ (z : K), z ∈ roots (map f p) → ‖z‖ ≤ B
hB : B < 0
h✝ : 0 = i
⊢ 1 ≤ Nat.choose 0 i
[PROOFSTEP]
simp [‹0 = i›]
[GOAL]
case inr
α : Type u_1
R : Type u_2
inst✝³ : NormedRing R
inst✝² : IsAbsoluteValue norm
F : Type u_3
K : Type u_4
inst✝¹ : CommRing F
inst✝ : NormedField K
p : F[X]
f : F →+* K
B : ℝ
i : ℕ
h1 : Monic p
h2 : Splits f p
h3 : ∀ (z : K), z ∈ roots (map f p) → ‖z‖ ≤ B
hB : 0 ≤ B
⊢ ‖coeff (map f p) i‖ ≤ B ^ (natDegree p - i) * ↑(Nat.choose (natDegree p) i)
[PROOFSTEP]
rw [← h1.natDegree_map f]
[GOAL]
case inr
α : Type u_1
R : Type u_2
inst✝³ : NormedRing R
inst✝² : IsAbsoluteValue norm
F : Type u_3
K : Type u_4
inst✝¹ : CommRing F
inst✝ : NormedField K
p : F[X]
f : F →+* K
B : ℝ
i : ℕ
h1 : Monic p
h2 : Splits f p
h3 : ∀ (z : K), z ∈ roots (map f p) → ‖z‖ ≤ B
hB : 0 ≤ B
⊢ ‖coeff (map f p) i‖ ≤ B ^ (natDegree (map f p) - i) * ↑(Nat.choose (natDegree (map f p)) i)
[PROOFSTEP]
obtain hi | hi := lt_or_le (map f p).natDegree i
[GOAL]
case inr.inl
α : Type u_1
R : Type u_2
inst✝³ : NormedRing R
inst✝² : IsAbsoluteValue norm
F : Type u_3
K : Type u_4
inst✝¹ : CommRing F
inst✝ : NormedField K
p : F[X]
f : F →+* K
B : ℝ
i : ℕ
h1 : Monic p
h2 : Splits f p
h3 : ∀ (z : K), z ∈ roots (map f p) → ‖z‖ ≤ B
hB : 0 ≤ B
hi : natDegree (map f p) < i
⊢ ‖coeff (map f p) i‖ ≤ B ^ (natDegree (map f p) - i) * ↑(Nat.choose (natDegree (map f p)) i)
[PROOFSTEP]
rw [coeff_eq_zero_of_natDegree_lt hi, norm_zero]
[GOAL]
case inr.inl
α : Type u_1
R : Type u_2
inst✝³ : NormedRing R
inst✝² : IsAbsoluteValue norm
F : Type u_3
K : Type u_4
inst✝¹ : CommRing F
inst✝ : NormedField K
p : F[X]
f : F →+* K
B : ℝ
i : ℕ
h1 : Monic p
h2 : Splits f p
h3 : ∀ (z : K), z ∈ roots (map f p) → ‖z‖ ≤ B
hB : 0 ≤ B
hi : natDegree (map f p) < i
⊢ 0 ≤ B ^ (natDegree (map f p) - i) * ↑(Nat.choose (natDegree (map f p)) i)
[PROOFSTEP]
positivity
[GOAL]
case inr.inr
α : Type u_1
R : Type u_2
inst✝³ : NormedRing R
inst✝² : IsAbsoluteValue norm
F : Type u_3
K : Type u_4
inst✝¹ : CommRing F
inst✝ : NormedField K
p : F[X]
f : F →+* K
B : ℝ
i : ℕ
h1 : Monic p
h2 : Splits f p
h3 : ∀ (z : K), z ∈ roots (map f p) → ‖z‖ ≤ B
hB : 0 ≤ B
hi : i ≤ natDegree (map f p)
⊢ ‖coeff (map f p) i‖ ≤ B ^ (natDegree (map f p) - i) * ↑(Nat.choose (natDegree (map f p)) i)
[PROOFSTEP]
rw [coeff_eq_esymm_roots_of_splits ((splits_id_iff_splits f).2 h2) hi, (h1.map _).leadingCoeff, one_mul, norm_mul,
  norm_pow, norm_neg, norm_one, one_pow, one_mul]
[GOAL]
case inr.inr
α : Type u_1
R : Type u_2
inst✝³ : NormedRing R
inst✝² : IsAbsoluteValue norm
F : Type u_3
K : Type u_4
inst✝¹ : CommRing F
inst✝ : NormedField K
p : F[X]
f : F →+* K
B : ℝ
i : ℕ
h1 : Monic p
h2 : Splits f p
h3 : ∀ (z : K), z ∈ roots (map f p) → ‖z‖ ≤ B
hB : 0 ≤ B
hi : i ≤ natDegree (map f p)
⊢ ‖esymm (roots (map f p)) (natDegree (map f p) - i)‖ ≤
    B ^ (natDegree (map f p) - i) * ↑(Nat.choose (natDegree (map f p)) i)
[PROOFSTEP]
apply ((norm_multiset_sum_le _).trans <| sum_le_card_nsmul _ _ fun r hr => _).trans
[GOAL]
case inr.inr
α : Type u_1
R : Type u_2
inst✝³ : NormedRing R
inst✝² : IsAbsoluteValue norm
F : Type u_3
K : Type u_4
inst✝¹ : CommRing F
inst✝ : NormedField K
p : F[X]
f : F →+* K
B : ℝ
i : ℕ
h1 : Monic p
h2 : Splits f p
h3 : ∀ (z : K), z ∈ roots (map f p) → ‖z‖ ≤ B
hB : 0 ≤ B
hi : i ≤ natDegree (map f p)
⊢ ↑card (Multiset.map (fun x => ‖x‖) (Multiset.map prod (powersetLen (natDegree (map f p) - i) (roots (map f p))))) •
      ?m.209879 ≤
    B ^ (natDegree (map f p) - i) * ↑(Nat.choose (natDegree (map f p)) i)
[PROOFSTEP]
rw [Multiset.map_map, card_map, card_powersetLen, ← natDegree_eq_card_roots' h2, Nat.choose_symm hi, mul_comm,
  nsmul_eq_mul]
[GOAL]
α : Type u_1
R : Type u_2
inst✝³ : NormedRing R
inst✝² : IsAbsoluteValue norm
F : Type u_3
K : Type u_4
inst✝¹ : CommRing F
inst✝ : NormedField K
p : F[X]
f : F →+* K
B : ℝ
i : ℕ
h1 : Monic p
h2 : Splits f p
h3 : ∀ (z : K), z ∈ roots (map f p) → ‖z‖ ≤ B
hB : 0 ≤ B
hi : i ≤ natDegree (map f p)
⊢ ∀ (r : ℝ),
    r ∈ Multiset.map (fun x => ‖x‖) (Multiset.map prod (powersetLen (natDegree (map f p) - i) (roots (map f p)))) →
      r ≤ B ^ (natDegree (map f p) - i)
[PROOFSTEP]
intro r hr
[GOAL]
α : Type u_1
R : Type u_2
inst✝³ : NormedRing R
inst✝² : IsAbsoluteValue norm
F : Type u_3
K : Type u_4
inst✝¹ : CommRing F
inst✝ : NormedField K
p : F[X]
f : F →+* K
B : ℝ
i : ℕ
h1 : Monic p
h2 : Splits f p
h3 : ∀ (z : K), z ∈ roots (map f p) → ‖z‖ ≤ B
hB : 0 ≤ B
hi : i ≤ natDegree (map f p)
r : ℝ
hr : r ∈ Multiset.map (fun x => ‖x‖) (Multiset.map prod (powersetLen (natDegree (map f p) - i) (roots (map f p))))
⊢ r ≤ B ^ (natDegree (map f p) - i)
[PROOFSTEP]
simp_rw [Multiset.mem_map] at hr
[GOAL]
α : Type u_1
R : Type u_2
inst✝³ : NormedRing R
inst✝² : IsAbsoluteValue norm
F : Type u_3
K : Type u_4
inst✝¹ : CommRing F
inst✝ : NormedField K
p : F[X]
f : F →+* K
B : ℝ
i : ℕ
h1 : Monic p
h2 : Splits f p
h3 : ∀ (z : K), z ∈ roots (map f p) → ‖z‖ ≤ B
hB : 0 ≤ B
hi : i ≤ natDegree (map f p)
r : ℝ
hr : ∃ a, (∃ a_1, a_1 ∈ powersetLen (natDegree (map f p) - i) (roots (map f p)) ∧ prod a_1 = a) ∧ ‖a‖ = r
⊢ r ≤ B ^ (natDegree (map f p) - i)
[PROOFSTEP]
obtain ⟨_, ⟨s, hs, rfl⟩, rfl⟩ := hr
[GOAL]
case intro.intro.intro.intro
α : Type u_1
R : Type u_2
inst✝³ : NormedRing R
inst✝² : IsAbsoluteValue norm
F : Type u_3
K : Type u_4
inst✝¹ : CommRing F
inst✝ : NormedField K
p : F[X]
f : F →+* K
B : ℝ
i : ℕ
h1 : Monic p
h2 : Splits f p
h3 : ∀ (z : K), z ∈ roots (map f p) → ‖z‖ ≤ B
hB : 0 ≤ B
hi : i ≤ natDegree (map f p)
s : Multiset K
hs : s ∈ powersetLen (natDegree (map f p) - i) (roots (map f p))
⊢ ‖prod s‖ ≤ B ^ (natDegree (map f p) - i)
[PROOFSTEP]
rw [mem_powersetLen] at hs
[GOAL]
case intro.intro.intro.intro
α : Type u_1
R : Type u_2
inst✝³ : NormedRing R
inst✝² : IsAbsoluteValue norm
F : Type u_3
K : Type u_4
inst✝¹ : CommRing F
inst✝ : NormedField K
p : F[X]
f : F →+* K
B : ℝ
i : ℕ
h1 : Monic p
h2 : Splits f p
h3 : ∀ (z : K), z ∈ roots (map f p) → ‖z‖ ≤ B
hB : 0 ≤ B
hi : i ≤ natDegree (map f p)
s : Multiset K
hs : s ≤ roots (map f p) ∧ ↑card s = natDegree (map f p) - i
⊢ ‖prod s‖ ≤ B ^ (natDegree (map f p) - i)
[PROOFSTEP]
lift B to ℝ≥0 using hB
[GOAL]
case intro.intro.intro.intro.intro
α : Type u_1
R : Type u_2
inst✝³ : NormedRing R
inst✝² : IsAbsoluteValue norm
F : Type u_3
K : Type u_4
inst✝¹ : CommRing F
inst✝ : NormedField K
p : F[X]
f : F →+* K
i : ℕ
h1 : Monic p
h2 : Splits f p
hi : i ≤ natDegree (map f p)
s : Multiset K
hs : s ≤ roots (map f p) ∧ ↑card s = natDegree (map f p) - i
B : ℝ≥0
h3 : ∀ (z : K), z ∈ roots (map f p) → ‖z‖ ≤ ↑B
⊢ ‖prod s‖ ≤ ↑B ^ (natDegree (map f p) - i)
[PROOFSTEP]
rw [← coe_nnnorm, ← NNReal.coe_pow, NNReal.coe_le_coe, ← nnnormHom_apply, ← MonoidHom.coe_coe,
  MonoidHom.map_multiset_prod]
[GOAL]
case intro.intro.intro.intro.intro
α : Type u_1
R : Type u_2
inst✝³ : NormedRing R
inst✝² : IsAbsoluteValue norm
F : Type u_3
K : Type u_4
inst✝¹ : CommRing F
inst✝ : NormedField K
p : F[X]
f : F →+* K
i : ℕ
h1 : Monic p
h2 : Splits f p
hi : i ≤ natDegree (map f p)
s : Multiset K
hs : s ≤ roots (map f p) ∧ ↑card s = natDegree (map f p) - i
B : ℝ≥0
h3 : ∀ (z : K), z ∈ roots (map f p) → ‖z‖ ≤ ↑B
⊢ prod (Multiset.map (↑↑nnnormHom) s) ≤ B ^ (natDegree (map f p) - i)
[PROOFSTEP]
refine' (prod_le_pow_card _ B fun x hx => _).trans_eq (by rw [card_map, hs.2])
[GOAL]
α : Type u_1
R : Type u_2
inst✝³ : NormedRing R
inst✝² : IsAbsoluteValue norm
F : Type u_3
K : Type u_4
inst✝¹ : CommRing F
inst✝ : NormedField K
p : F[X]
f : F →+* K
i : ℕ
h1 : Monic p
h2 : Splits f p
hi : i ≤ natDegree (map f p)
s : Multiset K
hs : s ≤ roots (map f p) ∧ ↑card s = natDegree (map f p) - i
B : ℝ≥0
h3 : ∀ (z : K), z ∈ roots (map f p) → ‖z‖ ≤ ↑B
⊢ B ^ ↑card (Multiset.map (↑↑nnnormHom) s) = B ^ (natDegree (map f p) - i)
[PROOFSTEP]
rw [card_map, hs.2]
[GOAL]
case intro.intro.intro.intro.intro
α : Type u_1
R : Type u_2
inst✝³ : NormedRing R
inst✝² : IsAbsoluteValue norm
F : Type u_3
K : Type u_4
inst✝¹ : CommRing F
inst✝ : NormedField K
p : F[X]
f : F →+* K
i : ℕ
h1 : Monic p
h2 : Splits f p
hi : i ≤ natDegree (map f p)
s : Multiset K
hs : s ≤ roots (map f p) ∧ ↑card s = natDegree (map f p) - i
B : ℝ≥0
h3 : ∀ (z : K), z ∈ roots (map f p) → ‖z‖ ≤ ↑B
x : ℝ≥0
hx : x ∈ Multiset.map (↑↑nnnormHom) s
⊢ x ≤ B
[PROOFSTEP]
obtain ⟨z, hz, rfl⟩ := Multiset.mem_map.1 hx
[GOAL]
case intro.intro.intro.intro.intro.intro.intro
α : Type u_1
R : Type u_2
inst✝³ : NormedRing R
inst✝² : IsAbsoluteValue norm
F : Type u_3
K : Type u_4
inst✝¹ : CommRing F
inst✝ : NormedField K
p : F[X]
f : F →+* K
i : ℕ
h1 : Monic p
h2 : Splits f p
hi : i ≤ natDegree (map f p)
s : Multiset K
hs : s ≤ roots (map f p) ∧ ↑card s = natDegree (map f p) - i
B : ℝ≥0
h3 : ∀ (z : K), z ∈ roots (map f p) → ‖z‖ ≤ ↑B
z : K
hz : z ∈ s
hx : ↑↑nnnormHom z ∈ Multiset.map (↑↑nnnormHom) s
⊢ ↑↑nnnormHom z ≤ B
[PROOFSTEP]
exact h3 z (mem_of_le hs.1 hz)
[GOAL]
α : Type u_1
R : Type u_2
inst✝³ : NormedRing R
inst✝² : IsAbsoluteValue norm
F : Type u_3
K : Type u_4
inst✝¹ : CommRing F
inst✝ : NormedField K
B : ℝ
d : ℕ
f : F →+* K
p : F[X]
h1 : Monic p
h2 : Splits f p
h3 : natDegree p ≤ d
h4 : ∀ (z : K), z ∈ roots (map f p) → ‖z‖ ≤ B
i : ℕ
⊢ ‖coeff (map f p) i‖ ≤ max B 1 ^ d * ↑(Nat.choose d (d / 2))
[PROOFSTEP]
obtain hB | hB := le_or_lt 0 B
[GOAL]
case inl
α : Type u_1
R : Type u_2
inst✝³ : NormedRing R
inst✝² : IsAbsoluteValue norm
F : Type u_3
K : Type u_4
inst✝¹ : CommRing F
inst✝ : NormedField K
B : ℝ
d : ℕ
f : F →+* K
p : F[X]
h1 : Monic p
h2 : Splits f p
h3 : natDegree p ≤ d
h4 : ∀ (z : K), z ∈ roots (map f p) → ‖z‖ ≤ B
i : ℕ
hB : 0 ≤ B
⊢ ‖coeff (map f p) i‖ ≤ max B 1 ^ d * ↑(Nat.choose d (d / 2))
[PROOFSTEP]
apply (coeff_le_of_roots_le i h1 h2 h4).trans
[GOAL]
case inl
α : Type u_1
R : Type u_2
inst✝³ : NormedRing R
inst✝² : IsAbsoluteValue norm
F : Type u_3
K : Type u_4
inst✝¹ : CommRing F
inst✝ : NormedField K
B : ℝ
d : ℕ
f : F →+* K
p : F[X]
h1 : Monic p
h2 : Splits f p
h3 : natDegree p ≤ d
h4 : ∀ (z : K), z ∈ roots (map f p) → ‖z‖ ≤ B
i : ℕ
hB : 0 ≤ B
⊢ B ^ (natDegree p - i) * ↑(Nat.choose (natDegree p) i) ≤ max B 1 ^ d * ↑(Nat.choose d (d / 2))
[PROOFSTEP]
calc
  _ ≤ max B 1 ^ (p.natDegree - i) * p.natDegree.choose i := by gcongr; apply le_max_left
  _ ≤ max B 1 ^ d * p.natDegree.choose i := by gcongr; apply le_max_right; exact le_trans (Nat.sub_le _ _) h3
  _ ≤ max B 1 ^ d * d.choose (d / 2) := by gcongr; exact (i.choose_mono h3).trans (i.choose_le_middle d)
[GOAL]
α : Type u_1
R : Type u_2
inst✝³ : NormedRing R
inst✝² : IsAbsoluteValue norm
F : Type u_3
K : Type u_4
inst✝¹ : CommRing F
inst✝ : NormedField K
B : ℝ
d : ℕ
f : F →+* K
p : F[X]
h1 : Monic p
h2 : Splits f p
h3 : natDegree p ≤ d
h4 : ∀ (z : K), z ∈ roots (map f p) → ‖z‖ ≤ B
i : ℕ
hB : 0 ≤ B
⊢ B ^ (natDegree p - i) * ↑(Nat.choose (natDegree p) i) ≤ max B 1 ^ (natDegree p - i) * ↑(Nat.choose (natDegree p) i)
[PROOFSTEP]
gcongr
[GOAL]
case h.hab
α : Type u_1
R : Type u_2
inst✝³ : NormedRing R
inst✝² : IsAbsoluteValue norm
F : Type u_3
K : Type u_4
inst✝¹ : CommRing F
inst✝ : NormedField K
B : ℝ
d : ℕ
f : F →+* K
p : F[X]
h1 : Monic p
h2 : Splits f p
h3 : natDegree p ≤ d
h4 : ∀ (z : K), z ∈ roots (map f p) → ‖z‖ ≤ B
i : ℕ
hB : 0 ≤ B
⊢ B ≤ max B 1
[PROOFSTEP]
apply le_max_left
[GOAL]
α : Type u_1
R : Type u_2
inst✝³ : NormedRing R
inst✝² : IsAbsoluteValue norm
F : Type u_3
K : Type u_4
inst✝¹ : CommRing F
inst✝ : NormedField K
B : ℝ
d : ℕ
f : F →+* K
p : F[X]
h1 : Monic p
h2 : Splits f p
h3 : natDegree p ≤ d
h4 : ∀ (z : K), z ∈ roots (map f p) → ‖z‖ ≤ B
i : ℕ
hB : 0 ≤ B
⊢ max B 1 ^ (natDegree p - i) * ↑(Nat.choose (natDegree p) i) ≤ max B 1 ^ d * ↑(Nat.choose (natDegree p) i)
[PROOFSTEP]
gcongr
[GOAL]
case h.ha
α : Type u_1
R : Type u_2
inst✝³ : NormedRing R
inst✝² : IsAbsoluteValue norm
F : Type u_3
K : Type u_4
inst✝¹ : CommRing F
inst✝ : NormedField K
B : ℝ
d : ℕ
f : F →+* K
p : F[X]
h1 : Monic p
h2 : Splits f p
h3 : natDegree p ≤ d
h4 : ∀ (z : K), z ∈ roots (map f p) → ‖z‖ ≤ B
i : ℕ
hB : 0 ≤ B
⊢ 1 ≤ max B 1
case h.h
α : Type u_1
R : Type u_2
inst✝³ : NormedRing R
inst✝² : IsAbsoluteValue norm
F : Type u_3
K : Type u_4
inst✝¹ : CommRing F
inst✝ : NormedField K
B : ℝ
d : ℕ
f : F →+* K
p : F[X]
h1 : Monic p
h2 : Splits f p
h3 : natDegree p ≤ d
h4 : ∀ (z : K), z ∈ roots (map f p) → ‖z‖ ≤ B
i : ℕ
hB : 0 ≤ B
⊢ natDegree p - i ≤ d
[PROOFSTEP]
apply le_max_right
[GOAL]
case h.h
α : Type u_1
R : Type u_2
inst✝³ : NormedRing R
inst✝² : IsAbsoluteValue norm
F : Type u_3
K : Type u_4
inst✝¹ : CommRing F
inst✝ : NormedField K
B : ℝ
d : ℕ
f : F →+* K
p : F[X]
h1 : Monic p
h2 : Splits f p
h3 : natDegree p ≤ d
h4 : ∀ (z : K), z ∈ roots (map f p) → ‖z‖ ≤ B
i : ℕ
hB : 0 ≤ B
⊢ natDegree p - i ≤ d
[PROOFSTEP]
exact le_trans (Nat.sub_le _ _) h3
[GOAL]
α : Type u_1
R : Type u_2
inst✝³ : NormedRing R
inst✝² : IsAbsoluteValue norm
F : Type u_3
K : Type u_4
inst✝¹ : CommRing F
inst✝ : NormedField K
B : ℝ
d : ℕ
f : F →+* K
p : F[X]
h1 : Monic p
h2 : Splits f p
h3 : natDegree p ≤ d
h4 : ∀ (z : K), z ∈ roots (map f p) → ‖z‖ ≤ B
i : ℕ
hB : 0 ≤ B
⊢ max B 1 ^ d * ↑(Nat.choose (natDegree p) i) ≤ max B 1 ^ d * ↑(Nat.choose d (d / 2))
[PROOFSTEP]
gcongr
[GOAL]
case h.h
α : Type u_1
R : Type u_2
inst✝³ : NormedRing R
inst✝² : IsAbsoluteValue norm
F : Type u_3
K : Type u_4
inst✝¹ : CommRing F
inst✝ : NormedField K
B : ℝ
d : ℕ
f : F →+* K
p : F[X]
h1 : Monic p
h2 : Splits f p
h3 : natDegree p ≤ d
h4 : ∀ (z : K), z ∈ roots (map f p) → ‖z‖ ≤ B
i : ℕ
hB : 0 ≤ B
⊢ Nat.choose (natDegree p) i ≤ Nat.choose d (d / 2)
[PROOFSTEP]
exact (i.choose_mono h3).trans (i.choose_le_middle d)
[GOAL]
case inr
α : Type u_1
R : Type u_2
inst✝³ : NormedRing R
inst✝² : IsAbsoluteValue norm
F : Type u_3
K : Type u_4
inst✝¹ : CommRing F
inst✝ : NormedField K
B : ℝ
d : ℕ
f : F →+* K
p : F[X]
h1 : Monic p
h2 : Splits f p
h3 : natDegree p ≤ d
h4 : ∀ (z : K), z ∈ roots (map f p) → ‖z‖ ≤ B
i : ℕ
hB : B < 0
⊢ ‖coeff (map f p) i‖ ≤ max B 1 ^ d * ↑(Nat.choose d (d / 2))
[PROOFSTEP]
rw [eq_one_of_roots_le hB h1 h2 h4, Polynomial.map_one, coeff_one]
[GOAL]
case inr
α : Type u_1
R : Type u_2
inst✝³ : NormedRing R
inst✝² : IsAbsoluteValue norm
F : Type u_3
K : Type u_4
inst✝¹ : CommRing F
inst✝ : NormedField K
B : ℝ
d : ℕ
f : F →+* K
p : F[X]
h1 : Monic p
h2 : Splits f p
h3 : natDegree p ≤ d
h4 : ∀ (z : K), z ∈ roots (map f p) → ‖z‖ ≤ B
i : ℕ
hB : B < 0
⊢ ‖if 0 = i then 1 else 0‖ ≤ max B 1 ^ d * ↑(Nat.choose d (d / 2))
[PROOFSTEP]
refine' _root_.trans _ (one_le_mul_of_one_le_of_one_le (one_le_pow_of_one_le (le_max_right B 1) d) _)
[GOAL]
case inr.refine'_1
α : Type u_1
R : Type u_2
inst✝³ : NormedRing R
inst✝² : IsAbsoluteValue norm
F : Type u_3
K : Type u_4
inst✝¹ : CommRing F
inst✝ : NormedField K
B : ℝ
d : ℕ
f : F →+* K
p : F[X]
h1 : Monic p
h2 : Splits f p
h3 : natDegree p ≤ d
h4 : ∀ (z : K), z ∈ roots (map f p) → ‖z‖ ≤ B
i : ℕ
hB : B < 0
⊢ ‖if 0 = i then 1 else 0‖ ≤ 1
[PROOFSTEP]
split_ifs
[GOAL]
case pos
α : Type u_1
R : Type u_2
inst✝³ : NormedRing R
inst✝² : IsAbsoluteValue norm
F : Type u_3
K : Type u_4
inst✝¹ : CommRing F
inst✝ : NormedField K
B : ℝ
d : ℕ
f : F →+* K
p : F[X]
h1 : Monic p
h2 : Splits f p
h3 : natDegree p ≤ d
h4 : ∀ (z : K), z ∈ roots (map f p) → ‖z‖ ≤ B
i : ℕ
hB : B < 0
h✝ : 0 = i
⊢ ‖1‖ ≤ 1
[PROOFSTEP]
norm_num
[GOAL]
case neg
α : Type u_1
R : Type u_2
inst✝³ : NormedRing R
inst✝² : IsAbsoluteValue norm
F : Type u_3
K : Type u_4
inst✝¹ : CommRing F
inst✝ : NormedField K
B : ℝ
d : ℕ
f : F →+* K
p : F[X]
h1 : Monic p
h2 : Splits f p
h3 : natDegree p ≤ d
h4 : ∀ (z : K), z ∈ roots (map f p) → ‖z‖ ≤ B
i : ℕ
hB : B < 0
h✝ : ¬0 = i
⊢ ‖0‖ ≤ 1
[PROOFSTEP]
norm_num
[GOAL]
case inr.refine'_2
α : Type u_1
R : Type u_2
inst✝³ : NormedRing R
inst✝² : IsAbsoluteValue norm
F : Type u_3
K : Type u_4
inst✝¹ : CommRing F
inst✝ : NormedField K
B : ℝ
d : ℕ
f : F →+* K
p : F[X]
h1 : Monic p
h2 : Splits f p
h3 : natDegree p ≤ d
h4 : ∀ (z : K), z ∈ roots (map f p) → ‖z‖ ≤ B
i : ℕ
hB : B < 0
⊢ 1 ≤ ↑(Nat.choose d (d / 2))
[PROOFSTEP]
exact_mod_cast Nat.succ_le_iff.mpr (Nat.choose_pos (d.div_le_self 2))


[GOAL]
ι : Type u_1
G : Type u_2
M : Type u_3
hom : Type u_4
inst✝⁶ : TopologicalSpace G
inst✝⁵ : UniformSpace M
inst✝⁴ : Group G
inst✝³ : Group M
inst✝² : TopologicalGroup G
inst✝¹ : UniformGroup M
inst✝ : MonoidHomClass hom G M
F : ι → hom
hf : EquicontinuousAt (FunLike.coe ∘ F) 1
⊢ Equicontinuous (FunLike.coe ∘ F)
[PROOFSTEP]
rw [equicontinuous_iff_continuous]
[GOAL]
ι : Type u_1
G : Type u_2
M : Type u_3
hom : Type u_4
inst✝⁶ : TopologicalSpace G
inst✝⁵ : UniformSpace M
inst✝⁴ : Group G
inst✝³ : Group M
inst✝² : TopologicalGroup G
inst✝¹ : UniformGroup M
inst✝ : MonoidHomClass hom G M
F : ι → hom
hf : EquicontinuousAt (FunLike.coe ∘ F) 1
⊢ Continuous (↑UniformFun.ofFun ∘ swap (FunLike.coe ∘ F))
[PROOFSTEP]
rw [equicontinuousAt_iff_continuousAt] at hf
[GOAL]
ι : Type u_1
G : Type u_2
M : Type u_3
hom : Type u_4
inst✝⁶ : TopologicalSpace G
inst✝⁵ : UniformSpace M
inst✝⁴ : Group G
inst✝³ : Group M
inst✝² : TopologicalGroup G
inst✝¹ : UniformGroup M
inst✝ : MonoidHomClass hom G M
F : ι → hom
hf : ContinuousAt (↑UniformFun.ofFun ∘ swap (FunLike.coe ∘ F)) 1
⊢ Continuous (↑UniformFun.ofFun ∘ swap (FunLike.coe ∘ F))
[PROOFSTEP]
let φ : G →* (ι →ᵤ M) :=
  { toFun := swap ((↑) ∘ F)
    map_one' := by dsimp [UniformFun]; ext; exact map_one _
    map_mul' := fun a b => by dsimp [UniformFun]; ext; exact map_mul _ _ _ }
[GOAL]
ι : Type u_1
G : Type u_2
M : Type u_3
hom : Type u_4
inst✝⁶ : TopologicalSpace G
inst✝⁵ : UniformSpace M
inst✝⁴ : Group G
inst✝³ : Group M
inst✝² : TopologicalGroup G
inst✝¹ : UniformGroup M
inst✝ : MonoidHomClass hom G M
F : ι → hom
hf : ContinuousAt (↑UniformFun.ofFun ∘ swap (FunLike.coe ∘ F)) 1
⊢ swap (FunLike.coe ∘ F) 1 = 1
[PROOFSTEP]
dsimp [UniformFun]
[GOAL]
ι : Type u_1
G : Type u_2
M : Type u_3
hom : Type u_4
inst✝⁶ : TopologicalSpace G
inst✝⁵ : UniformSpace M
inst✝⁴ : Group G
inst✝³ : Group M
inst✝² : TopologicalGroup G
inst✝¹ : UniformGroup M
inst✝ : MonoidHomClass hom G M
F : ι → hom
hf : ContinuousAt (↑UniformFun.ofFun ∘ swap (FunLike.coe ∘ F)) 1
⊢ swap (FunLike.coe ∘ F) 1 = 1
[PROOFSTEP]
ext
[GOAL]
case h
ι : Type u_1
G : Type u_2
M : Type u_3
hom : Type u_4
inst✝⁶ : TopologicalSpace G
inst✝⁵ : UniformSpace M
inst✝⁴ : Group G
inst✝³ : Group M
inst✝² : TopologicalGroup G
inst✝¹ : UniformGroup M
inst✝ : MonoidHomClass hom G M
F : ι → hom
hf : ContinuousAt (↑UniformFun.ofFun ∘ swap (FunLike.coe ∘ F)) 1
x✝ : ι
⊢ swap (FunLike.coe ∘ F) 1 x✝ = OfNat.ofNat 1 x✝
[PROOFSTEP]
exact map_one _
[GOAL]
ι : Type u_1
G : Type u_2
M : Type u_3
hom : Type u_4
inst✝⁶ : TopologicalSpace G
inst✝⁵ : UniformSpace M
inst✝⁴ : Group G
inst✝³ : Group M
inst✝² : TopologicalGroup G
inst✝¹ : UniformGroup M
inst✝ : MonoidHomClass hom G M
F : ι → hom
hf : ContinuousAt (↑UniformFun.ofFun ∘ swap (FunLike.coe ∘ F)) 1
a b : G
⊢ OneHom.toFun { toFun := swap (FunLike.coe ∘ F), map_one' := (_ : swap (FunLike.coe ∘ F) 1 = 1) } (a * b) =
    OneHom.toFun { toFun := swap (FunLike.coe ∘ F), map_one' := (_ : swap (FunLike.coe ∘ F) 1 = 1) } a *
      OneHom.toFun { toFun := swap (FunLike.coe ∘ F), map_one' := (_ : swap (FunLike.coe ∘ F) 1 = 1) } b
[PROOFSTEP]
dsimp [UniformFun]
[GOAL]
ι : Type u_1
G : Type u_2
M : Type u_3
hom : Type u_4
inst✝⁶ : TopologicalSpace G
inst✝⁵ : UniformSpace M
inst✝⁴ : Group G
inst✝³ : Group M
inst✝² : TopologicalGroup G
inst✝¹ : UniformGroup M
inst✝ : MonoidHomClass hom G M
F : ι → hom
hf : ContinuousAt (↑UniformFun.ofFun ∘ swap (FunLike.coe ∘ F)) 1
a b : G
⊢ swap (FunLike.coe ∘ F) (a * b) = swap (FunLike.coe ∘ F) a * swap (FunLike.coe ∘ F) b
[PROOFSTEP]
ext
[GOAL]
case h
ι : Type u_1
G : Type u_2
M : Type u_3
hom : Type u_4
inst✝⁶ : TopologicalSpace G
inst✝⁵ : UniformSpace M
inst✝⁴ : Group G
inst✝³ : Group M
inst✝² : TopologicalGroup G
inst✝¹ : UniformGroup M
inst✝ : MonoidHomClass hom G M
F : ι → hom
hf : ContinuousAt (↑UniformFun.ofFun ∘ swap (FunLike.coe ∘ F)) 1
a b : G
x✝ : ι
⊢ swap (FunLike.coe ∘ F) (a * b) x✝ = (swap (FunLike.coe ∘ F) a * swap (FunLike.coe ∘ F) b) x✝
[PROOFSTEP]
exact map_mul _ _ _
[GOAL]
ι : Type u_1
G : Type u_2
M : Type u_3
hom : Type u_4
inst✝⁶ : TopologicalSpace G
inst✝⁵ : UniformSpace M
inst✝⁴ : Group G
inst✝³ : Group M
inst✝² : TopologicalGroup G
inst✝¹ : UniformGroup M
inst✝ : MonoidHomClass hom G M
F : ι → hom
hf : ContinuousAt (↑UniformFun.ofFun ∘ swap (FunLike.coe ∘ F)) 1
φ : G →* ι →ᵤ M :=
  { toOneHom := { toFun := swap (FunLike.coe ∘ F), map_one' := (_ : swap (FunLike.coe ∘ F) 1 = 1) },
    map_mul' :=
      (_ :
        ∀ (a b : G),
          OneHom.toFun { toFun := swap (FunLike.coe ∘ F), map_one' := (_ : swap (FunLike.coe ∘ F) 1 = 1) } (a * b) =
            OneHom.toFun { toFun := swap (FunLike.coe ∘ F), map_one' := (_ : swap (FunLike.coe ∘ F) 1 = 1) } a *
              OneHom.toFun { toFun := swap (FunLike.coe ∘ F), map_one' := (_ : swap (FunLike.coe ∘ F) 1 = 1) } b) }
⊢ Continuous (↑UniformFun.ofFun ∘ swap (FunLike.coe ∘ F))
[PROOFSTEP]
exact continuous_of_continuousAt_one φ hf
[GOAL]
ι : Type u_1
G : Type u_2
M : Type u_3
hom : Type u_4
inst✝⁶ : UniformSpace G
inst✝⁵ : UniformSpace M
inst✝⁴ : Group G
inst✝³ : Group M
inst✝² : UniformGroup G
inst✝¹ : UniformGroup M
inst✝ : MonoidHomClass hom G M
F : ι → hom
hf : EquicontinuousAt (FunLike.coe ∘ F) 1
⊢ UniformEquicontinuous (FunLike.coe ∘ F)
[PROOFSTEP]
rw [uniformEquicontinuous_iff_uniformContinuous]
[GOAL]
ι : Type u_1
G : Type u_2
M : Type u_3
hom : Type u_4
inst✝⁶ : UniformSpace G
inst✝⁵ : UniformSpace M
inst✝⁴ : Group G
inst✝³ : Group M
inst✝² : UniformGroup G
inst✝¹ : UniformGroup M
inst✝ : MonoidHomClass hom G M
F : ι → hom
hf : EquicontinuousAt (FunLike.coe ∘ F) 1
⊢ UniformContinuous (↑UniformFun.ofFun ∘ swap (FunLike.coe ∘ F))
[PROOFSTEP]
rw [equicontinuousAt_iff_continuousAt] at hf
[GOAL]
ι : Type u_1
G : Type u_2
M : Type u_3
hom : Type u_4
inst✝⁶ : UniformSpace G
inst✝⁵ : UniformSpace M
inst✝⁴ : Group G
inst✝³ : Group M
inst✝² : UniformGroup G
inst✝¹ : UniformGroup M
inst✝ : MonoidHomClass hom G M
F : ι → hom
hf : ContinuousAt (↑UniformFun.ofFun ∘ swap (FunLike.coe ∘ F)) 1
⊢ UniformContinuous (↑UniformFun.ofFun ∘ swap (FunLike.coe ∘ F))
[PROOFSTEP]
let φ : G →* (ι →ᵤ M) :=
  { toFun := swap ((↑) ∘ F)
    map_one' := by dsimp [UniformFun]; ext; exact map_one _
    map_mul' := fun a b => by dsimp [UniformFun]; ext; exact map_mul _ _ _ }
[GOAL]
ι : Type u_1
G : Type u_2
M : Type u_3
hom : Type u_4
inst✝⁶ : UniformSpace G
inst✝⁵ : UniformSpace M
inst✝⁴ : Group G
inst✝³ : Group M
inst✝² : UniformGroup G
inst✝¹ : UniformGroup M
inst✝ : MonoidHomClass hom G M
F : ι → hom
hf : ContinuousAt (↑UniformFun.ofFun ∘ swap (FunLike.coe ∘ F)) 1
⊢ swap (FunLike.coe ∘ F) 1 = 1
[PROOFSTEP]
dsimp [UniformFun]
[GOAL]
ι : Type u_1
G : Type u_2
M : Type u_3
hom : Type u_4
inst✝⁶ : UniformSpace G
inst✝⁵ : UniformSpace M
inst✝⁴ : Group G
inst✝³ : Group M
inst✝² : UniformGroup G
inst✝¹ : UniformGroup M
inst✝ : MonoidHomClass hom G M
F : ι → hom
hf : ContinuousAt (↑UniformFun.ofFun ∘ swap (FunLike.coe ∘ F)) 1
⊢ swap (FunLike.coe ∘ F) 1 = 1
[PROOFSTEP]
ext
[GOAL]
case h
ι : Type u_1
G : Type u_2
M : Type u_3
hom : Type u_4
inst✝⁶ : UniformSpace G
inst✝⁵ : UniformSpace M
inst✝⁴ : Group G
inst✝³ : Group M
inst✝² : UniformGroup G
inst✝¹ : UniformGroup M
inst✝ : MonoidHomClass hom G M
F : ι → hom
hf : ContinuousAt (↑UniformFun.ofFun ∘ swap (FunLike.coe ∘ F)) 1
x✝ : ι
⊢ swap (FunLike.coe ∘ F) 1 x✝ = OfNat.ofNat 1 x✝
[PROOFSTEP]
exact map_one _
[GOAL]
ι : Type u_1
G : Type u_2
M : Type u_3
hom : Type u_4
inst✝⁶ : UniformSpace G
inst✝⁵ : UniformSpace M
inst✝⁴ : Group G
inst✝³ : Group M
inst✝² : UniformGroup G
inst✝¹ : UniformGroup M
inst✝ : MonoidHomClass hom G M
F : ι → hom
hf : ContinuousAt (↑UniformFun.ofFun ∘ swap (FunLike.coe ∘ F)) 1
a b : G
⊢ OneHom.toFun { toFun := swap (FunLike.coe ∘ F), map_one' := (_ : swap (FunLike.coe ∘ F) 1 = 1) } (a * b) =
    OneHom.toFun { toFun := swap (FunLike.coe ∘ F), map_one' := (_ : swap (FunLike.coe ∘ F) 1 = 1) } a *
      OneHom.toFun { toFun := swap (FunLike.coe ∘ F), map_one' := (_ : swap (FunLike.coe ∘ F) 1 = 1) } b
[PROOFSTEP]
dsimp [UniformFun]
[GOAL]
ι : Type u_1
G : Type u_2
M : Type u_3
hom : Type u_4
inst✝⁶ : UniformSpace G
inst✝⁵ : UniformSpace M
inst✝⁴ : Group G
inst✝³ : Group M
inst✝² : UniformGroup G
inst✝¹ : UniformGroup M
inst✝ : MonoidHomClass hom G M
F : ι → hom
hf : ContinuousAt (↑UniformFun.ofFun ∘ swap (FunLike.coe ∘ F)) 1
a b : G
⊢ swap (FunLike.coe ∘ F) (a * b) = swap (FunLike.coe ∘ F) a * swap (FunLike.coe ∘ F) b
[PROOFSTEP]
ext
[GOAL]
case h
ι : Type u_1
G : Type u_2
M : Type u_3
hom : Type u_4
inst✝⁶ : UniformSpace G
inst✝⁵ : UniformSpace M
inst✝⁴ : Group G
inst✝³ : Group M
inst✝² : UniformGroup G
inst✝¹ : UniformGroup M
inst✝ : MonoidHomClass hom G M
F : ι → hom
hf : ContinuousAt (↑UniformFun.ofFun ∘ swap (FunLike.coe ∘ F)) 1
a b : G
x✝ : ι
⊢ swap (FunLike.coe ∘ F) (a * b) x✝ = (swap (FunLike.coe ∘ F) a * swap (FunLike.coe ∘ F) b) x✝
[PROOFSTEP]
exact map_mul _ _ _
[GOAL]
ι : Type u_1
G : Type u_2
M : Type u_3
hom : Type u_4
inst✝⁶ : UniformSpace G
inst✝⁵ : UniformSpace M
inst✝⁴ : Group G
inst✝³ : Group M
inst✝² : UniformGroup G
inst✝¹ : UniformGroup M
inst✝ : MonoidHomClass hom G M
F : ι → hom
hf : ContinuousAt (↑UniformFun.ofFun ∘ swap (FunLike.coe ∘ F)) 1
φ : G →* ι →ᵤ M :=
  { toOneHom := { toFun := swap (FunLike.coe ∘ F), map_one' := (_ : swap (FunLike.coe ∘ F) 1 = 1) },
    map_mul' :=
      (_ :
        ∀ (a b : G),
          OneHom.toFun { toFun := swap (FunLike.coe ∘ F), map_one' := (_ : swap (FunLike.coe ∘ F) 1 = 1) } (a * b) =
            OneHom.toFun { toFun := swap (FunLike.coe ∘ F), map_one' := (_ : swap (FunLike.coe ∘ F) 1 = 1) } a *
              OneHom.toFun { toFun := swap (FunLike.coe ∘ F), map_one' := (_ : swap (FunLike.coe ∘ F) 1 = 1) } b) }
⊢ UniformContinuous (↑UniformFun.ofFun ∘ swap (FunLike.coe ∘ F))
[PROOFSTEP]
exact uniformContinuous_of_continuousAt_one φ hf


[GOAL]
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
U✝ V : OpenSubgroup G
g : G
inst✝ : ContinuousMul G
U : OpenSubgroup G
⊢ IsClosed ↑U
[PROOFSTEP]
apply isOpen_compl_iff.1
[GOAL]
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
U✝ V : OpenSubgroup G
g : G
inst✝ : ContinuousMul G
U : OpenSubgroup G
⊢ IsOpen (↑U)ᶜ
[PROOFSTEP]
refine' isOpen_iff_forall_mem_open.2 fun x hx => ⟨(fun y => y * x⁻¹) ⁻¹' U, _, _, _⟩
[GOAL]
case refine'_1
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
U✝ V : OpenSubgroup G
g : G
inst✝ : ContinuousMul G
U : OpenSubgroup G
x : G
hx : x ∈ (↑U)ᶜ
⊢ (fun y => y * x⁻¹) ⁻¹' ↑U ⊆ (↑U)ᶜ
[PROOFSTEP]
refine' fun u hux hu => hx _
[GOAL]
case refine'_1
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
U✝ V : OpenSubgroup G
g : G
inst✝ : ContinuousMul G
U : OpenSubgroup G
x : G
hx : x ∈ (↑U)ᶜ
u : G
hux : u ∈ (fun y => y * x⁻¹) ⁻¹' ↑U
hu : u ∈ ↑U
⊢ x ∈ ↑U
[PROOFSTEP]
simp only [Set.mem_preimage, SetLike.mem_coe] at hux hu ⊢
[GOAL]
case refine'_1
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
U✝ V : OpenSubgroup G
g : G
inst✝ : ContinuousMul G
U : OpenSubgroup G
x : G
hx : x ∈ (↑U)ᶜ
u : G
hux : u * x⁻¹ ∈ U
hu : u ∈ U
⊢ x ∈ U
[PROOFSTEP]
convert U.mul_mem (U.inv_mem hux) hu
[GOAL]
case a
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
U✝ V : OpenSubgroup G
g : G
inst✝ : ContinuousMul G
U : OpenSubgroup G
x : G
hx : x ∈ (↑U)ᶜ
u : G
hux : u * x⁻¹ ∈ U
hu : u ∈ U
⊢ x ∈ U ↔ (u * x⁻¹)⁻¹ * u ∈ ↑U
[PROOFSTEP]
simp
[GOAL]
case refine'_2
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
U✝ V : OpenSubgroup G
g : G
inst✝ : ContinuousMul G
U : OpenSubgroup G
x : G
hx : x ∈ (↑U)ᶜ
⊢ IsOpen ((fun y => y * x⁻¹) ⁻¹' ↑U)
[PROOFSTEP]
exact U.isOpen.preimage (continuous_mul_right _)
[GOAL]
case refine'_3
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
U✝ V : OpenSubgroup G
g : G
inst✝ : ContinuousMul G
U : OpenSubgroup G
x : G
hx : x ∈ (↑U)ᶜ
⊢ x ∈ (fun y => y * x⁻¹) ⁻¹' ↑U
[PROOFSTEP]
simp [one_mem]
[GOAL]
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : ContinuousMul G
H : Subgroup G
g : G
hg : ↑H ∈ 𝓝 g
⊢ IsOpen ↑H
[PROOFSTEP]
refine' isOpen_iff_mem_nhds.2 fun x hx => _
[GOAL]
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : ContinuousMul G
H : Subgroup G
g : G
hg : ↑H ∈ 𝓝 g
x : G
hx : x ∈ ↑H
⊢ ↑H ∈ 𝓝 x
[PROOFSTEP]
have hg' : g ∈ H := SetLike.mem_coe.1 (mem_of_mem_nhds hg)
[GOAL]
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : ContinuousMul G
H : Subgroup G
g : G
hg : ↑H ∈ 𝓝 g
x : G
hx : x ∈ ↑H
hg' : g ∈ H
⊢ ↑H ∈ 𝓝 x
[PROOFSTEP]
have : Filter.Tendsto (fun y => y * (x⁻¹ * g)) (𝓝 x) (𝓝 g) :=
  (continuous_id.mul continuous_const).tendsto' _ _ (mul_inv_cancel_left _ _)
[GOAL]
G : Type u_1
inst✝² : Group G
inst✝¹ : TopologicalSpace G
inst✝ : ContinuousMul G
H : Subgroup G
g : G
hg : ↑H ∈ 𝓝 g
x : G
hx : x ∈ ↑H
hg' : g ∈ H
this : Filter.Tendsto (fun y => y * (x⁻¹ * g)) (𝓝 x) (𝓝 g)
⊢ ↑H ∈ 𝓝 x
[PROOFSTEP]
simpa only [SetLike.mem_coe, Filter.mem_map', H.mul_mem_cancel_right (H.mul_mem (H.inv_mem hx) hg')] using this hg


[GOAL]
R : Type u_1
E : Type u_2
F : Type u_3
inst✝⁷ : AddCommGroup E
inst✝⁶ : TopologicalSpace E
inst✝⁵ : AddCommGroup F
inst✝⁴ : TopologicalSpace F
inst✝³ : TopologicalAddGroup F
inst✝² : Ring R
inst✝¹ : Module R E
inst✝ : Module R F
f : E →ᵃ[R] F
⊢ Continuous ↑f ↔ Continuous ↑f.linear
[PROOFSTEP]
constructor
[GOAL]
case mp
R : Type u_1
E : Type u_2
F : Type u_3
inst✝⁷ : AddCommGroup E
inst✝⁶ : TopologicalSpace E
inst✝⁵ : AddCommGroup F
inst✝⁴ : TopologicalSpace F
inst✝³ : TopologicalAddGroup F
inst✝² : Ring R
inst✝¹ : Module R E
inst✝ : Module R F
f : E →ᵃ[R] F
⊢ Continuous ↑f → Continuous ↑f.linear
[PROOFSTEP]
intro hc
[GOAL]
case mp
R : Type u_1
E : Type u_2
F : Type u_3
inst✝⁷ : AddCommGroup E
inst✝⁶ : TopologicalSpace E
inst✝⁵ : AddCommGroup F
inst✝⁴ : TopologicalSpace F
inst✝³ : TopologicalAddGroup F
inst✝² : Ring R
inst✝¹ : Module R E
inst✝ : Module R F
f : E →ᵃ[R] F
hc : Continuous ↑f
⊢ Continuous ↑f.linear
[PROOFSTEP]
rw [decomp' f]
[GOAL]
case mp
R : Type u_1
E : Type u_2
F : Type u_3
inst✝⁷ : AddCommGroup E
inst✝⁶ : TopologicalSpace E
inst✝⁵ : AddCommGroup F
inst✝⁴ : TopologicalSpace F
inst✝³ : TopologicalAddGroup F
inst✝² : Ring R
inst✝¹ : Module R E
inst✝ : Module R F
f : E →ᵃ[R] F
hc : Continuous ↑f
⊢ Continuous (↑f - fun x => ↑f 0)
[PROOFSTEP]
exact hc.sub continuous_const
[GOAL]
case mpr
R : Type u_1
E : Type u_2
F : Type u_3
inst✝⁷ : AddCommGroup E
inst✝⁶ : TopologicalSpace E
inst✝⁵ : AddCommGroup F
inst✝⁴ : TopologicalSpace F
inst✝³ : TopologicalAddGroup F
inst✝² : Ring R
inst✝¹ : Module R E
inst✝ : Module R F
f : E →ᵃ[R] F
⊢ Continuous ↑f.linear → Continuous ↑f
[PROOFSTEP]
intro hc
[GOAL]
case mpr
R : Type u_1
E : Type u_2
F : Type u_3
inst✝⁷ : AddCommGroup E
inst✝⁶ : TopologicalSpace E
inst✝⁵ : AddCommGroup F
inst✝⁴ : TopologicalSpace F
inst✝³ : TopologicalAddGroup F
inst✝² : Ring R
inst✝¹ : Module R E
inst✝ : Module R F
f : E →ᵃ[R] F
hc : Continuous ↑f.linear
⊢ Continuous ↑f
[PROOFSTEP]
rw [decomp f]
[GOAL]
case mpr
R : Type u_1
E : Type u_2
F : Type u_3
inst✝⁷ : AddCommGroup E
inst✝⁶ : TopologicalSpace E
inst✝⁵ : AddCommGroup F
inst✝⁴ : TopologicalSpace F
inst✝³ : TopologicalAddGroup F
inst✝² : Ring R
inst✝¹ : Module R E
inst✝ : Module R F
f : E →ᵃ[R] F
hc : Continuous ↑f.linear
⊢ Continuous (↑f.linear + fun x => ↑f 0)
[PROOFSTEP]
exact hc.add continuous_const
[GOAL]
R : Type u_1
E : Type u_2
F : Type u_3
inst✝⁷ : AddCommGroup E
inst✝⁶ : TopologicalSpace E
inst✝⁵ : AddCommGroup F
inst✝⁴ : TopologicalSpace F
inst✝³ : TopologicalAddGroup F
inst✝² : CommRing R
inst✝¹ : Module R F
inst✝ : ContinuousConstSMul R F
x : F
t : R
⊢ Continuous ↑(homothety x t)
[PROOFSTEP]
suffices ⇑(homothety x t) = fun y => t • (y - x) + x by
  rw [this]
  exact ((continuous_id.sub continuous_const).const_smul _).add continuous_const
[GOAL]
R : Type u_1
E : Type u_2
F : Type u_3
inst✝⁷ : AddCommGroup E
inst✝⁶ : TopologicalSpace E
inst✝⁵ : AddCommGroup F
inst✝⁴ : TopologicalSpace F
inst✝³ : TopologicalAddGroup F
inst✝² : CommRing R
inst✝¹ : Module R F
inst✝ : ContinuousConstSMul R F
x : F
t : R
this : ↑(homothety x t) = fun y => t • (y - x) + x
⊢ Continuous ↑(homothety x t)
[PROOFSTEP]
rw [this]
[GOAL]
R : Type u_1
E : Type u_2
F : Type u_3
inst✝⁷ : AddCommGroup E
inst✝⁶ : TopologicalSpace E
inst✝⁵ : AddCommGroup F
inst✝⁴ : TopologicalSpace F
inst✝³ : TopologicalAddGroup F
inst✝² : CommRing R
inst✝¹ : Module R F
inst✝ : ContinuousConstSMul R F
x : F
t : R
this : ↑(homothety x t) = fun y => t • (y - x) + x
⊢ Continuous fun y => t • (y - x) + x
[PROOFSTEP]
exact ((continuous_id.sub continuous_const).const_smul _).add continuous_const
[GOAL]
R : Type u_1
E : Type u_2
F : Type u_3
inst✝⁷ : AddCommGroup E
inst✝⁶ : TopologicalSpace E
inst✝⁵ : AddCommGroup F
inst✝⁴ : TopologicalSpace F
inst✝³ : TopologicalAddGroup F
inst✝² : CommRing R
inst✝¹ : Module R F
inst✝ : ContinuousConstSMul R F
x : F
t : R
⊢ ↑(homothety x t) = fun y => t • (y - x) + x
[PROOFSTEP]
ext y
[GOAL]
case h
R : Type u_1
E : Type u_2
F : Type u_3
inst✝⁷ : AddCommGroup E
inst✝⁶ : TopologicalSpace E
inst✝⁵ : AddCommGroup F
inst✝⁴ : TopologicalSpace F
inst✝³ : TopologicalAddGroup F
inst✝² : CommRing R
inst✝¹ : Module R F
inst✝ : ContinuousConstSMul R F
x : F
t : R
y : F
⊢ ↑(homothety x t) y = t • (y - x) + x
[PROOFSTEP]
simp [homothety_apply]
[GOAL]
R : Type u_1
E : Type u_2
F : Type u_3
inst✝⁷ : AddCommGroup E
inst✝⁶ : TopologicalSpace E
inst✝⁵ : AddCommGroup F
inst✝⁴ : TopologicalSpace F
inst✝³ : TopologicalAddGroup F
inst✝² : Field R
inst✝¹ : Module R F
inst✝ : ContinuousConstSMul R F
x : F
t : R
ht : t ≠ 0
⊢ IsOpenMap ↑(homothety x t)
[PROOFSTEP]
apply IsOpenMap.of_inverse (homothety_continuous x t⁻¹)
[GOAL]
case l_inv
R : Type u_1
E : Type u_2
F : Type u_3
inst✝⁷ : AddCommGroup E
inst✝⁶ : TopologicalSpace E
inst✝⁵ : AddCommGroup F
inst✝⁴ : TopologicalSpace F
inst✝³ : TopologicalAddGroup F
inst✝² : Field R
inst✝¹ : Module R F
inst✝ : ContinuousConstSMul R F
x : F
t : R
ht : t ≠ 0
⊢ Function.LeftInverse ↑(homothety x t) ↑(homothety x t⁻¹)
[PROOFSTEP]
intro e
[GOAL]
case r_inv
R : Type u_1
E : Type u_2
F : Type u_3
inst✝⁷ : AddCommGroup E
inst✝⁶ : TopologicalSpace E
inst✝⁵ : AddCommGroup F
inst✝⁴ : TopologicalSpace F
inst✝³ : TopologicalAddGroup F
inst✝² : Field R
inst✝¹ : Module R F
inst✝ : ContinuousConstSMul R F
x : F
t : R
ht : t ≠ 0
⊢ Function.RightInverse ↑(homothety x t) ↑(homothety x t⁻¹)
[PROOFSTEP]
intro e
[GOAL]
case l_inv
R : Type u_1
E : Type u_2
F : Type u_3
inst✝⁷ : AddCommGroup E
inst✝⁶ : TopologicalSpace E
inst✝⁵ : AddCommGroup F
inst✝⁴ : TopologicalSpace F
inst✝³ : TopologicalAddGroup F
inst✝² : Field R
inst✝¹ : Module R F
inst✝ : ContinuousConstSMul R F
x : F
t : R
ht : t ≠ 0
e : F
⊢ ↑(homothety x t) (↑(homothety x t⁻¹) e) = e
[PROOFSTEP]
simp [← AffineMap.comp_apply, ← homothety_mul, ht]
[GOAL]
case r_inv
R : Type u_1
E : Type u_2
F : Type u_3
inst✝⁷ : AddCommGroup E
inst✝⁶ : TopologicalSpace E
inst✝⁵ : AddCommGroup F
inst✝⁴ : TopologicalSpace F
inst✝³ : TopologicalAddGroup F
inst✝² : Field R
inst✝¹ : Module R F
inst✝ : ContinuousConstSMul R F
x : F
t : R
ht : t ≠ 0
e : F
⊢ ↑(homothety x t⁻¹) (↑(homothety x t) e) = e
[PROOFSTEP]
simp [← AffineMap.comp_apply, ← homothety_mul, ht]


[GOAL]
M : Type u_1
inst✝⁴ : Nonempty M
inst✝³ : Semigroup M
inst✝² : TopologicalSpace M
inst✝¹ : CompactSpace M
inst✝ : T2Space M
continuous_mul_left : ∀ (r : M), Continuous fun x => x * r
⊢ ∃ m, m * m = m
[PROOFSTEP]
let S : Set (Set M) := {N | IsClosed N ∧ N.Nonempty ∧ ∀ (m) (_ : m ∈ N) (m') (_ : m' ∈ N), m * m' ∈ N}
[GOAL]
M : Type u_1
inst✝⁴ : Nonempty M
inst✝³ : Semigroup M
inst✝² : TopologicalSpace M
inst✝¹ : CompactSpace M
inst✝ : T2Space M
continuous_mul_left : ∀ (r : M), Continuous fun x => x * r
S : Set (Set M) := {N | IsClosed N ∧ Set.Nonempty N ∧ ∀ (m : M), m ∈ N → ∀ (m' : M), m' ∈ N → m * m' ∈ N}
⊢ ∃ m, m * m = m
[PROOFSTEP]
obtain ⟨N, ⟨N_closed, ⟨m, hm⟩, N_mul⟩, N_minimal⟩ : ∃ N ∈ S, ∀ N' ∈ S, N' ⊆ N → N' = N
[GOAL]
M : Type u_1
inst✝⁴ : Nonempty M
inst✝³ : Semigroup M
inst✝² : TopologicalSpace M
inst✝¹ : CompactSpace M
inst✝ : T2Space M
continuous_mul_left : ∀ (r : M), Continuous fun x => x * r
S : Set (Set M) := {N | IsClosed N ∧ Set.Nonempty N ∧ ∀ (m : M), m ∈ N → ∀ (m' : M), m' ∈ N → m * m' ∈ N}
⊢ ∃ N, N ∈ S ∧ ∀ (N' : Set M), N' ∈ S → N' ⊆ N → N' = N
case intro.intro.intro.intro.intro
M : Type u_1
inst✝⁴ : Nonempty M
inst✝³ : Semigroup M
inst✝² : TopologicalSpace M
inst✝¹ : CompactSpace M
inst✝ : T2Space M
continuous_mul_left : ∀ (r : M), Continuous fun x => x * r
S : Set (Set M) := {N | IsClosed N ∧ Set.Nonempty N ∧ ∀ (m : M), m ∈ N → ∀ (m' : M), m' ∈ N → m * m' ∈ N}
N : Set M
N_minimal : ∀ (N' : Set M), N' ∈ S → N' ⊆ N → N' = N
N_closed : IsClosed N
N_mul : ∀ (m : M), m ∈ N → ∀ (m' : M), m' ∈ N → m * m' ∈ N
m : M
hm : m ∈ N
⊢ ∃ m, m * m = m
[PROOFSTEP]
rotate_left
  -- Porting note: restore to `rsuffices`
[GOAL]
case intro.intro.intro.intro.intro
M : Type u_1
inst✝⁴ : Nonempty M
inst✝³ : Semigroup M
inst✝² : TopologicalSpace M
inst✝¹ : CompactSpace M
inst✝ : T2Space M
continuous_mul_left : ∀ (r : M), Continuous fun x => x * r
S : Set (Set M) := {N | IsClosed N ∧ Set.Nonempty N ∧ ∀ (m : M), m ∈ N → ∀ (m' : M), m' ∈ N → m * m' ∈ N}
N : Set M
N_minimal : ∀ (N' : Set M), N' ∈ S → N' ⊆ N → N' = N
N_closed : IsClosed N
N_mul : ∀ (m : M), m ∈ N → ∀ (m' : M), m' ∈ N → m * m' ∈ N
m : M
hm : m ∈ N
⊢ ∃ m, m * m = m
[PROOFSTEP]
use m
[GOAL]
case h
M : Type u_1
inst✝⁴ : Nonempty M
inst✝³ : Semigroup M
inst✝² : TopologicalSpace M
inst✝¹ : CompactSpace M
inst✝ : T2Space M
continuous_mul_left : ∀ (r : M), Continuous fun x => x * r
S : Set (Set M) := {N | IsClosed N ∧ Set.Nonempty N ∧ ∀ (m : M), m ∈ N → ∀ (m' : M), m' ∈ N → m * m' ∈ N}
N : Set M
N_minimal : ∀ (N' : Set M), N' ∈ S → N' ⊆ N → N' = N
N_closed : IsClosed N
N_mul : ∀ (m : M), m ∈ N → ∀ (m' : M), m' ∈ N → m * m' ∈ N
m : M
hm : m ∈ N
⊢ m * m = m
[PROOFSTEP]
have scaling_eq_self : (· * m) '' N = N := by
  apply N_minimal
  · refine' ⟨(continuous_mul_left m).isClosedMap _ N_closed, ⟨_, ⟨m, hm, rfl⟩⟩, _⟩
    rintro _ ⟨m'', hm'', rfl⟩ _ ⟨m', hm', rfl⟩
    refine' ⟨m'' * m * m', N_mul _ (N_mul _ hm'' _ hm) _ hm', mul_assoc _ _ _⟩
  · rintro _ ⟨m', hm', rfl⟩
    exact N_mul _ hm' _ hm
[GOAL]
M : Type u_1
inst✝⁴ : Nonempty M
inst✝³ : Semigroup M
inst✝² : TopologicalSpace M
inst✝¹ : CompactSpace M
inst✝ : T2Space M
continuous_mul_left : ∀ (r : M), Continuous fun x => x * r
S : Set (Set M) := {N | IsClosed N ∧ Set.Nonempty N ∧ ∀ (m : M), m ∈ N → ∀ (m' : M), m' ∈ N → m * m' ∈ N}
N : Set M
N_minimal : ∀ (N' : Set M), N' ∈ S → N' ⊆ N → N' = N
N_closed : IsClosed N
N_mul : ∀ (m : M), m ∈ N → ∀ (m' : M), m' ∈ N → m * m' ∈ N
m : M
hm : m ∈ N
⊢ (fun x => x * m) '' N = N
[PROOFSTEP]
apply N_minimal
[GOAL]
case a
M : Type u_1
inst✝⁴ : Nonempty M
inst✝³ : Semigroup M
inst✝² : TopologicalSpace M
inst✝¹ : CompactSpace M
inst✝ : T2Space M
continuous_mul_left : ∀ (r : M), Continuous fun x => x * r
S : Set (Set M) := {N | IsClosed N ∧ Set.Nonempty N ∧ ∀ (m : M), m ∈ N → ∀ (m' : M), m' ∈ N → m * m' ∈ N}
N : Set M
N_minimal : ∀ (N' : Set M), N' ∈ S → N' ⊆ N → N' = N
N_closed : IsClosed N
N_mul : ∀ (m : M), m ∈ N → ∀ (m' : M), m' ∈ N → m * m' ∈ N
m : M
hm : m ∈ N
⊢ (fun x => x * m) '' N ∈ S
[PROOFSTEP]
refine' ⟨(continuous_mul_left m).isClosedMap _ N_closed, ⟨_, ⟨m, hm, rfl⟩⟩, _⟩
[GOAL]
case a
M : Type u_1
inst✝⁴ : Nonempty M
inst✝³ : Semigroup M
inst✝² : TopologicalSpace M
inst✝¹ : CompactSpace M
inst✝ : T2Space M
continuous_mul_left : ∀ (r : M), Continuous fun x => x * r
S : Set (Set M) := {N | IsClosed N ∧ Set.Nonempty N ∧ ∀ (m : M), m ∈ N → ∀ (m' : M), m' ∈ N → m * m' ∈ N}
N : Set M
N_minimal : ∀ (N' : Set M), N' ∈ S → N' ⊆ N → N' = N
N_closed : IsClosed N
N_mul : ∀ (m : M), m ∈ N → ∀ (m' : M), m' ∈ N → m * m' ∈ N
m : M
hm : m ∈ N
⊢ ∀ (m_1 : M), m_1 ∈ (fun x => x * m) '' N → ∀ (m' : M), m' ∈ (fun x => x * m) '' N → m_1 * m' ∈ (fun x => x * m) '' N
[PROOFSTEP]
rintro _ ⟨m'', hm'', rfl⟩ _ ⟨m', hm', rfl⟩
[GOAL]
case a.intro.intro.intro.intro
M : Type u_1
inst✝⁴ : Nonempty M
inst✝³ : Semigroup M
inst✝² : TopologicalSpace M
inst✝¹ : CompactSpace M
inst✝ : T2Space M
continuous_mul_left : ∀ (r : M), Continuous fun x => x * r
S : Set (Set M) := {N | IsClosed N ∧ Set.Nonempty N ∧ ∀ (m : M), m ∈ N → ∀ (m' : M), m' ∈ N → m * m' ∈ N}
N : Set M
N_minimal : ∀ (N' : Set M), N' ∈ S → N' ⊆ N → N' = N
N_closed : IsClosed N
N_mul : ∀ (m : M), m ∈ N → ∀ (m' : M), m' ∈ N → m * m' ∈ N
m : M
hm : m ∈ N
m'' : M
hm'' : m'' ∈ N
m' : M
hm' : m' ∈ N
⊢ (fun x => x * m) m'' * (fun x => x * m) m' ∈ (fun x => x * m) '' N
[PROOFSTEP]
refine' ⟨m'' * m * m', N_mul _ (N_mul _ hm'' _ hm) _ hm', mul_assoc _ _ _⟩
[GOAL]
case a
M : Type u_1
inst✝⁴ : Nonempty M
inst✝³ : Semigroup M
inst✝² : TopologicalSpace M
inst✝¹ : CompactSpace M
inst✝ : T2Space M
continuous_mul_left : ∀ (r : M), Continuous fun x => x * r
S : Set (Set M) := {N | IsClosed N ∧ Set.Nonempty N ∧ ∀ (m : M), m ∈ N → ∀ (m' : M), m' ∈ N → m * m' ∈ N}
N : Set M
N_minimal : ∀ (N' : Set M), N' ∈ S → N' ⊆ N → N' = N
N_closed : IsClosed N
N_mul : ∀ (m : M), m ∈ N → ∀ (m' : M), m' ∈ N → m * m' ∈ N
m : M
hm : m ∈ N
⊢ (fun x => x * m) '' N ⊆ N
[PROOFSTEP]
rintro _ ⟨m', hm', rfl⟩
[GOAL]
case a.intro.intro
M : Type u_1
inst✝⁴ : Nonempty M
inst✝³ : Semigroup M
inst✝² : TopologicalSpace M
inst✝¹ : CompactSpace M
inst✝ : T2Space M
continuous_mul_left : ∀ (r : M), Continuous fun x => x * r
S : Set (Set M) := {N | IsClosed N ∧ Set.Nonempty N ∧ ∀ (m : M), m ∈ N → ∀ (m' : M), m' ∈ N → m * m' ∈ N}
N : Set M
N_minimal : ∀ (N' : Set M), N' ∈ S → N' ⊆ N → N' = N
N_closed : IsClosed N
N_mul : ∀ (m : M), m ∈ N → ∀ (m' : M), m' ∈ N → m * m' ∈ N
m : M
hm : m ∈ N
m' : M
hm' : m' ∈ N
⊢ (fun x => x * m) m' ∈ N
[PROOFSTEP]
exact N_mul _ hm' _ hm
[GOAL]
case h
M : Type u_1
inst✝⁴ : Nonempty M
inst✝³ : Semigroup M
inst✝² : TopologicalSpace M
inst✝¹ : CompactSpace M
inst✝ : T2Space M
continuous_mul_left : ∀ (r : M), Continuous fun x => x * r
S : Set (Set M) := {N | IsClosed N ∧ Set.Nonempty N ∧ ∀ (m : M), m ∈ N → ∀ (m' : M), m' ∈ N → m * m' ∈ N}
N : Set M
N_minimal : ∀ (N' : Set M), N' ∈ S → N' ⊆ N → N' = N
N_closed : IsClosed N
N_mul : ∀ (m : M), m ∈ N → ∀ (m' : M), m' ∈ N → m * m' ∈ N
m : M
hm : m ∈ N
scaling_eq_self : (fun x => x * m) '' N = N
⊢ m * m = m
[PROOFSTEP]
have absorbing_eq_self : N ∩ {m' | m' * m = m} = N :=
  by
  apply N_minimal
  · refine' ⟨N_closed.inter ((T1Space.t1 m).preimage (continuous_mul_left m)), _, _⟩
    · rwa [← scaling_eq_self] at hm
    · rintro m'' ⟨mem'', eq'' : _ = m⟩ m' ⟨mem', eq' : _ = m⟩
      refine' ⟨N_mul _ mem'' _ mem', _⟩
      rw [Set.mem_setOf_eq, mul_assoc, eq', eq'']
  apply Set.inter_subset_left
[GOAL]
M : Type u_1
inst✝⁴ : Nonempty M
inst✝³ : Semigroup M
inst✝² : TopologicalSpace M
inst✝¹ : CompactSpace M
inst✝ : T2Space M
continuous_mul_left : ∀ (r : M), Continuous fun x => x * r
S : Set (Set M) := {N | IsClosed N ∧ Set.Nonempty N ∧ ∀ (m : M), m ∈ N → ∀ (m' : M), m' ∈ N → m * m' ∈ N}
N : Set M
N_minimal : ∀ (N' : Set M), N' ∈ S → N' ⊆ N → N' = N
N_closed : IsClosed N
N_mul : ∀ (m : M), m ∈ N → ∀ (m' : M), m' ∈ N → m * m' ∈ N
m : M
hm : m ∈ N
scaling_eq_self : (fun x => x * m) '' N = N
⊢ N ∩ {m' | m' * m = m} = N
[PROOFSTEP]
apply N_minimal
[GOAL]
case a
M : Type u_1
inst✝⁴ : Nonempty M
inst✝³ : Semigroup M
inst✝² : TopologicalSpace M
inst✝¹ : CompactSpace M
inst✝ : T2Space M
continuous_mul_left : ∀ (r : M), Continuous fun x => x * r
S : Set (Set M) := {N | IsClosed N ∧ Set.Nonempty N ∧ ∀ (m : M), m ∈ N → ∀ (m' : M), m' ∈ N → m * m' ∈ N}
N : Set M
N_minimal : ∀ (N' : Set M), N' ∈ S → N' ⊆ N → N' = N
N_closed : IsClosed N
N_mul : ∀ (m : M), m ∈ N → ∀ (m' : M), m' ∈ N → m * m' ∈ N
m : M
hm : m ∈ N
scaling_eq_self : (fun x => x * m) '' N = N
⊢ N ∩ {m' | m' * m = m} ∈ S
[PROOFSTEP]
refine' ⟨N_closed.inter ((T1Space.t1 m).preimage (continuous_mul_left m)), _, _⟩
[GOAL]
case a.refine'_1
M : Type u_1
inst✝⁴ : Nonempty M
inst✝³ : Semigroup M
inst✝² : TopologicalSpace M
inst✝¹ : CompactSpace M
inst✝ : T2Space M
continuous_mul_left : ∀ (r : M), Continuous fun x => x * r
S : Set (Set M) := {N | IsClosed N ∧ Set.Nonempty N ∧ ∀ (m : M), m ∈ N → ∀ (m' : M), m' ∈ N → m * m' ∈ N}
N : Set M
N_minimal : ∀ (N' : Set M), N' ∈ S → N' ⊆ N → N' = N
N_closed : IsClosed N
N_mul : ∀ (m : M), m ∈ N → ∀ (m' : M), m' ∈ N → m * m' ∈ N
m : M
hm : m ∈ N
scaling_eq_self : (fun x => x * m) '' N = N
⊢ Set.Nonempty (N ∩ {m' | m' * m = m})
[PROOFSTEP]
rwa [← scaling_eq_self] at hm
[GOAL]
case a.refine'_2
M : Type u_1
inst✝⁴ : Nonempty M
inst✝³ : Semigroup M
inst✝² : TopologicalSpace M
inst✝¹ : CompactSpace M
inst✝ : T2Space M
continuous_mul_left : ∀ (r : M), Continuous fun x => x * r
S : Set (Set M) := {N | IsClosed N ∧ Set.Nonempty N ∧ ∀ (m : M), m ∈ N → ∀ (m' : M), m' ∈ N → m * m' ∈ N}
N : Set M
N_minimal : ∀ (N' : Set M), N' ∈ S → N' ⊆ N → N' = N
N_closed : IsClosed N
N_mul : ∀ (m : M), m ∈ N → ∀ (m' : M), m' ∈ N → m * m' ∈ N
m : M
hm : m ∈ N
scaling_eq_self : (fun x => x * m) '' N = N
⊢ ∀ (m_1 : M), m_1 ∈ N ∩ {m' | m' * m = m} → ∀ (m' : M), m' ∈ N ∩ {m' | m' * m = m} → m_1 * m' ∈ N ∩ {m' | m' * m = m}
[PROOFSTEP]
rintro m'' ⟨mem'', eq'' : _ = m⟩ m' ⟨mem', eq' : _ = m⟩
[GOAL]
case a.refine'_2.intro.intro
M : Type u_1
inst✝⁴ : Nonempty M
inst✝³ : Semigroup M
inst✝² : TopologicalSpace M
inst✝¹ : CompactSpace M
inst✝ : T2Space M
continuous_mul_left : ∀ (r : M), Continuous fun x => x * r
S : Set (Set M) := {N | IsClosed N ∧ Set.Nonempty N ∧ ∀ (m : M), m ∈ N → ∀ (m' : M), m' ∈ N → m * m' ∈ N}
N : Set M
N_minimal : ∀ (N' : Set M), N' ∈ S → N' ⊆ N → N' = N
N_closed : IsClosed N
N_mul : ∀ (m : M), m ∈ N → ∀ (m' : M), m' ∈ N → m * m' ∈ N
m : M
hm : m ∈ N
scaling_eq_self : (fun x => x * m) '' N = N
m'' : M
mem'' : m'' ∈ N
eq'' : m'' * m = m
m' : M
mem' : m' ∈ N
eq' : m' * m = m
⊢ m'' * m' ∈ N ∩ {m' | m' * m = m}
[PROOFSTEP]
refine' ⟨N_mul _ mem'' _ mem', _⟩
[GOAL]
case a.refine'_2.intro.intro
M : Type u_1
inst✝⁴ : Nonempty M
inst✝³ : Semigroup M
inst✝² : TopologicalSpace M
inst✝¹ : CompactSpace M
inst✝ : T2Space M
continuous_mul_left : ∀ (r : M), Continuous fun x => x * r
S : Set (Set M) := {N | IsClosed N ∧ Set.Nonempty N ∧ ∀ (m : M), m ∈ N → ∀ (m' : M), m' ∈ N → m * m' ∈ N}
N : Set M
N_minimal : ∀ (N' : Set M), N' ∈ S → N' ⊆ N → N' = N
N_closed : IsClosed N
N_mul : ∀ (m : M), m ∈ N → ∀ (m' : M), m' ∈ N → m * m' ∈ N
m : M
hm : m ∈ N
scaling_eq_self : (fun x => x * m) '' N = N
m'' : M
mem'' : m'' ∈ N
eq'' : m'' * m = m
m' : M
mem' : m' ∈ N
eq' : m' * m = m
⊢ m'' * m' ∈ {m' | m' * m = m}
[PROOFSTEP]
rw [Set.mem_setOf_eq, mul_assoc, eq', eq'']
[GOAL]
case a
M : Type u_1
inst✝⁴ : Nonempty M
inst✝³ : Semigroup M
inst✝² : TopologicalSpace M
inst✝¹ : CompactSpace M
inst✝ : T2Space M
continuous_mul_left : ∀ (r : M), Continuous fun x => x * r
S : Set (Set M) := {N | IsClosed N ∧ Set.Nonempty N ∧ ∀ (m : M), m ∈ N → ∀ (m' : M), m' ∈ N → m * m' ∈ N}
N : Set M
N_minimal : ∀ (N' : Set M), N' ∈ S → N' ⊆ N → N' = N
N_closed : IsClosed N
N_mul : ∀ (m : M), m ∈ N → ∀ (m' : M), m' ∈ N → m * m' ∈ N
m : M
hm : m ∈ N
scaling_eq_self : (fun x => x * m) '' N = N
⊢ N ∩ {m' | m' * m = m} ⊆ N
[PROOFSTEP]
apply Set.inter_subset_left
[GOAL]
case h
M : Type u_1
inst✝⁴ : Nonempty M
inst✝³ : Semigroup M
inst✝² : TopologicalSpace M
inst✝¹ : CompactSpace M
inst✝ : T2Space M
continuous_mul_left : ∀ (r : M), Continuous fun x => x * r
S : Set (Set M) := {N | IsClosed N ∧ Set.Nonempty N ∧ ∀ (m : M), m ∈ N → ∀ (m' : M), m' ∈ N → m * m' ∈ N}
N : Set M
N_minimal : ∀ (N' : Set M), N' ∈ S → N' ⊆ N → N' = N
N_closed : IsClosed N
N_mul : ∀ (m : M), m ∈ N → ∀ (m' : M), m' ∈ N → m * m' ∈ N
m : M
hm : m ∈ N
scaling_eq_self : (fun x => x * m) '' N = N
absorbing_eq_self : N ∩ {m' | m' * m = m} = N
⊢ m * m = m
[PROOFSTEP]
rw [← absorbing_eq_self] at hm
[GOAL]
case h
M : Type u_1
inst✝⁴ : Nonempty M
inst✝³ : Semigroup M
inst✝² : TopologicalSpace M
inst✝¹ : CompactSpace M
inst✝ : T2Space M
continuous_mul_left : ∀ (r : M), Continuous fun x => x * r
S : Set (Set M) := {N | IsClosed N ∧ Set.Nonempty N ∧ ∀ (m : M), m ∈ N → ∀ (m' : M), m' ∈ N → m * m' ∈ N}
N : Set M
N_minimal : ∀ (N' : Set M), N' ∈ S → N' ⊆ N → N' = N
N_closed : IsClosed N
N_mul : ∀ (m : M), m ∈ N → ∀ (m' : M), m' ∈ N → m * m' ∈ N
m : M
hm : m ∈ N ∩ {m' | m' * m = m}
scaling_eq_self : (fun x => x * m) '' N = N
absorbing_eq_self : N ∩ {m' | m' * m = m} = N
⊢ m * m = m
[PROOFSTEP]
exact hm.2
[GOAL]
M : Type u_1
inst✝⁴ : Nonempty M
inst✝³ : Semigroup M
inst✝² : TopologicalSpace M
inst✝¹ : CompactSpace M
inst✝ : T2Space M
continuous_mul_left : ∀ (r : M), Continuous fun x => x * r
S : Set (Set M) := {N | IsClosed N ∧ Set.Nonempty N ∧ ∀ (m : M), m ∈ N → ∀ (m' : M), m' ∈ N → m * m' ∈ N}
⊢ ∃ N, N ∈ S ∧ ∀ (N' : Set M), N' ∈ S → N' ⊆ N → N' = N
[PROOFSTEP]
refine' zorn_superset _ fun c hcs hc => _
[GOAL]
M : Type u_1
inst✝⁴ : Nonempty M
inst✝³ : Semigroup M
inst✝² : TopologicalSpace M
inst✝¹ : CompactSpace M
inst✝ : T2Space M
continuous_mul_left : ∀ (r : M), Continuous fun x => x * r
S : Set (Set M) := {N | IsClosed N ∧ Set.Nonempty N ∧ ∀ (m : M), m ∈ N → ∀ (m' : M), m' ∈ N → m * m' ∈ N}
c : Set (Set M)
hcs : c ⊆ S
hc : IsChain (fun x x_1 => x ⊆ x_1) c
⊢ ∃ lb, lb ∈ S ∧ ∀ (s : Set M), s ∈ c → lb ⊆ s
[PROOFSTEP]
refine'
  ⟨⋂₀ c, ⟨isClosed_sInter fun t ht => (hcs ht).1, _, fun m hm m' hm' => _⟩, fun s hs => Set.sInter_subset_of_mem hs⟩
[GOAL]
case refine'_1
M : Type u_1
inst✝⁴ : Nonempty M
inst✝³ : Semigroup M
inst✝² : TopologicalSpace M
inst✝¹ : CompactSpace M
inst✝ : T2Space M
continuous_mul_left : ∀ (r : M), Continuous fun x => x * r
S : Set (Set M) := {N | IsClosed N ∧ Set.Nonempty N ∧ ∀ (m : M), m ∈ N → ∀ (m' : M), m' ∈ N → m * m' ∈ N}
c : Set (Set M)
hcs : c ⊆ S
hc : IsChain (fun x x_1 => x ⊆ x_1) c
⊢ Set.Nonempty (⋂₀ c)
[PROOFSTEP]
obtain rfl | hcnemp := c.eq_empty_or_nonempty
[GOAL]
case refine'_1.inl
M : Type u_1
inst✝⁴ : Nonempty M
inst✝³ : Semigroup M
inst✝² : TopologicalSpace M
inst✝¹ : CompactSpace M
inst✝ : T2Space M
continuous_mul_left : ∀ (r : M), Continuous fun x => x * r
S : Set (Set M) := {N | IsClosed N ∧ Set.Nonempty N ∧ ∀ (m : M), m ∈ N → ∀ (m' : M), m' ∈ N → m * m' ∈ N}
hcs : ∅ ⊆ S
hc : IsChain (fun x x_1 => x ⊆ x_1) ∅
⊢ Set.Nonempty (⋂₀ ∅)
[PROOFSTEP]
rw [Set.sInter_empty]
[GOAL]
case refine'_1.inl
M : Type u_1
inst✝⁴ : Nonempty M
inst✝³ : Semigroup M
inst✝² : TopologicalSpace M
inst✝¹ : CompactSpace M
inst✝ : T2Space M
continuous_mul_left : ∀ (r : M), Continuous fun x => x * r
S : Set (Set M) := {N | IsClosed N ∧ Set.Nonempty N ∧ ∀ (m : M), m ∈ N → ∀ (m' : M), m' ∈ N → m * m' ∈ N}
hcs : ∅ ⊆ S
hc : IsChain (fun x x_1 => x ⊆ x_1) ∅
⊢ Set.Nonempty Set.univ
[PROOFSTEP]
apply Set.univ_nonempty
[GOAL]
case refine'_1.inr
M : Type u_1
inst✝⁴ : Nonempty M
inst✝³ : Semigroup M
inst✝² : TopologicalSpace M
inst✝¹ : CompactSpace M
inst✝ : T2Space M
continuous_mul_left : ∀ (r : M), Continuous fun x => x * r
S : Set (Set M) := {N | IsClosed N ∧ Set.Nonempty N ∧ ∀ (m : M), m ∈ N → ∀ (m' : M), m' ∈ N → m * m' ∈ N}
c : Set (Set M)
hcs : c ⊆ S
hc : IsChain (fun x x_1 => x ⊆ x_1) c
hcnemp : Set.Nonempty c
⊢ Set.Nonempty (⋂₀ c)
[PROOFSTEP]
convert
  @IsCompact.nonempty_iInter_of_directed_nonempty_compact_closed _ _ _ hcnemp.coe_sort ((↑) : c → Set M) ?_ ?_ ?_ ?_
[GOAL]
case h.e'_2
M : Type u_1
inst✝⁴ : Nonempty M
inst✝³ : Semigroup M
inst✝² : TopologicalSpace M
inst✝¹ : CompactSpace M
inst✝ : T2Space M
continuous_mul_left : ∀ (r : M), Continuous fun x => x * r
S : Set (Set M) := {N | IsClosed N ∧ Set.Nonempty N ∧ ∀ (m : M), m ∈ N → ∀ (m' : M), m' ∈ N → m * m' ∈ N}
c : Set (Set M)
hcs : c ⊆ S
hc : IsChain (fun x x_1 => x ⊆ x_1) c
hcnemp : Set.Nonempty c
⊢ ⋂₀ c = ⋂ (i : ↑c), ↑i
[PROOFSTEP]
exact Set.sInter_eq_iInter
[GOAL]
case refine'_1.inr.convert_1
M : Type u_1
inst✝⁴ : Nonempty M
inst✝³ : Semigroup M
inst✝² : TopologicalSpace M
inst✝¹ : CompactSpace M
inst✝ : T2Space M
continuous_mul_left : ∀ (r : M), Continuous fun x => x * r
S : Set (Set M) := {N | IsClosed N ∧ Set.Nonempty N ∧ ∀ (m : M), m ∈ N → ∀ (m' : M), m' ∈ N → m * m' ∈ N}
c : Set (Set M)
hcs : c ⊆ S
hc : IsChain (fun x x_1 => x ⊆ x_1) c
hcnemp : Set.Nonempty c
⊢ Directed (fun x x_1 => x ⊇ x_1) Subtype.val
[PROOFSTEP]
refine' DirectedOn.directed_val (IsChain.directedOn hc.symm)
[GOAL]
case refine'_1.inr.convert_2
M : Type u_1
inst✝⁴ : Nonempty M
inst✝³ : Semigroup M
inst✝² : TopologicalSpace M
inst✝¹ : CompactSpace M
inst✝ : T2Space M
continuous_mul_left : ∀ (r : M), Continuous fun x => x * r
S : Set (Set M) := {N | IsClosed N ∧ Set.Nonempty N ∧ ∀ (m : M), m ∈ N → ∀ (m' : M), m' ∈ N → m * m' ∈ N}
c : Set (Set M)
hcs : c ⊆ S
hc : IsChain (fun x x_1 => x ⊆ x_1) c
hcnemp : Set.Nonempty c
⊢ ∀ (i : ↑c), Set.Nonempty ↑i
case refine'_1.inr.convert_3
M : Type u_1
inst✝⁴ : Nonempty M
inst✝³ : Semigroup M
inst✝² : TopologicalSpace M
inst✝¹ : CompactSpace M
inst✝ : T2Space M
continuous_mul_left : ∀ (r : M), Continuous fun x => x * r
S : Set (Set M) := {N | IsClosed N ∧ Set.Nonempty N ∧ ∀ (m : M), m ∈ N → ∀ (m' : M), m' ∈ N → m * m' ∈ N}
c : Set (Set M)
hcs : c ⊆ S
hc : IsChain (fun x x_1 => x ⊆ x_1) c
hcnemp : Set.Nonempty c
⊢ ∀ (i : ↑c), IsCompact ↑i
case refine'_1.inr.convert_4
M : Type u_1
inst✝⁴ : Nonempty M
inst✝³ : Semigroup M
inst✝² : TopologicalSpace M
inst✝¹ : CompactSpace M
inst✝ : T2Space M
continuous_mul_left : ∀ (r : M), Continuous fun x => x * r
S : Set (Set M) := {N | IsClosed N ∧ Set.Nonempty N ∧ ∀ (m : M), m ∈ N → ∀ (m' : M), m' ∈ N → m * m' ∈ N}
c : Set (Set M)
hcs : c ⊆ S
hc : IsChain (fun x x_1 => x ⊆ x_1) c
hcnemp : Set.Nonempty c
⊢ ∀ (i : ↑c), IsClosed ↑i
[PROOFSTEP]
exacts [fun i => (hcs i.prop).2.1, fun i => (hcs i.prop).1.isCompact, fun i => (hcs i.prop).1]
[GOAL]
case refine'_2
M : Type u_1
inst✝⁴ : Nonempty M
inst✝³ : Semigroup M
inst✝² : TopologicalSpace M
inst✝¹ : CompactSpace M
inst✝ : T2Space M
continuous_mul_left : ∀ (r : M), Continuous fun x => x * r
S : Set (Set M) := {N | IsClosed N ∧ Set.Nonempty N ∧ ∀ (m : M), m ∈ N → ∀ (m' : M), m' ∈ N → m * m' ∈ N}
c : Set (Set M)
hcs : c ⊆ S
hc : IsChain (fun x x_1 => x ⊆ x_1) c
m : M
hm : m ∈ ⋂₀ c
m' : M
hm' : m' ∈ ⋂₀ c
⊢ m * m' ∈ ⋂₀ c
[PROOFSTEP]
rw [Set.mem_sInter]
[GOAL]
case refine'_2
M : Type u_1
inst✝⁴ : Nonempty M
inst✝³ : Semigroup M
inst✝² : TopologicalSpace M
inst✝¹ : CompactSpace M
inst✝ : T2Space M
continuous_mul_left : ∀ (r : M), Continuous fun x => x * r
S : Set (Set M) := {N | IsClosed N ∧ Set.Nonempty N ∧ ∀ (m : M), m ∈ N → ∀ (m' : M), m' ∈ N → m * m' ∈ N}
c : Set (Set M)
hcs : c ⊆ S
hc : IsChain (fun x x_1 => x ⊆ x_1) c
m : M
hm : m ∈ ⋂₀ c
m' : M
hm' : m' ∈ ⋂₀ c
⊢ ∀ (t : Set M), t ∈ c → m * m' ∈ t
[PROOFSTEP]
exact fun t ht => (hcs ht).2.2 m (Set.mem_sInter.mp hm t ht) m' (Set.mem_sInter.mp hm' t ht)
[GOAL]
M : Type u_1
inst✝² : Semigroup M
inst✝¹ : TopologicalSpace M
inst✝ : T2Space M
continuous_mul_left : ∀ (r : M), Continuous fun x => x * r
s : Set M
snemp : Set.Nonempty s
s_compact : IsCompact s
s_add : ∀ (x : M), x ∈ s → ∀ (y : M), y ∈ s → x * y ∈ s
⊢ ∃ m, m ∈ s ∧ m * m = m
[PROOFSTEP]
let M' := { m // m ∈ s }
[GOAL]
M : Type u_1
inst✝² : Semigroup M
inst✝¹ : TopologicalSpace M
inst✝ : T2Space M
continuous_mul_left : ∀ (r : M), Continuous fun x => x * r
s : Set M
snemp : Set.Nonempty s
s_compact : IsCompact s
s_add : ∀ (x : M), x ∈ s → ∀ (y : M), y ∈ s → x * y ∈ s
M' : Type u_1 := { m // m ∈ s }
⊢ ∃ m, m ∈ s ∧ m * m = m
[PROOFSTEP]
letI : Semigroup M' :=
  { mul := fun p q => ⟨p.1 * q.1, s_add _ p.2 _ q.2⟩
    mul_assoc := fun p q r => Subtype.eq (mul_assoc _ _ _) }
[GOAL]
M : Type u_1
inst✝² : Semigroup M
inst✝¹ : TopologicalSpace M
inst✝ : T2Space M
continuous_mul_left : ∀ (r : M), Continuous fun x => x * r
s : Set M
snemp : Set.Nonempty s
s_compact : IsCompact s
s_add : ∀ (x : M), x ∈ s → ∀ (y : M), y ∈ s → x * y ∈ s
M' : Type u_1 := { m // m ∈ s }
this : Semigroup M' := Semigroup.mk (_ : ∀ (p q r : M'), p * q * r = p * (q * r))
⊢ ∃ m, m ∈ s ∧ m * m = m
[PROOFSTEP]
haveI : CompactSpace M' := isCompact_iff_compactSpace.mp s_compact
[GOAL]
M : Type u_1
inst✝² : Semigroup M
inst✝¹ : TopologicalSpace M
inst✝ : T2Space M
continuous_mul_left : ∀ (r : M), Continuous fun x => x * r
s : Set M
snemp : Set.Nonempty s
s_compact : IsCompact s
s_add : ∀ (x : M), x ∈ s → ∀ (y : M), y ∈ s → x * y ∈ s
M' : Type u_1 := { m // m ∈ s }
this✝ : Semigroup M' := Semigroup.mk (_ : ∀ (p q r : M'), p * q * r = p * (q * r))
this : CompactSpace M'
⊢ ∃ m, m ∈ s ∧ m * m = m
[PROOFSTEP]
haveI : Nonempty M' := nonempty_subtype.mpr snemp
[GOAL]
M : Type u_1
inst✝² : Semigroup M
inst✝¹ : TopologicalSpace M
inst✝ : T2Space M
continuous_mul_left : ∀ (r : M), Continuous fun x => x * r
s : Set M
snemp : Set.Nonempty s
s_compact : IsCompact s
s_add : ∀ (x : M), x ∈ s → ∀ (y : M), y ∈ s → x * y ∈ s
M' : Type u_1 := { m // m ∈ s }
this✝¹ : Semigroup M' := Semigroup.mk (_ : ∀ (p q r : M'), p * q * r = p * (q * r))
this✝ : CompactSpace M'
this : Nonempty M'
⊢ ∃ m, m ∈ s ∧ m * m = m
[PROOFSTEP]
have : ∀ p : M', Continuous (· * p) := fun p => ((continuous_mul_left p.1).comp continuous_subtype_val).subtype_mk _
[GOAL]
M : Type u_1
inst✝² : Semigroup M
inst✝¹ : TopologicalSpace M
inst✝ : T2Space M
continuous_mul_left : ∀ (r : M), Continuous fun x => x * r
s : Set M
snemp : Set.Nonempty s
s_compact : IsCompact s
s_add : ∀ (x : M), x ∈ s → ∀ (y : M), y ∈ s → x * y ∈ s
M' : Type u_1 := { m // m ∈ s }
this✝² : Semigroup M' := Semigroup.mk (_ : ∀ (p q r : M'), p * q * r = p * (q * r))
this✝¹ : CompactSpace M'
this✝ : Nonempty M'
this : ∀ (p : M'), Continuous fun x => x * p
⊢ ∃ m, m ∈ s ∧ m * m = m
[PROOFSTEP]
obtain ⟨⟨m, hm⟩, idem⟩ := exists_idempotent_of_compact_t2_of_continuous_mul_left this
[GOAL]
case intro.mk
M : Type u_1
inst✝² : Semigroup M
inst✝¹ : TopologicalSpace M
inst✝ : T2Space M
continuous_mul_left : ∀ (r : M), Continuous fun x => x * r
s : Set M
snemp : Set.Nonempty s
s_compact : IsCompact s
s_add : ∀ (x : M), x ∈ s → ∀ (y : M), y ∈ s → x * y ∈ s
M' : Type u_1 := { m // m ∈ s }
this✝² : Semigroup M' := Semigroup.mk (_ : ∀ (p q r : M'), p * q * r = p * (q * r))
this✝¹ : CompactSpace M'
this✝ : Nonempty M'
this : ∀ (p : M'), Continuous fun x => x * p
m : M
hm : m ∈ s
idem : { val := m, property := hm } * { val := m, property := hm } = { val := m, property := hm }
⊢ ∃ m, m ∈ s ∧ m * m = m
[PROOFSTEP]
exact ⟨m, hm, Subtype.ext_iff.mp idem⟩


[GOAL]
G : Type u_1
inst✝ : AddCommGroup G
B : AddGroupFilterBasis G
F : Filter G
⊢ Cauchy F ↔ NeBot F ∧ ∀ (U : Set G), U ∈ B → ∃ M, M ∈ F ∧ ∀ (x : G), x ∈ M → ∀ (y : G), y ∈ M → y - x ∈ U
[PROOFSTEP]
letI := B.uniformSpace
[GOAL]
G : Type u_1
inst✝ : AddCommGroup G
B : AddGroupFilterBasis G
F : Filter G
this : UniformSpace G := AddGroupFilterBasis.uniformSpace B
⊢ Cauchy F ↔ NeBot F ∧ ∀ (U : Set G), U ∈ B → ∃ M, M ∈ F ∧ ∀ (x : G), x ∈ M → ∀ (y : G), y ∈ M → y - x ∈ U
[PROOFSTEP]
haveI := B.uniformAddGroup
[GOAL]
G : Type u_1
inst✝ : AddCommGroup G
B : AddGroupFilterBasis G
F : Filter G
this✝ : UniformSpace G := AddGroupFilterBasis.uniformSpace B
this : UniformAddGroup G
⊢ Cauchy F ↔ NeBot F ∧ ∀ (U : Set G), U ∈ B → ∃ M, M ∈ F ∧ ∀ (x : G), x ∈ M → ∀ (y : G), y ∈ M → y - x ∈ U
[PROOFSTEP]
suffices F ×ˢ F ≤ uniformity G ↔ ∀ U ∈ B, ∃ M ∈ F, ∀ (x) (_ : x ∈ M) (y) (_ : y ∈ M), y - x ∈ U by
  constructor <;> rintro ⟨h', h⟩ <;> refine' ⟨h', _⟩ <;> [rwa [← this]; rwa [this]]
[GOAL]
G : Type u_1
inst✝ : AddCommGroup G
B : AddGroupFilterBasis G
F : Filter G
this✝¹ : UniformSpace G := AddGroupFilterBasis.uniformSpace B
this✝ : UniformAddGroup G
this : F ×ˢ F ≤ uniformity G ↔ ∀ (U : Set G), U ∈ B → ∃ M, M ∈ F ∧ ∀ (x : G), x ∈ M → ∀ (y : G), y ∈ M → y - x ∈ U
⊢ Cauchy F ↔ NeBot F ∧ ∀ (U : Set G), U ∈ B → ∃ M, M ∈ F ∧ ∀ (x : G), x ∈ M → ∀ (y : G), y ∈ M → y - x ∈ U
[PROOFSTEP]
constructor <;> rintro ⟨h', h⟩ <;> refine' ⟨h', _⟩ <;> [rwa [← this]; rwa [this]]
[GOAL]
G : Type u_1
inst✝ : AddCommGroup G
B : AddGroupFilterBasis G
F : Filter G
this✝¹ : UniformSpace G := AddGroupFilterBasis.uniformSpace B
this✝ : UniformAddGroup G
this : F ×ˢ F ≤ uniformity G ↔ ∀ (U : Set G), U ∈ B → ∃ M, M ∈ F ∧ ∀ (x : G), x ∈ M → ∀ (y : G), y ∈ M → y - x ∈ U
⊢ Cauchy F ↔ NeBot F ∧ ∀ (U : Set G), U ∈ B → ∃ M, M ∈ F ∧ ∀ (x : G), x ∈ M → ∀ (y : G), y ∈ M → y - x ∈ U
[PROOFSTEP]
constructor
[GOAL]
case mp
G : Type u_1
inst✝ : AddCommGroup G
B : AddGroupFilterBasis G
F : Filter G
this✝¹ : UniformSpace G := AddGroupFilterBasis.uniformSpace B
this✝ : UniformAddGroup G
this : F ×ˢ F ≤ uniformity G ↔ ∀ (U : Set G), U ∈ B → ∃ M, M ∈ F ∧ ∀ (x : G), x ∈ M → ∀ (y : G), y ∈ M → y - x ∈ U
⊢ Cauchy F → NeBot F ∧ ∀ (U : Set G), U ∈ B → ∃ M, M ∈ F ∧ ∀ (x : G), x ∈ M → ∀ (y : G), y ∈ M → y - x ∈ U
[PROOFSTEP]
rintro ⟨h', h⟩
[GOAL]
case mpr
G : Type u_1
inst✝ : AddCommGroup G
B : AddGroupFilterBasis G
F : Filter G
this✝¹ : UniformSpace G := AddGroupFilterBasis.uniformSpace B
this✝ : UniformAddGroup G
this : F ×ˢ F ≤ uniformity G ↔ ∀ (U : Set G), U ∈ B → ∃ M, M ∈ F ∧ ∀ (x : G), x ∈ M → ∀ (y : G), y ∈ M → y - x ∈ U
⊢ (NeBot F ∧ ∀ (U : Set G), U ∈ B → ∃ M, M ∈ F ∧ ∀ (x : G), x ∈ M → ∀ (y : G), y ∈ M → y - x ∈ U) → Cauchy F
[PROOFSTEP]
rintro ⟨h', h⟩
[GOAL]
case mp.intro
G : Type u_1
inst✝ : AddCommGroup G
B : AddGroupFilterBasis G
F : Filter G
this✝¹ : UniformSpace G := AddGroupFilterBasis.uniformSpace B
this✝ : UniformAddGroup G
this : F ×ˢ F ≤ uniformity G ↔ ∀ (U : Set G), U ∈ B → ∃ M, M ∈ F ∧ ∀ (x : G), x ∈ M → ∀ (y : G), y ∈ M → y - x ∈ U
h' : NeBot F
h : F ×ˢ F ≤ uniformity G
⊢ NeBot F ∧ ∀ (U : Set G), U ∈ B → ∃ M, M ∈ F ∧ ∀ (x : G), x ∈ M → ∀ (y : G), y ∈ M → y - x ∈ U
[PROOFSTEP]
refine' ⟨h', _⟩
[GOAL]
case mpr.intro
G : Type u_1
inst✝ : AddCommGroup G
B : AddGroupFilterBasis G
F : Filter G
this✝¹ : UniformSpace G := AddGroupFilterBasis.uniformSpace B
this✝ : UniformAddGroup G
this : F ×ˢ F ≤ uniformity G ↔ ∀ (U : Set G), U ∈ B → ∃ M, M ∈ F ∧ ∀ (x : G), x ∈ M → ∀ (y : G), y ∈ M → y - x ∈ U
h' : NeBot F
h : ∀ (U : Set G), U ∈ B → ∃ M, M ∈ F ∧ ∀ (x : G), x ∈ M → ∀ (y : G), y ∈ M → y - x ∈ U
⊢ Cauchy F
[PROOFSTEP]
refine' ⟨h', _⟩
[GOAL]
case mp.intro
G : Type u_1
inst✝ : AddCommGroup G
B : AddGroupFilterBasis G
F : Filter G
this✝¹ : UniformSpace G := AddGroupFilterBasis.uniformSpace B
this✝ : UniformAddGroup G
this : F ×ˢ F ≤ uniformity G ↔ ∀ (U : Set G), U ∈ B → ∃ M, M ∈ F ∧ ∀ (x : G), x ∈ M → ∀ (y : G), y ∈ M → y - x ∈ U
h' : NeBot F
h : F ×ˢ F ≤ uniformity G
⊢ ∀ (U : Set G), U ∈ B → ∃ M, M ∈ F ∧ ∀ (x : G), x ∈ M → ∀ (y : G), y ∈ M → y - x ∈ U
[PROOFSTEP]
rwa [← this]
[GOAL]
case mpr.intro
G : Type u_1
inst✝ : AddCommGroup G
B : AddGroupFilterBasis G
F : Filter G
this✝¹ : UniformSpace G := AddGroupFilterBasis.uniformSpace B
this✝ : UniformAddGroup G
this : F ×ˢ F ≤ uniformity G ↔ ∀ (U : Set G), U ∈ B → ∃ M, M ∈ F ∧ ∀ (x : G), x ∈ M → ∀ (y : G), y ∈ M → y - x ∈ U
h' : NeBot F
h : ∀ (U : Set G), U ∈ B → ∃ M, M ∈ F ∧ ∀ (x : G), x ∈ M → ∀ (y : G), y ∈ M → y - x ∈ U
⊢ F ×ˢ F ≤ uniformity G
[PROOFSTEP]
rwa [this]
[GOAL]
G : Type u_1
inst✝ : AddCommGroup G
B : AddGroupFilterBasis G
F : Filter G
this✝ : UniformSpace G := AddGroupFilterBasis.uniformSpace B
this : UniformAddGroup G
⊢ F ×ˢ F ≤ uniformity G ↔ ∀ (U : Set G), U ∈ B → ∃ M, M ∈ F ∧ ∀ (x : G), x ∈ M → ∀ (y : G), y ∈ M → y - x ∈ U
[PROOFSTEP]
rw [uniformity_eq_comap_nhds_zero G, ← map_le_iff_le_comap]
[GOAL]
G : Type u_1
inst✝ : AddCommGroup G
B : AddGroupFilterBasis G
F : Filter G
this✝ : UniformSpace G := AddGroupFilterBasis.uniformSpace B
this : UniformAddGroup G
⊢ map (fun x => x.snd - x.fst) (F ×ˢ F) ≤ nhds 0 ↔
    ∀ (U : Set G), U ∈ B → ∃ M, M ∈ F ∧ ∀ (x : G), x ∈ M → ∀ (y : G), y ∈ M → y - x ∈ U
[PROOFSTEP]
change Tendsto _ _ _ ↔ _
[GOAL]
G : Type u_1
inst✝ : AddCommGroup G
B : AddGroupFilterBasis G
F : Filter G
this✝ : UniformSpace G := AddGroupFilterBasis.uniformSpace B
this : UniformAddGroup G
⊢ Tendsto (fun x => x.snd - x.fst) (F ×ˢ F) (nhds 0) ↔
    ∀ (U : Set G), U ∈ B → ∃ M, M ∈ F ∧ ∀ (x : G), x ∈ M → ∀ (y : G), y ∈ M → y - x ∈ U
[PROOFSTEP]
simp [(basis_sets F).prod_self.tendsto_iff B.nhds_zero_hasBasis, @forall_swap (_ ∈ _) G]


[GOAL]
R : Type u
M : Type v
N : Type w
X : Type x
Y : Type y
inst✝⁵ : UniformSpace X
inst✝⁴ : UniformSpace Y
inst✝³ : SMul M X
inst✝² : SMul Mᵐᵒᵖ X
inst✝¹ : IsCentralScalar M X
inst✝ : UniformContinuousConstSMul M X
c : M
⊢ UniformContinuous ((fun x x_1 => x • x_1) (MulOpposite.op c))
[PROOFSTEP]
dsimp only
[GOAL]
R : Type u
M : Type v
N : Type w
X : Type x
Y : Type y
inst✝⁵ : UniformSpace X
inst✝⁴ : UniformSpace Y
inst✝³ : SMul M X
inst✝² : SMul Mᵐᵒᵖ X
inst✝¹ : IsCentralScalar M X
inst✝ : UniformContinuousConstSMul M X
c : M
⊢ UniformContinuous fun x => MulOpposite.op c • x
[PROOFSTEP]
simp_rw [op_smul_eq_smul]
[GOAL]
R : Type u
M : Type v
N : Type w
X : Type x
Y : Type y
inst✝⁵ : UniformSpace X
inst✝⁴ : UniformSpace Y
inst✝³ : SMul M X
inst✝² : SMul Mᵐᵒᵖ X
inst✝¹ : IsCentralScalar M X
inst✝ : UniformContinuousConstSMul M X
c : M
⊢ UniformContinuous fun x => c • x
[PROOFSTEP]
exact uniformContinuous_const_smul c
[GOAL]
R : Type u
M : Type v
N : Type w
X : Type x
Y : Type y
inst✝⁷ : UniformSpace X
inst✝⁶ : UniformSpace Y
inst✝⁵ : SMul M X
inst✝⁴ : SMul N X
inst✝³ : SMul M N
inst✝² : UniformContinuousConstSMul M X
inst✝¹ : UniformContinuousConstSMul N X
inst✝ : IsScalarTower M N X
m : M
n : N
x : Completion X
⊢ (m • n) • x = m • n • x
[PROOFSTEP]
have : _ = (_ : Completion X → Completion X) :=
  map_comp (uniformContinuous_const_smul m) (uniformContinuous_const_smul n)
[GOAL]
R : Type u
M : Type v
N : Type w
X : Type x
Y : Type y
inst✝⁷ : UniformSpace X
inst✝⁶ : UniformSpace Y
inst✝⁵ : SMul M X
inst✝⁴ : SMul N X
inst✝³ : SMul M N
inst✝² : UniformContinuousConstSMul M X
inst✝¹ : UniformContinuousConstSMul N X
inst✝ : IsScalarTower M N X
m : M
n : N
x : Completion X
this :
  Completion.map ((fun x x_1 => x • x_1) m) ∘ Completion.map ((fun x x_1 => x • x_1) n) =
    Completion.map ((fun x x_1 => x • x_1) m ∘ (fun x x_1 => x • x_1) n)
⊢ (m • n) • x = m • n • x
[PROOFSTEP]
refine' Eq.trans _ (congr_fun this.symm x)
[GOAL]
R : Type u
M : Type v
N : Type w
X : Type x
Y : Type y
inst✝⁷ : UniformSpace X
inst✝⁶ : UniformSpace Y
inst✝⁵ : SMul M X
inst✝⁴ : SMul N X
inst✝³ : SMul M N
inst✝² : UniformContinuousConstSMul M X
inst✝¹ : UniformContinuousConstSMul N X
inst✝ : IsScalarTower M N X
m : M
n : N
x : Completion X
this :
  Completion.map ((fun x x_1 => x • x_1) m) ∘ Completion.map ((fun x x_1 => x • x_1) n) =
    Completion.map ((fun x x_1 => x • x_1) m ∘ (fun x x_1 => x • x_1) n)
⊢ (m • n) • x = Completion.map ((fun x x_1 => x • x_1) m ∘ (fun x x_1 => x • x_1) n) x
[PROOFSTEP]
exact congr_arg (fun f => Completion.map f x) (funext (smul_assoc _ _))
[GOAL]
R : Type u
M : Type v
N : Type w
X : Type x
Y : Type y
inst✝⁶ : UniformSpace X
inst✝⁵ : UniformSpace Y
inst✝⁴ : SMul M X
inst✝³ : SMul N X
inst✝² : SMulCommClass M N X
inst✝¹ : UniformContinuousConstSMul M X
inst✝ : UniformContinuousConstSMul N X
m : M
n : N
x : Completion X
⊢ m • n • x = n • m • x
[PROOFSTEP]
have hmn : m • n • x = (Completion.map (SMul.smul m) ∘ Completion.map (SMul.smul n)) x := rfl
[GOAL]
R : Type u
M : Type v
N : Type w
X : Type x
Y : Type y
inst✝⁶ : UniformSpace X
inst✝⁵ : UniformSpace Y
inst✝⁴ : SMul M X
inst✝³ : SMul N X
inst✝² : SMulCommClass M N X
inst✝¹ : UniformContinuousConstSMul M X
inst✝ : UniformContinuousConstSMul N X
m : M
n : N
x : Completion X
hmn : m • n • x = (Completion.map (SMul.smul m) ∘ Completion.map (SMul.smul n)) x
⊢ m • n • x = n • m • x
[PROOFSTEP]
have hnm : n • m • x = (Completion.map (SMul.smul n) ∘ Completion.map (SMul.smul m)) x := rfl
[GOAL]
R : Type u
M : Type v
N : Type w
X : Type x
Y : Type y
inst✝⁶ : UniformSpace X
inst✝⁵ : UniformSpace Y
inst✝⁴ : SMul M X
inst✝³ : SMul N X
inst✝² : SMulCommClass M N X
inst✝¹ : UniformContinuousConstSMul M X
inst✝ : UniformContinuousConstSMul N X
m : M
n : N
x : Completion X
hmn : m • n • x = (Completion.map (SMul.smul m) ∘ Completion.map (SMul.smul n)) x
hnm : n • m • x = (Completion.map (SMul.smul n) ∘ Completion.map (SMul.smul m)) x
⊢ m • n • x = n • m • x
[PROOFSTEP]
rw [hmn, hnm, map_comp, map_comp]
[GOAL]
R : Type u
M : Type v
N : Type w
X : Type x
Y : Type y
inst✝⁶ : UniformSpace X
inst✝⁵ : UniformSpace Y
inst✝⁴ : SMul M X
inst✝³ : SMul N X
inst✝² : SMulCommClass M N X
inst✝¹ : UniformContinuousConstSMul M X
inst✝ : UniformContinuousConstSMul N X
m : M
n : N
x : Completion X
hmn : m • n • x = (Completion.map (SMul.smul m) ∘ Completion.map (SMul.smul n)) x
hnm : n • m • x = (Completion.map (SMul.smul n) ∘ Completion.map (SMul.smul m)) x
⊢ Completion.map (SMul.smul m ∘ SMul.smul n) x = Completion.map (SMul.smul n ∘ SMul.smul m) x
case hg
R : Type u
M : Type v
N : Type w
X : Type x
Y : Type y
inst✝⁶ : UniformSpace X
inst✝⁵ : UniformSpace Y
inst✝⁴ : SMul M X
inst✝³ : SMul N X
inst✝² : SMulCommClass M N X
inst✝¹ : UniformContinuousConstSMul M X
inst✝ : UniformContinuousConstSMul N X
m : M
n : N
x : Completion X
hmn : m • n • x = (Completion.map (SMul.smul m) ∘ Completion.map (SMul.smul n)) x
hnm : n • m • x = (Completion.map (SMul.smul n) ∘ Completion.map (SMul.smul m)) x
⊢ UniformContinuous (SMul.smul n)
case hf
R : Type u
M : Type v
N : Type w
X : Type x
Y : Type y
inst✝⁶ : UniformSpace X
inst✝⁵ : UniformSpace Y
inst✝⁴ : SMul M X
inst✝³ : SMul N X
inst✝² : SMulCommClass M N X
inst✝¹ : UniformContinuousConstSMul M X
inst✝ : UniformContinuousConstSMul N X
m : M
n : N
x : Completion X
hmn : m • n • x = (Completion.map (SMul.smul m) ∘ Completion.map (SMul.smul n)) x
hnm : n • m • x = (Completion.map (SMul.smul n) ∘ Completion.map (SMul.smul m)) x
⊢ UniformContinuous (SMul.smul m)
case hg
R : Type u
M : Type v
N : Type w
X : Type x
Y : Type y
inst✝⁶ : UniformSpace X
inst✝⁵ : UniformSpace Y
inst✝⁴ : SMul M X
inst✝³ : SMul N X
inst✝² : SMulCommClass M N X
inst✝¹ : UniformContinuousConstSMul M X
inst✝ : UniformContinuousConstSMul N X
m : M
n : N
x : Completion X
hmn : m • n • x = (Completion.map (SMul.smul m) ∘ Completion.map (SMul.smul n)) x
hnm : n • m • x = (Completion.map (SMul.smul n) ∘ Completion.map (SMul.smul m)) x
⊢ UniformContinuous (SMul.smul m)
case hf
R : Type u
M : Type v
N : Type w
X : Type x
Y : Type y
inst✝⁶ : UniformSpace X
inst✝⁵ : UniformSpace Y
inst✝⁴ : SMul M X
inst✝³ : SMul N X
inst✝² : SMulCommClass M N X
inst✝¹ : UniformContinuousConstSMul M X
inst✝ : UniformContinuousConstSMul N X
m : M
n : N
x : Completion X
hmn : m • n • x = (Completion.map (SMul.smul m) ∘ Completion.map (SMul.smul n)) x
hnm : n • m • x = (Completion.map (SMul.smul n) ∘ Completion.map (SMul.smul m)) x
⊢ UniformContinuous (SMul.smul n)
[PROOFSTEP]
exact congr_arg (fun f => Completion.map f x) (funext (smul_comm _ _))
[GOAL]
case hg
R : Type u
M : Type v
N : Type w
X : Type x
Y : Type y
inst✝⁶ : UniformSpace X
inst✝⁵ : UniformSpace Y
inst✝⁴ : SMul M X
inst✝³ : SMul N X
inst✝² : SMulCommClass M N X
inst✝¹ : UniformContinuousConstSMul M X
inst✝ : UniformContinuousConstSMul N X
m : M
n : N
x : Completion X
hmn : m • n • x = (Completion.map (SMul.smul m) ∘ Completion.map (SMul.smul n)) x
hnm : n • m • x = (Completion.map (SMul.smul n) ∘ Completion.map (SMul.smul m)) x
⊢ UniformContinuous (SMul.smul n)
case hf
R : Type u
M : Type v
N : Type w
X : Type x
Y : Type y
inst✝⁶ : UniformSpace X
inst✝⁵ : UniformSpace Y
inst✝⁴ : SMul M X
inst✝³ : SMul N X
inst✝² : SMulCommClass M N X
inst✝¹ : UniformContinuousConstSMul M X
inst✝ : UniformContinuousConstSMul N X
m : M
n : N
x : Completion X
hmn : m • n • x = (Completion.map (SMul.smul m) ∘ Completion.map (SMul.smul n)) x
hnm : n • m • x = (Completion.map (SMul.smul n) ∘ Completion.map (SMul.smul m)) x
⊢ UniformContinuous (SMul.smul m)
case hg
R : Type u
M : Type v
N : Type w
X : Type x
Y : Type y
inst✝⁶ : UniformSpace X
inst✝⁵ : UniformSpace Y
inst✝⁴ : SMul M X
inst✝³ : SMul N X
inst✝² : SMulCommClass M N X
inst✝¹ : UniformContinuousConstSMul M X
inst✝ : UniformContinuousConstSMul N X
m : M
n : N
x : Completion X
hmn : m • n • x = (Completion.map (SMul.smul m) ∘ Completion.map (SMul.smul n)) x
hnm : n • m • x = (Completion.map (SMul.smul n) ∘ Completion.map (SMul.smul m)) x
⊢ UniformContinuous (SMul.smul m)
case hf
R : Type u
M : Type v
N : Type w
X : Type x
Y : Type y
inst✝⁶ : UniformSpace X
inst✝⁵ : UniformSpace Y
inst✝⁴ : SMul M X
inst✝³ : SMul N X
inst✝² : SMulCommClass M N X
inst✝¹ : UniformContinuousConstSMul M X
inst✝ : UniformContinuousConstSMul N X
m : M
n : N
x : Completion X
hmn : m • n • x = (Completion.map (SMul.smul m) ∘ Completion.map (SMul.smul n)) x
hnm : n • m • x = (Completion.map (SMul.smul n) ∘ Completion.map (SMul.smul m)) x
⊢ UniformContinuous (SMul.smul n)
[PROOFSTEP]
repeat' exact uniformContinuous_const_smul _
[GOAL]
case hg
R : Type u
M : Type v
N : Type w
X : Type x
Y : Type y
inst✝⁶ : UniformSpace X
inst✝⁵ : UniformSpace Y
inst✝⁴ : SMul M X
inst✝³ : SMul N X
inst✝² : SMulCommClass M N X
inst✝¹ : UniformContinuousConstSMul M X
inst✝ : UniformContinuousConstSMul N X
m : M
n : N
x : Completion X
hmn : m • n • x = (Completion.map (SMul.smul m) ∘ Completion.map (SMul.smul n)) x
hnm : n • m • x = (Completion.map (SMul.smul n) ∘ Completion.map (SMul.smul m)) x
⊢ UniformContinuous (SMul.smul n)
[PROOFSTEP]
exact uniformContinuous_const_smul _
[GOAL]
case hf
R : Type u
M : Type v
N : Type w
X : Type x
Y : Type y
inst✝⁶ : UniformSpace X
inst✝⁵ : UniformSpace Y
inst✝⁴ : SMul M X
inst✝³ : SMul N X
inst✝² : SMulCommClass M N X
inst✝¹ : UniformContinuousConstSMul M X
inst✝ : UniformContinuousConstSMul N X
m : M
n : N
x : Completion X
hmn : m • n • x = (Completion.map (SMul.smul m) ∘ Completion.map (SMul.smul n)) x
hnm : n • m • x = (Completion.map (SMul.smul n) ∘ Completion.map (SMul.smul m)) x
⊢ UniformContinuous (SMul.smul m)
[PROOFSTEP]
exact uniformContinuous_const_smul _
[GOAL]
case hg
R : Type u
M : Type v
N : Type w
X : Type x
Y : Type y
inst✝⁶ : UniformSpace X
inst✝⁵ : UniformSpace Y
inst✝⁴ : SMul M X
inst✝³ : SMul N X
inst✝² : SMulCommClass M N X
inst✝¹ : UniformContinuousConstSMul M X
inst✝ : UniformContinuousConstSMul N X
m : M
n : N
x : Completion X
hmn : m • n • x = (Completion.map (SMul.smul m) ∘ Completion.map (SMul.smul n)) x
hnm : n • m • x = (Completion.map (SMul.smul n) ∘ Completion.map (SMul.smul m)) x
⊢ UniformContinuous (SMul.smul m)
[PROOFSTEP]
exact uniformContinuous_const_smul _
[GOAL]
case hf
R : Type u
M : Type v
N : Type w
X : Type x
Y : Type y
inst✝⁶ : UniformSpace X
inst✝⁵ : UniformSpace Y
inst✝⁴ : SMul M X
inst✝³ : SMul N X
inst✝² : SMulCommClass M N X
inst✝¹ : UniformContinuousConstSMul M X
inst✝ : UniformContinuousConstSMul N X
m : M
n : N
x : Completion X
hmn : m • n • x = (Completion.map (SMul.smul m) ∘ Completion.map (SMul.smul n)) x
hnm : n • m • x = (Completion.map (SMul.smul n) ∘ Completion.map (SMul.smul m)) x
⊢ UniformContinuous (SMul.smul n)
[PROOFSTEP]
exact uniformContinuous_const_smul _
[GOAL]
R : Type u
M : Type v
N : Type w
X : Type x
Y : Type y
inst✝⁴ : UniformSpace X
inst✝³ : UniformSpace Y
inst✝² : Monoid M
inst✝¹ : MulAction M X
inst✝ : UniformContinuousConstSMul M X
a : X
⊢ 1 • ↑X a = ↑X a
[PROOFSTEP]
rw [← coe_smul, one_smul]
[GOAL]
R : Type u
M : Type v
N : Type w
X : Type x
Y : Type y
inst✝⁴ : UniformSpace X
inst✝³ : UniformSpace Y
inst✝² : Monoid M
inst✝¹ : MulAction M X
inst✝ : UniformContinuousConstSMul M X
x y : M
a : X
⊢ (x * y) • ↑X a = x • y • ↑X a
[PROOFSTEP]
simp only [← coe_smul, mul_smul]