awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Star.Subalgebra
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
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 ⋯)
      { toSubalgebra := toSubalgebra, star_mem' := @star_mem' }
⊢ S.toNonUnitalStarSubalgebra.toStarSubalgebra ⋯ = S

Tactic:
cases S
-- Module: Mathlib.Algebra.Star.Subalgebra
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
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 ⋯)
    { toSubalgebra := toSubalgebra, star_mem' := @star_mem' }

Tactic:
rfl
-- Module: Mathlib.Algebra.Star.Subalgebra
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
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' }
⊢ StarSubalgebra.toNonUnitalStarSubalgebra (S.toStarSubalgebra h1) = S

Tactic:
cases S
-- Module: Mathlib.Algebra.Star.Subalgebra
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
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:
rfl
-- Module: Mathlib.Algebra.Star.Subalgebra
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 : Set A
⊢ LE.le (α := NonUnitalStarSubalgebra R A) (adjoin R s : NonUnitalStarSubalgebra R A)
    (StarSubalgebra.toNonUnitalStarSubalgebra (StarAlgebra.adjoin R s) : NonUnitalStarSubalgebra R A)

Tactic:
adjoin_le <| StarAlgebra.subset_adjoin R s

Premises used: NonUnitalStarAlgebra.adjoin_le, StarAlgebra.subset_adjoin
-- Module: Mathlib.Algebra.Star.Subalgebra
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 : Set A
⊢ Eq (α := StarSubalgebra R A) (adjoin R (↑(NonUnitalStarAlgebra.adjoin R s : NonUnitalStarSubalgebra R A) : Set A))
    (adjoin R s)

Tactic:
le_antisymm
    (adjoin_le <| NonUnitalStarAlgebra.adjoin_le_starAlgebra_adjoin R s)
    (adjoin_le <| (NonUnitalStarAlgebra.subset_adjoin R s).trans <| subset_adjoin R _)

Premises used: HasSubset.Subset.trans, NonUnitalStarAlgebra.subset_adjoin, StarAlgebra.subset_adjoin, le_antisymm, StarAlgebra.adjoin_le, NonUnitalStarAlgebra.adjoin_le_starAlgebra_adjoin
-- Module: Mathlib.Algebra.Star.Subalgebra
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
ι : Type u_3
inst_6 : Nonempty ι
S : ι → StarSubalgebra R A
dir : Directed (fun (x1 x2 : StarSubalgebra R A) ↦ x1 ≤ x2) S
⊢ (↑(iSup S) : Set A) = ⋃ (i : ι), (↑(S i) : Set A)

Tactic:
let K : StarSubalgebra R A :=
    { __ := NonUnitalStarSubalgebra.copy _ _ (NonUnitalStarSubalgebra.coe_iSup_of_directed
        (S := fun i ↦ (S i).toNonUnitalStarSubalgebra) dir).symm
      algebraMap_mem' x :=
        let ⟨i⟩ := ‹Nonempty ι›
        Set.mem_iUnion.mpr ⟨i, algebraMap_mem (S i) x⟩ }
  have : iSup S = K := le_antisymm (iSup_le fun i ↦ le_iSup (fun i ↦ (S i : Set A)) i)
    (Set.iUnion_subset fun _ ↦ le_iSup S _)
  this.symm ▸ rfl

Premises used: Iff.mpr, Set.iUnion_subset, Algebra.algebraMap, Subsemigroup.mk, iSup, Set.mem_iUnion, AddSubsemigroup.carrier, Membership.mem, RingHom.map_one, Eq.rec, le_iSup, StarSubalgebra.mk, AddSubmonoid.toAddSubsemigroup, AddSubsemigroup.add_mem', le_antisymm, NonUnitalSubsemiring.toAddSubmonoid, SetLike.coe, NonUnitalSubsemiring.mul_mem', _private.0.StarSubalgebra.coe_iSup_of_directed.match_1, NonUnitalSubalgebra.toNonUnitalSubsemiring, Subsemiring.mk, NonUnitalStarSubalgebra.coe_iSup_of_directed, AddSubmonoid.zero_mem', algebraMap_mem, StarSubalgebra.toNonUnitalStarSubalgebra, Exists.intro, NonUnitalStarSubalgebra.star_mem', iSup_le, NonUnitalStarSubalgebra.toNonUnitalSubalgebra, Submonoid.mk, OfNat.ofNat, Eq.symm, DFunLike.coe, Set.iUnion, rfl, Subalgebra.mk, NonUnitalStarSubalgebra.copy
-- Module: Mathlib.Algebra.Star.Subalgebra
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
ι : Type u_3
inst_6 : Nonempty ι
S : ι → StarSubalgebra R A
hS : ∀ (i : ι), IsMulCommutative.{u_2} ↥(S i)
dir : Directed (fun (x1 x2 : StarSubalgebra R A) ↦ x1 ≤ x2) S
⊢ IsMulCommutative.{u_2} ↥(⨆ (i : ι), S i)

Tactic:
simpa [isMulCommutative_iff, ← SetLike.mem_coe, coe_iSup_of_directed dir,
    Subalgebra.coe_iSup_of_directed dir] using Subalgebra.isMulCommutative_iSup dir

Premises used: Subalgebra.coe_iSup_of_directed, Subalgebra.isMulCommutative_iSup, StarSubalgebra.coe_iSup_of_directed, SetLike.mem_coe, isMulCommutative_iff
-- Module: Mathlib.Algebra.Star.Subalgebra
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
ι : Type u_3
inst_6 : Nonempty ι
inst_7 : Preorder ι
inst_8 : IsDirectedOrder ι
S : OrderHom.{u_3, u_2} ι (StarSubalgebra R A)
hS : ∀ (i : ι), IsMulCommutative.{u_2} ↥((S : (a : ι) → StarSubalgebra R A) i : StarSubalgebra R A)
⊢ IsMulCommutative.{u_2} ↥(⨆ (i : ι), (S : (a : ι) → StarSubalgebra R A) i)

Tactic:
isMulCommutative_iSup S.monotone.directed_le

Premises used: OrderHom.monotone, StarSubalgebra.isMulCommutative_iSup, Monotone.directed_le
-- Module: Mathlib.Algebra.Star.Subsemiring
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))
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
⊢ p = q

Tactic:
obtain ⟨⟨⟨⟨_, _⟩, _⟩, _⟩, _⟩ := p
-- Module: Mathlib.Algebra.Star.Subsemiring
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))
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 }
⊢ { 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:
cases q
-- Module: Mathlib.Algebra.Star.Subsemiring
Goal:
R : Type v
inst : NonAssocSemiring R
inst_1 : Star 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
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:
congr
-- Module: Mathlib.Algebra.Star.Subsemiring
Goal:
R : Type v
inst : NonAssocSemiring R
inst_1 : StarRing R
s : StarSubsemiring R
x : R
⊢ x ∈ s.carrier ↔ x ∈ s

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl
-- Module: Mathlib.Algebra.Star.Subsemiring
Goal:
R : Type v
inst : NonAssocSemiring R
inst_1 : StarRing R
S T : StarSubsemiring R
h : ∀ (x : R), x ∈ S ↔ x ∈ T
⊢ S = T

Tactic:
SetLike.ext h

Premises used: SetLike.ext
-- Module: Mathlib.Algebra.Star.Subsemiring
Goal:
R : Type v
inst : NonAssocSemiring R
inst_1 : StarRing R
S : Subsemiring R
h : ∀ {a : R}, a ∈ S.carrier → star a ∈ S.carrier
⊢ (↑{ toSubsemiring := S, star_mem' := @h : StarSubsemiring R } : Set R) = (↑S : Set R)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Star.Subsemiring
Goal:
R : Type v
inst : NonAssocSemiring R
inst_1 : StarRing R
S : StarSubsemiring R
x : R
⊢ x ∈ S.toSubsemiring ↔ x ∈ S

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl
-- Module: Mathlib.Algebra.Star.Subsemiring
Goal:
R : Type v
inst : NonAssocSemiring R
inst_1 : StarRing R
S : StarSubsemiring R
⊢ (↑S.toSubsemiring : Set R) = (↑S : Set R)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Star.Subsemiring
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
rw₂ rw₃ : x ∈ T.toSubsemiring ↔ x ∈ T.toSubsemiring
⊢ x ∈ S ↔ x ∈ T

Tactic:
rw [← mem_toSubsemiring, ← mem_toSubsemiring, h]

Premises used: StarSubsemiring.mem_toSubsemiring
-- Module: Mathlib.Algebra.Star.Subsemiring
Goal:
R : Type v
inst : NonAssocSemiring R
inst_1 : StarRing R
S U : StarSubsemiring R
⊢ S.toSubsemiring = U.toSubsemiring ↔ S = U

Tactic:
toSubsemiring_injective.eq_iff

Premises used: Function.Injective.eq_iff, StarSubsemiring.toSubsemiring_injective
-- Module: Mathlib.Algebra.Star.Subsemiring
Goal:
R : Type v
inst : NonAssocSemiring R
inst_1 : StarRing R
S₁ S₂ : StarSubsemiring R
⊢ S₁.toSubsemiring ≤ S₂.toSubsemiring ↔ S₁ ≤ S₂

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl
-- Module: Mathlib.Algebra.Star.Subsemiring
Goal:
R : Type v
inst : NonAssocSemiring R
inst_1 : StarRing R
S : StarSubsemiring R
s : Set R
hs : s = (↑S : Set R)
a : R
ha : a ∈ (S.copy s hs).carrier
⊢ a ∈ S.carrier

Tactic:
simpa [hs] using ha
-- Module: Mathlib.Algebra.Star.Subsemiring
Goal:
R : Type v
inst : NonAssocSemiring R
inst_1 : StarRing R
S : StarSubsemiring R
a : R
hs : (↑S : Set R) = (↑S : Set R)
__Subsemiring : Subsemiring R := S.copy (↑S : Set R) hs
ha : a ∈ (S.copy (↑S : Set R) hs).carrier
⊢ a ∈ S.carrier

Tactic:
simpa [hs] using ha
-- Module: Mathlib.Algebra.Star.Subsemiring
Goal:
R : Type v
inst : NonAssocSemiring R
inst_1 : StarRing R
S : StarSubsemiring R
s : Set R
hs : s = (↑S : Set R)
⊢ (↑(S.copy s hs) : Set R) = s

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Star.Subsemiring
Goal:
R : Type v
inst : NonAssocSemiring R
inst_1 : StarRing R
S : StarSubsemiring R
s : Set R
hs : s = (↑S : Set R)
⊢ S.copy s hs = S

Tactic:
SetLike.coe_injective hs

Premises used: SetLike.coe_injective
-- Module: Mathlib.Algebra.Star.TensorProduct
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
y : B
⊢ Eq (α := A ⊗[R] B) (star (x ⊗ₜ[R] y)) (star x ⊗ₜ[R] star y)

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, List.foldl, TensorProduct.tmul, AddCon.toQuotient, FreeAddMonoid.sumAux, rfl
-- Module: Mathlib.Algebra.Star.TensorProduct
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
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
⊢ (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

Tactic:
rw [congr_congr]

Premises used: TensorProduct.congr_congr
-- Module: Mathlib.Algebra.Star.TensorProduct
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] B) ((congr (LinearEquiv.refl R A) (LinearEquiv.refl R B) : (a : A ⊗[R] B) → A ⊗[R] B) x : A ⊗[R] B)
    ((LinearEquiv.refl R (A ⊗[R] B) : (a : A ⊗[R] B) → A ⊗[R] B) x : A ⊗[R] B)

Tactic:
congr($congr_refl_refl x)

Premises used: congrArg, TensorProduct.congr_refl_refl, id, DFunLike.coe
-- Module: Mathlib.Algebra.Star.TensorProduct
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)
h₁ :
  Eq (α := B ≃ₗ[R] B)
    (LinearEquiv.trans (σ₁₂ := starRingEnd R) (σ₂₃ := starRingEnd R) (starLinearEquiv R) (starLinearEquiv R))
    (LinearEquiv.refl 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

Tactic:
convert! congr($congr_refl_refl x)
-- Module: Mathlib.Algebra.Star.TensorProduct
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 :
  ∀ (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)
⊢ Eq (α := A ≃ₗ[R] A)
    (LinearEquiv.trans (σ₁₂ := starRingEnd R) (σ₂₃ := starRingEnd R) (starLinearEquiv R) (starLinearEquiv R))
    (LinearEquiv.refl R A)

Tactic:
ext
-- Module: Mathlib.Algebra.Star.TensorProduct
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 :
  ∀ (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)
⊢ Eq (α := B ≃ₗ[R] B)
    (LinearEquiv.trans (σ₁₂ := starRingEnd R) (σ₂₃ := starRingEnd R) (starLinearEquiv R) (starLinearEquiv R))
    (LinearEquiv.refl R B)

Tactic:
ext
-- Module: Mathlib.Algebra.Star.TensorProduct
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
x_1 : A
⊢ Eq (α := A)
    ((LinearEquiv.trans (σ₁₂ := starRingEnd R) (σ₂₃ := starRingEnd R) (starLinearEquiv R) (starLinearEquiv R) :
          (a : A) → A)
        x_1 :
      A)
    ((LinearEquiv.refl R A : (a : A) → A) x_1 : A)

Tactic:
simp
-- Module: Mathlib.Algebra.Star.TensorProduct
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
x_1 : B
⊢ Eq (α := B)
    ((LinearEquiv.trans (σ₁₂ := starRingEnd R) (σ₂₃ := starRingEnd R) (starLinearEquiv R) (starLinearEquiv R) :
          (a : B) → B)
        x_1 :
      B)
    ((LinearEquiv.refl R B : (a : B) → B) x_1 : B)

Tactic:
simp
-- Module: Mathlib.Algebra.Star.TensorProduct
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
⊢ Eq (α := A ⊗[R] B ≃ₗ⋆[R] A ⊗[R] B) (starLinearEquiv R) (congr (starLinearEquiv R) (starLinearEquiv R))

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, LinearEquiv.ofLinear, TensorProduct.congr, TensorProduct.map, TensorProduct, TensorProduct.lift, starLinearEquiv, rfl
-- 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
⊢ Membership.mem (γ := Set R) {U : R | star U * U = 1 ∧ U * star U = 1} (U * B)

Tactic:
⟨?_, ?_⟩

Premises used: Set.Mem, setOf, And.intro
-- 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
refine_1 : star (U * B) * (U * B) = 1
refine_2 : U * B * star (U * B) = 1
⊢ Membership.mem (γ := Set R) {U : R | star U * U = 1 ∧ U * star U = 1} (U * B)

Tactic:
refine ⟨?_, ?_⟩
-- 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
⊢ star (U * B) * (U * B) = star B * star U * U * B

Tactic:
simp only [mul_assoc, star_mul]

Premises used: mul_assoc, StarMul.star_mul