internlm/Lean-Github huggingface dataset:
Theorem: DirectSum.toModule_comp_lmap'_eq
Proof 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]
Proof state after:
no goals
Theorem: DirectSum.map'_apply
Proof 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] }
Proof 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)
Theorem: DirectSum.map'_apply
Proof 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] }
Proof 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)
Theorem: DirectSum.map'_apply
Proof 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
Proof 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
Theorem: DirectSum.map'_apply
Proof 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
Proof 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
Theorem: DirectSum.map'_apply
Proof 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
Proof 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
Theorem: DirectSum.map'_apply
Proof 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]
Proof 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)
Theorem: DirectSum.map'_apply
Proof 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
Proof 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)
Theorem: DirectSum.map'_apply
Proof 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]
Proof state after:
no goals
Theorem: DirectSum.map'_apply
Proof 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]
Proof state after:
no goals
Theorem: DirectSum.map'_apply
Proof 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]
Proof state after:
no goals
Theorem: DirectSum.map'_apply
Proof 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]
Proof state after:
no goals
Theorem: DirectSum.map'_apply
Proof 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]
Proof 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)
Theorem: DirectSum.map'_apply
Proof 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]
Proof state after:
no goals
Theorem: DirectSum.map'_apply
Proof 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]
Proof state after:
no goals
Theorem: DirectSum.mk_eq_sum'
Proof state before:
ι : Type u_1
inst✝² : DecidableEq ι
R : Type u_2
inst✝¹ : Semiring R
β : ι → Type u_3
inst✝ : (i : ι) → AddCommMonoid (β i)
s : Finset ι
f : (i : ι) → β i
⊢ ((mk β s) fun i => f ↑i) = ∑ i ∈ s, (of β i) (f i)
Tactic:
apply DFinsupp.ext
Proof state after:
case h
ι : Type u_1
inst✝² : DecidableEq ι
R : Type u_2
inst✝¹ : Semiring R
β : ι → Type u_3
inst✝ : (i : ι) → AddCommMonoid (β i)
s : Finset ι
f : (i : ι) → β i
⊢ ∀ (i : ι), ((mk β s) fun i => f ↑i) i = (∑ i ∈ s, (of β i) (f i)) i
Theorem: DirectSum.mk_eq_sum'
Proof state before:
case h
ι : Type u_1
inst✝² : DecidableEq ι
R : Type u_2
inst✝¹ : Semiring R
β : ι → Type u_3
inst✝ : (i : ι) → AddCommMonoid (β i)
s : Finset ι
f : (i : ι) → β i
⊢ ∀ (i : ι), ((mk β s) fun i => f ↑i) i = (∑ i ∈ s, (of β i) (f i)) i
Tactic:
intro i
Proof state after:
case h
ι : Type u_1
inst✝² : DecidableEq ι
R : Type u_2
inst✝¹ : Semiring R
β : ι → Type u_3
inst✝ : (i : ι) → AddCommMonoid (β i)
s : Finset ι
f : (i : ι) → β i
i : ι
⊢ ((mk β s) fun i => f ↑i) i = (∑ i ∈ s, (of β i) (f i)) i
Theorem: DirectSum.mk_eq_sum'
Proof state before:
case h
ι : Type u_1
inst✝² : DecidableEq ι
R : Type u_2
inst✝¹ : Semiring R
β : ι → Type u_3
inst✝ : (i : ι) → AddCommMonoid (β i)
s : Finset ι
f : (i : ι) → β i
i : ι
⊢ ((mk β s) fun i => f ↑i) i = (∑ i ∈ s, (of β i) (f i)) i
Tactic:
convert mk_apply s _ i
Proof state after:
case h.e'_3
ι : Type u_1
inst✝² : DecidableEq ι
R : Type u_2
inst✝¹ : Semiring R
β : ι → Type u_3
inst✝ : (i : ι) → AddCommMonoid (β i)
s : Finset ι
f : (i : ι) → β i
i : ι
⊢ (∑ i ∈ s, (of β i) (f i)) i = if h : i ∈ s then f ↑⟨i, h⟩ else 0
Theorem: DirectSum.mk_eq_sum'
Proof state before:
case h.e'_3
ι : Type u_1
inst✝² : DecidableEq ι
R : Type u_2
inst✝¹ : Semiring R
β : ι → Type u_3
inst✝ : (i : ι) → AddCommMonoid (β i)
s : Finset ι
f : (i : ι) → β i
i : ι
⊢ (∑ i ∈ s, (of β i) (f i)) i = if h : i ∈ s then f ↑⟨i, h⟩ else 0
Tactic:
rw [DFinsupp.finset_sum_apply]
Proof state after:
case h.e'_3
ι : Type u_1
inst✝² : DecidableEq ι
R : Type u_2
inst✝¹ : Semiring R
β : ι → Type u_3
inst✝ : (i : ι) → AddCommMonoid (β i)
s : Finset ι
f : (i : ι) → β i
i : ι
⊢ ∑ a ∈ s, ((of β a) (f a)) i = if h : i ∈ s then f ↑⟨i, h⟩ else 0
Theorem: DirectSum.mk_eq_sum'
Proof state before:
case h.e'_3
ι : Type u_1
inst✝² : DecidableEq ι
R : Type u_2
inst✝¹ : Semiring R
β : ι → Type u_3
inst✝ : (i : ι) → AddCommMonoid (β i)
s : Finset ι
f : (i : ι) → β i
i : ι
⊢ ∑ a ∈ s, ((of β a) (f a)) i = if h : i ∈ s then f ↑⟨i, h⟩ else 0
Tactic:
split_ifs with hi
Proof state after:
case pos
ι : Type u_1
inst✝² : DecidableEq ι
R : Type u_2
inst✝¹ : Semiring R
β : ι → Type u_3
inst✝ : (i : ι) → AddCommMonoid (β i)
s : Finset ι
f : (i : ι) → β i
i : ι
hi : i ∈ s
⊢ ∑ a ∈ s, ((of β a) (f a)) i = f ↑⟨i, hi⟩

case neg
ι : Type u_1
inst✝² : DecidableEq ι
R : Type u_2
inst✝¹ : Semiring R
β : ι → Type u_3
inst✝ : (i : ι) → AddCommMonoid (β i)
s : Finset ι
f : (i : ι) → β i
i : ι
hi : i ∉ s
⊢ ∑ a ∈ s, ((of β a) (f a)) i = 0
Theorem: DirectSum.mk_eq_sum'
Proof state before:
case pos
ι : Type u_1
inst✝² : DecidableEq ι
R : Type u_2
inst✝¹ : Semiring R
β : ι → Type u_3
inst✝ : (i : ι) → AddCommMonoid (β i)
s : Finset ι
f : (i : ι) → β i
i : ι
hi : i ∈ s
⊢ ∑ a ∈ s, ((of β a) (f a)) i = f ↑⟨i, hi⟩
Tactic:
rw [Finset.sum_eq_single_of_mem i hi (fun j _ hij => of_eq_of_ne _ _ _ _ hij),
  ← lof_eq_of ℕ, lof_apply]
Proof state after:
no goals
Theorem: DirectSum.mk_eq_sum'
Proof state before:
case neg
ι : Type u_1
inst✝² : DecidableEq ι
R : Type u_2
inst✝¹ : Semiring R
β : ι → Type u_3
inst✝ : (i : ι) → AddCommMonoid (β i)
s : Finset ι
f : (i : ι) → β i
i : ι
hi : i ∉ s
⊢ ∑ a ∈ s, ((of β a) (f a)) i = 0
Tactic:
exact Finset.sum_eq_zero (fun j hj => of_eq_of_ne _ _ _ _ (ne_of_mem_of_not_mem hj hi))
Proof state after:
no goals
Theorem: DFinsupp.mk_eq_sum
Proof state before:
ι : Type u_1
inst✝² : DecidableEq ι
R : Type u_2
inst✝¹ : Semiring R
β : ι → Type u_3
inst✝ : (i : ι) → AddCommMonoid (β i)
s : Finset ι
f : (i : ι) → β i
⊢ (DFinsupp.mk s fun i => f ↑i) = ∑ i ∈ s, (of β i) (f i)
Tactic:
ext i
Proof state after:
case h
ι : Type u_1
inst✝² : DecidableEq ι
R : Type u_2
inst✝¹ : Semiring R
β : ι → Type u_3
inst✝ : (i : ι) → AddCommMonoid (β i)
s : Finset ι
f : (i : ι) → β i
i : ι
⊢ (DFinsupp.mk s fun i => f ↑i) i = (∑ i ∈ s, (of β i) (f i)) i
Theorem: DFinsupp.mk_eq_sum
Proof state before:
case h
ι : Type u_1
inst✝² : DecidableEq ι
R : Type u_2
inst✝¹ : Semiring R
β : ι → Type u_3
inst✝ : (i : ι) → AddCommMonoid (β i)
s : Finset ι
f : (i : ι) → β i
i : ι
⊢ (DFinsupp.mk s fun i => f ↑i) i = (∑ i ∈ s, (of β i) (f i)) i
Tactic:
simp only [DFinsupp.mk_apply, DFinsupp.finset_sum_apply]
Proof state after:
case h
ι : Type u_1
inst✝² : DecidableEq ι
R : Type u_2
inst✝¹ : Semiring R
β : ι → Type u_3
inst✝ : (i : ι) → AddCommMonoid (β i)
s : Finset ι
f : (i : ι) → β i
i : ι
⊢ (if h : i ∈ s then f i else 0) = (∑ i ∈ s, (of β i) (f i)) i
Theorem: DFinsupp.mk_eq_sum
Proof state before:
case h
ι : Type u_1
inst✝² : DecidableEq ι
R : Type u_2
inst✝¹ : Semiring R
β : ι → Type u_3
inst✝ : (i : ι) → AddCommMonoid (β i)
s : Finset ι
f : (i : ι) → β i
i : ι
⊢ (if h : i ∈ s then f i else 0) = (∑ i ∈ s, (of β i) (f i)) i
Tactic:
split_ifs with hi
Proof state after:
case pos
ι : Type u_1
inst✝² : DecidableEq ι
R : Type u_2
inst✝¹ : Semiring R
β : ι → Type u_3
inst✝ : (i : ι) → AddCommMonoid (β i)
s : Finset ι
f : (i : ι) → β i
i : ι
hi : i ∈ s
⊢ f i = (∑ i ∈ s, (of β i) (f i)) i

case neg
ι : Type u_1
inst✝² : DecidableEq ι
R : Type u_2
inst✝¹ : Semiring R
β : ι → Type u_3
inst✝ : (i : ι) → AddCommMonoid (β i)
s : Finset ι
f : (i : ι) → β i
i : ι
hi : i ∉ s
⊢ 0 = (∑ i ∈ s, (of β i) (f i)) i
Theorem: DFinsupp.mk_eq_sum
Proof state before:
case pos
ι : Type u_1
inst✝² : DecidableEq ι
R : Type u_2
inst✝¹ : Semiring R
β : ι → Type u_3
inst✝ : (i : ι) → AddCommMonoid (β i)
s : Finset ι
f : (i : ι) → β i
i : ι
hi : i ∈ s
⊢ f i = (∑ i ∈ s, (of β i) (f i)) i
Tactic:
rw [DFinsupp.finset_sum_apply, Finset.sum_eq_single_of_mem i hi
  (fun j _ hij =>  of_eq_of_ne _ _ _ _ hij), of_eq_same]
Proof state after:
no goals
Theorem: DFinsupp.mk_eq_sum
Proof state before:
case neg
ι : Type u_1
inst✝² : DecidableEq ι
R : Type u_2
inst✝¹ : Semiring R
β : ι → Type u_3
inst✝ : (i : ι) → AddCommMonoid (β i)
s : Finset ι
f : (i : ι) → β i
i : ι
hi : i ∉ s
⊢ 0 = (∑ i ∈ s, (of β i) (f i)) i
Tactic:
rw [DFinsupp.finset_sum_apply, Finset.sum_eq_zero
  (fun j hj => of_eq_of_ne _ _ _ _ (ne_of_mem_of_not_mem hj hi))]
Proof state after:
no goals
Theorem: DirectSum.mk_eq_sum
Proof state before:
ι : Type u_1
inst✝² : DecidableEq ι
R : Type u_2
inst✝¹ : Semiring R
β : ι → Type u_3
inst✝ : (i : ι) → AddCommMonoid (β i)
s : Finset ι
x : (i : { x // x ∈ s }) → β ↑i
⊢ (mk β s) x = ∑ i ∈ s, (of β i) (if h : i ∈ s then x ⟨i, h⟩ else 0)
Tactic:
apply DFinsupp.ext
Proof state after:
case h
ι : Type u_1
inst✝² : DecidableEq ι
R : Type u_2
inst✝¹ : Semiring R
β : ι → Type u_3
inst✝ : (i : ι) → AddCommMonoid (β i)
s : Finset ι
x : (i : { x // x ∈ s }) → β ↑i
⊢ ∀ (i : ι), ((mk β s) x) i = (∑ i ∈ s, (of β i) (if h : i ∈ s then x ⟨i, h⟩ else 0)) i
Theorem: DirectSum.mk_eq_sum
Proof state before:
case h
ι : Type u_1
inst✝² : DecidableEq ι
R : Type u_2
inst✝¹ : Semiring R
β : ι → Type u_3
inst✝ : (i : ι) → AddCommMonoid (β i)
s : Finset ι
x : (i : { x // x ∈ s }) → β ↑i
⊢ ∀ (i : ι), ((mk β s) x) i = (∑ i ∈ s, (of β i) (if h : i ∈ s then x ⟨i, h⟩ else 0)) i
Tactic:
intro i
Proof state after:
case h
ι : Type u_1
inst✝² : DecidableEq ι
R : Type u_2
inst✝¹ : Semiring R
β : ι → Type u_3
inst✝ : (i : ι) → AddCommMonoid (β i)
s : Finset ι
x : (i : { x // x ∈ s }) → β ↑i
i : ι
⊢ ((mk β s) x) i = (∑ i ∈ s, (of β i) (if h : i ∈ s then x ⟨i, h⟩ else 0)) i
Theorem: DirectSum.mk_eq_sum
Proof state before:
case h
ι : Type u_1
inst✝² : DecidableEq ι
R : Type u_2
inst✝¹ : Semiring R
β : ι → Type u_3
inst✝ : (i : ι) → AddCommMonoid (β i)
s : Finset ι
x : (i : { x // x ∈ s }) → β ↑i
i : ι
⊢ ((mk β s) x) i = (∑ i ∈ s, (of β i) (if h : i ∈ s then x ⟨i, h⟩ else 0)) i
Tactic:
rw [mk_apply]
Proof state after:
case h
ι : Type u_1
inst✝² : DecidableEq ι
R : Type u_2
inst✝¹ : Semiring R
β : ι → Type u_3
inst✝ : (i : ι) → AddCommMonoid (β i)
s : Finset ι
x : (i : { x // x ∈ s }) → β ↑i
i : ι
⊢ (if h : i ∈ s then x ⟨i, h⟩ else 0) = (∑ i ∈ s, (of β i) (if h : i ∈ s then x ⟨i, h⟩ else 0)) i
Theorem: DirectSum.mk_eq_sum
Proof state before:
case h
ι : Type u_1
inst✝² : DecidableEq ι
R : Type u_2
inst✝¹ : Semiring R
β : ι → Type u_3
inst✝ : (i : ι) → AddCommMonoid (β i)
s : Finset ι
x : (i : { x // x ∈ s }) → β ↑i
i : ι
⊢ (if h : i ∈ s then x ⟨i, h⟩ else 0) = (∑ i ∈ s, (of β i) (if h : i ∈ s then x ⟨i, h⟩ else 0)) i
Tactic:
split_ifs with hi
Proof state after:
case pos
ι : Type u_1
inst✝² : DecidableEq ι
R : Type u_2
inst✝¹ : Semiring R
β : ι → Type u_3
inst✝ : (i : ι) → AddCommMonoid (β i)
s : Finset ι
x : (i : { x // x ∈ s }) → β ↑i
i : ι
hi : i ∈ s
⊢ x ⟨i, hi⟩ = (∑ i ∈ s, (of β i) (if h : i ∈ s then x ⟨i, h⟩ else 0)) i

case neg
ι : Type u_1
inst✝² : DecidableEq ι
R : Type u_2
inst✝¹ : Semiring R
β : ι → Type u_3
inst✝ : (i : ι) → AddCommMonoid (β i)
s : Finset ι
x : (i : { x // x ∈ s }) → β ↑i
i : ι
hi : i ∉ s
⊢ 0 = (∑ i ∈ s, (of β i) (if h : i ∈ s then x ⟨i, h⟩ else 0)) i
Theorem: DirectSum.mk_eq_sum
Proof state before:
case pos
ι : Type u_1
inst✝² : DecidableEq ι
R : Type u_2
inst✝¹ : Semiring R
β : ι → Type u_3
inst✝ : (i : ι) → AddCommMonoid (β i)
s : Finset ι
x : (i : { x // x ∈ s }) → β ↑i
i : ι
hi : i ∈ s
⊢ x ⟨i, hi⟩ = (∑ i ∈ s, (of β i) (if h : i ∈ s then x ⟨i, h⟩ else 0)) i
Tactic:
rw [DFinsupp.finset_sum_apply, Finset.sum_eq_single i (fun j _ hji => of_eq_of_ne _ _ _ _ hji),
  of_eq_same, dif_pos hi]
Proof state after:
case pos
ι : Type u_1
inst✝² : DecidableEq ι
R : Type u_2
inst✝¹ : Semiring R
β : ι → Type u_3
inst✝ : (i : ι) → AddCommMonoid (β i)
s : Finset ι
x : (i : { x // x ∈ s }) → β ↑i
i : ι
hi : i ∈ s
⊢ i ∉ s → ((of β i) (if h : i ∈ s then x ⟨i, h⟩ else 0)) i = 0
Theorem: DirectSum.mk_eq_sum
Proof state before:
case pos
ι : Type u_1
inst✝² : DecidableEq ι
R : Type u_2
inst✝¹ : Semiring R
β : ι → Type u_3
inst✝ : (i : ι) → AddCommMonoid (β i)
s : Finset ι
x : (i : { x // x ∈ s }) → β ↑i
i : ι
hi : i ∈ s
⊢ i ∉ s → ((of β i) (if h : i ∈ s then x ⟨i, h⟩ else 0)) i = 0
Tactic:
intro his
Proof state after:
case pos
ι : Type u_1
inst✝² : DecidableEq ι
R : Type u_2
inst✝¹ : Semiring R
β : ι → Type u_3
inst✝ : (i : ι) → AddCommMonoid (β i)
s : Finset ι
x : (i : { x // x ∈ s }) → β ↑i
i : ι
hi : i ∈ s
his : i ∉ s
⊢ ((of β i) (if h : i ∈ s then x ⟨i, h⟩ else 0)) i = 0
Theorem: DirectSum.mk_eq_sum
Proof state before:
case pos
ι : Type u_1
inst✝² : DecidableEq ι
R : Type u_2
inst✝¹ : Semiring R
β : ι → Type u_3
inst✝ : (i : ι) → AddCommMonoid (β i)
s : Finset ι
x : (i : { x // x ∈ s }) → β ↑i
i : ι
hi : i ∈ s
his : i ∉ s
⊢ ((of β i) (if h : i ∈ s then x ⟨i, h⟩ else 0)) i = 0
Tactic:
rw [of_eq_same, dif_neg his]
Proof state after:
no goals