awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Module.SpanRankOperations
Goal:
R : Type u_1
inst : CommRing R
M : Type u_3
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Submodule R M
inst_3 : IsLocalRing R
fg : N.FG
this : Module.Finite.{u_1, u_3} R ↥N := ⋯
s : Set (TensorProduct.{u_1, u_1, u_3} R 𝓀 ↥N)
hs₁ : Cardinal.mk (↑s : Type (max u_1 u_3)) = spanRank (R := 𝓀) (M := TensorProduct.{u_1, u_1, u_3} R 𝓀 ↥N) ⊤
hs₂ : Eq (α := Submodule 𝓀 (TensorProduct.{u_1, u_1, u_3} R 𝓀 ↥N)) (span 𝓀 s) ⊤
hs₃ : s.Finite
t : Set ↥N := Function.surjInv ⋯ '' s
ht₁ : (⇑((mk R 𝓀 ↥N : (a : 𝓀) → ↥N →ₗ[R] 𝓀 ⊗[R] ↥N) 1) : (a : ↥N) → 𝓀 ⊗[R] ↥N) '' t = s
rwa :
  ∀ (hs₂ : Eq (α := Submodule R (TensorProduct.{u_1, u_1, u_3} R 𝓀 ↥N)) (restrictScalars R (R := 𝓀) (span 𝓀 s)) ⊤)
    (hs₃ : s.Finite),
    let t := Function.surjInv ⋯ '' s;
    ∀ (ht₁ : (⇑((mk R 𝓀 ↥N : (a : 𝓀) → ↥N →ₗ[R] 𝓀 ⊗[R] ↥N) 1) : (a : ↥N) → 𝓀 ⊗[R] ↥N) '' t = s),
      Eq (α := Submodule R ↥N) (span R t) ⊤
rwa₁ :
  ∀ (hs₂ : Eq (α := Submodule R (TensorProduct.{u_1, u_1, u_3} R 𝓀 ↥N)) (span R s) ⊤) (hs₃ : s.Finite),
    let t := Function.surjInv ⋯ '' s;
    ∀ (ht₁ : (⇑((mk R 𝓀 ↥N : (a : 𝓀) → ↥N →ₗ[R] 𝓀 ⊗[R] ↥N) 1) : (a : ↥N) → 𝓀 ⊗[R] ↥N) '' t = s),
      Eq (α := Submodule R ↥N) (span R t) ⊤
rwa₂ :
  ∀ (hs₃ : s.Finite),
    let t := Function.surjInv ⋯ '' s;
    ∀
      (hs₂ :
        Eq (α := Submodule R (TensorProduct.{u_1, u_1, u_3} R 𝓀 ↥N))
          (span R ((⇑((mk R 𝓀 ↥N : (a : 𝓀) → ↥N →ₗ[R] 𝓀 ⊗[R] ↥N) 1) : (a : ↥N) → 𝓀 ⊗[R] ↥N) '' t)) ⊤)
      (ht₁ : (⇑((mk R 𝓀 ↥N : (a : 𝓀) → ↥N →ₗ[R] 𝓀 ⊗[R] ↥N) 1) : (a : ↥N) → 𝓀 ⊗[R] ↥N) '' t = s),
      Eq (α := Submodule R ↥N) (span R t) ⊤
rwa₃ :
  ∀ (hs₃ : s.Finite),
    let t := Function.surjInv ⋯ '' s;
    ∀
      (hs₂ :
        Eq (α := Submodule R (TensorProduct.{u_1, u_1, u_3} R 𝓀 ↥N))
          (Submodule.map (σ₁₂ := RingHom.id R) ((mk R 𝓀 ↥N : (a : 𝓀) → ↥N →ₗ[R] 𝓀 ⊗[R] ↥N) 1) (span R t)) ⊤)
      (ht₁ : (⇑((mk R 𝓀 ↥N : (a : 𝓀) → ↥N →ₗ[R] 𝓀 ⊗[R] ↥N) 1) : (a : ↥N) → 𝓀 ⊗[R] ↥N) '' t = s),
      Eq (α := Submodule R ↥N) (span R t) ⊤
rwa₄ rwa₅ rwa₆ rwa₇ :
  ∀ (hs₃ : s.Finite),
    let t := Function.surjInv ⋯ '' s;
    ∀ (hs₂ : Eq (α := Submodule R ↥N) (span R t) ⊤)
      (ht₁ : (⇑((mk R 𝓀 ↥N : (a : 𝓀) → ↥N →ₗ[R] 𝓀 ⊗[R] ↥N) 1) : (a : ↥N) → 𝓀 ⊗[R] ↥N) '' t = s),
      Eq (α := Submodule R ↥N) (span R t) ⊤
⊢ Eq (α := Submodule R ↥N) (span R t) ⊤

Tactic:
rwa [← restrictScalars_eq_top_iff R, restrictScalars_span _ _ (by exact residue_surjective),
      ← ht₁, ← map_span, map_tensorProduct_mk_eq_top] at hs₂

Premises used: IsLocalRing.map_tensorProduct_mk_eq_top, Submodule.map_span, Submodule.restrictScalars_eq_top_iff, Submodule.restrictScalars_span
-- Module: Mathlib.Algebra.Module.SpanRankOperations
Goal:
R : Type u_1
inst : CommRing R
M : Type u_3
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Submodule R M
inst_3 : IsLocalRing R
fg : N.FG
this : Module.Finite.{u_1, u_3} R ↥N := ⋯
s : Set (TensorProduct.{u_1, u_1, u_3} R 𝓀 ↥N)
hs₁ : Cardinal.mk (↑s : Type (max u_1 u_3)) = spanRank (R := 𝓀) (M := TensorProduct.{u_1, u_1, u_3} R 𝓀 ↥N) ⊤
hs₂ : Eq (α := Submodule 𝓀 (TensorProduct.{u_1, u_1, u_3} R 𝓀 ↥N)) (span 𝓀 s) ⊤
hs₃ : s.Finite
t : Set ↥N := Function.surjInv ⋯ '' s
ht₁ : (⇑((mk R 𝓀 ↥N : (a : 𝓀) → ↥N →ₗ[R] 𝓀 ⊗[R] ↥N) 1) : (a : ↥N) → 𝓀 ⊗[R] ↥N) '' t = s
⊢ Eq (α := Submodule R ↥N) (span R t) ⊤

Tactic:
have ht₂ : span R t = ⊤ := by
    rwa [← restrictScalars_eq_top_iff R, restrictScalars_span _ _ (by exact residue_surjective),
      ← ht₁, ← map_span, map_tensorProduct_mk_eq_top] at hs₂
-- Module: Mathlib.Algebra.Module.SpanRankOperations
Goal:
R : Type u_1
inst : CommRing R
M : Type u_3
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Submodule R M
inst_3 : IsLocalRing R
fg : N.FG
this : Module.Finite.{u_1, u_3} R ↥N := ⋯
s : Set (TensorProduct.{u_1, u_1, u_3} R 𝓀 ↥N)
hs₁ : Cardinal.mk (↑s : Type (max u_1 u_3)) = spanRank (R := 𝓀) (M := TensorProduct.{u_1, u_1, u_3} R 𝓀 ↥N) ⊤
hs₂ : Eq (α := Submodule 𝓀 (TensorProduct.{u_1, u_1, u_3} R 𝓀 ↥N)) (span 𝓀 s) ⊤
hs₃ : s.Finite
t : Set ↥N := Function.surjInv ⋯ '' s
ht₁ : (⇑((mk R 𝓀 ↥N : (a : 𝓀) → ↥N →ₗ[R] 𝓀 ⊗[R] ↥N) 1) : (a : ↥N) → 𝓀 ⊗[R] ↥N) '' t = s
ht₂ : Eq (α := Submodule R ↥N) (span R t) ⊤
grw : s.ncard ≤ s.ncard
⊢ N.spanFinrank ≤ spanFinrank (R := 𝓀) (M := TensorProduct.{u_1, u_1, u_3} R 𝓀 ↥N) ⊤

Tactic:
grw [← N.spanFinrank_top, ← ht₂, spanFinrank_span_le_ncard_of_finite (hs₃.image _), spanFinrank,
    ← hs₁, Set.ncard_image_le hs₃]

Premises used: Set.ncard_image_le, Submodule.spanFinrank_span_le_ncard_of_finite, Set.Finite.image, Submodule.spanFinrank, Submodule.spanFinrank_top
-- Module: Mathlib.Algebra.Module.SpanRankOperations
Goal:
R : Type u_1
inst : CommRing R
M : Type u_3
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Submodule R M
inst_3 : IsLocalRing R
fg : N.FG
this : Module.Finite.{u_1, u_3} R ↥N := ⋯
s : Set (TensorProduct.{u_1, u_1, u_3} R 𝓀 ↥N)
hs₁ : Cardinal.mk (↑s : Type (max u_1 u_3)) = spanRank (R := 𝓀) (M := TensorProduct.{u_1, u_1, u_3} R 𝓀 ↥N) ⊤
hs₂ : Eq (α := Submodule 𝓀 (TensorProduct.{u_1, u_1, u_3} R 𝓀 ↥N)) (span 𝓀 s) ⊤
hs₃ : s.Finite
t : Set ↥N := Function.surjInv ⋯ '' s
ht₁ : (⇑((mk R 𝓀 ↥N : (a : 𝓀) → ↥N →ₗ[R] 𝓀 ⊗[R] ↥N) 1) : (a : ↥N) → 𝓀 ⊗[R] ↥N) '' t = s
ht₂ : Eq (α := Submodule R ↥N) (span R t) ⊤
⊢ s.ncard ≤ s.ncard

Tactic:
rfl
-- Module: Mathlib.Algebra.Module.SpanRankOperations
Goal:
R : Type u_1
inst : CommRing R
M : Type u_3
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsLocalRing R
N : Submodule R M
fg : N.FG
this_1 : Module.{u_1, u_3} 𝓀 (↥N ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R ↥N) (maximalIdeal R) ⊤) :=
  { smul := spanFinrank_eq_finrank_quotient._aux_1 N, mul_smul := ⋯, one_smul := ⋯, smul_zero := ⋯, smul_add := ⋯,
    add_smul := ⋯, zero_smul := ⋯ }
this : IsScalarTower.{u_1, u_1, u_3} R 𝓀 (↥N ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R ↥N) (maximalIdeal R) ⊤) := ⋯
rw :
  Module.finrank 𝓀 (TensorProduct.{u_1, u_1, u_3} R 𝓀 ↥N) =
    Module.finrank.{u_1, u_3} (HasQuotient.Quotient R (B := Ideal R) (maximalIdeal R))
      (↥N ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R ↥N) (maximalIdeal R) ⊤)
⊢ N.spanFinrank =
    Module.finrank.{u_1, u_3} (HasQuotient.Quotient R (B := Ideal R) (maximalIdeal R))
      (↥N ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R ↥N) (maximalIdeal R) ⊤)

Tactic:
rw [← spanFinrank_top_eq_of_residueField N fg, ← Module.finrank_eq_spanFinrank_of_free]

Premises used: TensorProduct.spanFinrank_top_eq_of_residueField, Module.finrank_eq_spanFinrank_of_free
-- Module: Mathlib.Algebra.Module.SpanRankOperations
Goal:
R : Type u_1
inst : CommRing R
M : Type u_3
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsLocalRing R
N : Submodule R M
fg : N.FG
this_1 : Module.{u_1, u_3} 𝓀 (↥N ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R ↥N) (maximalIdeal R) ⊤) :=
  { smul := spanFinrank_eq_finrank_quotient._aux_1 N, mul_smul := ⋯, one_smul := ⋯, smul_zero := ⋯, smul_add := ⋯,
    add_smul := ⋯, zero_smul := ⋯ }
this : IsScalarTower.{u_1, u_1, u_3} R 𝓀 (↥N ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R ↥N) (maximalIdeal R) ⊤) := ⋯
e : TensorProduct.{u_1, u_1, u_3} R 𝓀 ↥N ≃ₗ[𝓀]
  ↥N ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R ↥N) (maximalIdeal R) ⊤ :=
  LinearEquiv.extendScalarsOfSurjective ⋯ (quotTensorEquivQuotSMul (↥N) (maximalIdeal R))
⊢ Module.finrank 𝓀 (TensorProduct.{u_1, u_1, u_3} R 𝓀 ↥N) =
    Module.finrank.{u_1, u_3} (HasQuotient.Quotient R (B := Ideal R) (maximalIdeal R))
      (↥N ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R ↥N) (maximalIdeal R) ⊤)

Tactic:
e.finrank_eq

Premises used: Set.Mem, LinearEquiv.finrank_eq, IsLocalRing.ResidueField
-- Module: Mathlib.Algebra.Module.SpanRankOperations
Goal:
R : Type u_1
inst : CommRing R
M : Type u_3
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsLocalRing R
N : Submodule R M
fg : N.FG
this_1 : Module.{u_1, u_3} 𝓀 (↥N ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R ↥N) (maximalIdeal R) ⊤) :=
  { smul := spanFinrank_eq_finrank_quotient._aux_1 N, mul_smul := ⋯, one_smul := ⋯, smul_zero := ⋯, smul_add := ⋯,
    add_smul := ⋯, zero_smul := ⋯ }
this : IsScalarTower.{u_1, u_1, u_3} R 𝓀 (↥N ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R ↥N) (maximalIdeal R) ⊤) := ⋯
e : TensorProduct.{u_1, u_1, u_3} R 𝓀 ↥N ≃ₗ[𝓀]
  ↥N ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R ↥N) (maximalIdeal R) ⊤ :=
  LinearEquiv.extendScalarsOfSurjective ⋯ (quotTensorEquivQuotSMul (↥N) (maximalIdeal R))
⊢ Module.finrank 𝓀 (TensorProduct.{u_1, u_1, u_3} R 𝓀 ↥N) =
    Module.finrank.{u_1, u_3} (HasQuotient.Quotient R (B := Ideal R) (maximalIdeal R))
      (↥N ⧸ HSMul.hSMul (α := Ideal R) (β := Submodule R ↥N) (maximalIdeal R) ⊤)

Tactic:
exact e.finrank_eq

Premises used: LinearEquiv.finrank_eq
-- Module: Mathlib.Algebra.Module.SpanRankOperations
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsLocalRing R
fg : Ideal.FG (maximalIdeal R)
⊢ spanFinrank (maximalIdeal R) = Module.finrank.{u_1, u_1} 𝓀 (CotangentSpace R)

Tactic:
spanFinrank_eq_finrank_quotient _ fg

Premises used: Set.Mem, Ideal.Cotangent, IsLocalRing.ResidueField, IsLocalRing.spanFinrank_eq_finrank_quotient
-- Module: Mathlib.Algebra.Module.SpanRankOperations
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsLocalRing R
inst_2 : IsNoetherianRing R
⊢ spanFinrank (maximalIdeal R) = Module.finrank.{u_1, u_1} 𝓀 (CotangentSpace R)

Tactic:
spanFinrank_maximalIdeal_eq_finrank_cotangentSpace_of_fg (maximalIdeal R).fg_of_isNoetherianRing

Premises used: Ideal.fg_of_isNoetherianRing, IsLocalRing.spanFinrank_maximalIdeal_eq_finrank_cotangentSpace_of_fg, IsLocalRing.maximalIdeal
-- Module: Mathlib.Algebra.Module.StablyFree.Basic
Goal:
R : Type u
inst : Ring R
M : Type v
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsStablyFree R M
⊢ ∃ (N : Type u) (x : AddCommGroup N) (x_1 : Module R N) (_ : Module.Finite R N) (_ : Free R N), Free R (M × N)

Tactic:
IsStablyFree.exist_free_prod'

Premises used: _private.0.Module.IsStablyFree.exist_free_prod'
-- Module: Mathlib.Algebra.Module.StablyFree.Basic
Goal:
R : Type u
inst : Ring R
M : Type v
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type w
inst_3 : AddCommGroup N
inst_4 : Module R N
e : M ≃ₗ[R] N
inst_5 : IsStablyFree R M
obtain :
  ∀ (P : Type u) (hPc : AddCommGroup P) (hPm : Module R P) (hPfin : Module.Finite R P) (hPfree : Free R P),
    Free R (M × P) → IsStablyFree R N
⊢ IsStablyFree R N

Tactic:
obtain ⟨P, hPc, hPm, hPfin, hPfree, _⟩ := IsStablyFree.exist_free_prod R M

Premises used: Module.IsStablyFree.exist_free_prod
-- Module: Mathlib.Algebra.Module.StablyFree.Basic
Goal:
R : Type u
inst : Ring R
M : Type v
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type w
inst_3 : AddCommGroup N
inst_4 : Module R N
e : M ≃ₗ[R] N
inst_5 : IsStablyFree R M
P : Type u
hPc : AddCommGroup P
hPm : Module R P
hPfin : Module.Finite R P
hPfree : Free R P
h : Free R (M × P)
⊢ IsStablyFree R N

Tactic:
⟨P, hPc, hPm, hPfin, hPfree, Free.of_equiv (e.prodCongr (LinearEquiv.refl R P))⟩

Premises used: LinearEquiv.prodCongr, _private.0.Module.IsStablyFree.mk, Module.Free.of_equiv, Exists.intro, LinearEquiv.refl
-- Module: Mathlib.Algebra.Module.StablyFree.Basic
Goal:
R : Type u
inst : Ring R
M : Type v
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type w
inst_3 : AddCommGroup N
inst_4 : Module R N
e : M ≃ₗ[R] N
inst_5 : IsStablyFree R M
P : Type u
hPc : AddCommGroup P
hPm : Module R P
hPfin : Module.Finite R P
hPfree : Free R P
h : Free R (M × P)
⊢ IsStablyFree R N

Tactic:
exact ⟨P, hPc, hPm, hPfin, hPfree, Free.of_equiv (e.prodCongr (LinearEquiv.refl R P))⟩
-- Module: Mathlib.Algebra.Module.StablyFree.Basic
Goal:
R : Type u
inst : Ring R
M : Type v
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type w
inst_3 : AddCommGroup N
inst_4 : Module R N
e : M ≃ₗ[R] N
⊢ IsStablyFree R M ↔ IsStablyFree R N

Tactic:
⟨fun h ↦ h.equiv e, fun h ↦ h.equiv e.symm⟩

Premises used: LinearEquiv.symm, Module.IsStablyFree.equiv, Iff.intro
-- Module: Mathlib.Algebra.Module.StablyFree.Basic
Goal:
R : Type u
inst : Ring R
M : Type v
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type w
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : IsStablyFree R M
⊢ IsStablyFree R (ULift.{w, v} M)

Tactic:
IsStablyFree.equiv ULift.moduleEquiv.symm

Premises used: LinearEquiv.symm, Module.IsStablyFree.equiv, ULift.moduleEquiv
-- Module: Mathlib.Algebra.Module.StablyFree.Basic
Goal:
R : Type u
inst : Ring R
M : Type v
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsStablyFree R (ULift.{w, v} M)
⊢ IsStablyFree R M

Tactic:
IsStablyFree.equiv ULift.moduleEquiv

Premises used: Module.IsStablyFree.equiv, ULift.moduleEquiv
-- Module: Mathlib.Algebra.Module.StablyFree.Basic
Goal:
R : Type u
inst : Ring R
M : Type v
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type w
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : Small.{w, v} M
inst_6 : IsStablyFree R M
⊢ IsStablyFree.{u, w} R (Shrink.{w, v} M)

Tactic:
IsStablyFree.equiv (Shrink.linearEquiv R M).symm

Premises used: LinearEquiv.symm, Module.IsStablyFree.equiv, Shrink.linearEquiv
-- Module: Mathlib.Algebra.Module.StablyFree.Basic
Goal:
R : Type u
inst : Ring R
M : Type v
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Small.{w, v} M
inst_4 : IsStablyFree.{u, w} R (Shrink.{w, v} M)
⊢ IsStablyFree R M

Tactic:
IsStablyFree.equiv (Shrink.linearEquiv R M)

Premises used: Module.IsStablyFree.equiv, Shrink.linearEquiv
-- Module: Mathlib.Algebra.Module.StablyFree.Basic
Goal:
R : Type u
inst : Ring R
M : Type v
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type w
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : Free R M
⊢ IsStablyFree R M

Tactic:
⟨PUnit, inferInstance, inferInstance, inferInstance, inferInstance, inferInstance⟩

Premises used: _private.0.Module.IsStablyFree.mk, inferInstance, PUnit, Exists.intro
-- Module: Mathlib.Algebra.Module.StablyFree.Basic
Goal:
R : Type u
inst : Ring R
M : Type v
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type w
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : Module.Finite R N
inst_6 : Free R N
inst_7 : Free R (M × N)
⊢ IsStablyFree R M

Tactic:
have : Small.{u} N := Module.Finite.small.{u} R N
  let +nondep eN : N ≃ₗ[R] Shrink.{u} N := (Shrink.linearEquiv R N).symm
  ⟨Shrink.{u} N, inferInstance, inferInstance, Module.Finite.equiv eN,
    Free.of_equiv eN, Free.of_equiv ((LinearEquiv.refl R M).prodCongr eN)⟩

Premises used: LinearEquiv.symm, LinearEquiv.prodCongr, _private.0.Module.IsStablyFree.mk, inferInstance, Module.Free.of_equiv, Module.Finite.small, Exists.intro, Shrink.linearEquiv, LinearEquiv.refl, Shrink, Module.Finite.equiv
-- Module: Mathlib.Algebra.Module.StablyFree.Basic
Goal:
R : Type u
inst : Ring R
M : Type v
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type w
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : Module.Finite R N
inst_6 : Free R N
inst_7 : Free R (N × M)
⊢ IsStablyFree R M

Tactic:
have : Free R (M × N) := Free.of_equiv (LinearEquiv.prodComm R N M)
  .of_free_prod R M N

Premises used: Module.IsStablyFree.of_free_prod, LinearEquiv.prodComm, Module.Free.of_equiv
-- Module: Mathlib.Algebra.Module.StablyFree.Basic
Goal:
R : Type u
inst : Ring R
M : Type v
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type w
inst_3 : AddCommGroup N
inst_4 : Module R N
inst_5 : IsStablyFree R M
obtain :
  ∀ (N : Type u) (w : AddCommGroup N) (w_1 : Module R N), Module.Finite R N → Free R N → Free R (M × N) → Projective R M
⊢ Projective R M

Tactic:
obtain ⟨N, _, _, _, _, _⟩ := IsStablyFree.exist_free_prod R M

Premises used: Module.IsStablyFree.exist_free_prod
-- Module: Mathlib.Algebra.Module.StablyFree.Basic
Goal:
R : Type u
inst : Ring R
M : Type v
inst_1 : AddCommGroup M
inst_2 : Module R M
N_1 : Type w
inst_3 : AddCommGroup N_1
inst_4 : Module R N_1
inst_5 : IsStablyFree R M
N : Type u
w : AddCommGroup N
w_1 : Module R N
w_2 : Module.Finite R N
w_3 : Free R N
h : Free R (M × N)
⊢ Projective R M

Tactic:
Projective.of_split (LinearMap.inl R M N) (LinearMap.fst R M N) (LinearMap.ext fun _ ↦ rfl)

Premises used: LinearMap.fst, LinearMap.inl, LinearMap.ext, Module.Projective.of_split, rfl
-- Module: Mathlib.Algebra.Module.StablyFree.Basic
Goal:
R : Type u
inst : Ring R
M : Type v
inst_1 : AddCommGroup M
inst_2 : Module R M
N_1 : Type w
inst_3 : AddCommGroup N_1
inst_4 : Module R N_1
inst_5 : IsStablyFree R M
N : Type u
w : AddCommGroup N
w_1 : Module R N
w_2 : Module.Finite R N
w_3 : Free R N
h : Free R (M × N)
⊢ Projective R M

Tactic:
exact Projective.of_split (LinearMap.inl R M N) (LinearMap.fst R M N) (LinearMap.ext fun _ ↦ rfl)

Premises used: LinearMap.fst, LinearMap.inl, LinearMap.ext, Module.Projective.of_split, rfl
-- Module: Mathlib.Algebra.Module.StablyFree.FreeOfInvertible
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
N : Type u_3
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
n : ℕ
bN : Module.Basis (Fin n) R N
x y : M × N
x_1 : Fin n → M × N
⊢ Eq.{u_2 + 1} (α := M)
    ((AlternatingMap.smulRight (bN.det.compLinearMap (LinearMap.snd R M N)) (x + y).1 : (a : Fin n → M × N) → M) x_1 :
      M)
    ((HAdd.hAdd (α := (M × N) [⋀^Fin n]→ₗ[R] M)
            (AlternatingMap.smulRight (bN.det.compLinearMap (LinearMap.snd R M N)) x.1)
            (AlternatingMap.smulRight (bN.det.compLinearMap (LinearMap.snd R M N)) y.1) :
          (a : Fin n → M × N) → M)
        x_1 :
      M)

Tactic:
simp
-- Module: Mathlib.Algebra.Module.StablyFree.FreeOfInvertible
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
N : Type u_3
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
n : ℕ
bN : Module.Basis (Fin n) R N
c : R
x : M × N
x_1 : Fin n → M × N
⊢ Eq.{u_2 + 1} (α := M)
    ((AlternatingMap.smulRight (bN.det.compLinearMap (LinearMap.snd R M N)) (c • x).1 : (a : Fin n → M × N) → M) x_1 :
      M)
    ((HSMul.hSMul (α := R) (β := (M × N) [⋀^Fin n]→ₗ[R] M) ((RingHom.id R : (a : R) → R) c : R)
            (AlternatingMap.smulRight (bN.det.compLinearMap (LinearMap.snd R M N)) x.1) :
          (a : Fin n → M × N) → M)
        x_1 :
      M)

Tactic:
simp [smul_smul, mul_comm]

Premises used: smul_smul, mul_comm
-- Module: Mathlib.Algebra.Module.StablyFree.FreeOfInvertible
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
N : Type u_3
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : AddCommGroup N
inst_4 : Module R N
n : ℕ
bN : Module.Basis (Fin n) R N
m : M
⊢ (cofactorToLeft bN : (a : ↥(⋀[R]^(n + 1) (M × N))) → M)
      (((ιMulti R (n + 1) (M := M × N) : (M × N) [⋀^Fin (n + 1)]→ₗ[R] ↥(⋀[R]^(n + 1) (M × N))) :
            (a : Fin (n + 1) → M × N) → ↥(⋀[R]^(n + 1) (M × N)))
          (Fin.cons (α := fun (a : Fin (n + 1)) ↦ M × N) (m, 0) fun (i : Fin n) ↦ (0, (bN : (a : Fin n) → N) i)) :
        ↥(⋀[R]^(n + 1) (M × N))) =
    m

Tactic:
simp [cofactorToLeft, cofactorLinear, AlternatingMap.alternatizeUncurryFin_apply,
    Fin.sum_univ_succ, Module.Basis.det_self]

Premises used: AlternatingMap.alternatizeUncurryFin_apply, _private.0.exteriorPower.cofactorToLeft, _private.0.exteriorPower.cofactorLinear, Module.Basis.det_self, Fin.sum_univ_succ
-- Module: Mathlib.Algebra.Module.StablyFree.FreeOfInvertible
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsStablyFree R M
inst_4 : Module.Invertible R M
inl : Subsingleton R → Free R M
inr : Nontrivial R → Free R M
⊢ Free R M

Tactic:
rcases subsingleton_or_nontrivial R with _ | _

Premises used: subsingleton_or_nontrivial
-- Module: Mathlib.Algebra.Module.StablyFree.FreeOfInvertible
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsStablyFree R M
inst_4 : Module.Invertible R M
h : Subsingleton R
⊢ Free R M

Tactic:
Module.Free.of_subsingleton' R M

Premises used: Module.Free.of_subsingleton'
-- Module: Mathlib.Algebra.Module.StablyFree.FreeOfInvertible
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsStablyFree R M
inst_4 : Module.Invertible R M
h : Subsingleton R
⊢ Free R M

Tactic:
exact Module.Free.of_subsingleton' R M

Premises used: Module.Free.of_subsingleton'
-- Module: Mathlib.Algebra.Module.StablyFree.FreeOfInvertible
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsStablyFree R M
inst_4 : Module.Invertible R M
h : Nontrivial R
inr : ∀ (N : Type u_1) (w : AddCommGroup N) (w_1 : Module R N), Module.Finite R N → Free R N → Free R (M × N) → Free R M
⊢ Free R M

Tactic:
obtain ⟨N, _, _, _, _, _⟩ := IsStablyFree.exist_free_prod R M

Premises used: Module.IsStablyFree.exist_free_prod
-- Module: Mathlib.Algebra.Module.StablyFree.FreeOfInvertible
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsStablyFree R M
inst_4 : Module.Invertible R M
h : Nontrivial R
N : Type u_1
w : AddCommGroup N
w_1 : Module R N
w_2 : Module.Finite R N
w_3 : Free R N
h_1 : Free R (M × N)
n : ℕ := finrank R N
𝔭 : PrimeSpectrum R := Nonempty.some ⋯
⊢ rankAtStalk M 𝔭 = 1

Tactic:
simp [rankAtStalk, Invertible.finrank_eq_one]

Premises used: Module.rankAtStalk, Module.Invertible.finrank_eq_one
-- Module: Mathlib.Algebra.Module.StablyFree.FreeOfInvertible
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsStablyFree R M
inst_4 : Module.Invertible R M
h : Nontrivial R
N : Type u_1
w : AddCommGroup N
w_1 : Module R N
w_2 : Module.Finite R N
w_3 : Free R N
h_1 : Free R (M × N)
n : ℕ := finrank R N
𝔭 : PrimeSpectrum R := Nonempty.some ⋯
⊢ rankAtStalk M 𝔭 = 1

Tactic:
have h1 : rankAtStalk M 𝔭 = 1 := by simp [rankAtStalk, Invertible.finrank_eq_one]
-- Module: Mathlib.Algebra.Module.StablyFree.FreeOfInvertible
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsStablyFree R M
inst_4 : Module.Invertible R M
h : Nontrivial R
N : Type u_1
w : AddCommGroup N
w_1 : Module R N
w_2 : Module.Finite R N
w_3 : Free R N
h_1 : Free R (M × N)
n : ℕ := finrank R N
𝔭 : PrimeSpectrum R := Nonempty.some ⋯
h1 : rankAtStalk M 𝔭 = 1
⊢ rankAtStalk (M × N) 𝔭 =
    HAdd.hAdd (α := (p : PrimeSpectrum R) → ℕ) (β := (p : PrimeSpectrum R) → ℕ) (rankAtStalk M) (rankAtStalk N) 𝔭

Tactic:
have heq := congr($(rankAtStalk_prod M N) 𝔭)
-- Module: Mathlib.Algebra.Module.StablyFree.FreeOfInvertible
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsStablyFree R M
inst_4 : Module.Invertible R M
h : Nontrivial R
N : Type u_1
w : AddCommGroup N
w_1 : Module R N
w_2 : Module.Finite R N
w_3 : Free R N
h_1 : Free R (M × N)
n : ℕ := finrank R N
𝔭 : PrimeSpectrum R := Nonempty.some ⋯
h1 : rankAtStalk M 𝔭 = 1
heq :
  rankAtStalk (M × N) 𝔭 =
    HAdd.hAdd (α := (p : PrimeSpectrum R) → ℕ) (β := (p : PrimeSpectrum R) → ℕ) (rankAtStalk M) (rankAtStalk N) 𝔭
⊢ (↑(finrank R (M × N)) : ℕ) = HAdd.hAdd (α := ℕ) 1 (↑(finrank R N) : ℕ)

Tactic:
simp only [rankAtStalk_eq_finrank_of_free, Pi.natCast_apply, Pi.add_apply, h1] at heq

Premises used: Pi.natCast_apply, Pi.add_apply, Module.rankAtStalk_eq_finrank_of_free
-- Module: Mathlib.Algebra.Module.StablyFree.FreeOfInvertible
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsStablyFree R M
inst_4 : Module.Invertible R M
h : Nontrivial R
N : Type u_1
w : AddCommGroup N
w_1 : Module R N
w_2 : Module.Finite R N
w_3 : Free R N
h_1 : Free R (M × N)
n : ℕ := finrank R N
𝔭 : PrimeSpectrum R := Nonempty.some ⋯
h1 : rankAtStalk M 𝔭 = 1
heq : (↑(finrank R (M × N)) : ℕ) = HAdd.hAdd (α := ℕ) 1 (↑(finrank R N) : ℕ)
⊢ finrank R (M × N) = n + 1

Tactic:
grind
-- Module: Mathlib.Algebra.Module.StablyFree.FreeOfInvertible
Goal:
R : Type u_1
inst : CommRing R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsStablyFree R M
inst_4 : Module.Invertible R M
h : Nontrivial R
N : Type u_1
w : AddCommGroup N
w_1 : Module R N
w_2 : Module.Finite R N
w_3 : Free R N
h_1 : Free R (M × N)
n : ℕ := finrank R N
⊢ finrank R (M × N) = n + 1

Tactic:
have hp : Module.finrank R (M × N) = n + 1 := by
    let 𝔭 : PrimeSpectrum R := Nonempty.some inferInstance
    have h1 : rankAtStalk M 𝔭 = 1 := by simp [rankAtStalk, Invertible.finrank_eq_one]
    have heq := congr($(rankAtStalk_prod M N) 𝔭)
    simp only [rankAtStalk_eq_finrank_of_free, Pi.natCast_apply, Pi.add_apply, h1] at heq
    grind