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)
h : (i : ι) → β i →+ γ i
x : ⨁ (i : ι), β i
i : ι
⊢ ((map' h) x) i = (h i) (x i)
Tactic:
let f : (⨁ i, β i) →+ γ 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, eq_self_iff_true, 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)
h : (i : ι) → β i →+ γ i
x : ⨁ (i : ι), β i
i : ι
f : (⨁ (i : ι), β i) →+ γ 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)
h : (i : ι) → β i →+ γ i
x : ⨁ (i : ι), β i
i : ι
f : (⨁ (i : ι), β i) →+ γ i := { toFun := fun x => ((map' h) x) i, map_zero' := ⋯, map_add' := ⋯ }
⊢ ((map' h) x) i = (h i) (x i)
Tactic:
let g : (⨁ i, β i) →+ γ 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, eq_self_iff_true, 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)
h : (i : ι) → β i →+ γ i
x : ⨁ (i : ι), β i
i : ι
f : (⨁ (i : ι), β i) →+ γ i := { toFun := fun x => ((map' h) x) i, map_zero' := ⋯, map_add' := ⋯ }
g : (⨁ (i : ι), β i) →+ γ 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)
h : (i : ι) → β i →+ γ i
x : ⨁ (i : ι), β i
i : ι
f : (⨁ (i : ι), β i) →+ γ i := { toFun := fun x => ((map' h) x) i, map_zero' := ⋯, map_add' := ⋯ }
g : (⨁ (i : ι), β i) →+ γ 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)
h : (i : ι) → β i →+ γ i
x : ⨁ (i : ι), β i
i : ι
f : (⨁ (i : ι), β i) →+ γ i := { toFun := fun x => ((map' h) x) i, map_zero' := ⋯, map_add' := ⋯ }
g : (⨁ (i : ι), β i) →+ γ 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)
h : (i : ι) → β i →+ γ i
x : ⨁ (i : ι), β i
i : ι
f : (⨁ (i : ι), β i) →+ γ i := { toFun := fun x => ((map' h) x) i, map_zero' := ⋯, map_add' := ⋯ }
g : (⨁ (i : ι), β i) →+ γ i := { toFun := fun y => (h i) (y i), map_zero' := ⋯, map_add' := ⋯ }
⊢ f x = g x
Tactic:
apply DFunLike.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)
h : (i : ι) → β i →+ γ i
x : ⨁ (i : ι), β i
i : ι
f : (⨁ (i : ι), β i) →+ γ i := { toFun := fun x => ((map' h) x) i, map_zero' := ⋯, map_add' := ⋯ }
g : (⨁ (i : ι), β i) →+ γ i := { toFun := fun y => (h i) (y i), map_zero' := ⋯, map_add' := ⋯ }
⊢ f = g

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)
h : (i : ι) → β i →+ γ i
x : ⨁ (i : ι), β i
i : ι
f : (⨁ (i : ι), β i) →+ γ i := { toFun := fun x => ((map' h) x) i, map_zero' := ⋯, map_add' := ⋯ }
g : (⨁ (i : ι), β i) →+ γ i := { toFun := fun y => (h i) (y i), map_zero' := ⋯, map_add' := ⋯ }
⊢ f = g
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)
h : (i : ι) → β i →+ γ i
x : ⨁ (i : ι), β i
i : ι
f : (⨁ (i : ι), β i) →+ γ i := { toFun := fun x => ((map' h) x) i, map_zero' := ⋯, map_add' := ⋯ }
g : (⨁ (i : ι), β i) →+ γ i := { toFun := fun y => (h i) (y i), map_zero' := ⋯, map_add' := ⋯ }
j : ι
y : β j
⊢ (f.comp (of (fun i => β i) j)) y = (g.comp (of (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)
h : (i : ι) → β i →+ γ i
x : ⨁ (i : ι), β i
i : ι
f : (⨁ (i : ι), β i) →+ γ i := { toFun := fun x => ((map' h) x) i, map_zero' := ⋯, map_add' := ⋯ }
g : (⨁ (i : ι), β i) →+ γ i := { toFun := fun y => (h i) (y i), map_zero' := ⋯, map_add' := ⋯ }
j : ι
y : β j
⊢ (f.comp (of (fun i => β i) j)) y = (g.comp (of (fun i => β i) j)) y
Tactic:
simp only [f, g, AddMonoidHom.coe_comp, AddMonoidHom.coe_mk, ZeroHom.coe_mk, comp_apply,
  map'_of]
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)
h : (i : ι) → β i →+ γ i
x : ⨁ (i : ι), β i
i : ι
f : (⨁ (i : ι), β i) →+ γ i := { toFun := fun x => ((map' h) x) i, map_zero' := ⋯, map_add' := ⋯ }
g : (⨁ (i : ι), β i) →+ γ 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₁.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)
h : (i : ι) → β i →+ γ i
x : ⨁ (i : ι), β i
i : ι
f : (⨁ (i : ι), β i) →+ γ i := { toFun := fun x => ((map' h) x) i, map_zero' := ⋯, map_add' := ⋯ }
g : (⨁ (i : ι), β i) →+ γ 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)
h : (i : ι) → β i →+ γ i
x : ⨁ (i : ι), β i
i : ι
f : (⨁ (i : ι), β i) →+ γ i := { toFun := fun x => ((map' h) x) i, map_zero' := ⋯, map_add' := ⋯ }
g : (⨁ (i : ι), β i) →+ γ 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)
h : (i : ι) → β i →+ γ i
x : ⨁ (i : ι), β i
i : ι
f : (⨁ (i : ι), β i) →+ γ i := { toFun := fun x => ((map' h) x) i, map_zero' := ⋯, map_add' := ⋯ }
g : (⨁ (i : ι), β i) →+ γ 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)
h : (i : ι) → β i →+ γ i
x : ⨁ (i : ι), β i
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)
h : (i : ι) → β i →+ γ i
x : ⨁ (i : ι), β i
i : ι
⊢ ∀ (x y : ⨁ (i : ι), β i),
    { 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, eq_self_iff_true, 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)
h : (i : ι) → β i →+ γ i
x : ⨁ (i : ι), β i
i : ι
f : (⨁ (i : ι), β i) →+ γ 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)
h : (i : ι) → β i →+ γ i
x : ⨁ (i : ι), β i
i : ι
f : (⨁ (i : ι), β i) →+ γ i := { toFun := fun x => ((map' h) x) i, map_zero' := ⋯, map_add' := ⋯ }
⊢ ∀ (x y : ⨁ (i : ι), β i),
    { 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, eq_self_iff_true, forall_const]
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)
h : (i : ι) → β i →+ γ i
x : ⨁ (i : ι), β i
i : ι
f : (⨁ (i : ι), β i) →+ γ i := { toFun := fun x => ((map' h) x) i, map_zero' := ⋯, map_add' := ⋯ }
g : (⨁ (i : ι), β i) →+ γ 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)
h : (i : ι) → β i →+ γ i
x : ⨁ (i : ι), β i
i : ι
f : (⨁ (i : ι), β i) →+ γ i := { toFun := fun x => ((map' h) x) i, map_zero' := ⋯, map_add' := ⋯ }
g : (⨁ (i : ι), β i) →+ γ 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)
h : (i : ι) → β i →+ γ i
x : ⨁ (i : ι), β i
i : ι
f : (⨁ (i : ι), β i) →+ γ i := { toFun := fun x => ((map' h) x) i, map_zero' := ⋯, map_add' := ⋯ }
g : (⨁ (i : ι), β i) →+ γ 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)
h : (i : ι) → β i →+ γ i
x : ⨁ (i : ι), β i
i : ι
f : (⨁ (i : ι), β i) →+ γ i := { toFun := fun x => ((map' h) x) i, map_zero' := ⋯, map_add' := ⋯ }
g : (⨁ (i : ι), β i) →+ γ 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