Theorem: DirectSum.lmap'_apply (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
x : ⨁ (i : ι), β i
i : ι
⊢ ((lmap' h) x) i = (h i) (x i)
Tactic:
simp only [apply_eq_component R, ← LinearMap.comp_apply]
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
x : ⨁ (i : ι), β i
i : ι
⊢ (component R ι (fun i => γ i) i ∘ₗ lmap' h) x = (h i ∘ₗ component R ι (fun i => β i) 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
x : ⨁ (i : ι), β i
i : ι
⊢ (component R ι (fun i => γ i) i ∘ₗ lmap' h) x = (h i ∘ₗ component R ι (fun i => β i) 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
inst✝³ : (i : ι) → AddCommMonoid (β i)
inst✝² : (i : ι) → AddCommMonoid (γ i)
inst✝¹ : (i : ι) → Module R (β i)
inst✝ : (i : ι) → Module R (γ i)
h : (i : ι) → β i →ₗ[R] γ i
x : ⨁ (i : ι), β i
i : ι
⊢ component R ι (fun i => γ i) i ∘ₗ lmap' h = h i ∘ₗ component R ι (fun i => β i) i

State before:
case h
ι : 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
x : ⨁ (i : ι), β i
i : ι
⊢ component R ι (fun i => γ i) i ∘ₗ lmap' h = h i ∘ₗ component R ι (fun i => β i) i
Tactic:
ext j 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
inst✝³ : (i : ι) → AddCommMonoid (β i)
inst✝² : (i : ι) → AddCommMonoid (γ i)
inst✝¹ : (i : ι) → Module R (β i)
inst✝ : (i : ι) → Module R (γ i)
h : (i : ι) → β i →ₗ[R] γ i
x : ⨁ (i : ι), β i
i j : ι
y : β j
⊢ ((component R ι (fun i => γ i) i ∘ₗ lmap' h) ∘ₗ lof R ι (fun i => β i) j) y =
    ((h i ∘ₗ component R ι (fun i => β i) i) ∘ₗ lof R ι (fun i => β i) j) 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
inst✝³ : (i : ι) → AddCommMonoid (β i)
inst✝² : (i : ι) → AddCommMonoid (γ i)
inst✝¹ : (i : ι) → Module R (β i)
inst✝ : (i : ι) → Module R (γ i)
h : (i : ι) → β i →ₗ[R] γ i
x : ⨁ (i : ι), β i
i j : ι
y : β j
⊢ ((component R ι (fun i => γ i) i ∘ₗ lmap' h) ∘ₗ lof R ι (fun i => β i) j) y =
    ((h i ∘ₗ component R ι (fun i => β i) i) ∘ₗ lof R ι (fun i => β i) j) y
Tactic:
simp only [LinearMap.comp_apply, lmap'_lof]
State after:
case h.H.h
ι : 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
x : ⨁ (i : ι), β i
i j : ι
y : β j
⊢ (component R ι (fun i => γ i) i) ((lof R ι (fun i => γ i) j) ((h j) y)) =
    (h i) ((component R ι (fun i => β i) i) ((lof R ι (fun i => β i) j) 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
inst✝³ : (i : ι) → AddCommMonoid (β i)
inst✝² : (i : ι) → AddCommMonoid (γ i)
inst✝¹ : (i : ι) → Module R (β i)
inst✝ : (i : ι) → Module R (γ i)
h : (i : ι) → β i →ₗ[R] γ i
x : ⨁ (i : ι), β i
i j : ι
y : β j
⊢ (component R ι (fun i => γ i) i) ((lof R ι (fun i => γ i) j) ((h j) y)) =
    (h i) ((component R ι (fun i => β i) i) ((lof R ι (fun i => β i) j) y))
Tactic:
simp only [lof_eq_of, ← apply_eq_component]
State after:
case h.H.h
ι : 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
x : ⨁ (i : ι), β i
i j : ι
y : β j
⊢ ((of (fun i => γ i) j) ((h j) y)) i = (h i) (((of (fun i => β i) j) y) i)

State before:
case h.H.h
ι : 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
x : ⨁ (i : ι), β i
i j : ι
y : β j
⊢ ((of (fun i => γ i) j) ((h j) y)) i = (h i) (((of (fun i => β i) j) y) i)
Tactic:
by_cases hji : j = i
State after:
case pos
ι : 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
x : ⨁ (i : ι), β i
i j : ι
y : β j
hji : j = i
⊢ ((of (fun i => γ i) j) ((h j) y)) i = (h i) (((of (fun i => β i) j) y) i)

case neg
ι : 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
x : ⨁ (i : ι), β i
i j : ι
y : β j
hji : ¬j = i
⊢ ((of (fun i => γ i) j) ((h j) y)) i = (h i) (((of (fun i => β i) j) y) i)

State before:
case pos
ι : 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
x : ⨁ (i : ι), β i
i j : ι
y : β j
hji : j = i
⊢ ((of (fun i => γ i) j) ((h j) y)) i = (h i) (((of (fun i => β i) j) y) i)
Tactic:
rw [← hji]
State after:
case pos
ι : 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
x : ⨁ (i : ι), β i
i j : ι
y : β j
hji : j = i
⊢ ((of (fun i => γ i) j) ((h j) y)) j = (h j) (((of (fun i => β i) j) y) j)

State before:
case pos
ι : 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
x : ⨁ (i : ι), β i
i j : ι
y : β j
hji : j = i
⊢ ((of (fun i => γ i) j) ((h j) y)) j = (h j) (((of (fun i => β i) j) y) j)
Tactic:
simp only [of_eq_same]
State after:
no goals

State before:
case neg
ι : 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
x : ⨁ (i : ι), β i
i j : ι
y : β j
hji : ¬j = i
⊢ ((of (fun i => γ i) j) ((h j) y)) i = (h i) (((of (fun i => β i) j) y) i)
Tactic:
simp only [of_eq_of_ne _ j i _ hji, map_zero]
State after:
no goals