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

Goal state before:
pp: β : Type v
o : Ordinal.{u}
c : Cardinal.{v}
ho : lift.{v, u} o.card ≤ lift.{u, v} c
hc : ℵ₀ ≤ c
A : Ordinal.{u} → Set β
hA : ∀ j < o, #↑(A j) ≤ c
⊢ #↑(sSup (range ((fun x ↦ A ↑x) ∘ ⇑ToType.mk.symm))) ≤ c

Tactic:
← lift_le.{u}

Goal state after:
β : Type v
o : Ordinal.{u}
c : Cardinal.{v}
ho : lift.{v, u} o.card ≤ lift.{u, v} c
hc : ℵ₀ ≤ c
A : Ordinal.{u} → Set β
hA : ∀ j < o, #↑(A j) ≤ c
⊢ lift.{u, v} #↑(sSup (range ((fun x ↦ A ↑x) ∘ ⇑ToType.mk.symm))) ≤ lift.{u, v} c
Module: Mathlib.SetTheory.Cardinal.Ordinal

Goal state before:
pp: o : Ordinal.{u}
c : Cardinal.{v}
f : ↑(Iio o) → Ordinal.{v}
hι : Cardinal.lift.{v, u} o.card ≤ Cardinal.lift.{u, v} c
hf : ∀ (i : ↑(Iio o)), (f i).card ≤ c
| Cardinal.lift.{u + 1, v} c

Tactic:
← Cardinal.lift_lift.{u, u + 1}

Goal state after:
o : Ordinal.{u}
c : Cardinal.{v}
f : ↑(Iio o) → Ordinal.{v}
hι : Cardinal.lift.{v, u} o.card ≤ Cardinal.lift.{u, v} c
hf : ∀ (i : ↑(Iio o)), (f i).card ≤ c
| Cardinal.lift.{u + 1, max u v} (Cardinal.lift.{u, v} c)
Module: Mathlib.SetTheory.Cardinal.Arithmetic

Goal state before:
pp: a b c : Cardinal.{u_1}
hc : c < ℵ₀
⊢ a + c < b + c ↔ a < b

Tactic:
constructor

Goal state after:
case mp
a b c : Cardinal.{u_1}
hc : c < ℵ₀
⊢ a + c < b + c → a < b

case mpr
a b c : Cardinal.{u_1}
hc : c < ℵ₀
⊢ a < b → a + c < b + c
Module: Mathlib.SetTheory.Ordinal.FundamentalSequence

Goal state before:
pp: case refine_2
f : Ordinal.{u} → Ordinal.{u}
hf : IsNormal f
a o : Ordinal.{u}
ha : IsSuccLimit a
g : (b : Ordinal.{u}) → b < o → Ordinal.{u}
hg : a.IsFundamentalSequence o g
⊢ (o.blsub fun b hb ↦ f (g b hb)) = f a

Tactic:
@blsub_comp.{u, u, u} a _ (fun b _ => f b) (@fun i j _ _ h => hf.strictMono.monotone h) g
        hg.2.2

Goal state after:
case refine_2
f : Ordinal.{u} → Ordinal.{u}
hf : IsNormal f
a o : Ordinal.{u}
ha : IsSuccLimit a
g : (b : Ordinal.{u}) → b < o → Ordinal.{u}
hg : a.IsFundamentalSequence o g
⊢ (a.blsub fun b x ↦ f b) = f a
Module: Mathlib.SetTheory.Cardinal.Regular

Goal state before:
pp: κ : Cardinal.{v}
h₁ : ℵ₀ ≤ κ
h₂ : κ ≤ κ.ord.cof
⊢ (Cardinal.lift.{u, v} κ).IsRegular

Tactic:
constructor

Goal state after:
case aleph0_le
κ : Cardinal.{v}
h₁ : ℵ₀ ≤ κ
h₂ : κ ≤ κ.ord.cof
⊢ ℵ₀ ≤ Cardinal.lift.{u, v} κ

case le_cof_ord
κ : Cardinal.{v}
h₁ : ℵ₀ ≤ κ
h₂ : κ ≤ κ.ord.cof
⊢ Cardinal.lift.{u, v} κ ≤ (Cardinal.lift.{u, v} κ).ord.cof
Module: Mathlib.SetTheory.Cardinal.Cofinality.Ordinal

Goal state before:
pp: case inl
α : Type u_1
h : (#α).IsStrongPrelimit
r : α → α → Prop
inst✝ : IsWellOrder α r
hr : (#α).ord = type r
ha : #α = 0
this : IsEmpty α
⊢ IsEmpty { s // Bounded r s }

Tactic:
constructor

Goal state after:
case inl
α : Type u_1
h : (#α).IsStrongPrelimit
r : α → α → Prop
inst✝ : IsWellOrder α r
hr : (#α).ord = type r
ha : #α = 0
this : IsEmpty α
⊢ ∀ (a : { s // Bounded r s }), False
Module: Mathlib.SetTheory.Cardinal.Pigeonhole

Goal state before:
pp: β α : Type u
f : β → α
h : #α < #β
hβ : ℵ₀ ≤ #β
hα : #α < ℵ₀
⊢ #α < ℵ₀.ord.cof

Tactic:
rwa [isRegular_aleph0.cof_ord]

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

Goal state before:
pp: β α : Type u
f : β → α
h : #α < #β
inst✝ : Infinite β
hα : #α < ℵ₀
⊢ #α < ℵ₀.ord.cof

Tactic:
rwa [isRegular_aleph0.cof_ord]

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

Goal state before:
pp: case h
α : Type u
inst✝ : Infinite α
β : Type u
s : Set α
g : ↑s ↪ β
x : α
⊢ 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 }) ↔
    x ∈ ↑⟨s, ⋯⟩

Tactic:
constructor

Goal state after:
case h.mp
α : Type u
inst✝ : Infinite α
β : Type u
s : Set α
g : ↑s ↪ β
x : α
⊢ 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 }) →
    x ∈ ↑⟨s, ⋯⟩

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

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

Tactic:
rw [dif_neg h'] at h
      cases h

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}
hω : ℵ₀ < c.ord.cof
⊢ a < c.ord → derivFamily f a < c.ord

Tactic:
induction a using limitRecOn with

Goal state after:
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 β
⊢ lift.{?u.48, u_2} #↑(range ⇑f) < lift.{?u.48, u_2} #β

Tactic:
mk_range_eq_of_injective f.injective,

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 β
⊢ lift.{u_2, u_1} #↑s < lift.{u_1, u_2} #β
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:
ext

Goal state after:
ι : Type u
β₁ : ι → Type v₁
inst✝ : (i : ι) → Zero (β₁ i)
h : ∀ (i : ι), id 0 = 0
g : Π₀ (i : ι), β₁ i
i✝ : ι
⊢ (mapRange (fun i ↦ id) h g) i✝ = g i✝
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:
ext

Goal state after:
ι : 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
i✝ : ι
⊢ (mapRange (fun i ↦ f i ∘ f₂ i) h g) i✝ = (mapRange f hf (mapRange f₂ hf₂ g)) i✝
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:
ext

Goal state after:
ι : Type u
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst✝¹ : (i : ι) → Zero (β₁ i)
inst✝ : (i : ι) → Zero (β₂ i)
f : (i : ι) → β₁ i → β₂ i
hf : ∀ (i : ι), f i 0 = 0
i✝ : ι
⊢ (mapRange f hf 0) i✝ = 0 i✝
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:
ext

Goal state after:
ι : Type u
β : ι → Type v
inst✝¹ : (i : ι) → Zero (β i)
p : ι → Prop
inst✝ : DecidablePred p
i✝ : ι
⊢ (filter p 0) i✝ = 0 i✝
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:
ext

Goal state after:
ι : Type u
β : ι → Type v
inst✝¹ : (i : ι) → AddZeroClass (β i)
p : ι → Prop
inst✝ : DecidablePred p
f g : Π₀ (i : ι), β i
i✝ : ι
⊢ (filter p (f + g)) i✝ = (filter p f + filter p g) i✝
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:
constructor

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

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: ι : Type u
β : ι → Type v
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : DecidableEq ι
f : Π₀ (i : ι), β i
i : ι
⊢ filter (fun x ↦ i = x) f = single i (f i)

Tactic:
ext

Goal state after:
ι : Type u
β : ι → Type v
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : DecidableEq ι
f : Π₀ (i : ι), β i
i i✝ : ι
⊢ (filter (fun x ↦ i = x) f) i✝ = (single i (f i)) i✝
Module: Mathlib.Data.DFinsupp.Module

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

Tactic:
ext

Goal state after:
ι : Type u
γ : Type w
β : ι → Type v
inst✝² : (i : ι) → Zero (β i)
inst✝¹ : (i : ι) → SMulZeroClass γ (β i)
p : ι → Prop
inst✝ : DecidablePred p
r : γ
f : Π₀ (i : ι), β i
i✝ : ι
⊢ (filter p (r • f)) i✝ = (r • filter p f) i✝
Module: Mathlib.Data.DFinsupp.Module

Goal state before:
pp: ι : Type u
γ : Type w
β : ι → Type v
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : (i : ι) → SMulZeroClass γ (β i)
s : Finset ι
c : γ
x : (i : ↑↑s) → β ↑i
i : ι
⊢ (if H : i ∈ s then (c • x) ⟨i, H⟩ else 0) = c • if H : i ∈ s then x ⟨i, H⟩ else 0

Tactic:
split_ifs <;> [rfl; rw [smul_zero]]

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 : ι
⊢ f.update i (f i) = f

Tactic:
ext

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

Goal state before:
pp: ι : Type u
γ : Type w
β : ι → Type v
κ : Type u_1
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : (i : ι) → SMulZeroClass γ (β i)
h : κ → ι
hh : Function.Injective h
r : γ
f : Π₀ (i : ι), β i
⊢ comapDomain h hh (r • f) = r • comapDomain h hh f

Tactic:
ext

Goal state after:
ι : Type u
γ : Type w
β : ι → Type v
κ : Type u_1
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : (i : ι) → SMulZeroClass γ (β i)
h : κ → ι
hh : Function.Injective h
r : γ
f : Π₀ (i : ι), β i
i✝ : κ
⊢ (comapDomain h hh (r • f)) i✝ = (r • comapDomain h hh f) i✝
Module: Mathlib.Data.DFinsupp.Module

Goal state before:
pp: ι : Type u
γ : Type w
β : ι → Type v
κ : Type u_1
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : (i : ι) → SMulZeroClass γ (β i)
h : κ → ι
h' : ι → κ
hh' : Function.LeftInverse h' h
r : γ
f : Π₀ (i : ι), β i
⊢ comapDomain' h hh' (r • f) = r • comapDomain' h hh' f

Tactic:
ext

Goal state after:
ι : Type u
γ : Type w
β : ι → Type v
κ : Type u_1
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : (i : ι) → SMulZeroClass γ (β i)
h : κ → ι
h' : ι → κ
hh' : Function.LeftInverse h' h
r : γ
f : Π₀ (i : ι), β i
i✝ : κ
⊢ (comapDomain' h hh' (r • f)) i✝ = (r • comapDomain' h hh' f) i✝
Module: Mathlib.Data.DFinsupp.Defs

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

Tactic:
simp only [mk_apply]; split_ifs <;> rfl

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

Goal state before:
pp: ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
f : Π₀ (i : ι), β i
sx : Multiset ι
hx : ∀ (i : ι), i ∈ sx ∨ f.toFun i = 0
sy : Multiset ι
hy : ∀ (i : ι), i ∈ sy ∨ f.toFun i = 0
i : ι
⊢ i ∈ {i ∈ sx.toFinset | f i ≠ 0} ↔ i ∈ {i ∈ sy.toFinset | f i ≠ 0}

Tactic:
constructor

Goal state after:
case mp
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
f : Π₀ (i : ι), β i
sx : Multiset ι
hx : ∀ (i : ι), i ∈ sx ∨ f.toFun i = 0
sy : Multiset ι
hy : ∀ (i : ι), i ∈ sy ∨ f.toFun i = 0
i : ι
⊢ i ∈ {i ∈ sx.toFinset | f i ≠ 0} → i ∈ {i ∈ sy.toFinset | f i ≠ 0}

case mpr
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
f : Π₀ (i : ι), β i
sx : Multiset ι
hx : ∀ (i : ι), i ∈ sx ∨ f.toFun i = 0
sy : Multiset ι
hy : ∀ (i : ι), i ∈ sy ∨ f.toFun i = 0
i : ι
⊢ i ∈ {i ∈ sy.toFinset | f i ≠ 0} → i ∈ {i ∈ sx.toFinset | f i ≠ 0}
Module: Mathlib.Data.DFinsupp.Sigma

Goal state before:
pp: case h
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
κ : Type u_1
α : ι → Type u_2
δ : (i : ι) → α i → Type v
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → (j : α i) → Zero (δ i j)
f : Π₀ (i : ι) (j : α i), δ i j
s : { s // ∀ (i : ι), i ∈ s ∨ f.toFun i = 0 }
fs : (i : ↥(↑s).toFinset) → { s_1 // ∀ (i_1 : α ↑i), i_1 ∈ s_1 ∨ (f ↑i).toFun i_1 = 0 }
i : ι
a : α i
hi : i ∈ ↑s
ha : a ∈ ↑(fs ⟨i, ⋯⟩)
⊢ ⟨i, ⋯⟩ ∈ (↑s).toFinset.attach.val ∧ ⟨i, a⟩ ∈ Multiset.map (Sigma.mk ↑⟨i, ⋯⟩) ↑(fs ⟨i, ⋯⟩)

Tactic:
constructor

Goal state after:
case h.left
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
κ : Type u_1
α : ι → Type u_2
δ : (i : ι) → α i → Type v
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → (j : α i) → Zero (δ i j)
f : Π₀ (i : ι) (j : α i), δ i j
s : { s // ∀ (i : ι), i ∈ s ∨ f.toFun i = 0 }
fs : (i : ↥(↑s).toFinset) → { s_1 // ∀ (i_1 : α ↑i), i_1 ∈ s_1 ∨ (f ↑i).toFun i_1 = 0 }
i : ι
a : α i
hi : i ∈ ↑s
ha : a ∈ ↑(fs ⟨i, ⋯⟩)
⊢ ⟨i, ⋯⟩ ∈ (↑s).toFinset.attach.val

case h.right
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
κ : Type u_1
α : ι → Type u_2
δ : (i : ι) → α i → Type v
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → (j : α i) → Zero (δ i j)
f : Π₀ (i : ι) (j : α i), δ i j
s : { s // ∀ (i : ι), i ∈ s ∨ f.toFun i = 0 }
fs : (i : ↥(↑s).toFinset) → { s_1 // ∀ (i_1 : α ↑i), i_1 ∈ s_1 ∨ (f ↑i).toFun i_1 = 0 }
i : ι
a : α i
hi : i ∈ ↑s
ha : a ∈ ↑(fs ⟨i, ⋯⟩)
⊢ ⟨i, a⟩ ∈ Multiset.map (Sigma.mk ↑⟨i, ⋯⟩) ↑(fs ⟨i, ⋯⟩)
Module: Mathlib.Data.DFinsupp.Defs

Goal state before:
pp: ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
f : Π₀ (i : ι), β i
i : ι
⊢ ↑((fun f_1 ↦ ⟨mk f.support fun i ↦ ↑(f_1 i), ⋯⟩)
          ((fun x ↦
              match (motive := { f_1 // f_1.support = f.support } → (i : ↥f.support) → { x // x ≠ 0 }) x with
              | ⟨f_1, hf⟩ => fun x ↦
                match x with
                | ⟨i, hi⟩ => ⟨f_1 i, ⋯⟩)
            ⟨f, ⋯⟩))
      i =
    ↑⟨f, ⋯⟩ i

Tactic:
simpa using Eq.symm

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

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

Tactic:
constructor

Goal state after:
case mp
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst✝³ : DecidableEq ι
inst✝² : (i : ι) → Zero (β i)
inst✝¹ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
inst✝ : (i : ι) → (x : β i) → Decidable (x = 0)
f : Π₀ (i : ι), β i
s : { s // ∀ (i : ι), i ∈ s ∨ f.toFun i = 0 }
⊢ (∀ i ∈ ↑s, f i = 0) → f = 0

case mpr
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst✝³ : DecidableEq ι
inst✝² : (i : ι) → Zero (β i)
inst✝¹ : (i : ι) → (x : β i) → Decidable (x ≠ 0)
inst✝ : (i : ι) → (x : β i) → Decidable (x = 0)
f : Π₀ (i : ι), β i
s : { s // ∀ (i : ι), i ∈ s ∨ f.toFun i = 0 }
⊢ f = 0 → ∀ i ∈ ↑s, f i = 0
Module: Mathlib.Data.Finsupp.ToDFinsupp

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝¹ : DecidableEq ι
inst✝ : Zero M
i : ι
m : M
⊢ (single i m).toDFinsupp = DFinsupp.single i m

Tactic:
ext

Goal state after:
ι : Type u_1
M : Type u_3
inst✝¹ : DecidableEq ι
inst✝ : Zero M
i : ι
m : M
i✝ : ι
⊢ (single i m).toDFinsupp i✝ = (DFinsupp.single i m) i✝
Module: Mathlib.Data.Finsupp.ToDFinsupp

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝² : DecidableEq ι
inst✝¹ : Zero M
inst✝ : (m : M) → Decidable (m ≠ 0)
f : ι →₀ M
⊢ f.toDFinsupp.support = f.support

Tactic:
ext

Goal state after:
ι : Type u_1
M : Type u_3
inst✝² : DecidableEq ι
inst✝¹ : Zero M
inst✝ : (m : M) → Decidable (m ≠ 0)
f : ι →₀ M
a✝ : ι
⊢ a✝ ∈ f.toDFinsupp.support ↔ a✝ ∈ f.support
Module: Mathlib.Data.Finsupp.ToDFinsupp

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝² : DecidableEq ι
inst✝¹ : Zero M
inst✝ : (m : M) → Decidable (m ≠ 0)
f : Π₀ (x : ι), M
⊢ f.toFinsupp.support = f.support

Tactic:
ext

Goal state after:
ι : Type u_1
M : Type u_3
inst✝² : DecidableEq ι
inst✝¹ : Zero M
inst✝ : (m : M) → Decidable (m ≠ 0)
f : Π₀ (x : ι), M
a✝ : ι
⊢ a✝ ∈ f.toFinsupp.support ↔ a✝ ∈ f.support
Module: Mathlib.Data.Finsupp.ToDFinsupp

Goal state before:
pp: ι : Type u_1
M : Type u_3
inst✝² : DecidableEq ι
inst✝¹ : Zero M
inst✝ : (m : M) → Decidable (m ≠ 0)
i : ι
m : M
⊢ (single i m).toFinsupp = Finsupp.single i m

Tactic:
ext

Goal state after:
ι : Type u_1
M : Type u_3
inst✝² : DecidableEq ι
inst✝¹ : Zero M
inst✝ : (m : M) → Decidable (m ≠ 0)
i : ι
m : M
a✝ : ι
⊢ (single i m).toFinsupp a✝ = (Finsupp.single i m) a✝
Module: Mathlib.Data.Finsupp.ToDFinsupp

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
η : ι → Type u_4
N : Type u_5
inst✝¹ : Semiring R
inst✝ : Zero N
f : (i : ι) × η i →₀ N
⊢ (fun f ↦ onFinset (f.support.sigma fun j ↦ (f j).support) (fun ji ↦ (f ji.fst) ji.snd) ⋯)
      ((fun f ↦ { toFun := f.split, support' := Trunc.mk ⟨f.splitSupport.val, ⋯⟩ }) f) =
    f

Tactic:
ext

Goal state after:
ι : Type u_1
R : Type u_2
M : Type u_3
η : ι → Type u_4
N : Type u_5
inst✝¹ : Semiring R
inst✝ : Zero N
f : (i : ι) × η i →₀ N
a✝ : (i : ι) × η i
⊢ ((fun f ↦ onFinset (f.support.sigma fun j ↦ (f j).support) (fun ji ↦ (f ji.fst) ji.snd) ⋯)
        ((fun f ↦ { toFun := f.split, support' := Trunc.mk ⟨f.splitSupport.val, ⋯⟩ }) f))
      a✝ =
    f a✝
Module: Mathlib.Data.Finsupp.ToDFinsupp

Goal state before:
pp: ι : Type u_1
R : Type u_2
M : Type u_3
η : ι → Type u_4
N : Type u_5
inst✝¹ : Semiring R
inst✝ : Zero N
f : Π₀ (i : ι), η i →₀ N
⊢ (fun f ↦ { toFun := f.split, support' := Trunc.mk ⟨f.splitSupport.val, ⋯⟩ })
      ((fun f ↦ onFinset (f.support.sigma fun j ↦ (f j).support) (fun ji ↦ (f ji.fst) ji.snd) ⋯) f) =
    f

Tactic:
ext

Goal state after:
ι : Type u_1
R : Type u_2
M : Type u_3
η : ι → Type u_4
N : Type u_5
inst✝¹ : Semiring R
inst✝ : Zero N
f : Π₀ (i : ι), η i →₀ N
i✝ : ι
a✝ : η i✝
⊢ (((fun f ↦ { toFun := f.split, support' := Trunc.mk ⟨f.splitSupport.val, ⋯⟩ })
          ((fun f ↦ onFinset (f.support.sigma fun j ↦ (f j).support) (fun ji ↦ (f ji.fst) ji.snd) ⋯) f))
        i✝)
      a✝ =
    (f i✝) a✝
Module: Mathlib.Data.Finsupp.ToDFinsupp

Goal state before:
pp: ι : Type u_1
η : ι → Type u_4
N : Type u_5
inst✝² : DecidableEq ι
inst✝¹ : Zero N
inst✝ : (i : ι) → (x : η i →₀ N) → Decidable (x ≠ 0)
f : (i : ι) × η i →₀ N
⊢ (sigmaFinsuppEquivDFinsupp f).support = f.splitSupport

Tactic:
ext

Goal state after:
ι : Type u_1
η : ι → Type u_4
N : Type u_5
inst✝² : DecidableEq ι
inst✝¹ : Zero N
inst✝ : (i : ι) → (x : η i →₀ N) → Decidable (x ≠ 0)
f : (i : ι) × η i →₀ N
a✝ : ι
⊢ a✝ ∈ (sigmaFinsuppEquivDFinsupp f).support ↔ a✝ ∈ f.splitSupport
Module: Mathlib.Data.DFinsupp.Defs

Goal state before:
pp: ι : Type u
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst✝³ : DecidableEq ι
inst✝² : (i : ι) → Zero (β₁ i)
inst✝¹ : (i : ι) → Zero (β₂ i)
inst✝ : (i : ι) → (x : β₁ i) → Decidable (x ≠ 0)
f : (i : ι) → β₁ i → β₂ i
hf : ∀ (i : ι), f i 0 = 0
g : Π₀ (i : ι), β₁ i
⊢ mapRange f hf g = mk g.support fun i ↦ f (↑i) (g ↑i)

Tactic:
ext

Goal state after:
ι : Type u
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst✝³ : DecidableEq ι
inst✝² : (i : ι) → Zero (β₁ i)
inst✝¹ : (i : ι) → Zero (β₂ i)
inst✝ : (i : ι) → (x : β₁ i) → Decidable (x ≠ 0)
f : (i : ι) → β₁ i → β₂ i
hf : ∀ (i : ι), f i 0 = 0
g : Π₀ (i : ι), β₁ i
i✝ : ι
⊢ (mapRange f hf g) i✝ = (mk g.support fun i ↦ f (↑i) (g ↑i)) i✝
Module: Mathlib.Data.Finsupp.ToDFinsupp

Goal state before:
pp: ι : Type u_1
η : ι → Type u_4
N : Type u_5
inst✝ : AddZeroClass N
f g : (i : ι) × η i →₀ N
⊢ sigmaFinsuppEquivDFinsupp (f + g) = sigmaFinsuppEquivDFinsupp f + sigmaFinsuppEquivDFinsupp g

Tactic:
ext

Goal state after:
ι : Type u_1
η : ι → Type u_4
N : Type u_5
inst✝ : AddZeroClass N
f g : (i : ι) × η i →₀ N
i✝ : ι
a✝ : η i✝
⊢ ((sigmaFinsuppEquivDFinsupp (f + g)) i✝) a✝ = ((sigmaFinsuppEquivDFinsupp f + sigmaFinsuppEquivDFinsupp g) i✝) a✝
Module: Mathlib.Data.Finsupp.ToDFinsupp

Goal state before:
pp: ι : Type u_1
η : ι → Type u_4
N : Type u_5
R : Type u_6
inst✝² : Monoid R
inst✝¹ : AddMonoid N
inst✝ : DistribMulAction R N
r : R
f : (i : ι) × η i →₀ N
⊢ sigmaFinsuppEquivDFinsupp (r • f) = r • sigmaFinsuppEquivDFinsupp f

Tactic:
ext

Goal state after:
ι : Type u_1
η : ι → Type u_4
N : Type u_5
R : Type u_6
inst✝² : Monoid R
inst✝¹ : AddMonoid N
inst✝ : DistribMulAction R N
r : R
f : (i : ι) × η i →₀ N
i✝ : ι
a✝ : η i✝
⊢ ((sigmaFinsuppEquivDFinsupp (r • f)) i✝) a✝ = ((r • sigmaFinsuppEquivDFinsupp f) i✝) a✝
Module: Mathlib.LinearAlgebra.Finsupp.SumProd

Goal state before:
pp: α✝ : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
R : Type u_5
S : Type u_6
inst✝⁷ : Semiring R
inst✝⁶ : Semiring S
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
α : Type u_7
β : Type u_8
m✝ : R
x✝ : α ⊕ β →₀ M
⊢ sumFinsuppAddEquivProdFinsupp.toFun (m✝ • x✝) = (RingHom.id R) m✝ • sumFinsuppAddEquivProdFinsupp.toFun x✝

Tactic:
ext

Goal state after:
case fst
α✝ : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
R : Type u_5
S : Type u_6
inst✝⁷ : Semiring R
inst✝⁶ : Semiring S
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
α : Type u_7
β : Type u_8
m✝ : R
x✝ : α ⊕ β →₀ M
a✝ : α
⊢ (sumFinsuppAddEquivProdFinsupp.toFun (m✝ • x✝)).1 a✝ =
    ((RingHom.id R) m✝ • sumFinsuppAddEquivProdFinsupp.toFun x✝).1 a✝

case snd
α✝ : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
R : Type u_5
S : Type u_6
inst✝⁷ : Semiring R
inst✝⁶ : Semiring S
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : AddCommMonoid N
inst✝² : Module R N
inst✝¹ : AddCommMonoid P
inst✝ : Module R P
α : Type u_7
β : Type u_8
m✝ : R
x✝ : α ⊕ β →₀ M
a✝ : β
⊢ (sumFinsuppAddEquivProdFinsupp.toFun (m✝ • x✝)).2 a✝ =
    ((RingHom.id R) m✝ • sumFinsuppAddEquivProdFinsupp.toFun x✝).2 a✝
Module: Mathlib.LinearAlgebra.Finsupp.SumProd

Goal state before:
pp: α : Type u_1
M✝ : Type u_2
N : Type u_3
P : Type u_4
R : Type u_5
S : Type u_6
inst✝¹¹ : Semiring R
inst✝¹⁰ : Semiring S
inst✝⁹ : AddCommMonoid M✝
inst✝⁸ : Module R M✝
inst✝⁷ : AddCommMonoid N
inst✝⁶ : Module R N
inst✝⁵ : AddCommMonoid P
inst✝⁴ : Module R P
η : Type u_7
inst✝³ : Fintype η
ιs✝ : η → Type u_8
inst✝² : Zero α
M : Type u_9
ιs : η → Type u_10
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
c : R
f : (j : η) × ιs j →₀ M
⊢ sigmaFinsuppAddEquivPiFinsupp.toFun (c • f) = (RingHom.id R) c • sigmaFinsuppAddEquivPiFinsupp.toFun f

Tactic:
ext

Goal state after:
α : Type u_1
M✝ : Type u_2
N : Type u_3
P : Type u_4
R : Type u_5
S : Type u_6
inst✝¹¹ : Semiring R
inst✝¹⁰ : Semiring S
inst✝⁹ : AddCommMonoid M✝
inst✝⁸ : Module R M✝
inst✝⁷ : AddCommMonoid N
inst✝⁶ : Module R N
inst✝⁵ : AddCommMonoid P
inst✝⁴ : Module R P
η : Type u_7
inst✝³ : Fintype η
ιs✝ : η → Type u_8
inst✝² : Zero α
M : Type u_9
ιs : η → Type u_10
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
c : R
f : (j : η) × ιs j →₀ M
x✝ : η
a✝ : ιs x✝
⊢ (sigmaFinsuppAddEquivPiFinsupp.toFun (c • f) x✝) a✝ =
    (((RingHom.id R) c • sigmaFinsuppAddEquivPiFinsupp.toFun f) x✝) a✝