mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Polynomial.HilbertPoly

Goal state before:
pp: F : Type u_1
inst✝¹ : Field F
inst✝ : CharZero F
p : F[X]
d n : ℕ
hn : p.natDegree < n
⊢ (PowerSeries.coeff n) (↑p * ↑(invOneSubPow F d)) =
    eval (↑n)
      (match d with
      | 0 => 0
      | d.succ => ∑ i ∈ p.support, p.coeff i • preHilbertPoly F d i)

Tactic:
induction d with
  | zero => simp only [invOneSubPow_zero, Units.val_one, mul_one, coeff_coe, eval_zero]
            exact coeff_eq_zero_of_natDegree_lt hn
  | succ d hd =>
      simp only [eval_finsetSum, eval_smul, smul_eq_mul]
      rw [← Finset.sum_coe_sort]
      have h_le (i : p.support) : (i : ℕ) ≤ n :=
        le_trans (le_natDegree_of_ne_zero <| mem_support_iff.1 i.2) hn.le
      have h (i : p.support) : eval ↑n (preHilbertPoly F d ↑i) = (n + d - ↑i).choose d := by
        rw [preHilbertPoly_eq_choose_sub_add _ _ (h_le i), Nat.sub_add_comm (h_le i)]
      simp_rw [h]
      rw [Finset.sum_coe_sort _ (fun x => (p.coeff ↑x) * (_ + d - ↑x).choose _),
        PowerSeries.coeff_mul, Finset.Nat.sum_antidiagonal_eq_sum_range_succ_mk,
        invOneSubPow_val_eq_mk_sub_one_add_choose_of_pos _ _ (zero_lt_succ d)]
      simp only [coeff_coe, coeff_mk]
      symm
      refine Finset.sum_subset_zero_on_sdiff (fun s hs ↦ ?_) (fun x hx ↦ ?_) (fun x hx ↦ ?_)
      · rw [Finset.mem_range_succ_iff]
        exact h_le ⟨s, hs⟩
      · simp only [Finset.mem_sdiff, mem_support_iff, not_not] at hx
        rw [hx.2, zero_mul]
      · rw [add_comm, Nat.add_sub_assoc (h_le ⟨x, hx⟩), succ_eq_add_one, add_tsub_cancel_right]

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

Goal state before:
pp: ⊢ (coeff 0) catalanSeries = 1

Tactic:
simp only [catalanSeries_coeff, catalan_zero]

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

Goal state before:
pp: R : Type u_2
inst✝ : CommRing R
p : ℕ
hp : p ≠ 0
φ : R⟦X⟧
⊢ ((expand p hp) φ).order = p • φ.order

Tactic:
by
  simp_rw [expand, order_eq_order, MvPowerSeries.order_expand p hp φ]

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

Goal state before:
pp: n : ℕ
hn : ¬n = 0
⊢ 0 < n

Tactic:
omega

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

Goal state before:
pp: n : ℕ
hn : ¬n = 0
hn' : 0 < n
⊢ n = n - 1 + 1

Tactic:
omega

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

Goal state before:
pp: A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n : ℕ
this : ↑n + 1 = (algebraMap ℚ A) (↑n + 1)
⊢ (coeff n) ((d⁄dX A) (log A)) = (coeff n) (mk fun n ↦ (algebraMap ℚ A) ((-1) ^ n))

Tactic:
coeff_derivative,

Goal state after:
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n : ℕ
this : ↑n + 1 = (algebraMap ℚ A) (↑n + 1)
⊢ (coeff (n + 1)) (log A) * (↑n + 1) = (coeff n) (mk fun n ↦ (algebraMap ℚ A) ((-1) ^ n))
Module: Mathlib.RingTheory.PolynomialLaw.Basic

Goal state before:
pp: R : Type u
inst✝⁶ : CommSemiring R
M : Type u_1
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
N : Type u_2
inst✝³ : AddCommMonoid N
inst✝² : Module R N
S : Type v
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
f : M →ₚₗ[R] N
s : Finset S
p : MvPolynomial (Fin s.card) R ⊗[R] M
s' : Finset S
p' : MvPolynomial (Fin s'.card) R ⊗[R] M
h : π R M S ⟨s, p⟩ = π R M S ⟨s', p'⟩
u : ↥(φ R s).range ⊗[R] M := (rTensor M (φ R s).rangeRestrict.toLinearMap) p
hu : u = (rTensor M (φ R s).rangeRestrict.toLinearMap) p
⊢ (rTensor N (φ R s).toLinearMap) (f.toFun' (MvPolynomial (Fin s.card) R) p) =
    (rTensor N (φ R s').toLinearMap) (f.toFun' (MvPolynomial (Fin s'.card) R) p')

Tactic:
have uFG : Subalgebra.FG (R := R) (φ R s).range := by
    rw [← Algebra.map_top]
    exact Subalgebra.FG.map _ Algebra.FiniteType.out

Goal state after:
R : Type u
inst✝⁶ : CommSemiring R
M : Type u_1
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
N : Type u_2
inst✝³ : AddCommMonoid N
inst✝² : Module R N
S : Type v
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
f : M →ₚₗ[R] N
s : Finset S
p : MvPolynomial (Fin s.card) R ⊗[R] M
s' : Finset S
p' : MvPolynomial (Fin s'.card) R ⊗[R] M
h : π R M S ⟨s, p⟩ = π R M S ⟨s', p'⟩
u : ↥(φ R s).range ⊗[R] M := (rTensor M (φ R s).rangeRestrict.toLinearMap) p
hu : u = (rTensor M (φ R s).rangeRestrict.toLinearMap) p
uFG : (φ R s).range.FG
⊢ (rTensor N (φ R s).toLinearMap) (f.toFun' (MvPolynomial (Fin s.card) R) p) =
    (rTensor N (φ R s').toLinearMap) (f.toFun' (MvPolynomial (Fin s'.card) R) p')
Module: Mathlib.RingTheory.RegularLocalRing.Polynomial

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsRegularLocalRing R
p : Ideal R[X]
inst✝ : p.IsPrime
max : comap C p = maximalIdeal R
q : Ideal R[X] := Ideal.map C (maximalIdeal R)
qle : q ≤ p
reg : ↑(Submodule.spanFinrank (maximalIdeal R)) = ringKrullDim R
fg' : (maximalIdeal R).FG
fg : (Submodule.generators (maximalIdeal R)).Finite
ht : (maximalIdeal R).height ≤ q.height
eq : p = q
ht1 : (maximalIdeal R).height ≤ p.height
⊢ span (⇑(algebraMap R[X] (Localization.AtPrime p)) ∘ ⇑(algebraMap R R[X]) '' Submodule.generators (maximalIdeal R)) =
    maximalIdeal (Localization.AtPrime p)

Tactic:
Set.image_comp,

Goal state after:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsRegularLocalRing R
p : Ideal R[X]
inst✝ : p.IsPrime
max : comap C p = maximalIdeal R
q : Ideal R[X] := Ideal.map C (maximalIdeal R)
qle : q ≤ p
reg : ↑(Submodule.spanFinrank (maximalIdeal R)) = ringKrullDim R
fg' : (maximalIdeal R).FG
fg : (Submodule.generators (maximalIdeal R)).Finite
ht : (maximalIdeal R).height ≤ q.height
eq : p = q
ht1 : (maximalIdeal R).height ≤ p.height
⊢ span (⇑(algebraMap R[X] (Localization.AtPrime p)) '' ⇑(algebraMap R R[X]) '' Submodule.generators (maximalIdeal R)) =
    maximalIdeal (Localization.AtPrime p)
Module: Mathlib.RingTheory.Regular.ProjectiveDimension

Goal state before:
pp: R : Type u
inst✝³ : CommRing R
inst✝² : Small.{v, u} R
inst✝¹ : IsLocalRing R
inst✝ : IsNoetherianRing R
rs : List R
reg : RingTheory.Sequence.IsRegular R rs
mem_max : ∀ x ∈ rs, x ∈ maximalIdeal R
e : Shrink.{v, u} (R ⧸ Ideal.ofList rs) ≃ₗ[R] Shrink.{v, u} R ⧸ Ideal.ofList rs • ⊤ :=
  Shrink.linearEquiv R (R ⧸ Ideal.ofList rs) ≪≫ₗ
    Submodule.Quotient.equiv (Ideal.ofList rs) (Ideal.ofList rs • ⊤) (Shrink.linearEquiv R R).symm ⋯
⊢ 0 + ↑rs.length = ↑rs.length

Tactic:
zero_add

Goal state after:
R : Type u
inst✝³ : CommRing R
inst✝² : Small.{v, u} R
inst✝¹ : IsLocalRing R
inst✝ : IsNoetherianRing R
rs : List R
reg : RingTheory.Sequence.IsRegular R rs
mem_max : ∀ x ∈ rs, x ∈ maximalIdeal R
e : Shrink.{v, u} (R ⧸ Ideal.ofList rs) ≃ₗ[R] Shrink.{v, u} R ⧸ Ideal.ofList rs • ⊤ :=
  Shrink.linearEquiv R (R ⧸ Ideal.ofList rs) ≪≫ₗ
    Submodule.Quotient.equiv (Ideal.ofList rs) (Ideal.ofList rs • ⊤) (Shrink.linearEquiv R R).symm ⋯
⊢ ↑rs.length = ↑rs.length
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Moebius

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

Tactic:
rcases subsingleton_or_nontrivial α
  · rw [Subsingleton.elim a 1, moebius_one, one_mul, one_mul]
  by_cases ha : Squarefree a; swap
  · simp [ha, mt Squarefree.of_mul_left ha]
  by_cases hb : Squarefree b; swap
  · simp [hb, mt Squarefree.of_mul_right hb]
  have hab : Squarefree (a * b) := squarefree_mul_iff.mpr ⟨h, ha, hb⟩
  rw [hab.moebius_eq, Multiset.card_eq_card_of_rel (factors_mul ha.ne_zero hb.ne_zero),
    Multiset.card_add, pow_add, ha.moebius_eq, hb.moebius_eq]

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

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

Tactic:
by simp only [Subalgebra.coe_mul, map_mul]

Goal state after:
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
inst✝ : FiniteDimensional K L
x : L
hx : IsUnit x
h_alg : Algebra.IsAlgebraic K L
hx₀ : IsIntegral K x
hdeg : 0 < finrank K L / (minpoly K x).natDegree
⊢ ¬v ((minpoly K x).coeff 0) = 0

Tactic:
Valuation.zero_iff

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
inst✝ : FiniteDimensional K L
x : L
hx : IsUnit x
h_alg : Algebra.IsAlgebraic K L
hx₀ : IsIntegral K x
hdeg : 0 < finrank K L / (minpoly K x).natDegree
⊢ ¬(minpoly K x).coeff 0 = 0
Module: Mathlib.RingTheory.WittVector.DiscreteValuationRing

Goal state before:
pp: p : ℕ
hp✝ : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : Field k
inst✝ : CharP k p
hp : ¬IsUnit ↑p
a b : 𝕎 k
hab : ↑p = a * b
⊢ IsUnit a ∨ IsUnit b

Tactic:
obtain ⟨ha0, hb0⟩ : a ≠ 0 ∧ b ≠ 0 := by
    rw [← mul_ne_zero_iff]; intro h; rw [h] at hab; exact p_nonzero p k hab

Goal state after:
p : ℕ
hp✝ : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : Field k
inst✝ : CharP k p
hp : ¬IsUnit ↑p
a b : 𝕎 k
hab : ↑p = a * b
ha0 : a ≠ 0
hb0 : b ≠ 0
⊢ IsUnit a ∨ IsUnit b
Module: Mathlib.RingTheory.WittVector.MulCoeff

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
n i : ℕ
m✝ : Fin 2 × ℕ →₀ ℕ
⊢ ¬p ^ (n - i) = 0

Tactic:
exact pow_ne_zero _ hp.out.ne_zero

Goal state after:
Module: Mathlib.SetTheory.Cardinal.EventuallyConst

Goal state before:
pp: α : Type u
β : Type v
inst✝² : LinearOrder α
inst✝¹ : PartialOrder β
f : α → β
inst✝ : Nonempty α
hf : Monotone f
hf' : ¬IsCofinal (range (rangeSplitting f))
⊢ EventuallyConst f atTop

Tactic:
by
  rw [eventuallyConst_atTop]
  obtain ⟨i, hi⟩ := not_isCofinal_iff.1 hf'
  refine ⟨i, fun j hij ↦ (hf hij).antisymm' <| (hf (hi _ ⟨⟨f j, j, rfl⟩, rfl⟩).le).trans' ?_⟩
  rw [apply_rangeSplitting f]

Goal state after:
Module: Mathlib.SetTheory.Cardinal.UnivLE

Goal state before:
pp: ⊢ UnivLE.{u, v} ↔ Nonempty (Ordinal.{u} ↪ Ordinal.{v})

Tactic:
univLE_iff_cardinal_le

Goal state after:
⊢ univ.{u, v + 1} ≤ univ.{v, u + 1} ↔ Nonempty (Ordinal.{u} ↪ Ordinal.{v})
Module: Mathlib.SetTheory.Cardinal.UnivLE

Goal state before:
pp: ⊢ UnivLE.{u, v} ∨ UnivLE.{v, u}

Tactic:
univLE_iff_cardinal_le

Goal state after:
⊢ univ.{u, v + 1} ≤ univ.{v, u + 1} ∨ univ.{v, u + 1} ≤ univ.{u, v + 1}
Module: Mathlib.SetTheory.Ordinal.Commute

Goal state before:
pp: o₁ o₂ : Ordinal.{u_1}
⊢ AddCommute o₁ o₂ ↔ ∃ o n₁ n₂, o * ↑n₁ = o₁ ∧ o * ↑n₂ = o₂

Tactic:
by
  refine ⟨fun hcomm ↦ ?_, ?_⟩
  · induction h : o₁ + o₂ using WellFoundedLT.induction generalizing o₁ o₂ with | ind o ih
    subst h
    wlog hle : o₁ ≤ o₂
    · grind [hcomm.symm]
    rcases eq_or_ne o₁ 0 with (rfl | h₁)
    · exact ⟨o₂, 0, 1, by simp, by simp⟩
    let o₃ := o₂ - o₁
    have hsub : o₁ + o₃ = o₂ := Ordinal.add_sub_cancel_of_le hle
    have hcomm' : AddCommute o₁ o₃ := add_left_cancel (a := o₁) <| by grind
    have hlt : o₁ + o₃ < o₁ + o₂ := by simpa [hsub, hcomm.eq] using h₁.pos
    rcases ih _ hlt hcomm' rfl with ⟨o, n₁, n₃, hn₁, hn₃⟩
    use o, n₁, n₁ + n₃, hn₁
    rw [Nat.cast_add, mul_add, hn₁, hn₃, hsub]
  · rintro ⟨o, n₁, n₂, rfl, rfl⟩
    rw [addCommute_iff_eq, ← mul_add, ← mul_add, ← Nat.cast_add, add_comm, Nat.cast_add]

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

Goal state before:
pp: case ind
α : Type u
inst✝ : CompleteLattice α
f : α →o α
x : α
a b✝ : Ordinal.{u}
hf : f (lfpApprox f x a) = lfpApprox f x a
b : Ordinal.{u}
IH : ∀ y < b, a ≤ y → lfpApprox f x y = lfpApprox f x a
hab : a ≤ b
⊢ lfpApprox f x b = lfpApprox f x a

Tactic:
apply (lfpApprox_mono_right f hab).antisymm'

Goal state after:
case ind
α : Type u
inst✝ : CompleteLattice α
f : α →o α
x : α
a b✝ : Ordinal.{u}
hf : f (lfpApprox f x a) = lfpApprox f x a
b : Ordinal.{u}
IH : ∀ y < b, a ≤ y → lfpApprox f x y = lfpApprox f x a
hab : a ≤ b
⊢ lfpApprox f x b ≤ lfpApprox f x a
Module: Mathlib.SetTheory.Lists

Goal state before:
pp: α : Type u_1
l₁ l₂ : Lists' α true
h : of' l₁ ~ of' l₂
⊢ l₁ ⊆ l₂ ∧ l₂ ⊆ l₁

Tactic:
obtain - | ⟨h₁, h₂⟩ := h

Goal state after:
case refl
α : Type u_1
l₁ : Lists' α true
⊢ l₁ ⊆ l₁ ∧ l₁ ⊆ l₁

case antisymm
α : Type u_1
l₁ l₂ : Lists' α true
h₁ : l₁.Subset l₂
h₂ : l₂.Subset l₁
⊢ l₁ ⊆ l₂ ∧ l₂ ⊆ l₁
Module: Mathlib.SetTheory.Lists

Goal state before:
pp: α : Type u_1
l₁ l₂ : Lists α
h : l₁ ~ l₂
⊢ l₂ ~ l₁

Tactic:
obtain - | ⟨h₁, h₂⟩ := h

Goal state after:
case refl
α : Type u_1
l₁ : Lists α
⊢ l₁ ~ l₁

case antisymm
α : Type u_1
l₁✝ l₂✝ : Lists' α true
h₁ : l₁✝.Subset l₂✝
h₂ : l₂✝.Subset l₁✝
⊢ ⟨true, l₂✝⟩ ~ ⟨true, l₁✝⟩
Module: Mathlib.SetTheory.Ordinal.CantorNormalForm

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

Tactic:
zero_add

Goal state after:
case inr
b e x y : Ordinal.{u_1}
hb : 1 < b
hx : x ≠ 0
hxb : x < b
hy : y < b ^ e
e' : Ordinal.{u_1}
he : e ≠ e'
⊢ (coeff b (b ^ e * x + y)) e' = (coeff b y) e'
Module: Mathlib.SetTheory.Ordinal.CantorNormalForm

Goal state before:
pp: case inr.e_a.e_a
b e x : Ordinal.{u_1}
f : Ordinal.{u_1} →₀ Ordinal.{u_1}
h : ∀ e' ∈ f.support, e' < e
hx : x ≠ 0
hf : f e = 0
e' : Ordinal.{u_1}
he' : e' ∈ f.support.sort fun x1 x2 ↦ x1 ≥ x2
b✝ : Ordinal.{u_1}
⊢ 0 + f e' = f e'

pp: case inr.e_a.e_a
b e x : Ordinal.{u_1}
f : Ordinal.{u_1} →₀ Ordinal.{u_1}
h : ∀ e' ∈ f.support, e' < e
hx : x ≠ 0
hf : f e = 0
e' : Ordinal.{u_1}
he' : e' ∈ f.support.sort fun x1 x2 ↦ x1 ≥ x2
b✝ : Ordinal.{u_1}
⊢ e' ≠ e

Tactic:
zero_add

Goal state after:
case inr.e_a.e_a
b e x : Ordinal.{u_1}
f : Ordinal.{u_1} →₀ Ordinal.{u_1}
h : ∀ e' ∈ f.support, e' < e
hx : x ≠ 0
hf : f e = 0
e' : Ordinal.{u_1}
he' : e' ∈ f.support.sort fun x1 x2 ↦ x1 ≥ x2
b✝ : Ordinal.{u_1}
⊢ f e' = f e'

case inr.e_a.e_a
b e x : Ordinal.{u_1}
f : Ordinal.{u_1} →₀ Ordinal.{u_1}
h : ∀ e' ∈ f.support, e' < e
hx : x ≠ 0
hf : f e = 0
e' : Ordinal.{u_1}
he' : e' ∈ f.support.sort fun x1 x2 ↦ x1 ≥ x2
b✝ : Ordinal.{u_1}
⊢ e' ≠ e
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: case oadd'
o : ONote
b : Ordinal.{0}
e✝ : ONote
n✝ : ℕ+
a✝² : ONote
eb✝ b✝ : Ordinal.{0}
a✝¹ : e✝.NFBelow eb✝
a✝ : a✝².NFBelow e✝.repr
h₃ : e✝.repr < b✝
a_ih✝ : e✝.repr < ω ^ eb✝
IH : a✝².repr < ω ^ e✝.repr
⊢ ω ^ succ e✝.repr ≤ ω ^ b✝

Tactic:
succ_le_of_lt h₃

Goal state after:
case oadd'
o : ONote
b : Ordinal.{0}
e✝ : ONote
n✝ : ℕ+
a✝² : ONote
eb✝ b✝ : Ordinal.{0}
a✝¹ : e✝.NFBelow eb✝
a✝ : a✝².NFBelow e✝.repr
h₃ : e✝.repr < b✝
a_ih✝ : e✝.repr < ω ^ eb✝
IH : a✝².repr < ω ^ e✝.repr
⊢ ω ^ b✝ ≤ ω ^ b✝

case hc
o : ONote
b : Ordinal.{0}
e✝ : ONote
n✝ : ℕ+
a✝² : ONote
eb✝ b✝ : Ordinal.{0}
a✝¹ : e✝.NFBelow eb✝
a✝ : a✝².NFBelow e✝.repr
h₃ : e✝.repr < b✝
a_ih✝ : e✝.repr < ω ^ eb✝
IH : a✝².repr < ω ^ e✝.repr
⊢ 0 < ω
Module: Mathlib.SetTheory.Ordinal.CantorNormalForm

Goal state before:
pp: case pos
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
a : Ordinal.{u_1}
ha : a ∈ f.support
⊢ 0 + f a = f a

pp: case pos
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
a : Ordinal.{u_1}
ha : a ∈ f.support
⊢ a ≠ e'

Tactic:
zero_add

Goal state after:
case pos
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
a : Ordinal.{u_1}
ha : a ∈ f.support
⊢ f a = f a

case pos
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
a : Ordinal.{u_1}
ha : a ∈ f.support
⊢ a ≠ e'
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
⊢ 0 + f e' = f e'

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
⊢ e' ≠ e

Tactic:
zero_add

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
⊢ f e' = f e'

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
⊢ e' ≠ e
Module: Mathlib.SetTheory.Ordinal.Topology

Goal state before:
pp: s : Set Ordinal.{u}
hs : ¬BddAbove s
Hs : StrictMono (enumOrd s)
h : IsClosed s
a : Ordinal.{u}
ha : IsSuccLimit a
o : Ordinal.{u}
H : ∀ b < a, enumOrd s b ≤ o
this✝ : sSup (enumOrd s '' Set.Iio a) ∈ closure (enumOrd s '' Set.Iio a)
this : sSup (enumOrd s '' Set.Iio a) ∈ s
⊢ ∀ b < a, enumOrd s b < sSup (enumOrd s '' Set.Iio a)

Tactic:
· exact fun b hb ↦ (enumOrd_strictMono hs (lt_add_one b)).trans_le <|
          le_csSup bddAbove_of_small <| Set.mem_image_of_mem _ (ha.add_one_lt hb)

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

Goal state before:
pp: f : Ordinal.{u_1} → Ordinal.{u_1}
⊢ veblenWith f 0 = f

Tactic:
veblenWith,

Goal state after:
f : Ordinal.{u_1} → Ordinal.{u_1}
⊢ (if 0 = 0 then f
    else
      derivFamily fun x ↦
        match (motive := { x // x ∈ Iio 0 } → Ordinal.{u_1} → Ordinal.{u_1}) x with
        | ⟨x, property⟩ => veblenWith f x) =
    f
Module: Mathlib.SetTheory.Ordinal.Veblen

Goal state before:
pp: o : Ordinal.{u}
f : Ordinal.{u} → Ordinal.{u}
h : o ≠ 0
⊢ veblenWith f o = derivFamily fun x ↦ veblenWith f ↑x

Tactic:
veblenWith,

Goal state after:
o : Ordinal.{u}
f : Ordinal.{u} → Ordinal.{u}
h : o ≠ 0
⊢ (if o = 0 then f
    else
      derivFamily fun x ↦
        match (motive := { x // x ∈ Iio o } → Ordinal.{u} → Ordinal.{u}) x with
        | ⟨x, property⟩ => veblenWith f x) =
    derivFamily fun x ↦ veblenWith f ↑x
Module: Mathlib.SetTheory.ZFC.Basic

Goal state before:
pp: x : PSet.{u_1}
a : ZFSet.{u_1}
h : a ∈ ↑(mk x)
⊢ x.Nonempty

Tactic:
induction a using Quotient.inductionOn

Goal state after:
case h
x a✝ : PSet.{u_1}
h : ⟦a✝⟧ ∈ ↑(mk x)
⊢ x.Nonempty
Module: Mathlib.SetTheory.ZFC.Basic

Goal state before:
pp: case h
α β : Type u
A : α → PSet.{u}
B : β → PSet.{u}
αβ : ∀ (a : α), ∃ b, (A a).Equiv (B b)
a : (PSet.mk α A).Type
c✝ : ((PSet.mk α A).Func a).Type
b : β
γ : Type u
Γ : γ → PSet.{u}
A_ih✝¹ : ∀ (a_1 : γ), A a = Γ a_1 → ∃ b, ((⋃₀ PSet.mk α A).Func ⟨a, c✝⟩).Equiv ((⋃₀ PSet.mk β B).Func b)
ea : A a = PSet.mk γ Γ
δ : Type u
Δ : δ → PSet.{u}
A_ih✝ : ∀ (a_1 : δ), B b = Δ a_1 → ∃ b, ((⋃₀ PSet.mk α A).Func ⟨a, c✝⟩).Equiv ((⋃₀ PSet.mk β B).Func b)
eb : B b = PSet.mk δ Δ
γδ : ∀ (a : γ), ∃ b, (Γ a).Equiv (Δ b)
δγ : ∀ (b : δ), ∃ a, (Γ a).Equiv (Δ b)
c : (A a).Type := c✝
d : δ
hd : (Γ (⋯.mp c)).Equiv (Δ d)
⊢ ((A a).Func c).Equiv ((B b).Func (⋯ ▸ d))

Tactic:
match A a, B b, ea, eb, c, d, hd with
    | _, _, rfl, rfl, _, _, hd => exact hd

Goal state after:
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
⊢ y = f z

Tactic:
let ⟨w, _, we⟩ := mem_image.1 yx

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
⊢ y = f z
Module: Mathlib.SetTheory.ZFC.Ordinal

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

Tactic:
revert hx hy
    refine Sym2.GameAdd.recursion mem_wf ?_ x y
    intro x y IH hx hy hxy
    by_cases hyx : y ⊆ x
    · exact Or.inl (subset_antisymm hxy hyx)
    · obtain ⟨m, hm, hm'⟩ := mem_wf.has_min (y \ x) (Set.sdiff_nonempty.2 hyx)
      have hmy : m ∈ y := by simp only [Set.mem_sdiff, SetLike.mem_coe] at hm; exact hm.1
      have hmx : m ⊆ x := by
        intro z hzm
        by_contra hzx
        exact hm' _ ⟨hy.mem_trans hzm hmy, hzx⟩ hzm
      obtain rfl | H := IH m x (Sym2.GameAdd.fst_snd hmy) (hy.mem hmy) hx hmx
      · exact Or.inr hmy
      · cases Set.notMem_of_mem_sdiff hm H

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

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

Tactic:
by
  constructor
  · revert hx hy
    refine Sym2.GameAdd.recursion mem_wf ?_ x y
    intro x y IH hx hy hxy
    by_cases hyx : y ⊆ x
    · exact Or.inl (subset_antisymm hxy hyx)
    · obtain ⟨m, hm, hm'⟩ := mem_wf.has_min (y \ x) (Set.sdiff_nonempty.2 hyx)
      have hmy : m ∈ y := by simp only [Set.mem_sdiff, SetLike.mem_coe] at hm; exact hm.1
      have hmx : m ⊆ x := by
        intro z hzm
        by_contra hzx
        exact hm' _ ⟨hy.mem_trans hzm hmy, hzx⟩ hzm
      obtain rfl | H := IH m x (Sym2.GameAdd.fst_snd hmy) (hy.mem hmy) hx hmx
      · exact Or.inr hmy
      · cases Set.notMem_of_mem_sdiff hm H
  · rintro (rfl | h)
    · rfl
    · exact hy.subset_of_mem h

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

Goal state before:
pp: o : Ordinal.{u_1}
⊢ o.toPSet.Type = o.ToType

Tactic:
toPSet

Goal state after:
o : Ordinal.{u_1}
⊢ (PSet.mk o.ToType fun a ↦ (↑a.toOrd).toPSet).Type = o.ToType
Module: Mathlib.SetTheory.ZFC.Ordinal

Goal state before:
pp: 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

pp: 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

Tactic:
· exact toZFSet_mem_toZFSet_iff.2 (hb.trans ha)

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.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
⊢ IsNat ((algebraMap R A) r + (algebraMap R A) s) 0

Tactic:
rw [← map_add, h, map_zero]

Goal state after:
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
⊢ IsNat 0 0
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basic

Goal state before:
pp: case cons
n : ℕ
r : ℝ
basis_hd : ℝ → ℝ
basis_tl : List (ℝ → ℝ)
⊢ (monomialRpow (basis_hd :: basis_tl) n r).Sorted

Tactic:
simpa only [sorted_iff_seq_sorted, monomialRpow_seq] using Multiseries.monomialRpow_sorted

Goal state after: