awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Squarefree.Basic
Goal:
R : Type u_1
inst : CommMonoidWithZero R
inst_1 : UniqueFactorizationMonoid R
inst_2 : NormalizationMonoid R
x : R
x0 : x ≠ 0
this : Nontrivial R
h : ∀ (a : R), Multiset.count a (normalizedFactors x) ≤ 1
hu : ¬IsUnit.{u_1} (M := R) 0
⊢ emultiplicity 0 x ≤ 1

Tactic:
simp [x0]
-- Module: Mathlib.Algebra.Squarefree.Basic
Goal:
R : Type u_1
inst : CommMonoidWithZero R
inst_1 : UniqueFactorizationMonoid R
inst_2 : NormalizationMonoid R
x : R
x0 : x ≠ 0
this : Nontrivial R
h : ∀ (a : R), Multiset.count a (normalizedFactors x) ≤ 1
a : R
hu : ¬IsUnit a
h0 : a ≠ 0
mpr : ∀ (b : R) (hib : Irreducible b) (hdvd : b ∣ a), emultiplicity a x ≤ 1
⊢ emultiplicity a x ≤ 1

Tactic:
rcases WfDvdMonoid.exists_irreducible_factor hu h0 with ⟨b, hib, hdvd⟩

Premises used: WfDvdMonoid.exists_irreducible_factor
-- Module: Mathlib.Algebra.Squarefree.Basic
Goal:
R : Type u_1
inst : CommMonoidWithZero R
inst_1 : UniqueFactorizationMonoid R
inst_2 : NormalizationMonoid R
x : R
x0 : x ≠ 0
this : Nontrivial R
h : ∀ (a : R), Multiset.count a (normalizedFactors x) ≤ 1
a : R
hu : ¬IsUnit a
h0 : a ≠ 0
b : R
hib : Irreducible b
hdvd : b ∣ a
mpr : emultiplicity b x ≤ 1
⊢ emultiplicity a x ≤ 1

Tactic:
apply le_trans (emultiplicity_le_emultiplicity_of_dvd_left hdvd)

Premises used: emultiplicity_le_emultiplicity_of_dvd_left, le_trans
-- Module: Mathlib.Algebra.Squarefree.Basic
Goal:
R : Type u_1
inst : CommMonoidWithZero R
inst_1 : UniqueFactorizationMonoid R
inst_2 : NormalizationMonoid R
x : R
x0 : x ≠ 0
this : Nontrivial R
h : ∀ (a : R), Multiset.count a (normalizedFactors x) ≤ 1
a : R
hu : ¬IsUnit a
h0 : a ≠ 0
b : R
hib : Irreducible b
hdvd : b ∣ a
mpr : LE.le (α := ℕ∞) (↑(Multiset.count ((normalize : (a : R) → R) b) (normalizedFactors x)) : ℕ∞) 1
⊢ emultiplicity b x ≤ 1

Tactic:
rw [emultiplicity_eq_count_normalizedFactors hib x0]

Premises used: UniqueFactorizationMonoid.emultiplicity_eq_count_normalizedFactors
-- Module: Mathlib.Algebra.Squarefree.Basic
Goal:
R : Type u_1
inst : CommMonoidWithZero R
inst_1 : UniqueFactorizationMonoid R
inst_2 : NormalizationMonoid R
x : R
x0 : x ≠ 0
this : Nontrivial R
h : ∀ (a : R), Multiset.count a (normalizedFactors x) ≤ 1
a : R
hu : ¬IsUnit a
h0 : a ≠ 0
b : R
hib : Irreducible b
hdvd : b ∣ a
⊢ LE.le (α := ℕ∞) (↑(Multiset.count ((normalize : (a : R) → R) b) (normalizedFactors x)) : ℕ∞) 1

Tactic:
exact_mod_cast h (normalize b)

Premises used: normalize, DFunLike.coe
-- Module: Mathlib.Algebra.Squarefree.Basic
Goal:
R : Type u_1
inst : CommMonoidWithZero R
inst_1 : UniqueFactorizationMonoid R
inst_2 : NormalizationMonoid R
x : R
x0 : x ≠ 0
rw : (∀ (x_1 : R), emultiplicity x_1 x ≤ 1 ∨ IsUnit x_1) ↔ (normalizedFactors x).Nodup
rw₁ rw₂ rw₃ :
  (∀ (x_1 : R), emultiplicity x_1 x ≤ 1 ∨ IsUnit x_1) ↔ ∀ (a : R), Multiset.count a (normalizedFactors x) ≤ 1
rw₄ :
  ∀ (this : Nontrivial R),
    (∀ (x_1 : R), emultiplicity x_1 x ≤ 1 ∨ IsUnit x_1) ↔ ∀ (a : R), Multiset.count a (normalizedFactors x) ≤ 1
mp :
  ∀ (this : Nontrivial R) (h : ∀ (x_1 : R), emultiplicity x_1 x ≤ 1 ∨ IsUnit x_1) (a : R),
    Multiset.count a (normalizedFactors x) ≤ 1
mpr mpr₁ :
  ∀ (this : Nontrivial R) (h : ∀ (a : R), Multiset.count a (normalizedFactors x) ≤ 1) (a : R),
    emultiplicity a x ≤ 1 ∨ IsUnit a
⊢ Squarefree x ↔ (normalizedFactors x).Nodup

Tactic:
classical
  rw [squarefree_iff_emultiplicity_le_one, Multiset.nodup_iff_count_le_one]
  haveI := nontrivial_of_ne x 0 x0
  constructor <;> intro h a
  · by_cases hmem : a ∈ normalizedFactors x
    · have ha := irreducible_of_normalized_factor _ hmem
      rcases h a with (h | h)
      · rw [← normalize_normalized_factor _ hmem]
        rw [emultiplicity_eq_count_normalizedFactors ha x0] at h
        assumption_mod_cast
      · have := ha.1
        contradiction
    · simp [Multiset.count_eq_zero_of_notMem hmem]
  · rw [or_iff_not_imp_right]
    intro hu
    rcases eq_or_ne a 0 with rfl | h0
    · simp [x0]
    rcases WfDvdMonoid.exists_irreducible_factor hu h0 with ⟨b, hib, hdvd⟩
    apply le_trans (emultiplicity_le_emultiplicity_of_dvd_left hdvd)
    rw [emultiplicity_eq_count_normalizedFactors hib x0]
    exact_mod_cast h (normalize b)

Premises used: UniqueFactorizationMonoid.normalizedFactors, Multiset.nodup_iff_count_le_one, Classical.or_iff_not_imp_right, squarefree_iff_emultiplicity_le_one, rfl
-- Module: Mathlib.Algebra.Squarefree.Basic
Goal:
n : ℤ
simp_rw : (∀ (x : ℕ), x * x ∣ n.natAbs → IsUnit x) ↔ ∀ (x : ℤ), x * x ∣ n → IsUnit x
simp_rw₁ : (∀ (x : ℤ), x.natAbs * x.natAbs ∣ n.natAbs → IsUnit x.natAbs) ↔ ∀ (x : ℤ), x * x ∣ n → IsUnit x
simp_rw₂ : (∀ (x : ℤ), (x * x).natAbs ∣ n.natAbs → IsUnit x.natAbs) ↔ ∀ (x : ℤ), x * x ∣ n → IsUnit x
simp_rw₃ : (∀ (x : ℤ), x * x ∣ n → IsUnit x.natAbs) ↔ ∀ (x : ℤ), x * x ∣ n → IsUnit x
simp_rw₄ : (∀ (x : ℤ), x * x ∣ n → IsUnit x.natAbs) ↔ ∀ (x : ℤ), x * x ∣ n → x.natAbs = 1
⊢ Squarefree n.natAbs ↔ Squarefree n

Tactic:
simp_rw [Squarefree, natAbs_surjective.forall, ← natAbs_mul, natAbs_dvd_natAbs,
    isUnit_iff_natAbs_eq, Nat.isUnit_iff]

Premises used: Function.Surjective.forall, Int.natAbs_mul, Int.isUnit_iff_natAbs_eq, Int.natAbs_surjective, Int.natAbs_dvd_natAbs, Nat.isUnit_iff, Squarefree
-- Module: Mathlib.Algebra.Squarefree.Basic
Goal:
n : ℕ
rw : Squarefree (natAbs (↑n : ℤ)) ↔ Squarefree n
rw₁ rw₂ : Squarefree n ↔ Squarefree n
⊢ Squarefree (R := ℤ) (↑n : ℤ) ↔ Squarefree n

Tactic:
rw [← squarefree_natAbs, natAbs_natCast]

Premises used: Int.squarefree_natAbs, Int.natAbs_natCast
-- Module: Mathlib.Algebra.Star.Basic
Goal:
R : Type u
S : Type w
inst : Star R
inst_1 : SetLike S R
hS : StarMemClass S R
s : S
x : ↥s
⊢ (↑(star x) : R) = star (↑x : R)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Star.Basic
Goal:
R : Type u
inst : InvolutiveStar R
r : R
⊢ star (star r) = r

Tactic:
star_involutive _

Premises used: InvolutiveStar.star_involutive
-- Module: Mathlib.Algebra.Star.Basic
Goal:
R : Type u
S : Type u_1
inst : SetLike S R
inst_1 : InvolutiveStar R
inst_2 : StarMemClass S R
s : S
x : R
⊢ star x ∈ s ↔ x ∈ s

Tactic:
⟨fun h => star_star x ▸ star_mem h, fun h => star_mem h⟩

Premises used: star_star, Eq.rec, StarMemClass.star_mem, Iff.intro
-- Module: Mathlib.Algebra.Star.Basic
Goal:
R : Type u
inst : InvolutiveStar R
⊢ Function.Injective.{u + 1, u + 1} (α := R) star

Tactic:
Function.Involutive.injective star_involutive

Premises used: InvolutiveStar.star_involutive, Function.Involutive.injective
-- Module: Mathlib.Algebra.Star.Basic
Goal:
S : Type u_1
R : Type u_2
inst : InvolutiveStar R
inst_1 : SetLike S R
inst_2 : StarMemClass S R
s : S
r : R
hr : star r ∈ s
rw : star (star r) ∈ s
⊢ r ∈ s

Tactic:
rw [← star_star r]

Premises used: star_star
-- Module: Mathlib.Algebra.Star.Basic
Goal:
S : Type u_1
R : Type u_2
inst : InvolutiveStar R
inst_1 : SetLike S R
inst_2 : StarMemClass S R
s : S
r : R
hr : star r ∈ s
⊢ star (star r) ∈ s

Tactic:
star_mem hr

Premises used: StarMemClass.star_mem
-- Module: Mathlib.Algebra.Star.Basic
Goal:
S : Type u_1
R : Type u_2
inst : InvolutiveStar R
inst_1 : SetLike S R
inst_2 : StarMemClass S R
s : S
r : R
hr : star r ∈ s
⊢ star (star r) ∈ s

Tactic:
exact star_mem hr

Premises used: StarMemClass.star_mem
-- Module: Mathlib.Algebra.Star.Basic
Goal:
R : Type u
inst : InvolutiveStar R
x y : R
⊢ star x = star y ↔ x = y

Tactic:
star_injective.eq_iff

Premises used: Function.Injective.eq_iff, star_injective
-- Module: Mathlib.Algebra.Star.Basic
Goal:
R : Type u
inst : InvolutiveStar R
r s : R
h : r = star s
⊢ s = star r

Tactic:
simp [h]
-- Module: Mathlib.Algebra.Star.Basic
Goal:
R : Type u
inst : InvolutiveStar R
r s : R
⊢ r = star s ↔ s = star r

Tactic:
⟨eq_star_of_eq_star, eq_star_of_eq_star⟩

Premises used: eq_star_of_eq_star, Iff.intro
-- Module: Mathlib.Algebra.Star.Basic
Goal:
R : Type u
inst : InvolutiveStar R
r s : R
⊢ star r = s ↔ star s = r

Tactic:
eq_comm.trans <| eq_star_iff_eq_star.trans eq_comm

Premises used: eq_star_iff_eq_star, eq_comm, Iff.trans
-- Module: Mathlib.Algebra.Star.Basic
Goal:
R : Type u
inst : Mul R
inst_1 : StarMul R
x y : R
rw : star y * star (star x) = star y * x
rw₁ rw₂ : star y * x = star y * x
⊢ star (star x * y) = star y * x

Tactic:
rw [star_mul, star_star]

Premises used: star_star, StarMul.star_mul
-- Module: Mathlib.Algebra.Star.Basic
Goal:
R : Type u
inst : Mul R
inst_1 : StarMul R
x y : R
rw : star (star y) * star x = y * star x
rw₁ rw₂ : y * star x = y * star x
⊢ star (x * star y) = y * star x

Tactic:
rw [star_mul, star_star]

Premises used: star_star, StarMul.star_mul
-- Module: Mathlib.Algebra.Star.Basic
Goal:
R : Type u
inst : Mul R
inst_1 : StarMul R
x y z : R
simp_rw : star x * star z = star y * star x ↔ x * y = z * x
simp_rw₁ : star (z * x) = star (x * y) ↔ x * y = z * x
simp_rw₂ : z * x = x * y ↔ x * y = z * x
⊢ SemiconjBy (star x) (star z) (star y) ↔ SemiconjBy x y z

Tactic:
simp_rw [SemiconjBy, ← star_mul, star_inj, eq_comm]

Premises used: SemiconjBy, eq_comm, StarMul.star_mul, star_inj
-- Module: Mathlib.Algebra.Star.Basic
Goal:
R : Type u
inst : Mul R
inst_1 : StarMul R
x y : R
⊢ Commute (star x) (star y) ↔ Commute x y

Tactic:
semiconjBy_star_star_star

Premises used: Commute, semiconjBy_star_star_star
-- Module: Mathlib.Algebra.Star.Basic
Goal:
R : Type u
inst : Mul R
inst_1 : StarMul R
x y : R
rw : Commute (star (star x)) (star y) ↔ Commute x (star y)
rw₁ rw₂ : Commute x (star y) ↔ Commute x (star y)
⊢ Commute (star x) y ↔ Commute x (star y)

Tactic:
rw [← commute_star_star, star_star]

Premises used: commute_star_star, star_star
-- Module: Mathlib.Algebra.Star.Basic
Goal:
R : Type u
inst : CommMagma R
inst_1 : StarMul R
x y : R
⊢ star (x * y) = star x * star y

Tactic:
(star_mul x y).trans (mul_comm _ _)

Premises used: mul_comm, StarMul.star_mul, Eq.trans
-- Module: Mathlib.Algebra.Star.Basic
Goal:
R : Type u
inst : Mul R
inst_1 : StarMul R
x y : R
⊢ op (star (x * y)) = op (star x) * op (star y)

Tactic:
simp only [star_mul, op_mul]

Premises used: MulOpposite.op_mul, StarMul.star_mul
-- Module: Mathlib.Algebra.Star.Basic
Goal:
R : Type u
inst : MulOneClass R
inst_1 : StarMul R
⊢ Eq.{u + 1} (α := R) (star 1) 1

Tactic:
op_injective <| (starMulEquiv : R ≃* Rᵐᵒᵖ).map_one.trans op_one.symm

Premises used: MulEquiv.map_one, MulOpposite.op_injective, starMulEquiv, MulOpposite.op_one, Eq.symm, Eq.trans
-- Module: Mathlib.Algebra.Star.Basic
Goal:
ι : Type u_1
R : ι → Type u_2
inst : DecidableEq ι
inst_1 : (i : ι) → MulOneClass (R i)
inst_2 : (i : ι) → StarMul (R i)
i : ι
r : R i
h : ∀ (x : ι), star (mulSingle (M := R) i r) x = mulSingle (M := R) i (star r) x
⊢ star (mulSingle (M := R) i r) = mulSingle (M := R) i (star r)

Tactic:
ext
-- Module: Mathlib.Algebra.Star.Basic
Goal:
ι : Type u_1
R : ι → Type u_2
inst : DecidableEq ι
inst_1 : (i : ι) → MulOneClass (R i)
inst_2 : (i : ι) → StarMul (R i)
i : ι
r : R i
x : ι
⊢ star (mulSingle (M := R) i r) x = mulSingle (M := R) i (star r) x

Tactic:
apply_mulSingle (fun _ ↦ star) (fun _ ↦ star_one _) ..

Premises used: Pi.apply_mulSingle, star_one, Star.star
-- Module: Mathlib.Algebra.Star.Basic
Goal:
ι : Type u_1
R : ι → Type u_2
inst : DecidableEq ι
inst_1 : (i : ι) → MulOneClass (R i)
inst_2 : (i : ι) → StarMul (R i)
i : ι
r : R i
x : ι
⊢ star (mulSingle (M := R) i r) x = mulSingle (M := R) i (star r) x

Tactic:
exact apply_mulSingle (fun _ ↦ star) (fun _ ↦ star_one _) ..

Premises used: Pi.apply_mulSingle, star_one, Star.star
-- Module: Mathlib.Algebra.Star.Basic
Goal:
R : Type u
inst : Monoid R
inst_1 : StarMul R
x : R
n : ℕ
⊢ star (x ^ n) = star x ^ n

Tactic:
op_injective <|
    ((starMulEquiv : R ≃* Rᵐᵒᵖ).toMonoidHom.map_pow x n).trans (op_pow (star x) n).symm

Premises used: MulOpposite.op_injective, starMulEquiv, MulOpposite.op_pow, MulEquiv.toMonoidHom, Eq.symm, Eq.trans, Star.star, MonoidHom.map_pow
-- Module: Mathlib.Algebra.Star.Basic
Goal:
R : Type u
inst : Group R
inst_1 : StarMul R
x : R
⊢ star x⁻¹ = (star x)⁻¹

Tactic:
op_injective <| ((starMulEquiv : R ≃* Rᵐᵒᵖ).toMonoidHom.map_inv x).trans (op_inv (star x)).symm

Premises used: MulOpposite.op_injective, starMulEquiv, MulEquiv.toMonoidHom, MonoidHom.map_inv, Eq.symm, MulOpposite.op_inv, Eq.trans, Star.star
-- Module: Mathlib.Algebra.Star.Basic
Goal:
R : Type u
inst : Group R
inst_1 : StarMul R
x : R
z : ℤ
⊢ star (x ^ z) = star x ^ z

Tactic:
op_injective <|
    ((starMulEquiv : R ≃* Rᵐᵒᵖ).toMonoidHom.map_zpow x z).trans (op_zpow (star x) z).symm

Premises used: MulOpposite.op_injective, starMulEquiv, MulEquiv.toMonoidHom, MulOpposite.op_zpow, Eq.symm, MonoidHom.map_zpow, Eq.trans, Star.star
-- Module: Mathlib.Algebra.Star.Basic
Goal:
R : Type u
inst : CommGroup R
inst_1 : StarMul R
x y : R
⊢ star (x / y) = star x / star y

Tactic:
map_div (starMulAut : R ≃* R) _ _

Premises used: starMulAut, map_div
-- Module: Mathlib.Algebra.Star.Basic
Goal:
R : Type u_1
inst : CommMonoid R
x : R
⊢ star x = x

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Star.Basic
Goal:
R : Type u
inst : AddMonoid R
inst_1 : StarAddMonoid R
⊢ Eq.{u + 1} (α := R) (star 0) 0

Tactic:
(starAddEquiv : R ≃+ R).map_zero

Premises used: AddEquiv.map_zero, starAddEquiv
-- Module: Mathlib.Algebra.Star.Basic
Goal:
ι : Type u_1
R : ι → Type u_2
inst : DecidableEq ι
inst_1 : (i : ι) → AddMonoid (R i)
inst_2 : (i : ι) → StarAddMonoid (R i)
i : ι
r : R i
h : ∀ (x : ι), star (single (M := R) i r) x = single (M := R) i (star r) x
⊢ star (single (M := R) i r) = single (M := R) i (star r)

Tactic:
ext
-- Module: Mathlib.Algebra.Star.Basic
Goal:
ι : Type u_1
R : ι → Type u_2
inst : DecidableEq ι
inst_1 : (i : ι) → AddMonoid (R i)
inst_2 : (i : ι) → StarAddMonoid (R i)
i : ι
r : R i
x : ι
⊢ star (single (M := R) i r) x = single (M := R) i (star r) x

Tactic:
apply_single (fun _ ↦ star) (fun _ ↦ star_zero _) ..

Premises used: Pi.apply_single, star_zero, Star.star
-- Module: Mathlib.Algebra.Star.Basic
Goal:
ι : Type u_1
R : ι → Type u_2
inst : DecidableEq ι
inst_1 : (i : ι) → AddMonoid (R i)
inst_2 : (i : ι) → StarAddMonoid (R i)
i : ι
r : R i
x : ι
⊢ star (single (M := R) i r) x = single (M := R) i (star r) x

Tactic:
exact apply_single (fun _ ↦ star) (fun _ ↦ star_zero _) ..

Premises used: Pi.apply_single, star_zero, Star.star
-- Module: Mathlib.Algebra.Star.Basic
Goal:
R : Type u
inst : AddMonoid R
inst_1 : StarAddMonoid R
x : R
⊢ star x = 0 ↔ x = 0

Tactic:
starAddEquiv.map_eq_zero_iff (M := R)

Premises used: AddEquiv.map_eq_zero_iff, starAddEquiv
-- Module: Mathlib.Algebra.Star.Basic
Goal:
R : Type u
inst : AddMonoid R
inst_1 : StarAddMonoid R
x : R
⊢ star x ≠ 0 ↔ x ≠ 0

Tactic:
simp only [ne_eq, star_eq_zero]

Premises used: star_eq_zero, ne_eq
-- Module: Mathlib.Algebra.Star.Basic
Goal:
R : Type u
inst : AddGroup R
inst_1 : StarAddMonoid R
r : R
⊢ star (-r) = -star r

Tactic:
(starAddEquiv : R ≃+ R).map_neg _

Premises used: starAddEquiv, AddEquiv.map_neg
-- Module: Mathlib.Algebra.Star.Basic
Goal:
R : Type u
inst : AddGroup R
inst_1 : StarAddMonoid R
r s : R
⊢ star (r - s) = star r - star s

Tactic:
(starAddEquiv : R ≃+ R).map_sub _ _

Premises used: starAddEquiv, AddEquiv.map_sub
-- Module: Mathlib.Algebra.Star.Basic
Goal:
R : Type u
inst : AddMonoid R
inst_1 : StarAddMonoid R
n : ℕ
x : R
⊢ star (n • x) = n • star x

Tactic:
(starAddEquiv : R ≃+ R).toAddMonoidHom.map_nsmul _ _

Premises used: AddEquiv.toAddMonoidHom, AddMonoidHom.map_nsmul, starAddEquiv
-- Module: Mathlib.Algebra.Star.Basic
Goal:
R : Type u
inst : AddGroup R
inst_1 : StarAddMonoid R
n : ℤ
x : R
⊢ star (n • x) = n • star x

Tactic:
(starAddEquiv : R ≃+ R).toAddMonoidHom.map_zsmul _ _

Premises used: AddMonoidHom.map_zsmul, AddEquiv.toAddMonoidHom, starAddEquiv
-- Module: Mathlib.Algebra.Star.Basic
Goal:
R : Type u
inst : NonAssocSemiring R
inst_1 : StarRing R
n : ℕ
⊢ Eq.{u + 1} (α := R) (star (↑n : R)) (↑n : R)

Tactic:
(congr_arg unop (map_natCast (starRingEquiv : R ≃+* Rᵐᵒᵖ) n)).trans (unop_natCast _)

Premises used: congr_arg, map_natCast, MulOpposite.unop, MulOpposite.unop_natCast, starRingEquiv, Eq.trans
-- Module: Mathlib.Algebra.Star.Basic
Goal:
R : Type u
inst : NonAssocSemiring R
inst_1 : StarRing R
n : ℕ
inst_2 : n.AtLeastTwo
⊢ Eq.{u + 1} (α := R) (star (OfNat.ofNat n)) (OfNat.ofNat n)

Tactic:
star_natCast _

Premises used: star_natCast
-- Module: Mathlib.Algebra.Star.Basic
Goal:
R : Type u
inst : NonAssocRing R
inst_1 : StarRing R
z : ℤ
⊢ Eq.{u + 1} (α := R) (star (↑z : R)) (↑z : R)

Tactic:
(congr_arg unop <| map_intCast (starRingEquiv : R ≃+* Rᵐᵒᵖ) z).trans (unop_intCast _)

Premises used: map_intCast, congr_arg, MulOpposite.unop_intCast, MulOpposite.unop, starRingEquiv, Eq.trans
-- Module: Mathlib.Algebra.Star.Basic
Goal:
R : Type u
inst : CommSemiring R
inst_1 : StarRing R
x : R
⊢ (starRingEnd R : (a : R) → R) x = star x

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Star.Basic
Goal:
R : Type u
inst : CommSemiring R
inst_1 : StarRing R
x : R
⊢ (starRingEnd R : (a : R) → R) ((starRingEnd R : (a : R) → R) x : R) = x

Tactic:
star_star x

Premises used: star_star
-- Module: Mathlib.Algebra.Star.Basic
Goal:
R : Type u
inst : CommSemiring R
inst_1 : StarRing R
S : Type u_1
inst_2 : NonAssocSemiring S
x : S →+* R
a :
  ∀ (x_1 : S),
    Eq.{u + 1} (α := R)
      (((fun (f : S →+* R) ↦ comp (starRingEnd R) f) ((fun (f : S →+* R) ↦ comp (starRingEnd R) f) x) : (a : S) → R)
          x_1 :
        R)
      ((x : (a : S) → R) x_1 : R)
⊢ (fun (f : S →+* R) ↦ comp (starRingEnd R) f) ((fun (f : S →+* R) ↦ comp (starRingEnd R) f) x) = x

Tactic:
ext
-- Module: Mathlib.Algebra.Star.Basic
Goal:
R : Type u
inst : CommSemiring R
inst_1 : StarRing R
S : Type u_1
inst_2 : NonAssocSemiring S
x : S →+* R
x_1 : S
⊢ Eq.{u + 1} (α := R)
    (((fun (f : S →+* R) ↦ comp (starRingEnd R) f) ((fun (f : S →+* R) ↦ comp (starRingEnd R) f) x) : (a : S) → R) x_1 :
      R)
    ((x : (a : S) → R) x_1 : R)

Tactic:
simp only [RingHom.coe_comp, Function.comp_apply, starRingEnd_self_apply]

Premises used: RingHom.coe_comp, Function.comp_apply, starRingEnd_self_apply
-- Module: Mathlib.Algebra.Star.Basic
Goal:
R : Type u
inst : CommSemiring R
inst_1 : StarRing R
S : Type u_1
inst_2 : NonAssocSemiring S
f : S →+* R
⊢ star f = comp (starRingEnd R) f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Star.Basic
Goal:
R : Type u
inst : CommSemiring R
inst_1 : StarRing R
S : Type u_1
inst_2 : NonAssocSemiring S
f : S →+* R
s : S
⊢ Eq.{u + 1} (α := R) ((star f : (a : S) → R) s : R) (star ((f : (a : S) → R) s) : R)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Star.Basic
Goal:
R : Type u
inst : CommSemiring R
inst_1 : StarRing R
inst_2 : TrivialStar R
a : R
⊢ (starRingEnd R : (a : R) → R) a = a

Tactic:
star_trivial _

Premises used: TrivialStar.star_trivial
-- Module: Mathlib.Algebra.Star.Basic
Goal:
R : Type u
inst : GroupWithZero R
inst_1 : StarMul R
x : R
⊢ star x⁻¹ = (star x)⁻¹

Tactic:
op_injective <| (map_inv₀ (starMulEquiv : R ≃* Rᵐᵒᵖ) x).trans (op_inv (star x)).symm

Premises used: MulOpposite.op_injective, starMulEquiv, map_inv₀, Eq.symm, MulOpposite.op_inv, Eq.trans, Star.star
-- Module: Mathlib.Algebra.Star.Basic
Goal:
R : Type u
inst : GroupWithZero R
inst_1 : StarMul R
x : R
z : ℤ
⊢ star (x ^ z) = star x ^ z

Tactic:
op_injective <| (map_zpow₀ (starMulEquiv : R ≃* Rᵐᵒᵖ) x z).trans (op_zpow (star x) z).symm

Premises used: MulOpposite.op_injective, starMulEquiv, MulOpposite.op_zpow, map_zpow₀, Eq.symm, Eq.trans, Star.star
-- Module: Mathlib.Algebra.Star.Basic
Goal:
R : Type u
inst : CommGroupWithZero R
inst_1 : StarMul R
x y : R
a : op (star (x / y)) = op (star x / star y)
⊢ star (x / y) = star x / star y

Tactic:
apply op_injective

Premises used: MulOpposite.op_injective
-- Module: Mathlib.Algebra.Star.Basic
Goal:
R : Type u
inst : CommGroupWithZero R
inst_1 : StarMul R
x y : R
a : op (star (x * y⁻¹)) = op (star x / star y)
a₁ : op (star (x * y⁻¹)) = (op (star y))⁻¹ * op (star x)
a₂ : op (star (y⁻¹ * x)) = (op (star y))⁻¹ * op (star x)
a₃ : op (star x * star y⁻¹) = (op (star y))⁻¹ * op (star x)
a₄ : op (star x * (star y)⁻¹) = (op (star y))⁻¹ * op (star x)
a₅ : op (star y)⁻¹ * op (star x) = (op (star y))⁻¹ * op (star x)
a₆ a₇ : (op (star y))⁻¹ * op (star x) = (op (star y))⁻¹ * op (star x)
⊢ op (star (x / y)) = op (star x / star y)

Tactic:
rw [division_def, op_div, mul_comm, star_mul, star_inv₀, op_mul, op_inv]

Premises used: division_def, MulOpposite.op_div, MulOpposite.op_mul, mul_comm, StarMul.star_mul, MulOpposite.op_inv, star_inv₀
-- Module: Mathlib.Algebra.Star.Basic
Goal:
R : Type u
⊢ TrivialStar ℕ

Tactic:
⟨fun _ ↦ rfl⟩

Premises used: TrivialStar.mk, rfl
-- Module: Mathlib.Algebra.Star.Basic
Goal:
R : Type u
⊢ TrivialStar ℤ

Tactic:
⟨fun _ ↦ rfl⟩

Premises used: TrivialStar.mk, rfl
-- Module: Mathlib.Algebra.Star.Basic
Goal:
R : Type u
inst : CommMonoid R
inst_1 : StarMul R
⊢ StarModule R R

Tactic:
⟨star_mul'⟩

Premises used: StarModule.mk, star_mul'
-- Module: Mathlib.Algebra.Star.Basic
Goal:
R : Type u
inst : CommSemiring R
inst_1 : StarRing R
⊢ RingHomInvPair (starRingEnd R) (starRingEnd R)

Tactic:
⟨RingHom.ext star_star, RingHom.ext star_star⟩

Premises used: star_star, RingHom.ext, RingHomInvPair.mk
-- Module: Mathlib.Algebra.Star.Basic
Goal:
R : Type u
inst : Monoid R
inst_1 : StarMul R
u : Rˣ
⊢ (↑(star u) : R) = star (↑u : R)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Star.Basic
Goal:
R : Type u
inst : Monoid R
inst_1 : StarMul R
u : Rˣ
⊢ (↑(star u)⁻¹ : R) = star (↑u⁻¹ : R)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Star.Basic
Goal:
R : Type u
inst : Monoid R
inst_1 : StarMul R
A : Type u_1
inst_2 : Star A
inst_3 : SMul R A
inst_4 : StarModule R A
⊢ StarModule.{u, u_1} Rˣ A

Tactic:
⟨fun u a => star_smul (u : R) a⟩

Premises used: Units.val, StarModule.star_smul, StarModule.mk
-- Module: Mathlib.Algebra.Star.Basic
Goal:
R : Type u
inst : Monoid R
inst_1 : StarMul R
a : R
⊢ IsUnit (star a) ↔ IsUnit a

Tactic:
⟨fun h => star_star a ▸ h.star, IsUnit.star⟩

Premises used: IsUnit.star, star_star, Eq.rec, Iff.intro
-- Module: Mathlib.Algebra.Star.Basic
Goal:
R : Type u
inst : Semiring R
inst_1 : StarRing R
a : R
pos : ∀ (ha : IsUnit a), (star a)⁻¹ʳ = star a⁻¹ʳ
neg : ∀ (ha : ¬IsUnit a), (star a)⁻¹ʳ = star a⁻¹ʳ
⊢ (star a)⁻¹ʳ = star a⁻¹ʳ

Tactic:
by_cases ha : IsUnit a

Premises used: IsUnit
-- Module: Mathlib.Algebra.Star.Basic
Goal:
R : Type u
inst : Semiring R
inst_1 : StarRing R
a : R
ha : IsUnit a
pos : ∀ (u : Rˣ), (star (↑u : R))⁻¹ʳ = star (↑u : R)⁻¹ʳ
⊢ (star a)⁻¹ʳ = star a⁻¹ʳ

Tactic:
obtain ⟨u, rfl⟩ := ha

Premises used: rfl
-- Module: Mathlib.Algebra.Star.Basic
Goal:
R : Type u
inst : Semiring R
inst_1 : StarRing R
u : Rˣ
pos : (star (↑u : R))⁻¹ʳ = star (↑u⁻¹ : R)
pos₁ : (↑(star u) : R)⁻¹ʳ = star (↑u⁻¹ : R)
pos₂ : (↑(star u)⁻¹ : R) = star (↑u⁻¹ : R)
pos₃ pos₄ : (↑(star u)⁻¹ : R) = (↑(star u)⁻¹ : R)
⊢ (star (↑u : R))⁻¹ʳ = star (↑u : R)⁻¹ʳ

Tactic:
rw [Ring.inverse_unit, ← Units.coe_star, Ring.inverse_unit, ← Units.coe_star_inv]

Premises used: Units.coe_star, Ring.inverse_unit, Units.coe_star_inv
-- Module: Mathlib.Algebra.Star.Basic
Goal:
R : Type u
inst : Semiring R
inst_1 : StarRing R
a : R
ha : ¬IsUnit a
neg : (star a)⁻¹ʳ = star 0
neg₁ : Eq.{u + 1} (α := R) 0 (star 0)
neg₂ neg₃ : Eq.{u + 1} (α := R) 0 0
⊢ (star a)⁻¹ʳ = star a⁻¹ʳ

Tactic:
rw [Ring.inverse_non_unit _ ha, Ring.inverse_non_unit _ (mt isUnit_star.mp ha), star_zero]

Premises used: mt, Ring.inverse_non_unit, star_zero, Iff.mp, isUnit_star
-- Module: Mathlib.Algebra.Star.Basic
Goal:
R_1 : Type u
R : Type u_1
inst : MulOneClass R
inst_1 : StarMul R
r : R
inst_2 : Invertible r
rw : star (r * @invOf _ MulOne.toMul MulOne.toOne r _) = 1
rw₁ : Eq.{u_1 + 1} (α := R) (star 1) 1
rw₂ rw₃ : Eq.{u_1 + 1} (α := R) 1 1
⊢ star (@invOf _ MulOne.toMul MulOne.toOne r _) * star r = 1

Tactic:
rw [← star_mul, mul_invOf_self, star_one]

Premises used: Invertible.mul_invOf_self, StarMul.star_mul, star_one
-- Module: Mathlib.Algebra.Star.Basic
Goal:
R_1 : Type u
R : Type u_1
inst : MulOneClass R
inst_1 : StarMul R
r : R
inst_2 : Invertible r
rw : star (@invOf _ MulOne.toMul MulOne.toOne r _ * r) = 1
rw₁ : Eq.{u_1 + 1} (α := R) (star 1) 1
rw₂ rw₃ : Eq.{u_1 + 1} (α := R) 1 1
⊢ star r * star (@invOf _ MulOne.toMul MulOne.toOne r _) = 1

Tactic:
rw [← star_mul, invOf_mul_self, star_one]

Premises used: Invertible.invOf_mul_self, StarMul.star_mul, star_one