-- Lean 4 proof step from Mathlib.RingTheory.GradedAlgebra.AlgHom (goal)
Goal:
R : Type u_1
S : Type u_2
T : Type u_3
U : Type u_4
V : Type u_5
A : Type u_6
B : Type u_7
C : Type u_8
D : Type u_9
ι : Type u_10
inst : CommSemiring R
inst_1 : Semiring A
inst_2 : Semiring B
inst_3 : Semiring C
inst_4 : Semiring D
inst_5 : Algebra R A
inst_6 : Algebra R B
inst_7 : Algebra R C
inst_8 : Algebra R D
inst_9 : DecidableEq ι
inst_10 : AddMonoid ι
𝒜 : ι → Submodule R A
ℬ : ι → Submodule R B
𝒞 : ι → Submodule R C
𝒟 : ι → Submodule R D
inst_11 : GradedAlgebra 𝒜
inst_12 : GradedAlgebra ℬ
inst_13 : GradedAlgebra 𝒞
inst_14 : GradedAlgebra 𝒟
g : 𝒜 →ₐᵍ[R] ℬ
toFun : A → B
map_one' : toFun 1 = 1
map_mul' :
  ∀ (x y : A),
    { toFun := toFun, map_one' := map_one' : OneHom A B }.toFun (x * y) =
      { toFun := toFun, map_one' := map_one' : OneHom A B }.toFun x *
        { toFun := toFun, map_one' := map_one' : OneHom A B }.toFun y
map_zero' : (↑{ toFun := toFun, map_one' := map_one', map_mul' := map_mul' : A →* B } : OneHom A B).toFun 0 = 0
map_add' :
  ∀ (x y : A),
    (↑{ toFun := toFun, map_one' := map_one', map_mul' := map_mul' : A →* B } : OneHom A B).toFun (x + y) =
      (↑{ toFun := toFun, map_one' := map_one', map_mul' := map_mul' : A →* B } : OneHom A B).toFun x +
        (↑{ toFun := toFun, map_one' := map_one', map_mul' := map_mul' : A →* B } : OneHom A B).toFun y
commutes' :
  ∀ (r : R),
    (↑(↑{ toFun := toFun, map_one' := map_one', map_mul' := map_mul', map_zero' := map_zero', map_add' := map_add' :
                    A →+* B } :
                A →* B) :
            OneHom A B).toFun
        ((algebraMap R A : (a : R) → A) r) =
      (algebraMap R B : (a : R) → B) r
map_mem :
  ∀ {i : ι} {x : A},
    x ∈ 𝒜 i →
      Membership.mem (α := B) (ℬ i)
        (({ toFun := toFun, map_one' := map_one', map_mul' := map_mul', map_zero' := map_zero', map_add' := map_add',
                  commutes' := commutes' : A →ₐ[R] B }.toRingHom :
              (a : A) → B)
            x :
          B)
h :
  Eq (α := (a : A) → B)
    ((fun (f : 𝒜 →ₐᵍ[R] ℬ) ↦ (↑(↑f.toRingHom : A →* B) : OneHom A B).toFun)
      { toFun := toFun, map_one' := map_one', map_mul' := map_mul', map_zero' := map_zero', map_add' := map_add',
        commutes' := commutes', map_mem := @map_mem })
    ((fun (f : 𝒜 →ₐᵍ[R] ℬ) ↦ (↑(↑f.toRingHom : A →* B) : OneHom A B).toFun) g)
⊢ { toFun := toFun, map_one' := map_one', map_mul' := map_mul', map_zero' := map_zero', map_add' := map_add',
      commutes' := commutes', map_mem := @map_mem } =
    g
have rcases : ∀ (toFun_1 : A → B) (map_one'_1 : toFun_1 1 = 1)
  (map_mul'_1 :
    ∀ (x y : A),
      { toFun := toFun_1, map_one' := map_one'_1 : OneHom A B }.toFun (x * y) =
        { toFun := toFun_1, map_one' := map_one'_1 : OneHom A B }.toFun x *
          { toFun := toFun_1, map_one' := map_one'_1 : OneHom A B }.toFun y)
  (map_zero'_1 :
    (↑{ toFun := toFun_1, map_one' := map_one'_1, map_mul' := map_mul'_1 : A →* B } : OneHom A B).toFun 0 = 0)
  (map_add'_1 :
    ∀ (x y : A),
      (↑{ toFun := toFun_1, map_one' := map_one'_1, map_mul' := map_mul'_1 : A →* B } : OneHom A B).toFun (x + y) =
        (↑{ toFun := toFun_1, map_one' := map_one'_1, map_mul' := map_mul'_1 : A →* B } : OneHom A B).toFun x +
          (↑{ toFun := toFun_1, map_one' := map_one'_1, map_mul' := map_mul'_1 : A →* B } : OneHom A B).toFun y)
  (commutes'_1 :
    ∀ (r : R),
      (↑(↑{ toFun := toFun_1, map_one' := map_one'_1, map_mul' := map_mul'_1, map_zero' := map_zero'_1,
                      map_add' := map_add'_1 : A →+* B } :
                  A →* B) :
              OneHom A B).toFun
          ((algebraMap R A : (a : R) → A) r) =
        (algebraMap R B : (a : R) → B) r)
  (map_mem_1 :
    ∀ {i : ι} {x : A},
      x ∈ 𝒜 i →
        Membership.mem (α := B) (ℬ i)
          (({ toFun := toFun_1, map_one' := map_one'_1, map_mul' := map_mul'_1, map_zero' := map_zero'_1,
                    map_add' := map_add'_1, commutes' := commutes'_1 : A →ₐ[R] B }.toRingHom :
                (a : A) → B)
              x :
            B))
  (h :
    Eq (α := (a : A) → B)
      ((fun (f : 𝒜 →ₐᵍ[R] ℬ) ↦ (↑(↑f.toRingHom : A →* B) : OneHom A B).toFun)
        { toFun := toFun, map_one' := map_one', map_mul' := map_mul', map_zero' := map_zero', map_add' := map_add',
          commutes' := commutes', map_mem := @map_mem })
      ((fun (f : 𝒜 →ₐᵍ[R] ℬ) ↦ (↑(↑f.toRingHom : A →* B) : OneHom A B).toFun)
        { toFun := toFun_1, map_one' := map_one'_1, map_mul' := map_mul'_1, map_zero' := map_zero'_1,
          map_add' := map_add'_1, commutes' := commutes'_1, map_mem := @map_mem_1 })),
  Eq (α := 𝒜 →ₐᵍ[R] ℬ)
    { toFun := toFun, map_one' := map_one', map_mul' := map_mul', map_zero' := map_zero', map_add' := map_add',
      commutes' := commutes', map_mem := @map_mem }
    { toFun := toFun_1, map_one' := map_one'_1, map_mul' := map_mul'_1, map_zero' := map_zero'_1,
      map_add' := map_add'_1, commutes' := commutes'_1, map_mem := @map_mem_1 }
Tactic: rcases g with ⟨⟨⟨⟨⟨_, _⟩, _⟩, _, _⟩, _⟩, _⟩
Cleared hypotheses: g, h