awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Sigma.Basic
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
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)
⊢ 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:
unfold Sigma.curry

Premises used: Sigma.curry
-- Module: Mathlib.Data.Sigma.Basic
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))
⊢ 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:
simp
-- Module: Mathlib.Data.Sigma.Basic
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
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
⊢ 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:
simp only [update_self]

Premises used: Function.update_self
-- Module: Mathlib.Data.Sigma.Basic
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
rw : mk (β := fun (a : α) ↦ β a) ia jb = mk (β := fun (a : α) ↦ β a) ia ib → jb = 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 jb) =
    update (β := γ ia) (fun (y : β ia) ↦ f (mk (β := fun (a : α) ↦ β a) ia y)) ib x jb

Tactic:
rw [Function.update_of_ne (mt _ hb.symm), Function.update_of_ne hb.symm]

Premises used: mt, Ne.symm, Function.update_of_ne
-- Module: Mathlib.Data.Sigma.Basic
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
h : mk (β := fun (a : α) ↦ β a) ia jb = mk (β := fun (a : α) ↦ β a) ia ib
⊢ jb = ib

Tactic:
injection h
-- Module: Mathlib.Data.Sigma.Basic
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)
rw :
  (mk (β := fun (a : α) ↦ β a) ja jb).fst (β := fun (a : α) ↦ β a) ≠
    (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)

Tactic:
rw [Function.update_of_ne (ne_of_apply_ne Sigma.fst _), Function.update_of_ne]

Premises used: Sigma.fst, ne_of_apply_ne, Function.update_of_ne
-- Module: Mathlib.Data.Sigma.Basic
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
⊢ ja ≠ (mk (β := fun (a : α) ↦ β a) ia ib).fst (β := fun (a : α) ↦ β a)

Tactic:
ha.symm

Premises used: Ne.symm
-- Module: Mathlib.Data.Sigma.Basic
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
⊢ ja ≠ (mk (β := fun (a : α) ↦ β a) ia ib).fst (β := fun (a : α) ↦ β a)

Tactic:
exact ha.symm

Premises used: Ne.symm
-- Module: Mathlib.Data.Sigma.Basic
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
⊢ (mk (β := fun (a : α) ↦ β a) ja jb).fst (β := fun (a : α) ↦ β a) ≠
    (mk (β := fun (a : α) ↦ β a) ia ib).fst (β := fun (a : α) ↦ β a)

Tactic:
ha.symm

Premises used: Ne.symm
-- Module: Mathlib.Data.Sigma.Basic
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
⊢ (mk (β := fun (a : α) ↦ β a) ja jb).fst (β := fun (a : α) ↦ β a) ≠
    (mk (β := fun (a : α) ↦ β a) ia ib).fst (β := fun (a : α) ↦ β a)

Tactic:
exact ha.symm

Premises used: Ne.symm
-- Module: Mathlib.Data.Sigma.Basic
Goal:
α : Type u_7
β : Type u_8
⊢ Eq (α := α × β → α) (Sigma.fst (β := fun (x : α) ↦ β) ∘ toSigma) fst

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Sigma.Basic
Goal:
α : Type u_7
β : Type u_8
x : α × β
⊢ x.toSigma.fst (β := fun (x : α) ↦ β) = x.fst

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Sigma.Basic
Goal:
α : Type u_7
β : Type u_8
x : α × β
⊢ x.toSigma.snd (β := fun (x : α) ↦ β) = x.snd

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Sigma.Basic
Goal:
α : Type u_7
β : Type u_8
x : α
y : β
⊢ (x, y).toSigma = Sigma.mk (β := fun (x : α) ↦ β) x y

Tactic:
rfl

Premises used: Prod.toSigma, rfl
-- Module: Mathlib.Data.Sigma.Basic
Goal:
α : Type u_7
β : Type u_8
a : α
b : β
c : α
d : β
h : (a, b).toSigma = (c, d).toSigma
⊢ (a, b) = (c, d)

Tactic:
simp_all
-- Module: Mathlib.Data.Sigma.Basic
Goal:
α : Type u_7
β : Type u_8
x y : α × β
⊢ x.toSigma = y.toSigma ↔ x = y

Tactic:
Prod.toSigma_injective.eq_iff

Premises used: Prod.toSigma_injective, Function.Injective.eq_iff
-- Module: Mathlib.Data.Sigma.Basic
Goal:
α : Sort u_1
β : α → Sort u_2
γ : Sort u_3
f : (a : α) → β a → γ
a : α
b : β a
⊢ elim (β := β) f (mk (β := β) a b) = f a b

Tactic:
rfl

Premises used: PSigma.elim, rfl
-- Module: Mathlib.Data.Sigma.Basic
Goal:
α : Sort u_1
β : α → Sort u_2
a₁ a₂ : α
b₁ : β a₁
b₂ : β a₂
⊢ mk (β := β) a₁ b₁ = mk (β := β) a₂ b₂ ↔ a₁ = a₂ ∧ b₁ ≍ b₂

Tactic:
(Iff.intro PSigma.mk.inj) fun ⟨h₁, h₂⟩ ↦
    match a₁, a₂, b₁, b₂, h₁, h₂ with
    | _, _, _, _, Eq.refl _, HEq.refl _ => rfl

Premises used: _private.0.PSigma.mk.inj_iff.match_1, _private.0.PSigma.mk.inj_iff.match_2, PSigma.mk.inj, Iff.intro, PSigma.mk, Eq, rfl
-- Module: Mathlib.Data.Sigma.Basic
Goal:
α : Sort u_1
β : α → Sort u_2
p : (a : α) ×' β a → Prop
⊢ (∀ (x : (a : α) ×' β a), p x) ↔ ∀ (a : α) (b : β a), p (mk (β := fun (a : α) ↦ β a) a b)

Tactic:
⟨fun h a b ↦ h ⟨a, b⟩, fun h ⟨a, b⟩ ↦ h a b⟩

Premises used: _private.0.PSigma.forall.match_1, Iff.intro, PSigma.mk
-- Module: Mathlib.Data.Sigma.Basic
Goal:
α : Sort u_1
β : α → Sort u_2
p : (a : α) ×' β a → Prop
⊢ (∃ (x : (a : α) ×' β a), p x) ↔ ∃ (a : α), ∃ (b : β a), p (mk (β := fun (a : α) ↦ β a) a b)

Tactic:
⟨fun ⟨⟨a, b⟩, h⟩ ↦ ⟨a, b, h⟩, fun ⟨a, b, h⟩ ↦ ⟨⟨a, b⟩, h⟩⟩

Premises used: Exists, _private.0.PSigma.exists.match_2, Iff.intro, Exists.intro, PSigma.mk, _private.0.PSigma.exists.match_1
-- Module: Mathlib.Data.Sigma.Interval
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
simp_rw :
  (∃ (h : i = k) (_ : 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 : i = k) (_ : Eq.rec (motive := fun (x : ι) (x_3 : i = x) ↦ α x) a ⋯ ≤ c) (h : k = j),
      Eq.rec (motive := fun (x : ι) (x_3 : k = x) ↦ α x) c ⋯ ≤ b
⊢ 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

Tactic:
simp_rw [mem_sigmaLift, le_def, mem_Icc, exists_and_left, ← exists_and_right, ← exists_prop]

Premises used: Sigma.le_def, Finset.mem_Icc, exists_and_left, Finset.mem_sigmaLift, exists_and_right, exists_prop
-- Module: Mathlib.Data.Sigma.Interval
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
mpr :
  (∃ (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 ⋯
⊢ (∃ (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

Tactic:
constructor
-- Module: Mathlib.Data.Sigma.Interval
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 c : α j
h : i = j
h_1 : Eq.rec (motive := fun (x : ι) (h : i = x) ↦ α x) a ⋯ ≤ c
ht : c ≤ Eq.rec (motive := fun (x : ι) (h : j = x) ↦ α x) b ⋯
⊢ ∃ (h : j = j), Eq.rec (motive := fun (x : ι) (x_3 : j = x) ↦ α x) c ⋯ ≤ b

Tactic:
⟨rfl, ht⟩

Premises used: Exists.intro, rfl
-- Module: Mathlib.Data.Sigma.Interval
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 c : α j
h : i = j
h_1 : Eq.rec (motive := fun (x : ι) (h : i = x) ↦ α x) a ⋯ ≤ c
ht : c ≤ Eq.rec (motive := fun (x : ι) (h : j = x) ↦ α x) b ⋯
⊢ ∃ (h : j = j), Eq.rec (motive := fun (x : ι) (x_3 : j = x) ↦ α x) c ⋯ ≤ b

Tactic:
exact ⟨rfl, ht⟩
-- Module: Mathlib.Data.Sigma.Interval
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 c : α j
h : i = j
h_1 : Eq.rec (motive := fun (x : ι) (h : i = x) ↦ α x) a ⋯ ≤ c
ht : Eq.rec (motive := fun (x : ι) (x_3 : j = x) ↦ α x) c ⋯ ≤ b
⊢ ∃ (x : j = j), c ≤ Eq.rec (motive := fun (x : ι) (h : j = x) ↦ α x) b ⋯

Tactic:
⟨rfl, ht⟩

Premises used: Exists.intro, rfl
-- Module: Mathlib.Data.Sigma.Interval
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 c : α j
h : i = j
h_1 : Eq.rec (motive := fun (x : ι) (h : i = x) ↦ α x) a ⋯ ≤ c
ht : Eq.rec (motive := fun (x : ι) (x_3 : j = x) ↦ α x) c ⋯ ≤ b
⊢ ∃ (x : j = j), c ≤ Eq.rec (motive := fun (x : ι) (h : j = x) ↦ α x) b ⋯

Tactic:
exact ⟨rfl, ht⟩
-- Module: Mathlib.Data.Sigma.Interval
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) (_ : 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 : i = k) (_ : Eq.rec (motive := fun (x : ι) (x_3 : i = x) ↦ α x) a ⋯ ≤ c) (h : k = j),
      Eq.rec (motive := fun (x : ι) (x_3 : k = x) ↦ α x) c ⋯ ≤ b

Tactic:
exact exists₂_congr fun _ _ => by constructor <;> rintro ⟨⟨⟩, ht⟩ <;> exact ⟨rfl, ht⟩

Premises used: exists₂_congr
-- Module: Mathlib.Data.Sigma.Interval
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
simp_rw :
  (∃ (h : i = k) (_ : 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 : i = k) (_ : Eq.rec (motive := fun (x : ι) (x_3 : i = x) ↦ α x) a ⋯ ≤ c) (h : k = j),
      Eq.rec (motive := fun (x : ι) (x_3 : k = x) ↦ α x) c ⋯ < b
⊢ 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

Tactic:
simp_rw [mem_sigmaLift, le_def, lt_def, mem_Ico, exists_and_left, ← exists_and_right, ←
      exists_prop]

Premises used: Sigma.le_def, Sigma.lt_def, exists_and_left, Finset.mem_sigmaLift, exists_and_right, exists_prop, Finset.mem_Ico
-- Module: Mathlib.Data.Sigma.Interval
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
mpr :
  (∃ (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 ⋯
⊢ (∃ (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

Tactic:
constructor
-- Module: Mathlib.Data.Sigma.Interval
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 c : α j
h : i = j
h_1 : Eq.rec (motive := fun (x : ι) (h : i = x) ↦ α x) a ⋯ ≤ c
ht : c < Eq.rec (motive := fun (x : ι) (h : j = x) ↦ α x) b ⋯
⊢ ∃ (h : j = j), Eq.rec (motive := fun (x : ι) (x_3 : j = x) ↦ α x) c ⋯ < b

Tactic:
⟨rfl, ht⟩

Premises used: Exists.intro, rfl
-- Module: Mathlib.Data.Sigma.Interval
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 c : α j
h : i = j
h_1 : Eq.rec (motive := fun (x : ι) (h : i = x) ↦ α x) a ⋯ ≤ c
ht : c < Eq.rec (motive := fun (x : ι) (h : j = x) ↦ α x) b ⋯
⊢ ∃ (h : j = j), Eq.rec (motive := fun (x : ι) (x_3 : j = x) ↦ α x) c ⋯ < b

Tactic:
exact ⟨rfl, ht⟩
-- Module: Mathlib.Data.Sigma.Interval
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 c : α j
h : i = j
h_1 : Eq.rec (motive := fun (x : ι) (h : i = x) ↦ α x) a ⋯ ≤ c
ht : Eq.rec (motive := fun (x : ι) (x_3 : j = x) ↦ α x) c ⋯ < b
⊢ ∃ (x : j = j), c < Eq.rec (motive := fun (x : ι) (h : j = x) ↦ α x) b ⋯

Tactic:
⟨rfl, ht⟩

Premises used: Exists.intro, rfl
-- Module: Mathlib.Data.Sigma.Interval
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 c : α j
h : i = j
h_1 : Eq.rec (motive := fun (x : ι) (h : i = x) ↦ α x) a ⋯ ≤ c
ht : Eq.rec (motive := fun (x : ι) (x_3 : j = x) ↦ α x) c ⋯ < b
⊢ ∃ (x : j = j), c < Eq.rec (motive := fun (x : ι) (h : j = x) ↦ α x) b ⋯

Tactic:
exact ⟨rfl, ht⟩
-- Module: Mathlib.Data.Sigma.Interval
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) (_ : 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 : i = k) (_ : Eq.rec (motive := fun (x : ι) (x_3 : i = x) ↦ α x) a ⋯ ≤ c) (h : k = j),
      Eq.rec (motive := fun (x : ι) (x_3 : k = x) ↦ α x) c ⋯ < b

Tactic:
exact exists₂_congr fun _ _ => by constructor <;> rintro ⟨⟨⟩, ht⟩ <;> exact ⟨rfl, ht⟩

Premises used: exists₂_congr
-- Module: Mathlib.Data.Sigma.Interval
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
simp_rw :
  (∃ (h : i = k) (_ : 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 : i = k) (_ : Eq.rec (motive := fun (x : ι) (x_3 : i = x) ↦ α x) a ⋯ < c) (h : k = j),
      Eq.rec (motive := fun (x : ι) (x_3 : k = x) ↦ α x) c ⋯ ≤ b
⊢ 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

Tactic:
simp_rw [mem_sigmaLift, le_def, lt_def, mem_Ioc, exists_and_left, ← exists_and_right, ←
      exists_prop]

Premises used: Sigma.le_def, Sigma.lt_def, exists_and_left, Finset.mem_sigmaLift, exists_and_right, exists_prop, Finset.mem_Ioc