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)
h : (i : ι) → β i →+ γ i
i : ι
x : β i
⊢ (map' h) ((of β i) x) = (of γ i) ((h i) x)
Tactic:
simp only [map', toAddMonoid_of, AddMonoidHom.coe_comp]
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)
h : (i : ι) → β i →+ γ 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)
h : (i : ι) → β i →+ γ i
i : ι
x : β i
⊢ (⇑(of (fun i => γ i) i) ∘ ⇑(h i)) x = (of γ i) ((h i) x)
Tactic:
rfl
State after:
no goals