awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Transvection.Basic
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
⊢ (ε : (a : Fin n → S) → V) vM = v

Tactic:
have hv : ε vM = v := by
    rw [of_fintype_basis_eq]
    ext i
    rw [RingHom.algebraMap_toAlgebra]
    simp only [vM, γ, Function.comp_apply]
    apply MvPolynomial.aeval_X
-- Module: Mathlib.LinearAlgebra.Transvection.Basic
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 :
  (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)
⊢ (LinearMap.det : (a : V →ₗ[R] V) → R) (transvection f v) =
    HAdd.hAdd (α := R) (β := R) (1 : R) ((f : (a : V) → R) v : R)

Tactic:
rw [← hf, ← hv, ← IsBaseChange.transvection, det_endHom, det_ofDomain]

Premises used: _private.0.LinearMap.transvection.det_ofDomain, IsBaseChange.transvection, IsBaseChange.det_endHom
-- Module: Mathlib.LinearAlgebra.Transvection.Basic
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)
inr₃ 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)
⊢ (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 [map_add, map_one, add_right_inj, toDual_comp_apply]

Premises used: map_add, IsBaseChange.toDual_comp_apply, map_one, add_right_inj
-- Module: Mathlib.LinearAlgebra.Transvection.Basic
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)
rw : Eq.{u_3 + 1} (α := R) ((LinearMap.det : (a : V →ₗ[R] V) → R) (transvection f v) : R) (1 : R)
⊢ Eq.{u_3 + 1} (α := Rˣ) ((LinearEquiv.det : (a : V ≃ₗ[R] V) → Rˣ) (LinearEquiv.transvection hfv) : Rˣ) (1 : Rˣ)

Tactic:
rw [← Units.val_inj, LinearEquiv.coe_det,
    LinearEquiv.transvection.coe_toLinearMap hfv, Units.val_one]

Premises used: Units.val_inj, LinearEquiv.transvection.coe_toLinearMap, Units.val_one, LinearEquiv.coe_det
-- Module: Mathlib.LinearAlgebra.Transvection.Basic
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)
by_contra! : ∀ (h : Ne.{u_3 + 1} (α := R) ((LinearMap.det : (a : V →ₗ[R] V) → R) (transvection f v) : R) (1 : R)), False
⊢ Eq.{u_3 + 1} (α := R) ((LinearMap.det : (a : V →ₗ[R] V) → R) (transvection f v) : R) (1 : R)

Tactic:
by_contra! h
-- Module: Mathlib.LinearAlgebra.Transvection.Basic
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)
⊢ Free R V

Tactic:
have : Free R V := Free.of_det_ne_one h
-- Module: Mathlib.LinearAlgebra.Transvection.Basic
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
⊢ Module.Finite R V

Tactic:
have : Module.Finite R V := finite_of_det_ne_one h
-- Module: Mathlib.LinearAlgebra.Transvection.Basic
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
apply : Eq.{u_3 + 1} (α := R) ((LinearMap.det : (a : V →ₗ[R] V) → R) (transvection f v) : R) (1 : R)
⊢ False

Tactic:
apply h
-- Module: Mathlib.LinearAlgebra.Transvection.Basic
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
rw₂ rw₃ : Eq.{u_3 + 1} (α := R) 1 1
⊢ Eq.{u_3 + 1} (α := R) ((LinearMap.det : (a : V →ₗ[R] V) → R) (transvection f v) : R) (1 : R)

Tactic:
rw [transvection.det, hfv, add_zero]

Premises used: LinearMap.transvection.det, add_zero
-- Module: Mathlib.LinearAlgebra.UnitaryGroup
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

Tactic:
⟨And.right, fun hA => ⟨?_, hA⟩⟩

Premises used: And.right, And.intro, Iff.intro
-- Module: Mathlib.LinearAlgebra.UnitaryGroup
Goal:
n : Type u
inst : DecidableEq n
inst_1 : Fintype n
α : Type v
inst_2 : CommRing α
inst_3 : StarRing α
A : Matrix n n α
refine : ∀ (hA : A * star A = 1), star A * A = 1
⊢ Membership.mem (γ := Submonoid (Matrix n n α)) (unitaryGroup n α) A ↔ A * star A = 1

Tactic:
refine ⟨And.right, fun hA => ⟨?_, hA⟩⟩
-- Module: Mathlib.LinearAlgebra.UnitaryGroup
Goal:
n : Type u
inst : DecidableEq n
inst_1 : Fintype n
α : Type v
inst_2 : CommRing α
inst_3 : StarRing α
A : Matrix n n α
hA : A * star A = 1
⊢ star A * A = 1

Tactic:
simpa only [mul_eq_one_comm] using hA

Premises used: mul_eq_one_comm
-- Module: Mathlib.LinearAlgebra.UnitaryGroup
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

Tactic:
⟨And.left, fun hA => ⟨hA, ?_⟩⟩

Premises used: And.left, And.intro, Iff.intro
-- Module: Mathlib.LinearAlgebra.UnitaryGroup
Goal:
n : Type u
inst : DecidableEq n
inst_1 : Fintype n
α : Type v
inst_2 : CommRing α
inst_3 : StarRing α
A : Matrix n n α
refine : ∀ (hA : star A * A = 1), A * star A = 1
⊢ Membership.mem (γ := Submonoid (Matrix n n α)) (unitaryGroup n α) A ↔ star A * A = 1

Tactic:
refine ⟨And.left, fun hA => ⟨hA, ?_⟩⟩
-- Module: Mathlib.LinearAlgebra.UnitaryGroup
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
rwa rwa₁ rwa₂ rwa₃ : ∀ (hA : A * star A = 1), A * star A = 1
⊢ A * star A = 1

Tactic:
rwa [mul_eq_one_comm] at hA

Premises used: mul_eq_one_comm
-- Module: Mathlib.LinearAlgebra.UnitaryGroup
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
right : A.det * star A.det = 1
⊢ Membership.mem (γ := Submonoid α) (unitary α) A.det

Tactic:
constructor
-- Module: Mathlib.LinearAlgebra.UnitaryGroup
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
⊢ star A.det * A.det = 1

Tactic:
simpa [star, det_transpose] using congr_arg det hA.1

Premises used: Matrix.det_transpose, congr_arg, And.left, Matrix.det, Star.star
-- Module: Mathlib.LinearAlgebra.UnitaryGroup
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
⊢ A.det * star A.det = 1

Tactic:
simpa [star, det_transpose] using congr_arg det hA.2

Premises used: Matrix.det_transpose, congr_arg, And.right, Matrix.det, Star.star
-- Module: Mathlib.LinearAlgebra.UnitaryGroup
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₂
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
⊢ 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₂)

Tactic:
simp_rw [Unitary.mem_iff, star_eq_conjTranspose, conjTranspose_kronecker']

Premises used: Matrix.star_eq_conjTranspose, Unitary.mem_iff, Matrix.conjTranspose_kronecker'
-- Module: Mathlib.LinearAlgebra.UnitaryGroup
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
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
⊢ 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:
constructor
-- Module: Mathlib.LinearAlgebra.UnitaryGroup
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 :
  ∀ (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
⊢ 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:
ext
-- Module: Mathlib.LinearAlgebra.UnitaryGroup
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₂
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
⊢ 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:
ext
-- Module: Mathlib.LinearAlgebra.UnitaryGroup
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
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)
⊢ 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:
simp only [mul_apply, submatrix_apply, kroneckerMap_apply, Prod.fst_swap,
    conjTranspose_apply, ← star_apply, Prod.snd_swap, ← mul_assoc]

Premises used: Prod.fst_swap, mul_assoc, Matrix.star_apply, Matrix.mul_apply, Matrix.kroneckerMap_apply, Prod.snd_swap, Matrix.conjTranspose_apply, Matrix.submatrix_apply
-- Module: Mathlib.LinearAlgebra.UnitaryGroup
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
right : Eq.{u_1 + 1} (α := R) (∑ x : n × m, U₁ i.1 x.1 * U₂ i.2 x.2 * star U₂ x.2 j.2 * star U₁ x.1 j.1) (1 i j)
⊢ 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:
simp only [mul_apply, submatrix_apply, kroneckerMap_apply, Prod.fst_swap,
    conjTranspose_apply, ← star_apply, Prod.snd_swap, ← mul_assoc]

Premises used: Prod.fst_swap, mul_assoc, Matrix.star_apply, Matrix.mul_apply, Matrix.kroneckerMap_apply, Prod.snd_swap, Matrix.conjTranspose_apply, Matrix.submatrix_apply
-- Module: Mathlib.LinearAlgebra.UnitaryGroup
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
left : Eq.{u_1 + 1} (α := R) (∑ x : n, ∑ x_1 : m, star U₂ i.2 x_1 * (star U₁ i.1 x * U₁ x j.1) * U₂ x_1 j.2) (1 i j)
⊢ 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_rw [mul_assoc _ (star U₁ _ _), ← Finset.univ_product_univ, Finset.sum_product]

Premises used: mul_assoc, Finset.univ_product_univ, Finset.sum_product, Star.star
-- Module: Mathlib.LinearAlgebra.UnitaryGroup
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
left : Eq.{u_1 + 1} (α := R) (∑ y : m, ∑ x : n, star U₂ i.2 y * (star U₁ i.1 x * U₁ x j.1) * U₂ y j.2) (1 i j)
⊢ Eq.{u_1 + 1} (α := R) (∑ x : n, ∑ x_1 : m, star U₂ i.2 x_1 * (star U₁ i.1 x * U₁ x j.1) * U₂ x_1 j.2) (1 i j)

Tactic:
rw [Finset.sum_comm]

Premises used: Finset.sum_comm
-- Module: Mathlib.LinearAlgebra.UnitaryGroup
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
left : Eq.{u_1 + 1} (α := R) (∑ x : m, (∑ i_1 : n, star U₂ i.2 x * (star U₁ i.1 i_1 * U₁ i_1 j.1)) * U₂ x j.2) (1 i j)
left₁ : Eq.{u_1 + 1} (α := R) (∑ x : m, (star U₂ i.2 x * ∑ i_1 : n, star U₁ i.1 i_1 * U₁ i_1 j.1) * U₂ x j.2) (1 i j)
left₂ : Eq.{u_1 + 1} (α := R) (∑ x : m, star U₂ i.2 x * (star U₁ * U₁) i.1 j.1 * U₂ x j.2) (1 i j)
left₃ : Eq.{u_1 + 1} (α := R) (∑ x : m, star U₂ i.2 x * 1 i.1 j.1 * U₂ x j.2) (1 i j)
left₄ :
  Eq.{u_1 + 1} (α := R) (∑ x : m, (star U₂ i.2 x * if i.1 = j.1 then 1 else 0) * U₂ x j.2) (if i = j then 1 else 0)
left₅ : Eq.{u_1 + 1} (α := R) (∑ x : m, (if i.1 = j.1 then star U₂ i.2 x else 0) * U₂ x j.2) (if i = j then 1 else 0)
left₆ :
  Eq.{u_1 + 1} (α := R) (∑ x : m, if i.1 = j.1 then star U₂ i.2 x * U₂ x j.2 else 0 * U₂ x j.2) (if i = j then 1 else 0)
left₇ : Eq.{u_1 + 1} (α := R) (∑ x : m, if i.1 = j.1 then star U₂ i.2 x * U₂ x j.2 else 0) (if i = j then 1 else 0)
left₈ :
  Eq.{u_1 + 1} (α := R) (if i.1 = j.1 then ∑ x : m, star U₂ i.2 x * U₂ x j.2 else ∑ x : m, 0) (if i = j then 1 else 0)
left₉ : (if i.1 = j.1 then (star U₂ * U₂) i.2 j.2 else ∑ x : m, 0) = if i = j then 1 else 0
left₁₀ : Eq.{u_1 + 1} (α := R) (if i.1 = j.1 then 1 i.2 j.2 else ∑ x : m, 0) (if i = j then 1 else 0)
left₁₁ : Eq.{u_1 + 1} (α := R) (if i.1 = j.1 then if i.2 = j.2 then 1 else 0 else ∑ x : m, 0) (if i = j then 1 else 0)
left₁₂ : Eq.{u_1 + 1} (α := R) (if i.1 = j.1 then if i.2 = j.2 then 1 else 0 else 0) (if i = j then 1 else 0)
left₁₃ : Eq.{u_1 + 1} (α := R) (if i.1 = j.1 ∧ i.2 = j.2 then 1 else 0) (if i = j then 1 else 0)
⊢ Eq.{u_1 + 1} (α := R) (∑ y : m, ∑ x : n, star U₂ i.2 y * (star U₁ i.1 x * U₁ x j.1) * U₂ y j.2) (1 i j)

Tactic:
simp_rw [← Finset.sum_mul, ← Finset.mul_sum, ← Matrix.mul_apply, hU₁.1, Matrix.one_apply,
      mul_boole, ite_mul, zero_mul, Finset.sum_ite_irrel, ← Matrix.mul_apply, hU₂.1,
      Matrix.one_apply, Finset.sum_const_zero, ← ite_and, Prod.eq_iff_fst_eq_snd_eq]

Premises used: Finset.mul_sum, Matrix.one_apply, MulZeroClass.zero_mul, Finset.sum_ite_irrel, mul_boole, Matrix.mul_apply, Finset.sum_const_zero, And.left, ite_mul, Prod.eq_iff_fst_eq_snd_eq, ite_and, Finset.sum_mul
-- Module: Mathlib.LinearAlgebra.UnitaryGroup
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
inst_5 : StarRing A
inst_6 : StarRing B
inst_7 : StarRing R
inst_8 : StarModule R A
inst_9 : StarModule R B
U : A
V : B
hU : Membership.mem (γ := Submonoid A) (unitary A) U
hV : Membership.mem (γ := Submonoid B) (unitary B) V
⊢ Membership.mem (γ := Submonoid (A ⊗[R] B)) (unitary (A ⊗[R] B)) (U ⊗ₜ[R] V)

Tactic:
simp [Unitary.mem_iff, hU, hV, Algebra.TensorProduct.one_def]

Premises used: Unitary.mem_iff, Algebra.TensorProduct.one_def
-- Module: Mathlib.LinearAlgebra.UnitaryGroup
Goal:
n : Type u
inst : DecidableEq n
inst_1 : Fintype n
R : Type u_1
A : Type u_2
B : Type u_3
inst_2 : CommSemiring R
inst_3 : Semiring A
inst_4 : Semiring B
inst_5 : Algebra R A
inst_6 : Algebra R B
inst_7 : StarRing A
inst_8 : StarRing B
inst_9 : StarRing R
inst_10 : StarModule R A
inst_11 : StarModule R B
m : Type u_4
inst_12 : Fintype m
inst_13 : DecidableEq m
U : Matrix m m A
V : Matrix n n B
hU : Membership.mem (γ := Submonoid (Matrix m m A)) (unitary (Matrix m m A)) U
hV : Membership.mem (γ := Submonoid (Matrix n n B)) (unitary (Matrix n n B)) V
⊢ Uᴴ * U = 1 ∧ U * Uᴴ = 1

Tactic:
simp_rw [Unitary.mem_iff, star_eq_conjTranspose] at hU hV ⊢

Premises used: Matrix.star_eq_conjTranspose, Unitary.mem_iff