no goals
α : Type u_1
β : Type ?u.320386
γ : Type ?u.320389
ι : Type ?u.320392
M : Type u_2
M' : Type ?u.320398
N : Type ?u.320401
P : Type ?u.320404
G : Type ?u.320407
H : Type ?u.320410
R : Type ?u.320413
S : Type ?u.320416
inst✝ : AddZeroClass M
p : (α →₀ M) → Prop
f✝ : α →₀ M
h0 : p 0
ha : ∀ (a : α) (b : M) (f : α →₀ M), ¬a ∈ f.support → b ≠ 0 → p f → p (f + single a b)
s : Finset α
f : α →₀ M
hf : f.support = ∅
⊢ p f
rwa [support_eq_empty.1 hf]
α : Type u_1
β : Type ?u.320386
γ : Type ?u.320389
ι : Type ?u.320392
M : Type u_2
M' : Type ?u.320398
N : Type ?u.320401
P : Type ?u.320404
G : Type ?u.320407
H : Type ?u.320410
R : Type ?u.320413
S : Type ?u.320416
inst✝ : AddZeroClass M
p : (α →₀ M) → Prop
f✝ : α →₀ M
h0 : p 0
ha : ∀ (a : α) (b : M) (f : α →₀ M), ¬a ∈ f.support → b ≠ 0 → p f → p (f + single a b)
s✝ : Finset α
a : α
s : Finset α
has : ¬a ∈ s
ih : ∀ (f : α →₀ M), f.support = s → p f
f : α →₀ M
hf : f.support = cons a s has
⊢ p (erase a f + single a (↑f a))
α : Type u_1
β : Type ?u.320386
γ : Type ?u.320389
ι : Type ?u.320392
M : Type u_2
M' : Type ?u.320398
N : Type ?u.320401
P : Type ?u.320404
G : Type ?u.320407
H : Type ?u.320410
R : Type ?u.320413
S : Type ?u.320416
inst✝ : AddZeroClass M
p : (α →₀ M) → Prop
f✝ : α →₀ M
h0 : p 0
ha : ∀ (a : α) (b : M) (f : α →₀ M), ¬a ∈ f.support → b ≠ 0 → p f → p (f + single a b)
s✝ : Finset α
a : α
s : Finset α
has : ¬a ∈ s
ih : ∀ (f : α →₀ M), f.support = s → p f
f : α →₀ M
hf : f.support = cons a s has
⊢ p f
suffices p (f.erase a + single a (f a)) by rwa [erase_add_single] at this
no goals
α : Type u_1
β : Type ?u.320386
γ : Type ?u.320389
ι : Type ?u.320392
M : Type u_2
M' : Type ?u.320398
N : Type ?u.320401
P : Type ?u.320404
G : Type ?u.320407
H : Type ?u.320410
R : Type ?u.320413
S : Type ?u.320416
inst✝ : AddZeroClass M
p : (α →₀ M) → Prop
f✝ : α →₀ M
h0 : p 0
ha : ∀ (a : α) (b : M) (f : α →₀ M), ¬a ∈ f.support → b ≠ 0 → p f → p (f + single a b)
s✝ : Finset α
a : α
s : Finset α
has : ¬a ∈ s
ih : ∀ (f : α →₀ M), f.support = s → p f
f : α →₀ M
hf : f.support = cons a s has
this : p (erase a f + single a (↑f a))
⊢ p f
rwa [erase_add_single] at this
case a
α : Type u_1
β : Type ?u.320386
γ : Type ?u.320389
ι : Type ?u.320392
M : Type u_2
M' : Type ?u.320398
N : Type ?u.320401
P : Type ?u.320404
G : Type ?u.320407
H : Type ?u.320410
R : Type ?u.320413
S : Type ?u.320416
inst✝ : AddZeroClass M
p : (α →₀ M) → Prop
f✝ : α →₀ M
h0 : p 0
ha : ∀ (a : α) (b : M) (f : α →₀ M), ¬a ∈ f.support → b ≠ 0 → p f → p (f + single a b)
s✝ : Finset α
a : α
s : Finset α
has : ¬a ∈ s
ih : ∀ (f : α →₀ M), f.support = s → p f
f : α →₀ M
hf : f.support = cons a s has
⊢ ¬a ∈ (erase a f).support

case a
α : Type u_1
β : Type ?u.320386
γ : Type ?u.320389
ι : Type ?u.320392
M : Type u_2
M' : Type ?u.320398
N : Type ?u.320401
P : Type ?u.320404
G : Type ?u.320407
H : Type ?u.320410
R : Type ?u.320413
S : Type ?u.320416
inst✝ : AddZeroClass M
p : (α →₀ M) → Prop
f✝ : α →₀ M
h0 : p 0
ha : ∀ (a : α) (b : M) (f : α →₀ M), ¬a ∈ f.support → b ≠ 0 → p f → p (f + single a b)
s✝ : Finset α
a : α
s : Finset α
has : ¬a ∈ s
ih : ∀ (f : α →₀ M), f.support = s → p f
f : α →₀ M
hf : f.support = cons a s has
⊢ ↑f a ≠ 0

case a
α : Type u_1
β : Type ?u.320386
γ : Type ?u.320389
ι : Type ?u.320392
M : Type u_2
M' : Type ?u.320398
N : Type ?u.320401
P : Type ?u.320404
G : Type ?u.320407
H : Type ?u.320410
R : Type ?u.320413
S : Type ?u.320416
inst✝ : AddZeroClass M
p : (α →₀ M) → Prop
f✝ : α →₀ M
h0 : p 0
ha : ∀ (a : α) (b : M) (f : α →₀ M), ¬a ∈ f.support → b ≠ 0 → p f → p (f + single a b)
s✝ : Finset α
a : α
s : Finset α
has : ¬a ∈ s
ih : ∀ (f : α →₀ M), f.support = s → p f
f : α →₀ M
hf : f.support = cons a s has
⊢ p (erase a f)
α : Type u_1
β : Type ?u.320386
γ : Type ?u.320389
ι : Type ?u.320392
M : Type u_2
M' : Type ?u.320398
N : Type ?u.320401
P : Type ?u.320404
G : Type ?u.320407
H : Type ?u.320410
R : Type ?u.320413
S : Type ?u.320416
inst✝ : AddZeroClass M
p : (α →₀ M) → Prop
f✝ : α →₀ M
h0 : p 0
ha : ∀ (a : α) (b : M) (f : α →₀ M), ¬a ∈ f.support → b ≠ 0 → p f → p (f + single a b)
s✝ : Finset α
a : α
s : Finset α
has : ¬a ∈ s
ih : ∀ (f : α →₀ M), f.support = s → p f
f : α →₀ M
hf : f.support = cons a s has
⊢ p (erase a f + single a (↑f a))
apply ha
case a
α : Type u_1
β : Type ?u.320386
γ : Type ?u.320389
ι : Type ?u.320392
M : Type u_2
M' : Type ?u.320398
N : Type ?u.320401
P : Type ?u.320404
G : Type ?u.320407
H : Type ?u.320410
R : Type ?u.320413
S : Type ?u.320416
inst✝ : AddZeroClass M
p : (α →₀ M) → Prop
f✝ : α →₀ M
h0 : p 0
ha : ∀ (a : α) (b : M) (f : α →₀ M), ¬a ∈ f.support → b ≠ 0 → p f → p (f + single a b)
s✝ : Finset α
a : α
s : Finset α
has : ¬a ∈ s
ih : ∀ (f : α →₀ M), f.support = s → p f
f : α →₀ M
hf : f.support = cons a s has
⊢ ¬(a ≠ a ∧ a ∈ f.support)
case a
α : Type u_1
β : Type ?u.320386
γ : Type ?u.320389
ι : Type ?u.320392
M : Type u_2
M' : Type ?u.320398
N : Type ?u.320401
P : Type ?u.320404
G : Type ?u.320407
H : Type ?u.320410
R : Type ?u.320413
S : Type ?u.320416
inst✝ : AddZeroClass M
p : (α →₀ M) → Prop
f✝ : α →₀ M
h0 : p 0
ha : ∀ (a : α) (b : M) (f : α →₀ M), ¬a ∈ f.support → b ≠ 0 → p f → p (f + single a b)
s✝ : Finset α
a : α
s : Finset α
has : ¬a ∈ s
ih : ∀ (f : α →₀ M), f.support = s → p f
f : α →₀ M
hf : f.support = cons a s has
⊢ ¬a ∈ (erase a f).support
rw [support_erase, mem_erase]
no goals
case a
α : Type u_1
β : Type ?u.320386
γ : Type ?u.320389
ι : Type ?u.320392
M : Type u_2
M' : Type ?u.320398
N : Type ?u.320401
P : Type ?u.320404
G : Type ?u.320407
H : Type ?u.320410
R : Type ?u.320413
S : Type ?u.320416
inst✝ : AddZeroClass M
p : (α →₀ M) → Prop
f✝ : α →₀ M
h0 : p 0
ha : ∀ (a : α) (b : M) (f : α →₀ M), ¬a ∈ f.support → b ≠ 0 → p f → p (f + single a b)
s✝ : Finset α
a : α
s : Finset α
has : ¬a ∈ s
ih : ∀ (f : α →₀ M), f.support = s → p f
f : α →₀ M
hf : f.support = cons a s has
⊢ ¬(a ≠ a ∧ a ∈ f.support)
exact fun H => H.1 rfl
case a
α : Type u_1
β : Type ?u.320386
γ : Type ?u.320389
ι : Type ?u.320392
M : Type u_2
M' : Type ?u.320398
N : Type ?u.320401
P : Type ?u.320404
G : Type ?u.320407
H : Type ?u.320410
R : Type ?u.320413
S : Type ?u.320416
inst✝ : AddZeroClass M
p : (α →₀ M) → Prop
f✝ : α →₀ M
h0 : p 0
ha : ∀ (a : α) (b : M) (f : α →₀ M), ¬a ∈ f.support → b ≠ 0 → p f → p (f + single a b)
s✝ : Finset α
a : α
s : Finset α
has : ¬a ∈ s
ih : ∀ (f : α →₀ M), f.support = s → p f
f : α →₀ M
hf : f.support = cons a s has
⊢ a ∈ cons a s has
case a
α : Type u_1
β : Type ?u.320386
γ : Type ?u.320389
ι : Type ?u.320392
M : Type u_2
M' : Type ?u.320398
N : Type ?u.320401
P : Type ?u.320404
G : Type ?u.320407
H : Type ?u.320410
R : Type ?u.320413
S : Type ?u.320416
inst✝ : AddZeroClass M
p : (α →₀ M) → Prop
f✝ : α →₀ M
h0 : p 0
ha : ∀ (a : α) (b : M) (f : α →₀ M), ¬a ∈ f.support → b ≠ 0 → p f → p (f + single a b)
s✝ : Finset α
a : α
s : Finset α
has : ¬a ∈ s
ih : ∀ (f : α →₀ M), f.support = s → p f
f : α →₀ M
hf : f.support = cons a s has
⊢ ↑f a ≠ 0
rw [← mem_support_iff, hf]
no goals
case a
α : Type u_1
β : Type ?u.320386
γ : Type ?u.320389
ι : Type ?u.320392
M : Type u_2
M' : Type ?u.320398
N : Type ?u.320401
P : Type ?u.320404
G : Type ?u.320407
H : Type ?u.320410
R : Type ?u.320413
S : Type ?u.320416
inst✝ : AddZeroClass M
p : (α →₀ M) → Prop
f✝ : α →₀ M
h0 : p 0
ha : ∀ (a : α) (b : M) (f : α →₀ M), ¬a ∈ f.support → b ≠ 0 → p f → p (f + single a b)
s✝ : Finset α
a : α
s : Finset α
has : ¬a ∈ s
ih : ∀ (f : α →₀ M), f.support = s → p f
f : α →₀ M
hf : f.support = cons a s has
⊢ a ∈ cons a s has
exact mem_cons_self _ _
α : Type u_1
β : Type ?u.320386
γ : Type ?u.320389
ι : Type ?u.320392
M : Type u_2
M' : Type ?u.320398
N : Type ?u.320401
P : Type ?u.320404
G : Type ?u.320407
H : Type ?u.320410
R : Type ?u.320413
S : Type ?u.320416
inst✝ : AddZeroClass M
p : (α →₀ M) → Prop
f✝ : α →₀ M
h0 : p 0
ha : ∀ (a : α) (b : M) (f : α →₀ M), ¬a ∈ f.support → b ≠ 0 → p f → p (f + single a b)
s✝ : Finset α
a : α
s : Finset α
has : ¬a ∈ s
ih : ∀ (f : α →₀ M), f.support = s → p f
f : α →₀ M
hf : f.support = cons a s has
⊢ (erase a f).support = s
case a
α : Type u_1
β : Type ?u.320386
γ : Type ?u.320389
ι : Type ?u.320392
M : Type u_2
M' : Type ?u.320398
N : Type ?u.320401
P : Type ?u.320404
G : Type ?u.320407
H : Type ?u.320410
R : Type ?u.320413
S : Type ?u.320416
inst✝ : AddZeroClass M
p : (α →₀ M) → Prop
f✝ : α →₀ M
h0 : p 0
ha : ∀ (a : α) (b : M) (f : α →₀ M), ¬a ∈ f.support → b ≠ 0 → p f → p (f + single a b)
s✝ : Finset α
a : α
s : Finset α
has : ¬a ∈ s
ih : ∀ (f : α →₀ M), f.support = s → p f
f : α →₀ M
hf : f.support = cons a s has
⊢ p (erase a f)
apply ih _ _
no goals
α : Type u_1
β : Type ?u.320386
γ : Type ?u.320389
ι : Type ?u.320392
M : Type u_2
M' : Type ?u.320398
N : Type ?u.320401
P : Type ?u.320404
G : Type ?u.320407
H : Type ?u.320410
R : Type ?u.320413
S : Type ?u.320416
inst✝ : AddZeroClass M
p : (α →₀ M) → Prop
f✝ : α →₀ M
h0 : p 0
ha : ∀ (a : α) (b : M) (f : α →₀ M), ¬a ∈ f.support → b ≠ 0 → p f → p (f + single a b)
s✝ : Finset α
a : α
s : Finset α
has : ¬a ∈ s
ih : ∀ (f : α →₀ M), f.support = s → p f
f : α →₀ M
hf : f.support = cons a s has
⊢ (erase a f).support = s
rw [support_erase, hf, Finset.erase_cons]