awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Order.Interval.Set.IsoIoo (goal)
Goal:
k : Type u_1
inst : Field k
inst_1 : LinearOrder k
inst_2 : IsStrictOrderedRing k
⊢ k ≃o (↑(Ioo (-1) 1) : Type u_1)
have refine_1 : k → (↑(Ioo (-1) 1) : Type u_1)
Tactic: refine StrictMono.orderIsoOfRightInverse ?_ ?_ (fun x ↦ x / (1 - |↑x|)) ?_
-- Lean 4 proof step from Mathlib.Order.Interval.Set.IsoIoo (goal)
Goal:
k : Type u_1
inst : Field k
inst_1 : LinearOrder k
inst_2 : IsStrictOrderedRing k
refine_1 : k → (↑(Ioo (-1) 1) : Type u_1)
⊢ k ≃o (↑(Ioo (-1) 1) : Type u_1)
have refine_2 : StrictMono.{u_1, u_1} (α := k) (β := (↑(Ioo (-1) 1) : Type u_1))
  (codRestrict (fun (x : k) ↦ x / (1 + |x|)) (Ioo (-1) 1) sorry)
Tactic: refine StrictMono.orderIsoOfRightInverse ?_ ?_ (fun x ↦ x / (1 - |↑x|)) ?_
-- Lean 4 proof step from Mathlib.Order.Interval.Set.IsoIoo (goal)
Goal:
k : Type u_1
inst : Field k
inst_1 : LinearOrder k
inst_2 : IsStrictOrderedRing k
refine_1 : k → (↑(Ioo (-1) 1) : Type u_1)
refine_2 :
  StrictMono.{u_1, u_1} (α := k) (β := (↑(Ioo (-1) 1) : Type u_1))
    (codRestrict (fun (x : k) ↦ x / (1 + |x|)) (Ioo (-1) 1) ⋯)
⊢ k ≃o (↑(Ioo (-1) 1) : Type u_1)
have refine_3 : Function.RightInverse (α := k) (fun (x : (↑(Ioo (-1) 1) : Type u_1)) ↦ (↑x : k) / (1 - |(↑x : k)|))
  (codRestrict (fun (x : k) ↦ x / (1 + |x|)) (Ioo (-1) 1) sorry)
Tactic: refine StrictMono.orderIsoOfRightInverse ?_ ?_ (fun x ↦ x / (1 - |↑x|)) ?_
-- Lean 4 proof step from Mathlib.Order.Interval.Set.IsoIoo (goal)
Goal:
k : Type u_1
inst : Field k
inst_1 : LinearOrder k
inst_2 : IsStrictOrderedRing k
⊢ k → (↑(Ioo (-1) 1) : Type u_1)
have refine_1 : ∀ (x : k), LT.lt.{u_1} (α := k) |(fun (x : k) ↦ x / (1 + |x|)) x| 1
Tactic: refine codRestrict (fun x ↦ x / (1 + |x|)) _ fun x ↦ abs_lt.1 ?_
-- Lean 4 proof step from Mathlib.Order.Interval.Set.IsoIoo (hypothesis)
Goal:
k : Type u_1
inst : Field k
inst_1 : LinearOrder k
inst_2 : IsStrictOrderedRing k
x : k
⊢ LT.lt.{u_1} (α := k) |(fun (x : k) ↦ x / (1 + |x|)) x| 1
have H : 0 < 1 + |x|
Tactic: have H : 0 < 1 + |x| := (abs_nonneg x).trans_lt (lt_one_add _)
-- Lean 4 proof step from Mathlib.Order.Interval.Set.IsoIoo (goal)
Goal:
k : Type u_1
inst : Field k
inst_1 : LinearOrder k
inst_2 : IsStrictOrderedRing k
x : k
H : 0 < 1 + |x|
⊢ |x / (1 + |x|)| = |x| / (1 + |x|)
have rw : |x| / |1 + |x|| = |x| / (1 + |x|)
Tactic: rw [abs_div, abs_of_pos H]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.IsoIoo (goal)
Goal:
k : Type u_1
inst : Field k
inst_1 : LinearOrder k
inst_2 : IsStrictOrderedRing k
x : k
H : 0 < 1 + |x|
rw : |x| / |1 + |x|| = |x| / (1 + |x|)
⊢ |x / (1 + |x|)| = |x| / (1 + |x|)
have rw₁ : |x| / (1 + |x|) = |x| / (1 + |x|)
Tactic: rw [abs_div, abs_of_pos H]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.IsoIoo (goal)
Goal:
k : Type u_1
inst : Field k
inst_1 : LinearOrder k
inst_2 : IsStrictOrderedRing k
x : k
H : 0 < 1 + |x|
⊢ LT.lt.{u_1} (α := k) |(fun (x : k) ↦ x / (1 + |x|)) x| 1
have by : |x / (1 + |x|)| = |x| / (1 + |x|)
Tactic: calc
      |x / (1 + |x|)| = |x| / (1 + |x|) := by rw [abs_div, abs_of_pos H]
      _ < 1 := (div_lt_one H).2 (lt_one_add _)
-- Lean 4 proof step from Mathlib.Order.Interval.Set.IsoIoo (goal)
Goal:
k : Type u_1
inst : Field k
inst_1 : LinearOrder k
inst_2 : IsStrictOrderedRing k
⊢ StrictMono.{u_1, u_1} (α := k) (β := (↑(Ioo (-1) 1) : Type u_1))
    (codRestrict (fun (x : k) ↦ x / (1 + |x|)) (Ioo (-1) 1) ⋯)
have refine_2 : ∀ (x : k), -x / (1 + |(-x)|) = -(x / (1 + |x|))
Tactic: refine (strictMono_of_odd_strictMonoOn_nonneg ?_ ?_).codRestrict _
-- Lean 4 proof step from Mathlib.Order.Interval.Set.IsoIoo (goal)
Goal:
k : Type u_1
inst : Field k
inst_1 : LinearOrder k
inst_2 : IsStrictOrderedRing k
refine_2 : ∀ (x : k), -x / (1 + |(-x)|) = -(x / (1 + |x|))
⊢ StrictMono.{u_1, u_1} (α := k) (β := (↑(Ioo (-1) 1) : Type u_1))
    (codRestrict (fun (x : k) ↦ x / (1 + |x|)) (Ioo (-1) 1) ⋯)
have refine_2₁ : StrictMonoOn (β := k) (fun (x : k) ↦ x / (1 + |x|)) (Ici 0)
Tactic: refine (strictMono_of_odd_strictMonoOn_nonneg ?_ ?_).codRestrict _
-- Lean 4 proof step from Mathlib.Order.Interval.Set.IsoIoo (goal)
Goal:
k : Type u_1
inst : Field k
inst_1 : LinearOrder k
inst_2 : IsStrictOrderedRing k
⊢ Function.RightInverse (α := k) (fun (x : (↑(Ioo (-1) 1) : Type u_1)) ↦ (↑x : k) / (1 - |(↑x : k)|))
    (codRestrict (fun (x : k) ↦ x / (1 + |x|)) (Ioo (-1) 1) ⋯)
have refine_3 : ∀ (x : (↑(Ioo (-1) 1) : Type u_1)),
  (↑(codRestrict (fun (x : k) ↦ x / (1 + |x|)) (Ioo (-1) 1) sorry
          ((fun (x : (↑(Ioo (-1) 1) : Type u_1)) ↦ (↑x : k) / (1 - |(↑x : k)|)) x)) :
      k) =
    (↑x : k)
Tactic: refine fun x ↦ Subtype.ext ?_
-- Lean 4 proof step from Mathlib.Order.Interval.Set.IsoIoo (hypothesis)
Goal:
k : Type u_1
inst : Field k
inst_1 : LinearOrder k
inst_2 : IsStrictOrderedRing k
x : (↑(Ioo (-1) 1) : Type u_1)
⊢ (↑(codRestrict (fun (x : k) ↦ x / (1 + |x|)) (Ioo (-1) 1) ⋯
          ((fun (x : (↑(Ioo (-1) 1) : Type u_1)) ↦ (↑x : k) / (1 - |(↑x : k)|)) x)) :
      k) =
    (↑x : k)
have this : 0 < 1 - |(↑x : k)|
Tactic: have : 0 < 1 - |(x : k)| := sub_pos.2 (abs_lt.2 x.2)
-- Lean 4 proof step from Mathlib.Order.Interval.Set.Limit (goal)
Goal:
J : Type u
inst : LinearOrder J
j : J
m : (↑(Ici j) : Type u)
hm : Order.IsSuccLimit m
b : J
⊢ ¬b ⋖ (↑m : J)
have simp : b < (↑m : J) → ∃ (x : J) (_ : b < x), x < (↑m : J)
Tactic: simp only [CovBy, not_lt, not_and, not_forall, not_le]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.Limit (goal)
Goal:
J : Type u
inst : LinearOrder J
j : J
m : (↑(Ici j) : Type u)
hm : Order.IsSuccLimit m
b : J
hb : b < (↑m : J)
⊢ ∃ (x : J) (_ : b < x), x < (↑m : J)
have pos : ∀ (hb' : j ≤ b), ∃ (x : J) (_ : b < x), x < (↑m : J)
Tactic: by_cases hb' : j ≤ b
-- Lean 4 proof step from Mathlib.Order.Interval.Set.Limit (goal)
Goal:
J : Type u
inst : LinearOrder J
j : J
m : (↑(Ici j) : Type u)
hm : Order.IsSuccLimit m
b : J
hb : b < (↑m : J)
pos : ∀ (hb' : j ≤ b), ∃ (x : J) (_ : b < x), x < (↑m : J)
⊢ ∃ (x : J) (_ : b < x), x < (↑m : J)
have neg : ∀ (hb' : ¬j ≤ b), ∃ (x : J) (_ : b < x), x < (↑m : J)
Tactic: by_cases hb' : j ≤ b
-- Lean 4 proof step from Mathlib.Order.Interval.Set.Limit (hypothesis)
Goal:
J : Type u
inst : LinearOrder J
j : J
m : (↑(Ici j) : Type u)
hm : Order.IsSuccLimit m
b : J
hb : b < (↑m : J)
hb' : j ≤ b
⊢ ∃ (x : J) (_ : b < x), x < (↑m : J)
have this : ¬Subtype.mk (p := fun (x : J) ↦ x ∈ Ici j) b hb' ⋖ m
Tactic: have := hm.2 ⟨b, hb'⟩
-- Lean 4 proof step from Mathlib.Order.Interval.Set.Limit (hypothesis)
Goal:
J : Type u
inst : LinearOrder J
j : J
m : (↑(Ici j) : Type u)
hm : Order.IsSuccLimit m
b : J
hb : b < (↑m : J)
hb' : j ≤ b
this : ¬Subtype.mk (p := fun (x : J) ↦ x ∈ Ici j) b hb' ⋖ m
⊢ ∃ (x : J) (_ : b < x), x < (↑m : J)
have this₁ : ∃ (c : (↑(Ici j) : Type u)), Subtype.mk (p := fun (x : J) ↦ x ∈ Ici j) b hb' < c ∧ c < m
Tactic: rw [not_covBy_iff (by exact hb)] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Order.Interval.Set.Limit (goal)
Goal:
J : Type u
inst : LinearOrder J
j : J
m : (↑(Ici j) : Type u)
hm : Order.IsSuccLimit m
b : J
hb : b < (↑m : J)
hb' : j ≤ b
this : ∃ (c : (↑(Ici j) : Type u)), Subtype.mk (p := fun (x : J) ↦ x ∈ Ici j) b hb' < c ∧ c < m
⊢ ∃ (x : J) (_ : b < x), x < (↑m : J)
have pos : ∀ (x : J) (h₁ : x ∈ Ici j)
  (h₂ : Subtype.mk (p := fun (x : J) ↦ x ∈ Ici j) b hb' < Subtype.mk (p := fun (x : J) ↦ x ∈ Ici j) x h₁)
  (h₃ : Subtype.mk (p := fun (x : J) ↦ x ∈ Ici j) x h₁ < m), ∃ (x : J) (_ : b < x), x < (↑m : J)
Tactic: obtain ⟨⟨x, h₁⟩, h₂, h₃⟩ := this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Order.Interval.Set.Limit (hypothesis)
Goal:
J : Type u
inst : LinearOrder J
j : J
m : (↑(Ici j) : Type u)
hm : Order.IsSuccLimit m
b : J
hb : b < (↑m : J)
hb' : ¬j ≤ b
⊢ ∃ (x : J) (_ : b < x), x < (↑m : J)
have hb'₁ : b < j
Tactic: simp only [not_le] at hb'
Cleared hypotheses: hb'
-- Lean 4 proof step from Mathlib.Order.Interval.Set.Limit (goal)
Goal:
J : Type u
inst : LinearOrder J
j : J
m : (↑(Ici j) : Type u)
hm : Order.IsSuccLimit m
b : J
hb : b < (↑m : J)
hb' : b < j
⊢ ∃ (x : J) (_ : b < x), x < (↑m : J)
have neg : j < (↑m : J)
Tactic: refine ⟨j, hb', ?_⟩
-- Lean 4 proof step from Mathlib.Order.Interval.Set.Limit (goal)
Goal:
J : Type u
inst : LinearOrder J
j : J
m : (↑(Ici j) : Type u)
hm : Order.IsSuccLimit m
b : J
hb : b < (↑m : J)
hb' : b < j
⊢ j < (↑m : J)
have neg : ∀ (this : (↑m : J) ≤ j), False
Tactic: by_contra!
-- Lean 4 proof step from Mathlib.Order.Interval.Set.Limit (goal)
Goal:
J : Type u
inst : LinearOrder J
j : J
m : (↑(Ici j) : Type u)
hm : Order.IsSuccLimit m
b : J
hb : b < (↑m : J)
hb' : b < j
this : (↑m : J) ≤ j
⊢ False
have neg : IsMin m
Tactic: apply hm.1
-- Lean 4 proof step from Mathlib.Order.Interval.Set.LinearOrder (goal)
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
⊢ Ici a \ Ici b = Ico a b
have rw : Ici a ∩ (Ici b)ᶜ = Ico a b
Tactic: rw [diff_eq, compl_Ici, Ici_inter_Iio]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.LinearOrder (goal)
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
rw : Ici a ∩ (Ici b)ᶜ = Ico a b
⊢ Ici a \ Ici b = Ico a b
have rw₁ : Ici a ∩ Iio b = Ico a b
Tactic: rw [diff_eq, compl_Ici, Ici_inter_Iio]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.LinearOrder (goal)
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
rw : Ici a ∩ (Ici b)ᶜ = Ico a b
rw₁ : Ici a ∩ Iio b = Ico a b
⊢ Ici a \ Ici b = Ico a b
have rw₂ : Ico a b = Ico a b
Tactic: rw [diff_eq, compl_Ici, Ici_inter_Iio]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.LinearOrder (goal)
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
⊢ Ici a \ Ioi b = Icc a b
have rw : Ici a ∩ (Ioi b)ᶜ = Icc a b
Tactic: rw [diff_eq, compl_Ioi, Ici_inter_Iic]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.LinearOrder (goal)
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
rw : Ici a ∩ (Ioi b)ᶜ = Icc a b
⊢ Ici a \ Ioi b = Icc a b
have rw₁ : Ici a ∩ Iic b = Icc a b
Tactic: rw [diff_eq, compl_Ioi, Ici_inter_Iic]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.LinearOrder (goal)
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
rw : Ici a ∩ (Ioi b)ᶜ = Icc a b
rw₁ : Ici a ∩ Iic b = Icc a b
⊢ Ici a \ Ioi b = Icc a b
have rw₂ : Icc a b = Icc a b
Tactic: rw [diff_eq, compl_Ioi, Ici_inter_Iic]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.LinearOrder (goal)
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
⊢ Ioi a \ Ioi b = Ioc a b
have rw : Ioi a ∩ (Ioi b)ᶜ = Ioc a b
Tactic: rw [diff_eq, compl_Ioi, Ioi_inter_Iic]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.LinearOrder (goal)
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
rw : Ioi a ∩ (Ioi b)ᶜ = Ioc a b
⊢ Ioi a \ Ioi b = Ioc a b
have rw₁ : Ioi a ∩ Iic b = Ioc a b
Tactic: rw [diff_eq, compl_Ioi, Ioi_inter_Iic]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.LinearOrder (goal)
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
rw : Ioi a ∩ (Ioi b)ᶜ = Ioc a b
rw₁ : Ioi a ∩ Iic b = Ioc a b
⊢ Ioi a \ Ioi b = Ioc a b
have rw₂ : Ioc a b = Ioc a b
Tactic: rw [diff_eq, compl_Ioi, Ioi_inter_Iic]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.LinearOrder (goal)
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
⊢ Ioi a \ Ici b = Ioo a b
have rw : Ioi a ∩ (Ici b)ᶜ = Ioo a b
Tactic: rw [diff_eq, compl_Ici, Ioi_inter_Iio]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.LinearOrder (goal)
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
rw : Ioi a ∩ (Ici b)ᶜ = Ioo a b
⊢ Ioi a \ Ici b = Ioo a b
have rw₁ : Ioi a ∩ Iio b = Ioo a b
Tactic: rw [diff_eq, compl_Ici, Ioi_inter_Iio]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.LinearOrder (goal)
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
rw : Ioi a ∩ (Ici b)ᶜ = Ioo a b
rw₁ : Ioi a ∩ Iio b = Ioo a b
⊢ Ioi a \ Ici b = Ioo a b
have rw₂ : Ioo a b = Ioo a b
Tactic: rw [diff_eq, compl_Ici, Ioi_inter_Iio]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.LinearOrder (goal)
Goal:
α : Type u_1
inst : LinearOrder α
a₁ a₂ b₁ b₂ : α
h₁ : a₁ < b₁
⊢ Ioc a₁ b₁ ⊆ Ioc a₂ b₂ ↔ b₁ ≤ b₂ ∧ a₂ ≤ a₁
have h : Set α = Set αᵒᵈ → Ioc a₁ b₁ = Ico b₁ a₁
Tactic: convert! @Ico_subset_Ico_iff αᵒᵈ _ b₁ b₂ a₁ a₂ h₁ using 2
-- Lean 4 proof step from Mathlib.Order.Interval.Set.LinearOrder (goal)
Goal:
α : Type u_1
inst : LinearOrder α
a₁ a₂ b₁ b₂ : α
h₁ : a₁ < b₁
h : Set α = Set αᵒᵈ → Ioc a₁ b₁ = Ico b₁ a₁
⊢ Ioc a₁ b₁ ⊆ Ioc a₂ b₂ ↔ b₁ ≤ b₂ ∧ a₂ ≤ a₁
have h₂ : Set α = Set αᵒᵈ → Ioc a₂ b₂ = Ico b₂ a₂
Tactic: convert! @Ico_subset_Ico_iff αᵒᵈ _ b₁ b₂ a₁ a₂ h₁ using 2
-- Lean 4 proof step from Mathlib.Order.Interval.Set.LinearOrder (goal)
Goal:
α : Type u_1
inst : LinearOrder α
a b c d : α
h : a < b ∨ c < d
⊢ Ico a b = Ico c d ↔ a = c ∧ b = d
have refine : ∀ (h : Ico a b = Ico c d), a = c ∧ b = d
Tactic: refine ⟨fun h ↦ ?_, by grind⟩
-- Lean 4 proof step from Mathlib.Order.Interval.Set.LinearOrder (hypothesis)
Goal:
α : Type u_1
inst : LinearOrder α
a b c d : α
h_1 : a < b ∨ c < d
h : Ico a b = Ico c d
⊢ a = c ∧ b = d
have this : c ≤ a ∧ b ≤ d
Tactic: have : c ≤ a ∧ b ≤ d := (Ico_subset_Ico_iff (show a < b by grind [Set.nonempty_Ico])).1 h.subset
-- Lean 4 proof step from Mathlib.Order.Interval.Set.LinearOrder (hypothesis)
Goal:
α : Type u_1
inst : LinearOrder α
a b c d : α
h_1 : a < b ∨ c < d
h : Ico a b = Ico c d
this : c ≤ a ∧ b ≤ d
⊢ a = c ∧ b = d
have this₁ : a ≤ c ∧ d ≤ b
Tactic: have : a ≤ c ∧ d ≤ b := (Ico_subset_Ico_iff (show c < d by grind)).1 h.superset
-- Lean 4 proof step from Mathlib.Order.Interval.Set.LinearOrder (goal)
Goal:
α : Type u_1
inst : LinearOrder α
a b c d : α
hab : a < b ∨ c < d
⊢ Ioc a b = Ioc c d ↔ a = c ∧ b = d
have refine : ∀ (h : Ioc a b = Ioc c d), a = c ∧ b = d
Tactic: refine ⟨fun h ↦ ?_, by grind⟩
-- Lean 4 proof step from Mathlib.Order.Interval.Set.LinearOrder (hypothesis)
Goal:
α : Type u_1
inst : LinearOrder α
a b c d : α
hab : a < b ∨ c < d
h : Ioc a b = Ioc c d
⊢ a = c ∧ b = d
have this : b ≤ d ∧ c ≤ a
Tactic: have : b ≤ d ∧ c ≤ a := (Ioc_subset_Ioc_iff (show a < b by grind [Set.nonempty_Ioc])).1 h.subset
-- Lean 4 proof step from Mathlib.Order.Interval.Set.LinearOrder (hypothesis)
Goal:
α : Type u_1
inst : LinearOrder α
a b c d : α
hab : a < b ∨ c < d
h : Ioc a b = Ioc c d
this : b ≤ d ∧ c ≤ a
⊢ a = c ∧ b = d
have this₁ : d ≤ b ∧ a ≤ c
Tactic: have : d ≤ b ∧ a ≤ c := (Ioc_subset_Ioc_iff (show c < d by grind)).1 h.superset
-- Lean 4 proof step from Mathlib.Order.Interval.Set.LinearOrder (goal)
Goal:
α : Type u_1
inst : LinearOrder α
a₁ a₂ b₁ b₂ : α
inst_1 : DenselyOrdered α
h₁ : a₁ < b₁
h : Ioo a₁ b₁ ⊆ Ioo a₂ b₂
⊢ a₂ ≤ a₁ ∧ b₁ ≤ b₂
have rcases : ∀ (x : α) (xa : a₁ < x) (xb : x < b₁), a₂ ≤ a₁ ∧ b₁ ≤ b₂
Tactic: rcases exists_between h₁ with ⟨x, xa, xb⟩
-- Lean 4 proof step from Mathlib.Order.Interval.Set.LinearOrder (goal)
Goal:
α : Type u_1
inst : LinearOrder α
a₁ a₂ b₁ b₂ : α
inst_1 : DenselyOrdered α
h₁ : a₁ < b₁
h : Ioo a₁ b₁ ⊆ Ioo a₂ b₂
x : α
xa : a₁ < x
xb : x < b₁
⊢ a₂ ≤ a₁ ∧ b₁ ≤ b₂
have left : a₂ ≤ a₁
Tactic: constructor
-- Lean 4 proof step from Mathlib.Order.Interval.Set.LinearOrder (goal)
Goal:
α : Type u_1
inst : LinearOrder α
a₁ a₂ b₁ b₂ : α
inst_1 : DenselyOrdered α
h₁ : a₁ < b₁
h : Ioo a₁ b₁ ⊆ Ioo a₂ b₂
x : α
xa : a₁ < x
xb : x < b₁
left : a₂ ≤ a₁
⊢ a₂ ≤ a₁ ∧ b₁ ≤ b₂
have right : b₁ ≤ b₂
Tactic: constructor
-- Lean 4 proof step from Mathlib.Order.Interval.Set.LinearOrder (goal)
Goal:
α : Type u_1
inst : LinearOrder α
a₁ a₂ b₁ b₂ : α
inst_1 : DenselyOrdered α
h₁ : a₁ < b₁
h : Ioo a₁ b₁ ⊆ Ioo a₂ b₂
x : α
xa : a₁ < x
xb : x < b₁
⊢ a₂ ≤ a₁
have left : ∀ (h' : a₁ < a₂), False
Tactic: refine le_of_not_gt fun h' => ?_
-- Lean 4 proof step from Mathlib.Order.Interval.Set.LinearOrder (goal)
Goal:
α : Type u_1
inst : LinearOrder α
a₁ a₂ b₁ b₂ : α
inst_1 : DenselyOrdered α
h₁ : a₁ < b₁
h : Ioo a₁ b₁ ⊆ Ioo a₂ b₂
x : α
xa : a₁ < x
xb : x < b₁
⊢ b₁ ≤ b₂
have right : ∀ (h' : b₂ < b₁), False
Tactic: refine le_of_not_gt fun h' => ?_
-- Lean 4 proof step from Mathlib.Order.Interval.Set.LinearOrder (hypothesis)
Goal:
α : Type u_1
inst : LinearOrder α
a₁ a₂ b₁ b₂ : α
inst_1 : DenselyOrdered α
h₁ : a₁ < b₁
h : Ioo a₁ b₁ ⊆ Ioo a₂ b₂
x : α
xa : a₁ < x
xb : x < b₁
h' : a₁ < a₂
⊢ False
have ab : a₂ < b₁
Tactic: have ab := (h ⟨xa, xb⟩).1.trans xb
-- Lean 4 proof step from Mathlib.Order.Interval.Set.LinearOrder (hypothesis)
Goal:
α : Type u_1
inst : LinearOrder α
a₁ a₂ b₁ b₂ : α
inst_1 : DenselyOrdered α
h₁ : a₁ < b₁
h : Ioo a₁ b₁ ⊆ Ioo a₂ b₂
x : α
xa : a₁ < x
xb : x < b₁
h' : b₂ < b₁
⊢ False
have ab : a₁ < b₂
Tactic: have ab := xa.trans (h ⟨xa, xb⟩).2
-- Lean 4 proof step from Mathlib.Order.Interval.Set.LinearOrder (goal)
Goal:
α : Type u_1
inst : LinearOrder α
x : α
h : IsTop x
⊢ Ici x = {x}
have h₁ : ∀ (y : α), y ∈ Ici x ↔ Membership.mem (γ := Set α) {x} y
Tactic: ext y
-- Lean 4 proof step from Mathlib.Order.Interval.Set.LinearOrder (goal)
Goal:
α : Type u_1
inst : LinearOrder α
x : α
⊢ Ici x = {x} ↔ IsTop x
have refine : ∀ (h : Ici x = {x}) (y : α), y ≤ x
Tactic: refine ⟨fun h y ↦ ?_, fun h ↦ by ext y; simp [(h y).ge_iff_eq]⟩
-- Lean 4 proof step from Mathlib.Order.Interval.Set.LinearOrder (goal)
Goal:
α : Type u_1
inst : LinearOrder α
x : α
h : Ici x = {x}
y : α
⊢ y ≤ x
have by_contra! : ∀ (H : x < y), False
Tactic: by_contra! H
-- Lean 4 proof step from Mathlib.Order.Interval.Set.LinearOrder (hypothesis)
Goal:
α : Type u_1
inst : LinearOrder α
x : α
h : Ici x = {x}
y : α
H : x < y
⊢ False
have this : y ∈ Ici x
Tactic: have : y ∈ Ici x := H.le
-- Lean 4 proof step from Mathlib.Order.Interval.Set.LinearOrder (hypothesis)
Goal:
α : Type u_1
inst : LinearOrder α
x : α
h : Ici x = {x}
y : α
H : x < y
this : y ∈ Ici x
⊢ False
have this₁ : y = x
Tactic: rw [h, mem_singleton_iff] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Order.Interval.Set.LinearOrder (goal)
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
⊢ Ioi b ⊆ Ioi a ↔ a ≤ b
have refine : ∀ (h : Ioi b ⊆ Ioi a), a ≤ b
Tactic: refine ⟨fun h => ?_, Ioi_subset_Ioi⟩
-- Lean 4 proof step from Mathlib.Order.Interval.Set.LinearOrder (goal)
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
h : Ioi b ⊆ Ioi a
⊢ a ≤ b
have by_contra : ∀ (ba : ¬a ≤ b), False
Tactic: by_contra ba
-- Lean 4 proof step from Mathlib.Order.Interval.Set.LinearOrder (goal)
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
⊢ Ioi b ⊂ Ioi a ↔ a < b
have refine : ∀ (h : Ioi b ⊂ Ioi a), a < b
Tactic: refine ⟨fun h => ?_, Ioi_ssubset_Ioi⟩
-- Lean 4 proof step from Mathlib.Order.Interval.Set.LinearOrder (goal)
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
h : Ioi b ⊂ Ioi a
⊢ a < b
have obtain : Ioi b ⊆ Ioi a → ∀ (c : α) (ac : c ∈ Ioi a) (cb : ¬c ∈ Ioi b), a < b
Tactic: obtain ⟨_, c, ac, cb⟩ := ssubset_iff_exists.mp h
-- Lean 4 proof step from Mathlib.Order.Interval.Set.LinearOrder (goal)
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
inst_1 : DenselyOrdered α
⊢ Ioi b ⊆ Ici a ↔ a ≤ b
have refine : ∀ (h : Ioi b ⊆ Ici a), a ≤ b
Tactic: refine ⟨fun h => ?_, Ioi_subset_Ici⟩
-- Lean 4 proof step from Mathlib.Order.Interval.Set.LinearOrder (goal)
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
inst_1 : DenselyOrdered α
h : Ioi b ⊆ Ici a
⊢ a ≤ b
have by_contra : ∀ (ba : ¬a ≤ b), False
Tactic: by_contra ba
-- Lean 4 proof step from Mathlib.Order.Interval.Set.LinearOrder (goal)
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
inst_1 : DenselyOrdered α
h : Ioi b ⊆ Ici a
ba : ¬a ≤ b
⊢ False
have obtain : ∀ (c : α) (bc : b < c) (ca : c < a), False
Tactic: obtain ⟨c, bc, ca⟩ : ∃ c, b < c ∧ c < a := exists_between (not_le.mp ba)
-- Lean 4 proof step from Mathlib.Order.Interval.Set.Monotone (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : SuccOrder α
inst_2 : IsSuccArchimedean α
inst_3 : OrderBot α
n : α
φ : α → α
hφ : StrictMonoOn φ (Iic n)
⊢ ∀ m ≤ n, m ≤ φ m
have revert : ∀ (hφ : StrictMonoOn φ (Iic n)), ∀ m ≤ n, m ≤ φ m
Tactic: revert hφ
Cleared hypotheses: hφ
-- Lean 4 proof step from Mathlib.Order.Interval.Set.Monotone (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : SuccOrder α
inst_2 : IsSuccArchimedean α
inst_3 : OrderBot α
n : α
φ : α → α
⊢ ∀ (hφ : StrictMonoOn φ (Iic n)), ∀ m ≤ n, m ≤ φ m
have n₁ : ∀ (a : α),
  (fun (n : α) ↦ StrictMonoOn φ (Iic n) → ∀ m ≤ n, m ≤ φ m) a →
    (fun (n : α) ↦ StrictMonoOn φ (Iic n) → ∀ m ≤ n, m ≤ φ m) (succ a)
Tactic: refine
    Succ.rec_bot (fun n => StrictMonoOn φ (Set.Iic n) → ∀ m ≤ n, m ≤ φ m)
      (fun _ _ hm => hm.trans bot_le) ?_ _
-- Lean 4 proof step from Mathlib.Order.Interval.Set.Monotone (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : SuccOrder α
inst_2 : IsSuccArchimedean α
inst_3 : OrderBot α
n : α
φ : α → α
k : α
ih : StrictMonoOn φ (Iic k) → ∀ m ≤ k, m ≤ φ m
hφ : StrictMonoOn φ (Iic (succ k))
m : α
hm : m ≤ succ k
⊢ m ≤ φ m
have pos : ∀ (hk : IsMax k), m ≤ φ m
Tactic: by_cases hk : IsMax k
-- Lean 4 proof step from Mathlib.Order.Interval.Set.Monotone (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : SuccOrder α
inst_2 : IsSuccArchimedean α
inst_3 : OrderBot α
n : α
φ : α → α
k : α
ih : StrictMonoOn φ (Iic k) → ∀ m ≤ k, m ≤ φ m
hφ : StrictMonoOn φ (Iic (succ k))
m : α
hm : m ≤ succ k
pos : ∀ (hk : IsMax k), m ≤ φ m
⊢ m ≤ φ m
have neg : ∀ (hk : ¬IsMax k), m ≤ φ m
Tactic: by_cases hk : IsMax k
-- Lean 4 proof step from Mathlib.Order.Interval.Set.Monotone (hypothesis)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : SuccOrder α
inst_2 : IsSuccArchimedean α
inst_3 : OrderBot α
n : α
φ : α → α
k : α
ih : StrictMonoOn φ (Iic k) → ∀ m ≤ k, m ≤ φ m
hφ : StrictMonoOn φ (Iic (succ k))
m : α
hm : m ≤ succ k
hk : IsMax k
⊢ m ≤ φ m
have hm₁ : m ≤ k
Tactic: rw [succ_eq_iff_isMax.2 hk] at hm
Cleared hypotheses: hm, hk
-- Lean 4 proof step from Mathlib.Order.Interval.Set.Monotone (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : SuccOrder α
inst_2 : IsSuccArchimedean α
inst_3 : OrderBot α
n : α
φ : α → α
k : α
ih : StrictMonoOn φ (Iic k) → ∀ m ≤ k, m ≤ φ m
hφ : StrictMonoOn φ (Iic (succ k))
m : α
hm : m ≤ succ k
hk : ¬IsMax k
⊢ m ≤ φ m
have neg : ∀ (hm : succ k ≤ succ k), succ k ≤ φ (succ k)
Tactic: obtain rfl | h := le_succ_iff_eq_or_le.1 hm
Cleared hypotheses: m, hm
-- Lean 4 proof step from Mathlib.Order.Interval.Set.Monotone (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : SuccOrder α
inst_2 : IsSuccArchimedean α
inst_3 : OrderBot α
n : α
φ : α → α
k : α
ih : StrictMonoOn φ (Iic k) → ∀ m ≤ k, m ≤ φ m
hφ : StrictMonoOn φ (Iic (succ k))
m : α
hm : m ≤ succ k
hk : ¬IsMax k
neg : ∀ (hm : succ k ≤ succ k), succ k ≤ φ (succ k)
⊢ m ≤ φ m
have neg₁ : ∀ (h : m ≤ k), m ≤ φ m
Tactic: obtain rfl | h := le_succ_iff_eq_or_le.1 hm
-- Lean 4 proof step from Mathlib.Order.Interval.Set.Monotone (hypothesis)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : SuccOrder α
inst_2 : IsSuccArchimedean α
inst_3 : OrderBot α
n : α
φ : α → α
k : α
ih : StrictMonoOn φ (Iic k) → ∀ m ≤ k, m ≤ φ m
hφ : StrictMonoOn φ (Iic (succ k))
hk : ¬IsMax k
hm : succ k ≤ succ k
⊢ succ k ≤ φ (succ k)
have ih₁ : k ≤ φ k
Tactic: specialize ih (StrictMonoOn.mono hφ fun x hx => le_trans hx (le_succ _)) k le_rfl
Cleared hypotheses: ih
-- Lean 4 proof step from Mathlib.Order.Interval.Set.Monotone (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : SuccOrder α
inst_2 : IsSuccArchimedean α
inst_3 : OrderBot α
n : α
φ : α → α
k : α
hφ : StrictMonoOn φ (Iic (succ k))
hk : ¬IsMax k
hm : succ k ≤ succ k
ih : k ≤ φ k
⊢ succ k ≤ φ (succ k)
have neg : succ (φ k) ≤ φ (succ k)
Tactic: nth_grw 1 [ih]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.Monotone (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : SuccOrder α
inst_2 : IsSuccArchimedean α
inst_3 : OrderBot α
n : α
φ : α → α
k : α
hφ : StrictMonoOn φ (Iic (succ k))
hk : ¬IsMax k
hm : succ k ≤ succ k
ih : k ≤ φ k
⊢ succ (φ k) ≤ φ (succ k)
have neg : k < succ k
Tactic: refine succ_le_of_lt (hφ (le_succ _) le_rfl ?_)
-- Lean 4 proof step from Mathlib.Order.Interval.Set.OrdConnected (goal)
Goal:
α : Type u_3
inst : PartialOrder α
s : Set α
hs : ∀ x ∈ s, ∀ y ∈ s, x < y → Ioo x y ⊆ s
⊢ s.OrdConnected
have rw : ∀ x ∈ s, ∀ y ∈ s, x ≤ y → Icc x y ⊆ s
Tactic: rw [ordConnected_iff]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.OrdConnected (goal)
Goal:
α : Type u_3
inst : PartialOrder α
s : Set α
hs : ∀ x ∈ s, ∀ y ∈ s, x < y → Ioo x y ⊆ s
x : α
hx : x ∈ s
y : α
hy : y ∈ s
hxy : x ≤ y
⊢ Icc x y ⊆ s
have inl : ∀ (hy : x ∈ s) (hxy : x ≤ x), Icc x x ⊆ s
Tactic: rcases eq_or_lt_of_le hxy with (rfl | hxy')
Cleared hypotheses: y, hy, hxy