awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.OmegaCompletePartialOrder
Goal:
α : Type u_2
inst : OmegaCompletePartialOrder α
f : α →𝒄 α
x : α
h : x ≤ (f : (a : α) → α) x
a :
  ∀ (i : ℕ),
    (iterateChain (↑f : α →o α) x h : (a : ℕ) → α) i ≤ ωSup ((iterateChain (↑f : α →o α) x h).map (↑f : α →o α))
⊢ ωSup (iterateChain (↑f : α →o α) x h) ≤ ωSup ((iterateChain (↑f : α →o α) x h).map (↑f : α →o α))

Tactic:
apply ωSup_le

Premises used: OmegaCompletePartialOrder.ωSup_le
-- Module: Mathlib.Order.OmegaCompletePartialOrder
Goal:
α : Type u_2
inst : OmegaCompletePartialOrder α
f : α →𝒄 α
x : α
h : x ≤ (f : (a : α) → α) x
a : (f : (a : α) → α) x ≤ ωSup ((iterateChain (↑f : α →o α) x h).map (↑f : α →o α))
⊢ (iterateChain (↑f : α →o α) x h : (a : ℕ) → α) 0 ≤ ωSup ((iterateChain (↑f : α →o α) x h).map (↑f : α →o α))

Tactic:
apply le_trans h

Premises used: le_trans
-- Module: Mathlib.Order.OmegaCompletePartialOrder
Goal:
α : Type u_2
inst : OmegaCompletePartialOrder α
f : α →𝒄 α
x : α
h : x ≤ (f : (a : α) → α) x
a :
  ((iterateChain (↑f : α →o α) x h).map (↑f : α →o α) : (a : ℕ) → α) 0 ≤
    ωSup ((iterateChain (↑f : α →o α) x h).map (↑f : α →o α))
⊢ (f : (a : α) → α) x ≤ ωSup ((iterateChain (↑f : α →o α) x h).map (↑f : α →o α))

Tactic:
change ((iterateChain f x h).map f) 0 ≤ ωSup ((iterateChain f x h).map (f : α →o α))

Premises used: OmegaCompletePartialOrder.fixedPoints.iterateChain, OrderHomClass.toOrderHom, OmegaCompletePartialOrder.Chain.map, OfNat.ofNat, OmegaCompletePartialOrder.ωSup, DFunLike.coe
-- Module: Mathlib.Order.OmegaCompletePartialOrder
Goal:
α : Type u_2
inst : OmegaCompletePartialOrder α
f : α →𝒄 α
x : α
h : x ≤ (f : (a : α) → α) x
⊢ ((iterateChain (↑f : α →o α) x h).map (↑f : α →o α) : (a : ℕ) → α) 0 ≤
    ωSup ((iterateChain (↑f : α →o α) x h).map (↑f : α →o α))

Tactic:
apply le_ωSup

Premises used: OmegaCompletePartialOrder.le_ωSup
-- Module: Mathlib.Order.OmegaCompletePartialOrder
Goal:
α : Type u_2
inst : OmegaCompletePartialOrder α
f : α →𝒄 α
x : α
h : x ≤ (f : (a : α) → α) x
n : ℕ
⊢ Eq (α := α) ((iterateChain (↑f : α →o α) x h : (a : ℕ) → α) n.succ : α)
    (((iterateChain (↑f : α →o α) x h).map (↑f : α →o α) : (a : ℕ) → α) n : α)

Tactic:
have : iterateChain f x h (n.succ) = (iterateChain f x h).map f n :=
        Function.iterate_succ_apply' ..
-- Module: Mathlib.Order.OmegaCompletePartialOrder
Goal:
α : Type u_2
inst : OmegaCompletePartialOrder α
f : α →𝒄 α
x : α
h : x ≤ (f : (a : α) → α) x
n : ℕ
this :
  Eq (α := α) ((iterateChain (↑f : α →o α) x h : (a : ℕ) → α) n.succ : α)
    (((iterateChain (↑f : α →o α) x h).map (↑f : α →o α) : (a : ℕ) → α) n : α)
a :
  ((iterateChain (↑f : α →o α) x h).map (↑f : α →o α) : (a : ℕ) → α) n ≤
    ωSup ((iterateChain (↑f : α →o α) x h).map (↑f : α →o α))
⊢ (iterateChain (↑f : α →o α) x h : (a : ℕ) → α) (n + 1) ≤ ωSup ((iterateChain (↑f : α →o α) x h).map (↑f : α →o α))

Tactic:
rw [this]
-- Module: Mathlib.Order.OmegaCompletePartialOrder
Goal:
α : Type u_2
inst : OmegaCompletePartialOrder α
f : α →𝒄 α
x : α
h : x ≤ (f : (a : α) → α) x
n : ℕ
this :
  Eq (α := α) ((iterateChain (↑f : α →o α) x h : (a : ℕ) → α) n.succ : α)
    (((iterateChain (↑f : α →o α) x h).map (↑f : α →o α) : (a : ℕ) → α) n : α)
⊢ ((iterateChain (↑f : α →o α) x h).map (↑f : α →o α) : (a : ℕ) → α) n ≤
    ωSup ((iterateChain (↑f : α →o α) x h).map (↑f : α →o α))

Tactic:
apply le_ωSup

Premises used: OmegaCompletePartialOrder.le_ωSup
-- Module: Mathlib.Order.OmegaCompletePartialOrder
Goal:
α : Type u_2
inst : OmegaCompletePartialOrder α
f : α →𝒄 α
x : α
h : x ≤ (f : (a : α) → α) x
a : α
h_a : (f : (a : α) → α) a ≤ a
h_x_le_a : x ≤ a
a₁ : ∀ (i : ℕ), (iterateChain (↑f : α →o α) x h : (a : ℕ) → α) i ≤ a
⊢ ωSup (iterateChain (↑f : α →o α) x h) ≤ a

Tactic:
apply ωSup_le

Premises used: OmegaCompletePartialOrder.ωSup_le
-- Module: Mathlib.Order.OmegaCompletePartialOrder
Goal:
α : Type u_2
inst : OmegaCompletePartialOrder α
f : α →𝒄 α
x : α
h : x ≤ (f : (a : α) → α) x
a : α
h_a : (f : (a : α) → α) a ≤ a
h_x_le_a : x ≤ a
⊢ (iterateChain (↑f : α →o α) x h : (a : ℕ) → α) 0 ≤ a

Tactic:
h_x_le_a

Premises used: Nat.iterate
-- Module: Mathlib.Order.OmegaCompletePartialOrder
Goal:
α : Type u_2
inst : OmegaCompletePartialOrder α
f : α →𝒄 α
x : α
h : x ≤ (f : (a : α) → α) x
a : α
h_a : (f : (a : α) → α) a ≤ a
h_x_le_a : x ≤ a
⊢ (iterateChain (↑f : α →o α) x h : (a : ℕ) → α) 0 ≤ a

Tactic:
exact h_x_le_a
-- Module: Mathlib.Order.OmegaCompletePartialOrder
Goal:
α : Type u_2
inst : OmegaCompletePartialOrder α
f : α →𝒄 α
x : α
h : x ≤ (f : (a : α) → α) x
a : α
h_a : (f : (a : α) → α) a ≤ a
h_x_le_a : x ≤ a
n : ℕ
h_ind : (iterateChain (↑f : α →o α) x h : (a : ℕ) → α) n ≤ a
⊢ Eq (α := α) ((iterateChain (↑f : α →o α) x h : (a : ℕ) → α) n.succ : α)
    ((f : (a : α) → α) ((iterateChain (↑f : α →o α) x h : (a : ℕ) → α) n : α) : α)

Tactic:
have : iterateChain f x h (n.succ) = f (iterateChain f x h n) :=
      Function.iterate_succ_apply' ..
-- Module: Mathlib.Order.OmegaCompletePartialOrder
Goal:
α : Type u_2
inst : OmegaCompletePartialOrder α
f : α →𝒄 α
x : α
h : x ≤ (f : (a : α) → α) x
a : α
h_a : (f : (a : α) → α) a ≤ a
h_x_le_a : x ≤ a
n : ℕ
h_ind : (iterateChain (↑f : α →o α) x h : (a : ℕ) → α) n ≤ a
this :
  Eq (α := α) ((iterateChain (↑f : α →o α) x h : (a : ℕ) → α) n.succ : α)
    ((f : (a : α) → α) ((iterateChain (↑f : α →o α) x h : (a : ℕ) → α) n : α) : α)
a₁ : (f : (a : α) → α) ((iterateChain (↑f : α →o α) x h : (a : ℕ) → α) n : α) ≤ a
⊢ (iterateChain (↑f : α →o α) x h : (a : ℕ) → α) (n + 1) ≤ a

Tactic:
rw [this]
-- Module: Mathlib.Order.OmegaCompletePartialOrder
Goal:
α : Type u_2
inst : OmegaCompletePartialOrder α
f : α →𝒄 α
x : α
h : x ≤ (f : (a : α) → α) x
a : α
h_a : (f : (a : α) → α) a ≤ a
h_x_le_a : x ≤ a
n : ℕ
h_ind : (iterateChain (↑f : α →o α) x h : (a : ℕ) → α) n ≤ a
this :
  Eq (α := α) ((iterateChain (↑f : α →o α) x h : (a : ℕ) → α) n.succ : α)
    ((f : (a : α) → α) ((iterateChain (↑f : α →o α) x h : (a : ℕ) → α) n : α) : α)
⊢ (f : (a : α) → α) ((iterateChain (↑f : α →o α) x h : (a : ℕ) → α) n : α) ≤ a

Tactic:
le_trans (f.monotone h_ind) h_a

Premises used: OmegaCompletePartialOrder.ContinuousHom.monotone, le_trans
-- Module: Mathlib.Order.OmegaCompletePartialOrder
Goal:
α : Type u_2
inst : OmegaCompletePartialOrder α
f : α →𝒄 α
x : α
h : x ≤ (f : (a : α) → α) x
a : α
h_a : (f : (a : α) → α) a ≤ a
h_x_le_a : x ≤ a
n : ℕ
h_ind : (iterateChain (↑f : α →o α) x h : (a : ℕ) → α) n ≤ a
this :
  Eq (α := α) ((iterateChain (↑f : α →o α) x h : (a : ℕ) → α) n.succ : α)
    ((f : (a : α) → α) ((iterateChain (↑f : α →o α) x h : (a : ℕ) → α) n : α) : α)
⊢ (f : (a : α) → α) ((iterateChain (↑f : α →o α) x h : (a : ℕ) → α) n : α) ≤ a

Tactic:
exact le_trans (f.monotone h_ind) h_a

Premises used: OmegaCompletePartialOrder.ContinuousHom.monotone, le_trans
-- Module: Mathlib.Order.OmegaCompletePartialOrder
Goal:
α : Type u_2
inst : OmegaCompletePartialOrder α
f : α →𝒄 α
x : α
h : x ≤ (f : (a : α) → α) x
a : α
h_a : (f : (a : α) → α) a ≤ a
h_x_le_a : x ≤ a
n : ℕ
a₁ : (iterateChain (↑f : α →o α) x h : (a : ℕ) → α) 0 ≤ a
a₂ :
  ∀ (n : ℕ) (h_ind : (iterateChain (↑f : α →o α) x h : (a : ℕ) → α) n ≤ a),
    (iterateChain (↑f : α →o α) x h : (a : ℕ) → α) (n + 1) ≤ a
⊢ (iterateChain (↑f : α →o α) x h : (a : ℕ) → α) n ≤ a

Tactic:
induction n with
  | zero => exact h_x_le_a
  | succ n h_ind =>
    have : iterateChain f x h (n.succ) = f (iterateChain f x h n) :=
      Function.iterate_succ_apply' ..
    rw [this]
    exact le_trans (f.monotone h_ind) h_a
-- Module: Mathlib.Order.OmegaCompletePartialOrder
Goal:
α : Type u_2
inst : OmegaCompletePartialOrder α
f : α →𝒄 α
x : α
h : x ≤ (f : (a : α) → α) x
a : α
h_a : Membership.mem (γ := Set α) (fixedPoints (⇑f : (a : α) → α)) a
h_x_le_a : x ≤ a
⊢ IsFixedPt (⇑f : (a : α) → α) a

Tactic:
rw [mem_fixedPoints] at h_a

Premises used: Function.mem_fixedPoints
-- Module: Mathlib.Order.OmegaCompletePartialOrder
Goal:
α : Type u_2
inst : OmegaCompletePartialOrder α
f : α →𝒄 α
x : α
h : x ≤ (f : (a : α) → α) x
a : α
h_a : Membership.mem (γ := Set α) (fixedPoints (⇑f : (a : α) → α)) a
h_x_le_a : x ≤ a
h_a₁ : IsFixedPt (⇑f : (a : α) → α) a
⊢ x ≤ a

Tactic:
rw [mem_fixedPoints] at h_a

Premises used: Function.mem_fixedPoints
-- Module: Mathlib.Order.OmegaCompletePartialOrder
Goal:
α : Type u_2
inst : OmegaCompletePartialOrder α
f : α →𝒄 α
x : α
h : x ≤ (f : (a : α) → α) x
a : α
h_a : IsFixedPt (⇑f : (a : α) → α) a
h_x_le_a : x ≤ a
⊢ (f : (a : α) → α) a ≤ a

Tactic:
obtain h_a := Eq.le h_a

Premises used: Eq.le
-- Module: Mathlib.Order.OmegaCompletePartialOrder
Goal:
α : Type u_2
inst : OmegaCompletePartialOrder α
f : α →𝒄 α
x : α
h : x ≤ (f : (a : α) → α) x
a : α
h_a_1 : IsFixedPt (⇑f : (a : α) → α) a
h_x_le_a : x ≤ a
h_a : (f : (a : α) → α) a ≤ a
⊢ ωSup (iterateChain (↑f : α →o α) x h) ≤ a

Tactic:
ωSup_iterate_le_prefixedPoint f x h h_a h_x_le_a

Premises used: OmegaCompletePartialOrder.fixedPoints.ωSup_iterate_le_prefixedPoint
-- Module: Mathlib.Order.OmegaCompletePartialOrder
Goal:
α : Type u_2
inst : OmegaCompletePartialOrder α
f : α →𝒄 α
x : α
h : x ≤ (f : (a : α) → α) x
a : α
h_a_1 : IsFixedPt (⇑f : (a : α) → α) a
h_x_le_a : x ≤ a
h_a : (f : (a : α) → α) a ≤ a
⊢ ωSup (iterateChain (↑f : α →o α) x h) ≤ a

Tactic:
exact ωSup_iterate_le_prefixedPoint f x h h_a h_x_le_a

Premises used: OmegaCompletePartialOrder.fixedPoints.ωSup_iterate_le_prefixedPoint
-- Module: Mathlib.Order.OrdContinuous
Goal:
α : Type u
inst : Preorder α
s : Set α
x : α
h : IsLUB s x
⊢ IsLUB (id '' s) (id x)

Tactic:
simpa only [image_id] using h

Premises used: Set.image_id
-- Module: Mathlib.Order.OrdContinuous
Goal:
α : Type u
β : Type v
inst : Preorder α
inst_1 : Preorder β
f : α → β
⊢ LeftOrdContinuous f →
    RightOrdContinuous (α := αᵒᵈ) (β := βᵒᵈ) ((⇑toDual : (a : β) → βᵒᵈ) ∘ f ∘ (⇑ofDual : (a : αᵒᵈ) → α))

Tactic:
id

Premises used: RightOrdContinuous, lowerBounds, Set.Mem, setOf, id, upperBounds, IsGreatest, IsGLB, OrderDual
-- Module: Mathlib.Order.OrdContinuous
Goal:
α : Type u
β : Type v
inst : Preorder α
inst_1 : Preorder β
f : α → β
hf : LeftOrdContinuous f
s : Set α
x : α
h : IsGreatest s x
⊢ IsGreatest (f '' s) (f x)

Tactic:
⟨mem_image_of_mem f h.1, (hf h.isLUB).1⟩

Premises used: IsGreatest.isLUB, IsGreatest, And.left, Set.mem_image_of_mem, And.intro
-- Module: Mathlib.Order.OrdContinuous
Goal:
α : Type u
β : Type v
inst : Preorder α
inst_1 : Preorder β
f : α → β
hf : LeftOrdContinuous f
a₁ a₂ : α
h : a₁ ≤ a₂
⊢ Membership.mem (γ := Set α) (upperBounds {a₁, a₂}) a₂

Tactic:
simp [*]
-- Module: Mathlib.Order.OrdContinuous
Goal:
α : Type u
β : Type v
γ : Type w
inst : Preorder α
inst_1 : Preorder β
inst_2 : Preorder γ
g : β → γ
f : α → β
hg : LeftOrdContinuous g
hf : LeftOrdContinuous f
s : Set α
x : α
h : IsLUB s x
⊢ IsLUB (g ∘ f '' s) ((g ∘ f) x)

Tactic:
simpa only [image_image] using hg (hf h)

Premises used: Set.image_image
-- Module: Mathlib.Order.OrdContinuous
Goal:
α : Type u
inst : Preorder α
f : α → α
hf : LeftOrdContinuous f
n : ℕ
⊢ LeftOrdContinuous f^[n]

Tactic:
match n with
  | 0 => LeftOrdContinuous.id α
  | (n + 1) => (LeftOrdContinuous.iterate hf n).comp hf

Premises used: LeftOrdContinuous, Nat.iterate, LeftOrdContinuous.id, _private.0.LeftOrdContinuous.iterate.match_1, LeftOrdContinuous.comp
-- Module: Mathlib.Order.OrdContinuous
Goal:
α : Type u
β : Type v
inst : SemilatticeSup α
inst_1 : SemilatticeSup β
f : α → β
hf : LeftOrdContinuous f
x y : α
⊢ IsLUB (f '' {x, y}) (f x ⊔ f y)

Tactic:
simp only [image_pair, isLUB_pair]

Premises used: Set.image_pair, isLUB_pair
-- Module: Mathlib.Order.OrdContinuous
Goal:
α : Type u
β : Type v
inst : SemilatticeSup α
inst_1 : SemilatticeSup β
f : α → β
hf : LeftOrdContinuous f
h : Injective f
x y : α
⊢ f x ≤ f y ↔ x ≤ y

Tactic:
simp only [← sup_eq_right, ← hf.map_sup, h.eq_iff]

Premises used: LeftOrdContinuous.map_sup, Function.Injective.eq_iff, sup_eq_right
-- Module: Mathlib.Order.OrdContinuous
Goal:
α : Type u
β : Type v
inst : SemilatticeSup α
inst_1 : SemilatticeSup β
f : α → β
hf : LeftOrdContinuous f
h : Injective f
x y : α
⊢ f x < f y ↔ x < y

Tactic:
simp only [lt_iff_le_not_ge, hf.le_iff h]

Premises used: LeftOrdContinuous.le_iff, lt_iff_le_not_ge
-- Module: Mathlib.Order.OrdContinuous
Goal:
α : Type u
β : Type v
inst : SemilatticeSup α
inst_1 : SemilatticeSup β
f : α → β
hf : LeftOrdContinuous f
h : Injective f
⊢ (⇑(toOrderEmbedding f hf h) : (a : α) → β) = f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.OrdContinuous
Goal:
α : Type u
β : Type v
inst : CompleteLattice α
inst_1 : CompleteLattice β
f : α → β
hf : LeftOrdContinuous f
s : Set α
⊢ f (sSup s) = sSup (f '' s)

Tactic:
(hf <| isLUB_sSup s).sSup_eq.symm

Premises used: IsLUB.sSup_eq, isLUB_sSup, Eq.symm
-- Module: Mathlib.Order.OrdContinuous
Goal:
α : Type u
β : Type v
inst : CompleteLattice α
inst_1 : CompleteLattice β
f : α → β
hf : LeftOrdContinuous f
s : Set α
rw : sSup (f '' s) = ⨆ x ∈ s, f x
rw₁ rw₂ : Eq.{v + 1} (α := β) (⨆ a ∈ s, f a) (⨆ x ∈ s, f x)
⊢ f (sSup s) = ⨆ x ∈ s, f x

Tactic:
rw [hf.map_sSup', sSup_image]

Premises used: LeftOrdContinuous.map_sSup', sSup_image
-- Module: Mathlib.Order.OrdContinuous
Goal:
α : Type u
β : Type v
ι : Sort x
inst : CompleteLattice α
inst_1 : CompleteLattice β
f : α → β
hf : LeftOrdContinuous f
g : ι → α
simp : sSup (range.{v, x} (ι := ι) (f ∘ fun (i : ι) ↦ g i)) = sSup (range fun (i : ι) ↦ f (g i))
⊢ f (⨆ (i : ι), g i) = ⨆ (i : ι), f (g i)

Tactic:
simp only [iSup, hf.map_sSup', ← range_comp]

Premises used: Set.range_comp, iSup, LeftOrdContinuous.map_sSup'
-- Module: Mathlib.Order.OrdContinuous
Goal:
α : Type u
β : Type v
ι : Sort x
inst : CompleteLattice α
inst_1 : CompleteLattice β
f : α → β
hf : LeftOrdContinuous f
g : ι → α
⊢ sSup (range.{v, x} (ι := ι) (f ∘ fun (i : ι) ↦ g i)) = sSup (range fun (i : ι) ↦ f (g i))

Tactic:
rfl
-- Module: Mathlib.Order.OrdContinuous
Goal:
α : Type u
β : Type v
inst : ConditionallyCompleteLattice α
inst_1 : ConditionallyCompleteLattice β
f : α → β
hf : LeftOrdContinuous f
s : Set α
sne : s.Nonempty
sbdd : BddAbove s
⊢ f (sSup s) = sSup (f '' s)

Tactic:
((hf <| isLUB_csSup sne sbdd).csSup_eq <| sne.image f).symm

Premises used: Set.Nonempty.image, IsLUB.csSup_eq, isLUB_csSup, Eq.symm
-- Module: Mathlib.Order.OrdContinuous
Goal:
α : Type u
β : Type v
ι : Sort x
inst : ConditionallyCompleteLattice α
inst_1 : ConditionallyCompleteLattice β
inst_2 : Nonempty ι
f : α → β
hf : LeftOrdContinuous f
g : ι → α
hg : BddAbove (range g)
simp : sSup (range (f ∘ g)) = sSup (range fun (i : ι) ↦ f (g i))
⊢ f (⨆ (i : ι), g i) = ⨆ (i : ι), f (g i)

Tactic:
simp only [iSup, hf.map_csSup (range_nonempty _) hg, ← range_comp]

Premises used: Set.range_comp, iSup, Set.range_nonempty, LeftOrdContinuous.map_csSup
-- Module: Mathlib.Order.OrdContinuous
Goal:
α : Type u
β : Type v
ι : Sort x
inst : ConditionallyCompleteLattice α
inst_1 : ConditionallyCompleteLattice β
inst_2 : Nonempty ι
f : α → β
hf : LeftOrdContinuous f
g : ι → α
hg : BddAbove (range g)
⊢ sSup (range (f ∘ g)) = sSup (range fun (i : ι) ↦ f (g i))

Tactic:
rfl
-- Module: Mathlib.Order.OrdContinuous
Goal:
α : Type u
β : Type v
inst : Preorder α
inst_1 : Preorder β
f : α → β
g : β → α
gc : GaloisConnection f g
⊢ LeftOrdContinuous f

Tactic:
fun _ _ ↦ gc.isLUB_l_image

Premises used: GaloisConnection.isLUB_l_image, LeftOrdContinuous
-- Module: Mathlib.Order.OrdContinuous
Goal:
α : Type u
β : Type v
inst : Preorder α
inst_1 : Preorder β
f : α → β
g : β → α
gc : GaloisConnection f g
⊢ RightOrdContinuous g

Tactic:
fun _ _ ↦ gc.isGLB_u_image

Premises used: RightOrdContinuous, GaloisConnection.isGLB_u_image
-- Module: Mathlib.Order.OrdContinuous
Goal:
α : Type u
β : Type v
inst : Preorder α
inst_1 : Preorder β
e : α ≃o β
⊢ LeftOrdContinuous.{u, v} (α := α) (β := β) (⇑e : (a : α) → β)

Tactic:
e.to_galoisConnection.leftOrdContinuous

Premises used: OrderIso.to_galoisConnection, GaloisConnection.leftOrdContinuous
-- Module: Mathlib.Order.OrdContinuous
Goal:
α : Type u
β : Type v
inst : Preorder α
inst_1 : Preorder β
e : α ≃o β
⊢ RightOrdContinuous.{u, v} (α := α) (β := β) (⇑e : (a : α) → β)

Tactic:
e.symm.to_galoisConnection.rightOrdContinuous

Premises used: OrderIso.to_galoisConnection, OrderIso.symm, GaloisConnection.rightOrdContinuous
-- Module: Mathlib.Order.OrderDual
Goal:
α_1 : Type u_1
α : Type u_2
h : Nonempty α
⊢ Nonempty.{u_2 + 1} αᵒᵈ

Tactic:
h

Premises used: OrderDual
-- Module: Mathlib.Order.OrderDual
Goal:
α_1 : Type u_1
α : Type u_2
h : Subsingleton α
⊢ Subsingleton.{u_2 + 1} αᵒᵈ

Tactic:
h

Premises used: OrderDual
-- Module: Mathlib.Order.OrderDual
Goal:
α : Type u_1
inst : LT α
T : Std.Trichotomous.{u_1 + 1} (α := α) LT.lt
a b : αᵒᵈ
rw : ¬a < b → ¬b < a → b = a
⊢ ¬a < b → ¬b < a → a = b

Tactic:
rw [eq_comm]

Premises used: eq_comm
-- Module: Mathlib.Order.OrderDual
Goal:
α : Type u_1
inst : LT α
T : Std.Trichotomous.{u_1 + 1} (α := α) LT.lt
a b : αᵒᵈ
⊢ ¬a < b → ¬b < a → b = a

Tactic:
T.trichotomous b a

Premises used: OrderDual, Std.Trichotomous.trichotomous
-- Module: Mathlib.Order.OrderDual
Goal:
α : Type u_1
inst : LT α
T : Std.Trichotomous.{u_1 + 1} (α := α) LT.lt
a b : αᵒᵈ
⊢ ¬a < b → ¬b < a → b = a

Tactic:
exact T.trichotomous b a

Premises used: Std.Trichotomous.trichotomous
-- Module: Mathlib.Order.OrderDual
Goal:
α_1 : Type u_1
α : Type u_2
inst : LinearOrder α
a b : αᵒᵈ
simp :
  (if b < a then Ordering.lt else if a = b then Ordering.eq else Ordering.gt) =
    if a < b then Ordering.lt else if a = b then Ordering.eq else Ordering.gt
⊢ compare a b = compareOfLessAndEq a b

Tactic:
simp only [compare, LinearOrder.compare_eq_compareOfLessAndEq, compareOfLessAndEq, eq_comm]

Premises used: compareOfLessAndEq, eq_comm, Ord.compare, LinearOrder.compare_eq_compareOfLessAndEq
-- Module: Mathlib.Order.OrderDual
Goal:
α_1 : Type u_1
α : Type u_2
inst : LinearOrder α
a b : αᵒᵈ
⊢ (if b < a then Ordering.lt else if a = b then Ordering.eq else Ordering.gt) =
    if a < b then Ordering.lt else if a = b then Ordering.eq else Ordering.gt

Tactic:
rfl
-- Module: Mathlib.Order.OrderDual
Goal:
α : Type u_2
H : Ord α
⊢ instOrd αᵒᵈ = H

Tactic:
rfl

Premises used: OrderDual, rfl
-- Module: Mathlib.Order.OrderDual
Goal:
α : Type u_2
H : Preorder α
⊢ instPreorder αᵒᵈ = H

Tactic:
rfl

Premises used: OrderDual, rfl
-- Module: Mathlib.Order.OrderDual
Goal:
α : Type u_2
H : PartialOrder α
⊢ instPartialOrder αᵒᵈ = H

Tactic:
rfl

Premises used: OrderDual, rfl
-- Module: Mathlib.Order.OrderDual
Goal:
α : Type u_2
H : LinearOrder α
⊢ instLinearOrder αᵒᵈ = H

Tactic:
rfl

Premises used: OrderDual, rfl
-- Module: Mathlib.Order.OrderDual
Goal:
α : Type u_1
h : Nontrivial α
⊢ Nontrivial.{u_1} αᵒᵈ

Tactic:
h

Premises used: OrderDual
-- Module: Mathlib.Order.OrderDual
Goal:
α : Type u_1
⊢ Eq.{u_1 + 1} (α := αᵒᵈ ≃ α) (Equiv.symm toDual) ofDual

Tactic:
rfl

Premises used: OrderDual.ofDual, OrderDual, Equiv.symm, Equiv.refl, rfl
-- Module: Mathlib.Order.OrderDual
Goal:
α : Type u_1
⊢ Eq.{u_1 + 1} (α := α ≃ αᵒᵈ) (Equiv.symm ofDual) toDual

Tactic:
rfl

Premises used: OrderDual.toDual, OrderDual, Equiv.symm, Equiv.refl, rfl
-- Module: Mathlib.Order.OrderDual
Goal:
α : Type u_1
a : αᵒᵈ
⊢ (toDual : (a : α) → αᵒᵈ) ((ofDual : (a : αᵒᵈ) → α) a : α) = a

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.OrderDual
Goal:
α : Type u_1
a : α
⊢ (ofDual : (a : αᵒᵈ) → α) ((toDual : (a : α) → αᵒᵈ) a : αᵒᵈ) = a

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.OrderDual
Goal:
α : Type u_1
⊢ Equiv.trans toDual ofDual = Equiv.refl α

Tactic:
rfl

Premises used: Equiv.refl, rfl
-- Module: Mathlib.Order.OrderDual
Goal:
α : Type u_1
⊢ Eq.{u_1 + 1} (α := αᵒᵈ ≃ αᵒᵈ) (Equiv.trans ofDual toDual) (Equiv.refl αᵒᵈ)

Tactic:
rfl

Premises used: Equiv.refl, rfl
-- Module: Mathlib.Order.OrderDual
Goal:
α : Type u_1
⊢ Eq.{u_1 + 1} (α := αᵒᵈ → αᵒᵈ) (Function.comp (β := α) (⇑toDual : (a : α) → αᵒᵈ) (⇑ofDual : (a : αᵒᵈ) → α)) id

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.OrderDual
Goal:
α : Type u_1
⊢ Eq.{u_1 + 1} (α := α → α) (Function.comp (β := αᵒᵈ) (⇑ofDual : (a : αᵒᵈ) → α) (⇑toDual : (a : α) → αᵒᵈ)) id

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.OrderDual
Goal:
α : Type u_1
a b : α
⊢ Eq (α := αᵒᵈ) ((toDual : (a : α) → αᵒᵈ) a : αᵒᵈ) ((toDual : (a : α) → αᵒᵈ) b : αᵒᵈ) ↔ a = b

Tactic:
simp
-- Module: Mathlib.Order.OrderDual
Goal:
α : Type u_1
a b : αᵒᵈ
⊢ Eq (α := α) ((ofDual : (a : αᵒᵈ) → α) a : α) ((ofDual : (a : αᵒᵈ) → α) b : α) ↔ a = b

Tactic:
simp
-- Module: Mathlib.Order.OrderDual
Goal:
α : Type u_1
a b : αᵒᵈ
h : Eq (α := α) ((ofDual : (a : αᵒᵈ) → α) a : α) ((ofDual : (a : αᵒᵈ) → α) b : α)
⊢ a = b

Tactic:
h

Premises used: OrderDual
-- Module: Mathlib.Order.OrderDual
Goal:
α : Type u_1
inst : LE α
a b : α
⊢ LE.le (α := αᵒᵈ) ((toDual : (a : α) → αᵒᵈ) a : αᵒᵈ) ((toDual : (a : α) → αᵒᵈ) b : αᵒᵈ) ↔ b ≤ a

Tactic:
.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Order.OrderDual
Goal:
α : Type u_1
inst : LT α
a b : α
⊢ LT.lt (α := αᵒᵈ) ((toDual : (a : α) → αᵒᵈ) a : αᵒᵈ) ((toDual : (a : α) → αᵒᵈ) b : αᵒᵈ) ↔ b < a

Tactic:
.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Order.OrderDual
Goal:
α : Type u_1
inst : LE α
a b : αᵒᵈ
⊢ LE.le (α := α) ((ofDual : (a : αᵒᵈ) → α) a : α) ((ofDual : (a : αᵒᵈ) → α) b : α) ↔ b ≤ a

Tactic:
.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Order.OrderDual
Goal:
α : Type u_1
inst : LT α
a b : αᵒᵈ
⊢ LT.lt (α := α) ((ofDual : (a : αᵒᵈ) → α) a : α) ((ofDual : (a : αᵒᵈ) → α) b : α) ↔ b < a

Tactic:
.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Order.OrderDual
Goal:
α : Type u_1
inst : LE α
a : αᵒᵈ
b : α
⊢ a ≤ (toDual : (a : α) → αᵒᵈ) b ↔ b ≤ (ofDual : (a : αᵒᵈ) → α) a

Tactic:
.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Order.OrderDual
Goal:
α : Type u_1
inst : LT α
a : αᵒᵈ
b : α
⊢ a < (toDual : (a : α) → αᵒᵈ) b ↔ b < (ofDual : (a : αᵒᵈ) → α) a

Tactic:
.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Order.OrderDual
Goal:
α : Type u_1
p : αᵒᵈ → Prop
⊢ (∀ (a : αᵒᵈ), p a) ↔ ∀ (a : α), p ((toDual : (a : α) → αᵒᵈ) a)

Tactic:
.rfl

Premises used: Iff.rfl, OrderDual
-- Module: Mathlib.Order.OrderDual
Goal:
α : Type u_1
p : αᵒᵈ → Prop
⊢ (∃ (a : αᵒᵈ), p a) ↔ ∃ (a : α), p ((toDual : (a : α) → αᵒᵈ) a)

Tactic:
.rfl

Premises used: Iff.rfl, OrderDual
-- Module: Mathlib.Order.OrderDual
Goal:
α_1 : Type u_1
α : Type u_2
inst : LT α
h : DenselyOrdered α
⊢ DenselyOrdered.{u_2} αᵒᵈ

Tactic:
⟨fun _ _ ha ↦ (@exists_between α _ h _ _ ha).imp fun _ ↦ And.symm⟩

Premises used: exists_between, Exists.imp, DenselyOrdered.mk, And.symm
-- Module: Mathlib.Order.OrderDual
Goal:
α : Type u_1
inst : LT α
⊢ ∀ [h : DenselyOrdered.{u_1} αᵒᵈ], DenselyOrdered.{u_1} αᵒᵈᵒᵈ

Tactic:
@OrderDual.denselyOrdered αᵒᵈ _

Premises used: OrderDual.denselyOrdered, OrderDual
-- Module: Mathlib.Order.OrderDual
Goal:
α : Type u_1
inst : LT α
⊢ DenselyOrdered.{u_1} αᵒᵈ → DenselyOrdered α

Tactic:
convert! @OrderDual.denselyOrdered αᵒᵈ _

Premises used: OrderDual.denselyOrdered, OrderDual
-- Module: Mathlib.Order.OrderDual
Goal:
α : Type u_1
β : Type u_2
e : α ≃ β
inst : Top β
⊢ Eq.{u_1 + 1} (α := α) (⊤ : α) ((e.symm : (a : β) → α) ⊤ : α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.OrderDual
Goal:
α : Type u_1
β : Type u_2
e : α ≃ β
inst : Bot β
⊢ Eq.{u_1 + 1} (α := α) (⊥ : α) ((e.symm : (a : β) → α) ⊥ : α)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.OrderDual
Goal:
α : Type u_1
β : Type u_2
e : α ≃ β
inst : Compl β
a : α
⊢ aᶜ = (e.symm : (a : β) → α) (((e : (a : α) → β) a)ᶜ : β)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.OrderDual
Goal:
α : Type u_1
β : Type u_2
e : α ≃ β
inst : SDiff β
a b : α
⊢ a \ b = (e.symm : (a : β) → α) ((e : (a : α) → β) a \ (e : (a : α) → β) b : β)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.OrderDual
Goal:
α : Type u_1
β : Type u_2
e : α ≃ β
inst : HImp β
a b : α
⊢ a ⇨ b = (e.symm : (a : β) → α) ((e : (a : α) → β) a ⇨ (e : (a : α) → β) b : β)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.OrderDual
Goal:
α : Type u_1
β : Type u_2
e : α ≃ β
inst : HNot β
a : α
⊢ ￢a = (e.symm : (a : β) → α) (￢(e : (a : α) → β) a : β)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.OrderIsoNat
Goal:
α : Type u_1
r : α → α → Prop
inst : IsStrictOrder α r
f : ℕ → α
H : ∀ (n : ℕ), r (f n) (f (n + 1))
⊢ (⇑(natLT (r := r) f H) : (a : ℕ) → α) = f

Tactic:
rfl

Premises used: rfl