awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.NatInt (goal)
Goal:
M : Type u_1
inst : CommMonoid M
inst_1 : TopologicalSpace M
m : M
f : ℤ → M
hf : HasProd f m
this : Injective Int.negSucc
u : Finset ℤ
v' : Finset ℕ
hv' : u.preimage Nat.cast ⋯ ∪ u.preimage Int.negSucc ⋯ ⊆ v'
x : ℤ
hx : x ∈ u
⊢ (∃ a ∈ v', (↑a : ℤ) = x) ∨ ∃ a ∈ v', Int.negSucc a = x
have refine_1 : ∀ (a : ℕ) (hx : Int.ofNat a ∈ u), (∃ a_1 ∈ v', (↑a_1 : ℤ) = Int.ofNat a) ∨ ∃ a_1 ∈ v', Int.negSucc a_1 = Int.ofNat a
Tactic: cases x
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.NatInt (goal)
Goal:
M : Type u_1
inst : CommMonoid M
inst_1 : TopologicalSpace M
m : M
f : ℤ → M
hf : HasProd f m
this : Injective Int.negSucc
u : Finset ℤ
v' : Finset ℕ
hv' : u.preimage Nat.cast ⋯ ∪ u.preimage Int.negSucc ⋯ ⊆ v'
x : ℤ
hx : x ∈ u
refine_1 :
  ∀ (a : ℕ) (hx : Int.ofNat a ∈ u), (∃ a_1 ∈ v', (↑a_1 : ℤ) = Int.ofNat a) ∨ ∃ a_1 ∈ v', Int.negSucc a_1 = Int.ofNat a
⊢ (∃ a ∈ v', (↑a : ℤ) = x) ∨ ∃ a ∈ v', Int.negSucc a = x
have refine_1₁ : ∀ (a : ℕ) (hx : Int.negSucc a ∈ u),
  (∃ a_1 ∈ v', (↑a_1 : ℤ) = Int.negSucc a) ∨ ∃ a_1 ∈ v', Int.negSucc a_1 = Int.negSucc a
Tactic: cases x
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.NatInt (goal)
Goal:
M : Type u_1
inst : CommMonoid M
inst_1 : TopologicalSpace M
m : M
f : ℤ → M
hf : HasProd f m
this : Injective Int.negSucc
u : Finset ℤ
v' : Finset ℕ
hv' : u.preimage Nat.cast ⋯ ∪ u.preimage Int.negSucc ⋯ ⊆ v'
⊢ Eq.{u_1 + 1} (α := M) (∏ x ∈ image Nat.cast v' ∪ image Int.negSucc v', f x) (∏ b ∈ v', f (↑b : ℤ) * f (Int.negSucc b))
have refine_2 : Disjoint (image Nat.cast v') (image Int.negSucc v')
Tactic: rw [prod_union, prod_image Nat.cast_injective.injOn, prod_image this.injOn,
      prod_mul_distrib]
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.NatInt (hypothesis)
Goal:
M : Type u_1
inst : CommMonoid M
inst_1 : TopologicalSpace M
m m' : M
inst_2 : ContinuousMul M
f : ℤ → M
hf₁ : HasProd (fun (n : ℕ) ↦ f (↑n : ℤ)) m
hf₂ : HasProd (fun (n : ℕ) ↦ f (-HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) m'
⊢ HasProd f (m * m')
have hi₂ : Injective Int.negSucc
Tactic: have hi₂ : Injective Int.negSucc := @Int.negSucc.inj
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.NatInt (goal)
Goal:
M : Type u_1
inst : CommMonoid M
inst_1 : TopologicalSpace M
m m' : M
inst_2 : ContinuousMul M
f : ℤ → M
hf₁ : HasProd (fun (n : ℕ) ↦ f (↑n : ℤ)) m
hf₂ : HasProd (fun (n : ℕ) ↦ f (-HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) m'
hi₂ : Injective Int.negSucc
⊢ IsCompl (Set.range Nat.cast) (Set.range Int.negSucc)
have disjoint : Disjoint (Set.range Nat.cast) (Set.range Int.negSucc)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.NatInt (goal)
Goal:
M : Type u_1
inst : CommMonoid M
inst_1 : TopologicalSpace M
m m' : M
inst_2 : ContinuousMul M
f : ℤ → M
hf₁ : HasProd (fun (n : ℕ) ↦ f (↑n : ℤ)) m
hf₂ : HasProd (fun (n : ℕ) ↦ f (-HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) m'
hi₂ : Injective Int.negSucc
disjoint : Disjoint (Set.range Nat.cast) (Set.range Int.negSucc)
⊢ IsCompl (Set.range Nat.cast) (Set.range Int.negSucc)
have codisjoint : Codisjoint (Set.range Nat.cast) (Set.range Int.negSucc)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.NatInt (goal)
Goal:
M : Type u_1
inst : CommMonoid M
inst_1 : TopologicalSpace M
m m' : M
inst_2 : ContinuousMul M
f : ℤ → M
hf₁ : HasProd (fun (n : ℕ) ↦ f (↑n : ℤ)) m
hf₂ : HasProd (fun (n : ℕ) ↦ f (-HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) m'
hi₂ : Injective Int.negSucc
⊢ Disjoint (Set.range Nat.cast) (Set.range Int.negSucc)
have disjoint : Set.range Nat.cast ⊓ Set.range Int.negSucc ≤ ⊥
Tactic: rw [disjoint_iff_inf_le]
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.NatInt (goal)
Goal:
M : Type u_1
inst : CommMonoid M
inst_1 : TopologicalSpace M
m m' : M
inst_2 : ContinuousMul M
f : ℤ → M
hf₁ : HasProd (fun (n : ℕ) ↦ f (↑n : ℤ)) m
hf₂ : HasProd (fun (n : ℕ) ↦ f (-HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) m'
hi₂ : Injective Int.negSucc
⊢ Codisjoint (Set.range Nat.cast) (Set.range Int.negSucc)
have codisjoint : ⊤ ≤ Set.range Nat.cast ⊔ Set.range Int.negSucc
Tactic: rw [codisjoint_iff_le_sup]
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.NatInt (hypothesis)
Goal:
M : Type u_1
inst : CommMonoid M
inst_1 : TopologicalSpace M
m m' : M
inst_2 : ContinuousMul M
f : ℤ → M
hf₁ : HasProd (fun (n : ℕ) ↦ f (↑n : ℤ)) m
hf₂ : HasProd (fun (n : ℕ) ↦ f (-HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) m'
hi₂ : Injective Int.negSucc
⊢ HasProd f (m * m')
have this : IsCompl (Set.range Nat.cast) (Set.range Int.negSucc)
Tactic: have : IsCompl (Set.range ((↑) : ℕ → ℤ)) (Set.range Int.negSucc) := by
    constructor
    · rw [disjoint_iff_inf_le]
      rintro _ ⟨⟨i, rfl⟩, ⟨j, ⟨⟩⟩⟩
    · rw [codisjoint_iff_le_sup]
      rintro (i | j) <;> simp
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.NatInt (goal)
Goal:
M : Type u_1
inst : CommMonoid M
inst_1 : TopologicalSpace M
m : M
inst_2 : ContinuousMul M
f : ℤ → M
hf : HasProd f m
⊢ HasProd (fun (n : ℕ) ↦ f (↑n : ℤ) * f (-(↑n : ℤ))) (m * f 0)
have apply : ∀ (u : Finset ℤ),
  ∃ (v : Finset ℕ),
    ∀ (v' : Finset ℕ),
      v ⊆ v' →
        ∃ (u' : Finset ℤ),
          u ⊆ u' ∧
            Eq.{u_1 + 1} (α := M) (∏ x ∈ u', f x * if x = 0 then f 0 else 1) (∏ b ∈ v', f (↑b : ℤ) * f (-(↑b : ℤ)))
Tactic: apply (hf.mul (hasProd_ite_eq (0 : ℤ) (f 0))).hasProd_of_prod_eq fun u ↦ ?_
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.NatInt (goal)
Goal:
M : Type u_1
inst : CommMonoid M
inst_1 : TopologicalSpace M
m : M
inst_2 : ContinuousMul M
f : ℤ → M
hf : HasProd f m
u : Finset ℤ
⊢ ∃ (v : Finset ℕ),
    ∀ (v' : Finset ℕ),
      v ⊆ v' →
        ∃ (u' : Finset ℤ),
          u ⊆ u' ∧
            Eq.{u_1 + 1} (α := M) (∏ x ∈ u', f x * if x = 0 then f 0 else 1) (∏ b ∈ v', f (↑b : ℤ) * f (-(↑b : ℤ)))
have refine : ∀ (v' : Finset ℕ) (hv' : image Int.natAbs u ⊆ v'),
  ∃ (u' : Finset ℤ),
    u ⊆ u' ∧ Eq.{u_1 + 1} (α := M) (∏ x ∈ u', f x * if x = 0 then f 0 else 1) (∏ b ∈ v', f (↑b : ℤ) * f (-(↑b : ℤ)))
Tactic: refine ⟨u.image Int.natAbs, fun v' hv' ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.NatInt (goal)
Goal:
M : Type u_1
inst : CommMonoid M
inst_1 : TopologicalSpace M
m : M
inst_2 : ContinuousMul M
f : ℤ → M
hf : HasProd f m
u : Finset ℤ
v' : Finset ℕ
hv' : image Int.natAbs u ⊆ v'
u1 : Finset ℤ := image (fun (x : ℕ) ↦ (↑x : ℤ)) v'
u2 : Finset ℤ := image (fun (x : ℕ) ↦ -(↑x : ℤ)) v'
x : ℤ
hx : x ∈ u
⊢ x ∈ u1 ∪ u2
have simp : (∃ a ∈ v', (↑a : ℤ) = x) ∨ ∃ a ∈ v', -(↑a : ℤ) = x
Tactic: simp only [u1, u2, mem_union, mem_image]
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.NatInt (goal)
Goal:
M : Type u_1
inst : CommMonoid M
inst_1 : TopologicalSpace M
m : M
inst_2 : ContinuousMul M
f : ℤ → M
hf : HasProd f m
u : Finset ℤ
v' : Finset ℕ
hv' : image Int.natAbs u ⊆ v'
u1 : Finset ℤ := image (fun (x : ℕ) ↦ (↑x : ℤ)) v'
u2 : Finset ℤ := image (fun (x : ℕ) ↦ -(↑x : ℤ)) v'
x : ℤ
hx : x ∈ u
⊢ (∃ a ∈ v', (↑a : ℤ) = x) ∨ ∃ a ∈ v', -(↑a : ℤ) = x
have inl : ∀ (h'x : 0 ≤ x), (∃ a ∈ v', (↑a : ℤ) = x) ∨ ∃ a ∈ v', -(↑a : ℤ) = x
Tactic: rcases le_total 0 x with (h'x | h'x)
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.NatInt (goal)
Goal:
M : Type u_1
inst : CommMonoid M
inst_1 : TopologicalSpace M
m : M
inst_2 : ContinuousMul M
f : ℤ → M
hf : HasProd f m
u : Finset ℤ
v' : Finset ℕ
hv' : image Int.natAbs u ⊆ v'
u1 : Finset ℤ := image (fun (x : ℕ) ↦ (↑x : ℤ)) v'
u2 : Finset ℤ := image (fun (x : ℕ) ↦ -(↑x : ℤ)) v'
x : ℤ
hx : x ∈ u
inl : ∀ (h'x : 0 ≤ x), (∃ a ∈ v', (↑a : ℤ) = x) ∨ ∃ a ∈ v', -(↑a : ℤ) = x
⊢ (∃ a ∈ v', (↑a : ℤ) = x) ∨ ∃ a ∈ v', -(↑a : ℤ) = x
have inr : ∀ (h'x : x ≤ 0), (∃ a ∈ v', (↑a : ℤ) = x) ∨ ∃ a ∈ v', -(↑a : ℤ) = x
Tactic: rcases le_total 0 x with (h'x | h'x)
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.NatInt (goal)
Goal:
M : Type u_1
inst : CommMonoid M
inst_1 : TopologicalSpace M
m : M
inst_2 : ContinuousMul M
f : ℤ → M
hf : HasProd f m
u : Finset ℤ
v' : Finset ℕ
hv' : image Int.natAbs u ⊆ v'
u1 : Finset ℤ := image (fun (x : ℕ) ↦ (↑x : ℤ)) v'
u2 : Finset ℤ := image (fun (x : ℕ) ↦ -(↑x : ℤ)) v'
x : ℤ
hx : x ∈ u
h'x : 0 ≤ x
⊢ (∃ a ∈ v', (↑a : ℤ) = x) ∨ ∃ a ∈ v', -(↑a : ℤ) = x
have inl : (↑x.natAbs : ℤ) = x
Tactic: refine Or.inl ⟨_, hv' <| mem_image.mpr ⟨x, hx, rfl⟩, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.NatInt (goal)
Goal:
M : Type u_1
inst : CommMonoid M
inst_1 : TopologicalSpace M
m : M
inst_2 : ContinuousMul M
f : ℤ → M
hf : HasProd f m
u : Finset ℤ
v' : Finset ℕ
hv' : image Int.natAbs u ⊆ v'
u1 : Finset ℤ := image (fun (x : ℕ) ↦ (↑x : ℤ)) v'
u2 : Finset ℤ := image (fun (x : ℕ) ↦ -(↑x : ℤ)) v'
x : ℤ
hx : x ∈ u
h'x : x ≤ 0
⊢ (∃ a ∈ v', (↑a : ℤ) = x) ∨ ∃ a ∈ v', -(↑a : ℤ) = x
have inr : -(↑x.natAbs : ℤ) = x
Tactic: refine Or.inr ⟨_, hv' <| mem_image.mpr ⟨x, hx, rfl⟩, ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.NatInt (hypothesis)
Goal:
M : Type u_1
inst : CommMonoid M
inst_1 : TopologicalSpace M
m : M
inst_2 : ContinuousMul M
f : ℤ → M
hf : HasProd f m
u : Finset ℤ
v' : Finset ℕ
hv' : image Int.natAbs u ⊆ v'
u1 : Finset ℤ := image (fun (x : ℕ) ↦ (↑x : ℤ)) v'
u2 : Finset ℤ := image (fun (x : ℕ) ↦ -(↑x : ℤ)) v'
⊢ ∃ (u' : Finset ℤ),
    u ⊆ u' ∧ Eq.{u_1 + 1} (α := M) (∏ x ∈ u', f x * if x = 0 then f 0 else 1) (∏ b ∈ v', f (↑b : ℤ) * f (-(↑b : ℤ)))
have A : u ⊆ u1 ∪ u2
Tactic: have A : u ⊆ u1 ∪ u2 := by
    intro x hx
    simp only [u1, u2, mem_union, mem_image]
    rcases le_total 0 x with (h'x | h'x)
    · refine Or.inl ⟨_, hv' <| mem_image.mpr ⟨x, hx, rfl⟩, ?_⟩
      simp only [Int.natCast_natAbs, abs_eq_self, h'x]
    · refine Or.inr ⟨_, hv' <| mem_image.mpr ⟨x, hx, rfl⟩, ?_⟩
      simp only [abs_of_nonpos h'x, Int.natCast_natAbs, neg_neg]
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.NatInt (goal)
Goal:
M : Type u_1
inst : CommMonoid M
inst_1 : TopologicalSpace M
m : M
inst_2 : ContinuousMul M
f : ℤ → M
hf : HasProd f m
u : Finset ℤ
v' : Finset ℕ
hv' : image Int.natAbs u ⊆ v'
u1 : Finset ℤ := image (fun (x : ℕ) ↦ (↑x : ℤ)) v'
u2 : Finset ℤ := image (fun (x : ℕ) ↦ -(↑x : ℤ)) v'
A : u ⊆ u1 ∪ u2
⊢ (∏ x ∈ u1 ∪ u2, f x * if x = 0 then f 0 else 1) = HMul.hMul (α := M) (∏ x ∈ u1 ∪ u2, f x) (∏ x ∈ u1 ∩ u2, f x)
have rw : HMul.hMul (α := M) (∏ x ∈ u1 ∪ u2, f x) (∏ x ∈ u1 ∪ u2, if x = 0 then f 0 else 1) =
  HMul.hMul (α := M) (∏ x ∈ u1 ∪ u2, f x) (∏ x ∈ u1 ∩ u2, f x)
Tactic: rw [prod_mul_distrib]
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.NatInt (goal)
Goal:
M : Type u_1
inst : CommMonoid M
inst_1 : TopologicalSpace M
m : M
inst_2 : ContinuousMul M
f : ℤ → M
hf : HasProd f m
u : Finset ℤ
v' : Finset ℕ
hv' : image Int.natAbs u ⊆ v'
u1 : Finset ℤ := image (fun (x : ℕ) ↦ (↑x : ℤ)) v'
u2 : Finset ℤ := image (fun (x : ℕ) ↦ -(↑x : ℤ)) v'
A : u ⊆ u1 ∪ u2
⊢ HMul.hMul (α := M) (∏ x ∈ u1 ∪ u2, f x) (∏ x ∈ u1 ∪ u2, if x = 0 then f 0 else 1) =
    HMul.hMul (α := M) (∏ x ∈ u1 ∪ u2, f x) (∏ x ∈ u1 ∩ u2, f x)
have e_a : Eq.{u_1 + 1} (α := M) (∏ x ∈ u1 ∪ u2, if x = 0 then f 0 else 1) (∏ x ∈ u1 ∩ u2, f x)
Tactic: congr 1
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.NatInt (goal)
Goal:
M : Type u_1
inst : CommMonoid M
inst_1 : TopologicalSpace M
m : M
inst_2 : ContinuousMul M
f : ℤ → M
hf : HasProd f m
u : Finset ℤ
v' : Finset ℕ
hv' : image Int.natAbs u ⊆ v'
u1 : Finset ℤ := image (fun (x : ℕ) ↦ (↑x : ℤ)) v'
u2 : Finset ℤ := image (fun (x : ℕ) ↦ -(↑x : ℤ)) v'
A : u ⊆ u1 ∪ u2
⊢ Eq.{u_1 + 1} (α := M) (∏ x ∈ u1 ∪ u2, if x = 0 then f 0 else 1) (∏ x ∈ u1 ∩ u2, f x)
have e_a : ∀ x ∈ (u1 ∪ u2) \ (u1 ∩ u2), (if x = 0 then f 0 else 1) = 1
Tactic: refine (prod_subset_one_on_sdiff inter_subset_union ?_ ?_).symm
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.NatInt (goal)
Goal:
M : Type u_1
inst : CommMonoid M
inst_1 : TopologicalSpace M
m : M
inst_2 : ContinuousMul M
f : ℤ → M
hf : HasProd f m
u : Finset ℤ
v' : Finset ℕ
hv' : image Int.natAbs u ⊆ v'
u1 : Finset ℤ := image (fun (x : ℕ) ↦ (↑x : ℤ)) v'
u2 : Finset ℤ := image (fun (x : ℕ) ↦ -(↑x : ℤ)) v'
A : u ⊆ u1 ∪ u2
e_a : ∀ x ∈ (u1 ∪ u2) \ (u1 ∩ u2), (if x = 0 then f 0 else 1) = 1
⊢ Eq.{u_1 + 1} (α := M) (∏ x ∈ u1 ∪ u2, if x = 0 then f 0 else 1) (∏ x ∈ u1 ∩ u2, f x)
have e_a₁ : ∀ x ∈ u1 ∩ u2, f x = if x = 0 then f 0 else 1
Tactic: refine (prod_subset_one_on_sdiff inter_subset_union ?_ ?_).symm
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.NatInt (goal)
Goal:
M : Type u_1
inst : CommMonoid M
inst_1 : TopologicalSpace M
m : M
inst_2 : ContinuousMul M
f : ℤ → M
hf : HasProd f m
u : Finset ℤ
v' : Finset ℕ
hv' : image Int.natAbs u ⊆ v'
u1 : Finset ℤ := image (fun (x : ℕ) ↦ (↑x : ℤ)) v'
u2 : Finset ℤ := image (fun (x : ℕ) ↦ -(↑x : ℤ)) v'
A : u ⊆ u1 ∪ u2
x : ℤ
hx : x ∈ (u1 ∪ u2) \ (u1 ∩ u2)
⊢ (if x = 0 then f 0 else 1) = 1
have e_a : x ≠ 0
Tactic: suffices x ≠ 0 by simp only [this, if_false]
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.NatInt (hypothesis)
Goal:
M : Type u_1
inst : CommMonoid M
inst_1 : TopologicalSpace M
m : M
inst_2 : ContinuousMul M
f : ℤ → M
hf : HasProd f m
u : Finset ℤ
v' : Finset ℕ
hv' : image Int.natAbs u ⊆ v'
u1 : Finset ℤ := image (fun (x : ℕ) ↦ (↑x : ℤ)) v'
u2 : Finset ℤ := image (fun (x : ℕ) ↦ -(↑x : ℤ)) v'
A : u ⊆ u1 ∪ u2
x : ℤ
hx : x ∈ u1 ∩ u2
⊢ f x = if x = 0 then f 0 else 1
have hx₁ : (∃ a ∈ v', (↑a : ℤ) = x) ∧ ∃ a ∈ v', -(↑a : ℤ) = x
Tactic: simp only [u1, u2, mem_inter, mem_image] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.NatInt (goal)
Goal:
M : Type u_1
inst : CommMonoid M
inst_1 : TopologicalSpace M
m : M
inst_2 : ContinuousMul M
f : ℤ → M
hf : HasProd f m
u : Finset ℤ
v' : Finset ℕ
hv' : image Int.natAbs u ⊆ v'
u1 : Finset ℤ := image (fun (x : ℕ) ↦ (↑x : ℤ)) v'
u2 : Finset ℤ := image (fun (x : ℕ) ↦ -(↑x : ℤ)) v'
A : u ⊆ u1 ∪ u2
x : ℤ
hx : (∃ a ∈ v', (↑a : ℤ) = x) ∧ ∃ a ∈ v', -(↑a : ℤ) = x
⊢ f x = if x = 0 then f 0 else 1
have e_a : x = 0
Tactic: suffices x = 0 by simp only [this, if_true]
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.NatInt (goal)
Goal:
G : Type u_2
inst : CommGroup G
g g' : G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
f : ℤ → G
hf₁ : HasProd (fun (n : ℕ) ↦ f (↑n : ℤ)) g
hf₂ : HasProd (fun (n : ℕ) ↦ f (-(↑n : ℤ))) g'
⊢ HasProd f (g * g' / f 0)
have refine : HasProd (fun (n : ℕ) ↦ f (-HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) (g' / f 0)
Tactic: refine mul_div_assoc' g .. ▸ hf₁.of_nat_of_neg_add_one (m' := g' / f 0) ?_
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.NatInt (goal)
Goal:
G : Type u_2
inst : CommGroup G
g g' : G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
f : ℤ → G
hf₁ : HasProd (fun (n : ℕ) ↦ f (↑n : ℤ)) g
hf₂ : HasProd (fun (n : ℕ) ↦ f (-(↑n : ℤ))) g'
⊢ HasProd (fun (n : ℕ) ↦ f (-HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) (g' / f 0)
have rwa : ∀ (hf₂ : HasProd (fun (n : ℕ) ↦ f (-(↑(n + 1) : ℤ))) (g' / ∏ i ∈ range 1, f (-(↑i : ℤ)))),
  HasProd (fun (n : ℕ) ↦ f (-HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) (g' / f 0)
Tactic: rwa [← hasProd_nat_add_iff' 1, prod_range_one, Nat.cast_zero, neg_zero] at hf₂
Cleared hypotheses: hf₂
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.NatInt (goal)
Goal:
G : Type u_2
inst : CommGroup G
g g' : G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
f : ℤ → G
hf₁ : HasProd (fun (n : ℕ) ↦ f (↑n : ℤ)) g
hf₂ : HasProd (fun (n : ℕ) ↦ f (-(↑n : ℤ))) g'
rwa :
  ∀ (hf₂ : HasProd (fun (n : ℕ) ↦ f (-(↑(n + 1) : ℤ))) (g' / ∏ i ∈ range 1, f (-(↑i : ℤ)))),
    HasProd (fun (n : ℕ) ↦ f (-HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) (g' / f 0)
⊢ HasProd (fun (n : ℕ) ↦ f (-HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) (g' / f 0)
have rwa₁ : ∀ (hf₂ : HasProd (fun (n : ℕ) ↦ f (-(↑(n + 1) : ℤ))) (g' / f (-(↑0 : ℤ)))),
  HasProd (fun (n : ℕ) ↦ f (-HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) (g' / f 0)
Tactic: rwa [← hasProd_nat_add_iff' 1, prod_range_one, Nat.cast_zero, neg_zero] at hf₂
Cleared hypotheses: hf₂
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.NatInt (goal)
Goal:
G : Type u_2
inst : CommGroup G
g g' : G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
f : ℤ → G
hf₁ : HasProd (fun (n : ℕ) ↦ f (↑n : ℤ)) g
hf₂ : HasProd (fun (n : ℕ) ↦ f (-(↑n : ℤ))) g'
rwa :
  ∀ (hf₂ : HasProd (fun (n : ℕ) ↦ f (-(↑(n + 1) : ℤ))) (g' / ∏ i ∈ range 1, f (-(↑i : ℤ)))),
    HasProd (fun (n : ℕ) ↦ f (-HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) (g' / f 0)
rwa₁ :
  ∀ (hf₂ : HasProd (fun (n : ℕ) ↦ f (-(↑(n + 1) : ℤ))) (g' / f (-(↑0 : ℤ)))),
    HasProd (fun (n : ℕ) ↦ f (-HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) (g' / f 0)
⊢ HasProd (fun (n : ℕ) ↦ f (-HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) (g' / f 0)
have rwa₂ : ∀ (hf₂ : HasProd (fun (n : ℕ) ↦ f (-(↑(n + 1) : ℤ))) (g' / f (-0))),
  HasProd (fun (n : ℕ) ↦ f (-HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) (g' / f 0)
Tactic: rwa [← hasProd_nat_add_iff' 1, prod_range_one, Nat.cast_zero, neg_zero] at hf₂
Cleared hypotheses: hf₂
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.NatInt (goal)
Goal:
G : Type u_2
inst : CommGroup G
g g' : G
inst_1 : TopologicalSpace G
inst_2 : IsTopologicalGroup G
f : ℤ → G
hf₁ : HasProd (fun (n : ℕ) ↦ f (↑n : ℤ)) g
hf₂ : HasProd (fun (n : ℕ) ↦ f (-(↑n : ℤ))) g'
rwa :
  ∀ (hf₂ : HasProd (fun (n : ℕ) ↦ f (-(↑(n + 1) : ℤ))) (g' / ∏ i ∈ range 1, f (-(↑i : ℤ)))),
    HasProd (fun (n : ℕ) ↦ f (-HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) (g' / f 0)
rwa₁ :
  ∀ (hf₂ : HasProd (fun (n : ℕ) ↦ f (-(↑(n + 1) : ℤ))) (g' / f (-(↑0 : ℤ)))),
    HasProd (fun (n : ℕ) ↦ f (-HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) (g' / f 0)
rwa₂ :
  ∀ (hf₂ : HasProd (fun (n : ℕ) ↦ f (-(↑(n + 1) : ℤ))) (g' / f (-0))),
    HasProd (fun (n : ℕ) ↦ f (-HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) (g' / f 0)
⊢ HasProd (fun (n : ℕ) ↦ f (-HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) (g' / f 0)
have rwa₃ : ∀ (hf₂ : HasProd (fun (n : ℕ) ↦ f (-(↑(n + 1) : ℤ))) (g' / f 0)),
  HasProd (fun (n : ℕ) ↦ f (-HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)) (g' / f 0)
Tactic: rwa [← hasProd_nat_add_iff' 1, prod_range_one, Nat.cast_zero, neg_zero] at hf₂
Cleared hypotheses: hf₂
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.NatInt (goal)
Goal:
G : Type u_2
inst : CommGroup G
inst_1 : UniformSpace G
inst_2 : IsUniformGroup G
inst_3 : CompleteSpace G
f : ℤ → G
⊢ Multipliable f ↔
    (Multipliable.{u_2, 0} (α := G) fun (n : ℕ) ↦ f (↑n : ℤ)) ∧
      Multipliable.{u_2, 0} (α := G) fun (n : ℕ) ↦ f (-HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)
have refine_1 : ∀ (p : Multipliable f), Multipliable.{u_2, 0} (α := G) fun (n : ℕ) ↦ f (↑n : ℤ)
Tactic: refine ⟨fun p ↦ ⟨?_, ?_⟩, fun ⟨hf₁, hf₂⟩ ↦ Multipliable.of_nat_of_neg_add_one hf₁ hf₂⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.NatInt (goal)
Goal:
G : Type u_2
inst : CommGroup G
inst_1 : UniformSpace G
inst_2 : IsUniformGroup G
inst_3 : CompleteSpace G
f : ℤ → G
refine_1 : ∀ (p : Multipliable f), Multipliable.{u_2, 0} (α := G) fun (n : ℕ) ↦ f (↑n : ℤ)
⊢ Multipliable f ↔
    (Multipliable.{u_2, 0} (α := G) fun (n : ℕ) ↦ f (↑n : ℤ)) ∧
      Multipliable.{u_2, 0} (α := G) fun (n : ℕ) ↦ f (-HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)
have refine_2 : ∀ (p : Multipliable f), Multipliable.{u_2, 0} (α := G) fun (n : ℕ) ↦ f (-HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)
Tactic: refine ⟨fun p ↦ ⟨?_, ?_⟩, fun ⟨hf₁, hf₂⟩ ↦ Multipliable.of_nat_of_neg_add_one hf₁ hf₂⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.NatInt (goal)
Goal:
G : Type u_2
inst : CommGroup G
inst_1 : UniformSpace G
inst_2 : IsUniformGroup G
inst_3 : CompleteSpace G
f : ℤ → G
p : Multipliable f
⊢ Multipliable.{u_2, 0} (α := G) fun (n : ℕ) ↦ f (↑n : ℤ)
have refine_1 : Injective (β := ℤ) Nat.cast
Tactic: apply p.comp_injective
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.NatInt (goal)
Goal:
G : Type u_2
inst : CommGroup G
inst_1 : UniformSpace G
inst_2 : IsUniformGroup G
inst_3 : CompleteSpace G
f : ℤ → G
p : Multipliable f
⊢ Multipliable.{u_2, 0} (α := G) fun (n : ℕ) ↦ f (-HAdd.hAdd (α := ℤ) (↑n : ℤ) 1)
have refine_2 : Injective (β := ℤ) fun (n : ℕ) ↦ -HAdd.hAdd (α := ℤ) (↑n : ℤ) 1
Tactic: apply p.comp_injective
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.NatInt (goal)
Goal:
G : Type u_2
inst : CommGroup G
inst_1 : UniformSpace G
inst_2 : IsUniformGroup G
inst_3 : CompleteSpace G
f : ℤ → G
⊢ Multipliable f ↔
    (Multipliable.{u_2, 0} (α := G) fun (n : ℕ) ↦ f (↑n : ℤ)) ∧
      Multipliable.{u_2, 0} (α := G) fun (n : ℕ) ↦ f (-(↑n : ℤ))
have refine_1 : ∀ (p : Multipliable f), Multipliable.{u_2, 0} (α := G) fun (n : ℕ) ↦ f (↑n : ℤ)
Tactic: refine ⟨fun p ↦ ⟨?_, ?_⟩, fun ⟨hf₁, hf₂⟩ ↦ Multipliable.of_nat_of_neg hf₁ hf₂⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.NatInt (goal)
Goal:
G : Type u_2
inst : CommGroup G
inst_1 : UniformSpace G
inst_2 : IsUniformGroup G
inst_3 : CompleteSpace G
f : ℤ → G
refine_1 : ∀ (p : Multipliable f), Multipliable.{u_2, 0} (α := G) fun (n : ℕ) ↦ f (↑n : ℤ)
⊢ Multipliable f ↔
    (Multipliable.{u_2, 0} (α := G) fun (n : ℕ) ↦ f (↑n : ℤ)) ∧
      Multipliable.{u_2, 0} (α := G) fun (n : ℕ) ↦ f (-(↑n : ℤ))
have refine_2 : ∀ (p : Multipliable f), Multipliable.{u_2, 0} (α := G) fun (n : ℕ) ↦ f (-(↑n : ℤ))
Tactic: refine ⟨fun p ↦ ⟨?_, ?_⟩, fun ⟨hf₁, hf₂⟩ ↦ Multipliable.of_nat_of_neg hf₁ hf₂⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.NatInt (goal)
Goal:
G : Type u_2
inst : CommGroup G
inst_1 : UniformSpace G
inst_2 : IsUniformGroup G
inst_3 : CompleteSpace G
f : ℤ → G
p : Multipliable f
⊢ Multipliable.{u_2, 0} (α := G) fun (n : ℕ) ↦ f (-(↑n : ℤ))
have refine_2 : Injective (β := ℤ) fun (n : ℕ) ↦ -(↑n : ℤ)
Tactic: apply p.comp_injective
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.NatInt (goal)
Goal:
α : Type u_3
inst : Ring α
inst_1 : UniformSpace α
inst_2 : IsUniformAddGroup α
inst_3 : CompleteSpace α
f : ℕ → α
hf : Summable f
⊢ Summable.{u_3, 0} (α := α) fun (n : ℕ) ↦ HPow.hPow (α := α) (-1) n * f n
have he : Summable.{u_3, 0} (α := α) fun (k : ℕ) ↦ HPow.hPow (α := α) (-1) (2 * k) * f (2 * k)
Tactic: apply Summable.even_add_odd
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.NatInt (goal)
Goal:
α : Type u_3
inst : Ring α
inst_1 : UniformSpace α
inst_2 : IsUniformAddGroup α
inst_3 : CompleteSpace α
f : ℕ → α
hf : Summable f
he : Summable.{u_3, 0} (α := α) fun (k : ℕ) ↦ HPow.hPow (α := α) (-1) (2 * k) * f (2 * k)
⊢ Summable.{u_3, 0} (α := α) fun (n : ℕ) ↦ HPow.hPow (α := α) (-1) n * f n
have ho : Summable.{u_3, 0} (α := α) fun (k : ℕ) ↦ HPow.hPow (α := α) (-1) (2 * k + 1) * f (2 * k + 1)
Tactic: apply Summable.even_add_odd
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.NatInt (goal)
Goal:
α : Type u_3
inst : Ring α
inst_1 : UniformSpace α
inst_2 : IsUniformAddGroup α
inst_3 : CompleteSpace α
f : ℕ → α
hf : Summable f
⊢ Summable.{u_3, 0} (α := α) fun (k : ℕ) ↦ HPow.hPow (α := α) (-1) (2 * k) * f (2 * k)
have he : Summable.{u_3, 0} (α := α) fun (k : ℕ) ↦ f (2 * k)
Tactic: simp only [even_two, Even.mul_right, Even.neg_pow, one_pow, one_mul]
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.NatInt (goal)
Goal:
α : Type u_3
inst : Ring α
inst_1 : UniformSpace α
inst_2 : IsUniformAddGroup α
inst_3 : CompleteSpace α
f : ℕ → α
hf : Summable f
⊢ Summable.{u_3, 0} (α := α) fun (k : ℕ) ↦ HPow.hPow (α := α) (-1) (2 * k + 1) * f (2 * k + 1)
have ho : Summable.{u_3, 0} (α := α) fun (k : ℕ) ↦ -f (2 * k + 1)
Tactic: simp only [pow_add, even_two, Even.mul_right, Even.neg_pow, one_pow, pow_one, mul_neg, mul_one,
      neg_mul, one_mul]
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.NatInt (goal)
Goal:
α : Type u_3
inst : Ring α
inst_1 : UniformSpace α
inst_2 : IsUniformAddGroup α
inst_3 : CompleteSpace α
f : ℕ → α
hf : Summable f
⊢ Summable.{u_3, 0} (α := α) fun (k : ℕ) ↦ -f (2 * k + 1)
have ho : Summable.{u_3, 0} (α := α) fun (b : ℕ) ↦ f (2 * b + 1)
Tactic: apply Summable.neg
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.NatInt (goal)
Goal:
α : Type u_3
inst : Ring α
inst_1 : UniformSpace α
inst_2 : IsUniformAddGroup α
inst_3 : CompleteSpace α
f : ℕ → α
hf : Summable f
⊢ Summable.{u_3, 0} (α := α) fun (b : ℕ) ↦ f (2 * b + 1)
have ho : Injective (β := ℕ) fun (b : ℕ) ↦ 2 * b + 1
Tactic: apply hf.comp_injective