awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Defs (goal)
Goal:
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
κ : Type u_1
inst : (i : ι) → Zero (β i)
h : ι ≃ κ
f : Π₀ (k : κ), β ((h.symm : (a : κ) → ι) k)
k : κ
h₁ :
  ((fun (f : Π₀ (k : κ), β ((h.symm : (a : κ) → ι) k)) ↦
            (mapRange (β₁ := fun (i : ι) ↦ β ((h.symm : (a : κ) → ι) ((h : (a : ι) → κ) i : κ))) (β₂ := β)
                (fun (i : ι) ↦ (⇑(Equiv.cast ⋯) : (a : β ((h.symm : (a : κ) → ι) ((h : (a : ι) → κ) i))) → β i)) ⋯
                (comapDomain' (β := fun (i : κ) ↦ β ((h.symm : (a : κ) → ι) i)) (⇑h : (a : ι) → κ) (h' := h.invFun) ⋯
                  f) :
              Π₀ (i : ι), β i))
          f :
        (a : ι) → β a)
      ((h.symm : (a : κ) → ι) k) =
    (f : (a : κ) → β ((h.symm : (a : κ) → ι) a)) k
h₂ :
  (Equiv.cast ⋯ :
        (a : β ((h.symm : (a : κ) → ι) ((h : (a : ι) → κ) ((h.symm : (a : κ) → ι) k)))) → β ((h.symm : (a : κ) → ι) k))
      ((comapDomain' (β := fun (i : κ) ↦ β ((h.symm : (a : κ) → ι) i)) (⇑h : (a : ι) → κ) (h' := h.invFun) ⋯ f :
          (a : ι) → β ((h.symm : (a : κ) → ι) ((h : (a : ι) → κ) a)))
        ((h.symm : (a : κ) → ι) k)) =
    (f : (a : κ) → β ((h.symm : (a : κ) → ι) a)) k
h₃ :
  (Equiv.cast ⋯ :
        (a : β ((h.symm : (a : κ) → ι) ((h : (a : ι) → κ) ((h.symm : (a : κ) → ι) k)))) → β ((h.symm : (a : κ) → ι) k))
      ((f : (a : κ) → β ((h.symm : (a : κ) → ι) a)) ((h : (a : ι) → κ) ((h.symm : (a : κ) → ι) k : ι))) =
    (f : (a : κ) → β ((h.symm : (a : κ) → ι) a)) k
⊢ (comapDomain' (β := β) (⇑h.symm : (a : κ) → ι) ⋯
          ((fun (f : Π₀ (k : κ), β ((h.symm : (a : κ) → ι) k)) ↦
              (mapRange (β₁ := fun (i : ι) ↦ β ((h.symm : (a : κ) → ι) ((h : (a : ι) → κ) i : κ))) (β₂ := β)
                  (fun (i : ι) ↦ (⇑(Equiv.cast ⋯) : (a : β ((h.symm : (a : κ) → ι) ((h : (a : ι) → κ) i))) → β i)) ⋯
                  (comapDomain' (β := fun (i : κ) ↦ β ((h.symm : (a : κ) → ι) i)) (⇑h : (a : ι) → κ) (h' := h.invFun) ⋯
                    f) :
                Π₀ (i : ι), β i))
            f) :
        (a : κ) → β ((h.symm : (a : κ) → ι) a))
      k =
    (f : (a : κ) → β ((h.symm : (a : κ) → ι) a)) k
have h₄ : HEq (α := β ((h.symm : (a : κ) → ι) ((h : (a : ι) → κ) ((h.symm : (a : κ) → ι) k : ι) : κ)))
  ((f : (a : κ) → β ((h.symm : (a : κ) → ι) a)) ((h : (a : ι) → κ) ((h.symm : (a : κ) → ι) k : ι)))
  ((f : (a : κ) → β ((h.symm : (a : κ) → ι) a)) k)
Tactic: rw [comapDomain'_apply, mapRange_apply, comapDomain'_apply, Equiv.cast_eq_iff_heq,
      h.apply_symm_apply]
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Defs (goal)
Goal:
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
κ : Type u_1
inst : (i : ι) → Zero (β i)
h : ι ≃ κ
f : Π₀ (k : κ), β ((h.symm : (a : κ) → ι) k)
k : κ
h₁ :
  ((fun (f : Π₀ (k : κ), β ((h.symm : (a : κ) → ι) k)) ↦
            (mapRange (β₁ := fun (i : ι) ↦ β ((h.symm : (a : κ) → ι) ((h : (a : ι) → κ) i : κ))) (β₂ := β)
                (fun (i : ι) ↦ (⇑(Equiv.cast ⋯) : (a : β ((h.symm : (a : κ) → ι) ((h : (a : ι) → κ) i))) → β i)) ⋯
                (comapDomain' (β := fun (i : κ) ↦ β ((h.symm : (a : κ) → ι) i)) (⇑h : (a : ι) → κ) (h' := h.invFun) ⋯
                  f) :
              Π₀ (i : ι), β i))
          f :
        (a : ι) → β a)
      ((h.symm : (a : κ) → ι) k) =
    (f : (a : κ) → β ((h.symm : (a : κ) → ι) a)) k
h₂ :
  (Equiv.cast ⋯ :
        (a : β ((h.symm : (a : κ) → ι) ((h : (a : ι) → κ) ((h.symm : (a : κ) → ι) k)))) → β ((h.symm : (a : κ) → ι) k))
      ((comapDomain' (β := fun (i : κ) ↦ β ((h.symm : (a : κ) → ι) i)) (⇑h : (a : ι) → κ) (h' := h.invFun) ⋯ f :
          (a : ι) → β ((h.symm : (a : κ) → ι) ((h : (a : ι) → κ) a)))
        ((h.symm : (a : κ) → ι) k)) =
    (f : (a : κ) → β ((h.symm : (a : κ) → ι) a)) k
h₃ :
  (Equiv.cast ⋯ :
        (a : β ((h.symm : (a : κ) → ι) ((h : (a : ι) → κ) ((h.symm : (a : κ) → ι) k)))) → β ((h.symm : (a : κ) → ι) k))
      ((f : (a : κ) → β ((h.symm : (a : κ) → ι) a)) ((h : (a : ι) → κ) ((h.symm : (a : κ) → ι) k : ι))) =
    (f : (a : κ) → β ((h.symm : (a : κ) → ι) a)) k
h₄ :
  HEq (α := β ((h.symm : (a : κ) → ι) ((h : (a : ι) → κ) ((h.symm : (a : κ) → ι) k : ι) : κ)))
    ((f : (a : κ) → β ((h.symm : (a : κ) → ι) a)) ((h : (a : ι) → κ) ((h.symm : (a : κ) → ι) k : ι)))
    ((f : (a : κ) → β ((h.symm : (a : κ) → ι) a)) k)
⊢ (comapDomain' (β := β) (⇑h.symm : (a : κ) → ι) ⋯
          ((fun (f : Π₀ (k : κ), β ((h.symm : (a : κ) → ι) k)) ↦
              (mapRange (β₁ := fun (i : ι) ↦ β ((h.symm : (a : κ) → ι) ((h : (a : ι) → κ) i : κ))) (β₂ := β)
                  (fun (i : ι) ↦ (⇑(Equiv.cast ⋯) : (a : β ((h.symm : (a : κ) → ι) ((h : (a : ι) → κ) i))) → β i)) ⋯
                  (comapDomain' (β := fun (i : κ) ↦ β ((h.symm : (a : κ) → ι) i)) (⇑h : (a : ι) → κ) (h' := h.invFun) ⋯
                    f) :
                Π₀ (i : ι), β i))
            f) :
        (a : κ) → β ((h.symm : (a : κ) → ι) a))
      k =
    (f : (a : κ) → β ((h.symm : (a : κ) → ι) a)) k
have h₅ : (f : (a : κ) → β ((h.symm : (a : κ) → ι) a)) k ≍ (f : (a : κ) → β ((h.symm : (a : κ) → ι) a)) k
Tactic: rw [comapDomain'_apply, mapRange_apply, comapDomain'_apply, Equiv.cast_eq_iff_heq,
      h.apply_symm_apply]
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Defs (goal)
Goal:
ι : Type u
α : Option ι → Type v
inst : DecidableEq ι
inst_1 : (i : Option ι) → Zero (α i)
i : ι
x : α (some i)
⊢ Eq (α := Π₀ (i : Option ι), α i) (extendWith (α := α) 0 (single (β := fun (i : ι) ↦ α (some i)) i x))
    (single (β := α) (some i) x)
have h : Eq (α := α none) ((extendWith (α := α) 0 (single (β := fun (i : ι) ↦ α (some i)) i x) : (a : Option ι) → α a) none)
  ((single (β := α) (some i) x : (a : Option ι) → α a) none)
Tactic: ext (_ | j)
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Defs (goal)
Goal:
ι : Type u
α : Option ι → Type v
inst : DecidableEq ι
inst_1 : (i : Option ι) → Zero (α i)
i : ι
x : α (some i)
h :
  Eq (α := α none) ((extendWith (α := α) 0 (single (β := fun (i : ι) ↦ α (some i)) i x) : (a : Option ι) → α a) none)
    ((single (β := α) (some i) x : (a : Option ι) → α a) none)
⊢ Eq (α := Π₀ (i : Option ι), α i) (extendWith (α := α) 0 (single (β := fun (i : ι) ↦ α (some i)) i x))
    (single (β := α) (some i) x)
have h₁ : ∀ (j : ι),
  Eq (α := α (some j))
    ((extendWith (α := α) 0 (single (β := fun (i : ι) ↦ α (some i)) i x) : (a : Option ι) → α a) (some j))
    ((single (β := α) (some i) x : (a : Option ι) → α a) (some j))
Tactic: ext (_ | j)
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Defs (goal)
Goal:
ι : Type u
α : Option ι → Type v
inst : DecidableEq ι
inst_1 : (i : Option ι) → Zero (α i)
i : ι
x : α (some i)
⊢ Eq (α := α none) ((extendWith (α := α) 0 (single (β := fun (i : ι) ↦ α (some i)) i x) : (a : Option ι) → α a) none)
    ((single (β := α) (some i) x : (a : Option ι) → α a) none)
have h : Eq (α := α none) 0 ((single (β := α) (some i) x : (a : Option ι) → α a) none)
Tactic: rw [extendWith_none, single_eq_of_ne (Option.some_ne_none _).symm]
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Defs (goal)
Goal:
ι : Type u
α : Option ι → Type v
inst : DecidableEq ι
inst_1 : (i : Option ι) → Zero (α i)
i : ι
x : α (some i)
h : Eq (α := α none) 0 ((single (β := α) (some i) x : (a : Option ι) → α a) none)
⊢ Eq (α := α none) ((extendWith (α := α) 0 (single (β := fun (i : ι) ↦ α (some i)) i x) : (a : Option ι) → α a) none)
    ((single (β := α) (some i) x : (a : Option ι) → α a) none)
have h₁ : Eq.{v + 1} (α := α none) 0 0
Tactic: rw [extendWith_none, single_eq_of_ne (Option.some_ne_none _).symm]
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Defs (goal)
Goal:
ι : Type u
α : Option ι → Type v
inst : DecidableEq ι
inst_1 : (i : Option ι) → Zero (α i)
i : ι
x : α (some i)
j : ι
⊢ Eq (α := α (some j))
    ((extendWith (α := α) 0 (single (β := fun (i : ι) ↦ α (some i)) i x) : (a : Option ι) → α a) (some j))
    ((single (β := α) (some i) x : (a : Option ι) → α a) (some j))
have h : (single (β := fun (i : ι) ↦ α (some i)) i x : (a : ι) → α (some a)) j =
  (single (β := α) (some i) x : (a : Option ι) → α a) (some j)
Tactic: rw [extendWith_some]
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Defs (goal)
Goal:
ι : Type u
α : Option ι → Type v
inst : DecidableEq ι
inst_1 : (i : Option ι) → Zero (α i)
i : ι
x : α (some i)
j : ι
⊢ (single (β := fun (i : ι) ↦ α (some i)) i x : (a : ι) → α (some a)) j =
    (single (β := α) (some i) x : (a : Option ι) → α a) (some j)
have h : ∀ (x : α (some j)),
  (single (β := fun (i : ι) ↦ α (some i)) j x : (a : ι) → α (some a)) j =
    (single (β := α) (some j) x : (a : Option ι) → α a) (some j)
Tactic: obtain rfl | hij := Decidable.eq_or_ne j i
Cleared hypotheses: i, x
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Defs (goal)
Goal:
ι : Type u
α : Option ι → Type v
inst : DecidableEq ι
inst_1 : (i : Option ι) → Zero (α i)
i : ι
x : α (some i)
j : ι
h :
  ∀ (x : α (some j)),
    (single (β := fun (i : ι) ↦ α (some i)) j x : (a : ι) → α (some a)) j =
      (single (β := α) (some j) x : (a : Option ι) → α a) (some j)
⊢ (single (β := fun (i : ι) ↦ α (some i)) i x : (a : ι) → α (some a)) j =
    (single (β := α) (some i) x : (a : Option ι) → α a) (some j)
have h₁ : ∀ (hij : j ≠ i),
  (single (β := fun (i : ι) ↦ α (some i)) i x : (a : ι) → α (some a)) j =
    (single (β := α) (some i) x : (a : Option ι) → α a) (some j)
Tactic: obtain rfl | hij := Decidable.eq_or_ne j i
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Defs (goal)
Goal:
ι : Type u
α : Option ι → Type v
inst : DecidableEq ι
inst_1 : (i : Option ι) → Zero (α i)
j : ι
x : α (some j)
⊢ (single (β := fun (i : ι) ↦ α (some i)) j x : (a : ι) → α (some a)) j =
    (single (β := α) (some j) x : (a : Option ι) → α a) (some j)
have h : x = (single (β := α) (some j) x : (a : Option ι) → α a) (some j)
Tactic: rw [single_eq_same, single_eq_same]
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Defs (goal)
Goal:
ι : Type u
α : Option ι → Type v
inst : DecidableEq ι
inst_1 : (i : Option ι) → Zero (α i)
j : ι
x : α (some j)
h : x = (single (β := α) (some j) x : (a : Option ι) → α a) (some j)
⊢ (single (β := fun (i : ι) ↦ α (some i)) j x : (a : ι) → α (some a)) j =
    (single (β := α) (some j) x : (a : Option ι) → α a) (some j)
have h₁ : x = x
Tactic: rw [single_eq_same, single_eq_same]
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Defs (goal)
Goal:
ι : Type u
α : Option ι → Type v
inst : DecidableEq ι
inst_1 : (i : Option ι) → Zero (α i)
i : ι
x : α (some i)
j : ι
hij : j ≠ i
⊢ (single (β := fun (i : ι) ↦ α (some i)) i x : (a : ι) → α (some a)) j =
    (single (β := α) (some i) x : (a : Option ι) → α a) (some j)
have h : Eq (α := α (some j)) 0 ((single (β := α) (some i) x : (a : Option ι) → α a) (some j))
Tactic: rw [single_eq_of_ne hij, single_eq_of_ne ((Option.some_injective _).ne hij)]
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Defs (goal)
Goal:
ι : Type u
α : Option ι → Type v
inst : DecidableEq ι
inst_1 : (i : Option ι) → Zero (α i)
i : ι
x : α (some i)
j : ι
hij : j ≠ i
h : Eq (α := α (some j)) 0 ((single (β := α) (some i) x : (a : Option ι) → α a) (some j))
⊢ (single (β := fun (i : ι) ↦ α (some i)) i x : (a : ι) → α (some a)) j =
    (single (β := α) (some i) x : (a : Option ι) → α a) (some j)
have h₁ : Eq.{v + 1} (α := α (some j)) 0 0
Tactic: rw [single_eq_of_ne hij, single_eq_of_ne ((Option.some_injective _).ne hij)]
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Defs (goal)
Goal:
ι : Type u
α : Option ι → Type v
inst : DecidableEq ι
inst_1 : (i : Option ι) → Zero (α i)
x : α none
⊢ Eq (α := Π₀ (i : Option ι), α i) (extendWith (α := α) x 0) (single (β := α) none x)
have h : Eq (α := α none) ((extendWith (α := α) x 0 : (a : Option ι) → α a) none)
  ((single (β := α) none x : (a : Option ι) → α a) none)
Tactic: ext (_ | j)
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Defs (goal)
Goal:
ι : Type u
α : Option ι → Type v
inst : DecidableEq ι
inst_1 : (i : Option ι) → Zero (α i)
x : α none
h :
  Eq (α := α none) ((extendWith (α := α) x 0 : (a : Option ι) → α a) none)
    ((single (β := α) none x : (a : Option ι) → α a) none)
⊢ Eq (α := Π₀ (i : Option ι), α i) (extendWith (α := α) x 0) (single (β := α) none x)
have h₁ : ∀ (j : ι),
  Eq (α := α (some j)) ((extendWith (α := α) x 0 : (a : Option ι) → α a) (some j))
    ((single (β := α) none x : (a : Option ι) → α a) (some j))
Tactic: ext (_ | j)
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Defs (goal)
Goal:
ι : Type u
α : Option ι → Type v
inst : DecidableEq ι
inst_1 : (i : Option ι) → Zero (α i)
x : α none
⊢ Eq (α := α none) ((extendWith (α := α) x 0 : (a : Option ι) → α a) none)
    ((single (β := α) none x : (a : Option ι) → α a) none)
have h : x = (single (β := α) none x : (a : Option ι) → α a) none
Tactic: rw [extendWith_none, single_eq_same]
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Defs (goal)
Goal:
ι : Type u
α : Option ι → Type v
inst : DecidableEq ι
inst_1 : (i : Option ι) → Zero (α i)
x : α none
h : x = (single (β := α) none x : (a : Option ι) → α a) none
⊢ Eq (α := α none) ((extendWith (α := α) x 0 : (a : Option ι) → α a) none)
    ((single (β := α) none x : (a : Option ι) → α a) none)
have h₁ : x = x
Tactic: rw [extendWith_none, single_eq_same]
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Defs (goal)
Goal:
ι : Type u
α : Option ι → Type v
inst : DecidableEq ι
inst_1 : (i : Option ι) → Zero (α i)
x : α none
j : ι
⊢ Eq (α := α (some j)) ((extendWith (α := α) x 0 : (a : Option ι) → α a) (some j))
    ((single (β := α) none x : (a : Option ι) → α a) (some j))
have h : (0 : (a : ι) → α (some a)) j = (single (β := α) none x : (a : Option ι) → α a) (some j)
Tactic: rw [extendWith_some, single_eq_of_ne (Option.some_ne_none _), zero_apply]
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Defs (goal)
Goal:
ι : Type u
α : Option ι → Type v
inst : DecidableEq ι
inst_1 : (i : Option ι) → Zero (α i)
x : α none
j : ι
h : (0 : (a : ι) → α (some a)) j = (single (β := α) none x : (a : Option ι) → α a) (some j)
⊢ Eq (α := α (some j)) ((extendWith (α := α) x 0 : (a : Option ι) → α a) (some j))
    ((single (β := α) none x : (a : Option ι) → α a) (some j))
have h₁ : (0 : (a : ι) → α (some a)) j = 0
Tactic: rw [extendWith_some, single_eq_of_ne (Option.some_ne_none _), zero_apply]
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Defs (goal)
Goal:
ι : Type u
α : Option ι → Type v
inst : DecidableEq ι
inst_1 : (i : Option ι) → Zero (α i)
x : α none
j : ι
h : (0 : (a : ι) → α (some a)) j = (single (β := α) none x : (a : Option ι) → α a) (some j)
h₁ : (0 : (a : ι) → α (some a)) j = 0
⊢ Eq (α := α (some j)) ((extendWith (α := α) x 0 : (a : Option ι) → α a) (some j))
    ((single (β := α) none x : (a : Option ι) → α a) (some j))
have h₂ : Eq.{v + 1} (α := α (some j)) 0 0
Tactic: rw [extendWith_some, single_eq_of_ne (Option.some_ne_none _), zero_apply]
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Defs (goal)
Goal:
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
κ : Type u_1
α : Option ι → Type v
inst : (i : Option ι) → Zero (α i)
f : Π₀ (i : Option ι), α i
⊢ (fun (f : α none × Π₀ (i : ι), α (some i)) ↦ extendWith (α := α) f.1 f.2)
      ((fun (f : Π₀ (i : Option ι), α i) ↦
          (((f : (a : Option ι) → α a) none, comapDomain (β := α) some ⋯ f) : α none × Π₀ (i : ι), α (some i)))
        f) =
    f
have h : ∀ (i : Option ι),
  ((fun (f : α none × Π₀ (i : ι), α (some i)) ↦ extendWith (α := α) f.1 f.2)
          ((fun (f : Π₀ (i : Option ι), α i) ↦
              (((f : (a : Option ι) → α a) none, comapDomain (β := α) some sorry f) : α none × Π₀ (i : ι), α (some i)))
            f) :
        (a : Option ι) → α a)
      i =
    (f : (a : Option ι) → α a) i
Tactic: ext i
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Defs (goal)
Goal:
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
κ : Type u_1
α : Option ι → Type v
inst : (i : Option ι) → Zero (α i)
f : Π₀ (i : Option ι), α i
i : Option ι
⊢ ((fun (f : α none × Π₀ (i : ι), α (some i)) ↦ extendWith (α := α) f.1 f.2)
          ((fun (f : Π₀ (i : Option ι), α i) ↦
              (((f : (a : Option ι) → α a) none, comapDomain (β := α) some ⋯ f) : α none × Π₀ (i : ι), α (some i)))
            f) :
        (a : Option ι) → α a)
      i =
    (f : (a : Option ι) → α a) i
have h : Eq (α := α none)
  (((fun (f : α none × Π₀ (i : ι), α (some i)) ↦ extendWith (α := α) f.1 f.2)
        ((fun (f : Π₀ (i : Option ι), α i) ↦
            (((f : (a : Option ι) → α a) none, comapDomain (β := α) some sorry f) : α none × Π₀ (i : ι), α (some i)))
          f) :
      (a : Option ι) → α a)
    none)
  ((f : (a : Option ι) → α a) none)
Tactic: obtain - | i := i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Defs (goal)
Goal:
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
κ : Type u_1
α : Option ι → Type v
inst : (i : Option ι) → Zero (α i)
f : Π₀ (i : Option ι), α i
i : Option ι
h :
  Eq (α := α none)
    (((fun (f : α none × Π₀ (i : ι), α (some i)) ↦ extendWith (α := α) f.1 f.2)
          ((fun (f : Π₀ (i : Option ι), α i) ↦
              (((f : (a : Option ι) → α a) none, comapDomain (β := α) some ⋯ f) : α none × Π₀ (i : ι), α (some i)))
            f) :
        (a : Option ι) → α a)
      none)
    ((f : (a : Option ι) → α a) none)
⊢ ((fun (f : α none × Π₀ (i : ι), α (some i)) ↦ extendWith (α := α) f.1 f.2)
          ((fun (f : Π₀ (i : Option ι), α i) ↦
              (((f : (a : Option ι) → α a) none, comapDomain (β := α) some ⋯ f) : α none × Π₀ (i : ι), α (some i)))
            f) :
        (a : Option ι) → α a)
      i =
    (f : (a : Option ι) → α a) i
have h₁ : ∀ (i : ι),
  Eq (α := α (some i))
    (((fun (f : α none × Π₀ (i : ι), α (some i)) ↦ extendWith (α := α) f.1 f.2)
          ((fun (f : Π₀ (i : Option ι), α i) ↦
              (((f : (a : Option ι) → α a) none, comapDomain (β := α) some sorry f) : α none × Π₀ (i : ι), α (some i)))
            f) :
        (a : Option ι) → α a)
      (some i))
    ((f : (a : Option ι) → α a) (some i))
Tactic: obtain - | i := i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Defs (goal)
Goal:
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
κ : Type u_1
α : Option ι → Type v
inst : (i : Option ι) → Zero (α i)
f : Π₀ (i : Option ι), α i
⊢ Eq (α := α none)
    (((fun (f : α none × Π₀ (i : ι), α (some i)) ↦ extendWith (α := α) f.1 f.2)
          ((fun (f : Π₀ (i : Option ι), α i) ↦
              (((f : (a : Option ι) → α a) none, comapDomain (β := α) some ⋯ f) : α none × Π₀ (i : ι), α (some i)))
            f) :
        (a : Option ι) → α a)
      none)
    ((f : (a : Option ι) → α a) none)
have h : Eq (α := α none)
  ((fun (f : Π₀ (i : Option ι), α i) ↦
        (((f : (a : Option ι) → α a) none, comapDomain (β := α) some sorry f) : α none × Π₀ (i : ι), α (some i)))
      f).1
  ((f : (a : Option ι) → α a) none)
Tactic: rw [extendWith_none]
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Defs (goal)
Goal:
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
κ : Type u_1
α : Option ι → Type v
inst : (i : Option ι) → Zero (α i)
f : Π₀ (i : Option ι), α i
i : ι
⊢ Eq (α := α (some i))
    (((fun (f : α none × Π₀ (i : ι), α (some i)) ↦ extendWith (α := α) f.1 f.2)
          ((fun (f : Π₀ (i : Option ι), α i) ↦
              (((f : (a : Option ι) → α a) none, comapDomain (β := α) some ⋯ f) : α none × Π₀ (i : ι), α (some i)))
            f) :
        (a : Option ι) → α a)
      (some i))
    ((f : (a : Option ι) → α a) (some i))
have h : (((fun (f : Π₀ (i : Option ι), α i) ↦
            (((f : (a : Option ι) → α a) none, comapDomain (β := α) some sorry f) : α none × Π₀ (i : ι), α (some i)))
          f).2 :
      (a : ι) → α (some a))
    i =
  (f : (a : Option ι) → α a) (some i)
Tactic: rw [extendWith_some, comapDomain_apply]
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Defs (goal)
Goal:
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
κ : Type u_1
α : Option ι → Type v
inst : (i : Option ι) → Zero (α i)
f : Π₀ (i : Option ι), α i
i : ι
h :
  (((fun (f : Π₀ (i : Option ι), α i) ↦
              (((f : (a : Option ι) → α a) none, comapDomain (β := α) some ⋯ f) : α none × Π₀ (i : ι), α (some i)))
            f).2 :
        (a : ι) → α (some a))
      i =
    (f : (a : Option ι) → α a) (some i)
⊢ Eq (α := α (some i))
    (((fun (f : α none × Π₀ (i : ι), α (some i)) ↦ extendWith (α := α) f.1 f.2)
          ((fun (f : Π₀ (i : Option ι), α i) ↦
              (((f : (a : Option ι) → α a) none, comapDomain (β := α) some ⋯ f) : α none × Π₀ (i : ι), α (some i)))
            f) :
        (a : Option ι) → α a)
      (some i))
    ((f : (a : Option ι) → α a) (some i))
have h₁ : Eq (α := α (some i)) ((f : (a : Option ι) → α a) (some i)) ((f : (a : Option ι) → α a) (some i))
Tactic: rw [extendWith_some, comapDomain_apply]
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Defs (goal)
Goal:
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
κ : Type u_1
α : Option ι → Type v
inst : (i : Option ι) → Zero (α i)
x : α none × Π₀ (i : ι), α (some i)
⊢ ((extendWith (α := α) x.1 x.2 : (a : Option ι) → α a) none,
      comapDomain (β := α) some ⋯ (extendWith (α := α) x.1 x.2)) =
    x
have fst : ((extendWith (α := α) x.1 x.2 : (a : Option ι) → α a) none,
      comapDomain (β := α) some sorry (extendWith (α := α) x.1 x.2)).1 =
  x.1
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Defs (goal)
Goal:
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
κ : Type u_1
α : Option ι → Type v
inst : (i : Option ι) → Zero (α i)
x : α none × Π₀ (i : ι), α (some i)
fst :
  ((extendWith (α := α) x.1 x.2 : (a : Option ι) → α a) none,
        comapDomain (β := α) some ⋯ (extendWith (α := α) x.1 x.2)).1 =
    x.1
⊢ ((extendWith (α := α) x.1 x.2 : (a : Option ι) → α a) none,
      comapDomain (β := α) some ⋯ (extendWith (α := α) x.1 x.2)) =
    x
have snd : ∀ (i : ι),
  (((extendWith (α := α) x.1 x.2 : (a : Option ι) → α a) none,
            comapDomain (β := α) some sorry (extendWith (α := α) x.1 x.2)).2 :
        (a : ι) → α (some a))
      i =
    (x.2 : (a : ι) → α (some a)) i
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Defs (goal)
Goal:
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
κ : Type u_1
α : Option ι → Type v
inst : (i : Option ι) → Zero (α i)
x : α none × Π₀ (i : ι), α (some i)
i : ι
⊢ (((extendWith (α := α) x.1 x.2 : (a : Option ι) → α a) none,
            comapDomain (β := α) some ⋯ (extendWith (α := α) x.1 x.2)).2 :
        (a : ι) → α (some a))
      i =
    (x.2 : (a : ι) → α (some a)) i
have snd : (extendWith (α := α) x.1 x.2 : (a : Option ι) → α a) (some i) = (x.2 : (a : ι) → α (some a)) i
Tactic: rw [comapDomain_apply, extendWith_some]
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Defs (goal)
Goal:
ι : Type u
γ : Type w
β : ι → Type v
β₁ : ι → Type v₁
β₂ : ι → Type v₂
κ : Type u_1
α : Option ι → Type v
inst : (i : Option ι) → Zero (α i)
x : α none × Π₀ (i : ι), α (some i)
i : ι
snd : (extendWith (α := α) x.1 x.2 : (a : Option ι) → α a) (some i) = (x.2 : (a : ι) → α (some a)) i
⊢ (((extendWith (α := α) x.1 x.2 : (a : Option ι) → α a) none,
            comapDomain (β := α) some ⋯ (extendWith (α := α) x.1 x.2)).2 :
        (a : ι) → α (some a))
      i =
    (x.2 : (a : ι) → α (some a)) i
have snd₁ : (x.2 : (a : ι) → α (some a)) i = (x.2 : (a : ι) → α (some a)) i
Tactic: rw [comapDomain_apply, extendWith_some]
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Defs (goal)
Goal:
ι : Type u
β₁ : ι → Type v₁
β₂ : ι → Type v₂
inst : (i : ι) → AddZeroClass (β₁ i)
inst_1 : (i : ι) → AddZeroClass (β₂ i)
f : (i : ι) → β₁ i → β₂ i
hf : ∀ (i : ι), f i 0 = 0
hf' : ∀ (i : ι) (x y : β₁ i), f i (x + y) = f i x + f i y
g₁ g₂ : Π₀ (i : ι), β₁ i
⊢ mapRange (β₁ := β₁) (β₂ := β₂) f hf (g₁ + g₂) =
    mapRange (β₁ := β₁) (β₂ := β₂) f hf g₁ + mapRange (β₁ := β₁) (β₂ := β₂) f hf g₂
have h : ∀ (i : ι),
  (mapRange (β₁ := β₁) (β₂ := β₂) f hf (g₁ + g₂) : (a : ι) → β₂ a) i =
    (mapRange (β₁ := β₁) (β₂ := β₂) f hf g₁ + mapRange (β₁ := β₁) (β₂ := β₂) f hf g₂ : (a : ι) → β₂ a) i
Tactic: ext