awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.DirectSum.Module
Goal:
R : Type u
inst : Semiring R
ι : Type v
M : ι → Type w
inst_1 : (i : ι) → AddCommMonoid (M i)
inst_2 : (i : ι) → Module.{u, w} R (M i)
inst_3 : DecidableEq ι
N : Type u₁
inst_4 : AddCommMonoid N
inst_5 : Module R N
ψ : (⨁ (i : ι), M i) →ₗ[R] N
f : ⨁ (i : ι), M i
⊢ Eq.{u₁ + 1} (α := N) ((ψ : (a : ⨁ (i : ι), M i) → N) f : N)
    ((toModule R ι (M := M) N fun (i : ι) ↦ ψ ∘ₗ lof R ι M i : (a : ⨁ (i : ι), M i) → N) f : N)

Tactic:
toAddMonoid.unique ψ.toAddMonoidHom f

Premises used: LinearMap.toAddMonoidHom, DirectSum.toAddMonoid.unique, Trunc.lift
-- Module: Mathlib.Algebra.DirectSum.Module
Goal:
R : Type u
inst : Semiring R
ι : Type v
M : ι → Type w
inst_1 : (i : ι) → AddCommMonoid (M i)
inst_2 : (i : ι) → Module.{u, w} R (M i)
inst_3 : DecidableEq ι
N : Type u₁
inst_4 : AddCommMonoid N
inst_5 : Module R N
ψ ψ' : (⨁ (i : ι), M i) →ₗ[R] N
H : ∀ (i : ι), ψ ∘ₗ lof R ι M i = ψ' ∘ₗ lof R ι M i
⊢ ψ = ψ'

Tactic:
DFinsupp.lhom_ext' H

Premises used: DFinsupp.lhom_ext', DirectSum
-- Module: Mathlib.Algebra.DirectSum.Module
Goal:
R : Type u
inst : Semiring R
ι : Type v
M : ι → Type w
inst_1 : (i : ι) → AddCommMonoid (M i)
inst_2 : (i : ι) → Module.{u, w} R (M i)
inst_3 : DecidableEq ι
inst_4 : Fintype ι
i : ι
m : M i
⊢ (linearEquivFunOnFintype R ι M : (a : ⨁ (i : ι), M i) → (i : ι) → M i)
      ((lof R ι M i : (a : M i) → ⨁ (i : ι), M i) m : ⨁ (i : ι), M i) =
    Pi.single (M := M) i m

Tactic:
rfl
-- Module: Mathlib.Algebra.DirectSum.Module
Goal:
R : Type u
inst : Semiring R
ι : Type v
M : ι → Type w
inst_1 : (i : ι) → AddCommMonoid (M i)
inst_2 : (i : ι) → Module.{u, w} R (M i)
inst_3 : DecidableEq ι
inst_4 : Fintype ι
i : ι
m : M i
⊢ Eq (α := ⨁ (i : ι), M i)
    ((LinearEquiv.symm (linearEquivFunOnFintype R ι M) : (a : (i : ι) → M i) → ⨁ (i : ι), M i)
        (Pi.single (M := M) i m) :
      ⨁ (i : ι), M i)
    ((lof R ι M i : (a : M i) → ⨁ (i : ι), M i) m : ⨁ (i : ι), M i)

Tactic:
DFinsupp.equivFunOnFintype_symm_single i m

Premises used: DFinsupp.single, DirectSum, DFinsupp.equivFunOnFintype_symm_single
-- Module: Mathlib.Algebra.DirectSum.Module
Goal:
R : Type u
inst : Semiring R
ι : Type v
M : ι → Type w
inst_1 : (i : ι) → AddCommMonoid (M i)
inst_2 : (i : ι) → Module.{u, w} R (M i)
inst_3 : Fintype ι
f : ⨁ (i : ι), M i
⊢ (LinearEquiv.symm (linearEquivFunOnFintype R ι M) : (a : (i : ι) → M i) → ⨁ (i : ι), M i) (⇑f : (a : ι) → M a) = f

Tactic:
(linearEquivFunOnFintype R ι M).symm_apply_apply _

Premises used: LinearEquiv.symm_apply_apply, DirectSum.linearEquivFunOnFintype
-- Module: Mathlib.Algebra.DirectSum.Module
Goal:
R : Type u
inst : Semiring R
M : Type v
ι : Type u_1
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Unique ι
x : ⨁ (x : ι), M
⊢ (DirectSum.lid R M ι : (a : ⨁ (x : ι), M) → M) x = (x : (a : ι) → M) default

Tactic:
DirectSum.id_apply x

Premises used: DirectSum.id_apply
-- Module: Mathlib.Algebra.DirectSum.Module
Goal:
R : Type u
inst : Semiring R
M : Type v
ι : Type u_1
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Unique ι
x : M
⊢ Eq (α := ⨁ (x : ι), M) ((LinearEquiv.symm (DirectSum.lid R M ι) : (a : M) → ⨁ (x : ι), M) x : ⨁ (x : ι), M)
    (((lof.{u, u_1, v} R ι (fun (i : ι) ↦ M) default : M →ₗ[R] ⨁ (i : ι), M) : (a : M) → ⨁ (i : ι), M) x : ⨁ (i : ι), M)

Tactic:
DirectSum.id_symm_apply x

Premises used: DFinsupp.single, DirectSum.id_symm_apply
-- Module: Mathlib.Algebra.DirectSum.Module
Goal:
R : Type u
inst : Semiring R
ι : Type v
M : ι → Type w
inst_1 : (i : ι) → AddCommMonoid (M i)
inst_2 : (i : ι) → Module.{u, w} R (M i)
f : ⨁ (i : ι), M i
i : ι
⊢ (f : (a : ι) → M a) i = (component R ι M i : (a : ⨁ (i : ι), M i) → M i) f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.DirectSum.Module
Goal:
R : Type u
inst : Semiring R
ι : Type v
M : ι → Type w
inst_1 : (i : ι) → AddCommMonoid (M i)
inst_2 : (i : ι) → Module.{u, w} R (M i)
f g : ⨁ (i : ι), M i
h :
  ∀ (i : ι),
    Eq.{w + 1} (α := M i) ((component R ι M i : (a : ⨁ (i : ι), M i) → M i) f : M i)
      ((component R ι M i : (a : ⨁ (i : ι), M i) → M i) g : M i)
⊢ f = g

Tactic:
DFinsupp.ext h

Premises used: DFinsupp.ext, DirectSum
-- Module: Mathlib.Algebra.DirectSum.Module
Goal:
R : Type u
inst : Semiring R
ι : Type v
M : ι → Type w
inst_1 : (i : ι) → AddCommMonoid (M i)
inst_2 : (i : ι) → Module.{u, w} R (M i)
f g : ⨁ (i : ι), M i
h : f = g
x : ι
rw rw₁ :
  Eq.{w + 1} (α := M x) ((component R ι M x : (a : ⨁ (i : ι), M i) → M x) g : M x)
    ((component R ι M x : (a : ⨁ (i : ι), M i) → M x) g : M x)
⊢ Eq.{w + 1} (α := M x) ((component R ι M x : (a : ⨁ (i : ι), M i) → M x) f : M x)
    ((component R ι M x : (a : ⨁ (i : ι), M i) → M x) g : M x)

Tactic:
rw [h]
-- Module: Mathlib.Algebra.DirectSum.Module
Goal:
R : Type u
inst : Semiring R
ι : Type v
M : ι → Type w
inst_1 : (i : ι) → AddCommMonoid (M i)
inst_2 : (i : ι) → Module.{u, w} R (M i)
inst_3 : DecidableEq ι
i : ι
b : M i
⊢ (((lof R ι M i : (a : M i) → ⨁ (i : ι), M i) b : ⨁ (i : ι), M i) : (a : ι) → M a) i = b

Tactic:
DFinsupp.single_eq_same

Premises used: DFinsupp.single_eq_same
-- Module: Mathlib.Algebra.DirectSum.Module
Goal:
R : Type u
inst : Semiring R
ι : Type v
M : ι → Type w
inst_1 : (i : ι) → AddCommMonoid (M i)
inst_2 : (i : ι) → Module.{u, w} R (M i)
inst_3 : DecidableEq ι
i : ι
b : M i
⊢ (component R ι M i : (a : ⨁ (i : ι), M i) → M i) ((lof R ι M i : (a : M i) → ⨁ (i : ι), M i) b) = b

Tactic:
lof_apply R i b

Premises used: Function.update, Pi.single, dite, DirectSum.lof_apply
-- Module: Mathlib.Algebra.DirectSum.Module
Goal:
R : Type u
inst : Semiring R
ι : Type v
M : ι → Type w
inst_1 : (i : ι) → AddCommMonoid (M i)
inst_2 : (i : ι) → Module.{u, w} R (M i)
inst_3 : DecidableEq ι
i j : ι
b : M j
⊢ Eq.{w + 1} (α := M i)
    ((component R ι M i : (a : ⨁ (i : ι), M i) → M i) ((lof R ι M j : (a : M j) → ⨁ (i : ι), M i) b) : M i)
    (if h : j = i then Eq.recOn (motive := fun (x : ι) (x_1 : j = x) ↦ M x) h b else 0 : M i)

Tactic:
DFinsupp.single_apply

Premises used: Function.update, Pi.single, dite, DFinsupp.single_apply
-- Module: Mathlib.Algebra.DirectSum.Module
Goal:
R : Type u
inst : Semiring R
ι : Type v
M : ι → Type w
inst_1 : (i : ι) → AddCommMonoid (M i)
inst_2 : (i : ι) → Module.{u, w} R (M i)
inst_3 : DecidableEq ι
i j : ι
⊢ Eq (α := M j →ₗ[R] M i) (component R ι M i ∘ₗ lof R ι M j)
    (if h : j = i then Eq.rec (motive := fun (x : ι) (h : j = x) ↦ M j →ₗ[R] M x) LinearMap.id h else 0)

Tactic:
aesop (add simp component.of)

Premises used: DirectSum.component.of
-- Module: Mathlib.Algebra.DirectSum.Module
Goal:
R : Type u
inst : Semiring R
ι : Type v
M : ι → Type w
inst_1 : (i : ι) → AddCommMonoid (M i)
inst_2 : (i : ι) → Module.{u, w} R (M i)
inst_3 : DecidableEq ι
i : ι
⊢ Eq (α := M i →ₗ[R] M i) (component R ι M i ∘ₗ lof R ι M i) LinearMap.id

Tactic:
simp [component_comp_lof]

Premises used: DirectSum.component_comp_lof
-- Module: Mathlib.Algebra.DirectSum.Module
Goal:
ι : Type v
M : ι → Type w
inst : (i : ι) → AddCommMonoid (M i)
N : ι → Type u_1
inst_1 : (i : ι) → AddCommMonoid (N i)
f : (i : ι) → AddMonoidHom.{w, u_1} (M i) (N i)
⊢ Eq (α := AddSubmonoid (⨁ (i : ι), M i)) (AddMonoidHom.mker (map (α := M) (β := N) f))
    (AddSubmonoid.comap (F := (⨁ (i : ι), M i) →+ (i : ι) → M i) (coeFnAddMonoidHom M)
      (AddSubmonoid.pi (M := M) Set.univ fun (i : ι) ↦ AddMonoidHom.mker (f i)))

Tactic:
DFinsupp.mker_mapRangeAddMonoidHom f

Premises used: DFinsupp.mker_mapRangeAddMonoidHom, DirectSum.coeFnAddMonoidHom, DFinsupp.coeFnAddMonoidHom, DirectSum.map, DirectSum
-- Module: Mathlib.Algebra.DirectSum.Module
Goal:
ι : Type v
M : ι → Type w
inst : (i : ι) → AddCommMonoid (M i)
N : ι → Type u_1
inst_1 : (i : ι) → AddCommMonoid (N i)
f : (i : ι) → AddMonoidHom.{w, u_1} (M i) (N i)
⊢ Eq (α := AddSubmonoid (⨁ (i : ι), N i)) (AddMonoidHom.mrange (map (α := M) (β := N) f))
    (AddSubmonoid.comap (F := (⨁ (i : ι), N i) →+ (i : ι) → N i) (coeFnAddMonoidHom N)
      (AddSubmonoid.pi (M := N) Set.univ fun (i : ι) ↦ AddMonoidHom.mrange (f i)))

Tactic:
DFinsupp.mrange_mapRangeAddMonoidHom f

Premises used: DFinsupp.mrange_mapRangeAddMonoidHom, DirectSum.coeFnAddMonoidHom, DFinsupp.coeFnAddMonoidHom, DirectSum.map, DirectSum
-- Module: Mathlib.Algebra.DirectSum.Module
Goal:
R : Type u
inst : Semiring R
ι : Type v
M : ι → Type w
inst_1 : (i : ι) → AddCommMonoid (M i)
inst_2 : (i : ι) → Module.{u, w} R (M i)
N : ι → Type u_1
inst_3 : (i : ι) → AddCommMonoid (N i)
inst_4 : (i : ι) → Module.{u, u_1} R (N i)
f : (i : ι) → LinearMap.{u, u, w, u_1} (RingHom.id R) (M i) (N i)
x : ⨁ (i : ι), M i
i : ι
⊢ (((lmap (M := M) (N := N) f : (a : ⨁ (i : ι), M i) → ⨁ (i : ι), N i) x : ⨁ (i : ι), N i) : (a : ι) → N a) i =
    (f i : (a : M i) → N i) ((x : (a : ι) → M a) i)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.DirectSum.Module
Goal:
R : Type u
inst : Semiring R
ι : Type v
M : ι → Type w
inst_1 : (i : ι) → AddCommMonoid (M i)
inst_2 : (i : ι) → Module.{u, w} R (M i)
N : ι → Type u_1
inst_3 : (i : ι) → AddCommMonoid (N i)
inst_4 : (i : ι) → Module.{u, u_1} R (N i)
f : (i : ι) → LinearMap.{u, u, w, u_1} (RingHom.id R) (M i) (N i)
inst_5 : DecidableEq ι
i : ι
x : M i
⊢ Eq (α := ⨁ (i : ι), N i)
    ((lmap (M := M) (N := N) f : (a : ⨁ (i : ι), M i) → ⨁ (i : ι), N i) ((of M i : (a : M i) → ⨁ (i : ι), M i) x) :
      ⨁ (i : ι), N i)
    ((of N i : (a : N i) → ⨁ (i : ι), N i) ((f i : (a : M i) → N i) x) : ⨁ (i : ι), N i)

Tactic:
DFinsupp.mapRange_single (hf := fun _ => map_zero _)

Premises used: DFinsupp.single, DFinsupp.mapRange_single, DFinsupp.mapRange, DirectSum
-- Module: Mathlib.Algebra.DirectSum.Module
Goal:
R : Type u
inst : Semiring R
ι : Type v
M : ι → Type w
inst_1 : (i : ι) → AddCommMonoid (M i)
inst_2 : (i : ι) → Module.{u, w} R (M i)
N : ι → Type u_1
inst_3 : (i : ι) → AddCommMonoid (N i)
inst_4 : (i : ι) → Module.{u, u_1} R (N i)
f : (i : ι) → LinearMap.{u, u, w, u_1} (RingHom.id R) (M i) (N i)
inst_5 : DecidableEq ι
i : ι
x : M i
⊢ Eq (α := ⨁ (i : ι), N i)
    ((lmap (M := M) (N := N) f : (a : ⨁ (i : ι), M i) → ⨁ (i : ι), N i) ((lof R ι M i : (a : M i) → ⨁ (i : ι), M i) x) :
      ⨁ (i : ι), N i)
    ((lof R ι N i : (a : N i) → ⨁ (i : ι), N i) ((f i : (a : M i) → N i) x) : ⨁ (i : ι), N i)

Tactic:
DFinsupp.mapRange_single (hf := fun _ ↦ map_zero _)

Premises used: DFinsupp.single, DFinsupp.mapRange_single, DFinsupp.mapRange, DirectSum
-- Module: Mathlib.Algebra.DirectSum.Module
Goal:
R : Type u
inst : Semiring R
ι : Type v
M : ι → Type w
inst_1 : (i : ι) → AddCommMonoid (M i)
inst_2 : (i : ι) → Module.{u, w} R (M i)
⊢ Eq (α := (⨁ (i : ι), M i) →ₗ[R] ⨁ (i : ι), M i) (lmap (M := M) (N := M) fun (i : ι) ↦ LinearMap.id) LinearMap.id

Tactic:
DFinsupp.mapRange.linearMap_id

Premises used: DirectSum.lmap, DFinsupp.mapRange.linearMap_id, DirectSum
-- Module: Mathlib.Algebra.DirectSum.Module
Goal:
R : Type u
inst : Semiring R
ι : Type v
M : ι → Type w
inst_1 : (i : ι) → AddCommMonoid (M i)
inst_2 : (i : ι) → Module.{u, w} R (M i)
N : ι → Type u_1
inst_3 : (i : ι) → AddCommMonoid (N i)
inst_4 : (i : ι) → Module.{u, u_1} R (N i)
f : (i : ι) → LinearMap.{u, u, w, u_1} (RingHom.id R) (M i) (N i)
K : ι → Type u_2
inst_5 : (i : ι) → AddCommMonoid (K i)
inst_6 : (i : ι) → Module.{u, u_2} R (K i)
g : (i : ι) → LinearMap.{u, u, u_1, u_2} (RingHom.id R) (N i) (K i)
⊢ (lmap (M := M) (N := K) fun (i : ι) ↦ g i ∘ₗ f i) = lmap (M := N) (N := K) g ∘ₗ lmap (M := M) (N := N) f

Tactic:
DFinsupp.mapRange.linearMap_comp _ _

Premises used: DirectSum.lmap, DFinsupp.mapRange.linearMap_comp, DirectSum
-- Module: Mathlib.Algebra.DirectSum.Module
Goal:
R : Type u
inst : Semiring R
ι : Type v
M : ι → Type w
inst_1 : (i : ι) → AddCommMonoid (M i)
inst_2 : (i : ι) → Module.{u, w} R (M i)
N : ι → Type u_1
inst_3 : (i : ι) → AddCommMonoid (N i)
inst_4 : (i : ι) → Module.{u, u_1} R (N i)
f : (i : ι) → LinearMap.{u, u, w, u_1} (RingHom.id R) (M i) (N i)
⊢ Function.Injective (α := ⨁ (i : ι), M i) (β := ⨁ (i : ι), N i)
      (⇑(lmap (M := M) (N := N) f) : (a : ⨁ (i : ι), M i) → ⨁ (i : ι), N i) ↔
    ∀ (i : ι), Function.Injective.{w + 1, u_1 + 1} (α := M i) (β := N i) (⇑(f i) : (a : M i) → N i)

Tactic:
DFinsupp.mapRange_injective (hf := fun _ ↦ map_zero _)

Premises used: map_zero, DFinsupp.mapRange, DFinsupp.mapRange_injective, DirectSum
-- Module: Mathlib.Algebra.DirectSum.Module
Goal:
R : Type u
inst : Semiring R
ι : Type v
M : ι → Type w
inst_1 : (i : ι) → AddCommMonoid (M i)
inst_2 : (i : ι) → Module.{u, w} R (M i)
N : ι → Type u_1
inst_3 : (i : ι) → AddCommMonoid (N i)
inst_4 : (i : ι) → Module.{u, u_1} R (N i)
f : (i : ι) → LinearMap.{u, u, w, u_1} (RingHom.id R) (M i) (N i)
⊢ Function.Injective (α := ⨁ (i : ι), M i) (β := ⨁ (i : ι), N i)
      (⇑(lmap (M := M) (N := N) f) : (a : ⨁ (i : ι), M i) → ⨁ (i : ι), N i) ↔
    ∀ (i : ι), Function.Injective.{w + 1, u_1 + 1} (α := M i) (β := N i) (⇑(f i) : (a : M i) → N i)

Tactic:
exact DFinsupp.mapRange_injective (hf := fun _ ↦ map_zero _)

Premises used: map_zero, DFinsupp.mapRange_injective
-- Module: Mathlib.Algebra.DirectSum.Module
Goal:
R : Type u
inst : Semiring R
ι : Type v
M : ι → Type w
inst_1 : (i : ι) → AddCommMonoid (M i)
inst_2 : (i : ι) → Module.{u, w} R (M i)
N : ι → Type u_1
inst_3 : (i : ι) → AddCommMonoid (N i)
inst_4 : (i : ι) → Module.{u, u_1} R (N i)
f : (i : ι) → LinearMap.{u, u, w, u_1} (RingHom.id R) (M i) (N i)
⊢ Function.Injective (α := ⨁ (i : ι), M i) (β := ⨁ (i : ι), N i)
      (⇑(lmap (M := M) (N := N) f) : (a : ⨁ (i : ι), M i) → ⨁ (i : ι), N i) ↔
    ∀ (i : ι), Function.Injective.{w + 1, u_1 + 1} (α := M i) (β := N i) (⇑(f i) : (a : M i) → N i)

Tactic:
classical exact DFinsupp.mapRange_injective (hf := fun _ ↦ map_zero _)

Premises used: map_zero, DFinsupp.mapRange_injective
-- Module: Mathlib.Algebra.DirectSum.Module
Goal:
R : Type u
inst : Semiring R
ι : Type v
M : ι → Type w
inst_1 : (i : ι) → AddCommMonoid (M i)
inst_2 : (i : ι) → Module.{u, w} R (M i)
N : ι → Type u_1
inst_3 : (i : ι) → AddCommMonoid (N i)
inst_4 : (i : ι) → Module.{u, u_1} R (N i)
f : (i : ι) → LinearMap.{u, u, w, u_1} (RingHom.id R) (M i) (N i)
⊢ Function.Surjective (α := ⨁ (i : ι), M i) (β := ⨁ (i : ι), N i)
      (⇑(lmap (M := M) (N := N) f) : (a : ⨁ (i : ι), M i) → ⨁ (i : ι), N i) ↔
    ∀ (i : ι), Function.Surjective.{w + 1, u_1 + 1} (α := M i) (β := N i) (⇑(f i) : (a : M i) → N i)

Tactic:
DFinsupp.mapRange_surjective (hf := fun _ ↦ map_zero _)

Premises used: map_zero, DFinsupp.mapRange, DFinsupp.mapRange_surjective, DirectSum
-- Module: Mathlib.Algebra.DirectSum.Module
Goal:
R : Type u
inst : Semiring R
ι : Type v
M : ι → Type w
inst_1 : (i : ι) → AddCommMonoid (M i)
inst_2 : (i : ι) → Module.{u, w} R (M i)
N : ι → Type u_1
inst_3 : (i : ι) → AddCommMonoid (N i)
inst_4 : (i : ι) → Module.{u, u_1} R (N i)
f : (i : ι) → LinearMap.{u, u, w, u_1} (RingHom.id R) (M i) (N i)
⊢ Function.Surjective (α := ⨁ (i : ι), M i) (β := ⨁ (i : ι), N i)
      (⇑(lmap (M := M) (N := N) f) : (a : ⨁ (i : ι), M i) → ⨁ (i : ι), N i) ↔
    ∀ (i : ι), Function.Surjective.{w + 1, u_1 + 1} (α := M i) (β := N i) (⇑(f i) : (a : M i) → N i)

Tactic:
exact DFinsupp.mapRange_surjective (hf := fun _ ↦ map_zero _)

Premises used: map_zero, DFinsupp.mapRange_surjective
-- Module: Mathlib.Algebra.DirectSum.Module
Goal:
R : Type u
inst : Semiring R
ι : Type v
M : ι → Type w
inst_1 : (i : ι) → AddCommMonoid (M i)
inst_2 : (i : ι) → Module.{u, w} R (M i)
N : ι → Type u_1
inst_3 : (i : ι) → AddCommMonoid (N i)
inst_4 : (i : ι) → Module.{u, u_1} R (N i)
f : (i : ι) → LinearMap.{u, u, w, u_1} (RingHom.id R) (M i) (N i)
⊢ Function.Surjective (α := ⨁ (i : ι), M i) (β := ⨁ (i : ι), N i)
      (⇑(lmap (M := M) (N := N) f) : (a : ⨁ (i : ι), M i) → ⨁ (i : ι), N i) ↔
    ∀ (i : ι), Function.Surjective.{w + 1, u_1 + 1} (α := M i) (β := N i) (⇑(f i) : (a : M i) → N i)

Tactic:
classical exact DFinsupp.mapRange_surjective (hf := fun _ ↦ map_zero _)

Premises used: map_zero, DFinsupp.mapRange_surjective
-- Module: Mathlib.Algebra.DirectSum.Module
Goal:
R : Type u
inst : Semiring R
ι : Type v
M : ι → Type w
inst_1 : (i : ι) → AddCommMonoid (M i)
inst_2 : (i : ι) → Module.{u, w} R (M i)
N : ι → Type u_1
inst_3 : (i : ι) → AddCommMonoid (N i)
inst_4 : (i : ι) → Module.{u, u_1} R (N i)
f : (i : ι) → LinearMap.{u, u, w, u_1} (RingHom.id R) (M i) (N i)
x y : ⨁ (i : ι), M i
⊢ Eq (α := ⨁ (i : ι), N i) ((lmap (M := M) (N := N) f : (a : ⨁ (i : ι), M i) → ⨁ (i : ι), N i) x : ⨁ (i : ι), N i)
      ((lmap (M := M) (N := N) f : (a : ⨁ (i : ι), M i) → ⨁ (i : ι), N i) y : ⨁ (i : ι), N i) ↔
    ∀ (i : ι),
      Eq.{u_1 + 1} (α := N i) ((f i : (a : M i) → N i) ((x : (a : ι) → M a) i) : N i)
        ((f i : (a : M i) → N i) ((y : (a : ι) → M a) i) : N i)

Tactic:
map_eq_iff (fun i => (f i).toAddMonoidHom) _ _

Premises used: LinearMap.toAddMonoidHom, DirectSum.map_eq_iff
-- Module: Mathlib.Algebra.DirectSum.Module
Goal:
R : Type u
inst : Semiring R
ι : Type v
M : ι → Type w
inst_1 : (i : ι) → AddCommMonoid (M i)
inst_2 : (i : ι) → Module.{u, w} R (M i)
N : ι → Type u_1
inst_3 : (i : ι) → AddCommMonoid (N i)
inst_4 : (i : ι) → Module.{u, u_1} R (N i)
f : (i : ι) → LinearMap.{u, u, w, u_1} (RingHom.id R) (M i) (N i)
⊢ (lmap (M := M) (N := N) f).toAddMonoidHom = map (α := M) (β := N) fun (i : ι) ↦ (f i).toAddMonoidHom

Tactic:
rfl

Premises used: LinearMap.toAddMonoidHom, DFinsupp.mapRange, DFinsupp.mapRange.addMonoidHom, DirectSum.map, DirectSum, rfl
-- Module: Mathlib.Algebra.DirectSum.Module
Goal:
R : Type u
inst : Semiring R
ι : Type v
M : ι → Type w
inst_1 : (i : ι) → AddCommMonoid (M i)
inst_2 : (i : ι) → Module.{u, w} R (M i)
N : ι → Type u_1
inst_3 : (i : ι) → AddCommMonoid (N i)
inst_4 : (i : ι) → Module.{u, u_1} R (N i)
f : (i : ι) → LinearMap.{u, u, w, u_1} (RingHom.id R) (M i) (N i)
x : ⨁ (i : ι), M i
⊢ Eq (α := ⨁ (i : ι), N i) ((lmap (M := M) (N := N) f : (a : ⨁ (i : ι), M i) → ⨁ (i : ι), N i) x : ⨁ (i : ι), N i)
    ((map (α := M) (β := N) fun (i : ι) ↦ (f i).toAddMonoidHom : (a : ⨁ (i : ι), M i) → ⨁ (i : ι), N i) x :
      ⨁ (i : ι), N i)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.DirectSum.Module
Goal:
R : Type u
inst : Semiring R
ι : Type v
M : ι → Type w
inst_1 : (i : ι) → AddCommMonoid (M i)
inst_2 : (i : ι) → Module.{u, w} R (M i)
N : ι → Type u_1
inst_3 : (i : ι) → AddCommMonoid (N i)
inst_4 : (i : ι) → Module.{u, u_1} R (N i)
f : (i : ι) → LinearMap.{u, u, w, u_1} (RingHom.id R) (M i) (N i)
⊢ (lmap (M := M) (N := N) f).ker =
    Submodule.comap (coeFnLinearMap R (M := M)) (Submodule.pi (φ := M) Set.univ fun (i : ι) ↦ (f i).ker)

Tactic:
DFinsupp.ker_mapRangeLinearMap f

Premises used: DirectSum.lmap, DirectSum.coeFnLinearMap, DFinsupp.ker_mapRangeLinearMap, DirectSum
-- Module: Mathlib.Algebra.DirectSum.Module
Goal:
R : Type u
inst : Semiring R
ι : Type v
M : ι → Type w
inst_1 : (i : ι) → AddCommMonoid (M i)
inst_2 : (i : ι) → Module.{u, w} R (M i)
N : ι → Type u_1
inst_3 : (i : ι) → AddCommMonoid (N i)
inst_4 : (i : ι) → Module.{u, u_1} R (N i)
f : (i : ι) → LinearMap.{u, u, w, u_1} (RingHom.id R) (M i) (N i)
⊢ (lmap (M := M) (N := N) f).range =
    Submodule.comap (coeFnLinearMap R (M := N)) (Submodule.pi (φ := N) Set.univ fun (i : ι) ↦ (f i).range)

Tactic:
DFinsupp.range_mapRangeLinearMap f

Premises used: DirectSum.lmap, DFinsupp.range_mapRangeLinearMap, DirectSum.coeFnLinearMap, DirectSum
-- Module: Mathlib.Algebra.DirectSum.Module
Goal:
ι : Type v
M : ι → Type w
N : ι → Type u_2
inst : (i : ι) → AddCommGroup (M i)
inst_1 : (i : ι) → AddCommMonoid (N i)
f : (i : ι) → AddMonoidHom.{w, u_2} (M i) (N i)
⊢ Eq (α := AddSubgroup (⨁ (i : ι), M i)) (AddMonoidHom.ker (M := ⨁ (i : ι), N i) (map (α := M) (β := N) f))
    (AddSubgroup.comap (N := (i : ι) → M i) (coeFnAddMonoidHom M)
      (AddSubgroup.pi (f := M) Set.univ fun (x : ι) ↦ (f x).ker))

Tactic:
DFinsupp.ker_mapRangeAddMonoidHom f

Premises used: DFinsupp.ker_mapRangeAddMonoidHom, DirectSum.coeFnAddMonoidHom, DFinsupp.coeFnAddMonoidHom, DirectSum.map, DirectSum
-- Module: Mathlib.Algebra.DirectSum.Module
Goal:
ι : Type v
M : ι → Type w
N : ι → Type u_2
inst : (i : ι) → AddCommGroup (M i)
inst_1 : (i : ι) → AddCommGroup (N i)
f : (i : ι) → AddMonoidHom.{w, u_2} (M i) (N i)
⊢ Eq (α := AddSubgroup (⨁ (i : ι), N i)) (AddMonoidHom.range (G := ⨁ (i : ι), M i) (map (α := M) (β := N) f))
    (AddSubgroup.comap (N := (i : ι) → N i) (coeFnAddMonoidHom N)
      (AddSubgroup.pi (f := N) Set.univ fun (x : ι) ↦ (f x).range))

Tactic:
DFinsupp.range_mapRangeAddMonoidHom f

Premises used: DFinsupp.range_mapRangeAddMonoidHom, DirectSum.coeFnAddMonoidHom, DFinsupp.coeFnAddMonoidHom, DirectSum.map, DirectSum
-- Module: Mathlib.Algebra.DirectSum.Module
Goal:
R : Type u
inst : Semiring R
ι : Type v
M : ι → Type w
inst_1 : (i : ι) → AddCommMonoid (M i)
inst_2 : (i : ι) → Module.{u, w} R (M i)
κ : Type u_1
h : ι ≃ κ
f : ⨁ (i : ι), M i
k : κ
⊢ (((lequivCongrLeft R (M := M) h : (a : ⨁ (i : ι), M i) → ⨁ (k : κ), M ((h.symm : (a : κ) → ι) k)) f :
          ⨁ (k : κ), M ((h.symm : (a : κ) → ι) k)) :
        (a : κ) → M ((h.symm : (a : κ) → ι) a))
      k =
    (f : (a : ι) → M a) ((h.symm : (a : κ) → ι) k)

Tactic:
equivCongrLeft_apply _ _ _

Premises used: DirectSum.equivCongrLeft_apply
-- Module: Mathlib.Algebra.DirectSum.Module
Goal:
R : Type u
inst : Semiring R
ι : Type v
M : ι → Type w
inst_1 : (i : ι) → AddCommMonoid (M i)
inst_2 : (i : ι) → Module.{u, w} R (M i)
κ : Type u_1
inst_3 : DecidableEq ι
inst_4 : DecidableEq κ
e : ι ≃ κ
i : ι
k : κ
hik : i = (e.symm : (a : κ) → ι) k
x : M i
y : M ((e.symm : (a : κ) → ι) k)
hxy : cast ⋯ x = y
subst :
  ∀ (x : M ((e.symm : (a : κ) → ι) k)),
    Eq (α := ⨁ (k : κ), M ((e.symm : (a : κ) → ι) k))
      ((lequivCongrLeft R (M := M) e : (a : ⨁ (i : ι), M i) → ⨁ (k : κ), M ((e.symm : (a : κ) → ι) k))
          ((lof R ι M ((e.symm : (a : κ) → ι) k) : (a : M ((e.symm : (a : κ) → ι) k)) → ⨁ (i : ι), M i) x) :
        ⨁ (k : κ), M ((e.symm : (a : κ) → ι) k))
      (((lof.{u, u_1, w} R κ (fun (i : κ) ↦ M ((e.symm : (a : κ) → ι) i)) k :
              M ((e.symm : (a : κ) → ι) k) →ₗ[R] ⨁ (i : κ), M ((e.symm : (a : κ) → ι) i)) :
            (a : M ((e.symm : (a : κ) → ι) k)) → ⨁ (i : κ), M ((e.symm : (a : κ) → ι) i))
          (cast ⋯ x) :
        ⨁ (i : κ), M ((e.symm : (a : κ) → ι) i))
⊢ Eq (α := ⨁ (k : κ), M ((e.symm : (a : κ) → ι) k))
    ((lequivCongrLeft R (M := M) e : (a : ⨁ (i : ι), M i) → ⨁ (k : κ), M ((e.symm : (a : κ) → ι) k))
        ((lof R ι M i : (a : M i) → ⨁ (i : ι), M i) x) :
      ⨁ (k : κ), M ((e.symm : (a : κ) → ι) k))
    (((lof.{u, u_1, w} R κ (fun (i : κ) ↦ M ((e.symm : (a : κ) → ι) i)) k :
            M ((e.symm : (a : κ) → ι) k) →ₗ[R] ⨁ (i : κ), M ((e.symm : (a : κ) → ι) i)) :
          (a : M ((e.symm : (a : κ) → ι) k)) → ⨁ (i : κ), M ((e.symm : (a : κ) → ι) i))
        y :
      ⨁ (i : κ), M ((e.symm : (a : κ) → ι) i))

Tactic:
subst hik hxy