awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Order.ModularLattice (goal)
Goal:
α : Type u_1
a b c : α
inst : Lattice α
inst_1 : OrderBot α
inst_2 : IsModularLattice α
h₁ : Disjoint a (b ⊔ c)
h₂ : Disjoint b (c ⊔ a)
⊢ Disjoint c (a ⊔ b)
have rw : ∀ (h₂ : Disjoint b (a ⊔ c)), Disjoint c (b ⊔ a)
Tactic: rw [sup_comm] at h₂ ⊢
Cleared hypotheses: h₂
-- Lean 4 proof step from Mathlib.Order.ModularLattice (goal)
Goal:
α : Type u_1
a b c : α
inst : Lattice α
inst_1 : OrderBot α
inst_2 : IsModularLattice α
h₁ : Disjoint a (b ⊔ c)
h₂ : Disjoint b (a ⊔ c)
⊢ Disjoint c (b ⊔ a)
have rw : Disjoint (b ⊔ a) c
Tactic: rw [disjoint_comm]
-- Lean 4 proof step from Mathlib.Order.ModularLattice (goal)
Goal:
α : Type u_1
inst : Lattice α
inst_1 : BoundedOrder α
inst_2 : IsModularLattice α
a b c : α
h₁ : IsCompl b c
h₂ : b ≤ a
⊢ IsCompl (α := { x : α // x ∈ Iic a }) (Subtype.mk (p := fun (x : α) ↦ x ∈ Iic a) (a ⊓ b) ⋯ : { x : α // x ∈ Iic a })
    (Subtype.mk (p := fun (x : α) ↦ x ∈ Iic a) (a ⊓ c) ⋯ : { x : α // x ∈ Iic a })
have disjoint : Disjoint (α := { x : α // x ∈ Iic a }) (Subtype.mk (p := fun (x : α) ↦ x ∈ Iic a) (a ⊓ b) sorry : { x : α // x ∈ Iic a })
  (Subtype.mk (p := fun (x : α) ↦ x ∈ Iic a) (a ⊓ c) sorry : { x : α // x ∈ Iic a })
Tactic: constructor
-- Lean 4 proof step from Mathlib.Order.ModularLattice (goal)
Goal:
α : Type u_1
inst : Lattice α
inst_1 : BoundedOrder α
inst_2 : IsModularLattice α
a b c : α
h₁ : IsCompl b c
h₂ : b ≤ a
disjoint :
  Disjoint (α := { x : α // x ∈ Iic a }) (Subtype.mk (p := fun (x : α) ↦ x ∈ Iic a) (a ⊓ b) ⋯ : { x : α // x ∈ Iic a })
    (Subtype.mk (p := fun (x : α) ↦ x ∈ Iic a) (a ⊓ c) ⋯ : { x : α // x ∈ Iic a })
⊢ IsCompl (α := { x : α // x ∈ Iic a }) (Subtype.mk (p := fun (x : α) ↦ x ∈ Iic a) (a ⊓ b) ⋯ : { x : α // x ∈ Iic a })
    (Subtype.mk (p := fun (x : α) ↦ x ∈ Iic a) (a ⊓ c) ⋯ : { x : α // x ∈ Iic a })
have codisjoint : Codisjoint (α := { x : α // x ∈ Iic a }) (Subtype.mk (p := fun (x : α) ↦ x ∈ Iic a) (a ⊓ b) sorry : { x : α // x ∈ Iic a })
  (Subtype.mk (p := fun (x : α) ↦ x ∈ Iic a) (a ⊓ c) sorry : { x : α // x ∈ Iic a })
Tactic: constructor
-- Lean 4 proof step from Mathlib.Order.ModularLattice (goal)
Goal:
α : Type u_1
inst : Lattice α
inst_1 : BoundedOrder α
inst_2 : IsModularLattice α
a b c : α
h₁ : IsCompl b c
h₂ : b ≤ a
⊢ Codisjoint (α := { x : α // x ∈ Iic a })
    (Subtype.mk (p := fun (x : α) ↦ x ∈ Iic a) (a ⊓ b) ⋯ : { x : α // x ∈ Iic a })
    (Subtype.mk (p := fun (x : α) ↦ x ∈ Iic a) (a ⊓ c) ⋯ : { x : α // x ∈ Iic a })
have codisjoint : (b ⊓ a ⊔ c) ⊓ a = a
Tactic: simp only [Iic.codisjoint_iff, inf_comm a, IsModularLattice.inf_sup_inf_assoc]
-- Lean 4 proof step from Mathlib.Order.ModularLattice (goal)
Goal:
α : Type u_1
inst : Lattice α
inst_1 : IsModularLattice α
a b c : α
inst_2 : BoundedOrder α
inst_3 : ComplementedLattice α
hb : a ≤ b
hc : b ≤ c
⊢ ∃ (b' : α), b ⊓ b' = a ∧ b ⊔ b' = c
have obtain : ∀ (d : α) (hdisjoint : Disjoint b d) (hcodisjoint : Codisjoint b d), ∃ (b' : α), b ⊓ b' = a ∧ b ⊔ b' = c
Tactic: obtain ⟨d, hdisjoint, hcodisjoint⟩ := exists_isCompl b
-- Lean 4 proof step from Mathlib.Order.ModularLattice (goal)
Goal:
α : Type u_1
inst : Lattice α
inst_1 : IsModularLattice α
a b c : α
inst_2 : BoundedOrder α
inst_3 : ComplementedLattice α
hb : a ≤ b
hc : b ≤ c
d : α
hdisjoint : Disjoint b d
hcodisjoint : Codisjoint b d
⊢ ∃ (b' : α), b ⊓ b' = a ∧ b ⊔ b' = c
have refine_1 : b ⊓ ((d ⊔ a) ⊓ c) = a
Tactic: refine ⟨(d ⊔ a) ⊓ c, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Order.ModularLattice (goal)
Goal:
α : Type u_1
inst : Lattice α
inst_1 : IsModularLattice α
a b c : α
inst_2 : BoundedOrder α
inst_3 : ComplementedLattice α
hb : a ≤ b
hc : b ≤ c
d : α
hdisjoint : Disjoint b d
hcodisjoint : Codisjoint b d
refine_1 : b ⊓ ((d ⊔ a) ⊓ c) = a
⊢ ∃ (b' : α), b ⊓ b' = a ∧ b ⊔ b' = c
have refine_2 : b ⊔ (d ⊔ a) ⊓ c = c
Tactic: refine ⟨(d ⊔ a) ⊓ c, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Order.ModularLattice (goal)
Goal:
α : Type u_1
inst : Lattice α
inst_1 : IsModularLattice α
a b : α
inst_2 : BoundedOrder α
inst_3 : ComplementedLattice α
h : a ≤ b
⊢ ∃ (a' : α), Disjoint a a' ∧ a ⊔ a' = b
have simp_rw : ∃ (a' : α), a ⊓ a' = ⊥ ∧ a ⊔ a' = b
Tactic: simp_rw [disjoint_iff]
-- Lean 4 proof step from Mathlib.Order.ModularLattice (goal)
Goal:
α : Type u_1
inst : Lattice α
inst_1 : IsModularLattice α
a b : α
inst_2 : BoundedOrder α
inst_3 : ComplementedLattice α
h : a ≤ b
⊢ ∃ (b' : α), b ⊓ b' = a ∧ Codisjoint b b'
have simp_rw : ∃ (b' : α), b ⊓ b' = a ∧ b ⊔ b' = ⊤
Tactic: simp_rw [codisjoint_iff]
-- Lean 4 proof step from Mathlib.Order.ModularLattice (goal)
Goal:
α : Type u_1
inst : Lattice α
inst_1 : IsModularLattice α
a b c : α
inst_2 : BoundedOrder α
inst_3 : ComplementedLattice α
inst_4 : Fact (a ≤ b)
x_1 : (↑(Icc a b) : Type u_1)
x : α
ha : a ≤ x
hb : x ≤ b
⊢ ∃ (b_1 : (↑(Icc a b) : Type u_1)), IsCompl (Subtype.mk (p := fun (x : α) ↦ x ∈ Icc a b) x ⋯) b_1
have simp_rw : ∃ (b_1 : (↑(Icc a b) : Type u_1)), x ⊓ (↑b_1 : α) = a ∧ x ⊔ (↑b_1 : α) = b
Tactic: simp_rw [Set.Icc.isCompl_iff]
-- Lean 4 proof step from Mathlib.Order.ModularLattice (goal)
Goal:
α : Type u_1
inst : Lattice α
inst_1 : IsModularLattice α
a b c : α
inst_2 : BoundedOrder α
inst_3 : ComplementedLattice α
inst_4 : Fact (a ≤ b)
x_1 : (↑(Icc a b) : Type u_1)
x : α
ha : a ≤ x
hb : x ≤ b
⊢ ∃ (b_1 : (↑(Icc a b) : Type u_1)), x ⊓ (↑b_1 : α) = a ∧ x ⊔ (↑b_1 : α) = b
have obtain : ∀ (y : α) (ha : x ⊓ y ≤ x) (hb : x ≤ x ⊔ y) [Fact (x ⊓ y ≤ x ⊔ y)] (x_2 : (↑(Icc (x ⊓ y) (x ⊔ y)) : Type u_1)),
  ∃ (b : (↑(Icc (x ⊓ y) (x ⊔ y)) : Type u_1)), x ⊓ (↑b : α) = x ⊓ y ∧ x ⊔ (↑b : α) = x ⊔ y
Tactic: obtain ⟨y, rfl, rfl⟩ := exists_inf_eq_and_sup_eq ha hb
Cleared hypotheses: a, b, inst_4, x_1, ha, hb
-- Lean 4 proof step from Mathlib.Order.ModularLattice (goal)
Goal:
α : Type u_1
inst : Lattice α
inst_1 : IsModularLattice α
a b c : α
inst_2 : BoundedOrder α
inst_3 : ComplementedLattice α
x_1 : (↑(Iic a) : Type u_1)
x : α
hx : x ∈ Iic a
⊢ ∃ (b : (↑(Iic a) : Type u_1)), IsCompl (Subtype.mk (p := fun (x : α) ↦ x ∈ Iic a) x hx) b
have simp_rw : ∃ (b : (↑(Iic a) : Type u_1)), Disjoint x (↑b : α) ∧ x ⊔ (↑b : α) = a
Tactic: simp_rw [Set.Iic.isCompl_iff]
-- Lean 4 proof step from Mathlib.Order.ModularLattice (goal)
Goal:
α : Type u_1
inst : Lattice α
inst_1 : IsModularLattice α
a b c : α
inst_2 : BoundedOrder α
inst_3 : ComplementedLattice α
x_1 : (↑(Iic a) : Type u_1)
x : α
hx : x ∈ Iic a
⊢ ∃ (b : (↑(Iic a) : Type u_1)), Disjoint x (↑b : α) ∧ x ⊔ (↑b : α) = a
have obtain : ∀ (y : α) (hdisjoint : Disjoint x y) (x_2 : (↑(Iic (x ⊔ y)) : Type u_1)) (hx : x ∈ Iic (x ⊔ y)),
  ∃ (b : (↑(Iic (x ⊔ y)) : Type u_1)), Disjoint x (↑b : α) ∧ x ⊔ (↑b : α) = x ⊔ y
Tactic: obtain ⟨y, hdisjoint, rfl⟩ := exists_disjoint_and_sup_eq hx
Cleared hypotheses: a, x_1, hx
-- Lean 4 proof step from Mathlib.Order.ModularLattice (goal)
Goal:
α : Type u_1
inst : Lattice α
inst_1 : IsModularLattice α
a b c : α
inst_2 : BoundedOrder α
inst_3 : ComplementedLattice α
x_1 : (↑(Ici a) : Type u_1)
x : α
hx : x ∈ Ici a
⊢ ∃ (b : (↑(Ici a) : Type u_1)), IsCompl (Subtype.mk (p := fun (x : α) ↦ x ∈ Ici a) x hx) b
have simp_rw : ∃ (b : (↑(Ici a) : Type u_1)), x ⊓ (↑b : α) = a ∧ Codisjoint x (↑b : α)
Tactic: simp_rw [Set.Ici.isCompl_iff]
-- Lean 4 proof step from Mathlib.Order.ModularLattice (goal)
Goal:
α : Type u_1
inst : Lattice α
inst_1 : IsModularLattice α
a b c : α
inst_2 : BoundedOrder α
inst_3 : ComplementedLattice α
x_1 : (↑(Ici a) : Type u_1)
x : α
hx : x ∈ Ici a
⊢ ∃ (b : (↑(Ici a) : Type u_1)), x ⊓ (↑b : α) = a ∧ Codisjoint x (↑b : α)
have obtain : ∀ (y : α) (hcodisjoint : Codisjoint x y) (x_2 : (↑(Ici (x ⊓ y)) : Type u_1)) (hx : x ∈ Ici (x ⊓ y)),
  ∃ (b : (↑(Ici (x ⊓ y)) : Type u_1)), x ⊓ (↑b : α) = x ⊓ y ∧ Codisjoint x (↑b : α)
Tactic: obtain ⟨y, rfl, hcodisjoint⟩ := exists_inf_eq_and_codisjoint hx
Cleared hypotheses: a, x_1, hx
-- Lean 4 proof step from Mathlib.Order.ModularLattice (goal)
Goal:
α : Type u_1
inst : Lattice α
inst_1 : IsModularLattice α
inst_2 : BoundedOrder α
inst_3 : ComplementedLattice α
a b : α
hab : Disjoint a b
⊢ ∃ (a' : α), a ≤ a' ∧ IsCompl a' b
have obtain : ∀ (u : α) (hu : IsCompl (a ⊔ b) u), ∃ (a' : α), a ≤ a' ∧ IsCompl a' b
Tactic: obtain ⟨u, hu⟩ := ComplementedLattice.exists_isCompl (a ⊔ b)
-- Lean 4 proof step from Mathlib.Order.Monotone.Basic (goal)
Goal:
α : Type u
β : Type v
inst : Preorder α
inst_1 : Preorder β
f : α → β
⊢ Monotone (α := αᵒᵈ) (β := βᵒᵈ) ((⇑toDual : (a : β) → βᵒᵈ) ∘ f ∘ (⇑ofDual : (a : αᵒᵈ) → α)) ↔ Monotone f
have rw : Antitone (α := αᵒᵈ) (f ∘ (⇑ofDual : (a : αᵒᵈ) → α)) ↔ Monotone f
Tactic: rw [monotone_toDual_comp_iff, antitone_comp_ofDual_iff]
-- Lean 4 proof step from Mathlib.Order.Monotone.Basic (goal)
Goal:
α : Type u
β : Type v
inst : Preorder α
inst_1 : Preorder β
f : α → β
rw : Antitone (α := αᵒᵈ) (f ∘ (⇑ofDual : (a : αᵒᵈ) → α)) ↔ Monotone f
⊢ Monotone (α := αᵒᵈ) (β := βᵒᵈ) ((⇑toDual : (a : β) → βᵒᵈ) ∘ f ∘ (⇑ofDual : (a : αᵒᵈ) → α)) ↔ Monotone f
have rw₁ : Monotone f ↔ Monotone f
Tactic: rw [monotone_toDual_comp_iff, antitone_comp_ofDual_iff]
-- Lean 4 proof step from Mathlib.Order.Monotone.Basic (goal)
Goal:
α : Type u
β : Type v
inst : Preorder α
inst_1 : Preorder β
f : α → β
⊢ Antitone (α := αᵒᵈ) (β := βᵒᵈ) ((⇑toDual : (a : β) → βᵒᵈ) ∘ f ∘ (⇑ofDual : (a : αᵒᵈ) → α)) ↔ Antitone f
have rw : Monotone (α := αᵒᵈ) (f ∘ (⇑ofDual : (a : αᵒᵈ) → α)) ↔ Antitone f
Tactic: rw [antitone_toDual_comp_iff, monotone_comp_ofDual_iff]
-- Lean 4 proof step from Mathlib.Order.Monotone.Basic (goal)
Goal:
α : Type u
β : Type v
inst : Preorder α
inst_1 : Preorder β
f : α → β
rw : Monotone (α := αᵒᵈ) (f ∘ (⇑ofDual : (a : αᵒᵈ) → α)) ↔ Antitone f
⊢ Antitone (α := αᵒᵈ) (β := βᵒᵈ) ((⇑toDual : (a : β) → βᵒᵈ) ∘ f ∘ (⇑ofDual : (a : αᵒᵈ) → α)) ↔ Antitone f
have rw₁ : Antitone f ↔ Antitone f
Tactic: rw [antitone_toDual_comp_iff, monotone_comp_ofDual_iff]
-- Lean 4 proof step from Mathlib.Order.Monotone.Basic (goal)
Goal:
α : Type u
β : Type v
inst : Preorder α
inst_1 : Preorder β
f : α → β
s : Set α
⊢ MonotoneOn (β := βᵒᵈ) ((⇑toDual : (a : β) → βᵒᵈ) ∘ f ∘ (⇑ofDual : (a : αᵒᵈ) → α)) s ↔ MonotoneOn f s
have rw : AntitoneOn (f ∘ (⇑ofDual : (a : αᵒᵈ) → α)) s ↔ MonotoneOn f s
Tactic: rw [monotoneOn_toDual_comp_iff, antitoneOn_comp_ofDual_iff]
-- Lean 4 proof step from Mathlib.Order.Monotone.Basic (goal)
Goal:
α : Type u
β : Type v
inst : Preorder α
inst_1 : Preorder β
f : α → β
s : Set α
rw : AntitoneOn (f ∘ (⇑ofDual : (a : αᵒᵈ) → α)) s ↔ MonotoneOn f s
⊢ MonotoneOn (β := βᵒᵈ) ((⇑toDual : (a : β) → βᵒᵈ) ∘ f ∘ (⇑ofDual : (a : αᵒᵈ) → α)) s ↔ MonotoneOn f s
have rw₁ : MonotoneOn f s ↔ MonotoneOn f s
Tactic: rw [monotoneOn_toDual_comp_iff, antitoneOn_comp_ofDual_iff]
-- Lean 4 proof step from Mathlib.Order.Monotone.Basic (goal)
Goal:
α : Type u
β : Type v
inst : Preorder α
inst_1 : Preorder β
f : α → β
s : Set α
⊢ AntitoneOn (β := βᵒᵈ) ((⇑toDual : (a : β) → βᵒᵈ) ∘ f ∘ (⇑ofDual : (a : αᵒᵈ) → α)) s ↔ AntitoneOn f s
have rw : MonotoneOn (f ∘ (⇑ofDual : (a : αᵒᵈ) → α)) s ↔ AntitoneOn f s
Tactic: rw [antitoneOn_toDual_comp_iff, monotoneOn_comp_ofDual_iff]
-- Lean 4 proof step from Mathlib.Order.Monotone.Basic (goal)
Goal:
α : Type u
β : Type v
inst : Preorder α
inst_1 : Preorder β
f : α → β
s : Set α
rw : MonotoneOn (f ∘ (⇑ofDual : (a : αᵒᵈ) → α)) s ↔ AntitoneOn f s
⊢ AntitoneOn (β := βᵒᵈ) ((⇑toDual : (a : β) → βᵒᵈ) ∘ f ∘ (⇑ofDual : (a : αᵒᵈ) → α)) s ↔ AntitoneOn f s
have rw₁ : AntitoneOn f s ↔ AntitoneOn f s
Tactic: rw [antitoneOn_toDual_comp_iff, monotoneOn_comp_ofDual_iff]
-- Lean 4 proof step from Mathlib.Order.Monotone.Basic (goal)
Goal:
α : Type u
β : Type v
inst : Preorder α
inst_1 : Preorder β
f : α → β
⊢ StrictMono (α := αᵒᵈ) (β := βᵒᵈ) ((⇑toDual : (a : β) → βᵒᵈ) ∘ f ∘ (⇑ofDual : (a : αᵒᵈ) → α)) ↔ StrictMono f
have rw : StrictAnti (α := αᵒᵈ) (f ∘ (⇑ofDual : (a : αᵒᵈ) → α)) ↔ StrictMono f
Tactic: rw [strictMono_toDual_comp_iff, strictAnti_comp_ofDual_iff]
-- Lean 4 proof step from Mathlib.Order.Monotone.Basic (goal)
Goal:
α : Type u
β : Type v
inst : Preorder α
inst_1 : Preorder β
f : α → β
rw : StrictAnti (α := αᵒᵈ) (f ∘ (⇑ofDual : (a : αᵒᵈ) → α)) ↔ StrictMono f
⊢ StrictMono (α := αᵒᵈ) (β := βᵒᵈ) ((⇑toDual : (a : β) → βᵒᵈ) ∘ f ∘ (⇑ofDual : (a : αᵒᵈ) → α)) ↔ StrictMono f
have rw₁ : StrictMono f ↔ StrictMono f
Tactic: rw [strictMono_toDual_comp_iff, strictAnti_comp_ofDual_iff]
-- Lean 4 proof step from Mathlib.Order.Monotone.Basic (goal)
Goal:
α : Type u
β : Type v
inst : Preorder α
inst_1 : Preorder β
f : α → β
⊢ StrictAnti (α := αᵒᵈ) (β := βᵒᵈ) ((⇑toDual : (a : β) → βᵒᵈ) ∘ f ∘ (⇑ofDual : (a : αᵒᵈ) → α)) ↔ StrictAnti f
have rw : StrictMono (α := αᵒᵈ) (f ∘ (⇑ofDual : (a : αᵒᵈ) → α)) ↔ StrictAnti f
Tactic: rw [strictAnti_toDual_comp_iff, strictMono_comp_ofDual_iff]
-- Lean 4 proof step from Mathlib.Order.Monotone.Basic (goal)
Goal:
α : Type u
β : Type v
inst : Preorder α
inst_1 : Preorder β
f : α → β
rw : StrictMono (α := αᵒᵈ) (f ∘ (⇑ofDual : (a : αᵒᵈ) → α)) ↔ StrictAnti f
⊢ StrictAnti (α := αᵒᵈ) (β := βᵒᵈ) ((⇑toDual : (a : β) → βᵒᵈ) ∘ f ∘ (⇑ofDual : (a : αᵒᵈ) → α)) ↔ StrictAnti f
have rw₁ : StrictAnti f ↔ StrictAnti f
Tactic: rw [strictAnti_toDual_comp_iff, strictMono_comp_ofDual_iff]
-- Lean 4 proof step from Mathlib.Order.Monotone.Basic (goal)
Goal:
α : Type u
β : Type v
inst : Preorder α
inst_1 : Preorder β
f : α → β
s : Set α
⊢ StrictMonoOn (β := βᵒᵈ) ((⇑toDual : (a : β) → βᵒᵈ) ∘ f ∘ (⇑ofDual : (a : αᵒᵈ) → α)) s ↔ StrictMonoOn f s
have rw : StrictAntiOn (f ∘ (⇑ofDual : (a : αᵒᵈ) → α)) s ↔ StrictMonoOn f s
Tactic: rw [strictMonoOn_toDual_comp_iff, strictAntiOn_comp_ofDual_iff]
-- Lean 4 proof step from Mathlib.Order.Monotone.Basic (goal)
Goal:
α : Type u
β : Type v
inst : Preorder α
inst_1 : Preorder β
f : α → β
s : Set α
rw : StrictAntiOn (f ∘ (⇑ofDual : (a : αᵒᵈ) → α)) s ↔ StrictMonoOn f s
⊢ StrictMonoOn (β := βᵒᵈ) ((⇑toDual : (a : β) → βᵒᵈ) ∘ f ∘ (⇑ofDual : (a : αᵒᵈ) → α)) s ↔ StrictMonoOn f s
have rw₁ : StrictMonoOn f s ↔ StrictMonoOn f s
Tactic: rw [strictMonoOn_toDual_comp_iff, strictAntiOn_comp_ofDual_iff]
-- Lean 4 proof step from Mathlib.Order.Monotone.Basic (goal)
Goal:
α : Type u
β : Type v
inst : Preorder α
inst_1 : Preorder β
f : α → β
s : Set α
⊢ StrictAntiOn (β := βᵒᵈ) ((⇑toDual : (a : β) → βᵒᵈ) ∘ f ∘ (⇑ofDual : (a : αᵒᵈ) → α)) s ↔ StrictAntiOn f s
have rw : StrictMonoOn (f ∘ (⇑ofDual : (a : αᵒᵈ) → α)) s ↔ StrictAntiOn f s
Tactic: rw [strictAntiOn_toDual_comp_iff, strictMonoOn_comp_ofDual_iff]
-- Lean 4 proof step from Mathlib.Order.Monotone.Basic (goal)
Goal:
α : Type u
β : Type v
inst : Preorder α
inst_1 : Preorder β
f : α → β
s : Set α
rw : StrictMonoOn (f ∘ (⇑ofDual : (a : αᵒᵈ) → α)) s ↔ StrictAntiOn f s
⊢ StrictAntiOn (β := βᵒᵈ) ((⇑toDual : (a : β) → βᵒᵈ) ∘ f ∘ (⇑ofDual : (a : αᵒᵈ) → α)) s ↔ StrictAntiOn f s
have rw₁ : StrictAntiOn f s ↔ StrictAntiOn f s
Tactic: rw [strictAntiOn_toDual_comp_iff, strictMonoOn_comp_ofDual_iff]
-- Lean 4 proof step from Mathlib.Order.Monotone.Basic (goal)
Goal:
f : ℕ → ℕ
hf : StrictMono f
m n : ℕ
⊢ m + f n ≤ f (m + n)
have rw : f n + m ≤ f (n + m)
Tactic: rw [Nat.add_comm m, Nat.add_comm m]
-- Lean 4 proof step from Mathlib.Order.Monotone.Basic (goal)
Goal:
f : ℕ → ℕ
hf : StrictMono f
n : ℕ
⊢ f n + 0 ≤ f (n + 0)
have zero : f n ≤ f (n + 0)
Tactic: rw [Nat.add_zero, Nat.add_zero]
-- Lean 4 proof step from Mathlib.Order.Monotone.Basic (goal)
Goal:
f : ℕ → ℕ
hf : StrictMono f
n : ℕ
zero : f n ≤ f (n + 0)
⊢ f n + 0 ≤ f (n + 0)
have zero₁ : f n ≤ f n
Tactic: rw [Nat.add_zero, Nat.add_zero]
-- Lean 4 proof step from Mathlib.Order.Monotone.Basic (goal)
Goal:
f : ℕ → ℕ
hf : StrictMono f
n m : ℕ
ih : f n + m ≤ f (n + m)
⊢ f n + (m + 1) ≤ f (n + (m + 1))
have succ : f n + m < f (n + m + 1)
Tactic: rw [← Nat.add_assoc, ← Nat.add_assoc, Nat.succ_le_iff]
-- Lean 4 proof step from Mathlib.Order.Monotone.Basic (goal)
Goal:
f : ℕ → ℕ
hf : StrictMono f
m n : ℕ
⊢ f n + m ≤ f (n + m)
have zero : f n + 0 ≤ f (n + 0)
Tactic: induction m with
  | zero => rw [Nat.add_zero, Nat.add_zero]
  | succ m ih =>
    rw [← Nat.add_assoc, ← Nat.add_assoc, Nat.succ_le_iff]
    exact ih.trans_lt (hf (n + m).lt_succ_self)
Cleared hypotheses: m
-- Lean 4 proof step from Mathlib.Order.Monotone.Basic (goal)
Goal:
f : ℕ → ℕ
hf : StrictMono f
m n : ℕ
zero : f n + 0 ≤ f (n + 0)
⊢ f n + m ≤ f (n + m)
have succ : ∀ (m : ℕ) (ih : f n + m ≤ f (n + m)), f n + (m + 1) ≤ f (n + (m + 1))
Tactic: induction m with
  | zero => rw [Nat.add_zero, Nat.add_zero]
  | succ m ih =>
    rw [← Nat.add_assoc, ← Nat.add_assoc, Nat.succ_le_iff]
    exact ih.trans_lt (hf (n + m).lt_succ_self)
Cleared hypotheses: m
-- Lean 4 proof step from Mathlib.Order.Monotone.Basic (goal)
Goal:
α : Type u
β : Type v
inst : Preorder α
inst_1 : Preorder β
f g : α → β
hf : StrictMono f
hg : StrictMono g
p : α → Prop
inst_2 : DecidablePred p
hp : ∀ ⦃x y : α⦄, x < y → p y → p x
hfg : ∀ ⦃x y : α⦄, p x → ¬p y → x < y → f x < g y
x y : α
h : x < y
⊢ LT.lt.{v} (α := β) ((fun (x : α) ↦ if p x then f x else g x) x) ((fun (x : α) ↦ if p x then f x else g x) y)
have pos : ∀ (hy : p y),
  LT.lt.{v} (α := β) ((fun (x : α) ↦ if p x then f x else g x) x) ((fun (x : α) ↦ if p x then f x else g x) y)
Tactic: by_cases hy : p y
-- Lean 4 proof step from Mathlib.Order.Monotone.Basic (goal)
Goal:
α : Type u
β : Type v
inst : Preorder α
inst_1 : Preorder β
f g : α → β
hf : StrictMono f
hg : StrictMono g
p : α → Prop
inst_2 : DecidablePred p
hp : ∀ ⦃x y : α⦄, x < y → p y → p x
hfg : ∀ ⦃x y : α⦄, p x → ¬p y → x < y → f x < g y
x y : α
h : x < y
pos :
  ∀ (hy : p y),
    LT.lt.{v} (α := β) ((fun (x : α) ↦ if p x then f x else g x) x) ((fun (x : α) ↦ if p x then f x else g x) y)
⊢ LT.lt.{v} (α := β) ((fun (x : α) ↦ if p x then f x else g x) x) ((fun (x : α) ↦ if p x then f x else g x) y)
have neg : ∀ (hy : ¬p y),
  LT.lt.{v} (α := β) ((fun (x : α) ↦ if p x then f x else g x) x) ((fun (x : α) ↦ if p x then f x else g x) y)
Tactic: by_cases hy : p y
-- Lean 4 proof step from Mathlib.Order.Monotone.Basic (hypothesis)
Goal:
α : Type u
β : Type v
inst : Preorder α
inst_1 : Preorder β
f g : α → β
hf : StrictMono f
hg : StrictMono g
p : α → Prop
inst_2 : DecidablePred p
hp : ∀ ⦃x y : α⦄, x < y → p y → p x
hfg : ∀ ⦃x y : α⦄, p x → ¬p y → x < y → f x < g y
x y : α
h : x < y
hy : p y
⊢ LT.lt.{v} (α := β) ((fun (x : α) ↦ if p x then f x else g x) x) ((fun (x : α) ↦ if p x then f x else g x) y)
have hx : p x
Tactic: have hx : p x := hp h hy
-- Lean 4 proof step from Mathlib.Order.Monotone.Basic (goal)
Goal:
α : Type u
β : Type v
inst : Preorder α
inst_1 : Preorder β
f g : α → β
hf : StrictMono f
hg : StrictMono g
p : α → Prop
inst_2 : DecidablePred p
hp : ∀ ⦃x y : α⦄, x < y → p y → p x
hfg : ∀ ⦃x y : α⦄, p x → ¬p y → x < y → f x < g y
x y : α
h : x < y
hy : ¬p y
⊢ LT.lt.{v} (α := β) ((fun (x : α) ↦ if p x then f x else g x) x) ((fun (x : α) ↦ if p x then f x else g x) y)
have pos : ∀ (hx : p x),
  LT.lt.{v} (α := β) ((fun (x : α) ↦ if p x then f x else g x) x) ((fun (x : α) ↦ if p x then f x else g x) y)
Tactic: by_cases hx : p x
-- Lean 4 proof step from Mathlib.Order.Monotone.Basic (goal)
Goal:
α : Type u
β : Type v
inst : Preorder α
inst_1 : Preorder β
f g : α → β
hf : StrictMono f
hg : StrictMono g
p : α → Prop
inst_2 : DecidablePred p
hp : ∀ ⦃x y : α⦄, x < y → p y → p x
hfg : ∀ ⦃x y : α⦄, p x → ¬p y → x < y → f x < g y
x y : α
h : x < y
hy : ¬p y
pos :
  ∀ (hx : p x),
    LT.lt.{v} (α := β) ((fun (x : α) ↦ if p x then f x else g x) x) ((fun (x : α) ↦ if p x then f x else g x) y)
⊢ LT.lt.{v} (α := β) ((fun (x : α) ↦ if p x then f x else g x) x) ((fun (x : α) ↦ if p x then f x else g x) y)
have neg : ∀ (hx : ¬p x),
  LT.lt.{v} (α := β) ((fun (x : α) ↦ if p x then f x else g x) x) ((fun (x : α) ↦ if p x then f x else g x) y)
Tactic: by_cases hx : p x
-- Lean 4 proof step from Mathlib.Order.Monotone.Basic (goal)
Goal:
α : Type u
β : Type v
inst : LinearOrder α
inst_1 : Preorder β
f : α → β
s : Set α
hf : StrictMonoOn f s
a b : α
ha : a ∈ s
hb : b ∈ s
⊢ f a < f b ↔ a < b
have rw : f a ≤ f b ∧ ¬f b ≤ f a ↔ a < b
Tactic: rw [lt_iff_le_not_ge, lt_iff_le_not_ge, hf.le_iff_le ha hb, hf.le_iff_le hb ha]
-- Lean 4 proof step from Mathlib.Order.Monotone.Basic (goal)
Goal:
α : Type u
β : Type v
inst : LinearOrder α
inst_1 : Preorder β
f : α → β
s : Set α
hf : StrictMonoOn f s
a b : α
ha : a ∈ s
hb : b ∈ s
rw : f a ≤ f b ∧ ¬f b ≤ f a ↔ a < b
⊢ f a < f b ↔ a < b
have rw₁ : f a ≤ f b ∧ ¬f b ≤ f a ↔ a ≤ b ∧ ¬b ≤ a
Tactic: rw [lt_iff_le_not_ge, lt_iff_le_not_ge, hf.le_iff_le ha hb, hf.le_iff_le hb ha]
-- Lean 4 proof step from Mathlib.Order.Monotone.Basic (goal)
Goal:
α : Type u
β : Type v
inst : LinearOrder α
inst_1 : Preorder β
f : α → β
s : Set α
hf : StrictMonoOn f s
a b : α
ha : a ∈ s
hb : b ∈ s
rw : f a ≤ f b ∧ ¬f b ≤ f a ↔ a < b
rw₁ : f a ≤ f b ∧ ¬f b ≤ f a ↔ a ≤ b ∧ ¬b ≤ a
⊢ f a < f b ↔ a < b
have rw₂ : a ≤ b ∧ ¬f b ≤ f a ↔ a ≤ b ∧ ¬b ≤ a
Tactic: rw [lt_iff_le_not_ge, lt_iff_le_not_ge, hf.le_iff_le ha hb, hf.le_iff_le hb ha]
-- Lean 4 proof step from Mathlib.Order.Monotone.Basic (goal)
Goal:
α : Type u
β : Type v
inst : LinearOrder α
inst_1 : Preorder β
f : α → β
s : Set α
hf : StrictMonoOn f s
a b : α
ha : a ∈ s
hb : b ∈ s
rw : f a ≤ f b ∧ ¬f b ≤ f a ↔ a < b
rw₁ : f a ≤ f b ∧ ¬f b ≤ f a ↔ a ≤ b ∧ ¬b ≤ a
rw₂ : a ≤ b ∧ ¬f b ≤ f a ↔ a ≤ b ∧ ¬b ≤ a
⊢ f a < f b ↔ a < b
have rw₃ : a ≤ b ∧ ¬b ≤ a ↔ a ≤ b ∧ ¬b ≤ a
Tactic: rw [lt_iff_le_not_ge, lt_iff_le_not_ge, hf.le_iff_le ha hb, hf.le_iff_le hb ha]
-- Lean 4 proof step from Mathlib.Order.Monotone.Basic (goal)
Goal:
α : Type u
β : Type v
inst : LinearOrder α
inst_1 : PartialOrder β
f : α → β
a₁ a₂ : α
h_mon : Monotone f
h_fa : f a₁ = f a₂
i : α
h₁ : a₁ ≤ i
h₂ : i ≤ a₂
⊢ f i = f a₁
have a : f i ≤ f a₁
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Order.Monotone.Basic (goal)
Goal:
α : Type u
β : Type v
inst : LinearOrder α
inst_1 : PartialOrder β
f : α → β
a₁ a₂ : α
h_mon : Monotone f
h_fa : f a₁ = f a₂
i : α
h₁ : a₁ ≤ i
h₂ : i ≤ a₂
a : f i ≤ f a₁
⊢ f i = f a₁
have a₃ : f a₁ ≤ f i
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Order.Monotone.Basic (goal)
Goal:
α : Type u
β : Type v
inst : LinearOrder α
inst_1 : PartialOrder β
f : α → β
a₁ a₂ : α
h_mon : Monotone f
h_fa : f a₁ = f a₂
i : α
h₁ : a₁ ≤ i
h₂ : i ≤ a₂
⊢ f i ≤ f a₁
have a : f i ≤ f a₂
Tactic: rw [h_fa]
-- Lean 4 proof step from Mathlib.Order.Monotone.Basic (goal)
Goal:
α : Type u
β : Type v
inst : LinearOrder α
inst_1 : PartialOrder β
f : α → β
a₁ a₂ : α
h_anti : Antitone f
h_fa : f a₁ = f a₂
i : α
h₁ : a₁ ≤ i
h₂ : i ≤ a₂
⊢ f i = f a₁
have a : f i ≤ f a₁
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Order.Monotone.Basic (goal)
Goal:
α : Type u
β : Type v
inst : LinearOrder α
inst_1 : PartialOrder β
f : α → β
a₁ a₂ : α
h_anti : Antitone f
h_fa : f a₁ = f a₂
i : α
h₁ : a₁ ≤ i
h₂ : i ≤ a₂
a : f i ≤ f a₁
⊢ f i = f a₁
have a₃ : f a₁ ≤ f i
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Order.Monotone.Basic (goal)
Goal:
α : Type u
β : Type v
inst : LinearOrder α
inst_1 : PartialOrder β
f : α → β
a₁ a₂ : α
h_anti : Antitone f
h_fa : f a₁ = f a₂
i : α
h₁ : a₁ ≤ i
h₂ : i ≤ a₂
⊢ f a₁ ≤ f i
have a : f a₂ ≤ f i
Tactic: rw [h_fa]
-- Lean 4 proof step from Mathlib.Order.Monotone.Basic (goal)
Goal:
α : Type u
β : Type v
inst : LinearOrder α
inst_1 : LinearOrder β
f : α → β
⊢ ¬Monotone f ∧ ¬Antitone f ↔
    ∃ (a : α), ∃ (b : α), ∃ (c : α), a < b ∧ b < c ∧ (f a < f b ∧ f c < f b ∨ f b < f a ∧ f b < f c)
have simp_rw : (∃ (a : α), ∃ (b : α), ∃ (c : α), (a ≤ b ∧ b ≤ c) ∧ (f a < f b ∧ f c < f b ∨ f b < f a ∧ f b < f c)) ↔
  ∃ (a : α), ∃ (b : α), ∃ (c : α), (a < b ∧ b < c) ∧ (f a < f b ∧ f c < f b ∨ f b < f a ∧ f b < f c)
Tactic: simp_rw [not_monotone_not_antitone_iff_exists_le_le, ← and_assoc]
-- Lean 4 proof step from Mathlib.Order.Monotone.Basic (goal)
Goal:
α : Type u
β : Type v
inst : LinearOrder α
inst_1 : LinearOrder β
f : α → β
⊢ (∃ (a : α), ∃ (b : α), ∃ (c : α), (a ≤ b ∧ b ≤ c) ∧ (f a < f b ∧ f c < f b ∨ f b < f a ∧ f b < f c)) ↔
    ∃ (a : α), ∃ (b : α), ∃ (c : α), (a < b ∧ b < c) ∧ (f a < f b ∧ f c < f b ∨ f b < f a ∧ f b < f c)
have refine_1 : ∀ (a b c : α) (h : f a < f b ∧ f c < f b ∨ f b < f a ∧ f b < f c), a ≠ b
Tactic: refine exists₃_congr (fun a b c ↦ and_congr_left <|
    fun h ↦ (Ne.le_iff_lt ?_).and <| Ne.le_iff_lt ?_)