-- Mathlib/LinearAlgebra/FreeModule/Int.lean
lemma subgroup_index_ne_zero_iff {H : Subgroup (ι → Multiplicative ℤ)} :
    H.index ≠ 0 ↔ Nonempty (H ≃* (ι → Multiplicative ℤ))

Proof state:
ι : Type u_1
inst✝ : Finite ι
H : Subgroup (ι → Multiplicative ℤ)
em : Multiplicative (ι → ℤ) ≃* (ι → Multiplicative ℤ) := MulEquiv.funMultiplicative ι ℤ
H' : Subgroup (Multiplicative (ι → ℤ)) := Subgroup.comap (↑em) H
eH' : ↥H' ≃* ↥H := (MulEquiv.subgroupCongr ⋯).trans (em.symm.subgroupMap H).symm
h : H'.index = H.index
⊢ H.index ≠ 0 ↔ Nonempty (↥H ≃* (ι → Multiplicative ℤ))

Tactic:
rw [← h, ← Subgroup.index_toAddSubgroup, addSubgroup_index_ne_zero_iff]

Result:
ι : Type u_1
inst✝ : Finite ι
H : Subgroup (ι → Multiplicative ℤ)
em : Multiplicative (ι → ℤ) ≃* (ι → Multiplicative ℤ) := MulEquiv.funMultiplicative ι ℤ
H' : Subgroup (Multiplicative (ι → ℤ)) := Subgroup.comap (↑em) H
eH' : ↥H' ≃* ↥H := (MulEquiv.subgroupCongr ⋯).trans (em.symm.subgroupMap H).symm
h : H'.index = H.index
⊢ Nonempty (↥(Subgroup.toAddSubgroup H') ≃+ (ι → ℤ)) ↔ Nonempty (↥H ≃* (ι → Multiplicative ℤ))

Proof state:
ι : Type u_1
inst✝ : Finite ι
H : Subgroup (ι → Multiplicative ℤ)
em : Multiplicative (ι → ℤ) ≃* (ι → Multiplicative ℤ) := MulEquiv.funMultiplicative ι ℤ
H' : Subgroup (Multiplicative (ι → ℤ)) := Subgroup.comap (↑em) H
⊢ H.index ≠ 0 ↔ Nonempty (↥H ≃* (ι → Multiplicative ℤ))

Tactic:
let eH' : H' ≃* H := (MulEquiv.subgroupCongr <| Subgroup.comap_equiv_eq_map_symm em H).trans
  (MulEquiv.subgroupMap em.symm _).symm

Result:
ι : Type u_1
inst✝ : Finite ι
H : Subgroup (ι → Multiplicative ℤ)
em : Multiplicative (ι → ℤ) ≃* (ι → Multiplicative ℤ) := MulEquiv.funMultiplicative ι ℤ
H' : Subgroup (Multiplicative (ι → ℤ)) := Subgroup.comap (↑em) H
eH' : ↥H' ≃* ↥H := (MulEquiv.subgroupCongr ⋯).trans (em.symm.subgroupMap H).symm
⊢ H.index ≠ 0 ↔ Nonempty (↥H ≃* (ι → Multiplicative ℤ))

Proof state:
ι : Type u_1
inst✝ : Finite ι
H : Subgroup (ι → Multiplicative ℤ)
em : Multiplicative (ι → ℤ) ≃* (ι → Multiplicative ℤ) := MulEquiv.funMultiplicative ι ℤ
H' : Subgroup (Multiplicative (ι → ℤ)) := Subgroup.comap (↑em) H
eH' : ↥H' ≃* ↥H := (MulEquiv.subgroupCongr ⋯).trans (em.symm.subgroupMap H).symm
h : H'.index = H.index
⊢ Nonempty (↥(Subgroup.toAddSubgroup H') ≃+ (ι → ℤ)) ↔ Nonempty (↥H ≃* (ι → Multiplicative ℤ))

Tactic:
exact ⟨fun ⟨e⟩ ↦ ⟨(eH'.symm.trans (AddEquiv.toMultiplicative e)).trans em⟩,
  fun ⟨e⟩ ↦ ⟨(MulEquiv.toAdditive ((eH'.trans e).trans em.symm)).trans
    (AddEquiv.additiveMultiplicative _)⟩⟩

Result:
no goals

Proof state:
ι : Type u_1
inst✝ : Finite ι
H : Subgroup (ι → Multiplicative ℤ)
em : Multiplicative (ι → ℤ) ≃* (ι → Multiplicative ℤ) := MulEquiv.funMultiplicative ι ℤ
H' : Subgroup (Multiplicative (ι → ℤ)) := Subgroup.comap (↑em) H
eH' : ↥H' ≃* ↥H := (MulEquiv.subgroupCongr ⋯).trans (em.symm.subgroupMap H).symm
⊢ H.index ≠ 0 ↔ Nonempty (↥H ≃* (ι → Multiplicative ℤ))

Tactic:
have h : H'.index = H.index := Subgroup.index_comap_of_surjective _ em.surjective

Result:
ι : Type u_1
inst✝ : Finite ι
H : Subgroup (ι → Multiplicative ℤ)
em : Multiplicative (ι → ℤ) ≃* (ι → Multiplicative ℤ) := MulEquiv.funMultiplicative ι ℤ
H' : Subgroup (Multiplicative (ι → ℤ)) := Subgroup.comap (↑em) H
eH' : ↥H' ≃* ↥H := (MulEquiv.subgroupCongr ⋯).trans (em.symm.subgroupMap H).symm
h : H'.index = H.index
⊢ H.index ≠ 0 ↔ Nonempty (↥H ≃* (ι → Multiplicative ℤ))

Proof state:
ι : Type u_1
inst✝ : Finite ι
H : Subgroup (ι → Multiplicative ℤ)
⊢ H.index ≠ 0 ↔ Nonempty (↥H ≃* (ι → Multiplicative ℤ))

Tactic:
let em : Multiplicative (ι → ℤ) ≃* (ι → Multiplicative ℤ) :=
  MulEquiv.funMultiplicative _ _

Result:
ι : Type u_1
inst✝ : Finite ι
H : Subgroup (ι → Multiplicative ℤ)
em : Multiplicative (ι → ℤ) ≃* (ι → Multiplicative ℤ) := MulEquiv.funMultiplicative ι ℤ
⊢ H.index ≠ 0 ↔ Nonempty (↥H ≃* (ι → Multiplicative ℤ))

Proof state:
ι : Type u_1
inst✝ : Finite ι
H : Subgroup (ι → Multiplicative ℤ)
em : Multiplicative (ι → ℤ) ≃* (ι → Multiplicative ℤ) := MulEquiv.funMultiplicative ι ℤ
⊢ H.index ≠ 0 ↔ Nonempty (↥H ≃* (ι → Multiplicative ℤ))

Tactic:
let H' : Subgroup (Multiplicative (ι → ℤ)) := H.comap em

Result:
ι : Type u_1
inst✝ : Finite ι
H : Subgroup (ι → Multiplicative ℤ)
em : Multiplicative (ι → ℤ) ≃* (ι → Multiplicative ℤ) := MulEquiv.funMultiplicative ι ℤ
H' : Subgroup (Multiplicative (ι → ℤ)) := Subgroup.comap (↑em) H
⊢ H.index ≠ 0 ↔ Nonempty (↥H ≃* (ι → Multiplicative ℤ))