awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Order.TransfiniteIteration
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₀ ≠ ⊤
⊢ ∃ (b : J), j₁ < b

Tactic:
exact ⟨_, hj⟩
-- Module: Mathlib.Order.TransfiniteIteration
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₁

Tactic:
have hj₁ : ¬ IsMax j₁ := by
    simp only [not_isMax_iff]
    exact ⟨_, hj⟩
-- Module: Mathlib.Order.TransfiniteIteration
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₀

Tactic:
lt_of_lt_of_le (hφ' _ (this j₁)) ?_

Premises used: lt_of_lt_of_le
-- Module: Mathlib.Order.TransfiniteIteration
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₁
refine : φ (transfiniteIterate φ j₁ i₀) ≤ transfiniteIterate φ j₂ i₀
⊢ transfiniteIterate φ j₁ i₀ < transfiniteIterate φ j₂ i₀

Tactic:
refine lt_of_lt_of_le (hφ' _ (this j₁)) ?_

Premises used: lt_of_lt_of_le
-- Module: Mathlib.Order.TransfiniteIteration
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₁
rw : transfiniteIterate φ (Order.succ j₁) i₀ ≤ transfiniteIterate φ j₂ i₀
⊢ φ (transfiniteIterate φ j₁ i₀) ≤ transfiniteIterate φ j₂ i₀

Tactic:
rw [← transfiniteIterate_succ φ i₀ j₁ hj₁]

Premises used: transfiniteIterate_succ
-- Module: Mathlib.Order.TransfiniteIteration
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 φ (Order.succ j₁) i₀ ≤ transfiniteIterate φ j₂ i₀

Tactic:
monotone_transfiniteIterate _ _ hφ (Order.succ_le_of_lt hj)

Premises used: monotone_transfiniteIterate, Order.succ_le_of_lt
-- Module: Mathlib.Order.TransfiniteIteration
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 φ (Order.succ j₁) i₀ ≤ transfiniteIterate φ j₂ i₀

Tactic:
exact monotone_transfiniteIterate _ _ hφ (Order.succ_le_of_lt hj)

Premises used: monotone_transfiniteIterate, Order.succ_le_of_lt
-- Module: Mathlib.Order.TypeTags
Goal:
α : Type u_1
C : WithBot α → Sort u_2
d : C ⊥
f : (a : α) → C (↑a : WithBot α)
⊢ recBotCoe (C := C) d f ⊥ = d

Tactic:
rfl

Premises used: WithBot.recBotCoe, rfl
-- Module: Mathlib.Order.TypeTags
Goal:
α : Type u_1
C : WithBot α → Sort u_2
d : C ⊥
f : (a : α) → C (↑a : WithBot α)
x : α
⊢ recBotCoe (C := C) d f (↑x : WithBot α) = f x

Tactic:
rfl

Premises used: WithBot.recBotCoe, rfl
-- Module: Mathlib.Order.Types.Arithmetic
Goal:
⊢ ZeroLEOneClass OrderType.{u_1}

Tactic:
⟨OrderType.zero_le _⟩

Premises used: ZeroLEOneClass.mk, OrderType.zero_le
-- Module: Mathlib.Order.Types.Arithmetic
Goal:
α : Type u
β : Type v
inst : LinearOrder α
inst_1 : LinearOrder β
⊢ type (Lex (α ⊕ β)) = type α + type β

Tactic:
simp [HAdd.hAdd]

Premises used: HAdd.hAdd
-- Module: Mathlib.Order.Types.Arithmetic
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 γ)

Tactic:
simp only [← type_lex_sum, (OrderIso.sumLexAssoc α β γ).type_congr]

Premises used: OrderIso.sumLexAssoc, OrderIso.type_congr, OrderType.type_lex_sum
-- Module: Mathlib.Order.Types.Arithmetic
Goal:
o : OrderType.{u}
α : Type u
x : LinearOrder α
⊢ 0 = type PEmpty.{?u.31182 + 1}

Tactic:
rfl
-- Module: Mathlib.Order.Types.Arithmetic
Goal:
o : OrderType.{u}
α : Type u
x : LinearOrder α
simp : type (Lex (PEmpty.{u + 1} ⊕ α)) = type α
⊢ 0 + type α = type α

Tactic:
simp only [show 0 = type PEmpty by rfl, ← type_lex_sum]

Premises used: OrderType.type_lex_sum
-- Module: Mathlib.Order.Types.Arithmetic
Goal:
o : OrderType.{u}
α : Type u
x : LinearOrder α
⊢ type (Lex (PEmpty.{u + 1} ⊕ α)) = type α

Tactic:
(OrderIso.emptySumLex (β := PEmpty) (α := α)).type_congr

Premises used: OrderIso.emptySumLex, OrderIso.type_congr
-- Module: Mathlib.Order.Types.Arithmetic
Goal:
o : OrderType.{u}
α : Type u
x : LinearOrder α
⊢ type (Lex (PEmpty.{u + 1} ⊕ α)) = type α

Tactic:
exact (OrderIso.emptySumLex (β := PEmpty) (α := α)).type_congr

Premises used: OrderIso.emptySumLex, OrderIso.type_congr
-- Module: Mathlib.Order.Types.Arithmetic
Goal:
o : OrderType.{u}
α : Type u
x : LinearOrder α
⊢ 0 = type PEmpty.{?u.31903 + 1}

Tactic:
rfl
-- Module: Mathlib.Order.Types.Arithmetic
Goal:
o : OrderType.{u}
α : Type u
x : LinearOrder α
simp : type (Lex (α ⊕ PEmpty.{u + 1})) = type α
⊢ type α + 0 = type α

Tactic:
simp only [show 0 = type PEmpty by rfl, ← type_lex_sum]

Premises used: OrderType.type_lex_sum
-- Module: Mathlib.Order.Types.Arithmetic
Goal:
o : OrderType.{u}
α : Type u
x : LinearOrder α
⊢ type (Lex (α ⊕ PEmpty.{u + 1})) = type α

Tactic:
(OrderIso.sumLexEmpty (β := PEmpty) (α := α)).type_congr

Premises used: OrderIso.sumLexEmpty, OrderIso.type_congr
-- Module: Mathlib.Order.Types.Arithmetic
Goal:
o : OrderType.{u}
α : Type u
x : LinearOrder α
⊢ type (Lex (α ⊕ PEmpty.{u + 1})) = type α

Tactic:
exact (OrderIso.sumLexEmpty (β := PEmpty) (α := α)).type_congr

Premises used: OrderIso.sumLexEmpty, OrderIso.type_congr
-- Module: Mathlib.Order.Types.Arithmetic
Goal:
α : Type u
β : Type v
inst : LinearOrder α
inst_1 : LinearOrder β
⊢ type (Lex (α × β)) = type β * type α

Tactic:
simp [HMul.hMul]

Premises used: HMul.hMul
-- Module: Mathlib.Order.Types.Arithmetic
Goal:
o₁ o₂ o₃ : OrderType.{u}
α : Type u
x : LinearOrder α
β : Type u
x_1 : LinearOrder β
γ : Type u
x_2 : LinearOrder γ
simp : type (Lex (γ × Lex (β × α))) = type (Lex (Lex (γ × β) × α))
⊢ type α * type β * type γ = type α * (type β * type γ)

Tactic:
simp only [← type_lex_prod]

Premises used: OrderType.type_lex_prod
-- Module: Mathlib.Order.Types.Arithmetic
Goal:
o₁ o₂ o₃ : OrderType.{u}
α : Type u
x : LinearOrder α
β : Type u
x_1 : LinearOrder β
γ : Type u
x_2 : LinearOrder γ
⊢ type (Lex (γ × Lex (β × α))) = type (Lex (Lex (γ × β) × α))

Tactic:
(Prod.Lex.prodLexAssoc γ β α).symm.type_congr

Premises used: OrderIso.type_congr, OrderIso.symm, Prod.Lex.prodLexAssoc
-- Module: Mathlib.Order.Types.Arithmetic
Goal:
o₁ o₂ o₃ : OrderType.{u}
α : Type u
x : LinearOrder α
β : Type u
x_1 : LinearOrder β
γ : Type u
x_2 : LinearOrder γ
⊢ type (Lex (γ × Lex (β × α))) = type (Lex (Lex (γ × β) × α))

Tactic:
exact (Prod.Lex.prodLexAssoc γ β α).symm.type_congr

Premises used: OrderIso.type_congr, OrderIso.symm, Prod.Lex.prodLexAssoc
-- Module: Mathlib.Order.Types.Arithmetic
Goal:
o : OrderType.{u}
α : Type u
x : LinearOrder α
⊢ 1 = type PUnit.{?u.56950 + 1}

Tactic:
rfl
-- Module: Mathlib.Order.Types.Arithmetic
Goal:
o : OrderType.{u}
α : Type u
x : LinearOrder α
simp : type (Lex (α × PUnit.{u + 1})) = type α
⊢ 1 * type α = type α

Tactic:
simp only [show 1 = type PUnit by rfl, ← type_lex_prod]

Premises used: OrderType.type_lex_prod
-- Module: Mathlib.Order.Types.Arithmetic
Goal:
o : OrderType.{u}
α : Type u
x : LinearOrder α
⊢ type (Lex (α × PUnit.{u + 1})) = type α

Tactic:
(Prod.Lex.prodUnique α PUnit).type_congr

Premises used: OrderIso.type_congr, Prod.Lex.prodUnique, PUnit
-- Module: Mathlib.Order.Types.Arithmetic
Goal:
o : OrderType.{u}
α : Type u
x : LinearOrder α
⊢ type (Lex (α × PUnit.{u + 1})) = type α

Tactic:
exact (Prod.Lex.prodUnique α PUnit).type_congr

Premises used: OrderIso.type_congr, Prod.Lex.prodUnique, PUnit
-- Module: Mathlib.Order.Types.Arithmetic
Goal:
o : OrderType.{u}
α : Type u
x : LinearOrder α
⊢ 1 = type PUnit.{?u.57444 + 1}

Tactic:
rfl
-- Module: Mathlib.Order.Types.Arithmetic
Goal:
o : OrderType.{u}
α : Type u
x : LinearOrder α
simp : type (Lex (PUnit.{u + 1} × α)) = type α
⊢ type α * 1 = type α

Tactic:
simp only [show 1 = type PUnit by rfl, ← type_lex_prod]

Premises used: OrderType.type_lex_prod
-- Module: Mathlib.Order.Types.Arithmetic
Goal:
o : OrderType.{u}
α : Type u
x : LinearOrder α
⊢ type (Lex (PUnit.{u + 1} × α)) = type α

Tactic:
(Prod.Lex.uniqueProd PUnit α).type_congr

Premises used: OrderIso.type_congr, PUnit, Prod.Lex.uniqueProd
-- Module: Mathlib.Order.Types.Arithmetic
Goal:
o : OrderType.{u}
α : Type u
x : LinearOrder α
⊢ type (Lex (PUnit.{u + 1} × α)) = type α

Tactic:
exact (Prod.Lex.uniqueProd PUnit α).type_congr

Premises used: OrderIso.type_congr, PUnit, Prod.Lex.uniqueProd
-- Module: Mathlib.Order.Types.Arithmetic
Goal:
α : Type u
inst : LinearOrder α
rw : (type α).liftOn (fun (α : Type u) (x : LinearOrder α) ↦ #α) card._proof_1 = #α
rw₁ rw₂ : #α = #α
⊢ (type α).card = #α

Tactic:
rw [card, liftOn_type]

Premises used: OrderType.liftOn_type, OrderType.card
-- Module: Mathlib.Order.Types.Arithmetic
Goal:
o₁ o₂ : OrderType.{u_1}
x : Type u_1
x_1 : LinearOrder x
x_2 : Type u_1
x_3 : LinearOrder x_2
hle : type x ≤ type x_2
⊢ (type x).card ≤ (type x_2).card

Tactic:
simp [card, (type_le_type_iff.mp hle).some.cardinal_le]

Premises used: Nonempty.some, RelEmbedding.toEmbedding, OrderType.card, OrderType.type_le_type_iff, Iff.mp, Function.Embedding.cardinal_le
-- Module: Mathlib.Order.Types.Arithmetic
Goal:
⊢ Monotone card

Tactic:
@card_mono

Premises used: Monotone, OrderType.card_mono
-- Module: Mathlib.Order.Types.Arithmetic
Goal:
⊢ card 0 = 0

Tactic:
simpa using card_type (α := PEmpty)

Premises used: OrderType.card_type
-- Module: Mathlib.Order.Types.Arithmetic
Goal:
⊢ card 1 = 1

Tactic:
simpa using card_type (α := PUnit)

Premises used: OrderType.card_type
-- Module: Mathlib.Order.Types.Arithmetic
Goal:
a b c : OrderType.{u_1}
⊢ a * (b + c) = a * b + a * c

Tactic:
inductionOn₃ a b c (fun _ _ _ _ _ _ ↦ ?_)

Premises used: OrderType.inductionOn₃
-- Module: Mathlib.Order.Types.Arithmetic
Goal:
a b c : OrderType.{u_1}
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
⊢ a * (b + c) = a * b + a * c

Tactic:
refine inductionOn₃ a b c (fun _ _ _ _ _ _ ↦ ?_)
-- Module: Mathlib.Order.Types.Arithmetic
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
simp : type (Lex (Lex (x_2 ⊕ x_4) × x)) = type (Lex (Lex (x_2 × x) ⊕ Lex (x_4 × x)))
⊢ type x * (type x_2 + type x_4) = type x * type x_2 + type x * type x_4

Tactic:
simp only [← type_lex_prod, ← type_lex_sum]

Premises used: OrderType.type_lex_prod, OrderType.type_lex_sum
-- Module: Mathlib.Order.Types.Arithmetic
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 (Lex (Lex (x_2 ⊕ x_4) × x)) = type (Lex (Lex (x_2 × x) ⊕ Lex (x_4 × x)))

Tactic:
(Prod.Lex.sumLexProdLexDistrib _ _ _).type_congr

Premises used: OrderIso.type_congr
-- Module: Mathlib.Order.Types.Arithmetic
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 (Lex (Lex (x_2 ⊕ x_4) × x)) = type (Lex (Lex (x_2 × x) ⊕ Lex (x_4 × x)))

Tactic:
exact (Prod.Lex.sumLexProdLexDistrib _ _ _).type_congr

Premises used: OrderIso.type_congr
-- Module: Mathlib.Order.Types.Defs
Goal:
o : OrderType.{u_1}
⊢ type o.ToType = o

Tactic:
surjInv_eq Quot.exists_rep o

Premises used: OrderType.type, Quot.exists_rep, OrderType.ToType, Function.surjInv, Quotient, Function.surjInv_eq, Classical.choose, OrderType
-- Module: Mathlib.Order.Types.Defs
Goal:
α β : Type u
inst : LinearOrder α
inst_1 : LinearOrder β
⊢ type α = type β ↔ Nonempty.{u + 1} (α ≃o β)

Tactic:
Quotient.eq'

Premises used: OrderType.type, Quotient.eq', Quotient.mk', OrderType
-- Module: Mathlib.Order.Types.Defs
Goal:
α β : Type u
inst : LinearOrder α
inst_1 : LinearOrder β
h : α ≃o β
⊢ type α = type β

Tactic:
type_eq_type.2 ⟨h⟩

Premises used: Iff.mpr, OrderType.type_eq_type, Nonempty.intro
-- Module: Mathlib.Order.Types.Defs
Goal:
α : Type u
inst : LinearOrder α
inst_1 : IsEmpty α
⊢ type α = 0

Tactic:
type_congr <| .ofIsEmpty α PEmpty

Premises used: OrderIso.ofIsEmpty, PEmpty, OrderType.type_congr
-- Module: Mathlib.Order.Types.Defs
Goal:
α : Type u
inst : LinearOrder α
⊢ type α ≠ 0 ↔ Nonempty α

Tactic:
simp [type_eq_zero]

Premises used: OrderType.type_eq_zero
-- Module: Mathlib.Order.Types.Defs
Goal:
α : Type u
inst : LinearOrder α
h : Nonempty α
⊢ type α ≠ 0

Tactic:
type_ne_zero_iff.2 h

Premises used: Iff.mpr, OrderType.type_ne_zero_iff
-- Module: Mathlib.Order.Types.Defs
Goal:
α : Type u
inst : LinearOrder α
inst_1 : Nonempty α
inst_2 : Subsingleton α
intro : ∀ (val : Unique α), type α = 1
⊢ type α = 1

Tactic:
cases nonempty_unique α

Premises used: nonempty_unique
-- Module: Mathlib.Order.Types.Defs
Goal:
α : Type u
inst : LinearOrder α
inst_1 : Nonempty α
inst_2 : Subsingleton α
val : Unique α
⊢ type α = 1

Tactic:
(OrderIso.ofUnique α _).type_congr

Premises used: OrderIso.type_congr, OrderIso.ofUnique
-- Module: Mathlib.Order.Types.Defs
Goal:
α : Type u
inst : LinearOrder α
inst_1 : Nonempty α
inst_2 : Subsingleton α
val : Unique α
⊢ type α = 1

Tactic:
exact (OrderIso.ofUnique α _).type_congr

Premises used: OrderIso.type_congr, OrderIso.ofUnique
-- Module: Mathlib.Order.Types.Defs
Goal:
α : Type u
inst : LinearOrder α
⊢ type α = 1 ↔ Nonempty.{max 1 (u + 1)} (Unique α)

Tactic:
⟨fun h ↦ let ⟨s⟩ := type_eq_type.1 h; ⟨s.toEquiv.unique⟩,
    fun ⟨_⟩ ↦ type_of_unique⟩

Premises used: Equiv.unique, OrderType.type_of_unique, Unique, OrderType.type, _private.0.OrderType.type_eq_one.match_1, OrderType.type_eq_type, _private.0.OrderType.type_eq_one.match_2, Nonempty.intro, Iff.intro, Iff.mp, Nonempty, RelIso.toEquiv, OfNat.ofNat, Eq
-- Module: Mathlib.Order.Types.Defs
Goal:
o : OrderType.{u_1}
rw : type o.ToType = 0 ↔ o = 0
rw₁ rw₂ : o = 0 ↔ o = 0
⊢ IsEmpty.{u_1 + 1} o.ToType ↔ o = 0

Tactic:
rw [← @type_eq_zero o.ToType, type_toType]

Premises used: OrderType.type_eq_zero, OrderType.type_toType
-- Module: Mathlib.Order.Types.Defs
Goal:
o : OrderType.{u_1}
rw : type o.ToType ≠ 0 ↔ o ≠ 0
rw₁ rw₂ : o ≠ 0 ↔ o ≠ 0
⊢ Nonempty.{u_1 + 1} o.ToType ↔ o ≠ 0

Tactic:
rw [← @type_ne_zero_iff o.ToType, type_toType]

Premises used: OrderType.type_ne_zero_iff, OrderType.type_toType
-- Module: Mathlib.Order.Types.Defs
Goal:
α β : Type u
inst : LinearOrder α
inst_1 : LinearOrder β
δ : Sort v
⊢ Nontrivial OrderType.{u}

Tactic:
⟨⟨1, 0, type_ne_zero⟩⟩

Premises used: OrderType.type_ne_zero, Nontrivial.mk, Exists.intro, OfNat.ofNat
-- Module: Mathlib.Order.Types.Defs
Goal:
C : OrderType.{u_1} → Prop
o : OrderType.{u_1}
H : ∀ (α : Type u_1) [inst : LinearOrder α], C (type α)
⊢ C o

Tactic:
Quot.inductionOn o (fun α ↦ H α)

Premises used: Quot.inductionOn
-- Module: Mathlib.Order.Types.Defs
Goal:
C : OrderType.{u_1} → OrderType.{u_2} → Prop
o₁ : OrderType.{u_1}
o₂ : OrderType.{u_2}
H : ∀ (α : Type u_1) [inst : LinearOrder α] (β : Type u_2) [inst_1 : LinearOrder β], C (type α) (type β)
⊢ C o₁ o₂

Tactic:
Quotient.inductionOn₂ o₁ o₂ fun α β ↦ H α β

Premises used: Quotient.inductionOn₂
-- Module: Mathlib.Order.Types.Defs
Goal:
C : OrderType.{u_1} → OrderType.{u_2} → OrderType.{u_3} → Prop
o₁ : OrderType.{u_1}
o₂ : OrderType.{u_2}
o₃ : OrderType.{u_3}
H :
  ∀ (α : Type u_1) [inst : LinearOrder α] (β : Type u_2) [inst_1 : LinearOrder β] (γ : Type u_3)
    [inst_2 : LinearOrder γ], C (type α) (type β) (type γ)
⊢ C o₁ o₂ o₃

Tactic:
Quotient.inductionOn₃ o₁ o₂ o₃ fun α β γ ↦
    H α β γ

Premises used: Quotient.inductionOn₃
-- Module: Mathlib.Order.Types.Defs
Goal:
δ : Sort v
f : (α : Type u_1) → [LinearOrder α] → δ
c : ∀ (α : Type u_1) [inst : LinearOrder α] (β : Type u_1) [inst_1 : LinearOrder β], type α = type β → f α = f β
γ : Type u_1
inst : LinearOrder γ
⊢ (type γ).liftOn f c = f γ

Tactic:
rfl
-- Module: Mathlib.Order.Types.Defs
Goal:
α : Type u
β : Type v
δ : Type u_1
inst : LinearOrder α
inst_1 : LinearOrder β
f : (α : Type u) → [LinearOrder α] → (β : Type v) → [LinearOrder β] → δ
c :
  ∀ (α₁ : Type u) [inst : LinearOrder α₁] (β₁ : Type v) [inst_2 : LinearOrder β₁] (α₂ : Type u)
    [inst_3 : LinearOrder α₂] (β₂ : Type v) [inst_4 : LinearOrder β₂],
    type α₁ = type α₂ → type β₁ = type β₂ → f α₁ β₁ = f α₂ β₂
⊢ (type α).liftOn₂ (type β) f c = f α β

Tactic:
rfl
-- Module: Mathlib.Order.Types.Defs
Goal:
α β : Type u
inst : LinearOrder α
inst_1 : LinearOrder β
δ : Sort v
⊢ NeZero.{u_1 + 1} (R := OrderType.{u_1}) 1

Tactic:
⟨type_ne_zero⟩

Premises used: NeZero.mk, OrderType.type_ne_zero
-- Module: Mathlib.Order.Types.Defs
Goal:
α β : Type u
inst : LinearOrder α
inst_1 : LinearOrder β
⊢ type α ≤ type β ↔ Nonempty.{u + 1} (α ↪o β)

Tactic:
.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Order.Types.Defs
Goal:
α β : Type u
inst : LinearOrder α
inst_1 : LinearOrder β
h : α ↪o β
⊢ type α ≤ type β

Tactic:
⟨h⟩

Premises used: Nonempty.intro
-- Module: Mathlib.Order.Types.Defs
Goal:
α β : Type u
inst : LinearOrder α
inst_1 : LinearOrder β
h : α ↪o β
hne : IsEmpty.{u + 1} (β ↪o α)
⊢ type α < type β

Tactic:
⟨⟨h⟩, not_nonempty_iff.mpr hne⟩

Premises used: Iff.mpr, Nonempty.intro, not_nonempty_iff, And.intro
-- Module: Mathlib.Order.Types.Defs
Goal:
o : OrderType.{u_1}
⊢ 0 ≤ o

Tactic:
inductionOn o fun _ ↦ OrderEmbedding.ofIsEmpty.type_le_type

Premises used: OrderType.inductionOn
-- Module: Mathlib.Order.Types.Defs
Goal:
⊢ Eq.{u_1 + 2} (α := OrderType.{u_1}) ⊥ 0

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Order.Types.Defs
Goal:
o : OrderType.{u_1}
⊢ ¬o < 0

Tactic:
not_lt_bot

Premises used: not_lt_bot
-- Module: Mathlib.Order.Types.Defs
Goal:
o : OrderType.{u_1}
ho : o ≠ 0
⊢ Nonempty.{u_1 + 1} o.ToType

Tactic:
have := nonempty_toType_iff.2 ho
-- Module: Mathlib.Order.Types.Defs
Goal:
o : OrderType.{u_1}
ho : o ≠ 0
this : Nonempty.{u_1 + 1} o.ToType
rw : 0 < type o.ToType
⊢ 0 < o

Tactic:
rw [← type_toType o]

Premises used: OrderType.type_toType
-- Module: Mathlib.Order.Types.Defs
Goal:
o : OrderType.{u_1}
ho : o ≠ 0
this : Nonempty.{u_1 + 1} o.ToType
⊢ 0 < type o.ToType

Tactic:
⟨⟨Function.Embedding.ofIsEmpty, nofun⟩, fun ⟨f⟩ ↦ IsEmpty.elim inferInstance f.toFun⟩

Premises used: RelEmbedding.mk, False, Function.Embedding.ofIsEmpty, IsEmpty.elim, inferInstance, RelEmbedding.toEmbedding, LE.le, Nonempty.intro, _private.0.OrderType.pos_iff_ne_zero.match_1, Iff, And.intro, _private.0.OrderType.pos_iff_ne_zero.match_2, Function.Embedding.toFun, DFunLike.coe
-- Module: Mathlib.Order.Types.Defs
Goal:
o : OrderType.{u_1}
ho : o ≠ 0
this : Nonempty.{u_1 + 1} o.ToType
⊢ 0 < type o.ToType

Tactic:
exact ⟨⟨Function.Embedding.ofIsEmpty, nofun⟩, fun ⟨f⟩ ↦ IsEmpty.elim inferInstance f.toFun⟩
-- Module: Mathlib.Order.Types.Defs
Goal:
α : Type u
inst : LinearOrder α
⊢ type (ULift.{v, u} α) = lift.{v, u} (type α)

Tactic:
(rfl)

Premises used: OrderType.liftOn, OrderType.lift, rfl
-- Module: Mathlib.Order.Types.Defs
Goal:
o : OrderType.{max u v}
⊢ lift.{u, max u v} o = o

Tactic:
inductionOn o fun _ ↦ type_congr ULift.orderIso

Premises used: OrderType.inductionOn
-- Module: Mathlib.Order.Types.Defs
Goal:
o : OrderType.{u}
⊢ lift.{u, u} o = o

Tactic:
lift_id'.{u, u} o

Premises used: OrderType.lift_id'
-- Module: Mathlib.Order.Types.Defs
Goal:
o : OrderType.{u}
⊢ lift.{0, u} o = o

Tactic:
lift_id'.{0, u} o

Premises used: OrderType.lift_id'
-- Module: Mathlib.Order.Types.Defs
Goal:
o : OrderType.{u_1}
⊢ lift.{u, max v u_1} (lift.{v, u_1} o) = lift.{max v u, u_1} o

Tactic:
inductionOn o fun _ ↦
    (ULift.orderIso.trans <| ULift.orderIso.trans ULift.orderIso.symm).type_congr

Premises used: OrderType.inductionOn
-- Module: Mathlib.Order.Types.Defs
Goal:
α β : Type u
inst : LinearOrder α
inst_1 : LinearOrder β
⊢ lift.{u_1, u} (type α) = lift.{u_1, u} (type β) ↔ Nonempty.{u + 1} (α ≃o β)

Tactic:
⟨fun h ↦ ?_, fun ⟨h⟩ ↦ congrArg lift <| type_congr h⟩

Premises used: _private.0.OrderType.lift_type_eq_iff.match_1, congrArg, OrderType.type, OrderType.lift, Iff.intro, OrderType.type_congr, Eq
-- Module: Mathlib.Order.Types.Defs
Goal:
α β : Type u
inst : LinearOrder α
inst_1 : LinearOrder β
refine : ∀ (h : lift.{u_1, u} (type α) = lift.{u_1, u} (type β)), Nonempty.{u + 1} (α ≃o β)
⊢ 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⟩
-- Module: Mathlib.Order.Types.Defs
Goal:
α β : Type u
inst : LinearOrder α
inst_1 : LinearOrder β
h : lift.{u_1, u} (type α) = lift.{u_1, u} (type β)
⊢ Nonempty (ULift.{u_1, u} α ≃o ULift.{u_1, u} β)

Tactic:
rw [← type_ulift, ← type_ulift, type_eq_type] at h

Premises used: OrderType.type_eq_type, OrderType.type_ulift
-- Module: Mathlib.Order.Types.Defs
Goal:
α β : Type u
inst : LinearOrder α
inst_1 : LinearOrder β
h : Nonempty (ULift.{u_1, u} α ≃o ULift.{u_1, u} β)
⊢ Nonempty.{u + 1} (α ≃o β)

Tactic:
⟨(ULift.orderIso.symm.trans h.some).trans ULift.orderIso⟩

Premises used: ULift.orderIso, Nonempty.some, Nonempty.intro, OrderIso.symm, OrderIso.trans
-- Module: Mathlib.Order.Types.Defs
Goal:
α β : Type u
inst : LinearOrder α
inst_1 : LinearOrder β
h : Nonempty (ULift.{u_1, u} α ≃o ULift.{u_1, u} β)
⊢ Nonempty.{u + 1} (α ≃o β)

Tactic:
exact ⟨(ULift.orderIso.symm.trans h.some).trans ULift.orderIso⟩
-- Module: Mathlib.Order.Types.Defs
Goal:
α β : Type u
inst : LinearOrder α
inst_1 : LinearOrder β
⊢ lift.{u_1, u} (type α) ≤ lift.{u_1, u} (type β) ↔ Nonempty.{u + 1} (α ↪o β)

Tactic:
⟨fun h ↦ ?_, fun ⟨h⟩ ↦ type_le_type <| (ULift.orderIso.toOrderEmbedding.trans h).trans
   ULift.orderIso.symm.toOrderEmbedding⟩

Premises used: OrderType.type_le_type, OrderIso.toOrderEmbedding, ULift.orderIso, OrderType.type, LE.le, OrderIso.symm, _private.0.OrderType.lift_type_le_iff.match_1, OrderType.lift, Iff.intro, RelEmbedding.trans