awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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))]_[𝓕₁]
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:
map_mul (φ i) _ _

Premises used: map_mul
-- 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))]_[𝓕₁]
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:
exact map_mul (φ i) _ _

Premises used: map_mul
-- Module: Mathlib.Topology.Algebra.RestrictedProduct.Basic
Goal:
ι₁ : Type u_3
ι₂ : Type u_4
R₁ : ι₁ → Type u_5
R₂ : ι₂ → Type u_6
𝓕₁ : Filter ι₁
𝓕₂ : Filter ι₂
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 : Πʳ (i : ι₁), [R₁ i, (↑(B₁ i) : Set ((fun (i : ι₁) ↦ R₁ i) i))]_[𝓕₁]
j : ι₂
⊢ (((mapAlongMonoidHom R₁ R₂ (S₁ := S₁) (S₂ := S₂) f hf φ hφ :
              (a : Πʳ (i : ι₁), [R₁ i, (↑(B₁ i) : Set ((fun (i : ι₁) ↦ R₁ i) i))]_[𝓕₁]) →
                Πʳ (j : ι₂), [R₂ j, (↑(B₂ j) : Set ((fun (j : ι₂) ↦ R₂ j) j))]_[𝓕₂])
            x :
          Πʳ (j : ι₂), [R₂ j, (↑(B₂ j) : Set ((fun (j : ι₂) ↦ R₂ j) j))]_[𝓕₂]) :
        (a : ι₂) → R₂ a)
      j =
    (φ j : (a : R₁ (f j)) → R₂ j) ((x : (a : ι₁) → R₁ a) (f j))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.RestrictedProduct.Basic
Goal:
ι₁ : Type u_3
ι₂ : Type u_4
R₁ : ι₁ → Type u_5
R₂ : ι₂ → Type u_6
𝓕₁ : Filter ι₁
𝓕₂ : Filter ι₂
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 : ι₁) → Ring (R₁ i)
inst_3 : (i : ι₂) → Ring (R₂ i)
inst_4 : ∀ (i : ι₁), SubringClass.{u_5, u_7} (S₁ i) (R₁ i)
inst_5 : ∀ (i : ι₂), SubringClass.{u_6, u_8} (S₂ i) (R₂ i)
φ : (j : ι₂) → RingHom.{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 : Πʳ (i : ι₁), [R₁ i, (↑(B₁ i) : Set ((fun (i : ι₁) ↦ R₁ i) i))]_[𝓕₁]
j : ι₂
⊢ (((mapAlongRingHom R₁ R₂ (S₁ := S₁) (S₂ := S₂) f hf φ hφ :
              (a : Πʳ (i : ι₁), [R₁ i, (↑(B₁ i) : Set ((fun (i : ι₁) ↦ R₁ i) i))]_[𝓕₁]) →
                Πʳ (j : ι₂), [R₂ j, (↑(B₂ j) : Set ((fun (j : ι₂) ↦ R₂ j) j))]_[𝓕₂])
            x :
          Πʳ (j : ι₂), [R₂ j, (↑(B₂ j) : Set ((fun (j : ι₂) ↦ R₂ j) j))]_[𝓕₂]) :
        (a : ι₂) → R₂ a)
      j =
    (φ j : (a : R₁ (f j)) → R₂ j) ((x : (a : ι₁) → R₁ a) (f j))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Topology.Algebra.RestrictedProduct.Basic
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
⊢ Membership.mem (γ := Filter ι) cofinite {i}ᶜ

Tactic:
simp
-- Module: Mathlib.Topology.Algebra.RestrictedProduct.Basic
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
h : ∀ (a : ι), Membership.mem (γ := Set ι) {i}ᶜ a → Pi.mulSingle (M := fun (i : ι) ↦ G i) i x a ∈ (↑(A a) : Set (G a))
⊢ ∀ᶠ (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)

Tactic:
filter_upwards [show {i}ᶜ ∈ Filter.cofinite by simp]
-- Module: Mathlib.Topology.Algebra.RestrictedProduct.Basic
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
⊢ ∀ (a : ι), Membership.mem (γ := Set ι) {i}ᶜ a → Pi.mulSingle (M := fun (i : ι) ↦ G i) i x a ∈ (↑(A a) : Set (G a))

Tactic:
simp_all
-- Module: Mathlib.Topology.Algebra.RestrictedProduct.Basic
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 : ι
x : G i
j : ι
⊢ (mulSingle (S := S) (G := G) A i x : (a : ι) → G a) j = Pi.mulSingle (M := G) i x j

Tactic:
rfl

Premises used: Function.update, dite, Pi.mulSingle, rfl
-- Module: Mathlib.Topology.Algebra.RestrictedProduct.Basic
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 : ι
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
⊢ 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

Tactic:
ext
-- Module: Mathlib.Topology.Algebra.RestrictedProduct.Basic
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 : ι
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:
simp
-- Module: Mathlib.Topology.Algebra.RestrictedProduct.Basic
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 : ι
x y : G i
⊢ Eq (α := Πʳ (i : ι), [G i, (↑(A i) : Set ((fun (i : ι) ↦ G i) i))]) (mulSingle (S := S) (G := G) A i x)
      (mulSingle (S := S) (G := G) A i y) ↔
    x = y

Tactic:
(mulSingle_injective A i).eq_iff

Premises used: RestrictedProduct.mulSingle_injective, Function.Injective.eq_iff
-- Module: Mathlib.Topology.Algebra.RestrictedProduct.Basic
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 : ι
r : G i
⊢ (mulSingle (S := S) (G := G) A i r : (a : ι) → G a) i = r

Tactic:
Pi.mulSingle_eq_same i r

Premises used: Function.update, Pi.mulSingle_eq_same, dite, Pi.mulSingle
-- Module: Mathlib.Topology.Algebra.RestrictedProduct.Basic
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 j : ι
r : G i
h : j ≠ i
⊢ (mulSingle (S := S) (G := G) A i r : (a : ι) → G a) j = 1

Tactic:
Pi.mulSingle_eq_of_ne h r

Premises used: Function.update, dite, Pi.mulSingle_eq_of_ne, Pi.mulSingle
-- Module: Mathlib.Topology.Algebra.RestrictedProduct.Basic
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 j : ι
r : G i
h : i ≠ j
⊢ (mulSingle (S := S) (G := G) A i r : (a : ι) → G a) j = 1

Tactic:
Pi.mulSingle_eq_of_ne' h r

Premises used: Function.update, dite, Pi.mulSingle_eq_of_ne', Pi.mulSingle
-- Module: Mathlib.Topology.Algebra.RestrictedProduct.Basic
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 : ι
h : ∀ (i_1 : ι), (mulSingle (S := S) (G := G) A i 1 : (a : ι) → G a) i_1 = (1 : (a : ι) → G a) i_1
⊢ Eq (α := Πʳ (i : ι), [G i, (↑(A i) : Set ((fun (i : ι) ↦ G i) i))]) (mulSingle (S := S) (G := G) A i 1) 1

Tactic:
ext
-- Module: Mathlib.Topology.Algebra.RestrictedProduct.Basic
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 i_1 : ι
⊢ (mulSingle (S := S) (G := G) A i 1 : (a : ι) → G a) i_1 = (1 : (a : ι) → G a) i_1

Tactic:
simp
-- Module: Mathlib.Topology.Algebra.RestrictedProduct.Basic
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 : ι
x : G i
⊢ Eq (α := Πʳ (i : ι), [G i, (↑(A i) : Set ((fun (i : ι) ↦ G i) i))]) (mulSingle (S := S) (G := G) A i x) 1 ↔ x = 1

Tactic:
Subtype.ext_iff.trans Pi.mulSingle_eq_one_iff

Premises used: Pi.mulSingle_eq_one_iff, Subtype.ext_iff, RestrictedProduct, Iff.trans
-- Module: Mathlib.Topology.Algebra.RestrictedProduct.Basic
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 : ι
x : G i
⊢ Ne (α := Πʳ (i : ι), [G i, (↑(A i) : Set ((fun (i : ι) ↦ G i) i))]) (mulSingle (S := S) (G := G) A i x) 1 ↔ x ≠ 1

Tactic:
Subtype.coe_ne_coe.symm.trans Pi.mulSingle_ne_one_iff

Premises used: RestrictedProduct, Pi.mulSingle_ne_one_iff, Iff.trans, Iff.symm, Subtype.coe_ne_coe
-- Module: Mathlib.Topology.Algebra.RestrictedProduct.Basic
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
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
⊢ 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)

Tactic:
ext
-- Module: Mathlib.Topology.Algebra.RestrictedProduct.Basic
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
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:
simp [Pi.mulSingle_mul]

Premises used: Pi.mulSingle_mul
-- Module: Mathlib.Topology.Algebra.RestrictedProduct.Basic
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 : ι) → MulZeroClass (G i)
inst_3 : ∀ (i : ι), ZeroMemClass.{u_3, u_4} (S i) (G i)
inst_4 : ∀ (i : ι), MulMemClass.{u_3, u_4} (S i) (G i)
i : ι
r : G i
x : Πʳ (i : ι), [G i, (↑(A i) : Set ((fun (i : ι) ↦ G i) i))]
h :
  ∀ (j : ι),
    (single (S := S) (G := G) A i ((x : (a : ι) → G a) i * r) : (a : ι) → G a) j =
      (x * single (S := S) (G := G) A i r : (a : ι) → G a) j
⊢ single (S := S) (G := G) A i ((x : (a : ι) → G a) i * r) = x * single (S := S) (G := G) A i r

Tactic:
ext j
-- Module: Mathlib.Topology.Algebra.RestrictedProduct.Basic
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 : ι) → MulZeroClass (G i)
inst_3 : ∀ (i : ι), ZeroMemClass.{u_3, u_4} (S i) (G i)
inst_4 : ∀ (i : ι), MulMemClass.{u_3, u_4} (S i) (G i)
i : ι
r : G i
x : Πʳ (i : ι), [G i, (↑(A i) : Set ((fun (i : ι) ↦ G i) i))]
j : ι
h :
  (single (S := S) (G := G) A i ((x : (a : ι) → G a) i * r) : (a : ι) → G a) i =
    (x * single (S := S) (G := G) A i r : (a : ι) → G a) i
h₁ :
  ∀ (hne : i ≠ j),
    (single (S := S) (G := G) A i ((x : (a : ι) → G a) i * r) : (a : ι) → G a) j =
      (x * single (S := S) (G := G) A i r : (a : ι) → G a) j
⊢ (single (S := S) (G := G) A i ((x : (a : ι) → G a) i * r) : (a : ι) → G a) j =
    (x * single (S := S) (G := G) A i r : (a : ι) → G a) j

Tactic:
rcases eq_or_ne i j with rfl | hne

Premises used: eq_or_ne, rfl
-- Module: Mathlib.Topology.Algebra.RestrictedProduct.Basic
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 : ι) → MulZeroClass (G i)
inst_3 : ∀ (i : ι), ZeroMemClass.{u_3, u_4} (S i) (G i)
inst_4 : ∀ (i : ι), MulMemClass.{u_3, u_4} (S i) (G i)
i : ι
r : G i
x : Πʳ (i : ι), [G i, (↑(A i) : Set ((fun (i : ι) ↦ G i) i))]
⊢ (single (S := S) (G := G) A i ((x : (a : ι) → G a) i * r) : (a : ι) → G a) i =
    (x * single (S := S) (G := G) A i r : (a : ι) → G a) i

Tactic:
simp
-- Module: Mathlib.Topology.Algebra.RestrictedProduct.Basic
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 : ι) → MulZeroClass (G i)
inst_3 : ∀ (i : ι), ZeroMemClass.{u_3, u_4} (S i) (G i)
inst_4 : ∀ (i : ι), MulMemClass.{u_3, u_4} (S i) (G i)
i : ι
r : G i
x : Πʳ (i : ι), [G i, (↑(A i) : Set ((fun (i : ι) ↦ G i) i))]
j : ι
hne : i ≠ j
⊢ (single (S := S) (G := G) A i ((x : (a : ι) → G a) i * r) : (a : ι) → G a) j =
    (x * single (S := S) (G := G) A i r : (a : ι) → G a) j

Tactic:
simp [single_eq_of_ne' A _ hne]

Premises used: RestrictedProduct.single_eq_of_ne'
-- Module: Mathlib.Topology.Algebra.RestrictedProduct.Basic
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 : ι) → MulZeroClass (G i)
inst_3 : ∀ (i : ι), ZeroMemClass.{u_3, u_4} (S i) (G i)
inst_4 : ∀ (i : ι), MulMemClass.{u_3, u_4} (S i) (G i)
i : ι
r : G i
x : Πʳ (i : ι), [G i, (↑(A i) : Set ((fun (i : ι) ↦ G i) i))]
h :
  ∀ (j : ι),
    (single (S := S) (G := G) A i (r * (x : (a : ι) → G a) i) : (a : ι) → G a) j =
      (single (S := S) (G := G) A i r * x : (a : ι) → G a) j
⊢ single (S := S) (G := G) A i (r * (x : (a : ι) → G a) i) = single (S := S) (G := G) A i r * x

Tactic:
ext j
-- Module: Mathlib.Topology.Algebra.RestrictedProduct.Basic
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 : ι) → MulZeroClass (G i)
inst_3 : ∀ (i : ι), ZeroMemClass.{u_3, u_4} (S i) (G i)
inst_4 : ∀ (i : ι), MulMemClass.{u_3, u_4} (S i) (G i)
i : ι
r : G i
x : Πʳ (i : ι), [G i, (↑(A i) : Set ((fun (i : ι) ↦ G i) i))]
j : ι
h :
  (single (S := S) (G := G) A i (r * (x : (a : ι) → G a) i) : (a : ι) → G a) i =
    (single (S := S) (G := G) A i r * x : (a : ι) → G a) i
h₁ :
  ∀ (hne : i ≠ j),
    (single (S := S) (G := G) A i (r * (x : (a : ι) → G a) i) : (a : ι) → G a) j =
      (single (S := S) (G := G) A i r * x : (a : ι) → G a) j
⊢ (single (S := S) (G := G) A i (r * (x : (a : ι) → G a) i) : (a : ι) → G a) j =
    (single (S := S) (G := G) A i r * x : (a : ι) → G a) j

Tactic:
rcases eq_or_ne i j with rfl | hne

Premises used: eq_or_ne, rfl
-- Module: Mathlib.Topology.Algebra.RestrictedProduct.Basic
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 : ι) → MulZeroClass (G i)
inst_3 : ∀ (i : ι), ZeroMemClass.{u_3, u_4} (S i) (G i)
inst_4 : ∀ (i : ι), MulMemClass.{u_3, u_4} (S i) (G i)
i : ι
r : G i
x : Πʳ (i : ι), [G i, (↑(A i) : Set ((fun (i : ι) ↦ G i) i))]
⊢ (single (S := S) (G := G) A i (r * (x : (a : ι) → G a) i) : (a : ι) → G a) i =
    (single (S := S) (G := G) A i r * x : (a : ι) → G a) i

Tactic:
simp
-- Module: Mathlib.Topology.Algebra.RestrictedProduct.Basic
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 : ι) → MulZeroClass (G i)
inst_3 : ∀ (i : ι), ZeroMemClass.{u_3, u_4} (S i) (G i)
inst_4 : ∀ (i : ι), MulMemClass.{u_3, u_4} (S i) (G i)
i : ι
r : G i
x : Πʳ (i : ι), [G i, (↑(A i) : Set ((fun (i : ι) ↦ G i) i))]
j : ι
hne : i ≠ j
⊢ (single (S := S) (G := G) A i (r * (x : (a : ι) → G a) i) : (a : ι) → G a) j =
    (single (S := S) (G := G) A i r * x : (a : ι) → G a) j

Tactic:
simp [single_eq_of_ne' A _ hne]

Premises used: RestrictedProduct.single_eq_of_ne'
-- Module: Mathlib.Topology.Algebra.RestrictedProduct.Basic
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 : ι) → Group (G i)
inst_3 : ∀ (i : ι), SubgroupClass.{u_3, u_4} (S i) (G i)
i : ι
r : G i
h :
  ∀ (i_1 : ι),
    (mulSingle (S := S) (G := G) A i r⁻¹ : (a : ι) → G a) i_1 =
      ((mulSingle (S := S) (G := G) A i r)⁻¹ : (a : ι) → G a) i_1
⊢ Eq (α := Πʳ (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 r)⁻¹

Tactic:
ext
-- Module: Mathlib.Topology.Algebra.RestrictedProduct.Basic
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 : ι) → Group (G i)
inst_3 : ∀ (i : ι), SubgroupClass.{u_3, u_4} (S i) (G i)
i : ι
r : G i
i_1 : ι
⊢ (mulSingle (S := S) (G := G) A i r⁻¹ : (a : ι) → G a) i_1 =
    ((mulSingle (S := S) (G := G) A i r)⁻¹ : (a : ι) → G a) i_1

Tactic:
simp [Pi.mulSingle_inv]

Premises used: Pi.mulSingle_inv
-- Module: Mathlib.Topology.Algebra.RestrictedProduct.Basic
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 : ι) → Group (G i)
inst_3 : ∀ (i : ι), SubgroupClass.{u_3, u_4} (S i) (G i)
i : ι
r s : G i
h :
  ∀ (i_1 : ι),
    (mulSingle (S := S) (G := G) A i (r / s) : (a : ι) → G a) i_1 =
      (HDiv.hDiv (α := Πʳ (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
⊢ mulSingle (S := S) (G := G) A i (r / s) =
    HDiv.hDiv (α := Πʳ (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)

Tactic:
ext
-- Module: Mathlib.Topology.Algebra.RestrictedProduct.Basic
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 : ι) → Group (G i)
inst_3 : ∀ (i : ι), SubgroupClass.{u_3, u_4} (S i) (G i)
i : ι
r s : G i
i_1 : ι
⊢ (mulSingle (S := S) (G := G) A i (r / s) : (a : ι) → G a) i_1 =
    (HDiv.hDiv (α := Πʳ (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:
simp [Pi.mulSingle_div]

Premises used: Pi.mulSingle_div