mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Order.Module.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
a✝ a₁ a₂ : α
b b₁✝ b₂ : β
inst✝⁵ : Zero α
inst✝⁴ : Zero β
inst✝³ : SMulWithZero α β
inst✝² : PartialOrder α
inst✝¹ : PartialOrder β
inst✝ : PosSMulReflectLE α β
a : α
ha : 0 < a
b₁ : β
h : a • b₁ < a • b₁
⊢ False

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
a✝ a₁ a₂ : α
b b₁✝ b₂ : β
inst✝⁵ : Zero α
inst✝⁴ : Zero β
inst✝³ : SMulWithZero α β
inst✝² : PartialOrder α
inst✝¹ : PartialOrder β
inst✝ : PosSMulReflectLE α β
a : α
ha : 0 < a
b₁ : β
h : a • b₁ < a • b₁
⊢ False
Module: Mathlib.Algebra.Order.Module.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
a a₁✝ a₂ : α
b✝ b₁ b₂ : β
inst✝⁵ : Zero α
inst✝⁴ : Zero β
inst✝³ : SMulWithZero α β
inst✝² : PartialOrder α
inst✝¹ : PartialOrder β
inst✝ : SMulPosReflectLE α β
b : β
hb : 0 < b
a₁ : α
h : a₁ • b < a₁ • b
⊢ False

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
a a₁✝ a₂ : α
b✝ b₁ b₂ : β
inst✝⁵ : Zero α
inst✝⁴ : Zero β
inst✝³ : SMulWithZero α β
inst✝² : PartialOrder α
inst✝¹ : PartialOrder β
inst✝ : SMulPosReflectLE α β
b : β
hb : 0 < b
a₁ : α
h : a₁ • b < a₁ • b
⊢ False
Module: Mathlib.Algebra.Order.Module.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
a₁ : α
b₁ : β
inst✝⁶ : Zero α
inst✝⁵ : Zero β
inst✝⁴ : SMulWithZero α β
inst✝³ : PartialOrder α
inst✝² : PartialOrder β
inst✝¹ : PosSMulStrictMono α β
inst✝ : SMulPosStrictMono α β
h₁ : 0 < a₁
ha : a₁ ≤ a₁
hb : b₁ ≤ b₁
h₂ : 0 < b₁
⊢ a₁ • b₁ = a₁ • b₁

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
a₁ : α
b₁ : β
inst✝⁶ : Zero α
inst✝⁵ : Zero β
inst✝⁴ : SMulWithZero α β
inst✝³ : PartialOrder α
inst✝² : PartialOrder β
inst✝¹ : PosSMulStrictMono α β
inst✝ : SMulPosStrictMono α β
h₁ : 0 < a₁
ha : a₁ ≤ a₁
hb : b₁ ≤ b₁
h₂ : 0 < b₁
⊢ a₁ • b₁ = a₁ • b₁
Module: Mathlib.Algebra.Order.Module.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
a₁ : α
b₁ : β
inst✝⁶ : Zero α
inst✝⁵ : Zero β
inst✝⁴ : SMulWithZero α β
inst✝³ : PartialOrder α
inst✝² : PartialOrder β
inst✝¹ : PosSMulStrictMono α β
inst✝ : SMulPosStrictMono α β
h₁ : 0 < b₁
ha : a₁ ≤ a₁
h₂ : 0 < a₁
hb : b₁ ≤ b₁
⊢ a₁ • b₁ = a₁ • b₁

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
a₁ : α
b₁ : β
inst✝⁶ : Zero α
inst✝⁵ : Zero β
inst✝⁴ : SMulWithZero α β
inst✝³ : PartialOrder α
inst✝² : PartialOrder β
inst✝¹ : PosSMulStrictMono α β
inst✝ : SMulPosStrictMono α β
h₁ : 0 < b₁
ha : a₁ ≤ a₁
h₂ : 0 < a₁
hb : b₁ ≤ b₁
⊢ a₁ • b₁ = a₁ • b₁
Module: Mathlib.RingTheory.Finiteness.Basic

Goal state before:
pp: case insert
R : Type u_4
M : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
motive : (N : Submodule R M) → N.FG → Prop
bot : motive ⊥ ⋯
sup : ∀ (N : Submodule R M) (x : M) (hN : N.FG), motive N hN → motive (N ⊔ R ∙ x) ⋯
x : M
s : Finset M
hxs : x ∉ s
ih : motive (span R ↑s) ⋯
⊢ motive (span R ↑(insert x s)) ⋯

Tactic:
simpa [span_insert, sup_comm] using sup (span R s) x (by use s) ih

Goal state after:
Module: Mathlib.Algebra.Order.Module.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁸ : Semiring α
inst✝⁷ : PartialOrder α
inst✝⁶ : IsStrictOrderedRing α
inst✝⁵ : ExistsAddOfLE α
inst✝⁴ : AddCommMonoid β
inst✝³ : PartialOrder β
inst✝² : IsOrderedCancelAddMonoid β
inst✝¹ : Module α β
inst✝ : PosSMulMono α β
a₁ a₂ : α
b₁ b₂ : β
ha : a₂ ≤ a₁
hb : b₂ ≤ b₁
⊢ a₂ • b₁ + a₁ • b₂ ≤ a₂ • b₂ + a₁ • b₁

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁸ : Semiring α
inst✝⁷ : PartialOrder α
inst✝⁶ : IsStrictOrderedRing α
inst✝⁵ : ExistsAddOfLE α
inst✝⁴ : AddCommMonoid β
inst✝³ : PartialOrder β
inst✝² : IsOrderedCancelAddMonoid β
inst✝¹ : Module α β
inst✝ : PosSMulMono α β
a₁ a₂ : α
b₁ b₂ : β
ha : a₂ ≤ a₁
hb : b₂ ≤ b₁
⊢ a₂ • b₁ + a₁ • b₂ ≤ a₂ • b₂ + a₁ • b₁
Module: Mathlib.Algebra.Order.Module.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁸ : Semiring α
inst✝⁷ : PartialOrder α
inst✝⁶ : IsStrictOrderedRing α
inst✝⁵ : ExistsAddOfLE α
inst✝⁴ : AddCommMonoid β
inst✝³ : PartialOrder β
inst✝² : IsOrderedCancelAddMonoid β
inst✝¹ : Module α β
inst✝ : PosSMulStrictMono α β
a₁ a₂ : α
b₁ b₂ : β
ha : a₂ < a₁
hb : b₂ < b₁
⊢ a₂ • b₁ + a₁ • b₂ < a₂ • b₂ + a₁ • b₁

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁸ : Semiring α
inst✝⁷ : PartialOrder α
inst✝⁶ : IsStrictOrderedRing α
inst✝⁵ : ExistsAddOfLE α
inst✝⁴ : AddCommMonoid β
inst✝³ : PartialOrder β
inst✝² : IsOrderedCancelAddMonoid β
inst✝¹ : Module α β
inst✝ : PosSMulStrictMono α β
a₁ a₂ : α
b₁ b₂ : β
ha : a₂ < a₁
hb : b₂ < b₁
⊢ a₂ • b₁ + a₁ • b₂ < a₂ • b₂ + a₁ • b₁
Module: Mathlib.Algebra.Order.Module.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
a a₁✝ a₂✝ : α
b b₁ b₂ : β
inst✝⁷ : Ring α
inst✝⁶ : PartialOrder α
inst✝⁵ : IsOrderedRing α
inst✝⁴ : AddCommGroup β
inst✝³ : PartialOrder β
inst✝² : IsOrderedAddMonoid β
inst✝¹ : Module α β
inst✝ : PosSMulMono α β
_b : β
hb : 0 ≤ _b
a₁ a₂ : α
ha : a₁ ≤ a₂
⊢ 0 ≤ (a₂ - a₁) • _b

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
a a₁✝ a₂✝ : α
b b₁ b₂ : β
inst✝⁷ : Ring α
inst✝⁶ : PartialOrder α
inst✝⁵ : IsOrderedRing α
inst✝⁴ : AddCommGroup β
inst✝³ : PartialOrder β
inst✝² : IsOrderedAddMonoid β
inst✝¹ : Module α β
inst✝ : PosSMulMono α β
_b : β
hb : 0 ≤ _b
a₁ a₂ : α
ha : a₁ ≤ a₂
⊢ 0 ≤ (a₂ - a₁) • _b
Module: Mathlib.Algebra.Order.Module.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
a a₁✝ a₂✝ : α
b b₁ b₂ : β
inst✝⁷ : Ring α
inst✝⁶ : PartialOrder α
inst✝⁵ : IsOrderedRing α
inst✝⁴ : AddCommGroup β
inst✝³ : PartialOrder β
inst✝² : IsOrderedAddMonoid β
inst✝¹ : Module α β
inst✝ : PosSMulStrictMono α β
_b : β
hb : 0 < _b
a₁ a₂ : α
ha : a₁ < a₂
⊢ 0 < (a₂ - a₁) • _b

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
a a₁✝ a₂✝ : α
b b₁ b₂ : β
inst✝⁷ : Ring α
inst✝⁶ : PartialOrder α
inst✝⁵ : IsOrderedRing α
inst✝⁴ : AddCommGroup β
inst✝³ : PartialOrder β
inst✝² : IsOrderedAddMonoid β
inst✝¹ : Module α β
inst✝ : PosSMulStrictMono α β
_b : β
hb : 0 < _b
a₁ a₂ : α
ha : a₁ < a₂
⊢ 0 < (a₂ - a₁) • _b
Module: Mathlib.Algebra.Order.Module.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
a : α
b₁ b₂ : β
inst✝⁸ : Ring α
inst✝⁷ : PartialOrder α
inst✝⁶ : IsOrderedRing α
inst✝⁵ : AddCommGroup β
inst✝⁴ : PartialOrder β
inst✝³ : IsOrderedAddMonoid β
inst✝² : Module α β
inst✝¹ : PosSMulMono α β
inst✝ : PosSMulReflectLE α β
ha : a < 0
⊢ a • b₁ ≤ a • b₂ ↔ b₂ ≤ b₁

Tactic:
rw [← neg_neg a, neg_smul, neg_smul (-a), neg_le_neg_iff]
  exact smul_le_smul_iff_of_pos_left (neg_pos_of_neg ha)

Goal state after:
Module: Mathlib.Order.DirSupClosed

Goal state before:
pp: α : Type u_1
s t : Set α
D : Set (Set α)
inst✝ : Preorder α
hs : DirSupInaccOn D s
ht : DirSupInaccOn D t
⊢ DirSupClosedOn D (sᶜ ∩ tᶜ)

Tactic:
;

Goal state after:
α : Type u_1
s t : Set α
D : Set (Set α)
inst✝ : Preorder α
hs : DirSupInaccOn D s
ht : DirSupInaccOn D t
⊢ DirSupClosedOn D (sᶜ ∩ tᶜ)
Module: Mathlib.Algebra.Order.Module.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁷ : Ring α
inst✝⁶ : LinearOrder α
inst✝⁵ : IsStrictOrderedRing α
inst✝⁴ : AddCommGroup β
inst✝³ : LinearOrder β
inst✝² : IsOrderedAddMonoid β
inst✝¹ : Module α β
inst✝ : PosSMulStrictMono α β
a : α
b : β
⊢ (0 < -a → 0 ≤ -b) ∧ (0 < -b → 0 ≤ -a) ↔ (a < 0 → b ≤ 0) ∧ (b < 0 → a ≤ 0)

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁷ : Ring α
inst✝⁶ : LinearOrder α
inst✝⁵ : IsStrictOrderedRing α
inst✝⁴ : AddCommGroup β
inst✝³ : LinearOrder β
inst✝² : IsOrderedAddMonoid β
inst✝¹ : Module α β
inst✝ : PosSMulStrictMono α β
a : α
b : β
⊢ (0 < -a → 0 ≤ -b) ∧ (0 < -b → 0 ≤ -a) ↔ (a < 0 → b ≤ 0) ∧ (b < 0 → a ≤ 0)
Module: Mathlib.Algebra.Order.Module.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁷ : Ring α
inst✝⁶ : LinearOrder α
inst✝⁵ : IsStrictOrderedRing α
inst✝⁴ : AddCommGroup β
inst✝³ : LinearOrder β
inst✝² : IsOrderedAddMonoid β
inst✝¹ : Module α β
inst✝ : PosSMulStrictMono α β
a : α
b : β
⊢ (0 < a → 0 ≤ -b) ∧ (0 < -b → 0 ≤ a) ↔ (0 < a → b ≤ 0) ∧ (b < 0 → 0 ≤ a)

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁷ : Ring α
inst✝⁶ : LinearOrder α
inst✝⁵ : IsStrictOrderedRing α
inst✝⁴ : AddCommGroup β
inst✝³ : LinearOrder β
inst✝² : IsOrderedAddMonoid β
inst✝¹ : Module α β
inst✝ : PosSMulStrictMono α β
a : α
b : β
⊢ (0 < a → 0 ≤ -b) ∧ (0 < -b → 0 ≤ a) ↔ (0 < a → b ≤ 0) ∧ (b < 0 → 0 ≤ a)
Module: Mathlib.Algebra.Order.Module.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁷ : Ring α
inst✝⁶ : LinearOrder α
inst✝⁵ : IsStrictOrderedRing α
inst✝⁴ : AddCommGroup β
inst✝³ : LinearOrder β
inst✝² : IsOrderedAddMonoid β
inst✝¹ : Module α β
inst✝ : PosSMulStrictMono α β
a : α
b : β
⊢ (0 < -a → 0 ≤ b) ∧ (0 < b → 0 ≤ -a) ↔ (a < 0 → 0 ≤ b) ∧ (0 < b → a ≤ 0)

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
inst✝⁷ : Ring α
inst✝⁶ : LinearOrder α
inst✝⁵ : IsStrictOrderedRing α
inst✝⁴ : AddCommGroup β
inst✝³ : LinearOrder β
inst✝² : IsOrderedAddMonoid β
inst✝¹ : Module α β
inst✝ : PosSMulStrictMono α β
a : α
b : β
⊢ (0 < -a → 0 ≤ b) ∧ (0 < b → 0 ≤ -a) ↔ (a < 0 → 0 ≤ b) ∧ (0 < b → a ≤ 0)
Module: Mathlib.Order.DirSupClosed

Goal state before:
pp: α : Type u_1
s t : Set α
D : Set (Set α)
inst✝ : Preorder α
hDL : IsLowerSet D
hs : DirSupInaccOn D s
ht : DirSupInaccOn D t
⊢ DirSupClosedOn D (sᶜ ∪ tᶜ)

Tactic:
;

Goal state after:
α : Type u_1
s t : Set α
D : Set (Set α)
inst✝ : Preorder α
hDL : IsLowerSet D
hs : DirSupInaccOn D s
ht : DirSupInaccOn D t
⊢ DirSupClosedOn D (sᶜ ∪ tᶜ)
Module: Mathlib.Algebra.Order.Module.Defs

Goal state before:
pp: α : Type u_1
β✝ : Type u_2
a a₁ a₂ : α
b b₁ b₂ : β✝
ι : Type u_3
β : ι → Type u_4
inst✝⁵ : Zero α
inst✝⁴ : Preorder α
inst✝³ : (i : ι) → Preorder (β i)
inst✝² : (i : ι) → SMul α (β i)
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : ∀ (i : ι), SMulPosReflectLE α (β i)
_b : (i : ι) → β i
hb : 0 < _b
_a₁ _a₂ : α
h : _a₁ • _b ≤ _a₂ • _b
i : ι
hi : 0 i < _b i
⊢ _a₁ ≤ _a₂

Tactic:
;

Goal state after:
α : Type u_1
β✝ : Type u_2
a a₁ a₂ : α
b b₁ b₂ : β✝
ι : Type u_3
β : ι → Type u_4
inst✝⁵ : Zero α
inst✝⁴ : Preorder α
inst✝³ : (i : ι) → Preorder (β i)
inst✝² : (i : ι) → SMul α (β i)
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : ∀ (i : ι), SMulPosReflectLE α (β i)
_b : (i : ι) → β i
hb : 0 < _b
_a₁ _a₂ : α
h : _a₁ • _b ≤ _a₂ • _b
i : ι
hi : 0 i < _b i
⊢ _a₁ ≤ _a₂
Module: Mathlib.Algebra.Order.Module.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁶ : Preorder α
inst✝⁵ : Preorder β
inst✝⁴ : Preorder γ
inst✝³ : SMul α β
inst✝² : SMul α γ
f : β → γ
inst✝¹ : Zero α
inst✝ : PosSMulMono α γ
a : α
ha : 0 ≤ a
b₁ b₂ : β
hf : ∀ {b₁ b₂ : β}, True
smul : ∀ (a : α) (b : β), True
hb : f b₁ ≤ f b₂
⊢ a • f b₁ ≤ a • f b₂

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁶ : Preorder α
inst✝⁵ : Preorder β
inst✝⁴ : Preorder γ
inst✝³ : SMul α β
inst✝² : SMul α γ
f : β → γ
inst✝¹ : Zero α
inst✝ : PosSMulMono α γ
a : α
ha : 0 ≤ a
b₁ b₂ : β
hf : ∀ {b₁ b₂ : β}, True
smul : ∀ (a : α) (b : β), True
hb : f b₁ ≤ f b₂
⊢ a • f b₁ ≤ a • f b₂
Module: Mathlib.Algebra.Order.Module.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁶ : Preorder α
inst✝⁵ : Preorder β
inst✝⁴ : Preorder γ
inst✝³ : SMul α β
inst✝² : SMul α γ
f : β → γ
inst✝¹ : Zero α
inst✝ : PosSMulStrictMono α γ
hf : ∀ {b₁ b₂ : β}, f b₁ ≤ f b₂ ↔ b₁ ≤ b₂
a : α
ha : 0 < a
b₁ b₂ : β
smul : ∀ (a : α) (b : β), True
hb : f b₁ < f b₂
⊢ a • f b₁ < a • f b₂

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁶ : Preorder α
inst✝⁵ : Preorder β
inst✝⁴ : Preorder γ
inst✝³ : SMul α β
inst✝² : SMul α γ
f : β → γ
inst✝¹ : Zero α
inst✝ : PosSMulStrictMono α γ
hf : ∀ {b₁ b₂ : β}, f b₁ ≤ f b₂ ↔ b₁ ≤ b₂
a : α
ha : 0 < a
b₁ b₂ : β
smul : ∀ (a : α) (b : β), True
hb : f b₁ < f b₂
⊢ a • f b₁ < a • f b₂
Module: Mathlib.Algebra.Order.Module.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁶ : Preorder α
inst✝⁵ : Preorder β
inst✝⁴ : Preorder γ
inst✝³ : SMul α β
inst✝² : SMul α γ
f : β → γ
inst✝¹ : Zero α
inst✝ : PosSMulReflectLT α γ
hf : ∀ {b₁ b₂ : β}, f b₁ ≤ f b₂ ↔ b₁ ≤ b₂
a : α
ha : 0 ≤ a
b₁ b₂ : β
smul : ∀ (a : α) (b : β), True
h : a • f b₁ < a • f b₂
⊢ f b₁ < f b₂

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁶ : Preorder α
inst✝⁵ : Preorder β
inst✝⁴ : Preorder γ
inst✝³ : SMul α β
inst✝² : SMul α γ
f : β → γ
inst✝¹ : Zero α
inst✝ : PosSMulReflectLT α γ
hf : ∀ {b₁ b₂ : β}, f b₁ ≤ f b₂ ↔ b₁ ≤ b₂
a : α
ha : 0 ≤ a
b₁ b₂ : β
smul : ∀ (a : α) (b : β), True
h : a • f b₁ < a • f b₂
⊢ f b₁ < f b₂
Module: Mathlib.Algebra.Order.Module.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁷ : Preorder α
inst✝⁶ : Preorder β
inst✝⁵ : Preorder γ
inst✝⁴ : SMul α β
inst✝³ : SMul α γ
f : β → γ
inst✝² : Zero β
inst✝¹ : Zero γ
inst✝ : SMulPosMono α γ
b : β
a₁ a₂ : α
ha : a₁ ≤ a₂
hf : ∀ {b₁ b₂ : β}, True
smul : ∀ (a : α) (b : β), True
zero : True
hb : 0 ≤ f b
⊢ a₁ • f b ≤ a₂ • f b

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁷ : Preorder α
inst✝⁶ : Preorder β
inst✝⁵ : Preorder γ
inst✝⁴ : SMul α β
inst✝³ : SMul α γ
f : β → γ
inst✝² : Zero β
inst✝¹ : Zero γ
inst✝ : SMulPosMono α γ
b : β
a₁ a₂ : α
ha : a₁ ≤ a₂
hf : ∀ {b₁ b₂ : β}, True
smul : ∀ (a : α) (b : β), True
zero : True
hb : 0 ≤ f b
⊢ a₁ • f b ≤ a₂ • f b
Module: Mathlib.Order.IsNormal

Goal state before:
pp: α : Type u_1
inst✝¹ : ConditionallyCompleteLinearOrder α
inst✝ : WellFoundedLT α
f : α → α
a : α
hf : IsNormal f
hf' : BddAbove (range fun n ↦ f^[n] a)
⊢ ⨆ n, f^[n] a ∈ Function.fixedPoints f

Tactic:
rw [f.mem_fixedPoints_iff, hf.map_iSup hf']

Goal state after:
α : Type u_1
inst✝¹ : ConditionallyCompleteLinearOrder α
inst✝ : WellFoundedLT α
f : α → α
a : α
hf : IsNormal f
hf' : BddAbove (range fun n ↦ f^[n] a)
⊢ ⨆ i, f (f^[i] a) = ⨆ n, f^[n] a
Module: Mathlib.SetTheory.Ordinal.Univ

Goal state before:
pp: b : Ordinal.{max (u + 1) v}
⊢ ∀ (α : Type (max (u + 1) v)) (r : α → α → Prop) [inst : IsWellOrder α r],
    type r ∈ Set.range ⇑liftInitialSeg.toRelEmbedding ↔ type r < univ.{u, v}

Tactic:
;

Goal state after:
b : Ordinal.{max (u + 1) v}
⊢ ∀ (α : Type (max (u + 1) v)) (r : α → α → Prop) [inst : IsWellOrder α r],
    type r ∈ Set.range ⇑liftInitialSeg.toRelEmbedding ↔ type r < univ.{u, v}
Module: Mathlib.SetTheory.Ordinal.Univ

Goal state before:
pp: b : Ordinal.{max (u + 1) v}
β : Type (max (u + 1) v)
s : β → β → Prop
inst✝ : IsWellOrder β s
⊢ type s ∈ Set.range ⇑liftInitialSeg.toRelEmbedding ↔ type s < lift.{max (u + 1) v, u + 1} (typeLT Ordinal.{u})

Tactic:
;

Goal state after:
b : Ordinal.{max (u + 1) v}
β : Type (max (u + 1) v)
s : β → β → Prop
inst✝ : IsWellOrder β s
⊢ type s ∈ Set.range ⇑liftInitialSeg.toRelEmbedding ↔ type s < lift.{max (u + 1) v, u + 1} (typeLT Ordinal.{u})
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: α✝ : Type u_1
β✝ : Type u_2
γ✝ : Type u_3
r✝ : α✝ → α✝ → Prop
s✝ : β✝ → β✝ → Prop
t✝ : γ✝ → γ✝ → Prop
c a b : Ordinal.{u}
α : Type u
r : α → α → Prop
x✝³ : IsWellOrder α r
β : Type u
s : β → β → Prop
x✝² : IsWellOrder β s
γ : Type u
t : γ → γ → Prop
x✝¹ : IsWellOrder γ t
x✝ : type t + type r ≤ type t + type s
f : InitialSeg (Sum.Lex t r) (Sum.Lex t s)
⊢ type r ≤ type s

Tactic:
have H₁ a : f (Sum.inl a) = Sum.inl a := by
      simpa using ((InitialSeg.leAdd t r).trans f).eq (InitialSeg.leAdd t s) a

Goal state after:
α✝ : Type u_1
β✝ : Type u_2
γ✝ : Type u_3
r✝ : α✝ → α✝ → Prop
s✝ : β✝ → β✝ → Prop
t✝ : γ✝ → γ✝ → Prop
c a b : Ordinal.{u}
α : Type u
r : α → α → Prop
x✝³ : IsWellOrder α r
β : Type u
s : β → β → Prop
x✝² : IsWellOrder β s
γ : Type u
t : γ → γ → Prop
x✝¹ : IsWellOrder γ t
x✝ : type t + type r ≤ type t + type s
f : InitialSeg (Sum.Lex t r) (Sum.Lex t s)
H₁ : ∀ (a : γ), f (Sum.inl a) = Sum.inl a
⊢ type r ≤ type s
Module: Mathlib.SetTheory.Cardinal.Cofinality.Enum

Goal state before:
pp: α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : WellFoundedLT α
inst✝ : IsRegularCardinalOrder α
s : Set α
hs : IsCofinal s
a o : α
ho : o ∈ s
H : ∀ b < a, ↑((enum s hs) b) < o
⊢ ↑((enum s hs) a) ≤ o

Tactic:
rw [← Subtype.coe_mk o ho, Subtype.coe_le_coe, ← OrderIso.le_symm_apply]
  apply le_of_forall_lt
  simpa [OrderIso.lt_symm_apply]

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Basic

Goal state before:
pp: α β : Type u
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsWellOrder α r
inst✝ : IsWellOrder β s
f : r ≃r s
o : Ordinal.{u}
⊢ ∀ (α_1 : Type u) (r_1 : α_1 → α_1 → Prop) [inst : IsWellOrder α_1 r_1] (hr : type r_1 < type r)
    (hs : type r_1 < type s), f ((enum r) ⟨type r_1, hr⟩) = (enum s) ⟨type r_1, hs⟩

Tactic:
;

Goal state after:
α β : Type u
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsWellOrder α r
inst✝ : IsWellOrder β s
f : r ≃r s
o : Ordinal.{u}
⊢ ∀ (α_1 : Type u) (r_1 : α_1 → α_1 → Prop) [inst : IsWellOrder α_1 r_1] (hr : type r_1 < type r)
    (hs : type r_1 < type s), f ((enum r) ⟨type r_1, hr⟩) = (enum s) ⟨type r_1, hs⟩
Module: Mathlib.SetTheory.Ordinal.Basic

Goal state before:
pp: α β : Type u
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsWellOrder α r
inst✝ : IsWellOrder β s
f : r ≃r s
o : Ordinal.{u}
γ : Type u
t : γ → γ → Prop
wo : IsWellOrder γ t
g : t ≺i r
h : t ≺i s
⊢ f g.top = (g.transRelIso f).top

Tactic:
;

Goal state after:
α β : Type u
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsWellOrder α r
inst✝ : IsWellOrder β s
f : r ≃r s
o : Ordinal.{u}
γ : Type u
t : γ → γ → Prop
wo : IsWellOrder γ t
g : t ≺i r
h : t ≺i s
⊢ f g.top = (g.transRelIso f).top
Module: Mathlib.SetTheory.Ordinal.Basic

Goal state before:
pp: α : Type u
β : Type v
γ : Type w
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
ho : 0 < 0
⊢ False

Tactic:
;

Goal state after:
α : Type u
β : Type v
γ : Type w
r : α → α → Prop
s : β → β → Prop
t : γ → γ → Prop
ho : 0 < 0
⊢ False
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: α β : Type u_4
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsWellOrder α r
inst✝ : IsWellOrder β s
c : Ordinal.{u_4}
h : IsSuccLimit (type s)
H : ∀ b' < type s, type r * b' ≤ c
l : c < type r * type s
a : α
b : β
⊢ Prod.Lex s r (b, a) ((enum (Prod.Lex s r)) ⟨c, l⟩)

Tactic:
← typein_lt_typein (Prod.Lex s r),

Goal state after:
α β : Type u_4
r : α → α → Prop
s : β → β → Prop
inst✝¹ : IsWellOrder α r
inst✝ : IsWellOrder β s
c : Ordinal.{u_4}
h : IsSuccLimit (type s)
H : ∀ b' < type s, type r * b' ≤ c
l : c < type r * type s
a : α
b : β
⊢ (typein (Prod.Lex s r)).toRelEmbedding (b, a) < (typein (Prod.Lex s r)).toRelEmbedding ((enum (Prod.Lex s r)) ⟨c, l⟩)
Module: Mathlib.SetTheory.Ordinal.Enum

Goal state before:
pp: case mpr.refine_2
s : Set Ordinal.{u}
hs : ¬BddAbove s
a : Ordinal.{u}
t : Set Ordinal.{u} := {b | a ≤ enumOrd s b}
ha : a ∈ s
⊢ a ≤ enumOrd s (sInf t)

Tactic:
exact csInf_mem (s := t) ⟨a, (enumOrd_strictMono hs).id_le a⟩

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Enum

Goal state before:
pp: s t : Set Ordinal.{u}
hs : ¬BddAbove s
hst : s ⊆ t
a : Ordinal.{u}
⊢ sInf (t ∩ {b | ∀ c < a, enumOrd t c < b}) ≤ sInf (s ∩ {b | ∀ c < a, enumOrd s c < b})

Tactic:
gcongr with b c

Goal state after:
case h₁
s t : Set Ordinal.{u}
hs : ¬BddAbove s
hst : s ⊆ t
a : Ordinal.{u}
⊢ (s ∩ {b | ∀ c < a, enumOrd s c < b}).Nonempty

case h₁
s t : Set Ordinal.{u}
hs : ¬BddAbove s
hst : s ⊆ t
a b c : Ordinal.{u}
a✝ : c < a
⊢ enumOrd t c ≤ enumOrd s c
Module: Mathlib.SetTheory.Ordinal.Enum

Goal state before:
pp: s : Set Ordinal.{u}
⊢ sInf (s ∩ {b | ∀ c < 0, enumOrd s c < b}) = sInf s

Tactic:
;

Goal state after:
s : Set Ordinal.{u}
⊢ sInf (s ∩ {b | ∀ c < 0, enumOrd s c < b}) = sInf s
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: a : Ordinal.{u_4}
h : 0 < a
⊢ IsNormal fun x ↦ a * x

Tactic:
by
  refine .of_succ_lt (fun b ↦ ?_) fun hb ↦ ?_
  · simpa [mul_add_one] using (add_lt_add_iff_left (a * b)).2 h
  · simpa [IsLUB, IsLeast, upperBounds, lowerBounds, mul_le_iff_of_isSuccLimit hb] using
      fun c hc ↦ mul_le_mul_right hc.le a

Goal state after:
Module: Mathlib.Data.Nat.Log

Goal state before:
pp: n b : ℕ
hb : 1 < b
hbn : b ≤ n
hfuel : n < b ^ (0 + 1)
⊢ False

Tactic:
;

Goal state after:
n b : ℕ
hb : 1 < b
hbn : b ≤ n
hfuel : n < b ^ (0 + 1)
⊢ False
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: case inr.inl
a : Ordinal.{u_4}
l : IsSuccLimit a
b : Ordinal.{u_4}
b0 : 0 < succ b
⊢ IsSuccLimit (a * succ b)

Tactic:
rw [mul_succ]
    exact isSuccLimit_add _ l

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Basic

Goal state before:
pp: o : Ordinal.{u_1}
c : Cardinal.{u_1}
ho : o ≤ c.ord
⊢ o.card ≤ c.ord.card

Tactic:
;

Goal state after:
o : Ordinal.{u_1}
c : Cardinal.{u_1}
ho : o ≤ c.ord
⊢ o.card ≤ c.ord.card
Module: Mathlib.SetTheory.Ordinal.Basic

Goal state before:
pp: case cons.nil
α : Type u
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
o : Ordinal.{u}
a : α
as : List α
hl : (a :: as).SortedGT
hlt : ∀ i ∈ a :: as, (Ordinal.typein fun x1 x2 ↦ x1 < x2).toRelEmbedding i < o
hm : [].SortedGT
hmltl : Lex (fun x1 x2 ↦ x1 < x2) [] (a :: as)
i : α
hi : i ∈ []
⊢ (Ordinal.typein fun x1 x2 ↦ x1 < x2).toRelEmbedding i < o

Tactic:
;

Goal state after:
case cons.nil
α : Type u
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
o : Ordinal.{u}
a : α
as : List α
hl : (a :: as).SortedGT
hlt : ∀ i ∈ a :: as, (Ordinal.typein fun x1 x2 ↦ x1 < x2).toRelEmbedding i < o
hm : [].SortedGT
hmltl : Lex (fun x1 x2 ↦ x1 < x2) [] (a :: as)
i : α
hi : i ∈ []
⊢ (Ordinal.typein fun x1 x2 ↦ x1 < x2).toRelEmbedding i < o
Module: Mathlib.SetTheory.Ordinal.Family

Goal state before:
pp: α : Type u_1
β : Type u_2
o o' : Ordinal.{max u v}
f : (a : Ordinal.{max u v}) → a < o → Ordinal.{max u v w}
hf : ∀ {i j : Ordinal.{max u v}} (hi : i < o) (hj : j < o), i ≤ j → f i hi ≤ f j hj
g : (a : Ordinal.{max u v}) → a < o' → Ordinal.{max u v}
hg : o'.blsub g = o
a : Ordinal.{max u v}
ha : a < o'
⊢ g a ha < o'.blsub g

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
o o' : Ordinal.{max u v}
f : (a : Ordinal.{max u v}) → a < o → Ordinal.{max u v w}
hf : ∀ {i j : Ordinal.{max u v}} (hi : i < o) (hj : j < o), i ≤ j → f i hi ≤ f j hj
g : (a : Ordinal.{max u v}) → a < o' → Ordinal.{max u v}
hg : o'.blsub g = o
a : Ordinal.{max u v}
ha : a < o'
⊢ g a ha < o'.blsub g
Module: Mathlib.SetTheory.Ordinal.Basic

Goal state before:
pp: α : Type u
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
o : Ordinal.{u}
a : α
as : List α
hl : (a :: as).SortedGT
hlt : ∀ i ∈ a :: as, (Ordinal.typein fun x1 x2 ↦ x1 < x2).toRelEmbedding i < o
b : α
bs : List α
hm : (b :: bs).SortedGT
hmltl : Lex (fun x1 x2 ↦ x1 < x2) (b :: bs) (a :: as)
i : α
hi : i ∈ b :: bs
h : i ≤ a
⊢ (Ordinal.typein fun x1 x2 ↦ x1 < x2).toRelEmbedding i ≤ (Ordinal.typein fun x1 x2 ↦ x1 < x2).toRelEmbedding a

Tactic:
;

Goal state after:
α : Type u
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
o : Ordinal.{u}
a : α
as : List α
hl : (a :: as).SortedGT
hlt : ∀ i ∈ a :: as, (Ordinal.typein fun x1 x2 ↦ x1 < x2).toRelEmbedding i < o
b : α
bs : List α
hm : (b :: bs).SortedGT
hmltl : Lex (fun x1 x2 ↦ x1 < x2) (b :: bs) (a :: as)
i : α
hi : i ∈ b :: bs
h : i ≤ a
⊢ (Ordinal.typein fun x1 x2 ↦ x1 < x2).toRelEmbedding i ≤ (Ordinal.typein fun x1 x2 ↦ x1 < x2).toRelEmbedding a
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: a : Ordinal.{u_4}
ha : a ≠ 0
b c : Ordinal.{u_4}
⊢ a * b / (a * c) = b / c

Tactic:
convert! mul_add_div_mul (pos_iff_ne_zero.2 ha) b c using 1

Goal state after:
a : Ordinal.{u_4}
ha : a ≠ 0
b c : Ordinal.{u_4}
⊢ a * b / (a * c) = (a * b + 0) / (a * c)
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: b : Ordinal.{u_4}
h₁ : 0 ∣ b
h₂ : b ∣ 0
⊢ 0 = b

Tactic:
;

Goal state after:
b : Ordinal.{u_4}
h₁ : 0 ∣ b
h₂ : b ∣ 0
⊢ 0 = b
Module: Mathlib.SetTheory.Ordinal.Arithmetic

Goal state before:
pp: a : Ordinal.{u_4}
a0 : ¬a = 0
h₁ : a ∣ 0
h₂ : 0 ∣ a
⊢ a = 0

Tactic:
;

Goal state after:
a : Ordinal.{u_4}
a0 : ¬a = 0
h₁ : a ∣ 0
h₂ : 0 ∣ a
⊢ a = 0
Module: Mathlib.Data.Nat.Log

Goal state before:
pp: case inl
b c : ℕ
hc : 1 < c
hb : c ≤ b
⊢ log b 0 ≤ log c 0

pp: case inr
b c n : ℕ
hc : 1 < c
hb : c ≤ b
hn : n ≠ 0
⊢ log b n ≤ log c n

Tactic:
;

Goal state after:
case inl
b c : ℕ
hc : 1 < c
hb : c ≤ b
⊢ log b 0 ≤ log c 0

case inr
b c n : ℕ
hc : 1 < c
hb : c ≤ b
hn : n ≠ 0
⊢ log b n ≤ log c n