awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
⊢ p = p * q ∧ p = p * q ↔ p = p * q

Tactic:
simp_rw [and_self]

Premises used: and_self
-- 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 : IsStarProjection (q - p) ↔ star (q * p) = star p
⊢ IsStarProjection (q - p) ↔ q * p = p

Tactic:
rw [← star_inj]

Premises used: star_inj
-- 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
⊢ IsStarProjection (q - p) ↔ star (q * p) = star p

Tactic:
simp [star_mul, hp.isSelfAdjoint.star_eq, hq.isSelfAdjoint.star_eq,
    sub_iff_mul_eq_left hp hq]

Premises used: IsStarProjection.sub_iff_mul_eq_left, IsStarProjection.isSelfAdjoint, StarMul.star_mul, IsSelfAdjoint.star_eq
-- Module: Mathlib.Algebra.Star.StarRingHom
Goal:
A : Type u_1
B : Type u_2
C : Type u_3
D : Type u_4
inst : NonUnitalNonAssocSemiring A
inst_1 : Star A
inst_2 : NonUnitalNonAssocSemiring B
inst_3 : Star B
inst_4 : NonUnitalNonAssocSemiring C
inst_5 : Star C
inst_6 : NonUnitalNonAssocSemiring D
inst_7 : Star D
f : A → B
map_mul' : ∀ (x y : A), f (x * y) = f x * f y
map_zero' : { toFun := f, map_mul' := map_mul' : A →ₙ* B }.toFun 0 = 0
map_add' :
  ∀ (x y : A),
    { toFun := f, map_mul' := map_mul' : A →ₙ* B }.toFun (x + y) =
      { toFun := f, map_mul' := map_mul' : A →ₙ* B }.toFun x + { toFun := f, map_mul' := map_mul' : A →ₙ* B }.toFun y
map_star' :
  ∀ (a : A),
    { toFun := f, map_mul' := map_mul', map_zero' := map_zero', map_add' := map_add' : A →ₙ+* B }.toFun (star a) =
      star ({ toFun := f, map_mul' := map_mul', map_zero' := map_zero', map_add' := map_add' : A →ₙ+* B }.toFun a)
g : A → B
map_mul'_1 : ∀ (x y : A), g (x * y) = g x * g y
map_zero'_1 : { toFun := g, map_mul' := map_mul'_1 : A →ₙ* B }.toFun 0 = 0
map_add'_1 :
  ∀ (x y : A),
    { toFun := g, map_mul' := map_mul'_1 : A →ₙ* B }.toFun (x + y) =
      { toFun := g, map_mul' := map_mul'_1 : A →ₙ* B }.toFun x +
        { toFun := g, map_mul' := map_mul'_1 : A →ₙ* B }.toFun y
map_star'_1 :
  ∀ (a : A),
    { toFun := g, map_mul' := map_mul'_1, map_zero' := map_zero'_1, map_add' := map_add'_1 : A →ₙ+* B }.toFun (star a) =
      star ({ toFun := g, map_mul' := map_mul'_1, map_zero' := map_zero'_1, map_add' := map_add'_1 : A →ₙ+* B }.toFun a)
h :
  Eq (α := (a : A) → B)
    ((fun (f : A →⋆ₙ+* B) ↦ f.toFun)
      { toFun := f, map_mul' := map_mul', map_zero' := map_zero', map_add' := map_add', map_star' := map_star' })
    ((fun (f : A →⋆ₙ+* B) ↦ f.toFun)
      { toFun := g, map_mul' := map_mul'_1, map_zero' := map_zero'_1, map_add' := map_add'_1,
        map_star' := map_star'_1 })
⊢ { toFun := f, map_mul' := map_mul', map_zero' := map_zero', map_add' := map_add', map_star' := map_star' :
      A →⋆ₙ+* B } =
    { toFun := g, map_mul' := map_mul'_1, map_zero' := map_zero'_1, map_add' := map_add'_1, map_star' := map_star'_1 }

Tactic:
congr
-- Module: Mathlib.Algebra.Star.StarRingHom
Goal:
A : Type u_1
B : Type u_2
inst : NonUnitalNonAssocSemiring A
inst_1 : Star A
inst_2 : NonUnitalNonAssocSemiring B
inst_3 : Star B
F : Type u_5
inst_4 : FunLike F A B
inst_5 : NonUnitalRingHomClass F A B
inst_6 : NonUnitalStarRingHomClass F A B
f : F
⊢ Eq (α := (a : A) → B) (⇑(↑f : A →⋆ₙ+* B) : (a : A) → B) (⇑f : (a : A) → B)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Star.StarRingHom
Goal:
A : Type u_1
B : Type u_2
inst : NonUnitalNonAssocSemiring A
inst_1 : Star A
inst_2 : NonUnitalNonAssocSemiring B
inst_3 : Star B
f : A →⋆ₙ+* B
⊢ Eq (α := (a : A) → B) (⇑f.toNonUnitalRingHom : (a : A) → B) (⇑f : (a : A) → B)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Star.StarRingHom
Goal:
A : Type u_1
B : Type u_2
inst : NonUnitalNonAssocSemiring A
inst_1 : Star A
inst_2 : NonUnitalNonAssocSemiring B
inst_3 : Star B
f g : A →⋆ₙ+* B
h : ∀ (x : A), Eq.{u_2 + 1} (α := B) ((f : (a : A) → B) x : B) ((g : (a : A) → B) x : B)
⊢ f = g

Tactic:
DFunLike.ext _ _ h

Premises used: DFunLike.ext
-- Module: Mathlib.Algebra.Star.StarRingHom
Goal:
A : Type u_1
B : Type u_2
inst : NonUnitalNonAssocSemiring A
inst_1 : Star A
inst_2 : NonUnitalNonAssocSemiring B
inst_3 : Star B
f : A →⋆ₙ+* B
f' : A → B
h : f' = (⇑f : (a : A) → B)
⊢ (⇑(f.copy f' h) : (a : A) → B) = f'

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Star.StarRingHom
Goal:
A : Type u_1
B : Type u_2
inst : NonUnitalNonAssocSemiring A
inst_1 : Star A
inst_2 : NonUnitalNonAssocSemiring B
inst_3 : Star B
f : A →⋆ₙ+* B
f' : A → B
h : f' = (⇑f : (a : A) → B)
⊢ f.copy f' h = f

Tactic:
DFunLike.ext' h

Premises used: DFunLike.ext'
-- Module: Mathlib.Algebra.Star.StarRingHom
Goal:
A : Type u_1
B : Type u_2
inst : NonUnitalNonAssocSemiring A
inst_1 : Star A
inst_2 : NonUnitalNonAssocSemiring B
inst_3 : Star B
f : A →ₙ+* B
h : ∀ (a : A), f.toFun (star a) = star (f.toFun a)
⊢ Eq (α := (a : A) → B) (⇑{ toNonUnitalRingHom := f, map_star' := h : A →⋆ₙ+* B } : (a : A) → B) (⇑f : (a : A) → B)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Star.StarRingHom
Goal:
A : Type u_1
B : Type u_2
inst : NonUnitalNonAssocSemiring A
inst_1 : Star A
inst_2 : NonUnitalNonAssocSemiring B
inst_3 : Star B
f : A →⋆ₙ+* B
h₁ :
  ∀ (x y : A),
    (f : (a : A) → B) (x * y) = HMul.hMul (α := B) (β := B) ((f : (a : A) → B) x : B) ((f : (a : A) → B) y : B)
h₂ : { toFun := (⇑f : (a : A) → B), map_mul' := h₁ : A →ₙ* B }.toFun 0 = 0
h₃ :
  ∀ (x y : A),
    { toFun := (⇑f : (a : A) → B), map_mul' := h₁ : A →ₙ* B }.toFun (x + y) =
      { toFun := (⇑f : (a : A) → B), map_mul' := h₁ : A →ₙ* B }.toFun x +
        { toFun := (⇑f : (a : A) → B), map_mul' := h₁ : A →ₙ* B }.toFun y
h₄ :
  ∀ (a : A),
    { toFun := (⇑f : (a : A) → B), map_mul' := h₁, map_zero' := h₂, map_add' := h₃ : A →ₙ+* B }.toFun (star a) =
      star ({ toFun := (⇑f : (a : A) → B), map_mul' := h₁, map_zero' := h₂, map_add' := h₃ : A →ₙ+* B }.toFun a)
h :
  ∀ (x : A),
    Eq.{u_2 + 1} (α := B)
      (({ toFun := (⇑f : (a : A) → B), map_mul' := h₁, map_zero' := h₂, map_add' := h₃, map_star' := h₄ : A →⋆ₙ+* B } :
            (a : A) → B)
          x :
        B)
      ((f : (a : A) → B) x : B)
⊢ { toFun := (⇑f : (a : A) → B), map_mul' := h₁, map_zero' := h₂, map_add' := h₃, map_star' := h₄ : A →⋆ₙ+* B } = f

Tactic:
ext
-- Module: Mathlib.Algebra.Star.StarRingHom
Goal:
A : Type u_1
B : Type u_2
inst : NonUnitalNonAssocSemiring A
inst_1 : Star A
inst_2 : NonUnitalNonAssocSemiring B
inst_3 : Star B
f : A →⋆ₙ+* B
h₁ :
  ∀ (x y : A),
    (f : (a : A) → B) (x * y) = HMul.hMul (α := B) (β := B) ((f : (a : A) → B) x : B) ((f : (a : A) → B) y : B)
h₂ : { toFun := (⇑f : (a : A) → B), map_mul' := h₁ : A →ₙ* B }.toFun 0 = 0
h₃ :
  ∀ (x y : A),
    { toFun := (⇑f : (a : A) → B), map_mul' := h₁ : A →ₙ* B }.toFun (x + y) =
      { toFun := (⇑f : (a : A) → B), map_mul' := h₁ : A →ₙ* B }.toFun x +
        { toFun := (⇑f : (a : A) → B), map_mul' := h₁ : A →ₙ* B }.toFun y
h₄ :
  ∀ (a : A),
    { toFun := (⇑f : (a : A) → B), map_mul' := h₁, map_zero' := h₂, map_add' := h₃ : A →ₙ+* B }.toFun (star a) =
      star ({ toFun := (⇑f : (a : A) → B), map_mul' := h₁, map_zero' := h₂, map_add' := h₃ : A →ₙ+* B }.toFun a)
x : A
⊢ Eq.{u_2 + 1} (α := B)
    (({ toFun := (⇑f : (a : A) → B), map_mul' := h₁, map_zero' := h₂, map_add' := h₃, map_star' := h₄ : A →⋆ₙ+* B } :
          (a : A) → B)
        x :
      B)
    ((f : (a : A) → B) x : B)

Tactic:
rfl
-- Module: Mathlib.Algebra.Star.StarRingHom
Goal:
A : Type u_1
inst : NonUnitalNonAssocSemiring A
inst_1 : Star A
⊢ Eq (α := (a : A) → A) (⇑(NonUnitalStarRingHom.id A) : (a : A) → A) id

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Star.StarRingHom
Goal:
A : Type u_1
B : Type u_2
C : Type u_3
D : Type u_4
inst : NonUnitalNonAssocSemiring A
inst_1 : Star A
inst_2 : NonUnitalNonAssocSemiring B
inst_3 : Star B
inst_4 : NonUnitalNonAssocSemiring C
inst_5 : Star C
inst_6 : NonUnitalNonAssocSemiring D
inst_7 : Star D
f : B →⋆ₙ+* C
g : A →⋆ₙ+* B
a : A
⊢ (f.comp g.toNonUnitalRingHom).toFun (star a) = star ((f.comp g.toNonUnitalRingHom).toFun a)

Tactic:
simp [map_star, map_star]

Premises used: StarHomClass.map_star
-- Module: Mathlib.Algebra.Star.StarRingHom
Goal:
A : Type u_1
B : Type u_2
C : Type u_3
inst : NonUnitalNonAssocSemiring A
inst_1 : Star A
inst_2 : NonUnitalNonAssocSemiring B
inst_3 : Star B
inst_4 : NonUnitalNonAssocSemiring C
inst_5 : Star C
f : B →⋆ₙ+* C
g : A →⋆ₙ+* B
⊢ Eq (α := (a : A) → C) (⇑(f.comp g) : (a : A) → C)
    (Function.comp.{u_1 + 1, u_2 + 1, u_3 + 1} (β := B) (⇑f : (a : B) → C) (⇑g : (a : A) → B))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Star.StarRingHom
Goal:
A : Type u_1
B : Type u_2
C : Type u_3
inst : NonUnitalNonAssocSemiring A
inst_1 : Star A
inst_2 : NonUnitalNonAssocSemiring B
inst_3 : Star B
inst_4 : NonUnitalNonAssocSemiring C
inst_5 : Star C
f : B →⋆ₙ+* C
g : A →⋆ₙ+* B
a : A
⊢ Eq.{u_3 + 1} (α := C) ((f.comp g : (a : A) → C) a : C) ((f : (a : B) → C) ((g : (a : A) → B) a : B) : C)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Star.StarRingHom
Goal:
A : Type u_1
B : Type u_2
C : Type u_3
D : Type u_4
inst : NonUnitalNonAssocSemiring A
inst_1 : Star A
inst_2 : NonUnitalNonAssocSemiring B
inst_3 : Star B
inst_4 : NonUnitalNonAssocSemiring C
inst_5 : Star C
inst_6 : NonUnitalNonAssocSemiring D
inst_7 : Star D
f : C →⋆ₙ+* D
g : B →⋆ₙ+* C
h : A →⋆ₙ+* B
⊢ (f.comp g).comp h = f.comp (g.comp h)

Tactic:
rfl

Premises used: NonUnitalStarRingHom.comp, rfl
-- Module: Mathlib.Algebra.Star.StarRingHom
Goal:
A : Type u_1
B : Type u_2
inst : NonUnitalNonAssocSemiring A
inst_1 : Star A
inst_2 : NonUnitalNonAssocSemiring B
inst_3 : Star B
f : A →⋆ₙ+* B
⊢ comp (NonUnitalStarRingHom.id B) f = f

Tactic:
ext fun _ => rfl

Premises used: NonUnitalStarRingHom.ext, rfl
-- Module: Mathlib.Algebra.Star.StarRingHom
Goal:
A : Type u_1
B : Type u_2
inst : NonUnitalNonAssocSemiring A
inst_1 : Star A
inst_2 : NonUnitalNonAssocSemiring B
inst_3 : Star B
f : A →⋆ₙ+* B
⊢ f.comp (NonUnitalStarRingHom.id A) = f

Tactic:
ext fun _ => rfl

Premises used: NonUnitalStarRingHom.ext, rfl
-- Module: Mathlib.Algebra.Star.StarRingHom
Goal:
A : Type u_1
inst : NonUnitalNonAssocSemiring A
inst_1 : Star A
⊢ Eq.{u_1 + 1} (α := (a : A) → A) (⇑1 : (a : A) → A) id

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Star.StarRingHom
Goal:
A : Type u_1
inst : NonUnitalNonAssocSemiring A
inst_1 : Star A
a : A
⊢ (1 : (a : A) → A) a = a

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Star.StarRingHom
Goal:
A : Type u_1
B : Type u_2
C : Type u_3
inst : NonUnitalNonAssocSemiring A
inst_1 : StarAddMonoid A
inst_2 : NonUnitalNonAssocSemiring B
inst_3 : StarAddMonoid B
⊢ ∀ (a : A),
    Eq.{u_2 + 1} (α := B) (MulHom.toFun (NonUnitalRingHom.toMulHom 0) (star a))
      (star (MulHom.toFun (NonUnitalRingHom.toMulHom 0) a))

Tactic:
simp
-- Module: Mathlib.Algebra.Star.StarRingHom
Goal:
A : Type u_1
B : Type u_2
inst : NonUnitalNonAssocSemiring A
inst_1 : StarAddMonoid A
inst_2 : NonUnitalNonAssocSemiring B
inst_3 : StarAddMonoid B
⊢ Eq (α := (a : A) → B) (⇑0 : (a : A) → B) 0

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Star.StarRingHom
Goal:
A : Type u_1
B : Type u_2
inst : NonUnitalNonAssocSemiring A
inst_1 : StarAddMonoid A
inst_2 : NonUnitalNonAssocSemiring B
inst_3 : StarAddMonoid B
a : A
⊢ Eq.{u_2 + 1} (α := B) ((0 : (a : A) → B) a : B) (0 : B)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Star.StarRingHom
Goal:
F : Type u_1
A : Type u_2
B : Type u_3
inst : Add A
inst_1 : Mul A
inst_2 : Star A
inst_3 : Add B
inst_4 : Mul B
inst_5 : Star B
inst_6 : EquivLike F A B
hF : StarRingEquivClass F A B
⊢ StarHomClass F A B

Tactic:
{ hF with }

Premises used: StarRingEquivClass.map_star, StarHomClass.mk
-- Module: Mathlib.Algebra.Star.StarRingHom
Goal:
F : Type u_1
A : Type u_2
B : Type u_3
inst : NonUnitalNonAssocSemiring A
inst_1 : Star A
inst_2 : NonUnitalNonAssocSemiring B
inst_3 : Star B
inst_4 : EquivLike F A B
inst_5 : RingEquivClass F A B
inst_6 : StarRingEquivClass F A B
⊢ NonUnitalStarRingHomClass F A B

Tactic:

Premises used: NonUnitalStarRingHomClass.mk
-- Module: Mathlib.Algebra.Star.StarRingHom
Goal:
A : Type u_1
B : Type u_2
C : Type u_3
inst : Add A
inst_1 : Add B
inst_2 : Mul A
inst_3 : Mul B
inst_4 : Star A
inst_5 : Star B
inst_6 : Add C
inst_7 : Mul C
inst_8 : Star C
f g : A ≃⋆+* B
h₁ : f.toFun = g.toFun
h₂ : f.invFun = g.invFun
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))
    (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' : A ≃⋆+* 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' : A ≃⋆+* 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' : A ≃⋆+* B } =
      g
⊢ f = g

Tactic:
rcases f with ⟨⟨⟨_, _, _⟩, _⟩, _⟩
-- Module: Mathlib.Algebra.Star.StarRingHom
Goal:
A : Type u_1
B : Type u_2
inst : Add A
inst_1 : Add B
inst_2 : Mul A
inst_3 : Mul B
inst_4 : Star A
inst_5 : Star B
e : A ≃⋆+* B
⊢ e.toRingEquiv = e.toRingEquiv

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Star.StarRingHom
Goal:
A : Type u_1
B : Type u_2
inst : Add A
inst_1 : Add B
inst_2 : Mul A
inst_3 : Mul B
inst_4 : Star A
inst_5 : Star B
f g : A ≃⋆+* B
h : ∀ (a : A), Eq.{u_2 + 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.StarRingHom
Goal:
A : Type u_1
inst : Add A
inst_1 : Mul A
inst_2 : Star A
⊢ Eq.{u_1 + 1} (α := (a : A) → A) (⇑refl : (a : A) → A) id

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Star.StarRingHom
Goal:
A : Type u_1
B : Type u_2
C : Type u_3
inst : Add A
inst_1 : Add B
inst_2 : Mul A
inst_3 : Mul B
inst_4 : Star A
inst_5 : Star B
inst_6 : Add C
inst_7 : Mul C
inst_8 : Star C
e : A ≃⋆+* B
b : B
⊢ e.symm.toFun (star b) = star (e.symm.toFun b)

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

Premises used: StarHomClass.map_star, EquivLike.inv_apply_apply, congr_arg, EquivLike.inv, Eq.symm, EquivLike.apply_inv_apply
-- Module: Mathlib.Algebra.Star.StarRingHom
Goal:
A : Type u_1
B : Type u_2
inst : Add A
inst_1 : Add B
inst_2 : Mul A
inst_3 : Mul B
inst_4 : Star A
inst_5 : Star B
e : A ≃⋆+* B
⊢ inv e = (⇑e.symm : (a : B) → A)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Star.StarRingHom
Goal:
A : Type u_1
B : Type u_2
inst : Add A
inst_1 : Add B
inst_2 : Mul A
inst_3 : Mul B
inst_4 : Star A
inst_5 : Star B
e : A ≃⋆+* B
⊢ e.symm.symm = e

Tactic:
rfl

Premises used: StarRingEquiv.symm, Equiv.symm, RingEquiv.symm, rfl
-- Module: Mathlib.Algebra.Star.StarRingHom
Goal:
A : Type u_1
B : Type u_2
inst : Add A
inst_1 : Add B
inst_2 : Mul A
inst_3 : Mul B
inst_4 : Star A
inst_5 : Star B
⊢ Function.Bijective (α := A ≃⋆+* B) symm

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

Premises used: Iff.mpr, StarRingEquiv.symm_symm, Function.bijective_iff_has_inverse, And.intro, Exists.intro
-- Module: Mathlib.Algebra.Star.StarRingHom
Goal:
A : Type u_1
B : Type u_2
inst : Add A
inst_1 : Add B
inst_2 : Mul A
inst_3 : Mul B
inst_4 : Star A
inst_5 : Star B
e : A ≃+* B
h₁ : ∀ (a : A), e.toFun (star a) = star (e.toFun a)
⊢ Eq (α := (a : A) → B) (⇑{ toRingEquiv := e, map_star' := h₁ : A ≃⋆+* B } : (a : A) → B) (⇑e : (a : A) → B)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Star.StarRingHom
Goal:
A : Type u_1
B : Type u_2
inst : Add A
inst_1 : Add B
inst_2 : Mul A
inst_3 : Mul B
inst_4 : Star A
inst_5 : Star B
e : A ≃⋆+* 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)
⊢ { toFun := (⇑e : (a : A) → B), invFun := e', left_inv := h₁, right_inv := h₂, map_mul' := h₃, map_add' := h₄,
      map_star' := h₅ : A ≃⋆+* B } =
    e

Tactic:
ext fun _ => rfl

Premises used: StarRingEquiv.ext, rfl
-- Module: Mathlib.Algebra.Star.StarRingHom
Goal:
A : Type u_1
B : Type u_2
inst : Add A
inst_1 : Add B
inst_2 : Mul A
inst_3 : Mul B
inst_4 : Star A
inst_5 : Star B
e : A ≃+* B
h₁ : ∀ (a : A), e.toFun (star a) = star (e.toFun a)
⊢ { toRingEquiv := e, map_star' := h₁ : A ≃⋆+* B }.symm = { toRingEquiv := e.symm, map_star' := ⋯ }

Tactic:
rfl

Premises used: StarRingEquiv.symm, rfl
-- Module: Mathlib.Algebra.Star.StarRingHom
Goal:
A : Type u_1
inst : Add A
inst_1 : Mul A
inst_2 : Star A
⊢ Eq.{u_1 + 1} (α := A ≃⋆+* A) (symm refl) refl

Tactic:
rfl

Premises used: RingEquiv.refl, StarRingEquiv.symm, StarRingEquiv.refl, Equiv.symm, Equiv.refl, RingEquiv.symm, rfl
-- Module: Mathlib.Algebra.Star.StarRingHom
Goal:
A : Type u_1
B : Type u_2
C : Type u_3
inst : Add A
inst_1 : Add B
inst_2 : Mul A
inst_3 : Mul B
inst_4 : Star A
inst_5 : Star B
inst_6 : Add C
inst_7 : Mul C
inst_8 : Star C
e₁ : A ≃⋆+* B
e₂ : B ≃⋆+* C
a : A
rw : e₂.toFun (star (e₁.toFun a)) = star (e₂.toFun (e₁.toFun a))
rw₁ rw₂ : star (e₂.toFun (e₁.toFun a)) = star (e₂.toFun (e₁.toFun a))
⊢ e₂.toFun (e₁.toFun (star a)) = star (e₂.toFun (e₁.toFun a))

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

Premises used: StarRingEquiv.map_star'
-- Module: Mathlib.Algebra.Star.StarRingHom
Goal:
A : Type u_1
B : Type u_2
inst : Add A
inst_1 : Add B
inst_2 : Mul A
inst_3 : Mul B
inst_4 : Star A
inst_5 : Star B
e : A ≃⋆+* B
⊢ ∀ (x : B), (e : (a : A) → B) ((e.symm : (a : B) → A) x : A) = x

Tactic:
e.toRingEquiv.apply_symm_apply

Premises used: RingEquiv.apply_symm_apply, StarRingEquiv.toRingEquiv
-- Module: Mathlib.Algebra.Star.StarRingHom
Goal:
A : Type u_1
B : Type u_2
inst : Add A
inst_1 : Add B
inst_2 : Mul A
inst_3 : Mul B
inst_4 : Star A
inst_5 : Star B
e : A ≃⋆+* B
⊢ ∀ (x : A), (e.symm : (a : B) → A) ((e : (a : A) → B) x : B) = x

Tactic:
e.toRingEquiv.symm_apply_apply

Premises used: StarRingEquiv.toRingEquiv, RingEquiv.symm_apply_apply
-- Module: Mathlib.Algebra.Star.StarRingHom
Goal:
A : Type u_1
B : Type u_2
C : Type u_3
inst : Add A
inst_1 : Add B
inst_2 : Mul A
inst_3 : Mul B
inst_4 : Star A
inst_5 : Star B
inst_6 : Add C
inst_7 : Mul C
inst_8 : Star C
e₁ : A ≃⋆+* B
e₂ : B ≃⋆+* C
x : C
⊢ Eq.{u_1 + 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.StarRingHom
Goal:
A : Type u_1
B : Type u_2
C : Type u_3
inst : Add A
inst_1 : Add B
inst_2 : Mul A
inst_3 : Mul B
inst_4 : Star A
inst_5 : Star B
inst_6 : Add C
inst_7 : Mul C
inst_8 : Star C
e₁ : A ≃⋆+* B
e₂ : B ≃⋆+* C
⊢ Eq (α := (a : A) → C) (⇑(e₁.trans e₂) : (a : A) → C)
    (Function.comp.{u_1 + 1, u_2 + 1, u_3 + 1} (β := B) (⇑e₂ : (a : B) → C) (⇑e₁ : (a : A) → B))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Star.StarRingHom
Goal:
A : Type u_1
B : Type u_2
C : Type u_3
inst : Add A
inst_1 : Add B
inst_2 : Mul A
inst_3 : Mul B
inst_4 : Star A
inst_5 : Star B
inst_6 : Add C
inst_7 : Mul C
inst_8 : Star C
e₁ : A ≃⋆+* B
e₂ : B ≃⋆+* C
x : A
⊢ Eq.{u_3 + 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.StarRingHom
Goal:
A : Type u_1
B : Type u_2
inst : Add A
inst_1 : Add B
inst_2 : Mul A
inst_3 : Mul B
inst_4 : Star A
inst_5 : Star B
e : A ≃⋆+* B
⊢ Function.LeftInverse.{u_1 + 1, u_2 + 1} (α := A) (β := B) (⇑e.symm : (a : B) → A) (⇑e : (a : A) → B)

Tactic:
e.left_inv

Premises used: RingEquiv.toEquiv, StarRingEquiv.toRingEquiv, Equiv.left_inv
-- Module: Mathlib.Algebra.Star.StarRingHom
Goal:
A : Type u_1
B : Type u_2
inst : Add A
inst_1 : Add B
inst_2 : Mul A
inst_3 : Mul B
inst_4 : Star A
inst_5 : Star B
e : A ≃⋆+* B
⊢ Function.RightInverse.{u_1 + 1, u_2 + 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
-- Module: Mathlib.Algebra.Star.StarRingHom
Goal:
F : Type u_1
A : Type u_3
B : Type u_4
inst : NonUnitalNonAssocSemiring A
inst_1 : Star A
inst_2 : NonUnitalNonAssocSemiring B
inst_3 : Star B
inst_4 : FunLike F A B
inst_5 : NonUnitalRingHomClass F A B
inst_6 : NonUnitalStarRingHomClass F A B
f : F
hf : Function.Bijective.{u_3 + 1, u_4 + 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.StarRingHom
Goal:
F : Type u_1
A : Type u_3
B : Type u_4
inst : NonUnitalNonAssocSemiring A
inst_1 : Star A
inst_2 : NonUnitalNonAssocSemiring B
inst_3 : Star B
inst_4 : FunLike F A B
inst_5 : NonUnitalRingHomClass F A B
inst_6 : NonUnitalStarRingHomClass F A B
f : F
hf : Function.Bijective.{u_3 + 1, u_4 + 1} (α := A) (β := B) (⇑f : (a : A) → B)
a : A
⊢ Eq.{u_4 + 1} (α := B) ((ofBijective f hf : (a : A) → B) a : B) ((f : (a : A) → B) a : B)

Tactic:
rfl

Premises used: rfl