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

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
R' : Type u_2
inst✝¹ : CommRing R'
e : R ≃+* R'
inst✝ : IsRegularRing R
this : IsNoetherianRing R'
p : Ideal R'
⊢ ∀ [inst : p.IsPrime], IsRegularLocalRing (Localization.AtPrime p)

Tactic:
hp

Goal state after:
R : Type u_1
inst✝² : CommRing R
R' : Type u_2
inst✝¹ : CommRing R'
e : R ≃+* R'
inst✝ : IsRegularRing R
this : IsNoetherianRing R'
p : Ideal R'
hp : p.IsPrime
⊢ IsRegularLocalRing (Localization.AtPrime p)
Module: Mathlib.RingTheory.RegularLocalRing.Defs

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
p : Ideal R
⊢ ∀ [inst : p.IsPrime], IsRegularLocalRing (Localization.AtPrime p)

Tactic:
hp

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
p : Ideal R
hp : p.IsPrime
⊢ IsRegularLocalRing (Localization.AtPrime p)
Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation

Goal state before:
pp: A : Type u_1
inst✝¹ : CommRing A
g : A⟦X⟧
I : Ideal A
H : g.IsWeierstrassDivisorAt I
a : A
f : A⟦X⟧
inst✝ : IsAdicComplete I A
⊢ H.div (a • f) = a • H.div f

Tactic:
by
  have H1 := (H.isWeierstrassDivisionAt_div_mod f).smul a
  have H2 := H.isWeierstrassDivisionAt_div_mod (a • f)
  exact (H.eq_of_mul_add_eq_mul_add H2.degree_lt H1.degree_lt
    (H2.eq_mul_add.symm.trans H1.eq_mul_add)).1

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

Goal state before:
pp: A : Type u_1
inst✝² : CommRing A
inst✝¹ : IsLocalRing A
f : A⟦X⟧
inst✝ : IsPrecomplete (IsLocalRing.maximalIdeal A) A
⊢ f %ʷ 0 = 0

Tactic:
rw [weierstrassMod, dif_neg (by simp)]

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

Goal state before:
pp: A : Type u_1
inst✝² : CommRing A
inst✝¹ : IsLocalRing A
f : A⟦X⟧
inst✝ : IsPrecomplete (IsLocalRing.maximalIdeal A) A
⊢ f %ʷ 0 = 0

Tactic:
by
  rw [weierstrassMod, dif_neg (by simp)]

Goal state after:
Module: Mathlib.RingTheory.Regular.ProjectiveDimension

Goal state before:
pp: R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : Small.{v, u} R
inst✝³ : IsLocalRing R
inst✝² : IsNoetherianRing R
M : ModuleCat R
inst✝¹ : Nontrivial ↑M
inst✝ : Module.Finite R ↑M
rs : List R
reg : IsWeaklyRegular (↑M) rs
mem : ∀ r ∈ rs, r ∈ maximalIdeal R
n : ℕ
len : rs.length = n
⊢ projectiveDimension (of R (↑M ⧸ Ideal.ofList rs • ⊤)) = projectiveDimension M + ↑n

Tactic:
induction n generalizing M rs with

Goal state after:
Module: Mathlib.RingTheory.Regular.ProjectiveDimension

Goal state before:
pp: R : Type u
inst✝³ : CommRing R
inst✝² : Small.{v, u} R
inst✝¹ : IsLocalRing R
inst✝ : IsNoetherianRing R
rs : List R
reg : RingTheory.Sequence.IsRegular R rs
mem_max : ∀ x ∈ rs, x ∈ maximalIdeal R
⊢ Submodule.map (↑(Shrink.linearEquiv R R).symm) (Ideal.ofList rs • ⊤) = Ideal.ofList rs • ⊤

Tactic:
Submodule.map_smul''

Goal state after:
R : Type u
inst✝³ : CommRing R
inst✝² : Small.{v, u} R
inst✝¹ : IsLocalRing R
inst✝ : IsNoetherianRing R
rs : List R
reg : RingTheory.Sequence.IsRegular R rs
mem_max : ∀ x ∈ rs, x ∈ maximalIdeal R
⊢ Ideal.ofList rs • Submodule.map ↑(Shrink.linearEquiv R R).symm ⊤ = Ideal.ofList rs • ⊤
Module: Mathlib.RingTheory.Spectrum.Prime.Homeomorph

Goal state before:
pp: k : Type u_1
K : Type u_2
R : Type u_3
inst✝⁵ : Field k
inst✝⁴ : Field K
inst✝³ : Algebra k K
inst✝² : CommRing R
inst✝¹ : Algebra k R
inst✝ : IsPurelyInseparable k K
⊢ IsHomeomorph (comap (algebraMap R (R ⊗[k] K)))

Tactic:
let q := ringExpChar k

Goal state after:
k : Type u_1
K : Type u_2
R : Type u_3
inst✝⁵ : Field k
inst✝⁴ : Field K
inst✝³ : Algebra k K
inst✝² : CommRing R
inst✝¹ : Algebra k R
inst✝ : IsPurelyInseparable k K
q : ℕ := ringExpChar k
⊢ IsHomeomorph (comap (algebraMap R (R ⊗[k] K)))
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Moebius

Goal state before:
pp: case neg
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a b : α
h : IsRelPrime a b
h✝ : Nontrivial α
ha : Squarefree a
hb : ¬Squarefree b
⊢ moebius (a * b) = moebius a * moebius b

pp: case pos
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a b : α
h : IsRelPrime a b
h✝ : Nontrivial α
ha : Squarefree a
hb : Squarefree b
⊢ moebius (a * b) = moebius a * moebius b

Tactic:
· simp [hb, mt Squarefree.of_mul_right hb]

Goal state after:
case pos
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a b : α
h : IsRelPrime a b
h✝ : Nontrivial α
ha : Squarefree a
hb : Squarefree b
⊢ moebius (a * b) = moebius a * moebius b
Module: Mathlib.RingTheory.Valuation.ValuativeRel.Trivial

Goal state before:
pp: R Γ : Type
inst✝³ : Ring R
inst✝² : DecidableEq R
inst✝¹ : IsDomain R
inst✝ : LinearOrderedCommGroupWithZero Γ
h : ValuativeRel R
hv : Valuation.Compatible 1
x✝¹ x✝ : R
⊢ x✝¹ ≤ᵥ x✝ ↔ if x✝ = 0 then x✝¹ = 0 else True

Tactic:
rw [hv.vle_iff_le]

Goal state after:
R Γ : Type
inst✝³ : Ring R
inst✝² : DecidableEq R
inst✝¹ : IsDomain R
inst✝ : LinearOrderedCommGroupWithZero Γ
h : ValuativeRel R
hv : Valuation.Compatible 1
x✝¹ x✝ : R
⊢ 1 x✝¹ ≤ 1 x✝ ↔ if x✝ = 0 then x✝¹ = 0 else True
Module: Mathlib.RingTheory.WittVector.Compare

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : CharP R p
i : ℕ
hin : i < n
this : ↑p ^ i = (WittVector.truncate n) (↑p ^ i)
⊢ ¬(WittVector.truncate n) (↑p ^ i) = 0

Tactic:
TruncatedWittVector.ext_iff,

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : CharP R p
i : ℕ
hin : i < n
this : ↑p ^ i = (WittVector.truncate n) (↑p ^ i)
⊢ ¬∀ (i_1 : Fin n), coeff i_1 ((WittVector.truncate n) (↑p ^ i)) = coeff i_1 0
Module: Mathlib.SetTheory.Descriptive.Tree

Goal state before:
pp: A : Type u_1
T : ↥(tree A)
x y : List A
hl : x.length ≤ y.length
⊢ (∃ z ∈ T, y = x ++ z) → y ∈ pullSub T x

Tactic:
simp +contextual [pullSub]

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

Goal state before:
pp: α : Type u
inst✝ : CompleteLattice α
f : α →o α
x : α
a b : Ordinal.{u}
h : a < b
⊢ f (lfpApprox f x a) ≤ lfpApprox f x b

Tactic:
nth_rw 2 [lfpApprox]

Goal state after:
α : Type u
inst✝ : CompleteLattice α
f : α →o α
x : α
a b : Ordinal.{u}
h : a < b
⊢ f (lfpApprox f x a) ≤ x ⊔ ⨆ b_1, ⨆ (_ : b_1 < b), f (lfpApprox f x b_1)
Module: Mathlib.SetTheory.Ordinal.FixedPointApproximants

Goal state before:
pp: α : Type u
inst✝ : CompleteLattice α
f : α →o α
x : α
a b : Ordinal.{u}
h : a < b
⊢ f (lfpApprox f x a) ≤ lfpApprox f x b

Tactic:
by
  nth_rw 2 [lfpApprox]
  exact le_sup_of_le_right <| le_iSup₂_of_le a h le_rfl

Goal state after:
Module: Mathlib.SetTheory.Lists

Goal state before:
pp: case C0
α : Type u_1
trans : Lists α → Prop := fun l₁ ↦ ∀ ⦃l₂ l₃ : Lists α⦄, l₁ ~ l₂ → l₂ ~ l₃ → l₁ ~ l₃
a : α
l₂ l₃ : Lists α
⊢ atom a ~ l₂ → l₂ ~ l₃ → atom a ~ l₃

Tactic:
h₁

Goal state after:
case C0
α : Type u_1
trans : Lists α → Prop := fun l₁ ↦ ∀ ⦃l₂ l₃ : Lists α⦄, l₁ ~ l₂ → l₂ ~ l₃ → l₁ ~ l₃
a : α
l₂ l₃ : Lists α
h₁ : atom a ~ l₂
⊢ l₂ ~ l₃ → atom a ~ l₃
Module: Mathlib.SetTheory.Lists

Goal state before:
pp: case C1
α : Type u_1
trans : Lists α → Prop := fun l₁ ↦ ∀ ⦃l₂ l₃ : Lists α⦄, l₁ ~ l₂ → l₂ ~ l₃ → l₁ ~ l₃
l₁ : Lists' α true
IH : ∀ (l' : Lists α), l' ∈ l₁.toList → trans l'
l₂ l₃ : Lists α
⊢ of' l₁ ~ l₂ → l₂ ~ l₃ → of' l₁ ~ l₃

Tactic:
h₁

Goal state after:
case C1
α : Type u_1
trans : Lists α → Prop := fun l₁ ↦ ∀ ⦃l₂ l₃ : Lists α⦄, l₁ ~ l₂ → l₂ ~ l₃ → l₁ ~ l₃
l₁ : Lists' α true
IH : ∀ (l' : Lists α), l' ∈ l₁.toList → trans l'
l₂ l₃ : Lists α
h₁ : of' l₁ ~ l₂
⊢ l₂ ~ l₃ → of' l₁ ~ l₃
Module: Mathlib.SetTheory.Ordinal.FixedPointApproximants

Goal state before:
pp: case ind
α : Type u
inst✝ : CompleteLattice α
f : α →o α
x a : α
ha : a ∈ fixedPoints ⇑f
hxa : x ≤ a
i : Ordinal.{u}
IH : ∀ y < i, lfpApprox f x y ≤ a
⊢ ⨆ b, ⨆ (_ : b < i), f (lfpApprox f x b) ≤ a

Tactic:
rw [iSup₂_le_iff, ← ha.eq]

Goal state after:
case ind
α : Type u
inst✝ : CompleteLattice α
f : α →o α
x a : α
ha : a ∈ fixedPoints ⇑f
hxa : x ≤ a
i : Ordinal.{u}
IH : ∀ y < i, lfpApprox f x y ≤ a
⊢ ∀ i_1 < i, f (lfpApprox f x i_1) ≤ f a
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: case oadd'
o : ONote
b₁ b₂ : Ordinal.{0}
e✝ : ONote
n✝ : ℕ+
a✝ : ONote
eb✝ b✝ : Ordinal.{0}
h₁ : e✝.NFBelow eb✝
h₂ : a✝.NFBelow e✝.repr
h₃ : e✝.repr < b✝
a_ih✝¹ : eb✝ ≤ b₂ → e✝.NFBelow b₂
a_ih✝ : e✝.repr ≤ b₂ → a✝.NFBelow b₂
bb : b✝ ≤ b₂
⊢ (e✝.oadd n✝ a✝).NFBelow b₂

Tactic:
| oadd' h₁ h₂ h₃ _ _ =>

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

Goal state before:
pp: case eq.inr.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.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:
obtain rfl := Subtype.ext (nhl.eq_of_not_lt nhr.1)

Goal state after:
case eq.inr.inr
o₁ e₁ a₁ o₂ : ONote
n₂ : ℕ+
a₂ : ONote
h✝¹ : o₂ = e₁.oadd n₂ a₂
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.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.Ordinal.Veblen

Goal state before:
pp: f : Ordinal.{u} → Ordinal.{u}
hf : IsNormal f
o : Ordinal.{u}
⊢ veblenWith f (o + 1) = deriv (veblenWith f o)

Tactic:
deriv_eq_enumOrd (isNormal_veblenWith hf o),

Goal state after:
f : Ordinal.{u} → Ordinal.{u}
hf : IsNormal f
o : Ordinal.{u}
⊢ veblenWith f (o + 1) = enumOrd (Function.fixedPoints (veblenWith f o))
Module: Mathlib.SetTheory.Ordinal.Veblen

Goal state before:
pp: f : Ordinal.{u} → Ordinal.{u}
o a : Ordinal.{u}
hf : IsNormal f
⊢ veblenWith f o (f a) = f a ↔ veblenWith f o a = a

Tactic:
simpa using veblenWith_veblenWith_eq_veblenWith_iff hf zero_le

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

Goal state before:
pp: f : Ordinal.{u} → Ordinal.{u}
o₁ o₂ a b : Ordinal.{u}
hf : IsNormal f
⊢ veblenWith f o₁ a = veblenWith f o₂ b ↔
    o₁ = o₂ ∧ a = b ∨ o₁ < o₂ ∧ a = veblenWith f o₂ b ∨ o₂ < o₁ ∧ veblenWith f o₁ a = b

Tactic:
by
  rw [← cmp_eq_eq_iff, cmp_veblenWith hf]
  aesop (add simp lt_asymm)

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

Goal state before:
pp: case pos
x : Ordinal.{u}
h : x.invVeblen₁ = 0
⊢ ω ^ x ∈ range (veblen x.invVeblen₁)

pp: case neg
x : Ordinal.{u}
h : ¬x.invVeblen₁ = 0
⊢ ω ^ x ∈ range (veblen x.invVeblen₁)

Tactic:
· simp [h]

Goal state after:
case neg
x : Ordinal.{u}
h : ¬x.invVeblen₁ = 0
⊢ ω ^ x ∈ range (veblen x.invVeblen₁)
Module: Mathlib.SetTheory.Ordinal.Veblen

Goal state before:
pp: case inr
x : Ordinal.{u_1}
h : 0 < x.invVeblen₁
⊢ x.invVeblen₂ ≤ x

Tactic:
· convert! (invVeblen₂_lt x).le
    rw [← veblen_zero_apply, veblen_eq_of_lt_invVeblen₁ h]

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

Goal state before:
pp: x y f : ZFSet.{u}
⊢ f ∈ x.funs y ↔ x.IsFunc y f

Tactic:
by simp [funs, IsFunc]

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

Goal state before:
pp: case pos
e₁ : ONote
n₁ : ℕ+
a₁ : ONote
n₂ : ℕ+
a₂ : ONote
b : Ordinal.{0}
h₁ : (e₁.oadd n₁ a₁).NFBelow b
h' : (a₁.sub a₂).NFBelow e₁.repr
h₂ : (e₁.oadd n₂ a₂).NF
h : e₁.cmp e₁ = Ordering.eq
en : n₁ = n₂
⊢ (a₁.sub a₂).NFBelow b

Tactic:
exact h'.mono (le_of_lt h₁.lt)

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

Goal state before:
pp: x y : Class.{u}
h : Set.Nonempty x
H : ∀ z ∈ x, y ∈ z
⊢ ∃ x_1, ↑x_1 = y ∧ ∀ (z : ZFSet.{u}), x z → x_1 ∈ z

Tactic:
obtain ⟨z, hz⟩ := h

Goal state after:
x y : Class.{u}
H : ∀ z ∈ x, y ∈ z
z : ZFSet.{u}
hz : z ∈ x
⊢ ∃ x_1, ↑x_1 = y ∧ ∀ (z : ZFSet.{u}), x z → x_1 ∈ z
Module: Mathlib.SetTheory.ZFC.Class

Goal state before:
pp: A : Class.{u_1}
hA : A.powerset ⊆ A
⊢ ∀ (x : ZFSet.{u_1}), A x

Tactic:
by_contra! hnA

Goal state after:
A : Class.{u_1}
hA : A.powerset ⊆ A
hnA : ∃ x, ¬A x
⊢ False
Module: Mathlib.SetTheory.ZFC.Class

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

Tactic:
exact ⟨_, h, rfl⟩

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

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

case refine_2.inr
x : ZFSet.{u_1}
h : x.IsOrdinal
y z w : ZFSet.{u_1}
hyz : y ∈ z
hzw : z ∈ w
hw✝ : w ∈ insert x x
hw : w ∈ x
⊢ y ∈ w
Module: Mathlib.SetTheory.ZFC.VonNeumann

Goal state before:
pp: case limit
o : Ordinal.{u}
ho : IsSuccLimit o
ih : ∀ o' < o, (V_ o').card = preBeth o'
⊢ (V_ o).card = ⨆ a, (V_ ↑a).card

Tactic:
vonNeumann_of_isSuccPrelimit ho.isSuccPrelimit

Goal state after:
case limit
o : Ordinal.{u}
ho : IsSuccLimit o
ih : ∀ o' < o, (V_ o').card = preBeth o'
⊢ (⋃ (a : ↑(Set.Iio o)), V_ ↑a).card = ⨆ a, (V_ ↑a).card
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Majorized

Goal state before:
pp: b : ℝ → ℝ
h_tendsto : Tendsto b atTop atTop
c exp : ℝ
h_exp : exp > 0
⊢ (fun x ↦ c) =o[atTop] (b ^ exp)

Tactic:
apply Asymptotics.isLittleO_const_left.mpr

Goal state after:
b : ℝ → ℝ
h_tendsto : Tendsto b atTop atTop
c exp : ℝ
h_exp : exp > 0
⊢ c = 0 ∨ Tendsto (norm ∘ (b ^ exp)) atTop atTop
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basis

Goal state before:
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 only [List.concat_eq_append, List.mem_append, List.mem_cons, List.not_mem_nil, or_false,
    List.getLast?_append, List.getLast?_singleton, Option.some_or, Option.some.injEq,
    forall_eq'] at hg h_comp

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

Goal state before:
pp: case pos
α : Type u_1
s t : Stream' α
h : s = t
⊢ dist s t ≤ 1

pp: case neg
α : Type u_1
s t : Stream' α
h : ¬s = t
⊢ dist s t ≤ 1

Tactic:
· simp [h]

Goal state after:
case neg
α : Type u_1
s t : Stream' α
h : ¬s = t
⊢ dist s t ≤ 1
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion

Goal state before:
pp: case pos
α : Type u_1
x : α
s t : Stream'.Seq α
h : s = t
⊢ dist (Seq.cons x s) (Seq.cons x t) = 2⁻¹ * dist s t

pp: case neg
α : Type u_1
x : α
s t : Stream'.Seq α
h : s ≠ t
⊢ dist (Seq.cons x s) (Seq.cons x t) = 2⁻¹ * dist s t

Tactic:
· simp [h]

Goal state after:
case neg
α : Type u_1
x : α
s t : Stream'.Seq α
h : s ≠ t
⊢ dist (Seq.cons x s) (Seq.cons x t) = 2⁻¹ * dist s t
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion

Goal state before:
pp: α : Type u_1
op₁ op₂ : Stream'.Seq α → Stream'.Seq α
h₁ : FriendlyOperation op₁
h₂ : FriendlyOperation op₂
P : Option α → Prop
inst✝ : DecidablePred P
⊢ FriendlyOperation fun s ↦ if P s.head then op₁ s else op₂ s

Tactic:
by
  rw [friendlyOperation_iff_dist_le_dist] at h₁ h₂ ⊢
  intro s t
  by_cases! h_head : s.head ≠ t.head
  · simp [dist_eq_one_of_head h_head]
  grind

Goal state after:
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 α
inst✝ : FriendlyOperationClass op
b : β
h : F b = none
⊢ gcorec F op b = nil

Tactic:
have := (FriendlyOperation.exists_fixed_point F op).choose_spec b
  simpa [h] using! this

Goal state after:
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 α
inst✝ : FriendlyOperationClass op
b : β
a : α
c : γ
b' : β
h : F b = some (a, c, b')
⊢ gcorec F op b = Seq.cons a (op c (gcorec F op b'))

Tactic:
have := (FriendlyOperation.exists_fixed_point F op).choose_spec b
  simpa [h] using! this

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

Goal state before:
pp: case neg.h
o₁ o₂ : ONote
inst✝¹ : o₁.NF
inst✝ : o₂.NF
N₁ : zero.NF
m : ℕ
e₁ : o₁.split = (zero, m + 1)
r₁ : o₁.repr = zero.repr + ↑(m + 1)
b' : ONote
k : ℕ
e₂ : o₂.split' = (b', k)
left✝ : b'.NF
r₂ : o₂.repr = ω * b'.repr + ↑k
h : ¬m = 0
⊢ ↑m + 1 < ω

Tactic:
← Nat.cast_succ,

Goal state after:
case neg.h
o₁ o₂ : ONote
inst✝¹ : o₁.NF
inst✝ : o₂.NF
N₁ : zero.NF
m : ℕ
e₁ : o₁.split = (zero, m + 1)
r₁ : o₁.repr = zero.repr + ↑(m + 1)
b' : ONote
k : ℕ
e₂ : o₂.split' = (b', k)
left✝ : b'.NF
r₂ : o₂.repr = ω * b'.repr + ↑k
h : ¬m = 0
⊢ ↑m.succ < ω
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs

Goal state before:
pp: case h.h.h.inl
γ : Type u_1
basis_hd : ℝ → ℝ
basis_tl : Basis
op : γ → Multiseries basis_hd basis_tl → Multiseries basis_hd basis_tl
inst✝ : FriendlyOperationClass op
x✝ y✝ : Multiseries basis_hd basis_tl
motive : Multiseries basis_hd basis_tl → Multiseries basis_hd basis_tl → Prop
base : motive x✝ y✝
step :
  ∀ (x y : Multiseries basis_hd basis_tl),
    motive x y → x = y ∨ ∃ exp coef c x' y', x = cons exp coef (op c x') ∧ y = cons exp coef (op c y') ∧ motive x' y'
x y : Stream'.Seq (ℝ × MultiseriesExpansion basis_tl)
ih : motive x y
h : x = y
⊢ x = y ∨ ∃ hd u' v' c, x = Seq.cons hd (op c u') ∧ y = Seq.cons hd (op c v') ∧ motive u' v'

pp: case h.h.h.inr
γ : Type u_1
basis_hd : ℝ → ℝ
basis_tl : Basis
op : γ → Multiseries basis_hd basis_tl → Multiseries basis_hd basis_tl
inst✝ : FriendlyOperationClass op
x y : Multiseries basis_hd basis_tl
motive : Multiseries basis_hd basis_tl → Multiseries basis_hd basis_tl → Prop
base : motive x y
step :
  ∀ (x y : Multiseries basis_hd basis_tl),
    motive x y → x = y ∨ ∃ exp coef c x' y', x = cons exp coef (op c x') ∧ y = cons exp coef (op c y') ∧ motive x' y'
exp : ℝ
coef : MultiseriesExpansion basis_tl
c : γ
x' y' : Multiseries basis_hd basis_tl
h_next : motive x' y'
ih : motive (cons exp coef (op c x')) (cons exp coef (op c y'))
⊢ cons exp coef (op c x') = cons exp coef (op c y') ∨
    ∃ hd u' v' c_1,
      cons exp coef (op c x') = Seq.cons hd (op c_1 u') ∧
        cons exp coef (op c y') = Seq.cons hd (op c_1 v') ∧ motive u' v'

Tactic:
· simp [h]

Goal state after:
case h.h.h.inr
γ : Type u_1
basis_hd : ℝ → ℝ
basis_tl : Basis
op : γ → Multiseries basis_hd basis_tl → Multiseries basis_hd basis_tl
inst✝ : FriendlyOperationClass op
x y : Multiseries basis_hd basis_tl
motive : Multiseries basis_hd basis_tl → Multiseries basis_hd basis_tl → Prop
base : motive x y
step :
  ∀ (x y : Multiseries basis_hd basis_tl),
    motive x y → x = y ∨ ∃ exp coef c x' y', x = cons exp coef (op c x') ∧ y = cons exp coef (op c y') ∧ motive x' y'
exp : ℝ
coef : MultiseriesExpansion basis_tl
c : γ
x' y' : Multiseries basis_hd basis_tl
h_next : motive x' y'
ih : motive (cons exp coef (op c x')) (cons exp coef (op c y'))
⊢ cons exp coef (op c x') = cons exp coef (op c y') ∨
    ∃ hd u' v' c_1,
      cons exp coef (op c x') = Seq.cons hd (op c_1 u') ∧
        cons exp coef (op c y') = Seq.cons hd (op c_1 v') ∧ motive u' v'
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic

Goal state before:
pp: exps_hd : ℝ
exps_tl : List ℝ
basis_hd : ℝ → ℝ
basis_tl : List (ℝ → ℝ)
h_basis : WellFormedBasis (basis_hd :: basis_tl)
h_length : (exps_hd :: exps_tl).length = (basis_hd :: basis_tl).length
h : exps_hd = 0 ∧ FirstNonzeroIsPos exps_tl
x : ℝ
⊢ toFun (exps_hd :: exps_tl) (basis_hd :: basis_tl) x = toFun exps_tl basis_tl x

Tactic:
simp [UnitMonomial.toFun, h.left]

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

Goal state before:
pp: exps_hd : ℝ
exps_tl : List ℝ
basis_hd : ℝ → ℝ
basis_tl : List (ℝ → ℝ)
h_basis : WellFormedBasis (basis_hd :: basis_tl)
h_length : (exps_hd :: exps_tl).length = (basis_hd :: basis_tl).length
h : exps_hd = 0 ∧ FirstNonzeroIsNeg exps_tl
x : ℝ
⊢ toFun (exps_hd :: exps_tl) (basis_hd :: basis_tl) x = toFun exps_tl basis_tl x

Tactic:
simp [UnitMonomial.toFun, h.left]

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

Goal state before:
pp: coef : ℝ
exps : UnitMonomial
basis : Basis
h_basis : WellFormedBasis basis
h_length : List.length exps = List.length basis
h_coef : coef < 0
h_exps : exps.FirstNonzeroIsPos
⊢ let t := { coef := coef, unit := exps };
  Tendsto (t.toFun basis) atTop atBot

Tactic:
intro t
  eta_expand
  simp only [toFun, Pi.smul_apply, smul_eq_mul]
  convert Filter.Tendsto.const_mul_atTop_of_neg h_coef
    (UnitMonomial.toFun_tendsto_top_of_firstNonzeroIsPos h_basis h_length h_exps)

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

Goal state before:
pp: case oadd.inr
a : ONote
m : ℕ+
b : ONote
iha : a.FundamentalSequenceProp a.fundamentalSequence
f : ℕ → ONote
e : b.fundamentalSequence = Sum.inr f
h1 : IsSuccLimit b.repr
h2 : ∀ (i : ℕ), f i < f (i + 1) ∧ f i < b ∧ (b.NF → (f i).NF)
h3 : ∀ a < b.repr, ∃ i, a < (f i).repr
⊢ IsSuccLimit (ω ^ a.repr * ↑↑m + b.repr) ∧
    (∀ (i : ℕ),
        a.oadd m (f i) < a.oadd m (f (i + 1)) ∧ a.oadd m (f i) < a.oadd m b ∧ ((a.oadd m b).NF → (a.oadd m (f i)).NF)) ∧
      ∀ a_1 < ω ^ a.repr * ↑↑m + b.repr, ∃ i, a_1 < ω ^ a.repr * ↑↑m + (f i).repr

Tactic:
exact
      ⟨isSuccLimit_add _ h1, fun i =>
        ⟨oadd_lt_oadd_3 (h2 i).1, oadd_lt_oadd_3 (h2 i).2.1, fun H =>
          H.fst.oadd _ (NF.below_of_lt' (lt_trans (h2 i).2.1 H.snd'.repr_lt) ((h2 i).2.2 H.snd))⟩,
        exists_lt_add h3⟩

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

Goal state before:
pp: a b c : ℕ
r : ℤ
ha : a % 2 = 0
hb : b % 8 = 1
hc : a / 2 = c
hr : jacobiSymNat c b = r
⊢ ¬(b % 8 = 3 ∨ b % 8 = 5)

Tactic:
by simp [hb]

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

Goal state before:
pp: a b c : ℕ
r : ℤ
ha : a % 2 = 0
hb : b % 8 = 7
hc : a / 2 = c
hr : jacobiSymNat c b = r
⊢ ¬(b % 8 = 3 ∨ b % 8 = 5)

Tactic:
by simp [hb]

Goal state after:
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
⊢ b % 8 = 3 ∨ b % 8 = 5

Tactic:
by simp [hb]

Goal state after:
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
⊢ b % 8 = 3 ∨ b % 8 = 5

Tactic:
by simp [hb]

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

Goal state before:
pp: x : ℝ
num den num_k : ℕ
hx_isNNRat : IsNNRat x num den
hx_coprime : num.Coprime den
hn1 : num_k ^ 2 < num
hn2 : num < (num_k + 1) ^ 2
⊢ IsNNRat (1 / 2) 1 2

Tactic:
exact ⟨Invertible.mk (1/2) (by simp) (by simp), by simp⟩

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

Goal state before:
pp: x : ℝ
num den den_k : ℕ
hx_isNNRat : IsNNRat x num den
hx_coprime : num.Coprime den
hd1 : den_k ^ 2 < den
hd2 : den < (den_k + 1) ^ 2
⊢ IsNNRat (1 / 2) 1 2

Tactic:
exact ⟨Invertible.mk (1/2) (by simp) (by simp), by simp⟩

Goal state after:
Module: Mathlib.Tactic.Simproc.FinsetInterval

Goal state before:
pp: m n : ℕ
hnm : n.blt m = true
⊢ Icc m n = ∅

Tactic:
simpa using hnm

Goal state after:
Module: Mathlib.Tactic.Simproc.FinsetInterval

Goal state before:
pp: m n : ℕ
s : Finset ℕ
hmn : m.ble n = true
hs : Icc (m + 1) n = s
⊢ m ≤ n

Tactic:
simpa using hmn

Goal state after:
Module: Mathlib.Tactic.Simproc.FinsetInterval

Goal state before:
pp: m n : ℤ
hnm : n < m
⊢ Icc m n = ∅

Tactic:
simpa using hnm

Goal state after:
Module: Mathlib.Tactic.Simproc.FinsetInterval

Goal state before:
pp: m n : ℤ
s : Finset ℤ
hmn : m ≤ n
hs : Icc (m + 1) n = s
⊢ m ≤ n

Tactic:
simpa using hmn

Goal state after: