mathlib-initiative/mathlib-tactics huggingface dataset:
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
M : ModuleCat R
inst✝ : Module.Finite R ↑M
x : R
reg : IsSMulRegular (↑M) x
mem : x ∈ maximalIdeal R
⊢ projectiveDimension (of R (QuotSMulTop x ↑M)) = projectiveDimension M + 1

Tactic:
have sub : Subsingleton M ↔ Subsingleton (QuotSMulTop x M) := by
    refine ⟨fun h ↦ inferInstance, fun h ↦ ?_⟩
    contrapose! h
    exact (nontrivial_quotSMulTop_of_mem_maximalIdeal M mem)
  have aux (n : ℕ) : projectiveDimension (ModuleCat.of R (QuotSMulTop x M)) ≤ n ↔
    projectiveDimension M + 1 ≤ n := by
    match n with
    | 0 =>
      rw [projectiveDimension_le_iff]
      simp only [HasProjectiveDimensionLE, zero_add, ← projective_iff_hasProjectiveDimensionLT_one,
        CharP.cast_eq_zero, ENat.WithBot.add_one_le_zero_iff, projectiveDimension_eq_bot_iff,
        ModuleCat.isZero_iff_subsingleton, sub, ← IsProjective.iff_projective]
      refine ⟨fun h ↦ ?_, fun h ↦ Projective.of_free⟩
      have : Module.Free R (QuotSMulTop x M) := Module.free_of_flat_of_isLocalRing
      by_contra! ntr
      have := QuotSMulTop.mem_annihilator M x
      simp only [annihilator_eq_bot.mpr inferInstance, Submodule.mem_bot] at this
      simp only [this, IsSMulRegular.zero_iff_subsingleton] at reg
      absurd not_subsingleton_iff_nontrivial.mpr ntr
      infer_instance
    | n + 1 =>
      nth_rw 2 [← Nat.cast_one, Nat.cast_add]
      simp only [ENat.WithBot.add_le_add_natCast_right_iff, projectiveDimension_le_iff]
      let S := M.smulShortComplex x
      have hS : S.ShortExact := reg.smulShortComplex_shortExact
      refine ⟨fun h ↦ ?_, fun h ↦ hS.hasProjectiveDimensionLT_X₃ (n + 1) h
        (hasProjectiveDimensionLT_of_ge M (n + 1) (n + 2) (Nat.le_add_right _ 1))⟩
      apply hasProjectiveDimensionLT_of_forall_finite
      intro L _
      have zero := HasProjectiveDimensionLT.subsingleton (ModuleCat.of R (QuotSMulTop x M))
        (n + 2) _ (le_refl _) L
      have exac := Ext.contravariant_sequence_exact₁' hS L (n + 1) (n + 2) (add_comm 1 (n + 1))
      have epi := exac.epi_f ((@AddCommGrpCat.isZero_of_subsingleton _ zero).eq_zero_of_tgt _)
      have : S.f = x • 𝟙 M := rfl
      simp only [S, this, AddCommGrpCat.epi_iff_surjective, AddCommGrpCat.hom_ofHom] at epi
      by_contra! ntr
      have : x ∈ (Module.annihilator R (Ext M L (n + 1))).jacobson :=
        (IsLocalRing.maximalIdeal_le_jacobson _) mem
      absurd Submodule.top_ne_pointwise_smul_of_mem_jacobson_annihilator this
      rw [eq_comm, eq_top_iff]
      intro y hy
      rcases epi y with ⟨z, hz⟩
      simp only [ModuleCat.smulShortComplex, Ext.mk₀_smul,
        Ext.bilinearComp_apply_apply, Ext.smul_comp, Ext.mk₀_id_comp] at hz
      simpa [← hz] using Submodule.smul_mem_pointwise_smul _ _ ⊤ trivial
  refine eq_of_forall_ge_iff (fun N ↦ ?_)
  induction N with
  | bot =>
    simpa [projectiveDimension_eq_bot_iff, ModuleCat.isZero_iff_subsingleton] using sub.symm
  | coe N =>
    induction N with
    | top => simp
    | coe n => simpa using aux n

Goal state after:
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 = (IsLocalRing.residue A) (constantCoeff q) * (IsLocalRing.residue A) ((coeff (n, 0).1) g)
⊢ IsUnit ((IsLocalRing.residue A) (constantCoeff q))

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)}
⊢ (coeff p.1) ((map (IsLocalRing.residue A)) g) * (coeff p.2) ((map (IsLocalRing.residue A)) q) = 0

Tactic:
· exact .of_mul_eq_one _ H2.symm

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 =
    ∑ 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)}
⊢ (coeff p.1) ((map (IsLocalRing.residue A)) g) * (coeff p.2) ((map (IsLocalRing.residue A)) q) = 0
Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation

Goal state before:
pp: case eq_mul_add
A : Type u_1
inst✝¹ : CommRing A
inst✝ : IsLocalRing A
g : A⟦X⟧
f : A[X]
h : A⟦X⟧
H : g.IsWeierstrassFactorization f h
n : ℕ := ⋯
hn : n = ((map (IsLocalRing.residue A)) g).order.toNat
⊢ X ^ n = g * ↑⋯.unit⁻¹ + ↑(Polynomial.X ^ n - f)

Tactic:
· simp_rw [H.eq_mul, mul_assoc, IsUnit.mul_val_inv, mul_one, Polynomial.coe_sub,
      Polynomial.coe_pow, Polynomial.coe_X, add_sub_cancel]

Goal state after:
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✝ : IsSimpleModule R S
s : Set ↑(isotypicComponents R M)
c : ↑(isotypicComponents R M)
hc : c ∈ {c | ↑c ≤ ↑(⨆ c ∈ s, ⟨↑c, ⋯⟩)}
hcs : c ∉ s
⊢ ⨆ i ∈ s, ↑i ≤ sSup (isotypicComponents R M \ {↑c})

Tactic:
iSup₂_le_iff

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✝ : IsSimpleModule R S
s : Set ↑(isotypicComponents R M)
c : ↑(isotypicComponents R M)
hc : c ∈ {c | ↑c ≤ ↑(⨆ c ∈ s, ⟨↑c, ⋯⟩)}
hcs : c ∉ s
⊢ ∀ i ∈ s, ↑i ≤ sSup (isotypicComponents R M \ {↑c})
Module: Mathlib.RingTheory.SimpleModule.WedderburnArtin

Goal state before:
pp: R : Type u
inst✝² : Ring R
inst✝¹ : IsSimpleRing R
inst✝ : IsArtinianRing R
n : ℕ
hn : NeZero n
S : Submodule R R
hS : IsSimpleModule R ↥S
e : R ≃ₗ[R] Fin n → ↥S
⊢ Rᵐᵒᵖ ≃+* Matrix (Fin n) (Fin n) (Module.End R ↥S)

Tactic:
exact .trans (.moduleEndSelf R) <| .trans e.conjRingEquiv (endVecRingEquivMatrixEnd ..)

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

Goal state before:
pp: case inr.inr.refine_1
α : 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
hg : BddAbove (range g)
t : Set α
ht : t ∈ s
n : ℕ
⊢ (fun n ↦ f ⟨t, ht⟩ (g n)) n ≤ sSup (range g)

Tactic:
apply (le_csSup (.of_not_isCofinal _) _).trans (le_csSup hg ⟨n + 1, rfl⟩)
      · exact fun hg' ↦ (cof_le hg').not_gt (mk_range_le.trans_lt hsα)
      · use ⟨t, ht⟩

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

Goal state before:
pp: case inr.refine_1
α : Type v
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
f : α → α
hα : cof α ≠ ℵ₀
hf : IsNormal f
h✝ : Nonempty α
s : Set α
hs : s ⊆ Function.fixedPoints f
hs₀ : s.Nonempty
x✝ : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s
a : α
ha : IsLUB s a
⊢ IsLUB (f '' s) a

Tactic:
image_congr hs,

Goal state after:
case inr.refine_1
α : Type v
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
f : α → α
hα : cof α ≠ ℵ₀
hf : IsNormal f
h✝ : Nonempty α
s : Set α
hs : s ⊆ Function.fixedPoints f
hs₀ : s.Nonempty
x✝ : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) s
a : α
ha : IsLUB s a
⊢ IsLUB ((fun a ↦ a) '' s) a
Module: Mathlib.SetTheory.Cardinal.Cofinality.Club

Goal state before:
pp: α : Type v
inst✝² : LinearOrder α
inst✝¹ : WellFoundedLT α
inst✝ : IsRegularCardinalOrder α
s : Set α
hs : IsCofinal s
⊢ IsNormal (Subtype.val ∘ ⇑(enum s hs)) ↔ DirSupClosed s ∧ IsCofinal s

Tactic:
hs,

Goal state after:
α : Type v
inst✝² : LinearOrder α
inst✝¹ : WellFoundedLT α
inst✝ : IsRegularCardinalOrder α
s : Set α
hs : IsCofinal s
⊢ IsNormal (Subtype.val ∘ ⇑(enum s hs)) ↔ DirSupClosed s ∧ True
Module: Mathlib.SetTheory.Ordinal.Commute

Goal state before:
pp: case right
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} := ⋯
hsub : o₁ + o₃ = o₂
hcomm' : AddCommute o₁ o₃
hlt : o₁ + o₃ < o₁ + o₂
o : Ordinal.{u_1}
n₁ n₃ : ℕ
hn₁ : o * ↑n₁ = o₁
hn₃ : o * ↑n₃ = o₃
⊢ o * ↑(n₁ + n₃) = o₂

Tactic:
rw [Nat.cast_add, mul_add, hn₁, hn₃, hsub]

Goal state after:
Module: Mathlib.SetTheory.Lists

Goal state before:
pp: α : Type u_1
a y : Lists α
l : Lists' α true
⊢ a ∈ cons y l ↔ a ~ y ∨ a ∈ l

Tactic:
by
  simp [mem_def, or_and_right, exists_or]

Goal state after:
Module: Mathlib.SetTheory.Lists

Goal state before:
pp: α : Type u_1
trans : Lists α → Prop := fun l₁ ↦ ∀ ⦃l₂ l₃ : Lists α⦄, l₁ ~ l₂ → l₂ ~ l₃ → l₁ ~ l₃
⊢ ∀ {l₁ l₂ l₃ : Lists α}, l₁ ~ l₂ → l₂ ~ l₃ → l₁ ~ l₃

Tactic:
suffices PProd (∀ l₁, trans l₁) (∀ (l : Lists' α true), ∀ l' ∈ l.toList, trans l') by exact this.1

Goal state after:
α : Type u_1
trans : Lists α → Prop := fun l₁ ↦ ∀ ⦃l₂ l₃ : Lists α⦄, l₁ ~ l₂ → l₂ ~ l₃ → l₁ ~ l₃
⊢ (∀ (l₁ : Lists α), trans l₁) ×' ∀ (l : Lists' α true) (l' : Lists α), l' ∈ l.toList → trans l'
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
⊢ ⨆ b_1, ⨆ (_ : b_1 < b), f (lfpApprox f x b_1) ≤ lfpApprox f x a

Tactic:
iSup₂_le_iff

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
⊢ ∀ i < b, f (lfpApprox f x i) ≤ lfpApprox f x a
Module: Mathlib.SetTheory.Lists

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
b : Bool
a : Lists' α b
l₁ l₂ : Lists' α true
⊢ sizeOf ⟨b, a⟩ < 1 + 1 + sizeOf a + sizeOf l₁

Tactic:
simp [sizeof_pos]

Goal state after:
Module: Mathlib.SetTheory.Lists

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
a : Lists α
b✝ : Bool
b : Lists' α b✝
l₂ : Lists' α true
⊢ sizeOf ⟨b✝, b⟩ < 1 + 1 + sizeOf b + sizeOf l₂

Tactic:
simp [sizeof_pos]

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

Goal state before:
pp: case inr
o₁ e₁ : ONote
n₁ : ℕ+
a₁ : ONote
h✝¹ : o₁ = e₁.oadd n₁ a₁
o₂ : ONote
n₂ : ℕ+
a₂ : ONote
h₁ : (namedPattern o₁ (e₁.oadd n₁ a₁) h✝¹).NF
h✝ : o₂ = e₁.oadd n₂ a₂
h₂ : (namedPattern o₂ (e₁.oadd n₂ a₂) h✝).NF
nh : ↑n₂ ≤ ↑n₁ ∧ (↑n₂ < ↑n₁ ∧ Ordering.gt = Ordering.lt ∨ ¬↑n₂ < ↑n₁ ∧ Ordering.eq = Ordering.lt)
⊢ (Ordering.eq.then (Ordering.lt.then (a₁.cmp a₂))).Compares (namedPattern o₁ (e₁.oadd n₁ a₁) h✝¹)
    (namedPattern o₂ (e₁.oadd n₂ a₂) h✝)

Tactic:
rcases nh.right with nh | nh <;> cases nh <;> contradiction

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

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

Tactic:
by
  obtain rfl | h := eq_zero_or_pos o
  · simp
  · rw [← veblenWith_veblenWith_of_lt hf h]
    simp

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

Goal state before:
pp: case nil
f : Ordinal.{u} → Ordinal.{u}
hf : IsNormal f
hp : 0 < f 0
o : Ordinal.{u}
ho : IsSuccLimit o
a : Ordinal.{u}
IH : ∀ b < o, veblenWith f b 0 ≤ a
⊢ ∃ b < o, List.foldr (fun x ↦ veblenWith f ↑x) 0 [] ≤ veblenWith f b 0

Tactic:
use 0

Goal state after:
case h
f : Ordinal.{u} → Ordinal.{u}
hf : IsNormal f
hp : 0 < f 0
o : Ordinal.{u}
ho : IsSuccLimit o
a : Ordinal.{u}
IH : ∀ b < o, veblenWith f b 0 ≤ a
⊢ 0 < o ∧ List.foldr (fun x ↦ veblenWith f ↑x) 0 [] ≤ veblenWith f 0 0
Module: Mathlib.SetTheory.Ordinal.Veblen

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

Tactic:
lt_succ_iff

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

Goal state before:
pp: case a
x : PSet.{u_1}
⊢ ∀ ⦃y : PSet.{u_1}⦄, y ⊆ x → y.rank < succ x.rank

Tactic:
lt_succ_iff

Goal state after:
case a
x : PSet.{u_1}
⊢ ∀ ⦃y : PSet.{u_1}⦄, y ⊆ x → y.rank ≤ x.rank
Module: Mathlib.SetTheory.ZFC.Basic

Goal state before:
pp: p : ZFSet.{u} → Prop
x : ZFSet.{u}
⊢ Hereditarily p x ↔ p x ∧ ∀ y ∈ x, Hereditarily p y

Tactic:
← Hereditarily

Goal state after:
p : ZFSet.{u} → Prop
x : ZFSet.{u}
⊢ Hereditarily p x ↔ Hereditarily p x
Module: Mathlib.SetTheory.Ordinal.Veblen

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

Tactic:
apply (gamma_le_gamma.2 zero_le).trans_lt'

Goal state after:
o : Ordinal.{u_1}
⊢ ε_ 0 < Γ_ 0
Module: Mathlib.SetTheory.ZFC.Class

Goal state before:
pp: case mpr
x : Class.{u_1}
y : ZFSet.{u_1}
⊢ (∃ z, x z ∧ y ∈ z) → (⋃₀ x) y

Tactic:
· exact fun ⟨z, hxz, hyz⟩ => ⟨_, coe_mem.2 hxz, hyz⟩

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

Goal state before:
pp: case mp
x : Class.{u}
w : ZFSet.{u}
z : Set ZFSet.{u}
hzx : z ∈ x.classToCong
hwz : w ∈ z
⊢ ∃ z ∈ x, ↑w ∈ z

Tactic:
exact ⟨z, hzx, coe_mem.2 hwz⟩

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

Goal state before:
pp: case mpr
x : ZFSet.{u}
h : ⋃₀ x ⊆ x
y : ZFSet.{u}
hy : y ∈ x
⊢ y ⊆ x

Tactic:
· exact fun z hz ↦ h <| mem_sUnion_of_mem hz hy

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

Goal state before:
pp: case pos
x✝ y✝ x y : ZFSet.{u}
IH :
  ∀ (a₂ b₂ : ZFSet.{u}),
    Sym2.GameAdd (fun x1 x2 ↦ x1 ∈ x2) s(a₂, b₂) s(x, y) → a₂.IsOrdinal → b₂.IsOrdinal → a₂ ⊆ b₂ → a₂ = b₂ ∨ a₂ ∈ b₂
hx : x.IsOrdinal
hy : y.IsOrdinal
hxy : x ⊆ y
hyx : y ⊆ x
⊢ x = y ∨ x ∈ y

pp: case neg
x✝ y✝ x y : ZFSet.{u}
IH :
  ∀ (a₂ b₂ : ZFSet.{u}),
    Sym2.GameAdd (fun x1 x2 ↦ x1 ∈ x2) s(a₂, b₂) s(x, y) → a₂.IsOrdinal → b₂.IsOrdinal → a₂ ⊆ b₂ → a₂ = b₂ ∨ a₂ ∈ b₂
hx : x.IsOrdinal
hy : y.IsOrdinal
hxy : x ⊆ y
hyx : ¬y ⊆ x
⊢ x = y ∨ x ∈ y

Tactic:
· exact Or.inl (subset_antisymm hxy hyx)

Goal state after:
case neg
x✝ y✝ x y : ZFSet.{u}
IH :
  ∀ (a₂ b₂ : ZFSet.{u}),
    Sym2.GameAdd (fun x1 x2 ↦ x1 ∈ x2) s(a₂, b₂) s(x, y) → a₂.IsOrdinal → b₂.IsOrdinal → a₂ ⊆ b₂ → a₂ = b₂ ∨ a₂ ∈ b₂
hx : x.IsOrdinal
hy : y.IsOrdinal
hxy : x ⊆ y
hyx : ¬y ⊆ x
⊢ x = y ∨ x ∈ y
Module: Mathlib.SetTheory.ZFC.Ordinal

Goal state before:
pp: case a
o : Ordinal.{u_1}
a✝ : PSet.{u_1}
⊢ a✝ ∈ o.toPSet ↔ ∃ a < o, a.toZFSet = mk a✝

Tactic:
mem_toPSet_iff

Goal state after:
case a
o : Ordinal.{u_1}
a✝ : PSet.{u_1}
⊢ (∃ a < o, a✝.Equiv a.toPSet) ↔ ∃ a < o, a.toZFSet = mk a✝
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: case neg
x : ONote
inst✝ : x.NF
e : ONote
n : ℕ+
a : ONote
h : (e.oadd n a).NF
this : a.NF
e0 : ¬e = 0
⊢ (x + e).oadd n (x.scale a) = Mul.mul (x.oadd 1 0) (e.oadd n a)

Tactic:
simp [e0, Mul.mul, mul, scale_eq_mul, (· * ·)]

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

Goal state before:
pp: case pos.succ
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
k0 : k = 0
m : ℕ
h : a'.repr + ↑(m + 1) < ω ^ a0.repr
R' : Ordinal.{0} := (opowAux 0 a0 (a0.oadd n a' * ↑(m + 1)) (k + 1) (m + 1)).repr
R : Ordinal.{0} := (opowAux 0 a0 (a0.oadd n a' * ↑(m + 1)) k (m + 1)).repr
IH : (k ≠ 0 → R < ω0 ^ succ ↑k) ∧ ω0 ^ ↑k * α' + R = (α' + ↑(m + 1)) ^ succ ↑k
RR : R' = ω0 ^ ↑k * (α' * ↑(m + 1)) + R
⊢ (opowAux 0 a0 (a0.oadd n a' * ↑(m + 1)) 0 (m + 1)).repr < ω ^ 1

Tactic:
· simpa [opowAux] using natCast_lt_omega0 (m + 1)

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

Goal state before:
pp: α : Type u_1
𝕜 : Type u_2
inst✝⁵ : Field 𝕜
inst✝⁴ : LinearOrder 𝕜
inst✝³ : IsStrictOrderedRing 𝕜
inst✝² : TopologicalSpace 𝕜
inst✝¹ : OrderTopology 𝕜
f : 𝕜 → α
c : 𝕜
inst✝ : TopologicalSpace α
a b : α
h_neg : Tendsto (fun x ↦ f (c - x⁻¹)) atTop (𝓝 a)
h_pos : Tendsto (fun x ↦ f (c + x⁻¹)) atTop (𝓝 b)
h_eq : a = b
⊢ Tendsto f (𝓝[≠] c) (𝓝 a)

Tactic:
apply tendsto_nhdsNE_of_tendsto_atTop _ _ h_neg
  convert! h_pos

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

Goal state before:
pp: case hbc
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} := ⋯
R : Ordinal.{0} := ⋯
ω0 : Ordinal.{0} := ⋯
α' : Ordinal.{0} := ⋯
IH : (k ≠ 0 → R < ω0 ^ succ ↑k) ∧ ω0 ^ ↑k * α' + R = (α' + ↑m) ^ succ ↑k
RR : R' = ω0 ^ ↑k * (α' * ↑m) + R
α0✝ : 0 < α'
ω00 : 0 < ω0 ^ ↑k
Rl : R < ω ^ (a0.repr * succ ↑k)
αd : ω ∣ α'
α0 : ¬IsMin α'
⊢ a'.repr < ω ^ a0.repr

Tactic:
exact No.snd'.repr_lt

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' : β
C : ℝ
hC : ∀ (a b : Stream'.Seq α), dist a b ≤ C
⊢ BddAbove (Set.range fun b ↦ dist (f b) (g b))

Tactic:
use C

Goal state after:
case h
α : Type u_1
β : Type u_2
γ : Type u_3
F : β → Option (α × γ × β)
op : γ → Stream'.Seq α → Stream'.Seq α
h : FriendlyOperationClass op
T : (β →ᵤ Stream'.Seq α) → β →ᵤ Stream'.Seq α := ⋯
f g : β →ᵤ Stream'.Seq α
b : β
a : α
c : γ
b' : β
C : ℝ
hC : ∀ (a b : Stream'.Seq α), dist a b ≤ C
⊢ C ∈ upperBounds (Set.range fun b ↦ dist (f b) (g b))
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: case succ.refine_2.e_a.succ
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
n✝ : ℕ
h : a'.repr + ↑(n✝ + 1) < ω ^ a0.repr
R' : Ordinal.{0} := (opowAux 0 a0 (a0.oadd n a' * ↑(n✝ + 1)) (k + 1) (n✝ + 1)).repr
R : Ordinal.{0} := (opowAux 0 a0 (a0.oadd n a' * ↑(n✝ + 1)) k (n✝ + 1)).repr
IH : (k ≠ 0 → R < ω0 ^ succ ↑k) ∧ ω0 ^ ↑k * α' + R = (α' + ↑(n✝ + 1)) ^ succ ↑k
RR : R' = ω0 ^ ↑k * (α' * ↑(n✝ + 1)) + R
Rl : R < ω ^ (a0.repr * succ ↑k)
⊢ ω0 ^ ↑k * α' * ↑(n✝ + 1) + R = (ω0 ^ ↑k * α' + R) * ↑(n✝ + 1)

Tactic:
· rw [Nat.cast_add_one, ← succ_eq_add_one, add_mul_succ]
      apply add_of_omega0_opow_le Rl
      rw [opow_mul, opow_succ]
      gcongr
      simpa [repr] using omega0_le_oadd a0 n a'

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

Goal state before:
pp: case succ
basis_hd : ℝ → ℝ
basis_tl : Basis
r : ℝ
m : ℕ
⊢ (Multiseries.monomialRpow basis_hd basis_tl (m + 1) r).Sorted

Tactic:
simp only [Multiseries.monomialRpow]
    exact Sorted.cons_nil monomialRpow_sorted

Goal state after:
Module: Mathlib.Tactic.DeriveEncodable

Goal state before:
pp: a b : ℕ
h : a ≠ 0
this✝ : a ≤ a * a
this : b ≤ b * b
⊢ b < if a < b then b * b + a else a * a + a + b

Tactic:
split

Goal state after:
case isTrue
a b : ℕ
h : a ≠ 0
this✝ : a ≤ a * a
this : b ≤ b * b
h✝ : a < b
⊢ b < b * b + a

case isFalse
a b : ℕ
h : a ≠ 0
this✝ : a ≤ a * a
this : b ≤ b * b
h✝ : ¬a < b
⊢ b < a * a + a + b
Module: Mathlib.Tactic.DeriveEncodable

Goal state before:
pp: case ind
n : ℕ
ih : ∀ m < n, (S.decode m).encode = m
⊢ (if h : (Nat.unpair n).1 = 0 then S.nat (Nat.unpair n).2
      else (S.decode ((Nat.unpair n).1 - 1)).cons (S.decode (Nat.unpair n).2)).encode =
    n

Tactic:
split

Goal state after:
case ind.isTrue
n : ℕ
ih : ∀ m < n, (S.decode m).encode = m
h✝ : (Nat.unpair n).1 = 0
⊢ (S.nat (Nat.unpair n).2).encode = n

case ind.isFalse
n : ℕ
ih : ∀ m < n, (S.decode m).encode = m
h✝ : ¬(Nat.unpair n).1 = 0
⊢ ((S.decode ((Nat.unpair n).1 - 1)).cons (S.decode (Nat.unpair n).2)).encode = n
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: ⊢ fastGrowing 2 = fun n ↦ 2 ^ n * n

Tactic:
rw [@fastGrowing_succ 2 1 rfl]

Goal state after:
⊢ (fun i ↦ (fastGrowing 1)^[i] i) = fun n ↦ 2 ^ n * n
Module: Mathlib.Testing.Plausible.Functions

Goal state before:
pp: α : Type u
inst✝ : DecidableEq α
xs : List (α × α)
x y z : α
⊢ applyId ((y, z) :: xs) x = if y = x then z else applyId xs x

Tactic:
simp only [List.applyId, List.dlookup, eq_rec_constant, Prod.toSigma, List.map]
  split_ifs <;> rfl

Goal state after:
Module: Mathlib.Testing.Plausible.Functions

Goal state before:
pp: case some
α : Type u
inst✝ : DecidableEq α
xs ys : List α
h₀ : xs.Nodup
h₁ : xs ~ ys
x val : α
h₃ : dlookup x (map Prod.toSigma (xs.zip ys)) = some val
⊢ (some val).getD x ∈ ys ↔ x ∈ xs

Tactic:
have h₂ : ys.Nodup := h₁.nodup_iff.1 h₀
    replace h₁ : xs.length = ys.length := h₁.length_eq
    dsimp
    induction xs generalizing ys with
    | nil => contradiction
    | cons x' xs xs_ih =>
      rcases ys with - | ⟨y, ys⟩
      · cases h₃
      simp only [zip_cons_cons, map_cons, Prod.toSigma_mk, dlookup, eq_rec_constant,
        dite_eq_ite] at h₃
      split_ifs at h₃ with h
      · rw [Option.some_inj] at h₃
        subst x'; subst val
        simp only [List.mem_cons, true_or]
      · obtain - | ⟨h₀, h₅⟩ := h₀
        obtain - | ⟨h₂, h₄⟩ := h₂
        have h₆ := Nat.succ.inj h₁
        specialize xs_ih h₅ h₃ h₄ h₆
        simp only [Ne.symm h, xs_ih, List.mem_cons]
        suffices val ∈ ys by tauto
        rw [← Option.mem_def, List.mem_dlookup_iff] at h₃
        · simp only [Prod.toSigma, List.mem_map, Prod.exists] at h₃
          rcases h₃ with ⟨a, b, h₃, h₄, h₅⟩
          apply (List.of_mem_zip h₃).2
        simp only [List.NodupKeys, List.keys, comp_def, Prod.fst_toSigma, List.map_map]
        rwa [List.map_fst_zip (le_of_eq h₆)]

Goal state after:
Module: Mathlib.Topology.Algebra.Module.EmbeddingOfLocal

Goal state before:
pp: 𝕜₁ : Type u_1
𝕜₂ : Type u_2
E : Type u_3
F : Type u_4
inst✝¹² : NontriviallyNormedField 𝕜₁
inst✝¹¹ : NontriviallyNormedField 𝕜₂
inst✝¹⁰ : AddCommGroup E
inst✝⁹ : AddCommGroup F
inst✝⁸ : Module 𝕜₁ E
inst✝⁷ : Module 𝕜₂ F
σ : 𝕜₁ →+* 𝕜₂
f : E →ₛₗ[σ] F
inst✝⁶ : TopologicalSpace E
inst✝⁵ : TopologicalSpace F
inst✝⁴ : IsTopologicalAddGroup E
inst✝³ : IsTopologicalAddGroup F
inst✝² : ContinuousSMul 𝕜₁ E
inst✝¹ : ContinuousSMul 𝕜₂ F
inst✝ : RingHomIsometric σ
V : Set E
V_mem : V ∈ 𝓝 0
H : IsEmbedding (V.domRestrict ⇑f)
⊢ IsEmbedding ⇑f

Tactic:
by
  refine ⟨isInducing_of_restrict_nhds_zero V_mem H.isInducing, ?_⟩
  have f_injOn : InjOn f V := injOn_iff_injective.2 H.injective
  rw [← LinearMap.ker_eq_bot, Submodule.eq_bot_iff]
  intro x hx
  obtain ⟨c, hc, c_ne : c ≠ 0⟩ := absorbent_nhds_zero (𝕜 := 𝕜₁) V_mem
    |>.eventually_nhdsNE_zero x |>.and eventually_mem_nhdsWithin |>.exists
  rw [← smul_eq_zero_iff_right c_ne, ← f_injOn.eq_iff hc (mem_of_mem_nhds V_mem), map_zero,
    map_smulₛₗ, hx, smul_zero]

Goal state after:
Module: Mathlib.Topology.Algebra.Ring.Compact

Goal state before:
pp: R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : TopologicalSpace R
inst✝³ : IsTopologicalRing R
inst✝² : CompactSpace R
inst✝¹ : T2Space R
inst✝ : IsArtinianRing R
n : ℕ
hn : ⊥.jacobson ^ n = 0
⊢ (∏ p, p.asIdeal) ^ n = ⊥

Tactic:
rw [← le_bot_iff, ← Ideal.zero_eq_bot, ← hn]

Goal state after:
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : TopologicalSpace R
inst✝³ : IsTopologicalRing R
inst✝² : CompactSpace R
inst✝¹ : T2Space R
inst✝ : IsArtinianRing R
n : ℕ
hn : ⊥.jacobson ^ n = 0
⊢ (∏ p, p.asIdeal) ^ n ≤ ⊥.jacobson ^ n