awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Module
Goal:
ι : Type u_5
R : Type u_7
R₂ : Type u_8
M : Type u_9
M₂ : Type u_10
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : AddCommMonoid M
inst_3 : Module R M
inst_4 : AddCommMonoid M₂
inst_5 : Module R₂ M₂
inst_6 : TopologicalSpace M
inst_7 : TopologicalSpace M₂
σ : R →+* R₂
σ' : R₂ →+* R
inst_8 : RingHomInvPair σ σ'
inst_9 : RingHomInvPair σ' σ
L : SummationFilter ι
f : ι → M
e : M ≃SL[σ] M₂
⊢ Summable.{u_10, u_5} (α := M₂) (fun (b : ι) ↦ (e : (a : M) → M₂) (f b)) L ↔ Summable f L

Tactic:
⟨fun hf ↦ (e.hasSum.1 hf.hasSum).summable, (e : M →SL[σ] M₂).summable⟩

Premises used: ContinuousLinearMap.summable, ContinuousLinearEquiv.hasSum, HasSum.summable, Summable.hasSum, Iff.intro, Iff.mp, ContinuousLinearEquiv.toContinuousLinearMap
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Module
Goal:
ι : Type u_5
R : Type u_7
R₂ : Type u_8
M : Type u_9
M₂ : Type u_10
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : AddCommMonoid M
inst_3 : Module R M
inst_4 : AddCommMonoid M₂
inst_5 : Module R₂ M₂
inst_6 : TopologicalSpace M
inst_7 : TopologicalSpace M₂
σ : R →+* R₂
σ' : R₂ →+* R
inst_8 : RingHomInvPair σ σ'
inst_9 : RingHomInvPair σ' σ
L : SummationFilter ι
inst_10 : T2Space M
inst_11 : T2Space M₂
f : ι → M
e : M ≃SL[σ] M₂
y : M₂
pos :
  ∀ (hf : Summable f L),
    ∑'[L] (z : ι), (e : (a : M) → M₂) (f z) = y ↔
      Eq.{u_9 + 1} (α := M) (∑'[L] (z : ι), f z : M) ((e.symm : (a : M₂) → M) y : M)
neg :
  ∀ (hf : ¬Summable f L),
    ∑'[L] (z : ι), (e : (a : M) → M₂) (f z) = y ↔
      Eq.{u_9 + 1} (α := M) (∑'[L] (z : ι), f z : M) ((e.symm : (a : M₂) → M) y : M)
⊢ ∑'[L] (z : ι), (e : (a : M) → M₂) (f z) = y ↔
    Eq.{u_9 + 1} (α := M) (∑'[L] (z : ι), f z : M) ((e.symm : (a : M₂) → M) y : M)

Tactic:
by_cases hf : Summable f L

Premises used: Summable
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Module
Goal:
ι : Type u_5
R : Type u_7
R₂ : Type u_8
M : Type u_9
M₂ : Type u_10
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : AddCommMonoid M
inst_3 : Module R M
inst_4 : AddCommMonoid M₂
inst_5 : Module R₂ M₂
inst_6 : TopologicalSpace M
inst_7 : TopologicalSpace M₂
σ : R →+* R₂
σ' : R₂ →+* R
inst_8 : RingHomInvPair σ σ'
inst_9 : RingHomInvPair σ' σ
L : SummationFilter ι
inst_10 : T2Space M
inst_11 : T2Space M₂
f : ι → M
e : M ≃SL[σ] M₂
y : M₂
hf : Summable f L
pos :
  ∀ (hL : L.NeBot),
    ∑'[L] (z : ι), (e : (a : M) → M₂) (f z) = y ↔
      Eq.{u_9 + 1} (α := M) (∑'[L] (z : ι), f z : M) ((e.symm : (a : M₂) → M) y : M)
neg :
  ∀ (hL : ¬L.NeBot),
    ∑'[L] (z : ι), (e : (a : M) → M₂) (f z) = y ↔
      Eq.{u_9 + 1} (α := M) (∑'[L] (z : ι), f z : M) ((e.symm : (a : M₂) → M) y : M)
⊢ ∑'[L] (z : ι), (e : (a : M) → M₂) (f z) = y ↔
    Eq.{u_9 + 1} (α := M) (∑'[L] (z : ι), f z : M) ((e.symm : (a : M₂) → M) y : M)

Tactic:
by_cases hL : L.NeBot

Premises used: SummationFilter.NeBot
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Module
Goal:
ι : Type u_5
R : Type u_7
R₂ : Type u_8
M : Type u_9
M₂ : Type u_10
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : AddCommMonoid M
inst_3 : Module R M
inst_4 : AddCommMonoid M₂
inst_5 : Module R₂ M₂
inst_6 : TopologicalSpace M
inst_7 : TopologicalSpace M₂
σ : R →+* R₂
σ' : R₂ →+* R
inst_8 : RingHomInvPair σ σ'
inst_9 : RingHomInvPair σ' σ
L : SummationFilter ι
inst_10 : T2Space M
inst_11 : T2Space M₂
f : ι → M
e : M ≃SL[σ] M₂
y : M₂
hf : Summable f L
hL : L.NeBot
⊢ ∑'[L] (z : ι), (e : (a : M) → M₂) (f z) = y ↔
    Eq.{u_9 + 1} (α := M) (∑'[L] (z : ι), f z : M) ((e.symm : (a : M₂) → M) y : M)

Tactic:
⟨fun h ↦ (e.hasSum.mp ((e.summable.mpr hf).hasSum_iff.mpr h)).tsum_eq, fun h ↦
        (e.hasSum.mpr (hf.hasSum_iff.mpr h)).tsum_eq⟩

Premises used: Iff.mpr, ContinuousLinearEquiv.hasSum, HasSum.tsum_eq, Summable.hasSum_iff, Iff.intro, Iff.mp, ContinuousLinearEquiv.summable
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Module
Goal:
ι : Type u_5
R : Type u_7
R₂ : Type u_8
M : Type u_9
M₂ : Type u_10
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : AddCommMonoid M
inst_3 : Module R M
inst_4 : AddCommMonoid M₂
inst_5 : Module R₂ M₂
inst_6 : TopologicalSpace M
inst_7 : TopologicalSpace M₂
σ : R →+* R₂
σ' : R₂ →+* R
inst_8 : RingHomInvPair σ σ'
inst_9 : RingHomInvPair σ' σ
L : SummationFilter ι
inst_10 : T2Space M
inst_11 : T2Space M₂
f : ι → M
e : M ≃SL[σ] M₂
y : M₂
hf : Summable f L
hL : L.NeBot
⊢ ∑'[L] (z : ι), (e : (a : M) → M₂) (f z) = y ↔
    Eq.{u_9 + 1} (α := M) (∑'[L] (z : ι), f z : M) ((e.symm : (a : M₂) → M) y : M)

Tactic:
exact ⟨fun h ↦ (e.hasSum.mp ((e.summable.mpr hf).hasSum_iff.mpr h)).tsum_eq, fun h ↦
        (e.hasSum.mpr (hf.hasSum_iff.mpr h)).tsum_eq⟩
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Module
Goal:
ι : Type u_5
R : Type u_7
R₂ : Type u_8
M : Type u_9
M₂ : Type u_10
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : AddCommMonoid M
inst_3 : Module R M
inst_4 : AddCommMonoid M₂
inst_5 : Module R₂ M₂
inst_6 : TopologicalSpace M
inst_7 : TopologicalSpace M₂
σ : R →+* R₂
σ' : R₂ →+* R
inst_8 : RingHomInvPair σ σ'
inst_9 : RingHomInvPair σ' σ
L : SummationFilter ι
inst_10 : T2Space M
inst_11 : T2Space M₂
f : ι → M
e : M ≃SL[σ] M₂
y : M₂
hf : Summable f L
hL : ¬L.NeBot
neg : ∑ᶠ (z : ι), (e : (a : M) → M₂) (f z) = y ↔ (e : (a : M) → M₂) (∑ᶠ (z : ι), f z) = y
⊢ ∑'[L] (z : ι), (e : (a : M) → M₂) (f z) = y ↔
    Eq.{u_9 + 1} (α := M) (∑'[L] (z : ι), f z : M) ((e.symm : (a : M₂) → M) y : M)

Tactic:
simp only [tsum_bot hL, eq_symm_apply]

Premises used: ContinuousLinearEquiv.eq_symm_apply, tsum_bot
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Module
Goal:
ι : Type u_5
R : Type u_7
R₂ : Type u_8
M : Type u_9
M₂ : Type u_10
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : AddCommMonoid M
inst_3 : Module R M
inst_4 : AddCommMonoid M₂
inst_5 : Module R₂ M₂
inst_6 : TopologicalSpace M
inst_7 : TopologicalSpace M₂
σ : R →+* R₂
σ' : R₂ →+* R
inst_8 : RingHomInvPair σ σ'
inst_9 : RingHomInvPair σ' σ
L : SummationFilter ι
inst_10 : T2Space M
inst_11 : T2Space M₂
f : ι → M
e : M ≃SL[σ] M₂
y : M₂
hf : Summable f L
hL : ¬L.NeBot
neg : ∑ᶠ (z : ι), (e : (a : M) → M₂) (f z) = y → (e : (a : M) → M₂) (∑ᶠ (z : ι), f z) = y
neg₁ : (e : (a : M) → M₂) (∑ᶠ (z : ι), f z) = y → ∑ᶠ (z : ι), (e : (a : M) → M₂) (f z) = y
⊢ ∑ᶠ (z : ι), (e : (a : M) → M₂) (f z) = y ↔ (e : (a : M) → M₂) (∑ᶠ (z : ι), f z) = y

Tactic:
constructor
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Module
Goal:
ι : Type u_5
R : Type u_7
R₂ : Type u_8
M : Type u_9
M₂ : Type u_10
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : AddCommMonoid M
inst_3 : Module R M
inst_4 : AddCommMonoid M₂
inst_5 : Module R₂ M₂
inst_6 : TopologicalSpace M
inst_7 : TopologicalSpace M₂
σ : R →+* R₂
σ' : R₂ →+* R
inst_8 : RingHomInvPair σ σ'
inst_9 : RingHomInvPair σ' σ
L : SummationFilter ι
inst_10 : T2Space M
inst_11 : T2Space M₂
f : ι → M
e : M ≃SL[σ] M₂
hf : Summable f L
hL : ¬L.NeBot
⊢ Eq.{u_10 + 1} (α := M₂) ((e : (a : M) → M₂) (∑ᶠ (z : ι), f z) : M₂) (∑ᶠ (z : ι), (e : (a : M) → M₂) (f z) : M₂)

Tactic:
e.map_finsum f

Premises used: ContinuousLinearEquiv.toLinearEquiv, LinearEquiv.toAddEquiv, AddEquiv.map_finsum
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Module
Goal:
ι : Type u_5
R : Type u_7
R₂ : Type u_8
M : Type u_9
M₂ : Type u_10
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : AddCommMonoid M
inst_3 : Module R M
inst_4 : AddCommMonoid M₂
inst_5 : Module R₂ M₂
inst_6 : TopologicalSpace M
inst_7 : TopologicalSpace M₂
σ : R →+* R₂
σ' : R₂ →+* R
inst_8 : RingHomInvPair σ σ'
inst_9 : RingHomInvPair σ' σ
L : SummationFilter ι
inst_10 : T2Space M
inst_11 : T2Space M₂
f : ι → M
e : M ≃SL[σ] M₂
hf : Summable f L
hL : ¬L.NeBot
⊢ Eq.{u_10 + 1} (α := M₂) (∑ᶠ (z : ι), (e : (a : M) → M₂) (f z) : M₂) ((e : (a : M) → M₂) (∑ᶠ (z : ι), f z) : M₂)

Tactic:
(e.map_finsum f).symm

Premises used: ContinuousLinearEquiv.toLinearEquiv, LinearEquiv.toAddEquiv, AddEquiv.map_finsum, Eq.symm
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Module
Goal:
ι : Type u_5
R : Type u_7
R₂ : Type u_8
M : Type u_9
M₂ : Type u_10
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : AddCommMonoid M
inst_3 : Module R M
inst_4 : AddCommMonoid M₂
inst_5 : Module R₂ M₂
inst_6 : TopologicalSpace M
inst_7 : TopologicalSpace M₂
σ : R →+* R₂
σ' : R₂ →+* R
inst_8 : RingHomInvPair σ σ'
inst_9 : RingHomInvPair σ' σ
L : SummationFilter ι
inst_10 : T2Space M
inst_11 : T2Space M₂
f : ι → M
e : M ≃SL[σ] M₂
hf : Summable f L
hL : ¬L.NeBot
⊢ Eq.{u_10 + 1} (α := M₂) ((e : (a : M) → M₂) (∑ᶠ (z : ι), f z) : M₂) (∑ᶠ (z : ι), (e : (a : M) → M₂) (f z) : M₂)

Tactic:
exacts [e.map_finsum f, (e.map_finsum f).symm]

Premises used: ContinuousLinearEquiv.toLinearEquiv, LinearEquiv.toAddEquiv, AddEquiv.map_finsum, Eq.symm
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Module
Goal:
ι : Type u_5
R : Type u_7
R₂ : Type u_8
M : Type u_9
M₂ : Type u_10
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : AddCommMonoid M
inst_3 : Module R M
inst_4 : AddCommMonoid M₂
inst_5 : Module R₂ M₂
inst_6 : TopologicalSpace M
inst_7 : TopologicalSpace M₂
σ : R →+* R₂
σ' : R₂ →+* R
inst_8 : RingHomInvPair σ σ'
inst_9 : RingHomInvPair σ' σ
L : SummationFilter ι
inst_10 : T2Space M
inst_11 : T2Space M₂
f : ι → M
e : M ≃SL[σ] M₂
y : M₂
hf : ¬Summable f L
⊢ ¬Summable.{u_10, u_5} (α := M₂) (fun (z : ι) ↦ (e : (a : M) → M₂) (f z)) L

Tactic:
have hf' : ¬Summable (fun z ↦ e (f z)) L := fun h ↦ hf (e.summable.mp h)
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Module
Goal:
ι : Type u_5
R : Type u_7
R₂ : Type u_8
M : Type u_9
M₂ : Type u_10
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : AddCommMonoid M
inst_3 : Module R M
inst_4 : AddCommMonoid M₂
inst_5 : Module R₂ M₂
inst_6 : TopologicalSpace M
inst_7 : TopologicalSpace M₂
σ : R →+* R₂
σ' : R₂ →+* R
inst_8 : RingHomInvPair σ σ'
inst_9 : RingHomInvPair σ' σ
L : SummationFilter ι
inst_10 : T2Space M
inst_11 : T2Space M₂
f : ι → M
e : M ≃SL[σ] M₂
y : M₂
hf : ¬Summable f L
hf' : ¬Summable.{u_10, u_5} (α := M₂) (fun (z : ι) ↦ (e : (a : M) → M₂) (f z)) L
neg : 0 = y ↔ Eq.{u_9 + 1} (α := M) (0 : M) ((e.symm : (a : M₂) → M) y : M)
⊢ ∑'[L] (z : ι), (e : (a : M) → M₂) (f z) = y ↔
    Eq.{u_9 + 1} (α := M) (∑'[L] (z : ι), f z : M) ((e.symm : (a : M₂) → M) y : M)

Tactic:
rw [tsum_eq_zero_of_not_summable hf, tsum_eq_zero_of_not_summable hf']

Premises used: tsum_eq_zero_of_not_summable
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Module
Goal:
ι : Type u_5
R : Type u_7
R₂ : Type u_8
M : Type u_9
M₂ : Type u_10
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : AddCommMonoid M
inst_3 : Module R M
inst_4 : AddCommMonoid M₂
inst_5 : Module R₂ M₂
inst_6 : TopologicalSpace M
inst_7 : TopologicalSpace M₂
σ : R →+* R₂
σ' : R₂ →+* R
inst_8 : RingHomInvPair σ σ'
inst_9 : RingHomInvPair σ' σ
L : SummationFilter ι
inst_10 : T2Space M
inst_11 : T2Space M₂
f : ι → M
e : M ≃SL[σ] M₂
y : M₂
hf : ¬Summable f L
hf' : ¬Summable.{u_10, u_5} (α := M₂) (fun (z : ι) ↦ (e : (a : M) → M₂) (f z)) L
⊢ 0 = y ↔ Eq.{u_9 + 1} (α := M) (0 : M) ((e.symm : (a : M₂) → M) y : M)

Tactic:
⟨?_, fun H ↦ ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Module
Goal:
ι : Type u_5
R : Type u_7
R₂ : Type u_8
M : Type u_9
M₂ : Type u_10
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : AddCommMonoid M
inst_3 : Module R M
inst_4 : AddCommMonoid M₂
inst_5 : Module R₂ M₂
inst_6 : TopologicalSpace M
inst_7 : TopologicalSpace M₂
σ : R →+* R₂
σ' : R₂ →+* R
inst_8 : RingHomInvPair σ σ'
inst_9 : RingHomInvPair σ' σ
L : SummationFilter ι
inst_10 : T2Space M
inst_11 : T2Space M₂
f : ι → M
e : M ≃SL[σ] M₂
y : M₂
hf : ¬Summable f L
hf' : ¬Summable.{u_10, u_5} (α := M₂) (fun (z : ι) ↦ (e : (a : M) → M₂) (f z)) L
neg : 0 = y → Eq.{u_9 + 1} (α := M) (0 : M) ((e.symm : (a : M₂) → M) y : M)
neg₁ : ∀ (H : Eq.{u_9 + 1} (α := M) (0 : M) ((e.symm : (a : M₂) → M) y : M)), 0 = y
⊢ 0 = y ↔ Eq.{u_9 + 1} (α := M) (0 : M) ((e.symm : (a : M₂) → M) y : M)

Tactic:
refine ⟨?_, fun H ↦ ?_⟩
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Module
Goal:
ι : Type u_5
R : Type u_7
R₂ : Type u_8
M : Type u_9
M₂ : Type u_10
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : AddCommMonoid M
inst_3 : Module R M
inst_4 : AddCommMonoid M₂
inst_5 : Module R₂ M₂
inst_6 : TopologicalSpace M
inst_7 : TopologicalSpace M₂
σ : R →+* R₂
σ' : R₂ →+* R
inst_8 : RingHomInvPair σ σ'
inst_9 : RingHomInvPair σ' σ
L : SummationFilter ι
inst_10 : T2Space M
inst_11 : T2Space M₂
f : ι → M
e : M ≃SL[σ] M₂
hf : ¬Summable f L
hf' : ¬Summable.{u_10, u_5} (α := M₂) (fun (z : ι) ↦ (e : (a : M) → M₂) (f z)) L
⊢ Eq.{u_9 + 1} (α := M) (0 : M) ((e.symm : (a : M₂) → M) 0 : M)

Tactic:
simp
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Module
Goal:
ι : Type u_5
R : Type u_7
R₂ : Type u_8
M : Type u_9
M₂ : Type u_10
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : AddCommMonoid M
inst_3 : Module R M
inst_4 : AddCommMonoid M₂
inst_5 : Module R₂ M₂
inst_6 : TopologicalSpace M
inst_7 : TopologicalSpace M₂
σ : R →+* R₂
σ' : R₂ →+* R
inst_8 : RingHomInvPair σ σ'
inst_9 : RingHomInvPair σ' σ
L : SummationFilter ι
inst_10 : T2Space M
inst_11 : T2Space M₂
f : ι → M
e : M ≃SL[σ] M₂
y : M₂
hf : ¬Summable f L
hf' : ¬Summable.{u_10, u_5} (α := M₂) (fun (z : ι) ↦ (e : (a : M) → M₂) (f z)) L
H : Eq.{u_9 + 1} (α := M) (0 : M) ((e.symm : (a : M₂) → M) y : M)
⊢ 0 = y

Tactic:
simpa using congr_arg (fun z ↦ e z) H

Premises used: congr_arg, DFunLike.coe
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Module
Goal:
ι : Type u_5
R : Type u_7
R₂ : Type u_8
M : Type u_9
M₂ : Type u_10
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : AddCommMonoid M
inst_3 : Module R M
inst_4 : AddCommMonoid M₂
inst_5 : Module R₂ M₂
inst_6 : TopologicalSpace M
inst_7 : TopologicalSpace M₂
σ : R →+* R₂
σ' : R₂ →+* R
inst_8 : RingHomInvPair σ σ'
inst_9 : RingHomInvPair σ' σ
L : SummationFilter ι
inst_10 : T2Space M
inst_11 : T2Space M₂
f : ι → M
e : M ≃SL[σ] M₂
⊢ Eq.{u_10 + 1} (α := M₂) ((e : (a : M) → M₂) (∑'[L] (z : ι), f z) : M₂) (∑'[L] (z : ι), (e : (a : M) → M₂) (f z) : M₂)

Tactic:
symm (e.tsum_eq_iff.mpr ?_)

Premises used: Iff.mpr, ContinuousLinearEquiv.tsum_eq_iff, symm
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Module
Goal:
ι : Type u_5
R : Type u_7
R₂ : Type u_8
M : Type u_9
M₂ : Type u_10
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : AddCommMonoid M
inst_3 : Module R M
inst_4 : AddCommMonoid M₂
inst_5 : Module R₂ M₂
inst_6 : TopologicalSpace M
inst_7 : TopologicalSpace M₂
σ : R →+* R₂
σ' : R₂ →+* R
inst_8 : RingHomInvPair σ σ'
inst_9 : RingHomInvPair σ' σ
L : SummationFilter ι
inst_10 : T2Space M
inst_11 : T2Space M₂
f : ι → M
e : M ≃SL[σ] M₂
refine :
  Eq.{u_9 + 1} (α := M) (∑'[L] (z : ι), f z : M)
    ((e.symm : (a : M₂) → M) ((e : (a : M) → M₂) (∑'[L] (z : ι), f z) : M₂) : M)
⊢ Eq.{u_10 + 1} (α := M₂) ((e : (a : M) → M₂) (∑'[L] (z : ι), f z) : M₂) (∑'[L] (z : ι), (e : (a : M) → M₂) (f z) : M₂)

Tactic:
refine symm (e.tsum_eq_iff.mpr ?_)

Premises used: Iff.mpr, ContinuousLinearEquiv.tsum_eq_iff, symm
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Module
Goal:
ι : Type u_5
R : Type u_7
R₂ : Type u_8
M : Type u_9
M₂ : Type u_10
inst : Semiring R
inst_1 : Semiring R₂
inst_2 : AddCommMonoid M
inst_3 : Module R M
inst_4 : AddCommMonoid M₂
inst_5 : Module R₂ M₂
inst_6 : TopologicalSpace M
inst_7 : TopologicalSpace M₂
σ : R →+* R₂
σ' : R₂ →+* R
inst_8 : RingHomInvPair σ σ'
inst_9 : RingHomInvPair σ' σ
L : SummationFilter ι
inst_10 : T2Space M
inst_11 : T2Space M₂
f : ι → M
e : M ≃SL[σ] M₂
rw rw₁ : Eq.{u_9 + 1} (α := M) (∑'[L] (z : ι), f z) (∑'[L] (z : ι), f z)
⊢ Eq.{u_9 + 1} (α := M) (∑'[L] (z : ι), f z : M)
    ((e.symm : (a : M₂) → M) ((e : (a : M) → M₂) (∑'[L] (z : ι), f z) : M₂) : M)

Tactic:
rw [e.symm_apply_apply _]

Premises used: ContinuousLinearEquiv.symm_apply_apply
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Module
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Type u_5
κ : Type u_6
R_1 : Type u_7
R₂ : Type u_8
M_1 : Type u_9
M₂ : Type u_10
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
refine :
  ∀ (a b : β),
    a ≈ b →
      Eq.{u_11 + 1} (α := M) ((fun (b : β) ↦ (∑' (a : α), f (a • b) : M)) a)
        ((fun (b : β) ↦ (∑' (a : α), f (a • b) : M)) b)
⊢ Quotient (orbitRel α β) → M

Tactic:
refine @Quotient.lift _ _ (_) (fun b ↦ ∑' (a : α), f (a • b)) ?_

Premises used: tsum, HSMul.hSMul, Quotient.lift, SummationFilter.unconditional
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Module
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Type u_5
κ : Type u_6
R_1 : Type u_7
R₂ : Type u_8
M_1 : Type u_9
M₂ : Type u_10
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
b₁ b₂ : β
a :
  ∀ (a : α) (ha : a • b₂ = b₁),
    Eq.{u_11 + 1} (α := M) ((fun (b : β) ↦ (∑' (a : α), f (a • b) : M)) b₁)
      ((fun (b : β) ↦ (∑' (a : α), f (a • b) : M)) b₂)
⊢ b₁ ≈ b₂ →
    Eq.{u_11 + 1} (α := M) ((fun (b : β) ↦ (∑' (a : α), f (a • b) : M)) b₁)
      ((fun (b : β) ↦ (∑' (a : α), f (a • b) : M)) b₂)

Tactic:
⟨a, (ha : a • b₂ = b₁)⟩
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Module
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Type u_5
κ : Type u_6
R_1 : Type u_7
R₂ : Type u_8
M_1 : Type u_9
M₂ : Type u_10
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
b₁ b₂ : β
a : α
ha : a • b₂ = b₁
rw : Eq.{u_11 + 1} (α := M) (∑' (a_1 : α), f (a_1 • a • b₂)) (∑' (a : α), f (a • b₂))
⊢ Eq.{u_11 + 1} (α := M) (∑' (a : α), f (a • b₁)) (∑' (a : α), f (a • b₂))

Tactic:
rw [← ha]
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Module
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Type u_5
κ : Type u_6
R_1 : Type u_7
R₂ : Type u_8
M_1 : Type u_9
M₂ : Type u_10
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
b₁ b₂ : β
a : α
ha : a • b₂ = b₁
⊢ Eq.{u_11 + 1} (α := M) (∑' (c : α), f (HSMul.hSMul (α := α) ((Equiv.mulRight a : (a : α) → α) c : α) b₂))
    (∑' (b : α), f (b • b₂))

Tactic:
(Equiv.mulRight a).tsum_eq (fun a' ↦ f (a' • b₂))

Premises used: Equiv.tsum_eq, Equiv.mulRight, HSMul.hSMul
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Module
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Type u_5
κ : Type u_6
R_1 : Type u_7
R₂ : Type u_8
M_1 : Type u_9
M₂ : Type u_10
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
b₁ b₂ : β
a : α
ha : a • b₂ = b₁
h :
  Eq.{u_11 + 1} (α := M) (∑' (a_1 : α), f (a_1 • a • b₂))
    (∑' (c : α), f (HSMul.hSMul (α := α) ((Equiv.mulRight a : (a : α) → α) c : α) b₂))
⊢ Eq.{u_11 + 1} (α := M) (∑' (a_1 : α), f (a_1 • a • b₂)) (∑' (a : α), f (a • b₂))

Tactic:
convert! (Equiv.mulRight a).tsum_eq (fun a' ↦ f (a' • b₂)) using 1

Premises used: Equiv.tsum_eq, Equiv.mulRight, HSMul.hSMul
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Module
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Type u_5
κ : Type u_6
R_1 : Type u_7
R₂ : Type u_8
M_1 : Type u_9
M₂ : Type u_10
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
b₁ b₂ : β
a : α
ha : a • b₂ = b₁
h : Eq.{u_11 + 1} (α := M) (∑' (a_1 : α), f (a_1 • a • b₂)) (∑' (c : α), f ((c * a) • b₂))
⊢ Eq.{u_11 + 1} (α := M) (∑' (a_1 : α), f (a_1 • a • b₂))
    (∑' (c : α), f (HSMul.hSMul (α := α) ((Equiv.mulRight a : (a : α) → α) c : α) b₂))

Tactic:
simp only [Equiv.coe_mulRight]

Premises used: Equiv.coe_mulRight
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Module
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Type u_5
κ : Type u_6
R_1 : Type u_7
R₂ : Type u_8
M_1 : Type u_9
M₂ : Type u_10
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
b₁ b₂ : β
a : α
ha : a • b₂ = b₁
h : Eq (α := α → M) (fun (a_1 : α) ↦ f (a_1 • a • b₂)) fun (c : α) ↦ f ((c * a) • b₂)
⊢ Eq.{u_11 + 1} (α := M) (∑' (a_1 : α), f (a_1 • a • b₂)) (∑' (c : α), f ((c * a) • b₂))

Tactic:
congr
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Module
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Type u_5
κ : Type u_6
R_1 : Type u_7
R₂ : Type u_8
M_1 : Type u_9
M₂ : Type u_10
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
b₁ b₂ : β
a : α
ha : a • b₂ = b₁
h : ∀ (x : α), f (x • a • b₂) = f ((x * a) • b₂)
⊢ Eq (α := α → M) (fun (a_1 : α) ↦ f (a_1 • a • b₂)) fun (c : α) ↦ f ((c * a) • b₂)

Tactic:
ext
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Module
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Type u_5
κ : Type u_6
R_1 : Type u_7
R₂ : Type u_8
M_1 : Type u_9
M₂ : Type u_10
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
b₁ b₂ : β
a : α
ha : a • b₂ = b₁
x : α
h : x • a • b₂ = (x * a) • b₂
⊢ f (x • a • b₂) = f ((x * a) • b₂)

Tactic:
congr 1
-- Module: Mathlib.Topology.Algebra.InfiniteSum.Module
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Type u_5
κ : Type u_6
R_1 : Type u_7
R₂ : Type u_8
M_1 : Type u_9
M₂ : Type u_10
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
b₁ b₂ : β
a : α
ha : a • b₂ = b₁
x : α
⊢ x • a • b₂ = (x * a) • b₂

Tactic:
simp only [mul_smul]

Premises used: SemigroupAction.mul_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
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 : Group α
inst_7 : MulAction α β
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