ι : Type u_2
α : ι → Type u_3
β : ι → Type u_4
γ : ι → Type u_1
inst✝ : DecidableEq ι
f g : ⦃i : ι⦄ → α i → β i → Finset (γ i)
a✝ : (i : ι) × α i
b✝ : (i : ι) × β i
h : ∀ ⦃i : ι⦄ ⦃a : α i⦄ ⦃b : β i⦄, f a b ⊆ g a b
a : (i : ι) × α i
b : (i : ι) × β i
x : (i : ι) × γ i
hx : x ∈ sigmaLift f a b
⊢ x ∈ sigmaLift g a b
ι : Type u_2
α : ι → Type u_3
β : ι → Type u_4
γ : ι → Type u_1
inst✝ : DecidableEq ι
f g : ⦃i : ι⦄ → α i → β i → Finset (γ i)
a✝ : (i : ι) × α i
b✝ : (i : ι) × β i
h : ∀ ⦃i : ι⦄ ⦃a : α i⦄ ⦃b : β i⦄, f a b ⊆ g a b
a : (i : ι) × α i
b : (i : ι) × β i
⊢ sigmaLift f a b ⊆ sigmaLift g a b
rintro x hx
ι : Type u_2
α : ι → Type u_3
β : ι → Type u_4
γ : ι → Type u_1
inst✝ : DecidableEq ι
f g : ⦃i : ι⦄ → α i → β i → Finset (γ i)
a✝ : (i : ι) × α i
b✝ : (i : ι) × β i
h : ∀ ⦃i : ι⦄ ⦃a : α i⦄ ⦃b : β i⦄, f a b ⊆ g a b
a : (i : ι) × α i
b : (i : ι) × β i
x : (i : ι) × γ i
hx : ∃ ha hb, x.snd ∈ f (ha ▸ a.snd) (hb ▸ b.snd)
⊢ ∃ ha hb, x.snd ∈ g (ha ▸ a.snd) (hb ▸ b.snd)
ι : Type u_2
α : ι → Type u_3
β : ι → Type u_4
γ : ι → Type u_1
inst✝ : DecidableEq ι
f g : ⦃i : ι⦄ → α i → β i → Finset (γ i)
a✝ : (i : ι) × α i
b✝ : (i : ι) × β i
h : ∀ ⦃i : ι⦄ ⦃a : α i⦄ ⦃b : β i⦄, f a b ⊆ g a b
a : (i : ι) × α i
b : (i : ι) × β i
x : (i : ι) × γ i
hx : x ∈ sigmaLift f a b
⊢ x ∈ sigmaLift g a b
rw [mem_sigmaLift] at hx⊢
case intro.intro
ι : Type u_2
α : ι → Type u_3
β : ι → Type u_4
γ : ι → Type u_1
inst✝ : DecidableEq ι
f g : ⦃i : ι⦄ → α i → β i → Finset (γ i)
a✝ : (i : ι) × α i
b✝ : (i : ι) × β i
h : ∀ ⦃i : ι⦄ ⦃a : α i⦄ ⦃b : β i⦄, f a b ⊆ g a b
a : (i : ι) × α i
b : (i : ι) × β i
x : (i : ι) × γ i
ha : a.fst = x.fst
hb : b.fst = x.fst
hx : x.snd ∈ f (ha ▸ a.snd) (hb ▸ b.snd)
⊢ ∃ ha hb, x.snd ∈ g (ha ▸ a.snd) (hb ▸ b.snd)
ι : Type u_2
α : ι → Type u_3
β : ι → Type u_4
γ : ι → Type u_1
inst✝ : DecidableEq ι
f g : ⦃i : ι⦄ → α i → β i → Finset (γ i)
a✝ : (i : ι) × α i
b✝ : (i : ι) × β i
h : ∀ ⦃i : ι⦄ ⦃a : α i⦄ ⦃b : β i⦄, f a b ⊆ g a b
a : (i : ι) × α i
b : (i : ι) × β i
x : (i : ι) × γ i
hx : ∃ ha hb, x.snd ∈ f (ha ▸ a.snd) (hb ▸ b.snd)
⊢ ∃ ha hb, x.snd ∈ g (ha ▸ a.snd) (hb ▸ b.snd)
obtain ⟨ha, hb, hx⟩ := hx
no goals
case intro.intro
ι : Type u_2
α : ι → Type u_3
β : ι → Type u_4
γ : ι → Type u_1
inst✝ : DecidableEq ι
f g : ⦃i : ι⦄ → α i → β i → Finset (γ i)
a✝ : (i : ι) × α i
b✝ : (i : ι) × β i
h : ∀ ⦃i : ι⦄ ⦃a : α i⦄ ⦃b : β i⦄, f a b ⊆ g a b
a : (i : ι) × α i
b : (i : ι) × β i
x : (i : ι) × γ i
ha : a.fst = x.fst
hb : b.fst = x.fst
hx : x.snd ∈ f (ha ▸ a.snd) (hb ▸ b.snd)
⊢ ∃ ha hb, x.snd ∈ g (ha ▸ a.snd) (hb ▸ b.snd)
exact ⟨ha, hb, h hx⟩