awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.FreeModule.PID (hypothesis)
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'
⊢ x ∈ M'
have hx₁ : ∃ (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 ⊢
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.LinearAlgebra.FreeModule.PID (goal)
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 :
  ∃ (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
⊢ x ∈ M'
have obtain : ∀ (x : O) (xN : x ∈ N)
  (hx :
    Eq.{u_2 + 1} (α := R) ((ϕ ∘ₗ inclusion N_le_M : (a : ↥N) → R) (Subtype.mk (p := fun (x : O) ↦ x ∈ N) x xN) : R)
      (0 : R)),
  Membership.mem (α := O) M' ((N.subtype : (a : ↥N) → O) (Subtype.mk (p := fun (x : O) ↦ x ∈ N) x xN) : O)
Tactic: obtain ⟨⟨x, xN⟩, hx, rfl⟩ := hx
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.LinearAlgebra.FreeModule.PID (hypothesis)
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'
⊢ ∃ 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)
have N'_le_N : N' ≤ N
Tactic: have N'_le_N : N' ≤ N := N.map_subtype_le (LinearMap.ker (ϕ.comp (inclusion N_le_M)))
-- Lean 4 proof step from Mathlib.LinearAlgebra.FreeModule.PID (goal)
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_1 : (i : ι) → R
hc_1 : ∀ (i : ι), (b'M.coord i : (a : ↥M) → R) (Subtype.mk (p := fun (x : O) ↦ x ∈ M) y ⋯) = a * c_1 i
val : Fintype ι
y' : O := ∑ i : ι, HSMul.hSMul (β := O) (c_1 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_1 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
c : R
x : O
xM' : x ∈ M'
hc : c • y' + x = 0
⊢ c = 0
have obtain : ∀ (x : O) (xM : x ∈ M) (hx' : Subtype.mk (p := fun (x : O) ↦ x ∈ M) x xM ∈ ϕ.ker)
  (xM' : Membership.mem (α := O) M' ((M.subtype : (a : ↥M) → O) (Subtype.mk (p := fun (x : O) ↦ x ∈ M) x xM) : O))
  (hc : HAdd.hAdd (β := O) (c • y') ((M.subtype : (a : ↥M) → O) (Subtype.mk (p := fun (x : O) ↦ x ∈ M) x xM) : O) = 0),
  c = 0
Tactic: obtain ⟨⟨x, xM⟩, hx', rfl⟩ := Submodule.mem_map.mp xM'
Cleared hypotheses: x, xM', hc
-- Lean 4 proof step from Mathlib.LinearAlgebra.FreeModule.PID (hypothesis)
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_1 : (i : ι) → R
hc_1 : ∀ (i : ι), (b'M.coord i : (a : ↥M) → R) (Subtype.mk (p := fun (x : O) ↦ x ∈ M) y ⋯) = a * c_1 i
val : Fintype ι
y' : O := ∑ i : ι, HSMul.hSMul (β := O) (c_1 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_1 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
c : R
x : O
xM : x ∈ M
hx' : Subtype.mk (p := fun (x : O) ↦ x ∈ M) x xM ∈ ϕ.ker
xM' : Membership.mem (α := O) M' ((M.subtype : (a : ↥M) → O) (Subtype.mk (p := fun (x : O) ↦ x ∈ M) x xM) : O)
hc : HAdd.hAdd (β := O) (c • y') ((M.subtype : (a : ↥M) → O) (Subtype.mk (p := fun (x : O) ↦ x ∈ M) x xM) : O) = 0
⊢ c = 0
have hx'₁ : Eq.{u_2 + 1} (α := R) ((ϕ : (a : ↥M) → R) (Subtype.mk (p := fun (x : O) ↦ x ∈ M) x xM) : R) (0 : R)
Tactic: rw [LinearMap.mem_ker] at hx'
Cleared hypotheses: hx', xM', hc
-- Lean 4 proof step from Mathlib.LinearAlgebra.FreeModule.PID (hypothesis)
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_1 : (i : ι) → R
hc_1 : ∀ (i : ι), (b'M.coord i : (a : ↥M) → R) (Subtype.mk (p := fun (x : O) ↦ x ∈ M) y ⋯) = a * c_1 i
val : Fintype ι
y' : O := ∑ i : ι, HSMul.hSMul (β := O) (c_1 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_1 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
c : R
x : O
xM : x ∈ M
hx' : Eq.{u_2 + 1} (α := R) ((ϕ : (a : ↥M) → R) (Subtype.mk (p := fun (x : O) ↦ x ∈ M) x xM) : R) (0 : R)
xM' : Membership.mem (α := O) M' ((M.subtype : (a : ↥M) → O) (Subtype.mk (p := fun (x : O) ↦ x ∈ M) x xM) : O)
hc : HAdd.hAdd (β := O) (c • y') ((M.subtype : (a : ↥M) → O) (Subtype.mk (p := fun (x : O) ↦ x ∈ M) x xM) : O) = 0
⊢ c = 0
have hc' : c • Subtype.mk (p := fun (x : O) ↦ x ∈ M) y' y'M + Subtype.mk (p := fun (x : O) ↦ x ∈ M) x xM = 0
Tactic: have hc' : (c • ⟨y', y'M⟩ + ⟨x, xM⟩ : M) = 0 := by exact @Subtype.coe_injective O (· ∈ M) _ _ hc
-- Lean 4 proof step from Mathlib.LinearAlgebra.FreeModule.PID (goal)
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_1 : (i : ι) → R
hc_1 : ∀ (i : ι), (b'M.coord i : (a : ↥M) → R) (Subtype.mk (p := fun (x : O) ↦ x ∈ M) y ⋯) = a * c_1 i
val : Fintype ι
y' : O := ∑ i : ι, HSMul.hSMul (β := O) (c_1 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_1 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
c : R
z : O
zN' : z ∈ N'
hc : c • a • y' + z = 0
⊢ c = 0
have refine : (a * c) • y' + z = 0
Tactic: refine (mul_eq_zero.mp (y'_ortho_M' (a * c) z (N'_le_M' zN') ?_)).resolve_left a_zero
-- Lean 4 proof step from Mathlib.LinearAlgebra.FreeModule.PID (goal)
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_1 : (i : ι) → R
hc_1 : ∀ (i : ι), (b'M.coord i : (a : ↥M) → R) (Subtype.mk (p := fun (x : O) ↦ x ∈ M) y ⋯) = a * c_1 i
val : Fintype ι
y' : O := ∑ i : ι, HSMul.hSMul (β := O) (c_1 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_1 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
c : R
z : O
zN' : z ∈ N'
hc : c • a • y' + z = 0
⊢ (a * c) • y' + z = 0
have rw : (c * a) • y' + z = 0
Tactic: rw [mul_comm, mul_smul, hc]
-- Lean 4 proof step from Mathlib.LinearAlgebra.FreeModule.PID (goal)
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_1 : (i : ι) → R
hc_1 : ∀ (i : ι), (b'M.coord i : (a : ↥M) → R) (Subtype.mk (p := fun (x : O) ↦ x ∈ M) y ⋯) = a * c_1 i
val : Fintype ι
y' : O := ∑ i : ι, HSMul.hSMul (β := O) (c_1 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_1 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
c : R
z : O
zN' : z ∈ N'
hc : c • a • y' + z = 0
rw : (c * a) • y' + z = 0
rw₁ : c • a • y' + z = 0
⊢ (a * c) • y' + z = 0
have rw₂ : Eq.{u_4 + 1} (α := O) 0 0
Tactic: rw [mul_comm, mul_smul, hc]