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)
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
N'_le_M' : N' ≤ M'
N'_le_N : N' ≤ N
y'_ortho_M' : ∀ (c : R), ∀ z ∈ M', c • y' + z = 0 → c = 0
ay'_ortho_N' : ∀ (c : R), ∀ z ∈ N', c • a • y' + z = 0 → c = 0
n' : ℕ
bN' : Basis.{0, u_2, u_4} (Fin n') R ↥N'
z : O
zN : z ∈ N
b : R
hb : (ϕ : (a : ↥M) → R) (Subtype.mk (p := fun (x : O) ↦ x ∈ M) z ⋯) = generator (ϕ.submoduleImage N) * b
neg : Subtype.mk (p := fun (x : O) ↦ x ∈ N) (z - b • y) ⋯ ∈ (ϕ ∘ₗ inclusion N_le_M).ker
neg₁ : (N.subtype : (a : ↥N) → O) (Subtype.mk (p := fun (x : O) ↦ x ∈ N) (z - b • y) ⋯) = z + -b • y
⊢ ∃ (c : R), z + c • y ∈ N'

Tactic:
refine ⟨-b, Submodule.mem_map.mpr ⟨⟨_, N.sub_mem zN (N.smul_mem b yN)⟩, ?_, ?_⟩⟩
-- 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
N'_le_M' : N' ≤ M'
N'_le_N : N' ≤ N
y'_ortho_M' : ∀ (c : R), ∀ z ∈ M', c • y' + z = 0 → c = 0
ay'_ortho_N' : ∀ (c : R), ∀ z ∈ N', c • a • y' + z = 0 → c = 0
n' : ℕ
bN' : Basis.{0, u_2, u_4} (Fin n') R ↥N'
z : O
zN : z ∈ N
b : R
hb : (ϕ : (a : ↥M) → R) (Subtype.mk (p := fun (x : O) ↦ x ∈ M) z ⋯) = generator (ϕ.submoduleImage N) * b
⊢ Subtype.mk (p := fun (x : O) ↦ x ∈ N) (z - b • y) ⋯ ∈ (ϕ ∘ₗ inclusion N_le_M).ker

Tactic:
LinearMap.mem_ker.mpr (show ϕ (⟨z, N_le_M zN⟩ - b • ⟨y, N_le_M yN⟩) = 0 from ?_)

Premises used: Iff.mpr, LinearMap.mem_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
N'_le_M' : N' ≤ M'
N'_le_N : N' ≤ N
y'_ortho_M' : ∀ (c : R), ∀ z ∈ M', c • y' + z = 0 → c = 0
ay'_ortho_N' : ∀ (c : R), ∀ z ∈ N', c • a • y' + z = 0 → c = 0
n' : ℕ
bN' : Basis.{0, u_2, u_4} (Fin n') R ↥N'
z : O
zN : z ∈ N
b : R
hb : (ϕ : (a : ↥M) → R) (Subtype.mk (p := fun (x : O) ↦ x ∈ M) z ⋯) = generator (ϕ.submoduleImage N) * b
⊢ (N.subtype : (a : ↥N) → O) (Subtype.mk (p := fun (x : O) ↦ x ∈ N) (z - b • y) ⋯) = z + -b • y

Tactic:
simp only [sub_eq_add_neg, neg_smul, coe_subtype]

Premises used: neg_smul, sub_eq_add_neg, Submodule.coe_subtype
-- 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
N'_le_M' : N' ≤ M'
N'_le_N : N' ≤ N
y'_ortho_M' : ∀ (c : R), ∀ z ∈ M', c • y' + z = 0 → c = 0
ay'_ortho_N' : ∀ (c : R), ∀ z ∈ N', c • a • y' + z = 0 → c = 0
n' : ℕ
bN' : Basis.{0, u_2, u_4} (Fin n') 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)),
            (↑((Basis.mkFinConsOfLE y yN bN' N'_le_N ⋯ ⋯ : (a : Fin (n' + 1)) → ↥N) i) : O) =
              HSMul.hSMul (β := O) (as' i) (↑((bM : (a : Fin (m' + 1)) → ↥M) (Fin.castLE hnm i)) : O)

Tactic:
⟨Nat.succ_le_succ hn'm', ?_, ?_⟩

Premises used: Exists.intro, Nat.succ_le_succ
-- 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
N'_le_M' : N' ≤ M'
N'_le_N : N' ≤ N
y'_ortho_M' : ∀ (c : R), ∀ z ∈ M', c • y' + z = 0 → c = 0
ay'_ortho_N' : ∀ (c : R), ∀ z ∈ N', c • a • y' + z = 0 → c = 0
n' : ℕ
bN' : Basis.{0, u_2, u_4} (Fin n') R ↥N'
m' : ℕ
hn'm' : n' ≤ m'
bM' : Basis.{0, u_2, u_4} (Fin m') R ↥M'
neg : ∀ z ∈ M, ∃ (c : R), z + c • y' ∈ M'
⊢ Basis.{0, u_2, u_4} (Fin (m' + 1)) R ↥M

Tactic:
refine Basis.mkFinConsOfLE y' y'M bM' M'_le_M y'_ortho_M' ?_

Premises used: Module.Basis.mkFinConsOfLE
-- 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
N'_le_M' : N' ≤ M'
N'_le_N : N' ≤ N
y'_ortho_M' : ∀ (c : R), ∀ z ∈ M', c • y' + z = 0 → c = 0
ay'_ortho_N' : ∀ (c : R), ∀ z ∈ N', c • a • y' + z = 0 → c = 0
n' : ℕ
bN' : Basis.{0, u_2, u_4} (Fin n') R ↥N'
m' : ℕ
hn'm' : n' ≤ m'
bM' : Basis.{0, u_2, u_4} (Fin m') R ↥M'
z : O
zM : z ∈ M
⊢ ∃ (c : R), z + c • y' ∈ M'

Tactic:
⟨-ϕ ⟨z, zM⟩, ⟨⟨z, zM⟩ - ϕ ⟨z, zM⟩ • ⟨y', y'M⟩, LinearMap.mem_ker.mpr ?_, ?_⟩⟩

Premises used: Iff.mpr, HSub.hSub, LinearMap.mem_ker, Subtype.mk, And.intro, Exists.intro, HSMul.hSMul, DFunLike.coe, Neg.neg
-- 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
N'_le_M' : N' ≤ M'
N'_le_N : N' ≤ N
y'_ortho_M' : ∀ (c : R), ∀ z ∈ M', c • y' + z = 0 → c = 0
ay'_ortho_N' : ∀ (c : R), ∀ z ∈ N', c • a • y' + z = 0 → c = 0
n' : ℕ
bN' : Basis.{0, u_2, u_4} (Fin n') R ↥N'
m' : ℕ
hn'm' : n' ≤ m'
bM' : Basis.{0, u_2, u_4} (Fin m') R ↥M'
z : O
zM : z ∈ M
neg :
  Eq.{u_2 + 1} (α := R)
    ((ϕ : (a : ↥M) → R)
        (Subtype.mk (p := fun (x : O) ↦ x ∈ M) z zM -
          HSMul.hSMul.{u_2, u_4, u_4} (α := R) ((ϕ : (a : ↥M) → R) (Subtype.mk (p := fun (x : O) ↦ x ∈ M) z zM) : R)
            (Subtype.mk (p := fun (x : O) ↦ x ∈ M) y' y'M)) :
      R)
    (0 : R)
neg₁ :
  (M.subtype : (a : ↥M) → O)
      (Subtype.mk (p := fun (x : O) ↦ x ∈ M) z zM -
        HSMul.hSMul.{u_2, u_4, u_4} (α := R) ((ϕ : (a : ↥M) → R) (Subtype.mk (p := fun (x : O) ↦ x ∈ M) z zM) : R)
          (Subtype.mk (p := fun (x : O) ↦ x ∈ M) y' y'M)) =
    z + HSMul.hSMul.{u_2, u_4, u_4} (α := R) (-(ϕ : (a : ↥M) → R) (Subtype.mk (p := fun (x : O) ↦ x ∈ M) z zM) : R) y'
⊢ ∃ (c : R), z + c • y' ∈ M'

Tactic:
refine ⟨-ϕ ⟨z, zM⟩, ⟨⟨z, zM⟩ - ϕ ⟨z, zM⟩ • ⟨y', y'M⟩, LinearMap.mem_ker.mpr ?_, ?_⟩⟩
-- 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
N'_le_M' : N' ≤ M'
N'_le_N : N' ≤ N
y'_ortho_M' : ∀ (c : R), ∀ z ∈ M', c • y' + z = 0 → c = 0
ay'_ortho_N' : ∀ (c : R), ∀ z ∈ N', c • a • y' + z = 0 → c = 0
n' : ℕ
bN' : Basis.{0, u_2, u_4} (Fin n') R ↥N'
m' : ℕ
hn'm' : n' ≤ m'
bM' : Basis.{0, u_2, u_4} (Fin m') R ↥M'
z : O
zM : z ∈ M
⊢ HAdd.hAdd (α := O) ((M.subtype : (a : ↥M) → O) (Subtype.mk (p := fun (x : O) ↦ x ∈ M) z zM) : O)
      (-HSMul.hSMul.{u_2, u_4, u_4} (α := R) (β := O)
          ((ϕ : (a : ↥M) → R) (Subtype.mk (p := fun (x : O) ↦ x ∈ M) z zM) : R)
          ((M.subtype : (a : ↥M) → O) (Subtype.mk (p := fun (x : O) ↦ x ∈ M) y' y'M) : O)) =
    z + -HSMul.hSMul.{u_2, u_4, u_4} (α := R) ((ϕ : (a : ↥M) → R) (Subtype.mk (p := fun (x : O) ↦ x ∈ M) z zM) : R) y'

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_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
N'_le_M' : N' ≤ M'
N'_le_N : N' ≤ N
y'_ortho_M' : ∀ (c : R), ∀ z ∈ M', c • y' + z = 0 → c = 0
ay'_ortho_N' : ∀ (c : R), ∀ z ∈ N', c • a • y' + z = 0 → c = 0
n' : ℕ
bN' : Basis.{0, u_2, u_4} (Fin n') R ↥N'
m' : ℕ
hn'm' : n' ≤ m'
bM' : Basis.{0, u_2, u_4} (Fin m') R ↥M'
as : Fin n' → R
h :
  ∀ (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)),
      (↑((Basis.mkFinConsOfLE y yN bN' N'_le_N ⋯ ⋯ : (a : Fin (n' + 1)) → ↥N) i) : O) =
        HSMul.hSMul (β := O) (as' i)
          (↑((Basis.mkFinConsOfLE y' y'M bM' M'_le_M y'_ortho_M' ⋯ : (a : Fin (m' + 1)) → ↥M) (Fin.castLE ⋯ i)) : O)

Tactic:
⟨Fin.cons a as, ?_⟩

Premises used: Fin.cons, Exists.intro