awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Star.Pi
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → CommSemiring (α i)
inst_1 : (i : ι) → StarRing (α i)
f : (i : ι) → α i
i : ι
⊢ Eq.{u_2 + 1} (α := α i) ((starRingEnd ((i : ι) → α i) : (a : (i : ι) → α i) → (i : ι) → α i) f i : α i)
    ((starRingEnd (α i) : (a : α i) → α i) (f i) : α i)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Star.Pi
Goal:
I : Type u
f : I → Type v
inst : (i : I) → Star (f i)
inst_1 : DecidableEq I
h : (i : I) → f i
i : I
a : f i
⊢ update (β := f) (star h) i (star a) = star (update (β := f) h i a)

Tactic:
funext fun j => (apply_update (fun _ => star) h i a j).symm

Premises used: Function.apply_update, funext, Eq.symm, Star.star
-- Module: Mathlib.Algebra.Star.Pi
Goal:
I : Type u_1
J : Type u_2
α : Type u_3
x : I → α
y : J → α
inst : Star α
h : ∀ (x_1 : I ⊕ J), star (Sum.elim x y) x_1 = Sum.elim (star x) (star y) x_1
⊢ star (Sum.elim x y) = Sum.elim (star x) (star y)

Tactic:
ext x
-- Module: Mathlib.Algebra.Star.Pi
Goal:
I : Type u_1
J : Type u_2
α : Type u_3
x_1 : I → α
y : J → α
inst : Star α
x : I ⊕ J
h : ∀ (val : I), star (Sum.elim x_1 y) (Sum.inl val) = Sum.elim (star x_1) (star y) (Sum.inl val)
h₁ : ∀ (val : J), star (Sum.elim x_1 y) (Sum.inr val) = Sum.elim (star x_1) (star y) (Sum.inr val)
⊢ star (Sum.elim x_1 y) x = Sum.elim (star x_1) (star y) x

Tactic:
cases x
-- Module: Mathlib.Algebra.Star.Pi
Goal:
I : Type u_1
J : Type u_2
α : Type u_3
x : I → α
y : J → α
inst : Star α
val : I
⊢ star (Sum.elim x y) (Sum.inl val) = Sum.elim (star x) (star y) (Sum.inl val)

Tactic:
simp only [Pi.star_apply, Sum.elim_inl, Sum.elim_inr]

Premises used: Sum.elim_inr, Pi.star_apply, Sum.elim_inl
-- Module: Mathlib.Algebra.Star.Pi
Goal:
I : Type u_1
J : Type u_2
α : Type u_3
x : I → α
y : J → α
inst : Star α
val : J
⊢ star (Sum.elim x y) (Sum.inr val) = Sum.elim (star x) (star y) (Sum.inr val)

Tactic:
simp only [Pi.star_apply, Sum.elim_inl, Sum.elim_inr]

Premises used: Sum.elim_inr, Pi.star_apply, Sum.elim_inl
-- Module: Mathlib.Algebra.Star.Pointwise
Goal:
α : Type u_1
inst : Star α
⊢ Eq.{u_1 + 1} (α := Set α) ∅⋆ ∅

Tactic:
rfl

Premises used: Set.Mem, setOf, Set.preimage, rfl
-- Module: Mathlib.Algebra.Star.Pointwise
Goal:
α : Type u_1
inst : Star α
⊢ Eq.{u_1 + 1} (α := Set α) univ⋆ univ

Tactic:
rfl

Premises used: Set.Mem, Set.univ, setOf, Set.preimage, rfl
-- Module: Mathlib.Algebra.Star.Pointwise
Goal:
α : Type u_1
inst : InvolutiveStar α
s : Set α
⊢ s⋆.Nonempty ↔ s.Nonempty

Tactic:
star_involutive.surjective.nonempty_preimage

Premises used: InvolutiveStar.star_involutive, Function.Involutive.surjective, Function.Surjective.nonempty_preimage
-- Module: Mathlib.Algebra.Star.Pointwise
Goal:
α : Type u_1
inst : InvolutiveStar α
s : Set α
h : s.Nonempty
⊢ s⋆.Nonempty

Tactic:
nonempty_star.2 h

Premises used: Iff.mpr, Set.nonempty_star
-- Module: Mathlib.Algebra.Star.Pointwise
Goal:
α : Type u_1
s : Set α
a : α
inst : Star α
⊢ a ∈ s⋆ ↔ a⋆ ∈ s

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.preimage
-- Module: Mathlib.Algebra.Star.Pointwise
Goal:
α : Type u_1
s : Set α
a : α
inst : InvolutiveStar α
⊢ a⋆ ∈ s⋆ ↔ a ∈ s

Tactic:
simp only [mem_star, star_star]

Premises used: star_star, Set.mem_star
-- Module: Mathlib.Algebra.Star.Pointwise
Goal:
α : Type u_1
s : Set α
inst : Star α
⊢ star ⁻¹' s = s⋆

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Star.Pointwise
Goal:
α : Type u_1
s : Set α
inst : InvolutiveStar α
h₁ : Function.LeftInverse.{u_1 + 1, u_1 + 1} (α := α) star star
h₂ : Function.RightInverse.{u_1 + 1, u_1 + 1} (α := α) star star
⊢ star '' s = star ⁻¹' s

Tactic:
rw [image_eq_preimage_of_inverse]

Premises used: Set.image_eq_preimage_of_inverse
-- Module: Mathlib.Algebra.Star.Pointwise
Goal:
α : Type u_1
s : Set α
inst : InvolutiveStar α
x : α
⊢ x⋆⋆ = x

Tactic:
simp only [star_star]

Premises used: star_star
-- Module: Mathlib.Algebra.Star.Pointwise
Goal:
α : Type u_1
s t : Set α
inst : Star α
⊢ (s ∩ t)⋆ = s⋆ ∩ t⋆

Tactic:
preimage_inter

Premises used: Set.preimage_inter
-- Module: Mathlib.Algebra.Star.Pointwise
Goal:
α : Type u_1
s t : Set α
inst : Star α
⊢ (s ∪ t)⋆ = s⋆ ∪ t⋆

Tactic:
preimage_union

Premises used: Set.preimage_union
-- Module: Mathlib.Algebra.Star.Pointwise
Goal:
α : Type u_1
ι : Sort u_2
inst : Star α
s : ι → Set α
⊢ Eq.{u_1 + 1} (α := Set α) (⋂ (i : ι), s i)⋆ (⋂ (i : ι), (s i)⋆)

Tactic:
preimage_iInter

Premises used: Set.preimage_iInter
-- Module: Mathlib.Algebra.Star.Pointwise
Goal:
α : Type u_1
ι : Sort u_2
inst : Star α
s : ι → Set α
⊢ Eq.{u_1 + 1} (α := Set α) (⋃ (i : ι), s i)⋆ (⋃ (i : ι), (s i)⋆)

Tactic:
preimage_iUnion

Premises used: Set.preimage_iUnion
-- Module: Mathlib.Algebra.Star.Pointwise
Goal:
α : Type u_1
s : Set α
inst : Star α
⊢ sᶜ⋆ = s⋆ᶜ

Tactic:
preimage_compl

Premises used: Set.Mem, setOf, Set.preimage_compl
-- Module: Mathlib.Algebra.Star.Pointwise
Goal:
α : Type u_1
s_1 t : Set α
a : α
inst : InvolutiveStar α
s : Set α
⊢ s⋆⋆ = s

Tactic:
simp only [← star_preimage, preimage_preimage, star_star, preimage_id']

Premises used: Set.preimage_preimage, star_star, Set.preimage_id', Set.star_preimage
-- Module: Mathlib.Algebra.Star.Pointwise
Goal:
α : Type u_1
inst : InvolutiveStar α
s t : Set α
⊢ s⋆ ⊆ t⋆ ↔ s ⊆ t

Tactic:
Equiv.star.surjective.preimage_subset_preimage_iff

Premises used: Function.Surjective.preimage_subset_preimage_iff, Equiv.star, Equiv.surjective
-- Module: Mathlib.Algebra.Star.Pointwise
Goal:
α : Type u_1
inst : InvolutiveStar α
s t : Set α
rw : s⋆⋆ ⊆ t⋆ ↔ s ⊆ t⋆
rw₁ rw₂ : s ⊆ t⋆ ↔ s ⊆ t⋆
⊢ s⋆ ⊆ t ↔ s ⊆ t⋆

Tactic:
rw [← star_subset_star, star_star]

Premises used: star_star, Set.star_subset_star
-- Module: Mathlib.Algebra.Star.Pointwise
Goal:
α : Type u_1
inst : InvolutiveStar α
s : Set α
hs : s.Finite
⊢ s⋆.Finite

Tactic:
hs.preimage star_injective.injOn

Premises used: Function.Injective.injOn, star_injective, Set.Finite.preimage
-- Module: Mathlib.Algebra.Star.Pointwise
Goal:
β : Type u_2
inst : InvolutiveStar β
x : β
h : ∀ (y : β), Membership.mem (γ := Set β) {x}⋆ y ↔ Membership.mem (γ := Set β) {x⋆} y
⊢ Eq (α := Set β) {x}⋆ {x⋆}

Tactic:
ext1 y
-- Module: Mathlib.Algebra.Star.Pointwise
Goal:
β : Type u_2
inst : InvolutiveStar β
x y : β
h : Membership.mem (γ := Set β) {x} y⋆ ↔ Membership.mem (γ := Set β) {x⋆} y
h₁ : y⋆ = x ↔ Membership.mem (γ := Set β) {x⋆} y
h₂ : y⋆ = x ↔ y = x⋆
h₃ : x⋆ = y ↔ y = x⋆
h₄ h₅ : y = x⋆ ↔ y = x⋆
⊢ Membership.mem (γ := Set β) {x}⋆ y ↔ Membership.mem (γ := Set β) {x⋆} y

Tactic:
rw [mem_star, mem_singleton_iff, mem_singleton_iff, star_eq_iff_star_eq, eq_comm]

Premises used: eq_comm, star_eq_iff_star_eq, Set.mem_singleton_iff, Set.mem_star
-- Module: Mathlib.Algebra.Star.Pointwise
Goal:
α : Type u_1
inst : Mul α
inst_1 : StarMul α
s t : Set α
simp_rw : star '' (s * t) = star '' t * star '' s
simp_rw₁ :
  Eq (α := Set α) (star '' image2 (fun (x1 x2 : α) ↦ x1 * x2) s t)
    (image2 (fun (x1 x2 : α) ↦ x1 * x2) (star '' t) (star '' s))
simp_rw₂ :
  Eq (α := Set α) (image2 (fun (a b : α) ↦ (a * b)⋆) s t) (image2 (fun (x1 x2 : α) ↦ x1 * x2) (star '' t) (star '' s))
simp_rw₃ : Eq (α := Set α) (image2 (fun (a b : α) ↦ (a * b)⋆) s t) (image2 (fun (a b : α) ↦ a⋆ * b) t (star '' s))
simp_rw₄ : Eq (α := Set α) (image2 (fun (a b : α) ↦ (a * b)⋆) s t) (image2 (fun (a b : α) ↦ a⋆ * b⋆) t s)
simp_rw₅ : Eq (α := Set α) (image2 (fun (a b : α) ↦ b⋆ * a⋆) s t) (image2 (fun (a b : α) ↦ a⋆ * b⋆) t s)
⊢ (s * t)⋆ = t⋆ * s⋆

Tactic:
simp_rw [← image_star, ← image2_mul, image_image2, image2_image_left, image2_image_right,
    star_mul, image2_swap _ s t]

Premises used: Set.image_star, Set.image2_image_right, Set.image2_image_left, Set.image_image2, Set.image2_mul, StarMul.star_mul, Set.image2_swap
-- Module: Mathlib.Algebra.Star.Pointwise
Goal:
α : Type u_1
inst : AddMonoid α
inst_1 : StarAddMonoid α
s t : Set α
simp_rw : star '' (s + t) = star '' s + star '' t
simp_rw₁ :
  Eq (α := Set α) (star '' image2 (fun (x1 x2 : α) ↦ x1 + x2) s t)
    (image2 (fun (x1 x2 : α) ↦ x1 + x2) (star '' s) (star '' t))
simp_rw₂ :
  Eq (α := Set α) (image2 (fun (a b : α) ↦ (a + b)⋆) s t) (image2 (fun (x1 x2 : α) ↦ x1 + x2) (star '' s) (star '' t))
simp_rw₃ : Eq (α := Set α) (image2 (fun (a b : α) ↦ (a + b)⋆) s t) (image2 (fun (a b : α) ↦ a⋆ + b) s (star '' t))
simp_rw₄ : Eq (α := Set α) (image2 (fun (a b : α) ↦ (a + b)⋆) s t) (image2 (fun (a b : α) ↦ a⋆ + b⋆) s t)
⊢ (s + t)⋆ = s⋆ + t⋆

Tactic:
simp_rw [← image_star, ← image2_add, image_image2, image2_image_left, image2_image_right,
    star_add]

Premises used: Set.image_star, Set.image2_image_right, StarAddMonoid.star_add, Set.image2_image_left, Set.image_image2, Set.image2_add
-- Module: Mathlib.Algebra.Star.Pointwise
Goal:
α : Type u_1
s_1 t : Set α
a : α
inst : Star α
inst_1 : TrivialStar α
s : Set α
h : ∀ (x : α), x ∈ star ⁻¹' s ↔ x ∈ s
⊢ star ⁻¹' s = s

Tactic:
ext1
-- Module: Mathlib.Algebra.Star.Pointwise
Goal:
α : Type u_1
s_1 t : Set α
a : α
inst : Star α
inst_1 : TrivialStar α
s : Set α
x : α
⊢ x ∈ star ⁻¹' s ↔ x ∈ s

Tactic:
simp [star_trivial]

Premises used: TrivialStar.star_trivial
-- Module: Mathlib.Algebra.Star.Pointwise
Goal:
α : Type u_1
inst : Group α
inst_1 : StarMul α
s : Set α
h : ∀ (x : α), x ∈ s⁻¹⋆ ↔ x ∈ s⋆⁻¹
⊢ s⁻¹⋆ = s⋆⁻¹

Tactic:
ext
-- Module: Mathlib.Algebra.Star.Pointwise
Goal:
α : Type u_1
inst : Group α
inst_1 : StarMul α
s : Set α
x : α
⊢ x ∈ s⁻¹⋆ ↔ x ∈ s⋆⁻¹

Tactic:
simp only [mem_star, mem_inv, star_inv]

Premises used: Set.mem_star, star_inv, Set.mem_inv
-- Module: Mathlib.Algebra.Star.Pointwise
Goal:
α : Type u_1
inst : GroupWithZero α
inst_1 : StarMul α
s : Set α
h : ∀ (x : α), x ∈ s⁻¹⋆ ↔ x ∈ s⋆⁻¹
⊢ s⁻¹⋆ = s⋆⁻¹

Tactic:
ext
-- Module: Mathlib.Algebra.Star.Pointwise
Goal:
α : Type u_1
inst : GroupWithZero α
inst_1 : StarMul α
s : Set α
x : α
⊢ x ∈ s⁻¹⋆ ↔ x ∈ s⋆⁻¹

Tactic:
simp only [mem_star, mem_inv, star_inv₀]

Premises used: Set.mem_star, star_inv₀, Set.mem_inv
-- Module: Mathlib.Algebra.Star.Pointwise
Goal:
S : Type u_1
α : Type u_2
inst : InvolutiveStar α
inst_1 : SetLike S α
inst_2 : StarMemClass S α
s : S
h : ∀ (x : α), x ∈ star (↑s : Set α) ↔ x ∈ (↑s : Set α)
⊢ star (↑s : Set α) = (↑s : Set α)

Tactic:
ext
-- Module: Mathlib.Algebra.Star.Pointwise
Goal:
S : Type u_1
α : Type u_2
inst : InvolutiveStar α
inst_1 : SetLike S α
inst_2 : StarMemClass S α
s : S
x : α
⊢ x ∈ star (↑s : Set α) ↔ x ∈ (↑s : Set α)

Tactic:
simpa using star_mem_iff

Premises used: star_mem_iff
-- Module: Mathlib.Algebra.Star.Prod
Goal:
R : Type u
inst : Monoid R
inst_1 : StarMul R
u : Rˣ
⊢ Eq (α := R × Rᵐᵒᵖ) ((embedProduct R : (a : Rˣ) → R × Rᵐᵒᵖ) (star u) : R × Rᵐᵒᵖ)
    (star ((embedProduct R : (a : Rˣ) → R × Rᵐᵒᵖ) u) : R × Rᵐᵒᵖ)

Tactic:
rfl

Premises used: MulOpposite.unop, rfl
-- Module: Mathlib.Algebra.Star.Rat
Goal:
⊢ TrivialStar ℚ

Tactic:
⟨fun _ ↦ rfl⟩

Premises used: TrivialStar.mk, rfl
-- Module: Mathlib.Algebra.Star.Rat
Goal:
⊢ TrivialStar ℚ≥0

Tactic:
⟨fun _ ↦ rfl⟩

Premises used: TrivialStar.mk, rfl
-- Module: Mathlib.Algebra.Star.Rat
Goal:
R : Type u_1
inst : DivisionSemiring R
inst_1 : StarRing R
q : ℚ≥0
⊢ Eq.{u_1 + 1} (α := R) (star (↑q : R)) (↑q : R)

Tactic:
(congr_arg unop <| map_nnratCast (starRingEquiv : R ≃+* Rᵐᵒᵖ) q).trans (unop_nnratCast _)

Premises used: MulOpposite.unop_nnratCast, map_nnratCast, congr_arg, MulOpposite.unop, starRingEquiv, Eq.trans
-- Module: Mathlib.Algebra.Star.Rat
Goal:
R : Type u_1
inst : DivisionRing R
inst_1 : StarRing R
r : ℚ
⊢ Eq.{u_1 + 1} (α := R) (star (↑r : R)) (↑r : R)

Tactic:
(congr_arg unop <| map_ratCast (starRingEquiv : R ≃+* Rᵐᵒᵖ) r).trans (unop_ratCast _)

Premises used: map_ratCast, MulOpposite.unop_ratCast, congr_arg, MulOpposite.unop, starRingEquiv, Eq.trans
-- Module: Mathlib.Algebra.Star.RingQuot
Goal:
R : Type u
inst : Semiring R
r : R → R → Prop
inst_1 : StarRing R
hr : ∀ (a b : R), r a b → r (Star.star a) (Star.star b)
a b x y : R
h : r x y
⊢ Rel r (Star.star x) (Star.star y)

Tactic:
Rel.of (hr _ _ h)

Premises used: RingQuot.Rel.of
-- Module: Mathlib.Algebra.Star.RingQuot
Goal:
R : Type u
inst : Semiring R
r : R → R → Prop
inst_1 : StarRing R
hr : ∀ (a b : R), r a b → r (Star.star a) (Star.star b)
a b x y : R
h : r x y
⊢ Rel r (Star.star x) (Star.star y)

Tactic:
exact Rel.of (hr _ _ h)

Premises used: RingQuot.Rel.of
-- Module: Mathlib.Algebra.Star.RingQuot
Goal:
R : Type u
inst : Semiring R
r : R → R → Prop
inst_1 : StarRing R
hr : ∀ (a b : R), r a b → r (Star.star a) (Star.star b)
a b a_1 b_1 c : R
h_1 : Rel r a_1 b_1
h : Rel r (Star.star a_1) (Star.star b_1)
add_left : Rel r (Star.star a_1 + Star.star c) (Star.star b_1 + Star.star c)
⊢ Rel r (Star.star (a_1 + c)) (Star.star (b_1 + c))

Tactic:
rw [star_add, star_add]

Premises used: StarAddMonoid.star_add
-- Module: Mathlib.Algebra.Star.RingQuot
Goal:
R : Type u
inst : Semiring R
r : R → R → Prop
inst_1 : StarRing R
hr : ∀ (a b : R), r a b → r (Star.star a) (Star.star b)
a b a_1 b_1 c : R
h_1 : Rel r a_1 b_1
h : Rel r (Star.star a_1) (Star.star b_1)
⊢ Rel r (Star.star a_1 + Star.star c) (Star.star b_1 + Star.star c)

Tactic:
Rel.add_left h

Premises used: RingQuot.Rel.add_left
-- Module: Mathlib.Algebra.Star.RingQuot
Goal:
R : Type u
inst : Semiring R
r : R → R → Prop
inst_1 : StarRing R
hr : ∀ (a b : R), r a b → r (Star.star a) (Star.star b)
a b a_1 b_1 c : R
h_1 : Rel r a_1 b_1
h : Rel r (Star.star a_1) (Star.star b_1)
⊢ Rel r (Star.star a_1 + Star.star c) (Star.star b_1 + Star.star c)

Tactic:
exact Rel.add_left h

Premises used: RingQuot.Rel.add_left
-- Module: Mathlib.Algebra.Star.RingQuot
Goal:
R : Type u
inst : Semiring R
r : R → R → Prop
inst_1 : StarRing R
hr : ∀ (a b : R), r a b → r (Star.star a) (Star.star b)
a b a_1 b_1 c : R
h_1 : Rel r a_1 b_1
h : Rel r (Star.star a_1) (Star.star b_1)
mul_left : Rel r (Star.star c * Star.star a_1) (Star.star c * Star.star b_1)
⊢ Rel r (Star.star (a_1 * c)) (Star.star (b_1 * c))

Tactic:
rw [star_mul, star_mul]

Premises used: StarMul.star_mul
-- Module: Mathlib.Algebra.Star.RingQuot
Goal:
R : Type u
inst : Semiring R
r : R → R → Prop
inst_1 : StarRing R
hr : ∀ (a b : R), r a b → r (Star.star a) (Star.star b)
a b a_1 b_1 c : R
h_1 : Rel r a_1 b_1
h : Rel r (Star.star a_1) (Star.star b_1)
⊢ Rel r (Star.star c * Star.star a_1) (Star.star c * Star.star b_1)

Tactic:
Rel.mul_right h

Premises used: RingQuot.Rel.mul_right
-- Module: Mathlib.Algebra.Star.RingQuot
Goal:
R : Type u
inst : Semiring R
r : R → R → Prop
inst_1 : StarRing R
hr : ∀ (a b : R), r a b → r (Star.star a) (Star.star b)
a b a_1 b_1 c : R
h_1 : Rel r a_1 b_1
h : Rel r (Star.star a_1) (Star.star b_1)
⊢ Rel r (Star.star c * Star.star a_1) (Star.star c * Star.star b_1)

Tactic:
exact Rel.mul_right h

Premises used: RingQuot.Rel.mul_right
-- Module: Mathlib.Algebra.Star.RingQuot
Goal:
R : Type u
inst : Semiring R
r : R → R → Prop
inst_1 : StarRing R
hr : ∀ (a b : R), r a b → r (Star.star a) (Star.star b)
a b a_1 b_1 c : R
h_1 : Rel r b_1 c
h : Rel r (Star.star b_1) (Star.star c)
mul_right : Rel r (Star.star b_1 * Star.star a_1) (Star.star c * Star.star a_1)
⊢ Rel r (Star.star (a_1 * b_1)) (Star.star (a_1 * c))

Tactic:
rw [star_mul, star_mul]

Premises used: StarMul.star_mul
-- Module: Mathlib.Algebra.Star.RingQuot
Goal:
R : Type u
inst : Semiring R
r : R → R → Prop
inst_1 : StarRing R
hr : ∀ (a b : R), r a b → r (Star.star a) (Star.star b)
a b a_1 b_1 c : R
h_1 : Rel r b_1 c
h : Rel r (Star.star b_1) (Star.star c)
⊢ Rel r (Star.star b_1 * Star.star a_1) (Star.star c * Star.star a_1)

Tactic:
Rel.mul_left h

Premises used: RingQuot.Rel.mul_left
-- Module: Mathlib.Algebra.Star.RingQuot
Goal:
R : Type u
inst : Semiring R
r : R → R → Prop
inst_1 : StarRing R
hr : ∀ (a b : R), r a b → r (Star.star a) (Star.star b)
a b a_1 b_1 c : R
h_1 : Rel r b_1 c
h : Rel r (Star.star b_1) (Star.star c)
⊢ Rel r (Star.star b_1 * Star.star a_1) (Star.star c * Star.star a_1)

Tactic:
exact Rel.mul_left h

Premises used: RingQuot.Rel.mul_left
-- Module: Mathlib.Algebra.Star.RingQuot
Goal:
R : Type u
inst : Semiring R
r : R → R → Prop
inst_1 : StarRing R
hr : ∀ (a b : R), r a b → r (Star.star a) (Star.star b)
a b : R
h : Rel r a b
of : ∀ ⦃x y : R⦄ (h : r x y), Rel r (Star.star x) (Star.star y)
add_left :
  ∀ ⦃a b c : R⦄, Rel r a b → ∀ (h : Rel r (Star.star a) (Star.star b)), Rel r (Star.star (a + c)) (Star.star (b + c))
mul_left :
  ∀ ⦃a b c : R⦄, Rel r a b → ∀ (h : Rel r (Star.star a) (Star.star b)), Rel r (Star.star (a * c)) (Star.star (b * c))
mul_right :
  ∀ ⦃a b c : R⦄, Rel r b c → ∀ (h : Rel r (Star.star b) (Star.star c)), Rel r (Star.star (a * b)) (Star.star (a * c))
⊢ Rel r (Star.star a) (Star.star b)

Tactic:
induction h with
  | of h          => exact Rel.of (hr _ _ h)
  | add_left _ h  => rw [star_add, star_add]
                     exact Rel.add_left h
  | mul_left _ h  => rw [star_mul, star_mul]
                     exact Rel.mul_right h
  | mul_right _ h => rw [star_mul, star_mul]
                     exact Rel.mul_left h

Premises used: StarAddMonoid.star_add, RingQuot.Rel.mul_left, StarMul.star_mul, RingQuot.Rel.mul_right, RingQuot.Rel.of, RingQuot.Rel.add_left
-- Module: Mathlib.Algebra.Star.RingQuot
Goal:
R : Type u
inst : Semiring R
r : R → R → Prop
inst_1 : StarRing R
hr : ∀ (a b : R), r a b → r (star a) (star b)
a : R
⊢ star' r hr (mk (r := r) (Quot.mk (Rel r) a)) = mk (r := r) (Quot.mk (Rel r) (star a))

Tactic:
rfl

Premises used: Quot.map, _private.0.RingQuot.star', rfl
-- Module: Mathlib.Algebra.Star.RingQuot
Goal:
R_1 : Type u
inst : Semiring R_1
r_1 : R_1 → R_1 → Prop
inst_1 : StarRing R_1
R : Type u
inst_2 : Semiring R
inst_3 : StarRing R
r : R → R → Prop
hr : ∀ (a b : R), r a b → r (star a) (star b)
toQuot : Quot (Rel r)
a : R
⊢ star' r hr (star' r hr (mk (r := r) (Quot.mk (Rel r) a))) = mk (r := r) (Quot.mk (Rel r) a)

Tactic:
simp [star'_quot]

Premises used: _private.0.RingQuot.star'_quot
-- Module: Mathlib.Algebra.Star.RingQuot
Goal:
R_1 : Type u
inst : Semiring R_1
r_1 : R_1 → R_1 → Prop
inst_1 : StarRing R_1
R : Type u
inst_2 : Semiring R
inst_3 : StarRing R
r : R → R → Prop
hr : ∀ (a b : R), r a b → r (star a) (star b)
toQuot : Quot (Rel r)
a : R
toQuot_1 : Quot (Rel r)
a_1 : R
⊢ star' r hr (mk (r := r) (Quot.mk (Rel r) a) * mk (r := r) (Quot.mk (Rel r) a_1)) =
    star' r hr (mk (r := r) (Quot.mk (Rel r) a_1)) * star' r hr (mk (r := r) (Quot.mk (Rel r) a))

Tactic:
simp [star'_quot, mul_quot, star_mul]

Premises used: RingQuot.mul_quot, _private.0.RingQuot.star'_quot, StarMul.star_mul
-- Module: Mathlib.Algebra.Star.RingQuot
Goal:
R_1 : Type u
inst : Semiring R_1
r_1 : R_1 → R_1 → Prop
inst_1 : StarRing R_1
R : Type u
inst_2 : Semiring R
inst_3 : StarRing R
r : R → R → Prop
hr : ∀ (a b : R), r a b → r (star a) (star b)
toQuot : Quot (Rel r)
a : R
toQuot_1 : Quot (Rel r)
a_1 : R
⊢ star' r hr (mk (r := r) (Quot.mk (Rel r) a) + mk (r := r) (Quot.mk (Rel r) a_1)) =
    star' r hr (mk (r := r) (Quot.mk (Rel r) a)) + star' r hr (mk (r := r) (Quot.mk (Rel r) a_1))

Tactic:
simp [star'_quot, add_quot, star_add]

Premises used: RingQuot.add_quot, StarAddMonoid.star_add, _private.0.RingQuot.star'_quot
-- Module: Mathlib.Algebra.Star.SelfAdjoint
Goal:
R : Type u_1
inst : Mul R
inst_1 : Star R
x : R
inst_2 : IsStarNormal x
⊢ star x * x = x * star x

Tactic:
IsStarNormal.star_comm_self

Premises used: IsStarNormal.star_comm_self, SemiconjBy, Commute
-- Module: Mathlib.Algebra.Star.SelfAdjoint
Goal:
R : Type u_1
inst : Star R
inst_1 : TrivialStar R
r : R
⊢ IsSelfAdjoint r

Tactic:
star_trivial _

Premises used: IsSelfAdjoint, TrivialStar.star_trivial
-- Module: Mathlib.Algebra.Star.SelfAdjoint
Goal:
R : Type u_1
inst : Star R
x : R
hx : IsSelfAdjoint x
⊢ star x = x

Tactic:
hx

Premises used: IsSelfAdjoint
-- Module: Mathlib.Algebra.Star.SelfAdjoint
Goal:
R : Type u_1
inst : Star R
x : R
⊢ IsSelfAdjoint x ↔ star x = x

Tactic:
Iff.rfl

Premises used: IsSelfAdjoint, Iff.rfl
-- Module: Mathlib.Algebra.Star.SelfAdjoint
Goal:
R : Type u_1
inst : InvolutiveStar R
x : R
⊢ IsSelfAdjoint (star x) ↔ IsSelfAdjoint x

Tactic:
simpa only [IsSelfAdjoint, star_star] using eq_comm

Premises used: IsSelfAdjoint, star_star, eq_comm
-- Module: Mathlib.Algebra.Star.SelfAdjoint
Goal:
R : Type u_1
inst : Mul R
inst_1 : StarMul R
x : R
⊢ IsSelfAdjoint (star x * x)

Tactic:
simp only [IsSelfAdjoint, star_mul, star_star]

Premises used: IsSelfAdjoint, star_star, StarMul.star_mul
-- Module: Mathlib.Algebra.Star.SelfAdjoint
Goal:
R : Type u_1
inst : Mul R
inst_1 : StarMul R
x : R
⊢ IsSelfAdjoint (x * star x)

Tactic:
simpa only [star_star] using star_mul_self (star x)

Premises used: IsSelfAdjoint.star_mul_self, star_star, Star.star
-- Module: Mathlib.Algebra.Star.SelfAdjoint
Goal:
R : Type u_3
inst : Mul R
inst_1 : StarMul R
x y : R
hx : IsSelfAdjoint x
hy : IsSelfAdjoint y
⊢ Commute x y ↔ IsSelfAdjoint (x * y)

Tactic:
⟨fun h ↦ ?_, fun h ↦ ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.Algebra.Star.SelfAdjoint
Goal:
R : Type u_3
inst : Mul R
inst_1 : StarMul R
x y : R
hx : IsSelfAdjoint x
hy : IsSelfAdjoint y
refine_1 : ∀ (h : Commute x y), IsSelfAdjoint (x * y)
refine_2 : ∀ (h : IsSelfAdjoint (x * y)), Commute x y
⊢ Commute x y ↔ IsSelfAdjoint (x * y)

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
-- Module: Mathlib.Algebra.Star.SelfAdjoint
Goal:
R : Type u_3
inst : Mul R
inst_1 : StarMul R
x y : R
hx : IsSelfAdjoint x
hy : IsSelfAdjoint y
h : Commute x y
refine_1 : star (x * y) = x * y
refine_1₁ : star y * star x = x * y
refine_1₂ : star y * x = x * y
refine_1₃ : y * x = x * y
refine_1₄ refine_1₅ : y * x = y * x
⊢ IsSelfAdjoint (x * y)

Tactic:
rw [isSelfAdjoint_iff, star_mul, hx.star_eq, hy.star_eq, h.eq]

Premises used: StarMul.star_mul, isSelfAdjoint_iff, Commute.eq, IsSelfAdjoint.star_eq
-- Module: Mathlib.Algebra.Star.SelfAdjoint
Goal:
R : Type u_3
inst : Mul R
inst_1 : StarMul R
x y : R
hx : IsSelfAdjoint x
hy : IsSelfAdjoint y
h : IsSelfAdjoint (x * y)
⊢ Commute x y

Tactic:
simpa only [star_mul, hx.star_eq, hy.star_eq] using h.symm

Premises used: StarMul.star_mul, Eq.symm, IsSelfAdjoint.star_eq
-- Module: Mathlib.Algebra.Star.SelfAdjoint
Goal:
R : Type u_3
inst : Mul R
inst_1 : StarMul R
x y z : R
hx : IsSelfAdjoint x
hy : IsSelfAdjoint y
hz : IsSelfAdjoint z
hxyz : x * y = z
⊢ Commute x y

Tactic:
grind [commute_iff hx hy]

Premises used: IsSelfAdjoint.commute_iff
-- Module: Mathlib.Algebra.Star.SelfAdjoint
Goal:
F : Type u_3
R : Type u_4
S : Type u_5
inst : Star R
inst_1 : Star S
inst_2 : FunLike F R S
inst_3 : StarHomClass F R S
x : R
hx : IsSelfAdjoint x
f : F
⊢ IsSelfAdjoint.{u_5} (R := S) ((f : (a : R) → S) x : S)

Tactic:
show star (f x) = f x from map_star f x ▸ congr_arg f hx

Premises used: IsSelfAdjoint, Eq.rec, StarHomClass.map_star, congr_arg, DFunLike.coe
-- Module: Mathlib.Algebra.Star.SelfAdjoint
Goal:
F : Type u_3
R : Type u_4
S : Type u_5
inst : Star R
inst_1 : Star S
inst_2 : FunLike F R S
inst_3 : StarHomClass F R S
inst_4 : TrivialStar R
f : F
x : R
⊢ IsSelfAdjoint.{u_5} (R := S) ((f : (a : R) → S) x : S)

Tactic:
(IsSelfAdjoint.all x).map f

Premises used: IsSelfAdjoint.map, IsSelfAdjoint.all
-- Module: Mathlib.Algebra.Star.SelfAdjoint
Goal:
R : Type u_3
inst : Mul R
inst_1 : Star R
x : R
hx : IsSelfAdjoint x
⊢ Commute (star x) x

Tactic:
simp only [Commute, SemiconjBy, hx.star_eq]

Premises used: SemiconjBy, Commute, IsSelfAdjoint.star_eq
-- Module: Mathlib.Algebra.Star.SelfAdjoint
Goal:
R : Type u_1
inst : AddMonoid R
inst_1 : StarAddMonoid R
⊢ IsSelfAdjoint.{u_1} (R := R) 0

Tactic:
star_zero R

Premises used: IsSelfAdjoint, star_zero
-- Module: Mathlib.Algebra.Star.SelfAdjoint
Goal:
R : Type u_1
inst : AddMonoid R
inst_1 : StarAddMonoid R
x y : R
hx : IsSelfAdjoint x
hy : IsSelfAdjoint y
⊢ IsSelfAdjoint (x + y)

Tactic:
simp only [isSelfAdjoint_iff, star_add, hx.star_eq, hy.star_eq]

Premises used: StarAddMonoid.star_add, isSelfAdjoint_iff, IsSelfAdjoint.star_eq
-- Module: Mathlib.Algebra.Star.SelfAdjoint
Goal:
R : Type u_1
inst : AddGroup R
inst_1 : StarAddMonoid R
x : R
hx : IsSelfAdjoint x
⊢ IsSelfAdjoint (-x)

Tactic:
simp only [isSelfAdjoint_iff, star_neg, hx.star_eq]

Premises used: star_neg, isSelfAdjoint_iff, IsSelfAdjoint.star_eq
-- Module: Mathlib.Algebra.Star.SelfAdjoint
Goal:
R : Type u_1
inst : AddGroup R
inst_1 : StarAddMonoid R
x y : R
hx : IsSelfAdjoint x
hy : IsSelfAdjoint y
⊢ IsSelfAdjoint (x - y)

Tactic:
simp only [isSelfAdjoint_iff, star_sub, hx.star_eq, hy.star_eq]

Premises used: isSelfAdjoint_iff, star_sub, IsSelfAdjoint.star_eq