awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Star.CentroidHom (goal)
Goal:
α : Type u_1
inst : NonUnitalNonAssocSemiring α
inst_1 : StarRing α
z : ↥(NonUnitalStarSubsemiring.center α)
⊢ Eq (α := ↥(Subsemiring.center (CentroidHom α)))
    (star
        ((centerToCentroidCenter : (a : ↥(NonUnitalSubsemiring.center α)) → ↥(Subsemiring.center (CentroidHom α))) z) :
      ↥(Subsemiring.center (CentroidHom α)))
    ((centerToCentroidCenter : (a : ↥(NonUnitalSubsemiring.center α)) → ↥(Subsemiring.center (CentroidHom α)))
        (star z) :
      ↥(Subsemiring.center (CentroidHom α)))
have a : ∀ (a : α),
  Eq (α := α)
    (((↑(star
                ((centerToCentroidCenter :
                    (a : ↥(NonUnitalSubsemiring.center α)) → ↥(Subsemiring.center (CentroidHom α)))
                  z)) :
            CentroidHom α) :
          (a : α) → α)
        a :
      α)
    (((↑((centerToCentroidCenter : (a : ↥(NonUnitalSubsemiring.center α)) → ↥(Subsemiring.center (CentroidHom α)))
                (star z)) :
            CentroidHom α) :
          (a : α) → α)
        a :
      α)
Tactic: ext a
-- Lean 4 proof step from Mathlib.Algebra.Star.CentroidHom (goal)
Goal:
α : Type u_1
inst : NonUnitalNonAssocSemiring α
inst_1 : StarRing α
z : ↥(NonUnitalStarSubsemiring.center α)
a : α
⊢ star (star a) * (↑(star z) : α) = a * (↑(star z) : α)
have rw : a * (↑(star z) : α) = a * (↑(star z) : α)
Tactic: rw [star_star]
-- Lean 4 proof step from Mathlib.Algebra.Star.CentroidHom (goal)
Goal:
α : Type u_1
inst : NonUnitalNonAssocSemiring α
inst_1 : StarRing α
z : ↥(NonUnitalStarSubsemiring.center α)
a : α
⊢ a * (↑(star z) : α) = (↑(star z) : α) * a
have rw : a * (↑(star z) : α) = a * (↑(star z) : α)
Tactic: rw [(star z).property.comm]
-- Lean 4 proof step from Mathlib.Algebra.Star.CentroidHom (goal)
Goal:
α : Type u_1
inst : NonUnitalNonAssocSemiring α
inst_1 : StarRing α
z : ↥(NonUnitalStarSubsemiring.center α)
a : α
⊢ Eq (α := α)
    (((↑(star
                ((centerToCentroidCenter :
                    (a : ↥(NonUnitalSubsemiring.center α)) → ↥(Subsemiring.center (CentroidHom α)))
                  z)) :
            CentroidHom α) :
          (a : α) → α)
        a :
      α)
    (((↑((centerToCentroidCenter : (a : ↥(NonUnitalSubsemiring.center α)) → ↥(Subsemiring.center (CentroidHom α)))
                (star z)) :
            CentroidHom α) :
          (a : α) → α)
        a :
      α)
have a₁ : star ((↑z : α) * star a) = star (star a) * (↑(star z) : α)
Tactic: calc
      (star (centerToCentroidCenter z)) a = star (z * star a) := rfl
      _ = star (star a) * star z := by simp only [star_mul, star_star, StarMemClass.coe_star]
      _ = a * star z := by rw [star_star]
      _ = (star z) * a := by rw [(star z).property.comm]
      _ = (centerToCentroidCenter ((star z) : NonUnitalStarSubsemiring.center α)) a := rfl
-- Lean 4 proof step from Mathlib.Algebra.Star.CentroidHom (goal)
Goal:
α : Type u_1
inst : NonUnitalNonAssocSemiring α
inst_1 : StarRing α
z : ↥(NonUnitalStarSubsemiring.center α)
a : α
a₁ : star ((↑z : α) * star a) = star (star a) * (↑(star z) : α)
⊢ Eq (α := α)
    (((↑(star
                ((centerToCentroidCenter :
                    (a : ↥(NonUnitalSubsemiring.center α)) → ↥(Subsemiring.center (CentroidHom α)))
                  z)) :
            CentroidHom α) :
          (a : α) → α)
        a :
      α)
    (((↑((centerToCentroidCenter : (a : ↥(NonUnitalSubsemiring.center α)) → ↥(Subsemiring.center (CentroidHom α)))
                (star z)) :
            CentroidHom α) :
          (a : α) → α)
        a :
      α)
have a₂ : star (star a) * (↑(star z) : α) = a * (↑(star z) : α)
Tactic: calc
      (star (centerToCentroidCenter z)) a = star (z * star a) := rfl
      _ = star (star a) * star z := by simp only [star_mul, star_star, StarMemClass.coe_star]
      _ = a * star z := by rw [star_star]
      _ = (star z) * a := by rw [(star z).property.comm]
      _ = (centerToCentroidCenter ((star z) : NonUnitalStarSubsemiring.center α)) a := rfl
-- Lean 4 proof step from Mathlib.Algebra.Star.CentroidHom (goal)
Goal:
α : Type u_1
inst : NonUnitalNonAssocSemiring α
inst_1 : StarRing α
z : ↥(NonUnitalStarSubsemiring.center α)
a : α
a₁ : star ((↑z : α) * star a) = star (star a) * (↑(star z) : α)
a₂ : star (star a) * (↑(star z) : α) = a * (↑(star z) : α)
⊢ Eq (α := α)
    (((↑(star
                ((centerToCentroidCenter :
                    (a : ↥(NonUnitalSubsemiring.center α)) → ↥(Subsemiring.center (CentroidHom α)))
                  z)) :
            CentroidHom α) :
          (a : α) → α)
        a :
      α)
    (((↑((centerToCentroidCenter : (a : ↥(NonUnitalSubsemiring.center α)) → ↥(Subsemiring.center (CentroidHom α)))
                (star z)) :
            CentroidHom α) :
          (a : α) → α)
        a :
      α)
have a₃ : a * (↑(star z) : α) = (↑(star z) : α) * a
Tactic: calc
      (star (centerToCentroidCenter z)) a = star (z * star a) := rfl
      _ = star (star a) * star z := by simp only [star_mul, star_star, StarMemClass.coe_star]
      _ = a * star z := by rw [star_star]
      _ = (star z) * a := by rw [(star z).property.comm]
      _ = (centerToCentroidCenter ((star z) : NonUnitalStarSubsemiring.center α)) a := rfl
-- Lean 4 proof step from Mathlib.Algebra.Star.CentroidHom (goal)
Goal:
α : Type u_1
inst : NonAssocSemiring α
inst_1 : StarRing α
T : CentroidHom α
⊢ Membership.mem (α := α) (γ := StarSubsemiring α) (StarSubsemiring.center α) ((T : (a : α) → α) 1 : α)
have comm : ∀ (a : α), Commute ((T : (a : α) → α) 1) a
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Star.CentroidHom (goal)
Goal:
α : Type u_1
inst : NonAssocSemiring α
inst_1 : StarRing α
T : CentroidHom α
comm : ∀ (a : α), Commute ((T : (a : α) → α) 1) a
⊢ Membership.mem (α := α) (γ := StarSubsemiring α) (StarSubsemiring.center α) ((T : (a : α) → α) 1 : α)
have left_assoc : ∀ (b c : α), HMul.hMul (α := α) ((T : (a : α) → α) 1 : α) (b * c) = HMul.hMul (α := α) ((T : (a : α) → α) 1 : α) b * c
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Star.CentroidHom (goal)
Goal:
α : Type u_1
inst : NonAssocSemiring α
inst_1 : StarRing α
T : CentroidHom α
comm : ∀ (a : α), Commute ((T : (a : α) → α) 1) a
left_assoc :
  ∀ (b c : α), HMul.hMul (α := α) ((T : (a : α) → α) 1 : α) (b * c) = HMul.hMul (α := α) ((T : (a : α) → α) 1 : α) b * c
⊢ Membership.mem (α := α) (γ := StarSubsemiring α) (StarSubsemiring.center α) ((T : (a : α) → α) 1 : α)
have right_assoc : ∀ (a b : α), HMul.hMul (β := α) (a * b) ((T : (a : α) → α) 1 : α) = a * HMul.hMul (β := α) b ((T : (a : α) → α) 1 : α)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Star.Conjneg (goal)
Goal:
G : Type u_2
R : Type u_3
inst : AddGroup G
inst_1 : CommSemiring R
inst_2 : StarRing R
f : G → R
⊢ conjneg (conjneg f) = f
have h : ∀ (x : G), conjneg (conjneg f) x = f x
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Star.Conjneg (goal)
Goal:
G : Type u_2
R : Type u_3
inst : AddGroup G
inst_1 : CommSemiring R
inst_2 : StarRing R
⊢ Eq (α := G → R) (conjneg 0) 0
have h : ∀ (x : G), Eq.{u_3 + 1} (α := R) (conjneg 0 x) (0 x)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Star.Conjneg (goal)
Goal:
G : Type u_2
R : Type u_3
inst : AddGroup G
inst_1 : CommSemiring R
inst_2 : StarRing R
⊢ Eq (α := G → R) (conjneg 1) 1
have h : ∀ (x : G), Eq.{u_3 + 1} (α := R) (conjneg 1 x) (1 x)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Star.Conjneg (goal)
Goal:
G : Type u_2
R : Type u_3
inst : AddGroup G
inst_1 : CommSemiring R
inst_2 : StarRing R
f g : G → R
⊢ conjneg (f + g) = conjneg f + conjneg g
have h : ∀ (x : G), conjneg (f + g) x = (conjneg f + conjneg g) x
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Star.Conjneg (goal)
Goal:
G : Type u_2
R : Type u_3
inst : AddGroup G
inst_1 : CommSemiring R
inst_2 : StarRing R
f g : G → R
⊢ conjneg (f * g) = conjneg f * conjneg g
have h : ∀ (x : G), conjneg (f * g) x = (conjneg f * conjneg g) x
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Star.Conjneg (goal)
Goal:
ι : Type u_1
G : Type u_2
R : Type u_3
inst : AddGroup G
inst_1 : CommSemiring R
inst_2 : StarRing R
s : Finset ι
f : ι → G → R
⊢ Eq (α := G → R) (conjneg (∑ i ∈ s, f i)) (∑ i ∈ s, conjneg (f i))
have h : ∀ (x : G), Eq.{u_3 + 1} (α := R) (conjneg (∑ i ∈ s, f i) x) ((∑ i ∈ s, conjneg (f i)) x)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Star.Conjneg (goal)
Goal:
ι : Type u_1
G : Type u_2
R : Type u_3
inst : AddGroup G
inst_1 : CommSemiring R
inst_2 : StarRing R
s : Finset ι
f : ι → G → R
⊢ Eq (α := G → R) (conjneg (∏ i ∈ s, f i)) (∏ i ∈ s, conjneg (f i))
have h : ∀ (x : G), Eq.{u_3 + 1} (α := R) (conjneg (∏ i ∈ s, f i) x) ((∏ i ∈ s, conjneg (f i)) x)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Star.Conjneg (goal)
Goal:
G : Type u_2
R : Type u_3
inst : AddGroup G
inst_1 : CommSemiring R
inst_2 : StarRing R
f : G → R
⊢ conjneg f = 0 ↔ f = 0
have rw : conjneg (conjneg f) = conjneg 0 ↔ f = 0
Tactic: rw [← conjneg_inj, conjneg_conjneg, conjneg_zero]
-- Lean 4 proof step from Mathlib.Algebra.Star.Conjneg (goal)
Goal:
G : Type u_2
R : Type u_3
inst : AddGroup G
inst_1 : CommSemiring R
inst_2 : StarRing R
f : G → R
rw : conjneg (conjneg f) = conjneg 0 ↔ f = 0
⊢ conjneg f = 0 ↔ f = 0
have rw₁ : f = conjneg 0 ↔ f = 0
Tactic: rw [← conjneg_inj, conjneg_conjneg, conjneg_zero]
-- Lean 4 proof step from Mathlib.Algebra.Star.Conjneg (goal)
Goal:
G : Type u_2
R : Type u_3
inst : AddGroup G
inst_1 : CommSemiring R
inst_2 : StarRing R
f : G → R
rw : conjneg (conjneg f) = conjneg 0 ↔ f = 0
rw₁ : f = conjneg 0 ↔ f = 0
⊢ conjneg f = 0 ↔ f = 0
have rw₂ : f = 0 ↔ f = 0
Tactic: rw [← conjneg_inj, conjneg_conjneg, conjneg_zero]
-- Lean 4 proof step from Mathlib.Algebra.Star.Conjneg (goal)
Goal:
G : Type u_2
R : Type u_3
inst : AddGroup G
inst_1 : CommSemiring R
inst_2 : StarRing R
f : G → R
⊢ conjneg f = 1 ↔ f = 1
have rw : conjneg (conjneg f) = conjneg 1 ↔ f = 1
Tactic: rw [← conjneg_inj, conjneg_conjneg, conjneg_one]
-- Lean 4 proof step from Mathlib.Algebra.Star.Conjneg (goal)
Goal:
G : Type u_2
R : Type u_3
inst : AddGroup G
inst_1 : CommSemiring R
inst_2 : StarRing R
f : G → R
rw : conjneg (conjneg f) = conjneg 1 ↔ f = 1
⊢ conjneg f = 1 ↔ f = 1
have rw₁ : f = conjneg 1 ↔ f = 1
Tactic: rw [← conjneg_inj, conjneg_conjneg, conjneg_one]
-- Lean 4 proof step from Mathlib.Algebra.Star.Conjneg (goal)
Goal:
G : Type u_2
R : Type u_3
inst : AddGroup G
inst_1 : CommSemiring R
inst_2 : StarRing R
f : G → R
rw : conjneg (conjneg f) = conjneg 1 ↔ f = 1
rw₁ : f = conjneg 1 ↔ f = 1
⊢ conjneg f = 1 ↔ f = 1
have rw₂ : f = 1 ↔ f = 1
Tactic: rw [← conjneg_inj, conjneg_conjneg, conjneg_one]
-- Lean 4 proof step from Mathlib.Algebra.Star.Conjneg (goal)
Goal:
G : Type u_2
R : Type u_3
inst : AddGroup G
inst_1 : CommSemiring R
inst_2 : StarRing R
f : G → R
⊢ support (conjneg f) = -support f
have h : ∀ (x : G), x ∈ support (conjneg f) ↔ x ∈ -support f
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Star.Conjneg (goal)
Goal:
G : Type u_2
R : Type u_3
inst : AddGroup G
inst_1 : CommRing R
inst_2 : StarRing R
f g : G → R
⊢ conjneg (f - g) = conjneg f - conjneg g
have h : ∀ (x : G), conjneg (f - g) x = (conjneg f - conjneg g) x
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Star.Conjneg (goal)
Goal:
G : Type u_2
R : Type u_3
inst : AddGroup G
inst_1 : CommRing R
inst_2 : StarRing R
f : G → R
⊢ conjneg (-f) = -conjneg f
have h : ∀ (x : G), conjneg (-f) x = (-conjneg f) x
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Star.Free (goal)
Goal:
R : Type u_1
inst : CommSemiring R
X : Type u_2
x : FreeAlgebra R X
y : FreeAlgebra R X →ₐ[R] (FreeAlgebra R X)ᵐᵒᵖ :=
  (lift R : (a : X → (FreeAlgebra R X)ᵐᵒᵖ) → FreeAlgebra R X →ₐ[R] (FreeAlgebra R X)ᵐᵒᵖ) (MulOpposite.op ∘ ι R)
⊢ MulOpposite.unop
      ((((lift R : (a : X → (FreeAlgebra R X)ᵐᵒᵖ) → FreeAlgebra R X →ₐ[R] (FreeAlgebra R X)ᵐᵒᵖ) (MulOpposite.op ∘ ι R) :
            FreeAlgebra R X →ₐ[R] (FreeAlgebra R X)ᵐᵒᵖ) :
          (a : FreeAlgebra R X) → (FreeAlgebra R X)ᵐᵒᵖ)
        (MulOpposite.unop
          ((((lift R : (a : X → (FreeAlgebra R X)ᵐᵒᵖ) → FreeAlgebra R X →ₐ[R] (FreeAlgebra R X)ᵐᵒᵖ)
                  (MulOpposite.op ∘ ι R) :
                FreeAlgebra R X →ₐ[R] (FreeAlgebra R X)ᵐᵒᵖ) :
              (a : FreeAlgebra R X) → (FreeAlgebra R X)ᵐᵒᵖ)
            x))) =
    x
have refine_1 : ∀ (r : R),
  (fun (x : FreeAlgebra R X) ↦
      MulOpposite.unop
          ((y : (a : FreeAlgebra R X) → (FreeAlgebra R X)ᵐᵒᵖ)
            (MulOpposite.unop ((y : (a : FreeAlgebra R X) → (FreeAlgebra R X)ᵐᵒᵖ) x))) =
        x)
    ((algebraMap R (FreeAlgebra R X) : (a : R) → FreeAlgebra R X) r)
Tactic: refine induction (motive := fun x ↦ (y (y x).unop).unop = x) _ _ ?_ ?_ ?_ ?_ x
-- Lean 4 proof step from Mathlib.Algebra.Star.Free (goal)
Goal:
R : Type u_1
inst : CommSemiring R
X : Type u_2
x : FreeAlgebra R X
y : FreeAlgebra R X →ₐ[R] (FreeAlgebra R X)ᵐᵒᵖ :=
  (lift R : (a : X → (FreeAlgebra R X)ᵐᵒᵖ) → FreeAlgebra R X →ₐ[R] (FreeAlgebra R X)ᵐᵒᵖ) (MulOpposite.op ∘ ι R)
refine_1 :
  ∀ (r : R),
    (fun (x : FreeAlgebra R X) ↦
        MulOpposite.unop
            ((y : (a : FreeAlgebra R X) → (FreeAlgebra R X)ᵐᵒᵖ)
              (MulOpposite.unop ((y : (a : FreeAlgebra R X) → (FreeAlgebra R X)ᵐᵒᵖ) x))) =
          x)
      ((algebraMap R (FreeAlgebra R X) : (a : R) → FreeAlgebra R X) r)
⊢ MulOpposite.unop
      ((((lift R : (a : X → (FreeAlgebra R X)ᵐᵒᵖ) → FreeAlgebra R X →ₐ[R] (FreeAlgebra R X)ᵐᵒᵖ) (MulOpposite.op ∘ ι R) :
            FreeAlgebra R X →ₐ[R] (FreeAlgebra R X)ᵐᵒᵖ) :
          (a : FreeAlgebra R X) → (FreeAlgebra R X)ᵐᵒᵖ)
        (MulOpposite.unop
          ((((lift R : (a : X → (FreeAlgebra R X)ᵐᵒᵖ) → FreeAlgebra R X →ₐ[R] (FreeAlgebra R X)ᵐᵒᵖ)
                  (MulOpposite.op ∘ ι R) :
                FreeAlgebra R X →ₐ[R] (FreeAlgebra R X)ᵐᵒᵖ) :
              (a : FreeAlgebra R X) → (FreeAlgebra R X)ᵐᵒᵖ)
            x))) =
    x
have refine_2 : ∀ (x : X),
  (fun (x : FreeAlgebra R X) ↦
      MulOpposite.unop
          ((y : (a : FreeAlgebra R X) → (FreeAlgebra R X)ᵐᵒᵖ)
            (MulOpposite.unop ((y : (a : FreeAlgebra R X) → (FreeAlgebra R X)ᵐᵒᵖ) x))) =
        x)
    (ι R x)
Tactic: refine induction (motive := fun x ↦ (y (y x).unop).unop = x) _ _ ?_ ?_ ?_ ?_ x
-- Lean 4 proof step from Mathlib.Algebra.Star.Free (goal)
Goal:
R : Type u_1
inst : CommSemiring R
X : Type u_2
x : FreeAlgebra R X
y : FreeAlgebra R X →ₐ[R] (FreeAlgebra R X)ᵐᵒᵖ :=
  (lift R : (a : X → (FreeAlgebra R X)ᵐᵒᵖ) → FreeAlgebra R X →ₐ[R] (FreeAlgebra R X)ᵐᵒᵖ) (MulOpposite.op ∘ ι R)
refine_1 :
  ∀ (r : R),
    (fun (x : FreeAlgebra R X) ↦
        MulOpposite.unop
            ((y : (a : FreeAlgebra R X) → (FreeAlgebra R X)ᵐᵒᵖ)
              (MulOpposite.unop ((y : (a : FreeAlgebra R X) → (FreeAlgebra R X)ᵐᵒᵖ) x))) =
          x)
      ((algebraMap R (FreeAlgebra R X) : (a : R) → FreeAlgebra R X) r)
refine_2 :
  ∀ (x : X),
    (fun (x : FreeAlgebra R X) ↦
        MulOpposite.unop
            ((y : (a : FreeAlgebra R X) → (FreeAlgebra R X)ᵐᵒᵖ)
              (MulOpposite.unop ((y : (a : FreeAlgebra R X) → (FreeAlgebra R X)ᵐᵒᵖ) x))) =
          x)
      (ι R x)
⊢ MulOpposite.unop
      ((((lift R : (a : X → (FreeAlgebra R X)ᵐᵒᵖ) → FreeAlgebra R X →ₐ[R] (FreeAlgebra R X)ᵐᵒᵖ) (MulOpposite.op ∘ ι R) :
            FreeAlgebra R X →ₐ[R] (FreeAlgebra R X)ᵐᵒᵖ) :
          (a : FreeAlgebra R X) → (FreeAlgebra R X)ᵐᵒᵖ)
        (MulOpposite.unop
          ((((lift R : (a : X → (FreeAlgebra R X)ᵐᵒᵖ) → FreeAlgebra R X →ₐ[R] (FreeAlgebra R X)ᵐᵒᵖ)
                  (MulOpposite.op ∘ ι R) :
                FreeAlgebra R X →ₐ[R] (FreeAlgebra R X)ᵐᵒᵖ) :
              (a : FreeAlgebra R X) → (FreeAlgebra R X)ᵐᵒᵖ)
            x))) =
    x
have refine_3 : ∀ (a b : FreeAlgebra R X),
  (fun (x : FreeAlgebra R X) ↦
        MulOpposite.unop
            ((y : (a : FreeAlgebra R X) → (FreeAlgebra R X)ᵐᵒᵖ)
              (MulOpposite.unop ((y : (a : FreeAlgebra R X) → (FreeAlgebra R X)ᵐᵒᵖ) x))) =
          x)
      a →
    (fun (x : FreeAlgebra R X) ↦
          MulOpposite.unop
              ((y : (a : FreeAlgebra R X) → (FreeAlgebra R X)ᵐᵒᵖ)
                (MulOpposite.unop ((y : (a : FreeAlgebra R X) → (FreeAlgebra R X)ᵐᵒᵖ) x))) =
            x)
        b →
      (fun (x : FreeAlgebra R X) ↦
          MulOpposite.unop
              ((y : (a : FreeAlgebra R X) → (FreeAlgebra R X)ᵐᵒᵖ)
                (MulOpposite.unop ((y : (a : FreeAlgebra R X) → (FreeAlgebra R X)ᵐᵒᵖ) x))) =
            x)
        (a * b)
Tactic: refine induction (motive := fun x ↦ (y (y x).unop).unop = x) _ _ ?_ ?_ ?_ ?_ x
-- Lean 4 proof step from Mathlib.Algebra.Star.Free (goal)
Goal:
R : Type u_1
inst : CommSemiring R
X : Type u_2
x : FreeAlgebra R X
y : FreeAlgebra R X →ₐ[R] (FreeAlgebra R X)ᵐᵒᵖ :=
  (lift R : (a : X → (FreeAlgebra R X)ᵐᵒᵖ) → FreeAlgebra R X →ₐ[R] (FreeAlgebra R X)ᵐᵒᵖ) (MulOpposite.op ∘ ι R)
refine_1 :
  ∀ (r : R),
    (fun (x : FreeAlgebra R X) ↦
        MulOpposite.unop
            ((y : (a : FreeAlgebra R X) → (FreeAlgebra R X)ᵐᵒᵖ)
              (MulOpposite.unop ((y : (a : FreeAlgebra R X) → (FreeAlgebra R X)ᵐᵒᵖ) x))) =
          x)
      ((algebraMap R (FreeAlgebra R X) : (a : R) → FreeAlgebra R X) r)
refine_2 :
  ∀ (x : X),
    (fun (x : FreeAlgebra R X) ↦
        MulOpposite.unop
            ((y : (a : FreeAlgebra R X) → (FreeAlgebra R X)ᵐᵒᵖ)
              (MulOpposite.unop ((y : (a : FreeAlgebra R X) → (FreeAlgebra R X)ᵐᵒᵖ) x))) =
          x)
      (ι R x)
refine_3 :
  ∀ (a b : FreeAlgebra R X),
    (fun (x : FreeAlgebra R X) ↦
          MulOpposite.unop
              ((y : (a : FreeAlgebra R X) → (FreeAlgebra R X)ᵐᵒᵖ)
                (MulOpposite.unop ((y : (a : FreeAlgebra R X) → (FreeAlgebra R X)ᵐᵒᵖ) x))) =
            x)
        a →
      (fun (x : FreeAlgebra R X) ↦
            MulOpposite.unop
                ((y : (a : FreeAlgebra R X) → (FreeAlgebra R X)ᵐᵒᵖ)
                  (MulOpposite.unop ((y : (a : FreeAlgebra R X) → (FreeAlgebra R X)ᵐᵒᵖ) x))) =
              x)
          b →
        (fun (x : FreeAlgebra R X) ↦
            MulOpposite.unop
                ((y : (a : FreeAlgebra R X) → (FreeAlgebra R X)ᵐᵒᵖ)
                  (MulOpposite.unop ((y : (a : FreeAlgebra R X) → (FreeAlgebra R X)ᵐᵒᵖ) x))) =
              x)
          (a * b)
⊢ MulOpposite.unop
      ((((lift R : (a : X → (FreeAlgebra R X)ᵐᵒᵖ) → FreeAlgebra R X →ₐ[R] (FreeAlgebra R X)ᵐᵒᵖ) (MulOpposite.op ∘ ι R) :
            FreeAlgebra R X →ₐ[R] (FreeAlgebra R X)ᵐᵒᵖ) :
          (a : FreeAlgebra R X) → (FreeAlgebra R X)ᵐᵒᵖ)
        (MulOpposite.unop
          ((((lift R : (a : X → (FreeAlgebra R X)ᵐᵒᵖ) → FreeAlgebra R X →ₐ[R] (FreeAlgebra R X)ᵐᵒᵖ)
                  (MulOpposite.op ∘ ι R) :
                FreeAlgebra R X →ₐ[R] (FreeAlgebra R X)ᵐᵒᵖ) :
              (a : FreeAlgebra R X) → (FreeAlgebra R X)ᵐᵒᵖ)
            x))) =
    x
have refine_4 : ∀ (a b : FreeAlgebra R X),
  (fun (x : FreeAlgebra R X) ↦
        MulOpposite.unop
            ((y : (a : FreeAlgebra R X) → (FreeAlgebra R X)ᵐᵒᵖ)
              (MulOpposite.unop ((y : (a : FreeAlgebra R X) → (FreeAlgebra R X)ᵐᵒᵖ) x))) =
          x)
      a →
    (fun (x : FreeAlgebra R X) ↦
          MulOpposite.unop
              ((y : (a : FreeAlgebra R X) → (FreeAlgebra R X)ᵐᵒᵖ)
                (MulOpposite.unop ((y : (a : FreeAlgebra R X) → (FreeAlgebra R X)ᵐᵒᵖ) x))) =
            x)
        b →
      (fun (x : FreeAlgebra R X) ↦
          MulOpposite.unop
              ((y : (a : FreeAlgebra R X) → (FreeAlgebra R X)ᵐᵒᵖ)
                (MulOpposite.unop ((y : (a : FreeAlgebra R X) → (FreeAlgebra R X)ᵐᵒᵖ) x))) =
            x)
        (a + b)
Tactic: refine induction (motive := fun x ↦ (y (y x).unop).unop = x) _ _ ?_ ?_ ?_ ?_ x
-- Lean 4 proof step from Mathlib.Algebra.Star.LinearMap (goal)
Goal:
R : Type u_1
E : Type u_2
F : Type u_3
inst : Semiring R
inst_1 : InvolutiveStar R
inst_2 : AddCommMonoid E
inst_3 : Module R E
inst_4 : StarAddMonoid E
inst_5 : StarModule R E
inst_6 : AddCommMonoid F
inst_7 : Module R F
inst_8 : StarAddMonoid F
inst_9 : StarModule R F
x : WithConv (E →ₗ[R] F)
⊢ star (star x) = x
have h : ∀ (x_1 : E), Eq.{u_3 + 1} (α := F) (((star (star x)).ofConv : (a : E) → F) x_1 : F) ((x.ofConv : (a : E) → F) x_1 : F)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Star.LinearMap (goal)
Goal:
R : Type u_1
E : Type u_2
F : Type u_3
inst : Semiring R
inst_1 : InvolutiveStar R
inst_2 : AddCommMonoid E
inst_3 : Module R E
inst_4 : StarAddMonoid E
inst_5 : StarModule R E
inst_6 : AddCommMonoid F
inst_7 : Module R F
inst_8 : StarAddMonoid F
inst_9 : StarModule R F
x y : WithConv (E →ₗ[R] F)
⊢ star (x + y) = star x + star y
have h : ∀ (x_1 : E),
  Eq.{u_3 + 1} (α := F) (((star (x + y)).ofConv : (a : E) → F) x_1 : F)
    (((star x + star y).ofConv : (a : E) → F) x_1 : F)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Star.LinearMap (goal)
Goal:
R : Type u_1
E : Type u_2
F : Type u_3
inst : Semiring R
inst_1 : InvolutiveStar R
inst_2 : AddCommMonoid E
inst_3 : Module R E
inst_4 : StarAddMonoid E
inst_5 : StarModule R E
inst_6 : AddCommMonoid F
inst_7 : Module R F
inst_8 : StarAddMonoid F
inst_9 : StarModule R F
f : WithConv (E →ₗ[R] F)
⊢ IsSelfAdjoint f ↔
    ∀ (x : E), Eq.{u_3 + 1} (α := F) ((f.ofConv : (a : E) → F) (star x) : F) (star ((f.ofConv : (a : E) → F) x) : F)
have simp_rw : star f = f ↔
  ∀ (x : E), Eq.{u_3 + 1} (α := F) ((f.ofConv : (a : E) → F) (star x) : F) (star ((f.ofConv : (a : E) → F) x) : F)
Tactic: simp_rw [IsSelfAdjoint, WithConv.ext_iff, LinearMap.ext_iff, intrinsicStar_apply,
   star_eq_iff_star_eq, eq_comm]
-- Lean 4 proof step from Mathlib.Algebra.Star.LinearMap (goal)
Goal:
R : Type u_1
E : Type u_2
F : Type u_3
inst : Semiring R
inst_1 : InvolutiveStar R
inst_2 : AddCommMonoid E
inst_3 : Module R E
inst_4 : StarAddMonoid E
inst_5 : StarModule R E
inst_6 : AddCommMonoid F
inst_7 : Module R F
inst_8 : StarAddMonoid F
inst_9 : StarModule R F
f : WithConv (E →ₗ[R] F)
simp_rw :
  star f = f ↔
    ∀ (x : E), Eq.{u_3 + 1} (α := F) ((f.ofConv : (a : E) → F) (star x) : F) (star ((f.ofConv : (a : E) → F) x) : F)
⊢ IsSelfAdjoint f ↔
    ∀ (x : E), Eq.{u_3 + 1} (α := F) ((f.ofConv : (a : E) → F) (star x) : F) (star ((f.ofConv : (a : E) → F) x) : F)
have simp_rw₁ : (star f).ofConv = f.ofConv ↔
  ∀ (x : E), Eq.{u_3 + 1} (α := F) ((f.ofConv : (a : E) → F) (star x) : F) (star ((f.ofConv : (a : E) → F) x) : F)
Tactic: simp_rw [IsSelfAdjoint, WithConv.ext_iff, LinearMap.ext_iff, intrinsicStar_apply,
   star_eq_iff_star_eq, eq_comm]
-- Lean 4 proof step from Mathlib.Algebra.Star.LinearMap (goal)
Goal:
R : Type u_1
E : Type u_2
F : Type u_3
inst : Semiring R
inst_1 : InvolutiveStar R
inst_2 : AddCommMonoid E
inst_3 : Module R E
inst_4 : StarAddMonoid E
inst_5 : StarModule R E
inst_6 : AddCommMonoid F
inst_7 : Module R F
inst_8 : StarAddMonoid F
inst_9 : StarModule R F
f : WithConv (E →ₗ[R] F)
simp_rw :
  star f = f ↔
    ∀ (x : E), Eq.{u_3 + 1} (α := F) ((f.ofConv : (a : E) → F) (star x) : F) (star ((f.ofConv : (a : E) → F) x) : F)
simp_rw₁ :
  (star f).ofConv = f.ofConv ↔
    ∀ (x : E), Eq.{u_3 + 1} (α := F) ((f.ofConv : (a : E) → F) (star x) : F) (star ((f.ofConv : (a : E) → F) x) : F)
⊢ IsSelfAdjoint f ↔
    ∀ (x : E), Eq.{u_3 + 1} (α := F) ((f.ofConv : (a : E) → F) (star x) : F) (star ((f.ofConv : (a : E) → F) x) : F)
have simp_rw₂ : (∀ (x : E), Eq.{u_3 + 1} (α := F) (((star f).ofConv : (a : E) → F) x : F) ((f.ofConv : (a : E) → F) x : F)) ↔
  ∀ (x : E), Eq.{u_3 + 1} (α := F) ((f.ofConv : (a : E) → F) (star x) : F) (star ((f.ofConv : (a : E) → F) x) : F)
Tactic: simp_rw [IsSelfAdjoint, WithConv.ext_iff, LinearMap.ext_iff, intrinsicStar_apply,
   star_eq_iff_star_eq, eq_comm]