mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.SetTheory.Ordinal.FixedPointApproximants

Goal state before:
pp: α : Type u
inst✝ : CompleteLattice α
f : α →o α
x : α
a : Ordinal.{u}
⊢ ∀ ⦃b : Ordinal.{u}⦄, a ≤ b → lfpApprox f x a ≤ lfpApprox f x b

Tactic:
b

Goal state after:
α : Type u
inst✝ : CompleteLattice α
f : α →o α
x : α
a b : Ordinal.{u}
⊢ a ≤ b → lfpApprox f x a ≤ lfpApprox f x b
Module: Mathlib.SetTheory.Ordinal.FixedPointApproximants

Goal state before:
pp: α : Type u
inst✝ : CompleteLattice α
f : α →o α
⊢ ∃ y, lfpApprox f ⊥ (succ #α).ord = ↑y

Tactic:
simpa only [Subtype.exists, mem_fixedPoints, exists_prop, exists_eq_right'] using
        lfpApprox_ord_mem_fixedPoint f bot_le

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

Goal state before:
pp: case pos
b e x y : Ordinal.{u_1}
hb : 1 < b
hx : x ≠ 0
hxb : x < b
hy : y < b ^ e
f c : Ordinal.{u_1}
hf : (f, c) ∈ CNF b y
he : e ≠ (f, c).1
⊢ ((f, c).1, c) ∈ (e, x) :: CNF b y

Tactic:
exact mem_cons_of_mem _ hf

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
⊢ 0 < b ^ e

Tactic:
exact opow_pos _ (hb 0)

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

Goal state before:
pp: o₁ e₁ : ONote
n₁ : ℕ+
a₁ : ONote
h✝¹ : o₁ = e₁.oadd n₁ a₁
o₂ e₂ : ONote
n₂ : ℕ+
a₂ : ONote
h✝ : o₂ = e₂.oadd n₂ a₂
h₁ : (namedPattern o₁ (e₁.oadd n₁ a₁) h✝¹).NF
h₂ : (namedPattern o₂ (e₂.oadd n₂ a₂) h✝).NF
IHe : e₁ = e₂
⊢ (Ordering.eq.then ((_root_.cmp ↑n₁ ↑n₂).then (a₁.cmp a₂))).Compares (namedPattern o₁ (e₁.oadd n₁ a₁) h✝¹)
    (namedPattern o₂ (e₂.oadd n₂ a₂) h✝)

Tactic:
subst IHe

Goal state after:
o₁ e₁ : ONote
n₁ : ℕ+
a₁ : ONote
h✝¹ : o₁ = e₁.oadd n₁ a₁
o₂ : ONote
n₂ : ℕ+
a₂ : ONote
h₁ : (namedPattern o₁ (e₁.oadd n₁ a₁) h✝¹).NF
h✝ : o₂ = e₁.oadd n₂ a₂
h₂ : (namedPattern o₂ (e₁.oadd n₂ a₂) h✝).NF
⊢ (Ordering.eq.then ((_root_.cmp ↑n₁ ↑n₂).then (a₁.cmp a₂))).Compares (namedPattern o₁ (e₁.oadd n₁ a₁) h✝¹)
    (namedPattern o₂ (e₁.oadd n₂ a₂) h✝)
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:
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.Ordinal.Veblen

Goal state before:
pp: case h
f : Ordinal.{u} → Ordinal.{u}
hf : IsNormal f
hp : 0 < f 0
o : Ordinal.{u}
ho : IsSuccLimit o
a : Ordinal.{u}
IH : ∀ b < o, veblenWith f b 0 ≤ a
⊢ 0 < o ∧ List.foldr (fun x ↦ veblenWith f ↑x) 0 [] ≤ veblenWith f 0 0

Tactic:
simpa using ho.bot_lt

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

Goal state before:
pp: x : ZFSet.{u}
h : x.Nonempty
⊢ ↑(⋂₀ x) = ⋂₀ (SetLike.coe '' ↑x)

Tactic:
by
  ext
  simp [mem_sInter h]

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

Goal state before:
pp: α : Type u_1
inst✝ : Small.{u, u_1} α
f : α → ZFSet.{u}
⊢ (range f).rank = ⨆ i, succ (f i).rank

Tactic:
by
  apply (Ordinal.iSup_le _).antisymm'
  · simpa [rank_le_iff, ← add_one_le_iff] using Ordinal.le_iSup _
  · simp [rank_lt_of_mem]

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

Goal state before:
pp: f : ZFSet.{u} → ZFSet.{u}
inst✝ : Definable₁ f
x y : ZFSet.{u}
h : y ∈ x
z : ZFSet.{u}
e : z = f y
⊢ ∃ z_1 ∈ x, z_1.pair (f z_1) = y.pair z

Tactic:
subst e
        exact ⟨_, h, rfl⟩

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

Goal state before:
pp: o : Ordinal.{u_1}
x : PSet.{u_1}
⊢ x ∈ o.toPSet ↔ ∃ a < o, x.Equiv a.toPSet

Tactic:
rw [toPSet, PSet.mem_def]
  simpa using ((@ToType.mk o).exists_congr_left (p := fun y ↦ x.Equiv y.1.toPSet)).symm

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

Goal state before:
pp: a : Ordinal.{u_1}
⊢ ∀ ⦃b : Ordinal.{u_1}⦄, a ≤ b → a.toZFSet ⊆ b.toZFSet

Tactic:
b

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

Goal state before:
pp: R : Type u_1
A : Type u_2
sR : CommSemiring R
sA : CommSemiring A
sAlg : Algebra R A
r s : R
h : r + s = 0
⊢ IsNat 0 0

Tactic:
exact ⟨by simp⟩

Goal state after:
Module: Mathlib.Tactic.Algebra.Lemmas

Goal state before:
pp: R : Type u_1
A : Type u_2
sR : CommSemiring R
sA : CommSemiring A
sAlg : Algebra R A
r : R
h : IsNat r 1
⊢ IsNat 1 1

Tactic:
exact ⟨by simp⟩

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

Goal state before:
pp: α : Type u_1
s t : Stream'.Seq α
h : s.head = t.head
⊢ dist s t = 2⁻¹ * dist s.tail t.tail

Tactic:
cases s <;> cases t

Goal state after:
case nil.nil
α : Type u_1
h : nil.head = nil.head
⊢ dist nil nil = 2⁻¹ * dist nil.tail nil.tail

case nil.cons
α : Type u_1
x✝ : α
s✝ : Stream'.Seq α
h : nil.head = (Seq.cons x✝ s✝).head
⊢ dist nil (Seq.cons x✝ s✝) = 2⁻¹ * dist nil.tail (Seq.cons x✝ s✝).tail

case cons.nil
α : Type u_1
x✝ : α
s✝ : Stream'.Seq α
h : (Seq.cons x✝ s✝).head = nil.head
⊢ dist (Seq.cons x✝ s✝) nil = 2⁻¹ * dist (Seq.cons x✝ s✝).tail nil.tail

case cons.cons
α : Type u_1
x✝¹ : α
s✝¹ : Stream'.Seq α
x✝ : α
s✝ : Stream'.Seq α
h : (Seq.cons x✝¹ s✝¹).head = (Seq.cons x✝ s✝).head
⊢ dist (Seq.cons x✝¹ s✝¹) (Seq.cons x✝ s✝) = 2⁻¹ * dist (Seq.cons x✝¹ s✝¹).tail (Seq.cons x✝ s✝).tail
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion

Goal state before:
pp: α : Type u_1
s t : Stream'.Seq α
h : dist s t ≤ 2⁻¹
⊢ s = nil ∧ t = nil ∨ ∃ hd s' t', s = Seq.cons hd s' ∧ t = Seq.cons hd t'

Tactic:
cases s <;> cases t

Goal state after:
case nil.nil
α : Type u_1
h : dist nil nil ≤ 2⁻¹
⊢ nil = nil ∧ nil = nil ∨ ∃ hd s' t', nil = Seq.cons hd s' ∧ nil = Seq.cons hd t'

case nil.cons
α : Type u_1
x✝ : α
s✝ : Stream'.Seq α
h : dist nil (Seq.cons x✝ s✝) ≤ 2⁻¹
⊢ nil = nil ∧ Seq.cons x✝ s✝ = nil ∨ ∃ hd s' t', nil = Seq.cons hd s' ∧ Seq.cons x✝ s✝ = Seq.cons hd t'

case cons.nil
α : Type u_1
x✝ : α
s✝ : Stream'.Seq α
h : dist (Seq.cons x✝ s✝) nil ≤ 2⁻¹
⊢ Seq.cons x✝ s✝ = nil ∧ nil = nil ∨ ∃ hd s' t', Seq.cons x✝ s✝ = Seq.cons hd s' ∧ nil = Seq.cons hd t'

case cons.cons
α : Type u_1
x✝¹ : α
s✝¹ : Stream'.Seq α
x✝ : α
s✝ : Stream'.Seq α
h : dist (Seq.cons x✝¹ s✝¹) (Seq.cons x✝ s✝) ≤ 2⁻¹
⊢ Seq.cons x✝¹ s✝¹ = nil ∧ Seq.cons x✝ s✝ = nil ∨
    ∃ hd s' t', Seq.cons x✝¹ s✝¹ = Seq.cons hd s' ∧ Seq.cons x✝ s✝ = Seq.cons hd t'
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basis

Goal state before:
pp: case hf
hd f : ℝ → ℝ
tl : Basis
h_basis : WellFormedBasis (hd :: tl)
hf : f ∈ tl
r exp : ℝ
h_exp : exp > 0
⊢ ∀ᶠ (x : ℝ) in atTop, 0 < f x

Tactic:
exact h_basis.tail.eventually_pos.mono fun _ h ↦ h _ hf

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

Goal state before:
pp: m : UnitMonomial
basis : Basis
h_basis : WellFormedBasis basis
⊢ m.inv.toFun basis =ᶠ[atTop] (m.toFun basis)⁻¹

Tactic:
eta_expand
  simp only [toFun, inv, Pi.inv_apply]
  induction m generalizing basis with
  | nil => simp
  | cons exp exps ih =>
    cases basis with
    | nil => simp
    | cons basis_hd basis_tl =>
      apply ((h_basis.head_eventually_pos).and (ih (h_basis.tail))).mono
      intro x ⟨h_pos, ih⟩
      simp only [List.map_cons, List.zipWith_cons_cons, List.prod_cons, mul_inv_rev]
      grind [Real.rpow_neg h_pos.le]

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

Goal state before:
pp: α : Type u_1
motive : (Stream'.Seq α → Stream'.Seq α) → Prop
op : Stream'.Seq α → Stream'.Seq α
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, op') => (hd, ↑op' s.tail))
              (T s.head)
⊢ FriendlyOperation op

Tactic:
by
  apply of_dist_le_pow
  intro s t n hn
  induction n generalizing op s t with
  | zero => simp
  | succ n ih =>
    obtain ⟨T, hT⟩ := h_step _ h_base
    have h_head : s.head = t.head := by
      replace hn : dist s t ≤ 2⁻¹ := by
        apply hn.trans
        simp only [pow_succ, inv_pos, Nat.ofNat_pos, mul_le_iff_le_one_left]
        apply pow_le_one₀ <;> norm_num
      rw [dist_le_half_iff] at hn
      obtain ⟨rfl, rfl⟩ | ⟨hd, s_tl, t_tl, rfl, rfl⟩ := hn <;> rfl
    have hs := hT s
    have ht := hT t
    cases hT_head : T s.head with
    | none =>
      simp only [hT_head, Option.map_none, ← h_head] at hs ht
      simp [hs, ht, destruct_eq_none]
    | some v =>
      obtain ⟨hd, op', h_next⟩ := v
      simp only [hT_head, Option.map_some, ← h_head] at hs ht
      simp only [destruct_eq_cons hs, destruct_eq_cons ht, dist_cons_cons, pow_succ', inv_pos,
        Nat.ofNat_pos, mul_le_mul_iff_right₀, ge_iff_le]
      apply ih h_next
      simpa [dist_eq_half_of_head h_head, pow_succ'] using hn

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

Goal state before:
pp: basis_hd : ℝ → ℝ
basis_tl : List (ℝ → ℝ)
motive : MultiseriesExpansion (basis_hd :: basis_tl) → Sort u_1
nil : (f : ℝ → ℝ) → motive (mk Multiseries.nil f)
cons :
  (exp : ℝ) →
    (coef : MultiseriesExpansion basis_tl) →
      (tl : Multiseries basis_hd basis_tl) → (f : ℝ → ℝ) → motive (mk (Multiseries.cons exp coef tl) f)
ms : MultiseriesExpansion (basis_hd :: basis_tl)
⊢ motive ms

Tactic:
let ⟨s, f⟩ := ms

Goal state after:
basis_hd : ℝ → ℝ
basis_tl : List (ℝ → ℝ)
motive : MultiseriesExpansion (basis_hd :: basis_tl) → Sort u_1
nil : (f : ℝ → ℝ) → motive (mk Multiseries.nil f)
cons :
  (exp : ℝ) →
    (coef : MultiseriesExpansion basis_tl) →
      (tl : Multiseries basis_hd basis_tl) → (f : ℝ → ℝ) → motive (mk (Multiseries.cons exp coef tl) f)
ms : MultiseriesExpansion (basis_hd :: basis_tl)
s : Stream'.Seq (ℝ × MultiseriesExpansion basis_tl)
f : ℝ → ℝ
⊢ motive (s, f)
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs

Goal state before:
pp: case seq.h_Pairwise
basis_hd : ℝ → ℝ
basis_tl : Basis
exp : ℝ
coef : MultiseriesExpansion basis_tl
tl : Multiseries basis_hd basis_tl
h_coef : coef.Sorted
h_comp : tl.leadingExp < ↑exp
h_tl_coef : ∀ x ∈ (mk tl 0).seq, x.2.Sorted
h_tl_tl : Seq.Pairwise (fun x1 x2 ↦ x1 > x2) (mk tl 0).seq
⊢ Seq.Pairwise (fun x1 x2 ↦ x1 > x2) (mk (Multiseries.cons exp coef tl) 0).seq

Tactic:
cases tl

Goal state after:
case seq.h_Pairwise.nil
basis_hd : ℝ → ℝ
basis_tl : Basis
exp : ℝ
coef : MultiseriesExpansion basis_tl
h_coef : coef.Sorted
h_comp : Multiseries.nil.leadingExp < ↑exp
h_tl_coef : ∀ x ∈ (mk Multiseries.nil 0).seq, x.2.Sorted
h_tl_tl : Seq.Pairwise (fun x1 x2 ↦ x1 > x2) (mk Multiseries.nil 0).seq
⊢ Seq.Pairwise (fun x1 x2 ↦ x1 > x2) (mk (Multiseries.cons exp coef Multiseries.nil) 0).seq

case seq.h_Pairwise.cons
basis_hd : ℝ → ℝ
basis_tl : Basis
exp : ℝ
coef : MultiseriesExpansion basis_tl
h_coef : coef.Sorted
exp✝ : ℝ
coef✝ : MultiseriesExpansion basis_tl
tl✝ : Multiseries basis_hd basis_tl
h_comp : (Multiseries.cons exp✝ coef✝ tl✝).leadingExp < ↑exp
h_tl_coef : ∀ x ∈ (mk (Multiseries.cons exp✝ coef✝ tl✝) 0).seq, x.2.Sorted
h_tl_tl : Seq.Pairwise (fun x1 x2 ↦ x1 > x2) (mk (Multiseries.cons exp✝ coef✝ tl✝) 0).seq
⊢ Seq.Pairwise (fun x1 x2 ↦ x1 > x2) (mk (Multiseries.cons exp coef (Multiseries.cons exp✝ coef✝ tl✝)) 0).seq
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion

Goal state before:
pp: case h.cons
α : 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 α
hF : some (s_hd, s_tl) = Option.map (fun x ↦ (x.1, ↑x.2 s.tail)) (h_opf.unfold s.head)
⊢ (op (Seq.cons s_hd s_tl)).destruct =
    Option.map (fun x ↦ (x.1, ↑x.2 s.tail))
      (match h_opf.unfold s.head 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:
generalize h_opf.unfold s.head = t? at *

Goal state after:
case h.cons
α : 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 α
t? : Option (α × Subtype FriendlyOperation)
hF : some (s_hd, s_tl) = Option.map (fun x ↦ (x.1, ↑x.2 s.tail)) t?
⊢ (op (Seq.cons s_hd s_tl)).destruct =
    Option.map (fun x ↦ (x.1, ↑x.2 s.tail))
      (match t? 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.SetTheory.Ordinal.Notation

Goal state before:
pp: a : ONote
m : ℕ+
b : ONote
iha : a = 0
ihb : b = 0
e✝ : b.fundamentalSequence = Sum.inl none
e : a.fundamentalSequence = Sum.inl none
m' : ℕ
e' : m.natPred = m' + 1
⊢ m = m.natPred.succPNat

Tactic:
← PNat.coe_inj,

Goal state after:
a : ONote
m : ℕ+
b : ONote
iha : a = 0
ihb : b = 0
e✝ : b.fundamentalSequence = Sum.inl none
e : a.fundamentalSequence = Sum.inl none
m' : ℕ
e' : m.natPred = m' + 1
⊢ ↑m = ↑m.natPred.succPNat
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
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
h_step : leadingExp tl < ↑exp
⊢ tl_exp < exp

Tactic:
cases tl

Goal state after:
case step.left.nil
basis_hd : ℝ → ℝ
basis_tl : Basis
s : Multiseries basis_hd basis_tl
motive : Multiseries basis_hd basis_tl → Prop
h_base : motive s
exp : ℝ
coef : MultiseriesExpansion basis_tl
tl_exp : ℝ
tl_coef : MultiseriesExpansion basis_tl
h : motive (Seq.cons (exp, coef) Seq.nil)
h_tl : (tl_exp, tl_coef) ∈ Seq.nil.head
h_step : leadingExp Seq.nil < ↑exp
⊢ tl_exp < exp

case step.left.cons
basis_hd : ℝ → ℝ
basis_tl : Basis
s : Multiseries basis_hd basis_tl
motive : Multiseries basis_hd basis_tl → Prop
h_base : motive s
exp : ℝ
coef : MultiseriesExpansion basis_tl
tl_exp : ℝ
tl_coef : MultiseriesExpansion basis_tl
x✝ : ℝ × MultiseriesExpansion basis_tl
s✝ : Stream'.Seq (ℝ × MultiseriesExpansion basis_tl)
h : motive (Seq.cons (exp, coef) (Seq.cons x✝ s✝))
h_tl : (tl_exp, tl_coef) ∈ (Seq.cons x✝ s✝).head
h_step : leadingExp (Seq.cons x✝ s✝) < ↑exp
⊢ tl_exp < exp
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: a : ONote
m : ℕ+
b : ONote
ihb : b = 0
e✝ : b.fundamentalSequence = Sum.inl none
a' : ONote
iha : a.repr = succ a'.repr ∧ (a.NF → a'.NF)
e : a.fundamentalSequence = Sum.inl (some a')
m' : ℕ
e' : m.natPred = m' + 1
⊢ m = m.natPred.succPNat

Tactic:
← PNat.coe_inj,

Goal state after:
a : ONote
m : ℕ+
b : ONote
ihb : b = 0
e✝ : b.fundamentalSequence = Sum.inl none
a' : ONote
iha : a.repr = succ a'.repr ∧ (a.NF → a'.NF)
e : a.fundamentalSequence = Sum.inl (some a')
m' : ℕ
e' : m.natPred = m' + 1
⊢ ↑m = ↑m.natPred.succPNat
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: a : ONote
m : ℕ+
b : ONote
ihb : b = 0
e✝ : b.fundamentalSequence = Sum.inl none
f : ℕ → ONote
iha :
  IsSuccLimit a.repr ∧
    (∀ (i : ℕ), f i < f (i + 1) ∧ f i < a ∧ (a.NF → (f i).NF)) ∧ ∀ a_1 < a.repr, ∃ i, a_1 < (f i).repr
e : a.fundamentalSequence = Sum.inr f
m' : ℕ
e' : m.natPred = m' + 1
⊢ m = m.natPred.succPNat

Tactic:
← PNat.coe_inj,

Goal state after:
a : ONote
m : ℕ+
b : ONote
ihb : b = 0
e✝ : b.fundamentalSequence = Sum.inl none
f : ℕ → ONote
iha :
  IsSuccLimit a.repr ∧
    (∀ (i : ℕ), f i < f (i + 1) ∧ f i < a ∧ (a.NF → (f i).NF)) ∧ ∀ a_1 < a.repr, ∃ i, a_1 < (f i).repr
e : a.fundamentalSequence = Sum.inr f
m' : ℕ
e' : m.natPred = m' + 1
⊢ ↑m = ↑m.natPred.succPNat
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs

Goal state before:
pp: f basis_hd : ℝ → ℝ
basis_tl : Basis
exp : ℝ
coef : MultiseriesExpansion basis_tl
tl : Multiseries basis_hd basis_tl
h : (mk (Multiseries.cons exp coef tl) f).Approximates
⊢ coef.Approximates ∧ Majorized f basis_hd exp ∧ (mk tl (f - basis_hd ^ exp * coef.toFun)).Approximates

Tactic:
by
  generalize h_ms : (mk (.cons exp coef tl) f) = ms at h
  cases h <;> simp at h_ms; grind

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

Goal state before:
pp: case refine_1
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)
h2 : ↑x_num * ⅟↑x_den = ↑(↑x_num / ↑x_den)
⊢ ∀ (p : ℚ), (↑x_num / ↑x_den) ^ y_num ≠ p ^ y_den

Tactic:
simp only [div_pow, ← Nat.cast_pow]

Goal state after:
case refine_1
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)
h2 : ↑x_num * ⅟↑x_den = ↑(↑x_num / ↑x_den)
⊢ ∀ (p : ℚ), ↑(x_num ^ y_num) / ↑(x_den ^ y_num) ≠ p ^ y_den
Module: Mathlib.Testing.Plausible.Functions

Goal state before:
pp: case cons.succ.cons.cons
α : Type u
inst✝ : DecidableEq α
x y x' : α
xs : List α
xs_ih :
  ∀ {ys : List α},
    xs.Nodup → xs.length = ys.length → ∀ (i : ℕ), xs[i]? = some x → (applyId (xs.zip ys) x = y ↔ ys[i]? = some y)
n✝ : ℕ
h₂ : xs[n✝]? = some x
head✝ : α
tail✝ : List α
h₁✝ : (x' :: xs).length = (head✝ :: tail✝).length
h₁ : List.Pairwise (fun x1 x2 ↦ x1 ≠ x2) xs
h₀ : ∀ a' ∈ xs, x' ≠ a'
⊢ (if x' = x then head✝ else applyId (xs.zip tail✝) x) = y ↔ tail✝[n✝]? = some y

Tactic:
if_neg

Goal state after:
case cons.succ.cons.cons
α : Type u
inst✝ : DecidableEq α
x y x' : α
xs : List α
xs_ih :
  ∀ {ys : List α},
    xs.Nodup → xs.length = ys.length → ∀ (i : ℕ), xs[i]? = some x → (applyId (xs.zip ys) x = y ↔ ys[i]? = some y)
n✝ : ℕ
h₂ : xs[n✝]? = some x
head✝ : α
tail✝ : List α
h₁✝ : (x' :: xs).length = (head✝ :: tail✝).length
h₁ : List.Pairwise (fun x1 x2 ↦ x1 ≠ x2) xs
h₀ : ∀ a' ∈ xs, x' ≠ a'
⊢ applyId (xs.zip tail✝) x = y ↔ tail✝[n✝]? = some y

case cons.succ.cons.cons.hnc
α : Type u
inst✝ : DecidableEq α
x y x' : α
xs : List α
xs_ih :
  ∀ {ys : List α},
    xs.Nodup → xs.length = ys.length → ∀ (i : ℕ), xs[i]? = some x → (applyId (xs.zip ys) x = y ↔ ys[i]? = some y)
n✝ : ℕ
h₂ : xs[n✝]? = some x
head✝ : α
tail✝ : List α
h₁✝ : (x' :: xs).length = (head✝ :: tail✝).length
h₁ : List.Pairwise (fun x1 x2 ↦ x1 ≠ x2) xs
h₀ : ∀ a' ∈ xs, x' ≠ a'
⊢ ¬x' = x
Module: Mathlib.Topology.UniformSpace.Ascoli

Goal state before:
pp: case inr.mpr
ι : 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 ℱ
H' : Tendsto id 𝒢 (𝓝 ⟨f, f_mem⟩)
⊢ Tendsto (⇑UniformFun.ofFun ∘ F) ℱ (𝓝 (UniformFun.ofFun f))

Tactic:
ind.tendsto_nhds_iff,

Goal state after:
case inr.mpr
ι : 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 ℱ
H' : Tendsto ((⇑UniformFun.ofFun ∘ Subtype.val) ∘ id) 𝒢 (𝓝 ((⇑UniformFun.ofFun ∘ Subtype.val) ⟨f, f_mem⟩))
⊢ Tendsto (⇑UniformFun.ofFun ∘ F) ℱ (𝓝 (UniformFun.ofFun f))
Module: Mathlib.Topology.Algebra.Category.ProfiniteGrp.Completion

Goal state before:
pp: G : GrpCat
⊢ Mono (eta G) ↔ Group.ResiduallyFinite ↑G

Tactic:
by
  rw [GrpCat.mono_iff_injective, injective_iff_map_eq_one,
    Group.residuallyFinite_iff_forall_finiteIndexNormalSubgroup]
  refine forall_congr' fun g ↦ imp_congr_left ?_
  rw [Subtype.ext_iff, funext_iff]
  exact forall_congr' fun H ↦ QuotientGroup.eq_one_iff g

Goal state after:
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 y : G
tfae_2_iff_1 : (MapClusterPt x atTop fun x ↦ y ^ x) ↔ MapClusterPt x atTop fun x ↦ y ^ x
tfae_3_to_4 : x ∈ closure[inst✝²] (range fun x ↦ y ^ x) → x ∈ closure[inst✝²] (range fun x ↦ y ^ x)
⊢ x ∈ closure[inst✝²] (range fun x ↦ y ^ x) → MapClusterPt x atTop fun x ↦ y ^ x

Tactic:
refine fun h ↦ closure_minimal ?_ isClosed_setOfPred_clusterPt h

Goal state after:
G : Type u_1
inst✝³ : Group G
inst✝² : TopologicalSpace G
inst✝¹ : CompactSpace G
inst✝ : IsTopologicalGroup G
x y : G
tfae_2_iff_1 : (MapClusterPt x atTop fun x ↦ y ^ x) ↔ MapClusterPt x atTop fun x ↦ y ^ x
tfae_3_to_4 : x ∈ closure[inst✝²] (range fun x ↦ y ^ x) → x ∈ closure[inst✝²] (range fun x ↦ y ^ x)
h : x ∈ closure[inst✝²] (range fun x ↦ y ^ x)
⊢ (range fun x ↦ y ^ x) ⊆ {x | ClusterPt x (map (fun x ↦ y ^ x) atTop)}
Module: Mathlib.Topology.Algebra.Category.ProfiniteGrp.Completion

Goal state before:
pp: G : GrpCat
P : ProfiniteGrp.{u}
f : G ⟶ GrpCat.of ↑P.toProfinite.toTop
⊢ eta G ≫ (forget₂ ProfiniteGrp.{u} GrpCat).map (lift f) = f

Tactic:
by
  let e := isoLimittoFiniteQuotientFunctor P
  rw [← (forget₂ ProfiniteGrp GrpCat).mapIso e |>.cancel_iso_hom_right]
  dsimp
  rw [Category.assoc, ← (forget₂ ProfiniteGrp GrpCat).map_comp (lift f) e.hom]
  change eta G ≫ ((forget₂ _ _).map ((_ ≫ e.inv) ≫ e.hom)) = _
  simp only [Category.assoc, Iso.inv_hom_id]
  rfl

Goal state after: