Theorem: DirectSum.toModule_comp_lmap'_eq (DividedPowers/ForMathlib/GradedRingQuot.lean)

State before:
ι : Type u_1
inst✝⁷ : DecidableEq ι
R : Type u_2
inst✝⁶ : Semiring R
β : ι → Type u_3
γ : ι → Type u_4
δ : Type u_5
inst✝⁵ : (i : ι) → AddCommMonoid (β i)
inst✝⁴ : (i : ι) → AddCommMonoid (γ i)
inst✝³ : AddCommMonoid δ
inst✝² : (i : ι) → Module R (β i)
inst✝¹ : (i : ι) → Module R (γ i)
inst✝ : Module R δ
h : (i : ι) → β i →ₗ[R] γ i
f : (i : ι) → γ i →ₗ[R] δ
x : ⨁ (i : ι), β i
⊢ (toModule R ι δ f) ((lmap' h) x) = (toModule R ι δ fun i => f i ∘ₗ h i) x
Tactic:
rw [← LinearMap.comp_apply]
State after:
ι : Type u_1
inst✝⁷ : DecidableEq ι
R : Type u_2
inst✝⁶ : Semiring R
β : ι → Type u_3
γ : ι → Type u_4
δ : Type u_5
inst✝⁵ : (i : ι) → AddCommMonoid (β i)
inst✝⁴ : (i : ι) → AddCommMonoid (γ i)
inst✝³ : AddCommMonoid δ
inst✝² : (i : ι) → Module R (β i)
inst✝¹ : (i : ι) → Module R (γ i)
inst✝ : Module R δ
h : (i : ι) → β i →ₗ[R] γ i
f : (i : ι) → γ i →ₗ[R] δ
x : ⨁ (i : ι), β i
⊢ (toModule R ι δ f ∘ₗ lmap' h) x = (toModule R ι δ fun i => f i ∘ₗ h i) x

State before:
ι : Type u_1
inst✝⁷ : DecidableEq ι
R : Type u_2
inst✝⁶ : Semiring R
β : ι → Type u_3
γ : ι → Type u_4
δ : Type u_5
inst✝⁵ : (i : ι) → AddCommMonoid (β i)
inst✝⁴ : (i : ι) → AddCommMonoid (γ i)
inst✝³ : AddCommMonoid δ
inst✝² : (i : ι) → Module R (β i)
inst✝¹ : (i : ι) → Module R (γ i)
inst✝ : Module R δ
h : (i : ι) → β i →ₗ[R] γ i
f : (i : ι) → γ i →ₗ[R] δ
x : ⨁ (i : ι), β i
⊢ (toModule R ι δ f ∘ₗ lmap' h) x = (toModule R ι δ fun i => f i ∘ₗ h i) x
Tactic:
apply LinearMap.congr_fun
State after:
case h
ι : Type u_1
inst✝⁷ : DecidableEq ι
R : Type u_2
inst✝⁶ : Semiring R
β : ι → Type u_3
γ : ι → Type u_4
δ : Type u_5
inst✝⁵ : (i : ι) → AddCommMonoid (β i)
inst✝⁴ : (i : ι) → AddCommMonoid (γ i)
inst✝³ : AddCommMonoid δ
inst✝² : (i : ι) → Module R (β i)
inst✝¹ : (i : ι) → Module R (γ i)
inst✝ : Module R δ
h : (i : ι) → β i →ₗ[R] γ i
f : (i : ι) → γ i →ₗ[R] δ
x : ⨁ (i : ι), β i
⊢ toModule R ι δ f ∘ₗ lmap' h = toModule R ι δ fun i => f i ∘ₗ h i

State before:
case h
ι : Type u_1
inst✝⁷ : DecidableEq ι
R : Type u_2
inst✝⁶ : Semiring R
β : ι → Type u_3
γ : ι → Type u_4
δ : Type u_5
inst✝⁵ : (i : ι) → AddCommMonoid (β i)
inst✝⁴ : (i : ι) → AddCommMonoid (γ i)
inst✝³ : AddCommMonoid δ
inst✝² : (i : ι) → Module R (β i)
inst✝¹ : (i : ι) → Module R (γ i)
inst✝ : Module R δ
h : (i : ι) → β i →ₗ[R] γ i
f : (i : ι) → γ i →ₗ[R] δ
x : ⨁ (i : ι), β i
⊢ toModule R ι δ f ∘ₗ lmap' h = toModule R ι δ fun i => f i ∘ₗ h i
Tactic:
ext i y
State after:
case h.H.h
ι : Type u_1
inst✝⁷ : DecidableEq ι
R : Type u_2
inst✝⁶ : Semiring R
β : ι → Type u_3
γ : ι → Type u_4
δ : Type u_5
inst✝⁵ : (i : ι) → AddCommMonoid (β i)
inst✝⁴ : (i : ι) → AddCommMonoid (γ i)
inst✝³ : AddCommMonoid δ
inst✝² : (i : ι) → Module R (β i)
inst✝¹ : (i : ι) → Module R (γ i)
inst✝ : Module R δ
h : (i : ι) → β i →ₗ[R] γ i
f : (i : ι) → γ i →ₗ[R] δ
x : ⨁ (i : ι), β i
i : ι
y : β i
⊢ ((toModule R ι δ f ∘ₗ lmap' h) ∘ₗ lof R ι (fun i => β i) i) y =
    ((toModule R ι δ fun i => f i ∘ₗ h i) ∘ₗ lof R ι (fun i => β i) i) y

State before:
case h.H.h
ι : Type u_1
inst✝⁷ : DecidableEq ι
R : Type u_2
inst✝⁶ : Semiring R
β : ι → Type u_3
γ : ι → Type u_4
δ : Type u_5
inst✝⁵ : (i : ι) → AddCommMonoid (β i)
inst✝⁴ : (i : ι) → AddCommMonoid (γ i)
inst✝³ : AddCommMonoid δ
inst✝² : (i : ι) → Module R (β i)
inst✝¹ : (i : ι) → Module R (γ i)
inst✝ : Module R δ
h : (i : ι) → β i →ₗ[R] γ i
f : (i : ι) → γ i →ₗ[R] δ
x : ⨁ (i : ι), β i
i : ι
y : β i
⊢ ((toModule R ι δ f ∘ₗ lmap' h) ∘ₗ lof R ι (fun i => β i) i) y =
    ((toModule R ι δ fun i => f i ∘ₗ h i) ∘ₗ lof R ι (fun i => β i) i) y
Tactic:
simp only [LinearMap.coe_comp, comp_apply, lmap'_lof, toModule_lof]
State after:
no goals