mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Separation.DisjointCover

Goal state before:
pp: ι : Type u_1
X : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TotallyDisconnectedSpace X
inst✝¹ : T2Space X
inst✝ : CompactSpace X
U : ι → Opens X
hU : IsOpenCover U
r : X → ι
hr : ∀ (a : X), a ∈ U (r a)
V : X → Set X
hV : ∀ (x : X), IsClopen (V x)
hVx : ∀ (x : X), x ∈ V x
hVU : ∀ (x : X), V x ⊆ ↑(U (r x))
t : Finset X
ht : univ ⊆ ⋃ i ∈ t, V i
x : X
hx : x ∈ univ
m : X
hm : m ∈ t
hm' : x ∈ V m
⊢ x ∈ ↑((fun j ↦ { carrier := V ↑(t.equivFin.symm j), isClopen' := ⋯ }) (t.equivFin ⟨m, hm⟩))

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Separation.DisjointCover

Goal state before:
pp: ι : Type u_1
X : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TotallyDisconnectedSpace X
inst✝¹ : T2Space X
inst✝ : CompactSpace X
U : ι → Opens X
hU : IsOpenCover U
⊢ ∃ n V, (∀ (j : Fin n), ∃ i, ↑(V j) ⊆ ↑(U i)) ∧ univ ⊆ ⋃ j, ↑(V j)

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Padics.WithVal

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
⊢ IsDenseInducing ⇑((Rat.castHom ℚ_[p]).comp (WithVal.equiv (Rat.padicValuation p)).toRingHom)

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Padics.WithVal

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
y : (Rat.padicValuation p).Completion
⊢ ⋯.extend coe' ((extensionHom ((Rat.castHom ℚ_[p]).comp (WithVal.equiv (Rat.padicValuation p)).toRingHom) ⋯) y) = y

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Padics.HeightOneSpectrum

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
inst✝² : Algebra R ℚ
inst✝¹ : IsIntegralClosure R ℤ ℚ
inst✝ : IsFractionRing R ℚ
x : R
y : ℤ
hy : (algebraMap ℤ ℚ) y = (algebraMap R ℚ) x
⊢ (algebraMap R ℚ) ((algebraMap ℤ R) y) = (algebraMap R ℚ) x

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Padics.HeightOneSpectrum

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
inst✝² : Algebra R ℚ
inst✝¹ : IsIntegralClosure R ℤ ℚ
inst✝ : IsFractionRing R ℚ
⊢ Function.Surjective ⇑(algebraMap ℤ R)

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Padics.HeightOneSpectrum

Goal state before:
pp: x : 𝓞 ℚ
⊢ (intEquiv (𝓞 ℚ)) x = ringOfIntegersEquiv x

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Padics.HeightOneSpectrum

Goal state before:
pp: R : Type u_2
inst✝² : CommRing R
inst✝¹ : Algebra R ℚ
inst✝ : IsIntegralClosure R ℤ ℚ
v : HeightOneSpectrum R
⊢ Ideal.span {↑(natGenerator v)} = Ideal.map (IsIntegralClosure.intEquiv R) v.asIdeal

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Padics.WithVal

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
a✝ : ℚ
⊢ ∀ (q : ℚ), ⋯.extend coe' ↑q = ↑((WithVal.equiv (Rat.padicValuation p)).symm q)

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Padics.HeightOneSpectrum

Goal state before:
pp: R : Type u_2
inst✝² : CommRing R
inst✝¹ : Algebra R ℚ
inst✝ : IsIntegralClosure R ℤ ℚ
v : HeightOneSpectrum R
n : ℕ
⊢ natGenerator v ∣ n ↔ ↑n ∈ Ideal.map (IsIntegralClosure.intEquiv R) v.asIdeal

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Padics.HeightOneSpectrum

Goal state before:
pp: R✝ : Type u_1
inst✝⁷ : CommRing R✝
inst✝⁶ : Algebra R✝ ℚ
inst✝⁵ : IsIntegralClosure R✝ ℤ ℚ
R : Type u_2
inst✝⁴ : CommRing R
inst✝³ : Algebra R ℚ
inst✝² : IsIntegralClosure R ℤ ℚ
inst✝¹ : IsDedekindDomain R
inst✝ : IsFractionRing R ℚ
p : Nat.Primes
⊢ Prime (Ideal.span {↑↑p})

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Padics.HeightOneSpectrum

Goal state before:
pp: R✝ : Type u_1
inst✝⁷ : CommRing R✝
inst✝⁶ : Algebra R✝ ℚ
inst✝⁵ : IsIntegralClosure R✝ ℤ ℚ
R : Type u_2
inst✝⁴ : CommRing R
inst✝³ : Algebra R ℚ
inst✝² : IsIntegralClosure R ℤ ℚ
inst✝¹ : IsDedekindDomain R
inst✝ : IsFractionRing R ℚ
p : Nat.Primes
⊢ Ideal.span {↑↑p} ≠ ⊥

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Separation.DisjointCover

Goal state before:
pp: ι : Type u_1
X : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TotallyDisconnectedSpace X
inst✝¹ : T2Space X
inst✝ : CompactSpace X
U : ι → Opens X
hU : IsOpenCover U
n : ℕ
V : Fin n → Clopens X
hVle : ∀ (j : Fin n), ∃ i, ↑(V j) ⊆ ↑(U i)
hVun : univ ⊆ ⋃ j, ↑(V j)
W : Fin n → Clopens X
hWle : W ≤ V
hWd : Pairwise (Disjoint on W)
hWun : ⋃ i, ↑(W i) = ⋃ i, ↑(V i)
t : Finset (Fin n) := {j | W j ≠ ⊥}
x : X
hx : x ∈ univ
j : Fin n
hj : x ∈ ↑(W j)
⊢ W j ≠ ⊥

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Padics.WithVal

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
y : ℚ_[p]
⊢ (extensionHom ((Rat.castHom ℚ_[p]).comp (WithVal.equiv (Rat.padicValuation p)).toRingHom) ⋯) (⋯.extend coe' y) = y

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Padics.WithVal

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
x : WithVal (Rat.padicValuation p)
⊢ withValUniformEquiv ↑x = ↑((WithVal.equiv (Rat.padicValuation p)) x)

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Padics.WithVal

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
x : ℚ
⊢ ‖↑x‖ ≤ 1 ↔ (Rat.padicValuation p) x ≤ 1

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Padics.HeightOneSpectrum

Goal state before:
pp: R✝ : Type u_1
inst✝⁷ : CommRing R✝
inst✝⁶ : Algebra R✝ ℚ
inst✝⁵ : IsIntegralClosure R✝ ℤ ℚ
R : Type u_2
inst✝⁴ : CommRing R
inst✝³ : Algebra R ℚ
inst✝² : IsIntegralClosure R ℤ ℚ
inst✝¹ : IsDedekindDomain R
inst✝ : IsFractionRing R ℚ
v : HeightOneSpectrum R
⊢ (fun p ↦
        have h := ⋯;
        HeightOneSpectrum.ofPrime h)
      ((fun v ↦ ⟨natGenerator v, ⋯⟩) v) =
    v

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Separation.DisjointCover

Goal state before:
pp: ι : Type u_1
X : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TotallyDisconnectedSpace X
inst✝¹ : T2Space X
inst✝ : CompactSpace X
U : ι → Opens X
hU : IsOpenCover U
n : ℕ
V : Fin n → Clopens X
hVle : ∀ (j : Fin n), ∃ i, ↑(V j) ⊆ ↑(U i)
hVun : univ ⊆ ⋃ j, ↑(V j)
W : Fin n → Clopens X
hWle : W ≤ V
hWd : Pairwise (Disjoint on W)
hWun : ⋃ i, ↑(W i) = ⋃ i, ↑(V i)
t : Finset (Fin n) := {j | W j ≠ ⊥}
x : X
hx : x ∈ univ
j : Fin n
hj : x ∈ ↑(W j)
this : W j ≠ ⊥
⊢ x ∈ ↑((fun k ↦ W ↑(t.equivFin.symm k)) (t.equivFin ⟨j, ⋯⟩))

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Padics.HeightOneSpectrum

Goal state before:
pp: R✝ : Type u_1
inst✝⁷ : CommRing R✝
inst✝⁶ : Algebra R✝ ℚ
inst✝⁵ : IsIntegralClosure R✝ ℤ ℚ
R : Type u_2
inst✝⁴ : CommRing R
inst✝³ : Algebra R ℚ
inst✝² : IsIntegralClosure R ℤ ℚ
inst✝¹ : IsDedekindDomain R
inst✝ : IsFractionRing R ℚ
p : Nat.Primes
⊢ (fun v ↦ ⟨natGenerator v, ⋯⟩)
      ((fun p ↦
          have h := ⋯;
          HeightOneSpectrum.ofPrime h)
        p) =
    p

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Padics.HeightOneSpectrum

Goal state before:
pp: R : Type u_2
inst✝⁴ : CommRing R
inst✝³ : Algebra R ℚ
inst✝² : IsIntegralClosure R ℤ ℚ
inst✝¹ : IsDedekindDomain R
inst✝ : IsFractionRing R ℚ
v : HeightOneSpectrum R
⊢ (HeightOneSpectrum.valuation ℚ v).IsEquiv (padicValuation ↑(primesEquiv v))

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Padics.WithVal

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
x : (Rat.padicValuation p).Completion
⊢ ‖withValUniformEquiv x‖ ≤ 1 ↔ Valued.v x ≤ 1

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Padics.HeightOneSpectrum

Goal state before:
pp: R✝ : Type u_1
inst✝⁷ : CommRing R✝
inst✝⁶ : Algebra R✝ ℚ
inst✝⁵ : IsIntegralClosure R✝ ℤ ℚ
R : Type u_2
inst✝⁴ : CommRing R
inst✝³ : Algebra R ℚ
inst✝² : IsIntegralClosure R ℤ ℚ
inst✝¹ : IsDedekindDomain R
inst✝ : IsFractionRing R ℚ
v : HeightOneSpectrum R
⊢ ∀ (r : ℚ),
    ((HeightOneSpectrum.adicCompletion.equiv ℚ v).trans
            ((mapRingEquiv
                  (WithVal.congr (HeightOneSpectrum.valuation ℚ v) (padicValuation ↑(primesEquiv v)) (RingEquiv.refl ℚ))
                  ⋯ ⋯).trans
              Padic.withValRingEquiv)).toFun
        ((algebraMap ℚ (HeightOneSpectrum.adicCompletion ℚ v)) r) =
      (algebraMap ℚ ℚ_[↑(primesEquiv v)]) r

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Separation.DisjointCover

Goal state before:
pp: ι : Type u_1
X : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TotallyDisconnectedSpace X
inst✝¹ : T2Space X
inst✝ : CompactSpace X
U : ι → Opens X
hU : IsOpenCover U
⊢ ∃ n W, (∀ (j : Fin n), W j ≠ ⊥ ∧ ∃ i, ↑(W j) ⊆ ↑(U i)) ∧ univ ⊆ ⋃ j, ↑(W j) ∧ Pairwise (Disjoint on W)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.UniformSpace.ProdApproximation

Goal state before:
pp: X : Type u_1
Y : Type u_2
R : Type u_3
V : Type u_4
inst✝¹¹ : TopologicalSpace X
inst✝¹⁰ : TotallyDisconnectedSpace X
inst✝⁹ : T2Space X
inst✝⁸ : CompactSpace X
inst✝⁷ : TopologicalSpace Y
inst✝⁶ : CompactSpace Y
inst✝⁵ : AddCommGroup V
inst✝⁴ : UniformSpace V
inst✝³ : IsUniformAddGroup V
S : Set (V × V)
inst✝² : TopologicalSpace R
inst✝¹ : MonoidWithZero R
inst✝ : MulActionWithZero R V
f : C(X × Y, V)
hS : S ∈ 𝓤 V
⊢ {fg | ∀ x ∈ Set.univ, (fg.1 x, fg.2 x) ∈ S} ⊆ {(f, g) | ∀ (y : Y), (f y, g y) ∈ S}

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Separation.DisjointCover

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
S : Set (X × X)
hS : S ∈ 𝓝ˢ (diagonal X)
x : X
this : S ∈ 𝓝 (x, x)
⊢ ?m.37

Tactic:
by

Goal state after:
Module: Mathlib.Topology.UniformSpace.ProdApproximation

Goal state before:
pp: X : Type u_1
Y : Type u_2
R : Type u_3
V : Type u_4
inst✝¹¹ : TopologicalSpace X
inst✝¹⁰ : TotallyDisconnectedSpace X
inst✝⁹ : T2Space X
inst✝⁸ : CompactSpace X
inst✝⁷ : TopologicalSpace Y
inst✝⁶ : CompactSpace Y
inst✝⁵ : AddCommGroup V
inst✝⁴ : UniformSpace V
inst✝³ : IsUniformAddGroup V
S : Set (V × V)
inst✝² : TopologicalSpace R
inst✝¹ : MonoidWithZero R
inst✝ : MulActionWithZero R V
f : C(X × Y, V)
hS : S ∈ 𝓤 V
⊢ ∃ n g h, ∀ (x : X) (y : Y), (f (x, y), ∑ i, (g i) x • (h i) y) ∈ S

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Padics.HeightOneSpectrum

Goal state before:
pp: R✝ : Type u_1
inst✝⁷ : CommRing R✝
inst✝⁶ : Algebra R✝ ℚ
inst✝⁵ : IsIntegralClosure R✝ ℤ ℚ
R : Type u_2
inst✝⁴ : CommRing R
inst✝³ : Algebra R ℚ
inst✝² : IsIntegralClosure R ℤ ℚ
inst✝¹ : IsDedekindDomain R
inst✝ : IsFractionRing R ℚ
v : HeightOneSpectrum R
x✝ : HeightOneSpectrum.adicCompletion ℚ v
⊢ x✝ ∈ HeightOneSpectrum.adicCompletionIntegers ℚ v ↔
    (HeightOneSpectrum.adicCompletion.equiv ℚ v) x✝ ∈ Valued.v.valuationSubring

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Separation.DisjointCover

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
S : Set (X × X)
hS : S ∈ 𝓝ˢ (diagonal X)
x : X
⊢ ∃ U, IsOpen[inst✝] U ∧ x ∈ U ∧ U ×ˢ U ⊆ S

Tactic:
by

Goal state after:
Module: Mathlib.Topology.UniformSpace.ProdApproximation

Goal state before:
pp: X✝ : Type u_1
Y✝ : Type u_2
R✝ : Type u_3
V : Type u_4
inst✝¹³ : TopologicalSpace X✝
inst✝¹² : TotallyDisconnectedSpace X✝
inst✝¹¹ : T2Space X✝
inst✝¹⁰ : CompactSpace X✝
inst✝⁹ : TopologicalSpace Y✝
inst✝⁸ : CompactSpace Y✝
inst✝⁷ : AddCommGroup V
inst✝⁶ : UniformSpace V
inst✝⁵ : IsUniformAddGroup V
S : Set (V × V)
X : Type u_5
Y : Type u_6
R : Type u_7
inst✝⁴ : TopologicalSpace X
inst✝³ : TopologicalSpace Y
inst✝² : CommRing R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalRing R
f f' : C(X, R)
g : C(Y, R)
⊢ (f + f').comp fst * g.comp snd = f.comp fst * g.comp snd + f'.comp fst * g.comp snd

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Padics.HeightOneSpectrum

Goal state before:
pp: R✝ : Type u_1
inst✝⁷ : CommRing R✝
inst✝⁶ : Algebra R✝ ℚ
inst✝⁵ : IsIntegralClosure R✝ ℤ ℚ
R : Type u_2
inst✝⁴ : CommRing R
inst✝³ : Algebra R ℚ
inst✝² : IsIntegralClosure R ℤ ℚ
inst✝¹ : IsDedekindDomain R
inst✝ : IsFractionRing R ℚ
v : HeightOneSpectrum R
e0 : ↥(HeightOneSpectrum.adicCompletionIntegers ℚ v) ≃+* ↥Valued.v.valuationSubring :=
  (HeightOneSpectrum.adicCompletion.equiv ℚ v).restrict (HeightOneSpectrum.adicCompletionIntegers ℚ v)
    Valued.v.valuationSubring ⋯
x✝ : UniformSpace.Completion (WithVal (HeightOneSpectrum.valuation ℚ v))
⊢ x✝ ∈ Valued.v.valuationSubring ↔
    (mapRingEquiv (WithVal.congr (HeightOneSpectrum.valuation ℚ v) (padicValuation ↑(primesEquiv v)) (RingEquiv.refl ℚ))
          ⋯ ⋯)
        x✝ ∈
      Valued.integer (padicValuation ↑(primesEquiv v)).Completion

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Separation.DisjointCover

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
S : Set (X × X)
inst✝ : CompactSpace X
hS : S ∈ 𝓝ˢ (diagonal X)
⊢ ∃ t U, IsOpenCover U ∧ ∀ (i : ↥t), ↑(U i) ×ˢ ↑(U i) ⊆ S

Tactic:
by

Goal state after:
Module: Mathlib.Topology.UniformSpace.ProdApproximation

Goal state before:
pp: X✝ : Type u_1
Y✝ : Type u_2
R✝ : Type u_3
V : Type u_4
inst✝¹³ : TopologicalSpace X✝
inst✝¹² : TotallyDisconnectedSpace X✝
inst✝¹¹ : T2Space X✝
inst✝¹⁰ : CompactSpace X✝
inst✝⁹ : TopologicalSpace Y✝
inst✝⁸ : CompactSpace Y✝
inst✝⁷ : AddCommGroup V
inst✝⁶ : UniformSpace V
inst✝⁵ : IsUniformAddGroup V
S : Set (V × V)
X : Type u_5
Y : Type u_6
R : Type u_7
inst✝⁴ : TopologicalSpace X
inst✝³ : TopologicalSpace Y
inst✝² : CommRing R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalRing R
r : R
f : C(X, R)
g : C(Y, R)
⊢ (r • f).comp fst * g.comp snd = r • (f.comp fst * g.comp snd)

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Padics.HeightOneSpectrum

Goal state before:
pp: R✝ : Type u_1
inst✝⁷ : CommRing R✝
inst✝⁶ : Algebra R✝ ℚ
inst✝⁵ : IsIntegralClosure R✝ ℤ ℚ
R : Type u_2
inst✝⁴ : CommRing R
inst✝³ : Algebra R ℚ
inst✝² : IsIntegralClosure R ℤ ℚ
inst✝¹ : IsDedekindDomain R
inst✝ : IsFractionRing R ℚ
v : HeightOneSpectrum R
x✝ : HeightOneSpectrum.adicCompletion ℚ v
⊢ x✝ ∈ HeightOneSpectrum.adicCompletionIntegers ℚ v ↔
    (HeightOneSpectrum.adicCompletion.uniformEquiv ℚ v) x✝ ∈ Valued.v.valuationSubring

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Separation.DisjointCover

Goal state before:
pp: X : Type u_1
inst✝³ : TopologicalSpace X
S : Set (X × X)
inst✝² : CompactSpace X
inst✝¹ : TotallyDisconnectedSpace X
inst✝ : T2Space X
hS : S ∈ 𝓝ˢ (diagonal X)
⊢ ∃ n D,
    (∀ (i : Fin n), D i ≠ ⊥) ∧
      (∀ (i : Fin n), ∀ y ∈ D i, ∀ z ∈ D i, (y, z) ∈ S) ∧ univ ⊆ ⋃ i, ↑(D i) ∧ Pairwise (Disjoint on D)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.UniformSpace.ProdApproximation

Goal state before:
pp: X✝ : Type u_1
Y✝ : Type u_2
R✝ : Type u_3
V : Type u_4
inst✝¹³ : TopologicalSpace X✝
inst✝¹² : TotallyDisconnectedSpace X✝
inst✝¹¹ : T2Space X✝
inst✝¹⁰ : CompactSpace X✝
inst✝⁹ : TopologicalSpace Y✝
inst✝⁸ : CompactSpace Y✝
inst✝⁷ : AddCommGroup V
inst✝⁶ : UniformSpace V
inst✝⁵ : IsUniformAddGroup V
S : Set (V × V)
X : Type u_5
Y : Type u_6
R : Type u_7
inst✝⁴ : TopologicalSpace X
inst✝³ : TopologicalSpace Y
inst✝² : CommRing R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalRing R
f : C(X, R)
g g' : C(Y, R)
⊢ f.comp fst * (g + g').comp snd = f.comp fst * g.comp snd + f.comp fst * g'.comp snd

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Padics.HeightOneSpectrum

Goal state before:
pp: R✝ : Type u_1
inst✝⁷ : CommRing R✝
inst✝⁶ : Algebra R✝ ℚ
inst✝⁵ : IsIntegralClosure R✝ ℤ ℚ
R : Type u_2
inst✝⁴ : CommRing R
inst✝³ : Algebra R ℚ
inst✝² : IsIntegralClosure R ℤ ℚ
inst✝¹ : IsDedekindDomain R
inst✝ : IsFractionRing R ℚ
v : HeightOneSpectrum R
e0 : ↥(HeightOneSpectrum.adicCompletionIntegers ℚ v) ≃ᵤ ↥Valued.v.valuationSubring :=
  (HeightOneSpectrum.adicCompletion.uniformEquiv ℚ v).subtype ⋯
x✝ : UniformSpace.Completion (WithVal (HeightOneSpectrum.valuation ℚ v))
⊢ x✝ ∈ Valued.v.valuationSubring ↔
    (mapEquiv (withValEquiv v)) x✝ ∈ Valued.integer (padicValuation ↑(primesEquiv v)).Completion

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Separation.DisjointCover

Goal state before:
pp: X : Type u_1
V : Type u_2
inst✝⁴ : TopologicalSpace X
inst✝³ : TopologicalSpace V
inst✝² : TotallyDisconnectedSpace X
inst✝¹ : T2Space X
inst✝ : CompactSpace X
S : Set (V × V)
f : C(X, V)
hS : S ∈ 𝓝ˢ (diagonal V)
⊢ ⇑(f.prodMap f) ⁻¹' S ∈ 𝓝ˢ (diagonal X)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Separation.DisjointCover

Goal state before:
pp: X : Type u_1
V : Type u_2
inst✝⁴ : TopologicalSpace X
inst✝³ : TopologicalSpace V
inst✝² : TotallyDisconnectedSpace X
inst✝¹ : T2Space X
inst✝ : CompactSpace X
S : Set (V × V)
f : C(X, V)
hS : S ∈ 𝓝ˢ (diagonal V)
⊢ ∃ n D,
    (∀ (i : Fin n), D i ≠ ⊥) ∧
      (∀ (i : Fin n), ∀ y ∈ D i, ∀ z ∈ D i, (f y, f z) ∈ S) ∧ univ ⊆ ⋃ i, ↑(D i) ∧ Pairwise (Disjoint on D)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.UniformSpace.ProdApproximation

Goal state before:
pp: X✝ : Type u_1
Y✝ : Type u_2
R✝ : Type u_3
V : Type u_4
inst✝¹³ : TopologicalSpace X✝
inst✝¹² : TotallyDisconnectedSpace X✝
inst✝¹¹ : T2Space X✝
inst✝¹⁰ : CompactSpace X✝
inst✝⁹ : TopologicalSpace Y✝
inst✝⁸ : CompactSpace Y✝
inst✝⁷ : AddCommGroup V
inst✝⁶ : UniformSpace V
inst✝⁵ : IsUniformAddGroup V
S : Set (V × V)
X : Type u_5
Y : Type u_6
R : Type u_7
inst✝⁴ : TopologicalSpace X
inst✝³ : TopologicalSpace Y
inst✝² : CommRing R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalRing R
r : R
f : C(X, R)
g : C(Y, R)
⊢ f.comp fst * (r • g).comp snd = r • (f.comp fst * g.comp snd)

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Padics.HeightOneSpectrum

Goal state before:
pp: R✝ : Type u_1
inst✝⁷ : CommRing R✝
inst✝⁶ : Algebra R✝ ℚ
inst✝⁵ : IsIntegralClosure R✝ ℤ ℚ
R : Type u_2
inst✝⁴ : CommRing R
inst✝³ : Algebra R ℚ
inst✝² : IsIntegralClosure R ℤ ℚ
inst✝¹ : IsDedekindDomain R
inst✝ : IsFractionRing R ℚ
v : HeightOneSpectrum R
⊢ ∀ (r : ℤ),
    (let e0 :=
            (HeightOneSpectrum.adicCompletion.equiv ℚ v).restrict (HeightOneSpectrum.adicCompletionIntegers ℚ v)
              Valued.v.valuationSubring ⋯;
          let e :=
            (mapRingEquiv
                  (WithVal.congr (HeightOneSpectrum.valuation ℚ v) (padicValuation ↑(primesEquiv v)) (RingEquiv.refl ℚ))
                  ⋯ ⋯).restrict
              Valued.v.valuationSubring (Valued.integer (padicValuation ↑(primesEquiv v)).Completion) ⋯;
          (e0.trans e).trans withValIntegersRingEquiv).toFun
        ((algebraMap ℤ ↥(HeightOneSpectrum.adicCompletionIntegers ℚ v)) r) =
      (algebraMap ℤ ℤ_[↑(primesEquiv v)]) r

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Separation.DisjointCover

Goal state before:
pp: X : Type u_1
V : Type u_2
inst✝⁴ : TopologicalSpace X
inst✝³ : TopologicalSpace V
inst✝² : TotallyDisconnectedSpace X
inst✝¹ : T2Space X
inst✝ : CompactSpace X
S : Set (V × V)
f : C(X, V)
hS : S ∈ 𝓝ˢ (diagonal V)
n : ℕ
E : Fin n → Clopens X
hEne : ∀ (i : Fin n), E i ≠ ⊥
hES : ∀ (i : Fin n), ∀ y ∈ E i, ∀ z ∈ E i, (f y, f z) ∈ S
hEuniv : univ ⊆ ⋃ i, ↑(E i)
hEdis : Pairwise (Disjoint on E)
x : X
⊢ ∃! i, x ∈ E i

Tactic:
by

Goal state after:
Module: Mathlib.Topology.UniformSpace.ProdApproximation

Goal state before:
pp: X : Type u_5
Y : Type u_6
R : Type u_7
inst✝⁴ : TopologicalSpace X
inst✝³ : TopologicalSpace Y
inst✝² : CommRing R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalRing R
f : C(X, R)
g : C(Y, R)
⊢ tensorHom (f ⊗ₜ[R] g) = (prodMul f) g

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Separation.DisjointCover

Goal state before:
pp: X : Type u_1
V : Type u_2
inst✝⁴ : TopologicalSpace X
inst✝³ : TopologicalSpace V
inst✝² : TotallyDisconnectedSpace X
inst✝¹ : T2Space X
inst✝ : CompactSpace X
S : Set (V × V)
f : C(X, V)
hS : S ∈ 𝓝ˢ (diagonal V)
n : ℕ
E : Fin n → Clopens X
hEne : ∀ (i : Fin n), E i ≠ ⊥
hES : ∀ (i : Fin n), ∀ y ∈ E i, ∀ z ∈ E i, (f y, f z) ∈ S
hEuniv : univ ⊆ ⋃ i, ↑(E i)
hEdis : Pairwise (Disjoint on E)
g : X → Fin n
hg : ∀ (x : X), (fun i ↦ x ∈ E i) (g x)
hg' : ∀ (x : X) (y : Fin n), (fun i ↦ x ∈ E i) y → y = g x
i : Fin n
⊢ ∃ x, x ∈ E i

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Separation.DisjointCover

Goal state before:
pp: X : Type u_1
V : Type u_2
inst✝⁴ : TopologicalSpace X
inst✝³ : TopologicalSpace V
inst✝² : TotallyDisconnectedSpace X
inst✝¹ : T2Space X
inst✝ : CompactSpace X
S : Set (V × V)
f : C(X, V)
hS : S ∈ 𝓝ˢ (diagonal V)
⊢ ∃ n g h, Continuous[inst✝⁴, _] g ∧ ∀ (x : X), (f x, h (g x)) ∈ S

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Separation.DisjointCover

Goal state before:
pp: X : Type u_1
V : Type u_2
inst✝⁴ : TopologicalSpace X
inst✝³ : TopologicalSpace V
inst✝² : TotallyDisconnectedSpace X
inst✝¹ : T2Space X
inst✝ : CompactSpace X
S : Set (V × V)
f : C(X, V)
hS : S ∈ 𝓝ˢ (diagonal V)
⊢ ∃ n g h, Continuous[inst✝⁴, _] g ∧ ∀ (x : X), (f x, h (g x)) ∈ S

Tactic:
by
  obtain ⟨n, E, hEne, hES, hEuniv, hEdis⟩ :=
    exists_disjoint_nonempty_clopen_cover_of_mem_nhds_diagonal f hS
  have h_uniq (x) : ∃! i, x ∈ E i := by
    refine match mem_iUnion.mp (hEuniv <| mem_univ x) with
      | ⟨i, hi⟩ => ⟨i, hi, fun j hj ↦ hEdis.eq ?_⟩
    simpa [← Clopens.coe_disjoint, not_disjoint_iff] using! ⟨x, hj, hi⟩
  choose g hg hg' using h_uniq -- for each `x`, `g x` is the unique `i` such that `x ∈ E i`
  have h_ex (i) : ∃ x, x ∈ E i := by
    simpa [← SetLike.coe_set_eq, ← nonempty_iff_ne_empty] using! hEne i
  choose r hr using h_ex -- for each `i`, choose an `r i ∈ E i`
  refine ⟨n, g, f ∘ r, continuous_discrete_rng.mpr fun j ↦ ?_, fun x ↦ (hES _) _ (hg _) _ (hr _)⟩
  convert! (E j).isOpen
  exact Set.ext fun x ↦ ⟨fun hj ↦ hj ▸ hg x, fun hx ↦ (hg' _ _ hx).symm⟩

Goal state after:
Module: Mathlib.Topology.Separation.DisjointCover

Goal state before:
pp: X : Type u_1
V : Type u_2
inst✝⁵ : TopologicalSpace X
inst✝⁴ : TopologicalSpace V
inst✝³ : TotallyDisconnectedSpace X
inst✝² : T2Space X
inst✝¹ : CompactSpace X
S : Set (V × V)
f : C(X, V)
inst✝ : CommMonoid V
hS : S ∈ 𝓝ˢ (diagonal V)
⊢ ∃ n U v, ∀ (x : X), (f x, ∏ n, (↑(U n)).mulIndicator (fun x ↦ v n) x) ∈ S

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Padics.HeightOneSpectrum

Goal state before:
pp: R : Type u_2
inst✝⁴ : CommRing R
inst✝³ : Algebra R ℚ
inst✝² : IsIntegralClosure R ℤ ℚ
inst✝¹ : IsDedekindDomain R
inst✝ : IsFractionRing R ℚ
v : HeightOneSpectrum R
y : ℚ_[↑(primesEquiv v)]
hy : y ∈ ↑(subring ↑(primesEquiv v))
x : ↥(HeightOneSpectrum.adicCompletionIntegers ℚ v)
hx : (adicCompletionIntegers.padicIntEquiv v) x = ⟨y, hy⟩
⊢ (padicEquiv v) ↑x = y

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Padics.HeightOneSpectrum

Goal state before:
pp: R : Type u_2
inst✝⁴ : CommRing R
inst✝³ : Algebra R ℚ
inst✝² : IsIntegralClosure R ℤ ℚ
inst✝¹ : IsDedekindDomain R
inst✝ : IsFractionRing R ℚ
v : HeightOneSpectrum R
⊢ Set.BijOn ⇑(padicEquiv v) ↑(HeightOneSpectrum.adicCompletionIntegers ℚ v) ↑(subring ↑(primesEquiv v))

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Padics.HeightOneSpectrum

Goal state before:
pp: R✝ : Type u_1
inst✝⁷ : CommRing R✝
inst✝⁶ : Algebra R✝ ℚ
inst✝⁵ : IsIntegralClosure R✝ ℤ ℚ
R : Type u_2
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
inst✝² : Algebra R ℚ
inst✝¹ : IsFractionRing R ℚ
inst✝ : IsIntegralClosure R ℤ ℚ
p : Nat.Primes
⊢ ℚ_[↑p] ≃A[ℚ] HeightOneSpectrum.adicCompletion ℚ (primesEquiv.symm p)

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Padics.HeightOneSpectrum

Goal state before:
pp: R✝ : Type u_1
inst✝⁷ : CommRing R✝
inst✝⁶ : Algebra R✝ ℚ
inst✝⁵ : IsIntegralClosure R✝ ℤ ℚ
R : Type u_2
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
inst✝² : Algebra R ℚ
inst✝¹ : IsFractionRing R ℚ
inst✝ : IsIntegralClosure R ℤ ℚ
p : Nat.Primes
⊢ ℤ_[↑p] ≃A[ℤ] ↥(HeightOneSpectrum.adicCompletionIntegers ℚ (primesEquiv.symm p))

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Padics.HeightOneSpectrum

Goal state before:
pp: R : Type u_2
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
inst✝² : Algebra R ℚ
inst✝¹ : IsFractionRing R ℚ
inst✝ : IsIntegralClosure R ℤ ℚ
p : Nat.Primes
x : ℤ_[↑p]
⊢ ℚ_[↑(primesEquiv (primesEquiv.symm p))] = ℚ_[↑p]

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Padics.HeightOneSpectrum

Goal state before:
pp: R : Type u_2
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
inst✝² : Algebra R ℚ
inst✝¹ : IsFractionRing R ℚ
inst✝ : IsIntegralClosure R ℤ ℚ
p : Nat.Primes
x : ℤ_[↑p]
⊢ (fun x ↦ ‖x‖ ≤ 1) ≍ fun x ↦ ‖x‖ ≤ 1

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Padics.HeightOneSpectrum

Goal state before:
pp: R : Type u_2
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
inst✝² : Algebra R ℚ
inst✝¹ : IsFractionRing R ℚ
inst✝ : IsIntegralClosure R ℤ ℚ
p : Nat.Primes
x : ℤ_[↑p]
⊢ ↑((adicCompletionIntegersEquiv R p) x) = (adicCompletionEquiv R p) ↑x

Tactic:
by

Goal state after: