[GOAL]
ι : Type u_1
α : ι → Type u_2
β : Type u_3
s s₁ s₂ : Finset ι
t t₁ t₂ : (i : ι) → Finset (α i)
⊢ Finset.Nonempty (Finset.sigma s t) ↔ ∃ i, i ∈ s ∧ Finset.Nonempty (t i)
[PROOFSTEP]
simp [Finset.Nonempty]
[GOAL]
ι : Type u_1
α : ι → Type u_2
β : Type u_3
s s₁ s₂ : Finset ι
t t₁ t₂ : (i : ι) → Finset (α i)
⊢ Finset.sigma s t = ∅ ↔ ∀ (i : ι), i ∈ s → t i = ∅
[PROOFSTEP]
simp only [← not_nonempty_iff_eq_empty, sigma_nonempty, not_exists, not_and]
[GOAL]
ι : Type u_1
α : ι → Type u_2
β : Type u_3
s s₁ s₂ : Finset ι
t t₁ t₂ : (i : ι) → Finset (α i)
⊢ Set.PairwiseDisjoint ↑s fun i => map (Embedding.sigmaMk i) (t i)
[PROOFSTEP]
intro i _ j _ hij
[GOAL]
ι : Type u_1
α : ι → Type u_2
β : Type u_3
s s₁ s₂ : Finset ι
t t₁ t₂ : (i : ι) → Finset (α i)
i : ι
a✝¹ : i ∈ ↑s
j : ι
a✝ : j ∈ ↑s
hij : i ≠ j
⊢ (_root_.Disjoint on fun i => map (Embedding.sigmaMk i) (t i)) i j
[PROOFSTEP]
rw [Function.onFun, disjoint_left]
[GOAL]
ι : Type u_1
α : ι → Type u_2
β : Type u_3
s s₁ s₂ : Finset ι
t t₁ t₂ : (i : ι) → Finset (α i)
i : ι
a✝¹ : i ∈ ↑s
j : ι
a✝ : j ∈ ↑s
hij : i ≠ j
⊢ ∀ ⦃a : (x : ι) × α x⦄, a ∈ map (Embedding.sigmaMk i) (t i) → ¬a ∈ map (Embedding.sigmaMk j) (t j)
[PROOFSTEP]
simp_rw [mem_map, Function.Embedding.sigmaMk_apply]
[GOAL]
ι : Type u_1
α : ι → Type u_2
β : Type u_3
s s₁ s₂ : Finset ι
t t₁ t₂ : (i : ι) → Finset (α i)
i : ι
a✝¹ : i ∈ ↑s
j : ι
a✝ : j ∈ ↑s
hij : i ≠ j
⊢ ∀ ⦃a : (x : ι) × α x⦄,
    (∃ a_1, a_1 ∈ t i ∧ { fst := i, snd := a_1 } = a) → ¬∃ a_2, a_2 ∈ t j ∧ { fst := j, snd := a_2 } = a
[PROOFSTEP]
rintro _ ⟨y, _, rfl⟩ ⟨z, _, hz'⟩
[GOAL]
case intro.intro.intro.intro
ι : Type u_1
α : ι → Type u_2
β : Type u_3
s s₁ s₂ : Finset ι
t t₁ t₂ : (i : ι) → Finset (α i)
i : ι
a✝¹ : i ∈ ↑s
j : ι
a✝ : j ∈ ↑s
hij : i ≠ j
y : α i
left✝¹ : y ∈ t i
z : α j
left✝ : z ∈ t j
hz' : { fst := j, snd := z } = { fst := i, snd := y }
⊢ False
[PROOFSTEP]
exact hij (congr_arg Sigma.fst hz'.symm)
[GOAL]
ι : Type u_1
α : ι → Type u_2
β : Type u_3
s✝ s₁ s₂ : Finset ι
t✝ t₁ t₂ : (i : ι) → Finset (α i)
inst✝ : DecidableEq ((i : ι) × α i)
s : Finset ι
t : (i : ι) → Finset (α i)
⊢ Finset.sigma s t = Finset.biUnion s fun i => map (Embedding.sigmaMk i) (t i)
[PROOFSTEP]
ext ⟨x, y⟩
[GOAL]
case a.mk
ι : Type u_1
α : ι → Type u_2
β : Type u_3
s✝ s₁ s₂ : Finset ι
t✝ t₁ t₂ : (i : ι) → Finset (α i)
inst✝ : DecidableEq ((i : ι) × α i)
s : Finset ι
t : (i : ι) → Finset (α i)
x : ι
y : α x
⊢ { fst := x, snd := y } ∈ Finset.sigma s t ↔
    { fst := x, snd := y } ∈ Finset.biUnion s fun i => map (Embedding.sigmaMk i) (t i)
[PROOFSTEP]
simp [and_left_comm]
[GOAL]
ι : Type u_1
α : ι → Type u_2
β : Type u_3
s s₁ s₂ : Finset ι
t t₁ t₂ : (i : ι) → Finset (α i)
f : (i : ι) × α i → β
inst✝¹ : SemilatticeSup β
inst✝ : OrderBot β
⊢ sup (Finset.sigma s t) f = sup s fun i => sup (t i) fun b => f { fst := i, snd := b }
[PROOFSTEP]
simp only [le_antisymm_iff, Finset.sup_le_iff, mem_sigma, and_imp, Sigma.forall]
[GOAL]
ι : Type u_1
α : ι → Type u_2
β : Type u_3
s s₁ s₂ : Finset ι
t t₁ t₂ : (i : ι) → Finset (α i)
f : (i : ι) × α i → β
inst✝¹ : SemilatticeSup β
inst✝ : OrderBot β
⊢ (∀ (a : ι) (b : α a),
      a ∈ s → b ∈ t a → f { fst := a, snd := b } ≤ sup s fun i => sup (t i) fun b => f { fst := i, snd := b }) ∧
    ∀ (b : ι), b ∈ s → ∀ (b_1 : α b), b_1 ∈ t b → f { fst := b, snd := b_1 } ≤ sup (Finset.sigma s t) f
[PROOFSTEP]
exact
  ⟨fun i a hi ha => (le_sup hi).trans' <| le_sup (f := fun a => f ⟨i, a⟩) ha, fun i hi a ha =>
    le_sup <| mem_sigma.2 ⟨hi, ha⟩⟩
[GOAL]
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
γ : ι → Type u_4
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)
[PROOFSTEP]
obtain ⟨⟨i, a⟩, j, b⟩ := a, b
[GOAL]
case mk.mk
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
γ : ι → Type u_4
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)
[PROOFSTEP]
obtain rfl | h := Decidable.eq_or_ne i j
[GOAL]
case mk.mk.inl
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
γ : ι → Type u_4
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)
[PROOFSTEP]
constructor
[GOAL]
case mk.mk.inl.mp
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
γ : ι → Type u_4
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)
[PROOFSTEP]
simp_rw [sigmaLift]
[GOAL]
case mk.mk.inl.mp
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
γ : ι → Type u_4
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)
[PROOFSTEP]
simp only [dite_eq_ite, ite_true, mem_map, Embedding.sigmaMk_apply, forall_exists_index, and_imp]
[GOAL]
case mk.mk.inl.mp
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
γ : ι → Type u_4
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)
[PROOFSTEP]
rintro x hx rfl
[GOAL]
case mk.mk.inl.mp
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
γ : ι → Type u_4
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)
[PROOFSTEP]
exact ⟨rfl, rfl, hx⟩
[GOAL]
case mk.mk.inl.mpr
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
γ : ι → Type u_4
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 }
[PROOFSTEP]
rintro ⟨⟨⟩, ⟨⟩, hx⟩
[GOAL]
case mk.mk.inl.mpr.intro.refl.intro.refl
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
γ : ι → Type u_4
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 }
[PROOFSTEP]
rw [sigmaLift, dif_pos rfl, mem_map]
[GOAL]
case mk.mk.inl.mpr.intro.refl.intro.refl
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
γ : ι → Type u_4
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
[PROOFSTEP]
exact ⟨_, hx, by simp [Sigma.ext_iff]⟩
[GOAL]
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
γ : ι → Type u_4
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
[PROOFSTEP]
simp [Sigma.ext_iff]
[GOAL]
case mk.mk.inr
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
γ : ι → Type u_4
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)
[PROOFSTEP]
rw [sigmaLift, dif_neg h]
[GOAL]
case mk.mk.inr
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
γ : ι → Type u_4
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)
[PROOFSTEP]
refine' iff_of_false (not_mem_empty _) _
[GOAL]
case mk.mk.inr
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
γ : ι → Type u_4
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)
[PROOFSTEP]
rintro ⟨⟨⟩, ⟨⟩, _⟩
[GOAL]
case mk.mk.inr.intro.refl.intro.refl
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
γ : ι → Type u_4
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
[PROOFSTEP]
exact h rfl
[GOAL]
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
γ : ι → Type u_4
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
[PROOFSTEP]
rw [sigmaLift, dif_pos rfl, mem_map]
[GOAL]
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
γ : ι → Type u_4
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
[PROOFSTEP]
refine' ⟨_, fun hx => ⟨_, hx, rfl⟩⟩
[GOAL]
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
γ : ι → Type u_4
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
[PROOFSTEP]
rintro ⟨x, hx, _, rfl⟩
[GOAL]
case intro.intro.refl
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
γ : ι → Type u_4
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
[PROOFSTEP]
exact hx
[GOAL]
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
γ : ι → Type u_4
inst✝ : DecidableEq ι
f : ⦃i : ι⦄ → α i → β i → Finset (γ i)
a : Sigma α
b : Sigma β
x : Sigma γ
h : a.fst ≠ x.fst
⊢ ¬x ∈ sigmaLift f a b
[PROOFSTEP]
rw [mem_sigmaLift]
[GOAL]
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
γ : ι → Type u_4
inst✝ : DecidableEq ι
f : ⦃i : ι⦄ → α i → β i → Finset (γ i)
a : Sigma α
b : Sigma β
x : Sigma γ
h : a.fst ≠ x.fst
⊢ ¬∃ ha hb, x.snd ∈ f (ha ▸ a.snd) (hb ▸ b.snd)
[PROOFSTEP]
exact fun H => h H.fst
[GOAL]
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
γ : ι → Type u_4
inst✝ : DecidableEq ι
f : ⦃i : ι⦄ → α i → β i → Finset (γ i)
a : Sigma α
b : Sigma β
x : Sigma γ
h : b.fst ≠ x.fst
⊢ ¬x ∈ sigmaLift f a b
[PROOFSTEP]
rw [mem_sigmaLift]
[GOAL]
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
γ : ι → Type u_4
inst✝ : DecidableEq ι
f : ⦃i : ι⦄ → α i → β i → Finset (γ i)
a : Sigma α
b : Sigma β
x : Sigma γ
h : b.fst ≠ x.fst
⊢ ¬∃ ha hb, x.snd ∈ f (ha ▸ a.snd) (hb ▸ b.snd)
[PROOFSTEP]
exact fun H => h H.snd.fst
[GOAL]
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
γ : ι → Type u_4
inst✝ : DecidableEq ι
f g : ⦃i : ι⦄ → α i → β i → Finset (γ i)
a : (i : ι) × α i
b : (i : ι) × β i
⊢ Finset.Nonempty (sigmaLift f a b) ↔ ∃ h, Finset.Nonempty (f (h ▸ a.snd) b.snd)
[PROOFSTEP]
simp_rw [nonempty_iff_ne_empty, sigmaLift]
[GOAL]
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
γ : ι → Type u_4
inst✝ : DecidableEq ι
f g : ⦃i : ι⦄ → α i → β i → Finset (γ i)
a : (i : ι) × α i
b : (i : ι) × β i
⊢ (if h : a.fst = b.fst then map (Embedding.sigmaMk b.fst) (f (h ▸ a.snd) b.snd) else ∅) ≠ ∅ ↔
    ∃ h, f ((_ : a.fst = b.fst) ▸ a.snd) b.snd ≠ ∅
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
γ : ι → Type u_4
inst✝ : DecidableEq ι
f g : ⦃i : ι⦄ → α i → β i → Finset (γ i)
a : (i : ι) × α i
b : (i : ι) × β i
h : a.fst = b.fst
⊢ map (Embedding.sigmaMk b.fst) (f (h ▸ a.snd) b.snd) ≠ ∅ ↔ ∃ h, f ((_ : a.fst = b.fst) ▸ a.snd) b.snd ≠ ∅
[PROOFSTEP]
simp [h]
[GOAL]
case neg
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
γ : ι → Type u_4
inst✝ : DecidableEq ι
f g : ⦃i : ι⦄ → α i → β i → Finset (γ i)
a : (i : ι) × α i
b : (i : ι) × β i
h : ¬a.fst = b.fst
⊢ ∅ ≠ ∅ ↔ ∃ h, f ((_ : a.fst = b.fst) ▸ a.snd) b.snd ≠ ∅
[PROOFSTEP]
simp [h]
[GOAL]
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
γ : ι → Type u_4
inst✝ : DecidableEq ι
f g : ⦃i : ι⦄ → α i → β i → Finset (γ i)
a : (i : ι) × α i
b : (i : ι) × β i
⊢ sigmaLift f a b = ∅ ↔ ∀ (h : a.fst = b.fst), f (h ▸ a.snd) b.snd = ∅
[PROOFSTEP]
simp_rw [sigmaLift]
[GOAL]
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
γ : ι → Type u_4
inst✝ : DecidableEq ι
f g : ⦃i : ι⦄ → α i → β i → Finset (γ i)
a : (i : ι) × α i
b : (i : ι) × β i
⊢ (if h : a.fst = b.fst then map (Embedding.sigmaMk b.fst) (f (h ▸ a.snd) b.snd) else ∅) = ∅ ↔
    ∀ (h : a.fst = b.fst), f (h ▸ a.snd) b.snd = ∅
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
γ : ι → Type u_4
inst✝ : DecidableEq ι
f g : ⦃i : ι⦄ → α i → β i → Finset (γ i)
a : (i : ι) × α i
b : (i : ι) × β i
h : a.fst = b.fst
⊢ map (Embedding.sigmaMk b.fst) (f (h ▸ a.snd) b.snd) = ∅ ↔ ∀ (h : a.fst = b.fst), f (h ▸ a.snd) b.snd = ∅
[PROOFSTEP]
simp [h, forall_prop_of_true h]
[GOAL]
case neg
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
γ : ι → Type u_4
inst✝ : DecidableEq ι
f g : ⦃i : ι⦄ → α i → β i → Finset (γ i)
a : (i : ι) × α i
b : (i : ι) × β i
h : ¬a.fst = b.fst
⊢ ∅ = ∅ ↔ ∀ (h : a.fst = b.fst), f (h ▸ a.snd) b.snd = ∅
[PROOFSTEP]
simp [h, forall_prop_of_false h]
[GOAL]
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
γ : ι → Type u_4
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
[PROOFSTEP]
rintro x hx
[GOAL]
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
γ : ι → Type u_4
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
[PROOFSTEP]
rw [mem_sigmaLift] at hx ⊢
[GOAL]
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
γ : ι → Type u_4
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)
[PROOFSTEP]
obtain ⟨ha, hb, hx⟩ := hx
[GOAL]
case intro.intro
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
γ : ι → Type u_4
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)
[PROOFSTEP]
exact ⟨ha, hb, h hx⟩
[GOAL]
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
γ : ι → Type u_4
inst✝ : DecidableEq ι
f g : ⦃i : ι⦄ → α i → β i → Finset (γ i)
a : (i : ι) × α i
b : (i : ι) × β i
⊢ card (sigmaLift f a b) = if h : a.fst = b.fst then card (f (h ▸ a.snd) b.snd) else 0
[PROOFSTEP]
simp_rw [sigmaLift]
[GOAL]
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
γ : ι → Type u_4
inst✝ : DecidableEq ι
f g : ⦃i : ι⦄ → α i → β i → Finset (γ i)
a : (i : ι) × α i
b : (i : ι) × β i
⊢ card (if h : a.fst = b.fst then map (Embedding.sigmaMk b.fst) (f (h ▸ a.snd) b.snd) else ∅) =
    if h : a.fst = b.fst then card (f (h ▸ a.snd) b.snd) else 0
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
γ : ι → Type u_4
inst✝ : DecidableEq ι
f g : ⦃i : ι⦄ → α i → β i → Finset (γ i)
a : (i : ι) × α i
b : (i : ι) × β i
h : a.fst = b.fst
⊢ card (map (Embedding.sigmaMk b.fst) (f (h ▸ a.snd) b.snd)) = card (f (h ▸ a.snd) b.snd)
[PROOFSTEP]
simp [h]
[GOAL]
case neg
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
γ : ι → Type u_4
inst✝ : DecidableEq ι
f g : ⦃i : ι⦄ → α i → β i → Finset (γ i)
a : (i : ι) × α i
b : (i : ι) × β i
h : ¬a.fst = b.fst
⊢ card ∅ = 0
[PROOFSTEP]
simp [h]
