awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Module.Presentation.DirectSum (goal)
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
s : (directSum relations).Solution N
i : ι
r : (relations i).R
⊢ Eq.{v + 1} (α := N)
    ((Finsupp.linearCombination A fun (g : (relations i).G) ↦
            s.var (Sigma.mk (β := fun (i : ι) ↦ (relations i).G) i g) :
          (a : (relations i).G →₀ A) → N)
        ((relations i).relation r) :
      N)
    ((Finsupp.linearCombination A s.var : (a : (directSum relations).G →₀ A) → N)
        ((directSum relations).relation (Sigma.mk (β := fun (i : ι) ↦ (relations i).R) i r)) :
      N)
have symm : Eq.{v + 1} (α := N)
  ((Finsupp.linearCombination A s.var : (a : (directSum relations).G →₀ A) → N)
      ((directSum relations).relation (Sigma.mk (β := fun (i : ι) ↦ (relations i).R) i r)) :
    N)
  ((Finsupp.linearCombination A fun (g : (relations i).G) ↦ s.var (Sigma.mk (β := fun (i : ι) ↦ (relations i).G) i g) :
        (a : (relations i).G →₀ A) → N)
      ((relations i).relation r) :
    N)
Tactic: symm
-- Lean 4 proof step from Mathlib.Algebra.Module.Presentation.DirectSum (goal)
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
t : (i : ι) → (relations i).Solution N
x : (directSum relations).R
i : ι
r : (relations i).R
⊢ Eq.{v + 1} (α := N)
    ((Finsupp.linearCombination A fun (x : (directSum relations).G) ↦
            match (motive := (directSum relations).G → N) x with
            | ⟨i, g⟩ => (t i).var g :
          (a : (directSum relations).G →₀ A) → N)
        ((directSum relations).relation (Sigma.mk (β := fun (i : ι) ↦ (relations i).R) i r)) :
      N)
    (0 : N)
have rw : Eq.{v + 1} (α := N)
  ((Finsupp.linearCombination A fun (x : (directSum relations).G) ↦
          match (motive := (directSum relations).G → N) x with
          | ⟨i, g⟩ => (t i).var g :
        (a : (directSum relations).G →₀ A) → N)
      ((directSum relations).relation (Sigma.mk (β := fun (i : ι) ↦ (relations i).R) i r)) :
    N)
  ((Finsupp.linearCombination A (t i).var : (a : (relations i).G →₀ A) → N) ((relations i).relation r) : N)
Tactic: rw [← (t i).linearCombination_var_relation r]
-- Lean 4 proof step from Mathlib.Algebra.Module.Presentation.DirectSum (goal)
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
s : (Relations.directSum relations).Solution N_1
⊢ (directSum (M := M) solution).postcomp
      (toModule A ι (M := M) N_1 fun (i : ι) ↦
        ⋯.desc
          ((directSumEquiv : (a : (Relations.directSum relations).Solution N_1) → (i : ι) → (relations i).Solution N_1)
            s i)) =
    s
have var : ∀ (i : ι) (g : (relations i).G),
  var
      ((directSum (M := M) solution).postcomp
        (toModule A ι (M := M) N_1 fun (i : ι) ↦
          sorry.desc
            ((directSumEquiv :
                (a : (Relations.directSum relations).Solution N_1) → (i : ι) → (relations i).Solution N_1)
              s i)))
      (Sigma.mk (β := fun (i : ι) ↦ (relations i).G) i g) =
    s.var (Sigma.mk (β := fun (i : ι) ↦ (relations i).G) i g)
Tactic: ext ⟨i, g⟩
-- Lean 4 proof step from Mathlib.Algebra.Module.Presentation.DirectSum (goal)
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'
⊢ f = f'
have H : ∀ (i : ι), f ∘ₗ lof A ι M i = f' ∘ₗ lof A ι M i
Tactic: ext i : 1
-- Lean 4 proof step from Mathlib.Algebra.Module.Presentation.DirectSum (goal)
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 : ι
⊢ f ∘ₗ lof A ι M i = f' ∘ₗ lof A ι M i
have H : (solution i).postcomp (f ∘ₗ lof A ι M i) = (solution i).postcomp (f' ∘ₗ lof A ι M i)
Tactic: apply (h i).postcomp_injective
-- Lean 4 proof step from Mathlib.Algebra.Module.Presentation.DirectSum (goal)
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 : ι
⊢ (solution i).postcomp (f ∘ₗ lof A ι M i) = (solution i).postcomp (f' ∘ₗ lof A ι M i)
have H : ∀ (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: ext g
-- Lean 4 proof step from Mathlib.Algebra.Module.Presentation.DirectSum (goal)
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
⊢ (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)
have 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)
Tactic: apply (finsuppLequivDFinsupp A).injective
-- Lean 4 proof step from Mathlib.Algebra.Module.Presentation.DirectSum (goal)
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)
    ((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)
have 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)))
Tactic: erw [(finsuppLequivDFinsupp A).apply_symm_apply]
-- Lean 4 proof step from Mathlib.Algebra.Module.Presentation.DirectSum (goal)
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)
    (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)))
have 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)
Tactic: rw [directSum_var, finsuppLequivDFinsupp_apply_apply, Finsupp.toDFinsupp_single]
-- Lean 4 proof step from Mathlib.Algebra.Module.Presentation.Finite (goal)
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
⊢ pres.π.ker.FG
have rw : Submodule.FG (Submodule.span A (Set.range pres.relation))
Tactic: rw [pres.ker_π]
-- Lean 4 proof step from Mathlib.Algebra.Module.Presentation.Finite (goal)
Goal:
A : Type u
inst : Ring A
M : Type v
inst_1 : AddCommGroup M
inst_2 : Module A M
⊢ FinitePresentation A M ↔ ∃ (pres : Presentation.{w₀, w₁, v, u} A M), Finite.{w₀ + 1} pres.G ∧ Finite.{w₁ + 1} pres.R
have mp : FinitePresentation A M → ∃ (pres : Presentation.{w₀, w₁, v, u} A M), Finite.{w₀ + 1} pres.G ∧ Finite.{w₁ + 1} pres.R
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Module.Presentation.Finite (goal)
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
⊢ FinitePresentation A M ↔ ∃ (pres : Presentation.{w₀, w₁, v, u} A M), Finite.{w₀ + 1} pres.G ∧ Finite.{w₁ + 1} pres.R
have mpr : (∃ (pres : Presentation.{w₀, w₁, v, u} A M), Finite.{w₀ + 1} pres.G ∧ Finite.{w₁ + 1} pres.R) → FinitePresentation A M
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Module.Presentation.Finite (goal)
Goal:
A : Type u
inst : Ring A
M : Type v
inst_1 : AddCommGroup M
inst_2 : Module A M
h : FinitePresentation A M
⊢ ∃ (pres : Presentation.{w₀, w₁, v, u} A M), Finite.{w₀ + 1} pres.G ∧ Finite.{w₁ + 1} pres.R
have 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
Tactic: obtain ⟨G : Type w₀, _, var, hG⟩ :=
      Submodule.fg_iff_exists_finite_generating_family.1
        (finite_def.1 (inferInstance : Module.Finite A M))
-- Lean 4 proof step from Mathlib.Algebra.Module.Presentation.Finite (goal)
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)) ⊤
⊢ Function.Surjective (α := G →₀ A) (β := M) (⇑(Finsupp.linearCombination A var) : (a : G →₀ A) → M)
have rw : Eq (α := Submodule A M) (LinearMap.range (Finsupp.linearCombination A var)) ⊤
Tactic: rw [← LinearMap.range_eq_top, Finsupp.range_linearCombination, hG]
-- Lean 4 proof step from Mathlib.Algebra.Module.Presentation.Finite (goal)
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)) ⊤
⊢ Function.Surjective (α := G →₀ A) (β := M) (⇑(Finsupp.linearCombination A var) : (a : G →₀ A) → M)
have rw₂ : Eq.{v + 1} (α := Submodule A M) ⊤ ⊤
Tactic: rw [← LinearMap.range_eq_top, Finsupp.range_linearCombination, hG]
-- Lean 4 proof step from Mathlib.Algebra.Module.Presentation.Finite (goal)
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)) ⊤
⊢ ∃ (pres : Presentation.{w₀, w₁, v, u} A M), Finite.{w₀ + 1} pres.G ∧ Finite.{w₁ + 1} pres.R
have 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
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]))
-- Lean 4 proof step from Mathlib.Algebra.Module.Presentation.Finite (goal)
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
⊢ Eq.{v + 1} (α := M) ((Finsupp.linearCombination A var : (a : G →₀ A) → M) (relation r) : M) (0 : M)
have 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)
Tactic: rw [Submodule.ext_iff] at hR
Cleared hypotheses: hR, r
-- Lean 4 proof step from Mathlib.Algebra.Module.Presentation.Finite (goal)
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)
⊢ Relations.Solution.IsPresentation.{w₀, w₁, v, u} (A := A) (relations := { G := G, R := R, relation := relation })
    (M := M) { var := var, linearCombination_var_relation := ⋯ }
have 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 := sorry })))
    ⊤ ∧
  LinearMap.ker (M₂ := M) (Relations.Solution.π { var := var, linearCombination_var_relation := sorry }) =
    Submodule.span A (Set.range { G := G, R := R, relation := relation : Relations.{w₀, w₁, u} A }.relation)
Tactic: rw [Relations.Solution.isPresentation_iff]
-- Lean 4 proof step from Mathlib.Algebra.Module.Presentation.Free (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
inst_3 : IsEmpty.{w₁ + 1} relations.R
r : relations.R
⊢ 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)
have exfalso : False
Tactic: exfalso
-- Lean 4 proof step from Mathlib.Algebra.Module.Presentation.Free (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
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'
⊢ f = f'
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Module.Presentation.Free (goal)
Goal:
A : Type u
inst : Ring A
M : Type v
inst_1 : AddCommGroup M
inst_2 : Module A M
⊢ Free A M ↔ ∃ (p : Presentation.{v, w₁, v, u} A M), IsEmpty.{w₁ + 1} p.R
have mp : Free A M → ∃ (p : Presentation.{v, w₁, v, u} A M), IsEmpty.{w₁ + 1} p.R
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Module.Presentation.Free (goal)
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
⊢ Free A M ↔ ∃ (p : Presentation.{v, w₁, v, u} A M), IsEmpty.{w₁ + 1} p.R
have mpr : (∃ (p : Presentation.{v, w₁, v, u} A M), IsEmpty.{w₁ + 1} p.R) → Free A M
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Module.Presentation.Free (goal)
Goal:
A : Type u
inst : Ring A
M : Type v
inst_1 : AddCommGroup M
inst_2 : Module A M
⊢ Free A M → ∃ (p : Presentation.{v, w₁, v, u} A M), IsEmpty.{w₁ + 1} p.R
have mp : (∃ (I : Type v), Nonempty (Basis I A M)) → ∃ (p : Presentation.{v, w₁, v, u} A M), IsEmpty.{w₁ + 1} p.R
Tactic: rw [free_def.{_, _, v}]
-- Lean 4 proof step from Mathlib.Algebra.Module.Presentation.RestrictScalars (goal)
Goal:
B : Type u_1
inst : Ring B
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module B M
inst_3 : DecidableEq B
presM : Presentation.{u_4, u_5, u_2, u_1} B M
inst_4 : DecidableEq presM.G
A : Type u_3
inst_5 : CommRing A
inst_6 : Algebra A B
inst_7 : Module A M
inst_8 : IsScalarTower A B M
presB : Presentation.{u_6, u_7, u_1, u_3} A B
data : presM.RestrictScalarsData presB
⊢ Eq (α := Submodule A (Finsupp.{u_5, u_1} presM.R B))
    (Submodule.span A
      (Set.range fun (x : Prod.{u_6, u_5} presB.G presM.R) ↦
        match (motive := Prod.{u_6, u_5} presB.G presM.R → Finsupp.{u_5, u_1} presM.R B) x with
        | (g, g') => HSMul.hSMul (β := Finsupp.{u_5, u_1} presM.R B) (presB.var g) (Finsupp.single g' 1)))
    ⊤
have h : ∀ (v : Finsupp.{u_5, u_1} presM.R B),
  Membership.mem (γ := Submodule A (Finsupp.{u_5, u_1} presM.R B))
      (Submodule.span A
        (Set.range fun (x : Prod.{u_6, u_5} presB.G presM.R) ↦
          match (motive := Prod.{u_6, u_5} presB.G presM.R → Finsupp.{u_5, u_1} presM.R B) x with
          | (g, g') => HSMul.hSMul (β := Finsupp.{u_5, u_1} presM.R B) (presB.var g) (Finsupp.single g' 1)))
      v ↔
    Membership.mem (γ := Submodule A (Finsupp.{u_5, u_1} presM.R B)) ⊤ v
Tactic: ext v
-- Lean 4 proof step from Mathlib.Algebra.Module.Presentation.RestrictScalars (goal)
Goal:
B : Type u_1
inst : Ring B
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module B M
inst_3 : DecidableEq B
presM : Presentation.{u_4, u_5, u_2, u_1} B M
inst_4 : DecidableEq presM.G
A : Type u_3
inst_5 : CommRing A
inst_6 : Algebra A B
inst_7 : Module A M
inst_8 : IsScalarTower A B M
presB : Presentation.{u_6, u_7, u_1, u_3} A B
data : presM.RestrictScalarsData presB
v : Finsupp.{u_5, u_1} presM.R B
⊢ Membership.mem (γ := Submodule A (Finsupp.{u_5, u_1} presM.R B))
      (Submodule.span A
        (Set.range fun (x : Prod.{u_6, u_5} presB.G presM.R) ↦
          HSMul.hSMul (β := Finsupp.{u_5, u_1} presM.R B) (presB.var x.1) (Finsupp.single x.2 1)))
      v ↔
    Membership.mem (γ := Submodule A (Finsupp.{u_5, u_1} presM.R B)) ⊤ v
have h : Membership.mem (γ := Submodule A (Finsupp.{u_5, u_1} presM.R B))
  (Submodule.span A
    (Set.range fun (x : Prod.{u_6, u_5} presB.G presM.R) ↦
      HSMul.hSMul (β := Finsupp.{u_5, u_1} presM.R B) (presB.var x.1) (Finsupp.single x.2 1)))
  v
Tactic: simp only [Submodule.mem_top, iff_true]
-- Lean 4 proof step from Mathlib.Algebra.Module.Presentation.RestrictScalars (goal)
Goal:
B : Type u_1
inst : Ring B
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module B M
inst_3 : DecidableEq B
presM : Presentation.{u_4, u_5, u_2, u_1} B M
inst_4 : DecidableEq presM.G
A : Type u_3
inst_5 : CommRing A
inst_6 : Algebra A B
inst_7 : Module A M
inst_8 : IsScalarTower A B M
presB : Presentation.{u_6, u_7, u_1, u_3} A B
data : presM.RestrictScalarsData presB
v : Finsupp.{u_5, u_1} presM.R B
⊢ Membership.mem (γ := Submodule A (Finsupp.{u_5, u_1} presM.R B))
    (Submodule.span A
      (Set.range fun (x : Prod.{u_6, u_5} presB.G presM.R) ↦
        HSMul.hSMul (β := Finsupp.{u_5, u_1} presM.R B) (presB.var x.1) (Finsupp.single x.2 1)))
    v
have h : Membership.mem (γ := Submodule A (Finsupp.{u_5, u_1} presM.R B))
  (Submodule.span A
    (Set.range
      fun
        (x :
          Prod.{u_6, u_5}
            (@Relations.G.{u_6, u_7, u_3} A inst_5.toRing (toRelations.{u_6, u_7, u_1, u_3} (M := B) presB))
            (@Relations.R.{u_4, u_5, u_1} B inst (toRelations.{u_4, u_5, u_2, u_1} (M := M) presM))) ↦
      HSMul.hSMul (β := Finsupp.{u_5, u_1} presM.R B) (presB.var x.1) (Finsupp.single x.2 1)))
  0
Tactic: apply Finsupp.induction