awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Order.WellQuasiOrder (goal)
Goal:
α : Type u_3
β : Type u_4
r : α → α → Prop
s : β → β → Prop
f : r ≃r s
⊢ ∀ (a : ℕ → α),
    (∃ (m : ℕ) (n : ℕ), m < n ∧ r (a m) (a n)) ↔
      ∃ (m : ℕ) (n : ℕ),
        m < n ∧
          s (((Equiv.refl ℕ).arrowCongr (↑f : α ≃ β) : (a : ℕ → α) → ℕ → β) a m)
            (((Equiv.refl ℕ).arrowCongr (↑f : α ≃ β) : (a : ℕ → α) → ℕ → β) a n)
have a : ∀ (g : ℕ → α) (a b : ℕ),
  r (g a) (g b) ↔
    s (((Equiv.refl ℕ).arrowCongr (↑f : α ≃ β) : (a : ℕ → α) → ℕ → β) g a)
      (((Equiv.refl ℕ).arrowCongr (↑f : α ≃ β) : (a : ℕ → α) → ℕ → β) g b)
Tactic: congr! with g a b
-- Lean 4 proof step from Mathlib.Order.WellQuasiOrder (goal)
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst : Preorder α
inst_1 : WellQuasiOrderedLE α
⊢ WellFoundedLT α
have rw : IsEmpty.{u_1 + 1} ((fun (x1 x2 : ℕ) ↦ x1 > x2) ↪r fun (x1 x2 : α) ↦ x1 < x2)
Tactic: rw [WellFoundedLT, isWellFounded_iff, RelEmbedding.wellFounded_iff_isEmpty]
-- Lean 4 proof step from Mathlib.Order.WellQuasiOrder (goal)
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst : Preorder α
inst_1 : WellQuasiOrderedLE α
⊢ IsEmpty.{u_1 + 1} ((fun (x1 x2 : ℕ) ↦ x1 > x2) ↪r fun (x1 x2 : α) ↦ x1 < x2)
have refine : ∀ (f : (fun (x1 x2 : ℕ) ↦ x1 > x2) ↪r fun (x1 x2 : α) ↦ x1 < x2), False
Tactic: refine ⟨fun f ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Order.WellQuasiOrder (goal)
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst : Preorder α
inst_1 : WellQuasiOrderedLE α
f : (fun (x1 x2 : ℕ) ↦ x1 > x2) ↪r fun (x1 x2 : α) ↦ x1 < x2
⊢ False
have obtain : ∀ (a b : ℕ) (h : a < b) (hf : LE.le (α := α) ((f : (a : ℕ) → α) a : α) ((f : (a : ℕ) → α) b : α)), False
Tactic: obtain ⟨a, b, h, hf⟩ := wellQuasiOrdered_le f
-- Lean 4 proof step from Mathlib.Order.WellQuasiOrder (hypothesis)
Goal:
α : Type u_3
r : α → α → Prop
inst : IsPreorder α r
h : WellQuasiOrdered r
x : Preorder α := { le := r, le_refl := ⋯, le_trans := ⋯, lt_iff_le_not_ge := ⋯ }
⊢ WellFounded fun (a b : α) ↦ r a b ∧ ¬r b a
have this : WellQuasiOrderedLE α
Tactic: have : WellQuasiOrderedLE α := ⟨h⟩
-- Lean 4 proof step from Mathlib.Order.WellQuasiOrder (goal)
Goal:
α : Type u_1
inst : Preorder α
⊢ WellQuasiOrderedLE α ↔ WellFoundedLT α ∧ ∀ (s : Set α), IsAntichain (fun (x1 x2 : α) ↦ x1 ≤ x2) s → s.Finite
have refine : (WellFoundedLT α ∧ ∀ (s : Set α), IsAntichain (fun (x1 x2 : α) ↦ x1 ≤ x2) s → s.Finite) →
  ∀ (hwf : WellFoundedLT α) (hc : ∀ (s : Set α), IsAntichain (fun (x1 x2 : α) ↦ x1 ≤ x2) s → s.Finite) (f : ℕ → α),
    ∃ (m : ℕ) (n : ℕ), m < n ∧ (fun (x1 x2 : α) ↦ x1 ≤ x2) (f m) (f n)
Tactic: refine ⟨fun h ↦ ⟨h.to_wellFoundedLT, fun s ↦ h.finite_of_isAntichain⟩,
    fun ⟨hwf, hc⟩ ↦ ⟨fun f ↦ ?_⟩⟩
-- Lean 4 proof step from Mathlib.Order.WellQuasiOrder (goal)
Goal:
α : Type u_1
inst : Preorder α
h : WellFoundedLT α ∧ ∀ (s : Set α), IsAntichain (fun (x1 x2 : α) ↦ x1 ≤ x2) s → s.Finite
hwf : WellFoundedLT α
hc : ∀ (s : Set α), IsAntichain (fun (x1 x2 : α) ↦ x1 ≤ x2) s → s.Finite
f : ℕ → α
⊢ ∃ (m : ℕ) (n : ℕ), m < n ∧ (fun (x1 x2 : α) ↦ x1 ≤ x2) (f m) (f n)
have inl : ∀ (g : ℕ ↪o ℕ) (h1 : ∀ (m n : ℕ), m < n → f ((g : (a : ℕ) → ℕ) m) > f ((g : (a : ℕ) → ℕ) n)),
  ∃ (m : ℕ) (n : ℕ), m < n ∧ (fun (x1 x2 : α) ↦ x1 ≤ x2) (f m) (f n)
Tactic: obtain ⟨g, h1 | h2⟩ := exists_increasing_or_nonincreasing_subseq (· > ·) f
-- Lean 4 proof step from Mathlib.Order.WellQuasiOrder (goal)
Goal:
α : Type u_1
inst : Preorder α
h : WellFoundedLT α ∧ ∀ (s : Set α), IsAntichain (fun (x1 x2 : α) ↦ x1 ≤ x2) s → s.Finite
hwf : WellFoundedLT α
hc : ∀ (s : Set α), IsAntichain (fun (x1 x2 : α) ↦ x1 ≤ x2) s → s.Finite
f : ℕ → α
inl :
  ∀ (g : ℕ ↪o ℕ) (h1 : ∀ (m n : ℕ), m < n → f ((g : (a : ℕ) → ℕ) m) > f ((g : (a : ℕ) → ℕ) n)),
    ∃ (m : ℕ) (n : ℕ), m < n ∧ (fun (x1 x2 : α) ↦ x1 ≤ x2) (f m) (f n)
⊢ ∃ (m : ℕ) (n : ℕ), m < n ∧ (fun (x1 x2 : α) ↦ x1 ≤ x2) (f m) (f n)
have inr : ∀ (g : ℕ ↪o ℕ) (h2 : ∀ (m n : ℕ), m < n → ¬f ((g : (a : ℕ) → ℕ) m) > f ((g : (a : ℕ) → ℕ) n)),
  ∃ (m : ℕ) (n : ℕ), m < n ∧ (fun (x1 x2 : α) ↦ x1 ≤ x2) (f m) (f n)
Tactic: obtain ⟨g, h1 | h2⟩ := exists_increasing_or_nonincreasing_subseq (· > ·) f
-- Lean 4 proof step from Mathlib.Order.WellQuasiOrder (goal)
Goal:
α : Type u_1
inst : Preorder α
h : WellFoundedLT α ∧ ∀ (s : Set α), IsAntichain (fun (x1 x2 : α) ↦ x1 ≤ x2) s → s.Finite
hwf : WellFoundedLT α
hc : ∀ (s : Set α), IsAntichain (fun (x1 x2 : α) ↦ x1 ≤ x2) s → s.Finite
f : ℕ → α
g : ℕ ↪o ℕ
h1 : ∀ (m n : ℕ), m < n → f ((g : (a : ℕ) → ℕ) m) > f ((g : (a : ℕ) → ℕ) n)
⊢ ∃ (m : ℕ) (n : ℕ), m < n ∧ (fun (x1 x2 : α) ↦ x1 ≤ x2) (f m) (f n)
have inl : False
Tactic: exfalso
-- Lean 4 proof step from Mathlib.Order.WellQuasiOrder (goal)
Goal:
α : Type u_1
inst : Preorder α
h : WellFoundedLT α ∧ ∀ (s : Set α), IsAntichain (fun (x1 x2 : α) ↦ x1 ≤ x2) s → s.Finite
hwf : WellFoundedLT α
hc : ∀ (s : Set α), IsAntichain (fun (x1 x2 : α) ↦ x1 ≤ x2) s → s.Finite
f : ℕ → α
g : ℕ ↪o ℕ
h1 : ∀ (m n : ℕ), m < n → f ((g : (a : ℕ) → ℕ) m) > f ((g : (a : ℕ) → ℕ) n)
⊢ False
have apply : (fun (x1 x2 : ℕ) ↦ x1 > x2) ↪r fun (x1 x2 : α) ↦ x1 < x2
Tactic: apply RelEmbedding.not_wellFounded _ hwf.wf
-- Lean 4 proof step from Mathlib.Order.WellQuasiOrder (goal)
Goal:
α : Type u_1
inst : Preorder α
h : WellFoundedLT α ∧ ∀ (s : Set α), IsAntichain (fun (x1 x2 : α) ↦ x1 ≤ x2) s → s.Finite
hwf : WellFoundedLT α
hc : ∀ (s : Set α), IsAntichain (fun (x1 x2 : α) ↦ x1 ≤ x2) s → s.Finite
f : ℕ → α
g : ℕ ↪o ℕ
h2 : ∀ (m n : ℕ), m < n → ¬f ((g : (a : ℕ) → ℕ) m) > f ((g : (a : ℕ) → ℕ) n)
⊢ ∃ (m : ℕ) (n : ℕ), m < n ∧ (fun (x1 x2 : α) ↦ x1 ≤ x2) (f m) (f n)
have inr : ∀ (hc : ∀ (m n : ℕ) (_ : m < n), ¬f m ≤ f n), ∃ (s : Set α), IsAntichain (fun (x1 x2 : α) ↦ x1 ≤ x2) s ∧ s.Infinite
Tactic: contrapose! hc
Cleared hypotheses: hc
-- Lean 4 proof step from Mathlib.Order.WellQuasiOrder (goal)
Goal:
α : Type u_1
inst : Preorder α
h : WellFoundedLT α ∧ ∀ (s : Set α), IsAntichain (fun (x1 x2 : α) ↦ x1 ≤ x2) s → s.Finite
hwf : WellFoundedLT α
f : ℕ → α
g : ℕ ↪o ℕ
h2 : ∀ (m n : ℕ), m < n → ¬f ((g : (a : ℕ) → ℕ) m) > f ((g : (a : ℕ) → ℕ) n)
hc : ∀ (m n : ℕ) (_ : m < n), ¬f m ≤ f n
⊢ ∃ (s : Set α), IsAntichain (fun (x1 x2 : α) ↦ x1 ≤ x2) s ∧ s.Infinite
have inr : IsAntichain (fun (x1 x2 : α) ↦ x1 ≤ x2) (Set.range (ι := ℕ) (f ∘ (⇑g : (a : ℕ) → ℕ)))
Tactic: refine ⟨Set.range (f ∘ g), ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Order.WellQuasiOrder (goal)
Goal:
α : Type u_1
inst : Preorder α
h : WellFoundedLT α ∧ ∀ (s : Set α), IsAntichain (fun (x1 x2 : α) ↦ x1 ≤ x2) s → s.Finite
hwf : WellFoundedLT α
f : ℕ → α
g : ℕ ↪o ℕ
h2 : ∀ (m n : ℕ), m < n → ¬f ((g : (a : ℕ) → ℕ) m) > f ((g : (a : ℕ) → ℕ) n)
hc : ∀ (m n : ℕ) (_ : m < n), ¬f m ≤ f n
inr : IsAntichain (fun (x1 x2 : α) ↦ x1 ≤ x2) (Set.range (ι := ℕ) (f ∘ (⇑g : (a : ℕ) → ℕ)))
⊢ ∃ (s : Set α), IsAntichain (fun (x1 x2 : α) ↦ x1 ≤ x2) s ∧ s.Infinite
have inr₁ : (Set.range (ι := ℕ) (f ∘ (⇑g : (a : ℕ) → ℕ))).Infinite
Tactic: refine ⟨Set.range (f ∘ g), ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Order.WellQuasiOrder (goal)
Goal:
α : Type u_1
inst : Preorder α
h : WellFoundedLT α ∧ ∀ (s : Set α), IsAntichain (fun (x1 x2 : α) ↦ x1 ≤ x2) s → s.Finite
hwf : WellFoundedLT α
f : ℕ → α
g : ℕ ↪o ℕ
h2 : ∀ (m n : ℕ), m < n → ¬f ((g : (a : ℕ) → ℕ) m) > f ((g : (a : ℕ) → ℕ) n)
hc : ∀ (m n : ℕ) (_ : m < n), ¬f m ≤ f n
m n : ℕ
h_1 : (f ∘ (⇑g : (a : ℕ) → ℕ)) m ≠ (f ∘ (⇑g : (a : ℕ) → ℕ)) n
hf : (f ∘ (⇑g : (a : ℕ) → ℕ)) m ≤ (f ∘ (⇑g : (a : ℕ) → ℕ)) n
⊢ False
have inr : ∀ (h : m < n), False
Tactic: obtain h | rfl | h := lt_trichotomy m n
-- Lean 4 proof step from Mathlib.Order.WellQuasiOrder (goal)
Goal:
α : Type u_1
inst : Preorder α
h : WellFoundedLT α ∧ ∀ (s : Set α), IsAntichain (fun (x1 x2 : α) ↦ x1 ≤ x2) s → s.Finite
hwf : WellFoundedLT α
f : ℕ → α
g : ℕ ↪o ℕ
h2 : ∀ (m n : ℕ), m < n → ¬f ((g : (a : ℕ) → ℕ) m) > f ((g : (a : ℕ) → ℕ) n)
hc : ∀ (m n : ℕ) (_ : m < n), ¬f m ≤ f n
m n : ℕ
h_1 : (f ∘ (⇑g : (a : ℕ) → ℕ)) m ≠ (f ∘ (⇑g : (a : ℕ) → ℕ)) n
hf : (f ∘ (⇑g : (a : ℕ) → ℕ)) m ≤ (f ∘ (⇑g : (a : ℕ) → ℕ)) n
inr : ∀ (h : m < n), False
⊢ False
have inr₁ : (f ∘ (⇑g : (a : ℕ) → ℕ)) m ≠ (f ∘ (⇑g : (a : ℕ) → ℕ)) m →
  ∀ (hf : (f ∘ (⇑g : (a : ℕ) → ℕ)) m ≤ (f ∘ (⇑g : (a : ℕ) → ℕ)) m), False
Tactic: obtain h | rfl | h := lt_trichotomy m n
Cleared hypotheses: n, h_1, hf
-- Lean 4 proof step from Mathlib.Order.WellQuasiOrder (goal)
Goal:
α : Type u_1
inst : Preorder α
h : WellFoundedLT α ∧ ∀ (s : Set α), IsAntichain (fun (x1 x2 : α) ↦ x1 ≤ x2) s → s.Finite
hwf : WellFoundedLT α
f : ℕ → α
g : ℕ ↪o ℕ
h2 : ∀ (m n : ℕ), m < n → ¬f ((g : (a : ℕ) → ℕ) m) > f ((g : (a : ℕ) → ℕ) n)
hc : ∀ (m n : ℕ) (_ : m < n), ¬f m ≤ f n
m n : ℕ
h_1 : (f ∘ (⇑g : (a : ℕ) → ℕ)) m ≠ (f ∘ (⇑g : (a : ℕ) → ℕ)) n
hf : (f ∘ (⇑g : (a : ℕ) → ℕ)) m ≤ (f ∘ (⇑g : (a : ℕ) → ℕ)) n
inr : ∀ (h : m < n), False
inr₁ :
  (f ∘ (⇑g : (a : ℕ) → ℕ)) m ≠ (f ∘ (⇑g : (a : ℕ) → ℕ)) m →
    ∀ (hf : (f ∘ (⇑g : (a : ℕ) → ℕ)) m ≤ (f ∘ (⇑g : (a : ℕ) → ℕ)) m), False
⊢ False
have inr₂ : ∀ (h : n < m), False
Tactic: obtain h | rfl | h := lt_trichotomy m n
-- Lean 4 proof step from Mathlib.Order.WellQuasiOrder (goal)
Goal:
α : Type u_1
inst : Preorder α
h : WellFoundedLT α ∧ ∀ (s : Set α), IsAntichain (fun (x1 x2 : α) ↦ x1 ≤ x2) s → s.Finite
hwf : WellFoundedLT α
f : ℕ → α
g : ℕ ↪o ℕ
h2 : ∀ (m n : ℕ), m < n → ¬f ((g : (a : ℕ) → ℕ) m) > f ((g : (a : ℕ) → ℕ) n)
hc : ∀ (m n : ℕ) (_ : m < n), ¬f m ≤ f n
⊢ (Set.range (ι := ℕ) (f ∘ (⇑g : (a : ℕ) → ℕ))).Infinite
have inr : ∀ (m n : ℕ) (hf : f ((g : (a : ℕ) → ℕ) m) = f ((g : (a : ℕ) → ℕ) n)), m = n
Tactic: refine Set.infinite_range_of_injective fun m n (hf : f (g m) = f (g n)) ↦ ?_
-- Lean 4 proof step from Mathlib.Order.WellQuasiOrder (goal)
Goal:
α : Type u_1
inst : Preorder α
h : WellFoundedLT α ∧ ∀ (s : Set α), IsAntichain (fun (x1 x2 : α) ↦ x1 ≤ x2) s → s.Finite
hwf : WellFoundedLT α
f : ℕ → α
g : ℕ ↪o ℕ
h2 : ∀ (m n : ℕ), m < n → ¬f ((g : (a : ℕ) → ℕ) m) > f ((g : (a : ℕ) → ℕ) n)
hc : ∀ (m n : ℕ) (_ : m < n), ¬f m ≤ f n
m n : ℕ
hf : f ((g : (a : ℕ) → ℕ) m) = f ((g : (a : ℕ) → ℕ) n)
⊢ m = n
have inr : ∀ (h : m < n), m = n
Tactic: obtain h | rfl | h := lt_trichotomy m n
-- Lean 4 proof step from Mathlib.Order.WellQuasiOrder (goal)
Goal:
α : Type u_1
inst : Preorder α
h : WellFoundedLT α ∧ ∀ (s : Set α), IsAntichain (fun (x1 x2 : α) ↦ x1 ≤ x2) s → s.Finite
hwf : WellFoundedLT α
f : ℕ → α
g : ℕ ↪o ℕ
h2 : ∀ (m n : ℕ), m < n → ¬f ((g : (a : ℕ) → ℕ) m) > f ((g : (a : ℕ) → ℕ) n)
hc : ∀ (m n : ℕ) (_ : m < n), ¬f m ≤ f n
m n : ℕ
hf : f ((g : (a : ℕ) → ℕ) m) = f ((g : (a : ℕ) → ℕ) n)
inr : ∀ (h : m < n), m = n
⊢ m = n
have inr₁ : ∀ (hf : f ((g : (a : ℕ) → ℕ) m) = f ((g : (a : ℕ) → ℕ) m)), m = m
Tactic: obtain h | rfl | h := lt_trichotomy m n
Cleared hypotheses: n, hf
-- Lean 4 proof step from Mathlib.Order.WellQuasiOrder (goal)
Goal:
α : Type u_1
inst : Preorder α
h : WellFoundedLT α ∧ ∀ (s : Set α), IsAntichain (fun (x1 x2 : α) ↦ x1 ≤ x2) s → s.Finite
hwf : WellFoundedLT α
f : ℕ → α
g : ℕ ↪o ℕ
h2 : ∀ (m n : ℕ), m < n → ¬f ((g : (a : ℕ) → ℕ) m) > f ((g : (a : ℕ) → ℕ) n)
hc : ∀ (m n : ℕ) (_ : m < n), ¬f m ≤ f n
m n : ℕ
hf : f ((g : (a : ℕ) → ℕ) m) = f ((g : (a : ℕ) → ℕ) n)
inr : ∀ (h : m < n), m = n
inr₁ : ∀ (hf : f ((g : (a : ℕ) → ℕ) m) = f ((g : (a : ℕ) → ℕ) m)), m = m
⊢ m = n
have inr₂ : ∀ (h : n < m), m = n
Tactic: obtain h | rfl | h := lt_trichotomy m n
-- Lean 4 proof step from Mathlib.Order.WellQuasiOrder (goal)
Goal:
α : Type u_1
inst : LinearOrder α
⊢ WellQuasiOrderedLE α ↔ WellFoundedLT α
have rw : WellFoundedLT α → ∀ (s : Set α), IsAntichain (fun (x1 x2 : α) ↦ x1 ≤ x2) s → s.Finite
Tactic: rw [wellQuasiOrderedLE_iff, and_iff_left_iff_imp]
-- Lean 4 proof step from Mathlib.Order.WithBot (goal)
Goal:
α : Type u_1
d y : α
x : WithBot α
⊢ unbotD d x = y ↔ x = (↑y : WithBot α) ∨ x = ⊥ ∧ y = d
have bot : unbotD d ⊥ = y ↔ ⊥ = (↑y : WithBot α) ∨ Eq.{u_1 + 1} (α := WithBot α) ⊥ ⊥ ∧ y = d
Tactic: induction x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Order.WithBot (goal)
Goal:
α : Type u_1
d y : α
x : WithBot α
bot : unbotD d ⊥ = y ↔ ⊥ = (↑y : WithBot α) ∨ Eq.{u_1 + 1} (α := WithBot α) ⊥ ⊥ ∧ y = d
⊢ unbotD d x = y ↔ x = (↑y : WithBot α) ∨ x = ⊥ ∧ y = d
have coe : ∀ (a : α), unbotD d (↑a : WithBot α) = y ↔ (↑a : WithBot α) = (↑y : WithBot α) ∨ (↑a : WithBot α) = ⊥ ∧ y = d
Tactic: induction x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Order.WithBot (goal)
Goal:
α : Type u_1
d : α
x y : WithBot α
⊢ unbotD d x = unbotD d y ↔ x = y ∨ x = (↑d : WithBot α) ∧ y = ⊥ ∨ x = ⊥ ∧ y = (↑d : WithBot α)
have bot : unbotD d x = unbotD d ⊥ ↔
  x = ⊥ ∨ x = (↑d : WithBot α) ∧ Eq.{u_1 + 1} (α := WithBot α) ⊥ ⊥ ∨ x = ⊥ ∧ ⊥ = (↑d : WithBot α)
Tactic: induction y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Order.WithBot (goal)
Goal:
α : Type u_1
d : α
x y : WithBot α
bot :
  unbotD d x = unbotD d ⊥ ↔
    x = ⊥ ∨ x = (↑d : WithBot α) ∧ Eq.{u_1 + 1} (α := WithBot α) ⊥ ⊥ ∨ x = ⊥ ∧ ⊥ = (↑d : WithBot α)
⊢ unbotD d x = unbotD d y ↔ x = y ∨ x = (↑d : WithBot α) ∧ y = ⊥ ∨ x = ⊥ ∧ y = (↑d : WithBot α)
have coe : ∀ (a : α),
  unbotD d x = unbotD d (↑a : WithBot α) ↔
    x = (↑a : WithBot α) ∨ x = (↑d : WithBot α) ∧ (↑a : WithBot α) = ⊥ ∨ x = ⊥ ∧ (↑a : WithBot α) = (↑d : WithBot α)
Tactic: induction y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Order.WithBot (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
y : β
v : WithBot α
⊢ (↑y : WithBot β) = map f v ↔ ∃ (x : α), v = (↑x : WithBot α) ∧ f x = y
have bot : (↑y : WithBot β) = map f ⊥ ↔ ∃ (x : α), ⊥ = (↑x : WithBot α) ∧ f x = y
Tactic: cases v
Cleared hypotheses: v
-- Lean 4 proof step from Mathlib.Order.WithBot (goal)
Goal:
α : Type u_1
β : Type u_2
f : α → β
y : β
v : WithBot α
bot : (↑y : WithBot β) = map f ⊥ ↔ ∃ (x : α), ⊥ = (↑x : WithBot α) ∧ f x = y
⊢ (↑y : WithBot β) = map f v ↔ ∃ (x : α), v = (↑x : WithBot α) ∧ f x = y
have coe : ∀ (a : α), (↑y : WithBot β) = map f (↑a : WithBot α) ↔ ∃ (x : α), (↑a : WithBot α) = (↑x : WithBot α) ∧ f x = y
Tactic: cases v
Cleared hypotheses: v
-- Lean 4 proof step from Mathlib.Order.WithBot (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
a : WithBot α
⊢ map₂ f a ⊥ = ⊥
have bot : map₂ f ⊥ ⊥ = ⊥
Tactic: cases a
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Order.WithBot (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
a : WithBot α
bot : map₂ f ⊥ ⊥ = ⊥
⊢ map₂ f a ⊥ = ⊥
have coe : ∀ (a : α), map₂ f (↑a : WithBot α) ⊥ = ⊥
Tactic: cases a
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Order.WithBot (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
a : WithBot α
b : β
⊢ map₂ f a (↑b : WithBot β) = map (fun (x : α) ↦ f x b) a
have bot : map₂ f ⊥ (↑b : WithBot β) = map (fun (x : α) ↦ f x b) ⊥
Tactic: cases a
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Order.WithBot (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
a : WithBot α
b : β
bot : map₂ f ⊥ (↑b : WithBot β) = map (fun (x : α) ↦ f x b) ⊥
⊢ map₂ f a (↑b : WithBot β) = map (fun (x : α) ↦ f x b) a
have coe : ∀ (a : α), map₂ f (↑a : WithBot α) (↑b : WithBot β) = map (fun (x : α) ↦ f x b) (↑a : WithBot α)
Tactic: cases a
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Order.WithBot (goal)
Goal:
α : Type u_1
a : WithBot α
b : α
h : a ≠ ⊥
⊢ a.unbot h = b ↔ a = (↑b : WithBot α)
have bot : ∀ (h : Ne.{u_1 + 1} (α := WithBot α) ⊥ ⊥), unbot ⊥ h = b ↔ ⊥ = (↑b : WithBot α)
Tactic: induction a
Cleared hypotheses: a, h
-- Lean 4 proof step from Mathlib.Order.WithBot (goal)
Goal:
α : Type u_1
a : WithBot α
b : α
h : a ≠ ⊥
bot : ∀ (h : Ne.{u_1 + 1} (α := WithBot α) ⊥ ⊥), unbot ⊥ h = b ↔ ⊥ = (↑b : WithBot α)
⊢ a.unbot h = b ↔ a = (↑b : WithBot α)
have coe : ∀ (a : α) (h : (↑a : WithBot α) ≠ ⊥), (↑a : WithBot α).unbot h = b ↔ (↑a : WithBot α) = (↑b : WithBot α)
Tactic: induction a
Cleared hypotheses: a, h
-- Lean 4 proof step from Mathlib.Order.WithBot (goal)
Goal:
α : Type u_1
a : α
b : WithBot α
h : b ≠ ⊥
⊢ a = b.unbot h ↔ (↑a : WithBot α) = b
have bot : ∀ (h : Ne.{u_1 + 1} (α := WithBot α) ⊥ ⊥), a = unbot ⊥ h ↔ (↑a : WithBot α) = ⊥
Tactic: induction b
Cleared hypotheses: b, h
-- Lean 4 proof step from Mathlib.Order.WithBot (goal)
Goal:
α : Type u_1
a : α
b : WithBot α
h : b ≠ ⊥
bot : ∀ (h : Ne.{u_1 + 1} (α := WithBot α) ⊥ ⊥), a = unbot ⊥ h ↔ (↑a : WithBot α) = ⊥
⊢ a = b.unbot h ↔ (↑a : WithBot α) = b
have coe : ∀ (a_1 : α) (h : (↑a_1 : WithBot α) ≠ ⊥), a = (↑a_1 : WithBot α).unbot h ↔ (↑a : WithBot α) = (↑a_1 : WithBot α)
Tactic: induction b
Cleared hypotheses: b, h
-- Lean 4 proof step from Mathlib.Order.WithBot (goal)
Goal:
α : Type u_1
a b : WithBot α
ha : a ≠ ⊥
hb : b ≠ ⊥
⊢ a.unbot ha = b.unbot hb ↔ a = b
have rw : a = (↑(b.unbot hb) : WithBot α) ↔ a = b
Tactic: rw [unbot_eq_iff, coe_unbot]
-- Lean 4 proof step from Mathlib.Order.WithBot (goal)
Goal:
α : Type u_1
a b : WithBot α
ha : a ≠ ⊥
hb : b ≠ ⊥
rw : a = (↑(b.unbot hb) : WithBot α) ↔ a = b
⊢ a.unbot ha = b.unbot hb ↔ a = b
have rw₁ : a = b ↔ a = b
Tactic: rw [unbot_eq_iff, coe_unbot]
-- Lean 4 proof step from Mathlib.Order.WithBot (goal)
Goal:
α : Type u_1
inst : Nonempty α
a : WithBot α
ha : a ≠ ⊥
⊢ a.unbotA = a.unbot ha
have bot : ∀ (ha : Ne.{u_1 + 1} (α := WithBot α) ⊥ ⊥), unbotA ⊥ = unbot ⊥ ha
Tactic: cases a with
  | bot => contradiction
  | coe a => simp
Cleared hypotheses: a, ha
-- Lean 4 proof step from Mathlib.Order.WithBot (goal)
Goal:
α : Type u_1
inst : Nonempty α
a : WithBot α
ha : a ≠ ⊥
bot : ∀ (ha : Ne.{u_1 + 1} (α := WithBot α) ⊥ ⊥), unbotA ⊥ = unbot ⊥ ha
⊢ a.unbotA = a.unbot ha
have coe : ∀ (a : α) (ha : (↑a : WithBot α) ≠ ⊥), (↑a : WithBot α).unbotA = (↑a : WithBot α).unbot ha
Tactic: cases a with
  | bot => contradiction
  | coe a => simp
Cleared hypotheses: a, ha
-- Lean 4 proof step from Mathlib.Order.WithBot (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
e : α ≃ β
x : WithBot α
⊢ WithBot.map.{u_2, u_1} (α := β) (⇑e.symm : (a : β) → α) (WithBot.map (⇑e : (a : α) → β) x) = x
have bot : Eq.{u_1 + 1} (α := WithBot α)
  (WithBot.map.{u_2, u_1} (α := β) (⇑e.symm : (a : β) → α) (WithBot.map.{u_1, u_2} (α := α) (⇑e : (a : α) → β) ⊥)) ⊥
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Order.WithBot (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
e : α ≃ β
x : WithBot α
bot :
  Eq.{u_1 + 1} (α := WithBot α)
    (WithBot.map.{u_2, u_1} (α := β) (⇑e.symm : (a : β) → α) (WithBot.map.{u_1, u_2} (α := α) (⇑e : (a : α) → β) ⊥)) ⊥
⊢ WithBot.map.{u_2, u_1} (α := β) (⇑e.symm : (a : β) → α) (WithBot.map (⇑e : (a : α) → β) x) = x
have coe : ∀ (a : α),
  WithBot.map.{u_2, u_1} (α := β) (⇑e.symm : (a : β) → α) (WithBot.map (⇑e : (a : α) → β) (↑a : WithBot α)) =
    (↑a : WithBot α)
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Order.WithBot (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
e : α ≃ β
x : WithBot β
⊢ WithBot.map.{u_1, u_2} (α := α) (⇑e : (a : α) → β) (WithBot.map (⇑e.symm : (a : β) → α) x) = x
have bot : Eq.{u_2 + 1} (α := WithBot β)
  (WithBot.map.{u_1, u_2} (α := α) (⇑e : (a : α) → β) (WithBot.map.{u_2, u_1} (α := β) (⇑e.symm : (a : β) → α) ⊥)) ⊥
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Order.WithBot (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
e : α ≃ β
x : WithBot β
bot :
  Eq.{u_2 + 1} (α := WithBot β)
    (WithBot.map.{u_1, u_2} (α := α) (⇑e : (a : α) → β) (WithBot.map.{u_2, u_1} (α := β) (⇑e.symm : (a : β) → α) ⊥)) ⊥
⊢ WithBot.map.{u_1, u_2} (α := α) (⇑e : (a : α) → β) (WithBot.map (⇑e.symm : (a : β) → α) x) = x
have coe : ∀ (a : β),
  WithBot.map.{u_1, u_2} (α := α) (⇑e : (a : α) → β) (WithBot.map (⇑e.symm : (a : β) → α) (↑a : WithBot β)) =
    (↑a : WithBot β)
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Order.WithBot (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
e₁ : α ≃ β
e₂ : β ≃ γ
⊢ (e₁.trans e₂).withBotCongr = e₁.withBotCongr.trans e₂.withBotCongr
have H : ∀ (x : WithBot α),
  Eq.{u_3 + 1} (α := WithBot γ) (((e₁.trans e₂).withBotCongr : (a : WithBot α) → WithBot γ) x : WithBot γ)
    ((e₁.withBotCongr.trans e₂.withBotCongr : (a : WithBot α) → WithBot γ) x : WithBot γ)
Tactic: ext x
-- Lean 4 proof step from Mathlib.Order.WithBot (goal)
Goal:
α : Type u_1
inst : LE α
x y : WithBot α
⊢ x ≤ y ↔ ∀ (a : α), x = (↑a : WithBot α) → ∃ (b : α), y = (↑b : WithBot α) ∧ a ≤ b
have bot : ⊥ ≤ y ↔ ∀ (a : α), ⊥ = (↑a : WithBot α) → ∃ (b : α), y = (↑b : WithBot α) ∧ a ≤ b
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Order.WithBot (goal)
Goal:
α : Type u_1
inst : LE α
x y : WithBot α
bot : ⊥ ≤ y ↔ ∀ (a : α), ⊥ = (↑a : WithBot α) → ∃ (b : α), y = (↑b : WithBot α) ∧ a ≤ b
⊢ x ≤ y ↔ ∀ (a : α), x = (↑a : WithBot α) → ∃ (b : α), y = (↑b : WithBot α) ∧ a ≤ b
have coe : ∀ (a : α),
  (↑a : WithBot α) ≤ y ↔ ∀ (a_1 : α), (↑a : WithBot α) = (↑a_1 : WithBot α) → ∃ (b : α), y = (↑b : WithBot α) ∧ a_1 ≤ b
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Order.WithBot (goal)
Goal:
α : Type u_1
inst : LE α
y : WithBot α
⊢ ⊥ ≤ y ↔ ∀ (a : α), ⊥ = (↑a : WithBot α) → ∃ (b : α), y = (↑b : WithBot α) ∧ a ≤ b
have bot : LE.le.{u_1} (α := WithBot α) ⊥ ⊥ ↔ ∀ (a : α), ⊥ = (↑a : WithBot α) → ∃ (b : α), ⊥ = (↑b : WithBot α) ∧ a ≤ b
Tactic: cases y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Order.WithBot (goal)
Goal:
α : Type u_1
inst : LE α
y : WithBot α
bot : LE.le.{u_1} (α := WithBot α) ⊥ ⊥ ↔ ∀ (a : α), ⊥ = (↑a : WithBot α) → ∃ (b : α), ⊥ = (↑b : WithBot α) ∧ a ≤ b
⊢ ⊥ ≤ y ↔ ∀ (a : α), ⊥ = (↑a : WithBot α) → ∃ (b : α), y = (↑b : WithBot α) ∧ a ≤ b
have bot₁ : ∀ (a : α),
  ⊥ ≤ (↑a : WithBot α) ↔ ∀ (a_1 : α), ⊥ = (↑a_1 : WithBot α) → ∃ (b : α), (↑a : WithBot α) = (↑b : WithBot α) ∧ a_1 ≤ b
Tactic: cases y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Order.WithBot (goal)
Goal:
α : Type u_1
inst : LE α
y : WithBot α
a : α
⊢ (↑a : WithBot α) ≤ y ↔ ∀ (a_1 : α), (↑a : WithBot α) = (↑a_1 : WithBot α) → ∃ (b : α), y = (↑b : WithBot α) ∧ a_1 ≤ b
have coe : (↑a : WithBot α) ≤ ⊥ ↔ ∀ (a_1 : α), (↑a : WithBot α) = (↑a_1 : WithBot α) → ∃ (b : α), ⊥ = (↑b : WithBot α) ∧ a_1 ≤ b
Tactic: cases y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Order.WithBot (goal)
Goal:
α : Type u_1
inst : LE α
y : WithBot α
a : α
coe :
  (↑a : WithBot α) ≤ ⊥ ↔ ∀ (a_1 : α), (↑a : WithBot α) = (↑a_1 : WithBot α) → ∃ (b : α), ⊥ = (↑b : WithBot α) ∧ a_1 ≤ b
⊢ (↑a : WithBot α) ≤ y ↔ ∀ (a_1 : α), (↑a : WithBot α) = (↑a_1 : WithBot α) → ∃ (b : α), y = (↑b : WithBot α) ∧ a_1 ≤ b
have coe₁ : ∀ (a_1 : α),
  (↑a : WithBot α) ≤ (↑a_1 : WithBot α) ↔
    ∀ (a_2 : α), (↑a : WithBot α) = (↑a_2 : WithBot α) → ∃ (b : α), (↑a_1 : WithBot α) = (↑b : WithBot α) ∧ a_2 ≤ b
Tactic: cases y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Order.WithBot (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst : LE α
x_1 y : WithBot α
inst_1 : OrderTop α
x : WithBot α
⊢ x ≤ ⊤
have bot : LE.le.{u_1} (α := WithBot α) ⊥ ⊤
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Order.WithBot (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst : LE α
x_1 y : WithBot α
inst_1 : OrderTop α
x : WithBot α
bot : LE.le.{u_1} (α := WithBot α) ⊥ ⊤
⊢ x ≤ ⊤
have coe : ∀ (a : α), (↑a : WithBot α) ≤ ⊤
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Order.WithBot (goal)
Goal:
α : Type u_1
a : α
inst : LE α
h : IsMax a
x : WithBot α
⊢ (↑a : WithBot α) ≤ x → x ≤ (↑a : WithBot α)
have bot : (↑a : WithBot α) ≤ ⊥ → ⊥ ≤ (↑a : WithBot α)
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Order.WithBot (goal)
Goal:
α : Type u_1
a : α
inst : LE α
h : IsMax a
x : WithBot α
bot : (↑a : WithBot α) ≤ ⊥ → ⊥ ≤ (↑a : WithBot α)
⊢ (↑a : WithBot α) ≤ x → x ≤ (↑a : WithBot α)
have coe : ∀ (a_1 : α), (↑a : WithBot α) ≤ (↑a_1 : WithBot α) → (↑a_1 : WithBot α) ≤ (↑a : WithBot α)
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Order.WithBot (goal)
Goal:
α : Type u_1
a : α
inst : LE α
h : IsMax a
a_1 : α
⊢ (↑a : WithBot α) ≤ (↑a_1 : WithBot α) → (↑a_1 : WithBot α) ≤ (↑a : WithBot α)
have coe : a ≤ a_1 → a_1 ≤ a
Tactic: simp
-- Lean 4 proof step from Mathlib.Order.WithBot (goal)
Goal:
α : Type u_1
a : α
inst : LE α
x : WithBot α
hx : x ≠ ⊥
⊢ a ≤ x.unbot hx ↔ (↑a : WithBot α) ≤ x
have lift : ∀ (x : α) (hx : (↑x : WithBot α) ≠ ⊥), a ≤ (↑x : WithBot α).unbot hx ↔ (↑a : WithBot α) ≤ (↑x : WithBot α)
Tactic: lift x to α using hx
Cleared hypotheses: x, hx