-- Mathlib/Analysis/Complex/Schwarz.lean
theorem norm_dslope_le_div_of_mapsTo_ball (hd : DifferentiableOn ℂ f (ball c R₁))
    (h_maps : MapsTo f (ball c R₁) (ball (f c) R₂)) (hz : z ∈ ball c R₁) :
    ‖dslope f c z‖ ≤ R₂ / R₁

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R₁ R₂ : ℝ
f : ℂ → E
c z : ℂ
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (ball (f c) R₂)
hz : z ∈ ball c R₁
hR₁ : 0 < R₁
hR₂ : 0 < R₂
hc : dslope f c z ≠ 0
g : E →L[ℂ] ℂ
hg : ‖g‖ = 1
hgf : g (dslope f c z) = ↑‖dslope f c z‖
hg' : ‖g‖₊ = 1
hg₀ : ‖g‖₊ ≠ 0
⊢ ‖dslope f c z‖ = ‖dslope (⇑g ∘ f) c z‖

Tactic:
rw [g.dslope_comp, hgf, RCLike.norm_ofReal, abs_norm]

Result:
case H
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R₁ R₂ : ℝ
f : ℂ → E
c z : ℂ
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (ball (f c) R₂)
hz : z ∈ ball c R₁
hR₁ : 0 < R₁
hR₂ : 0 < R₂
hc : dslope f c z ≠ 0
g : E →L[ℂ] ℂ
hg : ‖g‖ = 1
hgf : g (dslope f c z) = ↑‖dslope f c z‖
hg' : ‖g‖₊ = 1
hg₀ : ‖g‖₊ ≠ 0
⊢ c = z → DifferentiableAt ℂ f c

Proof state:
case inr.intro.intro
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R₁ R₂ : ℝ
f : ℂ → E
c z : ℂ
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (ball (f c) R₂)
hz : z ∈ ball c R₁
hR₁ : 0 < R₁
hR₂ : 0 < R₂
hc : dslope f c z ≠ 0
g : E →L[ℂ] ℂ
hg : ‖g‖ = 1
hgf : g (dslope f c z) = ↑‖dslope f c z‖
hg' : ‖g‖₊ = 1
⊢ ‖dslope f c z‖ ≤ R₂ / R₁

Tactic:
have hg₀ : ‖g‖₊ ≠ 0 := by simpa only [hg'] using one_ne_zero

Result:
case inr.intro.intro
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R₁ R₂ : ℝ
f : ℂ → E
c z : ℂ
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (ball (f c) R₂)
hz : z ∈ ball c R₁
hR₁ : 0 < R₁
hR₂ : 0 < R₂
hc : dslope f c z ≠ 0
g : E →L[ℂ] ℂ
hg : ‖g‖ = 1
hgf : g (dslope f c z) = ↑‖dslope f c z‖
hg' : ‖g‖₊ = 1
hg₀ : ‖g‖₊ ≠ 0
⊢ ‖dslope f c z‖ ≤ R₂ / R₁

Proof state:
case inr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R₁ R₂ : ℝ
f : ℂ → E
c z : ℂ
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (ball (f c) R₂)
hz : z ∈ ball c R₁
hR₁ : 0 < R₁
hR₂ : 0 < R₂
hc : dslope f c z ≠ 0
⊢ ‖dslope f c z‖ ≤ R₂ / R₁

Tactic:
rcases exists_dual_vector ℂ _ hc with ⟨g, hg, hgf⟩

Result:
case inr.intro.intro
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R₁ R₂ : ℝ
f : ℂ → E
c z : ℂ
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (ball (f c) R₂)
hz : z ∈ ball c R₁
hR₁ : 0 < R₁
hR₂ : 0 < R₂
hc : dslope f c z ≠ 0
g : E →L[ℂ] ℂ
hg : ‖g‖ = 1
hgf : g (dslope f c z) = ↑‖dslope f c z‖
⊢ ‖dslope f c z‖ ≤ R₂ / R₁

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R₁ R₂ : ℝ
f : ℂ → E
c z : ℂ
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (ball (f c) R₂)
hz : z ∈ ball c R₁
⊢ ‖dslope f c z‖ ≤ R₂ / R₁

Tactic:
have hR₁ : 0 < R₁ := nonempty_ball.1 ⟨z, hz⟩

Result:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R₁ R₂ : ℝ
f : ℂ → E
c z : ℂ
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (ball (f c) R₂)
hz : z ∈ ball c R₁
hR₁ : 0 < R₁
⊢ ‖dslope f c z‖ ≤ R₂ / R₁

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R₁ R₂ : ℝ
f : ℂ → E
c z : ℂ
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (ball (f c) R₂)
hz : z ∈ ball c R₁
hR₁ : 0 < R₁
hR₂ : 0 < R₂
⊢ ‖dslope f c z‖ ≤ R₂ / R₁

Tactic:
rcases eq_or_ne (dslope f c z) 0 with hc | hc

Result:
case inl
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R₁ R₂ : ℝ
f : ℂ → E
c z : ℂ
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (ball (f c) R₂)
hz : z ∈ ball c R₁
hR₁ : 0 < R₁
hR₂ : 0 < R₂
hc : dslope f c z = 0
⊢ ‖dslope f c z‖ ≤ R₂ / R₁

case inr
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R₁ R₂ : ℝ
f : ℂ → E
c z : ℂ
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (ball (f c) R₂)
hz : z ∈ ball c R₁
hR₁ : 0 < R₁
hR₂ : 0 < R₂
hc : dslope f c z ≠ 0
⊢ ‖dslope f c z‖ ≤ R₂ / R₁

Proof state:
case H
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R₁ R₂ : ℝ
f : ℂ → E
c z : ℂ
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (ball (f c) R₂)
hz : z ∈ ball c R₁
hR₁ : 0 < R₁
hR₂ : 0 < R₂
hc : dslope f c z ≠ 0
g : E →L[ℂ] ℂ
hg : ‖g‖ = 1
hgf : g (dslope f c z) = ↑‖dslope f c z‖
hg' : ‖g‖₊ = 1
hg₀ : ‖g‖₊ ≠ 0
⊢ c = z → DifferentiableAt ℂ f c

Tactic:
exact fun _ => hd.differentiableAt (ball_mem_nhds _ hR₁)

Result:
no goals

Proof state:
case inl
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R₁ R₂ : ℝ
f : ℂ → E
c z : ℂ
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (ball (f c) R₂)
hz : z ∈ ball c R₁
hR₁ : 0 < R₁
hR₂ : 0 < R₂
hc : dslope f c z = 0
⊢ ‖dslope f c z‖ ≤ R₂ / R₁

Tactic:
rw [hc, norm_zero]

Result:
case inl
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R₁ R₂ : ℝ
f : ℂ → E
c z : ℂ
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (ball (f c) R₂)
hz : z ∈ ball c R₁
hR₁ : 0 < R₁
hR₂ : 0 < R₂
hc : dslope f c z = 0
⊢ 0 ≤ R₂ / R₁

Proof state:
case inl
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R₁ R₂ : ℝ
f : ℂ → E
c z : ℂ
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (ball (f c) R₂)
hz : z ∈ ball c R₁
hR₁ : 0 < R₁
hR₂ : 0 < R₂
hc : dslope f c z = 0
⊢ 0 ≤ R₂ / R₁

Tactic:
exact div_nonneg hR₂.le hR₁.le

Result:
no goals

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R₁ R₂ : ℝ
f : ℂ → E
c z : ℂ
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (ball (f c) R₂)
hz : z ∈ ball c R₁
hR₁ : 0 < R₁
hR₂ : 0 < R₂
hc : dslope f c z ≠ 0
g : E →L[ℂ] ℂ
hg : ‖g‖ = 1
hgf : g (dslope f c z) = ↑‖dslope f c z‖
hg' : ‖g‖₊ = 1
hg₀ : ‖g‖₊ ≠ 0
⊢ ‖dslope (⇑g ∘ f) c z‖ ≤ R₂ / R₁

Tactic:
refine schwarz_aux (g.differentiable.comp_differentiableOn hd) (MapsTo.comp ?_ h_maps) hz

Result:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R₁ R₂ : ℝ
f : ℂ → E
c z : ℂ
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (ball (f c) R₂)
hz : z ∈ ball c R₁
hR₁ : 0 < R₁
hR₂ : 0 < R₂
hc : dslope f c z ≠ 0
g : E →L[ℂ] ℂ
hg : ‖g‖ = 1
hgf : g (dslope f c z) = ↑‖dslope f c z‖
hg' : ‖g‖₊ = 1
hg₀ : ‖g‖₊ ≠ 0
⊢ MapsTo (⇑g) (ball (f c) R₂) (ball ((⇑g ∘ f) c) R₂)

Proof state:
case inr.intro.intro
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R₁ R₂ : ℝ
f : ℂ → E
c z : ℂ
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (ball (f c) R₂)
hz : z ∈ ball c R₁
hR₁ : 0 < R₁
hR₂ : 0 < R₂
hc : dslope f c z ≠ 0
g : E →L[ℂ] ℂ
hg : ‖g‖ = 1
hgf : g (dslope f c z) = ↑‖dslope f c z‖
hg' : ‖g‖₊ = 1
hg₀ : ‖g‖₊ ≠ 0
⊢ ‖dslope f c z‖ ≤ R₂ / R₁

Tactic:
calc
  ‖dslope f c z‖ = ‖dslope (g ∘ f) c z‖ := by
    rw [g.dslope_comp, hgf, RCLike.norm_ofReal, abs_norm]
    exact fun _ => hd.differentiableAt (ball_mem_nhds _ hR₁)
  _ ≤ R₂ / R₁ := by
    refine schwarz_aux (g.differentiable.comp_differentiableOn hd) (MapsTo.comp ?_ h_maps) hz
    simpa only [hg', NNReal.coe_one, one_mul] using g.lipschitz.mapsTo_ball hg₀ (f c) R₂

Result:
no goals

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R₁ R₂ : ℝ
f : ℂ → E
c z : ℂ
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (ball (f c) R₂)
hz : z ∈ ball c R₁
hR₁ : 0 < R₁
⊢ ‖dslope f c z‖ ≤ R₂ / R₁

Tactic:
have hR₂ : 0 < R₂ := nonempty_ball.1 ⟨f z, h_maps hz⟩

Result:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
R₁ R₂ : ℝ
f : ℂ → E
c z : ℂ
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (ball (f c) R₂)
hz : z ∈ ball c R₁
hR₁ : 0 < R₁
hR₂ : 0 < R₂
⊢ ‖dslope f c z‖ ≤ R₂ / R₁