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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
R : Type u_1
inst✝² : CommRing R
inst✝¹ : CharP R p
inst✝ : PerfectRing R p
x : 𝕎 R
n i : ℕ
hi : i < n + 1
g : ℕ → R := fun x ↦ 0
⊢ ∀ x_1 ∈ Finset.Iic n \ {i},
    ((teichmuller p) (((_root_.frobeniusEquiv R p).symm ^ x_1) (x.coeff x_1)) * ↑p ^ x_1).coeff i = g x_1

Tactic:
intro b hb

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
R : Type u_1
inst✝² : CommRing R
inst✝¹ : CharP R p
inst✝ : PerfectRing R p
x : 𝕎 R
n i : ℕ
hi : i < n + 1
g : ℕ → R := fun x ↦ 0
b : ℕ
hb : b ∈ Finset.Iic n \ {i}
⊢ ((teichmuller p) (((_root_.frobeniusEquiv R p).symm ^ b) (x.coeff b)) * ↑p ^ b).coeff i = g b
Module: Mathlib.RingTheory.Polynomial.HilbertPoly

Goal state before:
pp: case h.right
F : Type u_1
inst✝¹ : Field F
inst✝ : CharZero F
p : F[X]
d : ℕ
⊢ ∀ (y : F[X]),
    (fun h ↦ ∃ N, ∀ n > N, (PowerSeries.coeff n) (↑p * ↑(invOneSubPow F d)) = eval (↑n) h) y → y = p.hilbertPoly d

Tactic:
rintro h ⟨N, hhN⟩
    apply eq_of_infinite_eval_eq h (hilbertPoly p d)
    apply ((Set.Ioi_infinite (max N p.natDegree)).image cast_injective.injOn).mono
    rintro x ⟨n, hn, rfl⟩
    simp only [Set.mem_Ioi, sup_lt_iff, Set.mem_ofPred_eq] at hn ⊢
    rw [← coeff_mul_invOneSubPow_eq_hilbertPoly_eval d hn.2, hhN n hn.1]

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

Goal state before:
pp: case p1
F : Type u_1
inst✝¹ : Field F
inst✝ : CharZero F
p : F[X]
d : ℕ
hp : p ≠ 0
hpd : rootMultiplicity 1 p < d
q : F[X]
hq1 : p = (X - C 1) ^ rootMultiplicity 1 p * q
hq2 : ¬X - C 1 ∣ q
heq : p = q * (-1) ^ rootMultiplicity 1 p * (1 - X) ^ rootMultiplicity 1 p
this : (fun x a ↦ a) = fun x a ↦ a * 1 ^ x
⊢ ¬eval 1 q = 0 ∧ ¬(d - rootMultiplicity 1 p - 1)! = 0

Tactic:
exact ⟨(not_iff_not.2 dvd_iff_isRoot).1 hq2, factorial_ne_zero _⟩

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

Goal state before:
pp: case inr.inl
n : ℕ
z : ℂ
h1 : z ^ n = z + 1
h2 : z ^ n + z ^ 2 = 0
h3 : z ^ 3 = 1
z_ne_zero : z ≠ 0
key : z ^ n = z
⊢ False

Tactic:
exact one_ne_zero (by rwa [key, left_eq_add] at h1)

Goal state after:
Module: Mathlib.RingTheory.Radical.NatInt

Goal state before:
pp: case inr.refine_2
z : ℤ
hz : z ≠ 0
p : ℤ
h : ∃ a, (Nat.Prime a ∧ a ∣ z.natAbs ∧ z.natAbs ≠ 0) ∧ Nat.castEmbedding.toFun a = p
⊢ Prime p ∧ 0 ≤ p ∧ p ∣ z

Tactic:
Function.Embedding.toFun_eq_coe,

Goal state after:
case inr.refine_2
z : ℤ
hz : z ≠ 0
p : ℤ
h : ∃ a, (Nat.Prime a ∧ a ∣ z.natAbs ∧ z.natAbs ≠ 0) ∧ Nat.castEmbedding a = p
⊢ Prime p ∧ 0 ≤ p ∧ p ∣ z
Module: Mathlib.RingTheory.TensorProduct.DirectLimitFG

Goal state before:
pp: R : Type u_1
S : Type u_2
N : Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : Semiring S
inst✝² : Algebra R S
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
A : Subalgebra R S
hA : A.FG
t : ↥A ⊗[R] N
A' : Subalgebra R S
hA' : A'.FG
t' : ↥A' ⊗[R] N
h : (rTensor N A.val.toLinearMap) t = (rTensor N A'.val.toLinearMap) t'
⊢ ∃ B,
    ∃ (hAB : A ≤ B) (hA'B : A' ≤ B),
      B.FG ∧
        (rTensor N (Subalgebra.inclusion hAB).toLinearMap) t = (rTensor N (Subalgebra.inclusion hA'B).toLinearMap) t'

Tactic:
have hj : (A ⊔ A').val.comp (Subalgebra.inclusion le_sup_left) = A.val := by ext; rfl
  have hj' : (A ⊔ A').val.comp (Subalgebra.inclusion le_sup_right) = A'.val := by ext; rfl
  simp only [← hj, ← hj', AlgHom.comp_toLinearMap, rTensor_comp, comp_apply] at h
  let ⟨B, hB_le, hB, h⟩ := TensorProduct.Algebra.eq_of_fg_of_subtype_eq
    (Subalgebra.FG.sup hA hA') h
  use B, le_trans le_sup_left hB_le, le_trans le_sup_right hB_le, hB
  simpa only [← rTensor_comp, ← comp_apply] using! h

Goal state after:
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
inst✝ : IsHausdorff I A
q q' : A⟦X⟧
r r' : A[X]
hr : r.degree < ↑((map (Ideal.Quotient.mk I)) g).order.toNat
hr' : r'.degree < ↑((map (Ideal.Quotient.mk I)) g).order.toNat
heq : g * (q - q') = ↑(r' - r)
h : q - q' = 0 ∧ r' - r = 0
⊢ q = q' ∧ r = r'

Tactic:
simp_rw [sub_eq_zero] at h

Goal state after:
A : Type u_1
inst✝¹ : CommRing A
g : A⟦X⟧
I : Ideal A
H : g.IsWeierstrassDivisorAt I
inst✝ : IsHausdorff I A
q q' : A⟦X⟧
r r' : A[X]
hr : r.degree < ↑((map (Ideal.Quotient.mk I)) g).order.toNat
hr' : r'.degree < ↑((map (Ideal.Quotient.mk I)) g).order.toNat
heq : g * (q - q') = ↑(r' - r)
h : q = q' ∧ r' = r
⊢ q = q' ∧ r = r'
Module: Mathlib.RingTheory.PolynomialLaw.Basic

Goal state before:
pp: R : Type u
inst✝⁸ : CommSemiring R
M : Type u_3
inst✝⁷ : AddCommMonoid M
inst✝⁶ : Module R M
N : Type u_4
inst✝⁵ : AddCommMonoid N
inst✝⁴ : Module R N
P : Type u_5
inst✝³ : AddCommMonoid P
inst✝² : Module R P
f : M →ₚₗ[R] N
g : N →ₚₗ[R] P
S : Type u_7
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
m : S ⊗[R] M
⊢ toFun S (g.comp f) m = toFun S g (toFun S f m)

Tactic:
by
  simp only [toFun_comp, Function.comp_apply]

Goal state after:
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 = ⊥
this✝² : IsSemisimpleModule R ↥c
this✝¹ : IsSemisimpleModule R ↥(c ⊓ sSup s)
this✝ : ∀ (c : ↑s), IsSemisimpleModule R ↥↑c
S : Submodule R M
le : S ≤ c ⊓ sSup s
right✝ : IsSimpleModule R ↥S
c' : Submodule R M
hc' : c' ∈ s
S' : Submodule R M
le' : S' ≤ c'
e : ↥S ≃ₗ[R] ↥S'
this : IsSimpleModule R ↥S'
⊢ False

Tactic:
refine hc'.2 ?_

Goal state after:
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 = ⊥
this✝² : IsSemisimpleModule R ↥c
this✝¹ : IsSemisimpleModule R ↥(c ⊓ sSup s)
this✝ : ∀ (c : ↑s), IsSemisimpleModule R ↥↑c
S : Submodule R M
le : S ≤ c ⊓ sSup s
right✝ : IsSimpleModule R ↥S
c' : Submodule R M
hc' : c' ∈ s
S' : Submodule R M
le' : S' ≤ c'
e : ↥S ≃ₗ[R] ↥S'
this : IsSimpleModule R ↥S'
⊢ c' ∈ {c}
Module: Mathlib.RingTheory.TensorProduct.IsBaseChangeRightExact

Goal state before:
pp: case refine_1
R : Type u_1
inst✝²⁰ : CommRing R
S : Type u_2
inst✝¹⁹ : CommRing S
inst✝¹⁸ : Algebra R S
M₁ : Type u_3
M₂ : Type u_4
M₃ : Type u_5
N₁ : Type u_6
N₂ : Type u_7
N₃ : Type u_8
inst✝¹⁷ : AddCommGroup M₁
inst✝¹⁶ : AddCommGroup M₂
inst✝¹⁵ : AddCommGroup M₃
inst✝¹⁴ : AddCommGroup N₁
inst✝¹³ : AddCommGroup N₂
inst✝¹² : AddCommGroup N₃
inst✝¹¹ : Module R M₁
inst✝¹⁰ : Module R M₂
inst✝⁹ : Module R M₃
inst✝⁸ : Module R N₁
inst✝⁷ : Module R N₂
inst✝⁶ : Module R N₃
inst✝⁵ : Module S N₁
inst✝⁴ : Module S N₂
inst✝³ : Module S N₃
inst✝² : IsScalarTower R S N₁
inst✝¹ : IsScalarTower R S N₂
inst✝ : IsScalarTower R S N₃
h₁ : M₁ →ₗ[R] N₁
h₂ : M₂ →ₗ[R] N₂
h₃ : M₃ →ₗ[R] N₃
f : M₁ →ₗ[R] M₂
g : M₂ →ₗ[R] M₃
f' : N₁ →ₗ[S] N₂
g' : N₂ →ₗ[S] N₃
comm₁ : h₂ ∘ₗ f = ↑R f' ∘ₗ h₁
comm₂ : h₃ ∘ₗ g = ↑R g' ∘ₗ h₂
isb₁ : Function.Bijective ⇑(TensorProduct.lift (↑R ((Algebra.linearMap S (Module.End S (M₁ →ₗ[R] N₁))).flip h₁)))
isb₂ : Function.Bijective ⇑(TensorProduct.lift (↑R ((Algebra.linearMap S (Module.End S (M₂ →ₗ[R] N₂))).flip h₂)))
exact₁ : Function.Exact ⇑f ⇑g
surj₁ : Function.Surjective ⇑g
exact₂ : Function.Exact ⇑f' ⇑g'
surj₂ : Function.Surjective ⇑g'
⊢ ↑R f' ∘ₗ TensorProduct.lift (↑R ((Algebra.linearMap S (Module.End S (M₁ →ₗ[R] N₁))).flip h₁)) =
    TensorProduct.lift (↑R ((Algebra.linearMap S (Module.End S (M₂ →ₗ[R] N₂))).flip h₂)) ∘ₗ
      ↑R (LinearMap.baseChange S f)

Tactic:
ext s m
    simpa using congr(s • ($comm₁ m)).symm

Goal state after:
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
hpi : ↑p ^ i = 0
⊢ i = n

Tactic:
contrapose! hpi
  replace hin := lt_of_le_of_ne hin hpi; clear hpi
  have : (p : TruncatedWittVector p n R) ^ i = WittVector.truncate n ((p : 𝕎 R) ^ i) := by
    rw [map_pow, map_natCast]
  rw [this, ne_eq, TruncatedWittVector.ext_iff, not_forall]; clear this
  use ⟨i, hin⟩
  rw [WittVector.coeff_truncate, coeff_zero, Fin.val_mk, WittVector.coeff_p_pow]
  have : Nontrivial R := CharP.nontrivial_of_char_ne_one hp.1.ne_one
  exact one_ne_zero

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
m n : ℕ
h : m ≤ n
⊢ (ZMod.castHom ⋯ (ZMod (p ^ m))).comp ((zmodEquivTrunc p n).symm.toRingHom.comp (truncate n)) =
    ((zmodEquivTrunc p m).symm.toRingHom.comp (TruncatedWittVector.truncate h)).comp (truncate n)

Tactic:
rw [commutes_symm, RingHom.comp_assoc]

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

Goal state before:
pp: p n : ℕ
mvpz : ↑p ^ (n + 1) = C (↑p ^ (n + 1))
| ∑ x ∈ range (n + 1), (rename (Prod.mk 0)) ((monomial (Finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x)) +
    (rename (Prod.mk 0)) (C (↑p ^ (n + 1)) * X (n + 1) ^ p ^ (n + 1 - (n + 1)))

Tactic:
tsub_self,

Goal state after:
p n : ℕ
mvpz : ↑p ^ (n + 1) = C (↑p ^ (n + 1))
| ∑ x ∈ range (n + 1), (rename (Prod.mk 0)) ((monomial (Finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x)) +
    (rename (Prod.mk 0)) (C (↑p ^ (n + 1)) * X (n + 1) ^ p ^ 0)
Module: Mathlib.RingTheory.WittVector.MulCoeff

Goal state before:
pp: p n : ℕ
mvpz : ↑p ^ (n + 1) = C (↑p ^ (n + 1))
| ∑ x ∈ range (n + 1), (rename (Prod.mk 1)) ((monomial (Finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x)) +
    (rename (Prod.mk 1)) (C (↑p ^ (n + 1)) * X (n + 1) ^ p ^ (n + 1 - (n + 1)))

Tactic:
tsub_self,

Goal state after:
p n : ℕ
mvpz : ↑p ^ (n + 1) = C (↑p ^ (n + 1))
| ∑ x ∈ range (n + 1), (rename (Prod.mk 1)) ((monomial (Finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x)) +
    (rename (Prod.mk 1)) (C (↑p ^ (n + 1)) * X (n + 1) ^ p ^ 0)
Module: Mathlib.SetTheory.Descriptive.Tree

Goal state before:
pp: A : Type u_1
T : ↥(tree A)
x : List A
⊢ x ∈ pullSub T x ↔ [] ∈ T

Tactic:
by
  simpa using mem_pullSub_append (y := [])

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

Goal state before:
pp: A : Type u_1
S T : ↥(tree A)
x : List A
x✝ : S ≤ subAt T x
⊢ pullSub S x ≤ pullSub (subAt T x) x

Tactic:
by gcongr

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

Goal state before:
pp: α : Type u
inst✝ : CompleteLattice α
f : α →o α
x : α
a : Ordinal.{u}
ha : IsSuccLimit a
⊢ lfpApprox f x a = ⨆ b, lfpApprox f x ↑b

Tactic:
by
  apply (iSup_le fun b => lfpApprox_mono_right f b.2.le).antisymm'
  rw [lfpApprox, sup_le_iff, iSup_le_iff]
  constructor
  · refine le_iSup_of_le ⟨0, ha.bot_lt⟩ (by simp [lfpApprox_zero])
  · exact fun b => iSup_mono' fun hab => ⟨⟨b + 1, ha.succ_lt hab⟩, (by
    simpa using apply_lfpApprox_le_lfpApprox_of_lt f (lt_add_one b))⟩

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

Goal state before:
pp: α : Type u
inst✝ : CompleteLattice α
f g : α →o α
h : f ≤ g
⊢ lfpApprox f ≤ lfpApprox g

Tactic:
x

Goal state after:
α : Type u
inst✝ : CompleteLattice α
f g : α →o α
h : f ≤ g
x : α
⊢ lfpApprox f x ≤ lfpApprox g x
Module: Mathlib.SetTheory.Ordinal.CantorNormalForm

Goal state before:
pp: b o : Ordinal.{u}
x : Ordinal.{u} × Ordinal.{u}
⊢ x ∈ CNF b o → 0 < x.2

Tactic:
refine CNF.rec b (by simp) (fun o ho IH ↦ ?_) o
  rw [CNF.ne_zero ho]
  rintro (h | ⟨_, h⟩)
  · exact div_opow_log_pos b ho
  · exact IH h

Goal state after:
Module: Mathlib.Topology.Order.SuccPred

Goal state before:
pp: α : Type u_1
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
a : α
inst✝¹ : SuccOrder α
inst✝ : NoMaxOrder α
a✝ : Nontrivial α
⊢ IsOpen[inst✝³] {a} ↔ ¬IsSuccLimit a

Tactic:
refine ⟨fun h ha ↦ ?_, fun ha ↦ ?_⟩

Goal state after:
case refine_1
α : Type u_1
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
a : α
inst✝¹ : SuccOrder α
inst✝ : NoMaxOrder α
a✝ : Nontrivial α
h : IsOpen[inst✝³] {a}
ha : IsSuccLimit a
⊢ False

case refine_2
α : Type u_1
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
a : α
inst✝¹ : SuccOrder α
inst✝ : NoMaxOrder α
a✝ : Nontrivial α
ha : ¬IsSuccLimit a
⊢ IsOpen[inst✝³] {a}
Module: Mathlib.SetTheory.Ordinal.Topology

Goal state before:
pp: case mpr
s : Set Ordinal.{u}
h : ∀ {ι : Type u}, Nonempty ι → ∀ (f : ι → Ordinal.{u}), (∀ (i : ι), f i ∈ s) → ⨆ i, f i ∈ s
⊢ closure s ⊆ s

Tactic:
x

Goal state after:
case mpr
s : Set Ordinal.{u}
h : ∀ {ι : Type u}, Nonempty ι → ∀ (f : ι → Ordinal.{u}), (∀ (i : ι), f i ∈ s) → ⨆ i, f i ∈ s
x : Ordinal.{u}
⊢ x ∈ closure s → x ∈ s
Module: Mathlib.SetTheory.Ordinal.CantorNormalForm

Goal state before:
pp: b o : Ordinal.{u_1}
a : Ordinal.{u_1} × Ordinal.{u_1}
ha : a ∈ CNF b o
⊢ ∀ (b_1 : Ordinal.{u_1}), b ^ a.1 * (coeff b o) a.1 + b_1 = b ^ a.1 * a.2 + b_1

Tactic:
x

Goal state after:
b o : Ordinal.{u_1}
a : Ordinal.{u_1} × Ordinal.{u_1}
ha : a ∈ CNF b o
x : Ordinal.{u_1}
⊢ b ^ a.1 * (coeff b o) a.1 + x = b ^ a.1 * a.2 + x
Module: Mathlib.SetTheory.Ordinal.CantorNormalForm

Goal state before:
pp: case pos
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
⊢ f e' < b

Tactic:
apply (hf e').trans_eq'

Goal state after:
case pos
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
⊢ (single e x + f) e' = f e'
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: 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
⊢ (a₁.cmp a₂).Compares a₁ a₂ →
    (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:
cases cmp a₁ a₂ <;> intro IHa

Goal state after:
case eq.inr.inr.lt
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
IHa : Ordering.lt.Compares a₁ a₂
⊢ (Ordering.eq.then (Ordering.eq.then Ordering.lt)).Compares (namedPattern o₁ (e₁.oadd n₂ a₁) h✝)
    (namedPattern o₂ (e₁.oadd n₂ a₂) h✝¹)

case eq.inr.inr.eq
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
IHa : Ordering.eq.Compares a₁ a₂
⊢ (Ordering.eq.then (Ordering.eq.then Ordering.eq)).Compares (namedPattern o₁ (e₁.oadd n₂ a₁) h✝)
    (namedPattern o₂ (e₁.oadd n₂ a₂) h✝¹)

case eq.inr.inr.gt
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
IHa : Ordering.gt.Compares a₁ a₂
⊢ (Ordering.eq.then (Ordering.eq.then Ordering.gt)).Compares (namedPattern o₁ (e₁.oadd n₂ a₁) h✝)
    (namedPattern o₂ (e₁.oadd n₂ a₂) h✝¹)
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: ⊢ DecidableRel TopBelow

Tactic:
intro b o

Goal state after:
b o : ONote
⊢ Decidable (b.TopBelow o)
Module: Mathlib.SetTheory.ZFC.Rank

Goal state before:
pp: case a
x : PSet.{u_1}
⊢ x.rank < x.powerset.rank

Tactic:
apply rank_lt_of_mem

Goal state after:
case a
x : PSet.{u_1}
⊢ x ∈ x.powerset
Module: Mathlib.SetTheory.ZFC.Rank

Goal state before:
pp: x y✝ w✝ : PSet.{u_1}
left✝ : w✝ ∈ x
right✝ : y✝ ∈ w✝
⊢ y✝.rank < ?m.36

Tactic:
apply rank_lt_of_mem

Goal state after:
case a
x y✝ w✝ : PSet.{u_1}
left✝ : w✝ ∈ x
right✝ : y✝ ∈ w✝
⊢ y✝ ∈ ?x

case x
x y✝ w✝ : PSet.{u_1}
left✝ : w✝ ∈ x
right✝ : y✝ ∈ w✝
⊢ PSet.{u_1}
Module: Mathlib.SetTheory.ZFC.Rank

Goal state before:
pp: x y✝ w✝ : PSet.{u_1}
left✝ : w✝ ∈ x
right✝ : y✝ ∈ w✝
⊢ rank ?x < x.rank

Tactic:
apply rank_lt_of_mem

Goal state after:
x y✝ w✝ : PSet.{u_1}
left✝ : w✝ ∈ x
right✝ : y✝ ∈ w✝
⊢ ?x✝ ∈ x
Module: Mathlib.SetTheory.ZFC.Rank

Goal state before:
pp: case a.f
x y y✝ : ZFSet.{u_1}
⊢ y✝ ∈ x → y✝.rank < x.rank

Tactic:
apply rank_lt_of_mem

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

Goal state before:
pp: case a.g
x y y✝ : ZFSet.{u_1}
⊢ y✝ ∈ y → y✝.rank < y.rank

Tactic:
apply rank_lt_of_mem

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

Goal state before:
pp: x y✝ w✝ : ZFSet.{u_1}
left✝ : w✝ ∈ x
right✝ : y✝ ∈ w✝
⊢ y✝.rank < ?m.36

Tactic:
apply rank_lt_of_mem

Goal state after:
case a
x y✝ w✝ : ZFSet.{u_1}
left✝ : w✝ ∈ x
right✝ : y✝ ∈ w✝
⊢ y✝ ∈ ?x

case x
x y✝ w✝ : ZFSet.{u_1}
left✝ : w✝ ∈ x
right✝ : y✝ ∈ w✝
⊢ ZFSet.{u_1}
Module: Mathlib.SetTheory.ZFC.Rank

Goal state before:
pp: x y✝ w✝ : ZFSet.{u_1}
left✝ : w✝ ∈ x
right✝ : y✝ ∈ w✝
⊢ rank ?x < x.rank

Tactic:
apply rank_lt_of_mem

Goal state after:
x y✝ w✝ : ZFSet.{u_1}
left✝ : w✝ ∈ x
right✝ : y✝ ∈ w✝
⊢ ?x✝ ∈ x
Module: Mathlib.SetTheory.ZFC.Ordinal

Goal state before:
pp: x y : ZFSet.{u}
hx : x.IsTransitive
hy : y.IsTransitive
z : ZFSet.{u}
hz : z ∈ x ∧ z ∈ y
w : ZFSet.{u}
hw : w ∈ z
⊢ w ∈ x ∧ w ∈ y

Tactic:
exact ⟨hx.mem_trans hw hz.1, hy.mem_trans hw hz.2⟩

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

Goal state before:
pp: a b : Ordinal.{u_1}
h : a ≤ b
⊢ a.toZFSet ⊆ b.toZFSet

Tactic:
x

Goal state after:
a b : Ordinal.{u_1}
h : a ≤ b
x : ZFSet.{u_1}
⊢ x ∈ a.toZFSet → x ∈ b.toZFSet
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Majorized

Goal state before:
pp: f : ℝ → ℝ
exp : ℝ
h : Tendsto f atTop atTop
exp' : ℝ
h_exp : exp' > exp
⊢ Tendsto (fun x ↦ (f ^ exp) x / (f ^ exp') x) atTop (𝓝 0)

Tactic:
have : (fun t ↦ f t ^ exp / f t ^ exp') =ᶠ[atTop] fun t ↦ (f t) ^ (exp - exp') :=
      (h.eventually_gt_atTop 0).mono (fun _ h ↦ by simp [← Real.rpow_sub h])
    apply Tendsto.congr' this.symm
    conv =>
      arg 1
      rw [show (fun t ↦ f t ^ (exp - exp')) = ((fun t ↦ t ^ (-(exp' - exp))) ∘ f) by ext; simp]
    exact (tendsto_rpow_neg_atTop (by linarith)).comp h

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

Goal state before:
pp: case succ.refine_1
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
⊢ R' < (ω ^ a0.repr) ^ succ ↑(k + 1)

pp: case succ.refine_2
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)
⊢ (ω ^ a0.repr) ^ ↑(k + 1) * (ω ^ a0.repr * ↑↑n + a'.repr) + R' = (ω ^ a0.repr * ↑↑n + a'.repr + ↑m) ^ succ ↑(k + 1)

Tactic:
· rw [RR, ← opow_mul _ _ (succ k.succ)]
    have e0 := pos_iff_ne_zero.2 e0
    have rr0 : 0 < repr a0 + repr a0 := lt_of_lt_of_le e0 le_add_self
    apply isPrincipal_add_omega0_opow
    · simp only [Nat.cast_add_one, opow_add_one, opow_mul, opow_succ, mul_assoc]
      gcongr ?_ * ?_
      rw [← Ordinal.opow_add]
      have : _ < ω ^ (repr a0 + repr a0) := (No.below_of_lt ?_).repr_lt
      · exact mul_lt_omega0_opow rr0 this (natCast_lt_omega0 _)
      · simpa using (add_lt_add_iff_left (repr a0)).2 e0
    · exact
        lt_of_lt_of_le Rl
          (opow_le_opow_right omega0_pos <|
            mul_le_mul_right (succ_le_succ_iff.2 (Nat.cast_le.2 (le_of_lt k.lt_succ_self))) _)

Goal state after:
case succ.refine_2
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)
⊢ (ω ^ a0.repr) ^ ↑(k + 1) * (ω ^ a0.repr * ↑↑n + a'.repr) + R' = (ω ^ a0.repr * ↑↑n + a'.repr + ↑m) ^ succ ↑(k + 1)
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: 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)
⊢ (ω0 ^ ↑k * α' + R) * (α' + ↑m) = (α' + ↑m) ^ succ ↑k.succ

Tactic:
opow_succ,

Goal state after:
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)
⊢ (ω0 ^ ↑k * α' + R) * (α' + ↑m) = (α' + ↑m) ^ ↑k.succ * (α' + ↑m)
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:
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: