awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace
Goal:
ι₁ : Type u_3
ι₂ : Type u_4
R₁ : ι₁ → Type u_5
R₂ : ι₂ → Type u_6
inst : (i : ι₁) → TopologicalSpace (R₁ i)
inst_1 : (i : ι₂) → TopologicalSpace (R₂ i)
𝓕₁ : Filter ι₁
𝓕₂ : Filter ι₂
A₁ : (i : ι₁) → Set (R₁ i)
A₂ : (i : ι₂) → Set (R₂ i)
f : ι₂ → ι₁
hf : Tendsto f 𝓕₂ 𝓕₁
φ : (j : ι₂) → R₁ (f j) → R₂ j
hφ : ∀ᶠ (j : ι₂) in 𝓕₂, MapsTo (φ j) (A₁ (f j)) (A₂ j)
φ_cont : ∀ (j : ι₂), Continuous[inst (f j), inst_1 j] (φ j)
S : Set ι₁
hS : 𝓕₁ ≤ 𝓟 S
T : Set ι₂ := f ⁻¹' S ∩ {j : ι₂ | MapsTo (φ j) (A₁ (f j)) (A₂ j)}
rw :
  ∀ (hS : S ∈ 𝓕₁),
    let T := f ⁻¹' S ∩ {j : ι₂ | MapsTo (φ j) (A₁ (f j)) (A₂ j)};
    T ∈ 𝓕₂
⊢ 𝓕₂ ≤ 𝓟 T

Tactic:
rw [le_principal_iff] at hS ⊢

Premises used: Filter.le_principal_iff
-- Module: Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace
Goal:
ι₁ : Type u_3
ι₂ : Type u_4
R₁ : ι₁ → Type u_5
R₂ : ι₂ → Type u_6
inst : (i : ι₁) → TopologicalSpace (R₁ i)
inst_1 : (i : ι₂) → TopologicalSpace (R₂ i)
𝓕₁ : Filter ι₁
𝓕₂ : Filter ι₂
A₁ : (i : ι₁) → Set (R₁ i)
A₂ : (i : ι₂) → Set (R₂ i)
f : ι₂ → ι₁
hf : Tendsto f 𝓕₂ 𝓕₁
φ : (j : ι₂) → R₁ (f j) → R₂ j
hφ : ∀ᶠ (j : ι₂) in 𝓕₂, MapsTo (φ j) (A₁ (f j)) (A₂ j)
φ_cont : ∀ (j : ι₂), Continuous[inst (f j), inst_1 j] (φ j)
S : Set ι₁
hS : S ∈ 𝓕₁
T : Set ι₂ := f ⁻¹' S ∩ {j : ι₂ | MapsTo (φ j) (A₁ (f j)) (A₂ j)}
⊢ T ∈ 𝓕₂

Tactic:
inter_mem (hf hS) hφ

Premises used: Set.Mem, Filter.inter_mem
-- Module: Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace
Goal:
ι₁ : Type u_3
ι₂ : Type u_4
R₁ : ι₁ → Type u_5
R₂ : ι₂ → Type u_6
inst : (i : ι₁) → TopologicalSpace (R₁ i)
inst_1 : (i : ι₂) → TopologicalSpace (R₂ i)
𝓕₁ : Filter ι₁
𝓕₂ : Filter ι₂
A₁ : (i : ι₁) → Set (R₁ i)
A₂ : (i : ι₂) → Set (R₂ i)
f : ι₂ → ι₁
hf : Tendsto f 𝓕₂ 𝓕₁
φ : (j : ι₂) → R₁ (f j) → R₂ j
hφ : ∀ᶠ (j : ι₂) in 𝓕₂, MapsTo (φ j) (A₁ (f j)) (A₂ j)
φ_cont : ∀ (j : ι₂), Continuous[inst (f j), inst_1 j] (φ j)
S : Set ι₁
hS : S ∈ 𝓕₁
T : Set ι₂ := f ⁻¹' S ∩ {j : ι₂ | MapsTo (φ j) (A₁ (f j)) (A₂ j)}
⊢ T ∈ 𝓕₂

Tactic:
exact inter_mem (hf hS) hφ

Premises used: Filter.inter_mem
-- Module: Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace
Goal:
ι₁ : Type u_3
ι₂ : Type u_4
R₁ : ι₁ → Type u_5
R₂ : ι₂ → Type u_6
inst : (i : ι₁) → TopologicalSpace (R₁ i)
inst_1 : (i : ι₂) → TopologicalSpace (R₂ i)
𝓕₁ : Filter ι₁
𝓕₂ : Filter ι₂
A₁ : (i : ι₁) → Set (R₁ i)
A₂ : (i : ι₂) → Set (R₂ i)
f : ι₂ → ι₁
hf : Tendsto f 𝓕₂ 𝓕₁
φ : (j : ι₂) → R₁ (f j) → R₂ j
hφ : ∀ᶠ (j : ι₂) in 𝓕₂, MapsTo (φ j) (A₁ (f j)) (A₂ j)
φ_cont : ∀ (j : ι₂), Continuous[inst (f j), inst_1 j] (φ j)
S : Set ι₁
hS : 𝓕₁ ≤ 𝓟 S
T : Set ι₂ := f ⁻¹' S ∩ {j : ι₂ | MapsTo (φ j) (A₁ (f j)) (A₂ j)}
⊢ 𝓕₂ ≤ 𝓟 T

Tactic:
have hT : 𝓕₂ ≤ 𝓟 T := by
    rw [le_principal_iff] at hS ⊢
    exact inter_mem (hf hS) hφ
-- Module: Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace
Goal:
ι₁ : Type u_3
ι₂ : Type u_4
R₁ : ι₁ → Type u_5
R₂ : ι₂ → Type u_6
inst : (i : ι₁) → TopologicalSpace (R₁ i)
inst_1 : (i : ι₂) → TopologicalSpace (R₂ i)
𝓕₁ : Filter ι₁
𝓕₂ : Filter ι₂
A₁ : (i : ι₁) → Set (R₁ i)
A₂ : (i : ι₂) → Set (R₂ i)
f : ι₂ → ι₁
hf : Tendsto f 𝓕₂ 𝓕₁
φ : (j : ι₂) → R₁ (f j) → R₂ j
hφ : ∀ᶠ (j : ι₂) in 𝓕₂, MapsTo (φ j) (A₁ (f j)) (A₂ j)
φ_cont : ∀ (j : ι₂), Continuous[inst (f j), inst_1 j] (φ j)
S : Set ι₁
hS : 𝓕₁ ≤ 𝓟 S
T : Set ι₂ := f ⁻¹' S ∩ {j : ι₂ | MapsTo (φ j) (A₁ (f j)) (A₂ j)}
hT : 𝓕₂ ≤ 𝓟 T
⊢ Tendsto f (𝓟 T) (𝓟 S)

Tactic:
aesop
-- Module: Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace
Goal:
ι₁ : Type u_3
ι₂ : Type u_4
R₁ : ι₁ → Type u_5
R₂ : ι₂ → Type u_6
inst : (i : ι₁) → TopologicalSpace (R₁ i)
inst_1 : (i : ι₂) → TopologicalSpace (R₂ i)
𝓕₁ : Filter ι₁
𝓕₂ : Filter ι₂
A₁ : (i : ι₁) → Set (R₁ i)
A₂ : (i : ι₂) → Set (R₂ i)
f : ι₂ → ι₁
hf : Tendsto f 𝓕₂ 𝓕₁
φ : (j : ι₂) → R₁ (f j) → R₂ j
hφ : ∀ᶠ (j : ι₂) in 𝓕₂, MapsTo (φ j) (A₁ (f j)) (A₂ j)
φ_cont : ∀ (j : ι₂), Continuous[inst (f j), inst_1 j] (φ j)
S : Set ι₁
hS : 𝓕₁ ≤ 𝓟 S
T : Set ι₂ := f ⁻¹' S ∩ {j : ι₂ | MapsTo (φ j) (A₁ (f j)) (A₂ j)}
hT : 𝓕₂ ≤ 𝓟 T
⊢ Tendsto f (𝓟 T) (𝓟 S)

Tactic:
have hf' : Tendsto f (𝓟 T) (𝓟 S) := by aesop
-- Module: Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace
Goal:
ι₁ : Type u_3
ι₂ : Type u_4
R₁ : ι₁ → Type u_5
R₂ : ι₂ → Type u_6
inst : (i : ι₁) → TopologicalSpace (R₁ i)
inst_1 : (i : ι₂) → TopologicalSpace (R₂ i)
𝓕₁ : Filter ι₁
𝓕₂ : Filter ι₂
A₁ : (i : ι₁) → Set (R₁ i)
A₂ : (i : ι₂) → Set (R₂ i)
f : ι₂ → ι₁
hf : Tendsto f 𝓕₂ 𝓕₁
φ : (j : ι₂) → R₁ (f j) → R₂ j
hφ : ∀ᶠ (j : ι₂) in 𝓕₂, MapsTo (φ j) (A₁ (f j)) (A₂ j)
φ_cont : ∀ (j : ι₂), Continuous[inst (f j), inst_1 j] (φ j)
S : Set ι₁
hS : 𝓕₁ ≤ 𝓟 S
T : Set ι₂ := f ⁻¹' S ∩ {j : ι₂ | MapsTo (φ j) (A₁ (f j)) (A₂ j)}
hT : 𝓕₂ ≤ 𝓟 T
hf' : Tendsto f (𝓟 T) (𝓟 S)
⊢ ∀ᶠ (j : ι₂) in 𝓟 T, MapsTo (φ j) (A₁ (f j)) (A₂ j)

Tactic:
aesop
-- Module: Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace
Goal:
ι₁ : Type u_3
ι₂ : Type u_4
R₁ : ι₁ → Type u_5
R₂ : ι₂ → Type u_6
inst : (i : ι₁) → TopologicalSpace (R₁ i)
inst_1 : (i : ι₂) → TopologicalSpace (R₂ i)
𝓕₁ : Filter ι₁
𝓕₂ : Filter ι₂
A₁ : (i : ι₁) → Set (R₁ i)
A₂ : (i : ι₂) → Set (R₂ i)
f : ι₂ → ι₁
hf : Tendsto f 𝓕₂ 𝓕₁
φ : (j : ι₂) → R₁ (f j) → R₂ j
hφ : ∀ᶠ (j : ι₂) in 𝓕₂, MapsTo (φ j) (A₁ (f j)) (A₂ j)
φ_cont : ∀ (j : ι₂), Continuous[inst (f j), inst_1 j] (φ j)
S : Set ι₁
hS : 𝓕₁ ≤ 𝓟 S
T : Set ι₂ := f ⁻¹' S ∩ {j : ι₂ | MapsTo (φ j) (A₁ (f j)) (A₂ j)}
hT : 𝓕₂ ≤ 𝓟 T
hf' : Tendsto f (𝓟 T) (𝓟 S)
⊢ ∀ᶠ (j : ι₂) in 𝓟 T, MapsTo (φ j) (A₁ (f j)) (A₂ j)

Tactic:
have hφ' : ∀ᶠ j in 𝓟 T, MapsTo (φ j) (A₁ (f j)) (A₂ j) := by aesop
-- Module: Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace
Goal:
ι₁ : Type u_3
ι₂ : Type u_4
R₁ : ι₁ → Type u_5
R₂ : ι₂ → Type u_6
inst : (i : ι₁) → TopologicalSpace (R₁ i)
inst_1 : (i : ι₂) → TopologicalSpace (R₂ i)
𝓕₁ : Filter ι₁
𝓕₂ : Filter ι₂
A₁ : (i : ι₁) → Set (R₁ i)
A₂ : (i : ι₂) → Set (R₂ i)
f : ι₂ → ι₁
hf : Tendsto f 𝓕₂ 𝓕₁
φ : (j : ι₂) → R₁ (f j) → R₂ j
hφ : ∀ᶠ (j : ι₂) in 𝓕₂, MapsTo (φ j) (A₁ (f j)) (A₂ j)
φ_cont : ∀ (j : ι₂), Continuous[inst (f j), inst_1 j] (φ j)
S : Set ι₁
hS : 𝓕₁ ≤ 𝓟 S
T : Set ι₂ := f ⁻¹' S ∩ {j : ι₂ | MapsTo (φ j) (A₁ (f j)) (A₂ j)}
hT : 𝓕₂ ≤ 𝓟 T
hf' : Tendsto f (𝓟 T) (𝓟 S)
hφ' : ∀ᶠ (j : ι₂) in 𝓟 T, MapsTo (φ j) (A₁ (f j)) (A₂ j)
⊢ mapAlong R₁ R₂ (A₁ := A₁) (A₂ := A₂) f hf φ hφ ∘ inclusion R₁ A₁ hS =
    inclusion R₂ A₂ hT ∘ mapAlong R₁ R₂ (A₁ := A₁) (A₂ := A₂) f hf' φ hφ'

Tactic:
have key : mapAlong R₁ R₂ f hf φ hφ ∘ inclusion R₁ A₁ hS =
      inclusion R₂ A₂ hT ∘ mapAlong R₁ R₂ f hf' φ hφ' := rfl
-- Module: Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace
Goal:
ι₁ : Type u_3
ι₂ : Type u_4
R₁ : ι₁ → Type u_5
R₂ : ι₂ → Type u_6
inst : (i : ι₁) → TopologicalSpace (R₁ i)
inst_1 : (i : ι₂) → TopologicalSpace (R₂ i)
𝓕₁ : Filter ι₁
𝓕₂ : Filter ι₂
A₁ : (i : ι₁) → Set (R₁ i)
A₂ : (i : ι₂) → Set (R₂ i)
f : ι₂ → ι₁
hf : Tendsto f 𝓕₂ 𝓕₁
φ : (j : ι₂) → R₁ (f j) → R₂ j
hφ : ∀ᶠ (j : ι₂) in 𝓕₂, MapsTo (φ j) (A₁ (f j)) (A₂ j)
φ_cont : ∀ (j : ι₂), Continuous[inst (f j), inst_1 j] (φ j)
S : Set ι₁
hS : 𝓕₁ ≤ 𝓟 S
T : Set ι₂ := f ⁻¹' S ∩ {j : ι₂ | MapsTo (φ j) (A₁ (f j)) (A₂ j)}
hT : 𝓕₂ ≤ 𝓟 T
hf' : Tendsto f (𝓟 T) (𝓟 S)
hφ' : ∀ᶠ (j : ι₂) in 𝓟 T, MapsTo (φ j) (A₁ (f j)) (A₂ j)
key :
  mapAlong R₁ R₂ (A₁ := A₁) (A₂ := A₂) f hf φ hφ ∘ inclusion R₁ A₁ hS =
    inclusion R₂ A₂ hT ∘ mapAlong R₁ R₂ (A₁ := A₁) (A₂ := A₂) f hf' φ hφ'
rw :
  Continuous[topologicalSpace R₁ A₁ (𝓟 S), topologicalSpace R₂ A₂ 𝓕₂]
    (inclusion R₂ A₂ hT ∘ mapAlong R₁ R₂ (A₁ := A₁) (A₂ := A₂) f hf' φ hφ')
⊢ Continuous[topologicalSpace R₁ A₁ (𝓟 S), topologicalSpace R₂ A₂ 𝓕₂]
    (mapAlong R₁ R₂ (A₁ := A₁) (A₂ := A₂) f hf φ hφ ∘ inclusion R₁ A₁ hS)

Tactic:
rw [key]
-- Module: Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace
Goal:
ι₁ : Type u_3
ι₂ : Type u_4
R₁ : ι₁ → Type u_5
R₂ : ι₂ → Type u_6
inst : (i : ι₁) → TopologicalSpace (R₁ i)
inst_1 : (i : ι₂) → TopologicalSpace (R₂ i)
𝓕₁ : Filter ι₁
𝓕₂ : Filter ι₂
A₁ : (i : ι₁) → Set (R₁ i)
A₂ : (i : ι₂) → Set (R₂ i)
f : ι₂ → ι₁
hf : Tendsto f 𝓕₂ 𝓕₁
φ : (j : ι₂) → R₁ (f j) → R₂ j
hφ : ∀ᶠ (j : ι₂) in 𝓕₂, MapsTo (φ j) (A₁ (f j)) (A₂ j)
φ_cont : ∀ (j : ι₂), Continuous[inst (f j), inst_1 j] (φ j)
S : Set ι₁
hS : 𝓕₁ ≤ 𝓟 S
T : Set ι₂ := f ⁻¹' S ∩ {j : ι₂ | MapsTo (φ j) (A₁ (f j)) (A₂ j)}
hT : 𝓕₂ ≤ 𝓟 T
hf' : Tendsto f (𝓟 T) (𝓟 S)
hφ' : ∀ᶠ (j : ι₂) in 𝓟 T, MapsTo (φ j) (A₁ (f j)) (A₂ j)
key :
  mapAlong R₁ R₂ (A₁ := A₁) (A₂ := A₂) f hf φ hφ ∘ inclusion R₁ A₁ hS =
    inclusion R₂ A₂ hT ∘ mapAlong R₁ R₂ (A₁ := A₁) (A₂ := A₂) f hf' φ hφ'
⊢ Continuous[topologicalSpace R₁ A₁ (𝓟 S), topologicalSpace R₂ A₂ 𝓕₂]
    (inclusion R₂ A₂ hT ∘ mapAlong R₁ R₂ (A₁ := A₁) (A₂ := A₂) f hf' φ hφ')

Tactic:
continuous_inclusion _ |>.comp <|
    continuous_rng_of_principal.mpr <|
    continuous_pi fun j ↦ φ_cont j |>.comp <| continuous_eval (f j)

Premises used: Iff.mpr, RestrictedProduct.continuous_rng_of_principal, Continuous.comp, continuous_pi, RestrictedProduct.continuous_inclusion, RestrictedProduct.continuous_eval
-- Module: Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace
Goal:
ι₁ : Type u_3
ι₂ : Type u_4
R₁ : ι₁ → Type u_5
R₂ : ι₂ → Type u_6
inst : (i : ι₁) → TopologicalSpace (R₁ i)
inst_1 : (i : ι₂) → TopologicalSpace (R₂ i)
𝓕₁ : Filter ι₁
𝓕₂ : Filter ι₂
A₁ : (i : ι₁) → Set (R₁ i)
A₂ : (i : ι₂) → Set (R₂ i)
f : ι₂ → ι₁
hf : Tendsto f 𝓕₂ 𝓕₁
φ : (j : ι₂) → R₁ (f j) → R₂ j
hφ : ∀ᶠ (j : ι₂) in 𝓕₂, MapsTo (φ j) (A₁ (f j)) (A₂ j)
φ_cont : ∀ (j : ι₂), Continuous[inst (f j), inst_1 j] (φ j)
S : Set ι₁
hS : 𝓕₁ ≤ 𝓟 S
T : Set ι₂ := f ⁻¹' S ∩ {j : ι₂ | MapsTo (φ j) (A₁ (f j)) (A₂ j)}
hT : 𝓕₂ ≤ 𝓟 T
hf' : Tendsto f (𝓟 T) (𝓟 S)
hφ' : ∀ᶠ (j : ι₂) in 𝓟 T, MapsTo (φ j) (A₁ (f j)) (A₂ j)
key :
  mapAlong R₁ R₂ (A₁ := A₁) (A₂ := A₂) f hf φ hφ ∘ inclusion R₁ A₁ hS =
    inclusion R₂ A₂ hT ∘ mapAlong R₁ R₂ (A₁ := A₁) (A₂ := A₂) f hf' φ hφ'
⊢ Continuous[topologicalSpace R₁ A₁ (𝓟 S), topologicalSpace R₂ A₂ 𝓕₂]
    (inclusion R₂ A₂ hT ∘ mapAlong R₁ R₂ (A₁ := A₁) (A₂ := A₂) f hf' φ hφ')

Tactic:
exact continuous_inclusion _ |>.comp <|
    continuous_rng_of_principal.mpr <|
    continuous_pi fun j ↦ φ_cont j |>.comp <| continuous_eval (f j)

Premises used: Iff.mpr, RestrictedProduct.continuous_rng_of_principal, Continuous.comp, continuous_pi, RestrictedProduct.continuous_inclusion, RestrictedProduct.continuous_eval
-- 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))]_[𝓕]
hx : ∀ (i : ι), IsUnit ((x : (a : ι) → R a) i)
hxr :
  ∀ᶠ (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)
rw : ∃ (b : Πʳ (i : ι), [R i, (↑(B i) : Set ((fun (i : ι) ↦ R i) i))]_[𝓕]), x * b = 1 ∧ b * x = 1
⊢ IsUnit x

Tactic:
rw [isUnit_iff_exists]

Premises used: isUnit_iff_exists
-- 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))]_[𝓕]
hx : ∀ (i : ι), IsUnit ((x : (a : ι) → R a) i)
hxr :
  ∀ᶠ (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)
i : ι
h :
  ∀ (h : (x : (a : ι) → R a) i ∈ B i)
    (hu : IsUnit (Subtype.mk (p := fun (x : R i) ↦ x ∈ B i) ((x : (a : ι) → R a) i) h)),
    ⋯.unit.inv ∈ (↑(B i) : Set (R i))
⊢ (∃ (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)) →
    ⋯.unit.inv ∈ (↑(B i) : Set (R i))

Tactic:
⟨h, hu⟩
-- 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))]_[𝓕]
hx : ∀ (i : ι), IsUnit ((x : (a : ι) → R a) i)
hxr :
  ∀ᶠ (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)
h :
  ∀ (i : ι) (h : (x : (a : ι) → R a) i ∈ B i)
    (hu : IsUnit (Subtype.mk (p := fun (x : R i) ↦ x ∈ B i) ((x : (a : ι) → R a) i) h)),
    ⋯.unit.inv ∈ (↑(B i) : Set (R i))
⊢ ∀ᶠ (i : ι) in 𝓕, (fun (i : ι) ↦ ⋯.unit.inv) i ∈ (↑(B i) : Set ((fun (i : ι) ↦ R i) i))

Tactic:
filter_upwards [hxr] with i ⟨h, hu⟩
-- 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))]_[𝓕]
hx : ∀ (i : ι), IsUnit ((x : (a : ι) → R a) i)
hxr :
  ∀ᶠ (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)
i : ι
h : (x : (a : ι) → R a) i ∈ B i
hu : IsUnit (Subtype.mk (p := fun (x : R i) ↦ x ∈ B i) ((x : (a : ι) → R a) i) h)
⊢ (↑⋯.unit : R i) * (↑hu.unit.inv : R i) = 1

Tactic:
have hu : (hx i).unit.1 * hu.unit.inv = 1 := Subtype.val_inj.2 hu.mul_val_inv
-- 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))]_[𝓕]
hx : ∀ (i : ι), IsUnit ((x : (a : ι) → R a) i)
hxr :
  ∀ᶠ (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)
i : ι
h : (x : (a : ι) → R a) i ∈ B i
hu_1 : IsUnit (Subtype.mk (p := fun (x : R i) ↦ x ∈ B i) ((x : (a : ι) → R a) i) h)
hu : (↑⋯.unit : R i) * (↑hu_1.unit.inv : R i) = 1
⊢ ⋯.unit.inv ∈ (↑(B i) : Set (R i))

Tactic:
simp [← Units.eq_inv_of_mul_eq_one_left hu]

Premises used: Units.eq_inv_of_mul_eq_one_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, (↑(B i) : Set ((fun (i : ι) ↦ R i) i))]_[𝓕]
hx : ∀ (i : ι), IsUnit ((x : (a : ι) → R a) i)
hxr :
  ∀ᶠ (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)
h :
  x * mk (R := R) (A := fun (i : ι) ↦ (↑(B i) : Set ((fun (i : ι) ↦ R i) i))) (fun (i : ι) ↦ ⋯.unit.inv) ⋯ = 1 ∧
    mk (R := R) (A := fun (i : ι) ↦ (↑(B i) : Set ((fun (i : ι) ↦ R i) i))) (fun (i : ι) ↦ ⋯.unit.inv) ⋯ * x = 1
⊢ ∃ (b : Πʳ (i : ι), [R i, (↑(B i) : Set ((fun (i : ι) ↦ R i) i))]_[𝓕]), x * b = 1 ∧ b * x = 1

Tactic:
use .mk (fun i ↦ (hx i).unit.inv) (by
    filter_upwards [hxr] with i ⟨h, hu⟩
    have hu : (hx i).unit.1 * hu.unit.inv = 1 := Subtype.val_inj.2 hu.mul_val_inv
    simp [← Units.eq_inv_of_mul_eq_one_left hu])
-- 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))]_[𝓕]
hx : ∀ (i : ι), IsUnit ((x : (a : ι) → R a) i)
hxr :
  ∀ᶠ (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)
⊢ x * mk (R := R) (A := fun (i : ι) ↦ (↑(B i) : Set ((fun (i : ι) ↦ R i) i))) (fun (i : ι) ↦ ⋯.unit.inv) ⋯ = 1 ∧
    mk (R := R) (A := fun (i : ι) ↦ (↑(B i) : Set ((fun (i : ι) ↦ R i) i))) (fun (i : ι) ↦ ⋯.unit.inv) ⋯ * x = 1

Tactic:
simp [RestrictedProduct.ext_iff]

Premises used: RestrictedProduct.ext_iff
-- 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))]_[𝓕]
hx : IsUnit x
⊢ ∃ (b : Πʳ (i : ι), [R i, (↑(B i) : Set (R i))]_[𝓕]),
    ∀ (x_1 : ι),
      (x * b : (a : ι) → R a) x_1 = (1 : (a : ι) → R a) x_1 ∧ (b * x : (a : ι) → R a) x_1 = (1 : (a : ι) → R a) x_1

Tactic:
simp only [isUnit_iff_exists, RestrictedProduct.ext_iff, ← forall_and] at hx

Premises used: isUnit_iff_exists, RestrictedProduct.ext_iff, forall_and
-- 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))]_[𝓕]
hx :
  ∃ (b : Πʳ (i : ι), [R i, (↑(B i) : Set (R i))]_[𝓕]),
    ∀ (x_1 : ι),
      (x * b : (a : ι) → R a) x_1 = (1 : (a : ι) → R a) x_1 ∧ (b * x : (a : ι) → R a) x_1 = (1 : (a : ι) → R a) x_1
simp :
  (∀ (i : ι), ∃ (b : R i), (x : (a : ι) → R a) i * b = 1 ∧ b * (x : (a : ι) → R a) i = 1) ∧
    ∀ᶠ (i : ι) in 𝓕,
      ∃ (h : (x : (a : ι) → R a) i ∈ B i) (b : ↥(B i)),
        Subtype.mk (p := fun (x : R i) ↦ x ∈ B i) ((x : (a : ι) → R a) i) ⋯ * b = 1 ∧
          b * Subtype.mk (p := fun (x : R i) ↦ x ∈ B i) ((x : (a : ι) → R a) i) ⋯ = 1
⊢ (∀ (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:
simp only [isUnit_iff_exists]

Premises used: isUnit_iff_exists
-- 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))]_[𝓕]
hx :
  ∃ (b : Πʳ (i : ι), [R i, (↑(B i) : Set (R i))]_[𝓕]),
    ∀ (x_1 : ι),
      (x * b : (a : ι) → R a) x_1 = (1 : (a : ι) → R a) x_1 ∧ (b * x : (a : ι) → R a) x_1 = (1 : (a : ι) → R a) x_1
choose :
  ∀ (b : Πʳ (i : ι), [R i, (↑(B i) : Set (R i))]_[𝓕])
    (hb :
      ∀ (x_1 : ι),
        (x * b : (a : ι) → R a) x_1 = (1 : (a : ι) → R a) x_1 ∧ (b * x : (a : ι) → R a) x_1 = (1 : (a : ι) → R a) x_1),
    (∀ (i : ι), ∃ (b : R i), (x : (a : ι) → R a) i * b = 1 ∧ b * (x : (a : ι) → R a) i = 1) ∧
      ∀ᶠ (i : ι) in 𝓕,
        ∃ (h : (x : (a : ι) → R a) i ∈ B i) (b : ↥(B i)),
          Subtype.mk (p := fun (x : R i) ↦ x ∈ B i) ((x : (a : ι) → R a) i) ⋯ * b = 1 ∧
            b * Subtype.mk (p := fun (x : R i) ↦ x ∈ B i) ((x : (a : ι) → R a) i) ⋯ = 1
⊢ (∀ (i : ι), ∃ (b : R i), (x : (a : ι) → R a) i * b = 1 ∧ b * (x : (a : ι) → R a) i = 1) ∧
    ∀ᶠ (i : ι) in 𝓕,
      ∃ (h : (x : (a : ι) → R a) i ∈ B i) (b : ↥(B i)),
        Subtype.mk (p := fun (x : R i) ↦ x ∈ B i) ((x : (a : ι) → R a) i) ⋯ * b = 1 ∧
          b * Subtype.mk (p := fun (x : R i) ↦ x ∈ B i) ((x : (a : ι) → R a) i) ⋯ = 1

Tactic:
choose b hb using hx
-- 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))]_[𝓕]
b : Πʳ (i : ι), [R i, (↑(B i) : Set (R i))]_[𝓕]
hb_1 :
  ∀ (x_1 : ι),
    (x * b : (a : ι) → R a) x_1 = (1 : (a : ι) → R a) x_1 ∧ (b * x : (a : ι) → R a) x_1 = (1 : (a : ι) → R a) x_1
i : ι
hx : (↑x : (i : ι) → R i) i ∈ (↑(B i) : Set (R i))
hb : (↑b : (i : ι) → R i) i ∈ (↑(B i) : Set (R i))
⊢ Subtype.mk (p := fun (x : R i) ↦ x ∈ B i) ((x : (a : ι) → R a) i) ⋯ *
        Subtype.mk (p := fun (x : R i) ↦ x ∈ B i) ((b : (a : ι) → R a) i) hb =
      1 ∧
    Subtype.mk (p := fun (x : R i) ↦ x ∈ B i) ((b : (a : ι) → R a) i) hb *
        Subtype.mk (p := fun (x : R i) ↦ x ∈ B i) ((x : (a : ι) → R a) i) ⋯ =
      1

Tactic:
simp_all [← SetLike.coe_eq_coe]

Premises used: SetLike.coe_eq_coe
-- 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))]_[𝓕]
b : Πʳ (i : ι), [R i, (↑(B i) : Set (R i))]_[𝓕]
hb :
  ∀ (x_1 : ι),
    (x * b : (a : ι) → R a) x_1 = (1 : (a : ι) → R a) x_1 ∧ (b * x : (a : ι) → R a) x_1 = (1 : (a : ι) → R a) x_1
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 : ι) → (fun (i : ι) ↦ R i) i) i))
                x_2}
            x_1 →
          Membership.mem (γ := Set ι)
            {x_2 : ι |
              Membership.mem (γ := Set ι)
                  {x : ι |
                    (fun (i : ι) ↦
                        Membership.mem (γ := Set ((fun (i : ι) ↦ R i) i)) ((fun (i : ι) ↦ (↑(B i) : Set (R i))) i)
                          ((↑b : (i : ι) → (fun (i : ι) ↦ R i) i) i))
                      x}
                  x_2 →
                Membership.mem (γ := Set ι)
                  {x_3 : ι |
                    (fun (i : ι) ↦
                        ∃ (h : (x : (a : ι) → R a) i ∈ B i) (b : ↥(B i)),
                          Subtype.mk (p := fun (x : R i) ↦ x ∈ B i) ((x : (a : ι) → R a) i) ⋯ * b = 1 ∧
                            b * Subtype.mk (p := fun (x : R i) ↦ x ∈ B i) ((x : (a : ι) → R a) i) ⋯ = 1)
                      x_3}
                  x_2}
            x_1}
      a
h₁ :
  ∀ (a : ι),
    (↑x : (i : ι) → R i) a ∈ (↑(B a) : Set (R a)) →
      (↑b : (i : ι) → R i) a ∈ (↑(B a) : Set (R a)) →
        ∃ (h : (x : (a : ι) → R a) a ∈ B a) (b : ↥(B a)),
          Subtype.mk (p := fun (x : R a) ↦ x ∈ B a) ((x : (a : ι) → R a) a) ⋯ * b = 1 ∧
            b * Subtype.mk (p := fun (x : R a) ↦ x ∈ B a) ((x : (a : ι) → R a) a) ⋯ = 1
⊢ ∀ᶠ (i : ι) in 𝓕,
    ∃ (h : (x : (a : ι) → R a) i ∈ B i) (b : ↥(B i)),
      Subtype.mk (p := fun (x : R i) ↦ x ∈ B i) ((x : (a : ι) → R a) i) ⋯ * b = 1 ∧
        b * Subtype.mk (p := fun (x : R i) ↦ x ∈ B i) ((x : (a : ι) → R a) i) ⋯ = 1

Tactic:
filter_upwards [x.2, b.2] using
    fun i hx hb ↦ ⟨hx, ⟨b i, hb⟩, by simp_all [← SetLike.coe_eq_coe]⟩

Premises used: 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 ι
x : Πʳ (i : ι), [R i, (↑(B i) : Set ((fun (i : ι) ↦ R i) i))]_[𝓕]
b : Πʳ (i : ι), [R i, (↑(B i) : Set (R i))]_[𝓕]
hb :
  ∀ (x_1 : ι),
    (x * b : (a : ι) → R a) x_1 = (1 : (a : ι) → R a) x_1 ∧ (b * x : (a : ι) → R a) x_1 = (1 : (a : ι) → R a) x_1
⊢ (∀ (i : ι), ∃ (b : R i), (x : (a : ι) → R a) i * b = 1 ∧ b * (x : (a : ι) → R a) i = 1) ∧
    ∀ᶠ (i : ι) in 𝓕,
      ∃ (h : (x : (a : ι) → R a) i ∈ B i) (b : ↥(B i)),
        Subtype.mk (p := fun (x : R i) ↦ x ∈ B i) ((x : (a : ι) → R a) i) ⋯ * b = 1 ∧
          b * Subtype.mk (p := fun (x : R i) ↦ x ∈ B i) ((x : (a : ι) → R a) i) ⋯ = 1

Tactic:
exact ⟨Classical.skolem.symm.1 ⟨b, hb⟩, by filter_upwards [x.2, b.2] using
    fun i hx hb ↦ ⟨hx, ⟨b i, hb⟩, by simp_all [← SetLike.coe_eq_coe]⟩⟩