awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.IsNormal
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : LinearOrder β
f : α → β
hf : IsNormal f
a : α
ha : IsSuccLimit a
refine : f a ∈ upperBounds (f '' Iio a)
⊢ IsLUB (f '' Iio a) (f a)

Tactic:
refine ⟨?_, hf.2 ha⟩
-- Module: Mathlib.Order.IsNormal
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : LinearOrder β
f : α → β
hf : IsNormal f
a : α
ha : IsSuccLimit a
b : α
hb : b ∈ Iio a
⊢ f b ≤ f a

Tactic:
(hf.1 hb).le

Premises used: LT.lt.le, Order.IsNormal.strictMono
-- Module: Mathlib.Order.IsNormal
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : LinearOrder β
f : α → β
hf : IsNormal f
a : α
ha : IsSuccLimit a
b : α
hb : b ∈ Iio a
⊢ f b ≤ f a

Tactic:
exact (hf.1 hb).le

Premises used: LT.lt.le, Order.IsNormal.strictMono
-- Module: Mathlib.Order.IsNormal
Goal:
α : Type u_1
β : Type u_2
a : α
f : α → β
inst : LinearOrder α
inst_1 : LinearOrder β
hf : IsNormal f
ha : IsSuccLimit a
b : β
⊢ f a ≤ b ↔ ∀ a' < a, f a' ≤ b

Tactic:
simpa [mem_upperBounds] using isLUB_le_iff (hf.isLUB_image_Iio_of_isSuccLimit ha)

Premises used: Order.IsNormal.isLUB_image_Iio_of_isSuccLimit, isLUB_le_iff, mem_upperBounds
-- Module: Mathlib.Order.IsNormal
Goal:
α : Type u_1
β : Type u_2
a : α
f : α → β
inst : LinearOrder α
inst_1 : LinearOrder β
hf : IsNormal f
ha : IsSuccLimit a
b : β
⊢ b < f a ↔ ∃ a' < a, b < f a'

Tactic:
simpa [mem_upperBounds] using lt_isLUB_iff (hf.isLUB_image_Iio_of_isSuccLimit ha)

Premises used: Order.IsNormal.isLUB_image_Iio_of_isSuccLimit, lt_isLUB_iff, mem_upperBounds
-- Module: Mathlib.Order.IsNormal
Goal:
α : Type u_1
β : Type u_2
a : α
f : α → β
inst : LinearOrder α
inst_1 : LinearOrder β
hf : IsNormal f
ha : IsSuccLimit a
⊢ IsSuccLimit (f a)

Tactic:
⟨?_, fun b hb ↦ ?_⟩

Premises used: Order.IsSuccLimit, And.intro
-- Module: Mathlib.Order.IsNormal
Goal:
α : Type u_1
β : Type u_2
a : α
f : α → β
inst : LinearOrder α
inst_1 : LinearOrder β
hf : IsNormal f
ha : IsSuccLimit a
refine_1 : ¬IsMin (f a)
refine_2 : ∀ (b : β) (hb : b ⋖ f a), False
⊢ IsSuccLimit (f a)

Tactic:
refine ⟨?_, fun b hb ↦ ?_⟩
-- Module: Mathlib.Order.IsNormal
Goal:
α : Type u_1
β : Type u_2
a : α
f : α → β
inst : LinearOrder α
inst_1 : LinearOrder β
hf : IsNormal f
ha : IsSuccLimit a
refine_1 : ∀ (b : α) (hb : b < a), ¬IsMin (f a)
⊢ ¬IsMin (f a)

Tactic:
obtain ⟨b, hb⟩ := not_isMin_iff.1 ha.not_isMin

Premises used: not_isMin_iff, Order.IsSuccLimit.not_isMin, Iff.mp
-- Module: Mathlib.Order.IsNormal
Goal:
α : Type u_1
β : Type u_2
a : α
f : α → β
inst : LinearOrder α
inst_1 : LinearOrder β
hf : IsNormal f
ha : IsSuccLimit a
b : α
hb : b < a
⊢ ¬IsMin (f a)

Tactic:
not_isMin_iff.2 ⟨_, hf.strictMono hb⟩

Premises used: not_isMin_iff, Iff.mpr, Exists.intro, Order.IsNormal.strictMono
-- Module: Mathlib.Order.IsNormal
Goal:
α : Type u_1
β : Type u_2
a : α
f : α → β
inst : LinearOrder α
inst_1 : LinearOrder β
hf : IsNormal f
ha : IsSuccLimit a
b : α
hb : b < a
⊢ ¬IsMin (f a)

Tactic:
exact not_isMin_iff.2 ⟨_, hf.strictMono hb⟩

Premises used: not_isMin_iff, Iff.mpr, Exists.intro, Order.IsNormal.strictMono
-- Module: Mathlib.Order.IsNormal
Goal:
α : Type u_1
β : Type u_2
a : α
f : α → β
inst : LinearOrder α
inst_1 : LinearOrder β
hf : IsNormal f
ha : IsSuccLimit a
b : β
hb : b ⋖ f a
refine_2 : ∀ (c : α) (hc : c < a) (hc' : b < f c), False
⊢ False

Tactic:
obtain ⟨c, hc, hc'⟩ := (hf.lt_iff_exists_lt ha).1 hb.lt

Premises used: Order.IsNormal.lt_iff_exists_lt, Iff.mp, CovBy.lt
-- Module: Mathlib.Order.IsNormal
Goal:
α : Type u_1
β : Type u_2
a : α
f : α → β
inst : LinearOrder α
inst_1 : LinearOrder β
hf : IsNormal f
ha : IsSuccLimit a
b : β
hb : b ⋖ f a
c : α
hc : c < a
hc' : b < f c
⊢ f a ≤ f c

Tactic:
have hc' := hb.ge_of_gt hc'
-- Module: Mathlib.Order.IsNormal
Goal:
α : Type u_1
β : Type u_2
a : α
f : α → β
inst : LinearOrder α
inst_1 : LinearOrder β
hf : IsNormal f
ha : IsSuccLimit a
b : β
hb : b ⋖ f a
c : α
hc : c < a
hc'_1 : b < f c
hc' : f a ≤ f c
⊢ a ≤ c

Tactic:
rw [hf.strictMono.le_iff_le] at hc'

Premises used: Order.IsNormal.strictMono, StrictMono.le_iff_le
-- Module: Mathlib.Order.IsNormal
Goal:
α : Type u_1
β : Type u_2
a : α
f : α → β
inst : LinearOrder α
inst_1 : LinearOrder β
hf : IsNormal f
ha : IsSuccLimit a
b : β
hb : b ⋖ f a
c : α
hc : c < a
hc'_1 : b < f c
hc' : a ≤ c
⊢ False

Tactic:
hc.not_ge hc'

Premises used: LT.lt.not_ge
-- Module: Mathlib.Order.IsNormal
Goal:
α : Type u_1
β : Type u_2
a : α
f : α → β
inst : LinearOrder α
inst_1 : LinearOrder β
hf : IsNormal f
ha : IsSuccLimit a
b : β
hb : b ⋖ f a
c : α
hc : c < a
hc'_1 : b < f c
hc' : a ≤ c
⊢ False

Tactic:
exact hc.not_ge hc'

Premises used: LT.lt.not_ge
-- Module: Mathlib.Order.IsNormal
Goal:
α : Type u_1
β : Type u_2
a : α
f : α → β
inst : LinearOrder α
inst_1 : LinearOrder β
hf : IsNormal f
s : Set α
hs : IsLUB s a
hs' : s.Nonempty
⊢ IsLUB (f '' s) (f a)

Tactic:
⟨?_, fun b hb ↦ ?_⟩

Premises used: IsLeast, And.intro, IsLUB
-- Module: Mathlib.Order.IsNormal
Goal:
α : Type u_1
β : Type u_2
a : α
f : α → β
inst : LinearOrder α
inst_1 : LinearOrder β
hf : IsNormal f
s : Set α
hs : IsLUB s a
hs' : s.Nonempty
refine_1 : f a ∈ upperBounds (f '' s)
refine_2 : ∀ (b : β) (hb : b ∈ upperBounds (f '' s)), f a ≤ b
⊢ IsLUB (f '' s) (f a)

Tactic:
refine ⟨?_, fun b hb ↦ ?_⟩
-- Module: Mathlib.Order.IsNormal
Goal:
α : Type u_1
β : Type u_2
a : α
f : α → β
inst : LinearOrder α
inst_1 : LinearOrder β
hf : IsNormal f
s : Set α
hs : IsLUB s a
hs' : s.Nonempty
⊢ f a ∈ upperBounds (f '' s)

Tactic:
simpa [mem_upperBounds, hf.strictMono.le_iff_le] using hs.1

Premises used: And.left, Order.IsNormal.strictMono, StrictMono.le_iff_le, mem_upperBounds
-- Module: Mathlib.Order.IsNormal
Goal:
α : Type u_1
β : Type u_2
a : α
f : α → β
inst : LinearOrder α
inst_1 : LinearOrder β
hf : IsNormal f
s : Set α
hs : IsLUB s a
hs' : s.Nonempty
b : β
hb : b ∈ upperBounds (f '' s)
pos : ∀ (ha : a ∈ s), f a ≤ b
neg : ∀ (ha : a ∉ s), f a ≤ b
⊢ f a ≤ b

Tactic:
by_cases ha : a ∈ s
-- Module: Mathlib.Order.IsNormal
Goal:
α : Type u_1
β : Type u_2
a : α
f : α → β
inst : LinearOrder α
inst_1 : LinearOrder β
hf : IsNormal f
s : Set α
hs : IsLUB s a
hs' : s.Nonempty
b : β
hb : b ∈ upperBounds (f '' s)
ha : a ∈ s
⊢ f a ≤ b

Tactic:
simp_all [mem_upperBounds]

Premises used: mem_upperBounds
-- Module: Mathlib.Order.IsNormal
Goal:
α : Type u_1
β : Type u_2
a : α
f : α → β
inst : LinearOrder α
inst_1 : LinearOrder β
hf : IsNormal f
s : Set α
hs : IsLUB s a
hs' : s.Nonempty
b : β
hb : b ∈ upperBounds (f '' s)
ha : a ∉ s
⊢ IsSuccLimit a

Tactic:
have ha' := hs.isSuccLimit_of_notMem hs' ha
-- Module: Mathlib.Order.IsNormal
Goal:
α : Type u_1
β : Type u_2
a : α
f : α → β
inst : LinearOrder α
inst_1 : LinearOrder β
hf : IsNormal f
s : Set α
hs : IsLUB s a
hs' : s.Nonempty
b : β
hb : b ∈ upperBounds (f '' s)
ha : a ∉ s
ha' : IsSuccLimit a
neg : ∀ a' < a, f a' ≤ b
⊢ f a ≤ b

Tactic:
rw [le_iff_forall_le hf ha']

Premises used: Order.IsNormal.le_iff_forall_le
-- Module: Mathlib.Order.IsNormal
Goal:
α : Type u_1
β : Type u_2
a : α
f : α → β
inst : LinearOrder α
inst_1 : LinearOrder β
hf : IsNormal f
s : Set α
hs : IsLUB s a
hs' : s.Nonempty
b : β
hb : b ∈ upperBounds (f '' s)
ha : a ∉ s
ha' : IsSuccLimit a
c : α
hc : c < a
neg : ∀ (d : α) (hd : d ∈ s) (hcd : c < d) (hda : d ≤ a), f c ≤ b
⊢ f c ≤ b

Tactic:
obtain ⟨d, hd, hcd, hda⟩ := hs.exists_between hc

Premises used: IsLUB.exists_between
-- Module: Mathlib.Order.IsNormal
Goal:
α : Type u_1
β : Type u_2
a : α
f : α → β
inst : LinearOrder α
inst_1 : LinearOrder β
hf : IsNormal f
s : Set α
hs : IsLUB s a
hs' : s.Nonempty
b : β
hb : b ∈ upperBounds (f '' s)
ha : a ∉ s
ha' : IsSuccLimit a
c : α
hc : c < a
d : α
hd : d ∈ s
hcd : c < d
hda : d ≤ a
⊢ ∀ ⦃x : α⦄, x ∈ s → f x ≤ b

Tactic:
simp_rw [mem_upperBounds, forall_mem_image] at hb

Premises used: Set.forall_mem_image, mem_upperBounds
-- Module: Mathlib.Order.IsNormal
Goal:
α : Type u_1
β : Type u_2
a : α
f : α → β
inst : LinearOrder α
inst_1 : LinearOrder β
hf : IsNormal f
s : Set α
hs : IsLUB s a
hs' : s.Nonempty
b : β
ha : a ∉ s
ha' : IsSuccLimit a
c : α
hc : c < a
d : α
hd : d ∈ s
hcd : c < d
hda : d ≤ a
hb : ∀ ⦃x : α⦄, x ∈ s → f x ≤ b
⊢ f c ≤ b

Tactic:
(hf.strictMono hcd).le.trans (hb hd)

Premises used: LT.lt.le, LE.le.trans, Order.IsNormal.strictMono
-- Module: Mathlib.Order.IsNormal
Goal:
α : Type u_1
β : Type u_2
a : α
f : α → β
inst : LinearOrder α
inst_1 : LinearOrder β
hf : IsNormal f
s : Set α
hs : IsLUB s a
hs' : s.Nonempty
b : β
ha : a ∉ s
ha' : IsSuccLimit a
c : α
hc : c < a
d : α
hd : d ∈ s
hcd : c < d
hda : d ≤ a
hb : ∀ ⦃x : α⦄, x ∈ s → f x ≤ b
⊢ f c ≤ b

Tactic:
exact (hf.strictMono hcd).le.trans (hb hd)

Premises used: LT.lt.le, LE.le.trans, Order.IsNormal.strictMono
-- Module: Mathlib.Order.IsNormal
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : LinearOrder β
f : InitialSeg (fun (x1 x2 : α) ↦ x1 < x2) fun (x1 x2 : β) ↦ x1 < x2
a : α
ha : IsSuccLimit a
rw :
  Membership.mem.{u_2, u_2} (α := β) (γ := Set β) (lowerBounds (upperBounds (Iio ((f : (a : α) → β) a))) : Set β)
    ((f : (a : α) → β) a : β)
⊢ Membership.mem.{u_2, u_2} (α := β) (γ := Set β) (lowerBounds (upperBounds ((⇑f : (a : α) → β) '' Iio a)))
    ((f : (a : α) → β) a : β)

Tactic:
rw [f.image_Iio]

Premises used: InitialSeg.image_Iio
-- Module: Mathlib.Order.IsNormal
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : LinearOrder β
f : InitialSeg (fun (x1 x2 : α) ↦ x1 < x2) fun (x1 x2 : β) ↦ x1 < x2
a : α
ha : IsSuccLimit a
⊢ Membership.mem.{u_2, u_2} (α := β) (γ := Set β) (lowerBounds (upperBounds (Iio ((f : (a : α) → β) a))) : Set β)
    ((f : (a : α) → β) a : β)

Tactic:
(f.map_isSuccLimit ha).isLUB_Iio.2

Premises used: Order.IsSuccLimit.isLUB_Iio, InitialSeg.map_isSuccLimit, And.right
-- Module: Mathlib.Order.IsNormal
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : LinearOrder β
f : InitialSeg (fun (x1 x2 : α) ↦ x1 < x2) fun (x1 x2 : β) ↦ x1 < x2
a : α
ha : IsSuccLimit a
⊢ Membership.mem.{u_2, u_2} (α := β) (γ := Set β) (lowerBounds (upperBounds (Iio ((f : (a : α) → β) a))) : Set β)
    ((f : (a : α) → β) a : β)

Tactic:
exact (f.map_isSuccLimit ha).isLUB_Iio.2

Premises used: Order.IsSuccLimit.isLUB_Iio, InitialSeg.map_isSuccLimit, And.right
-- Module: Mathlib.Order.IsNormal
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : LinearOrder β
f : PrincipalSeg (fun (x1 x2 : α) ↦ x1 < x2) fun (x1 x2 : β) ↦ x1 < x2
⊢ IsNormal.{u_1, u_2} (α := α) (β := β)
    (⇑(f.toRelEmbedding (r := fun (x1 x2 : α) ↦ x1 < x2) (s := fun (x1 x2 : β) ↦ x1 < x2)) : (a : α) → β)

Tactic:
(f : α ≤i β).isNormal

Premises used: InitialSeg.isNormal, PrincipalSeg.toRelEmbedding, PrincipalSeg.mem_range_of_rel, InitialSeg.mk
-- Module: Mathlib.Order.IsNormal
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
inst_1 : LinearOrder β
f : α ≃o β
⊢ IsNormal.{u_1, u_2} (α := α) (β := β) (⇑f : (a : α) → β)

Tactic:
f.toInitialSeg.isNormal

Premises used: OrderIso.toInitialSeg, InitialSeg.isNormal
-- Module: Mathlib.Order.IsNormal
Goal:
α : Type u_1
inst : LinearOrder α
⊢ IsNormal.{u_1, u_1} (α := α) id

Tactic:
(OrderIso.refl _).isNormal

Premises used: OrderIso.isNormal, OrderIso.refl
-- Module: Mathlib.Order.IsNormal
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
g : β → γ
inst : LinearOrder α
inst_1 : LinearOrder β
inst_2 : LinearOrder γ
hg : IsNormal g
hf : IsNormal f
⊢ IsNormal (g ∘ f)

Tactic:
⟨hg.strictMono.comp hf.strictMono, fun ha b hb ↦ ?_⟩

Premises used: Order.IsNormal.mk, StrictMono.comp, Order.IsNormal.strictMono
-- Module: Mathlib.Order.IsNormal
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
g : β → γ
inst : LinearOrder α
inst_1 : LinearOrder β
inst_2 : LinearOrder γ
hg : IsNormal g
hf : IsNormal f
refine : ∀ {a : α} (ha : IsSuccLimit a) (b : γ) (hb : b ∈ upperBounds (g ∘ f '' Iio a)), (g ∘ f) a ≤ b
⊢ IsNormal (g ∘ f)

Tactic:
refine ⟨hg.strictMono.comp hf.strictMono, fun ha b hb ↦ ?_⟩
-- Module: Mathlib.Order.IsNormal
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
g : β → γ
inst : LinearOrder α
inst_1 : LinearOrder β
inst_2 : LinearOrder γ
hg : IsNormal g
hf : IsNormal f
a : α
ha : IsSuccLimit a
b : γ
hb : b ∈ upperBounds (g ∘ f '' Iio a)
⊢ ∀ ⦃x : α⦄, x ∈ Iio a → g (f x) ≤ b

Tactic:
simp_rw [Function.comp_apply, mem_upperBounds, forall_mem_image] at hb

Premises used: Function.comp_apply, Set.forall_mem_image, mem_upperBounds
-- Module: Mathlib.Order.IsNormal
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
g : β → γ
inst : LinearOrder α
inst_1 : LinearOrder β
inst_2 : LinearOrder γ
hg : IsNormal g
hf : IsNormal f
a : α
ha : IsSuccLimit a
b : γ
hb : ∀ ⦃x : α⦄, x ∈ Iio a → g (f x) ≤ b
⊢ (g ∘ f) a ≤ b

Tactic:
simpa [hg.le_iff_forall_le (hf.map_isSuccLimit ha), hf.lt_iff_exists_lt ha] using
    fun c d hd hc ↦ (hg.strictMono hc).le.trans (hb hd)

Premises used: LT.lt.le, Order.IsNormal.le_iff_forall_le, Order.IsNormal.lt_iff_exists_lt, Order.IsNormal.map_isSuccLimit, LE.le.trans, Order.IsNormal.strictMono
-- Module: Mathlib.Order.IsNormal
Goal:
α : Type u_1
β : Type u_2
f : α → β
inst : LinearOrder α
inst_1 : LinearOrder β
hf : IsNormal f
a : α
rw :
  (StrictMono.{u_1, u_2} (β := (↑(Iio (f a)) : Type u_2)) fun (x : (↑(Iio a) : Type u_1)) ↦
      Subtype.mk (p := fun (x : β) ↦ x ∈ Iio (f a)) (f (↑x : α)) ⋯) ∧
    ∀ (o : (↑(Iio a) : Type u_1)),
      IsSuccLimit o →
        ∀ (a_2 : (↑(Iio (f a)) : Type u_2)),
          (∀ b < o, Subtype.mk (p := fun (x : β) ↦ x ∈ Iio (f a)) (f (↑b : α)) ⋯ ≤ a_2) →
            Subtype.mk (p := fun (x : β) ↦ x ∈ Iio (f a)) (f (↑o : α)) ⋯ ≤ a_2
⊢ IsNormal.{u_1, u_2} (β := (↑(Iio (f a)) : Type u_2)) fun (x : (↑(Iio a) : Type u_1)) ↦
    Subtype.mk (p := fun (x : β) ↦ x ∈ Iio (f a)) (f (↑x : α)) ⋯

Tactic:
rw [isNormal_iff]

Premises used: Order.isNormal_iff
-- Module: Mathlib.Order.IsNormal
Goal:
α : Type u_1
β : Type u_2
f : α → β
inst : LinearOrder α
inst_1 : LinearOrder β
hf : IsNormal f
a : α
⊢ (StrictMono.{u_1, u_2} (β := (↑(Iio (f a)) : Type u_2)) fun (x : (↑(Iio a) : Type u_1)) ↦
      Subtype.mk (p := fun (x : β) ↦ x ∈ Iio (f a)) (f (↑x : α)) ⋯) ∧
    ∀ (o : (↑(Iio a) : Type u_1)),
      IsSuccLimit o →
        ∀ (a_2 : (↑(Iio (f a)) : Type u_2)),
          (∀ b < o, Subtype.mk (p := fun (x : β) ↦ x ∈ Iio (f a)) (f (↑b : α)) ⋯ ≤ a_2) →
            Subtype.mk (p := fun (x : β) ↦ x ∈ Iio (f a)) (f (↑o : α)) ⋯ ≤ a_2

Tactic:
⟨fun x y h ↦ hf.strictMono h, fun b hb c hc ↦ hf.2 (hb.subtypeVal (isLowerSet_Iio _)) ?_⟩

Premises used: isLowerSet_Iio, Order.IsNormal.mem_lowerBounds_upperBounds_of_isSuccLimit, And.intro, Order.IsSuccLimit.subtypeVal, Order.IsNormal.strictMono
-- Module: Mathlib.Order.IsNormal
Goal:
α : Type u_1
β : Type u_2
f : α → β
inst : LinearOrder α
inst_1 : LinearOrder β
hf : IsNormal f
a : α
refine :
  ∀ (b : (↑(Iio a) : Type u_1)) (hb : IsSuccLimit b) (c : (↑(Iio (f a)) : Type u_2))
    (hc : ∀ b_1 < b, Subtype.mk (p := fun (x : β) ↦ x ∈ Iio (f a)) (f (↑b_1 : α)) ⋯ ≤ c),
    (↑c : β) ∈ upperBounds (f '' Iio (↑b : α))
⊢ (StrictMono.{u_1, u_2} (β := (↑(Iio (f a)) : Type u_2)) fun (x : (↑(Iio a) : Type u_1)) ↦
      Subtype.mk (p := fun (x : β) ↦ x ∈ Iio (f a)) (f (↑x : α)) ⋯) ∧
    ∀ (o : (↑(Iio a) : Type u_1)),
      IsSuccLimit o →
        ∀ (a_2 : (↑(Iio (f a)) : Type u_2)),
          (∀ b < o, Subtype.mk (p := fun (x : β) ↦ x ∈ Iio (f a)) (f (↑b : α)) ⋯ ≤ a_2) →
            Subtype.mk (p := fun (x : β) ↦ x ∈ Iio (f a)) (f (↑o : α)) ⋯ ≤ a_2

Tactic:
refine ⟨fun x y h ↦ hf.strictMono h, fun b hb c hc ↦ hf.2 (hb.subtypeVal (isLowerSet_Iio _)) ?_⟩
-- Module: Mathlib.Order.IsNormal
Goal:
α : Type u_1
β : Type u_2
f : α → β
inst : LinearOrder α
inst_1 : LinearOrder β
hf : IsNormal f
a : α
b : (↑(Iio a) : Type u_1)
hb : IsSuccLimit b
c : (↑(Iio (f a)) : Type u_2)
hc : ∀ b_1 < b, Subtype.mk (p := fun (x : β) ↦ x ∈ Iio (f a)) (f (↑b_1 : α)) ⋯ ≤ c
⊢ (↑c : β) ∈ upperBounds (f '' Iio (↑b : α))

Tactic:
simpa [upperBounds] using fun d hd ↦ hc ⟨d, hd.trans b.2⟩ hd

Premises used: upperBounds, Subtype.mk
-- Module: Mathlib.Order.IsNormal
Goal:
α : Type u_1
β : Type u_2
f : α → β
inst : ConditionallyCompleteLinearOrder α
inst_1 : ConditionallyCompleteLinearOrder β
hf : IsNormal f
s : Set α
hs : s.Nonempty
hs' : BddAbove s
⊢ f (sSup s) = sSup (f '' s)

Tactic:
((hf.map_isLUB (isLUB_csSup hs hs') hs).csSup_eq (hs.image f)).symm

Premises used: Order.IsNormal.map_isLUB, Set.Nonempty.image, IsLUB.csSup_eq, isLUB_csSup, Eq.symm
-- Module: Mathlib.Order.IsNormal
Goal:
α : Type u_1
β : Type u_2
f : α → β
inst : ConditionallyCompleteLinearOrder α
inst_1 : ConditionallyCompleteLinearOrder β
ι : Sort u_4
inst_2 : Nonempty ι
g : ι → α
hf : IsNormal f
hg : BddAbove (range g)
unfold : f (sSup (range fun (i : ι) ↦ g i)) = sSup (range fun (i : ι) ↦ f (g i))
⊢ f (⨆ (i : ι), g i) = ⨆ (i : ι), f (g i)

Tactic:
unfold iSup

Premises used: iSup
-- Module: Mathlib.Order.IsNormal
Goal:
α : Type u_1
β : Type u_2
f : α → β
inst : ConditionallyCompleteLinearOrder α
inst_1 : ConditionallyCompleteLinearOrder β
ι : Sort u_4
inst_2 : Nonempty ι
g : ι → α
hf : IsNormal f
hg : BddAbove (range g)
⊢ f (sSup (range g)) = sSup (f '' range g)

Tactic:
map_sSup hf (range_nonempty g) hg

Premises used: Set.range_nonempty, Order.IsNormal.map_sSup
-- Module: Mathlib.Order.IsNormal
Goal:
α : Type u_1
β : Type u_2
f : α → β
inst : ConditionallyCompleteLinearOrder α
inst_1 : ConditionallyCompleteLinearOrder β
ι : Sort u_4
inst_2 : Nonempty ι
g : ι → α
hf : IsNormal f
hg : BddAbove (range g)
h : (range fun (i : ι) ↦ f (g i)) = f '' range g
⊢ f (sSup (range fun (i : ι) ↦ g i)) = sSup (range fun (i : ι) ↦ f (g i))

Tactic:
convert! map_sSup hf (range_nonempty g) hg

Premises used: Set.range_nonempty, Order.IsNormal.map_sSup
-- Module: Mathlib.Order.IsNormal
Goal:
α : Type u_1
β : Type u_2
f : α → β
inst : ConditionallyCompleteLinearOrder α
inst_1 : ConditionallyCompleteLinearOrder β
ι : Sort u_4
inst_2 : Nonempty ι
g : ι → α
hf : IsNormal f
hg : BddAbove (range g)
h : ∀ (x : β), Membership.mem (γ := Set β) (range fun (i : ι) ↦ f (g i)) x ↔ x ∈ f '' range g
⊢ (range fun (i : ι) ↦ f (g i)) = f '' range g

Tactic:
ext
-- Module: Mathlib.Order.IsNormal
Goal:
α : Type u_1
β : Type u_2
f : α → β
inst : ConditionallyCompleteLinearOrder α
inst_1 : ConditionallyCompleteLinearOrder β
ι : Sort u_4
inst_2 : Nonempty ι
g : ι → α
hf : IsNormal f
hg : BddAbove (range g)
x : β
⊢ Membership.mem (γ := Set β) (range fun (i : ι) ↦ f (g i)) x ↔ x ∈ f '' range g

Tactic:
simp
-- Module: Mathlib.Order.IsNormal
Goal:
α : Type u_1
inst : ConditionallyCompleteLinearOrder α
inst_1 : WellFoundedLT α
f : α → α
a : α
hf : IsNormal f
hf' : BddAbove.{u_1} (α := α) (range fun (n : ℕ) ↦ f^[n] a)
rw : Eq.{u_1 + 1} (α := α) (⨆ (i : ℕ), f (f^[i] a)) (⨆ (n : ℕ), f^[n] a)
⊢ ⨆ (n : ℕ), f^[n] a ∈ Function.fixedPoints f

Tactic:
rw [f.mem_fixedPoints_iff, hf.map_iSup hf']

Premises used: Function.mem_fixedPoints_iff, Order.IsNormal.map_iSup
-- Module: Mathlib.Order.IsNormal
Goal:
α : Type u_1
inst : ConditionallyCompleteLinearOrder α
inst_1 : WellFoundedLT α
f : α → α
a : α
hf : IsNormal f
hf' : BddAbove.{u_1} (α := α) (range fun (n : ℕ) ↦ f^[n] a)
a₁ : LE.le.{u_1} (α := α) (⨆ (i : ℕ), f (f^[i] a)) (⨆ (n : ℕ), f^[n] a)
a₂ : LE.le.{u_1} (α := α) (⨆ (n : ℕ), f^[n] a) (⨆ (i : ℕ), f (f^[i] a))
⊢ Eq.{u_1 + 1} (α := α) (⨆ (i : ℕ), f (f^[i] a)) (⨆ (n : ℕ), f^[n] a)

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.Order.IsNormal
Goal:
α : Type u_1
inst : ConditionallyCompleteLinearOrder α
inst_1 : WellFoundedLT α
f : α → α
a : α
hf : IsNormal f
hf' : BddAbove.{u_1} (α := α) (range fun (n : ℕ) ↦ f^[n] a)
⊢ LE.le.{u_1} (α := α) (⨆ (i : ℕ), f (f^[i] a)) (⨆ (n : ℕ), f^[n] a)

Tactic:
ciSup_le fun n ↦ ?_

Premises used: ciSup_le
-- Module: Mathlib.Order.IsNormal
Goal:
α : Type u_1
inst : ConditionallyCompleteLinearOrder α
inst_1 : WellFoundedLT α
f : α → α
a : α
hf : IsNormal f
hf' : BddAbove.{u_1} (α := α) (range fun (n : ℕ) ↦ f^[n] a)
a₁ : ∀ (n : ℕ), f (f^[n] a) ≤ ⨆ (n : ℕ), f^[n] a
⊢ LE.le.{u_1} (α := α) (⨆ (i : ℕ), f (f^[i] a)) (⨆ (n : ℕ), f^[n] a)

Tactic:
refine ciSup_le fun n ↦ ?_

Premises used: ciSup_le
-- Module: Mathlib.Order.IsNormal
Goal:
α : Type u_1
inst : ConditionallyCompleteLinearOrder α
inst_1 : WellFoundedLT α
f : α → α
a : α
hf : IsNormal f
hf' : BddAbove.{u_1} (α := α) (range fun (n : ℕ) ↦ f^[n] a)
⊢ LE.le.{u_1} (α := α) (⨆ (n : ℕ), f^[n] a) (⨆ (i : ℕ), f (f^[i] a))

Tactic:
ciSup_le fun n ↦ ?_

Premises used: ciSup_le
-- Module: Mathlib.Order.IsNormal
Goal:
α : Type u_1
inst : ConditionallyCompleteLinearOrder α
inst_1 : WellFoundedLT α
f : α → α
a : α
hf : IsNormal f
hf' : BddAbove.{u_1} (α := α) (range fun (n : ℕ) ↦ f^[n] a)
a₁ : ∀ (n : ℕ), f^[n] a ≤ ⨆ (i : ℕ), f (f^[i] a)
⊢ LE.le.{u_1} (α := α) (⨆ (n : ℕ), f^[n] a) (⨆ (i : ℕ), f (f^[i] a))

Tactic:
refine ciSup_le fun n ↦ ?_

Premises used: ciSup_le
-- Module: Mathlib.Order.IsNormal
Goal:
α : Type u_1
inst : ConditionallyCompleteLinearOrder α
inst_1 : WellFoundedLT α
f : α → α
a : α
hf : IsNormal f
hf' : BddAbove.{u_1} (α := α) (range fun (n : ℕ) ↦ f^[n] a)
n : ℕ
a₁ : f^[n.succ] a ≤ ⨆ (n : ℕ), f^[n] a
⊢ f (f^[n] a) ≤ ⨆ (n : ℕ), f^[n] a

Tactic:
rw [← f.iterate_succ_apply']

Premises used: Function.iterate_succ_apply'
-- Module: Mathlib.Order.IsNormal
Goal:
α : Type u_1
inst : ConditionallyCompleteLinearOrder α
inst_1 : WellFoundedLT α
f : α → α
a : α
hf : IsNormal f
hf' : BddAbove.{u_1} (α := α) (range fun (n : ℕ) ↦ f^[n] a)
n : ℕ
⊢ f^[n.succ] a ≤ ⨆ (n : ℕ), f^[n] a

Tactic:
le_ciSup hf' _

Premises used: le_ciSup
-- Module: Mathlib.Order.IsNormal
Goal:
α : Type u_1
inst : ConditionallyCompleteLinearOrder α
inst_1 : WellFoundedLT α
f : α → α
a : α
hf : IsNormal f
hf' : BddAbove.{u_1} (α := α) (range fun (n : ℕ) ↦ f^[n] a)
n : ℕ
⊢ f^[n.succ] a ≤ ⨆ (n : ℕ), f^[n] a

Tactic:
exact le_ciSup hf' _

Premises used: le_ciSup
-- Module: Mathlib.Order.IsNormal
Goal:
α : Type u_1
inst : ConditionallyCompleteLinearOrder α
inst_1 : WellFoundedLT α
f : α → α
a : α
hf : IsNormal f
hf' : BddAbove.{u_1} (α := α) (range fun (n : ℕ) ↦ f^[n] a)
n : ℕ
a₁ : f (f^[n] a) ≤ ⨆ (i : ℕ), f (f^[i] a)
⊢ f^[n] a ≤ ⨆ (i : ℕ), f (f^[i] a)

Tactic:
apply hf.strictMono.le_apply.trans

Premises used: StrictMono.le_apply, LE.le.trans, Order.IsNormal.strictMono
-- Module: Mathlib.Order.IsNormal
Goal:
α : Type u_1
inst : ConditionallyCompleteLinearOrder α
inst_1 : WellFoundedLT α
f : α → α
a : α
hf : IsNormal f
hf' : BddAbove.{u_1} (α := α) (range fun (n : ℕ) ↦ f^[n] a)
n : ℕ
apply : Subset.{u_1} (α := Set α) (range fun (n : ℕ) ↦ f (f^[n] a)) (range fun (n : ℕ) ↦ f^[n] a)
⊢ f (f^[n] a) ≤ ⨆ (i : ℕ), f (f^[i] a)

Tactic:
apply (le_ciSup (hf'.mono _) n)

Premises used: le_ciSup, BddAbove.mono
-- Module: Mathlib.Order.IsNormal
Goal:
α : Type u_1
inst : ConditionallyCompleteLinearOrder α
inst_1 : WellFoundedLT α
f : α → α
a : α
hf : IsNormal f
hf' : BddAbove.{u_1} (α := α) (range fun (n : ℕ) ↦ f^[n] a)
n : ℕ
simp_rw : Subset.{u_1} (α := Set α) (range fun (n : ℕ) ↦ f^[n.succ] a) (range fun (n : ℕ) ↦ f^[n] a)
⊢ Subset.{u_1} (α := Set α) (range fun (n : ℕ) ↦ f (f^[n] a)) (range fun (n : ℕ) ↦ f^[n] a)

Tactic:
simp_rw [← f.iterate_succ_apply']

Premises used: Function.iterate_succ_apply'
-- Module: Mathlib.Order.IsNormal
Goal:
α : Type u_1
inst : ConditionallyCompleteLinearOrder α
inst_1 : WellFoundedLT α
f : α → α
a : α
hf : IsNormal f
hf' : BddAbove.{u_1} (α := α) (range fun (n : ℕ) ↦ f^[n] a)
n : ℕ
⊢ Subset.{u_1} (α := Set α) (range fun (n : ℕ) ↦ f^[n.succ] a) (range fun (n : ℕ) ↦ f^[n] a)

Tactic:
grind
-- Module: Mathlib.Order.IsNormal
Goal:
α : Type u_1
β : Type u_2
f : α → β
inst : ConditionallyCompleteLinearOrder α
inst_1 : ConditionallyCompleteLinearOrder β
hf : IsNormal f
x : β
h₁ : (f ⁻¹' Iic x).Nonempty
h₂ : BddAbove (f ⁻¹' Iic x)
⊢ f ⁻¹' Iic x = Iic (sSup (f ⁻¹' Iic x))

Tactic:
le_antisymm (fun _ ↦ le_csSup h₂) (fun y hy ↦ ?_)

Premises used: le_antisymm, le_csSup
-- Module: Mathlib.Order.IsNormal
Goal:
α : Type u_1
β : Type u_2
f : α → β
inst : ConditionallyCompleteLinearOrder α
inst_1 : ConditionallyCompleteLinearOrder β
hf : IsNormal f
x : β
h₁ : (f ⁻¹' Iic x).Nonempty
h₂ : BddAbove (f ⁻¹' Iic x)
refine : ∀ (y : α) (hy : y ∈ Iic (sSup (f ⁻¹' Iic x))), y ∈ f ⁻¹' Iic x
⊢ f ⁻¹' Iic x = Iic (sSup (f ⁻¹' Iic x))

Tactic:
refine le_antisymm (fun _ ↦ le_csSup h₂) (fun y hy ↦ ?_)

Premises used: le_antisymm