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

Goal state before:
pp: case nil
α : Type u_1
l : Lists' α true
h : ofList [] ⊆ nil
⊢ ofList [] = nil

pp: case cons
α : Type u_1
l : Lists' α true
head✝ : Lists α
tail✝ : List (Lists α)
tail_ih✝ : ofList tail✝ ⊆ nil → ofList tail✝ = nil
h : ofList (head✝ :: tail✝) ⊆ nil
⊢ ofList (head✝ :: tail✝) = nil

Tactic:
· rfl

Goal state after:
case cons
α : Type u_1
l : Lists' α true
head✝ : Lists α
tail✝ : List (Lists α)
tail_ih✝ : ofList tail✝ ⊆ nil → ofList tail✝ = nil
h : ofList (head✝ :: tail✝) ⊆ nil
⊢ ofList (head✝ :: tail✝) = nil
Module: Mathlib.Topology.Order.IsNormal

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁷ : LinearOrder α
inst✝⁶ : WellFoundedLT α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : LinearOrder β
inst✝² : WellFoundedLT β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
hs : StrictMono f
hc : Continuous f
⊢ IsNormal f

Tactic:
refine ⟨hs, fun {a} ha ↦ (isLUB_of_mem_closure ?_ ?_).2⟩

Goal state after:
case refine_1
α : Type u_1
β : Type u_2
inst✝⁷ : LinearOrder α
inst✝⁶ : WellFoundedLT α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : LinearOrder β
inst✝² : WellFoundedLT β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
hs : StrictMono f
hc : Continuous f
a : α
ha : IsSuccLimit a
⊢ f a ∈ upperBounds (f '' Iio a)

case refine_2
α : Type u_1
β : Type u_2
inst✝⁷ : LinearOrder α
inst✝⁶ : WellFoundedLT α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : LinearOrder β
inst✝² : WellFoundedLT β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
hs : StrictMono f
hc : Continuous f
a : α
ha : IsSuccLimit a
⊢ f a ∈ closure (f '' Iio a)
Module: Mathlib.SetTheory.Ordinal.CantorNormalForm

Goal state before:
pp: case inr
b e x : Ordinal.{u_1}
f : Ordinal.{u_1} →₀ Ordinal.{u_1}
h : ∀ e' ∈ f.support, e' < e
hx : x ≠ 0
hf : f e = 0
⊢ eval b (single e x + f) = b ^ e * x + eval b f

Tactic:
eval,

Goal state after:
case inr
b e x : Ordinal.{u_1}
f : Ordinal.{u_1} →₀ Ordinal.{u_1}
h : ∀ e' ∈ f.support, e' < e
hx : x ≠ 0
hf : f e = 0
⊢ foldr (fun p r ↦ b ^ p * (single e x + f) p + r) 0 ((single e x + f).support.sort fun x1 x2 ↦ x1 ≥ x2) =
    b ^ e * x + eval b f
Module: Mathlib.Topology.Order.SuccPred

Goal state before:
pp: case refine_2.inl
α : Type u_1
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
a : α
inst✝¹ : SuccOrder α
inst✝ : NoMaxOrder α
a✝ : Nontrivial α
ha✝ : ¬IsSuccLimit a
ha : IsMin a
⊢ IsOpen[inst✝³] {a}

pp: case refine_2.inr
α : Type u_1
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
a : α
inst✝¹ : SuccOrder α
inst✝ : NoMaxOrder α
a✝ : Nontrivial α
ha✝ : ¬IsSuccLimit a
ha : ¬IsSuccPrelimit a
⊢ IsOpen[inst✝³] {a}

Tactic:
· convert! isOpen_Iio (a := Order.succ a) using 1
      simp [ha.Iic_eq]

Goal state after:
case refine_2.inr
α : Type u_1
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
a : α
inst✝¹ : SuccOrder α
inst✝ : NoMaxOrder α
a✝ : Nontrivial α
ha✝ : ¬IsSuccLimit a
ha : ¬IsSuccPrelimit a
⊢ IsOpen[inst✝³] {a}
Module: Mathlib.SetTheory.Ordinal.CantorNormalForm

Goal state before:
pp: b e x : Ordinal.{u_1}
f : Ordinal.{u_1} →₀ Ordinal.{u_1}
h : ∀ e' ∈ f.support, e' < e
⊢ eval b (single e x + f) = b ^ e * x + eval b f

Tactic:
obtain rfl | hx := eq_or_ne x 0; · simp
  have hf : f e = 0 := by
    rw [← notMem_support_iff]
    exact fun he ↦ (h e he).false
  rw [eval, support_single_add (by simpa) hx, Finset.sort_cons]
  · simp only [add_apply, foldr_cons, single_eq_same, hf, add_zero, add_right_inj]
    apply foldr_ext
    intro e' he' _
    congr
    rw [single_eq_of_ne, zero_add]
    aesop
  · exact fun e' he' ↦ (h e' he').le

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

Goal state before:
pp: case eq
e₁ : ONote
n₁ : ℕ+
a₁ : ONote
n₂ : ℕ+
a₂ : ONote
h₁ : e₁.cmp e₁ = Ordering.eq
⊢ Ordering.eq.then ((_root_.cmp ↑n₁ ↑n₂).then (a₁.cmp a₂)) = Ordering.eq → e₁.oadd n₁ a₁ = e₁.oadd n₂ a₂

Tactic:
cases h₂ : _root_.cmp (n₁ : ℕ) n₂

Goal state after:
case eq.lt
e₁ : ONote
n₁ : ℕ+
a₁ : ONote
n₂ : ℕ+
a₂ : ONote
h₁ : e₁.cmp e₁ = Ordering.eq
h₂ : _root_.cmp ↑n₁ ↑n₂ = Ordering.lt
⊢ Ordering.eq.then (Ordering.lt.then (a₁.cmp a₂)) = Ordering.eq → e₁.oadd n₁ a₁ = e₁.oadd n₂ a₂

case eq.eq
e₁ : ONote
n₁ : ℕ+
a₁ : ONote
n₂ : ℕ+
a₂ : ONote
h₁ : e₁.cmp e₁ = Ordering.eq
h₂ : _root_.cmp ↑n₁ ↑n₂ = Ordering.eq
⊢ Ordering.eq.then (Ordering.eq.then (a₁.cmp a₂)) = Ordering.eq → e₁.oadd n₁ a₁ = e₁.oadd n₂ a₂

case eq.gt
e₁ : ONote
n₁ : ℕ+
a₁ : ONote
n₂ : ℕ+
a₂ : ONote
h₁ : e₁.cmp e₁ = Ordering.eq
h₂ : _root_.cmp ↑n₁ ↑n₂ = Ordering.gt
⊢ Ordering.eq.then (Ordering.gt.then (a₁.cmp a₂)) = Ordering.eq → e₁.oadd n₁ a₁ = e₁.oadd n₂ a₂
Module: Mathlib.SetTheory.Ordinal.CantorNormalForm

Goal state before:
pp: b o : Ordinal.{u_1}
⊢ eval b (coeff b o) = foldr (fun p r ↦ b ^ p.1 * p.2 + r) 0 (CNF b o)

Tactic:
eval,

Goal state after:
b o : Ordinal.{u_1}
⊢ foldr (fun p r ↦ b ^ p * (coeff b o) p + r) 0 ((coeff b o).support.sort fun x1 x2 ↦ x1 ≥ x2) =
    foldr (fun p r ↦ b ^ p.1 * p.2 + r) 0 (CNF b o)
Module: Mathlib.SetTheory.Ordinal.Topology

Goal state before:
pp: s : Set Ordinal.{u}
hs : ¬BddAbove s
Hs : StrictMono (enumOrd s)
h : IsNormal (enumOrd s)
ι : Type u
hι : Nonempty ι
f : ι → Ordinal.{u}
hf : ∀ (i : ι), f i ∈ s
g : ι → Ordinal.{u} := fun i ↦ (enumOrdOrderIso s hs).symm ⟨f i, ⋯⟩
this : enumOrd s (⨆ i, g i) = ⨆ i, f i
⊢ enumOrd s (⨆ i, g i) ∈ s

Tactic:
exact enumOrd_mem hs _

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

Goal state before:
pp: case lt
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
nh : ↑n₁ < ↑n₂ ∧ Ordering.lt = Ordering.lt ∨ ↑n₂ ≤ ↑n₁ ∧ (if ↑n₂ < ↑n₁ then Ordering.gt else Ordering.eq) = Ordering.lt
⊢ (Ordering.eq.then (Ordering.lt.then (a₁.cmp a₂))).Compares (namedPattern o₁ (e₁.oadd n₁ a₁) h✝¹)
    (namedPattern o₂ (e₁.oadd n₂ a₂) h✝)

pp: case eq
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
nh : ↑n₁ < ↑n₂ ∧ Ordering.lt = Ordering.eq ∨ ↑n₂ ≤ ↑n₁ ∧ (if ↑n₂ < ↑n₁ then Ordering.gt else Ordering.eq) = Ordering.eq
⊢ (Ordering.eq.then (Ordering.eq.then (a₁.cmp a₂))).Compares (namedPattern o₁ (e₁.oadd n₁ a₁) h✝¹)
    (namedPattern o₂ (e₁.oadd n₂ a₂) h✝)

pp: case gt
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
nh : ↑n₁ < ↑n₂ ∧ Ordering.lt = Ordering.gt ∨ ↑n₂ ≤ ↑n₁ ∧ (if ↑n₂ < ↑n₁ then Ordering.gt else Ordering.eq) = Ordering.gt
⊢ (Ordering.eq.then (Ordering.gt.then (a₁.cmp a₂))).Compares (namedPattern o₁ (e₁.oadd n₁ a₁) h✝¹)
    (namedPattern o₂ (e₁.oadd n₂ a₂) h✝)

Tactic:
case lt =>
        rcases nh with nh | nh
        · exact oadd_lt_oadd_2 h₁ nh.left
        · rw [ite_eq_iff] at nh; rcases nh.right with nh | nh <;> cases nh <;> contradiction

Goal state after:
case eq
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
nh : ↑n₁ < ↑n₂ ∧ Ordering.lt = Ordering.eq ∨ ↑n₂ ≤ ↑n₁ ∧ (if ↑n₂ < ↑n₁ then Ordering.gt else Ordering.eq) = Ordering.eq
⊢ (Ordering.eq.then (Ordering.eq.then (a₁.cmp a₂))).Compares (namedPattern o₁ (e₁.oadd n₁ a₁) h✝¹)
    (namedPattern o₂ (e₁.oadd n₂ a₂) h✝)

case gt
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
nh : ↑n₁ < ↑n₂ ∧ Ordering.lt = Ordering.gt ∨ ↑n₂ ≤ ↑n₁ ∧ (if ↑n₂ < ↑n₁ then Ordering.gt else Ordering.eq) = Ordering.gt
⊢ (Ordering.eq.then (Ordering.gt.then (a₁.cmp a₂))).Compares (namedPattern o₁ (e₁.oadd n₁ a₁) h✝¹)
    (namedPattern o₂ (e₁.oadd n₂ a₂) h✝)
Module: Mathlib.SetTheory.Ordinal.Veblen

Goal state before:
pp: f : Ordinal.{u} → Ordinal.{u}
o a : Ordinal.{u}
hf : IsNormal f
h : o ≠ 0
⊢ a ∈ range (derivFamily fun x ↦ veblenWith f ↑x) ↔ ∀ b < o, veblenWith f b a = a

Tactic:
mem_range_derivFamily (fun _ ↦ isNormal_veblenWith hf _)

Goal state after:
f : Ordinal.{u} → Ordinal.{u}
o a : Ordinal.{u}
hf : IsNormal f
h : o ≠ 0
⊢ (∀ (i : ↑(Iio o)), veblenWith f (↑i) a = a) ↔ ∀ b < o, veblenWith f b a = a
Module: Mathlib.SetTheory.ZFC.Class

Goal state before:
pp: x : ZFSet.{u}
h : ∅ ∉ x
y : ZFSet.{u}
yx : y ∈ x
⊢ ↑(map (fun y ↦ Classical.epsilon fun z ↦ z ∈ y) x) ′ ↑y ∈ ↑y

Tactic:
rw [@map_fval _ (Classical.allZFSetDefinable _) x y yx, Class.coe_mem, Class.coe_apply]

Goal state after:
x : ZFSet.{u}
h : ∅ ∉ x
y : ZFSet.{u}
yx : y ∈ x
⊢ (Classical.epsilon fun z ↦ z ∈ y) ∈ y
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: case lt
e₁ : ONote
n₁ : ℕ+
a₁ e₂ : ONote
n₂ : ℕ+
a₂ : ONote
h₁ : (e₁.oadd n₁ a₁).NF
h₂ : (e₂.oadd n₂ a₂).NF
this✝ : a₁.NF
this : a₂.NF
h' : (a₁.sub a₂).repr = a₁.repr - a₂.repr
h : e₁.cmp e₂ = Ordering.lt
ee : Ordering.lt.Compares e₁ e₂
⊢ (match Ordering.lt with
      | Ordering.lt => 0
      | Ordering.gt => e₁.oadd n₁ a₁
      | Ordering.eq =>
        match ↑n₁ - ↑n₂ with
        | 0 => if n₁ = n₂ then a₁.sub a₂ else 0
        | k.succ => e₁.oadd k.succPNat a₁).repr =
    0

pp: case lt
e₁ : ONote
n₁ : ℕ+
a₁ e₂ : ONote
n₂ : ℕ+
a₂ : ONote
h₁ : (e₁.oadd n₁ a₁).NF
h₂ : (e₂.oadd n₂ a₂).NF
this✝ : a₁.NF
this : a₂.NF
h' : (a₁.sub a₂).repr = a₁.repr - a₂.repr
h : e₁.cmp e₂ = Ordering.lt
ee : Ordering.lt.Compares e₁ e₂
⊢ (e₁.oadd n₁ a₁).repr ≤ (e₂.oadd n₂ a₂).repr

Tactic:
· rfl

Goal state after:
case lt
e₁ : ONote
n₁ : ℕ+
a₁ e₂ : ONote
n₂ : ℕ+
a₂ : ONote
h₁ : (e₁.oadd n₁ a₁).NF
h₂ : (e₂.oadd n₂ a₂).NF
this✝ : a₁.NF
this : a₂.NF
h' : (a₁.sub a₂).repr = a₁.repr - a₂.repr
h : e₁.cmp e₂ = Ordering.lt
ee : Ordering.lt.Compares e₁ e₂
⊢ (e₁.oadd n₁ a₁).repr ≤ (e₂.oadd n₂ a₂).repr
Module: Mathlib.SetTheory.ZFC.Ordinal

Goal state before:
pp: case mpr.inl
x : ZFSet.{u}
hx hy : x.IsOrdinal
⊢ x ⊆ x

pp: case mpr.inr
x y : ZFSet.{u}
hx : x.IsOrdinal
hy : y.IsOrdinal
h : x ∈ y
⊢ x ⊆ y

Tactic:
· rfl

Goal state after:
case mpr.inr
x y : ZFSet.{u}
hx : x.IsOrdinal
hy : y.IsOrdinal
h : x ∈ y
⊢ x ⊆ y
Module: Mathlib.SetTheory.ZFC.Ordinal

Goal state before:
pp: x y : ZFSet.{u}
hx : x.IsOrdinal
hy : y.IsOrdinal
⊢ x ∈ y ∨ x = y ∨ y ∈ x

Tactic:
by
  rw [eq_comm, ← subset_iff_eq_or_mem hy hx]
  exact mem_or_subset hx hy

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

Goal state before:
pp: x : ZFSet.{u}
⊢ x.IsTransitive ∧ Std.Trichotomous (Subrel (fun x1 x2 ↦ x1 ∈ x2) fun x_1 ↦ x_1 ∈ x) → x.IsOrdinal

Tactic:
by
    rintro ⟨h₁, h₂⟩
    rw [isOrdinal_iff_isTrans]
    refine ⟨h₁, ⟨@fun y z w hyz hzw ↦ ?_⟩⟩
    obtain hyw | rfl | hwy := trichotomous_of (Subrel (· ∈ ·) (· ∈ x)) y w
    · exact hyw
    · cases asymm hyz hzw
    · cases mem_wf.asymmetric₃ _ _ _ hyz hzw hwy

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

Goal state before:
pp: case pos
o₁ o₂ : ONote
inst✝¹ : o₁.NF
inst✝ : o₂.NF
b' : ONote
k : ℕ
e₂ : o₂.split' = (b', k)
this : b'.NF
na : zero.NF
e₁ : o₁.split = (zero, 0)
h : o₂ = 0
⊢ (o₁ ^ o₂).NF

Tactic:
subst h

Goal state after:
case pos
o₁ : ONote
inst✝¹ : o₁.NF
b' : ONote
k : ℕ
this : b'.NF
na : zero.NF
e₁ : o₁.split = (zero, 0)
inst✝ : NF 0
e₂ : split' 0 = (b', k)
⊢ (o₁ ^ 0).NF
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion

Goal state before:
pp: α : Type u_1
s t : Stream'.Seq α
h : s.head ≠ t.head
⊢ ↑s ≠ ↑t

Tactic:
Subtype.coe_ne_coe

Goal state after:
α : Type u_1
s t : Stream'.Seq α
h : s.head ≠ t.head
⊢ s ≠ t
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 g : β →ᵤ Stream'.Seq α
b : β
⊢ dist
      (match F b with
      | none => nil
      | some (a, c, b') => Seq.cons a (op c (f b')))
      (match F b with
      | none => nil
      | some (a, c, b') => Seq.cons a (op c (g b'))) ≤
    2⁻¹ * dist f g

Tactic:
cases F b with
    | none => simp
    | some v =>
      obtain ⟨a, c, b'⟩ := v
      simp
      calc
        _ ≤ dist (f b') (g b') := by
          have := h.friend c
          rw [FriendlyOperation, lipschitzWith_iff_dist_le_mul] at this
          specialize this (f b') (g b')
          simpa using this
        _ ≤ _ := by
          simp only [UniformFun.dist_def]
          apply le_ciSup (f := fun b ↦ dist (f b) (g b))
          have : ∃ C, ∀ (a b : Seq α), dist a b ≤ C := by
            rw [← Metric.boundedSpace_iff]
            infer_instance
          obtain ⟨C, hC⟩ := this
          use C
          simp [upperBounds]
          grind

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

Goal state before:
pp: case pos
o₁ o₂ : ONote
inst✝¹ : o₁.NF
inst✝ : o₂.NF
N₁ : zero.NF
e₁ : o₁.split = (zero, 0)
r₁ : o₁.repr = zero.repr + ↑0
hzero : 0 = zero
h : o₂ = 0
⊢ (o₁ ^ o₂).repr = o₁.repr ^ o₂.repr

Tactic:
subst h

Goal state after:
case pos
o₁ : ONote
inst✝¹ : o₁.NF
N₁ : zero.NF
e₁ : o₁.split = (zero, 0)
r₁ : o₁.repr = zero.repr + ↑0
hzero : 0 = zero
inst✝ : NF 0
⊢ (o₁ ^ 0).repr = o₁.repr ^ repr 0
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic

Goal state before:
pp: case cons
x exp1 : ℝ
exps1 : List ℝ
ih :
  ∀ {m2 : UnitMonomial} {basis : Basis},
    WellFormedBasis basis →
      exps1.length = List.length m2 →
        (∀ f ∈ basis, 0 < f x) →
          (List.zipWith (fun exp b ↦ b x ^ exp) (List.zipWith (fun x1 x2 ↦ x1 + x2) exps1 m2) basis).prod =
            (List.zipWith (fun exp b ↦ b x ^ exp) exps1 basis).prod *
              (List.zipWith (fun exp b ↦ b x ^ exp) m2 basis).prod
m2 : UnitMonomial
basis : Basis
h_basis : WellFormedBasis basis
h_length : (exp1 :: exps1).length = List.length m2
h_pos : ∀ f ∈ basis, 0 < f x
⊢ (List.zipWith (fun exp b ↦ b x ^ exp) (List.zipWith (fun x1 x2 ↦ x1 + x2) (exp1 :: exps1) m2) basis).prod =
    (List.zipWith (fun exp b ↦ b x ^ exp) (exp1 :: exps1) basis).prod *
      (List.zipWith (fun exp b ↦ b x ^ exp) m2 basis).prod

Tactic:
cases m2 with
    | nil => simp at h_length
    | cons exp2 exps2 =>
    cases basis with
    | nil => simp
    | cons basis_hd basis_tl =>
      simp only [List.zipWith_cons_cons, List.prod_cons] at ih ⊢
      have h1 : exps1.length = exps2.length := by grind
      have h2 : ∀ f ∈ basis_tl, 0 < f x := by grind
      have h3 : 0 < basis_hd x := h_pos _ (by simp)
      rw [ih h_basis.tail h1 h2, Real.rpow_add h3]
      grind

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

Goal state before:
pp: α : 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)
⊢ FriendlyOperation op

Tactic:
by
  let motive' (op : Seq α → Seq α) : Prop :=
    ∃ opf op', op = opf ∘ op' ∧ FriendlyOperation opf ∧ motive op'
  apply FriendlyOperation.coind motive'
  · exact ⟨_root_.id, op, rfl, FriendlyOperation.id, h_base⟩
  rintro _ ⟨opf, op, rfl, h_opf, h_op⟩
  obtain ⟨T, hT⟩ := h_step _ h_op
  use fun hd? ↦
    match (T hd?) with
    | none => (h_opf.unfold none).map fun (hd, opf') =>
      (hd, ⟨_, fun _ ↦ opf'.val nil, op, rfl, FriendlyOperation.const, h_op⟩)
    | some (hd, opf', op') => (h_opf.unfold (some hd)).map fun (hd', opf'') =>
      (hd', ⟨_, opf''.val ∘ opf'.val, op'.val, rfl,
        FriendlyOperation.comp opf''.prop opf'.prop, op'.prop⟩)
  intro s
  specialize hT s
  simp only [Function.comp_apply]
  generalize op s = s' at *
  cases s' with
  | nil =>
    symm at hT
    simp at hT
    simp [hT, destruct_apply_eq_unfold h_opf]
    rfl
  | cons s_hd s_tl =>
    simp only [destruct_cons] at hT
    simp only [destruct_apply_eq_unfold h_opf, Seq.tail_cons, Seq.head_cons]
    generalize T s.head = t? at *
    cases t? with
    | none => simp at hT
    | some v =>
      obtain ⟨hd, opf', op'⟩ := v
      simp at hT
      simp [hT]
      rfl

Goal state after:
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.coef * t2.coef) • (t1.unit.mul t2.unit).toFun basis =ᶠ[atTop]
    t2.coef • t1.coef • (t1.unit.toFun basis * t2.unit.toFun basis)

Tactic:
UnitMonomial.mul_toFun h_basis h_length

Goal state after:
t1 t2 : Monomial
basis : Basis
h_basis : WellFormedBasis basis
h_length : List.length t1.unit = List.length t2.unit
⊢ (t1.coef * t2.coef) • (t1.unit.toFun basis * t2.unit.toFun basis) =ᶠ[atTop]
    t2.coef • t1.coef • (t1.unit.toFun basis * t2.unit.toFun basis)
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Trimming

Goal state before:
pp: basis : Basis
ms : MultiseriesExpansion basis
h_zero : ms.IsZero
h_approx : ms.Approximates
⊢ ms.toFun =ᶠ[atTop] 0

Tactic:
cases h_zero with
  | const hc => simp [hc, Pi.zero_def]
  | nil => simpa using h_approx

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

Goal state before:
pp: a b d : ℕ
h_coprime : a.Coprime b
ha : ∀ (x : ℕ), a ≠ x ^ d
q : ℚ
hq : 0 ≤ q
hb_zero : ¬b = 0
x' : ℤ := q.num
y : ℕ := q.den
h : ↑a / ↑b = (↑x' / ↑y) ^ d
⊢ 0 ≤ x'

Tactic:
Rat.num_nonneg

Goal state after:
a b d : ℕ
h_coprime : a.Coprime b
ha : ∀ (x : ℕ), a ≠ x ^ d
q : ℚ
hq : 0 ≤ q
hb_zero : ¬b = 0
x' : ℤ := q.num
y : ℕ := q.den
h : ↑a / ↑b = (↑x' / ↑y) ^ d
⊢ 0 ≤ q
Module: Mathlib.Testing.Plausible.Functions

Goal state before:
pp: case neg
α : 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₃ : dlookup x (map Prod.toSigma (xs.zip ys)) = some val
⊢ val ∈ y :: ys ↔ x ∈ x' :: xs

Tactic:
obtain - | ⟨h₀, h₅⟩ := h₀
        obtain - | ⟨h₂, h₄⟩ := h₂
        have h₆ := Nat.succ.inj h₁
        specialize xs_ih h₅ h₃ h₄ h₆
        simp only [Ne.symm h, xs_ih, List.mem_cons]
        suffices val ∈ ys by tauto
        rw [← Option.mem_def, List.mem_dlookup_iff] at h₃
        · simp only [Prod.toSigma, List.mem_map, Prod.exists] at h₃
          rcases h₃ with ⟨a, b, h₃, h₄, h₅⟩
          apply (List.of_mem_zip h₃).2
        simp only [List.NodupKeys, List.keys, comp_def, Prod.fst_toSigma, List.map_map]
        rwa [List.map_fst_zip (le_of_eq h₆)]

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

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

pp: α : Type u
inst✝ : DecidableEq α
xs ys : List α
x : α
h : x ∉ xs
⊢ x ∉ (map Prod.toSigma (xs.zip ys)).keys

Tactic:
· rfl

Goal state after:
α : Type u
inst✝ : DecidableEq α
xs ys : List α
x : α
h : x ∉ xs
⊢ x ∉ (map Prod.toSigma (xs.zip ys)).keys
Module: Mathlib.Topology.UniformSpace.Ascoli

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

Tactic:
simp_rw [UniformOnFun.uniformSpace, UniformSpace.comap_iInf, ← UniformSpace.comap_comap,
      UniformFun.ofFun, Equiv.coe_fn_mk, UniformOnFun.toFun, UniformOnFun.ofFun, Function.comp_def,
      UniformFun, Equiv.coe_fn_symm_mk]

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

Goal state before:
pp: G : GrpCat
P : ProfiniteGrp.{u}
f : G ⟶ GrpCat.of ↑P.toProfinite.toTop
X : OpenNormalSubgroup ↑P.toProfinite.toTop
⊢ ∀ ⦃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:
Y

Goal state after:
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
Module: Mathlib.Topology.Algebra.Category.ProfiniteGrp.Completion

Goal state before:
pp: X'✝ X✝ : GrpCat
Y✝ : ProfiniteGrp.{?u.22}
f : X'✝ ⟶ X✝
g : X✝ ⟶ (forget₂ ProfiniteGrp.{?u.22} GrpCat).obj Y✝
⊢ eta X'✝ ≫ (forget₂ ProfiniteGrp.{?u.22} GrpCat).map ((homEquiv X'✝ Y✝).symm (f ≫ g)) =
    eta X'✝ ≫ (forget₂ ProfiniteGrp.{?u.22} GrpCat).map (profiniteCompletion.map f ≫ (homEquiv X✝ Y✝).symm g)

Tactic:
simp [homEquiv]

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✝ : LocallyCompactSpace H
Vn : ℕ → Set Circle := fun n ↦ Circle.centeredArc (π / 2 ^ (n + 1))
hVn : ∀ (n : ℕ) (x : Circle), x ∈ Vn n ↔ |(↑x).arg| < π / 2 ^ (n + 1)
n : ℕ
x : Circle
h1 : x ∈ Vn n
h2 : x * x ∈ Vn n
⊢ x ∈ Vn (n + 1)

Tactic:
rw [hVn] at h1 h2 ⊢

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✝ : LocallyCompactSpace H
Vn : ℕ → Set Circle := fun n ↦ Circle.centeredArc (π / 2 ^ (n + 1))
hVn : ∀ (n : ℕ) (x : Circle), x ∈ Vn n ↔ |(↑x).arg| < π / 2 ^ (n + 1)
n : ℕ
x : Circle
h1 : |(↑x).arg| < π / 2 ^ (n + 1)
h2 : |(↑(x * x)).arg| < π / 2 ^ (n + 1)
⊢ |(↑x).arg| < π / 2 ^ (n + 1 + 1)
Module: Mathlib.Topology.Algebra.Ring.Compact

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : TopologicalSpace R
inst✝³ : IsTopologicalRing R
inst✝² : CompactSpace R
inst✝¹ : T2Space R
inst✝ : IsArtinianRing R
n : ℕ
hn : ⊥.jacobson ^ n = 0
H : (∏ p, p.asIdeal) ^ n = ⊥
this✝ : Finite (R ⧸ ∏ i, i.asIdeal)
this : Finite (R ⧸ (∏ p, p.asIdeal) ^ n)
⊢ Finite R

Tactic:
rw [H] at this

Goal state after:
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : TopologicalSpace R
inst✝³ : IsTopologicalRing R
inst✝² : CompactSpace R
inst✝¹ : T2Space R
inst✝ : IsArtinianRing R
n : ℕ
hn : ⊥.jacobson ^ n = 0
H : (∏ p, p.asIdeal) ^ n = ⊥
this✝ : Finite (R ⧸ ∏ i, i.asIdeal)
this : Finite (R ⧸ ⊥)
⊢ Finite R
Module: Mathlib.Topology.Baire.BaireMeasurable

Goal state before:
pp: case compl
α : Type u_1
inst✝² : TopologicalSpace α
s✝ : Set α
inst✝¹ : MeasurableSpace α
inst✝ : BorelSpace α
s : Set α
ht✝ : MeasurableSet s
ihs : ∃ u, IsOpen[inst✝²] u ∧ s =ᶠ[residual α] u
⊢ ∃ u, IsOpen[inst✝²] u ∧ sᶜ =ᶠ[residual α] u

Tactic:
obtain ⟨U, Uo, hsU⟩ := ihs

Goal state after:
case compl
α : Type u_1
inst✝² : TopologicalSpace α
s✝ : Set α
inst✝¹ : MeasurableSpace α
inst✝ : BorelSpace α
s : Set α
ht✝ : MeasurableSet s
U : Set α
Uo : IsOpen[inst✝²] U
hsU : s =ᶠ[residual α] U
⊢ ∃ u, IsOpen[inst✝²] u ∧ sᶜ =ᶠ[residual α] u