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

Goal state before:
pp: case a.h₁
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : OmegaCompletePartialOrder α
inst✝¹ : OmegaCompletePartialOrder β
inst✝ : OmegaCompletePartialOrder γ
f : α → β →𝒄 γ
hf : ωScottContinuous f
g : α → β
hg : ωScottContinuous g
c : Chain α
i j : ℕ
⊢ f (c i) ≤ f (c.toOrderHom (max i j))

pp: case a.h₂
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : OmegaCompletePartialOrder α
inst✝¹ : OmegaCompletePartialOrder β
inst✝ : OmegaCompletePartialOrder γ
f : α → β →𝒄 γ
hf : ωScottContinuous f
g : α → β
hg : ωScottContinuous g
c : Chain α
i j : ℕ
⊢ (c.map { toFun := g, monotone' := ⋯ }).toOrderHom j ≤ g (c.toOrderHom (max i j))

Tactic:
·

Goal state after:
case a.h₁
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : OmegaCompletePartialOrder α
inst✝¹ : OmegaCompletePartialOrder β
inst✝ : OmegaCompletePartialOrder γ
f : α → β →𝒄 γ
hf : ωScottContinuous f
g : α → β
hg : ωScottContinuous g
c : Chain α
i j : ℕ
⊢ f (c i) ≤ f (c.toOrderHom (max i j))
Module: Mathlib.Order.OmegaCompletePartialOrder

Goal state before:
pp: case a.h₂
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : OmegaCompletePartialOrder α
inst✝¹ : OmegaCompletePartialOrder β
inst✝ : OmegaCompletePartialOrder γ
f : α → β →𝒄 γ
hf : ωScottContinuous f
g : α → β
hg : ωScottContinuous g
c : Chain α
i j : ℕ
⊢ (c.map { toFun := g, monotone' := ⋯ }).toOrderHom j ≤ g (c.toOrderHom (max i j))

Tactic:
·

Goal state after:
case a.h₂
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : OmegaCompletePartialOrder α
inst✝¹ : OmegaCompletePartialOrder β
inst✝ : OmegaCompletePartialOrder γ
f : α → β →𝒄 γ
hf : ωScottContinuous f
g : α → β
hg : ωScottContinuous g
c : Chain α
i j : ℕ
⊢ (c.map { toFun := g, monotone' := ⋯ }).toOrderHom j ≤ g (c.toOrderHom (max i j))
Module: Mathlib.Order.OmegaCompletePartialOrder

Goal state before:
pp: case a
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : OmegaCompletePartialOrder α
inst✝¹ : OmegaCompletePartialOrder β
inst✝ : OmegaCompletePartialOrder γ
f : α → β →𝒄 γ
hf : ωScottContinuous f
g : α → β
hg : ωScottContinuous g
c : Chain α
⊢ ωSup (c.map { toFun := fun x ↦ (f x) (g x), monotone' := ⋯ }) ≤
    ωSup
      (((c.map { toFun := f, monotone' := ⋯ }).map toMono).map
        (OrderHom.apply (ωSup (c.map { toFun := g, monotone' := ⋯ }))))

Tactic:
·

Goal state after:
case a
α : Type u_2
β : Type u_3
γ : Type u_4
inst✝² : OmegaCompletePartialOrder α
inst✝¹ : OmegaCompletePartialOrder β
inst✝ : OmegaCompletePartialOrder γ
f : α → β →𝒄 γ
hf : ωScottContinuous f
g : α → β
hg : ωScottContinuous g
c : Chain α
⊢ ωSup (c.map { toFun := fun x ↦ (f x) (g x), monotone' := ⋯ }) ≤
    ωSup
      (((c.map { toFun := f, monotone' := ⋯ }).map toMono).map
        (OrderHom.apply (ωSup (c.map { toFun := g, monotone' := ⋯ }))))
Module: Mathlib.SetTheory.Cardinal.Order

Goal state before:
pp: case pos
c : Cardinal.{u}
h : c = 0
⊢ 0 ^ c ≤ 1

pp: case neg
c : Cardinal.{u}
h : ¬c = 0
⊢ 0 ^ c ≤ 1

Tactic:
·

Goal state after:
case pos
c : Cardinal.{u}
h : c = 0
⊢ 0 ^ c ≤ 1
Module: Mathlib.SetTheory.Cardinal.Order

Goal state before:
pp: case neg
c : Cardinal.{u}
h : ¬c = 0
⊢ 0 ^ c ≤ 1

Tactic:
·

Goal state after:
case neg
c : Cardinal.{u}
h : ¬c = 0
⊢ 0 ^ c ≤ 1
Module: Mathlib.SetTheory.Cardinal.Order

Goal state before:
pp: case inl
b : Cardinal.{u_1}
hb : 1 ≤ b
⊢ 0 ≤ 0 ^ b

pp: case inr
a b : Cardinal.{u_1}
hb : 1 ≤ b
ha : a ≠ 0
⊢ a ≤ a ^ b

Tactic:
·

Goal state after:
case inl
b : Cardinal.{u_1}
hb : 1 ≤ b
⊢ 0 ≤ 0 ^ b
Module: Mathlib.SetTheory.Cardinal.Order

Goal state before:
pp: case inr
a b : Cardinal.{u_1}
hb : 1 ≤ b
ha : a ≠ 0
⊢ a ≤ a ^ b

Tactic:
·

Goal state after:
case inr
a b : Cardinal.{u_1}
hb : 1 ≤ b
ha : a ≠ 0
⊢ a ≤ a ^ b
Module: Mathlib.SetTheory.Cardinal.Order

Goal state before:
pp: case pos
a b c : Cardinal.{u_1}
h : b ≤ c
ha : a = 0
⊢ a ^ b ≤ max (a ^ c) 1

pp: case neg
a b c : Cardinal.{u_1}
h : b ≤ c
ha : ¬a = 0
⊢ a ^ b ≤ max (a ^ c) 1

Tactic:
·

Goal state after:
case pos
a b c : Cardinal.{u_1}
h : b ≤ c
ha : a = 0
⊢ a ^ b ≤ max (a ^ c) 1
Module: Mathlib.SetTheory.Cardinal.Order

Goal state before:
pp: case neg
a b c : Cardinal.{u_1}
h : b ≤ c
ha : ¬a = 0
⊢ a ^ b ≤ max (a ^ c) 1

Tactic:
·

Goal state after:
case neg
a b c : Cardinal.{u_1}
h : b ≤ c
ha : ¬a = 0
⊢ a ^ b ≤ max (a ^ c) 1
Module: Mathlib.SetTheory.Cardinal.SchroederBernstein

Goal state before:
pp: case inr.isTrue
α : Type u
β : Type v
f : α → β
g : β → α
hf : Injective f
hg : Injective g
R : α → β → Prop
hp₁ : ∀ (a : α), R a (f a)
hp₂ : ∀ (b : β), R (g b) b
hβ : Nonempty β
F : Set α →o Set α := { toFun := fun s ↦ (g '' (f '' s)ᶜ)ᶜ, monotone' := ⋯ }
s : Set α := OrderHom.lfp F
hs : (g '' (f '' s)ᶜ)ᶜ = s
hns : g '' (f '' s)ᶜ = sᶜ
g' : α → β := invFun g
g'g : LeftInverse g' g
hg'ns : g' '' sᶜ = (f '' s)ᶜ
h : α → β := s.piecewise f g'
this✝ : Surjective h
this : Injective h
a : α
h✝ : a ∈ s
⊢ R a (f a)

pp: case inr.isFalse
α : Type u
β : Type v
f : α → β
g : β → α
hf : Injective f
hg : Injective g
R : α → β → Prop
hp₁ : ∀ (a : α), R a (f a)
hp₂ : ∀ (b : β), R (g b) b
hβ : Nonempty β
F : Set α →o Set α := { toFun := fun s ↦ (g '' (f '' s)ᶜ)ᶜ, monotone' := ⋯ }
s : Set α := OrderHom.lfp F
hs : (g '' (f '' s)ᶜ)ᶜ = s
hns : g '' (f '' s)ᶜ = sᶜ
g' : α → β := invFun g
g'g : LeftInverse g' g
hg'ns : g' '' sᶜ = (f '' s)ᶜ
h : α → β := s.piecewise f g'
this✝ : Surjective h
this : Injective h
a : α
h✝ : a ∉ s
⊢ R a (invFun g a)

Tactic:
·

Goal state after:
case inr.isTrue
α : Type u
β : Type v
f : α → β
g : β → α
hf : Injective f
hg : Injective g
R : α → β → Prop
hp₁ : ∀ (a : α), R a (f a)
hp₂ : ∀ (b : β), R (g b) b
hβ : Nonempty β
F : Set α →o Set α := { toFun := fun s ↦ (g '' (f '' s)ᶜ)ᶜ, monotone' := ⋯ }
s : Set α := OrderHom.lfp F
hs : (g '' (f '' s)ᶜ)ᶜ = s
hns : g '' (f '' s)ᶜ = sᶜ
g' : α → β := invFun g
g'g : LeftInverse g' g
hg'ns : g' '' sᶜ = (f '' s)ᶜ
h : α → β := s.piecewise f g'
this✝ : Surjective h
this : Injective h
a : α
h✝ : a ∈ s
⊢ R a (f a)
Module: Mathlib.SetTheory.Cardinal.SchroederBernstein

Goal state before:
pp: case inr.isFalse
α : Type u
β : Type v
f : α → β
g : β → α
hf : Injective f
hg : Injective g
R : α → β → Prop
hp₁ : ∀ (a : α), R a (f a)
hp₂ : ∀ (b : β), R (g b) b
hβ : Nonempty β
F : Set α →o Set α := { toFun := fun s ↦ (g '' (f '' s)ᶜ)ᶜ, monotone' := ⋯ }
s : Set α := OrderHom.lfp F
hs : (g '' (f '' s)ᶜ)ᶜ = s
hns : g '' (f '' s)ᶜ = sᶜ
g' : α → β := invFun g
g'g : LeftInverse g' g
hg'ns : g' '' sᶜ = (f '' s)ᶜ
h : α → β := s.piecewise f g'
this✝ : Surjective h
this : Injective h
a : α
h✝ : a ∉ s
⊢ R a (invFun g a)

Tactic:
·

Goal state after:
case inr.isFalse
α : Type u
β : Type v
f : α → β
g : β → α
hf : Injective f
hg : Injective g
R : α → β → Prop
hp₁ : ∀ (a : α), R a (f a)
hp₂ : ∀ (b : β), R (g b) b
hβ : Nonempty β
F : Set α →o Set α := { toFun := fun s ↦ (g '' (f '' s)ᶜ)ᶜ, monotone' := ⋯ }
s : Set α := OrderHom.lfp F
hs : (g '' (f '' s)ᶜ)ᶜ = s
hns : g '' (f '' s)ᶜ = sᶜ
g' : α → β := invFun g
g'g : LeftInverse g' g
hg'ns : g' '' sᶜ = (f '' s)ᶜ
h : α → β := s.piecewise f g'
this✝ : Surjective h
this : Injective h
a : α
h✝ : a ∉ s
⊢ R a (invFun g a)
Module: Mathlib.SetTheory.Cardinal.Order

Goal state before:
pp: a b : Cardinal.{u_1}
h : a < b
⊢ a + 1 ≤ b

Tactic:
induction a, b using Cardinal.inductionOn₂ with

Goal state after:
case mk
α β : Type u_1
h : #α < #β
⊢ #α + 1 ≤ #β
Module: Mathlib.Order.OmegaCompletePartialOrder

Goal state before:
pp: case a
α : Type u_2
inst✝ : OmegaCompletePartialOrder α
f : α →𝒄 α
x : α
h : x ≤ f x
⊢ ωSup ((iterateChain (↑f) x h).map ↑f) ≤ ωSup (iterateChain (↑f) x h)

pp: case a
α : Type u_2
inst✝ : OmegaCompletePartialOrder α
f : α →𝒄 α
x : α
h : x ≤ f x
⊢ ωSup (iterateChain (↑f) x h) ≤ ωSup ((iterateChain (↑f) x h).map ↑f)

Tactic:
·

Goal state after:
case a
α : Type u_2
inst✝ : OmegaCompletePartialOrder α
f : α →𝒄 α
x : α
h : x ≤ f x
⊢ ωSup ((iterateChain (↑f) x h).map ↑f) ≤ ωSup (iterateChain (↑f) x h)
Module: Mathlib.Order.OmegaCompletePartialOrder

Goal state before:
pp: case a
α : Type u_2
inst✝ : OmegaCompletePartialOrder α
f : α →𝒄 α
x : α
h : x ≤ f x
⊢ ωSup (iterateChain (↑f) x h) ≤ ωSup ((iterateChain (↑f) x h).map ↑f)

Tactic:
·

Goal state after:
case a
α : Type u_2
inst✝ : OmegaCompletePartialOrder α
f : α →𝒄 α
x : α
h : x ≤ f x
⊢ ωSup (iterateChain (↑f) x h) ≤ ωSup ((iterateChain (↑f) x h).map ↑f)
Module: Mathlib.Order.OmegaCompletePartialOrder

Goal state before:
pp: case a.zero
α : Type u_2
inst✝ : OmegaCompletePartialOrder α
f : α →𝒄 α
x : α
h : x ≤ f x
⊢ (iterateChain (↑f) x h) 0 ≤ ωSup ((iterateChain (↑f) x h).map ↑f)

pp: case a.succ
α : Type u_2
inst✝ : OmegaCompletePartialOrder α
f : α →𝒄 α
x : α
h : x ≤ f x
n : ℕ
⊢ (iterateChain (↑f) x h) (n + 1) ≤ ωSup ((iterateChain (↑f) x h).map ↑f)

Tactic:
·

Goal state after:
case a.zero
α : Type u_2
inst✝ : OmegaCompletePartialOrder α
f : α →𝒄 α
x : α
h : x ≤ f x
⊢ (iterateChain (↑f) x h) 0 ≤ ωSup ((iterateChain (↑f) x h).map ↑f)
Module: Mathlib.Order.OmegaCompletePartialOrder

Goal state before:
pp: case a.succ
α : Type u_2
inst✝ : OmegaCompletePartialOrder α
f : α →𝒄 α
x : α
h : x ≤ f x
n : ℕ
⊢ (iterateChain (↑f) x h) (n + 1) ≤ ωSup ((iterateChain (↑f) x h).map ↑f)

Tactic:
·

Goal state after:
case a.succ
α : Type u_2
inst✝ : OmegaCompletePartialOrder α
f : α →𝒄 α
x : α
h : x ≤ f x
n : ℕ
⊢ (iterateChain (↑f) x h) (n + 1) ≤ ωSup ((iterateChain (↑f) x h).map ↑f)
Module: Mathlib.SetTheory.Cardinal.SchroederBernstein

Goal state before:
pp: case inl.inl
ι : Type u
β : ι → Type v
I : Nonempty ι
s : Set ((i : ι) → β i)
hs : Maximal (fun x ↦ x ∈ sets β) s
h✝ : ¬∃ i, Surjective fun x ↦ ↑x i
h : ∀ (i : ι), ∃ y, ∀ x ∈ s, x i ≠ y
f : (x : ι) → β x
hf : ∀ (x : ι), ∀ x_1 ∈ s, x_1 x ≠ f x
i : ι
x y : (i : ι) → β i
hx : x = f
hy : y = f
⊢ (fun x ↦ x i) x = (fun x ↦ x i) y → x = y

pp: case inl.inr
ι : Type u
β : ι → Type v
I : Nonempty ι
s : Set ((i : ι) → β i)
hs : Maximal (fun x ↦ x ∈ sets β) s
h✝ : ¬∃ i, Surjective fun x ↦ ↑x i
h : ∀ (i : ι), ∃ y, ∀ x ∈ s, x i ≠ y
f : (x : ι) → β x
hf : ∀ (x : ι), ∀ x_1 ∈ s, x_1 x ≠ f x
i : ι
x y : (i : ι) → β i
hx : x = f
hy : y ∈ s
⊢ (fun x ↦ x i) x = (fun x ↦ x i) y → x = y

pp: case inr.inl
ι : Type u
β : ι → Type v
I : Nonempty ι
s : Set ((i : ι) → β i)
hs : Maximal (fun x ↦ x ∈ sets β) s
h✝ : ¬∃ i, Surjective fun x ↦ ↑x i
h : ∀ (i : ι), ∃ y, ∀ x ∈ s, x i ≠ y
f : (x : ι) → β x
hf : ∀ (x : ι), ∀ x_1 ∈ s, x_1 x ≠ f x
i : ι
x y : (i : ι) → β i
hx : x ∈ s
hy : y = f
⊢ (fun x ↦ x i) x = (fun x ↦ x i) y → x = y

pp: case inr.inr
ι : Type u
β : ι → Type v
I : Nonempty ι
s : Set ((i : ι) → β i)
hs : Maximal (fun x ↦ x ∈ sets β) s
h✝ : ¬∃ i, Surjective fun x ↦ ↑x i
h : ∀ (i : ι), ∃ y, ∀ x ∈ s, x i ≠ y
f : (x : ι) → β x
hf : ∀ (x : ι), ∀ x_1 ∈ s, x_1 x ≠ f x
i : ι
x y : (i : ι) → β i
hx : x ∈ s
hy : y ∈ s
⊢ (fun x ↦ x i) x = (fun x ↦ x i) y → x = y

Tactic:
·

Goal state after:
case inl.inl
ι : Type u
β : ι → Type v
I : Nonempty ι
s : Set ((i : ι) → β i)
hs : Maximal (fun x ↦ x ∈ sets β) s
h✝ : ¬∃ i, Surjective fun x ↦ ↑x i
h : ∀ (i : ι), ∃ y, ∀ x ∈ s, x i ≠ y
f : (x : ι) → β x
hf : ∀ (x : ι), ∀ x_1 ∈ s, x_1 x ≠ f x
i : ι
x y : (i : ι) → β i
hx : x = f
hy : y = f
⊢ (fun x ↦ x i) x = (fun x ↦ x i) y → x = y
Module: Mathlib.SetTheory.Cardinal.SchroederBernstein

Goal state before:
pp: case inl.inr
ι : Type u
β : ι → Type v
I : Nonempty ι
s : Set ((i : ι) → β i)
hs : Maximal (fun x ↦ x ∈ sets β) s
h✝ : ¬∃ i, Surjective fun x ↦ ↑x i
h : ∀ (i : ι), ∃ y, ∀ x ∈ s, x i ≠ y
f : (x : ι) → β x
hf : ∀ (x : ι), ∀ x_1 ∈ s, x_1 x ≠ f x
i : ι
x y : (i : ι) → β i
hx : x = f
hy : y ∈ s
⊢ (fun x ↦ x i) x = (fun x ↦ x i) y → x = y

pp: case inr.inl
ι : Type u
β : ι → Type v
I : Nonempty ι
s : Set ((i : ι) → β i)
hs : Maximal (fun x ↦ x ∈ sets β) s
h✝ : ¬∃ i, Surjective fun x ↦ ↑x i
h : ∀ (i : ι), ∃ y, ∀ x ∈ s, x i ≠ y
f : (x : ι) → β x
hf : ∀ (x : ι), ∀ x_1 ∈ s, x_1 x ≠ f x
i : ι
x y : (i : ι) → β i
hx : x ∈ s
hy : y = f
⊢ (fun x ↦ x i) x = (fun x ↦ x i) y → x = y

pp: case inr.inr
ι : Type u
β : ι → Type v
I : Nonempty ι
s : Set ((i : ι) → β i)
hs : Maximal (fun x ↦ x ∈ sets β) s
h✝ : ¬∃ i, Surjective fun x ↦ ↑x i
h : ∀ (i : ι), ∃ y, ∀ x ∈ s, x i ≠ y
f : (x : ι) → β x
hf : ∀ (x : ι), ∀ x_1 ∈ s, x_1 x ≠ f x
i : ι
x y : (i : ι) → β i
hx : x ∈ s
hy : y ∈ s
⊢ (fun x ↦ x i) x = (fun x ↦ x i) y → x = y

Tactic:
·

Goal state after:
case inl.inr
ι : Type u
β : ι → Type v
I : Nonempty ι
s : Set ((i : ι) → β i)
hs : Maximal (fun x ↦ x ∈ sets β) s
h✝ : ¬∃ i, Surjective fun x ↦ ↑x i
h : ∀ (i : ι), ∃ y, ∀ x ∈ s, x i ≠ y
f : (x : ι) → β x
hf : ∀ (x : ι), ∀ x_1 ∈ s, x_1 x ≠ f x
i : ι
x y : (i : ι) → β i
hx : x = f
hy : y ∈ s
⊢ (fun x ↦ x i) x = (fun x ↦ x i) y → x = y
Module: Mathlib.SetTheory.Cardinal.SchroederBernstein

Goal state before:
pp: case inr.inl
ι : Type u
β : ι → Type v
I : Nonempty ι
s : Set ((i : ι) → β i)
hs : Maximal (fun x ↦ x ∈ sets β) s
h✝ : ¬∃ i, Surjective fun x ↦ ↑x i
h : ∀ (i : ι), ∃ y, ∀ x ∈ s, x i ≠ y
f : (x : ι) → β x
hf : ∀ (x : ι), ∀ x_1 ∈ s, x_1 x ≠ f x
i : ι
x y : (i : ι) → β i
hx : x ∈ s
hy : y = f
⊢ (fun x ↦ x i) x = (fun x ↦ x i) y → x = y

pp: case inr.inr
ι : Type u
β : ι → Type v
I : Nonempty ι
s : Set ((i : ι) → β i)
hs : Maximal (fun x ↦ x ∈ sets β) s
h✝ : ¬∃ i, Surjective fun x ↦ ↑x i
h : ∀ (i : ι), ∃ y, ∀ x ∈ s, x i ≠ y
f : (x : ι) → β x
hf : ∀ (x : ι), ∀ x_1 ∈ s, x_1 x ≠ f x
i : ι
x y : (i : ι) → β i
hx : x ∈ s
hy : y ∈ s
⊢ (fun x ↦ x i) x = (fun x ↦ x i) y → x = y

Tactic:
·

Goal state after:
case inr.inl
ι : Type u
β : ι → Type v
I : Nonempty ι
s : Set ((i : ι) → β i)
hs : Maximal (fun x ↦ x ∈ sets β) s
h✝ : ¬∃ i, Surjective fun x ↦ ↑x i
h : ∀ (i : ι), ∃ y, ∀ x ∈ s, x i ≠ y
f : (x : ι) → β x
hf : ∀ (x : ι), ∀ x_1 ∈ s, x_1 x ≠ f x
i : ι
x y : (i : ι) → β i
hx : x ∈ s
hy : y = f
⊢ (fun x ↦ x i) x = (fun x ↦ x i) y → x = y
Module: Mathlib.SetTheory.Cardinal.SchroederBernstein

Goal state before:
pp: case inr.inr
ι : Type u
β : ι → Type v
I : Nonempty ι
s : Set ((i : ι) → β i)
hs : Maximal (fun x ↦ x ∈ sets β) s
h✝ : ¬∃ i, Surjective fun x ↦ ↑x i
h : ∀ (i : ι), ∃ y, ∀ x ∈ s, x i ≠ y
f : (x : ι) → β x
hf : ∀ (x : ι), ∀ x_1 ∈ s, x_1 x ≠ f x
i : ι
x y : (i : ι) → β i
hx : x ∈ s
hy : y ∈ s
⊢ (fun x ↦ x i) x = (fun x ↦ x i) y → x = y

Tactic:
·

Goal state after:
case inr.inr
ι : Type u
β : ι → Type v
I : Nonempty ι
s : Set ((i : ι) → β i)
hs : Maximal (fun x ↦ x ∈ sets β) s
h✝ : ¬∃ i, Surjective fun x ↦ ↑x i
h : ∀ (i : ι), ∃ y, ∀ x ∈ s, x i ≠ y
f : (x : ι) → β x
hf : ∀ (x : ι), ∀ x_1 ∈ s, x_1 x ≠ f x
i : ι
x y : (i : ι) → β i
hx : x ∈ s
hy : y ∈ s
⊢ (fun x ↦ x i) x = (fun x ↦ x i) y → x = y
Module: Mathlib.SetTheory.Cardinal.ToNat

Goal state before:
pp: case inl
a : Cardinal.{u_1}
h : a < ℵ₀
⊢ ↑(toNat a) ≤ a

pp: case inr
a : Cardinal.{u_1}
h : ℵ₀ ≤ a
⊢ ↑(toNat a) ≤ a

Tactic:
·

Goal state after:
case inl
a : Cardinal.{u_1}
h : a < ℵ₀
⊢ ↑(toNat a) ≤ a
Module: Mathlib.SetTheory.Cardinal.ToNat

Goal state before:
pp: case inr
a : Cardinal.{u_1}
h : ℵ₀ ≤ a
⊢ ↑(toNat a) ≤ a

Tactic:
·

Goal state after:
case inr
a : Cardinal.{u_1}
h : ℵ₀ ≤ a
⊢ ↑(toNat a) ≤ a
Module: Mathlib.SetTheory.Cardinal.ToNat

Goal state before:
pp: case inl
c : Cardinal.{u}
d : Cardinal.{v}
h : ∀ (n : ℕ), ↑n ≤ c ↔ ↑n ≤ d
h' : ℵ₀ ≤ c ↔ ℵ₀ ≤ d
hc : ℵ₀ ≤ c
hd : ℵ₀ ≤ d
⊢ toNat c = toNat d

pp: case inr
c : Cardinal.{u}
d : Cardinal.{v}
h : ∀ (n : ℕ), ↑n ≤ c ↔ ↑n ≤ d
h' : ℵ₀ ≤ c ↔ ℵ₀ ≤ d
hc : ¬ℵ₀ ≤ c
hd : ¬ℵ₀ ≤ d
⊢ toNat c = toNat d

Tactic:
·

Goal state after:
case inl
c : Cardinal.{u}
d : Cardinal.{v}
h : ∀ (n : ℕ), ↑n ≤ c ↔ ↑n ≤ d
h' : ℵ₀ ≤ c ↔ ℵ₀ ≤ d
hc : ℵ₀ ≤ c
hd : ℵ₀ ≤ d
⊢ toNat c = toNat d
Module: Mathlib.SetTheory.Cardinal.ToNat

Goal state before:
pp: case inr
c : Cardinal.{u}
d : Cardinal.{v}
h : ∀ (n : ℕ), ↑n ≤ c ↔ ↑n ≤ d
h' : ℵ₀ ≤ c ↔ ℵ₀ ≤ d
hc : ¬ℵ₀ ≤ c
hd : ¬ℵ₀ ≤ d
⊢ toNat c = toNat d

Tactic:
·

Goal state after:
case inr
c : Cardinal.{u}
d : Cardinal.{v}
h : ∀ (n : ℕ), ↑n ≤ c ↔ ↑n ≤ d
h' : ℵ₀ ≤ c ↔ ℵ₀ ≤ d
hc : ¬ℵ₀ ≤ c
hd : ¬ℵ₀ ≤ d
⊢ toNat c = toNat d
Module: Mathlib.SetTheory.Cardinal.ENat

Goal state before:
pp: case inl
x : Cardinal.{u_1}
hx : x ≤ ℵ₀
hlt : x < ℵ₀
⊢ x ∈ range ofENat

pp: case inr
hx : ℵ₀ ≤ ℵ₀
⊢ ℵ₀ ∈ range ofENat

Tactic:
·

Goal state after:
case inl
x : Cardinal.{u_1}
hx : x ≤ ℵ₀
hlt : x < ℵ₀
⊢ x ∈ range ofENat
Module: Mathlib.SetTheory.Cardinal.ENat

Goal state before:
pp: case inr
hx : ℵ₀ ≤ ℵ₀
⊢ ℵ₀ ∈ range ofENat

Tactic:
·

Goal state after:
case inr
hx : ℵ₀ ≤ ℵ₀
⊢ ℵ₀ ∈ range ofENat
Module: Mathlib.SetTheory.Cardinal.ENat

Goal state before:
pp: case inr
x y : Cardinal.{u}
this : ∀ (x y : Cardinal.{u}), x ≤ y → (x * y).toENatAux = x.toENatAux * y.toENatAux
hle : ¬x ≤ y
⊢ (x * y).toENatAux = x.toENatAux * y.toENatAux

pp: x y : Cardinal.{u}
hle : x ≤ y
⊢ (x * y).toENatAux = x.toENatAux * y.toENatAux

Tactic:
·

Goal state after:
case inr
x y : Cardinal.{u}
this : ∀ (x y : Cardinal.{u}), x ≤ y → (x * y).toENatAux = x.toENatAux * y.toENatAux
hle : ¬x ≤ y
⊢ (x * y).toENatAux = x.toENatAux * y.toENatAux
Module: Mathlib.SetTheory.Cardinal.ENat

Goal state before:
pp: case inr.inl
y : Cardinal.{u}
hy : ℵ₀ ≤ y
hle : 0 ≤ y
⊢ (0 * y).toENatAux = toENatAux 0 * y.toENatAux

pp: case inr.inr
x y : Cardinal.{u}
hle : x ≤ y
hy : ℵ₀ ≤ y
hx : x ≠ 0
⊢ (x * y).toENatAux = x.toENatAux * y.toENatAux

Tactic:
·

Goal state after:
case inr.inl
y : Cardinal.{u}
hy : ℵ₀ ≤ y
hle : 0 ≤ y
⊢ (0 * y).toENatAux = toENatAux 0 * y.toENatAux
Module: Mathlib.SetTheory.Cardinal.ENat

Goal state before:
pp: case inr.inr
x y : Cardinal.{u}
hle : x ≤ y
hy : ℵ₀ ≤ y
hx : x ≠ 0
⊢ (x * y).toENatAux = x.toENatAux * y.toENatAux

Tactic:
·

Goal state after:
case inr.inr
x y : Cardinal.{u}
hle : x ≤ y
hy : ℵ₀ ≤ y
hx : x ≠ 0
⊢ (x * y).toENatAux = x.toENatAux * y.toENatAux
Module: Mathlib.SetTheory.Cardinal.ENat

Goal state before:
pp: case inr.inr
x y : Cardinal.{u}
hle : x ≤ y
hy : ℵ₀ ≤ y
hx : x ≠ 0
⊢ x.toENatAux ≠ 0

pp: case inr.inr
x y : Cardinal.{u}
hle : x ≤ y
hy : ℵ₀ ≤ y
hx : x ≠ 0
⊢ ℵ₀ ≤ x * y

Tactic:
·

Goal state after:
case inr.inr
x y : Cardinal.{u}
hle : x ≤ y
hy : ℵ₀ ≤ y
hx : x ≠ 0
⊢ x.toENatAux ≠ 0
Module: Mathlib.SetTheory.Cardinal.ENat

Goal state before:
pp: case inr.inr
x y : Cardinal.{u}
hle : x ≤ y
hy : ℵ₀ ≤ y
hx : x ≠ 0
⊢ ℵ₀ ≤ x * y

Tactic:
·

Goal state after:
case inr.inr
x y : Cardinal.{u}
hle : x ≤ y
hy : ℵ₀ ≤ y
hx : x ≠ 0
⊢ ℵ₀ ≤ x * y
Module: Mathlib.SetTheory.Cardinal.ENat

Goal state before:
pp: case inr
x y : Cardinal.{u}
this : ∀ (x y : Cardinal.{u}), x ≤ y → (x + y).toENatAux = x.toENatAux + y.toENatAux
hle : ¬x ≤ y
⊢ (x + y).toENatAux = x.toENatAux + y.toENatAux

pp: x y : Cardinal.{u}
hle : x ≤ y
⊢ (x + y).toENatAux = x.toENatAux + y.toENatAux

Tactic:
·

Goal state after:
case inr
x y : Cardinal.{u}
this : ∀ (x y : Cardinal.{u}), x ≤ y → (x + y).toENatAux = x.toENatAux + y.toENatAux
hle : ¬x ≤ y
⊢ (x + y).toENatAux = x.toENatAux + y.toENatAux
Module: Mathlib.Algebra.Group.Hom.CompTypeclasses

Goal state before:
pp: case mp
M : Type u_1
N : Type u_2
P : Type u_3
inst✝³ : Monoid M
inst✝² : Monoid N
inst✝¹ : Monoid P
Q : Type u_4
inst✝ : Monoid Q
φ₁ : M →* N
φ₂ : N →* P
φ₁₂ : M →* P
κ : φ₁.CompTriple φ₂ φ₁₂
φ₃ : P →* Q
φ₂₃ : N →* Q
κ' : φ₂.CompTriple φ₃ φ₂₃
φ₁₂₃ : M →* Q
⊢ φ₁.CompTriple φ₂₃ φ₁₂₃ → φ₁₂.CompTriple φ₃ φ₁₂₃

Tactic:
·

Goal state after:
case mp
M : Type u_1
N : Type u_2
P : Type u_3
inst✝³ : Monoid M
inst✝² : Monoid N
inst✝¹ : Monoid P
Q : Type u_4
inst✝ : Monoid Q
φ₁ : M →* N
φ₂ : N →* P
φ₁₂ : M →* P
κ : φ₁.CompTriple φ₂ φ₁₂
φ₃ : P →* Q
φ₂₃ : N →* Q
κ' : φ₂.CompTriple φ₃ φ₂₃
φ₁₂₃ : M →* Q
⊢ φ₁.CompTriple φ₂₃ φ₁₂₃ → φ₁₂.CompTriple φ₃ φ₁₂₃
Module: Mathlib.Algebra.Group.Hom.CompTypeclasses

Goal state before:
pp: case mpr
M : Type u_1
N : Type u_2
P : Type u_3
inst✝³ : Monoid M
inst✝² : Monoid N
inst✝¹ : Monoid P
Q : Type u_4
inst✝ : Monoid Q
φ₁ : M →* N
φ₂ : N →* P
φ₁₂ : M →* P
κ : φ₁.CompTriple φ₂ φ₁₂
φ₃ : P →* Q
φ₂₃ : N →* Q
κ' : φ₂.CompTriple φ₃ φ₂₃
φ₁₂₃ : M →* Q
⊢ φ₁₂.CompTriple φ₃ φ₁₂₃ → φ₁.CompTriple φ₂₃ φ₁₂₃

Tactic:
·

Goal state after:
case mpr
M : Type u_1
N : Type u_2
P : Type u_3
inst✝³ : Monoid M
inst✝² : Monoid N
inst✝¹ : Monoid P
Q : Type u_4
inst✝ : Monoid Q
φ₁ : M →* N
φ₂ : N →* P
φ₁₂ : M →* P
κ : φ₁.CompTriple φ₂ φ₁₂
φ₃ : P →* Q
φ₂₃ : N →* Q
κ' : φ₂.CompTriple φ₃ φ₂₃
φ₁₂₃ : M →* Q
⊢ φ₁₂.CompTriple φ₃ φ₁₂₃ → φ₁.CompTriple φ₂₃ φ₁₂₃
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: case refine_1
α : Type u
h : Fintype α
⊢ ∀ (α β : Type u) [inst : Fintype β] (e : α ≃ β),
    (∀ (f : α → Cardinal.{v}), prod f = lift.{u, v} (∏ i, f i)) →
      ∀ (f : β → Cardinal.{v}), prod f = lift.{u, v} (∏ i, f i)

pp: case refine_2
α : Type u
h : Fintype α
⊢ ∀ (f : PEmpty.{u + 1} → Cardinal.{v}), prod f = lift.{u, v} (∏ i, f i)

pp: case refine_3
α : Type u
h : Fintype α
⊢ ∀ (α : Type u) [inst : Fintype α],
    (∀ (f : α → Cardinal.{v}), prod f = lift.{u, v} (∏ i, f i)) →
      ∀ (f : Option α → Cardinal.{v}), prod f = lift.{u, v} (∏ i, f i)

Tactic:
·

Goal state after:
case refine_1
α : Type u
h : Fintype α
⊢ ∀ (α β : Type u) [inst : Fintype β] (e : α ≃ β),
    (∀ (f : α → Cardinal.{v}), prod f = lift.{u, v} (∏ i, f i)) →
      ∀ (f : β → Cardinal.{v}), prod f = lift.{u, v} (∏ i, f i)
Module: Mathlib.Algebra.Regular.SMul

Goal state before:
pp: case inl
M : Type u_3
inst✝ : SubtractionMonoid M
n : ℤ
h : n.sign = 1
⊢ (∀ ⦃a₁ a₂ : M⦄, n.natAbs • a₁ = n.natAbs • a₂ → a₁ = a₂) ↔
    ∀ ⦃a₁ a₂ : M⦄, (n.sign * ↑n.natAbs) • a₁ = (n.sign * ↑n.natAbs) • a₂ → a₁ = a₂

pp: case inr.inl
M : Type u_3
inst✝ : SubtractionMonoid M
n : ℤ
h : n.sign = 0
⊢ (∀ ⦃a₁ a₂ : M⦄, n.natAbs • a₁ = n.natAbs • a₂ → a₁ = a₂) ↔
    ∀ ⦃a₁ a₂ : M⦄, (n.sign * ↑n.natAbs) • a₁ = (n.sign * ↑n.natAbs) • a₂ → a₁ = a₂

pp: case inr.inr
M : Type u_3
inst✝ : SubtractionMonoid M
n : ℤ
h : n.sign = -1
⊢ (∀ ⦃a₁ a₂ : M⦄, n.natAbs • a₁ = n.natAbs • a₂ → a₁ = a₂) ↔
    ∀ ⦃a₁ a₂ : M⦄, (n.sign * ↑n.natAbs) • a₁ = (n.sign * ↑n.natAbs) • a₂ → a₁ = a₂

Tactic:
·

Goal state after:
case inl
M : Type u_3
inst✝ : SubtractionMonoid M
n : ℤ
h : n.sign = 1
⊢ (∀ ⦃a₁ a₂ : M⦄, n.natAbs • a₁ = n.natAbs • a₂ → a₁ = a₂) ↔
    ∀ ⦃a₁ a₂ : M⦄, (n.sign * ↑n.natAbs) • a₁ = (n.sign * ↑n.natAbs) • a₂ → a₁ = a₂
Module: Mathlib.Algebra.Regular.SMul

Goal state before:
pp: case inr.inl
M : Type u_3
inst✝ : SubtractionMonoid M
n : ℤ
h : n.sign = 0
⊢ (∀ ⦃a₁ a₂ : M⦄, n.natAbs • a₁ = n.natAbs • a₂ → a₁ = a₂) ↔
    ∀ ⦃a₁ a₂ : M⦄, (n.sign * ↑n.natAbs) • a₁ = (n.sign * ↑n.natAbs) • a₂ → a₁ = a₂

pp: case inr.inr
M : Type u_3
inst✝ : SubtractionMonoid M
n : ℤ
h : n.sign = -1
⊢ (∀ ⦃a₁ a₂ : M⦄, n.natAbs • a₁ = n.natAbs • a₂ → a₁ = a₂) ↔
    ∀ ⦃a₁ a₂ : M⦄, (n.sign * ↑n.natAbs) • a₁ = (n.sign * ↑n.natAbs) • a₂ → a₁ = a₂

Tactic:
·

Goal state after:
case inr.inl
M : Type u_3
inst✝ : SubtractionMonoid M
n : ℤ
h : n.sign = 0
⊢ (∀ ⦃a₁ a₂ : M⦄, n.natAbs • a₁ = n.natAbs • a₂ → a₁ = a₂) ↔
    ∀ ⦃a₁ a₂ : M⦄, (n.sign * ↑n.natAbs) • a₁ = (n.sign * ↑n.natAbs) • a₂ → a₁ = a₂
Module: Mathlib.Algebra.Regular.SMul

Goal state before:
pp: case inr.inr
M : Type u_3
inst✝ : SubtractionMonoid M
n : ℤ
h : n.sign = -1
⊢ (∀ ⦃a₁ a₂ : M⦄, n.natAbs • a₁ = n.natAbs • a₂ → a₁ = a₂) ↔
    ∀ ⦃a₁ a₂ : M⦄, (n.sign * ↑n.natAbs) • a₁ = (n.sign * ↑n.natAbs) • a₂ → a₁ = a₂

Tactic:
·

Goal state after:
case inr.inr
M : Type u_3
inst✝ : SubtractionMonoid M
n : ℤ
h : n.sign = -1
⊢ (∀ ⦃a₁ a₂ : M⦄, n.natAbs • a₁ = n.natAbs • a₂ → a₁ = a₂) ↔
    ∀ ⦃a₁ a₂ : M⦄, (n.sign * ↑n.natAbs) • a₁ = (n.sign * ↑n.natAbs) • a₂ → a₁ = a₂
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: case refine_2
α : Type u
h : Fintype α
⊢ ∀ (f : PEmpty.{u + 1} → Cardinal.{v}), prod f = lift.{u, v} (∏ i, f i)

pp: case refine_3
α : Type u
h : Fintype α
⊢ ∀ (α : Type u) [inst : Fintype α],
    (∀ (f : α → Cardinal.{v}), prod f = lift.{u, v} (∏ i, f i)) →
      ∀ (f : Option α → Cardinal.{v}), prod f = lift.{u, v} (∏ i, f i)

Tactic:
·

Goal state after:
case refine_2
α : Type u
h : Fintype α
⊢ ∀ (f : PEmpty.{u + 1} → Cardinal.{v}), prod f = lift.{u, v} (∏ i, f i)