awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)
      (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
have 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)
Tactic: simp only [mul_apply, submatrix_apply, kroneckerMap_apply, Prod.fst_swap,
    conjTranspose_apply, ← star_apply, Prod.snd_swap, ← mul_assoc]
-- 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
⊢ 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)
have 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)
Tactic: simp_rw [mul_assoc _ (star U₁ _ _), ← Finset.univ_product_univ, Finset.sum_product]
-- 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
⊢ 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)
have 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)
Tactic: rw [Finset.sum_comm]
-- 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
⊢ 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)
have 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)
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]
-- 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
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)
⊢ 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)
have 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)
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]
-- 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
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)
⊢ 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)
have 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)
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]
-- 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
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)
⊢ 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)
have 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)
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]
-- 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
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)
⊢ 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)
have 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)
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]
-- 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
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)
⊢ 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)
have 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)
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]
-- 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
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)
⊢ 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)
have 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)
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]
-- 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
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)
⊢ 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)
have 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)
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]
-- 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
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)
⊢ 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)
have 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)
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]
-- 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
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)
⊢ 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)
have 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
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]
-- 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
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
⊢ 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)
have 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)
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]
-- 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
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)
⊢ 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)
have 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)
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]
-- 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
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)
⊢ 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)
have 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)
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]