awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Module (goal)
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)
⊢ 0 = y ↔ Eq.{u_9 + 1} (α := M) (0 : M) ((e.symm : (a : M₂) → M) y : M)
have neg₁ : ∀ (H : Eq.{u_9 + 1} (α := M) (0 : M) ((e.symm : (a : M₂) → M) y : M)), 0 = y
Tactic: refine ⟨?_, fun H ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Module (goal)
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₂)
have 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)
Tactic: refine symm (e.tsum_eq_iff.mpr ?_)
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Module (goal)
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_9 + 1} (α := M) (∑'[L] (z : ι), f z : M)
    ((e.symm : (a : M₂) → M) ((e : (a : M) → M₂) (∑'[L] (z : ι), f z) : M₂) : M)
have rw : Eq.{u_9 + 1} (α := M) (∑'[L] (z : ι), f z) (∑'[L] (z : ι), f z)
Tactic: rw [e.symm_apply_apply _]
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Module (goal)
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
⊢ Quotient (orbitRel α β) → M
have 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)
Tactic: refine @Quotient.lift _ _ (_) (fun b ↦ ∑' (a : α), f (a • b)) ?_
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Module (goal)
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₂ : β
⊢ b₁ ≈ b₂ →
    Eq.{u_11 + 1} (α := M) ((fun (b : β) ↦ (∑' (a : α), f (a • b) : M)) b₁)
      ((fun (b : β) ↦ (∑' (a : α), f (a • b) : M)) b₂)
have 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₂)
Tactic: ⟨a, (ha : a • b₂ = b₁)⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Module (goal)
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) (∑' (a : α), f (a • b₁)) (∑' (a : α), f (a • b₂))
have rw : Eq.{u_11 + 1} (α := M) (∑' (a_1 : α), f (a_1 • a • b₂)) (∑' (a : α), f (a • b₂))
Tactic: rw [← ha]
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Module (goal)
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) (∑' (a_1 : α), f (a_1 • a • b₂)) (∑' (a : α), f (a • b₂))
have h : Eq.{u_11 + 1} (α := M) (∑' (a_1 : α), f (a_1 • a • b₂))
  (∑' (c : α), f (HSMul.hSMul (α := α) ((Equiv.mulRight a : (a : α) → α) c : α) b₂))
Tactic: convert! (Equiv.mulRight a).tsum_eq (fun a' ↦ f (a' • b₂)) using 1
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Module (goal)
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) (∑' (a_1 : α), f (a_1 • a • b₂))
    (∑' (c : α), f (HSMul.hSMul (α := α) ((Equiv.mulRight a : (a : α) → α) c : α) b₂))
have h : Eq.{u_11 + 1} (α := M) (∑' (a_1 : α), f (a_1 • a • b₂)) (∑' (c : α), f ((c * a) • b₂))
Tactic: simp only [Equiv.coe_mulRight]
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Module (goal)
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) (∑' (a_1 : α), f (a_1 • a • b₂)) (∑' (c : α), f ((c * a) • b₂))
have h : Eq (α := α → M) (fun (a_1 : α) ↦ f (a_1 • a • b₂)) fun (c : α) ↦ f ((c * a) • b₂)
Tactic: congr
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Module (goal)
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 (α := α → M) (fun (a_1 : α) ↦ f (a_1 • a • b₂)) fun (c : α) ↦ f ((c * a) • b₂)
have h : ∀ (x : α), f (x • a • b₂) = f ((x * a) • b₂)
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Module (goal)
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 : α
⊢ f (x • a • b₂) = f ((x * a) • b₂)
have h : x • a • b₂ = (x * a) • b₂
Tactic: congr 1
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Module (goal)
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
⊢ automorphize (g ∘ Quotient.mk' • f) = HSMul.hSMul (β := Quotient (orbitRel α β) → M) g (automorphize f)
have h : ∀ (x : Quotient (orbitRel α β)),
  automorphize (g ∘ Quotient.mk' • f) x = HSMul.hSMul (β := Quotient (orbitRel α β) → M) g (automorphize f) x
Tactic: ext x
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Module (goal)
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 α β)
⊢ automorphize (g ∘ Quotient.mk' • f) x = HSMul.hSMul (β := Quotient (orbitRel α β) → M) g (automorphize f) x
have h : ∀ (b : β),
  automorphize (g ∘ Quotient.mk' • f) ⟦b⟧ = HSMul.hSMul (β := Quotient (orbitRel α β) → M) g (automorphize f) ⟦b⟧
Tactic: induction x using Quotient.inductionOn with | _ b
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Module (goal)
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 : β
⊢ automorphize (g ∘ Quotient.mk' • f) ⟦b⟧ = HSMul.hSMul (β := Quotient (orbitRel α β) → M) g (automorphize f) ⟦b⟧
have h : Quotient.lift (fun (b : β) ↦ ∑' (a : α), g (Quotient.mk' (a • b)) • f (a • b)) sorry ⟦b⟧ =
  g ⟦b⟧ • Quotient.lift (fun (b : β) ↦ ∑' (a : α), f (a • b)) sorry ⟦b⟧
Tactic: simp only [automorphize, Pi.smul_apply', comp_apply]
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Module (goal)
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
have apply : (orbitRel α β : β → β → Prop) (a • b) b
Tactic: apply (@Quotient.eq _ (MulAction.orbitRel α β) (a • b) b).mpr
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Module (goal)
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 : α
⊢ (orbitRel α β : β → β → Prop) (a • b) b
have h : (fun (m : α) ↦ m • b) a = a • b
Tactic: use a
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Module (hypothesis)
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 α β)
⊢ 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)
have H₁ : ∀ (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
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Module (goal)
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
⊢ 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)
have h : ∑' (a : α), g (π (a • b)) • f (a • b) = HSMul.hSMul (β := M) (g (π b)) (∑' (a : α), f (a • b))
Tactic: change ∑' a : α, g (π (a • b)) • f (a • b) = g (π b) • ∑' a : α, f (a • b)
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Module (goal)
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 (π (a • b)) • f (a • b) = HSMul.hSMul (β := M) (g (π b)) (∑' (a : α), f (a • b))
have h : ∑' (a : α), g (π b) • f (a • b) = HSMul.hSMul (β := M) (g (π b)) (∑' (a : α), f (a • b))
Tactic: simp_rw [H₁]
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Module (goal)
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
⊢ automorphize (g ∘ Quotient.mk' • f) = HSMul.hSMul (β := Quotient (orbitRel α β) → M) g (automorphize f)
have h : ∀ (x : Quotient (orbitRel α β)),
  automorphize (g ∘ Quotient.mk' • f) x = HSMul.hSMul (β := Quotient (orbitRel α β) → M) g (automorphize f) x
Tactic: ext x
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Module (goal)
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 α β)
⊢ automorphize (g ∘ Quotient.mk' • f) x = HSMul.hSMul (β := Quotient (orbitRel α β) → M) g (automorphize f) x
have h : ∀ (b : β),
  automorphize (g ∘ Quotient.mk' • f) ⟦b⟧ = HSMul.hSMul (β := Quotient (orbitRel α β) → M) g (automorphize f) ⟦b⟧
Tactic: induction x using Quotient.inductionOn with | _ b
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Module (goal)
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 : β
⊢ automorphize (g ∘ Quotient.mk' • f) ⟦b⟧ = HSMul.hSMul (β := Quotient (orbitRel α β) → M) g (automorphize f) ⟦b⟧
have h : Quotient.lift (fun (b : β) ↦ ∑' (a : α), g (Quotient.mk' (a +ᵥ b)) • f (a +ᵥ b)) sorry ⟦b⟧ =
  g ⟦b⟧ • Quotient.lift (fun (b : β) ↦ ∑' (a : α), f (a +ᵥ b)) sorry ⟦b⟧
Tactic: simp only [automorphize, Pi.smul_apply', comp_apply]
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Module (goal)
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
have apply : (orbitRel α β : β → β → Prop) (a +ᵥ b) b
Tactic: apply (@Quotient.eq _ (AddAction.orbitRel α β) (a +ᵥ b) b).mpr
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Module (goal)
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 : α
⊢ (orbitRel α β : β → β → Prop) (a +ᵥ b) b
have h : (fun (m : α) ↦ m +ᵥ b) a = a +ᵥ b
Tactic: use a
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Module (hypothesis)
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 α β)
⊢ 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)
have H₁ : ∀ (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
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Module (goal)
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
⊢ 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)
have h : ∑' (a : α), g (π (a +ᵥ b)) • f (a +ᵥ b) = HSMul.hSMul (β := M) (g (π b)) (∑' (a : α), f (a +ᵥ b))
Tactic: change ∑' a : α, g (π (a +ᵥ b)) • f (a +ᵥ b) = g (π b) • ∑' a : α, f (a +ᵥ b)
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.Module (goal)
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 (π (a +ᵥ b)) • f (a +ᵥ b) = HSMul.hSMul (β := M) (g (π b)) (∑' (a : α), f (a +ᵥ b))
have h : ∑' (a : α), g (π b) • f (a +ᵥ b) = HSMul.hSMul (β := M) (g (π b)) (∑' (a : α), f (a +ᵥ b))
Tactic: simp_rw [H₁]
-- 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
he : HasProd (fun (k : ℕ) ↦ f (2 * k)) m
ho : HasProd (fun (k : ℕ) ↦ f (2 * k + 1)) m'
⊢ HasProd f (m * m')
have this : Injective (β := ℕ) fun (x : ℕ) ↦ 2 * x
Tactic: have := mul_right_injective₀ (two_ne_zero' ℕ)
-- 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
he : HasProd (fun (k : ℕ) ↦ f (2 * k)) m
ho : HasProd (fun (k : ℕ) ↦ f (2 * k + 1)) m'
this : Injective (β := ℕ) fun (x : ℕ) ↦ 2 * x
⊢ HasProd f (m * m')
have ho₁ : 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
Cleared hypotheses: ho
-- 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
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')
have refine : IsCompl (α := Set ℕ) (Set.range fun (x : ℕ) ↦ 2 * x) (Set.range (ι := ℕ) ((fun (x : ℕ) ↦ x + 1) ∘ fun (x : ℕ) ↦ 2 * x))
Tactic: refine (this.hasProd_range_iff.2 he).mul_isCompl ?_ ho
-- 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 : T2Space M
f : ℕ → M
hf : Multipliable f
⊢ HasProd f m ↔ Tendsto (fun (n : ℕ) ↦ ∏ i ∈ range n, f i) atTop (𝓝 m)
have refine : ∀ (h : Tendsto (fun (n : ℕ) ↦ ∏ i ∈ range n, f i) atTop (𝓝 m)), HasProd f m
Tactic: refine ⟨fun h ↦ h.tendsto_prod_nat, fun h ↦ ?_⟩
-- 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 : T2Space M
f : ℕ → M
hf : Multipliable f
h : Tendsto (fun (n : ℕ) ↦ ∏ i ∈ range n, f i) atTop (𝓝 m)
⊢ HasProd f m
have rw : HasProd f (∏' (b : ℕ), f b)
Tactic: rw [tendsto_nhds_unique h hf.hasProd.tendsto_prod_nat]
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.NatInt (goal)
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)) (∏' (b : β), m (s b))
have rw : Eq.{u_1 + 1} (α := M) (∏' (i : ℕ), m (⨆ b ∈ decode₂ β i, s b)) (∏' (y : ℕ), extend encode (fun (b : β) ↦ m (s b)) 1 y)
Tactic: rw [← tprod_extend_one (@encode_injective β _)]
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.NatInt (goal)
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)
have refine : ∀ (n : ℕ), m (⨆ b ∈ decode₂ β n, s b) = extend encode (fun (b : β) ↦ m (s b)) 1 n
Tactic: refine tprod_congr fun n ↦ ?_
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.NatInt (goal)
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 : ℕ
⊢ m (⨆ b ∈ decode₂ β n, s b) = extend encode (fun (b : β) ↦ m (s b)) 1 n
have inl : ∀ (a : β), m (⨆ b ∈ decode₂ β (encode a), s b) = extend encode (fun (b : β) ↦ m (s b)) 1 (encode a)
Tactic: rcases em (n ∈ Set.range (encode : β → ℕ)) with ⟨a, rfl⟩ | hn
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.NatInt (goal)
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)
⊢ m (⨆ b ∈ decode₂ β n, s b) = extend encode (fun (b : β) ↦ m (s b)) 1 n
have 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
Tactic: rcases em (n ∈ Set.range (encode : β → ℕ)) with ⟨a, rfl⟩ | hn
-- Lean 4 proof step from Mathlib.Topology.Algebra.InfiniteSum.NatInt (goal)
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
⊢ m (⨆ b ∈ decode₂ β n, s b) = extend encode (fun (b : β) ↦ m (s b)) 1 n
have inr : m (⨆ b ∈ decode₂ β n, s b) = 1 n
Tactic: rw [extend_apply' _ _ _ hn]