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
h : solution.IsPresentation
N : Type v'
inst_3 : AddCommGroup N
inst_4 : Module A N
s : relations.Solution N
x : Finsupp.{w₀, u} relations.G A
⊢ Eq.{v' + 1} (α := N) ((h.desc s : (a : M) → N) ((solution.π : (a : relations.G →₀ A) → M) x : M) : N)
    ((s.π : (a : relations.G →₀ A) → N) x : N)

Tactic:
DFunLike.congr_fun (h.desc_comp_π s) x

Premises used: DFunLike.congr_fun, Quotient.liftOn', AddCon.liftOn, Module.Relations.Solution.IsPresentation.desc_comp_π
-- 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
⊢ solution.postcomp (h.desc s) = s

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
h : solution.IsPresentation
N : Type v'
inst_3 : AddCommGroup N
inst_4 : Module A N
f f' : M →ₗ[A] N
h' : solution.postcomp f = solution.postcomp f'
this : f ∘ₗ solution.fromQuotient = f' ∘ₗ solution.fromQuotient
h₁ : ∀ (x : M), Eq.{v' + 1} (α := N) ((f : (a : M) → N) x : N) ((f' : (a : M) → N) x : N)
⊢ f = f'

Tactic:
ext x
-- 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
f f' : M →ₗ[A] N
h' : solution.postcomp f = solution.postcomp f'
this : f ∘ₗ solution.fromQuotient = f' ∘ₗ solution.fromQuotient
x : M
h₁ :
  ∀ (y : relations.Quotient),
    Eq.{v' + 1} (α := N) ((f : (a : M) → N) ((solution.fromQuotient : (a : relations.Quotient) → M) y : M) : N)
      ((f' : (a : M) → N) ((solution.fromQuotient : (a : relations.Quotient) → M) y : M) : N)
⊢ Eq.{v' + 1} (α := N) ((f : (a : M) → N) x : N) ((f' : (a : M) → N) x : N)

Tactic:
obtain ⟨y, rfl⟩ := h.bijective.2 x

Premises used: And.right, Module.Relations.Solution.IsPresentation.bijective, 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
N : Type v'
inst_3 : AddCommGroup N
inst_4 : Module A N
f f' : M →ₗ[A] N
h' : solution.postcomp f = solution.postcomp f'
this : f ∘ₗ solution.fromQuotient = f' ∘ₗ solution.fromQuotient
y : relations.Quotient
⊢ Eq.{v' + 1} (α := N) ((f : (a : M) → N) ((solution.fromQuotient : (a : relations.Quotient) → M) y : M) : N)
    ((f' : (a : M) → N) ((solution.fromQuotient : (a : relations.Quotient) → M) y : M) : N)

Tactic:
DFunLike.congr_fun this y

Premises used: DFunLike.congr_fun
-- 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
f f' : M →ₗ[A] N
h' : solution.postcomp f = solution.postcomp f'
this : f ∘ₗ solution.fromQuotient = f' ∘ₗ solution.fromQuotient
y : relations.Quotient
⊢ Eq.{v' + 1} (α := N) ((f : (a : M) → N) ((solution.fromQuotient : (a : relations.Quotient) → M) y : M) : N)
    ((f' : (a : M) → N) ((solution.fromQuotient : (a : relations.Quotient) → M) y : M) : N)

Tactic:
exact DFunLike.congr_fun this y

Premises used: DFunLike.congr_fun
-- 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
f f' : M →ₗ[A] N
h' : solution.postcomp f = solution.postcomp f'
suffices : f ∘ₗ solution.fromQuotient = f' ∘ₗ solution.fromQuotient
⊢ f = f'

Tactic:
suffices f.comp solution.fromQuotient = f'.comp solution.fromQuotient by
    ext x
    obtain ⟨y, rfl⟩ := h.bijective.2 x
    exact DFunLike.congr_fun this y
-- 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
f f' : M →ₗ[A] N
h' : solution.postcomp f = solution.postcomp f'
h₁ :
  ∀ (g : relations.G),
    Eq.{v' + 1} (α := N)
      ((f ∘ₗ solution.fromQuotient : (a : relations.Quotient) → N)
          ((relations.toQuotient : (a : relations.G →₀ A) → relations.Quotient) (Finsupp.single g 1) :
            relations.Quotient) :
        N)
      ((f' ∘ₗ solution.fromQuotient : (a : relations.Quotient) → N)
          ((relations.toQuotient : (a : relations.G →₀ A) → relations.Quotient) (Finsupp.single g 1) :
            relations.Quotient) :
        N)
⊢ f ∘ₗ solution.fromQuotient = f' ∘ₗ solution.fromQuotient

Tactic:
ext g
-- 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
f f' : M →ₗ[A] N
h' : solution.postcomp f = solution.postcomp f'
g : relations.G
⊢ Eq.{v' + 1} (α := N)
    ((f ∘ₗ solution.fromQuotient : (a : relations.Quotient) → N)
        ((relations.toQuotient : (a : relations.G →₀ A) → relations.Quotient) (Finsupp.single g 1) :
          relations.Quotient) :
      N)
    ((f' ∘ₗ solution.fromQuotient : (a : relations.Quotient) → N)
        ((relations.toQuotient : (a : relations.G →₀ A) → relations.Quotient) (Finsupp.single g 1) :
          relations.Quotient) :
      N)

Tactic:
simpa using congr_var h' g

Premises used: Module.Relations.Solution.congr_var
-- 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
f : M →ₗ[A] N
⊢ solution.postcomp ((fun (s : relations.Solution N) ↦ h.desc s) ((fun (f : M →ₗ[A] N) ↦ solution.postcomp f) f)) =
    solution.postcomp f

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
N : Type v'
inst_3 : AddCommGroup N
inst_4 : Module A N
s : relations.Solution N
⊢ (fun (f : M →ₗ[A] N) ↦ solution.postcomp f) ((fun (s : relations.Solution N) ↦ h.desc s) s) = s

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
N : Type v'
inst_3 : AddCommGroup N
inst_4 : Module A N
solution' : relations.Solution N
h' : solution'.IsPresentation
⊢ solution'.postcomp (h.desc solution' ∘ₗ h'.desc solution) = solution'.postcomp LinearMap.id

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
N : Type v'
inst_3 : AddCommGroup N
inst_4 : Module A N
solution' : relations.Solution N
h' : solution'.IsPresentation
⊢ solution.postcomp (h'.desc solution ∘ₗ h.desc solution') = solution.postcomp LinearMap.id

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
N : Type v'
inst_3 : AddCommGroup N
inst_4 : Module A N
solution' : relations.Solution N
h' : solution'.IsPresentation
⊢ solution.postcomp (↑(h.uniq h') : M →ₗ[A] N) = solution'

Tactic:
simp [uniq]

Premises used: Module.Relations.Solution.IsPresentation.uniq
-- 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
solution' : relations.Solution N
h' : solution'.IsPresentation
⊢ solution'.postcomp (↑(h.uniq h').symm : N →ₗ[A] M) = solution

Tactic:
simp [uniq]

Premises used: Module.Relations.Solution.IsPresentation.uniq
-- 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
solution' : relations.Solution N
h' : solution'.IsPresentation
g : relations.G
⊢ (h.uniq h' : (a : M) → N) (solution.var g) = solution'.var g

Tactic:
simp [uniq]

Premises used: Module.Relations.Solution.IsPresentation.uniq
-- 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
solution' : relations.Solution N
h' : solution'.IsPresentation
g : relations.G
⊢ ((h.uniq h').symm : (a : N) → M) (solution'.var g) = solution.var g

Tactic:
simp [uniq]

Premises used: Module.Relations.Solution.IsPresentation.uniq
-- 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
e : M ≃ₗ[A] N
⊢ (solution.postcomp (↑e : M →ₗ[A] N)).fromQuotient = (↑e : M →ₗ[A] N) ∘ₗ solution.fromQuotient

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
h : solution.IsPresentation
N : Type v'
inst_3 : AddCommGroup N
inst_4 : Module A N
e : M ≃ₗ[A] N
⊢ (solution.postcomp (↑e : M →ₗ[A] N)).fromQuotient = (↑e : M →ₗ[A] N) ∘ₗ solution.fromQuotient

Tactic:
have : (solution.postcomp e.toLinearMap).fromQuotient =
      e.toLinearMap.comp (solution.fromQuotient) := 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
h : solution.IsPresentation
N : Type v'
inst_3 : AddCommGroup N
inst_4 : Module A N
e : M ≃ₗ[A] N
this : (solution.postcomp (↑e : M →ₗ[A] N)).fromQuotient = (↑e : M →ₗ[A] N) ∘ₗ solution.fromQuotient
rw :
  Function.Bijective (α := relations.Quotient) (β := N)
    (Function.comp (β := M) (⇑e : (a : M) → N) (⇑solution.fromQuotient : (a : relations.Quotient) → M))
⊢ Function.Bijective (α := relations.Quotient) (β := N)
    (⇑(solution.postcomp (↑e : M →ₗ[A] N)).fromQuotient : (a : relations.Quotient) → N)

Tactic:
rw [this, LinearMap.coe_comp, LinearEquiv.coe_coe]

Premises used: LinearMap.coe_comp, LinearEquiv.coe_coe
-- 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
e : M ≃ₗ[A] N
this : (solution.postcomp (↑e : M →ₗ[A] N)).fromQuotient = (↑e : M →ₗ[A] N) ∘ₗ solution.fromQuotient
⊢ Function.Bijective (α := relations.Quotient) (β := N)
    (Function.comp (β := M) (⇑e : (a : M) → N) (⇑solution.fromQuotient : (a : relations.Quotient) → M))

Tactic:
Function.Bijective.comp e.bijective h.bijective

Premises used: LinearEquiv.bijective, Module.Relations.Solution.IsPresentation.bijective, Function.Bijective.comp
-- 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
e : M ≃ₗ[A] N
this : (solution.postcomp (↑e : M →ₗ[A] N)).fromQuotient = (↑e : M →ₗ[A] N) ∘ₗ solution.fromQuotient
⊢ Function.Bijective (α := relations.Quotient) (β := N)
    (Function.comp (β := M) (⇑e : (a : M) → N) (⇑solution.fromQuotient : (a : relations.Quotient) → M))

Tactic:
exact Function.Bijective.comp e.bijective h.bijective

Premises used: LinearEquiv.bijective, Module.Relations.Solution.IsPresentation.bijective, Function.Bijective.comp
-- 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
⊢ ∀ (r : relations.R),
    Eq (α := relations.Quotient)
      ((relations.toQuotient : (a : relations.G →₀ A) → relations.Quotient) (relations.relation r) : relations.Quotient)
      (0 : relations.Quotient)

Tactic:
simp
-- Module: Mathlib.Algebra.Module.Presentation.Basic
Goal:
A : Type u
inst : Ring A
relations : Relations.{w₀, w₁, u} A
⊢ (ofQuotient relations).π = Submodule.mkQ (Submodule.span A (Set.range relations.relation))

Tactic:
ofπ_π _ _

Premises used: Module.Relations.Solution.ofQuotient, Module.Relations.toQuotient, Module.Relations.Solution.ofπ_π
-- Module: Mathlib.Algebra.Module.Presentation.Basic
Goal:
A : Type u
inst : Ring A
relations : Relations.{w₀, w₁, u} A
⊢ (ofQuotient relations).fromQuotient = LinearMap.id

Tactic:
aesop
-- Module: Mathlib.Algebra.Module.Presentation.Basic
Goal:
A : Type u
inst : Ring A
relations : Relations.{w₀, w₁, u} A
⊢ Function.Bijective (α := relations.Quotient) (β := relations.Quotient)
    (⇑(ofQuotient relations).fromQuotient : (a : relations.Quotient) → relations.Quotient)

Tactic:
simpa only [ofQuotient_fromQuotient, LinearMap.id_coe] using Function.bijective_id

Premises used: Function.bijective_id, LinearMap.id_coe, Module.Relations.Solution.ofQuotient_fromQuotient
-- 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 : IsPresentationCore.{w', w₀, w₁, v, u} solution
N : Type w'
inst_3 : AddCommGroup N
inst_4 : Module A N
s : relations.Solution N
g : relations.G
⊢ (h.desc s : (a : M) → N) (solution.var g) = s.var g

Tactic:
congr_var (h.postcomp_desc s) g

Premises used: Module.Relations.Solution.IsPresentationCore.postcomp_desc, Module.Relations.Solution.congr_var
-- 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.IsPresentationCore
N : Type w''
inst_3 : AddCommGroup N
inst_4 : Module A N
s : relations.Solution N
⊢ solution.postcomp
      ((↑ULift.moduleEquiv : ULift.{w', w''} N →ₗ[A] N) ∘ₗ
        h.desc (N := ULift.{w', w''} N)
          (s.postcomp (↑(LinearEquiv.symm ULift.moduleEquiv) : N →ₗ[A] ULift.{w', w''} N))) =
    s

Tactic:
simpa using congr_postcomp
      (h.postcomp_desc (s.postcomp ULift.moduleEquiv.symm.toLinearMap))
        ULift.moduleEquiv.toLinearMap

Premises used: LinearEquiv.symm, Module.Relations.Solution.IsPresentationCore.postcomp_desc, LinearEquiv.toLinearMap, ULift.moduleEquiv, Module.Relations.Solution.congr_postcomp, Module.Relations.Solution.postcomp
-- 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.IsPresentationCore
N : Type w''
x : AddCommGroup N
x_1 : Module A N
f f' : M →ₗ[A] N
h' : solution.postcomp f = solution.postcomp f'
h₁ : ∀ (x_2 : M), Eq.{w'' + 1} (α := N) ((f : (a : M) → N) x_2 : N) ((f' : (a : M) → N) x_2 : N)
⊢ f = f'

Tactic:
ext x
-- 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.IsPresentationCore
N : Type w''
x_1 : AddCommGroup N
x_2 : Module A N
f f' : M →ₗ[A] N
h' : solution.postcomp f = solution.postcomp f'
x : M
⊢ Eq (α := relations.Solution (ULift.{w', w''} N))
    ((solution.postcomp f).postcomp (↑(LinearEquiv.symm ULift.moduleEquiv) : N →ₗ[A] ULift.{w', w''} N))
    ((solution.postcomp f').postcomp (↑(LinearEquiv.symm ULift.moduleEquiv) : N →ₗ[A] ULift.{w', w''} N))

Tactic:
have := congr_postcomp h' ULift.moduleEquiv.{_, _, w'}.symm.toLinearMap
-- 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.IsPresentationCore
N : Type w''
x_1 : AddCommGroup N
x_2 : Module A N
f f' : M →ₗ[A] N
h' : solution.postcomp f = solution.postcomp f'
x : M
this :
  Eq (α := relations.Solution (ULift.{w', w''} N))
    (solution.postcomp ((↑(LinearEquiv.symm ULift.moduleEquiv) : N →ₗ[A] ULift.{w', w''} N) ∘ₗ f))
    (solution.postcomp ((↑(LinearEquiv.symm ULift.moduleEquiv) : N →ₗ[A] ULift.{w', w''} N) ∘ₗ f'))
⊢ Eq.{w'' + 1} (α := N) ((f : (a : M) → N) x : N) ((f' : (a : M) → N) x : N)

Tactic:
simpa using DFunLike.congr_fun (h.postcomp_injective this) x

Premises used: DFunLike.congr_fun, Module.Relations.Solution.IsPresentationCore.postcomp_injective
-- 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.IsPresentationCore
⊢ solution.postcomp (solution.fromQuotient ∘ₗ h.down.desc (ofQuotient relations)) = solution.postcomp LinearMap.id

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
h : solution.IsPresentationCore
⊢ h.down.desc (ofQuotient relations) ∘ₗ solution.fromQuotient = LinearMap.id

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
h : solution.IsPresentationCore
e : relations.Quotient ≃ₗ[A] M := LinearEquiv.ofLinear solution.fromQuotient (h.down.desc (ofQuotient relations)) ⋯ ⋯
⊢ Function.Bijective (α := relations.Quotient) (β := M) (⇑solution.fromQuotient : (a : relations.Quotient) → M)

Tactic:
e.bijective

Premises used: LinearEquiv.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.IsPresentationCore
e : relations.Quotient ≃ₗ[A] M := LinearEquiv.ofLinear solution.fromQuotient (h.down.desc (ofQuotient relations)) ⋯ ⋯
⊢ Function.Bijective (α := relations.Quotient) (β := M) (⇑solution.fromQuotient : (a : relations.Quotient) → M)

Tactic:
exact e.bijective

Premises used: LinearEquiv.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
rw :
  solution.IsPresentation ↔
    Function.Surjective (α := relations.Quotient) (β := M) (⇑solution.fromQuotient : (a : relations.Quotient) → M) ∧
      Function.Injective (α := relations.Quotient) (β := M) (⇑solution.fromQuotient : (a : relations.Quotient) → M)
⊢ solution.IsPresentation ↔
    Eq (α := Submodule A M) (Submodule.span A (Set.range solution.var)) ⊤ ∧
      solution.π.ker = Submodule.span A (Set.range relations.relation)

Tactic:
rw [← injective_fromQuotient_iff_ker_π_eq_span,
    ← surjective_π_iff_span_eq_top, ← surjective_fromQuotient_iff_surjective_π, ]

Premises used: Module.Relations.Solution.surjective_π_iff_span_eq_top, Module.Relations.Solution.injective_fromQuotient_iff_ker_π_eq_span, Module.Relations.Solution.surjective_fromQuotient_iff_surjective_π
-- 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.IsPresentation ↔
    Function.Surjective (α := relations.Quotient) (β := M) (⇑solution.fromQuotient : (a : relations.Quotient) → M) ∧
      Function.Injective (α := relations.Quotient) (β := M) (⇑solution.fromQuotient : (a : relations.Quotient) → M)

Tactic:
⟨fun h ↦ ⟨h.bijective.2, h.bijective.1⟩, fun h ↦ ⟨⟨h.2, h.1⟩⟩⟩

Premises used: And.right, And.left, Module.Relations.Solution.IsPresentation.bijective, And.intro, Iff.intro, Module.Relations.Solution.IsPresentation.mk
-- 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.IsPresentation ↔
    Function.Surjective (α := relations.Quotient) (β := M) (⇑solution.fromQuotient : (a : relations.Quotient) → M) ∧
      Function.Injective (α := relations.Quotient) (β := M) (⇑solution.fromQuotient : (a : relations.Quotient) → M)

Tactic:
exact ⟨fun h ↦ ⟨h.bijective.2, h.bijective.1⟩, fun h ↦ ⟨⟨h.2, h.1⟩⟩⟩
-- 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₁ : Eq (α := Submodule A M) (Submodule.span A (Set.range solution.var)) ⊤
h₂ : solution.π.ker = Submodule.span A (Set.range relations.relation)
rw :
  Eq (α := Submodule A M) (Submodule.span A (Set.range solution.var)) ⊤ ∧
    solution.π.ker = Submodule.span A (Set.range relations.relation)
⊢ solution.IsPresentation

Tactic:
rw [isPresentation_iff]

Premises used: Module.Relations.Solution.isPresentation_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₁ : Eq (α := Submodule A M) (Submodule.span A (Set.range solution.var)) ⊤
h₂ : solution.π.ker = Submodule.span A (Set.range relations.relation)
left : Eq (α := Submodule A M) (Submodule.span A (Set.range solution.var)) ⊤
right : solution.π.ker = Submodule.span A (Set.range relations.relation)
⊢ Eq (α := Submodule A M) (Submodule.span A (Set.range solution.var)) ⊤ ∧
    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₁ : Eq (α := Submodule A M) (Submodule.span A (Set.range solution.var)) ⊤
h₂ : solution.π.ker = Submodule.span A (Set.range relations.relation)
⊢ Eq (α := Submodule A M) (Submodule.span A (Set.range solution.var)) ⊤

Tactic:
assumption