Module: Mathlib.RingTheory.GradedAlgebra.AlgHom

Goal state before:
pp: 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✝¹³ : Semiring A
inst✝¹² : Semiring B
inst✝¹¹ : Semiring C
inst✝¹⁰ : Semiring D
inst✝⁹ : Algebra R A
inst✝⁸ : Algebra R B
inst✝⁷ : Algebra R C
inst✝⁶ : Algebra R D
inst✝⁵ : DecidableEq ι
inst✝⁴ : AddMonoid ι
𝒜 : ι → Submodule R A
ℬ : ι → Submodule R B
𝒞 : ι → Submodule R C
𝒟 : ι → Submodule R D
inst✝³ : GradedAlgebra 𝒜
inst✝² : GradedAlgebra ℬ
inst✝¹ : GradedAlgebra 𝒞
inst✝ : GradedAlgebra 𝒟
g : 𝒜 →ₐᵍ[R] ℬ
toFun✝ : A → B
map_one'✝ : toFun✝ 1 = 1
map_mul'✝ :
  ∀ (x y : A),
    { toFun := toFun✝, map_one' := map_one'✝ }.toFun (x * y) =
      { toFun := toFun✝, map_one' := map_one'✝ }.toFun x * { toFun := toFun✝, map_one' := map_one'✝ }.toFun y
map_zero'✝ : (↑{ toFun := toFun✝, map_one' := map_one'✝, map_mul' := map_mul'✝ }).toFun 0 = 0
map_add'✝ :
  ∀ (x y : A),
    (↑{ toFun := toFun✝, map_one' := map_one'✝, map_mul' := map_mul'✝ }).toFun (x + y) =
      (↑{ toFun := toFun✝, map_one' := map_one'✝, map_mul' := map_mul'✝ }).toFun x +
        (↑{ toFun := toFun✝, map_one' := map_one'✝, map_mul' := map_mul'✝ }).toFun y
commutes'✝ :
  ∀ (r : R),
    (↑↑{ toFun := toFun✝, map_one' := map_one'✝, map_mul' := map_mul'✝, map_zero' := map_zero'✝,
                map_add' := map_add'✝ }).toFun
        ((algebraMap R A) r) =
      (algebraMap R B) r
map_mem✝ :
  ∀ {i : ι} {x : A},
    x ∈ 𝒜 i →
      { toFun := toFun✝, map_one' := map_one'✝, map_mul' := map_mul'✝, map_zero' := map_zero'✝, map_add' := map_add'✝,
              commutes' := commutes'✝ }.toRingHom
          x ∈
        ℬ i
h :
  (fun f ↦ (↑↑f.toRingHom).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 ↦ (↑↑f.toRingHom).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

Tactic:
rcases g with ⟨⟨⟨⟨⟨_, _⟩, _⟩, _, _⟩, _⟩, _⟩

Goal state after:
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✝¹³ : Semiring A
inst✝¹² : Semiring B
inst✝¹¹ : Semiring C
inst✝¹⁰ : Semiring D
inst✝⁹ : Algebra R A
inst✝⁸ : Algebra R B
inst✝⁷ : Algebra R C
inst✝⁶ : Algebra R D
inst✝⁵ : DecidableEq ι
inst✝⁴ : AddMonoid ι
𝒜 : ι → Submodule R A
ℬ : ι → Submodule R B
𝒞 : ι → Submodule R C
𝒟 : ι → Submodule R D
inst✝³ : GradedAlgebra 𝒜
inst✝² : GradedAlgebra ℬ
inst✝¹ : GradedAlgebra 𝒞
inst✝ : GradedAlgebra 𝒟
toFun✝¹ : A → B
map_one'✝¹ : toFun✝¹ 1 = 1
map_mul'✝¹ :
  ∀ (x y : A),
    { toFun := toFun✝¹, map_one' := map_one'✝¹ }.toFun (x * y) =
      { toFun := toFun✝¹, map_one' := map_one'✝¹ }.toFun x * { toFun := toFun✝¹, map_one' := map_one'✝¹ }.toFun y
map_zero'✝¹ : (↑{ toFun := toFun✝¹, map_one' := map_one'✝¹, map_mul' := map_mul'✝¹ }).toFun 0 = 0
map_add'✝¹ :
  ∀ (x y : A),
    (↑{ toFun := toFun✝¹, map_one' := map_one'✝¹, map_mul' := map_mul'✝¹ }).toFun (x + y) =
      (↑{ toFun := toFun✝¹, map_one' := map_one'✝¹, map_mul' := map_mul'✝¹ }).toFun x +
        (↑{ toFun := toFun✝¹, map_one' := map_one'✝¹, map_mul' := map_mul'✝¹ }).toFun y
commutes'✝¹ :
  ∀ (r : R),
    (↑↑{ toFun := toFun✝¹, map_one' := map_one'✝¹, map_mul' := map_mul'✝¹, map_zero' := map_zero'✝¹,
                map_add' := map_add'✝¹ }).toFun
        ((algebraMap R A) r) =
      (algebraMap R B) r
map_mem✝¹ :
  ∀ {i : ι} {x : A},
    x ∈ 𝒜 i →
      { toFun := toFun✝¹, map_one' := map_one'✝¹, map_mul' := map_mul'✝¹, map_zero' := map_zero'✝¹,
              map_add' := map_add'✝¹, commutes' := commutes'✝¹ }.toRingHom
          x ∈
        ℬ i
toFun✝ : A → B
map_one'✝ : toFun✝ 1 = 1
map_mul'✝ :
  ∀ (x y : A),
    { toFun := toFun✝, map_one' := map_one'✝ }.toFun (x * y) =
      { toFun := toFun✝, map_one' := map_one'✝ }.toFun x * { toFun := toFun✝, map_one' := map_one'✝ }.toFun y
map_zero'✝ : (↑{ toFun := toFun✝, map_one' := map_one'✝, map_mul' := map_mul'✝ }).toFun 0 = 0
map_add'✝ :
  ∀ (x y : A),
    (↑{ toFun := toFun✝, map_one' := map_one'✝, map_mul' := map_mul'✝ }).toFun (x + y) =
      (↑{ toFun := toFun✝, map_one' := map_one'✝, map_mul' := map_mul'✝ }).toFun x +
        (↑{ toFun := toFun✝, map_one' := map_one'✝, map_mul' := map_mul'✝ }).toFun y
commutes'✝ :
  ∀ (r : R),
    (↑↑{ toFun := toFun✝, map_one' := map_one'✝, map_mul' := map_mul'✝, map_zero' := map_zero'✝,
                map_add' := map_add'✝ }).toFun
        ((algebraMap R A) r) =
      (algebraMap R B) r
map_mem✝ :
  ∀ {i : ι} {x : A},
    x ∈ 𝒜 i →
      { toFun := toFun✝, map_one' := map_one'✝, map_mul' := map_mul'✝, map_zero' := map_zero'✝, map_add' := map_add'✝,
              commutes' := commutes'✝ }.toRingHom
          x ∈
        ℬ i
h :
  (fun f ↦ (↑↑f.toRingHom).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 ↦ (↑↑f.toRingHom).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✝ }
⊢ { 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✝, map_one' := map_one'✝, map_mul' := map_mul'✝, map_zero' := map_zero'✝, map_add' := map_add'✝,
      commutes' := commutes'✝, map_mem := map_mem✝ }