awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Star.Center
Goal:
R : Type u_1
inst : Mul R
inst_1 : StarMul R
a : R
s : Set R
ha : a ∈ (s ∪ star s).centralizer
⊢ star a ∈ (s ∪ star s).centralizer

Tactic:
Set.star_mem_centralizer'
    (fun _x hx => hx.elim (fun hx => Or.inr <| Set.star_mem_star.mpr hx) Or.inl) ha

Premises used: Iff.mpr, Set.star_mem_star, Set.star_mem_centralizer', Or.inl, Or.elim, Or.inr
-- Module: Mathlib.Algebra.Star.CentroidHom
Goal:
α : Type u_1
inst : NonUnitalNonAssocSemiring α
inst_1 : StarRing α
f : CentroidHom α
⊢ Eq (α := α) (star ((f : (a : α) → α) (star 0)) : α) (0 : α)

Tactic:
simp only [star_zero, map_zero]

Premises used: map_zero, star_zero
-- Module: Mathlib.Algebra.Star.CentroidHom
Goal:
α : Type u_1
inst : NonUnitalNonAssocSemiring α
inst_1 : StarRing α
f : CentroidHom α
a b : α
⊢ star ((f : (a : α) → α) (star (a + b))) =
    HAdd.hAdd (α := α) (β := α) (star ((f : (a : α) → α) (star a)) : α) (star ((f : (a : α) → α) (star b)) : α)

Tactic:
simp only [star_add, map_add]

Premises used: StarAddMonoid.star_add, map_add
-- Module: Mathlib.Algebra.Star.CentroidHom
Goal:
α : Type u_1
inst : NonUnitalNonAssocSemiring α
inst_1 : StarRing α
f : CentroidHom α
a b : α
⊢ star ((f : (a : α) → α) (star (a * b))) = HMul.hMul (β := α) a (star ((f : (a : α) → α) (star b)) : α)

Tactic:
simp only [star_mul, map_mul_right, star_star]

Premises used: star_star, StarMul.star_mul, CentroidHomClass.map_mul_right
-- Module: Mathlib.Algebra.Star.CentroidHom
Goal:
α : Type u_1
inst : NonUnitalNonAssocSemiring α
inst_1 : StarRing α
f : CentroidHom α
a b : α
⊢ star ((f : (a : α) → α) (star (a * b))) = HMul.hMul (α := α) (star ((f : (a : α) → α) (star a)) : α) b

Tactic:
simp only [star_mul, map_mul_left, star_star]

Premises used: star_star, CentroidHomClass.map_mul_left, StarMul.star_mul
-- Module: Mathlib.Algebra.Star.CentroidHom
Goal:
α : Type u_1
inst : NonUnitalNonAssocSemiring α
inst_1 : StarRing α
f : CentroidHom α
a : α
⊢ Eq (α := α) ((star f : (a : α) → α) a : α) (star ((f : (a : α) → α) (star a)) : α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Star.CentroidHom
Goal:
α : Type u_1
inst : NonUnitalNonAssocSemiring α
inst_1 : StarRing α
f : CentroidHom α
x : α
rw : Eq (α := α) (star ((star f : (a : α) → α) (star x)) : α) ((f : (a : α) → α) x : α)
rw₁ : Eq (α := α) (star (star ((f : (a : α) → α) (star (star x)))) : α) ((f : (a : α) → α) x : α)
rw₂ : Eq (α := α) ((f : (a : α) → α) (star (star x)) : α) ((f : (a : α) → α) x : α)
rw₃ rw₄ : Eq (α := α) ((f : (a : α) → α) x : α) ((f : (a : α) → α) x : α)
⊢ Eq (α := α) ((star (star f) : (a : α) → α) x : α) ((f : (a : α) → α) x : α)

Tactic:
rw [star_apply, star_apply, star_star, star_star]

Premises used: star_star, CentroidHom.star_apply
-- Module: Mathlib.Algebra.Star.CentroidHom
Goal:
α : Type u_1
inst : NonUnitalNonAssocSemiring α
inst_1 : StarRing α
f : ↥(Subsemiring.center (CentroidHom α))
g : CentroidHom α
a : α
rw :
  Eq (α := α) ((g : (a : α) → α) (star ((f : (a : α) → α) (star a)) : α) : α)
    (star (star ((g : (a : α) → α) (star ((f : (a : α) → α) (star a)) : α))) : α)
rw₁ rw₂ :
  Eq (α := α) ((g : (a : α) → α) (star ((f : (a : α) → α) (star a)) : α) : α)
    ((g : (a : α) → α) (star ((f : (a : α) → α) (star a)) : α) : α)
⊢ Eq (α := α) ((g : (a : α) → α) (star ((f : (a : α) → α) (star a)) : α) : α)
    (star ((star g : (a : α) → α) ((f : (a : α) → α) (star a) : α)) : α)

Tactic:
rw [star_apply, star_star]

Premises used: star_star, CentroidHom.star_apply
-- Module: Mathlib.Algebra.Star.CentroidHom
Goal:
α : Type u_1
inst : NonUnitalNonAssocSemiring α
inst_1 : StarRing α
f : ↥(Subsemiring.center (CentroidHom α))
g : CentroidHom α
a : α
rw rw₁ :
  Eq (α := α) (star ((star g * (↑f : CentroidHom α) : (a : α) → α) (star a)) : α)
    (star ((star g * (↑f : CentroidHom α) : (a : α) → α) (star a)) : α)
⊢ Eq (α := α) (star ((star g * (↑f : CentroidHom α) : (a : α) → α) (star a)) : α)
    (star (((↑f : CentroidHom α) * star g : (a : α) → α) (star a)) : α)

Tactic:
rw [f.property.comm]

Premises used: IsMulCentral.comm, Subtype.property
-- Module: Mathlib.Algebra.Star.CentroidHom
Goal:
α : Type u_1
inst : NonUnitalNonAssocSemiring α
inst_1 : StarRing α
f : ↥(Subsemiring.center (CentroidHom α))
g : CentroidHom α
a : α
rw :
  Eq (α := α) (star ((f : (a : α) → α) (star ((g : (a : α) → α) (star (star a))) : α)) : α)
    (star ((f : (a : α) → α) (star ((g : (a : α) → α) a) : α)) : α)
rw₁ rw₂ :
  Eq (α := α) (star ((f : (a : α) → α) (star ((g : (a : α) → α) a) : α)) : α)
    (star ((f : (a : α) → α) (star ((g : (a : α) → α) a) : α)) : α)
⊢ Eq (α := α) (star ((f : (a : α) → α) ((star g : (a : α) → α) (star a) : α)) : α)
    (star ((f : (a : α) → α) (star ((g : (a : α) → α) a) : α)) : α)

Tactic:
rw [star_apply, star_star]

Premises used: star_star, CentroidHom.star_apply
-- Module: Mathlib.Algebra.Star.CentroidHom
Goal:
α : Type u_1
inst : NonUnitalNonAssocSemiring α
inst_1 : StarRing α
f g : ↥(Subsemiring.center (CentroidHom α))
a :
  ∀ (a : α),
    Eq (α := α) (((↑(star (f * g)) : CentroidHom α) : (a : α) → α) a : α)
      (((↑(star g * star f) : CentroidHom α) : (a : α) → α) a : α)
⊢ star (f * g) = star g * star f

Tactic:
ext a
-- Module: Mathlib.Algebra.Star.CentroidHom
Goal:
α : Type u_1
inst : NonUnitalNonAssocSemiring α
inst_1 : StarRing α
f g : ↥(Subsemiring.center (CentroidHom α))
a : α
rw rw₁ : Eq (α := α) ((star (g * f) : (a : α) → α) a : α) ((star (g * f) : (a : α) → α) a : α)
⊢ Eq (α := α) ((star (f * g) : (a : α) → α) a : α) ((star (g * f) : (a : α) → α) a : α)

Tactic:
rw [CommMonoid.mul_comm f g]

Premises used: CommMonoid.mul_comm
-- Module: Mathlib.Algebra.Star.CentroidHom
Goal:
α : Type u_1
inst : NonUnitalNonAssocSemiring α
inst_1 : StarRing α
f g : ↥(Subsemiring.center (CentroidHom α))
a : α
⊢ Eq (α := α) ((star (g * f) : (a : α) → α) a : α) (star ((g : (a : α) → α) ((f : (a : α) → α) (star a) : α)) : α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Star.CentroidHom
Goal:
α : Type u_1
inst : NonUnitalNonAssocSemiring α
inst_1 : StarRing α
f g : ↥(Subsemiring.center (CentroidHom α))
a : α
⊢ Eq (α := α) (star ((g : (a : α) → α) ((f : (a : α) → α) (star a) : α)) : α)
    (star ((g : (a : α) → α) (star (star ((f : (a : α) → α) (star a))) : α)) : α)

Tactic:
simp only [star_star]

Premises used: star_star
-- Module: Mathlib.Algebra.Star.CentroidHom
Goal:
α : Type u_1
inst : NonUnitalNonAssocSemiring α
inst_1 : StarRing α
f g : ↥(Subsemiring.center (CentroidHom α))
a : α
⊢ Eq (α := α) (star ((g : (a : α) → α) (star (star ((f : (a : α) → α) (star a))) : α)) : α)
    ((star g * star f : (a : α) → α) a : α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Star.CentroidHom
Goal:
α : Type u_1
inst : NonUnitalNonAssocSemiring α
inst_1 : StarRing α
f g : ↥(Subsemiring.center (CentroidHom α))
a : α
star : Eq (α := α) ((Star.star (f * g) : (a : α) → α) a : α) ((Star.star (g * f) : (a : α) → α) a : α)
star₁ :
  Eq (α := α) (Star.star ((g : (a : α) → α) ((f : (a : α) → α) (Star.star a) : α)) : α)
    (Star.star ((g : (a : α) → α) (Star.star (Star.star ((f : (a : α) → α) (Star.star a))) : α)) : α)
⊢ Eq (α := α) (((↑(Star.star (f * g)) : CentroidHom α) : (a : α) → α) a : α)
    (((↑(Star.star g * Star.star f) : CentroidHom α) : (a : α) → α) a : α)

Tactic:
calc
      star (f * g) a = star (g * f) a := by rw [CommMonoid.mul_comm f g]
      _ = star (g (f (star a))) := rfl
      _ = star (g (star (star (f (star a))))) := by simp only [star_star]
      _ = (star g * star f) a := rfl

Premises used: HMul.hMul, DFunLike.coe, rfl, Star.star
-- Module: Mathlib.Algebra.Star.CentroidHom
Goal:
α : Type u_1
inst : NonUnitalNonAssocSemiring α
inst_1 : StarRing α
z : ↥(NonUnitalStarSubsemiring.center α)
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 :
        α)
⊢ 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 α)))

Tactic:
ext a
-- Module: Mathlib.Algebra.Star.CentroidHom
Goal:
α : Type u_1
inst : NonUnitalNonAssocSemiring α
inst_1 : StarRing α
z : ↥(NonUnitalStarSubsemiring.center α)
a : α
⊢ ((star ((centerToCentroidCenter : (a : ↥(NonUnitalSubsemiring.center α)) → ↥(Subsemiring.center (CentroidHom α))) z) :
          ↥(Subsemiring.center (CentroidHom α))) :
        (a : α) → α)
      a =
    star ((↑z : α) * star a)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Star.CentroidHom
Goal:
α : Type u_1
inst : NonUnitalNonAssocSemiring α
inst_1 : StarRing α
z : ↥(NonUnitalStarSubsemiring.center α)
a : α
⊢ star ((↑z : α) * star a) = star (star a) * (↑(star z) : α)

Tactic:
simp only [star_mul, star_star, StarMemClass.coe_star]

Premises used: star_star, StarMemClass.coe_star, StarMul.star_mul
-- Module: Mathlib.Algebra.Star.CentroidHom
Goal:
α : Type u_1
inst : NonUnitalNonAssocSemiring α
inst_1 : StarRing α
z : ↥(NonUnitalStarSubsemiring.center α)
a : α
rw rw₁ : a * (↑(star z) : α) = a * (↑(star z) : α)
⊢ star (star a) * (↑(star z) : α) = a * (↑(star z) : α)

Tactic:
rw [star_star]

Premises used: star_star
-- Module: Mathlib.Algebra.Star.CentroidHom
Goal:
α : Type u_1
inst : NonUnitalNonAssocSemiring α
inst_1 : StarRing α
z : ↥(NonUnitalStarSubsemiring.center α)
a : α
rw rw₁ : a * (↑(star z) : α) = a * (↑(star z) : α)
⊢ a * (↑(star z) : α) = (↑(star z) : α) * a

Tactic:
rw [(star z).property.comm]

Premises used: IsMulCentral.comm, Subtype.property, Star.star
-- Module: Mathlib.Algebra.Star.CentroidHom
Goal:
α : Type u_1
inst : NonUnitalNonAssocSemiring α
inst_1 : StarRing α
z : ↥(NonUnitalStarSubsemiring.center α)
a : α
⊢ (↑(star z) : α) * a =
    (((centerToCentroidCenter : (a : ↥(NonUnitalSubsemiring.center α)) → ↥(Subsemiring.center (CentroidHom α)))
            (star z) :
          ↥(Subsemiring.center (CentroidHom α))) :
        (a : α) → α)
      a

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Star.CentroidHom
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) : α)
a₃ : a * (↑(star z) : α) = (↑(star z) : α) * 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:
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

Premises used: HMul.hMul, CentroidHom.centerToCentroidCenter, Subtype.val, DFunLike.coe, rfl, Star.star
-- Module: Mathlib.Algebra.Star.CentroidHom
Goal:
α : Type u_1
inst : NonUnitalNonAssocSemiring α
inst_1 : StarRing α
z : ↥(NonUnitalStarSubsemiring.center α)
a : α
⊢ (((starCenterToCentroid : (a : ↥(NonUnitalStarSubsemiring.center α)) → CentroidHom α) z : CentroidHom α) :
        (a : α) → α)
      a =
    (↑z : α) * a

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Star.CentroidHom
Goal:
α : Type u_1
inst : NonUnitalNonAssocSemiring α
inst_1 : StarRing α
mul_comm : IsMulCommutative.{u_1} (CentroidHom α)
x x_1 : CentroidHom α
x_2 : α
⊢ Eq (α := α) ((star (x * x_1) : (a : α) → α) x_2 : α) ((star x_1 * star x : (a : α) → α) x_2 : α)

Tactic:
simp [mul_comm']

Premises used: mul_comm'
-- Module: Mathlib.Algebra.Star.CentroidHom
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
right_assoc :
  ∀ (a b : α), HMul.hMul (β := α) (a * b) ((T : (a : α) → α) 1 : α) = a * HMul.hMul (β := α) b ((T : (a : α) → α) 1 : α)
⊢ Membership.mem (α := α) (γ := StarSubsemiring α) (StarSubsemiring.center α) ((T : (a : α) → α) 1 : α)

Tactic:
constructor
-- Module: Mathlib.Algebra.Star.CentroidHom
Goal:
α : Type u_1
inst : NonAssocSemiring α
inst_1 : StarRing α
T : CentroidHom α
⊢ ∀ (a : α), Commute ((T : (a : α) → α) 1) a

Tactic:
simp [commute_iff_eq, ← map_mul_left, ← map_mul_right]

Premises used: commute_iff_eq, CentroidHomClass.map_mul_left, CentroidHomClass.map_mul_right
-- Module: Mathlib.Algebra.Star.CentroidHom
Goal:
α : Type u_1
inst : NonAssocSemiring α
inst_1 : StarRing α
T : CentroidHom α
⊢ ∀ (b c : α), HMul.hMul (α := α) ((T : (a : α) → α) 1 : α) (b * c) = HMul.hMul (α := α) ((T : (a : α) → α) 1 : α) b * c

Tactic:
simp [commute_iff_eq, ← map_mul_left, ← map_mul_right]

Premises used: commute_iff_eq, CentroidHomClass.map_mul_left, CentroidHomClass.map_mul_right
-- Module: Mathlib.Algebra.Star.CentroidHom
Goal:
α : Type u_1
inst : NonAssocSemiring α
inst_1 : StarRing α
T : CentroidHom α
⊢ ∀ (a b : α), HMul.hMul (β := α) (a * b) ((T : (a : α) → α) 1 : α) = a * HMul.hMul (β := α) b ((T : (a : α) → α) 1 : α)

Tactic:
simp [commute_iff_eq, ← map_mul_left, ← map_mul_right]

Premises used: commute_iff_eq, CentroidHomClass.map_mul_left, CentroidHomClass.map_mul_right
-- Module: Mathlib.Algebra.Star.CentroidHom
Goal:
α : Type u_1
inst : NonAssocSemiring α
inst_1 : StarRing α
z : ↥(StarSubsemiring.center α)
⊢ (↑((fun (T : CentroidHom α) ↦
            (Subtype.mk (p := fun (x : α) ↦ Membership.mem (γ := StarSubsemiring α) (StarSubsemiring.center α) x)
                ((T : (a : α) → α) 1) ⋯ :
              ↥(StarSubsemiring.center α)))
          (MulHom.toFun (NonUnitalRingHom.toMulHom (NonUnitalStarRingHom.toNonUnitalRingHom starCenterToCentroid)) z)) :
      α) =
    (↑z : α)

Tactic:
simp only [MulHom.toFun_eq_coe,
    NonUnitalRingHom.coe_toMulHom, NonUnitalStarRingHom.coe_toNonUnitalRingHom,
    starCenterToCentroid_apply, mul_one]

Premises used: MulHom.toFun_eq_coe, NonUnitalStarRingHom.coe_toNonUnitalRingHom, mul_one, CentroidHom.starCenterToCentroid_apply, NonUnitalRingHom.coe_toMulHom
-- Module: Mathlib.Algebra.Star.CentroidHom
Goal:
α : Type u_1
inst : NonAssocSemiring α
inst_1 : StarRing α
T : CentroidHom α
x : α
⊢ Eq (α := α)
    ((MulHom.toFun (M := ↥(NonUnitalStarSubsemiring.center α))
            (NonUnitalRingHom.toMulHom (NonUnitalStarRingHom.toNonUnitalRingHom starCenterToCentroid))
            ((fun (T : CentroidHom α) ↦
                (Subtype.mk (p := fun (x : α) ↦ Membership.mem (γ := StarSubsemiring α) (StarSubsemiring.center α) x)
                    ((T : (a : α) → α) 1) ⋯ :
                  ↥(StarSubsemiring.center α)))
              T) :
          (a : α) → α)
        x :
      α)
    ((T : (a : α) → α) x : α)

Tactic:
simp [starCenterToCentroid_apply, ← map_mul_right]

Premises used: CentroidHom.starCenterToCentroid_apply, CentroidHomClass.map_mul_right
-- Module: Mathlib.Algebra.Star.CentroidHom
Goal:
α : Type u_1
inst : NonAssocSemiring α
inst_1 : StarRing α
a : ↥(NonUnitalStarSubsemiring.center α)
⊢ Eq (α := CentroidHom α)
    ((starCenterIsoCentroid : (a : ↥(StarSubsemiring.center α)) → CentroidHom α) a : CentroidHom α)
    ((starCenterToCentroid : (a : ↥(NonUnitalStarSubsemiring.center α)) → CentroidHom α) a : CentroidHom α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Star.CentroidHom
Goal:
α : Type u_1
inst : NonAssocSemiring α
inst_1 : StarRing α
T : CentroidHom α
⊢ Eq (α := α)
    ((↑((StarRingEquiv.symm starCenterIsoCentroid : (a : CentroidHom α) → ↥(StarSubsemiring.center α)) T) : α) : α)
    ((T : (a : α) → α) 1 : α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Star.Conjneg
Goal:
G : Type u_2
R : Type u_3
inst : AddGroup G
inst_1 : CommSemiring R
inst_2 : StarRing R
f : G → R
x : G
⊢ conjneg f x = (starRingEnd R : (a : R) → R) (f (-x))

Tactic:
rfl

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

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

Tactic:
simp
-- Module: Mathlib.Algebra.Star.Conjneg
Goal:
G : Type u_2
R : Type u_3
inst : AddGroup G
inst_1 : CommSemiring R
inst_2 : StarRing R
⊢ Involutive (α := G → R) conjneg

Tactic:
conjneg_conjneg

Premises used: conjneg_conjneg, Function.Involutive
-- Module: Mathlib.Algebra.Star.Conjneg
Goal:
G : Type u_2
R : Type u_3
inst : AddGroup G
inst_1 : CommSemiring R
inst_2 : StarRing R
⊢ Bijective (α := G → R) conjneg

Tactic:
conjneg_involutive.bijective

Premises used: conjneg_involutive, Function.Involutive.bijective
-- Module: Mathlib.Algebra.Star.Conjneg
Goal:
G : Type u_2
R : Type u_3
inst : AddGroup G
inst_1 : CommSemiring R
inst_2 : StarRing R
⊢ Injective (α := G → R) conjneg

Tactic:
conjneg_involutive.injective

Premises used: Function.Involutive.injective, conjneg_involutive
-- Module: Mathlib.Algebra.Star.Conjneg
Goal:
G : Type u_2
R : Type u_3
inst : AddGroup G
inst_1 : CommSemiring R
inst_2 : StarRing R
⊢ Surjective (α := G → R) conjneg

Tactic:
conjneg_involutive.surjective

Premises used: Function.Involutive.surjective, conjneg_involutive
-- Module: Mathlib.Algebra.Star.Conjneg
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 = conjneg g ↔ f = g

Tactic:
conjneg_injective.eq_iff

Premises used: conjneg_injective, Function.Injective.eq_iff
-- Module: Mathlib.Algebra.Star.Conjneg
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 ≠ conjneg g ↔ f ≠ g

Tactic:
conjneg_injective.ne_iff

Premises used: conjneg_injective, Function.Injective.ne_iff
-- Module: Mathlib.Algebra.Star.Conjneg
Goal:
G : Type u_2
R : Type u_3
inst : AddGroup G
inst_1 : CommSemiring R
inst_2 : StarRing R
f : G → R
⊢ Eq (α := G → R) (conjneg ((starRingEnd (G → R) : (a : G → R) → G → R) f))
    ((starRingEnd (G → R) : (a : G → R) → G → R) (conjneg f))

Tactic:
rfl

Premises used: conjneg, rfl
-- Module: Mathlib.Algebra.Star.Conjneg
Goal:
G : Type u_2
R : Type u_3
inst : AddGroup G
inst_1 : CommSemiring R
inst_2 : StarRing R
h : ∀ (x : G), Eq.{u_3 + 1} (α := R) (conjneg 0 x) (0 x)
⊢ Eq (α := G → R) (conjneg 0) 0

Tactic:
ext
-- Module: Mathlib.Algebra.Star.Conjneg
Goal:
G : Type u_2
R : Type u_3
inst : AddGroup G
inst_1 : CommSemiring R
inst_2 : StarRing R
x : G
⊢ Eq.{u_3 + 1} (α := R) (conjneg 0 x) (0 x)

Tactic:
simp
-- Module: Mathlib.Algebra.Star.Conjneg
Goal:
G : Type u_2
R : Type u_3
inst : AddGroup G
inst_1 : CommSemiring R
inst_2 : StarRing R
h : ∀ (x : G), Eq.{u_3 + 1} (α := R) (conjneg 1 x) (1 x)
⊢ Eq (α := G → R) (conjneg 1) 1

Tactic:
ext
-- Module: Mathlib.Algebra.Star.Conjneg
Goal:
G : Type u_2
R : Type u_3
inst : AddGroup G
inst_1 : CommSemiring R
inst_2 : StarRing R
x : G
⊢ Eq.{u_3 + 1} (α := R) (conjneg 1 x) (1 x)

Tactic:
simp
-- Module: Mathlib.Algebra.Star.Conjneg
Goal:
G : Type u_2
R : Type u_3
inst : AddGroup G
inst_1 : CommSemiring 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 : CommSemiring 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 : CommSemiring 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 : CommSemiring 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:
ι : 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
h : ∀ (x : G), Eq.{u_3 + 1} (α := R) (conjneg (∑ i ∈ s, f i) x) ((∑ i ∈ s, conjneg (f i)) x)
⊢ Eq (α := G → R) (conjneg (∑ i ∈ s, f i)) (∑ i ∈ s, conjneg (f i))

Tactic:
ext
-- Module: Mathlib.Algebra.Star.Conjneg
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
x : G
⊢ Eq.{u_3 + 1} (α := R) (conjneg (∑ i ∈ s, f i) x) ((∑ i ∈ s, conjneg (f i)) x)

Tactic:
simp
-- Module: Mathlib.Algebra.Star.Conjneg
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
h : ∀ (x : G), Eq.{u_3 + 1} (α := R) (conjneg (∏ i ∈ s, f i) x) ((∏ i ∈ s, conjneg (f i)) x)
⊢ Eq (α := G → R) (conjneg (∏ i ∈ s, f i)) (∏ i ∈ s, conjneg (f i))

Tactic:
ext
-- Module: Mathlib.Algebra.Star.Conjneg
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
x : G
⊢ Eq.{u_3 + 1} (α := R) (conjneg (∏ i ∈ s, f i) x) ((∏ i ∈ s, conjneg (f i)) x)

Tactic:
simp
-- Module: Mathlib.Algebra.Star.Conjneg
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
rw₂ rw₃ : f = 0 ↔ f = 0
⊢ conjneg f = 0 ↔ f = 0

Tactic:
rw [← conjneg_inj, conjneg_conjneg, conjneg_zero]

Premises used: conjneg_zero, conjneg_conjneg, conjneg_inj
-- Module: Mathlib.Algebra.Star.Conjneg
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
rw₂ rw₃ : f = 1 ↔ f = 1
⊢ conjneg f = 1 ↔ f = 1

Tactic:
rw [← conjneg_inj, conjneg_conjneg, conjneg_one]

Premises used: conjneg_one, conjneg_conjneg, conjneg_inj
-- Module: Mathlib.Algebra.Star.Conjneg
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

Tactic:
conjneg_eq_zero.not

Premises used: Iff.not, conjneg_eq_zero
-- Module: Mathlib.Algebra.Star.Conjneg
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

Tactic:
conjneg_eq_one.not

Premises used: Iff.not, conjneg_eq_one
-- Module: Mathlib.Algebra.Star.Conjneg
Goal:
G : Type u_2
R : Type u_3
inst : AddGroup G
inst_1 : CommSemiring R
inst_2 : StarRing R
inst_3 : Fintype G
f : G → R
⊢ Eq.{u_3 + 1} (α := R) (∑ a : G, conjneg f a) (∑ a : G, (starRingEnd R : (a : R) → R) (f a))

Tactic:
Fintype.sum_equiv (Equiv.neg _) _ _ fun _ ↦ rfl

Premises used: Equiv.neg, Fintype.sum_equiv, rfl
-- Module: Mathlib.Algebra.Star.Conjneg
Goal:
G : Type u_2
R : Type u_3
inst : AddGroup G
inst_1 : CommSemiring R
inst_2 : StarRing R
f : G → R
h : ∀ (x : G), x ∈ support (conjneg f) ↔ x ∈ -support f
⊢ support (conjneg f) = -support f

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

Tactic:
simp [starRingEnd_apply]

Premises used: starRingEnd_apply