awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Defs (goal)
Goal:
ι : Type u
β : ι → Type v
κ : Type u_1
inst : (i : ι) → Zero (β i)
h : κ → ι
h' : ι → κ
hh' : Function.LeftInverse h' h
i : κ
h₁ : (comapDomain' (β := β) h hh' 0 : (a : κ) → β (h a)) i = 0
⊢ (comapDomain' (β := β) h hh' 0 : (a : κ) → β (h a)) i = ((0 : Π₀ (k : κ), β (h k)) : (a : κ) → β (h a)) i
have h₂ : Eq (α := β (h i)) ((0 : (a : ι) → β a) (h i)) 0
Tactic: rw [zero_apply, comapDomain'_apply, zero_apply]
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Defs (goal)
Goal:
ι : Type u
β : ι → Type v
κ : Type u_1
inst : (i : ι) → Zero (β i)
h : κ → ι
h' : ι → κ
hh' : Function.LeftInverse h' h
i : κ
h₁ : (comapDomain' (β := β) h hh' 0 : (a : κ) → β (h a)) i = 0
h₂ : Eq (α := β (h i)) ((0 : (a : ι) → β a) (h i)) 0
⊢ (comapDomain' (β := β) h hh' 0 : (a : κ) → β (h a)) i = ((0 : Π₀ (k : κ), β (h k)) : (a : κ) → β (h a)) i
have h₃ : Eq.{v + 1} (α := β (h i)) 0 0
Tactic: rw [zero_apply, comapDomain'_apply, zero_apply]
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Defs (goal)
Goal:
ι : Type u
β : ι → Type v
κ : Type u_1
inst : (i : ι) → AddZeroClass (β i)
h : κ → ι
h' : ι → κ
hh' : Function.LeftInverse h' h
f g : Π₀ (i : ι), β i
⊢ comapDomain' (β := β) h hh' (f + g) = comapDomain' (β := β) h hh' f + comapDomain' (β := β) h hh' g
have h₁ : ∀ (i : κ),
  (comapDomain' (β := β) h hh' (f + g) : (a : κ) → β (h a)) i =
    (comapDomain' (β := β) h hh' f + comapDomain' (β := β) h hh' g : (a : κ) → β (h a)) i
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Defs (goal)
Goal:
ι : Type u
β : ι → Type v
κ : Type u_1
inst : (i : ι) → AddZeroClass (β i)
h : κ → ι
h' : ι → κ
hh' : Function.LeftInverse h' h
f g : Π₀ (i : ι), β i
i : κ
⊢ (comapDomain' (β := β) h hh' (f + g) : (a : κ) → β (h a)) i =
    (comapDomain' (β := β) h hh' f + comapDomain' (β := β) h hh' g : (a : κ) → β (h a)) i
have h₁ : (comapDomain' (β := β) h hh' (f + g) : (a : κ) → β (h a)) i =
  (comapDomain' (β := β) h hh' f : (a : κ) → β (h a)) i + (comapDomain' (β := β) h hh' g : (a : κ) → β (h a)) i
Tactic: rw [add_apply, comapDomain'_apply, comapDomain'_apply, comapDomain'_apply, add_apply]
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Defs (goal)
Goal:
ι : Type u
β : ι → Type v
κ : Type u_1
inst : (i : ι) → AddZeroClass (β i)
h : κ → ι
h' : ι → κ
hh' : Function.LeftInverse h' h
f g : Π₀ (i : ι), β i
i : κ
h₁ :
  (comapDomain' (β := β) h hh' (f + g) : (a : κ) → β (h a)) i =
    (comapDomain' (β := β) h hh' f : (a : κ) → β (h a)) i + (comapDomain' (β := β) h hh' g : (a : κ) → β (h a)) i
⊢ (comapDomain' (β := β) h hh' (f + g) : (a : κ) → β (h a)) i =
    (comapDomain' (β := β) h hh' f + comapDomain' (β := β) h hh' g : (a : κ) → β (h a)) i
have h₂ : (f + g : (a : ι) → β a) (h i) =
  (comapDomain' (β := β) h hh' f : (a : κ) → β (h a)) i + (comapDomain' (β := β) h hh' g : (a : κ) → β (h a)) i
Tactic: rw [add_apply, comapDomain'_apply, comapDomain'_apply, comapDomain'_apply, add_apply]
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Defs (goal)
Goal:
ι : Type u
β : ι → Type v
κ : Type u_1
inst : (i : ι) → AddZeroClass (β i)
h : κ → ι
h' : ι → κ
hh' : Function.LeftInverse h' h
f g : Π₀ (i : ι), β i
i : κ
h₁ :
  (comapDomain' (β := β) h hh' (f + g) : (a : κ) → β (h a)) i =
    (comapDomain' (β := β) h hh' f : (a : κ) → β (h a)) i + (comapDomain' (β := β) h hh' g : (a : κ) → β (h a)) i
h₂ :
  (f + g : (a : ι) → β a) (h i) =
    (comapDomain' (β := β) h hh' f : (a : κ) → β (h a)) i + (comapDomain' (β := β) h hh' g : (a : κ) → β (h a)) i
⊢ (comapDomain' (β := β) h hh' (f + g) : (a : κ) → β (h a)) i =
    (comapDomain' (β := β) h hh' f + comapDomain' (β := β) h hh' g : (a : κ) → β (h a)) i
have h₃ : (f + g : (a : ι) → β a) (h i) = (f : (a : ι) → β a) (h i) + (comapDomain' (β := β) h hh' g : (a : κ) → β (h a)) i
Tactic: rw [add_apply, comapDomain'_apply, comapDomain'_apply, comapDomain'_apply, add_apply]
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Defs (goal)
Goal:
ι : Type u
β : ι → Type v
κ : Type u_1
inst : (i : ι) → AddZeroClass (β i)
h : κ → ι
h' : ι → κ
hh' : Function.LeftInverse h' h
f g : Π₀ (i : ι), β i
i : κ
h₁ :
  (comapDomain' (β := β) h hh' (f + g) : (a : κ) → β (h a)) i =
    (comapDomain' (β := β) h hh' f : (a : κ) → β (h a)) i + (comapDomain' (β := β) h hh' g : (a : κ) → β (h a)) i
h₂ :
  (f + g : (a : ι) → β a) (h i) =
    (comapDomain' (β := β) h hh' f : (a : κ) → β (h a)) i + (comapDomain' (β := β) h hh' g : (a : κ) → β (h a)) i
h₃ : (f + g : (a : ι) → β a) (h i) = (f : (a : ι) → β a) (h i) + (comapDomain' (β := β) h hh' g : (a : κ) → β (h a)) i
⊢ (comapDomain' (β := β) h hh' (f + g) : (a : κ) → β (h a)) i =
    (comapDomain' (β := β) h hh' f + comapDomain' (β := β) h hh' g : (a : κ) → β (h a)) i
have h₄ : (f + g : (a : ι) → β a) (h i) = HAdd.hAdd (α := β (h i)) ((f : (a : ι) → β a) (h i)) ((g : (a : ι) → β a) (h i))
Tactic: rw [add_apply, comapDomain'_apply, comapDomain'_apply, comapDomain'_apply, add_apply]
-- Lean 4 proof step from Mathlib.Data.DFinsupp.Defs (goal)
Goal:
ι : Type u
β : ι → Type v
κ : Type u_1
inst : (i : ι) → AddZeroClass (β i)
h : κ → ι
h' : ι → κ
hh' : Function.LeftInverse h' h
f g : Π₀ (i : ι), β i
i : κ
h₁ :
  (comapDomain' (β := β) h hh' (f + g) : (a : κ) → β (h a)) i =
    (comapDomain' (β := β) h hh' f : (a : κ) → β (h a)) i + (comapDomain' (β := β) h hh' g : (a : κ) → β (h a)) i
h₂ :
  (f + g : (a : ι) → β a) (h i) =
    (comapDomain' (β := β) h hh' f : (a : κ) → β (h a)) i + (comapDomain' (β := β) h hh' g : (a : κ) → β (h a)) i
h₃ : (f + g : (a : ι) → β a) (h i) = (f : (a : ι) → β a) (h i) + (comapDomain' (β := β) h hh' g : (a : κ) → β (h a)) i
h₄ : (f + g : (a : ι) → β a) (h i) = HAdd.hAdd (α := β (h i)) ((f : (a : ι) → β a) (h i)) ((g : (a : ι) → β a) (h i))
⊢ (comapDomain' (β := β) h hh' (f + g) : (a : κ) → β (h a)) i =
    (comapDomain' (β := β) h hh' f + comapDomain' (β := β) h hh' g : (a : κ) → β (h a)) i
have h₅ : HAdd.hAdd (α := β (h i)) ((f : (a : ι) → β a) (h i)) ((g : (a : ι) → β a) (h i)) =
  HAdd.hAdd (α := β (h i)) ((f : (a : ι) → β a) (h i)) ((g : (a : ι) → β a) (h i))
Tactic: rw [add_apply, comapDomain'_apply, comapDomain'_apply, comapDomain'_apply, add_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)
i : ι
⊢ HEq.{v + 1} (α := β ((h.symm : (a : κ) → ι) ((h : (a : ι) → κ) i : κ))) 0 (β := β i) 0
have rw : HEq.{v + 1} (α := β i) 0 (β := β i) 0
Tactic: rw [Equiv.symm_apply_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 : Π₀ (i : ι), β i
⊢ (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))
      (comapDomain' (β := β) (⇑h.symm : (a : κ) → ι) ⋯ f) =
    f
have h₁ : ∀ (i : ι),
  ((fun (f : Π₀ (k : κ), β ((h.symm : (a : κ) → ι) k)) ↦
            (mapRange (β₁ := fun (i : ι) ↦ β ((h.symm : (a : κ) → ι) ((h : (a : ι) → κ) i : κ))) (β₂ := β)
                (fun (i : ι) ↦ (⇑(Equiv.cast sorry) : (a : β ((h.symm : (a : κ) → ι) ((h : (a : ι) → κ) i))) → β i)) sorry
                (comapDomain' (β := fun (i : κ) ↦ β ((h.symm : (a : κ) → ι) i)) (⇑h : (a : ι) → κ) (h' := h.invFun) sorry
                  f) :
              Π₀ (i : ι), β i))
          (comapDomain' (β := β) (⇑h.symm : (a : κ) → ι) sorry f) :
        (a : ι) → β a)
      i =
    (f : (a : ι) → β 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
inst : (i : ι) → Zero (β i)
h : ι ≃ κ
f : Π₀ (i : ι), β i
i : ι
⊢ ((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))
          (comapDomain' (β := β) (⇑h.symm : (a : κ) → ι) ⋯ f) :
        (a : ι) → β a)
      i =
    (f : (a : ι) → β a) i
have h₁ : (Equiv.cast sorry : (a : β ((h.symm : (a : κ) → ι) ((h : (a : ι) → κ) i))) → β i)
    ((comapDomain' (β := fun (i : κ) ↦ β ((h.symm : (a : κ) → ι) i)) (⇑h : (a : ι) → κ) (h' := h.invFun) sorry
          (comapDomain' (β := β) (⇑h.symm : (a : κ) → ι) sorry f) :
        (a : ι) → β ((h.symm : (a : κ) → ι) ((h : (a : ι) → κ) a)))
      i) =
  (f : (a : ι) → β a) i
Tactic: rw [mapRange_apply, comapDomain'_apply, comapDomain'_apply, Equiv.cast_eq_iff_heq,
      h.symm_apply_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 : Π₀ (i : ι), β i
i : ι
h₁ :
  (Equiv.cast ⋯ : (a : β ((h.symm : (a : κ) → ι) ((h : (a : ι) → κ) i))) → β i)
      ((comapDomain' (β := fun (i : κ) ↦ β ((h.symm : (a : κ) → ι) i)) (⇑h : (a : ι) → κ) (h' := h.invFun) ⋯
            (comapDomain' (β := β) (⇑h.symm : (a : κ) → ι) ⋯ f) :
          (a : ι) → β ((h.symm : (a : κ) → ι) ((h : (a : ι) → κ) a)))
        i) =
    (f : (a : ι) → β a) i
⊢ ((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))
          (comapDomain' (β := β) (⇑h.symm : (a : κ) → ι) ⋯ f) :
        (a : ι) → β a)
      i =
    (f : (a : ι) → β a) i
have h₂ : (Equiv.cast sorry : (a : β ((h.symm : (a : κ) → ι) ((h : (a : ι) → κ) i))) → β i)
    ((comapDomain' (β := β) (⇑h.symm : (a : κ) → ι) sorry f : (a : κ) → β ((h.symm : (a : κ) → ι) a))
      ((h : (a : ι) → κ) i)) =
  (f : (a : ι) → β a) i
Tactic: rw [mapRange_apply, comapDomain'_apply, comapDomain'_apply, Equiv.cast_eq_iff_heq,
      h.symm_apply_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 : Π₀ (i : ι), β i
i : ι
h₁ :
  (Equiv.cast ⋯ : (a : β ((h.symm : (a : κ) → ι) ((h : (a : ι) → κ) i))) → β i)
      ((comapDomain' (β := fun (i : κ) ↦ β ((h.symm : (a : κ) → ι) i)) (⇑h : (a : ι) → κ) (h' := h.invFun) ⋯
            (comapDomain' (β := β) (⇑h.symm : (a : κ) → ι) ⋯ f) :
          (a : ι) → β ((h.symm : (a : κ) → ι) ((h : (a : ι) → κ) a)))
        i) =
    (f : (a : ι) → β a) i
h₂ :
  (Equiv.cast ⋯ : (a : β ((h.symm : (a : κ) → ι) ((h : (a : ι) → κ) i))) → β i)
      ((comapDomain' (β := β) (⇑h.symm : (a : κ) → ι) ⋯ f : (a : κ) → β ((h.symm : (a : κ) → ι) a))
        ((h : (a : ι) → κ) i)) =
    (f : (a : ι) → β a) i
⊢ ((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))
          (comapDomain' (β := β) (⇑h.symm : (a : κ) → ι) ⋯ f) :
        (a : ι) → β a)
      i =
    (f : (a : ι) → β a) i
have h₃ : (Equiv.cast sorry : (a : β ((h.symm : (a : κ) → ι) ((h : (a : ι) → κ) i))) → β i)
    ((f : (a : ι) → β a) ((h.symm : (a : κ) → ι) ((h : (a : ι) → κ) i : κ))) =
  (f : (a : ι) → β a) i
Tactic: rw [mapRange_apply, comapDomain'_apply, comapDomain'_apply, Equiv.cast_eq_iff_heq,
      h.symm_apply_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 : Π₀ (i : ι), β i
i : ι
h₁ :
  (Equiv.cast ⋯ : (a : β ((h.symm : (a : κ) → ι) ((h : (a : ι) → κ) i))) → β i)
      ((comapDomain' (β := fun (i : κ) ↦ β ((h.symm : (a : κ) → ι) i)) (⇑h : (a : ι) → κ) (h' := h.invFun) ⋯
            (comapDomain' (β := β) (⇑h.symm : (a : κ) → ι) ⋯ f) :
          (a : ι) → β ((h.symm : (a : κ) → ι) ((h : (a : ι) → κ) a)))
        i) =
    (f : (a : ι) → β a) i
h₂ :
  (Equiv.cast ⋯ : (a : β ((h.symm : (a : κ) → ι) ((h : (a : ι) → κ) i))) → β i)
      ((comapDomain' (β := β) (⇑h.symm : (a : κ) → ι) ⋯ f : (a : κ) → β ((h.symm : (a : κ) → ι) a))
        ((h : (a : ι) → κ) i)) =
    (f : (a : ι) → β a) i
h₃ :
  (Equiv.cast ⋯ : (a : β ((h.symm : (a : κ) → ι) ((h : (a : ι) → κ) i))) → β i)
      ((f : (a : ι) → β a) ((h.symm : (a : κ) → ι) ((h : (a : ι) → κ) i : κ))) =
    (f : (a : ι) → β a) i
⊢ ((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))
          (comapDomain' (β := β) (⇑h.symm : (a : κ) → ι) ⋯ f) :
        (a : ι) → β a)
      i =
    (f : (a : ι) → β a) i
have h₄ : HEq (α := β ((h.symm : (a : κ) → ι) ((h : (a : ι) → κ) i : κ)))
  ((f : (a : ι) → β a) ((h.symm : (a : κ) → ι) ((h : (a : ι) → κ) i : κ))) ((f : (a : ι) → β a) i)
Tactic: rw [mapRange_apply, comapDomain'_apply, comapDomain'_apply, Equiv.cast_eq_iff_heq,
      h.symm_apply_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 : Π₀ (i : ι), β i
i : ι
h₁ :
  (Equiv.cast ⋯ : (a : β ((h.symm : (a : κ) → ι) ((h : (a : ι) → κ) i))) → β i)
      ((comapDomain' (β := fun (i : κ) ↦ β ((h.symm : (a : κ) → ι) i)) (⇑h : (a : ι) → κ) (h' := h.invFun) ⋯
            (comapDomain' (β := β) (⇑h.symm : (a : κ) → ι) ⋯ f) :
          (a : ι) → β ((h.symm : (a : κ) → ι) ((h : (a : ι) → κ) a)))
        i) =
    (f : (a : ι) → β a) i
h₂ :
  (Equiv.cast ⋯ : (a : β ((h.symm : (a : κ) → ι) ((h : (a : ι) → κ) i))) → β i)
      ((comapDomain' (β := β) (⇑h.symm : (a : κ) → ι) ⋯ f : (a : κ) → β ((h.symm : (a : κ) → ι) a))
        ((h : (a : ι) → κ) i)) =
    (f : (a : ι) → β a) i
h₃ :
  (Equiv.cast ⋯ : (a : β ((h.symm : (a : κ) → ι) ((h : (a : ι) → κ) i))) → β i)
      ((f : (a : ι) → β a) ((h.symm : (a : κ) → ι) ((h : (a : ι) → κ) i : κ))) =
    (f : (a : ι) → β a) i
h₄ :
  HEq (α := β ((h.symm : (a : κ) → ι) ((h : (a : ι) → κ) i : κ)))
    ((f : (a : ι) → β a) ((h.symm : (a : κ) → ι) ((h : (a : ι) → κ) i : κ))) ((f : (a : ι) → β a) i)
⊢ ((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))
          (comapDomain' (β := β) (⇑h.symm : (a : κ) → ι) ⋯ f) :
        (a : ι) → β a)
      i =
    (f : (a : ι) → β a) i
have h₅ : (f : (a : ι) → β a) i ≍ (f : (a : ι) → β a) i
Tactic: rw [mapRange_apply, comapDomain'_apply, comapDomain'_apply, Equiv.cast_eq_iff_heq,
      h.symm_apply_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)
⊢ 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) =
    f
have h₁ : ∀ (k : κ),
  (comapDomain' (β := β) (⇑h.symm : (a : κ) → ι) sorry
          ((fun (f : Π₀ (k : κ), β ((h.symm : (a : κ) → ι) k)) ↦
              (mapRange (β₁ := fun (i : ι) ↦ β ((h.symm : (a : κ) → ι) ((h : (a : ι) → κ) i : κ))) (β₂ := β)
                  (fun (i : ι) ↦ (⇑(Equiv.cast sorry) : (a : β ((h.symm : (a : κ) → ι) ((h : (a : ι) → κ) i))) → β i)) sorry
                  (comapDomain' (β := fun (i : κ) ↦ β ((h.symm : (a : κ) → ι) i)) (⇑h : (a : ι) → κ) (h' := h.invFun) sorry
                    f) :
                Π₀ (i : ι), β i))
            f) :
        (a : κ) → β ((h.symm : (a : κ) → ι) a))
      k =
    (f : (a : κ) → β ((h.symm : (a : κ) → ι) a)) k
Tactic: ext k
-- 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 : κ
⊢ (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₁ : ((fun (f : Π₀ (k : κ), β ((h.symm : (a : κ) → ι) k)) ↦
          (mapRange (β₁ := fun (i : ι) ↦ β ((h.symm : (a : κ) → ι) ((h : (a : ι) → κ) i : κ))) (β₂ := β)
              (fun (i : ι) ↦ (⇑(Equiv.cast sorry) : (a : β ((h.symm : (a : κ) → ι) ((h : (a : ι) → κ) i))) → β i)) sorry
              (comapDomain' (β := fun (i : κ) ↦ β ((h.symm : (a : κ) → ι) i)) (⇑h : (a : ι) → κ) (h' := h.invFun) sorry f) :
            Π₀ (i : ι), β i))
        f :
      (a : ι) → β 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
⊢ (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₂ : (Equiv.cast sorry :
      (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) sorry f :
        (a : ι) → β ((h.symm : (a : κ) → ι) ((h : (a : ι) → κ) 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
⊢ (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₃ : (Equiv.cast sorry :
      (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
Tactic: rw [comapDomain'_apply, mapRange_apply, comapDomain'_apply, Equiv.cast_eq_iff_heq,
      h.apply_symm_apply]