-- Mathlib/Topology/Algebra/InfiniteSum/NatInt.lean
@[to_additive HasSum.of_nat_of_neg_add_one]
lemma HasProd.of_nat_of_neg_add_one {f : ℤ → M}
    (hf₁ : HasProd (fun n : ℕ ↦ f n) m) (hf₂ : HasProd (fun n : ℕ ↦ f (-(n + 1))) m') :
    HasProd f (m * m')

Proof state:
case disjoint
M : Type u_1
inst✝² : CommMonoid M
inst✝¹ : TopologicalSpace M
m m' : M
inst✝ : ContinuousMul M
f : ℤ → M
hf₁ : HasProd (fun n => f ↑n) m
hf₂ : HasProd (fun n => f (-(↑n + 1))) m'
hi₂ : Injective Int.negSucc
⊢ Disjoint (Set.range Nat.cast) (Set.range Int.negSucc)

Tactic:
rw [disjoint_iff_inf_le]

Result:
case disjoint
M : Type u_1
inst✝² : CommMonoid M
inst✝¹ : TopologicalSpace M
m m' : M
inst✝ : ContinuousMul M
f : ℤ → M
hf₁ : HasProd (fun n => f ↑n) m
hf₂ : HasProd (fun n => f (-(↑n + 1))) m'
hi₂ : Injective Int.negSucc
⊢ Set.range Nat.cast ⊓ Set.range Int.negSucc ≤ ⊥

Proof state:
case codisjoint
M : Type u_1
inst✝² : CommMonoid M
inst✝¹ : TopologicalSpace M
m m' : M
inst✝ : ContinuousMul M
f : ℤ → M
hf₁ : HasProd (fun n => f ↑n) m
hf₂ : HasProd (fun n => f (-(↑n + 1))) m'
hi₂ : Injective Int.negSucc
⊢ Codisjoint (Set.range Nat.cast) (Set.range Int.negSucc)

Tactic:
rw [codisjoint_iff_le_sup]

Result:
case codisjoint
M : Type u_1
inst✝² : CommMonoid M
inst✝¹ : TopologicalSpace M
m m' : M
inst✝ : ContinuousMul M
f : ℤ → M
hf₁ : HasProd (fun n => f ↑n) m
hf₂ : HasProd (fun n => f (-(↑n + 1))) m'
hi₂ : Injective Int.negSucc
⊢ ⊤ ≤ Set.range Nat.cast ⊔ Set.range Int.negSucc

Proof state:
case codisjoint
M : Type u_1
inst✝² : CommMonoid M
inst✝¹ : TopologicalSpace M
m m' : M
inst✝ : ContinuousMul M
f : ℤ → M
hf₁ : HasProd (fun n => f ↑n) m
hf₂ : HasProd (fun n => f (-(↑n + 1))) m'
hi₂ : Injective Int.negSucc
⊢ ⊤ ≤ Set.range Nat.cast ⊔ Set.range Int.negSucc

Tactic:
rintro (i | j) <;> simp

Result:
no goals

Proof state:
case disjoint
M : Type u_1
inst✝² : CommMonoid M
inst✝¹ : TopologicalSpace M
m m' : M
inst✝ : ContinuousMul M
f : ℤ → M
hf₁ : HasProd (fun n => f ↑n) m
hf₂ : HasProd (fun n => f (-(↑n + 1))) m'
hi₂ : Injective Int.negSucc
⊢ Set.range Nat.cast ⊓ Set.range Int.negSucc ≤ ⊥

Tactic:
rintro _ ⟨⟨i, rfl⟩, ⟨j, ⟨⟩⟩⟩

Result:
no goals

Proof state:
M : Type u_1
inst✝² : CommMonoid M
inst✝¹ : TopologicalSpace M
m m' : M
inst✝ : ContinuousMul M
f : ℤ → M
hf₁ : HasProd (fun n => f ↑n) m
hf₂ : HasProd (fun n => f (-(↑n + 1))) m'
hi₂ : Injective Int.negSucc
this : IsCompl (Set.range Nat.cast) (Set.range Int.negSucc)
⊢ HasProd f (m * m')

Tactic:
exact (Nat.cast_injective.hasProd_range_iff.mpr hf₁).mul_isCompl
  this (hi₂.hasProd_range_iff.mpr hf₂)

Result:
no goals

Proof state:
M : Type u_1
inst✝² : CommMonoid M
inst✝¹ : TopologicalSpace M
m m' : M
inst✝ : ContinuousMul M
f : ℤ → M
hf₁ : HasProd (fun n => f ↑n) m
hf₂ : HasProd (fun n => f (-(↑n + 1))) m'
⊢ HasProd f (m * m')

Tactic:
have hi₂ : Injective Int.negSucc := @Int.negSucc.inj

Result:
M : Type u_1
inst✝² : CommMonoid M
inst✝¹ : TopologicalSpace M
m m' : M
inst✝ : ContinuousMul M
f : ℤ → M
hf₁ : HasProd (fun n => f ↑n) m
hf₂ : HasProd (fun n => f (-(↑n + 1))) m'
hi₂ : Injective Int.negSucc
⊢ HasProd f (m * m')

Proof state:
M : Type u_1
inst✝² : CommMonoid M
inst✝¹ : TopologicalSpace M
m m' : M
inst✝ : ContinuousMul M
f : ℤ → M
hf₁ : HasProd (fun n => f ↑n) m
hf₂ : HasProd (fun n => f (-(↑n + 1))) m'
hi₂ : Injective Int.negSucc
⊢ IsCompl (Set.range Nat.cast) (Set.range Int.negSucc)

Tactic:
constructor

Result:
case disjoint
M : Type u_1
inst✝² : CommMonoid M
inst✝¹ : TopologicalSpace M
m m' : M
inst✝ : ContinuousMul M
f : ℤ → M
hf₁ : HasProd (fun n => f ↑n) m
hf₂ : HasProd (fun n => f (-(↑n + 1))) m'
hi₂ : Injective Int.negSucc
⊢ Disjoint (Set.range Nat.cast) (Set.range Int.negSucc)

case codisjoint
M : Type u_1
inst✝² : CommMonoid M
inst✝¹ : TopologicalSpace M
m m' : M
inst✝ : ContinuousMul M
f : ℤ → M
hf₁ : HasProd (fun n => f ↑n) m
hf₂ : HasProd (fun n => f (-(↑n + 1))) m'
hi₂ : Injective Int.negSucc
⊢ Codisjoint (Set.range Nat.cast) (Set.range Int.negSucc)