awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Star.Pointwise (goal)
Goal:
β : Type u_2
inst : InvolutiveStar β
x y : β
⊢ Membership.mem (γ := Set β) {x}⋆ y ↔ Membership.mem (γ := Set β) {x⋆} y
have h : 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]
-- Lean 4 proof step from Mathlib.Algebra.Star.Pointwise (goal)
Goal:
β : Type u_2
inst : InvolutiveStar β
x y : β
h : Membership.mem (γ := Set β) {x} y⋆ ↔ Membership.mem (γ := Set β) {x⋆} y
⊢ Membership.mem (γ := Set β) {x}⋆ y ↔ Membership.mem (γ := Set β) {x⋆} y
have h₁ : y⋆ = x ↔ Membership.mem (γ := Set β) {x⋆} y
Tactic: rw [mem_star, mem_singleton_iff, mem_singleton_iff, star_eq_iff_star_eq, eq_comm]
-- Lean 4 proof step from Mathlib.Algebra.Star.Pointwise (goal)
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
⊢ Membership.mem (γ := Set β) {x}⋆ y ↔ Membership.mem (γ := Set β) {x⋆} y
have h₂ : y⋆ = x ↔ y = x⋆
Tactic: rw [mem_star, mem_singleton_iff, mem_singleton_iff, star_eq_iff_star_eq, eq_comm]
-- Lean 4 proof step from Mathlib.Algebra.Star.Pointwise (goal)
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⋆
⊢ Membership.mem (γ := Set β) {x}⋆ y ↔ Membership.mem (γ := Set β) {x⋆} y
have h₃ : x⋆ = y ↔ y = x⋆
Tactic: rw [mem_star, mem_singleton_iff, mem_singleton_iff, star_eq_iff_star_eq, eq_comm]
-- Lean 4 proof step from Mathlib.Algebra.Star.Pointwise (goal)
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⋆
⊢ Membership.mem (γ := Set β) {x}⋆ y ↔ Membership.mem (γ := Set β) {x⋆} y
have h₄ : y = x⋆ ↔ y = x⋆
Tactic: rw [mem_star, mem_singleton_iff, mem_singleton_iff, star_eq_iff_star_eq, eq_comm]
-- Lean 4 proof step from Mathlib.Algebra.Star.Pointwise (goal)
Goal:
α : Type u_1
inst : Mul α
inst_1 : StarMul α
s t : Set α
⊢ (s * t)⋆ = t⋆ * s⋆
have simp_rw : star '' (s * t) = star '' t * star '' s
Tactic: simp_rw [← image_star, ← image2_mul, image_image2, image2_image_left, image2_image_right,
    star_mul, image2_swap _ s t]
-- Lean 4 proof step from Mathlib.Algebra.Star.Pointwise (goal)
Goal:
α : Type u_1
inst : Mul α
inst_1 : StarMul α
s t : Set α
simp_rw : star '' (s * t) = star '' t * star '' s
⊢ (s * t)⋆ = t⋆ * s⋆
have simp_rw₁ : Eq (α := Set α) (star '' image2 (fun (x1 x2 : α) ↦ x1 * x2) s t)
  (image2 (fun (x1 x2 : α) ↦ x1 * x2) (star '' t) (star '' s))
Tactic: simp_rw [← image_star, ← image2_mul, image_image2, image2_image_left, image2_image_right,
    star_mul, image2_swap _ s t]
-- Lean 4 proof step from Mathlib.Algebra.Star.Pointwise (goal)
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))
⊢ (s * t)⋆ = t⋆ * s⋆
have simp_rw₂ : Eq (α := Set α) (image2 (fun (a b : α) ↦ (a * b)⋆) s t) (image2 (fun (x1 x2 : α) ↦ x1 * x2) (star '' t) (star '' s))
Tactic: simp_rw [← image_star, ← image2_mul, image_image2, image2_image_left, image2_image_right,
    star_mul, image2_swap _ s t]
-- Lean 4 proof step from Mathlib.Algebra.Star.Pointwise (goal)
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))
⊢ (s * t)⋆ = t⋆ * s⋆
have simp_rw₃ : Eq (α := Set α) (image2 (fun (a b : α) ↦ (a * b)⋆) s t) (image2 (fun (a b : α) ↦ a⋆ * b) t (star '' s))
Tactic: simp_rw [← image_star, ← image2_mul, image_image2, image2_image_left, image2_image_right,
    star_mul, image2_swap _ s t]
-- Lean 4 proof step from Mathlib.Algebra.Star.Pointwise (goal)
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))
⊢ (s * t)⋆ = t⋆ * s⋆
have simp_rw₄ : Eq (α := Set α) (image2 (fun (a b : α) ↦ (a * b)⋆) s t) (image2 (fun (a b : α) ↦ a⋆ * b⋆) t s)
Tactic: simp_rw [← image_star, ← image2_mul, image_image2, image2_image_left, image2_image_right,
    star_mul, image2_swap _ s t]
-- Lean 4 proof step from Mathlib.Algebra.Star.Pointwise (goal)
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)
⊢ (s * t)⋆ = t⋆ * s⋆
have simp_rw₅ : Eq (α := Set α) (image2 (fun (a b : α) ↦ b⋆ * a⋆) s t) (image2 (fun (a b : α) ↦ a⋆ * b⋆) t s)
Tactic: simp_rw [← image_star, ← image2_mul, image_image2, image2_image_left, image2_image_right,
    star_mul, image2_swap _ s t]
-- Lean 4 proof step from Mathlib.Algebra.Star.Pointwise (goal)
Goal:
α : Type u_1
inst : AddMonoid α
inst_1 : StarAddMonoid α
s t : Set α
⊢ (s + t)⋆ = s⋆ + t⋆
have simp_rw : star '' (s + t) = star '' s + star '' t
Tactic: simp_rw [← image_star, ← image2_add, image_image2, image2_image_left, image2_image_right,
    star_add]
-- Lean 4 proof step from Mathlib.Algebra.Star.Pointwise (goal)
Goal:
α : Type u_1
inst : AddMonoid α
inst_1 : StarAddMonoid α
s t : Set α
simp_rw : star '' (s + t) = star '' s + star '' t
⊢ (s + t)⋆ = s⋆ + t⋆
have simp_rw₁ : Eq (α := Set α) (star '' image2 (fun (x1 x2 : α) ↦ x1 + x2) s t)
  (image2 (fun (x1 x2 : α) ↦ x1 + x2) (star '' s) (star '' t))
Tactic: simp_rw [← image_star, ← image2_add, image_image2, image2_image_left, image2_image_right,
    star_add]
-- Lean 4 proof step from Mathlib.Algebra.Star.Pointwise (goal)
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))
⊢ (s + t)⋆ = s⋆ + t⋆
have simp_rw₂ : Eq (α := Set α) (image2 (fun (a b : α) ↦ (a + b)⋆) s t) (image2 (fun (x1 x2 : α) ↦ x1 + x2) (star '' s) (star '' t))
Tactic: simp_rw [← image_star, ← image2_add, image_image2, image2_image_left, image2_image_right,
    star_add]
-- Lean 4 proof step from Mathlib.Algebra.Star.Pointwise (goal)
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))
⊢ (s + t)⋆ = s⋆ + t⋆
have simp_rw₃ : Eq (α := Set α) (image2 (fun (a b : α) ↦ (a + b)⋆) s t) (image2 (fun (a b : α) ↦ a⋆ + b) s (star '' t))
Tactic: simp_rw [← image_star, ← image2_add, image_image2, image2_image_left, image2_image_right,
    star_add]
-- Lean 4 proof step from Mathlib.Algebra.Star.Pointwise (goal)
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))
⊢ (s + t)⋆ = s⋆ + t⋆
have simp_rw₄ : Eq (α := Set α) (image2 (fun (a b : α) ↦ (a + b)⋆) s t) (image2 (fun (a b : α) ↦ a⋆ + b⋆) s t)
Tactic: simp_rw [← image_star, ← image2_add, image_image2, image2_image_left, image2_image_right,
    star_add]
-- Lean 4 proof step from Mathlib.Algebra.Star.Pointwise (goal)
Goal:
α : Type u_1
s_1 t : Set α
a : α
inst : Star α
inst_1 : TrivialStar α
s : Set α
⊢ star ⁻¹' s = s
have h : ∀ (x : α), x ∈ star ⁻¹' s ↔ x ∈ s
Tactic: ext1
-- Lean 4 proof step from Mathlib.Algebra.Star.Pointwise (goal)
Goal:
α : Type u_1
inst : Group α
inst_1 : StarMul α
s : Set α
⊢ s⁻¹⋆ = s⋆⁻¹
have h : ∀ (x : α), x ∈ s⁻¹⋆ ↔ x ∈ s⋆⁻¹
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Star.Pointwise (goal)
Goal:
α : Type u_1
inst : GroupWithZero α
inst_1 : StarMul α
s : Set α
⊢ s⁻¹⋆ = s⋆⁻¹
have h : ∀ (x : α), x ∈ s⁻¹⋆ ↔ x ∈ s⋆⁻¹
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Star.Pointwise (goal)
Goal:
S : Type u_1
α : Type u_2
inst : InvolutiveStar α
inst_1 : SetLike S α
inst_2 : StarMemClass S α
s : S
⊢ star (↑s : Set α) = (↑s : Set α)
have h : ∀ (x : α), x ∈ star (↑s : Set α) ↔ x ∈ (↑s : Set α)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Star.RingQuot (goal)
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 + c)) (Star.star (b_1 + c))
have add_left : Rel r (Star.star a_1 + Star.star c) (Star.star b_1 + Star.star c)
Tactic: rw [star_add, star_add]
-- Lean 4 proof step from Mathlib.Algebra.Star.RingQuot (goal)
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 * c)) (Star.star (b_1 * c))
have mul_left : Rel r (Star.star c * Star.star a_1) (Star.star c * Star.star b_1)
Tactic: rw [star_mul, star_mul]
-- Lean 4 proof step from Mathlib.Algebra.Star.RingQuot (goal)
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 (a_1 * b_1)) (Star.star (a_1 * c))
have mul_right : Rel r (Star.star b_1 * Star.star a_1) (Star.star c * Star.star a_1)
Tactic: rw [star_mul, star_mul]
-- Lean 4 proof step from Mathlib.Algebra.Star.RingQuot (goal)
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
⊢ Rel r (Star.star a) (Star.star b)
have of : ∀ ⦃x y : R⦄ (h : r x y), Rel r (Star.star x) (Star.star y)
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
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Star.RingQuot (goal)
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)
⊢ Rel r (Star.star a) (Star.star b)
have 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))
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
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Star.RingQuot (goal)
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))
⊢ Rel r (Star.star a) (Star.star b)
have 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))
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
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Star.RingQuot (goal)
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))
⊢ Rel r (Star.star a) (Star.star b)
have 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))
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
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Star.SelfAdjoint (goal)
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)
have refine_1 : ∀ (h : Commute x y), IsSelfAdjoint (x * y)
Tactic: refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Star.SelfAdjoint (goal)
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)
⊢ Commute x y ↔ IsSelfAdjoint (x * y)
have refine_2 : ∀ (h : IsSelfAdjoint (x * y)), Commute x y
Tactic: refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Star.SelfAdjoint (goal)
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
⊢ IsSelfAdjoint (x * y)
have refine_1 : star (x * y) = x * y
Tactic: rw [isSelfAdjoint_iff, star_mul, hx.star_eq, hy.star_eq, h.eq]
-- Lean 4 proof step from Mathlib.Algebra.Star.SelfAdjoint (goal)
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
⊢ IsSelfAdjoint (x * y)
have refine_1₁ : star y * star x = x * y
Tactic: rw [isSelfAdjoint_iff, star_mul, hx.star_eq, hy.star_eq, h.eq]
-- Lean 4 proof step from Mathlib.Algebra.Star.SelfAdjoint (goal)
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
⊢ IsSelfAdjoint (x * y)
have refine_1₂ : star y * x = x * y
Tactic: rw [isSelfAdjoint_iff, star_mul, hx.star_eq, hy.star_eq, h.eq]
-- Lean 4 proof step from Mathlib.Algebra.Star.SelfAdjoint (goal)
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
⊢ IsSelfAdjoint (x * y)
have refine_1₃ : y * x = x * y
Tactic: rw [isSelfAdjoint_iff, star_mul, hx.star_eq, hy.star_eq, h.eq]
-- Lean 4 proof step from Mathlib.Algebra.Star.SelfAdjoint (goal)
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
⊢ IsSelfAdjoint (x * y)
have refine_1₄ : y * x = y * x
Tactic: rw [isSelfAdjoint_iff, star_mul, hx.star_eq, hy.star_eq, h.eq]
-- Lean 4 proof step from Mathlib.Algebra.Star.SelfAdjoint (goal)
Goal:
R : Type u_1
inst : Semigroup R
inst_1 : StarMul R
x : R
hx : IsSelfAdjoint x
z : R
hz : IsSelfAdjoint z
⊢ IsSelfAdjoint (z * x * z)
have nth_rewrite : IsSelfAdjoint (z * x * star z)
Tactic: nth_rewrite 2 [← hz]
-- Lean 4 proof step from Mathlib.Algebra.Star.SelfAdjoint (goal)
Goal:
R : Type u_1
inst : Monoid R
inst_1 : StarMul R
x : R
inst_2 : Invertible x
⊢ IsSelfAdjoint (@Invertible.invOf _ MulOne.toMul MulOne.toOne x _) ↔ IsSelfAdjoint x
have rw : star (@Invertible.invOf _ MulOne.toMul MulOne.toOne x _) = @Invertible.invOf _ MulOne.toMul MulOne.toOne x _ ↔
  IsSelfAdjoint x
Tactic: rw [isSelfAdjoint_iff, isSelfAdjoint_iff, star_invOf, invOf_inj]
-- Lean 4 proof step from Mathlib.Algebra.Star.SelfAdjoint (goal)
Goal:
R : Type u_1
inst : Monoid R
inst_1 : StarMul R
x : R
inst_2 : Invertible x
rw :
  star (@Invertible.invOf _ MulOne.toMul MulOne.toOne x _) = @Invertible.invOf _ MulOne.toMul MulOne.toOne x _ ↔
    IsSelfAdjoint x
⊢ IsSelfAdjoint (@Invertible.invOf _ MulOne.toMul MulOne.toOne x _) ↔ IsSelfAdjoint x
have rw₁ : star (@Invertible.invOf _ MulOne.toMul MulOne.toOne x _) = @Invertible.invOf _ MulOne.toMul MulOne.toOne x _ ↔
  star x = x
Tactic: rw [isSelfAdjoint_iff, isSelfAdjoint_iff, star_invOf, invOf_inj]
-- Lean 4 proof step from Mathlib.Algebra.Star.SelfAdjoint (goal)
Goal:
R : Type u_1
inst : Monoid R
inst_1 : StarMul R
x : R
inst_2 : Invertible x
rw :
  star (@Invertible.invOf _ MulOne.toMul MulOne.toOne x _) = @Invertible.invOf _ MulOne.toMul MulOne.toOne x _ ↔
    IsSelfAdjoint x
rw₁ :
  star (@Invertible.invOf _ MulOne.toMul MulOne.toOne x _) = @Invertible.invOf _ MulOne.toMul MulOne.toOne x _ ↔
    star x = x
⊢ IsSelfAdjoint (@Invertible.invOf _ MulOne.toMul MulOne.toOne x _) ↔ IsSelfAdjoint x
have rw₂ : @Invertible.invOf _ MulOne.toMul MulOne.toOne (star x) _ = @Invertible.invOf _ MulOne.toMul MulOne.toOne x _ ↔
  star x = x
Tactic: rw [isSelfAdjoint_iff, isSelfAdjoint_iff, star_invOf, invOf_inj]
-- Lean 4 proof step from Mathlib.Algebra.Star.SelfAdjoint (goal)
Goal:
R : Type u_1
inst : Monoid R
inst_1 : StarMul R
x : R
inst_2 : Invertible x
rw :
  star (@Invertible.invOf _ MulOne.toMul MulOne.toOne x _) = @Invertible.invOf _ MulOne.toMul MulOne.toOne x _ ↔
    IsSelfAdjoint x
rw₁ :
  star (@Invertible.invOf _ MulOne.toMul MulOne.toOne x _) = @Invertible.invOf _ MulOne.toMul MulOne.toOne x _ ↔
    star x = x
rw₂ :
  @Invertible.invOf _ MulOne.toMul MulOne.toOne (star x) _ = @Invertible.invOf _ MulOne.toMul MulOne.toOne x _ ↔
    star x = x
⊢ IsSelfAdjoint (@Invertible.invOf _ MulOne.toMul MulOne.toOne x _) ↔ IsSelfAdjoint x
have rw₃ : star x = x ↔ star x = x
Tactic: rw [isSelfAdjoint_iff, isSelfAdjoint_iff, star_invOf, invOf_inj]
-- Lean 4 proof step from Mathlib.Algebra.Star.SelfAdjoint (goal)
Goal:
A : Type u_2
a : A
inst : Semiring A
inst_1 : StarRing A
ha : IsSelfAdjoint a
⊢ IsSelfAdjoint a⁻¹ʳ
have rw : star a⁻¹ʳ = a⁻¹ʳ
Tactic: rw [isSelfAdjoint_iff, ← Ring.inverse_star, ha.star_eq]
-- Lean 4 proof step from Mathlib.Algebra.Star.SelfAdjoint (goal)
Goal:
A : Type u_2
a : A
inst : Semiring A
inst_1 : StarRing A
ha : IsSelfAdjoint a
rw : star a⁻¹ʳ = a⁻¹ʳ
⊢ IsSelfAdjoint a⁻¹ʳ
have rw₁ : (star a)⁻¹ʳ = a⁻¹ʳ
Tactic: rw [isSelfAdjoint_iff, ← Ring.inverse_star, ha.star_eq]
-- Lean 4 proof step from Mathlib.Algebra.Star.SelfAdjoint (goal)
Goal:
A : Type u_2
a : A
inst : Semiring A
inst_1 : StarRing A
ha : IsSelfAdjoint a
rw : star a⁻¹ʳ = a⁻¹ʳ
rw₁ : (star a)⁻¹ʳ = a⁻¹ʳ
⊢ IsSelfAdjoint a⁻¹ʳ
have rw₂ : a⁻¹ʳ = a⁻¹ʳ
Tactic: rw [isSelfAdjoint_iff, ← Ring.inverse_star, ha.star_eq]
-- Lean 4 proof step from Mathlib.Algebra.Star.SelfAdjoint (goal)
Goal:
R : Type u_1
A : Type u_2
inst : Monoid R
inst_1 : StarMul R
inst_2 : Star A
inst_3 : MulAction R A
inst_4 : StarModule R A
r : R
hr : IsSelfAdjoint r
hu : IsUnit r
x : A
⊢ IsSelfAdjoint (r • x) ↔ IsSelfAdjoint x
have refine : ∀ (hrx : IsSelfAdjoint (r • x)), IsSelfAdjoint x
Tactic: refine ⟨fun hrx ↦ ?_, .smul hr⟩
-- Lean 4 proof step from Mathlib.Algebra.Star.SelfAdjoint (goal)
Goal:
R : Type u_1
A : Type u_2
inst : Monoid R
inst_1 : StarMul R
inst_2 : Star A
inst_3 : MulAction R A
inst_4 : StarModule R A
r : R
hr : IsSelfAdjoint r
hu : IsUnit r
x : A
hrx : IsSelfAdjoint (r • x)
⊢ IsSelfAdjoint x
have lift : ∀ (r : Rˣ) (hr : IsSelfAdjoint (↑r : R)) (hrx : IsSelfAdjoint ((↑r : R) • x)), IsSelfAdjoint x
Tactic: lift r to Rˣ using hu
Cleared hypotheses: r, hr, hu, hrx
-- Lean 4 proof step from Mathlib.Algebra.Star.SelfAdjoint (goal)
Goal:
R : Type u_1
A : Type u_2
inst : Monoid R
inst_1 : StarMul R
inst_2 : Star A
inst_3 : MulAction R A
inst_4 : StarModule R A
x : A
r : Rˣ
hr : IsSelfAdjoint (↑r : R)
hrx : IsSelfAdjoint ((↑r : R) • x)
⊢ IsSelfAdjoint x
have rw : IsSelfAdjoint (r⁻¹ • r • x)
Tactic: rw [← inv_smul_smul r x]
-- Lean 4 proof step from Mathlib.Algebra.Star.SelfAdjoint (hypothesis)
Goal:
R : Type u_1
A : Type u_2
inst : Monoid R
inst_1 : StarMul R
inst_2 : Star A
inst_3 : MulAction R A
inst_4 : StarModule R A
x : A
r : Rˣ
hr : IsSelfAdjoint (↑r : R)
hrx : IsSelfAdjoint ((↑r : R) • x)
⊢ IsSelfAdjoint (r⁻¹ • r • x)
have hr₁ : IsSelfAdjoint r
Tactic: replace hr : IsSelfAdjoint r := Units.ext hr.star_eq
Cleared hypotheses: hr
-- Lean 4 proof step from Mathlib.Algebra.Star.SelfAdjoint (goal)
Goal:
R : Type u_1
A : Type u_2
inst : AddCommGroup R
inst_1 : StarAddMonoid R
x y : R
hx : star x = -x
hy : star y = -y
⊢ star (x + y) = -(x + y)
have rw : star x + star y = -(x + y)
Tactic: rw [star_add x y, hx, hy, neg_add]
-- Lean 4 proof step from Mathlib.Algebra.Star.SelfAdjoint (goal)
Goal:
R : Type u_1
A : Type u_2
inst : AddCommGroup R
inst_1 : StarAddMonoid R
x y : R
hx : star x = -x
hy : star y = -y
rw : star x + star y = -(x + y)
⊢ star (x + y) = -(x + y)
have rw₁ : -x + star y = -(x + y)
Tactic: rw [star_add x y, hx, hy, neg_add]
-- Lean 4 proof step from Mathlib.Algebra.Star.SelfAdjoint (goal)
Goal:
R : Type u_1
A : Type u_2
inst : AddCommGroup R
inst_1 : StarAddMonoid R
x y : R
hx : star x = -x
hy : star y = -y
rw : star x + star y = -(x + y)
rw₁ : -x + star y = -(x + y)
⊢ star (x + y) = -(x + y)
have rw₂ : -x + -y = -(x + y)
Tactic: rw [star_add x y, hx, hy, neg_add]
-- Lean 4 proof step from Mathlib.Algebra.Star.SelfAdjoint (goal)
Goal:
R : Type u_1
A : Type u_2
inst : AddCommGroup R
inst_1 : StarAddMonoid R
x y : R
hx : star x = -x
hy : star y = -y
rw : star x + star y = -(x + y)
rw₁ : -x + star y = -(x + y)
rw₂ : -x + -y = -(x + y)
⊢ star (x + y) = -(x + y)
have rw₃ : -x + -y = -x + -y
Tactic: rw [star_add x y, hx, hy, neg_add]
-- Lean 4 proof step from Mathlib.Algebra.Star.SelfAdjoint (goal)
Goal:
R : Type u_1
A : Type u_2
inst : Field R
inst_1 : StarRing R
a : ℚ≥0
x : ↥(selfAdjoint R)
⊢ Membership.mem (γ := AddSubgroup R) (selfAdjoint R) (a • (↑x : R))
have rw : Membership.mem (γ := AddSubgroup R) (selfAdjoint R) ((↑a : R) * (↑x : R))
Tactic: rw [NNRat.smul_def]
-- Lean 4 proof step from Mathlib.Algebra.Star.SelfAdjoint (goal)
Goal:
R : Type u_1
A : Type u_2
inst : Field R
inst_1 : StarRing R
a : ℚ
x : ↥(selfAdjoint R)
⊢ Membership.mem (γ := AddSubgroup R) (selfAdjoint R) (a • (↑x : R))
have rw : Membership.mem (γ := AddSubgroup R) (selfAdjoint R) ((↑a : R) * (↑x : R))
Tactic: rw [Rat.smul_def]