mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.RegularLocalRing.Polynomial

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsRegularRing R
p : Ideal R[X]
hp : p.IsPrime
q : Ideal R := comap C p
S : Type u_1 := (Localization.AtPrime q)[X]
pc : Submonoid R[X] := Submonoid.map (↑C) q.primeCompl
this✝¹ : Algebra R[X] S := algebra R (Localization.AtPrime q)
this✝ : IsLocalization pc S
pS : Ideal S := Ideal.map (algebraMap R[X] S) p
disj : Disjoint ↑pc ↑p
this : pS.IsPrime
⊢ IsRegularLocalRing (Localization.AtPrime p)

Tactic:
have : IsLocalization.AtPrime (Localization.AtPrime pS) p := by
    convert IsLocalization.isLocalization_isLocalization_atPrime_isLocalization pc
      (Localization.AtPrime pS) pS
    exact (IsLocalization.under_map_of_isPrime_disjoint pc _ ‹_› disj).symm

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsRegularRing R
p : Ideal R[X]
hp : p.IsPrime
q : Ideal R := comap C p
S : Type u_1 := (Localization.AtPrime q)[X]
pc : Submonoid R[X] := Submonoid.map (↑C) q.primeCompl
this✝² : Algebra R[X] S := algebra R (Localization.AtPrime q)
this✝¹ : IsLocalization pc S
pS : Ideal S := Ideal.map (algebraMap R[X] S) p
disj : Disjoint ↑pc ↑p
this✝ : pS.IsPrime
this : IsLocalization.AtPrime (Localization.AtPrime pS) p
⊢ IsRegularLocalRing (Localization.AtPrime p)
Module: Mathlib.RingTheory.WittVector.FrobeniusFractionField

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : Field k
inst✝¹ : CharP k p
inst✝ : IsAlgClosed k
m n : ℕ
r' q' : 𝕎 k
hr' : r'.coeff 0 ≠ 0
hq' : q'.coeff 0 ≠ 0
hq : ↑p ^ n * q' ∈ nonZeroDivisors (𝕎 k)
⊢ let b := frobeniusRotation p hr' hq';
  φ ((algebraMap (𝕎 k) (FractionRing (𝕎 k))) b) * Localization.mk (↑p ^ m * r') ⟨↑p ^ n * q', hq⟩ =
    ↑p ^ (↑m - ↑n) * (algebraMap (𝕎 k) (FractionRing (𝕎 k))) b

Tactic:
intro b

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : Field k
inst✝¹ : CharP k p
inst✝ : IsAlgClosed k
m n : ℕ
r' q' : 𝕎 k
hr' : r'.coeff 0 ≠ 0
hq' : q'.coeff 0 ≠ 0
hq : ↑p ^ n * q' ∈ nonZeroDivisors (𝕎 k)
b : 𝕎 k := frobeniusRotation p hr' hq'
⊢ φ ((algebraMap (𝕎 k) (FractionRing (𝕎 k))) b) * Localization.mk (↑p ^ m * r') ⟨↑p ^ n * q', hq⟩ =
    ↑p ^ (↑m - ↑n) * (algebraMap (𝕎 k) (FractionRing (𝕎 k))) b
Module: Mathlib.SetTheory.Descriptive.Tree

Goal state before:
pp: A : Type u_1
T : ↥(tree A)
m n : ℕ
x : ↥T
⊢ take m (take n x) = take (min m n) x

Tactic:
by
  simp [Subtype.ext_iff, List.take_take]

Goal state after:
Module: Mathlib.SetTheory.Lists

Goal state before:
pp: α : Type u_1
C : Lists α → Sort u_2
D : Lists' α true → Sort u_3
C0 : (a : α) → C (atom a)
C1 : (l : Lists' α true) → D l → C (of' l)
D0 : D Lists'.nil
D1 : (a : Lists α) → (l : Lists' α true) → C a → D l → D (Lists'.cons a l)
⊢ {b : Bool} →
    (l : Lists' α b) →
      C ⟨b, l⟩ ×'
        match b, l with
        | true, l => D l
        | false, x => PUnit

Tactic:
intro b

Goal state after:
α : Type u_1
C : Lists α → Sort u_2
D : Lists' α true → Sort u_3
C0 : (a : α) → C (atom a)
C1 : (l : Lists' α true) → D l → C (of' l)
D0 : D Lists'.nil
D1 : (a : Lists α) → (l : Lists' α true) → C a → D l → D (Lists'.cons a l)
b : Bool
⊢ (l : Lists' α b) →
    C ⟨b, l⟩ ×'
      match b, l with
      | true, l => D l
      | false, x => PUnit
Module: Mathlib.SetTheory.Ordinal.FixedPointApproximants

Goal state before:
pp: case pos
α : Type u
inst✝ : CompleteLattice α
f : α →o α
x : α
a b✝ : Ordinal.{u}
hf : f (lfpApprox f x a) = lfpApprox f x a
b : Ordinal.{u}
IH : ∀ y < b, a ≤ y → lfpApprox f x y = lfpApprox f x a
hab : a ≤ b
i : Ordinal.{u}
hi : i < b
hi' : i < a
⊢ f (lfpApprox f x i) ≤ lfpApprox f x a

pp: case neg
α : Type u
inst✝ : CompleteLattice α
f : α →o α
x : α
a b✝ : Ordinal.{u}
hf : f (lfpApprox f x a) = lfpApprox f x a
b : Ordinal.{u}
IH : ∀ y < b, a ≤ y → lfpApprox f x y = lfpApprox f x a
hab : a ≤ b
i : Ordinal.{u}
hi : i < b
hi' : a ≤ i
⊢ f (lfpApprox f x i) ≤ lfpApprox f x a

Tactic:
· exact apply_lfpApprox_le_lfpApprox_of_lt f hi'

Goal state after:
case neg
α : Type u
inst✝ : CompleteLattice α
f : α →o α
x : α
a b✝ : Ordinal.{u}
hf : f (lfpApprox f x a) = lfpApprox f x a
b : Ordinal.{u}
IH : ∀ y < b, a ≤ y → lfpApprox f x y = lfpApprox f x a
hab : a ≤ b
i : Ordinal.{u}
hi : i < b
hi' : a ≤ i
⊢ f (lfpApprox f x i) ≤ lfpApprox f x a
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: e : ONote
n : ℕ+
a : ONote
h : (e.oadd n a).NF
e0 : e = 0
⊢ a = 0

Tactic:
by
  simpa [e0, NFBelow_zero] using h.snd'

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

Goal state before:
pp: ⊢ DecidableRel TopBelow

Tactic:
intro b

Goal state after:
b : ONote
⊢ (b_1 : ONote) → Decidable (b.TopBelow b_1)
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: b o : ONote
⊢ Decidable (b.TopBelow o)

Tactic:
cases o <;> delta TopBelow

Goal state after:
case zero
b : ONote
⊢ Decidable
    (match zero with
    | zero => True
    | e.oadd a a_1 => e.cmp b = Ordering.lt)

case oadd
b a✝² : ONote
a✝¹ : ℕ+
a✝ : ONote
⊢ Decidable
    (match a✝².oadd a✝¹ a✝ with
    | zero => True
    | e.oadd a a_1 => e.cmp b = Ordering.lt)
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: b : Ordinal.{0}
e : ONote
n : ℕ+
a o : ONote
h₁ : (e.oadd n a).NFBelow b
h₂ : o.NFBelow b
⊢ (e.oadd n a + o).NFBelow b

Tactic:
by
    have h' := add_nfBelow (h₁.snd.mono <| le_of_lt h₁.lt) h₂
    simp only [oadd_add]; revert h'; obtain - | ⟨e', n', a'⟩ := a + o <;> intro h'
    · exact NFBelow.oadd h₁.fst NFBelow.zero h₁.lt
    have : ((e.cmp e').Compares e e') := @cmp_compares _ _ h₁.fst h'.fst
    cases h : cmp e e' <;> dsimp [addAux] <;> simp only [h]
    · exact h'
    · simp only [h] at this
      subst e'
      exact NFBelow.oadd h'.fst h'.snd h'.lt
    · simp only [h] at this
      exact NFBelow.oadd h₁.fst (NF.below_of_lt this ⟨⟨_, h'⟩⟩) h₁.lt

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

Goal state before:
pp: o : Ordinal.{u}
x : ZFSet.{u}
⊢ x ∈ V_ o ↔ x.rank < o

Tactic:
simp_rw [mem_vonNeumann', subset_vonNeumann]
  exact ⟨fun ⟨a, h₁, h₂⟩ ↦ h₂.trans_lt h₁, by aesop⟩

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

Goal state before:
pp: case pos
e₁ : ONote
n₁ : ℕ+
a₁ : ONote
b₁ : Ordinal.{0}
h₁ : (e₁.oadd n₁ a₁).NFBelow b₁
e₂ : ONote
n₂ : ℕ+
a₂ : ONote
b₂ : Ordinal.{0}
h₂ : (e₂.oadd n₂ a₂).NFBelow b₂
IH : (e₁.oadd n₁ a₁ * a₂).NFBelow (e₁.repr + e₂.repr)
e0 : e₂ = 0
⊢ e₁.repr < e₁.repr + b₂

Tactic:
← h₂.lt.pos,

Goal state after:
case pos
e₁ : ONote
n₁ : ℕ+
a₁ : ONote
b₁ : Ordinal.{0}
h₁ : (e₁.oadd n₁ a₁).NFBelow b₁
e₂ : ONote
n₂ : ℕ+
a₂ : ONote
b₂ : Ordinal.{0}
h₂ : (e₂.oadd n₂ a₂).NFBelow b₂
IH : (e₁.oadd n₁ a₁ * a₂).NFBelow (e₁.repr + e₂.repr)
e0 : e₂ = 0
⊢ e₁.repr ≤ e₁.repr + 0
Module: Mathlib.SetTheory.ZFC.Ordinal

Goal state before:
pp: case refine_2
x : ZFSet.{u_1}
h : x.IsOrdinal
y z w : ZFSet.{u_1}
hyz : y ∈ z
hzw : z ∈ w
hw : w ∈ insert x x
⊢ y ∈ w

Tactic:
obtain rfl | hw := mem_insert_iff.1 hw
    exacts [h.mem_trans hyz hzw, h.mem_trans' hyz hzw hw]

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

Goal state before:
pp: e a : ONote
Ne : e.NF
Na : a.NF
e0 : e.repr ≠ 0
n : ℕ+
h : a.repr < ω ^ e.repr
No : (e.oadd n a).NF
this : ω ^ e.repr ≤ ω ^ e.repr * ↑↑n + a.repr
⊢ ∀ b' < ω, (ω ^ e.repr * ↑↑n + a.repr) ^ b' ≤ (ω ^ e.repr) ^ ω

Tactic:
intro b

Goal state after:
e a : ONote
Ne : e.NF
Na : a.NF
e0 : e.repr ≠ 0
n : ℕ+
h : a.repr < ω ^ e.repr
No : (e.oadd n a).NF
this : ω ^ e.repr ≤ ω ^ e.repr * ↑↑n + a.repr
b : Ordinal.{0}
⊢ b < ω → (ω ^ e.repr * ↑↑n + a.repr) ^ b ≤ (ω ^ e.repr) ^ ω
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 α
⊢ ∀ (x : β), dist (UniformFun.toFun (T f) x) (UniformFun.toFun (T g) x) ≤ ↑2⁻¹ * dist f g

Tactic:
intro b

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 α
b : β
⊢ dist (UniformFun.toFun (T f) b) (UniformFun.toFun (T g) b) ≤ ↑2⁻¹ * dist f g
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion

Goal state before:
pp: case some
α : 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 : β
v : α × γ × β
⊢ dist
      (match some v with
      | none => nil
      | some (a, c, b') => Seq.cons a (op c (f b')))
      (match some v with
      | none => nil
      | some (a, c, b') => Seq.cons a (op c (g b'))) ≤
    2⁻¹ * dist f g

Tactic:
| some v =>

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

Goal state before:
pp: case h
α : Type u_1
β : Type u_2
γ : Type u_3
F : β → Option (α × γ × β)
op : γ → Stream'.Seq α → Stream'.Seq α
h : FriendlyOperationClass op
T : (β →ᵤ Stream'.Seq α) → β →ᵤ Stream'.Seq α := ⋯
hT : LipschitzWith 2⁻¹ T
f : β → Stream'.Seq α
hf : Function.IsFixedPt T f
⊢ ∀ (b : β),
    match F b with
    | none => f b = nil
    | some (a, c, b') => f b = Seq.cons a (op c (f b'))

Tactic:
intro b

Goal state after:
case h
α : 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'))
hT : LipschitzWith 2⁻¹ T
f : β → Stream'.Seq α
hf : Function.IsFixedPt T f
b : β
⊢ match F b with
  | none => f b = nil
  | some (a, c, b') => f b = Seq.cons a (op c (f b'))
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion

Goal state before:
pp: case h.some
α : 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'))
hT : LipschitzWith 2⁻¹ T
f : β → Stream'.Seq α
hf : Function.IsFixedPt T f
b : β
v : α × γ × β
hb : F b = some v
⊢ match some v with
  | none =>
    (match some v with
      | none => nil
      | some (a, c, b') => Seq.cons a (op c (f b'))) =
      nil
  | some (a, c, b') =>
    (match some v with
      | none => nil
      | some (a, c, b') => Seq.cons a (op c (f b'))) =
      Seq.cons a
        (op c
          (match F b' with
          | none => nil
          | some (a, c, b') => Seq.cons a (op c (f b'))))

Tactic:
| some v =>

Goal state after:
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

pp: case hg
hd f : ℝ → ℝ
tl : Basis
h_basis : WellFormedBasis (hd :: tl)
hf : f ∈ tl
r exp : ℝ
h_exp : exp > 0
⊢ Tendsto hd atTop atTop

pp: case h
hd f : ℝ → ℝ
tl : Basis
h_basis : WellFormedBasis (hd :: tl)
hf : f ∈ tl
r exp : ℝ
h_exp : exp > 0
⊢ (Real.log ∘ f) =o[atTop] (Real.log ∘ hd)

pp: case hb
hd f : ℝ → ℝ
tl : Basis
h_basis : WellFormedBasis (hd :: tl)
hf : f ∈ tl
r exp : ℝ
h_exp : exp > 0
⊢ 0 < exp

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

Goal state after:
case hg
hd f : ℝ → ℝ
tl : Basis
h_basis : WellFormedBasis (hd :: tl)
hf : f ∈ tl
r exp : ℝ
h_exp : exp > 0
⊢ Tendsto hd atTop atTop

case h
hd f : ℝ → ℝ
tl : Basis
h_basis : WellFormedBasis (hd :: tl)
hf : f ∈ tl
r exp : ℝ
h_exp : exp > 0
⊢ (Real.log ∘ f) =o[atTop] (Real.log ∘ hd)

case hb
hd f : ℝ → ℝ
tl : Basis
h_basis : WellFormedBasis (hd :: tl)
hf : f ∈ tl
r exp : ℝ
h_exp : exp > 0
⊢ 0 < exp
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion

Goal state before:
pp: case succ.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, op') => (hd, ↑op' s.tail))
              (T s.head)
n : ℕ
ih :
  ∀ {op : Stream'.Seq α → Stream'.Seq α},
    motive op → ∀ (s t : Stream'.Seq α), dist s t ≤ 2⁻¹ ^ n → dist (op s) (op t) ≤ 2⁻¹ ^ n
op : Stream'.Seq α → Stream'.Seq α
h_base : motive op
s t : Stream'.Seq α
hn : dist s t ≤ 2⁻¹ ^ (n + 1)
T : Option α → Option (α × Subtype motive)
hT :
  ∀ (s : Stream'.Seq α),
    (op s).destruct =
      Option.map
        (fun x ↦
          match x with
          | (hd, op') => (hd, ↑op' s.tail))
        (T s.head)
h_head : s.head = t.head
hs :
  (op s).destruct =
    Option.map
      (fun x ↦
        match x with
        | (hd, op') => (hd, ↑op' s.tail))
      (T s.head)
ht :
  (op t).destruct =
    Option.map
      (fun x ↦
        match x with
        | (hd, op') => (hd, ↑op' t.tail))
      (T t.head)
v : α × Subtype motive
hT_head : T s.head = some v
⊢ dist (op s) (op t) ≤ 2⁻¹ ^ (n + 1)

Tactic:
| some v =>

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

Goal state before:
pp: case seq.h_coef
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
⊢ ∀ x ∈ (mk (Multiseries.cons exp coef tl) 0).seq, x.2.Sorted

Tactic:
simp at h_tl_coef ⊢
    grind

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:
| some v =>

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:
| some v =>

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

Goal state before:
pp: case nil
basis_hd : ℝ → ℝ
basis_tl : Basis
ms : MultiseriesExpansion (basis_hd :: basis_tl)
f✝ : ℝ → ℝ
h_equiv : ms.toFun =ᶠ[atTop] f✝
h_approx✝ : ms.Approximates
motive : MultiseriesExpansion (basis_hd :: basis_tl) → Prop :=
  fun ms ↦ ∃ ms' f', ms = ms'.replaceFun f' ∧ ms'.Approximates ∧ ms'.toFun =ᶠ[atTop] f'
f g : ℝ → ℝ
h_approx : (mk Multiseries.nil g).Approximates
h_eq : (mk Multiseries.nil g).toFun =ᶠ[atTop] f
⊢ ((mk Multiseries.nil g).replaceFun f).seq = Multiseries.nil ∧
      ((mk Multiseries.nil g).replaceFun f).toFun =ᶠ[atTop] 0 ∨
    ∃ exp coef tl,
      ((mk Multiseries.nil g).replaceFun f).seq = Multiseries.cons exp coef tl ∧
        coef.Approximates ∧
          Majorized ((mk Multiseries.nil g).replaceFun f).toFun basis_hd exp ∧
            motive (mk tl (((mk Multiseries.nil g).replaceFun f).toFun - basis_hd ^ exp * coef.toFun))

Tactic:
| nil g =>

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

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

Tactic:
simp [Nat.mod, Nat.modCore_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 → α
𝔖 : Set (Set X)
𝔖_compact : ∀ K ∈ 𝔖, IsCompact K
F_eqcont : ∀ K ∈ 𝔖, EquicontinuousOn F K
H1 :
  UniformSpace.comap F (UniformOnFun.uniformSpace X α 𝔖) =
    ⨅ K ∈ 𝔖, UniformSpace.comap (K.domRestrict ∘ F) (UniformFun.uniformSpace (↑K) α)
⊢ UniformSpace.comap F (⨅ S ∈ 𝔖, UniformSpace.comap S.domRestrict (Pi.uniformSpace fun i ↦ α)) =
    ⨅ K ∈ 𝔖, UniformSpace.comap F (UniformSpace.comap K.domRestrict (Pi.uniformSpace fun i ↦ α))

Tactic:
UniformSpace.comap_iInf

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

Goal state before:
pp: α : Type u
inst✝ : DecidableEq α
xs : List ((_ : α) × α)
hperm : map Sigma.fst xs ~ map Sigma.snd xs
hnodup : (map Sigma.snd xs).Nodup
xs₀ : List α
h₀ : map Sigma.fst xs = xs₀
xs₁ : List α
h₁ : map Sigma.snd xs = xs₁
hxs : xs = List.toFinmap' (xs₀.zip xs₁)
⊢ Injective (mapToSelf xs hperm hnodup).apply

Tactic:
revert hperm hnodup

Goal state after:
α : Type u
inst✝ : DecidableEq α
xs : List ((_ : α) × α)
xs₀ : List α
h₀ : map Sigma.fst xs = xs₀
xs₁ : List α
h₁ : map Sigma.snd xs = xs₁
hxs : xs = List.toFinmap' (xs₀.zip xs₁)
⊢ ∀ (hperm : map Sigma.fst xs ~ map Sigma.snd xs) (hnodup : (map Sigma.snd xs).Nodup),
    Injective (mapToSelf xs hperm hnodup).apply
Module: Mathlib.Topology.Algebra.Group.OpenMapping

Goal state before:
pp: case hU
G : Type u_1
X : Type u_2
inst✝⁹ : TopologicalSpace G
inst✝⁸ : TopologicalSpace X
inst✝⁷ : Group G
inst✝⁶ : IsTopologicalGroup G
inst✝⁵ : MulAction G X
inst✝⁴ : SigmaCompactSpace G
inst✝³ : BaireSpace X
inst✝² : T2Space X
inst✝¹ : ContinuousSMul G X
inst✝ : IsPretransitive G X
U : Set G
hU : U ∈ 𝓝 1
x : X
V : Set G
V_mem : V ∈ 𝓝 1
V_closed : IsClosed[inst✝⁹] V
V_symm : V⁻¹ = V
VU : V * V ⊆ U
s : Set G
s_count : s.Countable
hs : ⋃ g ∈ s, g • V = univ
K : ℕ → Set G := ⋯
F : ℕ × ↑s → Set X := ⋯
this✝ : Nonempty X
this : Encodable ↑s
⊢ ⋃ i, F i = univ

Tactic:
apply eq_univ_iff_forall.2 (fun y ↦ ?_)

Goal state after:
G : Type u_1
X : Type u_2
inst✝⁹ : TopologicalSpace G
inst✝⁸ : TopologicalSpace X
inst✝⁷ : Group G
inst✝⁶ : IsTopologicalGroup G
inst✝⁵ : MulAction G X
inst✝⁴ : SigmaCompactSpace G
inst✝³ : BaireSpace X
inst✝² : T2Space X
inst✝¹ : ContinuousSMul G X
inst✝ : IsPretransitive G X
U : Set G
hU : U ∈ 𝓝 1
x : X
V : Set G
V_mem : V ∈ 𝓝 1
V_closed : IsClosed[inst✝⁹] V
V_symm : V⁻¹ = V
VU : V * V ⊆ U
s : Set G
s_count : s.Countable
hs : ⋃ g ∈ s, g • V = univ
K : ℕ → Set G := compactCovering G
F : ℕ × ↑s → Set X := fun p ↦ (K p.1 ∩ ↑p.2 • V) • {x}
this✝ : Nonempty X
this : Encodable ↑s
y : X
⊢ y ∈ ⋃ i, F i
Module: Mathlib.Topology.Category.Compactum

Goal state before:
pp: X : Compactum
uux : Ultrafilter (Ultrafilter X.A)
⊢ X.str (X.join uux) = X.str (Ultrafilter.map X.str uux)

Tactic:
change ((β).μ.app _ ≫ X.a) _ = _
  rw [Monad.Algebra.assoc]
  rfl

Goal state after:
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
⊢ generatedBy X = coinduced (fun x ↦ x.fst.snd x.snd) inferInstance

Tactic:
rw [generatedBy, instTopologicalSpaceSigma, coinduced_iSup, iSup_sigma]

Goal state after:
ι : Type t
X : ι → Type u
inst✝ : (i : ι) → TopologicalSpace (X i)
Y : Type v
tY : TopologicalSpace Y
⊢ ⨆ i, ⨆ f, coinduced (⇑f) inferInstance =
    ⨆ i, ⨆ j, coinduced (fun x ↦ x.fst.snd x.snd) (coinduced (Sigma.mk ⟨i, j⟩) (inst✝ ⟨i, j⟩.fst))
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✝ : IsGeneratedBy X Y
f : Y → Z
x✝ : TopologicalSpace Z := TopologicalSpace.coinduced f tY
⊢ TopologicalSpace.coinduced f tY ≤ TopologicalSpace.generatedBy X

Tactic:
exact ((equiv_symm_comp_continuous_iff (X := X) f).2 continuous_coinduced_rng).coinduced_le

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

Goal state before:
pp: I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
s : Finset I
a : I
as : List I
ha : List.IsChain (fun x1 x2 ↦ x1 > x2) (a :: as)
c : Products I →₀ ℤ
hc : ↑c.support ⊆ {m | ↑m ≤ as}
m : Products I
⊢ c m ≠ 0 →
    e (π C fun x ↦ x ∈ s) a * c m • Products.eval (π C fun x ↦ x ∈ s) m ∈
      Submodule.span ℤ (Products.eval (π C fun x ↦ x ∈ s) '' {m | ↑m ≤ a :: as})

Tactic:
hm

Goal state after:
I : Type u
C : Set (I → Bool)
inst✝ : LinearOrder I
s : Finset I
a : I
as : List I
ha : List.IsChain (fun x1 x2 ↦ x1 > x2) (a :: as)
c : Products I →₀ ℤ
hc : ↑c.support ⊆ {m | ↑m ≤ as}
m : Products I
hm : c m ≠ 0
⊢ e (π C fun x ↦ x ∈ s) a * c m • Products.eval (π C fun x ↦ x ∈ s) m ∈
    Submodule.span ℤ (Products.eval (π C fun x ↦ x ∈ s) '' {m | ↑m ≤ a :: as})
Module: Mathlib.Topology.CWComplex.Classical.Basic

Goal state before:
pp: case a
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝ : RelCWComplex C D
n : ℕ∞
⊢ D ∪ ⋃ m, ⋃ (_ : ↑m < n), ⋃ j, openCell m j ⊆ D ∪ ⋃ m, ⋃ (_ : ↑m < n), ⋃ j, closedCell m j

pp: case a
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝ : RelCWComplex C D
n : ℕ∞
⊢ D ∪ ⋃ m, ⋃ (_ : ↑m < n), ⋃ j, closedCell m j ⊆ D ∪ ⋃ m, ⋃ (_ : ↑m < n), ⋃ j, openCell m j

Tactic:
· apply union_subset
    · exact subset_union_left
    · apply iUnion₂_subset fun m hm ↦ iUnion_subset fun j ↦ ?_
      apply subset_union_of_subset_right
      apply subset_iUnion₂_of_subset m hm
      apply subset_iUnion_of_subset j
      exact openCell_subset_closedCell m j

Goal state after:
case a
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝ : RelCWComplex C D
n : ℕ∞
⊢ D ∪ ⋃ m, ⋃ (_ : ↑m < n), ⋃ j, closedCell m j ⊆ D ∪ ⋃ m, ⋃ (_ : ↑m < n), ⋃ j, openCell m j
Module: Mathlib.Topology.Category.Profinite.Nobeling.Basic

Goal state before:
pp: case refine_1
I : Type u
C : Set (I → Bool)
J K : I → Prop
inst✝¹ : (i : I) → Decidable (J i)
inst✝ : (i : I) → Decidable (K i)
h✝ : ∀ (i : I), J i → K i
x : I → Bool
h : x ∈ π (π C K) J
⊢ x ∈ π C J

Tactic:
obtain ⟨y, ⟨z, hz, rfl⟩, rfl⟩ := h
    refine ⟨z, hz, (?_ : _ = (Proj J ∘ Proj K) z)⟩
    rw [proj_comp_of_subset J K h]

Goal state after: