awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Module.Presentation.Basic
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
solution : relations.Solution M
⊢ solution.fromQuotient ∘ₗ relations.toQuotient = solution.π

Tactic:
rfl

Premises used: Multiset.sum, Multiset.foldr, Quotient.liftOn', AddCon.liftOn, Finsupp.sum, Module.Relations.Solution.π, Finsupp.linearCombination, Finset.sum, rfl
-- Module: Mathlib.Algebra.Module.Presentation.Basic
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
solution : relations.Solution M
x : Finsupp.{w₀, u} relations.G A
⊢ Eq.{v + 1} (α := M)
    ((solution.fromQuotient : (a : relations.Quotient) → M)
        ((relations.toQuotient : (a : relations.G →₀ A) → relations.Quotient) x : relations.Quotient) :
      M)
    ((solution.π : (a : relations.G →₀ A) → M) x : M)

Tactic:
rfl

Premises used: Multiset.sum, Multiset.foldr, Quotient.liftOn', AddCon.liftOn, Finsupp.sum, Finset.sum, rfl
-- Module: Mathlib.Algebra.Module.Presentation.Basic
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
solution : relations.Solution M
N : Type v'
inst_3 : AddCommGroup N
inst_4 : Module A N
f : M →ₗ[A] N
r : relations.R
⊢ (Finsupp.linearCombination A fun (g : relations.G) ↦ (f : (a : M) → N) (solution.var g)) = f ∘ₗ solution.π

Tactic:
aesop
-- Module: Mathlib.Algebra.Module.Presentation.Basic
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
solution : relations.Solution M
N : Type v'
inst_3 : AddCommGroup N
inst_4 : Module A N
f : M →ₗ[A] N
r : relations.R
⊢ (Finsupp.linearCombination A fun (g : relations.G) ↦ (f : (a : M) → N) (solution.var g)) = f ∘ₗ solution.π

Tactic:
have : Finsupp.linearCombination _ (fun g ↦ f (solution.var g)) = f.comp solution.π := by aesop
-- Module: Mathlib.Algebra.Module.Presentation.Basic
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
solution : relations.Solution M
N : Type v'
inst_3 : AddCommGroup N
inst_4 : Module A N
f : M →ₗ[A] N
r : relations.R
this : (Finsupp.linearCombination A fun (g : relations.G) ↦ (f : (a : M) → N) (solution.var g)) = f ∘ₗ solution.π
⊢ Eq.{v' + 1} (α := N)
    ((Finsupp.linearCombination A fun (g : relations.G) ↦ (f : (a : M) → N) (solution.var g) :
          (a : relations.G →₀ A) → N)
        (relations.relation r) :
      N)
    (0 : N)

Tactic:
simp [this]
-- Module: Mathlib.Algebra.Module.Presentation.Basic
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
solution : relations.Solution M
N : Type v'
inst_3 : AddCommGroup N
inst_4 : Module A N
f : M →ₗ[A] N
N' : Type v''
inst_5 : AddCommGroup N'
inst_6 : Module A N'
g : N →ₗ[A] N'
⊢ solution.postcomp (g ∘ₗ f) = (solution.postcomp f).postcomp g

Tactic:
rfl

Premises used: Module.Relations.Solution.postcomp, rfl
-- Module: Mathlib.Algebra.Module.Presentation.Basic
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
solution : relations.Solution M
⊢ solution.postcomp LinearMap.id = solution

Tactic:
rfl

Premises used: Module.Relations.Solution.postcomp, rfl
-- Module: Mathlib.Algebra.Module.Presentation.Basic
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
solution solution' : relations.Solution M
h : solution = solution'
g : relations.G
rw rw₁ : solution'.var g = solution'.var g
⊢ solution.var g = solution'.var g

Tactic:
rw [h]
-- Module: Mathlib.Algebra.Module.Presentation.Basic
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
solution : relations.Solution M
N : Type v'
inst_3 : AddCommGroup N
inst_4 : Module A N
solution' : relations.Solution M
h : solution = solution'
f : M →ₗ[A] N
rw rw₁ : solution'.postcomp f = solution'.postcomp f
⊢ solution.postcomp f = solution'.postcomp f

Tactic:
rw [h]
-- Module: Mathlib.Algebra.Module.Presentation.Basic
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
π : Finsupp.{w₀, u} relations.G A →ₗ[A] M
hπ : ∀ (r : relations.R), Eq.{v + 1} (α := M) ((π : (a : relations.G →₀ A) → M) (relations.relation r) : M) (0 : M)
r : relations.R
h :
  ∀ (a : relations.G),
    Eq.{v + 1} (α := M) ((π ∘ₗ Finsupp.lsingle a : (a : A) → M) 1 : M)
      (((Finsupp.linearCombination A fun (g : relations.G) ↦ (π : (a : relations.G →₀ A) → M) (Finsupp.single g 1)) ∘ₗ
              Finsupp.lsingle a :
            (a : A) → M)
          1 :
        M)
⊢ π = Finsupp.linearCombination A fun (g : relations.G) ↦ (π : (a : relations.G →₀ A) → M) (Finsupp.single g 1)

Tactic:
ext
-- Module: Mathlib.Algebra.Module.Presentation.Basic
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
π : Finsupp.{w₀, u} relations.G A →ₗ[A] M
hπ : ∀ (r : relations.R), Eq.{v + 1} (α := M) ((π : (a : relations.G →₀ A) → M) (relations.relation r) : M) (0 : M)
r : relations.R
a : relations.G
⊢ Eq.{v + 1} (α := M) ((π ∘ₗ Finsupp.lsingle a : (a : A) → M) 1 : M)
    (((Finsupp.linearCombination A fun (g : relations.G) ↦ (π : (a : relations.G →₀ A) → M) (Finsupp.single g 1)) ∘ₗ
            Finsupp.lsingle a :
          (a : A) → M)
        1 :
      M)

Tactic:
simp
-- Module: Mathlib.Algebra.Module.Presentation.Basic
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
π : Finsupp.{w₀, u} relations.G A →ₗ[A] M
hπ : ∀ (r : relations.R), Eq.{v + 1} (α := M) ((π : (a : relations.G →₀ A) → M) (relations.relation r) : M) (0 : M)
r : relations.R
⊢ π = Finsupp.linearCombination A fun (g : relations.G) ↦ (π : (a : relations.G →₀ A) → M) (Finsupp.single g 1)

Tactic:
have : π = Finsupp.linearCombination _ (fun g ↦ π (Finsupp.single g 1)) := by ext; simp
-- Module: Mathlib.Algebra.Module.Presentation.Basic
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
π : Finsupp.{w₀, u} relations.G A →ₗ[A] M
hπ : ∀ (r : relations.R), Eq.{v + 1} (α := M) ((π : (a : relations.G →₀ A) → M) (relations.relation r) : M) (0 : M)
r : relations.R
this : π = Finsupp.linearCombination A fun (g : relations.G) ↦ (π : (a : relations.G →₀ A) → M) (Finsupp.single g 1)
rw : Eq.{v + 1} (α := M) ((π : (a : relations.G →₀ A) → M) (relations.relation r) : M) (0 : M)
⊢ Eq.{v + 1} (α := M)
    ((Finsupp.linearCombination A fun (g : relations.G) ↦ (π : (a : relations.G →₀ A) → M) (Finsupp.single g 1) :
          (a : relations.G →₀ A) → M)
        (relations.relation r) :
      M)
    (0 : M)

Tactic:
rw [← this]
-- Module: Mathlib.Algebra.Module.Presentation.Basic
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
π : Finsupp.{w₀, u} relations.G A →ₗ[A] M
hπ : ∀ (r : relations.R), Eq.{v + 1} (α := M) ((π : (a : relations.G →₀ A) → M) (relations.relation r) : M) (0 : M)
r : relations.R
this : π = Finsupp.linearCombination A fun (g : relations.G) ↦ (π : (a : relations.G →₀ A) → M) (Finsupp.single g 1)
⊢ Eq.{v + 1} (α := M) ((π : (a : relations.G →₀ A) → M) (relations.relation r) : M) (0 : M)

Tactic:
hπ r
-- Module: Mathlib.Algebra.Module.Presentation.Basic
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
π : Finsupp.{w₀, u} relations.G A →ₗ[A] M
hπ : ∀ (r : relations.R), Eq.{v + 1} (α := M) ((π : (a : relations.G →₀ A) → M) (relations.relation r) : M) (0 : M)
r : relations.R
this : π = Finsupp.linearCombination A fun (g : relations.G) ↦ (π : (a : relations.G →₀ A) → M) (Finsupp.single g 1)
⊢ Eq.{v + 1} (α := M) ((π : (a : relations.G →₀ A) → M) (relations.relation r) : M) (0 : M)

Tactic:
exact hπ r
-- Module: Mathlib.Algebra.Module.Presentation.Basic
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
π : Finsupp.{w₀, u} relations.G A →ₗ[A] M
hπ : ∀ (r : relations.R), Eq.{v + 1} (α := M) ((π : (a : relations.G →₀ A) → M) (relations.relation r) : M) (0 : M)
h :
  ∀ (a : relations.G),
    Eq.{v + 1} (α := M) (((ofπ π hπ).π ∘ₗ Finsupp.lsingle a : (a : A) → M) 1 : M)
      ((π ∘ₗ Finsupp.lsingle a : (a : A) → M) 1 : M)
⊢ (ofπ π hπ).π = π

Tactic:
ext
-- Module: Mathlib.Algebra.Module.Presentation.Basic
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
π : Finsupp.{w₀, u} relations.G A →ₗ[A] M
hπ : ∀ (r : relations.R), Eq.{v + 1} (α := M) ((π : (a : relations.G →₀ A) → M) (relations.relation r) : M) (0 : M)
a : relations.G
⊢ Eq.{v + 1} (α := M) (((ofπ π hπ).π ∘ₗ Finsupp.lsingle a : (a : A) → M) 1 : M)
    ((π ∘ₗ Finsupp.lsingle a : (a : A) → M) 1 : M)

Tactic:
simp [ofπ]

Premises used: Module.Relations.Solution.ofπ
-- Module: Mathlib.Algebra.Module.Presentation.Basic
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
π : Finsupp.{w₀, u} relations.G A →ₗ[A] M
hπ : π ∘ₗ relations.map = 0
r : relations.R
⊢ Eq.{v + 1} (α := M) ((π : (a : relations.G →₀ A) → M) (relations.relation r) : M) (0 : M)

Tactic:
simpa using DFunLike.congr_fun hπ (Finsupp.single r 1)

Premises used: DFunLike.congr_fun, OfNat.ofNat, Finsupp.single
-- Module: Mathlib.Algebra.Module.Presentation.Basic
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
π : Finsupp.{w₀, u} relations.G A →ₗ[A] M
hπ : π ∘ₗ relations.map = 0
⊢ (ofπ' π hπ).π = π

Tactic:
simp [ofπ']

Premises used: Module.Relations.Solution.ofπ'
-- Module: Mathlib.Algebra.Module.Presentation.Basic
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
solution : relations.Solution M
mp :
  Function.Injective (α := relations.Quotient) (β := M) (⇑solution.fromQuotient : (a : relations.Quotient) → M) →
    solution.π.ker = Submodule.span A (Set.range relations.relation)
mpr :
  solution.π.ker = Submodule.span A (Set.range relations.relation) →
    Function.Injective (α := relations.Quotient) (β := M) (⇑solution.fromQuotient : (a : relations.Quotient) → M)
⊢ Function.Injective (α := relations.Quotient) (β := M) (⇑solution.fromQuotient : (a : relations.Quotient) → M) ↔
    solution.π.ker = Submodule.span A (Set.range relations.relation)

Tactic:
constructor
-- Module: Mathlib.Algebra.Module.Presentation.Basic
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
solution : relations.Solution M
h : Function.Injective (α := relations.Quotient) (β := M) (⇑solution.fromQuotient : (a : relations.Quotient) → M)
mp : solution.π.ker = relations.toQuotient.ker
mp₁ : (solution.fromQuotient ∘ₗ relations.toQuotient).ker = relations.toQuotient.ker
mp₂ : Submodule.comap relations.toQuotient solution.fromQuotient.ker = relations.toQuotient.ker
mp₃ : Submodule.comap relations.toQuotient ⊥ = relations.toQuotient.ker
mp₄ mp₅ : relations.toQuotient.ker = relations.toQuotient.ker
⊢ solution.π.ker = Submodule.span A (Set.range relations.relation)

Tactic:
rw [← ker_toQuotient, ← fromQuotient_comp_toQuotient, LinearMap.ker_comp,
      LinearMap.ker_eq_bot.2 h, Submodule.comap_bot]

Premises used: Iff.mpr, LinearMap.ker_eq_bot, LinearMap.ker_comp, Module.Relations.ker_toQuotient, Module.Relations.Solution.fromQuotient_comp_toQuotient, Submodule.comap_bot
-- Module: Mathlib.Algebra.Module.Presentation.Basic
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
solution : relations.Solution M
h : solution.π.ker = Submodule.span A (Set.range relations.relation)
mpr : solution.fromQuotient.ker ≤ ⊥
⊢ Function.Injective (α := relations.Quotient) (β := M) (⇑solution.fromQuotient : (a : relations.Quotient) → M)

Tactic:
rw [← LinearMap.ker_eq_bot, eq_bot_iff]

Premises used: LinearMap.ker_eq_bot, eq_bot_iff
-- Module: Mathlib.Algebra.Module.Presentation.Basic
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
solution : relations.Solution M
h : solution.π.ker = Submodule.span A (Set.range relations.relation)
x : relations.Quotient
hx : x ∈ solution.fromQuotient.ker
mpr :
  ∀ (x : Finsupp.{w₀, u} relations.G A)
    (hx :
      Membership.mem (α := relations.Quotient) solution.fromQuotient.ker
        ((relations.toQuotient : (a : relations.G →₀ A) → relations.Quotient) x : relations.Quotient)),
    Membership.mem (α := relations.Quotient) (γ := Submodule A relations.Quotient) ⊥
      ((relations.toQuotient : (a : relations.G →₀ A) → relations.Quotient) x : relations.Quotient)
⊢ Membership.mem (γ := Submodule A relations.Quotient) ⊥ x

Tactic:
obtain ⟨x, rfl⟩ := relations.surjective_toQuotient x

Premises used: Module.Relations.surjective_toQuotient, rfl
-- Module: Mathlib.Algebra.Module.Presentation.Basic
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
solution : relations.Solution M
h : solution.π.ker = Submodule.span A (Set.range relations.relation)
x : Finsupp.{w₀, u} relations.G A
hx :
  Membership.mem (α := relations.Quotient) solution.fromQuotient.ker
    ((relations.toQuotient : (a : relations.G →₀ A) → relations.Quotient) x : relations.Quotient)
⊢ x ∈ solution.π.ker

Tactic:
simpa only [LinearMap.mem_ker, fromQuotient_toQuotient] using hx

Premises used: Module.Relations.Solution.fromQuotient_toQuotient, LinearMap.mem_ker
-- Module: Mathlib.Algebra.Module.Presentation.Basic
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
solution : relations.Solution M
h : solution.π.ker = Submodule.span A (Set.range relations.relation)
x : Finsupp.{w₀, u} relations.G A
hx :
  Membership.mem (α := relations.Quotient) solution.fromQuotient.ker
    ((relations.toQuotient : (a : relations.G →₀ A) → relations.Quotient) x : relations.Quotient)
⊢ x ∈ solution.π.ker

Tactic:
replace hx : x ∈ LinearMap.ker solution.π := by
      simpa only [LinearMap.mem_ker, fromQuotient_toQuotient] using hx
-- Module: Mathlib.Algebra.Module.Presentation.Basic
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
solution : relations.Solution M
h : solution.π.ker = Submodule.span A (Set.range relations.relation)
x : Finsupp.{w₀, u} relations.G A
hx : x ∈ solution.π.ker
⊢ x ∈ relations.map.range

Tactic:
rw [h, ← range_map] at hx

Premises used: Module.Relations.range_map
-- Module: Mathlib.Algebra.Module.Presentation.Basic
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
solution : relations.Solution M
h : solution.π.ker = Submodule.span A (Set.range relations.relation)
x : Finsupp.{w₀, u} relations.G A
hx : x ∈ relations.map.range
mpr :
  ∀ (x : Finsupp.{w₁, u} relations.R A),
    Membership.mem (α := relations.Quotient) (γ := Submodule A relations.Quotient) ⊥
      ((relations.toQuotient : (a : relations.G →₀ A) → relations.Quotient)
          ((relations.map : (a : relations.R →₀ A) → relations.G →₀ A) x) :
        relations.Quotient)
⊢ Membership.mem (α := relations.Quotient) (γ := Submodule A relations.Quotient) ⊥
    ((relations.toQuotient : (a : relations.G →₀ A) → relations.Quotient) x : relations.Quotient)

Tactic:
obtain ⟨x, rfl⟩ := hx

Premises used: rfl
-- Module: Mathlib.Algebra.Module.Presentation.Basic
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
solution : relations.Solution M
h : solution.π.ker = Submodule.span A (Set.range relations.relation)
x : Finsupp.{w₁, u} relations.R A
⊢ Membership.mem (α := relations.Quotient) (γ := Submodule A relations.Quotient) ⊥
    ((relations.toQuotient : (a : relations.G →₀ A) → relations.Quotient)
        ((relations.map : (a : relations.R →₀ A) → relations.G →₀ A) x) :
      relations.Quotient)

Tactic:
simp only [toQuotient_map_apply, Submodule.zero_mem]

Premises used: Submodule.zero_mem, Module.Relations.toQuotient_map_apply
-- Module: Mathlib.Algebra.Module.Presentation.Basic
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
solution : relations.Solution M
⊢ Function.Surjective (α := relations.Quotient) (β := M) (⇑solution.fromQuotient : (a : relations.Quotient) → M) ↔
    Function.Surjective (α := Finsupp.{w₀, u} relations.G A) (β := M) (⇑solution.π : (a : relations.G →₀ A) → M)

Tactic:
simpa only [← fromQuotient_comp_toQuotient] using
    (Function.Surjective.of_comp_iff (f := solution.fromQuotient)
      relations.surjective_toQuotient).symm

Premises used: Module.Relations.surjective_toQuotient, Module.Relations.Solution.fromQuotient, Function.Surjective.of_comp_iff, Module.Relations.Solution.fromQuotient_comp_toQuotient, DFunLike.coe, Iff.symm
-- Module: Mathlib.Algebra.Module.Presentation.Basic
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
solution : relations.Solution M
rw : solution.π.range = ⊤ ↔ Eq (α := Submodule A M) (Submodule.span A (Set.range solution.var)) ⊤
rw₁ rw₂ :
  Eq (α := Submodule A M) (Submodule.span A (Set.range solution.var)) ⊤ ↔
    Eq (α := Submodule A M) (Submodule.span A (Set.range solution.var)) ⊤
⊢ Function.Surjective (α := Finsupp.{w₀, u} relations.G A) (β := M) (⇑solution.π : (a : relations.G →₀ A) → M) ↔
    Eq (α := Submodule A M) (Submodule.span A (Set.range solution.var)) ⊤

Tactic:
rw [← LinearMap.range_eq_top, range_π]

Premises used: Module.Relations.Solution.range_π, LinearMap.range_eq_top
-- Module: Mathlib.Algebra.Module.Presentation.Basic
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
solution : relations.Solution M
h : solution.IsPresentation
x : relations.Quotient
⊢ Eq.{v + 1} (α := M) ((h.linearEquiv : (a : relations.Quotient) → M) x : M)
    ((solution.fromQuotient : (a : relations.Quotient) → M) x : M)

Tactic:
rfl

Premises used: Quotient.liftOn', AddCon.liftOn, rfl
-- Module: Mathlib.Algebra.Module.Presentation.Basic
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
solution : relations.Solution M
h : solution.IsPresentation
g : relations.G
⊢ Eq.{v + 1} (α := M)
    ((h.linearEquiv : (a : relations.Quotient) → M)
        ((h.linearEquiv.symm : (a : M) → relations.Quotient) (solution.var g) : relations.Quotient) :
      M)
    ((h.linearEquiv : (a : relations.Quotient) → M)
        ((relations.toQuotient : (a : relations.G →₀ A) → relations.Quotient) (Finsupp.single g 1) :
          relations.Quotient) :
      M)

Tactic:
simp
-- Module: Mathlib.Algebra.Module.Presentation.Basic
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
solution : relations.Solution M
h : solution.IsPresentation
⊢ Function.Surjective (α := Finsupp.{w₀, u} relations.G A) (β := M) (⇑solution.π : (a : relations.G →₀ A) → M)

Tactic:
simpa only [← surjective_fromQuotient_iff_surjective_π] using h.bijective.2

Premises used: Module.Relations.Solution.surjective_fromQuotient_iff_surjective_π, And.right, Module.Relations.Solution.IsPresentation.bijective
-- Module: Mathlib.Algebra.Module.Presentation.Basic
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
solution : relations.Solution M
h : solution.IsPresentation
⊢ solution.π.ker = Submodule.span A (Set.range relations.relation)

Tactic:
simpa only [← injective_fromQuotient_iff_ker_π_eq_span] using h.bijective.1

Premises used: Module.Relations.Solution.injective_fromQuotient_iff_ker_π_eq_span, And.left, Module.Relations.Solution.IsPresentation.bijective
-- Module: Mathlib.Algebra.Module.Presentation.Basic
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
solution : relations.Solution M
h : solution.IsPresentation
rw : Function.Injective (α := relations.Quotient) (β := M) (⇑solution.fromQuotient : (a : relations.Quotient) → M)
⊢ Function.Exact (M := Finsupp.{w₁, u} relations.R A) (N := Finsupp.{w₀, u} relations.G A) (P := M)
    (⇑relations.map : (a : relations.R →₀ A) → relations.G →₀ A) (⇑solution.π : (a : relations.G →₀ A) → M)

Tactic:
rw [LinearMap.exact_iff, range_map, ← solution.injective_fromQuotient_iff_ker_π_eq_span]

Premises used: Module.Relations.Solution.injective_fromQuotient_iff_ker_π_eq_span, Module.Relations.range_map, LinearMap.exact_iff
-- Module: Mathlib.Algebra.Module.Presentation.Basic
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
solution : relations.Solution M
h : solution.IsPresentation
⊢ Function.Injective (α := relations.Quotient) (β := M) (⇑solution.fromQuotient : (a : relations.Quotient) → M)

Tactic:
h.bijective.1

Premises used: And.left, Module.Relations.Solution.IsPresentation.bijective
-- Module: Mathlib.Algebra.Module.Presentation.Basic
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
solution : relations.Solution M
h : solution.IsPresentation
⊢ Function.Injective (α := relations.Quotient) (β := M) (⇑solution.fromQuotient : (a : relations.Quotient) → M)

Tactic:
exact h.bijective.1

Premises used: And.left, Module.Relations.Solution.IsPresentation.bijective
-- Module: Mathlib.Algebra.Module.Presentation.Basic
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
solution : relations.Solution M
h : solution.IsPresentation
N : Type v'
inst_3 : AddCommGroup N
inst_4 : Module A N
s : relations.Solution N
g : relations.G
dsimp :
  (s.fromQuotient : (a : relations.Quotient) → N)
      ((h.linearEquiv.symm : (a : M) → relations.Quotient) (solution.var g) : relations.Quotient) =
    s.var g
⊢ (h.desc s : (a : M) → N) (solution.var g) = s.var g

Tactic:
dsimp [desc]

Premises used: Module.Relations.Solution.IsPresentation.desc
-- Module: Mathlib.Algebra.Module.Presentation.Basic
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
solution : relations.Solution M
h : solution.IsPresentation
N : Type v'
inst_3 : AddCommGroup N
inst_4 : Module A N
s : relations.Solution N
g : relations.G
⊢ (s.fromQuotient : (a : relations.Quotient) → N)
      ((h.linearEquiv.symm : (a : M) → relations.Quotient) (solution.var g) : relations.Quotient) =
    s.var g

Tactic:
simp only [linearEquiv_symm_var, fromQuotient_toQuotient, π_single]

Premises used: Module.Relations.Solution.IsPresentation.linearEquiv_symm_var, Module.Relations.Solution.fromQuotient_toQuotient, Module.Relations.Solution.π_single
-- Module: Mathlib.Algebra.Module.Presentation.Basic
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
solution : relations.Solution M
h : solution.IsPresentation
N : Type v'
inst_3 : AddCommGroup N
inst_4 : Module A N
s : relations.Solution N
⊢ h.desc s ∘ₗ solution.π = s.π

Tactic:
aesop