Theorem: DirectSum.map_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)
F : ι → Type u_5
inst✝¹ : (i : ι) → FunLike (F i) (β i) (γ i)
inst✝ : ∀ (i : ι), AddMonoidHomClass (F i) (β i) (γ i)
h : (i : ι) → F i
x : DirectSum ι β
i : ι
⊢ ((map h) x) i = (h i) (x i)
Tactic:
let f : DirectSum ι β →+ γ i :=
{ toFun := fun x => map h x i
  map_zero' := by simp only [map_zero, zero_apply]
  map_add' := by simp only [map_add, add_apply, forall_const] }
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
x : DirectSum ι β
i : ι
f : DirectSum ι β →+ γ i := { toFun := fun x => ((map h) x) i, map_zero' := ⋯, map_add' := ⋯ }
⊢ ((map h) x) i = (h i) (x i)

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
x : DirectSum ι β
i : ι
f : DirectSum ι β →+ γ i := { toFun := fun x => ((map h) x) i, map_zero' := ⋯, map_add' := ⋯ }
⊢ ((map h) x) i = (h i) (x i)
Tactic:
let g : DirectSum ι β →+ γ i :=
{ toFun := fun y => h i (y i)
  map_zero' := by simp only [zero_apply, map_zero]
  map_add' := by simp only [add_apply, map_add, forall_const] }
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
x : DirectSum ι β
i : ι
f : DirectSum ι β →+ γ i := { toFun := fun x => ((map h) x) i, map_zero' := ⋯, map_add' := ⋯ }
g : DirectSum ι β →+ γ i := { toFun := fun y => (h i) (y i), map_zero' := ⋯, map_add' := ⋯ }
⊢ ((map h) x) i = (h i) (x i)

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
x : DirectSum ι β
i : ι
f : DirectSum ι β →+ γ i := { toFun := fun x => ((map h) x) i, map_zero' := ⋯, map_add' := ⋯ }
g : DirectSum ι β →+ γ i := { toFun := fun y => (h i) (y i), map_zero' := ⋯, map_add' := ⋯ }
⊢ ((map h) x) i = (h i) (x i)
Tactic:
change f x = g x
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
x : DirectSum ι β
i : ι
f : DirectSum ι β →+ γ i := { toFun := fun x => ((map h) x) i, map_zero' := ⋯, map_add' := ⋯ }
g : DirectSum ι β →+ γ i := { toFun := fun y => (h i) (y i), map_zero' := ⋯, map_add' := ⋯ }
⊢ f x = g 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
x : DirectSum ι β
i : ι
f : DirectSum ι β →+ γ i := { toFun := fun x => ((map h) x) i, map_zero' := ⋯, map_add' := ⋯ }
g : DirectSum ι β →+ γ i := { toFun := fun y => (h i) (y i), map_zero' := ⋯, map_add' := ⋯ }
⊢ f x = g x
Tactic:
suffices f = g by
  rw [this]
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
x : DirectSum ι β
i : ι
f : DirectSum ι β →+ γ i := { toFun := fun x => ((map h) x) i, map_zero' := ⋯, map_add' := ⋯ }
g : DirectSum ι β →+ γ i := { toFun := fun y => (h i) (y i), map_zero' := ⋯, map_add' := ⋯ }
⊢ f = g

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
x : DirectSum ι β
i : ι
f : DirectSum ι β →+ γ i := { toFun := fun x => ((map h) x) i, map_zero' := ⋯, map_add' := ⋯ }
g : DirectSum ι β →+ γ i := { toFun := fun y => (h i) (y i), map_zero' := ⋯, map_add' := ⋯ }
⊢ f = g
Tactic:
apply addHom_ext
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)
F : ι → Type u_5
inst✝¹ : (i : ι) → FunLike (F i) (β i) (γ i)
inst✝ : ∀ (i : ι), AddMonoidHomClass (F i) (β i) (γ i)
h : (i : ι) → F i
x : DirectSum ι β
i : ι
f : DirectSum ι β →+ γ i := { toFun := fun x => ((map h) x) i, map_zero' := ⋯, map_add' := ⋯ }
g : DirectSum ι β →+ γ i := { toFun := fun y => (h i) (y i), map_zero' := ⋯, map_add' := ⋯ }
⊢ ∀ (i_1 : ι) (y : β i_1), f ((of (fun i => β i) i_1) y) = g ((of (fun i => β i) i_1) y)

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)
F : ι → Type u_5
inst✝¹ : (i : ι) → FunLike (F i) (β i) (γ i)
inst✝ : ∀ (i : ι), AddMonoidHomClass (F i) (β i) (γ i)
h : (i : ι) → F i
x : DirectSum ι β
i : ι
f : DirectSum ι β →+ γ i := { toFun := fun x => ((map h) x) i, map_zero' := ⋯, map_add' := ⋯ }
g : DirectSum ι β →+ γ i := { toFun := fun y => (h i) (y i), map_zero' := ⋯, map_add' := ⋯ }
⊢ ∀ (i_1 : ι) (y : β i_1), f ((of (fun i => β i) i_1) y) = g ((of (fun i => β i) i_1) y)
Tactic:
intros j y
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)
F : ι → Type u_5
inst✝¹ : (i : ι) → FunLike (F i) (β i) (γ i)
inst✝ : ∀ (i : ι), AddMonoidHomClass (F i) (β i) (γ i)
h : (i : ι) → F i
x : DirectSum ι β
i : ι
f : DirectSum ι β →+ γ i := { toFun := fun x => ((map h) x) i, map_zero' := ⋯, map_add' := ⋯ }
g : DirectSum ι β →+ γ i := { toFun := fun y => (h i) (y i), map_zero' := ⋯, map_add' := ⋯ }
j : ι
y : β j
⊢ f ((of (fun i => β i) j) y) = g ((of (fun i => β i) j) y)

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)
F : ι → Type u_5
inst✝¹ : (i : ι) → FunLike (F i) (β i) (γ i)
inst✝ : ∀ (i : ι), AddMonoidHomClass (F i) (β i) (γ i)
h : (i : ι) → F i
x : DirectSum ι β
i : ι
f : DirectSum ι β →+ γ i := { toFun := fun x => ((map h) x) i, map_zero' := ⋯, map_add' := ⋯ }
g : DirectSum ι β →+ γ i := { toFun := fun y => (h i) (y i), map_zero' := ⋯, map_add' := ⋯ }
j : ι
y : β j
⊢ f ((of (fun i => β i) j) y) = g ((of (fun i => β i) j) y)
Tactic:
simp only [AddMonoidHom.coe_mk, ZeroHom.coe_mk, map_of, f, g]
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)
F : ι → Type u_5
inst✝¹ : (i : ι) → FunLike (F i) (β i) (γ i)
inst✝ : ∀ (i : ι), AddMonoidHomClass (F i) (β i) (γ i)
h : (i : ι) → F i
x : DirectSum ι β
i : ι
f : DirectSum ι β →+ γ i := { toFun := fun x => ((map h) x) i, map_zero' := ⋯, map_add' := ⋯ }
g : DirectSum ι β →+ γ i := { toFun := fun y => (h i) (y i), map_zero' := ⋯, map_add' := ⋯ }
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
ι : 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
x : DirectSum ι β
i : ι
f : DirectSum ι β →+ γ i := { toFun := fun x => ((map h) x) i, map_zero' := ⋯, map_add' := ⋯ }
g : DirectSum ι β →+ γ i := { toFun := fun y => (h i) (y i), map_zero' := ⋯, map_add' := ⋯ }
j : ι
y : β j
⊢ ((of (fun i => γ i) j) ((h j) y)) i = (h i) (((of (fun i => β i) j) y) i)
Tactic:
by_cases hj : 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)
F : ι → Type u_5
inst✝¹ : (i : ι) → FunLike (F i) (β i) (γ i)
inst✝ : ∀ (i : ι), AddMonoidHomClass (F i) (β i) (γ i)
h : (i : ι) → F i
x : DirectSum ι β
i : ι
f : DirectSum ι β →+ γ i := { toFun := fun x => ((map h) x) i, map_zero' := ⋯, map_add' := ⋯ }
g : DirectSum ι β →+ γ i := { toFun := fun y => (h i) (y i), map_zero' := ⋯, map_add' := ⋯ }
j : ι
y : β j
hj : 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)
F : ι → Type u_5
inst✝¹ : (i : ι) → FunLike (F i) (β i) (γ i)
inst✝ : ∀ (i : ι), AddMonoidHomClass (F i) (β i) (γ i)
h : (i : ι) → F i
x : DirectSum ι β
i : ι
f : DirectSum ι β →+ γ i := { toFun := fun x => ((map h) x) i, map_zero' := ⋯, map_add' := ⋯ }
g : DirectSum ι β →+ γ i := { toFun := fun y => (h i) (y i), map_zero' := ⋯, map_add' := ⋯ }
j : ι
y : β j
hj : ¬j = i
⊢ ((of (fun i => γ i) j) ((h j) y)) i = (h i) (((of (fun i => β i) j) y) i)

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
x : DirectSum ι β
i : ι
⊢ (fun x => ((map h) x) i) 0 = 0
Tactic:
simp only [map_zero, zero_apply]
State after:
no goals

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
x : DirectSum ι β
i : ι
⊢ ∀ (x y : DirectSum ι β),
    { toFun := fun x => ((map h) x) i, map_zero' := ⋯ }.toFun (x + y) =
      { toFun := fun x => ((map h) x) i, map_zero' := ⋯ }.toFun x +
        { toFun := fun x => ((map h) x) i, map_zero' := ⋯ }.toFun y
Tactic:
simp only [map_add, add_apply, forall_const]
State after:
no goals

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
x : DirectSum ι β
i : ι
f : DirectSum ι β →+ γ i := { toFun := fun x => ((map h) x) i, map_zero' := ⋯, map_add' := ⋯ }
⊢ (fun y => (h i) (y i)) 0 = 0
Tactic:
simp only [zero_apply, map_zero]
State after:
no goals

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
x : DirectSum ι β
i : ι
f : DirectSum ι β →+ γ i := { toFun := fun x => ((map h) x) i, map_zero' := ⋯, map_add' := ⋯ }
⊢ ∀ (x y : DirectSum ι β),
    { toFun := fun y => (h i) (y i), map_zero' := ⋯ }.toFun (x + y) =
      { toFun := fun y => (h i) (y i), map_zero' := ⋯ }.toFun x +
        { toFun := fun y => (h i) (y i), map_zero' := ⋯ }.toFun y
Tactic:
simp only [add_apply, map_add, forall_const]
State after:
no goals

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
x : DirectSum ι β
i : ι
f : DirectSum ι β →+ γ i := { toFun := fun x => ((map h) x) i, map_zero' := ⋯, map_add' := ⋯ }
g : DirectSum ι β →+ γ i := { toFun := fun y => (h i) (y i), map_zero' := ⋯, map_add' := ⋯ }
this : f = g
⊢ f x = g x
Tactic:
rw [this]
State after:
no goals

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)
F : ι → Type u_5
inst✝¹ : (i : ι) → FunLike (F i) (β i) (γ i)
inst✝ : ∀ (i : ι), AddMonoidHomClass (F i) (β i) (γ i)
h : (i : ι) → F i
x : DirectSum ι β
i : ι
f : DirectSum ι β →+ γ i := { toFun := fun x => ((map h) x) i, map_zero' := ⋯, map_add' := ⋯ }
g : DirectSum ι β →+ γ i := { toFun := fun y => (h i) (y i), map_zero' := ⋯, map_add' := ⋯ }
j : ι
y : β j
hj : j = i
⊢ ((of (fun i => γ i) j) ((h j) y)) i = (h i) (((of (fun i => β i) j) y) i)
Tactic:
rw [← hj]
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)
F : ι → Type u_5
inst✝¹ : (i : ι) → FunLike (F i) (β i) (γ i)
inst✝ : ∀ (i : ι), AddMonoidHomClass (F i) (β i) (γ i)
h : (i : ι) → F i
x : DirectSum ι β
i : ι
f : DirectSum ι β →+ γ i := { toFun := fun x => ((map h) x) i, map_zero' := ⋯, map_add' := ⋯ }
g : DirectSum ι β →+ γ i := { toFun := fun y => (h i) (y i), map_zero' := ⋯, map_add' := ⋯ }
j : ι
y : β j
hj : 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)
F : ι → Type u_5
inst✝¹ : (i : ι) → FunLike (F i) (β i) (γ i)
inst✝ : ∀ (i : ι), AddMonoidHomClass (F i) (β i) (γ i)
h : (i : ι) → F i
x : DirectSum ι β
i : ι
f : DirectSum ι β →+ γ i := { toFun := fun x => ((map h) x) i, map_zero' := ⋯, map_add' := ⋯ }
g : DirectSum ι β →+ γ i := { toFun := fun y => (h i) (y i), map_zero' := ⋯, map_add' := ⋯ }
j : ι
y : β j
hj : 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)
F : ι → Type u_5
inst✝¹ : (i : ι) → FunLike (F i) (β i) (γ i)
inst✝ : ∀ (i : ι), AddMonoidHomClass (F i) (β i) (γ i)
h : (i : ι) → F i
x : DirectSum ι β
i : ι
f : DirectSum ι β →+ γ i := { toFun := fun x => ((map h) x) i, map_zero' := ⋯, map_add' := ⋯ }
g : DirectSum ι β →+ γ i := { toFun := fun y => (h i) (y i), map_zero' := ⋯, map_add' := ⋯ }
j : ι
y : β j
hj : ¬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 _ hj, map_zero]
State after:
no goals