awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Complex.FiniteDimensional (goal)
Goal:
⊢ Module.rank ℚ ℝ = 𝔠
have refine : lift.{0, 0} #ℚ < lift.{0, 0} #ℝ
Tactic: refine (Free.rank_eq_mk_of_infinite_lt ℚ ℝ ?_).trans mk_real
-- Lean 4 proof step from Mathlib.LinearAlgebra.Complex.FiniteDimensional (goal)
Goal:
⊢ Module.rank ℚ ℂ = 𝔠
have refine : Cardinal.lift.{0, 0} #ℚ < Cardinal.lift.{0, 0} #ℂ
Tactic: refine (Free.rank_eq_mk_of_infinite_lt ℚ ℂ ?_).trans Cardinal.mk_complex
-- Lean 4 proof step from Mathlib.LinearAlgebra.Complex.Module (goal)
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 = s • r • x
have a : (r • s • x).re = (s • r • x).re
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Complex.Module (goal)
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
⊢ r • s • x = s • r • x
have a₁ : (r • s • x).im = (s • r • x).im
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Complex.Module (goal)
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 = r • s • x
have a : ((r • s) • x).re = (r • s • x).re
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Complex.Module (goal)
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
⊢ (r • s) • x = r • s • x
have a₁ : ((r • s) • x).im = (r • s • x).im
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Complex.Module (goal)
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 = r • x
have a : (MulOpposite.op r • x).re = (r • x).re
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Complex.Module (goal)
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
⊢ MulOpposite.op r • x = r • x
have a₁ : (MulOpposite.op r • x).im = (r • x).im
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Complex.Module (goal)
Goal:
R : Type u_1
S : Type u_2
inst : Monoid R
inst_1 : MulAction R ℝ
r s : R
x : ℂ
⊢ (r * s) • x = r • s • x
have a : ((r * s) • x).re = (r • s • x).re
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Complex.Module (goal)
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
⊢ (r * s) • x = r • s • x
have a₁ : ((r * s) • x).im = (r • s • x).im
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Complex.Module (goal)
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 = x
have a : (HSMul.hSMul.{u_1, 0, 0} (α := R) 1 x).re = x.re
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Complex.Module (goal)
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
⊢ HSMul.hSMul.{u_1, 0, 0} (α := R) 1 x = x
have a₁ : (HSMul.hSMul.{u_1, 0, 0} (α := R) 1 x).im = x.im
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Complex.Module (goal)
Goal:
R : Type u_1
S : Type u_2
inst : DistribSMul R ℝ
r : R
⊢ HSMul.hSMul (β := ℂ) r 0 = 0
have a : (HSMul.hSMul (β := ℂ) r 0).re = re 0
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Complex.Module (goal)
Goal:
R : Type u_1
S : Type u_2
inst : DistribSMul R ℝ
r : R
a : (HSMul.hSMul (β := ℂ) r 0).re = re 0
⊢ HSMul.hSMul (β := ℂ) r 0 = 0
have a₁ : (HSMul.hSMul (β := ℂ) r 0).im = im 0
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Complex.Module (goal)
Goal:
R : Type u_1
S : Type u_2
inst : DistribSMul R ℝ
r : R
x y : ℂ
⊢ r • (x + y) = r • x + r • y
have a : (r • (x + y)).re = (r • x + r • y).re
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Complex.Module (goal)
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
⊢ r • (x + y) = r • x + r • y
have a₁ : (r • (x + y)).im = (r • x + r • y).im
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Complex.Module (goal)
Goal:
R : Type u_1
S : Type u_2
inst : Semiring R
inst_1 : Module R ℝ
r s : R
x : ℂ
⊢ (r + s) • x = r • x + s • x
have a : ((r + s) • x).re = (r • x + s • x).re
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Complex.Module (goal)
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
⊢ (r + s) • x = r • x + s • x
have a₁ : ((r + s) • x).im = (r • x + s • x).im
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Complex.Module (goal)
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 = 0
have a : (HSMul.hSMul.{u_1, 0, 0} (α := R) 0 r).re = re 0
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Complex.Module (goal)
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
⊢ HSMul.hSMul.{u_1, 0, 0} (α := R) 0 r = 0
have a₁ : (HSMul.hSMul.{u_1, 0, 0} (α := R) 0 r).im = im 0
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Complex.Module (goal)
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 : ℂ } =
    HMul.hMul (β := ℂ) { re := xr, im := xi : ℂ } ((ofRealHom.comp (algebraMap R ℝ) : (a : R) → ℂ) r : ℂ)
have 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
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Complex.Module (goal)
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
⊢ 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 : ℂ)
have 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
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Complex.Module (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : Algebra R ℝ
r : R
x : ℂ
⊢ r • x = HMul.hMul (α := ℂ) ((ofRealHom.comp (algebraMap R ℝ) : (a : R) → ℂ) r : ℂ) x
have a : (r • x).re = (HMul.hMul (α := ℂ) ((ofRealHom.comp (algebraMap R ℝ) : (a : R) → ℂ) r : ℂ) x).re
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Complex.Module (goal)
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
⊢ r • x = HMul.hMul (α := ℂ) ((ofRealHom.comp (algebraMap R ℝ) : (a : R) → ℂ) r : ℂ) x
have a₁ : (r • x).im = (HMul.hMul (α := ℂ) ((ofRealHom.comp (algebraMap R ℝ) : (a : R) → ℂ) r : ℂ) x).im
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.Complex.Module (goal)
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)
⊢ f = g
have H : ∀ (x y : ℝ),
  Eq (α := A) ((f : (a : ℂ) → A) { re := x, im := y : ℂ } : A) ((g : (a : ℂ) → A) { re := x, im := y : ℂ } : A)
Tactic: ext ⟨x, y⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.Complex.Module (goal)
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) = c
have 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
Tactic: ext i
-- Lean 4 proof step from Mathlib.LinearAlgebra.Complex.Module (goal)
Goal:
R : Type u_1
S : Type u_2
c : Fin 2 → ℝ
i : Fin (Nat.succ 1)
⊢ (fun (z : ℂ) ↦ ![z.re, z.im]) ((fun (c : Fin 2 → ℝ) ↦ (↑(c 0) : ℂ) + c 1 • I) c) i = c i
have 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, sorry⟩) =
  c ((fun (i : Fin (Nat.succ 1)) ↦ i) (⟨0, sorry⟩ : Fin (Nat.succ 1)))
Tactic: fin_cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.LinearAlgebra.Complex.Module (goal)
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)))
⊢ (fun (z : ℂ) ↦ ![z.re, z.im]) ((fun (c : Fin 2 → ℝ) ↦ (↑(c 0) : ℂ) + c 1 • I) c) i = c i
have 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, sorry⟩) =
  c ((fun (i : Fin (Nat.succ 1)) ↦ i) (⟨1, sorry⟩ : Fin (Nat.succ 1)))
Tactic: fin_cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.LinearAlgebra.Complex.Module (goal)
Goal:
i j : Fin 2
⊢ Eq (α := ℝ) ((((basisOneI.repr : (a : ℂ) → Fin 2 →₀ ℝ) (![1, I] i) : Fin 2 →₀ ℝ) : (a : Fin 2) → ℝ) j : ℝ)
    ((Finsupp.single i 1 : (a : Fin 2) → ℝ) j)
have 0 : Eq (α := ℝ)
  ((((basisOneI.repr : (a : ℂ) → Fin 2 →₀ ℝ) (![1, I] ((fun (i : Fin 2) ↦ i) ⟨0, sorry⟩)) : Fin 2 →₀ ℝ) : (a : Fin 2) → ℝ)
      j :
    ℝ)
  ((Finsupp.single ((fun (i : Fin 2) ↦ i) ⟨0, sorry⟩) 1 : (a : Fin 2) → ℝ) j)
Tactic: fin_cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.LinearAlgebra.Complex.Module (goal)
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)
⊢ Eq (α := ℝ) ((((basisOneI.repr : (a : ℂ) → Fin 2 →₀ ℝ) (![1, I] i) : Fin 2 →₀ ℝ) : (a : Fin 2) → ℝ) j : ℝ)
    ((Finsupp.single i 1 : (a : Fin 2) → ℝ) j)
have 1 : Eq (α := ℝ)
  ((((basisOneI.repr : (a : ℂ) → Fin 2 →₀ ℝ) (![1, I] ((fun (i : Fin 2) ↦ i) ⟨1, sorry⟩)) : Fin 2 →₀ ℝ) : (a : Fin 2) → ℝ)
      j :
    ℝ)
  ((Finsupp.single ((fun (i : Fin 2) ↦ i) ⟨1, sorry⟩) 1 : (a : Fin 2) → ℝ) j)
Tactic: fin_cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.LinearAlgebra.Complex.Module (goal)
Goal:
j : Fin 2
⊢ 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)
have 0 : Eq (α := ℝ)
  ((((basisOneI.repr : (a : ℂ) → Fin 2 →₀ ℝ) (![1, I] ((fun (i : Fin 2) ↦ i) ⟨0, sorry⟩)) : Fin 2 →₀ ℝ) : (a : Fin 2) → ℝ)
      ((fun (i : Fin 2) ↦ i) ⟨0, sorry⟩) :
    ℝ)
  ((Finsupp.single ((fun (i : Fin 2) ↦ i) ⟨0, sorry⟩) 1 : (a : Fin 2) → ℝ) ((fun (i : Fin 2) ↦ i) ⟨0, sorry⟩) : ℝ)
Tactic: fin_cases j
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.LinearAlgebra.Complex.Module (goal)
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, ⋯⟩) : ℝ)
⊢ 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)
have 0₁ : Eq (α := ℝ)
  ((((basisOneI.repr : (a : ℂ) → Fin 2 →₀ ℝ) (![1, I] ((fun (i : Fin 2) ↦ i) ⟨0, sorry⟩)) : Fin 2 →₀ ℝ) : (a : Fin 2) → ℝ)
      ((fun (i : Fin 2) ↦ i) ⟨1, sorry⟩) :
    ℝ)
  ((Finsupp.single ((fun (i : Fin 2) ↦ i) ⟨0, sorry⟩) 1 : (a : Fin 2) → ℝ) ((fun (i : Fin 2) ↦ i) ⟨1, sorry⟩) : ℝ)
Tactic: fin_cases j
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.LinearAlgebra.Complex.Module (goal)
Goal:
j : Fin 2
⊢ 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)
have 1 : Eq (α := ℝ)
  ((((basisOneI.repr : (a : ℂ) → Fin 2 →₀ ℝ) (![1, I] ((fun (i : Fin 2) ↦ i) ⟨1, sorry⟩)) : Fin 2 →₀ ℝ) : (a : Fin 2) → ℝ)
      ((fun (i : Fin 2) ↦ i) ⟨0, sorry⟩) :
    ℝ)
  ((Finsupp.single ((fun (i : Fin 2) ↦ i) ⟨1, sorry⟩) 1 : (a : Fin 2) → ℝ) ((fun (i : Fin 2) ↦ i) ⟨0, sorry⟩) : ℝ)
Tactic: fin_cases j
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.LinearAlgebra.Complex.Module (goal)
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, ⋯⟩) : ℝ)
⊢ 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)
have 1₁ : Eq (α := ℝ)
  ((((basisOneI.repr : (a : ℂ) → Fin 2 →₀ ℝ) (![1, I] ((fun (i : Fin 2) ↦ i) ⟨1, sorry⟩)) : Fin 2 →₀ ℝ) : (a : Fin 2) → ℝ)
      ((fun (i : Fin 2) ↦ i) ⟨1, sorry⟩) :
    ℝ)
  ((Finsupp.single ((fun (i : Fin 2) ↦ i) ⟨1, sorry⟩) 1 : (a : Fin 2) → ℝ) ((fun (i : Fin 2) ↦ i) ⟨1, sorry⟩) : ℝ)
Tactic: fin_cases j
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.LinearAlgebra.Complex.Module (goal)
Goal:
E : Type u_1
inst : AddCommGroup E
inst_1 : Star E
inst_2 : Module ℂ E
inst_3 : StarModule ℂ E
r : ℝ
a : E
⊢ star (r • a) = star r • star a
have rw : star (HSMul.hSMul (β := ℂ) r 1 • a) = star r • star a
Tactic: rw [← smul_one_smul ℂ r a, star_smul, star_smul, star_one, smul_one_smul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Complex.Module (goal)
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
⊢ star (r • a) = star r • star a
have rw₁ : star (HSMul.hSMul (β := ℂ) r 1) • star a = star r • star a
Tactic: rw [← smul_one_smul ℂ r a, star_smul, star_smul, star_one, smul_one_smul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Complex.Module (goal)
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
⊢ star (r • a) = star r • star a
have rw₂ : HSMul.hSMul (β := ℂ) (star r) (star 1) • star a = star r • star a
Tactic: rw [← smul_one_smul ℂ r a, star_smul, star_smul, star_one, smul_one_smul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Complex.Module (goal)
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
⊢ star (r • a) = star r • star a
have rw₃ : HSMul.hSMul (β := ℂ) (star r) 1 • star a = star r • star a
Tactic: rw [← smul_one_smul ℂ r a, star_smul, star_smul, star_one, smul_one_smul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Complex.Module (goal)
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
⊢ star (r • a) = star r • star a
have rw₄ : star r • star a = star r • star a
Tactic: rw [← smul_one_smul ℂ r a, star_smul, star_smul, star_one, smul_one_smul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Complex.Module (goal)
Goal:
⊢ 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) ℝ)
have 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 : ℝ)
Tactic: ext i j
-- Lean 4 proof step from Mathlib.LinearAlgebra.Complex.Module (goal)
Goal:
i j : Fin 2
⊢ Eq (α := ℝ)
    ((LinearMap.toMatrix basisOneI basisOneI : (a : ℂ →ₗ[ℝ] ℂ) → Matrix (Fin 2) (Fin 2) ℝ)
        (↑(↑conjAe : ℂ ≃ₗ[ℝ] ℂ) : ℂ →ₗ[ℝ] ℂ) i j :
      ℝ)
    (!![1, 0; 0, -1] i j : ℝ)
have a : Eq (α := ℝ)
  ((LinearMap.toMatrix basisOneI basisOneI : (a : ℂ →ₗ[ℝ] ℂ) → Matrix (Fin 2) (Fin 2) ℝ)
      (↑(↑conjAe : ℂ ≃ₗ[ℝ] ℂ) : ℂ →ₗ[ℝ] ℂ) ((fun (i : Fin 2) ↦ i) ⟨0, sorry⟩) j :
    ℝ)
  (!![1, 0; 0, -1] ((fun (i : Fin 2) ↦ i) ⟨0, sorry⟩) j : ℝ)
Tactic: fin_cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.LinearAlgebra.Complex.Module (goal)
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 : ℝ)
⊢ Eq (α := ℝ)
    ((LinearMap.toMatrix basisOneI basisOneI : (a : ℂ →ₗ[ℝ] ℂ) → Matrix (Fin 2) (Fin 2) ℝ)
        (↑(↑conjAe : ℂ ≃ₗ[ℝ] ℂ) : ℂ →ₗ[ℝ] ℂ) i j :
      ℝ)
    (!![1, 0; 0, -1] i j : ℝ)
have a₁ : Eq (α := ℝ)
  ((LinearMap.toMatrix basisOneI basisOneI : (a : ℂ →ₗ[ℝ] ℂ) → Matrix (Fin 2) (Fin 2) ℝ)
      (↑(↑conjAe : ℂ ≃ₗ[ℝ] ℂ) : ℂ →ₗ[ℝ] ℂ) ((fun (i : Fin 2) ↦ i) ⟨1, sorry⟩) j :
    ℝ)
  (!![1, 0; 0, -1] ((fun (i : Fin 2) ↦ i) ⟨1, sorry⟩) j : ℝ)
Tactic: fin_cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.LinearAlgebra.Complex.Module (goal)
Goal:
j : Fin 2
⊢ 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 : ℝ)
have a : Eq (α := ℝ)
  ((LinearMap.toMatrix basisOneI basisOneI : (a : ℂ →ₗ[ℝ] ℂ) → Matrix (Fin 2) (Fin 2) ℝ)
      (↑(↑conjAe : ℂ ≃ₗ[ℝ] ℂ) : ℂ →ₗ[ℝ] ℂ) ((fun (i : Fin 2) ↦ i) ⟨0, sorry⟩) ((fun (i : Fin 2) ↦ i) ⟨0, sorry⟩) :
    ℝ)
  (!![1, 0; 0, -1] ((fun (i : Fin 2) ↦ i) ⟨0, sorry⟩) ((fun (i : Fin 2) ↦ i) ⟨0, sorry⟩) : ℝ)
Tactic: fin_cases j
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.LinearAlgebra.Complex.Module (goal)
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, ⋯⟩) : ℝ)
⊢ 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 : ℝ)
have a₁ : Eq (α := ℝ)
  ((LinearMap.toMatrix basisOneI basisOneI : (a : ℂ →ₗ[ℝ] ℂ) → Matrix (Fin 2) (Fin 2) ℝ)
      (↑(↑conjAe : ℂ ≃ₗ[ℝ] ℂ) : ℂ →ₗ[ℝ] ℂ) ((fun (i : Fin 2) ↦ i) ⟨0, sorry⟩) ((fun (i : Fin 2) ↦ i) ⟨1, sorry⟩) :
    ℝ)
  (!![1, 0; 0, -1] ((fun (i : Fin 2) ↦ i) ⟨0, sorry⟩) ((fun (i : Fin 2) ↦ i) ⟨1, sorry⟩) : ℝ)
Tactic: fin_cases j
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.LinearAlgebra.Complex.Module (goal)
Goal:
j : Fin 2
⊢ 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 : ℝ)
have a : Eq (α := ℝ)
  ((LinearMap.toMatrix basisOneI basisOneI : (a : ℂ →ₗ[ℝ] ℂ) → Matrix (Fin 2) (Fin 2) ℝ)
      (↑(↑conjAe : ℂ ≃ₗ[ℝ] ℂ) : ℂ →ₗ[ℝ] ℂ) ((fun (i : Fin 2) ↦ i) ⟨1, sorry⟩) ((fun (i : Fin 2) ↦ i) ⟨0, sorry⟩) :
    ℝ)
  (!![1, 0; 0, -1] ((fun (i : Fin 2) ↦ i) ⟨1, sorry⟩) ((fun (i : Fin 2) ↦ i) ⟨0, sorry⟩) : ℝ)
Tactic: fin_cases j
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.LinearAlgebra.Complex.Module (goal)
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, ⋯⟩) : ℝ)
⊢ 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 : ℝ)
have a₁ : Eq (α := ℝ)
  ((LinearMap.toMatrix basisOneI basisOneI : (a : ℂ →ₗ[ℝ] ℂ) → Matrix (Fin 2) (Fin 2) ℝ)
      (↑(↑conjAe : ℂ ≃ₗ[ℝ] ℂ) : ℂ →ₗ[ℝ] ℂ) ((fun (i : Fin 2) ↦ i) ⟨1, sorry⟩) ((fun (i : Fin 2) ↦ i) ⟨1, sorry⟩) :
    ℝ)
  (!![1, 0; 0, -1] ((fun (i : Fin 2) ↦ i) ⟨1, sorry⟩) ((fun (i : Fin 2) ↦ i) ⟨1, sorry⟩) : ℝ)
Tactic: fin_cases j
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.LinearAlgebra.Complex.Module (goal)
Goal:
f : ℂ →ₐ[ℝ] ℂ
⊢ HPow.hPow (α := ℂ) (β := ℕ) ((f : (a : ℂ) → ℂ) I : ℂ) 2 = HPow.hPow (β := ℕ) I 2
have rw : (f : (a : ℂ) → ℂ) (HPow.hPow (β := ℕ) I 2) = HPow.hPow (β := ℕ) I 2
Tactic: rw [← map_pow, I_sq, map_neg, map_one]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Complex.Module (goal)
Goal:
f : ℂ →ₐ[ℝ] ℂ
rw : (f : (a : ℂ) → ℂ) (HPow.hPow (β := ℕ) I 2) = HPow.hPow (β := ℕ) I 2
⊢ HPow.hPow (α := ℂ) (β := ℕ) ((f : (a : ℂ) → ℂ) I : ℂ) 2 = HPow.hPow (β := ℕ) I 2
have rw₁ : Eq (α := ℂ) ((f : (a : ℂ) → ℂ) (-1) : ℂ) (-1 : ℂ)
Tactic: rw [← map_pow, I_sq, map_neg, map_one]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Complex.Module (goal)
Goal:
f : ℂ →ₐ[ℝ] ℂ
rw : (f : (a : ℂ) → ℂ) (HPow.hPow (β := ℕ) I 2) = HPow.hPow (β := ℕ) I 2
rw₁ : Eq (α := ℂ) ((f : (a : ℂ) → ℂ) (-1) : ℂ) (-1 : ℂ)
⊢ HPow.hPow (α := ℂ) (β := ℕ) ((f : (a : ℂ) → ℂ) I : ℂ) 2 = HPow.hPow (β := ℕ) I 2
have rw₂ : Eq (α := ℂ) (-(f : (a : ℂ) → ℂ) 1 : ℂ) (-1 : ℂ)
Tactic: rw [← map_pow, I_sq, map_neg, map_one]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Complex.Module (goal)
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 : ℂ)
⊢ HPow.hPow (α := ℂ) (β := ℕ) ((f : (a : ℂ) → ℂ) I : ℂ) 2 = HPow.hPow (β := ℕ) I 2
have rw₃ : Eq (α := ℂ) (-1) (-1)
Tactic: rw [← map_pow, I_sq, map_neg, map_one]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Complex.Module (goal)
Goal:
f : ℂ →ₐ[ℝ] ℂ
⊢ f = AlgHom.id ℝ ℂ ∨ f = (↑conjAe : ℂ →ₐ[ℝ] ℂ)
have refine_1 : (f : (a : ℂ) → ℂ) I = I → f = AlgHom.id ℝ ℂ
Tactic: refine
      (eq_or_eq_neg_of_sq_eq_sq (f I) I <| by rw [← map_pow, I_sq, map_neg, map_one]).imp ?_ ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.Complex.Module (goal)
Goal:
f : ℂ →ₐ[ℝ] ℂ
refine_1 : (f : (a : ℂ) → ℂ) I = I → f = AlgHom.id ℝ ℂ
⊢ f = AlgHom.id ℝ ℂ ∨ f = (↑conjAe : ℂ →ₐ[ℝ] ℂ)
have refine_2 : (f : (a : ℂ) → ℂ) I = -I → 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 ?_ ?_