case a
ι : Type ?u.612021
β : Type u
α : Type v
γ : Type w
s s₁ s₂ : Finset α
a : α
f✝ g✝ : α → β
inst✝¹ : CommMonoid β
inst✝ : DecidableEq α
m : Multiset α
f : { x // x ∈ m } → β
g : α → β
hfg : ∀ (x : { x // x ∈ m }), f x = g ↑x
x✝³ x✝² : { x // x ∈ m }
x✝¹ : x✝³ ∈ univ
x✝ : x✝² ∈ univ
h : (fun x x_1 => ↑x) x✝³ x✝¹ = (fun x x_1 => ↑x) x✝² x✝
⊢ ↑x✝³ = ↑x✝²
ι : Type ?u.612021
β : Type u
α : Type v
γ : Type w
s s₁ s₂ : Finset α
a : α
f✝ g✝ : α → β
inst✝¹ : CommMonoid β
inst✝ : DecidableEq α
m : Multiset α
f : { x // x ∈ m } → β
g : α → β
hfg : ∀ (x : { x // x ∈ m }), f x = g ↑x
x✝³ x✝² : { x // x ∈ m }
x✝¹ : x✝³ ∈ univ
x✝ : x✝² ∈ univ
h : (fun x x_1 => ↑x) x✝³ x✝¹ = (fun x x_1 => ↑x) x✝² x✝
⊢ x✝³ = x✝²
ext
no goals
case a
ι : Type ?u.612021
β : Type u
α : Type v
γ : Type w
s s₁ s₂ : Finset α
a : α
f✝ g✝ : α → β
inst✝¹ : CommMonoid β
inst✝ : DecidableEq α
m : Multiset α
f : { x // x ∈ m } → β
g : α → β
hfg : ∀ (x : { x // x ∈ m }), f x = g ↑x
x✝³ x✝² : { x // x ∈ m }
x✝¹ : x✝³ ∈ univ
x✝ : x✝² ∈ univ
h : (fun x x_1 => ↑x) x✝³ x✝¹ = (fun x x_1 => ↑x) x✝² x✝
⊢ ↑x✝³ = ↑x✝²
assumption