awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Complex.Determinant
Goal:
rw : HMul.hMul (α := ℝ) 1 (-1) - HMul.hMul (α := ℝ) 0 0 = -1
⊢ Eq (α := ℝ) ((LinearMap.det : (a : ℂ →ₗ[ℝ] ℂ) → ℝ) (↑(↑conjAe : ℂ ≃ₗ[ℝ] ℂ) : ℂ →ₗ[ℝ] ℂ) : ℝ) (-1 : ℝ)

Tactic:
rw [← LinearMap.det_toMatrix basisOneI, toMatrix_conjAe, Matrix.det_fin_two_of]

Premises used: Complex.basisOneI, Complex.toMatrix_conjAe, Matrix.det_fin_two_of, LinearMap.det_toMatrix
-- Module: Mathlib.LinearAlgebra.Complex.Determinant
Goal:
⊢ HMul.hMul (α := ℝ) 1 (-1) - HMul.hMul (α := ℝ) 0 0 = -1

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Complex.Determinant
Goal:
⊢ Eq (α := ℝˣ) ((LinearEquiv.det : (a : ℂ ≃ₗ[ℝ] ℂ) → ℝˣ) (↑conjAe : ℂ ≃ₗ[ℝ] ℂ) : ℝˣ) (-1 : ℝˣ)

Tactic:
simp [← Units.val_inj]

Premises used: Units.val_inj
-- Module: Mathlib.LinearAlgebra.Complex.FiniteDimensional
Goal:
⊢ FiniteDimensional ℝ ℂ

Tactic:
basisOneI.finiteDimensional_of_finite

Premises used: Module.Basis.finiteDimensional_of_finite, Complex.basisOneI
-- Module: Mathlib.LinearAlgebra.Complex.FiniteDimensional
Goal:
rw : Fintype.card (Fin 2) = 2
rw₁ rw₂ : Eq (α := ℕ) 2 2
⊢ finrank ℝ ℂ = 2

Tactic:
rw [finrank_eq_card_basis basisOneI, Fintype.card_fin]

Premises used: Fintype.card_fin, Module.finrank_eq_card_basis, Complex.basisOneI
-- Module: Mathlib.LinearAlgebra.Complex.FiniteDimensional
Goal:
⊢ Module.rank ℝ ℂ = 2

Tactic:
simp [← finrank_eq_rank, finrank_real_complex]

Premises used: Module.finrank_eq_rank, Complex.finrank_real_complex
-- Module: Mathlib.LinearAlgebra.Complex.FiniteDimensional
Goal:
rw : Cardinal.lift.{u, 0} (↑(finrank ℝ ℂ) : Cardinal.{0}) = 2
rw₁ : Cardinal.lift.{u, 0} (↑2 : Cardinal.{0}) = 2
rw₂ : Eq.{u + 2} (α := Cardinal.{u}) (↑2 : Cardinal.{u}) 2
rw₃ rw₄ : Eq.{u + 2} (α := Cardinal.{u}) 2 2
⊢ Cardinal.lift.{u, 0} (Module.rank ℝ ℂ) = 2

Tactic:
rw [← finrank_eq_rank, finrank_real_complex, Cardinal.lift_natCast, Nat.cast_ofNat]

Premises used: Nat.cast_ofNat, Module.finrank_eq_rank, Cardinal.lift_natCast, Complex.finrank_real_complex
-- Module: Mathlib.LinearAlgebra.Complex.FiniteDimensional
Goal:
⊢ Fact (finrank ℝ ℂ = 2)

Tactic:
⟨finrank_real_complex⟩

Premises used: Fact.mk, Complex.finrank_real_complex
-- Module: Mathlib.LinearAlgebra.Complex.FiniteDimensional
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℂ E
inst_2 : FiniteDimensional ℂ E
⊢ FiniteDimensional ℝ E

Tactic:
FiniteDimensional.trans ℝ ℂ E

Premises used: Real, FiniteDimensional.trans, Complex
-- Module: Mathlib.LinearAlgebra.Complex.FiniteDimensional
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℂ E
rw : 2 * Cardinal.lift.{0, u_1} (Module.rank ℂ E) = Cardinal.lift.{0, u_1} (2 * Module.rank ℂ E)
⊢ Cardinal.lift.{0, u_1} (Module.rank ℝ E) = Cardinal.lift.{0, u_1} (2 * Module.rank ℂ E)

Tactic:
rw [← lift_rank_mul_lift_rank ℝ ℂ E, Complex.rank_real_complex']

Premises used: lift_rank_mul_lift_rank, Real, Complex.rank_real_complex', Complex
-- Module: Mathlib.LinearAlgebra.Complex.FiniteDimensional
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℂ E
⊢ 2 * Cardinal.lift.{0, u_1} (Module.rank ℂ E) = Cardinal.lift.{0, u_1} (2 * Module.rank ℂ E)

Tactic:
simp only [Cardinal.lift_id']

Premises used: Cardinal.lift_id'
-- Module: Mathlib.LinearAlgebra.Complex.FiniteDimensional
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Module ℂ E
rw : finrank ℝ ℂ * finrank ℂ E = 2 * finrank ℂ E
rw₁ rw₂ : 2 * finrank ℂ E = 2 * finrank ℂ E
⊢ finrank ℝ E = 2 * finrank ℂ E

Tactic:
rw [← Module.finrank_mul_finrank ℝ ℂ E, Complex.finrank_real_complex]

Premises used: Real, Module.finrank_mul_finrank, Complex.finrank_real_complex, Complex
-- Module: Mathlib.LinearAlgebra.Complex.FiniteDimensional
Goal:
⊢ Module.rank ℚ ℝ = 𝔠

Tactic:
(Free.rank_eq_mk_of_infinite_lt ℚ ℝ ?_).trans mk_real

Premises used: Real, Rat, Cardinal.mk_real, Module.Free.rank_eq_mk_of_infinite_lt, Eq.trans
-- Module: Mathlib.LinearAlgebra.Complex.FiniteDimensional
Goal:
refine : lift.{0, 0} #ℚ < lift.{0, 0} #ℝ
⊢ Module.rank ℚ ℝ = 𝔠

Tactic:
refine (Free.rank_eq_mk_of_infinite_lt ℚ ℝ ?_).trans mk_real

Premises used: Real, Rat, Cardinal.mk_real, Module.Free.rank_eq_mk_of_infinite_lt, Eq.trans
-- Module: Mathlib.LinearAlgebra.Complex.FiniteDimensional
Goal:
⊢ lift.{0, 0} #ℚ < lift.{0, 0} #ℝ

Tactic:
simpa [mk_real] using aleph0_lt_continuum

Premises used: Cardinal.mk_real, Cardinal.aleph0_lt_continuum
-- Module: Mathlib.LinearAlgebra.Complex.FiniteDimensional
Goal:
⊢ Module.rank ℚ ℂ = 𝔠

Tactic:
(Free.rank_eq_mk_of_infinite_lt ℚ ℂ ?_).trans Cardinal.mk_complex

Premises used: Rat, Module.Free.rank_eq_mk_of_infinite_lt, Cardinal.mk_complex, Complex, Eq.trans
-- Module: Mathlib.LinearAlgebra.Complex.FiniteDimensional
Goal:
refine : Cardinal.lift.{0, 0} #ℚ < Cardinal.lift.{0, 0} #ℂ
⊢ Module.rank ℚ ℂ = 𝔠

Tactic:
refine (Free.rank_eq_mk_of_infinite_lt ℚ ℂ ?_).trans Cardinal.mk_complex

Premises used: Rat, Module.Free.rank_eq_mk_of_infinite_lt, Cardinal.mk_complex, Complex, Eq.trans
-- Module: Mathlib.LinearAlgebra.Complex.FiniteDimensional
Goal:
⊢ Cardinal.lift.{0, 0} #ℚ < Cardinal.lift.{0, 0} #ℂ

Tactic:
simpa using aleph0_lt_continuum

Premises used: Cardinal.aleph0_lt_continuum
-- Module: Mathlib.LinearAlgebra.Complex.FiniteDimensional
Goal:
⊢ Module.rank ℚ ℂ = Module.rank ℚ ℝ

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Complex.Module
Goal:
R : Type u_1
S : Type u_2
inst : SMul R ℝ
inst_1 : SMul S ℝ
inst_2 : SMulCommClass R S ℝ
r : R
s : S
x : ℂ
a : (r • s • x).re = (s • r • x).re
a₁ : (r • s • x).im = (s • r • x).im
⊢ r • s • x = s • r • x

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.Complex.Module
Goal:
R : Type u_1
S : Type u_2
inst : SMul R ℝ
inst_1 : SMul S ℝ
inst_2 : SMulCommClass R S ℝ
r : R
s : S
x : ℂ
⊢ (r • s • x).re = (s • r • x).re

Tactic:
simp [smul_re, smul_im, smul_comm]

Premises used: Complex.smul_re, SMulCommClass.smul_comm, Complex.smul_im
-- Module: Mathlib.LinearAlgebra.Complex.Module
Goal:
R : Type u_1
S : Type u_2
inst : SMul R ℝ
inst_1 : SMul S ℝ
inst_2 : SMulCommClass R S ℝ
r : R
s : S
x : ℂ
⊢ (r • s • x).im = (s • r • x).im

Tactic:
simp [smul_re, smul_im, smul_comm]

Premises used: Complex.smul_re, SMulCommClass.smul_comm, Complex.smul_im
-- Module: Mathlib.LinearAlgebra.Complex.Module
Goal:
R : Type u_1
S : Type u_2
inst : SMul R S
inst_1 : SMul R ℝ
inst_2 : SMul S ℝ
inst_3 : IsScalarTower R S ℝ
r : R
s : S
x : ℂ
a : ((r • s) • x).re = (r • s • x).re
a₁ : ((r • s) • x).im = (r • s • x).im
⊢ (r • s) • x = r • s • x

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.Complex.Module
Goal:
R : Type u_1
S : Type u_2
inst : SMul R S
inst_1 : SMul R ℝ
inst_2 : SMul S ℝ
inst_3 : IsScalarTower R S ℝ
r : R
s : S
x : ℂ
⊢ ((r • s) • x).re = (r • s • x).re

Tactic:
simp [smul_re, smul_im, smul_assoc]

Premises used: smul_assoc, Complex.smul_re, Complex.smul_im
-- Module: Mathlib.LinearAlgebra.Complex.Module
Goal:
R : Type u_1
S : Type u_2
inst : SMul R S
inst_1 : SMul R ℝ
inst_2 : SMul S ℝ
inst_3 : IsScalarTower R S ℝ
r : R
s : S
x : ℂ
⊢ ((r • s) • x).im = (r • s • x).im

Tactic:
simp [smul_re, smul_im, smul_assoc]

Premises used: smul_assoc, Complex.smul_re, Complex.smul_im
-- Module: Mathlib.LinearAlgebra.Complex.Module
Goal:
R : Type u_1
S : Type u_2
inst : SMul R ℝ
inst_1 : SMul Rᵐᵒᵖ ℝ
inst_2 : IsCentralScalar R ℝ
r : R
x : ℂ
a : (MulOpposite.op r • x).re = (r • x).re
a₁ : (MulOpposite.op r • x).im = (r • x).im
⊢ MulOpposite.op r • x = r • x

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.Complex.Module
Goal:
R : Type u_1
S : Type u_2
inst : SMul R ℝ
inst_1 : SMul Rᵐᵒᵖ ℝ
inst_2 : IsCentralScalar R ℝ
r : R
x : ℂ
⊢ (MulOpposite.op r • x).re = (r • x).re

Tactic:
simp [smul_re, smul_im, op_smul_eq_smul]

Premises used: Complex.smul_re, Complex.smul_im, IsCentralScalar.op_smul_eq_smul
-- Module: Mathlib.LinearAlgebra.Complex.Module
Goal:
R : Type u_1
S : Type u_2
inst : SMul R ℝ
inst_1 : SMul Rᵐᵒᵖ ℝ
inst_2 : IsCentralScalar R ℝ
r : R
x : ℂ
⊢ (MulOpposite.op r • x).im = (r • x).im

Tactic:
simp [smul_re, smul_im, op_smul_eq_smul]

Premises used: Complex.smul_re, Complex.smul_im, IsCentralScalar.op_smul_eq_smul
-- Module: Mathlib.LinearAlgebra.Complex.Module
Goal:
R : Type u_1
S : Type u_2
inst : Monoid R
inst_1 : MulAction R ℝ
r s : R
x : ℂ
a : ((r * s) • x).re = (r • s • x).re
a₁ : ((r * s) • x).im = (r • s • x).im
⊢ (r * s) • x = r • s • x

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.Complex.Module
Goal:
R : Type u_1
S : Type u_2
inst : Monoid R
inst_1 : MulAction R ℝ
r s : R
x : ℂ
⊢ ((r * s) • x).re = (r • s • x).re

Tactic:
simp [smul_re, smul_im, mul_smul]

Premises used: Complex.smul_re, Complex.smul_im, SemigroupAction.mul_smul
-- Module: Mathlib.LinearAlgebra.Complex.Module
Goal:
R : Type u_1
S : Type u_2
inst : Monoid R
inst_1 : MulAction R ℝ
r s : R
x : ℂ
⊢ ((r * s) • x).im = (r • s • x).im

Tactic:
simp [smul_re, smul_im, mul_smul]

Premises used: Complex.smul_re, Complex.smul_im, SemigroupAction.mul_smul
-- Module: Mathlib.LinearAlgebra.Complex.Module
Goal:
R : Type u_1
S : Type u_2
inst : Monoid R
inst_1 : MulAction R ℝ
x : ℂ
a : (HSMul.hSMul.{u_1, 0, 0} (α := R) 1 x).re = x.re
a₁ : (HSMul.hSMul.{u_1, 0, 0} (α := R) 1 x).im = x.im
⊢ HSMul.hSMul.{u_1, 0, 0} (α := R) 1 x = x

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.Complex.Module
Goal:
R : Type u_1
S : Type u_2
inst : Monoid R
inst_1 : MulAction R ℝ
x : ℂ
⊢ (HSMul.hSMul.{u_1, 0, 0} (α := R) 1 x).re = x.re

Tactic:
simp [smul_re, smul_im, one_smul]

Premises used: Complex.smul_re, one_smul, Complex.smul_im
-- Module: Mathlib.LinearAlgebra.Complex.Module
Goal:
R : Type u_1
S : Type u_2
inst : Monoid R
inst_1 : MulAction R ℝ
x : ℂ
⊢ (HSMul.hSMul.{u_1, 0, 0} (α := R) 1 x).im = x.im

Tactic:
simp [smul_re, smul_im, one_smul]

Premises used: Complex.smul_re, one_smul, Complex.smul_im
-- Module: Mathlib.LinearAlgebra.Complex.Module
Goal:
R : Type u_1
S : Type u_2
inst : DistribSMul R ℝ
r : R
a : (HSMul.hSMul (β := ℂ) r 0).re = re 0
a₁ : (HSMul.hSMul (β := ℂ) r 0).im = im 0
⊢ HSMul.hSMul (β := ℂ) r 0 = 0

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.Complex.Module
Goal:
R : Type u_1
S : Type u_2
inst : DistribSMul R ℝ
r : R
⊢ (HSMul.hSMul (β := ℂ) r 0).re = re 0

Tactic:
simp [smul_re, smul_im, smul_zero]

Premises used: Complex.smul_re, smul_zero, Complex.smul_im
-- Module: Mathlib.LinearAlgebra.Complex.Module
Goal:
R : Type u_1
S : Type u_2
inst : DistribSMul R ℝ
r : R
⊢ (HSMul.hSMul (β := ℂ) r 0).im = im 0

Tactic:
simp [smul_re, smul_im, smul_zero]

Premises used: Complex.smul_re, smul_zero, Complex.smul_im
-- Module: Mathlib.LinearAlgebra.Complex.Module
Goal:
R : Type u_1
S : Type u_2
inst : DistribSMul R ℝ
r : R
x y : ℂ
a : (r • (x + y)).re = (r • x + r • y).re
a₁ : (r • (x + y)).im = (r • x + r • y).im
⊢ r • (x + y) = r • x + r • y

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.Complex.Module
Goal:
R : Type u_1
S : Type u_2
inst : DistribSMul R ℝ
r : R
x y : ℂ
⊢ (r • (x + y)).re = (r • x + r • y).re

Tactic:
simp [smul_re, smul_im, smul_add]

Premises used: Complex.smul_re, Complex.smul_im, smul_add
-- Module: Mathlib.LinearAlgebra.Complex.Module
Goal:
R : Type u_1
S : Type u_2
inst : DistribSMul R ℝ
r : R
x y : ℂ
⊢ (r • (x + y)).im = (r • x + r • y).im

Tactic:
simp [smul_re, smul_im, smul_add]

Premises used: Complex.smul_re, Complex.smul_im, smul_add
-- Module: Mathlib.LinearAlgebra.Complex.Module
Goal:
R : Type u_1
S : Type u_2
inst : Semiring R
inst_1 : Module R ℝ
r s : R
x : ℂ
a : ((r + s) • x).re = (r • x + s • x).re
a₁ : ((r + s) • x).im = (r • x + s • x).im
⊢ (r + s) • x = r • x + s • x

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.Complex.Module
Goal:
R : Type u_1
S : Type u_2
inst : Semiring R
inst_1 : Module R ℝ
r s : R
x : ℂ
⊢ ((r + s) • x).re = (r • x + s • x).re

Tactic:
simp [smul_re, smul_im, add_smul]

Premises used: Complex.smul_re, add_smul, Complex.smul_im
-- Module: Mathlib.LinearAlgebra.Complex.Module
Goal:
R : Type u_1
S : Type u_2
inst : Semiring R
inst_1 : Module R ℝ
r s : R
x : ℂ
⊢ ((r + s) • x).im = (r • x + s • x).im

Tactic:
simp [smul_re, smul_im, add_smul]

Premises used: Complex.smul_re, add_smul, Complex.smul_im
-- Module: Mathlib.LinearAlgebra.Complex.Module
Goal:
R : Type u_1
S : Type u_2
inst : Semiring R
inst_1 : Module R ℝ
r : ℂ
a : (HSMul.hSMul.{u_1, 0, 0} (α := R) 0 r).re = re 0
a₁ : (HSMul.hSMul.{u_1, 0, 0} (α := R) 0 r).im = im 0
⊢ HSMul.hSMul.{u_1, 0, 0} (α := R) 0 r = 0

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.Complex.Module
Goal:
R : Type u_1
S : Type u_2
inst : Semiring R
inst_1 : Module R ℝ
r : ℂ
⊢ (HSMul.hSMul.{u_1, 0, 0} (α := R) 0 r).re = re 0

Tactic:
simp [smul_re, smul_im, zero_smul]

Premises used: Complex.smul_re, zero_smul, Complex.smul_im
-- Module: Mathlib.LinearAlgebra.Complex.Module
Goal:
R : Type u_1
S : Type u_2
inst : Semiring R
inst_1 : Module R ℝ
r : ℂ
⊢ (HSMul.hSMul.{u_1, 0, 0} (α := R) 0 r).im = im 0

Tactic:
simp [smul_re, smul_im, zero_smul]

Premises used: Complex.smul_re, zero_smul, Complex.smul_im
-- Module: Mathlib.LinearAlgebra.Complex.Module
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : Algebra R ℝ
r : R
x : ℂ
xr xi : ℝ
a :
  (HMul.hMul (α := ℂ) ((ofRealHom.comp (algebraMap R ℝ) : (a : R) → ℂ) r : ℂ) { re := xr, im := xi : ℂ }).re =
    (HMul.hMul (β := ℂ) { re := xr, im := xi : ℂ } ((ofRealHom.comp (algebraMap R ℝ) : (a : R) → ℂ) r : ℂ)).re
a₁ :
  (HMul.hMul (α := ℂ) ((ofRealHom.comp (algebraMap R ℝ) : (a : R) → ℂ) r : ℂ) { re := xr, im := xi : ℂ }).im =
    (HMul.hMul (β := ℂ) { re := xr, im := xi : ℂ } ((ofRealHom.comp (algebraMap R ℝ) : (a : R) → ℂ) r : ℂ)).im
⊢ HMul.hMul (α := ℂ) ((ofRealHom.comp (algebraMap R ℝ) : (a : R) → ℂ) r : ℂ) { re := xr, im := xi : ℂ } =
    HMul.hMul (β := ℂ) { re := xr, im := xi : ℂ } ((ofRealHom.comp (algebraMap R ℝ) : (a : R) → ℂ) r : ℂ)

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.Complex.Module
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : Algebra R ℝ
r : R
x : ℂ
xr xi : ℝ
⊢ (HMul.hMul (α := ℂ) ((ofRealHom.comp (algebraMap R ℝ) : (a : R) → ℂ) r : ℂ) { re := xr, im := xi : ℂ }).re =
    (HMul.hMul (β := ℂ) { re := xr, im := xi : ℂ } ((ofRealHom.comp (algebraMap R ℝ) : (a : R) → ℂ) r : ℂ)).re

Tactic:
simp [Algebra.commutes]

Premises used: Algebra.commutes
-- Module: Mathlib.LinearAlgebra.Complex.Module
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : Algebra R ℝ
r : R
x : ℂ
xr xi : ℝ
⊢ (HMul.hMul (α := ℂ) ((ofRealHom.comp (algebraMap R ℝ) : (a : R) → ℂ) r : ℂ) { re := xr, im := xi : ℂ }).im =
    (HMul.hMul (β := ℂ) { re := xr, im := xi : ℂ } ((ofRealHom.comp (algebraMap R ℝ) : (a : R) → ℂ) r : ℂ)).im

Tactic:
simp [Algebra.commutes]

Premises used: Algebra.commutes
-- Module: Mathlib.LinearAlgebra.Complex.Module
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : Algebra R ℝ
r : R
x : ℂ
a : (r • x).re = (HMul.hMul (α := ℂ) ((ofRealHom.comp (algebraMap R ℝ) : (a : R) → ℂ) r : ℂ) x).re
a₁ : (r • x).im = (HMul.hMul (α := ℂ) ((ofRealHom.comp (algebraMap R ℝ) : (a : R) → ℂ) r : ℂ) x).im
⊢ r • x = HMul.hMul (α := ℂ) ((ofRealHom.comp (algebraMap R ℝ) : (a : R) → ℂ) r : ℂ) x

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.Complex.Module
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : Algebra R ℝ
r : R
x : ℂ
⊢ (r • x).re = (HMul.hMul (α := ℂ) ((ofRealHom.comp (algebraMap R ℝ) : (a : R) → ℂ) r : ℂ) x).re

Tactic:
simp [smul_re, smul_im, Algebra.smul_def]

Premises used: Complex.smul_re, Algebra.smul_def, Complex.smul_im
-- Module: Mathlib.LinearAlgebra.Complex.Module
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : Algebra R ℝ
r : R
x : ℂ
⊢ (r • x).im = (HMul.hMul (α := ℂ) ((ofRealHom.comp (algebraMap R ℝ) : (a : R) → ℂ) r : ℂ) x).im

Tactic:
simp [smul_re, smul_im, Algebra.smul_def]

Premises used: Complex.smul_re, Algebra.smul_def, Complex.smul_im
-- Module: Mathlib.LinearAlgebra.Complex.Module
Goal:
R : Type u_1
S : Type u_2
r : ℝ
x : ℂ
⊢ star (r • x) = star r • star x

Tactic:
simp only [star_def, star_trivial, real_smul, map_mul, conj_ofReal]

Premises used: Complex.real_smul, Complex.star_def, TrivialStar.star_trivial, map_mul, Complex.conj_ofReal
-- Module: Mathlib.LinearAlgebra.Complex.Module
Goal:
⊢ (⇑(algebraMap ℝ ℂ) : (a : ℝ) → ℂ) = ofReal

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.Complex.Module
Goal:
R : Type u_1
S : Type u_2
⊢ Semiring.toNatAlgebra = instAlgebraOfReal

Tactic:
rfl
-- Module: Mathlib.LinearAlgebra.Complex.Module
Goal:
R : Type u_1
S : Type u_2
⊢ Semiring.toNatAlgebra = instAlgebraOfReal

Tactic:
with_reducible_and_instances rfl
-- Module: Mathlib.LinearAlgebra.Complex.Module
Goal:
R : Type u_1
S : Type u_2
⊢ Ring.toIntAlgebra ℂ = instAlgebraOfReal

Tactic:
rfl
-- Module: Mathlib.LinearAlgebra.Complex.Module
Goal:
R : Type u_1
S : Type u_2
⊢ Ring.toIntAlgebra ℂ = instAlgebraOfReal

Tactic:
with_reducible_and_instances rfl
-- Module: Mathlib.LinearAlgebra.Complex.Module
Goal:
R : Type u_1
S : Type u_2
⊢ Eq (α := Module ℝ ℂ) (Module.restrictScalars ℝ ℂ ℂ) instModule

Tactic:
rfl
-- Module: Mathlib.LinearAlgebra.Complex.Module
Goal:
R : Type u_1
S : Type u_2
⊢ Eq (α := Module ℝ ℂ) (Module.restrictScalars ℝ ℂ ℂ) instModule

Tactic:
with_reducible_and_instances rfl
-- Module: Mathlib.LinearAlgebra.Complex.Module
Goal:
A : Type u_3
inst : Semiring A
inst_1 : Algebra ℝ A
f : ℂ →ₐ[ℝ] A
x : ℝ
⊢ Eq (α := A) ((f : (a : ℂ) → A) (↑x : ℂ) : A) ((algebraMap ℝ A : (a : ℝ) → A) x : A)

Tactic:
f.commutes x

Premises used: AlgHom.commutes
-- Module: Mathlib.LinearAlgebra.Complex.Module
Goal:
A : Type u_3
inst : Semiring A
inst_1 : Algebra ℝ A
f g : ℂ →ₐ[ℝ] A
h : Eq (α := A) ((f : (a : ℂ) → A) I : A) ((g : (a : ℂ) → A) I : A)
H :
  ∀ (x y : ℝ),
    Eq (α := A) ((f : (a : ℂ) → A) { re := x, im := y : ℂ } : A) ((g : (a : ℂ) → A) { re := x, im := y : ℂ } : A)
⊢ f = g

Tactic:
ext ⟨x, y⟩
-- Module: Mathlib.LinearAlgebra.Complex.Module
Goal:
A : Type u_3
inst : Semiring A
inst_1 : Algebra ℝ A
f g : ℂ →ₐ[ℝ] A
h : Eq (α := A) ((f : (a : ℂ) → A) I : A) ((g : (a : ℂ) → A) I : A)
x y : ℝ
⊢ Eq (α := A) ((f : (a : ℂ) → A) { re := x, im := y : ℂ } : A) ((g : (a : ℂ) → A) { re := x, im := y : ℂ } : A)

Tactic:
simp only [mk_eq_add_mul_I, map_add, AlgHom.map_coe_real_complex, map_mul, h]

Premises used: Complex.mk_eq_add_mul_I, map_add, map_mul, AlgHom.map_coe_real_complex
-- Module: Mathlib.LinearAlgebra.Complex.Module
Goal:
R : Type u_1
S : Type u_2
z z' : ℂ
⊢ ![(z + z').re, (z + z').im] = ![z.re, z.im] + ![z'.re, z'.im]

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Complex.Module
Goal:
R : Type u_1
S : Type u_2
c : ℝ
z : ℂ
⊢ ![(c • z).re, (c • z).im] = HSMul.hSMul (α := ℝ) ((RingHom.id ℝ : (a : ℝ) → ℝ) c : ℝ) ![z.re, z.im]

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Complex.Module
Goal:
R : Type u_1
S : Type u_2
z : ℂ
⊢ (fun (c : Fin 2 → ℝ) ↦ (↑(c 0) : ℂ) + c 1 • I) ((fun (z : ℂ) ↦ ![z.re, z.im]) z) = z

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Complex.Module
Goal:
R : Type u_1
S : Type u_2
c : Fin 2 → ℝ
h : ∀ (i : Fin (Nat.succ 1)), (fun (z : ℂ) ↦ ![z.re, z.im]) ((fun (c : Fin 2 → ℝ) ↦ (↑(c 0) : ℂ) + c 1 • I) c) i = c i
⊢ (fun (z : ℂ) ↦ ![z.re, z.im]) ((fun (c : Fin 2 → ℝ) ↦ (↑(c 0) : ℂ) + c 1 • I) c) = c

Tactic:
ext i
-- Module: Mathlib.LinearAlgebra.Complex.Module
Goal:
R : Type u_1
S : Type u_2
c : Fin 2 → ℝ
i : Fin (Nat.succ 1)
h :
  (fun (z : ℂ) ↦ ![z.re, z.im]) ((fun (c : Fin 2 → ℝ) ↦ (↑(c 0) : ℂ) + c 1 • I) c)
      ((fun (i : Fin (Nat.succ 1)) ↦ i) ⟨0, ⋯⟩) =
    c ((fun (i : Fin (Nat.succ 1)) ↦ i) (⟨0, ⋯⟩ : Fin (Nat.succ 1)))
h₁ :
  (fun (z : ℂ) ↦ ![z.re, z.im]) ((fun (c : Fin 2 → ℝ) ↦ (↑(c 0) : ℂ) + c 1 • I) c)
      ((fun (i : Fin (Nat.succ 1)) ↦ i) ⟨1, ⋯⟩) =
    c ((fun (i : Fin (Nat.succ 1)) ↦ i) (⟨1, ⋯⟩ : Fin (Nat.succ 1)))
⊢ (fun (z : ℂ) ↦ ![z.re, z.im]) ((fun (c : Fin 2 → ℝ) ↦ (↑(c 0) : ℂ) + c 1 • I) c) i = c i

Tactic:
fin_cases i
-- Module: Mathlib.LinearAlgebra.Complex.Module
Goal:
R : Type u_1
S : Type u_2
c : Fin 2 → ℝ
⊢ (fun (z : ℂ) ↦ ![z.re, z.im]) ((fun (c : Fin 2 → ℝ) ↦ (↑(c 0) : ℂ) + c 1 • I) c)
      ((fun (i : Fin (Nat.succ 1)) ↦ i) ⟨0, ⋯⟩) =
    c ((fun (i : Fin (Nat.succ 1)) ↦ i) (⟨0, ⋯⟩ : Fin (Nat.succ 1)))

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Complex.Module
Goal:
R : Type u_1
S : Type u_2
c : Fin 2 → ℝ
⊢ (fun (z : ℂ) ↦ ![z.re, z.im]) ((fun (c : Fin 2 → ℝ) ↦ (↑(c 0) : ℂ) + c 1 • I) c)
      ((fun (i : Fin (Nat.succ 1)) ↦ i) ⟨1, ⋯⟩) =
    c ((fun (i : Fin (Nat.succ 1)) ↦ i) (⟨1, ⋯⟩ : Fin (Nat.succ 1)))

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Complex.Module
Goal:
z : ℂ
⊢ (⇑((basisOneI.repr : (a : ℂ) → Fin 2 →₀ ℝ) z : Fin 2 →₀ ℝ) : (a : Fin 2) → ℝ) = ![z.re, z.im]

Tactic:
rfl

Premises used: Fin.cons, Fin.induction, Fin.cases, Matrix.vecCons, rfl
-- Module: Mathlib.LinearAlgebra.Complex.Module
Goal:
i j : Fin 2
0 :
  Eq (α := ℝ)
    ((((basisOneI.repr : (a : ℂ) → Fin 2 →₀ ℝ) (![1, I] ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩)) : Fin 2 →₀ ℝ) : (a : Fin 2) → ℝ)
        j :
      ℝ)
    ((Finsupp.single ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) 1 : (a : Fin 2) → ℝ) j)
1 :
  Eq (α := ℝ)
    ((((basisOneI.repr : (a : ℂ) → Fin 2 →₀ ℝ) (![1, I] ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩)) : Fin 2 →₀ ℝ) : (a : Fin 2) → ℝ)
        j :
      ℝ)
    ((Finsupp.single ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) 1 : (a : Fin 2) → ℝ) j)
⊢ Eq (α := ℝ) ((((basisOneI.repr : (a : ℂ) → Fin 2 →₀ ℝ) (![1, I] i) : Fin 2 →₀ ℝ) : (a : Fin 2) → ℝ) j : ℝ)
    ((Finsupp.single i 1 : (a : Fin 2) → ℝ) j)

Tactic:
fin_cases i
-- Module: Mathlib.LinearAlgebra.Complex.Module
Goal:
j : Fin 2
0 :
  Eq (α := ℝ)
    ((((basisOneI.repr : (a : ℂ) → Fin 2 →₀ ℝ) (![1, I] ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩)) : Fin 2 →₀ ℝ) : (a : Fin 2) → ℝ)
        ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) :
      ℝ)
    ((Finsupp.single ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) 1 : (a : Fin 2) → ℝ) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) : ℝ)
h :
  Eq (α := ℝ)
    ((((basisOneI.repr : (a : ℂ) → Fin 2 →₀ ℝ) (![1, I] ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩)) : Fin 2 →₀ ℝ) : (a : Fin 2) → ℝ)
        ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) :
      ℝ)
    ((Finsupp.single ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) 1 : (a : Fin 2) → ℝ) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) : ℝ)
⊢ Eq (α := ℝ)
    ((((basisOneI.repr : (a : ℂ) → Fin 2 →₀ ℝ) (![1, I] ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩)) : Fin 2 →₀ ℝ) : (a : Fin 2) → ℝ)
        j :
      ℝ)
    ((Finsupp.single ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) 1 : (a : Fin 2) → ℝ) j)

Tactic:
fin_cases j
-- Module: Mathlib.LinearAlgebra.Complex.Module
Goal:
j : Fin 2
1 :
  Eq (α := ℝ)
    ((((basisOneI.repr : (a : ℂ) → Fin 2 →₀ ℝ) (![1, I] ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩)) : Fin 2 →₀ ℝ) : (a : Fin 2) → ℝ)
        ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) :
      ℝ)
    ((Finsupp.single ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) 1 : (a : Fin 2) → ℝ) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) : ℝ)
h :
  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, ⋯⟩) : ℝ)
⊢ Eq (α := ℝ)
    ((((basisOneI.repr : (a : ℂ) → Fin 2 →₀ ℝ) (![1, I] ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩)) : Fin 2 →₀ ℝ) : (a : Fin 2) → ℝ)
        j :
      ℝ)
    ((Finsupp.single ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) 1 : (a : Fin 2) → ℝ) j)

Tactic:
fin_cases j
-- Module: Mathlib.LinearAlgebra.Complex.Module
Goal:
⊢ Eq (α := ℝ)
    ((((basisOneI.repr : (a : ℂ) → Fin 2 →₀ ℝ) (![1, I] ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩)) : Fin 2 →₀ ℝ) : (a : Fin 2) → ℝ)
        ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) :
      ℝ)
    ((Finsupp.single ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) 1 : (a : Fin 2) → ℝ) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) : ℝ)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Complex.Module
Goal:
⊢ Eq (α := ℝ)
    ((((basisOneI.repr : (a : ℂ) → Fin 2 →₀ ℝ) (![1, I] ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩)) : Fin 2 →₀ ℝ) : (a : Fin 2) → ℝ)
        ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) :
      ℝ)
    ((Finsupp.single ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) 1 : (a : Fin 2) → ℝ) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) : ℝ)

Tactic:
simp
-- 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) ⟨0, ⋯⟩) :
      ℝ)
    ((Finsupp.single ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) 1 : (a : Fin 2) → ℝ) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) : ℝ)

Tactic:
simp