awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.FreeModule.ModN
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_1 : 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_1.repr : G →ₗ[ℤ] ι →₀ ℤ)
x : G
b : ι
⊢ Eq (α := ZMod n)
    ((((mod ∘ₗ f : (a : G) → ι →₀ ZMod n)
              ((((LinearMap.lsmul ℤ G : (a : ℤ) → G →ₗ[ℤ] G) (↑n : ℤ) : G →ₗ[ℤ] G) : (a : G) → G) x) :
            ι →₀ ZMod n) :
          (a : ι) → ZMod n)
        b :
      ZMod n)
    (((0 : ι →₀ ZMod n) : (a : ι) → ZMod n) b : ZMod n)

Tactic:
simp [mod, f]
-- Module: Mathlib.LinearAlgebra.FreeModule.ModN
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 →ₗ[ℤ] ι →₀ ℤ)
⊢ nG ≤ (mod ∘ₗ f).ker

Tactic:
have hker : nG ≤ LinearMap.ker (mod.comp f) := by
    rintro _ ⟨x, rfl⟩
    ext b
    simp [mod, f]
-- Module: Mathlib.LinearAlgebra.FreeModule.ModN
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)
refine_2 :
  Surjective.{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)

Tactic:
refine ⟨.ofBijective (g.toAddMonoidHom.toZModLinearMap n) ⟨?_, ?_⟩⟩
-- Module: Mathlib.LinearAlgebra.FreeModule.ModN
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 :
  ∀ (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)
⊢ Injective.{u_1 + 1, u_4 + 1} (α := H) (β := ι →₀ ZMod n)
    (⇑(AddMonoidHom.toZModLinearMap n g.toAddMonoidHom) : (a : H) → ι →₀ ZMod n)

Tactic:
rw [AddMonoidHom.coe_toZModLinearMap, LinearMap.toAddMonoidHom_coe, injective_iff_map_eq_zero,
      nG.mkQ_surjective.forall]

Premises used: LinearMap.toAddMonoidHom_coe, Function.Surjective.forall, injective_iff_map_eq_zero, Submodule.mkQ_surjective, AddMonoidHom.coe_toZModLinearMap
-- Module: Mathlib.LinearAlgebra.FreeModule.ModN
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.{u_4 + 1} (α := ι →₀ ZMod n) ((mod ∘ₗ f : (a : G) → ι →₀ ZMod n) x : ι →₀ ZMod n) (0 : ι →₀ ZMod n)

Tactic:
rw [Submodule.liftQ_apply] at hx

Premises used: Submodule.liftQ_apply
-- Module: Mathlib.LinearAlgebra.FreeModule.ModN
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)
⊢ ∀ (b : ι), Dvd.dvd (α := ℤ) ((↑n : ℤ) : ℤ) ((((f : (a : G) → ι →₀ ℤ) x : ι →₀ ℤ) : (a : ι) → ℤ) b : ℤ)

Tactic:
simpa [mod, DFunLike.ext_iff, ZMod.intCast_zmod_eq_zero_iff_dvd] using hx

Premises used: DFunLike.ext_iff, ZMod.intCast_zmod_eq_zero_iff_dvd
-- Module: Mathlib.LinearAlgebra.FreeModule.ModN
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)
⊢ ∀ (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
-- Module: Mathlib.LinearAlgebra.FreeModule.ModN
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 : ℤ)
refine_1 : x ∈ nG
⊢ Eq (α := H) (Submodule.Quotient.mk x) 0

Tactic:
rw [Submodule.Quotient.mk_eq_zero]

Premises used: Submodule.Quotient.mk_eq_zero
-- Module: Mathlib.LinearAlgebra.FreeModule.ModN
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 : ℤ)
refine_1 :
  ∀ (c : (b : ι) → ℤ) (hc : ∀ (b : ι), (((f : (a : G) → ι →₀ ℤ) x : ι →₀ ℤ) : (a : ι) → ℤ) b = (↑n : ℤ) * c b), x ∈ nG
⊢ x ∈ nG

Tactic:
choose c hc using hx
-- Module: Mathlib.LinearAlgebra.FreeModule.ModN
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
⊢ ∀ (a : ι), Membership.mem (γ := Finset ι) (Finsupp.support (M := ℤ) ((f : (a : G) → ι →₀ ℤ) x)) a ↔ c a ≠ 0

Tactic:
simp [hc, NeZero.ne]

Premises used: NeZero.ne
-- Module: Mathlib.LinearAlgebra.FreeModule.ModN
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
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 := ⋯ :
                ι →₀ ℤ } :
            G)) :
      ι →₀ ℤ)
    ((b.repr : (a : G) → ι →₀ ℤ) x : ι →₀ ℤ)
⊢ x ∈ nG

Tactic:
refine ⟨b.repr.symm ⟨(f x).support, c, by simp [hc, NeZero.ne]⟩, b.repr.injective ?_⟩
-- Module: Mathlib.LinearAlgebra.FreeModule.ModN
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
⊢ 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 := ⋯ :
                ι →₀ ℤ } :
            G)) :
      ι →₀ ℤ)
    ((b.repr : (a : G) → ι →₀ ℤ) x : ι →₀ ℤ)

Tactic:
simpa [DFunLike.ext_iff, eq_comm] using hc

Premises used: DFunLike.ext_iff, eq_comm
-- Module: Mathlib.LinearAlgebra.FreeModule.ModN
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
this :
  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))
⊢ Surjective.{u_1 + 1, u_4 + 1} (α := H) (β := ι →₀ ZMod n)
    (⇑(AddMonoidHom.toZModLinearMap n g.toAddMonoidHom) : (a : H) → ι →₀ ZMod n)

Tactic:
exact (this ▸ (mapRange_surjective _ (map_zero _) ZMod.intCast_surjective).comp
        b.repr.surjective).of_comp
-- Module: Mathlib.LinearAlgebra.FreeModule.ModN
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_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))
⊢ Surjective.{u_1 + 1, u_4 + 1} (α := H) (β := ι →₀ ZMod n)
    (⇑(AddMonoidHom.toZModLinearMap n g.toAddMonoidHom) : (a : H) → ι →₀ ZMod n)

Tactic:
suffices mod ∘ b.repr = g ∘ nG.mkQ by
      exact (this ▸ (mapRange_surjective _ (map_zero _) ZMod.intCast_surjective).comp
        b.repr.surjective).of_comp
-- Module: Mathlib.LinearAlgebra.FreeModule.ModN
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_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)
⊢ 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:
ext x b
-- Module: Mathlib.LinearAlgebra.FreeModule.ModN
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_1 : 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_1.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
b : ι
⊢ Eq (α := ZMod n)
    (((comp (β := ι →₀ ℤ) (⇑mod : (a : ι →₀ ℤ) → ι →₀ ZMod n) (⇑b_1.repr : (a : G) → ι →₀ ℤ) x : ι →₀ ZMod n) :
          (a : ι) → ZMod n)
        b :
      ZMod n)
    (((comp (β := H) (⇑g : (a : H) → ι →₀ ZMod n) (⇑nG.mkQ : (a : G) → G ⧸ nG) x : ι →₀ ZMod n) : (a : ι) → ZMod n) b :
      ZMod n)

Tactic:
simp [mod, g, f, H]
-- Module: Mathlib.LinearAlgebra.FreeModule.ModN
Goal:
G : Type u_1
inst : AddCommGroup G
n : ℕ
inst_1 : NeZero n
ι : Type u_4
b : Basis ι ℤ G
i : ι
rw :
  Eq.{max (u_4 + 1) 1} (α := ι →₀ ZMod n)
    (((Basis.repr (basis b) : LinearEquiv.{0, 0, u_1, u_4} (RingHom.id (ZMod n)) (ModN G n) (ι →₀ ZMod n)) :
          (a : ModN G n) → ι →₀ ZMod n)
        ((mkQ n : (a : G) → ModN G n) ((b : (a : ι) → G) i)) :
      ι →₀ ZMod n)
    (single i 1 : ι →₀ ZMod n)
⊢ Eq.{u_1 + 1} (α := ModN G n)
    (((basis b : Basis.{u_4, 0, u_1} ι (ZMod n) (ModN G n)) : (a : ι) → ModN G n) i : ModN G n)
    ((mkQ n : (a : G) → ModN G n) ((b : (a : ι) → G) i) : ModN G n)

Tactic:
rw [Basis.apply_eq_iff]

Premises used: Module.Basis.apply_eq_iff
-- Module: Mathlib.LinearAlgebra.FreeModule.ModN
Goal:
G : Type u_1
inst : AddCommGroup G
n : ℕ
inst_1 : NeZero n
ι : Type u_4
b : Basis ι ℤ G
i : ι
⊢ Eq.{max (u_4 + 1) 1} (α := ι →₀ ZMod n)
    (((Basis.repr (basis b) : LinearEquiv.{0, 0, u_1, u_4} (RingHom.id (ZMod n)) (ModN G n) (ι →₀ ZMod n)) :
          (a : ModN G n) → ι →₀ ZMod n)
        ((mkQ n : (a : G) → ModN G n) ((b : (a : ι) → G) i)) :
      ι →₀ ZMod n)
    (single i 1 : ι →₀ ZMod n)

Tactic:
simp [basis, mkQ]

Premises used: ModN.basis, ModN.mkQ
-- Module: Mathlib.LinearAlgebra.FreeModule.ModN
Goal:
G : Type u_1
H : Type u_2
M : Type u_3
inst : AddCommGroup G
n : ℕ
inst_1 : NeZero n
inst_2 : Free ℤ G
inst_3 : Module.Finite ℤ G
⊢ Module.Finite.{0, u_1} (ZMod n) (ModN G n)

Tactic:
.of_basis <| basis <| Module.Free.chooseBasis ℤ G

Premises used: ModN.basis, Int, Module.Finite.of_basis, Module.Free.chooseBasis
-- Module: Mathlib.LinearAlgebra.FreeModule.ModN
Goal:
G : Type u_1
H : Type u_2
M : Type u_3
inst : AddCommGroup G
n : ℕ
inst_1 : NeZero n
inst_2 : Free ℤ G
inst_3 : Module.Finite ℤ G
⊢ Finite.{u_1 + 1} (ModN G n)

Tactic:
Module.finite_of_finite (ZMod n)

Premises used: ZMod, Module.finite_of_finite
-- Module: Mathlib.LinearAlgebra.FreeModule.ModN
Goal:
G : Type u_1
inst : AddCommGroup G
n : ℕ
inst_1 : NeZero n
inst_2 : Free ℤ G
inst_3 : Module.Finite ℤ G
⊢ Nat.card.{u_1} (ModN G n) = n ^ finrank ℤ G

Tactic:
simp [Nat.card_congr (basis <| Module.Free.chooseBasis ℤ G).repr.toEquiv,
    Nat.card_eq_fintype_card, Module.finrank_eq_card_chooseBasisIndex]

Premises used: ModN.basis, Int, Module.Basis.repr, Nat.card_congr, Module.finrank_eq_card_chooseBasisIndex, LinearEquiv.toEquiv, Nat.card_eq_fintype_card, Module.Free.chooseBasis
-- Module: Mathlib.LinearAlgebra.FreeModule.Norm
Goal:
R : Type u_1
S : Type u_2
ι : Type u_3
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsPrincipalIdealRing R
inst_3 : CommRing S
inst_4 : IsDomain S
inst_5 : Algebra R S
inst_6 : Fintype ι
b : Basis ι R S
f : S
hf : f ≠ 0
⊢ ¬Eq (α := Ideal S) (span {f}) ⊥

Tactic:
have hI := span_singleton_eq_bot.not.2 hf
-- Module: Mathlib.LinearAlgebra.FreeModule.Norm
Goal:
R : Type u_1
S : Type u_2
ι : Type u_3
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsPrincipalIdealRing R
inst_3 : CommRing S
inst_4 : IsDomain S
inst_5 : Algebra R S
inst_6 : Fintype ι
b : Basis ι R S
f : S
hf : f ≠ 0
hI : ¬Eq (α := Ideal S) (span {f}) ⊥
b' : Basis ι R S := ringBasis b (span {f}) hI
rw :
  Associated.{u_1} (M := R) ((Algebra.norm R : (a : S) → R) f : R)
    (((LinearMap.det.{u_2, u_1} (M := S) (A := R) : MonoidHom.{u_2, u_1} (S →ₗ[R] S) R) : (a : S →ₗ[R] S) → R)
        ((Matrix.toLin b' b' : (a : Matrix ι ι R) → S →ₗ[R] S) (Matrix.diagonal (smithCoeffs b (span {f}) ⋯)) :
          S →ₗ[R] S) :
      R)
⊢ Associated.{u_1} (M := R) ((Algebra.norm R : (a : S) → R) f : R) (∏ i : ι, smithCoeffs b (span {f}) ⋯ i : R)

Tactic:
rw [← Matrix.det_diagonal, ← LinearMap.det_toLin b']

Premises used: Matrix.det_diagonal, LinearMap.det_toLin
-- Module: Mathlib.LinearAlgebra.FreeModule.Norm
Goal:
R : Type u_1
S : Type u_2
ι : Type u_3
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsPrincipalIdealRing R
inst_3 : CommRing S
inst_4 : IsDomain S
inst_5 : Algebra R S
inst_6 : Fintype ι
b : Basis ι R S
f : S
hf : f ≠ 0
hI : ¬Eq (α := Ideal S) (span {f}) ⊥
b' : Basis ι R S := ringBasis b (span {f}) hI
e : S ≃ₗ[R] S :=
  b'.equiv (selfBasis b (span {f}) hI) (Equiv.refl ι) ≪≫ₗ
    LinearEquiv.restrictScalars R (S := S) (LinearEquiv.coord S S f hf)
⊢ Associated.{u_1} (M := R) ((Algebra.norm R : (a : S) → R) f : R)
    (((LinearMap.det.{u_2, u_1} (M := S) (A := R) : MonoidHom.{u_2, u_1} (S →ₗ[R] S) R) : (a : S →ₗ[R] S) → R)
        ((Matrix.toLin b' b' : (a : Matrix ι ι R) → S →ₗ[R] S) (Matrix.diagonal (smithCoeffs b (span {f}) ⋯)) :
          S →ₗ[R] S) :
      R)

Tactic:
(LinearMap.associated_det_of_eq_comp e _ _ ?_).symm

Premises used: LinearMap.associated_det_of_eq_comp, Associated.symm
-- Module: Mathlib.LinearAlgebra.FreeModule.Norm
Goal:
R : Type u_1
S : Type u_2
ι : Type u_3
inst : CommRing R
inst_1 : IsDomain R
inst_2 : IsPrincipalIdealRing R
inst_3 : CommRing S
inst_4 : IsDomain S
inst_5 : Algebra R S
inst_6 : Fintype ι
b : Basis ι R S
f : S
hf : f ≠ 0
hI : ¬Eq (α := Ideal S) (span {f}) ⊥
b' : Basis ι R S := ringBasis b (span {f}) hI
e : S ≃ₗ[R] S :=
  b'.equiv (selfBasis b (span {f}) hI) (Equiv.refl ι) ≪≫ₗ
    LinearEquiv.restrictScalars R (S := S) (LinearEquiv.coord S S f hf)
refine :
  ∀ (x : S),
    Eq (α := S)
      ((((Matrix.toLin b' b' : (a : Matrix ι ι R) → S →ₗ[R] S) (Matrix.diagonal (smithCoeffs b (span {f}) ⋯)) :
              S →ₗ[R] S) :
            (a : S) → S)
          x :
        S)
      (((((↑(AlgHom.toRingHom (Algebra.lmul R S)) : S →* End R S) : (a : S) → S →ₗ[R] S) f : S →ₗ[R] S) : (a : S) → S)
          ((e : (a : S) → S) x : S) :
        S)
⊢ Associated.{u_1} (M := R) ((Algebra.norm R : (a : S) → R) f : R)
    (((LinearMap.det.{u_2, u_1} (M := S) (A := R) : MonoidHom.{u_2, u_1} (S →ₗ[R] S) R) : (a : S →ₗ[R] S) → R)
        ((Matrix.toLin b' b' : (a : Matrix ι ι R) → S →ₗ[R] S) (Matrix.diagonal (smithCoeffs b (span {f}) ⋯)) :
          S →ₗ[R] S) :
      R)

Tactic:
refine (LinearMap.associated_det_of_eq_comp e _ _ ?_).symm

Premises used: LinearMap.associated_det_of_eq_comp, Associated.symm