awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Algebra.Ring.Basic
Goal:
R : Type u_1
inst : NonUnitalNonAssocRing R
inst_1 : TopologicalSpace R
inst_2 : ContinuousNeg R
⊢ ContinuousNeg.{u_1} Rᵐᵒᵖ

Tactic:
opHomeomorph.symm.isInducing.continuousNeg fun _ => rfl

Premises used: Homeomorph.isInducing, MulOpposite.opHomeomorph, Homeomorph.symm, Topology.IsInducing.continuousNeg, rfl
-- Module: Mathlib.Topology.Algebra.Ring.Basic
Goal:
R : Type u_1
inst : NonUnitalNonAssocRing R
inst_1 : TopologicalSpace R
inst_2 : IsTopologicalRing R
⊢ IsTopologicalRing.{u_1} Rᵐᵒᵖ

Tactic:
⟨⟩

Premises used: IsTopologicalRing.mk
-- Module: Mathlib.Topology.Algebra.Ring.Basic
Goal:
R : Type u_1
inst : NonUnitalNonAssocRing R
inst_1 : TopologicalSpace R
inst_2 : IsSemitopologicalRing R
⊢ IsSemitopologicalRing.{u_1} Rᵐᵒᵖ

Tactic:
⟨⟩

Premises used: IsSemitopologicalRing.mk
-- Module: Mathlib.Topology.Algebra.Ring.Basic
Goal:
R : Type u_1
inst : NonUnitalNonAssocSemiring R
inst_1 : TopologicalSpace R
inst_2 : SeparatelyContinuousMul R
⊢ SeparatelyContinuousMul.{u_1} Rᵃᵒᵖ

Tactic:
separatelyContinuousMul_induced opMulEquiv.symm

Premises used: separatelyContinuousMul_induced, AddOpposite.opMulEquiv, AddOpposite, AddOpposite.unop, MulEquiv.symm
-- Module: Mathlib.Topology.Algebra.Ring.Basic
Goal:
R : Type u_1
inst : NonUnitalNonAssocSemiring R
inst_1 : TopologicalSpace R
inst_2 : IsSemitopologicalSemiring R
⊢ IsSemitopologicalSemiring.{u_1} Rᵃᵒᵖ

Tactic:
⟨⟩

Premises used: IsSemitopologicalSemiring.mk
-- Module: Mathlib.Topology.Algebra.Ring.Basic
Goal:
R : Type u_1
inst : NonUnitalNonAssocRing R
inst_1 : TopologicalSpace R
inst_2 : IsSemitopologicalRing R
⊢ IsSemitopologicalRing.{u_1} Rᵃᵒᵖ

Tactic:
⟨⟩

Premises used: IsSemitopologicalRing.mk
-- Module: Mathlib.Topology.Algebra.Ring.Basic
Goal:
R : Type u_1
inst : NonUnitalNonAssocSemiring R
inst_1 : TopologicalSpace R
inst_2 : ContinuousMul R
⊢ ContinuousMul.{u_1} Rᵃᵒᵖ

Tactic:
continuousMul_induced opMulEquiv.symm

Premises used: AddOpposite.opMulEquiv, AddOpposite, continuousMul_induced, AddOpposite.unop, MulEquiv.symm
-- Module: Mathlib.Topology.Algebra.Ring.Basic
Goal:
R : Type u_1
inst : NonUnitalNonAssocSemiring R
inst_1 : TopologicalSpace R
inst_2 : IsTopologicalSemiring R
⊢ IsTopologicalSemiring.{u_1} Rᵃᵒᵖ

Tactic:
⟨⟩

Premises used: IsTopologicalSemiring.mk
-- Module: Mathlib.Topology.Algebra.Ring.Basic
Goal:
R : Type u_1
inst : NonUnitalNonAssocRing R
inst_1 : TopologicalSpace R
inst_2 : IsTopologicalRing R
⊢ IsTopologicalRing.{u_1} Rᵃᵒᵖ

Tactic:
⟨⟩

Premises used: IsTopologicalRing.mk
-- Module: Mathlib.Topology.Algebra.Ring.Basic
Goal:
R : Type u_2
inst : NonUnitalNonAssocRing R
inst_1 : TopologicalSpace R
inst_2 : IsTopologicalAddGroup R
hmul :
  Tendsto (β := R) (uncurry fun (x1 x2 : R) ↦ x1 * x2) (SProd.sprod (α := Filter R) (β := Filter R) (𝓝 0) (𝓝 0)) (𝓝 0)
hmul_left : ∀ (x₀ : R), Tendsto (β := R) (fun (x : R) ↦ x₀ * x) (𝓝 0) (𝓝 0)
hmul_right : ∀ (x₀ : R), Tendsto (β := R) (fun (x : R) ↦ x * x₀) (𝓝 0) (𝓝 0)
⊢ Continuous[instTopologicalSpaceProd, inst_1] fun (p : R × R) ↦ p.1 * p.2

Tactic:
continuous_of_continuousAt_zero₂ (AddMonoidHom.mul (R := R)) ?_ ?_ ?_

Premises used: continuous_of_continuousAt_zero₂, AddMonoidHom.mul
-- Module: Mathlib.Topology.Algebra.Ring.Basic
Goal:
R : Type u_2
inst : NonUnitalNonAssocRing R
inst_1 : TopologicalSpace R
inst_2 : IsTopologicalAddGroup R
hmul :
  Tendsto (β := R) (uncurry fun (x1 x2 : R) ↦ x1 * x2) (SProd.sprod (α := Filter R) (β := Filter R) (𝓝 0) (𝓝 0)) (𝓝 0)
hmul_left : ∀ (x₀ : R), Tendsto (β := R) (fun (x : R) ↦ x₀ * x) (𝓝 0) (𝓝 0)
hmul_right : ∀ (x₀ : R), Tendsto (β := R) (fun (x : R) ↦ x * x₀) (𝓝 0) (𝓝 0)
refine_1 :
  ContinuousAt (Y := R)
    (fun (x : R × R) ↦ ((((AddMonoidHom.mul : R →+ R →+ R) : (a : R) → R →+ R) x.1 : R →+ R) : (a : R) → R) x.2) (0, 0)
refine_2 :
  ∀ (x : R),
    ContinuousAt (X := R) (Y := R) (⇑(((AddMonoidHom.mul : R →+ R →+ R) : (a : R) → R →+ R) x : R →+ R) : (a : R) → R) 0
refine_3 :
  ∀ (y : R),
    ContinuousAt (Y := R)
      (fun (x : R) ↦ ((((AddMonoidHom.mul : R →+ R →+ R) : (a : R) → R →+ R) x : R →+ R) : (a : R) → R) y) 0
⊢ Continuous[instTopologicalSpaceProd, inst_1] fun (p : R × R) ↦ p.1 * p.2

Tactic:
refine continuous_of_continuousAt_zero₂ (AddMonoidHom.mul (R := R)) ?_ ?_ ?_

Premises used: continuous_of_continuousAt_zero₂, AddMonoidHom.mul
-- Module: Mathlib.Topology.Algebra.Ring.Basic
Goal:
R : Type u_2
inst : NonUnitalNonAssocRing R
inst_1 : TopologicalSpace R
inst_2 : IsTopologicalAddGroup R
hmul :
  Tendsto (β := R) (uncurry fun (x1 x2 : R) ↦ x1 * x2) (SProd.sprod (α := Filter R) (β := Filter R) (𝓝 0) (𝓝 0)) (𝓝 0)
hmul_left : ∀ (x₀ : R), Tendsto (β := R) (fun (x : R) ↦ x₀ * x) (𝓝 0) (𝓝 0)
hmul_right : ∀ (x₀ : R), Tendsto (β := R) (fun (x : R) ↦ x * x₀) (𝓝 0) (𝓝 0)
⊢ ContinuousAt (Y := R)
    (fun (x : R × R) ↦ ((((AddMonoidHom.mul : R →+ R →+ R) : (a : R) → R →+ R) x.1 : R →+ R) : (a : R) → R) x.2) (0, 0)

Tactic:
simpa only [ContinuousAt, mul_zero, zero_mul, nhds_prod_eq, AddMonoidHom.mul_apply]

Premises used: ContinuousAt, MulZeroClass.zero_mul, AddMonoidHom.mul_apply, MulZeroClass.mul_zero, nhds_prod_eq
-- Module: Mathlib.Topology.Algebra.Ring.Basic
Goal:
R : Type u_2
inst : NonUnitalNonAssocRing R
inst_1 : TopologicalSpace R
inst_2 : IsTopologicalAddGroup R
hmul :
  Tendsto (β := R) (uncurry fun (x1 x2 : R) ↦ x1 * x2) (SProd.sprod (α := Filter R) (β := Filter R) (𝓝 0) (𝓝 0)) (𝓝 0)
hmul_left : ∀ (x₀ : R), Tendsto (β := R) (fun (x : R) ↦ x₀ * x) (𝓝 0) (𝓝 0)
hmul_right : ∀ (x₀ : R), Tendsto (β := R) (fun (x : R) ↦ x * x₀) (𝓝 0) (𝓝 0)
⊢ ∀ (x : R),
    ContinuousAt (X := R) (Y := R) (⇑(((AddMonoidHom.mul : R →+ R →+ R) : (a : R) → R →+ R) x : R →+ R) : (a : R) → R) 0

Tactic:
simpa only [ContinuousAt, mul_zero, zero_mul, nhds_prod_eq, AddMonoidHom.mul_apply]

Premises used: ContinuousAt, MulZeroClass.zero_mul, AddMonoidHom.mul_apply, MulZeroClass.mul_zero, nhds_prod_eq
-- Module: Mathlib.Topology.Algebra.Ring.Basic
Goal:
R : Type u_2
inst : NonUnitalNonAssocRing R
inst_1 : TopologicalSpace R
inst_2 : IsTopologicalAddGroup R
hmul :
  Tendsto (β := R) (uncurry fun (x1 x2 : R) ↦ x1 * x2) (SProd.sprod (α := Filter R) (β := Filter R) (𝓝 0) (𝓝 0)) (𝓝 0)
hmul_left : ∀ (x₀ : R), Tendsto (β := R) (fun (x : R) ↦ x₀ * x) (𝓝 0) (𝓝 0)
hmul_right : ∀ (x₀ : R), Tendsto (β := R) (fun (x : R) ↦ x * x₀) (𝓝 0) (𝓝 0)
⊢ ∀ (y : R),
    ContinuousAt (Y := R)
      (fun (x : R) ↦ ((((AddMonoidHom.mul : R →+ R →+ R) : (a : R) → R →+ R) x : R →+ R) : (a : R) → R) y) 0

Tactic:
simpa only [ContinuousAt, mul_zero, zero_mul, nhds_prod_eq, AddMonoidHom.mul_apply]

Premises used: ContinuousAt, MulZeroClass.zero_mul, AddMonoidHom.mul_apply, MulZeroClass.mul_zero, nhds_prod_eq
-- Module: Mathlib.Topology.Algebra.Ring.Basic
Goal:
R : Type u_2
inst : NonUnitalNonAssocRing R
inst_1 : TopologicalSpace R
hadd :
  Tendsto (β := R) (uncurry fun (x1 x2 : R) ↦ x1 + x2) (SProd.sprod (α := Filter R) (β := Filter R) (𝓝 0) (𝓝 0)) (𝓝 0)
hneg : Tendsto (β := R) (fun (x : R) ↦ -x) (𝓝 0) (𝓝 0)
hmul :
  Tendsto (β := R) (uncurry fun (x1 x2 : R) ↦ x1 * x2) (SProd.sprod (α := Filter R) (β := Filter R) (𝓝 0) (𝓝 0)) (𝓝 0)
hmul_left : ∀ (x₀ : R), Tendsto (β := R) (fun (x : R) ↦ x₀ * x) (𝓝 0) (𝓝 0)
hmul_right : ∀ (x₀ : R), Tendsto (β := R) (fun (x : R) ↦ x * x₀) (𝓝 0) (𝓝 0)
hleft : ∀ (x₀ : R), 𝓝 x₀ = map (fun (x : R) ↦ x₀ + x) (𝓝 0)
⊢ IsTopologicalRing R

Tactic:
have := IsTopologicalAddGroup.of_comm_of_nhds_zero hadd hneg hleft
  IsTopologicalRing.of_addGroup_of_nhds_zero hmul hmul_left hmul_right

Premises used: IsTopologicalAddGroup.of_comm_of_nhds_zero, IsTopologicalRing.of_addGroup_of_nhds_zero
-- Module: Mathlib.Topology.Algebra.Ring.Basic
Goal:
R : Type u_1
inst : TopologicalSpace R
inst_1 : NonUnitalNonAssocRing R
inst_2 : IsSemitopologicalRing R
x : R
⊢ Continuous[inst, inst] (⇑(AddMonoidHom.mulLeft x) : (a : R) → R)

Tactic:
continuous_id.const_mul _

Premises used: continuous_id, Continuous.const_mul
-- Module: Mathlib.Topology.Algebra.Ring.Basic
Goal:
R : Type u_1
inst : TopologicalSpace R
inst_1 : NonUnitalNonAssocRing R
inst_2 : IsSemitopologicalRing R
x : R
⊢ Continuous[inst, inst] (⇑(AddMonoidHom.mulRight x) : (a : R) → R)

Tactic:
continuous_id.mul_const _

Premises used: continuous_id, Continuous.mul_const
-- Module: Mathlib.Topology.Algebra.Ring.Basic
Goal:
R : Type u_1
inst : TopologicalSpace R
inst_1 : NonUnitalRing R
inst_2 : IsTopologicalRing R
S : NonUnitalSubring R
⊢ IsTopologicalRing.{u_1} ↥S

Tactic:
{ S.toSubsemigroup.continuousMul, (inferInstance : IsTopologicalAddGroup S.toAddSubgroup) with }

Premises used: NonUnitalSubring.toSubsemigroup, inferInstance, Subsemigroup.continuousMul, IsTopologicalRing.mk
-- Module: Mathlib.Topology.Algebra.Ring.Basic
Goal:
R : Type u_1
inst : TopologicalSpace R
inst_1 : NonUnitalRing R
inst_2 : IsSemitopologicalRing R
S : NonUnitalSubring R
⊢ IsSemitopologicalRing.{u_1} ↥S

Tactic:
{ S.toSubsemigroup.separatelyContinuousMul,
    (inferInstance : IsTopologicalAddGroup S.toAddSubgroup) with }

Premises used: NonUnitalSubring.toSubsemigroup, inferInstance, Subsemigroup.separatelyContinuousMul, IsSemitopologicalRing.mk
-- Module: Mathlib.Topology.Algebra.Ring.Basic
Goal:
R : Type u_1
inst : TopologicalSpace R
inst_1 : NonUnitalRing R
inst_2 : IsSemitopologicalRing R
s : NonUnitalSubring R
⊢ s ≤ s.topologicalClosure

Tactic:
_root_.subset_closure

Premises used: Set.Mem, subset_closure, setOf, Set.Subset, closure, Set.sInter
-- Module: Mathlib.Topology.Algebra.Ring.Basic
Goal:
R : Type u_1
inst : TopologicalSpace R
inst_1 : NonUnitalRing R
inst_2 : IsSemitopologicalRing R
s : NonUnitalSubring R
⊢ IsClosed[inst] (↑s.topologicalClosure : Set R)

Tactic:
isClosed_closure

Premises used: setOf, closure, isClosed_closure, Set.sInter
-- Module: Mathlib.Topology.Algebra.Ring.Basic
Goal:
R : Type u_1
inst : TopologicalSpace R
inst_1 : NonUnitalRing R
inst_2 : IsSemitopologicalRing R
s t : NonUnitalSubring R
h : s ≤ t
ht : IsClosed[inst] (↑t : Set R)
⊢ s.topologicalClosure ≤ t

Tactic:
closure_minimal h ht

Premises used: Set.Mem, closure_minimal, setOf, Set.Subset, closure, Set.sInter
-- Module: Mathlib.Topology.Algebra.Ring.Basic
Goal:
R : Type u_1
inst : TopologicalSpace R
inst_1 : NonUnitalRing R
inst_2 : IsSemitopologicalRing R
s t : NonUnitalSubring R
h : s ≤ t
⊢ s.topologicalClosure ≤ t.topologicalClosure

Tactic:
_root_.closure_mono h

Premises used: Set.Mem, setOf, closure_mono, Set.Subset, closure, Set.sInter
-- Module: Mathlib.Topology.Algebra.Ring.Basic
Goal:
R : Type u_1
inst : TopologicalSpace R
inst_1 : Ring R
inst_2 : IsTopologicalRing R
S : Subring R
⊢ IsTopologicalRing.{u_1} ↥S

Tactic:
{ S.toSubmonoid.continuousMul, (inferInstance : IsTopologicalAddGroup S.toAddSubgroup) with }

Premises used: Subring.toSubsemiring, inferInstance, Subsemiring.toSubmonoid, IsTopologicalRing.mk, Submonoid.continuousMul
-- Module: Mathlib.Topology.Algebra.Ring.Basic
Goal:
R : Type u_1
inst : TopologicalSpace R
inst_1 : Ring R
inst_2 : IsSemitopologicalRing R
S : Subring R
⊢ IsSemitopologicalRing.{u_1} ↥S

Tactic:
{ S.toSubmonoid.separatelyContinuousMul,
    (inferInstance : IsTopologicalAddGroup S.toAddSubgroup) with }

Premises used: Subring.toSubsemiring, inferInstance, Submonoid.separatelyContinuousMul, Subsemiring.toSubmonoid, IsSemitopologicalRing.mk
-- Module: Mathlib.Topology.Algebra.Ring.Basic
Goal:
R : Type u_1
inst : TopologicalSpace R
inst_1 : Ring R
inst_2 : IsSemitopologicalRing R
s : Subring R
X : Type u_2
inst_3 : TopologicalSpace X
inst_4 : MulAction R X
inst_5 : ContinuousSMul R X
⊢ ContinuousSMul.{u_1, u_2} (↥s) X

Tactic:
Subsemiring.continuousSMul s.toSubsemiring X

Premises used: Subring.toSubsemiring, Set.Mem, Subsemiring.continuousSMul
-- Module: Mathlib.Topology.Algebra.Ring.Basic
Goal:
R : Type u_1
inst : TopologicalSpace R
inst_1 : Ring R
inst_2 : IsSemitopologicalRing R
s : Subring R
⊢ s ≤ s.topologicalClosure

Tactic:
_root_.subset_closure

Premises used: Set.Mem, subset_closure, setOf, Set.Subset, closure, Set.sInter
-- Module: Mathlib.Topology.Algebra.Ring.Basic
Goal:
R : Type u_1
inst : TopologicalSpace R
inst_1 : Ring R
inst_2 : IsSemitopologicalRing R
s : Subring R
⊢ IsClosed[inst] (↑s.topologicalClosure : Set R)

Tactic:
isClosed_closure

Premises used: setOf, closure, isClosed_closure, Set.sInter
-- Module: Mathlib.Topology.Algebra.Ring.Basic
Goal:
R : Type u_1
inst : TopologicalSpace R
inst_1 : Ring R
inst_2 : IsSemitopologicalRing R
s t : Subring R
h : s ≤ t
ht : IsClosed[inst] (↑t : Set R)
⊢ s.topologicalClosure ≤ t

Tactic:
closure_minimal h ht

Premises used: Set.Mem, closure_minimal, setOf, Set.Subset, closure, Set.sInter
-- Module: Mathlib.Topology.Algebra.Ring.Basic
Goal:
R : Type u_1
inst : TopologicalSpace R
inst_1 : Ring R
inst_2 : IsSemitopologicalRing R
s t : Subring R
h : s ≤ t
⊢ s.topologicalClosure ≤ t.topologicalClosure

Tactic:
_root_.closure_mono h

Premises used: Set.Mem, setOf, closure_mono, Set.Subset, closure, Set.sInter
-- Module: Mathlib.Topology.Algebra.Ring.Basic
Goal:
R : Type u_1
inst : Ring R
f g : RingTopology R
_ : f.toTopologicalSpace = g.toTopologicalSpace → f = g
⊢ f.toTopologicalSpace = g.toTopologicalSpace → f = g

Tactic:
_
-- Module: Mathlib.Topology.Algebra.Ring.Basic
Goal:
R : Type u_1
inst : Ring R
f g : RingTopology R
h : f.toTopologicalSpace = g.toTopologicalSpace
mk :
  ∀ (toTopologicalSpace : TopologicalSpace R) (toIsTopologicalRing : IsTopologicalRing R),
    { toTopologicalSpace := toTopologicalSpace, toIsTopologicalRing := toIsTopologicalRing :
            RingTopology R }.toTopologicalSpace =
        g.toTopologicalSpace →
      { toTopologicalSpace := toTopologicalSpace, toIsTopologicalRing := toIsTopologicalRing : RingTopology R } = g
⊢ f = g

Tactic:
cases f
-- Module: Mathlib.Topology.Algebra.Ring.Basic
Goal:
R : Type u_1
inst : Ring R
g : RingTopology R
toTopologicalSpace : TopologicalSpace R
toIsTopologicalRing : IsTopologicalRing R
h :
  { toTopologicalSpace := toTopologicalSpace, toIsTopologicalRing := toIsTopologicalRing :
        RingTopology R }.toTopologicalSpace =
    g.toTopologicalSpace
mk :
  ∀ (toTopologicalSpace_1 : TopologicalSpace R) (toIsTopologicalRing_1 : IsTopologicalRing R),
    { toTopologicalSpace := toTopologicalSpace, toIsTopologicalRing := toIsTopologicalRing :
            RingTopology R }.toTopologicalSpace =
        { toTopologicalSpace := toTopologicalSpace_1, toIsTopologicalRing := toIsTopologicalRing_1 :
            RingTopology R }.toTopologicalSpace →
      { toTopologicalSpace := toTopologicalSpace, toIsTopologicalRing := toIsTopologicalRing : RingTopology R } =
        { toTopologicalSpace := toTopologicalSpace_1, toIsTopologicalRing := toIsTopologicalRing_1 }
⊢ { toTopologicalSpace := toTopologicalSpace, toIsTopologicalRing := toIsTopologicalRing : RingTopology R } = g

Tactic:
cases g
-- Module: Mathlib.Topology.Algebra.Ring.Basic
Goal:
R : Type u_1
inst : Ring R
toTopologicalSpace : TopologicalSpace R
toIsTopologicalRing : IsTopologicalRing R
toTopologicalSpace_1 : TopologicalSpace R
toIsTopologicalRing_1 : IsTopologicalRing R
h :
  { toTopologicalSpace := toTopologicalSpace, toIsTopologicalRing := toIsTopologicalRing :
        RingTopology R }.toTopologicalSpace =
    { toTopologicalSpace := toTopologicalSpace_1, toIsTopologicalRing := toIsTopologicalRing_1 :
        RingTopology R }.toTopologicalSpace
⊢ { toTopologicalSpace := toTopologicalSpace, toIsTopologicalRing := toIsTopologicalRing : RingTopology R } =
    { toTopologicalSpace := toTopologicalSpace_1, toIsTopologicalRing := toIsTopologicalRing_1 }

Tactic:
congr
-- Module: Mathlib.Topology.Algebra.Ring.Basic
Goal:
R : Type u_1
inst : Ring R
f g : RingTopology R
h : Eq.{u_1 + 1} (α := Set R → Prop) TopologicalSpace.IsOpen TopologicalSpace.IsOpen
⊢ f = g

Tactic:
toTopologicalSpace_injective <| TopologicalSpace.ext h

Premises used: RingTopology.toTopologicalSpace_injective, TopologicalSpace.ext
-- Module: Mathlib.Topology.Algebra.Ring.Basic
Goal:
R : Type u_2
S : Type u_3
t : TopologicalSpace R
inst : Ring S
f : R → S
⊢ Continuous[t, (coinduced f).toTopologicalSpace] f

Tactic:
continuous_sInf_rng.2 <| forall_mem_image.2 fun _ => continuous_iff_coinduced_le.2

Premises used: Iff.mpr, continuous_iff_coinduced_le, Set.forall_mem_image, continuous_sInf_rng
-- 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 : IsArtinianRing R
obtain : ∀ (n : ℕ) (hn : HPow.hPow (α := Ideal R) (Ideal.jacobson ⊥) n = 0), Finite R
⊢ Finite R

Tactic:
obtain ⟨n, hn⟩ := IsArtinianRing.isNilpotent_jacobson_bot (R := R)

Premises used: IsArtinianRing.isNilpotent_jacobson_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 : IsArtinianRing R
n : ℕ
hn : HPow.hPow (α := Ideal R) (Ideal.jacobson ⊥) n = 0
rw : HPow.hPow (α := Ideal R) (∏ p : PrimeSpectrum R, p.asIdeal) n ≤ HPow.hPow (α := Ideal R) (Ideal.jacobson ⊥) n
⊢ HPow.hPow (α := Ideal R) (∏ p : PrimeSpectrum R, p.asIdeal) n = ⊥

Tactic:
rw [← le_bot_iff, ← Ideal.zero_eq_bot, ← hn]

Premises used: le_bot_iff, Ideal.zero_eq_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 : IsArtinianRing R
n : ℕ
hn : HPow.hPow (α := Ideal R) (Ideal.jacobson ⊥) n = 0
hab : LE.le.{u_1} (α := Ideal R) (∏ p : PrimeSpectrum R, p.asIdeal) (Ideal.jacobson ⊥)
⊢ HPow.hPow (α := Ideal R) (∏ p : PrimeSpectrum R, p.asIdeal) n ≤ HPow.hPow (α := Ideal R) (Ideal.jacobson ⊥) n

Tactic:
gcongr
-- 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 : IsArtinianRing R
n : ℕ
hn : HPow.hPow (α := Ideal R) (Ideal.jacobson ⊥) n = 0
hab :
  ∀ (b : Ideal R),
    Membership.mem (γ := Set (Ideal R)) {I : Ideal R | I.IsMaximal} b → ∏ p : PrimeSpectrum R, p.asIdeal ≤ b
⊢ LE.le.{u_1} (α := Ideal R) (∏ p : PrimeSpectrum R, p.asIdeal) (Ideal.jacobson ⊥)

Tactic:
rw [Ideal.jacobson_bot, Ring.jacobson_eq_sInf_isMaximal, le_sInf_iff]

Premises used: le_sInf_iff, Ideal.jacobson_bot, Ring.jacobson_eq_sInf_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 : IsArtinianRing R
n : ℕ
hn : HPow.hPow (α := Ideal R) (Ideal.jacobson ⊥) n = 0
I : Ideal R
hI : Membership.mem (γ := Set (Ideal R)) {I : Ideal R | I.IsMaximal} I
⊢ Membership.mem (γ := Finset (PrimeSpectrum R)) Finset.univ { asIdeal := I, isPrime := ⋯ : PrimeSpectrum 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 : IsArtinianRing R
n : ℕ
hn : HPow.hPow (α := Ideal R) (Ideal.jacobson ⊥) n = 0
⊢ ∀ (b : Ideal R),
    Membership.mem (γ := Set (Ideal R)) {I : Ideal R | I.IsMaximal} b → ∏ p : PrimeSpectrum R, p.asIdeal ≤ b

Tactic:
exact fun I hI ↦ Ideal.prod_le_inf.trans
      (Finset.inf_le (b := PrimeSpectrum.mk I hI.isPrime) (by simp))

Premises used: Ideal.prod_le_inf, LE.le.trans, Finset.inf_le
-- 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 : IsArtinianRing R
n : ℕ
hn : HPow.hPow (α := Ideal R) (Ideal.jacobson ⊥) n = 0
⊢ HPow.hPow (α := Ideal R) (∏ p : PrimeSpectrum R, p.asIdeal) n = ⊥

Tactic:
have H : (∏ p : PrimeSpectrum R, p.asIdeal) ^ n = ⊥ := by
    rw [← le_bot_iff, ← Ideal.zero_eq_bot, ← hn]
    gcongr
    rw [Ideal.jacobson_bot, Ring.jacobson_eq_sInf_isMaximal, le_sInf_iff]
    exact fun I hI ↦ Ideal.prod_le_inf.trans
      (Finset.inf_le (b := PrimeSpectrum.mk I hI.isPrime) (by 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 : IsArtinianRing R
n : ℕ
hn : HPow.hPow (α := Ideal R) (Ideal.jacobson ⊥) n = 0
H : HPow.hPow (α := Ideal R) (∏ p : PrimeSpectrum R, p.asIdeal) n = ⊥
⊢ Finite.{u_1 + 1} (HasQuotient.Quotient R (B := Ideal R) (∏ i : PrimeSpectrum R, i.asIdeal))

Tactic:
have := Ideal.finite_quotient_prod (R := R) PrimeSpectrum.asIdeal Finset.univ
    (fun _ _ ↦ IsNoetherian.noetherian _) (fun _ _ ↦ 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 : IsArtinianRing R
n : ℕ
hn : HPow.hPow (α := Ideal R) (Ideal.jacobson ⊥) n = 0
H : HPow.hPow (α := Ideal R) (∏ p : PrimeSpectrum R, p.asIdeal) n = ⊥
this : Finite.{u_1 + 1} (HasQuotient.Quotient R (B := Ideal R) (∏ i : PrimeSpectrum R, i.asIdeal))
⊢ Finite.{u_1 + 1} (R ⧸ HPow.hPow (α := Ideal R) (∏ p : PrimeSpectrum R, p.asIdeal) n)

Tactic:
have := Ideal.finite_quotient_pow (IsNoetherian.noetherian (∏ p : PrimeSpectrum R, p.asIdeal)) n
-- 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 : IsArtinianRing R
n : ℕ
hn : HPow.hPow (α := Ideal R) (Ideal.jacobson ⊥) n = 0
H : HPow.hPow (α := Ideal R) (∏ p : PrimeSpectrum R, p.asIdeal) n = ⊥
this_1 : Finite.{u_1 + 1} (HasQuotient.Quotient R (B := Ideal R) (∏ i : PrimeSpectrum R, i.asIdeal))
this : Finite.{u_1 + 1} (R ⧸ HPow.hPow (α := Ideal R) (∏ p : PrimeSpectrum R, p.asIdeal) n)
⊢ Finite.{u_1 + 1} (HasQuotient.Quotient R (B := Ideal R) ⊥)

Tactic:
rw [H] at this
-- 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 : IsArtinianRing R
n : ℕ
hn : HPow.hPow (α := Ideal R) (Ideal.jacobson ⊥) n = 0
H : HPow.hPow (α := Ideal R) (∏ p : PrimeSpectrum R, p.asIdeal) n = ⊥
this_1 : Finite.{u_1 + 1} (HasQuotient.Quotient R (B := Ideal R) (∏ i : PrimeSpectrum R, i.asIdeal))
this : Finite.{u_1 + 1} (HasQuotient.Quotient R (B := Ideal R) ⊥)
⊢ Finite R

Tactic:
.of_equiv _ (RingEquiv.quotientBot R).toEquiv

Premises used: Finite.of_equiv, RingEquiv.toEquiv, RingEquiv.quotientBot
-- 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 : IsArtinianRing R
n : ℕ
hn : HPow.hPow (α := Ideal R) (Ideal.jacobson ⊥) n = 0
H : HPow.hPow (α := Ideal R) (∏ p : PrimeSpectrum R, p.asIdeal) n = ⊥
this_1 : Finite.{u_1 + 1} (HasQuotient.Quotient R (B := Ideal R) (∏ i : PrimeSpectrum R, i.asIdeal))
this : Finite.{u_1 + 1} (HasQuotient.Quotient R (B := Ideal R) ⊥)
⊢ Finite R

Tactic:
exact .of_equiv _ (RingEquiv.quotientBot R).toEquiv
-- 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
⊢ IsOpen (↑I : Set R)

Tactic:
have : I.toAddSubgroup.FiniteIndex :=
    @AddSubgroup.finiteIndex_of_finite_quotient _ _ _
      (inferInstanceAs (Finite (R ⧸ I)))
  I.toAddSubgroup.isOpen_of_isClosed_of_finiteIndex (inferInstanceAs (IsClosed (X := R) I))

Premises used: _private.0.Ideal.isOpen_of_isMaximal._proof_2, AddSubgroup.isOpen_of_isClosed_of_finiteIndex, Submodule.toAddSubgroup, AddSubgroup.finiteIndex_of_finite_quotient