internlm/Lean-Github huggingface dataset:
Theorem: Algebra.TensorProduct.map_includeRight_eq_range_baseChange
Proof state before:
case h.mpr
R✝ : Type u_1
inst✝⁶ : CommRing R✝
A : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R✝ A
J : Ideal A
S : Type u_3
inst✝³ : CommRing S
inst✝² : Algebra A S
I : Ideal S
R : Type u_4
inst✝¹ : CommRing R
inst✝ : Algebra A R
x : R ⊗[A] S
⊢ (∃ y, (LinearMap.baseChange R (Submodule.restrictScalars A I).subtype) y = x) → x ∈ Ideal.map includeRight I
Tactic:
rintro ⟨y, rfl⟩
Proof state after:
case h.mpr.intro
R✝ : Type u_1
inst✝⁶ : CommRing R✝
A : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R✝ A
J : Ideal A
S : Type u_3
inst✝³ : CommRing S
inst✝² : Algebra A S
I : Ideal S
R : Type u_4
inst✝¹ : CommRing R
inst✝ : Algebra A R
y : R ⊗[A] ↥(Submodule.restrictScalars A I)
⊢ (LinearMap.baseChange R (Submodule.restrictScalars A I).subtype) y ∈ Ideal.map includeRight I
Theorem: Algebra.TensorProduct.map_includeRight_eq_range_baseChange
Proof state before:
case h.mpr.intro
R✝ : Type u_1
inst✝⁶ : CommRing R✝
A : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R✝ A
J : Ideal A
S : Type u_3
inst✝³ : CommRing S
inst✝² : Algebra A S
I : Ideal S
R : Type u_4
inst✝¹ : CommRing R
inst✝ : Algebra A R
y : R ⊗[A] ↥(Submodule.restrictScalars A I)
⊢ (LinearMap.baseChange R (Submodule.restrictScalars A I).subtype) y ∈ Ideal.map includeRight I
Tactic:
induction y using TensorProduct.induction_on with
| zero => simp only [_root_.map_zero, Submodule.zero_mem]
| tmul r s =>
  rcases s with ⟨s, hs⟩
  simp only [restrictScalars_mem] at hs
  simp only [baseChange_tmul, coeSubtype]
  rw [← mul_one r, ← smul_eq_mul, ← TensorProduct.smul_tmul']
  rw [← IsScalarTower.algebraMap_smul (R ⊗[A] S) r, smul_eq_mul]
  apply Ideal.mul_mem_left
  exact Ideal.mem_map_of_mem Algebra.TensorProduct.includeRight hs
| add x y hx hy =>
  simp only [map_add]
  exact Ideal.add_mem _ hx hy
Proof state after:
no goals
Theorem: Algebra.TensorProduct.map_includeRight_eq_range_baseChange
Proof state before:
case h.mpr.intro.zero
R✝ : Type u_1
inst✝⁶ : CommRing R✝
A : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R✝ A
J : Ideal A
S : Type u_3
inst✝³ : CommRing S
inst✝² : Algebra A S
I : Ideal S
R : Type u_4
inst✝¹ : CommRing R
inst✝ : Algebra A R
⊢ (LinearMap.baseChange R (Submodule.restrictScalars A I).subtype) 0 ∈ Ideal.map includeRight I
Tactic:
simp only [_root_.map_zero, Submodule.zero_mem]
Proof state after:
no goals
Theorem: Algebra.TensorProduct.map_includeRight_eq_range_baseChange
Proof state before:
case h.mpr.intro.tmul
R✝ : Type u_1
inst✝⁶ : CommRing R✝
A : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R✝ A
J : Ideal A
S : Type u_3
inst✝³ : CommRing S
inst✝² : Algebra A S
I : Ideal S
R : Type u_4
inst✝¹ : CommRing R
inst✝ : Algebra A R
r : R
s : ↥(Submodule.restrictScalars A I)
⊢ (LinearMap.baseChange R (Submodule.restrictScalars A I).subtype) (r ⊗ₜ[A] s) ∈ Ideal.map includeRight I
Tactic:
rcases s with ⟨s, hs⟩
Proof state after:
case h.mpr.intro.tmul.mk
R✝ : Type u_1
inst✝⁶ : CommRing R✝
A : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R✝ A
J : Ideal A
S : Type u_3
inst✝³ : CommRing S
inst✝² : Algebra A S
I : Ideal S
R : Type u_4
inst✝¹ : CommRing R
inst✝ : Algebra A R
r : R
s : S
hs : s ∈ Submodule.restrictScalars A I
⊢ (LinearMap.baseChange R (Submodule.restrictScalars A I).subtype) (r ⊗ₜ[A] ⟨s, hs⟩) ∈ Ideal.map includeRight I
Theorem: Algebra.TensorProduct.map_includeRight_eq_range_baseChange
Proof state before:
case h.mpr.intro.tmul.mk
R✝ : Type u_1
inst✝⁶ : CommRing R✝
A : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R✝ A
J : Ideal A
S : Type u_3
inst✝³ : CommRing S
inst✝² : Algebra A S
I : Ideal S
R : Type u_4
inst✝¹ : CommRing R
inst✝ : Algebra A R
r : R
s : S
hs : s ∈ Submodule.restrictScalars A I
⊢ (LinearMap.baseChange R (Submodule.restrictScalars A I).subtype) (r ⊗ₜ[A] ⟨s, hs⟩) ∈ Ideal.map includeRight I
Tactic:
simp only [restrictScalars_mem] at hs
Proof state after:
case h.mpr.intro.tmul.mk
R✝ : Type u_1
inst✝⁶ : CommRing R✝
A : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R✝ A
J : Ideal A
S : Type u_3
inst✝³ : CommRing S
inst✝² : Algebra A S
I : Ideal S
R : Type u_4
inst✝¹ : CommRing R
inst✝ : Algebra A R
r : R
s : S
hs✝ : s ∈ Submodule.restrictScalars A I
hs : s ∈ I
⊢ (LinearMap.baseChange R (Submodule.restrictScalars A I).subtype) (r ⊗ₜ[A] ⟨s, hs✝⟩) ∈ Ideal.map includeRight I
Theorem: Algebra.TensorProduct.map_includeRight_eq_range_baseChange
Proof state before:
case h.mpr.intro.tmul.mk
R✝ : Type u_1
inst✝⁶ : CommRing R✝
A : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R✝ A
J : Ideal A
S : Type u_3
inst✝³ : CommRing S
inst✝² : Algebra A S
I : Ideal S
R : Type u_4
inst✝¹ : CommRing R
inst✝ : Algebra A R
r : R
s : S
hs✝ : s ∈ Submodule.restrictScalars A I
hs : s ∈ I
⊢ (LinearMap.baseChange R (Submodule.restrictScalars A I).subtype) (r ⊗ₜ[A] ⟨s, hs✝⟩) ∈ Ideal.map includeRight I
Tactic:
simp only [baseChange_tmul, coeSubtype]
Proof state after:
case h.mpr.intro.tmul.mk
R✝ : Type u_1
inst✝⁶ : CommRing R✝
A : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R✝ A
J : Ideal A
S : Type u_3
inst✝³ : CommRing S
inst✝² : Algebra A S
I : Ideal S
R : Type u_4
inst✝¹ : CommRing R
inst✝ : Algebra A R
r : R
s : S
hs✝ : s ∈ Submodule.restrictScalars A I
hs : s ∈ I
⊢ r ⊗ₜ[A] s ∈ Ideal.map includeRight I
Theorem: Algebra.TensorProduct.map_includeRight_eq_range_baseChange
Proof state before:
case h.mpr.intro.tmul.mk
R✝ : Type u_1
inst✝⁶ : CommRing R✝
A : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R✝ A
J : Ideal A
S : Type u_3
inst✝³ : CommRing S
inst✝² : Algebra A S
I : Ideal S
R : Type u_4
inst✝¹ : CommRing R
inst✝ : Algebra A R
r : R
s : S
hs✝ : s ∈ Submodule.restrictScalars A I
hs : s ∈ I
⊢ r ⊗ₜ[A] s ∈ Ideal.map includeRight I
Tactic:
rw [← mul_one r, ← smul_eq_mul, ← TensorProduct.smul_tmul']
Proof state after:
case h.mpr.intro.tmul.mk
R✝ : Type u_1
inst✝⁶ : CommRing R✝
A : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R✝ A
J : Ideal A
S : Type u_3
inst✝³ : CommRing S
inst✝² : Algebra A S
I : Ideal S
R : Type u_4
inst✝¹ : CommRing R
inst✝ : Algebra A R
r : R
s : S
hs✝ : s ∈ Submodule.restrictScalars A I
hs : s ∈ I
⊢ r • 1 ⊗ₜ[A] s ∈ Ideal.map includeRight I
Theorem: Algebra.TensorProduct.map_includeRight_eq_range_baseChange
Proof state before:
case h.mpr.intro.tmul.mk
R✝ : Type u_1
inst✝⁶ : CommRing R✝
A : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R✝ A
J : Ideal A
S : Type u_3
inst✝³ : CommRing S
inst✝² : Algebra A S
I : Ideal S
R : Type u_4
inst✝¹ : CommRing R
inst✝ : Algebra A R
r : R
s : S
hs✝ : s ∈ Submodule.restrictScalars A I
hs : s ∈ I
⊢ r • 1 ⊗ₜ[A] s ∈ Ideal.map includeRight I
Tactic:
rw [← IsScalarTower.algebraMap_smul (R ⊗[A] S) r, smul_eq_mul]
Proof state after:
case h.mpr.intro.tmul.mk
R✝ : Type u_1
inst✝⁶ : CommRing R✝
A : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R✝ A
J : Ideal A
S : Type u_3
inst✝³ : CommRing S
inst✝² : Algebra A S
I : Ideal S
R : Type u_4
inst✝¹ : CommRing R
inst✝ : Algebra A R
r : R
s : S
hs✝ : s ∈ Submodule.restrictScalars A I
hs : s ∈ I
⊢ (algebraMap R (R ⊗[A] S)) r * 1 ⊗ₜ[A] s ∈ Ideal.map includeRight I
Theorem: Algebra.TensorProduct.map_includeRight_eq_range_baseChange
Proof state before:
case h.mpr.intro.tmul.mk
R✝ : Type u_1
inst✝⁶ : CommRing R✝
A : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R✝ A
J : Ideal A
S : Type u_3
inst✝³ : CommRing S
inst✝² : Algebra A S
I : Ideal S
R : Type u_4
inst✝¹ : CommRing R
inst✝ : Algebra A R
r : R
s : S
hs✝ : s ∈ Submodule.restrictScalars A I
hs : s ∈ I
⊢ (algebraMap R (R ⊗[A] S)) r * 1 ⊗ₜ[A] s ∈ Ideal.map includeRight I
Tactic:
apply Ideal.mul_mem_left
Proof state after:
case h.mpr.intro.tmul.mk.a
R✝ : Type u_1
inst✝⁶ : CommRing R✝
A : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R✝ A
J : Ideal A
S : Type u_3
inst✝³ : CommRing S
inst✝² : Algebra A S
I : Ideal S
R : Type u_4
inst✝¹ : CommRing R
inst✝ : Algebra A R
r : R
s : S
hs✝ : s ∈ Submodule.restrictScalars A I
hs : s ∈ I
⊢ 1 ⊗ₜ[A] s ∈ Ideal.map includeRight I
Theorem: Algebra.TensorProduct.map_includeRight_eq_range_baseChange
Proof state before:
case h.mpr.intro.tmul.mk.a
R✝ : Type u_1
inst✝⁶ : CommRing R✝
A : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R✝ A
J : Ideal A
S : Type u_3
inst✝³ : CommRing S
inst✝² : Algebra A S
I : Ideal S
R : Type u_4
inst✝¹ : CommRing R
inst✝ : Algebra A R
r : R
s : S
hs✝ : s ∈ Submodule.restrictScalars A I
hs : s ∈ I
⊢ 1 ⊗ₜ[A] s ∈ Ideal.map includeRight I
Tactic:
exact Ideal.mem_map_of_mem Algebra.TensorProduct.includeRight hs
Proof state after:
no goals
Theorem: Algebra.TensorProduct.map_includeRight_eq_range_baseChange
Proof state before:
case h.mpr.intro.add
R✝ : Type u_1
inst✝⁶ : CommRing R✝
A : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R✝ A
J : Ideal A
S : Type u_3
inst✝³ : CommRing S
inst✝² : Algebra A S
I : Ideal S
R : Type u_4
inst✝¹ : CommRing R
inst✝ : Algebra A R
x y : R ⊗[A] ↥(Submodule.restrictScalars A I)
hx : (LinearMap.baseChange R (Submodule.restrictScalars A I).subtype) x ∈ Ideal.map includeRight I
hy : (LinearMap.baseChange R (Submodule.restrictScalars A I).subtype) y ∈ Ideal.map includeRight I
⊢ (LinearMap.baseChange R (Submodule.restrictScalars A I).subtype) (x + y) ∈ Ideal.map includeRight I
Tactic:
simp only [map_add]
Proof state after:
case h.mpr.intro.add
R✝ : Type u_1
inst✝⁶ : CommRing R✝
A : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R✝ A
J : Ideal A
S : Type u_3
inst✝³ : CommRing S
inst✝² : Algebra A S
I : Ideal S
R : Type u_4
inst✝¹ : CommRing R
inst✝ : Algebra A R
x y : R ⊗[A] ↥(Submodule.restrictScalars A I)
hx : (LinearMap.baseChange R (Submodule.restrictScalars A I).subtype) x ∈ Ideal.map includeRight I
hy : (LinearMap.baseChange R (Submodule.restrictScalars A I).subtype) y ∈ Ideal.map includeRight I
⊢ (LinearMap.baseChange R (Submodule.restrictScalars A I).subtype) x +
      (LinearMap.baseChange R (Submodule.restrictScalars A I).subtype) y ∈
    Ideal.map includeRight I
Theorem: Algebra.TensorProduct.map_includeRight_eq_range_baseChange
Proof state before:
case h.mpr.intro.add
R✝ : Type u_1
inst✝⁶ : CommRing R✝
A : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R✝ A
J : Ideal A
S : Type u_3
inst✝³ : CommRing S
inst✝² : Algebra A S
I : Ideal S
R : Type u_4
inst✝¹ : CommRing R
inst✝ : Algebra A R
x y : R ⊗[A] ↥(Submodule.restrictScalars A I)
hx : (LinearMap.baseChange R (Submodule.restrictScalars A I).subtype) x ∈ Ideal.map includeRight I
hy : (LinearMap.baseChange R (Submodule.restrictScalars A I).subtype) y ∈ Ideal.map includeRight I
⊢ (LinearMap.baseChange R (Submodule.restrictScalars A I).subtype) x +
      (LinearMap.baseChange R (Submodule.restrictScalars A I).subtype) y ∈
    Ideal.map includeRight I
Tactic:
exact Ideal.add_mem _ hx hy
Proof state after:
no goals
Theorem: Ideal.isAugmentation_baseChange
Proof state before:
R✝ : Type u_1
inst✝⁶ : CommRing R✝
A : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R✝ A
J : Ideal A
S : Type u_3
inst✝³ : CommRing S
inst✝² : Algebra A S
I : Ideal S
hI : IsCompl (Subalgebra.toSubmodule ⊥) (Submodule.restrictScalars A I)
R : Type u_4
inst✝¹ : CommRing R
inst✝ : Algebra A R
⊢ IsAugmentation R (map Algebra.TensorProduct.includeRight I)
Tactic:
unfold Ideal.IsAugmentation
Proof state after:
R✝ : Type u_1
inst✝⁶ : CommRing R✝
A : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R✝ A
J : Ideal A
S : Type u_3
inst✝³ : CommRing S
inst✝² : Algebra A S
I : Ideal S
hI : IsCompl (Subalgebra.toSubmodule ⊥) (Submodule.restrictScalars A I)
R : Type u_4
inst✝¹ : CommRing R
inst✝ : Algebra A R
⊢ IsCompl (Subalgebra.toSubmodule ⊥) (Submodule.restrictScalars R (map Algebra.TensorProduct.includeRight I))
Theorem: Ideal.isAugmentation_baseChange
Proof state before:
R✝ : Type u_1
inst✝⁶ : CommRing R✝
A : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R✝ A
J : Ideal A
S : Type u_3
inst✝³ : CommRing S
inst✝² : Algebra A S
I : Ideal S
hI : IsCompl (Subalgebra.toSubmodule ⊥) (Submodule.restrictScalars A I)
R : Type u_4
inst✝¹ : CommRing R
inst✝ : Algebra A R
⊢ IsCompl (Subalgebra.toSubmodule ⊥) (Submodule.restrictScalars R (map Algebra.TensorProduct.includeRight I))
Tactic:
rw [Algebra.baseChange_bot]
Proof state after:
R✝ : Type u_1
inst✝⁶ : CommRing R✝
A : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R✝ A
J : Ideal A
S : Type u_3
inst✝³ : CommRing S
inst✝² : Algebra A S
I : Ideal S
hI : IsCompl (Subalgebra.toSubmodule ⊥) (Submodule.restrictScalars A I)
R : Type u_4
inst✝¹ : CommRing R
inst✝ : Algebra A R
⊢ IsCompl (LinearMap.range (LinearMap.baseChange R (Subalgebra.toSubmodule ⊥).subtype))
    (Submodule.restrictScalars R (map Algebra.TensorProduct.includeRight I))
Theorem: Ideal.isAugmentation_baseChange
Proof state before:
R✝ : Type u_1
inst✝⁶ : CommRing R✝
A : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R✝ A
J : Ideal A
S : Type u_3
inst✝³ : CommRing S
inst✝² : Algebra A S
I : Ideal S
hI : IsCompl (Subalgebra.toSubmodule ⊥) (Submodule.restrictScalars A I)
R : Type u_4
inst✝¹ : CommRing R
inst✝ : Algebra A R
⊢ IsCompl (LinearMap.range (LinearMap.baseChange R (Subalgebra.toSubmodule ⊥).subtype))
    (Submodule.restrictScalars R (map Algebra.TensorProduct.includeRight I))
Tactic:
rw [Algebra.TensorProduct.map_includeRight_eq_range_baseChange]
Proof state after:
R✝ : Type u_1
inst✝⁶ : CommRing R✝
A : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R✝ A
J : Ideal A
S : Type u_3
inst✝³ : CommRing S
inst✝² : Algebra A S
I : Ideal S
hI : IsCompl (Subalgebra.toSubmodule ⊥) (Submodule.restrictScalars A I)
R : Type u_4
inst✝¹ : CommRing R
inst✝ : Algebra A R
⊢ IsCompl (LinearMap.range (LinearMap.baseChange R (Subalgebra.toSubmodule ⊥).subtype))
    (LinearMap.range (LinearMap.baseChange R (Submodule.restrictScalars A I).subtype))
Theorem: Ideal.isAugmentation_baseChange
Proof state before:
R✝ : Type u_1
inst✝⁶ : CommRing R✝
A : Type u_2
inst✝⁵ : CommRing A
inst✝⁴ : Algebra R✝ A
J : Ideal A
S : Type u_3
inst✝³ : CommRing S
inst✝² : Algebra A S
I : Ideal S
hI : IsCompl (Subalgebra.toSubmodule ⊥) (Submodule.restrictScalars A I)
R : Type u_4
inst✝¹ : CommRing R
inst✝ : Algebra A R
⊢ IsCompl (LinearMap.range (LinearMap.baseChange R (Subalgebra.toSubmodule ⊥).subtype))
    (LinearMap.range (LinearMap.baseChange R (Submodule.restrictScalars A I).subtype))
Tactic:
exact isCompl_baseChange hI R
Proof state after:
no goals
Theorem: algebraMap_injective'
Proof state before:
R : Type u_1
A : Type u_2
K : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : Field A
inst✝⁵ : Algebra R A
inst✝⁴ : IsFractionRing R A
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : Algebra A K
inst✝ : IsScalarTower R A K
⊢ Function.Injective ⇑(algebraMap R K)
Tactic:
rw [IsScalarTower.algebraMap_eq R A K]
Proof state after:
R : Type u_1
A : Type u_2
K : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : Field A
inst✝⁵ : Algebra R A
inst✝⁴ : IsFractionRing R A
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : Algebra A K
inst✝ : IsScalarTower R A K
⊢ Function.Injective ⇑((algebraMap A K).comp (algebraMap R A))
Theorem: algebraMap_injective'
Proof state before:
R : Type u_1
A : Type u_2
K : Type u_3
inst✝⁷ : CommRing R
inst✝⁶ : Field A
inst✝⁵ : Algebra R A
inst✝⁴ : IsFractionRing R A
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : Algebra A K
inst✝ : IsScalarTower R A K
⊢ Function.Injective ⇑((algebraMap A K).comp (algebraMap R A))
Tactic:
apply Function.Injective.comp (RingHom.injective (algebraMap A K)) (IsFractionRing.injective R A)
Proof state after:
no goals
Theorem: PowerSeries.WithPiTopology.tendsto_iff_coeff_tendsto
Proof state before:
α : Type u_1
inst✝¹ : TopologicalSpace α
σ : ?m.916
inst✝ : Semiring α
ι : Type u_2
f : ι → α⟦X⟧
u : Filter ι
g : α⟦X⟧
⊢ Filter.Tendsto f u (nhds g) ↔ ∀ (d : ℕ), Filter.Tendsto (fun i => (coeff α d) (f i)) u (nhds ((coeff α d) g))
Tactic:
rw [MvPowerSeries.WithPiTopology.tendsto_iff_coeff_tendsto]
Proof state after:
α : Type u_1
inst✝¹ : TopologicalSpace α
σ : ?m.916
inst✝ : Semiring α
ι : Type u_2
f : ι → α⟦X⟧
u : Filter ι
g : α⟦X⟧
⊢ (∀ (d : Unit →₀ ℕ),
      Filter.Tendsto (fun i => (MvPowerSeries.coeff α d) (f i)) u (nhds ((MvPowerSeries.coeff α d) g))) ↔
    ∀ (d : ℕ), Filter.Tendsto (fun i => (coeff α d) (f i)) u (nhds ((coeff α d) g))
Theorem: PowerSeries.WithPiTopology.tendsto_iff_coeff_tendsto
Proof state before:
α : Type u_1
inst✝¹ : TopologicalSpace α
σ : ?m.916
inst✝ : Semiring α
ι : Type u_2
f : ι → α⟦X⟧
u : Filter ι
g : α⟦X⟧
⊢ (∀ (d : Unit →₀ ℕ),
      Filter.Tendsto (fun i => (MvPowerSeries.coeff α d) (f i)) u (nhds ((MvPowerSeries.coeff α d) g))) ↔
    ∀ (d : ℕ), Filter.Tendsto (fun i => (coeff α d) (f i)) u (nhds ((coeff α d) g))
Tactic:
apply (Finsupp.LinearEquiv.finsuppUnique ℕ ℕ Unit).toEquiv.forall_congr
Proof state after:
α : Type u_1
inst✝¹ : TopologicalSpace α
σ : ?m.916
inst✝ : Semiring α
ι : Type u_2
f : ι → α⟦X⟧
u : Filter ι
g : α⟦X⟧
⊢ ∀ {x : Unit →₀ ℕ},
    Filter.Tendsto (fun i => (MvPowerSeries.coeff α x) (f i)) u (nhds ((MvPowerSeries.coeff α x) g)) ↔
      Filter.Tendsto (fun i => (coeff α ((Finsupp.LinearEquiv.finsuppUnique ℕ ℕ Unit).toEquiv x)) (f i)) u
        (nhds ((coeff α ((Finsupp.LinearEquiv.finsuppUnique ℕ ℕ Unit).toEquiv x)) g))
Theorem: PowerSeries.WithPiTopology.tendsto_iff_coeff_tendsto
Proof state before:
α : Type u_1
inst✝¹ : TopologicalSpace α
σ : ?m.916
inst✝ : Semiring α
ι : Type u_2
f : ι → α⟦X⟧
u : Filter ι
g : α⟦X⟧
⊢ ∀ {x : Unit →₀ ℕ},
    Filter.Tendsto (fun i => (MvPowerSeries.coeff α x) (f i)) u (nhds ((MvPowerSeries.coeff α x) g)) ↔
      Filter.Tendsto (fun i => (coeff α ((Finsupp.LinearEquiv.finsuppUnique ℕ ℕ Unit).toEquiv x)) (f i)) u
        (nhds ((coeff α ((Finsupp.LinearEquiv.finsuppUnique ℕ ℕ Unit).toEquiv x)) g))
Tactic:
intro d
Proof state after:
α : Type u_1
inst✝¹ : TopologicalSpace α
σ : ?m.916
inst✝ : Semiring α
ι : Type u_2
f : ι → α⟦X⟧
u : Filter ι
g : α⟦X⟧
d : Unit →₀ ℕ
⊢ Filter.Tendsto (fun i => (MvPowerSeries.coeff α d) (f i)) u (nhds ((MvPowerSeries.coeff α d) g)) ↔
    Filter.Tendsto (fun i => (coeff α ((Finsupp.LinearEquiv.finsuppUnique ℕ ℕ Unit).toEquiv d)) (f i)) u
      (nhds ((coeff α ((Finsupp.LinearEquiv.finsuppUnique ℕ ℕ Unit).toEquiv d)) g))
Theorem: PowerSeries.WithPiTopology.tendsto_iff_coeff_tendsto
Proof state before:
α : Type u_1
inst✝¹ : TopologicalSpace α
σ : ?m.916
inst✝ : Semiring α
ι : Type u_2
f : ι → α⟦X⟧
u : Filter ι
g : α⟦X⟧
d : Unit →₀ ℕ
⊢ Filter.Tendsto (fun i => (MvPowerSeries.coeff α d) (f i)) u (nhds ((MvPowerSeries.coeff α d) g)) ↔
    Filter.Tendsto (fun i => (coeff α ((Finsupp.LinearEquiv.finsuppUnique ℕ ℕ Unit).toEquiv d)) (f i)) u
      (nhds ((coeff α ((Finsupp.LinearEquiv.finsuppUnique ℕ ℕ Unit).toEquiv d)) g))
Tactic:
simp only [LinearEquiv.coe_toEquiv, Finsupp.LinearEquiv.finsuppUnique_apply,
  PUnit.default_eq_unit, coeff]
Proof state after:
α : Type u_1
inst✝¹ : TopologicalSpace α
σ : ?m.916
inst✝ : Semiring α
ι : Type u_2
f : ι → α⟦X⟧
u : Filter ι
g : α⟦X⟧
d : Unit →₀ ℕ
⊢ Filter.Tendsto (fun i => (MvPowerSeries.coeff α d) (f i)) u (nhds ((MvPowerSeries.coeff α d) g)) ↔
    Filter.Tendsto (fun i => (MvPowerSeries.coeff α (Finsupp.single () (d PUnit.unit))) (f i)) u
      (nhds ((MvPowerSeries.coeff α (Finsupp.single () (d PUnit.unit))) g))
Theorem: PowerSeries.WithPiTopology.tendsto_iff_coeff_tendsto
Proof state before:
α : Type u_1
inst✝¹ : TopologicalSpace α
σ : ?m.916
inst✝ : Semiring α
ι : Type u_2
f : ι → α⟦X⟧
u : Filter ι
g : α⟦X⟧
d : Unit →₀ ℕ
⊢ Filter.Tendsto (fun i => (MvPowerSeries.coeff α d) (f i)) u (nhds ((MvPowerSeries.coeff α d) g)) ↔
    Filter.Tendsto (fun i => (MvPowerSeries.coeff α (Finsupp.single () (d PUnit.unit))) (f i)) u
      (nhds ((MvPowerSeries.coeff α (Finsupp.single () (d PUnit.unit))) g))
Tactic:
apply iff_of_eq
Proof state after:
case a
α : Type u_1
inst✝¹ : TopologicalSpace α
σ : ?m.916
inst✝ : Semiring α
ι : Type u_2
f : ι → α⟦X⟧
u : Filter ι
g : α⟦X⟧
d : Unit →₀ ℕ
⊢ Filter.Tendsto (fun i => (MvPowerSeries.coeff α d) (f i)) u (nhds ((MvPowerSeries.coeff α d) g)) =
    Filter.Tendsto (fun i => (MvPowerSeries.coeff α (Finsupp.single () (d PUnit.unit))) (f i)) u
      (nhds ((MvPowerSeries.coeff α (Finsupp.single () (d PUnit.unit))) g))
Theorem: PowerSeries.WithPiTopology.tendsto_iff_coeff_tendsto
Proof state before:
case a
α : Type u_1
inst✝¹ : TopologicalSpace α
σ : ?m.916
inst✝ : Semiring α
ι : Type u_2
f : ι → α⟦X⟧
u : Filter ι
g : α⟦X⟧
d : Unit →₀ ℕ
⊢ Filter.Tendsto (fun i => (MvPowerSeries.coeff α d) (f i)) u (nhds ((MvPowerSeries.coeff α d) g)) =
    Filter.Tendsto (fun i => (MvPowerSeries.coeff α (Finsupp.single () (d PUnit.unit))) (f i)) u
      (nhds ((MvPowerSeries.coeff α (Finsupp.single () (d PUnit.unit))) g))
Tactic:
congr
Proof state after:
case a.e_f
α : Type u_1
inst✝¹ : TopologicalSpace α
σ : ?m.916
inst✝ : Semiring α
ι : Type u_2
f : ι → α⟦X⟧
u : Filter ι
g : α⟦X⟧
d : Unit →₀ ℕ
⊢ (fun i => (MvPowerSeries.coeff α d) (f i)) = fun i => (MvPowerSeries.coeff α (Finsupp.single () (d PUnit.unit))) (f i)

case a.e_l₂.e_x.e_a.e_n
α : Type u_1
inst✝¹ : TopologicalSpace α
σ : ?m.916
inst✝ : Semiring α
ι : Type u_2
f : ι → α⟦X⟧
u : Filter ι
g : α⟦X⟧
d : Unit →₀ ℕ
⊢ d = Finsupp.single () (d PUnit.unit)
Theorem: PowerSeries.WithPiTopology.tendsto_iff_coeff_tendsto
Proof state before:
case a.e_f
α : Type u_1
inst✝¹ : TopologicalSpace α
σ : ?m.916
inst✝ : Semiring α
ι : Type u_2
f : ι → α⟦X⟧
u : Filter ι
g : α⟦X⟧
d : Unit →₀ ℕ
⊢ (fun i => (MvPowerSeries.coeff α d) (f i)) = fun i => (MvPowerSeries.coeff α (Finsupp.single () (d PUnit.unit))) (f i)

case a.e_l₂.e_x.e_a.e_n
α : Type u_1
inst✝¹ : TopologicalSpace α
σ : ?m.916
inst✝ : Semiring α
ι : Type u_2
f : ι → α⟦X⟧
u : Filter ι
g : α⟦X⟧
d : Unit →₀ ℕ
⊢ d = Finsupp.single () (d PUnit.unit)
Tactic:
ext i
Proof state after:
case a.e_f.h
α : Type u_1
inst✝¹ : TopologicalSpace α
σ : ?m.916
inst✝ : Semiring α
ι : Type u_2
f : ι → α⟦X⟧
u : Filter ι
g : α⟦X⟧
d : Unit →₀ ℕ
i : ι
⊢ (MvPowerSeries.coeff α d) (f i) = (MvPowerSeries.coeff α (Finsupp.single () (d PUnit.unit))) (f i)

case a.e_l₂.e_x.e_a.e_n
α : Type u_1
inst✝¹ : TopologicalSpace α
σ : ?m.916
inst✝ : Semiring α
ι : Type u_2
f : ι → α⟦X⟧
u : Filter ι
g : α⟦X⟧
d : Unit →₀ ℕ
⊢ d = Finsupp.single () (d PUnit.unit)
Theorem: PowerSeries.WithPiTopology.tendsto_iff_coeff_tendsto
Proof state before:
case a.e_f.h
α : Type u_1
inst✝¹ : TopologicalSpace α
σ : ?m.916
inst✝ : Semiring α
ι : Type u_2
f : ι → α⟦X⟧
u : Filter ι
g : α⟦X⟧
d : Unit →₀ ℕ
i : ι
⊢ (MvPowerSeries.coeff α d) (f i) = (MvPowerSeries.coeff α (Finsupp.single () (d PUnit.unit))) (f i)

case a.e_l₂.e_x.e_a.e_n
α : Type u_1
inst✝¹ : TopologicalSpace α
σ : ?m.916
inst✝ : Semiring α
ι : Type u_2
f : ι → α⟦X⟧
u : Filter ι
g : α⟦X⟧
d : Unit →₀ ℕ
⊢ d = Finsupp.single () (d PUnit.unit)
Tactic:
congr
Proof state after:
case a.e_f.h.e_a.e_n
α : Type u_1
inst✝¹ : TopologicalSpace α
σ : ?m.916
inst✝ : Semiring α
ι : Type u_2
f : ι → α⟦X⟧
u : Filter ι
g : α⟦X⟧
d : Unit →₀ ℕ
i : ι
⊢ d = Finsupp.single () (d PUnit.unit)

case a.e_l₂.e_x.e_a.e_n
α : Type u_1
inst✝¹ : TopologicalSpace α
σ : ?m.916
inst✝ : Semiring α
ι : Type u_2
f : ι → α⟦X⟧
u : Filter ι
g : α⟦X⟧
d : Unit →₀ ℕ
⊢ d = Finsupp.single () (d PUnit.unit)
Theorem: PowerSeries.WithPiTopology.tendsto_iff_coeff_tendsto
Proof state before:
case a.e_f.h.e_a.e_n
α : Type u_1
inst✝¹ : TopologicalSpace α
σ : ?m.916
inst✝ : Semiring α
ι : Type u_2
f : ι → α⟦X⟧
u : Filter ι
g : α⟦X⟧
d : Unit →₀ ℕ
i : ι
⊢ d = Finsupp.single () (d PUnit.unit)

case a.e_l₂.e_x.e_a.e_n
α : Type u_1
inst✝¹ : TopologicalSpace α
σ : ?m.916
inst✝ : Semiring α
ι : Type u_2
f : ι → α⟦X⟧
u : Filter ι
g : α⟦X⟧
d : Unit →₀ ℕ
⊢ d = Finsupp.single () (d PUnit.unit)
Tactic:
all_goals { ext; simp }
Proof state after:
no goals
Theorem: PowerSeries.WithPiTopology.tendsto_iff_coeff_tendsto
Proof state before:
case a.e_l₂.e_x.e_a.e_n
α : Type u_1
inst✝¹ : TopologicalSpace α
σ : ?m.916
inst✝ : Semiring α
ι : Type u_2
f : ι → α⟦X⟧
u : Filter ι
g : α⟦X⟧
d : Unit →₀ ℕ
⊢ d = Finsupp.single () (d PUnit.unit)
Tactic:
ext
Proof state after:
case a.e_l₂.e_x.e_a.e_n.h
α : Type u_1
inst✝¹ : TopologicalSpace α
σ : ?m.916
inst✝ : Semiring α
ι : Type u_2
f : ι → α⟦X⟧
u : Filter ι
g : α⟦X⟧
d : Unit →₀ ℕ
⊢ d default = (Finsupp.single () (d PUnit.unit)) default
Theorem: PowerSeries.WithPiTopology.tendsto_iff_coeff_tendsto
Proof state before:
case a.e_l₂.e_x.e_a.e_n.h
α : Type u_1
inst✝¹ : TopologicalSpace α
σ : ?m.916
inst✝ : Semiring α
ι : Type u_2
f : ι → α⟦X⟧
u : Filter ι
g : α⟦X⟧
d : Unit →₀ ℕ
⊢ d default = (Finsupp.single () (d PUnit.unit)) default
Tactic:
simp
Proof state after:
no goals