awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Module.Presentation.DirectSum
Goal:
A : Type u
inst : Ring A
ι : Type w
inst_1 : DecidableEq ι
relations : ι → Relations.{w₀, w₁, u} A
M : ι → Type v
inst_2 : (i : ι) → AddCommGroup (M i)
inst_3 : (i : ι) → Module.{u, v} A (M i)
N : Type v
inst_4 : AddCommGroup N
inst_5 : Module A N
solution : (i : ι) → Solution.{w₀, w₁, v, u} (relations i) (M i)
h : ∀ (i : ι), (solution i).IsPresentation
N_1 : Type w'
inst_6 : AddCommGroup N_1
inst_7 : Module A N_1
f f' : (⨁ (i : ι), M i) →ₗ[A] N_1
h' : (directSum (M := M) solution).postcomp f = (directSum (M := M) solution).postcomp f'
i : ι
g : (relations i).G
⊢ ((solution i).postcomp (f ∘ₗ lof A ι M i)).var g = ((solution i).postcomp (f' ∘ₗ lof A ι M i)).var g

Tactic:
exact Solution.congr_var h' ⟨i, g⟩

Premises used: Sigma.mk, Module.Relations.Solution.congr_var
-- Module: Mathlib.Algebra.Module.Presentation.DirectSum
Goal:
A : Type u
inst : Ring A
ι : Type w
inst_1 : DecidableEq ι
relations : ι → Relations.{w₀, w₁, u} A
M : ι → Type v
inst_2 : (i : ι) → AddCommGroup (M i)
inst_3 : (i : ι) → Module.{u, v} A (M i)
solution : (i : ι) → Solution.{w₀, w₁, v, u} (relations i) (M i)
h : ∀ (i : ι), (solution i).IsPresentation
⊢ (Solution.directSum (M := M) solution).IsPresentation

Tactic:
(directSum.isRepresentationCore h).isPresentation

Premises used: Module.Relations.Solution.IsPresentation.directSum.isRepresentationCore, Module.Relations.Solution.IsPresentationCore.isPresentation
-- Module: Mathlib.Algebra.Module.Presentation.DirectSum
Goal:
A : Type u
inst : Ring A
ι : Type w
inst_1 : DecidableEq ι
M : ι → Type v
inst_2 : (i : ι) → AddCommGroup (M i)
inst_3 : (i : ι) → Module.{u, v} A (M i)
pres : (i : ι) → Presentation.{u_1, u_2, v, u} A (M i)
i : ι
g : (pres i).G
⊢ (directSum (M := M) pres).var
      (Sigma.mk (β := fun (i : ι) ↦ Relations.G.{u_1, u_2, u} (A := A) ((fun (i : ι) ↦ (pres i).toRelations) i)) i g) =
    (lof A ι M i : (a : M i) → ⨁ (i : ι), M i) ((pres i).var g)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Module.Presentation.DirectSum
Goal:
A : Type u
inst : Ring A
N : Type v
inst_1 : AddCommGroup N
inst_2 : Module A N
pres : Presentation.{u_1, u_2, v, u} A N
ι : Type w
inst_3 : DecidableEq ι
inst_4 : DecidableEq N
i : ι
g : pres.G
a :
  Eq (α := Π₀ (x : ι), N)
    ((finsuppLequivDFinsupp A : (a : ι →₀ N) → Π₀ (x : ι), N)
        ((pres.finsupp ι).var
          (Sigma.mk (β := fun (i : ι) ↦
            Relations.G.{u_1, u_2, u} (A := A)
              ((fun (i : ι) ↦
                  (toRelations.{u_1, u_2, v, u} (M := (fun (x : ι) ↦ N) i) ((fun (x : ι) ↦ pres) i) :
                    Relations.{u_1, u_2, u} A))
                i))
            i g)) :
      Π₀ (x : ι), N)
    ((finsuppLequivDFinsupp A : (a : ι →₀ N) → Π₀ (x : ι), N) (Finsupp.single i (pres.var g)) : Π₀ (x : ι), N)
⊢ (pres.finsupp ι).var
      (Sigma.mk (β := fun (i : ι) ↦
        Relations.G.{u_1, u_2, u} (A := A)
          ((fun (i : ι) ↦
              (toRelations.{u_1, u_2, v, u} (M := (fun (x : ι) ↦ N) i) ((fun (x : ι) ↦ pres) i) :
                Relations.{u_1, u_2, u} A))
            i))
        i g) =
    Finsupp.single i (pres.var g)

Tactic:
apply (finsuppLequivDFinsupp A).injective

Premises used: finsuppLequivDFinsupp, LinearEquiv.injective
-- Module: Mathlib.Algebra.Module.Presentation.DirectSum
Goal:
A : Type u
inst : Ring A
N : Type v
inst_1 : AddCommGroup N
inst_2 : Module A N
pres : Presentation.{u_1, u_2, v, u} A N
ι : Type w
inst_3 : DecidableEq ι
inst_4 : DecidableEq N
i : ι
g : pres.G
a :
  Eq (α := Π₀ (x : ι), N)
    (Relations.Solution.var (A := A) (relations :=
      toRelations (M := ⨁ (i : ι), N) (directSum.{w, v, u, u_1, u_2} (M := fun (x : ι) ↦ N) fun (x : ι) ↦ pres))
      (toSolution (directSum.{w, v, u, u_1, u_2} (M := fun (x : ι) ↦ N) fun (x : ι) ↦ pres))
      (Sigma.mk (β := fun (i : ι) ↦
        Relations.G.{u_1, u_2, u} (A := A)
          ((fun (i : ι) ↦
              (toRelations.{u_1, u_2, v, u} (M := (fun (x : ι) ↦ N) i) ((fun (x : ι) ↦ pres) i) :
                Relations.{u_1, u_2, u} A))
            i))
        i g))
    ((finsuppLequivDFinsupp A : (a : ι →₀ N) → Π₀ (x : ι), N) (Finsupp.single i (pres.var g)))
⊢ Eq (α := Π₀ (x : ι), N)
    ((finsuppLequivDFinsupp A : (a : ι →₀ N) → Π₀ (x : ι), N)
        ((pres.finsupp ι).var
          (Sigma.mk (β := fun (i : ι) ↦
            Relations.G.{u_1, u_2, u} (A := A)
              ((fun (i : ι) ↦
                  (toRelations.{u_1, u_2, v, u} (M := (fun (x : ι) ↦ N) i) ((fun (x : ι) ↦ pres) i) :
                    Relations.{u_1, u_2, u} A))
                i))
            i g)) :
      Π₀ (x : ι), N)
    ((finsuppLequivDFinsupp A : (a : ι →₀ N) → Π₀ (x : ι), N) (Finsupp.single i (pres.var g)) : Π₀ (x : ι), N)

Tactic:
erw [(finsuppLequivDFinsupp A).apply_symm_apply]

Premises used: finsuppLequivDFinsupp, LinearEquiv.apply_symm_apply
-- Module: Mathlib.Algebra.Module.Presentation.DirectSum
Goal:
A : Type u
inst : Ring A
N : Type v
inst_1 : AddCommGroup N
inst_2 : Module A N
pres : Presentation.{u_1, u_2, v, u} A N
ι : Type w
inst_3 : DecidableEq ι
inst_4 : DecidableEq N
i : ι
g : pres.G
a :
  Eq (α := Π₀ (x : ι), N)
    (((lof.{u, w, v} A ι (fun (x : ι) ↦ N) i : N →ₗ[A] ⨁ (i : ι), N) : (a : N) → ⨁ (i : ι), N) (pres.var g) :
      ⨁ (i : ι), N)
    (DFinsupp.single (β := fun (i : ι) ↦ N) i (pres.var g) : Π₀ (i : ι), N)
⊢ Eq (α := Π₀ (x : ι), N)
    (Relations.Solution.var (A := A) (relations :=
      toRelations (M := ⨁ (i : ι), N) (directSum.{w, v, u, u_1, u_2} (M := fun (x : ι) ↦ N) fun (x : ι) ↦ pres))
      (toSolution (directSum.{w, v, u, u_1, u_2} (M := fun (x : ι) ↦ N) fun (x : ι) ↦ pres))
      (Sigma.mk (β := fun (i : ι) ↦
        Relations.G.{u_1, u_2, u} (A := A)
          ((fun (i : ι) ↦
              (toRelations.{u_1, u_2, v, u} (M := (fun (x : ι) ↦ N) i) ((fun (x : ι) ↦ pres) i) :
                Relations.{u_1, u_2, u} A))
            i))
        i g))
    ((finsuppLequivDFinsupp A : (a : ι →₀ N) → Π₀ (x : ι), N) (Finsupp.single i (pres.var g)))

Tactic:
rw [directSum_var, finsuppLequivDFinsupp_apply_apply, Finsupp.toDFinsupp_single]

Premises used: Module.Presentation.directSum_var, finsuppLequivDFinsupp_apply_apply, Finsupp.toDFinsupp_single
-- Module: Mathlib.Algebra.Module.Presentation.DirectSum
Goal:
A : Type u
inst : Ring A
N : Type v
inst_1 : AddCommGroup N
inst_2 : Module A N
pres : Presentation.{u_1, u_2, v, u} A N
ι : Type w
inst_3 : DecidableEq ι
inst_4 : DecidableEq N
i : ι
g : pres.G
⊢ Eq (α := Π₀ (x : ι), N)
    (((lof.{u, w, v} A ι (fun (x : ι) ↦ N) i : N →ₗ[A] ⨁ (i : ι), N) : (a : N) → ⨁ (i : ι), N) (pres.var g) :
      ⨁ (i : ι), N)
    (DFinsupp.single (β := fun (i : ι) ↦ N) i (pres.var g) : Π₀ (i : ι), N)

Tactic:
rfl
-- Module: Mathlib.Algebra.Module.Presentation.Finite
Goal:
A : Type u
inst : Ring A
M : Type v
inst_1 : AddCommGroup M
inst_2 : Module A M
pres : Presentation.{u_1, u_2, v, u} A M
inst_3 : Finite.{u_1 + 1} pres.G
⊢ Module.Finite A M

Tactic:
Finite.of_surjective _ pres.surjective_π

Premises used: Module.Finite.of_surjective, Module.Presentation.toIsPresentation, Module.Relations.Solution.IsPresentation.surjective_π
-- Module: Mathlib.Algebra.Module.Presentation.Finite
Goal:
A : Type u
inst : Ring A
M : Type v
inst_1 : AddCommGroup M
inst_2 : Module A M
pres : Presentation.{u_1, u_2, v, u} A M
inst_3 : Finite.{u_1 + 1} pres.G
inst_4 : Finite.{u_2 + 1} pres.R
rw : Submodule.FG (Submodule.span A (Set.range pres.relation))
⊢ pres.π.ker.FG

Tactic:
rw [pres.ker_π]

Premises used: Module.Presentation.toIsPresentation, Module.Relations.Solution.IsPresentation.ker_π
-- Module: Mathlib.Algebra.Module.Presentation.Finite
Goal:
A : Type u
inst : Ring A
M : Type v
inst_1 : AddCommGroup M
inst_2 : Module A M
pres : Presentation.{u_1, u_2, v, u} A M
inst_3 : Finite.{u_1 + 1} pres.G
inst_4 : Finite.{u_2 + 1} pres.R
⊢ Submodule.FG (Submodule.span A (Set.range pres.relation))

Tactic:
Submodule.fg_span (Set.finite_range _)

Premises used: Set.finite_range, Submodule.fg_span
-- Module: Mathlib.Algebra.Module.Presentation.Finite
Goal:
A : Type u
inst : Ring A
M : Type v
inst_1 : AddCommGroup M
inst_2 : Module A M
pres : Presentation.{u_1, u_2, v, u} A M
inst_3 : Finite.{u_1 + 1} pres.G
inst_4 : Finite.{u_2 + 1} pres.R
⊢ Submodule.FG (Submodule.span A (Set.range pres.relation))

Tactic:
exact Submodule.fg_span (Set.finite_range _)

Premises used: Set.finite_range, Submodule.fg_span
-- Module: Mathlib.Algebra.Module.Presentation.Finite
Goal:
A : Type u
inst : Ring A
M : Type v
inst_1 : AddCommGroup M
inst_2 : Module A M
mp :
  FinitePresentation A M → ∃ (pres : Presentation.{w₀, w₁, v, u} A M), Finite.{w₀ + 1} pres.G ∧ Finite.{w₁ + 1} pres.R
mpr :
  (∃ (pres : Presentation.{w₀, w₁, v, u} A M), Finite.{w₀ + 1} pres.G ∧ Finite.{w₁ + 1} pres.R) → FinitePresentation A M
⊢ FinitePresentation A M ↔ ∃ (pres : Presentation.{w₀, w₁, v, u} A M), Finite.{w₀ + 1} pres.G ∧ Finite.{w₁ + 1} pres.R

Tactic:
constructor
-- Module: Mathlib.Algebra.Module.Presentation.Finite
Goal:
A : Type u
inst : Ring A
M : Type v
inst_1 : AddCommGroup M
inst_2 : Module A M
h : FinitePresentation A M
mp :
  ∀ (G : Type w₀),
    Finite G →
      ∀ (var : G → M) (hG : Eq (α := Submodule A M) (Submodule.span A (Set.range var)) ⊤),
        ∃ (pres : Presentation.{w₀, w₁, v, u} A M), Finite.{w₀ + 1} pres.G ∧ Finite.{w₁ + 1} pres.R
⊢ ∃ (pres : Presentation.{w₀, w₁, v, u} A M), Finite.{w₀ + 1} pres.G ∧ Finite.{w₁ + 1} pres.R

Tactic:
obtain ⟨G : Type w₀, _, var, hG⟩ :=
      Submodule.fg_iff_exists_finite_generating_family.1
        (finite_def.1 (inferInstance : Module.Finite A M))

Premises used: Submodule.fg_iff_exists_finite_generating_family, inferInstance, Module.finite_def, Iff.mp
-- Module: Mathlib.Algebra.Module.Presentation.Finite
Goal:
A : Type u
inst : Ring A
M : Type v
inst_1 : AddCommGroup M
inst_2 : Module A M
h : FinitePresentation A M
G : Type w₀
w : Finite G
var : G → M
hG : Eq (α := Submodule A M) (Submodule.span A (Set.range var)) ⊤
rw : Eq (α := Submodule A M) (LinearMap.range (Finsupp.linearCombination A var)) ⊤
rw₁ : Eq (α := Submodule A M) (Submodule.span A (Set.range var)) ⊤
rw₂ rw₃ : Eq.{v + 1} (α := Submodule A M) ⊤ ⊤
⊢ Function.Surjective (α := G →₀ A) (β := M) (⇑(Finsupp.linearCombination A var) : (a : G →₀ A) → M)

Tactic:
rw [← LinearMap.range_eq_top, Finsupp.range_linearCombination, hG]

Premises used: LinearMap.range_eq_top, Finsupp.range_linearCombination
-- Module: Mathlib.Algebra.Module.Presentation.Finite
Goal:
A : Type u
inst : Ring A
M : Type v
inst_1 : AddCommGroup M
inst_2 : Module A M
h : FinitePresentation A M
G : Type w₀
w : Finite G
var : G → M
hG : Eq (α := Submodule A M) (Submodule.span A (Set.range var)) ⊤
mp :
  ∀ (R : Type w₁),
    Finite R →
      ∀ (relation : R → G →₀ A)
        (hR : Submodule.span A (Set.range relation) = LinearMap.ker (Finsupp.linearCombination A var)),
        ∃ (pres : Presentation.{w₀, w₁, v, u} A M), Finite.{w₀ + 1} pres.G ∧ Finite.{w₁ + 1} pres.R
⊢ ∃ (pres : Presentation.{w₀, w₁, v, u} A M), Finite.{w₀ + 1} pres.G ∧ Finite.{w₁ + 1} pres.R

Tactic:
obtain ⟨R : Type w₁, _, relation, hR⟩ :=
      Submodule.fg_iff_exists_finite_generating_family.1
        (Module.FinitePresentation.fg_ker (Finsupp.linearCombination A var) (by
          rw [← LinearMap.range_eq_top, Finsupp.range_linearCombination, hG]))

Premises used: Module.FinitePresentation.fg_ker, Submodule.fg_iff_exists_finite_generating_family, Iff.mp, Finsupp.linearCombination
-- Module: Mathlib.Algebra.Module.Presentation.Finite
Goal:
A : Type u
inst : Ring A
M : Type v
inst_1 : AddCommGroup M
inst_2 : Module A M
h : FinitePresentation A M
G : Type w₀
w : Finite G
var : G → M
hG : Eq (α := Submodule A M) (Submodule.span A (Set.range var)) ⊤
R : Type w₁
w_1 : Finite R
relation : R → G →₀ A
hR : Submodule.span A (Set.range relation) = LinearMap.ker (Finsupp.linearCombination A var)
r : R
rw :
  ∀
    (hR :
      ∀ (x : G →₀ A),
        Membership.mem (γ := Submodule A (G →₀ A)) (Submodule.span A (Set.range relation)) x ↔
          Membership.mem (γ := Submodule A (G →₀ A)) (LinearMap.ker (Finsupp.linearCombination A var)) x)
    (r : R), Eq.{v + 1} (α := M) ((Finsupp.linearCombination A var : (a : G →₀ A) → M) (relation r) : M) (0 : M)
⊢ Eq.{v + 1} (α := M) ((Finsupp.linearCombination A var : (a : G →₀ A) → M) (relation r) : M) (0 : M)

Tactic:
rw [Submodule.ext_iff] at hR

Premises used: Submodule.ext_iff
-- Module: Mathlib.Algebra.Module.Presentation.Finite
Goal:
A : Type u
inst : Ring A
M : Type v
inst_1 : AddCommGroup M
inst_2 : Module A M
h : FinitePresentation A M
G : Type w₀
w : Finite G
var : G → M
hG : Eq (α := Submodule A M) (Submodule.span A (Set.range var)) ⊤
R : Type w₁
w_1 : Finite R
relation : R → G →₀ A
hR :
  ∀ (x : G →₀ A),
    Membership.mem (γ := Submodule A (G →₀ A)) (Submodule.span A (Set.range relation)) x ↔
      Membership.mem (γ := Submodule A (G →₀ A)) (LinearMap.ker (Finsupp.linearCombination A var)) x
r : R
⊢ Eq.{v + 1} (α := M) ((Finsupp.linearCombination A var : (a : G →₀ A) → M) (relation r) : M) (0 : M)

Tactic:
(hR _).1 (Submodule.subset_span ⟨_, rfl⟩)

Premises used: Set.Mem, setOf, Set.preimage, Set.singleton, Exists.intro, Iff.mp, Submodule.subset_span, rfl
-- Module: Mathlib.Algebra.Module.Presentation.Finite
Goal:
A : Type u
inst : Ring A
M : Type v
inst_1 : AddCommGroup M
inst_2 : Module A M
h : FinitePresentation A M
G : Type w₀
w : Finite G
var : G → M
hG : Eq (α := Submodule A M) (Submodule.span A (Set.range var)) ⊤
R : Type w₁
w_1 : Finite R
relation : R → G →₀ A
hR :
  ∀ (x : G →₀ A),
    Membership.mem (γ := Submodule A (G →₀ A)) (Submodule.span A (Set.range relation)) x ↔
      Membership.mem (γ := Submodule A (G →₀ A)) (LinearMap.ker (Finsupp.linearCombination A var)) x
r : R
⊢ Eq.{v + 1} (α := M) ((Finsupp.linearCombination A var : (a : G →₀ A) → M) (relation r) : M) (0 : M)

Tactic:
exact (hR _).1 (Submodule.subset_span ⟨_, rfl⟩)

Premises used: Exists.intro, Iff.mp, Submodule.subset_span, rfl
-- Module: Mathlib.Algebra.Module.Presentation.Finite
Goal:
A : Type u
inst : Ring A
M : Type v
inst_1 : AddCommGroup M
inst_2 : Module A M
h : FinitePresentation A M
G : Type w₀
w : Finite G
var : G → M
hG : Eq (α := Submodule A M) (Submodule.span A (Set.range var)) ⊤
R : Type w₁
w_1 : Finite R
relation : R → G →₀ A
hR : Submodule.span A (Set.range relation) = LinearMap.ker (Finsupp.linearCombination A var)
rw :
  Eq.{v + 1} (α := Submodule A M)
      (Submodule.span A
        (Set.range.{v, w₀ + 1} (ι := { G := G, R := R, relation := relation : Relations.{w₀, w₁, u} A }.G)
          (Relations.Solution.var { var := var, linearCombination_var_relation := ⋯ })))
      ⊤ ∧
    LinearMap.ker (M₂ := M) (Relations.Solution.π { var := var, linearCombination_var_relation := ⋯ }) =
      Submodule.span A (Set.range { G := G, R := R, relation := relation : Relations.{w₀, w₁, u} A }.relation)
⊢ Relations.Solution.IsPresentation.{w₀, w₁, v, u} (A := A) (relations := { G := G, R := R, relation := relation })
    (M := M) { var := var, linearCombination_var_relation := ⋯ }

Tactic:
rw [Relations.Solution.isPresentation_iff]

Premises used: Module.Relations.Solution.isPresentation_iff
-- Module: Mathlib.Algebra.Module.Presentation.Finite
Goal:
A : Type u
inst : Ring A
M : Type v
inst_1 : AddCommGroup M
inst_2 : Module A M
h : FinitePresentation A M
G : Type w₀
w : Finite G
var : G → M
hG : Eq (α := Submodule A M) (Submodule.span A (Set.range var)) ⊤
R : Type w₁
w_1 : Finite R
relation : R → G →₀ A
hR : Submodule.span A (Set.range relation) = LinearMap.ker (Finsupp.linearCombination A var)
⊢ Eq.{v + 1} (α := Submodule A M)
      (Submodule.span A
        (Set.range.{v, w₀ + 1} (ι := { G := G, R := R, relation := relation : Relations.{w₀, w₁, u} A }.G)
          (Relations.Solution.var { var := var, linearCombination_var_relation := ⋯ })))
      ⊤ ∧
    LinearMap.ker (M₂ := M) (Relations.Solution.π { var := var, linearCombination_var_relation := ⋯ }) =
      Submodule.span A (Set.range { G := G, R := R, relation := relation : Relations.{w₀, w₁, u} A }.relation)

Tactic:
⟨hG, hR.symm⟩

Premises used: And.intro, Eq.symm
-- Module: Mathlib.Algebra.Module.Presentation.Finite
Goal:
A : Type u
inst : Ring A
M : Type v
inst_1 : AddCommGroup M
inst_2 : Module A M
h : FinitePresentation A M
G : Type w₀
w : Finite G
var : G → M
hG : Eq (α := Submodule A M) (Submodule.span A (Set.range var)) ⊤
R : Type w₁
w_1 : Finite R
relation : R → G →₀ A
hR : Submodule.span A (Set.range relation) = LinearMap.ker (Finsupp.linearCombination A var)
⊢ Eq.{v + 1} (α := Submodule A M)
      (Submodule.span A
        (Set.range.{v, w₀ + 1} (ι := { G := G, R := R, relation := relation : Relations.{w₀, w₁, u} A }.G)
          (Relations.Solution.var { var := var, linearCombination_var_relation := ⋯ })))
      ⊤ ∧
    LinearMap.ker (M₂ := M) (Relations.Solution.π { var := var, linearCombination_var_relation := ⋯ }) =
      Submodule.span A (Set.range { G := G, R := R, relation := relation : Relations.{w₀, w₁, u} A }.relation)

Tactic:
exact ⟨hG, hR.symm⟩
-- Module: Mathlib.Algebra.Module.Presentation.Finite
Goal:
A : Type u
inst : Ring A
M : Type v
inst_1 : AddCommGroup M
inst_2 : Module A M
h : FinitePresentation A M
G : Type w₀
w : Finite G
var : G → M
hG : Eq (α := Submodule A M) (Submodule.span A (Set.range var)) ⊤
R : Type w₁
w_1 : Finite R
relation : R → G →₀ A
hR : Submodule.span A (Set.range relation) = LinearMap.ker (Finsupp.linearCombination A var)
⊢ ∃ (pres : Presentation.{w₀, w₁, v, u} A M), Finite.{w₀ + 1} pres.G ∧ Finite.{w₁ + 1} pres.R

Tactic:
exact
     ⟨{ G := G
        R := R
        relation := relation
        var := var
        linearCombination_var_relation := fun r ↦ by
          rw [Submodule.ext_iff] at hR
          exact (hR _).1 (Submodule.subset_span ⟨_, rfl⟩)
        toIsPresentation := by
          rw [Relations.Solution.isPresentation_iff]
          exact ⟨hG, hR.symm⟩ },
        inferInstance, inferInstance⟩
-- Module: Mathlib.Algebra.Module.Presentation.Finite
Goal:
A : Type u
inst : Ring A
M : Type v
inst_1 : AddCommGroup M
inst_2 : Module A M
pres : Presentation.{w₀, w₁, v, u} A M
left : Finite.{w₀ + 1} pres.G
right : Finite.{w₁ + 1} pres.R
⊢ FinitePresentation A M

Tactic:
pres.finitePresentation

Premises used: Module.Presentation.finitePresentation
-- Module: Mathlib.Algebra.Module.Presentation.Finite
Goal:
A : Type u
inst : Ring A
M : Type v
inst_1 : AddCommGroup M
inst_2 : Module A M
pres : Presentation.{w₀, w₁, v, u} A M
left : Finite.{w₀ + 1} pres.G
right : Finite.{w₁ + 1} pres.R
⊢ FinitePresentation A M

Tactic:
exact pres.finitePresentation

Premises used: Module.Presentation.finitePresentation
-- Module: Mathlib.Algebra.Module.Presentation.Free
Goal:
A : Type u
inst : Ring A
relations : Relations.{w₀, w₁, u} A
M : Type v
inst_1 : AddCommGroup M
inst_2 : Module A M
inst_3 : IsEmpty.{w₁ + 1} relations.R
r : relations.R
exfalso : False
⊢ Eq (α := Finsupp.{w₀, u} relations.G A)
    ((Finsupp.linearCombination A fun (g : relations.G) ↦ Finsupp.single g 1 :
          (a : relations.G →₀ A) → relations.G →₀ A)
        (relations.relation r) :
      Finsupp.{w₀, u} relations.G A)
    (0 : Finsupp.{w₀, u} relations.G A)

Tactic:
exfalso
-- Module: Mathlib.Algebra.Module.Presentation.Free
Goal:
A : Type u
inst : Ring A
relations : Relations.{w₀, w₁, u} A
M : Type v
inst_1 : AddCommGroup M
inst_2 : Module A M
inst_3 : IsEmpty.{w₁ + 1} relations.R
r : relations.R
⊢ False

Tactic:
IsEmpty.false r

Premises used: IsEmpty.false
-- Module: Mathlib.Algebra.Module.Presentation.Free
Goal:
A : Type u
inst : Ring A
relations : Relations.{w₀, w₁, u} A
M : Type v
inst_1 : AddCommGroup M
inst_2 : Module A M
inst_3 : IsEmpty.{w₁ + 1} relations.R
r : relations.R
⊢ False

Tactic:
exact IsEmpty.false r

Premises used: IsEmpty.false
-- Module: Mathlib.Algebra.Module.Presentation.Free
Goal:
A : Type u
inst : Ring A
relations : Relations.{w₀, w₁, u} A
M : Type v
inst_1 : AddCommGroup M
inst_2 : Module A M
inst_3 : IsEmpty.{w₁ + 1} relations.R
⊢ ∀ {N : Type w} [inst_4 : AddCommGroup N] [inst_5 : Module A N] (s : relations.Solution N),
    relations.solutionFinsupp.postcomp (Finsupp.linearCombination A s.var) = s

Tactic:
aesop
-- Module: Mathlib.Algebra.Module.Presentation.Free
Goal:
A : Type u
inst : Ring A
relations : Relations.{w₀, w₁, u} A
M : Type v
inst_1 : AddCommGroup M
inst_2 : Module A M
inst_3 : IsEmpty.{w₁ + 1} relations.R
N : Type w
inst_4 : AddCommGroup N
inst_5 : Module A N
f f' : Finsupp.{w₀, u} relations.G A →ₗ[A] N
h : relations.solutionFinsupp.postcomp f = relations.solutionFinsupp.postcomp f'
h₁ :
  ∀ (a : relations.G),
    Eq.{w + 1} (α := N) ((f ∘ₗ Finsupp.lsingle a : (a : A) → N) 1 : N) ((f' ∘ₗ Finsupp.lsingle a : (a : A) → N) 1 : N)
⊢ f = f'

Tactic:
ext
-- Module: Mathlib.Algebra.Module.Presentation.Free
Goal:
A : Type u
inst : Ring A
relations : Relations.{w₀, w₁, u} A
M : Type v
inst_1 : AddCommGroup M
inst_2 : Module A M
inst_3 : IsEmpty.{w₁ + 1} relations.R
N : Type w
inst_4 : AddCommGroup N
inst_5 : Module A N
f f' : Finsupp.{w₀, u} relations.G A →ₗ[A] N
h : relations.solutionFinsupp.postcomp f = relations.solutionFinsupp.postcomp f'
a : relations.G
⊢ Eq.{w + 1} (α := N) ((f ∘ₗ Finsupp.lsingle a : (a : A) → N) 1 : N) ((f' ∘ₗ Finsupp.lsingle a : (a : A) → N) 1 : N)

Tactic:
apply Solution.congr_var h

Premises used: Module.Relations.Solution.congr_var
-- Module: Mathlib.Algebra.Module.Presentation.Free
Goal:
A : Type u
inst : Ring A
relations : Relations.{w₀, w₁, u} A
inst_1 : IsEmpty.{w₁ + 1} relations.R
⊢ relations.solutionFinsupp.IsPresentation

Tactic:
(solutionFinsupp.isPresentationCore relations).isPresentation

Premises used: Module.Relations.solutionFinsupp.isPresentationCore, Module.Relations.Solution.IsPresentationCore.isPresentation
-- Module: Mathlib.Algebra.Module.Presentation.Free
Goal:
A : Type u
inst : Ring A
relations : Relations.{w₀, w₁, u} A
M : Type v
inst_1 : AddCommGroup M
inst_2 : Module A M
inst_3 : IsEmpty.{w₁ + 1} relations.R
solution : relations.Solution M
h : solution.IsPresentation
⊢ Free A M

Tactic:
Free.of_equiv ((solutionFinsupp_isPresentation relations).uniq h)

Premises used: Module.Free.of_equiv, Module.Relations.Solution.IsPresentation.uniq, Module.Relations.solutionFinsupp_isPresentation
-- Module: Mathlib.Algebra.Module.Presentation.Free
Goal:
A : Type u
inst : Ring A
relations : Relations.{w₀, w₁, u} A
M : Type v
inst_1 : AddCommGroup M
inst_2 : Module A M
G : Type w₀
⊢ Relations.Solution.IsPresentation (A := A) (relations :=
    { G := G, R := PEmpty.{w₁ + 1},
      relation := fun (r : PEmpty.{w₁ + 1}) ↦ PEmpty.casesOn (fun (x : PEmpty.{w₁ + 1}) ↦ G →₀ A) r })
    (Relations.solutionFinsupp
      { G := G, R := PEmpty.{w₁ + 1},
        relation := fun (r : PEmpty.{w₁ + 1}) ↦ PEmpty.casesOn (fun (x : PEmpty.{w₁ + 1}) ↦ G →₀ A) r })

Tactic:
Relations.solutionFinsupp_isPresentation _

Premises used: Module.Relations.solutionFinsupp_isPresentation
-- Module: Mathlib.Algebra.Module.Presentation.Free
Goal:
A : Type u
inst : Ring A
relations : Relations.{w₀, w₁, u} A
M : Type v
inst_1 : AddCommGroup M
inst_2 : Module A M
G : Type w₀
⊢ Relations.Solution.IsPresentation (A := A) (relations :=
    { G := G, R := PEmpty.{w₁ + 1},
      relation := fun (r : PEmpty.{w₁ + 1}) ↦ PEmpty.casesOn (fun (x : PEmpty.{w₁ + 1}) ↦ G →₀ A) r })
    (Relations.solutionFinsupp
      { G := G, R := PEmpty.{w₁ + 1},
        relation := fun (r : PEmpty.{w₁ + 1}) ↦ PEmpty.casesOn (fun (x : PEmpty.{w₁ + 1}) ↦ G →₀ A) r })

Tactic:
exact Relations.solutionFinsupp_isPresentation _
-- Module: Mathlib.Algebra.Module.Presentation.Free
Goal:
A : Type u
inst : Ring A
M : Type v
inst_1 : AddCommGroup M
inst_2 : Module A M
mp : Free A M → ∃ (p : Presentation.{v, w₁, v, u} A M), IsEmpty.{w₁ + 1} p.R
mpr : (∃ (p : Presentation.{v, w₁, v, u} A M), IsEmpty.{w₁ + 1} p.R) → Free A M
⊢ Free A M ↔ ∃ (p : Presentation.{v, w₁, v, u} A M), IsEmpty.{w₁ + 1} p.R

Tactic:
constructor
-- Module: Mathlib.Algebra.Module.Presentation.Free
Goal:
A : Type u
inst : Ring A
M : Type v
inst_1 : AddCommGroup M
inst_2 : Module A M
mp : (∃ (I : Type v), Nonempty (Basis I A M)) → ∃ (p : Presentation.{v, w₁, v, u} A M), IsEmpty.{w₁ + 1} p.R
⊢ Free A M → ∃ (p : Presentation.{v, w₁, v, u} A M), IsEmpty.{w₁ + 1} p.R

Tactic:
rw [free_def.{_, _, v}]