awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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_sub_right]
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Order (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → Zero (α i)
inst_1 : (i : ι) → Lattice (α i)
f g : Π₀ (i : ι), α i
inst_2 : DecidableEq ι
inst_3 : (i : ι) → (x : α i) → Decidable (x ≠ 0)
⊢ (↑((f ⊓ g).support (β := α) ∪ (f ⊔ g).support (β := α)) : Set ι)ᶜ =
    (↑(f.support (β := α) ∪ g.support (β := α)) : Set ι)ᶜ
have h : ∀ (x : ι),
  x ∈ (↑((f ⊓ g).support (β := α) ∪ (f ⊔ g).support (β := α)) : Set ι)ᶜ ↔
    x ∈ (↑(f.support (β := α) ∪ g.support (β := α)) : Set ι)ᶜ
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Order (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → AddCommMonoid (α i)
inst_1 : (i : ι) → PartialOrder (α i)
inst_2 : ∀ (i : ι), CanonicallyOrderedAdd.{u_2} (α i)
inst_3 : DecidableEq ι
inst_4 : (i : ι) → (x : α i) → Decidable (x ≠ 0)
f g : Π₀ (i : ι), α i
h : f ≤ g
a : ι
ha : a ∈ f.support (β := α)
⊢ a ∈ g.support (β := α)
have rw : ∀ (ha : 0 < (f : (a : ι) → α a) a), 0 < (g : (a : ι) → α a) a
Tactic: rw [mem_support_iff, ← pos_iff_ne_zero] at ha ⊢
Cleared hypotheses: ha
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Order (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → AddCommMonoid (α i)
inst_1 : (i : ι) → PartialOrder (α i)
inst_2 : ∀ (i : ι), CanonicallyOrderedAdd.{u_2} (α i)
inst_3 : (i : ι) → Sub (α i)
inst_4 : ∀ (i : ι), OrderedSub.{u_2} (α i)
f g : Π₀ (i : ι), α i
⊢ (⇑(f - g) : (a : ι) → α a) = (⇑f : (a : ι) → α a) - (⇑g : (a : ι) → α a)
have h : ∀ (i : ι), (f - g : (a : ι) → α a) i = ((⇑f : (a : ι) → α a) - (⇑g : (a : ι) → α a)) i
Tactic: ext i
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Order (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → AddCommMonoid (α i)
inst_1 : (i : ι) → PartialOrder (α i)
inst_2 : ∀ (i : ι), CanonicallyOrderedAdd.{u_2} (α i)
inst_3 : (i : ι) → Sub (α i)
inst_4 : ∀ (i : ι), OrderedSub.{u_2} (α i)
f_1 g_1 : Π₀ (i : ι), α i
i : ι
a b : α i
inst_5 : ∀ (i : ι), AddLeftMono.{u_2} (α i)
f g : Π₀ (i : ι), α i
h : f ≤ g
⊢ ∃ (c : Π₀ (i : ι), α i), g = f + c
have exists : g = f + (g - f)
Tactic: exists g - f
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Order (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → AddCommMonoid (α i)
inst_1 : (i : ι) → PartialOrder (α i)
inst_2 : ∀ (i : ι), CanonicallyOrderedAdd.{u_2} (α i)
inst_3 : (i : ι) → Sub (α i)
inst_4 : ∀ (i : ι), OrderedSub.{u_2} (α i)
f_1 g_1 : Π₀ (i : ι), α i
i : ι
a b : α i
inst_5 : ∀ (i : ι), AddLeftMono.{u_2} (α i)
f g : Π₀ (i : ι), α i
h : f ≤ g
⊢ g = f + (g - f)
have h₁ : ∀ (i : ι), (g : (a : ι) → α a) i = (f + (g - f) : (a : ι) → α a) i
Tactic: ext i
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Order (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → AddCommMonoid (α i)
inst_1 : (i : ι) → PartialOrder (α i)
inst_2 : ∀ (i : ι), CanonicallyOrderedAdd.{u_2} (α i)
inst_3 : (i : ι) → Sub (α i)
inst_4 : ∀ (i : ι), OrderedSub.{u_2} (α i)
i : ι
a b : α i
inst_5 : DecidableEq ι
⊢ single (β := α) i (a - b) = HSub.hSub (α := Π₀ (i : ι), α i) (single (β := α) i a) (single (β := α) i b)
have h : ∀ (j : ι),
  (single (β := α) i (a - b) : (a : ι) → α a) j =
    (HSub.hSub (α := Π₀ (i : ι), α i) (single (β := α) i a) (single (β := α) i b) : (a : ι) → α a) j
Tactic: ext j
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Order (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → AddCommMonoid (α i)
inst_1 : (i : ι) → PartialOrder (α i)
inst_2 : ∀ (i : ι), CanonicallyOrderedAdd.{u_2} (α i)
inst_3 : (i : ι) → Sub (α i)
inst_4 : ∀ (i : ι), OrderedSub.{u_2} (α i)
i : ι
a b : α i
inst_5 : DecidableEq ι
j : ι
⊢ (single (β := α) i (a - b) : (a : ι) → α a) j =
    (HSub.hSub (α := Π₀ (i : ι), α i) (single (β := α) i a) (single (β := α) i b) : (a : ι) → α a) j
have h : ∀ {a b : α j},
  (single (β := α) j (a - b) : (a : ι) → α a) j =
    (HSub.hSub (α := Π₀ (i : ι), α i) (single (β := α) j a) (single (β := α) j b) : (a : ι) → α a) j
Tactic: obtain rfl | h := eq_or_ne j i
Cleared hypotheses: i, a, b
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Order (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → AddCommMonoid (α i)
inst_1 : (i : ι) → PartialOrder (α i)
inst_2 : ∀ (i : ι), CanonicallyOrderedAdd.{u_2} (α i)
inst_3 : (i : ι) → Sub (α i)
inst_4 : ∀ (i : ι), OrderedSub.{u_2} (α i)
i : ι
a b : α i
inst_5 : DecidableEq ι
j : ι
h :
  ∀ {a b : α j},
    (single (β := α) j (a - b) : (a : ι) → α a) j =
      (HSub.hSub (α := Π₀ (i : ι), α i) (single (β := α) j a) (single (β := α) j b) : (a : ι) → α a) j
⊢ (single (β := α) i (a - b) : (a : ι) → α a) j =
    (HSub.hSub (α := Π₀ (i : ι), α i) (single (β := α) i a) (single (β := α) i b) : (a : ι) → α a) j
have h₁ : ∀ (h : j ≠ i),
  (single (β := α) i (a - b) : (a : ι) → α a) j =
    (HSub.hSub (α := Π₀ (i : ι), α i) (single (β := α) i a) (single (β := α) i b) : (a : ι) → α a) j
Tactic: obtain rfl | h := eq_or_ne j i
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Order (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → AddCommMonoid (α i)
inst_1 : (i : ι) → PartialOrder (α i)
inst_2 : ∀ (i : ι), CanonicallyOrderedAdd.{u_2} (α i)
inst_3 : (i : ι) → Sub (α i)
inst_4 : ∀ (i : ι), OrderedSub.{u_2} (α i)
inst_5 : DecidableEq ι
j : ι
a b : α j
⊢ (single (β := α) j (a - b) : (a : ι) → α a) j =
    (HSub.hSub (α := Π₀ (i : ι), α i) (single (β := α) j a) (single (β := α) j b) : (a : ι) → α a) j
have h : (single (β := α) j (a - b) : (a : ι) → α a) j =
  (single (β := α) j a : (a : ι) → α a) j - (single (β := α) j b : (a : ι) → α a) j
Tactic: rw [tsub_apply, single_eq_same, single_eq_same, single_eq_same]
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Order (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → AddCommMonoid (α i)
inst_1 : (i : ι) → PartialOrder (α i)
inst_2 : ∀ (i : ι), CanonicallyOrderedAdd.{u_2} (α i)
inst_3 : (i : ι) → Sub (α i)
inst_4 : ∀ (i : ι), OrderedSub.{u_2} (α i)
inst_5 : DecidableEq ι
j : ι
a b : α j
h :
  (single (β := α) j (a - b) : (a : ι) → α a) j =
    (single (β := α) j a : (a : ι) → α a) j - (single (β := α) j b : (a : ι) → α a) j
⊢ (single (β := α) j (a - b) : (a : ι) → α a) j =
    (HSub.hSub (α := Π₀ (i : ι), α i) (single (β := α) j a) (single (β := α) j b) : (a : ι) → α a) j
have h₁ : a - b = (single (β := α) j a : (a : ι) → α a) j - (single (β := α) j b : (a : ι) → α a) j
Tactic: rw [tsub_apply, single_eq_same, single_eq_same, single_eq_same]
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Order (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → AddCommMonoid (α i)
inst_1 : (i : ι) → PartialOrder (α i)
inst_2 : ∀ (i : ι), CanonicallyOrderedAdd.{u_2} (α i)
inst_3 : (i : ι) → Sub (α i)
inst_4 : ∀ (i : ι), OrderedSub.{u_2} (α i)
inst_5 : DecidableEq ι
j : ι
a b : α j
h :
  (single (β := α) j (a - b) : (a : ι) → α a) j =
    (single (β := α) j a : (a : ι) → α a) j - (single (β := α) j b : (a : ι) → α a) j
h₁ : a - b = (single (β := α) j a : (a : ι) → α a) j - (single (β := α) j b : (a : ι) → α a) j
⊢ (single (β := α) j (a - b) : (a : ι) → α a) j =
    (HSub.hSub (α := Π₀ (i : ι), α i) (single (β := α) j a) (single (β := α) j b) : (a : ι) → α a) j
have h₂ : a - b = a - (single (β := α) j b : (a : ι) → α a) j
Tactic: rw [tsub_apply, single_eq_same, single_eq_same, single_eq_same]
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Order (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → AddCommMonoid (α i)
inst_1 : (i : ι) → PartialOrder (α i)
inst_2 : ∀ (i : ι), CanonicallyOrderedAdd.{u_2} (α i)
inst_3 : (i : ι) → Sub (α i)
inst_4 : ∀ (i : ι), OrderedSub.{u_2} (α i)
inst_5 : DecidableEq ι
j : ι
a b : α j
h :
  (single (β := α) j (a - b) : (a : ι) → α a) j =
    (single (β := α) j a : (a : ι) → α a) j - (single (β := α) j b : (a : ι) → α a) j
h₁ : a - b = (single (β := α) j a : (a : ι) → α a) j - (single (β := α) j b : (a : ι) → α a) j
h₂ : a - b = a - (single (β := α) j b : (a : ι) → α a) j
⊢ (single (β := α) j (a - b) : (a : ι) → α a) j =
    (HSub.hSub (α := Π₀ (i : ι), α i) (single (β := α) j a) (single (β := α) j b) : (a : ι) → α a) j
have h₃ : a - b = a - b
Tactic: rw [tsub_apply, single_eq_same, single_eq_same, single_eq_same]
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Order (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → AddCommMonoid (α i)
inst_1 : (i : ι) → PartialOrder (α i)
inst_2 : ∀ (i : ι), CanonicallyOrderedAdd.{u_2} (α i)
inst_3 : (i : ι) → Sub (α i)
inst_4 : ∀ (i : ι), OrderedSub.{u_2} (α i)
i : ι
a b : α i
inst_5 : DecidableEq ι
j : ι
h : j ≠ i
⊢ (single (β := α) i (a - b) : (a : ι) → α a) j =
    (HSub.hSub (α := Π₀ (i : ι), α i) (single (β := α) i a) (single (β := α) i b) : (a : ι) → α a) j
have h₁ : (single (β := α) i (a - b) : (a : ι) → α a) j =
  (single (β := α) i a : (a : ι) → α a) j - (single (β := α) i b : (a : ι) → α a) j
Tactic: rw [tsub_apply, single_eq_of_ne h, single_eq_of_ne h, single_eq_of_ne h, tsub_self]
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Order (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → AddCommMonoid (α i)
inst_1 : (i : ι) → PartialOrder (α i)
inst_2 : ∀ (i : ι), CanonicallyOrderedAdd.{u_2} (α i)
inst_3 : (i : ι) → Sub (α i)
inst_4 : ∀ (i : ι), OrderedSub.{u_2} (α i)
i : ι
a b : α i
inst_5 : DecidableEq ι
j : ι
h : j ≠ i
h₁ :
  (single (β := α) i (a - b) : (a : ι) → α a) j =
    (single (β := α) i a : (a : ι) → α a) j - (single (β := α) i b : (a : ι) → α a) j
⊢ (single (β := α) i (a - b) : (a : ι) → α a) j =
    (HSub.hSub (α := Π₀ (i : ι), α i) (single (β := α) i a) (single (β := α) i b) : (a : ι) → α a) j
have h₂ : 0 = (single (β := α) i a : (a : ι) → α a) j - (single (β := α) i b : (a : ι) → α a) j
Tactic: rw [tsub_apply, single_eq_of_ne h, single_eq_of_ne h, single_eq_of_ne h, tsub_self]
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Order (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → AddCommMonoid (α i)
inst_1 : (i : ι) → PartialOrder (α i)
inst_2 : ∀ (i : ι), CanonicallyOrderedAdd.{u_2} (α i)
inst_3 : (i : ι) → Sub (α i)
inst_4 : ∀ (i : ι), OrderedSub.{u_2} (α i)
i : ι
a b : α i
inst_5 : DecidableEq ι
j : ι
h : j ≠ i
h₁ :
  (single (β := α) i (a - b) : (a : ι) → α a) j =
    (single (β := α) i a : (a : ι) → α a) j - (single (β := α) i b : (a : ι) → α a) j
h₂ : 0 = (single (β := α) i a : (a : ι) → α a) j - (single (β := α) i b : (a : ι) → α a) j
⊢ (single (β := α) i (a - b) : (a : ι) → α a) j =
    (HSub.hSub (α := Π₀ (i : ι), α i) (single (β := α) i a) (single (β := α) i b) : (a : ι) → α a) j
have h₃ : 0 = 0 - (single (β := α) i b : (a : ι) → α a) j
Tactic: rw [tsub_apply, single_eq_of_ne h, single_eq_of_ne h, single_eq_of_ne h, tsub_self]
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Order (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → AddCommMonoid (α i)
inst_1 : (i : ι) → PartialOrder (α i)
inst_2 : ∀ (i : ι), CanonicallyOrderedAdd.{u_2} (α i)
inst_3 : (i : ι) → Sub (α i)
inst_4 : ∀ (i : ι), OrderedSub.{u_2} (α i)
i : ι
a b : α i
inst_5 : DecidableEq ι
j : ι
h : j ≠ i
h₁ :
  (single (β := α) i (a - b) : (a : ι) → α a) j =
    (single (β := α) i a : (a : ι) → α a) j - (single (β := α) i b : (a : ι) → α a) j
h₂ : 0 = (single (β := α) i a : (a : ι) → α a) j - (single (β := α) i b : (a : ι) → α a) j
h₃ : 0 = 0 - (single (β := α) i b : (a : ι) → α a) j
⊢ (single (β := α) i (a - b) : (a : ι) → α a) j =
    (HSub.hSub (α := Π₀ (i : ι), α i) (single (β := α) i a) (single (β := α) i b) : (a : ι) → α a) j
have h₄ : 0 = HSub.hSub (α := α j) 0 0
Tactic: rw [tsub_apply, single_eq_of_ne h, single_eq_of_ne h, single_eq_of_ne h, tsub_self]
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Order (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → AddCommMonoid (α i)
inst_1 : (i : ι) → PartialOrder (α i)
inst_2 : ∀ (i : ι), CanonicallyOrderedAdd.{u_2} (α i)
inst_3 : (i : ι) → Sub (α i)
inst_4 : ∀ (i : ι), OrderedSub.{u_2} (α i)
i : ι
a b : α i
inst_5 : DecidableEq ι
j : ι
h : j ≠ i
h₁ :
  (single (β := α) i (a - b) : (a : ι) → α a) j =
    (single (β := α) i a : (a : ι) → α a) j - (single (β := α) i b : (a : ι) → α a) j
h₂ : 0 = (single (β := α) i a : (a : ι) → α a) j - (single (β := α) i b : (a : ι) → α a) j
h₃ : 0 = 0 - (single (β := α) i b : (a : ι) → α a) j
h₄ : 0 = HSub.hSub (α := α j) 0 0
⊢ (single (β := α) i (a - b) : (a : ι) → α a) j =
    (HSub.hSub (α := Π₀ (i : ι), α i) (single (β := α) i a) (single (β := α) i b) : (a : ι) → α a) j
have h₅ : Eq.{u_2 + 1} (α := α j) 0 0
Tactic: rw [tsub_apply, single_eq_of_ne h, single_eq_of_ne h, single_eq_of_ne h, tsub_self]
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Order (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → AddCommMonoid (α i)
inst_1 : (i : ι) → LinearOrder (α i)
inst_2 : ∀ (i : ι), IsBotZeroClass.{u_2} (α i)
inst_3 : DecidableEq ι
f g : Π₀ (i : ι), α i
⊢ (f ⊓ g).support (β := α) = f.support (β := α) ∩ g.support (β := α)
have h : ∀ (a : ι), a ∈ (f ⊓ g).support (β := α) ↔ a ∈ f.support (β := α) ∩ g.support (β := α)
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Order (goal)
Goal:
ι : Type u_1
α : ι → Type u_2
inst : (i : ι) → AddCommMonoid (α i)
inst_1 : (i : ι) → LinearOrder (α i)
inst_2 : ∀ (i : ι), IsBotZeroClass.{u_2} (α i)
inst_3 : DecidableEq ι
f g : Π₀ (i : ι), α i
⊢ (f ⊔ g).support (β := α) = f.support (β := α) ∪ g.support (β := α)
have h : ∀ (a : ι), a ∈ (f ⊔ g).support (β := α) ↔ a ∈ f.support (β := α) ∪ g.support (β := α)
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Sigma (goal)
Goal:
ι : Type u
α : ι → Type u_2
δ : (i : ι) → α i → Type v
inst : DecidableEq ι
inst_1 : (i : ι) → (j : α i) → AddZeroClass (δ i j)
f g : Π₀ (i : (x : ι) × α x), δ (i.fst (β := fun (x : ι) ↦ α x)) (i.snd (β := fun (x : ι) ↦ α x))
⊢ (f + g).sigmaCurry (α := α) (δ := δ) =
    HAdd.hAdd (α := Π₀ (i : ι) (j : α i), δ i j) (f.sigmaCurry (α := α) (δ := δ)) (g.sigmaCurry (α := α) (δ := δ))
have h : ∀ (i : ι) (j : α i),
  (((f + g).sigmaCurry (α := α) (δ := δ) : (a : ι) → Π₀ (j : α a), δ a j) i : (a : α i) → δ i a) j =
    ((HAdd.hAdd (α := Π₀ (i : ι) (j : α i), δ i j) (f.sigmaCurry (α := α) (δ := δ)) (g.sigmaCurry (α := α) (δ := δ)) :
            (a : ι) → Π₀ (j : α a), δ a j)
          i :
        (a : α i) → δ i a)
      j
Tactic: ext (i j)
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Sigma (goal)
Goal:
ι : Type u
γ : Type w
α : ι → Type u_2
δ : (i : ι) → α i → Type v
inst : DecidableEq ι
inst_1 : Monoid γ
inst_2 : (i : ι) → (j : α i) → AddMonoid (δ i j)
inst_3 : (i : ι) → (j : α i) → DistribMulAction.{w, v} γ (δ i j)
r : γ
f : Π₀ (i : (x : ι) × α x), δ (i.fst (β := fun (x : ι) ↦ α x)) (i.snd (β := fun (x : ι) ↦ α x))
⊢ (r • f).sigmaCurry (α := α) (δ := δ) =
    HSMul.hSMul (β := Π₀ (i : ι) (j : α i), δ i j) r (f.sigmaCurry (α := α) (δ := δ))
have h : ∀ (i : ι) (j : α i),
  (((r • f).sigmaCurry (α := α) (δ := δ) : (a : ι) → Π₀ (j : α a), δ a j) i : (a : α i) → δ i a) j =
    ((HSMul.hSMul (β := Π₀ (i : ι) (j : α i), δ i j) r (f.sigmaCurry (α := α) (δ := δ)) : (a : ι) → Π₀ (j : α a), δ a j)
          i :
        (a : α i) → δ i a)
      j
Tactic: ext (i j)
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Sigma (goal)
Goal:
ι : Type u
α : ι → Type u_2
δ : (i : ι) → α i → Type v
inst : DecidableEq ι
inst_1 : (i : ι) → DecidableEq (α i)
inst_2 : (i : ι) → (j : α i) → Zero (δ i j)
ij : (i : ι) × α i
x : δ (ij.fst (β := fun (i : ι) ↦ α i)) (ij.snd (β := fun (i : ι) ↦ α i))
⊢ Eq (α := Π₀ (i : ι) (j : α i), δ i j)
    (sigmaCurry (α := α) (δ := δ)
      (single (β := fun (i : (x : ι) × α x) ↦ δ (i.fst (β := fun (x : ι) ↦ α x)) (i.snd (β := fun (x : ι) ↦ α x))) ij
        x))
    (single (β := fun (i : ι) ↦ Π₀ (j : α i), δ i j) (ij.fst (β := fun (i : ι) ↦ α i))
      (single (β := δ (ij.fst (β := fun (i : ι) ↦ α i))) (ij.snd (β := fun (i : ι) ↦ α i)) x))
have obtain : ∀ (i : ι) (j : α i)
  (x :
    δ ((Sigma.mk (β := fun (i : ι) ↦ α i) i j).fst (β := fun (i : ι) ↦ α i))
      ((Sigma.mk (β := fun (i : ι) ↦ α i) i j).snd (β := fun (i : ι) ↦ α i))),
  Eq (α := Π₀ (i : ι) (j : α i), δ i j)
    (sigmaCurry (α := α) (δ := δ)
      (single (β := fun (i : (x : ι) × α x) ↦ δ (i.fst (β := fun (x : ι) ↦ α x)) (i.snd (β := fun (x : ι) ↦ α x)))
        (Sigma.mk (β := fun (i : ι) ↦ α i) i j) x))
    (single (β := fun (i : ι) ↦ Π₀ (j : α i), δ i j)
      ((Sigma.mk (β := fun (i : ι) ↦ α i) i j).fst (β := fun (i : ι) ↦ α i))
      (single (β := δ ((Sigma.mk (β := fun (i : ι) ↦ α i) i j).fst (β := fun (i : ι) ↦ α i)))
        ((Sigma.mk (β := fun (i : ι) ↦ α i) i j).snd (β := fun (i : ι) ↦ α i)) x))
Tactic: obtain ⟨i, j⟩ := ij
Cleared hypotheses: ij, x
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Sigma (goal)
Goal:
ι : Type u
α : ι → Type u_2
δ : (i : ι) → α i → Type v
inst : DecidableEq ι
inst_1 : (i : ι) → DecidableEq (α i)
inst_2 : (i : ι) → (j : α i) → Zero (δ i j)
i : ι
j : α i
x :
  δ ((Sigma.mk (β := fun (i : ι) ↦ α i) i j).fst (β := fun (i : ι) ↦ α i))
    ((Sigma.mk (β := fun (i : ι) ↦ α i) i j).snd (β := fun (i : ι) ↦ α i))
⊢ Eq (α := Π₀ (i : ι) (j : α i), δ i j)
    (sigmaCurry (α := α) (δ := δ)
      (single (β := fun (i : (x : ι) × α x) ↦ δ (i.fst (β := fun (x : ι) ↦ α x)) (i.snd (β := fun (x : ι) ↦ α x)))
        (Sigma.mk (β := fun (i : ι) ↦ α i) i j) x))
    (single (β := fun (i : ι) ↦ Π₀ (j : α i), δ i j)
      ((Sigma.mk (β := fun (i : ι) ↦ α i) i j).fst (β := fun (i : ι) ↦ α i))
      (single (β := δ ((Sigma.mk (β := fun (i : ι) ↦ α i) i j).fst (β := fun (i : ι) ↦ α i)))
        ((Sigma.mk (β := fun (i : ι) ↦ α i) i j).snd (β := fun (i : ι) ↦ α i)) x))
have h : ∀ (i' : ι) (j' : α i'),
  ((sigmaCurry (α := α) (δ := δ)
              (single (β := fun (i : (x : ι) × α x) ↦
                δ (i.fst (β := fun (x : ι) ↦ α x)) (i.snd (β := fun (x : ι) ↦ α x)))
                (Sigma.mk (β := fun (i : ι) ↦ α i) i j) x) :
            (a : ι) → Π₀ (j : α a), δ a j)
          i' :
        (a : α i') → δ i' a)
      j' =
    ((single (β := fun (i : ι) ↦ Π₀ (j : α i), δ i j)
              ((Sigma.mk (β := fun (i : ι) ↦ α i) i j).fst (β := fun (i : ι) ↦ α i))
              (single (β := δ ((Sigma.mk (β := fun (i : ι) ↦ α i) i j).fst (β := fun (i : ι) ↦ α i)))
                ((Sigma.mk (β := fun (i : ι) ↦ α i) i j).snd (β := fun (i : ι) ↦ α i)) x) :
            (a : ι) → Π₀ (j : α a), δ a j)
          i' :
        (a : α i') → δ i' a)
      j'
Tactic: ext i' j'
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Sigma (goal)
Goal:
ι : Type u
α : ι → Type u_2
δ : (i : ι) → α i → Type v
inst : DecidableEq ι
inst_1 : (i : ι) → DecidableEq (α i)
inst_2 : (i : ι) → (j : α i) → Zero (δ i j)
i : ι
j : α i
x :
  δ ((Sigma.mk (β := fun (i : ι) ↦ α i) i j).fst (β := fun (i : ι) ↦ α i))
    ((Sigma.mk (β := fun (i : ι) ↦ α i) i j).snd (β := fun (i : ι) ↦ α i))
i' : ι
j' : α i'
⊢ ((sigmaCurry (α := α) (δ := δ)
              (single (β := fun (i : (x : ι) × α x) ↦
                δ (i.fst (β := fun (x : ι) ↦ α x)) (i.snd (β := fun (x : ι) ↦ α x)))
                (Sigma.mk (β := fun (i : ι) ↦ α i) i j) x) :
            (a : ι) → Π₀ (j : α a), δ a j)
          i' :
        (a : α i') → δ i' a)
      j' =
    ((single (β := fun (i : ι) ↦ Π₀ (j : α i), δ i j)
              ((Sigma.mk (β := fun (i : ι) ↦ α i) i j).fst (β := fun (i : ι) ↦ α i))
              (single (β := δ ((Sigma.mk (β := fun (i : ι) ↦ α i) i j).fst (β := fun (i : ι) ↦ α i)))
                ((Sigma.mk (β := fun (i : ι) ↦ α i) i j).snd (β := fun (i : ι) ↦ α i)) x) :
            (a : ι) → Π₀ (j : α a), δ a j)
          i' :
        (a : α i') → δ i' a)
      j'
have h : ((sigmaCurry (α := α) (δ := δ)
            (single (β := fun (i : (x : ι) × α x) ↦ δ (i.fst (β := fun (x : ι) ↦ α x)) (i.snd (β := fun (x : ι) ↦ α x)))
              (Sigma.mk (β := fun (i : ι) ↦ α i) i j) x) :
          (a : ι) → Π₀ (j : α a), δ a j)
        i' :
      (a : α i') → δ i' a)
    j' =
  ((single (β := fun (i : ι) ↦ Π₀ (j : α i), δ i j) i (single (β := δ i) j x) : (a : ι) → Π₀ (j : α a), δ a j) i' :
      (a : α i') → δ i' a)
    j'
Tactic: dsimp only
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Sigma (goal)
Goal:
ι : Type u
α : ι → Type u_2
δ : (i : ι) → α i → Type v
inst : DecidableEq ι
inst_1 : (i : ι) → DecidableEq (α i)
inst_2 : (i : ι) → (j : α i) → Zero (δ i j)
i : ι
j : α i
x :
  δ ((Sigma.mk (β := fun (i : ι) ↦ α i) i j).fst (β := fun (i : ι) ↦ α i))
    ((Sigma.mk (β := fun (i : ι) ↦ α i) i j).snd (β := fun (i : ι) ↦ α i))
i' : ι
j' : α i'
⊢ ((sigmaCurry (α := α) (δ := δ)
              (single (β := fun (i : (x : ι) × α x) ↦
                δ (i.fst (β := fun (x : ι) ↦ α x)) (i.snd (β := fun (x : ι) ↦ α x)))
                (Sigma.mk (β := fun (i : ι) ↦ α i) i j) x) :
            (a : ι) → Π₀ (j : α a), δ a j)
          i' :
        (a : α i') → δ i' a)
      j' =
    ((single (β := fun (i : ι) ↦ Π₀ (j : α i), δ i j) i (single (β := δ i) j x) : (a : ι) → Π₀ (j : α a), δ a j) i' :
        (a : α i') → δ i' a)
      j'
have h : (single (β := fun (i : (x : ι) × α x) ↦ δ (i.fst (β := fun (x : ι) ↦ α x)) (i.snd (β := fun (x : ι) ↦ α x)))
        (Sigma.mk (β := fun (i : ι) ↦ α i) i j) x :
      (a : (x : ι) × α x) → δ a.fst a.snd)
    (Sigma.mk (β := fun (x : ι) ↦ α x) i' j') =
  ((single (β := fun (i : ι) ↦ Π₀ (j : α i), δ i j) i (single (β := δ i) j x) : (a : ι) → Π₀ (j : α a), δ a j) i' :
      (a : α i') → δ i' a)
    j'
Tactic: rw [sigmaCurry_apply]
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Sigma (goal)
Goal:
ι : Type u
α : ι → Type u_2
δ : (i : ι) → α i → Type v
inst : DecidableEq ι
inst_1 : (i : ι) → DecidableEq (α i)
inst_2 : (i : ι) → (j : α i) → Zero (δ i j)
i : ι
j : α i
x :
  δ ((Sigma.mk (β := fun (i : ι) ↦ α i) i j).fst (β := fun (i : ι) ↦ α i))
    ((Sigma.mk (β := fun (i : ι) ↦ α i) i j).snd (β := fun (i : ι) ↦ α i))
i' : ι
j' : α i'
⊢ (single (β := fun (i : (x : ι) × α x) ↦ δ (i.fst (β := fun (x : ι) ↦ α x)) (i.snd (β := fun (x : ι) ↦ α x)))
          (Sigma.mk (β := fun (i : ι) ↦ α i) i j) x :
        (a : (x : ι) × α x) → δ a.fst a.snd)
      (Sigma.mk (β := fun (x : ι) ↦ α x) i' j') =
    ((single (β := fun (i : ι) ↦ Π₀ (j : α i), δ i j) i (single (β := δ i) j x) : (a : ι) → Π₀ (j : α a), δ a j) i' :
        (a : α i') → δ i' a)
      j'
have h : ∀ (j' : α i),
  (single (β := fun (i : (x : ι) × α x) ↦ δ (i.fst (β := fun (x : ι) ↦ α x)) (i.snd (β := fun (x : ι) ↦ α x)))
          (Sigma.mk (β := fun (i : ι) ↦ α i) i j) x :
        (a : (x : ι) × α x) → δ a.fst a.snd)
      (Sigma.mk (β := fun (x : ι) ↦ α x) i j') =
    ((single (β := fun (i : ι) ↦ Π₀ (j : α i), δ i j) i (single (β := δ i) j x) : (a : ι) → Π₀ (j : α a), δ a j) i :
        (a : α i) → δ i a)
      j'
Tactic: obtain rfl | hi := eq_or_ne i i'
Cleared hypotheses: i', j'