awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Complex.Conformal (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
ℓ : ℂ →ₗ[ℝ] E
h : (ℓ : (a : ℂ) → E) I = HSMul.hSMul (β := E) I ((ℓ : (a : ℂ) → E) 1 : E)
a b : ℂ
t₀ : ((↑a.im : ℂ) • I) • (↑b.re : ℂ) = (↑(a.im * b.re) : ℂ) • I
t₁ : ((↑a.im : ℂ) • I) • (↑b.im : ℂ) • I = HSMul.hSMul (β := ℂ) (↑(-a.im * b.im) : ℂ) 1
⊢ HSMul.hSMul (β := E) a.re ((ℓ : (a : ℂ) → E) (↑b.re : ℂ) : E) +
        HSMul.hSMul (β := E) (a.im * b.re) ((ℓ : (a : ℂ) → E) I : E) +
      HAdd.hAdd (β := E) (HSMul.hSMul (β := E) a.re ((ℓ : (a : ℂ) → E) ((↑b.im : ℂ) • I) : E))
        ((ℓ : (a : ℂ) → E) (HSMul.hSMul (β := ℂ) (↑(-a.im * b.im) : ℂ) 1) : E) =
    HSMul.hSMul (β := E) (↑a.re : ℂ) ((ℓ : (a : ℂ) → E) (↑b.re : ℂ) : E) +
        HSMul.hSMul (β := E) ((↑a.im : ℂ) • I) ((ℓ : (a : ℂ) → E) (↑b.re : ℂ) : E) +
      (HSMul.hSMul (β := E) (↑a.re : ℂ) ((ℓ : (a : ℂ) → E) ((↑b.im : ℂ) • I) : E) +
        HSMul.hSMul (β := E) ((↑a.im : ℂ) • I) ((ℓ : (a : ℂ) → E) ((↑b.im : ℂ) • I) : E))
have rw : HSMul.hSMul (β := E) a.re ((ℓ : (a : ℂ) → E) (↑b.re : ℂ) : E) +
      HSMul.hSMul (β := E) (a.im * b.re) ((ℓ : (a : ℂ) → E) I : E) +
    HAdd.hAdd (β := E) (a.re • HSMul.hSMul (β := E) b.im ((ℓ : (a : ℂ) → E) I : E))
      ((ℓ : (a : ℂ) → E) (HSMul.hSMul (β := ℂ) (↑(-a.im * b.im) : ℂ) 1) : E) =
  HSMul.hSMul (β := E) (↑a.re : ℂ) ((ℓ : (a : ℂ) → E) (↑b.re : ℂ) : E) +
      HSMul.hSMul (β := E) ((↑a.im : ℂ) • I) ((ℓ : (a : ℂ) → E) (↑b.re : ℂ) : E) +
    ((↑a.re : ℂ) • HSMul.hSMul (β := E) b.im ((ℓ : (a : ℂ) → E) I : E) +
      ((↑a.im : ℂ) • I) • HSMul.hSMul (β := E) b.im ((ℓ : (a : ℂ) → E) I : E))
Tactic: rw [Complex.coe_smul, ℓ.map_smul]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Conformal (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
ℓ : ℂ →ₗ[ℝ] E
h : (ℓ : (a : ℂ) → E) I = HSMul.hSMul (β := E) I ((ℓ : (a : ℂ) → E) 1 : E)
a b : ℂ
t₀ : ((↑a.im : ℂ) • I) • (↑b.re : ℂ) = (↑(a.im * b.re) : ℂ) • I
t₁ : ((↑a.im : ℂ) • I) • (↑b.im : ℂ) • I = HSMul.hSMul (β := ℂ) (↑(-a.im * b.im) : ℂ) 1
⊢ HSMul.hSMul (β := E) a.re ((ℓ : (a : ℂ) → E) (↑b.re : ℂ) : E) +
        HSMul.hSMul (β := E) (a.im * b.re) ((ℓ : (a : ℂ) → E) I : E) +
      HAdd.hAdd (β := E) (a.re • HSMul.hSMul (β := E) b.im ((ℓ : (a : ℂ) → E) I : E))
        ((ℓ : (a : ℂ) → E) (HSMul.hSMul (β := ℂ) (↑(-a.im * b.im) : ℂ) 1) : E) =
    HSMul.hSMul (β := E) (↑a.re : ℂ) ((ℓ : (a : ℂ) → E) (↑b.re : ℂ) : E) +
        HSMul.hSMul (β := E) ((↑a.im : ℂ) • I) ((ℓ : (a : ℂ) → E) (↑b.re : ℂ) : E) +
      ((↑a.re : ℂ) • HSMul.hSMul (β := E) b.im ((ℓ : (a : ℂ) → E) I : E) +
        ((↑a.im : ℂ) • I) • HSMul.hSMul (β := E) b.im ((ℓ : (a : ℂ) → E) I : E))
have rw : HSMul.hSMul (β := E) a.re ((ℓ : (a : ℂ) → E) (↑b.re : ℂ) : E) +
      HSMul.hSMul (β := E) (a.im * b.re) ((ℓ : (a : ℂ) → E) I : E) +
    (a.re • HSMul.hSMul (β := E) b.im ((ℓ : (a : ℂ) → E) I : E) +
      HSMul.hSMul (β := E) (-a.im * b.im) ((ℓ : (a : ℂ) → E) 1 : E)) =
  HSMul.hSMul (β := E) (↑a.re : ℂ) ((ℓ : (a : ℂ) → E) (↑b.re : ℂ) : E) +
      HSMul.hSMul (β := E) ((↑a.im : ℂ) • I) ((ℓ : (a : ℂ) → E) (↑b.re : ℂ) : E) +
    ((↑a.re : ℂ) • HSMul.hSMul (β := E) b.im ((ℓ : (a : ℂ) → E) I : E) +
      ((↑a.im : ℂ) • I) • HSMul.hSMul (β := E) b.im ((ℓ : (a : ℂ) → E) I : E))
Tactic: rw [Complex.coe_smul, ℓ.map_smul]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Conformal (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
ℓ : ℂ →ₗ[ℝ] E
h : (ℓ : (a : ℂ) → E) I = HSMul.hSMul (β := E) I ((ℓ : (a : ℂ) → E) 1 : E)
a b : ℂ
t₀ : ((↑a.im : ℂ) • I) • (↑b.re : ℂ) = (↑(a.im * b.re) : ℂ) • I
t₁ : ((↑a.im : ℂ) • I) • (↑b.im : ℂ) • I = HSMul.hSMul (β := ℂ) (↑(-a.im * b.im) : ℂ) 1
⊢ HAdd.hAdd (α := E) (β := E) ((ℓ : (a : ℂ) → E) ((↑a.re : ℂ) • (↑b.re : ℂ)) : E)
        ((ℓ : (a : ℂ) → E) ((↑(a.im * b.re) : ℂ) • I) : E) +
      HAdd.hAdd (α := E) (β := E) ((ℓ : (a : ℂ) → E) ((↑a.re : ℂ) • (↑b.im : ℂ) • I) : E)
        ((ℓ : (a : ℂ) → E) (HSMul.hSMul (β := ℂ) (↑(-a.im * b.im) : ℂ) 1) : E) =
    HSMul.hSMul (β := E) (↑a.re : ℂ) ((ℓ : (a : ℂ) → E) (↑b.re : ℂ) : E) +
        HSMul.hSMul (β := E) ((↑a.im : ℂ) • I) ((ℓ : (a : ℂ) → E) (↑b.re : ℂ) : E) +
      (HSMul.hSMul (β := E) (↑a.re : ℂ) ((ℓ : (a : ℂ) → E) ((↑b.im : ℂ) • I) : E) +
        HSMul.hSMul (β := E) ((↑a.im : ℂ) • I) ((ℓ : (a : ℂ) → E) ((↑b.im : ℂ) • I) : E))
have repeat : HSMul.hSMul (β := E) a.re ((ℓ : (a : ℂ) → E) (↑b.re : ℂ) : E) +
      HSMul.hSMul (β := E) (a.im * b.re) ((ℓ : (a : ℂ) → E) I : E) +
    (a.re • HSMul.hSMul (β := E) b.im ((ℓ : (a : ℂ) → E) I : E) +
      HSMul.hSMul (β := E) (-a.im * b.im) ((ℓ : (a : ℂ) → E) 1 : E)) =
  HSMul.hSMul (β := E) (↑a.re : ℂ) ((ℓ : (a : ℂ) → E) (↑b.re : ℂ) : E) +
      HSMul.hSMul (β := E) ((↑a.im : ℂ) • I) ((ℓ : (a : ℂ) → E) (↑b.re : ℂ) : E) +
    ((↑a.re : ℂ) • HSMul.hSMul (β := E) b.im ((ℓ : (a : ℂ) → E) I : E) +
      ((↑a.im : ℂ) • I) • HSMul.hSMul (β := E) b.im ((ℓ : (a : ℂ) → E) I : E))
Tactic: repeat rw [Complex.coe_smul, ℓ.map_smul]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Conformal (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
ℓ : ℂ →ₗ[ℝ] E
h : (ℓ : (a : ℂ) → E) I = HSMul.hSMul (β := E) I ((ℓ : (a : ℂ) → E) 1 : E)
a b : ℂ
t₀ : ((↑a.im : ℂ) • I) • (↑b.re : ℂ) = (↑(a.im * b.re) : ℂ) • I
t₁ : ((↑a.im : ℂ) • I) • (↑b.im : ℂ) • I = HSMul.hSMul (β := ℂ) (↑(-a.im * b.im) : ℂ) 1
⊢ HSMul.hSMul (β := E) a.re ((ℓ : (a : ℂ) → E) (↑b.re : ℂ) : E) +
        HSMul.hSMul (β := E) (a.im * b.re) ((ℓ : (a : ℂ) → E) I : E) +
      (a.re • HSMul.hSMul (β := E) b.im ((ℓ : (a : ℂ) → E) I : E) +
        HSMul.hSMul (β := E) (-a.im * b.im) ((ℓ : (a : ℂ) → E) 1 : E)) =
    HSMul.hSMul (β := E) (↑a.re : ℂ) ((ℓ : (a : ℂ) → E) (↑b.re : ℂ) : E) +
        HSMul.hSMul (β := E) ((↑a.im : ℂ) • I) ((ℓ : (a : ℂ) → E) (↑b.re : ℂ) : E) +
      ((↑a.re : ℂ) • HSMul.hSMul (β := E) b.im ((ℓ : (a : ℂ) → E) I : E) +
        ((↑a.im : ℂ) • I) • HSMul.hSMul (β := E) b.im ((ℓ : (a : ℂ) → E) I : E))
have t₂ : ∀ {r : ℝ}, (ℓ : (a : ℂ) → E) (↑r : ℂ) = HSMul.hSMul (β := E) r ((ℓ : (a : ℂ) → E) 1 : E)
Tactic: have t₂ {r : ℝ} : ℓ (r : ℂ) = r • ℓ (1 : ℂ) := by simp [← ℓ.map_smul]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Conformal (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
ℓ : ℂ →ₗ[ℝ] E
h : (ℓ : (a : ℂ) → E) I = HSMul.hSMul (β := E) I ((ℓ : (a : ℂ) → E) 1 : E)
a b : ℂ
t₀ : ((↑a.im : ℂ) • I) • (↑b.re : ℂ) = (↑(a.im * b.re) : ℂ) • I
t₁ : ((↑a.im : ℂ) • I) • (↑b.im : ℂ) • I = HSMul.hSMul (β := ℂ) (↑(-a.im * b.im) : ℂ) 1
t₂ : ∀ {r : ℝ}, (ℓ : (a : ℂ) → E) (↑r : ℂ) = HSMul.hSMul (β := E) r ((ℓ : (a : ℂ) → E) 1 : E)
⊢ HSMul.hSMul (β := E) a.re ((ℓ : (a : ℂ) → E) (↑b.re : ℂ) : E) +
        HSMul.hSMul (β := E) (a.im * b.re) ((ℓ : (a : ℂ) → E) I : E) +
      (a.re • HSMul.hSMul (β := E) b.im ((ℓ : (a : ℂ) → E) I : E) +
        HSMul.hSMul (β := E) (-a.im * b.im) ((ℓ : (a : ℂ) → E) 1 : E)) =
    HSMul.hSMul (β := E) (↑a.re : ℂ) ((ℓ : (a : ℂ) → E) (↑b.re : ℂ) : E) +
        HSMul.hSMul (β := E) ((↑a.im : ℂ) • I) ((ℓ : (a : ℂ) → E) (↑b.re : ℂ) : E) +
      ((↑a.re : ℂ) • HSMul.hSMul (β := E) b.im ((ℓ : (a : ℂ) → E) I : E) +
        ((↑a.im : ℂ) • I) • HSMul.hSMul (β := E) b.im ((ℓ : (a : ℂ) → E) I : E))
have simp : a.re • HSMul.hSMul (β := E) b.re ((ℓ : (a : ℂ) → E) 1 : E) +
      (a.im * b.re) • HSMul.hSMul (β := E) I ((ℓ : (a : ℂ) → E) 1 : E) +
    (a.re • b.im • HSMul.hSMul (β := E) I ((ℓ : (a : ℂ) → E) 1 : E) +
      HSMul.hSMul (β := E) (-a.im * b.im) ((ℓ : (a : ℂ) → E) 1 : E)) =
  (↑a.re : ℂ) • HSMul.hSMul (β := E) b.re ((ℓ : (a : ℂ) → E) 1 : E) +
      ((↑a.im : ℂ) • I) • HSMul.hSMul (β := E) b.re ((ℓ : (a : ℂ) → E) 1 : E) +
    ((↑a.re : ℂ) • b.im • HSMul.hSMul (β := E) I ((ℓ : (a : ℂ) → E) 1 : E) +
      ((↑a.im : ℂ) • I) • b.im • HSMul.hSMul (β := E) I ((ℓ : (a : ℂ) → E) 1 : E))
Tactic: simp only [t₂, h]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Conformal (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
ℓ : ℂ →ₗ[ℝ] E
h : (ℓ : (a : ℂ) → E) I = HSMul.hSMul (β := E) I ((ℓ : (a : ℂ) → E) 1 : E)
a b : ℂ
t₀ : ((↑a.im : ℂ) • I) • (↑b.re : ℂ) = (↑(a.im * b.re) : ℂ) • I
t₁ : ((↑a.im : ℂ) • I) • (↑b.im : ℂ) • I = HSMul.hSMul (β := ℂ) (↑(-a.im * b.im) : ℂ) 1
t₂ : ∀ {r : ℝ}, (ℓ : (a : ℂ) → E) (↑r : ℂ) = HSMul.hSMul (β := E) r ((ℓ : (a : ℂ) → E) 1 : E)
⊢ a.re • HSMul.hSMul (β := E) b.re ((ℓ : (a : ℂ) → E) 1 : E) +
        (a.im * b.re) • HSMul.hSMul (β := E) I ((ℓ : (a : ℂ) → E) 1 : E) +
      (a.re • b.im • HSMul.hSMul (β := E) I ((ℓ : (a : ℂ) → E) 1 : E) +
        HSMul.hSMul (β := E) (-a.im * b.im) ((ℓ : (a : ℂ) → E) 1 : E)) =
    (↑a.re : ℂ) • HSMul.hSMul (β := E) b.re ((ℓ : (a : ℂ) → E) 1 : E) +
        ((↑a.im : ℂ) • I) • HSMul.hSMul (β := E) b.re ((ℓ : (a : ℂ) → E) 1 : E) +
      ((↑a.re : ℂ) • b.im • HSMul.hSMul (β := E) I ((ℓ : (a : ℂ) → E) 1 : E) +
        ((↑a.im : ℂ) • I) • b.im • HSMul.hSMul (β := E) I ((ℓ : (a : ℂ) → E) 1 : E))
have match_scalars : (↑a.re : ℂ) * HMul.hMul (α := ℂ) (↑b.re : ℂ) 1 + HMul.hMul (α := ℂ) (↑a.im : ℂ) (↑b.re : ℂ) * (I * 1) +
    (HMul.hMul (α := ℂ) ((algebraMap ℝ ℂ : (a : ℝ) → ℂ) a.re : ℂ)
        (HMul.hMul (α := ℂ) ((algebraMap ℝ ℂ : (a : ℝ) → ℂ) b.im : ℂ) (I * 1)) +
      HMul.hMul (α := ℂ) (-(↑a.im : ℂ)) (↑b.im : ℂ) * 1) =
  (↑a.re : ℂ) * HMul.hMul (α := ℂ) (↑b.re : ℂ) 1 + (↑a.im : ℂ) • I * HMul.hMul (α := ℂ) (↑b.re : ℂ) 1 +
    ((↑a.re : ℂ) * HMul.hMul (α := ℂ) ((algebraMap ℝ ℂ : (a : ℝ) → ℂ) b.im : ℂ) (I * 1) +
      (↑a.im : ℂ) • I * HMul.hMul (α := ℂ) ((algebraMap ℝ ℂ : (a : ℝ) → ℂ) b.im : ℂ) (I * 1))
Tactic: match_scalars
-- Lean 4 proof step from Mathlib.Analysis.Complex.Conformal (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
ℓ : ℂ →ₗ[ℝ] E
h : (ℓ : (a : ℂ) → E) I = HSMul.hSMul (β := E) I ((ℓ : (a : ℂ) → E) 1 : E)
a b : ℂ
t₀ : ((↑a.im : ℂ) • I) • (↑b.re : ℂ) = (↑(a.im * b.re) : ℂ) • I
t₁ : ((↑a.im : ℂ) • I) • (↑b.im : ℂ) • I = HSMul.hSMul (β := ℂ) (↑(-a.im * b.im) : ℂ) 1
t₂ : ∀ {r : ℝ}, (ℓ : (a : ℂ) → E) (↑r : ℂ) = HSMul.hSMul (β := E) r ((ℓ : (a : ℂ) → E) 1 : E)
⊢ (↑a.re : ℂ) * HMul.hMul (α := ℂ) (↑b.re : ℂ) 1 + HMul.hMul (α := ℂ) (↑a.im : ℂ) (↑b.re : ℂ) * (I * 1) +
      (HMul.hMul (α := ℂ) ((algebraMap ℝ ℂ : (a : ℝ) → ℂ) a.re : ℂ)
          (HMul.hMul (α := ℂ) ((algebraMap ℝ ℂ : (a : ℝ) → ℂ) b.im : ℂ) (I * 1)) +
        HMul.hMul (α := ℂ) (-(↑a.im : ℂ)) (↑b.im : ℂ) * 1) =
    (↑a.re : ℂ) * HMul.hMul (α := ℂ) (↑b.re : ℂ) 1 + (↑a.im : ℂ) • I * HMul.hMul (α := ℂ) (↑b.re : ℂ) 1 +
      ((↑a.re : ℂ) * HMul.hMul (α := ℂ) ((algebraMap ℝ ℂ : (a : ℝ) → ℂ) b.im : ℂ) (I * 1) +
        (↑a.im : ℂ) • I * HMul.hMul (α := ℂ) ((algebraMap ℝ ℂ : (a : ℝ) → ℂ) b.im : ℂ) (I * 1))
have simp : (↑a.im : ℂ) * (↑b.re : ℂ) * I = (↑a.im : ℂ) * I * (↑b.re : ℂ)
Tactic: simp [mul_mul_mul_comm _ I]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Conformal (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
x : ℂ
s : Set ℂ
hs : UniqueDiffWithinAt ℝ s x
⊢ DifferentiableWithinAt ℂ f s x ↔
    DifferentiableWithinAt ℝ f s x ∧
      (fderivWithin ℝ f s x : (a : ℂ) → E) I = HSMul.hSMul (β := E) I ((fderivWithin ℝ f s x : (a : ℂ) → E) 1 : E)
have refine_1 : ∀ (h : DifferentiableWithinAt ℂ f s x),
  (fderivWithin ℝ f s x : (a : ℂ) → E) I = HSMul.hSMul (β := E) I ((fderivWithin ℝ f s x : (a : ℂ) → E) 1 : E)
Tactic: refine ⟨fun h ↦ ⟨h.restrictScalars ℝ, ?_⟩, fun ⟨h₁, h₂⟩ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Complex.Conformal (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
x : ℂ
s : Set ℂ
hs : UniqueDiffWithinAt ℝ s x
refine_1 :
  ∀ (h : DifferentiableWithinAt ℂ f s x),
    (fderivWithin ℝ f s x : (a : ℂ) → E) I = HSMul.hSMul (β := E) I ((fderivWithin ℝ f s x : (a : ℂ) → E) 1 : E)
⊢ DifferentiableWithinAt ℂ f s x ↔
    DifferentiableWithinAt ℝ f s x ∧
      (fderivWithin ℝ f s x : (a : ℂ) → E) I = HSMul.hSMul (β := E) I ((fderivWithin ℝ f s x : (a : ℂ) → E) 1 : E)
have refine_2 : DifferentiableWithinAt ℝ f s x ∧
    (fderivWithin ℝ f s x : (a : ℂ) → E) I = HSMul.hSMul (β := E) I ((fderivWithin ℝ f s x : (a : ℂ) → E) 1 : E) →
  ∀ (h₁ : DifferentiableWithinAt ℝ f s x)
    (h₂ : (fderivWithin ℝ f s x : (a : ℂ) → E) I = HSMul.hSMul (β := E) I ((fderivWithin ℝ f s x : (a : ℂ) → E) 1 : E)),
    DifferentiableWithinAt ℂ f s x
Tactic: refine ⟨fun h ↦ ⟨h.restrictScalars ℝ, ?_⟩, fun ⟨h₁, h₂⟩ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Complex.Conformal (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
x : ℂ
s : Set ℂ
hs : UniqueDiffWithinAt ℝ s x
h : DifferentiableWithinAt ℂ f s x
⊢ (fderivWithin ℝ f s x : (a : ℂ) → E) I = HSMul.hSMul (β := E) I ((fderivWithin ℝ f s x : (a : ℂ) → E) 1 : E)
have refine_1 : (fderivWithin ℂ f s x : (a : ℂ) → E) I = HSMul.hSMul (β := E) I ((fderivWithin ℂ f s x : (a : ℂ) → E) 1 : E)
Tactic: simp only [← h.restrictScalars_fderivWithin ℝ hs, ContinuousLinearMap.coe_restrictScalars']
-- Lean 4 proof step from Mathlib.Analysis.Complex.Conformal (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
x : ℂ
s : Set ℂ
hs : UniqueDiffWithinAt ℝ s x
h : DifferentiableWithinAt ℂ f s x
⊢ (fderivWithin ℂ f s x : (a : ℂ) → E) I = HSMul.hSMul (β := E) I ((fderivWithin ℂ f s x : (a : ℂ) → E) 1 : E)
have refine_1 : HSMul.hSMul (β := E) I ((fderivWithin ℂ f s x : (a : ℂ) → E) 1 : E) =
  HSMul.hSMul (β := E) (HSMul.hSMul (β := ℂ) I 1) ((fderivWithin ℂ f s x : (a : ℂ) → E) 1 : E)
Tactic: rw [(by simp : I = I • 1), (fderivWithin ℂ f s x).map_smul]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Conformal (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
x : ℂ
s : Set ℂ
hs : UniqueDiffWithinAt ℝ s x
h :
  DifferentiableWithinAt ℝ f s x ∧
    (fderivWithin ℝ f s x : (a : ℂ) → E) I = HSMul.hSMul (β := E) I ((fderivWithin ℝ f s x : (a : ℂ) → E) 1 : E)
h₁ : DifferentiableWithinAt ℝ f s x
h₂ : (fderivWithin ℝ f s x : (a : ℂ) → E) I = HSMul.hSMul (β := E) I ((fderivWithin ℝ f s x : (a : ℂ) → E) 1 : E)
⊢ DifferentiableWithinAt ℂ f s x
have refine_2 : ∃ (g' : ℂ →L[ℂ] E), Eq (α := ℂ →L[ℝ] E) (restrictScalars ℝ g') (fderivWithin ℝ f s x)
Tactic: apply (differentiableWithinAt_iff_restrictScalars ℝ h₁ hs).2
-- Lean 4 proof step from Mathlib.Analysis.Complex.Conformal (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
x : ℂ
s : Set ℂ
hs : UniqueDiffWithinAt ℝ s x
h :
  DifferentiableWithinAt ℝ f s x ∧
    (fderivWithin ℝ f s x : (a : ℂ) → E) I = HSMul.hSMul (β := E) I ((fderivWithin ℝ f s x : (a : ℂ) → E) 1 : E)
h₁ : DifferentiableWithinAt ℝ f s x
h₂ : (fderivWithin ℝ f s x : (a : ℂ) → E) I = HSMul.hSMul (β := E) I ((fderivWithin ℝ f s x : (a : ℂ) → E) 1 : E)
⊢ ∃ (g' : ℂ →L[ℂ] E), Eq (α := ℂ →L[ℝ] E) (restrictScalars ℝ g') (fderivWithin ℝ f s x)
have h : Eq (α := ℂ →L[ℝ] E) (restrictScalars ℝ (complexOfReal (fderivWithin ℝ f s x) h₂)) (fderivWithin ℝ f s x)
Tactic: use (fderivWithin ℝ f s x).complexOfReal h₂
-- Lean 4 proof step from Mathlib.Analysis.Complex.Conformal (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
x : ℂ
s : Set ℂ
h₁ : DifferentiableWithinAt ℝ f s x
h₂ : (fderivWithin ℝ f s x : (a : ℂ) → E) I = HSMul.hSMul (β := E) I ((fderivWithin ℝ f s x : (a : ℂ) → E) 1 : E)
hs : UniqueDiffWithinAt ℝ s x
⊢ fderivWithin ℂ f s x = complexOfReal (fderivWithin ℝ f s x) h₂
have this : Eq (α := ℂ →L[ℝ] E) (restrictScalars ℝ (fderivWithin ℂ f s x)) (fderivWithin ℝ f s x)
Tactic: have := ((differentiableWithinAt_complex_iff_differentiableWithinAt_real hs).2
      ⟨h₁, h₂⟩).restrictScalars_fderivWithin ℝ hs
-- Lean 4 proof step from Mathlib.Analysis.Complex.Conformal (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
x : ℂ
s : Set ℂ
h₁ : DifferentiableWithinAt ℝ f s x
h₂ : (fderivWithin ℝ f s x : (a : ℂ) → E) I = HSMul.hSMul (β := E) I ((fderivWithin ℝ f s x : (a : ℂ) → E) 1 : E)
⊢ HasDerivWithinAt f ((complexOfReal (fderivWithin ℝ f s x) h₂ : (a : ℂ) → E) 1) s x
have rw : HasFDerivWithinAt f (complexOfReal (fderivWithin ℝ f s x) h₂) s x
Tactic: rw [hasDerivWithinAt_iff_hasFDerivWithinAt, toSpanSingleton_apply_map_one]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Conformal (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f : ℂ → E
x : ℂ
h₁ : DifferentiableAt ℝ f x
h₂ : (fderiv ℝ f x : (a : ℂ) → E) I = HSMul.hSMul (β := E) I ((fderiv ℝ f x : (a : ℂ) → E) 1 : E)
⊢ HasDerivAt f ((complexOfReal (fderiv ℝ f x) h₂ : (a : ℂ) → E) 1) x
have rw : HasFDerivAt f (complexOfReal (fderiv ℝ f x) h₂) x
Tactic: rw [hasDerivAt_iff_hasFDerivAt, toSpanSingleton_apply_map_one]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Convex (goal)
Goal:
s t : Set ℝ
⊢ preimage (β := ℝ × ℝ) (⇑equivRealProdLm : (a : ℂ) → ℝ × ℝ)
      ((convexHull ℝ : (a : Set (ℝ × ℝ)) → Set (ℝ × ℝ)) (s ×ˢ t)) =
    (convexHull ℝ : (a : Set ℝ) → Set ℝ) s ×ℂ (convexHull ℝ : (a : Set ℝ) → Set ℝ) t
have rw : (⇑equivRealProdLm : (a : ℂ) → ℝ × ℝ) ⁻¹'
    SProd.sprod (α := Set ℝ) (β := Set ℝ) ((convexHull ℝ : (a : Set ℝ) → Set ℝ) s : Set ℝ)
      ((convexHull ℝ : (a : Set ℝ) → Set ℝ) t : Set ℝ) =
  (convexHull ℝ : (a : Set ℝ) → Set ℝ) s ×ℂ (convexHull ℝ : (a : Set ℝ) → Set ℝ) t
Tactic: rw [convexHull_prod]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Convex (goal)
Goal:
r : ℝ
s : Set ℂ
hs₁ : {z : ℂ | r < z.im} ⊆ s
hs₂ : s ⊆ {z : ℂ | r ≤ z.im}
⊢ IsConnected s
have refine : IsConnected (α := ℂ) {z : ℂ | r < z.im}
Tactic: refine .subset_closure ?_ hs₁ (by simpa only [closure_setOf_lt_im] using hs₂)
-- Lean 4 proof step from Mathlib.Analysis.Complex.Convex (goal)
Goal:
r : ℝ
s : Set ℂ
hs₁ : {z : ℂ | z.im < r} ⊆ s
hs₂ : s ⊆ {z : ℂ | z.im ≤ r}
⊢ IsConnected s
have refine : IsConnected (α := ℂ) {z : ℂ | z.im < r}
Tactic: refine .subset_closure ?_ hs₁ (by simpa only [closure_setOf_im_lt] using hs₂)
-- Lean 4 proof step from Mathlib.Analysis.Complex.Convex (goal)
Goal:
z w : ℂ
⊢ z.Rectangle w =
    (convexHull ℝ : (a : Set ℂ) → Set ℂ) {z, (↑z.re : ℂ) + (↑w.im : ℂ) * I, (↑w.re : ℂ) + (↑z.im : ℂ) * I, w}
have simp_rw : uIcc z.re w.re ×ℂ uIcc z.im w.im =
  (convexHull ℝ : (a : Set ℂ) → Set ℂ) {z, (↑z.re : ℂ) + (↑w.im : ℂ) * I, (↑w.re : ℂ) + (↑z.im : ℂ) * I, w}
Tactic: simp_rw [Rectangle, ← segment_eq_uIcc, ← convexHull_pair, ← convexHull_reProdIm,
    ← preimage_equivRealProd_prod, insert_prod, singleton_prod, image_pair, insert_union,
    ← insert_eq, ← Equiv.image_symm_eq_preimage, image_insert_eq, image_singleton,
    equivRealProd_symm_apply, re_add_im]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Convex (goal)
Goal:
z w : ℂ
simp_rw :
  uIcc z.re w.re ×ℂ uIcc z.im w.im =
    (convexHull ℝ : (a : Set ℂ) → Set ℂ) {z, (↑z.re : ℂ) + (↑w.im : ℂ) * I, (↑w.re : ℂ) + (↑z.im : ℂ) * I, w}
⊢ z.Rectangle w =
    (convexHull ℝ : (a : Set ℂ) → Set ℂ) {z, (↑z.re : ℂ) + (↑w.im : ℂ) * I, (↑w.re : ℂ) + (↑z.im : ℂ) * I, w}
have simp_rw₁ : segment ℝ z.re w.re ×ℂ segment ℝ z.im w.im =
  (convexHull ℝ : (a : Set ℂ) → Set ℂ) {z, (↑z.re : ℂ) + (↑w.im : ℂ) * I, (↑w.re : ℂ) + (↑z.im : ℂ) * I, w}
Tactic: simp_rw [Rectangle, ← segment_eq_uIcc, ← convexHull_pair, ← convexHull_reProdIm,
    ← preimage_equivRealProd_prod, insert_prod, singleton_prod, image_pair, insert_union,
    ← insert_eq, ← Equiv.image_symm_eq_preimage, image_insert_eq, image_singleton,
    equivRealProd_symm_apply, re_add_im]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Convex (goal)
Goal:
z w : ℂ
simp_rw :
  uIcc z.re w.re ×ℂ uIcc z.im w.im =
    (convexHull ℝ : (a : Set ℂ) → Set ℂ) {z, (↑z.re : ℂ) + (↑w.im : ℂ) * I, (↑w.re : ℂ) + (↑z.im : ℂ) * I, w}
simp_rw₁ :
  segment ℝ z.re w.re ×ℂ segment ℝ z.im w.im =
    (convexHull ℝ : (a : Set ℂ) → Set ℂ) {z, (↑z.re : ℂ) + (↑w.im : ℂ) * I, (↑w.re : ℂ) + (↑z.im : ℂ) * I, w}
⊢ z.Rectangle w =
    (convexHull ℝ : (a : Set ℂ) → Set ℂ) {z, (↑z.re : ℂ) + (↑w.im : ℂ) * I, (↑w.re : ℂ) + (↑z.im : ℂ) * I, w}
have simp_rw₂ : (convexHull ℝ : (a : Set ℝ) → Set ℝ) {z.re, w.re} ×ℂ (convexHull ℝ : (a : Set ℝ) → Set ℝ) {z.im, w.im} =
  (convexHull ℝ : (a : Set ℂ) → Set ℂ) {z, (↑z.re : ℂ) + (↑w.im : ℂ) * I, (↑w.re : ℂ) + (↑z.im : ℂ) * I, w}
Tactic: simp_rw [Rectangle, ← segment_eq_uIcc, ← convexHull_pair, ← convexHull_reProdIm,
    ← preimage_equivRealProd_prod, insert_prod, singleton_prod, image_pair, insert_union,
    ← insert_eq, ← Equiv.image_symm_eq_preimage, image_insert_eq, image_singleton,
    equivRealProd_symm_apply, re_add_im]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Convex (goal)
Goal:
z w : ℂ
simp_rw :
  uIcc z.re w.re ×ℂ uIcc z.im w.im =
    (convexHull ℝ : (a : Set ℂ) → Set ℂ) {z, (↑z.re : ℂ) + (↑w.im : ℂ) * I, (↑w.re : ℂ) + (↑z.im : ℂ) * I, w}
simp_rw₁ :
  segment ℝ z.re w.re ×ℂ segment ℝ z.im w.im =
    (convexHull ℝ : (a : Set ℂ) → Set ℂ) {z, (↑z.re : ℂ) + (↑w.im : ℂ) * I, (↑w.re : ℂ) + (↑z.im : ℂ) * I, w}
simp_rw₂ :
  (convexHull ℝ : (a : Set ℝ) → Set ℝ) {z.re, w.re} ×ℂ (convexHull ℝ : (a : Set ℝ) → Set ℝ) {z.im, w.im} =
    (convexHull ℝ : (a : Set ℂ) → Set ℂ) {z, (↑z.re : ℂ) + (↑w.im : ℂ) * I, (↑w.re : ℂ) + (↑z.im : ℂ) * I, w}
⊢ z.Rectangle w =
    (convexHull ℝ : (a : Set ℂ) → Set ℂ) {z, (↑z.re : ℂ) + (↑w.im : ℂ) * I, (↑w.re : ℂ) + (↑z.im : ℂ) * I, w}
have simp_rw₃ : Eq (α := Set ℂ) ((convexHull ℝ : (a : Set ℂ) → Set ℂ) ({z.re, w.re} ×ℂ {z.im, w.im}) : Set ℂ)
  ((convexHull ℝ : (a : Set ℂ) → Set ℂ) {z, (↑z.re : ℂ) + (↑w.im : ℂ) * I, (↑w.re : ℂ) + (↑z.im : ℂ) * I, w} : Set ℂ)
Tactic: simp_rw [Rectangle, ← segment_eq_uIcc, ← convexHull_pair, ← convexHull_reProdIm,
    ← preimage_equivRealProd_prod, insert_prod, singleton_prod, image_pair, insert_union,
    ← insert_eq, ← Equiv.image_symm_eq_preimage, image_insert_eq, image_singleton,
    equivRealProd_symm_apply, re_add_im]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Convex (goal)
Goal:
z w : ℂ
simp_rw :
  uIcc z.re w.re ×ℂ uIcc z.im w.im =
    (convexHull ℝ : (a : Set ℂ) → Set ℂ) {z, (↑z.re : ℂ) + (↑w.im : ℂ) * I, (↑w.re : ℂ) + (↑z.im : ℂ) * I, w}
simp_rw₁ :
  segment ℝ z.re w.re ×ℂ segment ℝ z.im w.im =
    (convexHull ℝ : (a : Set ℂ) → Set ℂ) {z, (↑z.re : ℂ) + (↑w.im : ℂ) * I, (↑w.re : ℂ) + (↑z.im : ℂ) * I, w}
simp_rw₂ :
  (convexHull ℝ : (a : Set ℝ) → Set ℝ) {z.re, w.re} ×ℂ (convexHull ℝ : (a : Set ℝ) → Set ℝ) {z.im, w.im} =
    (convexHull ℝ : (a : Set ℂ) → Set ℂ) {z, (↑z.re : ℂ) + (↑w.im : ℂ) * I, (↑w.re : ℂ) + (↑z.im : ℂ) * I, w}
simp_rw₃ :
  Eq (α := Set ℂ) ((convexHull ℝ : (a : Set ℂ) → Set ℂ) ({z.re, w.re} ×ℂ {z.im, w.im}) : Set ℂ)
    ((convexHull ℝ : (a : Set ℂ) → Set ℂ) {z, (↑z.re : ℂ) + (↑w.im : ℂ) * I, (↑w.re : ℂ) + (↑z.im : ℂ) * I, w} : Set ℂ)
⊢ z.Rectangle w =
    (convexHull ℝ : (a : Set ℂ) → Set ℂ) {z, (↑z.re : ℂ) + (↑w.im : ℂ) * I, (↑w.re : ℂ) + (↑z.im : ℂ) * I, w}
have simp_rw₄ : Eq (α := Set ℂ)
  ((convexHull ℝ : (a : Set ℂ) → Set ℂ)
      ((⇑equivRealProd : (a : ℂ) → ℝ × ℝ) ⁻¹' SProd.sprod (α := Set ℝ) (β := Set ℝ) {z.re, w.re} {z.im, w.im}) :
    Set ℂ)
  ((convexHull ℝ : (a : Set ℂ) → Set ℂ) {z, (↑z.re : ℂ) + (↑w.im : ℂ) * I, (↑w.re : ℂ) + (↑z.im : ℂ) * I, w} : Set ℂ)
Tactic: simp_rw [Rectangle, ← segment_eq_uIcc, ← convexHull_pair, ← convexHull_reProdIm,
    ← preimage_equivRealProd_prod, insert_prod, singleton_prod, image_pair, insert_union,
    ← insert_eq, ← Equiv.image_symm_eq_preimage, image_insert_eq, image_singleton,
    equivRealProd_symm_apply, re_add_im]