awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
inst : Lattice α
inst_1 : LocallyFiniteOrder α
a b x : α
ha : a ≤ x
hb : x ≤ b
⊢ x ∈ [[a, b]]

Tactic:
Icc_subset_uIcc <| mem_Icc.2 ⟨ha, hb⟩

Premises used: Iff.mpr, Finset.mem_Icc, Finset.Icc_subset_uIcc, And.intro
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
inst : Lattice α
inst_1 : LocallyFiniteOrder α
a b x : α
hb : b ≤ x
ha : x ≤ a
⊢ x ∈ [[a, b]]

Tactic:
Icc_subset_uIcc' <| mem_Icc.2 ⟨hb, ha⟩

Premises used: Iff.mpr, Finset.Icc_subset_uIcc', Finset.mem_Icc, And.intro
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
inst : Lattice α
inst_1 : LocallyFiniteOrder α
a₁ a₂ b₁ b₂ : α
h₁ : a₁ ∈ [[a₂, b₂]]
h₂ : b₁ ∈ [[a₂, b₂]]
⊢ a₂ ⊓ b₂ ≤ a₁ ∧ a₁ ≤ a₂ ⊔ b₂

Tactic:
rw [mem_uIcc] at h₁ h₂

Premises used: Finset.mem_uIcc
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
inst : Lattice α
inst_1 : LocallyFiniteOrder α
a₁ a₂ b₁ b₂ : α
h₁ : a₁ ∈ [[a₂, b₂]]
h₂ : b₁ ∈ [[a₂, b₂]]
h₃ : a₂ ⊓ b₂ ≤ a₁ ∧ a₁ ≤ a₂ ⊔ b₂
⊢ a₂ ⊓ b₂ ≤ b₁ ∧ b₁ ≤ a₂ ⊔ b₂

Tactic:
rw [mem_uIcc] at h₁ h₂

Premises used: Finset.mem_uIcc
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
inst : Lattice α
inst_1 : LocallyFiniteOrder α
a₁ a₂ b₁ b₂ : α
h₁ : a₂ ⊓ b₂ ≤ a₁ ∧ a₁ ≤ a₂ ⊔ b₂
h₂ : a₂ ⊓ b₂ ≤ b₁ ∧ b₁ ≤ a₂ ⊔ b₂
⊢ [[a₁, b₁]] ⊆ [[a₂, b₂]]

Tactic:
Icc_subset_Icc (_root_.le_inf h₁.1 h₂.1) (_root_.sup_le h₁.2 h₂.2)

Premises used: Set.Mem, setOf, le_inf, Finset.Icc_subset_Icc, And.right, And.left, sup_le
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
inst : Lattice α
inst_1 : LocallyFiniteOrder α
a₁ a₂ b₁ b₂ : α
h₁ : a₂ ⊓ b₂ ≤ a₁ ∧ a₁ ≤ a₂ ⊔ b₂
h₂ : a₂ ⊓ b₂ ≤ b₁ ∧ b₁ ≤ a₂ ⊔ b₂
⊢ [[a₁, b₁]] ⊆ [[a₂, b₂]]

Tactic:
exact Icc_subset_Icc (_root_.le_inf h₁.1 h₂.1) (_root_.sup_le h₁.2 h₂.2)

Premises used: le_inf, Finset.Icc_subset_Icc, And.right, And.left, sup_le
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
inst : Lattice α
inst_1 : LocallyFiniteOrder α
a₁ a₂ b₁ b₂ : α
ha : a₁ ∈ Icc a₂ b₂
hb : b₁ ∈ Icc a₂ b₂
⊢ a₂ ≤ a₁ ∧ a₁ ≤ b₂

Tactic:
rw [mem_Icc] at ha hb

Premises used: Finset.mem_Icc
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
inst : Lattice α
inst_1 : LocallyFiniteOrder α
a₁ a₂ b₁ b₂ : α
ha : a₁ ∈ Icc a₂ b₂
hb : b₁ ∈ Icc a₂ b₂
ha₁ : a₂ ≤ a₁ ∧ a₁ ≤ b₂
⊢ a₂ ≤ b₁ ∧ b₁ ≤ b₂

Tactic:
rw [mem_Icc] at ha hb

Premises used: Finset.mem_Icc
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
inst : Lattice α
inst_1 : LocallyFiniteOrder α
a₁ a₂ b₁ b₂ : α
ha : a₂ ≤ a₁ ∧ a₁ ≤ b₂
hb : a₂ ≤ b₁ ∧ b₁ ≤ b₂
⊢ [[a₁, b₁]] ⊆ Icc a₂ b₂

Tactic:
Icc_subset_Icc (_root_.le_inf ha.1 hb.1) (_root_.sup_le ha.2 hb.2)

Premises used: Set.Mem, setOf, le_inf, Finset.Icc_subset_Icc, And.right, And.left, sup_le
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
inst : Lattice α
inst_1 : LocallyFiniteOrder α
a₁ a₂ b₁ b₂ : α
ha : a₂ ≤ a₁ ∧ a₁ ≤ b₂
hb : a₂ ≤ b₁ ∧ b₁ ≤ b₂
⊢ [[a₁, b₁]] ⊆ Icc a₂ b₂

Tactic:
exact Icc_subset_Icc (_root_.le_inf ha.1 hb.1) (_root_.sup_le ha.2 hb.2)

Premises used: le_inf, Finset.Icc_subset_Icc, And.right, And.left, sup_le
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
inst : Lattice α
inst_1 : LocallyFiniteOrder α
a₁ a₂ b₁ b₂ : α
⊢ [[a₁, b₁]] ⊆ [[a₂, b₂]] ↔ a₁ ∈ [[a₂, b₂]] ∧ b₁ ∈ [[a₂, b₂]]

Tactic:
⟨fun h => ⟨h left_mem_uIcc, h right_mem_uIcc⟩, fun h => uIcc_subset_uIcc h.1 h.2⟩

Premises used: Finset.right_mem_uIcc, Finset.uIcc_subset_uIcc, Finset.left_mem_uIcc, And.right, And.left, And.intro, Iff.intro
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
inst : Lattice α
inst_1 : LocallyFiniteOrder α
a₁ a₂ b₁ b₂ : α
⊢ [[a₁, b₁]] ⊆ [[a₂, b₂]] ↔ a₂ ⊓ b₂ ≤ a₁ ⊓ b₁ ∧ a₁ ⊔ b₁ ≤ a₂ ⊔ b₂

Tactic:
Icc_subset_Icc_iff inf_le_sup

Premises used: Set.Mem, setOf, inf_le_sup, Finset.Icc_subset_Icc_iff
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
inst : Lattice α
inst_1 : LocallyFiniteOrder α
a b x : α
h : x ∈ [[a, b]]
⊢ [[x, b]] ⊆ [[a, b]]

Tactic:
uIcc_subset_uIcc h right_mem_uIcc

Premises used: Finset.right_mem_uIcc, Finset.uIcc_subset_uIcc
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
inst : Lattice α
inst_1 : LocallyFiniteOrder α
a b x : α
h : x ∈ [[a, b]]
⊢ [[a, x]] ⊆ [[a, b]]

Tactic:
uIcc_subset_uIcc left_mem_uIcc h

Premises used: Finset.uIcc_subset_uIcc, Finset.left_mem_uIcc
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
inst : DistribLattice α
inst_1 : LocallyFiniteOrder α
a b c : α
simp_rw : b ⊓ c ≤ a ∧ a ≤ b ⊔ c → a ⊓ c ≤ b ∧ b ≤ a ⊔ c → a = b
⊢ a ∈ [[b, c]] → b ∈ [[a, c]] → a = b

Tactic:
simp_rw [mem_uIcc]

Premises used: Finset.mem_uIcc
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
inst : DistribLattice α
inst_1 : LocallyFiniteOrder α
a b c : α
⊢ b ⊓ c ≤ a ∧ a ≤ b ⊔ c → a ⊓ c ≤ b ∧ b ≤ a ⊔ c → a = b

Tactic:
Set.eq_of_mem_uIcc_of_mem_uIcc

Premises used: Set.Mem, setOf, Set.eq_of_mem_uIcc_of_mem_uIcc, Set.Icc, Set.uIcc
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
inst : DistribLattice α
inst_1 : LocallyFiniteOrder α
a b c : α
⊢ b ⊓ c ≤ a ∧ a ≤ b ⊔ c → a ⊓ c ≤ b ∧ b ≤ a ⊔ c → a = b

Tactic:
exact Set.eq_of_mem_uIcc_of_mem_uIcc

Premises used: Set.eq_of_mem_uIcc_of_mem_uIcc
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
inst : DistribLattice α
inst_1 : LocallyFiniteOrder α
a b c : α
simp_rw : a ⊓ c ≤ b ∧ b ≤ a ⊔ c → a ⊓ b ≤ c ∧ c ≤ a ⊔ b → b = c
⊢ b ∈ [[a, c]] → c ∈ [[a, b]] → b = c

Tactic:
simp_rw [mem_uIcc]

Premises used: Finset.mem_uIcc
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
inst : DistribLattice α
inst_1 : LocallyFiniteOrder α
a b c : α
⊢ a ⊓ c ≤ b ∧ b ≤ a ⊔ c → a ⊓ b ≤ c ∧ c ≤ a ⊔ b → b = c

Tactic:
Set.eq_of_mem_uIcc_of_mem_uIcc'

Premises used: Set.eq_of_mem_uIcc_of_mem_uIcc', Set.Mem, setOf, Set.Icc, Set.uIcc
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
inst : DistribLattice α
inst_1 : LocallyFiniteOrder α
a b c : α
⊢ a ⊓ c ≤ b ∧ b ≤ a ⊔ c → a ⊓ b ≤ c ∧ c ≤ a ⊔ b → b = c

Tactic:
exact Set.eq_of_mem_uIcc_of_mem_uIcc'

Premises used: Set.eq_of_mem_uIcc_of_mem_uIcc'
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
inst : DistribLattice α
inst_1 : LocallyFiniteOrder α
a b c : α
h : Eq.{u_2 + 1} (α := Finset α) ((fun (b : α) ↦ [[b, a]]) b) ((fun (b : α) ↦ [[b, a]]) c)
⊢ ∀ (a_1 : α),
    Membership.mem (γ := Finset α) ((fun (b : α) ↦ [[b, a]]) b) a_1 ↔
      Membership.mem (γ := Finset α) ((fun (b : α) ↦ [[b, a]]) c) a_1

Tactic:
rw [Finset.ext_iff] at h

Premises used: Finset.ext_iff
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
inst : DistribLattice α
inst_1 : LocallyFiniteOrder α
a b c : α
h :
  ∀ (a_1 : α),
    Membership.mem (γ := Finset α) ((fun (b : α) ↦ [[b, a]]) b) a_1 ↔
      Membership.mem (γ := Finset α) ((fun (b : α) ↦ [[b, a]]) c) a_1
⊢ b = c

Tactic:
eq_of_mem_uIcc_of_mem_uIcc ((h _).1 left_mem_uIcc) ((h _).2 left_mem_uIcc)

Premises used: Iff.mpr, Finset.eq_of_mem_uIcc_of_mem_uIcc, Finset.left_mem_uIcc, Iff.mp
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
inst : DistribLattice α
inst_1 : LocallyFiniteOrder α
a b c : α
h :
  ∀ (a_1 : α),
    Membership.mem (γ := Finset α) ((fun (b : α) ↦ [[b, a]]) b) a_1 ↔
      Membership.mem (γ := Finset α) ((fun (b : α) ↦ [[b, a]]) c) a_1
⊢ b = c

Tactic:
exact eq_of_mem_uIcc_of_mem_uIcc ((h _).1 left_mem_uIcc) ((h _).2 left_mem_uIcc)

Premises used: Iff.mpr, Finset.eq_of_mem_uIcc_of_mem_uIcc, Finset.left_mem_uIcc, Iff.mp
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
inst : DistribLattice α
inst_1 : LocallyFiniteOrder α
a : α
⊢ Injective (uIcc a)

Tactic:
simpa only [uIcc_comm] using uIcc_injective_right a

Premises used: Finset.uIcc_injective_right, Finset.uIcc_comm
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
inst : LinearOrder α
inst_1 : LocallyFiniteOrder α
a b : α
⊢ Icc (min a b) (max a b) = [[a, b]]

Tactic:
rfl

Premises used: rfl, Finset.uIcc
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
inst : LinearOrder α
inst_1 : LocallyFiniteOrder α
a b : α
h : ¬a ≤ b
⊢ [[a, b]] = Icc b a

Tactic:
uIcc_of_ge <| le_of_not_ge h

Premises used: Finset.uIcc_of_ge, le_of_not_ge
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
inst : LinearOrder α
inst_1 : LocallyFiniteOrder α
a b : α
h : ¬b ≤ a
⊢ [[a, b]] = Icc a b

Tactic:
uIcc_of_le <| le_of_not_ge h

Premises used: Finset.uIcc_of_le, le_of_not_ge
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
inst : LinearOrder α
inst_1 : LocallyFiniteOrder α
a b : α
push_cast : Set.uIcc a b = Set.Icc a b ∪ Set.Icc b a
⊢ (↑[[a, b]] : Set α) = (↑(Icc a b ∪ Icc b a) : Set α)

Tactic:
push_cast
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
inst : LinearOrder α
inst_1 : LocallyFiniteOrder α
a b : α
⊢ Set.uIcc a b = Set.Icc a b ∪ Set.Icc b a

Tactic:
Set.uIcc_eq_union

Premises used: Set.uIcc_eq_union
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
inst : LinearOrder α
inst_1 : LocallyFiniteOrder α
a b : α
⊢ Set.uIcc a b = Set.Icc a b ∪ Set.Icc b a

Tactic:
exact Set.uIcc_eq_union

Premises used: Set.uIcc_eq_union
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
inst : LinearOrder α
inst_1 : LocallyFiniteOrder α
a b c : α
⊢ a ∈ [[b, c]] ↔ b ≤ a ∧ a ≤ c ∨ c ≤ a ∧ a ≤ b

Tactic:
simp [uIcc_eq_union]

Premises used: Finset.uIcc_eq_union
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
inst : LinearOrder α
inst_1 : LocallyFiniteOrder α
a b c : α
rw : c < a → c < b → ¬(min a b ≤ c ∧ c ≤ max a b)
⊢ c < a → c < b → c ∉ [[a, b]]

Tactic:
rw [mem_uIcc]

Premises used: Finset.mem_uIcc
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
inst : LinearOrder α
inst_1 : LocallyFiniteOrder α
a b c : α
⊢ c < a → c < b → ¬(min a b ≤ c ∧ c ≤ max a b)

Tactic:
Set.notMem_uIcc_of_lt

Premises used: Set.Mem, Set.notMem_uIcc_of_lt, setOf, Set.Icc, Set.uIcc
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
inst : LinearOrder α
inst_1 : LocallyFiniteOrder α
a b c : α
⊢ c < a → c < b → ¬(min a b ≤ c ∧ c ≤ max a b)

Tactic:
exact Set.notMem_uIcc_of_lt

Premises used: Set.notMem_uIcc_of_lt
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
inst : LinearOrder α
inst_1 : LocallyFiniteOrder α
a b c : α
rw : a < c → b < c → ¬(min a b ≤ c ∧ c ≤ max a b)
⊢ a < c → b < c → c ∉ [[a, b]]

Tactic:
rw [mem_uIcc]

Premises used: Finset.mem_uIcc
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
inst : LinearOrder α
inst_1 : LocallyFiniteOrder α
a b c : α
⊢ a < c → b < c → ¬(min a b ≤ c ∧ c ≤ max a b)

Tactic:
Set.notMem_uIcc_of_gt

Premises used: Set.Mem, setOf, Set.notMem_uIcc_of_gt, Set.Icc, Set.uIcc
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
inst : LinearOrder α
inst_1 : LocallyFiniteOrder α
a b c : α
⊢ a < c → b < c → ¬(min a b ≤ c ∧ c ≤ max a b)

Tactic:
exact Set.notMem_uIcc_of_gt

Premises used: Set.notMem_uIcc_of_gt
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
inst : LinearOrder α
inst_1 : LocallyFiniteOrder α
a₁ a₂ b₁ b₂ : α
⊢ [[a₁, b₁]] ⊆ [[a₂, b₂]] ↔ min a₂ b₂ ≤ min a₁ b₁ ∧ max a₁ b₁ ≤ max a₂ b₂

Tactic:
uIcc_subset_uIcc_iff_le'

Premises used: Finset.uIcc_subset_uIcc_iff_le'
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
inst : LinearOrder α
inst_1 : LocallyFiniteOrder α
a b c : α
push_cast : Set.uIcc a c ⊆ Set.uIcc a b ∪ Set.uIcc b c
⊢ (↑[[a, c]] : Set α) ⊆ (↑([[a, b]] ∪ [[b, c]]) : Set α)

Tactic:
push_cast
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
inst : LinearOrder α
inst_1 : LocallyFiniteOrder α
a b c : α
⊢ Set.uIcc a c ⊆ Set.uIcc a b ∪ Set.uIcc b c

Tactic:
Set.uIcc_subset_uIcc_union_uIcc

Premises used: Set.uIcc_subset_uIcc_union_uIcc
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
inst : LinearOrder α
inst_1 : LocallyFiniteOrder α
a b c : α
⊢ Set.uIcc a c ⊆ Set.uIcc a b ∪ Set.uIcc b c

Tactic:
exact Set.uIcc_subset_uIcc_union_uIcc

Premises used: Set.uIcc_subset_uIcc_union_uIcc
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
inst : Preorder α
inst_1 : LocallyFiniteOrder α
x y : α
hxy : x ≤ y
⊢ #(Ico x y) < #(Icc x y)

Tactic:
have : #(Ico x y) < #(Icc x y) := card_lt_card <|
    ⟨Ico_subset_Icc_self, not_subset.mpr ⟨y, ⟨right_mem_Icc.mpr hxy, right_notMem_Ico⟩⟩⟩
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
inst : Preorder α
inst_1 : LocallyFiniteOrder α
x y : α
hxy : x ≤ y
this : #(Ico x y) < #(Icc x y)
pos : ∀ (hxy' : y ≤ x), TransGen (fun (x1 x2 : α) ↦ x1 ⩿ x2) x y
neg : ∀ (hxy' : ¬y ≤ x), TransGen (fun (x1 x2 : α) ↦ x1 ⩿ x2) x y
⊢ TransGen (fun (x1 x2 : α) ↦ x1 ⩿ x2) x y

Tactic:
by_cases hxy' : y ≤ x
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
inst : Preorder α
inst_1 : LocallyFiniteOrder α
x y : α
hxy : x ≤ y
this : #(Ico x y) < #(Icc x y)
hxy' : y ≤ x
⊢ TransGen (fun (x1 x2 : α) ↦ x1 ⩿ x2) x y

Tactic:
.single <| wcovBy_of_le_of_le hxy hxy'

Premises used: wcovBy_of_le_of_le, Relation.TransGen.single
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
inst : Preorder α
inst_1 : LocallyFiniteOrder α
x y : α
hxy : x ≤ y
this : #(Ico x y) < #(Icc x y)
hxy' : y ≤ x
⊢ TransGen (fun (x1 x2 : α) ↦ x1 ⩿ x2) x y

Tactic:
exact .single <| wcovBy_of_le_of_le hxy hxy'

Premises used: wcovBy_of_le_of_le
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
inst : Preorder α
inst_1 : LocallyFiniteOrder α
x y : α
hxy : x ≤ y
this : #(Ico x y) < #(Icc x y)
hxy' : ¬y ≤ x
neg :
  ∀ (z : α) (hxz : x ≤ z) (hz : Maximal (fun (x_1 : α) ↦ x_1 ∈ Set.Ico x y) z), TransGen (fun (x1 x2 : α) ↦ x1 ⩿ x2) x y
⊢ TransGen (fun (x1 x2 : α) ↦ x1 ⩿ x2) x y

Tactic:
obtain ⟨z, hxz, hz⟩ :=
      (Set.finite_Ico x y).exists_le_maximal <| Set.left_mem_Ico.2 <| hxy.lt_of_not_ge hxy'

Premises used: Iff.mpr, LE.le.lt_of_not_ge, Set.left_mem_Ico, Set.Finite.exists_le_maximal, Set.finite_Ico
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
inst : Preorder α
inst_1 : LocallyFiniteOrder α
x y : α
hxy : x ≤ y
this : #(Ico x y) < #(Icc x y)
hxy' : ¬y ≤ x
z : α
hxz : x ≤ z
hz : Maximal (fun (x_1 : α) ↦ x_1 ∈ Set.Ico x y) z
⊢ #(Icc x z) < #(Icc x y)

Tactic:
have z_card := calc
      #(Icc x z) ≤ #(Ico x y) := card_le_card <| Icc_subset_Ico_right hz.1.2
      _          < #(Icc x y) := this
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
inst : Preorder α
inst_1 : LocallyFiniteOrder α
x y : α
hxy : x ≤ y
this : #(Ico x y) < #(Icc x y)
hxy' : ¬y ≤ x
z : α
hxz : x ≤ z
hz : Maximal (fun (x_1 : α) ↦ x_1 ∈ Set.Ico x y) z
z_card : #(Icc x z) < #(Icc x y)
⊢ TransGen (fun (x1 x2 : α) ↦ x1 ⩿ x2) x z

Tactic:
have h₁ := transGen_wcovBy_of_le hz.1.1
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
inst : Preorder α
inst_1 : LocallyFiniteOrder α
x y : α
hxy : x ≤ y
this : #(Ico x y) < #(Icc x y)
hxy' : ¬y ≤ x
z : α
hxz : x ≤ z
hz : Maximal (fun (x_1 : α) ↦ x_1 ∈ Set.Ico x y) z
z_card : #(Icc x z) < #(Icc x y)
h₁ : TransGen (fun (x1 x2 : α) ↦ x1 ⩿ x2) x z
⊢ z ⩿ y

Tactic:
have h₂ : z ⩿ y :=
      ⟨hz.1.2.le, fun c hzc hcy ↦ hzc.not_ge <| hz.2 ⟨hz.1.1.trans hzc.le, hcy⟩ hzc.le⟩
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
inst : Preorder α
inst_1 : LocallyFiniteOrder α
x y : α
hxy : x ≤ y
this : #(Ico x y) < #(Icc x y)
hxy' : ¬y ≤ x
z : α
hxz : x ≤ z
hz : Maximal (fun (x_1 : α) ↦ x_1 ∈ Set.Ico x y) z
z_card : #(Icc x z) < #(Icc x y)
h₁ : TransGen (fun (x1 x2 : α) ↦ x1 ⩿ x2) x z
h₂ : z ⩿ y
⊢ TransGen (fun (x1 x2 : α) ↦ x1 ⩿ x2) x y

Tactic:
.tail h₁ h₂

Premises used: Relation.TransGen.tail
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
inst : Preorder α
inst_1 : LocallyFiniteOrder α
x y : α
hxy : x ≤ y
this : #(Ico x y) < #(Icc x y)
hxy' : ¬y ≤ x
z : α
hxz : x ≤ z
hz : Maximal (fun (x_1 : α) ↦ x_1 ∈ Set.Ico x y) z
z_card : #(Icc x z) < #(Icc x y)
h₁ : TransGen (fun (x1 x2 : α) ↦ x1 ⩿ x2) x z
h₂ : z ⩿ y
⊢ TransGen (fun (x1 x2 : α) ↦ x1 ⩿ x2) x y

Tactic:
exact .tail h₁ h₂
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
inst : Preorder α
inst_1 : LocallyFiniteOrder α
x y : α
⊢ x ≤ y ↔ TransGen (fun (x1 x2 : α) ↦ x1 ⩿ x2) x y

Tactic:
⟨transGen_wcovBy_of_le, fun h ↦ ?_⟩

Premises used: transGen_wcovBy_of_le, Iff.intro
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
inst : Preorder α
inst_1 : LocallyFiniteOrder α
x y : α
refine : ∀ (h : TransGen (fun (x1 x2 : α) ↦ x1 ⩿ x2) x y), x ≤ y
⊢ x ≤ y ↔ TransGen (fun (x1 x2 : α) ↦ x1 ⩿ x2) x y

Tactic:
refine ⟨transGen_wcovBy_of_le, fun h ↦ ?_⟩
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
inst : Preorder α
inst_1 : LocallyFiniteOrder α
x y b : α
h : x ⩿ b
⊢ x ≤ b

Tactic:
h.le

Premises used: WCovBy.le
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
inst : Preorder α
inst_1 : LocallyFiniteOrder α
x y b : α
h : x ⩿ b
⊢ x ≤ b

Tactic:
exact h.le

Premises used: WCovBy.le
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
inst : Preorder α
inst_1 : LocallyFiniteOrder α
x y b c : α
h : TransGen (fun (x1 x2 : α) ↦ x1 ⩿ x2) x b
h₁ : b ⩿ c
h₂ : x ≤ b
⊢ x ≤ c

Tactic:
h₂.trans h₁.le

Premises used: LE.le.trans, WCovBy.le
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
inst : Preorder α
inst_1 : LocallyFiniteOrder α
x y b c : α
h : TransGen (fun (x1 x2 : α) ↦ x1 ⩿ x2) x b
h₁ : b ⩿ c
h₂ : x ≤ b
⊢ x ≤ c

Tactic:
exact h₂.trans h₁.le

Premises used: LE.le.trans, WCovBy.le
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
inst : Preorder α
inst_1 : LocallyFiniteOrder α
x y : α
h : TransGen (fun (x1 x2 : α) ↦ x1 ⩿ x2) x y
single : ∀ {b : α} (h : x ⩿ b), x ≤ b
tail : ∀ {b c : α}, TransGen (fun (x1 x2 : α) ↦ x1 ⩿ x2) x b → ∀ (h₁ : b ⩿ c) (h₂ : x ≤ b), x ≤ c
⊢ x ≤ y

Tactic:
induction h with
  | single h => exact h.le
  | tail _ h₁ h₂ => exact h₂.trans h₁.le
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
inst : PartialOrder α
inst_1 : LocallyFiniteOrder α
x y : α
rw : TransGen (fun (x1 x2 : α) ↦ x1 ⩿ x2) x y ↔ ReflTransGen (fun (x1 x2 : α) ↦ x1 ⋖ x2) x y
rw₁ : TransGen (ReflGen fun (x1 x2 : α) ↦ x1 ⋖ x2) x y ↔ ReflTransGen (fun (x1 x2 : α) ↦ x1 ⋖ x2) x y
rw₂ rw₃ : ReflTransGen (fun (x1 x2 : α) ↦ x1 ⋖ x2) x y ↔ ReflTransGen (fun (x1 x2 : α) ↦ x1 ⋖ x2) x y
⊢ x ≤ y ↔ ReflTransGen (fun (x1 x2 : α) ↦ x1 ⋖ x2) x y

Tactic:
rw [le_iff_transGen_wcovBy, wcovBy_eq_reflGen_covBy, transGen_reflGen]

Premises used: le_iff_transGen_wcovBy, Relation.transGen_reflGen, wcovBy_eq_reflGen_covBy
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
inst : Preorder α
inst_1 : LocallyFiniteOrder α
x y : α
hxy : x < y
obtain :
  ∀ (z : α) (hxz : x ≤ z) (hz : Maximal (fun (x_1 : α) ↦ x_1 ∈ Set.Ico x y) z), TransGen (fun (x1 x2 : α) ↦ x1 ⋖ x2) x y
⊢ TransGen (fun (x1 x2 : α) ↦ x1 ⋖ x2) x y

Tactic:
obtain ⟨z, hxz, hz⟩ := (Set.finite_Ico x y).exists_le_maximal <| Set.left_mem_Ico.2 hxy

Premises used: Iff.mpr, Set.left_mem_Ico, Set.Finite.exists_le_maximal, Set.finite_Ico
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
inst : Preorder α
inst_1 : LocallyFiniteOrder α
x y : α
hxy : x < y
z : α
hxz : x ≤ z
hz : Maximal (fun (x_1 : α) ↦ x_1 ∈ Set.Ico x y) z
⊢ #(Ico x z) < #(Ico x y)

Tactic:
have z_card : #(Ico x z) < #(Ico x y) := card_lt_card <| ssubset_iff_of_subset
    (Ico_subset_Ico_right hz.1.2.le) |>.mpr ⟨z, mem_Ico.2 hz.1, right_notMem_Ico⟩
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
inst : Preorder α
inst_1 : LocallyFiniteOrder α
x y : α
hxy : x < y
z : α
hxz : x ≤ z
hz : Maximal (fun (x_1 : α) ↦ x_1 ∈ Set.Ico x y) z
z_card : #(Ico x z) < #(Ico x y)
⊢ z ⋖ y

Tactic:
have hzy : z ⋖ y :=
    ⟨hz.1.2, fun c hc hcy ↦ hc.not_ge <| hz.2 (⟨(hz.1.1.trans_lt hc).le, hcy⟩) hc.le⟩
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
inst : Preorder α
inst_1 : LocallyFiniteOrder α
x y : α
hxy : x < y
z : α
hxz : x ≤ z
hz : Maximal (fun (x_1 : α) ↦ x_1 ∈ Set.Ico x y) z
z_card : #(Ico x z) < #(Ico x y)
hzy : z ⋖ y
pos : ∀ (hxz : x < z), TransGen (fun (x1 x2 : α) ↦ x1 ⋖ x2) x y
neg : ∀ (hxz : ¬x < z), TransGen (fun (x1 x2 : α) ↦ x1 ⋖ x2) x y
⊢ TransGen (fun (x1 x2 : α) ↦ x1 ⋖ x2) x y

Tactic:
by_cases hxz : x < z
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
inst : Preorder α
inst_1 : LocallyFiniteOrder α
x y : α
hxy : x < y
z : α
hxz_1 : x ≤ z
hz : Maximal (fun (x_1 : α) ↦ x_1 ∈ Set.Ico x y) z
z_card : #(Ico x z) < #(Ico x y)
hzy : z ⋖ y
hxz : x < z
⊢ TransGen (fun (x1 x2 : α) ↦ x1 ⋖ x2) x y

Tactic:
.tail (transGen_covBy_of_lt hxz) hzy

Premises used: Relation.TransGen.tail
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
inst : Preorder α
inst_1 : LocallyFiniteOrder α
x y : α
hxy : x < y
z : α
hxz_1 : x ≤ z
hz : Maximal (fun (x_1 : α) ↦ x_1 ∈ Set.Ico x y) z
z_card : #(Ico x z) < #(Ico x y)
hzy : z ⋖ y
hxz : x < z
⊢ TransGen (fun (x1 x2 : α) ↦ x1 ⋖ x2) x y

Tactic:
exact .tail (transGen_covBy_of_lt hxz) hzy
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
inst : Preorder α
inst_1 : LocallyFiniteOrder α
x y : α
hxy : x < y
z : α
hxz_1 : x ≤ z
hz : Maximal (fun (x_1 : α) ↦ x_1 ∈ Set.Ico x y) z
z_card : #(Ico x z) < #(Ico x y)
hzy : z ⋖ y
hxz : ¬x < z
⊢ x ≤ z → z ≤ x

Tactic:
simp only [lt_iff_le_not_ge, not_and, not_not] at hxz

Premises used: Classical.not_not, lt_iff_le_not_ge, not_and
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
inst : Preorder α
inst_1 : LocallyFiniteOrder α
x y : α
hxy : x < y
z : α
hxz_1 : x ≤ z
hz : Maximal (fun (x_1 : α) ↦ x_1 ∈ Set.Ico x y) z
z_card : #(Ico x z) < #(Ico x y)
hzy : z ⋖ y
hxz : x ≤ z → z ≤ x
⊢ TransGen (fun (x1 x2 : α) ↦ x1 ⋖ x2) x y

Tactic:
.single (hzy.of_le_of_lt (hxz hz.1.1) hxy)

Premises used: And.left, Relation.TransGen.single, CovBy.of_le_of_lt
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
inst : Preorder α
inst_1 : LocallyFiniteOrder α
x y : α
hxy : x < y
z : α
hxz_1 : x ≤ z
hz : Maximal (fun (x_1 : α) ↦ x_1 ∈ Set.Ico x y) z
z_card : #(Ico x z) < #(Ico x y)
hzy : z ⋖ y
hxz : x ≤ z → z ≤ x
⊢ TransGen (fun (x1 x2 : α) ↦ x1 ⋖ x2) x y

Tactic:
exact .single (hzy.of_le_of_lt (hxz hz.1.1) hxy)
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
inst : Preorder α
inst_1 : LocallyFiniteOrder α
x y : α
⊢ x < y ↔ TransGen (fun (x1 x2 : α) ↦ x1 ⋖ x2) x y

Tactic:
⟨transGen_covBy_of_lt, fun h ↦ ?_⟩

Premises used: transGen_covBy_of_lt, Iff.intro
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
inst : Preorder α
inst_1 : LocallyFiniteOrder α
x y : α
refine : ∀ (h : TransGen (fun (x1 x2 : α) ↦ x1 ⋖ x2) x y), x < y
⊢ x < y ↔ TransGen (fun (x1 x2 : α) ↦ x1 ⋖ x2) x y

Tactic:
refine ⟨transGen_covBy_of_lt, fun h ↦ ?_⟩
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
inst : Preorder α
inst_1 : LocallyFiniteOrder α
x y b : α
hx : x ⋖ b
⊢ x < b

Tactic:
hx.1

Premises used: And.left
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
inst : Preorder α
inst_1 : LocallyFiniteOrder α
x y b : α
hx : x ⋖ b
⊢ x < b

Tactic:
exact hx.1

Premises used: And.left
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
inst : Preorder α
inst_1 : LocallyFiniteOrder α
x y b c : α
h : TransGen (fun (x1 x2 : α) ↦ x1 ⋖ x2) x b
hb : b ⋖ c
ih : x < b
⊢ x < c

Tactic:
ih.trans hb.1

Premises used: And.left, LT.lt.trans
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
inst : Preorder α
inst_1 : LocallyFiniteOrder α
x y b c : α
h : TransGen (fun (x1 x2 : α) ↦ x1 ⋖ x2) x b
hb : b ⋖ c
ih : x < b
⊢ x < c

Tactic:
exact ih.trans hb.1

Premises used: And.left, LT.lt.trans
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
inst : Preorder α
inst_1 : LocallyFiniteOrder α
x y : α
h : TransGen (fun (x1 x2 : α) ↦ x1 ⋖ x2) x y
single : ∀ {b : α} (hx : x ⋖ b), x < b
tail : ∀ {b c : α}, TransGen (fun (x1 x2 : α) ↦ x1 ⋖ x2) x b → ∀ (hb : b ⋖ c) (ih : x < b), x < c
⊢ x < y

Tactic:
induction h with
  | single hx => exact hx.1
  | tail _ hb ih => exact ih.trans hb.1
-- Module: Mathlib.Order.Interval.Finset.Basic
Goal:
α : Type u_2
β : Type u_3
inst : Preorder α
inst_1 : LocallyFiniteOrder α
inst_2 : Preorder β
f : α → β
⊢ Monotone f ↔ ∀ (a b : α), a ⩿ b → f a ≤ f b

Tactic:
⟨fun hf _ _ h ↦ hf h.le, fun h a b hab ↦ ?_⟩

Premises used: Iff.intro, WCovBy.le