Theorem: DirectSum.map_of (DividedPowers/ForMathlib/GradedRingQuot.lean)

State before:
ι : Type u_1
inst✝⁵ : DecidableEq ι
R : Type u_2
inst✝⁴ : Semiring R
β : ι → Type u_3
γ : ι → Type u_4
inst✝³ : (i : ι) → AddCommMonoid (β i)
inst✝² : (i : ι) → AddCommMonoid (γ i)
F : ι → Type u_5
inst✝¹ : (i : ι) → FunLike (F i) (β i) (γ i)
inst✝ : ∀ (i : ι), AddMonoidHomClass (F i) (β i) (γ i)
h : (i : ι) → F i
i : ι
x : β i
⊢ (map h) ((of β i) x) = (of γ i) ((h i) x)
Tactic:
simp only [map, toAddMonoid_of, AddMonoidHom.coe_comp, AddMonoidHom.coe_coe]
State after:
ι : Type u_1
inst✝⁵ : DecidableEq ι
R : Type u_2
inst✝⁴ : Semiring R
β : ι → Type u_3
γ : ι → Type u_4
inst✝³ : (i : ι) → AddCommMonoid (β i)
inst✝² : (i : ι) → AddCommMonoid (γ i)
F : ι → Type u_5
inst✝¹ : (i : ι) → FunLike (F i) (β i) (γ i)
inst✝ : ∀ (i : ι), AddMonoidHomClass (F i) (β i) (γ i)
h : (i : ι) → F i
i : ι
x : β i
⊢ (⇑(of (fun i => γ i) i) ∘ ⇑(h i)) x = (of γ i) ((h i) x)

State before:
ι : Type u_1
inst✝⁵ : DecidableEq ι
R : Type u_2
inst✝⁴ : Semiring R
β : ι → Type u_3
γ : ι → Type u_4
inst✝³ : (i : ι) → AddCommMonoid (β i)
inst✝² : (i : ι) → AddCommMonoid (γ i)
F : ι → Type u_5
inst✝¹ : (i : ι) → FunLike (F i) (β i) (γ i)
inst✝ : ∀ (i : ι), AddMonoidHomClass (F i) (β i) (γ i)
h : (i : ι) → F i
i : ι
x : β i
⊢ (⇑(of (fun i => γ i) i) ∘ ⇑(h i)) x = (of γ i) ((h i) x)
Tactic:
rfl
State after:
no goals