awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : ι) ↦ 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

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

Premises used: Sigma.lt_def, exists_and_left, Finset.mem_sigmaLift, exists_and_right, exists_prop, Finset.mem_Ioo
-- 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)
a b : (i : ι) × α i
⊢ #(Icc a b) =
    if h : a.fst (β := fun (i : ι) ↦ α i) = b.fst (β := fun (i : ι) ↦ α i) then
      card.{u_2} (α := α (b.fst (β := fun (i : ι) ↦ α i)))
        (Icc
            (Eq.rec (motive := fun (x : ι) (x_1 : a.fst (β := fun (i : ι) ↦ α i) = x) ↦ α x)
              (a.snd (β := fun (i : ι) ↦ α i)) h)
            (b.snd (β := fun (i : ι) ↦ α i)) :
          Finset (α (b.fst (β := fun (i : ι) ↦ α i))))
    else 0

Tactic:
card_sigmaLift (fun _ => Icc) _ _

Premises used: Finset.card_sigmaLift, Finset.Icc, dite, Finset.sigmaLift
-- Module: Mathlib.Data.Sigma.Interval
Goal:
ι : Type u_1
α : ι → Type u_2
inst : DecidableEq ι
inst_1 : (i : ι) → Preorder (α i)
inst_2 : (i : ι) → LocallyFiniteOrder (α i)
a b : (i : ι) × α i
⊢ #(Ico a b) =
    if h : a.fst (β := fun (i : ι) ↦ α i) = b.fst (β := fun (i : ι) ↦ α i) then
      card.{u_2} (α := α (b.fst (β := fun (i : ι) ↦ α i)))
        (Ico
            (Eq.rec (motive := fun (x : ι) (x_1 : a.fst (β := fun (i : ι) ↦ α i) = x) ↦ α x)
              (a.snd (β := fun (i : ι) ↦ α i)) h)
            (b.snd (β := fun (i : ι) ↦ α i)) :
          Finset (α (b.fst (β := fun (i : ι) ↦ α i))))
    else 0

Tactic:
card_sigmaLift (fun _ => Ico) _ _

Premises used: Finset.card_sigmaLift, Finset.Ico, dite, Finset.sigmaLift
-- Module: Mathlib.Data.Sigma.Interval
Goal:
ι : Type u_1
α : ι → Type u_2
inst : DecidableEq ι
inst_1 : (i : ι) → Preorder (α i)
inst_2 : (i : ι) → LocallyFiniteOrder (α i)
a b : (i : ι) × α i
⊢ #(Ioc a b) =
    if h : a.fst (β := fun (i : ι) ↦ α i) = b.fst (β := fun (i : ι) ↦ α i) then
      card.{u_2} (α := α (b.fst (β := fun (i : ι) ↦ α i)))
        (Ioc
            (Eq.rec (motive := fun (x : ι) (x_1 : a.fst (β := fun (i : ι) ↦ α i) = x) ↦ α x)
              (a.snd (β := fun (i : ι) ↦ α i)) h)
            (b.snd (β := fun (i : ι) ↦ α i)) :
          Finset (α (b.fst (β := fun (i : ι) ↦ α i))))
    else 0

Tactic:
card_sigmaLift (fun _ => Ioc) _ _

Premises used: Finset.card_sigmaLift, dite, Finset.sigmaLift, Finset.Ioc
-- Module: Mathlib.Data.Sigma.Interval
Goal:
ι : Type u_1
α : ι → Type u_2
inst : DecidableEq ι
inst_1 : (i : ι) → Preorder (α i)
inst_2 : (i : ι) → LocallyFiniteOrder (α i)
a b : (i : ι) × α i
⊢ #(Ioo a b) =
    if h : a.fst (β := fun (i : ι) ↦ α i) = b.fst (β := fun (i : ι) ↦ α i) then
      card.{u_2} (α := α (b.fst (β := fun (i : ι) ↦ α i)))
        (Ioo
            (Eq.rec (motive := fun (x : ι) (x_1 : a.fst (β := fun (i : ι) ↦ α i) = x) ↦ α x)
              (a.snd (β := fun (i : ι) ↦ α i)) h)
            (b.snd (β := fun (i : ι) ↦ α i)) :
          Finset (α (b.fst (β := fun (i : ι) ↦ α i))))
    else 0

Tactic:
card_sigmaLift (fun _ => Ioo) _ _

Premises used: Finset.card_sigmaLift, dite, Finset.sigmaLift, Finset.Ioo
-- Module: Mathlib.Data.Sigma.Interval
Goal:
ι : Type u_1
α : ι → Type u_2
inst : DecidableEq ι
inst_1 : (i : ι) → Preorder (α i)
inst_2 : (i : ι) → LocallyFiniteOrder (α i)
i : ι
a b : α i
⊢ Icc (mk (β := α) i a) (mk (β := α) i b) = Finset.map (Embedding.sigmaMk (β := α) i) (Icc a b)

Tactic:
dif_pos rfl

Premises used: dif_pos, Finset.Icc, dite, Finset.sigmaLift, 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)
i : ι
a b : α i
⊢ Ico (mk (β := α) i a) (mk (β := α) i b) = Finset.map (Embedding.sigmaMk (β := α) i) (Ico a b)

Tactic:
dif_pos rfl

Premises used: dif_pos, Finset.Ico, dite, Finset.sigmaLift, 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)
i : ι
a b : α i
⊢ Ioc (mk (β := α) i a) (mk (β := α) i b) = Finset.map (Embedding.sigmaMk (β := α) i) (Ioc a b)

Tactic:
dif_pos rfl

Premises used: dif_pos, dite, Finset.sigmaLift, rfl, Finset.Ioc
-- Module: Mathlib.Data.Sigma.Interval
Goal:
ι : Type u_1
α : ι → Type u_2
inst : DecidableEq ι
inst_1 : (i : ι) → Preorder (α i)
inst_2 : (i : ι) → LocallyFiniteOrder (α i)
i : ι
a b : α i
⊢ Ioo (mk (β := α) i a) (mk (β := α) i b) = Finset.map (Embedding.sigmaMk (β := α) i) (Ioo a b)

Tactic:
dif_pos rfl

Premises used: dif_pos, dite, Finset.sigmaLift, Finset.Ioo, rfl
-- Module: Mathlib.Data.Sigma.Interval
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → Preorder (α i)
inst_1 : (i : ι) → LocallyFiniteOrderBot (α i)
x x_1 : (i : ι) × α i
i : ι
a : α i
j : ι
b : α j
inl :
  ∀ (b : α i),
    Membership.mem (γ := Finset ((i : ι) × α i))
        (match (motive := (i : ι) × α i → Finset ((i : ι) × α i)) mk (β := fun (i : ι) ↦ α i) i a with
          | ⟨i, a⟩ => Finset.map (Embedding.sigmaMk (β := α) i) (Iic a) :
          Finset ((i : ι) × α i))
        (mk (β := fun (i : ι) ↦ α i) i b) ↔
      mk (β := fun (i : ι) ↦ α i) i b ≤ mk (β := fun (i : ι) ↦ α i) i a
inr :
  ∀ (hij : i ≠ j),
    Membership.mem (γ := Finset ((i : ι) × α i))
        (match (motive := (i : ι) × α i → Finset ((i : ι) × α i)) mk (β := fun (i : ι) ↦ α i) i a with
          | ⟨i, a⟩ => Finset.map (Embedding.sigmaMk (β := α) i) (Iic a) :
          Finset ((i : ι) × α i))
        (mk (β := fun (i : ι) ↦ α i) j b) ↔
      mk (β := fun (i : ι) ↦ α i) j b ≤ mk (β := fun (i : ι) ↦ α i) i a
⊢ Membership.mem (γ := Finset ((i : ι) × α i))
      (match (motive := (i : ι) × α i → Finset ((i : ι) × α i)) mk (β := fun (i : ι) ↦ α i) i a with
        | ⟨i, a⟩ => Finset.map (Embedding.sigmaMk (β := α) i) (Iic a) :
        Finset ((i : ι) × α i))
      (mk (β := fun (i : ι) ↦ α i) j b) ↔
    mk (β := fun (i : ι) ↦ α i) j b ≤ mk (β := fun (i : ι) ↦ α i) i a

Tactic:
obtain rfl | hij := eq_or_ne i j

Premises used: eq_or_ne, rfl
-- Module: Mathlib.Data.Sigma.Interval
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → Preorder (α i)
inst_1 : (i : ι) → LocallyFiniteOrderBot (α i)
x x_1 : (i : ι) × α i
i : ι
a b : α i
⊢ Membership.mem (γ := Finset ((i : ι) × α i))
      (match (motive := (i : ι) × α i → Finset ((i : ι) × α i)) mk (β := fun (i : ι) ↦ α i) i a with
        | ⟨i, a⟩ => Finset.map (Embedding.sigmaMk (β := α) i) (Iic a) :
        Finset ((i : ι) × α i))
      (mk (β := fun (i : ι) ↦ α i) i b) ↔
    mk (β := fun (i : ι) ↦ α i) i b ≤ mk (β := fun (i : ι) ↦ α i) i a

Tactic:
simp
-- Module: Mathlib.Data.Sigma.Interval
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → Preorder (α i)
inst_1 : (i : ι) → LocallyFiniteOrderBot (α i)
x x_1 : (i : ι) × α i
i : ι
a : α i
j : ι
b : α j
hij : i ≠ j
⊢ Membership.mem (γ := Finset ((i : ι) × α i))
      (match (motive := (i : ι) × α i → Finset ((i : ι) × α i)) mk (β := fun (i : ι) ↦ α i) i a with
        | ⟨i, a⟩ => Finset.map (Embedding.sigmaMk (β := α) i) (Iic a) :
        Finset ((i : ι) × α i))
      (mk (β := fun (i : ι) ↦ α i) j b) ↔
    mk (β := fun (i : ι) ↦ α i) j b ≤ mk (β := fun (i : ι) ↦ α i) i a

Tactic:
simp [hij, le_def, hij.symm]

Premises used: Sigma.le_def, Ne.symm
-- Module: Mathlib.Data.Sigma.Interval
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → Preorder (α i)
inst_1 : (i : ι) → LocallyFiniteOrderBot (α i)
x x_1 : (i : ι) × α i
i : ι
a : α i
j : ι
b : α j
inl :
  ∀ (b : α i),
    Membership.mem (γ := Finset ((i : ι) × α i))
        (match (motive := (i : ι) × α i → Finset ((i : ι) × α i)) mk (β := fun (i : ι) ↦ α i) i a with
          | ⟨i, a⟩ => Finset.map (Embedding.sigmaMk (β := α) i) (Iio a) :
          Finset ((i : ι) × α i))
        (mk (β := fun (i : ι) ↦ α i) i b) ↔
      mk (β := fun (i : ι) ↦ α i) i b < mk (β := fun (i : ι) ↦ α i) i a
inr :
  ∀ (hij : i ≠ j),
    Membership.mem (γ := Finset ((i : ι) × α i))
        (match (motive := (i : ι) × α i → Finset ((i : ι) × α i)) mk (β := fun (i : ι) ↦ α i) i a with
          | ⟨i, a⟩ => Finset.map (Embedding.sigmaMk (β := α) i) (Iio a) :
          Finset ((i : ι) × α i))
        (mk (β := fun (i : ι) ↦ α i) j b) ↔
      mk (β := fun (i : ι) ↦ α i) j b < mk (β := fun (i : ι) ↦ α i) i a
⊢ Membership.mem (γ := Finset ((i : ι) × α i))
      (match (motive := (i : ι) × α i → Finset ((i : ι) × α i)) mk (β := fun (i : ι) ↦ α i) i a with
        | ⟨i, a⟩ => Finset.map (Embedding.sigmaMk (β := α) i) (Iio a) :
        Finset ((i : ι) × α i))
      (mk (β := fun (i : ι) ↦ α i) j b) ↔
    mk (β := fun (i : ι) ↦ α i) j b < mk (β := fun (i : ι) ↦ α i) i a

Tactic:
obtain rfl | hij := eq_or_ne i j

Premises used: eq_or_ne, rfl
-- Module: Mathlib.Data.Sigma.Interval
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → Preorder (α i)
inst_1 : (i : ι) → LocallyFiniteOrderBot (α i)
x x_1 : (i : ι) × α i
i : ι
a b : α i
⊢ Membership.mem (γ := Finset ((i : ι) × α i))
      (match (motive := (i : ι) × α i → Finset ((i : ι) × α i)) mk (β := fun (i : ι) ↦ α i) i a with
        | ⟨i, a⟩ => Finset.map (Embedding.sigmaMk (β := α) i) (Iio a) :
        Finset ((i : ι) × α i))
      (mk (β := fun (i : ι) ↦ α i) i b) ↔
    mk (β := fun (i : ι) ↦ α i) i b < mk (β := fun (i : ι) ↦ α i) i a

Tactic:
simp
-- Module: Mathlib.Data.Sigma.Interval
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → Preorder (α i)
inst_1 : (i : ι) → LocallyFiniteOrderBot (α i)
x x_1 : (i : ι) × α i
i : ι
a : α i
j : ι
b : α j
hij : i ≠ j
⊢ Membership.mem (γ := Finset ((i : ι) × α i))
      (match (motive := (i : ι) × α i → Finset ((i : ι) × α i)) mk (β := fun (i : ι) ↦ α i) i a with
        | ⟨i, a⟩ => Finset.map (Embedding.sigmaMk (β := α) i) (Iio a) :
        Finset ((i : ι) × α i))
      (mk (β := fun (i : ι) ↦ α i) j b) ↔
    mk (β := fun (i : ι) ↦ α i) j b < mk (β := fun (i : ι) ↦ α i) i a

Tactic:
simp [hij, lt_def, hij.symm]

Premises used: Sigma.lt_def, Ne.symm
-- Module: Mathlib.Data.Sigma.Interval
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → Preorder (α i)
inst_1 : (i : ι) → LocallyFiniteOrderBot (α i)
i : ι
a : α i
⊢ Iic (mk (β := α) i a) = Finset.map (Embedding.sigmaMk (β := α) i) (Iic a)

Tactic:
rfl

Premises used: Finset.map, Finset.Iic, rfl
-- Module: Mathlib.Data.Sigma.Interval
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → Preorder (α i)
inst_1 : (i : ι) → LocallyFiniteOrderBot (α i)
i : ι
a : α i
⊢ Iio (mk (β := α) i a) = Finset.map (Embedding.sigmaMk (β := α) i) (Iio a)

Tactic:
rfl

Premises used: Finset.Iio, Finset.map, rfl
-- Module: Mathlib.Data.Sigma.Interval
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → Preorder (α i)
inst_1 : (i : ι) → LocallyFiniteOrderTop (α i)
x x_1 : (i : ι) × α i
i : ι
a : α i
j : ι
b : α j
inl :
  ∀ (b : α i),
    Membership.mem (γ := Finset ((i : ι) × α i))
        (match (motive := (i : ι) × α i → Finset ((i : ι) × α i)) mk (β := fun (i : ι) ↦ α i) i a with
          | ⟨i, a⟩ => Finset.map (Embedding.sigmaMk (β := α) i) (Ici a) :
          Finset ((i : ι) × α i))
        (mk (β := fun (i : ι) ↦ α i) i b) ↔
      mk (β := fun (i : ι) ↦ α i) i a ≤ mk (β := fun (i : ι) ↦ α i) i b
inr :
  ∀ (hij : i ≠ j),
    Membership.mem (γ := Finset ((i : ι) × α i))
        (match (motive := (i : ι) × α i → Finset ((i : ι) × α i)) mk (β := fun (i : ι) ↦ α i) i a with
          | ⟨i, a⟩ => Finset.map (Embedding.sigmaMk (β := α) i) (Ici a) :
          Finset ((i : ι) × α i))
        (mk (β := fun (i : ι) ↦ α i) j b) ↔
      mk (β := fun (i : ι) ↦ α i) i a ≤ mk (β := fun (i : ι) ↦ α i) j b
⊢ Membership.mem (γ := Finset ((i : ι) × α i))
      (match (motive := (i : ι) × α i → Finset ((i : ι) × α i)) mk (β := fun (i : ι) ↦ α i) i a with
        | ⟨i, a⟩ => Finset.map (Embedding.sigmaMk (β := α) i) (Ici a) :
        Finset ((i : ι) × α i))
      (mk (β := fun (i : ι) ↦ α i) j b) ↔
    mk (β := fun (i : ι) ↦ α i) i a ≤ mk (β := fun (i : ι) ↦ α i) j b

Tactic:
obtain rfl | hij := eq_or_ne i j

Premises used: eq_or_ne, rfl
-- Module: Mathlib.Data.Sigma.Interval
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → Preorder (α i)
inst_1 : (i : ι) → LocallyFiniteOrderTop (α i)
x x_1 : (i : ι) × α i
i : ι
a b : α i
⊢ Membership.mem (γ := Finset ((i : ι) × α i))
      (match (motive := (i : ι) × α i → Finset ((i : ι) × α i)) mk (β := fun (i : ι) ↦ α i) i a with
        | ⟨i, a⟩ => Finset.map (Embedding.sigmaMk (β := α) i) (Ici a) :
        Finset ((i : ι) × α i))
      (mk (β := fun (i : ι) ↦ α i) i b) ↔
    mk (β := fun (i : ι) ↦ α i) i a ≤ mk (β := fun (i : ι) ↦ α i) i b

Tactic:
simp
-- Module: Mathlib.Data.Sigma.Interval
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → Preorder (α i)
inst_1 : (i : ι) → LocallyFiniteOrderTop (α i)
x x_1 : (i : ι) × α i
i : ι
a : α i
j : ι
b : α j
hij : i ≠ j
⊢ Membership.mem (γ := Finset ((i : ι) × α i))
      (match (motive := (i : ι) × α i → Finset ((i : ι) × α i)) mk (β := fun (i : ι) ↦ α i) i a with
        | ⟨i, a⟩ => Finset.map (Embedding.sigmaMk (β := α) i) (Ici a) :
        Finset ((i : ι) × α i))
      (mk (β := fun (i : ι) ↦ α i) j b) ↔
    mk (β := fun (i : ι) ↦ α i) i a ≤ mk (β := fun (i : ι) ↦ α i) j b

Tactic:
simp [hij, le_def]

Premises used: Sigma.le_def
-- Module: Mathlib.Data.Sigma.Interval
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → Preorder (α i)
inst_1 : (i : ι) → LocallyFiniteOrderTop (α i)
x x_1 : (i : ι) × α i
i : ι
a : α i
j : ι
b : α j
inl :
  ∀ (b : α i),
    Membership.mem (γ := Finset ((i : ι) × α i))
        (match (motive := (i : ι) × α i → Finset ((i : ι) × α i)) mk (β := fun (i : ι) ↦ α i) i a with
          | ⟨i, a⟩ => Finset.map (Embedding.sigmaMk (β := α) i) (Ioi a) :
          Finset ((i : ι) × α i))
        (mk (β := fun (i : ι) ↦ α i) i b) ↔
      mk (β := fun (i : ι) ↦ α i) i a < mk (β := fun (i : ι) ↦ α i) i b
inr :
  ∀ (hij : i ≠ j),
    Membership.mem (γ := Finset ((i : ι) × α i))
        (match (motive := (i : ι) × α i → Finset ((i : ι) × α i)) mk (β := fun (i : ι) ↦ α i) i a with
          | ⟨i, a⟩ => Finset.map (Embedding.sigmaMk (β := α) i) (Ioi a) :
          Finset ((i : ι) × α i))
        (mk (β := fun (i : ι) ↦ α i) j b) ↔
      mk (β := fun (i : ι) ↦ α i) i a < mk (β := fun (i : ι) ↦ α i) j b
⊢ Membership.mem (γ := Finset ((i : ι) × α i))
      (match (motive := (i : ι) × α i → Finset ((i : ι) × α i)) mk (β := fun (i : ι) ↦ α i) i a with
        | ⟨i, a⟩ => Finset.map (Embedding.sigmaMk (β := α) i) (Ioi a) :
        Finset ((i : ι) × α i))
      (mk (β := fun (i : ι) ↦ α i) j b) ↔
    mk (β := fun (i : ι) ↦ α i) i a < mk (β := fun (i : ι) ↦ α i) j b

Tactic:
obtain rfl | hij := eq_or_ne i j

Premises used: eq_or_ne, rfl
-- Module: Mathlib.Data.Sigma.Interval
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → Preorder (α i)
inst_1 : (i : ι) → LocallyFiniteOrderTop (α i)
x x_1 : (i : ι) × α i
i : ι
a b : α i
⊢ Membership.mem (γ := Finset ((i : ι) × α i))
      (match (motive := (i : ι) × α i → Finset ((i : ι) × α i)) mk (β := fun (i : ι) ↦ α i) i a with
        | ⟨i, a⟩ => Finset.map (Embedding.sigmaMk (β := α) i) (Ioi a) :
        Finset ((i : ι) × α i))
      (mk (β := fun (i : ι) ↦ α i) i b) ↔
    mk (β := fun (i : ι) ↦ α i) i a < mk (β := fun (i : ι) ↦ α i) i b

Tactic:
simp
-- Module: Mathlib.Data.Sigma.Interval
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → Preorder (α i)
inst_1 : (i : ι) → LocallyFiniteOrderTop (α i)
x x_1 : (i : ι) × α i
i : ι
a : α i
j : ι
b : α j
hij : i ≠ j
⊢ Membership.mem (γ := Finset ((i : ι) × α i))
      (match (motive := (i : ι) × α i → Finset ((i : ι) × α i)) mk (β := fun (i : ι) ↦ α i) i a with
        | ⟨i, a⟩ => Finset.map (Embedding.sigmaMk (β := α) i) (Ioi a) :
        Finset ((i : ι) × α i))
      (mk (β := fun (i : ι) ↦ α i) j b) ↔
    mk (β := fun (i : ι) ↦ α i) i a < mk (β := fun (i : ι) ↦ α i) j b

Tactic:
simp [hij, lt_def]

Premises used: Sigma.lt_def
-- Module: Mathlib.Data.Sigma.Interval
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → Preorder (α i)
inst_1 : (i : ι) → LocallyFiniteOrderTop (α i)
i : ι
a : α i
⊢ Ici (mk (β := α) i a) = Finset.map (Embedding.sigmaMk (β := α) i) (Ici a)

Tactic:
rfl

Premises used: Finset.map, Finset.Ici, rfl
-- Module: Mathlib.Data.Sigma.Interval
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → Preorder (α i)
inst_1 : (i : ι) → LocallyFiniteOrderTop (α i)
i : ι
a : α i
⊢ Ioi (mk (β := α) i a) = Finset.map (Embedding.sigmaMk (β := α) i) (Ioi a)

Tactic:
rfl

Premises used: Finset.Ioi, Finset.map, rfl