awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Complex.Hadamard
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
apply₁ : (norm ∘ f '' re ⁻¹' {1}).Nonempty
⊢ sSup (norm ∘ f '' re ⁻¹' {1}) ≤ b

Tactic:
apply csSup_le _

Premises used: csSup_le
-- Module: Mathlib.Analysis.Complex.Hadamard
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
⊢ ∀ b_1 ∈ norm ∘ f '' re ⁻¹' {1}, b_1 ≤ b

Tactic:
simpa [comp_apply, mem_image, forall_exists_index,
          and_imp, forall_apply_eq_imp_iff₂] using hb

Premises used: and_imp, Set.mem_image, forall_exists_index, Function.comp_apply, forall_apply_eq_imp_iff₂
-- Module: Mathlib.Analysis.Complex.Hadamard
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 : 1 ∈ re ⁻¹' {1} ∧ (norm ∘ f) 1 = ‖f 1‖
⊢ (norm ∘ f '' re ⁻¹' {1}).Nonempty

Tactic:
use ‖(f 1)‖, 1

Premises used: OfNat.ofNat
-- Module: Mathlib.Analysis.Complex.Hadamard
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
⊢ 1 ∈ re ⁻¹' {1} ∧ (norm ∘ f) 1 = ‖f 1‖

Tactic:
simp only [mem_preimage, one_re, mem_singleton_iff, comp_apply,
          and_self]

Premises used: and_self, Set.mem_singleton_iff, Function.comp_apply, Complex.one_re, Set.mem_preimage
-- Module: Mathlib.Analysis.Complex.Hadamard
Goal:
l u : ℝ
hul : l < u
z : ℂ
hz : z ∈ verticalStrip 0 1
⊢ 0 < z.re ∧ z.re < 1

Tactic:
simp only [verticalStrip, mem_preimage, mem_Ioo] at hz

Premises used: Set.mem_Ioo, Complex.HadamardThreeLines.verticalStrip, Set.mem_preimage
-- Module: Mathlib.Analysis.Complex.Hadamard
Goal:
l u : ℝ
hul : l < u
z : ℂ
hz : 0 < z.re ∧ z.re < 1
simp : 0 < z.re * (u - l) ∧ l + z.re * (u - l) < u
⊢ (↑l : ℂ) + z * ((↑u : ℂ) - (↑l : ℂ)) ∈ verticalStrip 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]

Premises used: lt_add_iff_pos_right, Set.mem_Ioo, Complex.mul_re, sub_self, Complex.sub_im, sub_zero, Complex.sub_re, Complex.add_re, Complex.HadamardThreeLines.verticalStrip, MulZeroClass.mul_zero, Complex.ofReal_re, Complex.ofReal_im, Set.mem_preimage
-- Module: Mathlib.Analysis.Complex.Hadamard
Goal:
l u : ℝ
hul : l < u
z : ℂ
hz : 0 < z.re ∧ z.re < 1
⊢ 0 < z.re

Tactic:
obtain ⟨hz₁, hz₂⟩ := hz
-- Module: Mathlib.Analysis.Complex.Hadamard
Goal:
l u : ℝ
hul : l < u
z : ℂ
hz : 0 < z.re ∧ z.re < 1
hz₁ : 0 < z.re
⊢ z.re < 1

Tactic:
obtain ⟨hz₁, hz₂⟩ := hz
-- Module: Mathlib.Analysis.Complex.Hadamard
Goal:
l u : ℝ
hul : l < u
z : ℂ
hz₁ : 0 < z.re
hz₂ : z.re < 1
simp : l + z.re * (u - l) < u
⊢ 0 < z.re * (u - l) ∧ l + z.re * (u - l) < u

Tactic:
simp only [hz₁, mul_pos_iff_of_pos_left, sub_pos, hul, true_and]

Premises used: sub_pos, mul_pos_iff_of_pos_left, true_and
-- Module: Mathlib.Analysis.Complex.Hadamard
Goal:
l u : ℝ
hul : l < u
z : ℂ
hz₁ : 0 < z.re
hz₂ : z.re < 1
rw : z.re * (u - l) < u - l
⊢ l + z.re * (u - l) < u

Tactic:
rw [add_comm, ← sub_lt_sub_iff_right l, add_sub_assoc, sub_self, add_zero]

Premises used: add_sub_assoc, sub_self, sub_lt_sub_iff_right, add_comm, add_zero
-- Module: Mathlib.Analysis.Complex.Hadamard
Goal:
l u : ℝ
hul : l < u
z : ℂ
hz₁ : 0 < z.re
hz₂ : z.re < 1
nth_rewrite : z.re * (u - l) < 1 * (u - l)
⊢ z.re * (u - l) < u - l

Tactic:
nth_rewrite 2 [← one_mul (u - l)]

Premises used: HSub.hSub, one_mul
-- Module: Mathlib.Analysis.Complex.Hadamard
Goal:
l u : ℝ
hul : l < u
z : ℂ
hz₁ : 0 < z.re
hz₂ : z.re < 1
ha : 0 < u - l
⊢ z.re * (u - l) < 1 * (u - l)

Tactic:
gcongr
-- Module: Mathlib.Analysis.Complex.Hadamard
Goal:
z : ℂ
l u : ℝ
hul : l < u
hz : z ∈ verticalClosedStrip l u
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 : ℂ)) : ℝ)
⊢ z / ((↑u : ℂ) - (↑l : ℂ)) - (↑l : ℂ) / ((↑u : ℂ) - (↑l : ℂ)) ∈ verticalClosedStrip 0 1

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]

Premises used: sub_self, Complex.sub_im, Complex.sub_re, zero_div, tsub_le_iff_right, MulZeroClass.mul_zero, Complex.div_re, Set.mem_Icc, Complex.ofReal_re, Complex.HadamardThreeLines.verticalClosedStrip, Complex.ofReal_im, add_zero, sub_nonneg, Set.mem_preimage
-- Module: Mathlib.Analysis.Complex.Hadamard
Goal:
z : ℂ
l u : ℝ
hul : l < u
hz : z ∈ re ⁻¹' Icc l u
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) : ℂ) : ℝ)
⊢ 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
-- Module: Mathlib.Analysis.Complex.Hadamard
Goal:
z : ℂ
l u : ℝ
hul : l < u
hz : z ∈ re ⁻¹' Icc l u
linarith : u - l = 0 → l - u + (u - l - 0) = 0
⊢ u - l ≠ 0

Tactic:
linarith
-- Module: Mathlib.Analysis.Complex.Hadamard
Goal:
z : ℂ
l u : ℝ
hul : l < u
hz : z ∈ re ⁻¹' Icc l u
simp_rw : l / (u - l) ≤ z.re / (u - l) ∧ z.re / (u - l) ≤ 1 + l / (u - l)
⊢ 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_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]

Premises used: mul_div_assoc, div_mul_eq_div_div_swap, Complex.normSq_ofReal, div_eq_mul_one_div, div_self
-- Module: Mathlib.Analysis.Complex.Hadamard
Goal:
z : ℂ
l u : ℝ
hul : l < u
hz : z ∈ re ⁻¹' Icc l u
left : l / (u - l) ≤ z.re / (u - l)
right : z.re / (u - l) ≤ 1 + l / (u - l)
⊢ l / (u - l) ≤ z.re / (u - l) ∧ z.re / (u - l) ≤ 1 + l / (u - l)

Tactic:
constructor
-- Module: Mathlib.Analysis.Complex.Hadamard
Goal:
z : ℂ
l u : ℝ
hul : l < u
hz : z ∈ re ⁻¹' Icc l u
left : l ≤ z.re
⊢ l / (u - l) ≤ z.re / (u - l)

Tactic:
gcongr
-- Module: Mathlib.Analysis.Complex.Hadamard
Goal:
z : ℂ
l u : ℝ
hul : l < u
hz : z ∈ re ⁻¹' Icc l u
⊢ l ≤ z.re

Tactic:
hz.1

Premises used: And.left
-- Module: Mathlib.Analysis.Complex.Hadamard
Goal:
z : ℂ
l u : ℝ
hul : l < u
hz : z ∈ re ⁻¹' Icc l u
⊢ l ≤ z.re

Tactic:
exact hz.1

Premises used: And.left
-- Module: Mathlib.Analysis.Complex.Hadamard
Goal:
z : ℂ
l u : ℝ
hul : l < u
hz : z ∈ re ⁻¹' Icc l u
⊢ 0 < u - l

Tactic:
simp [hul]
-- Module: Mathlib.Analysis.Complex.Hadamard
Goal:
z : ℂ
l u : ℝ
hul : l < u
hz : z ∈ re ⁻¹' Icc l u
right : z.re ≤ u
⊢ z.re / (u - l) ≤ 1 + l / (u - l)

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]

Premises used: add_sub_assoc, sub_self, HSub.hSub, sub_le_sub_iff_right, HDiv.hDiv, div_le_one, div_sub_div_same, add_zero
-- Module: Mathlib.Analysis.Complex.Hadamard
Goal:
z : ℂ
l u : ℝ
hul : l < u
hz : z ∈ re ⁻¹' Icc l u
⊢ z.re ≤ u

Tactic:
hz.2

Premises used: And.right
-- Module: Mathlib.Analysis.Complex.Hadamard
Goal:
z : ℂ
l u : ℝ
hul : l < u
hz : z ∈ re ⁻¹' Icc l u
⊢ z.re ≤ u

Tactic:
exact hz.2

Premises used: And.right
-- Module: Mathlib.Analysis.Complex.Hadamard
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)
unfold :
  DiffContOnCl.{0, 0, u_1} ℂ (F := E) (fun (z : ℂ) ↦ f ((↑l : ℂ) + z • ((↑u : ℂ) - (↑l : ℂ)))) (verticalStrip 0 1)
⊢ DiffContOnCl ℂ (scale f l u) (verticalStrip 0 1)

Tactic:
unfold scale

Premises used: Complex.HadamardThreeLines.scale
-- Module: Mathlib.Analysis.Complex.Hadamard
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)
h : MapsTo (fun (z : ℂ) ↦ (↑l : ℂ) + z • ((↑u : ℂ) - (↑l : ℂ))) (verticalStrip 0 1) (verticalStrip l u)
⊢ DiffContOnCl.{0, 0, u_1} ℂ (F := E) (fun (z : ℂ) ↦ f ((↑l : ℂ) + z • ((↑u : ℂ) - (↑l : ℂ)))) (verticalStrip 0 1)

Tactic:
apply DiffContOnCl.comp (s := verticalStrip l u) hd

Premises used: DiffContOnCl.comp
-- Module: Mathlib.Analysis.Complex.Hadamard
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 (x : ℂ) ↦ x • ((↑u : ℂ) - (↑l : ℂ))) (verticalStrip 0 1)
⊢ DiffContOnCl ℂ (F := ℂ) (fun (z : ℂ) ↦ (↑l : ℂ) + z • ((↑u : ℂ) - (↑l : ℂ))) (verticalStrip 0 1)

Tactic:
apply DiffContOnCl.const_add

Premises used: DiffContOnCl.const_add
-- Module: Mathlib.Analysis.Complex.Hadamard
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 (x : ℂ) ↦ x) (verticalStrip 0 1)
⊢ DiffContOnCl ℂ (F := ℂ) (fun (x : ℂ) ↦ x • ((↑u : ℂ) - (↑l : ℂ))) (verticalStrip 0 1)

Tactic:
apply DiffContOnCl.smul_const

Premises used: DiffContOnCl.smul_const
-- Module: Mathlib.Analysis.Complex.Hadamard
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) (verticalStrip 0 1)

Tactic:
Differentiable.diffContOnCl differentiable_id

Premises used: Differentiable.diffContOnCl, differentiable_id
-- Module: Mathlib.Analysis.Complex.Hadamard
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) (verticalStrip 0 1)

Tactic:
exact Differentiable.diffContOnCl differentiable_id

Premises used: Differentiable.diffContOnCl, differentiable_id
-- Module: Mathlib.Analysis.Complex.Hadamard
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)
z : ℂ
hz : z ∈ verticalStrip 0 1
⊢ (↑l : ℂ) + z • ((↑u : ℂ) - (↑l : ℂ)) ∈ verticalStrip l u

Tactic:
scale_id_mem_verticalStrip_of_mem_verticalStrip hul hz

Premises used: Set.Mem, Complex.HadamardThreeLines.scale_id_mem_verticalStrip_of_mem_verticalStrip
-- Module: Mathlib.Analysis.Complex.Hadamard
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)
z : ℂ
hz : z ∈ verticalStrip 0 1
⊢ (↑l : ℂ) + z • ((↑u : ℂ) - (↑l : ℂ)) ∈ verticalStrip l u

Tactic:
exact scale_id_mem_verticalStrip_of_mem_verticalStrip hul hz

Premises used: Complex.HadamardThreeLines.scale_id_mem_verticalStrip_of_mem_verticalStrip
-- Module: Mathlib.Analysis.Complex.Hadamard
Goal:
l u : ℝ
hul : l < u
z : ℂ
norm_cast : ¬u - l = 0
⊢ (↑u : ℂ) - (↑l : ℂ) ≠ 0

Tactic:
norm_cast
-- Module: Mathlib.Analysis.Complex.Hadamard
Goal:
l u : ℝ
hul : l < u
z : ℂ
linarith : u - l = 0 → l - u + (u - l - 0) = 0
⊢ ¬u - l = 0

Tactic:
linarith
-- Module: Mathlib.Analysis.Complex.Hadamard
Goal:
l u : ℝ
hul : l < u
z : ℂ
rw : (↑l : ℂ) + (1 * z - 1 * (↑l : ℂ)) = z
⊢ (↑l : ℂ) + (z / ((↑u : ℂ) - (↑l : ℂ)) - (↑l : ℂ) / ((↑u : ℂ) - (↑l : ℂ))) * ((↑u : ℂ) - (↑l : ℂ)) = z

Tactic:
rw [sub_mul, div_mul_comm, div_self (by norm_cast; linarith),
    div_mul_comm, div_self (by norm_cast; linarith)]

Premises used: sub_mul, div_mul_comm, div_self
-- Module: Mathlib.Analysis.Complex.Hadamard
Goal:
l u : ℝ
hul : l < u
z : ℂ
⊢ (↑l : ℂ) + (1 * z - 1 * (↑l : ℂ)) = z

Tactic:
simp
-- Module: Mathlib.Analysis.Complex.Hadamard
Goal:
l u : ℝ
hul : l < u
z : ℂ
norm_cast : (z / (↑(u - l) : ℂ)).re - l / (u - l) = (z.re - l) / (u - l)
⊢ (z / ((↑u : ℂ) - (↑l : ℂ))).re - ((↑l : ℂ) / ((↑u : ℂ) - (↑l : ℂ))).re = (z.re - l) / (u - l)

Tactic:
norm_cast
-- Module: Mathlib.Analysis.Complex.Hadamard
Goal:
l u : ℝ
hul : l < u
z : ℂ
rw : z.re / (u - l) + z.im * 0 / ((u - l) * (u - l)) - l / (u - l) = (z.re - l) / (u - l)
⊢ (z / (↑(u - l) : ℂ)).re - 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]

Premises used: mul_div_assoc, div_mul_eq_div_div_swap, Complex.div_re, Complex.normSq_ofReal, div_eq_mul_one_div, Complex.ofReal_re, Complex.ofReal_im, div_self
-- Module: Mathlib.Analysis.Complex.Hadamard
Goal:
l u : ℝ
hul : l < u
z : ℂ
simp : z.re / (u - l) - l / (u - l) = (z.re - l) / (u - l)
⊢ z.re / (u - l) + z.im * 0 / ((u - l) * (u - l)) - l / (u - l) = (z.re - l) / (u - l)

Tactic:
simp only [mul_zero, zero_div, add_zero]

Premises used: zero_div, MulZeroClass.mul_zero, add_zero
-- Module: Mathlib.Analysis.Complex.Hadamard
Goal:
l u : ℝ
hul : l < u
z : ℂ
rw rw₁ : z.re / (u - l) - l / (u - l) = z.re / (u - l) - l / (u - l)
⊢ z.re / (u - l) - l / (u - l) = (z.re - l) / (u - l)

Tactic:
rw [← div_sub_div_same]

Premises used: div_sub_div_same
-- Module: Mathlib.Analysis.Complex.Hadamard
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)
⊢ ‖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)
-- Module: Mathlib.Analysis.Complex.Hadamard
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)
hgoal :
  ‖f ((↑l : ℂ) + (z / ((↑u : ℂ) - (↑l : ℂ)) - (↑l : ℂ) / ((↑u : ℂ) - (↑l : ℂ))) * ((↑u : ℂ) - (↑l : ℂ)))‖ ≤
    ‖interpStrip (scale f l u) (z / ((↑u : ℂ) - (↑l : ℂ)) - (↑l : ℂ) / ((↑u : ℂ) - (↑l : ℂ)))‖
⊢ ‖f z‖ ≤ ‖interpStrip' f l u z‖

Tactic:
rw [fun_arg_eq hul, div_sub_div_same, interpStrip_scale f hul z] at hgoal

Premises used: Complex.HadamardThreeLines.interpStrip_scale, div_sub_div_same, _private.0.Complex.HadamardThreeLines.fun_arg_eq
-- Module: Mathlib.Analysis.Complex.Hadamard
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)
hgoal : ‖f z‖ ≤ ‖interpStrip' f l u z‖
⊢ ‖f z‖ ≤ ‖interpStrip' f l u z‖

Tactic:
hgoal
-- Module: Mathlib.Analysis.Complex.Hadamard
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)
hgoal : ‖f z‖ ≤ ‖interpStrip' f l u z‖
⊢ ‖f z‖ ≤ ‖interpStrip' f l u z‖

Tactic:
exact hgoal
-- Module: Mathlib.Analysis.Complex.Hadamard
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
⊢ ‖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)
-- Module: Mathlib.Analysis.Complex.Hadamard
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
hgoal :
  ‖f ((↑l : ℂ) + (z / ((↑u : ℂ) - (↑l : ℂ)) - (↑l : ℂ) / ((↑u : ℂ) - (↑l : ℂ))) * ((↑u : ℂ) - (↑l : ℂ)))‖ ≤
    a ^ (1 - ((z / ((↑u : ℂ) - (↑l : ℂ))).re - ((↑l : ℂ) / ((↑u : ℂ) - (↑l : ℂ))).re)) *
      b ^ ((z / ((↑u : ℂ) - (↑l : ℂ))).re - ((↑l : ℂ) / ((↑u : ℂ) - (↑l : ℂ))).re)
⊢ ‖f z‖ ≤ a ^ (1 - (z.re - l) / (u - l)) * b ^ ((z.re - l) / (u - l))

Tactic:
rw [fun_arg_eq hul, bound_exp_eq hul] at hgoal

Premises used: _private.0.Complex.HadamardThreeLines.bound_exp_eq, _private.0.Complex.HadamardThreeLines.fun_arg_eq
-- Module: Mathlib.Analysis.Complex.Hadamard
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
hgoal : ‖f z‖ ≤ a ^ (1 - (z.re - l) / (u - l)) * b ^ ((z.re - l) / (u - l))
⊢ ‖f z‖ ≤ a ^ (1 - (z.re - l) / (u - l)) * b ^ ((z.re - l) / (u - l))

Tactic:
hgoal
-- Module: Mathlib.Analysis.Complex.Hadamard
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
hgoal : ‖f z‖ ≤ a ^ (1 - (z.re - l) / (u - l)) * b ^ ((z.re - l) / (u - l))
⊢ ‖f z‖ ≤ a ^ (1 - (z.re - l) / (u - l)) * b ^ ((z.re - l) / (u - l))

Tactic:
exact hgoal
-- Module: Mathlib.Analysis.Complex.HalfPlane
Goal:
x : EReal
⊢ IsOpen (X := ℂ) {z : ℂ | (↑z.re : EReal) < x}

Tactic:
isOpen_lt (EReal.continuous_coe_iff.mpr continuous_re) continuous_const

Premises used: Iff.mpr, isOpen_lt, Complex.continuous_re, continuous_const, setOf, EReal.continuous_coe_iff
-- Module: Mathlib.Analysis.Complex.HalfPlane
Goal:
x : EReal
⊢ IsOpen (X := ℂ) {z : ℂ | x < (↑z.re : EReal)}

Tactic:
isOpen_lt continuous_const <| EReal.continuous_coe_iff.mpr continuous_re

Premises used: Iff.mpr, isOpen_lt, Complex.continuous_re, continuous_const, setOf, EReal.continuous_coe_iff
-- Module: Mathlib.Analysis.Complex.HalfPlane
Goal:
x : EReal
⊢ IsOpen (X := ℂ) {z : ℂ | (↑z.im : EReal) < x}

Tactic:
isOpen_lt (EReal.continuous_coe_iff.mpr continuous_im) continuous_const

Premises used: Iff.mpr, isOpen_lt, continuous_const, setOf, EReal.continuous_coe_iff, Complex.continuous_im
-- Module: Mathlib.Analysis.Complex.HalfPlane
Goal:
x : EReal
⊢ IsOpen (X := ℂ) {z : ℂ | x < (↑z.im : EReal)}

Tactic:
isOpen_lt continuous_const <| EReal.continuous_coe_iff.mpr continuous_im

Premises used: Iff.mpr, isOpen_lt, continuous_const, setOf, EReal.continuous_coe_iff, Complex.continuous_im
-- Module: Mathlib.Analysis.Complex.Harmonic.Analytic
Goal:
f : ℂ → ℝ
x : ℂ
hf : HarmonicAt f x
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
⊢ (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:
ext
-- Module: Mathlib.Analysis.Complex.Harmonic.Analytic
Goal:
f : ℂ → ℝ
x : ℂ
hf : HarmonicAt f x
x_1 : ℂ
⊢ (↑((fderiv ℝ f x_1 : (a : ℂ) → ℝ) 1) : ℂ) - I * (↑((fderiv ℝ f x_1 : (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_1

Tactic:
simp
-- Module: Mathlib.Analysis.Complex.Harmonic.Analytic
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)

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
-- Module: Mathlib.Analysis.Complex.Harmonic.Analytic
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)
⊢ ContDiffAt ℝ 2 f x

Tactic:
have h₁f := hf.1
-- Module: Mathlib.Analysis.Complex.Harmonic.Analytic
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)
h₁f : ContDiffAt ℝ 2 f x
funProp : IsBoundedLinearMap ℝ (F := ℂ →L[ℝ] ℝ) fun (x : ℂ) ↦ fderiv ℝ f x
⊢ 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

Tactic:
fun_prop