-- 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
g : A ≃⋆ₐ[R] B
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
have rcases : ∀ (toFun_1 : A → B) (invFun_1 : B → A) (left_inv_1 : Function.LeftInverse invFun_1 toFun_1)
  (right_inv_1 : Function.RightInverse invFun_1 toFun_1)
  (map_mul'_1 :
    ∀ (x y : A),
      { toFun := toFun_1, invFun := invFun_1, left_inv := left_inv_1, right_inv := right_inv_1 : A ≃ B }.toFun (x * y) =
        { toFun := toFun_1, invFun := invFun_1, left_inv := left_inv_1, right_inv := right_inv_1 : A ≃ B }.toFun x *
          { toFun := toFun_1, invFun := invFun_1, left_inv := left_inv_1, right_inv := right_inv_1 : A ≃ B }.toFun y)
  (map_add'_1 :
    ∀ (x y : A),
      { toFun := toFun_1, invFun := invFun_1, left_inv := left_inv_1, right_inv := right_inv_1 : A ≃ B }.toFun (x + y) =
        { toFun := toFun_1, invFun := invFun_1, left_inv := left_inv_1, right_inv := right_inv_1 : A ≃ B }.toFun x +
          { toFun := toFun_1, invFun := invFun_1, left_inv := left_inv_1, right_inv := right_inv_1 : A ≃ B }.toFun y)
  (map_star'_1 :
    ∀ (a : A),
      { toFun := toFun_1, invFun := invFun_1, left_inv := left_inv_1, right_inv := right_inv_1, map_mul' := map_mul'_1,
              map_add' := map_add'_1 : A ≃+* B }.toFun
          (star a) =
        star
          ({ toFun := toFun_1, invFun := invFun_1, left_inv := left_inv_1, right_inv := right_inv_1,
                map_mul' := map_mul'_1, map_add' := map_add'_1 : A ≃+* B }.toFun
            a))
  (map_smul'_1 :
    ∀ (r : R) (a : A),
      { toFun := toFun_1, invFun := invFun_1, left_inv := left_inv_1, right_inv := right_inv_1, map_mul' := map_mul'_1,
              map_add' := map_add'_1, map_star' := map_star'_1 : A ≃⋆+* B }.toFun
          (r • a) =
        r •
          { toFun := toFun_1, invFun := invFun_1, left_inv := left_inv_1, right_inv := right_inv_1,
                map_mul' := map_mul'_1, map_add' := map_add'_1, map_star' := map_star'_1 : 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 =
      { toFun := toFun_1, invFun := invFun_1, left_inv := left_inv_1, right_inv := right_inv_1, map_mul' := map_mul'_1,
          map_add' := map_add'_1, map_star' := map_star'_1, map_smul' := map_smul'_1 : A ≃⋆ₐ[R] B }.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 =
      { toFun := toFun_1, invFun := invFun_1, left_inv := left_inv_1, right_inv := right_inv_1, map_mul' := map_mul'_1,
          map_add' := map_add'_1, map_star' := map_star'_1, map_smul' := map_smul'_1 : A ≃⋆ₐ[R] B }.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 } =
    { toFun := toFun_1, invFun := invFun_1, left_inv := left_inv_1, right_inv := right_inv_1, map_mul' := map_mul'_1,
      map_add' := map_add'_1, map_star' := map_star'_1, map_smul' := map_smul'_1 }
Tactic: rcases g with ⟨⟨⟨⟨_, _, _⟩, _⟩, _⟩, _⟩
Cleared hypotheses: g, h₁, h₂