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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
F : β → Option (α × γ × β)
op : γ → Stream'.Seq α → Stream'.Seq α
h : FriendlyOperationClass op
T : (β →ᵤ Stream'.Seq α) → β →ᵤ Stream'.Seq α :=
  fun f b ↦
    match F b with
    | none => nil
    | some (a, c, b') => Seq.cons a (op c (f b'))
f : β →ᵤ Stream'.Seq α
⊢ ∀ (y : β →ᵤ Stream'.Seq α), dist (T f) (T y) ≤ ↑2⁻¹ * dist f y

Tactic:
g

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
F : β → Option (α × γ × β)
op : γ → Stream'.Seq α → Stream'.Seq α
h : FriendlyOperationClass op
T : (β →ᵤ Stream'.Seq α) → β →ᵤ Stream'.Seq α :=
  fun f b ↦
    match F b with
    | none => nil
    | some (a, c, b') => Seq.cons a (op c (f b'))
f g : β →ᵤ Stream'.Seq α
⊢ dist (T f) (T g) ≤ ↑2⁻¹ * dist f g
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: case succ.refine_2.e_a
a0 a' : ONote
N0 : a0.NF
Na' : a'.NF
m : ℕ
d : ω ∣ a'.repr
e0 : a0.repr ≠ 0
h : a'.repr + ↑m < ω ^ a0.repr
n : ℕ+
No : (a0.oadd n a').NF
k : ℕ
R' : Ordinal.{0} := (opowAux 0 a0 (a0.oadd n a' * ↑m) (k + 1) m).repr
R : Ordinal.{0} := (opowAux 0 a0 (a0.oadd n a' * ↑m) k m).repr
ω0 : Ordinal.{0} := ω ^ a0.repr
α' : Ordinal.{0} := ω0 * ↑↑n + a'.repr
IH : (k ≠ 0 → R < ω0 ^ succ ↑k) ∧ ω0 ^ ↑k * α' + R = (α' + ↑m) ^ succ ↑k
RR : R' = ω0 ^ ↑k * (α' * ↑m) + R
α0 : 0 < α'
ω00 : 0 < ω0 ^ ↑k
Rl : R < ω ^ (a0.repr * succ ↑k)
⊢ ω0 ^ ↑k * α' * ↑m + R = (ω0 ^ ↑k * α' + R) * ↑m

Tactic:
· cases m
    · have : R = 0 := by cases k <;> simp [R, opowAux]
      simp [this]
    · rw [Nat.cast_add_one, ← succ_eq_add_one, add_mul_succ]
      apply add_of_omega0_opow_le Rl
      rw [opow_mul, opow_succ]
      gcongr
      simpa [repr] using omega0_le_oadd a0 n a'

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

Goal state before:
pp: basis : Basis
c : ℝ
⊢ (const [] c).toFun = fun x ↦ c

Tactic:
| =>

Goal state after:
basis : Basis
c : ℝ
⊢ (const [] c).toFun = fun x ↦ c
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basic

Goal state before:
pp: basis : Basis
c : ℝ
head✝ : ℝ → ℝ
tail✝ : List (ℝ → ℝ)
⊢ (const (head✝ :: tail✝) c).toFun = fun x ↦ c

Tactic:
| =>

Goal state after:
basis : Basis
c : ℝ
head✝ : ℝ → ℝ
tail✝ : List (ℝ → ℝ)
⊢ (const (head✝ :: tail✝) c).toFun = fun x ↦ c
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basic

Goal state before:
pp: basis : Basis
⊢ zero.toFun = 0

Tactic:
| =>

Goal state after:
basis : Basis
⊢ zero.toFun = 0
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basic

Goal state before:
pp: basis : Basis
head✝ : ℝ → ℝ
tail✝ : List (ℝ → ℝ)
⊢ zero.toFun = 0

Tactic:
| =>

Goal state after:
basis : Basis
head✝ : ℝ → ℝ
tail✝ : List (ℝ → ℝ)
⊢ zero.toFun = 0
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basic

Goal state before:
pp: basis : Basis
⊢ one.toFun = 1

Tactic:
by
  simp [one]
  rfl

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

Goal state before:
pp: α : Type u_1
op : Stream'.Seq α → Stream'.Seq α
h : FriendlyOperation op
s t : Stream'.Seq α
h_head : Option.map Prod.fst s.destruct = Option.map Prod.fst t.destruct
⊢ Option.map (Prod.fst ∘ fun x ↦ (x.1, ↑x.2 s.tail)) (h.unfold (Option.map Prod.fst s.destruct)) =
    Option.map (Prod.fst ∘ fun x ↦ (x.1, ↑x.2 t.tail)) (h.unfold (Option.map Prod.fst t.destruct))

Tactic:
simp [h_head]

Goal state after:
α : Type u_1
op : Stream'.Seq α → Stream'.Seq α
h : FriendlyOperation op
s t : Stream'.Seq α
h_head : Option.map Prod.fst s.destruct = Option.map Prod.fst t.destruct
⊢ Option.map (Prod.fst ∘ fun x ↦ (x.1, ↑x.2 s.tail)) (h.unfold (Option.map Prod.fst t.destruct)) =
    Option.map (Prod.fst ∘ fun x ↦ (x.1, ↑x.2 t.tail)) (h.unfold (Option.map Prod.fst t.destruct))
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs

Goal state before:
pp: basis_hd : ℝ → ℝ
basis_tl : Basis
ms : Multiseries basis_hd basis_tl
h : ms.destruct = none
⊢ ms = nil

Tactic:
apply Stream'.Seq.destruct_eq_none
  simpa [destruct] using h

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

Goal state before:
pp: basis_hd : ℝ → ℝ
basis_tl : Basis
R : ℝ × MultiseriesExpansion basis_tl → ℝ × MultiseriesExpansion basis_tl → Prop
⊢ Seq.Pairwise R nil

Tactic:
by
  simp [nil]

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

Goal state before:
pp: case h.cons.some
α : Type u_1
op✝ : Stream'.Seq α → Stream'.Seq α
motive : (Stream'.Seq α → Stream'.Seq α) → Prop
h_base : motive op✝
h_step :
  ∀ (op : Stream'.Seq α → Stream'.Seq α),
    motive op →
      ∃ T,
        ∀ (s : Stream'.Seq α),
          (op s).destruct =
            Option.map
              (fun x ↦
                match x with
                | (hd, opf, op') => (hd, ↑opf (↑op' s.tail)))
              (T s.head)
motive' : (Stream'.Seq α → Stream'.Seq α) → Prop :=
  fun op ↦ ∃ opf op', op = opf ∘ op' ∧ FriendlyOperation opf ∧ motive op'
opf op : Stream'.Seq α → Stream'.Seq α
h_opf : FriendlyOperation opf
h_op : motive op
T : Option α → Option (α × Subtype FriendlyOperation × Subtype motive)
s : Stream'.Seq α
s_hd : α
s_tl : Stream'.Seq α
v : α × Subtype FriendlyOperation × Subtype motive
hT : some (s_hd, s_tl) = Option.map (fun x ↦ (x.1, ↑x.2.1 (↑x.2.2 s.tail))) (some v)
⊢ Option.map (fun x ↦ (x.1, ↑x.2 s_tl)) (h_opf.unfold (some s_hd)) =
    Option.map (fun x ↦ (x.1, ↑x.2 s.tail))
      (match some v with
      | none => Option.map (fun x ↦ (x.1, ⟨(fun x_1 ↦ ↑x.2 nil) ∘ op, ⋯⟩)) (h_opf.unfold none)
      | some (hd, opf', op') => Option.map (fun x ↦ (x.1, ⟨(↑x.2 ∘ ↑opf') ∘ ↑op', ⋯⟩)) (h_opf.unfold (some hd)))

Tactic:
obtain ⟨hd, opf', op'⟩ := v

Goal state after:
case h.cons.some
α : Type u_1
op✝ : Stream'.Seq α → Stream'.Seq α
motive : (Stream'.Seq α → Stream'.Seq α) → Prop
h_base : motive op✝
h_step :
  ∀ (op : Stream'.Seq α → Stream'.Seq α),
    motive op →
      ∃ T,
        ∀ (s : Stream'.Seq α),
          (op s).destruct =
            Option.map
              (fun x ↦
                match x with
                | (hd, opf, op') => (hd, ↑opf (↑op' s.tail)))
              (T s.head)
motive' : (Stream'.Seq α → Stream'.Seq α) → Prop :=
  fun op ↦ ∃ opf op', op = opf ∘ op' ∧ FriendlyOperation opf ∧ motive op'
opf op : Stream'.Seq α → Stream'.Seq α
h_opf : FriendlyOperation opf
h_op : motive op
T : Option α → Option (α × Subtype FriendlyOperation × Subtype motive)
s : Stream'.Seq α
s_hd : α
s_tl : Stream'.Seq α
hd : α
opf' : Subtype FriendlyOperation
op' : Subtype motive
hT : some (s_hd, s_tl) = Option.map (fun x ↦ (x.1, ↑x.2.1 (↑x.2.2 s.tail))) (some (hd, opf', op'))
⊢ Option.map (fun x ↦ (x.1, ↑x.2 s_tl)) (h_opf.unfold (some s_hd)) =
    Option.map (fun x ↦ (x.1, ↑x.2 s.tail))
      (match some (hd, opf', op') with
      | none => Option.map (fun x ↦ (x.1, ⟨(fun x_1 ↦ ↑x.2 nil) ∘ op, ⋯⟩)) (h_opf.unfold none)
      | some (hd, opf', op') => Option.map (fun x ↦ (x.1, ⟨(↑x.2 ∘ ↑opf') ∘ ↑op', ⋯⟩)) (h_opf.unfold (some hd)))
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic

Goal state before:
pp: case cons.cons.inl
exps_hd : ℝ
exps_tl : List ℝ
basis_hd : ℝ → ℝ
basis_tl : List (ℝ → ℝ)
h_basis : WellFormedBasis (basis_hd :: basis_tl)
h_length : (exps_hd :: exps_tl).length = (basis_hd :: basis_tl).length
h : 0 < exps_hd
⊢ Tendsto (toFun (exps_hd :: exps_tl) (basis_hd :: basis_tl)) atTop atTop

Tactic:
exact toFun_tendsto_top_of_head_pos h_basis h

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

Goal state before:
pp: case step.left
basis_hd : ℝ → ℝ
basis_tl : Basis
s : Multiseries basis_hd basis_tl
motive : Multiseries basis_hd basis_tl → Prop
h_base : motive s
h_step :
  ∀ (exp : ℝ) (coef : MultiseriesExpansion basis_tl) (tl : Multiseries basis_hd basis_tl),
    motive (Multiseries.cons exp coef tl) → coef.Sorted ∧ tl.leadingExp < ↑exp ∧ motive tl
exp : ℝ
coef : MultiseriesExpansion basis_tl
tl : Stream'.Seq (ℝ × MultiseriesExpansion basis_tl)
h : motive (Seq.cons (exp, coef) tl)
tl_exp : ℝ
tl_coef : MultiseriesExpansion basis_tl
⊢ (tl_exp, tl_coef) ∈ tl.head → (exp, coef) > (tl_exp, tl_coef)

Tactic:
h_tl

Goal state after:
case step.left
basis_hd : ℝ → ℝ
basis_tl : Basis
s : Multiseries basis_hd basis_tl
motive : Multiseries basis_hd basis_tl → Prop
h_base : motive s
h_step :
  ∀ (exp : ℝ) (coef : MultiseriesExpansion basis_tl) (tl : Multiseries basis_hd basis_tl),
    motive (Multiseries.cons exp coef tl) → coef.Sorted ∧ tl.leadingExp < ↑exp ∧ motive tl
exp : ℝ
coef : MultiseriesExpansion basis_tl
tl : Stream'.Seq (ℝ × MultiseriesExpansion basis_tl)
h : motive (Seq.cons (exp, coef) tl)
tl_exp : ℝ
tl_coef : MultiseriesExpansion basis_tl
h_tl : (tl_exp, tl_coef) ∈ tl.head
⊢ (exp, coef) > (tl_exp, tl_coef)
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs

Goal state before:
pp: case step.left
basis_hd : ℝ → ℝ
basis_tl : Basis
s : Multiseries basis_hd basis_tl
motive : Multiseries basis_hd basis_tl → Prop
h_base : motive s
h_step :
  ∀ (exp : ℝ) (coef : MultiseriesExpansion basis_tl) (tl : Multiseries basis_hd basis_tl),
    motive (Multiseries.cons exp coef tl) → coef.Sorted ∧ tl.leadingExp < ↑exp ∧ motive tl
exp : ℝ
coef : MultiseriesExpansion basis_tl
tl : Stream'.Seq (ℝ × MultiseriesExpansion basis_tl)
h : motive (Seq.cons (exp, coef) tl)
⊢ ∀ x ∈ tl.head, (exp, coef) > x

Tactic:
intro (tl_exp, tl_coef) h_tl

Goal state after:
case step.left
basis_hd : ℝ → ℝ
basis_tl : Basis
s : Multiseries basis_hd basis_tl
motive : Multiseries basis_hd basis_tl → Prop
h_base : motive s
h_step :
  ∀ (exp : ℝ) (coef : MultiseriesExpansion basis_tl) (tl : Multiseries basis_hd basis_tl),
    motive (Multiseries.cons exp coef tl) → coef.Sorted ∧ tl.leadingExp < ↑exp ∧ motive tl
exp : ℝ
coef : MultiseriesExpansion basis_tl
tl : Stream'.Seq (ℝ × MultiseriesExpansion basis_tl)
h : motive (Seq.cons (exp, coef) tl)
tl_exp : ℝ
tl_coef : MultiseriesExpansion basis_tl
h_tl : (tl_exp, tl_coef) ∈ tl.head
⊢ (exp, coef) > (tl_exp, tl_coef)
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic

Goal state before:
pp: t1 t2 : Monomial
basis : Basis
h_basis : WellFormedBasis basis
h_length : List.length t1.unit = List.length t2.unit
⊢ (t1.mul t2).toFun basis =ᶠ[atTop] t1.toFun basis * t2.toFun basis

Tactic:
simp only [toFun, mul, Algebra.mul_smul_comm, Algebra.smul_mul_assoc]
  grw [UnitMonomial.mul_toFun h_basis h_length]
  filter_upwards [] with t
  simp [Pi.smul_apply, Pi.mul_apply]
  ring

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

Goal state before:
pp: case h.cons.some
α : Type u_1
motive : (Stream'.Seq α → Stream'.Seq α) → Prop
h_step :
  ∀ (op : Stream'.Seq α → Stream'.Seq α),
    motive op →
      ∃ T,
        ∀ (s : Stream'.Seq α),
          (op s).destruct =
            Option.map
              (fun x ↦
                match x with
                | (hd, opf, op') => (hd, ↑op' (↑opf s.tail)))
              (T s.head)
motive' : (Stream'.Seq α → Stream'.Seq α) → Prop :=
  fun op ↦ ∃ opf op', op = op' ∘ opf ∧ FriendlyOperation opf ∧ motive op'
opf op : Stream'.Seq α → Stream'.Seq α
h_opf : FriendlyOperation opf
h_op : motive op
T : Option α → Option (α × Subtype FriendlyOperation × Subtype motive)
hT :
  ∀ (s : Stream'.Seq α),
    (op s).destruct =
      Option.map
        (fun x ↦
          match x with
          | (hd, opf, op') => (hd, ↑op' (↑opf s.tail)))
        (T s.head)
s : Stream'.Seq α
s_hd : α
s_tl : Stream'.Seq α
v : α × Subtype FriendlyOperation
hF : some (s_hd, s_tl) = Option.map (fun x ↦ (x.1, ↑x.2 s.tail)) (some v)
⊢ (op (Seq.cons s_hd s_tl)).destruct =
    Option.map (fun x ↦ (x.1, ↑x.2 s.tail))
      (match some v with
      | none => Option.map (fun x ↦ (x.1, ⟨↑x.2.2 ∘ fun x_1 ↦ ↑x.2.1 nil, ⋯⟩)) (T none)
      | some (hd, opf') => Option.map (fun x ↦ (x.1, ⟨↑x.2.2 ∘ ↑x.2.1 ∘ ↑opf', ⋯⟩)) (T (some hd)))

Tactic:
obtain ⟨hd, opf', op'⟩ := v

Goal state after:
case h.cons.some
α : Type u_1
motive : (Stream'.Seq α → Stream'.Seq α) → Prop
h_step :
  ∀ (op : Stream'.Seq α → Stream'.Seq α),
    motive op →
      ∃ T,
        ∀ (s : Stream'.Seq α),
          (op s).destruct =
            Option.map
              (fun x ↦
                match x with
                | (hd, opf, op') => (hd, ↑op' (↑opf s.tail)))
              (T s.head)
motive' : (Stream'.Seq α → Stream'.Seq α) → Prop :=
  fun op ↦ ∃ opf op', op = op' ∘ opf ∧ FriendlyOperation opf ∧ motive op'
opf op : Stream'.Seq α → Stream'.Seq α
h_opf : FriendlyOperation opf
h_op : motive op
T : Option α → Option (α × Subtype FriendlyOperation × Subtype motive)
hT :
  ∀ (s : Stream'.Seq α),
    (op s).destruct =
      Option.map
        (fun x ↦
          match x with
          | (hd, opf, op') => (hd, ↑op' (↑opf s.tail)))
        (T s.head)
s : Stream'.Seq α
s_hd : α
s_tl : Stream'.Seq α
hd : α
opf' : Stream'.Seq α → Stream'.Seq α
op' : FriendlyOperation opf'
hF : some (s_hd, s_tl) = Option.map (fun x ↦ (x.1, ↑x.2 s.tail)) (some (hd, ⟨opf', op'⟩))
⊢ (op (Seq.cons s_hd s_tl)).destruct =
    Option.map (fun x ↦ (x.1, ↑x.2 s.tail))
      (match some (hd, ⟨opf', op'⟩) with
      | none => Option.map (fun x ↦ (x.1, ⟨↑x.2.2 ∘ fun x_1 ↦ ↑x.2.1 nil, ⋯⟩)) (T none)
      | some (hd, opf') => Option.map (fun x ↦ (x.1, ⟨↑x.2.2 ∘ ↑x.2.1 ∘ ↑opf', ⋯⟩)) (T (some hd)))
Module: Mathlib.Tactic.ITauto

Goal state before:
pp: case and.and
⊢ Ordering

pp: case and.iff
⊢ Ordering

pp: case and.eq
⊢ Ordering

pp: case iff.and
⊢ Ordering

pp: case iff.iff
⊢ Ordering

pp: case iff.eq
⊢ Ordering

pp: case eq.and
⊢ Ordering

pp: case eq.iff
⊢ Ordering

pp: case eq.eq
⊢ Ordering

Tactic:
exacts [.eq, .lt, .lt, .gt, .eq, .lt, .gt, .gt, .eq]

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 (Pi.uniformSpace fun i ↦ α) ≤ UniformSpace.comap F (UniformFun.uniformSpace X α)

Tactic:
simp_rw [UniformSpace.comap, UniformSpace.le_def, uniformity_comap, Pi.uniformity,
    Filter.comap_iInf, comap_comap, 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.Topology.Algebra.Category.ProfiniteGrp.Completion

Goal state before:
pp: G : GrpCat
P : ProfiniteGrp.{u}
f : G ⟶ GrpCat.of ↑P.toProfinite.toTop
X Y : OpenNormalSubgroup ↑P.toProfinite.toTop
⊢ ∀ (f_1 : X ⟶ Y),
    ((Functor.const (OpenNormalSubgroup ↑P.toProfinite.toTop)).obj (limitCone (diagram G)).pt).map f_1 ≫
        (limitCone (diagram G)).π.app (preimage f Y) ≫ ofFiniteGrpHom (quotientMap f Y) =
      ((limitCone (diagram G)).π.app (preimage f X) ≫ ofFiniteGrpHom (quotientMap f X)) ≫ P.diagram.map f_1

Tactic:
g

Goal state after:
G : GrpCat
P : ProfiniteGrp.{u}
f : G ⟶ GrpCat.of ↑P.toProfinite.toTop
X Y : OpenNormalSubgroup ↑P.toProfinite.toTop
g : X ⟶ Y
⊢ ((Functor.const (OpenNormalSubgroup ↑P.toProfinite.toTop)).obj (limitCone (diagram G)).pt).map g ≫
      (limitCone (diagram G)).π.app (preimage f Y) ≫ ofFiniteGrpHom (quotientMap f Y) =
    ((limitCone (diagram G)).π.app (preimage f X) ≫ ofFiniteGrpHom (quotientMap f X)) ≫ P.diagram.map g
Module: Mathlib.Topology.Algebra.Group.SubmonoidClosure

Goal state before:
pp: G : Type u_1
inst✝³ : Group G
inst✝² : TopologicalSpace G
inst✝¹ : CompactSpace G
inst✝ : IsTopologicalGroup G
x : G
m : ℤ
y : G
hy : MapClusterPt y atTop fun x_1 ↦ x ^ x_1
⊢ MapClusterPt (x ^ m) atTop fun x_1 ↦ x ^ x_1

Tactic:
← mapClusterPt_atTop_zpow_iff_pow

Goal state after:
G : Type u_1
inst✝³ : Group G
inst✝² : TopologicalSpace G
inst✝¹ : CompactSpace G
inst✝ : IsTopologicalGroup G
x : G
m : ℤ
y : G
hy : MapClusterPt y atTop fun x_1 ↦ x ^ x_1
⊢ MapClusterPt (x ^ m) atTop fun x_1 ↦ x ^ x_1
Module: Mathlib.Topology.Algebra.Valued.WithZeroMulInt

Goal state before:
pp: R : Type u_1
Γ₀ : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrderedCommGroupWithZero Γ₀
inst✝¹ : MulArchimedean Γ₀
inst✝ : Valued R Γ₀
x : R
hx : Valued.v x < 1
y : (MonoidWithZeroHom.ofClass Valued.v).ValueGroup₀ˣ
v : Valuation R Γ₀ := Valued.v
n : ℕ
hn : Valued.v x ^ n < ↑((Units.map ↑MonoidWithZeroHom.ValueGroup₀.embedding) y)
m : ℕ
hm : n ≤ m
⊢ Valued.v.restrict x ^ m < ↑y

Tactic:
rw [← map_pow, Valuation.restrict_lt_iff_lt_embedding]

Goal state after:
R : Type u_1
Γ₀ : Type u_2
inst✝³ : Ring R
inst✝² : LinearOrderedCommGroupWithZero Γ₀
inst✝¹ : MulArchimedean Γ₀
inst✝ : Valued R Γ₀
x : R
hx : Valued.v x < 1
y : (MonoidWithZeroHom.ofClass Valued.v).ValueGroup₀ˣ
v : Valuation R Γ₀ := Valued.v
n : ℕ
hn : Valued.v x ^ n < ↑((Units.map ↑MonoidWithZeroHom.ValueGroup₀.embedding) y)
m : ℕ
hm : n ≤ m
⊢ Valued.v (x ^ m) < MonoidWithZeroHom.ValueGroup₀.embedding ↑y
Module: Mathlib.Topology.DerivedSet

Goal state before:
pp: case h₁
X : Type u_1
inst✝¹ : TopologicalSpace X
β : Type u_2
inst✝ : TopologicalSpace β
F : Filter X
x : X
h : AccPt x F
f : X → β
hf1 : ContinuousAt f x
hf2 : Function.Injective f
⊢ Filter.map f (𝓝[≠] x) ≤ 𝓝[≠] f x

Tactic:
apply tendsto_nhdsWithin_of_tendsto_nhds_of_eventually_within _ hf1.continuousWithinAt

Goal state after:
case h₁
X : Type u_1
inst✝¹ : TopologicalSpace X
β : Type u_2
inst✝ : TopologicalSpace β
F : Filter X
x : X
h : AccPt x F
f : X → β
hf1 : ContinuousAt f x
hf2 : Function.Injective f
⊢ ∀ᶠ (x_1 : X) in 𝓝[≠] x, f x_1 ∈ {f x}ᶜ
Module: Mathlib.Topology.DerivedSet

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
A : Set X
⊢ closure[inst✝] A = A ∪ derivedSet A

Tactic:
ext
  simp [closure_eq_cluster_pts, clusterPt_principal]

Goal state after:
Module: Mathlib.Topology.CWComplex.Classical.Subcomplex

Goal state before:
pp: case a
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝¹ : T2Space X
inst✝ : RelCWComplex C D
E : Subcomplex C
⊢ ⋃ n, ⋃ j, closedCell n ↑j ⊆ ↑E

Tactic:
exact iUnion₂_subset fun n i ↦ closedCell_subset_of_mem E i.2

Goal state after:
Module: Mathlib.Topology.CWComplex.Classical.Subcomplex

Goal state before:
pp: case a
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝¹ : T2Space X
inst✝ : RelCWComplex C D
E : Subcomplex C
⊢ ↑E ⊆ D ∪ ⋃ n, ⋃ j, closedCell n ↑j

Tactic:
rw [← E.union]
    apply union_subset_union_right
    apply iUnion₂_mono fun n i ↦ ?_
    exact openCell_subset_closedCell (C := C) n i

Goal state after:
Module: Mathlib.Topology.DerivedSet

Goal state before:
pp: case pos
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
U : Set X
hs : IsPreconnected U
a b : Set X
h : U ⊆ a ∪ b
ha : (U ∩ derivedSet a).Nonempty
hb : (U ∩ derivedSet b).Nonempty
hu : U.Nontrivial
⊢ (U ∩ (derivedSet a ∩ derivedSet b)).Nonempty

Tactic:
apply isPreconnected_closed_iff.mp hs
    · simp
    · simp
    · trans derivedSet U
      · apply hs.preperfect_of_nontrivial hu
      · rw [← derivedSet_union]
        exact derivedSet_mono _ _ h
    · exact ha
    · exact hb

Goal state after:
Module: Mathlib.Topology.DerivedSet

Goal state before:
pp: case neg
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
U : Set X
hs : IsPreconnected U
a b : Set X
h : U ⊆ a ∪ b
ha : (U ∩ derivedSet a).Nonempty
hb : (U ∩ derivedSet b).Nonempty
hu : ¬U.Nontrivial
⊢ (U ∩ (derivedSet a ∩ derivedSet b)).Nonempty

Tactic:
obtain ⟨x, hx⟩ := ha.left.exists_eq_singleton_or_nontrivial.resolve_right hu

Goal state after:
case neg
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
U : Set X
hs : IsPreconnected U
a b : Set X
h : U ⊆ a ∪ b
ha : (U ∩ derivedSet a).Nonempty
hb : (U ∩ derivedSet b).Nonempty
hu : ¬U.Nontrivial
x : X
hx : U = {x}
⊢ (U ∩ (derivedSet a ∩ derivedSet b)).Nonempty
Module: Mathlib.Topology.CantorBendixson

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
hs : IsClosed s
a : Ordinal.{u}
ha : sᵈ[a] ∈ fixedPoints ⇑relDerivedSet
⊢ Perfect (perfectKernel s)

Tactic:
rw [perfectKernel_eq_iteratedDerivedSet_of_mem_fixedPoints ha]

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
s : Set X
hs : IsClosed s
a : Ordinal.{u}
ha : sᵈ[a] ∈ fixedPoints ⇑relDerivedSet
⊢ Perfect sᵈ[a]
Module: Mathlib.Topology.Category.Compactum

Goal state before:
pp: case mp
X : Compactum
S : Set X.A
⊢ IsOpen Sᶜ → ∀ (F : Ultrafilter X.A), S ∈ F → X.str F ∈ S

pp: case mpr
X : Compactum
S : Set X.A
⊢ (∀ (F : Ultrafilter X.A), S ∈ F → X.str F ∈ S) → IsOpen Sᶜ

Tactic:
· intro cond F h
    by_contra c
    specialize cond F c
    rw [compl_mem_iff_notMem] at cond
    contradiction

Goal state after:
case mpr
X : Compactum
S : Set X.A
⊢ (∀ (F : Ultrafilter X.A), S ∈ F → X.str F ∈ S) → IsOpen Sᶜ
Module: Mathlib.Topology.Convenient.GeneratedBy

Goal state before:
pp: ι : Type t
X : ι → Type u
inst✝² : (i : ι) → TopologicalSpace (X i)
Y : Type v
tY : TopologicalSpace Y
Z : Type v'
inst✝¹ : TopologicalSpace Z
inst✝ : IsGeneratedBy X Y
g : Y → Z
⊢ Continuous[tY, _] (⇑WithGeneratedByTopology.equiv.symm ∘ g) ↔ Continuous[tY, inst✝¹] g

Tactic:
refine ⟨fun hg ↦ WithGeneratedByTopology.continuous_equiv.comp hg, fun hg ↦ ?_⟩

Goal state after:
ι : Type t
X : ι → Type u
inst✝² : (i : ι) → TopologicalSpace (X i)
Y : Type v
tY : TopologicalSpace Y
Z : Type v'
inst✝¹ : TopologicalSpace Z
inst✝ : IsGeneratedBy X Y
g : Y → Z
hg : Continuous[tY, inst✝¹] g
⊢ Continuous[tY, _] (⇑WithGeneratedByTopology.equiv.symm ∘ g)
Module: Mathlib.Topology.Convenient.GeneratedBy

Goal state before:
pp: ι : Type t
X : ι → Type u
inst✝¹ : (i : ι) → TopologicalSpace (X i)
Y : Type v
tY : TopologicalSpace Y
Z : Type v'
inst✝ : TopologicalSpace Z
U : Set (WithGeneratedByTopology X (WithGeneratedByTopology X Y))
hU :
  ∀ ⦃i : ι⦄ (f : C(X i, WithGeneratedByTopology X Y)),
    IsOpen[inst✝¹ i] (⇑f ⁻¹' ⇑WithGeneratedByTopology.equiv.symm ⁻¹' U)
i : ι
f : C(X i, Y)
j : ι
⊢ ∀ (f_1 : C(X j, X i)), Continuous[inst✝¹ j, _] ((⇑WithGeneratedByTopology.equiv.symm ∘ ⇑f) ∘ ⇑f_1)

Tactic:
g

Goal state after:
ι : Type t
X : ι → Type u
inst✝¹ : (i : ι) → TopologicalSpace (X i)
Y : Type v
tY : TopologicalSpace Y
Z : Type v'
inst✝ : TopologicalSpace Z
U : Set (WithGeneratedByTopology X (WithGeneratedByTopology X Y))
hU :
  ∀ ⦃i : ι⦄ (f : C(X i, WithGeneratedByTopology X Y)),
    IsOpen[inst✝¹ i] (⇑f ⁻¹' ⇑WithGeneratedByTopology.equiv.symm ⁻¹' U)
i : ι
f : C(X i, Y)
j : ι
g : C(X j, X i)
⊢ Continuous[inst✝¹ j, _] ((⇑WithGeneratedByTopology.equiv.symm ∘ ⇑f) ∘ ⇑g)
Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic

Goal state before:
pp: I : Type u
J : I → Prop
inst✝ : (i : I) → Decidable (J i)
x : I → Bool
h : ∀ (i : I), x i ≠ false → J i
⊢ Proj J x = x

Tactic:
ext i
  simp only [Proj, ite_eq_left_iff]
  contrapose!
  simpa only [ne_comm] using h i

Goal state after:
Module: Mathlib.Topology.Category.Compactum

Goal state before:
pp: X Y : Compactum
f : X ⟶ Y
x : X.A
⊢ ∀ (g : Ultrafilter X.A), ↑g ≤ 𝓝 x → Tendsto (⇑(ConcreteCategory.hom f)) (↑g) (𝓝 ((ConcreteCategory.hom f) x))

Tactic:
g

Goal state after:
X Y : Compactum
f : X ⟶ Y
x : X.A
g : Ultrafilter X.A
⊢ ↑g ≤ 𝓝 x → Tendsto (⇑(ConcreteCategory.hom f)) (↑g) (𝓝 ((ConcreteCategory.hom f) x))
Module: Mathlib.Topology.CWComplex.Classical.Basic

Goal state before:
pp: X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝¹ : RelCWComplex C D
inst✝ : T2Space X
A : Set X
n : ℕ
hn : ∀ m ≤ n, ∀ (j : cell C m), IsClosed[t] (A ∩ closedCell m j)
j : cell C (n + 1)
hD : IsClosed[t] (A ∩ D)
I : (m : ℕ) → Finset (cell C m)
hI : cellFrontier (n + 1) j ⊆ D ∪ ⋃ m, ⋃ (_ : m < n + 1), ⋃ j ∈ I m, closedCell m j
m : ℕ
mlt : m < n + 1
⊢ IsClosed[t] (⋃ x, A ∩ closedCell m ↑x)

Tactic:
exact isClosed_iUnion_of_finite (fun ⟨j, _⟩ ↦ hn m (Nat.le_of_lt_succ mlt) j)

Goal state after:
Module: Mathlib.Topology.Category.Compactum

Goal state before:
pp: D : CompHaus
x✝ : Set (Compactum.ofTopologicalSpace ↑D.toTop).A
h1 : IsOpen x✝
F✝ : Ultrafilter ↑D.1
h2 : F✝.lim ∈ id ⁻¹' x✝
⊢ id ⁻¹' x✝ ∈ ↑F✝

Tactic:
exact h1 _ h2

Goal state after:
Module: Mathlib.Topology.Category.Profinite.Nobeling.Successor

Goal state before:
pp: case inl
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
ho : o < Ordinal.type fun x1 x2 ↦ x1 < x2
x : I → Bool
hx : x ∈ C0 C ho
i : I
hi✝ : o ≤ ord I i
hi : o < ord I i
hsC : o < ord I i → x i = false
⊢ false = x i

Tactic:
exact (hsC hi).symm

Goal state after: