awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Star.Conjneg
Goal:
G : Type u_2
R : Type u_3
inst : AddGroup G
inst_1 : CommRing R
inst_2 : StarRing R
f g : G → R
h : ∀ (x : G), conjneg (f - g) x = (conjneg f - conjneg g) x
⊢ conjneg (f - g) = conjneg f - conjneg g

Tactic:
ext
-- Module: Mathlib.Algebra.Star.Conjneg
Goal:
G : Type u_2
R : Type u_3
inst : AddGroup G
inst_1 : CommRing R
inst_2 : StarRing R
f g : G → R
x : G
⊢ conjneg (f - g) x = (conjneg f - conjneg g) x

Tactic:
simp
-- Module: Mathlib.Algebra.Star.Conjneg
Goal:
G : Type u_2
R : Type u_3
inst : AddGroup G
inst_1 : CommRing R
inst_2 : StarRing R
f : G → R
h : ∀ (x : G), conjneg (-f) x = (-conjneg f) x
⊢ conjneg (-f) = -conjneg f

Tactic:
ext
-- Module: Mathlib.Algebra.Star.Conjneg
Goal:
G : Type u_2
R : Type u_3
inst : AddGroup G
inst_1 : CommRing R
inst_2 : StarRing R
f : G → R
x : G
⊢ conjneg (-f) x = (-conjneg f) x

Tactic:
simp
-- Module: Mathlib.Algebra.Star.Free
Goal:
α : Type u_1
x : α
⊢ star (of x) = of x

Tactic:
rfl

Premises used: List.reverseAux, FreeMonoid.of, List.reverse, rfl
-- Module: Mathlib.Algebra.Star.Free
Goal:
α : Type u_1
⊢ Eq.{u_1 + 1} (α := FreeMonoid α) (star 1) 1

Tactic:
rfl

Premises used: List.reverseAux, List.reverse, rfl
-- Module: Mathlib.Algebra.Star.Free
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

Tactic:
induction (motive := fun x ↦ (y (y x).unop).unop = x) _ _ ?_ ?_ ?_ ?_ x

Premises used: FreeAlgebra.induction
-- Module: Mathlib.Algebra.Star.Free
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)
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)
⊢ 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

Tactic:
refine induction (motive := fun x ↦ (y (y x).unop).unop = x) _ _ ?_ ?_ ?_ ?_ x

Premises used: FreeAlgebra.induction
-- Module: Mathlib.Algebra.Star.Free
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)
r : R
⊢ Eq (α := FreeAlgebra R X)
    (MulOpposite.unop
        ((y : (a : FreeAlgebra R X) → (FreeAlgebra R X)ᵐᵒᵖ)
          (MulOpposite.unop
            ((y : (a : FreeAlgebra R X) → (FreeAlgebra R X)ᵐᵒᵖ)
              ((algebraMap R (FreeAlgebra R X) : (a : R) → FreeAlgebra R X) r)))) :
      FreeAlgebra R X)
    ((algebraMap R (FreeAlgebra R X) : (a : R) → FreeAlgebra R X) r : FreeAlgebra R X)

Tactic:
simp only [AlgHom.commutes, MulOpposite.algebraMap_apply, MulOpposite.unop_op]

Premises used: MulOpposite.algebraMap_apply, MulOpposite.unop_op, AlgHom.commutes
-- Module: Mathlib.Algebra.Star.Free
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)
x_1 : X
⊢ Eq (α := FreeAlgebra R X)
    (MulOpposite.unop
      ((y : (a : FreeAlgebra R X) → (FreeAlgebra R X)ᵐᵒᵖ)
        (MulOpposite.unop ((y : (a : FreeAlgebra R X) → (FreeAlgebra R X)ᵐᵒᵖ) (ι R x_1)))))
    (ι R x_1)

Tactic:
simp only [y, lift_ι_apply, Function.comp_apply, MulOpposite.unop_op]

Premises used: FreeAlgebra.lift_ι_apply, MulOpposite.unop_op, Function.comp_apply
-- Module: Mathlib.Algebra.Star.Free
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)
a b : FreeAlgebra R X
h :
  MulOpposite.unop
      ((y : (a : FreeAlgebra R X) → (FreeAlgebra R X)ᵐᵒᵖ)
        (MulOpposite.unop ((y : (a : FreeAlgebra R X) → (FreeAlgebra R X)ᵐᵒᵖ) a))) =
    a
h_1 :
  MulOpposite.unop
      ((y : (a : FreeAlgebra R X) → (FreeAlgebra R X)ᵐᵒᵖ)
        (MulOpposite.unop ((y : (a : FreeAlgebra R X) → (FreeAlgebra R X)ᵐᵒᵖ) b))) =
    b
⊢ MulOpposite.unop
      ((y : (a : FreeAlgebra R X) → (FreeAlgebra R X)ᵐᵒᵖ)
        (MulOpposite.unop ((y : (a : FreeAlgebra R X) → (FreeAlgebra R X)ᵐᵒᵖ) (a * b)))) =
    a * b

Tactic:
simp only [*, map_mul, MulOpposite.unop_mul]

Premises used: MulOpposite.unop_mul, map_mul
-- Module: Mathlib.Algebra.Star.Free
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)
a b : FreeAlgebra R X
h :
  MulOpposite.unop
      ((y : (a : FreeAlgebra R X) → (FreeAlgebra R X)ᵐᵒᵖ)
        (MulOpposite.unop ((y : (a : FreeAlgebra R X) → (FreeAlgebra R X)ᵐᵒᵖ) a))) =
    a
h_1 :
  MulOpposite.unop
      ((y : (a : FreeAlgebra R X) → (FreeAlgebra R X)ᵐᵒᵖ)
        (MulOpposite.unop ((y : (a : FreeAlgebra R X) → (FreeAlgebra R X)ᵐᵒᵖ) b))) =
    b
⊢ MulOpposite.unop
      ((y : (a : FreeAlgebra R X) → (FreeAlgebra R X)ᵐᵒᵖ)
        (MulOpposite.unop ((y : (a : FreeAlgebra R X) → (FreeAlgebra R X)ᵐᵒᵖ) (a + b)))) =
    a + b

Tactic:
simp only [*, map_add, MulOpposite.unop_add]

Premises used: MulOpposite.unop_add, map_add
-- Module: Mathlib.Algebra.Star.Free
Goal:
R : Type u_1
inst : CommSemiring R
X : Type u_2
a b : 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)ᵐᵒᵖ))
      (a * b) =
    HMul.hMul (α := 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)ᵐᵒᵖ))
        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)ᵐᵒᵖ))
        a)

Tactic:
simp only [Function.comp_apply, map_mul, MulOpposite.unop_mul]

Premises used: MulOpposite.unop_mul, map_mul, Function.comp_apply
-- Module: Mathlib.Algebra.Star.Free
Goal:
R : Type u_1
inst : CommSemiring R
X : Type u_2
a b : 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)ᵐᵒᵖ))
      (a + b) =
    HAdd.hAdd (α := 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)ᵐᵒᵖ))
        a)
      ((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)ᵐᵒᵖ))
        b)

Tactic:
simp only [Function.comp_apply, map_add, MulOpposite.unop_add]

Premises used: MulOpposite.unop_add, map_add, Function.comp_apply
-- Module: Mathlib.Algebra.Star.Free
Goal:
R : Type u_1
inst : CommSemiring R
X : Type u_2
x : X
⊢ Eq (α := FreeAlgebra R X) (star (ι R x)) (ι R x)

Tactic:
simp [star, Star.star]

Premises used: Star.star
-- Module: Mathlib.Algebra.Star.Free
Goal:
R : Type u_1
inst : CommSemiring R
X : Type u_2
r : R
⊢ Eq (α := FreeAlgebra R X) (star ((algebraMap R (FreeAlgebra R X) : (a : R) → FreeAlgebra R X) r) : FreeAlgebra R X)
    ((algebraMap R (FreeAlgebra R X) : (a : R) → FreeAlgebra R X) r : FreeAlgebra R X)

Tactic:
simp [star, Star.star]

Premises used: Star.star
-- Module: Mathlib.Algebra.Star.Free
Goal:
R : Type u_1
inst : CommSemiring R
X : Type u_2
r : R
⊢ Eq (α := (FreeAlgebra R X)ᵐᵒᵖ)
    (Equiv.toFun (RingEquiv.toEquiv starRingEquiv) ((algebraMap R (FreeAlgebra R X) : (a : R) → FreeAlgebra R X) r) :
      (FreeAlgebra R X)ᵐᵒᵖ)
    ((algebraMap R (FreeAlgebra R X)ᵐᵒᵖ : (a : R) → (FreeAlgebra R X)ᵐᵒᵖ) r : (FreeAlgebra R X)ᵐᵒᵖ)

Tactic:
simp [star_algebraMap]

Premises used: FreeAlgebra.star_algebraMap
-- Module: Mathlib.Algebra.Star.LinearMap
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)
⊢ ∀ (x y : E),
    star ((f.ofConv : (a : E) → F) (star (x + y))) =
      HAdd.hAdd (α := F) (β := F) (star ((f.ofConv : (a : E) → F) (star x)) : F)
        (star ((f.ofConv : (a : E) → F) (star y)) : F)

Tactic:
simp
-- Module: Mathlib.Algebra.Star.LinearMap
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)
⊢ ∀ (m : R) (x : E),
    star ((f.ofConv : (a : E) → F) (star (m • x))) =
      HSMul.hSMul (α := R) (β := F) ((RingHom.id R : (a : R) → R) m : R) (star ((f.ofConv : (a : E) → F) (star x)) : F)

Tactic:
simp
-- Module: Mathlib.Algebra.Star.LinearMap
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)
x : E
⊢ Eq.{u_3 + 1} (α := F) (((star f).ofConv : (a : E) → F) x : F) (star ((f.ofConv : (a : E) → F) (star x)) : F)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Star.LinearMap
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)
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)
⊢ star (star x) = x

Tactic:
ext
-- Module: Mathlib.Algebra.Star.LinearMap
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)
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:
simp
-- Module: Mathlib.Algebra.Star.LinearMap
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)
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)
⊢ star (x + y) = star x + star y

Tactic:
ext
-- Module: Mathlib.Algebra.Star.LinearMap
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)
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:
simp
-- Module: Mathlib.Algebra.Star.LinearMap
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)
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)
simp_rw₃ :
  (∀ (x : E), Eq.{u_3 + 1} (α := F) (star ((f.ofConv : (a : E) → F) (star 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)
simp_rw₄ :
  (∀ (x : E), Eq.{u_3 + 1} (α := F) (star ((f.ofConv : (a : E) → F) x) : F) ((f.ofConv : (a : E) → F) (star 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)
⊢ 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)

Tactic:
simp_rw [IsSelfAdjoint, WithConv.ext_iff, LinearMap.ext_iff, intrinsicStar_apply,
   star_eq_iff_star_eq, eq_comm]

Premises used: IsSelfAdjoint, LinearMap.ext_iff, eq_comm, star_eq_iff_star_eq, LinearMap.intrinsicStar_apply, WithConv.ext_iff
-- Module: Mathlib.Algebra.Star.LinearMap
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
S : Type u_4
inst_10 : FunLike S E F
inst_11 : LinearMapClass S R E F
inst_12 : StarHomClass S E F
f : S
⊢ IsSelfAdjoint (R := WithConv (E →ₗ[R] F))
    (toConv (↑f : [inst_13 : FunLike S E F] → [SemilinearMapClass S (RingHom.id R) E F] → E →ₗ[R] F))

Tactic:
IntrinsicStar.isSelfAdjoint_iff_map_star _ |>.mpr (map_star f)

Premises used: Iff.mpr, StarHomClass.map_star, LinearMap.IntrinsicStar.isSelfAdjoint_iff_map_star
-- Module: Mathlib.Algebra.Star.LinearMap
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
G : Type u_4
inst_10 : AddCommMonoid G
inst_11 : Module R G
inst_12 : StarAddMonoid G
inst_13 : StarModule R G
f : WithConv (E →ₗ[R] F)
g : WithConv (G →ₗ[R] E)
h :
  ∀ (x : G),
    Eq.{u_3 + 1} (α := F) (((star (toConv (f.ofConv ∘ₗ g.ofConv))).ofConv : (a : G) → F) x : F)
      (((toConv ((star f).ofConv ∘ₗ (star g).ofConv)).ofConv : (a : G) → F) x : F)
⊢ star (toConv (f.ofConv ∘ₗ g.ofConv)) = toConv ((star f).ofConv ∘ₗ (star g).ofConv)

Tactic:
ext
-- Module: Mathlib.Algebra.Star.LinearMap
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
G : Type u_4
inst_10 : AddCommMonoid G
inst_11 : Module R G
inst_12 : StarAddMonoid G
inst_13 : StarModule R G
f : WithConv (E →ₗ[R] F)
g : WithConv (G →ₗ[R] E)
x : G
⊢ Eq.{u_3 + 1} (α := F) (((star (toConv (f.ofConv ∘ₗ g.ofConv))).ofConv : (a : G) → F) x : F)
    (((toConv ((star f).ofConv ∘ₗ (star g).ofConv)).ofConv : (a : G) → F) x : F)

Tactic:
simp
-- Module: Mathlib.Algebra.Star.LinearMap
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
G : Type u_4
inst_10 : AddCommMonoid G
inst_11 : Module R G
inst_12 : StarAddMonoid G
inst_13 : StarModule R G
f : E →ₗ[R] F
g : G →ₗ[R] E
⊢ star (toConv (f ∘ₗ g)) = toConv ((star (toConv f)).ofConv ∘ₗ (star (toConv g)).ofConv)

Tactic:
simpa using intrinsicStar_comp _ _

Premises used: LinearMap.intrinsicStar_comp
-- Module: Mathlib.Algebra.Star.LinearMap
Goal:
R : Type u_1
E : Type u_2
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
h : ∀ (x : E), Eq (α := E) ((ofConv (star (toConv id)) : (a : E) → E) x : E) ((ofConv (toConv id) : (a : E) → E) x : E)
⊢ Eq.{u_2 + 1} (α := WithConv (E →ₗ[R] E)) (star (toConv id)) (toConv id)

Tactic:
ext
-- Module: Mathlib.Algebra.Star.LinearMap
Goal:
R : Type u_1
E : Type u_2
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
x : E
⊢ Eq (α := E) ((ofConv (star (toConv id)) : (a : E) → E) x : E) ((ofConv (toConv id) : (a : E) → E) x : E)

Tactic:
simp
-- Module: Mathlib.Algebra.Star.LinearMap
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
⊢ Eq (α := WithConv (E →ₗ[R] F)) (star 0) 0

Tactic:
simp
-- Module: Mathlib.Algebra.Star.LinearMap
Goal:
R : Type u_1
inst : Semiring R
inst_1 : InvolutiveStar R
E : Type u_6
inst_2 : NonUnitalNonAssocSemiring E
inst_3 : StarRing E
inst_4 : Module R E
inst_5 : StarModule R E
inst_6 : SMulCommClass R E E
inst_7 : IsScalarTower R E E
x : E
h :
  ∀ (x_1 : E),
    Eq (α := E) ((ofConv (star (toConv (mulLeft R x))) : (a : E) → E) x_1 : E)
      ((ofConv (toConv (mulRight R (star x))) : (a : E) → E) x_1 : E)
⊢ Eq (α := WithConv (E →ₗ[R] E)) (star (toConv (mulLeft R x))) (toConv (mulRight R (star x)))

Tactic:
ext
-- Module: Mathlib.Algebra.Star.LinearMap
Goal:
R : Type u_1
inst : Semiring R
inst_1 : InvolutiveStar R
E : Type u_6
inst_2 : NonUnitalNonAssocSemiring E
inst_3 : StarRing E
inst_4 : Module R E
inst_5 : StarModule R E
inst_6 : SMulCommClass R E E
inst_7 : IsScalarTower R E E
x x_1 : E
⊢ Eq (α := E) ((ofConv (star (toConv (mulLeft R x))) : (a : E) → E) x_1 : E)
    ((ofConv (toConv (mulRight R (star x))) : (a : E) → E) x_1 : E)

Tactic:
simp
-- Module: Mathlib.Algebra.Star.LinearMap
Goal:
R : Type u_1
inst : Semiring R
inst_1 : InvolutiveStar R
E : Type u_6
inst_2 : NonUnitalNonAssocSemiring E
inst_3 : StarRing E
inst_4 : Module R E
inst_5 : StarModule R E
inst_6 : SMulCommClass R E E
inst_7 : IsScalarTower R E E
x : E
rw : Eq (α := WithConv (E →ₗ[R] E)) (star (toConv (mulLeft R (star x)))) (toConv (mulRight R x))
rw₁ : Eq (α := WithConv (E →ₗ[R] E)) (toConv (mulRight R (star (star x)))) (toConv (mulRight R x))
rw₂ rw₃ : Eq (α := WithConv (E →ₗ[R] E)) (toConv (mulRight R x)) (toConv (mulRight R x))
⊢ Eq (α := WithConv (E →ₗ[R] E)) (star (toConv (mulRight R x))) (toConv (mulLeft R (star x)))

Tactic:
rw [star_eq_iff_star_eq, intrinsicStar_mulLeft, star_star]

Premises used: star_star, star_eq_iff_star_eq, LinearMap.intrinsicStar_mulLeft
-- Module: Mathlib.Algebra.Star.LinearMap
Goal:
R' : Type u_5
E : Type u_6
inst : CommSemiring R'
inst_1 : StarRing R'
inst_2 : NonUnitalNonAssocSemiring E
inst_3 : StarRing E
inst_4 : Module R' E
inst_5 : StarModule R' E
inst_6 : SMulCommClass R' E E
inst_7 : IsScalarTower R' E E
x x_1 : E
⊢ Eq (α := E) ((ofConv (star (toConv (mul' R' E))) : (a : TensorProduct R' E E) → E) (x ⊗ₜ[R'] x_1) : E)
    ((ofConv (toConv (mul' R' E ∘ₗ (↑(TensorProduct.comm R' E E) : TensorProduct R' E E →ₗ[R'] TensorProduct R' E E))) :
          (a : TensorProduct R' E E) → E)
        (x ⊗ₜ[R'] x_1) :
      E)

Tactic:
simp