awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.Transvection.Basic (goal)
Goal:
R : Type u_3
V : Type u_4
inst : CommRing R
inst_1 : AddCommGroup V
inst_2 : Module R V
inst_3 : Free R V
inst_4 : Module.Finite R V
f : Dual R V
v : V
hR : Nontrivial R
n : ℕ := finrank R V
b : Basis (Fin n) R V
S : Type := MvPolynomial (Fin n ⊕ Fin n) ℤ
γ : S →+* R :=
  (↑(MvPolynomial.aeval.{0, u_3, 0} (R := ℤ) (S₁ := R) (σ := Fin n ⊕ Fin n)
          (Sum.elim (fun (i : Fin n) ↦ (f : (a : V) → R) ((b : (a : Fin n) → V) i : V)) fun (i : Fin n) ↦
            (b.coord i : (a : V) → R) v) :
        MvPolynomial (Fin n ⊕ Fin n) ℤ →ₐ[ℤ] R) :
    S →+* R)
this : IsDomain S
x : Algebra S R := γ.toAlgebra
x_1 : Module S V := compHom V γ
h : IsScalarTower S R V
ε : (Fin n → S) →ₗ[S] V := Fintype.linearCombination S fun (i : Fin n) ↦ (b : (a : Fin n) → V) i
ibc : IsBaseChange R ε
M : Type := Fin n → S
hε :
  ∀ (i : Fin n),
    Eq (α := V) ((ε : (a : Fin n → S) → V) (Pi.single (M := fun (a : Fin n) ↦ S) i 1) : V) ((b : (a : Fin n) → V) i : V)
fM : Dual S M := Fintype.linearCombination S fun (i : Fin n) ↦ MvPolynomial.X (Sum.inl i)
vM : M := fun (i : Fin n) ↦ MvPolynomial.X (Sum.inr i)
hf : (ibc.toDual : (a : Dual S (Fin n → S)) → Dual R V) fM = f
hv : (ε : (a : Fin n → S) → V) vM = v
⊢ (LinearMap.det : (a : V →ₗ[R] V) → R) (transvection f v) =
    HAdd.hAdd (α := R) (β := R) (1 : R) ((f : (a : V) → R) v : R)
have inr : (algebraMap S R : (a : S) → R) (HAdd.hAdd (α := S) (β := S) (1 : S) ((fM : (a : Fin n → S) → S) vM : S)) =
  HAdd.hAdd (α := R) (β := R) (1 : R)
    ((((ibc.toDual : (a : Dual S (Fin n → S)) → Dual R V) fM : Dual R V) : (a : V) → R)
        ((ε : (a : Fin n → S) → V) vM : V) :
      R)
Tactic: rw [← hf, ← hv, ← IsBaseChange.transvection, det_endHom, det_ofDomain]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Transvection.Basic (goal)
Goal:
R : Type u_3
V : Type u_4
inst : CommRing R
inst_1 : AddCommGroup V
inst_2 : Module R V
inst_3 : Free R V
inst_4 : Module.Finite R V
f : Dual R V
v : V
hR : Nontrivial R
n : ℕ := finrank R V
b : Basis (Fin n) R V
S : Type := MvPolynomial (Fin n ⊕ Fin n) ℤ
γ : S →+* R :=
  (↑(MvPolynomial.aeval.{0, u_3, 0} (R := ℤ) (S₁ := R) (σ := Fin n ⊕ Fin n)
          (Sum.elim (fun (i : Fin n) ↦ (f : (a : V) → R) ((b : (a : Fin n) → V) i : V)) fun (i : Fin n) ↦
            (b.coord i : (a : V) → R) v) :
        MvPolynomial (Fin n ⊕ Fin n) ℤ →ₐ[ℤ] R) :
    S →+* R)
this : IsDomain S
x : Algebra S R := γ.toAlgebra
x_1 : Module S V := compHom V γ
h : IsScalarTower S R V
ε : (Fin n → S) →ₗ[S] V := Fintype.linearCombination S fun (i : Fin n) ↦ (b : (a : Fin n) → V) i
ibc : IsBaseChange R ε
M : Type := Fin n → S
hε :
  ∀ (i : Fin n),
    Eq (α := V) ((ε : (a : Fin n → S) → V) (Pi.single (M := fun (a : Fin n) ↦ S) i 1) : V) ((b : (a : Fin n) → V) i : V)
fM : Dual S M := Fintype.linearCombination S fun (i : Fin n) ↦ MvPolynomial.X (Sum.inl i)
vM : M := fun (i : Fin n) ↦ MvPolynomial.X (Sum.inr i)
hf : (ibc.toDual : (a : Dual S (Fin n → S)) → Dual R V) fM = f
hv : (ε : (a : Fin n → S) → V) vM = v
⊢ (algebraMap S R : (a : S) → R) (HAdd.hAdd (α := S) (β := S) (1 : S) ((fM : (a : Fin n → S) → S) vM : S)) =
    HAdd.hAdd (α := R) (β := R) (1 : R)
      ((((ibc.toDual : (a : Dual S (Fin n → S)) → Dual R V) fM : Dual R V) : (a : V) → R)
          ((ε : (a : Fin n → S) → V) vM : V) :
        R)
have inr : HAdd.hAdd (α := R) (β := R) ((algebraMap S R : (a : S) → R) 1 : R)
    ((algebraMap S R : (a : S) → R) ((fM : (a : Fin n → S) → S) vM : S) : R) =
  HAdd.hAdd (α := R) (β := R) (1 : R)
    ((((ibc.toDual : (a : Dual S (Fin n → S)) → Dual R V) fM : Dual R V) : (a : V) → R)
        ((ε : (a : Fin n → S) → V) vM : V) :
      R)
Tactic: rw [map_add, map_one, add_right_inj, toDual_comp_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Transvection.Basic (goal)
Goal:
R : Type u_3
V : Type u_4
inst : CommRing R
inst_1 : AddCommGroup V
inst_2 : Module R V
inst_3 : Free R V
inst_4 : Module.Finite R V
f : Dual R V
v : V
hR : Nontrivial R
n : ℕ := finrank R V
b : Basis (Fin n) R V
S : Type := MvPolynomial (Fin n ⊕ Fin n) ℤ
γ : S →+* R :=
  (↑(MvPolynomial.aeval.{0, u_3, 0} (R := ℤ) (S₁ := R) (σ := Fin n ⊕ Fin n)
          (Sum.elim (fun (i : Fin n) ↦ (f : (a : V) → R) ((b : (a : Fin n) → V) i : V)) fun (i : Fin n) ↦
            (b.coord i : (a : V) → R) v) :
        MvPolynomial (Fin n ⊕ Fin n) ℤ →ₐ[ℤ] R) :
    S →+* R)
this : IsDomain S
x : Algebra S R := γ.toAlgebra
x_1 : Module S V := compHom V γ
h : IsScalarTower S R V
ε : (Fin n → S) →ₗ[S] V := Fintype.linearCombination S fun (i : Fin n) ↦ (b : (a : Fin n) → V) i
ibc : IsBaseChange R ε
M : Type := Fin n → S
hε :
  ∀ (i : Fin n),
    Eq (α := V) ((ε : (a : Fin n → S) → V) (Pi.single (M := fun (a : Fin n) ↦ S) i 1) : V) ((b : (a : Fin n) → V) i : V)
fM : Dual S M := Fintype.linearCombination S fun (i : Fin n) ↦ MvPolynomial.X (Sum.inl i)
vM : M := fun (i : Fin n) ↦ MvPolynomial.X (Sum.inr i)
hf : (ibc.toDual : (a : Dual S (Fin n → S)) → Dual R V) fM = f
hv : (ε : (a : Fin n → S) → V) vM = v
inr :
  HAdd.hAdd (α := R) (β := R) ((algebraMap S R : (a : S) → R) 1 : R)
      ((algebraMap S R : (a : S) → R) ((fM : (a : Fin n → S) → S) vM : S) : R) =
    HAdd.hAdd (α := R) (β := R) (1 : R)
      ((((ibc.toDual : (a : Dual S (Fin n → S)) → Dual R V) fM : Dual R V) : (a : V) → R)
          ((ε : (a : Fin n → S) → V) vM : V) :
        R)
⊢ (algebraMap S R : (a : S) → R) (HAdd.hAdd (α := S) (β := S) (1 : S) ((fM : (a : Fin n → S) → S) vM : S)) =
    HAdd.hAdd (α := R) (β := R) (1 : R)
      ((((ibc.toDual : (a : Dual S (Fin n → S)) → Dual R V) fM : Dual R V) : (a : V) → R)
          ((ε : (a : Fin n → S) → V) vM : V) :
        R)
have inr₁ : HAdd.hAdd (α := R) (β := R) (1 : R) ((algebraMap S R : (a : S) → R) ((fM : (a : Fin n → S) → S) vM : S) : R) =
  HAdd.hAdd (α := R) (β := R) (1 : R)
    ((((ibc.toDual : (a : Dual S (Fin n → S)) → Dual R V) fM : Dual R V) : (a : V) → R)
        ((ε : (a : Fin n → S) → V) vM : V) :
      R)
Tactic: rw [map_add, map_one, add_right_inj, toDual_comp_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Transvection.Basic (goal)
Goal:
R : Type u_3
V : Type u_4
inst : CommRing R
inst_1 : AddCommGroup V
inst_2 : Module R V
inst_3 : Free R V
inst_4 : Module.Finite R V
f : Dual R V
v : V
hR : Nontrivial R
n : ℕ := finrank R V
b : Basis (Fin n) R V
S : Type := MvPolynomial (Fin n ⊕ Fin n) ℤ
γ : S →+* R :=
  (↑(MvPolynomial.aeval.{0, u_3, 0} (R := ℤ) (S₁ := R) (σ := Fin n ⊕ Fin n)
          (Sum.elim (fun (i : Fin n) ↦ (f : (a : V) → R) ((b : (a : Fin n) → V) i : V)) fun (i : Fin n) ↦
            (b.coord i : (a : V) → R) v) :
        MvPolynomial (Fin n ⊕ Fin n) ℤ →ₐ[ℤ] R) :
    S →+* R)
this : IsDomain S
x : Algebra S R := γ.toAlgebra
x_1 : Module S V := compHom V γ
h : IsScalarTower S R V
ε : (Fin n → S) →ₗ[S] V := Fintype.linearCombination S fun (i : Fin n) ↦ (b : (a : Fin n) → V) i
ibc : IsBaseChange R ε
M : Type := Fin n → S
hε :
  ∀ (i : Fin n),
    Eq (α := V) ((ε : (a : Fin n → S) → V) (Pi.single (M := fun (a : Fin n) ↦ S) i 1) : V) ((b : (a : Fin n) → V) i : V)
fM : Dual S M := Fintype.linearCombination S fun (i : Fin n) ↦ MvPolynomial.X (Sum.inl i)
vM : M := fun (i : Fin n) ↦ MvPolynomial.X (Sum.inr i)
hf : (ibc.toDual : (a : Dual S (Fin n → S)) → Dual R V) fM = f
hv : (ε : (a : Fin n → S) → V) vM = v
inr :
  HAdd.hAdd (α := R) (β := R) ((algebraMap S R : (a : S) → R) 1 : R)
      ((algebraMap S R : (a : S) → R) ((fM : (a : Fin n → S) → S) vM : S) : R) =
    HAdd.hAdd (α := R) (β := R) (1 : R)
      ((((ibc.toDual : (a : Dual S (Fin n → S)) → Dual R V) fM : Dual R V) : (a : V) → R)
          ((ε : (a : Fin n → S) → V) vM : V) :
        R)
inr₁ :
  HAdd.hAdd (α := R) (β := R) (1 : R) ((algebraMap S R : (a : S) → R) ((fM : (a : Fin n → S) → S) vM : S) : R) =
    HAdd.hAdd (α := R) (β := R) (1 : R)
      ((((ibc.toDual : (a : Dual S (Fin n → S)) → Dual R V) fM : Dual R V) : (a : V) → R)
          ((ε : (a : Fin n → S) → V) vM : V) :
        R)
⊢ (algebraMap S R : (a : S) → R) (HAdd.hAdd (α := S) (β := S) (1 : S) ((fM : (a : Fin n → S) → S) vM : S)) =
    HAdd.hAdd (α := R) (β := R) (1 : R)
      ((((ibc.toDual : (a : Dual S (Fin n → S)) → Dual R V) fM : Dual R V) : (a : V) → R)
          ((ε : (a : Fin n → S) → V) vM : V) :
        R)
have inr₂ : Eq (α := R) ((algebraMap S R : (a : S) → R) ((fM : (a : Fin n → S) → S) vM : S) : R)
  ((((ibc.toDual : (a : Dual S (Fin n → S)) → Dual R V) fM : Dual R V) : (a : V) → R)
      ((ε : (a : Fin n → S) → V) vM : V) :
    R)
Tactic: rw [map_add, map_one, add_right_inj, toDual_comp_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Transvection.Basic (goal)
Goal:
R : Type u_3
V : Type u_4
inst : CommRing R
inst_1 : AddCommGroup V
inst_2 : Module R V
inst_3 : Free R V
inst_4 : Module.Finite R V
f : Dual R V
v : V
hR : Nontrivial R
n : ℕ := finrank R V
b : Basis (Fin n) R V
S : Type := MvPolynomial (Fin n ⊕ Fin n) ℤ
γ : S →+* R :=
  (↑(MvPolynomial.aeval.{0, u_3, 0} (R := ℤ) (S₁ := R) (σ := Fin n ⊕ Fin n)
          (Sum.elim (fun (i : Fin n) ↦ (f : (a : V) → R) ((b : (a : Fin n) → V) i : V)) fun (i : Fin n) ↦
            (b.coord i : (a : V) → R) v) :
        MvPolynomial (Fin n ⊕ Fin n) ℤ →ₐ[ℤ] R) :
    S →+* R)
this : IsDomain S
x : Algebra S R := γ.toAlgebra
x_1 : Module S V := compHom V γ
h : IsScalarTower S R V
ε : (Fin n → S) →ₗ[S] V := Fintype.linearCombination S fun (i : Fin n) ↦ (b : (a : Fin n) → V) i
ibc : IsBaseChange R ε
M : Type := Fin n → S
hε :
  ∀ (i : Fin n),
    Eq (α := V) ((ε : (a : Fin n → S) → V) (Pi.single (M := fun (a : Fin n) ↦ S) i 1) : V) ((b : (a : Fin n) → V) i : V)
fM : Dual S M := Fintype.linearCombination S fun (i : Fin n) ↦ MvPolynomial.X (Sum.inl i)
vM : M := fun (i : Fin n) ↦ MvPolynomial.X (Sum.inr i)
hf : (ibc.toDual : (a : Dual S (Fin n → S)) → Dual R V) fM = f
hv : (ε : (a : Fin n → S) → V) vM = v
inr :
  HAdd.hAdd (α := R) (β := R) ((algebraMap S R : (a : S) → R) 1 : R)
      ((algebraMap S R : (a : S) → R) ((fM : (a : Fin n → S) → S) vM : S) : R) =
    HAdd.hAdd (α := R) (β := R) (1 : R)
      ((((ibc.toDual : (a : Dual S (Fin n → S)) → Dual R V) fM : Dual R V) : (a : V) → R)
          ((ε : (a : Fin n → S) → V) vM : V) :
        R)
inr₁ :
  HAdd.hAdd (α := R) (β := R) (1 : R) ((algebraMap S R : (a : S) → R) ((fM : (a : Fin n → S) → S) vM : S) : R) =
    HAdd.hAdd (α := R) (β := R) (1 : R)
      ((((ibc.toDual : (a : Dual S (Fin n → S)) → Dual R V) fM : Dual R V) : (a : V) → R)
          ((ε : (a : Fin n → S) → V) vM : V) :
        R)
inr₂ :
  Eq (α := R) ((algebraMap S R : (a : S) → R) ((fM : (a : Fin n → S) → S) vM : S) : R)
    ((((ibc.toDual : (a : Dual S (Fin n → S)) → Dual R V) fM : Dual R V) : (a : V) → R)
        ((ε : (a : Fin n → S) → V) vM : V) :
      R)
⊢ (algebraMap S R : (a : S) → R) (HAdd.hAdd (α := S) (β := S) (1 : S) ((fM : (a : Fin n → S) → S) vM : S)) =
    HAdd.hAdd (α := R) (β := R) (1 : R)
      ((((ibc.toDual : (a : Dual S (Fin n → S)) → Dual R V) fM : Dual R V) : (a : V) → R)
          ((ε : (a : Fin n → S) → V) vM : V) :
        R)
have inr₃ : Eq (α := R) ((algebraMap S R : (a : S) → R) ((fM : (a : Fin n → S) → S) vM : S) : R)
  ((algebraMap S R : (a : S) → R) ((fM : (a : Fin n → S) → S) vM : S) : R)
Tactic: rw [map_add, map_one, add_right_inj, toDual_comp_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Transvection.Basic (goal)
Goal:
R : Type u_3
V : Type u_4
inst : CommRing R
inst_1 : AddCommGroup V
inst_2 : Module R V
f : Dual R V
v : V
hfv : Eq.{u_3 + 1} (α := R) ((f : (a : V) → R) v : R) (0 : R)
⊢ Eq.{u_3 + 1} (α := Rˣ) ((LinearEquiv.det : (a : V ≃ₗ[R] V) → Rˣ) (LinearEquiv.transvection hfv) : Rˣ) (1 : Rˣ)
have rw : Eq.{u_3 + 1} (α := R) ((LinearMap.det : (a : V →ₗ[R] V) → R) (transvection f v) : R) (1 : R)
Tactic: rw [← Units.val_inj, LinearEquiv.coe_det,
    LinearEquiv.transvection.coe_toLinearMap hfv, Units.val_one]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Transvection.Basic (goal)
Goal:
R : Type u_3
V : Type u_4
inst : CommRing R
inst_1 : AddCommGroup V
inst_2 : Module R V
f : Dual R V
v : V
hfv : Eq.{u_3 + 1} (α := R) ((f : (a : V) → R) v : R) (0 : R)
⊢ Eq.{u_3 + 1} (α := R) ((LinearMap.det : (a : V →ₗ[R] V) → R) (transvection f v) : R) (1 : R)
have by_contra! : ∀ (h : Ne.{u_3 + 1} (α := R) ((LinearMap.det : (a : V →ₗ[R] V) → R) (transvection f v) : R) (1 : R)), False
Tactic: by_contra! h
-- Lean 4 proof step from Mathlib.LinearAlgebra.Transvection.Basic (hypothesis)
Goal:
R : Type u_3
V : Type u_4
inst : CommRing R
inst_1 : AddCommGroup V
inst_2 : Module R V
f : Dual R V
v : V
hfv : Eq.{u_3 + 1} (α := R) ((f : (a : V) → R) v : R) (0 : R)
h : Ne.{u_3 + 1} (α := R) ((LinearMap.det : (a : V →ₗ[R] V) → R) (transvection f v) : R) (1 : R)
⊢ False
have this : Free R V
Tactic: have : Free R V := Free.of_det_ne_one h
-- Lean 4 proof step from Mathlib.LinearAlgebra.Transvection.Basic (hypothesis)
Goal:
R : Type u_3
V : Type u_4
inst : CommRing R
inst_1 : AddCommGroup V
inst_2 : Module R V
f : Dual R V
v : V
hfv : Eq.{u_3 + 1} (α := R) ((f : (a : V) → R) v : R) (0 : R)
h : Ne.{u_3 + 1} (α := R) ((LinearMap.det : (a : V →ₗ[R] V) → R) (transvection f v) : R) (1 : R)
this : Free R V
⊢ False
have this₁ : Module.Finite R V
Tactic: have : Module.Finite R V := finite_of_det_ne_one h
-- Lean 4 proof step from Mathlib.LinearAlgebra.Transvection.Basic (goal)
Goal:
R : Type u_3
V : Type u_4
inst : CommRing R
inst_1 : AddCommGroup V
inst_2 : Module R V
f : Dual R V
v : V
hfv : Eq.{u_3 + 1} (α := R) ((f : (a : V) → R) v : R) (0 : R)
h : Ne.{u_3 + 1} (α := R) ((LinearMap.det : (a : V →ₗ[R] V) → R) (transvection f v) : R) (1 : R)
this_1 : Free R V
this : Module.Finite R V
⊢ False
have apply : Eq.{u_3 + 1} (α := R) ((LinearMap.det : (a : V →ₗ[R] V) → R) (transvection f v) : R) (1 : R)
Tactic: apply h
-- Lean 4 proof step from Mathlib.LinearAlgebra.Transvection.Basic (goal)
Goal:
R : Type u_3
V : Type u_4
inst : CommRing R
inst_1 : AddCommGroup V
inst_2 : Module R V
f : Dual R V
v : V
hfv : Eq.{u_3 + 1} (α := R) ((f : (a : V) → R) v : R) (0 : R)
h : Ne.{u_3 + 1} (α := R) ((LinearMap.det : (a : V →ₗ[R] V) → R) (transvection f v) : R) (1 : R)
this_1 : Free R V
this : Module.Finite R V
⊢ Eq.{u_3 + 1} (α := R) ((LinearMap.det : (a : V →ₗ[R] V) → R) (transvection f v) : R) (1 : R)
have rw : HAdd.hAdd (α := R) (β := R) (1 : R) ((f : (a : V) → R) v : R) = 1
Tactic: rw [transvection.det, hfv, add_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Transvection.Basic (goal)
Goal:
R : Type u_3
V : Type u_4
inst : CommRing R
inst_1 : AddCommGroup V
inst_2 : Module R V
f : Dual R V
v : V
hfv : Eq.{u_3 + 1} (α := R) ((f : (a : V) → R) v : R) (0 : R)
h : Ne.{u_3 + 1} (α := R) ((LinearMap.det : (a : V →ₗ[R] V) → R) (transvection f v) : R) (1 : R)
this_1 : Free R V
this : Module.Finite R V
rw : HAdd.hAdd (α := R) (β := R) (1 : R) ((f : (a : V) → R) v : R) = 1
⊢ Eq.{u_3 + 1} (α := R) ((LinearMap.det : (a : V →ₗ[R] V) → R) (transvection f v) : R) (1 : R)
have rw₁ : HAdd.hAdd (α := R) 1 0 = 1
Tactic: rw [transvection.det, hfv, add_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.Transvection.Basic (goal)
Goal:
R : Type u_3
V : Type u_4
inst : CommRing R
inst_1 : AddCommGroup V
inst_2 : Module R V
f : Dual R V
v : V
hfv : Eq.{u_3 + 1} (α := R) ((f : (a : V) → R) v : R) (0 : R)
h : Ne.{u_3 + 1} (α := R) ((LinearMap.det : (a : V →ₗ[R] V) → R) (transvection f v) : R) (1 : R)
this_1 : Free R V
this : Module.Finite R V
rw : HAdd.hAdd (α := R) (β := R) (1 : R) ((f : (a : V) → R) v : R) = 1
rw₁ : HAdd.hAdd (α := R) 1 0 = 1
⊢ Eq.{u_3 + 1} (α := R) ((LinearMap.det : (a : V →ₗ[R] V) → R) (transvection f v) : R) (1 : R)
have rw₂ : Eq.{u_3 + 1} (α := R) 1 1
Tactic: rw [transvection.det, hfv, add_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.UnitaryGroup (goal)
Goal:
n : Type u
inst : DecidableEq n
inst_1 : Fintype n
α : Type v
inst_2 : CommRing α
inst_3 : StarRing α
A : Matrix n n α
⊢ Membership.mem (γ := Submonoid (Matrix n n α)) (unitaryGroup n α) A ↔ A * star A = 1
have refine : ∀ (hA : A * star A = 1), star A * A = 1
Tactic: refine ⟨And.right, fun hA => ⟨?_, hA⟩⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.UnitaryGroup (goal)
Goal:
n : Type u
inst : DecidableEq n
inst_1 : Fintype n
α : Type v
inst_2 : CommRing α
inst_3 : StarRing α
A : Matrix n n α
⊢ Membership.mem (γ := Submonoid (Matrix n n α)) (unitaryGroup n α) A ↔ star A * A = 1
have refine : ∀ (hA : star A * A = 1), A * star A = 1
Tactic: refine ⟨And.left, fun hA => ⟨hA, ?_⟩⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.UnitaryGroup (goal)
Goal:
n : Type u
inst : DecidableEq n
inst_1 : Fintype n
α : Type v
inst_2 : CommRing α
inst_3 : StarRing α
A : Matrix n n α
hA : star A * A = 1
⊢ A * star A = 1
have rwa : ∀ (hA : A * star A = 1), A * star A = 1
Tactic: rwa [mul_eq_one_comm] at hA
Cleared hypotheses: hA
-- Lean 4 proof step from Mathlib.LinearAlgebra.UnitaryGroup (goal)
Goal:
n : Type u
inst : DecidableEq n
inst_1 : Fintype n
α : Type v
inst_2 : CommRing α
inst_3 : StarRing α
A : Matrix n n α
hA : Membership.mem (γ := Submonoid (Matrix n n α)) (unitaryGroup n α) A
⊢ Membership.mem (γ := Submonoid α) (unitary α) A.det
have left : star A.det * A.det = 1
Tactic: constructor
-- Lean 4 proof step from Mathlib.LinearAlgebra.UnitaryGroup (goal)
Goal:
n : Type u
inst : DecidableEq n
inst_1 : Fintype n
α : Type v
inst_2 : CommRing α
inst_3 : StarRing α
A : Matrix n n α
hA : Membership.mem (γ := Submonoid (Matrix n n α)) (unitaryGroup n α) A
left : star A.det * A.det = 1
⊢ Membership.mem (γ := Submonoid α) (unitary α) A.det
have right : A.det * star A.det = 1
Tactic: constructor
-- Lean 4 proof step from Mathlib.LinearAlgebra.UnitaryGroup (goal)
Goal:
n : Type u
inst : DecidableEq n
inst_1 : Fintype n
R : Type u_1
m : Type u_2
inst_2 : Semiring R
inst_3 : StarRing R
inst_4 : Fintype m
inst_5 : DecidableEq m
U₁ : Matrix n n R
U₂ : Matrix m m R
hU₁ : Membership.mem (γ := Submonoid (Matrix n n R)) (unitary (Matrix n n R)) U₁
hU₂ : Membership.mem (γ := Submonoid (Matrix m m R)) (unitary (Matrix m m R)) U₂
⊢ Membership.mem (γ := Submonoid (Matrix (n × m) (n × m) R)) (unitary (Matrix (n × m) (n × m) R))
    (kroneckerMap (fun (x1 x2 : R) ↦ x1 * x2) U₁ U₂)
have simp_rw : HMul.hMul (α := Matrix (n × m) (n × m) R)
      (submatrix (kroneckerMap (fun (x1 x2 : R) ↦ x1 * x2) U₂ᴴ U₁ᴴ) Prod.swap Prod.swap)
      (kroneckerMap (fun (x1 x2 : R) ↦ x1 * x2) U₁ U₂) =
    1 ∧
  HMul.hMul (α := Matrix (n × m) (n × m) R) (kroneckerMap (fun (x1 x2 : R) ↦ x1 * x2) U₁ U₂)
      (submatrix (kroneckerMap (fun (x1 x2 : R) ↦ x1 * x2) U₂ᴴ U₁ᴴ) Prod.swap Prod.swap) =
    1
Tactic: simp_rw [Unitary.mem_iff, star_eq_conjTranspose, conjTranspose_kronecker']
-- Lean 4 proof step from Mathlib.LinearAlgebra.UnitaryGroup (goal)
Goal:
n : Type u
inst : DecidableEq n
inst_1 : Fintype n
R : Type u_1
m : Type u_2
inst_2 : Semiring R
inst_3 : StarRing R
inst_4 : Fintype m
inst_5 : DecidableEq m
U₁ : Matrix n n R
U₂ : Matrix m m R
hU₁ : Membership.mem (γ := Submonoid (Matrix n n R)) (unitary (Matrix n n R)) U₁
hU₂ : Membership.mem (γ := Submonoid (Matrix m m R)) (unitary (Matrix m m R)) U₂
⊢ HMul.hMul (α := Matrix (n × m) (n × m) R)
        (submatrix (kroneckerMap (fun (x1 x2 : R) ↦ x1 * x2) U₂ᴴ U₁ᴴ) Prod.swap Prod.swap)
        (kroneckerMap (fun (x1 x2 : R) ↦ x1 * x2) U₁ U₂) =
      1 ∧
    HMul.hMul (α := Matrix (n × m) (n × m) R) (kroneckerMap (fun (x1 x2 : R) ↦ x1 * x2) U₁ U₂)
        (submatrix (kroneckerMap (fun (x1 x2 : R) ↦ x1 * x2) U₂ᴴ U₁ᴴ) Prod.swap Prod.swap) =
      1
have left : HMul.hMul (α := Matrix (n × m) (n × m) R)
    (submatrix (kroneckerMap (fun (x1 x2 : R) ↦ x1 * x2) U₂ᴴ U₁ᴴ) Prod.swap Prod.swap)
    (kroneckerMap (fun (x1 x2 : R) ↦ x1 * x2) U₁ U₂) =
  1
Tactic: constructor
-- Lean 4 proof step from Mathlib.LinearAlgebra.UnitaryGroup (goal)
Goal:
n : Type u
inst : DecidableEq n
inst_1 : Fintype n
R : Type u_1
m : Type u_2
inst_2 : Semiring R
inst_3 : StarRing R
inst_4 : Fintype m
inst_5 : DecidableEq m
U₁ : Matrix n n R
U₂ : Matrix m m R
hU₁ : Membership.mem (γ := Submonoid (Matrix n n R)) (unitary (Matrix n n R)) U₁
hU₂ : Membership.mem (γ := Submonoid (Matrix m m R)) (unitary (Matrix m m R)) U₂
left :
  HMul.hMul (α := Matrix (n × m) (n × m) R)
      (submatrix (kroneckerMap (fun (x1 x2 : R) ↦ x1 * x2) U₂ᴴ U₁ᴴ) Prod.swap Prod.swap)
      (kroneckerMap (fun (x1 x2 : R) ↦ x1 * x2) U₁ U₂) =
    1
⊢ HMul.hMul (α := Matrix (n × m) (n × m) R)
        (submatrix (kroneckerMap (fun (x1 x2 : R) ↦ x1 * x2) U₂ᴴ U₁ᴴ) Prod.swap Prod.swap)
        (kroneckerMap (fun (x1 x2 : R) ↦ x1 * x2) U₁ U₂) =
      1 ∧
    HMul.hMul (α := Matrix (n × m) (n × m) R) (kroneckerMap (fun (x1 x2 : R) ↦ x1 * x2) U₁ U₂)
        (submatrix (kroneckerMap (fun (x1 x2 : R) ↦ x1 * x2) U₂ᴴ U₁ᴴ) Prod.swap Prod.swap) =
      1
have right : HMul.hMul (α := Matrix (n × m) (n × m) R) (kroneckerMap (fun (x1 x2 : R) ↦ x1 * x2) U₁ U₂)
    (submatrix (kroneckerMap (fun (x1 x2 : R) ↦ x1 * x2) U₂ᴴ U₁ᴴ) Prod.swap Prod.swap) =
  1
Tactic: constructor
-- Lean 4 proof step from Mathlib.LinearAlgebra.UnitaryGroup (goal)
Goal:
n : Type u
inst : DecidableEq n
inst_1 : Fintype n
R : Type u_1
m : Type u_2
inst_2 : Semiring R
inst_3 : StarRing R
inst_4 : Fintype m
inst_5 : DecidableEq m
U₁ : Matrix n n R
U₂ : Matrix m m R
hU₁ : Membership.mem (γ := Submonoid (Matrix n n R)) (unitary (Matrix n n R)) U₁
hU₂ : Membership.mem (γ := Submonoid (Matrix m m R)) (unitary (Matrix m m R)) U₂
⊢ HMul.hMul (α := Matrix (n × m) (n × m) R)
      (submatrix (kroneckerMap (fun (x1 x2 : R) ↦ x1 * x2) U₂ᴴ U₁ᴴ) Prod.swap Prod.swap)
      (kroneckerMap (fun (x1 x2 : R) ↦ x1 * x2) U₁ U₂) =
    1
have left : ∀ (i j : n × m),
  HMul.hMul (α := Matrix (n × m) (n × m) R) (β := Matrix (n × m) (n × m) R)
      (submatrix (kroneckerMap (fun (x1 x2 : R) ↦ x1 * x2) U₂ᴴ U₁ᴴ) Prod.swap Prod.swap)
      (kroneckerMap (fun (x1 x2 : R) ↦ x1 * x2) U₁ U₂) i j =
    1 i j
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.UnitaryGroup (goal)
Goal:
n : Type u
inst : DecidableEq n
inst_1 : Fintype n
R : Type u_1
m : Type u_2
inst_2 : Semiring R
inst_3 : StarRing R
inst_4 : Fintype m
inst_5 : DecidableEq m
U₁ : Matrix n n R
U₂ : Matrix m m R
hU₁ : Membership.mem (γ := Submonoid (Matrix n n R)) (unitary (Matrix n n R)) U₁
hU₂ : Membership.mem (γ := Submonoid (Matrix m m R)) (unitary (Matrix m m R)) U₂
⊢ HMul.hMul (α := Matrix (n × m) (n × m) R) (kroneckerMap (fun (x1 x2 : R) ↦ x1 * x2) U₁ U₂)
      (submatrix (kroneckerMap (fun (x1 x2 : R) ↦ x1 * x2) U₂ᴴ U₁ᴴ) Prod.swap Prod.swap) =
    1
have right : ∀ (i j : n × m),
  HMul.hMul (α := Matrix (n × m) (n × m) R) (β := Matrix (n × m) (n × m) R)
      (kroneckerMap (fun (x1 x2 : R) ↦ x1 * x2) U₁ U₂)
      (submatrix (kroneckerMap (fun (x1 x2 : R) ↦ x1 * x2) U₂ᴴ U₁ᴴ) Prod.swap Prod.swap) i j =
    1 i j
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.UnitaryGroup (goal)
Goal:
n : Type u
inst : DecidableEq n
inst_1 : Fintype n
R : Type u_1
m : Type u_2
inst_2 : Semiring R
inst_3 : StarRing R
inst_4 : Fintype m
inst_5 : DecidableEq m
U₁ : Matrix n n R
U₂ : Matrix m m R
hU₁ : Membership.mem (γ := Submonoid (Matrix n n R)) (unitary (Matrix n n R)) U₁
hU₂ : Membership.mem (γ := Submonoid (Matrix m m R)) (unitary (Matrix m m R)) U₂
i j : n × m
⊢ HMul.hMul (α := Matrix (n × m) (n × m) R) (β := Matrix (n × m) (n × m) R)
      (submatrix (kroneckerMap (fun (x1 x2 : R) ↦ x1 * x2) U₂ᴴ U₁ᴴ) Prod.swap Prod.swap)
      (kroneckerMap (fun (x1 x2 : R) ↦ x1 * x2) U₁ U₂) i j =
    1 i j
have left : Eq.{u_1 + 1} (α := R) (∑ x : n × m, star U₂ i.2 x.2 * star U₁ i.1 x.1 * U₁ x.1 j.1 * U₂ x.2 j.2) (1 i j)
Tactic: simp only [mul_apply, submatrix_apply, kroneckerMap_apply, Prod.fst_swap,
    conjTranspose_apply, ← star_apply, Prod.snd_swap, ← mul_assoc]