awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Star.UnitaryStarAlgAut
Goal:
R : Type u_3
S : Type u_4
inst : Ring R
inst_1 : StarMul R
inst_2 : CommRing S
inst_3 : StarMul S
inst_4 : Algebra S R
inst_5 : StarModule S R
inst_6 : Algebra.IsCentral S R
inst_7 : IsCancelMulZero S
inst_8 : Module.IsTorsionFree S R
u v : ↥(unitary R)
h_1 : ∃ (y : S), HSMul.hSMul (β := R) y 1 = star (↑v : R) * (↑u : R)
y : S
h : HSMul.hSMul (β := R) y 1 = star (↑v : R) * (↑u : R)
huv : (↑u : R) = y • (↑v : R)
hvu : (↑v : R) = star y • (↑u : R)
hvy : star y * y = 1 ∨ (↑v : R) = 0
inl : ∀ (this : star y * y = 1), ∃ (α : ↥(unitary S)), u = α • v
inr : ∀ (this : (↑v : R) = 0), ∃ (α : ↥(unitary S)), u = α • v
⊢ ∃ (α : ↥(unitary S)), u = α • v

Tactic:
obtain (this | this) := hvy
-- Module: Mathlib.Algebra.Star.UnitaryStarAlgAut
Goal:
R : Type u_3
S : Type u_4
inst : Ring R
inst_1 : StarMul R
inst_2 : CommRing S
inst_3 : StarMul S
inst_4 : Algebra S R
inst_5 : StarModule S R
inst_6 : Algebra.IsCentral S R
inst_7 : IsCancelMulZero S
inst_8 : Module.IsTorsionFree S R
u v : ↥(unitary R)
h_1 : ∃ (y : S), HSMul.hSMul (β := R) y 1 = star (↑v : R) * (↑u : R)
y : S
h : HSMul.hSMul (β := R) y 1 = star (↑v : R) * (↑u : R)
huv : (↑u : R) = y • (↑v : R)
hvu : (↑v : R) = star y • (↑u : R)
this : star y * y = 1
⊢ Membership.mem (γ := Submonoid S) (unitary S) y

Tactic:
simp [mem_iff, this, mul_comm y]

Premises used: mul_comm, Unitary.mem_iff
-- Module: Mathlib.Algebra.Star.UnitaryStarAlgAut
Goal:
R : Type u_3
S : Type u_4
inst : Ring R
inst_1 : StarMul R
inst_2 : CommRing S
inst_3 : StarMul S
inst_4 : Algebra S R
inst_5 : StarModule S R
inst_6 : Algebra.IsCentral S R
inst_7 : IsCancelMulZero S
inst_8 : Module.IsTorsionFree S R
u v : ↥(unitary R)
h_1 : ∃ (y : S), HSMul.hSMul (β := R) y 1 = star (↑v : R) * (↑u : R)
y : S
h : HSMul.hSMul (β := R) y 1 = star (↑v : R) * (↑u : R)
huv : (↑u : R) = y • (↑v : R)
hvu : (↑v : R) = star y • (↑u : R)
this : star y * y = 1
a : (↑u : R) = (↑(Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Submonoid S) (unitary S) x) y ⋯ • v) : R)
⊢ u = Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Submonoid S) (unitary S) x) y ⋯ • v

Tactic:
ext
-- Module: Mathlib.Algebra.Star.UnitaryStarAlgAut
Goal:
R : Type u_3
S : Type u_4
inst : Ring R
inst_1 : StarMul R
inst_2 : CommRing S
inst_3 : StarMul S
inst_4 : Algebra S R
inst_5 : StarModule S R
inst_6 : Algebra.IsCentral S R
inst_7 : IsCancelMulZero S
inst_8 : Module.IsTorsionFree S R
u v : ↥(unitary R)
h_1 : ∃ (y : S), HSMul.hSMul (β := R) y 1 = star (↑v : R) * (↑u : R)
y : S
h : HSMul.hSMul (β := R) y 1 = star (↑v : R) * (↑u : R)
huv : (↑u : R) = y • (↑v : R)
hvu : (↑v : R) = star y • (↑u : R)
this : star y * y = 1
⊢ (↑u : R) = (↑(Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Submonoid S) (unitary S) x) y ⋯ • v) : R)

Tactic:
huv
-- Module: Mathlib.Algebra.Star.UnitaryStarAlgAut
Goal:
R : Type u_3
S : Type u_4
inst : Ring R
inst_1 : StarMul R
inst_2 : CommRing S
inst_3 : StarMul S
inst_4 : Algebra S R
inst_5 : StarModule S R
inst_6 : Algebra.IsCentral S R
inst_7 : IsCancelMulZero S
inst_8 : Module.IsTorsionFree S R
u v : ↥(unitary R)
h_1 : ∃ (y : S), HSMul.hSMul (β := R) y 1 = star (↑v : R) * (↑u : R)
y : S
h : HSMul.hSMul (β := R) y 1 = star (↑v : R) * (↑u : R)
huv : (↑u : R) = y • (↑v : R)
hvu : (↑v : R) = star y • (↑u : R)
this : star y * y = 1
⊢ (↑u : R) = (↑(Subtype.mk (p := fun (x : S) ↦ Membership.mem (γ := Submonoid S) (unitary S) x) y ⋯ • v) : R)

Tactic:
exact huv
-- Module: Mathlib.Algebra.Star.UnitaryStarAlgAut
Goal:
R : Type u_3
S : Type u_4
inst : Ring R
inst_1 : StarMul R
inst_2 : CommRing S
inst_3 : StarMul S
inst_4 : Algebra S R
inst_5 : StarModule S R
inst_6 : Algebra.IsCentral S R
inst_7 : IsCancelMulZero S
inst_8 : Module.IsTorsionFree S R
u v : ↥(unitary R)
h_1 : ∃ (y : S), HSMul.hSMul (β := R) y 1 = star (↑v : R) * (↑u : R)
y : S
h : HSMul.hSMul (β := R) y 1 = star (↑v : R) * (↑u : R)
huv : (↑u : R) = y • (↑v : R)
hvu : (↑v : R) = star y • (↑u : R)
this : star y * y = 1
⊢ ∃ (α : ↥(unitary S)), u = α • v

Tactic:
exact ⟨⟨y, by simp [mem_iff, this, mul_comm y]⟩, by ext; exact huv⟩
-- Module: Mathlib.Algebra.Star.UnitaryStarAlgAut
Goal:
R : Type u_3
S : Type u_4
inst : Ring R
inst_1 : StarMul R
inst_2 : CommRing S
inst_3 : StarMul S
inst_4 : Algebra S R
inst_5 : StarModule S R
inst_6 : Algebra.IsCentral S R
inst_7 : IsCancelMulZero S
inst_8 : Module.IsTorsionFree S R
u v : ↥(unitary R)
h_1 : ∃ (y : S), HSMul.hSMul (β := R) y 1 = star (↑v : R) * (↑u : R)
y : S
h : HSMul.hSMul (β := R) y 1 = star (↑v : R) * (↑u : R)
huv : (↑u : R) = y • (↑v : R)
hvu : (↑v : R) = star y • (↑u : R)
this : (↑v : R) = 0
a : (↑u : R) = (↑(HSMul.hSMul.{u_4, u_3, u_3} (α := ↥(unitary S)) 1 v) : R)
⊢ u = HSMul.hSMul.{u_4, u_3, u_3} (α := ↥(unitary S)) 1 v

Tactic:
ext
-- Module: Mathlib.Algebra.Star.UnitaryStarAlgAut
Goal:
R : Type u_3
S : Type u_4
inst : Ring R
inst_1 : StarMul R
inst_2 : CommRing S
inst_3 : StarMul S
inst_4 : Algebra S R
inst_5 : StarModule S R
inst_6 : Algebra.IsCentral S R
inst_7 : IsCancelMulZero S
inst_8 : Module.IsTorsionFree S R
u v : ↥(unitary R)
h_1 : ∃ (y : S), HSMul.hSMul (β := R) y 1 = star (↑v : R) * (↑u : R)
y : S
h : HSMul.hSMul (β := R) y 1 = star (↑v : R) * (↑u : R)
huv : (↑u : R) = y • (↑v : R)
hvu : (↑v : R) = star y • (↑u : R)
this : (↑v : R) = 0
⊢ (↑u : R) = (↑(HSMul.hSMul.{u_4, u_3, u_3} (α := ↥(unitary S)) 1 v) : R)

Tactic:
simp [this, huv] at huv ⊢
-- Module: Mathlib.Algebra.Star.UnitaryStarAlgAut
Goal:
R : Type u_3
S : Type u_4
inst : Ring R
inst_1 : StarMul R
inst_2 : CommRing S
inst_3 : StarMul S
inst_4 : Algebra S R
inst_5 : StarModule S R
inst_6 : Algebra.IsCentral S R
inst_7 : IsCancelMulZero S
inst_8 : Module.IsTorsionFree S R
u v : ↥(unitary R)
h_1 : ∃ (y : S), HSMul.hSMul (β := R) y 1 = star (↑v : R) * (↑u : R)
y : S
h : HSMul.hSMul (β := R) y 1 = star (↑v : R) * (↑u : R)
huv : (↑u : R) = y • (↑v : R)
hvu : (↑v : R) = star y • (↑u : R)
this : (↑v : R) = 0
⊢ ∃ (α : ↥(unitary S)), u = α • v

Tactic:
exact ⟨1, by ext; simp [this, huv] at huv ⊢⟩
-- Module: Mathlib.Algebra.Symmetrized
Goal:
α : Type u_1
a : α
⊢ (unsym : (a : αˢʸᵐ) → α) ((sym : (a : α) → αˢʸᵐ) a : αˢʸᵐ) = a

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Symmetrized
Goal:
α : Type u_1
a : α
⊢ (sym : (a : α) → αˢʸᵐ) ((unsym : (a : αˢʸᵐ) → α) a : α) = a

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Symmetrized
Goal:
α : Type u_1
⊢ Eq.{u_1 + 1} (α := αˢʸᵐ → αˢʸᵐ) (comp (β := α) (⇑sym : (a : α) → αˢʸᵐ) (⇑unsym : (a : αˢʸᵐ) → α)) id

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Symmetrized
Goal:
α : Type u_1
⊢ Eq.{u_1 + 1} (α := α → α) (comp (β := αˢʸᵐ) (⇑unsym : (a : αˢʸᵐ) → α) (⇑sym : (a : α) → αˢʸᵐ)) id

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Symmetrized
Goal:
α : Type u_1
⊢ Eq.{u_1 + 1} (α := αˢʸᵐ ≃ α) (Equiv.symm sym) unsym

Tactic:
rfl

Premises used: SymAlg.unsym, Equiv.symm, Equiv.refl, rfl, SymAlg
-- Module: Mathlib.Algebra.Symmetrized
Goal:
α : Type u_1
⊢ Eq.{u_1 + 1} (α := α ≃ αˢʸᵐ) (Equiv.symm unsym) sym

Tactic:
rfl

Premises used: SymAlg.sym, Equiv.symm, Equiv.refl, rfl, SymAlg
-- Module: Mathlib.Algebra.Symmetrized
Goal:
α : Type u_1
⊢ Bijective.{u_1 + 1, u_1 + 1} (α := α) (β := αˢʸᵐ) (⇑sym : (a : α) → αˢʸᵐ)

Tactic:
sym.bijective

Premises used: Equiv.bijective, SymAlg.sym
-- Module: Mathlib.Algebra.Symmetrized
Goal:
α : Type u_1
⊢ Bijective.{u_1 + 1, u_1 + 1} (α := αˢʸᵐ) (β := α) (⇑unsym : (a : αˢʸᵐ) → α)

Tactic:
unsym.symm.bijective

Premises used: Equiv.bijective, SymAlg.unsym, Equiv.symm, SymAlg
-- Module: Mathlib.Algebra.Symmetrized
Goal:
α : Type u_1
⊢ Injective.{u_1 + 1, u_1 + 1} (α := α) (β := αˢʸᵐ) (⇑sym : (a : α) → αˢʸᵐ)

Tactic:
sym.injective

Premises used: SymAlg.sym, Equiv.injective
-- Module: Mathlib.Algebra.Symmetrized
Goal:
α : Type u_1
⊢ Surjective.{u_1 + 1, u_1 + 1} (α := α) (β := αˢʸᵐ) (⇑sym : (a : α) → αˢʸᵐ)

Tactic:
sym.surjective

Premises used: SymAlg.sym, Equiv.surjective
-- Module: Mathlib.Algebra.Symmetrized
Goal:
α : Type u_1
⊢ Injective.{u_1 + 1, u_1 + 1} (α := αˢʸᵐ) (β := α) (⇑unsym : (a : αˢʸᵐ) → α)

Tactic:
unsym.injective

Premises used: SymAlg.unsym, Equiv.injective
-- Module: Mathlib.Algebra.Symmetrized
Goal:
α : Type u_1
⊢ Surjective.{u_1 + 1, u_1 + 1} (α := αˢʸᵐ) (β := α) (⇑unsym : (a : αˢʸᵐ) → α)

Tactic:
unsym.surjective

Premises used: SymAlg.unsym, Equiv.surjective
-- Module: Mathlib.Algebra.Symmetrized
Goal:
α : Type u_1
a b : α
⊢ Eq (α := αˢʸᵐ) ((sym : (a : α) → αˢʸᵐ) a : αˢʸᵐ) ((sym : (a : α) → αˢʸᵐ) b : αˢʸᵐ) ↔ a = b

Tactic:
sym_injective.eq_iff

Premises used: Function.Injective.eq_iff, SymAlg.sym_injective
-- Module: Mathlib.Algebra.Symmetrized
Goal:
α : Type u_1
a b : αˢʸᵐ
⊢ Eq (α := α) ((unsym : (a : αˢʸᵐ) → α) a : α) ((unsym : (a : αˢʸᵐ) → α) b : α) ↔ a = b

Tactic:
unsym_injective.eq_iff

Premises used: Function.Injective.eq_iff, SymAlg.unsym_injective
-- Module: Mathlib.Algebra.Symmetrized
Goal:
α : Type u_1
inst : Nontrivial α
⊢ Nontrivial.{u_1} αˢʸᵐ

Tactic:
sym_injective.nontrivial

Premises used: Function.Injective.nontrivial, SymAlg.sym_injective
-- Module: Mathlib.Algebra.Symmetrized
Goal:
α : Type u_1
inst : Subsingleton α
⊢ Subsingleton.{u_1 + 1} αˢʸᵐ

Tactic:
unsym_injective.subsingleton

Premises used: Function.Injective.subsingleton, SymAlg.unsym_injective
-- Module: Mathlib.Algebra.Symmetrized
Goal:
α : Type u_1
inst : IsEmpty α
⊢ IsEmpty.{u_1 + 1} αˢʸᵐ

Tactic:
Function.isEmpty unsym

Premises used: Function.isEmpty, SymAlg.unsym, DFunLike.coe
-- Module: Mathlib.Algebra.Symmetrized
Goal:
α : Type u_1
inst : One α
⊢ Eq.{u_1 + 1} (α := αˢʸᵐ) ((sym : (a : α) → αˢʸᵐ) 1 : αˢʸᵐ) (1 : αˢʸᵐ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Symmetrized
Goal:
α : Type u_1
inst : One α
⊢ Eq.{u_1 + 1} (α := α) ((unsym : (a : αˢʸᵐ) → α) 1 : α) (1 : α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Symmetrized
Goal:
α : Type u_1
inst : Add α
a b : α
⊢ (sym : (a : α) → αˢʸᵐ) (a + b) =
    HAdd.hAdd (α := αˢʸᵐ) (β := αˢʸᵐ) ((sym : (a : α) → αˢʸᵐ) a : αˢʸᵐ) ((sym : (a : α) → αˢʸᵐ) b : αˢʸᵐ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Symmetrized
Goal:
α : Type u_1
inst : Add α
a b : αˢʸᵐ
⊢ (unsym : (a : αˢʸᵐ) → α) (a + b) =
    HAdd.hAdd (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) a : α) ((unsym : (a : αˢʸᵐ) → α) b : α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Symmetrized
Goal:
α : Type u_1
inst : Sub α
a b : α
⊢ (sym : (a : α) → αˢʸᵐ) (a - b) =
    HSub.hSub (α := αˢʸᵐ) (β := αˢʸᵐ) ((sym : (a : α) → αˢʸᵐ) a : αˢʸᵐ) ((sym : (a : α) → αˢʸᵐ) b : αˢʸᵐ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Symmetrized
Goal:
α : Type u_1
inst : Sub α
a b : αˢʸᵐ
⊢ (unsym : (a : αˢʸᵐ) → α) (a - b) =
    HSub.hSub (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) a : α) ((unsym : (a : αˢʸᵐ) → α) b : α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Symmetrized
Goal:
α : Type u_1
inst : Neg α
a : α
⊢ Eq (α := αˢʸᵐ) ((sym : (a : α) → αˢʸᵐ) (-a) : αˢʸᵐ) (-(sym : (a : α) → αˢʸᵐ) a : αˢʸᵐ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Symmetrized
Goal:
α : Type u_1
inst : Neg α
a : αˢʸᵐ
⊢ Eq (α := α) ((unsym : (a : αˢʸᵐ) → α) (-a) : α) (-(unsym : (a : αˢʸᵐ) → α) a : α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Symmetrized
Goal:
α : Type u_1
inst : Add α
inst_1 : Mul α
inst_2 : One α
inst_3 : OfNat α 2
inst_4 : Invertible (α := α) 2
a b : αˢʸᵐ
⊢ a * b =
    (sym : (a : α) → αˢʸᵐ)
      (@Invertible.invOf _ inst_1 inst_2 2 _ *
        (HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) a : α) ((unsym : (a : αˢʸᵐ) → α) b : α) +
          HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) b : α) ((unsym : (a : αˢʸᵐ) → α) a : α)))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Symmetrized
Goal:
α : Type u_1
inst : Mul α
inst_1 : Add α
inst_2 : One α
inst_3 : OfNat α 2
inst_4 : Invertible (α := α) 2
a b : αˢʸᵐ
⊢ (unsym : (a : αˢʸᵐ) → α) (a * b) =
    @Invertible.invOf _ inst inst_2 2 _ *
      (HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) a : α) ((unsym : (a : αˢʸᵐ) → α) b : α) +
        HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) b : α) ((unsym : (a : αˢʸᵐ) → α) a : α))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Symmetrized
Goal:
α : Type u_1
inst : Mul α
inst_1 : Add α
inst_2 : One α
inst_3 : OfNat α 2
inst_4 : Invertible (α := α) 2
a b : α
⊢ HMul.hMul (α := αˢʸᵐ) (β := αˢʸᵐ) ((sym : (a : α) → αˢʸᵐ) a : αˢʸᵐ) ((sym : (a : α) → αˢʸᵐ) b : αˢʸᵐ) =
    (sym : (a : α) → αˢʸᵐ) (@Invertible.invOf _ inst inst_2 2 _ * (a * b + b * a))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Symmetrized
Goal:
α : Type u_1
inst : Inv α
a : α
⊢ Eq (α := αˢʸᵐ) ((sym : (a : α) → αˢʸᵐ) a⁻¹ : αˢʸᵐ) (((sym : (a : α) → αˢʸᵐ) a)⁻¹ : αˢʸᵐ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Symmetrized
Goal:
α : Type u_1
inst : Inv α
a : αˢʸᵐ
⊢ Eq (α := α) ((unsym : (a : αˢʸᵐ) → α) a⁻¹ : α) (((unsym : (a : αˢʸᵐ) → α) a)⁻¹ : α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Symmetrized
Goal:
α : Type u_1
R : Type u_2
inst : SMul R α
c : R
a : α
⊢ (sym : (a : α) → αˢʸᵐ) (c • a) = HSMul.hSMul (β := αˢʸᵐ) c ((sym : (a : α) → αˢʸᵐ) a : αˢʸᵐ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Symmetrized
Goal:
α : Type u_1
R : Type u_2
inst : SMul R α
c : R
a : αˢʸᵐ
⊢ (unsym : (a : αˢʸᵐ) → α) (c • a) = HSMul.hSMul (β := α) c ((unsym : (a : αˢʸᵐ) → α) a : α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Symmetrized
Goal:
α : Type u_1
inst : One α
a : αˢʸᵐ
⊢ Eq (α := α) ((unsym : (a : αˢʸᵐ) → α) a : α) (1 : α) ↔ a = 1

Tactic:
unsym_injective.eq_iff' rfl

Premises used: Function.Injective.eq_iff', SymAlg.unsym_injective, rfl
-- Module: Mathlib.Algebra.Symmetrized
Goal:
α : Type u_1
inst : One α
a : α
⊢ Eq (α := αˢʸᵐ) ((sym : (a : α) → αˢʸᵐ) a : αˢʸᵐ) (1 : αˢʸᵐ) ↔ a = 1

Tactic:
sym_injective.eq_iff' rfl

Premises used: SymAlg.sym_injective, Function.Injective.eq_iff', rfl
-- Module: Mathlib.Algebra.Symmetrized
Goal:
α : Type u_1
inst : One α
a : αˢʸᵐ
⊢ Ne (α := α) ((unsym : (a : αˢʸᵐ) → α) a : α) (1 : α) ↔ a ≠ 1

Tactic:
not_congr <| unsym_eq_one_iff a

Premises used: SymAlg.unsym_eq_one_iff, not_congr
-- Module: Mathlib.Algebra.Symmetrized
Goal:
α : Type u_1
inst : One α
a : α
⊢ Ne (α := αˢʸᵐ) ((sym : (a : α) → αˢʸᵐ) a : αˢʸᵐ) (1 : αˢʸᵐ) ↔ a ≠ 1

Tactic:
not_congr <| sym_eq_one_iff a

Premises used: SymAlg.sym_eq_one_iff, not_congr
-- Module: Mathlib.Algebra.Symmetrized
Goal:
α : Type u_1
inst : Mul α
inst_1 : AddMonoidWithOne α
inst_2 : Invertible (α := α) 2
a : α
inst_3 : Invertible a
rw :
  Eq (α := αˢʸᵐ)
    ((sym : (a : α) → αˢʸᵐ)
        (@Invertible.invOf _ inst AddMonoidWithOne.toOne 2 _ *
          (@Invertible.invOf _ inst AddMonoidWithOne.toOne a _ * a +
            a * @Invertible.invOf _ inst AddMonoidWithOne.toOne a _)) :
      αˢʸᵐ)
    (1 : αˢʸᵐ)
rw₁ :
  Eq (α := αˢʸᵐ)
    ((sym : (a : α) → αˢʸᵐ)
        (@Invertible.invOf _ inst AddMonoidWithOne.toOne 2 _ *
          (@Invertible.invOf _ inst AddMonoidWithOne.toOne a _ * a + 1)) :
      αˢʸᵐ)
    (1 : αˢʸᵐ)
rw₂ :
  Eq (α := αˢʸᵐ)
    ((sym : (a : α) → αˢʸᵐ) (@Invertible.invOf _ inst AddMonoidWithOne.toOne 2 _ * HAdd.hAdd (α := α) 1 1) : αˢʸᵐ)
    (1 : αˢʸᵐ)
rw₃ :
  Eq (α := αˢʸᵐ)
    ((sym : (a : α) → αˢʸᵐ) (HMul.hMul (α := α) (@Invertible.invOf _ inst AddMonoidWithOne.toOne 2 _) 2) : αˢʸᵐ)
    (1 : αˢʸᵐ)
rw₄ : Eq.{u_1 + 1} (α := αˢʸᵐ) ((sym : (a : α) → αˢʸᵐ) 1 : αˢʸᵐ) (1 : αˢʸᵐ)
rw₅ rw₆ : Eq.{u_1 + 1} (α := αˢʸᵐ) 1 1
⊢ HMul.hMul (α := αˢʸᵐ) (β := αˢʸᵐ)
      ((sym : (a : α) → αˢʸᵐ) (@Invertible.invOf _ inst AddMonoidWithOne.toOne a _) : αˢʸᵐ)
      ((sym : (a : α) → αˢʸᵐ) a : αˢʸᵐ) =
    1

Tactic:
rw [sym_mul_sym, mul_invOf_self, invOf_mul_self, one_add_one_eq_two, invOf_mul_self, sym_one]

Premises used: invOf_mul_self, mul_invOf_self, one_add_one_eq_two, SymAlg.sym_one, SymAlg.sym_mul_sym
-- Module: Mathlib.Algebra.Symmetrized
Goal:
α : Type u_1
inst : Mul α
inst_1 : AddMonoidWithOne α
inst_2 : Invertible (α := α) 2
a : α
inst_3 : Invertible a
rw :
  Eq (α := αˢʸᵐ)
    ((sym : (a : α) → αˢʸᵐ)
        (@Invertible.invOf _ inst AddMonoidWithOne.toOne 2 _ *
          (a * @Invertible.invOf _ inst AddMonoidWithOne.toOne a _ +
            @Invertible.invOf _ inst AddMonoidWithOne.toOne a _ * a)) :
      αˢʸᵐ)
    (1 : αˢʸᵐ)
rw₁ :
  Eq (α := αˢʸᵐ)
    ((sym : (a : α) → αˢʸᵐ)
        (@Invertible.invOf _ inst AddMonoidWithOne.toOne 2 _ *
          (1 + @Invertible.invOf _ inst AddMonoidWithOne.toOne a _ * a)) :
      αˢʸᵐ)
    (1 : αˢʸᵐ)
rw₂ :
  Eq (α := αˢʸᵐ)
    ((sym : (a : α) → αˢʸᵐ) (@Invertible.invOf _ inst AddMonoidWithOne.toOne 2 _ * HAdd.hAdd (α := α) 1 1) : αˢʸᵐ)
    (1 : αˢʸᵐ)
rw₃ :
  Eq (α := αˢʸᵐ)
    ((sym : (a : α) → αˢʸᵐ) (HMul.hMul (α := α) (@Invertible.invOf _ inst AddMonoidWithOne.toOne 2 _) 2) : αˢʸᵐ)
    (1 : αˢʸᵐ)
rw₄ : Eq.{u_1 + 1} (α := αˢʸᵐ) ((sym : (a : α) → αˢʸᵐ) 1 : αˢʸᵐ) (1 : αˢʸᵐ)
rw₅ rw₆ : Eq.{u_1 + 1} (α := αˢʸᵐ) 1 1
⊢ HMul.hMul (α := αˢʸᵐ) (β := αˢʸᵐ) ((sym : (a : α) → αˢʸᵐ) a : αˢʸᵐ)
      ((sym : (a : α) → αˢʸᵐ) (@Invertible.invOf _ inst AddMonoidWithOne.toOne a _) : αˢʸᵐ) =
    1

Tactic:
rw [sym_mul_sym, mul_invOf_self, invOf_mul_self, one_add_one_eq_two, invOf_mul_self, sym_one]

Premises used: invOf_mul_self, mul_invOf_self, one_add_one_eq_two, SymAlg.sym_one, SymAlg.sym_mul_sym
-- Module: Mathlib.Algebra.Symmetrized
Goal:
α : Type u_1
inst : Mul α
inst_1 : AddMonoidWithOne α
inst_2 : Invertible (α := α) 2
a : α
inst_3 : Invertible a
⊢ Eq (α := αˢʸᵐ) (@Invertible.invOf _ instMulOfAddOfInvertibleOfNat instOne ((sym : (a : α) → αˢʸᵐ) a) _ : αˢʸᵐ)
    ((sym : (a : α) → αˢʸᵐ) (@Invertible.invOf _ inst AddMonoidWithOne.toOne a _) : αˢʸᵐ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Symmetrized
Goal:
α : Type u_1
inst : Semiring α
inst_1 : Invertible (α := α) 2
a b c : αˢʸᵐ
rw :
  Eq (α := αˢʸᵐ)
    ((sym : (a : α) → αˢʸᵐ)
        (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _ *
          (HMul.hMul (α := α) ((unsym : (a : αˢʸᵐ) → α) a : α)
              (HAdd.hAdd (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) b : α) ((unsym : (a : αˢʸᵐ) → α) c : α)) +
            (HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) b : α) ((unsym : (a : αˢʸᵐ) → α) a : α) +
              HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) c : α) ((unsym : (a : αˢʸᵐ) → α) a : α)))) :
      αˢʸᵐ)
    ((sym : (a : α) → αˢʸᵐ)
        (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _ *
          (HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) a : α) ((unsym : (a : αˢʸᵐ) → α) b : α) +
              HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) b : α) ((unsym : (a : αˢʸᵐ) → α) a : α) +
            (HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) a : α) ((unsym : (a : αˢʸᵐ) → α) c : α) +
              HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) c : α) ((unsym : (a : αˢʸᵐ) → α) a : α)))) :
      αˢʸᵐ)
⊢ a * (b + c) = a * b + a * c

Tactic:
rw [mul_def, mul_def, mul_def, ← sym_add, ← mul_add, unsym_add, add_mul]

Premises used: add_mul, SymAlg.unsym_add, SymAlg.sym_add, mul_add, SymAlg.mul_def
-- Module: Mathlib.Algebra.Symmetrized
Goal:
α : Type u_1
inst : Semiring α
inst_1 : Invertible (α := α) 2
a b c : αˢʸᵐ
h :
  HMul.hMul (α := α) ((unsym : (a : αˢʸᵐ) → α) a : α)
        (HAdd.hAdd (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) b : α) ((unsym : (a : αˢʸᵐ) → α) c : α)) +
      (HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) b : α) ((unsym : (a : αˢʸᵐ) → α) a : α) +
        HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) c : α) ((unsym : (a : αˢʸᵐ) → α) a : α)) =
    HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) a : α) ((unsym : (a : αˢʸᵐ) → α) b : α) +
        HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) b : α) ((unsym : (a : αˢʸᵐ) → α) a : α) +
      (HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) a : α) ((unsym : (a : αˢʸᵐ) → α) c : α) +
        HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) c : α) ((unsym : (a : αˢʸᵐ) → α) a : α))
⊢ Eq (α := αˢʸᵐ)
    ((sym : (a : α) → αˢʸᵐ)
        (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _ *
          (HMul.hMul (α := α) ((unsym : (a : αˢʸᵐ) → α) a : α)
              (HAdd.hAdd (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) b : α) ((unsym : (a : αˢʸᵐ) → α) c : α)) +
            (HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) b : α) ((unsym : (a : αˢʸᵐ) → α) a : α) +
              HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) c : α) ((unsym : (a : αˢʸᵐ) → α) a : α)))) :
      αˢʸᵐ)
    ((sym : (a : α) → αˢʸᵐ)
        (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _ *
          (HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) a : α) ((unsym : (a : αˢʸᵐ) → α) b : α) +
              HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) b : α) ((unsym : (a : αˢʸᵐ) → α) a : α) +
            (HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) a : α) ((unsym : (a : αˢʸᵐ) → α) c : α) +
              HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) c : α) ((unsym : (a : αˢʸᵐ) → α) a : α)))) :
      αˢʸᵐ)

Tactic:
congr 2
-- Module: Mathlib.Algebra.Symmetrized
Goal:
α : Type u_1
inst : Semiring α
inst_1 : Invertible (α := α) 2
a b c : αˢʸᵐ
h :
  HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) a : α) ((unsym : (a : αˢʸᵐ) → α) b : α) +
        HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) a : α) ((unsym : (a : αˢʸᵐ) → α) c : α) +
      (HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) b : α) ((unsym : (a : αˢʸᵐ) → α) a : α) +
        HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) c : α) ((unsym : (a : αˢʸᵐ) → α) a : α)) =
    HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) a : α) ((unsym : (a : αˢʸᵐ) → α) b : α) +
        HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) b : α) ((unsym : (a : αˢʸᵐ) → α) a : α) +
      (HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) a : α) ((unsym : (a : αˢʸᵐ) → α) c : α) +
        HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) c : α) ((unsym : (a : αˢʸᵐ) → α) a : α))
⊢ HMul.hMul (α := α) ((unsym : (a : αˢʸᵐ) → α) a : α)
        (HAdd.hAdd (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) b : α) ((unsym : (a : αˢʸᵐ) → α) c : α)) +
      (HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) b : α) ((unsym : (a : αˢʸᵐ) → α) a : α) +
        HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) c : α) ((unsym : (a : αˢʸᵐ) → α) a : α)) =
    HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) a : α) ((unsym : (a : αˢʸᵐ) → α) b : α) +
        HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) b : α) ((unsym : (a : αˢʸᵐ) → α) a : α) +
      (HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) a : α) ((unsym : (a : αˢʸᵐ) → α) c : α) +
        HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) c : α) ((unsym : (a : αˢʸᵐ) → α) a : α))

Tactic:
rw [mul_add]

Premises used: mul_add
-- Module: Mathlib.Algebra.Symmetrized
Goal:
α : Type u_1
inst : Semiring α
inst_1 : Invertible (α := α) 2
a b c : αˢʸᵐ
⊢ HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) a : α) ((unsym : (a : αˢʸᵐ) → α) b : α) +
        HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) a : α) ((unsym : (a : αˢʸᵐ) → α) c : α) +
      (HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) b : α) ((unsym : (a : αˢʸᵐ) → α) a : α) +
        HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) c : α) ((unsym : (a : αˢʸᵐ) → α) a : α)) =
    HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) a : α) ((unsym : (a : αˢʸᵐ) → α) b : α) +
        HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) b : α) ((unsym : (a : αˢʸᵐ) → α) a : α) +
      (HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) a : α) ((unsym : (a : αˢʸᵐ) → α) c : α) +
        HMul.hMul (α := α) (β := α) ((unsym : (a : αˢʸᵐ) → α) c : α) ((unsym : (a : αˢʸᵐ) → α) a : α))

Tactic:
abel