awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Algebra.ProperAction.Basic (hypothesis)
Goal:
G : Type u_1
X : Type u_2
inst : Group G
inst_1 : MulAction G X
inst_2 : TopologicalSpace G
inst_3 : TopologicalSpace X
inst_4 : ProperSMul G X
s : Set G
t : Set X
hs : IsClosed[inst_2] s
ht : IsCompact t
Ψ : Prod.{u_1, u_2} G (↑t : Type u_2) → X × (↑t : Type u_2) :=
  fun (gx : Prod.{u_1, u_2} G (↑t : Type u_2)) ↦ (gx.1 • (↑gx.2 : X), gx.2)
Ψ_proper : IsProperMap Ψ
this : s • t = fst ∘ Ψ '' fst ⁻¹' s
⊢ IsClosed[inst_3] (fst ∘ Ψ '' fst ⁻¹' s)
have this₁ : CompactSpace.{u_2} (↑t : Type u_2)
Tactic: have : CompactSpace t := isCompact_iff_compactSpace.mp ht
-- Lean 4 proof step from Mathlib.Topology.Algebra.ProperAction.Basic (goal)
Goal:
X : Type u_2
inst : TopologicalSpace X
G : Type u_3
inst_1 : Group G
inst_2 : MulAction G X
inst_3 : TopologicalSpace G
inst_4 : ProperSMul G X
U V : Set X
hU : IsCompact U
hV : IsCompact V
⊢ IsCompact.{u_3} (X := G) {g : G | (g • U ∩ V).Nonempty}
have h : Eq.{u_3 + 1} (α := Set G) {g : G | (g • U ∩ V).Nonempty}
  (image (α := G × X) fst ((fun (gx : G × X) ↦ (gx.1 • gx.2, gx.2)) ⁻¹' V ×ˢ U))
Tactic: convert!
    ((ProperSMul.isProperMap_smul_pair (G := G)).isCompact_preimage (hV.prod hU)).image
      continuous_fst
-- Lean 4 proof step from Mathlib.Topology.Algebra.ProperAction.Basic (goal)
Goal:
X : Type u_2
inst : TopologicalSpace X
G : Type u_3
inst_1 : Group G
inst_2 : MulAction G X
inst_3 : TopologicalSpace G
inst_4 : ProperSMul G X
U V : Set X
hU : IsCompact U
hV : IsCompact V
⊢ Eq.{u_3 + 1} (α := Set G) {g : G | (g • U ∩ V).Nonempty}
    (image (α := G × X) fst ((fun (gx : G × X) ↦ (gx.1 • gx.2, gx.2)) ⁻¹' V ×ˢ U))
have h : ∀ (g : G),
  Membership.mem (γ := Set G) {g : G | (g • U ∩ V).Nonempty} g ↔
    Membership.mem (γ := Set G) (image (α := G × X) fst ((fun (gx : G × X) ↦ (gx.1 • gx.2, gx.2)) ⁻¹' V ×ˢ U)) g
Tactic: ext g
-- Lean 4 proof step from Mathlib.Topology.Algebra.ProperAction.Basic (goal)
Goal:
X : Type u_2
inst : TopologicalSpace X
G : Type u_3
inst_1 : Group G
inst_2 : MulAction G X
inst_3 : TopologicalSpace G
inst_4 : ProperSMul G X
U V : Set X
hU : IsCompact U
hV : IsCompact V
g : G
⊢ Membership.mem (γ := Set G) {g : G | (g • U ∩ V).Nonempty} g ↔
    Membership.mem (γ := Set G) (image (α := G × X) fst ((fun (gx : G × X) ↦ (gx.1 • gx.2, gx.2)) ⁻¹' V ×ˢ U)) g
have h : (∃ v ∈ g • U, v ∈ V) ↔ ∃ (u : X), g • u ∈ V ∧ u ∈ U
Tactic: suffices (∃ v, v ∈ g • U ∧ v ∈ V) ↔ ∃ u, g • u ∈ V ∧ u ∈ U by simpa
-- Lean 4 proof step from Mathlib.Topology.Algebra.ProperAction.Basic (goal)
Goal:
X : Type u_2
inst : TopologicalSpace X
G : Type u_3
inst_1 : Group G
inst_2 : MulAction G X
inst_3 : TopologicalSpace G
inst_4 : ProperSMul G X
U V : Set X
hU : IsCompact U
hV : IsCompact V
g : G
⊢ (∃ v ∈ g • U, v ∈ V) ↔ ∃ (u : X), g • u ∈ V ∧ u ∈ U
have h : (∃ (a : X),
    Membership.mem (α := X) (g • U) ((MulAction.toPerm g : (a : X) → X) a : X) ∧
      Membership.mem (α := X) V ((MulAction.toPerm g : (a : X) → X) a : X)) ↔
  ∃ (u : X), g • u ∈ V ∧ u ∈ U
Tactic: rw [← (MulAction.toPerm g).exists_congr_right]
-- Lean 4 proof step from Mathlib.Topology.Algebra.ProperAction.Basic (goal)
Goal:
G : Type u_1
X : Type u_2
inst : Group G
inst_1 : MulAction G X
inst_2 : TopologicalSpace G
inst_3 : TopologicalSpace X
inst_4 : ContinuousSMul G X
inst_5 : IsTopologicalGroup G
inst_6 : IsPretransitive G X
x : X
hx : IsProperMap.{u_1, u_2} (Y := X) fun (g : G) ↦ g • x
⊢ ProperSMul G X
have isProperMap_smul_pair : IsProperMap (Y := X × X) fun (gx : G × X) ↦ (gx.1 • gx.2, gx.2)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Topology.Algebra.ProperAction.Basic (hypothesis)
Goal:
G : Type u_1
X : Type u_2
inst : Group G
inst_1 : MulAction G X
inst_2 : TopologicalSpace G
inst_3 : TopologicalSpace X
inst_4 : ContinuousSMul G X
inst_5 : IsTopologicalGroup G
inst_6 : IsPretransitive G X
x : X
hx : IsProperMap.{u_1, u_2} (Y := X) fun (g : G) ↦ g • x
f : G × G → G × X := Prod.map id fun (g : G) ↦ g • x
⊢ IsProperMap (Y := X × X) fun (gx : G × X) ↦ (gx.1 • gx.2, gx.2)
have hfsurj : Function.Surjective f
Tactic: have hfsurj : f.Surjective := Function.surjective_id.prodMap (surjective_smul G x)
-- Lean 4 proof step from Mathlib.Topology.Algebra.ProperAction.Basic (goal)
Goal:
G : Type u_1
X : Type u_2
inst : Group G
inst_1 : MulAction G X
inst_2 : TopologicalSpace G
inst_3 : TopologicalSpace X
inst_4 : ContinuousSMul G X
inst_5 : IsTopologicalGroup G
inst_6 : IsPretransitive G X
x : X
hx : IsProperMap.{u_1, u_2} (Y := X) fun (g : G) ↦ g • x
f : G × G → G × X := Prod.map id fun (g : G) ↦ g • x
hfsurj : Function.Surjective f
⊢ IsProperMap (Y := X × X) fun (gx : G × X) ↦ (gx.1 • gx.2, gx.2)
have isProperMap_smul_pair : IsProperMap.{u_1, u_2} (Y := X × X) ((fun (gx : G × X) ↦ (gx.1 • gx.2, gx.2)) ∘ f)
Tactic: refine isProperMap_of_comp_of_surj (by fun_prop) (by fun_prop) ?_ hfsurj
-- Lean 4 proof step from Mathlib.Topology.Algebra.ProperAction.CompactlyGenerated (goal)
Goal:
G : Type u_1
X : Type u_2
inst : TopologicalSpace X
inst_1 : Group G
inst_2 : TopologicalSpace G
inst_3 : MulAction G X
inst_4 : CompactlyGeneratedSpace.{u_2} (X × X)
inst_5 : T2Space X
inst_6 : ContinuousSMul G X
⊢ ProperSMul G X ↔ ∀ {U V : Set X}, IsCompact U → IsCompact V → IsCompact.{u_1} (X := G) {g : G | (g • U ∩ V).Nonempty}
have refine : ∀ (h : ∀ {U V : Set X}, IsCompact U → IsCompact V → IsCompact.{u_1} (X := G) {g : G | (g • U ∩ V).Nonempty}),
  IsProperMap (Y := X × X) fun (gx : G × X) ↦ (gx.1 • gx.2, gx.2)
Tactic: refine ⟨fun h ↦ ProperSMul.isCompact_setOf_inter_nonempty, fun h ↦ ⟨?_⟩⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.ProperAction.CompactlyGenerated (goal)
Goal:
G : Type u_1
X : Type u_2
inst : TopologicalSpace X
inst_1 : Group G
inst_2 : TopologicalSpace G
inst_3 : MulAction G X
inst_4 : CompactlyGeneratedSpace.{u_2} (X × X)
inst_5 : T2Space X
inst_6 : ContinuousSMul G X
h : ∀ {U V : Set X}, IsCompact U → IsCompact V → IsCompact.{u_1} (X := G) {g : G | (g • U ∩ V).Nonempty}
⊢ IsProperMap (Y := X × X) fun (gx : G × X) ↦ (gx.1 • gx.2, gx.2)
have refine : ∀ {K : Set (X × X)} (hK : IsCompact K), IsCompact (X := G × X) ((fun (gx : G × X) ↦ (gx.1 • gx.2, gx.2)) ⁻¹' K)
Tactic: refine isProperMap_iff_isCompact_preimage.mpr ⟨by fun_prop, fun {K} hK ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.ProperAction.CompactlyGenerated (hypothesis)
Goal:
G : Type u_1
X : Type u_2
inst : TopologicalSpace X
inst_1 : Group G
inst_2 : TopologicalSpace G
inst_3 : MulAction G X
inst_4 : CompactlyGeneratedSpace.{u_2} (X × X)
inst_5 : T2Space X
inst_6 : ContinuousSMul G X
h : ∀ {U V : Set X}, IsCompact U → IsCompact V → IsCompact.{u_1} (X := G) {g : G | (g • U ∩ V).Nonempty}
K : Set (X × X)
hK : IsCompact K
U : Set X := fst '' K
V : Set X := snd '' K
⊢ IsCompact (X := G × X) ((fun (gx : G × X) ↦ (gx.1 • gx.2, gx.2)) ⁻¹' K)
have hU : IsCompact U
Tactic: have hU : IsCompact U := hK.image continuous_fst
-- Lean 4 proof step from Mathlib.Topology.Algebra.ProperAction.CompactlyGenerated (hypothesis)
Goal:
G : Type u_1
X : Type u_2
inst : TopologicalSpace X
inst_1 : Group G
inst_2 : TopologicalSpace G
inst_3 : MulAction G X
inst_4 : CompactlyGeneratedSpace.{u_2} (X × X)
inst_5 : T2Space X
inst_6 : ContinuousSMul G X
h : ∀ {U V : Set X}, IsCompact U → IsCompact V → IsCompact.{u_1} (X := G) {g : G | (g • U ∩ V).Nonempty}
K : Set (X × X)
hK : IsCompact K
U : Set X := fst '' K
V : Set X := snd '' K
hU : IsCompact U
⊢ IsCompact (X := G × X) ((fun (gx : G × X) ↦ (gx.1 • gx.2, gx.2)) ⁻¹' K)
have hV : IsCompact V
Tactic: have hV : IsCompact V := hK.image continuous_snd
-- Lean 4 proof step from Mathlib.Topology.Algebra.ProperAction.CompactlyGenerated (goal)
Goal:
G : Type u_1
X : Type u_2
inst : TopologicalSpace X
inst_1 : Group G
inst_2 : TopologicalSpace G
inst_3 : MulAction G X
inst_4 : CompactlyGeneratedSpace.{u_2} (X × X)
inst_5 : T2Space X
inst_6 : ContinuousSMul G X
h : ∀ {U V : Set X}, IsCompact U → IsCompact V → IsCompact.{u_1} (X := G) {g : G | (g • U ∩ V).Nonempty}
K : Set (X × X)
hK : IsCompact K
U : Set X := fst '' K
V : Set X := snd '' K
hU : IsCompact U
hV : IsCompact V
this : IsCompact (X := G × X) ((fun (gx : G × X) ↦ (gx.1 • gx.2, gx.2)) ⁻¹' U ×ˢ V)
⊢ IsCompact (X := G × X) ((fun (gx : G × X) ↦ (gx.1 • gx.2, gx.2)) ⁻¹' K)
have apply : Subset (α := Set (G × X)) ((fun (gx : G × X) ↦ (gx.1 • gx.2, gx.2)) ⁻¹' K)
  ((fun (gx : G × X) ↦ (gx.1 • gx.2, gx.2)) ⁻¹' U ×ˢ V)
Tactic: apply this.of_isClosed_subset (hK.isClosed.preimage <| by fun_prop)
-- Lean 4 proof step from Mathlib.Topology.Algebra.ProperAction.CompactlyGenerated (goal)
Goal:
G : Type u_1
X : Type u_2
inst : TopologicalSpace X
inst_1 : Group G
inst_2 : TopologicalSpace G
inst_3 : MulAction G X
inst_4 : CompactlyGeneratedSpace.{u_2} (X × X)
inst_5 : T2Space X
inst_6 : ContinuousSMul G X
h : ∀ {U V : Set X}, IsCompact U → IsCompact V → IsCompact.{u_1} (X := G) {g : G | (g • U ∩ V).Nonempty}
K : Set (X × X)
hK : IsCompact K
U : Set X := fst '' K
V : Set X := snd '' K
hU : IsCompact U
hV : IsCompact V
⊢ IsCompact (X := G × X) ((fun (gx : G × X) ↦ (gx.1 • gx.2, gx.2)) ⁻¹' K)
have suffices : IsCompact (X := G × X) ((fun (gx : G × X) ↦ (gx.1 • gx.2, gx.2)) ⁻¹' U ×ˢ V)
Tactic: suffices IsCompact ((fun (gx : G × X) ↦ (gx.1 • gx.2, gx.2)) ⁻¹' (U ×ˢ V)) by
    apply this.of_isClosed_subset (hK.isClosed.preimage <| by fun_prop)
    exact Set.preimage_mono Set.subset_fst_image_prod_snd_image
-- Lean 4 proof step from Mathlib.Topology.Algebra.ProperAction.CompactlyGenerated (goal)
Goal:
G : Type u_1
X : Type u_2
inst : TopologicalSpace X
inst_1 : Group G
inst_2 : TopologicalSpace G
inst_3 : MulAction G X
inst_4 : CompactlyGeneratedSpace.{u_2} (X × X)
inst_5 : T2Space X
inst_6 : ContinuousSMul G X
h : ∀ {U V : Set X}, IsCompact U → IsCompact V → IsCompact.{u_1} (X := G) {g : G | (g • U ∩ V).Nonempty}
K : Set (X × X)
hK : IsCompact K
U : Set X := fst '' K
V : Set X := snd '' K
hU : IsCompact U
hV : IsCompact V
⊢ IsCompact (X := G × X) ((fun (gx : G × X) ↦ (gx.1 • gx.2, gx.2)) ⁻¹' U ×ˢ V)
have ht : IsClosed (X := G × X) ((fun (gx : G × X) ↦ (gx.1 • gx.2, gx.2)) ⁻¹' U ×ˢ V)
Tactic: apply ((h hV hU).prod hV).of_isClosed_subset
-- Lean 4 proof step from Mathlib.Topology.Algebra.ProperAction.CompactlyGenerated (goal)
Goal:
G : Type u_1
X : Type u_2
inst : TopologicalSpace X
inst_1 : Group G
inst_2 : TopologicalSpace G
inst_3 : MulAction G X
inst_4 : CompactlyGeneratedSpace.{u_2} (X × X)
inst_5 : T2Space X
inst_6 : ContinuousSMul G X
h : ∀ {U V : Set X}, IsCompact U → IsCompact V → IsCompact.{u_1} (X := G) {g : G | (g • U ∩ V).Nonempty}
K : Set (X × X)
hK : IsCompact K
U : Set X := fst '' K
V : Set X := snd '' K
hU : IsCompact U
hV : IsCompact V
ht : IsClosed (X := G × X) ((fun (gx : G × X) ↦ (gx.1 • gx.2, gx.2)) ⁻¹' U ×ˢ V)
⊢ IsCompact (X := G × X) ((fun (gx : G × X) ↦ (gx.1 • gx.2, gx.2)) ⁻¹' U ×ˢ V)
have h₁ : (fun (gx : G × X) ↦ (gx.1 • gx.2, gx.2)) ⁻¹' U ×ˢ V ⊆ SProd.sprod (α := Set G) {g : G | (g • V ∩ U).Nonempty} V
Tactic: apply ((h hV hU).prod hV).of_isClosed_subset
-- Lean 4 proof step from Mathlib.Topology.Algebra.ProperAction.CompactlyGenerated (hypothesis)
Goal:
G : Type u_1
X : Type u_2
inst : TopologicalSpace X
inst_1 : Group G
inst_2 : TopologicalSpace G
inst_3 : MulAction G X
inst_4 : CompactlyGeneratedSpace.{u_2} (X × X)
inst_5 : T2Space X
inst_6 : DiscreteTopology G
inst_7 : ContinuousConstSMul G X
⊢ ProperlyDiscontinuousSMul G X ↔ ProperSMul G X
have this : ContinuousSMul G X
Tactic: have : ContinuousSMul G X := ⟨continuous_prod_of_discrete_left.mpr continuous_const_smul⟩
-- Lean 4 proof step from Mathlib.Topology.Algebra.ProperAction.CompactlyGenerated (goal)
Goal:
G : Type u_1
X : Type u_2
inst : TopologicalSpace X
inst_1 : Group G
inst_2 : TopologicalSpace G
inst_3 : MulAction G X
inst_4 : CompactlyGeneratedSpace.{u_2} (X × X)
inst_5 : T2Space X
inst_6 : DiscreteTopology G
inst_7 : ContinuousConstSMul G X
this : ContinuousSMul G X
⊢ ProperlyDiscontinuousSMul G X ↔ ProperSMul G X
have simp : ProperlyDiscontinuousSMul G X ↔
  ∀ {U V : Set X}, IsCompact U → IsCompact V → Set.Finite.{u_1} (α := G) {g : G | (g • U ∩ V).Nonempty}
Tactic: simp only [MulAction.properSMul_iff_isCompact_setOf_inter_nonempty, isCompact_iff_finite]
-- Lean 4 proof step from Mathlib.Topology.Algebra.ProperAction.CompactlyGenerated (goal)
Goal:
G : Type u_1
X : Type u_2
inst : TopologicalSpace X
inst_1 : Group G
inst_2 : TopologicalSpace G
inst_3 : MulAction G X
inst_4 : CompactlyGeneratedSpace.{u_2} (X × X)
inst_5 : T2Space X
inst_6 : DiscreteTopology G
inst_7 : ContinuousConstSMul G X
this : ContinuousSMul G X
⊢ ProperlyDiscontinuousSMul G X ↔
    ∀ {U V : Set X}, IsCompact U → IsCompact V → Set.Finite.{u_1} (α := G) {g : G | (g • U ∩ V).Nonempty}
have rw : (∀ {K L : Set X}, IsCompact K → IsCompact L → Set.Finite.{u_1} (α := G) {m : G | (m • K ∩ L).Nonempty}) ↔
  ∀ {U V : Set X}, IsCompact U → IsCompact V → Set.Finite.{u_1} (α := G) {g : G | (g • U ∩ V).Nonempty}
Tactic: rw [properlyDiscontinuousSMul_iff]
-- Lean 4 proof step from Mathlib.Topology.Algebra.RestrictedProduct.Basic (goal)
Goal:
ι : Type u_1
R : ι → Type u_2
A : (i : ι) → Set (R i)
𝓕 𝓖 : Filter ι
ι₁ : Type u_3
ι₂ : Type u_4
R₁ : ι₁ → Type u_5
R₂ : ι₂ → Type u_6
𝓕₁ : Filter ι₁
𝓕₂ : Filter ι₂
A₁ : (i : ι₁) → Set (R₁ i)
A₂ : (i : ι₂) → Set (R₂ i)
S₁ : ι₁ → Type u_7
S₂ : ι₂ → Type u_8
inst : (i : ι₁) → SetLike.{u_7, u_5} (S₁ i) (R₁ i)
inst_1 : (j : ι₂) → SetLike.{u_8, u_6} (S₂ j) (R₂ j)
B₁ : (i : ι₁) → S₁ i
B₂ : (j : ι₂) → S₂ j
f : ι₂ → ι₁
hf : Tendsto f 𝓕₂ 𝓕₁
φ : (j : ι₂) → R₁ (f j) → R₂ j
hφ : ∀ᶠ (j : ι₂) in 𝓕₂, MapsTo (φ j) (A₁ (f j)) (A₂ j)
x : Πʳ (i : ι₁), [R₁ i, A₁ i]_[𝓕₁]
⊢ ∀ᶠ (i : ι₂) in 𝓕₂,
    Membership.mem (γ := Set ((fun (j : ι₂) ↦ R₂ j) i)) ((fun (j : ι₂) ↦ A₂ j) i)
      ((fun (j : ι₂) ↦ φ j ((x : (a : ι₁) → R₁ a) (f j))) i)
have h : ∀ (a : ι₂),
  Membership.mem (γ := Set ι₂)
    {x_1 : ι₂ |
      Membership.mem (γ := Set ι₂)
          {x_2 : ι₂ |
            (fun (x_3 : ι₂) ↦
                Membership.mem (γ := Set ((fun (i : ι₁) ↦ R₁ i) (f x_3))) ((fun (i : ι₁) ↦ A₁ i) (f x_3))
                  ((↑x : (i : ι₁) → (fun (i : ι₁) ↦ R₁ i) i) (f x_3)))
              x_2}
          x_1 →
        Membership.mem (γ := Set ι₂)
          {x_2 : ι₂ |
            Membership.mem (γ := Set ι₂) {x : ι₂ | (fun (j : ι₂) ↦ MapsTo (φ j) (A₁ (f j)) (A₂ j)) x} x_2 →
              Membership.mem (γ := Set ι₂)
                {x_3 : ι₂ |
                  (fun (i : ι₂) ↦
                      Membership.mem (γ := Set ((fun (j : ι₂) ↦ R₂ j) i)) ((fun (j : ι₂) ↦ A₂ j) i)
                        ((fun (j : ι₂) ↦ φ j ((x : (a : ι₁) → R₁ a) (f j))) i))
                    x_3}
                x_2}
          x_1}
    a
Tactic: filter_upwards [hf.eventually x.2, hφ] using fun _ h1 h2 ↦ h2 h1
-- Lean 4 proof step from Mathlib.Topology.Algebra.RestrictedProduct.Basic (goal)
Goal:
ι : Type u_1
R : ι → Type u_2
A : (i : ι) → Set (R i)
𝓕 𝓖 : Filter ι
ι₁ : Type u_3
ι₂ : Type u_4
R₁ : ι₁ → Type u_5
R₂ : ι₂ → Type u_6
𝓕₁ : Filter ι₁
𝓕₂ : Filter ι₂
A₁ : (i : ι₁) → Set (R₁ i)
A₂ : (i : ι₂) → Set (R₂ i)
S₁ : ι₁ → Type u_7
S₂ : ι₂ → Type u_8
inst : (i : ι₁) → SetLike.{u_7, u_5} (S₁ i) (R₁ i)
inst_1 : (j : ι₂) → SetLike.{u_8, u_6} (S₂ j) (R₂ j)
B₁ : (i : ι₁) → S₁ i
B₂ : (j : ι₂) → S₂ j
f : ι₂ → ι₁
hf : Tendsto f 𝓕₂ 𝓕₁
φ : (j : ι₂) → R₁ (f j) → R₂ j
hφ : ∀ᶠ (j : ι₂) in 𝓕₂, MapsTo (φ j) (A₁ (f j)) (A₂ j)
x : Πʳ (i : ι₁), [R₁ i, A₁ i]_[𝓕₁]
h :
  ∀ (a : ι₂),
    Membership.mem (γ := Set ι₂)
      {x_1 : ι₂ |
        Membership.mem (γ := Set ι₂)
            {x_2 : ι₂ |
              (fun (x_3 : ι₂) ↦
                  Membership.mem (γ := Set ((fun (i : ι₁) ↦ R₁ i) (f x_3))) ((fun (i : ι₁) ↦ A₁ i) (f x_3))
                    ((↑x : (i : ι₁) → (fun (i : ι₁) ↦ R₁ i) i) (f x_3)))
                x_2}
            x_1 →
          Membership.mem (γ := Set ι₂)
            {x_2 : ι₂ |
              Membership.mem (γ := Set ι₂) {x : ι₂ | (fun (j : ι₂) ↦ MapsTo (φ j) (A₁ (f j)) (A₂ j)) x} x_2 →
                Membership.mem (γ := Set ι₂)
                  {x_3 : ι₂ |
                    (fun (i : ι₂) ↦
                        Membership.mem (γ := Set ((fun (j : ι₂) ↦ R₂ j) i)) ((fun (j : ι₂) ↦ A₂ j) i)
                          ((fun (j : ι₂) ↦ φ j ((x : (a : ι₁) → R₁ a) (f j))) i))
                      x_3}
                  x_2}
            x_1}
      a
⊢ ∀ᶠ (i : ι₂) in 𝓕₂,
    Membership.mem (γ := Set ((fun (j : ι₂) ↦ R₂ j) i)) ((fun (j : ι₂) ↦ A₂ j) i)
      ((fun (j : ι₂) ↦ φ j ((x : (a : ι₁) → R₁ a) (f j))) i)
have h₁ : ∀ (a : ι₂),
  Membership.mem (γ := Set (R₁ (f a))) (A₁ (f a)) ((↑x : (i : ι₁) → R₁ i) (f a)) →
    MapsTo (φ a) (A₁ (f a)) (A₂ a) → φ a ((x : (a : ι₁) → R₁ a) (f a)) ∈ A₂ a
Tactic: filter_upwards [hf.eventually x.2, hφ] using fun _ h1 h2 ↦ h2 h1
-- Lean 4 proof step from Mathlib.Topology.Algebra.RestrictedProduct.Basic (goal)
Goal:
ι : Type u_1
R : ι → Type u_2
A : (i : ι) → Set (R i)
𝓕 𝓖 : Filter ι
ι₁ : Type u_3
ι₂ : Type u_4
R₁ : ι₁ → Type u_5
R₂ : ι₂ → Type u_6
𝓕₁ : Filter ι₁
𝓕₂ : Filter ι₂
A₁ : (i : ι₁) → Set (R₁ i)
A₂ : (i : ι₂) → Set (R₂ i)
S₁ : ι₁ → Type u_7
S₂ : ι₂ → Type u_8
inst : (i : ι₁) → SetLike.{u_7, u_5} (S₁ i) (R₁ i)
inst_1 : (j : ι₂) → SetLike.{u_8, u_6} (S₂ j) (R₂ j)
B₁ : (i : ι₁) → S₁ i
B₂ : (j : ι₂) → S₂ j
f : ι₂ → ι₁
hf : Tendsto f 𝓕₂ 𝓕₁
inst_2 : (i : ι₁) → Monoid (R₁ i)
inst_3 : (i : ι₂) → Monoid (R₂ i)
inst_4 : ∀ (i : ι₁), SubmonoidClass.{u_7, u_5} (S₁ i) (R₁ i)
inst_5 : ∀ (i : ι₂), SubmonoidClass.{u_8, u_6} (S₂ i) (R₂ i)
φ : (j : ι₂) → MonoidHom.{u_5, u_6} (R₁ (f j)) (R₂ j)
hφ : ∀ᶠ (j : ι₂) in 𝓕₂, MapsTo (⇑(φ j) : (a : R₁ (f j)) → R₂ j) (↑(B₁ (f j)) : Set (R₁ (f j))) (↑(B₂ j) : Set (R₂ j))
⊢ Eq (α := Πʳ (j : ι₂), [R₂ j, (↑(B₂ j) : Set ((fun (j : ι₂) ↦ R₂ j) j))]_[𝓕₂])
    (mapAlong R₁ R₂ (A₁ := fun (i : ι₁) ↦ (↑(B₁ i) : Set ((fun (i : ι₁) ↦ R₁ i) i))) (A₂ := fun (j : ι₂) ↦
      (↑(B₂ j) : Set ((fun (j : ι₂) ↦ R₂ j) j))) f hf (fun (j : ι₂) (r : R₁ (f j)) ↦ (φ j : (a : R₁ (f j)) → R₂ j) r) hφ
      1)
    1
have h : ∀ (i : ι₂),
  (mapAlong R₁ R₂ (A₁ := fun (i : ι₁) ↦ (↑(B₁ i) : Set ((fun (i : ι₁) ↦ R₁ i) i))) (A₂ := fun (j : ι₂) ↦
          (↑(B₂ j) : Set ((fun (j : ι₂) ↦ R₂ j) j))) f hf
          (fun (j : ι₂) (r : R₁ (f j)) ↦ (φ j : (a : R₁ (f j)) → R₂ j) r) hφ 1 :
        (a : ι₂) → R₂ a)
      i =
    (1 : (a : ι₂) → R₂ a) i
Tactic: ext i
-- Lean 4 proof step from Mathlib.Topology.Algebra.RestrictedProduct.Basic (goal)
Goal:
ι : Type u_1
R : ι → Type u_2
A : (i : ι) → Set (R i)
𝓕 𝓖 : Filter ι
ι₁ : Type u_3
ι₂ : Type u_4
R₁ : ι₁ → Type u_5
R₂ : ι₂ → Type u_6
𝓕₁ : Filter ι₁
𝓕₂ : Filter ι₂
A₁ : (i : ι₁) → Set (R₁ i)
A₂ : (i : ι₂) → Set (R₂ i)
S₁ : ι₁ → Type u_7
S₂ : ι₂ → Type u_8
inst : (i : ι₁) → SetLike.{u_7, u_5} (S₁ i) (R₁ i)
inst_1 : (j : ι₂) → SetLike.{u_8, u_6} (S₂ j) (R₂ j)
B₁ : (i : ι₁) → S₁ i
B₂ : (j : ι₂) → S₂ j
f : ι₂ → ι₁
hf : Tendsto f 𝓕₂ 𝓕₁
inst_2 : (i : ι₁) → Monoid (R₁ i)
inst_3 : (i : ι₂) → Monoid (R₂ i)
inst_4 : ∀ (i : ι₁), SubmonoidClass.{u_7, u_5} (S₁ i) (R₁ i)
inst_5 : ∀ (i : ι₂), SubmonoidClass.{u_8, u_6} (S₂ i) (R₂ i)
φ : (j : ι₂) → MonoidHom.{u_5, u_6} (R₁ (f j)) (R₂ j)
hφ : ∀ᶠ (j : ι₂) in 𝓕₂, MapsTo (⇑(φ j) : (a : R₁ (f j)) → R₂ j) (↑(B₁ (f j)) : Set (R₁ (f j))) (↑(B₂ j) : Set (R₂ j))
x y : Πʳ (i : ι₁), [R₁ i, (↑(B₁ i) : Set ((fun (i : ι₁) ↦ R₁ i) i))]_[𝓕₁]
⊢ mapAlong R₁ R₂ (A₁ := fun (i : ι₁) ↦ (↑(B₁ i) : Set ((fun (i : ι₁) ↦ R₁ i) i))) (A₂ := fun (j : ι₂) ↦
      (↑(B₂ j) : Set ((fun (j : ι₂) ↦ R₂ j) j))) f hf (fun (j : ι₂) (r : R₁ (f j)) ↦ (φ j : (a : R₁ (f j)) → R₂ j) r) hφ
      (x * y) =
    HMul.hMul (α := Πʳ (j : ι₂), [R₂ j, (↑(B₂ j) : Set ((fun (j : ι₂) ↦ R₂ j) j))]_[𝓕₂])
      (mapAlong R₁ R₂ (A₁ := fun (i : ι₁) ↦ (↑(B₁ i) : Set ((fun (i : ι₁) ↦ R₁ i) i))) (A₂ := fun (j : ι₂) ↦
        (↑(B₂ j) : Set ((fun (j : ι₂) ↦ R₂ j) j))) f hf (fun (j : ι₂) (r : R₁ (f j)) ↦ (φ j : (a : R₁ (f j)) → R₂ j) r)
        hφ x)
      (mapAlong R₁ R₂ (A₁ := fun (i : ι₁) ↦ (↑(B₁ i) : Set ((fun (i : ι₁) ↦ R₁ i) i))) (A₂ := fun (j : ι₂) ↦
        (↑(B₂ j) : Set ((fun (j : ι₂) ↦ R₂ j) j))) f hf (fun (j : ι₂) (r : R₁ (f j)) ↦ (φ j : (a : R₁ (f j)) → R₂ j) r)
        hφ y)
have h : ∀ (i : ι₂),
  (mapAlong R₁ R₂ (A₁ := fun (i : ι₁) ↦ (↑(B₁ i) : Set ((fun (i : ι₁) ↦ R₁ i) i))) (A₂ := fun (j : ι₂) ↦
          (↑(B₂ j) : Set ((fun (j : ι₂) ↦ R₂ j) j))) f hf
          (fun (j : ι₂) (r : R₁ (f j)) ↦ (φ j : (a : R₁ (f j)) → R₂ j) r) hφ (x * y) :
        (a : ι₂) → R₂ a)
      i =
    (HMul.hMul (α := Πʳ (j : ι₂), [R₂ j, (↑(B₂ j) : Set ((fun (j : ι₂) ↦ R₂ j) j))]_[𝓕₂])
          (mapAlong R₁ R₂ (A₁ := fun (i : ι₁) ↦ (↑(B₁ i) : Set ((fun (i : ι₁) ↦ R₁ i) i))) (A₂ := fun (j : ι₂) ↦
            (↑(B₂ j) : Set ((fun (j : ι₂) ↦ R₂ j) j))) f hf
            (fun (j : ι₂) (r : R₁ (f j)) ↦ (φ j : (a : R₁ (f j)) → R₂ j) r) hφ x)
          (mapAlong R₁ R₂ (A₁ := fun (i : ι₁) ↦ (↑(B₁ i) : Set ((fun (i : ι₁) ↦ R₁ i) i))) (A₂ := fun (j : ι₂) ↦
            (↑(B₂ j) : Set ((fun (j : ι₂) ↦ R₂ j) j))) f hf
            (fun (j : ι₂) (r : R₁ (f j)) ↦ (φ j : (a : R₁ (f j)) → R₂ j) r) hφ y) :
        (a : ι₂) → R₂ a)
      i
Tactic: ext i
-- Lean 4 proof step from Mathlib.Topology.Algebra.RestrictedProduct.Basic (goal)
Goal:
ι : Type u_1
R : ι → Type u_2
A_1 : (i : ι) → Set (R i)
𝓕 𝓖 : Filter ι
S : ι → Type u_3
G : ι → Type u_4
inst : (i : ι) → SetLike.{u_3, u_4} (S i) (G i)
A : (i : ι) → S i
inst_1 : DecidableEq ι
inst_2 : (i : ι) → One (G i)
inst_3 : ∀ (i : ι), OneMemClass.{u_3, u_4} (S i) (G i)
i : ι
x : G i
⊢ ∀ᶠ (i_1 : ι) in cofinite,
    Membership.mem (γ := Set ((fun (i : ι) ↦ G i) i_1)) ((fun (i : ι) ↦ (↑(A i) : Set ((fun (i : ι) ↦ G i) i))) i_1)
      (Pi.mulSingle (M := fun (i : ι) ↦ G i) i x i_1)
have h : ∀ (a : ι), Membership.mem (γ := Set ι) {i}ᶜ a → Pi.mulSingle (M := fun (i : ι) ↦ G i) i x a ∈ (↑(A a) : Set (G a))
Tactic: filter_upwards [show {i}ᶜ ∈ Filter.cofinite by simp]
-- Lean 4 proof step from Mathlib.Topology.Algebra.RestrictedProduct.Basic (goal)
Goal:
ι : Type u_1
S : ι → Type u_3
G : ι → Type u_4
inst : (i : ι) → SetLike.{u_3, u_4} (S i) (G i)
A : (i : ι) → S i
inst_1 : DecidableEq ι
inst_2 : (i : ι) → One (G i)
inst_3 : ∀ (i : ι), OneMemClass.{u_3, u_4} (S i) (G i)
i : ι
⊢ Function.comp (β := Πʳ (i : ι), [G i, (↑(A i) : Set ((fun (i : ι) ↦ G i) i))]) (DFunLike.coe (β := G))
      (mulSingle (S := S) (G := G) A i) =
    Pi.mulSingle (M := G) i
have h : ∀ (x : G i) (x_1 : ι),
  Function.comp (β := Πʳ (i : ι), [G i, (↑(A i) : Set ((fun (i : ι) ↦ G i) i))]) (DFunLike.coe (β := G))
      (mulSingle (S := S) (G := G) A i) x x_1 =
    Pi.mulSingle (M := G) i x x_1
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.Algebra.RestrictedProduct.Basic (goal)
Goal:
ι : Type u_1
S : ι → Type u_3
G : ι → Type u_4
inst : (i : ι) → SetLike.{u_3, u_4} (S i) (G i)
A : (i : ι) → S i
inst_1 : DecidableEq ι
inst_2 : (i : ι) → One (G i)
inst_3 : ∀ (i : ι), OneMemClass.{u_3, u_4} (S i) (G i)
i : ι
⊢ Eq (α := Πʳ (i : ι), [G i, (↑(A i) : Set ((fun (i : ι) ↦ G i) i))]) (mulSingle (S := S) (G := G) A i 1) 1
have h : ∀ (i_1 : ι), (mulSingle (S := S) (G := G) A i 1 : (a : ι) → G a) i_1 = (1 : (a : ι) → G a) i_1
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.Algebra.RestrictedProduct.Basic (goal)
Goal:
ι : Type u_1
S : ι → Type u_3
G : ι → Type u_4
inst : (i : ι) → SetLike.{u_3, u_4} (S i) (G i)
A : (i : ι) → S i
inst_1 : DecidableEq ι
inst_2 : (i : ι) → MulOneClass (G i)
inst_3 : ∀ (i : ι), OneMemClass.{u_3, u_4} (S i) (G i)
inst_4 : ∀ (i : ι), MulMemClass.{u_3, u_4} (S i) (G i)
i : ι
r s : G i
⊢ mulSingle (S := S) (G := G) A i (r * s) =
    HMul.hMul (α := Πʳ (i : ι), [G i, (↑(A i) : Set ((fun (i : ι) ↦ G i) i))]) (mulSingle (S := S) (G := G) A i r)
      (mulSingle (S := S) (G := G) A i s)
have h : ∀ (i_1 : ι),
  (mulSingle (S := S) (G := G) A i (r * s) : (a : ι) → G a) i_1 =
    (HMul.hMul (α := Πʳ (i : ι), [G i, (↑(A i) : Set ((fun (i : ι) ↦ G i) i))]) (mulSingle (S := S) (G := G) A i r)
          (mulSingle (S := S) (G := G) A i s) :
        (a : ι) → G a)
      i_1
Tactic: ext