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

Goal state before:
pp: α : Type u_2
inst✝ : OmegaCompletePartialOrder α
β γ : Type v
c : Chain α
f : α →o Part β
g : α →o β → Part γ
⊢ ∀ (c_1 : Part γ), ωSup (c.map (f.partBind g)) ≤ c_1 ↔ ωSup (c.map f) >>= ωSup (c.map g) ≤ c_1

Tactic:
;

Goal state after:
α : Type u_2
inst✝ : OmegaCompletePartialOrder α
β γ : Type v
c : Chain α
f : α →o Part β
g : α →o β → Part γ
⊢ ∀ (c_1 : Part γ), ωSup (c.map (f.partBind g)) ≤ c_1 ↔ ωSup (c.map f) >>= ωSup (c.map g) ≤ c_1
Module: Mathlib.Order.BourbakiWitt

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : CompleteLattice β
s : Set (α → β)
hs : ∀ f ∈ s, ωScottContinuous f
⊢ ωScottContinuous (⨆ a ∈ s, a)

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : CompleteLattice β
s : Set (α → β)
hs : ∀ f ∈ s, ωScottContinuous f
⊢ ωScottContinuous (⨆ a ∈ s, a)
Module: Mathlib.SetTheory.Cardinal.SchroederBernstein

Goal state before:
pp: α : 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 β
s t : Set α
hst : s ⊆ t
⊢ (g '' (f '' s)ᶜ)ᶜ ⊆ (g '' (f '' t)ᶜ)ᶜ

Tactic:
;

Goal state after:
α : 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 β
s t : Set α
hst : s ⊆ t
⊢ (g '' (f '' s)ᶜ)ᶜ ⊆ (g '' (f '' t)ᶜ)ᶜ
Module: Mathlib.Order.BourbakiWitt

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : CompleteLattice β
⊢ ωScottContinuous (SupSet.sSup ∅)

Tactic:
;

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : OmegaCompletePartialOrder α
inst✝ : CompleteLattice β
⊢ ωScottContinuous (SupSet.sSup ∅)
Module: Mathlib.Order.OmegaCompletePartialOrder

Goal state before:
pp: α : Type u_2
inst✝ : OmegaCompletePartialOrder α
β γ : Type u_6
f : α → Part β
g : α → β → Part γ
hf : ωScottContinuous f
hg : ωScottContinuous g
c : Chain α
⊢ ωSup (c.map ({ toFun := f, monotone' := ⋯ }.partBind { toFun := g, monotone' := ⋯ })) =
    ωSup (c.map { toFun := fun x ↦ f x >>= g x, monotone' := ⋯ })

Tactic:
;

Goal state after:
α : Type u_2
inst✝ : OmegaCompletePartialOrder α
β γ : Type u_6
f : α → Part β
g : α → β → Part γ
hf : ωScottContinuous f
hg : ωScottContinuous g
c : Chain α
⊢ ωSup (c.map ({ toFun := f, monotone' := ⋯ }.partBind { toFun := g, monotone' := ⋯ })) =
    ωSup (c.map { toFun := fun x ↦ f x >>= g x, monotone' := ⋯ })
Module: Mathlib.Order.OmegaCompletePartialOrder

Goal state before:
pp: ι : Sort u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝³ : OmegaCompletePartialOrder α
inst✝² : OmegaCompletePartialOrder β
inst✝¹ : OmegaCompletePartialOrder γ
inst✝ : OmegaCompletePartialOrder δ
f : α → β
g : α →𝒄 β
h : f = ⇑g
⊢ ∀ (c : Chain α), g.toFun (ωSup c) = ωSup (c.map g.toOrderHom)

Tactic:
;

Goal state after:
ι : Sort u_1
α : Type u_2
β : Type u_3
γ : Type u_4
δ : Type u_5
inst✝³ : OmegaCompletePartialOrder α
inst✝² : OmegaCompletePartialOrder β
inst✝¹ : OmegaCompletePartialOrder γ
inst✝ : OmegaCompletePartialOrder δ
f : α → β
g : α →𝒄 β
h : f = ⇑g
⊢ ∀ (c : Chain α), g.toFun (ωSup c) = ωSup (c.map g.toOrderHom)
Module: Mathlib.SetTheory.Cardinal.Order

Goal state before:
pp: α β : Type u
n : ℕ
c : Cardinal.{u}
⊢ c ^ ↑(n + 1) = c ^ ↑n * c

Tactic:
;

Goal state after:
α β : Type u
n : ℕ
c : Cardinal.{u}
⊢ c ^ ↑(n + 1) = c ^ ↑n * c
Module: Mathlib.SetTheory.Cardinal.Order

Goal state before:
pp: case mk
α✝ β : Type u
a✝ : Cardinal.{u}
α : Type u
⊢ 0 ≤ Quot.mk (⇑isEquivalent) α

Tactic:
;

Goal state after:
case mk
α✝ β : Type u
a✝ : Cardinal.{u}
α : Type u
⊢ 0 ≤ Quot.mk (⇑isEquivalent) α
Module: Mathlib.SetTheory.Cardinal.Order

Goal state before:
pp: case mk.mk.mk.mk
a✝ : Cardinal.{u_1}
α : Type u_1
b✝ : Cardinal.{u_1}
β : Type u_1
c✝ : Cardinal.{u_1}
γ : Type u_1
d✝ : Cardinal.{u_1}
δ : Type u_1
e₁ : α ↪ β
e₂ : γ ↪ δ
⊢ Quot.mk (⇑isEquivalent) α + Quot.mk (⇑isEquivalent) γ ≤ Quot.mk (⇑isEquivalent) β + Quot.mk (⇑isEquivalent) δ

Tactic:
;

Goal state after:
case mk.mk.mk.mk
a✝ : Cardinal.{u_1}
α : Type u_1
b✝ : Cardinal.{u_1}
β : Type u_1
c✝ : Cardinal.{u_1}
γ : Type u_1
d✝ : Cardinal.{u_1}
δ : Type u_1
e₁ : α ↪ β
e₂ : γ ↪ δ
⊢ Quot.mk (⇑isEquivalent) α + Quot.mk (⇑isEquivalent) γ ≤ Quot.mk (⇑isEquivalent) β + Quot.mk (⇑isEquivalent) δ
Module: Mathlib.SetTheory.Cardinal.Order

Goal state before:
pp: ι : Type u_1
f g : ι → Cardinal.{u_2}
H : ∀ (i : ι), f i ≤ g i
i : ι
this : f i ≤ g i
⊢ Nonempty (Quotient.out (f i) ↪ Quotient.out (g ((Embedding.refl ι) i)))

Tactic:
;

Goal state after:
ι : Type u_1
f g : ι → Cardinal.{u_2}
H : ∀ (i : ι), f i ≤ g i
i : ι
this : f i ≤ g i
⊢ Nonempty (Quotient.out (f i) ↪ Quotient.out (g ((Embedding.refl ι) i)))
Module: Mathlib.SetTheory.Cardinal.Order

Goal state before:
pp: α : Type u
x✝ : Nonempty (Cardinal.{u} ↪ α)
f : Cardinal.{u} → α
hf : Injective f
g : α → Cardinal.{u} := invFun f
x : α
hx : g x = 2 ^ Cardinal.sum g
this : g x ≤ Cardinal.sum g
⊢ Cardinal.sum g < 2 ^ Cardinal.sum g

Tactic:
;

Goal state after:
α : Type u
x✝ : Nonempty (Cardinal.{u} ↪ α)
f : Cardinal.{u} → α
hf : Injective f
g : α → Cardinal.{u} := invFun f
x : α
hx : g x = 2 ^ Cardinal.sum g
this : g x ≤ Cardinal.sum g
⊢ Cardinal.sum g < 2 ^ Cardinal.sum g
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

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

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

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.Order

Goal state before:
pp: ι : Type u_1
f g : ι → Cardinal.{u_2}
H : ∀ (i : ι), f i ≤ g i
i : ι
this : f i ≤ g i
⊢ Nonempty (Quotient.out (f i) ↪ Quotient.out (g i))

Tactic:
;

Goal state after:
ι : Type u_1
f g : ι → Cardinal.{u_2}
H : ∀ (i : ι), f i ≤ g i
i : ι
this : f i ≤ g i
⊢ Nonempty (Quotient.out (f i) ↪ Quotient.out (g i))
Module: Mathlib.SetTheory.Cardinal.ToNat

Goal state before:
pp: c : Cardinal.{u_1}
h : ↑(toNat c) = c
⊢ ↑(toNat c) < ℵ₀

Tactic:
;

Goal state after:
c : Cardinal.{u_1}
h : ↑(toNat c) = c
⊢ ↑(toNat c) < ℵ₀
Module: Mathlib.SetTheory.Cardinal.ToNat

Goal state before:
pp: c : Cardinal.{u}
n : ℕ
hn : n ≠ 0
⊢ toENat c = ↑n ↔ c = ↑n

Tactic:
toENat_eq_natCast

Goal state after:
c : Cardinal.{u}
n : ℕ
hn : n ≠ 0
⊢ c = ↑n ↔ c = ↑n
Module: Mathlib.SetTheory.Cardinal.ENat

Goal state before:
pp: m : ℕ∞
⊢ 0 = m ↔ m = 0

Tactic:
;

Goal state after:
m : ℕ∞
⊢ 0 = m ↔ m = 0
Module: Mathlib.SetTheory.Cardinal.ENat

Goal state before:
pp: m : ℕ∞
⊢ 1 = m ↔ m = 1

Tactic:
;

Goal state after:
m : ℕ∞
⊢ 1 = m ↔ m = 1
Module: Mathlib.SetTheory.Cardinal.ENat

Goal state before:
pp: ⊢ range ofENat = Iic ℵ₀

Tactic:
refine (range_subset_iff.2 ofENat_le_aleph0).antisymm fun x (hx : x ≤ ℵ₀) ↦ ?_

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

Goal state before:
pp: case inl
n : ℕ∞
x : ℕ
⊢ ↑n ≤ ↑x ↔ n ≤ (↑x).toENatAux

Tactic:
;

Goal state after:
case inl
n : ℕ∞
x : ℕ
⊢ ↑n ≤ ↑x ↔ n ≤ (↑x).toENatAux
Module: Mathlib.SetTheory.Cardinal.ENat

Goal state before:
pp: case inl
n x : ℕ
⊢ (↑x).toENatAux ≤ ↑n ↔ ↑x ≤ ↑n

Tactic:
;

Goal state after:
case inl
n x : ℕ
⊢ (↑x).toENatAux ≤ ↑n ↔ ↑x ≤ ↑n
Module: Mathlib.SetTheory.Cardinal.ENat

Goal state before:
pp: x : Cardinal.{u_1}
n : ℕ
⊢ x.toENatAux ≤ ↑n ↔ x ≤ ↑n

Tactic:
by
  cases lt_or_ge x ℵ₀ with
  | inl hx => lift x to ℕ using hx; simp
  | inr hx => simp [toENatAux_eq_top hx, natCast_lt_aleph0.trans_le hx]

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 * 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

x y : Cardinal.{u}
hle : x ≤ y
⊢ (x * y).toENatAux = x.toENatAux * y.toENatAux
Module: Mathlib.SetTheory.Cardinal.ENat

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

Tactic:
;

Goal state after:
case inl
y : Cardinal.{u}
hy : y < ℵ₀
x : ℕ
hle : ↑x ≤ y
⊢ (↑x * y).toENatAux = (↑x).toENatAux * y.toENatAux
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

x y : Cardinal.{u}
hle : x ≤ y
⊢ (x + y).toENatAux = x.toENatAux + y.toENatAux
Module: Mathlib.SetTheory.Cardinal.ENat

Goal state before:
pp: case inl
y : Cardinal.{u}
hy : y < ℵ₀
x : ℕ
hle : ↑x ≤ y
⊢ (↑x + y).toENatAux = (↑x).toENatAux + y.toENatAux

Tactic:
;

Goal state after:
case inl
y : Cardinal.{u}
hy : y < ℵ₀
x : ℕ
hle : ↑x ≤ y
⊢ (↑x + y).toENatAux = (↑x).toENatAux + y.toENatAux
Module: Mathlib.SetTheory.Cardinal.ENat

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

Tactic:
;

Goal state after:
c' : Cardinal.{u}
c : ℕ∞
⊢ toENat ↑c ≤ toENat c' ↔ ↑c ≤ c'
Module: Mathlib.SetTheory.Cardinal.ENat

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

Tactic:
;

Goal state after:
c : Cardinal.{u}
c' : ℕ
⊢ toENat c ≤ toENat ↑c' ↔ c ≤ ↑c'
Module: Mathlib.SetTheory.Cardinal.ENat

Goal state before:
pp: case inl
c : ℕ∞
⊢ toENat (lift.{v, u} ↑c) = toENat ↑c

Tactic:
;

Goal state after:
case inl
c : ℕ∞
⊢ toENat (lift.{v, u} ↑c) = toENat ↑c
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 →* M
h : _root_.CompTriple.IsId ⇑σ
x✝ : M
⊢ σ x✝ = (id M) x✝

Tactic:
;

Goal state after:
M : Type u_1
N : Type u_2
P : Type u_3
inst✝² : Monoid M
inst✝¹ : Monoid N
inst✝ : Monoid P
σ : M →* M
h : _root_.CompTriple.IsId ⇑σ
x✝ : M
⊢ σ x✝ = (id M) x✝
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₃
σ : R₁ →+* R₂
σ' : R₂ →+* R₁
inst✝¹ : RingHomInvPair σ σ'
σ₂₁ : R₂ →+* R₁
inst✝ : RingHomInvPair σ₁₂ σ₂₁
⊢ σ₁₂.comp σ₂₁ = RingHom.id R₂

Tactic:
by simp only [comp_eq₂]

Goal state after:
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: 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 • a = 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 • a = 0 • b
Module: Mathlib.SetTheory.Cardinal.Basic

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

Tactic:
convert! natCast_add_one_le_iff

Goal state after:
case e'_1.e'_3
c : Cardinal.{u_1}
⊢ 2 = ↑1 + 1
Module: Mathlib.SetTheory.Cardinal.Basic

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

Tactic:
exact ⟨⟨(↑), fun a b => Fin.ext⟩⟩

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: 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
f : α → β → γ
s : Set α
t : Set β
⊢ #↑(image2 f s t) ≤ #↑s * #↑t

Tactic:
← image_uncurry_prod,

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: case inj'
α : Type u
β : Type v
f : α → β
s : Set β
h : Injective f
⊢ Injective fun x ↦ f ↑x

Tactic:
;

Goal state after:
case inj'
α : Type u
β : Type v
f : α → β
s : Set β
h : Injective f
⊢ Injective fun x ↦ f ↑x
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: c : Cardinal.{u}
α : Type u
s : Set α
⊢ ∀ (a : Set ↑s), #↑a = c ↔ #↑(Subtype.val '' a) = c

Tactic:
;

Goal state after:
c : Cardinal.{u}
α : Type u
s : Set α
⊢ ∀ (a : Set ↑s), #↑a = c ↔ #↑(Subtype.val '' a) = c
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: c : Cardinal.{u}
α : Type u
s : Set α
t : Set ↑s
⊢ #↑t = c ↔ #↑(Subtype.val '' t) = c

Tactic:
;

Goal state after:
c : Cardinal.{u}
α : Type u
s : Set α
t : Set ↑s
⊢ #↑t = c ↔ #↑(Subtype.val '' t) = c
Module: Mathlib.SetTheory.Cardinal.Basic

Goal state before:
pp: c : Cardinal.{u}
α : Type u
s : Set α
t : Set ↑s
⊢ Injective Subtype.val

Tactic:
;

Goal state after:
c : Cardinal.{u}
α : Type u
s : Set α
t : Set ↑s
⊢ Injective Subtype.val
Module: Mathlib.SetTheory.Cardinal.Basic

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

Tactic:
;

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: b c a : Cardinal.{u}
h : c < b
⊢ a ^ c ≤ a ^< b

Tactic:
refine le_ciSup (f := fun y : Iio b => a ^ (y : Cardinal)) ?_ ⟨c, h⟩
  rw [← image_eq_range]
  exact bddAbove_image.{u, u} _ bddAbove_Iio

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✝¹ : Monoid M
inst✝ : Monoid N
toSemigroupAction✝ : SemigroupAction (M × N) α
one_smul✝ : ∀ (b : α), 1 • b = b
⊢ (fun _insts ↦
        have this := ⋯;
        prodOfSMulCommClass M N α)
      ((fun x ↦ ⟨compHom α (MonoidHom.inl M N), ⟨compHom α (MonoidHom.inr M N), ⋯⟩⟩)
        { toSemigroupAction := toSemigroupAction✝, one_smul := one_smul✝ }) =
    { toSemigroupAction := toSemigroupAction✝, one_smul := one_smul✝ }

Tactic:
;

Goal state after:
M : Type u_1
N : Type u_2
P : Type u_3
E : Type u_4
α : Type u_5
β : Type u_6
inst✝¹ : Monoid M
inst✝ : Monoid N
toSemigroupAction✝ : SemigroupAction (M × N) α
one_smul✝ : ∀ (b : α), 1 • b = b
⊢ (fun _insts ↦
        have this := ⋯;
        prodOfSMulCommClass M N α)
      ((fun x ↦ ⟨compHom α (MonoidHom.inl M N), ⟨compHom α (MonoidHom.inr M N), ⋯⟩⟩)
        { toSemigroupAction := toSemigroupAction✝, one_smul := one_smul✝ }) =
    { toSemigroupAction := toSemigroupAction✝, one_smul := one_smul✝ }
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✝¹ : Monoid M
inst✝ : Monoid N
toSemigroupAction✝ : SemigroupAction (M × N) α
one_smul✝ : ∀ (b : α), 1 • b = b
⊢ prodOfSMulCommClass M N α = { toSemigroupAction := toSemigroupAction✝, one_smul := one_smul✝ }

Tactic:
;

Goal state after:
M : Type u_1
N : Type u_2
P : Type u_3
E : Type u_4
α : Type u_5
β : Type u_6
inst✝¹ : Monoid M
inst✝ : Monoid N
toSemigroupAction✝ : SemigroupAction (M × N) α
one_smul✝ : ∀ (b : α), 1 • b = b
⊢ prodOfSMulCommClass M N α = { toSemigroupAction := toSemigroupAction✝, one_smul := one_smul✝ }
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✝¹ : Monoid M
inst✝ : Monoid N
toSemigroupAction✝ : SemigroupAction (M × N) α
one_smul✝ : ∀ (b : α), 1 • b = b
m : M
n : N
a : α
⊢ (m, 1) • (1, n) • a = SMul.smul (m, n) a

Tactic:
← mul_smul,

Goal state after:
M : Type u_1
N : Type u_2
P : Type u_3
E : Type u_4
α : Type u_5
β : Type u_6
inst✝¹ : Monoid M
inst✝ : Monoid N
toSemigroupAction✝ : SemigroupAction (M × N) α
one_smul✝ : ∀ (b : α), 1 • b = b
m : M
n : N
a : α
⊢ ((m, 1) * (1, n)) • a = SMul.smul (m, n) a
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✝¹ : Monoid M
inst✝ : Monoid N
toSemigroupAction✝ : SemigroupAction (M × N) α
one_smul✝ : ∀ (b : α), 1 • b = b
m : M
n : N
a : α
⊢ (m, n) • a = SMul.smul (m, n) a

Tactic:
;

Goal state after:
M : Type u_1
N : Type u_2
P : Type u_3
E : Type u_4
α : Type u_5
β : Type u_6
inst✝¹ : Monoid M
inst✝ : Monoid N
toSemigroupAction✝ : SemigroupAction (M × N) α
one_smul✝ : ∀ (b : α), 1 • b = b
m : M
n : N
a : α
⊢ (m, n) • a = SMul.smul (m, n) a
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✝¹ : Monoid M
inst✝ : Monoid N
hM : MulAction M α
hN : MulAction N α
snd✝ : SMulCommClass M N α
⊢ ⟨compHom α (MonoidHom.inl M N), ⟨compHom α (MonoidHom.inr M N), ⋯⟩⟩ = ⟨hM, ⟨hN, snd✝⟩⟩

Tactic:
;

Goal state after:
M : Type u_1
N : Type u_2
P : Type u_3
E : Type u_4
α : Type u_5
β : Type u_6
inst✝¹ : Monoid M
inst✝ : Monoid N
hM : MulAction M α
hN : MulAction N α
snd✝ : SMulCommClass M N α
⊢ ⟨compHom α (MonoidHom.inl M N), ⟨compHom α (MonoidHom.inr M N), ⋯⟩⟩ = ⟨hM, ⟨hN, snd✝⟩⟩
Module: Mathlib.Algebra.Group.Action.Prod

Goal state before:
pp: case e_3
M : Type u_1
N : Type u_2
P : Type u_3
E : Type u_4
α : Type u_5
β : Type u_6
inst✝¹ : Monoid M
inst✝ : Monoid N
hM : MulAction M α
hN : MulAction N α
snd✝ : SMulCommClass M N α
m : M
a : α
⊢ SMul.smul m a = SMul.smul m a

Tactic:
;

Goal state after:
case e_3
M : Type u_1
N : Type u_2
P : Type u_3
E : Type u_4
α : Type u_5
β : Type u_6
inst✝¹ : Monoid M
inst✝ : Monoid N
hM : MulAction M α
hN : MulAction N α
snd✝ : SMulCommClass M N α
m : M
a : α
⊢ SMul.smul m a = SMul.smul m a
Module: Mathlib.Algebra.Group.Action.Prod

Goal state before:
pp: case e_3
M : Type u_1
N : Type u_2
P : Type u_3
E : Type u_4
α : Type u_5
β : Type u_6
inst✝¹ : Monoid M
inst✝ : Monoid N
hM : MulAction M α
hN : MulAction N α
snd✝ : SMulCommClass M N α
m : M
a : α
⊢ SMul.smul m a = SMul.smul m (1 • a)

Tactic:
;

Goal state after:
case e_3
M : Type u_1
N : Type u_2
P : Type u_3
E : Type u_4
α : Type u_5
β : Type u_6
inst✝¹ : Monoid M
inst✝ : Monoid N
hM : MulAction M α
hN : MulAction N α
snd✝ : SMulCommClass M N α
m : M
a : α
⊢ SMul.smul m a = SMul.smul m (1 • a)
Module: Mathlib.Algebra.Group.Action.Prod

Goal state before:
pp: case e_4.e_2
M : Type u_1
N : Type u_2
P : Type u_3
E : Type u_4
α : Type u_5
β : Type u_6
inst✝¹ : Monoid M
inst✝ : Monoid N
hM : MulAction M α
hN : MulAction N α
snd✝ : SMulCommClass M N α
x✝ : MulAction N α
⊢ SMulCommClass M N α = SMulCommClass M N α

Tactic:
;

Goal state after:
case e_4.e_2
M : Type u_1
N : Type u_2
P : Type u_3
E : Type u_4
α : Type u_5
β : Type u_6
inst✝¹ : Monoid M
inst✝ : Monoid N
hM : MulAction M α
hN : MulAction N α
snd✝ : SMulCommClass M N α
x✝ : MulAction N α
⊢ SMulCommClass M N α = SMulCommClass M N α
Module: Mathlib.Algebra.Group.Action.Prod

Goal state before:
pp: case e_4.e_2.e_4.e_4.e_4
M : Type u_1
N : Type u_2
P : Type u_3
E : Type u_4
α : Type u_5
β : Type u_6
inst✝¹ : Monoid M
inst✝ : Monoid N
hM : MulAction M α
hN : MulAction N α
snd✝ : SMulCommClass M N α
x✝ : MulAction N α
⊢ compHom α (MonoidHom.inl M N) = hM

Tactic:
;

Goal state after:
case e_4.e_2.e_4.e_4.e_4
M : Type u_1
N : Type u_2
P : Type u_3
E : Type u_4
α : Type u_5
β : Type u_6
inst✝¹ : Monoid M
inst✝ : Monoid N
hM : MulAction M α
hN : MulAction N α
snd✝ : SMulCommClass M N α
x✝ : MulAction N α
⊢ compHom α (MonoidHom.inl M N) = hM
Module: Mathlib.Algebra.Group.Action.Prod

Goal state before:
pp: case e_4.e_2.e_4.e_4.e_4
M : Type u_1
N : Type u_2
P : Type u_3
E : Type u_4
α : Type u_5
β : Type u_6
inst✝¹ : Monoid M
inst✝ : Monoid N
hM : MulAction M α
hN : MulAction N α
snd✝ : SMulCommClass M N α
x✝ : MulAction N α
m : M
a : α
⊢ SMul.smul m a = SMul.smul m a

Tactic:
;

Goal state after:
case e_4.e_2.e_4.e_4.e_4
M : Type u_1
N : Type u_2
P : Type u_3
E : Type u_4
α : Type u_5
β : Type u_6
inst✝¹ : Monoid M
inst✝ : Monoid N
hM : MulAction M α
hN : MulAction N α
snd✝ : SMulCommClass M N α
x✝ : MulAction N α
m : M
a : α
⊢ SMul.smul m a = SMul.smul m a