Theorem: LipschitzWith.is_const (Ray/Hartogs/Duals.lean)

State before:
G : Type
inst✝³ : NormedAddCommGroup G
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : SecondCountableTopology E
g : ℝ → ℝ
g0 : LipschitzWith 0 g
⊢ ∀ (x y : ℝ), g x = g y
Tactic:
intro x y
State after:
G : Type
inst✝³ : NormedAddCommGroup G
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : SecondCountableTopology E
g : ℝ → ℝ
g0 : LipschitzWith 0 g
x y : ℝ
⊢ g x = g y

State before:
G : Type
inst✝³ : NormedAddCommGroup G
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : SecondCountableTopology E
g : ℝ → ℝ
g0 : LipschitzWith 0 g
x y : ℝ
⊢ g x = g y
Tactic:
simpa only [ENNReal.coe_zero, zero_mul, nonpos_iff_eq_zero, edist_eq_zero] using g0 x y
State after:
no goals