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)
inst✝² : (i : ι) → (x : β i) → Decidable (x ≠ 0)
F : ι → Type u_5
inst✝¹ : (i : ι) → FunLike (F i) (β i) (γ i)
inst✝ : ∀ (i : ι), AddMonoidHomClass (F i) (β i) (γ i)
h : (i : ι) → F i
x : ⨁ (i : ι), β i
⊢ (map h) x = (mk γ (DFinsupp.support x)) fun i => (h ↑i) (x ↑i)
Tactic:
conv_lhs => rw [← sum_support_of β 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)
inst✝² : (i : ι) → (x : β i) → Decidable (x ≠ 0)
F : ι → Type u_5
inst✝¹ : (i : ι) → FunLike (F i) (β i) (γ i)
inst✝ : ∀ (i : ι), AddMonoidHomClass (F i) (β i) (γ i)
h : (i : ι) → F i
x : ⨁ (i : ι), β i
⊢ (map h) (∑ i ∈ DFinsupp.support x, (of β i) (x i)) = (mk γ (DFinsupp.support x)) fun 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)
inst✝² : (i : ι) → (x : β i) → Decidable (x ≠ 0)
F : ι → Type u_5
inst✝¹ : (i : ι) → FunLike (F i) (β i) (γ i)
inst✝ : ∀ (i : ι), AddMonoidHomClass (F i) (β i) (γ i)
h : (i : ι) → F i
x : ⨁ (i : ι), β i
⊢ (map h) (∑ i ∈ DFinsupp.support x, (of β i) (x i)) = (mk γ (DFinsupp.support x)) fun i => (h ↑i) (x ↑i)
Tactic:
simp_rw [map_sum, map_of]
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 : ι) → (x : β i) → Decidable (x ≠ 0)
F : ι → Type u_5
inst✝¹ : (i : ι) → FunLike (F i) (β i) (γ i)
inst✝ : ∀ (i : ι), AddMonoidHomClass (F i) (β i) (γ i)
h : (i : ι) → F i
x : ⨁ (i : ι), β i
⊢ ∑ x_1 ∈ DFinsupp.support x, (of (fun i => γ i) x_1) ((h x_1) (x x_1)) =
    (mk γ (DFinsupp.support x)) fun 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)
inst✝² : (i : ι) → (x : β i) → Decidable (x ≠ 0)
F : ι → Type u_5
inst✝¹ : (i : ι) → FunLike (F i) (β i) (γ i)
inst✝ : ∀ (i : ι), AddMonoidHomClass (F i) (β i) (γ i)
h : (i : ι) → F i
x : ⨁ (i : ι), β i
⊢ ∑ x_1 ∈ DFinsupp.support x, (of (fun i => γ i) x_1) ((h x_1) (x x_1)) =
    (mk γ (DFinsupp.support x)) fun i => (h ↑i) (x ↑i)
Tactic:
rw [eq_comm]
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 : ι) → (x : β i) → Decidable (x ≠ 0)
F : ι → Type u_5
inst✝¹ : (i : ι) → FunLike (F i) (β i) (γ i)
inst✝ : ∀ (i : ι), AddMonoidHomClass (F i) (β i) (γ i)
h : (i : ι) → F i
x : ⨁ (i : ι), β i
⊢ ((mk γ (DFinsupp.support x)) fun i => (h ↑i) (x ↑i)) =
    ∑ x_1 ∈ DFinsupp.support x, (of (fun i => γ i) x_1) ((h x_1) (x x_1))

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 : ι) → (x : β i) → Decidable (x ≠ 0)
F : ι → Type u_5
inst✝¹ : (i : ι) → FunLike (F i) (β i) (γ i)
inst✝ : ∀ (i : ι), AddMonoidHomClass (F i) (β i) (γ i)
h : (i : ι) → F i
x : ⨁ (i : ι), β i
⊢ ((mk γ (DFinsupp.support x)) fun i => (h ↑i) (x ↑i)) =
    ∑ x_1 ∈ DFinsupp.support x, (of (fun i => γ i) x_1) ((h x_1) (x x_1))
Tactic:
convert mk_eq_sum x.support fun i => (h i) (x i)
State after:
case h.e'_3.a.h.e'_6
ι : 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 : ι) → (x : β i) → Decidable (x ≠ 0)
F : ι → Type u_5
inst✝¹ : (i : ι) → FunLike (F i) (β i) (γ i)
inst✝ : ∀ (i : ι), AddMonoidHomClass (F i) (β i) (γ i)
h : (i : ι) → F i
x : ⨁ (i : ι), β i
x✝ : ι
a✝ : x✝ ∈ DFinsupp.support x
⊢ (h x✝) (x x✝) = if h_1 : x✝ ∈ DFinsupp.support x then (h ↑⟨x✝, h_1⟩) (x ↑⟨x✝, h_1⟩) else 0

State before:
case h.e'_3.a.h.e'_6
ι : 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 : ι) → (x : β i) → Decidable (x ≠ 0)
F : ι → Type u_5
inst✝¹ : (i : ι) → FunLike (F i) (β i) (γ i)
inst✝ : ∀ (i : ι), AddMonoidHomClass (F i) (β i) (γ i)
h : (i : ι) → F i
x : ⨁ (i : ι), β i
x✝ : ι
a✝ : x✝ ∈ DFinsupp.support x
⊢ (h x✝) (x x✝) = if h_1 : x✝ ∈ DFinsupp.support x then (h ↑⟨x✝, h_1⟩) (x ↑⟨x✝, h_1⟩) else 0
Tactic:
rwa [dif_pos]
State after:
no goals