awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Finset.Sigma
Goal:
ι : Type u_1
α : ι → Type u_2
s : Finset ι
t : (i : ι) → Finset (α i)
p : (i : ι) × α i → Prop
inst : DecidablePred p
h :
  ∀ (i : ι) (a : α i),
    Sigma.mk (β := fun (i : ι) ↦ α i) i a ∈ filter p (s.sigma (α := α) t) ↔
      Membership.mem (γ := Finset ((i : ι) × α i))
        (s.sigma (α := α) fun (i : ι) ↦ {x ∈ t i | p (Sigma.mk (β := fun (i : ι) ↦ α i) i x)})
        (Sigma.mk (β := fun (i : ι) ↦ α i) i a)
⊢ filter p (s.sigma (α := α) t) = s.sigma (α := α) fun (i : ι) ↦ {x ∈ t i | p (Sigma.mk (β := fun (i : ι) ↦ α i) i x)}

Tactic:
ext ⟨i, a⟩
-- Module: Mathlib.Data.Finset.Sigma
Goal:
ι : Type u_1
α : ι → Type u_2
s : Finset ι
t : (i : ι) → Finset (α i)
p : (i : ι) × α i → Prop
inst : DecidablePred p
i : ι
a : α i
⊢ Sigma.mk (β := fun (i : ι) ↦ α i) i a ∈ filter p (s.sigma (α := α) t) ↔
    Membership.mem (γ := Finset ((i : ι) × α i))
      (s.sigma (α := α) fun (i : ι) ↦ {x ∈ t i | p (Sigma.mk (β := fun (i : ι) ↦ α i) i x)})
      (Sigma.mk (β := fun (i : ι) ↦ α i) i a)

Tactic:
simp [Finset.mem_filter, Finset.mem_sigma, and_assoc]

Premises used: Finset.mem_sigma, and_assoc, Finset.mem_filter
-- Module: Mathlib.Data.Finset.Sigma
Goal:
ι : Type u_1
α : ι → Type u_2
s : Finset ι
t : (i : ι) → Finset (α i)
p : (i : ι) → α i → Prop
inst : (i : ι) → DecidablePred (p i)
⊢ {x ∈ s.sigma (α := α) t | p (x.fst (β := fun (i : ι) ↦ α i)) (x.snd (β := fun (i : ι) ↦ α i))} =
    s.sigma (α := α) fun (i : ι) ↦ filter (p i) (t i)

Tactic:
simp [filter_sigma]

Premises used: Finset.filter_sigma
-- Module: Mathlib.Data.Finset.Sigma
Goal:
ι : Type u_1
α : ι → Type u_2
β : Type u_3
s : Finset ι
t : (i : ι) → Finset (α i)
f : (i : ι) × α i → β
inst : SemilatticeSup β
inst_1 : OrderBot β
simp :
  (∀ (a : ι) (b : α a),
      a ∈ s →
        b ∈ t a →
          f (Sigma.mk (β := fun (a : ι) ↦ α a) a b) ≤
            s.sup fun (i : ι) ↦ (t i).sup fun (b : α i) ↦ f (Sigma.mk (β := fun (i : ι) ↦ α i) i b)) ∧
    ∀ b ∈ s, ∀ b_1 ∈ t b, f (Sigma.mk (β := fun (i : ι) ↦ α i) b b_1) ≤ (s.sigma (α := α) t).sup f
⊢ (s.sigma (α := α) t).sup f = s.sup fun (i : ι) ↦ (t i).sup fun (b : α i) ↦ f (Sigma.mk (β := fun (i : ι) ↦ α i) i b)

Tactic:
simp only [le_antisymm_iff, Finset.sup_le_iff, mem_sigma, and_imp, Sigma.forall]

Premises used: and_imp, Sigma.forall, Finset.mem_sigma, le_antisymm_iff, Finset.sup_le_iff
-- Module: Mathlib.Data.Finset.Sigma
Goal:
ι : Type u_1
α : ι → Type u_2
β : Type u_3
s : Finset ι
t : (i : ι) → Finset (α i)
f : (i : ι) × α i → β
inst : SemilatticeSup β
inst_1 : OrderBot β
⊢ (∀ (a : ι) (b : α a),
      a ∈ s →
        b ∈ t a →
          f (Sigma.mk (β := fun (a : ι) ↦ α a) a b) ≤
            s.sup fun (i : ι) ↦ (t i).sup fun (b : α i) ↦ f (Sigma.mk (β := fun (i : ι) ↦ α i) i b)) ∧
    ∀ b ∈ s, ∀ b_1 ∈ t b, f (Sigma.mk (β := fun (i : ι) ↦ α i) b b_1) ≤ (s.sigma (α := α) t).sup f

Tactic:
⟨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⟩⟩

Premises used: Iff.mpr, Finset.mem_sigma, And.intro, LE.le.trans', Finset.le_sup
-- Module: Mathlib.Data.Finset.Sigma
Goal:
ι : Type u_1
α : ι → Type u_2
β : Type u_3
s : Finset ι
t : (i : ι) → Finset (α i)
f : (i : ι) × α i → β
inst : SemilatticeSup β
inst_1 : OrderBot β
⊢ (∀ (a : ι) (b : α a),
      a ∈ s →
        b ∈ t a →
          f (Sigma.mk (β := fun (a : ι) ↦ α a) a b) ≤
            s.sup fun (i : ι) ↦ (t i).sup fun (b : α i) ↦ f (Sigma.mk (β := fun (i : ι) ↦ α i) i b)) ∧
    ∀ b ∈ s, ∀ b_1 ∈ t b, f (Sigma.mk (β := fun (i : ι) ↦ α i) b b_1) ≤ (s.sigma (α := α) t).sup f

Tactic:
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⟩⟩
-- Module: Mathlib.Data.Finset.Sigma
Goal:
ι : Type u_1
α : ι → Type u_2
β : Type u_3
s : Finset ι
t : (i : ι) → Finset (α i)
f : (i : ι) × α i → β
inst : SemilatticeInf β
inst_1 : OrderTop β
⊢ (s.sigma (α := α) t).inf f = s.inf fun (i : ι) ↦ (t i).inf fun (b : α i) ↦ f (Sigma.mk (β := fun (i : ι) ↦ α i) i b)

Tactic:
@sup_sigma _ _ βᵒᵈ _ _ _ _ _

Premises used: OrderDual, Finset.inf, Finset.sup_sigma
-- Module: Mathlib.Data.Finset.Sigma
Goal:
ι : Type u_1
α : ι → Type u_2
β : Type u_3
inst : CompleteLattice β
s : Finset ι
t : (i : ι) → Finset (α i)
f : Sigma α → β
simp_rw :
  Eq.{u_3 + 1} (α := β) (⨆ x ∈ (↑(s.sigma (α := α) t) : Set ((i : ι) × α i)), f x)
    (⨆ x ∈ (↑s : Set ι), ⨆ x_1 ∈ (↑(t x) : Set (α x)), f (Sigma.mk (β := α) x x_1))
simp_rw₁ :
  Eq.{u_3 + 1} (α := β)
    (⨆ (x : (i : ι) × α i),
      ⨆ (_ :
        Membership.mem (γ := Set ((i : ι) × α i)) ((↑s : Set ι).sigma (α := α) fun (i : ι) ↦ (↑(t i) : Set (α i))) x),
        f x)
    (⨆ x ∈ (↑s : Set ι), ⨆ x_1 ∈ (↑(t x) : Set (α x)), f (Sigma.mk (β := α) x x_1))
⊢ Eq.{u_3 + 1} (α := β) (⨆ ij ∈ s.sigma (α := α) t, f ij) (⨆ i ∈ s, ⨆ j ∈ t i, f (Sigma.mk (β := α) i j))

Tactic:
simp_rw [← Finset.iSup_coe, Finset.coe_sigma, biSup_sigma]

Premises used: Finset.iSup_coe, biSup_sigma, Finset.coe_sigma
-- Module: Mathlib.Data.Finset.Sigma
Goal:
ι : Type u_1
α : ι → Type u_2
β : Type u_3
inst : CompleteLattice β
s : Finset ι
t : (i : ι) → Finset (α i)
f : (i : ι) → α i → β
⊢ Eq.{u_3 + 1} (α := β) (⨆ i ∈ s, ⨆ j ∈ t i, f i j)
    (⨆ ij ∈ s.sigma (α := α) t, f (ij.fst (β := fun (i : ι) ↦ α i)) (ij.snd (β := fun (i : ι) ↦ α i)))

Tactic:
Eq.symm (biSup_finsetSigma _ _ _)

Premises used: Eq.symm, biSup_finsetSigma
-- Module: Mathlib.Data.Finset.Sigma
Goal:
ι : Type u_1
α : ι → Type u_2
β : Type u_3
inst : CompleteLattice β
s : Finset ι
t : (i : ι) → Finset (α i)
f : Sigma α → β
⊢ Eq.{u_3 + 1} (α := β) (⨅ ij ∈ s.sigma (α := α) t, f ij) (⨅ i ∈ s, ⨅ j ∈ t i, f (Sigma.mk (β := α) i j))

Tactic:
biSup_finsetSigma (β := βᵒᵈ) _ _ _

Premises used: iInf, OrderDual, biSup_finsetSigma
-- Module: Mathlib.Data.Finset.Sigma
Goal:
ι : Type u_1
α : ι → Type u_2
β : Type u_3
inst : CompleteLattice β
s : Finset ι
t : (i : ι) → Finset (α i)
f : (i : ι) → α i → β
⊢ Eq.{u_3 + 1} (α := β) (⨅ i ∈ s, ⨅ j ∈ t i, f i j)
    (⨅ ij ∈ s.sigma (α := α) t, f (ij.fst (β := fun (i : ι) ↦ α i)) (ij.snd (β := fun (i : ι) ↦ α i)))

Tactic:
Eq.symm (biInf_finsetSigma _ _ _)

Premises used: biInf_finsetSigma, Eq.symm
-- Module: Mathlib.Data.Finset.Sigma
Goal:
ι : Type u_1
α : ι → Type u_2
β : Type u_3
s : Finset ι
t : (i : ι) → Finset (α i)
f : Sigma α → Set β
⊢ Eq.{u_3 + 1} (α := Set β) (⋃ ij ∈ s.sigma (α := α) t, f ij) (⋃ i ∈ s, ⋃ j ∈ t i, f (Sigma.mk (β := α) i j))

Tactic:
biSup_finsetSigma _ _ _

Premises used: Set.iUnion, biSup_finsetSigma
-- Module: Mathlib.Data.Finset.Sigma
Goal:
ι : Type u_1
α : ι → Type u_2
β : Type u_3
s : Finset ι
t : (i : ι) → Finset (α i)
f : (i : ι) → α i → Set β
⊢ Eq.{u_3 + 1} (α := Set β) (⋃ i ∈ s, ⋃ j ∈ t i, f i j)
    (⋃ ij ∈ s.sigma (α := α) t, f (ij.fst (β := fun (i : ι) ↦ α i)) (ij.snd (β := fun (i : ι) ↦ α i)))

Tactic:
biSup_finsetSigma' _ _ _

Premises used: biSup_finsetSigma', Set.iUnion
-- Module: Mathlib.Data.Finset.Sigma
Goal:
ι : Type u_1
α : ι → Type u_2
β : Type u_3
s : Finset ι
t : (i : ι) → Finset (α i)
f : Sigma α → Set β
⊢ Eq.{u_3 + 1} (α := Set β) (⋂ ij ∈ s.sigma (α := α) t, f ij) (⋂ i ∈ s, ⋂ j ∈ t i, f (Sigma.mk (β := α) i j))

Tactic:
biInf_finsetSigma _ _ _

Premises used: Set.iInter, biInf_finsetSigma
-- Module: Mathlib.Data.Finset.Sigma
Goal:
ι : Type u_1
α : ι → Type u_2
β : Type u_3
s : Finset ι
t : (i : ι) → Finset (α i)
f : (i : ι) → α i → Set β
⊢ Eq.{u_3 + 1} (α := Set β) (⋂ i ∈ s, ⋂ j ∈ t i, f i j)
    (⋂ ij ∈ s.sigma (α := α) t, f (ij.fst (β := fun (i : ι) ↦ α i)) (ij.snd (β := fun (i : ι) ↦ α i)))

Tactic:
biInf_finsetSigma' _ _ _

Premises used: Set.iInter, biInf_finsetSigma'
-- 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 γ
obtain :
  ∀ (i : ι) (a : α i) (j : ι) (b : β j),
    x ∈ sigmaLift (α := α) (β := β) (γ := γ) f (Sigma.mk (β := α) i a) (Sigma.mk (β := β) j b) ↔
      ∃ (ha : (Sigma.mk (β := α) i a).fst (β := α) = x.fst (β := γ)) (hb :
        (Sigma.mk (β := β) j b).fst (β := β) = x.fst (β := γ)),
        Membership.mem (γ := Finset (γ (x.fst (β := γ))))
          (f
            (Eq.rec (motive := fun (x : ι) (h : (Sigma.mk (β := α) i a).fst (β := α) = x) ↦ α x)
              ((Sigma.mk (β := α) i a).snd (β := α)) ha)
            (Eq.rec (motive := fun (x : ι) (h : (Sigma.mk (β := β) j b).fst (β := β) = x) ↦ β x)
              ((Sigma.mk (β := β) j b).snd (β := β)) hb))
          (x.snd (β := γ))
⊢ x ∈ sigmaLift (α := α) (β := β) (γ := γ) f a b ↔
    ∃ (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 ⟨⟨i, a⟩, j, b⟩ := a, b
-- 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 γ
i : ι
a : α i
j : ι
b : β j
inl :
  ∀ (b : β i),
    x ∈ sigmaLift (α := α) (β := β) (γ := γ) f (Sigma.mk (β := α) i a) (Sigma.mk (β := β) i b) ↔
      ∃ (ha : (Sigma.mk (β := α) i a).fst (β := α) = x.fst (β := γ)) (hb :
        (Sigma.mk (β := β) i b).fst (β := β) = x.fst (β := γ)),
        Membership.mem (γ := Finset (γ (x.fst (β := γ))))
          (f
            (Eq.rec (motive := fun (x : ι) (h : (Sigma.mk (β := α) i a).fst (β := α) = x) ↦ α x)
              ((Sigma.mk (β := α) i a).snd (β := α)) ha)
            (Eq.rec (motive := fun (x : ι) (h : (Sigma.mk (β := β) i b).fst (β := β) = x) ↦ β x)
              ((Sigma.mk (β := β) i b).snd (β := β)) hb))
          (x.snd (β := γ))
inr :
  ∀ (h : i ≠ j),
    x ∈ sigmaLift (α := α) (β := β) (γ := γ) f (Sigma.mk (β := α) i a) (Sigma.mk (β := β) j b) ↔
      ∃ (ha : (Sigma.mk (β := α) i a).fst (β := α) = x.fst (β := γ)) (hb :
        (Sigma.mk (β := β) j b).fst (β := β) = x.fst (β := γ)),
        Membership.mem (γ := Finset (γ (x.fst (β := γ))))
          (f
            (Eq.rec (motive := fun (x : ι) (h : (Sigma.mk (β := α) i a).fst (β := α) = x) ↦ α x)
              ((Sigma.mk (β := α) i a).snd (β := α)) ha)
            (Eq.rec (motive := fun (x : ι) (h : (Sigma.mk (β := β) j b).fst (β := β) = x) ↦ β x)
              ((Sigma.mk (β := β) j b).snd (β := β)) hb))
          (x.snd (β := γ))
⊢ x ∈ sigmaLift (α := α) (β := β) (γ := γ) f (Sigma.mk (β := α) i a) (Sigma.mk (β := β) j b) ↔
    ∃ (ha : (Sigma.mk (β := α) i a).fst (β := α) = x.fst (β := γ)) (hb :
      (Sigma.mk (β := β) j b).fst (β := β) = x.fst (β := γ)),
      Membership.mem (γ := Finset (γ (x.fst (β := γ))))
        (f
          (Eq.rec (motive := fun (x : ι) (h : (Sigma.mk (β := α) i a).fst (β := α) = x) ↦ α x)
            ((Sigma.mk (β := α) i a).snd (β := α)) ha)
          (Eq.rec (motive := fun (x : ι) (h : (Sigma.mk (β := β) j b).fst (β := β) = x) ↦ β x)
            ((Sigma.mk (β := β) j b).snd (β := β)) hb))
        (x.snd (β := γ))

Tactic:
obtain rfl | h := Decidable.eq_or_ne i j

Premises used: Decidable.eq_or_ne, 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)
x : Sigma γ
i : ι
a : α i
b : β i
inl :
  x ∈ sigmaLift (α := α) (β := β) (γ := γ) f (Sigma.mk (β := α) i a) (Sigma.mk (β := β) i b) →
    ∃ (ha : (Sigma.mk (β := α) i a).fst (β := α) = x.fst (β := γ)) (hb :
      (Sigma.mk (β := β) i b).fst (β := β) = x.fst (β := γ)),
      Membership.mem (γ := Finset (γ (x.fst (β := γ))))
        (f
          (Eq.rec (motive := fun (x : ι) (h : (Sigma.mk (β := α) i a).fst (β := α) = x) ↦ α x)
            ((Sigma.mk (β := α) i a).snd (β := α)) ha)
          (Eq.rec (motive := fun (x : ι) (h : (Sigma.mk (β := β) i b).fst (β := β) = x) ↦ β x)
            ((Sigma.mk (β := β) i b).snd (β := β)) hb))
        (x.snd (β := γ))
inl₁ :
  (∃ (ha : (Sigma.mk (β := α) i a).fst (β := α) = x.fst (β := γ)) (hb :
      (Sigma.mk (β := β) i b).fst (β := β) = x.fst (β := γ)),
      Membership.mem (γ := Finset (γ (x.fst (β := γ))))
        (f
          (Eq.rec (motive := fun (x : ι) (h : (Sigma.mk (β := α) i a).fst (β := α) = x) ↦ α x)
            ((Sigma.mk (β := α) i a).snd (β := α)) ha)
          (Eq.rec (motive := fun (x : ι) (h : (Sigma.mk (β := β) i b).fst (β := β) = x) ↦ β x)
            ((Sigma.mk (β := β) i b).snd (β := β)) hb))
        (x.snd (β := γ))) →
    x ∈ sigmaLift (α := α) (β := β) (γ := γ) f (Sigma.mk (β := α) i a) (Sigma.mk (β := β) i b)
⊢ x ∈ sigmaLift (α := α) (β := β) (γ := γ) f (Sigma.mk (β := α) i a) (Sigma.mk (β := β) i b) ↔
    ∃ (ha : (Sigma.mk (β := α) i a).fst (β := α) = x.fst (β := γ)) (hb :
      (Sigma.mk (β := β) i b).fst (β := β) = x.fst (β := γ)),
      Membership.mem (γ := Finset (γ (x.fst (β := γ))))
        (f
          (Eq.rec (motive := fun (x : ι) (h : (Sigma.mk (β := α) i a).fst (β := α) = x) ↦ α x)
            ((Sigma.mk (β := α) i a).snd (β := α)) ha)
          (Eq.rec (motive := fun (x : ι) (h : (Sigma.mk (β := β) i b).fst (β := β) = x) ↦ β x)
            ((Sigma.mk (β := β) i b).snd (β := β)) hb))
        (x.snd (β := γ))

Tactic:
constructor
-- 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 γ
i : ι
a : α i
b : β i
inl :
  Membership.mem (γ := Finset (Sigma γ)) (if h : True then map (Embedding.sigmaMk (β := γ) i) (f a b) else ∅) x →
    ∃ (h : i = x.fst (β := γ)) (h_1 : i = x.fst (β := γ)),
      Membership.mem (γ := Finset (γ (x.fst (β := γ))))
        (f (Eq.rec (motive := fun (x : ι) (h : i = x) ↦ α x) a ⋯)
          (Eq.rec (motive := fun (x : ι) (h : i = x) ↦ β x) b ⋯))
        (x.snd (β := γ))
⊢ x ∈ sigmaLift (α := α) (β := β) (γ := γ) f (Sigma.mk (β := α) i a) (Sigma.mk (β := β) i b) →
    ∃ (ha : (Sigma.mk (β := α) i a).fst (β := α) = x.fst (β := γ)) (hb :
      (Sigma.mk (β := β) i b).fst (β := β) = x.fst (β := γ)),
      Membership.mem (γ := Finset (γ (x.fst (β := γ))))
        (f
          (Eq.rec (motive := fun (x : ι) (h : (Sigma.mk (β := α) i a).fst (β := α) = x) ↦ α x)
            ((Sigma.mk (β := α) i a).snd (β := α)) ha)
          (Eq.rec (motive := fun (x : ι) (h : (Sigma.mk (β := β) i b).fst (β := β) = x) ↦ β x)
            ((Sigma.mk (β := β) i b).snd (β := β)) hb))
        (x.snd (β := γ))

Tactic:
simp_rw [sigmaLift]

Premises used: 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)
x : Sigma γ
i : ι
a : α i
b : β i
inl :
  ∀ x_1 ∈ f a b,
    Sigma.mk (β := γ) i x_1 = x →
      ∃ (h : i = x.fst (β := γ)) (h_1 : i = x.fst (β := γ)),
        Membership.mem (γ := Finset (γ (x.fst (β := γ))))
          (f (Eq.rec (motive := fun (x : ι) (h : i = x) ↦ α x) a ⋯)
            (Eq.rec (motive := fun (x : ι) (h : i = x) ↦ β x) b ⋯))
          (x.snd (β := γ))
⊢ Membership.mem (γ := Finset (Sigma γ)) (if h : True then map (Embedding.sigmaMk (β := γ) i) (f a b) else ∅) x →
    ∃ (h : i = x.fst (β := γ)) (h_1 : i = x.fst (β := γ)),
      Membership.mem (γ := Finset (γ (x.fst (β := γ))))
        (f (Eq.rec (motive := fun (x : ι) (h : i = x) ↦ α x) a ⋯)
          (Eq.rec (motive := fun (x : ι) (h : i = x) ↦ β x) b ⋯))
        (x.snd (β := γ))

Tactic:
simp only [dite_eq_ite, ite_true, mem_map, Embedding.sigmaMk_apply, forall_exists_index,
        and_imp]

Premises used: Function.Embedding.sigmaMk_apply, and_imp, forall_exists_index, ite_true, dite_eq_ite, Finset.mem_map
-- 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 a b
⊢ ∃ (h : i = (Sigma.mk (β := γ) i x).fst (β := γ)) (h_1 : i = (Sigma.mk (β := γ) i x).fst (β := γ)),
    Membership.mem (γ := Finset (γ ((Sigma.mk (β := γ) i x).fst (β := γ))))
      (f (Eq.rec (motive := fun (x : ι) (h : i = x) ↦ α x) a ⋯) (Eq.rec (motive := fun (x : ι) (h : i = x) ↦ β x) b ⋯))
      ((Sigma.mk (β := γ) i x).snd (β := γ))

Tactic:
⟨rfl, rfl, hx⟩

Premises used: 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
hx : x ∈ f a b
⊢ ∃ (h : i = (Sigma.mk (β := γ) i x).fst (β := γ)) (h_1 : i = (Sigma.mk (β := γ) i x).fst (β := γ)),
    Membership.mem (γ := Finset (γ ((Sigma.mk (β := γ) i x).fst (β := γ))))
      (f (Eq.rec (motive := fun (x : ι) (h : i = x) ↦ α x) a ⋯) (Eq.rec (motive := fun (x : ι) (h : i = x) ↦ β x) b ⋯))
      ((Sigma.mk (β := γ) i x).snd (β := γ))

Tactic:
exact ⟨rfl, rfl, 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)
x : Sigma γ
a : α x.1
b : β x.1
hx :
  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 (β := γ))
inl :
  ∃
    a_1 ∈
      f
        (Eq.rec (motive := fun (x_1 : ι) (h : (Sigma.mk (β := α) x.1 a).fst (β := α) = x_1) ↦ α x_1)
          ((Sigma.mk (β := α) x.1 a).snd (β := α)) ⋯)
        ((Sigma.mk (β := β) x.1 b).snd (β := β)),
    (Embedding.sigmaMk (β := γ) ((Sigma.mk (β := β) x.1 b).fst (β := β)) : (a : γ ⟨x.1, b⟩.fst) → Sigma γ) a_1 = x
⊢ x ∈ sigmaLift (α := α) (β := β) (γ := γ) f (Sigma.mk (β := α) x.1 a) (Sigma.mk (β := β) x.1 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)
x : Sigma γ
a : α x.1
b : β x.1
hx :
  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 (β := γ))
⊢ (Embedding.sigmaMk (β := γ) ((Sigma.mk (β := β) x.1 b).fst (β := β)) : (a : γ ⟨x.1, b⟩.fst) → Sigma γ)
      (x.snd (β := γ)) =
    x

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)
x : Sigma γ
a : α x.1
b : β x.1
hx :
  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 (β := γ))
⊢ ∃
    a_1 ∈
      f
        (Eq.rec (motive := fun (x_1 : ι) (h : (Sigma.mk (β := α) x.1 a).fst (β := α) = x_1) ↦ α x_1)
          ((Sigma.mk (β := α) x.1 a).snd (β := α)) ⋯)
        ((Sigma.mk (β := β) x.1 b).snd (β := β)),
    (Embedding.sigmaMk (β := γ) ((Sigma.mk (β := β) x.1 b).fst (β := β)) : (a : γ ⟨x.1, b⟩.fst) → Sigma γ) a_1 = x

Tactic:
exact ⟨_, hx, by 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)
x : Sigma γ
i : ι
a : α i
j : ι
b : β j
h : i ≠ j
inr :
  Membership.mem (γ := Finset (Sigma γ)) ∅ x ↔
    ∃ (ha : (Sigma.mk (β := α) i a).fst (β := α) = x.fst (β := γ)) (hb :
      (Sigma.mk (β := β) j b).fst (β := β) = x.fst (β := γ)),
      Membership.mem (γ := Finset (γ (x.fst (β := γ))))
        (f
          (Eq.rec (motive := fun (x : ι) (h : (Sigma.mk (β := α) i a).fst (β := α) = x) ↦ α x)
            ((Sigma.mk (β := α) i a).snd (β := α)) ha)
          (Eq.rec (motive := fun (x : ι) (h : (Sigma.mk (β := β) j b).fst (β := β) = x) ↦ β x)
            ((Sigma.mk (β := β) j b).snd (β := β)) hb))
        (x.snd (β := γ))
⊢ x ∈ sigmaLift (α := α) (β := β) (γ := γ) f (Sigma.mk (β := α) i a) (Sigma.mk (β := β) j b) ↔
    ∃ (ha : (Sigma.mk (β := α) i a).fst (β := α) = x.fst (β := γ)) (hb :
      (Sigma.mk (β := β) j b).fst (β := β) = x.fst (β := γ)),
      Membership.mem (γ := Finset (γ (x.fst (β := γ))))
        (f
          (Eq.rec (motive := fun (x : ι) (h : (Sigma.mk (β := α) i a).fst (β := α) = x) ↦ α x)
            ((Sigma.mk (β := α) i a).snd (β := α)) ha)
          (Eq.rec (motive := fun (x : ι) (h : (Sigma.mk (β := β) j b).fst (β := β) = x) ↦ β x)
            ((Sigma.mk (β := β) j b).snd (β := β)) hb))
        (x.snd (β := γ))

Tactic:
rw [sigmaLift, dif_neg h]

Premises used: dif_neg, 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)
x : Sigma γ
i : ι
a : α i
j : ι
b : β j
h : i ≠ j
⊢ Membership.mem (γ := Finset (Sigma γ)) ∅ x ↔
    ∃ (ha : (Sigma.mk (β := α) i a).fst (β := α) = x.fst (β := γ)) (hb :
      (Sigma.mk (β := β) j b).fst (β := β) = x.fst (β := γ)),
      Membership.mem (γ := Finset (γ (x.fst (β := γ))))
        (f
          (Eq.rec (motive := fun (x : ι) (h : (Sigma.mk (β := α) i a).fst (β := α) = x) ↦ α x)
            ((Sigma.mk (β := α) i a).snd (β := α)) ha)
          (Eq.rec (motive := fun (x : ι) (h : (Sigma.mk (β := β) j b).fst (β := β) = x) ↦ β x)
            ((Sigma.mk (β := β) j b).snd (β := β)) hb))
        (x.snd (β := γ))

Tactic:
iff_of_false (notMem_empty _) ?_

Premises used: iff_of_false, Finset.notMem_empty
-- 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 γ
i : ι
a : α i
j : ι
b : β j
h : i ≠ j
inr :
  ¬∃ (ha : (Sigma.mk (β := α) i a).fst (β := α) = x.fst (β := γ)) (hb :
      (Sigma.mk (β := β) j b).fst (β := β) = x.fst (β := γ)),
      Membership.mem (γ := Finset (γ (x.fst (β := γ))))
        (f
          (Eq.rec (motive := fun (x : ι) (h : (Sigma.mk (β := α) i a).fst (β := α) = x) ↦ α x)
            ((Sigma.mk (β := α) i a).snd (β := α)) ha)
          (Eq.rec (motive := fun (x : ι) (h : (Sigma.mk (β := β) j b).fst (β := β) = x) ↦ β x)
            ((Sigma.mk (β := β) j b).snd (β := β)) hb))
        (x.snd (β := γ))
⊢ Membership.mem (γ := Finset (Sigma γ)) ∅ x ↔
    ∃ (ha : (Sigma.mk (β := α) i a).fst (β := α) = x.fst (β := γ)) (hb :
      (Sigma.mk (β := β) j b).fst (β := β) = x.fst (β := γ)),
      Membership.mem (γ := Finset (γ (x.fst (β := γ))))
        (f
          (Eq.rec (motive := fun (x : ι) (h : (Sigma.mk (β := α) i a).fst (β := α) = x) ↦ α x)
            ((Sigma.mk (β := α) i a).snd (β := α)) ha)
          (Eq.rec (motive := fun (x : ι) (h : (Sigma.mk (β := β) j b).fst (β := β) = x) ↦ β x)
            ((Sigma.mk (β := β) j b).snd (β := β)) hb))
        (x.snd (β := γ))

Tactic:
refine iff_of_false (notMem_empty _) ?_

Premises used: iff_of_false, Finset.notMem_empty
-- 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:
h rfl

Premises used: rfl