mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Valuation.Quotient

Goal state before:
pp: R : Type u_1
Γ₀ : Type u_2
inst✝¹ : CommRing R
inst✝ : LinearOrderedCommMonoidWithZero Γ₀
J : Ideal R
v : Valuation (R ⧸ J) Γ₀
⊢ J ≤ (comap (Ideal.Quotient.mk J) v).supp

Tactic:
rw [comap_supp, ← Ideal.map_le_iff_le_comap]

Goal state after:
R : Type u_1
Γ₀ : Type u_2
inst✝¹ : CommRing R
inst✝ : LinearOrderedCommMonoidWithZero Γ₀
J : Ideal R
v : Valuation (R ⧸ J) Γ₀
⊢ Ideal.map (Ideal.Quotient.mk J) J ≤ v.supp
Module: Mathlib.RingTheory.Valuation.Quotient

Goal state before:
pp: case a
R : Type u_1
Γ₀ : Type u_2
inst✝¹ : CommRing R
inst✝ : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
J : Ideal R
hJ : J ≤ v.supp
⊢ (v.onQuot hJ).supp ≤ Ideal.map (Ideal.Quotient.mk J) v.supp

Tactic:
rintro ⟨x⟩ hx
    apply Ideal.subset_span
    exact ⟨x, hx, rfl⟩

Goal state after:
Module: Mathlib.RingTheory.Smooth.Quotient

Goal state before:
pp: R : Type u_1
inst✝¹⁰ : CommRing R
S : Type u_2
inst✝⁹ : CommRing S
R' : Type u_3
S' : Type u_4
inst✝⁸ : CommRing R'
inst✝⁷ : CommRing S'
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra R R'
inst✝⁴ : Algebra R' S'
inst✝³ : Algebra S S'
inst✝² : Algebra R S'
inst✝¹ : IsScalarTower R S S'
inst✝ : IsScalarTower R R' S'
surjRS : Function.Surjective ⇑(algebraMap R S)
eqmap : RingHom.ker (algebraMap S S') = Ideal.map (algebraMap R S) (RingHom.ker (algebraMap R R'))
⊢ Ideal.comap (algebraMap R R') (RingHom.ker (algebraMap R' S')) =
    RingHom.ker (algebraMap R R') ⊔ RingHom.ker (algebraMap R S)

Tactic:
rw [RingHom.comap_ker, ← IsScalarTower.algebraMap_eq, IsScalarTower.algebraMap_eq _ S,
      ← RingHom.comap_ker]
  simp [eqmap, Ideal.comap_map_of_surjective' _ surjRS]

Goal state after:
Module: Mathlib.RingTheory.WittVector.Compare

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ ((PadicInt.toZModPow n).comp (PadicInt.lift ⋯)).comp (fromPadicInt p) = (PadicInt.toZModPow n).comp (RingHom.id ℤ_[p])

Tactic:
PadicInt.lift_spec

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ (toZModPow p n).comp (fromPadicInt p) = (PadicInt.toZModPow n).comp (RingHom.id ℤ_[p])
Module: Mathlib.RingTheory.WittVector.FrobeniusFractionField

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : Field k
inst✝ : IsAlgClosed k
a₁ : 𝕎 k
ha₁ : a₁.coeff 0 ≠ 0
a₂ : 𝕎 k
this : solution p a₁ a₂ ^ (p - 1) = a₂.coeff 0 / a₁.coeff 0
⊢ solution p a₁ a₂ ^ p * a₁.coeff 0 = solution p a₁ a₂ * a₂.coeff 0

Tactic:
have := Nat.exists_eq_succ_of_ne_zero hp.out.ne_zero

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : Field k
inst✝ : IsAlgClosed k
a₁ : 𝕎 k
ha₁ : a₁.coeff 0 ≠ 0
a₂ : 𝕎 k
this✝ : solution p a₁ a₂ ^ (p - 1) = a₂.coeff 0 / a₁.coeff 0
this : ∃ k, p = k.succ
⊢ solution p a₁ a₂ ^ p * a₁.coeff 0 = solution p a₁ a₂ * a₂.coeff 0
Module: Mathlib.RingTheory.WittVector.MulCoeff

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ ↑p ^ (n + 1) * wittMul p (n + 1) + ↑p ^ (n + 1) * (↑p ^ (n + 1) * X (0, n + 1) * X (1, n + 1)) =
    ↑p ^ (n + 1) * (X (0, n + 1) * (rename (Prod.mk 1)) (wittPolynomial p ℤ (n + 1))) +
      (↑p ^ (n + 1) * (X (1, n + 1) * (rename (Prod.mk 0)) (wittPolynomial p ℤ (n + 1))) +
        (remainder p n - wittPolyProdRemainder p (n + 1)))

Tactic:
rw [mul_polyOfInterest_aux4 p n]

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ -(↑p ^ (n + 1) * X (0, n + 1)) * (↑p ^ (n + 1) * X (1, n + 1)) +
            ↑p ^ (n + 1) * X (0, n + 1) * (rename (Prod.mk 1)) (wittPolynomial p ℤ (n + 1)) +
          ↑p ^ (n + 1) * X (1, n + 1) * (rename (Prod.mk 0)) (wittPolynomial p ℤ (n + 1)) +
        (remainder p n - wittPolyProdRemainder p (n + 1)) +
      ↑p ^ (n + 1) * (↑p ^ (n + 1) * X (0, n + 1) * X (1, n + 1)) =
    ↑p ^ (n + 1) * (X (0, n + 1) * (rename (Prod.mk 1)) (wittPolynomial p ℤ (n + 1))) +
      (↑p ^ (n + 1) * (X (1, n + 1) * (rename (Prod.mk 0)) (wittPolynomial p ℤ (n + 1))) +
        (remainder p n - wittPolyProdRemainder p (n + 1)))
Module: Mathlib.SetTheory.Cardinal.Cofinality.Club

Goal state before:
pp: α : Type v
inst✝ : LinearOrder α
s : Set (Set α)
hα : cof α ≤ 1
hs : ∀ x ∈ s, IsClub x
⊢ IsClub (⋂₀ s)

Tactic:
cases isEmpty_or_nonempty α

Goal state after:
case inl
α : Type v
inst✝ : LinearOrder α
s : Set (Set α)
hα : cof α ≤ 1
hs : ∀ x ∈ s, IsClub x
h✝ : IsEmpty α
⊢ IsClub (⋂₀ s)

case inr
α : Type v
inst✝ : LinearOrder α
s : Set (Set α)
hα : cof α ≤ 1
hs : ∀ x ∈ s, IsClub x
h✝ : Nonempty α
⊢ IsClub (⋂₀ s)
Module: Mathlib.SetTheory.Cardinal.Cofinality.Club

Goal state before:
pp: α : Type v
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
s : Set (Set α)
hα : cof α ≠ ℵ₀
hsα : #↑s < cof α
hs : ∀ x ∈ s, IsClub x
⊢ IsClub (⋂₀ s)

Tactic:
cases isEmpty_or_nonempty α

Goal state after:
case inl
α : Type v
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
s : Set (Set α)
hα : cof α ≠ ℵ₀
hsα : #↑s < cof α
hs : ∀ x ∈ s, IsClub x
h✝ : IsEmpty α
⊢ IsClub (⋂₀ s)

case inr
α : Type v
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
s : Set (Set α)
hα : cof α ≠ ℵ₀
hsα : #↑s < cof α
hs : ∀ x ∈ s, IsClub x
h✝ : Nonempty α
⊢ IsClub (⋂₀ s)
Module: Mathlib.SetTheory.Cardinal.UnivLE

Goal state before:
pp: ⊢ UnivLE.{u, v} ↔ Nonempty (Ordinal.{u} ↪ Ordinal.{v})

Tactic:
by
  rw [univLE_iff_cardinal_le]
  exact lift_mk_le'

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Cofinality.Club

Goal state before:
pp: α : Type v
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
f : α → α
hα : cof α ≠ ℵ₀
hf : IsNormal f
⊢ IsClub (Function.fixedPoints f)

Tactic:
cases isEmpty_or_nonempty α

Goal state after:
case inl
α : Type v
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
f : α → α
hα : cof α ≠ ℵ₀
hf : IsNormal f
h✝ : IsEmpty α
⊢ IsClub (Function.fixedPoints f)

case inr
α : Type v
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
f : α → α
hα : cof α ≠ ℵ₀
hf : IsNormal f
h✝ : Nonempty α
⊢ IsClub (Function.fixedPoints f)
Module: Mathlib.SetTheory.Ordinal.FixedPointApproximants

Goal state before:
pp: case ind
α : 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
⊢ lfpApprox f x b = lfpApprox f x a

Tactic:
| ind b IH
   => 

Goal state after:
case ind
α : 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
⊢ lfpApprox f x b = lfpApprox f x 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
e' : Ordinal.{u_1}
⊢ (e' ∈ f.support.sort fun x1 x2 ↦ x1 ≥ x2) →
    ∀ (b_1 : Ordinal.{u_1}), b ^ e' * ((single e x) e' + f e') + b_1 = b ^ e' * f e' + b_1

Tactic:
he'

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
e' : Ordinal.{u_1}
he' : e' ∈ f.support.sort fun x1 x2 ↦ x1 ≥ x2
⊢ ∀ (b_1 : Ordinal.{u_1}), b ^ e' * ((single e x) e' + f e') + b_1 = b ^ e' * f e' + b_1
Module: Mathlib.SetTheory.Ordinal.Topology

Goal state before:
pp: p o : Ordinal.{u_1}
S : Set Ordinal.{u_1}
hpo : p < o
⊢ AccPt p (𝓟 S) ↔ AccPt ⟨p, hpo⟩ (𝓟 (Iio o ↓∩ S))

Tactic:
rw [← comap_principal, isOpen_Iio.isOpenEmbedding_subtypeVal.accPt_comap_iff]

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

Goal state before:
pp: case inr
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₁ ∧ (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✝)

Tactic:
ite_eq_iff

Goal state after:
case inr
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₁ ∧ (↑n₂ < ↑n₁ ∧ Ordering.gt = Ordering.lt ∨ ¬↑n₂ < ↑n₁ ∧ 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✝)
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: case inr
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
left✝ : ↑n₂ ≤ ↑n₁
nh : (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:
ite_eq_iff

Goal state after:
case inr
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
left✝ : ↑n₂ ≤ ↑n₁
nh : ↑n₂ < ↑n₁ ∧ Ordering.gt = Ordering.gt ∨ ¬↑n₂ < ↑n₁ ∧ 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.Notation

Goal state before:
pp: case eq.inr
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
nhl : ↑n₂ ≤ ↑n₁
nhr : (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✝)

Tactic:
ite_eq_iff

Goal state after:
case eq.inr
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
nhl : ↑n₂ ≤ ↑n₁
nhr : ↑n₂ < ↑n₁ ∧ Ordering.gt = Ordering.eq ∨ ¬↑n₂ < ↑n₁ ∧ 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✝)
Module: Mathlib.SetTheory.ZFC.Basic

Goal state before:
pp: x✝ y z x : ZFSet.{u}
a : PSet.{u}
⊢ Small.{u, u + 1} ↥(⟦a⟧)

Tactic:
let f (i : a.Type) : mk a := ⟨mk <| a.Func i, func_mem a i⟩
    suffices Function.Surjective f by exact small_of_surjective this
    rintro ⟨y, hb⟩
    induction y using Quotient.inductionOn
    obtain ⟨i, h⟩ := hb
    exact ⟨i, Subtype.coe_injective (Quotient.sound h.symm)⟩

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

Goal state before:
pp: case refine_1
x y z : ZFSet.{u_1}
h : {x, y} = {z}
⊢ x = z ∧ y = z

Tactic:
← mem_singleton,

Goal state after:
case refine_1
x y z : ZFSet.{u_1}
h : {x, y} = {z}
⊢ x ∈ {z} ∧ y = z
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: case oadd.lt
e : ONote
n : ℕ+
a o : ONote
h₁ : (e.oadd n a).NF
h₂ : o.NF
this✝¹ : a.NF
h' : (a.add o).repr = a.repr + o.repr
e' : ONote
n' : ℕ+
a' : ONote
h : a.add o = e'.oadd n' a'
nf : (e'.oadd n' a').NF
this✝ : e.NF
this : e'.NF
he : e.cmp e' = Ordering.lt
ee : e < e'
⊢ ω ^ e'.repr * ↑↑n' + a'.repr = ω ^ e.repr * ↑↑n + ω ^ e'.repr * ↑↑n' + a'.repr

Tactic:
@add_of_omega0_opow_le _ (repr e') (ω ^ repr e' * (n' : ℕ))

Goal state after:
case oadd.lt
e : ONote
n : ℕ+
a o : ONote
h₁ : (e.oadd n a).NF
h₂ : o.NF
this✝¹ : a.NF
h' : (a.add o).repr = a.repr + o.repr
e' : ONote
n' : ℕ+
a' : ONote
h : a.add o = e'.oadd n' a'
nf : (e'.oadd n' a').NF
this✝ : e.NF
this : e'.NF
he : e.cmp e' = Ordering.lt
ee : e < e'
⊢ ω ^ e'.repr * ↑↑n' + a'.repr = ω ^ e'.repr * ↑↑n' + a'.repr

case oadd.lt.h₁
e : ONote
n : ℕ+
a o : ONote
h₁ : (e.oadd n a).NF
h₂ : o.NF
this✝¹ : a.NF
h' : (a.add o).repr = a.repr + o.repr
e' : ONote
n' : ℕ+
a' : ONote
h : a.add o = e'.oadd n' a'
nf : (e'.oadd n' a').NF
this✝ : e.NF
this : e'.NF
he : e.cmp e' = Ordering.lt
ee : e < e'
⊢ ω ^ e.repr * ↑↑n < ω ^ e'.repr

case oadd.lt.h₂
e : ONote
n : ℕ+
a o : ONote
h₁ : (e.oadd n a).NF
h₂ : o.NF
this✝¹ : a.NF
h' : (a.add o).repr = a.repr + o.repr
e' : ONote
n' : ℕ+
a' : ONote
h : a.add o = e'.oadd n' a'
nf : (e'.oadd n' a').NF
this✝ : e.NF
this : e'.NF
he : e.cmp e' = Ordering.lt
ee : e < e'
⊢ ω ^ e'.repr ≤ ω ^ e'.repr * ↑↑n'
Module: Mathlib.SetTheory.ZFC.Class

Goal state before:
pp: A : Class.{u}
x : ZFSet.{u}
x✝ : A.ToSet ↑x
y : ZFSet.{u}
yx : ↑y = ↑x
py : A y
⊢ A x

Tactic:
ofSet.inj yx

Goal state after:
A : Class.{u}
x : ZFSet.{u}
x✝ : A.ToSet ↑x
y : ZFSet.{u}
yx : ↑y = ↑x
py : A x
⊢ A x
Module: Mathlib.SetTheory.ZFC.VonNeumann

Goal state before:
pp: case mpr
o : Ordinal.{u_1}
x : ZFSet.{u_1}
hx : ∀ ⦃y : ZFSet.{u_1}⦄, y ∈ x → y.rank < o
y : ZFSet.{u_1}
hy : y ∈ x
⊢ y ∈ V_ o

Tactic:
rw [mem_vonNeumann']
    have := hx hy
    exact ⟨_, this, subset_vonNeumann.2 le_rfl⟩

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

Goal state before:
pp: x : ZFSet.{u_1}
⊢ x ∈ V_ (succ x.rank)

Tactic:
simp [mem_vonNeumann]

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

Goal state before:
pp: a b : Ordinal.{u}
⊢ V_ a ∈ V_ b ↔ a < b

Tactic:
simp [mem_vonNeumann]

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

Goal state before:
pp: ⊢ ∀ (y : ZFSet.{u_1}), y ∉ V_ 0

Tactic:
simp [mem_vonNeumann]

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' : Type u_3
inst✝ : HSMul R' A A
r' : R'
r r'' : R
hr : r = r''
h_smul : ∀ (a : A), r • a = r' • a
a : A
⊢ r' • a = ((algebraMap R A) r'' + 0) * a

Tactic:
simp [← h_smul, ← hr, Algebra.smul_def r a]

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

Goal state before:
pp: case cons.cons
x e : ℝ
es : List ℝ
ih :
  ∀ {basis : Basis},
    WellFormedBasis basis →
      (∀ f ∈ basis, 0 < f x) → 0 < toFun es basis x ∧ (log ∘ toFun es basis) x = toLogFun es basis x
b : ℝ → ℝ
bs : List (ℝ → ℝ)
h_basis : WellFormedBasis (b :: bs)
hx : ∀ f ∈ b :: bs, 0 < f x
hpos : 0 < toFun es bs x
heq : (log ∘ toFun es bs) x = toLogFun es bs x
⊢ log (b x ^ e * toFun es bs x) = e * log (b x) + toLogFun es bs x

Tactic:
rw [Real.log_mul (Real.rpow_pos_of_pos (hx b (by simp)) _).ne' hpos.ne',
            Real.log_rpow (hx b (by simp)), ← heq]

Goal state after:
case cons.cons
x e : ℝ
es : List ℝ
ih :
  ∀ {basis : Basis},
    WellFormedBasis basis →
      (∀ f ∈ basis, 0 < f x) → 0 < toFun es basis x ∧ (log ∘ toFun es basis) x = toLogFun es basis x
b : ℝ → ℝ
bs : List (ℝ → ℝ)
h_basis : WellFormedBasis (b :: bs)
hx : ∀ f ∈ b :: bs, 0 < f x
hpos : 0 < toFun es bs x
heq : (log ∘ toFun es bs) x = toLogFun es bs x
⊢ e * log (b x) + log (toFun es bs x) = e * log (b x) + (log ∘ toFun es bs) x
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs

Goal state before:
pp: basis_hd : ℝ → ℝ
basis_tl : List (ℝ → ℝ)
ms₁ ms₂ : MultiseriesExpansion (basis_hd :: basis_tl)
h : ms₁.seq = ms₂.seq ∧ ms₁.toFun = ms₂.toFun
⊢ ms₁ = ms₂

Tactic:
eq_mk ms₁,

Goal state after:
basis_hd : ℝ → ℝ
basis_tl : List (ℝ → ℝ)
ms₁ ms₂ : MultiseriesExpansion (basis_hd :: basis_tl)
h : ms₁.seq = ms₂.seq ∧ ms₁.toFun = ms₂.toFun
⊢ mk ms₁.seq ms₁.toFun = ms₂
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic

Goal state before:
pp: case cons.cons.cons
basis_hd : ℝ → ℝ
basis_tl : List (ℝ → ℝ)
h_basis : WellFormedBasis (basis_hd :: basis_tl)
exp1 : ℝ
m1 : List ℝ
h1 : (exp1 :: m1).length = (basis_hd :: basis_tl).length
exp2 : ℝ
m2 : List ℝ
h2 : (exp2 :: m2).length = (basis_hd :: basis_tl).length
h_lt : exp1 :: m1 < exp2 :: m2
⊢ toFun (exp1 :: m1) (basis_hd :: basis_tl) =o[atTop] toFun (exp2 :: m2) (basis_hd :: basis_tl)

Tactic:
cases h_lt with
  | cons h =>
    simp only [toFun_cons]
    apply IsBigO.mul_isLittleO (isBigO_refl _ _)
    exact isLittleO_of_lt h_basis.tail (by simpa using h1) (by simpa using h2) h
  | rel h =>
    simp only [List.length_cons, Nat.add_right_cancel_iff, toFun_cons] at h1 h2 ⊢
    apply IsLittleO.of_tendsto_div_atTop
    apply Filter.Tendsto.congr' (f₁ := UnitMonomial.toFun ((exp2 - exp1) ::
      UnitMonomial.mul m2 (UnitMonomial.inv m1)) (basis_hd :: basis_tl))
    · simp only [toFun_cons, Pi.mul_apply, Pi.pow_apply]
      grw [mul_toFun h_basis.tail (by grind [inv_length]), inv_toFun h_basis.tail]
      apply h_basis.head_eventually_pos.mono
      intro x hx
      simp only [Pi.mul_apply, Pi.pow_apply, Pi.inv_apply, Real.rpow_sub hx]
      field
    · apply toFun_tendsto_top_of_firstNonzeroIsPos h_basis
      · grind [inv_length, mul_length]
      · apply FirstNonzeroIsPos.of_head
        grind

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

Goal state before:
pp: ⊢ fastGrowingε₀ 1 = 2

Tactic:
by
  simp [fastGrowingε₀, show oadd 0 1 0 = 1 from rfl]

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

Goal state before:
pp: case inr
n p q : ℕ
h_coprime : p.Coprime q
hq : 0 < q
m : ℕ
hn : n ≠ 0
h : n ^ p = m ^ q
f : ℕ →₀ ℕ := Finsupp.mapRange (fun x ↦ x / q) ⋯ n.factorization
z : ℕ
⊢ n.factorization z = q * f z

Tactic:
Finsupp.mapRange_apply,

Goal state after:
case inr
n p q : ℕ
h_coprime : p.Coprime q
hq : 0 < q
m : ℕ
hn : n ≠ 0
h : n ^ p = m ^ q
f : ℕ →₀ ℕ := Finsupp.mapRange (fun x ↦ x / q) ⋯ n.factorization
z : ℕ
⊢ n.factorization z = q * (n.factorization z / q)
Module: Mathlib.Tactic.NormNum.LegendreSymbol

Goal state before:
pp: a b c : ℕ
r : ℤ
ha : a % 2 = 0
hb : b % 8 = 3
hc : a / 2 = c
hr : jacobiSymNat c b = r
⊢ (if b % 8 = 3 ∨ b % 8 = 5 then -jacobiSym (↑a / 2) b else jacobiSym (↑a / 2) b) = -jacobiSym (↑a / 2) b

pp: a b c : ℕ
r : ℤ
ha : a % 2 = 0
hb : b % 8 = 3
hc : a / 2 = c
hr : jacobiSymNat c b = r
⊢ b % 2 = 1

Tactic:
if_pos (by simp [hb])

Goal state after:
a b c : ℕ
r : ℤ
ha : a % 2 = 0
hb : b % 8 = 3
hc : a / 2 = c
hr : jacobiSymNat c b = r
⊢ -jacobiSym (↑a / 2) b = -jacobiSym (↑a / 2) b

a b c : ℕ
r : ℤ
ha : a % 2 = 0
hb : b % 8 = 3
hc : a / 2 = c
hr : jacobiSymNat c b = r
⊢ b % 2 = 1
Module: Mathlib.Tactic.NormNum.LegendreSymbol

Goal state before:
pp: a b c : ℕ
r : ℤ
ha : a % 2 = 0
hb : b % 8 = 5
hc : a / 2 = c
hr : jacobiSymNat c b = r
⊢ (if b % 8 = 3 ∨ b % 8 = 5 then -jacobiSym (↑a / 2) b else jacobiSym (↑a / 2) b) = -jacobiSym (↑a / 2) b

pp: a b c : ℕ
r : ℤ
ha : a % 2 = 0
hb : b % 8 = 5
hc : a / 2 = c
hr : jacobiSymNat c b = r
⊢ b % 2 = 1

Tactic:
if_pos (by simp [hb])

Goal state after:
a b c : ℕ
r : ℤ
ha : a % 2 = 0
hb : b % 8 = 5
hc : a / 2 = c
hr : jacobiSymNat c b = r
⊢ -jacobiSym (↑a / 2) b = -jacobiSym (↑a / 2) b

a b c : ℕ
r : ℤ
ha : a % 2 = 0
hb : b % 8 = 5
hc : a / 2 = c
hr : jacobiSymNat c b = r
⊢ b % 2 = 1
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 α 𝔖) =
    UniformSpace.comap ((⋃₀ 𝔖).domRestrict ∘ F) (Pi.uniformSpace fun i ↦ α)

Tactic:
by
  -- Recall that the uniform structure on `X →ᵤ[𝔖] α` is the one induced by all the maps
  -- `K.domRestrict : (X →ᵤ[𝔖] α) → (K →ᵤ α)` for `K ∈ 𝔖`. Its pullback along `F`, which is
  -- the LHS of our goal, is thus the uniform structure induced by the maps
  -- `K.domRestrict ∘ F : ι → (K →ᵤ α)` for `K ∈ 𝔖`.
  have H1 : (UniformOnFun.uniformSpace X α 𝔖).comap F =
      ⨅ (K ∈ 𝔖), (UniformFun.uniformSpace _ _).comap (K.domRestrict ∘ F) := by
    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]
  -- Now, note that a similar fact is true for the uniform structure on `X → α` induced by
  -- the map `(⋃₀ 𝔖).domRestrict : (X → α) → ((⋃₀ 𝔖) → α)`: it is equal to the one induced by
  -- all maps `K.domRestrict : (X → α) → (K → α)` for `K ∈ 𝔖`, which means that the RHS of our
  -- goal is the uniform structure induced by the maps `K.domRestrict ∘ F : ι → (K → α)`
  -- for `K ∈ 𝔖`.
  have H2 : (Pi.uniformSpace _).comap ((⋃₀ 𝔖).domRestrict ∘ F) =
      ⨅ (K ∈ 𝔖), (Pi.uniformSpace _).comap (K.domRestrict ∘ F) := by
    simp_rw [UniformSpace.comap_comap, Pi.uniformSpace_comap_restrict_sUnion (fun _ ↦ α) 𝔖,
      UniformSpace.comap_iInf]
  -- But, for `K ∈ 𝔖` fixed, we know that the uniform structures of `K →ᵤ α` and `K → α`
  -- induce, via the equicontinuous family `K.domRestrict ∘ F`, the same uniform structure on `ι`.
  have H3 : ∀ K ∈ 𝔖, (UniformFun.uniformSpace K α).comap (K.domRestrict ∘ F) =
      (Pi.uniformSpace _).comap (K.domRestrict ∘ F) := fun K hK ↦ by
    have : CompactSpace K := isCompact_iff_compactSpace.mp (𝔖_compact K hK)
    exact (equicontinuous_restrict_iff _ |>.mpr <| F_eqcont K hK).comap_uniformFun_eq
  -- Combining these three facts completes the proof.
  simp_rw [H1, H2, iInf_congr fun K ↦ iInf_congr fun hK ↦ H3 K hK]

Goal state after:
Module: Mathlib.Topology.CantorBendixson

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
s : Set X
a : Ordinal.{u}
ha : sᵈ[a + 1] = sᵈ[a]
⊢ relDerivedSet sᵈ[a] = sᵈ[a]

Tactic:
simpa [iteratedDerivedSet_succ] using ha.symm

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

Goal state before:
pp: X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝² : T2Space X
inst✝¹ : RelCWComplex C D
inst✝ : FiniteDimensional C
E : Subcomplex C
n : ℕ
hn : IsEmpty (cell C n)
⊢ IsEmpty (cell (↑E) n)

Tactic:
simp [isEmpty_subtype]

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
Z : Type v'
inst✝ : IsGeneratedBy X Y
f : Y → Z
⊢ IsGeneratedBy X Z

Tactic:
let _ := tY.coinduced f
  refine iff_le_generatedBy.2 ?_
  exact ((equiv_symm_comp_continuous_iff (X := X) f).2 continuous_coinduced_rng).coinduced_le

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

Goal state before:
pp: X : Compactum
A : Set X.A
F : Ultrafilter X.A
hF : cl A ∈ F
⊢ X.str F ∈ cl A

Tactic:
exact cl_cl _ ⟨F, hF, rfl⟩

Goal state after:
Module: Mathlib.Topology.Category.Profinite.Product

Goal state before:
pp: ι : Type u
X : ι → Type
inst✝² : (i : ι) → TopologicalSpace (X i)
C : Set ((i : ι) → X i)
J✝ K : ι → Prop
inst✝¹ : ∀ (i : ι), T2Space (X i)
inst✝ : ∀ (i : ι), TotallyDisconnectedSpace (X i)
hC : IsCompact C
this : CompactSpace ↑C
a : (fun X ↦ ↑X.toTop) (limitCone (indexFunctor hC)).pt
J : Finset ι
s : ↑(obj C fun x ↦ x ∈ J)
⊢ IsClosed {s}

Tactic:
exact T1Space.t1 s

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

Goal state before:
pp: X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝ : RelCWComplex C D
e : cell C 1
⊢ cellFrontier 1 e = ↑(map 1 e) '' {-1, 1}

Tactic:
rw [cellFrontier]

Goal state after:
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝ : RelCWComplex C D
e : cell C 1
⊢ ↑(map 1 e) '' sphere 0 1 = ↑(map 1 e) '' {-1, 1}
Module: Mathlib.Topology.Category.Profinite.Nobeling.ZeroLimit

Goal state before:
pp: I : Type u_1
inst✝ : LinearOrder I
⊢ {m | m < nil} = ∅

Tactic:
by
  ext ⟨m, hm⟩
  refine ⟨fun h ↦ ?_, by tauto⟩
  simp only [Set.mem_ofPred_eq, lt_iff_lex_lt, nil, List.not_lex_nil] at h

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

Goal state before:
pp: case zero.zero
X : Type u_1
t : TopologicalSpace X
C D : Set X
hD : IsDiscrete D
Dc : IsClosed[t] D
j :
  match 0 with
  | 0 => ↑D
  | n.succ => PEmpty.{u_1 + 1}
a✝¹ : ⟨0, j⟩ ∈ univ
i :
  match 0 with
  | 0 => ↑D
  | n.succ => PEmpty.{u_1 + 1}
a✝ : ⟨0, i⟩ ∈ univ
ne : ⟨0, j⟩ ≠ ⟨0, i⟩
⊢ Disjoint
    ((fun a ↦
        ↑(match ⟨0, j⟩.fst, ⟨0, j⟩.snd with
            | 0, i => PartialEquiv.single ![] ↑i
            | n.succ, i => i.elim)
          a) ''
      ball 0 1)
    ((fun a ↦
        ↑(match ⟨0, i⟩.fst, ⟨0, i⟩.snd with
            | 0, i => PartialEquiv.single ![] ↑i
            | n.succ, i => i.elim)
          a) ''
      ball 0 1)

Tactic:
simp_all [Subtype.coe_injective.ne]

Goal state after: