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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
p : R[X]
hp : p.degree ≤ 2
⊢ p = C (p.coeff 2) * X ^ 2 + C (p.coeff 1) * X + C (p.coeff 0)

Tactic:
p.as_sum_range_C_mul_X_pow'
    (Nat.lt_of_le_of_lt (natDegree_le_iff_degree_le.mpr hp) (Nat.lt_add_one 2))

Goal state after:
R : Type u_1
inst✝ : Semiring R
p : R[X]
hp : p.degree ≤ 2
⊢ ∑ i ∈ Finset.range (2 + 1), C (p.coeff i) * X ^ i =
    C ((∑ i ∈ Finset.range (2 + 1), C (p.coeff i) * X ^ i).coeff 2) * X ^ 2 +
        C ((∑ i ∈ Finset.range (2 + 1), C (p.coeff i) * X ^ i).coeff 1) * X +
      C ((∑ i ∈ Finset.range (2 + 1), C (p.coeff i) * X ^ i).coeff 0)
Module: Mathlib.RingTheory.Polynomial.ShiftedLegendre

Goal state before:
pp: n : ℕ
⊢ (⇑derivative)^[n] (X ^ n * (1 - X) ^ n) = ↑n ! * shiftedLegendre n

Tactic:
calc
  _ = derivative^[n] (((X : ℤ[X]) - X ^ 2) ^ n) := by
    rw [← mul_pow, mul_one_sub, ← pow_two]
  _ = derivative^[n] (∑ m ∈ range (n + 1), n.choose m • (-1) ^ m * X ^ (n + m)) := by
    congr
    rw [sub_eq_add_neg, add_comm, add_pow]
    congr! 1 with m hm
    rw [neg_pow, pow_two, mul_pow, ← mul_assoc, mul_comm, mul_assoc, pow_mul_pow_sub, mul_assoc,
      ← pow_add, ← mul_assoc, nsmul_eq_mul, add_comm]
    rw [Finset.mem_range] at hm
    linarith
  _ = ∑ x ∈ range (n + 1), ↑((n + x)! / x !) * C (↑(n.choose x) * (-1) ^ x) * X ^ x := by
    rw [iterate_derivative_sum]
    congr! 1 with x _
    rw [show (n.choose x • (-1) ^ x : ℤ[X]) = C (n.choose x • (-1) ^ x) by simp,
      iterate_derivative_C_mul, iterate_derivative_X_pow_eq_smul,
      descFactorial_eq_div (by lia), show n + x - n = x by lia]
    simp only [Int.reduceNeg, nsmul_eq_mul, eq_intCast, Int.cast_mul, Int.cast_natCast,
      Int.cast_pow, Int.cast_neg, Int.cast_one, zsmul_eq_mul]
    ring
  _ = ∑ i ∈ range (n + 1), ↑n ! * C ((-1) ^ i * ↑(n.choose i) * ↑((n + i).choose n)) * X ^ i := by
    congr! 2 with x _
    rw [C_mul (b := ((n + x).choose n : ℤ)), mul_comm, mul_comm (n ! : ℤ[X]), mul_comm _ ((-1) ^ x),
      mul_assoc]
    congr 1
    rw [add_comm, add_choose]
    simp only [Int.natCast_ediv, cast_mul, eq_intCast]
    norm_cast
    rw [mul_comm, ← Nat.mul_div_assoc]
    · rw [mul_comm, Nat.mul_div_mul_right _ _ (by positivity)]
    · simp only [factorial_mul_factorial_dvd_factorial_add]
  _ = (n ! : ℤ[X]) * (shiftedLegendre n) := by simp [← mul_assoc, shiftedLegendre, mul_sum]

Goal state after:
Module: Mathlib.RingTheory.PolynomialLaw.Basic

Goal state before:
pp: R : Type u
inst✝⁸ : CommSemiring R
M : Type u_1
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
N : Type u_2
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
f : M →ₚₗ[R] N
S : Type u
inst✝³ : CommSemiring S
inst✝² : Algebra R S
S' : Type u
inst✝¹ : CommSemiring S'
inst✝ : Algebra R S'
φ : S →ₐ[R] S'
x : S ⊗[R] M
⊢ (rTensor N φ.toLinearMap) (f.toFun' S x) = f.toFun' S' ((rTensor M φ.toLinearMap) x)

Tactic:
simpa only using! congr_fun (f.isCompat' φ) x

Goal state after:
Module: Mathlib.RingTheory.PowerSeries.Schroder

Goal state before:
pp: n : ℕ
hn : 0 < n
⊢ (coeff n) (X * largeSchroderSeries ^ 2) = ∑ i ∈ range n, i.largeSchroder * (n - 1 - i).largeSchroder

Tactic:
pow_two,

Goal state after:
n : ℕ
hn : 0 < n
⊢ (coeff n) (X * (largeSchroderSeries * largeSchroderSeries)) =
    ∑ i ∈ range n, i.largeSchroder * (n - 1 - i).largeSchroder
Module: Mathlib.RingTheory.TensorProduct.DirectLimitFG

Goal state before:
pp: R : Type u
M : Type u_1
N : Type u_2
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
inst✝² : AddCommMonoid N
inst✝¹ : Module R N
inst✝ : DecidableEq { P // P.FG }
Q : { Q // Q.FG }
u : M ⊗[R] ↥↑Q
⊢ (directLimit R M N)
      ((Module.DirectLimit.of R { Q // Q.FG } (fun Q ↦ M ⊗[R] ↥↑Q) (fun x x_1 hPQ ↦ lTensor M (inclusion hPQ)) Q) u) =
    (lTensor M (↑Q).subtype) u

Tactic:
by
  suffices (Submodule.FG.lTensor.directLimit R M N).toLinearMap.comp
      (Module.DirectLimit.of R {Q : Submodule R N // Q.FG} (fun Q ↦ M ⊗[R] Q.val)
        (fun _ _ hPQ ↦ lTensor M (inclusion hPQ)) Q)
      = lTensor M (Submodule.subtype Q.val) by
    exact DFunLike.congr_fun this u
  ext p n
  simp [Submodule.FG.lTensor.directLimit, Submodule.FG.directLimit]

Goal state after:
Module: Mathlib.RingTheory.PolynomialLaw.Basic

Goal state before:
pp: R : Type u
inst✝² : CommSemiring R
S : Type v
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
s : Finset S
⊢ (aeval fun n ↦ ↑(s.equivFin.symm n)).range = Algebra.adjoin R ↑s

Tactic:
rw [← Algebra.adjoin_range_eq_range_aeval]

Goal state after:
R : Type u
inst✝² : CommSemiring R
S : Type v
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
s : Finset S
⊢ Algebra.adjoin R (Set.range fun n ↦ ↑(s.equivFin.symm n)) = Algebra.adjoin R ↑s
Module: Mathlib.RingTheory.RegularLocalRing.Defs

Goal state before:
pp: case neg
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsLocalRing R
inst✝¹ : IsDomain R
inst✝ : IsPrincipalIdealRing R
isf : ¬IsField R
x : R
hx : maximalIdeal R = R ∙ x
⊢ ↑(Submodule.spanFinrank (maximalIdeal R)) ≤ ringKrullDim R

Tactic:
simpa only [(IsPrincipalIdealRing.ringKrullDim_eq_one R) isf,
      Nat.cast_le_one, ← Set.ncard_singleton x, hx] using
        Submodule.spanFinrank_span_le_ncard_of_finite (Set.finite_singleton x)

Goal state after:
Module: Mathlib.RingTheory.RegularLocalRing.Polynomial

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsRegularLocalRing R
p : Ideal R[X]
inst✝ : p.IsPrime
max : comap C p = maximalIdeal R
⊢ IsRegularLocalRing (Localization.AtPrime p)

Tactic:
apply IsRegularLocalRing.of_spanFinrank_maximalIdeal_le

Goal state after:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsRegularLocalRing R
p : Ideal R[X]
inst✝ : p.IsPrime
max : comap C p = maximalIdeal R
⊢ ↑(Submodule.spanFinrank (maximalIdeal (Localization.AtPrime p))) ≤ ringKrullDim (Localization.AtPrime p)
Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation

Goal state before:
pp: A : Type u_1
inst✝¹ : CommRing A
inst✝ : IsLocalRing A
g q : A⟦X⟧
r : A[X]
hg : (map (IsLocalRing.residue A)) g ≠ 0
n : ℕ := ((map (IsLocalRing.residue A)) g).order.toNat
H1 : r.degree < ↑n
H2 : (coeff n) (X ^ n) = (coeff n) ((map (IsLocalRing.residue A)) (g * q + ↑r))
⊢ IsUnit q

Tactic:
coeff_X_pow_self,

Goal state after:
A : Type u_1
inst✝¹ : CommRing A
inst✝ : IsLocalRing A
g q : A⟦X⟧
r : A[X]
hg : (map (IsLocalRing.residue A)) g ≠ 0
n : ℕ := ((map (IsLocalRing.residue A)) g).order.toNat
H1 : r.degree < ↑n
H2 : 1 = (coeff n) ((map (IsLocalRing.residue A)) (g * q + ↑r))
⊢ IsUnit q
Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation

Goal state before:
pp: case refine_1
A : Type u_1
inst✝¹ : CommRing A
inst✝ : IsLocalRing A
g q : A⟦X⟧
r : A[X]
hg : (map (IsLocalRing.residue A)) g ≠ 0
H✝ : (X ^ ((map (IsLocalRing.residue A)) g).order.toNat).IsWeierstrassDivision g q r
n : ℕ := ((map (IsLocalRing.residue A)) g).order.toNat
H : (X ^ n).IsWeierstrassDivision g q r
f : A[X] := Polynomial.X ^ n - r
H1 : r.degree < (Polynomial.X ^ n).degree
hfdeg : f.natDegree = n
i : ℕ
hi : i < f.natDegree
⊢ f.coeff i ∈ IsLocalRing.maximalIdeal A

Tactic:
rw [hfdeg] at hi

Goal state after:
case refine_1
A : Type u_1
inst✝¹ : CommRing A
inst✝ : IsLocalRing A
g q : A⟦X⟧
r : A[X]
hg : (map (IsLocalRing.residue A)) g ≠ 0
H✝ : (X ^ ((map (IsLocalRing.residue A)) g).order.toNat).IsWeierstrassDivision g q r
n : ℕ := ((map (IsLocalRing.residue A)) g).order.toNat
H : (X ^ n).IsWeierstrassDivision g q r
f : A[X] := Polynomial.X ^ n - r
H1 : r.degree < (Polynomial.X ^ n).degree
hfdeg : f.natDegree = n
i : ℕ
hi : i < n
⊢ f.coeff i ∈ IsLocalRing.maximalIdeal A
Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation

Goal state before:
pp: A : Type u_1
inst✝² : CommRing A
inst✝¹ : IsLocalRing A
inst✝ : IsHausdorff (IsLocalRing.maximalIdeal A) A
g : A⟦X⟧
f f' : A[X]
h h' : A⟦X⟧
H : g.IsWeierstrassFactorization f h
H2 : g.IsWeierstrassFactorization f' h'
h1 : ⋯.unit⁻¹ = ⋯.unit⁻¹
h2 :
  Polynomial.X ^ ((map (IsLocalRing.residue A)) g).order.toNat - f =
    Polynomial.X ^ ((map (IsLocalRing.residue A)) g).order.toNat - f'
⊢ f = f' ∧ h = h'

Tactic:
inv_inj,

Goal state after:
A : Type u_1
inst✝² : CommRing A
inst✝¹ : IsLocalRing A
inst✝ : IsHausdorff (IsLocalRing.maximalIdeal A) A
g : A⟦X⟧
f f' : A[X]
h h' : A⟦X⟧
H : g.IsWeierstrassFactorization f h
H2 : g.IsWeierstrassFactorization f' h'
h1 : ⋯.unit = ⋯.unit
h2 :
  Polynomial.X ^ ((map (IsLocalRing.residue A)) g).order.toNat - f =
    Polynomial.X ^ ((map (IsLocalRing.residue A)) g).order.toNat - f'
⊢ f = f' ∧ h = h'
Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation

Goal state before:
pp: A : Type u_1
inst✝² : CommRing A
inst✝¹ : IsLocalRing A
inst✝ : IsHausdorff (IsLocalRing.maximalIdeal A) A
g : A⟦X⟧
f f' : A[X]
h h' : A⟦X⟧
H : g.IsWeierstrassFactorization f h
H2 : g.IsWeierstrassFactorization f' h'
h1 : ⋯.unit = ⋯.unit
h2 :
  Polynomial.X ^ ((map (IsLocalRing.residue A)) g).order.toNat - f =
    Polynomial.X ^ ((map (IsLocalRing.residue A)) g).order.toNat - f'
⊢ f = f' ∧ h = h'

Tactic:
Units.ext_iff

Goal state after:
A : Type u_1
inst✝² : CommRing A
inst✝¹ : IsLocalRing A
inst✝ : IsHausdorff (IsLocalRing.maximalIdeal A) A
g : A⟦X⟧
f f' : A[X]
h h' : A⟦X⟧
H : g.IsWeierstrassFactorization f h
H2 : g.IsWeierstrassFactorization f' h'
h1 : ↑⋯.unit = ↑⋯.unit
h2 :
  Polynomial.X ^ ((map (IsLocalRing.residue A)) g).order.toNat - f =
    Polynomial.X ^ ((map (IsLocalRing.residue A)) g).order.toNat - f'
⊢ f = f' ∧ h = h'
Module: Mathlib.RingTheory.Valuation.ValuativeRel.Trivial

Goal state before:
pp: R✝ Γ : Type
inst✝⁶ : Ring R✝
inst✝⁵ : DecidableEq R✝
inst✝⁴ : IsDomain R✝
inst✝³ : LinearOrderedCommGroupWithZero Γ
R : Type
inst✝² : Semiring R
inst✝¹ : DecidableEq R
inst✝ : IsDomain R
x✝¹ x✝ : R
⊢ if x✝ * x✝¹ = 0 then x✝¹ * x✝ = 0 else True

Tactic:
simpa using Or.symm

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

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

Tactic:
intro n

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
⊢ ∀ (k : ℕ), (truncate k).comp ((fromPadicInt p).comp (toPadicInt p)) = (truncate k).comp (RingHom.id (𝕎 (ZMod p)))

Tactic:
intro n

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ (truncate n).comp ((fromPadicInt p).comp (toPadicInt p)) = (truncate n).comp (RingHom.id (𝕎 (ZMod p)))
Module: Mathlib.SetTheory.Cardinal.Cofinality.Club

Goal state before:
pp: α : Type v
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
ι : Type u
f : ι → Set α
hα : cof α ≠ ℵ₀
hι : lift.{v, u} #ι < lift.{u, v} (cof α)
hf : ∀ (i : ι), IsClub (f i)
⊢ #↑(range f) < cof α

Tactic:
← Cardinal.lift_lt

Goal state after:
α : Type v
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
ι : Type u
f : ι → Set α
hα : cof α ≠ ℵ₀
hι : lift.{v, u} #ι < lift.{u, v} (cof α)
hf : ∀ (i : ι), IsClub (f i)
⊢ lift.{?u.38, v} #↑(range f) < lift.{?u.38, v} (cof α)
Module: Mathlib.SetTheory.Descriptive.Tree

Goal state before:
pp: case inl
A : Type u_1
T : ↥(tree A)
x y : List A
h : y <+: x ∧ [] ∈ subAt T x
h' : y.length ≤ x.length
⊢ y ∈ ↑T

Tactic:
exact mem_of_prefix h.1 (by simpa using h.2)

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

Goal state before:
pp: α : Type v
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
ι : Type u
f : ι → Set α
hα : cof α ≠ ℵ₀
hι : lift.{v, u} #ι < lift.{u, v} (cof α)
⊢ #↑(range f) < cof α

Tactic:
← Cardinal.lift_lt

Goal state after:
α : Type v
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
ι : Type u
f : ι → Set α
hα : cof α ≠ ℵ₀
hι : lift.{v, u} #ι < lift.{u, v} (cof α)
⊢ lift.{?u.37, v} #↑(range f) < lift.{?u.37, v} (cof α)
Module: Mathlib.SetTheory.Ordinal.CantorNormalForm

Goal state before:
pp: b o : Ordinal.{u_1}
ho : o ≠ 0
hb : o < b
⊢ (0, o) :: CNF b (o % 1) = [(0, o)]

Tactic:
mod_one,

Goal state after:
b o : Ordinal.{u_1}
ho : o ≠ 0
hb : o < b
⊢ (0, o) :: CNF b 0 = [(0, o)]
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: case oadd'
o : ONote
b : Ordinal.{0}
e✝ : ONote
n✝ : ℕ+
a✝² : ONote
eb✝ b✝ : Ordinal.{0}
a✝¹ : e✝.NFBelow eb✝
a✝ : a✝².NFBelow e✝.repr
h₃ : e✝.repr < b✝
a_ih✝ : e✝.repr < ω ^ eb✝
IH : a✝².repr < ω ^ e✝.repr
⊢ (e✝.oadd n✝ a✝²).repr < ω ^ b✝

Tactic:
rw [repr]

Goal state after:
case oadd'
o : ONote
b : Ordinal.{0}
e✝ : ONote
n✝ : ℕ+
a✝² : ONote
eb✝ b✝ : Ordinal.{0}
a✝¹ : e✝.NFBelow eb✝
a✝ : a✝².NFBelow e✝.repr
h₃ : e✝.repr < b✝
a_ih✝ : e✝.repr < ω ^ eb✝
IH : a✝².repr < ω ^ e✝.repr
⊢ ω ^ e✝.repr * ↑↑n✝ + a✝².repr < ω ^ b✝
Module: Mathlib.SetTheory.Ordinal.CantorNormalForm

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

Tactic:
exact hb.pos

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

Goal state before:
pp: case cons
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✝
a : ↑(Iio o)
l : List ↑(Iio o)
IH : ∃ b < o, List.foldr (fun x ↦ veblenWith f ↑x) 0 l ≤ veblenWith f b 0
⊢ ∃ b < o, List.foldr (fun x ↦ veblenWith f ↑x) 0 (a :: l) ≤ veblenWith f b 0

Tactic:
| cons a l IH =>

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

Goal state before:
pp: x y : ZFSet.{u_1}
H : {x} = {y}
⊢ x = y

Tactic:
by
  let := congr_arg sUnion H
  rwa [sUnion_singleton, sUnion_singleton] at this

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

Goal state before:
pp: α : Type u_1
inst✝ : Small.{u, u_1} α
f : α → ZFSet.{u}
x : ZFSet.{u}
y : PSet.{u}
⊢ ⟦y⟧ ∈ range f ↔ ∃ i, f i = ⟦y⟧

Tactic:
constructor
    · rintro ⟨z, hz⟩
      exact ⟨(equivShrink α).symm z, Quotient.eq_mk_iff_out.2 hz.symm⟩
    · rintro ⟨z, hz⟩
      use equivShrink α z
      simpa [hz] using PSet.Equiv.symm (Quotient.mk_out y)

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

Goal state before:
pp: x✝ y✝ x y : ZFSet.{u}
IH :
  ∀ (a₂ b₂ : ZFSet.{u}),
    Sym2.GameAdd (fun x1 x2 ↦ x1 ∈ x2) s(a₂, b₂) s(x, y) → a₂.IsOrdinal → b₂.IsOrdinal → a₂ ⊆ b₂ → a₂ = b₂ ∨ a₂ ∈ b₂
hx : x.IsOrdinal
hy : y.IsOrdinal
hxy : x ⊆ y
hyx : ¬y ⊆ x
m : ZFSet.{u}
hm : m ∈ ↑y \ ↑x
hm' : ∀ x_1 ∈ ↑y \ ↑x, x_1 ∉ m
hmy : m ∈ y
z : ZFSet.{u}
hzm : z ∈ m
hzx : z ∉ x
⊢ False

Tactic:
exact hm' _ ⟨hy.mem_trans hzm hmy, hzx⟩ hzm

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

Goal state before:
pp: case pos
e₁ : ONote
n₁ : ℕ+
a₁ : ONote
n₂ : ℕ+
a₂ : ONote
h₁ : (e₁.oadd n₁ a₁).NF
this✝ : a₁.NF
this : a₂.NF
h' : (a₁.sub a₂).repr = a₁.repr - a₂.repr
h₂ : (e₁.oadd n₂ a₂).NF
h : e₁.cmp e₁ = Ordering.eq
mn : ↑n₁ - ↑n₂ = 0
en : n₁ = n₂
⊢ (if n₁ = n₂ then a₁.sub a₂ else 0).repr = (e₁.oadd n₁ a₁).repr - (e₁.oadd n₂ a₂).repr

Tactic:
simpa [en]

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

Goal state before:
pp: case inl
f g : ℝ → ℝ
h : WellFormedBasis []
h_comp : ∀ (g : ℝ → ℝ), [].getLast? = some g → (Real.log ∘ f) =o[atTop] (Real.log ∘ g)
hg : g ∈ []
⊢ (Real.log ∘ f) =o[atTop] (Real.log ∘ g)

pp: case inr
f g : ℝ → ℝ
basis_begin : List (ℝ → ℝ)
basis_end : ℝ → ℝ
h : WellFormedBasis (basis_begin.concat basis_end)
h_comp : ∀ (g : ℝ → ℝ), (basis_begin.concat basis_end).getLast? = some g → (Real.log ∘ f) =o[atTop] (Real.log ∘ g)
hg : g ∈ basis_begin.concat basis_end
⊢ (Real.log ∘ f) =o[atTop] (Real.log ∘ g)

Tactic:
· simp at hg

Goal state after:
case inr
f g : ℝ → ℝ
basis_begin : List (ℝ → ℝ)
basis_end : ℝ → ℝ
h : WellFormedBasis (basis_begin.concat basis_end)
h_comp : ∀ (g : ℝ → ℝ), (basis_begin.concat basis_end).getLast? = some g → (Real.log ∘ f) =o[atTop] (Real.log ∘ g)
hg : g ∈ basis_begin.concat basis_end
⊢ (Real.log ∘ f) =o[atTop] (Real.log ∘ g)
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs

Goal state before:
pp: basis_hd : ℝ → ℝ
basis_tl : Basis
op : Multiseries basis_hd basis_tl → Multiseries basis_hd basis_tl
motive : (Multiseries basis_hd basis_tl → Multiseries basis_hd basis_tl) → Prop
h_base : motive op
h_step :
  ∀ (op : Multiseries basis_hd basis_tl → Multiseries basis_hd basis_tl),
    motive op →
      ∃ T,
        ∀ (s : Multiseries basis_hd basis_tl),
          (op s).destruct =
            Option.map
              (fun x ↦
                match x with
                | (exp, coef, opf, op') => (exp, coef, ↑opf (↑op' s.tail)))
              (T s.head)
⊢ FriendlyOperation op

Tactic:
by
  refine Seq.FriendlyOperation.coind_comp_friend_left motive h_base (fun op h_op ↦ ?_)
  obtain ⟨T, hT⟩ := h_step op h_op
  use fun hd? ↦ (T hd?).map (fun (exp, coef, opf, op') => ((exp, coef), opf, op'))
  intro s
  rw [destruct_eq_destruct_map, hT s]
  simp
  rfl

Goal state after:
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
    · exact Seq.Pairwise_cons_nil
    · exact h_tl_tl.cons_cons_of_trans (by simpa [lt_iff_lt] using h_comp)

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

Goal state before:
pp: case cons.cons.cons.rel.hl
basis_hd : ℝ → ℝ
basis_tl : List (ℝ → ℝ)
h_basis : WellFormedBasis (basis_hd :: basis_tl)
exp1 : ℝ
m1 : List ℝ
exp2 : ℝ
m2 : List ℝ
h : exp1 < exp2
h1 : m1.length = basis_tl.length
h2 : m2.length = basis_tl.length
⊢ basis_hd ^ (exp2 - exp1) * (mul m2 (inv m1)).toFun basis_tl =ᶠ[atTop] fun x ↦
    basis_hd x ^ exp2 * toFun m2 basis_tl x / (basis_hd x ^ exp1 * toFun m1 basis_tl x)

Tactic:
grw [mul_toFun h_basis.tail (by grind [inv_length]), inv_toFun h_basis.tail]

Goal state after:
case cons.cons.cons.rel.hl
basis_hd : ℝ → ℝ
basis_tl : List (ℝ → ℝ)
h_basis : WellFormedBasis (basis_hd :: basis_tl)
exp1 : ℝ
m1 : List ℝ
exp2 : ℝ
m2 : List ℝ
h : exp1 < exp2
h1 : m1.length = basis_tl.length
h2 : m2.length = basis_tl.length
⊢ basis_hd ^ (exp2 - exp1) * (toFun m2 basis_tl * (toFun m1 basis_tl)⁻¹) =ᶠ[atTop] fun x ↦
    basis_hd x ^ exp2 * toFun m2 basis_tl x / (basis_hd x ^ exp1 * toFun m1 basis_tl x)
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion

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

Tactic:
intro n

Goal state after:
α : Type u_1
γ : Type u_3
s t : Stream'.Seq α
op : γ → Stream'.Seq α → Stream'.Seq α
inst✝ : FriendlyOperationClass op
motive : Stream'.Seq α → Stream'.Seq α → Prop
base : motive s t
step :
  ∀ (u v : Stream'.Seq α),
    motive u v → u = v ∨ ∃ hd u' v' c, u = Seq.cons hd (op c u') ∧ v = Seq.cons hd (op c v') ∧ motive u' v'
n : ℕ
⊢ dist s t ≤ 2⁻¹ ^ n
Module: Mathlib.Tactic.LinearCombinationPrime

Goal state before:
pp: α : Type u_1
a a' b b' : α
inst✝ : AddGroup α
p : a - b = 0
H : a' - b' = a - b
⊢ a' - b' = 0

Tactic:
p

Goal state after:
α : Type u_1
a a' b b' : α
inst✝ : AddGroup α
p : a - b = 0
H : a' - b' = 0
⊢ a' - b' = 0
Module: Mathlib.Tactic.LinearCombinationPrime

Goal state before:
pp: α : Type u_1
a a' b b' : α
inst✝¹ : Ring α
inst✝ : IsReduced α
n : ℕ
p : a - b = 0
H : (a' - b') ^ n = a - b
⊢ (a' - b') ^ n = 0

Tactic:
p

Goal state after:
α : Type u_1
a a' b b' : α
inst✝¹ : Ring α
inst✝ : IsReduced α
n : ℕ
p : a - b = 0
H : (a' - b') ^ n = 0
⊢ (a' - b') ^ n = 0
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.smul_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 • f z
Module: Mathlib.Tactic.NormNum.Irrational

Goal state before:
pp: case pos
a b d : ℕ
h_coprime : a.Coprime b
ha : ∀ (x : ℕ), a ≠ x ^ d
q : ℚ
hq : 0 ≤ q
hb_zero : b = 0
⊢ ↑a / ↑b ≠ q ^ d

Tactic:
subst hb_zero
    contrapose! ha
    simp only [Nat.coprime_zero_right] at h_coprime
    subst h_coprime
    use 1
    simp

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

Goal state before:
pp: A : Type u_1
inst✝³ : DivisionRing A
inst✝² : TopologicalSpace A
inst✝¹ : SeparatelyContinuousMul A
inst✝ : CharZero A
r : ℚ
⊢ Continuous fun x ↦ r • x

Tactic:
simpa only [Algebra.smul_def] using! continuous_id.const_mul _

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

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

Tactic:
induction xs generalizing ys with

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}, x ∈ Vn n → x * x ∈ Vn n → x ∈ Vn (n + 1)

Tactic:
intro n

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}, x ∈ Vn n → x * x ∈ Vn n → x ∈ Vn (n + 1)
Module: Mathlib.Topology.Algebra.Star.Unitary

Goal state before:
pp: R : Type u_1
inst✝⁵ : Monoid R
inst✝⁴ : StarMul R
inst✝³ : TopologicalSpace R
inst✝² : T1Space R
inst✝¹ : ContinuousStar R
inst✝ : ContinuousMul R
⊢ IsClosed ↑(unitary R)

Tactic:
let f (u : R) : R × R := (star u * u, u * star u)

Goal state after:
R : Type u_1
inst✝⁵ : Monoid R
inst✝⁴ : StarMul R
inst✝³ : TopologicalSpace R
inst✝² : T1Space R
inst✝¹ : ContinuousStar R
inst✝ : ContinuousMul R
f : R → R × R := fun u ↦ (star u * u, u * star u)
⊢ IsClosed ↑(unitary R)
Module: Mathlib.Topology.CWComplex.Classical.Subcomplex

Goal state before:
pp: case a
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝¹ : T2Space X
inst✝ : RelCWComplex C D
E : Subcomplex C
⊢ D ∪ ⋃ n, ⋃ j, openCell n ↑j ⊆ D ∪ ⋃ n, ⋃ j, closedCell n ↑j

Tactic:
apply union_subset_union_right

Goal state after:
case a
X : Type u_1
t : TopologicalSpace X
C D : Set X
inst✝¹ : T2Space X
inst✝ : RelCWComplex C D
E : Subcomplex C
⊢ ⋃ n, ⋃ j, openCell n ↑j ⊆ ⋃ n, ⋃ j, closedCell n ↑j
Module: Mathlib.Topology.DerivedSet

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
A : Set X
⊢ IsClosed[inst✝¹] (derivedSet (closure[inst✝¹] A))

Tactic:
isClosed_iff_derivedSet_subset

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
A : Set X
⊢ derivedSet (derivedSet (closure[inst✝¹] A)) ⊆ derivedSet (closure[inst✝¹] A)