case mk.mk
ι : Type u_2
α : ι → Type u_3
β : ι → Type u_4
γ : ι → Type u_1
inst✝ : DecidableEq ι
f : ⦃i : ι⦄ → α i → β i → Finset (γ i)
x : Sigma γ
i : ι
a : α i
j : ι
b : β j
⊢ x ∈ sigmaLift f { fst := i, snd := a } { fst := j, snd := b } ↔
    ∃ ha hb, x.snd ∈ f (ha ▸ { fst := i, snd := a }.snd) (hb ▸ { fst := j, snd := b }.snd)
ι : Type u_2
α : ι → Type u_3
β : ι → Type u_4
γ : ι → Type u_1
inst✝ : DecidableEq ι
f : ⦃i : ι⦄ → α i → β i → Finset (γ i)
a : Sigma α
b : Sigma β
x : Sigma γ
⊢ x ∈ sigmaLift f a b ↔ ∃ ha hb, x.snd ∈ f (ha ▸ a.snd) (hb ▸ b.snd)
obtain ⟨⟨i, a⟩, j, b⟩ := a, b
case mk.mk.inl
ι : Type u_2
α : ι → Type u_3
β : ι → Type u_4
γ : ι → Type u_1
inst✝ : DecidableEq ι
f : ⦃i : ι⦄ → α i → β i → Finset (γ i)
x : Sigma γ
i : ι
a : α i
b : β i
⊢ x ∈ sigmaLift f { fst := i, snd := a } { fst := i, snd := b } ↔
    ∃ ha hb, x.snd ∈ f (ha ▸ { fst := i, snd := a }.snd) (hb ▸ { fst := i, snd := b }.snd)

case mk.mk.inr
ι : Type u_2
α : ι → Type u_3
β : ι → Type u_4
γ : ι → Type u_1
inst✝ : DecidableEq ι
f : ⦃i : ι⦄ → α i → β i → Finset (γ i)
x : Sigma γ
i : ι
a : α i
j : ι
b : β j
h : i ≠ j
⊢ x ∈ sigmaLift f { fst := i, snd := a } { fst := j, snd := b } ↔
    ∃ ha hb, x.snd ∈ f (ha ▸ { fst := i, snd := a }.snd) (hb ▸ { fst := j, snd := b }.snd)
case mk.mk
ι : Type u_2
α : ι → Type u_3
β : ι → Type u_4
γ : ι → Type u_1
inst✝ : DecidableEq ι
f : ⦃i : ι⦄ → α i → β i → Finset (γ i)
x : Sigma γ
i : ι
a : α i
j : ι
b : β j
⊢ x ∈ sigmaLift f { fst := i, snd := a } { fst := j, snd := b } ↔
    ∃ ha hb, x.snd ∈ f (ha ▸ { fst := i, snd := a }.snd) (hb ▸ { fst := j, snd := b }.snd)
obtain rfl | h := Decidable.eq_or_ne i j
case mk.mk.inl.mp
ι : Type u_2
α : ι → Type u_3
β : ι → Type u_4
γ : ι → Type u_1
inst✝ : DecidableEq ι
f : ⦃i : ι⦄ → α i → β i → Finset (γ i)
x : Sigma γ
i : ι
a : α i
b : β i
⊢ x ∈ sigmaLift f { fst := i, snd := a } { fst := i, snd := b } →
    ∃ ha hb, x.snd ∈ f (ha ▸ { fst := i, snd := a }.snd) (hb ▸ { fst := i, snd := b }.snd)

case mk.mk.inl.mpr
ι : Type u_2
α : ι → Type u_3
β : ι → Type u_4
γ : ι → Type u_1
inst✝ : DecidableEq ι
f : ⦃i : ι⦄ → α i → β i → Finset (γ i)
x : Sigma γ
i : ι
a : α i
b : β i
⊢ (∃ ha hb, x.snd ∈ f (ha ▸ { fst := i, snd := a }.snd) (hb ▸ { fst := i, snd := b }.snd)) →
    x ∈ sigmaLift f { fst := i, snd := a } { fst := i, snd := b }
case mk.mk.inl
ι : Type u_2
α : ι → Type u_3
β : ι → Type u_4
γ : ι → Type u_1
inst✝ : DecidableEq ι
f : ⦃i : ι⦄ → α i → β i → Finset (γ i)
x : Sigma γ
i : ι
a : α i
b : β i
⊢ x ∈ sigmaLift f { fst := i, snd := a } { fst := i, snd := b } ↔
    ∃ ha hb, x.snd ∈ f (ha ▸ { fst := i, snd := a }.snd) (hb ▸ { fst := i, snd := b }.snd)
constructor
case mk.mk.inl.mp
ι : Type u_2
α : ι → Type u_3
β : ι → Type u_4
γ : ι → Type u_1
inst✝ : DecidableEq ι
f : ⦃i : ι⦄ → α i → β i → Finset (γ i)
x : Sigma γ
i : ι
a : α i
b : β i
⊢ (x ∈ if h : True then map (Embedding.sigmaMk i) (f a b) else ∅) →
    ∃ h h_1, x.snd ∈ f ((_ : { fst := i, snd := a }.fst = x.fst) ▸ a) ((_ : { fst := i, snd := b }.fst = x.fst) ▸ b)
case mk.mk.inl.mp
ι : Type u_2
α : ι → Type u_3
β : ι → Type u_4
γ : ι → Type u_1
inst✝ : DecidableEq ι
f : ⦃i : ι⦄ → α i → β i → Finset (γ i)
x : Sigma γ
i : ι
a : α i
b : β i
⊢ x ∈ sigmaLift f { fst := i, snd := a } { fst := i, snd := b } →
    ∃ ha hb, x.snd ∈ f (ha ▸ { fst := i, snd := a }.snd) (hb ▸ { fst := i, snd := b }.snd)
simp_rw [sigmaLift]
case mk.mk.inl.mp
ι : Type u_2
α : ι → Type u_3
β : ι → Type u_4
γ : ι → Type u_1
inst✝ : DecidableEq ι
f : ⦃i : ι⦄ → α i → β i → Finset (γ i)
x : Sigma γ
i : ι
a : α i
b : β i
⊢ ∀ (x_1 : γ i),
    x_1 ∈ f a b →
      { fst := i, snd := x_1 } = x →
        ∃ h h_1, x.snd ∈ f ((_ : { fst := i, snd := a }.fst = x.fst) ▸ a) ((_ : { fst := i, snd := b }.fst = x.fst) ▸ b)
case mk.mk.inl.mp
ι : Type u_2
α : ι → Type u_3
β : ι → Type u_4
γ : ι → Type u_1
inst✝ : DecidableEq ι
f : ⦃i : ι⦄ → α i → β i → Finset (γ i)
x : Sigma γ
i : ι
a : α i
b : β i
⊢ (x ∈ if h : True then map (Embedding.sigmaMk i) (f a b) else ∅) →
    ∃ h h_1, x.snd ∈ f ((_ : { fst := i, snd := a }.fst = x.fst) ▸ a) ((_ : { fst := i, snd := b }.fst = x.fst) ▸ b)
simp only [dite_eq_ite, ite_true, mem_map, Embedding.sigmaMk_apply, forall_exists_index,
  and_imp]
case mk.mk.inl.mp
ι : 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 a b
⊢ ∃ h h_1,
    { fst := i, snd := x }.snd ∈
      f ((_ : { fst := i, snd := a }.fst = { fst := i, snd := x }.fst) ▸ a)
        ((_ : { fst := i, snd := b }.fst = { fst := i, snd := x }.fst) ▸ b)
case mk.mk.inl.mp
ι : Type u_2
α : ι → Type u_3
β : ι → Type u_4
γ : ι → Type u_1
inst✝ : DecidableEq ι
f : ⦃i : ι⦄ → α i → β i → Finset (γ i)
x : Sigma γ
i : ι
a : α i
b : β i
⊢ ∀ (x_1 : γ i),
    x_1 ∈ f a b →
      { fst := i, snd := x_1 } = x →
        ∃ h h_1, x.snd ∈ f ((_ : { fst := i, snd := a }.fst = x.fst) ▸ a) ((_ : { fst := i, snd := b }.fst = x.fst) ▸ b)
rintro x hx rfl
no goals
case mk.mk.inl.mp
ι : 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 a b
⊢ ∃ h h_1,
    { fst := i, snd := x }.snd ∈
      f ((_ : { fst := i, snd := a }.fst = { fst := i, snd := x }.fst) ▸ a)
        ((_ : { fst := i, snd := b }.fst = { fst := i, snd := x }.fst) ▸ b)
exact ⟨rfl, rfl, hx⟩
case mk.mk.inl.mpr.intro.refl.intro.refl
ι : Type u_2
α : ι → Type u_3
β : ι → Type u_4
γ : ι → Type u_1
inst✝ : DecidableEq ι
f : ⦃i : ι⦄ → α i → β i → Finset (γ i)
x : Sigma γ
a : α x.1
b : β x.1
hx :
  x.snd ∈
    f ((_ : { fst := x.1, snd := a }.fst = { fst := x.1, snd := a }.fst) ▸ { fst := x.1, snd := a }.snd)
      ((_ : { fst := x.1, snd := b }.fst = { fst := x.1, snd := b }.fst) ▸ { fst := x.1, snd := b }.snd)
⊢ x ∈ sigmaLift f { fst := x.1, snd := a } { fst := x.1, snd := b }
case mk.mk.inl.mpr
ι : Type u_2
α : ι → Type u_3
β : ι → Type u_4
γ : ι → Type u_1
inst✝ : DecidableEq ι
f : ⦃i : ι⦄ → α i → β i → Finset (γ i)
x : Sigma γ
i : ι
a : α i
b : β i
⊢ (∃ ha hb, x.snd ∈ f (ha ▸ { fst := i, snd := a }.snd) (hb ▸ { fst := i, snd := b }.snd)) →
    x ∈ sigmaLift f { fst := i, snd := a } { fst := i, snd := b }
rintro ⟨⟨⟩, ⟨⟩, hx⟩
case mk.mk.inl.mpr.intro.refl.intro.refl
ι : Type u_2
α : ι → Type u_3
β : ι → Type u_4
γ : ι → Type u_1
inst✝ : DecidableEq ι
f : ⦃i : ι⦄ → α i → β i → Finset (γ i)
x : Sigma γ
a : α x.1
b : β x.1
hx :
  x.snd ∈
    f ((_ : { fst := x.1, snd := a }.fst = { fst := x.1, snd := a }.fst) ▸ { fst := x.1, snd := a }.snd)
      ((_ : { fst := x.1, snd := b }.fst = { fst := x.1, snd := b }.fst) ▸ { fst := x.1, snd := b }.snd)
⊢ ∃ a_1,
    a_1 ∈
        f ((_ : { fst := x.1, snd := a }.fst = { fst := x.1, snd := a }.fst) ▸ { fst := x.1, snd := a }.snd)
          { fst := x.1, snd := b }.snd ∧
      ↑(Embedding.sigmaMk { fst := x.1, snd := b }.fst) a_1 = x
case mk.mk.inl.mpr.intro.refl.intro.refl
ι : Type u_2
α : ι → Type u_3
β : ι → Type u_4
γ : ι → Type u_1
inst✝ : DecidableEq ι
f : ⦃i : ι⦄ → α i → β i → Finset (γ i)
x : Sigma γ
a : α x.1
b : β x.1
hx :
  x.snd ∈
    f ((_ : { fst := x.1, snd := a }.fst = { fst := x.1, snd := a }.fst) ▸ { fst := x.1, snd := a }.snd)
      ((_ : { fst := x.1, snd := b }.fst = { fst := x.1, snd := b }.fst) ▸ { fst := x.1, snd := b }.snd)
⊢ x ∈ sigmaLift f { fst := x.1, snd := a } { fst := x.1, snd := b }
rw [sigmaLift, dif_pos rfl, mem_map]
no goals
case mk.mk.inl.mpr.intro.refl.intro.refl
ι : Type u_2
α : ι → Type u_3
β : ι → Type u_4
γ : ι → Type u_1
inst✝ : DecidableEq ι
f : ⦃i : ι⦄ → α i → β i → Finset (γ i)
x : Sigma γ
a : α x.1
b : β x.1
hx :
  x.snd ∈
    f ((_ : { fst := x.1, snd := a }.fst = { fst := x.1, snd := a }.fst) ▸ { fst := x.1, snd := a }.snd)
      ((_ : { fst := x.1, snd := b }.fst = { fst := x.1, snd := b }.fst) ▸ { fst := x.1, snd := b }.snd)
⊢ ∃ a_1,
    a_1 ∈
        f ((_ : { fst := x.1, snd := a }.fst = { fst := x.1, snd := a }.fst) ▸ { fst := x.1, snd := a }.snd)
          { fst := x.1, snd := b }.snd ∧
      ↑(Embedding.sigmaMk { fst := x.1, snd := b }.fst) a_1 = x
exact ⟨_, hx, by simp [Sigma.ext_iff]⟩
no goals
ι : Type u_2
α : ι → Type u_3
β : ι → Type u_4
γ : ι → Type u_1
inst✝ : DecidableEq ι
f : ⦃i : ι⦄ → α i → β i → Finset (γ i)
x : Sigma γ
a : α x.1
b : β x.1
hx :
  x.snd ∈
    f ((_ : { fst := x.1, snd := a }.fst = { fst := x.1, snd := a }.fst) ▸ { fst := x.1, snd := a }.snd)
      ((_ : { fst := x.1, snd := b }.fst = { fst := x.1, snd := b }.fst) ▸ { fst := x.1, snd := b }.snd)
⊢ ↑(Embedding.sigmaMk { fst := x.1, snd := b }.fst) x.snd = x
simp [Sigma.ext_iff]
case mk.mk.inr
ι : Type u_2
α : ι → Type u_3
β : ι → Type u_4
γ : ι → Type u_1
inst✝ : DecidableEq ι
f : ⦃i : ι⦄ → α i → β i → Finset (γ i)
x : Sigma γ
i : ι
a : α i
j : ι
b : β j
h : i ≠ j
⊢ x ∈ ∅ ↔ ∃ ha hb, x.snd ∈ f (ha ▸ { fst := i, snd := a }.snd) (hb ▸ { fst := j, snd := b }.snd)
case mk.mk.inr
ι : Type u_2
α : ι → Type u_3
β : ι → Type u_4
γ : ι → Type u_1
inst✝ : DecidableEq ι
f : ⦃i : ι⦄ → α i → β i → Finset (γ i)
x : Sigma γ
i : ι
a : α i
j : ι
b : β j
h : i ≠ j
⊢ x ∈ sigmaLift f { fst := i, snd := a } { fst := j, snd := b } ↔
    ∃ ha hb, x.snd ∈ f (ha ▸ { fst := i, snd := a }.snd) (hb ▸ { fst := j, snd := b }.snd)
rw [sigmaLift, dif_neg h]
case mk.mk.inr
ι : Type u_2
α : ι → Type u_3
β : ι → Type u_4
γ : ι → Type u_1
inst✝ : DecidableEq ι
f : ⦃i : ι⦄ → α i → β i → Finset (γ i)
x : Sigma γ
i : ι
a : α i
j : ι
b : β j
h : i ≠ j
⊢ ¬∃ ha hb, x.snd ∈ f (ha ▸ { fst := i, snd := a }.snd) (hb ▸ { fst := j, snd := b }.snd)
case mk.mk.inr
ι : Type u_2
α : ι → Type u_3
β : ι → Type u_4
γ : ι → Type u_1
inst✝ : DecidableEq ι
f : ⦃i : ι⦄ → α i → β i → Finset (γ i)
x : Sigma γ
i : ι
a : α i
j : ι
b : β j
h : i ≠ j
⊢ x ∈ ∅ ↔ ∃ ha hb, x.snd ∈ f (ha ▸ { fst := i, snd := a }.snd) (hb ▸ { fst := j, snd := b }.snd)
refine' iff_of_false (not_mem_empty _) _
case mk.mk.inr.intro.refl.intro.refl
ι : Type u_2
α : ι → Type u_3
β : ι → Type u_4
γ : ι → Type u_1
inst✝ : DecidableEq ι
f : ⦃i : ι⦄ → α i → β i → Finset (γ i)
x : Sigma γ
a : α x.1
b : β x.1
h : x.1 ≠ x.1
h✝ :
  x.snd ∈
    f ((_ : { fst := x.1, snd := a }.fst = { fst := x.1, snd := a }.fst) ▸ { fst := x.1, snd := a }.snd)
      ((_ : { fst := x.1, snd := b }.fst = { fst := x.1, snd := b }.fst) ▸ { fst := x.1, snd := b }.snd)
⊢ False
case mk.mk.inr
ι : Type u_2
α : ι → Type u_3
β : ι → Type u_4
γ : ι → Type u_1
inst✝ : DecidableEq ι
f : ⦃i : ι⦄ → α i → β i → Finset (γ i)
x : Sigma γ
i : ι
a : α i
j : ι
b : β j
h : i ≠ j
⊢ ¬∃ ha hb, x.snd ∈ f (ha ▸ { fst := i, snd := a }.snd) (hb ▸ { fst := j, snd := b }.snd)
rintro ⟨⟨⟩, ⟨⟩, _⟩
no goals
case mk.mk.inr.intro.refl.intro.refl
ι : Type u_2
α : ι → Type u_3
β : ι → Type u_4
γ : ι → Type u_1
inst✝ : DecidableEq ι
f : ⦃i : ι⦄ → α i → β i → Finset (γ i)
x : Sigma γ
a : α x.1
b : β x.1
h : x.1 ≠ x.1
h✝ :
  x.snd ∈
    f ((_ : { fst := x.1, snd := a }.fst = { fst := x.1, snd := a }.fst) ▸ { fst := x.1, snd := a }.snd)
      ((_ : { fst := x.1, snd := b }.fst = { fst := x.1, snd := b }.fst) ▸ { fst := x.1, snd := b }.snd)
⊢ False
exact h rfl