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

Goal state before:
pp: case cons
R : Type u_1
S : Type u_2
inst✝⁹ : CommRing R
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
inst✝⁶ : Flat R S
x : R
tail✝ : List R
ih :
  ∀ {M : Type u_3} {N : Type u_4} [inst : AddCommGroup M] [inst_1 : Module R M] [inst_2 : AddCommGroup N]
    [inst_3 : Module R N] [inst_4 : Module S N] [inst_5 : IsScalarTower R S N] {f : M →ₗ[R] N},
    IsBaseChange S f → IsWeaklyRegular M tail✝ → IsWeaklyRegular N (List.map (⇑(algebraMap R S)) tail✝)
M : Type u_3
N : Type u_4
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
inst✝¹ : Module S N
inst✝ : IsScalarTower R S N
f : M →ₗ[R] N
hf : IsBaseChange S f
reg : IsWeaklyRegular M (x :: tail✝)
⊢ IsWeaklyRegular N (List.map (⇑(algebraMap R S)) (x :: tail✝))

Tactic:
simp only [List.map_cons, isWeaklyRegular_cons_iff] at reg ⊢
    have e := (QuotSMulTop.algebraMapTensorEquivTensorQuotSMulTop x M S).symm ≪≫ₗ
      QuotSMulTop.congr ((algebraMap R S) x) hf.equiv
    have hg : IsBaseChange S <|
        e.toLinearMap.restrictScalars R ∘ₗ TensorProduct.mk R S (QuotSMulTop x M) 1 :=
      IsBaseChange.of_equiv e (fun _ ↦ by simp)
    exact ⟨reg.1.of_flat_of_isBaseChange hf, ih hg reg.2⟩

Goal state after:
Module: Mathlib.RingTheory.RegularLocalRing.Defs

Goal state before:
pp: case neg
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsLocalRing R
inst✝¹ : IsDomain R
inst✝ : IsPrincipalIdealRing R
isf : ¬IsField R
⊢ IsRegularLocalRing R

Tactic:
apply of_spanFinrank_maximalIdeal_le

Goal state after:
case neg
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsLocalRing R
inst✝¹ : IsDomain R
inst✝ : IsPrincipalIdealRing R
isf : ¬IsField R
⊢ ↑(Submodule.spanFinrank (maximalIdeal R)) ≤ ringKrullDim R
Module: Mathlib.RingTheory.RegularLocalRing.Defs

Goal state before:
pp: case pos
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDedekindDomain R
p : Ideal R
hp : p.IsPrime
eqbot : p = ⊥
⊢ IsRegularLocalRing (Localization.AtPrime p)

Tactic:
let : Field (Localization.AtPrime p) := IsField.toField <| by
      simp [isField_iff_maximalIdeal_eq, ← Localization.AtPrime.map_eq_maximalIdeal, eqbot]
    infer_instance

Goal state after:
Module: Mathlib.RingTheory.Regular.ProjectiveDimension

Goal state before:
pp: R : Type u
inst✝³ : CommRing R
inst✝² : Small.{v, u} R
inst✝¹ : IsNoetherianRing R
n : ℕ
M : ModuleCat R
inst✝ : Module.Finite R ↑M
w✝⁴ : Type v
w✝³ : AddCommGroup w✝⁴
w✝² : Module R w✝⁴
w✝¹ : Free R w✝⁴
w✝ : Module.Finite R w✝⁴
f✝ : w✝⁴ →ₗ[R] ↑M
surjf : Function.Surjective ⇑f✝
S : ShortComplex (ModuleCat R) := f✝.shortComplexKer
hS : S.ShortExact
hn :
  ∀ (M : ModuleCat R) [Module.Finite R ↑M],
    (∀ (L : ModuleCat R), Module.Finite R ↑L → Subsingleton (Ext M L 0)) → HasProjectiveDimensionLT M 0
h : ∀ (L : ModuleCat R), Module.Finite R ↑L → Subsingleton (Ext M L (0 + 1))
this : Subsingleton (Ext M S.X₁ 1)
f' : Ext M S.X₂ 0
hf' : f'.comp (Ext.mk₀ S.g) ⋯ = Ext.mk₀ (𝟙 M)
f : M ⟶ S.X₂
hf : Ext.mk₀ f = f'
⊢ CategoryTheory.Projective M

Tactic:
← hf,

Goal state after:
R : Type u
inst✝³ : CommRing R
inst✝² : Small.{v, u} R
inst✝¹ : IsNoetherianRing R
n : ℕ
M : ModuleCat R
inst✝ : Module.Finite R ↑M
w✝⁴ : Type v
w✝³ : AddCommGroup w✝⁴
w✝² : Module R w✝⁴
w✝¹ : Free R w✝⁴
w✝ : Module.Finite R w✝⁴
f✝ : w✝⁴ →ₗ[R] ↑M
surjf : Function.Surjective ⇑f✝
S : ShortComplex (ModuleCat R) := f✝.shortComplexKer
hS : S.ShortExact
hn :
  ∀ (M : ModuleCat R) [Module.Finite R ↑M],
    (∀ (L : ModuleCat R), Module.Finite R ↑L → Subsingleton (Ext M L 0)) → HasProjectiveDimensionLT M 0
h : ∀ (L : ModuleCat R), Module.Finite R ↑L → Subsingleton (Ext M L (0 + 1))
this : Subsingleton (Ext M S.X₁ 1)
f' : Ext M S.X₂ 0
f : M ⟶ S.X₂
hf' : (Ext.mk₀ f).comp (Ext.mk₀ S.g) ⋯ = Ext.mk₀ (𝟙 M)
hf : Ext.mk₀ f = f'
⊢ CategoryTheory.Projective M
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 = (coeff n) ((map (IsLocalRing.residue A)) g * (map (IsLocalRing.residue A)) q) + 0
⊢ IsUnit q

Tactic:
add_zero

Goal state after:
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 = (coeff n) ((map (IsLocalRing.residue A)) g * (map (IsLocalRing.residue A)) q)
⊢ IsUnit q
Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation

Goal state before:
pp: case refine_2
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
⊢ g = ↑f * ↑⋯.unit⁻¹

Tactic:
· have := congr($(H.2) * ↑(H.isUnit_of_map_ne_zero hg).unit⁻¹)
    rw [add_mul, mul_assoc, IsUnit.mul_val_inv, mul_one, ← sub_eq_iff_eq_add] at this
    simp_rw [← this, f, Polynomial.coe_sub, Polynomial.coe_pow, Polynomial.coe_X, sub_mul]

Goal state after:
Module: Mathlib.RingTheory.SimpleModule.Isotypic

Goal state before:
pp: R : Type u_2
M : Type u
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
c✝ : Submodule R M
hc : c✝ ∈ isotypicComponents R M
s : Set (Submodule R M) := isotypicComponents R M \ {c✝}
ne : ¬c✝ ⊓ sSup s = ⊥
this✝ : IsSemisimpleModule R ↥c✝
this : IsSemisimpleModule R ↥(c✝ ⊓ sSup s)
c : ↑s
⊢ IsSemisimpleModule R ↥↑c

Tactic:
obtain ⟨_, ⟨_, _, rfl⟩, _⟩ := c

Goal state after:
R : Type u_2
M : Type u
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
c : Submodule R M
hc : c ∈ isotypicComponents R M
s : Set (Submodule R M) := isotypicComponents R M \ {c}
ne : ¬c ⊓ sSup s = ⊥
this✝ : IsSemisimpleModule R ↥c
this : IsSemisimpleModule R ↥(c ⊓ sSup s)
w✝ : Submodule R M
left✝ : IsSimpleModule R ↥w✝
right✝ : isotypicComponent R M ↥w✝ ∉ {c}
⊢ IsSemisimpleModule R ↥↑⟨isotypicComponent R M ↥w✝, ⋯⟩
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Moebius

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

Tactic:
ha.squarefree.moebius_eq,

Goal state after:
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a : α
ha : Irreducible a
⊢ (-1) ^ (factors a).card = -1
Module: Mathlib.RingTheory.Smooth.Quotient

Goal state before:
pp: case add
R : Type u_1
inst✝ : CommRing R
J I : Ideal R
sq : I * I = ⊥
f : J.Cotangent →ₗ[R] J.Cotangent
le : f.range ≤ Submodule.map J.toCotangent (Submodule.comap (Submodule.subtype J) (I * J))
x y : R
ymem : y ∈ I * J
z : R
zmem : z ∈ I * J
hy : f (J.toCotangent ⟨y, ⋯⟩) = 0
hz : f (J.toCotangent ⟨z, ⋯⟩) = 0
this : ⟨y + z, ⋯⟩ = ⟨y, ⋯⟩ + ⟨z, ⋯⟩
⊢ 0 + 0 = 0

Tactic:
add_zero

Goal state after:
case add
R : Type u_1
inst✝ : CommRing R
J I : Ideal R
sq : I * I = ⊥
f : J.Cotangent →ₗ[R] J.Cotangent
le : f.range ≤ Submodule.map J.toCotangent (Submodule.comap (Submodule.subtype J) (I * J))
x y : R
ymem : y ∈ I * J
z : R
zmem : z ∈ I * J
hy : f (J.toCotangent ⟨y, ⋯⟩) = 0
hz : f (J.toCotangent ⟨z, ⋯⟩) = 0
this : ⟨y + z, ⋯⟩ = ⟨y, ⋯⟩ + ⟨z, ⋯⟩
⊢ 0 = 0
Module: Mathlib.RingTheory.WittVector.DiscreteValuationRing

Goal state before:
pp: case a
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : CommRing k
inst✝ : CharP k p
a : kˣ
A : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
hA : A.coeff 0 = ↑a
n : ℕ
a✝ : (A * { coeff := inverseCoeff a A }).coeff n = coeff 1 n
H_coeff : k := ⋯
H : ↑(a ^ p ^ (n + 1)) * ↑(a ^ p ^ (n + 1))⁻¹ = 1
⊢ (A * { coeff := inverseCoeff a A }).coeff (n + 1) + -H_coeff * 1 -
      (coeff 1 (n + 1) + -H_coeff * (↑(a ^ p ^ (n + 1)) * ↑(a ^ p ^ (n + 1))⁻¹)) =
    0

Tactic:
skip

Goal state after:
case a
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : CommRing k
inst✝ : CharP k p
a : kˣ
A : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
hA : A.coeff 0 = ↑a
n : ℕ
a✝ : (A * { coeff := inverseCoeff a A }).coeff n = coeff 1 n
H_coeff : k := ⋯
H : ↑(a ^ p ^ (n + 1)) * ↑(a ^ p ^ (n + 1))⁻¹ = 1
⊢ (A * { coeff := inverseCoeff a A }).coeff (n + 1) + -H_coeff * 1 -
      (coeff 1 (n + 1) + -H_coeff * (↑(a ^ p ^ (n + 1)) * ↑(a ^ p ^ (n + 1))⁻¹)) =
    0
Module: Mathlib.RingTheory.WittVector.MulCoeff

Goal state before:
pp: case e'_2.e_f
p : ℕ
hp : Fact (Nat.Prime p)
n i : ℕ
m✝ : Fin 2 × ℕ →₀ ℕ
⊢ MvPolynomial.coeff m✝ (↑p ^ i * wittStructureInt p (X 0 * X 1) i ^ p ^ (n - i)) =
    MvPolynomial.coeff m✝
      ((bind₁ (wittStructureInt p (X 0 * X 1))) ((monomial (Finsupp.single i (p ^ (n - i)))) (↑p ^ i)))

Tactic:
congr 1

Goal state after:
case e'_2.e_f.e_p
p : ℕ
hp : Fact (Nat.Prime p)
n i : ℕ
m✝ : Fin 2 × ℕ →₀ ℕ
⊢ ↑p ^ i * wittStructureInt p (X 0 * X 1) i ^ p ^ (n - i) =
    (bind₁ (wittStructureInt p (X 0 * X 1))) ((monomial (Finsupp.single i (p ^ (n - i)))) (↑p ^ i))
Module: Mathlib.RingTheory.WittVector.FrobeniusFractionField

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : CommRing k
inst✝¹ : CharP k p
inst✝ : IsDomain k
n : ℕ
a₁ a₂ : 𝕎 k
bs : Fin (n + 1) → k
ha₁ : a₁.coeff 0 ≠ 0
ha₂ : a₂.coeff 0 ≠ 0
this : (X ^ p * C (a₁.coeff 0 ^ p ^ (n + 1))).degree = ↑p
⊢ 1 + 0 < ↑p

pp: p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : CommRing k
inst✝¹ : CharP k p
inst✝ : IsDomain k
n : ℕ
a₁ a₂ : 𝕎 k
bs : Fin (n + 1) → k
ha₁ : a₁.coeff 0 ≠ 0
ha₂ : a₂.coeff 0 ≠ 0
this : (X ^ p * C (a₁.coeff 0 ^ p ^ (n + 1))).degree = ↑p
⊢ a₂.coeff 0 ^ p ^ (n + 1) ≠ 0

Tactic:
add_zero

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : CommRing k
inst✝¹ : CharP k p
inst✝ : IsDomain k
n : ℕ
a₁ a₂ : 𝕎 k
bs : Fin (n + 1) → k
ha₁ : a₁.coeff 0 ≠ 0
ha₂ : a₂.coeff 0 ≠ 0
this : (X ^ p * C (a₁.coeff 0 ^ p ^ (n + 1))).degree = ↑p
⊢ 1 < ↑p

p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : CommRing k
inst✝¹ : CharP k p
inst✝ : IsDomain k
n : ℕ
a₁ a₂ : 𝕎 k
bs : Fin (n + 1) → k
ha₁ : a₁.coeff 0 ≠ 0
ha₂ : a₂.coeff 0 ≠ 0
this : (X ^ p * C (a₁.coeff 0 ^ p ^ (n + 1))).degree = ↑p
⊢ a₂.coeff 0 ^ p ^ (n + 1) ≠ 0
Module: Mathlib.RingTheory.ZMod.Torsion

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
⊢ p - 1 ≠ 0

Tactic:
by have : 2 ≤ p := Nat.Prime.two_le Fact.out; grind

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 * (φ(p, k) c * a)) • x = (b * (↑p ^ m * φ(p, k) c)) • x

Tactic:
congr 1

Goal state after:
case h.e_a
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 * (φ(p, k) c * a) = b * (↑p ^ m * φ(p, k) c)
Module: Mathlib.SetTheory.Cardinal.UnivLE

Goal state before:
pp: ⊢ (∀ (α : Type u), Small.{v, u} α) ↔ univ.{u, v + 1} ≤ univ.{v, u + 1}

Tactic:
small_iff_lift_mk_lt_univ

Goal state after:
⊢ (∀ (α : Type u), lift.{v + 1, u} #α < univ.{v, max u (v + 1)}) ↔ univ.{u, v + 1} ≤ univ.{v, u + 1}
Module: Mathlib.SetTheory.Cardinal.Cofinality.Club

Goal state before:
pp: case h
α : Type v
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
f : α → α
hα : cof α ≠ ℵ₀
hf : IsNormal f
h✝ : Nonempty α
a : α
val✝ : OrderTop α
⊢ ⊤ ∈ Function.fixedPoints f ∧ a ≤ ⊤

Tactic:
simpa using! hf.strictMono.id_le ⊤

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

Goal state before:
pp: case neg.mp
A : Type u_1
T : ↥(tree A)
x y z : List A
hl : x.length ≤ z.length
hp : ¬x <+: z
h : List.take x.length z <+: x
right✝ : List.drop x.length z ∈ pullSub T y
⊢ z ∈ pullSub T (x ++ y)

Tactic:
skip

Goal state after:
case neg.mp
A : Type u_1
T : ↥(tree A)
x y z : List A
hl : x.length ≤ z.length
hp : ¬x <+: z
h : List.take x.length z <+: x
right✝ : List.drop x.length z ∈ pullSub T y
⊢ z ∈ pullSub T (x ++ y)
Module: Mathlib.SetTheory.Ordinal.CantorNormalForm

Goal state before:
pp: b o✝ : Ordinal.{u}
x : Ordinal.{u} × Ordinal.{u}
o : Ordinal.{u}
ho : o ≠ 0
IH : x ∈ CNF b (o % b ^ log b o) → 0 < x.2
⊢ x ∈ CNF b o → 0 < x.2

Tactic:
CNF.ne_zero ho

Goal state after:
b o✝ : Ordinal.{u}
x : Ordinal.{u} × Ordinal.{u}
o : Ordinal.{u}
ho : o ≠ 0
IH : x ∈ CNF b (o % b ^ log b o) → 0 < x.2
⊢ x ∈ (log b o, o / b ^ log b o) :: CNF b (o % b ^ log b o) → 0 < x.2
Module: Mathlib.SetTheory.Ordinal.CantorNormalForm

Goal state before:
pp: case refine_2
b o✝ : Ordinal.{u}
hb : 1 < b
x : Ordinal.{u} × Ordinal.{u}
o : Ordinal.{u}
ho : o ≠ 0
IH : x ∈ CNF b (o % b ^ log b o) → x.2 < b
⊢ x ∈ CNF b o → x.2 < b

Tactic:
CNF.ne_zero ho

Goal state after:
case refine_2
b o✝ : Ordinal.{u}
hb : 1 < b
x : Ordinal.{u} × Ordinal.{u}
o : Ordinal.{u}
ho : o ≠ 0
IH : x ∈ CNF b (o % b ^ log b o) → x.2 < b
⊢ x ∈ (log b o, o / b ^ log b o) :: CNF b (o % b ^ log b o) → x.2 < b
Module: Mathlib.SetTheory.Ordinal.CantorNormalForm

Goal state before:
pp: b o : Ordinal.{u_1}
⊢ (map Prod.fst (CNF b o)).Nodup

Tactic:
exact (CNF.sortedGT ..).nodup

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

Goal state before:
pp: case inl
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)) e = x + 0

Tactic:
add_zero

Goal state after:
case inl
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)) e = x
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
⊢ x + 0 = x

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' ∉ f.support

Tactic:
add_zero

Goal state after:
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
⊢ x = x

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' ∉ f.support
Module: Mathlib.SetTheory.Ordinal.Topology

Goal state before:
pp: case refine_1
s : Set Ordinal.{u}
hs : ¬BddAbove s
Hs : StrictMono (enumOrd s)
h : IsNormal (enumOrd s)
ι : Type u
hι : Nonempty ι
f : ι → Ordinal.{u}
hf : ∀ (i : ι), f i ∈ s
g : ι → Ordinal.{u} := fun i ↦ (enumOrdOrderIso s hs).symm ⟨f i, ⋯⟩
x : ι
⊢ enumOrd s (g x) = f x

Tactic:
change (enumOrdOrderIso s hs _).val = f x

Goal state after:
case refine_1
s : Set Ordinal.{u}
hs : ¬BddAbove s
Hs : StrictMono (enumOrd s)
h : IsNormal (enumOrd s)
ι : Type u
hι : Nonempty ι
f : ι → Ordinal.{u}
hf : ∀ (i : ι), f i ∈ s
g : ι → Ordinal.{u} := fun i ↦ (enumOrdOrderIso s hs).symm ⟨f i, ⋯⟩
x : ι
⊢ ↑((enumOrdOrderIso s hs) (g x)) = f x
Module: Mathlib.SetTheory.Ordinal.CantorNormalForm

Goal state before:
pp: case single_add.hxb
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
IH' : ∀ (e' : Ordinal.{u_1}), f e' < b
⊢ x + 0 = x

pp: case single_add.hxb
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
IH' : ∀ (e' : Ordinal.{u_1}), f e' < b
⊢ e ∉ f.support

Tactic:
add_zero

Goal state after:
case single_add.hxb
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
IH' : ∀ (e' : Ordinal.{u_1}), f e' < b
⊢ x = x

case single_add.hxb
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
IH' : ∀ (e' : Ordinal.{u_1}), f e' < b
⊢ e ∉ f.support
Module: Mathlib.SetTheory.Ordinal.Veblen

Goal state before:
pp: case inr
f : Ordinal.{u} → Ordinal.{u}
o a : Ordinal.{u}
hf : IsNormal f
h : 0 < o
⊢ veblenWith f o a ∈ range f

Tactic:
rw [← veblenWith_veblenWith_of_lt hf h]

Goal state after:
case inr
f : Ordinal.{u} → Ordinal.{u}
o a : Ordinal.{u}
hf : IsNormal f
h : 0 < o
⊢ veblenWith f 0 (veblenWith f o a) ∈ range f
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 β B).Func a) }
b : (PSet.mk β B).Type
pb : (fun y ↦ p (mk y)) ((PSet.mk β B).Func b)
a : α
ha : (A a).Equiv (B b)
⊢ (fun y ↦ p (mk y)) ((PSet.mk α A).Func a)

Tactic:
simpa only [mk_func, ZFSet.sound ha]

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

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

Tactic:
rw [← veblenWith_veblenWith_of_lt hf h]

Goal state after:
f : Ordinal.{u} → Ordinal.{u}
hf : IsNormal f
a o₁ o₂ : Ordinal.{u}
h : o₁ < o₂
⊢ veblenWith f o₁ a ≤ veblenWith f o₁ (veblenWith f o₂ a)
Module: Mathlib.SetTheory.Ordinal.Veblen

Goal state before:
pp: case inr
f : Ordinal.{u} → Ordinal.{u}
o a : Ordinal.{u}
hf : IsNormal f
hp : 0 < f 0
H : ∀ (b : Ordinal.{u}), 0 < veblenWith f 0 b
h : 0 < o
⊢ 0 < veblenWith f o a

Tactic:
rw [← veblenWith_veblenWith_of_lt hf h]

Goal state after:
case inr
f : Ordinal.{u} → Ordinal.{u}
o a : Ordinal.{u}
hf : IsNormal f
hp : 0 < f 0
H : ∀ (b : Ordinal.{u}), 0 < veblenWith f 0 b
h : 0 < o
⊢ 0 < veblenWith f 0 (veblenWith f o a)
Module: Mathlib.SetTheory.Ordinal.Veblen

Goal state before:
pp: f : Ordinal.{u} → Ordinal.{u}
hf : IsNormal f
hp : 0 < f 0
⊢ IsNormal fun x ↦ veblenWith f x 0

Tactic:
by
  rw [isNormal_iff]
  refine ⟨veblenWith_zero_strictMono hf hp, fun o ho a IH ↦ ?_⟩
  rw [veblenWith_of_ne_zero f ho.ne_bot, derivFamily_zero]
  apply nfpFamily_le fun l ↦ ?_
  suffices ∃ b < o, List.foldr _ 0 l ≤ veblenWith f b 0 by
    obtain ⟨b, hb, hb'⟩ := this
    exact hb'.trans (IH b hb)
  induction l with
  | nil => use 0; simpa using ho.bot_lt
  | cons a l IH =>
    obtain ⟨b, hb, hb'⟩ := IH
    refine ⟨_, ho.succ_lt (max_lt a.2 hb), ((veblenWith_right_strictMono hf _).monotone <|
      hb'.trans <| veblenWith_left_monotone hf _ <|
        (le_max_right a.1 b).trans (le_succ _)).trans ?_⟩
    rw [veblenWith_veblenWith_of_lt hf]
    rw [lt_succ_iff]
    exact le_max_left _ b

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

Goal state before:
pp: x y z : ZFSet.{u}
⊢ z ∈ x \ y ↔ z ∈ x ∧ z ∉ y

Tactic:
by simp [← sep_notMem]

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

Goal state before:
pp: f : Ordinal.{u} → Ordinal.{u}
o₁ o₂ a b : Ordinal.{u}
hf : IsNormal f
h : o₁ < o₂
| cmp (veblenWith f o₁ a) (veblenWith f o₂ b)

Tactic:
rw [← veblenWith_veblenWith_of_lt hf h]

Goal state after:
f : Ordinal.{u} → Ordinal.{u}
o₁ o₂ a b : Ordinal.{u}
hf : IsNormal f
h : o₁ < o₂
| cmp (veblenWith f o₁ a) (veblenWith f o₁ (veblenWith f o₂ b))
Module: Mathlib.SetTheory.Ordinal.Veblen

Goal state before:
pp: f : Ordinal.{u} → Ordinal.{u}
o₁ o₂ a b : Ordinal.{u}
hf : IsNormal f
h : o₂ < o₁
| cmp (veblenWith f o₁ a) (veblenWith f o₂ b)

Tactic:
rw [← veblenWith_veblenWith_of_lt hf h]

Goal state after:
f : Ordinal.{u} → Ordinal.{u}
o₁ o₂ a b : Ordinal.{u}
hf : IsNormal f
h : o₂ < o₁
| cmp (veblenWith f o₂ (veblenWith f o₁ a)) (veblenWith f o₂ b)
Module: Mathlib.SetTheory.ZFC.Rank

Goal state before:
pp: o : Ordinal.{u_1}
α✝ : Type u_1
A : α✝ → PSet.{u_1}
h : ∀ ⦃y : PSet.{u_1}⦄, y ∈ mk α✝ A → y.rank < o
a : α✝
⊢ succ (A a).rank ≤ o

Tactic:
succ_le_iff

Goal state after:
o : Ordinal.{u_1}
α✝ : Type u_1
A : α✝ → PSet.{u_1}
h : ∀ ⦃y : PSet.{u_1}⦄, y ∈ mk α✝ A → y.rank < o
a : α✝
⊢ (A a).rank < o
Module: Mathlib.SetTheory.ZFC.Rank

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

Tactic:
succ_le_iff

Goal state after:
case a
x : PSet.{u_1}
⊢ x.rank < x.powerset.rank
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: case pos
e₁ : ONote
n₁ : ℕ+
a₁ : ONote
b₁ : Ordinal.{0}
h₁ : (e₁.oadd n₁ a₁).NFBelow b₁
e₂ : ONote
n₂ : ℕ+
a₂ : ONote
b₂ : Ordinal.{0}
h₂ : (e₂.oadd n₂ a₂).NFBelow b₂
IH : (e₁.oadd n₁ a₁ * a₂).NFBelow (e₁.repr + e₂.repr)
e0 : e₂ = 0
⊢ e₁.repr ≤ e₁.repr + 0

Tactic:
add_zero

Goal state after:
case pos
e₁ : ONote
n₁ : ℕ+
a₁ : ONote
b₁ : Ordinal.{0}
h₁ : (e₁.oadd n₁ a₁).NFBelow b₁
e₂ : ONote
n₂ : ℕ+
a₂ : ONote
b₂ : Ordinal.{0}
h₂ : (e₂.oadd n₂ a₂).NFBelow b₂
IH : (e₁.oadd n₁ a₁ * a₂).NFBelow (e₁.repr + e₂.repr)
e0 : e₂ = 0
⊢ e₁.repr ≤ e₁.repr
Module: Mathlib.Tactic.Algebra.Lemmas

Goal state before:
pp: A : Type u_2
sA : CommSemiring A
a₁ a₂ b₁ b₂ : A
ha : a₁ = b₁
hb : a₂ = b₂
⊢ a₁ + a₂ = b₁ + b₂

Tactic:
subst_vars
  rfl

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

Goal state before:
pp: A : Type u_2
e₁ e₂ a b : A
ha : e₁ = a
hb : e₂ = b
hab : a = b
⊢ e₁ = e₂

Tactic:
subst_vars
  rfl

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

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

Tactic:
simp only [α', ω0, R, R', ONote.repr_scale, ONote.repr,
        ONote.mulNat_eq_mul, ONote.opowAux, ONote.repr_ofNat, ONote.repr_mul, ONote.repr_add,
        Ordinal.opow_mul, ONote.zero_add]

Goal state after: