awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Order.Atoms (goal)
Goal:
ι_1 : Sort u_1
α : Type u_2
β : Type u_3
ι : Type u_4
π : ι → Type u
inst : (i : ι) → PartialOrder (π i)
inst_1 : (i : ι) → OrderBot (π i)
inst_2 : ∀ (i : ι), IsAtomistic.{u} (π i)
s : (i : ι) → π i
refine : IsLUB {f : (i : ι) → π i | IsAtom f ∧ f ≤ s} s
refine₁ refine₂ : ∀ (i : ι), IsLUB (Function.eval (β := π) i '' {f : (i : ι) → π i | IsAtom f ∧ f ≤ s}) (s i)
refine₃ :
  ∀ (i : ι),
    IsLUB
      (Function.eval (β := π) i ''
        {f : (i : ι) → π i | (∃ (i : ι) (a : π i), IsAtom a ∧ f = Function.update (β := π) ⊥ i a) ∧ f ≤ s})
      (s i)
refine_1 :
  ∀ (i : ι),
    Membership.mem (γ := Set (π i))
      (upperBounds
        (Function.eval (β := π) i ''
          {f : (i : ι) → π i | (∃ (i : ι) (a : π i), IsAtom a ∧ f = Function.update (β := π) ⊥ i a) ∧ f ≤ s}))
      (s i)
⊢ ∃ (s_1 : Set ((i : ι) → π i)), IsLUB s_1 s ∧ ∀ a ∈ s_1, IsAtom a
have refine_2 : ∀ (i : ι),
  Membership.mem (γ := Set (π i))
    (lowerBounds
      (upperBounds
        (Function.eval (β := π) i ''
          {f : (i : ι) → π i | (∃ (i : ι) (a : π i), IsAtom a ∧ f = Function.update (β := π) ⊥ i a) ∧ f ≤ s})))
    (s i)
Tactic: classical
    refine ⟨{f | IsAtom f ∧ f ≤ s}, ?_, by simp +contextual⟩
    rw [isLUB_pi]
    intro i
    simp_rw [isAtom_iff_eq_single]
    refine ⟨?_, ?_⟩
    · rintro _ ⟨_, ⟨⟨_, _, _, rfl⟩, hs⟩, rfl⟩
      exact hs i
    · refine fun j hj ↦ (isLUB_atoms_le (s i)).2 fun x ⟨hx₁, hx₂⟩ ↦ ?_
      exact hj ⟨Function.update ⊥ i x, ⟨⟨_, x, hx₁, rfl⟩, by simp [update_le_iff, hx₂]⟩, by simp⟩
-- Lean 4 proof step from Mathlib.Order.Atoms (goal)
Goal:
α : Type u_2
s : Set α
⊢ IsAtom s ↔ ∃ (x : α), s = {x}
have rintro : IsAtom s → ∃ (x : α), s = {x}
Tactic: refine
    ⟨?_, by
      rintro ⟨x, rfl⟩
      exact isAtom_singleton x⟩
-- Lean 4 proof step from Mathlib.Order.Atoms (goal)
Goal:
α : Type u_2
s : Set α
⊢ IsAtom s → ∃ (x : α), s = {x}
have rw : (s.Nonempty ∧ ∀ (b : Set α), b ≠ ∅ → b ≤ s → s ≤ b) → ∃ (x : α), s = {x}
Tactic: rw [isAtom_iff_le_of_ge, bot_eq_empty, ← nonempty_iff_ne_empty]
-- Lean 4 proof step from Mathlib.Order.Atoms (goal)
Goal:
α : Type u_2
s : Set α
⊢ IsCoatom s ↔ ∃ (x : α), s = {x}ᶜ
have rw : (∃ (x : α), sᶜ = {x}) ↔ ∃ (x : α), s = {x}ᶜ
Tactic: rw [isCompl_compl.isCoatom_iff_isAtom, isAtom_iff]
-- Lean 4 proof step from Mathlib.Order.Atoms (goal)
Goal:
α : Type u_2
s : Set α
⊢ (∃ (x : α), sᶜ = {x}) ↔ ∃ (x : α), s = {x}ᶜ
have simp_rw : (∃ (x : α), sᶜ = {x}) ↔ ∃ (x : α), {x}ᶜ = s
Tactic: simp_rw [@eq_comm _ s, compl_eq_comm]
-- Lean 4 proof step from Mathlib.Order.Basic (goal)
Goal:
α : Type u_2
inst : Preorder α
a b : α
⊢ ¬a < b ↔ ¬a ≤ b ∨ b ≤ a
have rw : ¬(a ≤ b ∧ ¬b ≤ a) ↔ ¬a ≤ b ∨ b ≤ a
Tactic: rw [lt_iff_le_not_ge, Classical.not_and_iff_not_or_not, Classical.not_not]
-- Lean 4 proof step from Mathlib.Order.Basic (goal)
Goal:
α : Type u_2
inst : Preorder α
a b : α
rw : ¬(a ≤ b ∧ ¬b ≤ a) ↔ ¬a ≤ b ∨ b ≤ a
⊢ ¬a < b ↔ ¬a ≤ b ∨ b ≤ a
have rw₁ : ¬a ≤ b ∨ ¬¬b ≤ a ↔ ¬a ≤ b ∨ b ≤ a
Tactic: rw [lt_iff_le_not_ge, Classical.not_and_iff_not_or_not, Classical.not_not]
-- Lean 4 proof step from Mathlib.Order.Basic (goal)
Goal:
α : Type u_2
inst : Preorder α
a b : α
rw : ¬(a ≤ b ∧ ¬b ≤ a) ↔ ¬a ≤ b ∨ b ≤ a
rw₁ : ¬a ≤ b ∨ ¬¬b ≤ a ↔ ¬a ≤ b ∨ b ≤ a
⊢ ¬a < b ↔ ¬a ≤ b ∨ b ≤ a
have rw₂ : ¬a ≤ b ∨ b ≤ a ↔ ¬a ≤ b ∨ b ≤ a
Tactic: rw [lt_iff_le_not_ge, Classical.not_and_iff_not_or_not, Classical.not_not]
-- Lean 4 proof step from Mathlib.Order.Basic (goal)
Goal:
α : Type u_2
inst : PartialOrder α
f : α → α → α
comm : Std.Commutative f
assoc : ∀ (a b c : α), f (f a b) c ≤ f a (f b c)
a b c : α
⊢ f a (f b c) ≤ f (f a b) c
have rw : f (f c b) a ≤ f c (f b a)
Tactic: rw [comm.comm, comm.comm b, comm.comm _ c, comm.comm a]
-- Lean 4 proof step from Mathlib.Order.Basic (goal)
Goal:
α : Type u_2
inst : LinearOrder α
a b : α
p : α → Prop
ha : a ≤ b → p a
hb : b ≤ a → p b
⊢ p (min a b)
have inl : ∀ (hab : a ≤ b), p (min a b)
Tactic: obtain hab | hba := le_total a b
-- Lean 4 proof step from Mathlib.Order.Basic (goal)
Goal:
α : Type u_2
inst : LinearOrder α
a b : α
p : α → Prop
ha : a ≤ b → p a
hb : b ≤ a → p b
inl : ∀ (hab : a ≤ b), p (min a b)
⊢ p (min a b)
have inr : ∀ (hba : b ≤ a), p (min a b)
Tactic: obtain hab | hba := le_total a b
-- Lean 4 proof step from Mathlib.Order.Basic (goal)
Goal:
α : Type u_2
inst : LinearOrder α
a b : α
⊢ min a b = if a < b then a else b
have rw : (if ¬b ≤ a then a else b) = if a < b then a else b
Tactic: rw [min_comm, min_def, ← ite_not]
-- Lean 4 proof step from Mathlib.Order.Basic (goal)
Goal:
α : Type u_2
inst : LinearOrder α
a b : α
⊢ max a b = if a < b then b else a
have rw : (if ¬b ≤ a then b else a) = if a < b then b else a
Tactic: rw [max_comm, max_def, ← ite_not]
-- Lean 4 proof step from Mathlib.Order.Basic (goal)
Goal:
α : Type u_2
le A_lt : α → α → Prop
le_refl : ∀ (a : α), le a a
le_trans : ∀ (a b c : α), le a b → le b c → le a c
A_iff : ∀ (a b : α), A_lt a b ↔ le a b ∧ ¬le b a
B_lt : α → α → Prop
le_refl_1 : ∀ (a : α), le a a
le_trans_1 : ∀ (a b c : α), le a b → le b c → le a c
B_iff : ∀ (a b : α), B_lt a b ↔ le a b ∧ ¬le b a
⊢ A_lt = B_lt
have h : ∀ (a b : α), A_lt a b = B_lt a b
Tactic: funext a b
-- Lean 4 proof step from Mathlib.Order.Basic (goal)
Goal:
α : Type u_2
le A_lt : α → α → Prop
le_refl : ∀ (a : α), le a a
le_trans : ∀ (a b c : α), le a b → le b c → le a c
A_iff : ∀ (a b : α), A_lt a b ↔ le a b ∧ ¬le b a
B_lt : α → α → Prop
le_refl_1 : ∀ (a : α), le a a
le_trans_1 : ∀ (a b c : α), le a b → le b c → le a c
B_iff : ∀ (a b : α), B_lt a b ↔ le a b ∧ ¬le b a
a b : α
⊢ A_lt a b = B_lt a b
have h : (le a b ∧ ¬le b a) = B_lt a b
Tactic: rw [A_iff, B_iff]
-- Lean 4 proof step from Mathlib.Order.Basic (goal)
Goal:
α : Type u_2
le A_lt : α → α → Prop
le_refl : ∀ (a : α), le a a
le_trans : ∀ (a b c : α), le a b → le b c → le a c
A_iff : ∀ (a b : α), A_lt a b ↔ le a b ∧ ¬le b a
B_lt : α → α → Prop
le_refl_1 : ∀ (a : α), le a a
le_trans_1 : ∀ (a b c : α), le a b → le b c → le a c
B_iff : ∀ (a b : α), B_lt a b ↔ le a b ∧ ¬le b a
a b : α
h : (le a b ∧ ¬le b a) = B_lt a b
⊢ A_lt a b = B_lt a b
have h₁ : (le a b ∧ ¬le b a) = (le a b ∧ ¬le b a)
Tactic: rw [A_iff, B_iff]
-- Lean 4 proof step from Mathlib.Order.Basic (hypothesis)
Goal:
α : Type u_2
le A_lt : α → α → Prop
le_refl : ∀ (a : α), le a a
le_trans : ∀ (a b c : α), le a b → le b c → le a c
A_iff : ∀ (a b : α), A_lt a b ↔ le a b ∧ ¬le b a
B_lt : α → α → Prop
le_refl_1 : ∀ (a : α), le a a
le_trans_1 : ∀ (a b c : α), le a b → le b c → le a c
B_iff : ∀ (a b : α), B_lt a b ↔ le a b ∧ ¬le b a
⊢ Eq.{u_2 + 1} (α := Preorder α)
    { le := le, lt := A_lt, le_refl := le_refl, le_trans := le_trans, lt_iff_le_not_ge := A_iff }
    { le := le, lt := B_lt, le_refl := le_refl_1, le_trans := le_trans_1, lt_iff_le_not_ge := B_iff }
have this : A_lt = B_lt
Tactic: have : A_lt = B_lt := by
      funext a b
      rw [A_iff, B_iff]
-- Lean 4 proof step from Mathlib.Order.Basic (goal)
Goal:
α : Type u_2
le A_lt : α → α → Prop
le_refl : ∀ (a : α), le a a
le_trans : ∀ (a b c : α), le a b → le b c → le a c
A_iff : ∀ (a b : α), A_lt a b ↔ le a b ∧ ¬le b a
B_lt : α → α → Prop
le_refl_1 : ∀ (a : α), le a a
le_trans_1 : ∀ (a b c : α), le a b → le b c → le a c
B_iff : ∀ (a b : α), B_lt a b ↔ le a b ∧ ¬le b a
this : A_lt = B_lt
⊢ Eq.{u_2 + 1} (α := Preorder α)
    { le := le, lt := A_lt, le_refl := le_refl, le_trans := le_trans, lt_iff_le_not_ge := A_iff }
    { le := le, lt := B_lt, le_refl := le_refl_1, le_trans := le_trans_1, lt_iff_le_not_ge := B_iff }
have refl : ∀ (B_iff : ∀ (a b : α), A_lt a b ↔ le a b ∧ ¬le b a),
  Eq.{u_2 + 1} (α := Preorder α)
    { le := le, lt := A_lt, le_refl := le_refl, le_trans := le_trans, lt_iff_le_not_ge := A_iff }
    { le := le, lt := A_lt, le_refl := le_refl_1, le_trans := le_trans_1, lt_iff_le_not_ge := B_iff }
Tactic: cases this
Cleared hypotheses: B_lt, B_iff, this
-- Lean 4 proof step from Mathlib.Order.Basic (goal)
Goal:
α : Type u_2
A_le A_lt : α → α → Prop
le_refl : ∀ (a : α), A_le a a
le_trans : ∀ (a b c : α), A_le a b → A_le b c → A_le a c
lt_iff_le_not_ge : autoParam (∀ (a b : α), A_lt a b ↔ A_le a b ∧ ¬A_le b a) Preorder.lt_iff_le_not_ge._autoParam
le_antisymm : ∀ (a b : α), A_le a b → A_le b a → a = b
A_min A_max : α → α → α
A_compare : α → α → Ordering
le_total : ∀ (a b : α), A_le a b ∨ A_le b a
A_decidableLE : DecidableLE α
A_decidableEq : DecidableEq α
A_decidableLT : DecidableLT α
A_min_def : ∀ (a b : α), A_min a b = if A_le a b then a else b
A_max_def : ∀ (a b : α), A_max a b = if A_le a b then b else a
A_compare_canonical : ∀ (a b : α), A_compare a b = compareOfLessAndEq a b
B_min B_max : α → α → α
B_compare : α → α → Ordering
le_refl_1 : ∀ (a : α), A_le a a
le_trans_1 : ∀ (a b c : α), A_le a b → A_le b c → A_le a c
le_antisymm_1 : ∀ (a b : α), A_le a b → A_le b a → a = b
le_total_1 : ∀ (a b : α), A_le a b ∨ A_le b a
lt_iff_le_not_ge_1 : autoParam (∀ (a b : α), A_lt a b ↔ A_le a b ∧ ¬A_le b a) Preorder.lt_iff_le_not_ge._autoParam
B_min_def : ∀ (a b : α), B_min a b = if A_le a b then a else b
B_max_def : ∀ (a b : α), B_max a b = if A_le a b then b else a
B_compare_canonical : ∀ (a b : α), B_compare a b = compareOfLessAndEq a b
⊢ A_min = B_min
have h : ∀ (a b : α), A_min a b = B_min a b
Tactic: funext a b
-- Lean 4 proof step from Mathlib.Order.Basic (hypothesis)
Goal:
α : Type u_2
A_le A_lt : α → α → Prop
le_refl : ∀ (a : α), A_le a a
le_trans : ∀ (a b c : α), A_le a b → A_le b c → A_le a c
lt_iff_le_not_ge : autoParam (∀ (a b : α), A_lt a b ↔ A_le a b ∧ ¬A_le b a) Preorder.lt_iff_le_not_ge._autoParam
le_antisymm : ∀ (a b : α), A_le a b → A_le b a → a = b
A_min A_max : α → α → α
A_compare : α → α → Ordering
le_total : ∀ (a b : α), A_le a b ∨ A_le b a
A_decidableLE : DecidableLE α
A_decidableEq : DecidableEq α
A_decidableLT : DecidableLT α
A_min_def : ∀ (a b : α), A_min a b = if A_le a b then a else b
A_max_def : ∀ (a b : α), A_max a b = if A_le a b then b else a
A_compare_canonical : ∀ (a b : α), A_compare a b = compareOfLessAndEq a b
B_min B_max : α → α → α
B_compare : α → α → Ordering
le_refl_1 : ∀ (a : α), A_le a a
le_trans_1 : ∀ (a b c : α), A_le a b → A_le b c → A_le a c
le_antisymm_1 : ∀ (a b : α), A_le a b → A_le b a → a = b
le_total_1 : ∀ (a b : α), A_le a b ∨ A_le b a
lt_iff_le_not_ge_1 : autoParam (∀ (a b : α), A_lt a b ↔ A_le a b ∧ ¬A_le b a) Preorder.lt_iff_le_not_ge._autoParam
B_min_def : ∀ (a b : α), B_min a b = if A_le a b then a else b
B_max_def : ∀ (a b : α), B_max a b = if A_le a b then b else a
B_compare_canonical : ∀ (a b : α), B_compare a b = compareOfLessAndEq a b
⊢ { le := A_le, lt := A_lt, le_refl := le_refl, le_trans := le_trans, lt_iff_le_not_ge := lt_iff_le_not_ge,
      le_antisymm := le_antisymm, min := A_min, max := A_max, compare := A_compare, le_total := le_total,
      toDecidableLE := A_decidableLE, toDecidableEq := A_decidableEq, toDecidableLT := A_decidableLT,
      min_def := A_min_def, max_def := A_max_def, compare_eq_compareOfLessAndEq := A_compare_canonical :
      LinearOrder α } =
    { le := A_le, lt := A_lt, le_refl := le_refl_1, le_trans := le_trans_1, lt_iff_le_not_ge := lt_iff_le_not_ge_1,
      le_antisymm := le_antisymm_1, min := B_min, max := B_max, compare := B_compare, le_total := le_total_1,
      toDecidableLE := A_decidableLE, toDecidableEq := A_decidableEq, toDecidableLT := A_decidableLT,
      min_def := B_min_def, max_def := B_max_def, compare_eq_compareOfLessAndEq := B_compare_canonical }
have this : A_min = B_min
Tactic: have : A_min = B_min := by
      funext a b
      exact (A_min_def _ _).trans (B_min_def _ _).symm
-- Lean 4 proof step from Mathlib.Order.Basic (goal)
Goal:
α : Type u_2
A_le A_lt : α → α → Prop
le_refl : ∀ (a : α), A_le a a
le_trans : ∀ (a b c : α), A_le a b → A_le b c → A_le a c
lt_iff_le_not_ge : autoParam (∀ (a b : α), A_lt a b ↔ A_le a b ∧ ¬A_le b a) Preorder.lt_iff_le_not_ge._autoParam
le_antisymm : ∀ (a b : α), A_le a b → A_le b a → a = b
A_min A_max : α → α → α
A_compare : α → α → Ordering
le_total : ∀ (a b : α), A_le a b ∨ A_le b a
A_decidableLE : DecidableLE α
A_decidableEq : DecidableEq α
A_decidableLT : DecidableLT α
A_min_def : ∀ (a b : α), A_min a b = if A_le a b then a else b
A_max_def : ∀ (a b : α), A_max a b = if A_le a b then b else a
A_compare_canonical : ∀ (a b : α), A_compare a b = compareOfLessAndEq a b
B_max : α → α → α
B_compare : α → α → Ordering
le_refl_1 : ∀ (a : α), A_le a a
le_trans_1 : ∀ (a b c : α), A_le a b → A_le b c → A_le a c
le_antisymm_1 : ∀ (a b : α), A_le a b → A_le b a → a = b
le_total_1 : ∀ (a b : α), A_le a b ∨ A_le b a
lt_iff_le_not_ge_1 : autoParam (∀ (a b : α), A_lt a b ↔ A_le a b ∧ ¬A_le b a) Preorder.lt_iff_le_not_ge._autoParam
B_max_def : ∀ (a b : α), B_max a b = if A_le a b then b else a
B_compare_canonical : ∀ (a b : α), B_compare a b = compareOfLessAndEq a b
B_min_def : ∀ (a b : α), A_min a b = if A_le a b then a else b
⊢ A_max = B_max
have h : ∀ (a b : α), A_max a b = B_max a b
Tactic: funext a b
-- Lean 4 proof step from Mathlib.Order.Basic (hypothesis)
Goal:
α : Type u_2
A_le A_lt : α → α → Prop
le_refl : ∀ (a : α), A_le a a
le_trans : ∀ (a b c : α), A_le a b → A_le b c → A_le a c
lt_iff_le_not_ge : autoParam (∀ (a b : α), A_lt a b ↔ A_le a b ∧ ¬A_le b a) Preorder.lt_iff_le_not_ge._autoParam
le_antisymm : ∀ (a b : α), A_le a b → A_le b a → a = b
A_min A_max : α → α → α
A_compare : α → α → Ordering
le_total : ∀ (a b : α), A_le a b ∨ A_le b a
A_decidableLE : DecidableLE α
A_decidableEq : DecidableEq α
A_decidableLT : DecidableLT α
A_min_def : ∀ (a b : α), A_min a b = if A_le a b then a else b
A_max_def : ∀ (a b : α), A_max a b = if A_le a b then b else a
A_compare_canonical : ∀ (a b : α), A_compare a b = compareOfLessAndEq a b
B_max : α → α → α
B_compare : α → α → Ordering
le_refl_1 : ∀ (a : α), A_le a a
le_trans_1 : ∀ (a b c : α), A_le a b → A_le b c → A_le a c
le_antisymm_1 : ∀ (a b : α), A_le a b → A_le b a → a = b
le_total_1 : ∀ (a b : α), A_le a b ∨ A_le b a
lt_iff_le_not_ge_1 : autoParam (∀ (a b : α), A_lt a b ↔ A_le a b ∧ ¬A_le b a) Preorder.lt_iff_le_not_ge._autoParam
B_max_def : ∀ (a b : α), B_max a b = if A_le a b then b else a
B_compare_canonical : ∀ (a b : α), B_compare a b = compareOfLessAndEq a b
B_min_def : ∀ (a b : α), A_min a b = if A_le a b then a else b
⊢ { le := A_le, lt := A_lt, le_refl := le_refl, le_trans := le_trans, lt_iff_le_not_ge := lt_iff_le_not_ge,
      le_antisymm := le_antisymm, min := A_min, max := A_max, compare := A_compare, le_total := le_total,
      toDecidableLE := A_decidableLE, toDecidableEq := A_decidableEq, toDecidableLT := A_decidableLT,
      min_def := A_min_def, max_def := A_max_def, compare_eq_compareOfLessAndEq := A_compare_canonical :
      LinearOrder α } =
    { le := A_le, lt := A_lt, le_refl := le_refl_1, le_trans := le_trans_1, lt_iff_le_not_ge := lt_iff_le_not_ge_1,
      le_antisymm := le_antisymm_1, min := A_min, max := B_max, compare := B_compare, le_total := le_total_1,
      toDecidableLE := A_decidableLE, toDecidableEq := A_decidableEq, toDecidableLT := A_decidableLT,
      min_def := B_min_def, max_def := B_max_def, compare_eq_compareOfLessAndEq := B_compare_canonical }
have this : A_max = B_max
Tactic: have : A_max = B_max := by
      funext a b
      exact (A_max_def _ _).trans (B_max_def _ _).symm
-- Lean 4 proof step from Mathlib.Order.Basic (goal)
Goal:
α : Type u_2
A_le A_lt : α → α → Prop
le_refl : ∀ (a : α), A_le a a
le_trans : ∀ (a b c : α), A_le a b → A_le b c → A_le a c
lt_iff_le_not_ge : autoParam (∀ (a b : α), A_lt a b ↔ A_le a b ∧ ¬A_le b a) Preorder.lt_iff_le_not_ge._autoParam
le_antisymm : ∀ (a b : α), A_le a b → A_le b a → a = b
A_min A_max : α → α → α
A_compare : α → α → Ordering
le_total : ∀ (a b : α), A_le a b ∨ A_le b a
A_decidableLE : DecidableLE α
A_decidableEq : DecidableEq α
A_decidableLT : DecidableLT α
A_min_def : ∀ (a b : α), A_min a b = if A_le a b then a else b
A_max_def : ∀ (a b : α), A_max a b = if A_le a b then b else a
A_compare_canonical : ∀ (a b : α), A_compare a b = compareOfLessAndEq a b
B_compare : α → α → Ordering
le_refl_1 : ∀ (a : α), A_le a a
le_trans_1 : ∀ (a b c : α), A_le a b → A_le b c → A_le a c
le_antisymm_1 : ∀ (a b : α), A_le a b → A_le b a → a = b
le_total_1 : ∀ (a b : α), A_le a b ∨ A_le b a
lt_iff_le_not_ge_1 : autoParam (∀ (a b : α), A_lt a b ↔ A_le a b ∧ ¬A_le b a) Preorder.lt_iff_le_not_ge._autoParam
B_compare_canonical : ∀ (a b : α), B_compare a b = compareOfLessAndEq a b
B_min_def : ∀ (a b : α), A_min a b = if A_le a b then a else b
B_max_def : ∀ (a b : α), A_max a b = if A_le a b then b else a
⊢ A_compare = B_compare
have h : ∀ (a b : α), A_compare a b = B_compare a b
Tactic: funext a b
-- Lean 4 proof step from Mathlib.Order.Basic (hypothesis)
Goal:
α : Type u_2
A_le A_lt : α → α → Prop
le_refl : ∀ (a : α), A_le a a
le_trans : ∀ (a b c : α), A_le a b → A_le b c → A_le a c
lt_iff_le_not_ge : autoParam (∀ (a b : α), A_lt a b ↔ A_le a b ∧ ¬A_le b a) Preorder.lt_iff_le_not_ge._autoParam
le_antisymm : ∀ (a b : α), A_le a b → A_le b a → a = b
A_min A_max : α → α → α
A_compare : α → α → Ordering
le_total : ∀ (a b : α), A_le a b ∨ A_le b a
A_decidableLE : DecidableLE α
A_decidableEq : DecidableEq α
A_decidableLT : DecidableLT α
A_min_def : ∀ (a b : α), A_min a b = if A_le a b then a else b
A_max_def : ∀ (a b : α), A_max a b = if A_le a b then b else a
A_compare_canonical : ∀ (a b : α), A_compare a b = compareOfLessAndEq a b
B_compare : α → α → Ordering
le_refl_1 : ∀ (a : α), A_le a a
le_trans_1 : ∀ (a b c : α), A_le a b → A_le b c → A_le a c
le_antisymm_1 : ∀ (a b : α), A_le a b → A_le b a → a = b
le_total_1 : ∀ (a b : α), A_le a b ∨ A_le b a
lt_iff_le_not_ge_1 : autoParam (∀ (a b : α), A_lt a b ↔ A_le a b ∧ ¬A_le b a) Preorder.lt_iff_le_not_ge._autoParam
B_compare_canonical : ∀ (a b : α), B_compare a b = compareOfLessAndEq a b
B_min_def : ∀ (a b : α), A_min a b = if A_le a b then a else b
B_max_def : ∀ (a b : α), A_max a b = if A_le a b then b else a
⊢ { le := A_le, lt := A_lt, le_refl := le_refl, le_trans := le_trans, lt_iff_le_not_ge := lt_iff_le_not_ge,
      le_antisymm := le_antisymm, min := A_min, max := A_max, compare := A_compare, le_total := le_total,
      toDecidableLE := A_decidableLE, toDecidableEq := A_decidableEq, toDecidableLT := A_decidableLT,
      min_def := A_min_def, max_def := A_max_def, compare_eq_compareOfLessAndEq := A_compare_canonical :
      LinearOrder α } =
    { le := A_le, lt := A_lt, le_refl := le_refl_1, le_trans := le_trans_1, lt_iff_le_not_ge := lt_iff_le_not_ge_1,
      le_antisymm := le_antisymm_1, min := A_min, max := A_max, compare := B_compare, le_total := le_total_1,
      toDecidableLE := A_decidableLE, toDecidableEq := A_decidableEq, toDecidableLT := A_decidableLT,
      min_def := B_min_def, max_def := B_max_def, compare_eq_compareOfLessAndEq := B_compare_canonical }
have this : A_compare = B_compare
Tactic: have : A_compare = B_compare := by
      funext a b
      exact (A_compare_canonical _ _).trans (B_compare_canonical _ _).symm
-- Lean 4 proof step from Mathlib.Order.Basic (goal)
Goal:
α : Type u_2
A B : PartialOrder α
H : ∀ (x y : α), x < y ↔ x < y
⊢ A = B
have a : ∀ (x y : α), x ≤ y ↔ x ≤ y
Tactic: ext x y
-- Lean 4 proof step from Mathlib.Order.Basic (goal)
Goal:
α : Type u_2
A B : PartialOrder α
H : ∀ (x y : α), x < y ↔ x < y
x y : α
⊢ x ≤ y ↔ x ≤ y
have a : x ≤ y ↔ x < y ∨ x = y
Tactic: rw [le_iff_lt_or_eq, @le_iff_lt_or_eq _ A, H]
-- Lean 4 proof step from Mathlib.Order.Basic (goal)
Goal:
α : Type u_2
A B : PartialOrder α
H : ∀ (x y : α), x < y ↔ x < y
x y : α
a : x ≤ y ↔ x < y ∨ x = y
⊢ x ≤ y ↔ x ≤ y
have a₁ : x < y ∨ x = y ↔ x < y ∨ x = y
Tactic: rw [le_iff_lt_or_eq, @le_iff_lt_or_eq _ A, H]
-- Lean 4 proof step from Mathlib.Order.Basic (goal)
Goal:
α : Type u_2
A B : PartialOrder α
H : ∀ (x y : α), x < y ↔ x < y
x y : α
a : x ≤ y ↔ x < y ∨ x = y
a₁ : x < y ∨ x = y ↔ x < y ∨ x = y
⊢ x ≤ y ↔ x ≤ y
have a₂ : x < y ∨ x = y ↔ x < y ∨ x = y
Tactic: rw [le_iff_lt_or_eq, @le_iff_lt_or_eq _ A, H]
-- Lean 4 proof step from Mathlib.Order.Basic (goal)
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
⊢ IsEquiv α (fun (x1 x2 : α) ↦ x1 ≠ x2)ᶜ
have h : ∀ (x x : α), Eq.{u_2 + 1} (α := α → α → Prop) (fun (x1 x2 : α) ↦ x1 ≠ x2)ᶜ Eq
Tactic: convert! eq_isEquiv α
-- Lean 4 proof step from Mathlib.Order.Basic (goal)
Goal:
ι : Type u_1
π : ι → Type u_4
inst : (i : ι) → Preorder (π i)
a b : (i : ι) → π i
inst_1 : Nonempty ι
h : StrongLT (π := π) a b
⊢ a < b
have inhabit : ∀ (inhabited_h : Inhabited ι), a < b
Tactic: inhabit ι
-- 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 : LE α
inst_2 : LT α
f : α → β
le : ∀ {x y : α}, f x ≤ f y ↔ x ≤ y
lt : ∀ {x y : α}, f x < f y ↔ x < y
x x_1 : α
⊢ x < x_1 ↔ x ≤ x_1 ∧ ¬x_1 ≤ x
have rw : x < x_1 ↔ f x ≤ f x_1 ∧ ¬x_1 ≤ x
Tactic: rw [← le, ← le, ← lt, lt_iff_le_not_ge]
-- 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 : LE α
inst_2 : LT α
f : α → β
le : ∀ {x y : α}, f x ≤ f y ↔ x ≤ y
lt : ∀ {x y : α}, f x < f y ↔ x < y
x x_1 : α
rw : x < x_1 ↔ f x ≤ f x_1 ∧ ¬x_1 ≤ x
⊢ x < x_1 ↔ x ≤ x_1 ∧ ¬x_1 ≤ x
have rw₁ : x < x_1 ↔ f x ≤ f x_1 ∧ ¬f x_1 ≤ f x
Tactic: rw [← le, ← le, ← lt, lt_iff_le_not_ge]
-- 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 : LE α
inst_2 : LT α
f : α → β
le : ∀ {x y : α}, f x ≤ f y ↔ x ≤ y
lt : ∀ {x y : α}, f x < f y ↔ x < y
x x_1 : α
rw : x < x_1 ↔ f x ≤ f x_1 ∧ ¬x_1 ≤ x
rw₁ : x < x_1 ↔ f x ≤ f x_1 ∧ ¬f x_1 ≤ f x
⊢ x < x_1 ↔ x ≤ x_1 ∧ ¬x_1 ≤ x
have rw₂ : f x < f x_1 ↔ f x ≤ f x_1 ∧ ¬f x_1 ≤ f x
Tactic: rw [← le, ← le, ← lt, lt_iff_le_not_ge]
-- 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 : LE α
inst_2 : LT α
f : α → β
le : ∀ {x y : α}, f x ≤ f y ↔ x ≤ y
lt : ∀ {x y : α}, f x < f y ↔ x < y
x x_1 : α
rw : x < x_1 ↔ f x ≤ f x_1 ∧ ¬x_1 ≤ x
rw₁ : x < x_1 ↔ f x ≤ f x_1 ∧ ¬f x_1 ≤ f x
rw₂ : f x < f x_1 ↔ f x ≤ f x_1 ∧ ¬f x_1 ≤ f x
⊢ x < x_1 ↔ x ≤ x_1 ∧ ¬x_1 ≤ x
have rw₃ : f x ≤ f x_1 ∧ ¬f x_1 ≤ f x ↔ f x ≤ f x_1 ∧ ¬f x_1 ≤ f x
Tactic: rw [← le, ← le, ← lt, lt_iff_le_not_ge]
-- 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 else x_1
have simp_rw : f (x ⊓ x_1) = f (if x ≤ x_1 then x else 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)
⊢ x ⊓ x_1 = if x ≤ x_1 then x else x_1
have simp_rw₁ : f (x ⊓ x_1) = f (if f x ≤ f x_1 then x else x_1)
Tactic: simp_rw [← hf.eq_iff, ← le, apply_ite f, ← min_def, min]