awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.DFinsupp
Goal:
ι : Type u_1
R : Type u_3
M : ι → Type u_5
inst : Semiring R
inst_1 : (i : ι) → AddCommMonoid (M i)
inst_2 : (i : ι) → Module.{u_3, u_5} R (M i)
inst_3 : DecidableEq ι
m : Π₀ (i : ι), M i
h : Membership.mem (γ := Submodule R (Π₀ (i : ι), M i)) ⊤ m
rw :
  Membership.mem (α := Π₀ (i : ι), M i) (γ := Submodule R (Π₀ (i : ι), M i))
    (⨆ (i : ι), LinearMap.range (lsingle (M := M) i))
    ((((lsum ℕ (M := M) : (a : (i : ι) → M i →ₗ[R] Π₀ (i : ι), M i) → (Π₀ (i : ι), M i) →ₗ[R] Π₀ (i : ι), M i)
              (lsingle (M := M)) :
            (Π₀ (i : ι), M i) →ₗ[R] Π₀ (i : ι), M i) :
          (a : Π₀ (i : ι), M i) → Π₀ (i : ι), M i)
        m :
      Π₀ (i : ι), M i)
⊢ Membership.mem (γ := Submodule R (Π₀ (i : ι), M i)) (⨆ (i : ι), LinearMap.range (lsingle (M := M) i)) m

Tactic:
rw [← LinearMap.id_apply (R := R) m, ← lsum_lsingle ℕ]

Premises used: DFinsupp.lsum_lsingle, LinearMap.id_apply, Nat
-- Module: Mathlib.LinearAlgebra.DFinsupp
Goal:
ι : Type u_1
R : Type u_3
M : ι → Type u_5
inst : Semiring R
inst_1 : (i : ι) → AddCommMonoid (M i)
inst_2 : (i : ι) → Module.{u_3, u_5} R (M i)
inst_3 : DecidableEq ι
m : Π₀ (i : ι), M i
h : Membership.mem (γ := Submodule R (Π₀ (i : ι), M i)) ⊤ m
⊢ Membership.mem (α := Π₀ (i : ι), M i) (γ := Submodule R (Π₀ (i : ι), M i))
    (⨆ (i : ι), LinearMap.range (lsingle (M := M) i))
    ((((lsum ℕ (M := M) : (a : (i : ι) → M i →ₗ[R] Π₀ (i : ι), M i) → (Π₀ (i : ι), M i) →ₗ[R] Π₀ (i : ι), M i)
              (lsingle (M := M)) :
            (Π₀ (i : ι), M i) →ₗ[R] Π₀ (i : ι), M i) :
          (a : Π₀ (i : ι), M i) → Π₀ (i : ι), M i)
        m :
      Π₀ (i : ι), M i)

Tactic:
dfinsuppSumAddHom_mem _ _ _ fun i _ ↦ Submodule.mem_iSup_of_mem i ⟨_, rfl⟩

Premises used: Set.Mem, Exists.intro, Submodule.mem_iSup_of_mem, dfinsuppSumAddHom_mem, DFunLike.coe, rfl, Trunc.lift
-- Module: Mathlib.LinearAlgebra.DFinsupp
Goal:
ι : Type u_1
R : Type u_3
M : ι → Type u_5
inst : Semiring R
inst_1 : (i : ι) → AddCommMonoid (M i)
inst_2 : (i : ι) → Module.{u_3, u_5} R (M i)
inst_3 : DecidableEq ι
m : Π₀ (i : ι), M i
h : Membership.mem (γ := Submodule R (Π₀ (i : ι), M i)) ⊤ m
⊢ Membership.mem (α := Π₀ (i : ι), M i) (γ := Submodule R (Π₀ (i : ι), M i))
    (⨆ (i : ι), LinearMap.range (lsingle (M := M) i))
    ((((lsum ℕ (M := M) : (a : (i : ι) → M i →ₗ[R] Π₀ (i : ι), M i) → (Π₀ (i : ι), M i) →ₗ[R] Π₀ (i : ι), M i)
              (lsingle (M := M)) :
            (Π₀ (i : ι), M i) →ₗ[R] Π₀ (i : ι), M i) :
          (a : Π₀ (i : ι), M i) → Π₀ (i : ι), M i)
        m :
      Π₀ (i : ι), M i)

Tactic:
exact dfinsuppSumAddHom_mem _ _ _ fun i _ ↦ Submodule.mem_iSup_of_mem i ⟨_, rfl⟩
-- Module: Mathlib.LinearAlgebra.DFinsupp
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.mker (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.mker (f i)))
        x
⊢ Eq (α := AddSubmonoid (Π₀ (i : ι), β₁ i)) (AddMonoidHom.mker (mapRange.addMonoidHom (β₁ := β₁) (β₂ := β₂) f))
    (AddSubmonoid.comap (F := (Π₀ (i : ι), β₁ i) →+ (i : ι) → β₁ i) (coeFnAddMonoidHom (β := β₁))
      (AddSubmonoid.pi (M := β₁) Set.univ fun (i : ι) ↦ AddMonoidHom.mker (f i)))

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.DFinsupp
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.mker (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.mker (f i)))
      x

Tactic:
simp [AddSubmonoid.pi, DFinsupp.ext_iff]

Premises used: DFinsupp.ext_iff, AddSubmonoid.pi
-- Module: Mathlib.LinearAlgebra.DFinsupp
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)))

Tactic:
ext x
-- Module: Mathlib.LinearAlgebra.DFinsupp
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 ↔
    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 ↔
    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:
simp only [AddSubmonoid.mem_comap, coeFnAddMonoidHom_apply]

Premises used: DFinsupp.coeFnAddMonoidHom_apply, AddSubmonoid.mem_comap
-- Module: Mathlib.LinearAlgebra.DFinsupp
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)

Tactic:
⟨fun ⟨y, hy⟩ i hi ↦ ?_, fun h ↦ ?_⟩

Premises used: _private.0.DFinsupp.mrange_mapRangeAddMonoidHom.match_1, AddSubsemigroup.carrier, Membership.mem, AddMonoidHom.mrange, AddSubmonoid.toAddSubsemigroup, Iff.intro, DFunLike.coe
-- Module: Mathlib.LinearAlgebra.DFinsupp
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)
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
⊢ 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:
refine ⟨fun ⟨y, hy⟩ i hi ↦ ?_, fun h ↦ ?_⟩
-- Module: Mathlib.LinearAlgebra.DFinsupp
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)

Tactic:
simp [← hy]
-- Module: Mathlib.LinearAlgebra.DFinsupp
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)
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
⊢ Membership.mem (γ := AddSubmonoid (Π₀ (i : ι), β₂ i))
    (AddMonoidHom.mrange (mapRange.addMonoidHom (β₁ := β₁) (β₂ := β₂) f)) x

Tactic:
choose g hg using fun i => h i (Set.mem_univ _)

Premises used: Set.mem_univ
-- Module: Mathlib.LinearAlgebra.DFinsupp
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
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
⊢ Membership.mem (γ := AddSubmonoid (Π₀ (i : ι), β₂ i))
    (AddMonoidHom.mrange (mapRange.addMonoidHom (β₁ := β₁) (β₂ := β₂) f)) x

Tactic:
use DFinsupp.mk x.support (g ·)

Premises used: DFinsupp.mk, DFinsupp.support, Subtype.val
-- Module: Mathlib.LinearAlgebra.DFinsupp
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
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
⊢ (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:
ext i
-- Module: Mathlib.LinearAlgebra.DFinsupp
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 : ι
h₁ :
  (f i : (a : β₁ i) → β₂ i)
      ((mk (β := β₁) (x.support (β := β₂)) fun (x_1 : ↥(x.support (β := β₂))) ↦ g (↑x_1 : ι) : (a : ι) → β₁ a) 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 : ι)) :
          Π₀ (i : ι), β₂ i) :
        (a : ι) → β₂ a)
      i =
    (x : (a : ι) → β₂ a) i

Tactic:
simp only [Finset.coe_sort_coe, mapRange.addMonoidHom_apply, mapRange_apply]

Premises used: Finset.coe_sort_coe, DFinsupp.mapRange_apply, DFinsupp.mapRange.addMonoidHom_apply
-- Module: Mathlib.LinearAlgebra.DFinsupp
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
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
⊢ (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

Premises used: DFinsupp.support
-- Module: Mathlib.LinearAlgebra.DFinsupp
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
pos₁ pos₂ : (x : (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

Tactic:
rw [mk_of_mem mem, hg]

Premises used: DFinsupp.mk_of_mem
-- Module: Mathlib.LinearAlgebra.DFinsupp
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
neg₂ neg₃ : Eq.{u_9 + 1} (α := β₂ 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

Tactic:
rw [DFinsupp.notMem_support_iff.mp mem, mk_of_notMem mem, map_zero]

Premises used: DFinsupp.notMem_support_iff, map_zero, Iff.mp, DFinsupp.mk_of_notMem
-- Module: Mathlib.LinearAlgebra.DFinsupp
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)
h₃ 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
⊢ 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)))

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]

Premises used: Finset.coe_sort_coe, DFinsupp.coeFnAddMonoidHom_apply, map_zero, DFinsupp.mapRange_apply, AddSubmonoid.mem_comap, DFinsupp.mapRange.addMonoidHom_apply
-- Module: Mathlib.LinearAlgebra.DFinsupp
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
h :
  ∀ (i : ι),
    (mapRange (β₁ := β₁) (β₂ := β₂) f hf (r • g) : (a : ι) → β₂ a) i =
      (r • mapRange (β₁ := β₁) (β₂ := β₂) f hf g : (a : ι) → β₂ a) i
⊢ mapRange (β₁ := β₁) (β₂ := β₂) f hf (r • g) = r • mapRange (β₁ := β₁) (β₂ := β₂) f hf g

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.DFinsupp
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
i : ι
⊢ (mapRange (β₁ := β₁) (β₂ := β₂) f hf (r • g) : (a : ι) → β₂ a) i =
    (r • mapRange (β₁ := β₁) (β₂ := β₂) f hf g : (a : ι) → β₂ a) i

Tactic:
simp only [mapRange_apply f, coe_smul, Pi.smul_apply, hf']

Premises used: DFinsupp.coe_smul, DFinsupp.mapRange_apply, Pi.smul_apply
-- Module: Mathlib.LinearAlgebra.DFinsupp
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)
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
⊢ Eq (α := (Π₀ (i : ι), β₂ i) →ₗ[R] Π₀ (i : ι), β₂ i) (linearMap (β₁ := β₂) (β₂ := β₂) fun (i : ι) ↦ LinearMap.id)
    LinearMap.id

Tactic:
ext
-- Module: Mathlib.LinearAlgebra.DFinsupp
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)
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:
simp [linearMap]

Premises used: DFinsupp.mapRange.linearMap
-- Module: Mathlib.LinearAlgebra.DFinsupp
Goal:
ι : Type u_1
R : Type u_3
inst : Semiring R
β : ι → Type u_7
β₁ : ι → Type u_8
β₂ : ι → Type u_9
inst_1 : (i : ι) → AddCommMonoid (β i)
inst_2 : (i : ι) → AddCommMonoid (β₁ i)
inst_3 : (i : ι) → AddCommMonoid (β₂ i)
inst_4 : (i : ι) → Module.{u_3, u_7} R (β i)
inst_5 : (i : ι) → Module.{u_3, u_8} R (β₁ i)
inst_6 : (i : ι) → Module.{u_3, u_9} R (β₂ i)
f : (i : ι) → LinearMap.{u_3, u_3, u_8, u_9} (RingHom.id R) (β₁ i) (β₂ i)
f₂ : (i : ι) → LinearMap.{u_3, u_3, u_7, u_8} (RingHom.id R) (β i) (β₁ i)
⊢ ∀ (i : ι),
    Eq.{u_9 + 1} (α := β₂ i)
      (Function.comp.{u_7 + 1, u_8 + 1, u_9 + 1} (α := β i) (β := β₁ i)
        ((fun (i : ι) (x : β₁ i) ↦ ((f i : (a : β₁ i) → β₂ i) x : β₂ i)) i)
        ((fun (i : ι) (x : β i) ↦ ((f₂ i : (a : β i) → β₁ i) x : β₁ i)) i) 0)
      0

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.DFinsupp
Goal:
ι : Type u_1
R : Type u_3
N : Type u_6
inst : Semiring R
inst_1 : AddCommMonoid N
inst_2 : Module R N
β₁ : ι → Type u_8
β₂ : ι → Type u_9
inst_3 : (i : ι) → AddCommMonoid (β₁ i)
inst_4 : (i : ι) → AddCommMonoid (β₂ i)
inst_5 : (i : ι) → Module.{u_3, u_8} R (β₁ i)
inst_6 : (i : ι) → Module.{u_3, u_9} R (β₂ i)
inst_7 : DecidableEq ι
f : (i : ι) → LinearMap.{u_3, u_3, u_8, u_9} (RingHom.id R) (β₁ i) (β₂ i)
h : (i : ι) → LinearMap.{u_3, u_3, u_9, u_6} (RingHom.id R) (β₂ i) N
l : Π₀ (i : ι), β₁ i
i : ι
⊢ Eq.{u_6 + 1} (α := N) ((h i : (a : β₂ i) → N) 0 : N) (0 : N)

Tactic:
simp