awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Module (goal)
Goal:
ι : Type u
γ : Type w
β : ι → Type v
κ : Type u_1
inst : (i : ι) → Zero (β i)
inst_1 : (i : ι) → SMulZeroClass.{w, v} γ (β i)
h : κ → ι
hh : Function.Injective h
r : γ
f : Π₀ (i : ι), β i
i : κ
h₁ : (comapDomain (β := β) h hh (r • f) : (a : κ) → β (h a)) i = r • (comapDomain (β := β) h hh f : (a : κ) → β (h a)) i
h₂ : (r • f : (a : ι) → β a) (h i) = r • (comapDomain (β := β) h hh f : (a : κ) → β (h a)) i
⊢ (comapDomain (β := β) h hh (r • f) : (a : κ) → β (h a)) i = (r • comapDomain (β := β) h hh f : (a : κ) → β (h a)) i
have h₃ : HSMul.hSMul (β := β (h i)) r ((f : (a : ι) → β a) (h i)) = r • (comapDomain (β := β) h hh f : (a : κ) → β (h a)) i
Tactic: rw [smul_apply, comapDomain_apply, smul_apply, comapDomain_apply]
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Module (goal)
Goal:
ι : Type u
γ : Type w
β : ι → Type v
κ : Type u_1
inst : (i : ι) → Zero (β i)
inst_1 : (i : ι) → SMulZeroClass.{w, v} γ (β i)
h : κ → ι
hh : Function.Injective h
r : γ
f : Π₀ (i : ι), β i
i : κ
h₁ : (comapDomain (β := β) h hh (r • f) : (a : κ) → β (h a)) i = r • (comapDomain (β := β) h hh f : (a : κ) → β (h a)) i
h₂ : (r • f : (a : ι) → β a) (h i) = r • (comapDomain (β := β) h hh f : (a : κ) → β (h a)) i
h₃ : HSMul.hSMul (β := β (h i)) r ((f : (a : ι) → β a) (h i)) = r • (comapDomain (β := β) h hh f : (a : κ) → β (h a)) i
⊢ (comapDomain (β := β) h hh (r • f) : (a : κ) → β (h a)) i = (r • comapDomain (β := β) h hh f : (a : κ) → β (h a)) i
have h₄ : HSMul.hSMul (β := β (h i)) r ((f : (a : ι) → β a) (h i)) = HSMul.hSMul (β := β (h i)) r ((f : (a : ι) → β a) (h i))
Tactic: rw [smul_apply, comapDomain_apply, smul_apply, comapDomain_apply]
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Module (goal)
Goal:
ι : Type u
γ : Type w
β : ι → Type v
κ : Type u_1
inst : (i : ι) → Zero (β i)
inst_1 : (i : ι) → SMulZeroClass.{w, v} γ (β i)
h : κ → ι
h' : ι → κ
hh' : Function.LeftInverse h' h
r : γ
f : Π₀ (i : ι), β i
⊢ comapDomain' (β := β) h hh' (r • f) = r • comapDomain' (β := β) h hh' f
have h₁ : ∀ (i : κ),
  (comapDomain' (β := β) h hh' (r • f) : (a : κ) → β (h a)) i =
    (r • comapDomain' (β := β) h hh' f : (a : κ) → β (h a)) i
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Module (goal)
Goal:
ι : Type u
γ : Type w
β : ι → Type v
κ : Type u_1
inst : (i : ι) → Zero (β i)
inst_1 : (i : ι) → SMulZeroClass.{w, v} γ (β i)
h : κ → ι
h' : ι → κ
hh' : Function.LeftInverse h' h
r : γ
f : Π₀ (i : ι), β i
i : κ
⊢ (comapDomain' (β := β) h hh' (r • f) : (a : κ) → β (h a)) i =
    (r • comapDomain' (β := β) h hh' f : (a : κ) → β (h a)) i
have h₁ : (comapDomain' (β := β) h hh' (r • f) : (a : κ) → β (h a)) i = r • (comapDomain' (β := β) h hh' f : (a : κ) → β (h a)) i
Tactic: rw [smul_apply, comapDomain'_apply, smul_apply, comapDomain'_apply]
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Module (goal)
Goal:
ι : Type u
γ : Type w
β : ι → Type v
κ : Type u_1
inst : (i : ι) → Zero (β i)
inst_1 : (i : ι) → SMulZeroClass.{w, v} γ (β i)
h : κ → ι
h' : ι → κ
hh' : Function.LeftInverse h' h
r : γ
f : Π₀ (i : ι), β i
i : κ
h₁ :
  (comapDomain' (β := β) h hh' (r • f) : (a : κ) → β (h a)) i =
    r • (comapDomain' (β := β) h hh' f : (a : κ) → β (h a)) i
⊢ (comapDomain' (β := β) h hh' (r • f) : (a : κ) → β (h a)) i =
    (r • comapDomain' (β := β) h hh' f : (a : κ) → β (h a)) i
have h₂ : (r • f : (a : ι) → β a) (h i) = r • (comapDomain' (β := β) h hh' f : (a : κ) → β (h a)) i
Tactic: rw [smul_apply, comapDomain'_apply, smul_apply, comapDomain'_apply]
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Module (goal)
Goal:
ι : Type u
γ : Type w
β : ι → Type v
κ : Type u_1
inst : (i : ι) → Zero (β i)
inst_1 : (i : ι) → SMulZeroClass.{w, v} γ (β i)
h : κ → ι
h' : ι → κ
hh' : Function.LeftInverse h' h
r : γ
f : Π₀ (i : ι), β i
i : κ
h₁ :
  (comapDomain' (β := β) h hh' (r • f) : (a : κ) → β (h a)) i =
    r • (comapDomain' (β := β) h hh' f : (a : κ) → β (h a)) i
h₂ : (r • f : (a : ι) → β a) (h i) = r • (comapDomain' (β := β) h hh' f : (a : κ) → β (h a)) i
⊢ (comapDomain' (β := β) h hh' (r • f) : (a : κ) → β (h a)) i =
    (r • comapDomain' (β := β) h hh' f : (a : κ) → β (h a)) i
have h₃ : HSMul.hSMul (β := β (h i)) r ((f : (a : ι) → β a) (h i)) = r • (comapDomain' (β := β) h hh' f : (a : κ) → β (h a)) i
Tactic: rw [smul_apply, comapDomain'_apply, smul_apply, comapDomain'_apply]
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Module (goal)
Goal:
ι : Type u
γ : Type w
β : ι → Type v
κ : Type u_1
inst : (i : ι) → Zero (β i)
inst_1 : (i : ι) → SMulZeroClass.{w, v} γ (β i)
h : κ → ι
h' : ι → κ
hh' : Function.LeftInverse h' h
r : γ
f : Π₀ (i : ι), β i
i : κ
h₁ :
  (comapDomain' (β := β) h hh' (r • f) : (a : κ) → β (h a)) i =
    r • (comapDomain' (β := β) h hh' f : (a : κ) → β (h a)) i
h₂ : (r • f : (a : ι) → β a) (h i) = r • (comapDomain' (β := β) h hh' f : (a : κ) → β (h a)) i
h₃ :
  HSMul.hSMul (β := β (h i)) r ((f : (a : ι) → β a) (h i)) = r • (comapDomain' (β := β) h hh' f : (a : κ) → β (h a)) i
⊢ (comapDomain' (β := β) h hh' (r • f) : (a : κ) → β (h a)) i =
    (r • comapDomain' (β := β) h hh' f : (a : κ) → β (h a)) i
have h₄ : HSMul.hSMul (β := β (h i)) r ((f : (a : ι) → β a) (h i)) = HSMul.hSMul (β := β (h i)) r ((f : (a : ι) → β a) (h i))
Tactic: rw [smul_apply, comapDomain'_apply, smul_apply, comapDomain'_apply]
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Multiset (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a : α
n : ℕ
⊢ Eq (α := Π₀ (x : α), ℕ) ((toDFinsupp : (a : Multiset α) → Π₀ (x : α), ℕ) (replicate n a) : Π₀ (x : α), ℕ)
    (DFinsupp.single (β := fun (i : α) ↦ ℕ) a n : Π₀ (i : α), ℕ)
have h : ∀ (i : α),
  (((toDFinsupp : (a : Multiset α) → Π₀ (x : α), ℕ) (replicate n a) : Π₀ (x : α), ℕ) : (a : α) → ℕ) i =
    (DFinsupp.single (β := fun (i : α) ↦ ℕ) a n : (a : α) → ℕ) i
Tactic: ext i
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Multiset (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a : α
n : ℕ
i : α
⊢ (((toDFinsupp : (a : Multiset α) → Π₀ (x : α), ℕ) (replicate n a) : Π₀ (x : α), ℕ) : (a : α) → ℕ) i =
    (DFinsupp.single (β := fun (i : α) ↦ ℕ) a n : (a : α) → ℕ) i
have h : count i (replicate n a) = (DFinsupp.single (β := fun (i : α) ↦ ℕ) a n : (a : α) → ℕ) i
Tactic: dsimp [toDFinsupp]
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Multiset (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a : α
⊢ Eq (α := Π₀ (x : α), ℕ) ((toDFinsupp : (a : Multiset α) → Π₀ (x : α), ℕ) {a})
    (DFinsupp.single (β := fun (i : α) ↦ ℕ) a 1)
have rw : Eq (α := Π₀ (x : α), ℕ) ((toDFinsupp : (a : Multiset α) → Π₀ (x : α), ℕ) (replicate 1 a) : Π₀ (x : α), ℕ)
  (DFinsupp.single (β := fun (i : α) ↦ ℕ) a 1 : Π₀ (i : α), ℕ)
Tactic: rw [← replicate_one, toDFinsupp_replicate]
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Multiset (goal)
Goal:
α : Type u_1
inst : DecidableEq α
a : α
rw :
  Eq (α := Π₀ (x : α), ℕ) ((toDFinsupp : (a : Multiset α) → Π₀ (x : α), ℕ) (replicate 1 a) : Π₀ (x : α), ℕ)
    (DFinsupp.single (β := fun (i : α) ↦ ℕ) a 1 : Π₀ (i : α), ℕ)
⊢ Eq (α := Π₀ (x : α), ℕ) ((toDFinsupp : (a : Multiset α) → Π₀ (x : α), ℕ) {a})
    (DFinsupp.single (β := fun (i : α) ↦ ℕ) a 1)
have rw₁ : Eq (α := Π₀ (x : α), ℕ) (DFinsupp.single (β := fun (i : α) ↦ ℕ) a 1) (DFinsupp.single (β := fun (i : α) ↦ ℕ) a 1)
Tactic: rw [← replicate_one, toDFinsupp_replicate]
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Multiset (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s t : Multiset α
⊢ Eq.{u_1 + 1} (α := Multiset α →+ Multiset α) (AddMonoidHom.comp DFinsupp.toMultiset toDFinsupp)
    (AddMonoidHom.id (Multiset α))
have h : ∀ (x a : α),
  count a ((AddMonoidHom.comp DFinsupp.toMultiset toDFinsupp : (a : Multiset α) → Multiset α) {x}) =
    count a ((AddMonoidHom.id (Multiset α) : (a : Multiset α) → Multiset α) {x})
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Multiset (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s t : Multiset α
⊢ Eq.{u_1 + 1} (α := (Π₀ (x : α), ℕ) →+ Π₀ (x : α), ℕ) (AddMonoidHom.comp toDFinsupp DFinsupp.toMultiset)
    (AddMonoidHom.id (Π₀ (x : α), ℕ))
have H : ∀ (x i : α),
  (((AddMonoidHom.comp (AddMonoidHom.comp toDFinsupp DFinsupp.toMultiset) (DFinsupp.singleAddHom (fun (i : α) ↦ ℕ) x) :
              (a : ℕ) → Π₀ (x : α), ℕ)
            1 :
          Π₀ (x : α), ℕ) :
        (a : α) → ℕ)
      i =
    ((((AddMonoidHom.comp (AddMonoidHom.id (Π₀ (x : α), ℕ)) (DFinsupp.singleAddHom (fun (i : α) ↦ ℕ) x) :
                ℕ →+ Π₀ (x : α), ℕ) :
              (a : ℕ) → Π₀ (x : α), ℕ)
            1 :
          Π₀ (x : α), ℕ) :
        (a : α) → ℕ)
      i
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Multiset (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s t : Multiset α
⊢ Eq (α := Π₀ (x : α), ℕ) ((toDFinsupp : (a : Multiset α) → Π₀ (x : α), ℕ) (s ∩ t) : Π₀ (x : α), ℕ)
    ((toDFinsupp : (a : Multiset α) → Π₀ (x : α), ℕ) s ⊓ (toDFinsupp : (a : Multiset α) → Π₀ (x : α), ℕ) t :
      Π₀ (x : α), ℕ)
have h : ∀ (i : α),
  (((toDFinsupp : (a : Multiset α) → Π₀ (x : α), ℕ) (s ∩ t) : Π₀ (x : α), ℕ) : (a : α) → ℕ) i =
    (((toDFinsupp : (a : Multiset α) → Π₀ (x : α), ℕ) s ⊓ (toDFinsupp : (a : Multiset α) → Π₀ (x : α), ℕ) t :
          Π₀ (x : α), ℕ) :
        (a : α) → ℕ)
      i
Tactic: ext i
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Multiset (goal)
Goal:
α : Type u_1
inst : DecidableEq α
s t : Multiset α
⊢ Eq (α := Π₀ (x : α), ℕ) ((toDFinsupp : (a : Multiset α) → Π₀ (x : α), ℕ) (s ∪ t) : Π₀ (x : α), ℕ)
    ((toDFinsupp : (a : Multiset α) → Π₀ (x : α), ℕ) s ⊔ (toDFinsupp : (a : Multiset α) → Π₀ (x : α), ℕ) t :
      Π₀ (x : α), ℕ)
have h : ∀ (i : α),
  (((toDFinsupp : (a : Multiset α) → Π₀ (x : α), ℕ) (s ∪ t) : Π₀ (x : α), ℕ) : (a : α) → ℕ) i =
    (((toDFinsupp : (a : Multiset α) → Π₀ (x : α), ℕ) s ⊔ (toDFinsupp : (a : Multiset α) → Π₀ (x : α), ℕ) t :
          Π₀ (x : α), ℕ) :
        (a : α) → ℕ)
      i
Tactic: ext i
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Multiset (goal)
Goal:
α : Type u_1
inst : DecidableEq α
f g : Π₀ (_a : α), ℕ
⊢ LE.le (α := Multiset α) ((toMultiset : (a : Π₀ (x : α), ℕ) → Multiset α) f : Multiset α)
      ((toMultiset : (a : Π₀ (x : α), ℕ) → Multiset α) g : Multiset α) ↔
    f ≤ g
have simp_rw : LE.le (α := Π₀ (x : α), ℕ)
    ((Multiset.toDFinsupp : (a : Multiset α) → Π₀ (x : α), ℕ) ((toMultiset : (a : Π₀ (x : α), ℕ) → Multiset α) f) :
      Π₀ (x : α), ℕ)
    ((Multiset.toDFinsupp : (a : Multiset α) → Π₀ (x : α), ℕ) ((toMultiset : (a : Π₀ (x : α), ℕ) → Multiset α) g) :
      Π₀ (x : α), ℕ) ↔
  f ≤ g
Tactic: simp_rw [← Multiset.toDFinsupp_le_toDFinsupp, toMultiset_toDFinsupp]
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Multiset (goal)
Goal:
α : Type u_1
inst : DecidableEq α
f g : Π₀ (_a : α), ℕ
⊢ LT.lt (α := Multiset α) ((toMultiset : (a : Π₀ (x : α), ℕ) → Multiset α) f : Multiset α)
      ((toMultiset : (a : Π₀ (x : α), ℕ) → Multiset α) g : Multiset α) ↔
    f < g
have simp_rw : LT.lt (α := Π₀ (x : α), ℕ)
    ((Multiset.toDFinsupp : (a : Multiset α) → Π₀ (x : α), ℕ) ((toMultiset : (a : Π₀ (x : α), ℕ) → Multiset α) f) :
      Π₀ (x : α), ℕ)
    ((Multiset.toDFinsupp : (a : Multiset α) → Π₀ (x : α), ℕ) ((toMultiset : (a : Π₀ (x : α), ℕ) → Multiset α) g) :
      Π₀ (x : α), ℕ) ↔
  f < g
Tactic: simp_rw [← Multiset.toDFinsupp_lt_toDFinsupp, toMultiset_toDFinsupp]
-- Lean 4 proof step from Mathlib.Data.DFinsupp.NeLocus (goal)
Goal:
α : Type u_1
N : α → Type u_2
inst : DecidableEq α
inst_1 : (a : α) → DecidableEq (N a)
inst_2 : (a : α) → Zero (N a)
f g : Π₀ (a : α), N a
⊢ f.neLocus (N := N) g = g.neLocus (N := N) f
have simp_rw : {x ∈ f.support (β := N) ∪ g.support (β := N) | (f : (a : α) → N a) x ≠ (g : (a : α) → N a) x} =
  {x ∈ g.support (β := N) ∪ f.support (β := N) | (g : (a : α) → N a) x ≠ (f : (a : α) → N a) x}
Tactic: simp_rw [neLocus, Finset.union_comm, ne_comm]
-- Lean 4 proof step from Mathlib.Data.DFinsupp.NeLocus (goal)
Goal:
α : Type u_1
N : α → Type u_2
inst : DecidableEq α
inst_1 : (a : α) → DecidableEq (N a)
inst_2 : (a : α) → Zero (N a)
f g : Π₀ (a : α), N a
simp_rw :
  {x ∈ f.support (β := N) ∪ g.support (β := N) | (f : (a : α) → N a) x ≠ (g : (a : α) → N a) x} =
    {x ∈ g.support (β := N) ∪ f.support (β := N) | (g : (a : α) → N a) x ≠ (f : (a : α) → N a) x}
⊢ f.neLocus (N := N) g = g.neLocus (N := N) f
have simp_rw₁ : {x ∈ f.support (β := N) ∪ g.support (β := N) | (f : (a : α) → N a) x ≠ (g : (a : α) → N a) x} =
  {x ∈ f.support (β := N) ∪ g.support (β := N) | (g : (a : α) → N a) x ≠ (f : (a : α) → N a) x}
Tactic: simp_rw [neLocus, Finset.union_comm, ne_comm]
-- Lean 4 proof step from Mathlib.Data.DFinsupp.NeLocus (goal)
Goal:
α : Type u_1
N : α → Type u_2
inst : DecidableEq α
inst_1 : (a : α) → DecidableEq (N a)
inst_2 : (a : α) → Zero (N a)
f : Π₀ (a : α), N a
⊢ f.neLocus (N := N) 0 = f.support (β := N)
have h : ∀ (a : α), a ∈ f.neLocus (N := N) 0 ↔ a ∈ f.support (β := N)
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.DFinsupp.NeLocus (goal)
Goal:
α : Type u_1
N : α → Type u_2
inst : DecidableEq α
inst_1 : (a : α) → DecidableEq (N a)
inst_2 : (a : α) → Zero (N a)
f : Π₀ (a : α), N a
a : α
⊢ a ∈ f.neLocus (N := N) 0 ↔ a ∈ f.support (β := N)
have h : (f : (a : α) → N a) a ≠ (0 : (a : α) → N a) a ↔ a ∈ f.support (β := N)
Tactic: rw [mem_neLocus, mem_support_iff, coe_zero, Pi.zero_apply]
-- Lean 4 proof step from Mathlib.Data.DFinsupp.NeLocus (goal)
Goal:
α : Type u_1
N : α → Type u_2
inst : DecidableEq α
inst_1 : (a : α) → DecidableEq (N a)
inst_2 : (a : α) → Zero (N a)
f : Π₀ (a : α), N a
a : α
h : (f : (a : α) → N a) a ≠ (0 : (a : α) → N a) a ↔ a ∈ f.support (β := N)
⊢ a ∈ f.neLocus (N := N) 0 ↔ a ∈ f.support (β := N)
have h₁ : (f : (a : α) → N a) a ≠ (0 : (a : α) → N a) a ↔ (f : (a : α) → N a) a ≠ 0
Tactic: rw [mem_neLocus, mem_support_iff, coe_zero, Pi.zero_apply]
-- Lean 4 proof step from Mathlib.Data.DFinsupp.NeLocus (goal)
Goal:
α : Type u_1
N : α → Type u_2
inst : DecidableEq α
inst_1 : (a : α) → DecidableEq (N a)
inst_2 : (a : α) → Zero (N a)
f : Π₀ (a : α), N a
a : α
h : (f : (a : α) → N a) a ≠ (0 : (a : α) → N a) a ↔ a ∈ f.support (β := N)
h₁ : (f : (a : α) → N a) a ≠ (0 : (a : α) → N a) a ↔ (f : (a : α) → N a) a ≠ 0
⊢ a ∈ f.neLocus (N := N) 0 ↔ a ∈ f.support (β := N)
have h₂ : (f : (a : α) → N a) a ≠ 0 a ↔ (f : (a : α) → N a) a ≠ 0
Tactic: rw [mem_neLocus, mem_support_iff, coe_zero, Pi.zero_apply]
-- Lean 4 proof step from Mathlib.Data.DFinsupp.NeLocus (goal)
Goal:
α : Type u_1
N : α → Type u_2
inst : DecidableEq α
inst_1 : (a : α) → DecidableEq (N a)
inst_2 : (a : α) → Zero (N a)
f : Π₀ (a : α), N a
a : α
h : (f : (a : α) → N a) a ≠ (0 : (a : α) → N a) a ↔ a ∈ f.support (β := N)
h₁ : (f : (a : α) → N a) a ≠ (0 : (a : α) → N a) a ↔ (f : (a : α) → N a) a ≠ 0
h₂ : (f : (a : α) → N a) a ≠ 0 a ↔ (f : (a : α) → N a) a ≠ 0
⊢ a ∈ f.neLocus (N := N) 0 ↔ a ∈ f.support (β := N)
have h₃ : (f : (a : α) → N a) a ≠ 0 ↔ (f : (a : α) → N a) a ≠ 0
Tactic: rw [mem_neLocus, mem_support_iff, coe_zero, Pi.zero_apply]
-- Lean 4 proof step from Mathlib.Data.DFinsupp.NeLocus (goal)
Goal:
α : Type u_1
N : α → Type u_2
inst : DecidableEq α
M : α → Type u_3
P : α → Type u_4
inst_1 : (a : α) → Zero (N a)
inst_2 : (a : α) → Zero (M a)
inst_3 : (a : α) → Zero (P a)
inst_4 : (a : α) → DecidableEq (N a)
inst_5 : (a : α) → DecidableEq (P a)
F : (a : α) → M a → N a → P a
F0 : ∀ (a : α), F a 0 0 = 0
f : Π₀ (a : α), M a
g₁ g₂ : Π₀ (a : α), N a
hF : ∀ (a : α) (f : M a), Function.Injective.{u_2 + 1, u_4 + 1} (β := P a) fun (g : N a) ↦ F a f g
⊢ (zipWith (β := P) (β₁ := M) (β₂ := N) F F0 f g₁).neLocus (N := P) (zipWith (β := P) (β₁ := M) (β₂ := N) F F0 f g₂) =
    g₁.neLocus (N := N) g₂
have h : ∀ (a : α),
  a ∈
      (zipWith (β := P) (β₁ := M) (β₂ := N) F F0 f g₁).neLocus (N := P)
        (zipWith (β := P) (β₁ := M) (β₂ := N) F F0 f g₂) ↔
    a ∈ g₁.neLocus (N := N) g₂
Tactic: ext a
-- Lean 4 proof step from Mathlib.Data.DFinsupp.NeLocus (goal)
Goal:
α : Type u_1
N : α → Type u_2
inst : DecidableEq α
M : α → Type u_3
P : α → Type u_4
inst_1 : (a : α) → Zero (N a)
inst_2 : (a : α) → Zero (M a)
inst_3 : (a : α) → Zero (P a)
inst_4 : (a : α) → DecidableEq (M a)
inst_5 : (a : α) → DecidableEq (P a)
F : (a : α) → M a → N a → P a
F0 : ∀ (a : α), F a 0 0 = 0
f₁ f₂ : Π₀ (a : α), M a
g : Π₀ (a : α), N a
hF : ∀ (a : α) (g : N a), Function.Injective.{u_3 + 1, u_4 + 1} (β := P a) fun (f : M a) ↦ F a f g
⊢ (zipWith (β := P) (β₁ := M) (β₂ := N) F F0 f₁ g).neLocus (N := P) (zipWith (β := P) (β₁ := M) (β₂ := N) F F0 f₂ g) =
    f₁.neLocus (N := M) f₂
have h : ∀ (a : α),
  a ∈
      (zipWith (β := P) (β₁ := M) (β₂ := N) F F0 f₁ g).neLocus (N := P)
        (zipWith (β := P) (β₁ := M) (β₂ := N) F F0 f₂ g) ↔
    a ∈ f₁.neLocus (N := M) f₂
Tactic: ext a
-- Lean 4 proof step from Mathlib.Data.DFinsupp.NeLocus (goal)
Goal:
α : Type u_1
N : α → Type u_2
inst : DecidableEq α
M : α → Type u_3
inst_1 : (a : α) → Zero (N a)
inst_2 : (a : α) → Zero (M a)
inst_3 : (a : α) → DecidableEq (N a)
inst_4 : (a : α) → DecidableEq (M a)
f g : Π₀ (a : α), N a
F : (a : α) → N a → M a
F0 : ∀ (a : α), F a 0 = 0
hF : ∀ (a : α), Function.Injective (F a)
⊢ (mapRange (β₁ := N) (β₂ := M) F F0 f).neLocus (N := M) (mapRange (β₁ := N) (β₂ := M) F F0 g) = f.neLocus (N := N) g
have h : ∀ (a : α),
  a ∈ (mapRange (β₁ := N) (β₂ := M) F F0 f).neLocus (N := M) (mapRange (β₁ := N) (β₂ := M) F F0 g) ↔
    a ∈ f.neLocus (N := N) g
Tactic: ext a
-- Lean 4 proof step from Mathlib.Data.DFinsupp.NeLocus (goal)
Goal:
α : Type u_1
N : α → Type u_2
inst : DecidableEq α
inst_1 : (a : α) → DecidableEq (N a)
inst_2 : (a : α) → AddGroup (N a)
f g : Π₀ (a : α), N a
⊢ (-f).neLocus (N := N) g = f.neLocus (N := N) (-g)
have rw : (- -f).neLocus (N := N) (-g) = f.neLocus (N := N) (-g)
Tactic: rw [← neLocus_neg_neg, neg_neg]
-- Lean 4 proof step from Mathlib.Data.DFinsupp.NeLocus (goal)
Goal:
α : Type u_1
N : α → Type u_2
inst : DecidableEq α
inst_1 : (a : α) → DecidableEq (N a)
inst_2 : (a : α) → AddGroup (N a)
f g : Π₀ (a : α), N a
rw : (- -f).neLocus (N := N) (-g) = f.neLocus (N := N) (-g)
⊢ (-f).neLocus (N := N) g = f.neLocus (N := N) (-g)
have rw₁ : f.neLocus (N := N) (-g) = f.neLocus (N := N) (-g)
Tactic: rw [← neLocus_neg_neg, neg_neg]
-- Lean 4 proof step from Mathlib.Data.DFinsupp.NeLocus (goal)
Goal:
α : Type u_1
N : α → Type u_2
inst : DecidableEq α
inst_1 : (a : α) → DecidableEq (N a)
inst_2 : (a : α) → AddGroup (N a)
f g : Π₀ (a : α), N a
⊢ f.neLocus (N := N) g = (f - g).support (β := N)
have rw : (f + -g).neLocus (N := N) (g + -g) = (f - g).support (β := N)
Tactic: rw [← @neLocus_add_right α N _ _ _ _ _ (-g), add_neg_cancel, neLocus_zero_right, sub_eq_add_neg]
-- Lean 4 proof step from Mathlib.Data.DFinsupp.NeLocus (goal)
Goal:
α : Type u_1
N : α → Type u_2
inst : DecidableEq α
inst_1 : (a : α) → DecidableEq (N a)
inst_2 : (a : α) → AddGroup (N a)
f g : Π₀ (a : α), N a
rw : (f + -g).neLocus (N := N) (g + -g) = (f - g).support (β := N)
⊢ f.neLocus (N := N) g = (f - g).support (β := N)
have rw₁ : (f + -g).neLocus (N := N) 0 = (f - g).support (β := N)
Tactic: rw [← @neLocus_add_right α N _ _ _ _ _ (-g), add_neg_cancel, neLocus_zero_right, sub_eq_add_neg]
-- Lean 4 proof step from Mathlib.Data.DFinsupp.NeLocus (goal)
Goal:
α : Type u_1
N : α → Type u_2
inst : DecidableEq α
inst_1 : (a : α) → DecidableEq (N a)
inst_2 : (a : α) → AddGroup (N a)
f g : Π₀ (a : α), N a
rw : (f + -g).neLocus (N := N) (g + -g) = (f - g).support (β := N)
rw₁ : (f + -g).neLocus (N := N) 0 = (f - g).support (β := N)
⊢ f.neLocus (N := N) g = (f - g).support (β := N)
have rw₂ : (f + -g).support (β := N) = (f - g).support (β := N)
Tactic: rw [← @neLocus_add_right α N _ _ _ _ _ (-g), add_neg_cancel, neLocus_zero_right, sub_eq_add_neg]
-- Lean 4 proof step from Mathlib.Data.DFinsupp.NeLocus (goal)
Goal:
α : Type u_1
N : α → Type u_2
inst : DecidableEq α
inst_1 : (a : α) → DecidableEq (N a)
inst_2 : (a : α) → AddGroup (N a)
f g : Π₀ (a : α), N a
rw : (f + -g).neLocus (N := N) (g + -g) = (f - g).support (β := N)
rw₁ : (f + -g).neLocus (N := N) 0 = (f - g).support (β := N)
rw₂ : (f + -g).support (β := N) = (f - g).support (β := N)
⊢ f.neLocus (N := N) g = (f - g).support (β := N)
have rw₃ : (f + -g).support (β := N) = (f + -g).support (β := N)
Tactic: rw [← @neLocus_add_right α N _ _ _ _ _ (-g), add_neg_cancel, neLocus_zero_right, sub_eq_add_neg]
-- Lean 4 proof step from Mathlib.Data.DFinsupp.NeLocus (goal)
Goal:
α : Type u_1
N : α → Type u_2
inst : DecidableEq α
inst_1 : (a : α) → DecidableEq (N a)
inst_2 : (a : α) → AddGroup (N a)
f g : Π₀ (a : α), N a
⊢ f.neLocus (N := N) (f + g) = g.support (β := N)
have rw : f.neLocus (N := N) (f + g) = neLocus (N := N) 0 g
Tactic: rw [← neLocus_zero_left, ← @neLocus_add_left α N _ _ _ f 0 g, add_zero]
-- Lean 4 proof step from Mathlib.Data.DFinsupp.NeLocus (goal)
Goal:
α : Type u_1
N : α → Type u_2
inst : DecidableEq α
inst_1 : (a : α) → DecidableEq (N a)
inst_2 : (a : α) → AddGroup (N a)
f g : Π₀ (a : α), N a
rw : f.neLocus (N := N) (f + g) = neLocus (N := N) 0 g
⊢ f.neLocus (N := N) (f + g) = g.support (β := N)
have rw₁ : f.neLocus (N := N) (f + g) = (f + 0).neLocus (N := N) (f + g)
Tactic: rw [← neLocus_zero_left, ← @neLocus_add_left α N _ _ _ f 0 g, add_zero]
-- Lean 4 proof step from Mathlib.Data.DFinsupp.NeLocus (goal)
Goal:
α : Type u_1
N : α → Type u_2
inst : DecidableEq α
inst_1 : (a : α) → DecidableEq (N a)
inst_2 : (a : α) → AddGroup (N a)
f g : Π₀ (a : α), N a
rw : f.neLocus (N := N) (f + g) = neLocus (N := N) 0 g
rw₁ : f.neLocus (N := N) (f + g) = (f + 0).neLocus (N := N) (f + g)
⊢ f.neLocus (N := N) (f + g) = g.support (β := N)
have rw₂ : f.neLocus (N := N) (f + g) = f.neLocus (N := N) (f + g)
Tactic: rw [← neLocus_zero_left, ← @neLocus_add_left α N _ _ _ f 0 g, add_zero]
-- Lean 4 proof step from Mathlib.Data.DFinsupp.NeLocus (goal)
Goal:
α : Type u_1
N : α → Type u_2
inst : DecidableEq α
inst_1 : (a : α) → DecidableEq (N a)
inst_2 : (a : α) → AddGroup (N a)
f g : Π₀ (a : α), N a
⊢ (f + g).neLocus (N := N) f = g.support (β := N)
have rw : f.neLocus (N := N) (f + g) = g.support (β := N)
Tactic: rw [neLocus_comm, neLocus_self_add_right]
-- Lean 4 proof step from Mathlib.Data.DFinsupp.NeLocus (goal)
Goal:
α : Type u_1
N : α → Type u_2
inst : DecidableEq α
inst_1 : (a : α) → DecidableEq (N a)
inst_2 : (a : α) → AddGroup (N a)
f g : Π₀ (a : α), N a
rw : f.neLocus (N := N) (f + g) = g.support (β := N)
⊢ (f + g).neLocus (N := N) f = g.support (β := N)
have rw₁ : g.support (β := N) = g.support (β := N)
Tactic: rw [neLocus_comm, neLocus_self_add_right]
-- Lean 4 proof step from Mathlib.Data.DFinsupp.NeLocus (goal)
Goal:
α : Type u_1
N : α → Type u_2
inst : DecidableEq α
inst_1 : (a : α) → DecidableEq (N a)
inst_2 : (a : α) → AddGroup (N a)
f g : Π₀ (a : α), N a
⊢ f.neLocus (N := N) (f - g) = g.support (β := N)
have rw : f.neLocus (N := N) (f + -g) = g.support (β := N)
Tactic: rw [sub_eq_add_neg, neLocus_self_add_right, support_neg]
-- Lean 4 proof step from Mathlib.Data.DFinsupp.NeLocus (goal)
Goal:
α : Type u_1
N : α → Type u_2
inst : DecidableEq α
inst_1 : (a : α) → DecidableEq (N a)
inst_2 : (a : α) → AddGroup (N a)
f g : Π₀ (a : α), N a
rw : f.neLocus (N := N) (f + -g) = g.support (β := N)
⊢ f.neLocus (N := N) (f - g) = g.support (β := N)
have rw₁ : (-g).support (β := N) = g.support (β := N)
Tactic: rw [sub_eq_add_neg, neLocus_self_add_right, support_neg]
-- Lean 4 proof step from Mathlib.Data.DFinsupp.NeLocus (goal)
Goal:
α : Type u_1
N : α → Type u_2
inst : DecidableEq α
inst_1 : (a : α) → DecidableEq (N a)
inst_2 : (a : α) → AddGroup (N a)
f g : Π₀ (a : α), N a
rw : f.neLocus (N := N) (f + -g) = g.support (β := N)
rw₁ : (-g).support (β := N) = g.support (β := N)
⊢ f.neLocus (N := N) (f - g) = g.support (β := N)
have rw₂ : g.support (β := N) = g.support (β := N)
Tactic: rw [sub_eq_add_neg, neLocus_self_add_right, support_neg]
-- Lean 4 proof step from Mathlib.Data.DFinsupp.NeLocus (goal)
Goal:
α : Type u_1
N : α → Type u_2
inst : DecidableEq α
inst_1 : (a : α) → DecidableEq (N a)
inst_2 : (a : α) → AddGroup (N a)
f g : Π₀ (a : α), N a
⊢ (f - g).neLocus (N := N) f = g.support (β := N)
have rw : f.neLocus (N := N) (f - g) = g.support (β := N)
Tactic: rw [neLocus_comm, neLocus_self_sub_right]