awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Algebra.Ring.Compact
Goal:
R : Type u_1
inst : CommRing R
inst_1 : TopologicalSpace R
inst_2 : IsTopologicalRing R
inst_3 : CompactSpace R
inst_4 : T2Space R
inst_5 : IsNoetherianRing R
I : Ideal R
inst_6 : I.IsMaximal
n : ℕ
⊢ IsOpen (↑(I ^ n) : Set R)

Tactic:
have : (I ^ n).toAddSubgroup.FiniteIndex :=
    @AddSubgroup.finiteIndex_of_finite_quotient _ _ _
      (Ideal.finite_quotient_pow (IsNoetherian.noetherian _) _)
  (I ^ n).toAddSubgroup.isOpen_of_isClosed_of_finiteIndex
    (Ideal.isCompact_of_fg (IsNoetherian.noetherian _)).isClosed

Premises used: AddSubgroup.isOpen_of_isClosed_of_finiteIndex, IsNoetherian.noetherian, Ideal.isCompact_of_fg, HPow.hPow, Submodule.toAddSubgroup, AddSubgroup.finiteIndex_of_finite_quotient, IsCompact.isClosed
-- Module: Mathlib.Topology.Algebra.Ring.Compact
Goal:
R : Type u_1
inst : CommRing R
inst_1 : TopologicalSpace R
inst_2 : IsTopologicalRing R
inst_3 : CompactSpace R
inst_4 : T2Space R
inst_5 : IsNoetherianRing R
I : Ideal R
inst_6 : I.IsMaximal
⊢ Finite.{u_1 + 1} (R ⧸ I)

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.Topology.Algebra.Ring.Compact
Goal:
R : Type u_1
inst : CommRing R
inst_1 : TopologicalSpace R
inst_2 : IsTopologicalRing R
inst_3 : CompactSpace R
inst_4 : T2Space R
inst_5 : IsLocalRing R
inst_6 : IsNoetherianRing R
n : ℕ
⊢ IsOpen (↑(HPow.hPow (α := Ideal R) (maximalIdeal R) n) : Set R)

Tactic:
Ideal.isOpen_pow_of_isMaximal _ _

Premises used: Ideal.isOpen_pow_of_isMaximal
-- Module: Mathlib.Topology.Algebra.Ring.Compact
Goal:
R : Type u_1
inst : CommRing R
inst_1 : TopologicalSpace R
inst_2 : IsTopologicalRing R
inst_3 : CompactSpace R
inst_4 : T2Space R
inst_5 : IsLocalRing R
inst_6 : IsNoetherianRing R
⊢ IsOpen (↑(maximalIdeal R) : Set R)

Tactic:
Ideal.isOpen_of_isMaximal _

Premises used: Ideal.isOpen_of_isMaximal
-- Module: Mathlib.Topology.Algebra.Ring.Compact
Goal:
R : Type u_1
inst : CommRing R
inst_1 : TopologicalSpace R
inst_2 : IsTopologicalRing R
inst_3 : CompactSpace R
inst_4 : T2Space R
inst_5 : IsLocalRing R
inst_6 : IsNoetherianRing R
⊢ Finite.{u_1 + 1} (ResidueField R)

Tactic:
inferInstanceAs (Finite (R ⧸ _))

Premises used: _private.0.IsLocalRing.finite_residueField_of_compactSpace._proof_1
-- Module: Mathlib.Topology.Algebra.Ring.Compact
Goal:
R : Type u_1
inst : CommRing R
inst_1 : TopologicalSpace R
inst_2 : IsTopologicalRing R
inst_3 : CompactSpace R
inst_4 : T2Space R
inst_5 : IsLocalRing R
inst_6 : IsNoetherianRing R
I : Ideal R
⊢ IsOpen (↑I : Set R) ↔ Finite.{u_1 + 1} (R ⧸ I)

Tactic:
⟨AddSubgroup.quotient_finite_of_isOpen I.toAddSubgroup, fun H ↦ ?_⟩

Premises used: Submodule.toAddSubgroup, Iff.intro, AddSubgroup.quotient_finite_of_isOpen
-- Module: Mathlib.Topology.Algebra.Ring.Compact
Goal:
R : Type u_1
inst : CommRing R
inst_1 : TopologicalSpace R
inst_2 : IsTopologicalRing R
inst_3 : CompactSpace R
inst_4 : T2Space R
inst_5 : IsLocalRing R
inst_6 : IsNoetherianRing R
I : Ideal R
refine : ∀ (H : Finite.{u_1 + 1} (R ⧸ I)), IsOpen (↑I : Set R)
⊢ IsOpen (↑I : Set R) ↔ Finite.{u_1 + 1} (R ⧸ I)

Tactic:
refine ⟨AddSubgroup.quotient_finite_of_isOpen I.toAddSubgroup, fun H ↦ ?_⟩
-- Module: Mathlib.Topology.Algebra.Ring.Compact
Goal:
R : Type u_1
inst : CommRing R
inst_1 : TopologicalSpace R
inst_2 : IsTopologicalRing R
inst_3 : CompactSpace R
inst_4 : T2Space R
inst_5 : IsLocalRing R
inst_6 : IsNoetherianRing R
I : Ideal R
H : Finite.{u_1 + 1} (R ⧸ I)
obtain : ∀ (n : ℕ) (hn : HPow.hPow (α := Ideal R) (maximalIdeal R) n ≤ I), IsOpen (↑I : Set R)
⊢ IsOpen (↑I : Set R)

Tactic:
obtain ⟨n, hn⟩ := exists_maximalIdeal_pow_le_of_isArtinianRing_quotient I

Premises used: IsLocalRing.exists_maximalIdeal_pow_le_of_isArtinianRing_quotient
-- Module: Mathlib.Topology.Algebra.Ring.Compact
Goal:
R : Type u_1
inst : CommRing R
inst_1 : TopologicalSpace R
inst_2 : IsTopologicalRing R
inst_3 : CompactSpace R
inst_4 : T2Space R
inst_5 : IsLocalRing R
inst_6 : IsNoetherianRing R
I : Ideal R
H : Finite.{u_1 + 1} (R ⧸ I)
n : ℕ
hn : HPow.hPow (α := Ideal R) (maximalIdeal R) n ≤ I
⊢ IsOpen (↑I : Set R)

Tactic:
AddSubgroup.isOpen_mono (H₁ := (maximalIdeal R ^ n).toAddSubgroup)
    (H₂ := I.toAddSubgroup) hn (isOpen_maximalIdeal_pow R n)

Premises used: AddSubgroup.isOpen_mono, IsLocalRing.isOpen_maximalIdeal_pow
-- Module: Mathlib.Topology.Algebra.Ring.Compact
Goal:
R : Type u_1
inst : CommRing R
inst_1 : TopologicalSpace R
inst_2 : IsTopologicalRing R
inst_3 : CompactSpace R
inst_4 : T2Space R
inst_5 : IsLocalRing R
inst_6 : IsNoetherianRing R
I : Ideal R
H : Finite.{u_1 + 1} (R ⧸ I)
n : ℕ
hn : HPow.hPow (α := Ideal R) (maximalIdeal R) n ≤ I
⊢ IsOpen (↑I : Set R)

Tactic:
exact AddSubgroup.isOpen_mono (H₁ := (maximalIdeal R ^ n).toAddSubgroup)
    (H₂ := I.toAddSubgroup) hn (isOpen_maximalIdeal_pow R n)

Premises used: AddSubgroup.isOpen_mono, IsLocalRing.isOpen_maximalIdeal_pow
-- Module: Mathlib.Topology.Algebra.Ring.Compact
Goal:
R : Type u_1
inst : CommRing R
inst_1 : TopologicalSpace R
inst_2 : IsTopologicalRing R
inst_3 : CompactSpace R
inst_4 : T2Space R
inst_5 : IsDedekindDomain R
I : Ideal R
hI : I ≠ ⊥
⊢ (Function.mulSupport (M := Ideal R) fun (v : HeightOneSpectrum R) ↦ v.maxPowDividing I) ⊆
    (↑(Set.Finite.toFinset (s := Function.mulSupport (M := Ideal R) fun (v : HeightOneSpectrum R) ↦ v.maxPowDividing I)
          ⋯) :
      Set (HeightOneSpectrum R))

Tactic:
simp
-- Module: Mathlib.Topology.Algebra.Ring.Compact
Goal:
R : Type u_1
inst : CommRing R
inst_1 : TopologicalSpace R
inst_2 : IsTopologicalRing R
inst_3 : CompactSpace R
inst_4 : T2Space R
inst_5 : IsDedekindDomain R
I : Ideal R
hI : I ≠ ⊥
rw :
  IsOpen
    (↑(∏
          i ∈
            Set.Finite.toFinset (s :=
              Function.mulSupport (M := Ideal R) fun (v : HeightOneSpectrum R) ↦ v.maxPowDividing I) ⋯,
          i.maxPowDividing I) :
      Set R)
⊢ IsOpen (↑I : Set R)

Tactic:
rw [← Ideal.finprod_heightOneSpectrum_factorization hI,
    finprod_eq_finsetProd_of_mulSupport_subset _
      (s := (Ideal.hasFiniteMulSupport hI).toFinset) (by simp)]

Premises used: Ideal.finprod_heightOneSpectrum_factorization, finprod_eq_finsetProd_of_mulSupport_subset
-- Module: Mathlib.Topology.Algebra.Ring.Compact
Goal:
R : Type u_1
inst : CommRing R
inst_1 : TopologicalSpace R
inst_2 : IsTopologicalRing R
inst_3 : CompactSpace R
inst_4 : T2Space R
inst_5 : IsDedekindDomain R
I : Ideal R
hI : I ≠ ⊥
⊢ IsOpen
    (↑(∏
          i ∈
            Set.Finite.toFinset (s :=
              Function.mulSupport (M := Ideal R) fun (v : HeightOneSpectrum R) ↦ v.maxPowDividing I) ⋯,
          i.maxPowDividing I) :
      Set R)

Tactic:
@AddSubgroup.isOpen_of_isClosed_of_finiteIndex _ _ _ _ (Submodule.toAddSubgroup _)
    ?_ (IsNoetherianRing.isClosed_ideal _)

Premises used: IsNoetherianRing.isClosed_ideal, AddSubgroup.isOpen_of_isClosed_of_finiteIndex, Submodule.toAddSubgroup
-- Module: Mathlib.Topology.Algebra.Ring.Compact
Goal:
R : Type u_1
inst : CommRing R
inst_1 : TopologicalSpace R
inst_2 : IsTopologicalRing R
inst_3 : CompactSpace R
inst_4 : T2Space R
inst_5 : IsDedekindDomain R
I : Ideal R
hI : I ≠ ⊥
refine :
  AddSubgroup.FiniteIndex (G := R)
    (Submodule.toAddSubgroup (R := R) (module_M := Semiring.toModule)
      (∏
        i ∈
          Set.Finite.toFinset (s :=
            Function.mulSupport (M := Ideal R) fun (v : HeightOneSpectrum R) ↦ v.maxPowDividing I) ⋯,
        i.maxPowDividing I))
⊢ IsOpen
    (↑(∏
          i ∈
            Set.Finite.toFinset (s :=
              Function.mulSupport (M := Ideal R) fun (v : HeightOneSpectrum R) ↦ v.maxPowDividing I) ⋯,
          i.maxPowDividing I) :
      Set R)

Tactic:
refine @AddSubgroup.isOpen_of_isClosed_of_finiteIndex _ _ _ _ (Submodule.toAddSubgroup _)
    ?_ (IsNoetherianRing.isClosed_ideal _)

Premises used: AddSubgroup.isOpen_of_isClosed_of_finiteIndex, Submodule.toAddSubgroup
-- Module: Mathlib.Topology.Algebra.Ring.Compact
Goal:
R : Type u_1
inst : CommRing R
inst_1 : TopologicalSpace R
inst_2 : IsTopologicalRing R
inst_3 : CompactSpace R
inst_4 : T2Space R
inst_5 : IsDedekindDomain R
I : Ideal R
hI : I ≠ ⊥
⊢ AddSubgroup.FiniteIndex (G := R)
    (Submodule.toAddSubgroup (R := R) (module_M := Semiring.toModule)
      (∏
        i ∈
          Set.Finite.toFinset (s :=
            Function.mulSupport (M := Ideal R) fun (v : HeightOneSpectrum R) ↦ v.maxPowDividing I) ⋯,
        i.maxPowDividing I))

Tactic:
@AddSubgroup.finiteIndex_of_finite_quotient _ _ _ ?_

Premises used: AddSubgroup.finiteIndex_of_finite_quotient
-- Module: Mathlib.Topology.Algebra.Ring.Compact
Goal:
R : Type u_1
inst : CommRing R
inst_1 : TopologicalSpace R
inst_2 : IsTopologicalRing R
inst_3 : CompactSpace R
inst_4 : T2Space R
inst_5 : IsDedekindDomain R
I : Ideal R
hI : I ≠ ⊥
refine :
  Finite.{u_1 + 1}
    (HasQuotient.Quotient R (B := AddSubgroup R)
      (Submodule.toAddSubgroup (R := R) (module_M := Semiring.toModule)
        (∏
          i ∈
            Set.Finite.toFinset (s :=
              Function.mulSupport (M := Ideal R) fun (v : HeightOneSpectrum R) ↦ v.maxPowDividing I) ⋯,
          i.maxPowDividing I)))
⊢ AddSubgroup.FiniteIndex (G := R)
    (Submodule.toAddSubgroup (R := R) (module_M := Semiring.toModule)
      (∏
        i ∈
          Set.Finite.toFinset (s :=
            Function.mulSupport (M := Ideal R) fun (v : HeightOneSpectrum R) ↦ v.maxPowDividing I) ⋯,
        i.maxPowDividing I))

Tactic:
refine @AddSubgroup.finiteIndex_of_finite_quotient _ _ _ ?_

Premises used: AddSubgroup.finiteIndex_of_finite_quotient
-- Module: Mathlib.Topology.Algebra.Ring.Compact
Goal:
R : Type u_1
inst : CommRing R
inst_1 : TopologicalSpace R
inst_2 : IsTopologicalRing R
inst_3 : CompactSpace R
inst_4 : T2Space R
inst_5 : IsDedekindDomain R
I : Ideal R
hI : I ≠ ⊥
⊢ Finite.{u_1 + 1}
    (HasQuotient.Quotient R (B := AddSubgroup R)
      (Submodule.toAddSubgroup (R := R) (module_M := Semiring.toModule)
        (∏
          i ∈
            Set.Finite.toFinset (s :=
              Function.mulSupport (M := Ideal R) fun (v : HeightOneSpectrum R) ↦ v.maxPowDividing I) ⋯,
          i.maxPowDividing I)))

Tactic:
Ideal.finite_quotient_prod _ _ (fun _ _ ↦ IsNoetherian.noetherian _) fun _ _ ↦ ?_

Premises used: IsNoetherian.noetherian, Submodule.quotientRel, IsDedekindDomain.HeightOneSpectrum.maxPowDividing, Ideal.finite_quotient_prod
-- Module: Mathlib.Topology.Algebra.Ring.Compact
Goal:
R : Type u_1
inst : CommRing R
inst_1 : TopologicalSpace R
inst_2 : IsTopologicalRing R
inst_3 : CompactSpace R
inst_4 : T2Space R
inst_5 : IsDedekindDomain R
I : Ideal R
hI : I ≠ ⊥
refine :
  ∀
    x ∈
      Set.Finite.toFinset (s := Function.mulSupport (M := Ideal R) fun (v : HeightOneSpectrum R) ↦ v.maxPowDividing I)
        ⋯,
    Finite.{u_1 + 1} (R ⧸ x.maxPowDividing I)
⊢ Finite.{u_1 + 1}
    (HasQuotient.Quotient R (B := AddSubgroup R)
      (Submodule.toAddSubgroup (R := R) (module_M := Semiring.toModule)
        (∏
          i ∈
            Set.Finite.toFinset (s :=
              Function.mulSupport (M := Ideal R) fun (v : HeightOneSpectrum R) ↦ v.maxPowDividing I) ⋯,
          i.maxPowDividing I)))

Tactic:
refine Ideal.finite_quotient_prod _ _ (fun _ _ ↦ IsNoetherian.noetherian _) fun _ _ ↦ ?_

Premises used: IsNoetherian.noetherian, Ideal.finite_quotient_prod
-- Module: Mathlib.Topology.Algebra.Ring.Compact
Goal:
R : Type u_1
inst : CommRing R
inst_1 : TopologicalSpace R
inst_2 : IsTopologicalRing R
inst_3 : CompactSpace R
inst_4 : T2Space R
inst_5 : IsDedekindDomain R
I : Ideal R
hI : I ≠ ⊥
x : HeightOneSpectrum R
h :
  x ∈ Set.Finite.toFinset (s := Function.mulSupport (M := Ideal R) fun (v : HeightOneSpectrum R) ↦ v.maxPowDividing I) ⋯
⊢ Finite.{u_1 + 1} (R ⧸ x.maxPowDividing I)

Tactic:
Ideal.finite_quotient_pow (IsNoetherian.noetherian _) _

Premises used: Set.Mem, IsNoetherian.noetherian, Ideal.finite_quotient_pow, IsDedekindDomain.HeightOneSpectrum.maxPowDividing
-- Module: Mathlib.Topology.Algebra.Ring.Compact
Goal:
R : Type u_1
inst : CommRing R
inst_1 : TopologicalSpace R
inst_2 : IsTopologicalRing R
inst_3 : CompactSpace R
inst_4 : T2Space R
inst_5 : IsDedekindDomain R
I : Ideal R
hI : I ≠ ⊥
x : HeightOneSpectrum R
h :
  x ∈ Set.Finite.toFinset (s := Function.mulSupport (M := Ideal R) fun (v : HeightOneSpectrum R) ↦ v.maxPowDividing I) ⋯
⊢ Finite.{u_1 + 1} (R ⧸ x.maxPowDividing I)

Tactic:
exact Ideal.finite_quotient_pow (IsNoetherian.noetherian _) _

Premises used: IsNoetherian.noetherian, Ideal.finite_quotient_pow
-- Module: Mathlib.Topology.Algebra.Ring.Compact
Goal:
R : Type u_1
inst : CommRing R
inst_1 : TopologicalSpace R
inst_2 : IsTopologicalRing R
inst_3 : CompactSpace R
inst_4 : T2Space R
inst_5 : IsDedekindDomain R
hR : ¬IsField R
I : Ideal R
⊢ IsOpen (↑I : Set R) ↔ I ≠ ⊥

Tactic:
⟨?_, IsDedekindDomain.isOpen_of_ne_bot⟩

Premises used: Iff.intro, IsDedekindDomain.isOpen_of_ne_bot
-- Module: Mathlib.Topology.Algebra.Ring.Compact
Goal:
R : Type u_1
inst : CommRing R
inst_1 : TopologicalSpace R
inst_2 : IsTopologicalRing R
inst_3 : CompactSpace R
inst_4 : T2Space R
inst_5 : IsDedekindDomain R
hR : ¬IsField R
I : Ideal R
refine : IsOpen (↑I : Set R) → I ≠ ⊥
⊢ IsOpen (↑I : Set R) ↔ I ≠ ⊥

Tactic:
refine ⟨?_, IsDedekindDomain.isOpen_of_ne_bot⟩
-- Module: Mathlib.Topology.Algebra.Ring.Compact
Goal:
R : Type u_1
inst : CommRing R
inst_1 : TopologicalSpace R
inst_2 : IsTopologicalRing R
inst_3 : CompactSpace R
inst_4 : T2Space R
inst_5 : IsDedekindDomain R
hR : ¬IsField R
H : IsOpen (↑⊥ : Set R)
⊢ DiscreteTopology R

Tactic:
have := discreteTopology_iff_isOpen_singleton_zero.mpr H
-- Module: Mathlib.Topology.Algebra.Ring.Compact
Goal:
R : Type u_1
inst : CommRing R
inst_1 : TopologicalSpace R
inst_2 : IsTopologicalRing R
inst_3 : CompactSpace R
inst_4 : T2Space R
inst_5 : IsDedekindDomain R
hR : ¬IsField R
H : IsOpen (↑⊥ : Set R)
this : DiscreteTopology R
⊢ False

Tactic:
hR (Finite.isField_of_domain R)

Premises used: Finite.isField_of_domain
-- Module: Mathlib.Topology.Algebra.Ring.Compact
Goal:
R : Type u_1
inst : CommRing R
inst_1 : TopologicalSpace R
inst_2 : IsTopologicalRing R
inst_3 : CompactSpace R
inst_4 : T2Space R
inst_5 : IsDedekindDomain R
hR : ¬IsField R
H : IsOpen (↑⊥ : Set R)
this : DiscreteTopology R
⊢ False

Tactic:
exact hR (Finite.isField_of_domain R)

Premises used: Finite.isField_of_domain
-- Module: Mathlib.Topology.Algebra.Ring.Compact
Goal:
R : Type u_1
inst : CommRing R
inst_1 : TopologicalSpace R
inst_2 : IsTopologicalRing R
inst_3 : CompactSpace R
inst_4 : T2Space R
inst_5 : IsDomain R
inst_6 : IsDiscreteValuationRing R
I : Ideal R
⊢ IsOpen (↑I : Set R) ↔ I ≠ ⊥

Tactic:
IsDedekindDomain.isOpen_iff (not_isField R)

Premises used: IsDiscreteValuationRing.not_isField, IsDedekindDomain.isOpen_iff
-- Module: Mathlib.Topology.Algebra.Ring.Ideal
Goal:
R : Type u_1
inst : TopologicalSpace R
inst_1 : Ring R
inst_2 : IsTopologicalRing R
I : Ideal R
⊢ (↑I.closure : Set R) = closure[inst] (↑I : Set R)

Tactic:
rfl

Premises used: setOf, closure, Set.sInter, rfl
-- Module: Mathlib.Topology.Algebra.Ring.Ideal
Goal:
R : Type u_1
inst : TopologicalSpace R
inst_1 : Ring R
inst_2 : IsTopologicalRing R
I : Ideal R
hI : IsClosed[inst] (↑I : Set R)
⊢ I.closure = I

Tactic:
SetLike.ext' hI.closure_eq

Premises used: IsClosed.closure_eq, SetLike.ext'
-- Module: Mathlib.Topology.Algebra.Ring.Ideal
Goal:
R : Type u_1
inst : TopologicalSpace R
inst_1 : Ring R
inst_2 : IsTopologicalRing R
⊢ (↑(connectedComponentOfZero R) : Set R) = connectedComponent 0

Tactic:
rfl

Premises used: Set.Mem, setOf, Set.sUnion, connectedComponent, rfl
-- Module: Mathlib.Topology.Algebra.Ring.Ideal
Goal:
R : Type u_1
inst : TopologicalSpace R
inst_1 : CommRing R
N : Ideal R
inst_2 : IsTopologicalRing R
⊢ IsOpenMap (X := R) (Y := R ⧸ N) (⇑(mk N) : (a : R) → R ⧸ N)

Tactic:
QuotientAddGroup.isOpenMap_coe

Premises used: Submodule.Quotient.mk, QuotientAddGroup.isOpenMap_coe, Submodule.quotientRel
-- Module: Mathlib.Topology.Algebra.Ring.Ideal
Goal:
R : Type u_1
inst : TopologicalSpace R
inst_1 : CommRing R
N : Ideal R
inst_2 : IsTopologicalRing R
⊢ IsOpenQuotientMap (X := R) (Y := R ⧸ N) (⇑(mk N) : (a : R) → R ⧸ N)

Tactic:
QuotientAddGroup.isOpenQuotientMap_mk

Premises used: QuotientAddGroup.isOpenQuotientMap_mk, Submodule.Quotient.mk, Submodule.quotientRel
-- Module: Mathlib.Topology.Algebra.Ring.Ideal
Goal:
R : Type u_1
inst : TopologicalSpace R
inst_1 : CommRing R
N : Ideal R
inst_2 : IsTopologicalRing R
⊢ IsQuotientMap (Y := (R ⧸ N) × R ⧸ N) fun (p : R × R) ↦ ((mk N : (a : R) → R ⧸ N) p.1, (mk N : (a : R) → R ⧸ N) p.2)

Tactic:
((isOpenQuotientMap_mk N).prodMap (isOpenQuotientMap_mk N)).isQuotientMap

Premises used: IsOpenQuotientMap.prodMap, Prod.map, IsOpenQuotientMap.isQuotientMap, QuotientRing.isOpenQuotientMap_mk
-- Module: Mathlib.Topology.Algebra.Ring.Ideal
Goal:
R : Type u_1
inst : TopologicalSpace R
inst_1 : CommRing R
N : Ideal R
inst_2 : IsTopologicalRing R
inst_3 : CompactSpace R
⊢ CompactSpace.{u_1} (R ⧸ N)

Tactic:
Quotient.compactSpace

Premises used: Quotient.compactSpace
-- Module: Mathlib.Topology.Algebra.Ring.Real
Goal:
α : Type u
β : Type v
γ : Type w
⊢ NoncompactSpace ℝ

Tactic:
Int.isClosedEmbedding_coe_real.noncompactSpace

Premises used: Topology.IsClosedEmbedding.noncompactSpace, Int.isClosedEmbedding_coe_real
-- Module: Mathlib.Topology.Algebra.Ring.Real
Goal:
⊢ UniformContinuous (β := ℝ) fun (p : ℝ × ℝ) ↦ p.1 + p.2

Tactic:
Metric.uniformContinuous_iff.2 fun _ε ε0 =>
    let ⟨δ, δ0, Hδ⟩ := rat_add_continuous_lemma abs ε0
    ⟨δ, δ0, fun _ _ h =>
      let ⟨h₁, h₂⟩ := max_lt_iff.1 h
      Hδ h₁ h₂⟩

Premises used: Iff.mpr, _private.0.Real.uniformContinuous_add.match_1, abs, Set.Mem, setOf, Exists, max_lt_iff, Prod.fst, GT.gt, And, HAdd.hAdd, And.intro, LT.lt, Exists.intro, Iff.mp, Dist.dist, OfNat.ofNat, Prod.snd, Metric.uniformContinuous_iff, _private.0.Real.uniformContinuous_add.match_2, rat_add_continuous_lemma
-- Module: Mathlib.Topology.Algebra.Ring.Real
Goal:
ε : ℝ
ε0 : ε > 0
x x_1 : ℝ
h : dist x x_1 < ε
⊢ dist (-x) (-x_1) < ε

Tactic:
simpa only [abs_sub_comm, Real.dist_eq, neg_sub_neg] using h

Premises used: Real.dist_eq, neg_sub_neg, abs_sub_comm
-- Module: Mathlib.Topology.Algebra.Ring.Real
Goal:
α : Type u
β : Type v
γ : Type w
⊢ IsUniformAddGroup ℝ

Tactic:
IsUniformAddGroup.mk' Real.uniformContinuous_add Real.uniformContinuous_neg

Premises used: Real.uniformContinuous_neg, IsUniformAddGroup.mk', Real.uniformContinuous_add
-- Module: Mathlib.Topology.Algebra.Ring.Real
Goal:
x : ℝ
⊢ UniformContinuous (β := ℝ) fun (x_1 : ℝ) ↦ x * x_1

Tactic:
uniformContinuous_of_continuousAt_zero (DistribSMul.toAddMonoidHom ℝ x)
    (continuous_const_smul x).continuousAt

Premises used: Real, ContinuousConstSMul.continuous_const_smul, uniformContinuous_of_continuousAt_zero, Continuous.continuousAt, DistribSMul.toAddMonoidHom
-- Module: Mathlib.Topology.Algebra.Ring.Real
Goal:
α : Type u
β : Type v
γ : Type w
⊢ IsTopologicalAddGroup ℝ

Tactic:
infer_instance
-- Module: Mathlib.Topology.Algebra.Ring.Real
Goal:
α : Type u
β : Type v
γ : Type w
⊢ IsTopologicalRing ℝ

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.Topology.Algebra.Ring.Real
Goal:
α : Type u
β : Type v
γ : Type w
⊢ IsTopologicalDivisionRing ℝ

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.Topology.Algebra.Ring.Real
Goal:
α : Type u
β : Type v
γ : Type w
⊢ ContinuousNeg EReal

Tactic:
⟨negOrderIso.continuous⟩

Premises used: OrderIso.continuous, ContinuousNeg.mk, EReal.negOrderIso
-- Module: Mathlib.Topology.Algebra.Ring.Real
Goal:
α : Type u
β : Type v
γ : Type w
⊢ ContinuousSub ℝ≥0

Tactic:
⟨((continuous_coe.fst'.sub continuous_coe.snd').max continuous_const).subtype_mk _⟩

Premises used: Continuous.fst', Continuous.snd', continuous_const, NNReal.continuous_coe, Continuous.subtype_mk, ContinuousSub.mk, Continuous.max, Continuous.sub
-- Module: Mathlib.Topology.Algebra.Ring.Real
Goal:
α : Type u
β : Type v
γ : Type w
⊢ ContinuousInv₀ ℝ≥0

Tactic:
inferInstance

Premises used: inferInstance
-- Module: Mathlib.Topology.Algebra.Ring.Real
Goal:
rw : OrdConnected (α := ℝ≥0∞) (Iio ∞)
⊢ (range ofNNReal).OrdConnected

Tactic:
rw [range_coe']

Premises used: ENNReal.range_coe'
-- Module: Mathlib.Topology.Algebra.Ring.Real
Goal:
⊢ OrdConnected (α := ℝ≥0∞) (Iio ∞)

Tactic:
ordConnected_Iio

Premises used: Set.ordConnected_Iio
-- Module: Mathlib.Topology.Algebra.Ring.Real
Goal:
⊢ OrdConnected (α := ℝ≥0∞) (Iio ∞)

Tactic:
exact ordConnected_Iio

Premises used: Set.ordConnected_Iio
-- Module: Mathlib.Topology.Algebra.Ring.Real
Goal:
α : Type u
f : Filter α
m : α → ℝ≥0
a : ℝ≥0
⊢ Tendsto (fun (a : α) ↦ (↑(m a) : ℝ≥0∞)) f (𝓝 (↑a : ℝ≥0∞)) ↔ Tendsto m f (𝓝 a)

Tactic:
isEmbedding_coe.tendsto_nhds_iff.symm

Premises used: ENNReal.ofNNReal, WithTop.some, Topology.IsEmbedding.tendsto_nhds_iff, Iff.symm, ENNReal.isEmbedding_coe
-- Module: Mathlib.Topology.Algebra.Ring.Real
Goal:
rw : IsOpen (X := ℝ≥0∞) (Iio ∞)
⊢ IsOpen (range ofNNReal)

Tactic:
rw [range_coe']

Premises used: ENNReal.range_coe'
-- Module: Mathlib.Topology.Algebra.Ring.Real
Goal:
⊢ IsOpen (X := ℝ≥0∞) (Iio ∞)

Tactic:
isOpen_Iio

Premises used: isOpen_Iio
-- Module: Mathlib.Topology.Algebra.Ring.Real
Goal:
⊢ IsOpen (X := ℝ≥0∞) (Iio ∞)

Tactic:
exact isOpen_Iio

Premises used: isOpen_Iio
-- Module: Mathlib.Topology.Algebra.Ring.Real
Goal:
r p : ℝ≥0
⊢ 𝓝 ((↑r : ℝ≥0∞), (↑p : ℝ≥0∞)) = map (fun (p : ℝ≥0 × ℝ≥0) ↦ ((↑p.1 : ℝ≥0∞), (↑p.2 : ℝ≥0∞))) (𝓝 (r, p))

Tactic:
((isOpenEmbedding_coe.prodMap isOpenEmbedding_coe).map_nhds_eq (r, p)).symm

Premises used: Topology.IsOpenEmbedding.map_nhds_eq, ENNReal.isOpenEmbedding_coe, Prod.mk, Prod.map, Eq.symm, Topology.IsOpenEmbedding.prodMap
-- Module: Mathlib.Topology.Algebra.Ring.Real
Goal:
α : Type u
β : Type v
γ : Type w
⊢ ContinuousAdd ℝ≥0∞

Tactic:
⟨continuous_iff_continuousAt.2 ?_⟩

Premises used: Iff.mpr, ContinuousAdd.mk, continuous_iff_continuousAt
-- Module: Mathlib.Topology.Algebra.Ring.Real
Goal:
α : Type u
β : Type v
γ : Type w
refine : ∀ (x : ℝ≥0∞ × ℝ≥0∞), ContinuousAt (Y := ℝ≥0∞) (fun (p : ℝ≥0∞ × ℝ≥0∞) ↦ p.1 + p.2) x
⊢ ContinuousAdd ℝ≥0∞

Tactic:
refine ⟨continuous_iff_continuousAt.2 ?_⟩
-- Module: Mathlib.Topology.Algebra.Ring.Real
Goal:
α : Type u
β : Type v
γ : Type w
b : ℝ≥0∞
⊢ ContinuousAt (Y := ℝ≥0∞) (fun (p : ℝ≥0∞ × ℝ≥0∞) ↦ p.1 + p.2) (none, b)

Tactic:
tendsto_nhds_top_mono' continuousAt_fst fun p => le_add_right le_rfl

Premises used: le_rfl, ContinuousAt, WithTop.map₂, tendsto_nhds_top_mono', continuousAt_fst, Option.map₂, le_add_right
-- Module: Mathlib.Topology.Algebra.Ring.Real
Goal:
α : Type u
β : Type v
γ : Type w
b : ℝ≥0∞
⊢ ContinuousAt (Y := ℝ≥0∞) (fun (p : ℝ≥0∞ × ℝ≥0∞) ↦ p.1 + p.2) (none, b)

Tactic:
exact tendsto_nhds_top_mono' continuousAt_fst fun p => le_add_right le_rfl
-- Module: Mathlib.Topology.Algebra.Ring.Real
Goal:
α : Type u
β : Type v
γ : Type w
b : ℝ≥0∞
a : ℝ≥0
some : ContinuousAt (Y := ℝ≥0∞) (fun (p : ℝ≥0∞ × ℝ≥0∞) ↦ p.1 + p.2) (Option.some a, none)
some₁ : ∀ (b : ℝ≥0), ContinuousAt (Y := ℝ≥0∞) (fun (p : ℝ≥0∞ × ℝ≥0∞) ↦ p.1 + p.2) (Option.some a, Option.some b)
⊢ ContinuousAt (Y := ℝ≥0∞) (fun (p : ℝ≥0∞ × ℝ≥0∞) ↦ p.1 + p.2) (Option.some a, b)

Tactic:
rcases b with (_ | b)
-- Module: Mathlib.Topology.Algebra.Ring.Real
Goal:
α : Type u
β : Type v
γ : Type w
a : ℝ≥0
⊢ ContinuousAt (Y := ℝ≥0∞) (fun (p : ℝ≥0∞ × ℝ≥0∞) ↦ p.1 + p.2) (some a, none)

Tactic:
tendsto_nhds_top_mono' continuousAt_snd fun p => le_add_left le_rfl

Premises used: le_rfl, ContinuousAt, WithTop.map₂, tendsto_nhds_top_mono', continuousAt_snd, Option.map₂, le_add_left
-- Module: Mathlib.Topology.Algebra.Ring.Real
Goal:
α : Type u
β : Type v
γ : Type w
a : ℝ≥0
⊢ ContinuousAt (Y := ℝ≥0∞) (fun (p : ℝ≥0∞ × ℝ≥0∞) ↦ p.1 + p.2) (some a, none)

Tactic:
exact tendsto_nhds_top_mono' continuousAt_snd fun p => le_add_left le_rfl
-- Module: Mathlib.Topology.Algebra.Ring.Real
Goal:
α : Type u
β : Type v
γ : Type w
a b : ℝ≥0
⊢ ContinuousAt (Y := ℝ≥0∞) (fun (p : ℝ≥0∞ × ℝ≥0∞) ↦ p.1 + p.2) (some a, some b)

Tactic:
simp only [ContinuousAt, some_eq_coe, nhds_coe_coe, ← coe_add, tendsto_map'_iff,
    Function.comp_def, tendsto_coe, tendsto_add]

Premises used: ContinuousAt, Filter.tendsto_map'_iff, ENNReal.coe_add, ENNReal.tendsto_coe, Function.comp_def, tendsto_add, ENNReal.some_eq_coe, ENNReal.nhds_coe_coe