mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Valuation.Quotient

Goal state before:
pp: R : Type u_1
Γ₀ : Type u_2
inst✝¹ : CommRing R
inst✝ : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
J : Ideal R
hJ : J ≤ v.supp
q : R ⧸ J
a b : R
h : (Submodule.quotientRel J) a b
⊢ v a = v (b + -(-a + b))

Tactic:
by simp

Goal state after:
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 ≤ (comap (Ideal.Quotient.mk J) v).supp

Tactic:
rw [comap_supp, ← Ideal.map_le_iff_le_comap]
  simp

Goal state after:
Module: Mathlib.RingTheory.Smooth.Quotient

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommRing R
M : Type u_2
N : Type u_3
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
I : Ideal R
f : M →ₗ[R] N
surj : Function.Surjective ⇑f
inst✝ : Module.Flat R N
⊢ f.ker ⊓ I • ⊤ = I • f.ker

Tactic:
refine le_antisymm (fun x hx ↦ ?_) (fun x hx ↦ ?_)
  · rcases (Submodule.ext_iff.mp (I.subtype_rTensor_range M) x).mpr hx.2 with ⟨y, hy⟩
    have inj : Function.Injective ((TensorProduct.lid R N).comp (I.subtype.rTensor N)) := by
      simpa using Module.Flat.iff_rTensor_injective'.mp ‹_› I
    have comm1 : ((TensorProduct.lid R N).comp (I.subtype.rTensor N)).comp (f.lTensor I) =
      f.comp ((TensorProduct.lid R M).comp (I.subtype.rTensor M)) := by
      ext
      simp
    have eq0 : f.lTensor I y = 0 := by
      apply inj
      rw [map_zero, ← LinearMap.comp_apply, comm1, LinearMap.comp_apply, hy, f.mem_ker.mp hx.1]
    rcases ((lTensor_exact I (f.exact_subtype_ker_map) surj) y).mp eq0 with ⟨z, hz⟩
    have comm2 : ((TensorProduct.lid R M).comp (I.subtype.rTensor M)).comp
      (f.ker.subtype.lTensor I) = f.ker.subtype.comp
      ((TensorProduct.lid R f.ker).comp (I.subtype.rTensor f.ker)) := by
      ext
      simp
    apply (Submodule.mem_smul_top_iff I f.ker ⟨x, hx.1⟩).mp
    rw [← Ideal.subtype_rTensor_range]
    use z
    apply f.ker.subtype_injective
    rw [← LinearMap.comp_apply, ← comm2, LinearMap.comp_apply, hz, hy, Submodule.subtype_apply]
  · induction hx using Submodule.smul_induction_on' with
    | smul r hr m hm =>
      simpa [LinearMap.mem_ker.mp hm] using Submodule.smul_mem_smul hr Submodule.mem_top
    | add y ymem z zmem hy hz => exact add_mem hy hz

Goal state after:
Module: Mathlib.RingTheory.Valuation.Extension

Goal state before:
pp: R : Type u_1
A : Type u_2
ΓR✝ : Type u_3
ΓA✝ : Type u_4
inst✝¹² : CommRing R
inst✝¹¹ : Ring A
inst✝¹⁰ : LinearOrderedCommMonoidWithZero ΓR✝
inst✝⁹ : LinearOrderedCommMonoidWithZero ΓA✝
inst✝⁸ : Algebra R A
vR✝ : Valuation R ΓR✝
vA✝ : Valuation A ΓA✝
K : Type u_5
inst✝⁷ : Field K
inst✝⁶ : Algebra K A
ΓR : Type u_6
ΓA : Type u_7
ΓK : Type u_8
inst✝⁵ : LinearOrderedCommGroupWithZero ΓR
inst✝⁴ : LinearOrderedCommGroupWithZero ΓK
inst✝³ : LinearOrderedCommGroupWithZero ΓA
vR : Valuation R ΓR
vK : Valuation K ΓK
vA : Valuation A ΓA
inst✝² : vR.HasExtension vA
inst✝¹ : IsDomain R
inst✝ : IsTorsionFree R A
⊢ ∀ (r : ↥vR.integer) (m : ↥vA.integer), r • m = 0 → r = 0 ∨ m = 0

Tactic:
by simp

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

Goal state before:
pp: case h
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 : StandardOneDimIsocrystal p k m ≃ₗ[K(p, k)] V := LinearEquiv.ofBijective F₀ ⋯
c : StandardOneDimIsocrystal p k m
⊢ Φ(p, k) (b • F₀ c) = b • F₀ (↑p ^ m • φ(p, k) c)

Tactic:
rw [LinearMap.toSpanSingleton_apply K(p, k) V x c, LinearMap.toSpanSingleton_apply K(p, k) V x]

Goal state after:
case h
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 : StandardOneDimIsocrystal p k m ≃ₗ[K(p, k)] V := LinearEquiv.ofBijective F₀ ⋯
c : StandardOneDimIsocrystal p k m
⊢ Φ(p, k) (b • c • x) = b • (↑p ^ m • φ(p, k) c) • x
Module: Mathlib.SetTheory.Descriptive.Tree

Goal state before:
pp: A : Type u_1
S T : ↥(tree A)
x✝ y : List A
n : ℕ
x : ↥T
⊢ List.drop n ↑x ∈ subAt T ↑(take n x)

Tactic:
by simp

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

Goal state before:
pp: A : Type u_1
T : ↥(tree A)
x y z : List A
hl : z.length ≤ x.length
⊢ [].length ≤ y.length

Tactic:
by simp

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

Goal state before:
pp: α : Type v
inst✝¹ : LinearOrder α
inst✝ : OrderTop α
s : Set (Set α)
⊢ cof α ≤ 1

Tactic:
by simp

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

Goal state before:
pp: α : Type v
inst✝¹ : LinearOrder α
inst✝ : OrderTop α
ι : Sort u_1
f : ι → Set α
⊢ cof α ≤ 1

Tactic:
by simp

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

Goal state before:
pp: α : Type v
inst✝² : LinearOrder α
inst✝¹ : WellFoundedLT α
ι : Sort u_1
f : ι → Set α
inst✝ : Countable ι
hα : cof α ≠ ℵ₀
⊢ IsStationary (⋃₀ range f) ↔ ∃ i, IsStationary (f i)

Tactic:
isStationary_sUnion_iff_of_countable hα (countable_range f)

Goal state after:
α : Type v
inst✝² : LinearOrder α
inst✝¹ : WellFoundedLT α
ι : Sort u_1
f : ι → Set α
inst✝ : Countable ι
hα : cof α ≠ ℵ₀
⊢ (∃ x ∈ range f, IsStationary x) ↔ ∃ i, IsStationary (f i)
Module: Mathlib.SetTheory.Ordinal.Commute

Goal state before:
pp: o₂ : Ordinal.{u_1}
hcomm : AddCommute 0 o₂
ih : ∀ y < 0 + o₂, ∀ {o₁ o₂ : Ordinal.{u_1}}, AddCommute o₁ o₂ → o₁ + o₂ = y → ∃ o n₁ n₂, o * ↑n₁ = o₁ ∧ o * ↑n₂ = o₂
hle : 0 ≤ o₂
⊢ o₂ * ↑0 = 0

Tactic:
by simp

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

Goal state before:
pp: o₂ : Ordinal.{u_1}
hcomm : AddCommute 0 o₂
ih : ∀ y < 0 + o₂, ∀ {o₁ o₂ : Ordinal.{u_1}}, AddCommute o₁ o₂ → o₁ + o₂ = y → ∃ o n₁ n₂, o * ↑n₁ = o₁ ∧ o * ↑n₂ = o₂
hle : 0 ≤ o₂
⊢ o₂ * ↑1 = o₂

Tactic:
by simp

Goal state after:
Module: Mathlib.SetTheory.Lists

Goal state before:
pp: α : Type u_1
motive : Lists' α true → Sort u_2
ofList : (l : List (Lists α)) → motive (Lists'.ofList l)
l : Lists' α true
⊢ motive (Lists'.ofList l.toList) = motive l

Tactic:
by simp

Goal state after:
Module: Mathlib.SetTheory.Lists

Goal state before:
pp: α : Type u_1
l₁ l₂ : List (Lists α)
h : l₁ ⊆ l₂
⊢ ofList l₁ ⊆ ofList l₂

Tactic:
induction l₁ with

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

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

Tactic:
by simp

Goal state after:
Module: Mathlib.SetTheory.Lists

Goal state before:
pp: case ofList
α : Type u_1
l₂ : Lists' α true
l₁ : List (Lists α)
H : ∀ (a : Lists α), a ∈ (ofList l₁).toList → a ∈ l₂
⊢ ofList l₁ ⊆ l₂

Tactic:
induction l₁ with

Goal state after:
Module: Mathlib.SetTheory.Lists

Goal state before:
pp: α : Type u_1
C : Lists α → Sort u_2
D : Lists' α true → Sort u_3
C0 : (a : α) → C (atom a)
C1 : (l : Lists' α true) → D l → C (of' l)
D0 : D Lists'.nil
D1 : (a : Lists α) → (l : Lists' α true) → C a → D l → D (Lists'.cons a l)
b : Bool
⊢ (l : Lists' α b) →
    C ⟨b, l⟩ ×'
      match b, l with
      | true, l => D l
      | false, x => PUnit

Tactic:
l

Goal state after:
α : Type u_1
C : Lists α → Sort u_2
D : Lists' α true → Sort u_3
C0 : (a : α) → C (atom a)
C1 : (l : Lists' α true) → D l → C (of' l)
D0 : D Lists'.nil
D1 : (a : Lists α) → (l : Lists' α true) → C a → D l → D (Lists'.cons a l)
b : Bool
l : Lists' α b
⊢ C ⟨b, l⟩ ×'
    match b, l with
    | true, l => D l
    | false, x => PUnit
Module: Mathlib.SetTheory.Lists

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

Tactic:
l

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

Goal state before:
pp: b e x y : Ordinal.{u_1}
hb : 1 < b
hx : x ≠ 0
hxb : x < b
hy : y < b ^ e
⊢ coeff b (b ^ e * x + y) = single e x + coeff b y

Tactic:
ext e'
  rw [add_apply]
  obtain rfl | he := eq_or_ne e e'
  · rw [single_eq_same, coeff_eq_zero_of_lt hy, add_zero]
    apply coeff_of_mem_CNF
    rw [CNF.opow_mul_add hb hx hxb hy]
    exact mem_cons_self
  · rw [single_eq_of_ne' he, zero_add]
    by_cases h : e' ∈ (CNF b y).map Prod.fst
    · rw [mem_map] at h
      obtain ⟨⟨f, c⟩, hf, rfl⟩ := h
      rw [coeff_of_mem_CNF hf]
      apply coeff_of_mem_CNF
      rw [CNF.opow_mul_add hb hx hxb hy]
      exact mem_cons_of_mem _ hf
    · rw [coeff_of_notMem_CNF h, coeff_of_notMem_CNF]
      rw [mem_map] at h ⊢
      rw [CNF.opow_mul_add hb hx hxb hy]
      simp_all

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

Goal state before:
pp: s : Set Ordinal.{u}
ι : Type u
w✝ : Nonempty ι
f : ι → Ordinal.{u}
hf : ∀ (i : ι), f i ∈ s
⊢ type WellOrderingRel ≠ 0

Tactic:
by simp

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

Goal state before:
pp: x : PSet.{u_1}
y : PSet.{u_2}
inst✝¹ : IsEmpty x.Type
inst✝ : IsEmpty y.Type
⊢ (∀ (i : x.Type), ∃ j, (x.Func i).Equiv (y.Func j)) ∧ ∀ (j : y.Type), ∃ i, (x.Func i).Equiv (y.Func j)

Tactic:
by simp

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

Goal state before:
pp: x y z : ZFSet.{u}
p : ZFSet.{?u.28} → Prop
x✝³ x✝² : PSet.{?u.28}
α : Type ?u.28
A : α → PSet.{?u.28}
β : Type ?u.28
B : β → PSet.{?u.28}
x✝¹ : PSet.mk α A ≈ PSet.mk β B
αβ : ∀ (a : α), ∃ b, (A a).Equiv (B b)
βα : ∀ (b : β), ∃ a, (A a).Equiv (B b)
x✝ : { a // (fun y ↦ p (mk y)) ((PSet.mk α A).Func a) }
a : (PSet.mk α A).Type
pa : (fun y ↦ p (mk y)) ((PSet.mk α A).Func a)
b : β
hb : (A a).Equiv (B b)
⊢ (fun y ↦ p (mk y)) ((PSet.mk β B).Func b)

Tactic:
simpa only [mk_func, ← ZFSet.sound hb]

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

Goal state before:
pp: o : ONote
x✝¹ : NF 0
x✝ : o.NF
⊢ (0 + o).repr = repr 0 + o.repr

Tactic:
by simp

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

Goal state before:
pp: case cons
f : Ordinal.{u} → Ordinal.{u}
hf : IsNormal f
hp : 0 < f 0
o : Ordinal.{u}
ho : IsSuccLimit o
a✝ : Ordinal.{u}
IH : ∀ b < o, veblenWith f b 0 ≤ a✝
a : ↑(Iio o)
l : List ↑(Iio o)
b : Ordinal.{u}
hb : b < o
hb' : List.foldr (fun x ↦ veblenWith f ↑x) 0 l ≤ veblenWith f b 0
⊢ veblenWith f (↑a) ((fun x ↦ veblenWith f x 0) (succ (max (↑a) b))) ≤ veblenWith f (succ (max (↑a) b)) 0

Tactic:
veblenWith_veblenWith_of_lt hf

Goal state after:
case cons
f : Ordinal.{u} → Ordinal.{u}
hf : IsNormal f
hp : 0 < f 0
o : Ordinal.{u}
ho : IsSuccLimit o
a✝ : Ordinal.{u}
IH : ∀ b < o, veblenWith f b 0 ≤ a✝
a : ↑(Iio o)
l : List ↑(Iio o)
b : Ordinal.{u}
hb : b < o
hb' : List.foldr (fun x ↦ veblenWith f ↑x) 0 l ≤ veblenWith f b 0
⊢ veblenWith f (succ (max (↑a) b)) 0 ≤ veblenWith f (succ (max (↑a) b)) 0

case cons.h
f : Ordinal.{u} → Ordinal.{u}
hf : IsNormal f
hp : 0 < f 0
o : Ordinal.{u}
ho : IsSuccLimit o
a✝ : Ordinal.{u}
IH : ∀ b < o, veblenWith f b 0 ≤ a✝
a : ↑(Iio o)
l : List ↑(Iio o)
b : Ordinal.{u}
hb : b < o
hb' : List.foldr (fun x ↦ veblenWith f ↑x) 0 l ≤ veblenWith f b 0
⊢ ↑a < succ (max (↑a) b)
Module: Mathlib.SetTheory.ZFC.Basic

Goal state before:
pp: α : Type u_1
inst✝ : Small.{u, u_1} α
f : α → ZFSet.{u}
a : α
⊢ f a ∈ range f

Tactic:
by simp

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

Goal state before:
pp: o a : Ordinal.{u}
⊢ 0 < ω ^ 0

Tactic:
by simp

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

Goal state before:
pp: ⊢ 0 < ω ^ 0

Tactic:
by simp

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

Goal state before:
pp: o a : Ordinal.{u_1}
⊢ 0 < ω ^ 0

Tactic:
by simp

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

Goal state before:
pp: x : PSet.{u_1}
⊢ max (succ x.rank) ∅.rank = succ x.rank

Tactic:
by simp

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

Goal state before:
pp: case neg
x : Ordinal.{u}
h : ¬x.invVeblen₁ = 0
⊢ ∀ b < x.invVeblen₁, veblen b x = x

Tactic:
exact fun o ↦ veblen_eq_of_lt_invVeblen₁

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

Goal state before:
pp: x y✝ : PSet.{u_1}
⊢ (∃ z ∈ x, y✝ ∈ z) → y✝.rank < x.rank

Tactic:
⟨_, _, _⟩

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

Goal state before:
pp: f : ZFSet.{u} → ZFSet.{u}
inst✝ : Definable₁ f
x z : ZFSet.{u}
zx : z ∈ x
y : ZFSet.{u}
yx : (fun w ↦ z.pair w ∈ map f x) y
w : ZFSet.{u}
left✝ : w ∈ x
we : w.pair (f w) = z.pair y
⊢ y = f z

Tactic:
let ⟨wz, fy⟩ := pair_injective we

Goal state after:
f : ZFSet.{u} → ZFSet.{u}
inst✝ : Definable₁ f
x z : ZFSet.{u}
zx : z ∈ x
y : ZFSet.{u}
yx : (fun w ↦ z.pair w ∈ map f x) y
w : ZFSet.{u}
left✝ : w ∈ x
we : w.pair (f w) = z.pair y
wz : w = z
fy : f w = y
⊢ y = f z
Module: Mathlib.SetTheory.ZFC.Rank

Goal state before:
pp: x : ZFSet.{u_1}
⊢ max (succ x.rank) ∅.rank = succ x.rank

Tactic:
by simp

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

Goal state before:
pp: x y✝ : ZFSet.{u_1}
⊢ (∃ z ∈ x, y✝ ∈ z) → y✝.rank < x.rank

Tactic:
⟨_, _, _⟩

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

Goal state before:
pp: x y : Class.{u}
h : Set.Nonempty x
H : ∀ z ∈ x, y ∈ z
⊢ y ∈ ⋂₀ x

Tactic:
mem_def,

Goal state after:
x y : Class.{u}
h : Set.Nonempty x
H : ∀ z ∈ x, y ∈ z
⊢ ∃ x_1, ↑x_1 = y ∧ (⋂₀ x) x_1
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: case eq
e₁ : ONote
n₁ : ℕ+
a₁ e₂ : ONote
n₂ : ℕ+
a₂ : ONote
h₁ : (e₁.oadd n₁ a₁).NF
h₂ : (e₂.oadd n₂ a₂).NF
this✝ : a₁.NF
this : a₂.NF
h' : (a₁.sub a₂).repr = a₁.repr - a₂.repr
h : e₁.cmp e₂ = Ordering.eq
ee : Ordering.eq.Compares e₁ e₂
⊢ (match Ordering.eq with
      | Ordering.lt => 0
      | Ordering.gt => e₁.oadd n₁ a₁
      | Ordering.eq =>
        match ↑n₁ - ↑n₂ with
        | 0 => if n₁ = n₂ then a₁.sub a₂ else 0
        | k.succ => e₁.oadd k.succPNat a₁).repr =
    (e₁.oadd n₁ a₁).repr - (e₂.oadd n₂ a₂).repr

Tactic:
change e₁ = e₂ at ee

Goal state after:
case eq
e₁ : ONote
n₁ : ℕ+
a₁ e₂ : ONote
n₂ : ℕ+
a₂ : ONote
h₁ : (e₁.oadd n₁ a₁).NF
h₂ : (e₂.oadd n₂ a₂).NF
this✝ : a₁.NF
this : a₂.NF
h' : (a₁.sub a₂).repr = a₁.repr - a₂.repr
h : e₁.cmp e₂ = Ordering.eq
ee : e₁ = e₂
⊢ (match Ordering.eq with
      | Ordering.lt => 0
      | Ordering.gt => e₁.oadd n₁ a₁
      | Ordering.eq =>
        match ↑n₁ - ↑n₂ with
        | 0 => if n₁ = n₂ then a₁.sub a₂ else 0
        | k.succ => e₁.oadd k.succPNat a₁).repr =
    (e₁.oadd n₁ a₁).repr - (e₂.oadd n₂ a₂).repr
Module: Mathlib.SetTheory.ZFC.VonNeumann

Goal state before:
pp: ⊢ ∀ (x y : Ordinal.{u_1}), x ≤ y ↔ V_ x ⊆ V_ y

Tactic:
by simp

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

Goal state before:
pp: case refine_1
o : Ordinal.{u_1}
x : ZFSet.{u_1}
hx : x ∈ o.toZFSet
y : ZFSet.{u_1}
hy : y ∈ x
⊢ y ∈ o.toZFSet

Tactic:
obtain ⟨a, ha, rfl⟩ := mem_toZFSet_iff.1 hx
    obtain ⟨b, hb, rfl⟩ := mem_toZFSet_iff.1 hy

Goal state after:
case refine_1
o a : Ordinal.{u_1}
ha : a < o
hx : a.toZFSet ∈ o.toZFSet
b : Ordinal.{u_1}
hb : b < a
hy : b.toZFSet ∈ a.toZFSet
⊢ b.toZFSet ∈ o.toZFSet
Module: Mathlib.SetTheory.ZFC.Ordinal

Goal state before:
pp: case refine_2
o : Ordinal.{u_1}
z y x : ZFSet.{u_1}
hz : z ∈ y
hy : y ∈ x
hx : x ∈ o.toZFSet
⊢ z ∈ x

Tactic:
obtain ⟨a, ha, rfl⟩ := mem_toZFSet_iff.1 hx
    obtain ⟨b, hb, rfl⟩ := mem_toZFSet_iff.1 hy

Goal state after:
case refine_2
o : Ordinal.{u_1}
z : ZFSet.{u_1}
a : Ordinal.{u_1}
ha : a < o
hx : a.toZFSet ∈ o.toZFSet
b : Ordinal.{u_1}
hb : b < a
hz : z ∈ b.toZFSet
hy : b.toZFSet ∈ a.toZFSet
⊢ z ∈ a.toZFSet
Module: Mathlib.SetTheory.ZFC.Ordinal

Goal state before:
pp: case refine_2
x : ZFSet.{u}
⊢ x ∈ Set.range toZFSet → x.IsOrdinal

Tactic:
· rintro ⟨a, rfl⟩
    exact isOrdinal_toZFSet a

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

Goal state before:
pp: x y z w : ZFSet.{u}
a b : Ordinal.{?u.18}
⊢ { toFun := fun o ↦ ⟨o.toZFSet, ⋯⟩, invFun := fun x ↦ (↑x).rank, left_inv := ⋯, right_inv := ⋯ } a ≤
      { toFun := fun o ↦ ⟨o.toZFSet, ⋯⟩, invFun := fun x ↦ (↑x).rank, left_inv := ⋯, right_inv := ⋯ } b ↔
    a ≤ b

Tactic:
by simp

Goal state after:
Module: Mathlib.Tactic.Algebra.Lemmas

Goal state before:
pp: R : Type u_3
inst✝ : Ring R
a b : R
⊢ a * -b = -(a * b)

Tactic:
by simp

Goal state after:
Module: Mathlib.Tactic.Algebra.Lemmas

Goal state before:
pp: R : Type u_1
sR : CommSemiring R
⊢ Nat.rawCast 0 = 0

Tactic:
by simp

Goal state after:
Module: Mathlib.Tactic.Algebra.Lemmas

Goal state before:
pp: R : Type u_1
sR : CommSemiring R
⊢ Nat.rawCast 1 = 1

Tactic:
by simp

Goal state after:
Module: Mathlib.Tactic.Algebra.Lemmas

Goal state before:
pp: n : ℕ
R : Type u_3
inst✝ : Ring R
⊢ (Int.negOfNat n).rawCast = -n.rawCast

Tactic:
by simp

Goal state after:
Module: Mathlib.Tactic.Algebra.Lemmas

Goal state before:
pp: n d : ℕ
R : Type u_3
inst✝ : DivisionSemiring R
⊢ NNRat.rawCast n d = n.rawCast / d.rawCast

Tactic:
by simp

Goal state after:
Module: Mathlib.Tactic.Algebra.Lemmas

Goal state before:
pp: n d : ℕ
R : Type u_3
inst✝ : DivisionRing R
⊢ Rat.rawCast (Int.negOfNat n) d = (Int.negOfNat n).rawCast / d.rawCast

Tactic:
by simp

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

Goal state before:
pp: x : ONote
inst✝ : x.NF
e : ONote
n : ℕ+
a : ONote
h : (e.oadd n a).NF
this : a.NF
e0 : e = 0
⊢ (x + 0).repr = x.repr

Tactic:
by simp

Goal state after:
Module: Mathlib.Tactic.Algebra.Lemmas

Goal state before:
pp: R : Type u_1
A : Type u_2
sR : CommSemiring R
sA : CommSemiring A
sAlg : Algebra R A
r s : R
h : r + s = 0
⊢ 0 = ↑0

Tactic:
by simp

Goal state after:
Module: Mathlib.Tactic.Algebra.Lemmas

Goal state before:
pp: R : Type u_1
A : Type u_2
sR : CommSemiring R
sA : CommSemiring A
sAlg : Algebra R A
r : R
h : IsNat r 1
⊢ 1 = ↑1

Tactic:
by simp

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

Goal state before:
pp: 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}
⊢ b < ω → (ω ^ e.repr * ↑↑n + a.repr) ^ b ≤ (ω ^ e.repr) ^ ω

Tactic:
l

Goal state after:
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 < ω
⊢ (ω ^ e.repr * ↑↑n + a.repr) ^ b ≤ (ω ^ e.repr) ^ ω
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basis

Goal state before:
pp: basis_hd : ℝ → ℝ
basis_tl : Basis
h : WellFormedBasis (basis_hd :: basis_tl)
⊢ List.Sublist basis_tl (basis_hd :: basis_tl)

Tactic:
by simp

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

Goal state before:
pp: left right : Basis
h : WellFormedBasis (left ++ right)
⊢ List.Sublist right (left ++ right)

Tactic:
by simp

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

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
γ' : Type u_4
s : Stream' (Option α)
hs : ∀ U ∈ nhds s, (U ∩ {x | ∀ {n : ℕ}, x n = none → x (n + 1) = none}).Nonempty
n : ℕ
hn : s n = none
t : Stream' (Option α)
hts : dist t s < (1 / 2) ^ (n + 1)
ht : t ∈ {x | ∀ {n : ℕ}, x n = none → x (n + 1) = none}
⊢ n ≤ n + 1

Tactic:
by simp

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

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

Tactic:
by simp

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

Goal state before:
pp: case nil
α : Type u_1
t : Stream'.Seq α
h : nil.head = t.head
⊢ dist nil t = 2⁻¹ * dist nil.tail t.tail

Tactic:
cases t

Goal state after:
case nil.nil
α : Type u_1
h : nil.head = nil.head
⊢ dist nil nil = 2⁻¹ * dist nil.tail nil.tail

case nil.cons
α : Type u_1
x✝ : α
s✝ : Stream'.Seq α
h : nil.head = (Seq.cons x✝ s✝).head
⊢ dist nil (Seq.cons x✝ s✝) = 2⁻¹ * dist nil.tail (Seq.cons x✝ s✝).tail
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion

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

Tactic:
cases t

Goal state after:
case cons.nil
α : Type u_1
x✝ : α
s✝ : Stream'.Seq α
h : (Seq.cons x✝ s✝).head = nil.head
⊢ dist (Seq.cons x✝ s✝) nil = 2⁻¹ * dist (Seq.cons x✝ s✝).tail nil.tail

case cons.cons
α : Type u_1
x✝¹ : α
s✝¹ : Stream'.Seq α
x✝ : α
s✝ : Stream'.Seq α
h : (Seq.cons x✝¹ s✝¹).head = (Seq.cons x✝ s✝).head
⊢ dist (Seq.cons x✝¹ s✝¹) (Seq.cons x✝ s✝) = 2⁻¹ * dist (Seq.cons x✝¹ s✝¹).tail (Seq.cons x✝ s✝).tail
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion

Goal state before:
pp: case nil
α : Type u_1
t : Stream'.Seq α
h : dist nil t ≤ 2⁻¹
⊢ nil = nil ∧ t = nil ∨ ∃ hd s' t', nil = Seq.cons hd s' ∧ t = Seq.cons hd t'

Tactic:
cases t

Goal state after:
case nil.nil
α : Type u_1
h : dist nil nil ≤ 2⁻¹
⊢ nil = nil ∧ nil = nil ∨ ∃ hd s' t', nil = Seq.cons hd s' ∧ nil = Seq.cons hd t'

case nil.cons
α : Type u_1
x✝ : α
s✝ : Stream'.Seq α
h : dist nil (Seq.cons x✝ s✝) ≤ 2⁻¹
⊢ nil = nil ∧ Seq.cons x✝ s✝ = nil ∨ ∃ hd s' t', nil = Seq.cons hd s' ∧ Seq.cons x✝ s✝ = Seq.cons hd t'
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion

Goal state before:
pp: case cons
α : Type u_1
t : Stream'.Seq α
x✝ : α
s✝ : Stream'.Seq α
h : dist (Seq.cons x✝ s✝) t ≤ 2⁻¹
⊢ Seq.cons x✝ s✝ = nil ∧ t = nil ∨ ∃ hd s' t', Seq.cons x✝ s✝ = Seq.cons hd s' ∧ t = Seq.cons hd t'

Tactic:
cases t

Goal state after:
case cons.nil
α : Type u_1
x✝ : α
s✝ : Stream'.Seq α
h : dist (Seq.cons x✝ s✝) nil ≤ 2⁻¹
⊢ Seq.cons x✝ s✝ = nil ∧ nil = nil ∨ ∃ hd s' t', Seq.cons x✝ s✝ = Seq.cons hd s' ∧ nil = Seq.cons hd t'

case cons.cons
α : Type u_1
x✝¹ : α
s✝¹ : Stream'.Seq α
x✝ : α
s✝ : Stream'.Seq α
h : dist (Seq.cons x✝¹ s✝¹) (Seq.cons x✝ s✝) ≤ 2⁻¹
⊢ Seq.cons x✝¹ s✝¹ = nil ∧ Seq.cons x✝ s✝ = nil ∨
    ∃ hd s' t', Seq.cons x✝¹ s✝¹ = Seq.cons hd s' ∧ Seq.cons x✝ s✝ = Seq.cons hd t'
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion

Goal state before:
pp: α : Type u_1
op₁ op₂ : Stream'.Seq α → Stream'.Seq α
h₁ : ∀ (s t : Stream'.Seq α), dist (op₁ s) (op₁ t) ≤ dist s t
h₂ : ∀ (s t : Stream'.Seq α), dist (op₂ s) (op₂ t) ≤ dist s t
P : Option α → Prop
inst✝ : DecidablePred P
s : Stream'.Seq α
⊢ ∀ (t : Stream'.Seq α), dist (if P s.head then op₁ s else op₂ s) (if P t.head then op₁ t else op₂ t) ≤ dist s t

Tactic:
t

Goal state after:
α : Type u_1
op₁ op₂ : Stream'.Seq α → Stream'.Seq α
h₁ : ∀ (s t : Stream'.Seq α), dist (op₁ s) (op₁ t) ≤ dist s t
h₂ : ∀ (s t : Stream'.Seq α), dist (op₂ s) (op₂ t) ≤ dist s t
P : Option α → Prop
inst✝ : DecidablePred P
s t : Stream'.Seq α
⊢ dist (if P s.head then op₁ s else op₂ s) (if P t.head then op₁ t else op₂ t) ≤ dist s t
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basis

Goal state before:
pp: left right : Basis
f : ℝ → ℝ
h : WellFormedBasis (left ++ right)
hf_tendsto : Tendsto f atTop atTop
hf_comp_left : ∀ (g : ℝ → ℝ), List.getLast? left = some g → (Real.log ∘ f) =o[atTop] (Real.log ∘ g)
hf_comp_right : ∀ (g : ℝ → ℝ), List.head? right = some g → (Real.log ∘ g) =o[atTop] (Real.log ∘ f)
⊢ List.Sublist right (left ++ right)

Tactic:
by simp

Goal state after: