awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.Interval.Finset.Fin
Goal:
n : ℕ
i : Fin n
⊢ map (Equiv.toEmbedding revPerm) (Iic i) = Ici i.rev

Tactic:
simp [← coe_inj]

Premises used: Finset.coe_inj
-- Module: Mathlib.Order.Interval.Finset.Fin
Goal:
n : ℕ
i : Fin n
⊢ map (Equiv.toEmbedding revPerm) (Iio i) = Ioi i.rev

Tactic:
simp [← coe_inj]

Premises used: Finset.coe_inj
-- Module: Mathlib.Order.Interval.Finset.Fin
Goal:
n : ℕ
a b : Fin n
rw : #(Icc a b) = #(Icc (↑a : ℕ) (↑b : ℕ))
rw₁ : #(Icc a b) = #(map valEmbedding (Icc a b))
rw₂ rw₃ : #(Icc a b) = #(Icc a b)
⊢ #(Icc a b) = (↑b : ℕ) + 1 - (↑a : ℕ)

Tactic:
rw [← Nat.card_Icc, ← map_valEmbedding_Icc, card_map]

Premises used: Finset.card_map, Nat.card_Icc, Fin.map_valEmbedding_Icc
-- Module: Mathlib.Order.Interval.Finset.Fin
Goal:
n : ℕ
a b : Fin n
rw : #(Ico a b) = #(Ico (↑a : ℕ) (↑b : ℕ))
rw₁ : #(Ico a b) = #(map valEmbedding (Ico a b))
rw₂ rw₃ : #(Ico a b) = #(Ico a b)
⊢ #(Ico a b) = (↑b : ℕ) - (↑a : ℕ)

Tactic:
rw [← Nat.card_Ico, ← map_valEmbedding_Ico, card_map]

Premises used: Finset.card_map, Nat.card_Ico, Fin.map_valEmbedding_Ico
-- Module: Mathlib.Order.Interval.Finset.Fin
Goal:
n : ℕ
a b : Fin n
rw : #(Ioc a b) = #(Ioc (↑a : ℕ) (↑b : ℕ))
rw₁ : #(Ioc a b) = #(map valEmbedding (Ioc a b))
rw₂ rw₃ : #(Ioc a b) = #(Ioc a b)
⊢ #(Ioc a b) = (↑b : ℕ) - (↑a : ℕ)

Tactic:
rw [← Nat.card_Ioc, ← map_valEmbedding_Ioc, card_map]

Premises used: Finset.card_map, Nat.card_Ioc, Fin.map_valEmbedding_Ioc
-- Module: Mathlib.Order.Interval.Finset.Fin
Goal:
n : ℕ
a b : Fin n
rw : #(Ioo a b) = #(Ioo (↑a : ℕ) (↑b : ℕ))
rw₁ : #(Ioo a b) = #(map valEmbedding (Ioo a b))
rw₂ rw₃ : #(Ioo a b) = #(Ioo a b)
⊢ #(Ioo a b) = (↑b : ℕ) - (↑a : ℕ) - 1

Tactic:
rw [← Nat.card_Ioo, ← map_valEmbedding_Ioo, card_map]

Premises used: Finset.card_map, Nat.card_Ioo, Fin.map_valEmbedding_Ioo
-- Module: Mathlib.Order.Interval.Finset.Fin
Goal:
n : ℕ
a b : Fin n
rw : #(uIcc a b) = #(uIcc (↑a : ℕ) (↑b : ℕ))
rw₁ : #(uIcc a b) = #(map valEmbedding (uIcc a b))
rw₂ rw₃ : #(uIcc a b) = #(uIcc a b)
⊢ #(uIcc a b) = (HSub.hSub (α := ℤ) (↑(↑b : ℕ) : ℤ) (↑(↑a : ℕ) : ℤ)).natAbs + 1

Tactic:
rw [← Nat.card_uIcc, ← map_valEmbedding_uIcc, card_map]

Premises used: Fin.map_valEmbedding_uIcc, Finset.card_map, Nat.card_uIcc
-- Module: Mathlib.Order.Interval.Finset.Fin
Goal:
n : ℕ
a : Fin n
rw : card (α := Fin n) ((Ico (↑a : ℕ) n).attachFin ⋯) = n - (↑a : ℕ)
rw₁ : #(Ico (↑a : ℕ) n) = n - (↑a : ℕ)
rw₂ rw₃ : n - (↑a : ℕ) = n - (↑a : ℕ)
⊢ #(Ici a) = n - (↑a : ℕ)

Tactic:
rw [← attachFin_Ico_eq_Ici, card_attachFin, Nat.card_Ico]

Premises used: Fin.attachFin_Ico_eq_Ici, Finset.card_attachFin, Nat.card_Ico
-- Module: Mathlib.Order.Interval.Finset.Fin
Goal:
n : ℕ
a : Fin n
rw : #(map valEmbedding (Ioi a)) = n - 1 - (↑a : ℕ)
rw₁ : Fin n ↪ ℕ
rw₂ : Type
rw₃ : #(Ioo (↑a : ℕ) n) = n - 1 - (↑a : ℕ)
rw₄ : n - (↑a : ℕ) - 1 = n - 1 - (↑a : ℕ)
rw₅ rw₆ : n - 1 - (↑a : ℕ) = n - 1 - (↑a : ℕ)
⊢ #(Ioi a) = n - 1 - (↑a : ℕ)

Tactic:
rw [← card_map, map_valEmbedding_Ioi, Nat.card_Ioo, Nat.sub_right_comm]

Premises used: Finset.card_map, Nat.card_Ioo, Fin.map_valEmbedding_Ioi, Nat.sub_right_comm
-- Module: Mathlib.Order.Interval.Finset.Fin
Goal:
n : ℕ
b : Fin n
rw : #(Iic b) = #(Iic (↑b : ℕ))
rw₁ : #(Iic b) = #(map valEmbedding (Iic b))
rw₂ rw₃ : #(Iic b) = #(Iic b)
⊢ #(Iic b) = (↑b : ℕ) + 1

Tactic:
rw [← Nat.card_Iic b, ← map_valEmbedding_Iic, card_map]

Premises used: Finset.card_map, Nat.card_Iic, Fin.val, Fin.map_valEmbedding_Iic
-- Module: Mathlib.Order.Interval.Finset.Fin
Goal:
n : ℕ
b : Fin n
rw : #(Iio b) = #(Iio (↑b : ℕ))
rw₁ : #(Iio b) = #(map valEmbedding (Iio b))
rw₂ rw₃ : #(Iio b) = #(Iio b)
⊢ #(Iio b) = (↑b : ℕ)

Tactic:
rw [← Nat.card_Iio b, ← map_valEmbedding_Iio, card_map]

Premises used: Finset.card_map, Fin.val, Nat.card_Iio, Fin.map_valEmbedding_Iio
-- Module: Mathlib.Order.Interval.Finset.Fin
Goal:
n : ℕ
b : Fin n
hb : (↑b : ℕ) + 1 < n
⊢ Iio (b + 1) = Iic b

Tactic:
grind [= Fin.lt_def, = Fin.le_def, = Fin.val_add_one_of_lt']

Premises used: Fin.le_def, Fin.lt_def, Fin.val_add_one_of_lt'
-- Module: Mathlib.Order.Interval.Finset.Fin
Goal:
n : ℕ
b : Fin n
⊢ ∀ (hb : 0 < b), Iic (b - 1) = Iio b

Tactic:
grind [= Fin.val_sub_one_of_ne_zero]

Premises used: Fin.val_sub_one_of_ne_zero
-- Module: Mathlib.Order.Interval.Finset.Fin
Goal:
n : ℕ
a : Fin n
ha : (↑a : ℕ) + 1 < n
⊢ Ici (a + 1) = Ioi a

Tactic:
grind [= Fin.le_def, = Fin.val_add_one_of_lt']

Premises used: Fin.le_def, Fin.val_add_one_of_lt'
-- Module: Mathlib.Order.Interval.Finset.Fin
Goal:
n : ℕ
a : Fin n
⊢ ∀ (ha : 0 < a), Ioi (a - 1) = Ici a

Tactic:
grind [= Fin.lt_def, = Fin.le_def, = Fin.val_sub_one_of_ne_zero]

Premises used: Fin.val_sub_one_of_ne_zero, Fin.le_def, Fin.lt_def
-- Module: Mathlib.Order.Interval.Finset.Fin
Goal:
n : ℕ
a b : Fin n
⊢ ∀ (ha : 0 < a), Ioc (a - 1) b = Icc a b

Tactic:
grind [= Fin.lt_def, = Fin.le_def, = Fin.val_sub_one_of_ne_zero]

Premises used: Fin.val_sub_one_of_ne_zero, Fin.le_def, Fin.lt_def
-- Module: Mathlib.Order.Interval.Finset.Fin
Goal:
n : ℕ
a b : Fin n
ha : (↑a : ℕ) + 1 < n
⊢ Icc (a + 1) b = Ioc a b

Tactic:
grind [= Fin.lt_def, = Fin.le_def, = Fin.val_add_one_of_lt']

Premises used: Fin.le_def, Fin.lt_def, Fin.val_add_one_of_lt'
-- Module: Mathlib.Order.Interval.Finset.Fin
Goal:
n : ℕ
a b : Fin n
⊢ ∀ (ha : 0 < a), Ioo (a - 1) b = Ico a b

Tactic:
grind [= Fin.lt_def, = Fin.le_def, = Fin.val_sub_one_of_ne_zero]

Premises used: Fin.val_sub_one_of_ne_zero, Fin.le_def, Fin.lt_def
-- Module: Mathlib.Order.Interval.Finset.Fin
Goal:
n : ℕ
a b : Fin n
ha : (↑a : ℕ) + 1 < n
⊢ Ico (a + 1) b = Ioo a b

Tactic:
grind [= Fin.lt_def, = Fin.le_def, = Fin.val_add_one_of_lt']

Premises used: Fin.le_def, Fin.lt_def, Fin.val_add_one_of_lt'
-- Module: Mathlib.Order.Interval.Finset.Fin
Goal:
n : ℕ
a b : Fin n
⊢ ∀ (hb : 0 < b), Icc a (b - 1) = Ico a b

Tactic:
grind [= Fin.lt_def, = Fin.le_def, = Fin.val_sub_one_of_ne_zero]

Premises used: Fin.val_sub_one_of_ne_zero, Fin.le_def, Fin.lt_def
-- Module: Mathlib.Order.Interval.Finset.Fin
Goal:
n : ℕ
a b : Fin n
hb : (↑b : ℕ) + 1 < n
⊢ Ico a (b + 1) = Icc a b

Tactic:
grind [= Fin.lt_def, = Fin.le_def, = Fin.val_add_one_of_lt']

Premises used: Fin.le_def, Fin.lt_def, Fin.val_add_one_of_lt'
-- Module: Mathlib.Order.Interval.Finset.Fin
Goal:
n : ℕ
a b : Fin n
⊢ ∀ (hb : 0 < b), Ioc a (b - 1) = Ioo a b

Tactic:
grind [= Fin.lt_def, = Fin.le_def, = Fin.val_sub_one_of_ne_zero]

Premises used: Fin.val_sub_one_of_ne_zero, Fin.le_def, Fin.lt_def
-- Module: Mathlib.Order.Interval.Finset.Fin
Goal:
n : ℕ
a b : Fin n
hb : (↑b : ℕ) + 1 < n
⊢ Ioo a (b + 1) = Ioc a b

Tactic:
grind [= Fin.lt_def, = Fin.le_def, = Fin.val_add_one_of_lt']

Premises used: Fin.le_def, Fin.lt_def, Fin.val_add_one_of_lt'
-- Module: Mathlib.Order.Interval.Finset.Gaps
Goal:
α : Type u_1
inst : LinearOrder α
F : Finset (α × α)
k : ℕ
h : #F = k
a b : α
⊢ (F.intervalGapsWithin h a b 0).1 = a

Tactic:
simp [intervalGapsWithin, intervalGapsWithin.fst]

Premises used: Finset.intervalGapsWithin, Finset.intervalGapsWithin.fst
-- Module: Mathlib.Order.Interval.Finset.Gaps
Goal:
α : Type u_1
inst : LinearOrder α
F : Finset (α × α)
k : ℕ
h : #F = k
a b : α
j : ℕ
hj : j < k
h₁ : (↑(↑j.succ : Fin (k + 1)) : ℕ) = (↑(⟨j, hj⟩ : Fin k).succ : ℕ)
⊢ (↑j.succ : Fin (k + 1)) = (⟨j, hj⟩ : Fin k).succ

Tactic:
ext
-- Module: Mathlib.Order.Interval.Finset.Gaps
Goal:
α : Type u_1
inst : LinearOrder α
F : Finset (α × α)
k : ℕ
h : #F = k
a b : α
j : ℕ
hj : j < k
⊢ (↑(↑j.succ : Fin (k + 1)) : ℕ) = (↑(⟨j, hj⟩ : Fin k).succ : ℕ)

Tactic:
simp [hj]
-- Module: Mathlib.Order.Interval.Finset.Gaps
Goal:
α : Type u_1
inst : LinearOrder α
F : Finset (α × α)
k : ℕ
h : #F = k
a b : α
j : ℕ
hj : j < k
⊢ (↑j.succ : Fin (k + 1)) = (⟨j, hj⟩ : Fin k).succ

Tactic:
have : (j.succ : Fin (k + 1)) = (⟨j, hj⟩ : Fin k).succ := by ext; simp [hj]
-- Module: Mathlib.Order.Interval.Finset.Gaps
Goal:
α : Type u_1
inst : LinearOrder α
F : Finset (α × α)
k : ℕ
h : #F = k
a b : α
j : ℕ
hj : j < k
this : (↑j.succ : Fin (k + 1)) = (⟨j, hj⟩ : Fin k).succ
⊢ (F.intervalGapsWithin h a b (↑j.succ : Fin (k + 1))).1 =
    ((F.orderEmbOfFin h : (a : Fin k) → Lex (α × α)) (⟨j, hj⟩ : Fin k)).2

Tactic:
grind [intervalGapsWithin, intervalGapsWithin.fst]

Premises used: Finset.intervalGapsWithin, Finset.intervalGapsWithin.fst
-- Module: Mathlib.Order.Interval.Finset.Gaps
Goal:
α : Type u_1
inst : LinearOrder α
F : Finset (α × α)
k : ℕ
h : #F = k
a b : α
j : ℕ
hj₁ : 0 < j
hj₂ : j - 1 < k
⊢ (F.intervalGapsWithin h a b (↑(j - 1).succ : Fin (k + 1))).1 =
    ((F.orderEmbOfFin h : (a : Fin k) → Lex (α × α)) (⟨j - 1, hj₂⟩ : Fin k)).2

Tactic:
F.intervalGapsWithin_succ_fst_of_lt h a b (j - 1) hj₂

Premises used: HSub.hSub, Finset.intervalGapsWithin_succ_fst_of_lt, OfNat.ofNat
-- Module: Mathlib.Order.Interval.Finset.Gaps
Goal:
α : Type u_1
inst : LinearOrder α
F : Finset (α × α)
k : ℕ
h : #F = k
a b : α
j : ℕ
hj₁ : 0 < j
hj₂ : j - 1 < k
h₁ : j = (j - 1).succ
⊢ (F.intervalGapsWithin h a b (↑j : Fin (k + 1))).1 =
    ((F.orderEmbOfFin h : (a : Fin k) → Lex (α × α)) (⟨j - 1, hj₂⟩ : Fin k)).2

Tactic:
convert! F.intervalGapsWithin_succ_fst_of_lt h a b (j - 1) hj₂

Premises used: HSub.hSub, Finset.intervalGapsWithin_succ_fst_of_lt, OfNat.ofNat
-- Module: Mathlib.Order.Interval.Finset.Gaps
Goal:
α : Type u_1
inst : LinearOrder α
F : Finset (α × α)
k : ℕ
h : #F = k
a b : α
j : ℕ
hj₁ : 0 < j
hj₂ : j - 1 < k
⊢ j = (j - 1).succ

Tactic:
omega
-- Module: Mathlib.Order.Interval.Finset.Gaps
Goal:
α : Type u_1
inst : LinearOrder α
F : Finset (α × α)
k : ℕ
h : #F = k
a b : α
⊢ (F.intervalGapsWithin h a b (last k)).2 = b

Tactic:
simp [intervalGapsWithin, intervalGapsWithin.snd]

Premises used: Finset.intervalGapsWithin, Finset.intervalGapsWithin.snd
-- Module: Mathlib.Order.Interval.Finset.Gaps
Goal:
α : Type u_1
inst : LinearOrder α
F : Finset (α × α)
k : ℕ
h : #F = k
a b : α
j : ℕ
hj : j < k
⊢ (↑j : Fin (k + 1)) ≠ last k

Tactic:
grind [val_cast_of_lt]

Premises used: Fin.val_cast_of_lt
-- Module: Mathlib.Order.Interval.Finset.Gaps
Goal:
α : Type u_1
inst : LinearOrder α
F : Finset (α × α)
k : ℕ
h : #F = k
a b : α
j : ℕ
hj : j < k
⊢ (↑j : Fin (k + 1)) ≠ last k

Tactic:
have : (j : Fin (k + 1)) ≠ last k := by grind [val_cast_of_lt]
-- Module: Mathlib.Order.Interval.Finset.Gaps
Goal:
α : Type u_1
inst : LinearOrder α
F : Finset (α × α)
k : ℕ
h : #F = k
a b : α
j : ℕ
hj : j < k
this : (↑j : Fin (k + 1)) ≠ last k
simp :
  Eq.{u_1 + 1} (α := α) ((F.orderEmbOfFin h : (a : Fin k) → Lex (α × α)) (castPred (↑j : Fin (k + 1)) ⋯)).1
    ((F.orderEmbOfFin h : (a : Fin k) → Lex (α × α)) (⟨j, hj⟩ : Fin k)).1
⊢ (F.intervalGapsWithin h a b (↑j : Fin (k + 1))).2 =
    ((F.orderEmbOfFin h : (a : Fin k) → Lex (α × α)) (⟨j, hj⟩ : Fin k)).1

Tactic:
simp only [intervalGapsWithin, intervalGapsWithin.snd, this, ↓reduceDIte]

Premises used: reduceDIte, Finset.intervalGapsWithin, Finset.intervalGapsWithin.snd
-- Module: Mathlib.Order.Interval.Finset.Gaps
Goal:
α : Type u_1
inst : LinearOrder α
F : Finset (α × α)
k : ℕ
h : #F = k
a b : α
j : ℕ
hj : j < k
this : (↑j : Fin (k + 1)) ≠ last k
e_self : castPred (↑j : Fin (k + 1)) ⋯ = ⟨j, hj⟩
⊢ Eq.{u_1 + 1} (α := α) ((F.orderEmbOfFin h : (a : Fin k) → Lex (α × α)) (castPred (↑j : Fin (k + 1)) ⋯)).1
    ((F.orderEmbOfFin h : (a : Fin k) → Lex (α × α)) (⟨j, hj⟩ : Fin k)).1

Tactic:
congr
-- Module: Mathlib.Order.Interval.Finset.Gaps
Goal:
α : Type u_1
inst : LinearOrder α
F : Finset (α × α)
k : ℕ
h : #F = k
a b : α
j : ℕ
hj : j < k
this : (↑j : Fin (k + 1)) ≠ last k
e_self : (↑(castPred (↑j : Fin (k + 1)) ⋯) : ℕ) = (↑(⟨j, hj⟩ : Fin k) : ℕ)
⊢ castPred (↑j : Fin (k + 1)) ⋯ = ⟨j, hj⟩

Tactic:
ext
-- Module: Mathlib.Order.Interval.Finset.Gaps
Goal:
α : Type u_1
inst : LinearOrder α
F : Finset (α × α)
k : ℕ
h : #F = k
a b : α
j : ℕ
hj : j < k
this : (↑j : Fin (k + 1)) ≠ last k
e_self : j < k.succ
⊢ (↑(castPred (↑j : Fin (k + 1)) ⋯) : ℕ) = (↑(⟨j, hj⟩ : Fin k) : ℕ)

Tactic:
simp only [coe_castPred, val_natCast, Nat.mod_succ_eq_iff_lt]

Premises used: Fin.val_natCast, Fin.coe_castPred, Nat.mod_succ_eq_iff_lt
-- Module: Mathlib.Order.Interval.Finset.Gaps
Goal:
α : Type u_1
inst : LinearOrder α
F : Finset (α × α)
k : ℕ
h : #F = k
a b : α
j : ℕ
hj : j < k
this : (↑j : Fin (k + 1)) ≠ last k
⊢ j < k.succ

Tactic:
lia
-- Module: Mathlib.Order.Interval.Finset.Gaps
Goal:
α : Type u_1
inst : LinearOrder α
F : Finset (α × α)
k : ℕ
h : #F = k
a b : α
j : ℕ
hj : j ∈ Iio k
⊢ j < k

Tactic:
rw [mem_Iio] at hj

Premises used: Set.mem_Iio
-- Module: Mathlib.Order.Interval.Finset.Gaps
Goal:
α : Type u_1
inst : LinearOrder α
F : Finset (α × α)
k : ℕ
h : #F = k
a b : α
j : ℕ
hj : j < k
simp : Membership.mem (α := α × α) F ((F.orderEmbOfFin h : (a : Fin k) → Lex (α × α)) (⟨j, hj⟩ : Fin k) : Lex (α × α))
⊢ (fun (j : ℕ) ↦
        ((F.intervalGapsWithin h a b (↑j : Fin (k + 1))).2, (F.intervalGapsWithin h a b (↑j.succ : Fin (k + 1))).1))
      j ∈
    (↑F : Set (α × α))

Tactic:
simp only [intervalGapsWithin_snd_of_lt, intervalGapsWithin_succ_fst_of_lt,
    Prod.mk.eta, SetLike.mem_coe, hj]

Premises used: Finset.intervalGapsWithin_snd_of_lt, Finset.intervalGapsWithin_succ_fst_of_lt, SetLike.mem_coe, Prod.mk.eta
-- Module: Mathlib.Order.Interval.Finset.Gaps
Goal:
α : Type u_1
inst : LinearOrder α
F : Finset (α × α)
k : ℕ
h : #F = k
a b : α
j : ℕ
hj : j < k
⊢ Membership.mem (α := α × α) F ((F.orderEmbOfFin h : (a : Fin k) → α × α) (⟨j, hj⟩ : Fin k) : α × α)

Tactic:
F.orderEmbOfFin_mem h ⟨j, hj⟩

Premises used: Fin.mk, Finset.orderEmbOfFin_mem
-- Module: Mathlib.Order.Interval.Finset.Gaps
Goal:
α : Type u_1
inst : LinearOrder α
F : Finset (α × α)
k : ℕ
h : #F = k
a b : α
j : ℕ
hj : j < k
⊢ Membership.mem (α := α × α) F ((F.orderEmbOfFin h : (a : Fin k) → Lex (α × α)) (⟨j, hj⟩ : Fin k) : Lex (α × α))

Tactic:
convert! F.orderEmbOfFin_mem h ⟨j, hj⟩ using 1
-- Module: Mathlib.Order.Interval.Finset.Gaps
Goal:
α : Type u_1
inst : LinearOrder α
F : Finset (α × α)
k : ℕ
h : #F = k
a b : α
j : ℕ
hj : j ∈ Iio k
j' : ℕ
hj' : j' ∈ Iio k
hjj' :
  Eq.{u_1 + 1} (α := α × α)
    ((fun (j : ℕ) ↦
        ((F.intervalGapsWithin h a b (↑j : Fin (k + 1))).2, (F.intervalGapsWithin h a b (↑j.succ : Fin (k + 1))).1))
      j)
    ((fun (j : ℕ) ↦
        ((F.intervalGapsWithin h a b (↑j : Fin (k + 1))).2, (F.intervalGapsWithin h a b (↑j.succ : Fin (k + 1))).1))
      j')
rw :
  ∀ (hj : j < k) ⦃j' : ℕ⦄ (hj' : j' < k)
    (hjj' :
      Eq.{u_1 + 1} (α := α × α)
        ((fun (j : ℕ) ↦
            ((F.intervalGapsWithin h a b (↑j : Fin (k + 1))).2, (F.intervalGapsWithin h a b (↑j.succ : Fin (k + 1))).1))
          j)
        ((fun (j : ℕ) ↦
            ((F.intervalGapsWithin h a b (↑j : Fin (k + 1))).2, (F.intervalGapsWithin h a b (↑j.succ : Fin (k + 1))).1))
          j')),
    j = j'
⊢ j = j'

Tactic:
rw [mem_Iio] at hj hj'

Premises used: Set.mem_Iio
-- Module: Mathlib.Order.Interval.Finset.Gaps
Goal:
α : Type u_1
inst : LinearOrder α
F : Finset (α × α)
k : ℕ
h : #F = k
a b : α
j : ℕ
hj : j < k
j' : ℕ
hj' : j' < k
hjj' :
  Eq.{u_1 + 1} (α := α × α)
    ((fun (j : ℕ) ↦
        ((F.intervalGapsWithin h a b (↑j : Fin (k + 1))).2, (F.intervalGapsWithin h a b (↑j.succ : Fin (k + 1))).1))
      j)
    ((fun (j : ℕ) ↦
        ((F.intervalGapsWithin h a b (↑j : Fin (k + 1))).2, (F.intervalGapsWithin h a b (↑j.succ : Fin (k + 1))).1))
      j')
⊢ Eq.{u_1 + 1} (α := α × α)
    (((F.orderEmbOfFin h : (a : Fin k) → Lex (α × α)) (⟨j, hj⟩ : Fin k)).1,
      ((F.orderEmbOfFin h : (a : Fin k) → Lex (α × α)) (⟨j, hj⟩ : Fin k)).2)
    (((F.orderEmbOfFin h : (a : Fin k) → Lex (α × α)) (⟨j', hj'⟩ : Fin k)).1,
      ((F.orderEmbOfFin h : (a : Fin k) → Lex (α × α)) (⟨j', hj'⟩ : Fin k)).2)

Tactic:
simp only [hj, hj', intervalGapsWithin_snd_of_lt, intervalGapsWithin_succ_fst_of_lt] at hjj'

Premises used: Finset.intervalGapsWithin_snd_of_lt, Finset.intervalGapsWithin_succ_fst_of_lt
-- Module: Mathlib.Order.Interval.Finset.Gaps
Goal:
α : Type u_1
inst : LinearOrder α
F : Finset (α × α)
k : ℕ
h : #F = k
a b : α
j : ℕ
hj : j < k
j' : ℕ
hj' : j' < k
hjj' :
  Eq.{u_1 + 1} (α := α × α)
    (((F.orderEmbOfFin h : (a : Fin k) → Lex (α × α)) (⟨j, hj⟩ : Fin k)).1,
      ((F.orderEmbOfFin h : (a : Fin k) → Lex (α × α)) (⟨j, hj⟩ : Fin k)).2)
    (((F.orderEmbOfFin h : (a : Fin k) → Lex (α × α)) (⟨j', hj'⟩ : Fin k)).1,
      ((F.orderEmbOfFin h : (a : Fin k) → Lex (α × α)) (⟨j', hj'⟩ : Fin k)).2)
⊢ j = j'

Tactic:
grind [F.orderEmbOfFin (α := α ×ₗ α) h |>.injective hjj']

Premises used: Finset.orderEmbOfFin, RelEmbedding.injective
-- Module: Mathlib.Order.Interval.Finset.Gaps
Goal:
α : Type u_1
inst : LinearOrder α
F : Finset (α × α)
k : ℕ
h : #F = k
a b : α
z : α × α
hz : z ∈ (↑F : Set (α × α))
⊢ Membership.mem (γ := Set (α × α)) (Set.range (ι := Fin k) (⇑(F.orderEmbOfFin h) : (a : Fin k) → Lex (α × α))) z

Tactic:
rw [← F.range_orderEmbOfFin h (α := α ×ₗ α)] at hz

Premises used: Finset.range_orderEmbOfFin
-- Module: Mathlib.Order.Interval.Finset.Gaps
Goal:
α : Type u_1
inst : LinearOrder α
F : Finset (α × α)
k : ℕ
h : #F = k
a b : α
z : α × α
hz : Membership.mem (γ := Set (α × α)) (Set.range (ι := Fin k) (⇑(F.orderEmbOfFin h) : (a : Fin k) → Lex (α × α))) z
obtain :
  ∀ (j : Fin k) (hj : (F.orderEmbOfFin h : (a : Fin k) → Lex (α × α)) j = z),
    Membership.mem (γ := Set (α × α))
      ((fun (j : ℕ) ↦
          ((F.intervalGapsWithin h a b (↑j : Fin (k + 1))).2,
            (F.intervalGapsWithin h a b (↑j.succ : Fin (k + 1))).1)) ''
        Iio k)
      z
⊢ Membership.mem (γ := Set (α × α))
    ((fun (j : ℕ) ↦
        ((F.intervalGapsWithin h a b (↑j : Fin (k + 1))).2, (F.intervalGapsWithin h a b (↑j.succ : Fin (k + 1))).1)) ''
      Iio k)
    z

Tactic:
obtain ⟨j, hj⟩ := hz
-- Module: Mathlib.Order.Interval.Finset.Gaps
Goal:
α : Type u_1
inst : LinearOrder α
F : Finset (α × α)
k : ℕ
h : #F = k
a b : α
z : α × α
j : Fin k
hj : (F.orderEmbOfFin h : (a : Fin k) → Lex (α × α)) j = z
right :
  (fun (j : ℕ) ↦
        ((F.intervalGapsWithin h a b (↑j : Fin (k + 1))).2, (F.intervalGapsWithin h a b (↑j.succ : Fin (k + 1))).1))
      (↑j : ℕ) =
    z
⊢ Membership.mem (γ := Set (α × α))
    ((fun (j : ℕ) ↦
        ((F.intervalGapsWithin h a b (↑j : Fin (k + 1))).2, (F.intervalGapsWithin h a b (↑j.succ : Fin (k + 1))).1)) ''
      Iio k)
    z

Tactic:
use j.val, j.prop

Premises used: Fin.prop, Fin.val
-- Module: Mathlib.Order.Interval.Finset.Gaps
Goal:
α : Type u_1
inst : LinearOrder α
F : Finset (α × α)
k : ℕ
h : #F = k
a b : α
z : α × α
j : Fin k
hj : (F.orderEmbOfFin h : (a : Fin k) → Lex (α × α)) j = z
⊢ (fun (j : ℕ) ↦
        ((F.intervalGapsWithin h a b (↑j : Fin (k + 1))).2, (F.intervalGapsWithin h a b (↑j.succ : Fin (k + 1))).1))
      (↑j : ℕ) =
    z

Tactic:
simp [intervalGapsWithin_snd_of_lt, intervalGapsWithin_succ_fst_of_lt, j.prop, hj,
    -coe_eq_castSucc]

Premises used: Fin.prop, Fin.coe_eq_castSucc, Finset.intervalGapsWithin_snd_of_lt, Finset.intervalGapsWithin_succ_fst_of_lt
-- Module: Mathlib.Order.Interval.Finset.Gaps
Goal:
α : Type u_1
inst : LinearOrder α
F : Finset (α × α)
k : ℕ
h : #F = k
j : ℕ
a b : α
hFab : ∀ ⦃z : α × α⦄, z ∈ F → a ≤ z.1 ∧ z.1 ≤ z.2 ∧ z.2 ≤ b
inr :
  ∀ (this : ∀ (j : ℕ) (hj : j < k + 1), a ≤ (F.intervalGapsWithin h a b (↑j : Fin (k + 1))).1) (hj : ¬j < k + 1),
    a ≤ (F.intervalGapsWithin h a b (↑j : Fin (k + 1))).1
wlog : ∀ (j : ℕ) (hj : j < k + 1), a ≤ (F.intervalGapsWithin h a b (↑j : Fin (k + 1))).1
⊢ a ≤ (F.intervalGapsWithin h a b (↑j : Fin (k + 1))).1

Tactic:
wlog hj : j < k + 1 generalizing j
-- Module: Mathlib.Order.Interval.Finset.Gaps
Goal:
α : Type u_1
inst : LinearOrder α
F : Finset (α × α)
k : ℕ
h : #F = k
j : ℕ
a b : α
hFab : ∀ ⦃z : α × α⦄, z ∈ F → a ≤ z.1 ∧ z.1 ≤ z.2 ∧ z.2 ≤ b
this : ∀ (j : ℕ) (hj : j < k + 1), a ≤ (F.intervalGapsWithin h a b (↑j : Fin (k + 1))).1
hj : ¬j < k + 1
⊢ a ≤ (F.intervalGapsWithin h a b (↑j : Fin (k + 1))).1

Tactic:
grind [cast_val_eq_self]

Premises used: Fin.cast_val_eq_self
-- Module: Mathlib.Order.Interval.Finset.Gaps
Goal:
α : Type u_1
inst : LinearOrder α
F : Finset (α × α)
k : ℕ
h : #F = k
j_1 : ℕ
a b : α
hFab : ∀ ⦃z : α × α⦄, z ∈ F → a ≤ z.1 ∧ z.1 ≤ z.2 ∧ z.2 ≤ b
j : ℕ
hj : j < k + 1
pos : ∀ (hj : j = 0), a ≤ (F.intervalGapsWithin h a b (↑j : Fin (k + 1))).1
neg : ∀ (hj : ¬j = 0), a ≤ (F.intervalGapsWithin h a b (↑j : Fin (k + 1))).1
⊢ a ≤ (F.intervalGapsWithin h a b (↑j : Fin (k + 1))).1

Tactic:
by_cases hj : j = 0
-- Module: Mathlib.Order.Interval.Finset.Gaps
Goal:
α : Type u_1
inst : LinearOrder α
F : Finset (α × α)
k : ℕ
h : #F = k
j_1 : ℕ
a b : α
hFab : ∀ ⦃z : α × α⦄, z ∈ F → a ≤ z.1 ∧ z.1 ≤ z.2 ∧ z.2 ≤ b
j : ℕ
hj_1 : j < k + 1
hj : j = 0
⊢ a ≤ (F.intervalGapsWithin h a b (↑j : Fin (k + 1))).1

Tactic:
simp [hj]
-- Module: Mathlib.Order.Interval.Finset.Gaps
Goal:
α : Type u_1
inst : LinearOrder α
F : Finset (α × α)
k : ℕ
h : #F = k
j_1 : ℕ
a b : α
hFab : ∀ ⦃z : α × α⦄, z ∈ F → a ≤ z.1 ∧ z.1 ≤ z.2 ∧ z.2 ≤ b
j : ℕ
hj_1 : j < k + 1
hj : ¬j = 0
⊢ j - 1 ∈ Iio k

Tactic:
grind
-- Module: Mathlib.Order.Interval.Finset.Gaps
Goal:
α : Type u_1
inst : LinearOrder α
F : Finset (α × α)
k : ℕ
h : #F = k
j_1 : ℕ
a b : α
hFab : ∀ ⦃z : α × α⦄, z ∈ F → a ≤ z.1 ∧ z.1 ≤ z.2 ∧ z.2 ≤ b
j : ℕ
hj_1 : j < k + 1
hj : ¬j = 0
⊢ a ≤
      ((fun (j : ℕ) ↦
            ((F.intervalGapsWithin h a b (↑j : Fin (k + 1))).2, (F.intervalGapsWithin h a b (↑j.succ : Fin (k + 1))).1))
          (j - 1)).1 ∧
    LE.le.{u_1} (α := α)
        ((fun (j : ℕ) ↦
              ((F.intervalGapsWithin h a b (↑j : Fin (k + 1))).2,
                (F.intervalGapsWithin h a b (↑j.succ : Fin (k + 1))).1))
            (j - 1)).1
        ((fun (j : ℕ) ↦
              ((F.intervalGapsWithin h a b (↑j : Fin (k + 1))).2,
                (F.intervalGapsWithin h a b (↑j.succ : Fin (k + 1))).1))
            (j - 1)).2 ∧
      ((fun (j : ℕ) ↦
              ((F.intervalGapsWithin h a b (↑j : Fin (k + 1))).2,
                (F.intervalGapsWithin h a b (↑j.succ : Fin (k + 1))).1))
            (j - 1)).2 ≤
        b

Tactic:
have := hFab (F.intervalGapsWithin_mapsTo h a b (x := j - 1) (by grind))
-- Module: Mathlib.Order.Interval.Finset.Gaps
Goal:
α : Type u_1
inst : LinearOrder α
F : Finset (α × α)
k : ℕ
h : #F = k
j_1 : ℕ
a b : α
hFab : ∀ ⦃z : α × α⦄, z ∈ F → a ≤ z.1 ∧ z.1 ≤ z.2 ∧ z.2 ≤ b
j : ℕ
hj_1 : j < k + 1
hj : ¬j = 0
this :
  a ≤
      ((fun (j : ℕ) ↦
            ((F.intervalGapsWithin h a b (↑j : Fin (k + 1))).2, (F.intervalGapsWithin h a b (↑j.succ : Fin (k + 1))).1))
          (j - 1)).1 ∧
    LE.le.{u_1} (α := α)
        ((fun (j : ℕ) ↦
              ((F.intervalGapsWithin h a b (↑j : Fin (k + 1))).2,
                (F.intervalGapsWithin h a b (↑j.succ : Fin (k + 1))).1))
            (j - 1)).1
        ((fun (j : ℕ) ↦
              ((F.intervalGapsWithin h a b (↑j : Fin (k + 1))).2,
                (F.intervalGapsWithin h a b (↑j.succ : Fin (k + 1))).1))
            (j - 1)).2 ∧
      ((fun (j : ℕ) ↦
              ((F.intervalGapsWithin h a b (↑j : Fin (k + 1))).2,
                (F.intervalGapsWithin h a b (↑j.succ : Fin (k + 1))).1))
            (j - 1)).2 ≤
        b
⊢ j - 1 + 1 = j

Tactic:
lia
-- Module: Mathlib.Order.Interval.Finset.Gaps
Goal:
α : Type u_1
inst : LinearOrder α
F : Finset (α × α)
k : ℕ
h : #F = k
j_1 : ℕ
a b : α
hFab : ∀ ⦃z : α × α⦄, z ∈ F → a ≤ z.1 ∧ z.1 ≤ z.2 ∧ z.2 ≤ b
j : ℕ
hj_1 : j < k + 1
hj : ¬j = 0
this :
  a ≤
      ((fun (j : ℕ) ↦
            ((F.intervalGapsWithin h a b (↑j : Fin (k + 1))).2, (F.intervalGapsWithin h a b (↑j.succ : Fin (k + 1))).1))
          (j - 1)).1 ∧
    LE.le.{u_1} (α := α)
        ((fun (j : ℕ) ↦
              ((F.intervalGapsWithin h a b (↑j : Fin (k + 1))).2,
                (F.intervalGapsWithin h a b (↑j.succ : Fin (k + 1))).1))
            (j - 1)).1
        ((fun (j : ℕ) ↦
              ((F.intervalGapsWithin h a b (↑j : Fin (k + 1))).2,
                (F.intervalGapsWithin h a b (↑j.succ : Fin (k + 1))).1))
            (j - 1)).2 ∧
      ((fun (j : ℕ) ↦
              ((F.intervalGapsWithin h a b (↑j : Fin (k + 1))).2,
                (F.intervalGapsWithin h a b (↑j.succ : Fin (k + 1))).1))
            (j - 1)).2 ≤
        b
⊢ j - 1 + 1 = j

Tactic:
have hj₀ : j - 1 + 1 = j := by lia