awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Set.MemPartition (goal)
Goal:
α : Type u_1
f : ℕ → Set α
n : ℕ
a : α
s : Set α
hs : s ∈ memPartition f n
h : a ∈ s
h_ne : ¬memPartitionSet f n a = s
h_disj : Disjoint s (memPartitionSet f n a)
⊢ ¬Disjoint s (memPartitionSet f n a)
have rw : (s ∩ memPartitionSet f n a).Nonempty
Tactic: rw [not_disjoint_iff_nonempty_inter]
-- Lean 4 proof step from Mathlib.Data.Set.Monotone (goal)
Goal:
α : Type u_1
β : Type u_2
s : Set α
f₁ f₂ : α → β
inst : Preorder α
inst_1 : Preorder β
h₁ : MonotoneOn f₁ s
h : EqOn f₁ f₂ s
a : α
ha : a ∈ s
b : α
hb : b ∈ s
hab : a ≤ b
⊢ f₂ a ≤ f₂ b
have rw : f₁ a ≤ f₁ b
Tactic: rw [← h ha, ← h hb]
-- Lean 4 proof step from Mathlib.Data.Set.Monotone (goal)
Goal:
α : Type u_1
β : Type u_2
s : Set α
f₁ f₂ : α → β
inst : Preorder α
inst_1 : Preorder β
h₁ : StrictMonoOn f₁ s
h : EqOn f₁ f₂ s
a : α
ha : a ∈ s
b : α
hb : b ∈ s
hab : a < b
⊢ f₂ a < f₂ b
have rw : f₁ a < f₁ b
Tactic: rw [← h ha, ← h hb]
-- 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
⊢ StrictMonoOn f (insert a s) ↔ (∀ (b : α), b ∈ s → b < a → f b < f a) ∧ StrictMonoOn f s
have rw : (∀ (b : α), b ∈ s → b < a → f b < f a) ∧ (∀ (b : α), b ∈ s → a < b → f a < f b) ∧ StrictMonoOn f s ↔
  (∀ (b : α), b ∈ s → b < a → f b < f a) ∧ StrictMonoOn f s
Tactic: rw [strictMonoOn_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 b < f a) ∧ (∀ (b : α), b ∈ s → a < b → f a < f b) ∧ StrictMonoOn f s ↔
    (∀ (b : α), b ∈ s → b < a → f b < f a) ∧ StrictMonoOn f s
have this : ∀ (b : α), b ∈ s → a < b → f a < f b
Tactic: have : ∀ b ∈ s, a < b → 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 → x ≤ a
this : ∀ (b : α), b ∈ s → a < b → f a < f b
⊢ (∀ (b : α), b ∈ s → b < a → f b < f a) ∧ (∀ (b : α), b ∈ s → a < b → f a < f b) ∧ StrictMonoOn f s ↔
    (∀ (b : α), b ∈ s → b < a → f b < f a) ∧ StrictMonoOn f s
have mp : (∀ (b : α), b ∈ s → b < a → f b < f a) ∧ (∀ (b : α), b ∈ s → a < b → f a < f b) ∧ StrictMonoOn f s →
  (∀ (b : α), b ∈ s → b < a → f b < f a) ∧ StrictMonoOn 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 a < f b
mp :
  (∀ (b : α), b ∈ s → b < a → f b < f a) ∧ (∀ (b : α), b ∈ s → a < b → f a < f b) ∧ StrictMonoOn f s →
    (∀ (b : α), b ∈ s → b < a → f b < f a) ∧ StrictMonoOn f s
⊢ (∀ (b : α), b ∈ s → b < a → f b < f a) ∧ (∀ (b : α), b ∈ s → a < b → f a < f b) ∧ StrictMonoOn f s ↔
    (∀ (b : α), b ∈ s → b < a → f b < f a) ∧ StrictMonoOn f s
have mpr : (∀ (b : α), b ∈ s → b < a → f b < f a) ∧ StrictMonoOn f s →
  (∀ (b : α), b ∈ s → b < a → f b < f a) ∧ (∀ (b : α), b ∈ s → a < b → f a < f b) ∧ StrictMonoOn 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 a < f b
mp :
  (∀ (b : α), b ∈ s → b < a → f b < f a) ∧ (∀ (b : α), b ∈ s → a < b → f a < f b) ∧ StrictMonoOn f s →
    (∀ (b : α), b ∈ s → b < a → f b < f a) ∧ StrictMonoOn f s
mpr :
  (∀ (b : α), b ∈ s → b < a → f b < f a) ∧ StrictMonoOn f s →
    (∀ (b : α), b ∈ s → b < a → f b < f a) ∧ (∀ (b : α), b ∈ s → a < b → f a < f b) ∧ StrictMonoOn f s
⊢ (∀ (b : α), b ∈ s → b < a → f b < f a) ∧ (∀ (b : α), b ∈ s → a < b → f a < f b) ∧ StrictMonoOn f s ↔
    (∀ (b : α), b ∈ s → b < a → f b < f a) ∧ StrictMonoOn f s
have mp₁ : (∀ (b : α), b ∈ s → b < a → f b < f a) →
  (∀ (b : α), b ∈ s → a < b → f a < f b) → StrictMonoOn f s → (∀ (b : α), b ∈ s → b < a → f b < f a) ∧ StrictMonoOn 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 a < f b
mp :
  (∀ (b : α), b ∈ s → b < a → f b < f a) ∧ (∀ (b : α), b ∈ s → a < b → f a < f b) ∧ StrictMonoOn f s →
    (∀ (b : α), b ∈ s → b < a → f b < f a) ∧ StrictMonoOn f s
mpr :
  (∀ (b : α), b ∈ s → b < a → f b < f a) ∧ StrictMonoOn f s →
    (∀ (b : α), b ∈ s → b < a → f b < f a) ∧ (∀ (b : α), b ∈ s → a < b → f a < f b) ∧ StrictMonoOn f s
mp₁ mp₂ :
  (∀ (b : α), b ∈ s → b < a → f b < f a) →
    (∀ (b : α), b ∈ s → a < b → f a < f b) →
      StrictMonoOn f s → (∀ (b : α), b ∈ s → b < a → f b < f a) ∧ StrictMonoOn f s
⊢ (∀ (b : α), b ∈ s → b < a → f b < f a) ∧ (∀ (b : α), b ∈ s → a < b → f a < f b) ∧ StrictMonoOn f s ↔
    (∀ (b : α), b ∈ s → b < a → f b < f a) ∧ StrictMonoOn f s
have mp₃ : (∀ (b : α), b ∈ s → b < a → f b < f a) →
  (∀ (b : α), b ∈ s → a < b → f a < f b) → StrictMonoOn f s → ∀ (b : α), b ∈ s → b < a → 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 a < f b
mp :
  (∀ (b : α), b ∈ s → b < a → f b < f a) ∧ (∀ (b : α), b ∈ s → a < b → f a < f b) ∧ StrictMonoOn f s →
    (∀ (b : α), b ∈ s → b < a → f b < f a) ∧ StrictMonoOn f s
mpr :
  (∀ (b : α), b ∈ s → b < a → f b < f a) ∧ StrictMonoOn f s →
    (∀ (b : α), b ∈ s → b < a → f b < f a) ∧ (∀ (b : α), b ∈ s → a < b → f a < f b) ∧ StrictMonoOn f s
mp₁ mp₂ :
  (∀ (b : α), b ∈ s → b < a → f b < f a) →
    (∀ (b : α), b ∈ s → a < b → f a < f b) →
      StrictMonoOn f s → (∀ (b : α), b ∈ s → b < a → f b < f a) ∧ StrictMonoOn f s
mp₃ :
  (∀ (b : α), b ∈ s → b < a → f b < f a) →
    (∀ (b : α), b ∈ s → a < b → f a < f b) → StrictMonoOn f s → ∀ (b : α), b ∈ s → b < a → f b < f a
⊢ (∀ (b : α), b ∈ s → b < a → f b < f a) ∧ (∀ (b : α), b ∈ s → a < b → f a < f b) ∧ StrictMonoOn f s ↔
    (∀ (b : α), b ∈ s → b < a → f b < f a) ∧ StrictMonoOn f s
have mp₄ : (∀ (b : α), b ∈ s → b < a → f b < f a) → (∀ (b : α), b ∈ s → a < b → f a < f b) → StrictMonoOn f s → StrictMonoOn 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 a < f b
mp :
  (∀ (b : α), b ∈ s → b < a → f b < f a) ∧ (∀ (b : α), b ∈ s → a < b → f a < f b) ∧ StrictMonoOn f s →
    (∀ (b : α), b ∈ s → b < a → f b < f a) ∧ StrictMonoOn f s
mpr :
  (∀ (b : α), b ∈ s → b < a → f b < f a) ∧ StrictMonoOn f s →
    (∀ (b : α), b ∈ s → b < a → f b < f a) ∧ (∀ (b : α), b ∈ s → a < b → f a < f b) ∧ StrictMonoOn f s
mp₁ mp₂ :
  (∀ (b : α), b ∈ s → b < a → f b < f a) →
    (∀ (b : α), b ∈ s → a < b → f a < f b) →
      StrictMonoOn f s → (∀ (b : α), b ∈ s → b < a → f b < f a) ∧ StrictMonoOn f s
mp₃ :
  (∀ (b : α), b ∈ s → b < a → f b < f a) →
    (∀ (b : α), b ∈ s → a < b → f a < f b) → StrictMonoOn f s → ∀ (b : α), b ∈ s → b < a → f b < f a
mp₄ :
  (∀ (b : α), b ∈ s → b < a → f b < f a) → (∀ (b : α), b ∈ s → a < b → f a < f b) → StrictMonoOn f s → StrictMonoOn f s
⊢ (∀ (b : α), b ∈ s → b < a → f b < f a) ∧ (∀ (b : α), b ∈ s → a < b → f a < f b) ∧ StrictMonoOn f s ↔
    (∀ (b : α), b ∈ s → b < a → f b < f a) ∧ StrictMonoOn f s
have mpr₁ : (∀ (b : α), b ∈ s → b < a → f b < f a) →
  StrictMonoOn f s → (∀ (b : α), b ∈ s → b < a → f b < f a) ∧ (∀ (b : α), b ∈ s → a < b → f a < f b) ∧ StrictMonoOn 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 a < f b
mp :
  (∀ (b : α), b ∈ s → b < a → f b < f a) ∧ (∀ (b : α), b ∈ s → a < b → f a < f b) ∧ StrictMonoOn f s →
    (∀ (b : α), b ∈ s → b < a → f b < f a) ∧ StrictMonoOn f s
mpr :
  (∀ (b : α), b ∈ s → b < a → f b < f a) ∧ StrictMonoOn f s →
    (∀ (b : α), b ∈ s → b < a → f b < f a) ∧ (∀ (b : α), b ∈ s → a < b → f a < f b) ∧ StrictMonoOn f s
mp₁ mp₂ :
  (∀ (b : α), b ∈ s → b < a → f b < f a) →
    (∀ (b : α), b ∈ s → a < b → f a < f b) →
      StrictMonoOn f s → (∀ (b : α), b ∈ s → b < a → f b < f a) ∧ StrictMonoOn f s
mp₃ :
  (∀ (b : α), b ∈ s → b < a → f b < f a) →
    (∀ (b : α), b ∈ s → a < b → f a < f b) → StrictMonoOn f s → ∀ (b : α), b ∈ s → b < a → f b < f a
mp₄ :
  (∀ (b : α), b ∈ s → b < a → f b < f a) → (∀ (b : α), b ∈ s → a < b → f a < f b) → StrictMonoOn f s → StrictMonoOn f s
mpr₁ mpr₂ :
  (∀ (b : α), b ∈ s → b < a → f b < f a) →
    StrictMonoOn f s →
      (∀ (b : α), b ∈ s → b < a → f b < f a) ∧ (∀ (b : α), b ∈ s → a < b → f a < f b) ∧ StrictMonoOn f s
⊢ (∀ (b : α), b ∈ s → b < a → f b < f a) ∧ (∀ (b : α), b ∈ s → a < b → f a < f b) ∧ StrictMonoOn f s ↔
    (∀ (b : α), b ∈ s → b < a → f b < f a) ∧ StrictMonoOn f s
have mpr₃ : (∀ (b : α), b ∈ s → b < a → f b < f a) → StrictMonoOn f s → ∀ (b : α), b ∈ s → b < a → 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 a < f b
mp :
  (∀ (b : α), b ∈ s → b < a → f b < f a) ∧ (∀ (b : α), b ∈ s → a < b → f a < f b) ∧ StrictMonoOn f s →
    (∀ (b : α), b ∈ s → b < a → f b < f a) ∧ StrictMonoOn f s
mpr :
  (∀ (b : α), b ∈ s → b < a → f b < f a) ∧ StrictMonoOn f s →
    (∀ (b : α), b ∈ s → b < a → f b < f a) ∧ (∀ (b : α), b ∈ s → a < b → f a < f b) ∧ StrictMonoOn f s
mp₁ mp₂ :
  (∀ (b : α), b ∈ s → b < a → f b < f a) →
    (∀ (b : α), b ∈ s → a < b → f a < f b) →
      StrictMonoOn f s → (∀ (b : α), b ∈ s → b < a → f b < f a) ∧ StrictMonoOn f s
mp₃ :
  (∀ (b : α), b ∈ s → b < a → f b < f a) →
    (∀ (b : α), b ∈ s → a < b → f a < f b) → StrictMonoOn f s → ∀ (b : α), b ∈ s → b < a → f b < f a
mp₄ :
  (∀ (b : α), b ∈ s → b < a → f b < f a) → (∀ (b : α), b ∈ s → a < b → f a < f b) → StrictMonoOn f s → StrictMonoOn f s
mpr₁ mpr₂ :
  (∀ (b : α), b ∈ s → b < a → f b < f a) →
    StrictMonoOn f s →
      (∀ (b : α), b ∈ s → b < a → f b < f a) ∧ (∀ (b : α), b ∈ s → a < b → f a < f b) ∧ StrictMonoOn f s
mpr₃ : (∀ (b : α), b ∈ s → b < a → f b < f a) → StrictMonoOn f s → ∀ (b : α), b ∈ s → b < a → f b < f a
⊢ (∀ (b : α), b ∈ s → b < a → f b < f a) ∧ (∀ (b : α), b ∈ s → a < b → f a < f b) ∧ StrictMonoOn f s ↔
    (∀ (b : α), b ∈ s → b < a → f b < f a) ∧ StrictMonoOn f s
have mpr₄ : (∀ (b : α), b ∈ s → b < a → f b < f a) → StrictMonoOn f s → ∀ (b : α), b ∈ s → a < b → 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 a < f b
mp :
  (∀ (b : α), b ∈ s → b < a → f b < f a) ∧ (∀ (b : α), b ∈ s → a < b → f a < f b) ∧ StrictMonoOn f s →
    (∀ (b : α), b ∈ s → b < a → f b < f a) ∧ StrictMonoOn f s
mpr :
  (∀ (b : α), b ∈ s → b < a → f b < f a) ∧ StrictMonoOn f s →
    (∀ (b : α), b ∈ s → b < a → f b < f a) ∧ (∀ (b : α), b ∈ s → a < b → f a < f b) ∧ StrictMonoOn f s
mp₁ mp₂ :
  (∀ (b : α), b ∈ s → b < a → f b < f a) →
    (∀ (b : α), b ∈ s → a < b → f a < f b) →
      StrictMonoOn f s → (∀ (b : α), b ∈ s → b < a → f b < f a) ∧ StrictMonoOn f s
mp₃ :
  (∀ (b : α), b ∈ s → b < a → f b < f a) →
    (∀ (b : α), b ∈ s → a < b → f a < f b) → StrictMonoOn f s → ∀ (b : α), b ∈ s → b < a → f b < f a
mp₄ :
  (∀ (b : α), b ∈ s → b < a → f b < f a) → (∀ (b : α), b ∈ s → a < b → f a < f b) → StrictMonoOn f s → StrictMonoOn f s
mpr₁ mpr₂ :
  (∀ (b : α), b ∈ s → b < a → f b < f a) →
    StrictMonoOn f s →
      (∀ (b : α), b ∈ s → b < a → f b < f a) ∧ (∀ (b : α), b ∈ s → a < b → f a < f b) ∧ StrictMonoOn f s
mpr₃ : (∀ (b : α), b ∈ s → b < a → f b < f a) → StrictMonoOn f s → ∀ (b : α), b ∈ s → b < a → f b < f a
mpr₄ : (∀ (b : α), b ∈ s → b < a → f b < f a) → StrictMonoOn f s → ∀ (b : α), b ∈ s → a < b → f a < f b
⊢ (∀ (b : α), b ∈ s → b < a → f b < f a) ∧ (∀ (b : α), b ∈ s → a < b → f a < f b) ∧ StrictMonoOn f s ↔
    (∀ (b : α), b ∈ s → b < a → f b < f a) ∧ StrictMonoOn f s
have mpr₅ : (∀ (b : α), b ∈ s → b < a → f b < f a) → StrictMonoOn f s → StrictMonoOn 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
⊢ StrictMonoOn f (insert a s) ↔ (∀ (b : α), b ∈ s → a < b → f a < f b) ∧ StrictMonoOn f s
have rw : (∀ (b : α), b ∈ s → b < a → f b < f a) ∧ (∀ (b : α), b ∈ s → a < b → f a < f b) ∧ StrictMonoOn f s ↔
  (∀ (b : α), b ∈ s → a < b → f a < f b) ∧ StrictMonoOn f s
Tactic: rw [strictMonoOn_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 b < f a) ∧ (∀ (b : α), b ∈ s → a < b → f a < f b) ∧ StrictMonoOn f s ↔
    (∀ (b : α), b ∈ s → a < b → f a < f b) ∧ StrictMonoOn f s
have this : ∀ (b : α), b ∈ s → b < a → f b < f a
Tactic: have : ∀ b ∈ s, b < a → 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 → a ≤ x
this : ∀ (b : α), b ∈ s → b < a → f b < f a
⊢ (∀ (b : α), b ∈ s → b < a → f b < f a) ∧ (∀ (b : α), b ∈ s → a < b → f a < f b) ∧ StrictMonoOn f s ↔
    (∀ (b : α), b ∈ s → a < b → f a < f b) ∧ StrictMonoOn f s
have mp : (∀ (b : α), b ∈ s → b < a → f b < f a) ∧ (∀ (b : α), b ∈ s → a < b → f a < f b) ∧ StrictMonoOn f s →
  (∀ (b : α), b ∈ s → a < b → f a < f b) ∧ StrictMonoOn 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 b < f a
mp :
  (∀ (b : α), b ∈ s → b < a → f b < f a) ∧ (∀ (b : α), b ∈ s → a < b → f a < f b) ∧ StrictMonoOn f s →
    (∀ (b : α), b ∈ s → a < b → f a < f b) ∧ StrictMonoOn f s
⊢ (∀ (b : α), b ∈ s → b < a → f b < f a) ∧ (∀ (b : α), b ∈ s → a < b → f a < f b) ∧ StrictMonoOn f s ↔
    (∀ (b : α), b ∈ s → a < b → f a < f b) ∧ StrictMonoOn f s
have mpr : (∀ (b : α), b ∈ s → a < b → f a < f b) ∧ StrictMonoOn f s →
  (∀ (b : α), b ∈ s → b < a → f b < f a) ∧ (∀ (b : α), b ∈ s → a < b → f a < f b) ∧ StrictMonoOn 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 b < f a
mp :
  (∀ (b : α), b ∈ s → b < a → f b < f a) ∧ (∀ (b : α), b ∈ s → a < b → f a < f b) ∧ StrictMonoOn f s →
    (∀ (b : α), b ∈ s → a < b → f a < f b) ∧ StrictMonoOn f s
mpr :
  (∀ (b : α), b ∈ s → a < b → f a < f b) ∧ StrictMonoOn f s →
    (∀ (b : α), b ∈ s → b < a → f b < f a) ∧ (∀ (b : α), b ∈ s → a < b → f a < f b) ∧ StrictMonoOn f s
⊢ (∀ (b : α), b ∈ s → b < a → f b < f a) ∧ (∀ (b : α), b ∈ s → a < b → f a < f b) ∧ StrictMonoOn f s ↔
    (∀ (b : α), b ∈ s → a < b → f a < f b) ∧ StrictMonoOn f s
have mp₁ : (∀ (b : α), b ∈ s → b < a → f b < f a) →
  (∀ (b : α), b ∈ s → a < b → f a < f b) → StrictMonoOn f s → (∀ (b : α), b ∈ s → a < b → f a < f b) ∧ StrictMonoOn 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 b < f a
mp :
  (∀ (b : α), b ∈ s → b < a → f b < f a) ∧ (∀ (b : α), b ∈ s → a < b → f a < f b) ∧ StrictMonoOn f s →
    (∀ (b : α), b ∈ s → a < b → f a < f b) ∧ StrictMonoOn f s
mpr :
  (∀ (b : α), b ∈ s → a < b → f a < f b) ∧ StrictMonoOn f s →
    (∀ (b : α), b ∈ s → b < a → f b < f a) ∧ (∀ (b : α), b ∈ s → a < b → f a < f b) ∧ StrictMonoOn f s
mp₁ mp₂ :
  (∀ (b : α), b ∈ s → b < a → f b < f a) →
    (∀ (b : α), b ∈ s → a < b → f a < f b) →
      StrictMonoOn f s → (∀ (b : α), b ∈ s → a < b → f a < f b) ∧ StrictMonoOn f s
⊢ (∀ (b : α), b ∈ s → b < a → f b < f a) ∧ (∀ (b : α), b ∈ s → a < b → f a < f b) ∧ StrictMonoOn f s ↔
    (∀ (b : α), b ∈ s → a < b → f a < f b) ∧ StrictMonoOn f s
have mp₃ : (∀ (b : α), b ∈ s → b < a → f b < f a) →
  (∀ (b : α), b ∈ s → a < b → f a < f b) → StrictMonoOn f s → ∀ (b : α), b ∈ s → a < b → 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 b < f a
mp :
  (∀ (b : α), b ∈ s → b < a → f b < f a) ∧ (∀ (b : α), b ∈ s → a < b → f a < f b) ∧ StrictMonoOn f s →
    (∀ (b : α), b ∈ s → a < b → f a < f b) ∧ StrictMonoOn f s
mpr :
  (∀ (b : α), b ∈ s → a < b → f a < f b) ∧ StrictMonoOn f s →
    (∀ (b : α), b ∈ s → b < a → f b < f a) ∧ (∀ (b : α), b ∈ s → a < b → f a < f b) ∧ StrictMonoOn f s
mp₁ mp₂ :
  (∀ (b : α), b ∈ s → b < a → f b < f a) →
    (∀ (b : α), b ∈ s → a < b → f a < f b) →
      StrictMonoOn f s → (∀ (b : α), b ∈ s → a < b → f a < f b) ∧ StrictMonoOn f s
mp₃ :
  (∀ (b : α), b ∈ s → b < a → f b < f a) →
    (∀ (b : α), b ∈ s → a < b → f a < f b) → StrictMonoOn f s → ∀ (b : α), b ∈ s → a < b → f a < f b
⊢ (∀ (b : α), b ∈ s → b < a → f b < f a) ∧ (∀ (b : α), b ∈ s → a < b → f a < f b) ∧ StrictMonoOn f s ↔
    (∀ (b : α), b ∈ s → a < b → f a < f b) ∧ StrictMonoOn f s
have mp₄ : (∀ (b : α), b ∈ s → b < a → f b < f a) → (∀ (b : α), b ∈ s → a < b → f a < f b) → StrictMonoOn f s → StrictMonoOn 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 b < f a
mp :
  (∀ (b : α), b ∈ s → b < a → f b < f a) ∧ (∀ (b : α), b ∈ s → a < b → f a < f b) ∧ StrictMonoOn f s →
    (∀ (b : α), b ∈ s → a < b → f a < f b) ∧ StrictMonoOn f s
mpr :
  (∀ (b : α), b ∈ s → a < b → f a < f b) ∧ StrictMonoOn f s →
    (∀ (b : α), b ∈ s → b < a → f b < f a) ∧ (∀ (b : α), b ∈ s → a < b → f a < f b) ∧ StrictMonoOn f s
mp₁ mp₂ :
  (∀ (b : α), b ∈ s → b < a → f b < f a) →
    (∀ (b : α), b ∈ s → a < b → f a < f b) →
      StrictMonoOn f s → (∀ (b : α), b ∈ s → a < b → f a < f b) ∧ StrictMonoOn f s
mp₃ :
  (∀ (b : α), b ∈ s → b < a → f b < f a) →
    (∀ (b : α), b ∈ s → a < b → f a < f b) → StrictMonoOn f s → ∀ (b : α), b ∈ s → a < b → f a < f b
mp₄ :
  (∀ (b : α), b ∈ s → b < a → f b < f a) → (∀ (b : α), b ∈ s → a < b → f a < f b) → StrictMonoOn f s → StrictMonoOn f s
⊢ (∀ (b : α), b ∈ s → b < a → f b < f a) ∧ (∀ (b : α), b ∈ s → a < b → f a < f b) ∧ StrictMonoOn f s ↔
    (∀ (b : α), b ∈ s → a < b → f a < f b) ∧ StrictMonoOn f s
have mpr₁ : (∀ (b : α), b ∈ s → a < b → f a < f b) →
  StrictMonoOn f s → (∀ (b : α), b ∈ s → b < a → f b < f a) ∧ (∀ (b : α), b ∈ s → a < b → f a < f b) ∧ StrictMonoOn 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 b < f a
mp :
  (∀ (b : α), b ∈ s → b < a → f b < f a) ∧ (∀ (b : α), b ∈ s → a < b → f a < f b) ∧ StrictMonoOn f s →
    (∀ (b : α), b ∈ s → a < b → f a < f b) ∧ StrictMonoOn f s
mpr :
  (∀ (b : α), b ∈ s → a < b → f a < f b) ∧ StrictMonoOn f s →
    (∀ (b : α), b ∈ s → b < a → f b < f a) ∧ (∀ (b : α), b ∈ s → a < b → f a < f b) ∧ StrictMonoOn f s
mp₁ mp₂ :
  (∀ (b : α), b ∈ s → b < a → f b < f a) →
    (∀ (b : α), b ∈ s → a < b → f a < f b) →
      StrictMonoOn f s → (∀ (b : α), b ∈ s → a < b → f a < f b) ∧ StrictMonoOn f s
mp₃ :
  (∀ (b : α), b ∈ s → b < a → f b < f a) →
    (∀ (b : α), b ∈ s → a < b → f a < f b) → StrictMonoOn f s → ∀ (b : α), b ∈ s → a < b → f a < f b
mp₄ :
  (∀ (b : α), b ∈ s → b < a → f b < f a) → (∀ (b : α), b ∈ s → a < b → f a < f b) → StrictMonoOn f s → StrictMonoOn f s
mpr₁ mpr₂ :
  (∀ (b : α), b ∈ s → a < b → f a < f b) →
    StrictMonoOn f s →
      (∀ (b : α), b ∈ s → b < a → f b < f a) ∧ (∀ (b : α), b ∈ s → a < b → f a < f b) ∧ StrictMonoOn f s
⊢ (∀ (b : α), b ∈ s → b < a → f b < f a) ∧ (∀ (b : α), b ∈ s → a < b → f a < f b) ∧ StrictMonoOn f s ↔
    (∀ (b : α), b ∈ s → a < b → f a < f b) ∧ StrictMonoOn f s
have mpr₃ : (∀ (b : α), b ∈ s → a < b → f a < f b) → StrictMonoOn f s → ∀ (b : α), b ∈ s → b < a → 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 b < f a
mp :
  (∀ (b : α), b ∈ s → b < a → f b < f a) ∧ (∀ (b : α), b ∈ s → a < b → f a < f b) ∧ StrictMonoOn f s →
    (∀ (b : α), b ∈ s → a < b → f a < f b) ∧ StrictMonoOn f s
mpr :
  (∀ (b : α), b ∈ s → a < b → f a < f b) ∧ StrictMonoOn f s →
    (∀ (b : α), b ∈ s → b < a → f b < f a) ∧ (∀ (b : α), b ∈ s → a < b → f a < f b) ∧ StrictMonoOn f s
mp₁ mp₂ :
  (∀ (b : α), b ∈ s → b < a → f b < f a) →
    (∀ (b : α), b ∈ s → a < b → f a < f b) →
      StrictMonoOn f s → (∀ (b : α), b ∈ s → a < b → f a < f b) ∧ StrictMonoOn f s
mp₃ :
  (∀ (b : α), b ∈ s → b < a → f b < f a) →
    (∀ (b : α), b ∈ s → a < b → f a < f b) → StrictMonoOn f s → ∀ (b : α), b ∈ s → a < b → f a < f b
mp₄ :
  (∀ (b : α), b ∈ s → b < a → f b < f a) → (∀ (b : α), b ∈ s → a < b → f a < f b) → StrictMonoOn f s → StrictMonoOn f s
mpr₁ mpr₂ :
  (∀ (b : α), b ∈ s → a < b → f a < f b) →
    StrictMonoOn f s →
      (∀ (b : α), b ∈ s → b < a → f b < f a) ∧ (∀ (b : α), b ∈ s → a < b → f a < f b) ∧ StrictMonoOn f s
mpr₃ : (∀ (b : α), b ∈ s → a < b → f a < f b) → StrictMonoOn f s → ∀ (b : α), b ∈ s → b < a → f b < f a
⊢ (∀ (b : α), b ∈ s → b < a → f b < f a) ∧ (∀ (b : α), b ∈ s → a < b → f a < f b) ∧ StrictMonoOn f s ↔
    (∀ (b : α), b ∈ s → a < b → f a < f b) ∧ StrictMonoOn f s
have mpr₄ : (∀ (b : α), b ∈ s → a < b → f a < f b) → StrictMonoOn f s → ∀ (b : α), b ∈ s → a < b → 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 b < f a
mp :
  (∀ (b : α), b ∈ s → b < a → f b < f a) ∧ (∀ (b : α), b ∈ s → a < b → f a < f b) ∧ StrictMonoOn f s →
    (∀ (b : α), b ∈ s → a < b → f a < f b) ∧ StrictMonoOn f s
mpr :
  (∀ (b : α), b ∈ s → a < b → f a < f b) ∧ StrictMonoOn f s →
    (∀ (b : α), b ∈ s → b < a → f b < f a) ∧ (∀ (b : α), b ∈ s → a < b → f a < f b) ∧ StrictMonoOn f s
mp₁ mp₂ :
  (∀ (b : α), b ∈ s → b < a → f b < f a) →
    (∀ (b : α), b ∈ s → a < b → f a < f b) →
      StrictMonoOn f s → (∀ (b : α), b ∈ s → a < b → f a < f b) ∧ StrictMonoOn f s
mp₃ :
  (∀ (b : α), b ∈ s → b < a → f b < f a) →
    (∀ (b : α), b ∈ s → a < b → f a < f b) → StrictMonoOn f s → ∀ (b : α), b ∈ s → a < b → f a < f b
mp₄ :
  (∀ (b : α), b ∈ s → b < a → f b < f a) → (∀ (b : α), b ∈ s → a < b → f a < f b) → StrictMonoOn f s → StrictMonoOn f s
mpr₁ mpr₂ :
  (∀ (b : α), b ∈ s → a < b → f a < f b) →
    StrictMonoOn f s →
      (∀ (b : α), b ∈ s → b < a → f b < f a) ∧ (∀ (b : α), b ∈ s → a < b → f a < f b) ∧ StrictMonoOn f s
mpr₃ : (∀ (b : α), b ∈ s → a < b → f a < f b) → StrictMonoOn f s → ∀ (b : α), b ∈ s → b < a → f b < f a
mpr₄ : (∀ (b : α), b ∈ s → a < b → f a < f b) → StrictMonoOn f s → ∀ (b : α), b ∈ s → a < b → f a < f b
⊢ (∀ (b : α), b ∈ s → b < a → f b < f a) ∧ (∀ (b : α), b ∈ s → a < b → f a < f b) ∧ StrictMonoOn f s ↔
    (∀ (b : α), b ∈ s → a < b → f a < f b) ∧ StrictMonoOn f s
have mpr₅ : (∀ (b : α), b ∈ s → a < b → f a < f b) → StrictMonoOn f s → StrictMonoOn f s
Tactic: tauto