awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.SuccPred.Relation
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : PredOrder α
inst_2 : IsPredArchimedean α
r : α → α → Prop
n m : α
h : ∀ i ∈ Ioc m n, r i (pred i)
hnm : m < n
⊢ TransGen r n m

Tactic:
transGen_of_succ_of_lt (α := αᵒᵈ) r (fun x hx => h x ⟨hx.2, hx.1⟩) hnm

Premises used: And.right, And.left, And.intro, OrderDual, transGen_of_succ_of_lt
-- Module: Mathlib.Order.SuccPred.Relation
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : PredOrder α
inst_2 : IsPredArchimedean α
r : α → α → Prop
n m : α
h : ∀ i ∈ Ioc n m, r (pred i) i
hmn : n < m
⊢ TransGen r n m

Tactic:
transGen_of_succ_of_gt (α := αᵒᵈ) r (fun x hx => h x ⟨hx.2, hx.1⟩) hmn

Premises used: transGen_of_succ_of_gt, And.right, And.left, And.intro, OrderDual
-- Module: Mathlib.Order.SuccPred.Relation
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : PredOrder α
inst_2 : IsPredArchimedean α
r : α → α → Prop
n m : α
h1 : ∀ i ∈ Ioc m n, r i (pred i)
h2 : ∀ i ∈ Ioc n m, r (pred i) i
⊢ ReflTransGen r n m

Tactic:
reflTransGen_of_succ (α := αᵒᵈ) r (fun x hx => h1 x ⟨hx.2, hx.1⟩) fun x hx =>
    h2 x ⟨hx.2, hx.1⟩

Premises used: And.right, And.left, And.intro, OrderDual, reflTransGen_of_succ
-- Module: Mathlib.Order.SuccPred.Relation
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : PredOrder α
inst_2 : IsPredArchimedean α
r : α → α → Prop
n m : α
h1 : ∀ i ∈ Ioc m n, r i (pred i)
h2 : ∀ i ∈ Ioc n m, r (pred i) i
hnm : n ≠ m
⊢ TransGen r n m

Tactic:
transGen_of_succ_of_ne (α := αᵒᵈ) r (fun x hx => h1 x ⟨hx.2, hx.1⟩)
    (fun x hx => h2 x ⟨hx.2, hx.1⟩) hnm

Premises used: transGen_of_succ_of_ne, And.right, And.left, And.intro, OrderDual
-- Module: Mathlib.Order.SuccPred.Relation
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : PredOrder α
inst_2 : IsPredArchimedean α
r : α → α → Prop
n m : α
inst_3 : Std.Refl r
h1 : ∀ i ∈ Ioc m n, r i (pred i)
h2 : ∀ i ∈ Ioc n m, r (pred i) i
⊢ TransGen r n m

Tactic:
@transGen_of_succ_of_refl αᵒᵈ _ _ _ r _ _ ‹_› (fun x hx ↦ h1 x ⟨hx.2, hx.1⟩)
    fun x hx ↦ h2 x ⟨hx.2, hx.1⟩

Premises used: transGen_of_succ_of_refl, And.right, And.left, And.intro, OrderDual
-- Module: Mathlib.Order.SuccPred.Tree
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : PredOrder α
inst_2 : IsPredArchimedean α
inst_3 : OrderBot α
inst_4 : DecidableEq α
r : α
⊢ findAtom r ≤ r

Tactic:
Order.pred_iterate_le _ _

Premises used: Order.pred_iterate_le, IsPredArchimedean.findAtom
-- Module: Mathlib.Order.SuccPred.Tree
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : PredOrder α
inst_2 : IsPredArchimedean α
inst_3 : OrderBot α
inst_4 : DecidableEq α
h : Eq.{u_1 + 1} (α := α) (Order.pred ⊥) ⊥
⊢ Eq.{u_1 + 1} (α := α) (findAtom ⊥) ⊥

Tactic:
apply Function.iterate_fixed

Premises used: Function.iterate_fixed
-- Module: Mathlib.Order.SuccPred.Tree
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : PredOrder α
inst_2 : IsPredArchimedean α
inst_3 : OrderBot α
inst_4 : DecidableEq α
⊢ Eq.{u_1 + 1} (α := α) (Order.pred ⊥) ⊥

Tactic:
simp
-- Module: Mathlib.Order.SuccPred.Tree
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : PredOrder α
inst_2 : IsPredArchimedean α
inst_3 : OrderBot α
inst_4 : DecidableEq α
r : α
generalize :
  ∀ (n : ℕ) (h : Nat.find (p := fun (n : ℕ) ↦ Order.pred^[n] r = ⊥) ⋯ = n), Order.pred (Order.pred^[n - 1] r) = ⊥
⊢ Order.pred (Order.pred^[Nat.find (p := fun (n : ℕ) ↦ Order.pred^[n] r = ⊥) ⋯ - 1] r) = ⊥

Tactic:
generalize h : Nat.find (bot_le (a := r)).exists_pred_iterate = n

Premises used: LE.le.exists_pred_iterate, Nat.find, bot_le
-- Module: Mathlib.Order.SuccPred.Tree
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : PredOrder α
inst_2 : IsPredArchimedean α
inst_3 : OrderBot α
inst_4 : DecidableEq α
r : α
n : ℕ
h : Nat.find (p := fun (n : ℕ) ↦ Order.pred^[n] r = ⊥) ⋯ = n
zero :
  ∀ (h : Nat.find (p := fun (n : ℕ) ↦ Order.pred^[n] r = ⊥) ⋯ = 0),
    Order.pred (Order.pred^[HSub.hSub (α := ℕ) 0 1] r) = ⊥
succ :
  ∀ (n : ℕ) (h : Nat.find (p := fun (n : ℕ) ↦ Order.pred^[n] r = ⊥) ⋯ = n + 1),
    Order.pred (Order.pred^[n + 1 - 1] r) = ⊥
⊢ Order.pred (Order.pred^[n - 1] r) = ⊥

Tactic:
cases n
-- Module: Mathlib.Order.SuccPred.Tree
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : PredOrder α
inst_2 : IsPredArchimedean α
inst_3 : OrderBot α
inst_4 : DecidableEq α
r : α
h : Nat.find (p := fun (n : ℕ) ↦ Order.pred^[n] r = ⊥) ⋯ = 0
rw : Order.pred^[Nat.find (p := fun (n : ℕ) ↦ Order.pred^[n] r = ⊥) ⋯] r = ⊥
⊢ Order.pred^[0] r = ⊥

Tactic:
rw [← h]
-- Module: Mathlib.Order.SuccPred.Tree
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : PredOrder α
inst_2 : IsPredArchimedean α
inst_3 : OrderBot α
inst_4 : DecidableEq α
r : α
h : Nat.find (p := fun (n : ℕ) ↦ Order.pred^[n] r = ⊥) ⋯ = 0
⊢ Order.pred^[Nat.find (p := fun (n : ℕ) ↦ Order.pred^[n] r = ⊥) ⋯] r = ⊥

Tactic:
apply Nat.find_spec (bot_le (a := r)).exists_pred_iterate

Premises used: LE.le.exists_pred_iterate, bot_le, Nat.find_spec
-- Module: Mathlib.Order.SuccPred.Tree
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : PredOrder α
inst_2 : IsPredArchimedean α
inst_3 : OrderBot α
inst_4 : DecidableEq α
r : α
h : Nat.find (p := fun (n : ℕ) ↦ Order.pred^[n] r = ⊥) ⋯ = 0
⊢ Order.pred^[0] r = ⊥

Tactic:
have : Order.pred^[0] r = ⊥ := by
      rw [← h]
      apply Nat.find_spec (bot_le (a := r)).exists_pred_iterate
-- Module: Mathlib.Order.SuccPred.Tree
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : PredOrder α
inst_2 : IsPredArchimedean α
inst_3 : OrderBot α
inst_4 : DecidableEq α
r : α
h : Nat.find (p := fun (n : ℕ) ↦ Order.pred^[n] r = ⊥) ⋯ = 0
this : r = ⊥
⊢ Order.pred (Order.pred^[HSub.hSub (α := ℕ) 0 1] r) = ⊥

Tactic:
simp [this]
-- Module: Mathlib.Order.SuccPred.Tree
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : PredOrder α
inst_2 : IsPredArchimedean α
inst_3 : OrderBot α
inst_4 : DecidableEq α
r : α
n : ℕ
h : Nat.find (p := fun (n : ℕ) ↦ Order.pred^[n] r = ⊥) ⋯ = n + 1
succ : Order.pred^[n + 1] r = ⊥
⊢ Order.pred (Order.pred^[n + 1 - 1] r) = ⊥

Tactic:
simp only [Nat.add_sub_cancel_right, ← Function.iterate_succ_apply', Nat.succ_eq_add_one]

Premises used: Function.iterate_succ_apply', Nat.add_sub_cancel_right, Nat.succ_eq_add_one
-- Module: Mathlib.Order.SuccPred.Tree
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : PredOrder α
inst_2 : IsPredArchimedean α
inst_3 : OrderBot α
inst_4 : DecidableEq α
r : α
n : ℕ
h : Nat.find (p := fun (n : ℕ) ↦ Order.pred^[n] r = ⊥) ⋯ = n + 1
succ : Order.pred^[Nat.find (p := fun (n : ℕ) ↦ Order.pred^[n] r = ⊥) ⋯] r = ⊥
⊢ Order.pred^[n + 1] r = ⊥

Tactic:
rw [← h]
-- Module: Mathlib.Order.SuccPred.Tree
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : PredOrder α
inst_2 : IsPredArchimedean α
inst_3 : OrderBot α
inst_4 : DecidableEq α
r : α
n : ℕ
h : Nat.find (p := fun (n : ℕ) ↦ Order.pred^[n] r = ⊥) ⋯ = n + 1
⊢ Order.pred^[Nat.find (p := fun (n : ℕ) ↦ Order.pred^[n] r = ⊥) ⋯] r = ⊥

Tactic:
apply Nat.find_spec (bot_le (a := r)).exists_pred_iterate

Premises used: LE.le.exists_pred_iterate, bot_le, Nat.find_spec
-- Module: Mathlib.Order.SuccPred.Tree
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : PredOrder α
inst_2 : IsPredArchimedean α
inst_3 : OrderBot α
inst_4 : DecidableEq α
r : α
h : Order.pred^[Nat.find (p := fun (n : ℕ) ↦ Order.pred^[n] r = ⊥) ⋯ - 1] r = ⊥
⊢ Nat.find (p := fun (n : ℕ) ↦ Order.pred^[n] r = ⊥) ⋯ ≤ Nat.find (p := fun (n : ℕ) ↦ Order.pred^[n] r = ⊥) ⋯ - 1

Tactic:
have := Nat.find_min' (bot_le (a := r)).exists_pred_iterate h
-- Module: Mathlib.Order.SuccPred.Tree
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : PredOrder α
inst_2 : IsPredArchimedean α
inst_3 : OrderBot α
inst_4 : DecidableEq α
r : α
h : Order.pred^[Nat.find (p := fun (n : ℕ) ↦ Order.pred^[n] r = ⊥) ⋯ - 1] r = ⊥
this : Nat.find (p := fun (n : ℕ) ↦ Order.pred^[n] r = ⊥) ⋯ ≤ Nat.find (p := fun (n : ℕ) ↦ Order.pred^[n] r = ⊥) ⋯ - 1
⊢ Nat.find (p := fun (n : ℕ) ↦ Order.pred^[n] r = ⊥) ⋯ = 0

Tactic:
lia
-- Module: Mathlib.Order.SuccPred.Tree
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : PredOrder α
inst_2 : IsPredArchimedean α
inst_3 : OrderBot α
inst_4 : DecidableEq α
r : α
h : Order.pred^[Nat.find (p := fun (n : ℕ) ↦ Order.pred^[n] r = ⊥) ⋯ - 1] r = ⊥
this : Nat.find (p := fun (n : ℕ) ↦ Order.pred^[n] r = ⊥) ⋯ ≤ Nat.find (p := fun (n : ℕ) ↦ Order.pred^[n] r = ⊥) ⋯ - 1
⊢ Nat.find (p := fun (n : ℕ) ↦ Order.pred^[n] r = ⊥) ⋯ = 0

Tactic:
replace : Nat.find (bot_le (a := r)).exists_pred_iterate = 0 := by lia
-- Module: Mathlib.Order.SuccPred.Tree
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : PredOrder α
inst_2 : IsPredArchimedean α
inst_3 : OrderBot α
inst_4 : DecidableEq α
r : α
h : Order.pred^[Nat.find (p := fun (n : ℕ) ↦ Order.pred^[n] r = ⊥) ⋯ - 1] r = ⊥
this : Nat.find (p := fun (n : ℕ) ↦ Order.pred^[n] r = ⊥) ⋯ = 0
⊢ r = ⊥

Tactic:
simpa [this] using h
-- Module: Mathlib.Order.SuccPred.Tree
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : PredOrder α
inst_2 : IsPredArchimedean α
inst_3 : OrderBot α
inst_4 : DecidableEq α
r : α
h : r = ⊥
⊢ findAtom r = ⊥

Tactic:
simp [h]
-- Module: Mathlib.Order.SuccPred.Tree
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : PredOrder α
inst_2 : IsPredArchimedean α
inst_3 : OrderBot α
inst_4 : DecidableEq α
r : α
⊢ findAtom r ≠ ⊥ ↔ r ≠ ⊥

Tactic:
findAtom_eq_bot.not

Premises used: IsPredArchimedean.findAtom_eq_bot, Iff.not
-- Module: Mathlib.Order.SuccPred.Tree
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : PredOrder α
inst_2 : IsPredArchimedean α
inst_3 : OrderBot α
inst_4 : DecidableEq α
r : α
hr : r ≠ ⊥
left : findAtom r ≠ ⊥
right : ∀ b < findAtom r, b = ⊥
⊢ IsAtom (findAtom r)

Tactic:
constructor
-- Module: Mathlib.Order.SuccPred.Tree
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : PredOrder α
inst_2 : IsPredArchimedean α
inst_3 : OrderBot α
inst_4 : DecidableEq α
r : α
hr : r ≠ ⊥
⊢ findAtom r ≠ ⊥

Tactic:
simp [hr]
-- Module: Mathlib.Order.SuccPred.Tree
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : PredOrder α
inst_2 : IsPredArchimedean α
inst_3 : OrderBot α
inst_4 : DecidableEq α
r : α
hr : r ≠ ⊥
b : α
hb : b < findAtom r
⊢ b ≤ Order.pred (findAtom r)

Tactic:
apply Order.le_pred_of_lt at hb

Premises used: Order.le_pred_of_lt
-- Module: Mathlib.Order.SuccPred.Tree
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : PredOrder α
inst_2 : IsPredArchimedean α
inst_3 : OrderBot α
inst_4 : DecidableEq α
r : α
hr : r ≠ ⊥
b : α
hb : b ≤ Order.pred (findAtom r)
⊢ b = ⊥

Tactic:
simpa using hb
-- Module: Mathlib.Order.SuccPred.Tree
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : PredOrder α
inst_2 : IsPredArchimedean α
inst_3 : OrderBot α
inst_4 : DecidableEq α
r : α
h : IsAtom (findAtom r)
nh : r = ⊥
⊢ IsAtom.{u_1} (α := α) ⊥

Tactic:
simp only [nh, findAtom_bot] at h

Premises used: IsPredArchimedean.findAtom_bot
-- Module: Mathlib.Order.SuccPred.Tree
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : PredOrder α
inst_2 : IsPredArchimedean α
inst_3 : OrderBot α
inst_4 : DecidableEq α
r : α
nh : r = ⊥
h : IsAtom.{u_1} (α := α) ⊥
⊢ False

Tactic:
h.1 rfl

Premises used: And.left, rfl
-- Module: Mathlib.Order.SuccPred.Tree
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : PredOrder α
inst_2 : IsPredArchimedean α
inst_3 : OrderBot α
inst_4 : DecidableEq α
r : α
nh : r = ⊥
h : IsAtom.{u_1} (α := α) ⊥
⊢ False

Tactic:
exact h.1 rfl

Premises used: And.left, rfl
-- Module: Mathlib.Order.SuccPred.Tree
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : PredOrder α
inst_2 : IsPredArchimedean α
inst_3 : OrderBot α
b : α
rw : ¬b = ⊥ → ∃ (a : α), IsAtom a ∧ a ≤ b
⊢ b = ⊥ ∨ ∃ (a : α), IsAtom a ∧ a ≤ b

Tactic:
rw [or_iff_not_imp_left]

Premises used: Classical.or_iff_not_imp_left
-- Module: Mathlib.Order.SuccPred.Tree
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : PredOrder α
inst_2 : IsPredArchimedean α
inst_3 : OrderBot α
b : α
hb : ¬b = ⊥
w : α
left : IsAtom (findAtom b)
right : findAtom b ≤ b
⊢ ∃ (a : α), IsAtom a ∧ a ≤ b

Tactic:
use findAtom b, isAtom_findAtom hb, findAtom_le b

Premises used: IsPredArchimedean.isAtom_findAtom, IsPredArchimedean.findAtom, IsPredArchimedean.findAtom_le
-- Module: Mathlib.Order.SuccPred.Tree
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : PredOrder α
inst_2 : IsPredArchimedean α
inst_3 : OrderBot α
b : α
rw rw₁ rw₂ rw₃ : ∀ (hb : ¬b = ⊥), ∃ (a : α), IsAtom a ∧ a ≤ b
⊢ b = ⊥ ∨ ∃ (a : α), IsAtom a ∧ a ≤ b

Tactic:
classical
    rw [or_iff_not_imp_left]
    intro hb
    use findAtom b, isAtom_findAtom hb, findAtom_le b

Premises used: Classical.or_iff_not_imp_left
-- Module: Mathlib.Order.SuccPred.Tree
Goal:
t : RootedTree
r : (↑t : Type u_2)
⊢ (t.subtree r).root = r

Tactic:
rfl

Premises used: SubRootedTree.root, RootedTree.subtree, rfl
-- Module: Mathlib.Order.SuccPred.Tree
Goal:
t : RootedTree
v : SubRootedTree t
⊢ t.subtree v.root = v

Tactic:
rfl

Premises used: SubRootedTree.root, RootedTree.subtree, rfl
-- Module: Mathlib.Order.SuccPred.Tree
Goal:
t : RootedTree
v₁ v₂ : SubRootedTree t
h : v₁.root = v₂.root
⊢ v₁ = v₂

Tactic:
h

Premises used: SubRootedTree, SubRootedTree.root
-- Module: Mathlib.Order.SuccPred.Tree
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : PredOrder α
inst_2 : IsPredArchimedean α
t : RootedTree
a₁ a₂ : SubRootedTree t
h :
  Eq.{u_2 + 1} (α := Set (↑t : Type u_2)) ((fun (v : SubRootedTree t) ↦ Set.Ici v.root) a₁)
    ((fun (v : SubRootedTree t) ↦ Set.Ici v.root) a₂)
⊢ a₁ = a₂

Tactic:
simpa only [Set.Ici_inj, ← SubRootedTree.ext_iff] using h

Premises used: SubRootedTree.ext_iff, Set.Ici_inj
-- Module: Mathlib.Order.SuccPred.Tree
Goal:
t : RootedTree
r : SubRootedTree t
v : (↑t : Type u_2)
⊢ v ∈ r ↔ r.root ≤ v

Tactic:
Iff.rfl

Premises used: Set.Ici, Set.Mem, Iff.rfl, setOf
-- Module: Mathlib.Order.SuccPred.Tree
Goal:
t : RootedTree
r : SubRootedTree t
⊢ ⊥ ∈ r ↔ r.root = ⊥

Tactic:
simp [mem_iff]

Premises used: SubRootedTree.mem_iff
-- Module: Mathlib.Order.SuccPred.Tree
Goal:
t : RootedTree
r : SubRootedTree t
hr : IsAtom r.root
⊢ r.root ≠ ⊥

Tactic:
hr.1

Premises used: And.left
-- Module: Mathlib.Order.SuccPred.Tree
Goal:
t : RootedTree
r : SubRootedTree t
hr : IsAtom r.root
⊢ r.root ≠ ⊥

Tactic:
exact hr.1

Premises used: And.left
-- Module: Mathlib.Order.SuccPred.Tree
Goal:
t : RootedTree
t₁ t₂ : SubRootedTree t
ht₁ : t₁ ∈ t.subtrees
ht₂ : t₂ ∈ t.subtrees
v₁ v₂ : (↑t : Type u_2)
h₁ : v₁ ∈ t₁
h₂ : v₂ ∈ t₂
h : Disjoint v₁ v₂
nh : t₁ = t₂
simp : t₁.root ≤ v₁ ∧ t₁.root ≤ v₂
⊢ t₁.root ≤ v₁ ⊓ v₂

Tactic:
simp only [le_inf_iff]

Premises used: le_inf_iff
-- Module: Mathlib.Order.SuccPred.Tree
Goal:
t : RootedTree
t₁ t₂ : SubRootedTree t
ht₁ : t₁ ∈ t.subtrees
ht₂ : t₂ ∈ t.subtrees
v₁ v₂ : (↑t : Type u_2)
h₁ : v₁ ∈ t₁
h₂ : v₂ ∈ t₂
h : Disjoint v₁ v₂
nh : t₁ = t₂
⊢ t₁.root ≤ v₁ ∧ t₁.root ≤ v₂

Tactic:
⟨h₁, nh ▸ h₂⟩

Premises used: Eq.rec, And.intro, Eq.symm
-- Module: Mathlib.Order.SuccPred.Tree
Goal:
t : RootedTree
t₁ t₂ : SubRootedTree t
ht₁ : t₁ ∈ t.subtrees
ht₂ : t₂ ∈ t.subtrees
v₁ v₂ : (↑t : Type u_2)
h₁ : v₁ ∈ t₁
h₂ : v₂ ∈ t₂
h : Disjoint v₁ v₂
nh : t₁ = t₂
⊢ t₁.root ≤ v₁ ∧ t₁.root ≤ v₂

Tactic:
exact ⟨h₁, nh ▸ h₂⟩
-- Module: Mathlib.Order.SuccPred.Tree
Goal:
t : RootedTree
t₁ t₂ : SubRootedTree t
ht₁ : t₁ ∈ t.subtrees
ht₂ : t₂ ∈ t.subtrees
v₁ v₂ : (↑t : Type u_2)
h₁ : v₁ ∈ t₁
h₂ : v₂ ∈ t₂
h : Disjoint v₁ v₂
nh : t₁ = t₂
⊢ t₁.root ≤ v₁ ⊓ v₂

Tactic:
have : t₁.root ≤ (v₁ : t) ⊓ (v₂ : t) := by
      simp only [le_inf_iff]
      exact ⟨h₁, nh ▸ h₂⟩
-- Module: Mathlib.Order.SuccPred.Tree
Goal:
t : RootedTree
t₁ t₂ : SubRootedTree t
ht₁ : t₁ ∈ t.subtrees
ht₂ : t₂ ∈ t.subtrees
v₁ v₂ : (↑t : Type u_2)
h₁ : v₁ ∈ t₁
h₂ : v₂ ∈ t₂
h : Disjoint v₁ v₂
nh : t₁ = t₂
this : t₁.root ≤ v₁ ⊓ v₂
⊢ t₁.root ≤ ⊥

Tactic:
rw [h.eq_bot] at this

Premises used: Disjoint.eq_bot
-- Module: Mathlib.Order.SuccPred.Tree
Goal:
t : RootedTree
t₁ t₂ : SubRootedTree t
ht₁ : t₁ ∈ t.subtrees
ht₂ : t₂ ∈ t.subtrees
v₁ v₂ : (↑t : Type u_2)
h₁ : v₁ ∈ t₁
h₂ : v₂ ∈ t₂
h : Disjoint v₁ v₂
nh : t₁ = t₂
this : t₁.root ≤ ⊥
⊢ t₁.root = ⊥

Tactic:
simp only [le_bot_iff] at this

Premises used: le_bot_iff
-- Module: Mathlib.Order.SuccPred.Tree
Goal:
t : RootedTree
t₁ t₂ : SubRootedTree t
ht₁ : t₁ ∈ t.subtrees
ht₂ : t₂ ∈ t.subtrees
v₁ v₂ : (↑t : Type u_2)
h₁ : v₁ ∈ t₁
h₂ : v₂ ∈ t₂
h : Disjoint v₁ v₂
nh : t₁ = t₂
this : t₁.root = ⊥
⊢ False

Tactic:
t₁.root_ne_bot_of_mem_subtrees ht₁ this

Premises used: SubRootedTree.root_ne_bot_of_mem_subtrees
-- Module: Mathlib.Order.SuccPred.Tree
Goal:
t : RootedTree
t₁ t₂ : SubRootedTree t
ht₁ : t₁ ∈ t.subtrees
ht₂ : t₂ ∈ t.subtrees
v₁ v₂ : (↑t : Type u_2)
h₁ : v₁ ∈ t₁
h₂ : v₂ ∈ t₂
h : Disjoint v₁ v₂
nh : t₁ = t₂
this : t₁.root = ⊥
⊢ False

Tactic:
exact t₁.root_ne_bot_of_mem_subtrees ht₁ this

Premises used: SubRootedTree.root_ne_bot_of_mem_subtrees
-- Module: Mathlib.Order.SuccPred.Tree
Goal:
t : RootedTree
t₁ t₂ : SubRootedTree t
ht₁ : t₁ ∈ t.subtrees
ht₂ : t₂ ∈ t.subtrees
v₁ v₂ : (↑t : Type u_2)
h₁ : v₁ ∈ t₁
h₂ : v₂ ∈ t₂
h : t₁ ≠ t₂
⊢ t₁.root ≤ v₁

Tactic:
rw [SubRootedTree.mem_iff] at h₁ h₂

Premises used: SubRootedTree.mem_iff
-- Module: Mathlib.Order.SuccPred.Tree
Goal:
t : RootedTree
t₁ t₂ : SubRootedTree t
ht₁ : t₁ ∈ t.subtrees
ht₂ : t₂ ∈ t.subtrees
v₁ v₂ : (↑t : Type u_2)
h₁ : v₁ ∈ t₁
h₂ : v₂ ∈ t₂
h : t₁ ≠ t₂
h₃ : t₁.root ≤ v₁
⊢ t₂.root ≤ v₂

Tactic:
rw [SubRootedTree.mem_iff] at h₁ h₂

Premises used: SubRootedTree.mem_iff
-- Module: Mathlib.Order.SuccPred.Tree
Goal:
t : RootedTree
t₁ t₂ : SubRootedTree t
ht₁ : t₁ ∈ t.subtrees
ht₂ : t₂ ∈ t.subtrees
v₁ v₂ : (↑t : Type u_2)
h₁ : v₁ ∈ t₁
h₂ : v₂ ∈ t₂
h : t₁ ≠ t₂
h₃ : t₁.root ≤ v₁
h₄ : t₂.root ≤ v₂
⊢ t₁ ≠ t₂

Tactic:
rw [SubRootedTree.mem_iff] at h₁ h₂

Premises used: SubRootedTree.mem_iff
-- Module: Mathlib.Order.SuccPred.Tree
Goal:
t : RootedTree
t₁ t₂ : SubRootedTree t
ht₁ : t₁ ∈ t.subtrees
ht₂ : t₂ ∈ t.subtrees
v₁ v₂ : (↑t : Type u_2)
h₁ : t₁.root ≤ v₁
h₂ : t₂.root ≤ v₂
h : t₁ ≠ t₂
contrapose : ∀ (h : ¬Disjoint v₁ v₂), t₁ = t₂
⊢ Disjoint v₁ v₂

Tactic:
contrapose h
-- Module: Mathlib.Order.SuccPred.Tree
Goal:
t : RootedTree
t₁ t₂ : SubRootedTree t
ht₁ : t₁ ∈ t.subtrees
ht₂ : t₂ ∈ t.subtrees
v₁ v₂ : (↑t : Type u_2)
h₁ : t₁.root ≤ v₁
h₂ : t₂.root ≤ v₂
h : ¬Disjoint v₁ v₂
⊢ ⊥ < v₁ ⊓ v₂

Tactic:
rw [disjoint_iff, ← ne_eq, ← bot_lt_iff_ne_bot] at h

Premises used: disjoint_iff, bot_lt_iff_ne_bot, ne_eq
-- Module: Mathlib.Order.SuccPred.Tree
Goal:
t : RootedTree
t₁ t₂ : SubRootedTree t
ht₁ : t₁ ∈ t.subtrees
ht₂ : t₂ ∈ t.subtrees
v₁ v₂ : (↑t : Type u_2)
h₁ : t₁.root ≤ v₁
h₂ : t₂.root ≤ v₂
h : ⊥ < v₁ ⊓ v₂
⊢ v₁ ⊓ v₂ ≤ v₁

Tactic:
simp
-- Module: Mathlib.Order.SuccPred.Tree
Goal:
t : RootedTree
t₁ t₂ : SubRootedTree t
ht₁ : t₁ ∈ t.subtrees
ht₂ : t₂ ∈ t.subtrees
v₁ v₂ : (↑t : Type u_2)
h₁ : t₁.root ≤ v₁
h₂ : t₂.root ≤ v₂
h : ⊥ < v₁ ⊓ v₂
inl : ∀ (oh : v₁ ⊓ v₂ < t₁.root), t₁ = t₂
inr : ∀ (oh : t₁.root ≤ v₁ ⊓ v₂), t₁ = t₂
⊢ t₁ = t₂

Tactic:
rcases lt_or_le_of_directed (by simp : v₁ ⊓ v₂ ≤ v₁) h₁ with oh | oh

Premises used: lt_or_le_of_directed
-- Module: Mathlib.Order.SuccPred.Tree
Goal:
t : RootedTree
t₁ t₂ : SubRootedTree t
ht₁ : t₁ ∈ t.subtrees
ht₂ : t₂ ∈ t.subtrees
v₁ v₂ : (↑t : Type u_2)
h₁ : t₁.root ≤ v₁
h₂ : t₂.root ≤ v₂
h : ⊥ < v₁ ⊓ v₂
oh : v₁ ⊓ v₂ < t₁.root
⊢ t₁ = t₂

Tactic:
simp_all [RootedTree.subtrees, IsAtom.lt_iff]

Premises used: IsAtom.lt_iff, RootedTree.subtrees
-- Module: Mathlib.Order.SuccPred.Tree
Goal:
t : RootedTree
t₁ t₂ : SubRootedTree t
ht₁ : t₁ ∈ t.subtrees
ht₂ : t₂ ∈ t.subtrees
v₁ v₂ : (↑t : Type u_2)
h₁ : t₁.root ≤ v₁
h₂ : t₂.root ≤ v₂
h : ⊥ < v₁ ⊓ v₂
oh : t₁.root ≤ v₁ ⊓ v₂
⊢ t₁.root ≤ v₁ ∧ t₁.root ≤ v₂

Tactic:
rw [le_inf_iff] at oh

Premises used: le_inf_iff
-- Module: Mathlib.Order.SuccPred.Tree
Goal:
t : RootedTree
t₁ t₂ : SubRootedTree t
ht₁ : t₁ ∈ t.subtrees
ht₂ : t₂ ∈ t.subtrees
v₁ v₂ : (↑t : Type u_2)
h₁ : t₁.root ≤ v₁
h₂ : t₂.root ≤ v₂
h : ⊥ < v₁ ⊓ v₂
oh : t₁.root ≤ v₁ ∧ t₁.root ≤ v₂
inr : t₁.root = t₂.root
⊢ t₁ = t₂

Tactic:
ext
-- Module: Mathlib.Order.SuccPred.Tree
Goal:
t : RootedTree
t₁ t₂ : SubRootedTree t
ht₁ : t₁ ∈ t.subtrees
ht₂ : t₂ ∈ t.subtrees
v₁ v₂ : (↑t : Type u_2)
h₁ : t₁.root ≤ v₁
h₂ : t₂.root ≤ v₂
h : ⊥ < v₁ ⊓ v₂
oh : t₁.root ≤ v₁ ∧ t₁.root ≤ v₂
⊢ t₁.root = t₂.root

Tactic:
simpa only [ht₂.le_iff_eq ht₁.1, ht₁.le_iff_eq ht₂.1, eq_comm, or_self] using
      le_total_of_directed oh.2 h₂

Premises used: eq_comm, And.right, And.left, or_self, IsAtom.le_iff_eq, le_total_of_directed
-- Module: Mathlib.Order.SuccPred.Tree
Goal:
t : RootedTree
t₁ : SubRootedTree t
ht₁ : t₁ ∈ t.subtrees
t₂ : SubRootedTree t
ht₂ : t₂ ∈ t.subtrees
h : t₁ ≠ t₂
rw : ∀ ⦃a : (↑t : Type u_2)⦄, a ∈ (↑t₁ : Set (↑t : Type u_2)) → a ∉ (↑t₂ : Set (↑t : Type u_2))
⊢ Function.onFun Disjoint SetLike.coe t₁ t₂

Tactic:
rw [Function.onFun_apply, Set.disjoint_left]

Premises used: Set.disjoint_left, Function.onFun_apply
-- Module: Mathlib.Order.SuccPred.Tree
Goal:
t : RootedTree
t₁ : SubRootedTree t
ht₁ : t₁ ∈ t.subtrees
t₂ : SubRootedTree t
ht₂ : t₂ ∈ t.subtrees
h : t₁ ≠ t₂
a : (↑t : Type u_2)
ha : a ∈ (↑t₁ : Set (↑t : Type u_2))
hb : a ∈ (↑t₂ : Set (↑t : Type u_2))
⊢ a = ⊥

Tactic:
rw [← mem_subtrees_disjoint_iff ht₁ ht₂ a a ha hb, disjoint_self] at h

Premises used: RootedTree.mem_subtrees_disjoint_iff, disjoint_self
-- Module: Mathlib.Order.SuccPred.Tree
Goal:
t : RootedTree
t₁ : SubRootedTree t
ht₁ : t₁ ∈ t.subtrees
t₂ : SubRootedTree t
ht₂ : t₂ ∈ t.subtrees
h : t₁ ≠ t₂
a : (↑t : Type u_2)
ha : a ∈ (↑t₁ : Set (↑t : Type u_2))
hb : a ∈ (↑t₂ : Set (↑t : Type u_2))
h₁ : a = ⊥
⊢ a ∈ (↑t₁ : Set (↑t : Type u_2))

Tactic:
rw [← mem_subtrees_disjoint_iff ht₁ ht₂ a a ha hb, disjoint_self] at h

Premises used: RootedTree.mem_subtrees_disjoint_iff, disjoint_self
-- Module: Mathlib.Order.SuccPred.Tree
Goal:
t : RootedTree
t₁ : SubRootedTree t
ht₁ : t₁ ∈ t.subtrees
t₂ : SubRootedTree t
ht₂ : t₂ ∈ t.subtrees
h : t₁ ≠ t₂
a : (↑t : Type u_2)
ha : a ∈ (↑t₁ : Set (↑t : Type u_2))
hb : a ∈ (↑t₂ : Set (↑t : Type u_2))
h₁ : a = ⊥
ha₁ : a ∈ (↑t₁ : Set (↑t : Type u_2))
⊢ a ∈ (↑t₂ : Set (↑t : Type u_2))

Tactic:
rw [← mem_subtrees_disjoint_iff ht₁ ht₂ a a ha hb, disjoint_self] at h

Premises used: RootedTree.mem_subtrees_disjoint_iff, disjoint_self
-- Module: Mathlib.Order.SuccPred.Tree
Goal:
t : RootedTree
t₁ : SubRootedTree t
ht₁ : t₁ ∈ t.subtrees
t₂ : SubRootedTree t
ht₂ : t₂ ∈ t.subtrees
a : (↑t : Type u_2)
h : a = ⊥
ha : a ∈ (↑t₁ : Set (↑t : Type u_2))
hb : a ∈ (↑t₂ : Set (↑t : Type u_2))
⊢ ⊥ ∈ (↑t₁ : Set (↑t : Type u_2))

Tactic:
subst h
-- Module: Mathlib.Order.SuccPred.Tree
Goal:
t : RootedTree
t₁ : SubRootedTree t
ht₁ : t₁ ∈ t.subtrees
t₂ : SubRootedTree t
ht₂ : t₂ ∈ t.subtrees
a : (↑t : Type u_2)
h : a = ⊥
ha : a ∈ (↑t₁ : Set (↑t : Type u_2))
hb : a ∈ (↑t₂ : Set (↑t : Type u_2))
ha₁ : ⊥ ∈ (↑t₁ : Set (↑t : Type u_2))
⊢ ⊥ ∈ (↑t₂ : Set (↑t : Type u_2))

Tactic:
subst h
-- Module: Mathlib.Order.SuccPred.Tree
Goal:
t : RootedTree
t₁ : SubRootedTree t
ht₁ : t₁ ∈ t.subtrees
t₂ : SubRootedTree t
ht₂ : t₂ ∈ t.subtrees
ha : ⊥ ∈ (↑t₁ : Set (↑t : Type u_2))
hb : ⊥ ∈ (↑t₂ : Set (↑t : Type u_2))
⊢ t₁.root = ⊥

Tactic:
simp only [SetLike.mem_coe, SubRootedTree.bot_mem_iff] at ha

Premises used: SetLike.mem_coe, SubRootedTree.bot_mem_iff
-- Module: Mathlib.Order.SuccPred.Tree
Goal:
t : RootedTree
t₁ : SubRootedTree t
ht₁ : t₁ ∈ t.subtrees
t₂ : SubRootedTree t
ht₂ : t₂ ∈ t.subtrees
hb : ⊥ ∈ (↑t₂ : Set (↑t : Type u_2))
ha : t₁.root = ⊥
⊢ False

Tactic:
t₁.root_ne_bot_of_mem_subtrees ht₁ ha

Premises used: SubRootedTree.root_ne_bot_of_mem_subtrees
-- Module: Mathlib.Order.SuccPred.Tree
Goal:
t : RootedTree
t₁ : SubRootedTree t
ht₁ : t₁ ∈ t.subtrees
t₂ : SubRootedTree t
ht₂ : t₂ ∈ t.subtrees
hb : ⊥ ∈ (↑t₂ : Set (↑t : Type u_2))
ha : t₁.root = ⊥
⊢ False

Tactic:
exact t₁.root_ne_bot_of_mem_subtrees ht₁ ha

Premises used: SubRootedTree.root_ne_bot_of_mem_subtrees
-- Module: Mathlib.Order.SuccPred.Tree
Goal:
t : RootedTree
inst : DecidableEq (↑t : Type u_2)
v : (↑t : Type u_2)
⊢ v ∈ t.subtreeOf v

Tactic:
simp [SubRootedTree.mem_iff, RootedTree.subtreeOf]

Premises used: SubRootedTree.mem_iff, RootedTree.subtreeOf
-- Module: Mathlib.Order.SuccPred.Tree
Goal:
t : RootedTree
inst : DecidableEq (↑t : Type u_2)
v : (↑t : Type u_2)
hr : v ≠ ⊥
⊢ t.subtreeOf v ∈ t.subtrees

Tactic:
simpa [RootedTree.subtrees, RootedTree.subtreeOf]

Premises used: RootedTree.subtrees, RootedTree.subtreeOf
-- Module: Mathlib.Order.SuccPred.WithBot
Goal:
α : Type u_1
inst : Preorder α
inst_1 : OrderBot α
inst_2 : SuccOrder α
⊢ Eq.{u_1 + 1} (α := α) (succ ⊥) ⊥

Tactic:
rfl

Premises used: WithBot.succ, WithBot.recBotCoe, rfl