awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Complex.Conformal
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 : ℂ
rw :
  (ℓ : (a : ℂ) → E) (((↑a.re : ℂ) + (↑a.im : ℂ) • I) • ((↑b.re : ℂ) + (↑b.im : ℂ) • I)) =
    HSMul.hSMul (β := E) ((↑a.re : ℂ) + (↑a.im : ℂ) • I) ((ℓ : (a : ℂ) → E) ((↑b.re : ℂ) + (↑b.im : ℂ) • I) : E)
⊢ (ℓ : (a : ℂ) → E) (a • b) = HSMul.hSMul (β := E) a ((ℓ : (a : ℂ) → E) b : E)

Tactic:
rw [← re_add_im a, ← re_add_im b, ← smul_eq_mul _ I, ← smul_eq_mul _ I]

Premises used: smul_eq_mul, Complex.re_add_im, Complex.I
-- Module: Mathlib.Analysis.Complex.Conformal
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 : ℂ
⊢ ((↑a.im : ℂ) • I) • (↑b.re : ℂ) = (↑(a.im * b.re) : ℂ) • I

Tactic:
simp only [smul_eq_mul, ofReal_mul, ← mul_assoc, mul_comm _ I]

Premises used: mul_assoc, mul_comm, smul_eq_mul, Complex.ofReal_mul, Complex.I
-- Module: Mathlib.Analysis.Complex.Conformal
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 : ℂ
⊢ ((↑a.im : ℂ) • I) • (↑b.re : ℂ) = (↑(a.im * b.re) : ℂ) • I

Tactic:
have t₀ : ((a.im : ℂ) • I) • (b.re : ℂ) = (↑(a.im * b.re) : ℂ) • I := by
    simp only [smul_eq_mul, ofReal_mul, ← mul_assoc, mul_comm _ I]
-- Module: Mathlib.Analysis.Complex.Conformal
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
⊢ ((↑a.im : ℂ) • I) • (↑b.im : ℂ) • I = HSMul.hSMul (β := ℂ) (↑(-a.im * b.im) : ℂ) 1

Tactic:
simp [mul_mul_mul_comm _ I]

Premises used: mul_mul_mul_comm, Complex.I
-- Module: Mathlib.Analysis.Complex.Conformal
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
⊢ ((↑a.im : ℂ) • I) • (↑b.im : ℂ) • I = HSMul.hSMul (β := ℂ) (↑(-a.im * b.im) : ℂ) 1

Tactic:
have t₁ : ((a.im : ℂ) • I) • (b.im : ℂ) • I = (↑(- a.im * b.im) : ℂ) • (1 : ℂ) := by
    simp [mul_mul_mul_comm _ I]
-- Module: Mathlib.Analysis.Complex.Conformal
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
simp :
  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))
⊢ (ℓ : (a : ℂ) → E) (((↑a.re : ℂ) + (↑a.im : ℂ) • I) • ((↑b.re : ℂ) + (↑b.im : ℂ) • I)) =
    HSMul.hSMul (β := E) ((↑a.re : ℂ) + (↑a.im : ℂ) • I) ((ℓ : (a : ℂ) → E) ((↑b.re : ℂ) + (↑b.im : ℂ) • I) : E)

Tactic:
simp only [add_smul, smul_add, ℓ.map_add, t₀, t₁]

Premises used: LinearMap.map_add, add_smul, smul_add
-- Module: Mathlib.Analysis.Complex.Conformal
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
rw :
  HAdd.hAdd (β := E) (HSMul.hSMul (β := E) a.re ((ℓ : (a : ℂ) → E) (↑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))
⊢ 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))

Tactic:
rw [Complex.coe_smul, ℓ.map_smul]

Premises used: Complex.coe_smul, LinearMap.map_smul
-- Module: Mathlib.Analysis.Complex.Conformal
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
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) (β := 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))
⊢ HAdd.hAdd (β := E) (HSMul.hSMul (β := E) a.re ((ℓ : (a : ℂ) → E) (↑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))

Tactic:
rw [Complex.coe_smul, ℓ.map_smul]

Premises used: Complex.coe_smul, LinearMap.map_smul
-- Module: Mathlib.Analysis.Complex.Conformal
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
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) (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))
⊢ HSMul.hSMul (β := E) a.re ((ℓ : (a : ℂ) → E) (↑b.re : ℂ) : E) +
        HSMul.hSMul (β := E) (a.im * b.re) ((ℓ : (a : ℂ) → E) 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))

Tactic:
rw [Complex.coe_smul, ℓ.map_smul]

Premises used: Complex.coe_smul, LinearMap.map_smul
-- Module: Mathlib.Analysis.Complex.Conformal
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
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))
⊢ 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))

Tactic:
rw [Complex.coe_smul, ℓ.map_smul]

Premises used: Complex.coe_smul, LinearMap.map_smul
-- Module: Mathlib.Analysis.Complex.Conformal
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
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))
⊢ 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]

Premises used: Complex.coe_smul, LinearMap.map_smul
-- Module: Mathlib.Analysis.Complex.Conformal
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
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))
⊢ 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))

Tactic:
repeat rw [Complex.coe_smul, ℓ.map_smul]

Premises used: Complex.coe_smul, LinearMap.map_smul
-- Module: Mathlib.Analysis.Complex.Conformal
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
r : ℝ
⊢ (ℓ : (a : ℂ) → E) (↑r : ℂ) = HSMul.hSMul (β := E) r ((ℓ : (a : ℂ) → E) 1 : E)

Tactic:
simp [← ℓ.map_smul]

Premises used: LinearMap.map_smul
-- Module: Mathlib.Analysis.Complex.Conformal
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
⊢ ∀ {r : ℝ}, (ℓ : (a : ℂ) → E) (↑r : ℂ) = HSMul.hSMul (β := E) r ((ℓ : (a : ℂ) → E) 1 : E)

Tactic:
have t₂ {r : ℝ} : ℓ (r : ℂ) = r • ℓ (1 : ℂ) := by simp [← ℓ.map_smul]
-- Module: Mathlib.Analysis.Complex.Conformal
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)
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))
⊢ 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:
simp only [t₂, h]
-- Module: Mathlib.Analysis.Complex.Conformal
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)
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))
⊢ 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:
match_scalars
-- Module: Mathlib.Analysis.Complex.Conformal
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)
simp : (↑a.im : ℂ) * (↑b.re : ℂ) * I = (↑a.im : ℂ) * I * (↑b.re : ℂ)
⊢ (↑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:
simp [mul_mul_mul_comm _ I]

Premises used: mul_mul_mul_comm, Complex.I
-- Module: Mathlib.Analysis.Complex.Conformal
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.im : ℂ) * (↑b.re : ℂ) * I = (↑a.im : ℂ) * I * (↑b.re : ℂ)

Tactic:
ring
-- Module: Mathlib.Analysis.Complex.Conformal
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)
⊢ Eq (α := (a : ℂ) → E) (⇑(ℓ.complexOfReal h) : (a : ℂ) → E) (⇑ℓ : (a : ℂ) → E)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Complex.Conformal
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
ℓ : ℂ →L[ℝ] E
h : (ℓ : (a : ℂ) → E) I = HSMul.hSMul (β := E) I ((ℓ : (a : ℂ) → E) 1 : E)
⊢ Eq (α := (a : ℂ) → E) (⇑(ℓ.complexOfReal h) : (a : ℂ) → E) (⇑ℓ : (a : ℂ) → E)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.Complex.Conformal
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)

Tactic:
⟨fun h ↦ ⟨h.restrictScalars ℝ, ?_⟩, fun ⟨h₁, h₂⟩ ↦ ?_⟩

Premises used: Real, DifferentiableWithinAt.restrictScalars, And.intro, Iff.intro, _private.0.differentiableWithinAt_complex_iff_differentiableWithinAt_real.match_1, DifferentiableWithinAt, Complex
-- Module: Mathlib.Analysis.Complex.Conformal
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)
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
⊢ 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)

Tactic:
refine ⟨fun h ↦ ⟨h.restrictScalars ℝ, ?_⟩, fun ⟨h₁, h₂⟩ ↦ ?_⟩
-- Module: Mathlib.Analysis.Complex.Conformal
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
refine_1 : (fderivWithin ℂ f s x : (a : ℂ) → E) I = HSMul.hSMul (β := E) I ((fderivWithin ℂ f s x : (a : ℂ) → E) 1 : E)
⊢ (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']

Premises used: Real, DifferentiableWithinAt.restrictScalars_fderivWithin, ContinuousLinearMap.coe_restrictScalars'
-- Module: Mathlib.Analysis.Complex.Conformal
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
⊢ I = HSMul.hSMul (β := ℂ) I 1

Tactic:
simp
-- Module: Mathlib.Analysis.Complex.Conformal
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
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)
⊢ (fderivWithin ℂ f s x : (a : ℂ) → E) I = HSMul.hSMul (β := E) I ((fderivWithin ℂ f s x : (a : ℂ) → E) 1 : E)

Tactic:
rw [(by simp : I = I • 1), (fderivWithin ℂ f s x).map_smul]

Premises used: fderivWithin, Complex, ContinuousLinearMap.map_smul