mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.WittVector.InitTail

Goal state before:
pp: case refine_3
p : ℕ
P : ℕ → Prop
hp : Fact (Nat.Prime p)
this : IsPoly p fun {R} [CommRing R] x ↦ select P x + select (fun i ↦ ¬P i) x
R : Type u_1
R._inst : CommRing R
x : 𝕎 R
n : ℕ
⊢ (ghostComponent n) (select P x) + (ghostComponent n) (select (fun i ↦ ¬P i) x) = (ghostComponent n) x

Tactic:
suffices
    (bind₁ (selectPoly P)) (wittPolynomial p ℤ n) +
        (bind₁ (selectPoly fun i => ¬P i)) (wittPolynomial p ℤ n) =
      wittPolynomial p ℤ n by
    apply_fun aeval x.coeff at this
    simpa only [map_add, aeval_bind₁, ← coeff_select]

Goal state after:
case refine_3
p : ℕ
P : ℕ → Prop
hp : Fact (Nat.Prime p)
this : IsPoly p fun {R} [CommRing R] x ↦ select P x + select (fun i ↦ ¬P i) x
R : Type u_1
R._inst : CommRing R
x : 𝕎 R
n : ℕ
⊢ (bind₁ (selectPoly P)) (wittPolynomial p ℤ n) + (bind₁ (selectPoly fun i ↦ ¬P i)) (wittPolynomial p ℤ n) =
    wittPolynomial p ℤ n
Module: Mathlib.RingTheory.WittVector.Truncated

Goal state before:
pp: p n : ℕ
R : Type u_1
inst✝² : CommRing R
inst✝¹ : Fact (Nat.Prime p)
S : Type u_2
inst✝ : Semiring S
f : (k : ℕ) → S →+* TruncatedWittVector p k R
f_compat : ∀ (k₁ k₂ : ℕ) (hk : k₁ ≤ k₂), (TruncatedWittVector.truncate hk).comp (f k₂) = f k₁
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
refine { toFun := liftFun f
           map_zero' := ?_
           map_one' := ?_
           map_add' := ?_
           map_mul' := ?_ } <;>
  ( intros
    rw [← sub_eq_zero, ← Ideal.mem_bot, ← iInf_ker_truncate, Ideal.mem_iInf]
    simp [RingHom.mem_ker, f_compat])

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : CommRing k
inst✝¹ : CharP k p
inst✝ : PerfectRing k p
x : 𝕎 k
⊢ ↑p ∣ x ↔ x.coeff 0 = 0

Tactic:
dvd_def,

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : CommRing k
inst✝¹ : CharP k p
inst✝ : PerfectRing k p
x : 𝕎 k
⊢ (∃ c, x = ↑p * c) ↔ x.coeff 0 = 0
Module: Mathlib.RingTheory.WittVector.Complete

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : CommRing k
inst✝¹ : CharP k p
inst✝ : PerfectRing k p
x : 𝕎 k
n : ℕ
⊢ ↑p ^ n ∣ x ↔ ∀ m < n, x.coeff m = 0

Tactic:
dvd_def,

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : CommRing k
inst✝¹ : CharP k p
inst✝ : PerfectRing k p
x : 𝕎 k
n : ℕ
⊢ (∃ c, x = ↑p ^ n * c) ↔ ∀ m < n, x.coeff m = 0
Module: Mathlib.RingTheory.Polynomial.Hermite.Basic

Goal state before:
pp: n k : ℕ
hermite_explicit : ℕ → ℕ → ℤ := fun n k ↦ (-1) ^ n * ↑(2 * n - 1)‼ * ↑((2 * n + k).choose k)
hermite_explicit_recur :
  ∀ (n k : ℕ), hermite_explicit (n + 1) (k + 1) = hermite_explicit (n + 1) k - (↑k + 2) * hermite_explicit n (k + 2)
⊢ (hermite (2 * (n + 1) + (k + 1))).coeff (k + 1) = hermite_explicit (n + 1) (k + 1)

Tactic:
rw [← add_assoc, coeff_hermite_succ_succ, hermite_explicit_recur]

Goal state after:
n k : ℕ
hermite_explicit : ℕ → ℕ → ℤ := fun n k ↦ (-1) ^ n * ↑(2 * n - 1)‼ * ↑((2 * n + k).choose k)
hermite_explicit_recur :
  ∀ (n k : ℕ), hermite_explicit (n + 1) (k + 1) = hermite_explicit (n + 1) k - (↑k + 2) * hermite_explicit n (k + 2)
⊢ (hermite (2 * (n + 1) + k)).coeff k - (↑k + 2) * (hermite (2 * (n + 1) + k)).coeff (k + 2) =
    hermite_explicit (n + 1) k - (↑k + 2) * hermite_explicit n (k + 2)
Module: Mathlib.RingTheory.Polynomial.ShiftedLegendre

Goal state before:
pp: case e_a.a
n m : ℕ
hm : m ∈ range (n + 1)
⊢ (-X ^ 2) ^ m * X ^ (n - m) * ↑(n.choose m) = n.choose m • (-1) ^ m * X ^ (n + m)

Tactic:
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]

Goal state after:
case e_a.a.h
n m : ℕ
hm : m ∈ range (n + 1)
⊢ m ≤ n
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
⊢ 0 ∈ I

Tactic:
zero_mem

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

Goal state before:
pp: case inr
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 : ((map (Ideal.Quotient.mk I)) g).order.toNat ≤ i
⊢ 0 ∈ I ^ (k + 1)

Tactic:
zero_mem

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

Goal state before:
pp: case refine_2
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
this : X ^ n * ↑⋯.unit⁻¹ - ↑r * ↑⋯.unit⁻¹ = g
⊢ X ^ n * ↑⋯.unit⁻¹ - ↑r * ↑⋯.unit⁻¹ = (↑Polynomial.X ^ n - ↑r) * ↑⋯.unit⁻¹

Tactic:
Polynomial.coe_X,

Goal state after:
case refine_2
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
this : X ^ n * ↑⋯.unit⁻¹ - ↑r * ↑⋯.unit⁻¹ = g
⊢ X ^ n * ↑⋯.unit⁻¹ - ↑r * ↑⋯.unit⁻¹ = (X ^ n - ↑r) * ↑⋯.unit⁻¹
Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation

Goal state before:
pp: case eq_mul_add
A : Type u_1
inst✝¹ : CommRing A
inst✝ : IsLocalRing A
g : A⟦X⟧
f : A[X]
h : A⟦X⟧
H : g.IsWeierstrassFactorization f h
n : ℕ := ((map (IsLocalRing.residue A)) g).order.toNat
hn : n = ((map (IsLocalRing.residue A)) g).order.toNat
⊢ X ^ n = ↑f + (↑Polynomial.X ^ n - ↑f)

Tactic:
Polynomial.coe_X,

Goal state after:
case eq_mul_add
A : Type u_1
inst✝¹ : CommRing A
inst✝ : IsLocalRing A
g : A⟦X⟧
f : A[X]
h : A⟦X⟧
H : g.IsWeierstrassFactorization f h
n : ℕ := ((map (IsLocalRing.residue A)) g).order.toNat
hn : n = ((map (IsLocalRing.residue A)) g).order.toNat
⊢ X ^ n = ↑f + (X ^ n - ↑f)
Module: Mathlib.RingTheory.SimpleModule.Isotypic

Goal state before:
pp: R : Type u_2
M : Type u
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
c : Submodule R M
hc : c ∈ isotypicComponents R M
s : Set (Submodule R M) := isotypicComponents R M \ {c}
ne : ¬c ⊓ sSup s = ⊥
⊢ IsSemisimpleModule R ↥c

Tactic:
obtain ⟨S, _, rfl⟩ := hc

Goal state after:
R : Type u_2
M : Type u
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
S : Submodule R M
left✝ : IsSimpleModule R ↥S
s : Set (Submodule R M) := isotypicComponents R M \ {isotypicComponent R M ↥S}
ne : ¬isotypicComponent R M ↥S ⊓ sSup s = ⊥
⊢ IsSemisimpleModule R ↥(isotypicComponent R M ↥S)
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 ≤ Ideal.comap (Ideal.Quotient.mk J) v.supp

Tactic:
← 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.WittVector.Isocrystal

Goal state before:
pp: 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
⊢ ∃ m, Nonempty (StandardOneDimIsocrystal p k m ≃ᶠⁱ[p, k] V)

Tactic:
have : Nontrivial V := Module.nontrivial_of_finrank_eq_succ h_dim

Goal state after:
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
⊢ ∃ m, Nonempty (StandardOneDimIsocrystal p k m ≃ᶠⁱ[p, k] V)
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}.ncard

Tactic:
rw [Set.ncard_def, ← ENat.natCast_le_natCast, ENat.natCast_toNat (by simpa)]
  exact count_le_setENCard n

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

Goal state before:
pp: C : Ordinal.{u_2} → Sort u_1
b : Ordinal.{u_2}
H0 : C 0
H : (o : Ordinal.{u_2}) → o ≠ 0 → C (o % b ^ log b o) → C o
⊢ CNF.rec b H0 H 0 = H0

Tactic:
by
  rw [CNF.rec, dif_pos rfl]

Goal state after:
Module: Mathlib.SetTheory.Lists

Goal state before:
pp: case C1.antisymm.antisymm.left
α : 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₂✝¹ : Lists' α true
l₂ : l₁.Subset l₂✝¹
a✝¹ : l₂✝¹.Subset l₁
h₁ : of' l₁ ~ ⟨true, l₂✝¹⟩
l₂✝ : Lists' α true
l₃ : l₂✝¹.Subset l₂✝
a✝ : l₂✝.Subset l₂✝¹
h₂ : ⟨true, l₂✝¹⟩ ~ ⟨true, l₂✝⟩
hl₁ : l₁ ⊆ l₂✝¹
hr₁ : l₂✝¹ ⊆ l₁
hl₂ : l₂✝¹ ⊆ l₂✝
hr₂ : l₂✝ ⊆ l₂✝¹
a₁ : Lists α
m₁ : a₁ ∈ l₁.toList
⊢ a₁ ∈ l₂✝

Tactic:
rcases Lists'.mem_of_subset' hl₁ m₁ with ⟨a₂, m₂, e₁₂⟩

Goal state after:
case C1.antisymm.antisymm.left
α : 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₂✝¹ : Lists' α true
l₂ : l₁.Subset l₂✝¹
a✝¹ : l₂✝¹.Subset l₁
h₁ : of' l₁ ~ ⟨true, l₂✝¹⟩
l₂✝ : Lists' α true
l₃ : l₂✝¹.Subset l₂✝
a✝ : l₂✝.Subset l₂✝¹
h₂ : ⟨true, l₂✝¹⟩ ~ ⟨true, l₂✝⟩
hl₁ : l₁ ⊆ l₂✝¹
hr₁ : l₂✝¹ ⊆ l₁
hl₂ : l₂✝¹ ⊆ l₂✝
hr₂ : l₂✝ ⊆ l₂✝¹
a₁ : Lists α
m₁ : a₁ ∈ l₁.toList
a₂ : Lists α
m₂ : a₂ ∈ l₂✝¹.toList
e₁₂ : a₁ ~ a₂
⊢ a₁ ∈ l₂✝
Module: Mathlib.SetTheory.Ordinal.CantorNormalForm

Goal state before:
pp: case single_add
b : Ordinal.{u_1}
f₂ : Ordinal.{u_1} →₀ Ordinal.{u_1}
e₁ x : Ordinal.{u_1}
f₁ : Ordinal.{u_1} →₀ Ordinal.{u_1}
hf₁ : ∀ c ∈ f₁.support, c < e₁
hx : x ≠ 0
IH : (∀ e₁ ∈ f₁.support, ∀ e₂ ∈ f₂.support, e₂ ≤ e₁) → eval b (f₁ + f₂) = eval b f₁ + eval b f₂
h : ∀ e₁_1 ∈ (single e₁ x + f₁).support, ∀ e₂ ∈ f₂.support, e₂ ≤ e₁_1
⊢ eval b (single e₁ x + (f₁ + f₂)) = eval b (single e₁ x + f₁) + eval b f₂

Tactic:
eval_single_add,

Goal state after:
case single_add
b : Ordinal.{u_1}
f₂ : Ordinal.{u_1} →₀ Ordinal.{u_1}
e₁ x : Ordinal.{u_1}
f₁ : Ordinal.{u_1} →₀ Ordinal.{u_1}
hf₁ : ∀ c ∈ f₁.support, c < e₁
hx : x ≠ 0
IH : (∀ e₁ ∈ f₁.support, ∀ e₂ ∈ f₂.support, e₂ ≤ e₁) → eval b (f₁ + f₂) = eval b f₁ + eval b f₂
h : ∀ e₁_1 ∈ (single e₁ x + f₁).support, ∀ e₂ ∈ f₂.support, e₂ ≤ e₁_1
⊢ b ^ e₁ * x + eval b (f₁ + f₂) = eval b (single e₁ x + f₁) + eval b f₂

case single_add.h
b : Ordinal.{u_1}
f₂ : Ordinal.{u_1} →₀ Ordinal.{u_1}
e₁ x : Ordinal.{u_1}
f₁ : Ordinal.{u_1} →₀ Ordinal.{u_1}
hf₁ : ∀ c ∈ f₁.support, c < e₁
hx : x ≠ 0
IH : (∀ e₁ ∈ f₁.support, ∀ e₂ ∈ f₂.support, e₂ ≤ e₁) → eval b (f₁ + f₂) = eval b f₁ + eval b f₂
h : ∀ e₁_1 ∈ (single e₁ x + f₁).support, ∀ e₂ ∈ f₂.support, e₂ ≤ e₁_1
⊢ ∀ e' ∈ (f₁ + f₂).support, e' ≤ e₁
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: e₁ : ONote
n₁ : ℕ+
a₁ e₂ : ONote
n₂ : ℕ+
a₂ : ONote
h : (e₁.oadd n₁ a₁).cmp (e₂.oadd n₂ a₂) = Ordering.eq
⊢ e₁.oadd n₁ a₁ = e₂.oadd n₂ a₂

Tactic:
revert h; simp only [cmp]
    cases h₁ : cmp e₁ e₂ <;> intro h <;> try cases h
    obtain rfl := eq_of_cmp_eq h₁
    revert h; cases h₂ : _root_.cmp (n₁ : ℕ) n₂ <;> intro h <;> try cases h
    obtain rfl := eq_of_cmp_eq h
    rw [_root_.cmp, cmpUsing_eq_eq, not_lt, not_lt, ← le_antisymm_iff] at h₂
    obtain rfl := Subtype.ext h₂
    simp

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

Goal state before:
pp: s : Set Ordinal.{u}
⊢ (∀ {ι : Type u}, Nonempty ι → ∀ (f : ι → Ordinal.{u}), (∀ (i : ι), f i ∈ s) → ⨆ i, f i ∈ s) ↔
    ∀ {o : Ordinal.{u}},
      o ≠ 0 →
        ∀ (f : (a : Ordinal.{u}) → a < o → Ordinal.{u}), (∀ (i : Ordinal.{u}) (hi : i < o), f i hi ∈ s) → o.bsup f ∈ s

Tactic:
refine ⟨fun H o ho f hf => H (nonempty_toType_iff.2 ho) _ ?_, fun H ι hι f hf => ?_⟩

Goal state after:
case refine_1
s : Set Ordinal.{u}
H : ∀ {ι : Type u}, Nonempty ι → ∀ (f : ι → Ordinal.{u}), (∀ (i : ι), f i ∈ s) → ⨆ i, f i ∈ s
o : Ordinal.{u}
ho : o ≠ 0
f : (a : Ordinal.{u}) → a < o → Ordinal.{u}
hf : ∀ (i : Ordinal.{u}) (hi : i < o), f i hi ∈ s
⊢ ∀ (i : o.ToType), o.familyOfBFamily f i ∈ s

case refine_2
s : Set Ordinal.{u}
H :
  ∀ {o : Ordinal.{u}},
    o ≠ 0 →
      ∀ (f : (a : Ordinal.{u}) → a < o → Ordinal.{u}), (∀ (i : Ordinal.{u}) (hi : i < o), f i hi ∈ s) → o.bsup f ∈ s
ι : Type u
hι : Nonempty ι
f : ι → Ordinal.{u}
hf : ∀ (i : ι), f i ∈ s
⊢ ⨆ i, f i ∈ s
Module: Mathlib.SetTheory.Ordinal.Topology

Goal state before:
pp: case refine_2
s : Set Ordinal.{u}
H :
  ∀ {o : Ordinal.{u}},
    o ≠ 0 →
      ∀ (f : (a : Ordinal.{u}) → a < o → Ordinal.{u}), (∀ (i : Ordinal.{u}) (hi : i < o), f i hi ∈ s) → o.bsup f ∈ s
ι : Type u
hι : Nonempty ι
f : ι → Ordinal.{u}
hf : ∀ (i : ι), f i ∈ s
⊢ (type WellOrderingRel).bsup (bfamilyOfFamily fun i ↦ f i) ∈ s

Tactic:
apply H (type_ne_zero_iff_nonempty.2 hι)

Goal state after:
case refine_2
s : Set Ordinal.{u}
H :
  ∀ {o : Ordinal.{u}},
    o ≠ 0 →
      ∀ (f : (a : Ordinal.{u}) → a < o → Ordinal.{u}), (∀ (i : Ordinal.{u}) (hi : i < o), f i hi ∈ s) → o.bsup f ∈ s
ι : Type u
hι : Nonempty ι
f : ι → Ordinal.{u}
hf : ∀ (i : ι), f i ∈ s
⊢ ∀ (i : Ordinal.{u}) (hi : i < type WellOrderingRel), bfamilyOfFamily (fun i ↦ f i) i hi ∈ s
Module: Mathlib.SetTheory.ZFC.Basic

Goal state before:
pp: x : ZFSet.{u}
⊢ x = ∅ ↔ ∀ (y : ZFSet.{u}), y ∉ x

Tactic:
simp [ZFSet.ext_iff]

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

Goal state before:
pp: f : Ordinal.{u} → Ordinal.{u}
o a : Ordinal.{u}
hf : IsNormal f
⊢ veblenWith f o a ∈ range f

Tactic:
obtain rfl | h := eq_zero_or_pos o

Goal state after:
case inl
f : Ordinal.{u} → Ordinal.{u}
a : Ordinal.{u}
hf : IsNormal f
⊢ veblenWith f 0 a ∈ range f

case inr
f : Ordinal.{u} → Ordinal.{u}
o a : Ordinal.{u}
hf : IsNormal f
h : 0 < o
⊢ veblenWith f o a ∈ range f
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: case oadd.eq
b : Ordinal.{0}
e : ONote
n : ℕ+
a o : ONote
h₁ : (e.oadd n a).NFBelow b
h₂ : o.NFBelow b
e' : ONote
n' : ℕ+
a' : ONote
h' : (e'.oadd n' a').NFBelow b
this : (e.cmp e').Compares e e'
h : e.cmp e' = Ordering.eq
⊢ (e.oadd (n + n') a').NFBelow b

Tactic:
simp only [h] at this

Goal state after:
case oadd.eq
b : Ordinal.{0}
e : ONote
n : ℕ+
a o : ONote
h₁ : (e.oadd n a).NFBelow b
h₂ : o.NFBelow b
e' : ONote
n' : ℕ+
a' : ONote
h' : (e'.oadd n' a').NFBelow b
h : e.cmp e' = Ordering.eq
this : Ordering.eq.Compares e e'
⊢ (e.oadd (n + n') a').NFBelow b
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: case oadd.gt
b : Ordinal.{0}
e : ONote
n : ℕ+
a o : ONote
h₁ : (e.oadd n a).NFBelow b
h₂ : o.NFBelow b
e' : ONote
n' : ℕ+
a' : ONote
h' : (e'.oadd n' a').NFBelow b
this : (e.cmp e').Compares e e'
h : e.cmp e' = Ordering.gt
⊢ (e.oadd n (e'.oadd n' a')).NFBelow b

Tactic:
simp only [h] at this

Goal state after:
case oadd.gt
b : Ordinal.{0}
e : ONote
n : ℕ+
a o : ONote
h₁ : (e.oadd n a).NFBelow b
h₂ : o.NFBelow b
e' : ONote
n' : ℕ+
a' : ONote
h' : (e'.oadd n' a').NFBelow b
h : e.cmp e' = Ordering.gt
this : Ordering.gt.Compares e e'
⊢ (e.oadd n (e'.oadd n' a')).NFBelow b
Module: Mathlib.SetTheory.Ordinal.Veblen

Goal state before:
pp: f : Ordinal.{u} → Ordinal.{u}
o a : Ordinal.{u}
hf : IsNormal f
hp : 0 < f 0
H : ∀ (b : Ordinal.{u}), 0 < veblenWith f 0 b
⊢ 0 < veblenWith f o a

Tactic:
obtain rfl | h := eq_zero_or_pos o

Goal state after:
case inl
f : Ordinal.{u} → Ordinal.{u}
a : Ordinal.{u}
hf : IsNormal f
hp : 0 < f 0
H : ∀ (b : Ordinal.{u}), 0 < veblenWith f 0 b
⊢ 0 < veblenWith f 0 a

case inr
f : Ordinal.{u} → Ordinal.{u}
o a : Ordinal.{u}
hf : IsNormal f
hp : 0 < f 0
H : ∀ (b : Ordinal.{u}), 0 < veblenWith f 0 b
h : 0 < o
⊢ 0 < veblenWith f o a
Module: Mathlib.SetTheory.ZFC.Rank

Goal state before:
pp: case a
x y : PSet.{u_1}
⊢ max (succ x.rank) y.rank ≤ (insert x y).rank

Tactic:
apply max_le

Goal state after:
case a.h₁
x y : PSet.{u_1}
⊢ succ x.rank ≤ (insert x y).rank

case h₂
x y : PSet.{u_1}
⊢ y.rank ≤ (insert x y).rank
Module: Mathlib.SetTheory.ZFC.Rank

Goal state before:
pp: case a
x y : ZFSet.{u_1}
⊢ ∀ ⦃y_1 : ZFSet.{u_1}⦄, y_1 ∈ x ∨ y_1 ∈ y → y_1.rank < max x.rank y.rank

Tactic:
lt_max_iff

Goal state after:
case a
x y : ZFSet.{u_1}
⊢ ∀ ⦃y_1 : ZFSet.{u_1}⦄, y_1 ∈ x ∨ y_1 ∈ y → y_1.rank < x.rank ∨ y_1.rank < y.rank
Module: Mathlib.SetTheory.ZFC.Rank

Goal state before:
pp: case a
x y : ZFSet.{u_1}
⊢ max x.rank y.rank ≤ (x ∪ y).rank

Tactic:
apply max_le

Goal state after:
case a.h₁
x y : ZFSet.{u_1}
⊢ x.rank ≤ (x ∪ y).rank

case h₂
x y : ZFSet.{u_1}
⊢ y.rank ≤ (x ∪ y).rank
Module: Mathlib.SetTheory.ZFC.Class

Goal state before:
pp: case mp
x : Class.{u_1}
y : ZFSet.{u_1}
⊢ (⋃₀ x) y → ∃ z, x z ∧ y ∈ z

Tactic:
rintro ⟨-, ⟨z, rfl, hxz⟩, hyz⟩
    exact ⟨z, hxz, hyz⟩

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

Goal state before:
pp: x : ZFSet.{u}
H : ∀ y ∈ x, y.IsTransitive
y : ZFSet.{u}
hy : y ∈ ⋃₀ x
z : ZFSet.{u}
hz : z ∈ y
⊢ z ∈ ⋃₀ x

Tactic:
rcases mem_sUnion.1 hy with ⟨w, hw, hw'⟩
  exact mem_sUnion_of_mem ((H w hw).mem_trans hz hw') hw

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

Goal state before:
pp: o o' : ONote
m : ℕ
inst✝ : o.NF
h : o.split = (o', m)
a : ONote
n : ℕ
e : o.split' = (a, n)
s₁ : a.NF
s₂ : o.repr = ω * a.repr + ↑n
⊢ o'.NF ∧ o.repr = o'.repr + ↑m

Tactic:
split_eq_scale_split' e

Goal state after:
o o' : ONote
m : ℕ
inst✝ : o.NF
a : ONote
n : ℕ
h : (scale 1 a, n) = (o', m)
e : o.split' = (a, n)
s₁ : a.NF
s₂ : o.repr = ω * a.repr + ↑n
⊢ o'.NF ∧ o.repr = o'.repr + ↑m
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: o o' : ONote
m : ℕ
inst✝ : o.NF
h : o.split = (o', m)
a : ONote
n : ℕ
e : o.split' = (a, n)
⊢ ω ∣ o'.repr

Tactic:
split_eq_scale_split' e

Goal state after:
o o' : ONote
m : ℕ
inst✝ : o.NF
a : ONote
n : ℕ
h : (scale 1 a, n) = (o', m)
e : o.split' = (a, n)
⊢ ω ∣ o'.repr
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: case hbd
e a : ONote
Ne : e.NF
Na : a.NF
e0 : e.repr ≠ 0
n : ℕ+
h✝ : a.repr < ω ^ e.repr
No : (e.oadd n a).NF
this✝ : ω ^ e.repr ≤ ω ^ e.repr * ↑↑n + a.repr
b : Ordinal.{0}
l : b < ω
this : ω ^ e.repr * ↑↑n + a.repr < ω ^ succ e.repr
h : ω ≤ e.repr
⊢ e.repr * succ b + 1 ≤ e.repr * ω

Tactic:
· exact succ_le_iff.2 <| by gcongr; exact isSuccLimit_omega0.succ_lt l

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

Goal state before:
pp: case inr
e a : ONote
Ne : e.NF
Na : a.NF
e0 : e.repr ≠ 0
n : ℕ+
h✝ : a.repr < ω ^ e.repr
No : (e.oadd n a).NF
this✝ : ω ^ e.repr ≤ ω ^ e.repr * ↑↑n + a.repr
b : Ordinal.{0}
l : b < ω
this : ω ^ e.repr * ↑↑n + a.repr < ω ^ succ e.repr
h : e.repr < ω
⊢ ω ^ (succ e.repr * b) ≤ ω ^ (e.repr * ω)

Tactic:
show _ * _ < _ from isPrincipal_mul_omega0 (isSuccLimit_omega0.succ_lt h) l

Goal state after:
case inr
e a : ONote
Ne : e.NF
Na : a.NF
e0 : e.repr ≠ 0
n : ℕ+
h✝ : a.repr < ω ^ e.repr
No : (e.oadd n a).NF
this✝ : ω ^ e.repr ≤ ω ^ e.repr * ↑↑n + a.repr
b : Ordinal.{0}
l : b < ω
this : ω ^ e.repr * ↑↑n + a.repr < ω ^ succ e.repr
h : e.repr < ω
⊢ ω ^ ω ≤ ω ^ (e.repr * ω)

case hc
e a : ONote
Ne : e.NF
Na : a.NF
e0 : e.repr ≠ 0
n : ℕ+
h✝ : a.repr < ω ^ e.repr
No : (e.oadd n a).NF
this✝ : ω ^ e.repr ≤ ω ^ e.repr * ↑↑n + a.repr
b : Ordinal.{0}
l : b < ω
this : ω ^ e.repr * ↑↑n + a.repr < ω ^ succ e.repr
h : e.repr < ω
⊢ 0 < ω
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Majorized

Goal state before:
pp: f : ℝ → ℝ
exp : ℝ
h : Tendsto f atTop atTop
exp' : ℝ
h_exp : exp' > exp
this : (fun t ↦ f t ^ exp / f t ^ exp') =ᶠ[atTop] fun t ↦ f t ^ (exp - exp')
⊢ Tendsto ((fun t ↦ t ^ (-(exp' - exp))) ∘ f) atTop (𝓝 0)

Tactic:
exact (tendsto_rpow_neg_atTop (by linarith)).comp h

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

Goal state before:
pp: case hbc
a0 a' : ONote
N0 : a0.NF
Na' : a'.NF
m : ℕ
d : ω ∣ a'.repr
e0✝ : a0.repr ≠ 0
h : a'.repr + ↑m < ω ^ a0.repr
n : ℕ+
No : (a0.oadd n a').NF
k : ℕ
R' : Ordinal.{0} := (opowAux 0 a0 (a0.oadd n a' * ↑m) (k + 1) m).repr
R : Ordinal.{0} := (opowAux 0 a0 (a0.oadd n a' * ↑m) k m).repr
ω0 : Ordinal.{0} := ω ^ a0.repr
α' : Ordinal.{0} := ω0 * ↑↑n + a'.repr
IH : (k ≠ 0 → R < ω0 ^ succ ↑k) ∧ ω0 ^ ↑k * α' + R = (α' + ↑m) ^ succ ↑k
RR : R' = ω0 ^ ↑k * (α' * ↑m) + R
α0 : 0 < α'
ω00 : 0 < ω0 ^ ↑k
Rl : R < ω ^ (a0.repr * succ ↑k)
x✝ : k + 1 ≠ 0
e0 : 0 < a0.repr
rr0 : 0 < a0.repr + a0.repr
⊢ α' * ↑m < ω ^ a0.repr * ω ^ a0.repr

Tactic:
← Ordinal.opow_add

Goal state after:
case hbc
a0 a' : ONote
N0 : a0.NF
Na' : a'.NF
m : ℕ
d : ω ∣ a'.repr
e0✝ : a0.repr ≠ 0
h : a'.repr + ↑m < ω ^ a0.repr
n : ℕ+
No : (a0.oadd n a').NF
k : ℕ
R' : Ordinal.{0} := (opowAux 0 a0 (a0.oadd n a' * ↑m) (k + 1) m).repr
R : Ordinal.{0} := (opowAux 0 a0 (a0.oadd n a' * ↑m) k m).repr
ω0 : Ordinal.{0} := ω ^ a0.repr
α' : Ordinal.{0} := ω0 * ↑↑n + a'.repr
IH : (k ≠ 0 → R < ω0 ^ succ ↑k) ∧ ω0 ^ ↑k * α' + R = (α' + ↑m) ^ succ ↑k
RR : R' = ω0 ^ ↑k * (α' * ↑m) + R
α0 : 0 < α'
ω00 : 0 < ω0 ^ ↑k
Rl : R < ω ^ (a0.repr * succ ↑k)
x✝ : k + 1 ≠ 0
e0 : 0 < a0.repr
rr0 : 0 < a0.repr + a0.repr
⊢ α' * ↑m < ω ^ (a0.repr + a0.repr)
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
F : β → Option (α × γ × β)
op : γ → Stream'.Seq α → Stream'.Seq α
inst✝ : FriendlyOperationClass op
b : β
h : F b = none
⊢ gcorec F op b = nil

Tactic:
by
  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:
by
  have := (FriendlyOperation.exists_fixed_point F op).choose_spec b
  simpa [h] using! this

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

Goal state before:
pp: basis : Basis
c : ℝ
⊢ (const [] c).toFun = fun x ↦ c

Tactic:
simp [const, ofReal, toReal]

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

Goal state before:
pp: basis_hd : ℝ → ℝ
basis_tl : Basis
ms : Multiseries basis_hd basis_tl
exp : ℝ
coef : MultiseriesExpansion basis_tl
tl : Multiseries basis_hd basis_tl
h : ms.destruct = some (exp, coef, tl)
⊢ Seq.destruct ms = some ((exp, coef), tl)

Tactic:
destruct_eq_destruct_map,

Goal state after:
basis_hd : ℝ → ℝ
basis_tl : Basis
ms : Multiseries basis_hd basis_tl
exp : ℝ
coef : MultiseriesExpansion basis_tl
tl : Multiseries basis_hd basis_tl
h : ms.destruct = some (exp, coef, tl)
⊢ Option.map
      (fun x ↦
        match x with
        | (exp, coef, tl) => ((exp, coef), tl))
      ms.destruct =
    some ((exp, coef), tl)

basis_hd : ℝ → ℝ
basis_tl : Basis
ms : Multiseries basis_hd basis_tl
exp : ℝ
coef : MultiseriesExpansion basis_tl
tl : Multiseries basis_hd basis_tl
h : ms.destruct = some (exp, coef, tl)
⊢ ℝ → ℝ