awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Complex.Module (goal)
Goal:
f : ℂ →ₐ[ℝ] ℂ
⊢ (f : (a : ℂ) → ℂ) I = I → f = AlgHom.id ℝ ℂ
have refine_1 : ∀ (h : (f : (a : ℂ) → ℂ) I = I), Eq (α := ℂ) ((f : (a : ℂ) → ℂ) I : ℂ) ((AlgHom.id ℝ ℂ : (a : ℂ) → ℂ) I : ℂ)
Tactic: refine fun h => algHom_ext ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.Complex.Module (goal)
Goal:
f : ℂ →ₐ[ℝ] ℂ
⊢ (f : (a : ℂ) → ℂ) I = -I → f = (↑conjAe : ℂ →ₐ[ℝ] ℂ)
have refine_2 : ∀ (h : (f : (a : ℂ) → ℂ) I = -I), Eq (α := ℂ) ((f : (a : ℂ) → ℂ) I : ℂ) (((↑conjAe : ℂ →ₐ[ℝ] ℂ) : (a : ℂ) → ℂ) I : ℂ)
Tactic: refine fun h => algHom_ext ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.Complex.Module (goal)
Goal:
A : Type u_1
inst : Ring A
inst_1 : Algebra ℝ A
I' : A
hf : I' * I' = -1
⊢ HAdd.hAdd (α := A) ((algebraMap ℝ A : (a : ℝ) → A) 1 : A) (HSMul.hSMul (α := ℝ) 0 I') = 1
have rw : 1 + HSMul.hSMul (α := ℝ) 0 I' = 1
Tactic: rw [map_one, zero_smul, add_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Complex.Module (goal)
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
⊢ HAdd.hAdd (α := A) ((algebraMap ℝ A : (a : ℝ) → A) 1 : A) (HSMul.hSMul (α := ℝ) 0 I') = 1
have rw₁ : HAdd.hAdd (α := A) 1 0 = 1
Tactic: rw [map_one, zero_smul, add_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Complex.Module (goal)
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
⊢ HAdd.hAdd (α := A) ((algebraMap ℝ A : (a : ℝ) → A) 1 : A) (HSMul.hSMul (α := ℝ) 0 I') = 1
have rw₂ : Eq.{u_1 + 1} (α := A) 1 1
Tactic: rw [map_one, zero_smul, add_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Complex.Module (goal)
Goal:
A : Type u_1
inst : Ring A
inst_1 : Algebra ℝ A
I' : A
hf : I' * I' = -1
x₁ y₁ x₂ y₂ : ℝ
⊢ (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)
have 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)
Tactic: rw [mk_mul_mk]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Complex.Module (goal)
Goal:
A : Type u_1
inst : Ring A
inst_1 : Algebra ℝ A
I' : A
hf : I' * I' = -1
x₁ y₁ x₂ y₂ : ℝ
⊢ (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)
have algebraMap : 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: change
    algebraMap ℝ A (x₁ * x₂ - y₁ * y₂) + (x₁ * y₂ + y₁ * x₂) • I' =
      (algebraMap ℝ A x₁ + y₁ • I') * (algebraMap ℝ A x₂ + y₂ • I')
-- Lean 4 proof step from Mathlib.LinearAlgebra.Complex.Module (goal)
Goal:
A : Type u_1
inst : Ring A
inst_1 : Algebra ℝ A
I' : A
hf : I' * I' = -1
x₁ y₁ x₂ y₂ : ℝ
⊢ 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')
have 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))
Tactic: rw [add_mul, mul_add, mul_add, add_comm _ (y₁ • I' * y₂ • I'), add_add_add_comm]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Complex.Module (goal)
Goal:
A : Type u_1
inst : Ring A
inst_1 : Algebra ℝ A
I' : A
hf : I' * I' = -1
x₁ y₁ x₂ y₂ : ℝ
⊢ 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))
have 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'
Tactic: congr 1
-- Lean 4 proof step from Mathlib.LinearAlgebra.Complex.Module (goal)
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'
⊢ 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))
have 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)
Tactic: congr 1
-- Lean 4 proof step from Mathlib.LinearAlgebra.Complex.Module (goal)
Goal:
A : Type u_1
inst : Ring A
inst_1 : Algebra ℝ A
I' : A
hf : I' * I' = -1
x₁ y₁ x₂ y₂ : ℝ
⊢ (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'
have 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')
Tactic: rw [smul_mul_smul_comm, hf, smul_neg, ← algebraMap_eq_smul_one, ← sub_eq_add_neg,
      ← map_mul, ← map_sub]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Complex.Module (goal)
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')
⊢ (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'
have 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)
Tactic: rw [smul_mul_smul_comm, hf, smul_neg, ← algebraMap_eq_smul_one, ← sub_eq_add_neg,
      ← map_mul, ← map_sub]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Complex.Module (goal)
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)
⊢ (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'
have 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
Tactic: rw [smul_mul_smul_comm, hf, smul_neg, ← algebraMap_eq_smul_one, ← sub_eq_add_neg,
      ← map_mul, ← map_sub]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Complex.Module (goal)
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
⊢ (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'
have 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)
Tactic: rw [smul_mul_smul_comm, hf, smul_neg, ← algebraMap_eq_smul_one, ← sub_eq_add_neg,
      ← map_mul, ← map_sub]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Complex.Module (goal)
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)
⊢ (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'
have 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)
Tactic: rw [smul_mul_smul_comm, hf, smul_neg, ← algebraMap_eq_smul_one, ← sub_eq_add_neg,
      ← map_mul, ← map_sub]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Complex.Module (goal)
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)
⊢ (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'
have 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)
Tactic: rw [smul_mul_smul_comm, hf, smul_neg, ← algebraMap_eq_smul_one, ← sub_eq_add_neg,
      ← map_mul, ← map_sub]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Complex.Module (goal)
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)
⊢ (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'
have e_a₆ : Eq (α := A) ((algebraMap ℝ A : (a : ℝ) → A) (x₁ * x₂ - y₁ * y₂) : A)
  ((algebraMap ℝ A : (a : ℝ) → A) (x₁ * x₂ - y₁ * y₂) : A)
Tactic: rw [smul_mul_smul_comm, hf, smul_neg, ← algebraMap_eq_smul_one, ← sub_eq_add_neg,
      ← map_mul, ← map_sub]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Complex.Module (goal)
Goal:
A : Type u_1
inst : Ring A
inst_1 : Algebra ℝ A
I' : A
hf : I' * I' = -1
x₁ y₁ x₂ y₂ : ℝ
⊢ (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)
have 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)
Tactic: rw [smul_def, smul_def, smul_def, ← right_comm _ x₂,
      ← mul_assoc, ← add_mul, ← map_mul, ← map_mul, ← map_add]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Complex.Module (goal)
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)
⊢ (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)
have 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)
Tactic: rw [smul_def, smul_def, smul_def, ← right_comm _ x₂,
      ← mul_assoc, ← add_mul, ← map_mul, ← map_mul, ← map_add]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Complex.Module (goal)
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)
⊢ (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)
have 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)
Tactic: rw [smul_def, smul_def, smul_def, ← right_comm _ x₂,
      ← mul_assoc, ← add_mul, ← map_mul, ← map_mul, ← map_add]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Complex.Module (goal)
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)
⊢ (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)
have 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'
Tactic: rw [smul_def, smul_def, smul_def, ← right_comm _ x₂,
      ← mul_assoc, ← add_mul, ← map_mul, ← map_mul, ← map_add]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Complex.Module (goal)
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'
⊢ (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)
have 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'
Tactic: rw [smul_def, smul_def, smul_def, ← right_comm _ x₂,
      ← mul_assoc, ← add_mul, ← map_mul, ← map_mul, ← map_add]