awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Module.PID (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsPrincipalIdealRing R
M : Type v
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : IsDomain R
inst_5 : Module.Finite R M
ι : Type u
w : Fintype ι
p : ι → R
irr : ∀ (i : ι), Irreducible (p i)
n : ι → ℕ
x : R
m : ℕ
e : M ≃ₗ[R] (Fin (m + 1) →₀ R) × ⨁ (i : ι), HasQuotient.Quotient R (B := Submodule R R) (R ∙ p i ^ n i)
h :
  (∀ (a : Fin (m + 1)),
      Eq (α := R)
        (((HSMul.hSMul (β :=
                  (Fin (m + 1) →₀ R) × ⨁ (i : ι), HasQuotient.Quotient R (B := Submodule R R) (R ∙ p i ^ n i)) x
                  ((Equiv.symm Finsupp.equivFunOnFinite : (a : Fin (m + 1) → R) → Fin (m + 1) →₀ R)
                      fun (x : Fin (m + 1)) ↦ 1,
                    (Equiv.symm
                          (DFinsupp.equivFunOnFintype (β := fun (i : ι) ↦
                            HasQuotient.Quotient R (B := Submodule R R) (R ∙ p i ^ n i))) :
                        (a : (i : ι) → R ⧸ R ∙ p i ^ n i) → Π₀ (i : ι), R ⧸ R ∙ p i ^ n i)
                      fun (x : ι) ↦ (mkQ (R ∙ p x ^ n x) : (a : R) → R ⧸ R ∙ p x ^ n x) 1)).1 :
              (a : Fin (m + 1)) → R)
            a :
          R)
        ((0.1 : (a : Fin (m + 1)) → R) a : R)) ∧
    ∀ (i : ι),
      ((HSMul.hSMul (β := (Fin (m + 1) →₀ R) × ⨁ (i : ι), HasQuotient.Quotient R (B := Submodule R R) (R ∙ p i ^ n i)) x
                ((Equiv.symm Finsupp.equivFunOnFinite : (a : Fin (m + 1) → R) → Fin (m + 1) →₀ R)
                    fun (x : Fin (m + 1)) ↦ 1,
                  (Equiv.symm
                        (DFinsupp.equivFunOnFintype (β := fun (i : ι) ↦
                          HasQuotient.Quotient R (B := Submodule R R) (R ∙ p i ^ n i))) :
                      (a : (i : ι) → R ⧸ R ∙ p i ^ n i) → Π₀ (i : ι), R ⧸ R ∙ p i ^ n i)
                    fun (x : ι) ↦ (mkQ (R ∙ p x ^ n x) : (a : R) → R ⧸ R ∙ p x ^ n x) 1)).2 :
            (a : ι) → R ⧸ R ∙ p a ^ n a)
          i =
        (0.2 : (a : ι) → R ⧸ R ∙ p a ^ n a) i
⊢ Membership.mem (γ := Submodule R R) (annihilator R M) x
have succ : Membership.mem (γ := Submodule R R) (annihilator R M) 0
Tactic: rw [show x = 0 by simpa using h.1 0]
-- Lean 4 proof step from Mathlib.Algebra.Module.Pi (goal)
Goal:
I : Type u
f : I → Type v
g : I → Type u_1
r : (i : I) → Semiring (f i)
m : (i : I) → AddCommMonoid (g i)
inst : (i : I) → Module.{v, u_1} (f i) (g i)
r_1 s : (i : I) → f i
x : (i : I) → g i
⊢ (r_1 + s) • x = r_1 • x + s • x
have h : ∀ (x_1 : I), ((r_1 + s) • x) x_1 = (r_1 • x + s • x) x_1
Tactic: ext1
-- Lean 4 proof step from Mathlib.Algebra.Module.Pi (goal)
Goal:
I : Type u
f : I → Type v
g : I → Type u_1
r : (i : I) → Semiring (f i)
m : (i : I) → AddCommMonoid (g i)
inst : (i : I) → Module.{v, u_1} (f i) (g i)
x : (i : I) → g i
⊢ HSMul.hSMul (α := (i : I) → f i) 0 x = 0
have h : ∀ (x_1 : I), HSMul.hSMul (α := (i : I) → f i) 0 x x_1 = 0 x_1
Tactic: ext1
-- Lean 4 proof step from Mathlib.Algebra.Module.Pi (goal)
Goal:
I : Type u
f : I → Type v
g : I → Type u_1
r : (i : I) → Semiring (f i)
m : (i : I) → AddCommMonoid (g i)
inst : (i : I) → Module.{v, u_1} (f i) (g i)
x : (i : I) → g i
x_1 : I
⊢ HSMul.hSMul (α := (i : I) → f i) 0 x x_1 = 0 x_1
have h : Eq.{u_1 + 1} (α := g x_1) (0 x_1) (0 x_1)
Tactic: rw [zero_smul]
-- Lean 4 proof step from Mathlib.Algebra.Module.Presentation.Basic (goal)
Goal:
A : Type u
inst : Ring A
relations : Relations.{w₀, w₁, u} A
r : relations.R
⊢ Eq (α :=
    HasQuotient.Quotient (Finsupp.{w₀, u} relations.G A) (B := Submodule A (Finsupp.{w₀, u} relations.G A))
      (Submodule.span A (Set.range relations.relation)))
    ((Submodule.mkQ (Submodule.span A (Set.range relations.relation)) :
          (a : relations.G →₀ A) → (relations.G →₀ A) ⧸ Submodule.span A (Set.range relations.relation))
        (relations.relation r) :
      HasQuotient.Quotient (Finsupp.{w₀, u} relations.G A) (B := Submodule A (Finsupp.{w₀, u} relations.G A))
        (Submodule.span A (Set.range relations.relation)))
    (0 : relations.Quotient)
have rw : Membership.mem (γ := Submodule A (Finsupp.{w₀, u} relations.G A)) (Submodule.span A (Set.range relations.relation))
  (relations.relation r)
Tactic: rw [Submodule.mkQ_apply, Submodule.Quotient.mk_eq_zero]
-- Lean 4 proof step from Mathlib.Algebra.Module.Presentation.Basic (goal)
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.R A
⊢ Eq.{v + 1} (α := M)
    ((solution.π : (a : relations.G →₀ A) → M)
        ((relations.map : (a : relations.R →₀ A) → relations.G →₀ A) x : Finsupp.{w₀, u} relations.G A) :
      M)
    (0 : M)
have change : Eq.{v + 1} (α := M) ((solution.π ∘ₗ relations.map : (a : relations.R →₀ A) → M) x : M) (0 : M)
Tactic: change solution.π.comp relations.map x = 0
-- Lean 4 proof step from Mathlib.Algebra.Module.Presentation.Basic (goal)
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.R A
⊢ Eq.{v + 1} (α := M) ((solution.π ∘ₗ relations.map : (a : relations.R →₀ A) → M) x : M) (0 : M)
have rw : Eq.{v + 1} (α := M) ((0 : (a : relations.R →₀ A) → M) x : M) (0 : M)
Tactic: rw [π_comp_map, LinearMap.zero_apply]
-- Lean 4 proof step from Mathlib.Algebra.Module.Presentation.Basic (goal)
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.R A
rw : Eq.{v + 1} (α := M) ((0 : (a : relations.R →₀ A) → M) x : M) (0 : M)
⊢ Eq.{v + 1} (α := M) ((solution.π ∘ₗ relations.map : (a : relations.R →₀ A) → M) x : M) (0 : M)
have rw₁ : Eq.{v + 1} (α := M) 0 0
Tactic: rw [π_comp_map, LinearMap.zero_apply]
-- Lean 4 proof step from Mathlib.Algebra.Module.Presentation.Basic (goal)
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
⊢ Submodule.span A (Set.range relations.relation) ≤ solution.π.ker
have rw : Set.range relations.relation ⊆ (↑solution.π.ker : Set (relations.G →₀ A))
Tactic: rw [Submodule.span_le]
-- Lean 4 proof step from Mathlib.Algebra.Module.Presentation.Basic (hypothesis)
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
⊢ 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)
have this : (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
-- Lean 4 proof step from Mathlib.Algebra.Module.Presentation.Basic (goal)
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
⊢ solution.var g = solution'.var g
have rw : solution'.var g = solution'.var g
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.Algebra.Module.Presentation.Basic (goal)
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
⊢ solution.postcomp f = solution'.postcomp f
have rw : solution'.postcomp f = solution'.postcomp f
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.Algebra.Module.Presentation.Basic (goal)
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)
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Module.Presentation.Basic (hypothesis)
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
⊢ 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)
have this : π = 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
-- Lean 4 proof step from Mathlib.Algebra.Module.Presentation.Basic (goal)
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)
    ((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)
have rw : Eq.{v + 1} (α := M) ((π : (a : relations.G →₀ A) → M) (relations.relation r) : M) (0 : M)
Tactic: rw [← this]
-- Lean 4 proof step from Mathlib.Algebra.Module.Presentation.Basic (goal)
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)
⊢ (ofπ π hπ).π = π
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Module.Presentation.Basic (goal)
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.Injective (α := relations.Quotient) (β := M) (⇑solution.fromQuotient : (a : relations.Quotient) → M) ↔
    solution.π.ker = Submodule.span A (Set.range relations.relation)
have mp : Function.Injective (α := relations.Quotient) (β := M) (⇑solution.fromQuotient : (a : relations.Quotient) → M) →
  solution.π.ker = Submodule.span A (Set.range relations.relation)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Module.Presentation.Basic (goal)
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)
⊢ Function.Injective (α := relations.Quotient) (β := M) (⇑solution.fromQuotient : (a : relations.Quotient) → M) ↔
    solution.π.ker = Submodule.span A (Set.range relations.relation)
have mpr : solution.π.ker = Submodule.span A (Set.range relations.relation) →
  Function.Injective (α := relations.Quotient) (β := M) (⇑solution.fromQuotient : (a : relations.Quotient) → M)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Module.Presentation.Basic (goal)
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)
⊢ solution.π.ker = Submodule.span A (Set.range relations.relation)
have mp : solution.π.ker = relations.toQuotient.ker
Tactic: rw [← ker_toQuotient, ← fromQuotient_comp_toQuotient, LinearMap.ker_comp,
      LinearMap.ker_eq_bot.2 h, Submodule.comap_bot]
-- Lean 4 proof step from Mathlib.Algebra.Module.Presentation.Basic (goal)
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
⊢ solution.π.ker = Submodule.span A (Set.range relations.relation)
have mp₁ : (solution.fromQuotient ∘ₗ relations.toQuotient).ker = relations.toQuotient.ker
Tactic: rw [← ker_toQuotient, ← fromQuotient_comp_toQuotient, LinearMap.ker_comp,
      LinearMap.ker_eq_bot.2 h, Submodule.comap_bot]
-- Lean 4 proof step from Mathlib.Algebra.Module.Presentation.Basic (goal)
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
⊢ solution.π.ker = Submodule.span A (Set.range relations.relation)
have mp₂ : Submodule.comap relations.toQuotient solution.fromQuotient.ker = relations.toQuotient.ker
Tactic: rw [← ker_toQuotient, ← fromQuotient_comp_toQuotient, LinearMap.ker_comp,
      LinearMap.ker_eq_bot.2 h, Submodule.comap_bot]
-- Lean 4 proof step from Mathlib.Algebra.Module.Presentation.Basic (goal)
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
⊢ solution.π.ker = Submodule.span A (Set.range relations.relation)
have mp₃ : Submodule.comap relations.toQuotient ⊥ = relations.toQuotient.ker
Tactic: rw [← ker_toQuotient, ← fromQuotient_comp_toQuotient, LinearMap.ker_comp,
      LinearMap.ker_eq_bot.2 h, Submodule.comap_bot]
-- Lean 4 proof step from Mathlib.Algebra.Module.Presentation.Basic (goal)
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
⊢ solution.π.ker = Submodule.span A (Set.range relations.relation)
have mp₄ : relations.toQuotient.ker = relations.toQuotient.ker
Tactic: rw [← ker_toQuotient, ← fromQuotient_comp_toQuotient, LinearMap.ker_comp,
      LinearMap.ker_eq_bot.2 h, Submodule.comap_bot]
-- Lean 4 proof step from Mathlib.Algebra.Module.Presentation.Basic (goal)
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)
⊢ Function.Injective (α := relations.Quotient) (β := M) (⇑solution.fromQuotient : (a : relations.Quotient) → M)
have mpr : solution.fromQuotient.ker ≤ ⊥
Tactic: rw [← LinearMap.ker_eq_bot, eq_bot_iff]
-- Lean 4 proof step from Mathlib.Algebra.Module.Presentation.Basic (goal)
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
⊢ Membership.mem (γ := Submodule A relations.Quotient) ⊥ x
have 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)
Tactic: obtain ⟨x, rfl⟩ := relations.surjective_toQuotient x
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.Algebra.Module.Presentation.Basic (hypothesis)
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)
⊢ Membership.mem (α := relations.Quotient) (γ := Submodule A relations.Quotient) ⊥
    ((relations.toQuotient : (a : relations.G →₀ A) → relations.Quotient) x : relations.Quotient)
have hx₁ : x ∈ solution.π.ker
Tactic: replace hx : x ∈ LinearMap.ker solution.π := by
      simpa only [LinearMap.mem_ker, fromQuotient_toQuotient] using hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Algebra.Module.Presentation.Basic (hypothesis)
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
⊢ Membership.mem (α := relations.Quotient) (γ := Submodule A relations.Quotient) ⊥
    ((relations.toQuotient : (a : relations.G →₀ A) → relations.Quotient) x : relations.Quotient)
have hx₁ : x ∈ relations.map.range
Tactic: rw [h, ← range_map] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Algebra.Module.Presentation.Basic (goal)
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
⊢ Membership.mem (α := relations.Quotient) (γ := Submodule A relations.Quotient) ⊥
    ((relations.toQuotient : (a : relations.G →₀ A) → relations.Quotient) x : relations.Quotient)
have 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)
Tactic: obtain ⟨x, rfl⟩ := hx
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.Algebra.Module.Presentation.Basic (goal)
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 (α := Finsupp.{w₀, u} relations.G A) (β := M) (⇑solution.π : (a : relations.G →₀ A) → M) ↔
    Eq (α := Submodule A M) (Submodule.span A (Set.range solution.var)) ⊤
have rw : solution.π.range = ⊤ ↔ Eq (α := Submodule A M) (Submodule.span A (Set.range solution.var)) ⊤
Tactic: rw [← LinearMap.range_eq_top, range_π]
-- Lean 4 proof step from Mathlib.Algebra.Module.Presentation.Basic (goal)
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)) ⊤
⊢ 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)) ⊤
have rw₁ : Eq (α := Submodule A M) (Submodule.span A (Set.range solution.var)) ⊤ ↔
  Eq (α := Submodule A M) (Submodule.span A (Set.range solution.var)) ⊤
Tactic: rw [← LinearMap.range_eq_top, range_π]
-- Lean 4 proof step from Mathlib.Algebra.Module.Presentation.Basic (goal)
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.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)
have rw : Function.Injective (α := relations.Quotient) (β := M) (⇑solution.fromQuotient : (a : relations.Quotient) → M)
Tactic: rw [LinearMap.exact_iff, range_map, ← solution.injective_fromQuotient_iff_ker_π_eq_span]
-- Lean 4 proof step from Mathlib.Algebra.Module.Presentation.Basic (goal)
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
⊢ (h.desc s : (a : M) → N) (solution.var g) = s.var g
have dsimp : (s.fromQuotient : (a : relations.Quotient) → N)
    ((h.linearEquiv.symm : (a : M) → relations.Quotient) (solution.var g) : relations.Quotient) =
  s.var g
Tactic: dsimp [desc]
-- Lean 4 proof step from Mathlib.Algebra.Module.Presentation.Basic (goal)
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
⊢ f = f'
have h₁ : ∀ (x : M), Eq.{v' + 1} (α := N) ((f : (a : M) → N) x : N) ((f' : (a : M) → N) x : N)
Tactic: ext x
-- Lean 4 proof step from Mathlib.Algebra.Module.Presentation.Basic (goal)
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
⊢ Eq.{v' + 1} (α := N) ((f : (a : M) → N) x : N) ((f' : (a : M) → N) x : N)
have 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)
Tactic: obtain ⟨y, rfl⟩ := h.bijective.2 x
Cleared hypotheses: x