mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.NumberTheory.ModularForms.LFunction

Goal state before:
pp: Γ : Subgroup (GL (Fin 2) ℝ)
inst✝² : Γ.IsArithmetic
k : ℤ
hk : 0 < k
F : Type u_1
inst✝¹ : FunLike F ℍ ℂ
f : F
inst✝ : CuspFormClass F Γ k
⊢ Differentiable ℂ (L hk f)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.DedekindDomain.FiniteAdeleRing

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
k : K
⊢ (Support R k).Finite

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.LFunction

Goal state before:
pp: Γ : Subgroup (GL (Fin 2) ℝ)
inst✝² : Γ.IsArithmetic
k : ℤ
hk : 0 < k
F : Type u_1
inst✝¹ : FunLike F ℍ ℂ
f : F
s : ℂ
inst✝ : CuspFormClass F Γ k
hs : ↑k / 2 + 1 < s.re
⊢ 0 < s.re

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.DedekindDomain.FiniteAdeleRing

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
k : K
⊢ ∀ᶠ (i : HeightOneSpectrum R) in Filter.cofinite,
    (fun i ↦ { toCompletion := ↑((WithVal.equiv (valuation K i)).symm k) }) i ∈
      (fun v ↦ ↑(adicCompletionIntegers K v)) i

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Multiplicity

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
x y : R
d : ℕ
hd : x ^ 2 ^ d - y ^ 2 ^ d = (∏ i ∈ range d, (x ^ 2 ^ i + y ^ 2 ^ i)) * (x - y)
this : x ^ 2 ^ d.succ - y ^ 2 ^ d.succ = (x ^ 2 ^ d + y ^ 2 ^ d) * (x ^ 2 ^ d - y ^ 2 ^ d)
⊢ x ^ 2 ^ (d + 1) - y ^ 2 ^ (d + 1) = (∏ i ∈ range (d + 1), (x ^ 2 ^ i + y ^ 2 ^ i)) * (x - y)

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.DedekindDomain.FiniteAdeleRing

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
a : 𝔸ᶠ[R, K]
⊢ IsUnit a ↔
    (∀ (v : HeightOneSpectrum R), a v ≠ 0) ∧ ∀ᶠ (v : HeightOneSpectrum R) in Filter.cofinite, Valued.v (a v) = 1

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.DedekindDomain.FiniteAdeleRing

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
a : 𝔸ᶠ[R, K]ˣ
⊢ ∀ᶠ (v : HeightOneSpectrum R) in Filter.cofinite,
    Valued.v ↑(((RestrictedProduct.unitsEquiv (adicCompletion K)) a) v) = 1

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace

Goal state before:
pp: ι : Type u_1
R : ι → Type u_2
A : (i : ι) → Set (R i)
inst✝¹ : (i : ι) → TopologicalSpace (R i)
S : Set ι
inst✝ : ∀ (i : ι), WeaklyLocallyCompactSpace (R i)
hS : cofinite ≤ 𝓟 S
hAcompact : ∀ i ∈ S, IsCompact (A i)
x : Πʳ (i : ι), [R i, A i]_[𝓟 S]
⊢ ∃ s, IsCompact s ∧ s ∈ 𝓝 x

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Multiplicity

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
x y : R
n : ℕ
⊢ x ^ 2 ^ n - y ^ 2 ^ n = (∏ i ∈ range n, (x ^ 2 ^ i + y ^ 2 ^ i)) * (x - y)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace

Goal state before:
pp: ι : Type u_1
R : ι → Type u_2
A : (i : ι) → Set (R i)
𝓕 : Filter ι
inst✝ : (i : ι) → TopologicalSpace (R i)
⊢ topologicalSpace R A 𝓕 =
    ⨆ S, ⨆ (hS : 𝓕 ≤ 𝓟 S), TopologicalSpace.coinduced (inclusion R A hS) (topologicalSpace R A (𝓟 S))

Tactic:
by

Goal state after:
Module: Mathlib.RingTheory.DedekindDomain.FiniteAdeleRing

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
a : 𝔸ᶠ[R, K]
ha₀ : ∀ (v : HeightOneSpectrum R), a v ≠ 0
ha : ¬IsUnit a
⊢ {v | Valued.v (a v) ≠ 1}.Infinite

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Multiplicity

Goal state before:
pp: x : ℤ
⊢ Odd x → x ^ 2 % 4 = 1

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Multiplicity

Goal state before:
pp: m : ℤ
⊢ (2 * m + 1) ^ 2 - 1 = 4 * (m * (m + 1))

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace

Goal state before:
pp: ι : Type u_1
R : ι → Type u_2
A : (i : ι) → Set (R i)
𝓕 : Filter ι
inst✝¹ : (i : ι) → TopologicalSpace (R i)
X : Type u_3
inst✝ : TopologicalSpace X
f : Πʳ (i : ι), [R i, A i]_[𝓕] → X
⊢ Continuous[topologicalSpace R A 𝓕, inst✝] f ↔
    ∀ (S : Set ι) (hS : 𝓕 ≤ 𝓟 S), Continuous[topologicalSpace R A (𝓟 S), inst✝] (f ∘ inclusion R A hS)

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Multiplicity

Goal state before:
pp: k : ℤ
hk : Odd k
⊢ 8 ∣ k ^ 2 - 1

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Multiplicity

Goal state before:
pp: m : ℕ
⊢ (2 * m + 1) ^ 2 - 1 = 4 * (m * (m + 1))

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Multiplicity

Goal state before:
pp: k : ℕ
hk : Odd k
⊢ 8 ∣ k ^ 2 - 1

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Multiplicity

Goal state before:
pp: x y : ℤ
hx : ¬2 ∣ x
hxy : 4 ∣ x - y
i : ℕ
⊢ Odd x

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Multiplicity

Goal state before:
pp: x y : ℤ
hx : ¬2 ∣ x
hxy : 4 ∣ x - y
i : ℕ
hx_odd : Odd x
⊢ 2 ∣ 4

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Multiplicity

Goal state before:
pp: x y : ℤ
hx : ¬2 ∣ x
hxy : 4 ∣ x - y
i : ℕ
hx_odd : Odd x
hxy_even : Even (x - y)
⊢ Odd y

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace

Goal state before:
pp: ι : Type u_1
R : ι → Type u_2
A : (i : ι) → Set (R i)
inst✝ : (i : ι) → TopologicalSpace (R i)
hAopen : ∀ (i : ι), IsOpen[inst✝ i] (A i)
S : Set ι
hS : cofinite ≤ 𝓟 S
p : ι → Prop
⊢ IsOpen[topologicalSpace R A (𝓟 S)] {f | ∀ (i : ι), p i → ↑f i ∈ A i}

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace

Goal state before:
pp: ι : Type u_1
R : ι → Type u_2
A : (i : ι) → Set (R i)
inst✝ : (i : ι) → TopologicalSpace (R i)
hAopen : ∀ (i : ι), IsOpen[inst✝ i] (A i)
S : Set ι
hS : cofinite ≤ 𝓟 S
⊢ IsOpen[topologicalSpace R A (𝓟 S)] {f | ∀ (i : ι), ↑f i ∈ A i}

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace

Goal state before:
pp: ι : Type u_1
R : ι → Type u_2
A : (i : ι) → Set (R i)
inst✝ : (i : ι) → TopologicalSpace (R i)
hAopen : ∀ (i : ι), IsOpen[inst✝ i] (A i)
p : ι → Prop
⊢ IsOpen[topologicalSpace R A cofinite] {f | ∀ (i : ι), p i → ↑f i ∈ A i}

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Multiplicity

Goal state before:
pp: x y : ℤ
hx : ¬2 ∣ x
hxy : 4 ∣ x - y
hx_odd : Odd x
hxy_even : Even (x - y)
hy_odd : Odd y
i : ℕ
this : ∀ (x : ℤ), Odd x → x ^ 2 ^ (i + 1) % 4 = 1
⊢ ¬2 ^ (1 + 1) ∣ x ^ 2 ^ (i + 1) + y ^ 2 ^ (i + 1)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace

Goal state before:
pp: ι : Type u_1
R : ι → Type u_2
A : (i : ι) → Set (R i)
inst✝ : (i : ι) → TopologicalSpace (R i)
hAopen : ∀ (i : ι), IsOpen[inst✝ i] (A i)
⊢ IsOpen[topologicalSpace R A cofinite] {f | ∀ (i : ι), ↑f i ∈ A i}

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Multiplicity

Goal state before:
pp: x y : ℤ
hx : ¬2 ∣ x
hxy : 4 ∣ x - y
i : ℕ
⊢ emultiplicity 2 (x ^ 2 ^ i + y ^ 2 ^ i) = ↑1

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Multiplicity

Goal state before:
pp: x y : ℤ
n : ℕ
hxy : 4 ∣ x - y
hx : ¬2 ∣ x
⊢ emultiplicity 2 (x ^ 2 ^ n - y ^ 2 ^ n) = emultiplicity 2 (x - y) + ↑n

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Multiplicity

Goal state before:
pp: x y : ℤ
n : ℕ
hxy : 4 ∣ x - y
hx : ¬2 ∣ x
⊢ Odd x

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Multiplicity

Goal state before:
pp: x y : ℤ
n : ℕ
hxy : 4 ∣ x - y
hx : ¬2 ∣ x
hx_odd : Odd x
⊢ 2 ∣ 4

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace

Goal state before:
pp: ι : Type u_1
R : ι → Type u_2
A : (i : ι) → Set (R i)
inst✝ : (i : ι) → TopologicalSpace (R i)
hAopen : ∀ (i : ι), IsOpen[inst✝ i] (A i)
S : Set ι
hS : cofinite ≤ 𝓟 S
⊢ IsOpen[topologicalSpace R A cofinite] (range (inclusion R A hS))

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Multiplicity

Goal state before:
pp: x y : ℤ
n : ℕ
hxy : 4 ∣ x - y
hx : ¬2 ∣ x
hx_odd : Odd x
hxy_even : Even (x - y)
⊢ Odd y

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace

Goal state before:
pp: ι : Type u_1
R : ι → Type u_2
A : (i : ι) → Set (R i)
inst✝ : (i : ι) → TopologicalSpace (R i)
hAopen : ∀ (i : ι), IsOpen[inst✝ i] (A i)
⊢ IsOpen[topologicalSpace R A cofinite] (range (structureMap R A cofinite))

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Multiplicity

Goal state before:
pp: x y : ℤ
hxy : 4 ∣ x - y
hx : ¬2 ∣ x
hx_odd : Odd x
hxy_even : Even (x - y)
hy_odd : Odd y
n : ℕ
⊢ 2 ≠ 1

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace

Goal state before:
pp: ι : Type u_1
R : ι → Type u_2
A : (i : ι) → Set (R i)
inst✝ : (i : ι) → TopologicalSpace (R i)
hAopen : ∀ (i : ι), IsOpen[inst✝ i] (A i)
S : Set ι
hS : cofinite ≤ 𝓟 S
x : Πʳ (i : ι), [R i, A i]_[𝓟 S]
⊢ 𝓝 (inclusion R A hS x) = Filter.map (inclusion R A hS) (𝓝 x)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace

Goal state before:
pp: ι : Type u_1
R : ι → Type u_2
A : (i : ι) → Set (R i)
inst✝ : (i : ι) → TopologicalSpace (R i)
hAopen : ∀ (i : ι), IsOpen[inst✝ i] (A i)
x : (i : ι) → ↑(A i)
⊢ 𝓝 (structureMap R A cofinite x) = Filter.map (structureMap R A cofinite) (𝓝 x)

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Multiplicity

Goal state before:
pp: x y : ℤ
n : ℕ
hxy : 4 ∣ x - y
hx : ¬2 ∣ x
⊢ emultiplicity 2 (x ^ n - y ^ n) = emultiplicity 2 (x - y) + emultiplicity 2 ↑n

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Multiplicity

Goal state before:
pp: x y : ℤ
n : ℕ
hxy : 2 ∣ x - y
hx : ¬2 ∣ x
hn : Even n
⊢ Odd y

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace

Goal state before:
pp: ι : Type u_1
R : ι → Type u_2
A : (i : ι) → Set (R i)
inst✝¹ : (i : ι) → TopologicalSpace (R i)
hAopen : ∀ (i : ι), IsOpen[inst✝¹ i] (A i)
inst✝ : ∀ (i : ι), WeaklyLocallyCompactSpace (R i)
hAcompact : ∀ᶠ (i : ι) in cofinite, IsCompact (A i)
x : Πʳ (i : ι), [R i, A i]
⊢ ∃ s, IsCompact s ∧ s ∈ 𝓝 x

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Multiplicity

Goal state before:
pp: x y : ℤ
hxy : 2 ∣ x - y
hx : ¬2 ∣ x
hy : Odd y
d : ℕ
⊢ 4 ∣ x ^ 2 - y ^ 2

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Multiplicity

Goal state before:
pp: x y : ℤ
hxy : 2 ∣ x - y
hx : ¬2 ∣ x
hy : Odd y
d : ℕ
hxy4 : 4 ∣ x ^ 2 - y ^ 2
this : emultiplicity 2 ↑2 = 1
⊢ emultiplicity 2 (x + y) + emultiplicity 2 (x - y) + emultiplicity 2 ↑d + 1 =
    emultiplicity 2 (x + y) + emultiplicity 2 (x - y) + (emultiplicity 2 ↑2 + emultiplicity 2 ↑d)

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Multiplicity

Goal state before:
pp: x y : ℤ
n : ℕ
hxy : 2 ∣ x - y
hx : ¬2 ∣ x
hn : Even n
⊢ emultiplicity 2 (x ^ n - y ^ n) + 1 = emultiplicity 2 (x + y) + emultiplicity 2 (x - y) + emultiplicity 2 ↑n

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace

Goal state before:
pp: ι : Type u_1
R : ι → Type u_2
A : (i : ι) → Set (R i)
inst✝² : (i : ι) → TopologicalSpace (R i)
hAopen : ∀ (i : ι), IsOpen[inst✝² i] (A i)
X : Type u_3
Y : Type u_4
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : Πʳ (i : ι), [R i, A i] × Y → X
⊢ Continuous[instTopologicalSpaceProd, inst✝¹] f ↔
    ∀ (S : Set ι) (hS : cofinite ≤ 𝓟 S),
      Continuous[instTopologicalSpaceProd, inst✝¹] (f ∘ Prod.map (inclusion R A hS) id)

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Multiplicity

Goal state before:
pp: x y : ℕ
hxy : 2 ∣ x - y
hx : ¬2 ∣ x
n : ℕ
hn : Even n
⊢ emultiplicity 2 (x ^ n - y ^ n) + 1 = emultiplicity 2 (x + y) + emultiplicity 2 (x - y) + emultiplicity 2 n

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace

Goal state before:
pp: ι : Type u_1
R : ι → Type u_2
A : (i : ι) → Set (R i)
inst✝² : (i : ι) → TopologicalSpace (R i)
hAopen : ∀ (i : ι), IsOpen[inst✝² i] (A i)
X : Type u_3
Y : Type u_4
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : Y × Πʳ (i : ι), [R i, A i] → X
⊢ Continuous[instTopologicalSpaceProd, inst✝¹] f ↔
    ∀ (S : Set ι) (hS : cofinite ≤ 𝓟 S),
      Continuous[instTopologicalSpaceProd, inst✝¹] (f ∘ Prod.map id (inclusion R A hS))

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Multiplicity

Goal state before:
pp: x y : ℕ
hyx : y < x
hxy : 2 ∣ x - y
hx : ¬2 ∣ x
n : ℕ
hn : n ≠ 0
hneven : Even n
⊢ padicValNat 2 (x ^ n - y ^ n) + 1 = padicValNat 2 (x + y) + padicValNat 2 (x - y) + padicValNat 2 n

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace

Goal state before:
pp: ι : Type u_1
R : ι → Type u_2
A : (i : ι) → Set (R i)
inst✝² : (i : ι) → TopologicalSpace (R i)
hAopen : ∀ (i : ι), IsOpen[inst✝² i] (A i)
R' : ι → Type u_3
A' : (i : ι) → Set (R' i)
inst✝¹ : (i : ι) → TopologicalSpace (R' i)
hAopen' : ∀ (i : ι), IsOpen[inst✝¹ i] (A' i)
X : Type u_4
inst✝ : TopologicalSpace X
f : Πʳ (i : ι), [R i, A i] × Πʳ (i : ι), [R' i, A' i] → X
⊢ Continuous[instTopologicalSpaceProd, inst✝] f ↔
    ∀ (S : Set ι) (hS : cofinite ≤ 𝓟 S),
      Continuous[instTopologicalSpaceProd, inst✝] (f ∘ Prod.map (inclusion R A hS) (inclusion R' A' hS))

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Multiplicity

Goal state before:
pp: x n : ℕ
h1x : 1 < x
hx : ¬2 ∣ x
hn : n ≠ 0
hneven : Even n
⊢ 2 ∣ x - 1

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Multiplicity

Goal state before:
pp: x n : ℕ
h1x : 1 < x
hx : ¬2 ∣ x
hn : n ≠ 0
hneven : Even n
⊢ padicValNat 2 (x ^ n - 1) + 1 = padicValNat 2 (x + 1) + padicValNat 2 (x - 1) + padicValNat 2 n

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace

Goal state before:
pp: ι : Type u_1
n : Type u_3
inst✝² : Finite n
X : Type u_4
inst✝¹ : TopologicalSpace X
A : n → ι → Type u_5
inst✝ : (j : n) → (i : ι) → TopologicalSpace (A j i)
C : (j : n) → (i : ι) → Set (A j i)
hCopen : ∀ (j : n) (i : ι), IsOpen[inst✝ j i] (C j i)
f : ((j : n) → Πʳ (i : ι), [A j i, C j i]) → X
⊢ Continuous[Pi.topologicalSpace, inst✝¹] f →
    ∀ (S : Set ι) (hS : cofinite ≤ 𝓟 S),
      Continuous[Pi.topologicalSpace, inst✝¹] (f ∘ Pi.map fun x ↦ inclusion (A x) (C x) hS)

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Multiplicity

Goal state before:
pp: n x : ℕ
h1x : 1 < x
hx : ¬2 ∣ x
hn : n ≠ 0
hneven : Even n
⊢ (x + 1) * (x - 1) ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Multiplicity

Goal state before:
pp: n x : ℕ
h1x : 1 < x
hx : ¬2 ∣ x
hn : n ≠ 0
hneven : Even n
⊢ padicValNat 2 ((x + 1) * (x - 1)) ≥ 3

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Multiplicity

Goal state before:
pp: n x : ℕ
h1x : 1 < x
hx : ¬2 ∣ x
hn : n ≠ 0
hneven : Even n
⊢ padicValNat 2 n + 2 ≤ padicValNat 2 (x ^ n - 1)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace

Goal state before:
pp: ι : Type u_1
n : Type u_3
inst✝² : Finite n
X : Type u_4
inst✝¹ : TopologicalSpace X
A : n → ι → Type u_5
inst✝ : (j : n) → (i : ι) → TopologicalSpace (A j i)
C : (j : n) → (i : ι) → Set (A j i)
hCopen : ∀ (j : n) (i : ι), IsOpen[inst✝ 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✝¹] (f ∘ Pi.map fun x ↦ inclusion (A x) (C x) hS)
x : (j : n) → Πʳ (i : ι), [A j i, C j i]
S : Set ι := {i | ∀ (j : n), (x j) i ∈ C j i}
⊢ cofinite ≤ 𝓟 S

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Multiplicity

Goal state before:
pp: x y p : ℕ
hp : Fact (Nat.Prime p)
hp1 : Odd p
hyx : y < x
hxy : p ∣ x - y
hx : ¬p ∣ x
n : ℕ
hn : n ≠ 0
⊢ padicValNat p (x ^ n - y ^ n) = padicValNat p (x - y) + padicValNat p n

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace

Goal state before:
pp: ι : Type u_1
n : Type u_3
inst✝² : Finite n
X : Type u_4
inst✝¹ : TopologicalSpace X
A : n → ι → Type u_5
inst✝ : (j : n) → (i : ι) → TopologicalSpace (A j i)
C : (j : n) → (i : ι) → Set (A j i)
hCopen : ∀ (j : n) (i : ι), IsOpen[inst✝ j i] (C j i)
f : ((j : n) → Πʳ (i : ι), [A j i, C j i]) → X
⊢ Continuous[Pi.topologicalSpace, inst✝¹] f ↔
    ∀ (S : Set ι) (hS : cofinite ≤ 𝓟 S),
      Continuous[Pi.topologicalSpace, inst✝¹] (f ∘ Pi.map fun x ↦ inclusion (A x) (C x) hS)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace

Goal state before:
pp: ι : Type u_1
R : ι → Type u_2
A : (i : ι) → Set (R i)
𝓕✝ 𝓖 : Filter ι
S : ι → Type u_3
inst✝⁴ : (i : ι) → SetLike (S i) (R i)
B : (i : ι) → S i
T : Set ι
𝓕 : Filter ι
inst✝³ : (i : ι) → TopologicalSpace (R i)
inst✝² : (i : ι) → Inv (R i)
inst✝¹ : ∀ (i : ι), InvMemClass (S i) (R i)
inst✝ : ∀ (i : ι), ContinuousInv (R i)
⊢ Continuous[topologicalSpace R (fun i ↦ ↑(B i)) 𝓕, topologicalSpace R (fun i ↦ ↑(B i)) 𝓕] fun a ↦ a⁻¹

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace

Goal state before:
pp: ι : Type u_1
R : ι → Type u_2
A : (i : ι) → Set (R i)
𝓕✝ 𝓖 : Filter ι
S : ι → Type u_3
inst✝⁴ : (i : ι) → SetLike (S i) (R i)
B : (i : ι) → S i
T : Set ι
𝓕 : Filter ι
inst✝³ : (i : ι) → TopologicalSpace (R i)
G : Type u_4
inst✝² : (i : ι) → SMul G (R i)
inst✝¹ : ∀ (i : ι), SMulMemClass (S i) G (R i)
inst✝ : ∀ (i : ι), ContinuousConstSMul G (R i)
g : G
⊢ Continuous[topologicalSpace R (fun i ↦ ↑(B i)) 𝓕, topologicalSpace R (fun i ↦ ↑(B i)) 𝓕] fun x ↦ g • x

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace

Goal state before:
pp: ι : Type u_1
R : ι → Type u_2
A : (i : ι) → Set (R i)
𝓕✝ 𝓖 : Filter ι
S : ι → Type u_3
inst✝⁴ : (i : ι) → SetLike (S i) (R i)
B : (i : ι) → S i
T : Set ι
𝓕 : Filter ι
inst✝³ : (i : ι) → TopologicalSpace (R i)
hBopen : Fact (∀ (i : ι), IsOpen[inst✝³ i] ↑(B i))
inst✝² : (i : ι) → Mul (R i)
inst✝¹ : ∀ (i : ι), MulMemClass (S i) (R i)
inst✝ : ∀ (i : ι), ContinuousMul (R i)
⊢ Continuous[instTopologicalSpaceProd, topologicalSpace R (fun i ↦ ↑(B i)) cofinite] fun p ↦ p.1 * p.2

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Multiplicity

Goal state before:
pp: x y p : ℕ
hp : Fact (Nat.Prime p)
hp1 : Odd p
hxy : p ∣ x + y
hx : ¬p ∣ x
n : ℕ
hn : Odd n
⊢ padicValNat p (x ^ n + y ^ n) = padicValNat p (x + y) + padicValNat p n

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace

Goal state before:
pp: ι : Type u_1
R : ι → Type u_2
A : (i : ι) → Set (R i)
𝓕✝ 𝓖 : Filter ι
S : ι → Type u_3
inst✝⁵ : (i : ι) → SetLike (S i) (R i)
B : (i : ι) → S i
T : Set ι
𝓕 : Filter ι
inst✝⁴ : (i : ι) → TopologicalSpace (R i)
hBopen : Fact (∀ (i : ι), IsOpen[inst✝⁴ i] ↑(B i))
G : Type u_4
inst✝³ : TopologicalSpace G
inst✝² : (i : ι) → SMul G (R i)
inst✝¹ : ∀ (i : ι), SMulMemClass (S i) G (R i)
inst✝ : ∀ (i : ι), ContinuousSMul G (R i)
⊢ Continuous[instTopologicalSpaceProd, topologicalSpace R (fun i ↦ ↑(B i)) cofinite] fun p ↦ p.1 • p.2

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace

Goal state before:
pp: ι : Type u_1
R : ι → Type u_2
A : (i : ι) → Set (R i)
𝓕✝ 𝓖 : Filter ι
S : ι → Type u_3
inst✝⁴ : (i : ι) → SetLike (S i) (R i)
B : (i : ι) → S i
T : Set ι
𝓕 : Filter ι
inst✝³ : (i : ι) → TopologicalSpace (R i)
hBopen : Fact (∀ (i : ι), IsOpen[inst✝³ i] ↑(B i))
inst✝² : (i : ι) → Group (R i)
inst✝¹ : ∀ (i : ι), SubgroupClass (S i) (R i)
inst✝ : ∀ (i : ι), IsTopologicalGroup (R i)
hAcompact : ∀ (i : ι), CompactSpace ↥(B i)
i : ι
x : R i
⊢ x ∈ x • ↑(B i)

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.NumberField.Units.Regulator

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ Fintype.card (Fin (rank K)) = Fintype.card { w // w ≠ w₀ }

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.NumberField.Units.Regulator

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
u : Fin (rank K) → (𝓞 K)ˣ
hu : IsMaxRank u
i : Fin (rank K)
⊢ (basisOfIsMaxRank hu) i = (logEmbedding K) (Additive.ofMul (u i))

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace

Goal state before:
pp: ι₁ : Type u_3
ι₂ : Type u_4
R₁ : ι₁ → Type u_5
R₂ : ι₂ → Type u_6
inst✝¹ : (i : ι₁) → TopologicalSpace (R₁ i)
inst✝ : (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✝ j] (φ j)
S : Set ι₁
hS : 𝓕₁ ≤ 𝓟 S
T : Set ι₂ := f ⁻¹' S ∩ {j | MapsTo (φ j) (A₁ (f j)) (A₂ j)}
⊢ 𝓕₂ ≤ 𝓟 T

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace

Goal state before:
pp: ι₁ : Type u_3
ι₂ : Type u_4
R₁ : ι₁ → Type u_5
R₂ : ι₂ → Type u_6
inst✝¹ : (i : ι₁) → TopologicalSpace (R₁ i)
inst✝ : (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✝ j] (φ j)
S : Set ι₁
hS : 𝓕₁ ≤ 𝓟 S
T : Set ι₂ := f ⁻¹' S ∩ {j | MapsTo (φ j) (A₁ (f j)) (A₂ j)}
hT : 𝓕₂ ≤ 𝓟 T
⊢ Tendsto f (𝓟 T) (𝓟 S)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace

Goal state before:
pp: ι₁ : Type u_3
ι₂ : Type u_4
R₁ : ι₁ → Type u_5
R₂ : ι₂ → Type u_6
inst✝¹ : (i : ι₁) → TopologicalSpace (R₁ i)
inst✝ : (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✝ j] (φ j)
S : Set ι₁
hS : 𝓕₁ ≤ 𝓟 S
T : Set ι₂ := f ⁻¹' S ∩ {j | MapsTo (φ j) (A₁ (f j)) (A₂ j)}
hT : 𝓕₂ ≤ 𝓟 T
hf' : Tendsto f (𝓟 T) (𝓟 S)
⊢ ∀ᶠ (j : ι₂) in 𝓟 T, MapsTo (φ j) (A₁ (f j)) (A₂ j)

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.NumberField.Units.Regulator

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
u : Fin (rank K) → (𝓞 K)ˣ
hu : IsMaxRank u
⊢ (span ℤ (Set.range ⇑(basisOfIsMaxRank hu))).toAddSubgroup =
    AddSubgroup.map (logEmbedding K) (Subgroup.toAddSubgroup (Subgroup.closure (Set.range u)))

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace

Goal state before:
pp: ι₁ : Type u_3
ι₂ : Type u_4
R₁ : ι₁ → Type u_5
R₂ : ι₂ → Type u_6
inst✝¹ : (i : ι₁) → TopologicalSpace (R₁ i)
inst✝ : (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✝ j] (φ j)
⊢ Continuous[topologicalSpace R₁ A₁ 𝓕₁, topologicalSpace R₂ A₂ 𝓕₂] (mapAlong R₁ R₂ f hf φ hφ)

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.NumberField.Units.Regulator

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
s : Subgroup (𝓞 K)ˣ
⊢ s.FiniteIndex ↔ (s ⊔ torsion K).FiniteIndex

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ Measurable ↑(polarCoordReal K).symm

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : realMixedSpace K
⊢ HasFDerivAt (↑(polarCoordReal K).symm) (FDerivPolarCoordRealSymm K x) x

Tactic:
by

Goal state after: