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

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

Tactic:
]

Goal state after:
c : Cardinal.{u}
d : Cardinal.{v}
h : ∀ (n : ℕ), ↑n ≤ c ↔ ↑n ≤ d
h' : ℵ₀ ≤ c ↔ ℵ₀ ≤ 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 ≤ ↑(toNat c) ↔ ↑n ≤ ↑(toNat d)
h' : ℵ₀ ≤ c ↔ ℵ₀ ≤ d
hc : ¬ℵ₀ ≤ c
hd : ¬ℵ₀ ≤ d
⊢ ∀ (c_1 : ℕ), c_1 ≤ toNat c ↔ c_1 ≤ toNat d

Tactic:
]

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

Goal state before:
pp: x : Cardinal.{v}
m : ℕ∞
⊢ x < ↑m ↔ x < ↑m

Tactic:
]

Goal state after:
Module: Mathlib.SetTheory.Cardinal.ENat

Goal state before:
pp: x : Cardinal.{v}
m : ℕ∞
⊢ x ≤ ↑m ↔ x ≤ ↑m

Tactic:
]

Goal state after:
Module: Mathlib.SetTheory.Cardinal.ENat

Goal state before:
pp: x : Cardinal.{v}
m : ℕ∞
⊢ x = ↑m ↔ x = ↑m

Tactic:
]

Goal state after:
Module: Mathlib.SetTheory.Cardinal.ENat

Goal state before:
pp: x : Cardinal.{v}
m : ℕ∞
⊢ ↑m < x ↔ ↑m < x

Tactic:
]

Goal state after:
Module: Mathlib.SetTheory.Cardinal.ENat

Goal state before:
pp: x : Cardinal.{v}
m : ℕ∞
⊢ ↑m ≤ x ↔ ↑m ≤ x

Tactic:
]

Goal state after:
Module: Mathlib.SetTheory.Cardinal.ENat

Goal state before:
pp: x : Cardinal.{v}
m : ℕ∞
⊢ ↑m = x ↔ ↑m = x

Tactic:
]

Goal state after:
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.toENatAux * y.toENatAux = x.toENatAux * y.toENatAux

Tactic:
]

Goal state after:
Module: Mathlib.SetTheory.Cardinal.ENat

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

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

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.inr
x y : Cardinal.{u}
hle : x ≤ y
hy : ℵ₀ ≤ y
hx : x ≠ 0
⊢ ¬x = 0

Tactic:
]

Goal state after:
case inr.inr
x y : Cardinal.{u}
hle : x ≤ y
hy : ℵ₀ ≤ y
hx : x ≠ 0
⊢ ¬x = 0
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.toENatAux + y.toENatAux = x.toENatAux + y.toENatAux

Tactic:
]

Goal state after:
Module: Mathlib.SetTheory.Cardinal.ENat

Goal state before:
pp: a : Cardinal.{u_1}
⊢ (∃ b, a = ↑b) ↔ a ≤ ℵ₀

Tactic:
]

Goal state after:
a : Cardinal.{u_1}
⊢ (∃ b, a = ↑b) ↔ a ≤ ℵ₀
Module: Mathlib.SetTheory.Cardinal.ENat

Goal state before:
pp: c : Cardinal.{u}
n : ℕ
⊢ ↑n ≤ c ↔ ↑n ≤ c

Tactic:
]

Goal state after:
Module: Mathlib.SetTheory.Cardinal.ENat

Goal state before:
pp: α : Type u
β : Type v
e : α ≃ β
⊢ toENat #β = toENat #β

Tactic:
]

Goal state after:
Module: Mathlib.SetTheory.Cardinal.ENat

Goal state before:
pp: m : ℕ∞
⊢ ℵ₀ = ℵ₀

Tactic:
]

Goal state after:
Module: Mathlib.SetTheory.Cardinal.ENat

Goal state before:
pp: case coe
m : ℕ
hm : ↑m ≠ 0
⊢ ℵ₀ = ℵ₀

Tactic:
]

Goal state after:
Module: Mathlib.SetTheory.Cardinal.ENat

Goal state before:
pp: m : ℕ∞
hm : m ≠ 0
⊢ ℵ₀ = ℵ₀

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Module.RingHom

Goal state before:
pp: R✝ : Type u_1
S✝ : Type u_2
M✝ : Type u_3
M₂ : Type u_4
inst✝⁷ : Semiring R✝
inst✝⁶ : AddCommMonoid M✝
inst✝⁵ : Module R✝ M✝
r s : R✝
x✝ : M✝
R : Type u_5
S : Type u_6
M : Type u_7
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Semiring S
inst✝ : SMul S M
f : R →+* S
hf : Surjective ⇑f
hsmul : ∀ (c : R) (x : M), f c • x = c • x
x : M
⊢ 0 = 0

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Ring.CompTypeclasses

Goal state before:
pp: R₁ : Type u_1
R₂ : Type u_2
inst✝² : Semiring R₁
inst✝¹ : Semiring R₂
σ : R₁ →+* R₂
σ' : R₂ →+* R₁
inst✝ : RingHomInvPair σ σ'
x : R₁
⊢ (RingHom.id R₁) x = x

Tactic:
]

Goal state after:
R₁ : Type u_1
R₂ : Type u_2
inst✝² : Semiring R₁
inst✝¹ : Semiring R₂
σ : R₁ →+* R₂
σ' : R₂ →+* R₁
inst✝ : RingHomInvPair σ σ'
x : R₁
⊢ (RingHom.id R₁) x = x
Module: Mathlib.Algebra.Group.Hom.CompTypeclasses

Goal state before:
pp: M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid P
φ : M →* N
ψ : N →* P
χ : M →* P
κ : φ.CompTriple ψ χ
⊢ ⇑χ = ⇑χ

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Group.Hom.CompTypeclasses

Goal state before:
pp: M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid P
φ : M →* N
ψ : N →* P
χ : M →* P
h : φ.CompTriple ψ χ
x : M
⊢ ψ (φ x) = ψ (φ x)

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Ring.CompTypeclasses

Goal state before:
pp: R₁ : Type u_1
R₂ : Type u_2
inst✝² : Semiring R₁
inst✝¹ : Semiring R₂
σ : R₁ →+* R₂
σ' : R₂ →+* R₁
inst✝ : RingHomInvPair σ σ'
x : R₂
⊢ (RingHom.id R₂) x = x

Tactic:
]

Goal state after:
R₁ : Type u_1
R₂ : Type u_2
inst✝² : Semiring R₁
inst✝¹ : Semiring R₂
σ : R₁ →+* R₂
σ' : R₂ →+* R₁
inst✝ : RingHomInvPair σ σ'
x : R₂
⊢ (RingHom.id R₂) x = x
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: α : Type u
s : Set α
⊢ Nonempty (↑(ULift.down ⁻¹' s) ≃ ULift.{v, u} ↑s)

Tactic:
]

Goal state after:
α : Type u
s : Set α
⊢ Nonempty (↑(ULift.down ⁻¹' s) ≃ ULift.{v, u} ↑s)
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: α : Type (max u v)
inst✝ : Small.{v, max u v} α
⊢ #α = #α

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Ring.CompTypeclasses

Goal state before:
pp: R₁ : Type u_1
R₂ : Type u_2
R₃ : Type u_3
inst✝⁵ : Semiring R₁
inst✝⁴ : Semiring R₂
inst✝³ : Semiring R₃
σ₁₂ : R₁ →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R₁ →+* R₃
inst✝² : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝¹ : RingHomSurjective σ₁₂
inst✝ : RingHomSurjective σ₂₃
this : Function.Surjective ⇑σ₁₃
⊢ Function.Surjective ⇑σ₁₃

Tactic:
]

Goal state after:
R₁ : Type u_1
R₂ : Type u_2
R₃ : Type u_3
inst✝⁵ : Semiring R₁
inst✝⁴ : Semiring R₂
inst✝³ : Semiring R₃
σ₁₂ : R₁ →+* R₂
σ₂₃ : R₂ →+* R₃
σ₁₃ : R₁ →+* R₃
inst✝² : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃
inst✝¹ : RingHomSurjective σ₁₂
inst✝ : RingHomSurjective σ₂₃
this : Function.Surjective ⇑σ₁₃
⊢ Function.Surjective ⇑σ₁₃
Module: Mathlib.Logic.Function.CompTypeclasses

Goal state before:
pp: M : Type u_1
N : Type u_2
P : Type u_3
φ : M → N
ψ : N → P
χ : M → P
h : CompTriple φ ψ χ
x : M
⊢ ψ (φ x) = ψ (φ x)

Tactic:
]

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

Goal state before:
pp: case refine_1
α✝ : Type u
h✝ : Fintype α✝
α β : Type u
hβ : Fintype β
e : α ≃ β
h : ∀ (f : α → Cardinal.{v}), prod f = lift.{u, v} (∏ i, f i)
f : β → Cardinal.{v}
this : Fintype α := Fintype.ofEquiv β e.symm
⊢ prod f = prod fun i ↦ f (e i)

Tactic:
]

Goal state after:
case refine_1
α✝ : Type u
h✝ : Fintype α✝
α β : Type u
hβ : Fintype β
e : α ≃ β
h : ∀ (f : α → Cardinal.{v}), prod f = lift.{u, v} (∏ i, f i)
f : β → Cardinal.{v}
this : Fintype α := Fintype.ofEquiv β e.symm
⊢ prod f = prod fun i ↦ f (e i)
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: case refine_1
α✝ : Type u
h✝ : Fintype α✝
α β : Type u
hβ : Fintype β
e : α ≃ β
h : ∀ (f : α → Cardinal.{v}), prod f = lift.{u, v} (∏ i, f i)
f : β → Cardinal.{v}
this : Fintype α := Fintype.ofEquiv β e.symm
⊢ prod f = prod fun i ↦ f (e i)

Tactic:
exact mk_congr (e.piCongrLeft _).symm

Goal state after:
Module: Mathlib.Algebra.Regular.SMul

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u_3
s : S
inst✝³ : SMul R M
inst✝² : SMul R S
inst✝¹ : SMul S M
inst✝ : IsScalarTower R S M
a : R
ab : IsSMulRegular M (a • s)
c d : M
cd : (a • s) • c = (a • s) • d
⊢ c = d

Tactic:
]

Goal state after:
R : Type u_1
S : Type u_2
M : Type u_3
s : S
inst✝³ : SMul R M
inst✝² : SMul R S
inst✝¹ : SMul S M
inst✝ : IsScalarTower R S M
a : R
ab : IsSMulRegular M (a • s)
c d : M
cd : (a • s) • c = (a • s) • d
⊢ c = d
Module: Mathlib.Algebra.Regular.SMul

Goal state before:
pp: R : Type u_1
M : Type u_3
a b : R
inst✝² : SMul R M
inst✝¹ : Mul R
inst✝ : IsScalarTower R R M
ab : IsSMulRegular M (a • b)
⊢ IsSMulRegular M b

Tactic:
]

Goal state after:
R : Type u_1
M : Type u_3
a b : R
inst✝² : SMul R M
inst✝¹ : Mul R
inst✝ : IsScalarTower R R M
ab : IsSMulRegular M (a • b)
⊢ IsSMulRegular M b
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: case refine_2
α : Type u
h : Fintype α
f : PEmpty.{u + 1} → Cardinal.{v}
⊢ 1 = 1

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Regular.SMul

Goal state before:
pp: R : Type u_1
M : Type u_3
inst✝¹ : Monoid R
inst✝ : MulAction R M
a b : M
ab : a = b
⊢ a = b

Tactic:
]

Goal state after:
R : Type u_1
M : Type u_3
inst✝¹ : Monoid R
inst✝ : MulAction R M
a b : M
ab : a = b
⊢ a = b
Module: Mathlib.Algebra.Regular.SMul

Goal state before:
pp: R : Type u_1
M : Type u_3
a b : R
inst✝¹ : Monoid R
inst✝ : MulAction R M
h : a * b = 1
⊢ IsSMulRegular M 1

Tactic:
]

Goal state after:
R : Type u_1
M : Type u_3
a b : R
inst✝¹ : Monoid R
inst✝ : MulAction R M
h : a * b = 1
⊢ IsSMulRegular M 1
Module: Mathlib.Algebra.Regular.SMul

Goal state before:
pp: case zero
R : Type u_1
M : Type u_3
a : R
inst✝¹ : Monoid R
inst✝ : MulAction R M
ra : IsSMulRegular M a
⊢ IsSMulRegular M 1

Tactic:
]

Goal state after:
case zero
R : Type u_1
M : Type u_3
a : R
inst✝¹ : Monoid R
inst✝ : MulAction R M
ra : IsSMulRegular M a
⊢ IsSMulRegular M 1
Module: Mathlib.Algebra.Regular.SMul

Goal state before:
pp: case succ
R : Type u_1
M : Type u_3
a : R
inst✝¹ : Monoid R
inst✝ : MulAction R M
ra : IsSMulRegular M a
n : ℕ
hn : IsSMulRegular M (a ^ n)
⊢ IsSMulRegular M (a * a ^ n)

Tactic:
]

Goal state after:
case succ
R : Type u_1
M : Type u_3
a : R
inst✝¹ : Monoid R
inst✝ : MulAction R M
ra : IsSMulRegular M a
n : ℕ
hn : IsSMulRegular M (a ^ n)
⊢ IsSMulRegular M (a * a ^ n)
Module: Mathlib.Algebra.Regular.SMul

Goal state before:
pp: R : Type u_1
M : Type u_3
a : R
inst✝¹ : Monoid R
inst✝ : MulAction R M
n : ℕ
n0 : 0 < n
⊢ IsSMulRegular M (a ^ n.pred • a) → IsSMulRegular M a

Tactic:
]

Goal state after:
R : Type u_1
M : Type u_3
a : R
inst✝¹ : Monoid R
inst✝ : MulAction R M
n : ℕ
n0 : 0 < n
⊢ IsSMulRegular M (a ^ n.pred • a) → IsSMulRegular M a
Module: Mathlib.Algebra.Regular.SMul

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u_3
a : R
s : S
inst✝⁴ : Monoid S
inst✝³ : SMul R M
inst✝² : SMul R S
inst✝¹ : MulAction S M
inst✝ : IsScalarTower R S M
h : a • s = 1
⊢ IsSMulRegular M 1

Tactic:
]

Goal state after:
R : Type u_1
S : Type u_2
M : Type u_3
a : R
s : S
inst✝⁴ : Monoid S
inst✝³ : SMul R M
inst✝² : SMul R S
inst✝¹ : MulAction S M
inst✝ : IsScalarTower R S M
h : a • s = 1
⊢ IsSMulRegular M 1
Module: Mathlib.Algebra.Regular.SMul

Goal state before:
pp: R : Type u_1
M : Type u_3
inst✝² : MonoidWithZero R
inst✝¹ : Zero M
inst✝ : MulActionWithZero R M
h : IsSMulRegular M 0
a b : M
⊢ 0 = 0 • b

Tactic:
]

Goal state after:
R : Type u_1
M : Type u_3
inst✝² : MonoidWithZero R
inst✝¹ : Zero M
inst✝ : MulActionWithZero R M
h : IsSMulRegular M 0
a b : M
⊢ 0 = 0 • b
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: case refine_3
α✝ : Type u
h✝ : Fintype α✝
α : Type u
hα : Fintype α
h : ∀ (f : α → Cardinal.{v}), prod f = lift.{u, v} (∏ i, f i)
f : Option α → Cardinal.{v}
⊢ (lift.{u, v} (f none) * prod fun i ↦ lift.{v, v} (f (some i))) = lift.{u, v} (f none) * prod fun a ↦ f (some a)

Tactic:
]

Goal state after:
case refine_3
α✝ : Type u
h✝ : Fintype α✝
α : Type u
hα : Fintype α
h : ∀ (f : α → Cardinal.{v}), prod f = lift.{u, v} (∏ i, f i)
f : Option α → Cardinal.{v}
⊢ (lift.{u, v} (f none) * prod fun i ↦ lift.{v, v} (f (some i))) = lift.{u, v} (f none) * prod fun a ↦ f (some a)
Module: Mathlib.Algebra.Regular.SMul

Goal state before:
pp: R : Type u_1
M : Type u_3
inst✝² : MonoidWithZero R
inst✝¹ : Zero M
inst✝ : MulActionWithZero R M
h : IsSMulRegular M 0
a b : M
⊢ 0 = 0

Tactic:
]

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

Goal state before:
pp: α : Type u
⊢ Nontrivial α ↔ Nontrivial α

Tactic:
]

Goal state after:
Module: Mathlib.Algebra.Regular.SMul

Goal state before:
pp: R : Type u_1
M : Type u_3
inst✝² : MonoidWithZero R
inst✝¹ : Zero M
inst✝ : MulActionWithZero R M
⊢ (¬∃ x y, x ≠ y) ↔ ∀ (x y : M), x = y

Tactic:
]

Goal state after:
R : Type u_1
M : Type u_3
inst✝² : MonoidWithZero R
inst✝¹ : Zero M
inst✝ : MulActionWithZero R M
⊢ (¬∃ x y, x ≠ y) ↔ ∀ (x y : M), x = y
Module: Mathlib.Algebra.Regular.SMul

Goal state before:
pp: R : Type u_1
M : Type u_3
a b : R
inst✝² : CommSemigroup R
inst✝¹ : SMul R M
inst✝ : IsScalarTower R R M
⊢ IsSMulRegular M (a * b) ↔ IsSMulRegular M (a * b) ∧ IsSMulRegular M (b * a)

Tactic:
]

Goal state after:
R : Type u_1
M : Type u_3
a b : R
inst✝² : CommSemigroup R
inst✝¹ : SMul R M
inst✝ : IsScalarTower R R M
⊢ IsSMulRegular M (a * b) ↔ IsSMulRegular M (a * b) ∧ IsSMulRegular M (b * a)
Module: Mathlib.Algebra.Regular.SMul

Goal state before:
pp: R : Type u_1
M : Type u_3
a b : R
inst✝² : CommSemigroup R
inst✝¹ : SMul R M
inst✝ : IsScalarTower R R M
ab : IsSMulRegular M (a * b)
⊢ IsSMulRegular M (a * b)

Tactic:
]

Goal state after:
R : Type u_1
M : Type u_3
a b : R
inst✝² : CommSemigroup R
inst✝¹ : SMul R M
inst✝ : IsScalarTower R R M
ab : IsSMulRegular M (a * b)
⊢ IsSMulRegular M (a * b)
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: α β : Type u
a : Cardinal.{u}
⊢ Small.{u, u + 1} ↑(Iic #(Quotient.out a))

Tactic:
]

Goal state after:
α β : Type u
a : Cardinal.{u}
⊢ Small.{u, u + 1} ↑(Iic #(Quotient.out a))
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: f : Cardinal.{u} → Cardinal.{max u v}
s : Set Cardinal.{u}
hs : Small.{u, u + 1} ↑s
⊢ Small.{max u v, (max u v) + 1} ↑(f '' s)

Tactic:
]

Goal state after:
f : Cardinal.{u} → Cardinal.{max u v}
s : Set Cardinal.{u}
hs : Small.{u, u + 1} ↑s
⊢ Small.{max u v, (max u v) + 1} ↑(f '' s)
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: ι : Type u
f : ι → Cardinal.{v}
hf : BddAbove (range f)
g : Cardinal.{v} → Cardinal.{max v w}
⊢ BddAbove (g '' range f)

Tactic:
]

Goal state after:
ι : Type u
f : ι → Cardinal.{v}
hf : BddAbove (range f)
g : Cardinal.{v} → Cardinal.{max v w}
⊢ BddAbove (g '' range f)
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: h : Small.{u, max (u + 1) (v + 1)} Cardinal.{max u v}
this : BddAbove univ
⊢ False

Tactic:
]

Goal state after:
h : Small.{u, max (u + 1) (v + 1)} Cardinal.{max u v}
this : BddAbove univ
⊢ False
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: ι : Type u
f : ι → Cardinal.{v}
⊢ (sum fun i ↦ lift.{max u v, v} (f i)) ≤ sum fun x ↦ ⨆ i, lift.{u, v} (f i)

Tactic:
]

Goal state after:
ι : Type u
f : ι → Cardinal.{v}
⊢ (sum fun i ↦ lift.{max u v, v} (f i)) ≤ sum fun x ↦ ⨆ i, lift.{u, v} (f i)
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: ι : Type u
f : ι → Cardinal.{v}
i : ι
⊢ lift.{u, v} (f i) ≤ ⨆ i, lift.{u, v} (f i)

Tactic:
]

Goal state after:
ι : Type u
f : ι → Cardinal.{v}
i : ι
⊢ lift.{u, v} (f i) ≤ ⨆ i, lift.{u, v} (f i)
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: s : Set Cardinal.{u_1}
hs : BddAbove s
d : Cardinal.{u_1}
hc : lift.{u, u_1} d ∈ upperBounds (lift.{u, u_1} '' s)
h : ¬∀ x ∈ s, x ≤ d
⊢ False

Tactic:
]

Goal state after:
s : Set Cardinal.{u_1}
hs : BddAbove s
d : Cardinal.{u_1}
hc : lift.{u, u_1} d ∈ upperBounds (lift.{u, u_1} '' s)
h : ¬∀ x ∈ s, x ≤ d
⊢ False
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: ι : Type v
f : ι → Cardinal.{w}
hf : BddAbove (range f)
⊢ sSup (range (lift.{u, w} ∘ f)) = sSup (range fun i ↦ lift.{u, w} (f i))

Tactic:
]

Goal state after:
ι : Type v
f : ι → Cardinal.{w}
hf : BddAbove (range f)
⊢ sSup (range (lift.{u, w} ∘ f)) = sSup (range fun i ↦ lift.{u, w} (f i))
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: ι : Type v
f : ι → Cardinal.{w}
t : Cardinal.{max u w}
hf : BddAbove (range f)
w : ∀ (i : ι), lift.{u, w} (f i) ≤ t
⊢ ⨆ i, lift.{u, w} (f i) ≤ t

Tactic:
]

Goal state after:
ι : Type v
f : ι → Cardinal.{w}
t : Cardinal.{max u w}
hf : BddAbove (range f)
w : ∀ (i : ι), lift.{u, w} (f i) ≤ t
⊢ ⨆ i, lift.{u, w} (f i) ≤ t
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: ι : Type v
f : ι → Cardinal.{w}
hf : BddAbove (range f)
t : Cardinal.{max u w}
⊢ ⨆ i, lift.{u, w} (f i) ≤ t ↔ ∀ (i : ι), lift.{u, w} (f i) ≤ t

Tactic:
]

Goal state after:
ι : Type v
f : ι → Cardinal.{w}
hf : BddAbove (range f)
t : Cardinal.{max u w}
⊢ ⨆ i, lift.{u, w} (f i) ≤ t ↔ ∀ (i : ι), lift.{u, w} (f i) ≤ t
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: ι : Type v
ι' : Type v'
f : ι → Cardinal.{w}
f' : ι' → Cardinal.{w'}
hf : BddAbove (range f)
hf' : BddAbove (range f')
g : ι → ι'
h : ∀ (i : ι), lift.{w', w} (f i) ≤ lift.{w, w'} (f' (g i))
⊢ ⨆ i, lift.{w', w} (f i) ≤ ⨆ i, lift.{w, w'} (f' i)

Tactic:
]

Goal state after:
ι : Type v
ι' : Type v'
f : ι → Cardinal.{w}
f' : ι' → Cardinal.{w'}
hf : BddAbove (range f)
hf' : BddAbove (range f')
g : ι → ι'
h : ∀ (i : ι), lift.{w', w} (f i) ≤ lift.{w, w'} (f' (g i))
⊢ ⨆ i, lift.{w', w} (f i) ≤ ⨆ i, lift.{w, w'} (f' i)
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: ι : Type u
inst✝ : Small.{v, u} ι
f : ι → Cardinal.{v}
⊢ ⨆ i, lift.{u, v} (f i) ≤ sum f

Tactic:
]

Goal state after:
ι : Type u
inst✝ : Small.{v, u} ι
f : ι → Cardinal.{v}
⊢ ⨆ i, lift.{u, v} (f i) ≤ sum f
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: n : ℕ
⊢ ↑n < ↑n.succ

Tactic:
]

Goal state after:
n : ℕ
⊢ ↑n < ↑n.succ
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: n : ℕ
c : Cardinal.{u_1}
⊢ ↑n + 1 ≤ c ↔ ↑n + 1 ≤ c

Tactic:
]

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

Goal state before:
pp: n : ℕ
c : Cardinal.{u_1}
⊢ c < ↑n + 1 ↔ c < ↑n + 1

Tactic:
]

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

Goal state before:
pp: α : Type u
n : ℕ
H : ↑n < #α
⊢ ↑(n + 1) ≤ #α

Tactic:
simpa using H

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

Goal state before:
pp: a b : Cardinal.{u_1}
hb : 2 ≤ b
⊢ a < b ^ a

Tactic:
]

Goal state after:
a b : Cardinal.{u_1}
hb : 2 ≤ b
⊢ a < b ^ a
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: c : Cardinal.{u_1}
⊢ 0 < c ↔ 0 < c

Tactic:
]

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

Goal state before:
pp: c : Cardinal.{u_1}
⊢ c ≠ 0 ↔ c ≠ 0

Tactic:
]

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

Goal state before:
pp: n : ℕ
⊢ Nonempty (Fin (n + 1) ↪ ℕ)

Tactic:
]

Goal state after:
n : ℕ
⊢ Nonempty (Fin (n + 1) ↪ ℕ)
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: c : Cardinal.{u_1}
h : c < ℵ₀
n : ℕ
hn : c = ↑n
⊢ ↑n + 1 = ↑n + 1

Tactic:
]

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

Goal state before:
pp: n : ℕ
ha : ↑n < ℵ₀
⊢ ↑(n + 1) < ℵ₀

Tactic:
]

Goal state after:
n : ℕ
ha : ↑n < ℵ₀
⊢ ↑(n + 1) < ℵ₀
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: ⊢ ℵ₀ ≠ 0 ∧ IsSuccPrelimit ℵ₀

Tactic:
]

Goal state after:
⊢ ℵ₀ ≠ 0 ∧ IsSuccPrelimit ℵ₀
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: n : ℕ
h : IsSuccLimit (succ ↑n)
⊢ False

Tactic:
]

Goal state after:
n : ℕ
h : IsSuccLimit (succ ↑n)
⊢ False
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: ι : Type u
inst✝ : Nonempty ι
f : ι → Cardinal.{v}
hf : BddAbove (range f)
n : ℕ
h : ⨆ i, f i = ↑n
⊢ ∃ i, f i = ⨆ i, f i

Tactic:
]

Goal state after:
ι : Type u
inst✝ : Nonempty ι
f : ι → Cardinal.{v}
hf : BddAbove (range f)
n : ℕ
h : ⨆ i, f i = ↑n
⊢ ∃ i, f i = ⨆ i, f i
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: α : Type u
n : ℕ
⊢ Nonempty (α ≃ Fin n) ↔ Nonempty (α ≃ Fin n)

Tactic:
]

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

Goal state before:
pp: α : Type u
⊢ Nonempty (α ↪ ℕ) ↔ Nonempty (α ↪ ℕ)

Tactic:
]

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

Goal state before:
pp: α : Type u
⊢ Countable α ↔ Countable α

Tactic:
]

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

Goal state before:
pp: a b : Cardinal.{u_1}
m n : ℕ
ha : ↑m < ℵ₀
hb : ↑n < ℵ₀
⊢ ↑(m + n) < ℵ₀

Tactic:
]

Goal state after:
a b : Cardinal.{u_1}
m n : ℕ
ha : ↑m < ℵ₀
hb : ↑n < ℵ₀
⊢ ↑(m + n) < ℵ₀
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: a : Cardinal.{u_1}
n : ℕ
⊢ (n + 1 = 0 ∨ a < ℵ₀) ∧ a < ℵ₀ ↔ n + 2 = 0 ∨ a < ℵ₀

Tactic:
]

Goal state after:
a : Cardinal.{u_1}
n : ℕ
⊢ (n + 1 = 0 ∨ a < ℵ₀) ∧ a < ℵ₀ ↔ n + 2 = 0 ∨ a < ℵ₀
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: a b : Cardinal.{u_1}
m n : ℕ
ha : ↑m < ℵ₀
hb : ↑n < ℵ₀
⊢ ↑(m * n) < ℵ₀

Tactic:
]

Goal state after:
a b : Cardinal.{u_1}
m n : ℕ
ha : ↑m < ℵ₀
hb : ↑n < ℵ₀
⊢ ↑(m * n) < ℵ₀
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: case neg
a b : Cardinal.{u_1}
h : a * b < ℵ₀
ha : 1 ≤ a
hb : 1 ≤ b
⊢ a < ℵ₀ ∧ b < ℵ₀

Tactic:
]

Goal state after:
case neg
a b : Cardinal.{u_1}
h : a * b < ℵ₀
ha : 1 ≤ a
hb : 1 ≤ b
⊢ a < ℵ₀ ∧ b < ℵ₀
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: case neg.left
a b : Cardinal.{u_1}
h : a * b < ℵ₀
ha : 1 ≤ a
hb : 1 ≤ b
⊢ a * 1 < ℵ₀

Tactic:
]

Goal state after:
case neg.left
a b : Cardinal.{u_1}
h : a * b < ℵ₀
ha : 1 ≤ a
hb : 1 ≤ b
⊢ a * 1 < ℵ₀
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: case neg.right
a b : Cardinal.{u_1}
h : a * b < ℵ₀
ha : 1 ≤ a
hb : 1 ≤ b
⊢ 1 * b < ℵ₀

Tactic:
]

Goal state after:
case neg.right
a b : Cardinal.{u_1}
h : a * b < ℵ₀
ha : 1 ≤ a
hb : 1 ≤ b
⊢ 1 * b < ℵ₀
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: a b : Cardinal.{u_1}
h : ℵ₀ ≤ a * b ↔ ¬a = 0 ∧ ¬b = 0 ∧ (ℵ₀ ≤ a ∨ ℵ₀ ≤ b)
⊢ ℵ₀ ≤ a * b ↔ a ≠ 0 ∧ b ≠ 0 ∧ (ℵ₀ ≤ a ∨ ℵ₀ ≤ b)

Tactic:
]

Goal state after:
a b : Cardinal.{u_1}
h : ℵ₀ ≤ a * b ↔ ¬a = 0 ∧ ¬b = 0 ∧ (ℵ₀ ≤ a ∨ ℵ₀ ≤ b)
⊢ ℵ₀ ≤ a * b ↔ a ≠ 0 ∧ b ≠ 0 ∧ (ℵ₀ ≤ a ∨ ℵ₀ ≤ b)
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: a b : Cardinal.{u_1}
m n : ℕ
ha : ↑m < ℵ₀
hb : ↑n < ℵ₀
⊢ ↑(m ^ n) < ℵ₀

Tactic:
]

Goal state after:
a b : Cardinal.{u_1}
m n : ℕ
ha : ↑m < ℵ₀
hb : ↑n < ℵ₀
⊢ ↑(m ^ n) < ℵ₀
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: α : Type u
⊢ Infinite α ↔ Infinite α

Tactic:
]

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

Goal state before:
pp: α : Type u_1
s : Set α
⊢ s.Countable ∧ Infinite ↑s ↔ s.Countable ∧ Infinite ↑s

Tactic:
]

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

Goal state before:
pp: n : ℕ
hn : n ≠ 0
⊢ n ≠ 0

Tactic:
]

Goal state after:
n : ℕ
hn : n ≠ 0
⊢ n ≠ 0
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: n : ℕ
hn : n ≠ 0
⊢ ℵ₀ = ℵ₀

Tactic:
]

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

Goal state before:
pp: n : ℕ
⊢ ℵ₀ = ℵ₀

Tactic:
]

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

Goal state before:
pp: ⊢ 1 = 1

Tactic:
]

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

Goal state before:
pp: α : Type u
s : Set α
⊢ s = ∅ ↔ s = ∅

Tactic:
]

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

Goal state before:
pp: α : Type u
s : Set α
⊢ s.Nonempty ↔ s.Nonempty

Tactic:
]

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

Goal state before:
pp: α β : Type u
s : Set α
t : Set β
⊢ #(↑s × ↑t) = #(↑s × ↑t)

Tactic:
]

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

Goal state before:
pp: α β γ : Type u
f : α → β → γ
s : Set α
t : Set β
⊢ #↑(uncurry f '' s ×ˢ t) ≤ #↑(s ×ˢ t)

Tactic:
]

Goal state after:
α β γ : Type u
f : α → β → γ
s : Set α
t : Set β
⊢ #↑(uncurry f '' s ×ˢ t) ≤ #↑(s ×ˢ t)
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: α : Type u
β : Type v
f : α → β
hf : Injective f
⊢ lift.{u, v} #↑(range f) ≤ lift.{u, v} #β

Tactic:
]

Goal state after:
α : Type u
β : Type v
f : α → β
hf : Injective f
⊢ lift.{u, v} #↑(range f) ≤ lift.{u, v} #β