awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Finset.Sigma (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
s : Finset ι
t : (i : ι) → Finset (α i)
p : (i : ι) × α i → Prop
inst : DecidablePred p
⊢ filter p (s.sigma (α := α) t) = s.sigma (α := α) fun (i : ι) ↦ {x ∈ t i | p (Sigma.mk (β := fun (i : ι) ↦ α i) i x)}
have 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)
Tactic: ext ⟨i, a⟩
-- Lean 4 proof step from Mathlib.Data.Finset.Sigma (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
β : Type u_3
s : Finset ι
t : (i : ι) → Finset (α i)
f : (i : ι) × α i → β
inst : SemilatticeSup β
inst_1 : OrderBot β
⊢ (s.sigma (α := α) t).sup f = s.sup fun (i : ι) ↦ (t i).sup fun (b : α i) ↦ f (Sigma.mk (β := fun (i : ι) ↦ α i) i b)
have 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
Tactic: simp only [le_antisymm_iff, Finset.sup_le_iff, mem_sigma, and_imp, Sigma.forall]
-- Lean 4 proof step from Mathlib.Data.Finset.Sigma (goal)
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))
have 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))
Tactic: simp_rw [← Finset.iSup_coe, Finset.coe_sigma, biSup_sigma]
-- Lean 4 proof step from Mathlib.Data.Finset.Sigma (goal)
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))
⊢ Eq.{u_3 + 1} (α := β) (⨆ ij ∈ s.sigma (α := α) t, f ij) (⨆ i ∈ s, ⨆ j ∈ t i, f (Sigma.mk (β := α) i j))
have 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))
Tactic: simp_rw [← Finset.iSup_coe, Finset.coe_sigma, biSup_sigma]
-- Lean 4 proof step from Mathlib.Data.Finset.Sigma (goal)
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 : 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 (β := γ))
have 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 (β := γ))
Tactic: obtain ⟨⟨i, a⟩, j, b⟩ := a, b
Cleared hypotheses: a, b
-- Lean 4 proof step from Mathlib.Data.Finset.Sigma (goal)
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
⊢ 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 (β := γ))
have 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 (β := γ))
Tactic: obtain rfl | h := Decidable.eq_or_ne i j
Cleared hypotheses: j, b
-- Lean 4 proof step from Mathlib.Data.Finset.Sigma (goal)
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 (β := γ))
⊢ 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 (β := γ))
have 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 (β := γ))
Tactic: obtain rfl | h := Decidable.eq_or_ne i j
-- Lean 4 proof step from Mathlib.Data.Finset.Sigma (goal)
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
⊢ 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 (β := γ))
have 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 (β := γ))
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Finset.Sigma (goal)
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 (β := γ))
⊢ 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 (β := γ))
have 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)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Finset.Sigma (goal)
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
⊢ 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 (β := γ))
have 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 sorry) (Eq.rec (motive := fun (x : ι) (h : i = x) ↦ β x) b sorry))
      (x.snd (β := γ))
Tactic: simp_rw [sigmaLift]
-- Lean 4 proof step from Mathlib.Data.Finset.Sigma (goal)
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
⊢ 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 (β := γ))
have 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 sorry)
          (Eq.rec (motive := fun (x : ι) (h : i = x) ↦ β x) b sorry))
        (x.snd (β := γ))
Tactic: simp only [dite_eq_ite, ite_true, mem_map, Embedding.sigmaMk_apply, forall_exists_index,
        and_imp]
-- Lean 4 proof step from Mathlib.Data.Finset.Sigma (goal)
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 (β := γ))
⊢ x ∈ sigmaLift (α := α) (β := β) (γ := γ) f (Sigma.mk (β := α) x.1 a) (Sigma.mk (β := β) x.1 b)
have 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 (β := α)) sorry)
      ((Sigma.mk (β := β) x.1 b).snd (β := β)),
  (Embedding.sigmaMk (β := γ) ((Sigma.mk (β := β) x.1 b).fst (β := β)) : (a : γ ⟨x.1, b⟩.fst) → Sigma γ) a_1 = x
Tactic: rw [sigmaLift, dif_pos rfl, mem_map]
-- Lean 4 proof step from Mathlib.Data.Finset.Sigma (goal)
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
⊢ 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 (β := γ))
have 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 (β := γ))
Tactic: rw [sigmaLift, dif_neg h]
-- Lean 4 proof step from Mathlib.Data.Finset.Sigma (goal)
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 (β := γ))
have 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 (β := γ))
Tactic: refine iff_of_false (notMem_empty _) ?_
-- Lean 4 proof step from Mathlib.Data.Finset.Sigma (goal)
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
⊢ Sigma.mk (β := γ) i x ∈ sigmaLift (α := α) (β := β) (γ := γ) f (Sigma.mk (β := α) i a) (Sigma.mk (β := β) i b) ↔
    x ∈ f a b
have rw : (∃
    a_1 ∈
      f
        (Eq.rec (motive := fun (x : ι) (h : (Sigma.mk (β := α) i a).fst (β := α) = x) ↦ α x)
          ((Sigma.mk (β := α) i a).snd (β := α)) sorry)
        ((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: rw [sigmaLift, dif_pos rfl, mem_map]
-- Lean 4 proof step from Mathlib.Data.Finset.Sigma (goal)
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
have refine : (∃
    a_1 ∈
      f
        (Eq.rec (motive := fun (x : ι) (h : (Sigma.mk (β := α) i a).fst (β := α) = x) ↦ α x)
          ((Sigma.mk (β := α) i a).snd (β := α)) sorry)
        ((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⟩⟩
-- Lean 4 proof step from Mathlib.Data.Finset.Sigma (goal)
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
have 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 (β := γ))
Tactic: rw [mem_sigmaLift]
-- Lean 4 proof step from Mathlib.Data.Finset.Sigma (goal)
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
have 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 (β := γ))
Tactic: rw [mem_sigmaLift]
-- Lean 4 proof step from Mathlib.Data.Finset.Sigma (goal)
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
⊢ (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
have 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)) sorry)
        (b.snd (β := fun (i : ι) ↦ β i)) ≠
      ∅
Tactic: simp_rw [nonempty_iff_ne_empty, sigmaLift]
-- Lean 4 proof step from Mathlib.Data.Finset.Sigma (goal)
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
⊢ 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)) ≠
        ∅
have 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)) sorry)
          (b.snd (β := fun (i : ι) ↦ β i)) ≠
        ∅
Tactic: split_ifs with h