mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Tactic.NormNum.PowMod

Goal state before:
pp: a✝ b✝ m✝ : Q(ℕ)
depth : ℕ
a m b₀ c₀ b : Q(ℕ)
p : Q(Prop)
hp : «$p» =Q ((«$a».pow «$b₀»).mod «$m» = «$c₀»)
b' : ℕ := Expr.natLit! b
m' : ℕ := Expr.natLit! m
d : ℕ := depth >>> 1
hi : Q(ℕ)
⊢ «$p» =Q ((«$a».pow «$b₀»).mod «$m» = «$c₀»)

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.NormNum.Irrational

Goal state before:
pp: x : ℝ
num den num_k : ℕ
hx_isNNRat : IsNNRat x num den
hx_coprime : num.Coprime den
hn1 : num_k ^ 2 < num
hn2 : num < (num_k + 1) ^ 2
⊢ Irrational √x

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.NormNum.Irrational

Goal state before:
pp: x : ℝ
num den den_k : ℕ
hx_isNNRat : IsNNRat x num den
hx_coprime : num.Coprime den
hd1 : den_k ^ 2 < den
hd2 : den < (den_k + 1) ^ 2
⊢ Nat.Coprime 1 2

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.NormNum.Irrational

Goal state before:
pp: x : ℝ
num den den_k : ℕ
hx_isNNRat : IsNNRat x num den
hx_coprime : num.Coprime den
hd1 : den_k ^ 2 < den
hd2 : den < (den_k + 1) ^ 2
⊢ 1 / 2 * ↑2 = 1

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.NormNum.Irrational

Goal state before:
pp: x : ℝ
num den den_k : ℕ
hx_isNNRat : IsNNRat x num den
hx_coprime : num.Coprime den
hd1 : den_k ^ 2 < den
hd2 : den < (den_k + 1) ^ 2
⊢ ↑2 * (1 / 2) = 1

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.NormNum.Irrational

Goal state before:
pp: x : ℝ
num den den_k : ℕ
hx_isNNRat : IsNNRat x num den
hx_coprime : num.Coprime den
hd1 : den_k ^ 2 < den
hd2 : den < (den_k + 1) ^ 2
⊢ 1 / 2 = ↑1 * ⅟↑2

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.NormNum.Irrational

Goal state before:
pp: x : ℝ
num den den_k : ℕ
hx_isNNRat : IsNNRat x num den
hx_coprime : num.Coprime den
hd1 : den_k ^ 2 < den
hd2 : den < (den_k + 1) ^ 2
⊢ Irrational √x

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.NormNum.Irrational

Goal state before:
pp: x : ℝ
n k : ℕ
hx_isNat : IsNat x n
hn1 : k ^ 2 < n
hn2 : n < (k + 1) ^ 2
⊢ n.Coprime 1

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.PNatToNat

Goal state before:
pp: m n : ℕ+
⊢ m = n ↔ ↑m = ↑n

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.PNatToNat

Goal state before:
pp: m n : ℕ+
⊢ m ≤ n ↔ ↑m ≤ ↑n

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.PNatToNat

Goal state before:
pp: m n : ℕ+
⊢ m < n ↔ ↑m < ↑n

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.PNatToNat

Goal state before:
pp: a b : ℕ+
⊢ ↑(a - b) = ↑a - 1 - ↑b + 1

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.NormNum.RealSqrt

Goal state before:
pp: x : ℝ
nx ny : ℕ
h : IsNat x nx
hy : ny * ny = nx
⊢ √x = ↑ny

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.NormNum.RealSqrt

Goal state before:
pp: x : ℝ≥0
nx ny : ℕ
h : IsNat x nx
hy : ny * ny = nx
⊢ sqrt x = ↑ny

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.NormNum.RealSqrt

Goal state before:
pp: x : ℝ≥0
n sn d sd : ℕ
hn : sn * sn = n
hd : sd * sd = d
h : IsNNRat x n d
⊢ IsNNRat (sqrt x) sn sd

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.NormNum.RealSqrt

Goal state before:
pp: x : ℝ
nx : ℕ
h : IsInt x (Int.negOfNat nx)
⊢ √x = ↑0

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.NormNum.RealSqrt

Goal state before:
pp: x : ℝ
num denom : ℕ
h : IsRat x (Int.negOfNat num) denom
⊢ IsNat (√x) 0

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.NormNum.RealSqrt

Goal state before:
pp: x : ℝ
n sn d sd : ℕ
hn : sn * sn = n
hd : sd * sd = d
h : IsNNRat x n d
⊢ IsNNRat (√x) sn sd

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.Polynomial.Basic

Goal state before:
pp: R : Type u_2
inst✝ : CommSemiring R
a : R
n : ℕ
⊢ (Polynomial.monomial n) a = a • Polynomial.X ^ n

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.Polynomial.Basic

Goal state before:
pp: R : Type u_2
A : Type u_3
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
r : R
⊢ Polynomial.map (algebraMap R A) ((algebraMap R (Polynomial R)) r) = (algebraMap A (Polynomial A)) ((algebraMap R A) r)

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.ReduceModChar

Goal state before:
pp: e' r : ℤ
α : Type u_1
inst✝ : Ring α
n n' : ℕ
inst : CharP α n
e : α
he : IsInt e e'
hn : IsNat n n'
h₂ : IsInt (e' % ↑n') r
⊢ e = ↑r

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.ReduceModChar

Goal state before:
pp: α : Type u_1
inst✝ : Semiring α
a✝ : α
a b n : ℕ
x✝ : CharP α ↑n
h : a✝ = ↑a
⊢ a✝ ^ ↑b = ↑((a.pow b).mod n)

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.ReduceModChar

Goal state before:
pp: α : Type u_1
inst✝ : Ring α
n : ℕ
inst : CharP α n
b : α
a : ℕ
a' : α
p : IsNat (↑n - 1) a
pa : ↑a = a'
⊢ -b = a' * b

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.ReduceModChar

Goal state before:
pp: α : Type u_1
inst✝ : Ring α
n : ℕ
inst : CharP α n
a b : α
na : ℕ
na' : α
p : IsNat ((↑n - 1) * a) na
pa : ↑na = na'
⊢ -(a * b) = na' * b

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.Sat.FromLRAT

Goal state before:
pp: p : Prop
as ps as₁ : List Prop
⊢ as = as₁.reverseAux ps → (mk as).implies p ps as₁.length → p

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.Simproc.Factors

Goal state before:
pp: n m a b : ℕ
l : List ℕ
h₁ : IsNat (b * m) n
h₂ : a ≤ b
h₃ : b.minFac = b
H : FactorsHelper m b l
pa : Nat.Prime a
pb : Nat.Prime b
f₁ : List.IsChain (fun x1 x2 ↦ x1 ≤ x2) (b :: l)
f₂ : ∀ (a : ℕ), a ∈ l → Nat.Prime a
f₃ : l.prod = m
⊢ (b :: l).prod = n

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.Sat.FromLRAT

Goal state before:
pp: v : Valuation
f₁ : Fmla
a : Prop
f₂ : Fmla
b : Prop
h₁ : reify v f₁ a
h₂ : reify v f₂ b
⊢ reify v (f₁.and f₂) (a ∨ b)

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.Simproc.Factors

Goal state before:
pp: en enl ea eal : Q(ℕ)
ehn : Q(IsNat «$en» «$enl»)
eha : Q(IsNat «$ea» «$eal»)
n : ℕ := Expr.natLit! enl
__x✝¹ : PLift (0 < n)
hn0 : 0 < n
a : ℕ := Expr.natLit! eal
b : ℕ := n.minFac
__x✝ : PLift (a ≤ b)
hab : a ≤ b
h_bn : b < n
m : ℕ := n / b
em : Q(ℕ)
ehm : Q(IsNat (OfNat.ofNat «$em») «$em»)
h_ba_eq : b = a
⊢ a * m = n

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.Simproc.Factors

Goal state before:
pp: en enl ea eal : Q(ℕ)
ehn : Q(IsNat «$en» «$enl»)
eha : Q(IsNat «$ea» «$eal»)
n : ℕ := Expr.natLit! enl
__x✝¹ : PLift (0 < n)
hn0 : 0 < n
a : ℕ := Expr.natLit! eal
b : ℕ := n.minFac
__x✝ : PLift (a ≤ b)
hab : a ≤ b
h_bn : ¬b < n
hbn_eq : b = n
hba : ¬b = a
⊢ a < n

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.Simproc.FinsetInterval

Goal state before:
pp: m n : ℕ
hnm : n.blt m = true
⊢ Icc m n = ∅

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.Simproc.FinsetInterval

Goal state before:
pp: m n : ℕ
s : Finset ℕ
hmn : m.ble n = true
hs : Icc (m + 1) n = s
⊢ m ≤ n

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.Simproc.FinsetInterval

Goal state before:
pp: m n : ℕ
s : Finset ℕ
hmn : m.ble n = true
hs : Icc (m + 1) n = s
⊢ Icc m n = insert m s

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.Simproc.FinsetInterval

Goal state before:
pp: m n : ℕ
s : Finset ℕ
hs : Icc m n = s
⊢ Ico m (n + 1) = s

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.Simproc.FinsetInterval

Goal state before:
pp: m : ℕ
⊢ Ico m 0 = ∅

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.Simproc.FinsetInterval

Goal state before:
pp: m n : ℕ
s : Finset ℕ
hs : Icc (m + 1) n = s
⊢ Ioc m n = s

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.Simproc.FinsetInterval

Goal state before:
pp: m n : ℕ
s : Finset ℕ
hs : Icc (m + 1) n = s
⊢ Ioc m n = s

Tactic:
by
  rw [← hs, Icc_add_one_left_eq_Ioc]

Goal state after:
Module: Mathlib.Tactic.Simproc.FinsetInterval

Goal state before:
pp: m n : ℕ
s : Finset ℕ
hs : Icc (m + 1) (n - 1) = s
⊢ Ioo m n = s

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.Simproc.FinsetInterval

Goal state before:
pp: n : ℕ
s : Finset ℕ
hs : Icc 0 n = s
⊢ Iio (n + 1) = s

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.Simproc.FinsetInterval

Goal state before:
pp: ⊢ Iio 0 = ∅

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.Simproc.FinsetInterval

Goal state before:
pp: m n : ℤ
hnm : n < m
⊢ Icc m n = ∅

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.Simproc.FinsetInterval

Goal state before:
pp: m n : ℤ
s : Finset ℤ
hmn : m ≤ n
hs : Icc (m + 1) n = s
⊢ m ≤ n

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.Simproc.FinsetInterval

Goal state before:
pp: m n : ℤ
s : Finset ℤ
hmn : m ≤ n
hs : Icc (m + 1) n = s
⊢ Icc m n = insert m s

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.Simproc.FinsetInterval

Goal state before:
pp: m n : ℤ
s : Finset ℤ
hs : Icc m (n - 1) = s
⊢ Ico m n = s

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.Simproc.FinsetInterval

Goal state before:
pp: m n : ℤ
s : Finset ℤ
hs : Icc (m + 1) n = s
⊢ Ioc m n = s

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.Simproc.FinsetInterval

Goal state before:
pp: m n : ℤ
s : Finset ℤ
hs : Icc (m + 1) n = s
⊢ Ioc m n = s

Tactic:
by
  rw [← hs, Icc_add_one_left_eq_Ioc]

Goal state after:
Module: Mathlib.Tactic.Simproc.FinsetInterval

Goal state before:
pp: m n : ℤ
s : Finset ℤ
hs : Icc (m + 1) (n - 1) = s
⊢ Ioo m n = s

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.Simproc.FinsetInterval

Goal state before:
pp: ⊢ Icc 1 0 = ∅

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.Simproc.FinsetInterval

Goal state before:
pp: ⊢ Icc 1 1 = {1}

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.Simproc.FinsetInterval

Goal state before:
pp: ⊢ Icc 1 2 = {1, 2}

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.Simproc.FinsetInterval

Goal state before:
pp: ⊢ Ico 1 1 = ∅

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.Simproc.FinsetInterval

Goal state before:
pp: ⊢ Ico 1 2 = {1}

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.Simproc.FinsetInterval

Goal state before:
pp: ⊢ Ico 1 3 = {1, 2}

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.Simproc.FinsetInterval

Goal state before:
pp: ⊢ Ioc 1 1 = ∅

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.Simproc.FinsetInterval

Goal state before:
pp: ⊢ Ioc 1 2 = {2}

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.Simproc.FinsetInterval

Goal state before:
pp: ⊢ Ioc 1 3 = {2, 3}

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.Simproc.FinsetInterval

Goal state before:
pp: ⊢ Ioo 1 2 = ∅

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.Simproc.FinsetInterval

Goal state before:
pp: ⊢ Ioo 1 3 = {2}

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.Simproc.FinsetInterval

Goal state before:
pp: ⊢ Ioo 1 4 = {2, 3}

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.Simproc.FinsetInterval

Goal state before:
pp: ⊢ Iic 0 = {0}

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.Simproc.FinsetInterval

Goal state before:
pp: ⊢ Iic 1 = {0, 1}

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.Simproc.FinsetInterval

Goal state before:
pp: ⊢ Iic 2 = {0, 1, 2}

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.Simproc.FinsetInterval

Goal state before:
pp: ⊢ Iio 1 = {0}

Tactic:
by

Goal state after:
Module: Mathlib.Tactic.Simproc.FinsetInterval

Goal state before:
pp: ⊢ Iio 2 = {0, 1}

Tactic:
by

Goal state after:
Module: Mathlib.Testing.Plausible.Sampleable

Goal state before:
pp: ⊢ SampleableExt Rat

Tactic:
by

Goal state after:
Module: Mathlib.Testing.Plausible.Sampleable

Goal state before:
pp: ⊢ SampleableExt ℕ+

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.Algebra.Rat

Goal state before:
pp: A : Type u_1
inst✝³ : DivisionRing A
inst✝² : TopologicalSpace A
inst✝¹ : SeparatelyContinuousMul A
inst✝ : CharZero A
r : ℚ
⊢ Continuous fun x ↦ r • x

Tactic:
by

Goal state after:
Module: Mathlib.Testing.Plausible.Functions

Goal state before:
pp: α : Type u
β : Type v
inst✝ : DecidableEq α
m : List ((_ : α) × β)
y : β
x : α
⊢ (withDefault m y).apply x = (List.dlookup x m).getD y

Tactic:
by

Goal state after:
Module: Mathlib.Testing.Plausible.Functions

Goal state before:
pp: α : Type u
β : Type v
inst✝² : DecidableEq α
inst✝¹ : Zero β
inst✝ : DecidableEq β
tf : TotalFunction α β
⊢ ∀ (a : α), a ∈ tf.zeroDefaultSupp ↔ tf.zeroDefault.apply a ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.Testing.Plausible.Functions

Goal state before:
pp: α : Type u
inst✝ : DecidableEq α
xs : List (α × α)
x y z : α
⊢ applyId ((y, z) :: xs) x = if y = x then z else applyId xs x

Tactic:
by

Goal state after:
Module: Mathlib.Testing.Plausible.Functions

Goal state before:
pp: α : Type u
inst✝ : DecidableEq α
xs ys : List α
h₀ : xs.Nodup
h₁ : xs.length = ys.length
x y : α
i : ℕ
h₂ : xs[i]? = some x
⊢ applyId (xs.zip ys) x = y ↔ ys[i]? = some y

Tactic:
by

Goal state after:
Module: Mathlib.Testing.Plausible.Functions

Goal state before:
pp: α : Type u
inst✝ : DecidableEq α
x val x' : α
xs : List α
y : α
ys : List α
xs_ih : val ∈ ys ↔ x ∈ xs
h₁ : (x' :: xs).length = (y :: ys).length
h : ¬x' = x
h₃ : dlookup x (map Prod.toSigma (xs.zip ys)) = some val
h₅ : List.Pairwise (fun x1 x2 ↦ x1 ≠ x2) xs
h₀ : ∀ a' ∈ xs, x' ≠ a'
h₄ : List.Pairwise (fun x1 x2 ↦ x1 ≠ x2) ys
h₂ : ∀ a' ∈ ys, y ≠ a'
h₆ : xs.length = ys.length
this : val ∈ ys
⊢ val = y ∨ x ∈ xs ↔ False ∨ x ∈ xs

Tactic:
by

Goal state after:
Module: Mathlib.Testing.Plausible.Functions

Goal state before:
pp: α : Type u
inst✝ : DecidableEq α
xs ys : List α
h₀ : xs.Nodup
h₁ : xs ~ ys
x : α
⊢ List.applyId (xs.zip ys) x ∈ ys ↔ x ∈ xs

Tactic:
by

Goal state after:
Module: Mathlib.Topology.UniformSpace.Ascoli

Goal state before:
pp: ι : Type u_1
X : Type u_2
α : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : UniformSpace α
F : ι → X → α
inst✝ : CompactSpace X
F_eqcont : Equicontinuous F
U : Set (α × α)
hU : U ∈ 𝓤 α
V : Set (α × α)
hV : V ∈ 𝓤 α
Vsymm : SetRel.IsSymm V
hVU : (SetRel.comp V V).comp V ⊆ U
Ω : X → Set X := fun x ↦ {y | ∀ (i : ι), (F i x, F i y) ∈ V}
A : Finset X
Acover : ⋃ x ∈ A, Ω x = ⊤
⊢ ⋂ a ∈ A, {ij | (F ij.1 a, F ij.2 a) ∈ V} ⊆ Prod.map F F ⁻¹' UniformFun.gen X α U

Tactic:
by

Goal state after:
Module: Mathlib.Testing.Plausible.Functions

Goal state before:
pp: α : Type u
inst✝ : DecidableEq α
xs ys : List α
x : α
⊢ x ∉ xs → applyId (xs.zip ys) x = x

Tactic:
by

Goal state after:
Module: Mathlib.Topology.UniformSpace.Ascoli

Goal state before:
pp: ι : Type u_1
X : Type u_2
α : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : UniformSpace α
F : ι → X → α
inst✝ : CompactSpace X
F_eqcont : Equicontinuous F
⊢ UniformSpace.comap F (UniformFun.uniformSpace X α) = UniformSpace.comap F (Pi.uniformSpace fun i ↦ α)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.UniformSpace.Ascoli

Goal state before:
pp: ι : Type u_1
X : Type u_2
α : Type u_3
inst✝³ : TopologicalSpace X
inst✝² : UniformSpace α
F : ι → X → α
inst✝¹ : UniformSpace ι
inst✝ : CompactSpace X
F_eqcont : Equicontinuous F
⊢ IsUniformInducing (⇑UniformFun.ofFun ∘ F) ↔ IsUniformInducing F

Tactic:
by

Goal state after:
Module: Mathlib.Topology.UniformSpace.Ascoli

Goal state before:
pp: ι : Type u_1
X : Type u_2
α : Type u_3
inst✝³ : TopologicalSpace X
inst✝² : UniformSpace α
F : ι → X → α
inst✝¹ : TopologicalSpace ι
inst✝ : CompactSpace X
F_eqcont : Equicontinuous F
⊢ IsInducing (⇑UniformFun.ofFun ∘ F) ↔ IsInducing F

Tactic:
by

Goal state after:
Module: Mathlib.Testing.Plausible.Functions

Goal state before:
pp: α : Type u
inst✝ : DecidableEq α
xs ys : List α
h₀ : xs.Nodup
h₁ : xs ~ ys
x y : α
h : List.applyId (xs.zip ys) x = List.applyId (xs.zip ys) y
i : ℕ
hx : xs[i]? = some x
j : ℕ
hy : xs[j]? = some y
this : some x = some y
⊢ x = y

Tactic:
by

Goal state after:
Module: Mathlib.Topology.UniformSpace.Ascoli

Goal state before:
pp: ι : Type u_1
X : Type u_2
α : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : UniformSpace α
F : ι → X → α
inst✝ : CompactSpace X
F_eqcont : Equicontinuous F
ℱ : Filter ι
f : X → α
ℱ_ne : ℱ.NeBot
H : Tendsto F ℱ (𝓝 f)
S : Set (X → α) := closure[Pi.topologicalSpace] (range F)
𝒢 : Filter ↑S := comap Subtype.val (map F ℱ)
⊢ Equicontinuous (id ∘ Subtype.val)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.UniformSpace.Ascoli

Goal state before:
pp: ι : Type u_1
X : Type u_2
α : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : UniformSpace α
F : ι → X → α
inst✝ : CompactSpace X
F_eqcont : Equicontinuous F
ℱ : Filter ι
f : X → α
ℱ_ne : ℱ.NeBot
H : Tendsto F ℱ (𝓝 f)
S : Set (X → α) := closure[Pi.topologicalSpace] (range F)
𝒢 : Filter ↑S := comap Subtype.val (map F ℱ)
hS : S.Equicontinuous
ind : IsInducing (⇑UniformFun.ofFun ∘ Subtype.val)
f_mem : f ∈ S
h𝒢ℱ : map Subtype.val 𝒢 = map F ℱ
⊢ Tendsto id 𝒢 (𝓝 ⟨f, f_mem⟩)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.UniformSpace.Ascoli

Goal state before:
pp: ι : Type u_1
X : Type u_2
α : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : UniformSpace α
F : ι → X → α
inst✝ : CompactSpace X
F_eqcont : Equicontinuous F
ℱ : Filter ι
f : X → α
⊢ Tendsto (⇑UniformFun.ofFun ∘ F) ℱ (𝓝 (UniformFun.ofFun f)) ↔ Tendsto F ℱ (𝓝 f)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.UniformSpace.Ascoli

Goal state before:
pp: ι : Type u_1
X : Type u_2
α : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : UniformSpace α
F : ι → X → α
𝔖 : Set (Set X)
𝔖_compact : ∀ K ∈ 𝔖, IsCompact K
F_eqcont : ∀ K ∈ 𝔖, EquicontinuousOn F K
⊢ ⨅ i ∈ 𝔖,
      UniformSpace.comap (((fun x ↦ x) ∘ i.domRestrict ∘ ⇑(UniformOnFun.toFun 𝔖)) ∘ F)
        (UniformFun.uniformSpace (↑i) α) =
    ⨅ K ∈ 𝔖, UniformSpace.comap (K.domRestrict ∘ F) (UniformFun.uniformSpace (↑K) α)

Tactic:
UniformOnFun.toFun,

Goal state after:
ι : Type u_1
X : Type u_2
α : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : UniformSpace α
F : ι → X → α
𝔖 : Set (Set X)
𝔖_compact : ∀ K ∈ 𝔖, IsCompact K
F_eqcont : ∀ K ∈ 𝔖, EquicontinuousOn F K
⊢ ⨅ i ∈ 𝔖,
      UniformSpace.comap (((fun x ↦ x) ∘ i.domRestrict ∘ ⇑(UniformOnFun.ofFun 𝔖).symm) ∘ F)
        (UniformFun.uniformSpace (↑i) α) =
    ⨅ K ∈ 𝔖, UniformSpace.comap (K.domRestrict ∘ F) (UniformFun.uniformSpace (↑K) α)
Module: Mathlib.Topology.UniformSpace.Ascoli

Goal state before:
pp: ι : Type u_1
X : Type u_2
α : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : UniformSpace α
F : ι → X → α
𝔖 : Set (Set X)
𝔖_compact : ∀ K ∈ 𝔖, IsCompact K
F_eqcont : ∀ K ∈ 𝔖, EquicontinuousOn F K
⊢ UniformSpace.comap F (UniformOnFun.uniformSpace X α 𝔖) =
    ⨅ K ∈ 𝔖, UniformSpace.comap (K.domRestrict ∘ F) (UniformFun.uniformSpace (↑K) α)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.UniformSpace.Ascoli

Goal state before:
pp: ι : Type u_1
X : Type u_2
α : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : UniformSpace α
F : ι → X → α
𝔖 : Set (Set X)
𝔖_compact : ∀ K ∈ 𝔖, IsCompact K
F_eqcont : ∀ K ∈ 𝔖, EquicontinuousOn F K
H1 :
  UniformSpace.comap F (UniformOnFun.uniformSpace X α 𝔖) =
    ⨅ K ∈ 𝔖, UniformSpace.comap (K.domRestrict ∘ F) (UniformFun.uniformSpace (↑K) α)
⊢ UniformSpace.comap ((⋃₀ 𝔖).domRestrict ∘ F) (Pi.uniformSpace fun i ↦ α) =
    ⨅ K ∈ 𝔖, UniformSpace.comap (K.domRestrict ∘ F) (Pi.uniformSpace fun i ↦ α)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.UniformSpace.Ascoli

Goal state before:
pp: ι : Type u_1
X : Type u_2
α : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : UniformSpace α
F : ι → X → α
𝔖 : Set (Set X)
𝔖_compact : ∀ K ∈ 𝔖, IsCompact K
F_eqcont : ∀ K ∈ 𝔖, EquicontinuousOn F K
H1 :
  UniformSpace.comap F (UniformOnFun.uniformSpace X α 𝔖) =
    ⨅ K ∈ 𝔖, UniformSpace.comap (K.domRestrict ∘ F) (UniformFun.uniformSpace (↑K) α)
H2 :
  UniformSpace.comap ((⋃₀ 𝔖).domRestrict ∘ F) (Pi.uniformSpace fun i ↦ α) =
    ⨅ K ∈ 𝔖, UniformSpace.comap (K.domRestrict ∘ F) (Pi.uniformSpace fun i ↦ α)
K : Set X
hK : K ∈ 𝔖
⊢ UniformSpace.comap (K.domRestrict ∘ F) (UniformFun.uniformSpace (↑K) α) =
    UniformSpace.comap (K.domRestrict ∘ F) (Pi.uniformSpace fun i ↦ α)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.Group.CompactOpen

Goal state before:
pp: A : Type u_2
B : Type u_3
inst✝³ : Monoid A
inst✝² : Monoid B
inst✝¹ : TopologicalSpace A
inst✝ : TopologicalSpace B
⊢ Set.range toContinuousMap = {f | f 1 = 1 ∧ ∀ (x y : A), f (x * y) = f x * f y}

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.Group.CompactOpen

Goal state before:
pp: A : Type u_2
B : Type u_3
inst✝⁵ : Monoid A
inst✝⁴ : Monoid B
inst✝³ : TopologicalSpace A
inst✝² : TopologicalSpace B
inst✝¹ : ContinuousMul B
inst✝ : T2Space B
⊢ IsClosed (Set.range toContinuousMap)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.UniformSpace.Ascoli

Goal state before:
pp: ι : Type u_1
X : Type u_2
α : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : UniformSpace α
F : ι → X → α
𝔖 : Set (Set X)
𝔖_compact : ∀ K ∈ 𝔖, IsCompact K
F_eqcont : ∀ K ∈ 𝔖, EquicontinuousOn F K
⊢ UniformSpace.comap F (UniformOnFun.uniformSpace X α 𝔖) =
    UniformSpace.comap ((⋃₀ 𝔖).domRestrict ∘ F) (Pi.uniformSpace fun i ↦ α)

Tactic:
by

Goal state after:
Module: Mathlib.Testing.Plausible.Functions

Goal state before:
pp: α : Type u
inst✝ : DecidableEq α
xs ys : List α
h₀ : xs.Nodup
h₁ : xs ~ ys
⊢ Injective (List.applyId (xs.zip ys))

Tactic:
by

Goal state after:
Module: Mathlib.Testing.Plausible.Functions

Goal state before:
pp: α : Type u
β : Type v
x✝ : ℕ
n : ℕ := x✝
h : 0 < n
⊢ 1 < 2

Tactic:
by

Goal state after:
Module: Mathlib.Testing.Plausible.Functions

Goal state before:
pp: α✝ : Type u
β : Type v
α : Type
inst✝ : DecidableEq α
xs✝ : List ((_ : α) × α)
h₀✝ : map Sigma.fst xs✝ ~ map Sigma.snd xs✝
h₁✝ : (map Sigma.snd xs✝).Nodup
xs' ys' : List α
h₀ : xs' ~ ys'
h₁ : ys'.Nodup
h₃ : xs'.length ≤ ys'.length
h₄ : ys'.length ≤ xs'.length
⊢ map Sigma.fst (map Prod.toSigma (xs'.zip ys')) ~ map Sigma.snd (map Prod.toSigma (xs'.zip ys'))

Tactic:
by

Goal state after:
Module: Mathlib.Testing.Plausible.Functions

Goal state before:
pp: α✝ : Type u
β : Type v
α : Type
inst✝ : DecidableEq α
xs✝ : List ((_ : α) × α)
h₀✝ : map Sigma.fst xs✝ ~ map Sigma.snd xs✝
h₁✝ : (map Sigma.snd xs✝).Nodup
xs' ys' : List α
h₀ : xs' ~ ys'
h₁ : ys'.Nodup
h₃ : xs'.length ≤ ys'.length
h₄ : ys'.length ≤ xs'.length
⊢ (map Sigma.snd (map Prod.toSigma (xs'.zip ys'))).Nodup

Tactic:
by

Goal state after:
Module: Mathlib.Testing.Plausible.Functions

Goal state before:
pp: α : Type u
β : Type v
xs ys : List α
h : xs ~ ys
h' : ys.Nodup
h₀ : xs.length ≤ ys.length
h₁ : ys.length ≤ xs.length
⊢ map Sigma.fst (List.toFinmap' (xs.zip ys)) ~ map Sigma.snd (List.toFinmap' (xs.zip ys))

Tactic:
by

Goal state after:
Module: Mathlib.Testing.Plausible.Functions

Goal state before:
pp: α : Type u
β : Type v
xs ys : List α
h : xs ~ ys
h' : ys.Nodup
h₀ : xs.length ≤ ys.length
h₁ : ys.length ≤ xs.length
⊢ (map Sigma.snd (List.toFinmap' (xs.zip ys))).Nodup

Tactic:
by

Goal state after:
Module: Mathlib.Topology.UniformSpace.Ascoli

Goal state before:
pp: ι : Type u_1
X : Type u_2
α : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : UniformSpace α
F : ι → X → α
inst✝ : UniformSpace ι
𝔖 : Set (Set X)
𝔖_compact : ∀ K ∈ 𝔖, IsCompact K
F_eqcont : ∀ K ∈ 𝔖, EquicontinuousOn F K
⊢ IsUniformInducing (⇑(UniformOnFun.ofFun 𝔖) ∘ F) ↔ IsUniformInducing ((⋃₀ 𝔖).domRestrict ∘ F)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.Group.CompactOpen

Goal state before:
pp: X : Type u_7
Y : Type u_8
inst✝⁷ : TopologicalSpace X
inst✝⁶ : Group X
inst✝⁵ : IsTopologicalGroup X
inst✝⁴ : UniformSpace Y
inst✝³ : CommGroup Y
inst✝² : IsUniformGroup Y
inst✝¹ : T0Space Y
inst✝ : CompactSpace Y
U : Set X
V : Set Y
hU : IsCompact U
hV : V ∈ 𝓝 1
W : Set Y
hWo : W ∈ 𝓝 1
hWV : W ⊆ V
hWc : IsCompact W
S1 : Set (X →* Y) := {f | Set.MapsTo (⇑f) U W}
S2 : Set (X →ₜ* Y) := {f | Set.MapsTo (⇑f) U W}
S3 : Set C(X, Y) := _root_.toContinuousMap '' S2
S4 : Set (X → Y) := DFunLike.coe '' S3
h : Equicontinuous fun x ↦ ⇑↑x
⊢ S4 = DFunLike.coe '' S1

Tactic:
by

Goal state after:
Module: Mathlib.Testing.Plausible.Functions

Goal state before:
pp: α : Type u
inst✝ : DecidableEq α
xs : List ((_ : α) × α)
hperm : map Sigma.fst xs ~ map Sigma.snd xs
hnodup : (map Sigma.snd xs).Nodup
xs₀ : List α
h₀ : map Sigma.fst xs = xs₀
xs₁ : List α
h₁ : map Sigma.snd xs = xs₁
⊢ xs = List.toFinmap' (xs₀.zip xs₁)

Tactic:
by

Goal state after: