awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
this :
  ∃ (ϕ : 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 :=
  this.choose (p := fun (ϕ : 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)
ϕ_max :
  ∀ (ψ : LinearMap.{u_2, u_2, u_4, u_2} (RingHom.id R) (↥M) R),
    ¬this.choose (p := fun (ϕ : 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).submoduleImage
          N <
        ψ.submoduleImage N
a : R := generator (ϕ.submoduleImage N)
a_mem : a ∈ ϕ.submoduleImage N
a_zero : ¬a = 0
y : O
yN : y ∈ N
ϕy_eq : (ϕ : (a : ↥M) → R) (Subtype.mk (p := fun (x : O) ↦ x ∈ M) y ⋯) = a
c : (i : ι) → R
hc : ∀ (i : ι), (b'M.coord i : (a : ↥M) → R) (Subtype.mk (p := fun (x : O) ↦ x ∈ M) y ⋯) = a * c i
val : Fintype ι
y' : O := ∑ i : ι, HSMul.hSMul (β := O) (c i) (↑((b'M : (a : ι) → ↥M) i) : O)
y'M : y' ∈ M
mk_y' :
  Subtype.mk (p := fun (x : O) ↦ x ∈ M) y' y'M = ∑ i : ι, HSMul.hSMul (β := ↥M) (c i) ((b'M : (a : ι) → ↥M) i : ↥M)
refine :
  ∀ (i : ι),
    Membership.mem (γ := Finset ι) Finset.univ i →
      a • HSMul.hSMul (β := ↥M) (c i) ((b'M : (a : ι) → ↥M) i : ↥M) =
        HSMul.hSMul.{u_2, u_4, u_4} (α := R) (β := ↥M)
          ((((b'M.repr : (a : ↥M) → ι →₀ R) (Subtype.mk (p := fun (x : O) ↦ x ∈ M) y ⋯) : ι →₀ R) : (a : ι) → R) i : R)
          ((b'M : (a : ι) → ↥M) i : ↥M)
⊢ Eq.{u_4 + 1} (α := ↥M) (∑ x : ι, a • HSMul.hSMul (β := ↥M) (c x) ((b'M : (a : ι) → ↥M) x : ↥M))
    (∑ i : ι,
      HSMul.hSMul.{u_2, u_4, u_4} (α := R) (β := ↥M)
        ((((b'M.repr : (a : ↥M) → ι →₀ R) (Subtype.mk (p := fun (x : O) ↦ x ∈ M) y ⋯) : ι →₀ R) : (a : ι) → R) i : R)
        ((b'M : (a : ι) → ↥M) i : ↥M))

Tactic:
refine Finset.sum_congr rfl fun i _ ↦ ?_

Premises used: Finset.sum_congr, 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
this :
  ∃ (ϕ : 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 :=
  this.choose (p := fun (ϕ : 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)
ϕ_max :
  ∀ (ψ : LinearMap.{u_2, u_2, u_4, u_2} (RingHom.id R) (↥M) R),
    ¬this.choose (p := fun (ϕ : 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).submoduleImage
          N <
        ψ.submoduleImage N
a : R := generator (ϕ.submoduleImage N)
a_mem : a ∈ ϕ.submoduleImage N
a_zero : ¬a = 0
y : O
yN : y ∈ N
ϕy_eq : (ϕ : (a : ↥M) → R) (Subtype.mk (p := fun (x : O) ↦ x ∈ M) y ⋯) = a
c : (i : ι) → R
hc : ∀ (i : ι), (b'M.coord i : (a : ↥M) → R) (Subtype.mk (p := fun (x : O) ↦ x ∈ M) y ⋯) = a * c i
val : Fintype ι
y' : O := ∑ i : ι, HSMul.hSMul (β := O) (c i) (↑((b'M : (a : ι) → ↥M) i) : O)
y'M : y' ∈ M
mk_y' :
  Subtype.mk (p := fun (x : O) ↦ x ∈ M) y' y'M = ∑ i : ι, HSMul.hSMul (β := ↥M) (c i) ((b'M : (a : ι) → ↥M) i : ↥M)
i : ι
h : Membership.mem (γ := Finset ι) Finset.univ i
rw :
  HSMul.hSMul.{u_2, u_4, u_4} (α := R) (β := ↥M)
      ((b'M.coord i : (a : ↥M) → R) (Subtype.mk (p := fun (x : O) ↦ x ∈ M) y ⋯) : R) ((b'M : (a : ι) → ↥M) i : ↥M) =
    HSMul.hSMul.{u_2, u_4, u_4} (α := R) (β := ↥M)
      ((((b'M.repr : (a : ↥M) → ι →₀ R) (Subtype.mk (p := fun (x : O) ↦ x ∈ M) y ⋯) : ι →₀ R) : (a : ι) → R) i : R)
      ((b'M : (a : ι) → ↥M) i : ↥M)
⊢ a • HSMul.hSMul (β := ↥M) (c i) ((b'M : (a : ι) → ↥M) i : ↥M) =
    HSMul.hSMul.{u_2, u_4, u_4} (α := R) (β := ↥M)
      ((((b'M.repr : (a : ↥M) → ι →₀ R) (Subtype.mk (p := fun (x : O) ↦ x ∈ M) y ⋯) : ι →₀ R) : (a : ι) → R) i : R)
      ((b'M : (a : ι) → ↥M) i : ↥M)

Tactic:
rw [← mul_smul, ← hc]

Premises used: SemigroupAction.mul_smul
-- 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
this :
  ∃ (ϕ : 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 :=
  this.choose (p := fun (ϕ : 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)
ϕ_max :
  ∀ (ψ : LinearMap.{u_2, u_2, u_4, u_2} (RingHom.id R) (↥M) R),
    ¬this.choose (p := fun (ϕ : 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).submoduleImage
          N <
        ψ.submoduleImage N
a : R := generator (ϕ.submoduleImage N)
a_mem : a ∈ ϕ.submoduleImage N
a_zero : ¬a = 0
y : O
yN : y ∈ N
ϕy_eq : (ϕ : (a : ↥M) → R) (Subtype.mk (p := fun (x : O) ↦ x ∈ M) y ⋯) = a
c : (i : ι) → R
hc : ∀ (i : ι), (b'M.coord i : (a : ↥M) → R) (Subtype.mk (p := fun (x : O) ↦ x ∈ M) y ⋯) = a * c i
val : Fintype ι
y' : O := ∑ i : ι, HSMul.hSMul (β := O) (c i) (↑((b'M : (a : ι) → ↥M) i) : O)
y'M : y' ∈ M
mk_y' :
  Subtype.mk (p := fun (x : O) ↦ x ∈ M) y' y'M = ∑ i : ι, HSMul.hSMul (β := ↥M) (c i) ((b'M : (a : ι) → ↥M) i : ↥M)
i : ι
h : Membership.mem (γ := Finset ι) Finset.univ i
⊢ HSMul.hSMul.{u_2, u_4, u_4} (α := R) (β := ↥M)
      ((b'M.coord i : (a : ↥M) → R) (Subtype.mk (p := fun (x : O) ↦ x ∈ M) y ⋯) : R) ((b'M : (a : ι) → ↥M) i : ↥M) =
    HSMul.hSMul.{u_2, u_4, u_4} (α := R) (β := ↥M)
      ((((b'M.repr : (a : ↥M) → ι →₀ R) (Subtype.mk (p := fun (x : O) ↦ x ∈ M) y ⋯) : ι →₀ R) : (a : ι) → R) i : R)
      ((b'M : (a : ι) → ↥M) i : ↥M)

Tactic:
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
this :
  ∃ (ϕ : 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 :=
  this.choose (p := fun (ϕ : 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)
ϕ_max :
  ∀ (ψ : LinearMap.{u_2, u_2, u_4, u_2} (RingHom.id R) (↥M) R),
    ¬this.choose (p := fun (ϕ : 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).submoduleImage
          N <
        ψ.submoduleImage N
a : R := generator (ϕ.submoduleImage N)
a_mem : a ∈ ϕ.submoduleImage N
a_zero : ¬a = 0
y : O
yN : y ∈ N
ϕy_eq : (ϕ : (a : ↥M) → R) (Subtype.mk (p := fun (x : O) ↦ x ∈ M) y ⋯) = a
c : (i : ι) → R
hc : ∀ (i : ι), (b'M.coord i : (a : ↥M) → R) (Subtype.mk (p := fun (x : O) ↦ x ∈ M) y ⋯) = a * c i
val : Fintype ι
y' : O := ∑ i : ι, HSMul.hSMul (β := O) (c i) (↑((b'M : (a : ι) → ↥M) i) : O)
y'M : y' ∈ M
mk_y' :
  Subtype.mk (p := fun (x : O) ↦ x ∈ M) y' y'M = ∑ i : ι, HSMul.hSMul (β := ↥M) (c i) ((b'M : (a : ι) → ↥M) i : ↥M)
⊢ a • y' = y

Tactic:
have a_smul_y' : a • y' = y := by
    refine Subtype.mk_eq_mk.mp (show (a • ⟨y', y'M⟩ : M) = ⟨y, N_le_M yN⟩ from ?_)
    rw [← b'M.sum_repr ⟨y, N_le_M yN⟩, mk_y', Finset.smul_sum]
    refine Finset.sum_congr rfl fun i _ ↦ ?_
    rw [← mul_smul, ← hc]
    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
this :
  ∃ (ϕ : 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 :=
  this.choose (p := fun (ϕ : 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)
ϕ_max :
  ∀ (ψ : LinearMap.{u_2, u_2, u_4, u_2} (RingHom.id R) (↥M) R),
    ¬this.choose (p := fun (ϕ : 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).submoduleImage
          N <
        ψ.submoduleImage N
a : R := generator (ϕ.submoduleImage N)
a_mem : a ∈ ϕ.submoduleImage N
a_zero : ¬a = 0
y : O
yN : y ∈ N
ϕy_eq : (ϕ : (a : ↥M) → R) (Subtype.mk (p := fun (x : O) ↦ x ∈ M) y ⋯) = a
c : (i : ι) → R
hc : ∀ (i : ι), (b'M.coord i : (a : ↥M) → R) (Subtype.mk (p := fun (x : O) ↦ x ∈ M) y ⋯) = a * c i
val : Fintype ι
y' : O := ∑ i : ι, HSMul.hSMul (β := O) (c i) (↑((b'M : (a : ι) → ↥M) i) : O)
y'M : y' ∈ M
mk_y' :
  Subtype.mk (p := fun (x : O) ↦ x ∈ M) y' y'M = ∑ i : ι, HSMul.hSMul (β := ↥M) (c i) ((b'M : (a : ι) → ↥M) i : ↥M)
a_smul_y' : a • y' = y
⊢ ∃ y ∈ M,
    ∃ (a : R),
      a • y ∈ N ∧
        ∃ M' ≤ M,
          ∃ N' ≤ N,
            N' ≤ M' ∧
              (∀ (c : R), ∀ z ∈ M', c • y + z = 0 → c = 0) ∧
                (∀ (c : R), ∀ z ∈ N', c • a • y + z = 0 → c = 0) ∧
                  ∀ (n' : ℕ) (bN' : Basis.{0, u_2, u_4} (Fin n') R ↥N'),
                    ∃ (bN : Basis.{0, u_2, u_4} (Fin (n' + 1)) R ↥N),
                      ∀ (m' : ℕ) (hn'm' : n' ≤ m') (bM' : Basis.{0, u_2, u_4} (Fin m') R ↥M'),
                        ∃ (hnm : n' + 1 ≤ m' + 1) (bM : Basis.{0, u_2, u_4} (Fin (m' + 1)) R ↥M),
                          ∀ (as : Fin n' → R),
                            (∀ (i : Fin n'),
                                (↑((bN' : (a : Fin n') → ↥N') i) : O) =
                                  HSMul.hSMul (β := O) (as i)
                                    (↑((bM' : (a : Fin m') → ↥M') (Fin.castLE hn'm' i)) : O)) →
                              ∃ (as' : Fin (n' + 1) → R),
                                ∀ (i : Fin (n' + 1)),
                                  (↑((bN : (a : Fin (n' + 1)) → ↥N) i) : O) =
                                    HSMul.hSMul (β := O) (as' i)
                                      (↑((bM : (a : Fin (m' + 1)) → ↥M) (Fin.castLE hnm i)) : O)

Tactic:
⟨y', y'M, a, a_smul_y'.symm ▸ yN, ?_⟩

Premises used: Eq.rec, And.intro, Exists.intro, Eq.symm
-- 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
this :
  ∃ (ϕ : 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 :=
  this.choose (p := fun (ϕ : 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)
ϕ_max :
  ∀ (ψ : LinearMap.{u_2, u_2, u_4, u_2} (RingHom.id R) (↥M) R),
    ¬this.choose (p := fun (ϕ : 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).submoduleImage
          N <
        ψ.submoduleImage N
a : R := generator (ϕ.submoduleImage N)
a_mem : a ∈ ϕ.submoduleImage N
a_zero : ¬a = 0
y : O
yN : y ∈ N
ϕy_eq : (ϕ : (a : ↥M) → R) (Subtype.mk (p := fun (x : O) ↦ x ∈ M) y ⋯) = a
c : (i : ι) → R
hc : ∀ (i : ι), (b'M.coord i : (a : ↥M) → R) (Subtype.mk (p := fun (x : O) ↦ x ∈ M) y ⋯) = a * c i
val : Fintype ι
y' : O := ∑ i : ι, HSMul.hSMul (β := O) (c i) (↑((b'M : (a : ι) → ↥M) i) : O)
y'M : y' ∈ M
mk_y' :
  Subtype.mk (p := fun (x : O) ↦ x ∈ M) y' y'M = ∑ i : ι, HSMul.hSMul (β := ↥M) (c i) ((b'M : (a : ι) → ↥M) i : ↥M)
a_smul_y' : a • y' = y
⊢ Eq.{u_2 + 1} (α := R) ((ϕ : (a : ↥M) → R) (Subtype.mk (p := fun (x : O) ↦ x ∈ M) (a • y') ⋯) : R)
    ((ϕ : (a : ↥M) → R) (Subtype.mk (p := fun (x : O) ↦ x ∈ M) y ⋯) : R)

Tactic:
simp only [a_smul_y']
-- 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
this :
  ∃ (ϕ : 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 :=
  this.choose (p := fun (ϕ : 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)
ϕ_max :
  ∀ (ψ : LinearMap.{u_2, u_2, u_4, u_2} (RingHom.id R) (↥M) R),
    ¬this.choose (p := fun (ϕ : 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).submoduleImage
          N <
        ψ.submoduleImage N
a : R := generator (ϕ.submoduleImage N)
a_mem : a ∈ ϕ.submoduleImage N
a_zero : ¬a = 0
y : O
yN : y ∈ N
ϕy_eq : (ϕ : (a : ↥M) → R) (Subtype.mk (p := fun (x : O) ↦ x ∈ M) y ⋯) = a
c : (i : ι) → R
hc : ∀ (i : ι), (b'M.coord i : (a : ↥M) → R) (Subtype.mk (p := fun (x : O) ↦ x ∈ M) y ⋯) = a * c i
val : Fintype ι
y' : O := ∑ i : ι, HSMul.hSMul (β := O) (c i) (↑((b'M : (a : ι) → ↥M) i) : O)
y'M : y' ∈ M
mk_y' :
  Subtype.mk (p := fun (x : O) ↦ x ∈ M) y' y'M = ∑ i : ι, HSMul.hSMul (β := ↥M) (c i) ((b'M : (a : ι) → ↥M) i : ↥M)
a_smul_y' : a • y' = y
⊢ Eq.{u_2 + 1} (α := R) ((ϕ : (a : ↥M) → R) (Subtype.mk (p := fun (x : O) ↦ x ∈ M) y' y'M) : R) (1 : R)

Tactic:
have ϕy'_eq : ϕ ⟨y', y'M⟩ = 1 :=
    mul_left_cancel₀ a_zero
      (calc
        a • ϕ ⟨y', y'M⟩ = ϕ ⟨a • y', _⟩ := (ϕ.map_smul a ⟨y', y'M⟩).symm
        _ = ϕ ⟨y, N_le_M yN⟩ := by simp only [a_smul_y']
        _ = a := ϕy_eq
        _ = a * 1 := (mul_one a).symm)
-- 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
this :
  ∃ (ϕ : 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 :=
  this.choose (p := fun (ϕ : 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)
ϕ_max :
  ∀ (ψ : LinearMap.{u_2, u_2, u_4, u_2} (RingHom.id R) (↥M) R),
    ¬this.choose (p := fun (ϕ : 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).submoduleImage
          N <
        ψ.submoduleImage N
a : R := generator (ϕ.submoduleImage N)
a_mem : a ∈ ϕ.submoduleImage N
a_zero : ¬a = 0
y : O
yN : y ∈ N
ϕy_eq : (ϕ : (a : ↥M) → R) (Subtype.mk (p := fun (x : O) ↦ x ∈ M) y ⋯) = a
c : (i : ι) → R
hc : ∀ (i : ι), (b'M.coord i : (a : ↥M) → R) (Subtype.mk (p := fun (x : O) ↦ x ∈ M) y ⋯) = a * c i
val : Fintype ι
y' : O := ∑ i : ι, HSMul.hSMul (β := O) (c i) (↑((b'M : (a : ι) → ↥M) i) : O)
y'M : y' ∈ M
mk_y' :
  Subtype.mk (p := fun (x : O) ↦ x ∈ M) y' y'M = ∑ i : ι, HSMul.hSMul (β := ↥M) (c i) ((b'M : (a : ι) → ↥M) i : ↥M)
a_smul_y' : a • y' = y
ϕy'_eq : Eq.{u_2 + 1} (α := R) ((ϕ : (a : ↥M) → R) (Subtype.mk (p := fun (x : O) ↦ x ∈ M) y' y'M) : R) (1 : R)
⊢ Ne.{u_2 + 1} (α := R) ((ϕ : (a : ↥M) → R) (Subtype.mk (p := fun (x : O) ↦ x ∈ M) y' y'M) : R) (0 : R)

Tactic:
simpa only [ϕy'_eq] using one_ne_zero

Premises used: one_ne_zero
-- 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
this :
  ∃ (ϕ : 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 :=
  this.choose (p := fun (ϕ : 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)
ϕ_max :
  ∀ (ψ : LinearMap.{u_2, u_2, u_4, u_2} (RingHom.id R) (↥M) R),
    ¬this.choose (p := fun (ϕ : 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).submoduleImage
          N <
        ψ.submoduleImage N
a : R := generator (ϕ.submoduleImage N)
a_mem : a ∈ ϕ.submoduleImage N
a_zero : ¬a = 0
y : O
yN : y ∈ N
ϕy_eq : (ϕ : (a : ↥M) → R) (Subtype.mk (p := fun (x : O) ↦ x ∈ M) y ⋯) = a
c : (i : ι) → R
hc : ∀ (i : ι), (b'M.coord i : (a : ↥M) → R) (Subtype.mk (p := fun (x : O) ↦ x ∈ M) y ⋯) = a * c i
val : Fintype ι
y' : O := ∑ i : ι, HSMul.hSMul (β := O) (c i) (↑((b'M : (a : ι) → ↥M) i) : O)
y'M : y' ∈ M
mk_y' :
  Subtype.mk (p := fun (x : O) ↦ x ∈ M) y' y'M = ∑ i : ι, HSMul.hSMul (β := ↥M) (c i) ((b'M : (a : ι) → ↥M) i : ↥M)
a_smul_y' : a • y' = y
ϕy'_eq : Eq.{u_2 + 1} (α := R) ((ϕ : (a : ↥M) → R) (Subtype.mk (p := fun (x : O) ↦ x ∈ M) y' y'M) : R) (1 : R)
⊢ Ne.{u_2 + 1} (α := R) ((ϕ : (a : ↥M) → R) (Subtype.mk (p := fun (x : O) ↦ x ∈ M) y' y'M) : R) (0 : R)

Tactic:
have ϕy'_ne_zero : ϕ ⟨y', y'M⟩ ≠ 0 := by simpa only [ϕy'_eq] using one_ne_zero
-- 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
this :
  ∃ (ϕ : 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 :=
  this.choose (p := fun (ϕ : 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)
ϕ_max :
  ∀ (ψ : LinearMap.{u_2, u_2, u_4, u_2} (RingHom.id R) (↥M) R),
    ¬this.choose (p := fun (ϕ : 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).submoduleImage
          N <
        ψ.submoduleImage N
a : R := generator (ϕ.submoduleImage N)
a_mem : a ∈ ϕ.submoduleImage N
a_zero : ¬a = 0
y : O
yN : y ∈ N
ϕy_eq : (ϕ : (a : ↥M) → R) (Subtype.mk (p := fun (x : O) ↦ x ∈ M) y ⋯) = a
c : (i : ι) → R
hc : ∀ (i : ι), (b'M.coord i : (a : ↥M) → R) (Subtype.mk (p := fun (x : O) ↦ x ∈ M) y ⋯) = a * c i
val : Fintype ι
y' : O := ∑ i : ι, HSMul.hSMul (β := O) (c i) (↑((b'M : (a : ι) → ↥M) i) : O)
y'M : y' ∈ M
mk_y' :
  Subtype.mk (p := fun (x : O) ↦ x ∈ M) y' y'M = ∑ i : ι, HSMul.hSMul (β := ↥M) (c i) ((b'M : (a : ι) → ↥M) i : ↥M)
a_smul_y' : a • y' = y
ϕy'_eq : Eq.{u_2 + 1} (α := R) ((ϕ : (a : ↥M) → R) (Subtype.mk (p := fun (x : O) ↦ x ∈ M) y' y'M) : R) (1 : R)
ϕy'_ne_zero : Ne.{u_2 + 1} (α := R) ((ϕ : (a : ↥M) → R) (Subtype.mk (p := fun (x : O) ↦ x ∈ M) y' y'M) : R) (0 : R)
M' : Submodule R O := map M.subtype ϕ.ker
N' : Submodule R O := map N.subtype (ϕ ∘ₗ inclusion N_le_M).ker
⊢ M' ≤ M

Tactic:
have M'_le_M : M' ≤ M := M.map_subtype_le (LinearMap.ker ϕ)
-- 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
this :
  ∃ (ϕ : 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 :=
  this.choose (p := fun (ϕ : 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)
ϕ_max :
  ∀ (ψ : LinearMap.{u_2, u_2, u_4, u_2} (RingHom.id R) (↥M) R),
    ¬this.choose (p := fun (ϕ : 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).submoduleImage
          N <
        ψ.submoduleImage N
a : R := generator (ϕ.submoduleImage N)
a_mem : a ∈ ϕ.submoduleImage N
a_zero : ¬a = 0
y : O
yN : y ∈ N
ϕy_eq : (ϕ : (a : ↥M) → R) (Subtype.mk (p := fun (x : O) ↦ x ∈ M) y ⋯) = a
c : (i : ι) → R
hc : ∀ (i : ι), (b'M.coord i : (a : ↥M) → R) (Subtype.mk (p := fun (x : O) ↦ x ∈ M) y ⋯) = a * c i
val : Fintype ι
y' : O := ∑ i : ι, HSMul.hSMul (β := O) (c i) (↑((b'M : (a : ι) → ↥M) i) : O)
y'M : y' ∈ M
mk_y' :
  Subtype.mk (p := fun (x : O) ↦ x ∈ M) y' y'M = ∑ i : ι, HSMul.hSMul (β := ↥M) (c i) ((b'M : (a : ι) → ↥M) i : ↥M)
a_smul_y' : a • y' = y
ϕy'_eq : Eq.{u_2 + 1} (α := R) ((ϕ : (a : ↥M) → R) (Subtype.mk (p := fun (x : O) ↦ x ∈ M) y' y'M) : R) (1 : R)
ϕy'_ne_zero : Ne.{u_2 + 1} (α := R) ((ϕ : (a : ↥M) → R) (Subtype.mk (p := fun (x : O) ↦ x ∈ M) y' y'M) : R) (0 : R)
M' : Submodule R O := map M.subtype ϕ.ker
N' : Submodule R O := map N.subtype (ϕ ∘ₗ inclusion N_le_M).ker
M'_le_M : M' ≤ M
x : O
hx : x ∈ N'
⊢ ∃ (y : ↥N),
    Eq.{u_2 + 1} (α := R) ((ϕ ∘ₗ inclusion N_le_M : (a : ↥N) → R) y : R) (0 : R) ∧ (N.subtype : (a : ↥N) → O) y = x

Tactic:
simp only [N', mem_map, LinearMap.mem_ker] at hx ⊢

Premises used: Submodule.mem_map, LinearMap.mem_ker