awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Set.Monotone (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
f : α → β
s : Set α
a : α
ha : ∀ (x : α), x ∈ s → x ≤ a
⊢ StrictAntiOn f (insert a s) ↔ (∀ (b : α), b ∈ s → b < a → f a < f b) ∧ StrictAntiOn f s
have rw : (∀ (b : α), b ∈ s → b < a → f a < f b) ∧ (∀ (b : α), b ∈ s → a < b → f b < f a) ∧ StrictAntiOn f s ↔
  (∀ (b : α), b ∈ s → b < a → f a < f b) ∧ StrictAntiOn f s
Tactic: rw [strictAntiOn_insert_iff]
-- Lean 4 proof step from Mathlib.Data.Set.Monotone (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
f : α → β
s : Set α
a : α
ha : ∀ (x : α), x ∈ s → x ≤ a
⊢ (∀ (b : α), b ∈ s → b < a → f a < f b) ∧ (∀ (b : α), b ∈ s → a < b → f b < f a) ∧ StrictAntiOn f s ↔
    (∀ (b : α), b ∈ s → b < a → f a < f b) ∧ StrictAntiOn f s
have this : ∀ (b : α), b ∈ s → a < b → f b < f a
Tactic: have : ∀ b ∈ s, a < b → f b < f a := by
    intro b hb hab
    cases (ha _ hb).not_gt hab
-- Lean 4 proof step from Mathlib.Data.Set.Monotone (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
f : α → β
s : Set α
a : α
ha : ∀ (x : α), x ∈ s → x ≤ a
this : ∀ (b : α), b ∈ s → a < b → f b < f a
⊢ (∀ (b : α), b ∈ s → b < a → f a < f b) ∧ (∀ (b : α), b ∈ s → a < b → f b < f a) ∧ StrictAntiOn f s ↔
    (∀ (b : α), b ∈ s → b < a → f a < f b) ∧ StrictAntiOn f s
have mp : (∀ (b : α), b ∈ s → b < a → f a < f b) ∧ (∀ (b : α), b ∈ s → a < b → f b < f a) ∧ StrictAntiOn f s →
  (∀ (b : α), b ∈ s → b < a → f a < f b) ∧ StrictAntiOn f s
Tactic: tauto
-- Lean 4 proof step from Mathlib.Data.Set.Monotone (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
f : α → β
s : Set α
a : α
ha : ∀ (x : α), x ∈ s → x ≤ a
this : ∀ (b : α), b ∈ s → a < b → f b < f a
mp :
  (∀ (b : α), b ∈ s → b < a → f a < f b) ∧ (∀ (b : α), b ∈ s → a < b → f b < f a) ∧ StrictAntiOn f s →
    (∀ (b : α), b ∈ s → b < a → f a < f b) ∧ StrictAntiOn f s
⊢ (∀ (b : α), b ∈ s → b < a → f a < f b) ∧ (∀ (b : α), b ∈ s → a < b → f b < f a) ∧ StrictAntiOn f s ↔
    (∀ (b : α), b ∈ s → b < a → f a < f b) ∧ StrictAntiOn f s
have mpr : (∀ (b : α), b ∈ s → b < a → f a < f b) ∧ StrictAntiOn f s →
  (∀ (b : α), b ∈ s → b < a → f a < f b) ∧ (∀ (b : α), b ∈ s → a < b → f b < f a) ∧ StrictAntiOn f s
Tactic: tauto
-- Lean 4 proof step from Mathlib.Data.Set.Monotone (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
f : α → β
s : Set α
a : α
ha : ∀ (x : α), x ∈ s → x ≤ a
this : ∀ (b : α), b ∈ s → a < b → f b < f a
mp :
  (∀ (b : α), b ∈ s → b < a → f a < f b) ∧ (∀ (b : α), b ∈ s → a < b → f b < f a) ∧ StrictAntiOn f s →
    (∀ (b : α), b ∈ s → b < a → f a < f b) ∧ StrictAntiOn f s
mpr :
  (∀ (b : α), b ∈ s → b < a → f a < f b) ∧ StrictAntiOn f s →
    (∀ (b : α), b ∈ s → b < a → f a < f b) ∧ (∀ (b : α), b ∈ s → a < b → f b < f a) ∧ StrictAntiOn f s
⊢ (∀ (b : α), b ∈ s → b < a → f a < f b) ∧ (∀ (b : α), b ∈ s → a < b → f b < f a) ∧ StrictAntiOn f s ↔
    (∀ (b : α), b ∈ s → b < a → f a < f b) ∧ StrictAntiOn f s
have mp₁ : (∀ (b : α), b ∈ s → b < a → f a < f b) →
  (∀ (b : α), b ∈ s → a < b → f b < f a) → StrictAntiOn f s → (∀ (b : α), b ∈ s → b < a → f a < f b) ∧ StrictAntiOn f s
Tactic: tauto
-- Lean 4 proof step from Mathlib.Data.Set.Monotone (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
f : α → β
s : Set α
a : α
ha : ∀ (x : α), x ∈ s → x ≤ a
this : ∀ (b : α), b ∈ s → a < b → f b < f a
mp :
  (∀ (b : α), b ∈ s → b < a → f a < f b) ∧ (∀ (b : α), b ∈ s → a < b → f b < f a) ∧ StrictAntiOn f s →
    (∀ (b : α), b ∈ s → b < a → f a < f b) ∧ StrictAntiOn f s
mpr :
  (∀ (b : α), b ∈ s → b < a → f a < f b) ∧ StrictAntiOn f s →
    (∀ (b : α), b ∈ s → b < a → f a < f b) ∧ (∀ (b : α), b ∈ s → a < b → f b < f a) ∧ StrictAntiOn f s
mp₁ mp₂ :
  (∀ (b : α), b ∈ s → b < a → f a < f b) →
    (∀ (b : α), b ∈ s → a < b → f b < f a) →
      StrictAntiOn f s → (∀ (b : α), b ∈ s → b < a → f a < f b) ∧ StrictAntiOn f s
⊢ (∀ (b : α), b ∈ s → b < a → f a < f b) ∧ (∀ (b : α), b ∈ s → a < b → f b < f a) ∧ StrictAntiOn f s ↔
    (∀ (b : α), b ∈ s → b < a → f a < f b) ∧ StrictAntiOn f s
have mp₃ : (∀ (b : α), b ∈ s → b < a → f a < f b) →
  (∀ (b : α), b ∈ s → a < b → f b < f a) → StrictAntiOn f s → ∀ (b : α), b ∈ s → b < a → f a < f b
Tactic: tauto
-- Lean 4 proof step from Mathlib.Data.Set.Monotone (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
f : α → β
s : Set α
a : α
ha : ∀ (x : α), x ∈ s → x ≤ a
this : ∀ (b : α), b ∈ s → a < b → f b < f a
mp :
  (∀ (b : α), b ∈ s → b < a → f a < f b) ∧ (∀ (b : α), b ∈ s → a < b → f b < f a) ∧ StrictAntiOn f s →
    (∀ (b : α), b ∈ s → b < a → f a < f b) ∧ StrictAntiOn f s
mpr :
  (∀ (b : α), b ∈ s → b < a → f a < f b) ∧ StrictAntiOn f s →
    (∀ (b : α), b ∈ s → b < a → f a < f b) ∧ (∀ (b : α), b ∈ s → a < b → f b < f a) ∧ StrictAntiOn f s
mp₁ mp₂ :
  (∀ (b : α), b ∈ s → b < a → f a < f b) →
    (∀ (b : α), b ∈ s → a < b → f b < f a) →
      StrictAntiOn f s → (∀ (b : α), b ∈ s → b < a → f a < f b) ∧ StrictAntiOn f s
mp₃ :
  (∀ (b : α), b ∈ s → b < a → f a < f b) →
    (∀ (b : α), b ∈ s → a < b → f b < f a) → StrictAntiOn f s → ∀ (b : α), b ∈ s → b < a → f a < f b
⊢ (∀ (b : α), b ∈ s → b < a → f a < f b) ∧ (∀ (b : α), b ∈ s → a < b → f b < f a) ∧ StrictAntiOn f s ↔
    (∀ (b : α), b ∈ s → b < a → f a < f b) ∧ StrictAntiOn f s
have mp₄ : (∀ (b : α), b ∈ s → b < a → f a < f b) → (∀ (b : α), b ∈ s → a < b → f b < f a) → StrictAntiOn f s → StrictAntiOn f s
Tactic: tauto
-- Lean 4 proof step from Mathlib.Data.Set.Monotone (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
f : α → β
s : Set α
a : α
ha : ∀ (x : α), x ∈ s → x ≤ a
this : ∀ (b : α), b ∈ s → a < b → f b < f a
mp :
  (∀ (b : α), b ∈ s → b < a → f a < f b) ∧ (∀ (b : α), b ∈ s → a < b → f b < f a) ∧ StrictAntiOn f s →
    (∀ (b : α), b ∈ s → b < a → f a < f b) ∧ StrictAntiOn f s
mpr :
  (∀ (b : α), b ∈ s → b < a → f a < f b) ∧ StrictAntiOn f s →
    (∀ (b : α), b ∈ s → b < a → f a < f b) ∧ (∀ (b : α), b ∈ s → a < b → f b < f a) ∧ StrictAntiOn f s
mp₁ mp₂ :
  (∀ (b : α), b ∈ s → b < a → f a < f b) →
    (∀ (b : α), b ∈ s → a < b → f b < f a) →
      StrictAntiOn f s → (∀ (b : α), b ∈ s → b < a → f a < f b) ∧ StrictAntiOn f s
mp₃ :
  (∀ (b : α), b ∈ s → b < a → f a < f b) →
    (∀ (b : α), b ∈ s → a < b → f b < f a) → StrictAntiOn f s → ∀ (b : α), b ∈ s → b < a → f a < f b
mp₄ :
  (∀ (b : α), b ∈ s → b < a → f a < f b) → (∀ (b : α), b ∈ s → a < b → f b < f a) → StrictAntiOn f s → StrictAntiOn f s
⊢ (∀ (b : α), b ∈ s → b < a → f a < f b) ∧ (∀ (b : α), b ∈ s → a < b → f b < f a) ∧ StrictAntiOn f s ↔
    (∀ (b : α), b ∈ s → b < a → f a < f b) ∧ StrictAntiOn f s
have mpr₁ : (∀ (b : α), b ∈ s → b < a → f a < f b) →
  StrictAntiOn f s → (∀ (b : α), b ∈ s → b < a → f a < f b) ∧ (∀ (b : α), b ∈ s → a < b → f b < f a) ∧ StrictAntiOn f s
Tactic: tauto
-- Lean 4 proof step from Mathlib.Data.Set.Monotone (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
f : α → β
s : Set α
a : α
ha : ∀ (x : α), x ∈ s → x ≤ a
this : ∀ (b : α), b ∈ s → a < b → f b < f a
mp :
  (∀ (b : α), b ∈ s → b < a → f a < f b) ∧ (∀ (b : α), b ∈ s → a < b → f b < f a) ∧ StrictAntiOn f s →
    (∀ (b : α), b ∈ s → b < a → f a < f b) ∧ StrictAntiOn f s
mpr :
  (∀ (b : α), b ∈ s → b < a → f a < f b) ∧ StrictAntiOn f s →
    (∀ (b : α), b ∈ s → b < a → f a < f b) ∧ (∀ (b : α), b ∈ s → a < b → f b < f a) ∧ StrictAntiOn f s
mp₁ mp₂ :
  (∀ (b : α), b ∈ s → b < a → f a < f b) →
    (∀ (b : α), b ∈ s → a < b → f b < f a) →
      StrictAntiOn f s → (∀ (b : α), b ∈ s → b < a → f a < f b) ∧ StrictAntiOn f s
mp₃ :
  (∀ (b : α), b ∈ s → b < a → f a < f b) →
    (∀ (b : α), b ∈ s → a < b → f b < f a) → StrictAntiOn f s → ∀ (b : α), b ∈ s → b < a → f a < f b
mp₄ :
  (∀ (b : α), b ∈ s → b < a → f a < f b) → (∀ (b : α), b ∈ s → a < b → f b < f a) → StrictAntiOn f s → StrictAntiOn f s
mpr₁ mpr₂ :
  (∀ (b : α), b ∈ s → b < a → f a < f b) →
    StrictAntiOn f s →
      (∀ (b : α), b ∈ s → b < a → f a < f b) ∧ (∀ (b : α), b ∈ s → a < b → f b < f a) ∧ StrictAntiOn f s
⊢ (∀ (b : α), b ∈ s → b < a → f a < f b) ∧ (∀ (b : α), b ∈ s → a < b → f b < f a) ∧ StrictAntiOn f s ↔
    (∀ (b : α), b ∈ s → b < a → f a < f b) ∧ StrictAntiOn f s
have mpr₃ : (∀ (b : α), b ∈ s → b < a → f a < f b) → StrictAntiOn f s → ∀ (b : α), b ∈ s → b < a → f a < f b
Tactic: tauto
-- Lean 4 proof step from Mathlib.Data.Set.Monotone (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
f : α → β
s : Set α
a : α
ha : ∀ (x : α), x ∈ s → x ≤ a
this : ∀ (b : α), b ∈ s → a < b → f b < f a
mp :
  (∀ (b : α), b ∈ s → b < a → f a < f b) ∧ (∀ (b : α), b ∈ s → a < b → f b < f a) ∧ StrictAntiOn f s →
    (∀ (b : α), b ∈ s → b < a → f a < f b) ∧ StrictAntiOn f s
mpr :
  (∀ (b : α), b ∈ s → b < a → f a < f b) ∧ StrictAntiOn f s →
    (∀ (b : α), b ∈ s → b < a → f a < f b) ∧ (∀ (b : α), b ∈ s → a < b → f b < f a) ∧ StrictAntiOn f s
mp₁ mp₂ :
  (∀ (b : α), b ∈ s → b < a → f a < f b) →
    (∀ (b : α), b ∈ s → a < b → f b < f a) →
      StrictAntiOn f s → (∀ (b : α), b ∈ s → b < a → f a < f b) ∧ StrictAntiOn f s
mp₃ :
  (∀ (b : α), b ∈ s → b < a → f a < f b) →
    (∀ (b : α), b ∈ s → a < b → f b < f a) → StrictAntiOn f s → ∀ (b : α), b ∈ s → b < a → f a < f b
mp₄ :
  (∀ (b : α), b ∈ s → b < a → f a < f b) → (∀ (b : α), b ∈ s → a < b → f b < f a) → StrictAntiOn f s → StrictAntiOn f s
mpr₁ mpr₂ :
  (∀ (b : α), b ∈ s → b < a → f a < f b) →
    StrictAntiOn f s →
      (∀ (b : α), b ∈ s → b < a → f a < f b) ∧ (∀ (b : α), b ∈ s → a < b → f b < f a) ∧ StrictAntiOn f s
mpr₃ : (∀ (b : α), b ∈ s → b < a → f a < f b) → StrictAntiOn f s → ∀ (b : α), b ∈ s → b < a → f a < f b
⊢ (∀ (b : α), b ∈ s → b < a → f a < f b) ∧ (∀ (b : α), b ∈ s → a < b → f b < f a) ∧ StrictAntiOn f s ↔
    (∀ (b : α), b ∈ s → b < a → f a < f b) ∧ StrictAntiOn f s
have mpr₄ : (∀ (b : α), b ∈ s → b < a → f a < f b) → StrictAntiOn f s → ∀ (b : α), b ∈ s → a < b → f b < f a
Tactic: tauto
-- Lean 4 proof step from Mathlib.Data.Set.Monotone (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
f : α → β
s : Set α
a : α
ha : ∀ (x : α), x ∈ s → x ≤ a
this : ∀ (b : α), b ∈ s → a < b → f b < f a
mp :
  (∀ (b : α), b ∈ s → b < a → f a < f b) ∧ (∀ (b : α), b ∈ s → a < b → f b < f a) ∧ StrictAntiOn f s →
    (∀ (b : α), b ∈ s → b < a → f a < f b) ∧ StrictAntiOn f s
mpr :
  (∀ (b : α), b ∈ s → b < a → f a < f b) ∧ StrictAntiOn f s →
    (∀ (b : α), b ∈ s → b < a → f a < f b) ∧ (∀ (b : α), b ∈ s → a < b → f b < f a) ∧ StrictAntiOn f s
mp₁ mp₂ :
  (∀ (b : α), b ∈ s → b < a → f a < f b) →
    (∀ (b : α), b ∈ s → a < b → f b < f a) →
      StrictAntiOn f s → (∀ (b : α), b ∈ s → b < a → f a < f b) ∧ StrictAntiOn f s
mp₃ :
  (∀ (b : α), b ∈ s → b < a → f a < f b) →
    (∀ (b : α), b ∈ s → a < b → f b < f a) → StrictAntiOn f s → ∀ (b : α), b ∈ s → b < a → f a < f b
mp₄ :
  (∀ (b : α), b ∈ s → b < a → f a < f b) → (∀ (b : α), b ∈ s → a < b → f b < f a) → StrictAntiOn f s → StrictAntiOn f s
mpr₁ mpr₂ :
  (∀ (b : α), b ∈ s → b < a → f a < f b) →
    StrictAntiOn f s →
      (∀ (b : α), b ∈ s → b < a → f a < f b) ∧ (∀ (b : α), b ∈ s → a < b → f b < f a) ∧ StrictAntiOn f s
mpr₃ : (∀ (b : α), b ∈ s → b < a → f a < f b) → StrictAntiOn f s → ∀ (b : α), b ∈ s → b < a → f a < f b
mpr₄ : (∀ (b : α), b ∈ s → b < a → f a < f b) → StrictAntiOn f s → ∀ (b : α), b ∈ s → a < b → f b < f a
⊢ (∀ (b : α), b ∈ s → b < a → f a < f b) ∧ (∀ (b : α), b ∈ s → a < b → f b < f a) ∧ StrictAntiOn f s ↔
    (∀ (b : α), b ∈ s → b < a → f a < f b) ∧ StrictAntiOn f s
have mpr₅ : (∀ (b : α), b ∈ s → b < a → f a < f b) → StrictAntiOn f s → StrictAntiOn f s
Tactic: tauto
-- Lean 4 proof step from Mathlib.Data.Set.Monotone (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
f : α → β
s : Set α
a : α
ha : ∀ (x : α), x ∈ s → a ≤ x
⊢ StrictAntiOn f (insert a s) ↔ (∀ (b : α), b ∈ s → a < b → f b < f a) ∧ StrictAntiOn f s
have rw : (∀ (b : α), b ∈ s → b < a → f a < f b) ∧ (∀ (b : α), b ∈ s → a < b → f b < f a) ∧ StrictAntiOn f s ↔
  (∀ (b : α), b ∈ s → a < b → f b < f a) ∧ StrictAntiOn f s
Tactic: rw [strictAntiOn_insert_iff]
-- Lean 4 proof step from Mathlib.Data.Set.Monotone (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
f : α → β
s : Set α
a : α
ha : ∀ (x : α), x ∈ s → a ≤ x
⊢ (∀ (b : α), b ∈ s → b < a → f a < f b) ∧ (∀ (b : α), b ∈ s → a < b → f b < f a) ∧ StrictAntiOn f s ↔
    (∀ (b : α), b ∈ s → a < b → f b < f a) ∧ StrictAntiOn f s
have this : ∀ (b : α), b ∈ s → b < a → f a < f b
Tactic: have : ∀ b ∈ s, b < a → f a < f b := by
    intro b hb hab
    cases (ha _ hb).not_gt hab
-- Lean 4 proof step from Mathlib.Data.Set.Monotone (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
f : α → β
s : Set α
a : α
ha : ∀ (x : α), x ∈ s → a ≤ x
this : ∀ (b : α), b ∈ s → b < a → f a < f b
⊢ (∀ (b : α), b ∈ s → b < a → f a < f b) ∧ (∀ (b : α), b ∈ s → a < b → f b < f a) ∧ StrictAntiOn f s ↔
    (∀ (b : α), b ∈ s → a < b → f b < f a) ∧ StrictAntiOn f s
have mp : (∀ (b : α), b ∈ s → b < a → f a < f b) ∧ (∀ (b : α), b ∈ s → a < b → f b < f a) ∧ StrictAntiOn f s →
  (∀ (b : α), b ∈ s → a < b → f b < f a) ∧ StrictAntiOn f s
Tactic: tauto
-- Lean 4 proof step from Mathlib.Data.Set.Monotone (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
f : α → β
s : Set α
a : α
ha : ∀ (x : α), x ∈ s → a ≤ x
this : ∀ (b : α), b ∈ s → b < a → f a < f b
mp :
  (∀ (b : α), b ∈ s → b < a → f a < f b) ∧ (∀ (b : α), b ∈ s → a < b → f b < f a) ∧ StrictAntiOn f s →
    (∀ (b : α), b ∈ s → a < b → f b < f a) ∧ StrictAntiOn f s
⊢ (∀ (b : α), b ∈ s → b < a → f a < f b) ∧ (∀ (b : α), b ∈ s → a < b → f b < f a) ∧ StrictAntiOn f s ↔
    (∀ (b : α), b ∈ s → a < b → f b < f a) ∧ StrictAntiOn f s
have mpr : (∀ (b : α), b ∈ s → a < b → f b < f a) ∧ StrictAntiOn f s →
  (∀ (b : α), b ∈ s → b < a → f a < f b) ∧ (∀ (b : α), b ∈ s → a < b → f b < f a) ∧ StrictAntiOn f s
Tactic: tauto
-- Lean 4 proof step from Mathlib.Data.Set.Monotone (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
f : α → β
s : Set α
a : α
ha : ∀ (x : α), x ∈ s → a ≤ x
this : ∀ (b : α), b ∈ s → b < a → f a < f b
mp :
  (∀ (b : α), b ∈ s → b < a → f a < f b) ∧ (∀ (b : α), b ∈ s → a < b → f b < f a) ∧ StrictAntiOn f s →
    (∀ (b : α), b ∈ s → a < b → f b < f a) ∧ StrictAntiOn f s
mpr :
  (∀ (b : α), b ∈ s → a < b → f b < f a) ∧ StrictAntiOn f s →
    (∀ (b : α), b ∈ s → b < a → f a < f b) ∧ (∀ (b : α), b ∈ s → a < b → f b < f a) ∧ StrictAntiOn f s
⊢ (∀ (b : α), b ∈ s → b < a → f a < f b) ∧ (∀ (b : α), b ∈ s → a < b → f b < f a) ∧ StrictAntiOn f s ↔
    (∀ (b : α), b ∈ s → a < b → f b < f a) ∧ StrictAntiOn f s
have mp₁ : (∀ (b : α), b ∈ s → b < a → f a < f b) →
  (∀ (b : α), b ∈ s → a < b → f b < f a) → StrictAntiOn f s → (∀ (b : α), b ∈ s → a < b → f b < f a) ∧ StrictAntiOn f s
Tactic: tauto
-- Lean 4 proof step from Mathlib.Data.Set.Monotone (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
f : α → β
s : Set α
a : α
ha : ∀ (x : α), x ∈ s → a ≤ x
this : ∀ (b : α), b ∈ s → b < a → f a < f b
mp :
  (∀ (b : α), b ∈ s → b < a → f a < f b) ∧ (∀ (b : α), b ∈ s → a < b → f b < f a) ∧ StrictAntiOn f s →
    (∀ (b : α), b ∈ s → a < b → f b < f a) ∧ StrictAntiOn f s
mpr :
  (∀ (b : α), b ∈ s → a < b → f b < f a) ∧ StrictAntiOn f s →
    (∀ (b : α), b ∈ s → b < a → f a < f b) ∧ (∀ (b : α), b ∈ s → a < b → f b < f a) ∧ StrictAntiOn f s
mp₁ mp₂ :
  (∀ (b : α), b ∈ s → b < a → f a < f b) →
    (∀ (b : α), b ∈ s → a < b → f b < f a) →
      StrictAntiOn f s → (∀ (b : α), b ∈ s → a < b → f b < f a) ∧ StrictAntiOn f s
⊢ (∀ (b : α), b ∈ s → b < a → f a < f b) ∧ (∀ (b : α), b ∈ s → a < b → f b < f a) ∧ StrictAntiOn f s ↔
    (∀ (b : α), b ∈ s → a < b → f b < f a) ∧ StrictAntiOn f s
have mp₃ : (∀ (b : α), b ∈ s → b < a → f a < f b) →
  (∀ (b : α), b ∈ s → a < b → f b < f a) → StrictAntiOn f s → ∀ (b : α), b ∈ s → a < b → f b < f a
Tactic: tauto
-- Lean 4 proof step from Mathlib.Data.Set.Monotone (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
f : α → β
s : Set α
a : α
ha : ∀ (x : α), x ∈ s → a ≤ x
this : ∀ (b : α), b ∈ s → b < a → f a < f b
mp :
  (∀ (b : α), b ∈ s → b < a → f a < f b) ∧ (∀ (b : α), b ∈ s → a < b → f b < f a) ∧ StrictAntiOn f s →
    (∀ (b : α), b ∈ s → a < b → f b < f a) ∧ StrictAntiOn f s
mpr :
  (∀ (b : α), b ∈ s → a < b → f b < f a) ∧ StrictAntiOn f s →
    (∀ (b : α), b ∈ s → b < a → f a < f b) ∧ (∀ (b : α), b ∈ s → a < b → f b < f a) ∧ StrictAntiOn f s
mp₁ mp₂ :
  (∀ (b : α), b ∈ s → b < a → f a < f b) →
    (∀ (b : α), b ∈ s → a < b → f b < f a) →
      StrictAntiOn f s → (∀ (b : α), b ∈ s → a < b → f b < f a) ∧ StrictAntiOn f s
mp₃ :
  (∀ (b : α), b ∈ s → b < a → f a < f b) →
    (∀ (b : α), b ∈ s → a < b → f b < f a) → StrictAntiOn f s → ∀ (b : α), b ∈ s → a < b → f b < f a
⊢ (∀ (b : α), b ∈ s → b < a → f a < f b) ∧ (∀ (b : α), b ∈ s → a < b → f b < f a) ∧ StrictAntiOn f s ↔
    (∀ (b : α), b ∈ s → a < b → f b < f a) ∧ StrictAntiOn f s
have mp₄ : (∀ (b : α), b ∈ s → b < a → f a < f b) → (∀ (b : α), b ∈ s → a < b → f b < f a) → StrictAntiOn f s → StrictAntiOn f s
Tactic: tauto
-- Lean 4 proof step from Mathlib.Data.Set.Monotone (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
f : α → β
s : Set α
a : α
ha : ∀ (x : α), x ∈ s → a ≤ x
this : ∀ (b : α), b ∈ s → b < a → f a < f b
mp :
  (∀ (b : α), b ∈ s → b < a → f a < f b) ∧ (∀ (b : α), b ∈ s → a < b → f b < f a) ∧ StrictAntiOn f s →
    (∀ (b : α), b ∈ s → a < b → f b < f a) ∧ StrictAntiOn f s
mpr :
  (∀ (b : α), b ∈ s → a < b → f b < f a) ∧ StrictAntiOn f s →
    (∀ (b : α), b ∈ s → b < a → f a < f b) ∧ (∀ (b : α), b ∈ s → a < b → f b < f a) ∧ StrictAntiOn f s
mp₁ mp₂ :
  (∀ (b : α), b ∈ s → b < a → f a < f b) →
    (∀ (b : α), b ∈ s → a < b → f b < f a) →
      StrictAntiOn f s → (∀ (b : α), b ∈ s → a < b → f b < f a) ∧ StrictAntiOn f s
mp₃ :
  (∀ (b : α), b ∈ s → b < a → f a < f b) →
    (∀ (b : α), b ∈ s → a < b → f b < f a) → StrictAntiOn f s → ∀ (b : α), b ∈ s → a < b → f b < f a
mp₄ :
  (∀ (b : α), b ∈ s → b < a → f a < f b) → (∀ (b : α), b ∈ s → a < b → f b < f a) → StrictAntiOn f s → StrictAntiOn f s
⊢ (∀ (b : α), b ∈ s → b < a → f a < f b) ∧ (∀ (b : α), b ∈ s → a < b → f b < f a) ∧ StrictAntiOn f s ↔
    (∀ (b : α), b ∈ s → a < b → f b < f a) ∧ StrictAntiOn f s
have mpr₁ : (∀ (b : α), b ∈ s → a < b → f b < f a) →
  StrictAntiOn f s → (∀ (b : α), b ∈ s → b < a → f a < f b) ∧ (∀ (b : α), b ∈ s → a < b → f b < f a) ∧ StrictAntiOn f s
Tactic: tauto
-- Lean 4 proof step from Mathlib.Data.Set.Monotone (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
f : α → β
s : Set α
a : α
ha : ∀ (x : α), x ∈ s → a ≤ x
this : ∀ (b : α), b ∈ s → b < a → f a < f b
mp :
  (∀ (b : α), b ∈ s → b < a → f a < f b) ∧ (∀ (b : α), b ∈ s → a < b → f b < f a) ∧ StrictAntiOn f s →
    (∀ (b : α), b ∈ s → a < b → f b < f a) ∧ StrictAntiOn f s
mpr :
  (∀ (b : α), b ∈ s → a < b → f b < f a) ∧ StrictAntiOn f s →
    (∀ (b : α), b ∈ s → b < a → f a < f b) ∧ (∀ (b : α), b ∈ s → a < b → f b < f a) ∧ StrictAntiOn f s
mp₁ mp₂ :
  (∀ (b : α), b ∈ s → b < a → f a < f b) →
    (∀ (b : α), b ∈ s → a < b → f b < f a) →
      StrictAntiOn f s → (∀ (b : α), b ∈ s → a < b → f b < f a) ∧ StrictAntiOn f s
mp₃ :
  (∀ (b : α), b ∈ s → b < a → f a < f b) →
    (∀ (b : α), b ∈ s → a < b → f b < f a) → StrictAntiOn f s → ∀ (b : α), b ∈ s → a < b → f b < f a
mp₄ :
  (∀ (b : α), b ∈ s → b < a → f a < f b) → (∀ (b : α), b ∈ s → a < b → f b < f a) → StrictAntiOn f s → StrictAntiOn f s
mpr₁ mpr₂ :
  (∀ (b : α), b ∈ s → a < b → f b < f a) →
    StrictAntiOn f s →
      (∀ (b : α), b ∈ s → b < a → f a < f b) ∧ (∀ (b : α), b ∈ s → a < b → f b < f a) ∧ StrictAntiOn f s
⊢ (∀ (b : α), b ∈ s → b < a → f a < f b) ∧ (∀ (b : α), b ∈ s → a < b → f b < f a) ∧ StrictAntiOn f s ↔
    (∀ (b : α), b ∈ s → a < b → f b < f a) ∧ StrictAntiOn f s
have mpr₃ : (∀ (b : α), b ∈ s → a < b → f b < f a) → StrictAntiOn f s → ∀ (b : α), b ∈ s → b < a → f a < f b
Tactic: tauto
-- Lean 4 proof step from Mathlib.Data.Set.Monotone (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
f : α → β
s : Set α
a : α
ha : ∀ (x : α), x ∈ s → a ≤ x
this : ∀ (b : α), b ∈ s → b < a → f a < f b
mp :
  (∀ (b : α), b ∈ s → b < a → f a < f b) ∧ (∀ (b : α), b ∈ s → a < b → f b < f a) ∧ StrictAntiOn f s →
    (∀ (b : α), b ∈ s → a < b → f b < f a) ∧ StrictAntiOn f s
mpr :
  (∀ (b : α), b ∈ s → a < b → f b < f a) ∧ StrictAntiOn f s →
    (∀ (b : α), b ∈ s → b < a → f a < f b) ∧ (∀ (b : α), b ∈ s → a < b → f b < f a) ∧ StrictAntiOn f s
mp₁ mp₂ :
  (∀ (b : α), b ∈ s → b < a → f a < f b) →
    (∀ (b : α), b ∈ s → a < b → f b < f a) →
      StrictAntiOn f s → (∀ (b : α), b ∈ s → a < b → f b < f a) ∧ StrictAntiOn f s
mp₃ :
  (∀ (b : α), b ∈ s → b < a → f a < f b) →
    (∀ (b : α), b ∈ s → a < b → f b < f a) → StrictAntiOn f s → ∀ (b : α), b ∈ s → a < b → f b < f a
mp₄ :
  (∀ (b : α), b ∈ s → b < a → f a < f b) → (∀ (b : α), b ∈ s → a < b → f b < f a) → StrictAntiOn f s → StrictAntiOn f s
mpr₁ mpr₂ :
  (∀ (b : α), b ∈ s → a < b → f b < f a) →
    StrictAntiOn f s →
      (∀ (b : α), b ∈ s → b < a → f a < f b) ∧ (∀ (b : α), b ∈ s → a < b → f b < f a) ∧ StrictAntiOn f s
mpr₃ : (∀ (b : α), b ∈ s → a < b → f b < f a) → StrictAntiOn f s → ∀ (b : α), b ∈ s → b < a → f a < f b
⊢ (∀ (b : α), b ∈ s → b < a → f a < f b) ∧ (∀ (b : α), b ∈ s → a < b → f b < f a) ∧ StrictAntiOn f s ↔
    (∀ (b : α), b ∈ s → a < b → f b < f a) ∧ StrictAntiOn f s
have mpr₄ : (∀ (b : α), b ∈ s → a < b → f b < f a) → StrictAntiOn f s → ∀ (b : α), b ∈ s → a < b → f b < f a
Tactic: tauto
-- Lean 4 proof step from Mathlib.Data.Set.Monotone (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
f : α → β
s : Set α
a : α
ha : ∀ (x : α), x ∈ s → a ≤ x
this : ∀ (b : α), b ∈ s → b < a → f a < f b
mp :
  (∀ (b : α), b ∈ s → b < a → f a < f b) ∧ (∀ (b : α), b ∈ s → a < b → f b < f a) ∧ StrictAntiOn f s →
    (∀ (b : α), b ∈ s → a < b → f b < f a) ∧ StrictAntiOn f s
mpr :
  (∀ (b : α), b ∈ s → a < b → f b < f a) ∧ StrictAntiOn f s →
    (∀ (b : α), b ∈ s → b < a → f a < f b) ∧ (∀ (b : α), b ∈ s → a < b → f b < f a) ∧ StrictAntiOn f s
mp₁ mp₂ :
  (∀ (b : α), b ∈ s → b < a → f a < f b) →
    (∀ (b : α), b ∈ s → a < b → f b < f a) →
      StrictAntiOn f s → (∀ (b : α), b ∈ s → a < b → f b < f a) ∧ StrictAntiOn f s
mp₃ :
  (∀ (b : α), b ∈ s → b < a → f a < f b) →
    (∀ (b : α), b ∈ s → a < b → f b < f a) → StrictAntiOn f s → ∀ (b : α), b ∈ s → a < b → f b < f a
mp₄ :
  (∀ (b : α), b ∈ s → b < a → f a < f b) → (∀ (b : α), b ∈ s → a < b → f b < f a) → StrictAntiOn f s → StrictAntiOn f s
mpr₁ mpr₂ :
  (∀ (b : α), b ∈ s → a < b → f b < f a) →
    StrictAntiOn f s →
      (∀ (b : α), b ∈ s → b < a → f a < f b) ∧ (∀ (b : α), b ∈ s → a < b → f b < f a) ∧ StrictAntiOn f s
mpr₃ : (∀ (b : α), b ∈ s → a < b → f b < f a) → StrictAntiOn f s → ∀ (b : α), b ∈ s → b < a → f a < f b
mpr₄ : (∀ (b : α), b ∈ s → a < b → f b < f a) → StrictAntiOn f s → ∀ (b : α), b ∈ s → a < b → f b < f a
⊢ (∀ (b : α), b ∈ s → b < a → f a < f b) ∧ (∀ (b : α), b ∈ s → a < b → f b < f a) ∧ StrictAntiOn f s ↔
    (∀ (b : α), b ∈ s → a < b → f b < f a) ∧ StrictAntiOn f s
have mpr₅ : (∀ (b : α), b ∈ s → a < b → f b < f a) → StrictAntiOn f s → StrictAntiOn f s
Tactic: tauto
-- Lean 4 proof step from Mathlib.Data.Set.Monotone (goal)
Goal:
α : Type u_4
β : Type u_5
inst : PartialOrder α
inst_1 : LinearOrder β
φ : β → α
ψ : α → β
t : Set β
s : Set α
hφ : MonotoneOn φ t
φψs : RightInvOn ψ φ s
ψts : MapsTo ψ s t
x : α
xs : x ∈ s
y : α
ys : y ∈ s
l : x ≤ y
⊢ ψ x ≤ ψ y
have inl : ∀ (ψxy : ψ x ≤ ψ y), ψ x ≤ ψ y
Tactic: rcases le_total (ψ x) (ψ y) with (ψxy | ψyx)
-- Lean 4 proof step from Mathlib.Data.Set.Monotone (goal)
Goal:
α : Type u_4
β : Type u_5
inst : PartialOrder α
inst_1 : LinearOrder β
φ : β → α
ψ : α → β
t : Set β
s : Set α
hφ : MonotoneOn φ t
φψs : RightInvOn ψ φ s
ψts : MapsTo ψ s t
x : α
xs : x ∈ s
y : α
ys : y ∈ s
l : x ≤ y
inl : ∀ (ψxy : ψ x ≤ ψ y), ψ x ≤ ψ y
⊢ ψ x ≤ ψ y
have inr : ∀ (ψyx : ψ y ≤ ψ x), ψ x ≤ ψ y
Tactic: rcases le_total (ψ x) (ψ y) with (ψxy | ψyx)