awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Finsupp.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : AddCommMonoid M
f : α →₀ M
g : β →₀ M
h :
  ∀ (val : α),
    Eq.{u_5 + 1} (α := M) ((f.sumElim g : (a : α ⊕ β) → M) (Sum.inl val) : M)
      ((mapDomain Sum.inl f + mapDomain Sum.inr g : (a : α ⊕ β) → M) (Sum.inl val) : M)
⊢ f.sumElim g = mapDomain Sum.inl f + mapDomain Sum.inr g
have h₁ : ∀ (val : β),
  Eq.{u_5 + 1} (α := M) ((f.sumElim g : (a : α ⊕ β) → M) (Sum.inr val) : M)
    ((mapDomain Sum.inl f + mapDomain Sum.inr g : (a : α ⊕ β) → M) (Sum.inr val) : M)
Tactic: ext (_ | _)
-- Lean 4 proof step from Mathlib.Data.Finsupp.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Zero γ
f : α →₀ γ
g : β →₀ γ
⊢ comapDomain Sum.inl (f.sumElim g) ⋯ = f
have h : ∀ (a : α), Eq.{u_3 + 1} (α := γ) ((comapDomain Sum.inl (f.sumElim g) sorry : (a : α) → γ) a : γ) ((f : (a : α) → γ) a : γ)
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Finsupp.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Zero γ
f : α →₀ γ
g : β →₀ γ
⊢ comapDomain Sum.inr (f.sumElim g) ⋯ = g
have h : ∀ (a : β), Eq.{u_3 + 1} (α := γ) ((comapDomain Sum.inr (f.sumElim g) sorry : (a : β) → γ) a : γ) ((g : (a : β) → γ) a : γ)
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Finsupp.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Zero γ
a : α →₀ γ
⊢ Eq (α := α ⊕ β →₀ γ) (embDomain Embedding.inl a) (a.sumElim 0)
have h : ∀ (val : α),
  Eq.{u_3 + 1} (α := γ) ((embDomain Embedding.inl a : (a : α ⊕ β) → γ) (Sum.inl val) : γ)
    ((a.sumElim 0 : (a : α ⊕ β) → γ) (Sum.inl val) : γ)
Tactic: ext (_ | _)
-- Lean 4 proof step from Mathlib.Data.Finsupp.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Zero γ
a : α →₀ γ
h :
  ∀ (val : α),
    Eq.{u_3 + 1} (α := γ) ((embDomain Embedding.inl a : (a : α ⊕ β) → γ) (Sum.inl val) : γ)
      ((a.sumElim 0 : (a : α ⊕ β) → γ) (Sum.inl val) : γ)
⊢ Eq (α := α ⊕ β →₀ γ) (embDomain Embedding.inl a) (a.sumElim 0)
have h₁ : ∀ (val : β),
  Eq.{u_3 + 1} (α := γ) ((embDomain Embedding.inl a : (a : α ⊕ β) → γ) (Sum.inr val) : γ)
    ((a.sumElim 0 : (a : α ⊕ β) → γ) (Sum.inr val) : γ)
Tactic: ext (_ | _)
-- Lean 4 proof step from Mathlib.Data.Finsupp.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Zero γ
b : β →₀ γ
⊢ Eq (α := α ⊕ β →₀ γ) (embDomain Embedding.inr b) (sumElim 0 b)
have h : ∀ (val : α),
  Eq.{u_3 + 1} (α := γ) ((embDomain Embedding.inr b : (a : α ⊕ β) → γ) (Sum.inl val) : γ)
    ((sumElim 0 b : (a : α ⊕ β) → γ) (Sum.inl val) : γ)
Tactic: ext (_ | _)
-- Lean 4 proof step from Mathlib.Data.Finsupp.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Zero γ
b : β →₀ γ
h :
  ∀ (val : α),
    Eq.{u_3 + 1} (α := γ) ((embDomain Embedding.inr b : (a : α ⊕ β) → γ) (Sum.inl val) : γ)
      ((sumElim 0 b : (a : α ⊕ β) → γ) (Sum.inl val) : γ)
⊢ Eq (α := α ⊕ β →₀ γ) (embDomain Embedding.inr b) (sumElim 0 b)
have h₁ : ∀ (val : β),
  Eq.{u_3 + 1} (α := γ) ((embDomain Embedding.inr b : (a : α ⊕ β) → γ) (Sum.inr val) : γ)
    ((sumElim 0 b : (a : α ⊕ β) → γ) (Sum.inr val) : γ)
Tactic: ext (_ | _)
-- Lean 4 proof step from Mathlib.Data.Finsupp.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
inst : Zero γ
c : α ⊕ β →₀ γ
⊢ (comapDomain Sum.inl c ⋯).sumElim (comapDomain Sum.inr c ⋯) = c
have h : ∀ (val : α),
  Eq.{u_3 + 1} (α := γ)
    (((comapDomain Sum.inl c sorry).sumElim (comapDomain Sum.inr c sorry) : (a : α ⊕ β) → γ) (Sum.inl val) : γ)
    ((c : (a : α ⊕ β) → γ) (Sum.inl val) : γ)
Tactic: ext (_ | _)
-- Lean 4 proof step from Mathlib.Data.Finsupp.Basic (goal)
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) : γ)
⊢ (comapDomain Sum.inl c ⋯).sumElim (comapDomain Sum.inr c ⋯) = c
have h₁ : ∀ (val : β),
  Eq.{u_3 + 1} (α := γ)
    (((comapDomain Sum.inl c sorry).sumElim (comapDomain Sum.inr c sorry) : (a : α ⊕ β) → γ) (Sum.inr val) : γ)
    ((c : (a : α ⊕ β) → γ) (Sum.inr val) : γ)
Tactic: ext (_ | _)
-- Lean 4 proof step from Mathlib.Data.Finsupp.Basic (goal)
Goal:
α : Type u_1
β : Type u_2
M : Type u_5
inst : AddZeroClass M
a b : α →₀ M
c d : β →₀ M
⊢ (a + b).sumElim (c + d) = a.sumElim c + b.sumElim d
have 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)
Tactic: ext (_ | _)
-- Lean 4 proof step from Mathlib.Data.Finsupp.Basic (goal)
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)
⊢ (a + b).sumElim (c + d) = a.sumElim c + b.sumElim d
have 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)
Tactic: ext (_ | _)
-- Lean 4 proof step from Mathlib.Data.Finsupp.Basic (goal)
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 : α ⊕ β →₀ γ
⊢ (fun (fg : (α →₀ γ) × (β →₀ γ)) ↦ fg.1.sumElim fg.2)
      ((fun (f : α ⊕ β →₀ γ) ↦ (comapDomain Sum.inl f ⋯, comapDomain Sum.inr f ⋯)) f) =
    f
have h : ∀ (ab : α ⊕ β),
  Eq.{u_14 + 1} (α := γ)
    (((fun (fg : (α →₀ γ) × (β →₀ γ)) ↦ fg.1.sumElim fg.2)
            ((fun (f : α ⊕ β →₀ γ) ↦ (comapDomain Sum.inl f sorry, comapDomain Sum.inr f sorry)) f) :
          (a : α ⊕ β) → γ)
        ab :
      γ)
    ((f : (a : α ⊕ β) → γ) ab : γ)
Tactic: ext ab
-- Lean 4 proof step from Mathlib.Data.Finsupp.Basic (goal)
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 : α ⊕ β
⊢ 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 : γ)
have h : ∀ (a : α),
  Eq.{u_14 + 1} (α := γ)
    (((fun (fg : (α →₀ γ) × (β →₀ γ)) ↦ fg.1.sumElim fg.2)
            ((fun (f : α ⊕ β →₀ γ) ↦ (comapDomain Sum.inl f sorry, comapDomain Sum.inr f sorry)) f) :
          (a : α ⊕ β) → γ)
        (Sum.inl a) :
      γ)
    ((f : (a : α ⊕ β) → γ) (Sum.inl a) : γ)
Tactic: rcases ab with a | b
Cleared hypotheses: ab
-- Lean 4 proof step from Mathlib.Data.Finsupp.Basic (goal)
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) : γ)
⊢ 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 : γ)
have h₁ : ∀ (b : β),
  Eq.{u_14 + 1} (α := γ)
    (((fun (fg : (α →₀ γ) × (β →₀ γ)) ↦ fg.1.sumElim fg.2)
            ((fun (f : α ⊕ β →₀ γ) ↦ (comapDomain Sum.inl f sorry, comapDomain Sum.inr f sorry)) f) :
          (a : α ⊕ β) → γ)
        (Sum.inr b) :
      γ)
    ((f : (a : α ⊕ β) → γ) (Sum.inr b) : γ)
Tactic: rcases ab with a | b
Cleared hypotheses: ab
-- Lean 4 proof step from Mathlib.Data.Finsupp.Basic (goal)
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 : (α →₀ γ) × (β →₀ γ)
⊢ (fun (f : α ⊕ β →₀ γ) ↦ (comapDomain Sum.inl f ⋯, comapDomain Sum.inr f ⋯))
      ((fun (fg : (α →₀ γ) × (β →₀ γ)) ↦ fg.1.sumElim fg.2) fg) =
    fg
have fst : ∀ (a : α),
  Eq.{u_14 + 1} (α := γ)
    ((((fun (f : α ⊕ β →₀ γ) ↦ (comapDomain Sum.inl f sorry, comapDomain Sum.inr f sorry))
              ((fun (fg : (α →₀ γ) × (β →₀ γ)) ↦ fg.1.sumElim fg.2) fg)).1 :
          (a : α) → γ)
        a :
      γ)
    ((fg.1 : (a : α) → γ) a : γ)
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Finsupp.Basic (goal)
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 : γ)
⊢ (fun (f : α ⊕ β →₀ γ) ↦ (comapDomain Sum.inl f ⋯, comapDomain Sum.inr f ⋯))
      ((fun (fg : (α →₀ γ) × (β →₀ γ)) ↦ fg.1.sumElim fg.2) fg) =
    fg
have snd : ∀ (a : β),
  Eq.{u_14 + 1} (α := γ)
    ((((fun (f : α ⊕ β →₀ γ) ↦ (comapDomain Sum.inl f sorry, comapDomain Sum.inr f sorry))
              ((fun (fg : (α →₀ γ) × (β →₀ γ)) ↦ fg.1.sumElim fg.2) fg)).2 :
          (a : β) → γ)
        a :
      γ)
    ((fg.2 : (a : β) → γ) a : γ)
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Finsupp.Basic (goal)
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
⊢ Equiv.toFun sumFinsuppEquivProdFinsupp (x + y) =
    Equiv.toFun sumFinsuppEquivProdFinsupp x + Equiv.toFun sumFinsuppEquivProdFinsupp y
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Finsupp.Basic (goal)
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)
⊢ Equiv.toFun sumFinsuppEquivProdFinsupp (x + y) =
    Equiv.toFun sumFinsuppEquivProdFinsupp x + Equiv.toFun sumFinsuppEquivProdFinsupp y
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Finsupp.Basic (goal)
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
⊢ Disjoint (map (Embedding.subtype P) f.support) (map (Embedding.subtype fun (a : α) ↦ ¬P a) g.support)
have 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 sorry ∈ g.support ∧ a_2 = a
Tactic: simp_rw [Finset.disjoint_left, mem_map, forall_exists_index, Embedding.coe_subtype,
      Subtype.forall, Subtype.exists]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Basic (goal)
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 : α
⊢ 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
have pos : ∀ (ha : P a),
  a ∈ (map (Embedding.subtype P) f.support).disjUnion (map (Embedding.subtype fun (a : α) ↦ ¬P a) g.support) sorry ↔
    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
-- Lean 4 proof step from Mathlib.Data.Finsupp.Basic (goal)
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
⊢ 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
have neg : ∀ (ha : ¬P a),
  a ∈ (map (Embedding.subtype P) f.support).disjUnion (map (Embedding.subtype fun (a : α) ↦ ¬P a) g.support) sorry ↔
    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
-- Lean 4 proof step from Mathlib.Data.Finsupp.Basic (goal)
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) = embDomain (Embedding.subtype P) f
have h : ∀ (a : α),
  Eq.{u_12 + 1} (α := M) ((f.extendDomain (P := P) : (a : α) → M) a : M)
    ((embDomain (Embedding.subtype P) f : (a : α) → M) a : M)
Tactic: ext a
-- Lean 4 proof step from Mathlib.Data.Finsupp.Basic (goal)
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 : α
⊢ Eq.{u_12 + 1} (α := M) ((f.extendDomain (P := P) : (a : α) → M) a : M)
    ((embDomain (Embedding.subtype P) f : (a : α) → M) a : M)
have 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)
Tactic: by_cases h : P a
-- Lean 4 proof step from Mathlib.Data.Finsupp.Basic (goal)
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)
⊢ Eq.{u_12 + 1} (α := M) ((f.extendDomain (P := P) : (a : α) → M) a : M)
    ((embDomain (Embedding.subtype P) f : (a : α) → M) a : M)
have 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)
Tactic: by_cases h : P a
-- Lean 4 proof step from Mathlib.Data.Finsupp.Basic (goal)
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)
have 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)
Tactic: refine Eq.trans ?_ (embDomain_apply_self (.subtype P) f (Subtype.mk a h)).symm
-- Lean 4 proof step from Mathlib.Data.Finsupp.Basic (goal)
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
⊢ (subtypeDomain P f).extendDomain (P := P) = f
have h : ∀ (a : α),
  Eq.{u_12 + 1} (α := M) (((subtypeDomain P f).extendDomain (P := P) : (a : α) → M) a : M) ((f : (a : α) → M) a : M)
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Finsupp.Basic (goal)
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 : α
⊢ Eq.{u_12 + 1} (α := M) (((subtypeDomain P f).extendDomain (P := P) : (a : α) → M) a : M) ((f : (a : α) → M) a : M)
have h : ¬P a → Eq.{u_12 + 1} (α := M) (0 : M) ((f : (a : α) → M) a : M)
Tactic: simp only [extendDomain_apply, subtypeDomain_apply, dite_eq_ite, ite_eq_left_iff]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Basic (goal)
Goal:
α : Type u_1
M : Type u_12
inst : Zero M
P : α → Prop
inst_1 : DecidablePred P
a : Subtype P
m : M
⊢ Eq (α := α →₀ M) (extendDomain (P := P) (single a m)) (single (↑a : α) m)
have h : ∀ (a' : α),
  Eq.{u_12 + 1} (α := M) ((extendDomain (P := P) (single a m) : (a : α) → M) a' : M)
    ((single (↑a : α) m : (a : α) → M) a' : M)
Tactic: ext a'
-- Lean 4 proof step from Mathlib.Data.Finsupp.Basic (goal)
Goal:
α : Type u_1
M : Type u_12
inst : Zero M
P : α → Prop
inst_1 : DecidablePred P
a : Subtype P
m : M
a' : α
⊢ Eq.{u_12 + 1} (α := M) ((extendDomain (P := P) (single a m) : (a : α) → M) a' : M)
    ((single (↑a : α) m : (a : α) → M) a' : M)
have h : 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
Cleared hypotheses: a'
-- Lean 4 proof step from Mathlib.Data.Finsupp.Basic (goal)
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)
⊢ Eq.{u_12 + 1} (α := M) ((extendDomain (P := P) (single a m) : (a : α) → M) a' : M)
    ((single (↑a : α) m : (a : α) → M) a' : M)
have 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)
Tactic: obtain rfl | ha := eq_or_ne a' a.val
-- Lean 4 proof step from Mathlib.Data.Finsupp.Basic (goal)
Goal:
α : Type u_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 : AddCommMonoid M
e : α ≃ β
v : α →₀ M
⊢ equivMapDomain e.symm (equivMapDomain e v) = v
have simp_rw : equivMapDomain (Equiv.refl α) v = v
Tactic: simp_rw [← equivMapDomain_trans, Equiv.self_trans_symm]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Basic (goal)
Goal:
α : Type u_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 : AddCommMonoid M
e : α ≃ β
v : β →₀ M
⊢ equivMapDomain e (equivMapDomain e.symm v) = v
have simp_rw : equivMapDomain (Equiv.refl β) v = v
Tactic: simp_rw [← equivMapDomain_trans, Equiv.symm_trans_self]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Basic (goal)
Goal:
ι : Type u_4
M : Type u_5
αs : ι → Type u_12
inst : Zero M
l : (i : ι) × αs i →₀ M
i : ι
x : αs i
⊢ Eq.{u_5 + 1} (α := M) ((l.split (αs := αs) i : (a : αs i) → M) x : M)
    ((l : (a : (i : ι) × αs i) → M) (Sigma.mk (β := fun (i : ι) ↦ αs i) i x) : M)
have rw : Eq.{u_5 + 1} (α := M) ((comapDomain (Sigma.mk (β := αs) i) l sorry : (a : αs i) → M) x : M)
  ((l : (a : (i : ι) × αs i) → M) (Sigma.mk (β := fun (i : ι) ↦ αs i) i x) : M)
Tactic: rw [split, comapDomain_apply]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Basic (goal)
Goal:
ι : Type u_4
M : Type u_5
αs : ι → Type u_12
inst : Zero M
l : (i : ι) × αs i →₀ M
i : ι
x : αs i
rw :
  Eq.{u_5 + 1} (α := M) ((comapDomain (Sigma.mk (β := αs) i) l ⋯ : (a : αs i) → M) x : M)
    ((l : (a : (i : ι) × αs i) → M) (Sigma.mk (β := fun (i : ι) ↦ αs i) i x) : M)
⊢ Eq.{u_5 + 1} (α := M) ((l.split (αs := αs) i : (a : αs i) → M) x : M)
    ((l : (a : (i : ι) × αs i) → M) (Sigma.mk (β := fun (i : ι) ↦ αs i) i x) : M)
have rw₁ : Eq.{u_5 + 1} (α := M) ((l : (a : Sigma αs) → M) (Sigma.mk (β := αs) i x) : M)
  ((l : (a : (i : ι) × αs i) → M) (Sigma.mk (β := fun (i : ι) ↦ αs i) i x) : M)
Tactic: rw [split, comapDomain_apply]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Basic (goal)
Goal:
ι : Type u_4
M : Type u_5
αs : ι → Type u_12
inst : Zero M
l : (i : ι) × αs i →₀ M
i : ι
⊢ i ∈ l.splitSupport (αs := αs) ↔ l.split (αs := αs) i ≠ 0
have rw : (∃ a ∈ l.support, a.fst (β := fun (i : ι) ↦ αs i) = i) ↔
  ∃ (x : αs i),
    x ∈
      { support := l.support.preimage (Sigma.mk (β := αs) i) sorry,
          toFun := fun (a : αs i) ↦ (l : (a : Sigma αs) → M) (Sigma.mk (β := αs) i a), mem_support_toFun := sorry :
          Finsupp.{u_12, u_5} (αs i) M }.support
Tactic: rw [splitSupport, mem_image, Ne, ← support_eq_empty, ← Ne,
    ← Finset.nonempty_iff_ne_empty, split, comapDomain, Finset.Nonempty]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Basic (goal)
Goal:
ι : Type u_4
M : Type u_5
αs : ι → Type u_12
inst : Zero M
l : (i : ι) × αs i →₀ M
i : ι
⊢ i ∈ l.splitSupport (αs := αs) ↔ l.split (αs := αs) i ≠ 0
have classical : (∃ a ∈ l.support, a.fst (β := fun (i : ι) ↦ αs i) = i) ↔
  ∃ (x : αs i),
    x ∈
      { support := l.support.preimage (Sigma.mk (β := αs) i) sorry,
          toFun := fun (a : αs i) ↦ (l : (a : Sigma αs) → M) (Sigma.mk (β := αs) i a), mem_support_toFun := sorry :
          Finsupp.{u_12, u_5} (αs i) M }.support
Tactic: classical rw [splitSupport, mem_image, Ne, ← support_eq_empty, ← Ne,
    ← Finset.nonempty_iff_ne_empty, split, comapDomain, Finset.Nonempty]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Basic (goal)
Goal:
α : Type u_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
αs : ι → Type u_12
inst : Zero M
l : (i : ι) × αs i →₀ M
inst_1 : Zero N
g : (i : ι) → Finsupp.{u_12, u_5} (αs i) M → N
hg : ∀ (i : ι) (x : Finsupp.{u_12, u_5} (αs i) M), x = 0 ↔ g i x = 0
i : ι
⊢ i ∈ l.splitSupport (αs := αs) ↔ g i (l.split (αs := αs) i) ≠ 0
have rw : l.split (αs := αs) i ≠ 0 ↔ g i (l.split (αs := αs) i) ≠ 0
Tactic: rw [mem_splitSupport_iff_nonzero, not_iff_not, hg]
-- Lean 4 proof step from Mathlib.Data.Finsupp.Basic (goal)
Goal:
α : Type u_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
αs : ι → Type u_12
inst : Zero M
l : (i : ι) × αs i →₀ M
inst_1 : Zero N
g : (i : ι) → Finsupp.{u_12, u_5} (αs i) M → N
hg : ∀ (i : ι) (x : Finsupp.{u_12, u_5} (αs i) M), x = 0 ↔ g i x = 0
i : ι
rw : l.split (αs := αs) i ≠ 0 ↔ g i (l.split (αs := αs) i) ≠ 0
⊢ i ∈ l.splitSupport (αs := αs) ↔ g i (l.split (αs := αs) i) ≠ 0
have rw₁ : l.split (αs := αs) i = 0 ↔ g i (l.split (αs := αs) i) = 0
Tactic: rw [mem_splitSupport_iff_nonzero, not_iff_not, hg]