awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Complex.Hadamard (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
z : ℂ
a b : ℝ
hz : z ∈ verticalClosedStrip 0 1
hd : DiffContOnCl ℂ f (verticalStrip 0 1)
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
ha : ∀ z ∈ re ⁻¹' {0}, ‖f z‖ ≤ a
hb : ∀ z ∈ re ⁻¹' {1}, ‖f z‖ ≤ b
this : ‖interpStrip f z‖ ≤ sSupNormIm f 0 ^ (1 - z.re) * sSupNormIm f 1 ^ z.re
⊢ ‖f z‖ ≤ a ^ (1 - z.re) * b ^ z.re
have apply : sSupNormIm f 0 ^ (1 - z.re) * sSupNormIm f 1 ^ z.re ≤ a ^ (1 - z.re) * b ^ z.re
Tactic: apply (norm_le_interpStrip_of_mem_verticalClosedStrip₀₁ f hz hd hB).trans (this.trans _)
-- Lean 4 proof step from Mathlib.Analysis.Complex.Hadamard (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
z : ℂ
a b : ℝ
hz : z ∈ verticalClosedStrip 0 1
hd : DiffContOnCl ℂ f (verticalStrip 0 1)
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
ha : ∀ z ∈ re ⁻¹' {0}, ‖f z‖ ≤ a
hb : ∀ z ∈ re ⁻¹' {1}, ‖f z‖ ≤ b
this : ‖interpStrip f z‖ ≤ sSupNormIm f 0 ^ (1 - z.re) * sSupNormIm f 1 ^ z.re
⊢ sSupNormIm f 0 ^ (1 - z.re) * sSupNormIm f 1 ^ z.re ≤ a ^ (1 - z.re) * b ^ z.re
have apply : 0 ≤ b ^ z.re
Tactic: apply mul_le_mul_of_nonneg _ _ (Real.rpow_nonneg (sSupNormIm_nonneg f _) _)
-- Lean 4 proof step from Mathlib.Analysis.Complex.Hadamard (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
z : ℂ
a b : ℝ
hz : z ∈ verticalClosedStrip 0 1
hd : DiffContOnCl ℂ f (verticalStrip 0 1)
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
ha : ∀ z ∈ re ⁻¹' {0}, ‖f z‖ ≤ a
hb : ∀ z ∈ re ⁻¹' {1}, ‖f z‖ ≤ b
this : ‖interpStrip f z‖ ≤ sSupNormIm f 0 ^ (1 - z.re) * sSupNormIm f 1 ^ z.re
apply : 0 ≤ b ^ z.re
⊢ sSupNormIm f 0 ^ (1 - z.re) * sSupNormIm f 1 ^ z.re ≤ a ^ (1 - z.re) * b ^ z.re
have apply₁ : sSupNormIm f 0 ^ (1 - z.re) ≤ a ^ (1 - z.re)
Tactic: apply mul_le_mul_of_nonneg _ _ (Real.rpow_nonneg (sSupNormIm_nonneg f _) _)
-- Lean 4 proof step from Mathlib.Analysis.Complex.Hadamard (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
z : ℂ
a b : ℝ
hz : z ∈ verticalClosedStrip 0 1
hd : DiffContOnCl ℂ f (verticalStrip 0 1)
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
ha : ∀ z ∈ re ⁻¹' {0}, ‖f z‖ ≤ a
hb : ∀ z ∈ re ⁻¹' {1}, ‖f z‖ ≤ b
this : ‖interpStrip f z‖ ≤ sSupNormIm f 0 ^ (1 - z.re) * sSupNormIm f 1 ^ z.re
apply : 0 ≤ b ^ z.re
apply₁ : sSupNormIm f 0 ^ (1 - z.re) ≤ a ^ (1 - z.re)
⊢ sSupNormIm f 0 ^ (1 - z.re) * sSupNormIm f 1 ^ z.re ≤ a ^ (1 - z.re) * b ^ z.re
have apply₂ : sSupNormIm f 1 ^ z.re ≤ b ^ z.re
Tactic: apply mul_le_mul_of_nonneg _ _ (Real.rpow_nonneg (sSupNormIm_nonneg f _) _)
-- Lean 4 proof step from Mathlib.Analysis.Complex.Hadamard (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
z : ℂ
a b : ℝ
hz : z ∈ verticalClosedStrip 0 1
hd : DiffContOnCl ℂ f (verticalStrip 0 1)
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
ha : ∀ z ∈ re ⁻¹' {0}, ‖f z‖ ≤ a
hb : ∀ z ∈ re ⁻¹' {1}, ‖f z‖ ≤ b
this : ‖interpStrip f z‖ ≤ sSupNormIm f 0 ^ (1 - z.re) * sSupNormIm f 1 ^ z.re
⊢ 0 ≤ b ^ z.re
have apply : 0 ≤ b
Tactic: apply (Real.rpow_nonneg _ _)
-- Lean 4 proof step from Mathlib.Analysis.Complex.Hadamard (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
z : ℂ
a b : ℝ
hz : z ∈ verticalClosedStrip 0 1
hd : DiffContOnCl ℂ f (verticalStrip 0 1)
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
ha : ∀ z ∈ re ⁻¹' {0}, ‖f z‖ ≤ a
hb : ∀ z ∈ re ⁻¹' {1}, ‖f z‖ ≤ b
this : ‖interpStrip f z‖ ≤ sSupNormIm f 0 ^ (1 - z.re) * sSupNormIm f 1 ^ z.re
⊢ 0 ≤ b
have hb₁ : 1 ∈ re ⁻¹' {1} → ‖f 1‖ ≤ b
Tactic: specialize hb 1
Cleared hypotheses: hb
-- Lean 4 proof step from Mathlib.Analysis.Complex.Hadamard (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
z : ℂ
a b : ℝ
hz : z ∈ verticalClosedStrip 0 1
hd : DiffContOnCl ℂ f (verticalStrip 0 1)
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
ha : ∀ z ∈ re ⁻¹' {0}, ‖f z‖ ≤ a
this : ‖interpStrip f z‖ ≤ sSupNormIm f 0 ^ (1 - z.re) * sSupNormIm f 1 ^ z.re
hb : 1 ∈ re ⁻¹' {1} → ‖f 1‖ ≤ b
⊢ 0 ≤ b
have hb₁ : ‖f 1‖ ≤ b
Tactic: simp only [mem_preimage, one_re, mem_singleton_iff, forall_true_left] at hb
Cleared hypotheses: hb
-- Lean 4 proof step from Mathlib.Analysis.Complex.Hadamard (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
z : ℂ
a b : ℝ
hz : z ∈ verticalClosedStrip 0 1
hd : DiffContOnCl ℂ f (verticalStrip 0 1)
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
ha : ∀ z ∈ re ⁻¹' {0}, ‖f z‖ ≤ a
hb : ∀ z ∈ re ⁻¹' {1}, ‖f z‖ ≤ b
this : ‖interpStrip f z‖ ≤ sSupNormIm f 0 ^ (1 - z.re) * sSupNormIm f 1 ^ z.re
⊢ sSupNormIm f 0 ^ (1 - z.re) ≤ a ^ (1 - z.re)
have h : 0 ≤ sSupNormIm f 0
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Complex.Hadamard (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
z : ℂ
a b : ℝ
hz : z ∈ verticalClosedStrip 0 1
hd : DiffContOnCl ℂ f (verticalStrip 0 1)
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
ha : ∀ z ∈ re ⁻¹' {0}, ‖f z‖ ≤ a
hb : ∀ z ∈ re ⁻¹' {1}, ‖f z‖ ≤ b
this : ‖interpStrip f z‖ ≤ sSupNormIm f 0 ^ (1 - z.re) * sSupNormIm f 1 ^ z.re
h : 0 ≤ sSupNormIm f 0
⊢ sSupNormIm f 0 ^ (1 - z.re) ≤ a ^ (1 - z.re)
have h₂ : 0 ≤ 1 - z.re
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Complex.Hadamard (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
z : ℂ
a b : ℝ
hz : z ∈ verticalClosedStrip 0 1
hd : DiffContOnCl ℂ f (verticalStrip 0 1)
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
ha : ∀ z ∈ re ⁻¹' {0}, ‖f z‖ ≤ a
hb : ∀ z ∈ re ⁻¹' {1}, ‖f z‖ ≤ b
this : ‖interpStrip f z‖ ≤ sSupNormIm f 0 ^ (1 - z.re) * sSupNormIm f 1 ^ z.re
h : 0 ≤ sSupNormIm f 0
h₂ : 0 ≤ 1 - z.re
⊢ sSupNormIm f 0 ^ (1 - z.re) ≤ a ^ (1 - z.re)
have h₁ : sSupNormIm f 0 ≤ a
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Complex.Hadamard (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
z : ℂ
a b : ℝ
hz : z ∈ verticalClosedStrip 0 1
hd : DiffContOnCl ℂ f (verticalStrip 0 1)
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
ha : ∀ z ∈ re ⁻¹' {0}, ‖f z‖ ≤ a
hb : ∀ z ∈ re ⁻¹' {1}, ‖f z‖ ≤ b
this : ‖interpStrip f z‖ ≤ sSupNormIm f 0 ^ (1 - z.re) * sSupNormIm f 1 ^ z.re
⊢ sSup (norm ∘ f '' re ⁻¹' {0}) ≤ a
have h₁ : ∀ b ∈ norm ∘ f '' re ⁻¹' {0}, b ≤ a
Tactic: apply csSup_le _
-- Lean 4 proof step from Mathlib.Analysis.Complex.Hadamard (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
z : ℂ
a b : ℝ
hz : z ∈ verticalClosedStrip 0 1
hd : DiffContOnCl ℂ f (verticalStrip 0 1)
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
ha : ∀ z ∈ re ⁻¹' {0}, ‖f z‖ ≤ a
hb : ∀ z ∈ re ⁻¹' {1}, ‖f z‖ ≤ b
this : ‖interpStrip f z‖ ≤ sSupNormIm f 0 ^ (1 - z.re) * sSupNormIm f 1 ^ z.re
h₁ : ∀ b ∈ norm ∘ f '' re ⁻¹' {0}, b ≤ a
⊢ sSup (norm ∘ f '' re ⁻¹' {0}) ≤ a
have apply : (norm ∘ f '' re ⁻¹' {0}).Nonempty
Tactic: apply csSup_le _
-- Lean 4 proof step from Mathlib.Analysis.Complex.Hadamard (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
z : ℂ
a b : ℝ
hz : z ∈ verticalClosedStrip 0 1
hd : DiffContOnCl ℂ f (verticalStrip 0 1)
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
ha : ∀ z ∈ re ⁻¹' {0}, ‖f z‖ ≤ a
hb : ∀ z ∈ re ⁻¹' {1}, ‖f z‖ ≤ b
this : ‖interpStrip f z‖ ≤ sSupNormIm f 0 ^ (1 - z.re) * sSupNormIm f 1 ^ z.re
⊢ (norm ∘ f '' re ⁻¹' {0}).Nonempty
have h : 0 ∈ re ⁻¹' {0} ∧ (norm ∘ f) 0 = ‖f 0‖
Tactic: use ‖(f 0)‖, 0
-- Lean 4 proof step from Mathlib.Analysis.Complex.Hadamard (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
z : ℂ
a b : ℝ
hz : z ∈ verticalClosedStrip 0 1
hd : DiffContOnCl ℂ f (verticalStrip 0 1)
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
ha : ∀ z ∈ re ⁻¹' {0}, ‖f z‖ ≤ a
hb : ∀ z ∈ re ⁻¹' {1}, ‖f z‖ ≤ b
this : ‖interpStrip f z‖ ≤ sSupNormIm f 0 ^ (1 - z.re) * sSupNormIm f 1 ^ z.re
⊢ sSupNormIm f 1 ^ z.re ≤ b ^ z.re
have apply : sSupNormIm f 1 ≤ b
Tactic: apply Real.rpow_le_rpow (sSupNormIm_nonneg f _) _ hz.1
-- Lean 4 proof step from Mathlib.Analysis.Complex.Hadamard (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
z : ℂ
a b : ℝ
hz : z ∈ verticalClosedStrip 0 1
hd : DiffContOnCl ℂ f (verticalStrip 0 1)
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
ha : ∀ z ∈ re ⁻¹' {0}, ‖f z‖ ≤ a
hb : ∀ z ∈ re ⁻¹' {1}, ‖f z‖ ≤ b
this : ‖interpStrip f z‖ ≤ sSupNormIm f 0 ^ (1 - z.re) * sSupNormIm f 1 ^ z.re
⊢ sSup (norm ∘ f '' re ⁻¹' {1}) ≤ b
have apply : ∀ b_1 ∈ norm ∘ f '' re ⁻¹' {1}, b_1 ≤ b
Tactic: apply csSup_le _
-- Lean 4 proof step from Mathlib.Analysis.Complex.Hadamard (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
z : ℂ
a b : ℝ
hz : z ∈ verticalClosedStrip 0 1
hd : DiffContOnCl ℂ f (verticalStrip 0 1)
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
ha : ∀ z ∈ re ⁻¹' {0}, ‖f z‖ ≤ a
hb : ∀ z ∈ re ⁻¹' {1}, ‖f z‖ ≤ b
this : ‖interpStrip f z‖ ≤ sSupNormIm f 0 ^ (1 - z.re) * sSupNormIm f 1 ^ z.re
apply : ∀ b_1 ∈ norm ∘ f '' re ⁻¹' {1}, b_1 ≤ b
⊢ sSup (norm ∘ f '' re ⁻¹' {1}) ≤ b
have apply₁ : (norm ∘ f '' re ⁻¹' {1}).Nonempty
Tactic: apply csSup_le _
-- Lean 4 proof step from Mathlib.Analysis.Complex.Hadamard (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
z : ℂ
a b : ℝ
hz : z ∈ verticalClosedStrip 0 1
hd : DiffContOnCl ℂ f (verticalStrip 0 1)
hB : BddAbove (norm ∘ f '' verticalClosedStrip 0 1)
ha : ∀ z ∈ re ⁻¹' {0}, ‖f z‖ ≤ a
hb : ∀ z ∈ re ⁻¹' {1}, ‖f z‖ ≤ b
this : ‖interpStrip f z‖ ≤ sSupNormIm f 0 ^ (1 - z.re) * sSupNormIm f 1 ^ z.re
⊢ (norm ∘ f '' re ⁻¹' {1}).Nonempty
have h : 1 ∈ re ⁻¹' {1} ∧ (norm ∘ f) 1 = ‖f 1‖
Tactic: use ‖(f 1)‖, 1
-- Lean 4 proof step from Mathlib.Analysis.Complex.Hadamard (hypothesis)
Goal:
l u : ℝ
hul : l < u
z : ℂ
hz : z ∈ verticalStrip 0 1
⊢ (↑l : ℂ) + z * ((↑u : ℂ) - (↑l : ℂ)) ∈ verticalStrip l u
have hz₁ : 0 < z.re ∧ z.re < 1
Tactic: simp only [verticalStrip, mem_preimage, mem_Ioo] at hz
Cleared hypotheses: hz
-- Lean 4 proof step from Mathlib.Analysis.Complex.Hadamard (goal)
Goal:
l u : ℝ
hul : l < u
z : ℂ
hz : 0 < z.re ∧ z.re < 1
⊢ (↑l : ℂ) + z * ((↑u : ℂ) - (↑l : ℂ)) ∈ verticalStrip l u
have simp : 0 < z.re * (u - l) ∧ l + z.re * (u - l) < u
Tactic: simp only [verticalStrip, mem_preimage, add_re, ofReal_re, mul_re, sub_re, sub_im, ofReal_im,
    sub_self, mul_zero, sub_zero, mem_Ioo, lt_add_iff_pos_right]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Hadamard (hypothesis)
Goal:
l u : ℝ
hul : l < u
z : ℂ
hz : 0 < z.re ∧ z.re < 1
⊢ 0 < z.re * (u - l) ∧ l + z.re * (u - l) < u
have hz₁ : 0 < z.re
Tactic: obtain ⟨hz₁, hz₂⟩ := hz
Cleared hypotheses: hz
-- Lean 4 proof step from Mathlib.Analysis.Complex.Hadamard (hypothesis)
Goal:
l u : ℝ
hul : l < u
z : ℂ
hz : 0 < z.re ∧ z.re < 1
hz₁ : 0 < z.re
⊢ 0 < z.re * (u - l) ∧ l + z.re * (u - l) < u
have hz₂ : z.re < 1
Tactic: obtain ⟨hz₁, hz₂⟩ := hz
Cleared hypotheses: hz
-- Lean 4 proof step from Mathlib.Analysis.Complex.Hadamard (goal)
Goal:
l u : ℝ
hul : l < u
z : ℂ
hz₁ : 0 < z.re
hz₂ : z.re < 1
⊢ 0 < z.re * (u - l) ∧ l + z.re * (u - l) < u
have simp : l + z.re * (u - l) < u
Tactic: simp only [hz₁, mul_pos_iff_of_pos_left, sub_pos, hul, true_and]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Hadamard (goal)
Goal:
l u : ℝ
hul : l < u
z : ℂ
hz₁ : 0 < z.re
hz₂ : z.re < 1
⊢ l + z.re * (u - l) < u
have rw : z.re * (u - l) < u - l
Tactic: rw [add_comm, ← sub_lt_sub_iff_right l, add_sub_assoc, sub_self, add_zero]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Hadamard (goal)
Goal:
l u : ℝ
hul : l < u
z : ℂ
hz₁ : 0 < z.re
hz₂ : z.re < 1
⊢ z.re * (u - l) < u - l
have nth_rewrite : z.re * (u - l) < 1 * (u - l)
Tactic: nth_rewrite 2 [← one_mul (u - l)]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Hadamard (goal)
Goal:
l u : ℝ
hul : l < u
z : ℂ
hz₁ : 0 < z.re
hz₂ : z.re < 1
⊢ z.re * (u - l) < 1 * (u - l)
have ha : 0 < u - l
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Complex.Hadamard (goal)
Goal:
z : ℂ
l u : ℝ
hul : l < u
hz : z ∈ verticalClosedStrip l u
⊢ z / ((↑u : ℂ) - (↑l : ℂ)) - (↑l : ℂ) / ((↑u : ℂ) - (↑l : ℂ)) ∈ verticalClosedStrip 0 1
have simp : HDiv.hDiv (β := ℝ) (l * (u - l)) ((normSq : (a : ℂ) → ℝ) ((↑u : ℂ) - (↑l : ℂ)) : ℝ) ≤
    HDiv.hDiv (β := ℝ) (z.re * (u - l)) ((normSq : (a : ℂ) → ℝ) ((↑u : ℂ) - (↑l : ℂ)) : ℝ) ∧
  HDiv.hDiv (β := ℝ) (z.re * (u - l)) ((normSq : (a : ℂ) → ℝ) ((↑u : ℂ) - (↑l : ℂ)) : ℝ) ≤
    1 + HDiv.hDiv (β := ℝ) (l * (u - l)) ((normSq : (a : ℂ) → ℝ) ((↑u : ℂ) - (↑l : ℂ)) : ℝ)
Tactic: simp only [verticalClosedStrip, Complex.div_re, mem_preimage, sub_re, mem_Icc,
    sub_nonneg, tsub_le_iff_right, ofReal_re, ofReal_im, sub_im, sub_self, mul_zero, zero_div,
    add_zero]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Hadamard (goal)
Goal:
z : ℂ
l u : ℝ
hul : l < u
hz : z ∈ re ⁻¹' Icc l u
⊢ HDiv.hDiv (β := ℝ) (l * (u - l)) ((normSq : (a : ℂ) → ℝ) ((↑u : ℂ) - (↑l : ℂ)) : ℝ) ≤
      HDiv.hDiv (β := ℝ) (z.re * (u - l)) ((normSq : (a : ℂ) → ℝ) ((↑u : ℂ) - (↑l : ℂ)) : ℝ) ∧
    HDiv.hDiv (β := ℝ) (z.re * (u - l)) ((normSq : (a : ℂ) → ℝ) ((↑u : ℂ) - (↑l : ℂ)) : ℝ) ≤
      1 + HDiv.hDiv (β := ℝ) (l * (u - l)) ((normSq : (a : ℂ) → ℝ) ((↑u : ℂ) - (↑l : ℂ)) : ℝ)
have norm_cast : HDiv.hDiv (β := ℝ) (l * (u - l)) ((normSq : (a : ℂ) → ℝ) (↑(u - l) : ℂ) : ℝ) ≤
    HDiv.hDiv (β := ℝ) (z.re * (u - l)) ((normSq : (a : ℂ) → ℝ) (↑(u - l) : ℂ) : ℝ) ∧
  HDiv.hDiv (β := ℝ) (z.re * (u - l)) ((normSq : (a : ℂ) → ℝ) (↑(u - l) : ℂ) : ℝ) ≤
    1 + HDiv.hDiv (β := ℝ) (l * (u - l)) ((normSq : (a : ℂ) → ℝ) (↑(u - l) : ℂ) : ℝ)
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Analysis.Complex.Hadamard (goal)
Goal:
z : ℂ
l u : ℝ
hul : l < u
hz : z ∈ re ⁻¹' Icc l u
⊢ u - l ≠ 0
have linarith : u - l = 0 → l - u + (u - l - 0) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.Complex.Hadamard (goal)
Goal:
z : ℂ
l u : ℝ
hul : l < u
hz : z ∈ re ⁻¹' Icc l u
⊢ HDiv.hDiv (β := ℝ) (l * (u - l)) ((normSq : (a : ℂ) → ℝ) (↑(u - l) : ℂ) : ℝ) ≤
      HDiv.hDiv (β := ℝ) (z.re * (u - l)) ((normSq : (a : ℂ) → ℝ) (↑(u - l) : ℂ) : ℝ) ∧
    HDiv.hDiv (β := ℝ) (z.re * (u - l)) ((normSq : (a : ℂ) → ℝ) (↑(u - l) : ℂ) : ℝ) ≤
      1 + HDiv.hDiv (β := ℝ) (l * (u - l)) ((normSq : (a : ℂ) → ℝ) (↑(u - l) : ℂ) : ℝ)
have simp_rw : l / (u - l) ≤ z.re / (u - l) ∧ z.re / (u - l) ≤ 1 + l / (u - l)
Tactic: simp_rw [Complex.normSq_ofReal, mul_div_assoc, div_mul_eq_div_div_swap,
    div_self (by linarith : u - l ≠ 0), ← div_eq_mul_one_div]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Hadamard (goal)
Goal:
z : ℂ
l u : ℝ
hul : l < u
hz : z ∈ re ⁻¹' Icc l u
⊢ l / (u - l) ≤ z.re / (u - l) ∧ z.re / (u - l) ≤ 1 + l / (u - l)
have left : l / (u - l) ≤ z.re / (u - l)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.Complex.Hadamard (goal)
Goal:
z : ℂ
l u : ℝ
hul : l < u
hz : z ∈ re ⁻¹' Icc l u
left : l / (u - l) ≤ z.re / (u - l)
⊢ l / (u - l) ≤ z.re / (u - l) ∧ z.re / (u - l) ≤ 1 + l / (u - l)
have right : z.re / (u - l) ≤ 1 + l / (u - l)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.Complex.Hadamard (goal)
Goal:
z : ℂ
l u : ℝ
hul : l < u
hz : z ∈ re ⁻¹' Icc l u
⊢ l / (u - l) ≤ z.re / (u - l)
have left : l ≤ z.re
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Complex.Hadamard (goal)
Goal:
z : ℂ
l u : ℝ
hul : l < u
hz : z ∈ re ⁻¹' Icc l u
⊢ z.re / (u - l) ≤ 1 + l / (u - l)
have right : z.re ≤ u
Tactic: rw [← sub_le_sub_iff_right (l / (u - l)), add_sub_assoc, sub_self, add_zero, div_sub_div_same,
      div_le_one (by simp [hul]), sub_le_sub_iff_right l]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Hadamard (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
l u : ℝ
hul : l < u
hd : DiffContOnCl ℂ f (verticalStrip l u)
⊢ DiffContOnCl ℂ (scale f l u) (verticalStrip 0 1)
have unfold : DiffContOnCl.{0, 0, u_1} ℂ (F := E) (fun (z : ℂ) ↦ f ((↑l : ℂ) + z • ((↑u : ℂ) - (↑l : ℂ)))) (verticalStrip 0 1)
Tactic: unfold scale
-- Lean 4 proof step from Mathlib.Analysis.Complex.Hadamard (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
l u : ℝ
hul : l < u
hd : DiffContOnCl ℂ f (verticalStrip l u)
⊢ DiffContOnCl.{0, 0, u_1} ℂ (F := E) (fun (z : ℂ) ↦ f ((↑l : ℂ) + z • ((↑u : ℂ) - (↑l : ℂ)))) (verticalStrip 0 1)
have hg : DiffContOnCl ℂ (F := ℂ) (fun (z : ℂ) ↦ (↑l : ℂ) + z • ((↑u : ℂ) - (↑l : ℂ))) (verticalStrip 0 1)
Tactic: apply DiffContOnCl.comp (s := verticalStrip l u) hd
-- Lean 4 proof step from Mathlib.Analysis.Complex.Hadamard (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
l u : ℝ
hul : l < u
hd : DiffContOnCl ℂ f (verticalStrip l u)
hg : DiffContOnCl ℂ (F := ℂ) (fun (z : ℂ) ↦ (↑l : ℂ) + z • ((↑u : ℂ) - (↑l : ℂ))) (verticalStrip 0 1)
⊢ DiffContOnCl.{0, 0, u_1} ℂ (F := E) (fun (z : ℂ) ↦ f ((↑l : ℂ) + z • ((↑u : ℂ) - (↑l : ℂ)))) (verticalStrip 0 1)
have h : MapsTo (fun (z : ℂ) ↦ (↑l : ℂ) + z • ((↑u : ℂ) - (↑l : ℂ))) (verticalStrip 0 1) (verticalStrip l u)
Tactic: apply DiffContOnCl.comp (s := verticalStrip l u) hd
-- Lean 4 proof step from Mathlib.Analysis.Complex.Hadamard (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
l u : ℝ
hul : l < u
hd : DiffContOnCl ℂ f (verticalStrip l u)
⊢ DiffContOnCl ℂ (F := ℂ) (fun (z : ℂ) ↦ (↑l : ℂ) + z • ((↑u : ℂ) - (↑l : ℂ))) (verticalStrip 0 1)
have hg : DiffContOnCl ℂ (F := ℂ) (fun (x : ℂ) ↦ x • ((↑u : ℂ) - (↑l : ℂ))) (verticalStrip 0 1)
Tactic: apply DiffContOnCl.const_add
-- Lean 4 proof step from Mathlib.Analysis.Complex.Hadamard (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
l u : ℝ
hul : l < u
hd : DiffContOnCl ℂ f (verticalStrip l u)
⊢ DiffContOnCl ℂ (F := ℂ) (fun (x : ℂ) ↦ x • ((↑u : ℂ) - (↑l : ℂ))) (verticalStrip 0 1)
have hg : DiffContOnCl ℂ (F := ℂ) (fun (x : ℂ) ↦ x) (verticalStrip 0 1)
Tactic: apply DiffContOnCl.smul_const
-- Lean 4 proof step from Mathlib.Analysis.Complex.Hadamard (goal)
Goal:
l u : ℝ
hul : l < u
z : ℂ
⊢ (↑u : ℂ) - (↑l : ℂ) ≠ 0
have norm_cast : ¬u - l = 0
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Analysis.Complex.Hadamard (goal)
Goal:
l u : ℝ
hul : l < u
z : ℂ
⊢ ¬u - l = 0
have linarith : u - l = 0 → l - u + (u - l - 0) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.Complex.Hadamard (goal)
Goal:
l u : ℝ
hul : l < u
z : ℂ
⊢ (↑l : ℂ) + (z / ((↑u : ℂ) - (↑l : ℂ)) - (↑l : ℂ) / ((↑u : ℂ) - (↑l : ℂ))) * ((↑u : ℂ) - (↑l : ℂ)) = z
have rw : (↑l : ℂ) + (1 * z - 1 * (↑l : ℂ)) = z
Tactic: rw [sub_mul, div_mul_comm, div_self (by norm_cast; linarith),
    div_mul_comm, div_self (by norm_cast; linarith)]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Hadamard (goal)
Goal:
l u : ℝ
hul : l < u
z : ℂ
⊢ (z / ((↑u : ℂ) - (↑l : ℂ))).re - ((↑l : ℂ) / ((↑u : ℂ) - (↑l : ℂ))).re = (z.re - l) / (u - l)
have norm_cast : (z / (↑(u - l) : ℂ)).re - l / (u - l) = (z.re - l) / (u - l)
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Analysis.Complex.Hadamard (goal)
Goal:
l u : ℝ
hul : l < u
z : ℂ
⊢ (z / (↑(u - l) : ℂ)).re - l / (u - l) = (z.re - l) / (u - l)
have rw : z.re / (u - l) + z.im * 0 / ((u - l) * (u - l)) - l / (u - l) = (z.re - l) / (u - l)
Tactic: rw [Complex.div_re, Complex.normSq_ofReal, Complex.ofReal_re, Complex.ofReal_im, mul_div_assoc,
    div_mul_eq_div_div_swap, div_self (by norm_cast; linarith),
    ← div_eq_mul_one_div]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Hadamard (goal)
Goal:
l u : ℝ
hul : l < u
z : ℂ
⊢ z.re / (u - l) + z.im * 0 / ((u - l) * (u - l)) - l / (u - l) = (z.re - l) / (u - l)
have simp : z.re / (u - l) - l / (u - l) = (z.re - l) / (u - l)
Tactic: simp only [mul_zero, zero_div, add_zero]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Hadamard (goal)
Goal:
l u : ℝ
hul : l < u
z : ℂ
⊢ z.re / (u - l) - l / (u - l) = (z.re - l) / (u - l)
have rw : z.re / (u - l) - l / (u - l) = z.re / (u - l) - l / (u - l)
Tactic: rw [← div_sub_div_same]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Hadamard (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
l u : ℝ
hul : l < u
f : ℂ → E
z : ℂ
hz : z ∈ verticalClosedStrip l u
hd : DiffContOnCl ℂ f (verticalStrip l u)
hB : BddAbove (norm ∘ f '' verticalClosedStrip l u)
⊢ ‖f z‖ ≤ ‖interpStrip' f l u z‖
have hgoal : ‖scale f l u (z / ((↑u : ℂ) - (↑l : ℂ)) - (↑l : ℂ) / ((↑u : ℂ) - (↑l : ℂ)))‖ ≤
  ‖interpStrip (scale f l u) (z / ((↑u : ℂ) - (↑l : ℂ)) - (↑l : ℂ) / ((↑u : ℂ) - (↑l : ℂ)))‖
Tactic: have hgoal := norm_le_interpStrip_of_mem_verticalClosedStrip₀₁ (scale f l u)
    (mem_verticalClosedStrip_of_scale_id_mem_verticalClosedStrip hul hz)
    (scale_diffContOnCl hul hd) (scale_bddAbove hul hB)
-- Lean 4 proof step from Mathlib.Analysis.Complex.Hadamard (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
z : ℂ
a b l u : ℝ
hul : l < u
hz : z ∈ verticalClosedStrip l u
hd : DiffContOnCl ℂ f (verticalStrip l u)
hB : BddAbove (norm ∘ f '' verticalClosedStrip l u)
ha : ∀ z ∈ re ⁻¹' {l}, ‖f z‖ ≤ a
hb : ∀ z ∈ re ⁻¹' {u}, ‖f z‖ ≤ b
⊢ ‖f z‖ ≤ a ^ (1 - (z.re - l) / (u - l)) * b ^ ((z.re - l) / (u - l))
have hgoal : ‖scale f l u (z / ((↑u : ℂ) - (↑l : ℂ)) - (↑l : ℂ) / ((↑u : ℂ) - (↑l : ℂ)))‖ ≤
  a ^ (1 - (z / ((↑u : ℂ) - (↑l : ℂ)) - (↑l : ℂ) / ((↑u : ℂ) - (↑l : ℂ))).re) *
    b ^ (z / ((↑u : ℂ) - (↑l : ℂ)) - (↑l : ℂ) / ((↑u : ℂ) - (↑l : ℂ))).re
Tactic: have hgoal := norm_le_interp_of_mem_verticalClosedStrip₀₁' (scale f l u)
    (mem_verticalClosedStrip_of_scale_id_mem_verticalClosedStrip hul hz) (scale_diffContOnCl hul hd)
    (scale_bddAbove hul hB) (scale_bound_left ha) (scale_bound_right hb)
-- Lean 4 proof step from Mathlib.Analysis.Complex.Harmonic.Analytic (goal)
Goal:
f : ℂ → ℝ
x : ℂ
hf : HarmonicAt f x
⊢ (fun (z : ℂ) ↦ (↑((fderiv ℝ f z : (a : ℂ) → ℝ) 1) : ℂ) - I * (↑((fderiv ℝ f z : (a : ℂ) → ℝ) I) : ℂ)) =
    (Function.comp (β := ℝ) (⇑ofRealCLM : (a : ℝ) → ℂ) fun (x : ℂ) ↦ (fderiv ℝ f x : (a : ℂ) → ℝ) 1) -
      HSMul.hSMul (β := ℂ → ℂ) I
        (Function.comp (β := ℝ) (⇑ofRealCLM : (a : ℝ) → ℂ) fun (x : ℂ) ↦ (fderiv ℝ f x : (a : ℂ) → ℝ) I)
have h : ∀ (x : ℂ),
  (↑((fderiv ℝ f x : (a : ℂ) → ℝ) 1) : ℂ) - I * (↑((fderiv ℝ f x : (a : ℂ) → ℝ) I) : ℂ) =
    HSub.hSub (α := ℂ → ℂ)
      (Function.comp (β := ℝ) (⇑ofRealCLM : (a : ℝ) → ℂ) fun (x : ℂ) ↦ (fderiv ℝ f x : (a : ℂ) → ℝ) 1)
      (HSMul.hSMul (β := ℂ → ℂ) I
        (Function.comp (β := ℝ) (⇑ofRealCLM : (a : ℝ) → ℂ) fun (x : ℂ) ↦ (fderiv ℝ f x : (a : ℂ) → ℝ) I))
      x
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.Complex.Harmonic.Analytic (hypothesis)
Goal:
f : ℂ → ℝ
x : ℂ
hf : HarmonicAt f x
⊢ DifferentiableAt ℂ (F := ℂ)
    (fun (z : ℂ) ↦ (↑((fderiv ℝ f z : (a : ℂ) → ℝ) 1) : ℂ) - I * (↑((fderiv ℝ f z : (a : ℂ) → ℝ) I) : ℂ)) x
have this : (fun (z : ℂ) ↦ (↑((fderiv ℝ f z : (a : ℂ) → ℝ) 1) : ℂ) - I * (↑((fderiv ℝ f z : (a : ℂ) → ℝ) I) : ℂ)) =
  (Function.comp (β := ℝ) (⇑ofRealCLM : (a : ℝ) → ℂ) fun (x : ℂ) ↦ (fderiv ℝ f x : (a : ℂ) → ℝ) 1) -
    HSMul.hSMul (β := ℂ → ℂ) I
      (Function.comp (β := ℝ) (⇑ofRealCLM : (a : ℝ) → ℂ) fun (x : ℂ) ↦ (fderiv ℝ f x : (a : ℂ) → ℝ) I)
Tactic: have : (fun z ↦ fderiv ℝ f z 1 - I * fderiv ℝ f z I) =
      (ofRealCLM ∘ (fderiv ℝ f · 1) - I • ofRealCLM ∘ (fderiv ℝ f · I)) := by
    ext; simp
-- Lean 4 proof step from Mathlib.Analysis.Complex.Harmonic.Analytic (hypothesis)
Goal:
f : ℂ → ℝ
x : ℂ
hf : HarmonicAt f x
this :
  (fun (z : ℂ) ↦ (↑((fderiv ℝ f z : (a : ℂ) → ℝ) 1) : ℂ) - I * (↑((fderiv ℝ f z : (a : ℂ) → ℝ) I) : ℂ)) =
    (Function.comp (β := ℝ) (⇑ofRealCLM : (a : ℝ) → ℂ) fun (x : ℂ) ↦ (fderiv ℝ f x : (a : ℂ) → ℝ) 1) -
      HSMul.hSMul (β := ℂ → ℂ) I
        (Function.comp (β := ℝ) (⇑ofRealCLM : (a : ℝ) → ℂ) fun (x : ℂ) ↦ (fderiv ℝ f x : (a : ℂ) → ℝ) I)
⊢ DifferentiableAt ℂ
    ((Function.comp (β := ℝ) (⇑ofRealCLM : (a : ℝ) → ℂ) fun (x : ℂ) ↦ (fderiv ℝ f x : (a : ℂ) → ℝ) 1) -
      HSMul.hSMul (β := ℂ → ℂ) I
        (Function.comp (β := ℝ) (⇑ofRealCLM : (a : ℝ) → ℂ) fun (x : ℂ) ↦ (fderiv ℝ f x : (a : ℂ) → ℝ) I))
    x
have h₁f : ContDiffAt ℝ 2 f x
Tactic: have h₁f := hf.1