awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Complex.Module
Goal:
⊢ Eq (α := ℝ)
    ((((basisOneI.repr : (a : ℂ) → Fin 2 →₀ ℝ) (![1, I] ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩)) : Fin 2 →₀ ℝ) : (a : Fin 2) → ℝ)
        ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) :
      ℝ)
    ((Finsupp.single ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) 1 : (a : Fin 2) → ℝ) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) : ℝ)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Complex.Module
Goal:
⊢ Eq (α := Algebra ℝ (ℂ × ℂ)) (Prod.algebra ℝ ℂ ℂ) Algebra.complexToReal

Tactic:
rfl

Premises used: RingHom.prod, rfl
-- Module: Mathlib.LinearAlgebra.Complex.Module
Goal:
ι : Type u_1
inst : Fintype ι
⊢ Eq (α := Algebra ℝ ((i : ι) → ℂ)) (Pi.algebra ι fun (x : ι) ↦ ℂ) Algebra.complexToReal

Tactic:
rfl

Premises used: Pi.ringHom, rfl
-- Module: Mathlib.LinearAlgebra.Complex.Module
Goal:
A : Type u_1
inst_1 : Ring A
inst : Algebra ℂ A
⊢ Eq.{u_1 + 1} (α := Module ℝ A) Algebra.toModule (Module.complexToReal A)

Tactic:
rfl
-- Module: Mathlib.LinearAlgebra.Complex.Module
Goal:
A : Type u_1
inst_1 : Ring A
inst : Algebra ℂ A
⊢ Eq.{u_1 + 1} (α := Module ℝ A) Algebra.toModule (Module.complexToReal A)

Tactic:
with_reducible_and_instances rfl
-- Module: Mathlib.LinearAlgebra.Complex.Module
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℂ E
x : ℝ
y : E
⊢ (↑x : ℂ) • y = x • y

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.Complex.Module
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℂ E
⊢ IsScalarTower ℝ ℂ E

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.LinearAlgebra.Complex.Module
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Star E
inst_2 : Module ℂ E
inst_3 : StarModule ℂ E
r : ℝ
a : E
rw : star (HSMul.hSMul (β := ℂ) r 1 • a) = star r • star a
rw₁ : star (HSMul.hSMul (β := ℂ) r 1) • star a = star r • star a
rw₂ : HSMul.hSMul (β := ℂ) (star r) (star 1) • star a = star r • star a
rw₃ : HSMul.hSMul (β := ℂ) (star r) 1 • star a = star r • star a
rw₄ rw₅ : star r • star a = star r • star a
⊢ star (r • a) = star r • star a

Tactic:
rw [← smul_one_smul ℂ r a, star_smul, star_smul, star_one, smul_one_smul]

Premises used: StarModule.star_smul, smul_one_smul, Complex, star_one
-- Module: Mathlib.LinearAlgebra.Complex.Module
Goal:
⊢ ∀ (m : ℝ) (x : ℂ), (m • x).re = HSMul.hSMul (α := ℝ) ((RingHom.id ℝ : (a : ℝ) → ℝ) m : ℝ) x.re

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Complex.Module
Goal:
⊢ (⇑reLm : (a : ℂ) → ℝ) = re

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.Complex.Module
Goal:
⊢ ∀ (m : ℝ) (x : ℂ), (m • x).im = HSMul.hSMul (α := ℝ) ((RingHom.id ℝ : (a : ℝ) → ℝ) m : ℝ) x.im

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Complex.Module
Goal:
⊢ (⇑imLm : (a : ℂ) → ℝ) = im

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.Complex.Module
Goal:
⊢ (⇑ofRealAm : (a : ℝ) → ℂ) = ofReal

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.Complex.Module
Goal:
⊢ Eq (α := (a : ℂ) → ℂ) (⇑conjAe : (a : ℂ) → ℂ) (⇑(starRingEnd ℂ) : (a : ℂ) → ℂ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.Complex.Module
Goal:
a :
  ∀ (i j : Fin 2),
    Eq (α := ℝ)
      ((LinearMap.toMatrix basisOneI basisOneI : (a : ℂ →ₗ[ℝ] ℂ) → Matrix (Fin 2) (Fin 2) ℝ)
          (↑(↑conjAe : ℂ ≃ₗ[ℝ] ℂ) : ℂ →ₗ[ℝ] ℂ) i j :
        ℝ)
      (!![1, 0; 0, -1] i j : ℝ)
⊢ Eq (α := Matrix (Fin 2) (Fin 2) ℝ)
    ((LinearMap.toMatrix basisOneI basisOneI : (a : ℂ →ₗ[ℝ] ℂ) → Matrix (Fin 2) (Fin 2) ℝ)
        (↑(↑conjAe : ℂ ≃ₗ[ℝ] ℂ) : ℂ →ₗ[ℝ] ℂ) :
      Matrix (Fin 2) (Fin 2) ℝ)
    (!![1, 0; 0, -1] : Matrix (Fin 2) (Fin 2) ℝ)

Tactic:
ext i j
-- Module: Mathlib.LinearAlgebra.Complex.Module
Goal:
i j : Fin 2
a :
  Eq (α := ℝ)
    ((LinearMap.toMatrix basisOneI basisOneI : (a : ℂ →ₗ[ℝ] ℂ) → Matrix (Fin 2) (Fin 2) ℝ)
        (↑(↑conjAe : ℂ ≃ₗ[ℝ] ℂ) : ℂ →ₗ[ℝ] ℂ) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) j :
      ℝ)
    (!![1, 0; 0, -1] ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) j : ℝ)
a₁ :
  Eq (α := ℝ)
    ((LinearMap.toMatrix basisOneI basisOneI : (a : ℂ →ₗ[ℝ] ℂ) → Matrix (Fin 2) (Fin 2) ℝ)
        (↑(↑conjAe : ℂ ≃ₗ[ℝ] ℂ) : ℂ →ₗ[ℝ] ℂ) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) j :
      ℝ)
    (!![1, 0; 0, -1] ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) j : ℝ)
⊢ Eq (α := ℝ)
    ((LinearMap.toMatrix basisOneI basisOneI : (a : ℂ →ₗ[ℝ] ℂ) → Matrix (Fin 2) (Fin 2) ℝ)
        (↑(↑conjAe : ℂ ≃ₗ[ℝ] ℂ) : ℂ →ₗ[ℝ] ℂ) i j :
      ℝ)
    (!![1, 0; 0, -1] i j : ℝ)

Tactic:
fin_cases i
-- Module: Mathlib.LinearAlgebra.Complex.Module
Goal:
j : Fin 2
a :
  Eq (α := ℝ)
    ((LinearMap.toMatrix basisOneI basisOneI : (a : ℂ →ₗ[ℝ] ℂ) → Matrix (Fin 2) (Fin 2) ℝ)
        (↑(↑conjAe : ℂ ≃ₗ[ℝ] ℂ) : ℂ →ₗ[ℝ] ℂ) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) :
      ℝ)
    (!![1, 0; 0, -1] ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) : ℝ)
a₁ :
  Eq (α := ℝ)
    ((LinearMap.toMatrix basisOneI basisOneI : (a : ℂ →ₗ[ℝ] ℂ) → Matrix (Fin 2) (Fin 2) ℝ)
        (↑(↑conjAe : ℂ ≃ₗ[ℝ] ℂ) : ℂ →ₗ[ℝ] ℂ) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) :
      ℝ)
    (!![1, 0; 0, -1] ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) : ℝ)
⊢ Eq (α := ℝ)
    ((LinearMap.toMatrix basisOneI basisOneI : (a : ℂ →ₗ[ℝ] ℂ) → Matrix (Fin 2) (Fin 2) ℝ)
        (↑(↑conjAe : ℂ ≃ₗ[ℝ] ℂ) : ℂ →ₗ[ℝ] ℂ) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) j :
      ℝ)
    (!![1, 0; 0, -1] ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) j : ℝ)

Tactic:
fin_cases j
-- Module: Mathlib.LinearAlgebra.Complex.Module
Goal:
j : Fin 2
a :
  Eq (α := ℝ)
    ((LinearMap.toMatrix basisOneI basisOneI : (a : ℂ →ₗ[ℝ] ℂ) → Matrix (Fin 2) (Fin 2) ℝ)
        (↑(↑conjAe : ℂ ≃ₗ[ℝ] ℂ) : ℂ →ₗ[ℝ] ℂ) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) :
      ℝ)
    (!![1, 0; 0, -1] ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) : ℝ)
a₁ :
  Eq (α := ℝ)
    ((LinearMap.toMatrix basisOneI basisOneI : (a : ℂ →ₗ[ℝ] ℂ) → Matrix (Fin 2) (Fin 2) ℝ)
        (↑(↑conjAe : ℂ ≃ₗ[ℝ] ℂ) : ℂ →ₗ[ℝ] ℂ) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) :
      ℝ)
    (!![1, 0; 0, -1] ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) : ℝ)
⊢ Eq (α := ℝ)
    ((LinearMap.toMatrix basisOneI basisOneI : (a : ℂ →ₗ[ℝ] ℂ) → Matrix (Fin 2) (Fin 2) ℝ)
        (↑(↑conjAe : ℂ ≃ₗ[ℝ] ℂ) : ℂ →ₗ[ℝ] ℂ) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) j :
      ℝ)
    (!![1, 0; 0, -1] ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) j : ℝ)

Tactic:
fin_cases j
-- Module: Mathlib.LinearAlgebra.Complex.Module
Goal:
⊢ Eq (α := ℝ)
    ((LinearMap.toMatrix basisOneI basisOneI : (a : ℂ →ₗ[ℝ] ℂ) → Matrix (Fin 2) (Fin 2) ℝ)
        (↑(↑conjAe : ℂ ≃ₗ[ℝ] ℂ) : ℂ →ₗ[ℝ] ℂ) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) :
      ℝ)
    (!![1, 0; 0, -1] ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) : ℝ)

Tactic:
simp [LinearMap.toMatrix_apply]

Premises used: LinearMap.toMatrix_apply
-- Module: Mathlib.LinearAlgebra.Complex.Module
Goal:
⊢ Eq (α := ℝ)
    ((LinearMap.toMatrix basisOneI basisOneI : (a : ℂ →ₗ[ℝ] ℂ) → Matrix (Fin 2) (Fin 2) ℝ)
        (↑(↑conjAe : ℂ ≃ₗ[ℝ] ℂ) : ℂ →ₗ[ℝ] ℂ) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) :
      ℝ)
    (!![1, 0; 0, -1] ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) : ℝ)

Tactic:
simp [LinearMap.toMatrix_apply]

Premises used: LinearMap.toMatrix_apply
-- Module: Mathlib.LinearAlgebra.Complex.Module
Goal:
⊢ Eq (α := ℝ)
    ((LinearMap.toMatrix basisOneI basisOneI : (a : ℂ →ₗ[ℝ] ℂ) → Matrix (Fin 2) (Fin 2) ℝ)
        (↑(↑conjAe : ℂ ≃ₗ[ℝ] ℂ) : ℂ →ₗ[ℝ] ℂ) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) :
      ℝ)
    (!![1, 0; 0, -1] ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) : ℝ)

Tactic:
simp [LinearMap.toMatrix_apply]

Premises used: LinearMap.toMatrix_apply
-- Module: Mathlib.LinearAlgebra.Complex.Module
Goal:
⊢ Eq (α := ℝ)
    ((LinearMap.toMatrix basisOneI basisOneI : (a : ℂ →ₗ[ℝ] ℂ) → Matrix (Fin 2) (Fin 2) ℝ)
        (↑(↑conjAe : ℂ ≃ₗ[ℝ] ℂ) : ℂ →ₗ[ℝ] ℂ) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) :
      ℝ)
    (!![1, 0; 0, -1] ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) : ℝ)

Tactic:
simp [LinearMap.toMatrix_apply]

Premises used: LinearMap.toMatrix_apply
-- Module: Mathlib.LinearAlgebra.Complex.Module
Goal:
f : ℂ →ₐ[ℝ] ℂ
rw : (f : (a : ℂ) → ℂ) (HPow.hPow (β := ℕ) I 2) = HPow.hPow (β := ℕ) I 2
rw₁ : Eq (α := ℂ) ((f : (a : ℂ) → ℂ) (-1) : ℂ) (-1 : ℂ)
rw₂ : Eq (α := ℂ) (-(f : (a : ℂ) → ℂ) 1 : ℂ) (-1 : ℂ)
rw₃ rw₄ : Eq (α := ℂ) (-1) (-1)
⊢ HPow.hPow (α := ℂ) (β := ℕ) ((f : (a : ℂ) → ℂ) I : ℂ) 2 = HPow.hPow (β := ℕ) I 2

Tactic:
rw [← map_pow, I_sq, map_neg, map_one]

Premises used: map_neg, map_pow, map_one, Complex.I_sq
-- Module: Mathlib.LinearAlgebra.Complex.Module
Goal:
f : ℂ →ₐ[ℝ] ℂ
refine_1 : (f : (a : ℂ) → ℂ) I = I → f = AlgHom.id ℝ ℂ
refine_2 : (f : (a : ℂ) → ℂ) I = -I → f = (↑conjAe : ℂ →ₐ[ℝ] ℂ)
⊢ f = AlgHom.id ℝ ℂ ∨ f = (↑conjAe : ℂ →ₐ[ℝ] ℂ)

Tactic:
refine
      (eq_or_eq_neg_of_sq_eq_sq (f I) I <| by rw [← map_pow, I_sq, map_neg, map_one]).imp ?_ ?_

Premises used: eq_or_eq_neg_of_sq_eq_sq, Or.imp, DFunLike.coe, Complex.I
-- Module: Mathlib.LinearAlgebra.Complex.Module
Goal:
f : ℂ →ₐ[ℝ] ℂ
⊢ (f : (a : ℂ) → ℂ) I = I → f = AlgHom.id ℝ ℂ

Tactic:
fun h => algHom_ext ?_

Premises used: Complex.algHom_ext
-- Module: Mathlib.LinearAlgebra.Complex.Module
Goal:
f : ℂ →ₐ[ℝ] ℂ
refine_1 : ∀ (h : (f : (a : ℂ) → ℂ) I = I), Eq (α := ℂ) ((f : (a : ℂ) → ℂ) I : ℂ) ((AlgHom.id ℝ ℂ : (a : ℂ) → ℂ) I : ℂ)
⊢ (f : (a : ℂ) → ℂ) I = I → f = AlgHom.id ℝ ℂ

Tactic:
refine fun h => algHom_ext ?_

Premises used: Complex.algHom_ext
-- Module: Mathlib.LinearAlgebra.Complex.Module
Goal:
f : ℂ →ₐ[ℝ] ℂ
⊢ (f : (a : ℂ) → ℂ) I = -I → f = (↑conjAe : ℂ →ₐ[ℝ] ℂ)

Tactic:
fun h => algHom_ext ?_

Premises used: Complex.algHom_ext
-- Module: Mathlib.LinearAlgebra.Complex.Module
Goal:
f : ℂ →ₐ[ℝ] ℂ
refine_2 :
  ∀ (h : (f : (a : ℂ) → ℂ) I = -I), Eq (α := ℂ) ((f : (a : ℂ) → ℂ) I : ℂ) (((↑conjAe : ℂ →ₐ[ℝ] ℂ) : (a : ℂ) → ℂ) I : ℂ)
⊢ (f : (a : ℂ) → ℂ) I = -I → f = (↑conjAe : ℂ →ₐ[ℝ] ℂ)

Tactic:
refine fun h => algHom_ext ?_

Premises used: Complex.algHom_ext
-- Module: Mathlib.LinearAlgebra.Complex.Module
Goal:
f : ℂ →ₐ[ℝ] ℂ
h : (f : (a : ℂ) → ℂ) I = I
⊢ Eq (α := ℂ) ((f : (a : ℂ) → ℂ) I : ℂ) ((AlgHom.id ℝ ℂ : (a : ℂ) → ℂ) I : ℂ)

Tactic:
h

Premises used: Complex.I
-- Module: Mathlib.LinearAlgebra.Complex.Module
Goal:
f : ℂ →ₐ[ℝ] ℂ
h : (f : (a : ℂ) → ℂ) I = -I
⊢ Eq (α := ℂ) ((f : (a : ℂ) → ℂ) I : ℂ) (((↑conjAe : ℂ →ₐ[ℝ] ℂ) : (a : ℂ) → ℂ) I : ℂ)

Tactic:
conj_I.symm ▸ h

Premises used: Eq.rec, Eq.symm, Complex.conj_I
-- Module: Mathlib.LinearAlgebra.Complex.Module
Goal:
f : ℂ →ₐ[ℝ] ℂ
h : (f : (a : ℂ) → ℂ) I = I
⊢ Eq (α := ℂ) ((f : (a : ℂ) → ℂ) I : ℂ) ((AlgHom.id ℝ ℂ : (a : ℂ) → ℂ) I : ℂ)

Tactic:
exacts [h, conj_I.symm ▸ h]
-- Module: Mathlib.LinearAlgebra.Complex.Module
Goal:
r : ℝ
c : ℂ
⊢ equivRealProdAddHom.toFun (r • c) =
    HSMul.hSMul (α := ℝ) ((RingHom.id ℝ : (a : ℝ) → ℝ) r : ℝ) (equivRealProdAddHom.toFun c)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Complex.Module
Goal:
p : ℝ × ℝ
⊢ (equivRealProdLm.symm : (a : ℝ × ℝ) → ℂ) p = (↑p.1 : ℂ) + (↑p.2 : ℂ) * I

Tactic:
Complex.equivRealProd_symm_apply p

Premises used: Complex.equivRealProd_symm_apply
-- Module: Mathlib.LinearAlgebra.Complex.Module
Goal:
A : Type u_1
inst : Ring A
inst_1 : Algebra ℝ A
I' : A
hf : I' * I' = -1
rw : 1 + HSMul.hSMul (α := ℝ) 0 I' = 1
rw₁ : HAdd.hAdd (α := A) 1 0 = 1
rw₂ rw₃ : Eq.{u_1 + 1} (α := A) 1 1
⊢ HAdd.hAdd (α := A) ((algebraMap ℝ A : (a : ℝ) → A) 1 : A) (HSMul.hSMul (α := ℝ) 0 I') = 1

Tactic:
rw [map_one, zero_smul, add_zero]

Premises used: zero_smul, map_one, add_zero
-- Module: Mathlib.LinearAlgebra.Complex.Module
Goal:
A : Type u_1
inst : Ring A
inst_1 : Algebra ℝ A
I' : A
hf : I' * I' = -1
x₁ y₁ x₂ y₂ : ℝ
rw :
  (HAdd.hAdd (α := ℂ →ₗ[ℝ] A) (Algebra.linearMap ℝ A ∘ₗ reLm) (LinearMap.toSpanSingleton ℝ A I' ∘ₗ imLm) : (a : ℂ) → A)
      { re := x₁ * x₂ - y₁ * y₂, im := x₁ * y₂ + y₁ * x₂ : ℂ } =
    HMul.hMul (α := A) (β := A)
      ((HAdd.hAdd (α := ℂ →ₗ[ℝ] A) (Algebra.linearMap ℝ A ∘ₗ reLm) (LinearMap.toSpanSingleton ℝ A I' ∘ₗ imLm) :
            (a : ℂ) → A)
          { re := x₁, im := y₁ : ℂ } :
        A)
      ((HAdd.hAdd (α := ℂ →ₗ[ℝ] A) (Algebra.linearMap ℝ A ∘ₗ reLm) (LinearMap.toSpanSingleton ℝ A I' ∘ₗ imLm) :
            (a : ℂ) → A)
          { re := x₂, im := y₂ : ℂ } :
        A)
⊢ (HAdd.hAdd (α := ℂ →ₗ[ℝ] A) (Algebra.linearMap ℝ A ∘ₗ reLm) (LinearMap.toSpanSingleton ℝ A I' ∘ₗ imLm) : (a : ℂ) → A)
      ({ re := x₁, im := y₁ : ℂ } * { re := x₂, im := y₂ : ℂ }) =
    HMul.hMul (α := A) (β := A)
      ((HAdd.hAdd (α := ℂ →ₗ[ℝ] A) (Algebra.linearMap ℝ A ∘ₗ reLm) (LinearMap.toSpanSingleton ℝ A I' ∘ₗ imLm) :
            (a : ℂ) → A)
          { re := x₁, im := y₁ : ℂ } :
        A)
      ((HAdd.hAdd (α := ℂ →ₗ[ℝ] A) (Algebra.linearMap ℝ A ∘ₗ reLm) (LinearMap.toSpanSingleton ℝ A I' ∘ₗ imLm) :
            (a : ℂ) → A)
          { re := x₂, im := y₂ : ℂ } :
        A)

Tactic:
rw [mk_mul_mk]

Premises used: Complex.mk_mul_mk
-- Module: Mathlib.LinearAlgebra.Complex.Module
Goal:
A : Type u_1
inst : Ring A
inst_1 : Algebra ℝ A
I' : A
hf : I' * I' = -1
x₁ y₁ x₂ y₂ : ℝ
algebraMap :
  HAdd.hAdd (α := A) ((Algebra.algebraMap ℝ A : (a : ℝ) → A) (x₁ * x₂ - y₁ * y₂) : A) ((x₁ * y₂ + y₁ * x₂) • I') =
    HAdd.hAdd (α := A) ((Algebra.algebraMap ℝ A : (a : ℝ) → A) x₁ : A) (y₁ • I') *
      HAdd.hAdd (α := A) ((Algebra.algebraMap ℝ A : (a : ℝ) → A) x₂ : A) (y₂ • I')
⊢ (HAdd.hAdd (α := ℂ →ₗ[ℝ] A) (Algebra.linearMap ℝ A ∘ₗ reLm) (LinearMap.toSpanSingleton ℝ A I' ∘ₗ imLm) : (a : ℂ) → A)
      { re := x₁ * x₂ - y₁ * y₂, im := x₁ * y₂ + y₁ * x₂ : ℂ } =
    HMul.hMul (α := A) (β := A)
      ((HAdd.hAdd (α := ℂ →ₗ[ℝ] A) (Algebra.linearMap ℝ A ∘ₗ reLm) (LinearMap.toSpanSingleton ℝ A I' ∘ₗ imLm) :
            (a : ℂ) → A)
          { re := x₁, im := y₁ : ℂ } :
        A)
      ((HAdd.hAdd (α := ℂ →ₗ[ℝ] A) (Algebra.linearMap ℝ A ∘ₗ reLm) (LinearMap.toSpanSingleton ℝ A I' ∘ₗ imLm) :
            (a : ℂ) → A)
          { re := x₂, im := y₂ : ℂ } :
        A)

Tactic:
change
    algebraMap ℝ A (x₁ * x₂ - y₁ * y₂) + (x₁ * y₂ + y₁ * x₂) • I' =
      (algebraMap ℝ A x₁ + y₁ • I') * (algebraMap ℝ A x₂ + y₂ • I')

Premises used: Real, HMul.hMul, Algebra.algebraMap, HSub.hSub, HAdd.hAdd, HSMul.hSMul, DFunLike.coe
-- Module: Mathlib.LinearAlgebra.Complex.Module
Goal:
A : Type u_1
inst : Ring A
inst_1 : Algebra ℝ A
I' : A
hf : I' * I' = -1
x₁ y₁ x₂ y₂ : ℝ
rw :
  HAdd.hAdd (α := A) ((algebraMap ℝ A : (a : ℝ) → A) (x₁ * x₂ - y₁ * y₂) : A) ((x₁ * y₂ + y₁ * x₂) • I') =
    HMul.hMul (α := A) (β := A) ((algebraMap ℝ A : (a : ℝ) → A) x₁ : A) ((algebraMap ℝ A : (a : ℝ) → A) x₂ : A) +
        y₁ • I' * y₂ • I' +
      (HMul.hMul (α := A) ((algebraMap ℝ A : (a : ℝ) → A) x₁ : A) (y₂ • I') +
        HMul.hMul (β := A) (y₁ • I') ((algebraMap ℝ A : (a : ℝ) → A) x₂ : A))
⊢ HAdd.hAdd (α := A) ((algebraMap ℝ A : (a : ℝ) → A) (x₁ * x₂ - y₁ * y₂) : A) ((x₁ * y₂ + y₁ * x₂) • I') =
    HAdd.hAdd (α := A) ((algebraMap ℝ A : (a : ℝ) → A) x₁ : A) (y₁ • I') *
      HAdd.hAdd (α := A) ((algebraMap ℝ A : (a : ℝ) → A) x₂ : A) (y₂ • I')

Tactic:
rw [add_mul, mul_add, mul_add, add_comm _ (y₁ • I' * y₂ • I'), add_add_add_comm]

Premises used: add_mul, HMul.hMul, add_comm, HSMul.hSMul, mul_add, add_add_add_comm
-- Module: Mathlib.LinearAlgebra.Complex.Module
Goal:
A : Type u_1
inst : Ring A
inst_1 : Algebra ℝ A
I' : A
hf : I' * I' = -1
x₁ y₁ x₂ y₂ : ℝ
e_a :
  (algebraMap ℝ A : (a : ℝ) → A) (x₁ * x₂ - y₁ * y₂) =
    HMul.hMul (α := A) (β := A) ((algebraMap ℝ A : (a : ℝ) → A) x₁ : A) ((algebraMap ℝ A : (a : ℝ) → A) x₂ : A) +
      y₁ • I' * y₂ • I'
e_a₁ :
  (x₁ * y₂ + y₁ * x₂) • I' =
    HMul.hMul (α := A) ((algebraMap ℝ A : (a : ℝ) → A) x₁ : A) (y₂ • I') +
      HMul.hMul (β := A) (y₁ • I') ((algebraMap ℝ A : (a : ℝ) → A) x₂ : A)
⊢ HAdd.hAdd (α := A) ((algebraMap ℝ A : (a : ℝ) → A) (x₁ * x₂ - y₁ * y₂) : A) ((x₁ * y₂ + y₁ * x₂) • I') =
    HMul.hMul (α := A) (β := A) ((algebraMap ℝ A : (a : ℝ) → A) x₁ : A) ((algebraMap ℝ A : (a : ℝ) → A) x₂ : A) +
        y₁ • I' * y₂ • I' +
      (HMul.hMul (α := A) ((algebraMap ℝ A : (a : ℝ) → A) x₁ : A) (y₂ • I') +
        HMul.hMul (β := A) (y₁ • I') ((algebraMap ℝ A : (a : ℝ) → A) x₂ : A))

Tactic:
congr 1
-- Module: Mathlib.LinearAlgebra.Complex.Module
Goal:
A : Type u_1
inst : Ring A
inst_1 : Algebra ℝ A
I' : A
hf : I' * I' = -1
x₁ y₁ x₂ y₂ : ℝ
e_a :
  (algebraMap ℝ A : (a : ℝ) → A) (x₁ * x₂ - y₁ * y₂) =
    HMul.hMul (α := A) (β := A) ((algebraMap ℝ A : (a : ℝ) → A) x₁ : A) ((algebraMap ℝ A : (a : ℝ) → A) x₂ : A) +
      (y₁ * y₂) • (I' * I')
e_a₁ :
  (algebraMap ℝ A : (a : ℝ) → A) (x₁ * x₂ - y₁ * y₂) =
    HMul.hMul (α := A) (β := A) ((algebraMap ℝ A : (a : ℝ) → A) x₁ : A) ((algebraMap ℝ A : (a : ℝ) → A) x₂ : A) +
      HSMul.hSMul (β := A) (y₁ * y₂) (-1)
e_a₂ :
  (algebraMap ℝ A : (a : ℝ) → A) (x₁ * x₂ - y₁ * y₂) =
    HMul.hMul (α := A) (β := A) ((algebraMap ℝ A : (a : ℝ) → A) x₁ : A) ((algebraMap ℝ A : (a : ℝ) → A) x₂ : A) +
      -HSMul.hSMul (β := A) (y₁ * y₂) 1
e_a₃ :
  (algebraMap ℝ A : (a : ℝ) → A) (x₁ * x₂ - y₁ * y₂) =
    HAdd.hAdd (β := A)
      (HMul.hMul (α := A) (β := A) ((algebraMap ℝ A : (a : ℝ) → A) x₁ : A) ((algebraMap ℝ A : (a : ℝ) → A) x₂ : A))
      (-(algebraMap ℝ A : (a : ℝ) → A) (y₁ * y₂) : A)
e_a₄ :
  (algebraMap ℝ A : (a : ℝ) → A) (x₁ * x₂ - y₁ * y₂) =
    HSub.hSub (β := A)
      (HMul.hMul (α := A) (β := A) ((algebraMap ℝ A : (a : ℝ) → A) x₁ : A) ((algebraMap ℝ A : (a : ℝ) → A) x₂ : A))
      ((algebraMap ℝ A : (a : ℝ) → A) (y₁ * y₂) : A)
e_a₅ :
  (algebraMap ℝ A : (a : ℝ) → A) (x₁ * x₂ - y₁ * y₂) =
    HSub.hSub (α := A) (β := A) ((algebraMap ℝ A : (a : ℝ) → A) (x₁ * x₂) : A)
      ((algebraMap ℝ A : (a : ℝ) → A) (y₁ * y₂) : A)
e_a₆ e_a₇ :
  Eq (α := A) ((algebraMap ℝ A : (a : ℝ) → A) (x₁ * x₂ - y₁ * y₂) : A)
    ((algebraMap ℝ A : (a : ℝ) → A) (x₁ * x₂ - y₁ * y₂) : A)
⊢ (algebraMap ℝ A : (a : ℝ) → A) (x₁ * x₂ - y₁ * y₂) =
    HMul.hMul (α := A) (β := A) ((algebraMap ℝ A : (a : ℝ) → A) x₁ : A) ((algebraMap ℝ A : (a : ℝ) → A) x₂ : A) +
      y₁ • I' * y₂ • I'

Tactic:
rw [smul_mul_smul_comm, hf, smul_neg, ← algebraMap_eq_smul_one, ← sub_eq_add_neg,
      ← map_mul, ← map_sub]

Premises used: map_sub, sub_eq_add_neg, smul_neg, smul_mul_smul_comm, Algebra.algebraMap_eq_smul_one, map_mul
-- Module: Mathlib.LinearAlgebra.Complex.Module
Goal:
A : Type u_1
inst : Ring A
inst_1 : Algebra ℝ A
I' : A
hf : I' * I' = -1
x₁ y₁ x₂ y₂ : ℝ
e_a :
  HMul.hMul (α := A) ((algebraMap ℝ A : (a : ℝ) → A) (x₁ * y₂ + y₁ * x₂) : A) I' =
    HMul.hMul (α := A) ((algebraMap ℝ A : (a : ℝ) → A) x₁ : A) (y₂ • I') +
      HMul.hMul (β := A) (y₁ • I') ((algebraMap ℝ A : (a : ℝ) → A) x₂ : A)
e_a₁ :
  HMul.hMul (α := A) ((algebraMap ℝ A : (a : ℝ) → A) (x₁ * y₂ + y₁ * x₂) : A) I' =
    HMul.hMul (α := A) ((algebraMap ℝ A : (a : ℝ) → A) x₁ : A)
        (HMul.hMul (α := A) ((algebraMap ℝ A : (a : ℝ) → A) y₂ : A) I') +
      HMul.hMul (β := A) (y₁ • I') ((algebraMap ℝ A : (a : ℝ) → A) x₂ : A)
e_a₂ :
  HMul.hMul (α := A) ((algebraMap ℝ A : (a : ℝ) → A) (x₁ * y₂ + y₁ * x₂) : A) I' =
    HMul.hMul (α := A) ((algebraMap ℝ A : (a : ℝ) → A) x₁ : A)
        (HMul.hMul (α := A) ((algebraMap ℝ A : (a : ℝ) → A) y₂ : A) I') +
      HMul.hMul (β := A) (HMul.hMul (α := A) ((algebraMap ℝ A : (a : ℝ) → A) y₁ : A) I')
        ((algebraMap ℝ A : (a : ℝ) → A) x₂ : A)
e_a₃ :
  HMul.hMul (α := A) ((algebraMap ℝ A : (a : ℝ) → A) (x₁ * y₂ + y₁ * x₂) : A) I' =
    HMul.hMul (α := A) ((algebraMap ℝ A : (a : ℝ) → A) x₁ : A)
        (HMul.hMul (α := A) ((algebraMap ℝ A : (a : ℝ) → A) y₂ : A) I') +
      HMul.hMul (α := A) (β := A) ((algebraMap ℝ A : (a : ℝ) → A) y₁ : A) ((algebraMap ℝ A : (a : ℝ) → A) x₂ : A) * I'
e_a₄ :
  HMul.hMul (α := A) ((algebraMap ℝ A : (a : ℝ) → A) (x₁ * y₂ + y₁ * x₂) : A) I' =
    HMul.hMul (α := A) (β := A) ((algebraMap ℝ A : (a : ℝ) → A) x₁ : A) ((algebraMap ℝ A : (a : ℝ) → A) y₂ : A) * I' +
      HMul.hMul (α := A) (β := A) ((algebraMap ℝ A : (a : ℝ) → A) y₁ : A) ((algebraMap ℝ A : (a : ℝ) → A) x₂ : A) * I'
e_a₅ :
  HMul.hMul (α := A) ((algebraMap ℝ A : (a : ℝ) → A) (x₁ * y₂ + y₁ * x₂) : A) I' =
    (HMul.hMul (α := A) (β := A) ((algebraMap ℝ A : (a : ℝ) → A) x₁ : A) ((algebraMap ℝ A : (a : ℝ) → A) y₂ : A) +
        HMul.hMul (α := A) (β := A) ((algebraMap ℝ A : (a : ℝ) → A) y₁ : A) ((algebraMap ℝ A : (a : ℝ) → A) x₂ : A)) *
      I'
e_a₆ :
  HMul.hMul (α := A) ((algebraMap ℝ A : (a : ℝ) → A) (x₁ * y₂ + y₁ * x₂) : A) I' =
    HAdd.hAdd (α := A) ((algebraMap ℝ A : (a : ℝ) → A) (x₁ * y₂) : A)
        (HMul.hMul (α := A) (β := A) ((algebraMap ℝ A : (a : ℝ) → A) y₁ : A) ((algebraMap ℝ A : (a : ℝ) → A) x₂ : A)) *
      I'
e_a₇ :
  HMul.hMul (α := A) ((algebraMap ℝ A : (a : ℝ) → A) (x₁ * y₂ + y₁ * x₂) : A) I' =
    HAdd.hAdd (α := A) (β := A) ((algebraMap ℝ A : (a : ℝ) → A) (x₁ * y₂) : A)
        ((algebraMap ℝ A : (a : ℝ) → A) (y₁ * x₂) : A) *
      I'
e_a₈ e_a₉ :
  HMul.hMul (α := A) ((algebraMap ℝ A : (a : ℝ) → A) (x₁ * y₂ + y₁ * x₂) : A) I' =
    HMul.hMul (α := A) ((algebraMap ℝ A : (a : ℝ) → A) (x₁ * y₂ + y₁ * x₂) : A) I'
⊢ (x₁ * y₂ + y₁ * x₂) • I' =
    HMul.hMul (α := A) ((algebraMap ℝ A : (a : ℝ) → A) x₁ : A) (y₂ • I') +
      HMul.hMul (β := A) (y₁ • I') ((algebraMap ℝ A : (a : ℝ) → A) x₂ : A)

Tactic:
rw [smul_def, smul_def, smul_def, ← right_comm _ x₂,
      ← mul_assoc, ← add_mul, ← map_mul, ← map_mul, ← map_add]

Premises used: add_mul, Algebra.right_comm, mul_assoc, map_add, map_mul, Algebra.smul_def
-- Module: Mathlib.LinearAlgebra.Complex.Module
Goal:
A : Type u_1
inst : Ring A
inst_1 : Algebra ℝ A
I' : A
hI' : I' * I' = -1
z : ℂ
⊢ (liftAux I' hI' : (a : ℂ) → A) z = HAdd.hAdd (α := A) ((algebraMap ℝ A : (a : ℝ) → A) z.re : A) (z.im • I')

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.Complex.Module
Goal:
A : Type u_1
inst : Ring A
inst_1 : Algebra ℝ A
I' : A
hI' : I' * I' = -1
⊢ (liftAux I' hI' : (a : ℂ) → A) I = I'

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Complex.Module
Goal:
⊢ Eq (α := Subalgebra ℝ ℂ) ℝ[I] ⊤

Tactic:
top_unique fun x hx => ?_

Premises used: top_unique
-- Module: Mathlib.LinearAlgebra.Complex.Module
Goal:
refine : ∀ (x : ℂ) (hx : Membership.mem (γ := Subalgebra ℝ ℂ) ⊤ x), Membership.mem (γ := Subalgebra ℝ ℂ) ℝ[I] x
⊢ Eq (α := Subalgebra ℝ ℂ) ℝ[I] ⊤

Tactic:
refine top_unique fun x hx => ?_

Premises used: top_unique
-- Module: Mathlib.LinearAlgebra.Complex.Module
Goal:
x : ℂ
rw :
  Membership.mem (γ := Subalgebra ℝ ℂ) ℝ[I]
    (HAdd.hAdd (α := ℂ) ((algebraMap ℝ ℂ : (a : ℝ) → ℂ) x.re : ℂ)
      (HSMul.hSMul (α := ℂ) ((algebraMap ℝ ℂ : (a : ℝ) → ℂ) x.im : ℂ) I))
⊢ Membership.mem (γ := Subalgebra ℝ ℂ) ℝ[I] x

Tactic:
rw [← x.re_add_im, ← smul_eq_mul, ← Complex.coe_algebraMap]

Premises used: Complex.coe_algebraMap, smul_eq_mul, Complex.re_add_im
-- Module: Mathlib.LinearAlgebra.Complex.Module
Goal:
x : ℂ
⊢ Membership.mem (γ := Set ℂ) {I} I

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Complex.Module
Goal:
x : ℂ
⊢ Membership.mem (γ := Subalgebra ℝ ℂ) ℝ[I]
    (HAdd.hAdd (α := ℂ) ((algebraMap ℝ ℂ : (a : ℝ) → ℂ) x.re : ℂ)
      (HSMul.hSMul (α := ℂ) ((algebraMap ℝ ℂ : (a : ℝ) → ℂ) x.im : ℂ) I))

Tactic:
exact add_mem (algebraMap_mem _ _) (Subalgebra.smul_mem _ (subset_adjoin <| by simp) _)

Premises used: Algebra.subset_adjoin, Subalgebra.smul_mem, algebraMap_mem, AddMemClass.add_mem
-- Module: Mathlib.LinearAlgebra.Complex.Module
Goal:
A : Type u_1
inst : Ring A
inst_1 : Algebra ℝ A
I' : A
hI' : I' * I' = -1
simp_rw : Eq (α := Subalgebra ℝ A) (Subalgebra.map (liftAux I' hI') ⊤) ℝ[I']
simp_rw₁ : Eq (α := Subalgebra ℝ A) (Subalgebra.map (liftAux I' hI') ℝ[I]) ℝ[I']
simp_rw₂ : Eq (α := Subalgebra ℝ A) (adjoin ℝ (Set.image (α := ℂ) (⇑(liftAux I' hI') : (a : ℂ) → A) {I})) ℝ[I']
simp_rw₃ : Eq (α := Subalgebra ℝ A) ℝ[((liftAux I' hI' : (a : ℂ) → A) I : A)] ℝ[I']
⊢ Eq (α := Subalgebra ℝ A) (AlgHom.range (liftAux I' hI')) ℝ[I']

Tactic:
simp_rw [← Algebra.map_top, ← adjoin_I, AlgHom.map_adjoin, Set.image_singleton, liftAux_apply_I]

Premises used: Set.image_singleton, Complex.liftAux_apply_I, AlgHom.map_adjoin, Algebra.map_top, Complex.adjoin_I