awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.ModularLattice
Goal:
α : Type u_1
inst : Lattice α
inst_1 : BoundedOrder α
inst_2 : IsModularLattice α
a b c : α
h₁ : IsCompl b c
h₂ : b ≤ a
codisjoint : (b ⊓ a ⊔ c) ⊓ a = 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 })

Tactic:
simp only [Iic.codisjoint_iff, inf_comm a, IsModularLattice.inf_sup_inf_assoc]

Premises used: IsModularLattice.inf_sup_inf_assoc, inf_comm, Set.Iic.codisjoint_iff
-- Module: Mathlib.Order.ModularLattice
Goal:
α : Type u_1
inst : Lattice α
inst_1 : BoundedOrder α
inst_2 : IsModularLattice α
a b c : α
h₁ : IsCompl b c
h₂ : b ≤ a
⊢ (b ⊓ a ⊔ c) ⊓ a = a

Tactic:
simp [inf_of_le_left h₂, h₁.sup_eq_top]

Premises used: IsCompl.sup_eq_top, inf_of_le_left
-- Module: Mathlib.Order.ModularLattice
Goal:
α : Type u_1
inst : Lattice α
inst_1 : IsModularLattice α
a b c : α
⊢ IsModularLattice.{u_1} (↑(Iic a) : Type u_1)

Tactic:
⟨@fun x y z xz => (sup_inf_le_assoc_of_le (y : α) xz : (↑x ⊔ ↑y) ⊓ ↑z ≤ ↑x ⊔ ↑y ⊓ ↑z)⟩

Premises used: IsModularLattice.mk
-- Module: Mathlib.Order.ModularLattice
Goal:
α : Type u_1
inst : Lattice α
inst_1 : IsModularLattice α
a b c : α
⊢ IsModularLattice.{u_1} (↑(Ici a) : Type u_1)

Tactic:
⟨@fun x y z xz => (sup_inf_le_assoc_of_le (y : α) xz : (↑x ⊔ ↑y) ⊓ ↑z ≤ ↑x ⊔ ↑y ⊓ ↑z)⟩

Premises used: IsModularLattice.mk
-- Module: Mathlib.Order.ModularLattice
Goal:
α : Type u_1
inst : Lattice α
inst_1 : IsModularLattice α
a b c : α
inst_2 : BoundedOrder α
inst_3 : ComplementedLattice α
hb : a ≤ b
hc : b ≤ c
obtain : ∀ (d : α) (hdisjoint : Disjoint b d) (hcodisjoint : Codisjoint b d), ∃ (b' : α), b ⊓ b' = a ∧ b ⊔ b' = c
⊢ ∃ (b' : α), b ⊓ b' = a ∧ b ⊔ b' = c

Tactic:
obtain ⟨d, hdisjoint, hcodisjoint⟩ := exists_isCompl b

Premises used: ComplementedLattice.exists_isCompl
-- Module: Mathlib.Order.ModularLattice
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

Tactic:
⟨(d ⊔ a) ⊓ c, ?_, ?_⟩

Premises used: Max.max, And.intro, Exists.intro, Min.min
-- Module: Mathlib.Order.ModularLattice
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
refine_2 : b ⊔ (d ⊔ a) ⊓ c = c
⊢ ∃ (b' : α), b ⊓ b' = a ∧ b ⊔ b' = c

Tactic:
refine ⟨(d ⊔ a) ⊓ c, ?_, ?_⟩
-- Module: Mathlib.Order.ModularLattice
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 ⊓ ((d ⊔ a) ⊓ c) = a

Tactic:
simpa [← inf_assoc, ← inf_sup_assoc_of_le _ hb, hdisjoint.eq_bot] using hb.trans hc

Premises used: inf_sup_assoc_of_le, LE.le.trans, inf_assoc, Disjoint.eq_bot
-- Module: Mathlib.Order.ModularLattice
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 ⊔ (d ⊔ a) ⊓ c = c

Tactic:
simp [← sup_inf_assoc_of_le _ hc, ← sup_assoc, hcodisjoint.eq_top]

Premises used: sup_assoc, sup_inf_assoc_of_le, Codisjoint.eq_top
-- Module: Mathlib.Order.ModularLattice
Goal:
α : Type u_1
inst : Lattice α
inst_1 : IsModularLattice α
a b : α
inst_2 : BoundedOrder α
inst_3 : ComplementedLattice α
h : a ≤ b
simp_rw : ∃ (a' : α), a ⊓ a' = ⊥ ∧ a ⊔ a' = b
⊢ ∃ (a' : α), Disjoint a a' ∧ a ⊔ a' = b

Tactic:
simp_rw [disjoint_iff]

Premises used: disjoint_iff
-- Module: Mathlib.Order.ModularLattice
Goal:
α : Type u_1
inst : Lattice α
inst_1 : IsModularLattice α
a b : α
inst_2 : BoundedOrder α
inst_3 : ComplementedLattice α
h : a ≤ b
⊢ ⊥ ≤ a

Tactic:
simp
-- Module: Mathlib.Order.ModularLattice
Goal:
α : Type u_1
inst : Lattice α
inst_1 : IsModularLattice α
a b : α
inst_2 : BoundedOrder α
inst_3 : ComplementedLattice α
h : a ≤ b
⊢ ∃ (a' : α), a ⊓ a' = ⊥ ∧ a ⊔ a' = b

Tactic:
apply exists_inf_eq_and_sup_eq (by simp) h

Premises used: IsModularLattice.exists_inf_eq_and_sup_eq
-- Module: Mathlib.Order.ModularLattice
Goal:
α : Type u_1
inst : Lattice α
inst_1 : IsModularLattice α
a b : α
inst_2 : BoundedOrder α
inst_3 : ComplementedLattice α
h : a ≤ b
simp_rw : ∃ (b' : α), b ⊓ b' = a ∧ b ⊔ b' = ⊤
⊢ ∃ (b' : α), b ⊓ b' = a ∧ Codisjoint b b'

Tactic:
simp_rw [codisjoint_iff]

Premises used: codisjoint_iff
-- Module: Mathlib.Order.ModularLattice
Goal:
α : Type u_1
inst : Lattice α
inst_1 : IsModularLattice α
a b : α
inst_2 : BoundedOrder α
inst_3 : ComplementedLattice α
h : a ≤ b
⊢ b ≤ ⊤

Tactic:
simp
-- Module: Mathlib.Order.ModularLattice
Goal:
α : Type u_1
inst : Lattice α
inst_1 : IsModularLattice α
a b : α
inst_2 : BoundedOrder α
inst_3 : ComplementedLattice α
h : a ≤ b
⊢ ∃ (b' : α), b ⊓ b' = a ∧ b ⊔ b' = ⊤

Tactic:
apply exists_inf_eq_and_sup_eq h (by simp)

Premises used: IsModularLattice.exists_inf_eq_and_sup_eq
-- Module: Mathlib.Order.ModularLattice
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
simp_rw : ∃ (b_1 : (↑(Icc a b) : Type u_1)), x ⊓ (↑b_1 : α) = a ∧ x ⊔ (↑b_1 : α) = b
⊢ ∃ (b_1 : (↑(Icc a b) : Type u_1)), IsCompl (Subtype.mk (p := fun (x : α) ↦ x ∈ Icc a b) x ⋯) b_1

Tactic:
simp_rw [Set.Icc.isCompl_iff]

Premises used: Set.Icc.isCompl_iff
-- Module: Mathlib.Order.ModularLattice
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
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
⊢ ∃ (b_1 : (↑(Icc a b) : Type u_1)), x ⊓ (↑b_1 : α) = a ∧ x ⊔ (↑b_1 : α) = b

Tactic:
obtain ⟨y, rfl, rfl⟩ := exists_inf_eq_and_sup_eq ha hb

Premises used: IsModularLattice.exists_inf_eq_and_sup_eq, rfl
-- Module: Mathlib.Order.ModularLattice
Goal:
α : Type u_1
inst : Lattice α
inst_1 : IsModularLattice α
c : α
inst_2 : BoundedOrder α
inst_3 : ComplementedLattice α
x y : α
ha : x ⊓ y ≤ x
hb : x ≤ x ⊔ y
inst_4 : Fact (x ⊓ y ≤ x ⊔ y)
x_1 : (↑(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:
⟨⟨y, inf_le_right, le_sup_right⟩, rfl, rfl⟩

Premises used: inf_le_right, le_sup_right, Subtype.mk, And.intro, Exists.intro, rfl
-- Module: Mathlib.Order.ModularLattice
Goal:
α : Type u_1
inst : Lattice α
inst_1 : IsModularLattice α
c : α
inst_2 : BoundedOrder α
inst_3 : ComplementedLattice α
x y : α
ha : x ⊓ y ≤ x
hb : x ≤ x ⊔ y
inst_4 : Fact (x ⊓ y ≤ x ⊔ y)
x_1 : (↑(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:
exact ⟨⟨y, inf_le_right, le_sup_right⟩, rfl, rfl⟩
-- Module: Mathlib.Order.ModularLattice
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
simp_rw : ∃ (b : (↑(Iic a) : Type u_1)), Disjoint x (↑b : α) ∧ x ⊔ (↑b : α) = a
⊢ ∃ (b : (↑(Iic a) : Type u_1)), IsCompl (Subtype.mk (p := fun (x : α) ↦ x ∈ Iic a) x hx) b

Tactic:
simp_rw [Set.Iic.isCompl_iff]

Premises used: Set.Iic.isCompl_iff
-- Module: Mathlib.Order.ModularLattice
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
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
⊢ ∃ (b : (↑(Iic a) : Type u_1)), Disjoint x (↑b : α) ∧ x ⊔ (↑b : α) = a

Tactic:
obtain ⟨y, hdisjoint, rfl⟩ := exists_disjoint_and_sup_eq hx

Premises used: IsModularLattice.exists_disjoint_and_sup_eq, rfl
-- Module: Mathlib.Order.ModularLattice
Goal:
α : Type u_1
inst : Lattice α
inst_1 : IsModularLattice α
b c : α
inst_2 : BoundedOrder α
inst_3 : ComplementedLattice α
x y : α
hdisjoint : Disjoint x y
x_1 : (↑(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:
⟨⟨y, le_sup_right⟩, hdisjoint, rfl⟩

Premises used: le_sup_right, Subtype.mk, And.intro, Exists.intro, rfl
-- Module: Mathlib.Order.ModularLattice
Goal:
α : Type u_1
inst : Lattice α
inst_1 : IsModularLattice α
b c : α
inst_2 : BoundedOrder α
inst_3 : ComplementedLattice α
x y : α
hdisjoint : Disjoint x y
x_1 : (↑(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:
exact ⟨⟨y, le_sup_right⟩, hdisjoint, rfl⟩
-- Module: Mathlib.Order.ModularLattice
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
simp_rw : ∃ (b : (↑(Ici a) : Type u_1)), x ⊓ (↑b : α) = a ∧ Codisjoint x (↑b : α)
⊢ ∃ (b : (↑(Ici a) : Type u_1)), IsCompl (Subtype.mk (p := fun (x : α) ↦ x ∈ Ici a) x hx) b

Tactic:
simp_rw [Set.Ici.isCompl_iff]

Premises used: Set.Ici.isCompl_iff
-- Module: Mathlib.Order.ModularLattice
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
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 : α)
⊢ ∃ (b : (↑(Ici a) : Type u_1)), x ⊓ (↑b : α) = a ∧ Codisjoint x (↑b : α)

Tactic:
obtain ⟨y, rfl, hcodisjoint⟩ := exists_inf_eq_and_codisjoint hx

Premises used: IsModularLattice.exists_inf_eq_and_codisjoint, rfl
-- Module: Mathlib.Order.ModularLattice
Goal:
α : Type u_1
inst : Lattice α
inst_1 : IsModularLattice α
b c : α
inst_2 : BoundedOrder α
inst_3 : ComplementedLattice α
x y : α
hcodisjoint : Codisjoint x y
x_1 : (↑(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:
⟨⟨y, inf_le_right⟩, rfl, hcodisjoint⟩

Premises used: inf_le_right, Subtype.mk, And.intro, Exists.intro, rfl
-- Module: Mathlib.Order.ModularLattice
Goal:
α : Type u_1
inst : Lattice α
inst_1 : IsModularLattice α
b c : α
inst_2 : BoundedOrder α
inst_3 : ComplementedLattice α
x y : α
hcodisjoint : Codisjoint x y
x_1 : (↑(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:
exact ⟨⟨y, inf_le_right⟩, rfl, hcodisjoint⟩
-- Module: Mathlib.Order.ModularLattice
Goal:
α : Type u_1
inst : Lattice α
inst_1 : IsModularLattice α
inst_2 : BoundedOrder α
inst_3 : ComplementedLattice α
a b : α
hab : Disjoint a b
obtain : ∀ (u : α) (hu : IsCompl (a ⊔ b) u), ∃ (a' : α), a ≤ a' ∧ IsCompl a' b
⊢ ∃ (a' : α), a ≤ a' ∧ IsCompl a' b

Tactic:
obtain ⟨u, hu⟩ := ComplementedLattice.exists_isCompl (a ⊔ b)

Premises used: ComplementedLattice.exists_isCompl, Max.max
-- Module: Mathlib.Order.ModularLattice
Goal:
α : Type u_1
inst : Lattice α
inst_1 : IsModularLattice α
inst_2 : BoundedOrder α
inst_3 : ComplementedLattice α
a b : α
hab : Disjoint a b
u : α
hu : IsCompl (a ⊔ b) u
⊢ ∃ (a' : α), a ≤ a' ∧ IsCompl a' b

Tactic:
⟨u ⊔ a, le_sup_right, hab.isCompl_sup_left_of_isCompl_sup_right hu.symm⟩

Premises used: le_sup_right, Max.max, And.intro, Exists.intro, Disjoint.isCompl_sup_left_of_isCompl_sup_right, IsCompl.symm
-- Module: Mathlib.Order.ModularLattice
Goal:
α : Type u_1
inst : Lattice α
inst_1 : IsModularLattice α
inst_2 : BoundedOrder α
inst_3 : ComplementedLattice α
a b : α
hab : Disjoint a b
u : α
hu : IsCompl (a ⊔ b) u
⊢ ∃ (a' : α), a ≤ a' ∧ IsCompl a' b

Tactic:
exact ⟨u ⊔ a, le_sup_right, hab.isCompl_sup_left_of_isCompl_sup_right hu.symm⟩
-- Module: Mathlib.Order.Monotone.Basic
Goal:
α : Type u
β : Type v
inst : Preorder α
inst_1 : Preorder β
f : α → β
⊢ Monotone (α := αᵒᵈ) (f ∘ (⇑ofDual : (a : αᵒᵈ) → α)) ↔ Antitone f

Tactic:
forall_comm

Premises used: Monotone, forall_comm, Antitone, OrderDual
-- Module: Mathlib.Order.Monotone.Basic
Goal:
α : Type u
β : Type v
inst : Preorder α
inst_1 : Preorder β
f : α → β
⊢ Antitone (α := αᵒᵈ) (f ∘ (⇑ofDual : (a : αᵒᵈ) → α)) ↔ Monotone f

Tactic:
forall_comm

Premises used: Monotone, forall_comm, Antitone, OrderDual
-- Module: Mathlib.Order.Monotone.Basic
Goal:
α : Type u
β : Type v
inst : Preorder α
inst_1 : Preorder β
f : α → β
⊢ Monotone (β := βᵒᵈ) ((⇑toDual : (a : β) → βᵒᵈ) ∘ f) ↔ Antitone f

Tactic:
Iff.rfl

Premises used: Iff.rfl, Antitone
-- Module: Mathlib.Order.Monotone.Basic
Goal:
α : Type u
β : Type v
inst : Preorder α
inst_1 : Preorder β
f : α → β
⊢ Antitone (β := βᵒᵈ) ((⇑toDual : (a : β) → βᵒᵈ) ∘ f) ↔ Monotone f

Tactic:
Iff.rfl

Premises used: Iff.rfl, Monotone
-- Module: Mathlib.Order.Monotone.Basic
Goal:
α : Type u
β : Type v
inst : Preorder α
inst_1 : Preorder β
f : α → β
s : Set α
⊢ MonotoneOn (f ∘ (⇑ofDual : (a : αᵒᵈ) → α)) s ↔ AntitoneOn f s

Tactic:
forall₂_comm

Premises used: Set.Mem, MonotoneOn, AntitoneOn, OrderDual, forall₂_comm
-- Module: Mathlib.Order.Monotone.Basic
Goal:
α : Type u
β : Type v
inst : Preorder α
inst_1 : Preorder β
f : α → β
s : Set α
⊢ AntitoneOn (f ∘ (⇑ofDual : (a : αᵒᵈ) → α)) s ↔ MonotoneOn f s

Tactic:
forall₂_comm

Premises used: Set.Mem, MonotoneOn, AntitoneOn, OrderDual, forall₂_comm
-- Module: Mathlib.Order.Monotone.Basic
Goal:
α : Type u
β : Type v
inst : Preorder α
inst_1 : Preorder β
f : α → β
s : Set α
⊢ MonotoneOn (β := βᵒᵈ) ((⇑toDual : (a : β) → βᵒᵈ) ∘ f) s ↔ AntitoneOn f s

Tactic:
Iff.rfl

Premises used: Iff.rfl, AntitoneOn
-- Module: Mathlib.Order.Monotone.Basic
Goal:
α : Type u
β : Type v
inst : Preorder α
inst_1 : Preorder β
f : α → β
s : Set α
⊢ AntitoneOn (β := βᵒᵈ) ((⇑toDual : (a : β) → βᵒᵈ) ∘ f) s ↔ MonotoneOn f s

Tactic:
Iff.rfl

Premises used: Iff.rfl, MonotoneOn
-- Module: Mathlib.Order.Monotone.Basic
Goal:
α : Type u
β : Type v
inst : Preorder α
inst_1 : Preorder β
f : α → β
⊢ StrictMono (α := αᵒᵈ) (f ∘ (⇑ofDual : (a : αᵒᵈ) → α)) ↔ StrictAnti f

Tactic:
forall_comm

Premises used: StrictMono, forall_comm, StrictAnti, OrderDual
-- Module: Mathlib.Order.Monotone.Basic
Goal:
α : Type u
β : Type v
inst : Preorder α
inst_1 : Preorder β
f : α → β
⊢ StrictAnti (α := αᵒᵈ) (f ∘ (⇑ofDual : (a : αᵒᵈ) → α)) ↔ StrictMono f

Tactic:
forall_comm

Premises used: StrictMono, forall_comm, StrictAnti, OrderDual
-- Module: Mathlib.Order.Monotone.Basic
Goal:
α : Type u
β : Type v
inst : Preorder α
inst_1 : Preorder β
f : α → β
⊢ StrictMono (β := βᵒᵈ) ((⇑toDual : (a : β) → βᵒᵈ) ∘ f) ↔ StrictAnti f

Tactic:
Iff.rfl

Premises used: Iff.rfl, StrictAnti
-- Module: Mathlib.Order.Monotone.Basic
Goal:
α : Type u
β : Type v
inst : Preorder α
inst_1 : Preorder β
f : α → β
⊢ StrictAnti (β := βᵒᵈ) ((⇑toDual : (a : β) → βᵒᵈ) ∘ f) ↔ StrictMono f

Tactic:
Iff.rfl

Premises used: StrictMono, Iff.rfl
-- Module: Mathlib.Order.Monotone.Basic
Goal:
α : Type u
β : Type v
inst : Preorder α
inst_1 : Preorder β
f : α → β
s : Set α
⊢ StrictMonoOn (f ∘ (⇑ofDual : (a : αᵒᵈ) → α)) s ↔ StrictAntiOn f s

Tactic:
forall₂_comm

Premises used: Set.Mem, StrictAntiOn, StrictMonoOn, OrderDual, forall₂_comm
-- Module: Mathlib.Order.Monotone.Basic
Goal:
α : Type u
β : Type v
inst : Preorder α
inst_1 : Preorder β
f : α → β
s : Set α
⊢ StrictAntiOn (f ∘ (⇑ofDual : (a : αᵒᵈ) → α)) s ↔ StrictMonoOn f s

Tactic:
forall₂_comm

Premises used: Set.Mem, StrictAntiOn, StrictMonoOn, OrderDual, forall₂_comm
-- Module: Mathlib.Order.Monotone.Basic
Goal:
α : Type u
β : Type v
inst : Preorder α
inst_1 : Preorder β
f : α → β
s : Set α
⊢ StrictMonoOn (β := βᵒᵈ) ((⇑toDual : (a : β) → βᵒᵈ) ∘ f) s ↔ StrictAntiOn f s

Tactic:
Iff.rfl

Premises used: Iff.rfl, StrictAntiOn
-- Module: Mathlib.Order.Monotone.Basic
Goal:
α : Type u
β : Type v
inst : Preorder α
inst_1 : Preorder β
f : α → β
s : Set α
⊢ StrictAntiOn (β := βᵒᵈ) ((⇑toDual : (a : β) → βᵒᵈ) ∘ f) s ↔ StrictMonoOn f s

Tactic:
Iff.rfl

Premises used: Iff.rfl, StrictMonoOn
-- Module: Mathlib.Order.Monotone.Basic
Goal:
α : Type u
β : Type v
inst : Preorder α
inst_1 : Preorder β
f : α → β
rw : Antitone (α := αᵒᵈ) (f ∘ (⇑ofDual : (a : αᵒᵈ) → α)) ↔ Monotone f
rw₁ rw₂ : Monotone f ↔ Monotone f
⊢ Monotone (α := αᵒᵈ) (β := βᵒᵈ) ((⇑toDual : (a : β) → βᵒᵈ) ∘ f ∘ (⇑ofDual : (a : αᵒᵈ) → α)) ↔ Monotone f

Tactic:
rw [monotone_toDual_comp_iff, antitone_comp_ofDual_iff]

Premises used: monotone_toDual_comp_iff, antitone_comp_ofDual_iff
-- Module: Mathlib.Order.Monotone.Basic
Goal:
α : Type u
β : Type v
inst : Preorder α
inst_1 : Preorder β
f : α → β
rw : Monotone (α := αᵒᵈ) (f ∘ (⇑ofDual : (a : αᵒᵈ) → α)) ↔ Antitone f
rw₁ rw₂ : Antitone f ↔ Antitone f
⊢ Antitone (α := αᵒᵈ) (β := βᵒᵈ) ((⇑toDual : (a : β) → βᵒᵈ) ∘ f ∘ (⇑ofDual : (a : αᵒᵈ) → α)) ↔ Antitone f

Tactic:
rw [antitone_toDual_comp_iff, monotone_comp_ofDual_iff]

Premises used: antitone_toDual_comp_iff, monotone_comp_ofDual_iff
-- Module: Mathlib.Order.Monotone.Basic
Goal:
α : Type u
β : Type v
inst : Preorder α
inst_1 : Preorder β
f : α → β
s : Set α
rw : AntitoneOn (f ∘ (⇑ofDual : (a : αᵒᵈ) → α)) s ↔ MonotoneOn f s
rw₁ rw₂ : MonotoneOn f s ↔ MonotoneOn f s
⊢ MonotoneOn (β := βᵒᵈ) ((⇑toDual : (a : β) → βᵒᵈ) ∘ f ∘ (⇑ofDual : (a : αᵒᵈ) → α)) s ↔ MonotoneOn f s

Tactic:
rw [monotoneOn_toDual_comp_iff, antitoneOn_comp_ofDual_iff]

Premises used: antitoneOn_comp_ofDual_iff, monotoneOn_toDual_comp_iff
-- Module: Mathlib.Order.Monotone.Basic
Goal:
α : Type u
β : Type v
inst : Preorder α
inst_1 : Preorder β
f : α → β
s : Set α
rw : MonotoneOn (f ∘ (⇑ofDual : (a : αᵒᵈ) → α)) s ↔ AntitoneOn f s
rw₁ rw₂ : AntitoneOn f s ↔ AntitoneOn f s
⊢ AntitoneOn (β := βᵒᵈ) ((⇑toDual : (a : β) → βᵒᵈ) ∘ f ∘ (⇑ofDual : (a : αᵒᵈ) → α)) s ↔ AntitoneOn f s

Tactic:
rw [antitoneOn_toDual_comp_iff, monotoneOn_comp_ofDual_iff]

Premises used: monotoneOn_comp_ofDual_iff, antitoneOn_toDual_comp_iff
-- Module: Mathlib.Order.Monotone.Basic
Goal:
α : Type u
β : Type v
inst : Preorder α
inst_1 : Preorder β
f : α → β
rw : StrictAnti (α := αᵒᵈ) (f ∘ (⇑ofDual : (a : αᵒᵈ) → α)) ↔ StrictMono f
rw₁ rw₂ : StrictMono f ↔ StrictMono f
⊢ StrictMono (α := αᵒᵈ) (β := βᵒᵈ) ((⇑toDual : (a : β) → βᵒᵈ) ∘ f ∘ (⇑ofDual : (a : αᵒᵈ) → α)) ↔ StrictMono f

Tactic:
rw [strictMono_toDual_comp_iff, strictAnti_comp_ofDual_iff]

Premises used: strictMono_toDual_comp_iff, strictAnti_comp_ofDual_iff
-- Module: Mathlib.Order.Monotone.Basic
Goal:
α : Type u
β : Type v
inst : Preorder α
inst_1 : Preorder β
f : α → β
rw : StrictMono (α := αᵒᵈ) (f ∘ (⇑ofDual : (a : αᵒᵈ) → α)) ↔ StrictAnti f
rw₁ rw₂ : StrictAnti f ↔ StrictAnti f
⊢ StrictAnti (α := αᵒᵈ) (β := βᵒᵈ) ((⇑toDual : (a : β) → βᵒᵈ) ∘ f ∘ (⇑ofDual : (a : αᵒᵈ) → α)) ↔ StrictAnti f

Tactic:
rw [strictAnti_toDual_comp_iff, strictMono_comp_ofDual_iff]

Premises used: strictMono_comp_ofDual_iff, strictAnti_toDual_comp_iff
-- Module: Mathlib.Order.Monotone.Basic
Goal:
α : Type u
β : Type v
inst : Preorder α
inst_1 : Preorder β
f : α → β
s : Set α
rw : StrictAntiOn (f ∘ (⇑ofDual : (a : αᵒᵈ) → α)) s ↔ StrictMonoOn f s
rw₁ rw₂ : StrictMonoOn f s ↔ StrictMonoOn f s
⊢ StrictMonoOn (β := βᵒᵈ) ((⇑toDual : (a : β) → βᵒᵈ) ∘ f ∘ (⇑ofDual : (a : αᵒᵈ) → α)) s ↔ StrictMonoOn f s

Tactic:
rw [strictMonoOn_toDual_comp_iff, strictAntiOn_comp_ofDual_iff]

Premises used: strictAntiOn_comp_ofDual_iff, strictMonoOn_toDual_comp_iff
-- Module: Mathlib.Order.Monotone.Basic
Goal:
α : Type u
β : Type v
inst : Preorder α
inst_1 : Preorder β
f : α → β
s : Set α
rw : StrictMonoOn (f ∘ (⇑ofDual : (a : αᵒᵈ) → α)) s ↔ StrictAntiOn f s
rw₁ rw₂ : StrictAntiOn f s ↔ StrictAntiOn f s
⊢ StrictAntiOn (β := βᵒᵈ) ((⇑toDual : (a : β) → βᵒᵈ) ∘ f ∘ (⇑ofDual : (a : αᵒᵈ) → α)) s ↔ StrictAntiOn f s

Tactic:
rw [strictAntiOn_toDual_comp_iff, strictMonoOn_comp_ofDual_iff]

Premises used: strictAntiOn_toDual_comp_iff, strictMonoOn_comp_ofDual_iff
-- Module: Mathlib.Order.Monotone.Basic
Goal:
α : Type u
β : Type v
inst : Preorder α
inst_1 : Preorder β
f : α → β
inst_2 : WellFoundedLT β
hf : StrictMono f
⊢ WellFoundedLT α

Tactic:
Subrelation.isWellFounded (InvImage (· < ·) f) hf.imp

Premises used: InvImage, StrictMono.imp, LT.lt, Subrelation.isWellFounded
-- Module: Mathlib.Order.Monotone.Basic
Goal:
α : Type u
β : Type v
inst : Preorder α
inst_1 : Preorder β
f : α → β
inst_2 : WellFoundedGT β
hf : StrictAnti f
⊢ WellFoundedLT α

Tactic:
Subrelation.isWellFounded (InvImage (· > ·) f) hf.imp

Premises used: InvImage, GT.gt, Subrelation.isWellFounded, StrictAnti.imp
-- Module: Mathlib.Order.Monotone.Basic
Goal:
α : Type u
β : Type v
inst : Preorder α
inst_1 : PartialOrder β
f : α → β
s : Set α
hmono : MonotoneOn f s
hinj : Set.InjOn f s
⊢ StrictMonoOn f s

Tactic:
fun _ hx _ hy h ↦ hmono hx hy h.le |>.lt_of_ne <| mt (hinj hx hy) h.ne

Premises used: mt, LT.lt.le, LE.le.lt_of_ne, StrictMonoOn, LT.lt.ne
-- Module: Mathlib.Order.Monotone.Basic
Goal:
α : Type u
β : Type v
inst : Preorder α
inst_1 : PartialOrder β
f : α → β
s : Set α
hanti : AntitoneOn f s
hinj : Set.InjOn f s
⊢ StrictAntiOn f s

Tactic:
fun _ hx _ hy h ↦ hanti hx hy h.le |>.lt_of_ne' <| mt (hinj hx hy) h.ne

Premises used: StrictAntiOn, mt, LT.lt.le, LE.le.lt_of_ne', LT.lt.ne
-- Module: Mathlib.Order.Monotone.Basic
Goal:
α : Type u
β : Type v
inst : Preorder α
inst_1 : Preorder β
f : α → β
a : α
hf : StrictMono f
ha : IsMax (f a)
⊢ IsMax a

Tactic:
of_not_not fun h ↦
    let ⟨_, hb⟩ := not_isMax_iff.1 h
    (hf hb).not_isMax ha

Premises used: False, Iff.mp, of_not_not, not_isMax_iff, _private.0.StrictMono.isMax_of_apply.match_1, LT.lt.not_isMax
-- Module: Mathlib.Order.Monotone.Basic
Goal:
α : Type u
β : Type v
inst : Preorder α
inst_1 : Preorder β
f : α → β
a : α
hf : StrictAnti f
ha : IsMin (f a)
⊢ IsMax a

Tactic:
of_not_not fun h ↦
    let ⟨_, hb⟩ := not_isMax_iff.1 h
    (hf hb).not_isMin ha

Premises used: False, LT.lt.not_isMin, Iff.mp, of_not_not, not_isMax_iff, _private.0.StrictMono.isMax_of_apply.match_1
-- Module: Mathlib.Order.Monotone.Basic
Goal:
f : ℕ → ℕ
hf : StrictMono f
m n : ℕ
rw : f n + m ≤ f (n + m)
⊢ m + f n ≤ f (m + n)

Tactic:
rw [Nat.add_comm m, Nat.add_comm m]

Premises used: Nat.add_comm
-- Module: Mathlib.Order.Monotone.Basic
Goal:
f : ℕ → ℕ
hf : StrictMono f
n : ℕ
zero : f n ≤ f (n + 0)
zero₁ zero₂ : f n ≤ f n
⊢ f n + 0 ≤ f (n + 0)

Tactic:
rw [Nat.add_zero, Nat.add_zero]

Premises used: Nat.add_zero
-- Module: Mathlib.Order.Monotone.Basic
Goal:
f : ℕ → ℕ
hf : StrictMono f
n m : ℕ
ih : f n + m ≤ f (n + m)
succ : f n + m < f (n + m + 1)
⊢ f n + (m + 1) ≤ f (n + (m + 1))

Tactic:
rw [← Nat.add_assoc, ← Nat.add_assoc, Nat.succ_le_iff]

Premises used: Nat.add_assoc, Nat.succ_le_iff
-- Module: Mathlib.Order.Monotone.Basic
Goal:
f : ℕ → ℕ
hf : StrictMono f
n m : ℕ
ih : f n + m ≤ f (n + m)
⊢ f n + m < f (n + m + 1)

Tactic:
ih.trans_lt (hf (n + m).lt_succ_self)

Premises used: Nat.lt_succ_self, HAdd.hAdd, LE.le.trans_lt
-- Module: Mathlib.Order.Monotone.Basic
Goal:
f : ℕ → ℕ
hf : StrictMono f
n m : ℕ
ih : f n + m ≤ f (n + m)
⊢ f n + m < f (n + m + 1)

Tactic:
exact ih.trans_lt (hf (n + m).lt_succ_self)

Premises used: Nat.lt_succ_self, HAdd.hAdd, LE.le.trans_lt
-- Module: Mathlib.Order.Monotone.Basic
Goal:
f : ℕ → ℕ
hf : StrictMono f
m n : ℕ
zero : f n + 0 ≤ f (n + 0)
succ : ∀ (m : ℕ) (ih : f n + m ≤ f (n + m)), f n + (m + 1) ≤ f (n + (m + 1))
⊢ f n + m ≤ f (n + m)

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)

Premises used: Nat.add_assoc, Nat.add_zero, Nat.succ_le_iff