mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.SetTheory.Lists

Goal state before:
pp: case antisymm
α : Type u_1
l₁ l₂ : Lists' α true
h₁ : l₁.Subset l₂
h₂ : l₂.Subset l₁
⊢ l₁ ⊆ l₂ ∧ l₂ ⊆ l₁

Tactic:
·

Goal state after:
case antisymm
α : Type u_1
l₁ l₂ : Lists' α true
h₁ : l₁.Subset l₂
h₂ : l₂.Subset l₁
⊢ l₁ ⊆ l₂ ∧ l₂ ⊆ l₁
Module: Mathlib.SetTheory.Lists

Goal state before:
pp: case C0
α : Type u_1
trans : Lists α → Prop := ⋯
⊢ ∀ (a : α), trans (atom a)

pp: case C1
α : Type u_1
trans : Lists α → Prop := ⋯
⊢ ∀ (l : Lists' α true), (∀ (l' : Lists α), l' ∈ l.toList → trans l') → trans (of' l)

pp: case D0
α : Type u_1
trans : Lists α → Prop := ⋯
⊢ ∀ (l' : Lists α), l' ∈ Lists'.nil.toList → trans l'

pp: case D1
α : Type u_1
trans : Lists α → Prop := ⋯
⊢ ∀ (a : Lists α) (l : Lists' α true),
    trans a → (∀ (l' : Lists α), l' ∈ l.toList → trans l') → ∀ (l' : Lists α), l' ∈ (Lists'.cons a l).toList → trans l'

Tactic:
·

Goal state after:
case C0
α : Type u_1
trans : Lists α → Prop := ⋯
⊢ ∀ (a : α), trans (atom a)
Module: Mathlib.SetTheory.Ordinal.CantorNormalForm

Goal state before:
pp: case refine_2.inl
b o✝ : Ordinal.{u}
hb : 1 < b
o : Ordinal.{u}
ho : o ≠ 0
IH : (log b o, o / b ^ log b o) ∈ CNF b (o % b ^ log b o) → (log b o, o / b ^ log b o).2 < b
h : (log b o, o / b ^ log b o) ∈ (log b o, o / b ^ log b o) :: CNF b (o % b ^ log b o)
⊢ (log b o, o / b ^ log b o).2 < b

pp: case refine_2.inr
b o✝ : Ordinal.{u}
hb : 1 < b
x : Ordinal.{u} × Ordinal.{u}
o : Ordinal.{u}
ho : o ≠ 0
IH : x ∈ CNF b (o % b ^ log b o) → x.2 < b
h✝ : x ∈ (log b o, o / b ^ log b o) :: CNF b (o % b ^ log b o)
h : x ∈ CNF b (o % b ^ log b o)
⊢ x.2 < b

Tactic:
·

Goal state after:
case refine_2.inl
b o✝ : Ordinal.{u}
hb : 1 < b
o : Ordinal.{u}
ho : o ≠ 0
IH : (log b o, o / b ^ log b o) ∈ CNF b (o % b ^ log b o) → (log b o, o / b ^ log b o).2 < b
h : (log b o, o / b ^ log b o) ∈ (log b o, o / b ^ log b o) :: CNF b (o % b ^ log b o)
⊢ (log b o, o / b ^ log b o).2 < b
Module: Mathlib.SetTheory.Lists

Goal state before:
pp: case C1
α : Type u_1
trans : Lists α → Prop := ⋯
⊢ ∀ (l : Lists' α true), (∀ (l' : Lists α), l' ∈ l.toList → trans l') → trans (of' l)

pp: case D0
α : Type u_1
trans : Lists α → Prop := ⋯
⊢ ∀ (l' : Lists α), l' ∈ Lists'.nil.toList → trans l'

pp: case D1
α : Type u_1
trans : Lists α → Prop := ⋯
⊢ ∀ (a : Lists α) (l : Lists' α true),
    trans a → (∀ (l' : Lists α), l' ∈ l.toList → trans l') → ∀ (l' : Lists α), l' ∈ (Lists'.cons a l).toList → trans l'

Tactic:
·

Goal state after:
case C1
α : Type u_1
trans : Lists α → Prop := ⋯
⊢ ∀ (l : Lists' α true), (∀ (l' : Lists α), l' ∈ l.toList → trans l') → trans (of' l)
Module: Mathlib.SetTheory.Ordinal.CantorNormalForm

Goal state before:
pp: case refine_2.inr
b o✝ : Ordinal.{u}
hb : 1 < b
x : Ordinal.{u} × Ordinal.{u}
o : Ordinal.{u}
ho : o ≠ 0
IH : x ∈ CNF b (o % b ^ log b o) → x.2 < b
h✝ : x ∈ (log b o, o / b ^ log b o) :: CNF b (o % b ^ log b o)
h : x ∈ CNF b (o % b ^ log b o)
⊢ x.2 < b

Tactic:
·

Goal state after:
case refine_2.inr
b o✝ : Ordinal.{u}
hb : 1 < b
x : Ordinal.{u} × Ordinal.{u}
o : Ordinal.{u}
ho : o ≠ 0
IH : x ∈ CNF b (o % b ^ log b o) → x.2 < b
h✝ : x ∈ (log b o, o / b ^ log b o) :: CNF b (o % b ^ log b o)
h : x ∈ CNF b (o % b ^ log b o)
⊢ x.2 < b
Module: Mathlib.SetTheory.Lists

Goal state before:
pp: case C1.refl
α : Type u_1
trans : Lists α → Prop := fun l₁ ↦ ∀ ⦃l₂ l₃ : Lists α⦄, l₁ ~ l₂ → l₂ ~ l₃ → l₁ ~ l₃
l₁ : Lists' α true
IH : ∀ (l' : Lists α), l' ∈ l₁.toList → trans l'
l₃ : Lists α
h₁ : of' l₁ ~ of' l₁
h₂ : of' l₁ ~ l₃
⊢ of' l₁ ~ l₃

pp: case C1.antisymm
α : Type u_1
trans : Lists α → Prop := fun l₁ ↦ ∀ ⦃l₂ l₃ : Lists α⦄, l₁ ~ l₂ → l₂ ~ l₃ → l₁ ~ l₃
l₁ : Lists' α true
IH : ∀ (l' : Lists α), l' ∈ l₁.toList → trans l'
l₃ : Lists α
l₂✝ : Lists' α true
l₂ : l₁.Subset l₂✝
a✝ : l₂✝.Subset l₁
h₁ : of' l₁ ~ ⟨true, l₂✝⟩
h₂ : ⟨true, l₂✝⟩ ~ l₃
⊢ of' l₁ ~ l₃

Tactic:
·

Goal state after:
case C1.refl
α : Type u_1
trans : Lists α → Prop := fun l₁ ↦ ∀ ⦃l₂ l₃ : Lists α⦄, l₁ ~ l₂ → l₂ ~ l₃ → l₁ ~ l₃
l₁ : Lists' α true
IH : ∀ (l' : Lists α), l' ∈ l₁.toList → trans l'
l₃ : Lists α
h₁ : of' l₁ ~ of' l₁
h₂ : of' l₁ ~ l₃
⊢ of' l₁ ~ l₃
Module: Mathlib.SetTheory.Ordinal.FixedPointApproximants

Goal state before:
pp: case pos
α : Type u
inst✝ : CompleteLattice α
f : α →o α
x : α
a b✝ : Ordinal.{u}
hf : f (lfpApprox f x a) = lfpApprox f x a
b : Ordinal.{u}
IH : ∀ y < b, a ≤ y → lfpApprox f x y = lfpApprox f x a
hab : a ≤ b
i : Ordinal.{u}
hi : i < b
hi' : i < a
⊢ f (lfpApprox f x i) ≤ lfpApprox f x a

pp: case neg
α : Type u
inst✝ : CompleteLattice α
f : α →o α
x : α
a b✝ : Ordinal.{u}
hf : f (lfpApprox f x a) = lfpApprox f x a
b : Ordinal.{u}
IH : ∀ y < b, a ≤ y → lfpApprox f x y = lfpApprox f x a
hab : a ≤ b
i : Ordinal.{u}
hi : i < b
hi' : a ≤ i
⊢ f (lfpApprox f x i) ≤ lfpApprox f x a

Tactic:
·

Goal state after:
case pos
α : Type u
inst✝ : CompleteLattice α
f : α →o α
x : α
a b✝ : Ordinal.{u}
hf : f (lfpApprox f x a) = lfpApprox f x a
b : Ordinal.{u}
IH : ∀ y < b, a ≤ y → lfpApprox f x y = lfpApprox f x a
hab : a ≤ b
i : Ordinal.{u}
hi : i < b
hi' : i < a
⊢ f (lfpApprox f x i) ≤ lfpApprox f x a
Module: Mathlib.SetTheory.Ordinal.FixedPointApproximants

Goal state before:
pp: case neg
α : Type u
inst✝ : CompleteLattice α
f : α →o α
x : α
a b✝ : Ordinal.{u}
hf : f (lfpApprox f x a) = lfpApprox f x a
b : Ordinal.{u}
IH : ∀ y < b, a ≤ y → lfpApprox f x y = lfpApprox f x a
hab : a ≤ b
i : Ordinal.{u}
hi : i < b
hi' : a ≤ i
⊢ f (lfpApprox f x i) ≤ lfpApprox f x a

Tactic:
·

Goal state after:
case neg
α : Type u
inst✝ : CompleteLattice α
f : α →o α
x : α
a b✝ : Ordinal.{u}
hf : f (lfpApprox f x a) = lfpApprox f x a
b : Ordinal.{u}
IH : ∀ y < b, a ≤ y → lfpApprox f x y = lfpApprox f x a
hab : a ≤ b
i : Ordinal.{u}
hi : i < b
hi' : a ≤ i
⊢ f (lfpApprox f x i) ≤ lfpApprox f x a
Module: Mathlib.SetTheory.Ordinal.CantorNormalForm

Goal state before:
pp: case refine_1
b o : Ordinal.{u_1}
⊢ List.Pairwise (fun x1 x2 ↦ x1 > x2) (map Prod.fst (CNF b 0))

pp: case refine_2
b o✝ o : Ordinal.{u_1}
ho : o ≠ 0
IH : List.Pairwise (fun x1 x2 ↦ x1 > x2) (map Prod.fst (CNF b (o % b ^ log b o)))
⊢ List.Pairwise (fun x1 x2 ↦ x1 > x2) (map Prod.fst (CNF b o))

Tactic:
·

Goal state after:
case refine_1
b o : Ordinal.{u_1}
⊢ List.Pairwise (fun x1 x2 ↦ x1 > x2) (map Prod.fst (CNF b 0))
Module: Mathlib.SetTheory.Lists

Goal state before:
pp: case C1.antisymm.refl
α : Type u_1
trans : Lists α → Prop := fun l₁ ↦ ∀ ⦃l₂ l₃ : Lists α⦄, l₁ ~ l₂ → l₂ ~ l₃ → l₁ ~ l₃
l₁ : Lists' α true
IH : ∀ (l' : Lists α), l' ∈ l₁.toList → trans l'
l₂✝ : Lists' α true
l₂ : l₁.Subset l₂✝
a✝ : l₂✝.Subset l₁
h₁ : of' l₁ ~ ⟨true, l₂✝⟩
h₂ : ⟨true, l₂✝⟩ ~ ⟨true, l₂✝⟩
⊢ of' l₁ ~ ⟨true, l₂✝⟩

pp: case C1.antisymm.antisymm
α : Type u_1
trans : Lists α → Prop := fun l₁ ↦ ∀ ⦃l₂ l₃ : Lists α⦄, l₁ ~ l₂ → l₂ ~ l₃ → l₁ ~ l₃
l₁ : Lists' α true
IH : ∀ (l' : Lists α), l' ∈ l₁.toList → trans l'
l₂✝¹ : Lists' α true
l₂ : l₁.Subset l₂✝¹
a✝¹ : l₂✝¹.Subset l₁
h₁ : of' l₁ ~ ⟨true, l₂✝¹⟩
l₂✝ : Lists' α true
l₃ : l₂✝¹.Subset l₂✝
a✝ : l₂✝.Subset l₂✝¹
h₂ : ⟨true, l₂✝¹⟩ ~ ⟨true, l₂✝⟩
⊢ of' l₁ ~ ⟨true, l₂✝⟩

Tactic:
·

Goal state after:
case C1.antisymm.refl
α : Type u_1
trans : Lists α → Prop := fun l₁ ↦ ∀ ⦃l₂ l₃ : Lists α⦄, l₁ ~ l₂ → l₂ ~ l₃ → l₁ ~ l₃
l₁ : Lists' α true
IH : ∀ (l' : Lists α), l' ∈ l₁.toList → trans l'
l₂✝ : Lists' α true
l₂ : l₁.Subset l₂✝
a✝ : l₂✝.Subset l₁
h₁ : of' l₁ ~ ⟨true, l₂✝⟩
h₂ : ⟨true, l₂✝⟩ ~ ⟨true, l₂✝⟩
⊢ of' l₁ ~ ⟨true, l₂✝⟩
Module: Mathlib.SetTheory.Ordinal.FixedPointApproximants

Goal state before:
pp: case refine_1
α : Type u
inst✝ : CompleteLattice α
f : α →o α
x : α
hx : x ≤ f x
h : ∀ (o : Ordinal.{u}), lfpApprox f x o = x
⊢ f x = x

pp: case refine_2
α : Type u
inst✝ : CompleteLattice α
f : α →o α
x : α
hx : x ≤ f x
h : f x = x
o : Ordinal.{u}
⊢ lfpApprox f x o = x

Tactic:
·

Goal state after:
case refine_1
α : Type u
inst✝ : CompleteLattice α
f : α →o α
x : α
hx : x ≤ f x
h : ∀ (o : Ordinal.{u}), lfpApprox f x o = x
⊢ f x = x
Module: Mathlib.SetTheory.Ordinal.FixedPointApproximants

Goal state before:
pp: case refine_2
α : Type u
inst✝ : CompleteLattice α
f : α →o α
x : α
hx : x ≤ f x
h : f x = x
o : Ordinal.{u}
⊢ lfpApprox f x o = x

Tactic:
·

Goal state after:
case refine_2
α : Type u
inst✝ : CompleteLattice α
f : α →o α
x : α
hx : x ≤ f x
h : f x = x
o : Ordinal.{u}
⊢ lfpApprox f x o = x
Module: Mathlib.SetTheory.Ordinal.CantorNormalForm

Goal state before:
pp: case refine_2
b o✝ o : Ordinal.{u_1}
ho : o ≠ 0
IH : List.Pairwise (fun x1 x2 ↦ x1 > x2) (map Prod.fst (CNF b (o % b ^ log b o)))
⊢ List.Pairwise (fun x1 x2 ↦ x1 > x2) (map Prod.fst (CNF b o))

Tactic:
·

Goal state after:
case refine_2
b o✝ o : Ordinal.{u_1}
ho : o ≠ 0
IH : List.Pairwise (fun x1 x2 ↦ x1 > x2) (map Prod.fst (CNF b (o % b ^ log b o)))
⊢ List.Pairwise (fun x1 x2 ↦ x1 > x2) (map Prod.fst (CNF b o))
Module: Mathlib.SetTheory.Ordinal.FixedPointApproximants

Goal state before:
pp: α : Type u
inst✝ : CompleteLattice α
f : α →o α
x : α
hx : x ≤ f x
⊢ (∀ (o : Ordinal.{u}), lfpApprox f x o = x) ↔ f x = x

Tactic:
refine ⟨fun h ↦ ?_, fun h o ↦ ?_⟩
  · specialize h 1
    rwa [← zero_add 1, lfpApprox_add_one f hx, lfpApprox_zero] at h
  · have : lfpApprox f x 0 ∈ fixedPoints f := by
      rwa [mem_fixedPoints_iff, lfpApprox_zero]
    simpa [lfpApprox_zero] using
      lfpApprox_eq_of_mem_fixedPoints f zero_le this

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

Goal state before:
pp: case refine_1
α : Type u
inst✝ : CompleteLattice α
f : α →o α
x : α
hx : x ≤ f x
o : Ordinal.{u}
h : lfpApprox f x o = x
⊢ f x = x ∨ o = 0

pp: case refine_2
α : Type u
inst✝ : CompleteLattice α
f : α →o α
x : α
hx : x ≤ f x
o : Ordinal.{u}
h : f x = x ∨ o = 0
⊢ lfpApprox f x o = x

Tactic:
·

Goal state after:
case refine_1
α : Type u
inst✝ : CompleteLattice α
f : α →o α
x : α
hx : x ≤ f x
o : Ordinal.{u}
h : lfpApprox f x o = x
⊢ f x = x ∨ o = 0
Module: Mathlib.SetTheory.Ordinal.FixedPointApproximants

Goal state before:
pp: case refine_1.inl
α : Type u
inst✝ : CompleteLattice α
f : α →o α
x : α
hx : x ≤ f x
h : lfpApprox f x 0 = x
⊢ f x = x ∨ 0 = 0

pp: case refine_1.inr
α : Type u
inst✝ : CompleteLattice α
f : α →o α
x : α
hx : x ≤ f x
o : Ordinal.{u}
h : lfpApprox f x o = x
ho : o ≠ 0
⊢ f x = x ∨ o = 0

Tactic:
·

Goal state after:
case refine_1.inl
α : Type u
inst✝ : CompleteLattice α
f : α →o α
x : α
hx : x ≤ f x
h : lfpApprox f x 0 = x
⊢ f x = x ∨ 0 = 0
Module: Mathlib.SetTheory.Ordinal.FixedPointApproximants

Goal state before:
pp: case refine_1.inr
α : Type u
inst✝ : CompleteLattice α
f : α →o α
x : α
hx : x ≤ f x
o : Ordinal.{u}
h : lfpApprox f x o = x
ho : o ≠ 0
⊢ f x = x ∨ o = 0

Tactic:
·

Goal state after:
case refine_1.inr
α : Type u
inst✝ : CompleteLattice α
f : α →o α
x : α
hx : x ≤ f x
o : Ordinal.{u}
h : lfpApprox f x o = x
ho : o ≠ 0
⊢ f x = x ∨ o = 0
Module: Mathlib.SetTheory.Ordinal.CantorNormalForm

Goal state before:
pp: case refine_2.inl
b o✝ o : Ordinal.{u_1}
ho : o ≠ 0
IH : List.Pairwise (fun x1 x2 ↦ x1 > x2) (map Prod.fst (CNF b (o % b ^ log b o)))
hb : b ≤ 1
⊢ List.Pairwise (fun x1 x2 ↦ x1 > x2) (map Prod.fst (CNF b o))

pp: case refine_2.inr
b o✝ o : Ordinal.{u_1}
ho : o ≠ 0
IH : List.Pairwise (fun x1 x2 ↦ x1 > x2) (map Prod.fst (CNF b (o % b ^ log b o)))
hb : 1 < b
⊢ List.Pairwise (fun x1 x2 ↦ x1 > x2) (map Prod.fst (CNF b o))

Tactic:
·

Goal state after:
case refine_2.inl
b o✝ o : Ordinal.{u_1}
ho : o ≠ 0
IH : List.Pairwise (fun x1 x2 ↦ x1 > x2) (map Prod.fst (CNF b (o % b ^ log b o)))
hb : b ≤ 1
⊢ List.Pairwise (fun x1 x2 ↦ x1 > x2) (map Prod.fst (CNF b o))
Module: Mathlib.SetTheory.Ordinal.FixedPointApproximants

Goal state before:
pp: case refine_2
α : Type u
inst✝ : CompleteLattice α
f : α →o α
x : α
hx : x ≤ f x
o : Ordinal.{u}
h : f x = x ∨ o = 0
⊢ lfpApprox f x o = x

Tactic:
·

Goal state after:
case refine_2
α : Type u
inst✝ : CompleteLattice α
f : α →o α
x : α
hx : x ≤ f x
o : Ordinal.{u}
h : f x = x ∨ o = 0
⊢ lfpApprox f x o = x
Module: Mathlib.SetTheory.Ordinal.FixedPointApproximants

Goal state before:
pp: case refine_2.inl
α : Type u
inst✝ : CompleteLattice α
f : α →o α
x : α
hx : x ≤ f x
o : Ordinal.{u}
hf : f x = x
⊢ lfpApprox f x o = x

pp: case refine_2.inr
α : Type u
inst✝ : CompleteLattice α
f : α →o α
x : α
hx : x ≤ f x
⊢ lfpApprox f x 0 = x

Tactic:
·

Goal state after:
case refine_2.inl
α : Type u
inst✝ : CompleteLattice α
f : α →o α
x : α
hx : x ≤ f x
o : Ordinal.{u}
hf : f x = x
⊢ lfpApprox f x o = x
Module: Mathlib.SetTheory.Ordinal.FixedPointApproximants

Goal state before:
pp: case refine_2.inr
α : Type u
inst✝ : CompleteLattice α
f : α →o α
x : α
hx : x ≤ f x
⊢ lfpApprox f x 0 = x

Tactic:
·

Goal state after:
case refine_2.inr
α : Type u
inst✝ : CompleteLattice α
f : α →o α
x : α
hx : x ≤ f x
⊢ lfpApprox f x 0 = x
Module: Mathlib.SetTheory.Ordinal.CantorNormalForm

Goal state before:
pp: case refine_2.inr
b o✝ o : Ordinal.{u_1}
ho : o ≠ 0
IH : List.Pairwise (fun x1 x2 ↦ x1 > x2) (map Prod.fst (CNF b (o % b ^ log b o)))
hb : 1 < b
⊢ List.Pairwise (fun x1 x2 ↦ x1 > x2) (map Prod.fst (CNF b o))

Tactic:
·

Goal state after:
case refine_2.inr
b o✝ o : Ordinal.{u_1}
ho : o ≠ 0
IH : List.Pairwise (fun x1 x2 ↦ x1 > x2) (map Prod.fst (CNF b (o % b ^ log b o)))
hb : 1 < b
⊢ List.Pairwise (fun x1 x2 ↦ x1 > x2) (map Prod.fst (CNF b o))
Module: Mathlib.SetTheory.Ordinal.CantorNormalForm

Goal state before:
pp: case refine_2.inr.inl
b o✝ o : Ordinal.{u_1}
ho : o ≠ 0
IH : List.Pairwise (fun x1 x2 ↦ x1 > x2) (map Prod.fst (CNF b (o % b ^ log b o)))
hb : 1 < b
hob : o < b
⊢ List.Pairwise (fun x1 x2 ↦ x1 > x2) (map Prod.fst (CNF b o))

pp: case refine_2.inr.inr
b o✝ o : Ordinal.{u_1}
ho : o ≠ 0
IH : List.Pairwise (fun x1 x2 ↦ x1 > x2) (map Prod.fst (CNF b (o % b ^ log b o)))
hb : 1 < b
hbo : b ≤ o
⊢ List.Pairwise (fun x1 x2 ↦ x1 > x2) (map Prod.fst (CNF b o))

Tactic:
·

Goal state after:
case refine_2.inr.inl
b o✝ o : Ordinal.{u_1}
ho : o ≠ 0
IH : List.Pairwise (fun x1 x2 ↦ x1 > x2) (map Prod.fst (CNF b (o % b ^ log b o)))
hb : 1 < b
hob : o < b
⊢ List.Pairwise (fun x1 x2 ↦ x1 > x2) (map Prod.fst (CNF b o))
Module: Mathlib.SetTheory.Lists

Goal state before:
pp: case C1.antisymm.antisymm.left
α : Type u_1
trans : Lists α → Prop := ⋯
l₁ : Lists' α true
IH : ∀ (l' : Lists α), l' ∈ l₁.toList → trans l'
l₂✝¹ : Lists' α true
l₂ : l₁.Subset l₂✝¹
a✝¹ : l₂✝¹.Subset l₁
h₁ : of' l₁ ~ ⟨true, l₂✝¹⟩
l₂✝ : Lists' α true
l₃ : l₂✝¹.Subset l₂✝
a✝ : l₂✝.Subset l₂✝¹
h₂ : ⟨true, l₂✝¹⟩ ~ ⟨true, l₂✝⟩
hl₁ : l₁ ⊆ l₂✝¹
hr₁ : l₂✝¹ ⊆ l₁
hl₂ : l₂✝¹ ⊆ l₂✝
hr₂ : l₂✝ ⊆ l₂✝¹
⊢ ∀ (a : Lists α), a ∈ l₁.toList → a ∈ l₂✝

pp: case C1.antisymm.antisymm.right
α : Type u_1
trans : Lists α → Prop := ⋯
l₁ : Lists' α true
IH : ∀ (l' : Lists α), l' ∈ l₁.toList → trans l'
l₂✝¹ : Lists' α true
l₂ : l₁.Subset l₂✝¹
a✝¹ : l₂✝¹.Subset l₁
h₁ : of' l₁ ~ ⟨true, l₂✝¹⟩
l₂✝ : Lists' α true
l₃ : l₂✝¹.Subset l₂✝
a✝ : l₂✝.Subset l₂✝¹
h₂ : ⟨true, l₂✝¹⟩ ~ ⟨true, l₂✝⟩
hl₁ : l₁ ⊆ l₂✝¹
hr₁ : l₂✝¹ ⊆ l₁
hl₂ : l₂✝¹ ⊆ l₂✝
hr₂ : l₂✝ ⊆ l₂✝¹
⊢ ∀ (a : Lists α), a ∈ l₂✝.toList → a ∈ l₁

Tactic:
·

Goal state after:
case C1.antisymm.antisymm.left
α : Type u_1
trans : Lists α → Prop := ⋯
l₁ : Lists' α true
IH : ∀ (l' : Lists α), l' ∈ l₁.toList → trans l'
l₂✝¹ : Lists' α true
l₂ : l₁.Subset l₂✝¹
a✝¹ : l₂✝¹.Subset l₁
h₁ : of' l₁ ~ ⟨true, l₂✝¹⟩
l₂✝ : Lists' α true
l₃ : l₂✝¹.Subset l₂✝
a✝ : l₂✝.Subset l₂✝¹
h₂ : ⟨true, l₂✝¹⟩ ~ ⟨true, l₂✝⟩
hl₁ : l₁ ⊆ l₂✝¹
hr₁ : l₂✝¹ ⊆ l₁
hl₂ : l₂✝¹ ⊆ l₂✝
hr₂ : l₂✝ ⊆ l₂✝¹
⊢ ∀ (a : Lists α), a ∈ l₁.toList → a ∈ l₂✝
Module: Mathlib.SetTheory.Ordinal.CantorNormalForm

Goal state before:
pp: case refine_2.inr.inr
b o✝ o : Ordinal.{u_1}
ho : o ≠ 0
IH : List.Pairwise (fun x1 x2 ↦ x1 > x2) (map Prod.fst (CNF b (o % b ^ log b o)))
hb : 1 < b
hbo : b ≤ o
⊢ List.Pairwise (fun x1 x2 ↦ x1 > x2) (map Prod.fst (CNF b o))

Tactic:
·

Goal state after:
case refine_2.inr.inr
b o✝ o : Ordinal.{u_1}
ho : o ≠ 0
IH : List.Pairwise (fun x1 x2 ↦ x1 > x2) (map Prod.fst (CNF b (o % b ^ log b o)))
hb : 1 < b
hbo : b ≤ o
⊢ List.Pairwise (fun x1 x2 ↦ x1 > x2) (map Prod.fst (CNF b o))
Module: Mathlib.SetTheory.Lists

Goal state before:
pp: case C1.antisymm.antisymm.right
α : Type u_1
trans : Lists α → Prop := ⋯
l₁ : Lists' α true
IH : ∀ (l' : Lists α), l' ∈ l₁.toList → trans l'
l₂✝¹ : Lists' α true
l₂ : l₁.Subset l₂✝¹
a✝¹ : l₂✝¹.Subset l₁
h₁ : of' l₁ ~ ⟨true, l₂✝¹⟩
l₂✝ : Lists' α true
l₃ : l₂✝¹.Subset l₂✝
a✝ : l₂✝.Subset l₂✝¹
h₂ : ⟨true, l₂✝¹⟩ ~ ⟨true, l₂✝⟩
hl₁ : l₁ ⊆ l₂✝¹
hr₁ : l₂✝¹ ⊆ l₁
hl₂ : l₂✝¹ ⊆ l₂✝
hr₂ : l₂✝ ⊆ l₂✝¹
⊢ ∀ (a : Lists α), a ∈ l₂✝.toList → a ∈ l₁

Tactic:
·

Goal state after:
case C1.antisymm.antisymm.right
α : Type u_1
trans : Lists α → Prop := ⋯
l₁ : Lists' α true
IH : ∀ (l' : Lists α), l' ∈ l₁.toList → trans l'
l₂✝¹ : Lists' α true
l₂ : l₁.Subset l₂✝¹
a✝¹ : l₂✝¹.Subset l₁
h₁ : of' l₁ ~ ⟨true, l₂✝¹⟩
l₂✝ : Lists' α true
l₃ : l₂✝¹.Subset l₂✝
a✝ : l₂✝.Subset l₂✝¹
h₂ : ⟨true, l₂✝¹⟩ ~ ⟨true, l₂✝⟩
hl₁ : l₁ ⊆ l₂✝¹
hr₁ : l₂✝¹ ⊆ l₁
hl₂ : l₂✝¹ ⊆ l₂✝
hr₂ : l₂✝ ⊆ l₂✝¹
⊢ ∀ (a : Lists α), a ∈ l₂✝.toList → a ∈ l₁
Module: Mathlib.SetTheory.Ordinal.FixedPointApproximants

Goal state before:
pp: case h.left
α : Type u
inst✝ : CompleteLattice α
f : α →o α
x : α
h_ninj :
  ∃ a b,
    (Set.Iio (SuccOrder.succ #α).ord).domRestrict (lfpApprox f x) a =
        (Set.Iio (SuccOrder.succ #α).ord).domRestrict (lfpApprox f x) b ∧
      a ≠ b
a b : ↑(Set.Iio (SuccOrder.succ #α).ord)
h_fab :
  (Set.Iio (SuccOrder.succ #α).ord).domRestrict (lfpApprox f x) a =
    (Set.Iio (SuccOrder.succ #α).ord).domRestrict (lfpApprox f x) b
h_nab : a ≠ b
⊢ ↑a ≠ ↑b

pp: case h.right
α : Type u
inst✝ : CompleteLattice α
f : α →o α
x : α
h_ninj :
  ∃ a b,
    (Set.Iio (SuccOrder.succ #α).ord).domRestrict (lfpApprox f x) a =
        (Set.Iio (SuccOrder.succ #α).ord).domRestrict (lfpApprox f x) b ∧
      a ≠ b
a b : ↑(Set.Iio (SuccOrder.succ #α).ord)
h_fab :
  (Set.Iio (SuccOrder.succ #α).ord).domRestrict (lfpApprox f x) a =
    (Set.Iio (SuccOrder.succ #α).ord).domRestrict (lfpApprox f x) b
h_nab : a ≠ b
⊢ lfpApprox f x ↑a = lfpApprox f x ↑b

Tactic:
·

Goal state after:
case h.left
α : Type u
inst✝ : CompleteLattice α
f : α →o α
x : α
h_ninj :
  ∃ a b,
    (Set.Iio (SuccOrder.succ #α).ord).domRestrict (lfpApprox f x) a =
        (Set.Iio (SuccOrder.succ #α).ord).domRestrict (lfpApprox f x) b ∧
      a ≠ b
a b : ↑(Set.Iio (SuccOrder.succ #α).ord)
h_fab :
  (Set.Iio (SuccOrder.succ #α).ord).domRestrict (lfpApprox f x) a =
    (Set.Iio (SuccOrder.succ #α).ord).domRestrict (lfpApprox f x) b
h_nab : a ≠ b
⊢ ↑a ≠ ↑b
Module: Mathlib.SetTheory.Lists

Goal state before:
pp: case D0
α : Type u_1
trans : Lists α → Prop := ⋯
⊢ ∀ (l' : Lists α), l' ∈ Lists'.nil.toList → trans l'

pp: case D1
α : Type u_1
trans : Lists α → Prop := ⋯
⊢ ∀ (a : Lists α) (l : Lists' α true),
    trans a → (∀ (l' : Lists α), l' ∈ l.toList → trans l') → ∀ (l' : Lists α), l' ∈ (Lists'.cons a l).toList → trans l'

Tactic:
·

Goal state after:
case D0
α : Type u_1
trans : Lists α → Prop := ⋯
⊢ ∀ (l' : Lists α), l' ∈ Lists'.nil.toList → trans l'
Module: Mathlib.SetTheory.Lists

Goal state before:
pp: case D1
α : Type u_1
trans : Lists α → Prop := ⋯
⊢ ∀ (a : Lists α) (l : Lists' α true),
    trans a → (∀ (l' : Lists α), l' ∈ l.toList → trans l') → ∀ (l' : Lists α), l' ∈ (Lists'.cons a l).toList → trans l'

Tactic:
·

Goal state after:
case D1
α : Type u_1
trans : Lists α → Prop := ⋯
⊢ ∀ (a : Lists α) (l : Lists' α true),
    trans a → (∀ (l' : Lists α), l' ∈ l.toList → trans l') → ∀ (l' : Lists α), l' ∈ (Lists'.cons a l).toList → trans l'
Module: Mathlib.SetTheory.Ordinal.CantorNormalForm

Goal state before:
pp: b o : Ordinal.{u_1}
⊢ { entries := map Prod.toSigma (CNF b o), nodupKeys := ⋯ }.entries.keys.toFinset = (map Prod.fst (CNF b o)).toFinset

pp: b o : Ordinal.{u_1}
⊢ ∀ a ∈ { entries := map Prod.toSigma (CNF b o), nodupKeys := ⋯ }.entries, decide (a.snd ≠ 0) = true

Tactic:
·

Goal state after:
b o : Ordinal.{u_1}
⊢ { entries := map Prod.toSigma (CNF b o), nodupKeys := ⋯ }.entries.keys.toFinset = (map Prod.fst (CNF b o)).toFinset
Module: Mathlib.SetTheory.Ordinal.CantorNormalForm

Goal state before:
pp: b o : Ordinal.{u_1}
⊢ ∀ a ∈ { entries := map Prod.toSigma (CNF b o), nodupKeys := ⋯ }.entries, decide (a.snd ≠ 0) = true

Tactic:
·

Goal state after:
b o : Ordinal.{u_1}
⊢ ∀ a ∈ { entries := map Prod.toSigma (CNF b o), nodupKeys := ⋯ }.entries, decide (a.snd ≠ 0) = true
Module: Mathlib.SetTheory.Ordinal.FixedPointApproximants

Goal state before:
pp: case h.right
α : Type u
inst✝ : CompleteLattice α
f : α →o α
x : α
h_ninj :
  ∃ a b,
    (Set.Iio (SuccOrder.succ #α).ord).domRestrict (lfpApprox f x) a =
        (Set.Iio (SuccOrder.succ #α).ord).domRestrict (lfpApprox f x) b ∧
      a ≠ b
a b : ↑(Set.Iio (SuccOrder.succ #α).ord)
h_fab :
  (Set.Iio (SuccOrder.succ #α).ord).domRestrict (lfpApprox f x) a =
    (Set.Iio (SuccOrder.succ #α).ord).domRestrict (lfpApprox f x) b
h_nab : a ≠ b
⊢ lfpApprox f x ↑a = lfpApprox f x ↑b

Tactic:
·

Goal state after:
case h.right
α : Type u
inst✝ : CompleteLattice α
f : α →o α
x : α
h_ninj :
  ∃ a b,
    (Set.Iio (SuccOrder.succ #α).ord).domRestrict (lfpApprox f x) a =
        (Set.Iio (SuccOrder.succ #α).ord).domRestrict (lfpApprox f x) b ∧
      a ≠ b
a b : ↑(Set.Iio (SuccOrder.succ #α).ord)
h_fab :
  (Set.Iio (SuccOrder.succ #α).ord).domRestrict (lfpApprox f x) a =
    (Set.Iio (SuccOrder.succ #α).ord).domRestrict (lfpApprox f x) b
h_nab : a ≠ b
⊢ lfpApprox f x ↑a = lfpApprox f x ↑b
Module: Mathlib.SetTheory.Ordinal.CantorNormalForm

Goal state before:
pp: case inl
b o c : Ordinal.{u_1}
he : (0, c) ∈ CNF b o
h : o < b ^ (0, c).1
⊢ False

pp: case inr
b o e c : Ordinal.{u_1}
he : (e, c) ∈ CNF b o
h : o < b ^ (e, c).1
he' : e ≠ 0
⊢ False

Tactic:
·

Goal state after:
case inl
b o c : Ordinal.{u_1}
he : (0, c) ∈ CNF b o
h : o < b ^ (0, c).1
⊢ False
Module: Mathlib.SetTheory.Ordinal.CantorNormalForm

Goal state before:
pp: case inr
b o e c : Ordinal.{u_1}
he : (e, c) ∈ CNF b o
h : o < b ^ (e, c).1
he' : e ≠ 0
⊢ False

Tactic:
·

Goal state after:
case inr
b o e c : Ordinal.{u_1}
he : (e, c) ∈ CNF b o
h : o < b ^ (e, c).1
he' : e ≠ 0
⊢ False
Module: Mathlib.SetTheory.Ordinal.CantorNormalForm

Goal state before:
pp: case inl
b : Ordinal.{u_1}
hb : b ≤ 1
a : Ordinal.{u_1}
⊢ (coeff b 0) a = (single 0 0) a

pp: case inr
b : Ordinal.{u_1}
hb : b ≤ 1
o a : Ordinal.{u_1}
ho : o ≠ 0
⊢ (coeff b o) a = (single 0 o) a

Tactic:
·

Goal state after:
case inl
b : Ordinal.{u_1}
hb : b ≤ 1
a : Ordinal.{u_1}
⊢ (coeff b 0) a = (single 0 0) a
Module: Mathlib.SetTheory.Ordinal.FixedPointApproximants

Goal state before:
pp: case a
α : Type u
inst✝ : CompleteLattice α
f : α →o α
⊢ lfpApprox f ⊥ (succ #α).ord ≤ lfp f

pp: case a
α : Type u
inst✝ : CompleteLattice α
f : α →o α
⊢ lfp f ≤ lfpApprox f ⊥ (succ #α).ord

Tactic:
·

Goal state after:
case a
α : Type u
inst✝ : CompleteLattice α
f : α →o α
⊢ lfpApprox f ⊥ (succ #α).ord ≤ lfp f
Module: Mathlib.SetTheory.Ordinal.CantorNormalForm

Goal state before:
pp: case inr
b : Ordinal.{u_1}
hb : b ≤ 1
o a : Ordinal.{u_1}
ho : o ≠ 0
⊢ (coeff b o) a = (single 0 o) a

Tactic:
·

Goal state after:
case inr
b : Ordinal.{u_1}
hb : b ≤ 1
o a : Ordinal.{u_1}
ho : o ≠ 0
⊢ (coeff b o) a = (single 0 o) a
Module: Mathlib.SetTheory.Ordinal.CantorNormalForm

Goal state before:
pp: case inr.inl
b : Ordinal.{u_1}
hb : b ≤ 1
o : Ordinal.{u_1}
ho : o ≠ 0
⊢ (coeff b o) 0 = (single 0 o) 0

pp: case inr.inr
b : Ordinal.{u_1}
hb : b ≤ 1
o a : Ordinal.{u_1}
ho : o ≠ 0
ha : a ≠ 0
⊢ (coeff b o) a = (single 0 o) a

Tactic:
·

Goal state after:
case inr.inl
b : Ordinal.{u_1}
hb : b ≤ 1
o : Ordinal.{u_1}
ho : o ≠ 0
⊢ (coeff b o) 0 = (single 0 o) 0
Module: Mathlib.SetTheory.Ordinal.FixedPointApproximants

Goal state before:
pp: case a
α : Type u
inst✝ : CompleteLattice α
f : α →o α
⊢ lfp f ≤ lfpApprox f ⊥ (succ #α).ord

Tactic:
·

Goal state after:
case a
α : Type u
inst✝ : CompleteLattice α
f : α →o α
⊢ lfp f ≤ lfpApprox f ⊥ (succ #α).ord
Module: Mathlib.SetTheory.Ordinal.CantorNormalForm

Goal state before:
pp: case inr.inr
b : Ordinal.{u_1}
hb : b ≤ 1
o a : Ordinal.{u_1}
ho : o ≠ 0
ha : a ≠ 0
⊢ (coeff b o) a = (single 0 o) a

Tactic:
·

Goal state after:
case inr.inr
b : Ordinal.{u_1}
hb : b ≤ 1
o a : Ordinal.{u_1}
ho : o ≠ 0
ha : a ≠ 0
⊢ (coeff b o) a = (single 0 o) a