mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Order.SuccPred

Goal state before:
pp: case refine_1
α : Type u_1
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
a : α
inst✝¹ : SuccOrder α
inst✝ : NoMaxOrder α
a✝ : Nontrivial α
h : IsOpen[inst✝³] {a}
ha : IsSuccLimit a
⊢ False

Tactic:
obtain ⟨l, u, h₁, h₂⟩ := mem_nhds_iff_exists_Ioo_subset' (by simpa using ha.not_isMin)
      (by simpa only [not_isMax_iff] using not_isMax a) |>.mp (h.mem_nhds (mem_singleton a))

Goal state after:
case refine_1
α : Type u_1
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
a : α
inst✝¹ : SuccOrder α
inst✝ : NoMaxOrder α
a✝ : Nontrivial α
h : IsOpen[inst✝³] {a}
ha : IsSuccLimit a
l u : α
h₁ : a ∈ Ioo l u
h₂ : Ioo l u ⊆ {a}
⊢ False
Module: Mathlib.SetTheory.Ordinal.CantorNormalForm

Goal state before:
pp: case zero
b e x : Ordinal.{u_1}
h : ∀ e' ∈ support 0, e' ≤ e
⊢ eval b (single e x + 0) = b ^ e * x + eval b 0

Tactic:
| zero =>

Goal state after:
Module: Mathlib.SetTheory.Ordinal.CantorNormalForm

Goal state before:
pp: case zero
b : Ordinal.{u_1}
f₂ : Ordinal.{u_1} →₀ Ordinal.{u_1}
h : ∀ e₁ ∈ support 0, ∀ e₂ ∈ f₂.support, e₂ ≤ e₁
⊢ eval b (0 + f₂) = eval b 0 + eval b f₂

Tactic:
| zero =>

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: case zero
o : ONote
b b✝ : Ordinal.{0}
⊢ repr 0 < ω ^ b✝

Tactic:
| zero =>

Goal state after:
Module: Mathlib.SetTheory.Ordinal.CantorNormalForm

Goal state before:
pp: case zero
b e : Ordinal.{u_1}
hb : ∀ (e' : Ordinal.{u_1}), 0 e' < b
he : ∀ e' ∈ support 0, e' < e
⊢ eval b 0 < b ^ e

Tactic:
| zero =>

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: case zero
o : ONote
b₁ b₂ b✝ : Ordinal.{0}
bb : b✝ ≤ b₂
⊢ NFBelow 0 b₂

Tactic:
| zero =>

Goal state after:
Module: Mathlib.SetTheory.Ordinal.CantorNormalForm

Goal state before:
pp: b e' x : Ordinal.{u_1}
f : Ordinal.{u_1} →₀ Ordinal.{u_1}
hf : ∀ c ∈ f.support, c < e'
hx : x ≠ 0
IH : ∀ {e : Ordinal.{u_1}}, (∀ (e' : Ordinal.{u_1}), f e' < b) → (∀ e' ∈ f.support, e' < e) → eval b f < b ^ e
e : Ordinal.{u_1}
hb : ∀ (e'_1 : Ordinal.{u_1}), (single e' x + f) e'_1 < b
he : ∀ e'_1 ∈ (single e' x + f).support, e'_1 < e
he' : e' ∉ f.support
⊢ ∀ (e' : Ordinal.{u_1}), f e' < b

Tactic:
intro a

Goal state after:
b e' x : Ordinal.{u_1}
f : Ordinal.{u_1} →₀ Ordinal.{u_1}
hf : ∀ c ∈ f.support, c < e'
hx : x ≠ 0
IH : ∀ {e : Ordinal.{u_1}}, (∀ (e' : Ordinal.{u_1}), f e' < b) → (∀ e' ∈ f.support, e' < e) → eval b f < b ^ e
e : Ordinal.{u_1}
hb : ∀ (e'_1 : Ordinal.{u_1}), (single e' x + f) e'_1 < b
he : ∀ e'_1 ∈ (single e' x + f).support, e'_1 < e
he' : e' ∉ f.support
a : Ordinal.{u_1}
⊢ f a < b
Module: Mathlib.SetTheory.Ordinal.CantorNormalForm

Goal state before:
pp: b o : Ordinal.{u_1}
⊢ ∀ a ∈ CNF b o, ∀ (b_1 : Ordinal.{u_1}), b ^ a.1 * (coeff b o) a.1 + b_1 = b ^ a.1 * a.2 + b_1

Tactic:
intro a

Goal state after:
b o : Ordinal.{u_1}
a : Ordinal.{u_1} × Ordinal.{u_1}
⊢ a ∈ CNF b o → ∀ (b_1 : Ordinal.{u_1}), b ^ a.1 * (coeff b o) a.1 + b_1 = b ^ a.1 * a.2 + b_1
Module: Mathlib.SetTheory.Ordinal.CantorNormalForm

Goal state before:
pp: case zero
b : Ordinal.{u_1}
hb : 1 < b
hf : ∀ (e : Ordinal.{u_1}), 0 e < b
⊢ coeff b (eval b 0) = 0

Tactic:
| zero =>

Goal state after:
Module: Mathlib.SetTheory.ZFC.PSet

Goal state before:
pp: α : Type u
A : α → PSet.{u}
β : Type u
B : β → PSet.{u}
H : (mk α A).Equiv (mk β B)
⊢ ∀ y ∈ mk β B, Acc (fun x1 x2 ↦ x1 ∈ x2) y

Tactic:
by
      rintro ⟨γ, C⟩ ⟨b, hc⟩
      obtain ⟨a, ha⟩ := H.exists_right b
      have H := ha.trans hc.symm
      rw [mk_func] at H
      exact mem_wf_aux H

Goal state after:
Module: Mathlib.SetTheory.ZFC.Basic

Goal state before:
pp: x y : ZFSet.{u}
⊢ y ∈ ⋃₀ {x} ↔ y ∈ x

Tactic:
mem_sUnion,

Goal state after:
x y : ZFSet.{u}
⊢ (∃ z ∈ {x}, y ∈ z) ↔ y ∈ x
Module: Mathlib.SetTheory.ZFC.Rank

Goal state before:
pp: case mp
α✝¹ : Type u_1
A✝¹ : α✝¹ → PSet.{u_1}
α✝ : Type u_1
A✝ : α✝ → PSet.{u_1}
αβ : ∀ (a : α✝¹), ∃ b, (A✝¹ a).Equiv (A✝ b)
βα : ∀ (b : α✝), ∃ a, (A✝¹ a).Equiv (A✝ b)
x✝ : Ordinal.{u_1}
⊢ ∀ (x : α✝¹), succ (A✝¹ x).rank = x✝ → ∃ y, succ (A✝ y).rank = x✝

Tactic:
intro a

Goal state after:
case mp
α✝¹ : Type u_1
A✝¹ : α✝¹ → PSet.{u_1}
α✝ : Type u_1
A✝ : α✝ → PSet.{u_1}
αβ : ∀ (a : α✝¹), ∃ b, (A✝¹ a).Equiv (A✝ b)
βα : ∀ (b : α✝), ∃ a, (A✝¹ a).Equiv (A✝ b)
x✝ : Ordinal.{u_1}
a : α✝¹
⊢ succ (A✝¹ a).rank = x✝ → ∃ y, succ (A✝ y).rank = x✝
Module: Mathlib.SetTheory.ZFC.Rank

Goal state before:
pp: case mpr
α✝¹ : Type u_1
A✝¹ : α✝¹ → PSet.{u_1}
α✝ : Type u_1
A✝ : α✝ → PSet.{u_1}
αβ : ∀ (a : α✝¹), ∃ b, (A✝¹ a).Equiv (A✝ b)
βα : ∀ (b : α✝), ∃ a, (A✝¹ a).Equiv (A✝ b)
x✝ : Ordinal.{u_1}
⊢ ∀ (x : α✝), succ (A✝ x).rank = x✝ → ∃ y, succ (A✝¹ y).rank = x✝

Tactic:
intro a

Goal state after:
case mpr
α✝¹ : Type u_1
A✝¹ : α✝¹ → PSet.{u_1}
α✝ : Type u_1
A✝ : α✝ → PSet.{u_1}
αβ : ∀ (a : α✝¹), ∃ b, (A✝¹ a).Equiv (A✝ b)
βα : ∀ (b : α✝), ∃ a, (A✝¹ a).Equiv (A✝ b)
x✝ : Ordinal.{u_1}
a : α✝
⊢ succ (A✝ a).rank = x✝ → ∃ y, succ (A✝¹ y).rank = x✝
Module: Mathlib.SetTheory.ZFC.Class

Goal state before:
pp: x : Class.{u}
y : ZFSet.{u}
⊢ (⋂₀ x) y ↔ ∀ (z : ZFSet.{u}), x z → y ∈ z

Tactic:
refine ⟨fun hxy z hxz => hxy _ ⟨z, rfl, hxz⟩, ?_⟩
  rintro H - ⟨z, rfl, hxz⟩
  exact H _ hxz

Goal state after:
Module: Mathlib.SetTheory.ZFC.VonNeumann

Goal state before:
pp: o : Ordinal.{u_1}
⊢ (V_ o).rank ≤ o

Tactic:
rw [← subset_vonNeumann]

Goal state after:
Module: Mathlib.SetTheory.ZFC.VonNeumann

Goal state before:
pp: case zero
⊢ (V_ 0).card = preBeth 0

Tactic:
| zero =>

Goal state after:
Module: Mathlib.SetTheory.ZFC.Ordinal

Goal state before:
pp: ⊢ Monotone toZFSet

Tactic:
intro a

Goal state after:
a : Ordinal.{u_1}
⊢ ∀ ⦃b : Ordinal.{u_1}⦄, a ≤ b → a.toZFSet ⊆ b.toZFSet
Module: Mathlib.Tactic.Algebra.Lemmas

Goal state before:
pp: n : ℕ
R : Type u_3
A : Type u_4
inst✝³ : CommSemiring R
inst✝² : CommSemiring A
inst✝¹ : Algebra R A
inst✝ : n.AtLeastTwo
a : A
⊢ OfNat.ofNat n • a = OfNat.ofNat n * a

Tactic:
← nat_rawCast_2

Goal state after:
n : ℕ
R : Type u_3
A : Type u_4
inst✝³ : CommSemiring R
inst✝² : CommSemiring A
inst✝¹ : Algebra R A
inst✝ : n.AtLeastTwo
a : A
⊢ n.rawCast • a = n.rawCast * a
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: case zero
e a0 a : ONote
inst✝² : e.NF
inst✝¹ : a0.NF
inst✝ : a.NF
k : ℕ
⊢ (match k, 0 with
    | x, 0 => 0
    | 0, m.succ => e.oadd m.succPNat 0
    | k.succ, m => (e + a0.mulNat k).scale a + e.opowAux a0 a k m).NF

Tactic:
| zero =>

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: case succ.zero
e a0 a : ONote
inst✝² : e.NF
inst✝¹ : a0.NF
inst✝ : a.NF
m : ℕ
⊢ (match 0, m + 1 with
    | x, 0 => 0
    | 0, m.succ => e.oadd m.succPNat 0
    | k.succ, m => (e + a0.mulNat k).scale a + e.opowAux a0 a k m).NF

Tactic:
| zero =>

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: case zero
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
R' : Ordinal.{0} := (opowAux 0 a0 (a0.oadd n a' * ↑m) 0 m).repr
⊢ (0 ≠ 0 → R' < (ω ^ a0.repr) ^ succ ↑0) ∧
    (ω ^ a0.repr) ^ ↑0 * (ω ^ a0.repr * ↑↑n + a'.repr) + R' = (ω ^ a0.repr * ↑↑n + a'.repr + ↑m) ^ succ ↑0

Tactic:
| zero =>

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: case neg
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
k0 : ¬k = 0
⊢ R < ω ^ (a0.repr * succ ↑k)

Tactic:
rw [opow_mul]
      exact IH.1 k0

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

Goal state before:
pp: f b : ℝ → ℝ
exp1 exp2 : ℝ
h_lt : exp1 ≤ exp2
h : Majorized f b exp1
⊢ Majorized f b exp2

Tactic:
simp only [Majorized] at *
  exact fun exp' h_exp ↦ h _ (by linarith)

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

Goal state before:
pp: case hl
f g : ℝ → ℝ
a b : ℝ
hf : ∀ᶠ (x : ℝ) in atTop, 0 < f x
hg : Tendsto g atTop atTop
h : (Real.log ∘ f) =o[atTop] (Real.log ∘ g)
hb : 0 < b
⊢ Real.exp ∘ (b • Real.log ∘ g - a • Real.log ∘ f) =ᶠ[atTop] fun x ↦ (g ^ b) x / (f ^ a) x

Tactic:
refine (hf.and (hg.eventually_gt_atTop 0)).mono (fun x ⟨hf, hg⟩ ↦ ?_)

Goal state after:
case hl
f g : ℝ → ℝ
a b : ℝ
hf✝ : ∀ᶠ (x : ℝ) in atTop, 0 < f x
hg✝ : Tendsto g atTop atTop
h : (Real.log ∘ f) =o[atTop] (Real.log ∘ g)
hb : 0 < b
x : ℝ
x✝ : 0 < f x ∧ 0 < g x
hf : 0 < f x
hg : 0 < g x
⊢ (Real.exp ∘ (b • Real.log ∘ g - a • Real.log ∘ f)) x = (fun x ↦ (g ^ b) x / (f ^ a) x) x
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion

Goal state before:
pp: α : Type u_1
op : Stream'.Seq α → Stream'.Seq α
a : α
s t : Stream'.Seq α
h :
  op (Seq.cons a s) = nil ∧ op (Seq.cons a t) = nil ∨
    ∃ hd s' t', op (Seq.cons a s) = Seq.cons hd s' ∧ op (Seq.cons a t) = Seq.cons hd t'
⊢ (op (Seq.cons a s)).head = (op (Seq.cons a t)).head

Tactic:
generalize op (Seq.cons a s) = s' at *

Goal state after:
α : Type u_1
op : Stream'.Seq α → Stream'.Seq α
a : α
s t s' : Stream'.Seq α
h : s' = nil ∧ op (Seq.cons a t) = nil ∨ ∃ hd s'_1 t', s' = Seq.cons hd s'_1 ∧ op (Seq.cons a t) = Seq.cons hd t'
⊢ s'.head = (op (Seq.cons a t)).head
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion

Goal state before:
pp: case cons
α : Type u_1
op : Stream'.Seq α → Stream'.Seq α
h : FriendlyOperation op
s_hd : α
s_tl : Stream'.Seq α
⊢ (op (Seq.cons s_hd s_tl)).destruct =
    Option.map
      (fun x ↦
        match x with
        | (hd, op') => (hd, ↑op' (Seq.cons s_hd s_tl).tail))
      (match (Seq.cons s_hd s_tl).head with
      | none =>
        match (op nil).destruct with
        | none => none
        | some (t_hd, t_tl) => some (t_hd, ⟨fun x ↦ t_tl, ⋯⟩)
      | some s_hd =>
        match (op (Seq.cons s_hd nil)).destruct with
        | none => none
        | some (t_hd, snd) => some (t_hd, ⟨fun s_tl ↦ (op (Seq.cons s_hd s_tl)).tail, ⋯⟩))

Tactic:
simp only [Seq.tail_cons, Seq.head_cons]

Goal state after:
case cons
α : Type u_1
op : Stream'.Seq α → Stream'.Seq α
h : FriendlyOperation op
s_hd : α
s_tl : Stream'.Seq α
⊢ (op (Seq.cons s_hd s_tl)).destruct =
    Option.map (fun x ↦ (x.1, ↑x.2 s_tl))
      (match (op (Seq.cons s_hd nil)).destruct with
      | none => none
      | some (t_hd, snd) => some (t_hd, ⟨fun s_tl ↦ (op (Seq.cons s_hd s_tl)).tail, ⋯⟩))
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basic

Goal state before:
pp: case zero
basis_hd : ℝ → ℝ
basis_tl : Basis
r : ℝ
⊢ (Multiseries.monomialRpow basis_hd basis_tl 0 r).Sorted

Tactic:
| zero =>

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

Goal state before:
pp: case cons.zero
r : ℝ
basis_hd : ℝ → ℝ
basis_tl : List (ℝ → ℝ)
h_basis : WellFormedBasis (basis_hd :: basis_tl)
⊢ (mk (Multiseries.monomialRpow basis_hd basis_tl (↑0) r) ((basis_hd :: basis_tl)[↑0] ^ r)).Approximates

Tactic:
| zero =>

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

Goal state before:
pp: case zero
α : 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, op') => (hd, ↑op' s.tail))
              (T s.head)
op : Stream'.Seq α → Stream'.Seq α
h_base : motive op
s t : Stream'.Seq α
hn : dist s t ≤ 2⁻¹ ^ 0
⊢ dist (op s) (op t) ≤ 2⁻¹ ^ 0

Tactic:
| zero =>

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: case zero
⊢ zero.FundamentalSequenceProp zero.fundamentalSequence

Tactic:
| zero =>

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

Goal state before:
pp: case zero
α : Type u_1
γ : Type u_3
op : γ → Stream'.Seq α → Stream'.Seq α
inst✝ : FriendlyOperationClass op
motive : Stream'.Seq α → Stream'.Seq α → Prop
step :
  ∀ (u v : Stream'.Seq α),
    motive u v → u = v ∨ ∃ hd u' v' c, u = Seq.cons hd (op c u') ∧ v = Seq.cons hd (op c v') ∧ motive u' v'
s t : Stream'.Seq α
base : motive s t
⊢ dist s t ≤ 2⁻¹ ^ 0

Tactic:
| zero =>

Goal state after:
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: case zero
C : NONote → Sort u_1
H0 : C 0
H1 : (e : NONote) → (n : ℕ+) → (a : NONote) → (h : a.below e) → C e → C a → C (e.oadd n a h)
h : ONote.zero.NF
⊢ C ⟨ONote.zero, h⟩

Tactic:
| zero =>

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:
Nat.cast_id,

Goal state after:
α : Type u_1
inst✝ : Semiring α
a✝ : α
a b n : ℕ
x✝ : CharP α ↑n
h : a✝ = ↑a
⊢ ↑a ^ b = ↑((a.pow b).mod n)
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:
← hs,

Goal state after:
m n : ℕ
s : Finset ℕ
hmn : m.ble n = true
hs : Icc (m + 1) n = s
⊢ Icc m n = insert m (Icc (m + 1) n)
Module: Mathlib.Tactic.Simproc.FinsetInterval

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

Tactic:
← hs,

Goal state after:
m n : ℕ
s : Finset ℕ
hs : Icc m n = s
⊢ Ico m (n + 1) = Icc m n
Module: Mathlib.Tactic.Simproc.FinsetInterval

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

Tactic:
← hs,

Goal state after:
m n : ℕ
s : Finset ℕ
hs : Icc (m + 1) n = s
⊢ Ioc m n = Icc (m + 1) n
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:
← hs,

Goal state after:
m n : ℕ
s : Finset ℕ
hs : Icc (m + 1) (n - 1) = s
⊢ Ioo m n = Icc (m + 1) (n - 1)
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:
← hs,

Goal state after:
m n : ℤ
s : Finset ℤ
hmn : m ≤ n
hs : Icc (m + 1) n = s
⊢ Icc m n = insert m (Icc (m + 1) n)
Module: Mathlib.Tactic.Simproc.FinsetInterval

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

Tactic:
← hs,

Goal state after:
m n : ℤ
s : Finset ℤ
hs : Icc m (n - 1) = s
⊢ Ico m n = Icc m (n - 1)
Module: Mathlib.Tactic.Simproc.FinsetInterval

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

Tactic:
← hs,

Goal state after:
m n : ℤ
s : Finset ℤ
hs : Icc (m + 1) n = s
⊢ Ioc m n = Icc (m + 1) n
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:
← hs,

Goal state after:
m n : ℤ
s : Finset ℤ
hs : Icc (m + 1) (n - 1) = s
⊢ Ioo m n = Icc (m + 1) (n - 1)
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:
intro a

Goal state after:
α : Type u
β : Type v
inst✝² : DecidableEq α
inst✝¹ : Zero β
inst✝ : DecidableEq β
tf : TotalFunction α β
a : α
⊢ a ∈ tf.zeroDefaultSupp ↔ tf.zeroDefault.apply a ≠ 0
Module: Mathlib.Testing.Plausible.Functions

Goal state before:
pp: case pos
α : Type u
inst✝ : DecidableEq α
x val x' : α
xs : List α
xs_ih :
  ∀ {ys : List α},
    xs.Nodup →
      dlookup x (map Prod.toSigma (xs.zip ys)) = some val → ys.Nodup → xs.length = ys.length → (val ∈ ys ↔ x ∈ xs)
h₀ : (x' :: xs).Nodup
y : α
ys : List α
h₂ : (y :: ys).Nodup
h₁ : (x' :: xs).length = (y :: ys).length
h : x' = x
h₃ : some y = some val
⊢ val ∈ y :: ys ↔ x ∈ x' :: xs

Tactic:
Option.some_inj

Goal state after:
case pos
α : Type u
inst✝ : DecidableEq α
x val x' : α
xs : List α
xs_ih :
  ∀ {ys : List α},
    xs.Nodup →
      dlookup x (map Prod.toSigma (xs.zip ys)) = some val → ys.Nodup → xs.length = ys.length → (val ∈ ys ↔ x ∈ xs)
h₀ : (x' :: xs).Nodup
y : α
ys : List α
h₂ : (y :: ys).Nodup
h₁ : (x' :: xs).length = (y :: ys).length
h : x' = x
h₃ : y = val
⊢ val ∈ y :: ys ↔ x ∈ x' :: xs
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:
isUniformInducing_iff_uniformSpace,

Goal state after:
ι : 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✝¹ ↔ IsUniformInducing F
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✝¹ ↔ IsUniformInducing F

Tactic:
isUniformInducing_iff_uniformSpace,

Goal state after:
ι : 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 (Pi.uniformSpace fun a ↦ α) = inst✝¹
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:
isUniformInducing_iff_uniformSpace,

Goal state after:
ι : 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✝ ↔
    IsUniformInducing ((⋃₀ 𝔖).domRestrict ∘ F)
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✝ ↔
    IsUniformInducing ((⋃₀ 𝔖).domRestrict ∘ F)

Tactic:
isUniformInducing_iff_uniformSpace,

Goal state after:
ι : 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 ((⋃₀ 𝔖).domRestrict ∘ F) (Pi.uniformSpace fun a ↦ α) = inst✝
Module: Mathlib.Topology.Algebra.Category.ProfiniteGrp.Completion

Goal state before:
pp: case h
G : GrpCat
U : Set ↑(completion G).toProfinite.toTop
s : Set ((j : FiniteIndexNormalSubgroup ↑G) → ↑((diagram G).obj j).toProfinite.toTop)
hsO : IsOpen s
hsv : Subtype.val ⁻¹' s = U
spc : (j : FiniteIndexNormalSubgroup ↑G) → ↑((diagram G).obj j).toProfinite.toTop
hspc : spc ∈ limitConePtAux (diagram G)
uDefaultSpec : ↑⟨spc, hspc⟩ ∈ s
J : Finset (FiniteIndexNormalSubgroup ↑G)
fJ : (a : FiniteIndexNormalSubgroup ↑G) → Set ↑((diagram G).obj a).toProfinite.toTop
hJ1 : ∀ a ∈ J, IsOpen (fJ a) ∧ ↑⟨spc, hspc⟩ a ∈ fJ a
hJ2 : (↑J).pi fJ ⊆ s
M : Subgroup ↑G := ⋯
hM : M.Normal
hMFinite : M.FiniteIndex
m : FiniteIndexNormalSubgroup ↑G := ⋯
origin : ↑G
horigin : (QuotientGroup.mk' M) origin = spc m
⊢ ↑(etaFn G origin) ∈ (↑J).pi fJ

Tactic:
intro a

Goal state after:
case h
G : GrpCat
U : Set ↑(completion G).toProfinite.toTop
s : Set ((j : FiniteIndexNormalSubgroup ↑G) → ↑((diagram G).obj j).toProfinite.toTop)
hsO : IsOpen s
hsv : Subtype.val ⁻¹' s = U
spc : (j : FiniteIndexNormalSubgroup ↑G) → ↑((diagram G).obj j).toProfinite.toTop
hspc : spc ∈ limitConePtAux (diagram G)
uDefaultSpec : ↑⟨spc, hspc⟩ ∈ s
J : Finset (FiniteIndexNormalSubgroup ↑G)
fJ : (a : FiniteIndexNormalSubgroup ↑G) → Set ↑((diagram G).obj a).toProfinite.toTop
hJ1 : ∀ a ∈ J, IsOpen (fJ a) ∧ ↑⟨spc, hspc⟩ a ∈ fJ a
hJ2 : (↑J).pi fJ ⊆ s
M : Subgroup ↑G := ⨅ j, (↑j).toSubgroup
hM : M.Normal
hMFinite : M.FiniteIndex
m : FiniteIndexNormalSubgroup ↑G := { toSubgroup := M, isNormal' := ⋯, isFiniteIndex' := ⋯ }
origin : ↑G
horigin : (QuotientGroup.mk' M) origin = spc m
a : FiniteIndexNormalSubgroup ↑G
⊢ a ∈ ↑J → ↑(etaFn G origin) a ∈ fJ a
Module: Mathlib.Topology.Algebra.Group.CompactOpen

Goal state before:
pp: case zero
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
inst✝ : LocallyCompactSpace X
V : ℕ → Set Y
hV : ∀ {n : ℕ} {x : Y}, x ∈ V n → x * x ∈ V n → x ∈ V (n + 1)
hVo : (𝓝 1).HasBasis (fun x ↦ True) V
U0 : Set X
hU0c : IsCompact U0
hU0o : U0 ∈ 𝓝 1
U_aux : ℕ → ↑{S | S ∈ 𝓝 1} :=
  fun t ↦
    Nat.rec ⟨U0, hU0o⟩
      (fun x S ↦
        let h := ⋯;
        ⟨Classical.choose h, ⋯⟩)
      t
U : ℕ → Set X := fun n ↦ ↑(U_aux n)
hU1 : ∀ (n : ℕ), U n ∈ 𝓝 1
hU2 : ∀ (n : ℕ), U (n + 1) * U (n + 1) ⊆ U n
hU3 : ∀ (n : ℕ), U (n + 1) ⊆ U n
f : X →* Y
hf : Set.MapsTo (⇑f) (U 0) (V 0)
⊢ Set.MapsTo (⇑f) (U 0) (V 0)

Tactic:
| zero =>

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

Goal state before:
pp: case refine_1
A : Type u_1
B : Type u_2
C : Type u_3
G : Type u_4
H : Type u_5
inst✝¹² : Monoid A
inst✝¹¹ : Monoid B
inst✝¹⁰ : Monoid C
inst✝⁹ : CommGroup G
inst✝⁸ : Group H
inst✝⁷ : TopologicalSpace A
inst✝⁶ : TopologicalSpace B
inst✝⁵ : TopologicalSpace C
inst✝⁴ : TopologicalSpace G
inst✝³ : TopologicalSpace H
inst✝² : IsTopologicalGroup G
inst✝¹ : IsTopologicalGroup H
inst✝ : CompactSpace A
V : Set (PontryaginDual A) := {ψ | Set.MapsTo (⇑ψ) Set.univ (Circle.centeredArc (π / 2))}
hVopen : IsOpen V
ψ : PontryaginDual A
hψ : ψ ∈ V
a : A
⊢ ψ a = 1 a

Tactic:
refine Circle.eq_one_of_forall_pow_mem_centeredArc_pi_div_two fun n hn ↦ ?_

Goal state after:
case refine_1
A : Type u_1
B : Type u_2
C : Type u_3
G : Type u_4
H : Type u_5
inst✝¹² : Monoid A
inst✝¹¹ : Monoid B
inst✝¹⁰ : Monoid C
inst✝⁹ : CommGroup G
inst✝⁸ : Group H
inst✝⁷ : TopologicalSpace A
inst✝⁶ : TopologicalSpace B
inst✝⁵ : TopologicalSpace C
inst✝⁴ : TopologicalSpace G
inst✝³ : TopologicalSpace H
inst✝² : IsTopologicalGroup G
inst✝¹ : IsTopologicalGroup H
inst✝ : CompactSpace A
V : Set (PontryaginDual A) := {ψ | Set.MapsTo (⇑ψ) Set.univ (Circle.centeredArc (π / 2))}
hVopen : IsOpen V
ψ : PontryaginDual A
hψ : ψ ∈ V
a : A
n : ℕ
hn : n > 0
⊢ ψ a ^ n ∈ Circle.centeredArc (π / 2)
Module: Mathlib.Topology.Baire.BaireMeasurable

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
s : Set α
h : IsOpen[inst✝] s
this✝¹ : MeasurableSpace α := borel α
this✝ : BorelSpace α
⊢ BaireMeasurableSet s

Tactic:
exact h.measurableSet.baireMeasurableSet

Goal state after:
Module: Mathlib.Topology.DerivedSet

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
A : Set X
h : derivedSet A ⊆ A
⊢ ∀ (a : X), ClusterPt a (𝓟 A) → a ∈ A

Tactic:
intro a

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
A : Set X
h : derivedSet A ⊆ A
a : X
⊢ ClusterPt a (𝓟 A) → a ∈ A
Module: Mathlib.Topology.CantorBendixson

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
hs : IsClosed s
⊢ ∀ (a : Ordinal.{u}), IsClosed sᵈ[a]

Tactic:
intro a

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
s : Set X
hs : IsClosed s
a : Ordinal.{u}
⊢ IsClosed sᵈ[a]