ι : Type u_2
α : ι → Type u_3
β : ι → Type u_4
γ : ι → Type u_1
inst✝ : DecidableEq ι
f : ⦃i : ι⦄ → α i → β i → Finset (γ i)
i : ι
a : α i
b : β i
x : γ i
⊢ (∃ a_1,
      a_1 ∈
          f ((_ : { fst := i, snd := a }.fst = { fst := i, snd := a }.fst) ▸ { fst := i, snd := a }.snd)
            { fst := i, snd := b }.snd ∧
        ↑(Embedding.sigmaMk { fst := i, snd := b }.fst) a_1 = { fst := i, snd := x }) ↔
    x ∈ f a b
ι : Type u_2
α : ι → Type u_3
β : ι → Type u_4
γ : ι → Type u_1
inst✝ : DecidableEq ι
f : ⦃i : ι⦄ → α i → β i → Finset (γ i)
i : ι
a : α i
b : β i
x : γ i
⊢ { fst := i, snd := x } ∈ sigmaLift f { fst := i, snd := a } { fst := i, snd := b } ↔ x ∈ f a b
rw [sigmaLift, dif_pos rfl, mem_map]
ι : Type u_2
α : ι → Type u_3
β : ι → Type u_4
γ : ι → Type u_1
inst✝ : DecidableEq ι
f : ⦃i : ι⦄ → α i → β i → Finset (γ i)
i : ι
a : α i
b : β i
x : γ i
⊢ (∃ a_1,
      a_1 ∈
          f ((_ : { fst := i, snd := a }.fst = { fst := i, snd := a }.fst) ▸ { fst := i, snd := a }.snd)
            { fst := i, snd := b }.snd ∧
        ↑(Embedding.sigmaMk { fst := i, snd := b }.fst) a_1 = { fst := i, snd := x }) →
    x ∈ f a b
ι : Type u_2
α : ι → Type u_3
β : ι → Type u_4
γ : ι → Type u_1
inst✝ : DecidableEq ι
f : ⦃i : ι⦄ → α i → β i → Finset (γ i)
i : ι
a : α i
b : β i
x : γ i
⊢ (∃ a_1,
      a_1 ∈
          f ((_ : { fst := i, snd := a }.fst = { fst := i, snd := a }.fst) ▸ { fst := i, snd := a }.snd)
            { fst := i, snd := b }.snd ∧
        ↑(Embedding.sigmaMk { fst := i, snd := b }.fst) a_1 = { fst := i, snd := x }) ↔
    x ∈ f a b
refine' ⟨_, fun hx => ⟨_, hx, rfl⟩⟩
case intro.intro.refl
ι : Type u_2
α : ι → Type u_3
β : ι → Type u_4
γ : ι → Type u_1
inst✝ : DecidableEq ι
f : ⦃i : ι⦄ → α i → β i → Finset (γ i)
i : ι
a : α i
b : β i
x : γ i
hx :
  x ∈
    f ((_ : { fst := i, snd := a }.fst = { fst := i, snd := a }.fst) ▸ { fst := i, snd := a }.snd)
      { fst := i, snd := b }.snd
⊢ x ∈ f a b
ι : Type u_2
α : ι → Type u_3
β : ι → Type u_4
γ : ι → Type u_1
inst✝ : DecidableEq ι
f : ⦃i : ι⦄ → α i → β i → Finset (γ i)
i : ι
a : α i
b : β i
x : γ i
⊢ (∃ a_1,
      a_1 ∈
          f ((_ : { fst := i, snd := a }.fst = { fst := i, snd := a }.fst) ▸ { fst := i, snd := a }.snd)
            { fst := i, snd := b }.snd ∧
        ↑(Embedding.sigmaMk { fst := i, snd := b }.fst) a_1 = { fst := i, snd := x }) →
    x ∈ f a b
rintro ⟨x, hx, _, rfl⟩
no goals
case intro.intro.refl
ι : Type u_2
α : ι → Type u_3
β : ι → Type u_4
γ : ι → Type u_1
inst✝ : DecidableEq ι
f : ⦃i : ι⦄ → α i → β i → Finset (γ i)
i : ι
a : α i
b : β i
x : γ i
hx :
  x ∈
    f ((_ : { fst := i, snd := a }.fst = { fst := i, snd := a }.fst) ▸ { fst := i, snd := a }.snd)
      { fst := i, snd := b }.snd
⊢ x ∈ f a b
exact hx