no goals
α : Type u_1
β : Type ?u.14308
γ : Type ?u.14311
ι : Type ?u.14314
M : Type u_2
M' : Type ?u.14320
N : Type ?u.14323
P : Type ?u.14326
G : Type ?u.14329
H : Type ?u.14332
R : Type ?u.14335
S : Type ?u.14338
inst✝ : Zero M
f g : α →₀ M
x✝ : f.support = g.support ∧ ∀ (x : α), x ∈ f.support → ↑f x = ↑g x
h₁ : f.support = g.support
h₂ : ∀ (x : α), x ∈ f.support → ↑f x = ↑g x
a : α
⊢ ↑f a = ↑g a
classical
exact if h : a ∈ f.support then h₂ a h else by
  have hf : f a = 0 := not_mem_support_iff.1 h
  have hg : g a = 0 := by rwa [h₁, not_mem_support_iff] at h
  rw [hf, hg]
no goals
α : Type u_1
β : Type ?u.14308
γ : Type ?u.14311
ι : Type ?u.14314
M : Type u_2
M' : Type ?u.14320
N : Type ?u.14323
P : Type ?u.14326
G : Type ?u.14329
H : Type ?u.14332
R : Type ?u.14335
S : Type ?u.14338
inst✝ : Zero M
f g : α →₀ M
x✝ : f.support = g.support ∧ ∀ (x : α), x ∈ f.support → ↑f x = ↑g x
h₁ : f.support = g.support
h₂ : ∀ (x : α), x ∈ f.support → ↑f x = ↑g x
a : α
⊢ ↑f a = ↑g a
exact if h : a ∈ f.support then h₂ a h else by
  have hf : f a = 0 := not_mem_support_iff.1 h
  have hg : g a = 0 := by rwa [h₁, not_mem_support_iff] at h
  rw [hf, hg]
α : Type u_1
β : Type ?u.14308
γ : Type ?u.14311
ι : Type ?u.14314
M : Type u_2
M' : Type ?u.14320
N : Type ?u.14323
P : Type ?u.14326
G : Type ?u.14329
H : Type ?u.14332
R : Type ?u.14335
S : Type ?u.14338
inst✝ : Zero M
f g : α →₀ M
x✝ : f.support = g.support ∧ ∀ (x : α), x ∈ f.support → ↑f x = ↑g x
h₁ : f.support = g.support
h₂ : ∀ (x : α), x ∈ f.support → ↑f x = ↑g x
a : α
h : ¬a ∈ f.support
hf : ↑f a = 0
⊢ ↑f a = ↑g a
α : Type u_1
β : Type ?u.14308
γ : Type ?u.14311
ι : Type ?u.14314
M : Type u_2
M' : Type ?u.14320
N : Type ?u.14323
P : Type ?u.14326
G : Type ?u.14329
H : Type ?u.14332
R : Type ?u.14335
S : Type ?u.14338
inst✝ : Zero M
f g : α →₀ M
x✝ : f.support = g.support ∧ ∀ (x : α), x ∈ f.support → ↑f x = ↑g x
h₁ : f.support = g.support
h₂ : ∀ (x : α), x ∈ f.support → ↑f x = ↑g x
a : α
h : ¬a ∈ f.support
⊢ ↑f a = ↑g a
have hf : f a = 0 := not_mem_support_iff.1 h
α : Type u_1
β : Type ?u.14308
γ : Type ?u.14311
ι : Type ?u.14314
M : Type u_2
M' : Type ?u.14320
N : Type ?u.14323
P : Type ?u.14326
G : Type ?u.14329
H : Type ?u.14332
R : Type ?u.14335
S : Type ?u.14338
inst✝ : Zero M
f g : α →₀ M
x✝ : f.support = g.support ∧ ∀ (x : α), x ∈ f.support → ↑f x = ↑g x
h₁ : f.support = g.support
h₂ : ∀ (x : α), x ∈ f.support → ↑f x = ↑g x
a : α
h : ¬a ∈ f.support
hf : ↑f a = 0
hg : ↑g a = 0
⊢ ↑f a = ↑g a
α : Type u_1
β : Type ?u.14308
γ : Type ?u.14311
ι : Type ?u.14314
M : Type u_2
M' : Type ?u.14320
N : Type ?u.14323
P : Type ?u.14326
G : Type ?u.14329
H : Type ?u.14332
R : Type ?u.14335
S : Type ?u.14338
inst✝ : Zero M
f g : α →₀ M
x✝ : f.support = g.support ∧ ∀ (x : α), x ∈ f.support → ↑f x = ↑g x
h₁ : f.support = g.support
h₂ : ∀ (x : α), x ∈ f.support → ↑f x = ↑g x
a : α
h : ¬a ∈ f.support
hf : ↑f a = 0
⊢ ↑f a = ↑g a
have hg : g a = 0 := by rwa [h₁, not_mem_support_iff] at h
no goals
α : Type u_1
β : Type ?u.14308
γ : Type ?u.14311
ι : Type ?u.14314
M : Type u_2
M' : Type ?u.14320
N : Type ?u.14323
P : Type ?u.14326
G : Type ?u.14329
H : Type ?u.14332
R : Type ?u.14335
S : Type ?u.14338
inst✝ : Zero M
f g : α →₀ M
x✝ : f.support = g.support ∧ ∀ (x : α), x ∈ f.support → ↑f x = ↑g x
h₁ : f.support = g.support
h₂ : ∀ (x : α), x ∈ f.support → ↑f x = ↑g x
a : α
h : ¬a ∈ f.support
hf : ↑f a = 0
hg : ↑g a = 0
⊢ ↑f a = ↑g a
rw [hf, hg]
no goals
α : Type u_1
β : Type ?u.14308
γ : Type ?u.14311
ι : Type ?u.14314
M : Type u_2
M' : Type ?u.14320
N : Type ?u.14323
P : Type ?u.14326
G : Type ?u.14329
H : Type ?u.14332
R : Type ?u.14335
S : Type ?u.14338
inst✝ : Zero M
f g : α →₀ M
x✝ : f.support = g.support ∧ ∀ (x : α), x ∈ f.support → ↑f x = ↑g x
h₁ : f.support = g.support
h₂ : ∀ (x : α), x ∈ f.support → ↑f x = ↑g x
a : α
h : ¬a ∈ f.support
hf : ↑f a = 0
⊢ ↑g a = 0
rwa [h₁, not_mem_support_iff] at h