awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
hU₁ : Uᴴ * U = 1 ∧ U * Uᴴ = 1
⊢ Vᴴ * V = 1 ∧ V * Vᴴ = 1

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

Premises used: Matrix.star_eq_conjTranspose, Unitary.mem_iff
-- 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 : Uᴴ * U = 1 ∧ U * Uᴴ = 1
hV : Vᴴ * V = 1 ∧ V * Vᴴ = 1
⊢ HMul.hMul (α := Matrix (m × n) (m × n) (A ⊗[R] B)) (U ⊗ₖₜ[R] V)ᴴ (U ⊗ₖₜ[R] V) = 1 ∧
    HMul.hMul (α := Matrix (m × n) (m × n) (A ⊗[R] B)) (U ⊗ₖₜ[R] V) (U ⊗ₖₜ[R] V)ᴴ = 1

Tactic:
simp [conjTranspose_kroneckerTMul, ← mul_kroneckerTMul_mul, hU, hV]

Premises used: Matrix.conjTranspose_kroneckerTMul, Matrix.mul_kroneckerTMul_mul
-- Module: Mathlib.LinearAlgebra.UnitaryGroup
Goal:
n : Type u
inst : DecidableEq n
inst_1 : Fintype n
α : Type v
inst_2 : CommRing α
inst_3 : StarRing α
A B : ↥(unitaryGroup n α)
⊢ A = B ↔ ∀ (i j : n), (↑A : Matrix n n α) i j = (↑B : Matrix n n α) i j

Tactic:
Subtype.ext_iff.trans ⟨fun h i j => congr_fun (congr_fun h i) j, Matrix.ext⟩

Premises used: Subtype.ext_iff, Iff.intro, Iff.trans, congr_fun, Matrix.ext
-- Module: Mathlib.LinearAlgebra.UnitaryGroup
Goal:
n : Type u
inst : DecidableEq n
inst_1 : Fintype n
α : Type v
inst_2 : CommRing α
inst_3 : StarRing α
A B : ↥(unitaryGroup n α)
⊢ (∀ (i j : n), (↑A : Matrix n n α) i j = (↑B : Matrix n n α) i j) → A = B

Tactic:
(UnitaryGroup.ext_iff A B).mpr

Premises used: Iff.mpr, Matrix.UnitaryGroup.ext_iff
-- Module: Mathlib.LinearAlgebra.UnitaryGroup
Goal:
n : Type u
inst : DecidableEq n
inst_1 : Fintype n
α : Type v
inst_2 : CommRing α
inst_3 : StarRing α
A : ↥(unitaryGroup n α)
⊢ star (↑A : Matrix n n α) * (↑A : Matrix n n α) = 1

Tactic:
A.2.1

Premises used: And.left, Subtype.property
-- Module: Mathlib.LinearAlgebra.UnitaryGroup
Goal:
n : Type u
inst : DecidableEq n
inst_1 : Fintype n
α : Type v
inst_2 : CommRing α
inst_3 : StarRing α
A : ↥(unitaryGroup n α)
⊢ IsUnit (↑A : Matrix n n α).det

Tactic:
isUnit_iff_isUnit_det _ |>.mp <| (Unitary.toUnits A).isUnit

Premises used: Unitary.toUnits, Matrix.isUnit_iff_isUnit_det, Iff.mp, Units.isUnit, DFunLike.coe
-- Module: Mathlib.LinearAlgebra.UnitaryGroup
Goal:
n : Type u
inst : DecidableEq n
inst_1 : Fintype n
α : Type v
inst_2 : CommRing α
inst_3 : StarRing α
A : ↥(unitaryGroup n α)
⊢ (↑A⁻¹ : Matrix n n α) = star (↑A : Matrix n n α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.UnitaryGroup
Goal:
n : Type u
inst : DecidableEq n
inst_1 : Fintype n
α : Type v
inst_2 : CommRing α
inst_3 : StarRing α
A B : ↥(unitaryGroup n α)
⊢ (↑(A * B) : Matrix n n α) = (↑A : Matrix n n α) * (↑B : Matrix n n α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.UnitaryGroup
Goal:
n : Type u
inst : DecidableEq n
inst_1 : Fintype n
α : Type v
inst_2 : CommRing α
inst_3 : StarRing α
⊢ Eq (α := Matrix n n α) (↑1 : Matrix n n α) 1

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.UnitaryGroup
Goal:
n : Type u
inst : DecidableEq n
inst_1 : Fintype n
α : Type v
inst_2 : CommRing α
inst_3 : StarRing α
A B : ↥(unitaryGroup n α)
⊢ toLin' (A * B) = toLin' A ∘ₗ toLin' B

Tactic:
Matrix.toLin'_mul A.1 B.1

Premises used: Matrix.toLin'_mul, Matrix.UnitaryGroup.toLin', Subtype.val
-- Module: Mathlib.LinearAlgebra.UnitaryGroup
Goal:
n : Type u
inst : DecidableEq n
inst_1 : Fintype n
α : Type v
inst_2 : CommRing α
inst_3 : StarRing α
⊢ Eq (α := (n → α) →ₗ[α] n → α) (toLin' 1) LinearMap.id

Tactic:
Matrix.toLin'_one

Premises used: Matrix.toLin'_one, Matrix.UnitaryGroup.toLin'
-- Module: Mathlib.LinearAlgebra.UnitaryGroup
Goal:
n : Type u
inst : DecidableEq n
inst_1 : Fintype n
α : Type v
inst_2 : CommRing α
inst_3 : StarRing α
A_1 : Matrix n n α
A : ↥(unitaryGroup n α)
x : n → α
rw rw₁ :
  Eq (α := n → α) ((toLin' (A⁻¹ * A) : (a : n → α) → n → α) x : n → α)
    ((toLin' (A⁻¹ * A) : (a : n → α) → n → α) x : n → α)
⊢ Eq (α := n → α) ((toLin' A⁻¹ ∘ₗ toLin' A : (a : n → α) → n → α) x : n → α)
    ((toLin' (A⁻¹ * A) : (a : n → α) → n → α) x : n → α)

Tactic:
rw [← toLin'_mul]

Premises used: Matrix.UnitaryGroup.toLin'_mul
-- Module: Mathlib.LinearAlgebra.UnitaryGroup
Goal:
n : Type u
inst : DecidableEq n
inst_1 : Fintype n
α : Type v
inst_2 : CommRing α
inst_3 : StarRing α
A_1 : Matrix n n α
A : ↥(unitaryGroup n α)
x : n → α
rw : (toLin' 1 : (a : n → α) → n → α) x = x
rw₁ : (LinearMap.id : (a : n → α) → n → α) x = x
rw₂ rw₃ : x = x
⊢ (toLin' (A⁻¹ * A) : (a : n → α) → n → α) x = x

Tactic:
rw [inv_mul_cancel, toLin'_one, id_apply]

Premises used: Matrix.UnitaryGroup.toLin'_one, inv_mul_cancel, LinearMap.id_apply
-- Module: Mathlib.LinearAlgebra.UnitaryGroup
Goal:
n : Type u
inst : DecidableEq n
inst_1 : Fintype n
α : Type v
inst_2 : CommRing α
inst_3 : StarRing α
A_1 : Matrix n n α
A : ↥(unitaryGroup n α)
x : n → α
rw rw₁ :
  Eq (α := n → α) ((toLin' (A * A⁻¹) : (a : n → α) → n → α) x : n → α)
    ((toLin' (A * A⁻¹) : (a : n → α) → n → α) x : n → α)
⊢ Eq (α := n → α) ((toLin' A ∘ₗ toLin' A⁻¹ : (a : n → α) → n → α) x : n → α)
    ((toLin' (A * A⁻¹) : (a : n → α) → n → α) x : n → α)

Tactic:
rw [← toLin'_mul]

Premises used: Matrix.UnitaryGroup.toLin'_mul
-- Module: Mathlib.LinearAlgebra.UnitaryGroup
Goal:
n : Type u
inst : DecidableEq n
inst_1 : Fintype n
α : Type v
inst_2 : CommRing α
inst_3 : StarRing α
A_1 : Matrix n n α
A : ↥(unitaryGroup n α)
x : n → α
rw : (toLin' 1 : (a : n → α) → n → α) x = x
rw₁ : (LinearMap.id : (a : n → α) → n → α) x = x
rw₂ rw₃ : x = x
⊢ (toLin' (A * A⁻¹) : (a : n → α) → n → α) x = x

Tactic:
rw [mul_inv_cancel, toLin'_one, id_apply]

Premises used: Matrix.UnitaryGroup.toLin'_one, LinearMap.id_apply, mul_inv_cancel
-- Module: Mathlib.LinearAlgebra.UnitaryGroup
Goal:
n : Type u
inst : DecidableEq n
inst_1 : Fintype n
α : Type v
inst_2 : CommRing α
inst_3 : StarRing α
A : ↥(unitaryGroup n α)
⊢ (↑(toGL A) : (n → α) →ₗ[α] n → α) = toLin' A

Tactic:
rfl

Premises used: Matrix.UnitaryGroup.toLin', rfl
-- Module: Mathlib.LinearAlgebra.UnitaryGroup
Goal:
n : Type u
inst : DecidableEq n
inst_1 : Fintype n
α : Type v
inst_2 : CommRing α
inst_3 : StarRing α
simp : Eq (α := (n → α) →ₗ[α] n → α) LinearMap.id (↑1 : (n → α) →ₗ[α] n → α)
⊢ Eq (α := (n → α) →ₗ[α] n → α) (↑(toGL 1) : (n → α) →ₗ[α] n → α) (↑1 : (n → α) →ₗ[α] n → α)

Tactic:
simp only [coe_toGL, toLin'_one]

Premises used: Matrix.UnitaryGroup.toLin'_one, Matrix.UnitaryGroup.coe_toGL
-- Module: Mathlib.LinearAlgebra.UnitaryGroup
Goal:
n : Type u
inst : DecidableEq n
inst_1 : Fintype n
α : Type v
inst_2 : CommRing α
inst_3 : StarRing α
⊢ Eq (α := (n → α) →ₗ[α] n → α) LinearMap.id (↑1 : (n → α) →ₗ[α] n → α)

Tactic:
rfl
-- Module: Mathlib.LinearAlgebra.UnitaryGroup
Goal:
n : Type u
inst : DecidableEq n
inst_1 : Fintype n
α : Type v
inst_2 : CommRing α
inst_3 : StarRing α
A B : ↥(unitaryGroup n α)
simp : toLin' A ∘ₗ toLin' B = (↑(toGL A * toGL B) : (n → α) →ₗ[α] n → α)
⊢ (↑(toGL (A * B)) : (n → α) →ₗ[α] n → α) = (↑(toGL A * toGL B) : (n → α) →ₗ[α] n → α)

Tactic:
simp only [coe_toGL, toLin'_mul]

Premises used: Matrix.UnitaryGroup.coe_toGL, Matrix.UnitaryGroup.toLin'_mul
-- Module: Mathlib.LinearAlgebra.UnitaryGroup
Goal:
n : Type u
inst : DecidableEq n
inst_1 : Fintype n
α : Type v
inst_2 : CommRing α
inst_3 : StarRing α
A B : ↥(unitaryGroup n α)
⊢ toLin' A ∘ₗ toLin' B = (↑(toGL A * toGL B) : (n → α) →ₗ[α] n → α)

Tactic:
rfl
-- Module: Mathlib.LinearAlgebra.UnitaryGroup
Goal:
n : Type u
inst : DecidableEq n
inst_1 : Fintype n
α : Type v
inst_2 : CommRing α
inst_3 : StarRing α
U : Matrix n n α
rw : star U * U = 1
| Membership.mem (γ := Submonoid (Matrix n n α)) (unitaryGroup n α) U

Tactic:
rw [mem_unitaryGroup_iff']

Premises used: Matrix.mem_unitaryGroup_iff'
-- Module: Mathlib.LinearAlgebra.UnitaryGroup
Goal:
n : Type u
inst : DecidableEq n
inst_1 : Fintype n
α : Type v
inst_2 : CommRing α
inst_3 : StarRing α
U : Matrix n n α
conv_rhs : Membership.mem (γ := Submonoid (Matrix n n α)) (unitaryGroup n α) Uᵀ ↔ star U * U = 1
⊢ Membership.mem (γ := Submonoid (Matrix n n α)) (unitaryGroup n α) Uᵀ ↔
    Membership.mem (γ := Submonoid (Matrix n n α)) (unitaryGroup n α) U

Tactic:
conv_rhs => rw [mem_unitaryGroup_iff']

Premises used: Matrix.mem_unitaryGroup_iff'
-- Module: Mathlib.LinearAlgebra.UnitaryGroup
Goal:
n : Type u
inst : DecidableEq n
inst_1 : Fintype n
α : Type v
inst_2 : CommRing α
inst_3 : StarRing α
U : Matrix n n α
⊢ star Uᵀ = (star U)ᵀ

Tactic:
rfl
-- Module: Mathlib.LinearAlgebra.UnitaryGroup
Goal:
n : Type u
inst : DecidableEq n
inst_1 : Fintype n
α : Type v
inst_2 : CommRing α
inst_3 : StarRing α
U : Matrix n n α
rw : (star U * U)ᵀᵀ = 1ᵀ ↔ star U * U = 1
⊢ Membership.mem (γ := Submonoid (Matrix n n α)) (unitaryGroup n α) Uᵀ ↔ star U * U = 1

Tactic:
rw [mem_unitaryGroup_iff, show star Uᵀ = (star U)ᵀ by rfl, ← transpose_mul, ← transpose_inj]

Premises used: Matrix.mem_unitaryGroup_iff, Matrix.transpose_mul, Matrix.transpose_inj
-- Module: Mathlib.LinearAlgebra.UnitaryGroup
Goal:
n : Type u
inst : DecidableEq n
inst_1 : Fintype n
α : Type v
inst_2 : CommRing α
inst_3 : StarRing α
U : Matrix n n α
⊢ (star U * U)ᵀᵀ = 1ᵀ ↔ star U * U = 1

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.UnitaryGroup
Goal:
n : Type u
inst : DecidableEq n
inst_1 : Fintype n
α : Type v
inst_2 : CommRing α
inst_3 : StarRing α
U : Matrix n n α
⊢ Membership.mem (γ := Submonoid (Matrix n n α)) (unitaryGroup n α) (U.map star) ↔
    Membership.mem (γ := Submonoid (Matrix n n α)) (unitaryGroup n α) U

Tactic:
simp [← conjTranspose_transpose, transpose_mem_unitaryGroup_iff, ← star_eq_conjTranspose]

Premises used: Matrix.star_eq_conjTranspose, Matrix.transpose_mem_unitaryGroup_iff, Matrix.conjTranspose_transpose
-- Module: Mathlib.LinearAlgebra.UnitaryGroup
Goal:
n : Type u
inst : DecidableEq n
inst_1 : Fintype n
α : Type v
inst_2 : CommRing α
inst_3 : StarRing α
U : ↥(unitaryGroup n α)
a : ∀ (i j : n), (↑(map_star U)⁻¹ : Matrix n n α) i j = (↑(transpose U) : Matrix n n α) i j
⊢ (map_star U)⁻¹ = transpose U

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.UnitaryGroup
Goal:
n : Type u
inst : DecidableEq n
inst_1 : Fintype n
α : Type v
inst_2 : CommRing α
inst_3 : StarRing α
U : ↥(unitaryGroup n α)
i j : n
⊢ (↑(map_star U)⁻¹ : Matrix n n α) i j = (↑(transpose U) : Matrix n n α) i j

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.UnitaryGroup
Goal:
n : Type u
inst : DecidableEq n
inst_1 : Fintype n
α : Type v
inst_2 : CommRing α
inst_3 : StarRing α
U : ↥(unitaryGroup n α)
⊢ (transpose U)⁻¹ = map_star U

Tactic:
simp [← map_star_inv_eq_transpose]

Premises used: Matrix.UnitaryGroup.map_star_inv_eq_transpose
-- Module: Mathlib.LinearAlgebra.UnitaryGroup
Goal:
n : Type u
inst : DecidableEq n
inst_1 : Fintype n
α : Type v
inst_2 : CommRing α
inst_3 : StarRing α
⊢ LE.le (α := Submonoid (Matrix n n α)) (specialUnitaryGroup n α) (unitaryGroup n α)

Tactic:
inf_le_left

Premises used: Set.Mem, inf_le_left
-- 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 α)) (specialUnitaryGroup n α) A ↔
    Membership.mem (γ := Submonoid (Matrix n n α)) (unitaryGroup n α) A ∧ A.det = 1

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.inter, Set.preimage, Set.singleton, Matrix.det
-- Module: Mathlib.LinearAlgebra.UnitaryGroup
Goal:
n : Type u
inst : DecidableEq n
inst_1 : Fintype n
α : Type v
inst_2 : CommRing α
inst_3 : StarRing α
A_1 : Matrix n n α
A : ↥(specialUnitaryGroup n α)
⊢ star (↑A : Matrix n n α) ∈ (↑(unitaryGroup n α) : Set (Matrix n n α))

Tactic:
simpa using A.prop.1

Premises used: And.left, Subtype.prop
-- Module: Mathlib.LinearAlgebra.UnitaryGroup
Goal:
n : Type u
inst : DecidableEq n
inst_1 : Fintype n
α : Type v
inst_2 : CommRing α
inst_3 : StarRing α
A_1 : Matrix n n α
A : ↥(specialUnitaryGroup n α)
⊢ (↑A : Matrix n n α) ∈ (↑(MonoidHom.mker (F := Matrix n n α →* α) detMonoidHom) : Set (Matrix n n α))

Tactic:
have := A.prop.2
-- Module: Mathlib.LinearAlgebra.UnitaryGroup
Goal:
n : Type u
inst : DecidableEq n
inst_1 : Fintype n
α : Type v
inst_2 : CommRing α
inst_3 : StarRing α
A_1 : Matrix n n α
A : ↥(specialUnitaryGroup n α)
this : (↑A : Matrix n n α) ∈ (↑(MonoidHom.mker (F := Matrix n n α →* α) detMonoidHom) : Set (Matrix n n α))
⊢ star (↑A : Matrix n n α) ∈ (↑(MonoidHom.mker (F := Matrix n n α →* α) detMonoidHom) : Set (Matrix n n α))

Tactic:
simp_all [star_eq_conjTranspose]

Premises used: Matrix.star_eq_conjTranspose
-- Module: Mathlib.LinearAlgebra.UnitaryGroup
Goal:
n : Type u
inst : DecidableEq n
inst_1 : Fintype n
α : Type v
inst_2 : CommRing α
inst_3 : StarRing α
A : ↥(specialUnitaryGroup n α)
⊢ (↑(star A) : Matrix n n α) = star (↑A : Matrix n n α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.UnitaryGroup
Goal:
n : Type u
inst : DecidableEq n
inst_1 : Fintype n
α : Type v
inst_2 : CommRing α
inst_3 : StarRing α
A : ↥(specialUnitaryGroup n α)
⊢ star A = A⁻¹

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.UnitaryGroup
Goal:
n : Type u
inst : DecidableEq n
inst_1 : Fintype n
R : Type v
inst_2 : CommRing R
A : Matrix n n R
⊢ Membership.mem (γ := Submonoid (Matrix n n R)) (orthogonalGroup n R) A ↔ A * Aᵀ = 1

Tactic:
mem_unitaryGroup_iff

Premises used: Set.Mem, Matrix.mem_unitaryGroup_iff, Matrix.transpose, Matrix.map, Matrix.conjTranspose
-- Module: Mathlib.LinearAlgebra.UnitaryGroup
Goal:
n : Type u
inst : DecidableEq n
inst_1 : Fintype n
R : Type v
inst_2 : CommRing R
A : Matrix n n R
⊢ Membership.mem (γ := Submonoid (Matrix n n R)) (orthogonalGroup n R) A ↔ Aᵀ * A = 1

Tactic:
mem_unitaryGroup_iff'

Premises used: Set.Mem, Matrix.transpose, Matrix.map, Matrix.mem_unitaryGroup_iff', Matrix.conjTranspose
-- Module: Mathlib.LinearAlgebra.UnitaryGroup
Goal:
n : Type u
inst : DecidableEq n
inst_1 : Fintype n
R : Type v
inst_2 : CommRing R
A : Matrix n n R
⊢ Membership.mem (γ := Submonoid (Matrix n n R)) (specialOrthogonalGroup n R) A ↔
    Membership.mem (γ := Submonoid (Matrix n n R)) (orthogonalGroup n R) A ∧ A.det = 1

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.inter, Set.preimage, Set.singleton, Matrix.det
-- Module: Mathlib.LinearAlgebra.UnitaryGroup
Goal:
R : Type v
inst : CommRing R
a b c d : R
trans :
  Membership.mem (α := Matrix (Fin 2) (Fin 2) R) (γ := Submonoid (Matrix (Fin 2) (Fin 2) R))
      (specialOrthogonalGroup (Fin 2) R) (!![a, b; c, d] : Matrix (Fin 2) (Fin 2) R) ↔
    ((a * a + b * b = 1 ∧ a * c + b * d = 0) ∧ c * a + d * b = 0 ∧ c * c + d * d = 1) ∧ a * d - b * c = 1
trans₁ :
  ((a * a + b * b = 1 ∧ a * c + b * d = 0) ∧ c * a + d * b = 0 ∧ c * c + d * d = 1) ∧ a * d - b * c = 1 ↔
    a = d ∧ b = -c ∧ HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 = 1
⊢ Membership.mem (α := Matrix (Fin 2) (Fin 2) R) (γ := Submonoid (Matrix (Fin 2) (Fin 2) R))
      (specialOrthogonalGroup (Fin 2) R) (!![a, b; c, d] : Matrix (Fin 2) (Fin 2) R) ↔
    a = d ∧ b = -c ∧ HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 = 1

Tactic:
trans ((a * a + b * b = 1 ∧ a * c + b * d = 0) ∧
    c * a + d * b = 0 ∧ c * c + d * d = 1) ∧ a * d - b * c = 1

Premises used: HMul.hMul, And, HAdd.hAdd, OfNat.ofNat, Eq
-- Module: Mathlib.LinearAlgebra.UnitaryGroup
Goal:
R : Type v
inst : CommRing R
a b c d : R
⊢ Membership.mem (α := Matrix (Fin 2) (Fin 2) R) (γ := Submonoid (Matrix (Fin 2) (Fin 2) R))
      (specialOrthogonalGroup (Fin 2) R) (!![a, b; c, d] : Matrix (Fin 2) (Fin 2) R) ↔
    ((a * a + b * b = 1 ∧ a * c + b * d = 0) ∧ c * a + d * b = 0 ∧ c * c + d * d = 1) ∧ a * d - b * c = 1

Tactic:
simp [Matrix.mem_specialOrthogonalGroup_iff, Matrix.mem_orthogonalGroup_iff,
      ← Matrix.ext_iff, Fin.forall_fin_succ, Matrix.vecHead, Matrix.vecTail]

Premises used: Matrix.mem_specialOrthogonalGroup_iff, Fin.forall_fin_succ, Matrix.vecHead, Matrix.mem_orthogonalGroup_iff, Matrix.ext_iff, Matrix.vecTail
-- Module: Mathlib.LinearAlgebra.UnitaryGroup
Goal:
R : Type v
inst : CommRing R
a b c d : R
⊢ ((a * a + b * b = 1 ∧ a * c + b * d = 0) ∧ c * a + d * b = 0 ∧ c * c + d * d = 1) ∧ a * d - b * c = 1 ↔
    a = d ∧ b = -c ∧ HPow.hPow (β := ℕ) a 2 + HPow.hPow (β := ℕ) b 2 = 1

Tactic:
grind
-- Module: Mathlib.LinearAlgebra.UnitaryGroup
Goal:
R : Type v
inst : CommRing R
M : Matrix (Fin 2) (Fin 2) R
rw :
  Membership.mem (γ := Submonoid (Matrix (Fin 2) (Fin 2) R)) (specialOrthogonalGroup (Fin 2) R) M.etaExpand ↔
    M.etaExpand 0 0 = M.etaExpand 1 1 ∧
      M.etaExpand 0 1 = -M.etaExpand 1 0 ∧
        HPow.hPow (β := ℕ) (M.etaExpand 0 0) 2 + HPow.hPow (β := ℕ) (M.etaExpand 0 1) 2 = 1
⊢ Membership.mem (γ := Submonoid (Matrix (Fin 2) (Fin 2) R)) (specialOrthogonalGroup (Fin 2) R) M ↔
    M 0 0 = M 1 1 ∧ M 0 1 = -M 1 0 ∧ HPow.hPow (β := ℕ) (M 0 0) 2 + HPow.hPow (β := ℕ) (M 0 1) 2 = 1

Tactic:
rw [← M.etaExpand_eq]

Premises used: Matrix.etaExpand_eq
-- Module: Mathlib.LinearAlgebra.UnitaryGroup
Goal:
R : Type v
inst : CommRing R
M : Matrix (Fin 2) (Fin 2) R
⊢ Membership.mem (γ := Submonoid (Matrix (Fin 2) (Fin 2) R)) (specialOrthogonalGroup (Fin 2) R) M.etaExpand ↔
    M.etaExpand 0 0 = M.etaExpand 1 1 ∧
      M.etaExpand 0 1 = -M.etaExpand 1 0 ∧
        HPow.hPow (β := ℕ) (M.etaExpand 0 0) 2 + HPow.hPow (β := ℕ) (M.etaExpand 0 1) 2 = 1

Tactic:
of_mem_specialOrthogonalGroup_fin_two_iff

Premises used: Eq.mpr, FinVec.etaExpand, FinVec.map, Set.Mem, Matrix.etaExpand, Fin.cons, Fin.induction.go, Fin.induction, Matrix.of_mem_specialOrthogonalGroup_fin_two_iff, Fin.cases, FinVec.seq, Matrix.vecTail, Matrix.vecCons
-- Module: Mathlib.LinearAlgebra.UnitaryGroup
Goal:
R : Type v
inst : CommRing R
M : Matrix (Fin 2) (Fin 2) R
⊢ Membership.mem (γ := Submonoid (Matrix (Fin 2) (Fin 2) R)) (specialOrthogonalGroup (Fin 2) R) M.etaExpand ↔
    M.etaExpand 0 0 = M.etaExpand 1 1 ∧
      M.etaExpand 0 1 = -M.etaExpand 1 0 ∧
        HPow.hPow (β := ℕ) (M.etaExpand 0 0) 2 + HPow.hPow (β := ℕ) (M.etaExpand 0 1) 2 = 1

Tactic:
exact of_mem_specialOrthogonalGroup_fin_two_iff

Premises used: Matrix.of_mem_specialOrthogonalGroup_fin_two_iff
-- Module: Mathlib.LinearAlgebra.Vandermonde
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
v : Fin n → R
⊢ vandermonde v = projVandermonde v 1

Tactic:
simp [projVandermonde, rectVandermonde, vandermonde]

Premises used: Matrix.projVandermonde, Matrix.vandermonde, Matrix.rectVandermonde
-- Module: Mathlib.LinearAlgebra.Vandermonde
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
v w : Fin n → R
i j : Fin n
⊢ projVandermonde v w i j = v i ^ (↑j : ℕ) * w i ^ (↑j.rev : ℕ)

Tactic:
rfl

Premises used: Matrix.projVandermonde, rfl, Matrix.rectVandermonde
-- Module: Mathlib.LinearAlgebra.Vandermonde
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
α : Type u_3
v w : α → R
i : α
j : Fin n
⊢ rectVandermonde v w n i j = v i ^ (↑j : ℕ) * w i ^ (↑j.rev : ℕ)

Tactic:
rfl

Premises used: rfl, Matrix.rectVandermonde
-- Module: Mathlib.LinearAlgebra.Vandermonde
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
v : Fin n → R
i j : Fin n
⊢ vandermonde v i j = v i ^ (↑j : ℕ)

Tactic:
rfl

Premises used: Matrix.vandermonde, rfl
-- Module: Mathlib.LinearAlgebra.Vandermonde
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
v0 : R
v : Fin n → R
a :
  ∀ (i j : Fin (n + 1)),
    Eq.{u_1 + 1} (α := R) (vandermonde (Fin.cons (α := fun (a : Fin n.succ) ↦ R) v0 v) i j : R)
      (Fin.cons (α := fun (i : Fin (n + 1)) ↦ Fin (n + 1) → R) (fun (j : Fin n.succ) ↦ v0 ^ (↑j : ℕ))
          (fun (i : Fin n) ↦ Fin.cons (α := fun (i : Fin (n + 1)) ↦ R) 1 fun (j : Fin n) ↦ v i * vandermonde v i j) i
          j :
        R)
⊢ Eq.{u_1 + 1} (α := Matrix (Fin (n + 1)) (Fin (n + 1)) R) (vandermonde (Fin.cons (α := fun (a : Fin n.succ) ↦ R) v0 v))
    (Fin.cons (α := fun (i : Fin (n + 1)) ↦ Fin (n + 1) → R) (fun (j : Fin n.succ) ↦ v0 ^ (↑j : ℕ)) fun (i : Fin n) ↦
      Fin.cons (α := fun (i : Fin (n + 1)) ↦ R) 1 fun (j : Fin n) ↦ v i * vandermonde v i j)

Tactic:
ext i j
-- Module: Mathlib.LinearAlgebra.Vandermonde
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
v0 : R
v : Fin n → R
i j : Fin (n + 1)
⊢ Eq.{u_1 + 1} (α := R) (vandermonde (Fin.cons (α := fun (a : Fin n.succ) ↦ R) v0 v) 0 j : R)
    (Fin.cons (α := fun (i : Fin (n + 1)) ↦ Fin (n + 1) → R) (fun (j : Fin n.succ) ↦ v0 ^ (↑j : ℕ))
        (fun (i : Fin n) ↦ Fin.cons (α := fun (i : Fin (n + 1)) ↦ R) 1 fun (j : Fin n) ↦ v i * vandermonde v i j) 0 j :
      R)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Vandermonde
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
v0 : R
v : Fin n → R
i j : Fin (n + 1)
a :
  ∀ (i : Fin n),
    Eq.{u_1 + 1} (α := R) (vandermonde (Fin.cons (α := fun (a : Fin n.succ) ↦ R) v0 v) i.succ j : R)
      (Fin.cons (α := fun (i : Fin (n + 1)) ↦ Fin (n + 1) → R) (fun (j : Fin n.succ) ↦ v0 ^ (↑j : ℕ))
          (fun (i : Fin n) ↦ Fin.cons (α := fun (i : Fin (n + 1)) ↦ R) 1 fun (j : Fin n) ↦ v i * vandermonde v i j)
          i.succ j :
        R)
⊢ Eq.{u_1 + 1} (α := R) (vandermonde (Fin.cons (α := fun (a : Fin n.succ) ↦ R) v0 v) i j : R)
    (Fin.cons (α := fun (i : Fin (n + 1)) ↦ Fin (n + 1) → R) (fun (j : Fin n.succ) ↦ v0 ^ (↑j : ℕ))
        (fun (i : Fin n) ↦ Fin.cons (α := fun (i : Fin (n + 1)) ↦ R) 1 fun (j : Fin n) ↦ v i * vandermonde v i j) i j :
      R)

Tactic:
refine Fin.cases (by simp) (fun i => ?_) i
-- Module: Mathlib.LinearAlgebra.Vandermonde
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
v0 : R
v : Fin n → R
i_1 j : Fin (n + 1)
i : Fin n
⊢ Eq.{u_1 + 1} (α := R) (vandermonde (Fin.cons (α := fun (a : Fin n.succ) ↦ R) v0 v) i.succ 0 : R)
    (Fin.cons (α := fun (i : Fin (n + 1)) ↦ Fin (n + 1) → R) (fun (j : Fin n.succ) ↦ v0 ^ (↑j : ℕ))
        (fun (i : Fin n) ↦ Fin.cons (α := fun (i : Fin (n + 1)) ↦ R) 1 fun (j : Fin n) ↦ v i * vandermonde v i j) i.succ
        0 :
      R)

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Vandermonde
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
v0 : R
v : Fin n → R
i_1 j : Fin (n + 1)
i : Fin n
a :
  ∀ (j : Fin n),
    Eq.{u_1 + 1} (α := R) (vandermonde (Fin.cons (α := fun (a : Fin n.succ) ↦ R) v0 v) i.succ j.succ : R)
      (Fin.cons (α := fun (i : Fin (n + 1)) ↦ Fin (n + 1) → R) (fun (j : Fin n.succ) ↦ v0 ^ (↑j : ℕ))
          (fun (i : Fin n) ↦ Fin.cons (α := fun (i : Fin (n + 1)) ↦ R) 1 fun (j : Fin n) ↦ v i * vandermonde v i j)
          i.succ j.succ :
        R)
⊢ Eq.{u_1 + 1} (α := R) (vandermonde (Fin.cons (α := fun (a : Fin n.succ) ↦ R) v0 v) i.succ j : R)
    (Fin.cons (α := fun (i : Fin (n + 1)) ↦ Fin (n + 1) → R) (fun (j : Fin n.succ) ↦ v0 ^ (↑j : ℕ))
        (fun (i : Fin n) ↦ Fin.cons (α := fun (i : Fin (n + 1)) ↦ R) 1 fun (j : Fin n) ↦ v i * vandermonde v i j) i.succ
        j :
      R)

Tactic:
refine Fin.cases (by simp) (fun j => ?_) j
-- Module: Mathlib.LinearAlgebra.Vandermonde
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
v0 : R
v : Fin n → R
i_1 j_1 : Fin (n + 1)
i j : Fin n
⊢ Eq.{u_1 + 1} (α := R) (vandermonde (Fin.cons (α := fun (a : Fin n.succ) ↦ R) v0 v) i.succ j.succ : R)
    (Fin.cons (α := fun (i : Fin (n + 1)) ↦ Fin (n + 1) → R) (fun (j : Fin n.succ) ↦ v0 ^ (↑j : ℕ))
        (fun (i : Fin n) ↦ Fin.cons (α := fun (i : Fin (n + 1)) ↦ R) 1 fun (j : Fin n) ↦ v i * vandermonde v i j) i.succ
        j.succ :
      R)

Tactic:
simp [pow_succ']

Premises used: pow_succ'