mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs

Goal state before:
pp: case hyp.inl.const
basis_hd : ℝ → ℝ
basis_tl : Basis
ms : MultiseriesExpansion (basis_hd :: basis_tl)
motive : MultiseriesExpansion (basis_hd :: basis_tl) → Prop
h_base : motive ms
h_step :
  ∀ (ms : MultiseriesExpansion (basis_hd :: basis_tl)),
    motive ms →
      ms.seq = Multiseries.nil ∧ ms.toFun =ᶠ[atTop] 0 ∨
        ∃ exp coef tl,
          ms.seq = Multiseries.cons exp coef tl ∧
            coef.Approximates ∧
              Majorized ms.toFun basis_hd exp ∧ motive (mk tl (ms.toFun - basis_hd ^ exp * coef.toFun))
ms✝ : MultiseriesExpansion []
⊢ [] = [] ∨
    (∃ basis_hd basis_tl f, f =ᶠ[atTop] 0 ∧ [] = basis_hd :: basis_tl ∧ ms✝ ≍ mk Multiseries.nil f) ∨
      ∃ basis_hd_1 f basis_tl_1 exp coef tl,
        (coef.Approximates ∨ ∃ (h_basis : basis_tl_1 = basis_hd :: basis_tl), motive (h_basis ▸ coef)) ∧
          Majorized f basis_hd_1 exp ∧
            ((mk tl (f - basis_hd_1 ^ exp * coef.toFun)).Approximates ∨
                ∃ (h_basis : basis_hd_1 :: basis_tl_1 = basis_hd :: basis_tl),
                  motive (h_basis ▸ mk tl (f - basis_hd_1 ^ exp * coef.toFun))) ∧
              [] = basis_hd_1 :: basis_tl_1 ∧ ms✝ ≍ mk (Multiseries.cons exp coef tl) f

Tactic:
grind

Goal state after:
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs

Goal state before:
pp: case hyp.inl.nil
basis_hd : ℝ → ℝ
basis_tl : Basis
ms : MultiseriesExpansion (basis_hd :: basis_tl)
motive : MultiseriesExpansion (basis_hd :: basis_tl) → Prop
h_base : motive ms
h_step :
  ∀ (ms : MultiseriesExpansion (basis_hd :: basis_tl)),
    motive ms →
      ms.seq = Multiseries.nil ∧ ms.toFun =ᶠ[atTop] 0 ∨
        ∃ exp coef tl,
          ms.seq = Multiseries.cons exp coef tl ∧
            coef.Approximates ∧
              Majorized ms.toFun basis_hd exp ∧ motive (mk tl (ms.toFun - basis_hd ^ exp * coef.toFun))
basis_hd✝ : ℝ → ℝ
basis_tl✝ : Basis
f✝ : ℝ → ℝ
hf✝ : f✝ =ᶠ[atTop] 0
⊢ basis_hd✝ :: basis_tl✝ = [] ∨
    (∃ basis_hd basis_tl f,
        f =ᶠ[atTop] 0 ∧ basis_hd✝ :: basis_tl✝ = basis_hd :: basis_tl ∧ mk Multiseries.nil f✝ ≍ mk Multiseries.nil f) ∨
      ∃ basis_hd_1 f basis_tl_1 exp coef tl,
        (coef.Approximates ∨ ∃ (h_basis : basis_tl_1 = basis_hd :: basis_tl), motive (h_basis ▸ coef)) ∧
          Majorized f basis_hd_1 exp ∧
            ((mk tl (f - basis_hd_1 ^ exp * coef.toFun)).Approximates ∨
                ∃ (h_basis : basis_hd_1 :: basis_tl_1 = basis_hd :: basis_tl),
                  motive (h_basis ▸ mk tl (f - basis_hd_1 ^ exp * coef.toFun))) ∧
              basis_hd✝ :: basis_tl✝ = basis_hd_1 :: basis_tl_1 ∧
                mk Multiseries.nil f✝ ≍ mk (Multiseries.cons exp coef tl) f

Tactic:
grind

Goal state after:
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs

Goal state before:
pp: case hyp.inl.cons
basis_hd : ℝ → ℝ
basis_tl : Basis
ms : MultiseriesExpansion (basis_hd :: basis_tl)
motive : MultiseriesExpansion (basis_hd :: basis_tl) → Prop
h_base : motive ms
h_step :
  ∀ (ms : MultiseriesExpansion (basis_hd :: basis_tl)),
    motive ms →
      ms.seq = Multiseries.nil ∧ ms.toFun =ᶠ[atTop] 0 ∨
        ∃ exp coef tl,
          ms.seq = Multiseries.cons exp coef tl ∧
            coef.Approximates ∧
              Majorized ms.toFun basis_hd exp ∧ motive (mk tl (ms.toFun - basis_hd ^ exp * coef.toFun))
basis_hd✝ f✝ : ℝ → ℝ
basis_tl✝ : Basis
exp✝ : ℝ
coef✝ : MultiseriesExpansion basis_tl✝
tl✝ : Multiseries basis_hd✝ basis_tl✝
h_coef✝ : coef✝.Approximates
h_maj✝ : Majorized f✝ basis_hd✝ exp✝
h_tl✝ : (mk tl✝ (f✝ - basis_hd✝ ^ exp✝ * coef✝.toFun)).Approximates
⊢ basis_hd✝ :: basis_tl✝ = [] ∨
    (∃ basis_hd basis_tl f,
        f =ᶠ[atTop] 0 ∧
          basis_hd✝ :: basis_tl✝ = basis_hd :: basis_tl ∧
            mk (Multiseries.cons exp✝ coef✝ tl✝) f✝ ≍ mk Multiseries.nil f) ∨
      ∃ basis_hd_1 f basis_tl_1 exp coef tl,
        (coef.Approximates ∨ ∃ (h_basis : basis_tl_1 = basis_hd :: basis_tl), motive (h_basis ▸ coef)) ∧
          Majorized f basis_hd_1 exp ∧
            ((mk tl (f - basis_hd_1 ^ exp * coef.toFun)).Approximates ∨
                ∃ (h_basis : basis_hd_1 :: basis_tl_1 = basis_hd :: basis_tl),
                  motive (h_basis ▸ mk tl (f - basis_hd_1 ^ exp * coef.toFun))) ∧
              basis_hd✝ :: basis_tl✝ = basis_hd_1 :: basis_tl_1 ∧
                mk (Multiseries.cons exp✝ coef✝ tl✝) f✝ ≍ mk (Multiseries.cons exp coef tl) f

Tactic:
grind

Goal state after:
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Trimming

Goal state before:
pp: case cons.h_trimmed
basis_hd : ℝ → ℝ
basis_tl : Basis
exp✝ : ℝ
f✝ : ℝ → ℝ
coef✝ : MultiseriesExpansion basis_tl
h_trimmed✝ : coef✝.Trimmed
h_ne_zero✝ : ¬coef✝.IsZero
tl✝ : Multiseries basis_hd basis_tl
⊢ coef✝.Trimmed

Tactic:
grind

Goal state after:
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Trimming

Goal state before:
pp: case cons.h_ne_zero
basis_hd : ℝ → ℝ
basis_tl : Basis
exp✝ : ℝ
f✝ : ℝ → ℝ
coef✝ : MultiseriesExpansion basis_tl
h_trimmed✝ : coef✝.Trimmed
h_ne_zero✝ : ¬coef✝.IsZero
tl✝ : Multiseries basis_hd basis_tl
⊢ ¬coef✝.IsZero

Tactic:
grind

Goal state after:
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Trimming

Goal state before:
pp: basis_hd : ℝ → ℝ
basis_tl : Basis
ms : MultiseriesExpansion (basis_hd :: basis_tl)
s : Multiseries basis_hd basis_tl
hs : ms.seq = s
h : s.Trimmed
⊢ ms.Trimmed

Tactic:
cases h with
    | nil =>
      convert Trimmed.nil (f := ms.toFun)
      simp [hs]
    | @cons _ _ exp coef tl _ h_trimmed h_ne_zero =>
      convert Trimmed.cons h_trimmed h_ne_zero (exp := exp) (tl := tl) (f := ms.toFun)
      simp only [ms_eq_mk_iff, hs, and_true]

Goal state after:
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Trimming

Goal state before:
pp: case nil
basis_hd : ℝ → ℝ
basis_tl : Basis
exp : ℝ
coef : MultiseriesExpansion basis_tl
tl : Multiseries basis_hd basis_tl
h_ms : Multiseries.cons exp coef tl = Multiseries.nil
⊢ coef.Trimmed ∧ ¬coef.IsZero

Tactic:
simp at h_ms

Goal state after:
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Trimming

Goal state before:
pp: case cons
basis_hd : ℝ → ℝ
basis_tl : Basis
exp : ℝ
coef : MultiseriesExpansion basis_tl
tl : Multiseries basis_hd basis_tl
exp✝ : ℝ
coef✝ : MultiseriesExpansion basis_tl
h_trimmed : coef✝.Trimmed
h_ne_zero : ¬coef✝.IsZero
tl✝ : Multiseries basis_hd basis_tl
h_ms : Multiseries.cons exp coef tl = Multiseries.cons exp✝ coef✝ tl✝
⊢ coef.Trimmed ∧ ¬coef.IsZero

Tactic:
simp at h_ms

Goal state after:
case cons
basis_hd : ℝ → ℝ
basis_tl : Basis
exp : ℝ
coef : MultiseriesExpansion basis_tl
tl : Multiseries basis_hd basis_tl
exp✝ : ℝ
coef✝ : MultiseriesExpansion basis_tl
h_trimmed : coef✝.Trimmed
h_ne_zero : ¬coef✝.IsZero
tl✝ : Multiseries basis_hd basis_tl
h_ms : exp = exp✝ ∧ coef = coef✝ ∧ tl = tl✝
⊢ coef.Trimmed ∧ ¬coef.IsZero
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Trimming

Goal state before:
pp: case cons
basis_hd : ℝ → ℝ
basis_tl : Basis
exp : ℝ
coef : MultiseriesExpansion basis_tl
tl : Multiseries basis_hd basis_tl
exp✝ : ℝ
coef✝ : MultiseriesExpansion basis_tl
h_trimmed : coef✝.Trimmed
h_ne_zero : ¬coef✝.IsZero
tl✝ : Multiseries basis_hd basis_tl
h_ms : exp = exp✝ ∧ coef = coef✝ ∧ tl = tl✝
⊢ coef.Trimmed ∧ ¬coef.IsZero

Tactic:
grind

Goal state after:
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs

Goal state before:
pp: case hyp.inr.inl
basis_hd : ℝ → ℝ
basis_tl : Basis
ms✝ : MultiseriesExpansion (basis_hd :: basis_tl)
motive : MultiseriesExpansion (basis_hd :: basis_tl) → Prop
h_base : motive ms✝
h_step✝ :
  ∀ (ms : MultiseriesExpansion (basis_hd :: basis_tl)),
    motive ms →
      ms.seq = Multiseries.nil ∧ ms.toFun =ᶠ[atTop] 0 ∨
        ∃ exp coef tl,
          ms.seq = Multiseries.cons exp coef tl ∧
            coef.Approximates ∧
              Majorized ms.toFun basis_hd exp ∧ motive (mk tl (ms.toFun - basis_hd ^ exp * coef.toFun))
ms : MultiseriesExpansion (basis_hd :: basis_tl)
h_ms : motive ms
h_step : ms.seq = Multiseries.nil ∧ ms.toFun =ᶠ[atTop] 0
⊢ ms.toFun =ᶠ[atTop] 0 ∧ ms.seq = Multiseries.nil ∨
    ∃ basis_hd_1 f basis_tl_1 exp coef,
      (coef.Approximates ∨ ∃ (h_basis : basis_tl_1 = basis_hd :: basis_tl), motive (h_basis ▸ coef)) ∧
        Majorized f basis_hd_1 exp ∧
          ∃ x,
            ((mk x (f - basis_hd_1 ^ exp * coef.toFun)).Approximates ∨
                ∃ (h : basis_hd_1 = basis_hd ∧ basis_tl_1 = basis_tl),
                  motive (⋯ ▸ mk x (f - basis_hd_1 ^ exp * coef.toFun))) ∧
              (basis_hd = basis_hd_1 ∧ basis_tl = basis_tl_1) ∧ ms ≍ mk (Multiseries.cons exp coef x) f

Tactic:
grind

Goal state after:
Module: Mathlib.Tactic.DeriveEncodable

Goal state before:
pp: case nat
n : ℕ
⊢ S.decode (S.nat n).encode = S.nat n

Tactic:
unfold S.encode S.decode
      simp

Goal state after:
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs

Goal state before:
pp: case hyp.inr.inr
basis_hd : ℝ → ℝ
basis_tl : Basis
ms✝ : MultiseriesExpansion (basis_hd :: basis_tl)
motive : MultiseriesExpansion (basis_hd :: basis_tl) → Prop
h_base : motive ms✝
h_step :
  ∀ (ms : MultiseriesExpansion (basis_hd :: basis_tl)),
    motive ms →
      ms.seq = Multiseries.nil ∧ ms.toFun =ᶠ[atTop] 0 ∨
        ∃ exp coef tl,
          ms.seq = Multiseries.cons exp coef tl ∧
            coef.Approximates ∧
              Majorized ms.toFun basis_hd exp ∧ motive (mk tl (ms.toFun - basis_hd ^ exp * coef.toFun))
ms : MultiseriesExpansion (basis_hd :: basis_tl)
h_ms : motive ms
exp : ℝ
coef : MultiseriesExpansion basis_tl
tl : Multiseries basis_hd basis_tl
h_seq : ms.seq = Multiseries.cons exp coef tl
h_coef : coef.Approximates
h_maj : Majorized ms.toFun basis_hd exp
h_tl : motive (mk tl (ms.toFun - basis_hd ^ exp * coef.toFun))
⊢ ((mk tl (ms.toFun - basis_hd ^ exp * coef.toFun)).Approximates ∨
      motive (mk tl (ms.toFun - basis_hd ^ exp * coef.toFun))) ∧
    ms.seq = Multiseries.cons exp coef tl

Tactic:
grind

Goal state after:
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs

Goal state before:
pp: case x
basis_hd : ℝ → ℝ
basis_tl : Basis
ms : MultiseriesExpansion (basis_hd :: basis_tl)
motive : MultiseriesExpansion (basis_hd :: basis_tl) → Prop
h_base : motive ms
h_step :
  ∀ (ms : MultiseriesExpansion (basis_hd :: basis_tl)),
    motive ms →
      ms.seq = Multiseries.nil ∧ ms.toFun =ᶠ[atTop] 0 ∨
        ∃ exp coef tl,
          ms.seq = Multiseries.cons exp coef tl ∧
            coef.Approximates ∧
              Majorized ms.toFun basis_hd exp ∧ motive (mk tl (ms.toFun - basis_hd ^ exp * coef.toFun))
⊢ ms.Approximates ∨ ∃ (h_basis : basis_hd :: basis_tl = basis_hd :: basis_tl), motive (h_basis ▸ ms)

Tactic:
grind

Goal state after:
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs

Goal state before:
pp: case nil
f basis_hd : ℝ → ℝ
basis_tl : Basis
f✝ : ℝ → ℝ
hf✝ : f✝ =ᶠ[atTop] 0
h_ms : mk Multiseries.nil f = mk Multiseries.nil f✝
⊢ f =ᶠ[atTop] 0

Tactic:
simp at h_ms

Goal state after:
case nil
f basis_hd : ℝ → ℝ
basis_tl : Basis
f✝ : ℝ → ℝ
hf✝ : f✝ =ᶠ[atTop] 0
h_ms : f = f✝
⊢ f =ᶠ[atTop] 0
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs

Goal state before:
pp: case cons
f basis_hd : ℝ → ℝ
basis_tl : Basis
f✝ : ℝ → ℝ
exp✝ : ℝ
h_maj✝ : Majorized f✝ basis_hd exp✝
coef✝ : MultiseriesExpansion basis_tl
h_coef✝ : coef✝.Approximates
tl✝ : Multiseries basis_hd basis_tl
h_tl✝ : (mk tl✝ (f✝ - basis_hd ^ exp✝ * coef✝.toFun)).Approximates
h_ms : mk Multiseries.nil f = mk (Multiseries.cons exp✝ coef✝ tl✝) f✝
⊢ f =ᶠ[atTop] 0

Tactic:
simp at h_ms

Goal state after:
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs

Goal state before:
pp: case nil
f basis_hd : ℝ → ℝ
basis_tl : Basis
f✝ : ℝ → ℝ
hf✝ : f✝ =ᶠ[atTop] 0
h_ms : f = f✝
⊢ f =ᶠ[atTop] 0

Tactic:
grind

Goal state after:
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs

Goal state before:
pp: case nil
f basis_hd : ℝ → ℝ
basis_tl : Basis
exp : ℝ
coef : MultiseriesExpansion basis_tl
tl : Multiseries basis_hd basis_tl
f✝ : ℝ → ℝ
hf✝ : f✝ =ᶠ[atTop] 0
h_ms : mk (Multiseries.cons exp coef tl) f = mk Multiseries.nil f✝
⊢ coef.Approximates ∧ Majorized f basis_hd exp ∧ (mk tl (f - basis_hd ^ exp * coef.toFun)).Approximates

Tactic:
simp at h_ms

Goal state after:
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs

Goal state before:
pp: case cons
f basis_hd : ℝ → ℝ
basis_tl : Basis
exp : ℝ
coef : MultiseriesExpansion basis_tl
tl : Multiseries basis_hd basis_tl
f✝ : ℝ → ℝ
exp✝ : ℝ
h_maj✝ : Majorized f✝ basis_hd exp✝
coef✝ : MultiseriesExpansion basis_tl
h_coef✝ : coef✝.Approximates
tl✝ : Multiseries basis_hd basis_tl
h_tl✝ : (mk tl✝ (f✝ - basis_hd ^ exp✝ * coef✝.toFun)).Approximates
h_ms : mk (Multiseries.cons exp coef tl) f = mk (Multiseries.cons exp✝ coef✝ tl✝) f✝
⊢ coef.Approximates ∧ Majorized f basis_hd exp ∧ (mk tl (f - basis_hd ^ exp * coef.toFun)).Approximates

Tactic:
simp at h_ms

Goal state after:
case cons
f basis_hd : ℝ → ℝ
basis_tl : Basis
exp : ℝ
coef : MultiseriesExpansion basis_tl
tl : Multiseries basis_hd basis_tl
f✝ : ℝ → ℝ
exp✝ : ℝ
h_maj✝ : Majorized f✝ basis_hd exp✝
coef✝ : MultiseriesExpansion basis_tl
h_coef✝ : coef✝.Approximates
tl✝ : Multiseries basis_hd basis_tl
h_tl✝ : (mk tl✝ (f✝ - basis_hd ^ exp✝ * coef✝.toFun)).Approximates
h_ms : (exp = exp✝ ∧ coef = coef✝ ∧ tl = tl✝) ∧ f = f✝
⊢ coef.Approximates ∧ Majorized f basis_hd exp ∧ (mk tl (f - basis_hd ^ exp * coef.toFun)).Approximates
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs

Goal state before:
pp: case cons
f basis_hd : ℝ → ℝ
basis_tl : Basis
exp : ℝ
coef : MultiseriesExpansion basis_tl
tl : Multiseries basis_hd basis_tl
f✝ : ℝ → ℝ
exp✝ : ℝ
h_maj✝ : Majorized f✝ basis_hd exp✝
coef✝ : MultiseriesExpansion basis_tl
h_coef✝ : coef✝.Approximates
tl✝ : Multiseries basis_hd basis_tl
h_tl✝ : (mk tl✝ (f✝ - basis_hd ^ exp✝ * coef✝.toFun)).Approximates
h_ms : (exp = exp✝ ∧ coef = coef✝ ∧ tl = tl✝) ∧ f = f✝
⊢ coef.Approximates ∧ Majorized f basis_hd exp ∧ (mk tl (f - basis_hd ^ exp * coef.toFun)).Approximates

Tactic:
grind

Goal state after:
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs

Goal state before:
pp: basis_hd : ℝ → ℝ
basis_tl : Basis
ms : MultiseriesExpansion (basis_hd :: basis_tl)
f : ℝ → ℝ
h_equiv : ms.toFun =ᶠ[atTop] f
h_approx : ms.Approximates
motive : MultiseriesExpansion (basis_hd :: basis_tl) → Prop :=
  fun ms ↦ ∃ ms' f', ms = ms'.replaceFun f' ∧ ms'.Approximates ∧ ms'.toFun =ᶠ[atTop] f'
⊢ ms.replaceFun f = ms.replaceFun f ∧ ms.Approximates ∧ ms.toFun =ᶠ[atTop] f

Tactic:
grind

Goal state after:
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs

Goal state before:
pp: basis_hd : ℝ → ℝ
basis_tl : Basis
x y : MultiseriesExpansion (basis_hd :: basis_tl)
⊢ x ≈ y ↔ x.seq = y.seq ∧ x.toFun =ᶠ[atTop] y.toFun

Tactic:
rfl

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

Goal state before:
pp: m b : ℕ
hk₁ : (m + 1) ^ 2 ≤ b ^ 2
hk₂ : b ^ 2 ≤ m ^ 2 + 2 * m
⊢ False

Tactic:
grind

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

Goal state before:
pp: a b ab : ℕ
r : ℤ
hab : a % b = ab
hr : jacobiSymNat ab b = r
⊢ jacobiSym (↑a % ↑b) b = jacobiSym (↑(a % b)) b

Tactic:
rfl

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

Goal state before:
pp: case ha
a : ℚ
n d : ℕ
hn : n ≠ 0
hd : d ≠ 0
ha : IsRat a (Int.negOfNat n) d
q : ℚ
hq : -(↑n / ↑d) = q * q
⊢ 0 < ↑n

Tactic:
simpa [Nat.pos_iff_ne_zero]

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

Goal state before:
pp: case hb
a : ℚ
n d : ℕ
hn : n ≠ 0
hd : d ≠ 0
ha : IsRat a (Int.negOfNat n) d
q : ℚ
hq : -(↑n / ↑d) = q * q
⊢ 0 < ↑d

Tactic:
simpa [Nat.pos_iff_ne_zero]

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

Goal state before:
pp: x y : ℝ
x_num x_den y_num y_den k_num : ℕ
hx_coprime : x_num.Coprime x_den
hy_coprime : y_num.Coprime y_den
hn1 : k_num ^ y_den < x_num
hn2 : x_num < (k_num + 1) ^ y_den
hy_den_pos : 0 < y_den
hx_inv : Invertible ↑x_den
hx_eq : x = ↑x_num * ⅟↑x_den
hy_inv : Invertible ↑y_den
hy_eq : y = ↑y_num * ⅟↑y_den
⊢ ↑y_num * (↑y_den)⁻¹ = ↑y_num / ↑y_den

Tactic:
rfl

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

Goal state before:
pp: x y : ℝ
x_num x_den y_num y_den k_num : ℕ
hx_coprime : x_num.Coprime x_den
hy_coprime : y_num.Coprime y_den
hn1 : k_num ^ y_den < x_num
hn2 : x_num < (k_num + 1) ^ y_den
hy_den_pos : 0 < y_den
hx_inv : Invertible ↑x_den
hx_eq : x = ↑x_num * ⅟↑x_den
hy_inv : Invertible ↑y_den
hy_eq : y = ↑y_num * ⅟↑y_den
h1 : ↑y_num * ⅟↑y_den = ↑(↑y_num / ↑y_den)
⊢ ↑x_num * (↑x_den)⁻¹ = ↑x_num / ↑x_den

Tactic:
rfl

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

Goal state before:
pp: a m : ℕ
⊢ (a.pow 0).mod m.succ.succ = 1

Tactic:
rfl

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 % n) = ↑((a ^ b).mod n)

Tactic:
rfl

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

Goal state before:
pp: case pos
α : Type u
inst✝ : DecidableEq α
xs : List (α × α)
x y z : α
h✝ : y = x
⊢ (some z).getD x = z

Tactic:
rfl

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

Goal state before:
pp: case neg
α : Type u
inst✝ : DecidableEq α
xs : List (α × α)
x y z : α
h✝ : ¬y = x
⊢ (dlookup x (map Prod.toSigma xs)).getD x = (dlookup x (map Prod.toSigma xs)).getD x

Tactic:
rfl

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

Goal state before:
pp: case neg.cons.cons
α : 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
⊢ val ∈ ys

Tactic:
← Option.mem_def,

Goal state after:
case neg.cons.cons
α : 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₃ : val ∈ dlookup x (map Prod.toSigma (xs.zip ys))
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
⊢ val ∈ ys
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
⊢ ⨅ i, comap ((fun a ↦ (a.1 i, a.2 i)) ∘ Prod.map F F) (𝓤 α) ≤ 𝓤 ι

Tactic:
Function.comp_def

Goal state after:
ι : Type u_1
X : Type u_2
α : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : UniformSpace α
F : ι → X → α
inst✝ : CompactSpace X
F_eqcont : Equicontinuous F
⊢ ⨅ i, comap (fun x ↦ ((Prod.map F F x).1 i, (Prod.map F F x).2 i)) (𝓤 α) ≤ 𝓤 ι
Module: Mathlib.Testing.Plausible.Functions

Goal state before:
pp: α : Type u
inst✝ : DecidableEq α
xs ys : List α
x : α
h : x ∉ xs
⊢ none.getD x = x

Tactic:
rfl

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
⊢ UniformSpace.comap (⇑UniformFun.ofFun ∘ F) (UniformFun.uniformSpace X α) = inst✝¹ ↔
    UniformSpace.comap F (UniformFun.uniformSpace X α) = inst✝¹

Tactic:
rfl

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
⊢ UniformSpace.comap (⇑(UniformOnFun.ofFun 𝔖) ∘ F) (UniformOnFun.uniformSpace X α 𝔖) = inst✝ ↔
    UniformSpace.comap F (UniformOnFun.uniformSpace X α 𝔖) = inst✝

Tactic:
rfl

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

Goal state before:
pp: case cons
α : Type u
inst✝ : DecidableEq α
xs_hd : (_ : α) × α
xs_tl : List ((_ : α) × α)
xs_ih :
  xs_tl =
    map
      (fun x ↦
        match x with
        | (a, b) => ⟨a, b⟩)
      ((map Sigma.fst xs_tl).zip (map Sigma.snd xs_tl))
⊢ xs_hd :: xs_tl =
    map
      (fun x ↦
        match x with
        | (a, b) => ⟨a, b⟩)
      ((map Sigma.fst (xs_hd :: xs_tl)).zip (map Sigma.snd (xs_hd :: xs_tl)))

Tactic:
| cons xs_hd xs_tl xs_ih =>

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)
𝔖_covers : ∀ (x : X), x ∈ ⋃₀ 𝔖
𝔖_compact : ∀ K ∈ 𝔖, IsCompact K
F_eqcont : ∀ K ∈ 𝔖, EquicontinuousOn F K
φ : (↑(⋃₀ 𝔖) → α) ≃ᵤ (X → α) := UniformEquiv.piCongrLeft (Equiv.subtypeUnivEquiv 𝔖_covers)
⊢ (⋃₀ 𝔖).domRestrict ∘ F = ⇑φ.symm ∘ F

Tactic:
rfl

Goal state after:
Module: Mathlib.Topology.Algebra.Category.ProfiniteGrp.Completion

Goal state before:
pp: case mk
G : GrpCat
H : FiniteIndexNormalSubgroup ↑G
x✝ : ↑(FiniteGrp.of (↑G ⧸ H.toSubgroup)).toGrp
x : ↑G
⊢ (ConcreteCategory.hom (FiniteGrp.ofHom (QuotientGroup.map H.toSubgroup H.toSubgroup (MonoidHom.id ↑G) ⋯)))
      (Quot.mk (⇑(QuotientGroup.leftRel H.toSubgroup)) x) =
    (ConcreteCategory.hom (𝟙 (FiniteGrp.of (↑G ⧸ H.toSubgroup)))) (Quot.mk (⇑(QuotientGroup.leftRel H.toSubgroup)) x)

Tactic:
rfl

Goal state after:
Module: Mathlib.Topology.Algebra.Category.ProfiniteGrp.Completion

Goal state before:
pp: case mk
G : GrpCat
X✝ Y✝ Z✝ : FiniteIndexNormalSubgroup ↑G
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
x✝ : ↑(FiniteGrp.of (↑G ⧸ X✝.toSubgroup)).toGrp
x : ↑G
⊢ (ConcreteCategory.hom (FiniteGrp.ofHom (QuotientGroup.map X✝.toSubgroup Z✝.toSubgroup (MonoidHom.id ↑G) ⋯)))
      (Quot.mk (⇑(QuotientGroup.leftRel X✝.toSubgroup)) x) =
    (ConcreteCategory.hom
        (FiniteGrp.ofHom (QuotientGroup.map X✝.toSubgroup Y✝.toSubgroup (MonoidHom.id ↑G) ⋯) ≫
          FiniteGrp.ofHom (QuotientGroup.map Y✝.toSubgroup Z✝.toSubgroup (MonoidHom.id ↑G) ⋯)))
      (Quot.mk (⇑(QuotientGroup.leftRel X✝.toSubgroup)) x)

Tactic:
rfl

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 ι
𝔖 : Set (Set X)
𝔖_covers : ∀ (x : X), x ∈ ⋃₀ 𝔖
𝔖_compact : ∀ K ∈ 𝔖, IsCompact K
F_eqcont : ∀ K ∈ 𝔖, EquicontinuousOn F K
φ : (↑(⋃₀ 𝔖) → α) ≃ₜ (X → α) := Homeomorph.piCongrLeft (Equiv.subtypeUnivEquiv 𝔖_covers)
⊢ (⋃₀ 𝔖).domRestrict ∘ F = ⇑φ.symm ∘ F

Tactic:
rfl

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
ℱ : Filter ι
f : X → α
K : Set X
hK : K ∈ 𝔖
this : CompactSpace ↑K
⊢ Tendsto ((⇑UniformFun.ofFun ∘ K.domRestrict ∘ ⇑(UniformOnFun.toFun 𝔖)) ∘ ⇑(UniformOnFun.ofFun 𝔖) ∘ F) ℱ
      (𝓝 ((⇑UniformFun.ofFun ∘ K.domRestrict ∘ ⇑(UniformOnFun.toFun 𝔖)) ((UniformOnFun.ofFun 𝔖) f))) ↔
    Tendsto (⇑UniformFun.ofFun ∘ K.domRestrict ∘ F) ℱ (𝓝 (UniformFun.ofFun (K.domRestrict f)))

Tactic:
rfl

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
𝔖_covers : ∀ (x : X), x ∈ ⋃₀ 𝔖
F_eqcont : ∀ K ∈ 𝔖, EquicontinuousOn F K
ℱ : Filter ι
f : X → α
φ : (↑(⋃₀ 𝔖) → α) ≃ₜ (X → α) := Homeomorph.piCongrLeft (Equiv.subtypeUnivEquiv 𝔖_covers)
⊢ (⋃₀ 𝔖).domRestrict ∘ F = ⇑φ.symm ∘ F

Tactic:
rfl

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
𝔖_covers : ∀ (x : X), x ∈ ⋃₀ 𝔖
F_eqcont : ∀ K ∈ 𝔖, EquicontinuousOn F K
ℱ : Filter ι
f : X → α
φ : (↑(⋃₀ 𝔖) → α) ≃ₜ (X → α) := Homeomorph.piCongrLeft (Equiv.subtypeUnivEquiv 𝔖_covers)
⊢ (⋃₀ 𝔖).domRestrict f = φ.symm f

Tactic:
rfl

Goal state after: