-- Mathlib/Topology/Algebra/InfiniteSum/Module.lean
/-- Automorphization of a function into an `R`-`Module` distributes, that is, commutes with the
`R`-scalar multiplication. -/
lemma AddAction.automorphize_smul_left [AddGroup α] [AddAction α β]  (f : β → M)
    (g : Quotient (AddAction.orbitRel α β) → R) :
    AddAction.automorphize ((g ∘ (@Quotient.mk' _ (_))) • f)
      = g • (AddAction.automorphize f : Quotient (AddAction.orbitRel α β) → M)

Proof state:
α : Type u_1
β : Type u_2
M : Type u_11
inst✝⁷ : TopologicalSpace M
inst✝⁶ : AddCommMonoid M
inst✝⁵ : T2Space M
R : Type u_12
inst✝⁴ : DivisionRing R
inst✝³ : Module R M
inst✝² : ContinuousConstSMul R M
inst✝¹ : AddGroup α
inst✝ : AddAction α β
f : β → M
g : Quotient (orbitRel α β) → R
x : Quotient (orbitRel α β)
b : β
π : β → Quotient (orbitRel α β) := Quotient.mk (orbitRel α β)
a : α
⊢ (orbitRel α β) (a +ᵥ b) b

Tactic:
use a

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
M : Type u_11
inst✝⁷ : TopologicalSpace M
inst✝⁶ : AddCommMonoid M
inst✝⁵ : T2Space M
R : Type u_12
inst✝⁴ : DivisionRing R
inst✝³ : Module R M
inst✝² : ContinuousConstSMul R M
inst✝¹ : AddGroup α
inst✝ : AddAction α β
f : β → M
g : Quotient (orbitRel α β) → R
x : Quotient (orbitRel α β)
b : β
π : β → Quotient (orbitRel α β) := Quotient.mk (orbitRel α β)
a : α
⊢ π (a +ᵥ b) = π b

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

Result:
α : Type u_1
β : Type u_2
M : Type u_11
inst✝⁷ : TopologicalSpace M
inst✝⁶ : AddCommMonoid M
inst✝⁵ : T2Space M
R : Type u_12
inst✝⁴ : DivisionRing R
inst✝³ : Module R M
inst✝² : ContinuousConstSMul R M
inst✝¹ : AddGroup α
inst✝ : AddAction α β
f : β → M
g : Quotient (orbitRel α β) → R
x : Quotient (orbitRel α β)
b : β
π : β → Quotient (orbitRel α β) := Quotient.mk (orbitRel α β)
a : α
⊢ (orbitRel α β) (a +ᵥ b) b

Proof state:
α : Type u_1
β : Type u_2
M : Type u_11
inst✝⁷ : TopologicalSpace M
inst✝⁶ : AddCommMonoid M
inst✝⁵ : T2Space M
R : Type u_12
inst✝⁴ : DivisionRing R
inst✝³ : Module R M
inst✝² : ContinuousConstSMul R M
inst✝¹ : AddGroup α
inst✝ : AddAction α β
f : β → M
g : Quotient (orbitRel α β) → R
x : Quotient (orbitRel α β)
b : β
⊢ automorphize (g ∘ Quotient.mk' • f) (Quotient.mk'' b) = (g • automorphize f) (Quotient.mk'' b)

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

Result:
α : Type u_1
β : Type u_2
M : Type u_11
inst✝⁷ : TopologicalSpace M
inst✝⁶ : AddCommMonoid M
inst✝⁵ : T2Space M
R : Type u_12
inst✝⁴ : DivisionRing R
inst✝³ : Module R M
inst✝² : ContinuousConstSMul R M
inst✝¹ : AddGroup α
inst✝ : AddAction α β
f : β → M
g : Quotient (orbitRel α β) → R
x : Quotient (orbitRel α β)
b : β
⊢ Quotient.lift (fun b => ∑' (a : α), g (Quotient.mk' (a +ᵥ b)) • f (a +ᵥ b)) ⋯ (Quotient.mk'' b) =
    g (Quotient.mk'' b) • Quotient.lift (fun b => ∑' (a : α), f (a +ᵥ b)) ⋯ (Quotient.mk'' b)

Proof state:
α : Type u_1
β : Type u_2
M : Type u_11
inst✝⁷ : TopologicalSpace M
inst✝⁶ : AddCommMonoid M
inst✝⁵ : T2Space M
R : Type u_12
inst✝⁴ : DivisionRing R
inst✝³ : Module R M
inst✝² : ContinuousConstSMul R M
inst✝¹ : AddGroup α
inst✝ : AddAction α β
f : β → M
g : Quotient (orbitRel α β) → R
x : Quotient (orbitRel α β)
b : β
π : β → Quotient (orbitRel α β) := Quotient.mk (orbitRel α β)
⊢ Quotient.lift (fun b => ∑' (a : α), g (Quotient.mk' (a +ᵥ b)) • f (a +ᵥ b)) ⋯ (Quotient.mk'' b) =
    g (Quotient.mk'' b) • Quotient.lift (fun b => ∑' (a : α), f (a +ᵥ b)) ⋯ (Quotient.mk'' b)

Tactic:
have H₁ : ∀ a : α, π (a +ᵥ b) = π b := by
  intro a
  apply (@Quotient.eq _ (AddAction.orbitRel α β) (a +ᵥ b) b).mpr
  use a

Result:
α : Type u_1
β : Type u_2
M : Type u_11
inst✝⁷ : TopologicalSpace M
inst✝⁶ : AddCommMonoid M
inst✝⁵ : T2Space M
R : Type u_12
inst✝⁴ : DivisionRing R
inst✝³ : Module R M
inst✝² : ContinuousConstSMul R M
inst✝¹ : AddGroup α
inst✝ : AddAction α β
f : β → M
g : Quotient (orbitRel α β) → R
x : Quotient (orbitRel α β)
b : β
π : β → Quotient (orbitRel α β) := Quotient.mk (orbitRel α β)
H₁ : ∀ (a : α), π (a +ᵥ b) = π b
⊢ Quotient.lift (fun b => ∑' (a : α), g (Quotient.mk' (a +ᵥ b)) • f (a +ᵥ b)) ⋯ (Quotient.mk'' b) =
    g (Quotient.mk'' b) • Quotient.lift (fun b => ∑' (a : α), f (a +ᵥ b)) ⋯ (Quotient.mk'' b)

Proof state:
α : Type u_1
β : Type u_2
M : Type u_11
inst✝⁷ : TopologicalSpace M
inst✝⁶ : AddCommMonoid M
inst✝⁵ : T2Space M
R : Type u_12
inst✝⁴ : DivisionRing R
inst✝³ : Module R M
inst✝² : ContinuousConstSMul R M
inst✝¹ : AddGroup α
inst✝ : AddAction α β
f : β → M
g : Quotient (orbitRel α β) → R
x : Quotient (orbitRel α β)
b : β
π : β → Quotient (orbitRel α β) := Quotient.mk (orbitRel α β)
H₁ : ∀ (a : α), π (a +ᵥ b) = π b
⊢ ∑' (a : α), g (π b) • f (a +ᵥ b) = g (π b) • ∑' (a : α), f (a +ᵥ b)

Tactic:
exact tsum_const_smul'' _

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
M : Type u_11
inst✝⁷ : TopologicalSpace M
inst✝⁶ : AddCommMonoid M
inst✝⁵ : T2Space M
R : Type u_12
inst✝⁴ : DivisionRing R
inst✝³ : Module R M
inst✝² : ContinuousConstSMul R M
inst✝¹ : AddGroup α
inst✝ : AddAction α β
f : β → M
g : Quotient (orbitRel α β) → R
x : Quotient (orbitRel α β)
b : β
π : β → Quotient (orbitRel α β) := Quotient.mk (orbitRel α β)
⊢ ∀ (a : α), π (a +ᵥ b) = π b

Tactic:
intro a

Result:
α : Type u_1
β : Type u_2
M : Type u_11
inst✝⁷ : TopologicalSpace M
inst✝⁶ : AddCommMonoid M
inst✝⁵ : T2Space M
R : Type u_12
inst✝⁴ : DivisionRing R
inst✝³ : Module R M
inst✝² : ContinuousConstSMul R M
inst✝¹ : AddGroup α
inst✝ : AddAction α β
f : β → M
g : Quotient (orbitRel α β) → R
x : Quotient (orbitRel α β)
b : β
π : β → Quotient (orbitRel α β) := Quotient.mk (orbitRel α β)
a : α
⊢ π (a +ᵥ b) = π b

Proof state:
α : Type u_1
β : Type u_2
M : Type u_11
inst✝⁷ : TopologicalSpace M
inst✝⁶ : AddCommMonoid M
inst✝⁵ : T2Space M
R : Type u_12
inst✝⁴ : DivisionRing R
inst✝³ : Module R M
inst✝² : ContinuousConstSMul R M
inst✝¹ : AddGroup α
inst✝ : AddAction α β
f : β → M
g : Quotient (orbitRel α β) → R
x : Quotient (orbitRel α β)
b : β
π : β → Quotient (orbitRel α β) := Quotient.mk (orbitRel α β)
H₁ : ∀ (a : α), π (a +ᵥ b) = π b
⊢ Quotient.lift (fun b => ∑' (a : α), g (Quotient.mk' (a +ᵥ b)) • f (a +ᵥ b)) ⋯ (Quotient.mk'' b) =
    g (Quotient.mk'' b) • Quotient.lift (fun b => ∑' (a : α), f (a +ᵥ b)) ⋯ (Quotient.mk'' b)

Tactic:
change ∑' a : α, g (π (a +ᵥ b)) • f (a +ᵥ b) = g (π b) • ∑' a : α, f (a +ᵥ b)

Result:
α : Type u_1
β : Type u_2
M : Type u_11
inst✝⁷ : TopologicalSpace M
inst✝⁶ : AddCommMonoid M
inst✝⁵ : T2Space M
R : Type u_12
inst✝⁴ : DivisionRing R
inst✝³ : Module R M
inst✝² : ContinuousConstSMul R M
inst✝¹ : AddGroup α
inst✝ : AddAction α β
f : β → M
g : Quotient (orbitRel α β) → R
x : Quotient (orbitRel α β)
b : β
π : β → Quotient (orbitRel α β) := Quotient.mk (orbitRel α β)
H₁ : ∀ (a : α), π (a +ᵥ b) = π b
⊢ ∑' (a : α), g (π (a +ᵥ b)) • f (a +ᵥ b) = g (π b) • ∑' (a : α), f (a +ᵥ b)

Proof state:
α : Type u_1
β : Type u_2
M : Type u_11
inst✝⁷ : TopologicalSpace M
inst✝⁶ : AddCommMonoid M
inst✝⁵ : T2Space M
R : Type u_12
inst✝⁴ : DivisionRing R
inst✝³ : Module R M
inst✝² : ContinuousConstSMul R M
inst✝¹ : AddGroup α
inst✝ : AddAction α β
f : β → M
g : Quotient (orbitRel α β) → R
x : Quotient (orbitRel α β)
b : β
π : β → Quotient (orbitRel α β) := Quotient.mk (orbitRel α β)
H₁ : ∀ (a : α), π (a +ᵥ b) = π b
⊢ ∑' (a : α), g (π (a +ᵥ b)) • f (a +ᵥ b) = g (π b) • ∑' (a : α), f (a +ᵥ b)

Tactic:
simp_rw [H₁]

Result:
α : Type u_1
β : Type u_2
M : Type u_11
inst✝⁷ : TopologicalSpace M
inst✝⁶ : AddCommMonoid M
inst✝⁵ : T2Space M
R : Type u_12
inst✝⁴ : DivisionRing R
inst✝³ : Module R M
inst✝² : ContinuousConstSMul R M
inst✝¹ : AddGroup α
inst✝ : AddAction α β
f : β → M
g : Quotient (orbitRel α β) → R
x : Quotient (orbitRel α β)
b : β
π : β → Quotient (orbitRel α β) := Quotient.mk (orbitRel α β)
H₁ : ∀ (a : α), π (a +ᵥ b) = π b
⊢ ∑' (a : α), g (π b) • f (a +ᵥ b) = g (π b) • ∑' (a : α), f (a +ᵥ b)