awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.FreeModule.Int (goal)
Goal:
ι : Type u_1
M : Type u_3
n : ℕ
inst : AddCommGroup M
inst_1 : Fintype ι
N : Submodule ℤ M
bM : Basis ι ℤ M
bN : Basis (Fin n) ℤ ↥N
f : Fin n ↪ ι
a : Fin n → ℤ
snf :
  ∀ (i : Fin n),
    (↑((bN : (a : Fin n) → ↥N) i) : M) =
      HSMul.hSMul (β := M) (a i) ((bM : (a : ι) → M) ((f : (a : Fin n) → ι) i : ι) : M)
i : Fin n
hi : a i = 0
⊢ False
have apply : Eq (α := ↥N) ((bN : (a : Fin n) → ↥N) i : ↥N) (0 : ↥N)
Tactic: apply Basis.ne_zero bN i
-- Lean 4 proof step from Mathlib.LinearAlgebra.FreeModule.Int (hypothesis)
Goal:
ι : Type u_1
M : Type u_3
n : ℕ
inst : AddCommGroup M
inst_1 : Fintype ι
N : Submodule ℤ M
bM : Basis ι ℤ M
bN : Basis (Fin n) ℤ ↥N
f : Fin n ↪ ι
a : Fin n → ℤ
snf :
  ∀ (i : Fin n),
    (↑((bN : (a : Fin n) → ↥N) i) : M) =
      HSMul.hSMul (β := M) (a i) ((bM : (a : ι) → M) ((f : (a : Fin n) → ι) i : ι) : M)
i : Fin n
hi : a i = 0
⊢ Eq (α := ↥N) ((bN : (a : Fin n) → ↥N) i : ↥N) (0 : ↥N)
have snf₁ : (↑((bN : (a : Fin n) → ↥N) i) : M) = HSMul.hSMul (β := M) (a i) ((bM : (a : ι) → M) ((f : (a : Fin n) → ι) i : ι) : M)
Tactic: specialize snf i
Cleared hypotheses: snf
-- Lean 4 proof step from Mathlib.LinearAlgebra.FreeModule.Int (hypothesis)
Goal:
ι : Type u_1
M : Type u_3
n : ℕ
inst : AddCommGroup M
inst_1 : Fintype ι
N : Submodule ℤ M
bM : Basis ι ℤ M
bN : Basis (Fin n) ℤ ↥N
f : Fin n ↪ ι
a : Fin n → ℤ
snf :
  ∀ (i : Fin n),
    (↑((bN : (a : Fin n) → ↥N) i) : M) =
      HSMul.hSMul (β := M) (a i) ((bM : (a : ι) → M) ((f : (a : Fin n) → ι) i : ι) : M)
⊢ n = Fintype.card ι →
    ¬Eq (α := ℕ) (∏ x : Fin n, AddSubgroup.index (G := ℤ) (Submodule.toAddSubgroup (Ideal.span {a x}))) 0
have ha : ∀ (i : Fin n), a i ≠ 0
Tactic: have ha : ∀ i, a i ≠ 0 := by
    intro i hi
    apply Basis.ne_zero bN i
    specialize snf i
    simpa [hi] using snf
-- Lean 4 proof step from Mathlib.LinearAlgebra.FreeModule.Int (goal)
Goal:
ι : Type u_1
inst : Finite ι
N : Submodule ℤ (ι → ℤ)
⊢ N.toAddSubgroup.index ≠ 0 ↔ Nonempty.{u_1 + 1} (↥N ≃ₗ[ℤ] ι → ℤ)
have obtain : ∀ (n : ℕ) (snf : Module.Basis.SmithNormalForm N ι n), N.toAddSubgroup.index ≠ 0 ↔ Nonempty.{u_1 + 1} (↥N ≃ₗ[ℤ] ι → ℤ)
Tactic: obtain ⟨n, snf⟩ := N.smithNormalForm <| .ofEquivFun <| .refl ..
-- Lean 4 proof step from Mathlib.LinearAlgebra.FreeModule.Int (goal)
Goal:
ι : Type u_1
inst : Finite ι
N : Submodule ℤ (ι → ℤ)
n : ℕ
snf : Module.Basis.SmithNormalForm N ι n
⊢ N.toAddSubgroup.index ≠ 0 ↔ Nonempty.{u_1 + 1} (↥N ≃ₗ[ℤ] ι → ℤ)
have have : ∀ (this : Fintype ι), N.toAddSubgroup.index ≠ 0 ↔ Nonempty.{u_1 + 1} (↥N ≃ₗ[ℤ] ι → ℤ)
Tactic: have := Fintype.ofFinite ι
-- Lean 4 proof step from Mathlib.LinearAlgebra.FreeModule.Int (goal)
Goal:
ι : Type u_1
inst : Finite ι
N : Submodule ℤ (ι → ℤ)
n : ℕ
snf : Module.Basis.SmithNormalForm N ι n
this : Fintype ι
⊢ N.toAddSubgroup.index ≠ 0 ↔ Nonempty.{u_1 + 1} (↥N ≃ₗ[ℤ] ι → ℤ)
have rw : n = Fintype.card ι ↔ Nonempty.{u_1 + 1} (↥N ≃ₗ[ℤ] ι → ℤ)
Tactic: rw [snf.toAddSubgroup_index_ne_zero_iff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.FreeModule.Int (goal)
Goal:
ι : Type u_1
inst : Finite ι
N : Submodule ℤ (ι → ℤ)
n : ℕ
snf : Module.Basis.SmithNormalForm N ι n
this : Fintype ι
⊢ n = Fintype.card ι ↔ Nonempty.{u_1 + 1} (↥N ≃ₗ[ℤ] ι → ℤ)
have rcases : ∀ (bN : Module.Basis (Fin n) ℤ ↥N), n = Fintype.card ι ↔ Nonempty.{u_1 + 1} (↥N ≃ₗ[ℤ] ι → ℤ)
Tactic: rcases snf with ⟨-, bN, -, -, -⟩
Cleared hypotheses: snf
-- Lean 4 proof step from Mathlib.LinearAlgebra.FreeModule.Int (goal)
Goal:
ι : Type u_1
inst : Finite ι
N : Submodule ℤ (ι → ℤ)
n : ℕ
this : Fintype ι
bN : Module.Basis (Fin n) ℤ ↥N
⊢ n = Fintype.card ι ↔ Nonempty.{u_1 + 1} (↥N ≃ₗ[ℤ] ι → ℤ)
have refine_1 : ∀ (h : n = Fintype.card ι), Nonempty.{u_1 + 1} (↥N ≃ₗ[ℤ] ι → ℤ)
Tactic: refine ⟨fun h ↦ ?_, fun ⟨e⟩ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.FreeModule.Int (goal)
Goal:
ι : Type u_1
inst : Finite ι
N : Submodule ℤ (ι → ℤ)
n : ℕ
this : Fintype ι
bN : Module.Basis (Fin n) ℤ ↥N
refine_1 : ∀ (h : n = Fintype.card ι), Nonempty.{u_1 + 1} (↥N ≃ₗ[ℤ] ι → ℤ)
⊢ n = Fintype.card ι ↔ Nonempty.{u_1 + 1} (↥N ≃ₗ[ℤ] ι → ℤ)
have refine_2 : Nonempty.{u_1 + 1} (↥N ≃ₗ[ℤ] ι → ℤ) → ∀ (e : ↥N ≃ₗ[ℤ] ι → ℤ), n = Fintype.card ι
Tactic: refine ⟨fun h ↦ ?_, fun ⟨e⟩ ↦ ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.FreeModule.Int (goal)
Goal:
ι : Type u_1
inst : Finite ι
N : Submodule ℤ (ι → ℤ)
n : ℕ
this : Fintype ι
bN : Module.Basis (Fin n) ℤ ↥N
h : n = Fintype.card ι
⊢ Nonempty.{u_1 + 1} (↥N ≃ₗ[ℤ] ι → ℤ)
have refine_1 : ∀ (bN : Module.Basis (Fin (Fintype.card ι)) ℤ ↥N), Nonempty.{u_1 + 1} (↥N ≃ₗ[ℤ] ι → ℤ)
Tactic: subst h
Cleared hypotheses: n, bN, h
-- Lean 4 proof step from Mathlib.LinearAlgebra.FreeModule.Int (hypothesis)
Goal:
ι : Type u_1
inst : Finite ι
N : Submodule ℤ (ι → ℤ)
n : ℕ
this : Fintype ι
bN : Module.Basis (Fin n) ℤ ↥N
h : Nonempty.{u_1 + 1} (↥N ≃ₗ[ℤ] ι → ℤ)
e : ↥N ≃ₗ[ℤ] ι → ℤ
⊢ n = Fintype.card ι
have hc : Fintype.card (Fin n) = Fintype.card ι
Tactic: have hc := card_eq_of_linearEquiv ℤ <| bN.equivFun.symm.trans e
-- Lean 4 proof step from Mathlib.LinearAlgebra.FreeModule.Int (goal)
Goal:
ι : Type u_1
inst : Finite ι
H : AddSubgroup (ι → ℤ)
⊢ H.index ≠ 0 ↔ Nonempty.{u_1 + 1} (↥H ≃+ (ι → ℤ))
have h : Nonempty.{u_1 + 1} (↥H ≃+ (ι → ℤ)) ↔
  Nonempty.{u_1 + 1}
    (↥((AddSubgroup.toIntSubmodule : (a : AddSubgroup (ι → ℤ)) → Submodule ℤ (ι → ℤ)) H : Submodule ℤ (ι → ℤ)) ≃ₗ[ℤ]
      ι → ℤ)
Tactic: convert! submodule_toAddSubgroup_index_ne_zero_iff (N := AddSubgroup.toIntSubmodule H) using 1
-- Lean 4 proof step from Mathlib.LinearAlgebra.FreeModule.Int (hypothesis)
Goal:
ι : Type u_1
inst : Finite ι
H : Subgroup (ι → Multiplicative ℤ)
em : Multiplicative (ι → ℤ) ≃* (ι → Multiplicative ℤ) := MulEquiv.funMultiplicative ι ℤ
H' : Subgroup (Multiplicative (ι → ℤ)) := Subgroup.comap (↑em : Multiplicative (ι → ℤ) →* ι → Multiplicative ℤ) H
eH' : ↥H' ≃* ↥H := (MulEquiv.subgroupCongr ⋯).trans (em.symm.subgroupMap H).symm
⊢ H.index ≠ 0 ↔ Nonempty.{u_1 + 1} (↥H ≃* (ι → Multiplicative ℤ))
have h : H'.index = H.index
Tactic: have h : H'.index = H.index := Subgroup.index_comap_of_surjective _ em.surjective
-- Lean 4 proof step from Mathlib.LinearAlgebra.FreeModule.Int (goal)
Goal:
ι : Type u_1
inst : Finite ι
H : Subgroup (ι → Multiplicative ℤ)
em : Multiplicative (ι → ℤ) ≃* (ι → Multiplicative ℤ) := MulEquiv.funMultiplicative ι ℤ
H' : Subgroup (Multiplicative (ι → ℤ)) := Subgroup.comap (↑em : Multiplicative (ι → ℤ) →* ι → Multiplicative ℤ) H
eH' : ↥H' ≃* ↥H := (MulEquiv.subgroupCongr ⋯).trans (em.symm.subgroupMap H).symm
h : H'.index = H.index
⊢ H.index ≠ 0 ↔ Nonempty.{u_1 + 1} (↥H ≃* (ι → Multiplicative ℤ))
have rw : Nonempty.{u_1 + 1}
    (↥((Subgroup.toAddSubgroup :
              (a : Subgroup (Multiplicative (ι → ℤ))) → AddSubgroup (Additive (Multiplicative (ι → ℤ))))
            H' :
          AddSubgroup (Additive (Multiplicative (ι → ℤ)))) ≃+
      (ι → ℤ)) ↔
  Nonempty.{u_1 + 1} (↥H ≃* (ι → Multiplicative ℤ))
Tactic: rw [← h, ← Subgroup.index_toAddSubgroup, addSubgroup_index_ne_zero_iff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.FreeModule.ModN (goal)
Goal:
G : Type u_1
H : Type u_2
M : Type u_3
inst : AddCommGroup G
n : ℕ
inst_1 : AddMonoid M
f : AddMonoidHom.{u_1, u_3} (ModN G n) M
g : G
Gn : AddSubgroup G :=
  Submodule.toAddSubgroup (R := ℤ) (module_M := AddCommGroup.toIntModule G)
    (LinearMap.range (R := ℤ) (M := G) (τ₁₂ := RingHom.id ℤ) ((LinearMap.lsmul ℤ G : (a : ℤ) → G →ₗ[ℤ] G) (↑n : ℤ)))
this : n • g ∈ AddMonoidHom.ker (QuotientAddGroup.mk' Gn)
⊢ HSMul.hSMul (β := M) n
      ((f.comp
              (QuotientAddGroup.mk'
                (Submodule.toAddSubgroup (R := ℤ) (module_M := AddCommGroup.toIntModule G)
                  (LinearMap.range (R := ℤ) (M := G) (τ₁₂ := RingHom.id ℤ)
                    ((LinearMap.lsmul ℤ G : (a : ℤ) → G →ₗ[ℤ] G) (↑n : ℤ))))) :
            (a : G) → M)
          g :
        M) =
    0
have simp : Eq.{u_3 + 1} (α := M)
  ((f : (a : ModN G n) → M)
      ((QuotientAddGroup.mk'
              (Submodule.toAddSubgroup (R := ℤ) (module_M := AddCommGroup.toIntModule G)
                (LinearMap.range (R := ℤ) (M := G) (τ₁₂ := RingHom.id ℤ)
                  ((LinearMap.lsmul ℤ G : (a : ℤ) → G →ₗ[ℤ] G) (↑n : ℤ)))) :
            (a : G) → ModN G n)
          (n • g) :
        ModN G n) :
    M)
  (0 : M)
Tactic: simp only [AddMonoidHom.coe_comp, comp_apply, ← map_nsmul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.FreeModule.ModN (goal)
Goal:
G : Type u_1
H : Type u_2
M : Type u_3
inst : AddCommGroup G
n : ℕ
inst_1 : AddMonoid M
f : AddMonoidHom.{u_1, u_3} (ModN G n) M
g : G
Gn : AddSubgroup G :=
  Submodule.toAddSubgroup (R := ℤ) (module_M := AddCommGroup.toIntModule G)
    (LinearMap.range (R := ℤ) (M := G) (τ₁₂ := RingHom.id ℤ) ((LinearMap.lsmul ℤ G : (a : ℤ) → G →ₗ[ℤ] G) (↑n : ℤ)))
this : n • g ∈ AddMonoidHom.ker (QuotientAddGroup.mk' Gn)
⊢ Eq.{u_3 + 1} (α := M)
    ((f : (a : ModN G n) → M)
        ((QuotientAddGroup.mk'
                (Submodule.toAddSubgroup (R := ℤ) (module_M := AddCommGroup.toIntModule G)
                  (LinearMap.range (R := ℤ) (M := G) (τ₁₂ := RingHom.id ℤ)
                    ((LinearMap.lsmul ℤ G : (a : ℤ) → G →ₗ[ℤ] G) (↑n : ℤ)))) :
              (a : G) → ModN G n)
            (n • g) :
          ModN G n) :
      M)
    (0 : M)
have change : Eq.{u_3 + 1} (α := M) ((f : (a : ModN G n) → M) ((QuotientAddGroup.mk' Gn : (a : G) → G ⧸ Gn) (n • g) : G ⧸ Gn) : M)
  (0 : M)
Tactic: change f (QuotientAddGroup.mk' Gn (n • g)) = 0
-- Lean 4 proof step from Mathlib.LinearAlgebra.FreeModule.ModN (goal)
Goal:
G : Type u_1
H : Type u_2
M : Type u_3
inst : AddCommGroup G
n : ℕ
inst_1 : AddMonoid M
f : AddMonoidHom.{u_1, u_3} (ModN G n) M
g : G
Gn : AddSubgroup G :=
  Submodule.toAddSubgroup (R := ℤ) (module_M := AddCommGroup.toIntModule G)
    (LinearMap.range (R := ℤ) (M := G) (τ₁₂ := RingHom.id ℤ) ((LinearMap.lsmul ℤ G : (a : ℤ) → G →ₗ[ℤ] G) (↑n : ℤ)))
this : n • g ∈ AddMonoidHom.ker (QuotientAddGroup.mk' Gn)
⊢ Eq.{u_3 + 1} (α := M) ((f : (a : ModN G n) → M) ((QuotientAddGroup.mk' Gn : (a : G) → G ⧸ Gn) (n • g) : G ⧸ Gn) : M)
    (0 : M)
have rw : Eq.{u_3 + 1} (α := M) ((f : (a : ModN G n) → M) 0 : M) (0 : M)
Tactic: rw [this, map_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.FreeModule.ModN (goal)
Goal:
G : Type u_1
H : Type u_2
M : Type u_3
inst : AddCommGroup G
n : ℕ
inst_1 : AddMonoid M
f : AddMonoidHom.{u_1, u_3} (ModN G n) M
g : G
Gn : AddSubgroup G :=
  Submodule.toAddSubgroup (R := ℤ) (module_M := AddCommGroup.toIntModule G)
    (LinearMap.range (R := ℤ) (M := G) (τ₁₂ := RingHom.id ℤ) ((LinearMap.lsmul ℤ G : (a : ℤ) → G →ₗ[ℤ] G) (↑n : ℤ)))
this : n • g ∈ AddMonoidHom.ker (QuotientAddGroup.mk' Gn)
rw : Eq.{u_3 + 1} (α := M) ((f : (a : ModN G n) → M) 0 : M) (0 : M)
⊢ Eq.{u_3 + 1} (α := M) ((f : (a : ModN G n) → M) ((QuotientAddGroup.mk' Gn : (a : G) → G ⧸ Gn) (n • g) : G ⧸ Gn) : M)
    (0 : M)
have rw₁ : Eq.{u_3 + 1} (α := M) 0 0
Tactic: rw [this, map_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.FreeModule.ModN (goal)
Goal:
G : Type u_1
H : Type u_2
M : Type u_3
inst : AddCommGroup G
n : ℕ
inst_1 : AddMonoid M
f : AddMonoidHom.{u_1, u_3} (ModN G n) M
g : G
Gn : AddSubgroup G :=
  Submodule.toAddSubgroup (R := ℤ) (module_M := AddCommGroup.toIntModule G)
    (LinearMap.range (R := ℤ) (M := G) (τ₁₂ := RingHom.id ℤ) ((LinearMap.lsmul ℤ G : (a : ℤ) → G →ₗ[ℤ] G) (↑n : ℤ)))
⊢ HSMul.hSMul (β := M) n
      ((f.comp
              (QuotientAddGroup.mk'
                (Submodule.toAddSubgroup (R := ℤ) (module_M := AddCommGroup.toIntModule G)
                  (LinearMap.range (R := ℤ) (M := G) (τ₁₂ := RingHom.id ℤ)
                    ((LinearMap.lsmul ℤ G : (a : ℤ) → G →ₗ[ℤ] G) (↑n : ℤ))))) :
            (a : G) → M)
          g :
        M) =
    0
have suffices : n • g ∈ AddMonoidHom.ker (QuotientAddGroup.mk' Gn)
Tactic: suffices n • g ∈ (QuotientAddGroup.mk' Gn).ker by
      simp only [AddMonoidHom.coe_comp, comp_apply, ← map_nsmul]
      change f (QuotientAddGroup.mk' Gn (n • g)) = 0 -- Can we avoid `change`?
      rw [this, map_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.FreeModule.ModN (hypothesis)
Goal:
G : Type u_1
H_1 : Type u_2
M : Type u_3
inst : AddCommGroup G
n : ℕ
inst_1 : NeZero n
ι : Type u_4
b : Basis ι ℤ G
ψ : G →+ G := zsmulAddGroupHom (↑n : ℤ)
nG : Submodule ℤ G :=
  LinearMap.range (R := ℤ) (M := G) (τ₁₂ := RingHom.id ℤ) ((LinearMap.lsmul ℤ G : (a : ℤ) → G →ₗ[ℤ] G) (↑n : ℤ))
H : Type u_1 := G ⧸ nG
φ : G →ₗ[ℤ] H := nG.mkQ
mod : (ι →₀ ℤ) →ₗ[ℤ] ι →₀ ZMod n := mapRange.linearMap (AddMonoidHom.toIntLinearMap (Int.castAddHom (ZMod n)))
f : LinearMap.{0, 0, u_1, u_4} (RingHom.id ℤ) G (ι →₀ ℤ) := (↑b.repr : G →ₗ[ℤ] ι →₀ ℤ)
⊢ Basis.{u_4, 0, u_1} ι (ZMod n) (ModN G n)
have hker : nG ≤ (mod ∘ₗ f).ker
Tactic: have hker : nG ≤ LinearMap.ker (mod.comp f) := by
    rintro _ ⟨x, rfl⟩
    ext b
    simp [mod, f]
-- Lean 4 proof step from Mathlib.LinearAlgebra.FreeModule.ModN (goal)
Goal:
G : Type u_1
H_1 : Type u_2
M : Type u_3
inst : AddCommGroup G
n : ℕ
inst_1 : NeZero n
ι : Type u_4
b : Basis ι ℤ G
ψ : G →+ G := zsmulAddGroupHom (↑n : ℤ)
nG : Submodule ℤ G :=
  LinearMap.range (R := ℤ) (M := G) (τ₁₂ := RingHom.id ℤ) ((LinearMap.lsmul ℤ G : (a : ℤ) → G →ₗ[ℤ] G) (↑n : ℤ))
H : Type u_1 := G ⧸ nG
φ : G →ₗ[ℤ] H := nG.mkQ
mod : (ι →₀ ℤ) →ₗ[ℤ] ι →₀ ZMod n := mapRange.linearMap (AddMonoidHom.toIntLinearMap (Int.castAddHom (ZMod n)))
f : LinearMap.{0, 0, u_1, u_4} (RingHom.id ℤ) G (ι →₀ ℤ) := (↑b.repr : G →ₗ[ℤ] ι →₀ ℤ)
hker : nG ≤ (mod ∘ₗ f).ker
g : LinearMap.{0, 0, u_1, u_4} (RingHom.id ℤ) H (ι →₀ ZMod n) := nG.liftQ (mod ∘ₗ f) hker
⊢ Basis.{u_4, 0, u_1} ι (ZMod n) (ModN G n)
have refine_1 : Injective.{u_1 + 1, u_4 + 1} (α := H) (β := ι →₀ ZMod n)
  (⇑(AddMonoidHom.toZModLinearMap n g.toAddMonoidHom) : (a : H) → ι →₀ ZMod n)
Tactic: refine ⟨.ofBijective (g.toAddMonoidHom.toZModLinearMap n) ⟨?_, ?_⟩⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.FreeModule.ModN (goal)
Goal:
G : Type u_1
H_1 : Type u_2
M : Type u_3
inst : AddCommGroup G
n : ℕ
inst_1 : NeZero n
ι : Type u_4
b : Basis ι ℤ G
ψ : G →+ G := zsmulAddGroupHom (↑n : ℤ)
nG : Submodule ℤ G :=
  LinearMap.range (R := ℤ) (M := G) (τ₁₂ := RingHom.id ℤ) ((LinearMap.lsmul ℤ G : (a : ℤ) → G →ₗ[ℤ] G) (↑n : ℤ))
H : Type u_1 := G ⧸ nG
φ : G →ₗ[ℤ] H := nG.mkQ
mod : (ι →₀ ℤ) →ₗ[ℤ] ι →₀ ZMod n := mapRange.linearMap (AddMonoidHom.toIntLinearMap (Int.castAddHom (ZMod n)))
f : LinearMap.{0, 0, u_1, u_4} (RingHom.id ℤ) G (ι →₀ ℤ) := (↑b.repr : G →ₗ[ℤ] ι →₀ ℤ)
hker : nG ≤ (mod ∘ₗ f).ker
g : LinearMap.{0, 0, u_1, u_4} (RingHom.id ℤ) H (ι →₀ ZMod n) := nG.liftQ (mod ∘ₗ f) hker
refine_1 :
  Injective.{u_1 + 1, u_4 + 1} (α := H) (β := ι →₀ ZMod n)
    (⇑(AddMonoidHom.toZModLinearMap n g.toAddMonoidHom) : (a : H) → ι →₀ ZMod n)
⊢ Basis.{u_4, 0, u_1} ι (ZMod n) (ModN G n)
have refine_2 : Surjective.{u_1 + 1, u_4 + 1} (α := H) (β := ι →₀ ZMod n)
  (⇑(AddMonoidHom.toZModLinearMap n g.toAddMonoidHom) : (a : H) → ι →₀ ZMod n)
Tactic: refine ⟨.ofBijective (g.toAddMonoidHom.toZModLinearMap n) ⟨?_, ?_⟩⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.FreeModule.ModN (goal)
Goal:
G : Type u_1
H_1 : Type u_2
M : Type u_3
inst : AddCommGroup G
n : ℕ
inst_1 : NeZero n
ι : Type u_4
b : Basis ι ℤ G
ψ : G →+ G := zsmulAddGroupHom (↑n : ℤ)
nG : Submodule ℤ G :=
  LinearMap.range (R := ℤ) (M := G) (τ₁₂ := RingHom.id ℤ) ((LinearMap.lsmul ℤ G : (a : ℤ) → G →ₗ[ℤ] G) (↑n : ℤ))
H : Type u_1 := G ⧸ nG
φ : G →ₗ[ℤ] H := nG.mkQ
mod : (ι →₀ ℤ) →ₗ[ℤ] ι →₀ ZMod n := mapRange.linearMap (AddMonoidHom.toIntLinearMap (Int.castAddHom (ZMod n)))
f : LinearMap.{0, 0, u_1, u_4} (RingHom.id ℤ) G (ι →₀ ℤ) := (↑b.repr : G →ₗ[ℤ] ι →₀ ℤ)
hker : nG ≤ (mod ∘ₗ f).ker
g : LinearMap.{0, 0, u_1, u_4} (RingHom.id ℤ) H (ι →₀ ZMod n) := nG.liftQ (mod ∘ₗ f) hker
⊢ Injective.{u_1 + 1, u_4 + 1} (α := H) (β := ι →₀ ZMod n)
    (⇑(AddMonoidHom.toZModLinearMap n g.toAddMonoidHom) : (a : H) → ι →₀ ZMod n)
have refine_1 : ∀ (x : G),
  Eq.{u_4 + 1} (α := ι →₀ ZMod n) ((g : (a : H) → ι →₀ ZMod n) ((nG.mkQ : (a : G) → G ⧸ nG) x) : ι →₀ ZMod n)
      (0 : ι →₀ ZMod n) →
    Eq (α := H) ((nG.mkQ : (a : G) → G ⧸ nG) x : G ⧸ nG) (0 : H)
Tactic: rw [AddMonoidHom.coe_toZModLinearMap, LinearMap.toAddMonoidHom_coe, injective_iff_map_eq_zero,
      nG.mkQ_surjective.forall]
-- Lean 4 proof step from Mathlib.LinearAlgebra.FreeModule.ModN (hypothesis)
Goal:
G : Type u_1
H_1 : Type u_2
M : Type u_3
inst : AddCommGroup G
n : ℕ
inst_1 : NeZero n
ι : Type u_4
b : Basis ι ℤ G
ψ : G →+ G := zsmulAddGroupHom (↑n : ℤ)
nG : Submodule ℤ G :=
  LinearMap.range (R := ℤ) (M := G) (τ₁₂ := RingHom.id ℤ) ((LinearMap.lsmul ℤ G : (a : ℤ) → G →ₗ[ℤ] G) (↑n : ℤ))
H : Type u_1 := G ⧸ nG
φ : G →ₗ[ℤ] H := nG.mkQ
mod : (ι →₀ ℤ) →ₗ[ℤ] ι →₀ ZMod n := mapRange.linearMap (AddMonoidHom.toIntLinearMap (Int.castAddHom (ZMod n)))
f : LinearMap.{0, 0, u_1, u_4} (RingHom.id ℤ) G (ι →₀ ℤ) := (↑b.repr : G →ₗ[ℤ] ι →₀ ℤ)
hker : nG ≤ (mod ∘ₗ f).ker
g : LinearMap.{0, 0, u_1, u_4} (RingHom.id ℤ) H (ι →₀ ZMod n) := nG.liftQ (mod ∘ₗ f) hker
x : G
hx :
  Eq.{u_4 + 1} (α := ι →₀ ZMod n)
    ((nG.liftQ (mod ∘ₗ f) hker : (a : H) → ι →₀ ZMod n) (Submodule.Quotient.mk x) : ι →₀ ZMod n) (0 : ι →₀ ZMod n)
⊢ Eq (α := H) ((nG.mkQ : (a : G) → G ⧸ nG) x : G ⧸ nG) (0 : H)
have hx₁ : Eq.{u_4 + 1} (α := ι →₀ ZMod n) ((mod ∘ₗ f : (a : G) → ι →₀ ZMod n) x : ι →₀ ZMod n) (0 : ι →₀ ZMod n)
Tactic: rw [Submodule.liftQ_apply] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.LinearAlgebra.FreeModule.ModN (hypothesis)
Goal:
G : Type u_1
H_1 : Type u_2
M : Type u_3
inst : AddCommGroup G
n : ℕ
inst_1 : NeZero n
ι : Type u_4
b : Basis ι ℤ G
ψ : G →+ G := zsmulAddGroupHom (↑n : ℤ)
nG : Submodule ℤ G :=
  LinearMap.range (R := ℤ) (M := G) (τ₁₂ := RingHom.id ℤ) ((LinearMap.lsmul ℤ G : (a : ℤ) → G →ₗ[ℤ] G) (↑n : ℤ))
H : Type u_1 := G ⧸ nG
φ : G →ₗ[ℤ] H := nG.mkQ
mod : (ι →₀ ℤ) →ₗ[ℤ] ι →₀ ZMod n := mapRange.linearMap (AddMonoidHom.toIntLinearMap (Int.castAddHom (ZMod n)))
f : LinearMap.{0, 0, u_1, u_4} (RingHom.id ℤ) G (ι →₀ ℤ) := (↑b.repr : G →ₗ[ℤ] ι →₀ ℤ)
hker : nG ≤ (mod ∘ₗ f).ker
g : LinearMap.{0, 0, u_1, u_4} (RingHom.id ℤ) H (ι →₀ ZMod n) := nG.liftQ (mod ∘ₗ f) hker
x : G
hx : Eq.{u_4 + 1} (α := ι →₀ ZMod n) ((mod ∘ₗ f : (a : G) → ι →₀ ZMod n) x : ι →₀ ZMod n) (0 : ι →₀ ZMod n)
⊢ Eq (α := H) ((nG.mkQ : (a : G) → G ⧸ nG) x : G ⧸ nG) (0 : H)
have hx₁ : ∀ (b : ι), Dvd.dvd (α := ℤ) ((↑n : ℤ) : ℤ) ((((f : (a : G) → ι →₀ ℤ) x : ι →₀ ℤ) : (a : ι) → ℤ) b : ℤ)
Tactic: replace hx : ∀ b, ↑n ∣ f x b := by
      simpa [mod, DFunLike.ext_iff, ZMod.intCast_zmod_eq_zero_iff_dvd] using hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.LinearAlgebra.FreeModule.ModN (goal)
Goal:
G : Type u_1
H_1 : Type u_2
M : Type u_3
inst : AddCommGroup G
n : ℕ
inst_1 : NeZero n
ι : Type u_4
b : Basis ι ℤ G
ψ : G →+ G := zsmulAddGroupHom (↑n : ℤ)
nG : Submodule ℤ G :=
  LinearMap.range (R := ℤ) (M := G) (τ₁₂ := RingHom.id ℤ) ((LinearMap.lsmul ℤ G : (a : ℤ) → G →ₗ[ℤ] G) (↑n : ℤ))
H : Type u_1 := G ⧸ nG
φ : G →ₗ[ℤ] H := nG.mkQ
mod : (ι →₀ ℤ) →ₗ[ℤ] ι →₀ ZMod n := mapRange.linearMap (AddMonoidHom.toIntLinearMap (Int.castAddHom (ZMod n)))
f : LinearMap.{0, 0, u_1, u_4} (RingHom.id ℤ) G (ι →₀ ℤ) := (↑b.repr : G →ₗ[ℤ] ι →₀ ℤ)
hker : nG ≤ (mod ∘ₗ f).ker
g : LinearMap.{0, 0, u_1, u_4} (RingHom.id ℤ) H (ι →₀ ZMod n) := nG.liftQ (mod ∘ₗ f) hker
x : G
hx : ∀ (b : ι), Dvd.dvd (α := ℤ) ((↑n : ℤ) : ℤ) ((((f : (a : G) → ι →₀ ℤ) x : ι →₀ ℤ) : (a : ι) → ℤ) b : ℤ)
⊢ Eq (α := H) (Submodule.Quotient.mk x) 0
have refine_1 : x ∈ nG
Tactic: rw [Submodule.Quotient.mk_eq_zero]
-- Lean 4 proof step from Mathlib.LinearAlgebra.FreeModule.ModN (goal)
Goal:
G : Type u_1
H_1 : Type u_2
M : Type u_3
inst : AddCommGroup G
n : ℕ
inst_1 : NeZero n
ι : Type u_4
b : Basis ι ℤ G
ψ : G →+ G := zsmulAddGroupHom (↑n : ℤ)
nG : Submodule ℤ G :=
  LinearMap.range (R := ℤ) (M := G) (τ₁₂ := RingHom.id ℤ) ((LinearMap.lsmul ℤ G : (a : ℤ) → G →ₗ[ℤ] G) (↑n : ℤ))
H : Type u_1 := G ⧸ nG
φ : G →ₗ[ℤ] H := nG.mkQ
mod : (ι →₀ ℤ) →ₗ[ℤ] ι →₀ ZMod n := mapRange.linearMap (AddMonoidHom.toIntLinearMap (Int.castAddHom (ZMod n)))
f : LinearMap.{0, 0, u_1, u_4} (RingHom.id ℤ) G (ι →₀ ℤ) := (↑b.repr : G →ₗ[ℤ] ι →₀ ℤ)
hker : nG ≤ (mod ∘ₗ f).ker
g : LinearMap.{0, 0, u_1, u_4} (RingHom.id ℤ) H (ι →₀ ZMod n) := nG.liftQ (mod ∘ₗ f) hker
x : G
hx : ∀ (b : ι), Dvd.dvd (α := ℤ) ((↑n : ℤ) : ℤ) ((((f : (a : G) → ι →₀ ℤ) x : ι →₀ ℤ) : (a : ι) → ℤ) b : ℤ)
⊢ x ∈ nG
have refine_1 : ∀ (c : (b : ι) → ℤ) (hc : ∀ (b : ι), (((f : (a : G) → ι →₀ ℤ) x : ι →₀ ℤ) : (a : ι) → ℤ) b = (↑n : ℤ) * c b), x ∈ nG
Tactic: choose c hc using hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.LinearAlgebra.FreeModule.ModN (goal)
Goal:
G : Type u_1
H_1 : Type u_2
M : Type u_3
inst : AddCommGroup G
n : ℕ
inst_1 : NeZero n
ι : Type u_4
b : Basis ι ℤ G
ψ : G →+ G := zsmulAddGroupHom (↑n : ℤ)
nG : Submodule ℤ G :=
  LinearMap.range (R := ℤ) (M := G) (τ₁₂ := RingHom.id ℤ) ((LinearMap.lsmul ℤ G : (a : ℤ) → G →ₗ[ℤ] G) (↑n : ℤ))
H : Type u_1 := G ⧸ nG
φ : G →ₗ[ℤ] H := nG.mkQ
mod : (ι →₀ ℤ) →ₗ[ℤ] ι →₀ ZMod n := mapRange.linearMap (AddMonoidHom.toIntLinearMap (Int.castAddHom (ZMod n)))
f : LinearMap.{0, 0, u_1, u_4} (RingHom.id ℤ) G (ι →₀ ℤ) := (↑b.repr : G →ₗ[ℤ] ι →₀ ℤ)
hker : nG ≤ (mod ∘ₗ f).ker
g : LinearMap.{0, 0, u_1, u_4} (RingHom.id ℤ) H (ι →₀ ZMod n) := nG.liftQ (mod ∘ₗ f) hker
x : G
c : (b : ι) → ℤ
hc : ∀ (b : ι), (((f : (a : G) → ι →₀ ℤ) x : ι →₀ ℤ) : (a : ι) → ℤ) b = (↑n : ℤ) * c b
⊢ x ∈ nG
have refine_1 : Eq.{u_4 + 1} (α := ι →₀ ℤ)
  ((b.repr : (a : G) → ι →₀ ℤ)
      ((((LinearMap.lsmul ℤ G : (a : ℤ) → G →ₗ[ℤ] G) (↑n : ℤ) : G →ₗ[ℤ] G) : (a : G) → G)
        ((b.repr.symm : (a : ι →₀ ℤ) → G)
            { support := Finsupp.support (M := ℤ) ((f : (a : G) → ι →₀ ℤ) x), toFun := c, mem_support_toFun := sorry :
              ι →₀ ℤ } :
          G)) :
    ι →₀ ℤ)
  ((b.repr : (a : G) → ι →₀ ℤ) x : ι →₀ ℤ)
Tactic: refine ⟨b.repr.symm ⟨(f x).support, c, by simp [hc, NeZero.ne]⟩, b.repr.injective ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.FreeModule.ModN (goal)
Goal:
G : Type u_1
H_1 : Type u_2
M : Type u_3
inst : AddCommGroup G
n : ℕ
inst_1 : NeZero n
ι : Type u_4
b : Basis ι ℤ G
ψ : G →+ G := zsmulAddGroupHom (↑n : ℤ)
nG : Submodule ℤ G :=
  LinearMap.range (R := ℤ) (M := G) (τ₁₂ := RingHom.id ℤ) ((LinearMap.lsmul ℤ G : (a : ℤ) → G →ₗ[ℤ] G) (↑n : ℤ))
H : Type u_1 := G ⧸ nG
φ : G →ₗ[ℤ] H := nG.mkQ
mod : (ι →₀ ℤ) →ₗ[ℤ] ι →₀ ZMod n := mapRange.linearMap (AddMonoidHom.toIntLinearMap (Int.castAddHom (ZMod n)))
f : LinearMap.{0, 0, u_1, u_4} (RingHom.id ℤ) G (ι →₀ ℤ) := (↑b.repr : G →ₗ[ℤ] ι →₀ ℤ)
hker : nG ≤ (mod ∘ₗ f).ker
g : LinearMap.{0, 0, u_1, u_4} (RingHom.id ℤ) H (ι →₀ ZMod n) := nG.liftQ (mod ∘ₗ f) hker
⊢ Surjective.{u_1 + 1, u_4 + 1} (α := H) (β := ι →₀ ZMod n)
    (⇑(AddMonoidHom.toZModLinearMap n g.toAddMonoidHom) : (a : H) → ι →₀ ZMod n)
have refine_2 : Eq (α := G → ι →₀ ZMod n) (comp (β := ι →₀ ℤ) (⇑mod : (a : ι →₀ ℤ) → ι →₀ ZMod n) (⇑b.repr : (a : G) → ι →₀ ℤ))
  (comp (β := H) (⇑g : (a : H) → ι →₀ ZMod n) (⇑nG.mkQ : (a : G) → G ⧸ nG))
Tactic: suffices mod ∘ b.repr = g ∘ nG.mkQ by
      exact (this ▸ (mapRange_surjective _ (map_zero _) ZMod.intCast_surjective).comp
        b.repr.surjective).of_comp
-- Lean 4 proof step from Mathlib.LinearAlgebra.FreeModule.ModN (goal)
Goal:
G : Type u_1
H_1 : Type u_2
M : Type u_3
inst : AddCommGroup G
n : ℕ
inst_1 : NeZero n
ι : Type u_4
b : Basis ι ℤ G
ψ : G →+ G := zsmulAddGroupHom (↑n : ℤ)
nG : Submodule ℤ G :=
  LinearMap.range (R := ℤ) (M := G) (τ₁₂ := RingHom.id ℤ) ((LinearMap.lsmul ℤ G : (a : ℤ) → G →ₗ[ℤ] G) (↑n : ℤ))
H : Type u_1 := G ⧸ nG
φ : G →ₗ[ℤ] H := nG.mkQ
mod : (ι →₀ ℤ) →ₗ[ℤ] ι →₀ ZMod n := mapRange.linearMap (AddMonoidHom.toIntLinearMap (Int.castAddHom (ZMod n)))
f : LinearMap.{0, 0, u_1, u_4} (RingHom.id ℤ) G (ι →₀ ℤ) := (↑b.repr : G →ₗ[ℤ] ι →₀ ℤ)
hker : nG ≤ (mod ∘ₗ f).ker
g : LinearMap.{0, 0, u_1, u_4} (RingHom.id ℤ) H (ι →₀ ZMod n) := nG.liftQ (mod ∘ₗ f) hker
⊢ Eq (α := G → ι →₀ ZMod n) (comp (β := ι →₀ ℤ) (⇑mod : (a : ι →₀ ℤ) → ι →₀ ZMod n) (⇑b.repr : (a : G) → ι →₀ ℤ))
    (comp (β := H) (⇑g : (a : H) → ι →₀ ZMod n) (⇑nG.mkQ : (a : G) → G ⧸ nG))
have refine_2 : ∀ (x : G) (b_1 : ι),
  Eq (α := ZMod n)
    (((comp (β := ι →₀ ℤ) (⇑mod : (a : ι →₀ ℤ) → ι →₀ ZMod n) (⇑b.repr : (a : G) → ι →₀ ℤ) x : ι →₀ ZMod n) :
          (a : ι) → ZMod n)
        b_1 :
      ZMod n)
    (((comp (β := H) (⇑g : (a : H) → ι →₀ ZMod n) (⇑nG.mkQ : (a : G) → G ⧸ nG) x : ι →₀ ZMod n) : (a : ι) → ZMod n)
        b_1 :
      ZMod n)
Tactic: ext x b