awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.WellQuasiOrder
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)
inr :
  ∀ (hc : ∀ (m n : ℕ) (_ : m < n), ¬f m ≤ f n), ∃ (s : Set α), IsAntichain (fun (x1 x2 : α) ↦ x1 ≤ x2) s ∧ s.Infinite
⊢ ∃ (m : ℕ) (n : ℕ), m < n ∧ (fun (x1 x2 : α) ↦ x1 ≤ x2) (f m) (f n)

Tactic:
contrapose! hc
-- Module: Mathlib.Order.WellQuasiOrder
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

Tactic:
⟨Set.range (f ∘ g), ?_, ?_⟩

Premises used: Function.comp, And.intro, Exists.intro, Set.range, DFunLike.coe
-- Module: Mathlib.Order.WellQuasiOrder
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 : ℕ) → ℕ)))
inr₁ : (Set.range (ι := ℕ) (f ∘ (⇑g : (a : ℕ) → ℕ))).Infinite
⊢ ∃ (s : Set α), IsAntichain (fun (x1 x2 : α) ↦ x1 ≤ x2) s ∧ s.Infinite

Tactic:
refine ⟨Set.range (f ∘ g), ?_, ?_⟩
-- Module: Mathlib.Order.WellQuasiOrder
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
inr₂ : ∀ (h : n < m), False
⊢ False

Tactic:
obtain h | rfl | h := lt_trichotomy m n

Premises used: rfl, lt_trichotomy
-- Module: Mathlib.Order.WellQuasiOrder
Goal:
α : Type u_1
inst : Preorder α
h_1 : 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_2 : (f ∘ (⇑g : (a : ℕ) → ℕ)) m ≠ (f ∘ (⇑g : (a : ℕ) → ℕ)) n
hf : (f ∘ (⇑g : (a : ℕ) → ℕ)) m ≤ (f ∘ (⇑g : (a : ℕ) → ℕ)) n
h : m < n
⊢ False

Tactic:
hc _ _ (g.strictMono h) hf

Premises used: OrderEmbedding.strictMono
-- Module: Mathlib.Order.WellQuasiOrder
Goal:
α : Type u_1
inst : Preorder α
h_1 : 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_2 : (f ∘ (⇑g : (a : ℕ) → ℕ)) m ≠ (f ∘ (⇑g : (a : ℕ) → ℕ)) n
hf : (f ∘ (⇑g : (a : ℕ) → ℕ)) m ≤ (f ∘ (⇑g : (a : ℕ) → ℕ)) n
h : m < n
⊢ False

Tactic:
exact hc _ _ (g.strictMono h) hf

Premises used: OrderEmbedding.strictMono
-- Module: Mathlib.Order.WellQuasiOrder
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 : ℕ
h_1 : (f ∘ (⇑g : (a : ℕ) → ℕ)) m ≠ (f ∘ (⇑g : (a : ℕ) → ℕ)) m
hf : (f ∘ (⇑g : (a : ℕ) → ℕ)) m ≤ (f ∘ (⇑g : (a : ℕ) → ℕ)) m
⊢ False

Tactic:
contradiction
-- Module: Mathlib.Order.WellQuasiOrder
Goal:
α : Type u_1
inst : Preorder α
h_1 : 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_2 : (f ∘ (⇑g : (a : ℕ) → ℕ)) m ≠ (f ∘ (⇑g : (a : ℕ) → ℕ)) n
hf : (f ∘ (⇑g : (a : ℕ) → ℕ)) m ≤ (f ∘ (⇑g : (a : ℕ) → ℕ)) n
h : n < m
⊢ False

Tactic:
h2 _ _ h (lt_of_le_not_ge hf (hc _ _ (g.strictMono h)))

Premises used: OrderEmbedding.strictMono, lt_of_le_not_ge
-- Module: Mathlib.Order.WellQuasiOrder
Goal:
α : Type u_1
inst : Preorder α
h_1 : 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_2 : (f ∘ (⇑g : (a : ℕ) → ℕ)) m ≠ (f ∘ (⇑g : (a : ℕ) → ℕ)) n
hf : (f ∘ (⇑g : (a : ℕ) → ℕ)) m ≤ (f ∘ (⇑g : (a : ℕ) → ℕ)) n
h : n < m
⊢ False

Tactic:
exact h2 _ _ h (lt_of_le_not_ge hf (hc _ _ (g.strictMono h)))

Premises used: OrderEmbedding.strictMono, lt_of_le_not_ge
-- Module: Mathlib.Order.WellQuasiOrder
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

Tactic:
Set.infinite_range_of_injective fun m n (hf : f (g m) = f (g n)) ↦ ?_

Premises used: Set.infinite_range_of_injective
-- Module: Mathlib.Order.WellQuasiOrder
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 : ∀ (m n : ℕ) (hf : f ((g : (a : ℕ) → ℕ) m) = f ((g : (a : ℕ) → ℕ) n)), m = n
⊢ (Set.range (ι := ℕ) (f ∘ (⇑g : (a : ℕ) → ℕ))).Infinite

Tactic:
refine Set.infinite_range_of_injective fun m n (hf : f (g m) = f (g n)) ↦ ?_

Premises used: Set.infinite_range_of_injective
-- Module: Mathlib.Order.WellQuasiOrder
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
inr₂ : ∀ (h : n < m), m = n
⊢ m = n

Tactic:
obtain h | rfl | h := lt_trichotomy m n

Premises used: rfl, lt_trichotomy
-- Module: Mathlib.Order.WellQuasiOrder
Goal:
α : Type u_1
inst : Preorder α
h_1 : 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)
h : m < n
⊢ m = n

Tactic:
cases (hf ▸ hc _ _ (g.strictMono h)) le_rfl
-- Module: Mathlib.Order.WellQuasiOrder
Goal:
α : Type u_1
inst : Preorder α
h_1 : 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)
h : m < n
⊢ m = n

Tactic:
first | rfl | cases (hf ▸ hc _ _ (g.strictMono h)) le_rfl
-- Module: Mathlib.Order.WellQuasiOrder
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 : ℕ
hf : f ((g : (a : ℕ) → ℕ) m) = f ((g : (a : ℕ) → ℕ) m)
⊢ m = m

Tactic:
rfl
-- Module: Mathlib.Order.WellQuasiOrder
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 : ℕ
hf : f ((g : (a : ℕ) → ℕ) m) = f ((g : (a : ℕ) → ℕ) m)
⊢ m = m

Tactic:
first | rfl | cases (hf ▸ hc _ _ (g.strictMono h)) le_rfl
-- Module: Mathlib.Order.WellQuasiOrder
Goal:
α : Type u_1
inst : Preorder α
h_1 : 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)
h : n < m
⊢ m = n

Tactic:
cases (hf ▸ hc _ _ (g.strictMono h)) le_rfl
-- Module: Mathlib.Order.WellQuasiOrder
Goal:
α : Type u_1
inst : Preorder α
h_1 : 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)
h : n < m
⊢ m = n

Tactic:
first | rfl | cases (hf ▸ hc _ _ (g.strictMono h)) le_rfl
-- Module: Mathlib.Order.WellQuasiOrder
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst : Preorder α
inst_1 : WellQuasiOrderedLE α
inst_2 : Preorder β
inst_3 : WellQuasiOrderedLE β
⊢ WellQuasiOrderedLE (α × β)

Tactic:
⟨wellQuasiOrdered_le.prod wellQuasiOrdered_le⟩

Premises used: WellQuasiOrdered.prod, WellQuasiOrderedLE.mk, wellQuasiOrdered_le
-- Module: Mathlib.Order.WellQuasiOrder
Goal:
α : Type u_1
inst : LinearOrder α
rw : WellFoundedLT α → ∀ (s : Set α), IsAntichain (fun (x1 x2 : α) ↦ x1 ≤ x2) s → s.Finite
⊢ WellQuasiOrderedLE α ↔ WellFoundedLT α

Tactic:
rw [wellQuasiOrderedLE_iff, and_iff_left_iff_imp]

Premises used: wellQuasiOrderedLE_iff, and_iff_left_iff_imp
-- Module: Mathlib.Order.WellQuasiOrder
Goal:
α : Type u_1
inst : LinearOrder α
⊢ WellFoundedLT α → ∀ (s : Set α), IsAntichain (fun (x1 x2 : α) ↦ x1 ≤ x2) s → s.Finite

Tactic:
fun _ s hs ↦ hs.subsingleton.finite

Premises used: IsAntichain.subsingleton, Set.Subsingleton.finite
-- Module: Mathlib.Order.WellQuasiOrder
Goal:
α : Type u_1
inst : LinearOrder α
⊢ WellFoundedLT α → ∀ (s : Set α), IsAntichain (fun (x1 x2 : α) ↦ x1 ≤ x2) s → s.Finite

Tactic:
exact fun _ s hs ↦ hs.subsingleton.finite
-- Module: Mathlib.Order.WellQuasiOrder
Goal:
α : Type u_1
β : Type u_2
r : α → α → Prop
s : β → β → Prop
inst : LinearOrder α
h : WellFoundedLT α
⊢ WellQuasiOrderedLE α

Tactic:
wellQuasiOrderedLE_iff_wellFoundedLT.mpr h

Premises used: Iff.mpr, wellQuasiOrderedLE_iff_wellFoundedLT
-- Module: Mathlib.Order.WellQuasiOrder
Goal:
α_1 : Type u_1
β : Type u_2
r : α_1 → α_1 → Prop
s : β → β → Prop
ι : Type u_3
α : ι → Type u_4
inst : (i : ι) → Preorder (α i)
h : ∀ (i : ι), WellQuasiOrderedLE.{u_4} (α i)
inst_1 : Finite ι
⊢ WellQuasiOrderedLE ((i : ι) → α i)

Tactic:
⟨WellQuasiOrdered.pi fun i => (h i).wqo⟩

Premises used: WellQuasiOrderedLE.mk, WellQuasiOrderedLE.wqo, WellQuasiOrdered.pi
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
a b : α
inst : Nonempty α
⊢ Nontrivial.{u_1} (WithBot α)

Tactic:
inferInstanceAs <| Nontrivial (Option α)

Premises used: _private.0.WithBot.nontrivial._proof_1
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
⊢ Injective.{u_1 + 1, u_1 + 1} (α := α) some

Tactic:
Option.some_injective _

Premises used: WithBot.some, WithBot, Option.some_injective
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
a b : α
⊢ (↑a : WithBot α) = (↑b : WithBot α) ↔ a = b

Tactic:
Option.some_inj

Premises used: WithBot.some, WithBot, Option.some_inj
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
p : WithBot α → Prop
⊢ (∀ (x : WithBot α), p x) ↔ p ⊥ ∧ ∀ (x : α), p (↑x : WithBot α)

Tactic:
Option.forall

Premises used: WithBot.some, WithBot, Option.forall
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
p : WithBot α → Prop
⊢ (∃ (x : WithBot α), p x) ↔ p ⊥ ∨ ∃ (x : α), p (↑x : WithBot α)

Tactic:
Option.exists

Premises used: WithBot.some, WithBot, Option.exists
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
⊢ Eq.{u_1 + 1} (α := Option α) none ⊥

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
a : α
⊢ Option.some a = (↑a : WithBot α)

Tactic:
rfl

Premises used: WithBot.some, rfl
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
a : α
⊢ ⊥ ≠ (↑a : WithBot α)

Tactic:
nofun

Premises used: False, _private.0.WithBot.bot_ne_coe.match_1, Not
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
a : α
⊢ (↑a : WithBot α) ≠ ⊥

Tactic:
nofun

Premises used: False, _private.0.WithBot.coe_ne_bot.match_1, Not
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_5
d : α
⊢ unbotD d ⊥ = d

Tactic:
rfl

Premises used: WithBot.recBotCoe, WithBot.unbotD, rfl
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_5
d x : α
⊢ unbotD d (↑x : WithBot α) = x

Tactic:
rfl

Premises used: WithBot.recBotCoe, WithBot.unbotD, rfl
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
a b : α
⊢ (↑a : WithBot α) = (↑b : WithBot α) ↔ a = b

Tactic:
coe_inj

Premises used: WithBot.coe_inj
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
d y : α
x : WithBot α
bot : unbotD d ⊥ = y ↔ ⊥ = (↑y : WithBot α) ∨ Eq.{u_1 + 1} (α := WithBot α) ⊥ ⊥ ∧ y = d
coe : ∀ (a : α), unbotD d (↑a : WithBot α) = y ↔ (↑a : WithBot α) = (↑y : WithBot α) ∨ (↑a : WithBot α) = ⊥ ∧ y = d
⊢ unbotD d x = y ↔ x = (↑y : WithBot α) ∨ x = ⊥ ∧ y = d

Tactic:
induction x
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
d y : α
⊢ unbotD d ⊥ = y ↔ ⊥ = (↑y : WithBot α) ∨ Eq.{u_1 + 1} (α := WithBot α) ⊥ ⊥ ∧ y = d

Tactic:
simp [@eq_comm _ d]

Premises used: eq_comm
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
d y a : α
⊢ unbotD d (↑a : WithBot α) = y ↔ (↑a : WithBot α) = (↑y : WithBot α) ∨ (↑a : WithBot α) = ⊥ ∧ y = d

Tactic:
simp [@eq_comm _ d]

Premises used: eq_comm
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
d : α
x : WithBot α
⊢ unbotD d x = d ↔ x = (↑d : WithBot α) ∨ x = ⊥

Tactic:
simp [unbotD_eq_iff]

Premises used: WithBot.unbotD_eq_iff
-- Module: Mathlib.Order.WithBot
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 α)
coe :
  ∀ (a : α),
    unbotD d x = unbotD d (↑a : WithBot α) ↔
      x = (↑a : WithBot α) ∨ x = (↑d : WithBot α) ∧ (↑a : WithBot α) = ⊥ ∨ x = ⊥ ∧ (↑a : WithBot α) = (↑d : WithBot α)
⊢ unbotD d x = unbotD d y ↔ x = y ∨ x = (↑d : WithBot α) ∧ y = ⊥ ∨ x = ⊥ ∧ y = (↑d : WithBot α)

Tactic:
induction y
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
d : α
x : WithBot α
⊢ unbotD d x = unbotD d ⊥ ↔
    x = ⊥ ∨ x = (↑d : WithBot α) ∧ Eq.{u_1 + 1} (α := WithBot α) ⊥ ⊥ ∨ x = ⊥ ∧ ⊥ = (↑d : WithBot α)

Tactic:
simp [unbotD_eq_iff, or_comm]

Premises used: WithBot.unbotD_eq_iff, or_comm
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
d : α
x : WithBot α
a : α
⊢ unbotD d x = unbotD d (↑a : WithBot α) ↔
    x = (↑a : WithBot α) ∨ x = (↑d : WithBot α) ∧ (↑a : WithBot α) = ⊥ ∨ x = ⊥ ∧ (↑a : WithBot α) = (↑d : WithBot α)

Tactic:
simp [unbotD_eq_iff, or_comm]

Premises used: WithBot.unbotD_eq_iff, or_comm
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
β : Type u_2
f : α → β
⊢ map f ⊥ = ⊥

Tactic:
rfl

Premises used: WithBot.map, rfl
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
β : Type u_2
f : α → β
a : α
⊢ map f (↑a : WithBot α) = (↑(f a) : WithBot β)

Tactic:
rfl

Premises used: WithBot.some, WithBot.map, rfl
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
β : Type u_2
f : α → β
a : WithBot α
⊢ map f a = ⊥ ↔ a = ⊥

Tactic:
Option.map_eq_none_iff

Premises used: WithBot, Option.map_eq_none_iff, WithBot.map
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
β : Type u_2
f : α → β
y : β
v : WithBot α
⊢ map f v = (↑y : WithBot β) ↔ ∃ (x : α), v = (↑x : WithBot α) ∧ f x = y

Tactic:
Option.map_eq_some_iff

Premises used: WithBot.some, WithBot, WithBot.map, Option.map_eq_some_iff
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
β : Type u_2
f : α → β
y : β
v : WithBot α
bot : (↑y : WithBot β) = map f ⊥ ↔ ∃ (x : α), ⊥ = (↑x : WithBot α) ∧ f x = y
coe : ∀ (a : α), (↑y : WithBot β) = map f (↑a : WithBot α) ↔ ∃ (x : α), (↑a : WithBot α) = (↑x : WithBot α) ∧ f x = y
⊢ (↑y : WithBot β) = map f v ↔ ∃ (x : α), v = (↑x : WithBot α) ∧ f x = y

Tactic:
cases v
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
β : Type u_2
f : α → β
y : β
⊢ (↑y : WithBot β) = map f ⊥ ↔ ∃ (x : α), ⊥ = (↑x : WithBot α) ∧ f x = y

Tactic:
simp [eq_comm]

Premises used: eq_comm
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
β : Type u_2
f : α → β
y : β
a : α
⊢ (↑y : WithBot β) = map f (↑a : WithBot α) ↔ ∃ (x : α), (↑a : WithBot α) = (↑x : WithBot α) ∧ f x = y

Tactic:
simp [eq_comm]

Premises used: eq_comm
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
⊢ Eq.{u_1 + 1} (α := WithBot α → WithBot α) (map id) id

Tactic:
Option.map_id

Premises used: WithBot, WithBot.map, Option.map_id
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
h : β → γ
g : α → β
a : WithBot α
⊢ map h (map g a) = map (h ∘ g) a

Tactic:
Option.map_map h g a

Premises used: WithBot, Option.map_map, WithBot.map
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
h : β → γ
g : α → β
x : WithBot α
⊢ map (h ∘ g) x = map h (map g x)

Tactic:
(map_map ..).symm

Premises used: WithBot.map_map, Eq.symm
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
g : β → γ
⊢ map g ∘ map f = map (g ∘ f)

Tactic:
Option.map_comp_map f g

Premises used: WithBot, Option.map_comp_map, WithBot.map
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
f₁ : α → β
f₂ : α → γ
g₁ : β → δ
g₂ : γ → δ
h : g₁ ∘ f₁ = g₂ ∘ f₂
a : α
⊢ map g₁ (map f₁ (↑a : WithBot α)) = map g₂ (map f₂ (↑a : WithBot α))

Tactic:
Option.map_comm h _

Premises used: WithBot.some, WithBot, Option.map_comm, WithBot.map
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
β : Type u_2
f : α → β
Hf : Injective f
⊢ Injective (map f)

Tactic:
Option.map_injective Hf

Premises used: Option.map_injective, WithBot, WithBot.map
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
a : α
b : β
⊢ map₂ f (↑a : WithBot α) (↑b : WithBot β) = (↑(f a b) : WithBot γ)

Tactic:
rfl

Premises used: WithBot.some, WithBot.map₂, rfl, Option.map₂
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
b : WithBot β
⊢ map₂ f ⊥ b = ⊥

Tactic:
rfl

Premises used: WithBot.map₂, rfl, Option.map₂
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
a : WithBot α
bot : map₂ f ⊥ ⊥ = ⊥
coe : ∀ (a : α), map₂ f (↑a : WithBot α) ⊥ = ⊥
⊢ map₂ f a ⊥ = ⊥

Tactic:
cases a
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
⊢ map₂ f ⊥ ⊥ = ⊥

Tactic:
rfl
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
a : α
⊢ map₂ f (↑a : WithBot α) ⊥ = ⊥

Tactic:
rfl
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
a : α
b : WithBot β
⊢ map₂ f (↑a : WithBot α) b = map (fun (b : β) ↦ f a b) b

Tactic:
rfl

Premises used: WithBot.map, WithBot.map₂, rfl
-- Module: Mathlib.Order.WithBot
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) ⊥
coe : ∀ (a : α), map₂ f (↑a : WithBot α) (↑b : WithBot β) = map (fun (x : α) ↦ f x b) (↑a : WithBot α)
⊢ map₂ f a (↑b : WithBot β) = map (fun (x : α) ↦ f x b) a

Tactic:
cases a
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
b : β
⊢ map₂ f ⊥ (↑b : WithBot β) = map (fun (x : α) ↦ f x b) ⊥

Tactic:
rfl
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
b : β
a : α
⊢ map₂ f (↑a : WithBot α) (↑b : WithBot β) = map (fun (x : α) ↦ f x b) (↑a : WithBot α)

Tactic:
rfl
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
a : WithBot α
b : WithBot β
⊢ map₂ f a b = ⊥ ↔ a = ⊥ ∨ b = ⊥

Tactic:
Option.map₂_eq_none_iff

Premises used: WithBot, Option.map₂_eq_none_iff, WithBot.map₂
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
x : WithBot α
⊢ x ≠ ⊥ ↔ ∃ (a : α), (↑a : WithBot α) = x

Tactic:
Option.ne_none_iff_exists

Premises used: WithBot.some, WithBot, Option.ne_none_iff_exists
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
x : WithBot α
⊢ x = ⊥ ↔ ∀ (a : α), (↑a : WithBot α) ≠ x

Tactic:
Option.eq_none_iff_forall_some_ne

Premises used: WithBot.some, WithBot, Option.eq_none_iff_forall_some_ne
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
p : WithBot α → Prop
⊢ (∀ (x : WithBot α), x ≠ ⊥ → p x) ↔ ∀ (x : α), p (↑x : WithBot α)

Tactic:
simp [ne_bot_iff_exists]

Premises used: WithBot.ne_bot_iff_exists
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
p : WithBot α → Prop
⊢ (∃ (x : WithBot α), x ≠ ⊥ ∧ p x) ↔ ∃ (x : α), p (↑x : WithBot α)

Tactic:
simp [ne_bot_iff_exists]

Premises used: WithBot.ne_bot_iff_exists
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
x : α
h : (↑x : WithBot α) ≠ ⊥
⊢ (↑x : WithBot α).unbot h = x

Tactic:
rfl

Premises used: WithBot.unbot, rfl
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
inst : Top α
⊢ Eq.{u_1 + 1} (α := WithBot α) (↑⊤ : WithBot α) ⊤

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
inst : Top α
a : α
⊢ (↑a : WithBot α) = ⊤ ↔ a = ⊤

Tactic:
coe_eq_coe

Premises used: WithBot.coe_eq_coe
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
inst : Top α
a : α
⊢ ⊤ = (↑a : WithBot α) ↔ ⊤ = a

Tactic:
coe_eq_coe

Premises used: WithBot.coe_eq_coe
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
a : WithBot α
b : α
h : a ≠ ⊥
bot : ∀ (h : Ne.{u_1 + 1} (α := WithBot α) ⊥ ⊥), unbot ⊥ h = b ↔ ⊥ = (↑b : WithBot α)
coe : ∀ (a : α) (h : (↑a : WithBot α) ≠ ⊥), (↑a : WithBot α).unbot h = b ↔ (↑a : WithBot α) = (↑b : WithBot α)
⊢ a.unbot h = b ↔ a = (↑b : WithBot α)

Tactic:
induction a
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
b : α
h : Ne.{u_1 + 1} (α := WithBot α) ⊥ ⊥
⊢ unbot ⊥ h = b ↔ ⊥ = (↑b : WithBot α)

Tactic:
simpa using h rfl

Premises used: rfl
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
b a : α
h : (↑a : WithBot α) ≠ ⊥
⊢ (↑a : WithBot α).unbot h = b ↔ (↑a : WithBot α) = (↑b : WithBot α)

Tactic:
simp
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
a : α
b : WithBot α
h : b ≠ ⊥
bot : ∀ (h : Ne.{u_1 + 1} (α := WithBot α) ⊥ ⊥), a = unbot ⊥ h ↔ (↑a : WithBot α) = ⊥
coe : ∀ (a_1 : α) (h : (↑a_1 : WithBot α) ≠ ⊥), a = (↑a_1 : WithBot α).unbot h ↔ (↑a : WithBot α) = (↑a_1 : WithBot α)
⊢ a = b.unbot h ↔ (↑a : WithBot α) = b

Tactic:
induction b
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
a : α
h : Ne.{u_1 + 1} (α := WithBot α) ⊥ ⊥
⊢ a = unbot ⊥ h ↔ (↑a : WithBot α) = ⊥

Tactic:
simpa using h rfl

Premises used: rfl
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
a a_1 : α
h : (↑a_1 : WithBot α) ≠ ⊥
⊢ a = (↑a_1 : WithBot α).unbot h ↔ (↑a : WithBot α) = (↑a_1 : WithBot α)

Tactic:
simp
-- Module: Mathlib.Order.WithBot
Goal:
α : Type u_1
a b : WithBot α
ha : a ≠ ⊥
hb : b ≠ ⊥
rw : a = (↑(b.unbot hb) : WithBot α) ↔ a = b
rw₁ rw₂ : a = b ↔ a = b
⊢ a.unbot ha = b.unbot hb ↔ a = b

Tactic:
rw [unbot_eq_iff, coe_unbot]

Premises used: WithBot.unbot_eq_iff, WithBot.coe_unbot