mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation

Goal state before:
pp: case refine_1
A : Type u_1
inst✝ : CommRing A
g : A⟦X⟧
f : A[X]
h : A⟦X⟧
I : Ideal A
H : g.IsWeierstrassFactorizationAt f h I
a : A
ha : IsUnit a
⊢ IsUnit (a • h)

pp: case refine_2
A : Type u_1
inst✝ : CommRing A
g : A⟦X⟧
f : A[X]
h : A⟦X⟧
I : Ideal A
H : g.IsWeierstrassFactorizationAt f h I
a : A
ha : IsUnit a
⊢ a • g = ↑f * a • h

Tactic:
· rw [Algebra.smul_def]
    exact (ha.map _).mul H.isUnit

Goal state after:
case refine_2
A : Type u_1
inst✝ : CommRing A
g : A⟦X⟧
f : A[X]
h : A⟦X⟧
I : Ideal A
H : g.IsWeierstrassFactorizationAt f h I
a : A
ha : IsUnit a
⊢ a • g = ↑f * a • h
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
⊢ 0 - r.coeff i ∈ IsLocalRing.maximalIdeal A

Tactic:
zero_sub,

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
⊢ -r.coeff i ∈ IsLocalRing.maximalIdeal A
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 : 0 - (coeff i) ↑r ∈ IsLocalRing.maximalIdeal A
⊢ r.coeff i ∈ IsLocalRing.maximalIdeal A

Tactic:
zero_sub,

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 : -(coeff i) ↑r ∈ IsLocalRing.maximalIdeal A
⊢ r.coeff i ∈ IsLocalRing.maximalIdeal A
Module: Mathlib.RingTheory.SimpleModule.Isotypic

Goal state before:
pp: R₀ : Type u_1
R : Type u_2
M : Type u
N : Type u_3
S : Type u_4
inst✝⁹ : CommSemiring R₀
inst✝⁸ : Ring R
inst✝⁷ : Algebra R₀ R
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup N
inst✝⁴ : AddCommGroup S
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module R S
inst✝ : IsSemisimpleModule R S
⊢ IsSemisimpleModule R ↥(sSup {m | Nonempty (↥m ≃ₗ[R] S)})

Tactic:
sSup_eq_iSup

Goal state after:
R₀ : Type u_1
R : Type u_2
M : Type u
N : Type u_3
S : Type u_4
inst✝⁹ : CommSemiring R₀
inst✝⁸ : Ring R
inst✝⁷ : Algebra R₀ R
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup N
inst✝⁴ : AddCommGroup S
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module R S
inst✝ : IsSemisimpleModule R S
⊢ IsSemisimpleModule R ↥(⨆ a ∈ {m | Nonempty (↥m ≃ₗ[R] S)}, a)
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
N : Submodule R M
inst✝ : IsSimpleModule R ↥N
s : Set (Submodule R M)
hs : ∀ (m : ↑s), IsSemisimpleModule R ↥↑m
hN : N ≤ sSup s
⊢ ∃ m ∈ s, ∃ S ≤ m, Nonempty (↥N ≃ₗ[R] ↥S)

Tactic:
sSup_eq_iSup

Goal state after:
R : Type u_2
M : Type u
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
N : Submodule R M
inst✝ : IsSimpleModule R ↥N
s : Set (Submodule R M)
hs : ∀ (m : ↑s), IsSemisimpleModule R ↥↑m
hN : N ≤ ⨆ a ∈ s, a
⊢ ∃ m ∈ s, ∃ S ≤ m, Nonempty (↥N ≃ₗ[R] ↥S)
Module: Mathlib.RingTheory.SimpleModule.WedderburnArtin

Goal state before:
pp: case refine_1
R : Type u
inst✝ : Ring R
x✝ : IsSimpleRing R ∧ IsArtinianRing R
left✝ : IsSimpleRing R
right✝ : IsArtinianRing R
⊢ IsSemisimpleRing R ∧ IsIsotypic R R ∧ Nontrivial R

Tactic:
have := IsSimpleRing.isSemisimpleRing_iff_isArtinianRing.mpr ‹_›

Goal state after:
case refine_1
R : Type u
inst✝ : Ring R
x✝ : IsSimpleRing R ∧ IsArtinianRing R
left✝ : IsSimpleRing R
right✝ : IsArtinianRing R
this : IsSemisimpleRing R
⊢ IsSemisimpleRing R ∧ IsIsotypic R R ∧ Nontrivial R
Module: Mathlib.RingTheory.SimpleModule.WedderburnArtin

Goal state before:
pp: R₀ : Type u_1
R : Type u
inst✝⁵ : CommSemiring R₀
inst✝⁴ : Ring R
inst✝³ : Algebra R₀ R
inst✝² : IsSimpleRing R
inst✝¹ : IsArtinianRing R
inst✝ : Module.Finite R₀ R
n : ℕ
hn : NeZero n
I : Ideal R
w✝ : IsSimpleModule R ↥I
e : R ≃ₐ[R₀] Matrix (Fin n) (Fin n) (Module.End R ↥I)ᵐᵒᵖ
⊢ ∃ n, ∃ (_ : NeZero n), ∃ D x x_1, ∃ (_ : Module.Finite R₀ D), Nonempty (R ≃ₐ[R₀] Matrix (Fin n) (Fin n) D)

Tactic:
have := Module.Finite.equiv e.toLinearEquiv

Goal state after:
R₀ : Type u_1
R : Type u
inst✝⁵ : CommSemiring R₀
inst✝⁴ : Ring R
inst✝³ : Algebra R₀ R
inst✝² : IsSimpleRing R
inst✝¹ : IsArtinianRing R
inst✝ : Module.Finite R₀ R
n : ℕ
hn : NeZero n
I : Ideal R
w✝ : IsSimpleModule R ↥I
e : R ≃ₐ[R₀] Matrix (Fin n) (Fin n) (Module.End R ↥I)ᵐᵒᵖ
this : Module.Finite R₀ (Matrix (Fin n) (Fin n) (Module.End R ↥I)ᵐᵒᵖ)
⊢ ∃ n, ∃ (_ : NeZero n), ∃ D x x_1, ∃ (_ : Module.Finite R₀ D), Nonempty (R ≃ₐ[R₀] Matrix (Fin n) (Fin n) D)
Module: Mathlib.RingTheory.SimpleModule.WedderburnArtin

Goal state before:
pp: R₀ : Type u_1
R : Type u
inst✝⁴ : CommSemiring R₀
inst✝³ : Ring R
inst✝² : Algebra R₀ R
inst✝¹ : IsSemisimpleRing R
inst✝ : Module.Finite R₀ R
n : ℕ
D : Fin n → Type u
d : Fin n → ℕ
w✝¹ : (i : Fin n) → DivisionRing (D i)
w✝ : (i : Fin n) → Algebra R₀ (D i)
hd : ∀ (i : Fin n), NeZero (d i)
e : R ≃ₐ[R₀] (i : Fin n) → Matrix (Fin (d i)) (Fin (d i)) (D i)
⊢ ∃ n D d x x_1,
    ∃ (_ : ∀ (i : Fin n), Module.Finite R₀ (D i)),
      (∀ (i : Fin n), NeZero (d i)) ∧ Nonempty (R ≃ₐ[R₀] (i : Fin n) → Matrix (Fin (d i)) (Fin (d i)) (D i))

Tactic:
have := Module.Finite.equiv e.toLinearEquiv

Goal state after:
R₀ : Type u_1
R : Type u
inst✝⁴ : CommSemiring R₀
inst✝³ : Ring R
inst✝² : Algebra R₀ R
inst✝¹ : IsSemisimpleRing R
inst✝ : Module.Finite R₀ R
n : ℕ
D : Fin n → Type u
d : Fin n → ℕ
w✝¹ : (i : Fin n) → DivisionRing (D i)
w✝ : (i : Fin n) → Algebra R₀ (D i)
hd : ∀ (i : Fin n), NeZero (d i)
e : R ≃ₐ[R₀] (i : Fin n) → Matrix (Fin (d i)) (Fin (d i)) (D i)
this : Module.Finite R₀ ((i : Fin n) → Matrix (Fin (d i)) (Fin (d i)) (D i))
⊢ ∃ n D d x x_1,
    ∃ (_ : ∀ (i : Fin n), Module.Finite R₀ (D i)),
      (∀ (i : Fin n), NeZero (d i)) ∧ Nonempty (R ≃ₐ[R₀] (i : Fin n) → Matrix (Fin (d i)) (Fin (d i)) (D i))
Module: Mathlib.RingTheory.Spectrum.Prime.IsOpenComapC

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
f : R[X]
⊢ IsOpen (imageOfDf f)

Tactic:
imageOfDf,

Goal state after:
R : Type u_1
inst✝ : CommRing R
f : R[X]
⊢ IsOpen {p | ∃ i, f.coeff i ∉ p.asIdeal}
Module: Mathlib.RingTheory.TwoSidedIdeal.BigOperators

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
I : TwoSidedIdeal R
ι : Type u_2
l : List ι
f : ι → R
hl : ∃ x ∈ l, f x ∈ I
⊢ (List.map f l).prod ∈ I

Tactic:
by
  induction l with
  | nil => simp only [List.not_mem_nil, false_and, exists_false] at hl
  | cons x l ih =>
    simp only [List.mem_cons, exists_eq_or_imp] at hl
    rcases hl with h | hal
    · simpa only [List.map_cons, List.prod_cons] using I.mul_mem_right _ _ h
    · simpa only [List.map_cons, List.prod_cons] using I.mul_mem_left _ _ <| ih hal

Goal state after:
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Moebius

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a : α
ha : IsUnit a
⊢ moebius 1 = 1

Tactic:
moebius_one

Goal state after:
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a : α
ha : IsUnit a
⊢ 1 = 1
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Moebius

Goal state before:
pp: case inl
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a b : α
h : IsRelPrime a b
h✝ : Subsingleton α
⊢ moebius (1 * b) = 1 * moebius b

Tactic:
one_mul,

Goal state after:
case inl
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a b : α
h : IsRelPrime a b
h✝ : Subsingleton α
⊢ moebius b = 1 * moebius b
Module: Mathlib.RingTheory.Valuation.Minpoly

Goal state before:
pp: K : Type u_1
inst✝³ : Field K
Γ₀ : Type u_2
inst✝² : LinearOrderedCommGroupWithZero Γ₀
v : Valuation K Γ₀
L : Type u_3
inst✝¹ : Field L
inst✝ : Algebra K L
x : K
⊢ v (0 - x) = v x

Tactic:
zero_sub,

Goal state after:
K : Type u_1
inst✝³ : Field K
Γ₀ : Type u_2
inst✝² : LinearOrderedCommGroupWithZero Γ₀
v : Valuation K Γ₀
L : Type u_3
inst✝¹ : Field L
inst✝ : Algebra K L
x : K
⊢ v (-x) = v x
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 : i ≠ n
⊢ ↑p ^ i ≠ 0

Tactic:
replace hin := lt_of_le_of_ne hin hpi

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : CharP R p
i : ℕ
hpi : i ≠ n
hin : i < n
⊢ ↑p ^ i ≠ 0
Module: Mathlib.RingTheory.WittVector.DiscreteValuationRing

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
a : 𝕎 k
ha : a ≠ 0
m : ℕ
b : 𝕎 k
hc : b.coeff 0 ^ p ^ m ≠ 0
hcm : a = (⇑verschiebung ∘ ⇑frobenius)^[m] b
this : (⇑verschiebung ∘ ⇑frobenius)^[m] b = (⇑verschiebung)^[m] ((⇑frobenius)^[m] b)
x : 𝕎 k
⊢ ↑p * x = (⇑verschiebung ∘ ⇑frobenius) x

Tactic:
mul_comm,

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : CommRing k
inst✝¹ : CharP k p
inst✝ : PerfectRing k p
a : 𝕎 k
ha : a ≠ 0
m : ℕ
b : 𝕎 k
hc : b.coeff 0 ^ p ^ m ≠ 0
hcm : a = (⇑verschiebung ∘ ⇑frobenius)^[m] b
this : (⇑verschiebung ∘ ⇑frobenius)^[m] b = (⇑verschiebung)^[m] ((⇑frobenius)^[m] b)
x : 𝕎 k
⊢ x * ↑p = (⇑verschiebung ∘ ⇑frobenius) x
Module: Mathlib.RingTheory.WittVector.MulCoeff

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : CommRing k
inst✝ : CharP k p
n : ℕ
x y : 𝕎 k
this : ↑p = 0
⊢ (x * y).coeff (n + 1) + ↑p ^ (n + 1) * x.coeff (n + 1) * y.coeff (n + 1) -
        y.coeff (n + 1) * ∑ i ∈ range (n + 1 + 1), ↑p ^ i * x.coeff i ^ p ^ (n + 1 - i) -
      x.coeff (n + 1) * ∑ i ∈ range (n + 1 + 1), ↑p ^ i * y.coeff i ^ p ^ (n + 1 - i) =
    (x * y).coeff (n + 1) - y.coeff (n + 1) * x.coeff 0 ^ p ^ (n + 1) - x.coeff (n + 1) * y.coeff 0 ^ p ^ (n + 1)

Tactic:
simp only [this, ne_eq, add_eq_zero, and_false, zero_pow, zero_mul, add_zero,
    not_false_eq_true, reduceCtorEq]

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : CommRing k
inst✝ : CharP k p
n : ℕ
x y : 𝕎 k
this : ↑p = 0
⊢ (x * y).coeff (n + 1) - y.coeff (n + 1) * ∑ x_1 ∈ range (n + 1 + 1), 0 ^ x_1 * x.coeff x_1 ^ p ^ (n + 1 - x_1) -
      x.coeff (n + 1) * ∑ x ∈ range (n + 1 + 1), 0 ^ x * y.coeff x ^ p ^ (n + 1 - x) =
    (x * y).coeff (n + 1) - y.coeff (n + 1) * x.coeff 0 ^ p ^ (n + 1) - x.coeff (n + 1) * y.coeff 0 ^ p ^ (n + 1)
Module: Mathlib.SetTheory.Cardinal.Cofinality.Club

Goal state before:
pp: case inr.inr
α : Type v
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
s : Set (Set α)
hα✝ : cof α ≠ ℵ₀
hsα : #↑s < cof α
hs : ∀ x ∈ s, IsClub x
h✝ : Nonempty α
hα : ℵ₀ < cof α
a : α
f : ↑s → α → α
hf : ∀ (x : ↑s) (x_1 : α), f x x_1 ∈ ↑x ∧ x_1 ≤ f x x_1
⊢ ∃ y ∈ ⋂₀ s, a ≤ y

Tactic:
let g : ℕ → α := Nat.rec a fun _ IH ↦ sSup (.range (f · IH))

Goal state after:
case inr.inr
α : Type v
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
s : Set (Set α)
hα✝ : cof α ≠ ℵ₀
hsα : #↑s < cof α
hs : ∀ x ∈ s, IsClub x
h✝ : Nonempty α
hα : ℵ₀ < cof α
a : α
f : ↑s → α → α
hf : ∀ (x : ↑s) (x_1 : α), f x x_1 ∈ ↑x ∧ x_1 ≤ f x x_1
g : ℕ → α := fun t ↦ Nat.rec a (fun x IH ↦ sSup (range fun x ↦ f x IH)) t
⊢ ∃ y ∈ ⋂₀ s, a ≤ y
Module: Mathlib.SetTheory.Cardinal.Cofinality.Club

Goal state before:
pp: α : Type v
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
ι : Type u
f : ι → Set α
hα : cof α ≠ ℵ₀
hι : lift.{v, u} #ι < lift.{u, v} (cof α)
hf : ∀ (i : ι), IsClub (f i)
⊢ IsClub (⋂₀ range f)

Tactic:
refine IsClub.sInter hα ?_ (by simpa)

Goal state after:
α : Type v
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
ι : Type u
f : ι → Set α
hα : cof α ≠ ℵ₀
hι : lift.{v, u} #ι < lift.{u, v} (cof α)
hf : ∀ (i : ι), IsClub (f i)
⊢ #↑(range f) < cof α
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₁
⊢ ∃ o n₁ n₂, o * ↑n₁ = o₁ ∧ o * ↑n₂ = o₂

Tactic:
have hsub : o₁ + o₃ = o₂ := Ordinal.add_sub_cancel_of_le hle

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₂
⊢ ∃ 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 b : Ordinal.{u}
hab : a ≤ b
hf : lfpApprox f x a ∈ fixedPoints ⇑f
⊢ lfpApprox f x b = lfpApprox f x a

Tactic:
mem_fixedPoints_iff

Goal state after:
α : Type u
inst✝ : CompleteLattice α
f : α →o α
x : α
a b : Ordinal.{u}
hab : a ≤ b
hf : f (lfpApprox f x a) = lfpApprox f x a
⊢ lfpApprox f x b = lfpApprox f x a
Module: Mathlib.SetTheory.Ordinal.FixedPointApproximants

Goal state before:
pp: α : Type u
inst✝ : CompleteLattice α
f : α →o α
x : α
a : Ordinal.{u}
hf : lfpApprox f x a ∈ fixedPoints ⇑f
⊢ ⨆ i, lfpApprox f x i = lfpApprox f x a

Tactic:
apply (le_iSup (lfpApprox f x) a).antisymm'

Goal state after:
α : Type u
inst✝ : CompleteLattice α
f : α →o α
x : α
a : Ordinal.{u}
hf : lfpApprox f x a ∈ fixedPoints ⇑f
⊢ iSup (lfpApprox f x) ≤ lfpApprox f x a
Module: Mathlib.SetTheory.Ordinal.Notation

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

Tactic:
by injection h

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

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

Tactic:
by injection h

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

Goal state before:
pp: 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}}, (∀ (e' : Ordinal.{u_1}), f e' < b) → (∀ e' ∈ f.support, e' < e) → eval b f < b ^ e
e : Ordinal.{u_1}
hb : ∀ (e'_1 : Ordinal.{u_1}), (single e' x + f) e'_1 < b
he : ∀ e'_1 ∈ (single e' x + f).support, e'_1 < e
he' : e' ∉ f.support
⊢ ∀ (e' : Ordinal.{u_1}), f e' < b

Tactic:
· intro a
      by_cases ha : a ∈ f.support
      · apply (hb a).trans_eq'
        rw [add_apply, single_eq_of_ne, zero_add]
        rintro rfl
        contradiction
      · rw [notMem_support_iff.1 ha]
        exact (hb 0).pos

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

Goal state before:
pp: S : Set Ordinal.{u_1}
o : Ordinal.{u_1}
⊢ IsClosedBelow S o ↔ ∀ p < o, p.IsAcc S → p ∈ S

Tactic:
simp [IsClosedBelow, IsAcc, isClosed_iff_accPt, ← comap_principal,
    isOpen_Iio.isOpenEmbedding_subtypeVal.accPt_comap_iff]

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

Goal state before:
pp: b : Ordinal.{0}
e : ONote
n : ℕ+
a : ONote
h✝ : (e.oadd n a).NF
d : ω ^ b ∣ (e.oadd n a).repr
h : e.oadd n a = 0
⊢ False

Tactic:
by injection h

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

Goal state before:
pp: f : Ordinal.{u} → Ordinal.{u}
o₁ o₂ a : Ordinal.{u}
hf : IsNormal f
h : o₁ ≤ o₂
h' : veblenWith f o₂ a = a
⊢ veblenWith f o₁ a = a

Tactic:
obtain rfl | h := h.eq_or_lt
  · assumption
  · rw [← h', veblenWith_veblenWith_of_lt hf h]

Goal state after:
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
this✝ : e.NF
this : e'.NF
ee : (e.cmp e').Compares e e'
⊢ (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:
cases he : cmp e e' <;> simp only [he, Ordering.compares_gt, Ordering.compares_lt,
        Ordering.compares_eq, repr, gt_iff_lt, PNat.add_coe, Nat.cast_add] at ee ⊢

Goal state after:
case oadd.lt
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
this : e'.NF
he : e.cmp e' = Ordering.lt
ee : e < e'
⊢ ω ^ e'.repr * ↑↑n' + a'.repr = ω ^ e.repr * ↑↑n + (ω ^ e'.repr * ↑↑n' + a'.repr)

case oadd.eq
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
this : e'.NF
he : e.cmp e' = Ordering.eq
ee : e = e'
⊢ ω ^ e.repr * (↑↑n + ↑↑n') + a'.repr = ω ^ e.repr * ↑↑n + (ω ^ e'.repr * ↑↑n' + a'.repr)
Module: Mathlib.SetTheory.Ordinal.Veblen

Goal state before:
pp: case h
o a : Ordinal.{u}
ho : o ≠ 0
h : a < veblen o a
⊢ 0 < o

Tactic:
exact ho.bot_lt

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

Goal state before:
pp: o : Ordinal.{u_1}
⊢ ω < ε_ o

Tactic:
by
  apply lt_of_lt_of_le _ <| (veblen_right_strictMono _).monotone zero_le
  simpa using iterate_omega0_opow_lt_epsilon_zero 2

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

Goal state before:
pp: x : Class.{u}
z : ZFSet.{u}
hz : z ∈ x
y : ZFSet.{u}
right✝ : ↑z y
H : ∀ z ∈ x, ↑y ∈ z
w : ZFSet.{u}
hxw : x w
⊢ y ∈ w

Tactic:
simpa only [coe_mem, coe_apply] using H w (coe_mem.2 hxw)

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

Goal state before:
pp: e a0 a : ONote
inst✝² : e.NF
inst✝¹ : a0.NF
inst✝ : a.NF
k m : ℕ
⊢ (match k, m with
    | x, 0 => 0
    | 0, m.succ => e.oadd m.succPNat 0
    | k.succ, m => (e + a0.mulNat k).scale a + e.opowAux a0 a k m).NF

Tactic:
cases m with
  | zero => cases k <;> exact NF.zero
  | succ m =>
    cases k with
    | zero => exact NF.oadd_zero _ _
    | succ k =>
      have := nf_opowAux e a0 a k
      simp only [mulNat_eq_mul]; infer_instance

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

Goal state before:
pp: α : Type u_1
s t : Stream'.Seq α
h : s.head ≠ t.head
⊢ dist s t = 1

Tactic:
rw [Subtype.dist_eq, PiNat.dist_eq_of_ne]
  · convert! pow_zero _
    simp only [PiNat.firstDiff, ne_eq, Classical.dite_not, dite_eq_left_iff,
      Nat.find_eq_zero]
    intro h'
    simpa [Stream'.cons]
  · rw [Subtype.coe_ne_coe]
    contrapose h
    simp [h]

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

Goal state before:
pp: case none
α : 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 : β
⊢ dist
      (match none with
      | none => nil
      | some (a, c, b') => Seq.cons a (op c (f b')))
      (match none with
      | none => nil
      | some (a, c, b') => Seq.cons a (op c (g b'))) ≤
    2⁻¹ * dist f g

Tactic:
| none =>

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 α
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' : β
this : FriendlyOperation (op c)
⊢ dist (op c (f b')) (op c (g b')) ≤ dist (f b') (g b')

Tactic:
rw [FriendlyOperation, lipschitzWith_iff_dist_le_mul] at this

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' : β
this : ∀ (x y : Stream'.Seq α), dist (op c x) (op c y) ≤ ↑1 * dist x y
⊢ dist (op c (f b')) (op c (g b')) ≤ dist (f b') (g b')
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion

Goal state before:
pp: case h.none
α : 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'))
hT : LipschitzWith 2⁻¹ T
f : β → Stream'.Seq α
hf : Function.IsFixedPt T f
b : β
hb : F b = none
⊢ match none with
  | none =>
    (match none with
      | none => nil
      | some (a, c, b') => Seq.cons a (op c (f b'))) =
      nil
  | some (a, c, b') =>
    (match none with
      | none => nil
      | some (a, c, b') => Seq.cons a (op c (f b'))) =
      Seq.cons a
        (op c
          (match F b' with
          | none => nil
          | some (a, c, b') => Seq.cons a (op c (f b'))))

Tactic:
| none =>

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

Goal state before:
pp: case hl
f g : ℝ → ℝ
a b : ℝ
hf✝ : ∀ᶠ (x : ℝ) in atTop, 0 < f x
hg✝ : Tendsto g atTop atTop
h : (Real.log ∘ f) =o[atTop] (Real.log ∘ g)
hb : 0 < b
x : ℝ
x✝ : 0 < f x ∧ 0 < g x
hf : 0 < f x
hg : 0 < g x
⊢ (Real.exp ∘ (b • Real.log ∘ g - a • Real.log ∘ f)) x = (fun x ↦ (g ^ b) x / (f ^ a) x) x

Tactic:
simp [Real.exp_sub, mul_comm a, mul_comm b, Real.exp_mul, Real.exp_log hg, Real.exp_log hf]

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

Goal state before:
pp: case zero.zero
o₁ o₂ : ONote
inst✝¹ : o₁.NF
inst✝ : o₂.NF
N₁ : zero.NF
e₁ : o₁.split = (zero, 0)
r₁ : o₁.repr = zero.repr + ↑0
⊢ (o₁ ^ o₂).repr = o₁.repr ^ o₂.repr

Tactic:
have hzero : (0 : ONote) = zero := rfl
      by_cases h : o₂ = 0
      · subst h; simp [-zero_def, opow_def, opowAux2, e₁, r₁, hzero]
      · have h' := mt repr_inj.1 h
        have hne : o₂ ≠ zero := fun he => h (he ▸ rfl)
        simp [-zero_def, opow_def, opowAux2, e₁, r₁, hne, hzero]
        exact (zero_opow h').symm

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

Goal state before:
pp: case cons
α : Type u_1
op : Stream'.Seq α → Stream'.Seq α
h : FriendlyOperation op
s_hd : α
s_tl : Stream'.Seq α
⊢ (op (Seq.cons s_hd s_tl)).destruct =
    Option.map
      (fun x ↦
        match x with
        | (hd, op') => (hd, ↑op' (Seq.cons s_hd s_tl).tail))
      (match (Seq.cons s_hd s_tl).head with
      | none =>
        match (op nil).destruct with
        | none => none
        | some (t_hd, t_tl) => some (t_hd, ⟨fun x ↦ t_tl, ⋯⟩)
      | some s_hd =>
        match (op (Seq.cons s_hd nil)).destruct with
        | none => none
        | some (t_hd, snd) => some (t_hd, ⟨fun s_tl ↦ (op (Seq.cons s_hd s_tl)).tail, ⋯⟩))

Tactic:
| cons s_hd s_tl =>

Goal state after: