awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Star.StarAlgHom
Goal:
R : Type u_2
A : Type u_3
B : Type u_4
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
e : A ≃⋆ₐ[R] B
⊢ e.toRingEquiv = StarRingEquiv.toRingEquiv (↑e : A ≃⋆+* B)

Tactic:
rfl

Premises used: RingEquivClass.toRingEquiv, EquivLike.toEquiv, rfl
-- Module: Mathlib.Algebra.Star.StarAlgHom
Goal:
R : Type u_2
A : Type u_3
B : Type u_4
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
f g : A ≃⋆ₐ[R] B
h : ∀ (a : A), Eq.{u_4 + 1} (α := B) ((f : (a : A) → B) a : B) ((g : (a : A) → B) a : B)
⊢ f = g

Tactic:
DFunLike.ext f g h

Premises used: DFunLike.ext
-- Module: Mathlib.Algebra.Star.StarAlgHom
Goal:
R : Type u_2
A : Type u_3
inst : Add A
inst_1 : Mul A
inst_2 : SMul R A
inst_3 : Star A
⊢ Eq.{u_3 + 1} (α := (a : A) → A) (⇑refl : (a : A) → A) id

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Star.StarAlgHom
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
r : R
b : B
⊢ e.symm.toFun (r • b) = r • e.symm.toFun b

Tactic:
simpa only [apply_inv_apply, inv_apply_apply] using
        congr_arg (inv e) (map_smul e r (inv e b)).symm

Premises used: EquivLike.inv_apply_apply, congr_arg, EquivLike.inv, Eq.symm, EquivLike.apply_inv_apply, map_smul
-- Module: Mathlib.Algebra.Star.StarAlgHom
Goal:
R : Type u_2
A : Type u_3
B : Type u_4
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
e : A ≃⋆ₐ[R] B
⊢ inv e = (⇑e.symm : (a : B) → A)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Star.StarAlgHom
Goal:
R : Type u_2
A : Type u_3
B : Type u_4
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
e : A ≃⋆ₐ[R] B
⊢ e.symm.symm = e

Tactic:
rfl

Premises used: StarRingEquiv.symm, StarAlgEquiv.symm, Equiv.symm, RingEquiv.symm, rfl
-- Module: Mathlib.Algebra.Star.StarAlgHom
Goal:
R : Type u_2
A : Type u_3
B : Type u_4
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
⊢ Function.Bijective (α := A ≃⋆ₐ[R] B) symm

Tactic:
Function.bijective_iff_has_inverse.mpr ⟨_, symm_symm, symm_symm⟩

Premises used: Iff.mpr, Function.bijective_iff_has_inverse, StarAlgEquiv.symm_symm, And.intro, Exists.intro
-- Module: Mathlib.Algebra.Star.StarAlgHom
Goal:
R : Type u_2
A : Type u_3
B : Type u_4
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
e : A ≃⋆+* B
h : ∀ (r : R) (a : A), e.toFun (r • a) = r • e.toFun a
⊢ Eq (α := (a : A) → B) (⇑{ toStarRingEquiv := e, map_smul' := h : A ≃⋆ₐ[R] B } : (a : A) → B) (⇑e : (a : A) → B)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Star.StarAlgHom
Goal:
R : Type u_2
A : Type u_3
B : Type u_4
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
e : A ≃⋆ₐ[R] B
e' : B → A
h₁ : Function.LeftInverse e' (⇑e : (a : A) → B)
h₂ : Function.RightInverse e' (⇑e : (a : A) → B)
h₃ :
  ∀ (x y : A),
    { toFun := (⇑e : (a : A) → B), invFun := e', left_inv := h₁, right_inv := h₂ : A ≃ B }.toFun (x * y) =
      { toFun := (⇑e : (a : A) → B), invFun := e', left_inv := h₁, right_inv := h₂ : A ≃ B }.toFun x *
        { toFun := (⇑e : (a : A) → B), invFun := e', left_inv := h₁, right_inv := h₂ : A ≃ B }.toFun y
h₄ :
  ∀ (x y : A),
    { toFun := (⇑e : (a : A) → B), invFun := e', left_inv := h₁, right_inv := h₂ : A ≃ B }.toFun (x + y) =
      { toFun := (⇑e : (a : A) → B), invFun := e', left_inv := h₁, right_inv := h₂ : A ≃ B }.toFun x +
        { toFun := (⇑e : (a : A) → B), invFun := e', left_inv := h₁, right_inv := h₂ : A ≃ B }.toFun y
h₅ :
  ∀ (a : A),
    { toFun := (⇑e : (a : A) → B), invFun := e', left_inv := h₁, right_inv := h₂, map_mul' := h₃, map_add' := h₄ :
            A ≃+* B }.toFun
        (star a) =
      star
        ({ toFun := (⇑e : (a : A) → B), invFun := e', left_inv := h₁, right_inv := h₂, map_mul' := h₃, map_add' := h₄ :
              A ≃+* B }.toFun
          a)
h₆ :
  ∀ (r : R) (a : A),
    { toFun := (⇑e : (a : A) → B), invFun := e', left_inv := h₁, right_inv := h₂, map_mul' := h₃, map_add' := h₄,
            map_star' := h₅ : A ≃⋆+* B }.toFun
        (r • a) =
      r •
        { toFun := (⇑e : (a : A) → B), invFun := e', left_inv := h₁, right_inv := h₂, map_mul' := h₃, map_add' := h₄,
              map_star' := h₅ : A ≃⋆+* B }.toFun
          a
⊢ { toFun := (⇑e : (a : A) → B), invFun := e', left_inv := h₁, right_inv := h₂, map_mul' := h₃, map_add' := h₄,
      map_star' := h₅, map_smul' := h₆ : A ≃⋆ₐ[R] B } =
    e

Tactic:
ext fun _ => rfl

Premises used: StarAlgEquiv.ext, rfl
-- Module: Mathlib.Algebra.Star.StarAlgHom
Goal:
R : Type u_2
A : Type u_3
B : Type u_4
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
e : A ≃⋆+* B
h₁ : ∀ (r : R) (a : A), e.toFun (r • a) = r • e.toFun a
⊢ { toStarRingEquiv := e, map_smul' := h₁ : A ≃⋆ₐ[R] B }.symm = { toStarRingEquiv := e.symm, map_smul' := ⋯ }

Tactic:
rfl

Premises used: StarAlgEquiv.symm, rfl
-- Module: Mathlib.Algebra.Star.StarAlgHom
Goal:
R : Type u_2
A : Type u_3
inst : Add A
inst_1 : Mul A
inst_2 : SMul R A
inst_3 : Star A
⊢ Eq.{u_3 + 1} (α := A ≃⋆ₐ[R] A) (symm refl) refl

Tactic:
rfl

Premises used: RingEquiv.refl, StarAlgEquiv.refl, StarRingEquiv.symm, StarRingEquiv.refl, StarAlgEquiv.symm, Equiv.symm, Equiv.refl, RingEquiv.symm, rfl
-- Module: Mathlib.Algebra.Star.StarAlgHom
Goal:
R : Type u_2
A : Type u_3
B : Type u_4
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
e : A ≃⋆ₐ[R] B
⊢ Eq (α := B ≃⋆+* A) (↑e.symm : B ≃⋆+* A) (StarRingEquiv.symm (↑e : A ≃⋆+* B))

Tactic:
rfl

Premises used: StarRingEquiv.symm, StarRingEquivClass.toStarRingEquiv, RingEquivClass.toRingEquiv, Equiv.symm, EquivLike.toEquiv, RingEquiv.symm, rfl
-- Module: Mathlib.Algebra.Star.StarAlgHom
Goal:
R : Type u_2
A : Type u_3
B : Type u_4
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
e : A ≃⋆ₐ[R] B
⊢ Eq (α := B ≃+* A) (StarRingEquiv.toRingEquiv (StarRingEquiv.symm (↑e : A ≃⋆+* B)))
    (RingEquiv.symm (StarRingEquiv.toRingEquiv (↑e : A ≃⋆+* B)))

Tactic:
rfl

Premises used: RingEquiv.symm, rfl
-- Module: Mathlib.Algebra.Star.StarAlgHom
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)
rw₁ rw₂ : r • e₂.toFun (e₁.toFun a) = r • e₂.toFun (e₁.toFun a)
⊢ e₂.toFun (e₁.toFun (r • a)) = r • e₂.toFun (e₁.toFun a)

Tactic:
rw [e₁.map_smul', e₂.map_smul']

Premises used: StarAlgEquiv.map_smul'
-- Module: Mathlib.Algebra.Star.StarAlgHom
Goal:
R : Type u_2
A : Type u_3
B : Type u_4
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
e : A ≃⋆ₐ[R] B
⊢ ∀ (x : B), (e : (a : A) → B) ((e.symm : (a : B) → A) x : A) = x

Tactic:
e.toStarRingEquiv.apply_symm_apply

Premises used: StarRingEquiv.apply_symm_apply, StarAlgEquiv.toStarRingEquiv
-- Module: Mathlib.Algebra.Star.StarAlgHom
Goal:
R : Type u_2
A : Type u_3
B : Type u_4
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
e : A ≃⋆ₐ[R] B
⊢ ∀ (x : A), (e.symm : (a : B) → A) ((e : (a : A) → B) x : B) = x

Tactic:
e.toStarRingEquiv.symm_apply_apply

Premises used: StarRingEquiv.symm_apply_apply, StarAlgEquiv.toStarRingEquiv
-- Module: Mathlib.Algebra.Star.StarAlgHom
Goal:
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
x : C
⊢ Eq.{u_3 + 1} (α := A) (((e₁.trans e₂).symm : (a : C) → A) x : A)
    ((e₁.symm : (a : B) → A) ((e₂.symm : (a : C) → B) x : B) : A)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Star.StarAlgHom
Goal:
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
⊢ Eq (α := (a : A) → C) (⇑(e₁.trans e₂) : (a : A) → C)
    (Function.comp.{u_3 + 1, u_4 + 1, u_5 + 1} (β := B) (⇑e₂ : (a : B) → C) (⇑e₁ : (a : A) → B))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Star.StarAlgHom
Goal:
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
x : A
⊢ Eq.{u_5 + 1} (α := C) ((e₁.trans e₂ : (a : A) → C) x : C) ((e₂ : (a : B) → C) ((e₁ : (a : A) → B) x : B) : C)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Star.StarAlgHom
Goal:
R : Type u_2
A : Type u_3
B : Type u_4
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
e : A ≃⋆ₐ[R] B
⊢ Function.LeftInverse.{u_3 + 1, u_4 + 1} (α := A) (β := B) (⇑e.symm : (a : B) → A) (⇑e : (a : A) → B)

Tactic:
e.left_inv

Premises used: RingEquiv.toEquiv, StarRingEquiv.toRingEquiv, StarAlgEquiv.toStarRingEquiv, Equiv.left_inv
-- Module: Mathlib.Algebra.Star.StarAlgHom
Goal:
R : Type u_2
A : Type u_3
B : Type u_4
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
e : A ≃⋆ₐ[R] B
⊢ Function.RightInverse.{u_3 + 1, u_4 + 1} (α := A) (β := B) (⇑e.symm : (a : B) → A) (⇑e : (a : A) → B)

Tactic:
e.right_inv

Premises used: RingEquiv.toEquiv, StarRingEquiv.toRingEquiv, Equiv.right_inv, StarAlgEquiv.toStarRingEquiv
-- Module: Mathlib.Algebra.Star.StarAlgHom
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
simp_rw : r • f.toFun 1 = HSMul.hSMul (β := B) r 1
⊢ f.toFun ((algebraMap R A : (a : R) → A) r) = (algebraMap R B : (a : R) → B) r

Tactic:
simp_rw [Algebra.algebraMap_eq_smul_one', map_smul']

Premises used: Algebra.algebraMap_eq_smul_one', StarAlgEquiv.map_smul'
-- Module: Mathlib.Algebra.Star.StarAlgHom
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
⊢ r • f.toFun 1 = HSMul.hSMul (β := B) r 1

Tactic:
simp
-- Module: Mathlib.Algebra.Star.StarAlgHom
Goal:
R : Type u_6
A : Type u_7
B : Type u_8
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
inst_5 : Star A
inst_6 : Star B
f : A ≃⋆ₐ[R] B
⊢ f.symm.toAlgEquiv = f.toAlgEquiv.symm

Tactic:
rfl

Premises used: StarAlgEquiv.toAlgEquiv, AlgEquiv.symm, rfl
-- Module: Mathlib.Algebra.Star.StarAlgHom
Goal:
R : Type u_6
A : Type u_7
B : Type u_8
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
inst_5 : Star A
inst_6 : Star B
f : A ≃⋆ₐ[R] B
⊢ Eq (α := (a : A) → B) (⇑f.toAlgEquiv : (a : A) → B) (⇑f : (a : A) → B)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Star.StarAlgHom
Goal:
R : Type u_6
A : Type u_7
B : Type u_8
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
inst_5 : Star A
inst_6 : Star B
f : A ≃⋆ₐ[R] B
⊢ Eq (α := (a : B) → A) (⇑f.toAlgEquiv.symm : (a : B) → A) (⇑f.symm : (a : B) → A)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Star.StarAlgHom
Goal:
R : Type u_6
A : Type u_7
B : Type u_8
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
inst_5 : Star A
inst_6 : Star B
C : Type u_9
inst_7 : Semiring C
inst_8 : Algebra R C
inst_9 : Star C
f : A ≃⋆ₐ[R] B
g : B ≃⋆ₐ[R] C
⊢ (f.trans g).toAlgEquiv = f.toAlgEquiv.trans g.toAlgEquiv

Tactic:
rfl

Premises used: StarAlgEquiv.toAlgEquiv, AlgEquiv.trans, rfl
-- Module: Mathlib.Algebra.Star.StarAlgHom
Goal:
R : Type u_6
A : Type u_7
B : Type u_8
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
inst_5 : Star A
inst_6 : Star B
⊢ Function.Injective (α := A ≃⋆ₐ[R] B) toAlgEquiv

Tactic:
fun _ _ h => ext <| AlgEquiv.congr_fun h

Premises used: Function.Injective, StarAlgEquiv.ext, AlgEquiv.congr_fun
-- Module: Mathlib.Algebra.Star.StarAlgHom
Goal:
R : Type u_6
A : Type u_7
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Algebra R A
inst_3 : Star A
⊢ Eq.{u_7 + 1} (α := A ≃ₐ[R] A) (toAlgEquiv refl) AlgEquiv.refl

Tactic:
rfl

Premises used: StarAlgEquiv.toAlgEquiv, AlgEquiv.refl, rfl
-- Module: Mathlib.Algebra.Star.StarAlgHom
Goal:
R : Type u_6
A : Type u_7
B : Type u_8
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
inst_5 : Star A
inst_6 : Star B
f : A ≃ₐ[R] B
map_star : ∀ (x : A), Eq.{u_8 + 1} (α := B) ((f : (a : A) → B) (star x) : B) (star ((f : (a : A) → B) x) : B)
x : A
⊢ Eq.{u_8 + 1} (α := B) ((ofAlgEquiv f map_star : (a : A) → B) x : B) ((f : (a : A) → B) x : B)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Star.StarAlgHom
Goal:
R : Type u_6
A : Type u_7
B : Type u_8
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
inst_5 : Star A
inst_6 : Star B
f : A ≃ₐ[R] B
map_star : ∀ (x : A), Eq.{u_8 + 1} (α := B) ((f : (a : A) → B) (star x) : B) (star ((f : (a : A) → B) x) : B)
⊢ (ofAlgEquiv f map_star).symm = ofAlgEquiv f.symm ⋯

Tactic:
rfl

Premises used: StarRingEquiv.symm, StarAlgEquiv.symm, StarAlgEquiv.ofAlgEquiv, Equiv.symm, RingEquiv.symm, rfl
-- Module: Mathlib.Algebra.Star.StarAlgHom
Goal:
R : Type u_6
A : Type u_7
B : Type u_8
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
inst_5 : Star A
inst_6 : Star B
f : A ≃ₐ[R] B
map_star : ∀ (x : A), Eq.{u_8 + 1} (α := B) ((f : (a : A) → B) (star x) : B) (star ((f : (a : A) → B) x) : B)
⊢ (ofAlgEquiv f map_star).toAlgEquiv = f

Tactic:
rfl

Premises used: StarAlgEquiv.toAlgEquiv, rfl
-- Module: Mathlib.Algebra.Star.StarAlgHom
Goal:
R : Type u_6
A : Type u_7
B : Type u_8
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Algebra R A
inst_4 : Algebra R B
inst_5 : Star A
inst_6 : Star B
f : A ≃⋆ₐ[R] B
map_star :
  ∀ (x : A),
    Eq.{u_8 + 1} (α := B) ((f.toAlgEquiv : (a : A) → B) (star x) : B) (star ((f.toAlgEquiv : (a : A) → B) x) : B)
⊢ ofAlgEquiv f.toAlgEquiv map_star = f

Tactic:
rfl

Premises used: StarAlgEquiv.ofAlgEquiv, rfl
-- Module: Mathlib.Algebra.Star.StarAlgHom
Goal:
F : Type u_1
R : Type u_3
A : Type u_4
B : Type u_5
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 : FunLike F A B
inst_8 : NonUnitalAlgHomClass F R A B
inst_9 : StarHomClass F A B
f : F
hf : Function.Bijective.{u_4 + 1, u_5 + 1} (α := A) (β := B) (⇑f : (a : A) → B)
⊢ Eq (α := (a : A) → B) (⇑(ofBijective f hf) : (a : A) → B) (⇑f : (a : A) → B)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Star.StarAlgHom
Goal:
F : Type u_1
R : Type u_3
A : Type u_4
B : Type u_5
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 : FunLike F A B
inst_8 : NonUnitalAlgHomClass F R A B
inst_9 : StarHomClass F A B
f : F
hf : Function.Bijective.{u_4 + 1, u_5 + 1} (α := A) (β := B) (⇑f : (a : A) → B)
a : A
⊢ Eq.{u_5 + 1} (α := B) ((ofBijective f hf : (a : A) → B) a : B) ((f : (a : A) → B) a : B)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Star.StarAlgHom
Goal:
S : Type u_1
R : Type u_2
inst : Mul R
inst_1 : Add R
inst_2 : Star R
inst_3 : SMul S R
f g : R ≃⋆ₐ[S] R
x : R
⊢ Eq (α := R) ((f * g : (a : R) → R) x : R) ((f : (a : R) → R) ((g : (a : R) → R) x : R) : R)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Star.StarAlgHom
Goal:
S : Type u_1
R : Type u_2
inst : Mul R
inst_1 : Add R
inst_2 : Star R
inst_3 : SMul S R
x : R
⊢ (1 : (a : R) → R) x = x

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Star.StarAlgHom
Goal:
S : Type u_1
R : Type u_2
inst : Mul R
inst_1 : Add R
inst_2 : Star R
inst_3 : SMul S R
f : R ≃⋆ₐ[S] R
⊢ f⁻¹ = f.symm

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Star.StarAlgHom
Goal:
S : Type u_1
R : Type u_2
inst : Mul R
inst_1 : Add R
inst_2 : Star R
inst_3 : SMul S R
f : R ≃⋆ₐ[S] R
n : ℕ
⊢ Eq (α := (a : R) → R) (⇑(f ^ n) : (a : R) → R) (⇑f : (a : R) → R)^[n]

Tactic:
hom_coe_pow _ (funext one_apply) (fun f g ↦ funext <| mul_apply f g) _ _

Premises used: StarAlgEquiv.mul_apply, StarAlgEquiv.one_apply, funext, hom_coe_pow
-- Module: Mathlib.Algebra.Star.StarProjection
Goal:
R : Type u_1
p : R
inst : Mul R
inst_1 : Star R
⊢ IsStarProjection p ↔ p * p = p ∧ star p = p

Tactic:
isStarProjection_iff _

Premises used: IsSelfAdjoint, isStarProjection_iff, IsIdempotentElem
-- Module: Mathlib.Algebra.Star.StarProjection
Goal:
R : Type u_1
p : R
inst : Mul R
inst_1 : Star R
hp : IsStarProjection p
⊢ IsStarNormal p

Tactic:
hp.isSelfAdjoint.isStarNormal

Premises used: IsSelfAdjoint.isStarNormal, IsStarProjection.isSelfAdjoint
-- Module: Mathlib.Algebra.Star.StarProjection
Goal:
R : Type u_1
inst : NonUnitalNonAssocSemiring R
inst_1 : StarAddMonoid R
⊢ IsStarProjection.{u_1} (R := R) 0

Tactic:
⟨.zero, .zero _⟩

Premises used: IsIdempotentElem.zero, IsStarProjection.mk, IsSelfAdjoint.zero
-- Module: Mathlib.Algebra.Star.StarProjection
Goal:
R : Type u_1
inst : MulOneClass R
inst_1 : StarMul R
⊢ IsStarProjection.{u_1} (R := R) 1

Tactic:
⟨.one, .one _⟩

Premises used: IsIdempotentElem.one, IsStarProjection.mk, IsSelfAdjoint.one
-- Module: Mathlib.Algebra.Star.StarProjection
Goal:
R : Type u_1
p : R
inst : Monoid R
inst_1 : Star R
hp : IsStarProjection p
n : ℕ
hn : n ≠ 0
⊢ p ^ n = p

Tactic:
hp.isIdempotentElem.pow_eq hn

Premises used: IsIdempotentElem.pow_eq, IsStarProjection.isIdempotentElem
-- Module: Mathlib.Algebra.Star.StarProjection
Goal:
R : Type u_1
p : R
inst : Monoid R
inst_1 : Star R
hp : IsStarProjection p
n : ℕ
⊢ p ^ (n + 1) = p

Tactic:
hp.isIdempotentElem.pow_succ_eq n

Premises used: IsStarProjection.isIdempotentElem, IsIdempotentElem.pow_succ_eq
-- Module: Mathlib.Algebra.Star.StarProjection
Goal:
R : Type u_1
p : R
inst : NonAssocRing R
inst_1 : StarRing R
⊢ IsStarProjection (1 - p) ↔ IsStarProjection p

Tactic:
⟨fun h ↦ sub_sub_cancel 1 p ▸ h.one_sub, .one_sub⟩

Premises used: Eq.rec, sub_sub_cancel, Iff.intro, IsStarProjection.one_sub, OfNat.ofNat
-- Module: Mathlib.Algebra.Star.StarProjection
Goal:
R : Type u_1
p : R
inst : NonAssocRing R
inst_1 : Star R
hp : IsStarProjection p
⊢ p * (1 - p) = 0

Tactic:
hp.isIdempotentElem.mul_one_sub_self

Premises used: IsStarProjection.isIdempotentElem, IsIdempotentElem.mul_one_sub_self
-- Module: Mathlib.Algebra.Star.StarProjection
Goal:
R : Type u_1
p : R
inst : NonAssocRing R
inst_1 : Star R
hp : IsStarProjection p
⊢ (1 - p) * p = 0

Tactic:
hp.isIdempotentElem.one_sub_mul_self

Premises used: IsStarProjection.isIdempotentElem, IsIdempotentElem.one_sub_mul_self
-- Module: Mathlib.Algebra.Star.StarProjection
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
rw : q * p = 0
⊢ p * q + q * p = 0

Tactic:
rw [hpq, zero_add]

Premises used: zero_add
-- Module: Mathlib.Algebra.Star.StarProjection
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
⊢ q * p = 0

Tactic:
simpa [hp.isSelfAdjoint.star_eq, hq.isSelfAdjoint.star_eq] using congr(star $(hpq))

Premises used: IsStarProjection.isSelfAdjoint, IsSelfAdjoint.star_eq
-- Module: Mathlib.Algebra.Star.StarProjection
Goal:
R : Type u_1
p q : R
inst : NonUnitalNonAssocRing R
inst_1 : StarRing R
hp : IsStarProjection p
hq : IsStarProjection q
hpq : p * q = p
⊢ q * p = p

Tactic:
simpa [hp.isSelfAdjoint.star_eq, hq.isSelfAdjoint.star_eq] using congr(star $(hpq))

Premises used: IsStarProjection.isSelfAdjoint, IsSelfAdjoint.star_eq
-- Module: Mathlib.Algebra.Star.StarProjection
Goal:
R : Type u_1
p q : R
inst : NonUnitalNonAssocRing R
inst_1 : StarRing R
hp : IsStarProjection p
hq : IsStarProjection q
hqp : q * p = p
⊢ p * q = p

Tactic:
simpa [hp.isSelfAdjoint.star_eq, hq.isSelfAdjoint.star_eq] using congr(star $(hqp))

Premises used: IsStarProjection.isSelfAdjoint, IsSelfAdjoint.star_eq
-- Module: Mathlib.Algebra.Star.StarProjection
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
rw : (p * q = p ∧ q * p = p) ∧ IsSelfAdjoint (q - p) ↔ p * q = p
⊢ IsStarProjection (q - p) ↔ p * q = p

Tactic:
rw [isStarProjection_iff, hp.isIdempotentElem.sub_iff hq.isIdempotentElem]

Premises used: IsStarProjection.isIdempotentElem, isStarProjection_iff, IsIdempotentElem.sub_iff
-- Module: Mathlib.Algebra.Star.StarProjection
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
simp_rw : p * q = p ∧ q * p = p ↔ p * q = p
⊢ (p * q = p ∧ q * p = p) ∧ IsSelfAdjoint (q - p) ↔ p * q = p

Tactic:
simp_rw [hq.isSelfAdjoint.sub hp.isSelfAdjoint, and_true]

Premises used: IsSelfAdjoint.sub, and_true, IsStarProjection.isSelfAdjoint
-- Module: Mathlib.Algebra.Star.StarProjection
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
nth_rw : p * q = p ∧ q * star p = p ↔ p * q = p
⊢ p * q = p ∧ q * p = p ↔ p * q = p

Tactic:
nth_rw 3 [← hp.isSelfAdjoint]

Premises used: IsStarProjection.isSelfAdjoint
-- Module: Mathlib.Algebra.Star.StarProjection
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
nth_rw : p * q = p ∧ star q * star p = p ↔ p * q = p
⊢ p * q = p ∧ q * star p = p ↔ p * q = p

Tactic:
nth_rw 2 [← hq.isSelfAdjoint]

Premises used: IsStarProjection.isSelfAdjoint
-- Module: Mathlib.Algebra.Star.StarProjection
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
rw : p = p * q ∧ p = p * q ↔ p = p * q
⊢ p * q = p ∧ star q * star p = p ↔ p * q = p

Tactic:
rw [← star_mul, star_eq_iff_star_eq, hp.isSelfAdjoint, eq_comm]

Premises used: eq_comm, star_eq_iff_star_eq, IsStarProjection.isSelfAdjoint, StarMul.star_mul