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

Goal state before:
pp: k : Type u_1
inst✝ : Field k
n : ℕ
I : Ideal (MvPolynomial (Fin 0) k)
hi : I ≠ ⊤
a b : MvPolynomial (Fin 0) k
hab : a - b ∈ I
ne✝ : ¬a = b
eq : a - b = MvPolynomial.C (MvPolynomial.coeff 0 (a - b))
ne : MvPolynomial.coeff 0 (a - b) ≠ 0
c : k
left✝ : MvPolynomial.coeff 0 (a - b) * c = 1
eqr : c * MvPolynomial.coeff 0 (a - b) = 1
⊢ c • (a - b) = 1

Tactic:
MvPolynomial.smul_eq_C_mul,

Goal state after:
k : Type u_1
inst✝ : Field k
n : ℕ
I : Ideal (MvPolynomial (Fin 0) k)
hi : I ≠ ⊤
a b : MvPolynomial (Fin 0) k
hab : a - b ∈ I
ne✝ : ¬a = b
eq : a - b = MvPolynomial.C (MvPolynomial.coeff 0 (a - b))
ne : MvPolynomial.coeff 0 (a - b) ≠ 0
c : k
left✝ : MvPolynomial.coeff 0 (a - b) * c = 1
eqr : c * MvPolynomial.coeff 0 (a - b) = 1
⊢ MvPolynomial.C c * (a - b) = 1
Module: Mathlib.RingTheory.WittVector.Basic

Goal state before:
pp: p : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Fact (Nat.Prime p)
x y : 𝕎 R
⊢ (x - y).ghostFun = x.ghostFun - y.ghostFun

Tactic:
by
  ghost_fun_tac X 0 - X 1, ![x.coeff, y.coeff]

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

Goal state before:
pp: case succ
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
x : 𝕎 R
n : ℕ
ih : ∀ (k : ℕ), (x * ↑n).coeff k = (aeval x.coeff) (wittMulN p n k)
k : ℕ
⊢ (x * ↑n + x).coeff k = (aeval fun i ↦ (aeval x.coeff) (Function.uncurry ![wittMulN p n, X] i)) (wittAdd p k)

Tactic:
add_coeff

Goal state after:
case succ
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
x : 𝕎 R
n : ℕ
ih : ∀ (k : ℕ), (x * ↑n).coeff k = (aeval x.coeff) (wittMulN p n k)
k : ℕ
⊢ peval (wittAdd p k) ![(x * ↑n).coeff, x.coeff] =
    (aeval fun i ↦ (aeval x.coeff) (Function.uncurry ![wittMulN p n, X] i)) (wittAdd p k)
Module: Mathlib.RingTheory.WittVector.Domain

Goal state before:
pp: p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
x : 𝕎 R
n : ℕ
h : ∀ i < n, x.coeff i = 0
⊢ x = (⇑verschiebung)^[n] (x.shift n)

Tactic:
induction n with
  | zero => cases x; simp [shift]
  | succ k ih =>
    dsimp; rw [verschiebung_shift]
    · exact ih fun i hi => h _ (hi.trans (Nat.lt_succ_self _))
    · exact h

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

Goal state before:
pp: p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
x : 𝕎 R
hx : x ≠ 0
hall : ∀ (k : ℕ), x.coeff k = 0
⊢ False

Tactic:
apply hx

Goal state after:
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
x : 𝕎 R
hx : x ≠ 0
hall : ∀ (k : ℕ), x.coeff k = 0
⊢ x = 0
Module: Mathlib.RingTheory.WittVector.InitTail

Goal state before:
pp: p n : ℕ
R : Type u_1
inst✝ : CommRing R
P✝ P : ℕ → Prop
⊢ IsPoly p fun x x_1 x_2 ↦ select P x_2

Tactic:
use selectPoly P
  rintro R _Rcr x
  funext i
  apply coeff_select

Goal state after:
Module: Mathlib.RingTheory.Perfection

Goal state before:
pp: K : Type u₁
inst✝⁴ : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝³ : CommRing O
inst✝² : Algebra O K
hv : v.Integers O
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fact ¬IsUnit ↑p
f g : PreTilt O p
hf : f ≠ 0
hg : g ≠ 0
m n : ℕ
hm : (Perfection.coeff (ModP O p) p (max m n)) f ≠ 0
hn : (Perfection.coeff (ModP O p) p (max m n)) g ≠ 0
⊢ (coeff (max m n + 1)) (f * g) ≠ 0

Tactic:
rw [map_mul]

Goal state after:
K : Type u₁
inst✝⁴ : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝³ : CommRing O
inst✝² : Algebra O K
hv : v.Integers O
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fact ¬IsUnit ↑p
f g : PreTilt O p
hf : f ≠ 0
hg : g ≠ 0
m n : ℕ
hm : (Perfection.coeff (ModP O p) p (max m n)) f ≠ 0
hn : (Perfection.coeff (ModP O p) p (max m n)) g ≠ 0
⊢ (coeff (max m n + 1)) f * (coeff (max m n + 1)) g ≠ 0
Module: Mathlib.RingTheory.WittVector.Teichmuller

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
R : Type u_3
x y : MvPolynomial R ℚ
⊢ ghostMap (teichmullerFun p (x * y)) = ghostMap (teichmullerFun p x * teichmullerFun p y)

Tactic:
rw [map_mul]

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
R : Type u_3
x y : MvPolynomial R ℚ
⊢ ghostMap (teichmullerFun p (x * y)) = ghostMap (teichmullerFun p x) * ghostMap (teichmullerFun p y)
Module: Mathlib.RingTheory.WittVector.Complete

Goal state before:

Tactic:
_ = verschiebung^[n] (x.shift n) := by
      simpa using eq_iterate_verschiebung (x := x) (n := n) h
    _ = _ := by
      congr
      rw [← Function.comp_apply (f := frobenius^[n]), ← Function.Commute.comp_iterate]
      · rw [← WittVector.frobeniusEquiv_apply, ← RingEquiv.coe_trans]
        simp
      · rw [Function.Commute, Function.Semiconj, ← WittVector.frobeniusEquiv_apply]
        simp only [RingEquiv.apply_symm_apply, RingEquiv.symm_apply_apply, implies_true]

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

Goal state before:
pp: R : Type u_1
inst✝² : CommRing R
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : CharP R p
⊢ dickson 1 1 p = X ^ p

Tactic:
have h : (1 : R) = ZMod.castHom (dvd_refl p) R 1 := by
    simp only [ZMod.castHom_apply, ZMod.cast_one']
  rw [h, ← map_dickson (ZMod.castHom (dvd_refl p) R), dickson_one_one_zmod_p, Polynomial.map_pow,
    map_X]

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

Goal state before:
pp: case neg.refine_1
n : ℕ
hn1 : n ≠ 1
hn0 : ¬n = 0
hp : X ^ n - X - 1 = trinomial 0 1 n (-1) (-1) 1
hn : 1 < n
⊢ (X ^ n - X - 1).IsPrimitive

Tactic:
exact hp.symm ▸ (trinomial_monic zero_lt_one hn).isPrimitive

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

Goal state before:
pp: R : Type u_2
S : Type u_3
inst✝¹ : CommRing R
inst✝ : CommRing S
p : ℕ
hp : p ≠ 0
f : R →+* S
φ : R⟦X⟧
⊢ (map f) ((expand p hp) φ) = (expand p hp) ((map f) φ)

Tactic:
simp [map, expand, MvPowerSeries.map_expand]

Goal state after:
Module: Mathlib.RingTheory.TensorProduct.DirectLimitFG

Goal state before:
pp: R : Type u
M : Type u_1
N : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
P : Submodule R M
hP : P.FG
t t' : ↥P ⊗[R] N
h : (rTensor N P.subtype) t = (rTensor N P.subtype) t'
⊢ ∃ Q, ∃ (hPQ : P ≤ Q), Q.FG ∧ (rTensor N (inclusion hPQ)) t = (rTensor N (inclusion hPQ)) t'

Tactic:
by
  simp only [← Submodule.FG.rTensor.directLimit_apply' R M N hP, EmbeddingLike.apply_eq_iff_eq] at h
  obtain ⟨Q, hPQ, h⟩ := Module.DirectLimit.exists_eq_of_of_eq h
  use Q.val, Subtype.coe_le_coe.mpr hPQ, Q.property

Goal state after:
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
A : Type u
inst✝⁵ : CommSemiring A
inst✝⁴ : Algebra R A
φ : A →ₐ[R] S
p : A ⊗[R] M
T : Type w
inst✝³ : CommSemiring T
inst✝² : Algebra R T
B : Type u
inst✝¹ : CommSemiring B
inst✝ : Algebra R B
ψ : B →ₐ[R] T
q : B ⊗[R] M
h : S →ₐ[R] T
h' : ↥φ.range →ₐ[R] ↥ψ.range
hh' : ψ.range.val.comp h' = h.comp φ.range.val
hpq : (rTensor M (h'.comp φ.rangeRestrict).toLinearMap) p = (rTensor M ψ.rangeRestrict.toLinearMap) q
θ : (RingCon.ker ↑φ).Quotient →ₐ[R] (RingCon.ker ↑ψ).Quotient :=
  (↑(quotientKerEquivRangeₐ ψ).symm).comp (h'.comp ↑(quotientKerEquivRangeₐ φ))
⊢ (h.comp φ.range.val).comp ↑(quotientKerEquivRangeₐ φ) = ψ.range.val.comp ((↑(quotientKerEquivRangeₐ ψ)).comp θ)

Tactic:
simp only [θ, ← AlgHom.comp_assoc, ← hh']

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
A : Type u
inst✝⁵ : CommSemiring A
inst✝⁴ : Algebra R A
φ : A →ₐ[R] S
p : A ⊗[R] M
T : Type w
inst✝³ : CommSemiring T
inst✝² : Algebra R T
B : Type u
inst✝¹ : CommSemiring B
inst✝ : Algebra R B
ψ : B →ₐ[R] T
q : B ⊗[R] M
h : S →ₐ[R] T
h' : ↥φ.range →ₐ[R] ↥ψ.range
hh' : ψ.range.val.comp h' = h.comp φ.range.val
hpq : (rTensor M (h'.comp φ.rangeRestrict).toLinearMap) p = (rTensor M ψ.rangeRestrict.toLinearMap) q
θ : (RingCon.ker ↑φ).Quotient →ₐ[R] (RingCon.ker ↑ψ).Quotient :=
  (↑(quotientKerEquivRangeₐ ψ).symm).comp (h'.comp ↑(quotientKerEquivRangeₐ φ))
⊢ (ψ.range.val.comp h').comp ↑(quotientKerEquivRangeₐ φ) =
    (((ψ.range.val.comp ↑(quotientKerEquivRangeₐ ψ)).comp ↑(quotientKerEquivRangeₐ ψ).symm).comp h').comp
      ↑(quotientKerEquivRangeₐ φ)
Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation

Goal state before:
pp: A : Type u_1
inst✝¹ : CommRing A
inst✝ : IsLocalRing A
g q : A⟦X⟧
r : A[X]
hg : (map (IsLocalRing.residue A)) g ≠ 0
n : ℕ := ((map (IsLocalRing.residue A)) g).order.toNat
H1 : r.degree < ↑n
H2 :
  1 =
    ∑ p ∈ Finset.antidiagonal n,
      (coeff p.1) ((map (IsLocalRing.residue A)) g) * (coeff p.2) ((map (IsLocalRing.residue A)) q)
p : ℕ × ℕ
hp : p ∈ Finset.antidiagonal n
hnotMem : p ∉ {(n, 0)}
⊢ ↑p.1 < ((map (IsLocalRing.residue A)) g).order

Tactic:
rw [← ENat.lt_lift_iff (h := order_finite_iff_ne_zero.2 hg), ENat.lift_eq_toNat_of_lt_top]
      refine (Finset.HasAntidiagonal.antidiagonal.fst_le hp).lt_of_ne ?_
      contrapose hnotMem
      rwa [Finset.mem_singleton, Finset.HasAntidiagonal.antidiagonal_congr hp (by simp)]

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
N : Submodule R M
inst✝¹ : IsSimpleModule R ↥N
s : Set (Submodule R M)
inst✝ : IsSemisimpleModule R M
hs : sSup s = ⊤
⊢ ∃ m ∈ s, ∃ S ≤ m, Nonempty (↥N ≃ₗ[R] ↥S)

Tactic:
by
  have := IsSimpleModule.nontrivial R N
  have ⟨_, compl⟩ := exists_isCompl N
  have ⟨m, hm, ne⟩ := exists_ne_zero_of_sSup_eq_top (ne_zero_of_surjective
    (projectionOnto_surjective compl)) _ hs
  have ⟨S, ⟨e⟩⟩ := linearEquiv_of_ne_zero ne
  exact ⟨m, hm, _, m.map_subtype_le S, ⟨e.trans (S.equivMapOfInjective _ m.subtype_injective)⟩⟩

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

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

Tactic:
(associated_one_iff_isUnit.mpr ha).moebius_eq,

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ ((range n).biUnion fun i ↦ (↑p ^ i * wittMul p i ^ p ^ (n - i)).vars) ⊆ univ ×ˢ range n

Tactic:
rw [biUnion_subset]

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ ∀ x ∈ range n, (↑p ^ x * wittMul p x ^ p ^ (n - x)).vars ⊆ univ ×ˢ range n
Module: Mathlib.RingTheory.WittVector.MulCoeff

Goal state before:
pp: case refine_1
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ ((range (n + 1)).biUnion fun i ↦
      ((rename (Prod.mk 0)) ((monomial (Finsupp.single i (p ^ (n + 1 - i)))) (↑p ^ i))).vars) ⊆
    univ ×ˢ range (n + 1)

Tactic:
rw [biUnion_subset]

Goal state after:
case refine_1
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ ∀ x ∈ range (n + 1),
    ((rename (Prod.mk 0)) ((monomial (Finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x))).vars ⊆ univ ×ˢ range (n + 1)
Module: Mathlib.RingTheory.WittVector.MulCoeff

Goal state before:
pp: case refine_2
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ ((range (n + 1)).biUnion fun i ↦
      ((rename (Prod.mk 1)) ((monomial (Finsupp.single i (p ^ (n + 1 - i)))) (↑p ^ i))).vars) ⊆
    univ ×ˢ range (n + 1)

Tactic:
rw [biUnion_subset]

Goal state after:
case refine_2
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ ∀ x ∈ range (n + 1),
    ((rename (Prod.mk 1)) ((monomial (Finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x))).vars ⊆ univ ×ˢ range (n + 1)
Module: Mathlib.RingTheory.WittVector.MulCoeff

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝ : CommRing k
n : ℕ
x y : 𝕎 k
⊢ peval (polyOfInterest p n) ![fun i ↦ x.coeff i, fun i ↦ y.coeff i] =
    (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)

Tactic:
simp only [polyOfInterest, peval,
    Function.uncurry_apply_pair, aeval_X, Matrix.cons_val_one, map_mul, Matrix.cons_val_zero,
    map_sub]
  rw [sub_sub, add_comm (_ * _), ← sub_sub]
  simp [wittPolynomial_eq_sum_C_mul_X_pow, aeval, mul_coeff, peval, map_natCast,
    map_add, map_pow, map_mul]

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

Goal state before:
pp: case inr
α : Type v
inst✝ : LinearOrder α
s : Set (Set α)
hα : cof α ≤ 1
hs : ∀ x ∈ s, IsClub x
h✝ : Nonempty α
⊢ IsClub (⋂₀ s)

Tactic:
cases topOrderOrNoTopOrder α

Goal state after:
case inr.inl
α : Type v
inst✝ : LinearOrder α
s : Set (Set α)
hα : cof α ≤ 1
hs : ∀ x ∈ s, IsClub x
h✝ : Nonempty α
val✝ : OrderTop α
⊢ IsClub (⋂₀ s)

case inr.inr
α : Type v
inst✝ : LinearOrder α
s : Set (Set α)
hα : cof α ≤ 1
hs : ∀ x ∈ s, IsClub x
h✝ : Nonempty α
val✝ : NoTopOrder α
⊢ IsClub (⋂₀ s)
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: case zero
o : ONote
b₁ b₂ b✝ : Ordinal.{0}
bb : b✝ ≤ b₂
⊢ NFBelow 0 b₂

Tactic:
exact zero

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

Goal state before:
pp: b : Ordinal.{0}
e : ONote
n : ℕ+
a o : ONote
h₁ : (e.oadd n a).NFBelow b
h₂ : o.NFBelow b
h' : (a + o).NFBelow b
⊢ (e.oadd n a + o).NFBelow b

Tactic:
simp only [oadd_add]

Goal state after:
b : Ordinal.{0}
e : ONote
n : ℕ+
a o : ONote
h₁ : (e.oadd n a).NFBelow b
h₂ : o.NFBelow b
h' : (a + o).NFBelow b
⊢ (e.addAux n (a + o)).NFBelow b
Module: Mathlib.SetTheory.ZFC.Basic

Goal state before:
pp: x✝ y✝ z✝ x y : ZFSet.{u}
hxy : x.toSet = y.toSet
z : ZFSet.{u}
⊢ z ∈ x.toSet ↔ z ∈ y.toSet

Tactic:
exact congr(z ∈ $hxy)

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

Goal state before:
pp: case refine_2
x y z : ZFSet.{u_1}
⊢ x = z ∧ y = z → {x, y} = {z}

Tactic:
· rintro ⟨rfl, rfl⟩
    exact pair_eq_singleton y

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

Goal state before:
pp: case oadd.lt.h₁
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 < ω ^ e'.repr

Tactic:
have := (h₁.below_of_lt ee).repr_lt

Goal state after:
case oadd.lt.h₁
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'
this : (e.oadd n a).repr < ω ^ e'.repr
⊢ ω ^ e.repr * ↑↑n < ω ^ e'.repr
Module: Mathlib.SetTheory.ZFC.Basic

Goal state before:
pp: x y y' : ZFSet.{u_1}
H : ∀ (z : ZFSet.{u_1}), z = {x} ∨ z = {x, y} ↔ z = {x} ∨ z = {x, y'}
he : y = x → y = y'
hx : {x, y} = {x} ∨ True ↔ {x, y} = {x} ∨ {x, y} = {x, y'}
⊢ x = x ∧ y = y'

Tactic:
pair_eq_singleton_iff,

Goal state after:
x y y' : ZFSet.{u_1}
H : ∀ (z : ZFSet.{u_1}), z = {x} ∨ z = {x, y} ↔ z = {x} ∨ z = {x, y'}
he : y = x → y = y'
hx : True ∧ y = x ∨ True ↔ True ∧ y = x ∨ {x, y} = {x, y'}
⊢ x = x ∧ y = y'
Module: Mathlib.SetTheory.Ordinal.Veblen

Goal state before:
pp: a x : Ordinal.{u}
⊢ x.invVeblen₂ < a ↔ ω ^ x < veblen x.invVeblen₁ a

Tactic:
← veblen_lt_veblen_iff_right (o := x.invVeblen₁),

Goal state after:
a x : Ordinal.{u}
⊢ veblen x.invVeblen₁ x.invVeblen₂ < veblen x.invVeblen₁ a ↔ ω ^ x < veblen x.invVeblen₁ a
Module: Mathlib.SetTheory.Ordinal.Veblen

Goal state before:
pp: a x : Ordinal.{u}
⊢ a < x.invVeblen₂ ↔ veblen x.invVeblen₁ a < ω ^ x

Tactic:
← veblen_lt_veblen_iff_right (o := x.invVeblen₁),

Goal state after:
a x : Ordinal.{u}
⊢ veblen x.invVeblen₁ a < veblen x.invVeblen₁ x.invVeblen₂ ↔ veblen x.invVeblen₁ a < ω ^ x
Module: Mathlib.SetTheory.Ordinal.Veblen

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

Tactic:
veblen_veblen_of_lt

Goal state after:
o a : Ordinal.{u}
ho : o ≠ 0
h : a < veblen o a
⊢ veblen o a = veblen o a

case h
o a : Ordinal.{u}
ho : o ≠ 0
h : a < veblen o a
⊢ 0 < o
Module: Mathlib.SetTheory.Ordinal.Veblen

Goal state before:
pp: o : Ordinal.{u_1}
⊢ ε_ o = deriv (fun a ↦ ω ^ a) o

Tactic:
simpa [epsilon] using congrFun (veblen_add_one 0) o

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

Goal state before:
pp: e₁ : ONote
n₁ : ℕ+
a₁ e₂ : ONote
n₂ : ℕ+
a₂ : ONote
b : Ordinal.{0}
h₁ : (e₁.oadd n₁ a₁).NFBelow b
h₂ : (e₂.oadd n₂ a₂).NF
⊢ (e₁.oadd n₁ a₁ - e₂.oadd n₂ a₂).NFBelow b

Tactic:
have h' := sub_nfBelow h₁.snd h₂.snd
    simp only [HSub.hSub, Sub.sub, sub] at h' ⊢
    have := @cmp_compares _ _ h₁.fst h₂.fst
    cases h : cmp e₁ e₂
    · apply NFBelow.zero
    · rw [Nat.sub_eq]
      simp only [h, Ordering.compares_eq] at this
      subst e₂
      cases (n₁ : ℕ) - n₂
      · by_cases en : n₁ = n₂ <;> simp only [en, ↓reduceIte]
        · exact h'.mono (le_of_lt h₁.lt)
        · exact NFBelow.zero
      · exact NFBelow.oadd h₁.fst h₁.snd h₁.lt
    · exact 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 ↔ y ∈ x

Tactic:
rw [not_iff_comm, notMem_iff_subset hy hx]

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

Goal state before:
pp: x : ZFSet.{u}
⊢ x.IsTransitive ∧ Std.Trichotomous (Subrel (fun x1 x2 ↦ x1 ∈ x2) fun x_1 ↦ x_1 ∈ x) → x.IsOrdinal

Tactic:
rintro ⟨h₁, h₂⟩

Goal state after:
x : ZFSet.{u}
h₁ : x.IsTransitive
h₂ : Std.Trichotomous (Subrel (fun x1 x2 ↦ x1 ∈ x2) fun x_1 ↦ x_1 ∈ x)
⊢ x.IsOrdinal
Module: Mathlib.SetTheory.ZFC.Ordinal

Goal state before:
pp: case mpr
x : ZFSet.{u}
⊢ x.IsTransitive ∧ IsWellOrder (↥x) (Subrel (fun x1 x2 ↦ x1 ∈ x2) fun x_1 ↦ x_1 ∈ x) → x.IsOrdinal

Tactic:
rintro ⟨h₁, h₂⟩

Goal state after:
case mpr
x : ZFSet.{u}
h₁ : x.IsTransitive
h₂ : IsWellOrder (↥x) (Subrel (fun x1 x2 ↦ x1 ∈ x2) fun x_1 ↦ x_1 ∈ x)
⊢ x.IsOrdinal
Module: Mathlib.SetTheory.ZFC.VonNeumann

Goal state before:
pp: case add_one
o : Ordinal.{u}
ih : (V_ o).card = preBeth o
⊢ (V_ (o + 1)).card = preBeth (o + 1)

Tactic:
simp [ih]

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

Goal state before:
pp: o' : ONote
m : ℕ
x✝ : NF 0
p : split' 0 = (o', m)
⊢ split 0 = (scale 1 o', m)

Tactic:
by injection p; subst o' m; rfl

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

Goal state before:
pp: case zero
e a0 a : ONote
inst✝² : e.NF
inst✝¹ : a0.NF
inst✝ : a.NF
k : ℕ
⊢ (match k, 0 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 k

Goal state after:
case zero.zero
e a0 a : ONote
inst✝² : e.NF
inst✝¹ : a0.NF
inst✝ : a.NF
⊢ (match 0, 0 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

case zero.succ
e a0 a : ONote
inst✝² : e.NF
inst✝¹ : a0.NF
inst✝ : a.NF
n✝ : ℕ
⊢ (match n✝ + 1, 0 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
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: case oadd.succ
o₁ o₂ : ONote
inst✝¹ : o₁.NF
inst✝ : o₂.NF
m : ℕ
b' : ONote
this✝ : b'.NF
a0 : ONote
n : ℕ+
a' : ONote
e₁ : o₁.split = (a0.oadd n a', m)
na : (a0.oadd n a').NF
this : a0.NF
k : ℕ
e₂ : o₂.split' = (b', k + 1)
⊢ (match (scale 1 b', k + 1) with
    | (b, 0) => (a0 * b).oadd 1 0
    | (b, k.succ) => (a0 * b + a0 * ↑k).scale (a0.oadd n a') + (a0 * b).opowAux a0 (a0.oadd n a' * ↑m) k m).NF

Tactic:
cases k

Goal state after:
case oadd.succ.zero
o₁ o₂ : ONote
inst✝¹ : o₁.NF
inst✝ : o₂.NF
m : ℕ
b' : ONote
this✝ : b'.NF
a0 : ONote
n : ℕ+
a' : ONote
e₁ : o₁.split = (a0.oadd n a', m)
na : (a0.oadd n a').NF
this : a0.NF
e₂ : o₂.split' = (b', 0 + 1)
⊢ (match (scale 1 b', 0 + 1) with
    | (b, 0) => (a0 * b).oadd 1 0
    | (b, k.succ) => (a0 * b + a0 * ↑k).scale (a0.oadd n a') + (a0 * b).opowAux a0 (a0.oadd n a' * ↑m) k m).NF

case oadd.succ.succ
o₁ o₂ : ONote
inst✝¹ : o₁.NF
inst✝ : o₂.NF
m : ℕ
b' : ONote
this✝ : b'.NF
a0 : ONote
n : ℕ+
a' : ONote
e₁ : o₁.split = (a0.oadd n a', m)
na : (a0.oadd n a').NF
this : a0.NF
n✝ : ℕ
e₂ : o₂.split' = (b', n✝ + 1 + 1)
⊢ (match (scale 1 b', n✝ + 1 + 1) with
    | (b, 0) => (a0 * b).oadd 1 0
    | (b, k.succ) => (a0 * b + a0 * ↑k).scale (a0.oadd n a') + (a0 * b).opowAux a0 (a0.oadd n a' * ↑m) k m).NF
Module: Mathlib.SetTheory.Ordinal.Notation

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

Tactic:
cases k

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

case succ
a0 a' : ONote
N0 : a0.NF
Na' : a'.NF
d : ω ∣ a'.repr
e0 : a0.repr ≠ 0
n : ℕ+
No : (a0.oadd n a').NF
ω0 : Ordinal.{0} := ω ^ a0.repr
α' : Ordinal.{0} := ω0 * ↑↑n + a'.repr
α0 : 0 < α'
h : a'.repr + ↑0 < ω ^ a0.repr
n✝ : ℕ
ω00 : 0 < ω0 ^ ↑(n✝ + 1)
R' : Ordinal.{0} := (opowAux 0 a0 (a0.oadd n a' * ↑0) (n✝ + 1 + 1) 0).repr
R : Ordinal.{0} := (opowAux 0 a0 (a0.oadd n a' * ↑0) (n✝ + 1) 0).repr
IH : (n✝ + 1 ≠ 0 → R < ω0 ^ succ ↑(n✝ + 1)) ∧ ω0 ^ ↑(n✝ + 1) * α' + R = (α' + ↑0) ^ succ ↑(n✝ + 1)
RR : R' = ω0 ^ ↑(n✝ + 1) * (α' * ↑0) + R
Rl : R < ω ^ (a0.repr * succ ↑(n✝ + 1))
⊢ R = 0
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 ↦ (x.1, ↑x.2 s_tl))
      (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:
generalize ht0 : op (.cons s_hd nil) = t0 at *

Goal state after:
case cons
α : Type u_1
op : Stream'.Seq α → Stream'.Seq α
h : FriendlyOperation op
s_hd : α
s_tl t0 : Stream'.Seq α
ht0 : op (Seq.cons s_hd nil) = t0
⊢ (op (Seq.cons s_hd s_tl)).destruct =
    Option.map (fun x ↦ (x.1, ↑x.2 s_tl))
      (match t0.destruct with
      | none => none
      | some (t_hd, snd) => some (t_hd, ⟨fun s_tl ↦ (op (Seq.cons s_hd s_tl)).tail, ⋯⟩))
Module: Mathlib.Tactic.NormNum.IsSquare

Goal state before:
pp: a : ℚ
d : ℕ
hnd : ↑d ≤ 0
hn : ¬IsSquare 1
ha : IsNNRat a 1 d
⊢ False

Tactic:
simp at hn

Goal state after:
Module: Mathlib.Tactic.NormNum.LegendreSymbol

Goal state before:
pp: a b c : ℕ
r : ℤ
ha : a % 4 = 0
hb : b % 2 = 1
hc : a / 4 = c
hr : jacobiSymNat c b = r
⊢ jacobiSymNat a b = r

Tactic:
simp only [jacobiSymNat, ← hr, ← hc, Int.natCast_ediv, Nat.cast_ofNat]
  exact (jacobiSym.div_four_left (mod_cast ha) hb).symm

Goal state after:
Module: Mathlib.Topology.Algebra.ProperAction.Torsor

Goal state before:
pp: V : Type u_1
P : Type u_2
inst✝⁴ : Group V
inst✝³ : Torsor V P
inst✝² : TopologicalSpace V
inst✝¹ : TopologicalSpace P
inst✝ : IsTopologicalTorsor P
⊢ IsProperMap fun gx ↦ (gx.1 • gx.2, gx.2)

Tactic:
by
    let Φ : V × P ≃ₜ P × P :=
    { toFun vp := (vp.1 • vp.2, vp.2)
      invFun pq := (pq.1 /ₛ pq.2, pq.2)
      left_inv _ := by simp
      right_inv _ := by simp }
    exact Φ.isProperMap

Goal state after: