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
f : ℂ → E
z : ℂ
hz : z ∈ verticalStrip 0 1
⊢ interpStrip f z = (↑(sSupNormIm f 0) : ℂ) ^ (1 - z) * (↑(sSupNormIm f 1) : ℂ) ^ z
have pos : ∀ (h : sSupNormIm f 0 = 0 ∨ sSupNormIm f 1 = 0),
  interpStrip f z = (↑(sSupNormIm f 0) : ℂ) ^ (1 - z) * (↑(sSupNormIm f 1) : ℂ) ^ z
Tactic: by_cases! h : sSupNormIm f 0 = 0 ∨ sSupNormIm f 1 = 0
-- Lean 4 proof step from Mathlib.Analysis.Complex.Hadamard (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℂ → E
z : ℂ
hz : z ∈ verticalStrip 0 1
pos :
  ∀ (h : sSupNormIm f 0 = 0 ∨ sSupNormIm f 1 = 0),
    interpStrip f z = (↑(sSupNormIm f 0) : ℂ) ^ (1 - z) * (↑(sSupNormIm f 1) : ℂ) ^ z
⊢ interpStrip f z = (↑(sSupNormIm f 0) : ℂ) ^ (1 - z) * (↑(sSupNormIm f 1) : ℂ) ^ z
have neg : ∀ (h : sSupNormIm f 0 ≠ 0 ∧ sSupNormIm f 1 ≠ 0),
  interpStrip f z = (↑(sSupNormIm f 0) : ℂ) ^ (1 - z) * (↑(sSupNormIm f 1) : ℂ) ^ z
Tactic: by_cases! h : sSupNormIm f 0 = 0 ∨ sSupNormIm f 1 = 0
-- Lean 4 proof step from Mathlib.Analysis.Complex.Hadamard (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℂ → E
z : ℂ
hz : z ∈ verticalStrip 0 1
h : sSupNormIm f 0 = 0 ∨ sSupNormIm f 1 = 0
⊢ interpStrip f z = (↑(sSupNormIm f 0) : ℂ) ^ (1 - z) * (↑(sSupNormIm f 1) : ℂ) ^ z
have pos : 0 = (↑(sSupNormIm f 0) : ℂ) ^ (1 - z) * (↑(sSupNormIm f 1) : ℂ) ^ z
Tactic: rw [interpStrip_eq_of_zero _ z h]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Hadamard (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℂ → E
z : ℂ
hz : z ∈ verticalStrip 0 1
h : sSupNormIm f 0 = 0 ∨ sSupNormIm f 1 = 0
⊢ 0 = (↑(sSupNormIm f 0) : ℂ) ^ (1 - z) * (↑(sSupNormIm f 1) : ℂ) ^ z
have pos : ∀ (h0 : sSupNormIm f 0 = 0), 0 = (↑(sSupNormIm f 0) : ℂ) ^ (1 - z) * (↑(sSupNormIm f 1) : ℂ) ^ z
Tactic: rcases h with h0 | h1
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.Complex.Hadamard (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℂ → E
z : ℂ
hz : z ∈ verticalStrip 0 1
h : sSupNormIm f 0 = 0 ∨ sSupNormIm f 1 = 0
pos : ∀ (h0 : sSupNormIm f 0 = 0), 0 = (↑(sSupNormIm f 0) : ℂ) ^ (1 - z) * (↑(sSupNormIm f 1) : ℂ) ^ z
⊢ 0 = (↑(sSupNormIm f 0) : ℂ) ^ (1 - z) * (↑(sSupNormIm f 1) : ℂ) ^ z
have pos₁ : ∀ (h1 : sSupNormIm f 1 = 0), 0 = (↑(sSupNormIm f 0) : ℂ) ^ (1 - z) * (↑(sSupNormIm f 1) : ℂ) ^ z
Tactic: rcases h with h0 | h1
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.Complex.Hadamard (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℂ → E
z : ℂ
hz : z ∈ verticalStrip 0 1
h0 : sSupNormIm f 0 = 0
⊢ 0 = (↑(sSupNormIm f 0) : ℂ) ^ (1 - z) * (↑(sSupNormIm f 1) : ℂ) ^ z
have pos : ¬1 - z = 0 ∨ sSupNormIm f 1 = 0 ∧ ¬z = 0
Tactic: simp only [h0, ofReal_zero, zero_eq_mul, cpow_eq_zero_iff, ne_eq, true_and, ofReal_eq_zero]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Hadamard (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℂ → E
z : ℂ
hz : z ∈ verticalStrip 0 1
h0 : sSupNormIm f 0 = 0
⊢ ¬1 - z = 0 ∨ sSupNormIm f 1 = 0 ∧ ¬z = 0
have pos : ¬1 - z = 0
Tactic: left
-- Lean 4 proof step from Mathlib.Analysis.Complex.Hadamard (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℂ → E
z : ℂ
hz : z ∈ verticalStrip 0 1
h0 : sSupNormIm f 0 = 0
⊢ ¬1 - z = 0
have pos : ¬z = 1
Tactic: rw [sub_eq_zero, eq_comm]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Hadamard (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℂ → E
z : ℂ
hz : z ∈ verticalStrip 0 1
h1 : sSupNormIm f 1 = 0
⊢ 0 = (↑(sSupNormIm f 0) : ℂ) ^ (1 - z) * (↑(sSupNormIm f 1) : ℂ) ^ z
have pos : sSupNormIm f 0 = 0 ∧ ¬1 - z = 0 ∨ ¬z = 0
Tactic: simp only [h1, ofReal_zero, zero_eq_mul, cpow_eq_zero_iff, ofReal_eq_zero, ne_eq, true_and]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Hadamard (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℂ → E
z : ℂ
hz : z ∈ verticalStrip 0 1
h1 : sSupNormIm f 1 = 0
⊢ sSupNormIm f 0 = 0 ∧ ¬1 - z = 0 ∨ ¬z = 0
have pos : ¬z = 0
Tactic: right
-- Lean 4 proof step from Mathlib.Analysis.Complex.Hadamard (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℂ → E
z : ℂ
hz : z ∈ verticalStrip 0 1
h1 : sSupNormIm f 1 = 0
⊢ ¬z = 0
have pos : ¬0 = z
Tactic: rw [eq_comm]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Hadamard (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℂ → E
z : ℂ
hz : z ∈ verticalStrip 0 1
h : sSupNormIm f 0 ≠ 0 ∧ sSupNormIm f 1 ≠ 0
⊢ interpStrip f z = (↑(sSupNormIm f 0) : ℂ) ^ (1 - z) * (↑(sSupNormIm f 1) : ℂ) ^ z
have h₁ : 0 < sSupNormIm f 0 ∧ 0 < sSupNormIm f 1
Tactic: replace h : (0 < sSupNormIm f 0) ∧ (0 < sSupNormIm f 1) :=
      ⟨(lt_of_le_of_ne (sSupNormIm_nonneg f 0) (ne_comm.mp h.1)),
        (lt_of_le_of_ne (sSupNormIm_nonneg f 1) (ne_comm.mp h.2))⟩
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.Complex.Hadamard (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℂ → E
⊢ DiffContOnCl ℂ (interpStrip f) (verticalStrip 0 1)
have pos : ∀ (h : sSupNormIm f 0 = 0 ∨ sSupNormIm f 1 = 0), DiffContOnCl ℂ (interpStrip f) (verticalStrip 0 1)
Tactic: by_cases! h : sSupNormIm f 0 = 0 ∨ sSupNormIm f 1 = 0
-- Lean 4 proof step from Mathlib.Analysis.Complex.Hadamard (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℂ → E
pos : ∀ (h : sSupNormIm f 0 = 0 ∨ sSupNormIm f 1 = 0), DiffContOnCl ℂ (interpStrip f) (verticalStrip 0 1)
⊢ DiffContOnCl ℂ (interpStrip f) (verticalStrip 0 1)
have neg : ∀ (h : sSupNormIm f 0 ≠ 0 ∧ sSupNormIm f 1 ≠ 0), DiffContOnCl ℂ (interpStrip f) (verticalStrip 0 1)
Tactic: by_cases! h : sSupNormIm f 0 = 0 ∨ sSupNormIm f 1 = 0
-- Lean 4 proof step from Mathlib.Analysis.Complex.Hadamard (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℂ → E
h : sSupNormIm f 0 = 0 ∨ sSupNormIm f 1 = 0
⊢ DiffContOnCl ℂ (F := ℂ) (fun (z : ℂ) ↦ interpStrip.{u_1} (E := E) (fun (a : ℂ) ↦ f a) z) fun (a : ℂ) ↦
    verticalStrip 0 1 a
have pos : DiffContOnCl ℂ (F := ℂ) (fun (z : ℂ) ↦ 0) fun (a : ℂ) ↦ verticalStrip 0 1 a
Tactic: simp_rw [interpStrip_eq_of_zero f _ h]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Hadamard (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℂ → E
h : sSupNormIm f 0 ≠ 0 ∧ sSupNormIm f 1 ≠ 0
⊢ DiffContOnCl ℂ (interpStrip f) (verticalStrip 0 1)
have h0 : sSupNormIm f 0 ≠ 0
Tactic: rcases h with ⟨h0, h1⟩
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.Complex.Hadamard (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℂ → E
h : sSupNormIm f 0 ≠ 0 ∧ sSupNormIm f 1 ≠ 0
h0 : sSupNormIm f 0 ≠ 0
⊢ DiffContOnCl ℂ (interpStrip f) (verticalStrip 0 1)
have h1 : sSupNormIm f 1 ≠ 0
Tactic: rcases h with ⟨h0, h1⟩
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.Complex.Hadamard (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℂ → E
h0 : sSupNormIm f 0 ≠ 0
h1 : sSupNormIm f 1 ≠ 0
⊢ DiffContOnCl ℂ (interpStrip f) (verticalStrip 0 1)
have h0₁ : 0 ≠ sSupNormIm f 0
Tactic: rw [ne_comm] at h0 h1
Cleared hypotheses: h0, h1
-- Lean 4 proof step from Mathlib.Analysis.Complex.Hadamard (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℂ → E
h0 : sSupNormIm f 0 ≠ 0
h1 : sSupNormIm f 1 ≠ 0
h0₁ : 0 ≠ sSupNormIm f 0
⊢ DiffContOnCl ℂ (interpStrip f) (verticalStrip 0 1)
have h1₁ : 0 ≠ sSupNormIm f 1
Tactic: rw [ne_comm] at h0 h1
Cleared hypotheses: h0, h1
-- Lean 4 proof step from Mathlib.Analysis.Complex.Hadamard (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℂ → E
h0 : 0 ≠ sSupNormIm f 0
h1 : 0 ≠ sSupNormIm f 1
⊢ DiffContOnCl ℂ (interpStrip f) (verticalStrip 0 1)
have neg : Differentiable ℂ (interpStrip f)
Tactic: apply Differentiable.diffContOnCl
-- Lean 4 proof step from Mathlib.Analysis.Complex.Hadamard (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℂ → E
h0 : 0 ≠ sSupNormIm f 0
h1 : 0 ≠ sSupNormIm f 1
z : ℂ
⊢ DifferentiableAt ℂ (F := ℂ) (fun (z : ℂ) ↦ interpStrip.{u_1} (E := E) (fun (a : ℂ) ↦ f a) z) z
have neg : DifferentiableAt ℂ (F := ℂ) (fun (z : ℂ) ↦ (↑(sSupNormIm f 0) : ℂ) ^ (1 - z) * (↑(sSupNormIm f 1) : ℂ) ^ z) z
Tactic: simp_rw [interpStrip_eq_of_pos f _ (lt_of_le_of_ne (sSupNormIm_nonneg f 0) h0)
      (lt_of_le_of_ne (sSupNormIm_nonneg f 1) h1)]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Hadamard (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℂ → E
h0 : 0 ≠ sSupNormIm f 0
h1 : 0 ≠ sSupNormIm f 1
z : ℂ
⊢ DifferentiableAt ℂ (F := ℂ) (fun (z : ℂ) ↦ (↑(sSupNormIm f 0) : ℂ) ^ (1 - z) * (↑(sSupNormIm f 1) : ℂ) ^ z) z
have neg : DifferentiableAt ℂ (F := ℂ) (fun (z : ℂ) ↦ (↑(sSupNormIm f 0) : ℂ) ^ (1 - z)) z
Tactic: refine DifferentiableAt.mul ?_ ?_
-- Lean 4 proof step from Mathlib.Analysis.Complex.Hadamard (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℂ → E
h0 : 0 ≠ sSupNormIm f 0
h1 : 0 ≠ sSupNormIm f 1
z : ℂ
neg : DifferentiableAt ℂ (F := ℂ) (fun (z : ℂ) ↦ (↑(sSupNormIm f 0) : ℂ) ^ (1 - z)) z
⊢ DifferentiableAt ℂ (F := ℂ) (fun (z : ℂ) ↦ (↑(sSupNormIm f 0) : ℂ) ^ (1 - z) * (↑(sSupNormIm f 1) : ℂ) ^ z) z
have neg₁ : DifferentiableAt ℂ (HPow.hPow (↑(sSupNormIm f 1) : ℂ)) z
Tactic: refine DifferentiableAt.mul ?_ ?_
-- Lean 4 proof step from Mathlib.Analysis.Complex.Hadamard (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℂ → E
h0 : 0 ≠ sSupNormIm f 0
h1 : 0 ≠ sSupNormIm f 1
z : ℂ
⊢ DifferentiableAt ℂ (F := ℂ) (fun (z : ℂ) ↦ (↑(sSupNormIm f 0) : ℂ) ^ (1 - z)) z
have apply : (↑(sSupNormIm f 0) : ℂ) ≠ 0 ∨ 1 - id z ≠ 0
Tactic: apply DifferentiableAt.const_cpow (DifferentiableAt.const_sub differentiableAt_id 1) _
-- Lean 4 proof step from Mathlib.Analysis.Complex.Hadamard (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℂ → E
h0 : 0 ≠ sSupNormIm f 0
h1 : 0 ≠ sSupNormIm f 1
z : ℂ
⊢ (↑(sSupNormIm f 0) : ℂ) ≠ 0 ∨ 1 - id z ≠ 0
have h : (↑(sSupNormIm f 0) : ℂ) ≠ 0
Tactic: left
-- Lean 4 proof step from Mathlib.Analysis.Complex.Hadamard (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℂ → E
h0 : 0 ≠ sSupNormIm f 0
h1 : 0 ≠ sSupNormIm f 1
z : ℂ
⊢ (↑(sSupNormIm f 0) : ℂ) ≠ 0
have h : ¬sSupNormIm f 0 = 0
Tactic: simp only [Ne, ofReal_eq_zero]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Hadamard (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℂ → E
h0 : 0 ≠ sSupNormIm f 0
h1 : 0 ≠ sSupNormIm f 1
z : ℂ
⊢ ¬sSupNormIm f 0 = 0
have h : ¬0 = sSupNormIm f 0
Tactic: rwa [eq_comm]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Hadamard (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℂ → E
h0 : 0 ≠ sSupNormIm f 0
h1 : 0 ≠ sSupNormIm f 1
z : ℂ
⊢ DifferentiableAt ℂ (HPow.hPow (↑(sSupNormIm f 1) : ℂ)) z
have neg : DifferentiableAt ℂ (F := ℂ) (fun (x : ℂ) ↦ x) z
Tactic: refine DifferentiableAt.const_cpow ?_ ?_
-- Lean 4 proof step from Mathlib.Analysis.Complex.Hadamard (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℂ → E
h0 : 0 ≠ sSupNormIm f 0
h1 : 0 ≠ sSupNormIm f 1
z : ℂ
neg : DifferentiableAt ℂ (F := ℂ) (fun (x : ℂ) ↦ x) z
⊢ DifferentiableAt ℂ (HPow.hPow (↑(sSupNormIm f 1) : ℂ)) z
have neg₁ : (↑(sSupNormIm f 1) : ℂ) ≠ 0 ∨ z ≠ 0
Tactic: refine DifferentiableAt.const_cpow ?_ ?_
-- Lean 4 proof step from Mathlib.Analysis.Complex.Hadamard (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℂ → E
h0 : 0 ≠ sSupNormIm f 0
h1 : 0 ≠ sSupNormIm f 1
z : ℂ
⊢ (↑(sSupNormIm f 1) : ℂ) ≠ 0 ∨ z ≠ 0
have neg : (↑(sSupNormIm f 1) : ℂ) ≠ 0
Tactic: left
-- Lean 4 proof step from Mathlib.Analysis.Complex.Hadamard (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℂ → E
h0 : 0 ≠ sSupNormIm f 0
h1 : 0 ≠ sSupNormIm f 1
z : ℂ
⊢ (↑(sSupNormIm f 1) : ℂ) ≠ 0
have neg : ¬sSupNormIm f 1 = 0
Tactic: simp only [Ne, ofReal_eq_zero]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Hadamard (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℂ → E
h0 : 0 ≠ sSupNormIm f 0
h1 : 0 ≠ sSupNormIm f 1
z : ℂ
⊢ ¬sSupNormIm f 1 = 0
have neg : ¬0 = sSupNormIm f 1
Tactic: rwa [eq_comm]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Hadamard (goal)
Goal:
l u : ℝ
hul : l < u
z : ℂ
hz : z ∈ verticalClosedStrip 0 1
⊢ (↑l : ℂ) + z * ((↑u : ℂ) - (↑l : ℂ)) ∈ verticalClosedStrip l u
have simp : ∀ (hz : 0 ≤ z.re ∧ z.re ≤ 1), l ≤ l + z.re * (u - l) ∧ l + z.re * (u - l) ≤ u
Tactic: simp only [verticalClosedStrip, mem_preimage, add_re, ofReal_re, mul_re, sub_re, sub_im,
    ofReal_im, sub_self, mul_zero, sub_zero, mem_Icc] 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 ≤ l + z.re * (u - l) ∧ l + z.re * (u - l) ≤ u
have left : l ≤ l + z.re * (u - l)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.Complex.Hadamard (goal)
Goal:
l u : ℝ
hul : l < u
z : ℂ
hz : 0 ≤ z.re ∧ z.re ≤ 1
left : l ≤ l + z.re * (u - l)
⊢ l ≤ l + z.re * (u - l) ∧ l + z.re * (u - l) ≤ u
have right : l + z.re * (u - l) ≤ u
Tactic: constructor
-- 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 ≤ l + z.re * (u - l)
have nlinarith : l + z.re * (u - l) < l → l + z.re * (u - l) - l + (0 - (l - u) * (0 - z.re)) = 0
Tactic: nlinarith [hz.1, hz.2, hul]
-- 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.re * (u - l) ≤ u
have nlinarith : u < l + z.re * (u - l) → u - (l + z.re * (u - l)) + (0 - (l - u) * (z.re - 1)) = 0
Tactic: nlinarith [hz.1, hz.2, hul]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Hadamard (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℂ → E
l u : ℝ
hul : l < u
hB : BddAbove (norm ∘ f '' verticalClosedStrip l u)
⊢ BddAbove (norm ∘ scale f l u '' verticalClosedStrip 0 1)
have refine : norm ∘ scale f l u '' verticalClosedStrip 0 1 ⊆ norm ∘ f '' verticalClosedStrip l u
Tactic: refine hB.mono ?_
-- Lean 4 proof step from Mathlib.Analysis.Complex.Hadamard (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℂ → E
l u a : ℝ
ha : ∀ z ∈ re ⁻¹' {l}, ‖f z‖ ≤ a
⊢ ∀ z ∈ re ⁻¹' {0}, ‖scale f l u z‖ ≤ a
have simp : ∀ (z : ℂ), z.re = 0 → ‖f ((↑l : ℂ) + z * ((↑u : ℂ) - (↑l : ℂ)))‖ ≤ a
Tactic: simp only [mem_preimage, mem_singleton_iff, scale, smul_eq_mul]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Hadamard (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℂ → E
l u b : ℝ
hb : ∀ z ∈ re ⁻¹' {u}, ‖f z‖ ≤ b
⊢ ∀ z ∈ re ⁻¹' {1}, ‖scale f l u z‖ ≤ b
have simp : ∀ (z : ℂ), z.re = 1 → ‖f ((↑l : ℂ) + z * ((↑u : ℂ) - (↑l : ℂ)))‖ ≤ b
Tactic: simp only [scale, mem_preimage, mem_singleton_iff, smul_eq_mul]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Hadamard (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℂ → E
l u : ℝ
hul : l < u
⊢ sSupNormIm (scale f l u) 0 = sSupNormIm f l
have simp_rw : sSup (norm '' scale f l u '' re ⁻¹' {0}) = sSup (norm '' f '' re ⁻¹' {l})
Tactic: simp_rw [sSupNormIm, image_comp]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Hadamard (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℂ → E
l u : ℝ
hul : l < u
⊢ scale f l u '' re ⁻¹' {0} = f '' re ⁻¹' {l}
have h : ∀ (e : E), e ∈ scale f l u '' re ⁻¹' {0} ↔ e ∈ f '' re ⁻¹' {l}
Tactic: ext e
-- Lean 4 proof step from Mathlib.Analysis.Complex.Hadamard (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℂ → E
l u : ℝ
hul : l < u
e : E
⊢ e ∈ scale f l u '' re ⁻¹' {0} ↔ e ∈ f '' re ⁻¹' {l}
have h : (∃ (x : ℂ), x.re = 0 ∧ f ((↑l : ℂ) + x * ((↑u : ℂ) - (↑l : ℂ))) = e) ↔ ∃ (x : ℂ), x.re = l ∧ f x = e
Tactic: simp only [scale, smul_eq_mul, mem_image, mem_preimage, mem_singleton_iff]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Hadamard (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℂ → E
l u : ℝ
hul : l < u
e : E
⊢ (∃ (x : ℂ), x.re = 0 ∧ f ((↑l : ℂ) + x * ((↑u : ℂ) - (↑l : ℂ))) = e) ↔ ∃ (x : ℂ), x.re = l ∧ f x = e
have h : (∃ (x : ℂ), x.re = 0 ∧ f ((↑l : ℂ) + x * ((↑u : ℂ) - (↑l : ℂ))) = e) → ∃ (x : ℂ), x.re = l ∧ f x = e
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.Complex.Hadamard (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℂ → E
l u : ℝ
hul : l < u
e : E
h : (∃ (x : ℂ), x.re = 0 ∧ f ((↑l : ℂ) + x * ((↑u : ℂ) - (↑l : ℂ))) = e) → ∃ (x : ℂ), x.re = l ∧ f x = e
⊢ (∃ (x : ℂ), x.re = 0 ∧ f ((↑l : ℂ) + x * ((↑u : ℂ) - (↑l : ℂ))) = e) ↔ ∃ (x : ℂ), x.re = l ∧ f x = e
have h₁ : (∃ (x : ℂ), x.re = l ∧ f x = e) → ∃ (x : ℂ), x.re = 0 ∧ f ((↑l : ℂ) + x * ((↑u : ℂ) - (↑l : ℂ))) = e
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.Complex.Hadamard (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℂ → E
l u : ℝ
hul : l < u
e : E
h : ∃ (x : ℂ), x.re = 0 ∧ f ((↑l : ℂ) + x * ((↑u : ℂ) - (↑l : ℂ))) = e
⊢ ∃ (x : ℂ), x.re = l ∧ f x = e
have h₁ : ∀ (z : ℂ) (hz₁ : z.re = 0) (hz₂ : f ((↑l : ℂ) + z * ((↑u : ℂ) - (↑l : ℂ))) = e), ∃ (x : ℂ), x.re = l ∧ f x = e
Tactic: obtain ⟨z, hz₁, hz₂⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.Complex.Hadamard (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℂ → E
l u : ℝ
hul : l < u
e : E
z : ℂ
hz₁ : z.re = 0
hz₂ : f ((↑l : ℂ) + z * ((↑u : ℂ) - (↑l : ℂ))) = e
⊢ ∃ (x : ℂ), x.re = l ∧ f x = e
have h : ((↑l : ℂ) + z * ((↑u : ℂ) - (↑l : ℂ))).re = l ∧ f ((↑l : ℂ) + z * ((↑u : ℂ) - (↑l : ℂ))) = e
Tactic: use ↑l + z * (↑u - ↑l)
-- Lean 4 proof step from Mathlib.Analysis.Complex.Hadamard (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℂ → E
l u : ℝ
hul : l < u
e : E
h : ∃ (x : ℂ), x.re = l ∧ f x = e
⊢ ∃ (x : ℂ), x.re = 0 ∧ f ((↑l : ℂ) + x * ((↑u : ℂ) - (↑l : ℂ))) = e
have h₁ : ∀ (z : ℂ) (hz₁ : z.re = l) (hz₂ : f z = e), ∃ (x : ℂ), x.re = 0 ∧ f ((↑l : ℂ) + x * ((↑u : ℂ) - (↑l : ℂ))) = e
Tactic: obtain ⟨z, hz₁, hz₂⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.Complex.Hadamard (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℂ → E
l u : ℝ
hul : l < u
e : E
z : ℂ
hz₁ : z.re = l
hz₂ : f z = e
⊢ ∃ (x : ℂ), x.re = 0 ∧ f ((↑l : ℂ) + x * ((↑u : ℂ) - (↑l : ℂ))) = e
have h : ((z - (↑l : ℂ)) / ((↑u : ℂ) - (↑l : ℂ))).re = 0 ∧
  f ((↑l : ℂ) + (z - (↑l : ℂ)) / ((↑u : ℂ) - (↑l : ℂ)) * ((↑u : ℂ) - (↑l : ℂ))) = e
Tactic: use ((z - l) / (u - l))
-- Lean 4 proof step from Mathlib.Analysis.Complex.Hadamard (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℂ → E
l u : ℝ
hul : l < u
e : E
z : ℂ
hz₁ : z.re = l
hz₂ : f z = e
⊢ ((z - (↑l : ℂ)) / ((↑u : ℂ) - (↑l : ℂ))).re = 0 ∧
    f ((↑l : ℂ) + (z - (↑l : ℂ)) / ((↑u : ℂ) - (↑l : ℂ)) * ((↑u : ℂ) - (↑l : ℂ))) = e
have h : ((z - (↑l : ℂ)) / ((↑u : ℂ) - (↑l : ℂ))).re = 0
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.Complex.Hadamard (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℂ → E
l u : ℝ
hul : l < u
e : E
z : ℂ
hz₁ : z.re = l
hz₂ : f z = e
h : ((z - (↑l : ℂ)) / ((↑u : ℂ) - (↑l : ℂ))).re = 0
⊢ ((z - (↑l : ℂ)) / ((↑u : ℂ) - (↑l : ℂ))).re = 0 ∧
    f ((↑l : ℂ) + (z - (↑l : ℂ)) / ((↑u : ℂ) - (↑l : ℂ)) * ((↑u : ℂ) - (↑l : ℂ))) = e
have h₁ : f ((↑l : ℂ) + (z - (↑l : ℂ)) / ((↑u : ℂ) - (↑l : ℂ)) * ((↑u : ℂ) - (↑l : ℂ))) = e
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.Complex.Hadamard (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℂ → E
l u : ℝ
hul : l < u
e : E
z : ℂ
hz₁ : z.re = l
hz₂ : f z = e
⊢ ((z - (↑l : ℂ)) / ((↑u : ℂ) - (↑l : ℂ))).re = 0
have h : ((z - (↑l : ℂ)) / (↑(u - l) : ℂ)).re = 0
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Analysis.Complex.Hadamard (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℂ → E
l u : ℝ
hul : l < u
e : E
z : ℂ
hz₁ : z.re = l
hz₂ : f z = e
⊢ ((z - (↑l : ℂ)) / (↑(u - l) : ℂ)).re = 0
have h : (z - (↑l : ℂ)).re * (u - l) / ((u - l) * (u - l)) + (z - (↑l : ℂ)).im * (↑(u - l) : ℂ).im / ((u - l) * (u - l)) = 0
Tactic: rw [Complex.div_re, Complex.normSq_ofReal, Complex.ofReal_re]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Hadamard (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℂ → E
l u : ℝ
hul : l < u
e : E
z : ℂ
hz₁ : z.re = l
hz₂ : f z = e
⊢ (↑u : ℂ) - (↑l : ℂ) ≠ 0
have norm_cast : ¬u - l = 0
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Analysis.Complex.Hadamard (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℂ → E
l u : ℝ
hul : l < u
e : E
z : ℂ
hz₁ : z.re = l
hz₂ : f z = e
⊢ ¬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:
E : Type u_1
inst : NormedAddCommGroup E
f : ℂ → E
l u : ℝ
hul : l < u
e : E
z : ℂ
hz₁ : z.re = l
hz₂ : f z = e
⊢ f ((↑l : ℂ) + (z - (↑l : ℂ)) / ((↑u : ℂ) - (↑l : ℂ)) * ((↑u : ℂ) - (↑l : ℂ))) = e
have h : f ((↑l : ℂ) + 1 * (z - (↑l : ℂ))) = e
Tactic: rw [div_mul_comm, div_self (by norm_cast; linarith)]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Hadamard (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℂ → E
l u : ℝ
hul : l < u
⊢ sSup (norm '' scale f l u '' re ⁻¹' {0}) = sSup (norm '' f '' re ⁻¹' {l})
have this : scale f l u '' re ⁻¹' {0} = f '' re ⁻¹' {l}
Tactic: have : scale f l u '' re ⁻¹' {0} = f '' re ⁻¹' {l} := by
    ext e
    simp only [scale, smul_eq_mul, mem_image, mem_preimage, mem_singleton_iff]
    constructor
    · intro h
      obtain ⟨z, hz₁, hz₂⟩ := h
      use ↑l + z * (↑u - ↑l)
      simp [hz₁, hz₂]
    · intro h
      obtain ⟨z, hz₁, hz₂⟩ := h
      use ((z - l) / (u - l))
      constructor
      · norm_cast
        rw [Complex.div_re, Complex.normSq_ofReal, Complex.ofReal_re]
        simp [hz₁]
      · rw [div_mul_comm, div_self (by norm_cast; linarith)]
        simp [hz₂]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Hadamard (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℂ → E
l u : ℝ
hul : l < u
this : scale f l u '' re ⁻¹' {0} = f '' re ⁻¹' {l}
⊢ sSup (norm '' scale f l u '' re ⁻¹' {0}) = sSup (norm '' f '' re ⁻¹' {l})
have rw : sSup (norm '' f '' re ⁻¹' {l}) = sSup (norm '' f '' re ⁻¹' {l})
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Hadamard (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℂ → E
l u : ℝ
hul : l < u
⊢ sSupNormIm (scale f l u) 1 = sSupNormIm f u
have simp_rw : sSup (norm '' scale f l u '' re ⁻¹' {1}) = sSup (norm '' f '' re ⁻¹' {u})
Tactic: simp_rw [sSupNormIm, image_comp]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Hadamard (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℂ → E
l u : ℝ
hul : l < u
⊢ scale f l u '' re ⁻¹' {1} = f '' re ⁻¹' {u}
have h : ∀ (e : E), e ∈ scale f l u '' re ⁻¹' {1} ↔ e ∈ f '' re ⁻¹' {u}
Tactic: ext e
-- Lean 4 proof step from Mathlib.Analysis.Complex.Hadamard (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℂ → E
l u : ℝ
hul : l < u
e : E
⊢ e ∈ scale f l u '' re ⁻¹' {1} ↔ e ∈ f '' re ⁻¹' {u}
have h : (∃ (x : ℂ), x.re = 1 ∧ f ((↑l : ℂ) + x * ((↑u : ℂ) - (↑l : ℂ))) = e) ↔ ∃ (x : ℂ), x.re = u ∧ f x = e
Tactic: simp only [scale, smul_eq_mul, mem_image, mem_preimage, mem_singleton_iff]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Hadamard (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℂ → E
l u : ℝ
hul : l < u
e : E
⊢ (∃ (x : ℂ), x.re = 1 ∧ f ((↑l : ℂ) + x * ((↑u : ℂ) - (↑l : ℂ))) = e) ↔ ∃ (x : ℂ), x.re = u ∧ f x = e
have h : (∃ (x : ℂ), x.re = 1 ∧ f ((↑l : ℂ) + x * ((↑u : ℂ) - (↑l : ℂ))) = e) → ∃ (x : ℂ), x.re = u ∧ f x = e
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.Complex.Hadamard (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℂ → E
l u : ℝ
hul : l < u
e : E
h : (∃ (x : ℂ), x.re = 1 ∧ f ((↑l : ℂ) + x * ((↑u : ℂ) - (↑l : ℂ))) = e) → ∃ (x : ℂ), x.re = u ∧ f x = e
⊢ (∃ (x : ℂ), x.re = 1 ∧ f ((↑l : ℂ) + x * ((↑u : ℂ) - (↑l : ℂ))) = e) ↔ ∃ (x : ℂ), x.re = u ∧ f x = e
have h₁ : (∃ (x : ℂ), x.re = u ∧ f x = e) → ∃ (x : ℂ), x.re = 1 ∧ f ((↑l : ℂ) + x * ((↑u : ℂ) - (↑l : ℂ))) = e
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.Complex.Hadamard (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℂ → E
l u : ℝ
hul : l < u
e : E
h : ∃ (x : ℂ), x.re = 1 ∧ f ((↑l : ℂ) + x * ((↑u : ℂ) - (↑l : ℂ))) = e
⊢ ∃ (x : ℂ), x.re = u ∧ f x = e
have h₁ : ∀ (z : ℂ) (hz₁ : z.re = 1) (hz₂ : f ((↑l : ℂ) + z * ((↑u : ℂ) - (↑l : ℂ))) = e), ∃ (x : ℂ), x.re = u ∧ f x = e
Tactic: obtain ⟨z, hz₁, hz₂⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.Complex.Hadamard (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℂ → E
l u : ℝ
hul : l < u
e : E
z : ℂ
hz₁ : z.re = 1
hz₂ : f ((↑l : ℂ) + z * ((↑u : ℂ) - (↑l : ℂ))) = e
⊢ ∃ (x : ℂ), x.re = u ∧ f x = e
have h : ((↑l : ℂ) + z * ((↑u : ℂ) - (↑l : ℂ))).re = u ∧ f ((↑l : ℂ) + z * ((↑u : ℂ) - (↑l : ℂ))) = e
Tactic: use ↑l + z * (↑u - ↑l)