awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.FreeModule.PID
Goal:
R : Type u_2
inst : CommRing R
M : Type u_3
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsPrincipalIdealRing R
N O : Submodule R M
hNO : N ≤ O
ϕ : LinearMap.{u_2, u_2, u_3, u_2} (RingHom.id R) (↥O) R
hϕ : ∀ (ψ : LinearMap.{u_2, u_2, u_3, u_2} (RingHom.id R) (↥O) R), ¬ϕ.submoduleImage N < ψ.submoduleImage N
inst_4 : (ϕ.submoduleImage N).IsPrincipal
y : M
yN : y ∈ N
ϕy_eq : (ϕ : (a : ↥O) → R) (Subtype.mk (p := fun (x : M) ↦ x ∈ O) y ⋯) = generator (ϕ.submoduleImage N)
ψ : LinearMap.{u_2, u_2, u_3, u_2} (RingHom.id R) (↥O) R
a : R := generator (ϕ.submoduleImage N)
d : R :=
  generator
    (span R (insert a (singleton (α := R) ((ψ : (a : ↥O) → R) (Subtype.mk (p := fun (x : M) ↦ x ∈ O) y ⋯) : R))))
d_dvd_left : d ∣ a
d_dvd_right : d ∣ (ψ : (a : ↥O) → R) (Subtype.mk (p := fun (x : M) ↦ x ∈ O) y ⋯)
r₁ r₂ : R
d_eq : d = r₁ * a + HMul.hMul (β := R) r₂ ((ψ : (a : ↥O) → R) (Subtype.mk (p := fun (x : M) ↦ x ∈ O) y ⋯) : R)
ψ' : LinearMap.{u_2, u_2, u_3, u_2} (RingHom.id R) (↥O) R := r₁ • ϕ + r₂ • ψ
refine : (ψ' : (a : ↥O) → R) (Subtype.mk (p := fun (x : M) ↦ x ∈ O) y ⋯) = d
⊢ ∃ (y : M) (yN : y ∈ N), (ψ' : (a : ↥O) → R) (Subtype.mk (p := fun (x : M) ↦ x ∈ O) y ⋯) = d

Tactic:
refine ⟨y, yN, ?_⟩
-- Module: Mathlib.LinearAlgebra.FreeModule.PID
Goal:
R : Type u_2
inst : CommRing R
M : Type u_3
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsPrincipalIdealRing R
N O : Submodule R M
hNO : N ≤ O
ϕ : LinearMap.{u_2, u_2, u_3, u_2} (RingHom.id R) (↥O) R
hϕ : ∀ (ψ : LinearMap.{u_2, u_2, u_3, u_2} (RingHom.id R) (↥O) R), ¬ϕ.submoduleImage N < ψ.submoduleImage N
inst_4 : (ϕ.submoduleImage N).IsPrincipal
y : M
yN : y ∈ N
ϕy_eq : (ϕ : (a : ↥O) → R) (Subtype.mk (p := fun (x : M) ↦ x ∈ O) y ⋯) = generator (ϕ.submoduleImage N)
ψ : LinearMap.{u_2, u_2, u_3, u_2} (RingHom.id R) (↥O) R
a : R := generator (ϕ.submoduleImage N)
d : R :=
  generator
    (span R (insert a (singleton (α := R) ((ψ : (a : ↥O) → R) (Subtype.mk (p := fun (x : M) ↦ x ∈ O) y ⋯) : R))))
d_dvd_left : d ∣ a
d_dvd_right : d ∣ (ψ : (a : ↥O) → R) (Subtype.mk (p := fun (x : M) ↦ x ∈ O) y ⋯)
r₁ r₂ : R
d_eq : d = r₁ * a + HMul.hMul (β := R) r₂ ((ψ : (a : ↥O) → R) (Subtype.mk (p := fun (x : M) ↦ x ∈ O) y ⋯) : R)
ψ' : LinearMap.{u_2, u_2, u_3, u_2} (RingHom.id R) (↥O) R := r₁ • ϕ + r₂ • ψ
change :
  HMul.hMul (β := R) r₁ ((ϕ : (a : ↥O) → R) (Subtype.mk (p := fun (x : M) ↦ x ∈ O) y ⋯) : R) +
      HMul.hMul (β := R) r₂ ((ψ : (a : ↥O) → R) (Subtype.mk (p := fun (x : M) ↦ x ∈ O) y ⋯) : R) =
    d
⊢ (ψ' : (a : ↥O) → R) (Subtype.mk (p := fun (x : M) ↦ x ∈ O) y ⋯) = d

Tactic:
change r₁ * ϕ ⟨y, hNO yN⟩ + r₂ * ψ ⟨y, hNO yN⟩ = d

Premises used: Subtype.mk, DFunLike.coe
-- Module: Mathlib.LinearAlgebra.FreeModule.PID
Goal:
R : Type u_2
inst : CommRing R
M : Type u_3
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsPrincipalIdealRing R
N O : Submodule R M
hNO : N ≤ O
ϕ : LinearMap.{u_2, u_2, u_3, u_2} (RingHom.id R) (↥O) R
hϕ : ∀ (ψ : LinearMap.{u_2, u_2, u_3, u_2} (RingHom.id R) (↥O) R), ¬ϕ.submoduleImage N < ψ.submoduleImage N
inst_4 : (ϕ.submoduleImage N).IsPrincipal
y : M
yN : y ∈ N
ϕy_eq : (ϕ : (a : ↥O) → R) (Subtype.mk (p := fun (x : M) ↦ x ∈ O) y ⋯) = generator (ϕ.submoduleImage N)
ψ : LinearMap.{u_2, u_2, u_3, u_2} (RingHom.id R) (↥O) R
a : R := generator (ϕ.submoduleImage N)
d : R :=
  generator
    (span R (insert a (singleton (α := R) ((ψ : (a : ↥O) → R) (Subtype.mk (p := fun (x : M) ↦ x ∈ O) y ⋯) : R))))
d_dvd_left : d ∣ a
d_dvd_right : d ∣ (ψ : (a : ↥O) → R) (Subtype.mk (p := fun (x : M) ↦ x ∈ O) y ⋯)
r₁ r₂ : R
d_eq : d = r₁ * a + HMul.hMul (β := R) r₂ ((ψ : (a : ↥O) → R) (Subtype.mk (p := fun (x : M) ↦ x ∈ O) y ⋯) : R)
ψ' : LinearMap.{u_2, u_2, u_3, u_2} (RingHom.id R) (↥O) R := r₁ • ϕ + r₂ • ψ
rw :
  HMul.hMul (β := R) r₁ ((ϕ : (a : ↥O) → R) (Subtype.mk (p := fun (x : M) ↦ x ∈ O) y ⋯) : R) +
      HMul.hMul (β := R) r₂ ((ψ : (a : ↥O) → R) (Subtype.mk (p := fun (x : M) ↦ x ∈ O) y ⋯) : R) =
    r₁ * a + HMul.hMul (β := R) r₂ ((ψ : (a : ↥O) → R) (Subtype.mk (p := fun (x : M) ↦ x ∈ O) y ⋯) : R)
rw₁ rw₂ :
  r₁ * generator (ϕ.submoduleImage N) +
      HMul.hMul (β := R) r₂ ((ψ : (a : ↥O) → R) (Subtype.mk (p := fun (x : M) ↦ x ∈ O) y ⋯) : R) =
    r₁ * a + HMul.hMul (β := R) r₂ ((ψ : (a : ↥O) → R) (Subtype.mk (p := fun (x : M) ↦ x ∈ O) y ⋯) : R)
⊢ HMul.hMul (β := R) r₁ ((ϕ : (a : ↥O) → R) (Subtype.mk (p := fun (x : M) ↦ x ∈ O) y ⋯) : R) +
      HMul.hMul (β := R) r₂ ((ψ : (a : ↥O) → R) (Subtype.mk (p := fun (x : M) ↦ x ∈ O) y ⋯) : R) =
    d

Tactic:
rw [d_eq, ϕy_eq]
-- Module: Mathlib.LinearAlgebra.FreeModule.PID
Goal:
R : Type u_2
inst : CommRing R
M : Type u_3
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsPrincipalIdealRing R
N O : Submodule R M
hNO : N ≤ O
ϕ : LinearMap.{u_2, u_2, u_3, u_2} (RingHom.id R) (↥O) R
hϕ : ∀ (ψ : LinearMap.{u_2, u_2, u_3, u_2} (RingHom.id R) (↥O) R), ¬ϕ.submoduleImage N < ψ.submoduleImage N
inst_4 : (ϕ.submoduleImage N).IsPrincipal
y : M
yN : y ∈ N
ϕy_eq : (ϕ : (a : ↥O) → R) (Subtype.mk (p := fun (x : M) ↦ x ∈ O) y ⋯) = generator (ϕ.submoduleImage N)
ψ : LinearMap.{u_2, u_2, u_3, u_2} (RingHom.id R) (↥O) R
a : R := generator (ϕ.submoduleImage N)
d : R :=
  generator
    (span R (insert a (singleton (α := R) ((ψ : (a : ↥O) → R) (Subtype.mk (p := fun (x : M) ↦ x ∈ O) y ⋯) : R))))
d_dvd_left : d ∣ a
d_dvd_right : d ∣ (ψ : (a : ↥O) → R) (Subtype.mk (p := fun (x : M) ↦ x ∈ O) y ⋯)
r₁ r₂ : R
d_eq : d = r₁ * a + HMul.hMul (β := R) r₂ ((ψ : (a : ↥O) → R) (Subtype.mk (p := fun (x : M) ↦ x ∈ O) y ⋯) : R)
ψ' : LinearMap.{u_2, u_2, u_3, u_2} (RingHom.id R) (↥O) R := r₁ • ϕ + r₂ • ψ
⊢ R ∙ d ≤ ψ'.submoduleImage N

Tactic:
have : span R {d} ≤ ψ'.submoduleImage N := by
      rw [span_le, singleton_subset_iff, SetLike.mem_coe, LinearMap.mem_submoduleImage_of_le hNO]
      refine ⟨y, yN, ?_⟩
      change r₁ * ϕ ⟨y, hNO yN⟩ + r₂ * ψ ⟨y, hNO yN⟩ = d
      rw [d_eq, ϕy_eq]
-- Module: Mathlib.LinearAlgebra.FreeModule.PID
Goal:
R : Type u_2
inst : CommRing R
M : Type u_3
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsPrincipalIdealRing R
N O : Submodule R M
hNO : N ≤ O
ϕ : LinearMap.{u_2, u_2, u_3, u_2} (RingHom.id R) (↥O) R
hϕ : ∀ (ψ : LinearMap.{u_2, u_2, u_3, u_2} (RingHom.id R) (↥O) R), ¬ϕ.submoduleImage N < ψ.submoduleImage N
inst_4 : (ϕ.submoduleImage N).IsPrincipal
y : M
yN : y ∈ N
ϕy_eq : (ϕ : (a : ↥O) → R) (Subtype.mk (p := fun (x : M) ↦ x ∈ O) y ⋯) = generator (ϕ.submoduleImage N)
ψ : LinearMap.{u_2, u_2, u_3, u_2} (RingHom.id R) (↥O) R
a : R := generator (ϕ.submoduleImage N)
d : R :=
  generator
    (span R (insert a (singleton (α := R) ((ψ : (a : ↥O) → R) (Subtype.mk (p := fun (x : M) ↦ x ∈ O) y ⋯) : R))))
d_dvd_left : d ∣ a
d_dvd_right : d ∣ (ψ : (a : ↥O) → R) (Subtype.mk (p := fun (x : M) ↦ x ∈ O) y ⋯)
r₁ r₂ : R
d_eq : d = r₁ * a + HMul.hMul (β := R) r₂ ((ψ : (a : ↥O) → R) (Subtype.mk (p := fun (x : M) ↦ x ∈ O) y ⋯) : R)
ψ' : LinearMap.{u_2, u_2, u_3, u_2} (RingHom.id R) (↥O) R := r₁ • ϕ + r₂ • ψ
this : R ∙ d ≤ ψ'.submoduleImage N
⊢ Eq (α := Ideal R)
    (R ∙
      generator
        (span R (insert a (singleton (α := R) ((ψ : (a : ↥O) → R) (Subtype.mk (p := fun (x : M) ↦ x ∈ O) y ⋯) : R)))))
    (R ∙ generator (ϕ.submoduleImage N))

Tactic:
le_antisymm (this.trans (le_of_eq ?_)) (Ideal.span_singleton_le_span_singleton.mpr d_dvd_left)

Premises used: Iff.mpr, Ideal.span_singleton_le_span_singleton, le_antisymm, LE.le.trans, le_of_eq
-- Module: Mathlib.LinearAlgebra.FreeModule.PID
Goal:
R : Type u_2
inst : CommRing R
M : Type u_3
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsPrincipalIdealRing R
N O : Submodule R M
hNO : N ≤ O
ϕ : LinearMap.{u_2, u_2, u_3, u_2} (RingHom.id R) (↥O) R
hϕ : ∀ (ψ : LinearMap.{u_2, u_2, u_3, u_2} (RingHom.id R) (↥O) R), ¬ϕ.submoduleImage N < ψ.submoduleImage N
inst_4 : (ϕ.submoduleImage N).IsPrincipal
y : M
yN : y ∈ N
ϕy_eq : (ϕ : (a : ↥O) → R) (Subtype.mk (p := fun (x : M) ↦ x ∈ O) y ⋯) = generator (ϕ.submoduleImage N)
ψ : LinearMap.{u_2, u_2, u_3, u_2} (RingHom.id R) (↥O) R
a : R := generator (ϕ.submoduleImage N)
d : R :=
  generator
    (span R (insert a (singleton (α := R) ((ψ : (a : ↥O) → R) (Subtype.mk (p := fun (x : M) ↦ x ∈ O) y ⋯) : R))))
d_dvd_left : d ∣ a
d_dvd_right : d ∣ (ψ : (a : ↥O) → R) (Subtype.mk (p := fun (x : M) ↦ x ∈ O) y ⋯)
r₁ r₂ : R
d_eq : d = r₁ * a + HMul.hMul (β := R) r₂ ((ψ : (a : ↥O) → R) (Subtype.mk (p := fun (x : M) ↦ x ∈ O) y ⋯) : R)
ψ' : LinearMap.{u_2, u_2, u_3, u_2} (RingHom.id R) (↥O) R := r₁ • ϕ + r₂ • ψ
this : R ∙ d ≤ ψ'.submoduleImage N
le_antisymm : ψ'.submoduleImage N = R ∙ generator (ϕ.submoduleImage N)
⊢ Eq (α := Ideal R)
    (R ∙
      generator
        (span R (insert a (singleton (α := R) ((ψ : (a : ↥O) → R) (Subtype.mk (p := fun (x : M) ↦ x ∈ O) y ⋯) : R)))))
    (R ∙ generator (ϕ.submoduleImage N))

Tactic:
refine
      le_antisymm (this.trans (le_of_eq ?_)) (Ideal.span_singleton_le_span_singleton.mpr d_dvd_left)

Premises used: Iff.mpr, Ideal.span_singleton_le_span_singleton, le_antisymm, LE.le.trans, le_of_eq
-- Module: Mathlib.LinearAlgebra.FreeModule.PID
Goal:
R : Type u_2
inst : CommRing R
M : Type u_3
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsPrincipalIdealRing R
N O : Submodule R M
hNO : N ≤ O
ϕ : LinearMap.{u_2, u_2, u_3, u_2} (RingHom.id R) (↥O) R
hϕ : ∀ (ψ : LinearMap.{u_2, u_2, u_3, u_2} (RingHom.id R) (↥O) R), ¬ϕ.submoduleImage N < ψ.submoduleImage N
inst_4 : (ϕ.submoduleImage N).IsPrincipal
y : M
yN : y ∈ N
ϕy_eq : (ϕ : (a : ↥O) → R) (Subtype.mk (p := fun (x : M) ↦ x ∈ O) y ⋯) = generator (ϕ.submoduleImage N)
ψ : LinearMap.{u_2, u_2, u_3, u_2} (RingHom.id R) (↥O) R
a : R := generator (ϕ.submoduleImage N)
d : R :=
  generator
    (span R (insert a (singleton (α := R) ((ψ : (a : ↥O) → R) (Subtype.mk (p := fun (x : M) ↦ x ∈ O) y ⋯) : R))))
d_dvd_left : d ∣ a
d_dvd_right : d ∣ (ψ : (a : ↥O) → R) (Subtype.mk (p := fun (x : M) ↦ x ∈ O) y ⋯)
r₁ r₂ : R
d_eq : d = r₁ * a + HMul.hMul (β := R) r₂ ((ψ : (a : ↥O) → R) (Subtype.mk (p := fun (x : M) ↦ x ∈ O) y ⋯) : R)
ψ' : LinearMap.{u_2, u_2, u_3, u_2} (RingHom.id R) (↥O) R := r₁ • ϕ + r₂ • ψ
this : R ∙ d ≤ ψ'.submoduleImage N
rw : ψ'.submoduleImage N = ϕ.submoduleImage N
⊢ ψ'.submoduleImage N = R ∙ generator (ϕ.submoduleImage N)

Tactic:
rw [span_singleton_generator]

Premises used: Submodule.IsPrincipal.span_singleton_generator
-- Module: Mathlib.LinearAlgebra.FreeModule.PID
Goal:
R : Type u_2
inst : CommRing R
M : Type u_3
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsPrincipalIdealRing R
N O : Submodule R M
hNO : N ≤ O
ϕ : LinearMap.{u_2, u_2, u_3, u_2} (RingHom.id R) (↥O) R
hϕ : ∀ (ψ : LinearMap.{u_2, u_2, u_3, u_2} (RingHom.id R) (↥O) R), ¬ϕ.submoduleImage N < ψ.submoduleImage N
inst_4 : (ϕ.submoduleImage N).IsPrincipal
y : M
yN : y ∈ N
ϕy_eq : (ϕ : (a : ↥O) → R) (Subtype.mk (p := fun (x : M) ↦ x ∈ O) y ⋯) = generator (ϕ.submoduleImage N)
ψ : LinearMap.{u_2, u_2, u_3, u_2} (RingHom.id R) (↥O) R
a : R := generator (ϕ.submoduleImage N)
d : R :=
  generator
    (span R (insert a (singleton (α := R) ((ψ : (a : ↥O) → R) (Subtype.mk (p := fun (x : M) ↦ x ∈ O) y ⋯) : R))))
d_dvd_left : d ∣ a
d_dvd_right : d ∣ (ψ : (a : ↥O) → R) (Subtype.mk (p := fun (x : M) ↦ x ∈ O) y ⋯)
r₁ r₂ : R
d_eq : d = r₁ * a + HMul.hMul (β := R) r₂ ((ψ : (a : ↥O) → R) (Subtype.mk (p := fun (x : M) ↦ x ∈ O) y ⋯) : R)
ψ' : LinearMap.{u_2, u_2, u_3, u_2} (RingHom.id R) (↥O) R := r₁ • ϕ + r₂ • ψ
this : R ∙ d ≤ ψ'.submoduleImage N
apply : ϕ.submoduleImage N ≤ R ∙ d
⊢ ψ'.submoduleImage N = ϕ.submoduleImage N

Tactic:
apply (le_trans _ this).eq_of_not_lt' (hϕ ψ')

Premises used: LE.le.eq_of_not_lt', le_trans
-- Module: Mathlib.LinearAlgebra.FreeModule.PID
Goal:
R : Type u_2
inst : CommRing R
M : Type u_3
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsPrincipalIdealRing R
N O : Submodule R M
hNO : N ≤ O
ϕ : LinearMap.{u_2, u_2, u_3, u_2} (RingHom.id R) (↥O) R
hϕ : ∀ (ψ : LinearMap.{u_2, u_2, u_3, u_2} (RingHom.id R) (↥O) R), ¬ϕ.submoduleImage N < ψ.submoduleImage N
inst_4 : (ϕ.submoduleImage N).IsPrincipal
y : M
yN : y ∈ N
ϕy_eq : (ϕ : (a : ↥O) → R) (Subtype.mk (p := fun (x : M) ↦ x ∈ O) y ⋯) = generator (ϕ.submoduleImage N)
ψ : LinearMap.{u_2, u_2, u_3, u_2} (RingHom.id R) (↥O) R
a : R := generator (ϕ.submoduleImage N)
d : R :=
  generator
    (span R (insert a (singleton (α := R) ((ψ : (a : ↥O) → R) (Subtype.mk (p := fun (x : M) ↦ x ∈ O) y ⋯) : R))))
d_dvd_left : d ∣ a
d_dvd_right : d ∣ (ψ : (a : ↥O) → R) (Subtype.mk (p := fun (x : M) ↦ x ∈ O) y ⋯)
r₁ r₂ : R
d_eq : d = r₁ * a + HMul.hMul (β := R) r₂ ((ψ : (a : ↥O) → R) (Subtype.mk (p := fun (x : M) ↦ x ∈ O) y ⋯) : R)
ψ' : LinearMap.{u_2, u_2, u_3, u_2} (RingHom.id R) (↥O) R := r₁ • ϕ + r₂ • ψ
this : R ∙ d ≤ ψ'.submoduleImage N
rw : LE.le (α := Submodule R R) (R ∙ generator (ϕ.submoduleImage N)) (R ∙ d)
⊢ ϕ.submoduleImage N ≤ R ∙ d

Tactic:
rw [← span_singleton_generator (ϕ.submoduleImage N)]

Premises used: Submodule.IsPrincipal.span_singleton_generator, LinearMap.submoduleImage
-- Module: Mathlib.LinearAlgebra.FreeModule.PID
Goal:
R : Type u_2
inst : CommRing R
M : Type u_3
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsPrincipalIdealRing R
N O : Submodule R M
hNO : N ≤ O
ϕ : LinearMap.{u_2, u_2, u_3, u_2} (RingHom.id R) (↥O) R
hϕ : ∀ (ψ : LinearMap.{u_2, u_2, u_3, u_2} (RingHom.id R) (↥O) R), ¬ϕ.submoduleImage N < ψ.submoduleImage N
inst_4 : (ϕ.submoduleImage N).IsPrincipal
y : M
yN : y ∈ N
ϕy_eq : (ϕ : (a : ↥O) → R) (Subtype.mk (p := fun (x : M) ↦ x ∈ O) y ⋯) = generator (ϕ.submoduleImage N)
ψ : LinearMap.{u_2, u_2, u_3, u_2} (RingHom.id R) (↥O) R
a : R := generator (ϕ.submoduleImage N)
d : R :=
  generator
    (span R (insert a (singleton (α := R) ((ψ : (a : ↥O) → R) (Subtype.mk (p := fun (x : M) ↦ x ∈ O) y ⋯) : R))))
d_dvd_left : d ∣ a
d_dvd_right : d ∣ (ψ : (a : ↥O) → R) (Subtype.mk (p := fun (x : M) ↦ x ∈ O) y ⋯)
r₁ r₂ : R
d_eq : d = r₁ * a + HMul.hMul (β := R) r₂ ((ψ : (a : ↥O) → R) (Subtype.mk (p := fun (x : M) ↦ x ∈ O) y ⋯) : R)
ψ' : LinearMap.{u_2, u_2, u_3, u_2} (RingHom.id R) (↥O) R := r₁ • ϕ + r₂ • ψ
this : R ∙ d ≤ ψ'.submoduleImage N
⊢ LE.le (α := Submodule R R) (R ∙ generator (ϕ.submoduleImage N)) (R ∙ d)

Tactic:
Ideal.span_singleton_le_span_singleton.mpr d_dvd_left

Premises used: Iff.mpr, Set.Mem, setOf, Ideal.span_singleton_le_span_singleton
-- Module: Mathlib.LinearAlgebra.FreeModule.PID
Goal:
R : Type u_2
inst : CommRing R
M : Type u_3
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsPrincipalIdealRing R
N O : Submodule R M
hNO : N ≤ O
ϕ : LinearMap.{u_2, u_2, u_3, u_2} (RingHom.id R) (↥O) R
hϕ : ∀ (ψ : LinearMap.{u_2, u_2, u_3, u_2} (RingHom.id R) (↥O) R), ¬ϕ.submoduleImage N < ψ.submoduleImage N
inst_4 : (ϕ.submoduleImage N).IsPrincipal
y : M
yN : y ∈ N
ϕy_eq : (ϕ : (a : ↥O) → R) (Subtype.mk (p := fun (x : M) ↦ x ∈ O) y ⋯) = generator (ϕ.submoduleImage N)
ψ : LinearMap.{u_2, u_2, u_3, u_2} (RingHom.id R) (↥O) R
a : R := generator (ϕ.submoduleImage N)
d : R :=
  generator
    (span R (insert a (singleton (α := R) ((ψ : (a : ↥O) → R) (Subtype.mk (p := fun (x : M) ↦ x ∈ O) y ⋯) : R))))
d_dvd_left : d ∣ a
d_dvd_right : d ∣ (ψ : (a : ↥O) → R) (Subtype.mk (p := fun (x : M) ↦ x ∈ O) y ⋯)
r₁ r₂ : R
d_eq : d = r₁ * a + HMul.hMul (β := R) r₂ ((ψ : (a : ↥O) → R) (Subtype.mk (p := fun (x : M) ↦ x ∈ O) y ⋯) : R)
ψ' : LinearMap.{u_2, u_2, u_3, u_2} (RingHom.id R) (↥O) R := r₁ • ϕ + r₂ • ψ
this : R ∙ d ≤ ψ'.submoduleImage N
⊢ LE.le (α := Submodule R R) (R ∙ generator (ϕ.submoduleImage N)) (R ∙ d)

Tactic:
exact Ideal.span_singleton_le_span_singleton.mpr d_dvd_left

Premises used: Iff.mpr, Ideal.span_singleton_le_span_singleton
-- Module: Mathlib.LinearAlgebra.FreeModule.PID
Goal:
R : Type u_2
inst : CommRing R
M : Type u_3
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsPrincipalIdealRing R
N O : Submodule R M
hNO : N ≤ O
ϕ : LinearMap.{u_2, u_2, u_3, u_2} (RingHom.id R) (↥O) R
hϕ : ∀ (ψ : LinearMap.{u_2, u_2, u_3, u_2} (RingHom.id R) (↥O) R), ¬ϕ.submoduleImage N < ψ.submoduleImage N
inst_4 : (ϕ.submoduleImage N).IsPrincipal
y : M
yN : y ∈ N
ϕy_eq : (ϕ : (a : ↥O) → R) (Subtype.mk (p := fun (x : M) ↦ x ∈ O) y ⋯) = generator (ϕ.submoduleImage N)
ψ : LinearMap.{u_2, u_2, u_3, u_2} (RingHom.id R) (↥O) R
a : R := generator (ϕ.submoduleImage N)
d : R :=
  generator
    (span R (insert a (singleton (α := R) ((ψ : (a : ↥O) → R) (Subtype.mk (p := fun (x : M) ↦ x ∈ O) y ⋯) : R))))
d_dvd_left : d ∣ a
d_dvd_right : d ∣ (ψ : (a : ↥O) → R) (Subtype.mk (p := fun (x : M) ↦ x ∈ O) y ⋯)
⊢ Membership.mem (γ := Ideal R)
    (span R (insert a (singleton (α := R) ((ψ : (a : ↥O) → R) (Subtype.mk (p := fun (x : M) ↦ x ∈ O) y ⋯) : R))))
    (generator (ϕ.submoduleImage N))

Tactic:
subset_span (mem_insert _ _)

Premises used: Set.Mem, Set.mem_insert, Submodule.subset_span
-- Module: Mathlib.LinearAlgebra.FreeModule.PID
Goal:
R : Type u_2
inst : CommRing R
M : Type u_3
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsPrincipalIdealRing R
N O : Submodule R M
hNO : N ≤ O
ϕ : LinearMap.{u_2, u_2, u_3, u_2} (RingHom.id R) (↥O) R
hϕ : ∀ (ψ : LinearMap.{u_2, u_2, u_3, u_2} (RingHom.id R) (↥O) R), ¬ϕ.submoduleImage N < ψ.submoduleImage N
inst_4 : (ϕ.submoduleImage N).IsPrincipal
y : M
yN : y ∈ N
ϕy_eq : (ϕ : (a : ↥O) → R) (Subtype.mk (p := fun (x : M) ↦ x ∈ O) y ⋯) = generator (ϕ.submoduleImage N)
ψ : LinearMap.{u_2, u_2, u_3, u_2} (RingHom.id R) (↥O) R
a : R := generator (ϕ.submoduleImage N)
d : R :=
  generator
    (span R (insert a (singleton (α := R) ((ψ : (a : ↥O) → R) (Subtype.mk (p := fun (x : M) ↦ x ∈ O) y ⋯) : R))))
d_dvd_left : d ∣ a
d_dvd_right : d ∣ (ψ : (a : ↥O) → R) (Subtype.mk (p := fun (x : M) ↦ x ∈ O) y ⋯)
⊢ Membership.mem (γ := Ideal R)
    (span R (insert a (singleton (α := R) ((ψ : (a : ↥O) → R) (Subtype.mk (p := fun (x : M) ↦ x ∈ O) y ⋯) : R))))
    (generator (ϕ.submoduleImage N))

Tactic:
exact subset_span (mem_insert _ _)

Premises used: Set.mem_insert, Submodule.subset_span
-- Module: Mathlib.LinearAlgebra.FreeModule.PID
Goal:
ι : Type u_1
R : Type u_2
inst : CommRing R
inst_1 : IsPrincipalIdealRing R
inst_2 : IsDomain R
inst_3 : Finite ι
O : Type u_4
inst_4 : AddCommGroup O
inst_5 : Module R O
M N : Submodule R O
b'M : Basis.{u_1, u_2, u_4} ι R ↥M
N_bot : N ≠ ⊥
N_le_M : N ≤ M
obtain :
  ∀ (P : Submodule R R)
    (P_eq :
      Membership.mem (γ := Set (Submodule R R))
        (range fun (ψ : LinearMap.{u_2, u_2, u_4, u_2} (RingHom.id R) (↥M) R) ↦ ψ.submoduleImage N) P)
    (P_max :
      ∀ (I : Submodule R R),
        Membership.mem (γ := Set (Submodule R R))
            (range fun (ψ : LinearMap.{u_2, u_2, u_4, u_2} (RingHom.id R) (↥M) R) ↦ ψ.submoduleImage N) I →
          ¬P < I),
    ∃ (ϕ : LinearMap.{u_2, u_2, u_4, u_2} (RingHom.id R) (↥M) R),
      ∀ (ψ : LinearMap.{u_2, u_2, u_4, u_2} (RingHom.id R) (↥M) R), ¬ϕ.submoduleImage N < ψ.submoduleImage N
⊢ ∃ (ϕ : LinearMap.{u_2, u_2, u_4, u_2} (RingHom.id R) (↥M) R),
    ∀ (ψ : LinearMap.{u_2, u_2, u_4, u_2} (RingHom.id R) (↥M) R), ¬ϕ.submoduleImage N < ψ.submoduleImage N

Tactic:
obtain ⟨P, P_eq, P_max⟩ :=
      set_has_maximal_iff_noetherian.mpr (inferInstance : IsNoetherian R R) _
        (show (Set.range fun ψ : M →ₗ[R] R ↦ ψ.submoduleImage N).Nonempty from
          ⟨_, Set.mem_range.mpr ⟨0, rfl⟩⟩)

Premises used: Iff.mpr, Set.mem_range, inferInstance, Exists.intro, set_has_maximal_iff_noetherian, OfNat.ofNat, LinearMap.submoduleImage, rfl
-- Module: Mathlib.LinearAlgebra.FreeModule.PID
Goal:
ι : Type u_1
R : Type u_2
inst : CommRing R
inst_1 : IsPrincipalIdealRing R
inst_2 : IsDomain R
inst_3 : Finite ι
O : Type u_4
inst_4 : AddCommGroup O
inst_5 : Module R O
M N : Submodule R O
b'M : Basis.{u_1, u_2, u_4} ι R ↥M
N_bot : N ≠ ⊥
N_le_M : N ≤ M
P : Submodule R R
P_eq :
  Membership.mem (γ := Set (Submodule R R))
    (range fun (ψ : LinearMap.{u_2, u_2, u_4, u_2} (RingHom.id R) (↥M) R) ↦ ψ.submoduleImage N) P
P_max :
  ∀ (I : Submodule R R),
    Membership.mem (γ := Set (Submodule R R))
        (range fun (ψ : LinearMap.{u_2, u_2, u_4, u_2} (RingHom.id R) (↥M) R) ↦ ψ.submoduleImage N) I →
      ¬P < I
obtain :
  ∀ (ϕ : LinearMap.{u_2, u_2, u_4, u_2} (RingHom.id R) (↥M) R)
    (P_eq :
      Membership.mem (γ := Set (Submodule R R))
        (range fun (ψ : LinearMap.{u_2, u_2, u_4, u_2} (RingHom.id R) (↥M) R) ↦ ψ.submoduleImage N)
        (ϕ.submoduleImage N))
    (P_max :
      ∀ (I : Submodule R R),
        Membership.mem (γ := Set (Submodule R R))
            (range fun (ψ : LinearMap.{u_2, u_2, u_4, u_2} (RingHom.id R) (↥M) R) ↦ ψ.submoduleImage N) I →
          ¬ϕ.submoduleImage N < I),
    ∃ (ϕ : LinearMap.{u_2, u_2, u_4, u_2} (RingHom.id R) (↥M) R),
      ∀ (ψ : LinearMap.{u_2, u_2, u_4, u_2} (RingHom.id R) (↥M) R), ¬ϕ.submoduleImage N < ψ.submoduleImage N
⊢ ∃ (ϕ : LinearMap.{u_2, u_2, u_4, u_2} (RingHom.id R) (↥M) R),
    ∀ (ψ : LinearMap.{u_2, u_2, u_4, u_2} (RingHom.id R) (↥M) R), ¬ϕ.submoduleImage N < ψ.submoduleImage N

Tactic:
obtain ⟨ϕ, rfl⟩ := Set.mem_range.mp P_eq

Premises used: Set.mem_range, Iff.mp, rfl
-- Module: Mathlib.LinearAlgebra.FreeModule.PID
Goal:
ι : Type u_1
R : Type u_2
inst : CommRing R
inst_1 : IsPrincipalIdealRing R
inst_2 : IsDomain R
inst_3 : Finite ι
O : Type u_4
inst_4 : AddCommGroup O
inst_5 : Module R O
M N : Submodule R O
b'M : Basis.{u_1, u_2, u_4} ι R ↥M
N_bot : N ≠ ⊥
N_le_M : N ≤ M
ϕ : LinearMap.{u_2, u_2, u_4, u_2} (RingHom.id R) (↥M) R
P_eq :
  Membership.mem (γ := Set (Submodule R R))
    (range fun (ψ : LinearMap.{u_2, u_2, u_4, u_2} (RingHom.id R) (↥M) R) ↦ ψ.submoduleImage N) (ϕ.submoduleImage N)
P_max :
  ∀ (I : Submodule R R),
    Membership.mem (γ := Set (Submodule R R))
        (range fun (ψ : LinearMap.{u_2, u_2, u_4, u_2} (RingHom.id R) (↥M) R) ↦ ψ.submoduleImage N) I →
      ¬ϕ.submoduleImage N < I
⊢ ∃ (ϕ : LinearMap.{u_2, u_2, u_4, u_2} (RingHom.id R) (↥M) R),
    ∀ (ψ : LinearMap.{u_2, u_2, u_4, u_2} (RingHom.id R) (↥M) R), ¬ϕ.submoduleImage N < ψ.submoduleImage N

Tactic:
⟨ϕ, fun ψ hψ ↦ P_max _ ⟨_, rfl⟩ hψ⟩

Premises used: Exists.intro, LinearMap.submoduleImage, rfl
-- Module: Mathlib.LinearAlgebra.FreeModule.PID
Goal:
ι : Type u_1
R : Type u_2
inst : CommRing R
inst_1 : IsPrincipalIdealRing R
inst_2 : IsDomain R
inst_3 : Finite ι
O : Type u_4
inst_4 : AddCommGroup O
inst_5 : Module R O
M N : Submodule R O
b'M : Basis.{u_1, u_2, u_4} ι R ↥M
N_bot : N ≠ ⊥
N_le_M : N ≤ M
ϕ : LinearMap.{u_2, u_2, u_4, u_2} (RingHom.id R) (↥M) R
P_eq :
  Membership.mem (γ := Set (Submodule R R))
    (range fun (ψ : LinearMap.{u_2, u_2, u_4, u_2} (RingHom.id R) (↥M) R) ↦ ψ.submoduleImage N) (ϕ.submoduleImage N)
P_max :
  ∀ (I : Submodule R R),
    Membership.mem (γ := Set (Submodule R R))
        (range fun (ψ : LinearMap.{u_2, u_2, u_4, u_2} (RingHom.id R) (↥M) R) ↦ ψ.submoduleImage N) I →
      ¬ϕ.submoduleImage N < I
⊢ ∃ (ϕ : LinearMap.{u_2, u_2, u_4, u_2} (RingHom.id R) (↥M) R),
    ∀ (ψ : LinearMap.{u_2, u_2, u_4, u_2} (RingHom.id R) (↥M) R), ¬ϕ.submoduleImage N < ψ.submoduleImage N

Tactic:
exact ⟨ϕ, fun ψ hψ ↦ P_max _ ⟨_, rfl⟩ hψ⟩
-- Module: Mathlib.LinearAlgebra.FreeModule.PID
Goal:
ι : Type u_1
R : Type u_2
inst : CommRing R
inst_1 : IsPrincipalIdealRing R
inst_2 : IsDomain R
inst_3 : Finite ι
O : Type u_4
inst_4 : AddCommGroup O
inst_5 : Module R O
M N : Submodule R O
b'M : Basis.{u_1, u_2, u_4} ι R ↥M
N_bot : N ≠ ⊥
N_le_M : N ≤ M
⊢ ∃ (ϕ : LinearMap.{u_2, u_2, u_4, u_2} (RingHom.id R) (↥M) R),
    ∀ (ψ : LinearMap.{u_2, u_2, u_4, u_2} (RingHom.id R) (↥M) R), ¬ϕ.submoduleImage N < ψ.submoduleImage N

Tactic:
have : ∃ ϕ : M →ₗ[R] R, ∀ ψ : M →ₗ[R] R, ¬ϕ.submoduleImage N < ψ.submoduleImage N := by
    obtain ⟨P, P_eq, P_max⟩ :=
      set_has_maximal_iff_noetherian.mpr (inferInstance : IsNoetherian R R) _
        (show (Set.range fun ψ : M →ₗ[R] R ↦ ψ.submoduleImage N).Nonempty from
          ⟨_, Set.mem_range.mpr ⟨0, rfl⟩⟩)
    obtain ⟨ϕ, rfl⟩ := Set.mem_range.mp P_eq
    exact ⟨ϕ, fun ψ hψ ↦ P_max _ ⟨_, rfl⟩ hψ⟩