awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Algebra.Support
Goal:
X : Type u_9
Y : Type u_10
inst : TopologicalSpace X
inst_1 : TopologicalSpace Y
M : Type u_11
inst_2 : One M
f : Y → M
hf : HasCompactMulSupport f
φ : X ≃ₜ Y
⊢ HasCompactMulSupport.{u_9, u_11} (α := X) (f ∘ (⇑φ : (a : X) → Y))

Tactic:
hf.comp_isClosedEmbedding φ.isClosedEmbedding

Premises used: HasCompactMulSupport.comp_isClosedEmbedding, Homeomorph.isClosedEmbedding
-- Module: Mathlib.Topology.Algebra.TopologicallyNilpotent
Goal:
R : Type u_1
S : Type u_2
inst : TopologicalSpace R
inst_1 : MonoidWithZero R
inst_2 : MonoidWithZero S
inst_3 : TopologicalSpace S
F : Type u_3
inst_4 : FunLike F R S
inst_5 : MonoidWithZeroHomClass F R S
φ : F
hφ : Continuous[inst, inst_3] (⇑φ : (a : R) → S)
a : R
ha : Tendsto.{0, u_1} (β := R) (fun (x : ℕ) ↦ a ^ x) atTop (𝓝 0)
simp_rw : Tendsto.{0, u_2} (β := S) (fun (x : ℕ) ↦ (φ : (a : R) → S) (a ^ x)) atTop (𝓝 0)
⊢ Tendsto.{0, u_2} (β := S) (fun (x : ℕ) ↦ HPow.hPow (α := S) ((φ : (a : R) → S) a : S) x) atTop (𝓝 0)

Tactic:
simp_rw [← map_pow]

Premises used: map_pow
-- Module: Mathlib.Topology.Algebra.TopologicallyNilpotent
Goal:
R : Type u_1
S : Type u_2
inst : TopologicalSpace R
inst_1 : MonoidWithZero R
inst_2 : MonoidWithZero S
inst_3 : TopologicalSpace S
F : Type u_3
inst_4 : FunLike F R S
inst_5 : MonoidWithZeroHomClass F R S
φ : F
hφ : Continuous[inst, inst_3] (⇑φ : (a : R) → S)
a : R
ha : Tendsto.{0, u_1} (β := R) (fun (x : ℕ) ↦ a ^ x) atTop (𝓝 0)
⊢ Tendsto.{0, u_2} (β := S) (fun (x : ℕ) ↦ (φ : (a : R) → S) (a ^ x)) atTop (𝓝 0)

Tactic:
exact (map_zero φ ▸ hφ.tendsto 0).comp ha
-- Module: Mathlib.Topology.Algebra.TopologicallyNilpotent
Goal:
R : Type u_1
inst : TopologicalSpace R
inst_1 : MonoidWithZero R
x : ℕ
hi : x ≥ 1
rw rw₁ : Eq.{u_1 + 1} (α := R) 0 0
⊢ HPow.hPow (α := R) 0 x = 0

Tactic:
rw [zero_pow (Nat.ne_zero_iff_zero_lt.mpr hi)]

Premises used: Iff.mpr, Nat.ne_zero_iff_zero_lt, zero_pow
-- Module: Mathlib.Topology.Algebra.TopologicallyNilpotent
Goal:
R : Type u_1
inst : TopologicalSpace R
inst_1 : MonoidWithZero R
a : R
ha : IsNilpotent a
obtain : ∀ (n : ℕ) (hn : a ^ n = 0), IsTopologicallyNilpotent a
⊢ IsTopologicallyNilpotent a

Tactic:
obtain ⟨n, hn⟩ := ha
-- Module: Mathlib.Topology.Algebra.TopologicallyNilpotent
Goal:
R : Type u_1
inst : TopologicalSpace R
inst_1 : MonoidWithZero R
a : R
n : ℕ
hn : a ^ n = 0
apply : ∀ i ≥ n, a ^ i = 0
⊢ IsTopologicallyNilpotent a

Tactic:
apply tendsto_atTop_of_eventually_const (i₀ := n)

Premises used: tendsto_atTop_of_eventually_const
-- Module: Mathlib.Topology.Algebra.TopologicallyNilpotent
Goal:
R : Type u_1
inst : TopologicalSpace R
inst_1 : MonoidWithZero R
a : R
n : ℕ
hn : a ^ n = 0
i : ℕ
hi : i ≥ n
rw : a ^ (n + (i - n)) = 0
rw₁ : a ^ n * a ^ (i - n) = 0
rw₂ : 0 * a ^ (i - n) = 0
rw₃ rw₄ : Eq.{u_1 + 1} (α := R) 0 0
⊢ a ^ i = 0

Tactic:
rw [← Nat.add_sub_of_le hi, pow_add, hn, zero_mul]

Premises used: MulZeroClass.zero_mul, pow_add, Nat.add_sub_of_le
-- Module: Mathlib.Topology.Algebra.TopologicallyNilpotent
Goal:
R : Type u_1
inst : TopologicalSpace R
inst_1 : MonoidWithZero R
a : R
ha : IsTopologicallyNilpotent a
v : Set R
hv : Membership.mem (γ := Filter R) (𝓝 0) v
⊢ ∃ (n : ℕ), a ^ n ∈ v

Tactic:
(ha.eventually_mem hv).exists

Premises used: Filter.Tendsto.eventually_mem, Filter.Eventually.exists
-- Module: Mathlib.Topology.Algebra.TopologicallyNilpotent
Goal:
R : Type u_1
inst : TopologicalSpace R
inst_1 : Ring R
inst_2 : IsLinearTopology Rᵐᵒᵖ R
a b : R
ha : IsTopologicallyNilpotent a
hab : Commute a b
simp_rw : Tendsto.{0, u_1} (β := R) (fun (x : ℕ) ↦ a ^ x * b ^ x) atTop (𝓝 0)
⊢ IsTopologicallyNilpotent (a * b)

Tactic:
simp_rw [IsTopologicallyNilpotent, hab.mul_pow]

Premises used: IsTopologicallyNilpotent, Commute.mul_pow
-- Module: Mathlib.Topology.Algebra.TopologicallyNilpotent
Goal:
R : Type u_1
inst : TopologicalSpace R
inst_1 : Ring R
inst_2 : IsLinearTopology Rᵐᵒᵖ R
a b : R
ha : IsTopologicallyNilpotent a
hab : Commute a b
⊢ Tendsto.{0, u_1} (β := R) (fun (x : ℕ) ↦ a ^ x * b ^ x) atTop (𝓝 0)

Tactic:
IsLinearTopology.tendsto_mul_zero_of_left _ _ ha

Premises used: IsLinearTopology.tendsto_mul_zero_of_left
-- Module: Mathlib.Topology.Algebra.TopologicallyNilpotent
Goal:
R : Type u_1
inst : TopologicalSpace R
inst_1 : Ring R
inst_2 : IsLinearTopology Rᵐᵒᵖ R
a b : R
ha : IsTopologicallyNilpotent a
hab : Commute a b
⊢ Tendsto.{0, u_1} (β := R) (fun (x : ℕ) ↦ a ^ x * b ^ x) atTop (𝓝 0)

Tactic:
exact IsLinearTopology.tendsto_mul_zero_of_left _ _ ha

Premises used: IsLinearTopology.tendsto_mul_zero_of_left
-- Module: Mathlib.Topology.Algebra.TopologicallyNilpotent
Goal:
R : Type u_1
inst : TopologicalSpace R
inst_1 : Ring R
inst_2 : IsLinearTopology R R
a b : R
hb : IsTopologicallyNilpotent b
hab : Commute a b
simp_rw : Tendsto.{0, u_1} (β := R) (fun (x : ℕ) ↦ a ^ x * b ^ x) atTop (𝓝 0)
⊢ IsTopologicallyNilpotent (a * b)

Tactic:
simp_rw [IsTopologicallyNilpotent, hab.mul_pow]

Premises used: IsTopologicallyNilpotent, Commute.mul_pow
-- Module: Mathlib.Topology.Algebra.TopologicallyNilpotent
Goal:
R : Type u_1
inst : TopologicalSpace R
inst_1 : Ring R
inst_2 : IsLinearTopology R R
a b : R
hb : IsTopologicallyNilpotent b
hab : Commute a b
⊢ Tendsto.{0, u_1} (β := R) (fun (x : ℕ) ↦ a ^ x * b ^ x) atTop (𝓝 0)

Tactic:
IsLinearTopology.tendsto_mul_zero_of_right _ _ hb

Premises used: IsLinearTopology.tendsto_mul_zero_of_right
-- Module: Mathlib.Topology.Algebra.TopologicallyNilpotent
Goal:
R : Type u_1
inst : TopologicalSpace R
inst_1 : Ring R
inst_2 : IsLinearTopology R R
a b : R
hb : IsTopologicallyNilpotent b
hab : Commute a b
⊢ Tendsto.{0, u_1} (β := R) (fun (x : ℕ) ↦ a ^ x * b ^ x) atTop (𝓝 0)

Tactic:
exact IsLinearTopology.tendsto_mul_zero_of_right _ _ hb

Premises used: IsLinearTopology.tendsto_mul_zero_of_right
-- Module: Mathlib.Topology.Algebra.TopologicallyNilpotent
Goal:
R : Type u_1
inst : TopologicalSpace R
inst_1 : Ring R
inst_2 : IsLinearTopology R R
a b : R
ha : IsTopologicallyNilpotent a
hb : IsTopologicallyNilpotent b
h : Commute a b
simp :
  ∀ (ib : Ideal R),
    Membership.mem (γ := Filter R) (𝓝 0) (↑ib : Set R) → ∃ (ia : ℕ), ∀ x ∈ Set.Ici ia, (a + b) ^ x ∈ (↑ib : Set R)
⊢ IsTopologicallyNilpotent (a + b)

Tactic:
simp only [IsTopologicallyNilpotent, atTop_basis.tendsto_iff IsLinearTopology.hasBasis_ideal,
    true_and]

Premises used: Filter.atTop_basis, Filter.HasBasis.tendsto_iff, IsTopologicallyNilpotent, IsLinearTopology.hasBasis_ideal, true_and
-- Module: Mathlib.Topology.Algebra.TopologicallyNilpotent
Goal:
R : Type u_1
inst : TopologicalSpace R
inst_1 : Ring R
inst_2 : IsLinearTopology R R
a b : R
ha : IsTopologicallyNilpotent a
hb : IsTopologicallyNilpotent b
h : Commute a b
I : Ideal R
I_mem_nhds : Membership.mem (γ := Filter R) (𝓝 0) (↑I : Set R)
obtain : ∀ (na : ℕ) (ha : a ^ na ∈ (↑I : Set R)), ∃ (ia : ℕ), ∀ x ∈ Set.Ici ia, (a + b) ^ x ∈ (↑I : Set R)
⊢ ∃ (ia : ℕ), ∀ x ∈ Set.Ici ia, (a + b) ^ x ∈ (↑I : Set R)

Tactic:
obtain ⟨na, ha⟩ := ha.exists_pow_mem_of_mem_nhds I_mem_nhds

Premises used: IsTopologicallyNilpotent.exists_pow_mem_of_mem_nhds
-- Module: Mathlib.Topology.Algebra.TopologicallyNilpotent
Goal:
R : Type u_1
inst : TopologicalSpace R
inst_1 : Ring R
inst_2 : IsLinearTopology R R
a b : R
ha_1 : IsTopologicallyNilpotent a
hb : IsTopologicallyNilpotent b
h : Commute a b
I : Ideal R
I_mem_nhds : Membership.mem (γ := Filter R) (𝓝 0) (↑I : Set R)
na : ℕ
ha : a ^ na ∈ (↑I : Set R)
obtain : ∀ (nb : ℕ) (hb : b ^ nb ∈ (↑I : Set R)), ∃ (ia : ℕ), ∀ x ∈ Set.Ici ia, (a + b) ^ x ∈ (↑I : Set R)
⊢ ∃ (ia : ℕ), ∀ x ∈ Set.Ici ia, (a + b) ^ x ∈ (↑I : Set R)

Tactic:
obtain ⟨nb, hb⟩ := hb.exists_pow_mem_of_mem_nhds I_mem_nhds

Premises used: IsTopologicallyNilpotent.exists_pow_mem_of_mem_nhds
-- Module: Mathlib.Topology.Algebra.TopologicallyNilpotent
Goal:
R : Type u_1
inst : TopologicalSpace R
inst_1 : Ring R
inst_2 : IsLinearTopology R R
a b : R
ha_1 : IsTopologicallyNilpotent a
hb_1 : IsTopologicallyNilpotent b
h : Commute a b
I : Ideal R
I_mem_nhds : Membership.mem (γ := Filter R) (𝓝 0) (↑I : Set R)
na : ℕ
ha : a ^ na ∈ (↑I : Set R)
nb : ℕ
hb : b ^ nb ∈ (↑I : Set R)
⊢ ∃ (ia : ℕ), ∀ x ∈ Set.Ici ia, (a + b) ^ x ∈ (↑I : Set R)

Tactic:
⟨na + nb, fun m hm ↦
    I.add_pow_mem_of_pow_mem_of_le_of_commute ha hb (le_trans hm (Nat.le_add_right _ _)) h⟩

Premises used: Nat.le_add_right, HAdd.hAdd, Exists.intro, Ideal.add_pow_mem_of_pow_mem_of_le_of_commute, OfNat.ofNat, le_trans
-- Module: Mathlib.Topology.Algebra.TopologicallyNilpotent
Goal:
R : Type u_1
inst : TopologicalSpace R
inst_1 : Ring R
inst_2 : IsLinearTopology R R
a b : R
ha_1 : IsTopologicallyNilpotent a
hb_1 : IsTopologicallyNilpotent b
h : Commute a b
I : Ideal R
I_mem_nhds : Membership.mem (γ := Filter R) (𝓝 0) (↑I : Set R)
na : ℕ
ha : a ^ na ∈ (↑I : Set R)
nb : ℕ
hb : b ^ nb ∈ (↑I : Set R)
⊢ ∃ (ia : ℕ), ∀ x ∈ Set.Ici ia, (a + b) ^ x ∈ (↑I : Set R)

Tactic:
exact ⟨na + nb, fun m hm ↦
    I.add_pow_mem_of_pow_mem_of_le_of_commute ha hb (le_trans hm (Nat.le_add_right _ _)) h⟩
-- Module: Mathlib.Topology.Algebra.TopologicallyNilpotent
Goal:
R : Type u_1
inst : TopologicalSpace R
inst_1 : CommRing R
inst_2 : IsLinearTopology R R
a : R
ha : IsTopologicallyNilpotent a
b : R
⊢ IsTopologicallyNilpotent (a * b)

Tactic:
ha.mul_right_of_commute (Commute.all ..)

Premises used: Commute.all, IsTopologicallyNilpotent.mul_right_of_commute
-- Module: Mathlib.Topology.Algebra.TopologicallyNilpotent
Goal:
R : Type u_1
inst : TopologicalSpace R
inst_1 : CommRing R
inst_2 : IsLinearTopology R R
a b : R
hb : IsTopologicallyNilpotent b
⊢ IsTopologicallyNilpotent (a * b)

Tactic:
hb.mul_left_of_commute (Commute.all ..)

Premises used: IsTopologicallyNilpotent.mul_left_of_commute, Commute.all
-- Module: Mathlib.Topology.Algebra.TopologicallyNilpotent
Goal:
R : Type u_1
inst : TopologicalSpace R
inst_1 : CommRing R
inst_2 : IsLinearTopology R R
a b : R
ha : IsTopologicallyNilpotent a
hb : IsTopologicallyNilpotent b
⊢ IsTopologicallyNilpotent (a + b)

Tactic:
ha.add_of_commute hb (Commute.all ..)

Premises used: IsTopologicallyNilpotent.add_of_commute, Commute.all
-- Module: Mathlib.Topology.Algebra.TopologicallyNilpotent
Goal:
R : Type u_1
inst : TopologicalSpace R
inst_1 : CommRing R
inst_2 : IsLinearTopology R R
a : R
⊢ Membership.mem (γ := Ideal R) (topologicalNilradical R) a ↔ IsTopologicallyNilpotent a

Tactic:
simp [topologicalNilradical]

Premises used: topologicalNilradical
-- Module: Mathlib.Topology.Algebra.UniformField
Goal:
K : Type u_1
inst : Field K
inst_1 : UniformSpace K
inst_2 : T0Space K
⊢ Nontrivial.{u_1} (hat K)

Tactic:
(isUniformEmbedding_coe K).injective.nontrivial

Premises used: IsUniformEmbedding.injective, Function.Injective.nontrivial, UniformSpace.Completion.isUniformEmbedding_coe
-- Module: Mathlib.Topology.Algebra.UniformField
Goal:
K : Type u_1
inst : Field K
inst_1 : UniformSpace K
inst_2 : CompletableTopField K
x : hat K
h : x ≠ 0
⊢ ContinuousAt hatInv x

Tactic:
isDenseInducing_coe.continuousAt_extend ?_

Premises used: UniformSpace.Completion.hatInv, IsDenseInducing.continuousAt_extend, UniformSpace.Completion.isDenseInducing_coe
-- Module: Mathlib.Topology.Algebra.UniformField
Goal:
K : Type u_1
inst : Field K
inst_1 : UniformSpace K
inst_2 : CompletableTopField K
x : hat K
h : x ≠ 0
refine : ∀ᶠ (x : hat K) in 𝓝 x, ∃ (c : hat K), Tendsto (fun (x : K) ↦ (↑x⁻¹ : hat K)) (Filter.comap coe' (𝓝 x)) (𝓝 c)
⊢ ContinuousAt hatInv x

Tactic:
refine isDenseInducing_coe.continuousAt_extend ?_

Premises used: IsDenseInducing.continuousAt_extend, UniformSpace.Completion.isDenseInducing_coe
-- Module: Mathlib.Topology.Algebra.UniformField
Goal:
K : Type u_1
inst : Field K
inst_1 : UniformSpace K
inst_2 : CompletableTopField K
x : hat K
h : x ≠ 0
apply :
  Subset (α := Set (hat K)) {0}ᶜ
    {x : hat K |
      (fun (x : hat K) ↦ ∃ (c : hat K), Tendsto (fun (x : K) ↦ (↑x⁻¹ : hat K)) (Filter.comap coe' (𝓝 x)) (𝓝 c)) x}
⊢ ∀ᶠ (x : hat K) in 𝓝 x, ∃ (c : hat K), Tendsto (fun (x : K) ↦ (↑x⁻¹ : hat K)) (Filter.comap coe' (𝓝 x)) (𝓝 c)

Tactic:
apply mem_of_superset (compl_singleton_mem_nhds h)

Premises used: compl_singleton_mem_nhds, Filter.mem_of_superset
-- Module: Mathlib.Topology.Algebra.UniformField
Goal:
K : Type u_1
inst : Field K
inst_1 : UniformSpace K
inst_2 : CompletableTopField K
x : hat K
h : x ≠ 0
y : hat K
y_ne : Membership.mem (γ := Set (hat K)) {0}ᶜ y
⊢ y ≠ 0

Tactic:
rw [mem_compl_singleton_iff] at y_ne

Premises used: Set.mem_compl_singleton_iff
-- Module: Mathlib.Topology.Algebra.UniformField
Goal:
K : Type u_1
inst : Field K
inst_1 : UniformSpace K
inst_2 : CompletableTopField K
x : hat K
h : x ≠ 0
y : hat K
y_ne : y ≠ 0
a : Cauchy (α := hat K) (map (fun (x : K) ↦ (↑x⁻¹ : hat K)) (Filter.comap coe' (𝓝 y)))
⊢ Membership.mem (γ := Set (hat K))
    {x : hat K |
      (fun (x : hat K) ↦ ∃ (c : hat K), Tendsto (fun (x : K) ↦ (↑x⁻¹ : hat K)) (Filter.comap coe' (𝓝 x)) (𝓝 c)) x}
    y

Tactic:
apply CompleteSpace.complete

Premises used: CompleteSpace.complete
-- Module: Mathlib.Topology.Algebra.UniformField
Goal:
K : Type u_1
inst : Field K
inst_1 : UniformSpace K
inst_2 : CompletableTopField K
x : hat K
h : x ≠ 0
y : hat K
y_ne : y ≠ 0
⊢ Eq.{u_1 + 1} (α := (x : K) → hat K) (fun (x : K) ↦ (↑x⁻¹ : hat K)) ((fun (y : K) ↦ (↑y : hat K)) ∘ fun (x : K) ↦ x⁻¹)

Tactic:
simp [Function.comp_def]

Premises used: Function.comp_def
-- Module: Mathlib.Topology.Algebra.UniformField
Goal:
K : Type u_1
inst : Field K
inst_1 : UniformSpace K
inst_2 : CompletableTopField K
x : hat K
h : x ≠ 0
y : hat K
y_ne : y ≠ 0
⊢ Eq.{u_1 + 1} (α := (x : K) → hat K) (fun (x : K) ↦ (↑x⁻¹ : hat K)) ((fun (y : K) ↦ (↑y : hat K)) ∘ fun (x : K) ↦ x⁻¹)

Tactic:
have : (fun (x : K) => (↑x⁻¹ : hat K)) =
      ((fun (y : K) => (↑y : hat K)) ∘ (fun (x : K) => (x⁻¹ : K))) := by
    simp [Function.comp_def]
-- Module: Mathlib.Topology.Algebra.UniformField
Goal:
K : Type u_1
inst : Field K
inst_1 : UniformSpace K
inst_2 : CompletableTopField K
x : hat K
h : x ≠ 0
y : hat K
y_ne : y ≠ 0
this :
  Eq.{u_1 + 1} (α := (x : K) → hat K) (fun (x : K) ↦ (↑x⁻¹ : hat K)) ((fun (y : K) ↦ (↑y : hat K)) ∘ fun (x : K) ↦ x⁻¹)
a : Cauchy (α := hat K) (map (fun (y : K) ↦ (↑y : hat K)) (map (fun (x : K) ↦ x⁻¹) (Filter.comap coe' (𝓝 y))))
⊢ Cauchy (α := hat K) (map (fun (x : K) ↦ (↑x⁻¹ : hat K)) (Filter.comap coe' (𝓝 y)))

Tactic:
rw [this, ← Filter.map_map]

Premises used: Filter.map_map
-- Module: Mathlib.Topology.Algebra.UniformField
Goal:
K : Type u_1
inst : Field K
inst_1 : UniformSpace K
inst_2 : CompletableTopField K
x : hat K
h : x ≠ 0
y : hat K
y_ne : y ≠ 0
this :
  Eq.{u_1 + 1} (α := (x : K) → hat K) (fun (x : K) ↦ (↑x⁻¹ : hat K)) ((fun (y : K) ↦ (↑y : hat K)) ∘ fun (x : K) ↦ x⁻¹)
apply : Cauchy (α := K) (map (fun (x : K) ↦ x⁻¹) (Filter.comap coe' (𝓝 y)))
⊢ Cauchy (α := hat K) (map (fun (y : K) ↦ (↑y : hat K)) (map (fun (x : K) ↦ x⁻¹) (Filter.comap coe' (𝓝 y))))

Tactic:
apply Cauchy.map _ (Completion.uniformContinuous_coe K)

Premises used: Cauchy.map, UniformSpace.Completion.uniformContinuous_coe
-- Module: Mathlib.Topology.Algebra.UniformField
Goal:
K : Type u_1
inst : Field K
inst_1 : UniformSpace K
inst_2 : CompletableTopField K
x : hat K
h : x ≠ 0
y : hat K
y_ne : y ≠ 0
this :
  Eq.{u_1 + 1} (α := (x : K) → hat K) (fun (x : K) ↦ (↑x⁻¹ : hat K)) ((fun (y : K) ↦ (↑y : hat K)) ∘ fun (x : K) ↦ x⁻¹)
a : Cauchy (Filter.comap coe' (𝓝 y))
a₁ : 𝓝 0 ⊓ Filter.comap coe' (𝓝 y) = ⊥
⊢ Cauchy (α := K) (map (fun (x : K) ↦ x⁻¹) (Filter.comap coe' (𝓝 y)))

Tactic:
apply CompletableTopField.nice

Premises used: CompletableTopField.nice
-- Module: Mathlib.Topology.Algebra.UniformField
Goal:
K : Type u_1
inst : Field K
inst_1 : UniformSpace K
inst_2 : CompletableTopField K
x : hat K
h : x ≠ 0
y : hat K
y_ne : y ≠ 0
this :
  Eq.{u_1 + 1} (α := (x : K) → hat K) (fun (x : K) ↦ (↑x⁻¹ : hat K)) ((fun (y : K) ↦ (↑y : hat K)) ∘ fun (x : K) ↦ x⁻¹)
⊢ (Filter.comap coe' (𝓝 y)).NeBot

Tactic:
haveI := isDenseInducing_coe.comap_nhds_neBot y
-- Module: Mathlib.Topology.Algebra.UniformField
Goal:
K : Type u_1
inst : Field K
inst_1 : UniformSpace K
inst_2 : CompletableTopField K
x : hat K
h : x ≠ 0
y : hat K
y_ne : y ≠ 0
this_1 :
  Eq.{u_1 + 1} (α := (x : K) → hat K) (fun (x : K) ↦ (↑x⁻¹ : hat K)) ((fun (y : K) ↦ (↑y : hat K)) ∘ fun (x : K) ↦ x⁻¹)
this : (Filter.comap coe' (𝓝 y)).NeBot
a :
  Filter.comap (β := hat K × hat K) (fun (p : K × K) ↦ ((↑p.1 : hat K), (↑p.2 : hat K))) (uniformity (hat K)) ≤
    uniformity K
⊢ Cauchy (Filter.comap coe' (𝓝 y))

Tactic:
apply cauchy_nhds.comap

Premises used: Cauchy.comap, cauchy_nhds
-- Module: Mathlib.Topology.Algebra.UniformField
Goal:
K : Type u_1
inst : Field K
inst_1 : UniformSpace K
inst_2 : CompletableTopField K
x : hat K
h : x ≠ 0
y : hat K
y_ne : y ≠ 0
this_1 :
  Eq.{u_1 + 1} (α := (x : K) → hat K) (fun (x : K) ↦ (↑x⁻¹ : hat K)) ((fun (y : K) ↦ (↑y : hat K)) ∘ fun (x : K) ↦ x⁻¹)
this : (Filter.comap coe' (𝓝 y)).NeBot
a a₁ : uniformity K ≤ uniformity K
⊢ Filter.comap (β := hat K × hat K) (fun (p : K × K) ↦ ((↑p.1 : hat K), (↑p.2 : hat K))) (uniformity (hat K)) ≤
    uniformity K

Tactic:
rw [Completion.comap_coe_eq_uniformity]

Premises used: UniformSpace.Completion.comap_coe_eq_uniformity
-- Module: Mathlib.Topology.Algebra.UniformField
Goal:
K : Type u_1
inst : Field K
inst_1 : UniformSpace K
inst_2 : CompletableTopField K
x : hat K
h : x ≠ 0
y : hat K
y_ne : y ≠ 0
this :
  Eq.{u_1 + 1} (α := (x : K) → hat K) (fun (x : K) ↦ (↑x⁻¹ : hat K)) ((fun (y : K) ↦ (↑y : hat K)) ∘ fun (x : K) ↦ x⁻¹)
by_contra : ∀ (h : ¬𝓝 0 ⊓ 𝓝 y = ⊥), False
⊢ 𝓝 0 ⊓ 𝓝 y = ⊥

Tactic:
by_contra h
-- Module: Mathlib.Topology.Algebra.UniformField
Goal:
K : Type u_1
inst : Field K
inst_1 : UniformSpace K
inst_2 : CompletableTopField K
x : hat K
h_1 : x ≠ 0
y : hat K
y_ne : y ≠ 0
this :
  Eq.{u_1 + 1} (α := (x : K) → hat K) (fun (x : K) ↦ (↑x⁻¹ : hat K)) ((fun (y : K) ↦ (↑y : hat K)) ∘ fun (x : K) ↦ x⁻¹)
h : ¬𝓝 0 ⊓ 𝓝 y = ⊥
⊢ False

Tactic:
y_ne (eq_of_nhds_neBot <| neBot_iff.mpr h).symm

Premises used: Iff.mpr, eq_of_nhds_neBot, Filter.neBot_iff, Eq.symm
-- Module: Mathlib.Topology.Algebra.UniformField
Goal:
K : Type u_1
inst : Field K
inst_1 : UniformSpace K
inst_2 : CompletableTopField K
x : hat K
h_1 : x ≠ 0
y : hat K
y_ne : y ≠ 0
this :
  Eq.{u_1 + 1} (α := (x : K) → hat K) (fun (x : K) ↦ (↑x⁻¹ : hat K)) ((fun (y : K) ↦ (↑y : hat K)) ∘ fun (x : K) ↦ x⁻¹)
h : ¬𝓝 0 ⊓ 𝓝 y = ⊥
⊢ False

Tactic:
exact y_ne (eq_of_nhds_neBot <| neBot_iff.mpr h).symm

Premises used: Iff.mpr, eq_of_nhds_neBot, Filter.neBot_iff, Eq.symm
-- Module: Mathlib.Topology.Algebra.UniformField
Goal:
K : Type u_1
inst : Field K
inst_1 : UniformSpace K
inst_2 : CompletableTopField K
x : hat K
h : x ≠ 0
y : hat K
y_ne : y ≠ 0
this :
  Eq.{u_1 + 1} (α := (x : K) → hat K) (fun (x : K) ↦ (↑x⁻¹ : hat K)) ((fun (y : K) ↦ (↑y : hat K)) ∘ fun (x : K) ↦ x⁻¹)
⊢ 𝓝 0 ⊓ 𝓝 y = ⊥

Tactic:
have eq_bot : 𝓝 (0 : hat K) ⊓ 𝓝 y = ⊥ := by
      by_contra h
      exact y_ne (eq_of_nhds_neBot <| neBot_iff.mpr h).symm
-- Module: Mathlib.Topology.Algebra.UniformField
Goal:
K : Type u_1
inst : Field K
inst_1 : UniformSpace K
inst_2 : CompletableTopField K
x : hat K
h : x ≠ 0
y : hat K
y_ne : y ≠ 0
this :
  Eq.{u_1 + 1} (α := (x : K) → hat K) (fun (x : K) ↦ (↑x⁻¹ : hat K)) ((fun (y : K) ↦ (↑y : hat K)) ∘ fun (x : K) ↦ x⁻¹)
eq_bot : 𝓝 0 ⊓ 𝓝 y = ⊥
a : Filter.comap coe' (𝓝 (↑0 : hat K) ⊓ 𝓝 y) = ⊥
⊢ 𝓝 0 ⊓ Filter.comap coe' (𝓝 y) = ⊥

Tactic:
rw [isDenseInducing_coe.nhds_eq_comap (0 : K), ← Filter.comap_inf]

Premises used: IsDenseInducing.nhds_eq_comap, Filter.comap_inf, OfNat.ofNat, UniformSpace.Completion.isDenseInducing_coe
-- Module: Mathlib.Topology.Algebra.UniformField
Goal:
K : Type u_1
inst : Field K
inst_1 : UniformSpace K
inst_2 : CompletableTopField K
x : hat K
h : x ≠ 0
y : hat K
y_ne : y ≠ 0
this :
  Eq.{u_1 + 1} (α := (x : K) → hat K) (fun (x : K) ↦ (↑x⁻¹ : hat K)) ((fun (y : K) ↦ (↑y : hat K)) ∘ fun (x : K) ↦ x⁻¹)
eq_bot : 𝓝 0 ⊓ 𝓝 y = ⊥
a : Filter.comap coe' (𝓝 0 ⊓ 𝓝 y) = ⊥
⊢ Filter.comap coe' (𝓝 (↑0 : hat K) ⊓ 𝓝 y) = ⊥

Tactic:
norm_cast
-- Module: Mathlib.Topology.Algebra.UniformField
Goal:
K : Type u_1
inst : Field K
inst_1 : UniformSpace K
inst_2 : CompletableTopField K
x : hat K
h : x ≠ 0
y : hat K
y_ne : y ≠ 0
this :
  Eq.{u_1 + 1} (α := (x : K) → hat K) (fun (x : K) ↦ (↑x⁻¹ : hat K)) ((fun (y : K) ↦ (↑y : hat K)) ∘ fun (x : K) ↦ x⁻¹)
eq_bot : 𝓝 0 ⊓ 𝓝 y = ⊥
a : Eq.{u_1 + 1} (α := Filter K) (Filter.comap (β := hat K) coe' ⊥) ⊥
⊢ Filter.comap coe' (𝓝 0 ⊓ 𝓝 y) = ⊥

Tactic:
rw [eq_bot]
-- Module: Mathlib.Topology.Algebra.UniformField
Goal:
K : Type u_1
inst : Field K
inst_1 : UniformSpace K
inst_2 : CompletableTopField K
x : hat K
h : x ≠ 0
y : hat K
y_ne : y ≠ 0
this :
  Eq.{u_1 + 1} (α := (x : K) → hat K) (fun (x : K) ↦ (↑x⁻¹ : hat K)) ((fun (y : K) ↦ (↑y : hat K)) ∘ fun (x : K) ↦ x⁻¹)
eq_bot : 𝓝 0 ⊓ 𝓝 y = ⊥
⊢ Eq.{u_1 + 1} (α := Filter K) (Filter.comap (β := hat K) coe' ⊥) ⊥

Tactic:
comap_bot

Premises used: Filter.comap_bot
-- Module: Mathlib.Topology.Algebra.UniformField
Goal:
K : Type u_1
inst : Field K
inst_1 : UniformSpace K
inst_2 : CompletableTopField K
x : hat K
h : x ≠ 0
y : hat K
y_ne : y ≠ 0
this :
  Eq.{u_1 + 1} (α := (x : K) → hat K) (fun (x : K) ↦ (↑x⁻¹ : hat K)) ((fun (y : K) ↦ (↑y : hat K)) ∘ fun (x : K) ↦ x⁻¹)
eq_bot : 𝓝 0 ⊓ 𝓝 y = ⊥
⊢ Eq.{u_1 + 1} (α := Filter K) (Filter.comap (β := hat K) coe' ⊥) ⊥

Tactic:
exact comap_bot

Premises used: Filter.comap_bot
-- Module: Mathlib.Topology.Algebra.UniformField
Goal:
K : Type u_1
inst : Field K
inst_1 : UniformSpace K
inst_2 : IsTopologicalDivisionRing K
x : K
h : x ≠ 0
⊢ Eq (α := hat K) (hatInv (↑x : hat K)) (↑x⁻¹ : hat K)

Tactic:
isDenseInducing_coe.extend_eq_at ((continuous_coe K).continuousAt.comp (continuousAt_inv₀ h))

Premises used: ContinuousInv₀.continuousAt_inv₀, UniformSpace.Completion.hatInv, Continuous.continuousAt, UniformSpace.Completion.continuous_coe, ContinuousAt.comp, IsDenseInducing.extend_eq_at, UniformSpace.Completion.isDenseInducing_coe
-- Module: Mathlib.Topology.Algebra.UniformField
Goal:
K : Type u_1
inst : Field K
inst_1 : UniformSpace K
inst_2 : IsTopologicalDivisionRing K
inst_3 : CompletableTopField K
x : K
pos : ∀ (h : x = 0), Eq (α := hat K) (↑x : hat K)⁻¹ (↑x⁻¹ : hat K)
neg : ∀ (h : ¬x = 0), Eq (α := hat K) (↑x : hat K)⁻¹ (↑x⁻¹ : hat K)
⊢ Eq (α := hat K) (↑x : hat K)⁻¹ (↑x⁻¹ : hat K)

Tactic:
by_cases h : x = 0
-- Module: Mathlib.Topology.Algebra.UniformField
Goal:
K : Type u_1
inst : Field K
inst_1 : UniformSpace K
inst_2 : IsTopologicalDivisionRing K
inst_3 : CompletableTopField K
x : K
h : x = 0
pos : Eq.{u_1 + 1} (α := hat K) (↑0 : hat K)⁻¹ (↑0 : hat K)
⊢ Eq (α := hat K) (↑x : hat K)⁻¹ (↑x⁻¹ : hat K)

Tactic:
rw [h, inv_zero]

Premises used: inv_zero
-- Module: Mathlib.Topology.Algebra.UniformField
Goal:
K : Type u_1
inst : Field K
inst_1 : UniformSpace K
inst_2 : IsTopologicalDivisionRing K
inst_3 : CompletableTopField K
x : K
h : x = 0
pos : Eq.{u_1 + 1} (α := hat K) (if Eq.{u_1 + 1} (α := hat K) 0 0 then 0 else hatInv 0) 0
⊢ Eq.{u_1 + 1} (α := hat K) (if Eq.{u_1 + 1} (α := hat K) (↑0 : hat K) 0 then 0 else hatInv (↑0 : hat K)) (↑0 : hat K)

Tactic:
norm_cast
-- Module: Mathlib.Topology.Algebra.UniformField
Goal:
K : Type u_1
inst : Field K
inst_1 : UniformSpace K
inst_2 : IsTopologicalDivisionRing K
inst_3 : CompletableTopField K
x : K
h : x = 0
⊢ Eq.{u_1 + 1} (α := hat K) (if Eq.{u_1 + 1} (α := hat K) 0 0 then 0 else hatInv 0) 0

Tactic:
simp
-- Module: Mathlib.Topology.Algebra.UniformField
Goal:
K : Type u_1
inst : Field K
inst_1 : UniformSpace K
inst_2 : IsTopologicalDivisionRing K
inst_3 : CompletableTopField K
x : K
h : ¬x = 0
neg : Eq (α := hat K) (hatInv (↑x : hat K)) (↑x⁻¹ : hat K)
neg₁ : ¬Eq (α := hat K) (↑x : hat K) 0
⊢ Eq (α := hat K) (if Eq (α := hat K) (↑x : hat K) 0 then 0 else hatInv (↑x : hat K)) (↑x⁻¹ : hat K)

Tactic:
rw [if_neg]

Premises used: if_neg
-- Module: Mathlib.Topology.Algebra.UniformField
Goal:
K : Type u_1
inst : Field K
inst_1 : UniformSpace K
inst_2 : IsTopologicalDivisionRing K
inst_3 : CompletableTopField K
x : K
h : ¬x = 0
⊢ Eq (α := hat K) (hatInv (↑x : hat K)) (↑x⁻¹ : hat K)

Tactic:
hatInv_extends h

Premises used: UniformSpace.Completion.hatInv_extends
-- Module: Mathlib.Topology.Algebra.UniformField
Goal:
K : Type u_1
inst : Field K
inst_1 : UniformSpace K
inst_2 : IsTopologicalDivisionRing K
inst_3 : CompletableTopField K
x : K
h : ¬x = 0
⊢ Eq (α := hat K) (hatInv (↑x : hat K)) (↑x⁻¹ : hat K)

Tactic:
exact hatInv_extends h

Premises used: UniformSpace.Completion.hatInv_extends