awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Sigma.Basic (goal)
Goal:
α : Type u_1
β : α → Type u_4
γ : (a : α) → β a → Type u_7
inst : DecidableEq α
inst_1 : (a : α) → DecidableEq (β a)
f : (i : (a : α) × β a) → γ (i.fst (β := fun (a : α) ↦ β a)) (i.snd (β := fun (a : α) ↦ β a))
ia : α
ib : β ia
x :
  γ ((mk (β := fun (a : α) ↦ β a) ia ib).fst (β := fun (a : α) ↦ β a))
    ((mk (β := fun (a : α) ↦ β a) ia ib).snd (β := fun (a : α) ↦ β a))
⊢ curry (β := fun (a : α) ↦ β a) (γ := γ)
      (update (β := fun (x : (a : α) × β a) ↦ γ (x.fst (β := fun (a : α) ↦ β a)) (x.snd (β := fun (a : α) ↦ β a))) f
        (mk (β := fun (a : α) ↦ β a) ia ib) x) =
    update (β := fun (a : α) ↦ (y : β a) → γ a y) (curry (β := fun (a : α) ↦ β a) (γ := γ) f)
      ((mk (β := fun (a : α) ↦ β a) ia ib).fst (β := fun (a : α) ↦ β a))
      (update (β := γ ((mk (β := fun (a : α) ↦ β a) ia ib).fst (β := fun (a : α) ↦ β a)))
        (curry (β := fun (a : α) ↦ β a) (γ := γ) f ((mk (β := fun (a : α) ↦ β a) ia ib).fst (β := fun (a : α) ↦ β a)))
        ((mk (β := fun (a : α) ↦ β a) ia ib).snd (β := fun (a : α) ↦ β a)) x)
have h : ∀ (ja : α) (jb : β ja),
  curry (β := fun (a : α) ↦ β a) (γ := γ)
      (update (β := fun (x : (a : α) × β a) ↦ γ (x.fst (β := fun (a : α) ↦ β a)) (x.snd (β := fun (a : α) ↦ β a))) f
        (mk (β := fun (a : α) ↦ β a) ia ib) x)
      ja jb =
    update (β := fun (a : α) ↦ (y : β a) → γ a y) (curry (β := fun (a : α) ↦ β a) (γ := γ) f)
      ((mk (β := fun (a : α) ↦ β a) ia ib).fst (β := fun (a : α) ↦ β a))
      (update (β := γ ((mk (β := fun (a : α) ↦ β a) ia ib).fst (β := fun (a : α) ↦ β a)))
        (curry (β := fun (a : α) ↦ β a) (γ := γ) f ((mk (β := fun (a : α) ↦ β a) ia ib).fst (β := fun (a : α) ↦ β a)))
        ((mk (β := fun (a : α) ↦ β a) ia ib).snd (β := fun (a : α) ↦ β a)) x)
      ja jb
Tactic: ext ja jb
-- Lean 4 proof step from Mathlib.Data.Sigma.Basic (goal)
Goal:
α : Type u_1
β : α → Type u_4
γ : (a : α) → β a → Type u_7
inst : DecidableEq α
inst_1 : (a : α) → DecidableEq (β a)
f : (i : (a : α) × β a) → γ (i.fst (β := fun (a : α) ↦ β a)) (i.snd (β := fun (a : α) ↦ β a))
ia : α
ib : β ia
x :
  γ ((mk (β := fun (a : α) ↦ β a) ia ib).fst (β := fun (a : α) ↦ β a))
    ((mk (β := fun (a : α) ↦ β a) ia ib).snd (β := fun (a : α) ↦ β a))
ja : α
jb : β ja
⊢ curry (β := fun (a : α) ↦ β a) (γ := γ)
      (update (β := fun (x : (a : α) × β a) ↦ γ (x.fst (β := fun (a : α) ↦ β a)) (x.snd (β := fun (a : α) ↦ β a))) f
        (mk (β := fun (a : α) ↦ β a) ia ib) x)
      ja jb =
    update (β := fun (a : α) ↦ (y : β a) → γ a y) (curry (β := fun (a : α) ↦ β a) (γ := γ) f)
      ((mk (β := fun (a : α) ↦ β a) ia ib).fst (β := fun (a : α) ↦ β a))
      (update (β := γ ((mk (β := fun (a : α) ↦ β a) ia ib).fst (β := fun (a : α) ↦ β a)))
        (curry (β := fun (a : α) ↦ β a) (γ := γ) f ((mk (β := fun (a : α) ↦ β a) ia ib).fst (β := fun (a : α) ↦ β a)))
        ((mk (β := fun (a : α) ↦ β a) ia ib).snd (β := fun (a : α) ↦ β a)) x)
      ja jb
have h : Eq (α := γ ja jb)
  (update (β := fun (x : (a : α) × β a) ↦ γ (x.fst (β := fun (a : α) ↦ β a)) (x.snd (β := fun (a : α) ↦ β a))) f
      (mk (β := fun (a : α) ↦ β a) ia ib) x (mk (β := fun (a : α) ↦ β a) ja jb) :
    γ ((mk (β := fun (a : α) ↦ β a) ja jb).fst (β := fun (a : α) ↦ β a))
      ((mk (β := fun (a : α) ↦ β a) ja jb).snd (β := fun (a : α) ↦ β a)))
  (update (β := fun (a : α) ↦ (y : β a) → γ a y)
    (fun (x : α) (y : (fun (a : α) ↦ β a) x) ↦ f (mk (β := fun (a : α) ↦ β a) x y))
    ((mk (β := fun (a : α) ↦ β a) ia ib).fst (β := fun (a : α) ↦ β a))
    (update (β := γ ((mk (β := fun (a : α) ↦ β a) ia ib).fst (β := fun (a : α) ↦ β a)))
      (fun (y : (fun (a : α) ↦ β a) ((mk (β := fun (a : α) ↦ β a) ia ib).fst (β := fun (a : α) ↦ β a))) ↦
        f (mk (β := fun (a : α) ↦ β a) ((mk (β := fun (a : α) ↦ β a) ia ib).fst (β := fun (a : α) ↦ β a)) y))
      ((mk (β := fun (a : α) ↦ β a) ia ib).snd (β := fun (a : α) ↦ β a)) x)
    ja jb)
Tactic: unfold Sigma.curry
-- Lean 4 proof step from Mathlib.Data.Sigma.Basic (goal)
Goal:
α : Type u_1
β : α → Type u_4
γ : (a : α) → β a → Type u_7
inst : DecidableEq α
inst_1 : (a : α) → DecidableEq (β a)
f : (i : (a : α) × β a) → γ (i.fst (β := fun (a : α) ↦ β a)) (i.snd (β := fun (a : α) ↦ β a))
ia : α
ib : β ia
x :
  γ ((mk (β := fun (a : α) ↦ β a) ia ib).fst (β := fun (a : α) ↦ β a))
    ((mk (β := fun (a : α) ↦ β a) ia ib).snd (β := fun (a : α) ↦ β a))
ja : α
jb : β ja
⊢ Eq (α := γ ja jb)
    (update (β := fun (x : (a : α) × β a) ↦ γ (x.fst (β := fun (a : α) ↦ β a)) (x.snd (β := fun (a : α) ↦ β a))) f
        (mk (β := fun (a : α) ↦ β a) ia ib) x (mk (β := fun (a : α) ↦ β a) ja jb) :
      γ ((mk (β := fun (a : α) ↦ β a) ja jb).fst (β := fun (a : α) ↦ β a))
        ((mk (β := fun (a : α) ↦ β a) ja jb).snd (β := fun (a : α) ↦ β a)))
    (update (β := fun (a : α) ↦ (y : β a) → γ a y)
      (fun (x : α) (y : (fun (a : α) ↦ β a) x) ↦ f (mk (β := fun (a : α) ↦ β a) x y))
      ((mk (β := fun (a : α) ↦ β a) ia ib).fst (β := fun (a : α) ↦ β a))
      (update (β := γ ((mk (β := fun (a : α) ↦ β a) ia ib).fst (β := fun (a : α) ↦ β a)))
        (fun (y : (fun (a : α) ↦ β a) ((mk (β := fun (a : α) ↦ β a) ia ib).fst (β := fun (a : α) ↦ β a))) ↦
          f (mk (β := fun (a : α) ↦ β a) ((mk (β := fun (a : α) ↦ β a) ia ib).fst (β := fun (a : α) ↦ β a)) y))
        ((mk (β := fun (a : α) ↦ β a) ia ib).snd (β := fun (a : α) ↦ β a)) x)
      ja jb)
have h : ∀ (jb : β ia),
  Eq (α := γ ia jb)
    (update (β := fun (x : (a : α) × β a) ↦ γ (x.fst (β := fun (a : α) ↦ β a)) (x.snd (β := fun (a : α) ↦ β a))) f
        (mk (β := fun (a : α) ↦ β a) ia ib) x (mk (β := fun (a : α) ↦ β a) ia jb) :
      γ ((mk (β := fun (a : α) ↦ β a) ia jb).fst (β := fun (a : α) ↦ β a))
        ((mk (β := fun (a : α) ↦ β a) ia jb).snd (β := fun (a : α) ↦ β a)))
    (update (β := fun (a : α) ↦ (y : β a) → γ a y)
      (fun (x : α) (y : (fun (a : α) ↦ β a) x) ↦ f (mk (β := fun (a : α) ↦ β a) x y))
      ((mk (β := fun (a : α) ↦ β a) ia ib).fst (β := fun (a : α) ↦ β a))
      (update (β := γ ((mk (β := fun (a : α) ↦ β a) ia ib).fst (β := fun (a : α) ↦ β a)))
        (fun (y : (fun (a : α) ↦ β a) ((mk (β := fun (a : α) ↦ β a) ia ib).fst (β := fun (a : α) ↦ β a))) ↦
          f (mk (β := fun (a : α) ↦ β a) ((mk (β := fun (a : α) ↦ β a) ia ib).fst (β := fun (a : α) ↦ β a)) y))
        ((mk (β := fun (a : α) ↦ β a) ia ib).snd (β := fun (a : α) ↦ β a)) x)
      ia jb)
Tactic: obtain rfl | ha := eq_or_ne ia ja
Cleared hypotheses: ja, jb
-- Lean 4 proof step from Mathlib.Data.Sigma.Basic (goal)
Goal:
α : Type u_1
β : α → Type u_4
γ : (a : α) → β a → Type u_7
inst : DecidableEq α
inst_1 : (a : α) → DecidableEq (β a)
f : (i : (a : α) × β a) → γ (i.fst (β := fun (a : α) ↦ β a)) (i.snd (β := fun (a : α) ↦ β a))
ia : α
ib : β ia
x :
  γ ((mk (β := fun (a : α) ↦ β a) ia ib).fst (β := fun (a : α) ↦ β a))
    ((mk (β := fun (a : α) ↦ β a) ia ib).snd (β := fun (a : α) ↦ β a))
jb : β ia
⊢ Eq (α := γ ia jb)
    (update (β := fun (x : (a : α) × β a) ↦ γ (x.fst (β := fun (a : α) ↦ β a)) (x.snd (β := fun (a : α) ↦ β a))) f
        (mk (β := fun (a : α) ↦ β a) ia ib) x (mk (β := fun (a : α) ↦ β a) ia jb) :
      γ ((mk (β := fun (a : α) ↦ β a) ia jb).fst (β := fun (a : α) ↦ β a))
        ((mk (β := fun (a : α) ↦ β a) ia jb).snd (β := fun (a : α) ↦ β a)))
    (update (β := fun (a : α) ↦ (y : β a) → γ a y)
      (fun (x : α) (y : (fun (a : α) ↦ β a) x) ↦ f (mk (β := fun (a : α) ↦ β a) x y))
      ((mk (β := fun (a : α) ↦ β a) ia ib).fst (β := fun (a : α) ↦ β a))
      (update (β := γ ((mk (β := fun (a : α) ↦ β a) ia ib).fst (β := fun (a : α) ↦ β a)))
        (fun (y : (fun (a : α) ↦ β a) ((mk (β := fun (a : α) ↦ β a) ia ib).fst (β := fun (a : α) ↦ β a))) ↦
          f (mk (β := fun (a : α) ↦ β a) ((mk (β := fun (a : α) ↦ β a) ia ib).fst (β := fun (a : α) ↦ β a)) y))
        ((mk (β := fun (a : α) ↦ β a) ia ib).snd (β := fun (a : α) ↦ β a)) x)
      ia jb)
have h : Eq (α := γ ia ib)
  (update (β := fun (x : (a : α) × β a) ↦ γ (x.fst (β := fun (a : α) ↦ β a)) (x.snd (β := fun (a : α) ↦ β a))) f
      (mk (β := fun (a : α) ↦ β a) ia ib) x (mk (β := fun (a : α) ↦ β a) ia ib) :
    γ ((mk (β := fun (a : α) ↦ β a) ia ib).fst (β := fun (a : α) ↦ β a))
      ((mk (β := fun (a : α) ↦ β a) ia ib).snd (β := fun (a : α) ↦ β a)))
  (update (β := fun (a : α) ↦ (y : β a) → γ a y)
    (fun (x : α) (y : (fun (a : α) ↦ β a) x) ↦ f (mk (β := fun (a : α) ↦ β a) x y))
    ((mk (β := fun (a : α) ↦ β a) ia ib).fst (β := fun (a : α) ↦ β a))
    (update (β := γ ((mk (β := fun (a : α) ↦ β a) ia ib).fst (β := fun (a : α) ↦ β a)))
      (fun (y : (fun (a : α) ↦ β a) ((mk (β := fun (a : α) ↦ β a) ia ib).fst (β := fun (a : α) ↦ β a))) ↦
        f (mk (β := fun (a : α) ↦ β a) ((mk (β := fun (a : α) ↦ β a) ia ib).fst (β := fun (a : α) ↦ β a)) y))
      ((mk (β := fun (a : α) ↦ β a) ia ib).snd (β := fun (a : α) ↦ β a)) x)
    ia ib)
Tactic: obtain rfl | hb := eq_or_ne ib jb
Cleared hypotheses: jb
-- Lean 4 proof step from Mathlib.Data.Sigma.Basic (goal)
Goal:
α : Type u_1
β : α → Type u_4
γ : (a : α) → β a → Type u_7
inst : DecidableEq α
inst_1 : (a : α) → DecidableEq (β a)
f : (i : (a : α) × β a) → γ (i.fst (β := fun (a : α) ↦ β a)) (i.snd (β := fun (a : α) ↦ β a))
ia : α
ib : β ia
x :
  γ ((mk (β := fun (a : α) ↦ β a) ia ib).fst (β := fun (a : α) ↦ β a))
    ((mk (β := fun (a : α) ↦ β a) ia ib).snd (β := fun (a : α) ↦ β a))
jb : β ia
hb : ib ≠ jb
⊢ Eq (α := γ ia jb)
    (update (β := fun (x : (a : α) × β a) ↦ γ (x.fst (β := fun (a : α) ↦ β a)) (x.snd (β := fun (a : α) ↦ β a))) f
        (mk (β := fun (a : α) ↦ β a) ia ib) x (mk (β := fun (a : α) ↦ β a) ia jb) :
      γ ((mk (β := fun (a : α) ↦ β a) ia jb).fst (β := fun (a : α) ↦ β a))
        ((mk (β := fun (a : α) ↦ β a) ia jb).snd (β := fun (a : α) ↦ β a)))
    (update (β := fun (a : α) ↦ (y : β a) → γ a y)
      (fun (x : α) (y : (fun (a : α) ↦ β a) x) ↦ f (mk (β := fun (a : α) ↦ β a) x y))
      ((mk (β := fun (a : α) ↦ β a) ia ib).fst (β := fun (a : α) ↦ β a))
      (update (β := γ ((mk (β := fun (a : α) ↦ β a) ia ib).fst (β := fun (a : α) ↦ β a)))
        (fun (y : (fun (a : α) ↦ β a) ((mk (β := fun (a : α) ↦ β a) ia ib).fst (β := fun (a : α) ↦ β a))) ↦
          f (mk (β := fun (a : α) ↦ β a) ((mk (β := fun (a : α) ↦ β a) ia ib).fst (β := fun (a : α) ↦ β a)) y))
        ((mk (β := fun (a : α) ↦ β a) ia ib).snd (β := fun (a : α) ↦ β a)) x)
      ia jb)
have h : update (β := fun (x : (a : α) × β a) ↦ γ (x.fst (β := fun (a : α) ↦ β a)) (x.snd (β := fun (a : α) ↦ β a))) f
    (mk (β := fun (a : α) ↦ β a) ia ib) x (mk (β := fun (a : α) ↦ β a) ia jb) =
  update (β := γ ia) (fun (y : β ia) ↦ f (mk (β := fun (a : α) ↦ β a) ia y)) ib x jb
Tactic: simp only [update_self]
-- Lean 4 proof step from Mathlib.Data.Sigma.Basic (goal)
Goal:
α : Type u_1
β : α → Type u_4
γ : (a : α) → β a → Type u_7
inst : DecidableEq α
inst_1 : (a : α) → DecidableEq (β a)
f : (i : (a : α) × β a) → γ (i.fst (β := fun (a : α) ↦ β a)) (i.snd (β := fun (a : α) ↦ β a))
ia : α
ib : β ia
x :
  γ ((mk (β := fun (a : α) ↦ β a) ia ib).fst (β := fun (a : α) ↦ β a))
    ((mk (β := fun (a : α) ↦ β a) ia ib).snd (β := fun (a : α) ↦ β a))
jb : β ia
hb : ib ≠ jb
⊢ update (β := fun (x : (a : α) × β a) ↦ γ (x.fst (β := fun (a : α) ↦ β a)) (x.snd (β := fun (a : α) ↦ β a))) f
      (mk (β := fun (a : α) ↦ β a) ia ib) x (mk (β := fun (a : α) ↦ β a) ia jb) =
    update (β := γ ia) (fun (y : β ia) ↦ f (mk (β := fun (a : α) ↦ β a) ia y)) ib x jb
have rw : mk (β := fun (a : α) ↦ β a) ia jb = mk (β := fun (a : α) ↦ β a) ia ib → jb = ib
Tactic: rw [Function.update_of_ne (mt _ hb.symm), Function.update_of_ne hb.symm]
-- Lean 4 proof step from Mathlib.Data.Sigma.Basic (goal)
Goal:
α : Type u_1
β : α → Type u_4
γ : (a : α) → β a → Type u_7
inst : DecidableEq α
inst_1 : (a : α) → DecidableEq (β a)
f : (i : (a : α) × β a) → γ (i.fst (β := fun (a : α) ↦ β a)) (i.snd (β := fun (a : α) ↦ β a))
ia : α
ib : β ia
x :
  γ ((mk (β := fun (a : α) ↦ β a) ia ib).fst (β := fun (a : α) ↦ β a))
    ((mk (β := fun (a : α) ↦ β a) ia ib).snd (β := fun (a : α) ↦ β a))
ja : α
jb : β ja
ha : ia ≠ ja
⊢ Eq (α := γ ja jb)
    (update (β := fun (x : (a : α) × β a) ↦ γ (x.fst (β := fun (a : α) ↦ β a)) (x.snd (β := fun (a : α) ↦ β a))) f
        (mk (β := fun (a : α) ↦ β a) ia ib) x (mk (β := fun (a : α) ↦ β a) ja jb) :
      γ ((mk (β := fun (a : α) ↦ β a) ja jb).fst (β := fun (a : α) ↦ β a))
        ((mk (β := fun (a : α) ↦ β a) ja jb).snd (β := fun (a : α) ↦ β a)))
    (update (β := fun (a : α) ↦ (y : β a) → γ a y)
      (fun (x : α) (y : (fun (a : α) ↦ β a) x) ↦ f (mk (β := fun (a : α) ↦ β a) x y))
      ((mk (β := fun (a : α) ↦ β a) ia ib).fst (β := fun (a : α) ↦ β a))
      (update (β := γ ((mk (β := fun (a : α) ↦ β a) ia ib).fst (β := fun (a : α) ↦ β a)))
        (fun (y : (fun (a : α) ↦ β a) ((mk (β := fun (a : α) ↦ β a) ia ib).fst (β := fun (a : α) ↦ β a))) ↦
          f (mk (β := fun (a : α) ↦ β a) ((mk (β := fun (a : α) ↦ β a) ia ib).fst (β := fun (a : α) ↦ β a)) y))
        ((mk (β := fun (a : α) ↦ β a) ia ib).snd (β := fun (a : α) ↦ β a)) x)
      ja jb)
have h : ja ≠ (mk (β := fun (a : α) ↦ β a) ia ib).fst (β := fun (a : α) ↦ β a)
Tactic: rw [Function.update_of_ne (ne_of_apply_ne Sigma.fst _), Function.update_of_ne]
-- Lean 4 proof step from Mathlib.Data.Sigma.Basic (goal)
Goal:
α : Type u_1
β : α → Type u_4
γ : (a : α) → β a → Type u_7
inst : DecidableEq α
inst_1 : (a : α) → DecidableEq (β a)
f : (i : (a : α) × β a) → γ (i.fst (β := fun (a : α) ↦ β a)) (i.snd (β := fun (a : α) ↦ β a))
ia : α
ib : β ia
x :
  γ ((mk (β := fun (a : α) ↦ β a) ia ib).fst (β := fun (a : α) ↦ β a))
    ((mk (β := fun (a : α) ↦ β a) ia ib).snd (β := fun (a : α) ↦ β a))
ja : α
jb : β ja
ha : ia ≠ ja
h : ja ≠ (mk (β := fun (a : α) ↦ β a) ia ib).fst (β := fun (a : α) ↦ β a)
⊢ Eq (α := γ ja jb)
    (update (β := fun (x : (a : α) × β a) ↦ γ (x.fst (β := fun (a : α) ↦ β a)) (x.snd (β := fun (a : α) ↦ β a))) f
        (mk (β := fun (a : α) ↦ β a) ia ib) x (mk (β := fun (a : α) ↦ β a) ja jb) :
      γ ((mk (β := fun (a : α) ↦ β a) ja jb).fst (β := fun (a : α) ↦ β a))
        ((mk (β := fun (a : α) ↦ β a) ja jb).snd (β := fun (a : α) ↦ β a)))
    (update (β := fun (a : α) ↦ (y : β a) → γ a y)
      (fun (x : α) (y : (fun (a : α) ↦ β a) x) ↦ f (mk (β := fun (a : α) ↦ β a) x y))
      ((mk (β := fun (a : α) ↦ β a) ia ib).fst (β := fun (a : α) ↦ β a))
      (update (β := γ ((mk (β := fun (a : α) ↦ β a) ia ib).fst (β := fun (a : α) ↦ β a)))
        (fun (y : (fun (a : α) ↦ β a) ((mk (β := fun (a : α) ↦ β a) ia ib).fst (β := fun (a : α) ↦ β a))) ↦
          f (mk (β := fun (a : α) ↦ β a) ((mk (β := fun (a : α) ↦ β a) ia ib).fst (β := fun (a : α) ↦ β a)) y))
        ((mk (β := fun (a : α) ↦ β a) ia ib).snd (β := fun (a : α) ↦ β a)) x)
      ja jb)
have rw : (mk (β := fun (a : α) ↦ β a) ja jb).fst (β := fun (a : α) ↦ β a) ≠
  (mk (β := fun (a : α) ↦ β a) ia ib).fst (β := fun (a : α) ↦ β a)
Tactic: rw [Function.update_of_ne (ne_of_apply_ne Sigma.fst _), Function.update_of_ne]
-- Lean 4 proof step from Mathlib.Data.Sigma.Interval (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : DecidableEq ι
inst_1 : (i : ι) → Preorder (α i)
inst_2 : (i : ι) → LocallyFiniteOrder (α i)
x x_1 x_2 : (i : ι) × α i
i : ι
a : α i
j : ι
b : α j
k : ι
c : α k
⊢ Membership.mem (γ := Finset ((i : ι) × α i))
      (sigmaLift (α := fun (i : ι) ↦ α i) (β := fun (i : ι) ↦ α i) (γ := fun (i : ι) ↦ α i) (fun (x : ι) ↦ Icc)
        (mk (β := fun (i : ι) ↦ α i) i a) (mk (β := fun (i : ι) ↦ α i) j b))
      (mk (β := fun (i : ι) ↦ α i) k c) ↔
    mk (β := fun (i : ι) ↦ α i) i a ≤ mk (β := fun (i : ι) ↦ α i) k c ∧
      mk (β := fun (i : ι) ↦ α i) k c ≤ mk (β := fun (i : ι) ↦ α i) j b
have simp_rw : (∃ (h : i = k) (_ : Eq.rec (motive := fun (x : ι) (h : i = x) ↦ α x) a sorry ≤ c) (x : j = k),
    c ≤ Eq.rec (motive := fun (x : ι) (h : j = x) ↦ α x) b sorry) ↔
  ∃ (h : i = k) (_ : Eq.rec (motive := fun (x : ι) (x_3 : i = x) ↦ α x) a sorry ≤ c) (h : k = j),
    Eq.rec (motive := fun (x : ι) (x_3 : k = x) ↦ α x) c sorry ≤ b
Tactic: simp_rw [mem_sigmaLift, le_def, mem_Icc, exists_and_left, ← exists_and_right, ← exists_prop]
-- Lean 4 proof step from Mathlib.Data.Sigma.Interval (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : DecidableEq ι
inst_1 : (i : ι) → Preorder (α i)
inst_2 : (i : ι) → LocallyFiniteOrder (α i)
x x_1 x_2 : (i : ι) × α i
i : ι
a : α i
j : ι
b : α j
k : ι
c : α k
h : i = k
h_1 : Eq.rec (motive := fun (x : ι) (h : i = x) ↦ α x) a ⋯ ≤ c
⊢ (∃ (x : j = k), c ≤ Eq.rec (motive := fun (x : ι) (h : j = x) ↦ α x) b ⋯) ↔
    ∃ (h : k = j), Eq.rec (motive := fun (x : ι) (x_3 : k = x) ↦ α x) c ⋯ ≤ b
have mp : (∃ (x : j = k), c ≤ Eq.rec (motive := fun (x : ι) (h : j = x) ↦ α x) b sorry) →
  ∃ (h : k = j), Eq.rec (motive := fun (x : ι) (x_3 : k = x) ↦ α x) c sorry ≤ b
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Sigma.Interval (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : DecidableEq ι
inst_1 : (i : ι) → Preorder (α i)
inst_2 : (i : ι) → LocallyFiniteOrder (α i)
x x_1 x_2 : (i : ι) × α i
i : ι
a : α i
j : ι
b : α j
k : ι
c : α k
h : i = k
h_1 : Eq.rec (motive := fun (x : ι) (h : i = x) ↦ α x) a ⋯ ≤ c
mp :
  (∃ (x : j = k), c ≤ Eq.rec (motive := fun (x : ι) (h : j = x) ↦ α x) b ⋯) →
    ∃ (h : k = j), Eq.rec (motive := fun (x : ι) (x_3 : k = x) ↦ α x) c ⋯ ≤ b
⊢ (∃ (x : j = k), c ≤ Eq.rec (motive := fun (x : ι) (h : j = x) ↦ α x) b ⋯) ↔
    ∃ (h : k = j), Eq.rec (motive := fun (x : ι) (x_3 : k = x) ↦ α x) c ⋯ ≤ b
have mpr : (∃ (h : k = j), Eq.rec (motive := fun (x : ι) (x_3 : k = x) ↦ α x) c sorry ≤ b) →
  ∃ (x : j = k), c ≤ Eq.rec (motive := fun (x : ι) (h : j = x) ↦ α x) b sorry
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Sigma.Interval (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : DecidableEq ι
inst_1 : (i : ι) → Preorder (α i)
inst_2 : (i : ι) → LocallyFiniteOrder (α i)
x x_1 x_2 : (i : ι) × α i
i : ι
a : α i
j : ι
b : α j
k : ι
c : α k
⊢ Membership.mem (γ := Finset ((i : ι) × α i))
      (sigmaLift (α := fun (i : ι) ↦ α i) (β := fun (i : ι) ↦ α i) (γ := fun (i : ι) ↦ α i) (fun (x : ι) ↦ Ico)
        (mk (β := fun (i : ι) ↦ α i) i a) (mk (β := fun (i : ι) ↦ α i) j b))
      (mk (β := fun (i : ι) ↦ α i) k c) ↔
    mk (β := fun (i : ι) ↦ α i) i a ≤ mk (β := fun (i : ι) ↦ α i) k c ∧
      mk (β := fun (i : ι) ↦ α i) k c < mk (β := fun (i : ι) ↦ α i) j b
have simp_rw : (∃ (h : i = k) (_ : Eq.rec (motive := fun (x : ι) (h : i = x) ↦ α x) a sorry ≤ c) (x : j = k),
    c < Eq.rec (motive := fun (x : ι) (h : j = x) ↦ α x) b sorry) ↔
  ∃ (h : i = k) (_ : Eq.rec (motive := fun (x : ι) (x_3 : i = x) ↦ α x) a sorry ≤ c) (h : k = j),
    Eq.rec (motive := fun (x : ι) (x_3 : k = x) ↦ α x) c sorry < b
Tactic: simp_rw [mem_sigmaLift, le_def, lt_def, mem_Ico, exists_and_left, ← exists_and_right, ←
      exists_prop]
-- Lean 4 proof step from Mathlib.Data.Sigma.Interval (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : DecidableEq ι
inst_1 : (i : ι) → Preorder (α i)
inst_2 : (i : ι) → LocallyFiniteOrder (α i)
x x_1 x_2 : (i : ι) × α i
i : ι
a : α i
j : ι
b : α j
k : ι
c : α k
h : i = k
h_1 : Eq.rec (motive := fun (x : ι) (h : i = x) ↦ α x) a ⋯ ≤ c
⊢ (∃ (x : j = k), c < Eq.rec (motive := fun (x : ι) (h : j = x) ↦ α x) b ⋯) ↔
    ∃ (h : k = j), Eq.rec (motive := fun (x : ι) (x_3 : k = x) ↦ α x) c ⋯ < b
have mp : (∃ (x : j = k), c < Eq.rec (motive := fun (x : ι) (h : j = x) ↦ α x) b sorry) →
  ∃ (h : k = j), Eq.rec (motive := fun (x : ι) (x_3 : k = x) ↦ α x) c sorry < b
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Sigma.Interval (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : DecidableEq ι
inst_1 : (i : ι) → Preorder (α i)
inst_2 : (i : ι) → LocallyFiniteOrder (α i)
x x_1 x_2 : (i : ι) × α i
i : ι
a : α i
j : ι
b : α j
k : ι
c : α k
h : i = k
h_1 : Eq.rec (motive := fun (x : ι) (h : i = x) ↦ α x) a ⋯ ≤ c
mp :
  (∃ (x : j = k), c < Eq.rec (motive := fun (x : ι) (h : j = x) ↦ α x) b ⋯) →
    ∃ (h : k = j), Eq.rec (motive := fun (x : ι) (x_3 : k = x) ↦ α x) c ⋯ < b
⊢ (∃ (x : j = k), c < Eq.rec (motive := fun (x : ι) (h : j = x) ↦ α x) b ⋯) ↔
    ∃ (h : k = j), Eq.rec (motive := fun (x : ι) (x_3 : k = x) ↦ α x) c ⋯ < b
have mpr : (∃ (h : k = j), Eq.rec (motive := fun (x : ι) (x_3 : k = x) ↦ α x) c sorry < b) →
  ∃ (x : j = k), c < Eq.rec (motive := fun (x : ι) (h : j = x) ↦ α x) b sorry
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Sigma.Interval (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : DecidableEq ι
inst_1 : (i : ι) → Preorder (α i)
inst_2 : (i : ι) → LocallyFiniteOrder (α i)
x x_1 x_2 : (i : ι) × α i
i : ι
a : α i
j : ι
b : α j
k : ι
c : α k
⊢ Membership.mem (γ := Finset ((i : ι) × α i))
      (sigmaLift (α := fun (i : ι) ↦ α i) (β := fun (i : ι) ↦ α i) (γ := fun (i : ι) ↦ α i) (fun (x : ι) ↦ Ioc)
        (mk (β := fun (i : ι) ↦ α i) i a) (mk (β := fun (i : ι) ↦ α i) j b))
      (mk (β := fun (i : ι) ↦ α i) k c) ↔
    mk (β := fun (i : ι) ↦ α i) i a < mk (β := fun (i : ι) ↦ α i) k c ∧
      mk (β := fun (i : ι) ↦ α i) k c ≤ mk (β := fun (i : ι) ↦ α i) j b
have simp_rw : (∃ (h : i = k) (_ : Eq.rec (motive := fun (x : ι) (h : i = x) ↦ α x) a sorry < c) (x : j = k),
    c ≤ Eq.rec (motive := fun (x : ι) (h : j = x) ↦ α x) b sorry) ↔
  ∃ (h : i = k) (_ : Eq.rec (motive := fun (x : ι) (x_3 : i = x) ↦ α x) a sorry < c) (h : k = j),
    Eq.rec (motive := fun (x : ι) (x_3 : k = x) ↦ α x) c sorry ≤ b
Tactic: simp_rw [mem_sigmaLift, le_def, lt_def, mem_Ioc, exists_and_left, ← exists_and_right, ←
      exists_prop]
-- Lean 4 proof step from Mathlib.Data.Sigma.Interval (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : DecidableEq ι
inst_1 : (i : ι) → Preorder (α i)
inst_2 : (i : ι) → LocallyFiniteOrder (α i)
x x_1 x_2 : (i : ι) × α i
i : ι
a : α i
j : ι
b : α j
k : ι
c : α k
h : i = k
h_1 : Eq.rec (motive := fun (x : ι) (h : i = x) ↦ α x) a ⋯ < c
⊢ (∃ (x : j = k), c ≤ Eq.rec (motive := fun (x : ι) (h : j = x) ↦ α x) b ⋯) ↔
    ∃ (h : k = j), Eq.rec (motive := fun (x : ι) (x_3 : k = x) ↦ α x) c ⋯ ≤ b
have mp : (∃ (x : j = k), c ≤ Eq.rec (motive := fun (x : ι) (h : j = x) ↦ α x) b sorry) →
  ∃ (h : k = j), Eq.rec (motive := fun (x : ι) (x_3 : k = x) ↦ α x) c sorry ≤ b
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Sigma.Interval (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : DecidableEq ι
inst_1 : (i : ι) → Preorder (α i)
inst_2 : (i : ι) → LocallyFiniteOrder (α i)
x x_1 x_2 : (i : ι) × α i
i : ι
a : α i
j : ι
b : α j
k : ι
c : α k
h : i = k
h_1 : Eq.rec (motive := fun (x : ι) (h : i = x) ↦ α x) a ⋯ < c
mp :
  (∃ (x : j = k), c ≤ Eq.rec (motive := fun (x : ι) (h : j = x) ↦ α x) b ⋯) →
    ∃ (h : k = j), Eq.rec (motive := fun (x : ι) (x_3 : k = x) ↦ α x) c ⋯ ≤ b
⊢ (∃ (x : j = k), c ≤ Eq.rec (motive := fun (x : ι) (h : j = x) ↦ α x) b ⋯) ↔
    ∃ (h : k = j), Eq.rec (motive := fun (x : ι) (x_3 : k = x) ↦ α x) c ⋯ ≤ b
have mpr : (∃ (h : k = j), Eq.rec (motive := fun (x : ι) (x_3 : k = x) ↦ α x) c sorry ≤ b) →
  ∃ (x : j = k), c ≤ Eq.rec (motive := fun (x : ι) (h : j = x) ↦ α x) b sorry
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Sigma.Interval (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : DecidableEq ι
inst_1 : (i : ι) → Preorder (α i)
inst_2 : (i : ι) → LocallyFiniteOrder (α i)
x x_1 x_2 : (i : ι) × α i
i : ι
a : α i
j : ι
b : α j
k : ι
c : α k
⊢ Membership.mem (γ := Finset ((i : ι) × α i))
      (sigmaLift (α := fun (i : ι) ↦ α i) (β := fun (i : ι) ↦ α i) (γ := fun (i : ι) ↦ α i) (fun (x : ι) ↦ Ioo)
        (mk (β := fun (i : ι) ↦ α i) i a) (mk (β := fun (i : ι) ↦ α i) j b))
      (mk (β := fun (i : ι) ↦ α i) k c) ↔
    mk (β := fun (i : ι) ↦ α i) i a < mk (β := fun (i : ι) ↦ α i) k c ∧
      mk (β := fun (i : ι) ↦ α i) k c < mk (β := fun (i : ι) ↦ α i) j b
have simp_rw : (∃ (h : i = k) (_ : Eq.rec (motive := fun (x : ι) (h : i = x) ↦ α x) a sorry < c) (x : j = k),
    c < Eq.rec (motive := fun (x : ι) (h : j = x) ↦ α x) b sorry) ↔
  ∃ (h : i = k) (_ : Eq.rec (motive := fun (x : ι) (x_3 : i = x) ↦ α x) a sorry < c) (h : k = j),
    Eq.rec (motive := fun (x : ι) (x_3 : k = x) ↦ α x) c sorry < b
Tactic: simp_rw [mem_sigmaLift, lt_def, mem_Ioo, exists_and_left, ← exists_and_right, ← exists_prop]