awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Star.SelfAdjoint (hypothesis)
Goal:
R : Type u_1
inst : Ring R
inst_1 : StarRing R
x : R
hx : Membership.mem (γ := AddSubgroup R) (skewAdjoint R) x
⊢ Commute (star x) x
have hx₁ : star x = -x
Tactic: simp only [mem_iff] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Algebra.Star.SelfAdjoint (goal)
Goal:
R : Type u_1
A : Type u_2
inst : Star R
inst_1 : TrivialStar R
inst_2 : AddCommGroup A
inst_3 : StarAddMonoid A
inst_4 : Monoid R
inst_5 : DistribMulAction R A
inst_6 : StarModule R A
r : R
x : A
h : Membership.mem (γ := AddSubgroup A) (skewAdjoint A) x
⊢ Membership.mem (γ := AddSubgroup A) (skewAdjoint A) (r • x)
have rw : star (r • x) = -(r • x)
Tactic: rw [mem_iff, star_smul, star_trivial, mem_iff.mp h, smul_neg r]
-- Lean 4 proof step from Mathlib.Algebra.Star.SelfAdjoint (goal)
Goal:
R : Type u_1
A : Type u_2
inst : Star R
inst_1 : TrivialStar R
inst_2 : AddCommGroup A
inst_3 : StarAddMonoid A
inst_4 : Monoid R
inst_5 : DistribMulAction R A
inst_6 : StarModule R A
r : R
x : A
h : Membership.mem (γ := AddSubgroup A) (skewAdjoint A) x
rw : star (r • x) = -(r • x)
⊢ Membership.mem (γ := AddSubgroup A) (skewAdjoint A) (r • x)
have rw₁ : star r • star x = -(r • x)
Tactic: rw [mem_iff, star_smul, star_trivial, mem_iff.mp h, smul_neg r]
-- Lean 4 proof step from Mathlib.Algebra.Star.SelfAdjoint (goal)
Goal:
R : Type u_1
A : Type u_2
inst : Star R
inst_1 : TrivialStar R
inst_2 : AddCommGroup A
inst_3 : StarAddMonoid A
inst_4 : Monoid R
inst_5 : DistribMulAction R A
inst_6 : StarModule R A
r : R
x : A
h : Membership.mem (γ := AddSubgroup A) (skewAdjoint A) x
rw : star (r • x) = -(r • x)
rw₁ : star r • star x = -(r • x)
⊢ Membership.mem (γ := AddSubgroup A) (skewAdjoint A) (r • x)
have rw₂ : r • star x = -(r • x)
Tactic: rw [mem_iff, star_smul, star_trivial, mem_iff.mp h, smul_neg r]
-- Lean 4 proof step from Mathlib.Algebra.Star.SelfAdjoint (goal)
Goal:
R : Type u_1
A : Type u_2
inst : Star R
inst_1 : TrivialStar R
inst_2 : AddCommGroup A
inst_3 : StarAddMonoid A
inst_4 : Monoid R
inst_5 : DistribMulAction R A
inst_6 : StarModule R A
r : R
x : A
h : Membership.mem (γ := AddSubgroup A) (skewAdjoint A) x
rw : star (r • x) = -(r • x)
rw₁ : star r • star x = -(r • x)
rw₂ : r • star x = -(r • x)
⊢ Membership.mem (γ := AddSubgroup A) (skewAdjoint A) (r • x)
have rw₃ : r • -x = -(r • x)
Tactic: rw [mem_iff, star_smul, star_trivial, mem_iff.mp h, smul_neg r]
-- Lean 4 proof step from Mathlib.Algebra.Star.SelfAdjoint (goal)
Goal:
R : Type u_1
A : Type u_2
inst : Star R
inst_1 : TrivialStar R
inst_2 : AddCommGroup A
inst_3 : StarAddMonoid A
inst_4 : Monoid R
inst_5 : DistribMulAction R A
inst_6 : StarModule R A
r : R
x : A
h : Membership.mem (γ := AddSubgroup A) (skewAdjoint A) x
rw : star (r • x) = -(r • x)
rw₁ : star r • star x = -(r • x)
rw₂ : r • star x = -(r • x)
rw₃ : r • -x = -(r • x)
⊢ Membership.mem (γ := AddSubgroup A) (skewAdjoint A) (r • x)
have rw₄ : -(r • x) = -(r • x)
Tactic: rw [mem_iff, star_smul, star_trivial, mem_iff.mp h, smul_neg r]
-- Lean 4 proof step from Mathlib.Algebra.Star.SelfAdjoint (goal)
Goal:
R : Type u_1
A : Type u_2
inst : Mul R
inst_1 : StarMul R
x : R
inst_2 : IsStarNormal x
⊢ star (star x) * star x = star x * star (star x)
have rw : x * star x = star x * x
Tactic: rw [star_star, star_comm_self']
-- Lean 4 proof step from Mathlib.Algebra.Star.SelfAdjoint (goal)
Goal:
R : Type u_1
A : Type u_2
inst : Mul R
inst_1 : StarMul R
x : R
inst_2 : IsStarNormal x
rw : x * star x = star x * x
⊢ star (star x) * star x = star x * star (star x)
have rw₁ : x * star x = x * star x
Tactic: rw [star_star, star_comm_self']
-- Lean 4 proof step from Mathlib.Algebra.Star.SelfAdjoint (goal)
Goal:
R : Type u_1
A : Type u_2
inst : NonUnitalNonAssocRing R
inst_1 : StarAddMonoid R
x : R
inst_2 : IsStarNormal x
⊢ star (-x) * -x = -x * star (-x)
have simp_rw : -star x * -x = -x * -star x
Tactic: simp_rw [star_neg, neg_mul_neg, star_comm_self']
-- Lean 4 proof step from Mathlib.Algebra.Star.SelfAdjoint (goal)
Goal:
R : Type u_1
A : Type u_2
inst : NonUnitalNonAssocRing R
inst_1 : StarAddMonoid R
x : R
inst_2 : IsStarNormal x
simp_rw : -star x * -x = -x * -star x
⊢ star (-x) * -x = -x * star (-x)
have simp_rw₁ : star x * x = x * star x
Tactic: simp_rw [star_neg, neg_mul_neg, star_comm_self']
-- Lean 4 proof step from Mathlib.Algebra.Star.SelfAdjoint (goal)
Goal:
R : Type u_1
A : Type u_2
inst : Mul R
inst_1 : StarMul R
inst_2 : TrivialStar R
x : R
⊢ Commute (star x) x
have rw : Commute x x
Tactic: rw [star_trivial]
-- Lean 4 proof step from Mathlib.Algebra.Star.SelfAdjoint (goal)
Goal:
R : Type u_1
inst : NonUnitalNonAssocSemiring R
inst_1 : StarRing R
a b : R
hab : Commute a (star b)
ha : IsStarNormal a
hb : IsStarNormal b
⊢ IsStarNormal (a + b)
have rw : ∀ (ha : Commute (star a) a) (hb : Commute (star b) b), Commute (star (a + b)) (a + b)
Tactic: rw [isStarNormal_iff] at ha hb ⊢
Cleared hypotheses: ha, hb
-- Lean 4 proof step from Mathlib.Algebra.Star.SelfAdjoint (hypothesis)
Goal:
R : Type u_1
inst : NonUnitalNonAssocSemiring R
inst_1 : StarRing R
a b : R
hab : Commute a (star b)
ha : Commute (star a) a
hb : Commute (star b) b
⊢ Commute (star (a + b)) (a + b)
have this : Commute (star a) b
Tactic: have := _root_.star_star b ▸ hab.star_star
-- Lean 4 proof step from Mathlib.Algebra.Star.SelfAdjoint (goal)
Goal:
R : Type u_1
inst : NonUnitalNonAssocSemiring R
inst_1 : StarRing R
a b : R
hab : Commute a (star b)
ha : Commute (star a) a
hb : Commute (star b) b
this : Commute (star a) b
⊢ Commute (star (a + b)) (a + b)
have simp : star a * a + star b * a + (star a * b + star b * b) = a * star a + b * star a + (a * star b + b * star b)
Tactic: simp only [star_add, commute_iff_eq, mul_add, add_mul]
-- Lean 4 proof step from Mathlib.Algebra.Star.SelfAdjoint (goal)
Goal:
R : Type u_1
inst : NonUnitalNonAssocSemiring R
inst_1 : StarRing R
a b : R
hab : Commute a (star b)
ha : Commute (star a) a
hb : Commute (star b) b
this : Commute (star a) b
⊢ star a * a + star b * a + (star a * b + star b * b) = a * star a + b * star a + (a * star b + b * star b)
have rw : a * star a + star b * a + (star a * b + star b * b) = a * star a + b * star a + (a * star b + b * star b)
Tactic: rw [ha.eq, hb.eq, add_add_add_comm, hab.eq, this.eq]
-- Lean 4 proof step from Mathlib.Algebra.Star.SelfAdjoint (goal)
Goal:
R : Type u_1
inst : NonUnitalNonAssocSemiring R
inst_1 : StarRing R
a b : R
hab : Commute a (star b)
ha : Commute (star a) a
hb : Commute (star b) b
this : Commute (star a) b
rw : a * star a + star b * a + (star a * b + star b * b) = a * star a + b * star a + (a * star b + b * star b)
⊢ star a * a + star b * a + (star a * b + star b * b) = a * star a + b * star a + (a * star b + b * star b)
have rw₁ : a * star a + star b * a + (star a * b + b * star b) = a * star a + b * star a + (a * star b + b * star b)
Tactic: rw [ha.eq, hb.eq, add_add_add_comm, hab.eq, this.eq]
-- Lean 4 proof step from Mathlib.Algebra.Star.SelfAdjoint (goal)
Goal:
R : Type u_1
inst : NonUnitalNonAssocSemiring R
inst_1 : StarRing R
a b : R
hab : Commute a (star b)
ha : Commute (star a) a
hb : Commute (star b) b
this : Commute (star a) b
rw : a * star a + star b * a + (star a * b + star b * b) = a * star a + b * star a + (a * star b + b * star b)
rw₁ : a * star a + star b * a + (star a * b + b * star b) = a * star a + b * star a + (a * star b + b * star b)
⊢ star a * a + star b * a + (star a * b + star b * b) = a * star a + b * star a + (a * star b + b * star b)
have rw₂ : a * star a + star a * b + (star b * a + b * star b) = a * star a + b * star a + (a * star b + b * star b)
Tactic: rw [ha.eq, hb.eq, add_add_add_comm, hab.eq, this.eq]
-- Lean 4 proof step from Mathlib.Algebra.Star.SelfAdjoint (goal)
Goal:
R : Type u_1
inst : NonUnitalNonAssocSemiring R
inst_1 : StarRing R
a b : R
hab : Commute a (star b)
ha : Commute (star a) a
hb : Commute (star b) b
this : Commute (star a) b
rw : a * star a + star b * a + (star a * b + star b * b) = a * star a + b * star a + (a * star b + b * star b)
rw₁ : a * star a + star b * a + (star a * b + b * star b) = a * star a + b * star a + (a * star b + b * star b)
rw₂ : a * star a + star a * b + (star b * a + b * star b) = a * star a + b * star a + (a * star b + b * star b)
⊢ star a * a + star b * a + (star a * b + star b * b) = a * star a + b * star a + (a * star b + b * star b)
have rw₃ : a * star a + star a * b + (star b * a + b * star b) = a * star a + b * star a + (star b * a + b * star b)
Tactic: rw [ha.eq, hb.eq, add_add_add_comm, hab.eq, this.eq]
-- Lean 4 proof step from Mathlib.Algebra.Star.SelfAdjoint (goal)
Goal:
R : Type u_1
inst : NonUnitalNonAssocSemiring R
inst_1 : StarRing R
a b : R
hab : Commute a (star b)
ha : Commute (star a) a
hb : Commute (star b) b
this : Commute (star a) b
rw : a * star a + star b * a + (star a * b + star b * b) = a * star a + b * star a + (a * star b + b * star b)
rw₁ : a * star a + star b * a + (star a * b + b * star b) = a * star a + b * star a + (a * star b + b * star b)
rw₂ : a * star a + star a * b + (star b * a + b * star b) = a * star a + b * star a + (a * star b + b * star b)
rw₃ : a * star a + star a * b + (star b * a + b * star b) = a * star a + b * star a + (star b * a + b * star b)
⊢ star a * a + star b * a + (star a * b + star b * b) = a * star a + b * star a + (a * star b + b * star b)
have rw₄ : a * star a + b * star a + (star b * a + b * star b) = a * star a + b * star a + (star b * a + b * star b)
Tactic: rw [ha.eq, hb.eq, add_add_add_comm, hab.eq, this.eq]
-- Lean 4 proof step from Mathlib.Algebra.Star.SelfAdjoint (hypothesis)
Goal:
R : Type u_1
inst : NonUnitalNonAssocRing R
inst_1 : StarRing R
a b : R
ha : IsSelfAdjoint a
hb : IsSelfAdjoint b
hab : a * b = 0
⊢ Commute a b
have this : b * a = 0
Tactic: have : b * a = 0 := by simpa [ha.star_eq, hb.star_eq] using congr(star $hab)
-- Lean 4 proof step from Mathlib.Algebra.Star.StarAlgHom (goal)
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : Monoid R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : DistribMulAction R A
inst_3 : Star A
inst_4 : NonUnitalNonAssocSemiring B
inst_5 : DistribMulAction R B
inst_6 : Star B
f : A →⋆ₙₐ[R] B
h₁ :
  ∀ (m : R) (x : A),
    (f : (a : A) → B) (m • x) =
      HSMul.hSMul (α := R) (β := B) ((MonoidHom.id R : (a : R) → R) m : R) ((f : (a : A) → B) x : B)
h₂ :
  { toFun := (⇑f : (a : A) → B), map_smul' := h₁ :
          MulActionHom (M := R) (N := R) (⇑(MonoidHom.id R) : (a : R) → R) A B }.toFun
      0 =
    0
h₃ :
  ∀ (x y : A),
    { toFun := (⇑f : (a : A) → B), map_smul' := h₁ :
            MulActionHom (M := R) (N := R) (⇑(MonoidHom.id R) : (a : R) → R) A B }.toFun
        (x + y) =
      { toFun := (⇑f : (a : A) → B), map_smul' := h₁ :
              MulActionHom (M := R) (N := R) (⇑(MonoidHom.id R) : (a : R) → R) A B }.toFun
          x +
        { toFun := (⇑f : (a : A) → B), map_smul' := h₁ :
              MulActionHom (M := R) (N := R) (⇑(MonoidHom.id R) : (a : R) → R) A B }.toFun
          y
h₄ :
  ∀ (x y : A),
    { toFun := (⇑f : (a : A) → B), map_smul' := h₁, map_zero' := h₂, map_add' := h₃ : A →+[R] B }.toFun (x * y) =
      { toFun := (⇑f : (a : A) → B), map_smul' := h₁, map_zero' := h₂, map_add' := h₃ : A →+[R] B }.toFun x *
        { toFun := (⇑f : (a : A) → B), map_smul' := h₁, map_zero' := h₂, map_add' := h₃ : A →+[R] B }.toFun y
h₅ :
  ∀ (a : A),
    { toFun := (⇑f : (a : A) → B), map_smul' := h₁, map_zero' := h₂, map_add' := h₃, map_mul' := h₄ : A →ₙₐ[R] B }.toFun
        (star a) =
      star
        ({ toFun := (⇑f : (a : A) → B), map_smul' := h₁, map_zero' := h₂, map_add' := h₃, map_mul' := h₄ :
              A →ₙₐ[R] B }.toFun
          a)
⊢ { toFun := (⇑f : (a : A) → B), map_smul' := h₁, map_zero' := h₂, map_add' := h₃, map_mul' := h₄, map_star' := h₅ :
      A →⋆ₙₐ[R] B } =
    f
have h : ∀ (x : A),
  Eq.{u_3 + 1} (α := B)
    (({ toFun := (⇑f : (a : A) → B), map_smul' := h₁, map_zero' := h₂, map_add' := h₃, map_mul' := h₄, map_star' := h₅ :
            A →⋆ₙₐ[R] B } :
          (a : A) → B)
        x :
      B)
    ((f : (a : A) → B) x : B)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Star.StarAlgHom (goal)
Goal:
R : Type u_2
A : Type u_3
B : Type u_4
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Star A
inst_4 : Semiring B
inst_5 : Algebra R B
inst_6 : Star B
f : A →⋆ₐ[R] B
h₁ : Eq.{u_4 + 1} (α := B) ((f : (a : A) → B) 1 : B) (1 : B)
h₂ :
  ∀ (x y : A),
    { toFun := (⇑f : (a : A) → B), map_one' := h₁ : OneHom A B }.toFun (x * y) =
      { toFun := (⇑f : (a : A) → B), map_one' := h₁ : OneHom A B }.toFun x *
        { toFun := (⇑f : (a : A) → B), map_one' := h₁ : OneHom A B }.toFun y
h₃ : (↑{ toFun := (⇑f : (a : A) → B), map_one' := h₁, map_mul' := h₂ : A →* B } : OneHom A B).toFun 0 = 0
h₄ :
  ∀ (x y : A),
    (↑{ toFun := (⇑f : (a : A) → B), map_one' := h₁, map_mul' := h₂ : A →* B } : OneHom A B).toFun (x + y) =
      (↑{ toFun := (⇑f : (a : A) → B), map_one' := h₁, map_mul' := h₂ : A →* B } : OneHom A B).toFun x +
        (↑{ toFun := (⇑f : (a : A) → B), map_one' := h₁, map_mul' := h₂ : A →* B } : OneHom A B).toFun y
h₅ :
  ∀ (r : R),
    (↑(↑{ toFun := (⇑f : (a : A) → B), map_one' := h₁, map_mul' := h₂, map_zero' := h₃, map_add' := h₄ : A →+* B } :
                A →* B) :
            OneHom A B).toFun
        ((algebraMap R A : (a : R) → A) r) =
      (algebraMap R B : (a : R) → B) r
h₆ :
  ∀ (x : A),
    (↑(↑{ toFun := (⇑f : (a : A) → B), map_one' := h₁, map_mul' := h₂, map_zero' := h₃, map_add' := h₄,
                      commutes' := h₅ : A →ₐ[R] B }.toRingHom :
                A →* B) :
            OneHom A B).toFun
        (star x) =
      star
        ((↑(↑{ toFun := (⇑f : (a : A) → B), map_one' := h₁, map_mul' := h₂, map_zero' := h₃, map_add' := h₄,
                        commutes' := h₅ : A →ₐ[R] B }.toRingHom :
                  A →* B) :
              OneHom A B).toFun
          x)
⊢ { toFun := (⇑f : (a : A) → B), map_one' := h₁, map_mul' := h₂, map_zero' := h₃, map_add' := h₄, commutes' := h₅,
      map_star' := h₆ : A →⋆ₐ[R] B } =
    f
have h : ∀ (x : A),
  Eq.{u_4 + 1} (α := B)
    (({ toFun := (⇑f : (a : A) → B), map_one' := h₁, map_mul' := h₂, map_zero' := h₃, map_add' := h₄, commutes' := h₅,
            map_star' := h₆ : A →⋆ₐ[R] B } :
          (a : A) → B)
        x :
      B)
    ((f : (a : A) → B) x : B)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Star.StarAlgHom (goal)
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
inst : Monoid R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : DistribMulAction R A
inst_3 : Star A
inst_4 : NonUnitalNonAssocSemiring B
inst_5 : DistribMulAction R B
inst_6 : Star B
inst_7 : NonUnitalNonAssocSemiring C
inst_8 : DistribMulAction R C
inst_9 : Star C
f : A →⋆ₙₐ[R] B
g : A →⋆ₙₐ[R] C
⊢ comp (fst R B C) (f.prod g) = f
have h : ∀ (x : A), Eq.{u_3 + 1} (α := B) ((comp (fst R B C) (f.prod g) : (a : A) → B) x : B) ((f : (a : A) → B) x : B)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Star.StarAlgHom (goal)
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
inst : Monoid R
inst_1 : NonUnitalNonAssocSemiring A
inst_2 : DistribMulAction R A
inst_3 : Star A
inst_4 : NonUnitalNonAssocSemiring B
inst_5 : DistribMulAction R B
inst_6 : Star B
inst_7 : NonUnitalNonAssocSemiring C
inst_8 : DistribMulAction R C
inst_9 : Star C
f : A →⋆ₙₐ[R] B
g : A →⋆ₙₐ[R] C
⊢ comp (snd R B C) (f.prod g) = g
have h : ∀ (x : A), Eq.{u_4 + 1} (α := C) ((comp (snd R B C) (f.prod g) : (a : A) → C) x : C) ((g : (a : A) → C) x : C)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Star.StarAlgHom (goal)
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Star A
inst_4 : Semiring B
inst_5 : Algebra R B
inst_6 : Star B
inst_7 : Semiring C
inst_8 : Algebra R C
inst_9 : Star C
f : A →⋆ₐ[R] B
g : A →⋆ₐ[R] C
⊢ comp (fst R B C) (f.prod g) = f
have h : ∀ (x : A), Eq.{u_3 + 1} (α := B) ((comp (fst R B C) (f.prod g) : (a : A) → B) x : B) ((f : (a : A) → B) x : B)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Star.StarAlgHom (goal)
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Star A
inst_4 : Semiring B
inst_5 : Algebra R B
inst_6 : Star B
inst_7 : Semiring C
inst_8 : Algebra R C
inst_9 : Star C
f : A →⋆ₐ[R] B
g : A →⋆ₐ[R] C
⊢ comp (snd R B C) (f.prod g) = g
have h : ∀ (x : A), Eq.{u_4 + 1} (α := C) ((comp (snd R B C) (f.prod g) : (a : A) → C) x : C) ((g : (a : A) → C) x : C)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Star.StarAlgHom (goal)
Goal:
F : Type u_1
R : Type u_2
A : Type u_3
B : Type u_4
C : Type u_5
inst : Add A
inst_1 : Add B
inst_2 : Mul A
inst_3 : Mul B
inst_4 : SMul R A
inst_5 : SMul R B
inst_6 : Star A
inst_7 : Star B
inst_8 : Add C
inst_9 : Mul C
inst_10 : SMul R C
inst_11 : Star C
f g : A ≃⋆ₐ[R] B
h₁ : f.toFun = g.toFun
h₂ : f.invFun = g.invFun
⊢ f = g
have rcases : ∀ (toFun : A → B) (invFun : B → A) (left_inv : Function.LeftInverse invFun toFun)
  (right_inv : Function.RightInverse invFun toFun)
  (map_mul' :
    ∀ (x y : A),
      { toFun := toFun, invFun := invFun, left_inv := left_inv, right_inv := right_inv : A ≃ B }.toFun (x * y) =
        { toFun := toFun, invFun := invFun, left_inv := left_inv, right_inv := right_inv : A ≃ B }.toFun x *
          { toFun := toFun, invFun := invFun, left_inv := left_inv, right_inv := right_inv : A ≃ B }.toFun y)
  (map_add' :
    ∀ (x y : A),
      { toFun := toFun, invFun := invFun, left_inv := left_inv, right_inv := right_inv : A ≃ B }.toFun (x + y) =
        { toFun := toFun, invFun := invFun, left_inv := left_inv, right_inv := right_inv : A ≃ B }.toFun x +
          { toFun := toFun, invFun := invFun, left_inv := left_inv, right_inv := right_inv : A ≃ B }.toFun y)
  (map_star' :
    ∀ (a : A),
      { toFun := toFun, invFun := invFun, left_inv := left_inv, right_inv := right_inv, map_mul' := map_mul',
              map_add' := map_add' : A ≃+* B }.toFun
          (star a) =
        star
          ({ toFun := toFun, invFun := invFun, left_inv := left_inv, right_inv := right_inv, map_mul' := map_mul',
                map_add' := map_add' : A ≃+* B }.toFun
            a))
  (map_smul' :
    ∀ (r : R) (a : A),
      { toFun := toFun, invFun := invFun, left_inv := left_inv, right_inv := right_inv, map_mul' := map_mul',
              map_add' := map_add', map_star' := map_star' : A ≃⋆+* B }.toFun
          (r • a) =
        r •
          { toFun := toFun, invFun := invFun, left_inv := left_inv, right_inv := right_inv, map_mul' := map_mul',
                map_add' := map_add', map_star' := map_star' : A ≃⋆+* B }.toFun
            a)
  (h₁ :
    { toFun := toFun, invFun := invFun, left_inv := left_inv, right_inv := right_inv, map_mul' := map_mul',
          map_add' := map_add', map_star' := map_star', map_smul' := map_smul' : A ≃⋆ₐ[R] B }.toFun =
      g.toFun)
  (h₂ :
    { toFun := toFun, invFun := invFun, left_inv := left_inv, right_inv := right_inv, map_mul' := map_mul',
          map_add' := map_add', map_star' := map_star', map_smul' := map_smul' : A ≃⋆ₐ[R] B }.invFun =
      g.invFun),
  { toFun := toFun, invFun := invFun, left_inv := left_inv, right_inv := right_inv, map_mul' := map_mul',
      map_add' := map_add', map_star' := map_star', map_smul' := map_smul' : A ≃⋆ₐ[R] B } =
    g
Tactic: rcases f with ⟨⟨⟨⟨_, _, _⟩, _⟩, _⟩, _⟩
Cleared hypotheses: f, h₁, h₂
-- Lean 4 proof step from Mathlib.Algebra.Star.StarAlgHom (goal)
Goal:
F : Type u_1
R : Type u_2
A : Type u_3
B : Type u_4
C : Type u_5
inst : Add A
inst_1 : Add B
inst_2 : Mul A
inst_3 : Mul B
inst_4 : SMul R A
inst_5 : SMul R B
inst_6 : Star A
inst_7 : Star B
inst_8 : Add C
inst_9 : Mul C
inst_10 : SMul R C
inst_11 : Star C
e₁ : A ≃⋆ₐ[R] B
e₂ : B ≃⋆ₐ[R] C
r : R
a : A
⊢ e₂.toFun (e₁.toFun (r • a)) = r • e₂.toFun (e₁.toFun a)
have rw : e₂.toFun (r • e₁.toFun a) = r • e₂.toFun (e₁.toFun a)
Tactic: rw [e₁.map_smul', e₂.map_smul']
-- Lean 4 proof step from Mathlib.Algebra.Star.StarAlgHom (goal)
Goal:
F : Type u_1
R : Type u_2
A : Type u_3
B : Type u_4
C : Type u_5
inst : Add A
inst_1 : Add B
inst_2 : Mul A
inst_3 : Mul B
inst_4 : SMul R A
inst_5 : SMul R B
inst_6 : Star A
inst_7 : Star B
inst_8 : Add C
inst_9 : Mul C
inst_10 : SMul R C
inst_11 : Star C
e₁ : A ≃⋆ₐ[R] B
e₂ : B ≃⋆ₐ[R] C
r : R
a : A
rw : e₂.toFun (r • e₁.toFun a) = r • e₂.toFun (e₁.toFun a)
⊢ e₂.toFun (e₁.toFun (r • a)) = r • e₂.toFun (e₁.toFun a)
have rw₁ : r • e₂.toFun (e₁.toFun a) = r • e₂.toFun (e₁.toFun a)
Tactic: rw [e₁.map_smul', e₂.map_smul']
-- Lean 4 proof step from Mathlib.Algebra.Star.StarAlgHom (goal)
Goal:
F : Type u_1
R_1 : Type u_2
A_1 : Type u_3
B_1 : Type u_4
C : Type u_5
inst : Add A_1
inst_1 : Add B_1
inst_2 : Mul A_1
inst_3 : Mul B_1
inst_4 : SMul R_1 A_1
inst_5 : SMul R_1 B_1
inst_6 : Star A_1
inst_7 : Star B_1
inst_8 : Add C
inst_9 : Mul C
inst_10 : SMul R_1 C
inst_11 : Star C
R : Type u_6
A : Type u_7
B : Type u_8
inst_12 : CommSemiring R
inst_13 : Semiring A
inst_14 : Semiring B
inst_15 : Algebra R A
inst_16 : Algebra R B
inst_17 : Star A
inst_18 : Star B
f : A ≃⋆ₐ[R] B
r : R
⊢ f.toFun ((algebraMap R A : (a : R) → A) r) = (algebraMap R B : (a : R) → B) r
have simp_rw : r • f.toFun 1 = HSMul.hSMul (β := B) r 1
Tactic: simp_rw [Algebra.algebraMap_eq_smul_one', map_smul']
-- Lean 4 proof step from Mathlib.Algebra.Star.StarProjection (goal)
Goal:
R : Type u_1
p q : R
inst : NonUnitalNonAssocSemiring R
inst_1 : StarRing R
hp : IsStarProjection p
hq : IsStarProjection q
hpq : p * q = 0
⊢ p * q + q * p = 0
have rw : q * p = 0
Tactic: rw [hpq, zero_add]
-- Lean 4 proof step from Mathlib.Algebra.Star.StarProjection (goal)
Goal:
R : Type u_1
inst : NonUnitalRing R
inst_1 : StarRing R
inst_2 : IsAddTorsionFree R
p q : R
hp : IsStarProjection p
hq : IsStarProjection q
⊢ IsStarProjection (q - p) ↔ p * q = p
have rw : (p * q = p ∧ q * p = p) ∧ IsSelfAdjoint (q - p) ↔ p * q = p
Tactic: rw [isStarProjection_iff, hp.isIdempotentElem.sub_iff hq.isIdempotentElem]
-- Lean 4 proof step from Mathlib.Algebra.Star.StarProjection (goal)
Goal:
R : Type u_1
inst : NonUnitalRing R
inst_1 : StarRing R
inst_2 : IsAddTorsionFree R
p q : R
hp : IsStarProjection p
hq : IsStarProjection q
⊢ (p * q = p ∧ q * p = p) ∧ IsSelfAdjoint (q - p) ↔ p * q = p
have simp_rw : p * q = p ∧ q * p = p ↔ p * q = p
Tactic: simp_rw [hq.isSelfAdjoint.sub hp.isSelfAdjoint, and_true]
-- Lean 4 proof step from Mathlib.Algebra.Star.StarProjection (goal)
Goal:
R : Type u_1
inst : NonUnitalRing R
inst_1 : StarRing R
inst_2 : IsAddTorsionFree R
p q : R
hp : IsStarProjection p
hq : IsStarProjection q
⊢ p * q = p ∧ q * p = p ↔ p * q = p
have nth_rw : p * q = p ∧ q * star p = p ↔ p * q = p
Tactic: nth_rw 3 [← hp.isSelfAdjoint]
-- Lean 4 proof step from Mathlib.Algebra.Star.StarProjection (goal)
Goal:
R : Type u_1
inst : NonUnitalRing R
inst_1 : StarRing R
inst_2 : IsAddTorsionFree R
p q : R
hp : IsStarProjection p
hq : IsStarProjection q
⊢ p * q = p ∧ q * star p = p ↔ p * q = p
have nth_rw : p * q = p ∧ star q * star p = p ↔ p * q = p
Tactic: nth_rw 2 [← hq.isSelfAdjoint]
-- Lean 4 proof step from Mathlib.Algebra.Star.StarProjection (goal)
Goal:
R : Type u_1
inst : NonUnitalRing R
inst_1 : StarRing R
inst_2 : IsAddTorsionFree R
p q : R
hp : IsStarProjection p
hq : IsStarProjection q
⊢ p * q = p ∧ star q * star p = p ↔ p * q = p
have rw : p = p * q ∧ p = p * q ↔ p = p * q
Tactic: rw [← star_mul, star_eq_iff_star_eq, hp.isSelfAdjoint, eq_comm]
-- Lean 4 proof step from Mathlib.Algebra.Star.StarProjection (goal)
Goal:
R : Type u_1
inst : NonUnitalRing R
inst_1 : StarRing R
inst_2 : IsAddTorsionFree R
p q : R
hp : IsStarProjection p
hq : IsStarProjection q
⊢ IsStarProjection (q - p) ↔ q * p = p
have rw : IsStarProjection (q - p) ↔ star (q * p) = star p
Tactic: rw [← star_inj]