mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.TensorProduct.DirectLimitFG

Goal state before:
pp: R : Type u
M : Type u_1
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
ι : Type u_3
inst✝² : Preorder ι
F : ι → Type u_4
inst✝¹ : (i : ι) → AddCommMonoid (F i)
inst✝ : (i : ι) → Module R (F i)
f : ⦃i j : ι⦄ → i ≤ j → F i →ₗ[R] F j
D : DirectedSystem F fun x x_1 h ↦ ⇑(f h)
i : ι
t : M ⊗[R] F i
⊢ (LinearMap.lTensor M (f ⋯)) t = t

Tactic:
← id_apply (R := R) t

Goal state after:
R : Type u
M : Type u_1
inst✝⁵ : CommSemiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
ι : Type u_3
inst✝² : Preorder ι
F : ι → Type u_4
inst✝¹ : (i : ι) → AddCommMonoid (F i)
inst✝ : (i : ι) → Module R (F i)
f : ⦃i j : ι⦄ → i ≤ j → F i →ₗ[R] F j
D : DirectedSystem F fun x x_1 h ↦ ⇑(f h)
i : ι
t : M ⊗[R] F i
⊢ (LinearMap.lTensor M (f ⋯)) (LinearMap.id t) = LinearMap.id t
Module: Mathlib.RingTheory.Radical.NatInt

Goal state before:
pp: z : ℤ
⊢ radical z = ↑(∏ p ∈ z.natAbs.primeFactors, p)

Tactic:
rw [← radical_natAbs_eq_radical, Nat.radical_eq_prod_primeFactors]

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

Goal state before:
pp: case succ
A : Type u_1
inst✝ : CommRing A
g : A⟦X⟧
I : Ideal A
H : g.IsWeierstrassDivisorAt I
f : A⟦X⟧
k i : ℕ
q : A⟦X⟧ := H.seq f k
s : A⟦X⟧ := f - g * q
n : ℕ := ((map (Ideal.Quotient.mk I)) g).order.toNat
hi : i ≥ n
hq : ∀ {i : ℕ}, i ≥ n → (coeff i) s ∈ I ^ k
s₀ : A[X] := (trunc n) s
s₁ : A⟦X⟧ := mk fun i ↦ (coeff (i + n)) s
hs : s = X ^ n * s₁ + ↑s₀
q' : A⟦X⟧ := q + s₁ * ↑⋯.unit⁻¹
key : f - g * q' = ↑s₀ - ↑((trunc n) g) * s₁ * ↑⋯.unit⁻¹
⊢ (if i < n then (coeff i) s else 0) - (coeff i) (↑((trunc n) g) * s₁ * ↑⋯.unit⁻¹) ∈ I ^ (k + 1)

Tactic:
if_neg hi.not_gt,

Goal state after:
case succ
A : Type u_1
inst✝ : CommRing A
g : A⟦X⟧
I : Ideal A
H : g.IsWeierstrassDivisorAt I
f : A⟦X⟧
k i : ℕ
q : A⟦X⟧ := H.seq f k
s : A⟦X⟧ := f - g * q
n : ℕ := ((map (Ideal.Quotient.mk I)) g).order.toNat
hi : i ≥ n
hq : ∀ {i : ℕ}, i ≥ n → (coeff i) s ∈ I ^ k
s₀ : A[X] := (trunc n) s
s₁ : A⟦X⟧ := mk fun i ↦ (coeff (i + n)) s
hs : s = X ^ n * s₁ + ↑s₀
q' : A⟦X⟧ := q + s₁ * ↑⋯.unit⁻¹
key : f - g * q' = ↑s₀ - ↑((trunc n) g) * s₁ * ↑⋯.unit⁻¹
⊢ 0 - (coeff i) (↑((trunc n) g) * s₁ * ↑⋯.unit⁻¹) ∈ I ^ (k + 1)
Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation

Goal state before:
pp: case inl
A : Type u_1
inst✝¹ : CommRing A
g : A⟦X⟧
I : Ideal A
H : g.IsWeierstrassDivisorAt I
inst✝ : IsHausdorff I A
q : A⟦X⟧
r : A[X]
hdeg : r.degree < ↑((map (Ideal.Quotient.mk I)) g).order.toNat
heq :
  ((X ^ ((map (Ideal.Quotient.mk I)) g).order.toNat *
          mk fun i ↦ (coeff (i + ((map (Ideal.Quotient.mk I)) g).order.toNat)) g) +
        ↑((trunc ((map (Ideal.Quotient.mk I)) g).order.toNat) g)) *
      q =
    ↑r
k : ℕ
ih : ∀ (i : ℕ), (coeff i) q ∈ I ^ k
i : ℕ
hi : i < ((map (Ideal.Quotient.mk I)) g).order.toNat
j : ℕ
hj : j ≤ i
⊢ (coeff j)
        (X ^ ((map (Ideal.Quotient.mk I)) g).order.toNat *
          mk fun i ↦ (coeff (i + ((map (Ideal.Quotient.mk I)) g).order.toNat)) g) +
      (coeff j) ↑((trunc ((map (Ideal.Quotient.mk I)) g).order.toNat) g) ∈
    I

Tactic:
Polynomial.coeff_coe

Goal state after:
case inl
A : Type u_1
inst✝¹ : CommRing A
g : A⟦X⟧
I : Ideal A
H : g.IsWeierstrassDivisorAt I
inst✝ : IsHausdorff I A
q : A⟦X⟧
r : A[X]
hdeg : r.degree < ↑((map (Ideal.Quotient.mk I)) g).order.toNat
heq :
  ((X ^ ((map (Ideal.Quotient.mk I)) g).order.toNat *
          mk fun i ↦ (coeff (i + ((map (Ideal.Quotient.mk I)) g).order.toNat)) g) +
        ↑((trunc ((map (Ideal.Quotient.mk I)) g).order.toNat) g)) *
      q =
    ↑r
k : ℕ
ih : ∀ (i : ℕ), (coeff i) q ∈ I ^ k
i : ℕ
hi : i < ((map (Ideal.Quotient.mk I)) g).order.toNat
j : ℕ
hj : j ≤ i
⊢ (coeff j)
        (X ^ ((map (Ideal.Quotient.mk I)) g).order.toNat *
          mk fun i ↦ (coeff (i + ((map (Ideal.Quotient.mk I)) g).order.toNat)) g) +
      ((trunc ((map (Ideal.Quotient.mk I)) g).order.toNat) g).coeff j ∈
    I
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
H1 : (a • f).IsWeierstrassDivisionAt g (a • H.div f) (a • H.mod f) I
⊢ H.div (a • f) = a • H.div f

Tactic:
have H2 := H.isWeierstrassDivisionAt_div_mod (a • f)

Goal state after:
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
H1 : (a • f).IsWeierstrassDivisionAt g (a • H.div f) (a • H.mod f) I
H2 : (a • f).IsWeierstrassDivisionAt g (H.div (a • f)) (H.mod (a • f)) I
⊢ H.div (a • f) = a • H.div f
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
H1 : (a • f).IsWeierstrassDivisionAt g (a • H.div f) (a • H.mod f) I
⊢ H.mod (a • f) = a • H.mod f

Tactic:
have H2 := H.isWeierstrassDivisionAt_div_mod (a • f)

Goal state after:
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
H1 : (a • f).IsWeierstrassDivisionAt g (a • H.div f) (a • H.mod f) I
H2 : (a • f).IsWeierstrassDivisionAt g (H.div (a • f)) (H.mod (a • f)) I
⊢ H.mod (a • f) = a • H.mod f
Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation

Goal state before:
pp: case inr
A : Type u_1
inst✝¹ : CommRing A
g✝ : A⟦X⟧
I✝ : Ideal A
g : A[X]
I : Ideal A
H : g.IsDistinguishedAt I
inst✝ : IsAdicComplete I A
h✝ : Nontrivial A
hI : I ≠ ⊤
this : Nontrivial (A ⧸ I)
f : A[X]
hfdeg : f.degree < g.degree
h1 : g.degree = ↑((map (Ideal.Quotient.mk I)) ↑g).order.toNat
⊢ (⇑(Ideal.Quotient.mk (Ideal.span {g})) ∘ ⇑⋯.mod')
      ((↑↑(Ideal.quotientMapₐ (Ideal.span {↑g}) (Polynomial.coeToPowerSeries.algHom A) ⋯).toRingHom).toFun
        ((Ideal.Quotient.mk (Ideal.span {g})) f)) =
    (Ideal.Quotient.mk (Ideal.span {g})) f

Tactic:
dsimp

Goal state after:
case inr
A : Type u_1
inst✝¹ : CommRing A
g✝ : A⟦X⟧
I✝ : Ideal A
g : A[X]
I : Ideal A
H : g.IsDistinguishedAt I
inst✝ : IsAdicComplete I A
h✝ : Nontrivial A
hI : I ≠ ⊤
this : Nontrivial (A ⧸ I)
f : A[X]
hfdeg : f.degree < g.degree
h1 : g.degree = ↑((map (Ideal.Quotient.mk I)) ↑g).order.toNat
⊢ (Ideal.Quotient.mk (Ideal.span {g})) (⋯.mod ↑f) = (Ideal.Quotient.mk (Ideal.span {g})) f
Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation

Goal state before:
pp: case neg
A : Type u_1
inst✝² : CommRing A
inst✝¹ : IsLocalRing A
f g : A⟦X⟧
inst✝ : IsPrecomplete (IsLocalRing.maximalIdeal A) A
hg : ¬(map (IsLocalRing.residue A)) g ≠ 0
⊢ Polynomial.degree 0 < ↑((map (IsLocalRing.residue A)) g).order.toNat

Tactic:
nontriviality A
    rw [Polynomial.degree_zero]
    exact WithBot.bot_lt_coe _

Goal state after:
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 < n
this : (coeff i) ↑r ∈ IsLocalRing.maximalIdeal A
⊢ r.coeff i ∈ IsLocalRing.maximalIdeal A

Tactic:
Polynomial.coeff_coe

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
this : r.coeff i ∈ IsLocalRing.maximalIdeal A
⊢ r.coeff i ∈ IsLocalRing.maximalIdeal A
Module: Mathlib.RingTheory.Valuation.AlgebraInstances

Goal state before:
pp: K : Type u_1
inst✝⁶ : Field K
v : Valuation K (WithZero (Multiplicative ℤ))
L : Type u_2
inst✝⁵ : Field L
inst✝⁴ : Algebra K L
E : Type ?u.16
inst✝³ : Field E
inst✝² : Algebra K E
inst✝¹ : Algebra L E
inst✝ : IsScalarTower K L E
⊢ ↑⟨(algebraMap L E) ↑1, ⋯⟩ = ↑1

Tactic:
by simp only [Subalgebra.coe_one, map_one]

Goal state after:
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₁ a₂ : 𝕎 k
ha₁ : a₁.coeff 0 ≠ 0
ha₂ : a₂.coeff 0 ≠ 0
h : solution p a₁ a₂ = 0
this : 0 ^ (p - 1) = a₂.coeff 0 / a₁.coeff 0
⊢ p - 1 ≠ 0

Tactic:
· exact Nat.sub_ne_zero_of_lt hp.out.one_lt

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

Goal state before:
pp: case refine_2
p : ℕ
inst✝⁵ : Fact (Nat.Prime p)
k : Type u_2
inst✝⁴ : Field k
inst✝³ : IsAlgClosed k
inst✝² : CharP k p
V : Type u_3
inst✝¹ : AddCommGroup V
inst✝ : Isocrystal p k V
h_dim : finrank K(p, k) V = 1
this✝ : Nontrivial V
x : V
hx : x ≠ 0
this : Φ(p, k) x ≠ 0
a : K(p, k)
ha : a ≠ 0
hax : Φ(p, k) x = a • x
b : K(p, k)
hb : b ≠ 0
m : ℤ
hmb : φ(p, k) b * a = ↑p ^ m * b
F₀ : StandardOneDimIsocrystal p k m →ₗ[K(p, k)] V := LinearMap.toSpanSingleton K(p, k) V x
⊢ F₀.range = ⊤

Tactic:
← (finrank_eq_one_iff_of_nonzero x hx).mp h_dim

Goal state after:
case refine_2
p : ℕ
inst✝⁵ : Fact (Nat.Prime p)
k : Type u_2
inst✝⁴ : Field k
inst✝³ : IsAlgClosed k
inst✝² : CharP k p
V : Type u_3
inst✝¹ : AddCommGroup V
inst✝ : Isocrystal p k V
h_dim : finrank K(p, k) V = 1
this✝ : Nontrivial V
x : V
hx : x ≠ 0
this : Φ(p, k) x ≠ 0
a : K(p, k)
ha : a ≠ 0
hax : Φ(p, k) x = a • x
b : K(p, k)
hb : b ≠ 0
m : ℤ
hmb : φ(p, k) b * a = ↑p ^ m * b
F₀ : StandardOneDimIsocrystal p k m →ₗ[K(p, k)] V := LinearMap.toSpanSingleton K(p, k) V x
⊢ F₀.range = K(p, k) ∙ x
Module: Mathlib.SetTheory.Cardinal.NatCount

Goal state before:
pp: p : ℕ → Prop
inst✝ : DecidablePred p
n : ℕ
h : {k | p k}.Finite
⊢ ↑(count p n) ≤ ↑{k | p k}.encard.toNat

Tactic:
ENat.natCast_toNat (by simpa)

Goal state after:
p : ℕ → Prop
inst✝ : DecidablePred p
n : ℕ
h : {k | p k}.Finite
⊢ ↑(count p n) ≤ {k | p k}.encard
Module: Mathlib.SetTheory.Cardinal.Cofinality.Club

Goal state before:
pp: α : Type v
s t : Set α
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
hα : cof α ≠ ℵ₀
hs : IsClub s
ht : IsClub t
⊢ IsClub (s ∩ t)

Tactic:
simpa [hs, ht] using IsClub.sInter_of_countable (s := {s, t}) hα

Goal state after:
Module: Mathlib.SetTheory.Descriptive.Tree

Goal state before:
pp: A : Type u_1
T : ↥(tree A)
⊢ pullSub T [] = T

Tactic:
by simp [pullSub]

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

Goal state before:
pp: case inr
o₁ o₂ : Ordinal.{u_1}
hcomm : AddCommute o₁ o₂
ih : ∀ y < o₁ + o₂, ∀ {o₁ o₂ : Ordinal.{u_1}}, AddCommute o₁ o₂ → o₁ + o₂ = y → ∃ o n₁ n₂, o * ↑n₁ = o₁ ∧ o * ↑n₂ = o₂
hle : o₁ ≤ o₂
h₁ : o₁ ≠ 0
o₃ : Ordinal.{u_1} := o₂ - o₁
hsub : o₁ + o₃ = o₂
hcomm' : AddCommute o₁ o₃
hlt : o₁ + o₃ < o₁ + o₂
⊢ ∃ o n₁ n₂, o * ↑n₁ = o₁ ∧ o * ↑n₂ = o₂

Tactic:
rcases ih _ hlt hcomm' rfl with ⟨o, n₁, n₃, hn₁, hn₃⟩

Goal state after:
case inr
o₁ o₂ : Ordinal.{u_1}
hcomm : AddCommute o₁ o₂
ih : ∀ y < o₁ + o₂, ∀ {o₁ o₂ : Ordinal.{u_1}}, AddCommute o₁ o₂ → o₁ + o₂ = y → ∃ o n₁ n₂, o * ↑n₁ = o₁ ∧ o * ↑n₂ = o₂
hle : o₁ ≤ o₂
h₁ : o₁ ≠ 0
o₃ : Ordinal.{u_1} := o₂ - o₁
hsub : o₁ + o₃ = o₂
hcomm' : AddCommute o₁ o₃
hlt : o₁ + o₃ < o₁ + o₂
o : Ordinal.{u_1}
n₁ n₃ : ℕ
hn₁ : o * ↑n₁ = o₁
hn₃ : o * ↑n₃ = o₃
⊢ ∃ o n₁ n₂, o * ↑n₁ = o₁ ∧ o * ↑n₂ = o₂
Module: Mathlib.SetTheory.Ordinal.FixedPointApproximants

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

Tactic:
exact le_sup_left

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

Goal state before:
pp: α : Type u
inst✝ : CompleteLattice α
f : α →o α
x : α
hx : x ≤ f x
a : Ordinal.{u}
⊢ ⨆ b, ⨆ (_ : b < a + 1), f (lfpApprox f x b) ≤ f (lfpApprox f x a)

Tactic:
simpa using fun i h ↦ f.monotone.comp (lfpApprox_mono_right f) h

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

Goal state before:
pp: b : Ordinal.{u_1}
hb : b ≤ 1
o a : Ordinal.{u_1}
⊢ (coeff b o) a = (single 0 o) a

Tactic:
obtain rfl | ho := eq_or_ne o 0

Goal state after:
case inl
b : Ordinal.{u_1}
hb : b ≤ 1
a : Ordinal.{u_1}
⊢ (coeff b 0) a = (single 0 0) a

case inr
b : Ordinal.{u_1}
hb : b ≤ 1
o a : Ordinal.{u_1}
ho : o ≠ 0
⊢ (coeff b o) a = (single 0 o) a
Module: Mathlib.SetTheory.Ordinal.FixedPointApproximants

Goal state before:
pp: case a
α : Type u
inst✝ : CompleteLattice α
f : α →o α
h_lfp : ∃ y, lfp f = ↑y
y : ↑(fixedPoints ⇑f)
h_y : lfp f = ↑y
⊢ lfpApprox f ⊥ (succ #α).ord ≤ ↑y

Tactic:
exact lfpApprox_le_of_mem_fixedPoints f y.2 bot_le (ord <| succ #α)

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

Goal state before:
pp: case single_add
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
IH' : ∀ (e' : Ordinal.{u_1}), f e' < b
⊢ single e x + coeff b (eval b f) = single e x + f

pp: case single_add.hxb
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
IH' : ∀ (e' : Ordinal.{u_1}), f e' < b
⊢ x < b

pp: case single_add.hy
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
IH' : ∀ (e' : Ordinal.{u_1}), f e' < b
⊢ eval b f < b ^ e

Tactic:
IH IH'

Goal state after:
case single_add
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
IH' : ∀ (e' : Ordinal.{u_1}), f e' < b
⊢ single e x + f = single e x + f

case single_add.hxb
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
IH' : ∀ (e' : Ordinal.{u_1}), f e' < b
⊢ x < b

case single_add.hy
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
IH' : ∀ (e' : Ordinal.{u_1}), f e' < b
⊢ eval b f < b ^ e
Module: Mathlib.SetTheory.ZFC.Basic

Goal state before:
pp: u : ZFSet.{u_1}
⊢ (∀ (y : ZFSet.{u_1}), y ∉ u) ∨ u.Nonempty

Tactic:
← not_exists

Goal state after:
u : ZFSet.{u_1}
⊢ (¬∃ x, x ∈ u) ∨ u.Nonempty
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: case oadd
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
⊢ (match e.cmp e' with
      | Ordering.lt => e'.oadd n' a'
      | Ordering.eq => e.oadd (n + n') a'
      | Ordering.gt => e.oadd n (e'.oadd n' a')).repr =
    ω ^ e.repr * ↑↑n + (ω ^ e'.repr * ↑↑n' + a'.repr)

Tactic:
have := h₁.fst

Goal state after:
case oadd
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
⊢ (match e.cmp e' with
      | Ordering.lt => e'.oadd n' a'
      | Ordering.eq => e.oadd (n + n') a'
      | Ordering.gt => e.oadd n (e'.oadd n' a')).repr =
    ω ^ e.repr * ↑↑n + (ω ^ e'.repr * ↑↑n' + a'.repr)
Module: Mathlib.SetTheory.Ordinal.Veblen

Goal state before:
pp: o x : Ordinal.{u}
h : o < x.invVeblen₁
⊢ veblen o x = x

Tactic:
by
  simpa using notMem_of_lt_csInf' h

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

Goal state before:
pp: case inr.inl
x : Ordinal.{u}
⊢ ω ^ x ∈ range (veblen x.invVeblen₁) ↔ x.invVeblen₁ ≤ x.invVeblen₁

Tactic:
apply iff_of_true _ le_rfl
    by_cases h : invVeblen₁ x = 0
    · simp [h]
    · simp_rw [mem_range_veblen h, veblen_opow_eq_opow_iff]
      exact fun o ↦ veblen_eq_of_lt_invVeblen₁

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

Goal state before:
pp: p : ZFSet.{u} → Prop
x : ZFSet.{u}
⊢ ∀ (x : ZFSet.{u}), (∀ y ∈ x, Hereditarily p y → p ∅) → Hereditarily p x → p ∅

Tactic:
intro y IH h

Goal state after:
p : ZFSet.{u} → Prop
x y : ZFSet.{u}
IH : ∀ y_1 ∈ y, Hereditarily p y_1 → p ∅
h : Hereditarily p y
⊢ p ∅
Module: Mathlib.SetTheory.ZFC.Ordinal

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

Tactic:
· rintro (rfl | h)
    · rfl
    · exact hy.subset_of_mem h

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

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

Tactic:
by
  rw [vonNeumann]; aesop

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

Goal state before:
pp: case neg
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₁ + e₂).oadd n₂ (e₁.oadd n₁ a₁ * a₂)).NFBelow (e₁.repr + b₂)

Tactic:
have := h₁.fst

Goal state after:
case neg
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
this : e₁.NF
⊢ ((e₁ + e₂).oadd n₂ (e₁.oadd n₁ a₁ * a₂)).NFBelow (e₁.repr + b₂)
Module: Mathlib.SetTheory.ZFC.Ordinal

Goal state before:
pp: case e'_3
o : Ordinal.{u_1}
x✝ : ↑(Iio o)
⊢ ↑x✝ = (↑x✝).toPSet.rank

Tactic:
rank_toPSet

Goal state after:
case e'_3
o : Ordinal.{u_1}
x✝ : ↑(Iio o)
⊢ ↑x✝ = ↑x✝
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: case neg
e₁ : ONote
n₁ : ℕ+
a₁ e₂ : ONote
n₂ : ℕ+
a₂ : ONote
h₁ : (e₁.oadd n₁ a₁).NF
h₂ : (e₂.oadd n₂ a₂).NF
IH : ((e₁.oadd n₁ a₁).mul a₂).repr = (e₁.oadd n₁ a₁).repr * a₂.repr
ao : a₁.repr + ω ^ e₁.repr * ↑↑n₁ = ω ^ e₁.repr * ↑↑n₁
e0 : ¬e₂ = 0
⊢ (Mul.mul (e₁.oadd n₁ a₁) (e₂.oadd n₂ a₂)).repr = (ω ^ e₁.repr * ↑↑n₁ + a₁.repr) * (ω ^ e₂.repr * ↑↑n₂ + a₂.repr)

Tactic:
have := h₁.fst

Goal state after:
case neg
e₁ : ONote
n₁ : ℕ+
a₁ e₂ : ONote
n₂ : ℕ+
a₂ : ONote
h₁ : (e₁.oadd n₁ a₁).NF
h₂ : (e₂.oadd n₂ a₂).NF
IH : ((e₁.oadd n₁ a₁).mul a₂).repr = (e₁.oadd n₁ a₁).repr * a₂.repr
ao : a₁.repr + ω ^ e₁.repr * ↑↑n₁ = ω ^ e₁.repr * ↑↑n₁
e0 : ¬e₂ = 0
this : e₁.NF
⊢ (Mul.mul (e₁.oadd n₁ a₁) (e₂.oadd n₂ a₂)).repr = (ω ^ e₁.repr * ↑↑n₁ + a₁.repr) * (ω ^ e₂.repr * ↑↑n₂ + a₂.repr)
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Majorized

Goal state before:
pp: b : ℝ → ℝ
h_tendsto : Tendsto b atTop atTop
c : ℝ
⊢ Majorized (fun x ↦ c) b 0

Tactic:
intro exp

Goal state after:
b : ℝ → ℝ
h_tendsto : Tendsto b atTop atTop
c exp : ℝ
⊢ exp > 0 → (fun x ↦ c) =o[atTop] (b ^ exp)
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Majorized

Goal state before:
pp: f g b : ℝ → ℝ
f_exp g_exp : ℝ
hf : ∀ exp' > f_exp, f =o[atTop] (b ^ exp')
hg : ∀ exp' > g_exp, g =o[atTop] (b ^ exp')
h_pos : ∀ᶠ (t : ℝ) in atTop, 0 < b t
⊢ ∀ exp' > f_exp + g_exp, (f * g) =o[atTop] (b ^ exp')

Tactic:
intro exp

Goal state after:
f g b : ℝ → ℝ
f_exp g_exp : ℝ
hf : ∀ exp' > f_exp, f =o[atTop] (b ^ exp')
hg : ∀ exp' > g_exp, g =o[atTop] (b ^ exp')
h_pos : ∀ᶠ (t : ℝ) in atTop, 0 < b t
exp : ℝ
⊢ exp > f_exp + g_exp → (f * g) =o[atTop] (b ^ exp)
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Majorized

Goal state before:
pp: f g b : ℝ → ℝ
f_exp g_exp : ℝ
h_pos : ∀ᶠ (t : ℝ) in atTop, 0 < b t
exp : ℝ
h_exp : exp > f_exp + g_exp
ε : ℝ := (exp - f_exp - g_exp) / 2
hg : g =o[atTop] (b ^ (g_exp + ε))
hf : f =o[atTop] (b ^ (f_exp + ε))
t : ℝ
hx : 0 < b t
⊢ (fun t ↦ b t ^ (f_exp + ε) * b t ^ (g_exp + ε)) t = (b ^ exp) t

Tactic:
simp only [Pi.pow_apply]

Goal state after:
f g b : ℝ → ℝ
f_exp g_exp : ℝ
h_pos : ∀ᶠ (t : ℝ) in atTop, 0 < b t
exp : ℝ
h_exp : exp > f_exp + g_exp
ε : ℝ := (exp - f_exp - g_exp) / 2
hg : g =o[atTop] (b ^ (g_exp + ε))
hf : f =o[atTop] (b ^ (f_exp + ε))
t : ℝ
hx : 0 < b t
⊢ b t ^ (f_exp + ε) * b t ^ (g_exp + ε) = b t ^ exp
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Majorized

Goal state before:
pp: f g basis_hd : ℝ → ℝ
exp : ℝ
hf : Majorized f basis_hd exp
hg : g =O[atTop] fun x ↦ 1
⊢ Majorized (f * g) basis_hd exp

Tactic:
intro exp

Goal state after:
f g basis_hd : ℝ → ℝ
exp✝ : ℝ
hf : Majorized f basis_hd exp✝
hg : g =O[atTop] fun x ↦ 1
exp : ℝ
⊢ exp > exp✝ → (f * g) =o[atTop] (basis_hd ^ exp)
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
F : β → Option (α × γ × β)
op : γ → Stream'.Seq α → Stream'.Seq α
h : FriendlyOperationClass op
T : (β →ᵤ Stream'.Seq α) → β →ᵤ Stream'.Seq α :=
  fun f b ↦
    match F b with
    | none => nil
    | some (a, c, b') => Seq.cons a (op c (f b'))
f g : β →ᵤ Stream'.Seq α
b : β
a : α
c : γ
b' : β
⊢ ∃ C, ∀ (a b : Stream'.Seq α), dist a b ≤ C

Tactic:
rw [← Metric.boundedSpace_iff]

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 : β
a : α
c : γ
b' : β
⊢ BoundedSpace (Stream'.Seq α)
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs

Goal state before:
pp: basis_hd : ℝ → ℝ
basis_tl : Basis
γ : Type u_1
op : γ → Multiseries basis_hd basis_tl → Multiseries basis_hd basis_tl
h : ∀ (c : γ), FriendlyOperation (op c)
⊢ FriendlyOperationClass op

Tactic:
by
  suffices Seq.FriendlyOperationClass op by constructor
  exact ⟨h⟩

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

Goal state before:
pp: α : Type u_1
op : Stream'.Seq α → Stream'.Seq α
hd : α
h : FriendlyOperation op
⊢ FriendlyOperation fun s ↦ (op (Seq.cons hd s)).tail

Tactic:
simp_rw [friendlyOperation_iff_dist_le_dist] at h ⊢
  intro x y
  specialize h (.cons hd x) (.cons hd y)
  exact dist_const_tail_cons_tail_le h

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

Goal state before:
pp: hd f : ℝ → ℝ
tl : Basis
h_basis : WellFormedBasis (hd :: tl)
hf : f ∈ tl
r : ℝ
⊢ Majorized (f ^ r) hd 0

Tactic:
intro exp

Goal state after:
hd f : ℝ → ℝ
tl : Basis
h_basis : WellFormedBasis (hd :: tl)
hf : f ∈ tl
r exp : ℝ
⊢ exp > 0 → (f ^ r) =o[atTop] (hd ^ exp)