awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Finiteness.Finsupp
Goal:
R : Type u_1
M : Type u_2
P : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup P
inst_4 : Module R P
f : M →ₗ[R] P
s : Submodule R M
this_1 : DecidableEq R
this_2 : DecidableEq M
this : DecidableEq P
t1 : Finset P
ht1 : span R (↑t1 : Set P) = map f s
t2 : Finset M
ht2 : span R (↑t2 : Set M) = s ⊓ f.ker
g : P → M
hg : ∀ y ∈ t1, g y ∈ s ∧ (f : (a : M) → P) (g y) = y
x : M
hx : x ∈ s
l : P →₀ R
hl1 : Membership.mem (γ := Submodule R (P →₀ R)) (supported R R (↑t1 : Set P)) l
hl2 : Eq.{u_4 + 1} (α := P) ((linearCombination R id : (a : P →₀ R) → P) l : P) ((f : (a : M) → P) x : P)
a : ∀ c ∈ l.support, (fun (a : P) (m : R) ↦ m • id (g a)) c ((l : (a : P) → R) c) ∈ s
⊢ (l.sum fun (a : P) (m : R) ↦ m • id (g a)) ∈ s

Tactic:
refine s.sum_mem ?_

Premises used: Submodule.sum_mem
-- Module: Mathlib.RingTheory.Finiteness.Finsupp
Goal:
R : Type u_1
M : Type u_2
P : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup P
inst_4 : Module R P
f : M →ₗ[R] P
s : Submodule R M
this_1 : DecidableEq R
this_2 : DecidableEq M
this : DecidableEq P
t1 : Finset P
ht1 : span R (↑t1 : Set P) = map f s
t2 : Finset M
ht2 : span R (↑t2 : Set M) = s ⊓ f.ker
g : P → M
hg : ∀ y ∈ t1, g y ∈ s ∧ (f : (a : M) → P) (g y) = y
x : M
hx : x ∈ s
l : P →₀ R
hl1 : Membership.mem (γ := Submodule R (P →₀ R)) (supported R R (↑t1 : Set P)) l
hl2 : Eq.{u_4 + 1} (α := P) ((linearCombination R id : (a : P →₀ R) → P) l : P) ((f : (a : M) → P) x : P)
y : P
hy : y ∈ l.support
⊢ (fun (a : P) (m : R) ↦ m • id (g a)) y ((l : (a : P) → R) y) ∈ s

Tactic:
s.smul_mem _ (hg y (hl1 hy)).1

Premises used: Set.Mem, And.left, Submodule.smul_mem
-- Module: Mathlib.RingTheory.Finiteness.Finsupp
Goal:
R : Type u_1
M : Type u_2
P : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup P
inst_4 : Module R P
f : M →ₗ[R] P
s : Submodule R M
this_1 : DecidableEq R
this_2 : DecidableEq M
this : DecidableEq P
t1 : Finset P
ht1 : span R (↑t1 : Set P) = map f s
t2 : Finset M
ht2 : span R (↑t2 : Set M) = s ⊓ f.ker
g : P → M
hg : ∀ y ∈ t1, g y ∈ s ∧ (f : (a : M) → P) (g y) = y
x : M
hx : x ∈ s
l : P →₀ R
hl1 : Membership.mem (γ := Submodule R (P →₀ R)) (supported R R (↑t1 : Set P)) l
hl2 : Eq.{u_4 + 1} (α := P) ((linearCombination R id : (a : P →₀ R) → P) l : P) ((f : (a : M) → P) x : P)
y : P
hy : y ∈ l.support
⊢ (fun (a : P) (m : R) ↦ m • id (g a)) y ((l : (a : P) → R) y) ∈ s

Tactic:
exact s.smul_mem _ (hg y (hl1 hy)).1

Premises used: And.left, Submodule.smul_mem
-- Module: Mathlib.RingTheory.Finiteness.Finsupp
Goal:
R : Type u_1
M : Type u_2
P : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup P
inst_4 : Module R P
f : M →ₗ[R] P
s : Submodule R M
this_1 : DecidableEq R
this_2 : DecidableEq M
this : DecidableEq P
t1 : Finset P
ht1 : span R (↑t1 : Set P) = map f s
t2 : Finset M
ht2 : span R (↑t2 : Set M) = s ⊓ f.ker
g : P → M
hg : ∀ y ∈ t1, g y ∈ s ∧ (f : (a : M) → P) (g y) = y
x : M
hx : x ∈ s
l : P →₀ R
hl1 : Membership.mem (γ := Submodule R (P →₀ R)) (supported R R (↑t1 : Set P)) l
hl2 : Eq.{u_4 + 1} (α := P) ((linearCombination R id : (a : P →₀ R) → P) l : P) ((f : (a : M) → P) x : P)
⊢ ∀ (b : M), HSMul.hSMul.{u_1, u_2, u_2} (α := R) 0 (id b) = 0

Tactic:
zero_smul _

Premises used: zero_smul
-- Module: Mathlib.RingTheory.Finiteness.Finsupp
Goal:
R : Type u_1
M : Type u_2
P : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup P
inst_4 : Module R P
f : M →ₗ[R] P
s : Submodule R M
this_1 : DecidableEq R
this_2 : DecidableEq M
this : DecidableEq P
t1 : Finset P
ht1 : span R (↑t1 : Set P) = map f s
t2 : Finset M
ht2 : span R (↑t2 : Set M) = s ⊓ f.ker
g : P → M
hg : ∀ y ∈ t1, g y ∈ s ∧ (f : (a : M) → P) (g y) = y
x : M
hx : x ∈ s
l : P →₀ R
hl1 : Membership.mem (γ := Submodule R (P →₀ R)) (supported R R (↑t1 : Set P)) l
hl2 : Eq.{u_4 + 1} (α := P) ((linearCombination R id : (a : P →₀ R) → P) l : P) ((f : (a : M) → P) x : P)
⊢ ∀ (b : M), HSMul.hSMul.{u_1, u_2, u_2} (α := R) 0 (id b) = 0

Tactic:
exact zero_smul _

Premises used: zero_smul
-- Module: Mathlib.RingTheory.Finiteness.Finsupp
Goal:
R : Type u_1
M : Type u_2
P : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup P
inst_4 : Module R P
f : M →ₗ[R] P
s : Submodule R M
this_1 : DecidableEq R
this_2 : DecidableEq M
this : DecidableEq P
t1 : Finset P
ht1 : span R (↑t1 : Set P) = map f s
t2 : Finset M
ht2 : span R (↑t2 : Set M) = s ⊓ f.ker
g : P → M
hg : ∀ y ∈ t1, g y ∈ s ∧ (f : (a : M) → P) (g y) = y
x : M
hx : x ∈ s
l : P →₀ R
hl1 : Membership.mem (γ := Submodule R (P →₀ R)) (supported R R (↑t1 : Set P)) l
hl2 : Eq.{u_4 + 1} (α := P) ((linearCombination R id : (a : P →₀ R) → P) l : P) ((f : (a : M) → P) x : P)
⊢ ∀ (b : M) (m₁ m₂ : R), (m₁ + m₂) • id b = m₁ • id b + m₂ • id b

Tactic:
fun _ _ _ => add_smul _ _ _

Premises used: id, add_smul
-- Module: Mathlib.RingTheory.Finiteness.Finsupp
Goal:
R : Type u_1
M : Type u_2
P : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup P
inst_4 : Module R P
f : M →ₗ[R] P
s : Submodule R M
this_1 : DecidableEq R
this_2 : DecidableEq M
this : DecidableEq P
t1 : Finset P
ht1 : span R (↑t1 : Set P) = map f s
t2 : Finset M
ht2 : span R (↑t2 : Set M) = s ⊓ f.ker
g : P → M
hg : ∀ y ∈ t1, g y ∈ s ∧ (f : (a : M) → P) (g y) = y
x : M
hx : x ∈ s
l : P →₀ R
hl1 : Membership.mem (γ := Submodule R (P →₀ R)) (supported R R (↑t1 : Set P)) l
hl2 : Eq.{u_4 + 1} (α := P) ((linearCombination R id : (a : P →₀ R) → P) l : P) ((f : (a : M) → P) x : P)
⊢ ∀ (b : M) (m₁ m₂ : R), (m₁ + m₂) • id b = m₁ • id b + m₂ • id b

Tactic:
exact fun _ _ _ => add_smul _ _ _

Premises used: add_smul
-- Module: Mathlib.RingTheory.Finiteness.Finsupp
Goal:
R : Type u_1
M : Type u_2
P : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup P
inst_4 : Module R P
f : M →ₗ[R] P
s : Submodule R M
this_1 : DecidableEq R
this_2 : DecidableEq M
this : DecidableEq P
t1 : Finset P
ht1 : span R (↑t1 : Set P) = map f s
t2 : Finset M
ht2 : span R (↑t2 : Set M) = s ⊓ f.ker
g : P → M
hg : ∀ y ∈ t1, g y ∈ s ∧ (f : (a : M) → P) (g y) = y
x : M
hx : x ∈ s
l : P →₀ R
hl1 : Membership.mem (γ := Submodule R (P →₀ R)) (supported R R (↑t1 : Set P)) l
hl2 : Eq.{u_4 + 1} (α := P) ((linearCombination R id : (a : P →₀ R) → P) l : P) ((f : (a : M) → P) x : P)
a :
  HSub.hSub (α := P) (β := P) ((linearCombination R id : (a : P →₀ R) → P) l : P)
      ((f : (a : M) → P)
          ((linearCombination R id : (a : M →₀ R) → M) ((lmapDomain R R g : (a : P →₀ R) → M →₀ R) l : M →₀ R) : M) :
        P) =
    0
⊢ HSub.hSub (β := M) x
      ((linearCombination R id : (a : M →₀ R) → M) ((lmapDomain R R g : (a : P →₀ R) → M →₀ R) l : M →₀ R) : M) ∈
    f.ker

Tactic:
rw [LinearMap.mem_ker, f.map_sub, ← hl2]

Premises used: LinearMap.mem_ker, LinearMap.map_sub
-- Module: Mathlib.RingTheory.Finiteness.Finsupp
Goal:
R : Type u_1
M : Type u_2
P : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup P
inst_4 : Module R P
f : M →ₗ[R] P
s : Submodule R M
this_1 : DecidableEq R
this_2 : DecidableEq M
this : DecidableEq P
t1 : Finset P
ht1 : span R (↑t1 : Set P) = map f s
t2 : Finset M
ht2 : span R (↑t2 : Set M) = s ⊓ f.ker
g : P → M
hg : ∀ y ∈ t1, g y ∈ s ∧ (f : (a : M) → P) (g y) = y
x : M
hx : x ∈ s
l : P →₀ R
hl1 : Membership.mem (γ := Submodule R (P →₀ R)) (supported R R (↑t1 : Set P)) l
hl2 : Eq.{u_4 + 1} (α := P) ((linearCombination R id : (a : P →₀ R) → P) l : P) ((f : (a : M) → P) x : P)
a :
  HSub.hSub (α := P) (β := P) (l.sum fun (i : P) (a : R) ↦ a • id i : P)
      ((f : (a : M) → P) ((mapDomain g l).sum fun (i : M) (a : R) ↦ a • id i) : P) =
    0
⊢ HSub.hSub (α := P) (β := P) ((linearCombination R id : (a : P →₀ R) → P) l : P)
      ((f : (a : M) → P)
          ((linearCombination R id : (a : M →₀ R) → M) ((lmapDomain R R g : (a : P →₀ R) → M →₀ R) l : M →₀ R) : M) :
        P) =
    0

Tactic:
rw [Finsupp.linearCombination_apply, Finsupp.linearCombination_apply, Finsupp.lmapDomain_apply]

Premises used: Finsupp.linearCombination_apply, Finsupp.lmapDomain_apply
-- Module: Mathlib.RingTheory.Finiteness.Finsupp
Goal:
R : Type u_1
M : Type u_2
P : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup P
inst_4 : Module R P
f : M →ₗ[R] P
s : Submodule R M
this_1 : DecidableEq R
this_2 : DecidableEq M
this : DecidableEq P
t1 : Finset P
ht1 : span R (↑t1 : Set P) = map f s
t2 : Finset M
ht2 : span R (↑t2 : Set M) = s ⊓ f.ker
g : P → M
hg : ∀ y ∈ t1, g y ∈ s ∧ (f : (a : M) → P) (g y) = y
x : M
hx : x ∈ s
l : P →₀ R
hl1 : Membership.mem (γ := Submodule R (P →₀ R)) (supported R R (↑t1 : Set P)) l
hl2 : Eq.{u_4 + 1} (α := P) ((linearCombination R id : (a : P →₀ R) → P) l : P) ((f : (a : M) → P) x : P)
a :
  HSub.hSub (α := P) (∑ a ∈ l.support, HSMul.hSMul.{u_1, u_4, u_4} (α := R) ((l : (a : P) → R) a : R) (id a))
      (∑ x ∈ l.support, (f : (a : M) → P) (HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((l : (a : P) → R) x : R) (id (g x)))) =
    0
a₁ : ∀ (b : M), HSMul.hSMul.{u_1, u_2, u_2} (α := R) 0 (id b) = 0
a₂ : ∀ (b : M) (m₁ m₂ : R), (m₁ + m₂) • id b = m₁ • id b + m₂ • id b
⊢ HSub.hSub (α := P) (β := P) (l.sum fun (i : P) (a : R) ↦ a • id i : P)
      ((f : (a : M) → P) ((mapDomain g l).sum fun (i : M) (a : R) ↦ a • id i) : P) =
    0

Tactic:
rw [Finsupp.sum_mapDomain_index, Finsupp.sum, Finsupp.sum, map_sum]

Premises used: Finsupp.sum, Finsupp.sum_mapDomain_index, map_sum
-- Module: Mathlib.RingTheory.Finiteness.Finsupp
Goal:
R : Type u_1
M : Type u_2
P : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup P
inst_4 : Module R P
f : M →ₗ[R] P
s : Submodule R M
this_1 : DecidableEq R
this_2 : DecidableEq M
this : DecidableEq P
t1 : Finset P
ht1 : span R (↑t1 : Set P) = map f s
t2 : Finset M
ht2 : span R (↑t2 : Set M) = s ⊓ f.ker
g : P → M
hg : ∀ y ∈ t1, g y ∈ s ∧ (f : (a : M) → P) (g y) = y
x : M
hx : x ∈ s
l : P →₀ R
hl1 : Membership.mem (γ := Submodule R (P →₀ R)) (supported R R (↑t1 : Set P)) l
hl2 : Eq.{u_4 + 1} (α := P) ((linearCombination R id : (a : P →₀ R) → P) l : P) ((f : (a : M) → P) x : P)
a :
  Eq (α := P) (∑ a ∈ l.support, HSMul.hSMul.{u_1, u_4, u_4} (α := R) ((l : (a : P) → R) a : R) (id a))
    (∑ x ∈ l.support, (f : (a : M) → P) (HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((l : (a : P) → R) x : R) (id (g x))))
⊢ HSub.hSub (α := P) (∑ a ∈ l.support, HSMul.hSMul.{u_1, u_4, u_4} (α := R) ((l : (a : P) → R) a : R) (id a))
      (∑ x ∈ l.support, (f : (a : M) → P) (HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((l : (a : P) → R) x : R) (id (g x)))) =
    0

Tactic:
rw [sub_eq_zero]

Premises used: sub_eq_zero
-- Module: Mathlib.RingTheory.Finiteness.Finsupp
Goal:
R : Type u_1
M : Type u_2
P : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup P
inst_4 : Module R P
f : M →ₗ[R] P
s : Submodule R M
this_1 : DecidableEq R
this_2 : DecidableEq M
this : DecidableEq P
t1 : Finset P
ht1 : span R (↑t1 : Set P) = map f s
t2 : Finset M
ht2 : span R (↑t2 : Set M) = s ⊓ f.ker
g : P → M
hg : ∀ y ∈ t1, g y ∈ s ∧ (f : (a : M) → P) (g y) = y
x : M
hx : x ∈ s
l : P →₀ R
hl1 : Membership.mem (γ := Submodule R (P →₀ R)) (supported R R (↑t1 : Set P)) l
hl2 : Eq.{u_4 + 1} (α := P) ((linearCombination R id : (a : P →₀ R) → P) l : P) ((f : (a : M) → P) x : P)
⊢ Eq (α := P) (∑ a ∈ l.support, HSMul.hSMul.{u_1, u_4, u_4} (α := R) ((l : (a : P) → R) a : R) (id a))
    (∑ x ∈ l.support, (f : (a : M) → P) (HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((l : (a : P) → R) x : R) (id (g x))))

Tactic:
Finset.sum_congr rfl fun y hy => ?_

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.RingTheory.Finiteness.Finsupp
Goal:
R : Type u_1
M : Type u_2
P : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup P
inst_4 : Module R P
f : M →ₗ[R] P
s : Submodule R M
this_1 : DecidableEq R
this_2 : DecidableEq M
this : DecidableEq P
t1 : Finset P
ht1 : span R (↑t1 : Set P) = map f s
t2 : Finset M
ht2 : span R (↑t2 : Set M) = s ⊓ f.ker
g : P → M
hg : ∀ y ∈ t1, g y ∈ s ∧ (f : (a : M) → P) (g y) = y
x : M
hx : x ∈ s
l : P →₀ R
hl1 : Membership.mem (γ := Submodule R (P →₀ R)) (supported R R (↑t1 : Set P)) l
hl2 : Eq.{u_4 + 1} (α := P) ((linearCombination R id : (a : P →₀ R) → P) l : P) ((f : (a : M) → P) x : P)
a :
  ∀ (y : P) (hy : y ∈ l.support),
    HSMul.hSMul.{u_1, u_4, u_4} (α := R) ((l : (a : P) → R) y : R) (id y) =
      (f : (a : M) → P) (HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((l : (a : P) → R) y : R) (id (g y)))
⊢ Eq (α := P) (∑ a ∈ l.support, HSMul.hSMul.{u_1, u_4, u_4} (α := R) ((l : (a : P) → R) a : R) (id a))
    (∑ x ∈ l.support, (f : (a : M) → P) (HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((l : (a : P) → R) x : R) (id (g x))))

Tactic:
refine Finset.sum_congr rfl fun y hy => ?_

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.RingTheory.Finiteness.Finsupp
Goal:
R : Type u_1
M : Type u_2
P : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup P
inst_4 : Module R P
f : M →ₗ[R] P
s : Submodule R M
this_1 : DecidableEq R
this_2 : DecidableEq M
this : DecidableEq P
t1 : Finset P
ht1 : span R (↑t1 : Set P) = map f s
t2 : Finset M
ht2 : span R (↑t2 : Set M) = s ⊓ f.ker
g : P → M
hg : ∀ y ∈ t1, g y ∈ s ∧ (f : (a : M) → P) (g y) = y
x : M
hx : x ∈ s
l : P →₀ R
hl1 : Membership.mem (γ := Submodule R (P →₀ R)) (supported R R (↑t1 : Set P)) l
hl2 : Eq.{u_4 + 1} (α := P) ((linearCombination R id : (a : P →₀ R) → P) l : P) ((f : (a : M) → P) x : P)
y : P
hy : y ∈ l.support
a :
  HSMul.hSMul.{u_1, u_4, u_4} (α := R) ((l : (a : P) → R) y : R) y =
    (f : (a : M) → P) (HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((l : (a : P) → R) y : R) (g y))
⊢ HSMul.hSMul.{u_1, u_4, u_4} (α := R) ((l : (a : P) → R) y : R) (id y) =
    (f : (a : M) → P) (HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((l : (a : P) → R) y : R) (id (g y)))

Tactic:
unfold id

Premises used: id
-- Module: Mathlib.RingTheory.Finiteness.Finsupp
Goal:
R : Type u_1
M : Type u_2
P : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup P
inst_4 : Module R P
f : M →ₗ[R] P
s : Submodule R M
this_1 : DecidableEq R
this_2 : DecidableEq M
this : DecidableEq P
t1 : Finset P
ht1 : span R (↑t1 : Set P) = map f s
t2 : Finset M
ht2 : span R (↑t2 : Set M) = s ⊓ f.ker
g : P → M
hg : ∀ y ∈ t1, g y ∈ s ∧ (f : (a : M) → P) (g y) = y
x : M
hx : x ∈ s
l : P →₀ R
hl1 : Membership.mem (γ := Submodule R (P →₀ R)) (supported R R (↑t1 : Set P)) l
hl2 : Eq.{u_4 + 1} (α := P) ((linearCombination R id : (a : P →₀ R) → P) l : P) ((f : (a : M) → P) x : P)
y : P
hy : y ∈ l.support
a :
  HSMul.hSMul.{u_1, u_4, u_4} (α := R) ((l : (a : P) → R) y : R) y =
    HSMul.hSMul.{u_1, u_4, u_4} (α := R) (β := P) ((l : (a : P) → R) y : R) ((f : (a : M) → P) (g y) : P)
a₁ a₂ :
  HSMul.hSMul.{u_1, u_4, u_4} (α := R) ((l : (a : P) → R) y : R) y =
    HSMul.hSMul.{u_1, u_4, u_4} (α := R) ((l : (a : P) → R) y : R) y
⊢ HSMul.hSMul.{u_1, u_4, u_4} (α := R) ((l : (a : P) → R) y : R) y =
    (f : (a : M) → P) (HSMul.hSMul.{u_1, u_2, u_2} (α := R) ((l : (a : P) → R) y : R) (g y))

Tactic:
rw [f.map_smul, (hg y (hl1 hy)).2]

Premises used: And.right, LinearMap.map_smul
-- Module: Mathlib.RingTheory.Finiteness.Finsupp
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : AddCommGroup P
inst_6 : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
hf1 : f.ker.FG
hf2 : g.ker.FG
hsur : Surjective.{u_2 + 1, u_3 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
rw : (comap f g.ker).FG
⊢ (g ∘ₗ f).ker.FG

Tactic:
rw [LinearMap.ker_comp]

Premises used: LinearMap.ker_comp
-- Module: Mathlib.RingTheory.Finiteness.Finsupp
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : AddCommGroup P
inst_6 : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
hf1 : f.ker.FG
hf2 : g.ker.FG
hsur : Surjective.{u_2 + 1, u_3 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
hs1 : (map f (comap f g.ker)).FG
hs2 : (comap f g.ker ⊓ f.ker).FG
⊢ (comap f g.ker).FG

Tactic:
apply fg_of_fg_map_of_fg_inf_ker f

Premises used: Submodule.fg_of_fg_map_of_fg_inf_ker
-- Module: Mathlib.RingTheory.Finiteness.Finsupp
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : AddCommGroup P
inst_6 : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
hf1 : f.ker.FG
hf2 : g.ker.FG
hsur : Surjective.{u_2 + 1, u_3 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
hs1 : (f.range ⊓ g.ker).FG
hs1₁ : (⊤ ⊓ g.ker).FG
hs1₂ hs1₃ hs1₄ hs1₅ : g.ker.FG
⊢ (map f (comap f g.ker)).FG

Tactic:
rwa [Submodule.map_comap_eq, LinearMap.range_eq_top.2 hsur, top_inf_eq]

Premises used: Iff.mpr, Submodule.map_comap_eq, top_inf_eq, LinearMap.range_eq_top
-- Module: Mathlib.RingTheory.Finiteness.Finsupp
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : AddCommGroup P
inst_6 : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
hf1 : f.ker.FG
hf2 : g.ker.FG
hsur : Surjective.{u_2 + 1, u_3 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
hs2 hs2₁ hs2₂ hs2₃ : f.ker.FG
⊢ (comap f g.ker ⊓ f.ker).FG

Tactic:
rwa [inf_of_le_right (show (LinearMap.ker f) ≤
      (LinearMap.ker g).comap f from comap_mono bot_le)]

Premises used: Submodule.comap_mono, inf_of_le_right, bot_le
-- Module: Mathlib.RingTheory.Finiteness.Finsupp
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : AddCommGroup P
inst_6 : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
h_exact : Function.Exact.{u_2, u_3, u_4} (M := M) (N := N) (P := P) (⇑f : (a : M) → N) (⇑g : (a : N) → P)
h_surj : Surjective.{u_3 + 1, u_4 + 1} (α := N) (β := P) (⇑g : (a : N) → P)
inst_7 : Module.Finite R M
inst_8 : Module.Finite R P
⊢ Module.Finite R N

Tactic:
⟨(⊤ : Submodule R _).fg_of_fg_map_of_fg_inf_ker g ?_ ?_⟩

Premises used: Module.Finite.of_fg_top, Submodule.fg_of_fg_map_of_fg_inf_ker
-- Module: Mathlib.RingTheory.Finiteness.Finsupp
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : AddCommGroup P
inst_6 : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
h_exact : Function.Exact.{u_2, u_3, u_4} (M := M) (N := N) (P := P) (⇑f : (a : M) → N) (⇑g : (a : N) → P)
h_surj : Surjective.{u_3 + 1, u_4 + 1} (α := N) (β := P) (⇑g : (a : N) → P)
inst_7 : Module.Finite R M
inst_8 : Module.Finite R P
refine_1 : (map g ⊤).FG
refine_2 : (⊤ ⊓ g.ker).FG
⊢ Module.Finite R N

Tactic:
refine ⟨(⊤ : Submodule R _).fg_of_fg_map_of_fg_inf_ker g ?_ ?_⟩
-- Module: Mathlib.RingTheory.Finiteness.Finsupp
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : AddCommGroup P
inst_6 : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
h_exact : Function.Exact.{u_2, u_3, u_4} (M := M) (N := N) (P := P) (⇑f : (a : M) → N) (⇑g : (a : N) → P)
h_surj : Surjective.{u_3 + 1, u_4 + 1} (α := N) (β := P) (⇑g : (a : N) → P)
inst_7 : Module.Finite R M
inst_8 : Module.Finite R P
⊢ g.range = ⊤

Tactic:
rw [← LinearMap.range_eq_top] at h_surj

Premises used: LinearMap.range_eq_top
-- Module: Mathlib.RingTheory.Finiteness.Finsupp
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : AddCommGroup P
inst_6 : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
h_exact : Function.Exact.{u_2, u_3, u_4} (M := M) (N := N) (P := P) (⇑f : (a : M) → N) (⇑g : (a : N) → P)
h_surj : Surjective.{u_3 + 1, u_4 + 1} (α := N) (β := P) (⇑g : (a : N) → P)
inst_7 : Module.Finite R M
inst_8 : Module.Finite R P
h_surj₁ : g.range = ⊤
⊢ Module.Finite R M

Tactic:
rw [← LinearMap.range_eq_top] at h_surj

Premises used: LinearMap.range_eq_top
-- Module: Mathlib.RingTheory.Finiteness.Finsupp
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst_1 : Ring R
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : AddCommGroup N
inst_5 : Module R N
inst_6 : AddCommGroup P
inst_7 : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
h_exact : Function.Exact.{u_2, u_3, u_4} (M := M) (N := N) (P := P) (⇑f : (a : M) → N) (⇑g : (a : N) → P)
h_surj : Surjective.{u_3 + 1, u_4 + 1} (α := N) (β := P) (⇑g : (a : N) → P)
inst_8 : Module.Finite R M
inst_9 : Module.Finite R P
h_surj₁ : g.range = ⊤
inst : Module.Finite R M
⊢ Module.Finite R P

Tactic:
rw [← LinearMap.range_eq_top] at h_surj

Premises used: LinearMap.range_eq_top
-- Module: Mathlib.RingTheory.Finiteness.Finsupp
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : AddCommGroup P
inst_6 : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
h_exact : Function.Exact.{u_2, u_3, u_4} (M := M) (N := N) (P := P) (⇑f : (a : M) → N) (⇑g : (a : N) → P)
h_surj : g.range = ⊤
inst_7 : Module.Finite R M
inst_8 : Module.Finite R P
refine_1 : FG.{u_1, u_4} (R := R) (M := P) ⊤
⊢ (map g ⊤).FG

Tactic:
rw [Submodule.map_top, h_surj]

Premises used: Submodule.map_top
-- Module: Mathlib.RingTheory.Finiteness.Finsupp
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : AddCommGroup P
inst_6 : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
h_exact : Function.Exact.{u_2, u_3, u_4} (M := M) (N := N) (P := P) (⇑f : (a : M) → N) (⇑g : (a : N) → P)
h_surj : g.range = ⊤
inst_7 : Module.Finite R M
inst_8 : Module.Finite R P
⊢ FG.{u_1, u_4} (R := R) (M := P) ⊤

Tactic:
Module.Finite.fg_top

Premises used: Module.Finite.fg_top
-- Module: Mathlib.RingTheory.Finiteness.Finsupp
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : AddCommGroup P
inst_6 : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
h_exact : Function.Exact.{u_2, u_3, u_4} (M := M) (N := N) (P := P) (⇑f : (a : M) → N) (⇑g : (a : N) → P)
h_surj : g.range = ⊤
inst_7 : Module.Finite R M
inst_8 : Module.Finite R P
⊢ FG.{u_1, u_4} (R := R) (M := P) ⊤

Tactic:
exact Module.Finite.fg_top

Premises used: Module.Finite.fg_top
-- Module: Mathlib.RingTheory.Finiteness.Finsupp
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : AddCommGroup P
inst_6 : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
h_exact : Function.Exact.{u_2, u_3, u_4} (M := M) (N := N) (P := P) (⇑f : (a : M) → N) (⇑g : (a : N) → P)
h_surj : Surjective.{u_3 + 1, u_4 + 1} (α := N) (β := P) (⇑g : (a : N) → P)
inst_7 : Module.Finite R M
inst_8 : Module.Finite R P
⊢ (⊤ ⊓ g.ker).FG

Tactic:
simp [LinearMap.exact_iff.1 h_exact]

Premises used: Iff.mp, LinearMap.exact_iff
-- Module: Mathlib.RingTheory.Finiteness.Finsupp
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Submodule R M
inst_3 : Module.Finite.{u_1, u_2} R ↥N
inst_4 : Module.Finite.{u_1, u_2} R (M ⧸ N)
⊢ Module.Finite R M

Tactic:
.of_exact (LinearMap.exact_subtype_mkQ N) (Quotient.mk_surjective _)

Premises used: LinearMap.exact_subtype_mkQ, Submodule.Quotient.mk_surjective, Module.Finite.of_exact
-- Module: Mathlib.RingTheory.Finiteness.Finsupp
Goal:
R : Type u_2
V : Type u_3
inst : Semiring R
inst_1 : AddCommMonoid V
inst_2 : Module R V
ι : Type u_1
inst_3 : Finite ι
inst_4 : Module.Finite R V
⊢ Module.Finite R (ι →₀ V)

Tactic:
Module.Finite.equiv (Finsupp.linearEquivFunOnFinite R V ι).symm

Premises used: LinearEquiv.symm, Finsupp.linearEquivFunOnFinite, Module.Finite.equiv
-- Module: Mathlib.RingTheory.Finiteness.Finsupp
Goal:
M : Type u_1
R : Type u_2
S : Type u_3
inst : Finite M
inst_1 : Semiring R
inst_2 : Semiring S
inst_3 : Module R S
inst_4 : Module.Finite R S
⊢ Module.Finite R S[M]

Tactic:
.finsupp

Premises used: AddMonoidAlgebra, Module.Finite.finsupp