-- 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:
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₁
h_eq : ‖dslope f c z₀‖ = R₂ / R₁
⊢ EqOn f (fun z => f c + (z - c) • dslope f c z₀) (ball c R₁)

Tactic:
set g := dslope f c

Result:
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₁
⊢ EqOn f (fun z => f c + (z - c) • g 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₁
⊢ f z = (fun z => f c + (z - c) • g z₀) z

Tactic:
have g_max : IsMaxOn (norm ∘ g) (ball c R₁) z₀ :=
  isMaxOn_iff.mpr fun z hz => by simpa [h_eq] using g_le_div z 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₁
g_max : IsMaxOn (norm ∘ g) (ball c R₁) z₀
⊢ f z = (fun z => f c + (z - c) • g z₀) z

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₁
⊢ EqOn f (fun z => f c + (z - c) • g z₀) (ball c R₁)

Tactic:
rintro z hz

Result:
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₁
⊢ f z = (fun z => f c + (z - c) • g z₀) z

Proof state:
case pos
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
⊢ f z = (fun z => f c + (z - c) • g z₀) z

Tactic:
simp [h]

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₁
g_le_div : ∀ z ∈ ball c R₁, ‖g z‖ ≤ R₂ / R₁
g_max : IsMaxOn (norm ∘ g) (ball c R₁) z₀
⊢ f z = (fun z => f c + (z - c) • g z₀) z

Tactic:
have g_diff : DifferentiableOn ℂ g (ball c R₁) :=
  (differentiableOn_dslope (isOpen_ball.mem_nhds (mem_ball_self h_R₁))).mpr hd

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₁)
⊢ 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
⊢ f z = (fun z => f c + (z - c) • g z₀) z

Tactic:
have h_R₁ : 0 < R₁ := nonempty_ball.mp ⟨_, h_z₀⟩

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₁
⊢ f z = (fun z => f c + (z - c) • g z₀) z

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₁
⊢ f z = (fun z => f c + (z - c) • g z₀) z

Tactic:
by_cases h : z = c

Result:
case pos
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
⊢ f z = (fun z => f c + (z - c) • g z₀) z

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
⊢ 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₁)
⊢ f z = (fun z => f c + (z - c) • g z₀) z

Tactic:
have : g z = g z₀ := eqOn_of_isPreconnected_of_isMaxOn_norm (convex_ball c R₁).isPreconnected
  isOpen_ball g_diff h_z₀ g_max 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₁
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