awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Order.Interval.Set.Pi (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : DecidableEq ι
inst_1 : (i : ι) → LinearOrder (α i)
x y : (i : ι) → α i
i₀ : ι
m : α i₀
hm : m ∈ Icc (x i₀) (y i₀)
simp_rw :
  Eq (α := Set ((i : ι) → α i))
    ((pi (α := α) univ fun (i : ι) ↦ Ioc (x i) (update (β := α) y i₀ m i)) ∪
      {z : (i : ι) → α i | m < z i₀} ∩ pi (α := α) univ fun (i : ι) ↦ Ioc (x i) (y i))
    (pi (α := α) univ fun (i : ι) ↦ Ioc (x i) (y i))
simp_rw₁ :
  Eq (α := Set ((i : ι) → α i))
    (({z : (i : ι) → α i | z i₀ ≤ m} ∩ pi (α := α) univ fun (i : ι) ↦ Ioc (x i) (y i)) ∪
      {z : (i : ι) → α i | m < z i₀} ∩ pi (α := α) univ fun (i : ι) ↦ Ioc (x i) (y i))
    (pi (α := α) univ fun (i : ι) ↦ Ioc (x i) (y i))
simp_rw₂ :
  Eq (α := Set ((i : ι) → α i))
    (({z : (i : ι) → α i | z i₀ ≤ m} ∪ {z : (i : ι) → α i | m < z i₀}) ∩ pi (α := α) univ fun (i : ι) ↦ Ioc (x i) (y i))
    (pi (α := α) univ fun (i : ι) ↦ Ioc (x i) (y i))
simp_rw₃ :
  Eq (α := Set ((i : ι) → α i))
    ({a : (i : ι) → α i | a i₀ ≤ m ∨ m < a i₀} ∩ pi (α := α) univ fun (i : ι) ↦ Ioc (x i) (y i))
    (pi (α := α) univ fun (i : ι) ↦ Ioc (x i) (y i))
⊢ Eq (α := Set ((i : ι) → α i))
    ((pi (α := α) univ fun (i : ι) ↦ Ioc (x i) (update (β := α) y i₀ m i)) ∪
      pi (α := α) univ fun (i : ι) ↦ Ioc (update (β := α) x i₀ m i) (y i))
    (pi (α := α) univ fun (i : ι) ↦ Ioc (x i) (y i))
have simp_rw₄ : Eq (α := Set ((i : ι) → α i)) ({a : (i : ι) → α i | True} ∩ pi (α := α) univ fun (i : ι) ↦ Ioc (x i) (y i))
  (pi (α := α) univ fun (i : ι) ↦ Ioc (x i) (y i))
Tactic: simp_rw [pi_univ_Ioc_update_left hm.1, pi_univ_Ioc_update_right hm.2, ← union_inter_distrib_right,
    ← setOf_or, le_or_gt, setOf_true, univ_inter]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.Pi (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : DecidableEq ι
inst_1 : (i : ι) → LinearOrder (α i)
x y : (i : ι) → α i
i₀ : ι
m : α i₀
hm : m ∈ Icc (x i₀) (y i₀)
simp_rw :
  Eq (α := Set ((i : ι) → α i))
    ((pi (α := α) univ fun (i : ι) ↦ Ioc (x i) (update (β := α) y i₀ m i)) ∪
      {z : (i : ι) → α i | m < z i₀} ∩ pi (α := α) univ fun (i : ι) ↦ Ioc (x i) (y i))
    (pi (α := α) univ fun (i : ι) ↦ Ioc (x i) (y i))
simp_rw₁ :
  Eq (α := Set ((i : ι) → α i))
    (({z : (i : ι) → α i | z i₀ ≤ m} ∩ pi (α := α) univ fun (i : ι) ↦ Ioc (x i) (y i)) ∪
      {z : (i : ι) → α i | m < z i₀} ∩ pi (α := α) univ fun (i : ι) ↦ Ioc (x i) (y i))
    (pi (α := α) univ fun (i : ι) ↦ Ioc (x i) (y i))
simp_rw₂ :
  Eq (α := Set ((i : ι) → α i))
    (({z : (i : ι) → α i | z i₀ ≤ m} ∪ {z : (i : ι) → α i | m < z i₀}) ∩ pi (α := α) univ fun (i : ι) ↦ Ioc (x i) (y i))
    (pi (α := α) univ fun (i : ι) ↦ Ioc (x i) (y i))
simp_rw₃ :
  Eq (α := Set ((i : ι) → α i))
    ({a : (i : ι) → α i | a i₀ ≤ m ∨ m < a i₀} ∩ pi (α := α) univ fun (i : ι) ↦ Ioc (x i) (y i))
    (pi (α := α) univ fun (i : ι) ↦ Ioc (x i) (y i))
simp_rw₄ :
  Eq (α := Set ((i : ι) → α i)) ({a : (i : ι) → α i | True} ∩ pi (α := α) univ fun (i : ι) ↦ Ioc (x i) (y i))
    (pi (α := α) univ fun (i : ι) ↦ Ioc (x i) (y i))
⊢ Eq (α := Set ((i : ι) → α i))
    ((pi (α := α) univ fun (i : ι) ↦ Ioc (x i) (update (β := α) y i₀ m i)) ∪
      pi (α := α) univ fun (i : ι) ↦ Ioc (update (β := α) x i₀ m i) (y i))
    (pi (α := α) univ fun (i : ι) ↦ Ioc (x i) (y i))
have simp_rw₅ : Eq (α := Set ((i : ι) → α i)) (univ ∩ pi (α := α) univ fun (i : ι) ↦ Ioc (x i) (y i))
  (pi (α := α) univ fun (i : ι) ↦ Ioc (x i) (y i))
Tactic: simp_rw [pi_univ_Ioc_update_left hm.1, pi_univ_Ioc_update_right hm.2, ← union_inter_distrib_right,
    ← setOf_or, le_or_gt, setOf_true, univ_inter]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.Pi (hypothesis)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : DecidableEq ι
inst_1 : (i : ι) → LinearOrder (α i)
x y x' y' a : (i : ι) → α i
ha' : a ∉ pi (α := α) univ fun (i : ι) ↦ Ioo (x' i) (y' i)
hxa : x ≤ a
hay : a ≤ y
⊢ Membership.mem (γ := Set ((i : ι) → α i))
    ((⋃ (i : ι), Icc x (update (β := α) y i (x' i))) ∪ ⋃ (i : ι), Icc (update (β := α) x i (y' i)) y) a
have ha'₁ : ∃ (x : ι), ¬(x' x < a x ∧ a x < y' x)
Tactic: simp only [mem_pi, mem_univ, mem_Ioo, true_implies, not_forall] at ha'
Cleared hypotheses: ha'
-- Lean 4 proof step from Mathlib.Order.Interval.Set.Pi (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : DecidableEq ι
inst_1 : (i : ι) → LinearOrder (α i)
x y x' y' a : (i : ι) → α i
hxa : x ≤ a
hay : a ≤ y
ha' : ∃ (x : ι), ¬(x' x < a x ∧ a x < y' x)
⊢ Membership.mem (γ := Set ((i : ι) → α i))
    ((⋃ (i : ι), Icc x (update (β := α) y i (x' i))) ∪ ⋃ (i : ι), Icc (update (β := α) x i (y' i)) y) a
have simp : ∃ (x : ι), (True ∧ a x ≤ x' x ∧ ∀ (j : ι), j ≠ x → True) ∨ (y' x ≤ a x ∧ ∀ (j : ι), j ≠ x → True) ∧ True
Tactic: simp only [le_update_iff, update_le_iff, mem_union, mem_iUnion, mem_Icc,
    hxa, hay _, hxa _, hay, ← exists_or]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.Pi (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : DecidableEq ι
inst_1 : (i : ι) → LinearOrder (α i)
x y x' y' a : (i : ι) → α i
hxa : x ≤ a
hay : a ≤ y
ha' : ∃ (x : ι), ¬(x' x < a x ∧ a x < y' x)
⊢ ∃ (x : ι), (True ∧ a x ≤ x' x ∧ ∀ (j : ι), j ≠ x → True) ∨ (y' x ≤ a x ∧ ∀ (j : ι), j ≠ x → True) ∧ True
have rcases : ∀ (w : ι) (hw : ¬(x' w < a w ∧ a w < y' w)),
  ∃ (x : ι), (True ∧ a x ≤ x' x ∧ ∀ (j : ι), j ≠ x → True) ∨ (y' x ≤ a x ∧ ∀ (j : ι), j ≠ x → True) ∧ True
Tactic: rcases ha' with ⟨w, hw⟩
Cleared hypotheses: ha'
-- Lean 4 proof step from Mathlib.Order.Interval.Set.Pi (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : DecidableEq ι
inst_1 : (i : ι) → LinearOrder (α i)
x y x' y' a : (i : ι) → α i
hxa : x ≤ a
hay : a ≤ y
w : ι
hw : ¬(x' w < a w ∧ a w < y' w)
⊢ ∃ (x : ι), (True ∧ a x ≤ x' x ∧ ∀ (j : ι), j ≠ x → True) ∨ (y' x ≤ a x ∧ ∀ (j : ι), j ≠ x → True) ∧ True
have apply : (True ∧ a w ≤ x' w ∧ ∀ (j : ι), j ≠ w → True) ∨ (y' w ≤ a w ∧ ∀ (j : ι), j ≠ w → True) ∧ True
Tactic: apply Exists.intro w
-- Lean 4 proof step from Mathlib.Order.Interval.Set.Pi (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : DecidableEq ι
inst_1 : (i : ι) → LinearOrder (α i)
x y x' y' a : (i : ι) → α i
hxa : x ≤ a
hay : a ≤ y
w : ι
hw : ¬(x' w < a w ∧ a w < y' w)
⊢ (True ∧ a w ≤ x' w ∧ ∀ (j : ι), j ≠ w → True) ∨ (y' w ≤ a w ∧ ∀ (j : ι), j ≠ w → True) ∧ True
have inl : x' w < a w → (True ∧ a w ≤ x' w ∧ ∀ (j : ι), j ≠ w → True) ∨ (y' w ≤ a w ∧ ∀ (j : ι), j ≠ w → True) ∧ True
Tactic: cases lt_or_ge (x' w) (a w)
-- Lean 4 proof step from Mathlib.Order.Interval.Set.Pi (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : DecidableEq ι
inst_1 : (i : ι) → LinearOrder (α i)
x y x' y' a : (i : ι) → α i
hxa : x ≤ a
hay : a ≤ y
w : ι
hw : ¬(x' w < a w ∧ a w < y' w)
inl : x' w < a w → (True ∧ a w ≤ x' w ∧ ∀ (j : ι), j ≠ w → True) ∨ (y' w ≤ a w ∧ ∀ (j : ι), j ≠ w → True) ∧ True
⊢ (True ∧ a w ≤ x' w ∧ ∀ (j : ι), j ≠ w → True) ∨ (y' w ≤ a w ∧ ∀ (j : ι), j ≠ w → True) ∧ True
have inr : a w ≤ x' w → (True ∧ a w ≤ x' w ∧ ∀ (j : ι), j ≠ w → True) ∨ (y' w ≤ a w ∧ ∀ (j : ι), j ≠ w → True) ∧ True
Tactic: cases lt_or_ge (x' w) (a w)
-- Lean 4 proof step from Mathlib.Order.Interval.Set.ProjIcc (goal)
Goal:
α : Type u_1
inst : LinearOrder α
a : α
x : (↑(Ici a) : Type u_1)
⊢ projIci a (↑x : α) = x
have mk : ∀ (val : α) (property : val ∈ Ici a),
  projIci a (↑(Subtype.mk (p := fun (x : α) ↦ x ∈ Ici a) val property) : α) =
    Subtype.mk (p := fun (x : α) ↦ x ∈ Ici a) val property
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Order.Interval.Set.ProjIcc (goal)
Goal:
α : Type u_1
inst : LinearOrder α
b : α
x : (↑(Iic b) : Type u_1)
⊢ projIic b (↑x : α) = x
have mk : ∀ (val : α) (property : val ∈ Iic b),
  projIic b (↑(Subtype.mk (p := fun (x : α) ↦ x ∈ Iic b) val property) : α) =
    Subtype.mk (p := fun (x : α) ↦ x ∈ Iic b) val property
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Order.Interval.Set.ProjIcc (goal)
Goal:
α : Type u_1
inst : LinearOrder α
a b : α
h : a ≤ b
x : (↑(Icc a b) : Type u_1)
⊢ projIcc a b h (↑x : α) = x
have mk : ∀ (val : α) (property : val ∈ Icc a b),
  projIcc a b h (↑(Subtype.mk (p := fun (x : α) ↦ x ∈ Icc a b) val property) : α) =
    Subtype.mk (p := fun (x : α) ↦ x ∈ Icc a b) val property
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Order.Interval.Set.ProjIcc (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
a b : α
h : a ≤ b
f : α → β
ha : ∀ x < a, f x = f a
hb : ∀ (x : α), b < x → f x = f b
⊢ IccExtend h (f ∘ Subtype.val (p := fun (x : α) ↦ x ∈ Icc a b)) = f
have h₁ : ∀ (x : α), IccExtend h (f ∘ Subtype.val (p := fun (x : α) ↦ x ∈ Icc a b)) x = f x
Tactic: ext x
-- Lean 4 proof step from Mathlib.Order.Interval.Set.ProjIcc (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
a b : α
h : a ≤ b
f : α → β
ha : ∀ x < a, f x = f a
hb : ∀ (x : α), b < x → f x = f b
x : α
⊢ IccExtend h (f ∘ Subtype.val (p := fun (x : α) ↦ x ∈ Icc a b)) x = f x
have h₁ : ∀ (hxa : x < a), IccExtend h (f ∘ Subtype.val (p := fun (x : α) ↦ x ∈ Icc a b)) x = f x
Tactic: rcases lt_or_ge x a with hxa | hax
-- Lean 4 proof step from Mathlib.Order.Interval.Set.ProjIcc (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
a b : α
h : a ≤ b
f : α → β
ha : ∀ x < a, f x = f a
hb : ∀ (x : α), b < x → f x = f b
x : α
h₁ : ∀ (hxa : x < a), IccExtend h (f ∘ Subtype.val (p := fun (x : α) ↦ x ∈ Icc a b)) x = f x
⊢ IccExtend h (f ∘ Subtype.val (p := fun (x : α) ↦ x ∈ Icc a b)) x = f x
have h₂ : ∀ (hax : a ≤ x), IccExtend h (f ∘ Subtype.val (p := fun (x : α) ↦ x ∈ Icc a b)) x = f x
Tactic: rcases lt_or_ge x a with hxa | hax
-- Lean 4 proof step from Mathlib.Order.Interval.Set.ProjIcc (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
a b : α
h : a ≤ b
f : α → β
ha : ∀ x < a, f x = f a
hb : ∀ (x : α), b < x → f x = f b
x : α
hax : a ≤ x
⊢ IccExtend h (f ∘ Subtype.val (p := fun (x : α) ↦ x ∈ Icc a b)) x = f x
have h₁ : ∀ (hxb : x ≤ b), IccExtend h (f ∘ Subtype.val (p := fun (x : α) ↦ x ∈ Icc a b)) x = f x
Tactic: rcases le_or_gt x b with hxb | hbx
-- Lean 4 proof step from Mathlib.Order.Interval.Set.ProjIcc (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
a b : α
h : a ≤ b
f : α → β
ha : ∀ x < a, f x = f a
hb : ∀ (x : α), b < x → f x = f b
x : α
hax : a ≤ x
h₁ : ∀ (hxb : x ≤ b), IccExtend h (f ∘ Subtype.val (p := fun (x : α) ↦ x ∈ Icc a b)) x = f x
⊢ IccExtend h (f ∘ Subtype.val (p := fun (x : α) ↦ x ∈ Icc a b)) x = f x
have h₂ : ∀ (hbx : b < x), IccExtend h (f ∘ Subtype.val (p := fun (x : α) ↦ x ∈ Icc a b)) x = f x
Tactic: rcases le_or_gt x b with hxb | hbx
-- Lean 4 proof step from Mathlib.Order.Interval.Set.ProjIcc (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
a b : α
h : a ≤ b
f : α → β
ha : ∀ x < a, f x = f a
hb : ∀ (x : α), b < x → f x = f b
x : α
hax : a ≤ x
hxb : x ≤ b
⊢ IccExtend h (f ∘ Subtype.val (p := fun (x : α) ↦ x ∈ Icc a b)) x = f x
have h₁ : ∀ (x : { x : α // x ∈ Icc a b }) (hax : a ≤ (↑x : α)) (hxb : (↑x : α) ≤ b),
  IccExtend h (f ∘ Subtype.val (p := fun (x : α) ↦ x ∈ Icc a b)) (↑x : α) = f (↑x : α)
Tactic: lift x to Icc a b using ⟨hax, hxb⟩
Cleared hypotheses: x, hax, hxb
-- Lean 4 proof step from Mathlib.Order.Interval.Set.ProjIcc (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
a b : α
h : a ≤ b
f : α → β
ha : ∀ x < a, f x = f a
hb : ∀ (x : α), b < x → f x = f b
x : { x : α // x ∈ Icc a b }
hax : a ≤ (↑x : α)
hxb : (↑x : α) ≤ b
⊢ IccExtend h (f ∘ Subtype.val (p := fun (x : α) ↦ x ∈ Icc a b)) (↑x : α) = f (↑x : α)
have h₁ : (f ∘ Subtype.val (p := fun (x : α) ↦ x ∈ Icc a b)) x = f (↑x : α)
Tactic: rw [IccExtend_val, comp_apply]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.ProjIcc (goal)
Goal:
α : Type u_1
β : Type u_2
inst : LinearOrder α
a b : α
h : a ≤ b
f : α → β
ha : ∀ x < a, f x = f a
hb : ∀ (x : α), b < x → f x = f b
x : { x : α // x ∈ Icc a b }
hax : a ≤ (↑x : α)
hxb : (↑x : α) ≤ b
h₁ : (f ∘ Subtype.val (p := fun (x : α) ↦ x ∈ Icc a b)) x = f (↑x : α)
⊢ IccExtend h (f ∘ Subtype.val (p := fun (x : α) ↦ x ∈ Icc a b)) (↑x : α) = f (↑x : α)
have h₂ : f (↑x : α) = f (↑x : α)
Tactic: rw [IccExtend_val, comp_apply]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.SuccOrder (goal)
Goal:
J : Type u_1
inst : PartialOrder J
inst_1 : SuccOrder J
j : J
i : (↑(Iic j) : Type u_1)
hi : ¬IsMax i
⊢ (↑(Order.succ i) : J) = Order.succ (↑i : J)
have rw : Order.succ (↑i : J) ∈ Iic j
Tactic: rw [coe_succ_of_mem]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.SuccOrder (goal)
Goal:
J : Type u_1
inst : PartialOrder J
inst_1 : SuccOrder J
j : J
i : (↑(Iic j) : Type u_1)
hi : ¬IsMax i
⊢ Order.succ (↑i : J) ∈ Iic j
have a : (↑i : J) < j
Tactic: apply Order.succ_le_of_lt
-- Lean 4 proof step from Mathlib.Order.Interval.Set.SuccOrder (goal)
Goal:
J : Type u_1
inst : PartialOrder J
inst_1 : SuccOrder J
j : J
i : (↑(Iic j) : Type u_1)
hi : ¬IsMax i
⊢ Order.succ (↑i : J) ∈ Iic j
have rw : (↑(Order.succ i) : J) ∈ Iic j
Tactic: rw [← coe_succ_of_not_isMax hi]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.SuccOrder (goal)
Goal:
J : Type u_1
inst : PartialOrder J
inst_1 : SuccOrder J
j : J
i : (↑(Iic j) : Type u_1)
hi : ¬IsMax i
⊢ Order.succ i = Subtype.mk (p := fun (x : J) ↦ x ∈ Iic j) (Order.succ (↑i : J)) ⋯
have a : (↑(Order.succ i) : J) = (↑(Subtype.mk (p := fun (x : J) ↦ x ∈ Iic j) (Order.succ (↑i : J)) sorry) : J)
Tactic: ext
-- Lean 4 proof step from Mathlib.Order.Interval.Set.SuccOrder (goal)
Goal:
J : Type u_1
inst : PartialOrder J
inst_1 : PredOrder J
j : J
i : (↑(Ici j) : Type u_1)
hi : ¬IsMin i
⊢ (↑(Order.pred i) : J) = Order.pred (↑i : J)
have rw : Order.pred (↑i : J) ∈ Ici j
Tactic: rw [coe_pred_of_mem]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.SuccOrder (goal)
Goal:
J : Type u_1
inst : PartialOrder J
inst_1 : PredOrder J
j : J
i : (↑(Ici j) : Type u_1)
hi : ¬IsMin i
⊢ Order.pred (↑i : J) ∈ Ici j
have a : j < (↑i : J)
Tactic: apply Order.le_pred_of_lt
-- Lean 4 proof step from Mathlib.Order.Interval.Set.SuccOrder (goal)
Goal:
J : Type u_1
inst : PartialOrder J
inst_1 : PredOrder J
j : J
i : (↑(Ici j) : Type u_1)
hi : ¬IsMin i
⊢ Order.pred (↑i : J) ∈ Ici j
have rw : (↑(Order.pred i) : J) ∈ Ici j
Tactic: rw [← coe_pred_of_not_isMin hi]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.SuccOrder (goal)
Goal:
J : Type u_1
inst : PartialOrder J
inst_1 : PredOrder J
j : J
i : (↑(Ici j) : Type u_1)
hi : ¬IsMin i
⊢ Order.pred i = Subtype.mk (p := fun (x : J) ↦ x ∈ Ici j) (Order.pred (↑i : J)) ⋯
have a : (↑(Order.pred i) : J) = (↑(Subtype.mk (p := fun (x : J) ↦ x ∈ Ici j) (Order.pred (↑i : J)) sorry) : J)
Tactic: ext
-- Lean 4 proof step from Mathlib.Order.Interval.Set.SuccPred (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : SuccOrder α
a b : α
⊢ Ico (succ a) b = Ioo a b
have pos : ∀ (ha : IsMax a), Ico (succ a) b = Ioo a b
Tactic: by_cases ha : IsMax a
-- Lean 4 proof step from Mathlib.Order.Interval.Set.SuccPred (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : SuccOrder α
a b : α
pos : ∀ (ha : IsMax a), Ico (succ a) b = Ioo a b
⊢ Ico (succ a) b = Ioo a b
have neg : ∀ (ha : ¬IsMax a), Ico (succ a) b = Ioo a b
Tactic: by_cases ha : IsMax a
-- Lean 4 proof step from Mathlib.Order.Interval.Set.SuccPred (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : SuccOrder α
a b : α
ha : IsMax a
⊢ Ico (succ a) b = Ioo a b
have pos : ∅ = Ioo a b
Tactic: rw [Ico_eq_empty (ha.mono <| le_succ _).not_lt, Ioo_eq_empty ha.not_lt]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.SuccPred (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : SuccOrder α
a b : α
ha : IsMax a
pos : ∅ = Ioo a b
⊢ Ico (succ a) b = Ioo a b
have pos₁ : Eq.{u_1 + 1} (α := Set α) ∅ ∅
Tactic: rw [Ico_eq_empty (ha.mono <| le_succ _).not_lt, Ioo_eq_empty ha.not_lt]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.SuccPred (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : SuccOrder α
a b : α
ha : ¬IsMax a
⊢ Ico (succ a) b = Ioo a b
have neg : ∀ (x : α), x ∈ Ico (succ a) b ↔ x ∈ Ioo a b
Tactic: ext x
-- Lean 4 proof step from Mathlib.Order.Interval.Set.SuccPred (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : SuccOrder α
a b : α
ha : ¬IsMax a
x : α
⊢ x ∈ Ico (succ a) b ↔ x ∈ Ioo a b
have neg : succ a ≤ x ∧ x < b ↔ x ∈ Ioo a b
Tactic: rw [mem_Ico, mem_Ioo, succ_le_iff_of_not_isMax ha]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.SuccPred (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : SuccOrder α
a b : α
ha : ¬IsMax a
x : α
neg : succ a ≤ x ∧ x < b ↔ x ∈ Ioo a b
⊢ x ∈ Ico (succ a) b ↔ x ∈ Ioo a b
have neg₁ : succ a ≤ x ∧ x < b ↔ a < x ∧ x < b
Tactic: rw [mem_Ico, mem_Ioo, succ_le_iff_of_not_isMax ha]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.SuccPred (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : SuccOrder α
a b : α
ha : ¬IsMax a
x : α
neg : succ a ≤ x ∧ x < b ↔ x ∈ Ioo a b
neg₁ : succ a ≤ x ∧ x < b ↔ a < x ∧ x < b
⊢ x ∈ Ico (succ a) b ↔ x ∈ Ioo a b
have neg₂ : a < x ∧ x < b ↔ a < x ∧ x < b
Tactic: rw [mem_Ico, mem_Ioo, succ_le_iff_of_not_isMax ha]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.SuccPred (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : SuccOrder α
a : α
ha : ¬IsMax a
b : α
⊢ Icc (succ a) b = Ioc a b
have h : ∀ (x : α), x ∈ Icc (succ a) b ↔ x ∈ Ioc a b
Tactic: ext x
-- Lean 4 proof step from Mathlib.Order.Interval.Set.SuccPred (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : SuccOrder α
a : α
ha : ¬IsMax a
b x : α
⊢ x ∈ Icc (succ a) b ↔ x ∈ Ioc a b
have h : succ a ≤ x ∧ x ≤ b ↔ x ∈ Ioc a b
Tactic: rw [mem_Icc, mem_Ioc, succ_le_iff_of_not_isMax ha]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.SuccPred (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : SuccOrder α
a : α
ha : ¬IsMax a
b x : α
h : succ a ≤ x ∧ x ≤ b ↔ x ∈ Ioc a b
⊢ x ∈ Icc (succ a) b ↔ x ∈ Ioc a b
have h₁ : succ a ≤ x ∧ x ≤ b ↔ a < x ∧ x ≤ b
Tactic: rw [mem_Icc, mem_Ioc, succ_le_iff_of_not_isMax ha]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.SuccPred (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : SuccOrder α
a : α
ha : ¬IsMax a
b x : α
h : succ a ≤ x ∧ x ≤ b ↔ x ∈ Ioc a b
h₁ : succ a ≤ x ∧ x ≤ b ↔ a < x ∧ x ≤ b
⊢ x ∈ Icc (succ a) b ↔ x ∈ Ioc a b
have h₂ : a < x ∧ x ≤ b ↔ a < x ∧ x ≤ b
Tactic: rw [mem_Icc, mem_Ioc, succ_le_iff_of_not_isMax ha]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.SuccPred (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : SuccOrder α
b : α
hb : ¬IsMax b
a : α
⊢ Ico a (succ b) = Icc a b
have h : ∀ (x : α), x ∈ Ico a (succ b) ↔ x ∈ Icc a b
Tactic: ext x
-- Lean 4 proof step from Mathlib.Order.Interval.Set.SuccPred (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : SuccOrder α
b : α
hb : ¬IsMax b
a x : α
⊢ x ∈ Ico a (succ b) ↔ x ∈ Icc a b
have h : a ≤ x ∧ x < succ b ↔ x ∈ Icc a b
Tactic: rw [mem_Ico, mem_Icc, lt_succ_iff_of_not_isMax hb]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.SuccPred (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : SuccOrder α
b : α
hb : ¬IsMax b
a x : α
h : a ≤ x ∧ x < succ b ↔ x ∈ Icc a b
⊢ x ∈ Ico a (succ b) ↔ x ∈ Icc a b
have h₁ : a ≤ x ∧ x < succ b ↔ a ≤ x ∧ x ≤ b
Tactic: rw [mem_Ico, mem_Icc, lt_succ_iff_of_not_isMax hb]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.SuccPred (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : SuccOrder α
b : α
hb : ¬IsMax b
a x : α
h : a ≤ x ∧ x < succ b ↔ x ∈ Icc a b
h₁ : a ≤ x ∧ x < succ b ↔ a ≤ x ∧ x ≤ b
⊢ x ∈ Ico a (succ b) ↔ x ∈ Icc a b
have h₂ : a ≤ x ∧ x ≤ b ↔ a ≤ x ∧ x ≤ b
Tactic: rw [mem_Ico, mem_Icc, lt_succ_iff_of_not_isMax hb]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.SuccPred (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : SuccOrder α
b : α
hb : ¬IsMax b
a : α
⊢ Ioo a (succ b) = Ioc a b
have h : ∀ (x : α), x ∈ Ioo a (succ b) ↔ x ∈ Ioc a b
Tactic: ext x
-- Lean 4 proof step from Mathlib.Order.Interval.Set.SuccPred (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : SuccOrder α
b : α
hb : ¬IsMax b
a x : α
⊢ x ∈ Ioo a (succ b) ↔ x ∈ Ioc a b
have h : a < x ∧ x < succ b ↔ x ∈ Ioc a b
Tactic: rw [mem_Ioo, mem_Ioc, lt_succ_iff_of_not_isMax hb]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.SuccPred (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : SuccOrder α
b : α
hb : ¬IsMax b
a x : α
h : a < x ∧ x < succ b ↔ x ∈ Ioc a b
⊢ x ∈ Ioo a (succ b) ↔ x ∈ Ioc a b
have h₁ : a < x ∧ x < succ b ↔ a < x ∧ x ≤ b
Tactic: rw [mem_Ioo, mem_Ioc, lt_succ_iff_of_not_isMax hb]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.SuccPred (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : SuccOrder α
b : α
hb : ¬IsMax b
a x : α
h : a < x ∧ x < succ b ↔ x ∈ Ioc a b
h₁ : a < x ∧ x < succ b ↔ a < x ∧ x ≤ b
⊢ x ∈ Ioo a (succ b) ↔ x ∈ Ioc a b
have h₂ : a < x ∧ x ≤ b ↔ a < x ∧ x ≤ b
Tactic: rw [mem_Ioo, mem_Ioc, lt_succ_iff_of_not_isMax hb]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.SuccPred (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : SuccOrder α
b : α
hb : ¬IsMax b
a : α
⊢ Ico (succ a) (succ b) = Ioc a b
have rw : Ioo a (succ b) = Ioc a b
Tactic: rw [Ico_succ_left_eq_Ioo, Ioo_succ_right_eq_Ioc_of_not_isMax hb]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.SuccPred (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : SuccOrder α
b : α
hb : ¬IsMax b
a : α
rw : Ioo a (succ b) = Ioc a b
⊢ Ico (succ a) (succ b) = Ioc a b
have rw₁ : Ioc a b = Ioc a b
Tactic: rw [Ico_succ_left_eq_Ioo, Ioo_succ_right_eq_Ioc_of_not_isMax hb]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.SuccPred (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : SuccOrder α
a b : α
h : a ≤ b
⊢ insert a (Icc (succ a) b) = Icc a b
have h₁ : ∀ (x : α), x ∈ insert a (Icc (succ a) b) ↔ x ∈ Icc a b
Tactic: ext x
-- Lean 4 proof step from Mathlib.Order.Interval.Set.SuccPred (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : SuccOrder α
a b : α
h : a ≤ b
x : α
⊢ x ∈ insert a (Icc (succ a) b) ↔ x ∈ Icc a b
have h₁ : a ≤ x → a = x → x ≤ b
Tactic: simp [or_and_left, eq_comm, ← le_iff_eq_or_succ_le]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.SuccPred (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : SuccOrder α
a b : α
h : a ≤ succ b
⊢ insert (succ b) (Icc a b) = Icc a (succ b)
have h₁ : ∀ (x : α), x ∈ insert (succ b) (Icc a b) ↔ x ∈ Icc a (succ b)
Tactic: ext x
-- Lean 4 proof step from Mathlib.Order.Interval.Set.SuccPred (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : SuccOrder α
a b : α
h : a ≤ succ b
x : α
⊢ x ∈ insert (succ b) (Icc a b) ↔ x ∈ Icc a (succ b)
have h₁ : x = succ b ∨ x ≤ b → x = succ b → a ≤ x
Tactic: simp [or_and_left, le_succ_iff_eq_or_le]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.SuccPred (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : SuccOrder α
a b : α
h : a ≤ b
hb : ¬IsMax b
⊢ insert b (Ico a b) = Ico a (succ b)
have rw : insert b (Ico a b) = Icc a b
Tactic: rw [Ico_succ_right_of_not_isMax hb, ← Ico_insert_right h]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.SuccPred (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : SuccOrder α
a b : α
h : a ≤ b
hb : ¬IsMax b
rw : insert b (Ico a b) = Icc a b
⊢ insert b (Ico a b) = Ico a (succ b)
have rw₁ : insert b (Ico a b) = insert b (Ico a b)
Tactic: rw [Ico_succ_right_of_not_isMax hb, ← Ico_insert_right h]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.SuccPred (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : SuccOrder α
a b : α
h : a < b
⊢ insert a (Ico (succ a) b) = Ico a b
have rw : insert a (Ioo a b) = Ico a b
Tactic: rw [Ico_succ_left_of_not_isMax h.not_isMax, ← Ioo_insert_left h]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.SuccPred (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : SuccOrder α
a b : α
h : a < b
rw : insert a (Ioo a b) = Ico a b
⊢ insert a (Ico (succ a) b) = Ico a b
have rw₁ : insert a (Ioo a b) = insert a (Ioo a b)
Tactic: rw [Ico_succ_left_of_not_isMax h.not_isMax, ← Ioo_insert_left h]
-- Lean 4 proof step from Mathlib.Order.Interval.Set.SuccPred (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : SuccOrder α
a b : α
h : a ≤ b
hb : ¬IsMax b
⊢ insert (succ b) (Ioc a b) = Ioc a (succ b)
have h₁ : ∀ (x : α), x ∈ insert (succ b) (Ioc a b) ↔ x ∈ Ioc a (succ b)
Tactic: ext x
-- Lean 4 proof step from Mathlib.Order.Interval.Set.SuccPred (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : SuccOrder α
a b : α
h : a < b
⊢ insert (succ a) (Ioc (succ a) b) = Ioc a b
have rw : Icc (succ a) b = Ioc a b
Tactic: rw [Ioc_insert_left (succ_le_of_lt h), Icc_succ_left_of_not_isMax h.not_isMax]