awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Star.Unitary
Goal:
R : Type u_1
inst : Monoid R
inst_1 : StarMul R
U B : R
h : Membership.mem (γ := Set R) {U : R | star U * U = 1 ∧ U * star U = 1} U
h_1 : Membership.mem (γ := Set R) {U : R | star U * U = 1 ∧ U * star U = 1} B
hA₁ : star U * U = 1
hA₂ : U * star U = 1
hB₁ : star B * B = 1
hB₂ : B * star B = 1
rw rw₁ : star B * star U * U * B = star B * star U * U * B
⊢ star B * star U * U * B = star B * (star U * U) * B

Tactic:
rw [← mul_assoc]

Premises used: mul_assoc
-- Module: Mathlib.Algebra.Star.Unitary
Goal:
R : Type u_1
inst : Monoid R
inst_1 : StarMul R
U B : R
h : Membership.mem (γ := Set R) {U : R | star U * U = 1 ∧ U * star U = 1} U
h_1 : Membership.mem (γ := Set R) {U : R | star U * U = 1 ∧ U * star U = 1} B
hA₁ : star U * U = 1
hA₂ : U * star U = 1
hB₁ : star B * B = 1
hB₂ : B * star B = 1
rw : star B * 1 * B = 1
rw₁ : star B * B = 1
rw₂ rw₃ : Eq.{u_1 + 1} (α := R) 1 1
⊢ star B * (star U * U) * B = 1

Tactic:
rw [hA₁, mul_one, hB₁]

Premises used: mul_one
-- Module: Mathlib.Algebra.Star.Unitary
Goal:
R : Type u_1
inst : Monoid R
inst_1 : StarMul R
U B : R
h : Membership.mem (γ := Set R) {U : R | Star.star U * U = 1 ∧ U * Star.star U = 1} U
h_1 : Membership.mem (γ := Set R) {U : R | Star.star U * U = 1 ∧ U * Star.star U = 1} B
hA₁ : Star.star U * U = 1
hA₂ : U * Star.star U = 1
hB₁ : Star.star B * B = 1
hB₂ : B * Star.star B = 1
star : Star.star (U * B) * (U * B) = Star.star B * Star.star U * U * B
star₁ : Star.star B * Star.star U * U * B = Star.star B * (Star.star U * U) * B
star₂ : Star.star B * (Star.star U * U) * B = 1
⊢ Star.star (U * B) * (U * B) = 1

Tactic:
calc
        star (U * B) * (U * B) = star B * star U * U * B := by simp only [mul_assoc, star_mul]
        _ = star B * (star U * U) * B := by rw [← mul_assoc]
        _ = 1 := by rw [hA₁, mul_one, hB₁]

Premises used: HMul.hMul, Star.star
-- Module: Mathlib.Algebra.Star.Unitary
Goal:
R : Type u_1
inst : Monoid R
inst_1 : StarMul R
U B : R
h : Membership.mem (γ := Set R) {U : R | star U * U = 1 ∧ U * star U = 1} U
h_1 : Membership.mem (γ := Set R) {U : R | star U * U = 1 ∧ U * star U = 1} B
hA₁ : star U * U = 1
hA₂ : U * star U = 1
hB₁ : star B * B = 1
hB₂ : B * star B = 1
rw rw₁ : U * B * (star B * star U) = U * B * (star B * star U)
⊢ U * B * star (U * B) = U * B * (star B * star U)

Tactic:
rw [star_mul]

Premises used: StarMul.star_mul
-- Module: Mathlib.Algebra.Star.Unitary
Goal:
R : Type u_1
inst : Monoid R
inst_1 : StarMul R
U B : R
h : Membership.mem (γ := Set R) {U : R | star U * U = 1 ∧ U * star U = 1} U
h_1 : Membership.mem (γ := Set R) {U : R | star U * U = 1 ∧ U * star U = 1} B
hA₁ : star U * U = 1
hA₂ : U * star U = 1
hB₁ : star B * B = 1
hB₂ : B * star B = 1
⊢ U * B * (star B * star U) = U * (B * star B) * star U

Tactic:
simp_rw [← mul_assoc]

Premises used: mul_assoc
-- Module: Mathlib.Algebra.Star.Unitary
Goal:
R : Type u_1
inst : Monoid R
inst_1 : StarMul R
U B : R
h : Membership.mem (γ := Set R) {U : R | star U * U = 1 ∧ U * star U = 1} U
h_1 : Membership.mem (γ := Set R) {U : R | star U * U = 1 ∧ U * star U = 1} B
hA₁ : star U * U = 1
hA₂ : U * star U = 1
hB₁ : star B * B = 1
hB₂ : B * star B = 1
rw : U * 1 * star U = 1
rw₁ : U * star U = 1
rw₂ rw₃ : Eq.{u_1 + 1} (α := R) 1 1
⊢ U * (B * star B) * star U = 1

Tactic:
rw [hB₂, mul_one, hA₂]

Premises used: mul_one
-- Module: Mathlib.Algebra.Star.Unitary
Goal:
R : Type u_1
inst : Monoid R
inst_1 : StarMul R
U B : R
h : Membership.mem (γ := Set R) {U : R | star U * U = 1 ∧ U * star U = 1} U
h_1 : Membership.mem (γ := Set R) {U : R | star U * U = 1 ∧ U * star U = 1} B
hA₁ : star U * U = 1
hA₂ : U * star U = 1
hB₁ : star B * B = 1
hB₂ : B * star B = 1
U₁ : U * B * star (U * B) = U * B * (star B * star U)
U₂ : U * B * (star B * star U) = U * (B * star B) * star U
U₃ : U * (B * star B) * star U = 1
⊢ U * B * star (U * B) = 1

Tactic:
calc
        U * B * star (U * B) = U * B * (star B * star U) := by rw [star_mul]
        _ = U * (B * star B) * star U := by simp_rw [← mul_assoc]
        _ = 1 := by rw [hB₂, mul_one, hA₂]

Premises used: HMul.hMul, Star.star
-- Module: Mathlib.Algebra.Star.Unitary
Goal:
R : Type u_1
inst : Monoid R
inst_1 : StarMul R
⊢ Membership.mem (γ := Set R) {U : R | star U * U = 1 ∧ U * star U = 1} 1

Tactic:
simp only [mul_one, and_self_iff, Set.mem_setOf_eq, star_one]

Premises used: Set.mem_setOf_eq, and_self_iff, mul_one, star_one
-- Module: Mathlib.Algebra.Star.Unitary
Goal:
R : Type u_1
inst : Monoid R
inst_1 : StarMul R
U : R
⊢ Membership.mem (γ := Submonoid R) (unitary R) U ↔ star U * U = 1 ∧ U * star U = 1

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf
-- Module: Mathlib.Algebra.Star.Unitary
Goal:
R : Type u_1
inst : Monoid R
inst_1 : StarMul R
U : R
hU : Membership.mem (γ := Submonoid R) (unitary R) U
⊢ star U * U = 1

Tactic:
hU.1

Premises used: And.left
-- Module: Mathlib.Algebra.Star.Unitary
Goal:
R : Type u_1
inst : Monoid R
inst_1 : StarMul R
U : R
hU : Membership.mem (γ := Submonoid R) (unitary R) U
⊢ U * star U = 1

Tactic:
hU.2

Premises used: And.right
-- Module: Mathlib.Algebra.Star.Unitary
Goal:
R : Type u_1
inst : Monoid R
inst_1 : StarMul R
U : R
hU : Membership.mem (γ := Submonoid R) (unitary R) U
rw : U * star U = 1
rw₁ rw₂ : Eq.{u_1 + 1} (α := R) 1 1
⊢ star (star U) * star U = 1

Tactic:
rw [star_star, mul_star_self_of_mem hU]

Premises used: star_star, Unitary.mul_star_self_of_mem
-- Module: Mathlib.Algebra.Star.Unitary
Goal:
R : Type u_1
inst : Monoid R
inst_1 : StarMul R
U : R
hU : Membership.mem (γ := Submonoid R) (unitary R) U
rw : star U * U = 1
rw₁ rw₂ : Eq.{u_1 + 1} (α := R) 1 1
⊢ star U * star (star U) = 1

Tactic:
rw [star_star, star_mul_self_of_mem hU]

Premises used: star_star, Unitary.star_mul_self_of_mem
-- Module: Mathlib.Algebra.Star.Unitary
Goal:
R : Type u_1
inst : Monoid R
inst_1 : StarMul R
U : R
⊢ Membership.mem (γ := Submonoid R) (unitary R) (star U) ↔ Membership.mem (γ := Submonoid R) (unitary R) U

Tactic:
⟨fun h => star_star U ▸ star_mem h, star_mem⟩

Premises used: star_star, Eq.rec, Iff.intro, Unitary.star_mem
-- Module: Mathlib.Algebra.Star.Unitary
Goal:
R : Type u_1
inst : Monoid R
inst_1 : StarMul R
U : ↥(unitary R)
⊢ (↑(star U) : R) = star (↑U : R)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Star.Unitary
Goal:
R : Type u_1
inst : Monoid R
inst_1 : StarMul R
U : ↥(unitary R)
⊢ star (↑U : R) * (↑U : R) = 1

Tactic:
star_mul_self_of_mem U.prop

Premises used: Unitary.star_mul_self_of_mem, Subtype.prop
-- Module: Mathlib.Algebra.Star.Unitary
Goal:
R : Type u_1
inst : Monoid R
inst_1 : StarMul R
U : ↥(unitary R)
⊢ (↑U : R) * (↑(star U) : R) = 1

Tactic:
mul_star_self_of_mem U.prop

Premises used: Subtype.prop, Unitary.mul_star_self_of_mem
-- Module: Mathlib.Algebra.Star.Unitary
Goal:
R : Type u_1
inst : Monoid R
inst_1 : StarMul R
U : ↥(unitary R)
⊢ star U * U = 1

Tactic:
Subtype.ext <| coe_star_mul_self U

Premises used: Unitary.coe_star_mul_self, Subtype.ext
-- Module: Mathlib.Algebra.Star.Unitary
Goal:
R : Type u_1
inst : Monoid R
inst_1 : StarMul R
U : ↥(unitary R)
⊢ U * star U = 1

Tactic:
Subtype.ext <| coe_mul_star_self U

Premises used: Unitary.coe_mul_star_self, Subtype.ext
-- Module: Mathlib.Algebra.Star.Unitary
Goal:
R : Type u_1
inst : Monoid R
inst_1 : StarMul R
x : ↥(unitary R)
a : (↑(star (star x)) : R) = (↑x : R)
⊢ star (star x) = x

Tactic:
ext
-- Module: Mathlib.Algebra.Star.Unitary
Goal:
R : Type u_1
inst : Monoid R
inst_1 : StarMul R
x : ↥(unitary R)
a : star (↑(star x) : R) = (↑x : R)
a₁ : star (star (↑x : R)) = (↑x : R)
a₂ a₃ : (↑x : R) = (↑x : R)
⊢ (↑(star (star x)) : R) = (↑x : R)

Tactic:
rw [coe_star, coe_star, star_star]

Premises used: star_star, Unitary.coe_star
-- Module: Mathlib.Algebra.Star.Unitary
Goal:
R : Type u_1
inst : Monoid R
inst_1 : StarMul R
x y : ↥(unitary R)
a : (↑(star (x * y)) : R) = (↑(star y * star x) : R)
⊢ star (x * y) = star y * star x

Tactic:
ext
-- Module: Mathlib.Algebra.Star.Unitary
Goal:
R : Type u_1
inst : Monoid R
inst_1 : StarMul R
x y : ↥(unitary R)
a : star (↑(x * y) : R) = (↑(star y * star x) : R)
a₁ : star ((↑x : R) * (↑y : R)) = (↑(star y * star x) : R)
a₂ : star ((↑x : R) * (↑y : R)) = (↑(star y) : R) * (↑(star x) : R)
a₃ : star ((↑x : R) * (↑y : R)) = star (↑y : R) * (↑(star x) : R)
a₄ : star ((↑x : R) * (↑y : R)) = star (↑y : R) * star (↑x : R)
a₅ a₆ : star (↑y : R) * star (↑x : R) = star (↑y : R) * star (↑x : R)
⊢ (↑(star (x * y)) : R) = (↑(star y * star x) : R)

Tactic:
rw [coe_star, Submonoid.coe_mul, Submonoid.coe_mul, coe_star, coe_star, star_mul]

Premises used: StarMul.star_mul, Unitary.coe_star, Submonoid.coe_mul
-- Module: Mathlib.Algebra.Star.Unitary
Goal:
R : Type u_1
inst : Monoid R
inst_1 : StarMul R
U : ↥(unitary R)
⊢ star U = U⁻¹

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Star.Unitary
Goal:
R : Type u_1
inst : Monoid R
inst_1 : StarMul R
⊢ Eq.{u_1 + 1} (α := ↥(unitary R) → ↥(unitary R)) star Inv.inv

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Star.Unitary
Goal:
R : Type u_1
inst : Monoid R
inst_1 : StarMul R
⊢ Function.Injective.{u_1 + 1, u_1 + 1} (α := ↥(unitary R)) (β := Rˣ) (⇑toUnits : (a : ↥(unitary R)) → Rˣ)

Tactic:
fun _ _ h =>
  Subtype.ext <| Units.ext_iff.mp h

Premises used: Units.ext_iff, Iff.mp, Function.Injective, Subtype.ext
-- Module: Mathlib.Algebra.Star.Unitary
Goal:
R : Type u_1
inst : Monoid R
inst_1 : StarMul R
u : R
hu : IsUnit u
rw : ∀ (h_mul : star u * u = 1), u * star u = 1
⊢ Membership.mem (γ := Submonoid R) (unitary R) u ↔ star u * u = 1

Tactic:
rw [mem_iff, and_iff_left_of_imp fun h_mul => ?_]

Premises used: and_iff_left_of_imp, Unitary.mem_iff
-- Module: Mathlib.Algebra.Star.Unitary
Goal:
R : Type u_1
inst : Monoid R
inst_1 : StarMul R
u : R
hu : IsUnit u
h_mul : star u * u = 1
⊢ IsUnit u

Tactic:
hu
-- Module: Mathlib.Algebra.Star.Unitary
Goal:
R : Type u_1
inst : Monoid R
inst_1 : StarMul R
u : R
hu : IsUnit u
h_mul : star u * u = 1
lift : ∀ (u : Rˣ) (h_mul : star (↑u : R) * (↑u : R) = 1), (↑u : R) * star (↑u : R) = 1
⊢ u * star u = 1

Tactic:
lift u to Rˣ using hu
-- Module: Mathlib.Algebra.Star.Unitary
Goal:
R : Type u_1
inst : Monoid R
inst_1 : StarMul R
u : Rˣ
h_mul : star (↑u : R) * (↑u : R) = 1
⊢ (↑u : R) * star (↑u : R) = 1

Tactic:
left_inv_eq_right_inv h_mul u.mul_inv ▸ u.mul_inv

Premises used: Eq.rec, Units.mul_inv, left_inv_eq_right_inv, Eq.symm
-- Module: Mathlib.Algebra.Star.Unitary
Goal:
R : Type u_1
inst : Monoid R
inst_1 : StarMul R
u : Rˣ
h_mul : star (↑u : R) * (↑u : R) = 1
⊢ (↑u : R) * star (↑u : R) = 1

Tactic:
exact left_inv_eq_right_inv h_mul u.mul_inv ▸ u.mul_inv
-- Module: Mathlib.Algebra.Star.Unitary
Goal:
R : Type u_1
inst : Monoid R
inst_1 : StarMul R
u : R
hu : IsUnit u
rw : Membership.mem (γ := Submonoid R) (unitary R) (star u) ↔ u * star u = 1
rw₁ : star (star u) * star u = 1 ↔ u * star u = 1
rw₂ rw₃ : u * star u = 1 ↔ u * star u = 1
⊢ Membership.mem (γ := Submonoid R) (unitary R) u ↔ u * star u = 1

Tactic:
rw [← star_mem_iff, hu.star.mem_unitary_iff_star_mul_self, star_star]

Premises used: IsUnit.star, star_star, Unitary.star_mem_iff, IsUnit.mem_unitary_iff_star_mul_self
-- Module: Mathlib.Algebra.Star.Unitary
Goal:
R : Type u_1
inst : Monoid R
inst_1 : StarMul R
U : ↥(unitary R)
⊢ IsUnit (↑U : R)

Tactic:
(Unitary.toUnits _).isUnit

Premises used: Unitary.toUnits, Units.isUnit, DFunLike.coe
-- Module: Mathlib.Algebra.Star.Unitary
Goal:
R : Type u_1
inst : Monoid R
inst_1 : StarMul R
x y : R
U : ↥(unitary R)
⊢ x * (↑U : R) = y * (↑U : R) ↔ x = y

Tactic:
val_toUnits_apply U ▸ Units.mul_left_inj _

Premises used: Eq.rec, Unitary.val_toUnits_apply, Units.mul_left_inj
-- Module: Mathlib.Algebra.Star.Unitary
Goal:
R : Type u_1
inst : Monoid R
inst_1 : StarMul R
x y : R
U : ↥(unitary R)
⊢ (↑U : R) * x = (↑U : R) * y ↔ x = y

Tactic:
val_toUnits_apply U ▸ Units.mul_right_inj _

Premises used: Eq.rec, Unitary.val_toUnits_apply, Units.mul_right_inj
-- Module: Mathlib.Algebra.Star.Unitary
Goal:
G : Type u_2
inst : Group G
inst_1 : StarMul G
a b : G
rw : star (a * b⁻¹) * (a * b⁻¹) = 1 ↔ star a * a = star b * b
rw₁ : star b⁻¹ * star a * (a * b⁻¹) = 1 ↔ star a * a = star b * b
rw₂ : (star b)⁻¹ * star a * (a * b⁻¹) = 1 ↔ star a * a = star b * b
rw₃ : (star b)⁻¹ * (star a * (a * b⁻¹)) = 1 ↔ star a * a = star b * b
rw₄ : star a * (a * b⁻¹) = star b * 1 ↔ star a * a = star b * b
rw₅ : star a * (a * b⁻¹) = star b ↔ star a * a = star b * b
rw₆ : star a * a * b⁻¹ = star b ↔ star a * a = star b * b
rw₇ rw₈ : star a * a = star b * b ↔ star a * a = star b * b
⊢ Membership.mem (γ := Submonoid G) (unitary G) (a * b⁻¹) ↔ star a * a = star b * b

Tactic:
rw [(Group.isUnit _).mem_unitary_iff_star_mul_self, star_mul, star_inv, mul_assoc,
    inv_mul_eq_iff_eq_mul, mul_one, ← mul_assoc, mul_inv_eq_iff_eq_mul]

Premises used: mul_assoc, Group.isUnit, StarMul.star_mul, mul_one, mul_inv_eq_iff_eq_mul, inv_mul_eq_iff_eq_mul, IsUnit.mem_unitary_iff_star_mul_self, star_inv
-- Module: Mathlib.Algebra.Star.Unitary
Goal:
G : Type u_2
inst : Group G
inst_1 : StarMul G
a b : G
⊢ Membership.mem (γ := Submonoid G) (unitary G) (a⁻¹ * b) ↔ a * star a = b * star b

Tactic:
simpa [← mul_inv_rev] using mul_inv_mem_iff a⁻¹ b⁻¹

Premises used: Unitary.mul_inv_mem_iff, Inv.inv, mul_inv_rev
-- Module: Mathlib.Algebra.Star.Unitary
Goal:
R : Type u_1
inst : Monoid R
inst_1 : StarMul R
h :
  ∀ (x : Rˣ),
    Membership.mem (γ := Submonoid Rˣ) (unitary Rˣ) x ↔
      Membership.mem (γ := Submonoid Rˣ) (Submonoid.comap (F := Rˣ →* R) (Units.coeHom R) (unitary R)) x
⊢ Eq (α := Submonoid Rˣ) (unitary Rˣ) (Submonoid.comap (F := Rˣ →* R) (Units.coeHom R) (unitary R))

Tactic:
ext
-- Module: Mathlib.Algebra.Star.Unitary
Goal:
R : Type u_1
inst : Monoid R
inst_1 : StarMul R
x : Rˣ
⊢ Membership.mem (γ := Submonoid Rˣ) (unitary Rˣ) x ↔
    Membership.mem (γ := Submonoid Rˣ) (Submonoid.comap (F := Rˣ →* R) (Units.coeHom R) (unitary R)) x

Tactic:
simp [mem_iff, Units.ext_iff]

Premises used: Units.ext_iff, Unitary.mem_iff
-- Module: Mathlib.Algebra.Star.Unitary
Goal:
R : Type u_1
inst : Monoid R
inst_1 : StarMul R
a b : Rˣ
⊢ Membership.mem (γ := Submonoid R) (unitary R) ((↑a : R) * (↑b⁻¹ : R)) ↔ star a * a = star b * b

Tactic:
simp [← mul_inv_mem_iff, Units.unitary_eq]

Premises used: Units.unitary_eq, Unitary.mul_inv_mem_iff
-- Module: Mathlib.Algebra.Star.Unitary
Goal:
R : Type u_1
inst : Monoid R
inst_1 : StarMul R
a b : Rˣ
⊢ Membership.mem (γ := Submonoid R) (unitary R) ((↑a⁻¹ : R) * (↑b : R)) ↔ a * star a = b * star b

Tactic:
simp [← inv_mul_mem_iff, Units.unitary_eq]

Premises used: Unitary.inv_mul_mem_iff, Units.unitary_eq
-- Module: Mathlib.Algebra.Star.Unitary
Goal:
R : Type u_1
inst : Monoid R
inst_1 : StarMul R
u : R
hu : Membership.mem (γ := Submonoid R) (unitary R) u
⊢ IsStarNormal u

Tactic:
coe_isStarNormal ⟨u, hu⟩

Premises used: Subtype.mk, Unitary.coe_isStarNormal
-- Module: Mathlib.Algebra.Star.Unitary
Goal:
G : Type u_2
inst : Group G
inst_1 : StarMul G
g : G
hg : Membership.mem (γ := Submonoid G) (unitary G) g
simp_rw : ∀ (hg : star g * g = 1 ∧ g * star g = 1), g * star g = 1 ∧ star g * g = 1
⊢ Membership.mem (γ := Submonoid G) (unitary G) g⁻¹

Tactic:
simp_rw [mem_iff, star_inv, ← mul_inv_rev, inv_eq_one] at *

Premises used: inv_eq_one, Unitary.mem_iff, mul_inv_rev, star_inv
-- Module: Mathlib.Algebra.Star.Unitary
Goal:
G : Type u_2
inst : Group G
inst_1 : StarMul G
g : G
hg : star g * g = 1 ∧ g * star g = 1
⊢ g * star g = 1 ∧ star g * g = 1

Tactic:
hg.symm

Premises used: And.symm
-- Module: Mathlib.Algebra.Star.Unitary
Goal:
G : Type u_2
inst : Group G
inst_1 : StarMul G
g : G
hg : star g * g = 1 ∧ g * star g = 1
⊢ g * star g = 1 ∧ star g * g = 1

Tactic:
exact hg.symm

Premises used: And.symm
-- Module: Mathlib.Algebra.Star.Unitary
Goal:
G : Type u_2
inst : Group G
inst_1 : StarMul G
⊢ Eq (α := Submonoid G) (Subgroup.toSubmonoid (unitarySubgroup G)) (unitary G)

Tactic:
rfl

Premises used: unitary, rfl
-- Module: Mathlib.Algebra.Star.Unitary
Goal:
G : Type u_2
inst : Group G
inst_1 : StarMul G
g : G
⊢ Membership.mem (γ := Subgroup G) (unitarySubgroup G) g ↔ Membership.mem (γ := Submonoid G) (unitary G) g

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl
-- Module: Mathlib.Algebra.Star.Unitary
Goal:
G : Type u_2
inst : Group G
inst_1 : StarMul G
g : G
⊢ Membership.mem (γ := Submonoid G) (unitary G) g⁻¹ ↔ Membership.mem (γ := Submonoid G) (unitary G) g

Tactic:
inv_mem_iff (H := unitarySubgroup G)

Premises used: Set.Mem, setOf, inv_mem_iff
-- Module: Mathlib.Algebra.Star.Unitary
Goal:
R : Type u_1
A : Type u_2
inst : Monoid R
inst_1 : Monoid A
inst_2 : MulAction R A
inst_3 : SMulCommClass R A A
inst_4 : IsScalarTower R A A
inst_5 : StarMul R
inst_6 : StarMul A
inst_7 : StarModule R A
r : R
a : A
hr : Membership.mem (γ := Submonoid R) (unitary R) r
ha : Membership.mem (γ := Submonoid A) (unitary A) a
⊢ Membership.mem (γ := Submonoid A) (unitary A) (r • a)

Tactic:
simp [mem_iff, smul_smul, mul_smul_comm, smul_mul_assoc, hr, ha]

Premises used: smul_smul, smul_mul_assoc, Unitary.mem_iff, mul_smul_comm
-- Module: Mathlib.Algebra.Star.Unitary
Goal:
R : Type u_1
A : Type u_2
inst : Monoid R
inst_1 : Monoid A
inst_2 : MulAction R A
inst_3 : SMulCommClass R A A
inst_4 : IsScalarTower R A A
inst_5 : StarMul R
inst_6 : StarMul A
inst_7 : StarModule R A
r : ↥(unitary R)
a : A
ha : Membership.mem (γ := Submonoid A) (unitary A) a
⊢ Membership.mem (γ := Submonoid A) (unitary A) (r • a)

Tactic:
smul_mem_of_mem (R := R) r.prop ha

Premises used: Set.Mem, setOf, Unitary.smul_mem_of_mem, Subtype.prop
-- Module: Mathlib.Algebra.Star.Unitary
Goal:
R : Type u_1
A : Type u_2
inst : Monoid R
inst_1 : Monoid A
inst_2 : MulAction R A
inst_3 : SMulCommClass R A A
inst_4 : IsScalarTower R A A
inst_5 : StarMul R
inst_6 : StarMul A
inst_7 : StarModule R A
r : ↥(unitary R)
a : ↥(unitary A)
⊢ (↑(r • a) : A) = r • (↑a : A)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Star.Unitary
Goal:
R : Type u_2
S : Type u_3
inst : Monoid R
inst_1 : StarMul R
inst_2 : Monoid S
inst_3 : StarMul S
F : Type u_5
inst_4 : FunLike F R S
inst_5 : StarHomClass F R S
inst_6 : MonoidHomClass F R S
f : F
r : R
hr : Membership.mem (γ := Submonoid R) (unitary R) r
⊢ star r * r = 1 ∧ r * star r = 1

Tactic:
rw [mem_iff] at hr

Premises used: Unitary.mem_iff
-- Module: Mathlib.Algebra.Star.Unitary
Goal:
R : Type u_2
S : Type u_3
inst : Monoid R
inst_1 : StarMul R
inst_2 : Monoid S
inst_3 : StarMul S
F : Type u_5
inst_4 : FunLike F R S
inst_5 : StarHomClass F R S
inst_6 : MonoidHomClass F R S
f : F
r : R
hr : star r * r = 1 ∧ r * star r = 1
⊢ Membership.mem (α := S) (γ := Submonoid S) (unitary S) ((f : (a : R) → S) r : S)

Tactic:
simpa [map_star, map_mul] using And.intro congr(f $(hr.1)) congr(f $(hr.2))

Premises used: congrArg, StarHomClass.map_star, id, map_mul, And.right, And.left, And.intro, DFunLike.coe
-- Module: Mathlib.Algebra.Star.Unitary
Goal:
R : Type u_2
S : Type u_3
inst : Monoid R
inst_1 : StarMul R
inst_2 : Monoid S
inst_3 : StarMul S
f : R →⋆* S
x : ↥(unitary R)
⊢ Eq.{u_3 + 1} (α := S) ((↑((map f : (a : ↥(unitary R)) → ↥(unitary S)) x) : S) : S) ((f : (a : R) → S) (↑x : R) : S)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Star.Unitary
Goal:
R : Type u_2
S : Type u_3
inst : Monoid R
inst_1 : StarMul R
inst_2 : Monoid S
inst_3 : StarMul S
f : R →⋆* S
x : ↥(unitary R)
⊢ Eq.{u_3 + 1} (α := S) ((↑((map f : (a : ↥(unitary R)) → ↥(unitary S)) (star x)) : S) : S)
    ((f : (a : R) → S) (star (↑x : R)) : S)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Star.Unitary
Goal:
R : Type u_2
inst : Monoid R
inst_1 : StarMul R
⊢ Eq (α := ↥(unitary R) →⋆* ↥(unitary R)) (map (StarMonoidHom.id R)) (StarMonoidHom.id ↥(unitary R))

Tactic:
rfl

Premises used: Subtype.map, Unitary.map, StarMonoidHom.id, rfl
-- Module: Mathlib.Algebra.Star.Unitary
Goal:
R : Type u_2
S : Type u_3
T : Type u_4
inst : Monoid R
inst_1 : StarMul R
inst_2 : Monoid S
inst_3 : StarMul S
inst_4 : Monoid T
inst_5 : StarMul T
g : S →⋆* T
f : R →⋆* S
⊢ map (g.comp f) = (map g).comp (map f)

Tactic:
rfl

Premises used: Subtype.map, Unitary.map, StarMonoidHom.comp, rfl
-- Module: Mathlib.Algebra.Star.Unitary
Goal:
R : Type u_2
S : Type u_3
inst : Monoid R
inst_1 : StarMul R
inst_2 : Monoid S
inst_3 : StarMul S
f : R →⋆* S
hf : Function.Injective.{u_2 + 1, u_3 + 1} (α := R) (β := S) (⇑f : (a : R) → S)
⊢ Function.Injective.{u_2 + 1, u_3 + 1} (α := ↥(unitary R)) (β := ↥(unitary S))
    (⇑(map f) : (a : ↥(unitary R)) → ↥(unitary S))

Tactic:
Subtype.map_injective (fun _ ↦ map_mem f) hf

Premises used: Subtype.map, Unitary.map_mem, Subtype.map_injective
-- Module: Mathlib.Algebra.Star.Unitary
Goal:
R : Type u_2
S : Type u_3
inst : Monoid R
inst_1 : StarMul R
inst_2 : Monoid S
inst_3 : StarMul S
f : R →⋆* S
h :
  ∀ (x : ↥(unitary R)),
    Eq.{u_3 + 1} (α := S) (↑((MonoidHom.comp toUnits (map f).toMonoidHom : (a : ↥(unitary R)) → Sˣ) x) : S)
      (↑((((Units.map f.toMonoidHom).comp toUnits : MonoidHom.{u_2, u_3} (↥(unitary R)) Sˣ) : (a : ↥(unitary R)) → Sˣ)
            x) :
        S)
⊢ MonoidHom.comp toUnits (map f).toMonoidHom = (Units.map f.toMonoidHom).comp toUnits

Tactic:
ext
-- Module: Mathlib.Algebra.Star.Unitary
Goal:
R : Type u_2
S : Type u_3
inst : Monoid R
inst_1 : StarMul R
inst_2 : Monoid S
inst_3 : StarMul S
f : R →⋆* S
x : ↥(unitary R)
⊢ Eq.{u_3 + 1} (α := S) (↑((MonoidHom.comp toUnits (map f).toMonoidHom : (a : ↥(unitary R)) → Sˣ) x) : S)
    (↑((((Units.map f.toMonoidHom).comp toUnits : MonoidHom.{u_2, u_3} (↥(unitary R)) Sˣ) : (a : ↥(unitary R)) → Sˣ)
          x) :
      S)

Tactic:
rfl
-- Module: Mathlib.Algebra.Star.Unitary
Goal:
R : Type u_2
inst : Monoid R
inst_1 : StarMul R
⊢ Eq (α := ↥(unitary R) ≃⋆* ↥(unitary R)) (mapEquiv (StarMulEquiv.refl R)) (StarMulEquiv.refl ↥(unitary R))

Tactic:
rfl

Premises used: MulEquiv.refl, Subtype.map, StarMulEquiv.refl, Equiv.refl, rfl, Unitary.mapEquiv
-- Module: Mathlib.Algebra.Star.Unitary
Goal:
R : Type u_2
S : Type u_3
inst : Monoid R
inst_1 : StarMul R
inst_2 : Monoid S
inst_3 : StarMul S
f : R ≃⋆* S
⊢ mapEquiv f.symm = (mapEquiv f).symm

Tactic:
rfl

Premises used: Equiv.symm, MulEquiv.symm, StarMulEquiv.symm, rfl, Unitary.mapEquiv
-- Module: Mathlib.Algebra.Star.Unitary
Goal:
R : Type u_2
S : Type u_3
T : Type u_4
inst : Monoid R
inst_1 : StarMul R
inst_2 : Monoid S
inst_3 : StarMul S
inst_4 : Monoid T
inst_5 : StarMul T
f : R ≃⋆* S
g : S ≃⋆* T
⊢ mapEquiv (f.trans g) = (mapEquiv f).trans (mapEquiv g)

Tactic:
rfl

Premises used: Subtype.map, Equiv.trans, MulEquiv.trans, StarMulEquiv.trans, rfl, Unitary.mapEquiv
-- Module: Mathlib.Algebra.Star.Unitary
Goal:
R : Type u_2
S : Type u_3
inst : Monoid R
inst_1 : StarMul R
inst_2 : Monoid S
inst_3 : StarMul S
f : R ≃⋆* S
⊢ (mapEquiv f).toStarMonoidHom = map f.toStarMonoidHom

Tactic:
rfl

Premises used: Subtype.map, Unitary.map, StarMulEquiv.toStarMonoidHom, rfl
-- Module: Mathlib.Algebra.Star.Unitary
Goal:
R : Type u_1
inst : CommMonoid R
inst_1 : StarMul R
U : R
⊢ Membership.mem (γ := Submonoid R) (unitary R) U ↔ star U * U = 1

Tactic:
mem_iff.trans <| and_iff_left_of_imp fun h => mul_comm (star U) U ▸ h

Premises used: and_iff_left_of_imp, Eq.rec, mul_comm, Iff.trans, Unitary.mem_iff, Star.star
-- Module: Mathlib.Algebra.Star.Unitary
Goal:
R : Type u_1
inst : CommMonoid R
inst_1 : StarMul R
U : R
⊢ Membership.mem (γ := Submonoid R) (unitary R) U ↔ U * star U = 1

Tactic:
mem_iff.trans <| and_iff_right_of_imp fun h => mul_comm U (star U) ▸ h

Premises used: Eq.rec, mul_comm, Iff.trans, Unitary.mem_iff, and_iff_right_of_imp, Star.star
-- Module: Mathlib.Algebra.Star.Unitary
Goal:
R : Type u_1
inst : GroupWithZero R
inst_1 : StarMul R
U : ↥(unitary R)
⊢ (↑U⁻¹ : R) = (↑U : R)⁻¹

Tactic:
eq_inv_of_mul_eq_one_right <| coe_mul_star_self _

Premises used: Unitary.coe_mul_star_self, eq_inv_of_mul_eq_one_right
-- Module: Mathlib.Algebra.Star.Unitary
Goal:
R : Type u_1
inst : GroupWithZero R
inst_1 : StarMul R
U₁ U₂ : ↥(unitary R)
⊢ (↑(U₁ / U₂) : R) = (↑U₁ : R) / (↑U₂ : R)

Tactic:
simp only [div_eq_mul_inv, coe_inv, Submonoid.coe_mul]

Premises used: div_eq_mul_inv, Submonoid.coe_mul, Unitary.coe_inv
-- Module: Mathlib.Algebra.Star.Unitary
Goal:
R : Type u_1
inst : GroupWithZero R
inst_1 : StarMul R
U : ↥(unitary R)
z : ℤ
ofNat : ∀ (a : ℕ), (↑(U ^ Int.ofNat a) : R) = (↑U : R) ^ Int.ofNat a
negSucc : ∀ (a : ℕ), (↑(U ^ Int.negSucc a) : R) = (↑U : R) ^ Int.negSucc a
⊢ (↑(U ^ z) : R) = (↑U : R) ^ z

Tactic:
cases z