awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Algebra.ProperAction.CompactlyGenerated
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
rw 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}
⊢ ProperlyDiscontinuousSMul G X ↔
    ∀ {U V : Set X}, IsCompact U → IsCompact V → Set.Finite.{u_1} (α := G) {g : G | (g • U ∩ V).Nonempty}

Tactic:
rw [properlyDiscontinuousSMul_iff]

Premises used: properlyDiscontinuousSMul_iff
-- Module: Mathlib.Topology.Algebra.ProperConstSMul
Goal:
M : Type u_1
c : M
X : Type u_2
inst : SMul M X
inst_1 : TopologicalSpace X
h : ProperConstSMul M X
⊢ IsProperMap (Y := X) fun (x : X) ↦ c • x

Tactic:
h.1 c

Premises used: ProperConstSMul.isProperMap_smul
-- Module: Mathlib.Topology.Algebra.ProperConstSMul
Goal:
M : Type u_1
X : Type u_2
inst : SMul M X
inst_1 : TopologicalSpace X
inst_2 : ProperConstSMul M X
s : Set X
hs : IsCompact s
c : M
⊢ IsCompact (X := X) ((fun (x : X) ↦ c • x) ⁻¹' s)

Tactic:
(isProperMap_smul c X).isCompact_preimage hs

Premises used: IsProperMap.isCompact_preimage, isProperMap_smul
-- Module: Mathlib.Topology.Algebra.ProperConstSMul
Goal:
M : Type u_1
X : Type u_2
inst : SMul M X
inst_1 : TopologicalSpace X
inst_2 : ContinuousConstSMul M X
inst_3 : T2Space X
inst_4 : CompactSpace X
⊢ ProperConstSMul M X

Tactic:
⟨fun c ↦ (continuous_const_smul c).isProperMap⟩

Premises used: ContinuousConstSMul.continuous_const_smul, ProperConstSMul.mk, Continuous.isProperMap
-- Module: Mathlib.Topology.Algebra.ProperConstSMul
Goal:
G : Type u_1
X : Type u_2
inst : Group G
inst_1 : MulAction G X
inst_2 : TopologicalSpace X
inst_3 : ContinuousConstSMul G X
⊢ ProperConstSMul G X

Tactic:
⟨fun c ↦ (Homeomorph.smul c).isProperMap⟩

Premises used: ProperConstSMul.mk, Homeomorph.isProperMap, Homeomorph.smul
-- Module: Mathlib.Topology.Algebra.ProperConstSMul
Goal:
M : Type u_1
X : Type u_2
Y : Type u_3
inst : SMul M X
inst_1 : TopologicalSpace X
inst_2 : ProperConstSMul M X
inst_3 : SMul M Y
inst_4 : TopologicalSpace Y
inst_5 : ProperConstSMul M Y
⊢ ProperConstSMul M (X × Y)

Tactic:
⟨fun c ↦ (isProperMap_smul c X).prodMap (isProperMap_smul c Y)⟩

Premises used: ProperConstSMul.mk, isProperMap_smul, IsProperMap.prodMap
-- Module: Mathlib.Topology.Algebra.ProperConstSMul
Goal:
M : Type u_1
ι : Type u_2
X : ι → Type u_3
inst : (i : ι) → SMul.{u_1, u_3} M (X i)
inst_1 : (i : ι) → TopologicalSpace (X i)
inst_2 : ∀ (i : ι), ProperConstSMul.{u_1, u_3} M (X i)
⊢ ProperConstSMul M ((i : ι) → X i)

Tactic:
⟨fun c ↦ .pi_map fun i ↦ isProperMap_smul c (X i)⟩

Premises used: IsProperMap.pi_map, ProperConstSMul.mk, isProperMap_smul
-- Module: Mathlib.Topology.Algebra.RestrictedProduct.Basic
Goal:
ι : Type u_1
R : ι → Type u_2
A : (i : ι) → Set (R i)
𝓕 : Filter ι
x : (i : ι) → R i
hx : ∀ᶠ (i : ι) in 𝓕, x i ∈ A i
i : ι
⊢ (mk (R := R) (A := A) x hx : (a : ι) → R a) i = x i

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.RestrictedProduct.Basic
Goal:
ι : Type u_1
R : ι → Type u_2
A : (i : ι) → Set (R i)
𝓕 : Filter ι
x y : Πʳ (i : ι), [R i, A i]_[𝓕]
h : ∀ (i : ι), (x : (a : ι) → R a) i = (y : (a : ι) → R a) i
⊢ x = y

Tactic:
Subtype.ext <| funext h

Premises used: RestrictedProduct, funext, Subtype.ext
-- Module: Mathlib.Topology.Algebra.RestrictedProduct.Basic
Goal:
ι : Type u_1
R : ι → Type u_2
A : (i : ι) → Set (R i)
𝓕 : Filter ι
⊢ range (ι := Πʳ (i : ι), [R i, A i]_[𝓕]) (DFunLike.coe (β := R)) = {x : (a : ι) → R a | ∀ᶠ (i : ι) in 𝓕, x i ∈ A i}

Tactic:
Subtype.range_val_subtype

Premises used: Set.Mem, setOf, RestrictedProduct, Subtype.range_val_subtype
-- Module: Mathlib.Topology.Algebra.RestrictedProduct.Basic
Goal:
ι : Type u_1
R : ι → Type u_2
A : (i : ι) → Set (R i)
S : Set ι
⊢ range (ι := Πʳ (i : ι), [R i, A i]_[𝓟 S]) (DFunLike.coe (β := R)) = S.pi (α := R) A

Tactic:
range_coe R A

Premises used: Set.Mem, Filter.Eventually, setOf, Set.Subset, RestrictedProduct.range_coe, Set.pi
-- Module: Mathlib.Topology.Algebra.RestrictedProduct.Basic
Goal:
ι : Type u_1
R : ι → Type u_2
A : (i : ι) → Set (R i)
𝓕 : Filter ι
x : Πʳ (i : ι), [R i, A i]_[𝓕]
⊢ ∀ᶠ (i : ι) in 𝓕, (x : (a : ι) → R a) i ∈ A i

Tactic:
x.2

Premises used: Set.Mem, Subtype.property
-- Module: Mathlib.Topology.Algebra.RestrictedProduct.Basic
Goal:
ι : Type u_1
R : ι → Type u_2
A : (i : ι) → Set (R i)
𝓕 : Filter ι
x : (i : ι) → (↑(A i) : Type u_2)
i : ι
⊢ (structureMap R A 𝓕 x : (a : ι) → R a) i = (↑(x i) : R i)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.RestrictedProduct.Basic
Goal:
ι : Type u_1
R : ι → Type u_2
A : (i : ι) → Set (R i)
𝓕 𝓖 : Filter ι
h : 𝓕 ≤ 𝓖
x : Πʳ (i : ι), [R i, A i]_[𝓖]
i : ι
⊢ (inclusion R A h x : (a : ι) → R a) i = (x : (a : ι) → R a) i

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.RestrictedProduct.Basic
Goal:
ι : Type u_1
R : ι → Type u_2
A : (i : ι) → Set (R i)
𝓕 : Filter ι
⊢ inclusion R A ⋯ = id

Tactic:
rfl

Premises used: RestrictedProduct.inclusion, RestrictedProduct, rfl
-- Module: Mathlib.Topology.Algebra.RestrictedProduct.Basic
Goal:
ι : Type u_1
R : ι → Type u_2
A : (i : ι) → Set (R i)
𝓕 𝓖 : Filter ι
h : 𝓕 ≤ 𝓖
x : Πʳ (i : ι), [R i, A i]_[𝓕]
hx𝓖 : ∀ᶠ (i : ι) in 𝓖, (x : (a : ι) → R a) i ∈ A i
⊢ ∃ (x' : Πʳ (i : ι), [R i, A i]_[𝓖]), inclusion R A h x' = x

Tactic:
⟨⟨x.1, hx𝓖⟩, rfl⟩

Premises used: Subtype.mk, Exists.intro, Subtype.val, rfl
-- Module: Mathlib.Topology.Algebra.RestrictedProduct.Basic
Goal:
ι : Type u_1
R : ι → Type u_2
A : (i : ι) → Set (R i)
𝓕 : Filter ι
x : Πʳ (i : ι), [R i, A i]_[𝓕]
hx : ∀ (i : ι), (↑x : (i : ι) → (fun (i : ι) ↦ R i) i) i ∈ A i
⊢ ∃ (x' : (i : ι) → (↑(A i) : Type u_2)), structureMap R A 𝓕 x' = x

Tactic:
⟨fun i ↦ ⟨x i, hx i⟩, rfl⟩

Premises used: Subtype.mk, Exists.intro, DFunLike.coe, rfl
-- Module: Mathlib.Topology.Algebra.RestrictedProduct.Basic
Goal:
ι : Type u_1
R : ι → Type u_2
A : (i : ι) → Set (R i)
𝓕 𝓖 : Filter ι
h : 𝓕 ≤ 𝓖
⊢ range (inclusion R A h) = {x : Πʳ (i : ι), [R i, A i]_[𝓕] | ∀ᶠ (i : ι) in 𝓖, (x : (a : ι) → R a) i ∈ A i}

Tactic:
subset_antisymm (range_subset_iff.mpr fun x ↦ x.2)
    (fun _ hx ↦ mem_range.mpr <| exists_inclusion_eq_of_eventually R A h hx)

Premises used: Iff.mpr, Set.mem_range, subset_antisymm, RestrictedProduct.exists_inclusion_eq_of_eventually, Set.range_subset_iff, Subtype.property
-- Module: Mathlib.Topology.Algebra.RestrictedProduct.Basic
Goal:
ι : Type u_1
R : ι → Type u_2
A : (i : ι) → Set (R i)
𝓕 𝓖 : Filter ι
h : 𝓕 ≤ 𝓖
⊢ DFunLike.coe (β := R) ∘ inclusion R A h = DFunLike.coe (β := R)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.RestrictedProduct.Basic
Goal:
ι : Type u_1
R : ι → Type u_2
A : (i : ι) → Set (R i)
𝓕 𝓖 : Filter ι
h : 𝓕 ≤ 𝓖
U : Set Πʳ (i : ι), [R i, A i]_[𝓕]
⊢ DFunLike.coe (β := R) '' inclusion R A h ⁻¹' U ⊆ DFunLike.coe (β := R) '' U

Tactic:
fun _ ⟨x, hx, hx'⟩ ↦ ⟨inclusion R A h x, hx, hx'⟩

Premises used: RestrictedProduct.inclusion, Membership.mem, Set.Subset, And.intro, Exists.intro, Set.image, DFunLike.coe, _private.0.RestrictedProduct.image_coe_preimage_inclusion_subset.match_1
-- Module: Mathlib.Topology.Algebra.RestrictedProduct.Basic
Goal:
ι : Type u_1
R : ι → Type u_2
A : (i : ι) → Set (R i)
𝓕 : Filter ι
⊢ range (structureMap R A 𝓕) =
    {f : Πʳ (i : ι), [R i, A i]_[𝓕] | ∀ (i : ι), (↑f : (i : ι) → (fun (i : ι) ↦ R i) i) i ∈ A i}

Tactic:
subset_antisymm (range_subset_iff.mpr fun x i ↦ (x i).2)
    (fun _ hx ↦ mem_range.mpr <| exists_structureMap_eq_of_forall R A hx)

Premises used: Iff.mpr, Set.mem_range, subset_antisymm, RestrictedProduct.exists_structureMap_eq_of_forall, Set.range_subset_iff, Subtype.property
-- Module: Mathlib.Topology.Algebra.RestrictedProduct.Basic
Goal:
ι : Type u_1
R : ι → Type u_2
A : (i : ι) → Set (R i)
𝓕 : Filter ι
⊢ DFunLike.coe (β := R) ∘ structureMap R A 𝓕 = fun (x : (i : ι) → (↑(A i) : Type u_2)) (i : ι) ↦ (↑(x i) : R i)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.RestrictedProduct.Basic
Goal:
ι : Type u_1
R : ι → Type u_2
𝓕 : Filter ι
S : ι → Type u_3
inst : (i : ι) → SetLike.{u_3, u_2} (S i) (R i)
B : (i : ι) → S i
inst_1 : (i : ι) → One (R i)
inst_2 : ∀ (i : ι), OneMemClass.{u_3, u_2} (S i) (R i)
i : ι
⊢ (1 : (a : ι) → R a) i = 1

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.RestrictedProduct.Basic
Goal:
ι : Type u_1
R : ι → Type u_2
𝓕 : Filter ι
S : ι → Type u_3
inst : (i : ι) → SetLike.{u_3, u_2} (S i) (R i)
B : (i : ι) → S i
inst_1 : (i : ι) → Inv (R i)
inst_2 : ∀ (i : ι), InvMemClass.{u_3, u_2} (S i) (R i)
x : Πʳ (i : ι), [R i, (↑(B i) : Set ((fun (i : ι) ↦ R i) i))]_[𝓕]
i : ι
⊢ (x⁻¹ : (a : ι) → R a) i = ((x : (a : ι) → R a) i)⁻¹

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.RestrictedProduct.Basic
Goal:
ι : Type u_1
R : ι → Type u_2
𝓕 : Filter ι
S : ι → Type u_3
inst : (i : ι) → SetLike.{u_3, u_2} (S i) (R i)
B : (i : ι) → S i
inst_1 : (i : ι) → Mul (R i)
inst_2 : ∀ (i : ι), MulMemClass.{u_3, u_2} (S i) (R i)
x y : Πʳ (i : ι), [R i, (↑(B i) : Set ((fun (i : ι) ↦ R i) i))]_[𝓕]
i : ι
⊢ (x * y : (a : ι) → R a) i = (x : (a : ι) → R a) i * (y : (a : ι) → R a) i

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.RestrictedProduct.Basic
Goal:
ι : Type u_1
R : ι → Type u_2
𝓕 : Filter ι
S : ι → Type u_3
inst : (i : ι) → SetLike.{u_3, u_2} (S i) (R i)
B : (i : ι) → S i
G : Type u_4
inst_1 : (i : ι) → SMul.{u_4, u_2} G (R i)
inst_2 : ∀ (i : ι), SMulMemClass.{u_3, u_4, u_2} (S i) G (R i)
g : G
x : Πʳ (i : ι), [R i, (↑(B i) : Set ((fun (i : ι) ↦ R i) i))]_[𝓕]
i : ι
⊢ (g • x : (a : ι) → R a) i = g • (x : (a : ι) → R a) i

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.RestrictedProduct.Basic
Goal:
ι : Type u_1
R : ι → Type u_2
𝓕 : Filter ι
S : ι → Type u_3
inst : (i : ι) → SetLike.{u_3, u_2} (S i) (R i)
B : (i : ι) → S i
inst_1 : (i : ι) → DivInvMonoid (R i)
inst_2 : ∀ (i : ι), SubgroupClass.{u_3, u_2} (S i) (R i)
x y : Πʳ (i : ι), [R i, (↑(B i) : Set ((fun (i : ι) ↦ R i) i))]_[𝓕]
i : ι
⊢ (x / y : (a : ι) → R a) i = (x : (a : ι) → R a) i / (y : (a : ι) → R a) i

Tactic:
rfl

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

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.RestrictedProduct.Basic
Goal:
ι : Type u_1
R : ι → Type u_2
𝓕 : Filter ι
S : ι → Type u_3
inst : (i : ι) → SetLike.{u_3, u_2} (S i) (R i)
B : (i : ι) → S i
inst_1 : (i : ι) → DivInvMonoid (R i)
inst_2 : ∀ (i : ι), SubgroupClass.{u_3, u_2} (S i) (R i)
x : Πʳ (i : ι), [R i, (↑(B i) : Set ((fun (i : ι) ↦ R i) i))]_[𝓕]
n : ℤ
i : ι
⊢ (x ^ n : (a : ι) → R a) i = (x : (a : ι) → R a) i ^ n

Tactic:
rfl

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

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.RestrictedProduct.Basic
Goal:
ι : Type u_1
R : ι → Type u_2
𝓕 : Filter ι
S : ι → Type u_3
inst : (i : ι) → SetLike.{u_3, u_2} (S i) (R i)
B : (i : ι) → S i
inst_1 : (i : ι) → Ring (R i)
inst_2 : ∀ (i : ι), SubringClass.{u_2, u_3} (S i) (R i)
x : Πʳ (i : ι), [R i, (↑(B i) : Set ((fun (i : ι) ↦ R i) i))]_[𝓕]
j : ι
⊢ (evalRingHom R (S := S) j : (a : Πʳ (i : ι), [R i, (↑(B i) : Set ((fun (i : ι) ↦ R i) i))]_[𝓕]) → R j) x =
    (x : (a : ι) → R a) j

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.RestrictedProduct.Basic
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]_[𝓕₁]
⊢ ∀ (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:
fun _ h1 h2 ↦ h2 h1

Premises used: Set.Mem
-- Module: Mathlib.Topology.Algebra.RestrictedProduct.Basic
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
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
⊢ ∀ᶠ (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)

Tactic:
filter_upwards [hf.eventually x.2, hφ] using fun _ h1 h2 ↦ h2 h1

Premises used: Filter.Tendsto.eventually, Subtype.property
-- Module: Mathlib.Topology.Algebra.RestrictedProduct.Basic
Goal:
ι₁ : 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)
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]_[𝓕₁]
j : ι₂
⊢ (mapAlong R₁ R₂ (A₁ := A₁) (A₂ := A₂) f hf φ hφ x : (a : ι₂) → R₂ a) j = φ j ((x : (a : ι₁) → R₁ a) (f j))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.RestrictedProduct.Basic
Goal:
ι : Type u_1
𝓕 : Filter ι
G : ι → Type u_9
H : ι → Type u_10
C : (i : ι) → Set (G i)
D : (i : ι) → Set (H i)
φ : (i : ι) → G i → H i
hφ : ∀ᶠ (i : ι) in 𝓕, MapsTo (φ i) (C i) (D i)
x : Πʳ (i : ι), [G i, C i]_[𝓕]
j : ι
⊢ (map (G := G) (H := H) (C := C) (D := D) φ hφ x : (a : ι) → H a) j = φ j ((x : (a : ι) → G a) j)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.RestrictedProduct.Basic
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))
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
⊢ 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

Tactic:
ext i
-- Module: Mathlib.Topology.Algebra.RestrictedProduct.Basic
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))
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:
map_one (φ i)

Premises used: map_one
-- Module: Mathlib.Topology.Algebra.RestrictedProduct.Basic
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))
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:
exact map_one (φ i)

Premises used: map_one
-- Module: Mathlib.Topology.Algebra.RestrictedProduct.Basic
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))]_[𝓕₁]
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
⊢ 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)

Tactic:
ext i