α : Type ?u.637459
ι : Type ?u.637462
γ : Type ?u.637465
A : Type ?u.637468
B : Type ?u.637471
C : Type ?u.637474
inst✝² : AddCommMonoid A
inst✝¹ : AddCommMonoid B
inst✝ : AddCommMonoid C
t : ι → A → C
h0 : ∀ (i : ι), t i 0 = 0
h1 : ∀ (i : ι) (x y : A), t i (x + y) = t i x + t i y
s : Finset α
f✝ : α → ι →₀ A
i : ι
g : ι →₀ A
k : ι → A → γ → B
x : γ
β : Type ?u.640604
M : Type ?u.640607
M' : Type ?u.640610
N : Type ?u.640613
P : Type ?u.640616
G : Type ?u.640619
H : Type ?u.640622
R : Type ?u.640625
S : Type ?u.640628
f : ℕ →₀ ℕ
hf : ¬0 ∈ f.support
ha : 0 ∈ f.support
⊢ False
α : Type ?u.637459
ι : Type ?u.637462
γ : Type ?u.637465
A : Type ?u.637468
B : Type ?u.637471
C : Type ?u.637474
inst✝² : AddCommMonoid A
inst✝¹ : AddCommMonoid B
inst✝ : AddCommMonoid C
t : ι → A → C
h0 : ∀ (i : ι), t i 0 = 0
h1 : ∀ (i : ι) (x y : A), t i (x + y) = t i x + t i y
s : Finset α
f✝ : α → ι →₀ A
i : ι
g : ι →₀ A
k : ι → A → γ → B
x : γ
β : Type ?u.640604
M : Type ?u.640607
M' : Type ?u.640610
N : Type ?u.640613
P : Type ?u.640616
G : Type ?u.640619
H✝ : Type ?u.640622
R : Type ?u.640625
S : Type ?u.640628
f : ℕ →₀ ℕ
hf : ¬0 ∈ f.support
a : ℕ
ha : a ∈ f.support
H : a = 0
⊢ False
subst H
no goals
α : Type ?u.637459
ι : Type ?u.637462
γ : Type ?u.637465
A : Type ?u.637468
B : Type ?u.637471
C : Type ?u.637474
inst✝² : AddCommMonoid A
inst✝¹ : AddCommMonoid B
inst✝ : AddCommMonoid C
t : ι → A → C
h0 : ∀ (i : ι), t i 0 = 0
h1 : ∀ (i : ι) (x y : A), t i (x + y) = t i x + t i y
s : Finset α
f✝ : α → ι →₀ A
i : ι
g : ι →₀ A
k : ι → A → γ → B
x : γ
β : Type ?u.640604
M : Type ?u.640607
M' : Type ?u.640610
N : Type ?u.640613
P : Type ?u.640616
G : Type ?u.640619
H : Type ?u.640622
R : Type ?u.640625
S : Type ?u.640628
f : ℕ →₀ ℕ
hf : ¬0 ∈ f.support
ha : 0 ∈ f.support
⊢ False
exact hf ha