[GOAL]
ι : Sort u_1
α : Type u_2
β : Type u_3
X : Type u_4
Y : Type u_5
s : Set α
⊢ IsOpen {l | s ∈ l}
[PROOFSTEP]
simpa only [Iic_principal] using isOpen_Iic_principal
[GOAL]
ι : Sort u_1
α : Type u_2
β : Type u_3
X : Type u_4
Y : Type u_5
⊢ ∀ (t₁ : Set (Filter α)),
    t₁ ∈ range (Iic ∘ 𝓟) →
      ∀ (t₂ : Set (Filter α)),
        t₂ ∈ range (Iic ∘ 𝓟) → ∀ (x : Filter α), x ∈ t₁ ∩ t₂ → ∃ t₃, t₃ ∈ range (Iic ∘ 𝓟) ∧ x ∈ t₃ ∧ t₃ ⊆ t₁ ∩ t₂
[PROOFSTEP]
rintro _ ⟨s, rfl⟩ _ ⟨t, rfl⟩ l hl
[GOAL]
case intro.intro
ι : Sort u_1
α : Type u_2
β : Type u_3
X : Type u_4
Y : Type u_5
s t : Set α
l : Filter α
hl : l ∈ (Iic ∘ 𝓟) s ∩ (Iic ∘ 𝓟) t
⊢ ∃ t₃, t₃ ∈ range (Iic ∘ 𝓟) ∧ l ∈ t₃ ∧ t₃ ⊆ (Iic ∘ 𝓟) s ∩ (Iic ∘ 𝓟) t
[PROOFSTEP]
exact ⟨Iic (𝓟 s) ∩ Iic (𝓟 t), ⟨s ∩ t, by simp⟩, hl, Subset.rfl⟩
[GOAL]
ι : Sort u_1
α : Type u_2
β : Type u_3
X : Type u_4
Y : Type u_5
s t : Set α
l : Filter α
hl : l ∈ (Iic ∘ 𝓟) s ∩ (Iic ∘ 𝓟) t
⊢ (Iic ∘ 𝓟) (s ∩ t) = Iic (𝓟 s) ∩ Iic (𝓟 t)
[PROOFSTEP]
simp
[GOAL]
ι : Sort u_1
α : Type u_2
β : Type u_3
X : Type u_4
Y : Type u_5
s : Set (Filter α)
⊢ (∃ S, S ⊆ range (Iic ∘ 𝓟) ∧ s = ⋃₀ S) ↔ ∃ T, s = ⋃ (t : Set α) (_ : t ∈ T), Iic (𝓟 t)
[PROOFSTEP]
simp only [exists_subset_range_and_iff, sUnion_image, (· ∘ ·)]
[GOAL]
ι : Sort u_1
α : Type u_2
β : Type u_3
X : Type u_4
Y : Type u_5
l : Filter α
⊢ ⨅ (s : Set (Filter α)) (_ : s ∈ {s | l ∈ s ∧ s ∈ range (Iic ∘ 𝓟)}), 𝓟 s = Filter.lift' l (Iic ∘ 𝓟)
[PROOFSTEP]
simp only [mem_setOf_eq, @and_comm (l ∈ _), iInf_and, iInf_range, Filter.lift', Filter.lift, (· ∘ ·), mem_Iic,
  le_principal_iff]
[GOAL]
ι : Sort u_1
α : Type u_2
β : Type u_3
X : Type u_4
Y : Type u_5
l : Filter α
⊢ 𝓝 l = Filter.lift' l fun s => {l' | s ∈ l'}
[PROOFSTEP]
simpa only [(· ∘ ·), Iic_principal] using nhds_eq l
[GOAL]
ι : Sort u_1
α : Type u_2
β : Type u_3
X : Type u_4
Y : Type u_5
la : Filter α
lb : Filter β
f : α → Filter β
⊢ Tendsto f la (𝓝 lb) ↔ ∀ (s : Set β), s ∈ lb → ∀ᶠ (a : α) in la, s ∈ f a
[PROOFSTEP]
simp only [nhds_eq', tendsto_lift', mem_setOf_eq]
[GOAL]
ι : Sort u_1
α : Type u_2
β : Type u_3
X : Type u_4
Y : Type u_5
l : Filter α
p : ι → Prop
s : ι → Set α
h : HasBasis l p s
⊢ HasBasis (𝓝 l) p fun i => Iic (𝓟 (s i))
[PROOFSTEP]
rw [nhds_eq]
[GOAL]
ι : Sort u_1
α : Type u_2
β : Type u_3
X : Type u_4
Y : Type u_5
l : Filter α
p : ι → Prop
s : ι → Set α
h : HasBasis l p s
⊢ HasBasis (Filter.lift' l (Iic ∘ 𝓟)) p fun i => Iic (𝓟 (s i))
[PROOFSTEP]
exact h.lift' monotone_principal.Iic
[GOAL]
ι : Sort u_1
α : Type u_2
β : Type u_3
X : Type u_4
Y : Type u_5
l : Filter X
⊢ Tendsto pure l (𝓝 l)
[PROOFSTEP]
rw [Filter.tendsto_nhds]
[GOAL]
ι : Sort u_1
α : Type u_2
β : Type u_3
X : Type u_4
Y : Type u_5
l : Filter X
⊢ ∀ (s : Set X), s ∈ l → ∀ᶠ (a : X) in l, s ∈ pure a
[PROOFSTEP]
refine fun s hs ↦ Eventually.mono hs fun x ↦ id
[GOAL]
ι : Sort u_1
α : Type u_2
β : Type u_3
X : Type u_4
Y : Type u_5
l : Filter α
p : ι → Prop
s : ι → Set α
h : HasBasis l p s
⊢ HasBasis (𝓝 l) p fun i => {l' | s i ∈ l'}
[PROOFSTEP]
simpa only [Iic_principal] using h.nhds
[GOAL]
ι : Sort u_1
α : Type u_2
β : Type u_3
X : Type u_4
Y : Type u_5
⊢ 𝓝 ⊥ = pure ⊥
[PROOFSTEP]
simp [nhds_eq, (· ∘ ·), lift'_bot monotone_principal.Iic]
[GOAL]
ι : Sort u_1
α : Type u_2
β : Type u_3
X : Type u_4
Y : Type u_5
⊢ 𝓝 ⊤ = ⊤
[PROOFSTEP]
simp [nhds_eq]
[GOAL]
ι : Sort u_1
α : Type u_2
β : Type u_3
X : Type u_4
Y : Type u_5
x : α
⊢ 𝓝 (pure x) = 𝓟 {⊥, pure x}
[PROOFSTEP]
rw [← principal_singleton, nhds_principal, principal_singleton, Iic_pure]
[GOAL]
ι : Sort u_1
α : Type u_2
β : Type u_3
X : Type u_4
Y : Type u_5
f : ι → Filter α
⊢ 𝓝 (⨅ (i : ι), f i) = ⨅ (i : ι), 𝓝 (f i)
[PROOFSTEP]
simp only [nhds_eq]
[GOAL]
ι : Sort u_1
α : Type u_2
β : Type u_3
X : Type u_4
Y : Type u_5
f : ι → Filter α
⊢ Filter.lift' (⨅ (i : ι), f i) (Iic ∘ 𝓟) = ⨅ (i : ι), Filter.lift' (f i) (Iic ∘ 𝓟)
[PROOFSTEP]
apply lift'_iInf_of_map_univ
[GOAL]
case hg
ι : Sort u_1
α : Type u_2
β : Type u_3
X : Type u_4
Y : Type u_5
f : ι → Filter α
⊢ ∀ {s t : Set α}, (Iic ∘ 𝓟) (s ∩ t) = (Iic ∘ 𝓟) s ∩ (Iic ∘ 𝓟) t
[PROOFSTEP]
simp
[GOAL]
case hg'
ι : Sort u_1
α : Type u_2
β : Type u_3
X : Type u_4
Y : Type u_5
f : ι → Filter α
⊢ (Iic ∘ 𝓟) univ = univ
[PROOFSTEP]
simp
[GOAL]
ι : Sort u_1
α : Type u_2
β : Type u_3
X : Type u_4
Y : Type u_5
l₁ l₂ : Filter α
⊢ 𝓝 (l₁ ⊓ l₂) = 𝓝 l₁ ⊓ 𝓝 l₂
[PROOFSTEP]
simpa only [iInf_bool_eq] using nhds_iInf fun b => cond b l₁ l₂
[GOAL]
ι : Sort u_1
α : Type u_2
β : Type u_3
X : Type u_4
Y : Type u_5
l : Filter α
⊢ ⋂₀ {s | s ∈ 𝓝 l} = Iic l
[PROOFSTEP]
simp_rw [nhds_eq, (· ∘ ·), sInter_lift'_sets monotone_principal.Iic, Iic, le_principal_iff, ← setOf_forall, ←
  Filter.le_def]
[GOAL]
ι : Sort u_1
α : Type u_2
β : Type u_3
X : Type u_4
Y : Type u_5
l₁ l₂ : Filter α
⊢ 𝓝 l₁ ≤ 𝓝 l₂ ↔ l₁ ≤ l₂
[PROOFSTEP]
refine' ⟨fun h => _, fun h => monotone_nhds h⟩
[GOAL]
ι : Sort u_1
α : Type u_2
β : Type u_3
X : Type u_4
Y : Type u_5
l₁ l₂ : Filter α
h : 𝓝 l₁ ≤ 𝓝 l₂
⊢ l₁ ≤ l₂
[PROOFSTEP]
rw [← Iic_subset_Iic, ← sInter_nhds, ← sInter_nhds]
[GOAL]
ι : Sort u_1
α : Type u_2
β : Type u_3
X : Type u_4
Y : Type u_5
l₁ l₂ : Filter α
h : 𝓝 l₁ ≤ 𝓝 l₂
⊢ ⋂₀ {s | s ∈ 𝓝 l₁} ⊆ ⋂₀ {s | s ∈ 𝓝 l₂}
[PROOFSTEP]
exact sInter_subset_sInter h
[GOAL]
ι : Sort u_1
α : Type u_2
β : Type u_3
X : Type u_4
Y : Type u_5
s : Set (Filter α)
l : Filter α
⊢ l ∈ interior s ↔ ∃ t, t ∈ l ∧ Iic (𝓟 t) ⊆ s
[PROOFSTEP]
rw [mem_interior_iff_mem_nhds, mem_nhds_iff]
[GOAL]
ι : Sort u_1
α : Type u_2
β : Type u_3
X : Type u_4
Y : Type u_5
s : Set (Filter α)
l : Filter α
⊢ l ∈ closure s ↔ ∀ (t : Set α), t ∈ l → ∃ l', l' ∈ s ∧ t ∈ l'
[PROOFSTEP]
simp only [closure_eq_compl_interior_compl, Filter.mem_interior, mem_compl_iff, not_exists, not_forall,
  Classical.not_not, exists_prop, not_and, and_comm, subset_def, mem_Iic, le_principal_iff]
[GOAL]
ι : Sort u_1
α : Type u_2
β : Type u_3
X : Type u_4
Y : Type u_5
l : Filter α
⊢ closure {l} = Ici l
[PROOFSTEP]
ext l'
[GOAL]
case h
ι : Sort u_1
α : Type u_2
β : Type u_3
X : Type u_4
Y : Type u_5
l l' : Filter α
⊢ l' ∈ closure {l} ↔ l' ∈ Ici l
[PROOFSTEP]
simp [Filter.mem_closure, Filter.le_def]
[GOAL]
ι : Sort u_1
α : Type u_2
β : Type u_3
X : Type u_4
Y : Type u_5
l₁ l₂ : Filter α
⊢ l₁ ⤳ l₂ ↔ l₁ ≤ l₂
[PROOFSTEP]
simp only [specializes_iff_closure_subset, Filter.closure_singleton, Ici_subset_Ici]
[GOAL]
ι : Sort u_1
α : Type u_2
β : Type u_3
X : Type u_4
Y : Type u_5
inst✝ : Preorder α
⊢ 𝓝 atTop = ⨅ (x : α), 𝓟 (Iic (𝓟 (Ici x)))
[PROOFSTEP]
simp only [atTop, nhds_iInf, nhds_principal]
[GOAL]
ι : Sort u_1
α : Type u_2
β : Type u_3
X : Type u_4
Y : Type u_5
inst✝ : Preorder β
l : Filter α
f : α → Filter β
⊢ Tendsto f l (𝓝 atTop) ↔ ∀ (y : β), ∀ᶠ (a : α) in l, Ici y ∈ f a
[PROOFSTEP]
simp only [nhds_atTop, tendsto_iInf, tendsto_principal, mem_Iic, le_principal_iff]
[GOAL]
ι : Sort u_1
α : Type u_2
β : Type u_3
X : Type u_4
Y : Type u_5
inst✝ : TopologicalSpace X
x : X
⊢ 𝓝 (𝓝 x) = ⨅ (s : Set X) (_ : IsOpen s) (_ : x ∈ s), 𝓟 (Iic (𝓟 s))
[PROOFSTEP]
simp only [(nhds_basis_opens x).nhds.eq_biInf, iInf_and, @iInf_comm _ (_ ∈ _)]
[GOAL]
ι : Sort u_1
α : Type u_2
β : Type u_3
X : Type u_4
Y : Type u_5
inst✝ : TopologicalSpace X
x : X
⊢ ⨅ (s : Set X) (_ : IsOpen s) (_ : x ∈ s), 𝓟 s = comap 𝓝 (𝓝 (𝓝 x))
[PROOFSTEP]
simp (config := { contextual := true }) only [nhds_nhds, comap_iInf, comap_principal, Iic_principal, preimage_setOf_eq,
  ← mem_interior_iff_mem_nhds, setOf_mem_eq, IsOpen.interior_eq]


[GOAL]
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
i j : ℕ
a : (⨂[R]^i) M
b : (⨂[R]^j) M
⊢ ↑toTensorAlgebra (GradedMonoid.GMul.mul a b) = ↑toTensorAlgebra a * ↑toTensorAlgebra b
[PROOFSTEP]
rw [TensorPower.gMul_eq_coe_linearMap, ← LinearMap.compr₂_apply, ← @LinearMap.mul_apply' R, ← LinearMap.compl₂_apply, ←
  LinearMap.comp_apply]
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
i j : ℕ
a : (⨂[R]^i) M
b : (⨂[R]^j) M
⊢ ↑(↑(LinearMap.compr₂ (LinearMap.compr₂ (TensorProduct.mk R ((⨂[R]^i) M) ((⨂[R]^j) M)) ↑mulEquiv) toTensorAlgebra) a)
      b =
    ↑(↑(LinearMap.comp (LinearMap.compl₂ (LinearMap.mul R ((fun x => TensorAlgebra R M) a)) toTensorAlgebra)
              toTensorAlgebra)
          a)
      b
[PROOFSTEP]
refine' LinearMap.congr_fun (LinearMap.congr_fun _ a) b
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
i j : ℕ
a : (⨂[R]^i) M
b : (⨂[R]^j) M
⊢ LinearMap.compr₂ (LinearMap.compr₂ (TensorProduct.mk R ((⨂[R]^i) M) ((⨂[R]^j) M)) ↑mulEquiv) toTensorAlgebra =
    LinearMap.comp (LinearMap.compl₂ (LinearMap.mul R ((fun x => TensorAlgebra R M) a)) toTensorAlgebra) toTensorAlgebra
[PROOFSTEP]
clear! a b
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
i j : ℕ
a : (⨂[R]^i) M
⊢ LinearMap.compr₂ (LinearMap.compr₂ (TensorProduct.mk R ((⨂[R]^i) M) ((⨂[R]^j) M)) ↑mulEquiv) toTensorAlgebra =
    LinearMap.comp (LinearMap.compl₂ (LinearMap.mul R ((fun x => TensorAlgebra R M) a)) toTensorAlgebra) toTensorAlgebra
[PROOFSTEP]
ext
  (a b)
    -- Porting note: pulled the next two lines out of the long `simp only` below.
[GOAL]
case H.H.H.H
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
i j : ℕ
a✝ : (⨂[R]^i) M
a : Fin i → M
b : Fin j → M
⊢ ↑(LinearMap.compMultilinearMap
          (↑(LinearMap.compMultilinearMap
                (LinearMap.compr₂ (LinearMap.compr₂ (TensorProduct.mk R ((⨂[R]^i) M) ((⨂[R]^j) M)) ↑mulEquiv)
                  toTensorAlgebra)
                (PiTensorProduct.tprod R))
            a)
          (PiTensorProduct.tprod R))
      b =
    ↑(LinearMap.compMultilinearMap
          (↑(LinearMap.compMultilinearMap
                (LinearMap.comp (LinearMap.compl₂ (LinearMap.mul R ((fun x => TensorAlgebra R M) a✝)) toTensorAlgebra)
                  toTensorAlgebra)
                (PiTensorProduct.tprod R))
            a)
          (PiTensorProduct.tprod R))
      b
[PROOFSTEP]
simp only [LinearMap.compMultilinearMap_apply]
[GOAL]
case H.H.H.H
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
i j : ℕ
a✝ : (⨂[R]^i) M
a : Fin i → M
b : Fin j → M
⊢ ↑(↑(LinearMap.compr₂ (LinearMap.compr₂ (TensorProduct.mk R ((⨂[R]^i) M) ((⨂[R]^j) M)) ↑mulEquiv) toTensorAlgebra)
          (↑(PiTensorProduct.tprod R) a))
      (↑(PiTensorProduct.tprod R) b) =
    ↑(↑(LinearMap.comp (LinearMap.compl₂ (LinearMap.mul R ((fun x => TensorAlgebra R M) a✝)) toTensorAlgebra)
              toTensorAlgebra)
          (↑(PiTensorProduct.tprod R) a))
      (↑(PiTensorProduct.tprod R) b)
[PROOFSTEP]
rw [LinearMap.compr₂_apply, ← gMul_eq_coe_linearMap]
[GOAL]
case H.H.H.H
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
i j : ℕ
a✝ : (⨂[R]^i) M
a : Fin i → M
b : Fin j → M
⊢ ↑toTensorAlgebra (GradedMonoid.GMul.mul (↑(PiTensorProduct.tprod R) a) (↑(PiTensorProduct.tprod R) b)) =
    ↑(↑(LinearMap.comp (LinearMap.compl₂ (LinearMap.mul R ((fun x => TensorAlgebra R M) a✝)) toTensorAlgebra)
              toTensorAlgebra)
          (↑(PiTensorProduct.tprod R) a))
      (↑(PiTensorProduct.tprod R) b)
[PROOFSTEP]
simp only [LinearMap.compr₂_apply, LinearMap.mul_apply', LinearMap.compl₂_apply, LinearMap.comp_apply,
  LinearMap.compMultilinearMap_apply, PiTensorProduct.lift.tprod, TensorPower.tprod_mul_tprod,
  TensorPower.toTensorAlgebra_tprod, TensorAlgebra.tprod_apply, ← gMul_eq_coe_linearMap]
[GOAL]
case H.H.H.H
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
i j : ℕ
a✝ : (⨂[R]^i) M
a : Fin i → M
b : Fin j → M
⊢ List.prod (List.ofFn fun i_1 => ↑(TensorAlgebra.ι R) (Fin.append a b i_1)) =
    List.prod (List.ofFn fun i => ↑(TensorAlgebra.ι R) (a i)) *
      List.prod (List.ofFn fun i => ↑(TensorAlgebra.ι R) (b i))
[PROOFSTEP]
refine' Eq.trans _ List.prod_append
[GOAL]
case H.H.H.H
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
i j : ℕ
a✝ : (⨂[R]^i) M
a : Fin i → M
b : Fin j → M
⊢ List.prod (List.ofFn fun i_1 => ↑(TensorAlgebra.ι R) (Fin.append a b i_1)) =
    List.prod ((List.ofFn fun i => ↑(TensorAlgebra.ι R) (a i)) ++ List.ofFn fun i => ↑(TensorAlgebra.ι R) (b i))
[PROOFSTEP]
apply congr_arg
[GOAL]
case H.H.H.H.h
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
i j : ℕ
a✝ : (⨂[R]^i) M
a : Fin i → M
b : Fin j → M
⊢ (List.ofFn fun i_1 => ↑(TensorAlgebra.ι R) (Fin.append a b i_1)) =
    (List.ofFn fun i => ↑(TensorAlgebra.ι R) (a i)) ++ List.ofFn fun i => ↑(TensorAlgebra.ι R) (b i)
[PROOFSTEP]
erw [← List.map_ofFn _ (TensorAlgebra.ι R), ← List.map_ofFn _ (TensorAlgebra.ι R), ←
  List.map_ofFn _ (TensorAlgebra.ι R), ← List.map_append, List.ofFn_fin_append]
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
r : R
⊢ ↑toTensorAlgebra (↑DirectSum.GAlgebra.toFun r) = ↑(algebraMap R (TensorAlgebra R M)) r
[PROOFSTEP]
rw [TensorPower.galgebra_toFun_def, TensorPower.algebraMap₀_eq_smul_one, LinearMap.map_smul,
  TensorPower.toTensorAlgebra_gOne, Algebra.algebraMap_eq_smul_one]
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
⊢ AlgHom.comp ofDirectSum toDirectSum = AlgHom.id R (TensorAlgebra R M)
[PROOFSTEP]
ext
[GOAL]
case w.h
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
x✝ : M
⊢ ↑(LinearMap.comp (AlgHom.toLinearMap (AlgHom.comp ofDirectSum toDirectSum)) (ι R)) x✝ =
    ↑(LinearMap.comp (AlgHom.toLinearMap (AlgHom.id R (TensorAlgebra R M))) (ι R)) x✝
[PROOFSTEP]
simp [DirectSum.lof_eq_of, tprod_apply]
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n m : ℕ
h : n = m
x : (⨂[R]^n) M
⊢ GradedMonoid.mk m (↑(PiTensorProduct.reindex R M (Fin.castIso h).toEquiv) x) = GradedMonoid.mk n x
[PROOFSTEP]
rw [Fin.castIso_to_equiv, mk_reindex_cast h]
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
x : Fin n → M
⊢ List.prod (List.map (fun a => GradedMonoid.mk 1 (⨂ₜ[R] (x_1 : Fin 1), x a)) (List.finRange n)) =
    GradedMonoid.mk n (↑(PiTensorProduct.tprod R) x)
[PROOFSTEP]
refine' Fin.consInduction _ _ x
[GOAL]
case refine'_1
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
x : Fin n → M
⊢ List.prod (List.map (fun a => GradedMonoid.mk 1 (⨂ₜ[R] (x : Fin 1), Fin.elim0 a)) (List.finRange 0)) =
    GradedMonoid.mk 0 (↑(PiTensorProduct.tprod R) Fin.elim0)
[PROOFSTEP]
clear x
[GOAL]
case refine'_2
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
x : Fin n → M
⊢ ∀ {n : ℕ} (x₀ : M) (x : Fin n → M),
    List.prod (List.map (fun a => GradedMonoid.mk 1 (⨂ₜ[R] (x_1 : Fin 1), x a)) (List.finRange n)) =
        GradedMonoid.mk n (↑(PiTensorProduct.tprod R) x) →
      List.prod (List.map (fun a => GradedMonoid.mk 1 (⨂ₜ[R] (x_1 : Fin 1), Fin.cons x₀ x a)) (List.finRange (n + 1))) =
        GradedMonoid.mk (n + 1) (↑(PiTensorProduct.tprod R) (Fin.cons x₀ x))
[PROOFSTEP]
clear x
[GOAL]
case refine'_1
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
⊢ List.prod (List.map (fun a => GradedMonoid.mk 1 (⨂ₜ[R] (x : Fin 1), Fin.elim0 a)) (List.finRange 0)) =
    GradedMonoid.mk 0 (↑(PiTensorProduct.tprod R) Fin.elim0)
[PROOFSTEP]
rw [List.finRange_zero, List.map_nil, List.prod_nil]
[GOAL]
case refine'_1
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
⊢ 1 = GradedMonoid.mk 0 (↑(PiTensorProduct.tprod R) Fin.elim0)
[PROOFSTEP]
rfl
[GOAL]
case refine'_2
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
⊢ ∀ {n : ℕ} (x₀ : M) (x : Fin n → M),
    List.prod (List.map (fun a => GradedMonoid.mk 1 (⨂ₜ[R] (x_1 : Fin 1), x a)) (List.finRange n)) =
        GradedMonoid.mk n (↑(PiTensorProduct.tprod R) x) →
      List.prod (List.map (fun a => GradedMonoid.mk 1 (⨂ₜ[R] (x_1 : Fin 1), Fin.cons x₀ x a)) (List.finRange (n + 1))) =
        GradedMonoid.mk (n + 1) (↑(PiTensorProduct.tprod R) (Fin.cons x₀ x))
[PROOFSTEP]
intro n x₀ x ih
[GOAL]
case refine'_2
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n✝ n : ℕ
x₀ : M
x : Fin n → M
ih :
  List.prod (List.map (fun a => GradedMonoid.mk 1 (⨂ₜ[R] (x_1 : Fin 1), x a)) (List.finRange n)) =
    GradedMonoid.mk n (↑(PiTensorProduct.tprod R) x)
⊢ List.prod (List.map (fun a => GradedMonoid.mk 1 (⨂ₜ[R] (x_1 : Fin 1), Fin.cons x₀ x a)) (List.finRange (n + 1))) =
    GradedMonoid.mk (n + 1) (↑(PiTensorProduct.tprod R) (Fin.cons x₀ x))
[PROOFSTEP]
rw [List.finRange_succ_eq_map, List.map_cons, List.prod_cons, List.map_map]
[GOAL]
case refine'_2
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n✝ n : ℕ
x₀ : M
x : Fin n → M
ih :
  List.prod (List.map (fun a => GradedMonoid.mk 1 (⨂ₜ[R] (x_1 : Fin 1), x a)) (List.finRange n)) =
    GradedMonoid.mk n (↑(PiTensorProduct.tprod R) x)
⊢ GradedMonoid.mk 1 (⨂ₜ[R] (x_1 : Fin 1), Fin.cons x₀ x 0) *
      List.prod
        (List.map ((fun a => GradedMonoid.mk 1 (⨂ₜ[R] (x_1 : Fin 1), Fin.cons x₀ x a)) ∘ Fin.succ) (List.finRange n)) =
    GradedMonoid.mk (n + 1) (↑(PiTensorProduct.tprod R) (Fin.cons x₀ x))
[PROOFSTEP]
simp_rw [Function.comp, Fin.cons_zero, Fin.cons_succ]
[GOAL]
case refine'_2
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n✝ n : ℕ
x₀ : M
x : Fin n → M
ih :
  List.prod (List.map (fun a => GradedMonoid.mk 1 (⨂ₜ[R] (x_1 : Fin 1), x a)) (List.finRange n)) =
    GradedMonoid.mk n (↑(PiTensorProduct.tprod R) x)
⊢ GradedMonoid.mk 1 (⨂ₜ[R] (x : Fin 1), x₀) *
      List.prod (List.map (fun x_1 => GradedMonoid.mk 1 (⨂ₜ[R] (x_2 : Fin 1), x x_1)) (List.finRange n)) =
    GradedMonoid.mk (n + 1) (↑(PiTensorProduct.tprod R) (Fin.cons x₀ x))
[PROOFSTEP]
rw [ih, GradedMonoid.mk_mul_mk, TensorPower.tprod_mul_tprod]
[GOAL]
case refine'_2
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n✝ n : ℕ
x₀ : M
x : Fin n → M
ih :
  List.prod (List.map (fun a => GradedMonoid.mk 1 (⨂ₜ[R] (x_1 : Fin 1), x a)) (List.finRange n)) =
    GradedMonoid.mk n (↑(PiTensorProduct.tprod R) x)
⊢ GradedMonoid.mk (1 + n) (↑(PiTensorProduct.tprod R) (Fin.append (fun x => x₀) x)) =
    GradedMonoid.mk (n + 1) (↑(PiTensorProduct.tprod R) (Fin.cons x₀ x))
[PROOFSTEP]
refine' TensorPower.gradedMonoid_eq_of_cast (add_comm _ _) _
[GOAL]
case refine'_2
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n✝ n : ℕ
x₀ : M
x : Fin n → M
ih :
  List.prod (List.map (fun a => GradedMonoid.mk 1 (⨂ₜ[R] (x_1 : Fin 1), x a)) (List.finRange n)) =
    GradedMonoid.mk n (↑(PiTensorProduct.tprod R) x)
⊢ ↑(TensorPower.cast R M (_ : 1 + n = n + 1))
      (GradedMonoid.mk (1 + n) (↑(PiTensorProduct.tprod R) (Fin.append (fun x => x₀) x))).snd =
    (GradedMonoid.mk (n + 1) (↑(PiTensorProduct.tprod R) (Fin.cons x₀ x))).snd
[PROOFSTEP]
dsimp only [GradedMonoid.mk]
[GOAL]
case refine'_2
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n✝ n : ℕ
x₀ : M
x : Fin n → M
ih :
  List.prod (List.map (fun a => GradedMonoid.mk 1 (⨂ₜ[R] (x_1 : Fin 1), x a)) (List.finRange n)) =
    GradedMonoid.mk n (↑(PiTensorProduct.tprod R) x)
⊢ ↑(TensorPower.cast R M (_ : 1 + n = n + 1)) (↑(PiTensorProduct.tprod R) (Fin.append (fun x => x₀) x)) =
    ↑(PiTensorProduct.tprod R) (Fin.cons x₀ x)
[PROOFSTEP]
rw [TensorPower.cast_tprod]
[GOAL]
case refine'_2
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n✝ n : ℕ
x₀ : M
x : Fin n → M
ih :
  List.prod (List.map (fun a => GradedMonoid.mk 1 (⨂ₜ[R] (x_1 : Fin 1), x a)) (List.finRange n)) =
    GradedMonoid.mk n (↑(PiTensorProduct.tprod R) x)
⊢ ↑(PiTensorProduct.tprod R) (Fin.append (fun x => x₀) x ∘ ↑(Fin.castIso (_ : n + 1 = 1 + n))) =
    ↑(PiTensorProduct.tprod R) (Fin.cons x₀ x)
[PROOFSTEP]
simp_rw [Fin.append_left_eq_cons, Function.comp]
[GOAL]
case refine'_2
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n✝ n : ℕ
x₀ : M
x : Fin n → M
ih :
  List.prod (List.map (fun a => GradedMonoid.mk 1 (⨂ₜ[R] (x_1 : Fin 1), x a)) (List.finRange n)) =
    GradedMonoid.mk n (↑(PiTensorProduct.tprod R) x)
⊢ (⨂ₜ[R] (x_1 : Fin (n + 1)),
      Fin.cons x₀ x (↑(Fin.castIso (_ : 1 + n = n + 1)) (↑(Fin.castIso (_ : n + 1 = 1 + n)) x_1))) =
    ↑(PiTensorProduct.tprod R) (Fin.cons x₀ x)
[PROOFSTEP]
congr 1 with i
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
x : Fin n → M
⊢ ↑toDirectSum (↑(tprod R M n) x) = ↑(DirectSum.of (fun i => (⨂[R]^i) M) n) (↑(PiTensorProduct.tprod R) x)
[PROOFSTEP]
rw [tprod_apply, AlgHom.map_list_prod, List.map_ofFn]
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
x : Fin n → M
⊢ List.prod (List.ofFn (↑toDirectSum ∘ fun i => ↑(ι R) (x i))) =
    ↑(DirectSum.of (fun i => (⨂[R]^i) M) n) (↑(PiTensorProduct.tprod R) x)
[PROOFSTEP]
simp_rw [Function.comp, toDirectSum_ι]
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
x : Fin n → M
⊢ List.prod (List.ofFn fun x_1 => ↑(DirectSum.of (fun n => (⨂[R]^n) M) 1) (⨂ₜ[R] (x_2 : Fin 1), x x_1)) =
    ↑(DirectSum.of (fun i => (⨂[R]^i) M) n) (↑(PiTensorProduct.tprod R) x)
[PROOFSTEP]
rw [DirectSum.list_prod_ofFn_of_eq_dProd]
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
x : Fin n → M
⊢ ↑(DirectSum.of (fun n => (⨂[R]^n) M) (List.dProdIndex (List.finRange n) fun x => 1))
      (List.dProd (List.finRange n) (fun x => 1) fun x_1 => ⨂ₜ[R] (x_2 : Fin 1), x x_1) =
    ↑(DirectSum.of (fun i => (⨂[R]^i) M) n) (↑(PiTensorProduct.tprod R) x)
[PROOFSTEP]
apply DirectSum.of_eq_of_gradedMonoid_eq
[GOAL]
case h
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
x : Fin n → M
⊢ GradedMonoid.mk (List.dProdIndex (List.finRange n) fun x => 1)
      (List.dProd (List.finRange n) (fun x => 1) fun x_1 => ⨂ₜ[R] (x_2 : Fin 1), x x_1) =
    GradedMonoid.mk n (↑(PiTensorProduct.tprod R) x)
[PROOFSTEP]
rw [GradedMonoid.mk_list_dProd]
[GOAL]
case h
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
x : Fin n → M
⊢ List.prod (List.map (fun a => GradedMonoid.mk 1 (⨂ₜ[R] (x_1 : Fin 1), x a)) (List.finRange n)) =
    GradedMonoid.mk n (↑(PiTensorProduct.tprod R) x)
[PROOFSTEP]
rw [TensorPower.list_prod_gradedMonoid_mk_single]
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
⊢ AlgHom.comp toDirectSum ofDirectSum = AlgHom.id R (⨁ (n : ℕ), (⨂[R]^n) M)
[PROOFSTEP]
ext
[GOAL]
case h.H.H
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
i✝ : ℕ
x✝ : Fin i✝ → M
⊢ ↑(LinearMap.compMultilinearMap
          (LinearMap.comp (AlgHom.toLinearMap (AlgHom.comp toDirectSum ofDirectSum))
            (DirectSum.lof R ℕ (fun i => (⨂[R]^i) M) i✝))
          (PiTensorProduct.tprod R))
      x✝ =
    ↑(LinearMap.compMultilinearMap
          (LinearMap.comp (AlgHom.toLinearMap (AlgHom.id R (⨁ (n : ℕ), (⨂[R]^n) M)))
            (DirectSum.lof R ℕ (fun i => (⨂[R]^i) M) i✝))
          (PiTensorProduct.tprod R))
      x✝
[PROOFSTEP]
simp [DirectSum.lof_eq_of, -tprod_apply, toDirectSum_tensorPower_tprod]


[GOAL]
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring S
inst✝⁶ : Semiring A
inst✝⁵ : Semiring B
inst✝⁴ : Algebra R S
inst✝³ : Algebra R A
inst✝² : Algebra R B
inst✝¹ : Algebra S A
inst✝ : IsScalarTower R S A
e₁ : Aᵐᵒᵖ ⊗[R] Bᵐᵒᵖ ≃ₗ[S] (A ⊗[R] B)ᵐᵒᵖ :=
  LinearEquiv.trans
    (TensorProduct.AlgebraTensorModule.congr (LinearEquiv.symm (opLinearEquiv S)) (LinearEquiv.symm (opLinearEquiv R)))
    (opLinearEquiv S)
e₂ : A ⊗[R] B ≃ₗ[S] (Aᵐᵒᵖ ⊗[R] Bᵐᵒᵖ)ᵐᵒᵖ :=
  LinearEquiv.trans (TensorProduct.AlgebraTensorModule.congr (opLinearEquiv S) (opLinearEquiv R)) (opLinearEquiv S)
⊢ ↑AlgHom.op.symm
      (AlgHom.comp
        (algHomOfLinearMapTensorProduct ↑e₁
          (_ :
            ∀ (a₁ a₂ : Aᵐᵒᵖ) (b₁ b₂ : Bᵐᵒᵖ), ↑↑e₁ ((a₁ * a₂) ⊗ₜ[R] (b₁ * b₂)) = ↑↑e₁ (a₁ ⊗ₜ[R] b₁) * ↑↑e₁ (a₂ ⊗ₜ[R] b₂))
          (_ : ∀ (r : S), ↑↑e₁ (↑(algebraMap S Aᵐᵒᵖ) r ⊗ₜ[R] 1) = ↑(algebraMap S (A ⊗[R] B)ᵐᵒᵖ) r))
        (↑AlgHom.opComm
          (algHomOfLinearMapTensorProduct ↑e₂
            (_ : ∀ (a₁ a₂ : A) (b₁ b₂ : B), ↑↑e₂ ((a₁ * a₂) ⊗ₜ[R] (b₁ * b₂)) = ↑↑e₂ (a₁ ⊗ₜ[R] b₁) * ↑↑e₂ (a₂ ⊗ₜ[R] b₂))
            (_ : ∀ (r : S), ↑↑e₂ (↑(algebraMap S A) r ⊗ₜ[R] 1) = ↑(algebraMap S (Aᵐᵒᵖ ⊗[R] Bᵐᵒᵖ)ᵐᵒᵖ) r)))) =
    ↑AlgHom.op.symm (AlgHom.id S (A ⊗[R] B)ᵐᵒᵖ)
[PROOFSTEP]
ext
[GOAL]
case ha.H
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring S
inst✝⁶ : Semiring A
inst✝⁵ : Semiring B
inst✝⁴ : Algebra R S
inst✝³ : Algebra R A
inst✝² : Algebra R B
inst✝¹ : Algebra S A
inst✝ : IsScalarTower R S A
e₁ : Aᵐᵒᵖ ⊗[R] Bᵐᵒᵖ ≃ₗ[S] (A ⊗[R] B)ᵐᵒᵖ :=
  LinearEquiv.trans
    (TensorProduct.AlgebraTensorModule.congr (LinearEquiv.symm (opLinearEquiv S)) (LinearEquiv.symm (opLinearEquiv R)))
    (opLinearEquiv S)
e₂ : A ⊗[R] B ≃ₗ[S] (Aᵐᵒᵖ ⊗[R] Bᵐᵒᵖ)ᵐᵒᵖ :=
  LinearEquiv.trans (TensorProduct.AlgebraTensorModule.congr (opLinearEquiv S) (opLinearEquiv R)) (opLinearEquiv S)
x✝ : A
⊢ ↑(AlgHom.comp
          (↑AlgHom.op.symm
            (AlgHom.comp
              (algHomOfLinearMapTensorProduct ↑e₁
                (_ :
                  ∀ (a₁ a₂ : Aᵐᵒᵖ) (b₁ b₂ : Bᵐᵒᵖ),
                    ↑↑e₁ ((a₁ * a₂) ⊗ₜ[R] (b₁ * b₂)) = ↑↑e₁ (a₁ ⊗ₜ[R] b₁) * ↑↑e₁ (a₂ ⊗ₜ[R] b₂))
                (_ : ∀ (r : S), ↑↑e₁ (↑(algebraMap S Aᵐᵒᵖ) r ⊗ₜ[R] 1) = ↑(algebraMap S (A ⊗[R] B)ᵐᵒᵖ) r))
              (↑AlgHom.opComm
                (algHomOfLinearMapTensorProduct ↑e₂
                  (_ :
                    ∀ (a₁ a₂ : A) (b₁ b₂ : B),
                      ↑↑e₂ ((a₁ * a₂) ⊗ₜ[R] (b₁ * b₂)) = ↑↑e₂ (a₁ ⊗ₜ[R] b₁) * ↑↑e₂ (a₂ ⊗ₜ[R] b₂))
                  (_ : ∀ (r : S), ↑↑e₂ (↑(algebraMap S A) r ⊗ₜ[R] 1) = ↑(algebraMap S (Aᵐᵒᵖ ⊗[R] Bᵐᵒᵖ)ᵐᵒᵖ) r)))))
          includeLeft)
      x✝ =
    ↑(AlgHom.comp (↑AlgHom.op.symm (AlgHom.id S (A ⊗[R] B)ᵐᵒᵖ)) includeLeft) x✝
[PROOFSTEP]
rfl
[GOAL]
case hb.H
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring S
inst✝⁶ : Semiring A
inst✝⁵ : Semiring B
inst✝⁴ : Algebra R S
inst✝³ : Algebra R A
inst✝² : Algebra R B
inst✝¹ : Algebra S A
inst✝ : IsScalarTower R S A
e₁ : Aᵐᵒᵖ ⊗[R] Bᵐᵒᵖ ≃ₗ[S] (A ⊗[R] B)ᵐᵒᵖ :=
  LinearEquiv.trans
    (TensorProduct.AlgebraTensorModule.congr (LinearEquiv.symm (opLinearEquiv S)) (LinearEquiv.symm (opLinearEquiv R)))
    (opLinearEquiv S)
e₂ : A ⊗[R] B ≃ₗ[S] (Aᵐᵒᵖ ⊗[R] Bᵐᵒᵖ)ᵐᵒᵖ :=
  LinearEquiv.trans (TensorProduct.AlgebraTensorModule.congr (opLinearEquiv S) (opLinearEquiv R)) (opLinearEquiv S)
x✝ : B
⊢ ↑(AlgHom.comp
          (AlgHom.restrictScalars R
            (↑AlgHom.op.symm
              (AlgHom.comp
                (algHomOfLinearMapTensorProduct ↑e₁
                  (_ :
                    ∀ (a₁ a₂ : Aᵐᵒᵖ) (b₁ b₂ : Bᵐᵒᵖ),
                      ↑↑e₁ ((a₁ * a₂) ⊗ₜ[R] (b₁ * b₂)) = ↑↑e₁ (a₁ ⊗ₜ[R] b₁) * ↑↑e₁ (a₂ ⊗ₜ[R] b₂))
                  (_ : ∀ (r : S), ↑↑e₁ (↑(algebraMap S Aᵐᵒᵖ) r ⊗ₜ[R] 1) = ↑(algebraMap S (A ⊗[R] B)ᵐᵒᵖ) r))
                (↑AlgHom.opComm
                  (algHomOfLinearMapTensorProduct ↑e₂
                    (_ :
                      ∀ (a₁ a₂ : A) (b₁ b₂ : B),
                        ↑↑e₂ ((a₁ * a₂) ⊗ₜ[R] (b₁ * b₂)) = ↑↑e₂ (a₁ ⊗ₜ[R] b₁) * ↑↑e₂ (a₂ ⊗ₜ[R] b₂))
                    (_ : ∀ (r : S), ↑↑e₂ (↑(algebraMap S A) r ⊗ₜ[R] 1) = ↑(algebraMap S (Aᵐᵒᵖ ⊗[R] Bᵐᵒᵖ)ᵐᵒᵖ) r))))))
          includeRight)
      x✝ =
    ↑(AlgHom.comp (AlgHom.restrictScalars R (↑AlgHom.op.symm (AlgHom.id S (A ⊗[R] B)ᵐᵒᵖ))) includeRight) x✝
[PROOFSTEP]
rfl
[GOAL]
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring S
inst✝⁶ : Semiring A
inst✝⁵ : Semiring B
inst✝⁴ : Algebra R S
inst✝³ : Algebra R A
inst✝² : Algebra R B
inst✝¹ : Algebra S A
inst✝ : IsScalarTower R S A
e₁ : Aᵐᵒᵖ ⊗[R] Bᵐᵒᵖ ≃ₗ[S] (A ⊗[R] B)ᵐᵒᵖ :=
  LinearEquiv.trans
    (TensorProduct.AlgebraTensorModule.congr (LinearEquiv.symm (opLinearEquiv S)) (LinearEquiv.symm (opLinearEquiv R)))
    (opLinearEquiv S)
e₂ : A ⊗[R] B ≃ₗ[S] (Aᵐᵒᵖ ⊗[R] Bᵐᵒᵖ)ᵐᵒᵖ :=
  LinearEquiv.trans (TensorProduct.AlgebraTensorModule.congr (opLinearEquiv S) (opLinearEquiv R)) (opLinearEquiv S)
⊢ AlgHom.comp
      (↑AlgHom.opComm
        (algHomOfLinearMapTensorProduct ↑e₂
          (_ : ∀ (a₁ a₂ : A) (b₁ b₂ : B), ↑↑e₂ ((a₁ * a₂) ⊗ₜ[R] (b₁ * b₂)) = ↑↑e₂ (a₁ ⊗ₜ[R] b₁) * ↑↑e₂ (a₂ ⊗ₜ[R] b₂))
          (_ : ∀ (r : S), ↑↑e₂ (↑(algebraMap S A) r ⊗ₜ[R] 1) = ↑(algebraMap S (Aᵐᵒᵖ ⊗[R] Bᵐᵒᵖ)ᵐᵒᵖ) r)))
      (algHomOfLinearMapTensorProduct ↑e₁
        (_ :
          ∀ (a₁ a₂ : Aᵐᵒᵖ) (b₁ b₂ : Bᵐᵒᵖ), ↑↑e₁ ((a₁ * a₂) ⊗ₜ[R] (b₁ * b₂)) = ↑↑e₁ (a₁ ⊗ₜ[R] b₁) * ↑↑e₁ (a₂ ⊗ₜ[R] b₂))
        (_ : ∀ (r : S), ↑↑e₁ (↑(algebraMap S Aᵐᵒᵖ) r ⊗ₜ[R] 1) = ↑(algebraMap S (A ⊗[R] B)ᵐᵒᵖ) r)) =
    AlgHom.id S (Aᵐᵒᵖ ⊗[R] Bᵐᵒᵖ)
[PROOFSTEP]
ext
[GOAL]
case ha.H
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring S
inst✝⁶ : Semiring A
inst✝⁵ : Semiring B
inst✝⁴ : Algebra R S
inst✝³ : Algebra R A
inst✝² : Algebra R B
inst✝¹ : Algebra S A
inst✝ : IsScalarTower R S A
e₁ : Aᵐᵒᵖ ⊗[R] Bᵐᵒᵖ ≃ₗ[S] (A ⊗[R] B)ᵐᵒᵖ :=
  LinearEquiv.trans
    (TensorProduct.AlgebraTensorModule.congr (LinearEquiv.symm (opLinearEquiv S)) (LinearEquiv.symm (opLinearEquiv R)))
    (opLinearEquiv S)
e₂ : A ⊗[R] B ≃ₗ[S] (Aᵐᵒᵖ ⊗[R] Bᵐᵒᵖ)ᵐᵒᵖ :=
  LinearEquiv.trans (TensorProduct.AlgebraTensorModule.congr (opLinearEquiv S) (opLinearEquiv R)) (opLinearEquiv S)
x✝ : Aᵐᵒᵖ
⊢ ↑(AlgHom.comp
          (AlgHom.comp
            (↑AlgHom.opComm
              (algHomOfLinearMapTensorProduct ↑e₂
                (_ :
                  ∀ (a₁ a₂ : A) (b₁ b₂ : B), ↑↑e₂ ((a₁ * a₂) ⊗ₜ[R] (b₁ * b₂)) = ↑↑e₂ (a₁ ⊗ₜ[R] b₁) * ↑↑e₂ (a₂ ⊗ₜ[R] b₂))
                (_ : ∀ (r : S), ↑↑e₂ (↑(algebraMap S A) r ⊗ₜ[R] 1) = ↑(algebraMap S (Aᵐᵒᵖ ⊗[R] Bᵐᵒᵖ)ᵐᵒᵖ) r)))
            (algHomOfLinearMapTensorProduct ↑e₁
              (_ :
                ∀ (a₁ a₂ : Aᵐᵒᵖ) (b₁ b₂ : Bᵐᵒᵖ),
                  ↑↑e₁ ((a₁ * a₂) ⊗ₜ[R] (b₁ * b₂)) = ↑↑e₁ (a₁ ⊗ₜ[R] b₁) * ↑↑e₁ (a₂ ⊗ₜ[R] b₂))
              (_ : ∀ (r : S), ↑↑e₁ (↑(algebraMap S Aᵐᵒᵖ) r ⊗ₜ[R] 1) = ↑(algebraMap S (A ⊗[R] B)ᵐᵒᵖ) r)))
          includeLeft)
      x✝ =
    ↑(AlgHom.comp (AlgHom.id S (Aᵐᵒᵖ ⊗[R] Bᵐᵒᵖ)) includeLeft) x✝
[PROOFSTEP]
rfl
[GOAL]
case hb.H
R : Type u_1
S : Type u_2
A : Type u_3
B : Type u_4
inst✝⁸ : CommSemiring R
inst✝⁷ : CommSemiring S
inst✝⁶ : Semiring A
inst✝⁵ : Semiring B
inst✝⁴ : Algebra R S
inst✝³ : Algebra R A
inst✝² : Algebra R B
inst✝¹ : Algebra S A
inst✝ : IsScalarTower R S A
e₁ : Aᵐᵒᵖ ⊗[R] Bᵐᵒᵖ ≃ₗ[S] (A ⊗[R] B)ᵐᵒᵖ :=
  LinearEquiv.trans
    (TensorProduct.AlgebraTensorModule.congr (LinearEquiv.symm (opLinearEquiv S)) (LinearEquiv.symm (opLinearEquiv R)))
    (opLinearEquiv S)
e₂ : A ⊗[R] B ≃ₗ[S] (Aᵐᵒᵖ ⊗[R] Bᵐᵒᵖ)ᵐᵒᵖ :=
  LinearEquiv.trans (TensorProduct.AlgebraTensorModule.congr (opLinearEquiv S) (opLinearEquiv R)) (opLinearEquiv S)
x✝ : Bᵐᵒᵖ
⊢ ↑(AlgHom.comp
          (AlgHom.restrictScalars R
            (AlgHom.comp
              (↑AlgHom.opComm
                (algHomOfLinearMapTensorProduct ↑e₂
                  (_ :
                    ∀ (a₁ a₂ : A) (b₁ b₂ : B),
                      ↑↑e₂ ((a₁ * a₂) ⊗ₜ[R] (b₁ * b₂)) = ↑↑e₂ (a₁ ⊗ₜ[R] b₁) * ↑↑e₂ (a₂ ⊗ₜ[R] b₂))
                  (_ : ∀ (r : S), ↑↑e₂ (↑(algebraMap S A) r ⊗ₜ[R] 1) = ↑(algebraMap S (Aᵐᵒᵖ ⊗[R] Bᵐᵒᵖ)ᵐᵒᵖ) r)))
              (algHomOfLinearMapTensorProduct ↑e₁
                (_ :
                  ∀ (a₁ a₂ : Aᵐᵒᵖ) (b₁ b₂ : Bᵐᵒᵖ),
                    ↑↑e₁ ((a₁ * a₂) ⊗ₜ[R] (b₁ * b₂)) = ↑↑e₁ (a₁ ⊗ₜ[R] b₁) * ↑↑e₁ (a₂ ⊗ₜ[R] b₂))
                (_ : ∀ (r : S), ↑↑e₁ (↑(algebraMap S Aᵐᵒᵖ) r ⊗ₜ[R] 1) = ↑(algebraMap S (A ⊗[R] B)ᵐᵒᵖ) r))))
          includeRight)
      x✝ =
    ↑(AlgHom.comp (AlgHom.restrictScalars R (AlgHom.id S (Aᵐᵒᵖ ⊗[R] Bᵐᵒᵖ))) includeRight) x✝
[PROOFSTEP]
rfl


[GOAL]
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
c : CU X
n : ℕ
x : X
hx : x ∈ c.C
⊢ approx n c x = 0
[PROOFSTEP]
induction' n with n ihn generalizing c
[GOAL]
case zero
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
c✝ : CU X
x : X
hx✝ : x ∈ c✝.C
c : CU X
hx : x ∈ c.C
⊢ approx Nat.zero c x = 0
[PROOFSTEP]
exact indicator_of_not_mem (fun (hU : x ∈ c.Uᶜ) => hU <| c.subset hx) _
[GOAL]
case succ
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
c✝ : CU X
x : X
hx✝ : x ∈ c✝.C
n : ℕ
ihn : ∀ (c : CU X), x ∈ c.C → approx n c x = 0
c : CU X
hx : x ∈ c.C
⊢ approx (Nat.succ n) c x = 0
[PROOFSTEP]
simp only [approx]
[GOAL]
case succ
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
c✝ : CU X
x : X
hx✝ : x ∈ c✝.C
n : ℕ
ihn : ∀ (c : CU X), x ∈ c.C → approx n c x = 0
c : CU X
hx : x ∈ c.C
⊢ midpoint ℝ (approx n (left c) x) (approx n (right c) x) = 0
[PROOFSTEP]
rw [ihn, ihn, midpoint_self]
[GOAL]
case succ.hx
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
c✝ : CU X
x : X
hx✝ : x ∈ c✝.C
n : ℕ
ihn : ∀ (c : CU X), x ∈ c.C → approx n c x = 0
c : CU X
hx : x ∈ c.C
⊢ x ∈ (right c).C
case succ.hx
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
c✝ : CU X
x : X
hx✝ : x ∈ c✝.C
n : ℕ
ihn : ∀ (c : CU X), x ∈ c.C → approx n c x = 0
c : CU X
hx : x ∈ c.C
⊢ x ∈ (left c).C
[PROOFSTEP]
exacts [c.subset_right_C hx, hx]
[GOAL]
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
c : CU X
n : ℕ
x : X
hx : ¬x ∈ c.U
⊢ approx n c x = 1
[PROOFSTEP]
induction' n with n ihn generalizing c
[GOAL]
case zero
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
c✝ : CU X
x : X
hx✝ : ¬x ∈ c✝.U
c : CU X
hx : ¬x ∈ c.U
⊢ approx Nat.zero c x = 1
[PROOFSTEP]
rw [← mem_compl_iff] at hx
[GOAL]
case zero
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
c✝ : CU X
x : X
hx✝ : ¬x ∈ c✝.U
c : CU X
hx : x ∈ c.Uᶜ
⊢ approx Nat.zero c x = 1
[PROOFSTEP]
exact indicator_of_mem hx _
[GOAL]
case succ
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
c✝ : CU X
x : X
hx✝ : ¬x ∈ c✝.U
n : ℕ
ihn : ∀ (c : CU X), ¬x ∈ c.U → approx n c x = 1
c : CU X
hx : ¬x ∈ c.U
⊢ approx (Nat.succ n) c x = 1
[PROOFSTEP]
simp only [approx]
[GOAL]
case succ
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
c✝ : CU X
x : X
hx✝ : ¬x ∈ c✝.U
n : ℕ
ihn : ∀ (c : CU X), ¬x ∈ c.U → approx n c x = 1
c : CU X
hx : ¬x ∈ c.U
⊢ midpoint ℝ (approx n (left c) x) (approx n (right c) x) = 1
[PROOFSTEP]
rw [ihn, ihn, midpoint_self]
[GOAL]
case succ.hx
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
c✝ : CU X
x : X
hx✝ : ¬x ∈ c✝.U
n : ℕ
ihn : ∀ (c : CU X), ¬x ∈ c.U → approx n c x = 1
c : CU X
hx : ¬x ∈ c.U
⊢ ¬x ∈ (right c).U
case succ.hx
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
c✝ : CU X
x : X
hx✝ : ¬x ∈ c✝.U
n : ℕ
ihn : ∀ (c : CU X), ¬x ∈ c.U → approx n c x = 1
c : CU X
hx : ¬x ∈ c.U
⊢ ¬x ∈ (left c).U
[PROOFSTEP]
exacts [hx, fun hU => hx <| c.left_U_subset hU]
[GOAL]
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
c : CU X
n : ℕ
x : X
⊢ 0 ≤ approx n c x
[PROOFSTEP]
induction' n with n ihn generalizing c
[GOAL]
case zero
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
c✝ : CU X
x : X
c : CU X
⊢ 0 ≤ approx Nat.zero c x
[PROOFSTEP]
exact indicator_nonneg (fun _ _ => zero_le_one) _
[GOAL]
case succ
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
c✝ : CU X
x : X
n : ℕ
ihn : ∀ (c : CU X), 0 ≤ approx n c x
c : CU X
⊢ 0 ≤ approx (Nat.succ n) c x
[PROOFSTEP]
simp only [approx, midpoint_eq_smul_add, invOf_eq_inv]
[GOAL]
case succ
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
c✝ : CU X
x : X
n : ℕ
ihn : ∀ (c : CU X), 0 ≤ approx n c x
c : CU X
⊢ 0 ≤ 2⁻¹ • (approx n (left c) x + approx n (right c) x)
[PROOFSTEP]
refine' mul_nonneg (inv_nonneg.2 zero_le_two) (add_nonneg _ _)
[GOAL]
case succ.refine'_1
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
c✝ : CU X
x : X
n : ℕ
ihn : ∀ (c : CU X), 0 ≤ approx n c x
c : CU X
⊢ 0 ≤ approx n (left c) x
[PROOFSTEP]
apply ihn
[GOAL]
case succ.refine'_2
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
c✝ : CU X
x : X
n : ℕ
ihn : ∀ (c : CU X), 0 ≤ approx n c x
c : CU X
⊢ 0 ≤ approx n (right c) x
[PROOFSTEP]
apply ihn
[GOAL]
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
c : CU X
n : ℕ
x : X
⊢ approx n c x ≤ 1
[PROOFSTEP]
induction' n with n ihn generalizing c
[GOAL]
case zero
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
c✝ : CU X
x : X
c : CU X
⊢ approx Nat.zero c x ≤ 1
[PROOFSTEP]
exact indicator_apply_le' (fun _ => le_rfl) fun _ => zero_le_one
[GOAL]
case succ
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
c✝ : CU X
x : X
n : ℕ
ihn : ∀ (c : CU X), approx n c x ≤ 1
c : CU X
⊢ approx (Nat.succ n) c x ≤ 1
[PROOFSTEP]
simp only [approx, midpoint_eq_smul_add, invOf_eq_inv, smul_eq_mul, ← div_eq_inv_mul]
[GOAL]
case succ
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
c✝ : CU X
x : X
n : ℕ
ihn : ∀ (c : CU X), approx n c x ≤ 1
c : CU X
⊢ (approx n (left c) x + approx n (right c) x) / 2 ≤ 1
[PROOFSTEP]
have := add_le_add (ihn (left c)) (ihn (right c))
[GOAL]
case succ
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
c✝ : CU X
x : X
n : ℕ
ihn : ∀ (c : CU X), approx n c x ≤ 1
c : CU X
this : approx n (left c) x + approx n (right c) x ≤ 1 + 1
⊢ (approx n (left c) x + approx n (right c) x) / 2 ≤ 1
[PROOFSTEP]
norm_num at this
[GOAL]
case succ
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
c✝ : CU X
x : X
n : ℕ
ihn : ∀ (c : CU X), approx n c x ≤ 1
c : CU X
this : approx n (left c) x + approx n (right c) x ≤ 2
⊢ (approx n (left c) x + approx n (right c) x) / 2 ≤ 1
[PROOFSTEP]
exact Iff.mpr (div_le_one zero_lt_two) this
[GOAL]
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
c₁ c₂ : CU X
h : c₁.U ⊆ c₂.C
n₁ n₂ : ℕ
x : X
⊢ approx n₂ c₂ x ≤ approx n₁ c₁ x
[PROOFSTEP]
by_cases hx : x ∈ c₁.U
[GOAL]
case pos
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
c₁ c₂ : CU X
h : c₁.U ⊆ c₂.C
n₁ n₂ : ℕ
x : X
hx : x ∈ c₁.U
⊢ approx n₂ c₂ x ≤ approx n₁ c₁ x
[PROOFSTEP]
calc
  approx n₂ c₂ x = 0 := approx_of_mem_C _ _ (h hx)
  _ ≤ approx n₁ c₁ x := approx_nonneg _ _ _
[GOAL]
case neg
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
c₁ c₂ : CU X
h : c₁.U ⊆ c₂.C
n₁ n₂ : ℕ
x : X
hx : ¬x ∈ c₁.U
⊢ approx n₂ c₂ x ≤ approx n₁ c₁ x
[PROOFSTEP]
calc
  approx n₂ c₂ x ≤ 1 := approx_le_one _ _ _
  _ = approx n₁ c₁ x := (approx_of_nmem_U _ _ hx).symm
[GOAL]
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
c : CU X
n : ℕ
x : X
⊢ approx n c x ∈ Icc (approx n (right c) x) (approx n (left c) x)
[PROOFSTEP]
induction' n with n ihn generalizing c
[GOAL]
case zero
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
c✝ : CU X
x : X
c : CU X
⊢ approx Nat.zero c x ∈ Icc (approx Nat.zero (right c) x) (approx Nat.zero (left c) x)
[PROOFSTEP]
exact ⟨le_rfl, indicator_le_indicator_of_subset (compl_subset_compl.2 c.left_U_subset) (fun _ => zero_le_one) _⟩
[GOAL]
case succ
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
c✝ : CU X
x : X
n : ℕ
ihn : ∀ (c : CU X), approx n c x ∈ Icc (approx n (right c) x) (approx n (left c) x)
c : CU X
⊢ approx (Nat.succ n) c x ∈ Icc (approx (Nat.succ n) (right c) x) (approx (Nat.succ n) (left c) x)
[PROOFSTEP]
simp only [approx, mem_Icc]
[GOAL]
case succ
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
c✝ : CU X
x : X
n : ℕ
ihn : ∀ (c : CU X), approx n c x ∈ Icc (approx n (right c) x) (approx n (left c) x)
c : CU X
⊢ midpoint ℝ (approx n (left (right c)) x) (approx n (right (right c)) x) ≤
      midpoint ℝ (approx n (left c) x) (approx n (right c) x) ∧
    midpoint ℝ (approx n (left c) x) (approx n (right c) x) ≤
      midpoint ℝ (approx n (left (left c)) x) (approx n (right (left c)) x)
[PROOFSTEP]
refine' ⟨midpoint_le_midpoint _ (ihn _).1, midpoint_le_midpoint (ihn _).2 _⟩
[GOAL]
case succ.refine'_1
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
c✝ : CU X
x : X
n : ℕ
ihn : ∀ (c : CU X), approx n c x ∈ Icc (approx n (right c) x) (approx n (left c) x)
c : CU X
⊢ approx n (left (right c)) x ≤ approx n (left c) x
[PROOFSTEP]
apply approx_le_approx_of_U_sub_C
[GOAL]
case succ.refine'_2
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
c✝ : CU X
x : X
n : ℕ
ihn : ∀ (c : CU X), approx n c x ∈ Icc (approx n (right c) x) (approx n (left c) x)
c : CU X
⊢ approx n (right c) x ≤ approx n (right (left c)) x
[PROOFSTEP]
apply approx_le_approx_of_U_sub_C
[GOAL]
case succ.refine'_1.h
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
c✝ : CU X
x : X
n : ℕ
ihn : ∀ (c : CU X), approx n c x ∈ Icc (approx n (right c) x) (approx n (left c) x)
c : CU X
⊢ (left c).U ⊆ (left (right c)).C
case succ.refine'_2.h
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
c✝ : CU X
x : X
n : ℕ
ihn : ∀ (c : CU X), approx n c x ∈ Icc (approx n (right c) x) (approx n (left c) x)
c : CU X
⊢ (right (left c)).U ⊆ (right c).C
[PROOFSTEP]
exacts [subset_closure, subset_closure]
[GOAL]
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
c : CU X
n : ℕ
x : X
⊢ approx n c x ≤ approx (n + 1) c x
[PROOFSTEP]
induction' n with n ihn generalizing c
[GOAL]
case zero
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
c✝ : CU X
x : X
c : CU X
⊢ approx Nat.zero c x ≤ approx (Nat.zero + 1) c x
[PROOFSTEP]
simp only [approx, right_U, right_le_midpoint]
[GOAL]
case zero
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
c✝ : CU X
x : X
c : CU X
⊢ indicator c.Uᶜ 1 x ≤ indicator (left c).Uᶜ 1 x
[PROOFSTEP]
exact (approx_mem_Icc_right_left c 0 x).2
[GOAL]
case succ
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
c✝ : CU X
x : X
n : ℕ
ihn : ∀ (c : CU X), approx n c x ≤ approx (n + 1) c x
c : CU X
⊢ approx (Nat.succ n) c x ≤ approx (Nat.succ n + 1) c x
[PROOFSTEP]
rw [approx, approx]
[GOAL]
case succ
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
c✝ : CU X
x : X
n : ℕ
ihn : ∀ (c : CU X), approx n c x ≤ approx (n + 1) c x
c : CU X
⊢ midpoint ℝ (approx n (left c) x) (approx n (right c) x) ≤
    midpoint ℝ (approx (n + 1) (left c) x) (approx (n + 1) (right c) x)
[PROOFSTEP]
exact midpoint_le_midpoint (ihn _) (ihn _)
[GOAL]
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
c : CU X
x : X
h : x ∈ c.C
⊢ CU.lim c x = 0
[PROOFSTEP]
simp only [CU.lim, approx_of_mem_C, h, ciSup_const]
[GOAL]
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
c : CU X
x : X
h : ¬x ∈ c.U
⊢ CU.lim c x = 1
[PROOFSTEP]
simp only [CU.lim, approx_of_nmem_U c _ h, ciSup_const]
[GOAL]
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
c : CU X
x : X
⊢ CU.lim c x = midpoint ℝ (CU.lim (left c) x) (CU.lim (right c) x)
[PROOFSTEP]
refine' tendsto_nhds_unique (c.tendsto_approx_atTop x) ((tendsto_add_atTop_iff_nat 1).1 _)
[GOAL]
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
c : CU X
x : X
⊢ Tendsto (fun n => approx (n + 1) c x) atTop (𝓝 (midpoint ℝ (CU.lim (left c) x) (CU.lim (right c) x)))
[PROOFSTEP]
simp only [approx]
[GOAL]
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
c : CU X
x : X
⊢ Tendsto (fun n => midpoint ℝ (approx (Nat.add n 0) (left c) x) (approx (Nat.add n 0) (right c) x)) atTop
    (𝓝 (midpoint ℝ (CU.lim (left c) x) (CU.lim (right c) x)))
[PROOFSTEP]
exact (c.left.tendsto_approx_atTop x).midpoint (c.right.tendsto_approx_atTop x)
[GOAL]
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
c : CU X
⊢ Continuous (CU.lim c)
[PROOFSTEP]
obtain ⟨h0, h1234, h1⟩ : 0 < (2⁻¹ : ℝ) ∧ (2⁻¹ : ℝ) < 3 / 4 ∧ (3 / 4 : ℝ) < 1 := by norm_num
[GOAL]
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
c : CU X
⊢ 0 < 2⁻¹ ∧ 2⁻¹ < 3 / 4 ∧ 3 / 4 < 1
[PROOFSTEP]
norm_num
[GOAL]
case intro.intro
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
c : CU X
h0 : 0 < 2⁻¹
h1234 : 2⁻¹ < 3 / 4
h1 : 3 / 4 < 1
⊢ Continuous (CU.lim c)
[PROOFSTEP]
refine'
  continuous_iff_continuousAt.2 fun x =>
    (Metric.nhds_basis_closedBall_pow (h0.trans h1234) h1).tendsto_right_iff.2 fun n _ => _
[GOAL]
case intro.intro
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
c : CU X
h0 : 0 < 2⁻¹
h1234 : 2⁻¹ < 3 / 4
h1 : 3 / 4 < 1
x : X
n : ℕ
x✝ : True
⊢ ∀ᶠ (x_1 : X) in 𝓝 x, CU.lim c x_1 ∈ Metric.closedBall (CU.lim c x) ((3 / 4) ^ n)
[PROOFSTEP]
simp only [Metric.mem_closedBall]
[GOAL]
case intro.intro
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
c : CU X
h0 : 0 < 2⁻¹
h1234 : 2⁻¹ < 3 / 4
h1 : 3 / 4 < 1
x : X
n : ℕ
x✝ : True
⊢ ∀ᶠ (x_1 : X) in 𝓝 x, dist (CU.lim c x_1) (CU.lim c x) ≤ (3 / 4) ^ n
[PROOFSTEP]
induction' n with n ihn generalizing c
[GOAL]
case intro.intro.zero
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
c✝ : CU X
h0 : 0 < 2⁻¹
h1234 : 2⁻¹ < 3 / 4
h1 : 3 / 4 < 1
x : X
x✝ : True
c : CU X
⊢ ∀ᶠ (x_1 : X) in 𝓝 x, dist (CU.lim c x_1) (CU.lim c x) ≤ (3 / 4) ^ Nat.zero
[PROOFSTEP]
refine' eventually_of_forall fun y => _
[GOAL]
case intro.intro.zero
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
c✝ : CU X
h0 : 0 < 2⁻¹
h1234 : 2⁻¹ < 3 / 4
h1 : 3 / 4 < 1
x : X
x✝ : True
c : CU X
y : X
⊢ dist (CU.lim c y) (CU.lim c x) ≤ (3 / 4) ^ Nat.zero
[PROOFSTEP]
rw [pow_zero]
[GOAL]
case intro.intro.zero
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
c✝ : CU X
h0 : 0 < 2⁻¹
h1234 : 2⁻¹ < 3 / 4
h1 : 3 / 4 < 1
x : X
x✝ : True
c : CU X
y : X
⊢ dist (CU.lim c y) (CU.lim c x) ≤ 1
[PROOFSTEP]
exact Real.dist_le_of_mem_Icc_01 (c.lim_mem_Icc _) (c.lim_mem_Icc _)
[GOAL]
case intro.intro.succ
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
c✝ : CU X
h0 : 0 < 2⁻¹
h1234 : 2⁻¹ < 3 / 4
h1 : 3 / 4 < 1
x : X
x✝ : True
n : ℕ
ihn : ∀ (c : CU X), ∀ᶠ (x_1 : X) in 𝓝 x, dist (CU.lim c x_1) (CU.lim c x) ≤ (3 / 4) ^ n
c : CU X
⊢ ∀ᶠ (x_1 : X) in 𝓝 x, dist (CU.lim c x_1) (CU.lim c x) ≤ (3 / 4) ^ Nat.succ n
[PROOFSTEP]
by_cases hxl : x ∈ c.left.U
[GOAL]
case pos
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
c✝ : CU X
h0 : 0 < 2⁻¹
h1234 : 2⁻¹ < 3 / 4
h1 : 3 / 4 < 1
x : X
x✝ : True
n : ℕ
ihn : ∀ (c : CU X), ∀ᶠ (x_1 : X) in 𝓝 x, dist (CU.lim c x_1) (CU.lim c x) ≤ (3 / 4) ^ n
c : CU X
hxl : x ∈ (left c).U
⊢ ∀ᶠ (x_1 : X) in 𝓝 x, dist (CU.lim c x_1) (CU.lim c x) ≤ (3 / 4) ^ Nat.succ n
[PROOFSTEP]
filter_upwards [IsOpen.mem_nhds c.left.open_U hxl, ihn c.left] with _ hyl hyd
[GOAL]
case h
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
c✝ : CU X
h0 : 0 < 2⁻¹
h1234 : 2⁻¹ < 3 / 4
h1 : 3 / 4 < 1
x : X
x✝ : True
n : ℕ
ihn : ∀ (c : CU X), ∀ᶠ (x_1 : X) in 𝓝 x, dist (CU.lim c x_1) (CU.lim c x) ≤ (3 / 4) ^ n
c : CU X
hxl : x ∈ (left c).U
a✝ : X
hyl : a✝ ∈ (left c).U
hyd : dist (CU.lim (left c) a✝) (CU.lim (left c) x) ≤ (3 / 4) ^ n
⊢ dist (CU.lim c a✝) (CU.lim c x) ≤ (3 / 4) ^ Nat.succ n
[PROOFSTEP]
rw [pow_succ, c.lim_eq_midpoint, c.lim_eq_midpoint, c.right.lim_of_mem_C _ (c.left_U_subset_right_C hyl),
  c.right.lim_of_mem_C _ (c.left_U_subset_right_C hxl)]
[GOAL]
case h
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
c✝ : CU X
h0 : 0 < 2⁻¹
h1234 : 2⁻¹ < 3 / 4
h1 : 3 / 4 < 1
x : X
x✝ : True
n : ℕ
ihn : ∀ (c : CU X), ∀ᶠ (x_1 : X) in 𝓝 x, dist (CU.lim c x_1) (CU.lim c x) ≤ (3 / 4) ^ n
c : CU X
hxl : x ∈ (left c).U
a✝ : X
hyl : a✝ ∈ (left c).U
hyd : dist (CU.lim (left c) a✝) (CU.lim (left c) x) ≤ (3 / 4) ^ n
⊢ dist (midpoint ℝ (CU.lim (left c) a✝) 0) (midpoint ℝ (CU.lim (left c) x) 0) ≤ 3 / 4 * (3 / 4) ^ n
[PROOFSTEP]
refine' (dist_midpoint_midpoint_le _ _ _ _).trans _
[GOAL]
case h
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
c✝ : CU X
h0 : 0 < 2⁻¹
h1234 : 2⁻¹ < 3 / 4
h1 : 3 / 4 < 1
x : X
x✝ : True
n : ℕ
ihn : ∀ (c : CU X), ∀ᶠ (x_1 : X) in 𝓝 x, dist (CU.lim c x_1) (CU.lim c x) ≤ (3 / 4) ^ n
c : CU X
hxl : x ∈ (left c).U
a✝ : X
hyl : a✝ ∈ (left c).U
hyd : dist (CU.lim (left c) a✝) (CU.lim (left c) x) ≤ (3 / 4) ^ n
⊢ (dist (CU.lim (left c) a✝) (CU.lim (left c) x) + dist 0 0) / 2 ≤ 3 / 4 * (3 / 4) ^ n
[PROOFSTEP]
rw [dist_self, add_zero, div_eq_inv_mul]
[GOAL]
case h
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
c✝ : CU X
h0 : 0 < 2⁻¹
h1234 : 2⁻¹ < 3 / 4
h1 : 3 / 4 < 1
x : X
x✝ : True
n : ℕ
ihn : ∀ (c : CU X), ∀ᶠ (x_1 : X) in 𝓝 x, dist (CU.lim c x_1) (CU.lim c x) ≤ (3 / 4) ^ n
c : CU X
hxl : x ∈ (left c).U
a✝ : X
hyl : a✝ ∈ (left c).U
hyd : dist (CU.lim (left c) a✝) (CU.lim (left c) x) ≤ (3 / 4) ^ n
⊢ 2⁻¹ * dist (CU.lim (left c) a✝) (CU.lim (left c) x) ≤ 3 / 4 * (3 / 4) ^ n
[PROOFSTEP]
gcongr
[GOAL]
case neg
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
c✝ : CU X
h0 : 0 < 2⁻¹
h1234 : 2⁻¹ < 3 / 4
h1 : 3 / 4 < 1
x : X
x✝ : True
n : ℕ
ihn : ∀ (c : CU X), ∀ᶠ (x_1 : X) in 𝓝 x, dist (CU.lim c x_1) (CU.lim c x) ≤ (3 / 4) ^ n
c : CU X
hxl : ¬x ∈ (left c).U
⊢ ∀ᶠ (x_1 : X) in 𝓝 x, dist (CU.lim c x_1) (CU.lim c x) ≤ (3 / 4) ^ Nat.succ n
[PROOFSTEP]
replace hxl : x ∈ c.left.right.Cᶜ
[GOAL]
case hxl
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
c✝ : CU X
h0 : 0 < 2⁻¹
h1234 : 2⁻¹ < 3 / 4
h1 : 3 / 4 < 1
x : X
x✝ : True
n : ℕ
ihn : ∀ (c : CU X), ∀ᶠ (x_1 : X) in 𝓝 x, dist (CU.lim c x_1) (CU.lim c x) ≤ (3 / 4) ^ n
c : CU X
hxl : ¬x ∈ (left c).U
⊢ x ∈ (right (left c)).Cᶜ
case neg
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
c✝ : CU X
h0 : 0 < 2⁻¹
h1234 : 2⁻¹ < 3 / 4
h1 : 3 / 4 < 1
x : X
x✝ : True
n : ℕ
ihn : ∀ (c : CU X), ∀ᶠ (x_1 : X) in 𝓝 x, dist (CU.lim c x_1) (CU.lim c x) ≤ (3 / 4) ^ n
c : CU X
hxl : x ∈ (right (left c)).Cᶜ
⊢ ∀ᶠ (x_1 : X) in 𝓝 x, dist (CU.lim c x_1) (CU.lim c x) ≤ (3 / 4) ^ Nat.succ n
[PROOFSTEP]
exact compl_subset_compl.2 c.left.right.subset hxl
[GOAL]
case neg
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
c✝ : CU X
h0 : 0 < 2⁻¹
h1234 : 2⁻¹ < 3 / 4
h1 : 3 / 4 < 1
x : X
x✝ : True
n : ℕ
ihn : ∀ (c : CU X), ∀ᶠ (x_1 : X) in 𝓝 x, dist (CU.lim c x_1) (CU.lim c x) ≤ (3 / 4) ^ n
c : CU X
hxl : x ∈ (right (left c)).Cᶜ
⊢ ∀ᶠ (x_1 : X) in 𝓝 x, dist (CU.lim c x_1) (CU.lim c x) ≤ (3 / 4) ^ Nat.succ n
[PROOFSTEP]
filter_upwards [IsOpen.mem_nhds (isOpen_compl_iff.2 c.left.right.closed_C) hxl, ihn c.left.right, ihn c.right] with y
  hyl hydl hydr
[GOAL]
case h
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
c✝ : CU X
h0 : 0 < 2⁻¹
h1234 : 2⁻¹ < 3 / 4
h1 : 3 / 4 < 1
x : X
x✝ : True
n : ℕ
ihn : ∀ (c : CU X), ∀ᶠ (x_1 : X) in 𝓝 x, dist (CU.lim c x_1) (CU.lim c x) ≤ (3 / 4) ^ n
c : CU X
hxl : x ∈ (right (left c)).Cᶜ
y : X
hyl : y ∈ (right (left c)).Cᶜ
hydl : dist (CU.lim (right (left c)) y) (CU.lim (right (left c)) x) ≤ (3 / 4) ^ n
hydr : dist (CU.lim (right c) y) (CU.lim (right c) x) ≤ (3 / 4) ^ n
⊢ dist (CU.lim c y) (CU.lim c x) ≤ (3 / 4) ^ Nat.succ n
[PROOFSTEP]
replace hxl : x ∉ c.left.left.U
[GOAL]
case hxl
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
c✝ : CU X
h0 : 0 < 2⁻¹
h1234 : 2⁻¹ < 3 / 4
h1 : 3 / 4 < 1
x : X
x✝ : True
n : ℕ
ihn : ∀ (c : CU X), ∀ᶠ (x_1 : X) in 𝓝 x, dist (CU.lim c x_1) (CU.lim c x) ≤ (3 / 4) ^ n
c : CU X
hxl : x ∈ (right (left c)).Cᶜ
y : X
hyl : y ∈ (right (left c)).Cᶜ
hydl : dist (CU.lim (right (left c)) y) (CU.lim (right (left c)) x) ≤ (3 / 4) ^ n
hydr : dist (CU.lim (right c) y) (CU.lim (right c) x) ≤ (3 / 4) ^ n
⊢ ¬x ∈ (left (left c)).U
case h
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
c✝ : CU X
h0 : 0 < 2⁻¹
h1234 : 2⁻¹ < 3 / 4
h1 : 3 / 4 < 1
x : X
x✝ : True
n : ℕ
ihn : ∀ (c : CU X), ∀ᶠ (x_1 : X) in 𝓝 x, dist (CU.lim c x_1) (CU.lim c x) ≤ (3 / 4) ^ n
c : CU X
y : X
hyl : y ∈ (right (left c)).Cᶜ
hydl : dist (CU.lim (right (left c)) y) (CU.lim (right (left c)) x) ≤ (3 / 4) ^ n
hydr : dist (CU.lim (right c) y) (CU.lim (right c) x) ≤ (3 / 4) ^ n
hxl : ¬x ∈ (left (left c)).U
⊢ dist (CU.lim c y) (CU.lim c x) ≤ (3 / 4) ^ Nat.succ n
[PROOFSTEP]
exact compl_subset_compl.2 c.left.left_U_subset_right_C hxl
[GOAL]
case h
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
c✝ : CU X
h0 : 0 < 2⁻¹
h1234 : 2⁻¹ < 3 / 4
h1 : 3 / 4 < 1
x : X
x✝ : True
n : ℕ
ihn : ∀ (c : CU X), ∀ᶠ (x_1 : X) in 𝓝 x, dist (CU.lim c x_1) (CU.lim c x) ≤ (3 / 4) ^ n
c : CU X
y : X
hyl : y ∈ (right (left c)).Cᶜ
hydl : dist (CU.lim (right (left c)) y) (CU.lim (right (left c)) x) ≤ (3 / 4) ^ n
hydr : dist (CU.lim (right c) y) (CU.lim (right c) x) ≤ (3 / 4) ^ n
hxl : ¬x ∈ (left (left c)).U
⊢ dist (CU.lim c y) (CU.lim c x) ≤ (3 / 4) ^ Nat.succ n
[PROOFSTEP]
replace hyl : y ∉ c.left.left.U
[GOAL]
case hyl
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
c✝ : CU X
h0 : 0 < 2⁻¹
h1234 : 2⁻¹ < 3 / 4
h1 : 3 / 4 < 1
x : X
x✝ : True
n : ℕ
ihn : ∀ (c : CU X), ∀ᶠ (x_1 : X) in 𝓝 x, dist (CU.lim c x_1) (CU.lim c x) ≤ (3 / 4) ^ n
c : CU X
y : X
hyl : y ∈ (right (left c)).Cᶜ
hydl : dist (CU.lim (right (left c)) y) (CU.lim (right (left c)) x) ≤ (3 / 4) ^ n
hydr : dist (CU.lim (right c) y) (CU.lim (right c) x) ≤ (3 / 4) ^ n
hxl : ¬x ∈ (left (left c)).U
⊢ ¬y ∈ (left (left c)).U
case h
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
c✝ : CU X
h0 : 0 < 2⁻¹
h1234 : 2⁻¹ < 3 / 4
h1 : 3 / 4 < 1
x : X
x✝ : True
n : ℕ
ihn : ∀ (c : CU X), ∀ᶠ (x_1 : X) in 𝓝 x, dist (CU.lim c x_1) (CU.lim c x) ≤ (3 / 4) ^ n
c : CU X
y : X
hydl : dist (CU.lim (right (left c)) y) (CU.lim (right (left c)) x) ≤ (3 / 4) ^ n
hydr : dist (CU.lim (right c) y) (CU.lim (right c) x) ≤ (3 / 4) ^ n
hxl : ¬x ∈ (left (left c)).U
hyl : ¬y ∈ (left (left c)).U
⊢ dist (CU.lim c y) (CU.lim c x) ≤ (3 / 4) ^ Nat.succ n
[PROOFSTEP]
exact compl_subset_compl.2 c.left.left_U_subset_right_C hyl
[GOAL]
case h
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
c✝ : CU X
h0 : 0 < 2⁻¹
h1234 : 2⁻¹ < 3 / 4
h1 : 3 / 4 < 1
x : X
x✝ : True
n : ℕ
ihn : ∀ (c : CU X), ∀ᶠ (x_1 : X) in 𝓝 x, dist (CU.lim c x_1) (CU.lim c x) ≤ (3 / 4) ^ n
c : CU X
y : X
hydl : dist (CU.lim (right (left c)) y) (CU.lim (right (left c)) x) ≤ (3 / 4) ^ n
hydr : dist (CU.lim (right c) y) (CU.lim (right c) x) ≤ (3 / 4) ^ n
hxl : ¬x ∈ (left (left c)).U
hyl : ¬y ∈ (left (left c)).U
⊢ dist (CU.lim c y) (CU.lim c x) ≤ (3 / 4) ^ Nat.succ n
[PROOFSTEP]
simp only [pow_succ, c.lim_eq_midpoint, c.left.lim_eq_midpoint, c.left.left.lim_of_nmem_U _ hxl,
  c.left.left.lim_of_nmem_U _ hyl]
[GOAL]
case h
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
c✝ : CU X
h0 : 0 < 2⁻¹
h1234 : 2⁻¹ < 3 / 4
h1 : 3 / 4 < 1
x : X
x✝ : True
n : ℕ
ihn : ∀ (c : CU X), ∀ᶠ (x_1 : X) in 𝓝 x, dist (CU.lim c x_1) (CU.lim c x) ≤ (3 / 4) ^ n
c : CU X
y : X
hydl : dist (CU.lim (right (left c)) y) (CU.lim (right (left c)) x) ≤ (3 / 4) ^ n
hydr : dist (CU.lim (right c) y) (CU.lim (right c) x) ≤ (3 / 4) ^ n
hxl : ¬x ∈ (left (left c)).U
hyl : ¬y ∈ (left (left c)).U
⊢ dist (midpoint ℝ (midpoint ℝ 1 (CU.lim (right (left c)) y)) (CU.lim (right c) y))
      (midpoint ℝ (midpoint ℝ 1 (CU.lim (right (left c)) x)) (CU.lim (right c) x)) ≤
    3 / 4 * (3 / 4) ^ n
[PROOFSTEP]
refine' (dist_midpoint_midpoint_le _ _ _ _).trans _
[GOAL]
case h
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
c✝ : CU X
h0 : 0 < 2⁻¹
h1234 : 2⁻¹ < 3 / 4
h1 : 3 / 4 < 1
x : X
x✝ : True
n : ℕ
ihn : ∀ (c : CU X), ∀ᶠ (x_1 : X) in 𝓝 x, dist (CU.lim c x_1) (CU.lim c x) ≤ (3 / 4) ^ n
c : CU X
y : X
hydl : dist (CU.lim (right (left c)) y) (CU.lim (right (left c)) x) ≤ (3 / 4) ^ n
hydr : dist (CU.lim (right c) y) (CU.lim (right c) x) ≤ (3 / 4) ^ n
hxl : ¬x ∈ (left (left c)).U
hyl : ¬y ∈ (left (left c)).U
⊢ (dist (midpoint ℝ 1 (CU.lim (right (left c)) y)) (midpoint ℝ 1 (CU.lim (right (left c)) x)) +
        dist (CU.lim (right c) y) (CU.lim (right c) x)) /
      2 ≤
    3 / 4 * (3 / 4) ^ n
[PROOFSTEP]
refine' (div_le_div_of_le_of_nonneg (add_le_add_right (dist_midpoint_midpoint_le _ _ _ _) _) zero_le_two).trans _
[GOAL]
case h
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
c✝ : CU X
h0 : 0 < 2⁻¹
h1234 : 2⁻¹ < 3 / 4
h1 : 3 / 4 < 1
x : X
x✝ : True
n : ℕ
ihn : ∀ (c : CU X), ∀ᶠ (x_1 : X) in 𝓝 x, dist (CU.lim c x_1) (CU.lim c x) ≤ (3 / 4) ^ n
c : CU X
y : X
hydl : dist (CU.lim (right (left c)) y) (CU.lim (right (left c)) x) ≤ (3 / 4) ^ n
hydr : dist (CU.lim (right c) y) (CU.lim (right c) x) ≤ (3 / 4) ^ n
hxl : ¬x ∈ (left (left c)).U
hyl : ¬y ∈ (left (left c)).U
⊢ ((dist 1 1 + dist (CU.lim (right (left c)) y) (CU.lim (right (left c)) x)) / 2 +
        dist (CU.lim (right c) y) (CU.lim (right c) x)) /
      2 ≤
    3 / 4 * (3 / 4) ^ n
[PROOFSTEP]
rw [dist_self, zero_add]
[GOAL]
case h
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
c✝ : CU X
h0 : 0 < 2⁻¹
h1234 : 2⁻¹ < 3 / 4
h1 : 3 / 4 < 1
x : X
x✝ : True
n : ℕ
ihn : ∀ (c : CU X), ∀ᶠ (x_1 : X) in 𝓝 x, dist (CU.lim c x_1) (CU.lim c x) ≤ (3 / 4) ^ n
c : CU X
y : X
hydl : dist (CU.lim (right (left c)) y) (CU.lim (right (left c)) x) ≤ (3 / 4) ^ n
hydr : dist (CU.lim (right c) y) (CU.lim (right c) x) ≤ (3 / 4) ^ n
hxl : ¬x ∈ (left (left c)).U
hyl : ¬y ∈ (left (left c)).U
⊢ (dist (CU.lim (right (left c)) y) (CU.lim (right (left c)) x) / 2 + dist (CU.lim (right c) y) (CU.lim (right c) x)) /
      2 ≤
    3 / 4 * (3 / 4) ^ n
[PROOFSTEP]
set r := (3 / 4 : ℝ) ^ n
[GOAL]
case h
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
c✝ : CU X
h0 : 0 < 2⁻¹
h1234 : 2⁻¹ < 3 / 4
h1 : 3 / 4 < 1
x : X
x✝ : True
n : ℕ
c : CU X
y : X
hxl : ¬x ∈ (left (left c)).U
hyl : ¬y ∈ (left (left c)).U
r : ℝ := (3 / 4) ^ n
ihn : ∀ (c : CU X), ∀ᶠ (x_1 : X) in 𝓝 x, dist (CU.lim c x_1) (CU.lim c x) ≤ r
hydl : dist (CU.lim (right (left c)) y) (CU.lim (right (left c)) x) ≤ r
hydr : dist (CU.lim (right c) y) (CU.lim (right c) x) ≤ r
⊢ (dist (CU.lim (right (left c)) y) (CU.lim (right (left c)) x) / 2 + dist (CU.lim (right c) y) (CU.lim (right c) x)) /
      2 ≤
    3 / 4 * r
[PROOFSTEP]
calc
  _ ≤ (r / 2 + r) / 2 := by gcongr
  _ = _ := by field_simp; ring
[GOAL]
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
c✝ : CU X
h0 : 0 < 2⁻¹
h1234 : 2⁻¹ < 3 / 4
h1 : 3 / 4 < 1
x : X
x✝ : True
n : ℕ
c : CU X
y : X
hxl : ¬x ∈ (left (left c)).U
hyl : ¬y ∈ (left (left c)).U
r : ℝ := (3 / 4) ^ n
ihn : ∀ (c : CU X), ∀ᶠ (x_1 : X) in 𝓝 x, dist (CU.lim c x_1) (CU.lim c x) ≤ r
hydl : dist (CU.lim (right (left c)) y) (CU.lim (right (left c)) x) ≤ r
hydr : dist (CU.lim (right c) y) (CU.lim (right c) x) ≤ r
⊢ (dist (CU.lim (right (left c)) y) (CU.lim (right (left c)) x) / 2 + dist (CU.lim (right c) y) (CU.lim (right c) x)) /
      2 ≤
    (r / 2 + r) / 2
[PROOFSTEP]
gcongr
[GOAL]
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
c✝ : CU X
h0 : 0 < 2⁻¹
h1234 : 2⁻¹ < 3 / 4
h1 : 3 / 4 < 1
x : X
x✝ : True
n : ℕ
c : CU X
y : X
hxl : ¬x ∈ (left (left c)).U
hyl : ¬y ∈ (left (left c)).U
r : ℝ := (3 / 4) ^ n
ihn : ∀ (c : CU X), ∀ᶠ (x_1 : X) in 𝓝 x, dist (CU.lim c x_1) (CU.lim c x) ≤ r
hydl : dist (CU.lim (right (left c)) y) (CU.lim (right (left c)) x) ≤ r
hydr : dist (CU.lim (right c) y) (CU.lim (right c) x) ≤ r
⊢ (r / 2 + r) / 2 = 3 / 4 * r
[PROOFSTEP]
field_simp
[GOAL]
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
c✝ : CU X
h0 : 0 < 2⁻¹
h1234 : 2⁻¹ < 3 / 4
h1 : 3 / 4 < 1
x : X
x✝ : True
n : ℕ
c : CU X
y : X
hxl : ¬x ∈ (left (left c)).U
hyl : ¬y ∈ (left (left c)).U
r : ℝ := (3 / 4) ^ n
ihn : ∀ (c : CU X), ∀ᶠ (x_1 : X) in 𝓝 x, dist (CU.lim c x_1) (CU.lim c x) ≤ r
hydl : dist (CU.lim (right (left c)) y) (CU.lim (right (left c)) x) ≤ r
hydr : dist (CU.lim (right c) y) (CU.lim (right c) x) ≤ r
⊢ (3 ^ n * 4 ^ n + 3 ^ n * (4 ^ n * 2)) * (4 * 4 ^ n) = 3 * 3 ^ n * (4 ^ n * 2 * 4 ^ n * 2)
[PROOFSTEP]
ring
[GOAL]
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
s t : Set X
hs : IsClosed s
ht : IsClosed t
hd : Disjoint s t
⊢ ∃ f, EqOn (↑f) 0 s ∧ EqOn (↑f) 1 t ∧ ∀ (x : X), ↑f x ∈ Icc 0 1
[PROOFSTEP]
set c : Urysohns.CU X := ⟨s, tᶜ, hs, ht.isOpen_compl, disjoint_left.1 hd⟩
[GOAL]
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : NormalSpace X
s t : Set X
hs : IsClosed s
ht : IsClosed t
hd : Disjoint s t
c : Urysohns.CU X :=
  { C := s, U := tᶜ, closed_C := hs, open_U := (_ : IsOpen tᶜ), subset := (_ : ∀ ⦃a : X⦄, a ∈ s → ¬a ∈ t) }
⊢ ∃ f, EqOn (↑f) 0 s ∧ EqOn (↑f) 1 t ∧ ∀ (x : X), ↑f x ∈ Icc 0 1
[PROOFSTEP]
exact ⟨⟨c.lim, c.continuous_lim⟩, c.lim_of_mem_C, fun x hx => c.lim_of_nmem_U _ fun h => h hx, c.lim_mem_Icc⟩


[GOAL]
R✝ : Type u
M✝ : Type v
N✝ : Type w
inst✝⁹ : Ring R✝
inst✝⁸ : AddCommGroup M✝
inst✝⁷ : Module R✝ M✝
inst✝⁶ : AddCommGroup N✝
inst✝⁵ : Module R✝ N✝
R : Type u_1
M : Type u_2
N : Type u_3
ι : Type u_4
κ : Type u_5
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
i : ι
m : M
k : κ
n : N
⊢ ↑(finsuppTensorFinsupp R M N ι κ) (Finsupp.single i m ⊗ₜ[R] Finsupp.single k n) = Finsupp.single (i, k) (m ⊗ₜ[R] n)
[PROOFSTEP]
classical simp [finsuppTensorFinsupp]
[GOAL]
R✝ : Type u
M✝ : Type v
N✝ : Type w
inst✝⁹ : Ring R✝
inst✝⁸ : AddCommGroup M✝
inst✝⁷ : Module R✝ M✝
inst✝⁶ : AddCommGroup N✝
inst✝⁵ : Module R✝ N✝
R : Type u_1
M : Type u_2
N : Type u_3
ι : Type u_4
κ : Type u_5
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
i : ι
m : M
k : κ
n : N
⊢ ↑(finsuppTensorFinsupp R M N ι κ) (Finsupp.single i m ⊗ₜ[R] Finsupp.single k n) = Finsupp.single (i, k) (m ⊗ₜ[R] n)
[PROOFSTEP]
simp [finsuppTensorFinsupp]
[GOAL]
R✝ : Type u
M✝ : Type v
N✝ : Type w
inst✝⁹ : Ring R✝
inst✝⁸ : AddCommGroup M✝
inst✝⁷ : Module R✝ M✝
inst✝⁶ : AddCommGroup N✝
inst✝⁵ : Module R✝ N✝
R : Type u_1
M : Type u_2
N : Type u_3
ι : Type u_4
κ : Type u_5
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : ι →₀ M
g : κ →₀ N
i : ι
k : κ
⊢ ↑(↑(finsuppTensorFinsupp R M N ι κ) (f ⊗ₜ[R] g)) (i, k) = ↑f i ⊗ₜ[R] ↑g k
[PROOFSTEP]
apply Finsupp.induction_linear f
[GOAL]
case h0
R✝ : Type u
M✝ : Type v
N✝ : Type w
inst✝⁹ : Ring R✝
inst✝⁸ : AddCommGroup M✝
inst✝⁷ : Module R✝ M✝
inst✝⁶ : AddCommGroup N✝
inst✝⁵ : Module R✝ N✝
R : Type u_1
M : Type u_2
N : Type u_3
ι : Type u_4
κ : Type u_5
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : ι →₀ M
g : κ →₀ N
i : ι
k : κ
⊢ ↑(↑(finsuppTensorFinsupp R M N ι κ) (0 ⊗ₜ[R] g)) (i, k) = ↑0 i ⊗ₜ[R] ↑g k
[PROOFSTEP]
simp
[GOAL]
case hadd
R✝ : Type u
M✝ : Type v
N✝ : Type w
inst✝⁹ : Ring R✝
inst✝⁸ : AddCommGroup M✝
inst✝⁷ : Module R✝ M✝
inst✝⁶ : AddCommGroup N✝
inst✝⁵ : Module R✝ N✝
R : Type u_1
M : Type u_2
N : Type u_3
ι : Type u_4
κ : Type u_5
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : ι →₀ M
g : κ →₀ N
i : ι
k : κ
⊢ ∀ (f g_1 : ι →₀ M),
    ↑(↑(finsuppTensorFinsupp R M N ι κ) (f ⊗ₜ[R] g)) (i, k) = ↑f i ⊗ₜ[R] ↑g k →
      ↑(↑(finsuppTensorFinsupp R M N ι κ) (g_1 ⊗ₜ[R] g)) (i, k) = ↑g_1 i ⊗ₜ[R] ↑g k →
        ↑(↑(finsuppTensorFinsupp R M N ι κ) ((f + g_1) ⊗ₜ[R] g)) (i, k) = ↑(f + g_1) i ⊗ₜ[R] ↑g k
[PROOFSTEP]
intro f₁ f₂ hf₁ hf₂
[GOAL]
case hadd
R✝ : Type u
M✝ : Type v
N✝ : Type w
inst✝⁹ : Ring R✝
inst✝⁸ : AddCommGroup M✝
inst✝⁷ : Module R✝ M✝
inst✝⁶ : AddCommGroup N✝
inst✝⁵ : Module R✝ N✝
R : Type u_1
M : Type u_2
N : Type u_3
ι : Type u_4
κ : Type u_5
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : ι →₀ M
g : κ →₀ N
i : ι
k : κ
f₁ f₂ : ι →₀ M
hf₁ : ↑(↑(finsuppTensorFinsupp R M N ι κ) (f₁ ⊗ₜ[R] g)) (i, k) = ↑f₁ i ⊗ₜ[R] ↑g k
hf₂ : ↑(↑(finsuppTensorFinsupp R M N ι κ) (f₂ ⊗ₜ[R] g)) (i, k) = ↑f₂ i ⊗ₜ[R] ↑g k
⊢ ↑(↑(finsuppTensorFinsupp R M N ι κ) ((f₁ + f₂) ⊗ₜ[R] g)) (i, k) = ↑(f₁ + f₂) i ⊗ₜ[R] ↑g k
[PROOFSTEP]
simp [add_tmul, hf₁, hf₂]
[GOAL]
case hsingle
R✝ : Type u
M✝ : Type v
N✝ : Type w
inst✝⁹ : Ring R✝
inst✝⁸ : AddCommGroup M✝
inst✝⁷ : Module R✝ M✝
inst✝⁶ : AddCommGroup N✝
inst✝⁵ : Module R✝ N✝
R : Type u_1
M : Type u_2
N : Type u_3
ι : Type u_4
κ : Type u_5
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : ι →₀ M
g : κ →₀ N
i : ι
k : κ
⊢ ∀ (a : ι) (b : M),
    ↑(↑(finsuppTensorFinsupp R M N ι κ) (Finsupp.single a b ⊗ₜ[R] g)) (i, k) = ↑(Finsupp.single a b) i ⊗ₜ[R] ↑g k
[PROOFSTEP]
intro i' m
[GOAL]
case hsingle
R✝ : Type u
M✝ : Type v
N✝ : Type w
inst✝⁹ : Ring R✝
inst✝⁸ : AddCommGroup M✝
inst✝⁷ : Module R✝ M✝
inst✝⁶ : AddCommGroup N✝
inst✝⁵ : Module R✝ N✝
R : Type u_1
M : Type u_2
N : Type u_3
ι : Type u_4
κ : Type u_5
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : ι →₀ M
g : κ →₀ N
i : ι
k : κ
i' : ι
m : M
⊢ ↑(↑(finsuppTensorFinsupp R M N ι κ) (Finsupp.single i' m ⊗ₜ[R] g)) (i, k) = ↑(Finsupp.single i' m) i ⊗ₜ[R] ↑g k
[PROOFSTEP]
apply Finsupp.induction_linear g
[GOAL]
case hsingle.h0
R✝ : Type u
M✝ : Type v
N✝ : Type w
inst✝⁹ : Ring R✝
inst✝⁸ : AddCommGroup M✝
inst✝⁷ : Module R✝ M✝
inst✝⁶ : AddCommGroup N✝
inst✝⁵ : Module R✝ N✝
R : Type u_1
M : Type u_2
N : Type u_3
ι : Type u_4
κ : Type u_5
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : ι →₀ M
g : κ →₀ N
i : ι
k : κ
i' : ι
m : M
⊢ ↑(↑(finsuppTensorFinsupp R M N ι κ) (Finsupp.single i' m ⊗ₜ[R] 0)) (i, k) = ↑(Finsupp.single i' m) i ⊗ₜ[R] ↑0 k
[PROOFSTEP]
simp
[GOAL]
case hsingle.hadd
R✝ : Type u
M✝ : Type v
N✝ : Type w
inst✝⁹ : Ring R✝
inst✝⁸ : AddCommGroup M✝
inst✝⁷ : Module R✝ M✝
inst✝⁶ : AddCommGroup N✝
inst✝⁵ : Module R✝ N✝
R : Type u_1
M : Type u_2
N : Type u_3
ι : Type u_4
κ : Type u_5
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : ι →₀ M
g : κ →₀ N
i : ι
k : κ
i' : ι
m : M
⊢ ∀ (f g : κ →₀ N),
    ↑(↑(finsuppTensorFinsupp R M N ι κ) (Finsupp.single i' m ⊗ₜ[R] f)) (i, k) = ↑(Finsupp.single i' m) i ⊗ₜ[R] ↑f k →
      ↑(↑(finsuppTensorFinsupp R M N ι κ) (Finsupp.single i' m ⊗ₜ[R] g)) (i, k) = ↑(Finsupp.single i' m) i ⊗ₜ[R] ↑g k →
        ↑(↑(finsuppTensorFinsupp R M N ι κ) (Finsupp.single i' m ⊗ₜ[R] (f + g))) (i, k) =
          ↑(Finsupp.single i' m) i ⊗ₜ[R] ↑(f + g) k
[PROOFSTEP]
intro g₁ g₂ hg₁ hg₂
[GOAL]
case hsingle.hadd
R✝ : Type u
M✝ : Type v
N✝ : Type w
inst✝⁹ : Ring R✝
inst✝⁸ : AddCommGroup M✝
inst✝⁷ : Module R✝ M✝
inst✝⁶ : AddCommGroup N✝
inst✝⁵ : Module R✝ N✝
R : Type u_1
M : Type u_2
N : Type u_3
ι : Type u_4
κ : Type u_5
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : ι →₀ M
g : κ →₀ N
i : ι
k : κ
i' : ι
m : M
g₁ g₂ : κ →₀ N
hg₁ : ↑(↑(finsuppTensorFinsupp R M N ι κ) (Finsupp.single i' m ⊗ₜ[R] g₁)) (i, k) = ↑(Finsupp.single i' m) i ⊗ₜ[R] ↑g₁ k
hg₂ : ↑(↑(finsuppTensorFinsupp R M N ι κ) (Finsupp.single i' m ⊗ₜ[R] g₂)) (i, k) = ↑(Finsupp.single i' m) i ⊗ₜ[R] ↑g₂ k
⊢ ↑(↑(finsuppTensorFinsupp R M N ι κ) (Finsupp.single i' m ⊗ₜ[R] (g₁ + g₂))) (i, k) =
    ↑(Finsupp.single i' m) i ⊗ₜ[R] ↑(g₁ + g₂) k
[PROOFSTEP]
simp [tmul_add, hg₁, hg₂]
[GOAL]
case hsingle.hsingle
R✝ : Type u
M✝ : Type v
N✝ : Type w
inst✝⁹ : Ring R✝
inst✝⁸ : AddCommGroup M✝
inst✝⁷ : Module R✝ M✝
inst✝⁶ : AddCommGroup N✝
inst✝⁵ : Module R✝ N✝
R : Type u_1
M : Type u_2
N : Type u_3
ι : Type u_4
κ : Type u_5
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : ι →₀ M
g : κ →₀ N
i : ι
k : κ
i' : ι
m : M
⊢ ∀ (a : κ) (b : N),
    ↑(↑(finsuppTensorFinsupp R M N ι κ) (Finsupp.single i' m ⊗ₜ[R] Finsupp.single a b)) (i, k) =
      ↑(Finsupp.single i' m) i ⊗ₜ[R] ↑(Finsupp.single a b) k
[PROOFSTEP]
intro k' n
[GOAL]
case hsingle.hsingle
R✝ : Type u
M✝ : Type v
N✝ : Type w
inst✝⁹ : Ring R✝
inst✝⁸ : AddCommGroup M✝
inst✝⁷ : Module R✝ M✝
inst✝⁶ : AddCommGroup N✝
inst✝⁵ : Module R✝ N✝
R : Type u_1
M : Type u_2
N : Type u_3
ι : Type u_4
κ : Type u_5
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : ι →₀ M
g : κ →₀ N
i : ι
k : κ
i' : ι
m : M
k' : κ
n : N
⊢ ↑(↑(finsuppTensorFinsupp R M N ι κ) (Finsupp.single i' m ⊗ₜ[R] Finsupp.single k' n)) (i, k) =
    ↑(Finsupp.single i' m) i ⊗ₜ[R] ↑(Finsupp.single k' n) k
[PROOFSTEP]
simp only [finsuppTensorFinsupp_single]
  -- split_ifs; finish can close the goal from here
[GOAL]
case hsingle.hsingle
R✝ : Type u
M✝ : Type v
N✝ : Type w
inst✝⁹ : Ring R✝
inst✝⁸ : AddCommGroup M✝
inst✝⁷ : Module R✝ M✝
inst✝⁶ : AddCommGroup N✝
inst✝⁵ : Module R✝ N✝
R : Type u_1
M : Type u_2
N : Type u_3
ι : Type u_4
κ : Type u_5
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : ι →₀ M
g : κ →₀ N
i : ι
k : κ
i' : ι
m : M
k' : κ
n : N
⊢ ↑(Finsupp.single (i', k') (m ⊗ₜ[R] n)) (i, k) = ↑(Finsupp.single i' m) i ⊗ₜ[R] ↑(Finsupp.single k' n) k
[PROOFSTEP]
by_cases h1 : (i', k') = (i, k)
[GOAL]
case pos
R✝ : Type u
M✝ : Type v
N✝ : Type w
inst✝⁹ : Ring R✝
inst✝⁸ : AddCommGroup M✝
inst✝⁷ : Module R✝ M✝
inst✝⁶ : AddCommGroup N✝
inst✝⁵ : Module R✝ N✝
R : Type u_1
M : Type u_2
N : Type u_3
ι : Type u_4
κ : Type u_5
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : ι →₀ M
g : κ →₀ N
i : ι
k : κ
i' : ι
m : M
k' : κ
n : N
h1 : (i', k') = (i, k)
⊢ ↑(Finsupp.single (i', k') (m ⊗ₜ[R] n)) (i, k) = ↑(Finsupp.single i' m) i ⊗ₜ[R] ↑(Finsupp.single k' n) k
[PROOFSTEP]
simp only [Prod.mk.inj_iff] at h1
[GOAL]
case pos
R✝ : Type u
M✝ : Type v
N✝ : Type w
inst✝⁹ : Ring R✝
inst✝⁸ : AddCommGroup M✝
inst✝⁷ : Module R✝ M✝
inst✝⁶ : AddCommGroup N✝
inst✝⁵ : Module R✝ N✝
R : Type u_1
M : Type u_2
N : Type u_3
ι : Type u_4
κ : Type u_5
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : ι →₀ M
g : κ →₀ N
i : ι
k : κ
i' : ι
m : M
k' : κ
n : N
h1 : i' = i ∧ k' = k
⊢ ↑(Finsupp.single (i', k') (m ⊗ₜ[R] n)) (i, k) = ↑(Finsupp.single i' m) i ⊗ₜ[R] ↑(Finsupp.single k' n) k
[PROOFSTEP]
simp [h1]
[GOAL]
case neg
R✝ : Type u
M✝ : Type v
N✝ : Type w
inst✝⁹ : Ring R✝
inst✝⁸ : AddCommGroup M✝
inst✝⁷ : Module R✝ M✝
inst✝⁶ : AddCommGroup N✝
inst✝⁵ : Module R✝ N✝
R : Type u_1
M : Type u_2
N : Type u_3
ι : Type u_4
κ : Type u_5
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : ι →₀ M
g : κ →₀ N
i : ι
k : κ
i' : ι
m : M
k' : κ
n : N
h1 : ¬(i', k') = (i, k)
⊢ ↑(Finsupp.single (i', k') (m ⊗ₜ[R] n)) (i, k) = ↑(Finsupp.single i' m) i ⊗ₜ[R] ↑(Finsupp.single k' n) k
[PROOFSTEP]
simp only [Prod.mk.inj_iff, not_and_or] at h1
[GOAL]
case neg
R✝ : Type u
M✝ : Type v
N✝ : Type w
inst✝⁹ : Ring R✝
inst✝⁸ : AddCommGroup M✝
inst✝⁷ : Module R✝ M✝
inst✝⁶ : AddCommGroup N✝
inst✝⁵ : Module R✝ N✝
R : Type u_1
M : Type u_2
N : Type u_3
ι : Type u_4
κ : Type u_5
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : ι →₀ M
g : κ →₀ N
i : ι
k : κ
i' : ι
m : M
k' : κ
n : N
h1 : ¬i' = i ∨ ¬k' = k
⊢ ↑(Finsupp.single (i', k') (m ⊗ₜ[R] n)) (i, k) = ↑(Finsupp.single i' m) i ⊗ₜ[R] ↑(Finsupp.single k' n) k
[PROOFSTEP]
cases' h1 with h1 h1
[GOAL]
case neg.inl
R✝ : Type u
M✝ : Type v
N✝ : Type w
inst✝⁹ : Ring R✝
inst✝⁸ : AddCommGroup M✝
inst✝⁷ : Module R✝ M✝
inst✝⁶ : AddCommGroup N✝
inst✝⁵ : Module R✝ N✝
R : Type u_1
M : Type u_2
N : Type u_3
ι : Type u_4
κ : Type u_5
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : ι →₀ M
g : κ →₀ N
i : ι
k : κ
i' : ι
m : M
k' : κ
n : N
h1 : ¬i' = i
⊢ ↑(Finsupp.single (i', k') (m ⊗ₜ[R] n)) (i, k) = ↑(Finsupp.single i' m) i ⊗ₜ[R] ↑(Finsupp.single k' n) k
[PROOFSTEP]
simp [h1]
[GOAL]
case neg.inr
R✝ : Type u
M✝ : Type v
N✝ : Type w
inst✝⁹ : Ring R✝
inst✝⁸ : AddCommGroup M✝
inst✝⁷ : Module R✝ M✝
inst✝⁶ : AddCommGroup N✝
inst✝⁵ : Module R✝ N✝
R : Type u_1
M : Type u_2
N : Type u_3
ι : Type u_4
κ : Type u_5
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : ι →₀ M
g : κ →₀ N
i : ι
k : κ
i' : ι
m : M
k' : κ
n : N
h1 : ¬k' = k
⊢ ↑(Finsupp.single (i', k') (m ⊗ₜ[R] n)) (i, k) = ↑(Finsupp.single i' m) i ⊗ₜ[R] ↑(Finsupp.single k' n) k
[PROOFSTEP]
simp [h1]
[GOAL]
R : Type u
M : Type v
N : Type w
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
S : Type u_1
inst✝ : CommRing S
α : Type u_2
β : Type u_3
f : α →₀ S
g : β →₀ S
a : α
b : β
⊢ ↑(↑(finsuppTensorFinsupp' S α β) (f ⊗ₜ[S] g)) (a, b) = ↑f a * ↑g b
[PROOFSTEP]
simp [finsuppTensorFinsupp']
[GOAL]
R : Type u
M : Type v
N : Type w
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
S : Type u_1
inst✝ : CommRing S
α : Type u_2
β : Type u_3
a : α
b : β
r₁ r₂ : S
⊢ ↑(finsuppTensorFinsupp' S α β) (Finsupp.single a r₁ ⊗ₜ[S] Finsupp.single b r₂) = Finsupp.single (a, b) (r₁ * r₂)
[PROOFSTEP]
ext ⟨a', b'⟩
[GOAL]
case h.mk
R : Type u
M : Type v
N : Type w
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
S : Type u_1
inst✝ : CommRing S
α : Type u_2
β : Type u_3
a : α
b : β
r₁ r₂ : S
a' : α
b' : β
⊢ ↑(↑(finsuppTensorFinsupp' S α β) (Finsupp.single a r₁ ⊗ₜ[S] Finsupp.single b r₂)) (a', b') =
    ↑(Finsupp.single (a, b) (r₁ * r₂)) (a', b')
[PROOFSTEP]
classical aesop (add norm [Finsupp.single_apply])
[GOAL]
case h.mk
R : Type u
M : Type v
N : Type w
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
S : Type u_1
inst✝ : CommRing S
α : Type u_2
β : Type u_3
a : α
b : β
r₁ r₂ : S
a' : α
b' : β
⊢ ↑(↑(finsuppTensorFinsupp' S α β) (Finsupp.single a r₁ ⊗ₜ[S] Finsupp.single b r₂)) (a', b') =
    ↑(Finsupp.single (a, b) (r₁ * r₂)) (a', b')
[PROOFSTEP]
aesop (add norm [Finsupp.single_apply])