awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Algebra.RestrictedProduct.Units
Goal:
ι : Type u_1
R : ι → Type u_2
inst : (i : ι) → Monoid (R i)
S : ι → Type u_3
inst_1 : (i : ι) → SetLike.{u_3, u_2} (S i) (R i)
inst_2 : ∀ (i : ι), SubmonoidClass.{u_3, u_2} (S i) (R i)
B : (i : ι) → S i
𝓕 : Filter ι
x : Πʳ (i : ι), [R i, (↑(B i) : Set ((fun (i : ι) ↦ R i) i))]_[𝓕]
⊢ IsUnit x ↔
    (∀ (i : ι), IsUnit ((x : (a : ι) → R a) i)) ∧
      ∀ᶠ (i : ι) in 𝓕,
        ∃ (h : (x : (a : ι) → R a) i ∈ B i),
          IsUnit (Subtype.mk (p := fun (x : R i) ↦ x ∈ B i) ((x : (a : ι) → R a) i) h)

Tactic:
⟨eventually_isUnit_of_isUnit, fun h ↦ isUnit_of_eventually_isUnit h.1 h.2⟩

Premises used: RestrictedProduct.isUnit_of_eventually_isUnit, RestrictedProduct.eventually_isUnit_of_isUnit, And.right, And.left, Iff.intro
-- Module: Mathlib.Topology.Algebra.RestrictedProduct.Units
Goal:
ι : Type u_1
R : ι → Type u_2
inst : (i : ι) → Monoid (R i)
S : ι → Type u_3
inst_1 : (i : ι) → SetLike.{u_3, u_2} (S i) (R i)
inst_2 : ∀ (i : ι), SubmonoidClass.{u_3, u_2} (S i) (R i)
B : (i : ι) → S i
𝓕 : Filter ι
x : (i : ι) → (R i)ˣ
hx : ∀ᶠ (i : ι) in 𝓕, Membership.mem (γ := Subgroup (R i)ˣ) (Submonoid.units (Submonoid.ofClass (B i))) (x i)
⊢ ∀ (a : ι),
    Membership.mem (γ := Subgroup (R a)ˣ) (Submonoid.units (Submonoid.ofClass (B a))) (x a) →
      (↑(x a) : R a) ∈ (↑(B a) : Set (R a))

Tactic:
fun i hi ↦ hi.1

Premises used: Set.Mem, setOf, Set.preimage, And.left
-- Module: Mathlib.Topology.Algebra.RestrictedProduct.Units
Goal:
ι : Type u_1
R : ι → Type u_2
inst : (i : ι) → Monoid (R i)
S : ι → Type u_3
inst_1 : (i : ι) → SetLike.{u_3, u_2} (S i) (R i)
inst_2 : ∀ (i : ι), SubmonoidClass.{u_3, u_2} (S i) (R i)
B : (i : ι) → S i
𝓕 : Filter ι
x : (i : ι) → (R i)ˣ
hx : ∀ᶠ (i : ι) in 𝓕, Membership.mem (γ := Subgroup (R i)ˣ) (Submonoid.units (Submonoid.ofClass (B i))) (x i)
h :
  ∀ (a : ι),
    Membership.mem (γ := Set ι)
      {x_1 : ι |
        Membership.mem (γ := Set ι)
            {x_2 : ι |
              (fun (i : ι) ↦ Membership.mem (γ := Subgroup (R i)ˣ) (Submonoid.units (Submonoid.ofClass (B i))) (x i))
                x_2}
            x_1 →
          Membership.mem (γ := Set ι)
            {x_2 : ι |
              (fun (i : ι) ↦
                  Membership.mem (γ := Set ((fun (i : ι) ↦ R i) i))
                    ((fun (i : ι) ↦ (↑(B i) : Set ((fun (i : ι) ↦ R i) i))) i) ((fun (i : ι) ↦ (↑(x i) : R i)) i))
                x_2}
            x_1}
      a
h₁ :
  ∀ (a : ι),
    Membership.mem (γ := Subgroup (R a)ˣ) (Submonoid.units (Submonoid.ofClass (B a))) (x a) →
      (↑(x a) : R a) ∈ (↑(B a) : Set (R a))
⊢ ∀ᶠ (i : ι) in 𝓕,
    Membership.mem (γ := Set ((fun (i : ι) ↦ R i) i)) ((fun (i : ι) ↦ (↑(B i) : Set ((fun (i : ι) ↦ R i) i))) i)
      ((fun (i : ι) ↦ (↑(x i) : R i)) i)

Tactic:
filter_upwards [hx] using fun i hi ↦ hi.1
-- Module: Mathlib.Topology.Algebra.RestrictedProduct.Units
Goal:
ι : Type u_1
R : ι → Type u_2
inst : (i : ι) → Monoid (R i)
S : ι → Type u_3
inst_1 : (i : ι) → SetLike.{u_3, u_2} (S i) (R i)
inst_2 : ∀ (i : ι), SubmonoidClass.{u_3, u_2} (S i) (R i)
B : (i : ι) → S i
𝓕 : Filter ι
x : (i : ι) → (R i)ˣ
hx : ∀ᶠ (i : ι) in 𝓕, Membership.mem (γ := Subgroup (R i)ˣ) (Submonoid.units (Submonoid.ofClass (B i))) (x i)
⊢ ∀ (a : ι),
    Membership.mem (γ := Subgroup (R a)ˣ) (Submonoid.units (Submonoid.ofClass (B a))) (x a) →
      (↑(x a)⁻¹ : R a) ∈ (↑(B a) : Set (R a))

Tactic:
fun i hi ↦ hi.2

Premises used: Set.Mem, setOf, And.right, Set.preimage
-- Module: Mathlib.Topology.Algebra.RestrictedProduct.Units
Goal:
ι : Type u_1
R : ι → Type u_2
inst : (i : ι) → Monoid (R i)
S : ι → Type u_3
inst_1 : (i : ι) → SetLike.{u_3, u_2} (S i) (R i)
inst_2 : ∀ (i : ι), SubmonoidClass.{u_3, u_2} (S i) (R i)
B : (i : ι) → S i
𝓕 : Filter ι
x : (i : ι) → (R i)ˣ
hx : ∀ᶠ (i : ι) in 𝓕, Membership.mem (γ := Subgroup (R i)ˣ) (Submonoid.units (Submonoid.ofClass (B i))) (x i)
h :
  ∀ (a : ι),
    Membership.mem (γ := Set ι)
      {x_1 : ι |
        Membership.mem (γ := Set ι)
            {x_2 : ι |
              (fun (i : ι) ↦ Membership.mem (γ := Subgroup (R i)ˣ) (Submonoid.units (Submonoid.ofClass (B i))) (x i))
                x_2}
            x_1 →
          Membership.mem (γ := Set ι)
            {x_2 : ι |
              (fun (i : ι) ↦
                  Membership.mem (γ := Set ((fun (i : ι) ↦ R i) i))
                    ((fun (i : ι) ↦ (↑(B i) : Set ((fun (i : ι) ↦ R i) i))) i) ((fun (i : ι) ↦ (↑(x i)⁻¹ : R i)) i))
                x_2}
            x_1}
      a
h₁ :
  ∀ (a : ι),
    Membership.mem (γ := Subgroup (R a)ˣ) (Submonoid.units (Submonoid.ofClass (B a))) (x a) →
      (↑(x a)⁻¹ : R a) ∈ (↑(B a) : Set (R a))
⊢ ∀ᶠ (i : ι) in 𝓕,
    Membership.mem (γ := Set ((fun (i : ι) ↦ R i) i)) ((fun (i : ι) ↦ (↑(B i) : Set ((fun (i : ι) ↦ R i) i))) i)
      ((fun (i : ι) ↦ (↑(x i)⁻¹ : R i)) i)

Tactic:
filter_upwards [hx] using fun i hi ↦ hi.2
-- Module: Mathlib.Topology.Algebra.RestrictedProduct.Units
Goal:
ι : Type u_1
R : ι → Type u_2
inst : (i : ι) → Monoid (R i)
S : ι → Type u_3
inst_1 : (i : ι) → SetLike.{u_3, u_2} (S i) (R i)
inst_2 : ∀ (i : ι), SubmonoidClass.{u_3, u_2} (S i) (R i)
B : (i : ι) → S i
𝓕 : Filter ι
x : (i : ι) → (R i)ˣ
hx : ∀ᶠ (i : ι) in 𝓕, Membership.mem (γ := Subgroup (R i)ˣ) (Submonoid.units (Submonoid.ofClass (B i))) (x i)
h :
  ∀ (i : ι),
    (Subtype.mk (p := fun (x : (i : ι) → (fun (i : ι) ↦ R i) i) ↦
              ∀ᶠ (i : ι) in 𝓕,
                Membership.mem (γ := Set ((fun (i : ι) ↦ R i) i))
                  ((fun (i : ι) ↦ (↑(B i) : Set ((fun (i : ι) ↦ R i) i))) i) (x i))
              (fun (i : ι) ↦ (↑(x i) : R i)) ⋯ *
            Subtype.mk (p := fun (x : (i : ι) → (fun (i : ι) ↦ R i) i) ↦
              ∀ᶠ (i : ι) in 𝓕,
                Membership.mem (γ := Set ((fun (i : ι) ↦ R i) i))
                  ((fun (i : ι) ↦ (↑(B i) : Set ((fun (i : ι) ↦ R i) i))) i) (x i))
              (fun (i : ι) ↦ (↑(x i)⁻¹ : R i)) ⋯ :
          (a : ι) → R a)
        i =
      (1 : (a : ι) → R a) i
⊢ Subtype.mk (p := fun (x : (i : ι) → (fun (i : ι) ↦ R i) i) ↦
        ∀ᶠ (i : ι) in 𝓕,
          Membership.mem (γ := Set ((fun (i : ι) ↦ R i) i)) ((fun (i : ι) ↦ (↑(B i) : Set ((fun (i : ι) ↦ R i) i))) i)
            (x i))
        (fun (i : ι) ↦ (↑(x i) : R i)) ⋯ *
      Subtype.mk (p := fun (x : (i : ι) → (fun (i : ι) ↦ R i) i) ↦
        ∀ᶠ (i : ι) in 𝓕,
          Membership.mem (γ := Set ((fun (i : ι) ↦ R i) i)) ((fun (i : ι) ↦ (↑(B i) : Set ((fun (i : ι) ↦ R i) i))) i)
            (x i))
        (fun (i : ι) ↦ (↑(x i)⁻¹ : R i)) ⋯ =
    1

Tactic:
ext
-- Module: Mathlib.Topology.Algebra.RestrictedProduct.Units
Goal:
ι : Type u_1
R : ι → Type u_2
inst : (i : ι) → Monoid (R i)
S : ι → Type u_3
inst_1 : (i : ι) → SetLike.{u_3, u_2} (S i) (R i)
inst_2 : ∀ (i : ι), SubmonoidClass.{u_3, u_2} (S i) (R i)
B : (i : ι) → S i
𝓕 : Filter ι
x : (i : ι) → (R i)ˣ
hx : ∀ᶠ (i : ι) in 𝓕, Membership.mem (γ := Subgroup (R i)ˣ) (Submonoid.units (Submonoid.ofClass (B i))) (x i)
i : ι
⊢ (Subtype.mk (p := fun (x : (i : ι) → (fun (i : ι) ↦ R i) i) ↦
            ∀ᶠ (i : ι) in 𝓕,
              Membership.mem (γ := Set ((fun (i : ι) ↦ R i) i))
                ((fun (i : ι) ↦ (↑(B i) : Set ((fun (i : ι) ↦ R i) i))) i) (x i))
            (fun (i : ι) ↦ (↑(x i) : R i)) ⋯ *
          Subtype.mk (p := fun (x : (i : ι) → (fun (i : ι) ↦ R i) i) ↦
            ∀ᶠ (i : ι) in 𝓕,
              Membership.mem (γ := Set ((fun (i : ι) ↦ R i) i))
                ((fun (i : ι) ↦ (↑(B i) : Set ((fun (i : ι) ↦ R i) i))) i) (x i))
            (fun (i : ι) ↦ (↑(x i)⁻¹ : R i)) ⋯ :
        (a : ι) → R a)
      i =
    (1 : (a : ι) → R a) i

Tactic:
simp
-- Module: Mathlib.Topology.Algebra.RestrictedProduct.Units
Goal:
ι : Type u_1
R : ι → Type u_2
inst : (i : ι) → Monoid (R i)
S : ι → Type u_3
inst_1 : (i : ι) → SetLike.{u_3, u_2} (S i) (R i)
inst_2 : ∀ (i : ι), SubmonoidClass.{u_3, u_2} (S i) (R i)
B : (i : ι) → S i
𝓕 : Filter ι
x : (i : ι) → (R i)ˣ
hx : ∀ᶠ (i : ι) in 𝓕, Membership.mem (γ := Subgroup (R i)ˣ) (Submonoid.units (Submonoid.ofClass (B i))) (x i)
h :
  ∀ (i : ι),
    (Subtype.mk (p := fun (x : (i : ι) → (fun (i : ι) ↦ R i) i) ↦
              ∀ᶠ (i : ι) in 𝓕,
                Membership.mem (γ := Set ((fun (i : ι) ↦ R i) i))
                  ((fun (i : ι) ↦ (↑(B i) : Set ((fun (i : ι) ↦ R i) i))) i) (x i))
              (fun (i : ι) ↦ (↑(x i)⁻¹ : R i)) ⋯ *
            Subtype.mk (p := fun (x : (i : ι) → (fun (i : ι) ↦ R i) i) ↦
              ∀ᶠ (i : ι) in 𝓕,
                Membership.mem (γ := Set ((fun (i : ι) ↦ R i) i))
                  ((fun (i : ι) ↦ (↑(B i) : Set ((fun (i : ι) ↦ R i) i))) i) (x i))
              (fun (i : ι) ↦ (↑(x i) : R i)) ⋯ :
          (a : ι) → R a)
        i =
      (1 : (a : ι) → R a) i
⊢ Subtype.mk (p := fun (x : (i : ι) → (fun (i : ι) ↦ R i) i) ↦
        ∀ᶠ (i : ι) in 𝓕,
          Membership.mem (γ := Set ((fun (i : ι) ↦ R i) i)) ((fun (i : ι) ↦ (↑(B i) : Set ((fun (i : ι) ↦ R i) i))) i)
            (x i))
        (fun (i : ι) ↦ (↑(x i)⁻¹ : R i)) ⋯ *
      Subtype.mk (p := fun (x : (i : ι) → (fun (i : ι) ↦ R i) i) ↦
        ∀ᶠ (i : ι) in 𝓕,
          Membership.mem (γ := Set ((fun (i : ι) ↦ R i) i)) ((fun (i : ι) ↦ (↑(B i) : Set ((fun (i : ι) ↦ R i) i))) i)
            (x i))
        (fun (i : ι) ↦ (↑(x i) : R i)) ⋯ =
    1

Tactic:
ext
-- Module: Mathlib.Topology.Algebra.RestrictedProduct.Units
Goal:
ι : Type u_1
R : ι → Type u_2
inst : (i : ι) → Monoid (R i)
S : ι → Type u_3
inst_1 : (i : ι) → SetLike.{u_3, u_2} (S i) (R i)
inst_2 : ∀ (i : ι), SubmonoidClass.{u_3, u_2} (S i) (R i)
B : (i : ι) → S i
𝓕 : Filter ι
x : (i : ι) → (R i)ˣ
hx : ∀ᶠ (i : ι) in 𝓕, Membership.mem (γ := Subgroup (R i)ˣ) (Submonoid.units (Submonoid.ofClass (B i))) (x i)
i : ι
⊢ (Subtype.mk (p := fun (x : (i : ι) → (fun (i : ι) ↦ R i) i) ↦
            ∀ᶠ (i : ι) in 𝓕,
              Membership.mem (γ := Set ((fun (i : ι) ↦ R i) i))
                ((fun (i : ι) ↦ (↑(B i) : Set ((fun (i : ι) ↦ R i) i))) i) (x i))
            (fun (i : ι) ↦ (↑(x i)⁻¹ : R i)) ⋯ *
          Subtype.mk (p := fun (x : (i : ι) → (fun (i : ι) ↦ R i) i) ↦
            ∀ᶠ (i : ι) in 𝓕,
              Membership.mem (γ := Set ((fun (i : ι) ↦ R i) i))
                ((fun (i : ι) ↦ (↑(B i) : Set ((fun (i : ι) ↦ R i) i))) i) (x i))
            (fun (i : ι) ↦ (↑(x i) : R i)) ⋯ :
        (a : ι) → R a)
      i =
    (1 : (a : ι) → R a) i

Tactic:
simp
-- Module: Mathlib.Topology.Algebra.RestrictedProduct.Units
Goal:
ι : Type u_1
R : ι → Type u_2
inst : (i : ι) → Monoid (R i)
S : ι → Type u_3
inst_1 : (i : ι) → SetLike.{u_3, u_2} (S i) (R i)
inst_2 : ∀ (i : ι), SubmonoidClass.{u_3, u_2} (S i) (R i)
B : (i : ι) → S i
𝓕 : Filter ι
x : Πʳ (i : ι), [R i, (↑(B i) : Set ((fun (i : ι) ↦ R i) i))]_[𝓕]ˣ
⊢ ∀ (a : ι),
    (↑(↑x : Πʳ (i : ι), [R i, (↑(B i) : Set (R i))]_[𝓕]) : (i : ι) → R i) a ∈ (↑(B a) : Set (R a)) →
      (↑x.inv : (i : ι) → R i) a ∈ (↑(B a) : Set (R a)) →
        Membership.mem (α := (R a)ˣ) (↑(Submonoid.units (Submonoid.ofClass (B a))) : Set (R a)ˣ)
          ((coeUnits (R := R) (S := S) : (a : Πʳ (i : ι), [R i, (↑(B i) : Set (R i))]_[𝓕]ˣ) → (i : ι) → (R i)ˣ) x a :
            (R a)ˣ)

Tactic:
fun i hi hi' ↦ ⟨hi, hi'⟩

Premises used: Set.Mem, setOf, Set.inter, And.intro
-- Module: Mathlib.Topology.Algebra.RestrictedProduct.Units
Goal:
ι : Type u_1
R : ι → Type u_2
inst : (i : ι) → Monoid (R i)
S : ι → Type u_3
inst_1 : (i : ι) → SetLike.{u_3, u_2} (S i) (R i)
inst_2 : ∀ (i : ι), SubmonoidClass.{u_3, u_2} (S i) (R i)
B : (i : ι) → S i
𝓕 : Filter ι
x : Πʳ (i : ι), [R i, (↑(B i) : Set ((fun (i : ι) ↦ R i) i))]_[𝓕]ˣ
h :
  ∀ (a : ι),
    Membership.mem (γ := Set ι)
      {x_1 : ι |
        Membership.mem (γ := Set ι)
            {x_2 : ι |
              (fun (i : ι) ↦
                  Membership.mem (γ := Set ((fun (i : ι) ↦ R i) i))
                    ((fun (i : ι) ↦ (↑(B i) : Set ((fun (i : ι) ↦ R i) i))) i)
                    ((↑(↑x : Πʳ (i : ι), [R i, (↑(B i) : Set ((fun (i : ι) ↦ R i) i))]_[𝓕]) :
                        (i : ι) → (fun (i : ι) ↦ R i) i)
                      i))
                x_2}
            x_1 →
          Membership.mem (γ := Set ι)
            {x_2 : ι |
              Membership.mem (γ := Set ι)
                  {x_3 : ι |
                    (fun (i : ι) ↦
                        Membership.mem (γ := Set ((fun (i : ι) ↦ R i) i))
                          ((fun (i : ι) ↦ (↑(B i) : Set ((fun (i : ι) ↦ R i) i))) i)
                          ((↑x.inv : (i : ι) → (fun (i : ι) ↦ R i) i) i))
                      x_3}
                  x_2 →
                Membership.mem (γ := Set ι)
                  {x_3 : ι |
                    (fun (i : ι) ↦
                        Membership.mem.{u_2, u_2} (α := (fun (i : ι) ↦ Units.{u_2} (R i)) i) (γ :=
                          Set ((fun (i : ι) ↦ Units.{u_2} (R i)) i))
                          ((fun (i : ι) ↦
                              (↑(Submonoid.units (Submonoid.ofClass (B i))) : Set ((fun (i : ι) ↦ (R i)ˣ) i)))
                            i)
                          ((coeUnits (R := R) (S := S) :
                                (a : Πʳ (i : ι), [R i, (↑(B i) : Set ((fun (i : ι) ↦ R i) i))]_[𝓕]ˣ) → (i : ι) → (R i)ˣ)
                              x i :
                            (R i)ˣ))
                      x_3}
                  x_2}
            x_1}
      a
h₁ :
  ∀ (a : ι),
    (↑(↑x : Πʳ (i : ι), [R i, (↑(B i) : Set (R i))]_[𝓕]) : (i : ι) → R i) a ∈ (↑(B a) : Set (R a)) →
      (↑x.inv : (i : ι) → R i) a ∈ (↑(B a) : Set (R a)) →
        Membership.mem (α := (R a)ˣ) (↑(Submonoid.units (Submonoid.ofClass (B a))) : Set (R a)ˣ)
          ((coeUnits (R := R) (S := S) : (a : Πʳ (i : ι), [R i, (↑(B i) : Set (R i))]_[𝓕]ˣ) → (i : ι) → (R i)ˣ) x a :
            (R a)ˣ)
⊢ ∀ᶠ (i : ι) in 𝓕,
    Membership.mem.{u_2, u_2} (α := (fun (i : ι) ↦ Units.{u_2} (R i)) i) (γ :=
      Set ((fun (i : ι) ↦ Units.{u_2} (R i)) i))
      ((fun (i : ι) ↦ (↑(Submonoid.units (Submonoid.ofClass (B i))) : Set ((fun (i : ι) ↦ (R i)ˣ) i))) i)
      ((coeUnits (R := R) (S := S) :
            (a : Πʳ (i : ι), [R i, (↑(B i) : Set ((fun (i : ι) ↦ R i) i))]_[𝓕]ˣ) → (i : ι) → (R i)ˣ)
          x i :
        (R i)ˣ)

Tactic:
filter_upwards [x.val.2, x.inv.2] using fun i hi hi' ↦ ⟨hi, hi'⟩

Premises used: Units.val, Units.inv, Subtype.property
-- Module: Mathlib.Topology.Algebra.RestrictedProduct.Units
Goal:
ι : Type u_1
R : ι → Type u_2
inst : (i : ι) → Monoid (R i)
S : ι → Type u_3
inst_1 : (i : ι) → SetLike.{u_3, u_2} (S i) (R i)
inst_2 : ∀ (i : ι), SubmonoidClass.{u_3, u_2} (S i) (R i)
B : (i : ι) → S i
𝓕 : Filter ι
i : ι
x : Πʳ (i : ι), [R i, (↑(B i) : Set ((fun (i : ι) ↦ R i) i))]_[𝓕]ˣ
⊢ (↑((((unitsEquiv R (S := S) :
                  (a : Πʳ (i : ι), [R i, (↑(B i) : Set ((fun (i : ι) ↦ R i) i))]_[𝓕]ˣ) →
                    Πʳ (i : ι), [(R i)ˣ, (↑(Submonoid.ofClass (B i)).units : Set ((fun (i : ι) ↦ (R i)ˣ) i))]_[𝓕])
                x :
              Πʳ (i : ι), [(R i)ˣ,
                (↑(Submonoid.units (Submonoid.ofClass (B i))) : Set ((fun (i : ι) ↦ (R i)ˣ) i))]_[𝓕]) :
            (a : ι) → (R a)ˣ)
          i) :
      R i) =
    ((↑x : Πʳ (i : ι), [R i, (↑(B i) : Set ((fun (i : ι) ↦ R i) i))]_[𝓕]) : (a : ι) → R a) i

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.RestrictedProduct.Units
Goal:
ι : Type u_1
R : ι → Type u_2
inst : (i : ι) → Monoid (R i)
S : ι → Type u_3
inst_1 : (i : ι) → SetLike.{u_3, u_2} (S i) (R i)
inst_2 : ∀ (i : ι), SubmonoidClass.{u_3, u_2} (S i) (R i)
B : (i : ι) → S i
𝓕 : Filter ι
x : Πʳ (i : ι), [R i, (↑(B i) : Set ((fun (i : ι) ↦ R i) i))]_[𝓕]ˣ
i : ι
⊢ (↑((unitsEquiv R (S := S) :
              (a : Πʳ (i : ι), [R i, (↑(B i) : Set ((fun (i : ι) ↦ R i) i))]_[𝓕]ˣ) →
                Πʳ (i : ι), [(R i)ˣ, (↑(Submonoid.ofClass (B i)).units : Set ((fun (i : ι) ↦ (R i)ˣ) i))]_[𝓕])
            x) :
        (i : ι) → (fun (i : ι) ↦ (R i)ˣ) i)
      i =
    (((unitsEquiv R (S := S) :
              (a : Πʳ (i : ι), [R i, (↑(B i) : Set ((fun (i : ι) ↦ R i) i))]_[𝓕]ˣ) →
                Πʳ (i : ι), [(R i)ˣ, (↑(Submonoid.ofClass (B i)).units : Set ((fun (i : ι) ↦ (R i)ˣ) i))]_[𝓕])
            x :
          Πʳ (i : ι), [(R i)ˣ, (↑(Submonoid.units (Submonoid.ofClass (B i))) : Set ((fun (i : ι) ↦ (R i)ˣ) i))]_[𝓕]) :
        (a : ι) → (R a)ˣ)
      i

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.Ring.Basic
Goal:
R : Type u_1
inst : TopologicalSpace R
inst_1 : NonAssocRing R
inst_2 : SeparatelyContinuousMul R
⊢ Continuous[inst, inst] fun (a : R) ↦ -a

Tactic:
simpa using continuous_id.const_mul (-1 : R)

Premises used: continuous_id, OfNat.ofNat, Continuous.const_mul, Neg.neg
-- Module: Mathlib.Topology.Algebra.Ring.Basic
Goal:
R : Type u_1
inst : NonUnitalNonAssocRing R
inst_1 : TopologicalSpace R
inst_2 : IsSemitopologicalRing R
⊢ IsTopologicalAddGroup R

Tactic:
⟨⟩

Premises used: IsTopologicalAddGroup.mk
-- Module: Mathlib.Topology.Algebra.Ring.Basic
Goal:
R : Type u_1
inst : NonUnitalNonAssocRing R
inst_1 : TopologicalSpace R
inst_2 : IsTopologicalRing R
⊢ IsTopologicalAddGroup R

Tactic:
⟨⟩

Premises used: IsTopologicalAddGroup.mk
-- Module: Mathlib.Topology.Algebra.Ring.Basic
Goal:
R : Type u_1
inst : TopologicalSpace R
inst_1 : NonUnitalNonAssocSemiring R
inst_2 : DiscreteTopology R
⊢ IsTopologicalSemiring R

Tactic:
⟨⟩

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

Tactic:
⟨⟩

Premises used: IsTopologicalRing.mk
-- Module: Mathlib.Topology.Algebra.Ring.Basic
Goal:
R : Type u_1
inst : TopologicalSpace R
inst_1 : NonUnitalSemiring R
inst_2 : IsSemitopologicalSemiring R
S : NonUnitalSubsemiring R
⊢ IsSemitopologicalSemiring.{u_1} ↥S

Tactic:
{ S.toSubsemigroup.separatelyContinuousMul, S.toAddSubmonoid.continuousAdd with }

Premises used: NonUnitalSubsemiring.toSubsemigroup, AddSubmonoid.continuousAdd, Subsemigroup.separatelyContinuousMul, IsSemitopologicalSemiring.mk, NonUnitalSubsemiring.toAddSubmonoid
-- Module: Mathlib.Topology.Algebra.Ring.Basic
Goal:
R : Type u_1
inst : TopologicalSpace R
inst_1 : NonUnitalSemiring R
inst_2 : IsTopologicalSemiring R
S : NonUnitalSubsemiring R
⊢ IsTopologicalSemiring.{u_1} ↥S

Tactic:
{ S.toSubsemigroup.continuousMul, S.toAddSubmonoid.continuousAdd with }

Premises used: NonUnitalSubsemiring.toSubsemigroup, AddSubmonoid.continuousAdd, Subsemigroup.continuousMul, NonUnitalSubsemiring.toAddSubmonoid, IsTopologicalSemiring.mk
-- Module: Mathlib.Topology.Algebra.Ring.Basic
Goal:
R : Type u_1
inst : TopologicalSpace R
inst_1 : NonUnitalSemiring R
inst_2 : IsSemitopologicalSemiring R
s : NonUnitalSubsemiring R
⊢ (↑s.topologicalClosure : Set R) = closure[inst] (↑s : Set R)

Tactic:
rfl

Premises used: setOf, closure, Set.sInter, rfl
-- Module: Mathlib.Topology.Algebra.Ring.Basic
Goal:
R : Type u_1
inst : TopologicalSpace R
inst_1 : NonUnitalSemiring R
inst_2 : IsSemitopologicalSemiring R
s : NonUnitalSubsemiring 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 : NonUnitalSemiring R
inst_2 : IsSemitopologicalSemiring R
s : NonUnitalSubsemiring 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 : NonUnitalSemiring R
inst_2 : IsSemitopologicalSemiring R
s t : NonUnitalSubsemiring 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 : NonUnitalSemiring R
inst_2 : IsSemitopologicalSemiring R
s t : NonUnitalSubsemiring 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 : Semiring R
inst_2 : IsSemitopologicalSemiring R
S : Subsemiring R
⊢ IsSemitopologicalSemiring.{u_1} ↥S

Tactic:
{ S.toSubmonoid.separatelyContinuousMul, S.toAddSubmonoid.continuousAdd with }

Premises used: AddSubmonoid.continuousAdd, IsSemitopologicalSemiring.mk, Submonoid.separatelyContinuousMul, Subsemiring.toSubmonoid, Subsemiring.toAddSubmonoid
-- Module: Mathlib.Topology.Algebra.Ring.Basic
Goal:
R : Type u_1
inst : TopologicalSpace R
inst_1 : Semiring R
inst_2 : IsTopologicalSemiring R
S : Subsemiring R
⊢ IsTopologicalSemiring.{u_1} ↥S

Tactic:
{ S.toSubmonoid.continuousMul, S.toAddSubmonoid.continuousAdd with }

Premises used: AddSubmonoid.continuousAdd, Subsemiring.toSubmonoid, Submonoid.continuousMul, IsTopologicalSemiring.mk, Subsemiring.toAddSubmonoid
-- Module: Mathlib.Topology.Algebra.Ring.Basic
Goal:
R : Type u_1
inst : TopologicalSpace R
inst_1 : Semiring R
s : Subsemiring R
X : Type u_2
inst_2 : TopologicalSpace X
inst_3 : MulAction R X
inst_4 : ContinuousSMul R X
⊢ ContinuousSMul.{u_1, u_2} (↥s) X

Tactic:
Submonoid.continuousSMul

Premises used: Set.Mem, Submonoid.continuousSMul
-- Module: Mathlib.Topology.Algebra.Ring.Basic
Goal:
R : Type u_1
inst : TopologicalSpace R
inst_1 : Semiring R
inst_2 : IsSemitopologicalSemiring R
s : Subsemiring R
⊢ (↑s.topologicalClosure : Set R) = closure[inst] (↑s : Set R)

Tactic:
rfl

Premises used: setOf, closure, Set.sInter, rfl
-- Module: Mathlib.Topology.Algebra.Ring.Basic
Goal:
R : Type u_1
inst : TopologicalSpace R
inst_1 : Semiring R
inst_2 : IsSemitopologicalSemiring R
s : Subsemiring 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 : Semiring R
inst_2 : IsSemitopologicalSemiring R
s : Subsemiring 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 : Semiring R
inst_2 : IsSemitopologicalSemiring R
s t : Subsemiring 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 : Semiring R
inst_2 : IsSemitopologicalSemiring R
s t : Subsemiring 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_1 : Type u_1
ι : Type u_2
R : ι → Type u_3
inst : (i : ι) → TopologicalSpace (R i)
inst_1 : (i : ι) → NonUnitalNonAssocRing (R i)
inst_2 : ∀ (i : ι), IsTopologicalRing.{u_3} (R i)
⊢ IsTopologicalRing ((i : ι) → R i)

Tactic:
⟨⟩

Premises used: IsTopologicalRing.mk
-- Module: Mathlib.Topology.Algebra.Ring.Basic
Goal:
R_1 : Type u_1
ι : Type u_2
R : ι → Type u_3
inst : (i : ι) → TopologicalSpace (R i)
inst_1 : (i : ι) → NonUnitalNonAssocRing (R i)
inst_2 : ∀ (i : ι), IsSemitopologicalRing.{u_3} (R i)
⊢ IsSemitopologicalRing ((i : ι) → R i)

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 : ContinuousAdd R
⊢ ContinuousAdd.{u_1} Rᵐᵒᵖ

Tactic:
continuousAdd_induced opAddEquiv.symm

Premises used: MulOpposite, MulOpposite.opAddEquiv, continuousAdd_induced, MulOpposite.unop, AddEquiv.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 : NonUnitalNonAssocSemiring R
inst_1 : TopologicalSpace R
inst_2 : IsTopologicalSemiring R
⊢ IsTopologicalSemiring.{u_1} Rᵐᵒᵖ

Tactic:
⟨⟩

Premises used: IsTopologicalSemiring.mk