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

Goal state before:
pp: case h.mpr
α : Type u
inst✝ : Infinite α
β : Type u
s : Set α
g : ↑s ↪ β
x : α
⊢ x ∈ ↑⟨s, ⋯⟩ →
    x ∈
      ↑((fun f ↦ ⟨Sum.inl ⁻¹' range f, ⋯⟩) fun y ↦
          if h : ∃ x, g x = y then Sum.inl ↑(Classical.choose h) else Sum.inr { down := 0 })

Tactic:
·

Goal state after:
case h.mpr
α : Type u
inst✝ : Infinite α
β : Type u
s : Set α
g : ↑s ↪ β
x : α
⊢ x ∈ ↑⟨s, ⋯⟩ →
    x ∈
      ↑((fun f ↦ ⟨Sum.inl ⁻¹' range f, ⋯⟩) fun y ↦
          if h : ∃ x, g x = y then Sum.inl ↑(Classical.choose h) else Sum.inr { down := 0 })
Module: Mathlib.SetTheory.Cardinal.Regular

Goal state before:
pp: case limit.hf
ι : 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
⊢ ∀ (i : ↑(Iio b)), derivFamily f ↑i < c.ord

Tactic:
·

Goal state after:
case limit.hf
ι : 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
⊢ ∀ (i : ↑(Iio b)), derivFamily f ↑i < c.ord
Module: Mathlib.SetTheory.Cardinal.Regular

Goal state before:
pp: case inl
c : Cardinal.{u_1}
hc : c < ℵ₀
⊢ ¬(succ c).IsSingular

pp: case inr
c : Cardinal.{u_1}
hc : ℵ₀ ≤ c
⊢ ¬(succ c).IsSingular

Tactic:
·

Goal state after:
case inl
c : Cardinal.{u_1}
hc : c < ℵ₀
⊢ ¬(succ c).IsSingular
Module: Mathlib.SetTheory.Cardinal.Regular

Goal state before:
pp: case inr
c : Cardinal.{u_1}
hc : ℵ₀ ≤ c
⊢ ¬(succ c).IsSingular

Tactic:
·

Goal state after:
case inr
c : Cardinal.{u_1}
hc : ℵ₀ ≤ c
⊢ ¬(succ 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:
·

Goal state after:
α : Type u
c : Cardinal.{u}
⊢ #{ t // #↑t ≤ c } ≤ #{ t // #↑t ≤ c }
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: case refine_1
α : Type u
c : Cardinal.{u}
⊢ Set α ↪ Set (ULift.{u, 0} ℕ ⊕ α)

pp: case refine_2
α : Type u
c : Cardinal.{u}
⊢ ∀ ⦃x : Set α⦄, #↑x ≤ c → #↑(?refine_1 x) ≤ c

Tactic:
·

Goal state after:
case refine_1
α : Type u
c : Cardinal.{u}
⊢ Set α ↪ Set (ULift.{u, 0} ℕ ⊕ α)
Module: Mathlib.SetTheory.Cardinal.Regular

Goal state before:
pp: case inl
⊢ (ℵ_ 0).IsSingular ↔ IsSuccLimit 0 ∧ Ordinal.cof 0 < ℵ_ 0

pp: case inr.inl
a : Ordinal.{u_1}
⊢ (ℵ_ (succ a)).IsSingular ↔ IsSuccLimit (succ a) ∧ (succ a).cof < ℵ_ (succ a)

pp: case inr.inr
o : Ordinal.{u_1}
ho : IsSuccLimit o
⊢ (ℵ_ o).IsSingular ↔ IsSuccLimit o ∧ o.cof < ℵ_ o

Tactic:
·

Goal state after:
case inl
⊢ (ℵ_ 0).IsSingular ↔ IsSuccLimit 0 ∧ Ordinal.cof 0 < ℵ_ 0
Module: Mathlib.SetTheory.Cardinal.Regular

Goal state before:
pp: case inr.inl
a : Ordinal.{u_1}
⊢ (ℵ_ (succ a)).IsSingular ↔ IsSuccLimit (succ a) ∧ (succ a).cof < ℵ_ (succ a)

pp: case inr.inr
o : Ordinal.{u_1}
ho : IsSuccLimit o
⊢ (ℵ_ o).IsSingular ↔ IsSuccLimit o ∧ o.cof < ℵ_ o

Tactic:
·

Goal state after:
case inr.inl
a : Ordinal.{u_1}
⊢ (ℵ_ (succ a)).IsSingular ↔ IsSuccLimit (succ a) ∧ (succ a).cof < ℵ_ (succ a)
Module: Mathlib.SetTheory.Cardinal.Regular

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

Tactic:
·

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

Goal state before:
pp: case refine_1
α : Type u
s : Set α
c : Cardinal.{u}
⊢ { t // t ⊆ s ∧ #↑t ≤ c } ↪ Set ↑s

pp: case refine_2
α : Type u
s : Set α
c : Cardinal.{u}
⊢ ∀ (a : { t // t ⊆ s ∧ #↑t ≤ c }), ?refine_1 a ∈ fun t ↦ Quot.lift ((fun α β ↦ Nonempty (α ↪ β)) ↑t) ⋯ c

Tactic:
·

Goal state after:
case refine_1
α : Type u
s : Set α
c : Cardinal.{u}
⊢ { t // t ⊆ s ∧ #↑t ≤ c } ↪ Set ↑s
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
⊢ lift.{u_1, u_1 + 1} #↑(Iio a) < (lift.{u_1 + 1, u_1} c).ord.cof

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
⊢ ∀ (i : ↑(Iio a)), 2 ^ preBeth ↑i < c

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
⊢ lift.{u_1, u_1 + 1} #↑(Iio a) < (lift.{u_1 + 1, u_1} c).ord.cof
Module: Mathlib.LinearAlgebra.Basis.Cardinality

Goal state before:
pp: case none
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
⊢ l none = l' none

pp: case some
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 : κ
⊢ l (Option.some a) = l' (Option.some a)

Tactic:
·

Goal state after:
case none
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
⊢ l none = l' none
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
⊢ ∀ (i : ↑(Iio a)), 2 ^ preBeth ↑i < c

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
⊢ ∀ (i : ↑(Iio a)), 2 ^ preBeth ↑i < c
Module: Mathlib.LinearAlgebra.Basis.Cardinality

Goal state before:
pp: case inl
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 : κ
⊢ (b.repr ((linearCombination R v) l.some)) i = (b.repr ((linearCombination R v) l'.some)) i

pp: case inr
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 : ι
ne : i ≠ j
⊢ (b.repr ((linearCombination R v) l.some)) j = (b.repr ((linearCombination R v) l'.some)) j

Tactic:
·

Goal state after:
case inl
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 : κ
⊢ (b.repr ((linearCombination R v) l.some)) i = (b.repr ((linearCombination R v) l'.some)) i
Module: Mathlib.Data.DFinsupp.Ext

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

pp: case ha
ι : Type u
β : ι → Type v
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → AddZeroClass (β i)
x : Π₀ (i : ι), β i
x✝ : x ∈ ⊤
⊢ ∀ (i : ι) (b : β i) (f : Π₀ (i : ι), β i),
    f i = 0 →
      b ≠ 0 →
        f ∈ AddSubmonoid.closure (⋃ i, Set.range (single i)) →
          single i b + f ∈ AddSubmonoid.closure (⋃ i, Set.range (single i))

Tactic:
·

Goal state after:
case h0
ι : Type u
β : ι → Type v
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → AddZeroClass (β i)
x : Π₀ (i : ι), β i
x✝ : x ∈ ⊤
⊢ 0 ∈ AddSubmonoid.closure (⋃ i, Set.range (single i))
Module: Mathlib.SetTheory.Cardinal.Arithmetic

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

pp: case inr
α : Type u_1
β : Type u_2
s : Set α
f : ↑s ↪ β
hs : #↑s < #α
h : Nonempty (α ≃ β)
val✝ : Infinite α
⊢ ∃ g, ∀ (x : ↑s), g ↑x = f x

Tactic:
·

Goal state after:
case inl
α : Type u_1
β : Type u_2
s : Set α
f : ↑s ↪ β
hs : #↑s < #α
h : Nonempty (α ≃ β)
val✝ : Fintype α
⊢ ∃ g, ∀ (x : ↑s), g ↑x = f x
Module: Mathlib.SetTheory.Cardinal.Arithmetic

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

Tactic:
·

Goal state after:
case inr
α : Type u_1
β : Type u_2
s : Set α
f : ↑s ↪ β
hs : #↑s < #α
h : Nonempty (α ≃ β)
val✝ : Infinite α
⊢ ∃ g, ∀ (x : ↑s), g ↑x = f x
Module: Mathlib.Data.DFinsupp.Submonoid

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

pp: case a
ι : Type u
γ : Type w
inst✝¹ : DecidableEq ι
inst✝ : AddCommMonoid γ
S : ι → AddSubmonoid γ
⊢ AddMonoidHom.mrange (sumAddHom fun i ↦ (S i).subtype) ≤ iSup S

Tactic:
·

Goal state after:
case a
ι : Type u
γ : Type w
inst✝¹ : DecidableEq ι
inst✝ : AddCommMonoid γ
S : ι → AddSubmonoid γ
⊢ iSup S ≤ AddMonoidHom.mrange (sumAddHom fun i ↦ (S i).subtype)
Module: Mathlib.Data.DFinsupp.Submonoid

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

Tactic:
·

Goal state after:
case a
ι : Type u
γ : Type w
inst✝¹ : DecidableEq ι
inst✝ : AddCommMonoid γ
S : ι → AddSubmonoid γ
⊢ AddMonoidHom.mrange (sumAddHom fun i ↦ (S i).subtype) ≤ iSup S
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, ⨆ (_ : p i), S i ≤
    AddMonoidHom.mrange ((sumAddHom fun i ↦ (S i).subtype).comp (filterAddMonoidHom (fun i ↦ ↥(S i)) p))

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

Tactic:
·

Goal state after:
case a
ι : 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))
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 γ
⊢ AddMonoidHom.mrange ((sumAddHom fun i ↦ (S i).subtype).comp (filterAddMonoidHom (fun i ↦ ↥(S i)) p)) ≤
    ⨆ i, ⨆ (_ : p i), S i

Tactic:
·

Goal state after:
case a
ι : Type u
γ : Type w
inst✝² : DecidableEq ι
p : ι → Prop
inst✝¹ : DecidablePred p
inst✝ : AddCommMonoid γ
S : ι → AddSubmonoid γ
⊢ AddMonoidHom.mrange ((sumAddHom fun i ↦ (S i).subtype).comp (filterAddMonoidHom (fun i ↦ ↥(S i)) p)) ≤
    ⨆ i, ⨆ (_ : p i), S i
Module: Mathlib.Data.DFinsupp.Submonoid

Goal state before:
pp: case pos
ι : Type u
γ : Type w
inst✝² : DecidableEq ι
p : ι → Prop
inst✝¹ : DecidablePred p
inst✝ : AddCommMonoid γ
S : ι → AddSubmonoid γ
v : Π₀ (i : ι), ↥(S i)
i : ι
x✝ : ((filterAddMonoidHom (fun i ↦ ↥(S i)) p) v) i ≠ 0
hp : p i
⊢ (S i).subtype (((filterAddMonoidHom (fun i ↦ ↥(S i)) p) v) i) ∈ ⨆ (_ : p i), S i

pp: case neg
ι : Type u
γ : Type w
inst✝² : DecidableEq ι
p : ι → Prop
inst✝¹ : DecidablePred p
inst✝ : AddCommMonoid γ
S : ι → AddSubmonoid γ
v : Π₀ (i : ι), ↥(S i)
i : ι
x✝ : ((filterAddMonoidHom (fun i ↦ ↥(S i)) p) v) i ≠ 0
hp : ¬p i
⊢ (S i).subtype (((filterAddMonoidHom (fun i ↦ ↥(S i)) p) v) i) ∈ ⨆ (_ : p i), S i

Tactic:
·

Goal state after:
case pos
ι : Type u
γ : Type w
inst✝² : DecidableEq ι
p : ι → Prop
inst✝¹ : DecidablePred p
inst✝ : AddCommMonoid γ
S : ι → AddSubmonoid γ
v : Π₀ (i : ι), ↥(S i)
i : ι
x✝ : ((filterAddMonoidHom (fun i ↦ ↥(S i)) p) v) i ≠ 0
hp : p i
⊢ (S i).subtype (((filterAddMonoidHom (fun i ↦ ↥(S i)) p) v) i) ∈ ⨆ (_ : p i), S i
Module: Mathlib.Data.DFinsupp.Defs

Goal state before:
pp: case inl
ι : 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
xs : { s // ∀ (i : ι), i ∈ s ∨ x.toFun i = 0 }
ys : { s // ∀ (i : ι), i ∈ s ∨ y.toFun i = 0 }
i : ι
h1 : i ∈ ↑xs
⊢ i ∈ ↑xs + ↑ys ∨ f i (x i) (y i) = 0

pp: case inr
ι : 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
xs : { s // ∀ (i : ι), i ∈ s ∨ x.toFun i = 0 }
ys : { s // ∀ (i : ι), i ∈ s ∨ y.toFun i = 0 }
i : ι
h1 : x i = 0
⊢ i ∈ ↑xs + ↑ys ∨ f i (x i) (y i) = 0

Tactic:
·

Goal state after:
case inl
ι : 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
xs : { s // ∀ (i : ι), i ∈ s ∨ x.toFun i = 0 }
ys : { s // ∀ (i : ι), i ∈ s ∨ y.toFun i = 0 }
i : ι
h1 : i ∈ ↑xs
⊢ i ∈ ↑xs + ↑ys ∨ f i (x i) (y i) = 0
Module: Mathlib.Data.DFinsupp.Submonoid

Goal state before:
pp: case neg
ι : Type u
γ : Type w
inst✝² : DecidableEq ι
p : ι → Prop
inst✝¹ : DecidablePred p
inst✝ : AddCommMonoid γ
S : ι → AddSubmonoid γ
v : Π₀ (i : ι), ↥(S i)
i : ι
x✝ : ((filterAddMonoidHom (fun i ↦ ↥(S i)) p) v) i ≠ 0
hp : ¬p i
⊢ (S i).subtype (((filterAddMonoidHom (fun i ↦ ↥(S i)) p) v) i) ∈ ⨆ (_ : p i), S i

Tactic:
·

Goal state after:
case neg
ι : Type u
γ : Type w
inst✝² : DecidableEq ι
p : ι → Prop
inst✝¹ : DecidablePred p
inst✝ : AddCommMonoid γ
S : ι → AddSubmonoid γ
v : Π₀ (i : ι), ↥(S i)
i : ι
x✝ : ((filterAddMonoidHom (fun i ↦ ↥(S i)) p) v) i ≠ 0
hp : ¬p i
⊢ (S i).subtype (((filterAddMonoidHom (fun i ↦ ↥(S i)) p) v) i) ∈ ⨆ (_ : p i), S i
Module: Mathlib.Data.DFinsupp.Defs

Goal state before:
pp: case inr.inl
ι : 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
xs : { s // ∀ (i : ι), i ∈ s ∨ x.toFun i = 0 }
ys : { s // ∀ (i : ι), i ∈ s ∨ y.toFun i = 0 }
i : ι
h1 : x i = 0
h2 : i ∈ ↑ys
⊢ i ∈ ↑xs + ↑ys ∨ f i (x i) (y i) = 0

pp: case inr.inr
ι : 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
xs : { s // ∀ (i : ι), i ∈ s ∨ x.toFun i = 0 }
ys : { s // ∀ (i : ι), i ∈ s ∨ y.toFun i = 0 }
i : ι
h1 : x i = 0
h2 : y i = 0
⊢ i ∈ ↑xs + ↑ys ∨ f i (x i) (y i) = 0

Tactic:
·

Goal state after:
case inr.inl
ι : 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
xs : { s // ∀ (i : ι), i ∈ s ∨ x.toFun i = 0 }
ys : { s // ∀ (i : ι), i ∈ s ∨ y.toFun i = 0 }
i : ι
h1 : x i = 0
h2 : i ∈ ↑ys
⊢ i ∈ ↑xs + ↑ys ∨ f i (x i) (y i) = 0
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 : ι
⊢ ((if p i then f i else 0) + if ¬p i then f i else 0) = f i

Tactic:
split_ifs <;> simp only [add_zero, zero_add]

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

Goal state before:
pp: case mp
ι : 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

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

Tactic:
·

Goal state after:
case mp
ι : 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
Module: Mathlib.Data.DFinsupp.Defs

Goal state before:
pp: case pos
ι : 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
⊢ i = j ∧ xi ≍ xj ∨ xi = 0 ∧ xj = 0

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

Tactic:
·

Goal state after:
case pos
ι : 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
⊢ 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
⊢ 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
⊢ i = j ∧ xi ≍ xj ∨ xi = 0 ∧ xj = 0
Module: Mathlib.Data.DFinsupp.Defs

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

Tactic:
·

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

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
⊢ single i xi = single j xj

Tactic:
·

Goal state after:
case mpr.inl
ι : Type u
β : ι → Type v
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : DecidableEq ι
i : ι
xi xj : β i
hxi : xi ≍ xj
⊢ single i xi = single i xj
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
⊢ single i xi = single j xj

Tactic:
·

Goal state after:
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
⊢ single i xi = single j xj
Module: Mathlib.Data.DFinsupp.Defs

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

pp: case isFalse
ι : Type u
β : ι → Type v
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : DecidableEq ι
f : Π₀ (i : ι), β i
i i✝ : ι
h✝ : ¬i = i✝
⊢ 0 = 0

Tactic:
·

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

Goal state before:
pp: case isFalse
ι : Type u
β : ι → Type v
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : DecidableEq ι
f : Π₀ (i : ι), β i
i i✝ : ι
h✝ : ¬i = i✝
⊢ 0 = 0

Tactic:
·

Goal state after:
case isFalse
ι : Type u
β : ι → Type v
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : DecidableEq ι
f : Π₀ (i : ι), β i
i i✝ : ι
h✝ : ¬i = i✝
⊢ 0 = 0
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}
⊢ (single i (x i)) j = x j

pp: case neg
ι : Type u
β : ι → Type v
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : DecidableEq ι
x : Π₀ (i : ι), β i
i j : ι
h : j ∉ {i}
⊢ (erase i x) j = x j

Tactic:
·

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

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

Tactic:
·

Goal state after:
case neg
ι : Type u
β : ι → Type v
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : DecidableEq ι
x : Π₀ (i : ι), β i
i j : ι
h : j ∉ {i}
⊢ (erase i x) j = x j
Module: Mathlib.Data.DFinsupp.Defs

Goal state before:
pp: case inl
ι : Type u
inst✝¹ : DecidableEq ι
β : ι → Type u_1
inst✝ : (i : ι) → AddGroup (β i)
f : Π₀ (i : ι), β i
j : ι
⊢ (erase j f) j = (f - single j (f j)) j

pp: case inr
ι : Type u
inst✝¹ : DecidableEq ι
β : ι → Type u_1
inst✝ : (i : ι) → AddGroup (β i)
f : Π₀ (i : ι), β i
i j : ι
h : j ≠ i
⊢ (erase i f) j = (f - single i (f i)) j

Tactic:
·

Goal state after:
case inl
ι : Type u
inst✝¹ : DecidableEq ι
β : ι → Type u_1
inst✝ : (i : ι) → AddGroup (β i)
f : Π₀ (i : ι), β i
j : ι
⊢ (erase j f) j = (f - single j (f j)) j
Module: Mathlib.Data.DFinsupp.Defs

Goal state before:
pp: case inr
ι : Type u
inst✝¹ : DecidableEq ι
β : ι → Type u_1
inst✝ : (i : ι) → AddGroup (β i)
f : Π₀ (i : ι), β i
i j : ι
h : j ≠ i
⊢ (erase i f) j = (f - single i (f i)) j

Tactic:
·

Goal state after:
case inr
ι : Type u
inst✝¹ : DecidableEq ι
β : ι → Type u_1
inst✝ : (i : ι) → AddGroup (β i)
f : Π₀ (i : ι), β i
i j : ι
h : j ≠ i
⊢ (erase i f) j = (f - single i (f i)) j