awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Star.Subalgebra (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : Semiring A
inst_3 : StarRing A
inst_4 : Algebra R A
inst_5 : StarModule R A
S : StarSubalgebra R A
⊢ S.toNonUnitalStarSubalgebra.toStarSubalgebra ⋯ = S
have mk : ∀ (toSubalgebra : Subalgebra R A) (star_mem' : ∀ {a : A}, a ∈ toSubalgebra.carrier → star a ∈ toSubalgebra.carrier),
  Eq (α := StarSubalgebra R A)
    ((toNonUnitalStarSubalgebra { toSubalgebra := toSubalgebra, star_mem' := @star_mem' }).toStarSubalgebra sorry)
    { toSubalgebra := toSubalgebra, star_mem' := @star_mem' }
Tactic: cases S
Cleared hypotheses: S
-- Lean 4 proof step from Mathlib.Algebra.Star.Subalgebra (goal)
Goal:
R : Type u_1
A : Type u_2
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : Semiring A
inst_3 : StarRing A
inst_4 : Algebra R A
inst_5 : StarModule R A
S : NonUnitalStarSubalgebra R A
h1 : 1 ∈ S
⊢ StarSubalgebra.toNonUnitalStarSubalgebra (S.toStarSubalgebra h1) = S
have mk : ∀ (toNonUnitalSubalgebra : NonUnitalSubalgebra R A)
  (star_mem' : ∀ {a : A} (_ha : a ∈ toNonUnitalSubalgebra.carrier), star a ∈ toNonUnitalSubalgebra.carrier)
  (h1 : 1 ∈ { toNonUnitalSubalgebra := toNonUnitalSubalgebra, star_mem' := @star_mem' : NonUnitalStarSubalgebra R A }),
  StarSubalgebra.toNonUnitalStarSubalgebra
      ({ toNonUnitalSubalgebra := toNonUnitalSubalgebra, star_mem' := @star_mem' :
            NonUnitalStarSubalgebra R A }.toStarSubalgebra
        h1) =
    { toNonUnitalSubalgebra := toNonUnitalSubalgebra, star_mem' := @star_mem' }
Tactic: cases S
Cleared hypotheses: S, h1
-- Lean 4 proof step from Mathlib.Algebra.Star.Subsemiring (goal)
Goal:
R : Type v
inst : NonAssocSemiring R
inst_1 : Star R
p q : StarSubsemiring R
h :
  Eq.{v + 1} (α := Set R) ((fun {s : StarSubsemiring R} ↦ s.carrier) (s := p))
    ((fun {s : StarSubsemiring R} ↦ s.carrier) (s := q))
⊢ p = q
have obtain : ∀ (carrier : Set R) (mul_mem' : ∀ {a b : R}, a ∈ carrier → b ∈ carrier → a * b ∈ carrier)
  (one_mem' : 1 ∈ { carrier := carrier, mul_mem' := @mul_mem' : Subsemigroup R }.carrier)
  (add_mem' :
    ∀ {a b : R},
      a ∈ { carrier := carrier, mul_mem' := @mul_mem', one_mem' := one_mem' : Submonoid R }.carrier →
        b ∈ { carrier := carrier, mul_mem' := @mul_mem', one_mem' := one_mem' : Submonoid R }.carrier →
          a + b ∈ { carrier := carrier, mul_mem' := @mul_mem', one_mem' := one_mem' : Submonoid R }.carrier)
  (zero_mem' : 0 ∈ { carrier := carrier, mul_mem' := @mul_mem', one_mem' := one_mem' : Submonoid R }.carrier)
  (star_mem' :
    ∀ {a : R},
      a ∈
          { carrier := carrier, mul_mem' := @mul_mem', one_mem' := one_mem', add_mem' := @add_mem',
              zero_mem' := zero_mem' : Subsemiring R }.carrier →
        star a ∈
          { carrier := carrier, mul_mem' := @mul_mem', one_mem' := one_mem', add_mem' := @add_mem',
              zero_mem' := zero_mem' : Subsemiring R }.carrier)
  (h :
    Eq.{v + 1} (α := Set R)
      ((fun {s : StarSubsemiring R} ↦ s.carrier) (s :=
        { carrier := carrier, mul_mem' := @mul_mem', one_mem' := one_mem', add_mem' := @add_mem',
          zero_mem' := zero_mem', star_mem' := @star_mem' }))
      ((fun {s : StarSubsemiring R} ↦ s.carrier) (s := q))),
  { carrier := carrier, mul_mem' := @mul_mem', one_mem' := one_mem', add_mem' := @add_mem', zero_mem' := zero_mem',
      star_mem' := @star_mem' : StarSubsemiring R } =
    q
Tactic: obtain ⟨⟨⟨⟨_, _⟩, _⟩, _⟩, _⟩ := p
Cleared hypotheses: p, h
-- Lean 4 proof step from Mathlib.Algebra.Star.Subsemiring (goal)
Goal:
R : Type v
inst : NonAssocSemiring R
inst_1 : Star R
q : StarSubsemiring R
carrier : Set R
mul_mem' : ∀ {a b : R}, a ∈ carrier → b ∈ carrier → a * b ∈ carrier
one_mem' : 1 ∈ { carrier := carrier, mul_mem' := @mul_mem' : Subsemigroup R }.carrier
add_mem' :
  ∀ {a b : R},
    a ∈ { carrier := carrier, mul_mem' := @mul_mem', one_mem' := one_mem' : Submonoid R }.carrier →
      b ∈ { carrier := carrier, mul_mem' := @mul_mem', one_mem' := one_mem' : Submonoid R }.carrier →
        a + b ∈ { carrier := carrier, mul_mem' := @mul_mem', one_mem' := one_mem' : Submonoid R }.carrier
zero_mem' : 0 ∈ { carrier := carrier, mul_mem' := @mul_mem', one_mem' := one_mem' : Submonoid R }.carrier
star_mem' :
  ∀ {a : R},
    a ∈
        { carrier := carrier, mul_mem' := @mul_mem', one_mem' := one_mem', add_mem' := @add_mem',
            zero_mem' := zero_mem' : Subsemiring R }.carrier →
      star a ∈
        { carrier := carrier, mul_mem' := @mul_mem', one_mem' := one_mem', add_mem' := @add_mem',
            zero_mem' := zero_mem' : Subsemiring R }.carrier
h :
  Eq.{v + 1} (α := Set R)
    ((fun {s : StarSubsemiring R} ↦ s.carrier) (s :=
      { carrier := carrier, mul_mem' := @mul_mem', one_mem' := one_mem', add_mem' := @add_mem', zero_mem' := zero_mem',
        star_mem' := @star_mem' }))
    ((fun {s : StarSubsemiring R} ↦ s.carrier) (s := q))
⊢ { carrier := carrier, mul_mem' := @mul_mem', one_mem' := one_mem', add_mem' := @add_mem', zero_mem' := zero_mem',
      star_mem' := @star_mem' : StarSubsemiring R } =
    q
have mk : ∀ (toSubsemiring : Subsemiring R) (star_mem'_1 : ∀ {a : R}, a ∈ toSubsemiring.carrier → star a ∈ toSubsemiring.carrier)
  (h :
    Eq.{v + 1} (α := Set R)
      ((fun {s : StarSubsemiring R} ↦ s.carrier) (s :=
        { carrier := carrier, mul_mem' := @mul_mem', one_mem' := one_mem', add_mem' := @add_mem',
          zero_mem' := zero_mem', star_mem' := @star_mem' }))
      ((fun {s : StarSubsemiring R} ↦ s.carrier) (s := { toSubsemiring := toSubsemiring, star_mem' := @star_mem'_1 }))),
  { carrier := carrier, mul_mem' := @mul_mem', one_mem' := one_mem', add_mem' := @add_mem', zero_mem' := zero_mem',
      star_mem' := @star_mem' : StarSubsemiring R } =
    { toSubsemiring := toSubsemiring, star_mem' := @star_mem'_1 }
Tactic: cases q
Cleared hypotheses: q, h
-- Lean 4 proof step from Mathlib.Algebra.Star.Subsemiring (goal)
Goal:
R : Type v
inst : NonAssocSemiring R
inst_1 : StarRing R
S T : StarSubsemiring R
h : S.toSubsemiring = T.toSubsemiring
x : R
⊢ x ∈ S ↔ x ∈ T
have rw : x ∈ S.toSubsemiring ↔ x ∈ T
Tactic: rw [← mem_toSubsemiring, ← mem_toSubsemiring, h]
-- Lean 4 proof step from Mathlib.Algebra.Star.Subsemiring (goal)
Goal:
R : Type v
inst : NonAssocSemiring R
inst_1 : StarRing R
S T : StarSubsemiring R
h : S.toSubsemiring = T.toSubsemiring
x : R
rw : x ∈ S.toSubsemiring ↔ x ∈ T
⊢ x ∈ S ↔ x ∈ T
have rw₁ : x ∈ S.toSubsemiring ↔ x ∈ T.toSubsemiring
Tactic: rw [← mem_toSubsemiring, ← mem_toSubsemiring, h]
-- Lean 4 proof step from Mathlib.Algebra.Star.Subsemiring (goal)
Goal:
R : Type v
inst : NonAssocSemiring R
inst_1 : StarRing R
S T : StarSubsemiring R
h : S.toSubsemiring = T.toSubsemiring
x : R
rw : x ∈ S.toSubsemiring ↔ x ∈ T
rw₁ : x ∈ S.toSubsemiring ↔ x ∈ T.toSubsemiring
⊢ x ∈ S ↔ x ∈ T
have rw₂ : x ∈ T.toSubsemiring ↔ x ∈ T.toSubsemiring
Tactic: rw [← mem_toSubsemiring, ← mem_toSubsemiring, h]
-- Lean 4 proof step from Mathlib.Algebra.Star.TensorProduct (goal)
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : AddCommMonoid A
inst_3 : StarAddMonoid A
inst_4 : Module R A
inst_5 : StarModule R A
inst_6 : AddCommMonoid B
inst_7 : StarAddMonoid B
inst_8 : Module R B
inst_9 : StarModule R B
x : A ⊗[R] B
⊢ (congr (starLinearEquiv R) (starLinearEquiv R) : (a : A ⊗[R] B) → A ⊗[R] B)
      ((congr (starLinearEquiv R) (starLinearEquiv R) : (a : A ⊗[R] B) → A ⊗[R] B) x) =
    x
have rw : (congr (LinearEquiv.trans (σ₁₂ := starRingEnd R) (σ₂₃ := starRingEnd R) (starLinearEquiv R) (starLinearEquiv R))
        (LinearEquiv.trans (σ₁₂ := starRingEnd R) (σ₂₃ := starRingEnd R) (starLinearEquiv R) (starLinearEquiv R)) :
      (a : A ⊗[R] B) → A ⊗[R] B)
    x =
  x
Tactic: rw [congr_congr]
-- Lean 4 proof step from Mathlib.Algebra.Star.TensorProduct (goal)
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : AddCommMonoid A
inst_3 : StarAddMonoid A
inst_4 : Module R A
inst_5 : StarModule R A
inst_6 : AddCommMonoid B
inst_7 : StarAddMonoid B
inst_8 : Module R B
inst_9 : StarModule R B
x : A ⊗[R] B
⊢ (congr (LinearEquiv.trans (σ₁₂ := starRingEnd R) (σ₂₃ := starRingEnd R) (starLinearEquiv R) (starLinearEquiv R))
          (LinearEquiv.trans (σ₁₂ := starRingEnd R) (σ₂₃ := starRingEnd R) (starLinearEquiv R) (starLinearEquiv R)) :
        (a : A ⊗[R] B) → A ⊗[R] B)
      x =
    x
have h : Eq (α := A ≃ₗ[R] A)
  (LinearEquiv.trans (σ₁₂ := starRingEnd R) (σ₂₃ := starRingEnd R) (starLinearEquiv R) (starLinearEquiv R))
  (LinearEquiv.refl R A)
Tactic: convert! congr($congr_refl_refl x)
-- Lean 4 proof step from Mathlib.Algebra.Star.TensorProduct (goal)
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : AddCommMonoid A
inst_3 : StarAddMonoid A
inst_4 : Module R A
inst_5 : StarModule R A
inst_6 : AddCommMonoid B
inst_7 : StarAddMonoid B
inst_8 : Module R B
inst_9 : StarModule R B
x : A ⊗[R] B
h :
  Eq (α := A ≃ₗ[R] A)
    (LinearEquiv.trans (σ₁₂ := starRingEnd R) (σ₂₃ := starRingEnd R) (starLinearEquiv R) (starLinearEquiv R))
    (LinearEquiv.refl R A)
⊢ (congr (LinearEquiv.trans (σ₁₂ := starRingEnd R) (σ₂₃ := starRingEnd R) (starLinearEquiv R) (starLinearEquiv R))
          (LinearEquiv.trans (σ₁₂ := starRingEnd R) (σ₂₃ := starRingEnd R) (starLinearEquiv R) (starLinearEquiv R)) :
        (a : A ⊗[R] B) → A ⊗[R] B)
      x =
    x
have h₁ : Eq (α := B ≃ₗ[R] B)
  (LinearEquiv.trans (σ₁₂ := starRingEnd R) (σ₂₃ := starRingEnd R) (starLinearEquiv R) (starLinearEquiv R))
  (LinearEquiv.refl R B)
Tactic: convert! congr($congr_refl_refl x)
-- Lean 4 proof step from Mathlib.Algebra.Star.TensorProduct (goal)
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : AddCommMonoid A
inst_3 : StarAddMonoid A
inst_4 : Module R A
inst_5 : StarModule R A
inst_6 : AddCommMonoid B
inst_7 : StarAddMonoid B
inst_8 : Module R B
inst_9 : StarModule R B
x : A ⊗[R] B
⊢ Eq (α := A ≃ₗ[R] A)
    (LinearEquiv.trans (σ₁₂ := starRingEnd R) (σ₂₃ := starRingEnd R) (starLinearEquiv R) (starLinearEquiv R))
    (LinearEquiv.refl R A)
have h : ∀ (x : A),
  Eq (α := A)
    ((LinearEquiv.trans (σ₁₂ := starRingEnd R) (σ₂₃ := starRingEnd R) (starLinearEquiv R) (starLinearEquiv R) :
          (a : A) → A)
        x :
      A)
    ((LinearEquiv.refl R A : (a : A) → A) x : A)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Star.TensorProduct (goal)
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : AddCommMonoid A
inst_3 : StarAddMonoid A
inst_4 : Module R A
inst_5 : StarModule R A
inst_6 : AddCommMonoid B
inst_7 : StarAddMonoid B
inst_8 : Module R B
inst_9 : StarModule R B
x : A ⊗[R] B
⊢ Eq (α := B ≃ₗ[R] B)
    (LinearEquiv.trans (σ₁₂ := starRingEnd R) (σ₂₃ := starRingEnd R) (starLinearEquiv R) (starLinearEquiv R))
    (LinearEquiv.refl R B)
have h : ∀ (x : B),
  Eq (α := B)
    ((LinearEquiv.trans (σ₁₂ := starRingEnd R) (σ₂₃ := starRingEnd R) (starLinearEquiv R) (starLinearEquiv R) :
          (a : B) → B)
        x :
      B)
    ((LinearEquiv.refl R B : (a : B) → B) x : B)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Star.Unitary (goal)
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
⊢ Membership.mem (γ := Set R) {U : R | star U * U = 1 ∧ U * star U = 1} (U * B)
have refine_1 : star (U * B) * (U * B) = 1
Tactic: refine ⟨?_, ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Star.Unitary (goal)
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
refine_1 : star (U * B) * (U * B) = 1
⊢ Membership.mem (γ := Set R) {U : R | star U * U = 1 ∧ U * star U = 1} (U * B)
have refine_2 : U * B * star (U * B) = 1
Tactic: refine ⟨?_, ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Star.Unitary (goal)
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
⊢ star B * star U * U * B = star B * (star U * U) * B
have rw : star B * star U * U * B = star B * star U * U * B
Tactic: rw [← mul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Star.Unitary (goal)
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
⊢ star B * (star U * U) * B = 1
have rw : star B * 1 * B = 1
Tactic: rw [hA₁, mul_one, hB₁]
-- Lean 4 proof step from Mathlib.Algebra.Star.Unitary (goal)
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
⊢ star B * (star U * U) * B = 1
have rw₂ : Eq.{u_1 + 1} (α := R) 1 1
Tactic: rw [hA₁, mul_one, hB₁]
-- Lean 4 proof step from Mathlib.Algebra.Star.Unitary (goal)
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
⊢ star (U * B) * (U * B) = 1
have star : star (U * B) * (U * B) = star B * star U * U * B
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₁]
-- Lean 4 proof step from Mathlib.Algebra.Star.Unitary (goal)
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 (U * B) * (U * B) = 1
have star₁ : Star.star B * Star.star U * U * B = Star.star B * (Star.star U * U) * B
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₁]
-- Lean 4 proof step from Mathlib.Algebra.Star.Unitary (goal)
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 (U * B) * (U * B) = 1
have star₂ : Star.star B * (Star.star U * 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₁]
-- Lean 4 proof step from Mathlib.Algebra.Star.Unitary (goal)
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 (U * B) = U * B * (star B * star U)
have rw : U * B * (star B * star U) = U * B * (star B * star U)
Tactic: rw [star_mul]
-- Lean 4 proof step from Mathlib.Algebra.Star.Unitary (goal)
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 = 1
have rw : U * 1 * star U = 1
Tactic: rw [hB₂, mul_one, hA₂]
-- Lean 4 proof step from Mathlib.Algebra.Star.Unitary (goal)
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
⊢ U * (B * star B) * star U = 1
have rw₂ : Eq.{u_1 + 1} (α := R) 1 1
Tactic: rw [hB₂, mul_one, hA₂]
-- Lean 4 proof step from Mathlib.Algebra.Star.Unitary (goal)
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 (U * B) = 1
have U₁ : U * B * star (U * B) = U * B * (star B * star U)
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₂]
-- Lean 4 proof step from Mathlib.Algebra.Star.Unitary (goal)
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 * B * star (U * B) = 1
have U₂ : U * B * (star B * star U) = U * (B * star B) * star U
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₂]
-- Lean 4 proof step from Mathlib.Algebra.Star.Unitary (goal)
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 * B * star (U * B) = 1
have U₃ : U * (B * star B) * star U = 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₂]
-- Lean 4 proof step from Mathlib.Algebra.Star.Unitary (goal)
Goal:
R : Type u_1
inst : Monoid R
inst_1 : StarMul R
U : R
hU : Membership.mem (γ := Submonoid R) (unitary R) U
⊢ star (star U) * star U = 1
have rw : U * star U = 1
Tactic: rw [star_star, mul_star_self_of_mem hU]
-- Lean 4 proof step from Mathlib.Algebra.Star.Unitary (goal)
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
⊢ star (star U) * star U = 1
have rw₁ : Eq.{u_1 + 1} (α := R) 1 1
Tactic: rw [star_star, mul_star_self_of_mem hU]
-- Lean 4 proof step from Mathlib.Algebra.Star.Unitary (goal)
Goal:
R : Type u_1
inst : Monoid R
inst_1 : StarMul R
U : R
hU : Membership.mem (γ := Submonoid R) (unitary R) U
⊢ star U * star (star U) = 1
have rw : star U * U = 1
Tactic: rw [star_star, star_mul_self_of_mem hU]
-- Lean 4 proof step from Mathlib.Algebra.Star.Unitary (goal)
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
⊢ star U * star (star U) = 1
have rw₁ : Eq.{u_1 + 1} (α := R) 1 1
Tactic: rw [star_star, star_mul_self_of_mem hU]
-- Lean 4 proof step from Mathlib.Algebra.Star.Unitary (goal)
Goal:
R : Type u_1
inst : Monoid R
inst_1 : StarMul R
x : ↥(unitary R)
⊢ star (star x) = x
have a : (↑(star (star x)) : R) = (↑x : R)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Star.Unitary (goal)
Goal:
R : Type u_1
inst : Monoid R
inst_1 : StarMul R
x : ↥(unitary R)
⊢ (↑(star (star x)) : R) = (↑x : R)
have a : star (↑(star x) : R) = (↑x : R)
Tactic: rw [coe_star, coe_star, star_star]
-- Lean 4 proof step from Mathlib.Algebra.Star.Unitary (goal)
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)) : R) = (↑x : R)
have a₁ : star (star (↑x : R)) = (↑x : R)
Tactic: rw [coe_star, coe_star, star_star]
-- Lean 4 proof step from Mathlib.Algebra.Star.Unitary (goal)
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)
⊢ (↑(star (star x)) : R) = (↑x : R)
have a₂ : (↑x : R) = (↑x : R)
Tactic: rw [coe_star, coe_star, star_star]
-- Lean 4 proof step from Mathlib.Algebra.Star.Unitary (goal)
Goal:
R : Type u_1
inst : Monoid R
inst_1 : StarMul R
x y : ↥(unitary R)
⊢ star (x * y) = star y * star x
have a : (↑(star (x * y)) : R) = (↑(star y * star x) : R)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Star.Unitary (goal)
Goal:
R : Type u_1
inst : Monoid R
inst_1 : StarMul R
x y : ↥(unitary R)
⊢ (↑(star (x * y)) : R) = (↑(star y * star x) : R)
have a : 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]
-- Lean 4 proof step from Mathlib.Algebra.Star.Unitary (goal)
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)) : R) = (↑(star y * star x) : R)
have a₁ : star ((↑x : R) * (↑y : R)) = (↑(star y * star x) : R)
Tactic: rw [coe_star, Submonoid.coe_mul, Submonoid.coe_mul, coe_star, coe_star, star_mul]
-- Lean 4 proof step from Mathlib.Algebra.Star.Unitary (goal)
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)
⊢ (↑(star (x * y)) : R) = (↑(star y * star x) : R)
have a₂ : star ((↑x : R) * (↑y : R)) = (↑(star y) : R) * (↑(star x) : R)
Tactic: rw [coe_star, Submonoid.coe_mul, Submonoid.coe_mul, coe_star, coe_star, star_mul]
-- Lean 4 proof step from Mathlib.Algebra.Star.Unitary (goal)
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)
⊢ (↑(star (x * y)) : R) = (↑(star y * star x) : R)
have a₃ : star ((↑x : R) * (↑y : R)) = star (↑y : R) * (↑(star x) : R)
Tactic: rw [coe_star, Submonoid.coe_mul, Submonoid.coe_mul, coe_star, coe_star, star_mul]
-- Lean 4 proof step from Mathlib.Algebra.Star.Unitary (goal)
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)
⊢ (↑(star (x * y)) : R) = (↑(star y * star x) : R)
have a₄ : star ((↑x : R) * (↑y : R)) = star (↑y : R) * star (↑x : R)
Tactic: rw [coe_star, Submonoid.coe_mul, Submonoid.coe_mul, coe_star, coe_star, star_mul]