awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Order.TransfiniteIteration (goal)
Goal:
I : Type u
inst : CompleteLattice I
φ : I → I
i₀ : I
J : Type w
inst_1 : LinearOrder J
inst_2 : OrderBot J
inst_3 : SuccOrder J
inst_4 : WellFoundedLT J
hφ : ∀ (i : I), i ≤ φ i
k j : J
hkj : k ≤ j
isMin :
  ∀ (k_1 : J) (hk : IsMin k_1) (hkj : k ≤ k_1),
    LE.le.{u} (α := I) ((fun (j : J) ↦ transfiniteIterate φ j i₀) k) ((fun (j : J) ↦ transfiniteIterate φ j i₀) k_1)
succ :
  ∀ (k' : J) (hk' : ¬IsMax k')
    (hkk' :
      ∀ (hkj : k ≤ k'),
        LE.le.{u} (α := I) ((fun (j : J) ↦ transfiniteIterate φ j i₀) k) ((fun (j : J) ↦ transfiniteIterate φ j i₀) k'))
    (hkj : k ≤ Order.succ k'),
    LE.le.{u} (α := I) ((fun (j : J) ↦ transfiniteIterate φ j i₀) k)
      ((fun (j : J) ↦ transfiniteIterate φ j i₀) (Order.succ k'))
⊢ LE.le.{u} (α := I) ((fun (j : J) ↦ transfiniteIterate φ j i₀) k) ((fun (j : J) ↦ transfiniteIterate φ j i₀) j)
have isSuccLimit : ∀ (k' : J) (hk' : Order.IsSuccLimit k'),
  (∀ b < k',
      ∀ (hkj : k ≤ b),
        LE.le.{u} (α := I) ((fun (j : J) ↦ transfiniteIterate φ j i₀) k)
          ((fun (j : J) ↦ transfiniteIterate φ j i₀) b)) →
    ∀ (hkj : k ≤ k'),
      LE.le.{u} (α := I) ((fun (j : J) ↦ transfiniteIterate φ j i₀) k) ((fun (j : J) ↦ transfiniteIterate φ j i₀) k')
Tactic: induction j using SuccOrder.limitRecOn with
  | isMin k hk =>
    obtain rfl := hk.eq_bot
    obtain rfl : k = ⊥ := by simpa using hkj
    rfl
  | succ k' hk' hkk' =>
    obtain hkj | rfl := hkj.lt_or_eq
    · refine (hkk' ((Order.lt_succ_iff_of_not_isMax hk').mp hkj)).trans ?_
      dsimp
      rw [transfiniteIterate_succ _ _ _ hk']
      apply hφ
    · rfl
  | isSuccLimit k' hk' _ =>
    obtain hkj | rfl := hkj.lt_or_eq
    · dsimp
      rw [transfiniteIterate_limit _ _ _ hk']
      exact le_iSup (fun (⟨l, hl⟩ : Set.Iio k') ↦ transfiniteIterate φ l i₀) ⟨k, hkj⟩
    · rfl
Cleared hypotheses: j, hkj
-- Lean 4 proof step from Mathlib.Order.TransfiniteIteration (goal)
Goal:
I : Type u
inst : CompleteLattice I
φ : I → I
i₀ : I
J : Type w
inst_1 : LinearOrder J
inst_2 : OrderBot J
inst_3 : SuccOrder J
inst_4 : WellFoundedLT J
hφ' : ∀ (i : I), i ≠ ⊤ → i < φ i
φtop : φ ⊤ = ⊤
H : ¬Function.Injective.{w + 1, u + 1} (β := I) fun (j : J) ↦ transfiniteIterate φ j i₀
i : I
⊢ i ≤ φ i
have pos : ∀ (hi : i = ⊤), i ≤ φ i
Tactic: by_cases hi : i = ⊤
-- Lean 4 proof step from Mathlib.Order.TransfiniteIteration (goal)
Goal:
I : Type u
inst : CompleteLattice I
φ : I → I
i₀ : I
J : Type w
inst_1 : LinearOrder J
inst_2 : OrderBot J
inst_3 : SuccOrder J
inst_4 : WellFoundedLT J
hφ' : ∀ (i : I), i ≠ ⊤ → i < φ i
φtop : φ ⊤ = ⊤
H : ¬Function.Injective.{w + 1, u + 1} (β := I) fun (j : J) ↦ transfiniteIterate φ j i₀
i : I
pos : ∀ (hi : i = ⊤), i ≤ φ i
⊢ i ≤ φ i
have neg : ∀ (hi : ¬i = ⊤), i ≤ φ i
Tactic: by_cases hi : i = ⊤
-- Lean 4 proof step from Mathlib.Order.TransfiniteIteration (goal)
Goal:
I : Type u
inst : CompleteLattice I
φ : I → I
i₀ : I
J : Type w
inst_1 : LinearOrder J
inst_2 : OrderBot J
inst_3 : SuccOrder J
inst_4 : WellFoundedLT J
hφ' : ∀ (i : I), i ≠ ⊤ → i < φ i
φtop : φ ⊤ = ⊤
H : ¬Function.Injective.{w + 1, u + 1} (β := I) fun (j : J) ↦ transfiniteIterate φ j i₀
i : I
hi : i = ⊤
⊢ i ≤ φ i
have pos : ⊤ ≤ φ ⊤
Tactic: subst hi
Cleared hypotheses: i, hi
-- Lean 4 proof step from Mathlib.Order.TransfiniteIteration (goal)
Goal:
I : Type u
inst : CompleteLattice I
φ : I → I
i₀ : I
J : Type w
inst_1 : LinearOrder J
inst_2 : OrderBot J
inst_3 : SuccOrder J
inst_4 : WellFoundedLT J
hφ' : ∀ (i : I), i ≠ ⊤ → i < φ i
φtop : φ ⊤ = ⊤
H : ¬Function.Injective.{w + 1, u + 1} (β := I) fun (j : J) ↦ transfiniteIterate φ j i₀
⊢ ⊤ ≤ φ ⊤
have pos : LE.le.{u} (α := I) ⊤ ⊤
Tactic: rw [φtop]
-- Lean 4 proof step from Mathlib.Order.TransfiniteIteration (hypothesis)
Goal:
I : Type u
inst : CompleteLattice I
φ : I → I
i₀ : I
J : Type w
inst_1 : LinearOrder J
inst_2 : OrderBot J
inst_3 : SuccOrder J
inst_4 : WellFoundedLT J
hφ' : ∀ (i : I), i ≠ ⊤ → i < φ i
φtop : φ ⊤ = ⊤
H : ¬Function.Injective.{w + 1, u + 1} (β := I) fun (j : J) ↦ transfiniteIterate φ j i₀
⊢ ∃ (j : J), transfiniteIterate φ j i₀ = ⊤
have hφ : ∀ (i : I), i ≤ φ i
Tactic: have hφ (i : I) : i ≤ φ i := by
    by_cases hi : i = ⊤
    · subst hi
      rw [φtop]
    · exact (hφ' i hi).le
-- Lean 4 proof step from Mathlib.Order.TransfiniteIteration (goal)
Goal:
I : Type u
inst : CompleteLattice I
φ : I → I
i₀ : I
J : Type w
inst_1 : LinearOrder J
inst_2 : OrderBot J
inst_3 : SuccOrder J
inst_4 : WellFoundedLT J
hφ' : ∀ (i : I), i ≠ ⊤ → i < φ i
φtop : φ ⊤ = ⊤
H : ¬Function.Injective.{w + 1, u + 1} (β := I) fun (j : J) ↦ transfiniteIterate φ j i₀
hφ : ∀ (i : I), i ≤ φ i
⊢ ∃ (j : J), transfiniteIterate φ j i₀ = ⊤
have obtain : ∀ (j₁ j₂ : J) (hj : j₁ < j₂) (eq : transfiniteIterate φ j₁ i₀ = transfiniteIterate φ j₂ i₀),
  ∃ (j : J), transfiniteIterate φ j i₀ = ⊤
Tactic: obtain ⟨j₁, j₂, hj, eq⟩ : ∃ (j₁ j₂ : J) (hj : j₁ < j₂),
      transfiniteIterate φ j₁ i₀ = transfiniteIterate φ j₂ i₀ := by
    grind [Function.Injective]
-- Lean 4 proof step from Mathlib.Order.TransfiniteIteration (goal)
Goal:
I : Type u
inst : CompleteLattice I
φ : I → I
i₀ : I
J : Type w
inst_1 : LinearOrder J
inst_2 : OrderBot J
inst_3 : SuccOrder J
inst_4 : WellFoundedLT J
hφ' : ∀ (i : I), i ≠ ⊤ → i < φ i
φtop : φ ⊤ = ⊤
H : ¬Function.Injective.{w + 1, u + 1} (β := I) fun (j : J) ↦ transfiniteIterate φ j i₀
hφ : ∀ (i : I), i ≤ φ i
j₁ j₂ : J
hj : j₁ < j₂
eq : transfiniteIterate φ j₁ i₀ = transfiniteIterate φ j₂ i₀
⊢ ∃ (j : J), transfiniteIterate φ j i₀ = ⊤
have by_contra! : ∀ (this : ∀ (j : J), transfiniteIterate φ j i₀ ≠ ⊤), False
Tactic: by_contra!
-- Lean 4 proof step from Mathlib.Order.TransfiniteIteration (goal)
Goal:
I : Type u
inst : CompleteLattice I
φ : I → I
i₀ : I
J : Type w
inst_1 : LinearOrder J
inst_2 : OrderBot J
inst_3 : SuccOrder J
inst_4 : WellFoundedLT J
hφ' : ∀ (i : I), i ≠ ⊤ → i < φ i
φtop : φ ⊤ = ⊤
H : ¬Function.Injective.{w + 1, u + 1} (β := I) fun (j : J) ↦ transfiniteIterate φ j i₀
hφ : ∀ (i : I), i ≤ φ i
j₁ j₂ : J
hj : j₁ < j₂
eq : transfiniteIterate φ j₁ i₀ = transfiniteIterate φ j₂ i₀
this : ∀ (j : J), transfiniteIterate φ j i₀ ≠ ⊤
⊢ False
have suffices : transfiniteIterate φ j₁ i₀ < transfiniteIterate φ j₂ i₀
Tactic: suffices transfiniteIterate φ j₁ i₀ < transfiniteIterate φ j₂ i₀ by
    simp only [eq, lt_self_iff_false] at this
-- Lean 4 proof step from Mathlib.Order.TransfiniteIteration (goal)
Goal:
I : Type u
inst : CompleteLattice I
φ : I → I
i₀ : I
J : Type w
inst_1 : LinearOrder J
inst_2 : OrderBot J
inst_3 : SuccOrder J
inst_4 : WellFoundedLT J
hφ' : ∀ (i : I), i ≠ ⊤ → i < φ i
φtop : φ ⊤ = ⊤
H : ¬Function.Injective.{w + 1, u + 1} (β := I) fun (j : J) ↦ transfiniteIterate φ j i₀
hφ : ∀ (i : I), i ≤ φ i
j₁ j₂ : J
hj : j₁ < j₂
eq : transfiniteIterate φ j₁ i₀ = transfiniteIterate φ j₂ i₀
this : ∀ (j : J), transfiniteIterate φ j i₀ ≠ ⊤
⊢ ¬IsMax j₁
have simp : ∃ (b : J), j₁ < b
Tactic: simp only [not_isMax_iff]
-- Lean 4 proof step from Mathlib.Order.TransfiniteIteration (hypothesis)
Goal:
I : Type u
inst : CompleteLattice I
φ : I → I
i₀ : I
J : Type w
inst_1 : LinearOrder J
inst_2 : OrderBot J
inst_3 : SuccOrder J
inst_4 : WellFoundedLT J
hφ' : ∀ (i : I), i ≠ ⊤ → i < φ i
φtop : φ ⊤ = ⊤
H : ¬Function.Injective.{w + 1, u + 1} (β := I) fun (j : J) ↦ transfiniteIterate φ j i₀
hφ : ∀ (i : I), i ≤ φ i
j₁ j₂ : J
hj : j₁ < j₂
eq : transfiniteIterate φ j₁ i₀ = transfiniteIterate φ j₂ i₀
this : ∀ (j : J), transfiniteIterate φ j i₀ ≠ ⊤
⊢ transfiniteIterate φ j₁ i₀ < transfiniteIterate φ j₂ i₀
have hj₁ : ¬IsMax j₁
Tactic: have hj₁ : ¬ IsMax j₁ := by
    simp only [not_isMax_iff]
    exact ⟨_, hj⟩
-- Lean 4 proof step from Mathlib.Order.TransfiniteIteration (goal)
Goal:
I : Type u
inst : CompleteLattice I
φ : I → I
i₀ : I
J : Type w
inst_1 : LinearOrder J
inst_2 : OrderBot J
inst_3 : SuccOrder J
inst_4 : WellFoundedLT J
hφ' : ∀ (i : I), i ≠ ⊤ → i < φ i
φtop : φ ⊤ = ⊤
H : ¬Function.Injective.{w + 1, u + 1} (β := I) fun (j : J) ↦ transfiniteIterate φ j i₀
hφ : ∀ (i : I), i ≤ φ i
j₁ j₂ : J
hj : j₁ < j₂
eq : transfiniteIterate φ j₁ i₀ = transfiniteIterate φ j₂ i₀
this : ∀ (j : J), transfiniteIterate φ j i₀ ≠ ⊤
hj₁ : ¬IsMax j₁
⊢ transfiniteIterate φ j₁ i₀ < transfiniteIterate φ j₂ i₀
have refine : φ (transfiniteIterate φ j₁ i₀) ≤ transfiniteIterate φ j₂ i₀
Tactic: refine lt_of_lt_of_le (hφ' _ (this j₁)) ?_
-- Lean 4 proof step from Mathlib.Order.TransfiniteIteration (goal)
Goal:
I : Type u
inst : CompleteLattice I
φ : I → I
i₀ : I
J : Type w
inst_1 : LinearOrder J
inst_2 : OrderBot J
inst_3 : SuccOrder J
inst_4 : WellFoundedLT J
hφ' : ∀ (i : I), i ≠ ⊤ → i < φ i
φtop : φ ⊤ = ⊤
H : ¬Function.Injective.{w + 1, u + 1} (β := I) fun (j : J) ↦ transfiniteIterate φ j i₀
hφ : ∀ (i : I), i ≤ φ i
j₁ j₂ : J
hj : j₁ < j₂
eq : transfiniteIterate φ j₁ i₀ = transfiniteIterate φ j₂ i₀
this : ∀ (j : J), transfiniteIterate φ j i₀ ≠ ⊤
hj₁ : ¬IsMax j₁
⊢ φ (transfiniteIterate φ j₁ i₀) ≤ transfiniteIterate φ j₂ i₀
have rw : transfiniteIterate φ (Order.succ j₁) i₀ ≤ transfiniteIterate φ j₂ i₀
Tactic: rw [← transfiniteIterate_succ φ i₀ j₁ hj₁]
-- Lean 4 proof step from Mathlib.Order.Types.Arithmetic (goal)
Goal:
o : OrderType.{u}
α : Type u
x : LinearOrder α
⊢ 0 + type α = type α
have simp : type (Lex (PEmpty.{u + 1} ⊕ α)) = type α
Tactic: simp only [show 0 = type PEmpty by rfl, ← type_lex_sum]
-- Lean 4 proof step from Mathlib.Order.Types.Arithmetic (goal)
Goal:
o : OrderType.{u}
α : Type u
x : LinearOrder α
⊢ type α + 0 = type α
have simp : type (Lex (α ⊕ PEmpty.{u + 1})) = type α
Tactic: simp only [show 0 = type PEmpty by rfl, ← type_lex_sum]
-- Lean 4 proof step from Mathlib.Order.Types.Arithmetic (goal)
Goal:
o₁ o₂ o₃ : OrderType.{u}
α : Type u
x : LinearOrder α
β : Type u
x_1 : LinearOrder β
γ : Type u
x_2 : LinearOrder γ
⊢ type α * type β * type γ = type α * (type β * type γ)
have simp : type (Lex (γ × Lex (β × α))) = type (Lex (Lex (γ × β) × α))
Tactic: simp only [← type_lex_prod]
-- Lean 4 proof step from Mathlib.Order.Types.Arithmetic (goal)
Goal:
o : OrderType.{u}
α : Type u
x : LinearOrder α
⊢ 1 * type α = type α
have simp : type (Lex (α × PUnit.{u + 1})) = type α
Tactic: simp only [show 1 = type PUnit by rfl, ← type_lex_prod]
-- Lean 4 proof step from Mathlib.Order.Types.Arithmetic (goal)
Goal:
o : OrderType.{u}
α : Type u
x : LinearOrder α
⊢ type α * 1 = type α
have simp : type (Lex (PUnit.{u + 1} × α)) = type α
Tactic: simp only [show 1 = type PUnit by rfl, ← type_lex_prod]
-- Lean 4 proof step from Mathlib.Order.Types.Arithmetic (goal)
Goal:
α : Type u
inst : LinearOrder α
⊢ (type α).card = #α
have rw : (type α).liftOn (fun (α : Type u) (x : LinearOrder α) ↦ #α) card._proof_1 = #α
Tactic: rw [card, liftOn_type]
-- Lean 4 proof step from Mathlib.Order.Types.Arithmetic (goal)
Goal:
α : Type u
inst : LinearOrder α
rw : (type α).liftOn (fun (α : Type u) (x : LinearOrder α) ↦ #α) card._proof_1 = #α
⊢ (type α).card = #α
have rw₁ : #α = #α
Tactic: rw [card, liftOn_type]
-- Lean 4 proof step from Mathlib.Order.Types.Arithmetic (goal)
Goal:
a b c : OrderType.{u_1}
⊢ a * (b + c) = a * b + a * c
have refine : ∀ (x : Type u_1) (x_1 : LinearOrder x) (x_2 : Type u_1) (x_3 : LinearOrder x_2) (x_4 : Type u_1)
  (x_5 : LinearOrder x_4), type x * (type x_2 + type x_4) = type x * type x_2 + type x * type x_4
Tactic: refine inductionOn₃ a b c (fun _ _ _ _ _ _ ↦ ?_)
-- Lean 4 proof step from Mathlib.Order.Types.Arithmetic (goal)
Goal:
a b c : OrderType.{u_1}
x : Type u_1
x_1 : LinearOrder x
x_2 : Type u_1
x_3 : LinearOrder x_2
x_4 : Type u_1
x_5 : LinearOrder x_4
⊢ type x * (type x_2 + type x_4) = type x * type x_2 + type x * type x_4
have simp : type (Lex (Lex (x_2 ⊕ x_4) × x)) = type (Lex (Lex (x_2 × x) ⊕ Lex (x_4 × x)))
Tactic: simp only [← type_lex_prod, ← type_lex_sum]
-- Lean 4 proof step from Mathlib.Order.Types.Defs (goal)
Goal:
α : Type u
inst : LinearOrder α
inst_1 : Nonempty α
inst_2 : Subsingleton α
⊢ type α = 1
have intro : ∀ (val : Unique α), type α = 1
Tactic: cases nonempty_unique α
-- Lean 4 proof step from Mathlib.Order.Types.Defs (goal)
Goal:
o : OrderType.{u_1}
⊢ IsEmpty.{u_1 + 1} o.ToType ↔ o = 0
have rw : type o.ToType = 0 ↔ o = 0
Tactic: rw [← @type_eq_zero o.ToType, type_toType]
-- Lean 4 proof step from Mathlib.Order.Types.Defs (goal)
Goal:
o : OrderType.{u_1}
rw : type o.ToType = 0 ↔ o = 0
⊢ IsEmpty.{u_1 + 1} o.ToType ↔ o = 0
have rw₁ : o = 0 ↔ o = 0
Tactic: rw [← @type_eq_zero o.ToType, type_toType]
-- Lean 4 proof step from Mathlib.Order.Types.Defs (goal)
Goal:
o : OrderType.{u_1}
⊢ Nonempty.{u_1 + 1} o.ToType ↔ o ≠ 0
have rw : type o.ToType ≠ 0 ↔ o ≠ 0
Tactic: rw [← @type_ne_zero_iff o.ToType, type_toType]
-- Lean 4 proof step from Mathlib.Order.Types.Defs (goal)
Goal:
o : OrderType.{u_1}
rw : type o.ToType ≠ 0 ↔ o ≠ 0
⊢ Nonempty.{u_1 + 1} o.ToType ↔ o ≠ 0
have rw₁ : o ≠ 0 ↔ o ≠ 0
Tactic: rw [← @type_ne_zero_iff o.ToType, type_toType]
-- Lean 4 proof step from Mathlib.Order.Types.Defs (hypothesis)
Goal:
o : OrderType.{u_1}
ho : o ≠ 0
⊢ 0 < o
have this : Nonempty.{u_1 + 1} o.ToType
Tactic: have := nonempty_toType_iff.2 ho
-- Lean 4 proof step from Mathlib.Order.Types.Defs (goal)
Goal:
o : OrderType.{u_1}
ho : o ≠ 0
this : Nonempty.{u_1 + 1} o.ToType
⊢ 0 < o
have rw : 0 < type o.ToType
Tactic: rw [← type_toType o]
-- Lean 4 proof step from Mathlib.Order.Types.Defs (goal)
Goal:
α β : Type u
inst : LinearOrder α
inst_1 : LinearOrder β
⊢ lift.{u_1, u} (type α) = lift.{u_1, u} (type β) ↔ Nonempty.{u + 1} (α ≃o β)
have refine : ∀ (h : lift.{u_1, u} (type α) = lift.{u_1, u} (type β)), Nonempty.{u + 1} (α ≃o β)
Tactic: refine ⟨fun h ↦ ?_, fun ⟨h⟩ ↦ congrArg lift <| type_congr h⟩
-- Lean 4 proof step from Mathlib.Order.Types.Defs (hypothesis)
Goal:
α β : Type u
inst : LinearOrder α
inst_1 : LinearOrder β
h : lift.{u_1, u} (type α) = lift.{u_1, u} (type β)
⊢ Nonempty.{u + 1} (α ≃o β)
have h₁ : Nonempty (ULift.{u_1, u} α ≃o ULift.{u_1, u} β)
Tactic: rw [← type_ulift, ← type_ulift, type_eq_type] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Order.Types.Defs (goal)
Goal:
α β : Type u
inst : LinearOrder α
inst_1 : LinearOrder β
⊢ lift.{u_1, u} (type α) ≤ lift.{u_1, u} (type β) ↔ Nonempty.{u + 1} (α ↪o β)
have refine : ∀ (h : lift.{u_1, u} (type α) ≤ lift.{u_1, u} (type β)), Nonempty.{u + 1} (α ↪o β)
Tactic: refine ⟨fun h ↦ ?_, fun ⟨h⟩ ↦ type_le_type <| (ULift.orderIso.toOrderEmbedding.trans h).trans
   ULift.orderIso.symm.toOrderEmbedding⟩
-- Lean 4 proof step from Mathlib.Order.Types.Defs (hypothesis)
Goal:
α β : Type u
inst : LinearOrder α
inst_1 : LinearOrder β
h : lift.{u_1, u} (type α) ≤ lift.{u_1, u} (type β)
⊢ Nonempty.{u + 1} (α ↪o β)
have h₁ : Nonempty (ULift.{u_1, u} α ↪o ULift.{u_1, u} β)
Tactic: rw [← type_ulift, ← type_ulift, type_le_type_iff] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Order.UpperLower.Basic (goal)
Goal:
α : Type u_1
inst : LE α
s : Set α
h : IsUpperSet sᶜ
⊢ IsLowerSet s
have h₁ : s = sᶜᶜ
Tactic: convert! h.compl
-- Lean 4 proof step from Mathlib.Order.UpperLower.Basic (goal)
Goal:
α : Type u_1
inst : LE α
s : Set α
h : IsUpperSet sᶜ
⊢ s = sᶜᶜ
have h₁ : s = s
Tactic: rw [compl_compl]
-- Lean 4 proof step from Mathlib.Order.UpperLower.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
s : Set α
hs : IsUpperSet s
f : α ≃o β
⊢ IsUpperSet.{u_2} (α := β) ((⇑f : (a : α) → β) '' s)
have change : IsUpperSet.{u_2} (α := β) ((⇑(↑f : α ≃ β) : (a : α) → β) '' s)
Tactic: change IsUpperSet ((f : α ≃ β) '' s)
-- Lean 4 proof step from Mathlib.Order.UpperLower.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
s : Set α
hs : IsUpperSet s
f : α ≃o β
⊢ IsUpperSet.{u_2} (α := β) ((⇑(↑f : α ≃ β) : (a : α) → β) '' s)
have rw : IsUpperSet.{u_2} (α := β) ((⇑(↑f : α ≃ β).symm : (a : β) → α) ⁻¹' s)
Tactic: rw [Equiv.image_eq_preimage_symm]
-- Lean 4 proof step from Mathlib.Order.UpperLower.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
e : α ↪o β
he : IsUpperSet.{u_2} (α := β) (range.{u_2, u_1 + 1} (ι := α) (⇑e : (a : α) → β))
a : α
⊢ Eq.{u_2 + 1} (α := Set β) ((⇑e : (a : α) → β) '' Ici a : Set β) (Ici ((e : (a : α) → β) a) : Set β)
have rw : Eq.{u_2 + 1} (α := Set β)
  (image.{u_1, u_2} (α := α) (⇑e : (a : α) → β)
      (preimage.{u_1, u_2} (β := β) ((⇑e : (a : α) → β) : (a : α) → β) (Ici ((e : (a : α) → β) a) : Set β)) :
    Set β)
  (Ici ((e : (a : α) → β) a) : Set β)
Tactic: rw [← e.preimage_Ici, image_preimage_eq_inter_range,
    inter_eq_left.2 <| he.Ici_subset (mem_range_self _)]
-- Lean 4 proof step from Mathlib.Order.UpperLower.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
e : α ↪o β
he : IsUpperSet.{u_2} (α := β) (range.{u_2, u_1 + 1} (ι := α) (⇑e : (a : α) → β))
a : α
rw :
  Eq.{u_2 + 1} (α := Set β)
    (image.{u_1, u_2} (α := α) (⇑e : (a : α) → β)
        (preimage.{u_1, u_2} (β := β) ((⇑e : (a : α) → β) : (a : α) → β) (Ici ((e : (a : α) → β) a) : Set β)) :
      Set β)
    (Ici ((e : (a : α) → β) a) : Set β)
⊢ Eq.{u_2 + 1} (α := Set β) ((⇑e : (a : α) → β) '' Ici a : Set β) (Ici ((e : (a : α) → β) a) : Set β)
have rw₁ : Eq.{u_2 + 1} (α := Set β) (Ici ((e : (a : α) → β) a) ∩ range.{u_2, u_1 + 1} (ι := α) (⇑e : (a : α) → β) : Set β)
  (Ici ((e : (a : α) → β) a) : Set β)
Tactic: rw [← e.preimage_Ici, image_preimage_eq_inter_range,
    inter_eq_left.2 <| he.Ici_subset (mem_range_self _)]
-- Lean 4 proof step from Mathlib.Order.UpperLower.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
e : α ↪o β
he : IsUpperSet.{u_2} (α := β) (range.{u_2, u_1 + 1} (ι := α) (⇑e : (a : α) → β))
a : α
rw :
  Eq.{u_2 + 1} (α := Set β)
    (image.{u_1, u_2} (α := α) (⇑e : (a : α) → β)
        (preimage.{u_1, u_2} (β := β) ((⇑e : (a : α) → β) : (a : α) → β) (Ici ((e : (a : α) → β) a) : Set β)) :
      Set β)
    (Ici ((e : (a : α) → β) a) : Set β)
rw₁ :
  Eq.{u_2 + 1} (α := Set β) (Ici ((e : (a : α) → β) a) ∩ range.{u_2, u_1 + 1} (ι := α) (⇑e : (a : α) → β) : Set β)
    (Ici ((e : (a : α) → β) a) : Set β)
⊢ Eq.{u_2 + 1} (α := Set β) ((⇑e : (a : α) → β) '' Ici a : Set β) (Ici ((e : (a : α) → β) a) : Set β)
have rw₂ : Eq.{u_2 + 1} (α := Set β) (Ici ((e : (a : α) → β) a) : Set β) (Ici ((e : (a : α) → β) a) : Set β)
Tactic: rw [← e.preimage_Ici, image_preimage_eq_inter_range,
    inter_eq_left.2 <| he.Ici_subset (mem_range_self _)]
-- Lean 4 proof step from Mathlib.Order.UpperLower.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
e : α ↪o β
he : IsUpperSet.{u_2} (α := β) (range.{u_2, u_1 + 1} (ι := α) (⇑e : (a : α) → β))
a : α
⊢ Eq.{u_2 + 1} (α := Set β) ((⇑e : (a : α) → β) '' Ioi a : Set β) (Ioi ((e : (a : α) → β) a) : Set β)
have rw : Eq.{u_2 + 1} (α := Set β)
  (image.{u_1, u_2} (α := α) (⇑e : (a : α) → β)
      (preimage.{u_1, u_2} (β := β) ((⇑e : (a : α) → β) : (a : α) → β) (Ioi ((e : (a : α) → β) a) : Set β)) :
    Set β)
  (Ioi ((e : (a : α) → β) a) : Set β)
Tactic: rw [← e.preimage_Ioi, image_preimage_eq_inter_range,
    inter_eq_left.2 <| he.Ioi_subset (mem_range_self _)]
-- Lean 4 proof step from Mathlib.Order.UpperLower.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
e : α ↪o β
he : IsUpperSet.{u_2} (α := β) (range.{u_2, u_1 + 1} (ι := α) (⇑e : (a : α) → β))
a : α
rw :
  Eq.{u_2 + 1} (α := Set β)
    (image.{u_1, u_2} (α := α) (⇑e : (a : α) → β)
        (preimage.{u_1, u_2} (β := β) ((⇑e : (a : α) → β) : (a : α) → β) (Ioi ((e : (a : α) → β) a) : Set β)) :
      Set β)
    (Ioi ((e : (a : α) → β) a) : Set β)
⊢ Eq.{u_2 + 1} (α := Set β) ((⇑e : (a : α) → β) '' Ioi a : Set β) (Ioi ((e : (a : α) → β) a) : Set β)
have rw₁ : Eq.{u_2 + 1} (α := Set β) (Ioi ((e : (a : α) → β) a) ∩ range.{u_2, u_1 + 1} (ι := α) (⇑e : (a : α) → β) : Set β)
  (Ioi ((e : (a : α) → β) a) : Set β)
Tactic: rw [← e.preimage_Ioi, image_preimage_eq_inter_range,
    inter_eq_left.2 <| he.Ioi_subset (mem_range_self _)]
-- Lean 4 proof step from Mathlib.Order.UpperLower.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
e : α ↪o β
he : IsUpperSet.{u_2} (α := β) (range.{u_2, u_1 + 1} (ι := α) (⇑e : (a : α) → β))
a : α
rw :
  Eq.{u_2 + 1} (α := Set β)
    (image.{u_1, u_2} (α := α) (⇑e : (a : α) → β)
        (preimage.{u_1, u_2} (β := β) ((⇑e : (a : α) → β) : (a : α) → β) (Ioi ((e : (a : α) → β) a) : Set β)) :
      Set β)
    (Ioi ((e : (a : α) → β) a) : Set β)
rw₁ :
  Eq.{u_2 + 1} (α := Set β) (Ioi ((e : (a : α) → β) a) ∩ range.{u_2, u_1 + 1} (ι := α) (⇑e : (a : α) → β) : Set β)
    (Ioi ((e : (a : α) → β) a) : Set β)
⊢ Eq.{u_2 + 1} (α := Set β) ((⇑e : (a : α) → β) '' Ioi a : Set β) (Ioi ((e : (a : α) → β) a) : Set β)
have rw₂ : Eq.{u_2 + 1} (α := Set β) (Ioi ((e : (a : α) → β) a) : Set β) (Ioi ((e : (a : α) → β) a) : Set β)
Tactic: rw [← e.preimage_Ioi, image_preimage_eq_inter_range,
    inter_eq_left.2 <| he.Ioi_subset (mem_range_self _)]
-- Lean 4 proof step from Mathlib.Order.UpperLower.Basic (goal)
Goal:
α : Type u_1
inst : Preorder α
s : Set α
inst_1 : NoMaxOrder α
hs : IsUpperSet s
a : α
ha : a ∈ s
b : α
hb : b ∈ upperBounds s
⊢ False
have obtain : ∀ (c : α) (hc : b < c), False
Tactic: obtain ⟨c, hc⟩ := exists_gt b
-- Lean 4 proof step from Mathlib.Order.UpperLower.Basic (goal)
Goal:
α : Type u_1
inst : LinearOrder α
s : Set α
inst_1 : WellFoundedLT α
h : IsUpperSet s
⊢ s = ∅ ∨ ∃ (a : α), s = Ici a
have refine : ∀ (ha : ¬s = ∅), ∃ (a : α), s = Ici a
Tactic: refine or_iff_not_imp_left.2 fun ha ↦ ?_
-- Lean 4 proof step from Mathlib.Order.UpperLower.Basic (goal)
Goal:
α : Type u_1
inst : LinearOrder α
s : Set α
inst_1 : WellFoundedLT α
h : IsUpperSet s
ha : ¬s = ∅
⊢ ∃ (a : α), s = Ici a
have obtain : ∀ (a : α) (ha : a ∈ s), ∃ (a : α), s = Ici a
Tactic: obtain ⟨a, ha⟩ := Set.nonempty_iff_ne_empty.2 ha
-- Lean 4 proof step from Mathlib.Order.UpperLower.Basic (goal)
Goal:
α : Type u_1
inst : LinearOrder α
s : Set α
inst_1 : WellFoundedLT α
h : IsLowerSet s
⊢ s = univ ∨ ∃ (a : α), s = Iio a
have simp_rw : sᶜ = univᶜ ∨ ∃ (a : α), sᶜ = (Iio a)ᶜ
Tactic: simp_rw [← @compl_inj_iff _ s]
-- Lean 4 proof step from Mathlib.Order.UpperLower.Closure (goal)
Goal:
α : Type u_1
inst : Preorder α
s : Set α
⊢ (↑(upperClosure s) : Set α) = ⋃ a ∈ s, Ici a
have h : ∀ (x : α), x ∈ (↑(upperClosure s) : Set α) ↔ Membership.mem (γ := Set α) (⋃ a ∈ s, Ici a) x
Tactic: ext
-- Lean 4 proof step from Mathlib.Order.UpperLower.Closure (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
s : Set α
f : α ≃o β
⊢ Eq.{u_2 + 1} (α := UpperSet β) (upperClosure ((⇑f : (a : α) → β) '' s))
    ((UpperSet.map f : (a : UpperSet α) → UpperSet β) (upperClosure s))
have rw : Eq.{u_2 + 1} (α := UpperSet β) (upperClosure ((⇑f : (a : α) → β) '' s))
  (((UpperSet.map f.symm).symm : (a : UpperSet α) → UpperSet β) (upperClosure s))
Tactic: rw [← f.symm_symm, ← UpperSet.symm_map, f.symm_symm]
-- Lean 4 proof step from Mathlib.Order.UpperLower.Closure (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Preorder α
inst_1 : Preorder β
s : Set α
f : α ≃o β
⊢ Eq.{u_2 + 1} (α := UpperSet β) (upperClosure ((⇑f : (a : α) → β) '' s))
    (((UpperSet.map f.symm).symm : (a : UpperSet α) → UpperSet β) (upperClosure s))
have a : ∀ (x : β),
  x ∈ (↑(upperClosure ((⇑f : (a : α) → β) '' s)) : Set β) ↔
    x ∈ (↑(((UpperSet.map f.symm).symm : (a : UpperSet α) → UpperSet β) (upperClosure s) : UpperSet β) : Set β)
Tactic: ext
-- Lean 4 proof step from Mathlib.Order.UpperLower.Closure (goal)
Goal:
α : Type u_1
inst : Preorder α
s : Set α
⊢ Eq (α := UpperSet α) (⨅ a ∈ s, Ici a) (upperClosure s)
have a : ∀ (x : α), x ∈ (↑(⨅ a ∈ s, Ici a) : Set α) ↔ x ∈ (↑(upperClosure s) : Set α)
Tactic: ext
-- Lean 4 proof step from Mathlib.Order.UpperLower.Closure (goal)
Goal:
α : Type u_1
inst : Preorder α
s : Set α
⊢ Eq (α := UpperSet α) (upperClosure s) ⊤ ↔ s = ∅
have rw : s ⊆ (↑⊤ : Set α) ↔ s = ∅
Tactic: rw [eq_top_iff, le_upperClosure]
-- Lean 4 proof step from Mathlib.Order.UpperLower.Closure (goal)
Goal:
α : Type u_1
inst : Preorder α
a : α
⊢ Eq (α := UpperSet α) (upperClosure {a}) (UpperSet.Ici a)
have a₁ : ∀ (x : α), x ∈ (↑(upperClosure {a}) : Set α) ↔ x ∈ (↑(UpperSet.Ici a) : Set α)
Tactic: ext
-- Lean 4 proof step from Mathlib.Order.UpperLower.Closure (goal)
Goal:
α : Type u_1
inst : Preorder α
S : Set (Set α)
⊢ Eq (α := UpperSet α) (upperClosure (⋃₀ S)) (⨅ s ∈ S, upperClosure s)
have simp_rw : Eq.{u_1 + 1} (α := UpperSet α) (upperClosure (⋃ i ∈ S, i)) (⨅ s ∈ S, upperClosure s)
Tactic: simp_rw [sUnion_eq_biUnion, upperClosure_iUnion]