awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace (goal)
Goal:
ι : Type u_1
n : Type u_3
inst : Finite n
X : Type u_4
inst_1 : TopologicalSpace X
A : n → ι → Type u_5
inst_2 : (j : n) → (i : ι) → TopologicalSpace (A j i)
C : (j : n) → (i : ι) → Set (A j i)
hCopen : ∀ (j : n) (i : ι), IsOpen[inst_2 j i] (C j i)
f : ((j : n) → Πʳ (i : ι), [A j i, C j i]) → X
H :
  ∀ (S : Set ι) (hS : cofinite ≤ 𝓟 S),
    Continuous[Pi.topologicalSpace, inst_1]
      (f ∘
        Pi.map (α := fun (x : n) ↦ Πʳ (i : ι), [A x i, C x i]_[𝓟 S]) (β := fun (j : n) ↦ Πʳ (i : ι), [A j i, C j i])
          fun (x : n) ↦ inclusion (A x) (C x) hS)
x : (j : n) → Πʳ (i : ι), [A j i, C j i]
S : Set ι := {i : ι | ∀ (j : n), (x j : (a : ι) → A j a) i ∈ C j i}
hS : cofinite ≤ 𝓟 S
x' : (j : n) → Πʳ (i : ι), [A j i, C j i]_[𝓟 S] :=
  fun (j : n) ↦ mk (R := A j) (A := C j) (fun (i : ι) ↦ (x j : (a : ι) → A j a) i) ⋯
hxx' :
  Pi.map (α := fun (j : n) ↦ Πʳ (i : ι), [A j i, C j i]_[𝓟 S]) (β := fun (j : n) ↦ Πʳ (i : ι), [A j i, C j i])
      (fun (j : n) ↦ inclusion (A j) (C j) hS) x' =
    x
⊢ Tendsto f (𝓝 x) (𝓝 (f x))
have simp_rw : Tendsto
  (f ∘
    Pi.map (α := fun (i : n) ↦ Πʳ (i_1 : ι), [A i i_1, C i i_1]_[𝓟 S]) (β := fun (i : n) ↦
      Πʳ (i_1 : ι), [A i i_1, C i i_1]) fun (i : n) ↦ inclusion (A i) (C i) hS)
  (𝓝 x')
  (𝓝
    (f
      (Pi.map (α := fun (j : n) ↦ Πʳ (i : ι), [A j i, C j i]_[𝓟 S]) (β := fun (j : n) ↦ Πʳ (i : ι), [A j i, C j i])
        (fun (i : n) ↦ inclusion (A i) (C i) hS) x')))
Tactic: simp_rw [← hxx', nhds_pi, Pi.map_apply, nhds_eq_map_inclusion (hCopen _), ← map_piMap_pi_finite,
    tendsto_map'_iff, ← nhds_pi]
-- Lean 4 proof step from Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace (goal)
Goal:
ι : Type u_1
R : ι → Type u_2
A : (i : ι) → Set (R i)
𝓕_1 𝓖 : Filter ι
S : ι → Type u_3
inst : (i : ι) → SetLike.{u_3, u_2} (S i) (R i)
B : (i : ι) → S i
T : Set ι
𝓕 : Filter ι
inst_1 : (i : ι) → TopologicalSpace (R i)
inst_2 : (i : ι) → Inv (R i)
inst_3 : ∀ (i : ι), InvMemClass.{u_3, u_2} (S i) (R i)
inst_4 : ∀ (i : ι), ContinuousInv.{u_2} (R i)
⊢ Continuous[topologicalSpace R (fun (i : ι) ↦ (↑(B i) : Set ((fun (i : ι) ↦ R i) i))) 𝓕,
      topologicalSpace R (fun (i : ι) ↦ (↑(B i) : Set ((fun (i : ι) ↦ R i) i))) 𝓕]
    fun (a : Πʳ (i : ι), [R i, (↑(B i) : Set ((fun (i : ι) ↦ R i) i))]_[𝓕]) ↦ a⁻¹
have rw : ∀ (S_1 : Set ι) (hS : 𝓕 ≤ 𝓟 S_1),
  Continuous[topologicalSpace R (fun (i : ι) ↦ (↑(B i) : Set ((fun (i : ι) ↦ R i) i))) (𝓟 S_1),
      topologicalSpace R (fun (i : ι) ↦ (↑(B i) : Set ((fun (i : ι) ↦ R i) i))) 𝓕]
    ((fun (a : Πʳ (i : ι), [R i, (↑(B i) : Set ((fun (i : ι) ↦ R i) i))]_[𝓕]) ↦ a⁻¹) ∘
      inclusion R (fun (i : ι) ↦ (↑(B i) : Set ((fun (i : ι) ↦ R i) i))) hS)
Tactic: rw [continuous_dom]
-- Lean 4 proof step from Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace (hypothesis)
Goal:
ι : Type u_1
R : ι → Type u_2
A : (i : ι) → Set (R i)
𝓕_1 𝓖 : Filter ι
S : ι → Type u_3
inst : (i : ι) → SetLike.{u_3, u_2} (S i) (R i)
B : (i : ι) → S i
T_1 : Set ι
𝓕 : Filter ι
inst_1 : (i : ι) → TopologicalSpace (R i)
inst_2 : (i : ι) → Inv (R i)
inst_3 : ∀ (i : ι), InvMemClass.{u_3, u_2} (S i) (R i)
inst_4 : ∀ (i : ι), ContinuousInv.{u_2} (R i)
T : Set ι
hT : 𝓕 ≤ 𝓟 T
⊢ Continuous[topologicalSpace R (fun (i : ι) ↦ (↑(B i) : Set ((fun (i : ι) ↦ R i) i))) (𝓟 T),
      topologicalSpace R (fun (i : ι) ↦ (↑(B i) : Set ((fun (i : ι) ↦ R i) i))) 𝓕]
    ((fun (a : Πʳ (i : ι), [R i, (↑(B i) : Set ((fun (i : ι) ↦ R i) i))]_[𝓕]) ↦ a⁻¹) ∘
      inclusion R (fun (i : ι) ↦ (↑(B i) : Set ((fun (i : ι) ↦ R i) i))) hT)
have this : ContinuousInv Πʳ (i : ι), [R i, (↑(B i) : Set ((fun (i : ι) ↦ R i) i))]_[𝓟 T]
Tactic: haveI : ContinuousInv (Πʳ i, [R i, B i]_[𝓟 T]) :=
      isEmbedding_coe_of_principal.continuousInv fun _ ↦ rfl
-- Lean 4 proof step from Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace (goal)
Goal:
ι : Type u_1
R : ι → Type u_2
A : (i : ι) → Set (R i)
𝓕_1 𝓖 : Filter ι
S : ι → Type u_3
inst : (i : ι) → SetLike.{u_3, u_2} (S i) (R i)
B : (i : ι) → S i
T : Set ι
𝓕 : Filter ι
inst_1 : (i : ι) → TopologicalSpace (R i)
G : Type u_4
inst_2 : (i : ι) → SMul.{u_4, u_2} G (R i)
inst_3 : ∀ (i : ι), SMulMemClass.{u_3, u_4, u_2} (S i) G (R i)
inst_4 : ∀ (i : ι), ContinuousConstSMul.{u_4, u_2} G (R i)
g : G
⊢ Continuous[topologicalSpace R (fun (i : ι) ↦ (↑(B i) : Set ((fun (i : ι) ↦ R i) i))) 𝓕,
      topologicalSpace R (fun (i : ι) ↦ (↑(B i) : Set ((fun (i : ι) ↦ R i) i))) 𝓕]
    fun (x : Πʳ (i : ι), [R i, (↑(B i) : Set ((fun (i : ι) ↦ R i) i))]_[𝓕]) ↦ g • x
have rw : ∀ (S_1 : Set ι) (hS : 𝓕 ≤ 𝓟 S_1),
  Continuous[topologicalSpace R (fun (i : ι) ↦ (↑(B i) : Set ((fun (i : ι) ↦ R i) i))) (𝓟 S_1),
      topologicalSpace R (fun (i : ι) ↦ (↑(B i) : Set ((fun (i : ι) ↦ R i) i))) 𝓕]
    ((fun (x : Πʳ (i : ι), [R i, (↑(B i) : Set ((fun (i : ι) ↦ R i) i))]_[𝓕]) ↦ g • x) ∘
      inclusion R (fun (i : ι) ↦ (↑(B i) : Set ((fun (i : ι) ↦ R i) i))) hS)
Tactic: rw [continuous_dom]
-- Lean 4 proof step from Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace (hypothesis)
Goal:
ι : Type u_1
R : ι → Type u_2
A : (i : ι) → Set (R i)
𝓕_1 𝓖 : Filter ι
S : ι → Type u_3
inst : (i : ι) → SetLike.{u_3, u_2} (S i) (R i)
B : (i : ι) → S i
T_1 : Set ι
𝓕 : Filter ι
inst_1 : (i : ι) → TopologicalSpace (R i)
G : Type u_4
inst_2 : (i : ι) → SMul.{u_4, u_2} G (R i)
inst_3 : ∀ (i : ι), SMulMemClass.{u_3, u_4, u_2} (S i) G (R i)
inst_4 : ∀ (i : ι), ContinuousConstSMul.{u_4, u_2} G (R i)
g : G
T : Set ι
hT : 𝓕 ≤ 𝓟 T
⊢ Continuous[topologicalSpace R (fun (i : ι) ↦ (↑(B i) : Set ((fun (i : ι) ↦ R i) i))) (𝓟 T),
      topologicalSpace R (fun (i : ι) ↦ (↑(B i) : Set ((fun (i : ι) ↦ R i) i))) 𝓕]
    ((fun (x : Πʳ (i : ι), [R i, (↑(B i) : Set ((fun (i : ι) ↦ R i) i))]_[𝓕]) ↦ g • x) ∘
      inclusion R (fun (i : ι) ↦ (↑(B i) : Set ((fun (i : ι) ↦ R i) i))) hT)
have this : ContinuousConstSMul G Πʳ (i : ι), [R i, (↑(B i) : Set ((fun (i : ι) ↦ R i) i))]_[𝓟 T]
Tactic: haveI : ContinuousConstSMul G (Πʳ i, [R i, B i]_[𝓟 T]) :=
      isEmbedding_coe_of_principal.continuousConstSMul id rfl
-- Lean 4 proof step from Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace (goal)
Goal:
ι : Type u_1
R : ι → Type u_2
A : (i : ι) → Set (R i)
𝓕_1 𝓖 : Filter ι
S : ι → Type u_3
inst : (i : ι) → SetLike.{u_3, u_2} (S i) (R i)
B : (i : ι) → S i
T : Set ι
𝓕 : Filter ι
inst_1 : (i : ι) → TopologicalSpace (R i)
hBopen : Fact (∀ (i : ι), IsOpen[inst_1 i] (↑(B i) : Set (R i)))
inst_2 : (i : ι) → Mul (R i)
inst_3 : ∀ (i : ι), MulMemClass.{u_3, u_2} (S i) (R i)
inst_4 : ∀ (i : ι), ContinuousMul.{u_2} (R i)
⊢ Continuous[instTopologicalSpaceProd,
      topologicalSpace R (fun (i : ι) ↦ (↑(B i) : Set ((fun (i : ι) ↦ R i) i))) cofinite]
    fun
      (p :
        Πʳ (i : ι), [R i, (↑(B i) : Set ((fun (i : ι) ↦ R i) i))] ×
          Πʳ (i : ι), [R i, (↑(B i) : Set ((fun (i : ι) ↦ R i) i))]) ↦
    p.1 * p.2
have rw : ∀ (S_1 : Set ι) (hS : cofinite ≤ 𝓟 S_1),
  Continuous[instTopologicalSpaceProd,
      topologicalSpace R (fun (i : ι) ↦ (↑(B i) : Set ((fun (i : ι) ↦ R i) i))) cofinite]
    ((fun
          (p :
            Πʳ (i : ι), [R i, (↑(B i) : Set ((fun (i : ι) ↦ R i) i))] ×
              Πʳ (i : ι), [R i, (↑(B i) : Set ((fun (i : ι) ↦ R i) i))]) ↦
        p.1 * p.2) ∘
      Prod.map (inclusion R (fun (i : ι) ↦ (↑(B i) : Set (R i))) hS)
        (inclusion R (fun (i : ι) ↦ (↑(B i) : Set (R i))) hS))
Tactic: rw [continuous_dom_prod hBopen.out hBopen.out]
-- Lean 4 proof step from Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace (goal)
Goal:
ι : Type u_1
R : ι → Type u_2
A : (i : ι) → Set (R i)
𝓕_1 𝓖 : Filter ι
S : ι → Type u_3
inst : (i : ι) → SetLike.{u_3, u_2} (S i) (R i)
B : (i : ι) → S i
T : Set ι
𝓕 : Filter ι
inst_1 : (i : ι) → TopologicalSpace (R i)
hBopen : Fact (∀ (i : ι), IsOpen[inst_1 i] (↑(B i) : Set (R i)))
G : Type u_4
inst_2 : TopologicalSpace G
inst_3 : (i : ι) → SMul.{u_4, u_2} G (R i)
inst_4 : ∀ (i : ι), SMulMemClass.{u_3, u_4, u_2} (S i) G (R i)
inst_5 : ∀ (i : ι), ContinuousSMul.{u_4, u_2} G (R i)
⊢ Continuous[instTopologicalSpaceProd,
      topologicalSpace R (fun (i : ι) ↦ (↑(B i) : Set ((fun (i : ι) ↦ R i) i))) cofinite]
    fun (p : G × Πʳ (i : ι), [R i, (↑(B i) : Set ((fun (i : ι) ↦ R i) i))]) ↦ p.1 • p.2
have rw : ∀ (S_1 : Set ι) (hS : cofinite ≤ 𝓟 S_1),
  Continuous[instTopologicalSpaceProd,
      topologicalSpace R (fun (i : ι) ↦ (↑(B i) : Set ((fun (i : ι) ↦ R i) i))) cofinite]
    ((fun (p : G × Πʳ (i : ι), [R i, (↑(B i) : Set ((fun (i : ι) ↦ R i) i))]) ↦ p.1 • p.2) ∘
      Prod.map id (inclusion R (fun (i : ι) ↦ (↑(B i) : Set (R i))) hS))
Tactic: rw [continuous_dom_prod_left hBopen.out]
-- Lean 4 proof step from Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace (goal)
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)
⊢ Continuous[topologicalSpace R₁ A₁ 𝓕₁, topologicalSpace R₂ A₂ 𝓕₂] (mapAlong R₁ R₂ (A₁ := A₁) (A₂ := A₂) f hf φ hφ)
have rw : ∀ (S : Set ι₁) (hS : 𝓕₁ ≤ 𝓟 S),
  Continuous[topologicalSpace R₁ A₁ (𝓟 S), topologicalSpace R₂ A₂ 𝓕₂]
    (mapAlong R₁ R₂ (A₁ := A₁) (A₂ := A₂) f hf φ hφ ∘ inclusion R₁ A₁ hS)
Tactic: rw [continuous_dom]
-- Lean 4 proof step from Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace (goal)
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
have rw : ∀ (hS : S ∈ 𝓕₁),
  let T := f ⁻¹' S ∩ {j : ι₂ | MapsTo (φ j) (A₁ (f j)) (A₂ j)};
  T ∈ 𝓕₂
Tactic: rw [le_principal_iff] at hS ⊢
Cleared hypotheses: hS, T
-- Lean 4 proof step from Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace (hypothesis)
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)}
⊢ Continuous[topologicalSpace R₁ A₁ (𝓟 S), topologicalSpace R₂ A₂ 𝓕₂]
    (mapAlong R₁ R₂ (A₁ := A₁) (A₂ := A₂) f hf φ hφ ∘ inclusion R₁ A₁ hS)
have hT : 𝓕₂ ≤ 𝓟 T
Tactic: have hT : 𝓕₂ ≤ 𝓟 T := by
    rw [le_principal_iff] at hS ⊢
    exact inter_mem (hf hS) hφ
-- Lean 4 proof step from Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace (hypothesis)
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
⊢ Continuous[topologicalSpace R₁ A₁ (𝓟 S), topologicalSpace R₂ A₂ 𝓕₂]
    (mapAlong R₁ R₂ (A₁ := A₁) (A₂ := A₂) f hf φ hφ ∘ inclusion R₁ A₁ hS)
have hf' : Tendsto f (𝓟 T) (𝓟 S)
Tactic: have hf' : Tendsto f (𝓟 T) (𝓟 S) := by aesop
-- Lean 4 proof step from Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace (hypothesis)
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)
⊢ Continuous[topologicalSpace R₁ A₁ (𝓟 S), topologicalSpace R₂ A₂ 𝓕₂]
    (mapAlong R₁ R₂ (A₁ := A₁) (A₂ := A₂) f hf φ hφ ∘ inclusion R₁ A₁ hS)
have hφ' : ∀ᶠ (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
-- Lean 4 proof step from Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace (hypothesis)
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)
⊢ Continuous[topologicalSpace R₁ A₁ (𝓟 S), topologicalSpace R₂ A₂ 𝓕₂]
    (mapAlong R₁ R₂ (A₁ := A₁) (A₂ := A₂) f hf φ hφ ∘ inclusion R₁ A₁ hS)
have 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φ'
Tactic: have key : mapAlong R₁ R₂ f hf φ hφ ∘ inclusion R₁ A₁ hS =
      inclusion R₂ A₂ hT ∘ mapAlong R₁ R₂ f hf' φ hφ' := rfl
-- Lean 4 proof step from Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace (goal)
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₂ 𝓕₂]
    (mapAlong R₁ R₂ (A₁ := A₁) (A₂ := A₂) f hf φ hφ ∘ inclusion R₁ A₁ hS)
have rw : Continuous[topologicalSpace R₁ A₁ (𝓟 S), topologicalSpace R₂ A₂ 𝓕₂]
  (inclusion R₂ A₂ hT ∘ mapAlong R₁ R₂ (A₁ := A₁) (A₂ := A₂) f hf' φ hφ')
Tactic: rw [key]
-- Lean 4 proof step from Mathlib.Topology.Algebra.RestrictedProduct.Units (goal)
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)
⊢ IsUnit x
have rw : ∃ (b : Πʳ (i : ι), [R i, (↑(B i) : Set ((fun (i : ι) ↦ R i) i))]_[𝓕]), x * b = 1 ∧ b * x = 1
Tactic: rw [isUnit_iff_exists]
-- Lean 4 proof step from Mathlib.Topology.Algebra.RestrictedProduct.Units (goal)
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), IsUnit (Subtype.mk (p := fun (x : R i) ↦ x ∈ B i) ((x : (a : ι) → R a) i) h)) →
    ⋯.unit.inv ∈ (↑(B i) : Set (R i))
have 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)),
  sorry.unit.inv ∈ (↑(B i) : Set (R i))
Tactic: ⟨h, hu⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.RestrictedProduct.Units (goal)
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 : ι) in 𝓕, (fun (i : ι) ↦ ⋯.unit.inv) i ∈ (↑(B i) : Set ((fun (i : ι) ↦ R i) i))
have 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)), sorry.unit.inv ∈ (↑(B i) : Set (R i))
Tactic: filter_upwards [hxr] with i ⟨h, hu⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.RestrictedProduct.Units (hypothesis)
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.inv ∈ (↑(B i) : Set (R i))
have hu₁ : (↑sorry.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
-- Lean 4 proof step from Mathlib.Topology.Algebra.RestrictedProduct.Units (goal)
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)
⊢ ∃ (b : Πʳ (i : ι), [R i, (↑(B i) : Set ((fun (i : ι) ↦ R i) i))]_[𝓕]), x * b = 1 ∧ b * x = 1
have h : x * mk (R := R) (A := fun (i : ι) ↦ (↑(B i) : Set ((fun (i : ι) ↦ R i) i))) (fun (i : ι) ↦ sorry.unit.inv) sorry = 1 ∧
  mk (R := R) (A := fun (i : ι) ↦ (↑(B i) : Set ((fun (i : ι) ↦ R i) i))) (fun (i : ι) ↦ sorry.unit.inv) sorry * 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])
-- Lean 4 proof step from Mathlib.Topology.Algebra.RestrictedProduct.Units (hypothesis)
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
⊢ (∀ (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)
have 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
Tactic: simp only [isUnit_iff_exists, RestrictedProduct.ext_iff, ← forall_and] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Topology.Algebra.RestrictedProduct.Units (goal)
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
⊢ (∀ (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)
have 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) sorry * b = 1 ∧
        b * Subtype.mk (p := fun (x : R i) ↦ x ∈ B i) ((x : (a : ι) → R a) i) sorry = 1
Tactic: simp only [isUnit_iff_exists]
-- Lean 4 proof step from Mathlib.Topology.Algebra.RestrictedProduct.Units (goal)
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
⊢ (∀ (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
have 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) sorry * b = 1 ∧
          b * Subtype.mk (p := fun (x : R i) ↦ x ∈ B i) ((x : (a : ι) → R a) i) sorry = 1
Tactic: choose b hb using hx
Cleared hypotheses: hx