awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Zero γ
c : α ⊕ β →₀ γ
h :
  ∀ (val : α),
    Eq.{u_3 + 1} (α := γ)
      (((comapDomain Sum.inl c ⋯).sumElim (comapDomain Sum.inr c ⋯) : (a : α ⊕ β) → γ) (Sum.inl val) : γ)
      ((c : (a : α ⊕ β) → γ) (Sum.inl val) : γ)
h₁ :
  ∀ (val : β),
    Eq.{u_3 + 1} (α := γ)
      (((comapDomain Sum.inl c ⋯).sumElim (comapDomain Sum.inr c ⋯) : (a : α ⊕ β) → γ) (Sum.inr val) : γ)
      ((c : (a : α ⊕ β) → γ) (Sum.inr val) : γ)
⊢ (comapDomain Sum.inl c ⋯).sumElim (comapDomain Sum.inr c ⋯) = c

Tactic:
ext (_ | _)
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Zero γ
c : α ⊕ β →₀ γ
val : α
⊢ Eq.{u_3 + 1} (α := γ)
    (((comapDomain Sum.inl c ⋯).sumElim (comapDomain Sum.inr c ⋯) : (a : α ⊕ β) → γ) (Sum.inl val) : γ)
    ((c : (a : α ⊕ β) → γ) (Sum.inl val) : γ)

Tactic:
simp
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Zero γ
c : α ⊕ β →₀ γ
val : β
⊢ Eq.{u_3 + 1} (α := γ)
    (((comapDomain Sum.inl c ⋯).sumElim (comapDomain Sum.inr c ⋯) : (a : α ⊕ β) → γ) (Sum.inr val) : γ)
    ((c : (a : α ⊕ β) → γ) (Sum.inr val) : γ)

Tactic:
simp
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : AddZeroClass M
a b : α →₀ M
c d : β →₀ M
h :
  ∀ (val : α),
    Eq.{u_5 + 1} (α := M) (((a + b).sumElim (c + d) : (a : α ⊕ β) → M) (Sum.inl val) : M)
      ((a.sumElim c + b.sumElim d : (a : α ⊕ β) → M) (Sum.inl val) : M)
h₁ :
  ∀ (val : β),
    Eq.{u_5 + 1} (α := M) (((a + b).sumElim (c + d) : (a : α ⊕ β) → M) (Sum.inr val) : M)
      ((a.sumElim c + b.sumElim d : (a : α ⊕ β) → M) (Sum.inr val) : M)
⊢ (a + b).sumElim (c + d) = a.sumElim c + b.sumElim d

Tactic:
ext (_ | _)
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : AddZeroClass M
a b : α →₀ M
c d : β →₀ M
val : α
⊢ Eq.{u_5 + 1} (α := M) (((a + b).sumElim (c + d) : (a : α ⊕ β) → M) (Sum.inl val) : M)
    ((a.sumElim c + b.sumElim d : (a : α ⊕ β) → M) (Sum.inl val) : M)

Tactic:
simp
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : AddZeroClass M
a b : α →₀ M
c d : β →₀ M
val : β
⊢ Eq.{u_5 + 1} (α := M) (((a + b).sumElim (c + d) : (a : α ⊕ β) → M) (Sum.inr val) : M)
    ((a.sumElim c + b.sumElim d : (a : α ⊕ β) → M) (Sum.inr val) : M)

Tactic:
simp
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α_1 : Type u_1
β_1 : Type u_2
γ_1 : Type u_3
ι : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
G : Type u_8
H : Type u_9
R : Type u_10
S : Type u_11
inst : Zero γ_1
α : Type u_12
β : Type u_13
γ : Type u_14
inst_1 : Zero γ
f : α ⊕ β →₀ γ
h :
  ∀ (ab : α ⊕ β),
    Eq.{u_14 + 1} (α := γ)
      (((fun (fg : (α →₀ γ) × (β →₀ γ)) ↦ fg.1.sumElim fg.2)
              ((fun (f : α ⊕ β →₀ γ) ↦ (comapDomain Sum.inl f ⋯, comapDomain Sum.inr f ⋯)) f) :
            (a : α ⊕ β) → γ)
          ab :
        γ)
      ((f : (a : α ⊕ β) → γ) ab : γ)
⊢ (fun (fg : (α →₀ γ) × (β →₀ γ)) ↦ fg.1.sumElim fg.2)
      ((fun (f : α ⊕ β →₀ γ) ↦ (comapDomain Sum.inl f ⋯, comapDomain Sum.inr f ⋯)) f) =
    f

Tactic:
ext ab
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α_1 : Type u_1
β_1 : Type u_2
γ_1 : Type u_3
ι : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
G : Type u_8
H : Type u_9
R : Type u_10
S : Type u_11
inst : Zero γ_1
α : Type u_12
β : Type u_13
γ : Type u_14
inst_1 : Zero γ
f : α ⊕ β →₀ γ
ab : α ⊕ β
h :
  ∀ (a : α),
    Eq.{u_14 + 1} (α := γ)
      (((fun (fg : (α →₀ γ) × (β →₀ γ)) ↦ fg.1.sumElim fg.2)
              ((fun (f : α ⊕ β →₀ γ) ↦ (comapDomain Sum.inl f ⋯, comapDomain Sum.inr f ⋯)) f) :
            (a : α ⊕ β) → γ)
          (Sum.inl a) :
        γ)
      ((f : (a : α ⊕ β) → γ) (Sum.inl a) : γ)
h₁ :
  ∀ (b : β),
    Eq.{u_14 + 1} (α := γ)
      (((fun (fg : (α →₀ γ) × (β →₀ γ)) ↦ fg.1.sumElim fg.2)
              ((fun (f : α ⊕ β →₀ γ) ↦ (comapDomain Sum.inl f ⋯, comapDomain Sum.inr f ⋯)) f) :
            (a : α ⊕ β) → γ)
          (Sum.inr b) :
        γ)
      ((f : (a : α ⊕ β) → γ) (Sum.inr b) : γ)
⊢ Eq.{u_14 + 1} (α := γ)
    (((fun (fg : (α →₀ γ) × (β →₀ γ)) ↦ fg.1.sumElim fg.2)
            ((fun (f : α ⊕ β →₀ γ) ↦ (comapDomain Sum.inl f ⋯, comapDomain Sum.inr f ⋯)) f) :
          (a : α ⊕ β) → γ)
        ab :
      γ)
    ((f : (a : α ⊕ β) → γ) ab : γ)

Tactic:
rcases ab with a | b
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α_1 : Type u_1
β_1 : Type u_2
γ_1 : Type u_3
ι : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
G : Type u_8
H : Type u_9
R : Type u_10
S : Type u_11
inst : Zero γ_1
α : Type u_12
β : Type u_13
γ : Type u_14
inst_1 : Zero γ
f : α ⊕ β →₀ γ
a : α
⊢ Eq.{u_14 + 1} (α := γ)
    (((fun (fg : (α →₀ γ) × (β →₀ γ)) ↦ fg.1.sumElim fg.2)
            ((fun (f : α ⊕ β →₀ γ) ↦ (comapDomain Sum.inl f ⋯, comapDomain Sum.inr f ⋯)) f) :
          (a : α ⊕ β) → γ)
        (Sum.inl a) :
      γ)
    ((f : (a : α ⊕ β) → γ) (Sum.inl a) : γ)

Tactic:
simp
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α_1 : Type u_1
β_1 : Type u_2
γ_1 : Type u_3
ι : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
G : Type u_8
H : Type u_9
R : Type u_10
S : Type u_11
inst : Zero γ_1
α : Type u_12
β : Type u_13
γ : Type u_14
inst_1 : Zero γ
f : α ⊕ β →₀ γ
b : β
⊢ Eq.{u_14 + 1} (α := γ)
    (((fun (fg : (α →₀ γ) × (β →₀ γ)) ↦ fg.1.sumElim fg.2)
            ((fun (f : α ⊕ β →₀ γ) ↦ (comapDomain Sum.inl f ⋯, comapDomain Sum.inr f ⋯)) f) :
          (a : α ⊕ β) → γ)
        (Sum.inr b) :
      γ)
    ((f : (a : α ⊕ β) → γ) (Sum.inr b) : γ)

Tactic:
simp
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α_1 : Type u_1
β_1 : Type u_2
γ_1 : Type u_3
ι : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
G : Type u_8
H : Type u_9
R : Type u_10
S : Type u_11
inst : Zero γ_1
α : Type u_12
β : Type u_13
γ : Type u_14
inst_1 : Zero γ
fg : (α →₀ γ) × (β →₀ γ)
fst :
  ∀ (a : α),
    Eq.{u_14 + 1} (α := γ)
      ((((fun (f : α ⊕ β →₀ γ) ↦ (comapDomain Sum.inl f ⋯, comapDomain Sum.inr f ⋯))
                ((fun (fg : (α →₀ γ) × (β →₀ γ)) ↦ fg.1.sumElim fg.2) fg)).1 :
            (a : α) → γ)
          a :
        γ)
      ((fg.1 : (a : α) → γ) a : γ)
snd :
  ∀ (a : β),
    Eq.{u_14 + 1} (α := γ)
      ((((fun (f : α ⊕ β →₀ γ) ↦ (comapDomain Sum.inl f ⋯, comapDomain Sum.inr f ⋯))
                ((fun (fg : (α →₀ γ) × (β →₀ γ)) ↦ fg.1.sumElim fg.2) fg)).2 :
            (a : β) → γ)
          a :
        γ)
      ((fg.2 : (a : β) → γ) a : γ)
⊢ (fun (f : α ⊕ β →₀ γ) ↦ (comapDomain Sum.inl f ⋯, comapDomain Sum.inr f ⋯))
      ((fun (fg : (α →₀ γ) × (β →₀ γ)) ↦ fg.1.sumElim fg.2) fg) =
    fg

Tactic:
ext
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α_1 : Type u_1
β_1 : Type u_2
γ_1 : Type u_3
ι : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
G : Type u_8
H : Type u_9
R : Type u_10
S : Type u_11
inst : Zero γ_1
α : Type u_12
β : Type u_13
γ : Type u_14
inst_1 : Zero γ
fg : (α →₀ γ) × (β →₀ γ)
a : α
⊢ Eq.{u_14 + 1} (α := γ)
    ((((fun (f : α ⊕ β →₀ γ) ↦ (comapDomain Sum.inl f ⋯, comapDomain Sum.inr f ⋯))
              ((fun (fg : (α →₀ γ) × (β →₀ γ)) ↦ fg.1.sumElim fg.2) fg)).1 :
          (a : α) → γ)
        a :
      γ)
    ((fg.1 : (a : α) → γ) a : γ)

Tactic:
simp
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α_1 : Type u_1
β_1 : Type u_2
γ_1 : Type u_3
ι : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
G : Type u_8
H : Type u_9
R : Type u_10
S : Type u_11
inst : Zero γ_1
α : Type u_12
β : Type u_13
γ : Type u_14
inst_1 : Zero γ
fg : (α →₀ γ) × (β →₀ γ)
a : β
⊢ Eq.{u_14 + 1} (α := γ)
    ((((fun (f : α ⊕ β →₀ γ) ↦ (comapDomain Sum.inl f ⋯, comapDomain Sum.inr f ⋯))
              ((fun (fg : (α →₀ γ) × (β →₀ γ)) ↦ fg.1.sumElim fg.2) fg)).2 :
          (a : β) → γ)
        a :
      γ)
    ((fg.2 : (a : β) → γ) a : γ)

Tactic:
simp
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_12
β : Type u_13
γ : Type u_14
inst : Zero γ
f : α ⊕ β →₀ γ
x : α
⊢ Eq.{u_14 + 1} (α := γ)
    ((((sumFinsuppEquivProdFinsupp : (a : α ⊕ β →₀ γ) → (α →₀ γ) × (β →₀ γ)) f).1 : (a : α) → γ) x : γ)
    ((f : (a : α ⊕ β) → γ) (Sum.inl x) : γ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_12
β : Type u_13
γ : Type u_14
inst : Zero γ
f : α ⊕ β →₀ γ
y : β
⊢ Eq.{u_14 + 1} (α := γ)
    ((((sumFinsuppEquivProdFinsupp : (a : α ⊕ β →₀ γ) → (α →₀ γ) × (β →₀ γ)) f).2 : (a : β) → γ) y : γ)
    ((f : (a : α ⊕ β) → γ) (Sum.inr y) : γ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_12
β : Type u_13
γ : Type u_14
inst : Zero γ
fg : (α →₀ γ) × (β →₀ γ)
x : α
⊢ Eq.{u_14 + 1} (α := γ)
    ((((Equiv.symm sumFinsuppEquivProdFinsupp : (a : (α →₀ γ) × (β →₀ γ)) → α ⊕ β →₀ γ) fg : α ⊕ β →₀ γ) :
          (a : α ⊕ β) → γ)
        (Sum.inl x) :
      γ)
    ((fg.1 : (a : α) → γ) x : γ)

Tactic:
rfl

Premises used: rfl, Sum.elim
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_12
β : Type u_13
γ : Type u_14
inst : Zero γ
fg : (α →₀ γ) × (β →₀ γ)
y : β
⊢ Eq.{u_14 + 1} (α := γ)
    ((((Equiv.symm sumFinsuppEquivProdFinsupp : (a : (α →₀ γ) × (β →₀ γ)) → α ⊕ β →₀ γ) fg : α ⊕ β →₀ γ) :
          (a : α ⊕ β) → γ)
        (Sum.inr y) :
      γ)
    ((fg.2 : (a : β) → γ) y : γ)

Tactic:
rfl

Premises used: rfl, Sum.elim
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α_1 : Type u_1
β_1 : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
G : Type u_8
H : Type u_9
R : Type u_10
S : Type u_11
inst : Zero γ
inst_1 : AddMonoid M
α : Type u_12
β : Type u_13
x y : α ⊕ β →₀ M
fst :
  ∀ (a : α),
    Eq.{u_5 + 1} (α := M) (((Equiv.toFun sumFinsuppEquivProdFinsupp (x + y)).1 : (a : α) → M) a : M)
      (((Equiv.toFun sumFinsuppEquivProdFinsupp x + Equiv.toFun sumFinsuppEquivProdFinsupp y).1 : (a : α) → M) a : M)
snd :
  ∀ (a : β),
    Eq.{u_5 + 1} (α := M) (((Equiv.toFun sumFinsuppEquivProdFinsupp (x + y)).2 : (a : β) → M) a : M)
      (((Equiv.toFun sumFinsuppEquivProdFinsupp x + Equiv.toFun sumFinsuppEquivProdFinsupp y).2 : (a : β) → M) a : M)
⊢ Equiv.toFun sumFinsuppEquivProdFinsupp (x + y) =
    Equiv.toFun sumFinsuppEquivProdFinsupp x + Equiv.toFun sumFinsuppEquivProdFinsupp y

Tactic:
ext
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α_1 : Type u_1
β_1 : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
G : Type u_8
H : Type u_9
R : Type u_10
S : Type u_11
inst : Zero γ
inst_1 : AddMonoid M
α : Type u_12
β : Type u_13
x y : α ⊕ β →₀ M
a : α
⊢ Eq.{u_5 + 1} (α := M) (((Equiv.toFun sumFinsuppEquivProdFinsupp (x + y)).1 : (a : α) → M) a : M)
    (((Equiv.toFun sumFinsuppEquivProdFinsupp x + Equiv.toFun sumFinsuppEquivProdFinsupp y).1 : (a : α) → M) a : M)

Tactic:
simp only [Equiv.toFun_as_coe, Prod.fst_add, Prod.snd_add, add_apply,
          snd_sumFinsuppEquivProdFinsupp, fst_sumFinsuppEquivProdFinsupp]

Premises used: Equiv.toFun_as_coe, Finsupp.add_apply, Finsupp.fst_sumFinsuppEquivProdFinsupp, Prod.fst_add, Finsupp.snd_sumFinsuppEquivProdFinsupp, Prod.snd_add
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α_1 : Type u_1
β_1 : Type u_2
γ : Type u_3
ι : Type u_4
M : Type u_5
N : Type u_6
P : Type u_7
G : Type u_8
H : Type u_9
R : Type u_10
S : Type u_11
inst : Zero γ
inst_1 : AddMonoid M
α : Type u_12
β : Type u_13
x y : α ⊕ β →₀ M
a : β
⊢ Eq.{u_5 + 1} (α := M) (((Equiv.toFun sumFinsuppEquivProdFinsupp (x + y)).2 : (a : β) → M) a : M)
    (((Equiv.toFun sumFinsuppEquivProdFinsupp x + Equiv.toFun sumFinsuppEquivProdFinsupp y).2 : (a : β) → M) a : M)

Tactic:
simp only [Equiv.toFun_as_coe, Prod.fst_add, Prod.snd_add, add_apply,
          snd_sumFinsuppEquivProdFinsupp, fst_sumFinsuppEquivProdFinsupp]

Premises used: Equiv.toFun_as_coe, Finsupp.add_apply, Finsupp.fst_sumFinsuppEquivProdFinsupp, Prod.fst_add, Finsupp.snd_sumFinsuppEquivProdFinsupp, Prod.snd_add
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
M : Type u_5
inst : AddMonoid M
α : Type u_12
β : Type u_13
f : α ⊕ β →₀ M
x : α
⊢ Eq.{u_5 + 1} (α := M)
    ((((sumFinsuppAddEquivProdFinsupp : (a : α ⊕ β →₀ M) → (α →₀ M) × (β →₀ M)) f).1 : (a : α) → M) x : M)
    ((f : (a : α ⊕ β) → M) (Sum.inl x) : M)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
M : Type u_5
inst : AddMonoid M
α : Type u_12
β : Type u_13
f : α ⊕ β →₀ M
y : β
⊢ Eq.{u_5 + 1} (α := M)
    ((((sumFinsuppAddEquivProdFinsupp : (a : α ⊕ β →₀ M) → (α →₀ M) × (β →₀ M)) f).2 : (a : β) → M) y : M)
    ((f : (a : α ⊕ β) → M) (Sum.inr y) : M)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
M : Type u_5
inst : AddMonoid M
α : Type u_12
β : Type u_13
fg : (α →₀ M) × (β →₀ M)
x : α
⊢ Eq.{u_5 + 1} (α := M)
    ((((AddEquiv.symm sumFinsuppAddEquivProdFinsupp : (a : (α →₀ M) × (β →₀ M)) → α ⊕ β →₀ M) fg : α ⊕ β →₀ M) :
          (a : α ⊕ β) → M)
        (Sum.inl x) :
      M)
    ((fg.1 : (a : α) → M) x : M)

Tactic:
rfl

Premises used: rfl, Sum.elim
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
M : Type u_5
inst : AddMonoid M
α : Type u_12
β : Type u_13
fg : (α →₀ M) × (β →₀ M)
y : β
⊢ Eq.{u_5 + 1} (α := M)
    ((((AddEquiv.symm sumFinsuppAddEquivProdFinsupp : (a : (α →₀ M) × (β →₀ M)) → α ⊕ β →₀ M) fg : α ⊕ β →₀ M) :
          (a : α ⊕ β) → M)
        (Sum.inr y) :
      M)
    ((fg.2 : (a : β) → M) y : M)

Tactic:
rfl

Premises used: rfl, Sum.elim
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M_1 : Type u_5
N : Type u_6
P_1 : Type u_7
G : Type u_8
H : Type u_9
R : Type u_10
S : Type u_11
M : Type u_12
inst : Zero M
P : α → Prop
inst_1 : DecidablePred P
f : Finsupp.{u_1, u_12} (Subtype P) M
g : Finsupp.{u_1, u_12} { a : α // ¬P a } M
simp_rw :
  ∀ ⦃a : α⦄ (a_1 : α) (b : P a_1) (h : Subtype.mk (p := fun (a : α) ↦ P a) a_1 b ∈ f.support ∧ a_1 = a),
    ¬∃ (a_2 : α) (h : ¬P a_2), Subtype.mk (p := fun (a : α) ↦ ¬P a) a_2 ⋯ ∈ g.support ∧ a_2 = a
⊢ Disjoint (map (Embedding.subtype P) f.support) (map (Embedding.subtype fun (a : α) ↦ ¬P a) g.support)

Tactic:
simp_rw [Finset.disjoint_left, mem_map, forall_exists_index, Embedding.coe_subtype,
      Subtype.forall, Subtype.exists]

Premises used: Function.Embedding.coe_subtype, Subtype.exists, forall_exists_index, Subtype.forall, Finset.disjoint_left, Finset.mem_map
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M_1 : Type u_5
N : Type u_6
P_1 : Type u_7
G : Type u_8
H : Type u_9
R : Type u_10
S : Type u_11
M : Type u_12
inst : Zero M
P : α → Prop
inst_1 : DecidablePred P
f : Finsupp.{u_1, u_12} (Subtype P) M
g : Finsupp.{u_1, u_12} { a : α // ¬P a } M
b : α
hb : ¬P b
ha : P b
⊢ False

Tactic:
hb ha
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M_1 : Type u_5
N : Type u_6
P_1 : Type u_7
G : Type u_8
H : Type u_9
R : Type u_10
S : Type u_11
M : Type u_12
inst : Zero M
P : α → Prop
inst_1 : DecidablePred P
f : Finsupp.{u_1, u_12} (Subtype P) M
g : Finsupp.{u_1, u_12} { a : α // ¬P a } M
b : α
hb : ¬P b
ha : P b
⊢ False

Tactic:
exact hb ha
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M_1 : Type u_5
N : Type u_6
P_1 : Type u_7
G : Type u_8
H : Type u_9
R : Type u_10
S : Type u_11
M : Type u_12
inst : Zero M
P : α → Prop
inst_1 : DecidablePred P
f : Finsupp.{u_1, u_12} (Subtype P) M
g : Finsupp.{u_1, u_12} { a : α // ¬P a } M
a : α
pos :
  ∀ (ha : P a),
    a ∈ (map (Embedding.subtype P) f.support).disjUnion (map (Embedding.subtype fun (a : α) ↦ ¬P a) g.support) ⋯ ↔
      Ne.{u_12 + 1} (α := M)
        (if h : P a then (f : (a : Subtype P) → M) (Subtype.mk (p := P) a h)
        else (g : (a : { a : α // ¬P a }) → M) (Subtype.mk (p := fun (a : α) ↦ ¬P a) a h))
        0
neg :
  ∀ (ha : ¬P a),
    a ∈ (map (Embedding.subtype P) f.support).disjUnion (map (Embedding.subtype fun (a : α) ↦ ¬P a) g.support) ⋯ ↔
      Ne.{u_12 + 1} (α := M)
        (if h : P a then (f : (a : Subtype P) → M) (Subtype.mk (p := P) a h)
        else (g : (a : { a : α // ¬P a }) → M) (Subtype.mk (p := fun (a : α) ↦ ¬P a) a h))
        0
⊢ a ∈ (map (Embedding.subtype P) f.support).disjUnion (map (Embedding.subtype fun (a : α) ↦ ¬P a) g.support) ⋯ ↔
    Ne.{u_12 + 1} (α := M)
      (if h : P a then (f : (a : Subtype P) → M) (Subtype.mk (p := P) a h)
      else (g : (a : { a : α // ¬P a }) → M) (Subtype.mk (p := fun (a : α) ↦ ¬P a) a h))
      0

Tactic:
by_cases ha : P a
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M_1 : Type u_5
N : Type u_6
P_1 : Type u_7
G : Type u_8
H : Type u_9
R : Type u_10
S : Type u_11
M : Type u_12
inst : Zero M
P : α → Prop
inst_1 : DecidablePred P
f : Finsupp.{u_1, u_12} (Subtype P) M
g : Finsupp.{u_1, u_12} { a : α // ¬P a } M
a : α
ha : P a
⊢ a ∈ (map (Embedding.subtype P) f.support).disjUnion (map (Embedding.subtype fun (a : α) ↦ ¬P a) g.support) ⋯ ↔
    Ne.{u_12 + 1} (α := M)
      (if h : P a then (f : (a : Subtype P) → M) (Subtype.mk (p := P) a h)
      else (g : (a : { a : α // ¬P a }) → M) (Subtype.mk (p := fun (a : α) ↦ ¬P a) a h))
      0

Tactic:
simp [ha]
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
ι : Type u_4
M_1 : Type u_5
N : Type u_6
P_1 : Type u_7
G : Type u_8
H : Type u_9
R : Type u_10
S : Type u_11
M : Type u_12
inst : Zero M
P : α → Prop
inst_1 : DecidablePred P
f : Finsupp.{u_1, u_12} (Subtype P) M
g : Finsupp.{u_1, u_12} { a : α // ¬P a } M
a : α
ha : ¬P a
⊢ a ∈ (map (Embedding.subtype P) f.support).disjUnion (map (Embedding.subtype fun (a : α) ↦ ¬P a) g.support) ⋯ ↔
    Ne.{u_12 + 1} (α := M)
      (if h : P a then (f : (a : Subtype P) → M) (Subtype.mk (p := P) a h)
      else (g : (a : { a : α // ¬P a }) → M) (Subtype.mk (p := fun (a : α) ↦ ¬P a) a h))
      0

Tactic:
simp [ha]
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
M : Type u_12
inst : Zero M
P : α → Prop
inst_1 : DecidablePred P
f : Finsupp.{u_1, u_12} (Subtype P) M
g : Finsupp.{u_1, u_12} { a : α // ¬P a } M
⊢ subtypeDomain P (f.piecewise (P := P) g) = f

Tactic:
Finsupp.ext fun a => dif_pos a.prop

Premises used: Finsupp.ext, dif_pos, Subtype.prop
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
M : Type u_12
inst : Zero M
P : α → Prop
inst_1 : DecidablePred P
f : Finsupp.{u_1, u_12} (Subtype P) M
g : Finsupp.{u_1, u_12} { a : α // ¬P a } M
⊢ subtypeDomain (fun (x : α) ↦ ¬P x) (f.piecewise (P := P) g) = g

Tactic:
Finsupp.ext fun a => dif_neg a.prop

Premises used: Finsupp.ext, dif_neg, Subtype.prop
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
M : Type u_12
inst : Zero M
P : α → Prop
inst_1 : DecidablePred P
f : Finsupp.{u_1, u_12} (Subtype P) M
h :
  ∀ (a : α),
    Eq.{u_12 + 1} (α := M) ((f.extendDomain (P := P) : (a : α) → M) a : M)
      ((embDomain (Embedding.subtype P) f : (a : α) → M) a : M)
⊢ f.extendDomain (P := P) = embDomain (Embedding.subtype P) f

Tactic:
ext a
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
M : Type u_12
inst : Zero M
P : α → Prop
inst_1 : DecidablePred P
f : Finsupp.{u_1, u_12} (Subtype P) M
a : α
pos :
  ∀ (h : P a),
    Eq.{u_12 + 1} (α := M) ((f.extendDomain (P := P) : (a : α) → M) a : M)
      ((embDomain (Embedding.subtype P) f : (a : α) → M) a : M)
neg :
  ∀ (h : ¬P a),
    Eq.{u_12 + 1} (α := M) ((f.extendDomain (P := P) : (a : α) → M) a : M)
      ((embDomain (Embedding.subtype P) f : (a : α) → M) a : M)
⊢ Eq.{u_12 + 1} (α := M) ((f.extendDomain (P := P) : (a : α) → M) a : M)
    ((embDomain (Embedding.subtype P) f : (a : α) → M) a : M)

Tactic:
by_cases h : P a
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
M : Type u_12
inst : Zero M
P : α → Prop
inst_1 : DecidablePred P
f : Finsupp.{u_1, u_12} (Subtype P) M
a : α
h : P a
⊢ Eq.{u_12 + 1} (α := M) ((f.extendDomain (P := P) : (a : α) → M) a : M)
    ((embDomain (Embedding.subtype P) f : (a : α) → M) a : M)

Tactic:
Eq.trans ?_ (embDomain_apply_self (.subtype P) f (Subtype.mk a h)).symm

Premises used: Finsupp.embDomain_apply_self, Subtype.mk, Function.Embedding.subtype, Eq.symm, Eq.trans
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
M : Type u_12
inst : Zero M
P : α → Prop
inst_1 : DecidablePred P
f : Finsupp.{u_1, u_12} (Subtype P) M
a : α
h : P a
pos :
  Eq.{u_12 + 1} (α := M) ((f.extendDomain (P := P) : (a : α) → M) a : M)
    ((f : (a : Subtype P) → M) (Subtype.mk (p := P) a h) : M)
⊢ Eq.{u_12 + 1} (α := M) ((f.extendDomain (P := P) : (a : α) → M) a : M)
    ((embDomain (Embedding.subtype P) f : (a : α) → M) a : M)

Tactic:
refine Eq.trans ?_ (embDomain_apply_self (.subtype P) f (Subtype.mk a h)).symm

Premises used: Finsupp.embDomain_apply_self, Subtype.mk, Function.Embedding.subtype, Eq.symm, Eq.trans
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
M : Type u_12
inst : Zero M
P : α → Prop
inst_1 : DecidablePred P
f : Finsupp.{u_1, u_12} (Subtype P) M
a : α
h : P a
⊢ Eq.{u_12 + 1} (α := M) ((f.extendDomain (P := P) : (a : α) → M) a : M)
    ((f : (a : Subtype P) → M) (Subtype.mk (p := P) a h) : M)

Tactic:
simp [h]
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
M : Type u_12
inst : Zero M
P : α → Prop
inst_1 : DecidablePred P
f : Finsupp.{u_1, u_12} (Subtype P) M
a : α
h : ¬P a
⊢ Eq.{u_12 + 1} (α := M) ((f.extendDomain (P := P) : (a : α) → M) a : M)
    ((embDomain (Embedding.subtype P) f : (a : α) → M) a : M)

Tactic:
simp [embDomain, h]

Premises used: Finsupp.embDomain
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
M : Type u_12
inst : Zero M
P : α → Prop
inst_1 : DecidablePred P
f : Finsupp.{u_1, u_12} (Subtype P) M
⊢ (↑f.extendDomain (P := P).support : Set α) ⊆ {x : α | P x}

Tactic:
grind
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
M : Type u_12
inst : Zero M
P : α → Prop
inst_1 : DecidablePred P
f : Finsupp.{u_1, u_12} (Subtype P) M
⊢ subtypeDomain P (f.extendDomain (P := P)) = f

Tactic:
subtypeDomain_piecewise _ _

Premises used: Finsupp.subtypeDomain_piecewise, Finsupp.extendDomain
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
M : Type u_12
inst : Zero M
P : α → Prop
inst_1 : DecidablePred P
f : α →₀ M
hf : ∀ a ∈ f.support, P a
h :
  ∀ (a : α),
    Eq.{u_12 + 1} (α := M) (((subtypeDomain P f).extendDomain (P := P) : (a : α) → M) a : M) ((f : (a : α) → M) a : M)
⊢ (subtypeDomain P f).extendDomain (P := P) = f

Tactic:
ext
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
M : Type u_12
inst : Zero M
P : α → Prop
inst_1 : DecidablePred P
f : α →₀ M
hf : ∀ a ∈ f.support, P a
a : α
h : ¬P a → Eq.{u_12 + 1} (α := M) (0 : M) ((f : (a : α) → M) a : M)
⊢ Eq.{u_12 + 1} (α := M) (((subtypeDomain P f).extendDomain (P := P) : (a : α) → M) a : M) ((f : (a : α) → M) a : M)

Tactic:
simp only [extendDomain_apply, subtypeDomain_apply, dite_eq_ite, ite_eq_left_iff]

Premises used: ite_eq_left_iff, Finsupp.subtypeDomain_apply, dite_eq_ite, Finsupp.extendDomain_apply
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
M : Type u_12
inst : Zero M
P : α → Prop
inst_1 : DecidablePred P
f : α →₀ M
hf : ∀ a ∈ f.support, P a
a : α
⊢ ¬P a → Eq.{u_12 + 1} (α := M) (0 : M) ((f : (a : α) → M) a : M)

Tactic:
grind
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
M : Type u_12
inst : Zero M
P : α → Prop
inst_1 : DecidablePred P
a : Subtype P
m : M
h :
  ∀ (a' : α),
    Eq.{u_12 + 1} (α := M) ((extendDomain (P := P) (single a m) : (a : α) → M) a' : M)
      ((single (↑a : α) m : (a : α) → M) a' : M)
⊢ Eq (α := α →₀ M) (extendDomain (P := P) (single a m)) (single (↑a : α) m)

Tactic:
ext a'
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
M : Type u_12
inst : Zero M
P : α → Prop
inst_1 : DecidablePred P
a : Subtype P
m : M
a' : α
h :
  Eq.{u_12 + 1} (α := M) ((extendDomain (P := P) (single a m) : (a : α) → M) (↑a : α) : M)
    ((single (↑a : α) m : (a : α) → M) (↑a : α) : M)
h₁ :
  ∀ (ha : a' ≠ (↑a : α)),
    Eq.{u_12 + 1} (α := M) ((extendDomain (P := P) (single a m) : (a : α) → M) a' : M)
      ((single (↑a : α) m : (a : α) → M) a' : M)
⊢ Eq.{u_12 + 1} (α := M) ((extendDomain (P := P) (single a m) : (a : α) → M) a' : M)
    ((single (↑a : α) m : (a : α) → M) a' : M)

Tactic:
obtain rfl | ha := eq_or_ne a' a.val

Premises used: eq_or_ne, Subtype.val, rfl
-- Module: Mathlib.Data.Finsupp.Basic
Goal:
α : Type u_1
M : Type u_12
inst : Zero M
P : α → Prop
inst_1 : DecidablePred P
a : Subtype P
m : M
⊢ Eq.{u_12 + 1} (α := M) ((extendDomain (P := P) (single a m) : (a : α) → M) (↑a : α) : M)
    ((single (↑a : α) m : (a : α) → M) (↑a : α) : M)

Tactic:
simp [*, a.prop, single, Pi.single, Function.update, Subtype.ext_iff]

Premises used: Function.update, Pi.single, Subtype.ext_iff, Subtype.prop, Finsupp.single