[GOAL]
H : Type u
inst✝² : NormedAddCommGroup H
inst✝¹ : InnerProductSpace ℂ H
inst✝ : CompleteSpace H
S T : VonNeumannAlgebra H
h : (fun S => S.carrier) S = (fun S => S.carrier) T
⊢ S = T
[PROOFSTEP]
obtain ⟨⟨⟨⟨⟨⟨_, _⟩, _⟩, _⟩, _⟩, _⟩, _⟩ := S
[GOAL]
case mk.mk.mk.mk.mk.mk
H : Type u
inst✝² : NormedAddCommGroup H
inst✝¹ : InnerProductSpace ℂ H
inst✝ : CompleteSpace H
T : VonNeumannAlgebra H
carrier✝ : Set (H →L[ℂ] H)
mul_mem'✝ : ∀ {a b : H →L[ℂ] H}, a ∈ carrier✝ → b ∈ carrier✝ → a * b ∈ carrier✝
one_mem'✝ : 1 ∈ { carrier := carrier✝, mul_mem' := mul_mem'✝ }.carrier
add_mem'✝ :
  ∀ {a b : H →L[ℂ] H},
    a ∈
        { toSubsemigroup := { carrier := carrier✝, mul_mem' := mul_mem'✝ },
              one_mem' := one_mem'✝ }.toSubsemigroup.carrier →
      b ∈
          { toSubsemigroup := { carrier := carrier✝, mul_mem' := mul_mem'✝ },
                one_mem' := one_mem'✝ }.toSubsemigroup.carrier →
        a + b ∈
          { toSubsemigroup := { carrier := carrier✝, mul_mem' := mul_mem'✝ },
                one_mem' := one_mem'✝ }.toSubsemigroup.carrier
zero_mem'✝ :
  0 ∈ { toSubsemigroup := { carrier := carrier✝, mul_mem' := mul_mem'✝ }, one_mem' := one_mem'✝ }.toSubsemigroup.carrier
algebraMap_mem'✝ :
  ∀ (r : ℂ),
    ↑(algebraMap ℂ (H →L[ℂ] H)) r ∈
      { toSubmonoid := { toSubsemigroup := { carrier := carrier✝, mul_mem' := mul_mem'✝ }, one_mem' := one_mem'✝ },
              add_mem' := add_mem'✝, zero_mem' := zero_mem'✝ }.toSubmonoid.toSubsemigroup.carrier
star_mem'✝ :
  ∀ {a : H →L[ℂ] H},
    a ∈
        {
                  toSubsemiring :=
                    {
                      toSubmonoid :=
                        { toSubsemigroup := { carrier := carrier✝, mul_mem' := mul_mem'✝ }, one_mem' := one_mem'✝ },
                      add_mem' := add_mem'✝, zero_mem' := zero_mem'✝ },
                  algebraMap_mem' := algebraMap_mem'✝ }.toSubsemiring.toSubmonoid.toSubsemigroup.carrier →
      star a ∈
        {
                  toSubsemiring :=
                    {
                      toSubmonoid :=
                        { toSubsemigroup := { carrier := carrier✝, mul_mem' := mul_mem'✝ }, one_mem' := one_mem'✝ },
                      add_mem' := add_mem'✝, zero_mem' := zero_mem'✝ },
                  algebraMap_mem' := algebraMap_mem'✝ }.toSubsemiring.toSubmonoid.toSubsemigroup.carrier
centralizer_centralizer'✝ :
  Set.centralizer
      (Set.centralizer
        {
                    toSubalgebra :=
                      {
                        toSubsemiring :=
                          {
                            toSubmonoid :=
                              { toSubsemigroup := { carrier := carrier✝, mul_mem' := mul_mem'✝ },
                                one_mem' := one_mem'✝ },
                            add_mem' := add_mem'✝, zero_mem' := zero_mem'✝ },
                        algebraMap_mem' := algebraMap_mem'✝ },
                    star_mem' := star_mem'✝ }.toSubalgebra.toSubsemiring.toSubmonoid.toSubsemigroup.carrier) =
    {
                toSubalgebra :=
                  {
                    toSubsemiring :=
                      {
                        toSubmonoid :=
                          { toSubsemigroup := { carrier := carrier✝, mul_mem' := mul_mem'✝ }, one_mem' := one_mem'✝ },
                        add_mem' := add_mem'✝, zero_mem' := zero_mem'✝ },
                    algebraMap_mem' := algebraMap_mem'✝ },
                star_mem' := star_mem'✝ }.toSubalgebra.toSubsemiring.toSubmonoid.toSubsemigroup.carrier
h :
  (fun S => S.carrier)
      {
        toStarSubalgebra :=
          {
            toSubalgebra :=
              {
                toSubsemiring :=
                  {
                    toSubmonoid :=
                      { toSubsemigroup := { carrier := carrier✝, mul_mem' := mul_mem'✝ }, one_mem' := one_mem'✝ },
                    add_mem' := add_mem'✝, zero_mem' := zero_mem'✝ },
                algebraMap_mem' := algebraMap_mem'✝ },
            star_mem' := star_mem'✝ },
        centralizer_centralizer' := centralizer_centralizer'✝ } =
    (fun S => S.carrier) T
⊢ {
      toStarSubalgebra :=
        {
          toSubalgebra :=
            {
              toSubsemiring :=
                {
                  toSubmonoid :=
                    { toSubsemigroup := { carrier := carrier✝, mul_mem' := mul_mem'✝ }, one_mem' := one_mem'✝ },
                  add_mem' := add_mem'✝, zero_mem' := zero_mem'✝ },
              algebraMap_mem' := algebraMap_mem'✝ },
          star_mem' := star_mem'✝ },
      centralizer_centralizer' := centralizer_centralizer'✝ } =
    T
[PROOFSTEP]
cases T
[GOAL]
case mk.mk.mk.mk.mk.mk.mk
H : Type u
inst✝² : NormedAddCommGroup H
inst✝¹ : InnerProductSpace ℂ H
inst✝ : CompleteSpace H
carrier✝ : Set (H →L[ℂ] H)
mul_mem'✝ : ∀ {a b : H →L[ℂ] H}, a ∈ carrier✝ → b ∈ carrier✝ → a * b ∈ carrier✝
one_mem'✝ : 1 ∈ { carrier := carrier✝, mul_mem' := mul_mem'✝ }.carrier
add_mem'✝ :
  ∀ {a b : H →L[ℂ] H},
    a ∈
        { toSubsemigroup := { carrier := carrier✝, mul_mem' := mul_mem'✝ },
              one_mem' := one_mem'✝ }.toSubsemigroup.carrier →
      b ∈
          { toSubsemigroup := { carrier := carrier✝, mul_mem' := mul_mem'✝ },
                one_mem' := one_mem'✝ }.toSubsemigroup.carrier →
        a + b ∈
          { toSubsemigroup := { carrier := carrier✝, mul_mem' := mul_mem'✝ },
                one_mem' := one_mem'✝ }.toSubsemigroup.carrier
zero_mem'✝ :
  0 ∈ { toSubsemigroup := { carrier := carrier✝, mul_mem' := mul_mem'✝ }, one_mem' := one_mem'✝ }.toSubsemigroup.carrier
algebraMap_mem'✝ :
  ∀ (r : ℂ),
    ↑(algebraMap ℂ (H →L[ℂ] H)) r ∈
      { toSubmonoid := { toSubsemigroup := { carrier := carrier✝, mul_mem' := mul_mem'✝ }, one_mem' := one_mem'✝ },
              add_mem' := add_mem'✝, zero_mem' := zero_mem'✝ }.toSubmonoid.toSubsemigroup.carrier
star_mem'✝ :
  ∀ {a : H →L[ℂ] H},
    a ∈
        {
                  toSubsemiring :=
                    {
                      toSubmonoid :=
                        { toSubsemigroup := { carrier := carrier✝, mul_mem' := mul_mem'✝ }, one_mem' := one_mem'✝ },
                      add_mem' := add_mem'✝, zero_mem' := zero_mem'✝ },
                  algebraMap_mem' := algebraMap_mem'✝ }.toSubsemiring.toSubmonoid.toSubsemigroup.carrier →
      star a ∈
        {
                  toSubsemiring :=
                    {
                      toSubmonoid :=
                        { toSubsemigroup := { carrier := carrier✝, mul_mem' := mul_mem'✝ }, one_mem' := one_mem'✝ },
                      add_mem' := add_mem'✝, zero_mem' := zero_mem'✝ },
                  algebraMap_mem' := algebraMap_mem'✝ }.toSubsemiring.toSubmonoid.toSubsemigroup.carrier
centralizer_centralizer'✝¹ :
  Set.centralizer
      (Set.centralizer
        {
                    toSubalgebra :=
                      {
                        toSubsemiring :=
                          {
                            toSubmonoid :=
                              { toSubsemigroup := { carrier := carrier✝, mul_mem' := mul_mem'✝ },
                                one_mem' := one_mem'✝ },
                            add_mem' := add_mem'✝, zero_mem' := zero_mem'✝ },
                        algebraMap_mem' := algebraMap_mem'✝ },
                    star_mem' := star_mem'✝ }.toSubalgebra.toSubsemiring.toSubmonoid.toSubsemigroup.carrier) =
    {
                toSubalgebra :=
                  {
                    toSubsemiring :=
                      {
                        toSubmonoid :=
                          { toSubsemigroup := { carrier := carrier✝, mul_mem' := mul_mem'✝ }, one_mem' := one_mem'✝ },
                        add_mem' := add_mem'✝, zero_mem' := zero_mem'✝ },
                    algebraMap_mem' := algebraMap_mem'✝ },
                star_mem' := star_mem'✝ }.toSubalgebra.toSubsemiring.toSubmonoid.toSubsemigroup.carrier
toStarSubalgebra✝ : StarSubalgebra ℂ (H →L[ℂ] H)
centralizer_centralizer'✝ : Set.centralizer (Set.centralizer toStarSubalgebra✝.carrier) = toStarSubalgebra✝.carrier
h :
  (fun S => S.carrier)
      {
        toStarSubalgebra :=
          {
            toSubalgebra :=
              {
                toSubsemiring :=
                  {
                    toSubmonoid :=
                      { toSubsemigroup := { carrier := carrier✝, mul_mem' := mul_mem'✝ }, one_mem' := one_mem'✝ },
                    add_mem' := add_mem'✝, zero_mem' := zero_mem'✝ },
                algebraMap_mem' := algebraMap_mem'✝ },
            star_mem' := star_mem'✝ },
        centralizer_centralizer' := centralizer_centralizer'✝¹ } =
    (fun S => S.carrier)
      { toStarSubalgebra := toStarSubalgebra✝, centralizer_centralizer' := centralizer_centralizer'✝ }
⊢ {
      toStarSubalgebra :=
        {
          toSubalgebra :=
            {
              toSubsemiring :=
                {
                  toSubmonoid :=
                    { toSubsemigroup := { carrier := carrier✝, mul_mem' := mul_mem'✝ }, one_mem' := one_mem'✝ },
                  add_mem' := add_mem'✝, zero_mem' := zero_mem'✝ },
              algebraMap_mem' := algebraMap_mem'✝ },
          star_mem' := star_mem'✝ },
      centralizer_centralizer' := centralizer_centralizer'✝¹ } =
    { toStarSubalgebra := toStarSubalgebra✝, centralizer_centralizer' := centralizer_centralizer'✝ }
[PROOFSTEP]
congr
  -- porting note: `StarMemClass` should be in `Prop`?
[GOAL]
H : Type u
inst✝² : NormedAddCommGroup H
inst✝¹ : InnerProductSpace ℂ H
inst✝ : CompleteSpace H
S : VonNeumannAlgebra H
⊢ Set.centralizer
      (Set.centralizer
        (StarSubalgebra.centralizer ℂ ↑S).toSubalgebra.toSubsemiring.toSubmonoid.toSubsemigroup.carrier) =
    (StarSubalgebra.centralizer ℂ ↑S).toSubalgebra.toSubsemiring.toSubmonoid.toSubsemigroup.carrier
[PROOFSTEP]
simp
[GOAL]
H : Type u
inst✝² : NormedAddCommGroup H
inst✝¹ : InnerProductSpace ℂ H
inst✝ : CompleteSpace H
S : VonNeumannAlgebra H
⊢ ↑(commutant S) = Set.centralizer ↑S
[PROOFSTEP]
simp [commutant]
[GOAL]
H : Type u
inst✝² : NormedAddCommGroup H
inst✝¹ : InnerProductSpace ℂ H
inst✝ : CompleteSpace H
S : VonNeumannAlgebra H
z : H →L[ℂ] H
⊢ z ∈ commutant S ↔ ∀ (g : H →L[ℂ] H), g ∈ S → g * z = z * g
[PROOFSTEP]
rw [← SetLike.mem_coe, coe_commutant]
[GOAL]
H : Type u
inst✝² : NormedAddCommGroup H
inst✝¹ : InnerProductSpace ℂ H
inst✝ : CompleteSpace H
S : VonNeumannAlgebra H
z : H →L[ℂ] H
⊢ z ∈ Set.centralizer ↑S ↔ ∀ (g : H →L[ℂ] H), g ∈ S → g * z = z * g
[PROOFSTEP]
rfl
[GOAL]
H : Type u
inst✝² : NormedAddCommGroup H
inst✝¹ : InnerProductSpace ℂ H
inst✝ : CompleteSpace H
S : VonNeumannAlgebra H
⊢ ↑(commutant (commutant S)) = ↑S
[PROOFSTEP]
simp


[GOAL]
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
δ K ε x : ℝ
⊢ HasDerivAt (gronwallBound δ K ε) (K * gronwallBound δ K ε x + ε) x
[PROOFSTEP]
by_cases hK : K = 0
[GOAL]
case pos
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
δ K ε x : ℝ
hK : K = 0
⊢ HasDerivAt (gronwallBound δ K ε) (K * gronwallBound δ K ε x + ε) x
[PROOFSTEP]
subst K
[GOAL]
case pos
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
δ ε x : ℝ
⊢ HasDerivAt (gronwallBound δ 0 ε) (0 * gronwallBound δ 0 ε x + ε) x
[PROOFSTEP]
simp only [gronwallBound_K0, zero_mul, zero_add]
[GOAL]
case pos
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
δ ε x : ℝ
⊢ HasDerivAt (fun x => δ + ε * x) ε x
[PROOFSTEP]
convert ((hasDerivAt_id x).const_mul ε).const_add δ
[GOAL]
case h.e'_7
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
δ ε x : ℝ
⊢ ε = ε * 1
[PROOFSTEP]
rw [mul_one]
[GOAL]
case neg
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
δ K ε x : ℝ
hK : ¬K = 0
⊢ HasDerivAt (gronwallBound δ K ε) (K * gronwallBound δ K ε x + ε) x
[PROOFSTEP]
simp only [gronwallBound_of_K_ne_0 hK]
[GOAL]
case neg
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
δ K ε x : ℝ
hK : ¬K = 0
⊢ HasDerivAt (fun x => δ * exp (K * x) + ε / K * (exp (K * x) - 1))
    (K * (δ * exp (K * x) + ε / K * (exp (K * x) - 1)) + ε) x
[PROOFSTEP]
convert
  (((hasDerivAt_id x).const_mul K).exp.const_mul δ).add
    ((((hasDerivAt_id x).const_mul K).exp.sub_const 1).const_mul (ε / K)) using
  1
[GOAL]
case h.e'_7
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
δ K ε x : ℝ
hK : ¬K = 0
⊢ K * (δ * exp (K * x) + ε / K * (exp (K * x) - 1)) + ε =
    δ * (exp (K * id x) * (K * 1)) + ε / K * (exp (K * id x) * (K * 1))
[PROOFSTEP]
simp only [id, mul_add, (mul_assoc _ _ _).symm, mul_comm _ K, mul_div_cancel' _ hK]
[GOAL]
case h.e'_7
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
δ K ε x : ℝ
hK : ¬K = 0
⊢ K * δ * exp (K * x) + ε * (exp (K * x) - 1) + ε = K * δ * exp (K * x) * 1 + ε * exp (K * x) * 1
[PROOFSTEP]
ring
[GOAL]
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
δ K ε x a : ℝ
⊢ HasDerivAt (fun y => gronwallBound δ K ε (y - a)) (K * gronwallBound δ K ε (x - a) + ε) x
[PROOFSTEP]
convert (hasDerivAt_gronwallBound δ K ε _).comp x ((hasDerivAt_id x).sub_const a) using 1
[GOAL]
case h.e'_7
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
δ K ε x a : ℝ
⊢ K * gronwallBound δ K ε (x - a) + ε = (K * gronwallBound δ K ε (id x - a) + ε) * 1
[PROOFSTEP]
rw [id, mul_one]
[GOAL]
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
δ K ε : ℝ
⊢ gronwallBound δ K ε 0 = δ
[PROOFSTEP]
by_cases hK : K = 0
[GOAL]
case pos
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
δ K ε : ℝ
hK : K = 0
⊢ gronwallBound δ K ε 0 = δ
[PROOFSTEP]
simp only [gronwallBound, if_pos hK, mul_zero, add_zero]
[GOAL]
case neg
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
δ K ε : ℝ
hK : ¬K = 0
⊢ gronwallBound δ K ε 0 = δ
[PROOFSTEP]
simp only [gronwallBound, if_neg hK, mul_zero, exp_zero, sub_self, mul_one, add_zero]
[GOAL]
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
δ K x : ℝ
⊢ gronwallBound δ K 0 x = δ * exp (K * x)
[PROOFSTEP]
by_cases hK : K = 0
[GOAL]
case pos
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
δ K x : ℝ
hK : K = 0
⊢ gronwallBound δ K 0 x = δ * exp (K * x)
[PROOFSTEP]
simp only [gronwallBound_K0, hK, zero_mul, exp_zero, add_zero, mul_one]
[GOAL]
case neg
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
δ K x : ℝ
hK : ¬K = 0
⊢ gronwallBound δ K 0 x = δ * exp (K * x)
[PROOFSTEP]
simp only [gronwallBound_of_K_ne_0 hK, zero_div, zero_mul, add_zero]
[GOAL]
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
K x : ℝ
⊢ gronwallBound 0 K 0 x = 0
[PROOFSTEP]
simp only [gronwallBound_ε0, zero_mul]
[GOAL]
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
δ K x : ℝ
⊢ Continuous fun ε => gronwallBound δ K ε x
[PROOFSTEP]
by_cases hK : K = 0
[GOAL]
case pos
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
δ K x : ℝ
hK : K = 0
⊢ Continuous fun ε => gronwallBound δ K ε x
[PROOFSTEP]
simp only [gronwallBound_K0, hK]
[GOAL]
case pos
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
δ K x : ℝ
hK : K = 0
⊢ Continuous fun ε => δ + ε * x
[PROOFSTEP]
exact continuous_const.add (continuous_id.mul continuous_const)
[GOAL]
case neg
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
δ K x : ℝ
hK : ¬K = 0
⊢ Continuous fun ε => gronwallBound δ K ε x
[PROOFSTEP]
simp only [gronwallBound_of_K_ne_0 hK]
[GOAL]
case neg
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
δ K x : ℝ
hK : ¬K = 0
⊢ Continuous fun ε => δ * exp (K * x) + ε / K * (exp (K * x) - 1)
[PROOFSTEP]
exact continuous_const.add ((continuous_id.mul continuous_const).mul continuous_const)
[GOAL]
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f f' : ℝ → ℝ
δ K ε a b : ℝ
hf : ContinuousOn f (Icc a b)
hf' : ∀ (x : ℝ), x ∈ Ico a b → ∀ (r : ℝ), f' x < r → ∃ᶠ (z : ℝ) in 𝓝[Ioi x] x, (z - x)⁻¹ * (f z - f x) < r
ha : f a ≤ δ
bound : ∀ (x : ℝ), x ∈ Ico a b → f' x ≤ K * f x + ε
⊢ ∀ (x : ℝ), x ∈ Icc a b → f x ≤ gronwallBound δ K ε (x - a)
[PROOFSTEP]
have H : ∀ x ∈ Icc a b, ∀ ε' ∈ Ioi ε, f x ≤ gronwallBound δ K ε' (x - a) :=
  by
  intro x hx ε' hε'
  apply image_le_of_liminf_slope_right_lt_deriv_boundary hf hf'
  · rwa [sub_self, gronwallBound_x0]
  · exact fun x => hasDerivAt_gronwallBound_shift δ K ε' x a
  · intro x hx hfB
    rw [← hfB]
    apply lt_of_le_of_lt (bound x hx)
    exact add_lt_add_left (mem_Ioi.1 hε') _
  · exact hx
[GOAL]
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f f' : ℝ → ℝ
δ K ε a b : ℝ
hf : ContinuousOn f (Icc a b)
hf' : ∀ (x : ℝ), x ∈ Ico a b → ∀ (r : ℝ), f' x < r → ∃ᶠ (z : ℝ) in 𝓝[Ioi x] x, (z - x)⁻¹ * (f z - f x) < r
ha : f a ≤ δ
bound : ∀ (x : ℝ), x ∈ Ico a b → f' x ≤ K * f x + ε
⊢ ∀ (x : ℝ), x ∈ Icc a b → ∀ (ε' : ℝ), ε' ∈ Ioi ε → f x ≤ gronwallBound δ K ε' (x - a)
[PROOFSTEP]
intro x hx ε' hε'
[GOAL]
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f f' : ℝ → ℝ
δ K ε a b : ℝ
hf : ContinuousOn f (Icc a b)
hf' : ∀ (x : ℝ), x ∈ Ico a b → ∀ (r : ℝ), f' x < r → ∃ᶠ (z : ℝ) in 𝓝[Ioi x] x, (z - x)⁻¹ * (f z - f x) < r
ha : f a ≤ δ
bound : ∀ (x : ℝ), x ∈ Ico a b → f' x ≤ K * f x + ε
x : ℝ
hx : x ∈ Icc a b
ε' : ℝ
hε' : ε' ∈ Ioi ε
⊢ f x ≤ gronwallBound δ K ε' (x - a)
[PROOFSTEP]
apply image_le_of_liminf_slope_right_lt_deriv_boundary hf hf'
[GOAL]
case ha
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f f' : ℝ → ℝ
δ K ε a b : ℝ
hf : ContinuousOn f (Icc a b)
hf' : ∀ (x : ℝ), x ∈ Ico a b → ∀ (r : ℝ), f' x < r → ∃ᶠ (z : ℝ) in 𝓝[Ioi x] x, (z - x)⁻¹ * (f z - f x) < r
ha : f a ≤ δ
bound : ∀ (x : ℝ), x ∈ Ico a b → f' x ≤ K * f x + ε
x : ℝ
hx : x ∈ Icc a b
ε' : ℝ
hε' : ε' ∈ Ioi ε
⊢ f a ≤ gronwallBound δ K ε' (a - a)
[PROOFSTEP]
rwa [sub_self, gronwallBound_x0]
[GOAL]
case hB
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f f' : ℝ → ℝ
δ K ε a b : ℝ
hf : ContinuousOn f (Icc a b)
hf' : ∀ (x : ℝ), x ∈ Ico a b → ∀ (r : ℝ), f' x < r → ∃ᶠ (z : ℝ) in 𝓝[Ioi x] x, (z - x)⁻¹ * (f z - f x) < r
ha : f a ≤ δ
bound : ∀ (x : ℝ), x ∈ Ico a b → f' x ≤ K * f x + ε
x : ℝ
hx : x ∈ Icc a b
ε' : ℝ
hε' : ε' ∈ Ioi ε
⊢ ∀ (x : ℝ), HasDerivAt (fun x => gronwallBound δ K ε' (x - a)) (?m.35213 x) x
[PROOFSTEP]
exact fun x => hasDerivAt_gronwallBound_shift δ K ε' x a
[GOAL]
case bound
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f f' : ℝ → ℝ
δ K ε a b : ℝ
hf : ContinuousOn f (Icc a b)
hf' : ∀ (x : ℝ), x ∈ Ico a b → ∀ (r : ℝ), f' x < r → ∃ᶠ (z : ℝ) in 𝓝[Ioi x] x, (z - x)⁻¹ * (f z - f x) < r
ha : f a ≤ δ
bound : ∀ (x : ℝ), x ∈ Ico a b → f' x ≤ K * f x + ε
x : ℝ
hx : x ∈ Icc a b
ε' : ℝ
hε' : ε' ∈ Ioi ε
⊢ ∀ (x : ℝ), x ∈ Ico a b → f x = gronwallBound δ K ε' (x - a) → f' x < K * gronwallBound δ K ε' (x - a) + ε'
[PROOFSTEP]
intro x hx hfB
[GOAL]
case bound
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f f' : ℝ → ℝ
δ K ε a b : ℝ
hf : ContinuousOn f (Icc a b)
hf' : ∀ (x : ℝ), x ∈ Ico a b → ∀ (r : ℝ), f' x < r → ∃ᶠ (z : ℝ) in 𝓝[Ioi x] x, (z - x)⁻¹ * (f z - f x) < r
ha : f a ≤ δ
bound : ∀ (x : ℝ), x ∈ Ico a b → f' x ≤ K * f x + ε
x✝ : ℝ
hx✝ : x✝ ∈ Icc a b
ε' : ℝ
hε' : ε' ∈ Ioi ε
x : ℝ
hx : x ∈ Ico a b
hfB : f x = gronwallBound δ K ε' (x - a)
⊢ f' x < K * gronwallBound δ K ε' (x - a) + ε'
[PROOFSTEP]
rw [← hfB]
[GOAL]
case bound
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f f' : ℝ → ℝ
δ K ε a b : ℝ
hf : ContinuousOn f (Icc a b)
hf' : ∀ (x : ℝ), x ∈ Ico a b → ∀ (r : ℝ), f' x < r → ∃ᶠ (z : ℝ) in 𝓝[Ioi x] x, (z - x)⁻¹ * (f z - f x) < r
ha : f a ≤ δ
bound : ∀ (x : ℝ), x ∈ Ico a b → f' x ≤ K * f x + ε
x✝ : ℝ
hx✝ : x✝ ∈ Icc a b
ε' : ℝ
hε' : ε' ∈ Ioi ε
x : ℝ
hx : x ∈ Ico a b
hfB : f x = gronwallBound δ K ε' (x - a)
⊢ f' x < K * f x + ε'
[PROOFSTEP]
apply lt_of_le_of_lt (bound x hx)
[GOAL]
case bound
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f f' : ℝ → ℝ
δ K ε a b : ℝ
hf : ContinuousOn f (Icc a b)
hf' : ∀ (x : ℝ), x ∈ Ico a b → ∀ (r : ℝ), f' x < r → ∃ᶠ (z : ℝ) in 𝓝[Ioi x] x, (z - x)⁻¹ * (f z - f x) < r
ha : f a ≤ δ
bound : ∀ (x : ℝ), x ∈ Ico a b → f' x ≤ K * f x + ε
x✝ : ℝ
hx✝ : x✝ ∈ Icc a b
ε' : ℝ
hε' : ε' ∈ Ioi ε
x : ℝ
hx : x ∈ Ico a b
hfB : f x = gronwallBound δ K ε' (x - a)
⊢ K * f x + ε < K * f x + ε'
[PROOFSTEP]
exact add_lt_add_left (mem_Ioi.1 hε') _
[GOAL]
case a
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f f' : ℝ → ℝ
δ K ε a b : ℝ
hf : ContinuousOn f (Icc a b)
hf' : ∀ (x : ℝ), x ∈ Ico a b → ∀ (r : ℝ), f' x < r → ∃ᶠ (z : ℝ) in 𝓝[Ioi x] x, (z - x)⁻¹ * (f z - f x) < r
ha : f a ≤ δ
bound : ∀ (x : ℝ), x ∈ Ico a b → f' x ≤ K * f x + ε
x : ℝ
hx : x ∈ Icc a b
ε' : ℝ
hε' : ε' ∈ Ioi ε
⊢ x ∈ Icc a b
[PROOFSTEP]
exact hx
[GOAL]
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f f' : ℝ → ℝ
δ K ε a b : ℝ
hf : ContinuousOn f (Icc a b)
hf' : ∀ (x : ℝ), x ∈ Ico a b → ∀ (r : ℝ), f' x < r → ∃ᶠ (z : ℝ) in 𝓝[Ioi x] x, (z - x)⁻¹ * (f z - f x) < r
ha : f a ≤ δ
bound : ∀ (x : ℝ), x ∈ Ico a b → f' x ≤ K * f x + ε
H : ∀ (x : ℝ), x ∈ Icc a b → ∀ (ε' : ℝ), ε' ∈ Ioi ε → f x ≤ gronwallBound δ K ε' (x - a)
⊢ ∀ (x : ℝ), x ∈ Icc a b → f x ≤ gronwallBound δ K ε (x - a)
[PROOFSTEP]
intro x hx
[GOAL]
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f f' : ℝ → ℝ
δ K ε a b : ℝ
hf : ContinuousOn f (Icc a b)
hf' : ∀ (x : ℝ), x ∈ Ico a b → ∀ (r : ℝ), f' x < r → ∃ᶠ (z : ℝ) in 𝓝[Ioi x] x, (z - x)⁻¹ * (f z - f x) < r
ha : f a ≤ δ
bound : ∀ (x : ℝ), x ∈ Ico a b → f' x ≤ K * f x + ε
H : ∀ (x : ℝ), x ∈ Icc a b → ∀ (ε' : ℝ), ε' ∈ Ioi ε → f x ≤ gronwallBound δ K ε' (x - a)
x : ℝ
hx : x ∈ Icc a b
⊢ f x ≤ gronwallBound δ K ε (x - a)
[PROOFSTEP]
change f x ≤ (fun ε' => gronwallBound δ K ε' (x - a)) ε
[GOAL]
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f f' : ℝ → ℝ
δ K ε a b : ℝ
hf : ContinuousOn f (Icc a b)
hf' : ∀ (x : ℝ), x ∈ Ico a b → ∀ (r : ℝ), f' x < r → ∃ᶠ (z : ℝ) in 𝓝[Ioi x] x, (z - x)⁻¹ * (f z - f x) < r
ha : f a ≤ δ
bound : ∀ (x : ℝ), x ∈ Ico a b → f' x ≤ K * f x + ε
H : ∀ (x : ℝ), x ∈ Icc a b → ∀ (ε' : ℝ), ε' ∈ Ioi ε → f x ≤ gronwallBound δ K ε' (x - a)
x : ℝ
hx : x ∈ Icc a b
⊢ f x ≤ (fun ε' => gronwallBound δ K ε' (x - a)) ε
[PROOFSTEP]
convert continuousWithinAt_const.closure_le _ _ (H x hx)
[GOAL]
case convert_2
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f f' : ℝ → ℝ
δ K ε a b : ℝ
hf : ContinuousOn f (Icc a b)
hf' : ∀ (x : ℝ), x ∈ Ico a b → ∀ (r : ℝ), f' x < r → ∃ᶠ (z : ℝ) in 𝓝[Ioi x] x, (z - x)⁻¹ * (f z - f x) < r
ha : f a ≤ δ
bound : ∀ (x : ℝ), x ∈ Ico a b → f' x ≤ K * f x + ε
H : ∀ (x : ℝ), x ∈ Icc a b → ∀ (ε' : ℝ), ε' ∈ Ioi ε → f x ≤ gronwallBound δ K ε' (x - a)
x : ℝ
hx : x ∈ Icc a b
⊢ ε ∈ closure (Ioi ε)
[PROOFSTEP]
simp only [closure_Ioi, left_mem_Ici]
[GOAL]
case convert_3
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
f f' : ℝ → ℝ
δ K ε a b : ℝ
hf : ContinuousOn f (Icc a b)
hf' : ∀ (x : ℝ), x ∈ Ico a b → ∀ (r : ℝ), f' x < r → ∃ᶠ (z : ℝ) in 𝓝[Ioi x] x, (z - x)⁻¹ * (f z - f x) < r
ha : f a ≤ δ
bound : ∀ (x : ℝ), x ∈ Ico a b → f' x ≤ K * f x + ε
H : ∀ (x : ℝ), x ∈ Icc a b → ∀ (ε' : ℝ), ε' ∈ Ioi ε → f x ≤ gronwallBound δ K ε' (x - a)
x : ℝ
hx : x ∈ Icc a b
⊢ ContinuousWithinAt (fun y => gronwallBound δ K y (x - a)) (Ioi ε) ε
[PROOFSTEP]
exact (gronwallBound_continuous_ε δ K (x - a)).continuousWithinAt
[GOAL]
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
v : ℝ → E → E
s : ℝ → Set E
K : ℝ
hv : ∀ (t : ℝ) (x : E), x ∈ s t → ∀ (y : E), y ∈ s t → dist (v t x) (v t y) ≤ K * dist x y
f g f' g' : ℝ → E
a b εf εg δ : ℝ
hf : ContinuousOn f (Icc a b)
hf' : ∀ (t : ℝ), t ∈ Ico a b → HasDerivWithinAt f (f' t) (Ici t) t
f_bound : ∀ (t : ℝ), t ∈ Ico a b → dist (f' t) (v t (f t)) ≤ εf
hfs : ∀ (t : ℝ), t ∈ Ico a b → f t ∈ s t
hg : ContinuousOn g (Icc a b)
hg' : ∀ (t : ℝ), t ∈ Ico a b → HasDerivWithinAt g (g' t) (Ici t) t
g_bound : ∀ (t : ℝ), t ∈ Ico a b → dist (g' t) (v t (g t)) ≤ εg
hgs : ∀ (t : ℝ), t ∈ Ico a b → g t ∈ s t
ha : dist (f a) (g a) ≤ δ
⊢ ∀ (t : ℝ), t ∈ Icc a b → dist (f t) (g t) ≤ gronwallBound δ K (εf + εg) (t - a)
[PROOFSTEP]
simp only [dist_eq_norm] at ha ⊢
[GOAL]
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
v : ℝ → E → E
s : ℝ → Set E
K : ℝ
hv : ∀ (t : ℝ) (x : E), x ∈ s t → ∀ (y : E), y ∈ s t → dist (v t x) (v t y) ≤ K * dist x y
f g f' g' : ℝ → E
a b εf εg δ : ℝ
hf : ContinuousOn f (Icc a b)
hf' : ∀ (t : ℝ), t ∈ Ico a b → HasDerivWithinAt f (f' t) (Ici t) t
f_bound : ∀ (t : ℝ), t ∈ Ico a b → dist (f' t) (v t (f t)) ≤ εf
hfs : ∀ (t : ℝ), t ∈ Ico a b → f t ∈ s t
hg : ContinuousOn g (Icc a b)
hg' : ∀ (t : ℝ), t ∈ Ico a b → HasDerivWithinAt g (g' t) (Ici t) t
g_bound : ∀ (t : ℝ), t ∈ Ico a b → dist (g' t) (v t (g t)) ≤ εg
hgs : ∀ (t : ℝ), t ∈ Ico a b → g t ∈ s t
ha : ‖f a - g a‖ ≤ δ
⊢ ∀ (t : ℝ), t ∈ Icc a b → ‖f t - g t‖ ≤ gronwallBound δ K (εf + εg) (t - a)
[PROOFSTEP]
have h_deriv : ∀ t ∈ Ico a b, HasDerivWithinAt (fun t => f t - g t) (f' t - g' t) (Ici t) t := fun t ht =>
  (hf' t ht).sub (hg' t ht)
[GOAL]
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
v : ℝ → E → E
s : ℝ → Set E
K : ℝ
hv : ∀ (t : ℝ) (x : E), x ∈ s t → ∀ (y : E), y ∈ s t → dist (v t x) (v t y) ≤ K * dist x y
f g f' g' : ℝ → E
a b εf εg δ : ℝ
hf : ContinuousOn f (Icc a b)
hf' : ∀ (t : ℝ), t ∈ Ico a b → HasDerivWithinAt f (f' t) (Ici t) t
f_bound : ∀ (t : ℝ), t ∈ Ico a b → dist (f' t) (v t (f t)) ≤ εf
hfs : ∀ (t : ℝ), t ∈ Ico a b → f t ∈ s t
hg : ContinuousOn g (Icc a b)
hg' : ∀ (t : ℝ), t ∈ Ico a b → HasDerivWithinAt g (g' t) (Ici t) t
g_bound : ∀ (t : ℝ), t ∈ Ico a b → dist (g' t) (v t (g t)) ≤ εg
hgs : ∀ (t : ℝ), t ∈ Ico a b → g t ∈ s t
ha : ‖f a - g a‖ ≤ δ
h_deriv : ∀ (t : ℝ), t ∈ Ico a b → HasDerivWithinAt (fun t => f t - g t) (f' t - g' t) (Ici t) t
⊢ ∀ (t : ℝ), t ∈ Icc a b → ‖f t - g t‖ ≤ gronwallBound δ K (εf + εg) (t - a)
[PROOFSTEP]
apply norm_le_gronwallBound_of_norm_deriv_right_le (hf.sub hg) h_deriv ha
[GOAL]
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
v : ℝ → E → E
s : ℝ → Set E
K : ℝ
hv : ∀ (t : ℝ) (x : E), x ∈ s t → ∀ (y : E), y ∈ s t → dist (v t x) (v t y) ≤ K * dist x y
f g f' g' : ℝ → E
a b εf εg δ : ℝ
hf : ContinuousOn f (Icc a b)
hf' : ∀ (t : ℝ), t ∈ Ico a b → HasDerivWithinAt f (f' t) (Ici t) t
f_bound : ∀ (t : ℝ), t ∈ Ico a b → dist (f' t) (v t (f t)) ≤ εf
hfs : ∀ (t : ℝ), t ∈ Ico a b → f t ∈ s t
hg : ContinuousOn g (Icc a b)
hg' : ∀ (t : ℝ), t ∈ Ico a b → HasDerivWithinAt g (g' t) (Ici t) t
g_bound : ∀ (t : ℝ), t ∈ Ico a b → dist (g' t) (v t (g t)) ≤ εg
hgs : ∀ (t : ℝ), t ∈ Ico a b → g t ∈ s t
ha : ‖f a - g a‖ ≤ δ
h_deriv : ∀ (t : ℝ), t ∈ Ico a b → HasDerivWithinAt (fun t => f t - g t) (f' t - g' t) (Ici t) t
⊢ ∀ (x : ℝ), x ∈ Ico a b → ‖f' x - g' x‖ ≤ K * ‖f x - g x‖ + (εf + εg)
[PROOFSTEP]
intro t ht
[GOAL]
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
v : ℝ → E → E
s : ℝ → Set E
K : ℝ
hv : ∀ (t : ℝ) (x : E), x ∈ s t → ∀ (y : E), y ∈ s t → dist (v t x) (v t y) ≤ K * dist x y
f g f' g' : ℝ → E
a b εf εg δ : ℝ
hf : ContinuousOn f (Icc a b)
hf' : ∀ (t : ℝ), t ∈ Ico a b → HasDerivWithinAt f (f' t) (Ici t) t
f_bound : ∀ (t : ℝ), t ∈ Ico a b → dist (f' t) (v t (f t)) ≤ εf
hfs : ∀ (t : ℝ), t ∈ Ico a b → f t ∈ s t
hg : ContinuousOn g (Icc a b)
hg' : ∀ (t : ℝ), t ∈ Ico a b → HasDerivWithinAt g (g' t) (Ici t) t
g_bound : ∀ (t : ℝ), t ∈ Ico a b → dist (g' t) (v t (g t)) ≤ εg
hgs : ∀ (t : ℝ), t ∈ Ico a b → g t ∈ s t
ha : ‖f a - g a‖ ≤ δ
h_deriv : ∀ (t : ℝ), t ∈ Ico a b → HasDerivWithinAt (fun t => f t - g t) (f' t - g' t) (Ici t) t
t : ℝ
ht : t ∈ Ico a b
⊢ ‖f' t - g' t‖ ≤ K * ‖f t - g t‖ + (εf + εg)
[PROOFSTEP]
have := dist_triangle4_right (f' t) (g' t) (v t (f t)) (v t (g t))
[GOAL]
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
v : ℝ → E → E
s : ℝ → Set E
K : ℝ
hv : ∀ (t : ℝ) (x : E), x ∈ s t → ∀ (y : E), y ∈ s t → dist (v t x) (v t y) ≤ K * dist x y
f g f' g' : ℝ → E
a b εf εg δ : ℝ
hf : ContinuousOn f (Icc a b)
hf' : ∀ (t : ℝ), t ∈ Ico a b → HasDerivWithinAt f (f' t) (Ici t) t
f_bound : ∀ (t : ℝ), t ∈ Ico a b → dist (f' t) (v t (f t)) ≤ εf
hfs : ∀ (t : ℝ), t ∈ Ico a b → f t ∈ s t
hg : ContinuousOn g (Icc a b)
hg' : ∀ (t : ℝ), t ∈ Ico a b → HasDerivWithinAt g (g' t) (Ici t) t
g_bound : ∀ (t : ℝ), t ∈ Ico a b → dist (g' t) (v t (g t)) ≤ εg
hgs : ∀ (t : ℝ), t ∈ Ico a b → g t ∈ s t
ha : ‖f a - g a‖ ≤ δ
h_deriv : ∀ (t : ℝ), t ∈ Ico a b → HasDerivWithinAt (fun t => f t - g t) (f' t - g' t) (Ici t) t
t : ℝ
ht : t ∈ Ico a b
this : dist (f' t) (g' t) ≤ dist (f' t) (v t (f t)) + dist (g' t) (v t (g t)) + dist (v t (f t)) (v t (g t))
⊢ ‖f' t - g' t‖ ≤ K * ‖f t - g t‖ + (εf + εg)
[PROOFSTEP]
rw [dist_eq_norm] at this
[GOAL]
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
v : ℝ → E → E
s : ℝ → Set E
K : ℝ
hv : ∀ (t : ℝ) (x : E), x ∈ s t → ∀ (y : E), y ∈ s t → dist (v t x) (v t y) ≤ K * dist x y
f g f' g' : ℝ → E
a b εf εg δ : ℝ
hf : ContinuousOn f (Icc a b)
hf' : ∀ (t : ℝ), t ∈ Ico a b → HasDerivWithinAt f (f' t) (Ici t) t
f_bound : ∀ (t : ℝ), t ∈ Ico a b → dist (f' t) (v t (f t)) ≤ εf
hfs : ∀ (t : ℝ), t ∈ Ico a b → f t ∈ s t
hg : ContinuousOn g (Icc a b)
hg' : ∀ (t : ℝ), t ∈ Ico a b → HasDerivWithinAt g (g' t) (Ici t) t
g_bound : ∀ (t : ℝ), t ∈ Ico a b → dist (g' t) (v t (g t)) ≤ εg
hgs : ∀ (t : ℝ), t ∈ Ico a b → g t ∈ s t
ha : ‖f a - g a‖ ≤ δ
h_deriv : ∀ (t : ℝ), t ∈ Ico a b → HasDerivWithinAt (fun t => f t - g t) (f' t - g' t) (Ici t) t
t : ℝ
ht : t ∈ Ico a b
this : ‖f' t - g' t‖ ≤ dist (f' t) (v t (f t)) + dist (g' t) (v t (g t)) + dist (v t (f t)) (v t (g t))
⊢ ‖f' t - g' t‖ ≤ K * ‖f t - g t‖ + (εf + εg)
[PROOFSTEP]
refine'
  this.trans ((add_le_add (add_le_add (f_bound t ht) (g_bound t ht)) (hv t (f t) (hfs t ht) (g t) (hgs t ht))).trans _)
[GOAL]
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
v : ℝ → E → E
s : ℝ → Set E
K : ℝ
hv : ∀ (t : ℝ) (x : E), x ∈ s t → ∀ (y : E), y ∈ s t → dist (v t x) (v t y) ≤ K * dist x y
f g f' g' : ℝ → E
a b εf εg δ : ℝ
hf : ContinuousOn f (Icc a b)
hf' : ∀ (t : ℝ), t ∈ Ico a b → HasDerivWithinAt f (f' t) (Ici t) t
f_bound : ∀ (t : ℝ), t ∈ Ico a b → dist (f' t) (v t (f t)) ≤ εf
hfs : ∀ (t : ℝ), t ∈ Ico a b → f t ∈ s t
hg : ContinuousOn g (Icc a b)
hg' : ∀ (t : ℝ), t ∈ Ico a b → HasDerivWithinAt g (g' t) (Ici t) t
g_bound : ∀ (t : ℝ), t ∈ Ico a b → dist (g' t) (v t (g t)) ≤ εg
hgs : ∀ (t : ℝ), t ∈ Ico a b → g t ∈ s t
ha : ‖f a - g a‖ ≤ δ
h_deriv : ∀ (t : ℝ), t ∈ Ico a b → HasDerivWithinAt (fun t => f t - g t) (f' t - g' t) (Ici t) t
t : ℝ
ht : t ∈ Ico a b
this : ‖f' t - g' t‖ ≤ dist (f' t) (v t (f t)) + dist (g' t) (v t (g t)) + dist (v t (f t)) (v t (g t))
⊢ εf + εg + K * dist (f t) (g t) ≤ K * ‖f t - g t‖ + (εf + εg)
[PROOFSTEP]
rw [dist_eq_norm, add_comm]
[GOAL]
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
v : ℝ → E → E
s : ℝ → Set E
K : ℝ
hv : ∀ (t : ℝ) (x : E), x ∈ s t → ∀ (y : E), y ∈ s t → dist (v t x) (v t y) ≤ K * dist x y
f g : ℝ → E
a b δ : ℝ
hf : ContinuousOn f (Icc a b)
hf' : ∀ (t : ℝ), t ∈ Ico a b → HasDerivWithinAt f (v t (f t)) (Ici t) t
hfs : ∀ (t : ℝ), t ∈ Ico a b → f t ∈ s t
hg : ContinuousOn g (Icc a b)
hg' : ∀ (t : ℝ), t ∈ Ico a b → HasDerivWithinAt g (v t (g t)) (Ici t) t
hgs : ∀ (t : ℝ), t ∈ Ico a b → g t ∈ s t
ha : dist (f a) (g a) ≤ δ
⊢ ∀ (t : ℝ), t ∈ Icc a b → dist (f t) (g t) ≤ δ * exp (K * (t - a))
[PROOFSTEP]
have f_bound : ∀ t ∈ Ico a b, dist (v t (f t)) (v t (f t)) ≤ 0 := by intros; rw [dist_self]
[GOAL]
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
v : ℝ → E → E
s : ℝ → Set E
K : ℝ
hv : ∀ (t : ℝ) (x : E), x ∈ s t → ∀ (y : E), y ∈ s t → dist (v t x) (v t y) ≤ K * dist x y
f g : ℝ → E
a b δ : ℝ
hf : ContinuousOn f (Icc a b)
hf' : ∀ (t : ℝ), t ∈ Ico a b → HasDerivWithinAt f (v t (f t)) (Ici t) t
hfs : ∀ (t : ℝ), t ∈ Ico a b → f t ∈ s t
hg : ContinuousOn g (Icc a b)
hg' : ∀ (t : ℝ), t ∈ Ico a b → HasDerivWithinAt g (v t (g t)) (Ici t) t
hgs : ∀ (t : ℝ), t ∈ Ico a b → g t ∈ s t
ha : dist (f a) (g a) ≤ δ
⊢ ∀ (t : ℝ), t ∈ Ico a b → dist (v t (f t)) (v t (f t)) ≤ 0
[PROOFSTEP]
intros
[GOAL]
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
v : ℝ → E → E
s : ℝ → Set E
K : ℝ
hv : ∀ (t : ℝ) (x : E), x ∈ s t → ∀ (y : E), y ∈ s t → dist (v t x) (v t y) ≤ K * dist x y
f g : ℝ → E
a b δ : ℝ
hf : ContinuousOn f (Icc a b)
hf' : ∀ (t : ℝ), t ∈ Ico a b → HasDerivWithinAt f (v t (f t)) (Ici t) t
hfs : ∀ (t : ℝ), t ∈ Ico a b → f t ∈ s t
hg : ContinuousOn g (Icc a b)
hg' : ∀ (t : ℝ), t ∈ Ico a b → HasDerivWithinAt g (v t (g t)) (Ici t) t
hgs : ∀ (t : ℝ), t ∈ Ico a b → g t ∈ s t
ha : dist (f a) (g a) ≤ δ
t✝ : ℝ
a✝ : t✝ ∈ Ico a b
⊢ dist (v t✝ (f t✝)) (v t✝ (f t✝)) ≤ 0
[PROOFSTEP]
rw [dist_self]
[GOAL]
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
v : ℝ → E → E
s : ℝ → Set E
K : ℝ
hv : ∀ (t : ℝ) (x : E), x ∈ s t → ∀ (y : E), y ∈ s t → dist (v t x) (v t y) ≤ K * dist x y
f g : ℝ → E
a b δ : ℝ
hf : ContinuousOn f (Icc a b)
hf' : ∀ (t : ℝ), t ∈ Ico a b → HasDerivWithinAt f (v t (f t)) (Ici t) t
hfs : ∀ (t : ℝ), t ∈ Ico a b → f t ∈ s t
hg : ContinuousOn g (Icc a b)
hg' : ∀ (t : ℝ), t ∈ Ico a b → HasDerivWithinAt g (v t (g t)) (Ici t) t
hgs : ∀ (t : ℝ), t ∈ Ico a b → g t ∈ s t
ha : dist (f a) (g a) ≤ δ
f_bound : ∀ (t : ℝ), t ∈ Ico a b → dist (v t (f t)) (v t (f t)) ≤ 0
⊢ ∀ (t : ℝ), t ∈ Icc a b → dist (f t) (g t) ≤ δ * exp (K * (t - a))
[PROOFSTEP]
have g_bound : ∀ t ∈ Ico a b, dist (v t (g t)) (v t (g t)) ≤ 0 := by intros; rw [dist_self]
[GOAL]
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
v : ℝ → E → E
s : ℝ → Set E
K : ℝ
hv : ∀ (t : ℝ) (x : E), x ∈ s t → ∀ (y : E), y ∈ s t → dist (v t x) (v t y) ≤ K * dist x y
f g : ℝ → E
a b δ : ℝ
hf : ContinuousOn f (Icc a b)
hf' : ∀ (t : ℝ), t ∈ Ico a b → HasDerivWithinAt f (v t (f t)) (Ici t) t
hfs : ∀ (t : ℝ), t ∈ Ico a b → f t ∈ s t
hg : ContinuousOn g (Icc a b)
hg' : ∀ (t : ℝ), t ∈ Ico a b → HasDerivWithinAt g (v t (g t)) (Ici t) t
hgs : ∀ (t : ℝ), t ∈ Ico a b → g t ∈ s t
ha : dist (f a) (g a) ≤ δ
f_bound : ∀ (t : ℝ), t ∈ Ico a b → dist (v t (f t)) (v t (f t)) ≤ 0
⊢ ∀ (t : ℝ), t ∈ Ico a b → dist (v t (g t)) (v t (g t)) ≤ 0
[PROOFSTEP]
intros
[GOAL]
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
v : ℝ → E → E
s : ℝ → Set E
K : ℝ
hv : ∀ (t : ℝ) (x : E), x ∈ s t → ∀ (y : E), y ∈ s t → dist (v t x) (v t y) ≤ K * dist x y
f g : ℝ → E
a b δ : ℝ
hf : ContinuousOn f (Icc a b)
hf' : ∀ (t : ℝ), t ∈ Ico a b → HasDerivWithinAt f (v t (f t)) (Ici t) t
hfs : ∀ (t : ℝ), t ∈ Ico a b → f t ∈ s t
hg : ContinuousOn g (Icc a b)
hg' : ∀ (t : ℝ), t ∈ Ico a b → HasDerivWithinAt g (v t (g t)) (Ici t) t
hgs : ∀ (t : ℝ), t ∈ Ico a b → g t ∈ s t
ha : dist (f a) (g a) ≤ δ
f_bound : ∀ (t : ℝ), t ∈ Ico a b → dist (v t (f t)) (v t (f t)) ≤ 0
t✝ : ℝ
a✝ : t✝ ∈ Ico a b
⊢ dist (v t✝ (g t✝)) (v t✝ (g t✝)) ≤ 0
[PROOFSTEP]
rw [dist_self]
[GOAL]
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
v : ℝ → E → E
s : ℝ → Set E
K : ℝ
hv : ∀ (t : ℝ) (x : E), x ∈ s t → ∀ (y : E), y ∈ s t → dist (v t x) (v t y) ≤ K * dist x y
f g : ℝ → E
a b δ : ℝ
hf : ContinuousOn f (Icc a b)
hf' : ∀ (t : ℝ), t ∈ Ico a b → HasDerivWithinAt f (v t (f t)) (Ici t) t
hfs : ∀ (t : ℝ), t ∈ Ico a b → f t ∈ s t
hg : ContinuousOn g (Icc a b)
hg' : ∀ (t : ℝ), t ∈ Ico a b → HasDerivWithinAt g (v t (g t)) (Ici t) t
hgs : ∀ (t : ℝ), t ∈ Ico a b → g t ∈ s t
ha : dist (f a) (g a) ≤ δ
f_bound : ∀ (t : ℝ), t ∈ Ico a b → dist (v t (f t)) (v t (f t)) ≤ 0
g_bound : ∀ (t : ℝ), t ∈ Ico a b → dist (v t (g t)) (v t (g t)) ≤ 0
⊢ ∀ (t : ℝ), t ∈ Icc a b → dist (f t) (g t) ≤ δ * exp (K * (t - a))
[PROOFSTEP]
intro t ht
[GOAL]
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
v : ℝ → E → E
s : ℝ → Set E
K : ℝ
hv : ∀ (t : ℝ) (x : E), x ∈ s t → ∀ (y : E), y ∈ s t → dist (v t x) (v t y) ≤ K * dist x y
f g : ℝ → E
a b δ : ℝ
hf : ContinuousOn f (Icc a b)
hf' : ∀ (t : ℝ), t ∈ Ico a b → HasDerivWithinAt f (v t (f t)) (Ici t) t
hfs : ∀ (t : ℝ), t ∈ Ico a b → f t ∈ s t
hg : ContinuousOn g (Icc a b)
hg' : ∀ (t : ℝ), t ∈ Ico a b → HasDerivWithinAt g (v t (g t)) (Ici t) t
hgs : ∀ (t : ℝ), t ∈ Ico a b → g t ∈ s t
ha : dist (f a) (g a) ≤ δ
f_bound : ∀ (t : ℝ), t ∈ Ico a b → dist (v t (f t)) (v t (f t)) ≤ 0
g_bound : ∀ (t : ℝ), t ∈ Ico a b → dist (v t (g t)) (v t (g t)) ≤ 0
t : ℝ
ht : t ∈ Icc a b
⊢ dist (f t) (g t) ≤ δ * exp (K * (t - a))
[PROOFSTEP]
have := dist_le_of_approx_trajectories_ODE_of_mem_set hv hf hf' f_bound hfs hg hg' g_bound hgs ha t ht
[GOAL]
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
v : ℝ → E → E
s : ℝ → Set E
K : ℝ
hv : ∀ (t : ℝ) (x : E), x ∈ s t → ∀ (y : E), y ∈ s t → dist (v t x) (v t y) ≤ K * dist x y
f g : ℝ → E
a b δ : ℝ
hf : ContinuousOn f (Icc a b)
hf' : ∀ (t : ℝ), t ∈ Ico a b → HasDerivWithinAt f (v t (f t)) (Ici t) t
hfs : ∀ (t : ℝ), t ∈ Ico a b → f t ∈ s t
hg : ContinuousOn g (Icc a b)
hg' : ∀ (t : ℝ), t ∈ Ico a b → HasDerivWithinAt g (v t (g t)) (Ici t) t
hgs : ∀ (t : ℝ), t ∈ Ico a b → g t ∈ s t
ha : dist (f a) (g a) ≤ δ
f_bound : ∀ (t : ℝ), t ∈ Ico a b → dist (v t (f t)) (v t (f t)) ≤ 0
g_bound : ∀ (t : ℝ), t ∈ Ico a b → dist (v t (g t)) (v t (g t)) ≤ 0
t : ℝ
ht : t ∈ Icc a b
this : dist (f t) (g t) ≤ gronwallBound δ K (0 + 0) (t - a)
⊢ dist (f t) (g t) ≤ δ * exp (K * (t - a))
[PROOFSTEP]
rwa [zero_add, gronwallBound_ε0] at this
[GOAL]
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
v : ℝ → E → E
s : ℝ → Set E
K : ℝ
hv : ∀ (t : ℝ) (x : E), x ∈ s t → ∀ (y : E), y ∈ s t → dist (v t x) (v t y) ≤ K * dist x y
f g : ℝ → E
a b : ℝ
hf : ContinuousOn f (Icc a b)
hf' : ∀ (t : ℝ), t ∈ Ico a b → HasDerivWithinAt f (v t (f t)) (Ici t) t
hfs : ∀ (t : ℝ), t ∈ Ico a b → f t ∈ s t
hg : ContinuousOn g (Icc a b)
hg' : ∀ (t : ℝ), t ∈ Ico a b → HasDerivWithinAt g (v t (g t)) (Ici t) t
hgs : ∀ (t : ℝ), t ∈ Ico a b → g t ∈ s t
ha : f a = g a
t : ℝ
ht : t ∈ Icc a b
⊢ f t = g t
[PROOFSTEP]
have := dist_le_of_trajectories_ODE_of_mem_set hv hf hf' hfs hg hg' hgs (dist_le_zero.2 ha) t ht
[GOAL]
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
v : ℝ → E → E
s : ℝ → Set E
K : ℝ
hv : ∀ (t : ℝ) (x : E), x ∈ s t → ∀ (y : E), y ∈ s t → dist (v t x) (v t y) ≤ K * dist x y
f g : ℝ → E
a b : ℝ
hf : ContinuousOn f (Icc a b)
hf' : ∀ (t : ℝ), t ∈ Ico a b → HasDerivWithinAt f (v t (f t)) (Ici t) t
hfs : ∀ (t : ℝ), t ∈ Ico a b → f t ∈ s t
hg : ContinuousOn g (Icc a b)
hg' : ∀ (t : ℝ), t ∈ Ico a b → HasDerivWithinAt g (v t (g t)) (Ici t) t
hgs : ∀ (t : ℝ), t ∈ Ico a b → g t ∈ s t
ha : f a = g a
t : ℝ
ht : t ∈ Icc a b
this : dist (f t) (g t) ≤ 0 * exp (K * (t - a))
⊢ f t = g t
[PROOFSTEP]
rwa [zero_mul, dist_le_zero] at this


[GOAL]
x y : ℂ
⊢ SameRay ℝ x y ↔ x = 0 ∨ y = 0 ∨ arg x = arg y
[PROOFSTEP]
rcases eq_or_ne x 0 with (rfl | hx)
[GOAL]
case inl
y : ℂ
⊢ SameRay ℝ 0 y ↔ 0 = 0 ∨ y = 0 ∨ arg 0 = arg y
[PROOFSTEP]
simp
[GOAL]
case inr
x y : ℂ
hx : x ≠ 0
⊢ SameRay ℝ x y ↔ x = 0 ∨ y = 0 ∨ arg x = arg y
[PROOFSTEP]
rcases eq_or_ne y 0 with (rfl | hy)
[GOAL]
case inr.inl
x : ℂ
hx : x ≠ 0
⊢ SameRay ℝ x 0 ↔ x = 0 ∨ 0 = 0 ∨ arg x = arg 0
[PROOFSTEP]
simp
[GOAL]
case inr.inr
x y : ℂ
hx : x ≠ 0
hy : y ≠ 0
⊢ SameRay ℝ x y ↔ x = 0 ∨ y = 0 ∨ arg x = arg y
[PROOFSTEP]
simp only [hx, hy, false_or_iff, sameRay_iff_norm_smul_eq, arg_eq_arg_iff hx hy]
[GOAL]
case inr.inr
x y : ℂ
hx : x ≠ 0
hy : y ≠ 0
⊢ ‖x‖ • y = ‖y‖ • x ↔ ↑(↑abs y) / ↑(↑abs x) * x = y
[PROOFSTEP]
field_simp [hx, hy]
[GOAL]
case inr.inr
x y : ℂ
hx : x ≠ 0
hy : y ≠ 0
⊢ ↑(↑abs x) * y = ↑(↑abs y) * x ↔ ↑(↑abs y) * x = y * ↑(↑abs x)
[PROOFSTEP]
rw [mul_comm, eq_comm]
[GOAL]
x y : ℂ
⊢ SameRay ℝ x y ↔ arg (x / y) = 0
[PROOFSTEP]
rw [← Real.Angle.toReal_zero, ← arg_coe_angle_eq_iff_eq_toReal, sameRay_iff]
[GOAL]
x y : ℂ
⊢ x = 0 ∨ y = 0 ∨ arg x = arg y ↔ ↑(arg (x / y)) = 0
[PROOFSTEP]
by_cases hx : x = 0
[GOAL]
case pos
x y : ℂ
hx : x = 0
⊢ x = 0 ∨ y = 0 ∨ arg x = arg y ↔ ↑(arg (x / y)) = 0
[PROOFSTEP]
simp [hx]
[GOAL]
case neg
x y : ℂ
hx : ¬x = 0
⊢ x = 0 ∨ y = 0 ∨ arg x = arg y ↔ ↑(arg (x / y)) = 0
[PROOFSTEP]
by_cases hy : y = 0
[GOAL]
case pos
x y : ℂ
hx : ¬x = 0
hy : y = 0
⊢ x = 0 ∨ y = 0 ∨ arg x = arg y ↔ ↑(arg (x / y)) = 0
[PROOFSTEP]
simp [hy]
[GOAL]
case neg
x y : ℂ
hx : ¬x = 0
hy : ¬y = 0
⊢ x = 0 ∨ y = 0 ∨ arg x = arg y ↔ ↑(arg (x / y)) = 0
[PROOFSTEP]
simp [hx, hy, arg_div_coe_angle, sub_eq_zero]


[GOAL]
M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
x : M ⧸ S
⊢ ‖x‖ = infDist 0 {m | ↑m = x}
[PROOFSTEP]
simp only [AddSubgroup.quotient_norm_eq, infDist_eq_iInf, sInf_image', dist_zero_left]
[GOAL]
M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
x : M
⊢ ‖↑x‖ = infDist x ↑S
[PROOFSTEP]
rw [norm_eq_infDist, ← infDist_image (IsometryEquiv.subLeft x).isometry, IsometryEquiv.subLeft_apply, sub_zero, ←
  IsometryEquiv.preimage_symm]
[GOAL]
M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
x : M
⊢ infDist x (↑(IsometryEquiv.symm (IsometryEquiv.subLeft x)) ⁻¹' {m | ↑m = ↑x}) = infDist x ↑S
[PROOFSTEP]
congr 1 with y
[GOAL]
case e_s.h
M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
x y : M
⊢ y ∈ ↑(IsometryEquiv.symm (IsometryEquiv.subLeft x)) ⁻¹' {m | ↑m = ↑x} ↔ y ∈ ↑S
[PROOFSTEP]
simp only [mem_preimage, IsometryEquiv.subLeft_symm_apply, mem_setOf_eq, QuotientAddGroup.eq, neg_add, neg_neg,
  neg_add_cancel_right, SetLike.mem_coe]
[GOAL]
M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
x : M ⧸ S
⊢ ‖-x‖ = ‖x‖
[PROOFSTEP]
simp only [AddSubgroup.quotient_norm_eq]
[GOAL]
M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
x : M ⧸ S
⊢ sInf (norm '' {m | ↑m = -x}) = sInf (norm '' {m | ↑m = x})
[PROOFSTEP]
congr 1 with r
[GOAL]
case e_a.h
M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
x : M ⧸ S
r : ℝ
⊢ r ∈ norm '' {m | ↑m = -x} ↔ r ∈ norm '' {m | ↑m = x}
[PROOFSTEP]
constructor
[GOAL]
case e_a.h.mp
M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
x : M ⧸ S
r : ℝ
⊢ r ∈ norm '' {m | ↑m = -x} → r ∈ norm '' {m | ↑m = x}
[PROOFSTEP]
{rintro ⟨m, hm, rfl⟩; use-m; simpa [neg_eq_iff_eq_neg] using hm
}
[GOAL]
case e_a.h.mp
M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
x : M ⧸ S
r : ℝ
⊢ r ∈ norm '' {m | ↑m = -x} → r ∈ norm '' {m | ↑m = x}
[PROOFSTEP]
rintro ⟨m, hm, rfl⟩
[GOAL]
case e_a.h.mp.intro.intro
M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
x : M ⧸ S
m : M
hm : m ∈ {m | ↑m = -x}
⊢ ‖m‖ ∈ norm '' {m | ↑m = x}
[PROOFSTEP]
use-m
[GOAL]
case h
M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
x : M ⧸ S
m : M
hm : m ∈ {m | ↑m = -x}
⊢ -m ∈ {m | ↑m = x} ∧ ‖-m‖ = ‖m‖
[PROOFSTEP]
simpa [neg_eq_iff_eq_neg] using hm
[GOAL]
case e_a.h.mpr
M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
x : M ⧸ S
r : ℝ
⊢ r ∈ norm '' {m | ↑m = x} → r ∈ norm '' {m | ↑m = -x}
[PROOFSTEP]
{rintro ⟨m, hm, rfl⟩; use-m; simpa [neg_eq_iff_eq_neg] using hm
}
[GOAL]
case e_a.h.mpr
M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
x : M ⧸ S
r : ℝ
⊢ r ∈ norm '' {m | ↑m = x} → r ∈ norm '' {m | ↑m = -x}
[PROOFSTEP]
rintro ⟨m, hm, rfl⟩
[GOAL]
case e_a.h.mpr.intro.intro
M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
x : M ⧸ S
m : M
hm : m ∈ {m | ↑m = x}
⊢ ‖m‖ ∈ norm '' {m | ↑m = -x}
[PROOFSTEP]
use-m
[GOAL]
case h
M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
x : M ⧸ S
m : M
hm : m ∈ {m | ↑m = x}
⊢ -m ∈ {m | ↑m = -x} ∧ ‖-m‖ = ‖m‖
[PROOFSTEP]
simpa [neg_eq_iff_eq_neg] using hm
[GOAL]
M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
x y : M ⧸ S
⊢ ‖x - y‖ = ‖y - x‖
[PROOFSTEP]
rw [← neg_sub, quotient_norm_neg]
[GOAL]
M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
m : M
⊢ ‖↑(mk' S) m‖ = sInf ((fun x => ‖m + x‖) '' ↑S)
[PROOFSTEP]
rw [mk'_apply, norm_mk, sInf_image', ← infDist_image isometry_neg, image_neg, neg_coe_set (H := S), infDist_eq_iInf]
[GOAL]
M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
m : M
⊢ ⨅ (y : ↑↑S), dist (-m) ↑y = ⨅ (a : ↑↑S), ‖m + ↑a‖
[PROOFSTEP]
simp only [dist_eq_norm', sub_neg_eq_add, add_comm]
[GOAL]
M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
m : M
⊢ ‖↑(mk' S) m‖ = 0 ↔ m ∈ closure ↑S
[PROOFSTEP]
rw [mk'_apply, norm_mk, ← mem_closure_iff_infDist_zero]
[GOAL]
M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
m : M
⊢ Set.Nonempty ↑S
[PROOFSTEP]
exact ⟨0, S.zero_mem⟩
[GOAL]
M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
x : M ⧸ S
r : ℝ
⊢ ‖x‖ < r ↔ ∃ m, ↑m = x ∧ ‖m‖ < r
[PROOFSTEP]
rw [isGLB_lt_iff (isGLB_quotient_norm _), bex_image_iff]
[GOAL]
M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
x : M ⧸ S
r : ℝ
⊢ (∃ x_1, x_1 ∈ {m | ↑(mk' S) m = x} ∧ ‖x_1‖ < r) ↔ ∃ m, ↑m = x ∧ ‖m‖ < r
[PROOFSTEP]
rfl
[GOAL]
M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
m : M
ε : ℝ
hε : 0 < ε
⊢ ∃ s, s ∈ S ∧ ‖m + s‖ < ‖↑(mk' S) m‖ + ε
[PROOFSTEP]
obtain ⟨n : M, hn : mk' S n = mk' S m, hn' : ‖n‖ < ‖mk' S m‖ + ε⟩ := norm_mk_lt (QuotientAddGroup.mk' S m) hε
[GOAL]
case intro.intro
M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
m : M
ε : ℝ
hε : 0 < ε
n : M
hn : ↑(mk' S) n = ↑(mk' S) m
hn' : ‖n‖ < ‖↑(mk' S) m‖ + ε
⊢ ∃ s, s ∈ S ∧ ‖m + s‖ < ‖↑(mk' S) m‖ + ε
[PROOFSTEP]
erw [eq_comm, QuotientAddGroup.eq] at hn
[GOAL]
case intro.intro
M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
m : M
ε : ℝ
hε : 0 < ε
n : M
hn : -m + n ∈ S
hn' : ‖n‖ < ‖↑(mk' S) m‖ + ε
⊢ ∃ s, s ∈ S ∧ ‖m + s‖ < ‖↑(mk' S) m‖ + ε
[PROOFSTEP]
use-m + n, hn
[GOAL]
case right
M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
m : M
ε : ℝ
hε : 0 < ε
n : M
hn : -m + n ∈ S
hn' : ‖n‖ < ‖↑(mk' S) m‖ + ε
⊢ ‖m + (-m + n)‖ < ‖↑(mk' S) m‖ + ε
[PROOFSTEP]
rwa [add_neg_cancel_left]
[GOAL]
M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
x y : M ⧸ S
⊢ ‖x + y‖ ≤ ‖x‖ + ‖y‖
[PROOFSTEP]
rcases And.intro (mk_surjective x) (mk_surjective y) with ⟨⟨x, rfl⟩, ⟨y, rfl⟩⟩
[GOAL]
case intro.intro.intro
M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
x y : M
⊢ ‖↑x + ↑y‖ ≤ ‖↑x‖ + ‖↑y‖
[PROOFSTEP]
simp only [← mk'_apply, ← map_add, quotient_norm_mk_eq, sInf_image']
[GOAL]
case intro.intro.intro
M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
x y : M
⊢ ⨅ (a : ↑↑S), ‖x + y + ↑a‖ ≤ (⨅ (a : ↑↑S), ‖x + ↑a‖) + ⨅ (a : ↑↑S), ‖y + ↑a‖
[PROOFSTEP]
refine le_ciInf_add_ciInf fun a b ↦ ?_
[GOAL]
case intro.intro.intro
M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
x y : M
a b : ↑↑S
⊢ ⨅ (a : ↑↑S), ‖x + y + ↑a‖ ≤ ‖x + ↑a‖ + ‖y + ↑b‖
[PROOFSTEP]
refine ciInf_le_of_le ⟨0, forall_range_iff.2 fun _ ↦ norm_nonneg _⟩ (a + b) ?_
[GOAL]
case intro.intro.intro
M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
x y : M
a b : ↑↑S
⊢ ‖x + y + ↑(a + b)‖ ≤ ‖x + ↑a‖ + ‖y + ↑b‖
[PROOFSTEP]
exact (congr_arg norm (add_add_add_comm _ _ _ _)).trans_le (norm_add_le _ _)
[GOAL]
M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
⊢ ‖0‖ = 0
[PROOFSTEP]
erw [quotient_norm_eq_zero_iff]
[GOAL]
M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
⊢ 0 ∈ closure ↑S
[PROOFSTEP]
exact subset_closure S.zero_mem
[GOAL]
M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
hS : IsClosed ↑S
m : M
h : ‖↑(mk' S) m‖ = 0
⊢ m ∈ S
[PROOFSTEP]
rwa [quotient_norm_eq_zero_iff, hS.closure_eq] at h
[GOAL]
M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
⊢ Filter.HasBasis (𝓝 0) (fun ε => 0 < ε) fun ε => {x | ‖x‖ < ε}
[PROOFSTEP]
have : ∀ ε : ℝ, mk '' ball (0 : M) ε = {x : M ⧸ S | ‖x‖ < ε}
[GOAL]
case this
M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
⊢ ∀ (ε : ℝ), mk '' ball 0 ε = {x | ‖x‖ < ε}
[PROOFSTEP]
refine fun ε ↦ Set.ext <| forall_mk.2 fun x ↦ ?_
[GOAL]
case this
M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
ε : ℝ
x : M
⊢ ↑x ∈ mk '' ball 0 ε ↔ ↑x ∈ {x | ‖x‖ < ε}
[PROOFSTEP]
rw [ball_zero_eq, mem_setOf_eq, norm_lt_iff, mem_image]
[GOAL]
case this
M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
ε : ℝ
x : M
⊢ (∃ x_1, x_1 ∈ {x | ‖x‖ < ε} ∧ ↑x_1 = ↑x) ↔ ∃ m, ↑m = ↑x ∧ ‖m‖ < ε
[PROOFSTEP]
exact exists_congr fun _ ↦ and_comm
[GOAL]
M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
this : ∀ (ε : ℝ), mk '' ball 0 ε = {x | ‖x‖ < ε}
⊢ Filter.HasBasis (𝓝 0) (fun ε => 0 < ε) fun ε => {x | ‖x‖ < ε}
[PROOFSTEP]
rw [← mk_zero, nhds_eq, ← funext this]
[GOAL]
M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
this : ∀ (ε : ℝ), mk '' ball 0 ε = {x | ‖x‖ < ε}
⊢ Filter.HasBasis (Filter.map mk (𝓝 0)) (fun ε => 0 < ε) fun x => mk '' ball 0 x
[PROOFSTEP]
exact .map _ Metric.nhds_basis_ball
[GOAL]
M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
x : M ⧸ S
⊢ dist x x = 0
[PROOFSTEP]
simp only [norm_mk_zero, sub_self]
[GOAL]
M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
x y z : M ⧸ S
⊢ dist x z ≤ dist x y + dist y z
[PROOFSTEP]
refine le_trans ?_ (quotient_norm_add_le _ _ _)
[GOAL]
M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
x y z : M ⧸ S
⊢ dist x z ≤ ‖x - y + (y - z)‖
[PROOFSTEP]
exact (congr_arg norm (sub_add_sub_cancel _ _ _).symm).le
[GOAL]
M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
x y : M ⧸ S
⊢ (fun x y => ↑{ val := ‖x - y‖, property := (_ : 0 ≤ ‖x - y‖) }) x y = ENNReal.ofReal (dist x y)
[PROOFSTEP]
exact ENNReal.coe_nnreal_eq _
[GOAL]
M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
⊢ uniformity (M ⧸ S) = ⨅ (ε : ℝ) (_ : ε > 0), Filter.principal {p | dist p.fst p.snd < ε}
[PROOFSTEP]
rw [uniformity_eq_comap_nhds_zero', ((quotient_nhd_basis S).comap _).eq_biInf]
[GOAL]
M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
⊢ ⨅ (i : ℝ) (_ : 0 < i), Filter.principal ((fun p => p.snd - p.fst) ⁻¹' {x | ‖x‖ < i}) =
    ⨅ (ε : ℝ) (_ : ε > 0), Filter.principal {p | dist p.fst p.snd < ε}
[PROOFSTEP]
simp only [dist, quotient_norm_sub_rev (Prod.fst _), preimage_setOf_eq]
[GOAL]
M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
src✝ : M →+ M ⧸ S := mk' S
m : M
⊢ ‖ZeroHom.toFun (↑src✝) m‖ ≤ 1 * ‖m‖
[PROOFSTEP]
simpa [one_mul] using quotient_norm_mk_le _ m
[GOAL]
M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
m : M
⊢ ‖↑(normedMk S) m‖ ≤ 1 * ‖m‖
[PROOFSTEP]
simp [quotient_norm_mk_le']
[GOAL]
M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
f : NormedAddGroupHom M N
hf : ∀ (x : M), x ∈ S → ↑f x = 0
x : M ⧸ S
⊢ ‖↑(lift S (toAddMonoidHom f) hf) x‖ ≤ ‖f‖ * ‖x‖
[PROOFSTEP]
cases (norm_nonneg f).eq_or_gt with
| inl h =>
  rcases mk_surjective x with ⟨x, rfl⟩
  simpa [h] using le_opNorm f x
| inr h =>
  rw [← not_lt, ← _root_.lt_div_iff' h, norm_lt_iff]
  rintro ⟨x, rfl, hx⟩
  exact ((lt_div_iff' h).1 hx).not_le (le_opNorm f x)
[GOAL]
M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
f : NormedAddGroupHom M N
hf : ∀ (x : M), x ∈ S → ↑f x = 0
x : M ⧸ S
x✝ : ‖f‖ = 0 ∨ 0 < ‖f‖
⊢ ‖↑(lift S (toAddMonoidHom f) hf) x‖ ≤ ‖f‖ * ‖x‖
[PROOFSTEP]
cases (norm_nonneg f).eq_or_gt with
| inl h =>
  rcases mk_surjective x with ⟨x, rfl⟩
  simpa [h] using le_opNorm f x
| inr h =>
  rw [← not_lt, ← _root_.lt_div_iff' h, norm_lt_iff]
  rintro ⟨x, rfl, hx⟩
  exact ((lt_div_iff' h).1 hx).not_le (le_opNorm f x)
[GOAL]
case inl
M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
f : NormedAddGroupHom M N
hf : ∀ (x : M), x ∈ S → ↑f x = 0
x : M ⧸ S
h : ‖f‖ = 0
⊢ ‖↑(lift S (toAddMonoidHom f) hf) x‖ ≤ ‖f‖ * ‖x‖
[PROOFSTEP]

| inl h =>
  rcases mk_surjective x with ⟨x, rfl⟩
  simpa [h] using le_opNorm f x
[GOAL]
case inl
M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
f : NormedAddGroupHom M N
hf : ∀ (x : M), x ∈ S → ↑f x = 0
x : M ⧸ S
h : ‖f‖ = 0
⊢ ‖↑(lift S (toAddMonoidHom f) hf) x‖ ≤ ‖f‖ * ‖x‖
[PROOFSTEP]
rcases mk_surjective x with ⟨x, rfl⟩
[GOAL]
case inl.intro
M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
f : NormedAddGroupHom M N
hf : ∀ (x : M), x ∈ S → ↑f x = 0
h : ‖f‖ = 0
x : M
⊢ ‖↑(lift S (toAddMonoidHom f) hf) ↑x‖ ≤ ‖f‖ * ‖↑x‖
[PROOFSTEP]
simpa [h] using le_opNorm f x
[GOAL]
case inr
M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
f : NormedAddGroupHom M N
hf : ∀ (x : M), x ∈ S → ↑f x = 0
x : M ⧸ S
h : 0 < ‖f‖
⊢ ‖↑(lift S (toAddMonoidHom f) hf) x‖ ≤ ‖f‖ * ‖x‖
[PROOFSTEP]

| inr h =>
  rw [← not_lt, ← _root_.lt_div_iff' h, norm_lt_iff]
  rintro ⟨x, rfl, hx⟩
  exact ((lt_div_iff' h).1 hx).not_le (le_opNorm f x)
[GOAL]
case inr
M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
f : NormedAddGroupHom M N
hf : ∀ (x : M), x ∈ S → ↑f x = 0
x : M ⧸ S
h : 0 < ‖f‖
⊢ ‖↑(lift S (toAddMonoidHom f) hf) x‖ ≤ ‖f‖ * ‖x‖
[PROOFSTEP]
rw [← not_lt, ← _root_.lt_div_iff' h, norm_lt_iff]
[GOAL]
case inr
M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
f : NormedAddGroupHom M N
hf : ∀ (x : M), x ∈ S → ↑f x = 0
x : M ⧸ S
h : 0 < ‖f‖
⊢ ¬∃ m, ↑m = x ∧ ‖m‖ < ‖↑(lift S (toAddMonoidHom f) hf) x‖ / ‖f‖
[PROOFSTEP]
rintro ⟨x, rfl, hx⟩
[GOAL]
case inr.intro.intro
M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
f : NormedAddGroupHom M N
hf : ∀ (x : M), x ∈ S → ↑f x = 0
h : 0 < ‖f‖
x : M
hx : ‖x‖ < ‖↑(lift S (toAddMonoidHom f) hf) ↑x‖ / ‖f‖
⊢ False
[PROOFSTEP]
exact ((lt_div_iff' h).1 hx).not_le (le_opNorm f x)
[GOAL]
M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
h : ↑(topologicalClosure S) ≠ univ
⊢ ‖normedMk S‖ = 1
[PROOFSTEP]
refine le_antisymm (norm_normedMk_le S) ?_
[GOAL]
M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
h : ↑(topologicalClosure S) ≠ univ
⊢ 1 ≤ ‖normedMk S‖
[PROOFSTEP]
obtain ⟨x, hx⟩ : ∃ x : M, 0 < ‖(x : M ⧸ S)‖
[GOAL]
M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
h : ↑(topologicalClosure S) ≠ univ
⊢ ∃ x, 0 < ‖↑x‖
[PROOFSTEP]
refine (Set.nonempty_compl.2 h).imp fun x hx ↦ ?_
[GOAL]
M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
h : ↑(topologicalClosure S) ≠ univ
x : M
hx : x ∈ (↑(topologicalClosure S))ᶜ
⊢ 0 < ‖↑x‖
[PROOFSTEP]
exact (norm_nonneg _).lt_of_ne' <| mt (quotient_norm_eq_zero_iff S x).1 hx
[GOAL]
case intro
M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
h : ↑(topologicalClosure S) ≠ univ
x : M
hx : 0 < ‖↑x‖
⊢ 1 ≤ ‖normedMk S‖
[PROOFSTEP]
refine (le_mul_iff_one_le_left hx).1 ?_
[GOAL]
case intro
M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
h : ↑(topologicalClosure S) ≠ univ
x : M
hx : 0 < ‖↑x‖
⊢ ‖↑x‖ ≤ ‖normedMk S‖ * ‖↑x‖
[PROOFSTEP]
exact norm_lift_apply_le S.normedMk (fun x ↦ (eq_zero_iff x).2) x
[GOAL]
M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
h : ↑(topologicalClosure S) = univ
⊢ ‖normedMk S‖ = 0
[PROOFSTEP]
refine' le_antisymm (opNorm_le_bound _ le_rfl fun x => _) (norm_nonneg _)
[GOAL]
M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
h : ↑(topologicalClosure S) = univ
x : M
⊢ ‖↑(normedMk S) x‖ ≤ 0 * ‖x‖
[PROOFSTEP]
have hker : x ∈ S.normedMk.ker.topologicalClosure :=
  by
  rw [S.ker_normedMk, ← SetLike.mem_coe, h]
  trivial
[GOAL]
M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
h : ↑(topologicalClosure S) = univ
x : M
⊢ x ∈ topologicalClosure (ker (normedMk S))
[PROOFSTEP]
rw [S.ker_normedMk, ← SetLike.mem_coe, h]
[GOAL]
M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
h : ↑(topologicalClosure S) = univ
x : M
⊢ x ∈ univ
[PROOFSTEP]
trivial
[GOAL]
M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
h : ↑(topologicalClosure S) = univ
x : M
hker : x ∈ topologicalClosure (ker (normedMk S))
⊢ ‖↑(normedMk S) x‖ ≤ 0 * ‖x‖
[PROOFSTEP]
rw [ker_normedMk] at hker
[GOAL]
M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
h : ↑(topologicalClosure S) = univ
x : M
hker : x ∈ topologicalClosure S
⊢ ‖↑(normedMk S) x‖ ≤ 0 * ‖x‖
[PROOFSTEP]
simp only [(quotient_norm_eq_zero_iff S x).mpr hker, normedMk.apply, zero_mul, le_rfl]
[GOAL]
M : Type u_1
N✝ : Type u_2
inst✝² : SeminormedAddCommGroup M
inst✝¹ : SeminormedAddCommGroup N✝
N : Type u_3
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
f : NormedAddGroupHom M N
hf : ∀ (s : M), s ∈ S → ↑f s = 0
g : NormedAddGroupHom (M ⧸ S) N
h : NormedAddGroupHom.comp g (AddSubgroup.normedMk S) = f
⊢ g = lift S f hf
[PROOFSTEP]
ext x
[GOAL]
case H
M : Type u_1
N✝ : Type u_2
inst✝² : SeminormedAddCommGroup M
inst✝¹ : SeminormedAddCommGroup N✝
N : Type u_3
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
f : NormedAddGroupHom M N
hf : ∀ (s : M), s ∈ S → ↑f s = 0
g : NormedAddGroupHom (M ⧸ S) N
h : NormedAddGroupHom.comp g (AddSubgroup.normedMk S) = f
x : M ⧸ S
⊢ ↑g x = ↑(lift S f hf) x
[PROOFSTEP]
rcases AddSubgroup.surjective_normedMk _ x with ⟨x, rfl⟩
[GOAL]
case H.intro
M : Type u_1
N✝ : Type u_2
inst✝² : SeminormedAddCommGroup M
inst✝¹ : SeminormedAddCommGroup N✝
N : Type u_3
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
f : NormedAddGroupHom M N
hf : ∀ (s : M), s ∈ S → ↑f s = 0
g : NormedAddGroupHom (M ⧸ S) N
h : NormedAddGroupHom.comp g (AddSubgroup.normedMk S) = f
x : M
⊢ ↑g (↑(AddSubgroup.normedMk S) x) = ↑(lift S f hf) (↑(AddSubgroup.normedMk S) x)
[PROOFSTEP]
change g.comp S.normedMk x = _
[GOAL]
case H.intro
M : Type u_1
N✝ : Type u_2
inst✝² : SeminormedAddCommGroup M
inst✝¹ : SeminormedAddCommGroup N✝
N : Type u_3
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
f : NormedAddGroupHom M N
hf : ∀ (s : M), s ∈ S → ↑f s = 0
g : NormedAddGroupHom (M ⧸ S) N
h : NormedAddGroupHom.comp g (AddSubgroup.normedMk S) = f
x : M
⊢ ↑(NormedAddGroupHom.comp g (AddSubgroup.normedMk S)) x = ↑(lift S f hf) (↑(AddSubgroup.normedMk S) x)
[PROOFSTEP]
simp only [h]
[GOAL]
case H.intro
M : Type u_1
N✝ : Type u_2
inst✝² : SeminormedAddCommGroup M
inst✝¹ : SeminormedAddCommGroup N✝
N : Type u_3
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
f : NormedAddGroupHom M N
hf : ∀ (s : M), s ∈ S → ↑f s = 0
g : NormedAddGroupHom (M ⧸ S) N
h : NormedAddGroupHom.comp g (AddSubgroup.normedMk S) = f
x : M
⊢ ↑f x = ↑(lift S f hf) (↑(AddSubgroup.normedMk S) x)
[PROOFSTEP]
rfl
[GOAL]
M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
m : M
⊢ ‖↑(AddSubgroup.normedMk S) m‖ = sInf ((fun m_1 => ‖m + m_1‖) '' ↑(ker (AddSubgroup.normedMk S)))
[PROOFSTEP]
simpa [S.ker_normedMk] using quotient_norm_mk_eq _ m
[GOAL]
M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
f : NormedAddGroupHom M N
hquot : IsQuotient f
ε : ℝ
hε : 0 < ε
n : N
⊢ ∃ m, ↑f m = n ∧ ‖m‖ < ‖n‖ + ε
[PROOFSTEP]
obtain ⟨m, rfl⟩ := hquot.surjective n
[GOAL]
case intro
M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
f : NormedAddGroupHom M N
hquot : IsQuotient f
ε : ℝ
hε : 0 < ε
m : M
⊢ ∃ m_1, ↑f m_1 = ↑f m ∧ ‖m_1‖ < ‖↑f m‖ + ε
[PROOFSTEP]
have nonemp : ((fun m' => ‖m + m'‖) '' f.ker).Nonempty :=
  by
  rw [Set.nonempty_image_iff]
  exact ⟨0, f.ker.zero_mem⟩
[GOAL]
M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
f : NormedAddGroupHom M N
hquot : IsQuotient f
ε : ℝ
hε : 0 < ε
m : M
⊢ Set.Nonempty ((fun m' => ‖m + m'‖) '' ↑(ker f))
[PROOFSTEP]
rw [Set.nonempty_image_iff]
[GOAL]
M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
f : NormedAddGroupHom M N
hquot : IsQuotient f
ε : ℝ
hε : 0 < ε
m : M
⊢ Set.Nonempty ↑(ker f)
[PROOFSTEP]
exact ⟨0, f.ker.zero_mem⟩
[GOAL]
case intro
M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
f : NormedAddGroupHom M N
hquot : IsQuotient f
ε : ℝ
hε : 0 < ε
m : M
nonemp : Set.Nonempty ((fun m' => ‖m + m'‖) '' ↑(ker f))
⊢ ∃ m_1, ↑f m_1 = ↑f m ∧ ‖m_1‖ < ‖↑f m‖ + ε
[PROOFSTEP]
rcases Real.lt_sInf_add_pos nonemp hε with
  ⟨_, ⟨⟨x, hx, rfl⟩, H : ‖m + x‖ < sInf ((fun m' : M => ‖m + m'‖) '' f.ker) + ε⟩⟩
[GOAL]
case intro.intro.intro.intro.intro
M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
f : NormedAddGroupHom M N
hquot : IsQuotient f
ε : ℝ
hε : 0 < ε
m : M
nonemp : Set.Nonempty ((fun m' => ‖m + m'‖) '' ↑(ker f))
x : M
hx : x ∈ ↑(ker f)
H : ‖m + x‖ < sInf ((fun m' => ‖m + m'‖) '' ↑(ker f)) + ε
⊢ ∃ m_1, ↑f m_1 = ↑f m ∧ ‖m_1‖ < ‖↑f m‖ + ε
[PROOFSTEP]
exact ⟨m + x, by rw [map_add, (NormedAddGroupHom.mem_ker f x).mp hx, add_zero], by rwa [hquot.norm]⟩
[GOAL]
M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
f : NormedAddGroupHom M N
hquot : IsQuotient f
ε : ℝ
hε : 0 < ε
m : M
nonemp : Set.Nonempty ((fun m' => ‖m + m'‖) '' ↑(ker f))
x : M
hx : x ∈ ↑(ker f)
H : ‖m + x‖ < sInf ((fun m' => ‖m + m'‖) '' ↑(ker f)) + ε
⊢ ↑f (m + x) = ↑f m
[PROOFSTEP]
rw [map_add, (NormedAddGroupHom.mem_ker f x).mp hx, add_zero]
[GOAL]
M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
f : NormedAddGroupHom M N
hquot : IsQuotient f
ε : ℝ
hε : 0 < ε
m : M
nonemp : Set.Nonempty ((fun m' => ‖m + m'‖) '' ↑(ker f))
x : M
hx : x ∈ ↑(ker f)
H : ‖m + x‖ < sInf ((fun m' => ‖m + m'‖) '' ↑(ker f)) + ε
⊢ ‖m + x‖ < ‖↑f m‖ + ε
[PROOFSTEP]
rwa [hquot.norm]
[GOAL]
M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
f : NormedAddGroupHom M N
hquot : IsQuotient f
m : M
⊢ ‖↑f m‖ ≤ ‖m‖
[PROOFSTEP]
rw [hquot.norm]
[GOAL]
M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
f : NormedAddGroupHom M N
hquot : IsQuotient f
m : M
⊢ sInf ((fun m_1 => ‖m + m_1‖) '' ↑(ker f)) ≤ ‖m‖
[PROOFSTEP]
apply csInf_le
[GOAL]
case h₁
M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
f : NormedAddGroupHom M N
hquot : IsQuotient f
m : M
⊢ BddBelow ((fun m_1 => ‖m + m_1‖) '' ↑(ker f))
[PROOFSTEP]
use 0
[GOAL]
case h
M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
f : NormedAddGroupHom M N
hquot : IsQuotient f
m : M
⊢ 0 ∈ lowerBounds ((fun m_1 => ‖m + m_1‖) '' ↑(ker f))
[PROOFSTEP]
rintro _ ⟨m', -, rfl⟩
[GOAL]
case h.intro.intro
M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
f : NormedAddGroupHom M N
hquot : IsQuotient f
m m' : M
⊢ 0 ≤ (fun m_1 => ‖m + m_1‖) m'
[PROOFSTEP]
apply norm_nonneg
[GOAL]
case h₂
M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
f : NormedAddGroupHom M N
hquot : IsQuotient f
m : M
⊢ ‖m‖ ∈ (fun m_1 => ‖m + m_1‖) '' ↑(ker f)
[PROOFSTEP]
exact ⟨0, f.ker.zero_mem, by simp⟩
[GOAL]
M : Type u_1
N : Type u_2
inst✝¹ : SeminormedAddCommGroup M
inst✝ : SeminormedAddCommGroup N
f : NormedAddGroupHom M N
hquot : IsQuotient f
m : M
⊢ (fun m_1 => ‖m + m_1‖) 0 = ‖m‖
[PROOFSTEP]
simp
[GOAL]
M : Type u_1
N✝ : Type u_2
inst✝² : SeminormedAddCommGroup M
inst✝¹ : SeminormedAddCommGroup N✝
N : Type u_3
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
f : NormedAddGroupHom M N
hf : ∀ (s : M), s ∈ S → ↑f s = 0
fb : NormNoninc f
x : M ⧸ S
⊢ ‖↑(lift S f hf) x‖ ≤ ‖x‖
[PROOFSTEP]
have fb' : ‖f‖ ≤ (1 : ℝ≥0) := NormNoninc.normNoninc_iff_norm_le_one.mp fb
[GOAL]
M : Type u_1
N✝ : Type u_2
inst✝² : SeminormedAddCommGroup M
inst✝¹ : SeminormedAddCommGroup N✝
N : Type u_3
inst✝ : SeminormedAddCommGroup N
S : AddSubgroup M
f : NormedAddGroupHom M N
hf : ∀ (s : M), s ∈ S → ↑f s = 0
fb : NormNoninc f
x : M ⧸ S
fb' : ‖f‖ ≤ ↑1
⊢ ‖↑(lift S f hf) x‖ ≤ ‖x‖
[PROOFSTEP]
simpa using le_of_opNorm_le _ (f.lift_norm_le _ _ fb') _
[GOAL]
M : Type u_1
N : Type u_2
inst✝⁷ : SeminormedAddCommGroup M
inst✝⁶ : SeminormedAddCommGroup N
R : Type u_3
inst✝⁵ : Ring R
inst✝⁴ : Module R M
S : Submodule R M
𝕜 : Type u_4
inst✝³ : NormedField 𝕜
inst✝² : NormedSpace 𝕜 M
inst✝¹ : SMul 𝕜 R
inst✝ : IsScalarTower 𝕜 R M
src✝ : Module 𝕜 (M ⧸ S) := module' S
k : 𝕜
x : M ⧸ S
ε : ℝ
hε : 0 < ε
⊢ ‖k • x‖ ≤ ‖k‖ * ‖x‖ + ε
[PROOFSTEP]
have :=
  (nhds_basis_ball.tendsto_iff nhds_basis_ball).mp ((@Real.uniformContinuous_const_mul ‖k‖).continuous.tendsto ‖x‖) ε hε
[GOAL]
M : Type u_1
N : Type u_2
inst✝⁷ : SeminormedAddCommGroup M
inst✝⁶ : SeminormedAddCommGroup N
R : Type u_3
inst✝⁵ : Ring R
inst✝⁴ : Module R M
S : Submodule R M
𝕜 : Type u_4
inst✝³ : NormedField 𝕜
inst✝² : NormedSpace 𝕜 M
inst✝¹ : SMul 𝕜 R
inst✝ : IsScalarTower 𝕜 R M
src✝ : Module 𝕜 (M ⧸ S) := module' S
k : 𝕜
x : M ⧸ S
ε : ℝ
hε : 0 < ε
this :
  ∃ ia,
    0 < ia ∧ ∀ (x_1 : ℝ), x_1 ∈ ball ‖x‖ ia → (fun x x_2 => x * x_2) ‖k‖ x_1 ∈ ball ((fun x x_2 => x * x_2) ‖k‖ ‖x‖) ε
⊢ ‖k • x‖ ≤ ‖k‖ * ‖x‖ + ε
[PROOFSTEP]
simp only [mem_ball, exists_prop, dist, abs_sub_lt_iff] at this
[GOAL]
M : Type u_1
N : Type u_2
inst✝⁷ : SeminormedAddCommGroup M
inst✝⁶ : SeminormedAddCommGroup N
R : Type u_3
inst✝⁵ : Ring R
inst✝⁴ : Module R M
S : Submodule R M
𝕜 : Type u_4
inst✝³ : NormedField 𝕜
inst✝² : NormedSpace 𝕜 M
inst✝¹ : SMul 𝕜 R
inst✝ : IsScalarTower 𝕜 R M
src✝ : Module 𝕜 (M ⧸ S) := module' S
k : 𝕜
x : M ⧸ S
ε : ℝ
hε : 0 < ε
this :
  ∃ ia, 0 < ia ∧ ∀ (x_1 : ℝ), x_1 - ‖x‖ < ia ∧ ‖x‖ - x_1 < ia → ‖k‖ * x_1 - ‖k‖ * ‖x‖ < ε ∧ ‖k‖ * ‖x‖ - ‖k‖ * x_1 < ε
⊢ ‖k • x‖ ≤ ‖k‖ * ‖x‖ + ε
[PROOFSTEP]
rcases this with ⟨δ, hδ, h⟩
[GOAL]
case intro.intro
M : Type u_1
N : Type u_2
inst✝⁷ : SeminormedAddCommGroup M
inst✝⁶ : SeminormedAddCommGroup N
R : Type u_3
inst✝⁵ : Ring R
inst✝⁴ : Module R M
S : Submodule R M
𝕜 : Type u_4
inst✝³ : NormedField 𝕜
inst✝² : NormedSpace 𝕜 M
inst✝¹ : SMul 𝕜 R
inst✝ : IsScalarTower 𝕜 R M
src✝ : Module 𝕜 (M ⧸ S) := module' S
k : 𝕜
x : M ⧸ S
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
h : ∀ (x_1 : ℝ), x_1 - ‖x‖ < δ ∧ ‖x‖ - x_1 < δ → ‖k‖ * x_1 - ‖k‖ * ‖x‖ < ε ∧ ‖k‖ * ‖x‖ - ‖k‖ * x_1 < ε
⊢ ‖k • x‖ ≤ ‖k‖ * ‖x‖ + ε
[PROOFSTEP]
obtain ⟨a, rfl, ha⟩ := Submodule.Quotient.norm_mk_lt x hδ
[GOAL]
case intro.intro.intro.intro
M : Type u_1
N : Type u_2
inst✝⁷ : SeminormedAddCommGroup M
inst✝⁶ : SeminormedAddCommGroup N
R : Type u_3
inst✝⁵ : Ring R
inst✝⁴ : Module R M
S : Submodule R M
𝕜 : Type u_4
inst✝³ : NormedField 𝕜
inst✝² : NormedSpace 𝕜 M
inst✝¹ : SMul 𝕜 R
inst✝ : IsScalarTower 𝕜 R M
src✝ : Module 𝕜 (M ⧸ S) := module' S
k : 𝕜
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
a : M
h : ∀ (x : ℝ), x - ‖mk a‖ < δ ∧ ‖mk a‖ - x < δ → ‖k‖ * x - ‖k‖ * ‖mk a‖ < ε ∧ ‖k‖ * ‖mk a‖ - ‖k‖ * x < ε
ha : ‖a‖ < ‖mk a‖ + δ
⊢ ‖k • mk a‖ ≤ ‖k‖ * ‖mk a‖ + ε
[PROOFSTEP]
specialize h ‖a‖ ⟨by linarith, by linarith [Submodule.Quotient.norm_mk_le S a]⟩
[GOAL]
M : Type u_1
N : Type u_2
inst✝⁷ : SeminormedAddCommGroup M
inst✝⁶ : SeminormedAddCommGroup N
R : Type u_3
inst✝⁵ : Ring R
inst✝⁴ : Module R M
S : Submodule R M
𝕜 : Type u_4
inst✝³ : NormedField 𝕜
inst✝² : NormedSpace 𝕜 M
inst✝¹ : SMul 𝕜 R
inst✝ : IsScalarTower 𝕜 R M
src✝ : Module 𝕜 (M ⧸ S) := module' S
k : 𝕜
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
a : M
h : ∀ (x : ℝ), x - ‖mk a‖ < δ ∧ ‖mk a‖ - x < δ → ‖k‖ * x - ‖k‖ * ‖mk a‖ < ε ∧ ‖k‖ * ‖mk a‖ - ‖k‖ * x < ε
ha : ‖a‖ < ‖mk a‖ + δ
⊢ ‖a‖ - ‖mk a‖ < δ
[PROOFSTEP]
linarith
[GOAL]
M : Type u_1
N : Type u_2
inst✝⁷ : SeminormedAddCommGroup M
inst✝⁶ : SeminormedAddCommGroup N
R : Type u_3
inst✝⁵ : Ring R
inst✝⁴ : Module R M
S : Submodule R M
𝕜 : Type u_4
inst✝³ : NormedField 𝕜
inst✝² : NormedSpace 𝕜 M
inst✝¹ : SMul 𝕜 R
inst✝ : IsScalarTower 𝕜 R M
src✝ : Module 𝕜 (M ⧸ S) := module' S
k : 𝕜
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
a : M
h : ∀ (x : ℝ), x - ‖mk a‖ < δ ∧ ‖mk a‖ - x < δ → ‖k‖ * x - ‖k‖ * ‖mk a‖ < ε ∧ ‖k‖ * ‖mk a‖ - ‖k‖ * x < ε
ha : ‖a‖ < ‖mk a‖ + δ
⊢ ‖mk a‖ - ‖a‖ < δ
[PROOFSTEP]
linarith [Submodule.Quotient.norm_mk_le S a]
[GOAL]
case intro.intro.intro.intro
M : Type u_1
N : Type u_2
inst✝⁷ : SeminormedAddCommGroup M
inst✝⁶ : SeminormedAddCommGroup N
R : Type u_3
inst✝⁵ : Ring R
inst✝⁴ : Module R M
S : Submodule R M
𝕜 : Type u_4
inst✝³ : NormedField 𝕜
inst✝² : NormedSpace 𝕜 M
inst✝¹ : SMul 𝕜 R
inst✝ : IsScalarTower 𝕜 R M
src✝ : Module 𝕜 (M ⧸ S) := module' S
k : 𝕜
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ : 0 < δ
a : M
ha : ‖a‖ < ‖mk a‖ + δ
h : ‖k‖ * ‖a‖ - ‖k‖ * ‖mk a‖ < ε ∧ ‖k‖ * ‖mk a‖ - ‖k‖ * ‖a‖ < ε
⊢ ‖k • mk a‖ ≤ ‖k‖ * ‖mk a‖ + ε
[PROOFSTEP]
calc
  _ ≤ ‖k‖ * ‖a‖ := (quotient_norm_mk_le S.toAddSubgroup (k • a)).trans_eq (norm_smul k a)
  _ ≤ _ := (sub_lt_iff_lt_add'.mp h.1).le
[GOAL]
M : Type u_1
N : Type u_2
inst✝² : SeminormedAddCommGroup M
inst✝¹ : SeminormedAddCommGroup N
R : Type u_3
inst✝ : SeminormedCommRing R
I : Ideal R
x y : R ⧸ I
ε : ℝ
hε : 0 < ε
⊢ ‖x * y‖ ≤ ‖x‖ * ‖y‖ + ε
[PROOFSTEP]
have :=
  ((nhds_basis_ball.prod_nhds nhds_basis_ball).tendsto_iff nhds_basis_ball).mp (continuous_mul.tendsto (‖x‖, ‖y‖)) ε hε
[GOAL]
M : Type u_1
N : Type u_2
inst✝² : SeminormedAddCommGroup M
inst✝¹ : SeminormedAddCommGroup N
R : Type u_3
inst✝ : SeminormedCommRing R
I : Ideal R
x y : R ⧸ I
ε : ℝ
hε : 0 < ε
this :
  ∃ ia,
    (0 < ia.fst ∧ 0 < ia.snd) ∧
      ∀ (x_1 : ℝ × ℝ),
        x_1 ∈ ball ‖x‖ ia.fst ×ˢ ball ‖y‖ ia.snd → x_1.fst * x_1.snd ∈ ball ((‖x‖, ‖y‖).fst * (‖x‖, ‖y‖).snd) ε
⊢ ‖x * y‖ ≤ ‖x‖ * ‖y‖ + ε
[PROOFSTEP]
simp only [Set.mem_prod, mem_ball, and_imp, Prod.forall, exists_prop, Prod.exists] at this
[GOAL]
M : Type u_1
N : Type u_2
inst✝² : SeminormedAddCommGroup M
inst✝¹ : SeminormedAddCommGroup N
R : Type u_3
inst✝ : SeminormedCommRing R
I : Ideal R
x y : R ⧸ I
ε : ℝ
hε : 0 < ε
this : ∃ a b, (0 < a ∧ 0 < b) ∧ ∀ (a_1 b_1 : ℝ), dist a_1 ‖x‖ < a → dist b_1 ‖y‖ < b → dist (a_1 * b_1) (‖x‖ * ‖y‖) < ε
⊢ ‖x * y‖ ≤ ‖x‖ * ‖y‖ + ε
[PROOFSTEP]
rcases this with ⟨ε₁, ε₂, ⟨h₁, h₂⟩, h⟩
[GOAL]
case intro.intro.intro.intro
M : Type u_1
N : Type u_2
inst✝² : SeminormedAddCommGroup M
inst✝¹ : SeminormedAddCommGroup N
R : Type u_3
inst✝ : SeminormedCommRing R
I : Ideal R
x y : R ⧸ I
ε : ℝ
hε : 0 < ε
ε₁ ε₂ : ℝ
h : ∀ (a b : ℝ), dist a ‖x‖ < ε₁ → dist b ‖y‖ < ε₂ → dist (a * b) (‖x‖ * ‖y‖) < ε
h₁ : 0 < ε₁
h₂ : 0 < ε₂
⊢ ‖x * y‖ ≤ ‖x‖ * ‖y‖ + ε
[PROOFSTEP]
obtain ⟨⟨a, rfl, ha⟩, ⟨b, rfl, hb⟩⟩ := Ideal.Quotient.norm_mk_lt x h₁, Ideal.Quotient.norm_mk_lt y h₂
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro
M : Type u_1
N : Type u_2
inst✝² : SeminormedAddCommGroup M
inst✝¹ : SeminormedAddCommGroup N
R : Type u_3
inst✝ : SeminormedCommRing R
I : Ideal R
ε : ℝ
hε : 0 < ε
ε₁ ε₂ : ℝ
h₁ : 0 < ε₁
h₂ : 0 < ε₂
a : R
ha : ‖a‖ < ‖↑(mk I) a‖ + ε₁
b : R
h :
  ∀ (a_1 b_1 : ℝ),
    dist a_1 ‖↑(mk I) a‖ < ε₁ → dist b_1 ‖↑(mk I) b‖ < ε₂ → dist (a_1 * b_1) (‖↑(mk I) a‖ * ‖↑(mk I) b‖) < ε
hb : ‖b‖ < ‖↑(mk I) b‖ + ε₂
⊢ ‖↑(mk I) a * ↑(mk I) b‖ ≤ ‖↑(mk I) a‖ * ‖↑(mk I) b‖ + ε
[PROOFSTEP]
simp only [dist, abs_sub_lt_iff] at h
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro
M : Type u_1
N : Type u_2
inst✝² : SeminormedAddCommGroup M
inst✝¹ : SeminormedAddCommGroup N
R : Type u_3
inst✝ : SeminormedCommRing R
I : Ideal R
ε : ℝ
hε : 0 < ε
ε₁ ε₂ : ℝ
h₁ : 0 < ε₁
h₂ : 0 < ε₂
a : R
ha : ‖a‖ < ‖↑(mk I) a‖ + ε₁
b : R
hb : ‖b‖ < ‖↑(mk I) b‖ + ε₂
h :
  ∀ (a_1 b_1 : ℝ),
    a_1 - ‖↑(mk I) a‖ < ε₁ ∧ ‖↑(mk I) a‖ - a_1 < ε₁ →
      b_1 - ‖↑(mk I) b‖ < ε₂ ∧ ‖↑(mk I) b‖ - b_1 < ε₂ →
        a_1 * b_1 - ‖↑(mk I) a‖ * ‖↑(mk I) b‖ < ε ∧ ‖↑(mk I) a‖ * ‖↑(mk I) b‖ - a_1 * b_1 < ε
⊢ ‖↑(mk I) a * ↑(mk I) b‖ ≤ ‖↑(mk I) a‖ * ‖↑(mk I) b‖ + ε
[PROOFSTEP]
specialize
  h ‖a‖ ‖b‖ ⟨by linarith, by linarith [Ideal.Quotient.norm_mk_le I a]⟩
    ⟨by linarith, by linarith [Ideal.Quotient.norm_mk_le I b]⟩
[GOAL]
M : Type u_1
N : Type u_2
inst✝² : SeminormedAddCommGroup M
inst✝¹ : SeminormedAddCommGroup N
R : Type u_3
inst✝ : SeminormedCommRing R
I : Ideal R
ε : ℝ
hε : 0 < ε
ε₁ ε₂ : ℝ
h₁ : 0 < ε₁
h₂ : 0 < ε₂
a : R
ha : ‖a‖ < ‖↑(mk I) a‖ + ε₁
b : R
hb : ‖b‖ < ‖↑(mk I) b‖ + ε₂
h :
  ∀ (a_1 b_1 : ℝ),
    a_1 - ‖↑(mk I) a‖ < ε₁ ∧ ‖↑(mk I) a‖ - a_1 < ε₁ →
      b_1 - ‖↑(mk I) b‖ < ε₂ ∧ ‖↑(mk I) b‖ - b_1 < ε₂ →
        a_1 * b_1 - ‖↑(mk I) a‖ * ‖↑(mk I) b‖ < ε ∧ ‖↑(mk I) a‖ * ‖↑(mk I) b‖ - a_1 * b_1 < ε
⊢ ‖a‖ - ‖↑(mk I) a‖ < ε₁
[PROOFSTEP]
linarith
[GOAL]
M : Type u_1
N : Type u_2
inst✝² : SeminormedAddCommGroup M
inst✝¹ : SeminormedAddCommGroup N
R : Type u_3
inst✝ : SeminormedCommRing R
I : Ideal R
ε : ℝ
hε : 0 < ε
ε₁ ε₂ : ℝ
h₁ : 0 < ε₁
h₂ : 0 < ε₂
a : R
ha : ‖a‖ < ‖↑(mk I) a‖ + ε₁
b : R
hb : ‖b‖ < ‖↑(mk I) b‖ + ε₂
h :
  ∀ (a_1 b_1 : ℝ),
    a_1 - ‖↑(mk I) a‖ < ε₁ ∧ ‖↑(mk I) a‖ - a_1 < ε₁ →
      b_1 - ‖↑(mk I) b‖ < ε₂ ∧ ‖↑(mk I) b‖ - b_1 < ε₂ →
        a_1 * b_1 - ‖↑(mk I) a‖ * ‖↑(mk I) b‖ < ε ∧ ‖↑(mk I) a‖ * ‖↑(mk I) b‖ - a_1 * b_1 < ε
⊢ ‖↑(mk I) a‖ - ‖a‖ < ε₁
[PROOFSTEP]
linarith [Ideal.Quotient.norm_mk_le I a]
[GOAL]
M : Type u_1
N : Type u_2
inst✝² : SeminormedAddCommGroup M
inst✝¹ : SeminormedAddCommGroup N
R : Type u_3
inst✝ : SeminormedCommRing R
I : Ideal R
ε : ℝ
hε : 0 < ε
ε₁ ε₂ : ℝ
h₁ : 0 < ε₁
h₂ : 0 < ε₂
a : R
ha : ‖a‖ < ‖↑(mk I) a‖ + ε₁
b : R
hb : ‖b‖ < ‖↑(mk I) b‖ + ε₂
h :
  ∀ (a_1 b_1 : ℝ),
    a_1 - ‖↑(mk I) a‖ < ε₁ ∧ ‖↑(mk I) a‖ - a_1 < ε₁ →
      b_1 - ‖↑(mk I) b‖ < ε₂ ∧ ‖↑(mk I) b‖ - b_1 < ε₂ →
        a_1 * b_1 - ‖↑(mk I) a‖ * ‖↑(mk I) b‖ < ε ∧ ‖↑(mk I) a‖ * ‖↑(mk I) b‖ - a_1 * b_1 < ε
⊢ ‖b‖ - ‖↑(mk I) b‖ < ε₂
[PROOFSTEP]
linarith
[GOAL]
M : Type u_1
N : Type u_2
inst✝² : SeminormedAddCommGroup M
inst✝¹ : SeminormedAddCommGroup N
R : Type u_3
inst✝ : SeminormedCommRing R
I : Ideal R
ε : ℝ
hε : 0 < ε
ε₁ ε₂ : ℝ
h₁ : 0 < ε₁
h₂ : 0 < ε₂
a : R
ha : ‖a‖ < ‖↑(mk I) a‖ + ε₁
b : R
hb : ‖b‖ < ‖↑(mk I) b‖ + ε₂
h :
  ∀ (a_1 b_1 : ℝ),
    a_1 - ‖↑(mk I) a‖ < ε₁ ∧ ‖↑(mk I) a‖ - a_1 < ε₁ →
      b_1 - ‖↑(mk I) b‖ < ε₂ ∧ ‖↑(mk I) b‖ - b_1 < ε₂ →
        a_1 * b_1 - ‖↑(mk I) a‖ * ‖↑(mk I) b‖ < ε ∧ ‖↑(mk I) a‖ * ‖↑(mk I) b‖ - a_1 * b_1 < ε
⊢ ‖↑(mk I) b‖ - ‖b‖ < ε₂
[PROOFSTEP]
linarith [Ideal.Quotient.norm_mk_le I b]
[GOAL]
case intro.intro.intro.intro.intro.intro.intro.intro
M : Type u_1
N : Type u_2
inst✝² : SeminormedAddCommGroup M
inst✝¹ : SeminormedAddCommGroup N
R : Type u_3
inst✝ : SeminormedCommRing R
I : Ideal R
ε : ℝ
hε : 0 < ε
ε₁ ε₂ : ℝ
h₁ : 0 < ε₁
h₂ : 0 < ε₂
a : R
ha : ‖a‖ < ‖↑(mk I) a‖ + ε₁
b : R
hb : ‖b‖ < ‖↑(mk I) b‖ + ε₂
h : ‖a‖ * ‖b‖ - ‖↑(mk I) a‖ * ‖↑(mk I) b‖ < ε ∧ ‖↑(mk I) a‖ * ‖↑(mk I) b‖ - ‖a‖ * ‖b‖ < ε
⊢ ‖↑(mk I) a * ↑(mk I) b‖ ≤ ‖↑(mk I) a‖ * ‖↑(mk I) b‖ + ε
[PROOFSTEP]
calc
  _ ≤ ‖a‖ * ‖b‖ := (Ideal.Quotient.norm_mk_le I (a * b)).trans (norm_mul_le a b)
  _ ≤ _ := (sub_lt_iff_lt_add'.mp h.1).le