Theorem: DirectSum.lmap'_lof (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)
inst✝¹ : (i : ι) → Module R (β i)
inst✝ : (i : ι) → Module R (γ i)
h : (i : ι) → β i →ₗ[R] γ i
i : ι
x : β i
⊢ (lmap' h) ((lof R ι β i) x) = (lof R ι γ i) ((h i) x)
Tactic:
simp only [lmap', toModule_lof, LinearMap.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)
inst✝¹ : (i : ι) → Module R (β i)
inst✝ : (i : ι) → Module R (γ i)
h : (i : ι) → β i →ₗ[R] γ i
i : ι
x : β i
⊢ (⇑(lof R ι (fun i => γ i) i) ∘ ⇑(h i)) x = (lof R ι γ 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)
inst✝¹ : (i : ι) → Module R (β i)
inst✝ : (i : ι) → Module R (γ i)
h : (i : ι) → β i →ₗ[R] γ i
i : ι
x : β i
⊢ (⇑(lof R ι (fun i => γ i) i) ∘ ⇑(h i)) x = (lof R ι γ i) ((h i) x)
Tactic:
rfl
State after:
no goals