awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Finset.Sigma
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
h : Ne.{u_1 + 1} (α := ι) x.1 x.1
h_1 :
  Membership.mem (γ := Finset (γ (x.fst (β := γ))))
    (f
      (Eq.rec (motive := fun (x_1 : ι) (h : (Sigma.mk (β := α) x.1 a).fst (β := α) = x_1) ↦ α x_1)
        ((Sigma.mk (β := α) x.1 a).snd (β := α)) ⋯)
      (Eq.rec (motive := fun (x_1 : ι) (h : (Sigma.mk (β := β) x.1 b).fst (β := β) = x_1) ↦ β x_1)
        ((Sigma.mk (β := β) x.1 b).snd (β := β)) ⋯))
    (x.snd (β := γ))
⊢ False

Tactic:
exact h rfl

Premises used: rfl
-- Module: Mathlib.Data.Finset.Sigma
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
rw :
  (∃
      a_1 ∈
        f
          (Eq.rec (motive := fun (x : ι) (h : (Sigma.mk (β := α) i a).fst (β := α) = x) ↦ α x)
            ((Sigma.mk (β := α) i a).snd (β := α)) ⋯)
          ((Sigma.mk (β := β) i b).snd (β := β)),
      (Embedding.sigmaMk (β := γ) ((Sigma.mk (β := β) i b).fst (β := β)) : (a : γ ⟨i, b⟩.fst) → Sigma γ) a_1 =
        Sigma.mk (β := γ) i x) ↔
    x ∈ f a b
⊢ Sigma.mk (β := γ) i x ∈ sigmaLift (α := α) (β := β) (γ := γ) f (Sigma.mk (β := α) i a) (Sigma.mk (β := β) i b) ↔
    x ∈ f a b

Tactic:
rw [sigmaLift, dif_pos rfl, mem_map]

Premises used: dif_pos, Finset.sigmaLift, Finset.mem_map, rfl
-- Module: Mathlib.Data.Finset.Sigma
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 ∈
        f
          (Eq.rec (motive := fun (x : ι) (h : (Sigma.mk (β := α) i a).fst (β := α) = x) ↦ α x)
            ((Sigma.mk (β := α) i a).snd (β := α)) ⋯)
          ((Sigma.mk (β := β) i b).snd (β := β)),
      (Embedding.sigmaMk (β := γ) ((Sigma.mk (β := β) i b).fst (β := β)) : (a : γ ⟨i, b⟩.fst) → Sigma γ) a_1 =
        Sigma.mk (β := γ) i x) ↔
    x ∈ f a b

Tactic:
⟨?_, fun hx => ⟨_, hx, rfl⟩⟩

Premises used: And.intro, Iff.intro, Exists.intro, rfl
-- Module: Mathlib.Data.Finset.Sigma
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
refine :
  (∃
      a_1 ∈
        f
          (Eq.rec (motive := fun (x : ι) (h : (Sigma.mk (β := α) i a).fst (β := α) = x) ↦ α x)
            ((Sigma.mk (β := α) i a).snd (β := α)) ⋯)
          ((Sigma.mk (β := β) i b).snd (β := β)),
      (Embedding.sigmaMk (β := γ) ((Sigma.mk (β := β) i b).fst (β := β)) : (a : γ ⟨i, b⟩.fst) → Sigma γ) a_1 =
        Sigma.mk (β := γ) i x) →
    x ∈ f a b
⊢ (∃
      a_1 ∈
        f
          (Eq.rec (motive := fun (x : ι) (h : (Sigma.mk (β := α) i a).fst (β := α) = x) ↦ α x)
            ((Sigma.mk (β := α) i a).snd (β := α)) ⋯)
          ((Sigma.mk (β := β) i b).snd (β := β)),
      (Embedding.sigmaMk (β := γ) ((Sigma.mk (β := β) i b).fst (β := β)) : (a : γ ⟨i, b⟩.fst) → Sigma γ) a_1 =
        Sigma.mk (β := γ) i x) ↔
    x ∈ f a b

Tactic:
refine ⟨?_, fun hx => ⟨_, hx, rfl⟩⟩
-- Module: Mathlib.Data.Finset.Sigma
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
hx :
  x ∈
    f
      (Eq.rec (motive := fun (x : ι) (h : (Sigma.mk (β := α) i a).fst (β := α) = x) ↦ α x)
        ((Sigma.mk (β := α) i a).snd (β := α)) ⋯)
      ((Sigma.mk (β := β) i b).snd (β := β))
⊢ x ∈ f a b

Tactic:
hx

Premises used: Set.Mem, setOf
-- Module: Mathlib.Data.Finset.Sigma
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
hx :
  x ∈
    f
      (Eq.rec (motive := fun (x : ι) (h : (Sigma.mk (β := α) i a).fst (β := α) = x) ↦ α x)
        ((Sigma.mk (β := α) i a).snd (β := α)) ⋯)
      ((Sigma.mk (β := β) i b).snd (β := β))
⊢ x ∈ f a b

Tactic:
exact hx
-- Module: Mathlib.Data.Finset.Sigma
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 (β := γ)
rw :
  ¬∃ (ha : a.fst (β := α) = x.fst (β := γ)) (hb : b.fst (β := β) = x.fst (β := γ)),
      Membership.mem (γ := Finset (γ (x.fst (β := γ))))
        (f (Eq.rec (motive := fun (x : ι) (h : a.fst (β := α) = x) ↦ α x) (a.snd (β := α)) ha)
          (Eq.rec (motive := fun (x : ι) (h : b.fst (β := β) = x) ↦ β x) (b.snd (β := β)) hb))
        (x.snd (β := γ))
⊢ x ∉ sigmaLift (α := α) (β := β) (γ := γ) f a b

Tactic:
rw [mem_sigmaLift]

Premises used: Finset.mem_sigmaLift
-- Module: Mathlib.Data.Finset.Sigma
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 : a.fst (β := α) = x.fst (β := γ)) (hb : b.fst (β := β) = x.fst (β := γ)),
      Membership.mem (γ := Finset (γ (x.fst (β := γ))))
        (f (Eq.rec (motive := fun (x : ι) (h : a.fst (β := α) = x) ↦ α x) (a.snd (β := α)) ha)
          (Eq.rec (motive := fun (x : ι) (h : b.fst (β := β) = x) ↦ β x) (b.snd (β := β)) hb))
        (x.snd (β := γ))

Tactic:
fun H => h H.fst

Premises used: Exists.fst, Not
-- Module: Mathlib.Data.Finset.Sigma
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 : a.fst (β := α) = x.fst (β := γ)) (hb : b.fst (β := β) = x.fst (β := γ)),
      Membership.mem (γ := Finset (γ (x.fst (β := γ))))
        (f (Eq.rec (motive := fun (x : ι) (h : a.fst (β := α) = x) ↦ α x) (a.snd (β := α)) ha)
          (Eq.rec (motive := fun (x : ι) (h : b.fst (β := β) = x) ↦ β x) (b.snd (β := β)) hb))
        (x.snd (β := γ))

Tactic:
exact fun H => h H.fst
-- Module: Mathlib.Data.Finset.Sigma
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 (β := γ)
rw :
  ¬∃ (ha : a.fst (β := α) = x.fst (β := γ)) (hb : b.fst (β := β) = x.fst (β := γ)),
      Membership.mem (γ := Finset (γ (x.fst (β := γ))))
        (f (Eq.rec (motive := fun (x : ι) (h : a.fst (β := α) = x) ↦ α x) (a.snd (β := α)) ha)
          (Eq.rec (motive := fun (x : ι) (h : b.fst (β := β) = x) ↦ β x) (b.snd (β := β)) hb))
        (x.snd (β := γ))
⊢ x ∉ sigmaLift (α := α) (β := β) (γ := γ) f a b

Tactic:
rw [mem_sigmaLift]

Premises used: Finset.mem_sigmaLift
-- Module: Mathlib.Data.Finset.Sigma
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 : a.fst (β := α) = x.fst (β := γ)) (hb : b.fst (β := β) = x.fst (β := γ)),
      Membership.mem (γ := Finset (γ (x.fst (β := γ))))
        (f (Eq.rec (motive := fun (x : ι) (h : a.fst (β := α) = x) ↦ α x) (a.snd (β := α)) ha)
          (Eq.rec (motive := fun (x : ι) (h : b.fst (β := β) = x) ↦ β x) (b.snd (β := β)) hb))
        (x.snd (β := γ))

Tactic:
fun H => h H.snd.fst

Premises used: Exists.fst, Exists.snd, Not
-- Module: Mathlib.Data.Finset.Sigma
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 : a.fst (β := α) = x.fst (β := γ)) (hb : b.fst (β := β) = x.fst (β := γ)),
      Membership.mem (γ := Finset (γ (x.fst (β := γ))))
        (f (Eq.rec (motive := fun (x : ι) (h : a.fst (β := α) = x) ↦ α x) (a.snd (β := α)) ha)
          (Eq.rec (motive := fun (x : ι) (h : b.fst (β := β) = x) ↦ β x) (b.snd (β := β)) hb))
        (x.snd (β := γ))

Tactic:
exact fun H => h H.snd.fst
-- Module: Mathlib.Data.Finset.Sigma
Goal:
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
γ : ι → Type u_4
inst : DecidableEq ι
f : ⦃i : ι⦄ → α i → β i → Finset (γ i)
a : (i : ι) × α i
b : (i : ι) × β i
simp_rw :
  Ne (α := Finset (Sigma γ))
      (if h : a.fst (β := α) = b.fst (β := β) then
        map (Embedding.sigmaMk (β := γ) (b.fst (β := β)))
          (f (Eq.rec (motive := fun (x : ι) (h : a.fst (β := α) = x) ↦ α x) (a.snd (β := α)) h) (b.snd (β := β)))
      else ∅)
      ∅ ↔
    ∃ (h : a.fst (β := fun (i : ι) ↦ α i) = b.fst (β := fun (i : ι) ↦ β i)),
      f
          (Eq.rec (motive := fun (x : ι) (h : a.fst (β := fun (i : ι) ↦ α i) = x) ↦ α x)
            (a.snd (β := fun (i : ι) ↦ α i)) ⋯)
          (b.snd (β := fun (i : ι) ↦ β i)) ≠
        ∅
⊢ (sigmaLift (α := α) (β := β) (γ := γ) f a b).Nonempty ↔
    ∃ (h : a.fst (β := fun (i : ι) ↦ α i) = b.fst (β := fun (i : ι) ↦ β i)),
      (f
          (Eq.rec (motive := fun (x : ι) (h : a.fst (β := fun (i : ι) ↦ α i) = x) ↦ α x)
            (a.snd (β := fun (i : ι) ↦ α i)) h)
          (b.snd (β := fun (i : ι) ↦ β i))).Nonempty

Tactic:
simp_rw [nonempty_iff_ne_empty, sigmaLift]

Premises used: Finset.nonempty_iff_ne_empty, Finset.sigmaLift
-- Module: Mathlib.Data.Finset.Sigma
Goal:
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
γ : ι → Type u_4
inst : DecidableEq ι
f : ⦃i : ι⦄ → α i → β i → Finset (γ i)
a : (i : ι) × α i
b : (i : ι) × β i
pos :
  ∀ (h : a.fst (β := α) = b.fst (β := β)),
    map (Embedding.sigmaMk (β := γ) (b.fst (β := β)))
          (f (Eq.rec (motive := fun (x : ι) (h : a.fst (β := α) = x) ↦ α x) (a.snd (β := α)) h) (b.snd (β := β))) ≠
        ∅ ↔
      ∃ (h : a.fst (β := fun (i : ι) ↦ α i) = b.fst (β := fun (i : ι) ↦ β i)),
        f
            (Eq.rec (motive := fun (x : ι) (h : a.fst (β := fun (i : ι) ↦ α i) = x) ↦ α x)
              (a.snd (β := fun (i : ι) ↦ α i)) ⋯)
            (b.snd (β := fun (i : ι) ↦ β i)) ≠
          ∅
neg :
  ∀ (h : ¬a.fst (β := α) = b.fst (β := β)),
    Ne (α := Finset (Sigma γ)) ∅ ∅ ↔
      ∃ (h : a.fst (β := fun (i : ι) ↦ α i) = b.fst (β := fun (i : ι) ↦ β i)),
        f
            (Eq.rec (motive := fun (x : ι) (h : a.fst (β := fun (i : ι) ↦ α i) = x) ↦ α x)
              (a.snd (β := fun (i : ι) ↦ α i)) ⋯)
            (b.snd (β := fun (i : ι) ↦ β i)) ≠
          ∅
⊢ Ne (α := Finset (Sigma γ))
      (if h : a.fst (β := α) = b.fst (β := β) then
        map (Embedding.sigmaMk (β := γ) (b.fst (β := β)))
          (f (Eq.rec (motive := fun (x : ι) (h : a.fst (β := α) = x) ↦ α x) (a.snd (β := α)) h) (b.snd (β := β)))
      else ∅)
      ∅ ↔
    ∃ (h : a.fst (β := fun (i : ι) ↦ α i) = b.fst (β := fun (i : ι) ↦ β i)),
      f
          (Eq.rec (motive := fun (x : ι) (h : a.fst (β := fun (i : ι) ↦ α i) = x) ↦ α x)
            (a.snd (β := fun (i : ι) ↦ α i)) ⋯)
          (b.snd (β := fun (i : ι) ↦ β i)) ≠
        ∅

Tactic:
split_ifs with h
-- Module: Mathlib.Data.Finset.Sigma
Goal:
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
γ : ι → Type u_4
inst : DecidableEq ι
f : ⦃i : ι⦄ → α i → β i → Finset (γ i)
a : (i : ι) × α i
b : (i : ι) × β i
h : a.fst (β := α) = b.fst (β := β)
⊢ map (Embedding.sigmaMk (β := γ) (b.fst (β := β)))
        (f (Eq.rec (motive := fun (x : ι) (h : a.fst (β := α) = x) ↦ α x) (a.snd (β := α)) h) (b.snd (β := β))) ≠
      ∅ ↔
    ∃ (h : a.fst (β := fun (i : ι) ↦ α i) = b.fst (β := fun (i : ι) ↦ β i)),
      f
          (Eq.rec (motive := fun (x : ι) (h : a.fst (β := fun (i : ι) ↦ α i) = x) ↦ α x)
            (a.snd (β := fun (i : ι) ↦ α i)) ⋯)
          (b.snd (β := fun (i : ι) ↦ β i)) ≠
        ∅

Tactic:
simp [h]
-- Module: Mathlib.Data.Finset.Sigma
Goal:
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
γ : ι → Type u_4
inst : DecidableEq ι
f : ⦃i : ι⦄ → α i → β i → Finset (γ i)
a : (i : ι) × α i
b : (i : ι) × β i
h : ¬a.fst (β := α) = b.fst (β := β)
⊢ Ne (α := Finset (Sigma γ)) ∅ ∅ ↔
    ∃ (h : a.fst (β := fun (i : ι) ↦ α i) = b.fst (β := fun (i : ι) ↦ β i)),
      f
          (Eq.rec (motive := fun (x : ι) (h : a.fst (β := fun (i : ι) ↦ α i) = x) ↦ α x)
            (a.snd (β := fun (i : ι) ↦ α i)) ⋯)
          (b.snd (β := fun (i : ι) ↦ β i)) ≠
        ∅

Tactic:
simp [h]
-- Module: Mathlib.Data.Finset.Sigma
Goal:
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
γ : ι → Type u_4
inst : DecidableEq ι
f : ⦃i : ι⦄ → α i → β i → Finset (γ i)
a : (i : ι) × α i
b : (i : ι) × β i
pos :
  ∀ (h : a.fst (β := α) = b.fst (β := β)),
    map (Embedding.sigmaMk (β := γ) (b.fst (β := β)))
          (f (Eq.rec (motive := fun (x : ι) (h : a.fst (β := α) = x) ↦ α x) (a.snd (β := α)) h) (b.snd (β := β))) =
        ∅ ↔
      ∀ (h : a.fst (β := fun (i : ι) ↦ α i) = b.fst (β := fun (i : ι) ↦ β i)),
        f
            (Eq.rec (motive := fun (x : ι) (h : a.fst (β := fun (i : ι) ↦ α i) = x) ↦ α x)
              (a.snd (β := fun (i : ι) ↦ α i)) h)
            (b.snd (β := fun (i : ι) ↦ β i)) =
          ∅
neg :
  ∀ (h : ¬a.fst (β := α) = b.fst (β := β)),
    Eq (α := Finset (Sigma γ)) ∅ ∅ ↔
      ∀ (h : a.fst (β := fun (i : ι) ↦ α i) = b.fst (β := fun (i : ι) ↦ β i)),
        f
            (Eq.rec (motive := fun (x : ι) (h : a.fst (β := fun (i : ι) ↦ α i) = x) ↦ α x)
              (a.snd (β := fun (i : ι) ↦ α i)) h)
            (b.snd (β := fun (i : ι) ↦ β i)) =
          ∅
⊢ Eq (α := Finset (Sigma γ))
      (if h : a.fst (β := α) = b.fst (β := β) then
        map (Embedding.sigmaMk (β := γ) (b.fst (β := β)))
          (f (Eq.rec (motive := fun (x : ι) (h : a.fst (β := α) = x) ↦ α x) (a.snd (β := α)) h) (b.snd (β := β)))
      else ∅)
      ∅ ↔
    ∀ (h : a.fst (β := fun (i : ι) ↦ α i) = b.fst (β := fun (i : ι) ↦ β i)),
      f
          (Eq.rec (motive := fun (x : ι) (h : a.fst (β := fun (i : ι) ↦ α i) = x) ↦ α x)
            (a.snd (β := fun (i : ι) ↦ α i)) h)
          (b.snd (β := fun (i : ι) ↦ β i)) =
        ∅

Tactic:
split_ifs with h
-- Module: Mathlib.Data.Finset.Sigma
Goal:
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
γ : ι → Type u_4
inst : DecidableEq ι
f : ⦃i : ι⦄ → α i → β i → Finset (γ i)
a : (i : ι) × α i
b : (i : ι) × β i
h : a.fst (β := α) = b.fst (β := β)
⊢ map (Embedding.sigmaMk (β := γ) (b.fst (β := β)))
        (f (Eq.rec (motive := fun (x : ι) (h : a.fst (β := α) = x) ↦ α x) (a.snd (β := α)) h) (b.snd (β := β))) =
      ∅ ↔
    ∀ (h : a.fst (β := fun (i : ι) ↦ α i) = b.fst (β := fun (i : ι) ↦ β i)),
      f
          (Eq.rec (motive := fun (x : ι) (h : a.fst (β := fun (i : ι) ↦ α i) = x) ↦ α x)
            (a.snd (β := fun (i : ι) ↦ α i)) h)
          (b.snd (β := fun (i : ι) ↦ β i)) =
        ∅

Tactic:
simp [h]
-- Module: Mathlib.Data.Finset.Sigma
Goal:
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
γ : ι → Type u_4
inst : DecidableEq ι
f : ⦃i : ι⦄ → α i → β i → Finset (γ i)
a : (i : ι) × α i
b : (i : ι) × β i
h : ¬a.fst (β := α) = b.fst (β := β)
⊢ Eq (α := Finset (Sigma γ)) ∅ ∅ ↔
    ∀ (h : a.fst (β := fun (i : ι) ↦ α i) = b.fst (β := fun (i : ι) ↦ β i)),
      f
          (Eq.rec (motive := fun (x : ι) (h : a.fst (β := fun (i : ι) ↦ α i) = x) ↦ α x)
            (a.snd (β := fun (i : ι) ↦ α i)) h)
          (b.snd (β := fun (i : ι) ↦ β i)) =
        ∅

Tactic:
simp [h]
-- Module: Mathlib.Data.Finset.Sigma
Goal:
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
γ : ι → Type u_4
inst : DecidableEq ι
f g : ⦃i : ι⦄ → α i → β i → Finset (γ i)
h : ∀ ⦃i : ι⦄ ⦃a : α i⦄ ⦃b : β i⦄, f a b ⊆ g a b
a : (i : ι) × α i
b : (i : ι) × β i
x : Sigma γ
hx : x ∈ sigmaLift (α := α) (β := β) (γ := γ) f a b
rw :
  ∀
    (hx :
      ∃ (ha : a.fst (β := α) = x.fst (β := γ)) (hb : b.fst (β := β) = x.fst (β := γ)),
        Membership.mem (γ := Finset (γ (x.fst (β := γ))))
          (f (Eq.rec (motive := fun (x : ι) (h : a.fst (β := α) = x) ↦ α x) (a.snd (β := α)) ha)
            (Eq.rec (motive := fun (x : ι) (h : b.fst (β := β) = x) ↦ β x) (b.snd (β := β)) hb))
          (x.snd (β := γ))),
    ∃ (ha : a.fst (β := α) = x.fst (β := γ)) (hb : b.fst (β := β) = x.fst (β := γ)),
      Membership.mem (γ := Finset (γ (x.fst (β := γ))))
        (g (Eq.rec (motive := fun (x : ι) (h : a.fst (β := α) = x) ↦ α x) (a.snd (β := α)) ha)
          (Eq.rec (motive := fun (x : ι) (h : b.fst (β := β) = x) ↦ β x) (b.snd (β := β)) hb))
        (x.snd (β := γ))
⊢ x ∈ sigmaLift (α := α) (β := β) (γ := γ) g a b

Tactic:
rw [mem_sigmaLift] at hx ⊢

Premises used: Finset.mem_sigmaLift
-- Module: Mathlib.Data.Finset.Sigma
Goal:
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
γ : ι → Type u_4
inst : DecidableEq ι
f g : ⦃i : ι⦄ → α i → β i → Finset (γ i)
h : ∀ ⦃i : ι⦄ ⦃a : α i⦄ ⦃b : β i⦄, f a b ⊆ g a b
a : (i : ι) × α i
b : (i : ι) × β i
x : Sigma γ
hx :
  ∃ (ha : a.fst (β := α) = x.fst (β := γ)) (hb : b.fst (β := β) = x.fst (β := γ)),
    Membership.mem (γ := Finset (γ (x.fst (β := γ))))
      (f (Eq.rec (motive := fun (x : ι) (h : a.fst (β := α) = x) ↦ α x) (a.snd (β := α)) ha)
        (Eq.rec (motive := fun (x : ι) (h : b.fst (β := β) = x) ↦ β x) (b.snd (β := β)) hb))
      (x.snd (β := γ))
⊢ a.fst (β := α) = x.fst (β := γ)

Tactic:
obtain ⟨ha, hb, hx⟩ := hx
-- Module: Mathlib.Data.Finset.Sigma
Goal:
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
γ : ι → Type u_4
inst : DecidableEq ι
f g : ⦃i : ι⦄ → α i → β i → Finset (γ i)
h : ∀ ⦃i : ι⦄ ⦃a : α i⦄ ⦃b : β i⦄, f a b ⊆ g a b
a : (i : ι) × α i
b : (i : ι) × β i
x : Sigma γ
hx :
  ∃ (ha : a.fst (β := α) = x.fst (β := γ)) (hb : b.fst (β := β) = x.fst (β := γ)),
    Membership.mem (γ := Finset (γ (x.fst (β := γ))))
      (f (Eq.rec (motive := fun (x : ι) (h : a.fst (β := α) = x) ↦ α x) (a.snd (β := α)) ha)
        (Eq.rec (motive := fun (x : ι) (h : b.fst (β := β) = x) ↦ β x) (b.snd (β := β)) hb))
      (x.snd (β := γ))
ha : a.fst (β := α) = x.fst (β := γ)
⊢ b.fst (β := β) = x.fst (β := γ)

Tactic:
obtain ⟨ha, hb, hx⟩ := hx
-- Module: Mathlib.Data.Finset.Sigma
Goal:
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
γ : ι → Type u_4
inst : DecidableEq ι
f g : ⦃i : ι⦄ → α i → β i → Finset (γ i)
h : ∀ ⦃i : ι⦄ ⦃a : α i⦄ ⦃b : β i⦄, f a b ⊆ g a b
a : (i : ι) × α i
b : (i : ι) × β i
x : Sigma γ
hx :
  ∃ (ha : a.fst (β := α) = x.fst (β := γ)) (hb : b.fst (β := β) = x.fst (β := γ)),
    Membership.mem (γ := Finset (γ (x.fst (β := γ))))
      (f (Eq.rec (motive := fun (x : ι) (h : a.fst (β := α) = x) ↦ α x) (a.snd (β := α)) ha)
        (Eq.rec (motive := fun (x : ι) (h : b.fst (β := β) = x) ↦ β x) (b.snd (β := β)) hb))
      (x.snd (β := γ))
ha : a.fst (β := α) = x.fst (β := γ)
hb : b.fst (β := β) = x.fst (β := γ)
⊢ Membership.mem (γ := Finset (γ (x.fst (β := γ))))
    (f (Eq.rec (motive := fun (x : ι) (h : a.fst (β := α) = x) ↦ α x) (a.snd (β := α)) ha)
      (Eq.rec (motive := fun (x : ι) (h : b.fst (β := β) = x) ↦ β x) (b.snd (β := β)) hb))
    (x.snd (β := γ))

Tactic:
obtain ⟨ha, hb, hx⟩ := hx
-- Module: Mathlib.Data.Finset.Sigma
Goal:
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
γ : ι → Type u_4
inst : DecidableEq ι
f g : ⦃i : ι⦄ → α i → β i → Finset (γ i)
h : ∀ ⦃i : ι⦄ ⦃a : α i⦄ ⦃b : β i⦄, f a b ⊆ g a b
a : (i : ι) × α i
b : (i : ι) × β i
x : Sigma γ
ha : a.fst (β := α) = x.fst (β := γ)
hb : b.fst (β := β) = x.fst (β := γ)
hx :
  Membership.mem (γ := Finset (γ (x.fst (β := γ))))
    (f (Eq.rec (motive := fun (x : ι) (h : a.fst (β := α) = x) ↦ α x) (a.snd (β := α)) ha)
      (Eq.rec (motive := fun (x : ι) (h : b.fst (β := β) = x) ↦ β x) (b.snd (β := β)) hb))
    (x.snd (β := γ))
⊢ ∃ (ha : a.fst (β := α) = x.fst (β := γ)) (hb : b.fst (β := β) = x.fst (β := γ)),
    Membership.mem (γ := Finset (γ (x.fst (β := γ))))
      (g (Eq.rec (motive := fun (x : ι) (h : a.fst (β := α) = x) ↦ α x) (a.snd (β := α)) ha)
        (Eq.rec (motive := fun (x : ι) (h : b.fst (β := β) = x) ↦ β x) (b.snd (β := β)) hb))
      (x.snd (β := γ))

Tactic:
⟨ha, hb, h hx⟩

Premises used: Exists.intro
-- Module: Mathlib.Data.Finset.Sigma
Goal:
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
γ : ι → Type u_4
inst : DecidableEq ι
f g : ⦃i : ι⦄ → α i → β i → Finset (γ i)
h : ∀ ⦃i : ι⦄ ⦃a : α i⦄ ⦃b : β i⦄, f a b ⊆ g a b
a : (i : ι) × α i
b : (i : ι) × β i
x : Sigma γ
ha : a.fst (β := α) = x.fst (β := γ)
hb : b.fst (β := β) = x.fst (β := γ)
hx :
  Membership.mem (γ := Finset (γ (x.fst (β := γ))))
    (f (Eq.rec (motive := fun (x : ι) (h : a.fst (β := α) = x) ↦ α x) (a.snd (β := α)) ha)
      (Eq.rec (motive := fun (x : ι) (h : b.fst (β := β) = x) ↦ β x) (b.snd (β := β)) hb))
    (x.snd (β := γ))
⊢ ∃ (ha : a.fst (β := α) = x.fst (β := γ)) (hb : b.fst (β := β) = x.fst (β := γ)),
    Membership.mem (γ := Finset (γ (x.fst (β := γ))))
      (g (Eq.rec (motive := fun (x : ι) (h : a.fst (β := α) = x) ↦ α x) (a.snd (β := α)) ha)
        (Eq.rec (motive := fun (x : ι) (h : b.fst (β := β) = x) ↦ β x) (b.snd (β := β)) hb))
      (x.snd (β := γ))

Tactic:
exact ⟨ha, hb, h hx⟩
-- Module: Mathlib.Data.Finset.Sigma
Goal:
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
γ : ι → Type u_4
inst : DecidableEq ι
f : ⦃i : ι⦄ → α i → β i → Finset (γ i)
a : (i : ι) × α i
b : (i : ι) × β i
pos :
  ∀ (h : a.fst (β := α) = b.fst (β := β)),
    #(map (Embedding.sigmaMk (β := γ) (b.fst (β := β)))
          (f (Eq.rec (motive := fun (x : ι) (h : a.fst (β := α) = x) ↦ α x) (a.snd (β := α)) h) (b.snd (β := β)))) =
      #(f
          (Eq.rec (motive := fun (x : ι) (h : a.fst (β := fun (i : ι) ↦ α i) = x) ↦ α x)
            (a.snd (β := fun (i : ι) ↦ α i)) h)
          (b.snd (β := fun (i : ι) ↦ β i)))
neg : ∀ (h : ¬a.fst (β := α) = b.fst (β := β)), card (α := Sigma γ) ∅ = 0
⊢ card (α := Sigma γ)
      (if h : a.fst (β := α) = b.fst (β := β) then
        map (Embedding.sigmaMk (β := γ) (b.fst (β := β)))
          (f (Eq.rec (motive := fun (x : ι) (h : a.fst (β := α) = x) ↦ α x) (a.snd (β := α)) h) (b.snd (β := β)))
      else ∅) =
    if h : a.fst (β := fun (i : ι) ↦ α i) = b.fst (β := fun (i : ι) ↦ β i) then
      #(f
          (Eq.rec (motive := fun (x : ι) (h : a.fst (β := fun (i : ι) ↦ α i) = x) ↦ α x)
            (a.snd (β := fun (i : ι) ↦ α i)) h)
          (b.snd (β := fun (i : ι) ↦ β i)))
    else 0

Tactic:
split_ifs with h
-- Module: Mathlib.Data.Finset.Sigma
Goal:
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
γ : ι → Type u_4
inst : DecidableEq ι
f : ⦃i : ι⦄ → α i → β i → Finset (γ i)
a : (i : ι) × α i
b : (i : ι) × β i
h : a.fst (β := α) = b.fst (β := β)
⊢ #(map (Embedding.sigmaMk (β := γ) (b.fst (β := β)))
        (f (Eq.rec (motive := fun (x : ι) (h : a.fst (β := α) = x) ↦ α x) (a.snd (β := α)) h) (b.snd (β := β)))) =
    #(f
        (Eq.rec (motive := fun (x : ι) (h : a.fst (β := fun (i : ι) ↦ α i) = x) ↦ α x) (a.snd (β := fun (i : ι) ↦ α i))
          h)
        (b.snd (β := fun (i : ι) ↦ β i)))

Tactic:
simp
-- Module: Mathlib.Data.Finset.Sigma
Goal:
ι : Type u_1
α : ι → Type u_2
β : ι → Type u_3
γ : ι → Type u_4
inst : DecidableEq ι
f : ⦃i : ι⦄ → α i → β i → Finset (γ i)
a : (i : ι) × α i
b : (i : ι) × β i
h : ¬a.fst (β := α) = b.fst (β := β)
⊢ card (α := Sigma γ) ∅ = 0

Tactic:
simp
-- Module: Mathlib.Data.Finset.Slice
Goal:
α : Type u_1
A B : Set (Finset α)
r : ℕ
h : A ⊆ B
hB : Sized r B
⊢ Sized r A

Tactic:
fun _x hx => hB <| h hx

Premises used: Set.Sized
-- Module: Mathlib.Data.Finset.Slice
Goal:
α : Type u_1
r : ℕ
⊢ Sized.{u_1} (α := α) r ∅

Tactic:
simp [Sized]

Premises used: Set.Sized
-- Module: Mathlib.Data.Finset.Slice
Goal:
α : Type u_1
s : Finset α
r : ℕ
⊢ Sized (α := α) r {s} ↔ #s = r

Tactic:
simp [Sized]

Premises used: Set.Sized
-- Module: Mathlib.Data.Finset.Slice
Goal:
α : Type u_1
A B : Set (Finset α)
r : ℕ
⊢ Sized r (A ∪ B) ↔ Sized r A ∧ Sized r B

Tactic:
⟨fun hA => ⟨hA.mono subset_union_left, hA.mono subset_union_right⟩, fun hA _x hx =>
    hx.elim (fun h => hA.1 h) fun h => hA.2 h⟩

Premises used: Set.subset_union_right, Set.subset_union_left, And.right, And.left, Set.Sized.mono, And.intro, Iff.intro, Or.elim
-- Module: Mathlib.Data.Finset.Slice
Goal:
α : Type u_1
ι : Sort u_2
r : ℕ
f : ι → Set (Finset α)
simp_rw : (∀ ⦃x : Finset α⦄ (x_1 : ι) (h : x ∈ f x_1), #x = r) ↔ ∀ (i : ι) ⦃x : Finset α⦄, x ∈ f i → #x = r
⊢ Sized.{u_1} (α := α) r (⋃ (i : ι), f i) ↔ ∀ (i : ι), Sized r (f i)

Tactic:
simp_rw [Set.Sized, Set.mem_iUnion, forall_exists_index]

Premises used: Set.Sized, Set.mem_iUnion, forall_exists_index
-- Module: Mathlib.Data.Finset.Slice
Goal:
α : Type u_1
ι : Sort u_2
r : ℕ
f : ι → Set (Finset α)
⊢ (∀ ⦃x : Finset α⦄ (x_1 : ι) (h : x ∈ f x_1), #x = r) ↔ ∀ (i : ι) ⦃x : Finset α⦄, x ∈ f i → #x = r

Tactic:
forall_comm

Premises used: forall_comm