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

Goal state before:
pp: case mk
α : Type u_1
hc : ℵ₀ ≤ #α
w✝¹ : LinearOrder α
w✝ : WellFoundedLT α
hα : (#α).ord = typeLT α
this : NoMaxOrder α
s : Set α
hs : IsCofinal s
hs' : typeLT ↑s = (Order.cof α).ord
⊢ #↑(⋃ i ∈ s, Iio i) ≤ #↑(⋃ i, ⋃ (h : i ∈ s), Iio ↑⟨i, h⟩)

Tactic:
]

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

Goal state before:
pp: case inr
α : Type u
h✝ : Infinite α
⊢ #α ≤ max ℵ₀ #α

Tactic:
]

Goal state after:
case inr
α : Type u
h✝ : Infinite α
⊢ #α ≤ max ℵ₀ #α
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: x : Cardinal.{u_1}
⊢ #(List (Quotient.out x)) ≤ max ℵ₀ #(Quotient.out x)

Tactic:
]

Goal state after:
x : Cardinal.{u_1}
⊢ #(List (Quotient.out x)) ≤ max ℵ₀ #(Quotient.out x)
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

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

Tactic:
]

Goal state after:
a b : Cardinal.{u_1}
ha : ℵ₀ ≤ a
hb : 1 < b
⊢ b ^ a < (b ^ a) ^ (b ^ a).ord.cof
Module: Mathlib.SetTheory.Cardinal.Regular

Goal state before:
pp: case add_one
ι : 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
⊢ nfpFamily f (derivFamily f b + 1) < c.ord

Tactic:
]

Goal state after:
case add_one
ι : 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
⊢ nfpFamily f (derivFamily f b + 1) < c.ord
Module: Mathlib.SetTheory.Cardinal.Arithmetic

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

Tactic:
]

Goal state after:
α : Type u
inst✝ : Infinite α
c : Cardinal.{u}
⊢ #{ t // #↑t ≤ c } ≤ (#α + 1) ^ c
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.{v, u} #ι < c

Tactic:
]

Goal state after:
ι : 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.{v, u} #ι < c
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
this : span R (⇑↑b.repr '' s) = ⊤
⊢ Finite ι

Tactic:
]

Goal state after:
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
this : span R (⇑↑b.repr '' s) = ⊤
⊢ Finite ι
Module: Mathlib.SetTheory.Cardinal.Regular

Goal state before:
pp: case limit
ι : 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 : IsSuccLimit b
H : ∀ o' < b, o' < c.ord → derivFamily f o' < c.ord
hb' : b < c.ord
⊢ ⨆ b_1, derivFamily f ↑b_1 < c.ord

Tactic:
]

Goal state after:
case limit
ι : 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 : IsSuccLimit b
H : ∀ o' < b, o' < c.ord → derivFamily f o' < c.ord
hb' : b < c.ord
⊢ ⨆ b_1, derivFamily f ↑b_1 < c.ord
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: case pos
α : Type u
inst✝ : Infinite α
β : Type u
s : Set α
g : ↑s ↪ β
x : α
y : β
h' : ∃ z, g z = y
h : Sum.inl ↑(Classical.choose h') = Sum.inl x
⊢ x ∈ ↑⟨s, ⋯⟩

Tactic:
]

Goal state after:
case pos
α : Type u
inst✝ : Infinite α
β : Type u
s : Set α
g : ↑s ↪ β
x : α
y : β
h' : ∃ z, g z = y
h : Sum.inl ↑(Classical.choose h') = Sum.inl x
⊢ x ∈ ↑⟨s, ⋯⟩
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: case neg
α : Type u
inst✝ : Infinite α
β : Type u
s : Set α
g : ↑s ↪ β
x : α
y : β
h : Sum.inr { down := 0 } = Sum.inl x
h' : ¬∃ z, g z = y
⊢ x ∈ ↑⟨s, ⋯⟩

Tactic:
]

Goal state after:
case neg
α : Type u
inst✝ : Infinite α
β : Type u
s : Set α
g : ↑s ↪ β
x : α
y : β
h : Sum.inr { down := 0 } = Sum.inl x
h' : ¬∃ z, g z = y
⊢ x ∈ ↑⟨s, ⋯⟩
Module: Mathlib.SetTheory.Cardinal.Regular

Goal state before:
pp: case limit.ha
ι : 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 : IsSuccLimit b
H : ∀ o' < b, o' < c.ord → derivFamily f o' < c.ord
hb' : b < c.ord
⊢ b < c.ord

Tactic:
]

Goal state after:
case limit.ha
ι : 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 : IsSuccLimit b
H : ∀ o' < b, o' < c.ord → derivFamily f o' < c.ord
hb' : b < c.ord
⊢ b < c.ord
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), (linearCombination R v') l₁ = (linearCombination R v') l₂ → l₁ = l₂

Tactic:
]

Goal state after:
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), (linearCombination R v') l₁ = (linearCombination R v') l₂ → l₁ = l₂
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: case h
α : Type u
inst✝ : Infinite α
β : Type u
s : Set α
g : ↑s ↪ β
x : α
h : x ∈ ↑⟨s, ⋯⟩
this : ∃ z, g z = g ⟨x, h⟩
⊢ Sum.inl ↑(Classical.choose this) = Sum.inl x

Tactic:
]

Goal state after:
case h
α : Type u
inst✝ : Infinite α
β : Type u
s : Set α
g : ↑s ↪ β
x : α
h : x ∈ ↑⟨s, ⋯⟩
this : ∃ z, g z = g ⟨x, h⟩
⊢ Sum.inl ↑(Classical.choose this) = Sum.inl x
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}
⊢ #ι < c

Tactic:
]

Goal state after:
ι : 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}
⊢ #ι < c
Module: Mathlib.SetTheory.Cardinal.Regular

Goal state before:
pp: case inl
n : ℕ
hc : ↑n < ℵ₀
h : (succ ↑n).IsSingular
⊢ ↑(n + 1) < ℵ₀

Tactic:
]

Goal state after:
case inl
n : ℕ
hc : ↑n < ℵ₀
h : (succ ↑n).IsSingular
⊢ ↑(n + 1) < ℵ₀
Module: Mathlib.SetTheory.Cardinal.Regular

Goal state before:
pp: c : Cardinal.{u_1}
hc : c.IsSingular
⊢ c ≠ 0 ∧ ∀ (b : Cardinal.{u_1}), succ b ≠ c

Tactic:
]

Goal state after:
c : Cardinal.{u_1}
hc : c.IsSingular
⊢ c ≠ 0 ∧ ∀ (b : Cardinal.{u_1}), succ b ≠ c
Module: Mathlib.SetTheory.Cardinal.Regular

Goal state before:
pp: c : Cardinal.{u_1}
h : ℵ₀ ≤ c
⊢ c.IsRegular ∨ ℵ₀ ≤ c ∧ ¬c ≤ c.ord.cof

Tactic:
]

Goal state after:
c : Cardinal.{u_1}
h : ℵ₀ ≤ c
⊢ c.IsRegular ∨ ℵ₀ ≤ c ∧ ¬c ≤ c.ord.cof
Module: Mathlib.SetTheory.Cardinal.Regular

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

Tactic:
]

Goal state after:
c : Cardinal.{u_1}
this : ℵ₀ ≤ c → c.IsRegular ∨ c.IsSingular
⊢ ¬ℵ₀ ≤ c ∨ c.IsRegular ∨ c.IsSingular
Module: Mathlib.SetTheory.Cardinal.Arithmetic

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

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

Tactic:
· refine ⟨Embedding.subtypeMap ?_ ?_⟩
    · apply Embedding.image
      use Sum.inr
      apply Sum.inr.inj
    intro s hs
    exact mk_image_le.trans hs

Goal state after:
α : Type u
c : Cardinal.{u}
⊢ #{ t // #↑t ≤ c } ≤ max #α ℵ₀ ^ c
Module: Mathlib.SetTheory.Cardinal.Regular

Goal state before:
pp: case inr.inr
o : Ordinal.{u_1}
ho : IsSuccLimit o
⊢ ℵ₀ ≤ ℵ_ o ∧ (ℵ_ o).ord.cof < ℵ_ o ↔ IsSuccLimit o ∧ o.cof < ℵ_ o

Tactic:
]

Goal state after:
case inr.inr
o : Ordinal.{u_1}
ho : IsSuccLimit o
⊢ ℵ₀ ≤ ℵ_ o ∧ (ℵ_ o).ord.cof < ℵ_ o ↔ IsSuccLimit o ∧ o.cof < ℵ_ o
Module: Mathlib.SetTheory.Cardinal.Regular

Goal state before:
pp: o : Ordinal.{u_1}
hc : IsSuccLimit o ∧ o.cof < ℵ_ o
⊢ ℵ_ ω ≤ ℵ_ o

Tactic:
]

Goal state after:
o : Ordinal.{u_1}
hc : IsSuccLimit o ∧ o.cof < ℵ_ o
⊢ ℵ_ ω ≤ ℵ_ o
Module: Mathlib.SetTheory.Cardinal.Regular

Goal state before:
pp: o : Ordinal.{u_1}
hc : IsSuccLimit o ∧ o.cof < ℵ_ o
⊢ ω ≤ o

Tactic:
]

Goal state after:
o : Ordinal.{u_1}
hc : IsSuccLimit o ∧ o.cof < ℵ_ o
⊢ ω ≤ o
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: α : Type u
c : Cardinal.{u}
⊢ #(ULift.{u, 0} ℕ ⊕ α) ^ c ≤ (ℵ₀ + #α) ^ c

pp: α : Type u
c : Cardinal.{u}
⊢ ℵ₀ ≤ ℵ₀

Tactic:
]

Goal state after:
α : Type u
c : Cardinal.{u}
⊢ #(ULift.{u, 0} ℕ ⊕ α) ^ c ≤ (ℵ₀ + #α) ^ c

α : Type u
c : Cardinal.{u}
⊢ ℵ₀ ≤ ℵ₀
Module: Mathlib.SetTheory.Cardinal.Regular

Goal state before:
pp: case ind
c : Cardinal.{u_1}
hc : c.IsInaccessible
a : Ordinal.{u_1}
IH : ∀ y < a, y < c.ord → preBeth y < c
ha : a < c.ord
⊢ ⨆ a_1, 2 ^ preBeth ↑a_1 < c

Tactic:
]

Goal state after:
case ind
c : Cardinal.{u_1}
hc : c.IsInaccessible
a : Ordinal.{u_1}
IH : ∀ y < a, y < c.ord → preBeth y < c
ha : a < c.ord
⊢ ⨆ a_1, 2 ^ preBeth ↑a_1 < c
Module: Mathlib.SetTheory.Cardinal.Regular

Goal state before:
pp: c : Cardinal.{u_1}
hc : c.IsInaccessible
a : Ordinal.{u_1}
IH : ∀ y < a, y < c.ord → preBeth y < c
ha : a < c.ord
⊢ a < c.ord

Tactic:
]

Goal state after:
c : Cardinal.{u_1}
hc : c.IsInaccessible
a : Ordinal.{u_1}
IH : ∀ y < a, y < c.ord → preBeth y < c
ha : a < c.ord
⊢ a < c.ord
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: case inj'.refine_1
α : Type u
s : Set α
c : Cardinal.{u}
t : Set α
ht1 : t ⊆ s
ht2 : #↑t ≤ c
t' : Set α
h1t' : t' ⊆ s
h2t' : #↑t' ≤ c
h : Subtype.val ⁻¹' t = Subtype.val ⁻¹' t'
⊢ t ⊆ s

Tactic:
]

Goal state after:
case inj'.refine_1
α : Type u
s : Set α
c : Cardinal.{u}
t : Set α
ht1 : t ⊆ s
ht2 : #↑t ≤ c
t' : Set α
h1t' : t' ⊆ s
h2t' : #↑t' ≤ c
h : Subtype.val ⁻¹' t = Subtype.val ⁻¹' t'
⊢ t ⊆ s
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: case inj'.refine_2
α : Type u
s : Set α
c : Cardinal.{u}
t : Set α
ht1 : t ⊆ s
ht2 : #↑t ≤ c
t' : Set α
h1t' : t' ⊆ s
h2t' : #↑t' ≤ c
h : Subtype.val ⁻¹' t = Subtype.val ⁻¹' t'
⊢ t' ⊆ s

Tactic:
]

Goal state after:
case inj'.refine_2
α : Type u
s : Set α
c : Cardinal.{u}
t : Set α
ht1 : t ⊆ s
ht2 : #↑t ≤ c
t' : Set α
h1t' : t' ⊆ s
h2t' : #↑t' ≤ c
h : Subtype.val ⁻¹' t = Subtype.val ⁻¹' t'
⊢ t' ⊆ s
Module: Mathlib.SetTheory.Cardinal.Regular

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

pp: c : Cardinal.{u_1}
hc : c.IsInaccessible
⊢ ω ^ 2 < c.ord

Tactic:
]

Goal state after:
c : Cardinal.{u_1}
hc : c.IsInaccessible
⊢ ω ^ 2 < c.ord
Module: Mathlib.SetTheory.Cardinal.Regular

Goal state before:
pp: c : Cardinal.{u_1}
hc : c.IsInaccessible
⊢ ℵ₀ < c

Tactic:
]

Goal state after:
c : Cardinal.{u_1}
hc : c.IsInaccessible
⊢ ℵ₀ < c
Module: Mathlib.SetTheory.Cardinal.Regular

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

Tactic:
]

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

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

Tactic:
]

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

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

Tactic:
]

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

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

Tactic:
]

Goal state after:
α β : Type u
inst✝ : Finite α
s : Set α
t : Set β
h1 : #α = #β
h : #↑s = #↑t
⊢ lift.{u, u} #↑sᶜ = lift.{u, u} #↑tᶜ
Module: Mathlib.SetTheory.Cardinal.Arithmetic

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

Tactic:
]

Goal state after:
case h1
α β : Type u
inst✝ : Finite α
s : Set α
t : Set β
h1 : #α = #β
h : #↑s = #↑t
⊢ #α = #β
Module: Mathlib.SetTheory.Cardinal.Arithmetic

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

Tactic:
]

Goal state after:
case h2
α β : Type u
inst✝ : Finite α
s : Set α
t : Set β
h1 : #α = #β
h : #↑s = #↑t
⊢ #↑s = #↑t
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: α : Type u
β : Type v
inst✝ : Finite α
s : Set α
f : ↑s ↪ β
h : lift.{v, u} #α = lift.{u, v} #β
⊢ Nonempty (↑sᶜ ≃ ↑(range ⇑f)ᶜ)

Tactic:
]

Goal state after:
α : Type u
β : Type v
inst✝ : Finite α
s : Set α
f : ↑s ↪ β
h : lift.{v, u} #α = lift.{u, v} #β
⊢ Nonempty (↑sᶜ ≃ ↑(range ⇑f)ᶜ)
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: α : Type u
β : Type v
inst✝ : Finite α
s : Set α
f : ↑s ↪ β
h : lift.{v, u} #α = lift.{u, v} #β
⊢ lift.{u, v} #↑?m.24ᶜ = lift.{u, v} #↑(range ⇑f)ᶜ

pp: α : Type u
β : Type v
inst✝ : Finite α
s : Set α
f : ↑s ↪ β
h : lift.{v, u} #α = lift.{u, v} #β
⊢ lift.{v, u} #↑s = lift.{u, v} #↑?m.24

pp: α : Type u
β : Type v
inst✝ : Finite α
s : Set α
f : ↑s ↪ β
h : lift.{v, u} #α = lift.{u, v} #β
⊢ Set β

Tactic:
]

Goal state after:
α : Type u
β : Type v
inst✝ : Finite α
s : Set α
f : ↑s ↪ β
h : lift.{v, u} #α = lift.{u, v} #β
⊢ lift.{v, u} #↑s = lift.{u, v} #↑(range ⇑f)
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: α : Type u
β : Type v
inst✝ : Finite α
s : Set α
f : ↑s ↪ β
h : lift.{v, u} #α = lift.{u, v} #β
⊢ lift.{v, u} #↑s = lift.{v, u} #↑s

pp: α : Type u
β : Type v
inst✝ : Finite α
s : Set α
f : ↑s ↪ β
h : lift.{v, u} #α = lift.{u, v} #β
⊢ Injective ⇑f

Tactic:
]

Goal state after:
α : Type u
β : Type v
inst✝ : Finite α
s : Set α
f : ↑s ↪ β
h : lift.{v, u} #α = lift.{u, v} #β
⊢ Injective ⇑f
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: case inr
α : Type u_1
β : Type u_2
s : Set α
f : ↑s ↪ β
hs : #↑s < #α
h : lift.{u_2, u_1} #α = lift.{u_1, u_2} #β
val✝ : Infinite α
g : α ≃ β
this : Infinite β
⊢ lift.{u_2, u_1} #↑sᶜ = lift.{u_1, u_2} #↑(range ⇑f)ᶜ

Tactic:
]

Goal state after:
case inr
α : Type u_1
β : Type u_2
s : Set α
f : ↑s ↪ β
hs : #↑s < #α
h : lift.{u_2, u_1} #α = lift.{u_1, u_2} #β
val✝ : Infinite α
g : α ≃ β
this : Infinite β
⊢ lift.{u_2, u_1} #↑sᶜ = lift.{u_1, u_2} #↑(range ⇑f)ᶜ
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: case inr
α : Type u_1
β : Type u_2
s : Set α
f : ↑s ↪ β
hs : #↑s < #α
h : lift.{u_2, u_1} #α = lift.{u_1, u_2} #β
val✝ : Infinite α
g : α ≃ β
this : Infinite β
⊢ lift.{u_2, u_1} #α = lift.{u_1, u_2} #β

pp: case inr.h2
α : Type u_1
β : Type u_2
s : Set α
f : ↑s ↪ β
hs : #↑s < #α
h : lift.{u_2, u_1} #α = lift.{u_1, u_2} #β
val✝ : Infinite α
g : α ≃ β
this : Infinite β
⊢ #↑(range ⇑f) < #β

Tactic:
]

Goal state after:
case inr
α : Type u_1
β : Type u_2
s : Set α
f : ↑s ↪ β
hs : #↑s < #α
h : lift.{u_2, u_1} #α = lift.{u_1, u_2} #β
val✝ : Infinite α
g : α ≃ β
this : Infinite β
⊢ lift.{u_2, u_1} #α = lift.{u_1, u_2} #β

case inr.h2
α : Type u_1
β : Type u_2
s : Set α
f : ↑s ↪ β
hs : #↑s < #α
h : lift.{u_2, u_1} #α = lift.{u_1, u_2} #β
val✝ : Infinite α
g : α ≃ β
this : Infinite β
⊢ #↑(range ⇑f) < #β
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: case inr.h2
α : Type u_1
β : Type u_2
s : Set α
f : ↑s ↪ β
hs : #↑s < #α
h : lift.{u_2, u_1} #α = lift.{u_1, u_2} #β
val✝ : Infinite α
g : α ≃ β
this : Infinite β
⊢ #↑s < #α

Tactic:
]

Goal state after:
case inr.h2
α : Type u_1
β : Type u_2
s : Set α
f : ↑s ↪ β
hs : #↑s < #α
h : lift.{u_2, u_1} #α = lift.{u_1, u_2} #β
val✝ : Infinite α
g : α ≃ β
this : Infinite β
⊢ #↑s < #α
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
⊢ (f.sum fun x ↦ ⇑(g x)) ∈ s

Tactic:
]

Goal state after:
ι : 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
⊢ (f.sum fun x ↦ ⇑(g x)) ∈ s
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) = f i (x i)

Tactic:
]

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

Goal state before:
pp: case a
ι : Type u
γ : Type w
inst✝² : DecidableEq ι
p : ι → Prop
inst✝¹ : DecidablePred p
inst✝ : AddCommMonoid γ
S : ι → AddSubmonoid γ
i : ι
hi : p i
y : γ
hy : y ∈ S i
⊢ (sumAddHom fun i ↦ (S i).subtype) (single i ⟨y, hy⟩) = y

Tactic:
]

Goal state after:
case a
ι : Type u
γ : Type w
inst✝² : DecidableEq ι
p : ι → Prop
inst✝¹ : DecidablePred p
inst✝ : AddCommMonoid γ
S : ι → AddSubmonoid γ
i : ι
hi : p i
y : γ
hy : y ∈ S i
⊢ (sumAddHom fun i ↦ (S i).subtype) (single i ⟨y, hy⟩) = y
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 : γ
⊢ (∃ f, (sumAddHom fun i ↦ (S i).subtype) f = x) ↔ ∃ f, (f.sum fun x xi ↦ ↑xi) = x

Tactic:
]

Goal state after:
ι : Type u
γ : Type w
inst✝² : DecidableEq ι
inst✝¹ : AddCommMonoid γ
S : ι → AddSubmonoid γ
inst✝ : (i : ι) → (x : ↥(S i)) → Decidable (x ≠ 0)
x : γ
⊢ (∃ f, (sumAddHom fun i ↦ (S i).subtype) f = x) ↔ ∃ f, (f.sum fun x xi ↦ ↑xi) = x
Module: Mathlib.Data.DFinsupp.Defs

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

Tactic:
]

Goal state after:
ι : Type u
β : ι → Type v
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : DecidableEq ι
i i' : ι
b : β i
⊢ (if h : i' = i then ⋯ ▸ b else 0 i') = if h : i = i' then Eq.recOn h b else 0
Module: Mathlib.Data.DFinsupp.Defs

Goal state before:
pp: case neg
ι : Type u
β : ι → Type v
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : DecidableEq ι
i j : ι
xi : β i
xj : β j
h : single i xi = single j xj
hij : ¬i = j
h_coe : ⇑(single i xi) = ⇑(single j xj)
hci : xi = (single j xj) i
hcj : (single i xi) j = xj
⊢ i = j ∧ xi ≍ xj ∨ xi = 0 ∧ xj = 0

Tactic:
]

Goal state after:
case neg
ι : Type u
β : ι → Type v
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : DecidableEq ι
i j : ι
xi : β i
xj : β j
h : single i xi = single j xj
hij : ¬i = j
h_coe : ⇑(single i xi) = ⇑(single j xj)
hci : xi = (single j xj) i
hcj : (single i xi) j = xj
⊢ i = j ∧ xi ≍ xj ∨ xi = 0 ∧ xj = 0
Module: Mathlib.Data.DFinsupp.Defs

Goal state before:
pp: case neg
ι : Type u
β : ι → Type v
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : DecidableEq ι
i j : ι
xi : β i
xj : β j
h : single i xi = single j xj
hij : ¬i = j
h_coe : ⇑(single i xi) = ⇑(single j xj)
hci : xi = 0
hcj : (single i xi) j = xj
⊢ i = j ∧ xi ≍ xj ∨ xi = 0 ∧ xj = 0

Tactic:
]

Goal state after:
case neg
ι : Type u
β : ι → Type v
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : DecidableEq ι
i j : ι
xi : β i
xj : β j
h : single i xi = single j xj
hij : ¬i = j
h_coe : ⇑(single i xi) = ⇑(single j xj)
hci : xi = 0
hcj : (single i xi) j = xj
⊢ i = j ∧ xi ≍ xj ∨ xi = 0 ∧ xj = 0
Module: Mathlib.Data.DFinsupp.Defs

Goal state before:
pp: case neg
ι : Type u
β : ι → Type v
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : DecidableEq ι
i j : ι
xi : β i
xj : β j
h : single i xi = single j xj
hij : ¬i = j
h_coe : ⇑(single i xi) = ⇑(single j xj)
hci : xi = 0
hcj : 0 = xj
⊢ i = j ∧ xi ≍ xj ∨ xi = 0 ∧ xj = 0

Tactic:
]

Goal state after:
case neg
ι : Type u
β : ι → Type v
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : DecidableEq ι
i j : ι
xi : β i
xj : β j
h : single i xi = single j xj
hij : ¬i = j
h_coe : ⇑(single i xi) = ⇑(single j xj)
hci : xi = 0
hcj : 0 = xj
⊢ i = j ∧ xi ≍ xj ∨ xi = 0 ∧ xj = 0
Module: Mathlib.Data.DFinsupp.Defs

Goal state before:
pp: case mpr.inl
ι : Type u
β : ι → Type v
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : DecidableEq ι
i : ι
xi xj : β i
hxi : xi ≍ xj
⊢ single i xj = single i xj

Tactic:
]

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

Goal state before:
pp: case mpr.inr
ι : Type u
β : ι → Type v
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : DecidableEq ι
i j : ι
xi : β i
xj : β j
hi : xi = 0
hj : xj = 0
⊢ 0 = 0

Tactic:
]

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
⊢ i = i ∧ xi ≍ 0 ∨ xi = 0 ∧ 0 = 0 ↔ xi = 0

Tactic:
]

Goal state after:
ι : Type u
β : ι → Type v
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : DecidableEq ι
i : ι
xi : β i
⊢ i = i ∧ xi ≍ 0 ∨ xi = 0 ∧ 0 = 0 ↔ xi = 0
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
⊢ single i x = single i x

Tactic:
]

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
⊢ 0 = 0

Tactic:
]

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

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

Tactic:
]

Goal state after:
ι : Type u
β : ι → Type v
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : DecidableEq ι
f : Π₀ (i : ι), β i
i i✝ : ι
⊢ (if i = i✝ then f i✝ else 0) = if h : i = i✝ then Eq.recOn h (f i) else 0
Module: Mathlib.Data.DFinsupp.Defs

Goal state before:
pp: ι : Type u
β : ι → Type v
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : DecidableEq ι
x : Π₀ (i : ι), β i
i j : ι
⊢ (if j ∈ {i} then (single i (x i)) j else (erase i x) j) = x j

Tactic:
]

Goal state after:
ι : Type u
β : ι → Type v
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : DecidableEq ι
x : Π₀ (i : ι), β i
i j : ι
⊢ (if j ∈ {i} then (single i (x i)) j else (erase i x) j) = x j
Module: Mathlib.Data.DFinsupp.Defs

Goal state before:
pp: case pos
ι : Type u
β : ι → Type v
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : DecidableEq ι
x : Π₀ (i : ι), β i
i j : ι
h : j ∈ {i}
⊢ x i = x i

Tactic:
]

Goal state after: