awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Order.Basic (goal)
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst : LinearOrder β
inst_1 : LE α
inst_2 : LT α
inst_3 : Max α
inst_4 : Min α
inst_5 : Ord α
inst_6 : DecidableEq α
inst_7 : DecidableLE α
inst_8 : DecidableLT α
f : α → β
hf : Injective f
le : ∀ {x y : α}, f x ≤ f y ↔ x ≤ y
lt : ∀ {x y : α}, f x < f y ↔ x < y
min : ∀ (x y : α), f (x ⊓ y) = Min.min (f x) (f y)
max : ∀ (x y : α), f (x ⊔ y) = Max.max (f x) (f y)
compare : ∀ (x y : α), Ord.compare (f x) (f y) = Ord.compare x y
x x_1 : α
simp_rw : f (x ⊓ x_1) = f (if x ≤ x_1 then x else x_1)
simp_rw₁ : f (x ⊓ x_1) = f (if f x ≤ f x_1 then x else x_1)
⊢ x ⊓ x_1 = if x ≤ x_1 then x else x_1
have simp_rw₂ : f (x ⊓ x_1) = if f x ≤ f x_1 then f x else f x_1
Tactic: simp_rw [← hf.eq_iff, ← le, apply_ite f, ← min_def, min]
-- Lean 4 proof step from Mathlib.Order.Basic (goal)
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst : LinearOrder β
inst_1 : LE α
inst_2 : LT α
inst_3 : Max α
inst_4 : Min α
inst_5 : Ord α
inst_6 : DecidableEq α
inst_7 : DecidableLE α
inst_8 : DecidableLT α
f : α → β
hf : Injective f
le : ∀ {x y : α}, f x ≤ f y ↔ x ≤ y
lt : ∀ {x y : α}, f x < f y ↔ x < y
min : ∀ (x y : α), f (x ⊓ y) = Min.min (f x) (f y)
max : ∀ (x y : α), f (x ⊔ y) = Max.max (f x) (f y)
compare : ∀ (x y : α), Ord.compare (f x) (f y) = Ord.compare x y
x x_1 : α
simp_rw : f (x ⊓ x_1) = f (if x ≤ x_1 then x else x_1)
simp_rw₁ : f (x ⊓ x_1) = f (if f x ≤ f x_1 then x else x_1)
simp_rw₂ : f (x ⊓ x_1) = if f x ≤ f x_1 then f x else f x_1
⊢ x ⊓ x_1 = if x ≤ x_1 then x else x_1
have simp_rw₃ : f (x ⊓ x_1) = Min.min (f x) (f x_1)
Tactic: simp_rw [← hf.eq_iff, ← le, apply_ite f, ← min_def, min]
-- Lean 4 proof step from Mathlib.Order.Basic (goal)
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst : LinearOrder β
inst_1 : LE α
inst_2 : LT α
inst_3 : Max α
inst_4 : Min α
inst_5 : Ord α
inst_6 : DecidableEq α
inst_7 : DecidableLE α
inst_8 : DecidableLT α
f : α → β
hf : Injective f
le : ∀ {x y : α}, f x ≤ f y ↔ x ≤ y
lt : ∀ {x y : α}, f x < f y ↔ x < y
min : ∀ (x y : α), f (x ⊓ y) = Min.min (f x) (f y)
max : ∀ (x y : α), f (x ⊔ y) = Max.max (f x) (f y)
compare : ∀ (x y : α), Ord.compare (f x) (f y) = Ord.compare x y
x x_1 : α
⊢ x ⊔ x_1 = if x ≤ x_1 then x_1 else x
have simp_rw : f (x ⊔ x_1) = f (if x ≤ x_1 then x_1 else x)
Tactic: simp_rw [← hf.eq_iff, ← le, apply_ite f, ← max_def, max]
-- Lean 4 proof step from Mathlib.Order.Basic (goal)
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst : LinearOrder β
inst_1 : LE α
inst_2 : LT α
inst_3 : Max α
inst_4 : Min α
inst_5 : Ord α
inst_6 : DecidableEq α
inst_7 : DecidableLE α
inst_8 : DecidableLT α
f : α → β
hf : Injective f
le : ∀ {x y : α}, f x ≤ f y ↔ x ≤ y
lt : ∀ {x y : α}, f x < f y ↔ x < y
min : ∀ (x y : α), f (x ⊓ y) = Min.min (f x) (f y)
max : ∀ (x y : α), f (x ⊔ y) = Max.max (f x) (f y)
compare : ∀ (x y : α), Ord.compare (f x) (f y) = Ord.compare x y
x x_1 : α
simp_rw : f (x ⊔ x_1) = f (if x ≤ x_1 then x_1 else x)
⊢ x ⊔ x_1 = if x ≤ x_1 then x_1 else x
have simp_rw₁ : f (x ⊔ x_1) = f (if f x ≤ f x_1 then x_1 else x)
Tactic: simp_rw [← hf.eq_iff, ← le, apply_ite f, ← max_def, max]
-- Lean 4 proof step from Mathlib.Order.Basic (goal)
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst : LinearOrder β
inst_1 : LE α
inst_2 : LT α
inst_3 : Max α
inst_4 : Min α
inst_5 : Ord α
inst_6 : DecidableEq α
inst_7 : DecidableLE α
inst_8 : DecidableLT α
f : α → β
hf : Injective f
le : ∀ {x y : α}, f x ≤ f y ↔ x ≤ y
lt : ∀ {x y : α}, f x < f y ↔ x < y
min : ∀ (x y : α), f (x ⊓ y) = Min.min (f x) (f y)
max : ∀ (x y : α), f (x ⊔ y) = Max.max (f x) (f y)
compare : ∀ (x y : α), Ord.compare (f x) (f y) = Ord.compare x y
x x_1 : α
simp_rw : f (x ⊔ x_1) = f (if x ≤ x_1 then x_1 else x)
simp_rw₁ : f (x ⊔ x_1) = f (if f x ≤ f x_1 then x_1 else x)
⊢ x ⊔ x_1 = if x ≤ x_1 then x_1 else x
have simp_rw₂ : f (x ⊔ x_1) = if f x ≤ f x_1 then f x_1 else f x
Tactic: simp_rw [← hf.eq_iff, ← le, apply_ite f, ← max_def, max]
-- Lean 4 proof step from Mathlib.Order.Basic (goal)
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst : LinearOrder β
inst_1 : LE α
inst_2 : LT α
inst_3 : Max α
inst_4 : Min α
inst_5 : Ord α
inst_6 : DecidableEq α
inst_7 : DecidableLE α
inst_8 : DecidableLT α
f : α → β
hf : Injective f
le : ∀ {x y : α}, f x ≤ f y ↔ x ≤ y
lt : ∀ {x y : α}, f x < f y ↔ x < y
min : ∀ (x y : α), f (x ⊓ y) = Min.min (f x) (f y)
max : ∀ (x y : α), f (x ⊔ y) = Max.max (f x) (f y)
compare : ∀ (x y : α), Ord.compare (f x) (f y) = Ord.compare x y
x x_1 : α
simp_rw : f (x ⊔ x_1) = f (if x ≤ x_1 then x_1 else x)
simp_rw₁ : f (x ⊔ x_1) = f (if f x ≤ f x_1 then x_1 else x)
simp_rw₂ : f (x ⊔ x_1) = if f x ≤ f x_1 then f x_1 else f x
⊢ x ⊔ x_1 = if x ≤ x_1 then x_1 else x
have simp_rw₃ : f (x ⊔ x_1) = Max.max (f x) (f x_1)
Tactic: simp_rw [← hf.eq_iff, ← le, apply_ite f, ← max_def, max]
-- Lean 4 proof step from Mathlib.Order.Basic (goal)
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst : LinearOrder β
inst_1 : LE α
inst_2 : LT α
inst_3 : Max α
inst_4 : Min α
inst_5 : Ord α
inst_6 : DecidableEq α
inst_7 : DecidableLE α
inst_8 : DecidableLT α
f : α → β
hf : Injective f
le : ∀ {x y : α}, f x ≤ f y ↔ x ≤ y
lt : ∀ {x y : α}, f x < f y ↔ x < y
min : ∀ (x y : α), f (x ⊓ y) = Min.min (f x) (f y)
max : ∀ (x y : α), f (x ⊔ y) = Max.max (f x) (f y)
compare : ∀ (x y : α), Ord.compare (f x) (f y) = Ord.compare x y
x x_1 : α
⊢ Ord.compare x x_1 = compareOfLessAndEq x x_1
have simp_rw : Ord.compare (f x) (f x_1) = compareOfLessAndEq x x_1
Tactic: simp_rw [← compare, LinearOrder.compare_eq_compareOfLessAndEq, compareOfLessAndEq, ← lt,
      hf.eq_iff]
-- Lean 4 proof step from Mathlib.Order.Basic (goal)
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst : LinearOrder β
inst_1 : LE α
inst_2 : LT α
inst_3 : Max α
inst_4 : Min α
inst_5 : Ord α
inst_6 : DecidableEq α
inst_7 : DecidableLE α
inst_8 : DecidableLT α
f : α → β
hf : Injective f
le : ∀ {x y : α}, f x ≤ f y ↔ x ≤ y
lt : ∀ {x y : α}, f x < f y ↔ x < y
min : ∀ (x y : α), f (x ⊓ y) = Min.min (f x) (f y)
max : ∀ (x y : α), f (x ⊔ y) = Max.max (f x) (f y)
compare : ∀ (x y : α), Ord.compare (f x) (f y) = Ord.compare x y
x x_1 : α
simp_rw : Ord.compare (f x) (f x_1) = compareOfLessAndEq x x_1
⊢ Ord.compare x x_1 = compareOfLessAndEq x x_1
have simp_rw₁ : compareOfLessAndEq (f x) (f x_1) = compareOfLessAndEq x x_1
Tactic: simp_rw [← compare, LinearOrder.compare_eq_compareOfLessAndEq, compareOfLessAndEq, ← lt,
      hf.eq_iff]
-- Lean 4 proof step from Mathlib.Order.Basic (goal)
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst : LinearOrder β
inst_1 : LE α
inst_2 : LT α
inst_3 : Max α
inst_4 : Min α
inst_5 : Ord α
inst_6 : DecidableEq α
inst_7 : DecidableLE α
inst_8 : DecidableLT α
f : α → β
hf : Injective f
le : ∀ {x y : α}, f x ≤ f y ↔ x ≤ y
lt : ∀ {x y : α}, f x < f y ↔ x < y
min : ∀ (x y : α), f (x ⊓ y) = Min.min (f x) (f y)
max : ∀ (x y : α), f (x ⊔ y) = Max.max (f x) (f y)
compare : ∀ (x y : α), Ord.compare (f x) (f y) = Ord.compare x y
x x_1 : α
simp_rw : Ord.compare (f x) (f x_1) = compareOfLessAndEq x x_1
simp_rw₁ : compareOfLessAndEq (f x) (f x_1) = compareOfLessAndEq x x_1
⊢ Ord.compare x x_1 = compareOfLessAndEq x x_1
have simp_rw₂ : (if f x < f x_1 then Ordering.lt else if f x = f x_1 then Ordering.eq else Ordering.gt) =
  if x < x_1 then Ordering.lt else if x = x_1 then Ordering.eq else Ordering.gt
Tactic: simp_rw [← compare, LinearOrder.compare_eq_compareOfLessAndEq, compareOfLessAndEq, ← lt,
      hf.eq_iff]
-- Lean 4 proof step from Mathlib.Order.Basic (goal)
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst : LinearOrder β
inst_1 : LE α
inst_2 : LT α
inst_3 : Max α
inst_4 : Min α
inst_5 : Ord α
inst_6 : DecidableEq α
inst_7 : DecidableLE α
inst_8 : DecidableLT α
f : α → β
hf : Injective f
le : ∀ {x y : α}, f x ≤ f y ↔ x ≤ y
lt : ∀ {x y : α}, f x < f y ↔ x < y
min : ∀ (x y : α), f (x ⊓ y) = Min.min (f x) (f y)
max : ∀ (x y : α), f (x ⊔ y) = Max.max (f x) (f y)
compare : ∀ (x y : α), Ord.compare (f x) (f y) = Ord.compare x y
x x_1 : α
simp_rw : Ord.compare (f x) (f x_1) = compareOfLessAndEq x x_1
simp_rw₁ : compareOfLessAndEq (f x) (f x_1) = compareOfLessAndEq x x_1
simp_rw₂ :
  (if f x < f x_1 then Ordering.lt else if f x = f x_1 then Ordering.eq else Ordering.gt) =
    if x < x_1 then Ordering.lt else if x = x_1 then Ordering.eq else Ordering.gt
⊢ Ord.compare x x_1 = compareOfLessAndEq x x_1
have simp_rw₃ : (if f x < f x_1 then Ordering.lt else if f x = f x_1 then Ordering.eq else Ordering.gt) =
  if f x < f x_1 then Ordering.lt else if x = x_1 then Ordering.eq else Ordering.gt
Tactic: simp_rw [← compare, LinearOrder.compare_eq_compareOfLessAndEq, compareOfLessAndEq, ← lt,
      hf.eq_iff]
-- Lean 4 proof step from Mathlib.Order.Basic (hypothesis)
Goal:
α : Type u_2
β : Type u_3
a b : α
inst : LinearOrder β
inst_1 : DecidableEq α
f : α → β
inj : Injective f
inst_2 : Decidable (a < b)
⊢ compare (f a) (f b) = compareOfLessAndEq a b
have h : compare (f a) (f b) = compareOfLessAndEq (f a) (f b)
Tactic: have h := LinearOrder.compare_eq_compareOfLessAndEq (f a) (f b)
-- Lean 4 proof step from Mathlib.Order.Basic (goal)
Goal:
α : Type u_2
β : Type u_3
a b : α
inst : LinearOrder β
inst_1 : DecidableEq α
f : α → β
inj : Injective f
inst_2 : Decidable (a < b)
h : compare (f a) (f b) = compareOfLessAndEq (f a) (f b)
⊢ compare (f a) (f b) = compareOfLessAndEq a b
have simp : (if f a < f b then Ordering.lt else if f a = f b then Ordering.eq else Ordering.gt) =
  if a < b then Ordering.lt else if a = b then Ordering.eq else Ordering.gt
Tactic: simp only [h, compareOfLessAndEq]
-- Lean 4 proof step from Mathlib.Order.Basic (goal)
Goal:
α : Type u_2
β : Type u_3
a b : α
inst : LinearOrder β
inst_1 : DecidableEq α
f : α → β
inj : Injective f
inst_2 : Decidable (a < b)
h : compare (f a) (f b) = compareOfLessAndEq (f a) (f b)
⊢ (if f a < f b then Ordering.lt else if f a = f b then Ordering.eq else Ordering.gt) =
    if a < b then Ordering.lt else if a = b then Ordering.eq else Ordering.gt
have pos : f a < f b → a < b → Ordering.lt = Ordering.lt
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Order.Basic (goal)
Goal:
α : Type u_2
β : Type u_3
a b : α
inst : LinearOrder β
inst_1 : DecidableEq α
f : α → β
inj : Injective f
inst_2 : Decidable (a < b)
h : compare (f a) (f b) = compareOfLessAndEq (f a) (f b)
pos : f a < f b → a < b → Ordering.lt = Ordering.lt
⊢ (if f a < f b then Ordering.lt else if f a = f b then Ordering.eq else Ordering.gt) =
    if a < b then Ordering.lt else if a = b then Ordering.eq else Ordering.gt
have pos₁ : f a < f b → ¬a < b → a = b → False
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Order.Basic (goal)
Goal:
α : Type u_2
β : Type u_3
a b : α
inst : LinearOrder β
inst_1 : DecidableEq α
f : α → β
inj : Injective f
inst_2 : Decidable (a < b)
h : compare (f a) (f b) = compareOfLessAndEq (f a) (f b)
pos : f a < f b → a < b → Ordering.lt = Ordering.lt
pos₁ : f a < f b → ¬a < b → a = b → False
⊢ (if f a < f b then Ordering.lt else if f a = f b then Ordering.eq else Ordering.gt) =
    if a < b then Ordering.lt else if a = b then Ordering.eq else Ordering.gt
have neg : f a < f b → ¬a < b → ¬a = b → False
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Order.Basic (goal)
Goal:
α : Type u_2
β : Type u_3
a b : α
inst : LinearOrder β
inst_1 : DecidableEq α
f : α → β
inj : Injective f
inst_2 : Decidable (a < b)
h : compare (f a) (f b) = compareOfLessAndEq (f a) (f b)
pos : f a < f b → a < b → Ordering.lt = Ordering.lt
pos₁ : f a < f b → ¬a < b → a = b → False
neg : f a < f b → ¬a < b → ¬a = b → False
⊢ (if f a < f b then Ordering.lt else if f a = f b then Ordering.eq else Ordering.gt) =
    if a < b then Ordering.lt else if a = b then Ordering.eq else Ordering.gt
have pos₂ : ¬f a < f b → f a = f b → a < b → False
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Order.Basic (goal)
Goal:
α : Type u_2
β : Type u_3
a b : α
inst : LinearOrder β
inst_1 : DecidableEq α
f : α → β
inj : Injective f
inst_2 : Decidable (a < b)
h : compare (f a) (f b) = compareOfLessAndEq (f a) (f b)
pos : f a < f b → a < b → Ordering.lt = Ordering.lt
pos₁ : f a < f b → ¬a < b → a = b → False
neg : f a < f b → ¬a < b → ¬a = b → False
pos₂ : ¬f a < f b → f a = f b → a < b → False
⊢ (if f a < f b then Ordering.lt else if f a = f b then Ordering.eq else Ordering.gt) =
    if a < b then Ordering.lt else if a = b then Ordering.eq else Ordering.gt
have pos₃ : ¬f a < f b → f a = f b → ¬a < b → a = b → Ordering.eq = Ordering.eq
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Order.Basic (goal)
Goal:
α : Type u_2
β : Type u_3
a b : α
inst : LinearOrder β
inst_1 : DecidableEq α
f : α → β
inj : Injective f
inst_2 : Decidable (a < b)
h : compare (f a) (f b) = compareOfLessAndEq (f a) (f b)
pos : f a < f b → a < b → Ordering.lt = Ordering.lt
pos₁ : f a < f b → ¬a < b → a = b → False
neg : f a < f b → ¬a < b → ¬a = b → False
pos₂ : ¬f a < f b → f a = f b → a < b → False
pos₃ : ¬f a < f b → f a = f b → ¬a < b → a = b → Ordering.eq = Ordering.eq
⊢ (if f a < f b then Ordering.lt else if f a = f b then Ordering.eq else Ordering.gt) =
    if a < b then Ordering.lt else if a = b then Ordering.eq else Ordering.gt
have neg₁ : ¬f a < f b → f a = f b → ¬a < b → ¬a = b → False
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Order.Basic (goal)
Goal:
α : Type u_2
β : Type u_3
a b : α
inst : LinearOrder β
inst_1 : DecidableEq α
f : α → β
inj : Injective f
inst_2 : Decidable (a < b)
h : compare (f a) (f b) = compareOfLessAndEq (f a) (f b)
pos : f a < f b → a < b → Ordering.lt = Ordering.lt
pos₁ : f a < f b → ¬a < b → a = b → False
neg : f a < f b → ¬a < b → ¬a = b → False
pos₂ : ¬f a < f b → f a = f b → a < b → False
pos₃ : ¬f a < f b → f a = f b → ¬a < b → a = b → Ordering.eq = Ordering.eq
neg₁ : ¬f a < f b → f a = f b → ¬a < b → ¬a = b → False
⊢ (if f a < f b then Ordering.lt else if f a = f b then Ordering.eq else Ordering.gt) =
    if a < b then Ordering.lt else if a = b then Ordering.eq else Ordering.gt
have pos₄ : ¬f a < f b → ¬f a = f b → a < b → False
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Order.Basic (goal)
Goal:
α : Type u_2
β : Type u_3
a b : α
inst : LinearOrder β
inst_1 : DecidableEq α
f : α → β
inj : Injective f
inst_2 : Decidable (a < b)
h : compare (f a) (f b) = compareOfLessAndEq (f a) (f b)
pos : f a < f b → a < b → Ordering.lt = Ordering.lt
pos₁ : f a < f b → ¬a < b → a = b → False
neg : f a < f b → ¬a < b → ¬a = b → False
pos₂ : ¬f a < f b → f a = f b → a < b → False
pos₃ : ¬f a < f b → f a = f b → ¬a < b → a = b → Ordering.eq = Ordering.eq
neg₁ : ¬f a < f b → f a = f b → ¬a < b → ¬a = b → False
pos₄ : ¬f a < f b → ¬f a = f b → a < b → False
⊢ (if f a < f b then Ordering.lt else if f a = f b then Ordering.eq else Ordering.gt) =
    if a < b then Ordering.lt else if a = b then Ordering.eq else Ordering.gt
have pos₅ : ¬f a < f b → ¬f a = f b → ¬a < b → a = b → False
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Order.Basic (goal)
Goal:
α : Type u_2
β : Type u_3
a b : α
inst : LinearOrder β
inst_1 : DecidableEq α
f : α → β
inj : Injective f
inst_2 : Decidable (a < b)
h : compare (f a) (f b) = compareOfLessAndEq (f a) (f b)
pos : f a < f b → a < b → Ordering.lt = Ordering.lt
pos₁ : f a < f b → ¬a < b → a = b → False
neg : f a < f b → ¬a < b → ¬a = b → False
pos₂ : ¬f a < f b → f a = f b → a < b → False
pos₃ : ¬f a < f b → f a = f b → ¬a < b → a = b → Ordering.eq = Ordering.eq
neg₁ : ¬f a < f b → f a = f b → ¬a < b → ¬a = b → False
pos₄ : ¬f a < f b → ¬f a = f b → a < b → False
pos₅ : ¬f a < f b → ¬f a = f b → ¬a < b → a = b → False
⊢ (if f a < f b then Ordering.lt else if f a = f b then Ordering.eq else Ordering.gt) =
    if a < b then Ordering.lt else if a = b then Ordering.eq else Ordering.gt
have neg₂ : ¬f a < f b → ¬f a = f b → ¬a < b → ¬a = b → Ordering.gt = Ordering.gt
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Order.Basic (hypothesis)
Goal:
α : Type u_2
β : Type u_3
a b : α
inst : LinearOrder β
inst_1 : DecidableEq α
f : α → β
inj : Injective f
inst_2 : Decidable (a < b)
h : compare (f a) (f b) = compareOfLessAndEq (f a) (f b)
h_1 : ¬f a < f b
h_2 : f a = f b
h_3 : ¬a < b
h_4 : ¬a = b
⊢ False
have this : ¬f a = f b
Tactic: have : ¬ f a = f b := by rename_i h; exact inj.ne h
-- Lean 4 proof step from Mathlib.Order.Basic (goal)
Goal:
α : Type u_2
β : Type u_3
inst : Preorder α
inst_1 : Preorder β
a : α
b : β
x : α × β
⊢ x.swap < (b, a) ↔ x < (a, b)
have rw : x.swap.swap < (b, a).swap ↔ x < (a, b)
Tactic: rw [← swap_lt_swap]
-- Lean 4 proof step from Mathlib.Order.Basic (goal)
Goal:
α : Type u_2
β : Type u_3
inst : Preorder α
inst_1 : Preorder β
x y : α × β
⊢ x < y ↔ x.fst < y.fst ∧ x.snd ≤ y.snd ∨ x.fst ≤ y.fst ∧ x.snd < y.snd
have refine_1 : ∀ (h : x < y), x.fst < y.fst ∧ x.snd ≤ y.snd ∨ x.fst ≤ y.fst ∧ x.snd < y.snd
Tactic: refine ⟨fun h ↦ ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Order.Basic (goal)
Goal:
α : Type u_2
β : Type u_3
inst : Preorder α
inst_1 : Preorder β
x y : α × β
refine_1 : ∀ (h : x < y), x.fst < y.fst ∧ x.snd ≤ y.snd ∨ x.fst ≤ y.fst ∧ x.snd < y.snd
⊢ x < y ↔ x.fst < y.fst ∧ x.snd ≤ y.snd ∨ x.fst ≤ y.fst ∧ x.snd < y.snd
have refine_2 : x.fst < y.fst ∧ x.snd ≤ y.snd ∨ x.fst ≤ y.fst ∧ x.snd < y.snd → x < y
Tactic: refine ⟨fun h ↦ ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Order.Basic (goal)
Goal:
α : Type u_2
β : Type u_3
inst : Preorder α
inst_1 : Preorder β
x y : α × β
h : x < y
⊢ x.fst < y.fst ∧ x.snd ≤ y.snd ∨ x.fst ≤ y.fst ∧ x.snd < y.snd
have pos : ∀ (h₁ : y.fst ≤ x.fst), x.fst < y.fst ∧ x.snd ≤ y.snd ∨ x.fst ≤ y.fst ∧ x.snd < y.snd
Tactic: by_cases h₁ : y.1 ≤ x.1
-- Lean 4 proof step from Mathlib.Order.Basic (goal)
Goal:
α : Type u_2
β : Type u_3
inst : Preorder α
inst_1 : Preorder β
x y : α × β
h : x < y
pos : ∀ (h₁ : y.fst ≤ x.fst), x.fst < y.fst ∧ x.snd ≤ y.snd ∨ x.fst ≤ y.fst ∧ x.snd < y.snd
⊢ x.fst < y.fst ∧ x.snd ≤ y.snd ∨ x.fst ≤ y.fst ∧ x.snd < y.snd
have neg : ∀ (h₁ : ¬y.fst ≤ x.fst), x.fst < y.fst ∧ x.snd ≤ y.snd ∨ x.fst ≤ y.fst ∧ x.snd < y.snd
Tactic: by_cases h₁ : y.1 ≤ x.1
-- Lean 4 proof step from Mathlib.Order.Basic (goal)
Goal:
α : Type u_2
inst : LT α
inst_1 : DenselyOrdered α
⊢ ∀ (a₁ a₂ : α), a₁ < a₂ → ∃ (a : α), a < a₂ ∧ a₁ < a
have simp_rw : ∀ (a₁ a₂ : α), a₁ < a₂ → ∃ (a : α), a₁ < a ∧ a < a₂
Tactic: simp_rw [and_comm]
-- Lean 4 proof step from Mathlib.Order.Basic (goal)
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst : Preorder α
inst_1 : Preorder β
inst_2 : DenselyOrdered α
inst_3 : DenselyOrdered β
a b : α × β
⊢ a < b → ∃ (a_2 : α × β), a < a_2 ∧ a_2 < b
have simp_rw : a.fst < b.fst ∧ a.snd ≤ b.snd ∨ a.fst ≤ b.fst ∧ a.snd < b.snd →
  ∃ (a_2 : α × β),
    (a.fst < a_2.fst ∧ a.snd ≤ a_2.snd ∨ a.fst ≤ a_2.fst ∧ a.snd < a_2.snd) ∧
      (a_2.fst < b.fst ∧ a_2.snd ≤ b.snd ∨ a_2.fst ≤ b.fst ∧ a_2.snd < b.snd)
Tactic: simp_rw [Prod.lt_iff]
-- Lean 4 proof step from Mathlib.Order.Basic (goal)
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst : Preorder α
inst_1 : Preorder β
inst_2 : DenselyOrdered α
inst_3 : DenselyOrdered β
a b : α × β
h₁ : a.fst < b.fst
h₂ : a.snd ≤ b.snd
⊢ ∃ (a_1 : α × β),
    (a.fst < a_1.fst ∧ a.snd ≤ a_1.snd ∨ a.fst ≤ a_1.fst ∧ a.snd < a_1.snd) ∧
      (a_1.fst < b.fst ∧ a_1.snd ≤ b.snd ∨ a_1.fst ≤ b.fst ∧ a_1.snd < b.snd)
have inl : ∀ (c : α) (ha : a.fst < c) (hb : c < b.fst),
  ∃ (a_1 : α × β),
    (a.fst < a_1.fst ∧ a.snd ≤ a_1.snd ∨ a.fst ≤ a_1.fst ∧ a.snd < a_1.snd) ∧
      (a_1.fst < b.fst ∧ a_1.snd ≤ b.snd ∨ a_1.fst ≤ b.fst ∧ a_1.snd < b.snd)
Tactic: obtain ⟨c, ha, hb⟩ := exists_between h₁
-- Lean 4 proof step from Mathlib.Order.Basic (goal)
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst : Preorder α
inst_1 : Preorder β
inst_2 : DenselyOrdered α
inst_3 : DenselyOrdered β
a b : α × β
h₁ : a.fst ≤ b.fst
h₂ : a.snd < b.snd
⊢ ∃ (a_1 : α × β),
    (a.fst < a_1.fst ∧ a.snd ≤ a_1.snd ∨ a.fst ≤ a_1.fst ∧ a.snd < a_1.snd) ∧
      (a_1.fst < b.fst ∧ a_1.snd ≤ b.snd ∨ a_1.fst ≤ b.fst ∧ a_1.snd < b.snd)
have inr : ∀ (c : β) (ha : a.snd < c) (hb : c < b.snd),
  ∃ (a_1 : α × β),
    (a.fst < a_1.fst ∧ a.snd ≤ a_1.snd ∨ a.fst ≤ a_1.fst ∧ a.snd < a_1.snd) ∧
      (a_1.fst < b.fst ∧ a_1.snd ≤ b.snd ∨ a_1.fst ≤ b.fst ∧ a_1.snd < b.snd)
Tactic: obtain ⟨c, ha, hb⟩ := exists_between h₂
-- Lean 4 proof step from Mathlib.Order.Basic (goal)
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst : (i : ι) → Preorder (π i)
inst_1 : ∀ (i : ι), DenselyOrdered.{u_4} (π i)
a b : (i : ι) → π i
⊢ a < b → ∃ (a_2 : (i : ι) → π i), a < a_2 ∧ a_2 < b
have simp_rw : (a ≤ b ∧ ∃ (i : ι), a i < b i) →
  ∃ (a_2 : (i : ι) → π i), (a ≤ a_2 ∧ ∃ (i : ι), a i < a_2 i) ∧ a_2 ≤ b ∧ ∃ (i : ι), a_2 i < b i
Tactic: simp_rw [Pi.lt_def]
-- Lean 4 proof step from Mathlib.Order.Basic (goal)
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst : (i : ι) → Preorder (π i)
inst_1 : ∀ (i : ι), DenselyOrdered.{u_4} (π i)
a b : (i : ι) → π i
hab : a ≤ b
i : ι
hi : a i < b i
⊢ ∃ (a_1 : (i : ι) → π i), (a ≤ a_1 ∧ ∃ (i : ι), a i < a_1 i) ∧ a_1 ≤ b ∧ ∃ (i : ι), a_1 i < b i
have obtain : ∀ (c : π i) (ha : a i < c) (hb : c < b i),
  ∃ (a_1 : (i : ι) → π i), (a ≤ a_1 ∧ ∃ (i : ι), a i < a_1 i) ∧ a_1 ≤ b ∧ ∃ (i : ι), a_1 i < b i
Tactic: obtain ⟨c, ha, hb⟩ := exists_between hi
-- Lean 4 proof step from Mathlib.Order.Basic (goal)
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst : (i : ι) → Preorder (π i)
inst_1 : ∀ (i : ι), DenselyOrdered.{u_4} (π i)
a b : (i : ι) → π i
⊢ a < b → ∃ (a_2 : (i : ι) → π i), a < a_2 ∧ a_2 < b
have simp_rw : (a ≤ b ∧ ∃ (i : ι), a i < b i) →
  ∃ (a_2 : (i : ι) → π i), (a ≤ a_2 ∧ ∃ (i : ι), a i < a_2 i) ∧ a_2 ≤ b ∧ ∃ (i : ι), a_2 i < b i
Tactic: classical
      simp_rw [Pi.lt_def]
      rintro ⟨hab, i, hi⟩
      obtain ⟨c, ha, hb⟩ := exists_between hi
      exact
        ⟨Function.update a i c,
          ⟨le_update_iff.2 ⟨ha.le, fun _ _ ↦ le_rfl⟩, i, by rwa [update_self]⟩,
          update_le_iff.2 ⟨hb.le, fun _ _ ↦ hab _⟩, i, by rwa [update_self]⟩
-- Lean 4 proof step from Mathlib.Order.Basic (goal)
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst : (i : ι) → Preorder (π i)
inst_1 : ∀ (i : ι), DenselyOrdered.{u_4} (π i)
a b : (i : ι) → π i
simp_rw :
  (a ≤ b ∧ ∃ (i : ι), a i < b i) →
    ∃ (a_2 : (i : ι) → π i), (a ≤ a_2 ∧ ∃ (i : ι), a i < a_2 i) ∧ a_2 ≤ b ∧ ∃ (i : ι), a_2 i < b i
⊢ a < b → ∃ (a_2 : (i : ι) → π i), a < a_2 ∧ a_2 < b
have simp_rw₁ : ∀ (hab : a ≤ b) (i : ι) (hi : a i < b i),
  ∃ (a_1 : (i : ι) → π i), (a ≤ a_1 ∧ ∃ (i : ι), a i < a_1 i) ∧ a_1 ≤ b ∧ ∃ (i : ι), a_1 i < b i
Tactic: classical
      simp_rw [Pi.lt_def]
      rintro ⟨hab, i, hi⟩
      obtain ⟨c, ha, hb⟩ := exists_between hi
      exact
        ⟨Function.update a i c,
          ⟨le_update_iff.2 ⟨ha.le, fun _ _ ↦ le_rfl⟩, i, by rwa [update_self]⟩,
          update_le_iff.2 ⟨hb.le, fun _ _ ↦ hab _⟩, i, by rwa [update_self]⟩
-- Lean 4 proof step from Mathlib.Order.Basic (goal)
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst : (i : ι) → Preorder (π i)
inst_1 : ∀ (i : ι), DenselyOrdered.{u_4} (π i)
a b : (i : ι) → π i
simp_rw :
  (a ≤ b ∧ ∃ (i : ι), a i < b i) →
    ∃ (a_2 : (i : ι) → π i), (a ≤ a_2 ∧ ∃ (i : ι), a i < a_2 i) ∧ a_2 ≤ b ∧ ∃ (i : ι), a_2 i < b i
simp_rw₁ :
  ∀ (hab : a ≤ b) (i : ι) (hi : a i < b i),
    ∃ (a_1 : (i : ι) → π i), (a ≤ a_1 ∧ ∃ (i : ι), a i < a_1 i) ∧ a_1 ≤ b ∧ ∃ (i : ι), a_1 i < b i
⊢ a < b → ∃ (a_2 : (i : ι) → π i), a < a_2 ∧ a_2 < b
have simp_rw₂ : ∀ (hab : a ≤ b) (i : ι) (hi : a i < b i) (c : π i) (ha : a i < c) (hb : c < b i),
  ∃ (a_1 : (i : ι) → π i), (a ≤ a_1 ∧ ∃ (i : ι), a i < a_1 i) ∧ a_1 ≤ b ∧ ∃ (i : ι), a_1 i < b i
Tactic: classical
      simp_rw [Pi.lt_def]
      rintro ⟨hab, i, hi⟩
      obtain ⟨c, ha, hb⟩ := exists_between hi
      exact
        ⟨Function.update a i c,
          ⟨le_update_iff.2 ⟨ha.le, fun _ _ ↦ le_rfl⟩, i, by rwa [update_self]⟩,
          update_le_iff.2 ⟨hb.le, fun _ _ ↦ hab _⟩, i, by rwa [update_self]⟩
-- Lean 4 proof step from Mathlib.Order.Basic (goal)
Goal:
α : Type u_2
inst : LinearOrder α
h : ∀ ⦃x y z : α⦄, x < y → y < z → False
x y z : α
⊢ x = y ∨ y = z ∨ x = z
have by_contra : ∀ (hne : ¬(x = y ∨ y = z ∨ x = z)), False
Tactic: by_contra hne