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

Goal state before:
pp: ι : Type u
f : ι → Ordinal.{u} → Ordinal.{u}
c : Cardinal.{u}
hc : c.IsRegular
hι : #ι < c
hc' : c ≠ ℵ₀
a : Ordinal.{u}
hf : ∀ (i : ι), ∀ b < c.ord, f i b < c.ord
⊢ lift.{?u.39, u} #ι < c

Tactic:
by

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

Goal state before:
pp: f : Ordinal.{u_1} → Ordinal.{u_1}
c : Cardinal.{u_1}
hc : c.IsRegular
hc' : c ≠ ℵ₀
hf : ∀ i < c.ord, f i < c.ord
a : Ordinal.{u_1}
⊢ ℵ₀ < c.ord.cof

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝ : Infinite β
f : α → Finset β
w : ⋃ a, ↑(f a) = Set.univ
⊢ #β ≤ #↑(range f)

Tactic:
by

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

Goal state before:
pp: ι : Type u
f : ι → Ordinal.{max u v} → Ordinal.{max u v}
c : Cardinal.{max u v}
hc : c.IsRegular
hι : lift.{v, u} #ι < c
hc' : c ≠ ℵ₀
hf : ∀ (i : ι), ∀ b < c.ord, f i b < c.ord
a : Ordinal.{max u v}
⊢ ℵ₀ < c.ord.cof

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: α : Type u_1
h : (#α).IsStrongPrelimit
⊢ #{ s // #↑s < (#α).ord.cof } = #α

Tactic:
by

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

Goal state before:
pp: α : Type u
β' : Type v
inst✝ : Infinite α
leq : lift.{v, u} #α = lift.{u, v} #β'
⊢ #(α ≃ β') = #(α → β')

Tactic:
by

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

Goal state before:
pp: α : Type u
β' : Type v
inst✝ : Infinite α
leq : lift.{v, u} #α = lift.{u, v} #β'
⊢ #(α ≃ β') = 2 ^ lift.{v, u} #α

Tactic:
by

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

Goal state before:
pp: α β : Type u
inst✝ : Infinite α
eq : #α = #β
⊢ #(α ≃ β) = 2 ^ #α

Tactic:
by

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

Goal state before:
pp: α : Type u
β' : Type v
inst✝ : Infinite α
lle : lift.{u, v} #β' ≤ lift.{v, u} #α
⊢ #(β' → α) ≤ #(β' ↪ α)

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: α : Type u_1
hc : ℵ₀ ≤ #α
w✝¹ : LinearOrder α
w✝ : WellFoundedLT α
hα : (#α).ord = typeLT α
⊢ NoMaxOrder α

Tactic:
by

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

Goal state before:
pp: α : Type u
β' : Type v
inst✝ : Infinite α
lle : lift.{u, v} #β' ≤ lift.{v, u} #α
⊢ Nonempty (α ≃ α ⊕ β')

Tactic:
by

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

Goal state before:
pp: α : Type u
β' : Type v
inst✝ : Infinite α
lle : lift.{u, v} #β' ≤ lift.{v, u} #α
e : α ≃ α ⊕ β'
f g : α → β'
h : (fun f ↦ ⟨fun a ↦ Sum.elim f id (e a), ⋯⟩) f = (fun f ↦ ⟨fun a ↦ Sum.elim f id (e a), ⋯⟩) g
a : α
⊢ f a = g a

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝ : Infinite α
H1 : ℵ₀ ≤ #α
x✝ : α
⊢ ∀ ⦃a₂ : α⦄, (fun a ↦ [a]) x✝ = (fun a ↦ [a]) a₂ → x✝ = a₂

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝ : Infinite α
H1 : ℵ₀ ≤ #α
⊢ (sum fun x ↦ #α) = #α

Tactic:
by

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

Goal state before:
pp: ι : Type u
f : ι → Ordinal.{max u v} → Ordinal.{max u v}
c : Cardinal.{max u v}
hc : c.IsRegular
hι : lift.{v, u} #ι < c
hc' : c ≠ ℵ₀
hf : ∀ (i : ι), ∀ b < c.ord, f i b < c.ord
hω : ℵ₀ < c.ord.cof
⊢ lift.{?u.55, u} #ι < c.ord.cof

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝ : Nonempty α
⊢ #(List α) = max ℵ₀ #α

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝ : Nonempty α
⊢ #(List α) = max #α ℵ₀

Tactic:
by

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

Goal state before:
pp: x : Cardinal.{u_1}
h : x ≠ 0
⊢ (sum fun n ↦ x ^ n) = max ℵ₀ x

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: c : Cardinal.{u_1}
hc : ℵ₀ ≤ c
⊢ c < c ^ c.ord.cof

Tactic:
by

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

Goal state before:
pp: α : Type u
⊢ #(List α) ≤ max ℵ₀ #α

Tactic:
by

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: a b : Cardinal.{u_1}
ha : ℵ₀ ≤ a
hb : 1 < b
⊢ a < (b ^ a).ord.cof

Tactic:
by

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

Goal state before:
pp: x : Cardinal.{u_1}
⊢ (sum fun n ↦ x ^ n) ≤ max ℵ₀ x

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝ : Infinite α
⊢ #(Finset α) = #α

Tactic:
by

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

Goal state before:
pp: ι : Type u
f : ι → Ordinal.{max u v} → Ordinal.{max u v}
c : Cardinal.{max u v}
hc : c.IsRegular
hι : lift.{v, u} #ι < c
hc' : c ≠ ℵ₀
hf : ∀ (i : ι), ∀ b < c.ord, f i b < c.ord
hω : ℵ₀ < c.ord.cof
b : Ordinal.{max u v}
hb : b < c.ord → derivFamily f b < c.ord
hb' : b + 1 < c.ord
⊢ lift.{?u.60, u} #ι < c.ord.cof

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Basis.Cardinality

Goal state before:
pp: R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Nontrivial M
ι : Type u_1
s : Set (ι →₀ M)
hs : s.Finite
hsspan : span R s = ⊤
this : ⋃ i ∈ s, ↑i.support = Set.univ
x✝¹ : ι →₀ M
x✝ : x✝¹ ∈ s
⊢ (↑x✝¹.support).Finite

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Basis.Cardinality

Goal state before:
pp: R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Nontrivial R
s : Set M
hs : s.Finite
hsspan : span R s = ⊤
ι : Type w
b : Basis ι R M
⊢ Finite ι

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Basis.Cardinality

Goal state before:
pp: R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Nontrivial R
inst✝ : Module R M
ι : Type w
b : Basis ι R M
κ : Type w'
v : κ → M
ind : LinearIndependent R v
m : ind.Maximal
i : ι
w : ∀ (x : κ), (b.repr (v x)) i = 0
l : κ →₀ R
⊢ (b.repr ((linearCombination R v) l)) i = 0

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Basis.Cardinality

Goal state before:
pp: R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Nontrivial R
inst✝ : Module R M
ι : Type w
b : Basis ι R M
κ : Type w'
v : κ → M
ind : LinearIndependent R v
m : ind.Maximal
i : ι
w : ∀ (x : κ), (b.repr (v x)) i = 0
repr_eq_zero : ∀ (l : κ →₀ R), (b.repr ((linearCombination R v) l)) i = 0
v' : Option κ → M := fun o ↦ o.elim (b i) v
⊢ range v ⊆ range v'

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Basis.Cardinality

Goal state before:
pp: R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Nontrivial R
inst✝ : Module R M
ι : Type w
b : Basis ι R M
κ : Type w'
v : κ → M
ind : LinearIndependent R v
m : ind.Maximal
i : ι
w : ∀ (x : κ), (b.repr (v x)) i = 0
repr_eq_zero : ∀ (l : κ →₀ R), (b.repr ((linearCombination R v) l)) i = 0
v' : Option κ → M := fun o ↦ o.elim (b i) v
r : range v ⊆ range v'
x✝ : b i ∈ range v
k : κ
p : v k = b i
⊢ False

Tactic:
by

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

Goal state before:
pp: ι : Type u
f : ι → Ordinal.{max u v} → Ordinal.{max u v}
c : Cardinal.{max u v}
hc : c.IsRegular
hι : lift.{v, u} #ι < c
hc' : c ≠ ℵ₀
hf : ∀ (i : ι), ∀ b < c.ord, f i b < c.ord
a : Ordinal.{max u v}
⊢ a < c.ord → derivFamily f a < c.ord

Tactic:
by

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

Goal state before:
pp: ι : Type u
f : ι → Ordinal.{u} → Ordinal.{u}
c : Cardinal.{u}
hc : c.IsRegular
hι : #ι < c
hc' : c ≠ ℵ₀
hf : ∀ (i : ι), ∀ b < c.ord, f i b < c.ord
a : Ordinal.{u}
⊢ lift.{?u.39, u} #ι < c

Tactic:
by

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

Goal state before:
pp: f : Ordinal.{u} → Ordinal.{u}
c : Cardinal.{u}
hc : c.IsRegular
hc' : c ≠ ℵ₀
hf : ∀ i < c.ord, f i < c.ord
a : Ordinal.{u}
⊢ lift.{u, 0} #Unit < c

Tactic:
by

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

Goal state before:
pp: α : Type u
inst✝ : Infinite α
c : Cardinal.{u}
⊢ #{ t // #↑t ≤ c } ≤ #α ^ c

Tactic:
by

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

Goal state before:
pp: c : Cardinal.{u_1}
⊢ ¬(succ c).IsSingular

Tactic:
by

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

Goal state before:
pp: o : Ordinal.{u_1}
⊢ ¬(ℵ_ (o + 1)).IsSingular

Tactic:
by

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

Goal state before:
pp: c : Cardinal.{u_1}
hc : c.IsSingular
⊢ IsSuccLimit c

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: c : Cardinal.{u_1}
⊢ c < ℵ₀ ∨ c.IsRegular ∨ c.IsSingular

Tactic:
by

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

Goal state before:
pp: o : Ordinal.{u_1}
⊢ (ℵ_ o).IsSingular ↔ IsSuccLimit o ∧ o.cof < ℵ_ o

Tactic:
by

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

Goal state before:
pp: ⊢ (ℵ_ ω).IsSingular

Tactic:
by

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

Goal state before:
pp: c : Cardinal.{u_1}
hc : c.IsSingular
⊢ ℵ_ ω ≤ c

Tactic:
by

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

Goal state before:
pp: ⊢ Cardinal.univ.{u, v} ≤ Cardinal.univ.{u, v}.ord.cof

Tactic:
by

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

Goal state before:
pp: α : Type u
c : Cardinal.{u}
⊢ #{ t // #↑t ≤ c } ≤ max #α ℵ₀ ^ c

Tactic:
by

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

Goal state before:
pp: c : Cardinal.{u_1}
hc : c.IsInaccessible
⊢ preBeth c.ord = c

Tactic:
by

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

Goal state before:
pp: α : Type u
s : Set α
c : Cardinal.{u}
⊢ #{ t // t ⊆ s ∧ #↑t ≤ c } ≤ max #↑s ℵ₀ ^ c

Tactic:
by

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

Goal state before:
pp: c : Cardinal.{u_1}
hc : c.IsInaccessible
⊢ ℶ_ c.ord = c

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : Infinite α
s : Set α
h2 : #↑s < #α
⊢ #↑sᶜ = #α

Tactic:
by

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

Goal state before:
pp: c : Cardinal.{u_1}
hc : c.IsInaccessible
⊢ preAleph.symm c = c.ord

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : Infinite α
s : Finset α
⊢ #↑(↑s)ᶜ = #α

Tactic:
by

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

Goal state before:
pp: c : Cardinal.{u_1}
hc : c.IsInaccessible
⊢ preOmega c.ord = c.ord

Tactic:
by

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

Goal state before:
pp: c : Cardinal.{u_1}
hc : c.IsInaccessible
⊢ ω_ c.ord = c.ord

Tactic:
by

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

Goal state before:
pp: α : Type u_1
inst✝ : Infinite α
s t : Set α
hs : #↑s < #α
ht : #↑t < #α
⊢ #↑sᶜ = #↑tᶜ

Tactic:
by

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

Goal state before:
pp: ⊢ preBeth Ordinal.univ.{u, v} = univ.{u, v}

Tactic:
by

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

Goal state before:
pp: ⊢ ℶ_ Ordinal.univ.{u, v} = univ.{u, v}

Tactic:
by

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

Goal state before:
pp: ⊢ preAleph Ordinal.univ.{u, v} = univ.{u, v}

Tactic:
by

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

Goal state before:
pp: ⊢ preAleph.symm univ.{u, v} = Ordinal.univ.{u, v}

Tactic:
by

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

Goal state before:
pp: ⊢ ℵ_ Ordinal.univ.{u, v} = univ.{u, v}

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Basis.Cardinality

Goal state before:
pp: R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Nontrivial R
inst✝ : Module R M
ι : Type w
b : Basis ι R M
κ : Type w'
v : κ → M
ind : LinearIndependent R v
m : ind.Maximal
i : ι
w : ∀ (x : κ), (b.repr (v x)) i = 0
repr_eq_zero : ∀ (l : κ →₀ R), (b.repr ((linearCombination R v) l)) i = 0
v' : Option κ → M := fun o ↦ o.elim (b i) v
r : range v ⊆ range v'
r' : b i ∉ range v
r'' : range v ≠ range v'
l l' : Option κ →₀ R
z : l none • b i + (linearCombination R v) l.some = l' none • b i + (linearCombination R v) l'.some
a : κ
j : ι
⊢ (b.repr ((linearCombination R v) l.some)) j = (b.repr ((linearCombination R v) l'.some)) j

Tactic:
by

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

Goal state before:
pp: ⊢ preOmega Ordinal.univ.{u, v} = Ordinal.univ.{u, v}

Tactic:
by

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

Goal state before:
pp: ⊢ ω_ Ordinal.univ.{u, v} = Ordinal.univ.{u, v}

Tactic:
by

Goal state after:
Module: Mathlib.Data.DFinsupp.Ext

Goal state before:
pp: ι : Type u
β : ι → Type v
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → AddZeroClass (β i)
x : Π₀ (i : ι), β i
x✝ : x ∈ ⊤
⊢ x ∈ AddSubmonoid.closure (⋃ i, Set.range (single i))

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Basis.Cardinality

Goal state before:
pp: R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Nontrivial R
inst✝ : Module R M
ι : Type w
b : Basis ι R M
κ : Type w'
v : κ → M
ind : LinearIndependent R v
m : ind.Maximal
i : ι
w : ∀ (x : κ), (b.repr (v x)) i = 0
repr_eq_zero : ∀ (l : κ →₀ R), (b.repr ((linearCombination R v) l)) i = 0
v' : Option κ → M := fun o ↦ o.elim (b i) v
r : range v ⊆ range v'
r' : b i ∉ range v
r'' : range v ≠ range v'
⊢ LinearIndepOn R id (range v')

Tactic:
by

Goal state after:
Module: Mathlib.Data.DFinsupp.Ext

Goal state before:
pp: ι : Type u
β : ι → Type v
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → AddZeroClass (β i)
γ : Type w
inst✝ : AddZeroClass γ
f g : (Π₀ (i : ι), β i) →+ γ
H : ∀ (i : ι) (y : β i), f (single i y) = g (single i y)
⊢ f = g

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Basis.Cardinality

Goal state before:
pp: R : Type u
M : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Nontrivial R
inst✝ : Module R M
ι : Type w
b : Basis ι R M
κ : Type w'
v : κ → M
ind : LinearIndependent R v
m : ind.Maximal
⊢ ⋃ k, ↑(b.repr (v k)).support = Set.univ

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Basis.Cardinality

Goal state before:
pp: R : Type u
M : Type v
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Nontrivial R
inst✝¹ : Module R M
ι : Type w
b : Basis ι R M
inst✝ : Infinite ι
κ : Type w'
v : κ → M
i : LinearIndependent R v
m : i.Maximal
Φ : κ → Finset ι := fun k ↦ (b.repr (v k)).support
⊢ #ι ≤ #↑(range Φ)

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
inst✝ : Finite α
s : Set α
t : Set β
h1 : lift.{v, u} #α = lift.{u, v} #β
h2 : lift.{v, u} #↑s = lift.{u, v} #↑t
⊢ lift.{v, u} #↑sᶜ = lift.{u, v} #↑tᶜ

Tactic:
by

Goal state after:
Module: Mathlib.LinearAlgebra.Basis.Cardinality

Goal state before:
pp: R : Type u
M : Type v
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Nontrivial R
inst✝¹ : Module R M
ι : Type w
b : Basis ι R M
inst✝ : Infinite ι
κ : Type w'
v : κ → M
i : LinearIndependent R v
m : i.Maximal
⊢ Cardinal.lift.{w', w} #ι ≤ Cardinal.lift.{w, w'} #κ

Tactic:
by

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

Goal state before:
pp: α β : Type u
inst✝ : Finite α
s : Set α
t : Set β
h1 : #α = #β
h : #↑s = #↑t
⊢ #↑sᶜ = #↑tᶜ

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
f : ↑s ↪ β
h : Nonempty (↑sᶜ ≃ ↑(range ⇑f)ᶜ)
⊢ ∃ g, ∀ (x : ↑s), g ↑x = f x

Tactic:
by

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

Goal state before:
pp: α : Type u
β : Type v
inst✝ : Finite α
s : Set α
f : ↑s ↪ β
h : Nonempty (α ≃ β)
⊢ ∃ g, ∀ (x : ↑s), g ↑x = f x

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
s : Set α
f : ↑s ↪ β
hs : #↑s < #α
h : Nonempty (α ≃ β)
⊢ ∃ g, ∀ (x : ↑s), g ↑x = f x

Tactic:
by

Goal state after:
Module: Mathlib.Data.DFinsupp.Submonoid

Goal state before:
pp: ι : Type u
γ : Type w
β : ι → Type v
inst✝⁴ : DecidableEq ι
inst✝³ : (i : ι) → AddZeroClass (β i)
inst✝² : AddCommMonoid γ
S : Type u_1
inst✝¹ : SetLike S γ
inst✝ : AddSubmonoidClass S γ
s : S
f : Π₀ (i : ι), β i
g : (i : ι) → β i →+ γ
h : ∀ (c : ι), f c ≠ 0 → (g c) (f c) ∈ s
⊢ (sumAddHom g) f ∈ s

Tactic:
by

Goal state after:
Module: Mathlib.Data.DFinsupp.Defs

Goal state before:
pp: ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst✝² : (i : ι) → Zero (β i)
inst✝¹ : (i : ι) → Zero (β₁ i)
inst✝ : (i : ι) → Zero (β₂ i)
x✝¹ x✝ : Π₀ (i : ι), β i
f₁ : (i : ι) → β i
s₁✝ : Trunc { s // ∀ (i : ι), i ∈ s ∨ f₁ i = 0 }
f₂ : (i : ι) → β i
s₁ : Trunc { s // ∀ (i : ι), i ∈ s ∨ f₂ i = 0 }
h : f₁ = f₂
⊢ { toFun := f₁, support' := s₁✝ } = { toFun := f₂, support' := s₁ }

Tactic:
by

Goal state after:
Module: Mathlib.Data.DFinsupp.Submonoid

Goal state before:
pp: ι : Type u
γ : Type w
inst✝¹ : DecidableEq ι
inst✝ : AddCommMonoid γ
S : ι → AddSubmonoid γ
⊢ iSup S = AddMonoidHom.mrange (sumAddHom fun i ↦ (S i).subtype)

Tactic:
by

Goal state after:
Module: Mathlib.Data.DFinsupp.Defs

Goal state before:
pp: ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst✝² : (i : ι) → Zero (β i)
inst✝¹ : (i : ι) → Zero (β₁ i)
inst✝ : (i : ι) → Zero (β₂ i)
f : (i : ι) → β₁ i → β₂ i
hf : ∀ (i : ι), f i 0 = 0
x : Π₀ (i : ι), β₁ i
s : { s // ∀ (i : ι), i ∈ s ∨ x.toFun i = 0 }
i : ι
h : x i = 0
⊢ f i (x i) = 0

Tactic:
by

Goal state after:
Module: Mathlib.Data.DFinsupp.Defs

Goal state before:
pp: ι : Type u
β₁ : ι → Type v₁
inst✝ : (i : ι) → Zero (β₁ i)
h : ∀ (i : ι), id 0 = 0
g : Π₀ (i : ι), β₁ i
⊢ mapRange (fun i ↦ id) h g = g

Tactic:
by

Goal state after:
Module: Mathlib.Data.DFinsupp.Defs

Goal state before:
pp: ι : Type u
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst✝² : (i : ι) → Zero (β i)
inst✝¹ : (i : ι) → Zero (β₁ i)
inst✝ : (i : ι) → Zero (β₂ i)
f : (i : ι) → β₁ i → β₂ i
f₂ : (i : ι) → β i → β₁ i
hf : ∀ (i : ι), f i 0 = 0
hf₂ : ∀ (i : ι), f₂ i 0 = 0
h : ∀ (i : ι), (f i ∘ f₂ i) 0 = 0
g : Π₀ (i : ι), β i
⊢ mapRange (fun i ↦ f i ∘ f₂ i) h g = mapRange f hf (mapRange f₂ hf₂ g)

Tactic:
by

Goal state after:
Module: Mathlib.Data.DFinsupp.Defs

Goal state before:
pp: ι : Type u
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst✝¹ : (i : ι) → Zero (β₁ i)
inst✝ : (i : ι) → Zero (β₂ i)
f : (i : ι) → β₁ i → β₂ i
hf : ∀ (i : ι), f i 0 = 0
⊢ mapRange f hf 0 = 0

Tactic:
by

Goal state after:
Module: Mathlib.Data.DFinsupp.Submonoid

Goal state before:
pp: ι : Type u
γ : Type w
inst✝² : DecidableEq ι
p : ι → Prop
inst✝¹ : DecidablePred p
inst✝ : AddCommMonoid γ
S : ι → AddSubmonoid γ
⊢ ⨆ i, ⨆ (_ : p i), S i =
    AddMonoidHom.mrange ((sumAddHom fun i ↦ (S i).subtype).comp (filterAddMonoidHom (fun i ↦ ↥(S i)) p))

Tactic:
by

Goal state after:
Module: Mathlib.Data.DFinsupp.Submonoid

Goal state before:
pp: ι : Type u
γ : Type w
inst✝² : DecidableEq ι
inst✝¹ : AddCommMonoid γ
S : ι → AddSubmonoid γ
inst✝ : (i : ι) → (x : ↥(S i)) → Decidable (x ≠ 0)
x : γ
⊢ x ∈ iSup S ↔ ∃ f, (f.sum fun x xi ↦ ↑xi) = x

Tactic:
by

Goal state after:
Module: Mathlib.Data.DFinsupp.Defs

Goal state before:
pp: ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst✝² : (i : ι) → Zero (β i)
inst✝¹ : (i : ι) → Zero (β₁ i)
inst✝ : (i : ι) → Zero (β₂ i)
f : (i : ι) → β₁ i → β₂ i → β i
hf : ∀ (i : ι), f i 0 0 = 0
x : Π₀ (i : ι), β₁ i
y : Π₀ (i : ι), β₂ i
⊢ Trunc { s // ∀ (i : ι), i ∈ s ∨ f i (x i) (y i) = 0 }

Tactic:
by

Goal state after:
Module: Mathlib.Data.DFinsupp.Defs

Goal state before:
pp: ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst✝¹ : (i : ι) → Zero (β i)
p : ι → Prop
inst✝ : DecidablePred p
x : Π₀ (i : ι), β i
xs : { s // ∀ (i : ι), i ∈ s ∨ x.toFun i = 0 }
i : ι
H : x i = 0
⊢ (if p i then x i else 0) = 0

Tactic:
by

Goal state after:
Module: Mathlib.Data.DFinsupp.Defs

Goal state before:
pp: ι : Type u
β : ι → Type v
inst✝¹ : (i : ι) → Zero (β i)
p : ι → Prop
inst✝ : DecidablePred p
f : Π₀ (i : ι), β i
i : ι
h : p i
⊢ (filter p f) i = f i

Tactic:
by

Goal state after:
Module: Mathlib.Data.DFinsupp.Defs

Goal state before:
pp: ι : Type u
β : ι → Type v
inst✝¹ : (i : ι) → Zero (β i)
p : ι → Prop
inst✝ : DecidablePred p
f : Π₀ (i : ι), β i
i : ι
h : ¬p i
⊢ (filter p f) i = 0

Tactic:
by

Goal state after:
Module: Mathlib.Data.DFinsupp.Defs

Goal state before:
pp: ι : Type u
β : ι → Type v
inst✝¹ : (i : ι) → AddZeroClass (β i)
f : Π₀ (i : ι), β i
p : ι → Prop
inst✝ : DecidablePred p
i : ι
⊢ (filter p f + filter (fun i ↦ ¬p i) f) i = f i

Tactic:
by

Goal state after:
Module: Mathlib.Data.DFinsupp.Defs

Goal state before:
pp: ι : Type u
β : ι → Type v
inst✝¹ : (i : ι) → Zero (β i)
p : ι → Prop
inst✝ : DecidablePred p
⊢ filter p 0 = 0

Tactic:
by

Goal state after:
Module: Mathlib.Data.DFinsupp.Defs

Goal state before:
pp: ι : Type u
β : ι → Type v
inst✝¹ : (i : ι) → AddZeroClass (β i)
p : ι → Prop
inst✝ : DecidablePred p
f g : Π₀ (i : ι), β i
⊢ filter p (f + g) = filter p f + filter p g

Tactic:
by

Goal state after:
Module: Mathlib.Data.DFinsupp.Defs

Goal state before:
pp: ι : Type u
β : ι → Type v
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : DecidableEq ι
s : Finset ι
x y : (i : ↑↑s) → β ↑i
H : mk s x = mk s y
i : ↑↑s
⊢ (mk s x) ↑i = (mk s y) ↑i

Tactic:
by

Goal state after:
Module: Mathlib.Data.DFinsupp.Defs

Goal state before:
pp: ι : Type u
β : ι → Type v
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : DecidableEq ι
s : Finset ι
⊢ Function.Injective (mk s)

Tactic:
by

Goal state after:
Module: Mathlib.Data.DFinsupp.Defs

Goal state before:
pp: ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : DecidableEq ι
i : ι
b : β i
j : ι
⊢ j = i → j ∈ {i}

Tactic:
by

Goal state after:
Module: Mathlib.Data.DFinsupp.Defs

Goal state before:
pp: ι : Type u
β : ι → Type v
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : DecidableEq ι
i i' : ι
b : β i
⊢ (single i b) i' = if h : i = i' then Eq.recOn h b else 0

Tactic:
by

Goal state after:
Module: Mathlib.Data.DFinsupp.Defs

Goal state before:
pp: ι : Type u
β : ι → Type v
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : DecidableEq ι
i : ι
b : β i
⊢ (single i b) i = b

Tactic:
by

Goal state after:
Module: Mathlib.Data.DFinsupp.Defs

Goal state before:
pp: ι : Type u
β : ι → Type v
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : DecidableEq ι
i i' : ι
b : β i
h : i' ≠ i
⊢ (single i b) i' = 0

Tactic:
by

Goal state after:
Module: Mathlib.Data.DFinsupp.Defs

Goal state before:
pp: ι : Type u
β : ι → Type v
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : DecidableEq ι
i j : ι
xi : β i
xj : β j
⊢ single i xi = single j xj ↔ i = j ∧ xi ≍ xj ∨ xi = 0 ∧ xj = 0

Tactic:
by

Goal state after:
Module: Mathlib.Data.DFinsupp.Defs

Goal state before:
pp: ι : Type u
β : ι → Type v
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : DecidableEq ι
i : ι
xi : β i
⊢ single i xi = 0 ↔ xi = 0

Tactic:
by

Goal state after:
Module: Mathlib.Data.DFinsupp.Defs

Goal state before:
pp: ι : Type u
β : ι → Type v
inst✝² : (i : ι) → Zero (β i)
inst✝¹ : DecidableEq ι
p : ι → Prop
inst✝ : DecidablePred p
i : ι
x : β i
⊢ filter p (single i x) = if p i then single i x else 0

Tactic:
by

Goal state after:
Module: Mathlib.Data.DFinsupp.Defs

Goal state before:
pp: ι : Type u
β : ι → Type v
inst✝² : (i : ι) → Zero (β i)
inst✝¹ : DecidableEq ι
p : ι → Prop
inst✝ : DecidablePred p
i : ι
x : β i
h : p i
⊢ filter p (single i x) = single i x

Tactic:
by

Goal state after:
Module: Mathlib.Data.DFinsupp.Defs

Goal state before:
pp: ι : Type u
β : ι → Type v
inst✝² : (i : ι) → Zero (β i)
inst✝¹ : DecidableEq ι
p : ι → Prop
inst✝ : DecidablePred p
i : ι
x : β i
h : ¬p i
⊢ filter p (single i x) = 0

Tactic:
by

Goal state after:
Module: Mathlib.Data.DFinsupp.Defs

Goal state before:
pp: ι : Type u
β : ι → Type v
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : DecidableEq ι
i j : ι
xi : β i
xj : β j
h : ⟨i, xi⟩ = ⟨j, xj⟩
⊢ single i xi = single j xj

Tactic:
by

Goal state after: