mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Regular.SMul

Goal state before:
pp: R : Type u_1
G : Type u_4
inst✝¹ : Group G
inst✝ : MulAction G R
g : G
⊢ IsSMulRegular R g

Tactic:
by

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

Goal state before:
pp: s : Set Cardinal.{u_1}
⊢ sInf s = 0 ↔ s = ∅ ∨ ∃ a ∈ s, a = 0

Tactic:
by

Goal state after:
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
ua : IsUnit a
⊢ IsSMulRegular M a

Tactic:
by

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

Goal state before:
pp: ι : Sort u_1
f : ι → Cardinal.{u_2}
⊢ ⨅ i, f i = 0 ↔ IsEmpty ι ∨ ∃ i, f i = 0

Tactic:
by

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

Goal state before:
pp: R : Type u_1
M : Type u_3
inst✝¹ : AddGroup M
inst✝ : DistribSMul R M
r : R
h : ∀ (m : M), r • m = 0 → m = 0
m₁ m₂ : M
eq : (fun x ↦ r • x) m₁ = (fun x ↦ r • x) m₂
⊢ r • (m₁ - m₂) = 0

Tactic:
by

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

Goal state before:
pp: s : Set Cardinal.{v}
⊢ lift.{u, v} (sInf s) = sInf (lift.{u, v} '' s)

Tactic:
by

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

Goal state before:
pp: ι : Sort u_1
f : ι → Cardinal.{v}
⊢ lift.{u, v} (iInf f) = ⨅ i, lift.{u, v} (f i)

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: s : Set Cardinal.{u}
⊢ Small.{u, u + 1} ↑s → BddAbove s

Tactic:
by

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

Goal state before:
pp: f : Cardinal.{u} → Cardinal.{max u v}
s : Set Cardinal.{u}
hs : BddAbove s
⊢ BddAbove (f '' s)

Tactic:
by

Goal state after:
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 (range (g ∘ f))

Tactic:
by

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

Goal state before:
pp: ⊢ ¬Small.{u, max (u + 1) (v + 1)} Cardinal.{max u v}

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: ι : Type u
f : ι → Cardinal.{max u v}
⊢ sum f ≤ lift.{v, u} #ι * ⨆ i, f i

Tactic:
by

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

Goal state before:
pp: ι : Type u
f : ι → Cardinal.{u}
⊢ sum f ≤ #ι * ⨆ i, f i

Tactic:
by

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

Goal state before:
pp: s : Set Cardinal.{u_1}
hs : BddAbove s
⊢ lift.{u, u_1} (sSup s) = sSup (lift.{u, u_1} '' s)

Tactic:
by

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

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

Tactic:
by

Goal state after:
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
⊢ lift.{u, w} (iSup f) ≤ t

Tactic:
by

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

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

Tactic:
by

Goal state after:
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))
⊢ lift.{w', w} (iSup f) ≤ lift.{w, w'} (iSup f')

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝ : Fintype α
⊢ #(Finset α) = 2 ^ Fintype.card α

Tactic:
by

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

Goal state before:
pp: n : ℕ
⊢ succ ↑n = ↑n + 1

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: c : Cardinal.{u_1}
⊢ 2 ≤ c ↔ 1 < c

Tactic:
by

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

Goal state before:
pp: ⊢ succ 0 = 1

Tactic:
by

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

Goal state before:
pp: ⊢ 1 < 2

Tactic:
by

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

Goal state before:
pp: α : Type u_1
n : ℕ
h : ↑n ≤ #α
hα✝ : Finite α
hα : Fintype α := Fintype.ofFinite α
⊢ n ≤ Finset.univ.card

Tactic:
by

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

Goal state before:
pp: α : Type u_1
n : ℕ
h : ↑n ≤ #α
⊢ ∃ s, n = s.card

Tactic:
by

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

Goal state before:
pp: α : Type u
n : ℕ
H : ∀ (s : Finset α), s.card ≤ n
⊢ #α ≤ ↑n

Tactic:
by

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

Goal state before:
pp: a b : Cardinal.{u_1}
hb : succ 1 ≤ b
⊢ succ 1 = 2

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: c : Cardinal.{u_1}
⊢ c ≤ 1 ↔ c = 0 ∨ c = 1

Tactic:
by

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

Goal state before:
pp: n : ℕ
⊢ ↑n < ℵ₀

Tactic:
by

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

Goal state before:
pp: ⊢ 1 < ℵ₀

Tactic:
by

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

Goal state before:
pp: S : Set ℕ
h' : #↑S < #ℕ
h : lift.{u_1, 0} #↑S < ℵ₀
this : S.Finite
⊢ ∃ n, lift.{u_1, 0} #↑S = ↑n

Tactic:
by

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

Goal state before:
pp: c : Cardinal.{u_1}
h : c < ℵ₀
⊢ ∃ n, c = ↑n

Tactic:
by

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

Goal state before:
pp: c : Cardinal.{u_1}
h : c < ℵ₀
⊢ succ c = c + 1

Tactic:
by

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

Goal state before:
pp: c : Cardinal.{u_1}
h : ∀ (n : ℕ), ↑n ≤ c
hn : c < ℵ₀
⊢ False

Tactic:
by

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

Goal state before:
pp: a : Cardinal.{u_1}
ha : a < ℵ₀
⊢ succ a < ℵ₀

Tactic:
by

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

Goal state before:
pp: ⊢ IsSuccLimit ℵ₀

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: c : Cardinal.{u_1}
h : c < ℵ₀
⊢ ¬IsSuccLimit c

Tactic:
by

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

Goal state before:
pp: c : Cardinal.{u_1}
h : IsSuccLimit c
⊢ ℵ₀ ≤ c

Tactic:
by

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

Goal state before:
pp: ⊢ ℵ₀.IsStrongLimit

Tactic:
by

Goal state after:
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 = ↑n

Tactic:
by

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

Goal state before:
pp: x : Cardinal.{u_1}
⊢ x ∈ range Nat.cast ↔ x ∈ Iio ℵ₀

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u
⊢ #α < ℵ₀ ↔ Finite α

Tactic:
by

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

Goal state before:
pp: α : Type u
⊢ #α ≤ ℵ₀ ↔ Countable α

Tactic:
by

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

Goal state before:
pp: α : Type u
⊢ ℵ₀ < #α ↔ Uncountable α

Tactic:
by

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:
by

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

Goal state before:
pp: a b : Cardinal.{u_1}
⊢ ℵ₀ ≤ a + b ↔ ℵ₀ ≤ a ∨ ℵ₀ ≤ b

Tactic:
by

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

Goal state before:
pp: a : Cardinal.{u_1}
⊢ 0 • a < ℵ₀ ↔ 0 = 0 ∨ a < ℵ₀

Tactic:
by

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

Goal state before:
pp: a : Cardinal.{u_1}
⊢ 1 • a < ℵ₀ ↔ 1 = 0 ∨ a < ℵ₀

Tactic:
by

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

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

Tactic:
by

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:
by

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

Goal state before:
pp: a b : Cardinal.{u_1}
⊢ a * b < ℵ₀ ↔ a = 0 ∨ b = 0 ∨ a < ℵ₀ ∧ b < ℵ₀

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: a b : Cardinal.{u}
⊢ ℵ₀ ≤ a * b ↔ a ≠ 0 ∧ ℵ₀ ≤ b ∨ ℵ₀ ≤ a ∧ b ≠ 0

Tactic:
by

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

Goal state before:
pp: a b : Cardinal.{u_1}
ha : a ≠ 0
hb : b ≠ 0
⊢ a * b < ℵ₀ ↔ a < ℵ₀ ∧ b < ℵ₀

Tactic:
by

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:
by

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

Goal state before:
pp: α : Type u
⊢ Infinite α ↔ ℵ₀ ≤ #α

Tactic:
by

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

Goal state before:
pp: α : Type u
h : #α = ℵ₀
⊢ Nonempty (Denumerable α)

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
Nat.one_le_iff_ne_zero

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

Goal state before:
pp: n : ℕ
hn : n ≠ 0
⊢ 1 ≤ ↑n

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: c : Cardinal.{u_1}
n : ℕ
h : c ≤ ↑n
⊢ ∃ m ≤ n, c = ↑m

Tactic:
by

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

Goal state before:
pp: α : Type u
n : ℕ
⊢ #(Fin n → α) = #α ^ n

Tactic:
by

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

Goal state before:
pp: α : Type u
⊢ #((n : ℕ) × List.Vector α n) = sum fun n ↦ #α ^ n

Tactic:
by

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

Goal state before:
pp: ⊢ (sum fun n ↦ 0 ^ n) = 1

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α : Type u
s : Set α
⊢ #↑s ≠ 0 ↔ s.Nonempty

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α β γ : Type u
f : α → β → γ
s : Set α
t : Set β
⊢ #↑(image2 f s t) ≤ #↑s * #↑t

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α β : Type u
f : α ↪ β
s : Set α
⊢ #↑(⇑f '' s) = #↑s

Tactic:
by

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

Goal state before:
pp: α : Type u
ι : Type v
f : ι → Set α
⊢ lift.{v, u} #↑(⋃ i, f i) ≤ lift.{u, v} #ι * ⨆ i, lift.{v, u} #↑(f i)

Tactic:
by

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

Goal state before:
pp: α : Type u
A : Set (Set α)
⊢ #↑(⋃₀ A) ≤ #↑A * ⨆ s, #↑↑s

Tactic:
by

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

Goal state before:
pp: ι α : Type u
A : ι → Set α
s : Set ι
⊢ #↑(⋃ x ∈ s, A x) ≤ #↑s * ⨆ x, #↑(A ↑x)

Tactic:
by

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

Goal state before:
pp: α : Type u
ι : Type v
A : ι → Set α
s : Set ι
⊢ lift.{v, u} #↑(⋃ x ∈ s, A x) ≤ lift.{u, v} #↑s * ⨆ x, lift.{v, u} #↑(A ↑x)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
s : Set α
n : ℕ
⊢ #↑s = ↑n ↔ ∃ t, ↑t = s ∧ t.card = n

Tactic:
by

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

Goal state before:
pp: α : Type u
n : ℕ
⊢ #α = ↑n ↔ ∃ t, ↑t = univ ∧ t.card = n

Tactic:
by

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

Goal state before:
pp: α : Type u
n : ℕ
⊢ #α = ↑n ↔ ∃ h, Fintype.card α = n

Tactic:
by

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

Goal state before:
pp: α : Type u
s : Set α
⊢ #↑s = 1 ↔ ∃ x, s = {x}

Tactic:
by

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

Goal state before:
pp: α : Type u
S T : Set α
⊢ #↑(S ∪ T) + #↑(S ∩ T) = #↑S + #↑T

Tactic:
by

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

Goal state before:
pp: α : Type u
S T : Set α
H : Disjoint S T
⊢ #↑(S ∪ T) = #↑S + #↑T

Tactic:
by

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

Goal state before:
pp: α : Type u
s : Set α
a : α
h : a ∉ s
⊢ #↑(insert a s) = #↑s + 1

Tactic:
by

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

Goal state before:
pp: α : Type u
s : Set α
a : α
⊢ #↑(insert a s) ≤ #↑s + 1

Tactic:
by

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

Goal state before:
pp: α : Type u_1
s : Set α
⊢ #↑s + #↑sᶜ = #α

Tactic:
by

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

Goal state before:
pp: α : Type u
n : ℕ
t : Set α
H : #↑t ≤ ↑n
s : Finset α
hs : ↑s ⊆ t
⊢ s.card ≤ n

Tactic:
by

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

Goal state before:
pp: α : Type u
n : ℕ
t : Set α
⊢ #↑t ≤ ↑n ↔ ∀ (s : Finset α), ↑s ⊆ t → s.card ≤ n

Tactic:
by

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

Goal state before:
pp: α : Type u
A B : Set α
hfin : B.Finite
hlt : A ⊂ B
⊢ #↑A < #↑B

Tactic:
by

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

Goal state before:
pp: α : Type u
A B : Set α
hfin : A.Finite
hlt : A ⊂ B
⊢ #↑A < #↑B

Tactic:
by

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

Goal state before:
pp: α : Type u
S T : Set α
h : T ⊆ S
⊢ #↑(S \ T ∪ T) = #↑S

Tactic:
by

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

Goal state before:
pp: α : Type u
S T : Set α
h : T ⊆ S
⊢ #↑(S \ T) + #↑T = #↑S

Tactic:
by

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

Goal state before:
pp: α : Type u
S T : Set α
h : #↑S < #↑T
h' : #↑(T \ S) = 0
⊢ #↑(T \ S) + #↑S ≤ #↑S

Tactic:
by

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

Goal state before:
pp: α : Type u
S T : Set α
h : #↑S < #↑T
⊢ (T \ S).Nonempty

Tactic:
by

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

Goal state before:
pp: α : Type u
S : Set α
h : #↑S < #α
⊢ Sᶜ.Nonempty

Tactic:
by

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

Goal state before:
pp: α : Type u_1
P Q : Set α
⊢ #↑(P ∪ Q) ≤ ℵ₀ ↔ #↑P ≤ ℵ₀ ∧ #↑Q ≤ ℵ₀

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
f : α → β
s : Set β
h : Injective f
⊢ lift.{v, u} #↑(f ⁻¹' s) ≤ lift.{u, v} #↑s

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
f : α → β
s : Set β
h : s ⊆ range f
⊢ lift.{u, v} #↑s ≤ lift.{v, u} #↑(f ⁻¹' s)

Tactic:
by

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

Goal state before:
pp: α β : Type u
f : α → β
s : Set β
h : Injective f
h2 : s ⊆ range f
⊢ #↑(f ⁻¹' s) = #↑s

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
f : α ≃ β
s : Set β
⊢ lift.{v, u} #↑(⇑f ⁻¹' s) = lift.{u, v} #↑s

Tactic:
by

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

Goal state before:
pp: α β : Type u
f : α ≃ β
s : Set β
⊢ #↑(⇑f ⁻¹' s) = #↑s

Tactic:
by

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

Goal state before:
pp: α β : Type u
f : α → β
s : Set β
h : Injective f
⊢ #↑(f ⁻¹' s) ≤ #↑s

Tactic:
by

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

Goal state before:
pp: α β : Type u
f : α → β
s : Set β
h : s ⊆ range f
⊢ #↑s ≤ #↑(f ⁻¹' s)

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
f : α → β
s : Set α
t : Set β
h : t ⊆ f '' s
⊢ lift.{u, v} #↑t ≤ lift.{v, u} #↑{x | x ∈ s ∧ f x ∈ t}

Tactic:
by

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

Goal state before:
pp: α β : Type u
f : α → β
s : Set α
t : Set β
h : t ⊆ f '' s
⊢ #↑t ≤ #↑{x | x ∈ s ∧ f x ∈ t}

Tactic:
by

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

Goal state before:
pp: c : Cardinal.{u}
α : Type u
s : Set α
⊢ c ≤ #↑s ↔ ∃ p ⊆ s, #↑p = c

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
⊢ #↑(range Sum.inl) = lift.{v, u} #α

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
⊢ #↑(range Sum.inr) = lift.{u, v} #β

Tactic:
by

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

Goal state before:
pp: α : Type u
⊢ 2 ≤ #α ↔ ∃ x y, x ≠ y

Tactic:
by

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

Goal state before:
pp: α : Type u
x : α
⊢ 2 ≤ #α ↔ ∃ y, y ≠ x

Tactic:
by

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

Goal state before:
pp: α : Type u
x y : α
hne : x ≠ y
ht : ↑{x, y} = univ
⊢ {x, y} = univ

Tactic:
by

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

Goal state before:
pp: α : Type u
x y : α
hne : x ≠ y
h : {x, y} = univ
⊢ ↑{x, y} = univ

Tactic:
by

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

Goal state before:
pp: α : Type u
⊢ #α = 2 ↔ ∃ x y, x ≠ y ∧ {x, y} = univ

Tactic:
by

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

Goal state before:
pp: α : Type u
x : α
⊢ #α = 2 ↔ ∃! y, y ≠ x

Tactic:
mk_eq_two_iff

Goal state after:
α : Type u
x : α
⊢ (∃ x y, x ≠ y ∧ {x, y} = univ) ↔ ∃! y, y ≠ x
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: α : Type u
x : α
⊢ #α = 2 ↔ ∃! y, y ≠ x

Tactic:
by

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

Goal state before:
pp: α : Type u_1
l : List α
h : ↑l.length < #α
⊢ ∃ z, z ∉ l

Tactic:
by

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

Goal state before:
pp: α : Type u_1
h : 3 ≤ #α
x y : α
⊢ ↑3 ≤ #α

Tactic:
by

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

Goal state before:
pp: α : Type u_1
h : 3 ≤ #α
x y : α
this : ↑3 ≤ #α
⊢ ↑2 < #α

Tactic:
by

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

Goal state before:
pp: α : Type u_1
h : 3 ≤ #α
x y : α
⊢ ∃ z, z ≠ x ∧ z ≠ y

Tactic:
by

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

Goal state before:
pp: b c a : Cardinal.{u}
h : c < b
⊢ a ^ c ≤ a ^< b

Tactic:
by

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

Goal state before:
pp: a b c : Cardinal.{u}
⊢ a ^< b ≤ c ↔ ∀ x < b, a ^ x ≤ c

Tactic:
by

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

Goal state before:
pp: R : Type u
S : Type v
A : Type w
B : Type u_1
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Module R A
h₁ : ∀ (r : R) (x : A), r • 1 * x = r • x
h₂ : ∀ (r : R) (x : A), x * r • 1 = r • x
r₁ r₂ : R
⊢ (r₁ * r₂) • 1 = r₁ • 1 * r₂ • 1

Tactic:
by

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

Goal state before:
pp: R : Type u
S : Type v
A : Type w
B : Type u_1
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Module R A
h₁ : ∀ (r : R) (x : A), r • 1 * x = r • x
h₂ : ∀ (r : R) (x : A), x * r • 1 = r • x
r₁ r₂ : R
⊢ (r₁ * r₂) • 1 = r₁ • 1 * r₂ • 1

Tactic:
by simp only [h₁, mul_smul]

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

Goal state before:
pp: a : Cardinal.{u_1}
h : a ≠ 0
⊢ 0 ^< a = 1

Tactic:
by

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

Goal state before:
pp: a : Cardinal.{u_1}
⊢ a ^< 0 = 0

Tactic:
by

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

Goal state before:
pp: R : Type u
S : Type v
A : Type w
B : Type u_1
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Module R A
h₁ : ∀ (r : R) (x : A), r • 1 * x = r • x
h₂ : ∀ (r : R) (x : A), x * r • 1 = r • x
r : R
x : A
⊢ { toFun := fun r ↦ r • 1, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ } r * x =
    x * { toFun := fun r ↦ r • 1, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ } r

Tactic:
by

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

Goal state before:
pp: R : Type u
S : Type v
A : Type w
B : Type u_1
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Module R A
h₁ : ∀ (r : R) (x : A), r • 1 * x = r • x
h₂ : ∀ (r : R) (x : A), x * r • 1 = r • x
r : R
x : A
⊢ r • x = { toFun := fun r ↦ r • 1, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ } r * x

Tactic:
by

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

Goal state before:
pp: R : Type u
S : Type v
A : Type w
B : Type u_1
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Module R A
h₁ : ∀ (r : R) (x y : A), r • x * y = r • (x * y)
h₂ : ∀ (r : R) (x y : A), x * r • y = r • (x * y)
r : R
x : A
⊢ r • 1 * x = r • x

Tactic:
by

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

Goal state before:
pp: R : Type u
S : Type v
A : Type w
B : Type u_1
inst✝² : CommSemiring R
inst✝¹ : Semiring A
inst✝ : Module R A
h₁ : ∀ (r : R) (x y : A), r • x * y = r • (x * y)
h₂ : ∀ (r : R) (x y : A), x * r • y = r • (x * y)
r : R
x : A
⊢ x * r • 1 = r • x

Tactic:
by

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

Goal state before:
pp: R : Type u_2
inst✝¹ : CommSemiring R
A : Type u_3
inst✝ : Semiring A
P Q : Algebra R A
h : algebraMap R A = algebraMap R A
⊢ (fun x1 x2 ↦ x1 • x2) = fun x1 x2 ↦ x1 • x2

Tactic:
by

Goal state after:
Module: Mathlib.Algebra.Group.Action.Prod

Goal state before:
pp: M : Type u_1
N : Type u_2
P : Type u_3
E : Type u_4
α : Type u_5
β : Type u_6
inst✝⁶ : SMul M α
inst✝⁵ : SMul M β
inst✝⁴ : SMul N α
inst✝³ : SMul N β
a : M
x : α × β
inst✝² : SMul M N
inst✝¹ : IsScalarTower M N α
inst✝ : IsScalarTower M N β
x✝² : M
x✝¹ : N
x✝ : α × β
⊢ (x✝² • x✝¹) • x✝ = x✝² • x✝¹ • x✝

Tactic:
by

Goal state after: