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

Goal state before:
pp: ι : 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 : (i : ι) → β i
hx : x ∈ insert f s
y : (i : ι) → β i
hy : y ∈ insert f s
⊢ (fun x ↦ x i) x = (fun x ↦ x i) y → x = y

Tactic:
by

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

Goal state before:
pp: c : Cardinal.{u}
⊢ ℵ₀ ≤ lift.{v, u} c ↔ ℵ₀ ≤ c

Tactic:
by

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

Goal state before:
pp: c : Cardinal.{u}
⊢ lift.{v, u} c ≤ ℵ₀ ↔ c ≤ ℵ₀

Tactic:
by

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

Goal state before:
pp: c : Cardinal.{u}
⊢ ℵ₀ < lift.{v, u} c ↔ ℵ₀ < c

Tactic:
by

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

Goal state before:
pp: c : Cardinal.{u}
⊢ lift.{v, u} c < ℵ₀ ↔ c < ℵ₀

Tactic:
by

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

Goal state before:
pp: c : Cardinal.{u}
⊢ ℵ₀ = lift.{v, u} c ↔ ℵ₀ = c

Tactic:
by

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

Goal state before:
pp: c : Cardinal.{u}
⊢ lift.{v, u} c = ℵ₀ ↔ c = ℵ₀

Tactic:
by

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

Goal state before:
pp: n : ℕ
⊢ #(Fin n) = ↑n

Tactic:
by

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

Goal state before:
pp: c : Cardinal.{u}
⊢ toNat c = 0 ↔ c = 0 ∨ ℵ₀ ≤ c

Tactic:
by

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

Goal state before:
pp: c : Cardinal.{u}
⊢ toNat c ≠ 0 ↔ c ≠ 0 ∧ c < ℵ₀

Tactic:
by

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

Goal state before:
pp: n : ℕ
⊢ lift.{u, v} ↑n = ↑n

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: n : ℕ
a : Cardinal.{u}
⊢ ↑n = lift.{v, u} a ↔ ↑n = a

Tactic:
by

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

Goal state before:
pp: a : Cardinal.{u}
⊢ 0 = lift.{v, u} a ↔ 0 = a

Tactic:
by

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

Goal state before:
pp: a : Cardinal.{u}
⊢ 1 = lift.{v, u} a ↔ 1 = a

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: a : Cardinal.{u}
n : ℕ
⊢ lift.{v, u} a ≤ ↑n ↔ a ≤ ↑n

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: a : Cardinal.{u}
⊢ lift.{v, u} a ≤ 1 ↔ a ≤ 1

Tactic:
by

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

Goal state before:
pp: n : ℕ
a : Cardinal.{u}
⊢ ↑n ≤ lift.{v, u} a ↔ ↑n ≤ a

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: a : Cardinal.{u}
⊢ 1 ≤ lift.{v, u} a ↔ 1 ≤ a

Tactic:
by

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

Goal state before:
pp: ⊢ StrictMonoOn (⇑toNat) (Iio ℵ₀)

Tactic:
by

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

Goal state before:
pp: α : Type u
h : Infinite α
⊢ toNat #α = 0

Tactic:
by

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

Goal state before:
pp: a : Cardinal.{u}
n : ℕ
⊢ lift.{v, u} a < ↑n ↔ a < ↑n

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝ : Fintype α
⊢ toNat #α = Fintype.card α

Tactic:
by

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

Goal state before:
pp: n : ℕ
a : Cardinal.{u}
⊢ ↑n < lift.{v, u} a ↔ ↑n < a

Tactic:
by

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

Goal state before:
pp: a : Cardinal.{u}
⊢ 0 < lift.{v, u} a ↔ 0 < a

Tactic:
by

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

Goal state before:
pp: a : Cardinal.{u}
⊢ 1 < lift.{v, u} a ↔ 1 < a

Tactic:
by

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

Goal state before:
pp: α : Type u
s : Finset α
⊢ #↥s = ↑s.card

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: α β : Type u
a b : ℕ
h : #(Fin a) = #(Fin b)
⊢ a = b

Tactic:
Cardinal.eq,

Goal state after:
α β : Type u
a b : ℕ
h : Nonempty (Fin a ≃ Fin b)
⊢ a = b
Module: Mathlib.SetTheory.Cardinal.ToNat

Goal state before:
pp: c : Cardinal.{u}
⊢ toNat c = 1 ↔ c = 1

Tactic:
by

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

Goal state before:
pp: α β : Type u
⊢ CharZero Cardinal.{u_1}

Tactic:
by

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

Goal state before:
pp: c : Cardinal.{v}
⊢ toNat (lift.{u, v} c) = toNat c

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: c d : Cardinal.{u}
hc : c < ℵ₀
hd : d < ℵ₀
⊢ toNat (c + d) = toNat c + toNat d

Tactic:
by

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

Goal state before:
pp: a : Cardinal.{u}
b : Cardinal.{v}
ha : a < ℵ₀
hb : b < ℵ₀
⊢ toNat (lift.{v, u} a + lift.{u, v} b) = toNat a + toNat b

Tactic:
by

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

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

Tactic:
simp [cast_toNat_of_lt_aleph0 h]

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

Goal state before:
pp: a : Cardinal.{u_1}
⊢ ↑(toNat a) ≤ a

Tactic:
by

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

Goal state before:
pp: a : Cardinal.{u}
n : ℕ
lt : a < ℵ₀
⊢ toNat a ≤ n ↔ a ≤ ↑n

Tactic:
by

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

Goal state before:
pp: a : Cardinal.{u}
n : ℕ
lt : a < ℵ₀
⊢ toNat a = n ↔ a = ↑n

Tactic:
by

Goal state after:
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:
apply eq_of_forall_le_iff

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

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

Tactic:
by

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

Goal state before:
pp: m : ℕ∞
n : ℕ
⊢ ↑m < ↑n ↔ m < ↑n

Tactic:
by

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

Goal state before:
pp: m : ℕ
n : ℕ∞
⊢ ↑m < ↑n ↔ ↑m < n

Tactic:
by

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

Goal state before:
pp: m : ℕ∞
⊢ 0 < ↑m ↔ 0 < m

Tactic:
by

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

Goal state before:
pp: m : ℕ∞
⊢ 1 < ↑m ↔ 1 < m

Tactic:
by

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

Goal state before:
pp: m : ℕ∞
n : ℕ
⊢ ↑m ≤ ↑n ↔ m ≤ ↑n

Tactic:
by

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

Goal state before:
pp: m : ℕ∞
⊢ ↑m ≤ 1 ↔ m ≤ 1

Tactic:
by

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

Goal state before:
pp: m : ℕ
n : ℕ∞
⊢ ↑m ≤ ↑n ↔ ↑m ≤ n

Tactic:
by

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

Goal state before:
pp: n : ℕ∞
⊢ 1 ≤ ↑n ↔ 1 ≤ n

Tactic:
by

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

Goal state before:
pp: m : ℕ∞
n : ℕ
⊢ ↑m = ↑n ↔ m = ↑n

Tactic:
by

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

Goal state before:
pp: m : ℕ
n : ℕ∞
⊢ ↑m = ↑n ↔ ↑m = n

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: x y : Cardinal.{u}
⊢ (x * y).toENatAux = x.toENatAux * y.toENatAux

Tactic:
by

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

Goal state before:
pp: x y : Cardinal.{u}
⊢ (x + y).toENatAux = x.toENatAux + y.toENatAux

Tactic:
by

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

Goal state before:
pp: ⊢ StrictMonoOn (⇑toENat) (Iic ℵ₀)

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: c c' : Cardinal.{u}
hc : c ≤ ℵ₀
⊢ toENat c ≤ toENat c' ↔ c ≤ c'

Tactic:
by

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

Goal state before:
pp: c c' : Cardinal.{u}
hc' : c' < ℵ₀
⊢ toENat c ≤ toENat c' ↔ c ≤ c'

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: c : Cardinal.{u}
⊢ toENat c < 1 ↔ c < 1

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: c : Cardinal.{u}
⊢ toENat c ≠ ⊤ ↔ c < ℵ₀

Tactic:
by

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

Goal state before:
pp: c : Cardinal.{u}
⊢ toENat c < ⊤ ↔ c < ℵ₀

Tactic:
by

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

Goal state before:
pp: c : Cardinal.{u}
⊢ toENat (lift.{v, u} c) = toENat c

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: m n : ℕ∞
⊢ ↑(m + n) = ↑m + ↑n

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: m n : ℕ∞
⊢ ↑(m * n) ∈ Iic ℵ₀

Tactic:
by

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

Goal state before:
pp: m n : ℕ∞
⊢ toENat ↑(m * n) = toENat (↑m * ↑n)

Tactic:
by

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
a b : R
x : M
⊢ (f a + f b) • x = f a • x + f b • x

Tactic:
by

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 • x = 0

Tactic:
by

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₁
⊢ σ' (σ x) = x

Tactic:
by

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 →* M
h : _root_.CompTriple.IsId ⇑σ
⊢ σ = id M

Tactic:
by

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✝
N : Type u_4
P : Type u_5
inst✝² : Monoid N
inst✝¹ : Monoid P
φ : N →* N
inst✝ : IsId φ
ψ : N →* P
⊢ ψ.comp φ = ψ

Tactic:
by

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 : Type u_4
N : Type u_5
inst✝² : Monoid M
inst✝¹ : Monoid N
φ : M →* N
ψ : N →* N
inst✝ : IsId ψ
⊢ ψ.comp φ = φ

Tactic:
by

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

Goal state before:
pp: M : Type u_1
N : Type u_2
inst✝² : Monoid M
inst✝¹ : Monoid N
φ : M →* N
ψ : N →* M
h : Function.RightInverse ⇑φ ⇑ψ
χ : M →* M
inst✝ : IsId χ
⊢ ψ.comp φ = χ

Tactic:
by

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
κ : φ.CompTriple ψ χ
⊢ ⇑ψ ∘ ⇑φ = ⇑χ

Tactic:
by

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

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
Q : Type u_4
inst✝ : Monoid Q
φ₁ : M →* N
φ₂ : N →* P
φ₁₂ : M →* P
κ : φ₁.CompTriple φ₂ φ₁₂
φ₃ : P →* Q
φ₂₃ : N →* Q
κ' : φ₂.CompTriple φ₃ φ₂₃
φ₁₂₃ : M →* Q
h : φ₂₃.comp φ₁ = φ₁₂₃
⊢ φ₃.comp φ₁₂ = φ₁₂₃

Tactic:
by

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₂
⊢ σ (σ' x) = x

Tactic:
by

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₃
σ : R₁ →+* R₂
σ' : R₂ →+* R₁
inst✝¹ : RingHomInvPair σ σ'
σ₂₁ : R₂ →+* R₁
inst✝ : RingHomInvPair σ₁₂ σ₂₁
⊢ σ₂₁.comp σ₁₂ = RingHom.id R₁

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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
Q : Type u_4
inst✝ : Monoid Q
φ₁ : M →* N
φ₂ : N →* P
φ₁₂ : M →* P
κ : φ₁.CompTriple φ₂ φ₁₂
φ₃ : P →* Q
φ₂₃ : N →* Q
κ' : φ₂.CompTriple φ₃ φ₂₃
φ₁₂₃ : M →* Q
h : φ₃.comp φ₁₂ = φ₁₂₃
⊢ φ₂₃.comp φ₁ = φ₁₂₃

Tactic:
by

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₃
σ : R₁ →+* R₂
σ' : R₂ →+* R₁
inst✝¹ : RingHomInvPair σ σ'
σ₂₁ : R₂ →+* R₁
inst✝ : RingHomInvPair σ₁₂ σ₂₁
⊢ σ₁₂.comp σ₂₁ = RingHom.id R₂

Tactic:
by

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₃
σ : R₁ →+* R₂
σ' : R₂ →+* R₁
⊢ σ₁₂.comp (RingHom.id R₁) = σ₁₂

Tactic:
by

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₃
σ : R₁ →+* R₂
σ' : R₂ →+* R₁
⊢ (RingHom.id R₂).comp σ₁₂ = σ₁₂

Tactic:
by

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
Q : Type u_4
inst✝ : Monoid Q
φ₁ : M →* N
φ₂ : N →* P
φ₁₂ : M →* P
κ : φ₁.CompTriple φ₂ φ₁₂
φ₃ : P →* Q
φ₂₃ : N →* Q
κ' : φ₂.CompTriple φ₃ φ₂₃
φ₁₂₃ : M →* Q
⊢ φ₁.CompTriple φ₂₃ φ₁₂₃ ↔ φ₁₂.CompTriple φ₃ φ₁₂₃

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Function.CompTypeclasses

Goal state before:
pp: N : Type u_1
P : Type u_2
φ : N → N
inst✝ : IsId φ
ψ : N → P
⊢ ψ ∘ φ = ψ

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Function.CompTypeclasses

Goal state before:
pp: M : Type u_1
N : Type u_2
φ : M → N
ψ : N → N
inst✝ : IsId ψ
⊢ ψ ∘ φ = φ

Tactic:
by

Goal state after:
Module: Mathlib.Logic.Function.CompTypeclasses

Goal state before:
pp: M : Type u_1
N : Type u_2
φ : M → N
ψ : N → M
h : Function.RightInverse φ ψ
χ : M → M
inst✝ : IsId χ
⊢ ψ ∘ φ = χ

Tactic:
by

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 σ₂₃
⊢ Function.Surjective ⇑σ₁₃

Tactic:
by

Goal state after:
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:
by

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

Goal state before:
pp: R : Type u_1
S : Type u_2
M : Type u_3
a : R
inst✝¹ : SMul R M
inst✝ : SMul S M
f : R → S
smul : ∀ (m : M), f a • m = a • m
⊢ IsSMulRegular M (f a) ↔ IsSMulRegular M a

Tactic:
by

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

Goal state before:
pp: M : Type u_3
inst✝ : SubtractionMonoid M
n : ℤ
⊢ IsSMulRegular M n.natAbs ↔ IsSMulRegular M n

Tactic:
by

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 : ((fun m ↦ a • m) ∘ fun x ↦ s • x) c = ((fun m ↦ a • m) ∘ fun x ↦ s • x) d
⊢ c = d

Tactic:
by

Goal state after:
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:
by

Goal state after:
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
⊢ IsSMulRegular M (a * b) ∧ IsSMulRegular M (b * a) ↔ IsSMulRegular M a ∧ IsSMulRegular M b

Tactic:
by

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 : (fun x ↦ 1 • x) a = (fun x ↦ 1 • x) b
⊢ a = b

Tactic:
by

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 (a * b)

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
n : ℕ
ra : IsSMulRegular M a
⊢ IsSMulRegular M (a ^ n)

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
n : ℕ
n0 : 0 < n
⊢ IsSMulRegular M (a ^ n) ↔ IsSMulRegular M a

Tactic:
by

Goal state after:
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 (a • s)

Tactic:
by

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

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

Tactic:
by

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
h : IsSMulRegular M 0
a b : M
⊢ (fun x ↦ 0 • x) a = (fun x ↦ 0 • x) b

Tactic:
by

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

Goal state before:
pp: α : Type u
⊢ 1 < #α ↔ Nontrivial α

Tactic:
by

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
⊢ ¬IsSMulRegular M 0 ↔ Nontrivial M

Tactic:
by

Goal state after:
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 (b * a)

Tactic:
by

Goal state after:
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 ∧ IsSMulRegular M b

Tactic:
by

Goal state after: