awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Module.Equiv.Defs (goal)
Goal:
R₁ : Type u_2
R₂ : Type u_3
M₁ : Type u_8
M₂ : Type u_9
inst : Semiring R₁
inst_1 : Semiring R₂
inst_2 : AddCommMonoid M₁
inst_3 : AddCommMonoid M₂
module_M₁ : Module R₁ M₁
module_M₂ : Module R₂ M₂
σ₁₂ : R₁ →+* R₂
σ₂₁ : R₂ →+* R₁
re₁₂ : RingHomInvPair σ₁₂ σ₂₁
re₂₁ : RingHomInvPair σ₂₁ σ₁₂
f : M₁ ≃ₛₗ[σ₁₂] M₂
⊢ f.trans f.symm = refl R₁ M₁
have h : ∀ (x : M₁), Eq (α := M₁) ((f.trans f.symm : (a : M₁) → M₁) x : M₁) ((refl R₁ M₁ : (a : M₁) → M₁) x : M₁)
Tactic: ext x
-- Lean 4 proof step from Mathlib.Algebra.Module.Equiv.Defs (goal)
Goal:
R₁ : Type u_2
R₂ : Type u_3
M₁ : Type u_8
M₂ : Type u_9
inst : Semiring R₁
inst_1 : Semiring R₂
inst_2 : AddCommMonoid M₁
inst_3 : AddCommMonoid M₂
module_M₁ : Module R₁ M₁
module_M₂ : Module R₂ M₂
σ₁₂ : R₁ →+* R₂
σ₂₁ : R₂ →+* R₁
re₁₂ : RingHomInvPair σ₁₂ σ₂₁
re₂₁ : RingHomInvPair σ₂₁ σ₁₂
f : M₁ ≃ₛₗ[σ₁₂] M₂
⊢ f.symm.trans f = refl R₂ M₂
have h : ∀ (x : M₂), Eq (α := M₂) ((f.symm.trans f : (a : M₂) → M₂) x : M₂) ((refl R₂ M₂ : (a : M₂) → M₂) x : M₂)
Tactic: ext x
-- Lean 4 proof step from Mathlib.Algebra.Module.Equiv.Defs (goal)
Goal:
R : Type u_1
R₁ : Type u_2
R₂ : Type u_3
R₃ : Type u_4
R₄ : Type u_5
S : Type u_6
M_1 : Type u_7
M₁ : Type u_8
M₂ : Type u_9
M₃ : Type u_10
M₄ : Type u_11
N₁ : Type u_12
N₂ : Type u_13
inst : Semiring R
inst_1 : Semiring S
ι : Type u_14
M : ι → Type u_15
inst_2 : (i : ι) → AddCommMonoid (M i)
inst_3 : (i : ι) → Module.{u_1, u_15} R (M i)
i j : ι
h : i = j
x : R
x_1 : M i
⊢ Equiv.toFun (AddEquiv.toEquiv (AddEquiv.cast (M := M) h : M i ≃+ M j)) (x • x_1) =
    HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) x : R)
      (Equiv.toFun (AddEquiv.toEquiv (AddEquiv.cast (M := M) h : M i ≃+ M j)) x_1)
have refl : Equiv.toFun (AddEquiv.toEquiv (AddEquiv.cast (M := M) sorry : M i ≃+ M i)) (x • x_1) =
  HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) x : R)
    (Equiv.toFun (AddEquiv.toEquiv (AddEquiv.cast (M := M) sorry : M i ≃+ M i)) x_1)
Tactic: cases h
Cleared hypotheses: j, h
-- Lean 4 proof step from Mathlib.Algebra.Module.Equiv.Defs (goal)
Goal:
S : Type u_14
R : Type u_15
V : Type u_16
W : Type u_17
G : Type u_18
inst : Semiring R
inst_1 : Semiring S
inst_2 : AddCommMonoid V
inst_3 : Module R V
inst_4 : Module S V
inst_5 : AddCommMonoid W
inst_6 : Module R W
inst_7 : Module S W
inst_8 : AddCommMonoid G
inst_9 : Module R G
inst_10 : Module S G
inst_11 : SMulCommClass R S W
inst_12 : SMul S R
inst_13 : IsScalarTower S R V
inst_14 : IsScalarTower S R W
inst_15 : SMulCommClass R S V
inst_16 : IsScalarTower S R G
α : Sˣ
e : G ≃ₗ[R] V
f : V ≃ₗ[R] W
⊢ (α • e) ≪≫ₗ f = HSMul.hSMul (β := G ≃ₗ[R] W) α (e ≪≫ₗ f)
have h : ∀ (x : G),
  Eq.{u_17 + 1} (α := W) (((α • e) ≪≫ₗ f : (a : G) → W) x : W)
    ((HSMul.hSMul (β := G ≃ₗ[R] W) α (e ≪≫ₗ f) : (a : G) → W) x : W)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Module.Equiv.Defs (goal)
Goal:
S : Type u_14
R : Type u_15
V : Type u_16
W : Type u_17
G : Type u_18
inst : Semiring R
inst_1 : Semiring S
inst_2 : AddCommMonoid V
inst_3 : Module R V
inst_4 : Module S V
inst_5 : AddCommMonoid W
inst_6 : Module R W
inst_7 : Module S W
inst_8 : AddCommMonoid G
inst_9 : Module R G
inst_10 : Module S G
inst_11 : SMulCommClass R S W
inst_12 : SMul S R
inst_13 : IsScalarTower S R V
inst_14 : IsScalarTower S R W
inst_15 : IsScalarTower S R G
α : Sˣ
e : G ≃ₗ[R] V
f : V ≃ₗ[R] W
⊢ e ≪≫ₗ (α • f) = HSMul.hSMul (β := G ≃ₗ[R] W) α (e ≪≫ₗ f)
have h : ∀ (x : G),
  Eq.{u_17 + 1} (α := W) ((e ≪≫ₗ (α • f) : (a : G) → W) x : W)
    ((HSMul.hSMul (β := G ≃ₗ[R] W) α (e ≪≫ₗ f) : (a : G) → W) x : W)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Module.Equiv.Opposite (goal)
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : Semiring S
inst_2 : AddCommMonoid M
inst_3 : Module S M
σ : RingHom.{u_1, u_2} Rᵐᵒᵖ S
f g : LinearMap.{u_1, u_2, u_1, u_3} (R := Rᵐᵒᵖ) (S := S) σ R M
h : Eq.{u_3 + 1} (α := M) ((f : (a : R) → M) 1 : M) ((g : (a : R) → M) 1 : M)
x : R
⊢ Eq.{u_3 + 1} (α := M) ((f : (a : R) → M) x : M) ((g : (a : R) → M) x : M)
have rw : Eq.{u_3 + 1} (α := M) ((f : (a : R) → M) (1 * x) : M) ((g : (a : R) → M) (1 * x) : M)
Tactic: rw [← one_mul x, ← op_smul_eq_mul, f.map_smulₛₗ, h, g.map_smulₛₗ]
-- Lean 4 proof step from Mathlib.Algebra.Module.Equiv.Opposite (goal)
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : Semiring S
inst_2 : AddCommMonoid M
inst_3 : Module S M
σ : RingHom.{u_1, u_2} Rᵐᵒᵖ S
f g : LinearMap.{u_1, u_2, u_1, u_3} (R := Rᵐᵒᵖ) (S := S) σ R M
h : Eq.{u_3 + 1} (α := M) ((f : (a : R) → M) 1 : M) ((g : (a : R) → M) 1 : M)
x : R
rw : Eq.{u_3 + 1} (α := M) ((f : (a : R) → M) (1 * x) : M) ((g : (a : R) → M) (1 * x) : M)
⊢ Eq.{u_3 + 1} (α := M) ((f : (a : R) → M) x : M) ((g : (a : R) → M) x : M)
have rw₁ : Eq.{u_3 + 1} (α := M) ((f : (a : R) → M) (HSMul.hSMul (β := R) (MulOpposite.op x) 1) : M)
  ((g : (a : R) → M) (HSMul.hSMul (β := R) (MulOpposite.op x) 1) : M)
Tactic: rw [← one_mul x, ← op_smul_eq_mul, f.map_smulₛₗ, h, g.map_smulₛₗ]
-- Lean 4 proof step from Mathlib.Algebra.Module.Equiv.Opposite (goal)
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : Semiring S
inst_2 : AddCommMonoid M
inst_3 : Module S M
σ : RingHom.{u_1, u_2} Rᵐᵒᵖ S
f g : LinearMap.{u_1, u_2, u_1, u_3} (R := Rᵐᵒᵖ) (S := S) σ R M
h : Eq.{u_3 + 1} (α := M) ((f : (a : R) → M) 1 : M) ((g : (a : R) → M) 1 : M)
x : R
rw : Eq.{u_3 + 1} (α := M) ((f : (a : R) → M) (1 * x) : M) ((g : (a : R) → M) (1 * x) : M)
rw₁ :
  Eq.{u_3 + 1} (α := M) ((f : (a : R) → M) (HSMul.hSMul (β := R) (MulOpposite.op x) 1) : M)
    ((g : (a : R) → M) (HSMul.hSMul (β := R) (MulOpposite.op x) 1) : M)
⊢ Eq.{u_3 + 1} (α := M) ((f : (a : R) → M) x : M) ((g : (a : R) → M) x : M)
have rw₂ : HSMul.hSMul.{u_2, u_3, u_3} (α := S) (β := M) ((σ : (a : Rᵐᵒᵖ) → S) (MulOpposite.op x) : S) ((f : (a : R) → M) 1 : M) =
  (g : (a : R) → M) (HSMul.hSMul (β := R) (MulOpposite.op x) 1)
Tactic: rw [← one_mul x, ← op_smul_eq_mul, f.map_smulₛₗ, h, g.map_smulₛₗ]
-- Lean 4 proof step from Mathlib.Algebra.Module.Equiv.Opposite (goal)
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : Semiring S
inst_2 : AddCommMonoid M
inst_3 : Module S M
σ : RingHom.{u_1, u_2} Rᵐᵒᵖ S
f g : LinearMap.{u_1, u_2, u_1, u_3} (R := Rᵐᵒᵖ) (S := S) σ R M
h : Eq.{u_3 + 1} (α := M) ((f : (a : R) → M) 1 : M) ((g : (a : R) → M) 1 : M)
x : R
rw : Eq.{u_3 + 1} (α := M) ((f : (a : R) → M) (1 * x) : M) ((g : (a : R) → M) (1 * x) : M)
rw₁ :
  Eq.{u_3 + 1} (α := M) ((f : (a : R) → M) (HSMul.hSMul (β := R) (MulOpposite.op x) 1) : M)
    ((g : (a : R) → M) (HSMul.hSMul (β := R) (MulOpposite.op x) 1) : M)
rw₂ :
  HSMul.hSMul.{u_2, u_3, u_3} (α := S) (β := M) ((σ : (a : Rᵐᵒᵖ) → S) (MulOpposite.op x) : S)
      ((f : (a : R) → M) 1 : M) =
    (g : (a : R) → M) (HSMul.hSMul (β := R) (MulOpposite.op x) 1)
⊢ Eq.{u_3 + 1} (α := M) ((f : (a : R) → M) x : M) ((g : (a : R) → M) x : M)
have rw₃ : HSMul.hSMul.{u_2, u_3, u_3} (α := S) (β := M) ((σ : (a : Rᵐᵒᵖ) → S) (MulOpposite.op x) : S) ((g : (a : R) → M) 1 : M) =
  (g : (a : R) → M) (HSMul.hSMul (β := R) (MulOpposite.op x) 1)
Tactic: rw [← one_mul x, ← op_smul_eq_mul, f.map_smulₛₗ, h, g.map_smulₛₗ]
-- Lean 4 proof step from Mathlib.Algebra.Module.Equiv.Opposite (goal)
Goal:
R : Type u_1
S : Type u_2
M : Type u_3
inst : Semiring R
inst_1 : Semiring S
inst_2 : AddCommMonoid M
inst_3 : Module S M
σ : RingHom.{u_1, u_2} Rᵐᵒᵖ S
f g : LinearMap.{u_1, u_2, u_1, u_3} (R := Rᵐᵒᵖ) (S := S) σ R M
h : Eq.{u_3 + 1} (α := M) ((f : (a : R) → M) 1 : M) ((g : (a : R) → M) 1 : M)
x : R
rw : Eq.{u_3 + 1} (α := M) ((f : (a : R) → M) (1 * x) : M) ((g : (a : R) → M) (1 * x) : M)
rw₁ :
  Eq.{u_3 + 1} (α := M) ((f : (a : R) → M) (HSMul.hSMul (β := R) (MulOpposite.op x) 1) : M)
    ((g : (a : R) → M) (HSMul.hSMul (β := R) (MulOpposite.op x) 1) : M)
rw₂ :
  HSMul.hSMul.{u_2, u_3, u_3} (α := S) (β := M) ((σ : (a : Rᵐᵒᵖ) → S) (MulOpposite.op x) : S)
      ((f : (a : R) → M) 1 : M) =
    (g : (a : R) → M) (HSMul.hSMul (β := R) (MulOpposite.op x) 1)
rw₃ :
  HSMul.hSMul.{u_2, u_3, u_3} (α := S) (β := M) ((σ : (a : Rᵐᵒᵖ) → S) (MulOpposite.op x) : S)
      ((g : (a : R) → M) 1 : M) =
    (g : (a : R) → M) (HSMul.hSMul (β := R) (MulOpposite.op x) 1)
⊢ Eq.{u_3 + 1} (α := M) ((f : (a : R) → M) x : M) ((g : (a : R) → M) x : M)
have rw₄ : HSMul.hSMul.{u_2, u_3, u_3} (α := S) (β := M) ((σ : (a : Rᵐᵒᵖ) → S) (MulOpposite.op x) : S) ((g : (a : R) → M) 1 : M) =
  HSMul.hSMul.{u_2, u_3, u_3} (α := S) (β := M) ((σ : (a : Rᵐᵒᵖ) → S) (MulOpposite.op x) : S) ((g : (a : R) → M) 1 : M)
Tactic: rw [← one_mul x, ← op_smul_eq_mul, f.map_smulₛₗ, h, g.map_smulₛₗ]
-- Lean 4 proof step from Mathlib.Algebra.Module.FinitePresentation (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
h : Module.FinitePresentation R M
⊢ Module.Finite R M
have obtain : ∀ (s : Finset M) (hs₁ : Eq (α := Submodule R M) (Submodule.span R (↑s : Set M)) ⊤),
  Submodule.FG (M := Finsupp.{u_2, u_1} (↥s) R)
      (LinearMap.ker (linearCombination R (Subtype.val (p := fun (x : M) ↦ x ∈ s)))) →
    Module.Finite R M
Tactic: obtain ⟨s, hs₁, _⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Module.FinitePresentation (goal)
Goal:
R : Type u
M : Type u_1
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
fp : FinitePresentation R M
ι : Finset M
hι₁ : Eq (α := Submodule R M) (Submodule.span R (↑ι : Set M)) ⊤
hι₂ :
  Submodule.FG (M := Finsupp.{u_1, u} (↥ι) R)
    (LinearMap.ker (linearCombination R (Subtype.val (p := fun (x : M) ↦ x ∈ ι))))
⊢ ∃ (n : ℕ) (K : Submodule R (Fin n → R)) (x : M ≃ₗ[R] (Fin n → R) ⧸ K), K.FG
have refine_1 : Eq (α := Submodule R M)
  (LinearMap.range
    (linearCombination R (Subtype.val (p := fun (x : M) ↦ x ∈ ι)) ∘ₗ
      (↑(LinearEquiv.symm (lcongr ι.equivFin (LinearEquiv.refl R R) ≪≫ₗ linearEquivFunOnFinite R R (Fin ι.card))) :
        (Fin ι.card → R) →ₗ[R] ↥ι →₀ R)))
  ⊤
Tactic: refine ⟨_, LinearMap.ker (linearCombination R Subtype.val ∘ₗ
    (lcongr ι.equivFin (.refl ..) ≪≫ₗ linearEquivFunOnFinite R R _).symm.toLinearMap),
    (LinearMap.quotKerEquivOfSurjective _ <| LinearMap.range_eq_top.mp ?_).symm, ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Module.FinitePresentation (goal)
Goal:
R : Type u
M : Type u_1
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
fp : FinitePresentation R M
ι : Finset M
hι₁ : Eq (α := Submodule R M) (Submodule.span R (↑ι : Set M)) ⊤
hι₂ :
  Submodule.FG (M := Finsupp.{u_1, u} (↥ι) R)
    (LinearMap.ker (linearCombination R (Subtype.val (p := fun (x : M) ↦ x ∈ ι))))
refine_1 :
  Eq (α := Submodule R M)
    (LinearMap.range
      (linearCombination R (Subtype.val (p := fun (x : M) ↦ x ∈ ι)) ∘ₗ
        (↑(LinearEquiv.symm (lcongr ι.equivFin (LinearEquiv.refl R R) ≪≫ₗ linearEquivFunOnFinite R R (Fin ι.card))) :
          (Fin ι.card → R) →ₗ[R] ↥ι →₀ R)))
    ⊤
⊢ ∃ (n : ℕ) (K : Submodule R (Fin n → R)) (x : M ≃ₗ[R] (Fin n → R) ⧸ K), K.FG
have refine_2 : (LinearMap.ker
    (linearCombination R (Subtype.val (p := fun (x : M) ↦ x ∈ ι)) ∘ₗ
      (↑(LinearEquiv.symm (lcongr ι.equivFin (LinearEquiv.refl R R) ≪≫ₗ linearEquivFunOnFinite R R (Fin ι.card))) :
        (Fin ι.card → R) →ₗ[R] ↥ι →₀ R))).FG
Tactic: refine ⟨_, LinearMap.ker (linearCombination R Subtype.val ∘ₗ
    (lcongr ι.equivFin (.refl ..) ≪≫ₗ linearEquivFunOnFinite R R _).symm.toLinearMap),
    (LinearMap.quotKerEquivOfSurjective _ <| LinearMap.range_eq_top.mp ?_).symm, ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Module.FinitePresentation (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsNoetherianRing R
h : Module.Finite R M
⊢ FinitePresentation R M
have obtain : ∀ (s : Finset M) (hs : Eq (α := Submodule R M) (Submodule.span R (↑s : Set M)) ⊤), FinitePresentation R M
Tactic: obtain ⟨s, hs⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Module.FinitePresentation (goal)
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : Free R M
inst_6 : Module.Finite R M
l : M →ₗ[R] N
hl : Function.Surjective.{u_2 + 1, u_3 + 1} (α := M) (β := N) (⇑l : (a : M) → N)
hl' : l.ker.FG
b : Basis (Free.ChooseBasisIndex R M) R M := Free.chooseBasis R M
π : Free.ChooseBasisIndex R M →
  ↥(Set.Finite.toFinset (s :=
      Set.range.{u_3, u_2 + 1} (ι := Free.ChooseBasisIndex R M)
        (Function.comp (β := M) (⇑l : (a : M) → N) (⇑b : (a : Free.ChooseBasisIndex R M) → M)))
      ⋯) :=
  fun (i : Free.ChooseBasisIndex R M) ↦
    Subtype.mk (p := fun (x : N) ↦
      Membership.mem (γ := Finset N)
        (Set.Finite.toFinset (s :=
          Set.range.{u_3, u_2 + 1} (ι := Free.ChooseBasisIndex R M)
            (Function.comp (β := M) (⇑l : (a : M) → N) (⇑b : (a : Free.ChooseBasisIndex R M) → M)))
          ⋯)
        x)
      ((l : (a : M) → N) ((b : (a : Free.ChooseBasisIndex R M) → M) i : M)) ⋯
x_1 :
  ↥(Set.Finite.toFinset (s :=
      Set.range.{u_3, u_2 + 1} (ι := Free.ChooseBasisIndex R M)
        (Function.comp (β := M) (⇑l : (a : M) → N) (⇑b : (a : Free.ChooseBasisIndex R M) → M)))
      ⋯)
x : N
hx :
  Membership.mem (γ := Finset N)
    (Set.Finite.toFinset (s :=
      Set.range.{u_3, u_2 + 1} (ι := Free.ChooseBasisIndex R M)
        (Function.comp (β := M) (⇑l : (a : M) → N) (⇑b : (a : Free.ChooseBasisIndex R M) → M)))
      ⋯)
    x
⊢ ∃ (a : Free.ChooseBasisIndex R M),
    π a =
      Subtype.mk (p := fun (x : N) ↦
        Membership.mem (γ := Finset N)
          (Set.Finite.toFinset (s :=
            Set.range.{u_3, u_2 + 1} (ι := Free.ChooseBasisIndex R M)
              (Function.comp (β := M) (⇑l : (a : M) → N) (⇑b : (a : Free.ChooseBasisIndex R M) → M)))
            ⋯)
          x)
        x hx
have obtain : ∀ (y : Free.ChooseBasisIndex R M)
  (hx :
    Membership.mem.{u_3, u_3} (α := N) (γ := Finset N)
      (Set.Finite.toFinset (s :=
        Set.range.{u_3, u_2 + 1} (ι := Free.ChooseBasisIndex R M)
          (Function.comp (β := M) (⇑l : (a : M) → N) (⇑b : (a : Free.ChooseBasisIndex R M) → M)))
        sorry)
      ((l : (a : M) → N) ((b : (a : Free.ChooseBasisIndex R M) → M) y : M) : N)),
  ∃ (a : Free.ChooseBasisIndex R M),
    π a =
      Subtype.mk (p := fun (x : N) ↦
        Membership.mem (γ := Finset N)
          (Set.Finite.toFinset (s :=
            Set.range.{u_3, u_2 + 1} (ι := Free.ChooseBasisIndex R M)
              (Function.comp (β := M) (⇑l : (a : M) → N) (⇑b : (a : Free.ChooseBasisIndex R M) → M)))
            sorry)
          x)
        ((l : (a : M) → N) ((b : (a : Free.ChooseBasisIndex R M) → M) y : M)) hx
Tactic: obtain ⟨y, rfl⟩ : ∃ a, l (b a) = x := by simpa using hx
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.Algebra.Module.FinitePresentation (goal)
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : Free R M
inst_6 : Module.Finite R M
l : M →ₗ[R] N
hl : Function.Surjective.{u_2 + 1, u_3 + 1} (α := M) (β := N) (⇑l : (a : M) → N)
hl' : l.ker.FG
b : Basis (Free.ChooseBasisIndex R M) R M := Free.chooseBasis R M
π : Free.ChooseBasisIndex R M →
  ↥(Set.Finite.toFinset (s :=
      Set.range.{u_3, u_2 + 1} (ι := Free.ChooseBasisIndex R M)
        (Function.comp (β := M) (⇑l : (a : M) → N) (⇑b : (a : Free.ChooseBasisIndex R M) → M)))
      ⋯) :=
  fun (i : Free.ChooseBasisIndex R M) ↦
    Subtype.mk (p := fun (x : N) ↦
      Membership.mem (γ := Finset N)
        (Set.Finite.toFinset (s :=
          Set.range.{u_3, u_2 + 1} (ι := Free.ChooseBasisIndex R M)
            (Function.comp (β := M) (⇑l : (a : M) → N) (⇑b : (a : Free.ChooseBasisIndex R M) → M)))
          ⋯)
        x)
      ((l : (a : M) → N) ((b : (a : Free.ChooseBasisIndex R M) → M) i : M)) ⋯
this : Function.Surjective π
⊢ FinitePresentation R N
have choose : ∀
  (σ :
    (b :
        ↥(Set.Finite.toFinset (s :=
            Set.range.{u_3, u_2 + 1} (ι := Free.ChooseBasisIndex R M)
              (Function.comp (β := M) (⇑l : (a : M) → N) (⇑b : (a : Free.ChooseBasisIndex R M) → M)))
            sorry)) →
      Free.ChooseBasisIndex R M)
  (hσ :
    ∀
      (b_1 :
        ↥(Set.Finite.toFinset (s :=
            Set.range.{u_3, u_2 + 1} (ι := Free.ChooseBasisIndex R M)
              (Function.comp (β := M) (⇑l : (a : M) → N) (⇑b : (a : Free.ChooseBasisIndex R M) → M)))
            sorry)),
      π (σ b_1) = b_1),
  FinitePresentation R N
Tactic: choose σ hσ using this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Algebra.Module.FinitePresentation (hypothesis)
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : Free R M
inst_6 : Module.Finite R M
l : M →ₗ[R] N
hl : Function.Surjective.{u_2 + 1, u_3 + 1} (α := M) (β := N) (⇑l : (a : M) → N)
hl' : l.ker.FG
b : Basis (Free.ChooseBasisIndex R M) R M := Free.chooseBasis R M
π : Free.ChooseBasisIndex R M →
  ↥(Set.Finite.toFinset (s :=
      Set.range.{u_3, u_2 + 1} (ι := Free.ChooseBasisIndex R M)
        (Function.comp (β := M) (⇑l : (a : M) → N) (⇑b : (a : Free.ChooseBasisIndex R M) → M)))
      ⋯) :=
  fun (i : Free.ChooseBasisIndex R M) ↦
    Subtype.mk (p := fun (x : N) ↦
      Membership.mem (γ := Finset N)
        (Set.Finite.toFinset (s :=
          Set.range.{u_3, u_2 + 1} (ι := Free.ChooseBasisIndex R M)
            (Function.comp (β := M) (⇑l : (a : M) → N) (⇑b : (a : Free.ChooseBasisIndex R M) → M)))
          ⋯)
        x)
      ((l : (a : M) → N) ((b : (a : Free.ChooseBasisIndex R M) → M) i : M)) ⋯
σ :
  (b :
      ↥(Set.Finite.toFinset (s :=
          Set.range.{u_3, u_2 + 1} (ι := Free.ChooseBasisIndex R M)
            (Function.comp (β := M) (⇑l : (a : M) → N) (⇑b : (a : Free.ChooseBasisIndex R M) → M)))
          ⋯)) →
    Free.ChooseBasisIndex R M
hσ :
  ∀
    (b_1 :
      ↥(Set.Finite.toFinset (s :=
          Set.range.{u_3, u_2 + 1} (ι := Free.ChooseBasisIndex R M)
            (Function.comp (β := M) (⇑l : (a : M) → N) (⇑b : (a : Free.ChooseBasisIndex R M) → M)))
          ⋯)),
    π (σ b_1) = b_1
⊢ FinitePresentation R N
have hπ : Subtype.val (p := fun (x : N) ↦
      Membership.mem (γ := Finset N)
        (Set.Finite.toFinset (s :=
          Set.range.{u_3, u_2 + 1} (ι := Free.ChooseBasisIndex R M)
            (Function.comp (β := M) (⇑l : (a : M) → N) (⇑b : (a : Free.ChooseBasisIndex R M) → M)))
          sorry)
        x) ∘
    π =
  Function.comp (β := M) (⇑l : (a : M) → N) (⇑b : (a : Free.ChooseBasisIndex R M) → M)
Tactic: have hπ : Subtype.val ∘ π = l ∘ b := rfl
-- Lean 4 proof step from Mathlib.Algebra.Module.FinitePresentation (goal)
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : Free R M
inst_6 : Module.Finite R M
l : M →ₗ[R] N
hl : Function.Surjective.{u_2 + 1, u_3 + 1} (α := M) (β := N) (⇑l : (a : M) → N)
hl' : l.ker.FG
b : Basis (Free.ChooseBasisIndex R M) R M := Free.chooseBasis R M
π : Free.ChooseBasisIndex R M →
  ↥(Set.Finite.toFinset (s :=
      Set.range.{u_3, u_2 + 1} (ι := Free.ChooseBasisIndex R M)
        (Function.comp (β := M) (⇑l : (a : M) → N) (⇑b : (a : Free.ChooseBasisIndex R M) → M)))
      ⋯) :=
  fun (i : Free.ChooseBasisIndex R M) ↦
    Subtype.mk (p := fun (x : N) ↦
      Membership.mem (γ := Finset N)
        (Set.Finite.toFinset (s :=
          Set.range.{u_3, u_2 + 1} (ι := Free.ChooseBasisIndex R M)
            (Function.comp (β := M) (⇑l : (a : M) → N) (⇑b : (a : Free.ChooseBasisIndex R M) → M)))
          ⋯)
        x)
      ((l : (a : M) → N) ((b : (a : Free.ChooseBasisIndex R M) → M) i : M)) ⋯
σ :
  (b :
      ↥(Set.Finite.toFinset (s :=
          Set.range.{u_3, u_2 + 1} (ι := Free.ChooseBasisIndex R M)
            (Function.comp (β := M) (⇑l : (a : M) → N) (⇑b : (a : Free.ChooseBasisIndex R M) → M)))
          ⋯)) →
    Free.ChooseBasisIndex R M
hσ :
  ∀
    (b_1 :
      ↥(Set.Finite.toFinset (s :=
          Set.range.{u_3, u_2 + 1} (ι := Free.ChooseBasisIndex R M)
            (Function.comp (β := M) (⇑l : (a : M) → N) (⇑b : (a : Free.ChooseBasisIndex R M) → M)))
          ⋯)),
    π (σ b_1) = b_1
hπ :
  Subtype.val (p := fun (x : N) ↦
        Membership.mem (γ := Finset N)
          (Set.Finite.toFinset (s :=
            Set.range.{u_3, u_2 + 1} (ι := Free.ChooseBasisIndex R M)
              (Function.comp (β := M) (⇑l : (a : M) → N) (⇑b : (a : Free.ChooseBasisIndex R M) → M)))
            ⋯)
          x) ∘
      π =
    Function.comp (β := M) (⇑l : (a : M) → N) (⇑b : (a : Free.ChooseBasisIndex R M) → M)
⊢ π ∘ σ = id
have h : ∀
  (i :
    ↥(Set.Finite.toFinset (s :=
        Set.range.{u_3, u_2 + 1} (ι := Free.ChooseBasisIndex R M)
          (Function.comp (β := M) (⇑l : (a : M) → N) (⇑b : (a : Free.ChooseBasisIndex R M) → M)))
        sorry)),
  (↑((π ∘ σ) i) : N) = (↑(id i) : N)
Tactic: ext i
-- Lean 4 proof step from Mathlib.Algebra.Module.FinitePresentation (hypothesis)
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : Free R M
inst_6 : Module.Finite R M
l : M →ₗ[R] N
hl : Function.Surjective.{u_2 + 1, u_3 + 1} (α := M) (β := N) (⇑l : (a : M) → N)
hl' : l.ker.FG
b : Basis (Free.ChooseBasisIndex R M) R M := Free.chooseBasis R M
π : Free.ChooseBasisIndex R M →
  ↥(Set.Finite.toFinset (s :=
      Set.range.{u_3, u_2 + 1} (ι := Free.ChooseBasisIndex R M)
        (Function.comp (β := M) (⇑l : (a : M) → N) (⇑b : (a : Free.ChooseBasisIndex R M) → M)))
      ⋯) :=
  fun (i : Free.ChooseBasisIndex R M) ↦
    Subtype.mk (p := fun (x : N) ↦
      Membership.mem (γ := Finset N)
        (Set.Finite.toFinset (s :=
          Set.range.{u_3, u_2 + 1} (ι := Free.ChooseBasisIndex R M)
            (Function.comp (β := M) (⇑l : (a : M) → N) (⇑b : (a : Free.ChooseBasisIndex R M) → M)))
          ⋯)
        x)
      ((l : (a : M) → N) ((b : (a : Free.ChooseBasisIndex R M) → M) i : M)) ⋯
σ :
  (b :
      ↥(Set.Finite.toFinset (s :=
          Set.range.{u_3, u_2 + 1} (ι := Free.ChooseBasisIndex R M)
            (Function.comp (β := M) (⇑l : (a : M) → N) (⇑b : (a : Free.ChooseBasisIndex R M) → M)))
          ⋯)) →
    Free.ChooseBasisIndex R M
hσ :
  ∀
    (b_1 :
      ↥(Set.Finite.toFinset (s :=
          Set.range.{u_3, u_2 + 1} (ι := Free.ChooseBasisIndex R M)
            (Function.comp (β := M) (⇑l : (a : M) → N) (⇑b : (a : Free.ChooseBasisIndex R M) → M)))
          ⋯)),
    π (σ b_1) = b_1
hπ :
  Subtype.val (p := fun (x : N) ↦
        Membership.mem (γ := Finset N)
          (Set.Finite.toFinset (s :=
            Set.range.{u_3, u_2 + 1} (ι := Free.ChooseBasisIndex R M)
              (Function.comp (β := M) (⇑l : (a : M) → N) (⇑b : (a : Free.ChooseBasisIndex R M) → M)))
            ⋯)
          x) ∘
      π =
    Function.comp (β := M) (⇑l : (a : M) → N) (⇑b : (a : Free.ChooseBasisIndex R M) → M)
⊢ FinitePresentation R N
have hσ₁ : π ∘ σ = id
Tactic: have hσ₁ : π ∘ σ = id := by ext i; exact congr_arg Subtype.val (hσ i)