-- Mathlib/Analysis/Complex/Schwarz.lean
theorem affine_of_mapsTo_ball_of_exists_norm_dslope_eq_div [CompleteSpace E] [StrictConvexSpace ℝ E]
    (hd : DifferentiableOn ℂ f (ball c R₁)) (h_maps : Set.MapsTo f (ball c R₁) (ball (f c) R₂))
    (h_z₀ : z₀ ∈ ball c R₁) (h_eq : ‖dslope f c z₀‖ = R₂ / R₁) :
    Set.EqOn f (fun z => f c + (z - c) • dslope f c z₀) (ball c R₁)

Proof state:
case neg
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
R₁ R₂ : ℝ
f : ℂ → E
c z₀ : ℂ
inst✝¹ : CompleteSpace E
inst✝ : StrictConvexSpace ℝ E
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (ball (f c) R₂)
h_z₀ : z₀ ∈ ball c R₁
g : ℂ → E := dslope f c
h_eq : ‖g z₀‖ = R₂ / R₁
z : ℂ
hz : z ∈ ball c R₁
h : ¬z = c
h_R₁ : 0 < R₁
g_le_div : ∀ z ∈ ball c R₁, ‖g z‖ ≤ R₂ / R₁
g_max : IsMaxOn (norm ∘ g) (ball c R₁) z₀
g_diff : DifferentiableOn ℂ g (ball c R₁)
this : g z = g z₀
⊢ f z = (fun z => f c + (z - c) • g z₀) z

Tactic:
simp only [g] at this

Result:
case neg
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
R₁ R₂ : ℝ
f : ℂ → E
c z₀ : ℂ
inst✝¹ : CompleteSpace E
inst✝ : StrictConvexSpace ℝ E
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (ball (f c) R₂)
h_z₀ : z₀ ∈ ball c R₁
g : ℂ → E := dslope f c
h_eq : ‖g z₀‖ = R₂ / R₁
z : ℂ
hz : z ∈ ball c R₁
h : ¬z = c
h_R₁ : 0 < R₁
g_le_div : ∀ z ∈ ball c R₁, ‖g z‖ ≤ R₂ / R₁
g_max : IsMaxOn (norm ∘ g) (ball c R₁) z₀
g_diff : DifferentiableOn ℂ g (ball c R₁)
this : dslope f c z = dslope f c z₀
⊢ f z = (fun z => f c + (z - c) • g z₀) z

Proof state:
case neg
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
R₁ R₂ : ℝ
f : ℂ → E
c z₀ : ℂ
inst✝¹ : CompleteSpace E
inst✝ : StrictConvexSpace ℝ E
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (ball (f c) R₂)
h_z₀ : z₀ ∈ ball c R₁
g : ℂ → E := dslope f c
h_eq : ‖g z₀‖ = R₂ / R₁
z : ℂ
hz : z ∈ ball c R₁
h : ¬z = c
h_R₁ : 0 < R₁
g_le_div : ∀ z ∈ ball c R₁, ‖g z‖ ≤ R₂ / R₁
g_max : IsMaxOn (norm ∘ g) (ball c R₁) z₀
g_diff : DifferentiableOn ℂ g (ball c R₁)
this : dslope f c z = dslope f c z₀
⊢ f z = (fun z => f c + (z - c) • g z₀) z

Tactic:
simp [g, ← this]

Result:
no goals

Proof state:
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
R₁ R₂ : ℝ
f : ℂ → E
c z₀ : ℂ
inst✝¹ : CompleteSpace E
inst✝ : StrictConvexSpace ℝ E
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (ball (f c) R₂)
h_z₀ : z₀ ∈ ball c R₁
g : ℂ → E := dslope f c
h_eq : ‖g z₀‖ = R₂ / R₁
z✝ : ℂ
hz✝ : z✝ ∈ ball c R₁
h : ¬z✝ = c
h_R₁ : 0 < R₁
g_le_div : ∀ z ∈ ball c R₁, ‖g z‖ ≤ R₂ / R₁
z : ℂ
hz : z ∈ ball c R₁
⊢ (norm ∘ g) z ≤ (norm ∘ g) z₀

Tactic:
simpa [h_eq] using g_le_div z hz

Result:
no goals

Proof state:
case neg
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
R₁ R₂ : ℝ
f : ℂ → E
c z₀ : ℂ
inst✝¹ : CompleteSpace E
inst✝ : StrictConvexSpace ℝ E
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (ball (f c) R₂)
h_z₀ : z₀ ∈ ball c R₁
g : ℂ → E := dslope f c
h_eq : ‖g z₀‖ = R₂ / R₁
z : ℂ
hz : z ∈ ball c R₁
h : ¬z = c
h_R₁ : 0 < R₁
⊢ f z = (fun z => f c + (z - c) • g z₀) z

Tactic:
have g_le_div : ∀ z ∈ ball c R₁, ‖g z‖ ≤ R₂ / R₁ := fun z hz =>
  norm_dslope_le_div_of_mapsTo_ball hd h_maps hz

Result:
case neg
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℂ E
R₁ R₂ : ℝ
f : ℂ → E
c z₀ : ℂ
inst✝¹ : CompleteSpace E
inst✝ : StrictConvexSpace ℝ E
hd : DifferentiableOn ℂ f (ball c R₁)
h_maps : MapsTo f (ball c R₁) (ball (f c) R₂)
h_z₀ : z₀ ∈ ball c R₁
g : ℂ → E := dslope f c
h_eq : ‖g z₀‖ = R₂ / R₁
z : ℂ
hz : z ∈ ball c R₁
h : ¬z = c
h_R₁ : 0 < R₁
g_le_div : ∀ z ∈ ball c R₁, ‖g z‖ ≤ R₂ / R₁
⊢ f z = (fun z => f c + (z - c) • g z₀) z