awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.DFinsupp (goal)
Goal:
ι : Type u_1
β₁ : ι → Type u_8
β₂ : ι → Type u_9
inst : (i : ι) → AddCommMonoid (β₁ i)
inst_1 : (i : ι) → AddCommMonoid (β₂ i)
f : (i : ι) → AddMonoidHom.{u_8, u_9} (β₁ i) (β₂ i)
x : Π₀ (i : ι), β₂ i
⊢ Membership.mem (γ := AddSubmonoid (Π₀ (i : ι), β₂ i))
      (AddMonoidHom.mrange (mapRange.addMonoidHom (β₁ := β₁) (β₂ := β₂) f)) x ↔
    Membership.mem (γ := AddSubmonoid ((i : ι) → β₂ i))
      (AddSubmonoid.pi (M := β₂) Set.univ fun (i : ι) ↦ AddMonoidHom.mrange (f i)) (⇑x : (a : ι) → β₂ a)
have h : Membership.mem (γ := AddSubmonoid (Π₀ (i : ι), β₂ i))
    (AddMonoidHom.mrange (mapRange.addMonoidHom (β₁ := β₁) (β₂ := β₂) f)) x →
  ∀ (i : ι) (hi : Membership.mem (γ := Set ι) Set.univ i) (y : Π₀ (i : ι), β₁ i)
    (hy : (mapRange.addMonoidHom (β₁ := β₁) (β₂ := β₂) f : (a : Π₀ (i : ι), β₁ i) → Π₀ (i : ι), β₂ i) y = x),
    Membership.mem (γ := Set (β₂ i))
      ((fun (i : ι) ↦
          (AddSubsemigroup.carrier
              (AddSubmonoid.toAddSubsemigroup ((fun (i : ι) ↦ (AddMonoidHom.mrange (f i) : AddSubmonoid (β₂ i))) i)) :
            Set (β₂ i)))
        i)
      ((x : (a : ι) → β₂ a) i)
Tactic: refine ⟨fun ⟨y, hy⟩ i hi ↦ ?_, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.DFinsupp (goal)
Goal:
ι : Type u_1
β₁ : ι → Type u_8
β₂ : ι → Type u_9
inst : (i : ι) → AddCommMonoid (β₁ i)
inst_1 : (i : ι) → AddCommMonoid (β₂ i)
f : (i : ι) → AddMonoidHom.{u_8, u_9} (β₁ i) (β₂ i)
x : Π₀ (i : ι), β₂ i
h :
  Membership.mem (γ := AddSubmonoid (Π₀ (i : ι), β₂ i))
      (AddMonoidHom.mrange (mapRange.addMonoidHom (β₁ := β₁) (β₂ := β₂) f)) x →
    ∀ (i : ι) (hi : Membership.mem (γ := Set ι) Set.univ i) (y : Π₀ (i : ι), β₁ i)
      (hy : (mapRange.addMonoidHom (β₁ := β₁) (β₂ := β₂) f : (a : Π₀ (i : ι), β₁ i) → Π₀ (i : ι), β₂ i) y = x),
      Membership.mem (γ := Set (β₂ i))
        ((fun (i : ι) ↦
            (AddSubsemigroup.carrier
                (AddSubmonoid.toAddSubsemigroup ((fun (i : ι) ↦ (AddMonoidHom.mrange (f i) : AddSubmonoid (β₂ i))) i)) :
              Set (β₂ i)))
          i)
        ((x : (a : ι) → β₂ a) i)
⊢ Membership.mem (γ := AddSubmonoid (Π₀ (i : ι), β₂ i))
      (AddMonoidHom.mrange (mapRange.addMonoidHom (β₁ := β₁) (β₂ := β₂) f)) x ↔
    Membership.mem (γ := AddSubmonoid ((i : ι) → β₂ i))
      (AddSubmonoid.pi (M := β₂) Set.univ fun (i : ι) ↦ AddMonoidHom.mrange (f i)) (⇑x : (a : ι) → β₂ a)
have h₁ : ∀
  (h :
    Membership.mem (γ := AddSubmonoid ((i : ι) → β₂ i))
      (AddSubmonoid.pi (M := β₂) Set.univ fun (i : ι) ↦ AddMonoidHom.mrange (f i)) (⇑x : (a : ι) → β₂ a)),
  Membership.mem (γ := AddSubmonoid (Π₀ (i : ι), β₂ i))
    (AddMonoidHom.mrange (mapRange.addMonoidHom (β₁ := β₁) (β₂ := β₂) f)) x
Tactic: refine ⟨fun ⟨y, hy⟩ i hi ↦ ?_, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.DFinsupp (goal)
Goal:
ι : Type u_1
β₁ : ι → Type u_8
β₂ : ι → Type u_9
inst : (i : ι) → AddCommMonoid (β₁ i)
inst_1 : (i : ι) → AddCommMonoid (β₂ i)
f : (i : ι) → AddMonoidHom.{u_8, u_9} (β₁ i) (β₂ i)
x : Π₀ (i : ι), β₂ i
h :
  Membership.mem (γ := AddSubmonoid ((i : ι) → β₂ i))
    (AddSubmonoid.pi (M := β₂) Set.univ fun (i : ι) ↦ AddMonoidHom.mrange (f i)) (⇑x : (a : ι) → β₂ a)
⊢ Membership.mem (γ := AddSubmonoid (Π₀ (i : ι), β₂ i))
    (AddMonoidHom.mrange (mapRange.addMonoidHom (β₁ := β₁) (β₂ := β₂) f)) x
have h₁ : ∀ (g : (i : ι) → β₁ i) (hg : ∀ (i : ι), (f i : (a : β₁ i) → β₂ i) (g i) = (x : (a : ι) → β₂ a) i),
  Membership.mem (γ := AddSubmonoid (Π₀ (i : ι), β₂ i))
    (AddMonoidHom.mrange (mapRange.addMonoidHom (β₁ := β₁) (β₂ := β₂) f)) x
Tactic: choose g hg using fun i => h i (Set.mem_univ _)
-- Lean 4 proof step from Mathlib.LinearAlgebra.DFinsupp (goal)
Goal:
ι : Type u_1
β₁ : ι → Type u_8
β₂ : ι → Type u_9
inst : (i : ι) → AddCommMonoid (β₁ i)
inst_1 : (i : ι) → AddCommMonoid (β₂ i)
f : (i : ι) → AddMonoidHom.{u_8, u_9} (β₁ i) (β₂ i)
x : Π₀ (i : ι), β₂ i
h :
  Membership.mem (γ := AddSubmonoid ((i : ι) → β₂ i))
    (AddSubmonoid.pi (M := β₂) Set.univ fun (i : ι) ↦ AddMonoidHom.mrange (f i)) (⇑x : (a : ι) → β₂ a)
g : (i : ι) → β₁ i
hg : ∀ (i : ι), (f i : (a : β₁ i) → β₂ i) (g i) = (x : (a : ι) → β₂ a) i
⊢ Membership.mem (γ := AddSubmonoid (Π₀ (i : ι), β₂ i))
    (AddMonoidHom.mrange (mapRange.addMonoidHom (β₁ := β₁) (β₂ := β₂) f)) x
have h₁ : (mapRange.addMonoidHom (β₁ := β₁) (β₂ := β₂) f : (a : Π₀ (i : ι), β₁ i) → Π₀ (i : ι), β₂ i)
    (mk (β := β₁) (x.support (β := β₂)) fun (x_1 : (↑(↑(x.support (β := β₂)) : Set ι) : Type u_1)) ↦ g (↑x_1 : ι)) =
  x
Tactic: use DFinsupp.mk x.support (g ·)
-- Lean 4 proof step from Mathlib.LinearAlgebra.DFinsupp (goal)
Goal:
ι : Type u_1
β₁ : ι → Type u_8
β₂ : ι → Type u_9
inst : (i : ι) → AddCommMonoid (β₁ i)
inst_1 : (i : ι) → AddCommMonoid (β₂ i)
f : (i : ι) → AddMonoidHom.{u_8, u_9} (β₁ i) (β₂ i)
x : Π₀ (i : ι), β₂ i
h :
  Membership.mem (γ := AddSubmonoid ((i : ι) → β₂ i))
    (AddSubmonoid.pi (M := β₂) Set.univ fun (i : ι) ↦ AddMonoidHom.mrange (f i)) (⇑x : (a : ι) → β₂ a)
g : (i : ι) → β₁ i
hg : ∀ (i : ι), (f i : (a : β₁ i) → β₂ i) (g i) = (x : (a : ι) → β₂ a) i
⊢ (mapRange.addMonoidHom (β₁ := β₁) (β₂ := β₂) f : (a : Π₀ (i : ι), β₁ i) → Π₀ (i : ι), β₂ i)
      (mk (β := β₁) (x.support (β := β₂)) fun (x_1 : (↑(↑(x.support (β := β₂)) : Set ι) : Type u_1)) ↦ g (↑x_1 : ι)) =
    x
have h₁ : ∀ (i : ι),
  (((mapRange.addMonoidHom (β₁ := β₁) (β₂ := β₂) f : (a : Π₀ (i : ι), β₁ i) → Π₀ (i : ι), β₂ i)
            (mk (β := β₁) (x.support (β := β₂)) fun (x_1 : (↑(↑(x.support (β := β₂)) : Set ι) : Type u_1)) ↦
              g (↑x_1 : ι)) :
          Π₀ (i : ι), β₂ i) :
        (a : ι) → β₂ a)
      i =
    (x : (a : ι) → β₂ a) i
Tactic: ext i
-- Lean 4 proof step from Mathlib.LinearAlgebra.DFinsupp (goal)
Goal:
ι : Type u_1
β₁ : ι → Type u_8
β₂ : ι → Type u_9
inst : (i : ι) → AddCommMonoid (β₁ i)
inst_1 : (i : ι) → AddCommMonoid (β₂ i)
f : (i : ι) → AddMonoidHom.{u_8, u_9} (β₁ i) (β₂ i)
x : Π₀ (i : ι), β₂ i
h :
  Membership.mem (γ := AddSubmonoid ((i : ι) → β₂ i))
    (AddSubmonoid.pi (M := β₂) Set.univ fun (i : ι) ↦ AddMonoidHom.mrange (f i)) (⇑x : (a : ι) → β₂ a)
g : (i : ι) → β₁ i
hg : ∀ (i : ι), (f i : (a : β₁ i) → β₂ i) (g i) = (x : (a : ι) → β₂ a) i
i : ι
⊢ (((mapRange.addMonoidHom (β₁ := β₁) (β₂ := β₂) f : (a : Π₀ (i : ι), β₁ i) → Π₀ (i : ι), β₂ i)
            (mk (β := β₁) (x.support (β := β₂)) fun (x_1 : (↑(↑(x.support (β := β₂)) : Set ι) : Type u_1)) ↦
              g (↑x_1 : ι)) :
          Π₀ (i : ι), β₂ i) :
        (a : ι) → β₂ a)
      i =
    (x : (a : ι) → β₂ a) i
have h₁ : (f i : (a : β₁ i) → β₂ i)
    ((mk (β := β₁) (x.support (β := β₂)) fun (x_1 : ↥(x.support (β := β₂))) ↦ g (↑x_1 : ι) : (a : ι) → β₁ a) i) =
  (x : (a : ι) → β₂ a) i
Tactic: simp only [Finset.coe_sort_coe, mapRange.addMonoidHom_apply, mapRange_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.DFinsupp (goal)
Goal:
ι : Type u_1
β₁ : ι → Type u_8
β₂ : ι → Type u_9
inst : (i : ι) → AddCommMonoid (β₁ i)
inst_1 : (i : ι) → AddCommMonoid (β₂ i)
f : (i : ι) → AddMonoidHom.{u_8, u_9} (β₁ i) (β₂ i)
x : Π₀ (i : ι), β₂ i
h :
  Membership.mem (γ := AddSubmonoid ((i : ι) → β₂ i))
    (AddSubmonoid.pi (M := β₂) Set.univ fun (i : ι) ↦ AddMonoidHom.mrange (f i)) (⇑x : (a : ι) → β₂ a)
g : (i : ι) → β₁ i
hg : ∀ (i : ι), (f i : (a : β₁ i) → β₂ i) (g i) = (x : (a : ι) → β₂ a) i
i : ι
⊢ (f i : (a : β₁ i) → β₂ i)
      ((mk (β := β₁) (x.support (β := β₂)) fun (x_1 : ↥(x.support (β := β₂))) ↦ g (↑x_1 : ι) : (a : ι) → β₁ a) i) =
    (x : (a : ι) → β₂ a) i
have pos : ∀ (mem : i ∈ x.support (β := β₂)),
  (f i : (a : β₁ i) → β₂ i)
      ((mk (β := β₁) (x.support (β := β₂)) fun (x_1 : ↥(x.support (β := β₂))) ↦ g (↑x_1 : ι) : (a : ι) → β₁ a) i) =
    (x : (a : ι) → β₂ a) i
Tactic: by_cases mem : i ∈ x.support
-- Lean 4 proof step from Mathlib.LinearAlgebra.DFinsupp (goal)
Goal:
ι : Type u_1
β₁ : ι → Type u_8
β₂ : ι → Type u_9
inst : (i : ι) → AddCommMonoid (β₁ i)
inst_1 : (i : ι) → AddCommMonoid (β₂ i)
f : (i : ι) → AddMonoidHom.{u_8, u_9} (β₁ i) (β₂ i)
x : Π₀ (i : ι), β₂ i
h :
  Membership.mem (γ := AddSubmonoid ((i : ι) → β₂ i))
    (AddSubmonoid.pi (M := β₂) Set.univ fun (i : ι) ↦ AddMonoidHom.mrange (f i)) (⇑x : (a : ι) → β₂ a)
g : (i : ι) → β₁ i
hg : ∀ (i : ι), (f i : (a : β₁ i) → β₂ i) (g i) = (x : (a : ι) → β₂ a) i
i : ι
pos :
  ∀ (mem : i ∈ x.support (β := β₂)),
    (f i : (a : β₁ i) → β₂ i)
        ((mk (β := β₁) (x.support (β := β₂)) fun (x_1 : ↥(x.support (β := β₂))) ↦ g (↑x_1 : ι) : (a : ι) → β₁ a) i) =
      (x : (a : ι) → β₂ a) i
⊢ (f i : (a : β₁ i) → β₂ i)
      ((mk (β := β₁) (x.support (β := β₂)) fun (x_1 : ↥(x.support (β := β₂))) ↦ g (↑x_1 : ι) : (a : ι) → β₁ a) i) =
    (x : (a : ι) → β₂ a) i
have neg : ∀ (mem : i ∉ x.support (β := β₂)),
  (f i : (a : β₁ i) → β₂ i)
      ((mk (β := β₁) (x.support (β := β₂)) fun (x_1 : ↥(x.support (β := β₂))) ↦ g (↑x_1 : ι) : (a : ι) → β₁ a) i) =
    (x : (a : ι) → β₂ a) i
Tactic: by_cases mem : i ∈ x.support
-- Lean 4 proof step from Mathlib.LinearAlgebra.DFinsupp (goal)
Goal:
ι : Type u_1
β₁ : ι → Type u_8
β₂ : ι → Type u_9
inst : (i : ι) → AddCommMonoid (β₁ i)
inst_1 : (i : ι) → AddCommMonoid (β₂ i)
f : (i : ι) → AddMonoidHom.{u_8, u_9} (β₁ i) (β₂ i)
x : Π₀ (i : ι), β₂ i
h :
  Membership.mem (γ := AddSubmonoid ((i : ι) → β₂ i))
    (AddSubmonoid.pi (M := β₂) Set.univ fun (i : ι) ↦ AddMonoidHom.mrange (f i)) (⇑x : (a : ι) → β₂ a)
g : (i : ι) → β₁ i
hg : ∀ (i : ι), (f i : (a : β₁ i) → β₂ i) (g i) = (x : (a : ι) → β₂ a) i
i : ι
mem : i ∈ x.support (β := β₂)
⊢ (f i : (a : β₁ i) → β₂ i)
      ((mk (β := β₁) (x.support (β := β₂)) fun (x_1 : ↥(x.support (β := β₂))) ↦ g (↑x_1 : ι) : (a : ι) → β₁ a) i) =
    (x : (a : ι) → β₂ a) i
have pos : (f i : (a : β₁ i) → β₂ i) (g (↑(Subtype.mk (p := fun (x_1 : ι) ↦ x_1 ∈ (↑(x.support (β := β₂)) : Set ι)) i mem) : ι)) =
  (x : (a : ι) → β₂ a) i
Tactic: rw [mk_of_mem mem, hg]
-- Lean 4 proof step from Mathlib.LinearAlgebra.DFinsupp (goal)
Goal:
ι : Type u_1
β₁ : ι → Type u_8
β₂ : ι → Type u_9
inst : (i : ι) → AddCommMonoid (β₁ i)
inst_1 : (i : ι) → AddCommMonoid (β₂ i)
f : (i : ι) → AddMonoidHom.{u_8, u_9} (β₁ i) (β₂ i)
x : Π₀ (i : ι), β₂ i
h :
  Membership.mem (γ := AddSubmonoid ((i : ι) → β₂ i))
    (AddSubmonoid.pi (M := β₂) Set.univ fun (i : ι) ↦ AddMonoidHom.mrange (f i)) (⇑x : (a : ι) → β₂ a)
g : (i : ι) → β₁ i
hg : ∀ (i : ι), (f i : (a : β₁ i) → β₂ i) (g i) = (x : (a : ι) → β₂ a) i
i : ι
mem : i ∈ x.support (β := β₂)
pos :
  (f i : (a : β₁ i) → β₂ i)
      (g (↑(Subtype.mk (p := fun (x_1 : ι) ↦ x_1 ∈ (↑(x.support (β := β₂)) : Set ι)) i mem) : ι)) =
    (x : (a : ι) → β₂ a) i
⊢ (f i : (a : β₁ i) → β₂ i)
      ((mk (β := β₁) (x.support (β := β₂)) fun (x_1 : ↥(x.support (β := β₂))) ↦ g (↑x_1 : ι) : (a : ι) → β₁ a) i) =
    (x : (a : ι) → β₂ a) i
have pos₁ : (x : (a : ι) → β₂ a) i = (x : (a : ι) → β₂ a) i
Tactic: rw [mk_of_mem mem, hg]
-- Lean 4 proof step from Mathlib.LinearAlgebra.DFinsupp (goal)
Goal:
ι : Type u_1
β₁ : ι → Type u_8
β₂ : ι → Type u_9
inst : (i : ι) → AddCommMonoid (β₁ i)
inst_1 : (i : ι) → AddCommMonoid (β₂ i)
f : (i : ι) → AddMonoidHom.{u_8, u_9} (β₁ i) (β₂ i)
x : Π₀ (i : ι), β₂ i
h :
  Membership.mem (γ := AddSubmonoid ((i : ι) → β₂ i))
    (AddSubmonoid.pi (M := β₂) Set.univ fun (i : ι) ↦ AddMonoidHom.mrange (f i)) (⇑x : (a : ι) → β₂ a)
g : (i : ι) → β₁ i
hg : ∀ (i : ι), (f i : (a : β₁ i) → β₂ i) (g i) = (x : (a : ι) → β₂ a) i
i : ι
mem : i ∉ x.support (β := β₂)
⊢ (f i : (a : β₁ i) → β₂ i)
      ((mk (β := β₁) (x.support (β := β₂)) fun (x_1 : ↥(x.support (β := β₂))) ↦ g (↑x_1 : ι) : (a : ι) → β₁ a) i) =
    (x : (a : ι) → β₂ a) i
have neg : Eq.{u_9 + 1} (α := β₂ i)
  ((f i : (a : β₁ i) → β₂ i)
      ((mk (β := β₁) (x.support (β := β₂)) fun (x_1 : ↥(x.support (β := β₂))) ↦ g (↑x_1 : ι) : (a : ι) → β₁ a) i) :
    β₂ i)
  (0 : β₂ i)
Tactic: rw [DFinsupp.notMem_support_iff.mp mem, mk_of_notMem mem, map_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.DFinsupp (goal)
Goal:
ι : Type u_1
β₁ : ι → Type u_8
β₂ : ι → Type u_9
inst : (i : ι) → AddCommMonoid (β₁ i)
inst_1 : (i : ι) → AddCommMonoid (β₂ i)
f : (i : ι) → AddMonoidHom.{u_8, u_9} (β₁ i) (β₂ i)
x : Π₀ (i : ι), β₂ i
h :
  Membership.mem (γ := AddSubmonoid ((i : ι) → β₂ i))
    (AddSubmonoid.pi (M := β₂) Set.univ fun (i : ι) ↦ AddMonoidHom.mrange (f i)) (⇑x : (a : ι) → β₂ a)
g : (i : ι) → β₁ i
hg : ∀ (i : ι), (f i : (a : β₁ i) → β₂ i) (g i) = (x : (a : ι) → β₂ a) i
i : ι
mem : i ∉ x.support (β := β₂)
neg :
  Eq.{u_9 + 1} (α := β₂ i)
    ((f i : (a : β₁ i) → β₂ i)
        ((mk (β := β₁) (x.support (β := β₂)) fun (x_1 : ↥(x.support (β := β₂))) ↦ g (↑x_1 : ι) : (a : ι) → β₁ a) i) :
      β₂ i)
    (0 : β₂ i)
⊢ (f i : (a : β₁ i) → β₂ i)
      ((mk (β := β₁) (x.support (β := β₂)) fun (x_1 : ↥(x.support (β := β₂))) ↦ g (↑x_1 : ι) : (a : ι) → β₁ a) i) =
    (x : (a : ι) → β₂ a) i
have neg₁ : Eq.{u_9 + 1} (α := β₂ i) ((f i : (a : β₁ i) → β₂ i) 0) 0
Tactic: rw [DFinsupp.notMem_support_iff.mp mem, mk_of_notMem mem, map_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.DFinsupp (goal)
Goal:
ι : Type u_1
β₁ : ι → Type u_8
β₂ : ι → Type u_9
inst : (i : ι) → AddCommMonoid (β₁ i)
inst_1 : (i : ι) → AddCommMonoid (β₂ i)
f : (i : ι) → AddMonoidHom.{u_8, u_9} (β₁ i) (β₂ i)
x : Π₀ (i : ι), β₂ i
h :
  Membership.mem (γ := AddSubmonoid ((i : ι) → β₂ i))
    (AddSubmonoid.pi (M := β₂) Set.univ fun (i : ι) ↦ AddMonoidHom.mrange (f i)) (⇑x : (a : ι) → β₂ a)
g : (i : ι) → β₁ i
hg : ∀ (i : ι), (f i : (a : β₁ i) → β₂ i) (g i) = (x : (a : ι) → β₂ a) i
i : ι
mem : i ∉ x.support (β := β₂)
neg :
  Eq.{u_9 + 1} (α := β₂ i)
    ((f i : (a : β₁ i) → β₂ i)
        ((mk (β := β₁) (x.support (β := β₂)) fun (x_1 : ↥(x.support (β := β₂))) ↦ g (↑x_1 : ι) : (a : ι) → β₁ a) i) :
      β₂ i)
    (0 : β₂ i)
neg₁ : Eq.{u_9 + 1} (α := β₂ i) ((f i : (a : β₁ i) → β₂ i) 0) 0
⊢ (f i : (a : β₁ i) → β₂ i)
      ((mk (β := β₁) (x.support (β := β₂)) fun (x_1 : ↥(x.support (β := β₂))) ↦ g (↑x_1 : ι) : (a : ι) → β₁ a) i) =
    (x : (a : ι) → β₂ a) i
have neg₂ : Eq.{u_9 + 1} (α := β₂ i) 0 0
Tactic: rw [DFinsupp.notMem_support_iff.mp mem, mk_of_notMem mem, map_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.DFinsupp (goal)
Goal:
ι : Type u_1
β₁ : ι → Type u_8
β₂ : ι → Type u_9
inst : (i : ι) → AddCommMonoid (β₁ i)
inst_1 : (i : ι) → AddCommMonoid (β₂ i)
f : (i : ι) → AddMonoidHom.{u_8, u_9} (β₁ i) (β₂ i)
⊢ Eq (α := AddSubmonoid (Π₀ (i : ι), β₂ i)) (AddMonoidHom.mrange (mapRange.addMonoidHom (β₁ := β₁) (β₂ := β₂) f))
    (AddSubmonoid.comap (F := (Π₀ (i : ι), β₂ i) →+ (i : ι) → β₂ i) (coeFnAddMonoidHom (β := β₂))
      (AddSubmonoid.pi (M := β₂) Set.univ fun (i : ι) ↦ AddMonoidHom.mrange (f i)))
have h : ∀ (x : Π₀ (i : ι), β₂ i),
  Membership.mem (γ := AddSubmonoid (Π₀ (i : ι), β₂ i))
      (AddMonoidHom.mrange (mapRange.addMonoidHom (β₁ := β₁) (β₂ := β₂) f)) x ↔
    Membership.mem (γ := AddSubmonoid (Π₀ (i : ι), β₂ i))
      (AddSubmonoid.comap (F := (Π₀ (i : ι), β₂ i) →+ (i : ι) → β₂ i) (coeFnAddMonoidHom (β := β₂))
        (AddSubmonoid.pi (M := β₂) Set.univ fun (i : ι) ↦ AddMonoidHom.mrange (f i)))
      x
Tactic: classical
  ext x
  simp only [AddSubmonoid.mem_comap, coeFnAddMonoidHom_apply]
  refine ⟨fun ⟨y, hy⟩ i hi ↦ ?_, fun h ↦ ?_⟩
  · simp [← hy]
  · choose g hg using fun i => h i (Set.mem_univ _)
    use DFinsupp.mk x.support (g ·)
    ext i
    simp only [Finset.coe_sort_coe, mapRange.addMonoidHom_apply, mapRange_apply]
    by_cases mem : i ∈ x.support
    · rw [mk_of_mem mem, hg]
    · rw [DFinsupp.notMem_support_iff.mp mem, mk_of_notMem mem, map_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.DFinsupp (goal)
Goal:
ι : Type u_1
β₁ : ι → Type u_8
β₂ : ι → Type u_9
inst : (i : ι) → AddCommMonoid (β₁ i)
inst_1 : (i : ι) → AddCommMonoid (β₂ i)
f : (i : ι) → AddMonoidHom.{u_8, u_9} (β₁ i) (β₂ i)
h :
  ∀ (x : Π₀ (i : ι), β₂ i),
    Membership.mem (γ := AddSubmonoid (Π₀ (i : ι), β₂ i))
        (AddMonoidHom.mrange (mapRange.addMonoidHom (β₁ := β₁) (β₂ := β₂) f)) x ↔
      Membership.mem (γ := AddSubmonoid (Π₀ (i : ι), β₂ i))
        (AddSubmonoid.comap (F := (Π₀ (i : ι), β₂ i) →+ (i : ι) → β₂ i) (coeFnAddMonoidHom (β := β₂))
          (AddSubmonoid.pi (M := β₂) Set.univ fun (i : ι) ↦ AddMonoidHom.mrange (f i)))
        x
⊢ Eq (α := AddSubmonoid (Π₀ (i : ι), β₂ i)) (AddMonoidHom.mrange (mapRange.addMonoidHom (β₁ := β₁) (β₂ := β₂) f))
    (AddSubmonoid.comap (F := (Π₀ (i : ι), β₂ i) →+ (i : ι) → β₂ i) (coeFnAddMonoidHom (β := β₂))
      (AddSubmonoid.pi (M := β₂) Set.univ fun (i : ι) ↦ AddMonoidHom.mrange (f i)))
have h₁ : ∀ (x : Π₀ (i : ι), β₂ i),
  Membership.mem (γ := AddSubmonoid (Π₀ (i : ι), β₂ i))
      (AddMonoidHom.mrange (mapRange.addMonoidHom (β₁ := β₁) (β₂ := β₂) f)) x ↔
    Membership.mem (γ := AddSubmonoid ((i : ι) → β₂ i))
      (AddSubmonoid.pi (M := β₂) Set.univ fun (i : ι) ↦ AddMonoidHom.mrange (f i)) (⇑x : (a : ι) → β₂ a)
Tactic: classical
  ext x
  simp only [AddSubmonoid.mem_comap, coeFnAddMonoidHom_apply]
  refine ⟨fun ⟨y, hy⟩ i hi ↦ ?_, fun h ↦ ?_⟩
  · simp [← hy]
  · choose g hg using fun i => h i (Set.mem_univ _)
    use DFinsupp.mk x.support (g ·)
    ext i
    simp only [Finset.coe_sort_coe, mapRange.addMonoidHom_apply, mapRange_apply]
    by_cases mem : i ∈ x.support
    · rw [mk_of_mem mem, hg]
    · rw [DFinsupp.notMem_support_iff.mp mem, mk_of_notMem mem, map_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.DFinsupp (goal)
Goal:
ι : Type u_1
β₁ : ι → Type u_8
β₂ : ι → Type u_9
inst : (i : ι) → AddCommMonoid (β₁ i)
inst_1 : (i : ι) → AddCommMonoid (β₂ i)
f : (i : ι) → AddMonoidHom.{u_8, u_9} (β₁ i) (β₂ i)
h :
  ∀ (x : Π₀ (i : ι), β₂ i),
    Membership.mem (γ := AddSubmonoid (Π₀ (i : ι), β₂ i))
        (AddMonoidHom.mrange (mapRange.addMonoidHom (β₁ := β₁) (β₂ := β₂) f)) x ↔
      Membership.mem (γ := AddSubmonoid (Π₀ (i : ι), β₂ i))
        (AddSubmonoid.comap (F := (Π₀ (i : ι), β₂ i) →+ (i : ι) → β₂ i) (coeFnAddMonoidHom (β := β₂))
          (AddSubmonoid.pi (M := β₂) Set.univ fun (i : ι) ↦ AddMonoidHom.mrange (f i)))
        x
h₁ :
  ∀ (x : Π₀ (i : ι), β₂ i),
    Membership.mem (γ := AddSubmonoid (Π₀ (i : ι), β₂ i))
        (AddMonoidHom.mrange (mapRange.addMonoidHom (β₁ := β₁) (β₂ := β₂) f)) x ↔
      Membership.mem (γ := AddSubmonoid ((i : ι) → β₂ i))
        (AddSubmonoid.pi (M := β₂) Set.univ fun (i : ι) ↦ AddMonoidHom.mrange (f i)) (⇑x : (a : ι) → β₂ a)
⊢ Eq (α := AddSubmonoid (Π₀ (i : ι), β₂ i)) (AddMonoidHom.mrange (mapRange.addMonoidHom (β₁ := β₁) (β₂ := β₂) f))
    (AddSubmonoid.comap (F := (Π₀ (i : ι), β₂ i) →+ (i : ι) → β₂ i) (coeFnAddMonoidHom (β := β₂))
      (AddSubmonoid.pi (M := β₂) Set.univ fun (i : ι) ↦ AddMonoidHom.mrange (f i)))
have h₂ : ∀ (x : Π₀ (i : ι), β₂ i),
  Membership.mem (γ := AddSubmonoid (Π₀ (i : ι), β₂ i))
      (AddMonoidHom.mrange (mapRange.addMonoidHom (β₁ := β₁) (β₂ := β₂) f)) x →
    ∀ (i : ι) (hi : Membership.mem (γ := Set ι) Set.univ i) (y : Π₀ (i : ι), β₁ i)
      (hy : (mapRange.addMonoidHom (β₁ := β₁) (β₂ := β₂) f : (a : Π₀ (i : ι), β₁ i) → Π₀ (i : ι), β₂ i) y = x),
      Membership.mem (γ := Set (β₂ i))
        ((fun (i : ι) ↦
            (AddSubsemigroup.carrier
                (AddSubmonoid.toAddSubsemigroup ((fun (i : ι) ↦ (AddMonoidHom.mrange (f i) : AddSubmonoid (β₂ i))) i)) :
              Set (β₂ i)))
          i)
        ((x : (a : ι) → β₂ a) i)
Tactic: classical
  ext x
  simp only [AddSubmonoid.mem_comap, coeFnAddMonoidHom_apply]
  refine ⟨fun ⟨y, hy⟩ i hi ↦ ?_, fun h ↦ ?_⟩
  · simp [← hy]
  · choose g hg using fun i => h i (Set.mem_univ _)
    use DFinsupp.mk x.support (g ·)
    ext i
    simp only [Finset.coe_sort_coe, mapRange.addMonoidHom_apply, mapRange_apply]
    by_cases mem : i ∈ x.support
    · rw [mk_of_mem mem, hg]
    · rw [DFinsupp.notMem_support_iff.mp mem, mk_of_notMem mem, map_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.DFinsupp (goal)
Goal:
ι : Type u_1
β₁ : ι → Type u_8
β₂ : ι → Type u_9
inst : (i : ι) → AddCommMonoid (β₁ i)
inst_1 : (i : ι) → AddCommMonoid (β₂ i)
f : (i : ι) → AddMonoidHom.{u_8, u_9} (β₁ i) (β₂ i)
h :
  ∀ (x : Π₀ (i : ι), β₂ i),
    Membership.mem (γ := AddSubmonoid (Π₀ (i : ι), β₂ i))
        (AddMonoidHom.mrange (mapRange.addMonoidHom (β₁ := β₁) (β₂ := β₂) f)) x ↔
      Membership.mem (γ := AddSubmonoid (Π₀ (i : ι), β₂ i))
        (AddSubmonoid.comap (F := (Π₀ (i : ι), β₂ i) →+ (i : ι) → β₂ i) (coeFnAddMonoidHom (β := β₂))
          (AddSubmonoid.pi (M := β₂) Set.univ fun (i : ι) ↦ AddMonoidHom.mrange (f i)))
        x
h₁ :
  ∀ (x : Π₀ (i : ι), β₂ i),
    Membership.mem (γ := AddSubmonoid (Π₀ (i : ι), β₂ i))
        (AddMonoidHom.mrange (mapRange.addMonoidHom (β₁ := β₁) (β₂ := β₂) f)) x ↔
      Membership.mem (γ := AddSubmonoid ((i : ι) → β₂ i))
        (AddSubmonoid.pi (M := β₂) Set.univ fun (i : ι) ↦ AddMonoidHom.mrange (f i)) (⇑x : (a : ι) → β₂ a)
h₂ :
  ∀ (x : Π₀ (i : ι), β₂ i),
    Membership.mem (γ := AddSubmonoid (Π₀ (i : ι), β₂ i))
        (AddMonoidHom.mrange (mapRange.addMonoidHom (β₁ := β₁) (β₂ := β₂) f)) x →
      ∀ (i : ι) (hi : Membership.mem (γ := Set ι) Set.univ i) (y : Π₀ (i : ι), β₁ i)
        (hy : (mapRange.addMonoidHom (β₁ := β₁) (β₂ := β₂) f : (a : Π₀ (i : ι), β₁ i) → Π₀ (i : ι), β₂ i) y = x),
        Membership.mem (γ := Set (β₂ i))
          ((fun (i : ι) ↦
              (AddSubsemigroup.carrier
                  (AddSubmonoid.toAddSubsemigroup
                    ((fun (i : ι) ↦ (AddMonoidHom.mrange (f i) : AddSubmonoid (β₂ i))) i)) :
                Set (β₂ i)))
            i)
          ((x : (a : ι) → β₂ a) i)
⊢ Eq (α := AddSubmonoid (Π₀ (i : ι), β₂ i)) (AddMonoidHom.mrange (mapRange.addMonoidHom (β₁ := β₁) (β₂ := β₂) f))
    (AddSubmonoid.comap (F := (Π₀ (i : ι), β₂ i) →+ (i : ι) → β₂ i) (coeFnAddMonoidHom (β := β₂))
      (AddSubmonoid.pi (M := β₂) Set.univ fun (i : ι) ↦ AddMonoidHom.mrange (f i)))
have h₃ : ∀ (x : Π₀ (i : ι), β₂ i)
  (h :
    Membership.mem (γ := AddSubmonoid ((i : ι) → β₂ i))
      (AddSubmonoid.pi (M := β₂) Set.univ fun (i : ι) ↦ AddMonoidHom.mrange (f i)) (⇑x : (a : ι) → β₂ a)),
  Membership.mem (γ := AddSubmonoid (Π₀ (i : ι), β₂ i))
    (AddMonoidHom.mrange (mapRange.addMonoidHom (β₁ := β₁) (β₂ := β₂) f)) x
Tactic: classical
  ext x
  simp only [AddSubmonoid.mem_comap, coeFnAddMonoidHom_apply]
  refine ⟨fun ⟨y, hy⟩ i hi ↦ ?_, fun h ↦ ?_⟩
  · simp [← hy]
  · choose g hg using fun i => h i (Set.mem_univ _)
    use DFinsupp.mk x.support (g ·)
    ext i
    simp only [Finset.coe_sort_coe, mapRange.addMonoidHom_apply, mapRange_apply]
    by_cases mem : i ∈ x.support
    · rw [mk_of_mem mem, hg]
    · rw [DFinsupp.notMem_support_iff.mp mem, mk_of_notMem mem, map_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.DFinsupp (goal)
Goal:
ι : Type u_1
R : Type u_3
inst : Semiring R
β₁ : ι → Type u_8
β₂ : ι → Type u_9
inst_1 : (i : ι) → AddCommMonoid (β₁ i)
inst_2 : (i : ι) → AddCommMonoid (β₂ i)
inst_3 : (i : ι) → Module.{u_3, u_8} R (β₁ i)
inst_4 : (i : ι) → Module.{u_3, u_9} R (β₂ i)
f : (i : ι) → β₁ i → β₂ i
hf : ∀ (i : ι), f i 0 = 0
r : R
hf' : ∀ (i : ι) (x : β₁ i), f i (r • x) = r • f i x
g : Π₀ (i : ι), β₁ i
⊢ mapRange (β₁ := β₁) (β₂ := β₂) f hf (r • g) = r • mapRange (β₁ := β₁) (β₂ := β₂) f hf g
have h : ∀ (i : ι),
  (mapRange (β₁ := β₁) (β₂ := β₂) f hf (r • g) : (a : ι) → β₂ a) i =
    (r • mapRange (β₁ := β₁) (β₂ := β₂) f hf g : (a : ι) → β₂ a) i
Tactic: ext
-- Lean 4 proof step from Mathlib.LinearAlgebra.DFinsupp (goal)
Goal:
ι : Type u_1
R : Type u_3
inst : Semiring R
β₂ : ι → Type u_9
inst_1 : (i : ι) → AddCommMonoid (β₂ i)
inst_2 : (i : ι) → Module.{u_3, u_9} R (β₂ i)
⊢ Eq (α := (Π₀ (i : ι), β₂ i) →ₗ[R] Π₀ (i : ι), β₂ i) (linearMap (β₁ := β₂) (β₂ := β₂) fun (i : ι) ↦ LinearMap.id)
    LinearMap.id
have h : ∀ (x : Π₀ (i : ι), β₂ i) (i : ι),
  (((linearMap (β₁ := β₂) (β₂ := β₂) fun (i : ι) ↦ LinearMap.id : (a : Π₀ (i : ι), β₂ i) → Π₀ (i : ι), β₂ i) x :
          Π₀ (i : ι), β₂ i) :
        (a : ι) → β₂ a)
      i =
    (((LinearMap.id : (a : Π₀ (i : ι), β₂ i) → Π₀ (i : ι), β₂ i) x : Π₀ (i : ι), β₂ i) : (a : ι) → β₂ a) i
Tactic: ext