ι : Type ?u.722181
β : Type u
α : Type v
γ : Type w
s s₁ s₂ : Finset α
a : α
f✝ g✝ : α → β
inst✝¹ : CommMonoid β
inst✝ : DecidableEq γ
f : γ → β
g : α → γ
⊢ ∀ (a : α), a ∈ s → (∃ a_1, a_1 ∈ s ∧ g a_1 = g a) ∧ a ∈ s
ι : Type ?u.722181
β : Type u
α : Type v
γ : Type w
s s₁ s₂ : Finset α
a : α
f✝ g✝ : α → β
inst✝¹ : CommMonoid β
inst✝ : DecidableEq γ
f : γ → β
g : α → γ
⊢ ∀ (a : α) (ha : a ∈ s),
    (fun a _ha => { fst := g a, snd := a }) a ha ∈ Finset.sigma (image g s) fun b => filter (fun a => g a = b) s
simp
no goals
ι : Type ?u.722181
β : Type u
α : Type v
γ : Type w
s s₁ s₂ : Finset α
a : α
f✝ g✝ : α → β
inst✝¹ : CommMonoid β
inst✝ : DecidableEq γ
f : γ → β
g : α → γ
⊢ ∀ (a : α), a ∈ s → (∃ a_1, a_1 ∈ s ∧ g a_1 = g a) ∧ a ∈ s
tauto
no goals
ι : Type ?u.722181
β : Type u
α : Type v
γ : Type w
s s₁ s₂ : Finset α
a : α
f✝ g✝ : α → β
inst✝¹ : CommMonoid β
inst✝ : DecidableEq γ
f : γ → β
g : α → γ
⊢ ∀ (a₁ a₂ : α) (ha₁ : a₁ ∈ s) (ha₂ : a₂ ∈ s),
    (fun a _ha => { fst := g a, snd := a }) a₁ ha₁ = (fun a _ha => { fst := g a, snd := a }) a₂ ha₂ → a₁ = a₂
simp
case mk
ι : Type ?u.722181
β : Type u
α : Type v
γ : Type w
s s₁ s₂ : Finset α
a : α
f✝ g✝ : α → β
inst✝¹ : CommMonoid β
inst✝ : DecidableEq γ
f : γ → β
g : α → γ
b_fst : γ
b_snd : α
H : { fst := b_fst, snd := b_snd } ∈ Finset.sigma (image g s) fun b => filter (fun a => g a = b) s
⊢ ∃ a ha, { fst := b_fst, snd := b_snd } = (fun a _ha => { fst := g a, snd := a }) a ha
ι : Type ?u.722181
β : Type u
α : Type v
γ : Type w
s s₁ s₂ : Finset α
a : α
f✝ g✝ : α → β
inst✝¹ : CommMonoid β
inst✝ : DecidableEq γ
f : γ → β
g : α → γ
⊢ ∀ (b : (_ : γ) × α),
    (b ∈ Finset.sigma (image g s) fun b => filter (fun a => g a = b) s) →
      ∃ a ha, b = (fun a _ha => { fst := g a, snd := a }) a ha
rintro ⟨b_fst, b_snd⟩ H
case mk
ι : Type ?u.722181
β : Type u
α : Type v
γ : Type w
s s₁ s₂ : Finset α
a : α
f✝ g✝ : α → β
inst✝¹ : CommMonoid β
inst✝ : DecidableEq γ
f : γ → β
g : α → γ
b_fst : γ
b_snd : α
H : (∃ a, a ∈ s ∧ g a = b_fst) ∧ b_snd ∈ s ∧ g b_snd = b_fst
⊢ ∃ a ha, { fst := b_fst, snd := b_snd } = (fun a _ha => { fst := g a, snd := a }) a ha
case mk
ι : Type ?u.722181
β : Type u
α : Type v
γ : Type w
s s₁ s₂ : Finset α
a : α
f✝ g✝ : α → β
inst✝¹ : CommMonoid β
inst✝ : DecidableEq γ
f : γ → β
g : α → γ
b_fst : γ
b_snd : α
H : { fst := b_fst, snd := b_snd } ∈ Finset.sigma (image g s) fun b => filter (fun a => g a = b) s
⊢ ∃ a ha, { fst := b_fst, snd := b_snd } = (fun a _ha => { fst := g a, snd := a }) a ha
simp only [mem_image, exists_prop, mem_filter, mem_sigma, decide_eq_true_eq] at H
no goals
case mk
ι : Type ?u.722181
β : Type u
α : Type v
γ : Type w
s s₁ s₂ : Finset α
a : α
f✝ g✝ : α → β
inst✝¹ : CommMonoid β
inst✝ : DecidableEq γ
f : γ → β
g : α → γ
b_fst : γ
b_snd : α
H : (∃ a, a ∈ s ∧ g a = b_fst) ∧ b_snd ∈ s ∧ g b_snd = b_fst
⊢ ∃ a ha, { fst := b_fst, snd := b_snd } = (fun a _ha => { fst := g a, snd := a }) a ha
tauto
no goals
ι : Type ?u.722181
β : Type u
α : Type v
γ : Type w
s s₁ s₂ : Finset α
a : α
f✝ g✝ : α → β
inst✝¹ : CommMonoid β
inst✝ : DecidableEq γ
f : γ → β
g : α → γ
b : γ
_hb : b ∈ image g s
⊢ ∀ (x : α), x ∈ filter (fun a => g a = b) s → f (g x) = f b
simp (config := { contextual := true })