awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Module
Goal:
α : Type u_1
β : Type u_2
M : Type u_11
inst : TopologicalSpace M
inst_1 : AddCommMonoid M
inst_2 : T2Space M
R : Type u_12
inst_3 : DivisionRing R
inst_4 : Module R M
inst_5 : ContinuousConstSMul R M
inst_6 : Group α
inst_7 : MulAction α β
f : β → M
g : Quotient (orbitRel α β) → R
b : β
h :
  Quotient.lift (fun (b : β) ↦ ∑' (a : α), g (Quotient.mk' (a • b)) • f (a • b)) ⋯ ⟦b⟧ =
    g ⟦b⟧ • Quotient.lift (fun (b : β) ↦ ∑' (a : α), f (a • b)) ⋯ ⟦b⟧
⊢ automorphize (g ∘ Quotient.mk' • f) ⟦b⟧ = HSMul.hSMul (β := Quotient (orbitRel α β) → M) g (automorphize f) ⟦b⟧

Tactic:
simp only [automorphize, Pi.smul_apply', comp_apply]

Premises used: Pi.smul_apply', MulAction.automorphize, Function.comp_apply
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Module
Goal:
α : Type u_1
β : Type u_2
M : Type u_11
inst : TopologicalSpace M
inst_1 : AddCommMonoid M
inst_2 : T2Space M
R : Type u_12
inst_3 : DivisionRing R
inst_4 : Module R M
inst_5 : ContinuousConstSMul R M
inst_6 : Group α
inst_7 : MulAction α β
f : β → M
g : Quotient (orbitRel α β) → R
b : β
h :
  let π := Quotient.mk (orbitRel α β);
  Quotient.lift (fun (b : β) ↦ ∑' (a : α), g (Quotient.mk' (a • b)) • f (a • b)) ⋯ (π b) =
    g (π b) • Quotient.lift (fun (b : β) ↦ ∑' (a : α), f (a • b)) ⋯ (π b)
⊢ Quotient.lift (fun (b : β) ↦ ∑' (a : α), g (Quotient.mk' (a • b)) • f (a • b)) ⋯ ⟦b⟧ =
    g ⟦b⟧ • Quotient.lift (fun (b : β) ↦ ∑' (a : α), f (a • b)) ⋯ ⟦b⟧

Tactic:
set π : β → Quotient (MulAction.orbitRel α β) := Quotient.mk (MulAction.orbitRel α β)

Premises used: MulAction.orbitRel, Quotient.mk
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Module
Goal:
α : Type u_1
β : Type u_2
M : Type u_11
inst : TopologicalSpace M
inst_1 : AddCommMonoid M
inst_2 : T2Space M
R : Type u_12
inst_3 : DivisionRing R
inst_4 : Module R M
inst_5 : ContinuousConstSMul R M
inst_6 : Group α
inst_7 : MulAction α β
f : β → M
g : Quotient (orbitRel α β) → R
b : β
π : β → Quotient (orbitRel α β) := Quotient.mk (orbitRel α β)
a : α
apply : (orbitRel α β : β → β → Prop) (a • b) b
⊢ π (a • b) = π b

Tactic:
apply (@Quotient.eq _ (MulAction.orbitRel α β) (a • b) b).mpr

Premises used: Iff.mpr, Quotient.eq
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Module
Goal:
α : Type u_1
β : Type u_2
M : Type u_11
inst : TopologicalSpace M
inst_1 : AddCommMonoid M
inst_2 : T2Space M
R : Type u_12
inst_3 : DivisionRing R
inst_4 : Module R M
inst_5 : ContinuousConstSMul R M
inst_6 : Group α
inst_7 : MulAction α β
f : β → M
g : Quotient (orbitRel α β) → R
b : β
π : β → Quotient (orbitRel α β) := Quotient.mk (orbitRel α β)
a w : α
h : (fun (m : α) ↦ m • b) a = a • b
⊢ (orbitRel α β : β → β → Prop) (a • b) b

Tactic:
use a
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Module
Goal:
α : Type u_1
β : Type u_2
M : Type u_11
inst : TopologicalSpace M
inst_1 : AddCommMonoid M
inst_2 : T2Space M
R : Type u_12
inst_3 : DivisionRing R
inst_4 : Module R M
inst_5 : ContinuousConstSMul R M
inst_6 : Group α
inst_7 : MulAction α β
f : β → M
g : Quotient (orbitRel α β) → R
b : β
π : β → Quotient (orbitRel α β) := Quotient.mk (orbitRel α β)
⊢ ∀ (a : α), π (a • b) = π b

Tactic:
have H₁ : ∀ a : α, π (a • b) = π b := by
    intro a
    apply (@Quotient.eq _ (MulAction.orbitRel α β) (a • b) b).mpr
    use a
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Module
Goal:
α : Type u_1
β : Type u_2
M : Type u_11
inst : TopologicalSpace M
inst_1 : AddCommMonoid M
inst_2 : T2Space M
R : Type u_12
inst_3 : DivisionRing R
inst_4 : Module R M
inst_5 : ContinuousConstSMul R M
inst_6 : Group α
inst_7 : MulAction α β
f : β → M
g : Quotient (orbitRel α β) → R
b : β
π : β → Quotient (orbitRel α β) := Quotient.mk (orbitRel α β)
H₁ : ∀ (a : α), π (a • b) = π b
h : ∑' (a : α), g (π (a • b)) • f (a • b) = HSMul.hSMul (β := M) (g (π b)) (∑' (a : α), f (a • b))
⊢ Quotient.lift (fun (b : β) ↦ ∑' (a : α), g (Quotient.mk' (a • b)) • f (a • b)) ⋯ (π b) =
    g (π b) • Quotient.lift (fun (b : β) ↦ ∑' (a : α), f (a • b)) ⋯ (π b)

Tactic:
change ∑' a : α, g (π (a • b)) • f (a • b) = g (π b) • ∑' a : α, f (a • b)
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Module
Goal:
α : Type u_1
β : Type u_2
M : Type u_11
inst : TopologicalSpace M
inst_1 : AddCommMonoid M
inst_2 : T2Space M
R : Type u_12
inst_3 : DivisionRing R
inst_4 : Module R M
inst_5 : ContinuousConstSMul R M
inst_6 : Group α
inst_7 : MulAction α β
f : β → M
g : Quotient (orbitRel α β) → R
b : β
π : β → Quotient (orbitRel α β) := Quotient.mk (orbitRel α β)
H₁ : ∀ (a : α), π (a • b) = π b
h : ∑' (a : α), g (π b) • f (a • b) = HSMul.hSMul (β := M) (g (π b)) (∑' (a : α), f (a • b))
⊢ ∑' (a : α), g (π (a • b)) • f (a • b) = HSMul.hSMul (β := M) (g (π b)) (∑' (a : α), f (a • b))

Tactic:
simp_rw [H₁]
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Module
Goal:
α : Type u_1
β : Type u_2
M : Type u_11
inst : TopologicalSpace M
inst_1 : AddCommMonoid M
inst_2 : T2Space M
R : Type u_12
inst_3 : DivisionRing R
inst_4 : Module R M
inst_5 : ContinuousConstSMul R M
inst_6 : Group α
inst_7 : MulAction α β
f : β → M
g : Quotient (orbitRel α β) → R
b : β
π : β → Quotient (orbitRel α β) := Quotient.mk (orbitRel α β)
H₁ : ∀ (a : α), π (a • b) = π b
⊢ ∑' (a : α), g (π b) • f (a • b) = HSMul.hSMul (β := M) (g (π b)) (∑' (a : α), f (a • b))

Tactic:
tsum_const_smul'' _

Premises used: tsum_const_smul''
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Module
Goal:
α : Type u_1
β : Type u_2
M : Type u_11
inst : TopologicalSpace M
inst_1 : AddCommMonoid M
inst_2 : T2Space M
R : Type u_12
inst_3 : DivisionRing R
inst_4 : Module R M
inst_5 : ContinuousConstSMul R M
inst_6 : Group α
inst_7 : MulAction α β
f : β → M
g : Quotient (orbitRel α β) → R
b : β
π : β → Quotient (orbitRel α β) := Quotient.mk (orbitRel α β)
H₁ : ∀ (a : α), π (a • b) = π b
⊢ ∑' (a : α), g (π b) • f (a • b) = HSMul.hSMul (β := M) (g (π b)) (∑' (a : α), f (a • b))

Tactic:
exact tsum_const_smul'' _

Premises used: tsum_const_smul''
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Module
Goal:
α : Type u_1
β : Type u_2
M : Type u_11
inst : TopologicalSpace M
inst_1 : AddCommMonoid M
inst_2 : T2Space M
R : Type u_12
inst_3 : DivisionRing R
inst_4 : Module R M
inst_5 : ContinuousConstSMul R M
inst_6 : AddGroup α
inst_7 : AddAction α β
f : β → M
g : Quotient (orbitRel α β) → R
h :
  ∀ (x : Quotient (orbitRel α β)),
    automorphize (g ∘ Quotient.mk' • f) x = HSMul.hSMul (β := Quotient (orbitRel α β) → M) g (automorphize f) x
⊢ automorphize (g ∘ Quotient.mk' • f) = HSMul.hSMul (β := Quotient (orbitRel α β) → M) g (automorphize f)

Tactic:
ext x
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Module
Goal:
α : Type u_1
β : Type u_2
M : Type u_11
inst : TopologicalSpace M
inst_1 : AddCommMonoid M
inst_2 : T2Space M
R : Type u_12
inst_3 : DivisionRing R
inst_4 : Module R M
inst_5 : ContinuousConstSMul R M
inst_6 : AddGroup α
inst_7 : AddAction α β
f : β → M
g : Quotient (orbitRel α β) → R
x : Quotient (orbitRel α β)
h :
  ∀ (b : β),
    automorphize (g ∘ Quotient.mk' • f) ⟦b⟧ = HSMul.hSMul (β := Quotient (orbitRel α β) → M) g (automorphize f) ⟦b⟧
⊢ automorphize (g ∘ Quotient.mk' • f) x = HSMul.hSMul (β := Quotient (orbitRel α β) → M) g (automorphize f) x

Tactic:
induction x using Quotient.inductionOn with | _ b
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Module
Goal:
α : Type u_1
β : Type u_2
M : Type u_11
inst : TopologicalSpace M
inst_1 : AddCommMonoid M
inst_2 : T2Space M
R : Type u_12
inst_3 : DivisionRing R
inst_4 : Module R M
inst_5 : ContinuousConstSMul R M
inst_6 : AddGroup α
inst_7 : AddAction α β
f : β → M
g : Quotient (orbitRel α β) → R
b : β
h :
  Quotient.lift (fun (b : β) ↦ ∑' (a : α), g (Quotient.mk' (a +ᵥ b)) • f (a +ᵥ b)) ⋯ ⟦b⟧ =
    g ⟦b⟧ • Quotient.lift (fun (b : β) ↦ ∑' (a : α), f (a +ᵥ b)) ⋯ ⟦b⟧
⊢ automorphize (g ∘ Quotient.mk' • f) ⟦b⟧ = HSMul.hSMul (β := Quotient (orbitRel α β) → M) g (automorphize f) ⟦b⟧

Tactic:
simp only [automorphize, Pi.smul_apply', comp_apply]

Premises used: Pi.smul_apply', Function.comp_apply, AddAction.automorphize
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Module
Goal:
α : Type u_1
β : Type u_2
M : Type u_11
inst : TopologicalSpace M
inst_1 : AddCommMonoid M
inst_2 : T2Space M
R : Type u_12
inst_3 : DivisionRing R
inst_4 : Module R M
inst_5 : ContinuousConstSMul R M
inst_6 : AddGroup α
inst_7 : AddAction α β
f : β → M
g : Quotient (orbitRel α β) → R
b : β
h :
  let π := Quotient.mk (orbitRel α β);
  Quotient.lift (fun (b : β) ↦ ∑' (a : α), g (Quotient.mk' (a +ᵥ b)) • f (a +ᵥ b)) ⋯ (π b) =
    g (π b) • Quotient.lift (fun (b : β) ↦ ∑' (a : α), f (a +ᵥ b)) ⋯ (π b)
⊢ Quotient.lift (fun (b : β) ↦ ∑' (a : α), g (Quotient.mk' (a +ᵥ b)) • f (a +ᵥ b)) ⋯ ⟦b⟧ =
    g ⟦b⟧ • Quotient.lift (fun (b : β) ↦ ∑' (a : α), f (a +ᵥ b)) ⋯ ⟦b⟧

Tactic:
set π : β → Quotient (AddAction.orbitRel α β) := Quotient.mk (AddAction.orbitRel α β)

Premises used: Quotient.mk, AddAction.orbitRel
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Module
Goal:
α : Type u_1
β : Type u_2
M : Type u_11
inst : TopologicalSpace M
inst_1 : AddCommMonoid M
inst_2 : T2Space M
R : Type u_12
inst_3 : DivisionRing R
inst_4 : Module R M
inst_5 : ContinuousConstSMul R M
inst_6 : AddGroup α
inst_7 : AddAction α β
f : β → M
g : Quotient (orbitRel α β) → R
b : β
π : β → Quotient (orbitRel α β) := Quotient.mk (orbitRel α β)
a : α
apply : (orbitRel α β : β → β → Prop) (a +ᵥ b) b
⊢ π (a +ᵥ b) = π b

Tactic:
apply (@Quotient.eq _ (AddAction.orbitRel α β) (a +ᵥ b) b).mpr

Premises used: Iff.mpr, Quotient.eq
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Module
Goal:
α : Type u_1
β : Type u_2
M : Type u_11
inst : TopologicalSpace M
inst_1 : AddCommMonoid M
inst_2 : T2Space M
R : Type u_12
inst_3 : DivisionRing R
inst_4 : Module R M
inst_5 : ContinuousConstSMul R M
inst_6 : AddGroup α
inst_7 : AddAction α β
f : β → M
g : Quotient (orbitRel α β) → R
b : β
π : β → Quotient (orbitRel α β) := Quotient.mk (orbitRel α β)
a w : α
h : (fun (m : α) ↦ m +ᵥ b) a = a +ᵥ b
⊢ (orbitRel α β : β → β → Prop) (a +ᵥ b) b

Tactic:
use a
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Module
Goal:
α : Type u_1
β : Type u_2
M : Type u_11
inst : TopologicalSpace M
inst_1 : AddCommMonoid M
inst_2 : T2Space M
R : Type u_12
inst_3 : DivisionRing R
inst_4 : Module R M
inst_5 : ContinuousConstSMul R M
inst_6 : AddGroup α
inst_7 : AddAction α β
f : β → M
g : Quotient (orbitRel α β) → R
b : β
π : β → Quotient (orbitRel α β) := Quotient.mk (orbitRel α β)
⊢ ∀ (a : α), π (a +ᵥ b) = π b

Tactic:
have H₁ : ∀ a : α, π (a +ᵥ b) = π b := by
    intro a
    apply (@Quotient.eq _ (AddAction.orbitRel α β) (a +ᵥ b) b).mpr
    use a
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Module
Goal:
α : Type u_1
β : Type u_2
M : Type u_11
inst : TopologicalSpace M
inst_1 : AddCommMonoid M
inst_2 : T2Space M
R : Type u_12
inst_3 : DivisionRing R
inst_4 : Module R M
inst_5 : ContinuousConstSMul R M
inst_6 : AddGroup α
inst_7 : AddAction α β
f : β → M
g : Quotient (orbitRel α β) → R
b : β
π : β → Quotient (orbitRel α β) := Quotient.mk (orbitRel α β)
H₁ : ∀ (a : α), π (a +ᵥ b) = π b
h : ∑' (a : α), g (π (a +ᵥ b)) • f (a +ᵥ b) = HSMul.hSMul (β := M) (g (π b)) (∑' (a : α), f (a +ᵥ b))
⊢ Quotient.lift (fun (b : β) ↦ ∑' (a : α), g (Quotient.mk' (a +ᵥ b)) • f (a +ᵥ b)) ⋯ (π b) =
    g (π b) • Quotient.lift (fun (b : β) ↦ ∑' (a : α), f (a +ᵥ b)) ⋯ (π b)

Tactic:
change ∑' a : α, g (π (a +ᵥ b)) • f (a +ᵥ b) = g (π b) • ∑' a : α, f (a +ᵥ b)
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Module
Goal:
α : Type u_1
β : Type u_2
M : Type u_11
inst : TopologicalSpace M
inst_1 : AddCommMonoid M
inst_2 : T2Space M
R : Type u_12
inst_3 : DivisionRing R
inst_4 : Module R M
inst_5 : ContinuousConstSMul R M
inst_6 : AddGroup α
inst_7 : AddAction α β
f : β → M
g : Quotient (orbitRel α β) → R
b : β
π : β → Quotient (orbitRel α β) := Quotient.mk (orbitRel α β)
H₁ : ∀ (a : α), π (a +ᵥ b) = π b
h : ∑' (a : α), g (π b) • f (a +ᵥ b) = HSMul.hSMul (β := M) (g (π b)) (∑' (a : α), f (a +ᵥ b))
⊢ ∑' (a : α), g (π (a +ᵥ b)) • f (a +ᵥ b) = HSMul.hSMul (β := M) (g (π b)) (∑' (a : α), f (a +ᵥ b))

Tactic:
simp_rw [H₁]
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Module
Goal:
α : Type u_1
β : Type u_2
M : Type u_11
inst : TopologicalSpace M
inst_1 : AddCommMonoid M
inst_2 : T2Space M
R : Type u_12
inst_3 : DivisionRing R
inst_4 : Module R M
inst_5 : ContinuousConstSMul R M
inst_6 : AddGroup α
inst_7 : AddAction α β
f : β → M
g : Quotient (orbitRel α β) → R
b : β
π : β → Quotient (orbitRel α β) := Quotient.mk (orbitRel α β)
H₁ : ∀ (a : α), π (a +ᵥ b) = π b
⊢ ∑' (a : α), g (π b) • f (a +ᵥ b) = HSMul.hSMul (β := M) (g (π b)) (∑' (a : α), f (a +ᵥ b))

Tactic:
tsum_const_smul'' _

Premises used: tsum_const_smul''
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Module
Goal:
α : Type u_1
β : Type u_2
M : Type u_11
inst : TopologicalSpace M
inst_1 : AddCommMonoid M
inst_2 : T2Space M
R : Type u_12
inst_3 : DivisionRing R
inst_4 : Module R M
inst_5 : ContinuousConstSMul R M
inst_6 : AddGroup α
inst_7 : AddAction α β
f : β → M
g : Quotient (orbitRel α β) → R
b : β
π : β → Quotient (orbitRel α β) := Quotient.mk (orbitRel α β)
H₁ : ∀ (a : α), π (a +ᵥ b) = π b
⊢ ∑' (a : α), g (π b) • f (a +ᵥ b) = HSMul.hSMul (β := M) (g (π b)) (∑' (a : α), f (a +ᵥ b))

Tactic:
exact tsum_const_smul'' _

Premises used: tsum_const_smul''
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Module
Goal:
M : Type u_11
inst : TopologicalSpace M
inst_1 : AddCommMonoid M
inst_2 : T2Space M
R : Type u_12
inst_3 : DivisionRing R
inst_4 : Module R M
inst_5 : ContinuousConstSMul R M
G : Type u_13
inst_6 : Group G
Γ : Subgroup G
f : G → M
g : G ⧸ Γ → R
⊢ automorphize (g ∘ Quotient.mk' • f) = HSMul.hSMul (β := G ⧸ Γ → M) g (automorphize f)

Tactic:
MulAction.automorphize_smul_left f g

Premises used: QuotientGroup.automorphize, MulAction.automorphize_smul_left
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Module
Goal:
M : Type u_11
inst : TopologicalSpace M
inst_1 : AddCommMonoid M
inst_2 : T2Space M
R : Type u_12
inst_3 : DivisionRing R
inst_4 : Module R M
inst_5 : ContinuousConstSMul R M
G : Type u_13
inst_6 : AddGroup G
Γ : AddSubgroup G
f : G → M
g : G ⧸ Γ → R
⊢ automorphize (g ∘ Quotient.mk' • f) = HSMul.hSMul (β := G ⧸ Γ → M) g (automorphize f)

Tactic:
AddAction.automorphize_smul_left f g

Premises used: AddAction.automorphize_smul_left, QuotientAddGroup.automorphize
-- Module: Mathlib.Topology.Algebra.InfiniteSum.NatInt
Goal:
M : Type u_1
inst : CommMonoid M
inst_1 : TopologicalSpace M
m : M
f : ℕ → M
h : HasProd f m
⊢ Tendsto (fun (n : ℕ) ↦ ∏ i ∈ range n, f i) atTop (𝓝 m)

Tactic:
h.comp tendsto_finset_range

Premises used: Multiset.foldr, Multiset.prod, Finset.prod, Filter.tendsto_finset_range, Filter.Tendsto.comp
-- Module: Mathlib.Topology.Algebra.InfiniteSum.NatInt
Goal:
M : Type u_1
inst : CommMonoid M
inst_1 : TopologicalSpace M
f : ℕ → M
h : Multipliable f
⊢ Tendsto.{0, u_1} (β := M) (fun (n : ℕ) ↦ ∏ i ∈ range n, f i) atTop (𝓝 (∏' (i : ℕ), f i))

Tactic:
h.hasProd.tendsto_prod_nat

Premises used: HasProd.tendsto_prod_nat, Multipliable.hasProd
-- Module: Mathlib.Topology.Algebra.InfiniteSum.NatInt
Goal:
M : Type u_1
inst : CommMonoid M
inst_1 : TopologicalSpace M
m : M
inst_2 : ContinuousMul M
f : ℕ → M
k : ℕ
h : HasProd (fun (n : ℕ) ↦ f (n + k)) m
⊢ HasProd f ((∏ i ∈ range k, f i) * m)

Tactic:
((range k).hasProd f).mul_compl <| (notMemRangeEquiv k).symm.hasProd_iff.mp h

Premises used: Set.Elem, Equiv.hasProd_iff, Finset.range, SetLike.coe, Iff.mp, Finset.hasProd, Equiv.symm, HasProd.mul_compl, notMemRangeEquiv, SummationFilter.unconditional
-- Module: Mathlib.Topology.Algebra.InfiniteSum.NatInt
Goal:
M : Type u_1
inst : CommMonoid M
inst_1 : TopologicalSpace M
m : M
inst_2 : ContinuousMul M
f : ℕ → M
h : HasProd (fun (n : ℕ) ↦ f (n + 1)) m
⊢ HasProd f (f 0 * m)

Tactic:
simpa only [prod_range_one] using h.prod_range_mul

Premises used: Finset.prod_range_one, HasProd.prod_range_mul
-- Module: Mathlib.Topology.Algebra.InfiniteSum.NatInt
Goal:
M : Type u_1
inst : CommMonoid M
inst_1 : TopologicalSpace M
m m' : M
inst_2 : ContinuousMul M
f : ℕ → M
he : HasProd (fun (k : ℕ) ↦ f (2 * k)) m
ho : HasProd (fun (k : ℕ) ↦ f (2 * k + 1)) m'
⊢ Injective (β := ℕ) fun (x : ℕ) ↦ 2 * x

Tactic:
have := mul_right_injective₀ (two_ne_zero' ℕ)
-- Module: Mathlib.Topology.Algebra.InfiniteSum.NatInt
Goal:
M : Type u_1
inst : CommMonoid M
inst_1 : TopologicalSpace M
m m' : M
inst_2 : ContinuousMul M
f : ℕ → M
he : HasProd (fun (k : ℕ) ↦ f (2 * k)) m
ho : HasProd (fun (k : ℕ) ↦ f (2 * k + 1)) m'
this : Injective (β := ℕ) fun (x : ℕ) ↦ 2 * x
⊢ HasProd (fun (x : (↑(Set.range (ι := ℕ) ((fun (x : ℕ) ↦ x + 1) ∘ fun (x : ℕ) ↦ 2 * x)) : Type)) ↦ f (↑x : ℕ)) m'

Tactic:
replace ho := ((add_left_injective 1).comp this).hasProd_range_iff.2 ho
-- Module: Mathlib.Topology.Algebra.InfiniteSum.NatInt
Goal:
M : Type u_1
inst : CommMonoid M
inst_1 : TopologicalSpace M
m m' : M
inst_2 : ContinuousMul M
f : ℕ → M
he : HasProd (fun (k : ℕ) ↦ f (2 * k)) m
this : Injective (β := ℕ) fun (x : ℕ) ↦ 2 * x
ho : HasProd (fun (x : (↑(Set.range (ι := ℕ) ((fun (x : ℕ) ↦ x + 1) ∘ fun (x : ℕ) ↦ 2 * x)) : Type)) ↦ f (↑x : ℕ)) m'
⊢ HasProd f (m * m')

Tactic:
(this.hasProd_range_iff.2 he).mul_isCompl ?_ ho

Premises used: Iff.mpr, HasProd.mul_isCompl, Function.Injective.hasProd_range_iff
-- Module: Mathlib.Topology.Algebra.InfiniteSum.NatInt
Goal:
M : Type u_1
inst : CommMonoid M
inst_1 : TopologicalSpace M
m m' : M
inst_2 : ContinuousMul M
f : ℕ → M
he : HasProd (fun (k : ℕ) ↦ f (2 * k)) m
this : Injective (β := ℕ) fun (x : ℕ) ↦ 2 * x
ho : HasProd (fun (x : (↑(Set.range (ι := ℕ) ((fun (x : ℕ) ↦ x + 1) ∘ fun (x : ℕ) ↦ 2 * x)) : Type)) ↦ f (↑x : ℕ)) m'
refine :
  IsCompl (α := Set ℕ) (Set.range fun (x : ℕ) ↦ 2 * x)
    (Set.range (ι := ℕ) ((fun (x : ℕ) ↦ x + 1) ∘ fun (x : ℕ) ↦ 2 * x))
⊢ HasProd f (m * m')

Tactic:
refine (this.hasProd_range_iff.2 he).mul_isCompl ?_ ho

Premises used: Iff.mpr, HasProd.mul_isCompl, Function.Injective.hasProd_range_iff
-- Module: Mathlib.Topology.Algebra.InfiniteSum.NatInt
Goal:
M : Type u_1
inst : CommMonoid M
inst_1 : TopologicalSpace M
m m' : M
inst_2 : ContinuousMul M
f : ℕ → M
he : HasProd (fun (k : ℕ) ↦ f (2 * k)) m
this : Injective (β := ℕ) fun (x : ℕ) ↦ 2 * x
ho : HasProd (fun (x : (↑(Set.range (ι := ℕ) ((fun (x : ℕ) ↦ x + 1) ∘ fun (x : ℕ) ↦ 2 * x)) : Type)) ↦ f (↑x : ℕ)) m'
⊢ IsCompl (α := Set ℕ) (Set.range fun (x : ℕ) ↦ 2 * x)
    (Set.range (ι := ℕ) ((fun (x : ℕ) ↦ x + 1) ∘ fun (x : ℕ) ↦ 2 * x))

Tactic:
simpa [Function.comp_def] using Nat.isCompl_even_odd

Premises used: Function.comp_def, Nat.isCompl_even_odd
-- Module: Mathlib.Topology.Algebra.InfiniteSum.NatInt
Goal:
M : Type u_1
inst : CommMonoid M
inst_1 : TopologicalSpace M
m : M
inst_2 : T2Space M
f : ℕ → M
hf : Multipliable f
⊢ HasProd f m ↔ Tendsto (fun (n : ℕ) ↦ ∏ i ∈ range n, f i) atTop (𝓝 m)

Tactic:
⟨fun h ↦ h.tendsto_prod_nat, fun h ↦ ?_⟩

Premises used: HasProd.tendsto_prod_nat, Iff.intro
-- Module: Mathlib.Topology.Algebra.InfiniteSum.NatInt
Goal:
M : Type u_1
inst : CommMonoid M
inst_1 : TopologicalSpace M
m : M
inst_2 : T2Space M
f : ℕ → M
hf : Multipliable f
refine : ∀ (h : Tendsto (fun (n : ℕ) ↦ ∏ i ∈ range n, f i) atTop (𝓝 m)), HasProd f m
⊢ HasProd f m ↔ Tendsto (fun (n : ℕ) ↦ ∏ i ∈ range n, f i) atTop (𝓝 m)

Tactic:
refine ⟨fun h ↦ h.tendsto_prod_nat, fun h ↦ ?_⟩
-- Module: Mathlib.Topology.Algebra.InfiniteSum.NatInt
Goal:
M : Type u_1
inst : CommMonoid M
inst_1 : TopologicalSpace M
m : M
inst_2 : T2Space M
f : ℕ → M
hf : Multipliable f
h : Tendsto (fun (n : ℕ) ↦ ∏ i ∈ range n, f i) atTop (𝓝 m)
rw : HasProd f (∏' (b : ℕ), f b)
⊢ HasProd f m

Tactic:
rw [tendsto_nhds_unique h hf.hasProd.tendsto_prod_nat]

Premises used: HasProd.tendsto_prod_nat, Multipliable.hasProd, tendsto_nhds_unique
-- Module: Mathlib.Topology.Algebra.InfiniteSum.NatInt
Goal:
M : Type u_1
inst : CommMonoid M
inst_1 : TopologicalSpace M
m : M
inst_2 : T2Space M
f : ℕ → M
hf : Multipliable f
h : Tendsto (fun (n : ℕ) ↦ ∏ i ∈ range n, f i) atTop (𝓝 m)
⊢ HasProd f (∏' (b : ℕ), f b)

Tactic:
hf.hasProd

Premises used: Multipliable.hasProd
-- Module: Mathlib.Topology.Algebra.InfiniteSum.NatInt
Goal:
M : Type u_1
inst : CommMonoid M
inst_1 : TopologicalSpace M
m : M
inst_2 : T2Space M
f : ℕ → M
hf : Multipliable f
h : Tendsto (fun (n : ℕ) ↦ ∏ i ∈ range n, f i) atTop (𝓝 m)
⊢ HasProd f (∏' (b : ℕ), f b)

Tactic:
exact hf.hasProd

Premises used: Multipliable.hasProd
-- Module: Mathlib.Topology.Algebra.InfiniteSum.NatInt
Goal:
M : Type u_1
inst : CommMonoid M
inst_1 : TopologicalSpace M
inst_2 : ContinuousMul M
f : ℕ → M
k : ℕ
h : Multipliable.{u_1, 0} (α := M) fun (n : ℕ) ↦ f (n + k)
⊢ Multipliable f

Tactic:
h.hasProd.prod_range_mul.multipliable

Premises used: Multipliable.hasProd, HasProd.multipliable, HasProd.prod_range_mul
-- Module: Mathlib.Topology.Algebra.InfiniteSum.NatInt
Goal:
M : Type u_1
inst : CommMonoid M
inst_1 : TopologicalSpace M
inst_2 : ContinuousMul M
f : ℕ → M
he : Multipliable.{u_1, 0} (α := M) fun (k : ℕ) ↦ f (2 * k)
ho : Multipliable.{u_1, 0} (α := M) fun (k : ℕ) ↦ f (2 * k + 1)
⊢ Multipliable f

Tactic:
(he.hasProd.even_mul_odd ho.hasProd).multipliable

Premises used: Multipliable.hasProd, HasProd.even_mul_odd, HasProd.multipliable
-- Module: Mathlib.Topology.Algebra.InfiniteSum.NatInt
Goal:
M : Type u_1
inst : CommMonoid M
inst_1 : TopologicalSpace M
α : Type u_3
β : Type u_4
inst_2 : Encodable β
inst_3 : CompleteLattice α
m : α → M
m0 : m ⊥ = 1
s : β → α
rw :
  Eq.{u_1 + 1} (α := M) (∏' (i : ℕ), m (⨆ b ∈ decode₂ β i, s b)) (∏' (y : ℕ), extend encode (fun (b : β) ↦ m (s b)) 1 y)
⊢ Eq.{u_1 + 1} (α := M) (∏' (i : ℕ), m (⨆ b ∈ decode₂ β i, s b)) (∏' (b : β), m (s b))

Tactic:
rw [← tprod_extend_one (@encode_injective β _)]

Premises used: tprod_extend_one, Encodable.encode_injective
-- Module: Mathlib.Topology.Algebra.InfiniteSum.NatInt
Goal:
M : Type u_1
inst : CommMonoid M
inst_1 : TopologicalSpace M
α : Type u_3
β : Type u_4
inst_2 : Encodable β
inst_3 : CompleteLattice α
m : α → M
m0 : m ⊥ = 1
s : β → α
⊢ Eq.{u_1 + 1} (α := M) (∏' (i : ℕ), m (⨆ b ∈ decode₂ β i, s b)) (∏' (y : ℕ), extend encode (fun (b : β) ↦ m (s b)) 1 y)

Tactic:
tprod_congr fun n ↦ ?_

Premises used: tprod_congr
-- Module: Mathlib.Topology.Algebra.InfiniteSum.NatInt
Goal:
M : Type u_1
inst : CommMonoid M
inst_1 : TopologicalSpace M
α : Type u_3
β : Type u_4
inst_2 : Encodable β
inst_3 : CompleteLattice α
m : α → M
m0 : m ⊥ = 1
s : β → α
refine : ∀ (n : ℕ), m (⨆ b ∈ decode₂ β n, s b) = extend encode (fun (b : β) ↦ m (s b)) 1 n
⊢ Eq.{u_1 + 1} (α := M) (∏' (i : ℕ), m (⨆ b ∈ decode₂ β i, s b)) (∏' (y : ℕ), extend encode (fun (b : β) ↦ m (s b)) 1 y)

Tactic:
refine tprod_congr fun n ↦ ?_

Premises used: tprod_congr
-- Module: Mathlib.Topology.Algebra.InfiniteSum.NatInt
Goal:
M : Type u_1
inst : CommMonoid M
inst_1 : TopologicalSpace M
α : Type u_3
β : Type u_4
inst_2 : Encodable β
inst_3 : CompleteLattice α
m : α → M
m0 : m ⊥ = 1
s : β → α
n : ℕ
inl : ∀ (a : β), m (⨆ b ∈ decode₂ β (encode a), s b) = extend encode (fun (b : β) ↦ m (s b)) 1 (encode a)
inr :
  ∀ (hn : n ∉ Set.range.{0, u_4 + 1} (ι := β) encode),
    m (⨆ b ∈ decode₂ β n, s b) = extend encode (fun (b : β) ↦ m (s b)) 1 n
⊢ m (⨆ b ∈ decode₂ β n, s b) = extend encode (fun (b : β) ↦ m (s b)) 1 n

Tactic:
rcases em (n ∈ Set.range (encode : β → ℕ)) with ⟨a, rfl⟩ | hn

Premises used: Membership.mem, em, Encodable.encode, Set.range, rfl
-- Module: Mathlib.Topology.Algebra.InfiniteSum.NatInt
Goal:
M : Type u_1
inst : CommMonoid M
inst_1 : TopologicalSpace M
α : Type u_3
β : Type u_4
inst_2 : Encodable β
inst_3 : CompleteLattice α
m : α → M
m0 : m ⊥ = 1
s : β → α
a : β
⊢ m (⨆ b ∈ decode₂ β (encode a), s b) = extend encode (fun (b : β) ↦ m (s b)) 1 (encode a)

Tactic:
simp [encode_injective.extend_apply]

Premises used: Encodable.encode_injective, Function.Injective.extend_apply
-- Module: Mathlib.Topology.Algebra.InfiniteSum.NatInt
Goal:
M : Type u_1
inst : CommMonoid M
inst_1 : TopologicalSpace M
α : Type u_3
β : Type u_4
inst_2 : Encodable β
inst_3 : CompleteLattice α
m : α → M
m0 : m ⊥ = 1
s : β → α
n : ℕ
hn : n ∉ Set.range.{0, u_4 + 1} (ι := β) encode
inr : m (⨆ b ∈ decode₂ β n, s b) = 1 n
⊢ m (⨆ b ∈ decode₂ β n, s b) = extend encode (fun (b : β) ↦ m (s b)) 1 n

Tactic:
rw [extend_apply' _ _ _ hn]

Premises used: Function.extend_apply'