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

Goal state before:
pp: case pos
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
this :
  span (⇑(algebraMap R (Localization.AtPrime p)) '' Submodule.generators (maximalIdeal R)) =
    maximalIdeal (Localization.AtPrime p)
⊢ ↑(Submodule.spanFinrank (maximalIdeal (Localization.AtPrime p))) ≤ ↑p.height

Tactic:
apply le_trans _ (WithBot.coe_le_coe.mpr ht1)

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] := ⋯
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
this :
  span (⇑(algebraMap R (Localization.AtPrime p)) '' Submodule.generators (maximalIdeal R)) =
    maximalIdeal (Localization.AtPrime p)
⊢ ↑(Submodule.spanFinrank (maximalIdeal (Localization.AtPrime p))) ≤ ↑(maximalIdeal R).height
Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation

Goal state before:
pp: A : Type u_1
inst✝ : CommRing A
g : A⟦X⟧
f : A[X]
h : A⟦X⟧
I : Ideal A
H : g.IsWeierstrassFactorizationAt f h I
g' : A⟦X⟧
f' : A[X]
h' : A⟦X⟧
H' : g'.IsWeierstrassFactorizationAt f' h' I
⊢ g * g' = ↑(f * f') * (h * h')

Tactic:
by
    rw [H.eq_mul, H'.eq_mul, Polynomial.coe_mul]; ring

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

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

Tactic:
refine ⟨H.isDistinguishedAt, ?_, ?_⟩

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

case refine_2
A : Type u_1
inst✝ : CommRing A
g : A⟦X⟧
f : A[X]
h : A⟦X⟧
I : Ideal A
H : g.IsWeierstrassFactorizationAt f h I
a : A
ha : IsUnit a
⊢ a • g = ↑f * a • h
Module: Mathlib.RingTheory.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
⊢ projectiveDimension (of R (Shrink.{v, u} (R ⧸ Ideal.ofList rs))) = ↑rs.length

Tactic:
let e : (Shrink.{v} (R ⧸ Ideal.ofList rs)) ≃ₗ[R]
    (Shrink.{v} R) ⧸ Ideal.ofList rs • (⊤ : Submodule R (Shrink.{v} R)) :=
    ((Shrink.linearEquiv R _).trans (Submodule.Quotient.equiv _ _ (Shrink.linearEquiv R R).symm (by
      nth_rw 1 [← (Ideal.ofList rs).mul_top, ← smul_eq_mul, Submodule.map_smul'']
      simp )))

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 ⋯
⊢ projectiveDimension (of R (Shrink.{v, u} (R ⧸ Ideal.ofList rs))) = ↑rs.length
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] := ⋯
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
lt : q < p
this : (comap C p).IsMaximal
y : R[X]
left✝ : y.Monic
hy : p = Ideal.map C (comap C p) ⊔ span {y}
peq : p = span (⇑(algebraMap R R[X]) '' Submodule.generators (maximalIdeal R) ∪ {y})
fin : (⇑(algebraMap R R[X]) '' Submodule.generators (maximalIdeal R) ∪ {y}).Finite
⊢ (⇑(algebraMap R R[X]) '' Submodule.generators (maximalIdeal R)).ncard + {y}.ncard ≤
    Submodule.spanFinrank (maximalIdeal R) + 1

Tactic:
Set.ncard_singleton,

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
lt : q < p
this : (comap C p).IsMaximal
y : R[X]
left✝ : y.Monic
hy : p = Ideal.map C (comap C p) ⊔ span {y}
peq : p = span (⇑(algebraMap R R[X]) '' Submodule.generators (maximalIdeal R) ∪ {y})
fin : (⇑(algebraMap R R[X]) '' Submodule.generators (maximalIdeal R) ∪ {y}).Finite
⊢ (⇑(algebraMap R R[X]) '' Submodule.generators (maximalIdeal R)).ncard + 1 ≤ Submodule.spanFinrank (maximalIdeal R) + 1
Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation

Goal state before:
pp: A : Type u_1
inst✝² : CommRing A
inst✝¹ : IsLocalRing A
inst✝ : IsAdicComplete (IsLocalRing.maximalIdeal A) A
g g' : A⟦X⟧
hg : (map (IsLocalRing.residue A)) (g * g') ≠ 0
⊢ (g * g').weierstrassUnit hg = g.weierstrassUnit ⋯ * g'.weierstrassUnit ⋯

Tactic:
by
  have H := g.isWeierstrassFactorization_weierstrassDistinguished_weierstrassUnit
    (fun h ↦ hg (by simp [h]))
  have H' := g'.isWeierstrassFactorization_weierstrassDistinguished_weierstrassUnit
    (fun h ↦ hg (by simp [h]))
  have H'' := (g * g').isWeierstrassFactorization_weierstrassDistinguished_weierstrassUnit hg
  exact (H''.elim (H.mul H')).2

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsRegularRing R
p : Ideal R[X]
hp : p.IsPrime
q : Ideal R := comap C p
S : Type u_1 := (Localization.AtPrime q)[X]
pc : Submonoid R[X] := Submonoid.map (↑C) q.primeCompl
this✝³ : Algebra R[X] S := algebra R (Localization.AtPrime q)
this✝² : IsLocalization pc S
pS : Ideal S := Ideal.map (algebraMap R[X] S) p
disj : Disjoint ↑pc ↑p
this✝¹ : pS.IsPrime
this✝ : IsLocalization.AtPrime (Localization.AtPrime pS) p
this : IsRegularLocalRing (Localization.AtPrime q)
⊢ Ideal.map (algebraMap R (Localization.AtPrime q))
      (comap (algebraMap R (Localization.AtPrime q)[X]) (Ideal.map (algebraMap R[X] (Localization.AtPrime q)[X]) p)) =
    Ideal.map (algebraMap R (Localization.AtPrime q)) (under R (maximalIdeal (Localization.AtPrime q)))

Tactic:
IsScalarTower.algebraMap_eq R R[X] (Localization.AtPrime q)[X],

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsRegularRing R
p : Ideal R[X]
hp : p.IsPrime
q : Ideal R := comap C p
S : Type u_1 := (Localization.AtPrime q)[X]
pc : Submonoid R[X] := Submonoid.map (↑C) q.primeCompl
this✝³ : Algebra R[X] S := algebra R (Localization.AtPrime q)
this✝² : IsLocalization pc S
pS : Ideal S := Ideal.map (algebraMap R[X] S) p
disj : Disjoint ↑pc ↑p
this✝¹ : pS.IsPrime
this✝ : IsLocalization.AtPrime (Localization.AtPrime pS) p
this : IsRegularLocalRing (Localization.AtPrime q)
⊢ Ideal.map (algebraMap R (Localization.AtPrime q))
      (comap ((algebraMap R[X] (Localization.AtPrime q)[X]).comp (algebraMap R R[X]))
        (Ideal.map (algebraMap R[X] (Localization.AtPrime q)[X]) p)) =
    Ideal.map (algebraMap R (Localization.AtPrime q)) (under R (maximalIdeal (Localization.AtPrime q)))
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
ne : ¬c ⊓ sSup (isotypicComponents R M \ {c}) = ⊥
⊢ False

Tactic:
set s := isotypicComponents R M \ {c}
    have : IsSemisimpleModule R c := by obtain ⟨S, _, rfl⟩ := hc; infer_instance
    have := IsSemisimpleModule.of_injective _
      (Submodule.inclusion_injective (inf_le_left : c ⊓ sSup s ≤ c))
    have (c : s) : IsSemisimpleModule R c := by obtain ⟨_, ⟨_, _, rfl⟩, _⟩ := c; infer_instance
    have ⟨S, le, _⟩ := (IsSemisimpleModule.eq_bot_or_exists_simple_le _).resolve_left ne
    have ⟨c', hc', S', le', ⟨e⟩⟩ := S.le_linearEquiv_of_le_sSup _ (le.trans inf_le_right)
    have := IsSimpleModule.congr e.symm
    refine hc'.2 ?_
    rw [eq_isotypicComponent_of_le hc (le.trans inf_le_left), eq_isotypicComponent_of_le hc'.1 le']
    exact e.symm.isotypicComponent_eq

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
ι : Type u_5
inst✝ : DecidableEq ι
N : ι → Submodule R M
ind : iSupIndep N
iSup_top : ⨆ i, N i = ⊤
invar : ∀ (i : ι), (N i).IsFullyInvariant
f : (i : ι) → Module.End R ↥(N i)
i : ι
x : ↥(N i)
⊢ ↑(((fun f i ↦ LinearMap.restrict f ⋯)
          ((fun f ↦ ↑(ind.linearEquiv iSup_top) ∘ₗ DFinsupp.mapRange.linearMap f ∘ₗ ↑(ind.linearEquiv iSup_top).symm) f)
          i)
        x) =
    ↑((f i) x)

Tactic:
simp [ind.linearEquiv_symm_apply _ x.2]

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
ι : Type u_5
inst✝ : DecidableEq ι
N : ι → Submodule R M
ind : iSupIndep N
iSup_top : ⨆ i, N i = ⊤
invar : ∀ (i : ι), (N i).IsFullyInvariant
f : (i : ι) → Module.End R ↥(N i)
⊢ (fun f i ↦ LinearMap.restrict f ⋯)
      ((fun f ↦ ↑(ind.linearEquiv iSup_top) ∘ₗ DFinsupp.mapRange.linearMap f ∘ₗ ↑(ind.linearEquiv iSup_top).symm) f) =
    f

Tactic:
by ext i x; simp [ind.linearEquiv_symm_apply _ x.2]

Goal state after:
Module: Mathlib.RingTheory.Spectrum.Prime.Homeomorph

Goal state before:
pp: case e'_3
k : Type u_1
K : Type u_2
R : Type u_3
inst✝⁵ : Field k
inst✝⁴ : Field K
inst✝³ : Algebra k K
inst✝² : CommRing R
inst✝¹ : Algebra k R
inst✝ : IsPurelyInseparable k K
q : ℕ := ringExpChar k
⊢ Function.Injective ⇑(algebraMap R (R ⊗[k] K))

Tactic:
exact Algebra.TensorProduct.includeLeft_injective (S := R) (algebraMap k K).injective

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
x : K
⊢ v (-x) = v x

Tactic:
Valuation.map_neg

Goal state after:
K : Type u_1
inst✝³ : Field K
Γ₀ : Type u_2
inst✝² : LinearOrderedCommGroupWithZero Γ₀
v : Valuation K Γ₀
L : Type u_3
inst✝¹ : Field L
inst✝ : Algebra K L
x : K
⊢ v x = v x
Module: Mathlib.SetTheory.Ordinal.CantorNormalForm

Goal state before:
pp: case refine_2.inr.inr
b o✝ o : Ordinal.{u_1}
ho : o ≠ 0
IH : List.Pairwise (fun x1 x2 ↦ x1 > x2) (map Prod.fst (CNF b (o % b ^ log b o)))
hb : 1 < b
hbo : b ≤ o
⊢ List.Pairwise (fun x1 x2 ↦ x1 > x2) (map Prod.fst (CNF b o))

Tactic:
· rw [CNF.ne_zero ho, map_cons, pairwise_cons]
        refine ⟨fun a H ↦ ?_, IH⟩
        rw [mem_map] at H
        rcases H with ⟨⟨a, a'⟩, H, rfl⟩
        exact (fst_le_log H).trans_lt (log_mod_opow_log_lt_log_self hb hbo)

Goal state after:
Module: Mathlib.Topology.Order.IsNormal

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝⁷ : LinearOrder α
inst✝⁶ : WellFoundedLT α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : OrderTopology α
inst✝³ : LinearOrder β
inst✝² : WellFoundedLT β
inst✝¹ : TopologicalSpace β
inst✝ : OrderTopology β
f : α → β
⊢ StrictMono f ∧ Continuous f → IsNormal f

Tactic:
rintro ⟨hs, hc⟩
    refine ⟨hs, fun {a} ha ↦ (isLUB_of_mem_closure ?_ ?_).2⟩
    · rintro _ ⟨b, hb, rfl⟩
      exact (hs hb).le
    · apply image_closure_subset_closure_image hc (mem_image_of_mem ..)
      exact ha.isLUB_Iio.mem_closure (Iio_nonempty.2 ha.1)

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

Goal state before:
pp: b e x : Ordinal.{u_1}
f : Ordinal.{u_1} →₀ Ordinal.{u_1}
h : ∀ e' ∈ f.support, e' < e
hx : x ≠ 0
⊢ f e = 0

Tactic:
rw [← notMem_support_iff]

Goal state after:
b e x : Ordinal.{u_1}
f : Ordinal.{u_1} →₀ Ordinal.{u_1}
h : ∀ e' ∈ f.support, e' < e
hx : x ≠ 0
⊢ e ∉ f.support
Module: Mathlib.Topology.Order.SuccPred

Goal state before:
pp: case pos
α : Type u_1
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
inst✝¹ : SuccOrder α
inst✝ : NoMaxOrder α
s : Set α
o : α
ho : o ∈ s
ho' : IsSuccLimit o
⊢ s ∈ 𝓝 o ↔ IsSuccLimit o → ∃ a < o, Ioo a o ⊆ s

Tactic:
(hasBasis_nhds_Ioc_of_exists_lt (not_isMin_iff.1 ho'.not_isMin)).mem_iff

Goal state after:
case pos
α : Type u_1
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
inst✝¹ : SuccOrder α
inst✝ : NoMaxOrder α
s : Set α
o : α
ho : o ∈ s
ho' : IsSuccLimit o
⊢ (∃ i < o, Ioc i o ⊆ s) ↔ IsSuccLimit o → ∃ a < o, Ioo a o ⊆ s
Module: Mathlib.SetTheory.Ordinal.CantorNormalForm

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

Tactic:
notMem_support_iff.1 ha

Goal state after:
case neg
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 < b
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: o₁ e₁ : ONote
n₁ : ℕ+
a₁ : ONote
h✝¹ : o₁ = e₁.oadd n₁ a₁
o₂ e₂ : ONote
n₂ : ℕ+
a₂ : ONote
h✝ : o₂ = e₂.oadd n₂ a₂
h₁ : (namedPattern o₁ (e₁.oadd n₁ a₁) h✝¹).NF
h₂ : (namedPattern o₂ (e₂.oadd n₂ a₂) h✝).NF
IHe :
  match Ordering.eq, e₁, e₂ with
  | Ordering.lt, a, b => a < b
  | Ordering.eq, a, b => a = b
  | Ordering.gt, a, b => b < a
⊢ (Ordering.eq.then ((_root_.cmp ↑n₁ ↑n₂).then (a₁.cmp a₂))).Compares (namedPattern o₁ (e₁.oadd n₁ a₁) h✝¹)
    (namedPattern o₂ (e₂.oadd n₂ a₂) h✝)

Tactic:
dsimp at IHe

Goal state after:
o₁ e₁ : ONote
n₁ : ℕ+
a₁ : ONote
h✝¹ : o₁ = e₁.oadd n₁ a₁
o₂ e₂ : ONote
n₂ : ℕ+
a₂ : ONote
h✝ : o₂ = e₂.oadd n₂ a₂
h₁ : (namedPattern o₁ (e₁.oadd n₁ a₁) h✝¹).NF
h₂ : (namedPattern o₂ (e₂.oadd n₂ a₂) h✝).NF
IHe : e₁ = e₂
⊢ (Ordering.eq.then ((_root_.cmp ↑n₁ ↑n₂).then (a₁.cmp a₂))).Compares (namedPattern o₁ (e₁.oadd n₁ a₁) h✝¹)
    (namedPattern o₂ (e₂.oadd n₂ a₂) h✝)
Module: Mathlib.SetTheory.ZFC.Basic

Goal state before:
pp: x y : ZFSet.{u}
⊢ (∃ z ∈ {x}, y ∈ z) ↔ y ∈ x

Tactic:
mem_singleton,

Goal state after:
x y : ZFSet.{u}
⊢ (∃ z, z = x ∧ y ∈ z) ↔ y ∈ x
Module: Mathlib.SetTheory.ZFC.Basic

Goal state before:
pp: x y : ZFSet.{u}
⊢ (∀ z ∈ {x}, y ∈ z) ↔ y ∈ x

Tactic:
mem_singleton,

Goal state after:
x y : ZFSet.{u}
⊢ (∀ (z : ZFSet.{u}), z = x → y ∈ z) ↔ y ∈ x
Module: Mathlib.SetTheory.ZFC.Basic

Goal state before:
pp: x y : ZFSet.{u}
⊢ y ∈ ⋂₀ {x} ↔ y ∈ x

Tactic:
by simp_rw [mem_sInter (singleton_nonempty x), mem_singleton, forall_eq]

Goal state after:
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:
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.Class

Goal state before:
pp: x y : ZFSet.{u}
h : ↑x = ↑y
z : ZFSet.{u}
⊢ z ∈ x ↔ z ∈ y

Tactic:
change (x : Class.{u}) z ↔ (y : Class.{u}) z

Goal state after:
x y : ZFSet.{u}
h : ↑x = ↑y
z : ZFSet.{u}
⊢ ↑x z ↔ ↑y z
Module: Mathlib.SetTheory.ZFC.Class

Goal state before:
pp: A : Class.{u_1}
x : ZFSet.{u_1}
H : ∀ (y : ZFSet.{u_1}), A y ↔ y = x
y : ZFSet.{u_1}
x✝ : A.iota y
x' : ZFSet.{u_1}
h : {x | ∀ (y : ZFSet.{u_1}), A y ↔ y = x} x'
yx' : y ∈ ↑x'
⊢ ↑x y

Tactic:
by rwa [← (H x').1 <| (h x').2 rfl]

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

Goal state before:
pp: x : ZFSet.{u}
h : ∅ ∉ x
y : ZFSet.{u}
yx : y ∈ x
n : ¬∃ y_1, y_1 ∈ y
⊢ ∅ ∈ x

Tactic:
rwa [← (eq_empty y).2 fun z zx => n ⟨z, zx⟩]

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

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

Tactic:
rintro (rfl | h)
    · rfl
    · exact hy.subset_of_mem h

Goal state after:
Module: Mathlib.Tactic.AddGroup

Goal state before:
pp: G : Type u_1
inst✝ : AddGroup G
b : G
⊢ -b + -b = -2 • b

Tactic:
by
  have h : -b = (-1 : ℤ) • b := (neg_one_zsmul b).symm
  rw [h, ← add_zsmul]; norm_num

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

Goal state before:
pp: o' : ONote
m : ℕ
x✝ : NF 0
p : split' 0 = (o', m)
⊢ o'.NF ∧ repr 0 = ω * o'.repr + ↑m

Tactic:
by injection p; subst o' m; simp [NF.zero]

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

Goal state before:
pp: o₁ o₂ : ONote
inst✝¹ : o₁.NF
inst✝ : o₂.NF
a : ONote
m : ℕ
e₁ : o₁.split = (a, m)
na : a.NF
b' : ONote
k : ℕ
e₂ : o₂.split' = (b', k)
⊢ (o₁ ^ o₂).NF

Tactic:
have := (nf_repr_split' e₂).1

Goal state after:
o₁ o₂ : ONote
inst✝¹ : o₁.NF
inst✝ : o₂.NF
a : ONote
m : ℕ
e₁ : o₁.split = (a, m)
na : a.NF
b' : ONote
k : ℕ
e₂ : o₂.split' = (b', k)
this : b'.NF
⊢ (o₁ ^ o₂).NF
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: e a : ONote
Ne : e.NF
Na : a.NF
a' : Ordinal.{0}
e0 : e.repr ≠ 0
h : a' < ω ^ e.repr
aa : a.repr = a'
n : ℕ+
⊢ (ω ^ e.repr * ↑↑n + a') ^ ω = (ω ^ e.repr) ^ ω

Tactic:
subst aa

Goal state after:
e a : ONote
Ne : e.NF
Na : a.NF
e0 : e.repr ≠ 0
n : ℕ+
h : a.repr < ω ^ e.repr
⊢ (ω ^ e.repr * ↑↑n + a.repr) ^ ω = (ω ^ e.repr) ^ ω
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Majorized

Goal state before:
pp: f g b : ℝ → ℝ
f_exp g_exp : ℝ
hf : ∀ exp' > f_exp, f =o[atTop] (b ^ exp')
hg : ∀ exp' > g_exp, g =o[atTop] (b ^ exp')
h_pos : ∀ᶠ (t : ℝ) in atTop, 0 < b t
exp : ℝ
h_exp : exp > f_exp + g_exp
ε : ℝ := (exp - f_exp - g_exp) / 2
⊢ f_exp + ε > f_exp

Tactic:
by dsimp [ε]; linarith

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

Goal state before:
pp: f g b : ℝ → ℝ
f_exp g_exp : ℝ
hg : ∀ exp' > g_exp, g =o[atTop] (b ^ exp')
h_pos : ∀ᶠ (t : ℝ) in atTop, 0 < b t
exp : ℝ
h_exp : exp > f_exp + g_exp
ε : ℝ := (exp - f_exp - g_exp) / 2
hf : f =o[atTop] (b ^ (f_exp + ε))
⊢ g_exp + ε > g_exp

Tactic:
by dsimp [ε]; linarith

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

Goal state before:
pp: case oadd.zero
o₁ o₂ : ONote
inst✝¹ : o₁.NF
inst✝ : o₂.NF
m : ℕ
a0 : ONote
n : ℕ+
a' : ONote
e₁ : o₁.split = (a0.oadd n a', m)
N₁ : (a0.oadd n a').NF
r₁ : o₁.repr = (a0.oadd n a').repr + ↑m
this✝ : a0.NF
this : a'.NF
a00 : a0.repr ≠ 0
ad : ω ∣ a'.repr
al : a'.repr + ↑m < ω ^ a0.repr
aa : (a' + ↑m).repr = a'.repr + ↑m
b' : ONote
left✝ : b'.NF
e₂ : o₂.split' = (b', 0)
r₂ : o₂.repr = ω * b'.repr + ↑0
⊢ (match (scale 1 b', 0) with
      | (b, 0) => (a0 * b).oadd 1 0
      | (b, k.succ) =>
        (a0 * b + a0.mulNat k).scale (a0.oadd n a') + (a0 * b).opowAux a0 ((a0.oadd n a').mulNat m) k m).repr =
    (ω ^ a0.repr * ↑↑n + a'.repr + ↑m) ^ o₂.repr

pp: case oadd.succ
o₁ o₂ : ONote
inst✝¹ : o₁.NF
inst✝ : o₂.NF
m : ℕ
a0 : ONote
n : ℕ+
a' : ONote
e₁ : o₁.split = (a0.oadd n a', m)
N₁ : (a0.oadd n a').NF
r₁ : o₁.repr = (a0.oadd n a').repr + ↑m
this✝ : a0.NF
this : a'.NF
a00 : a0.repr ≠ 0
ad : ω ∣ a'.repr
al : a'.repr + ↑m < ω ^ a0.repr
aa : (a' + ↑m).repr = a'.repr + ↑m
b' : ONote
left✝ : b'.NF
k : ℕ
e₂ : o₂.split' = (b', k + 1)
r₂ : o₂.repr = ω * b'.repr + ↑(k + 1)
⊢ (match (scale 1 b', k + 1) with
      | (b, 0) => (a0 * b).oadd 1 0
      | (b, k.succ) =>
        (a0 * b + a0.mulNat k).scale (a0.oadd n a') + (a0 * b).opowAux a0 ((a0.oadd n a').mulNat m) k m).repr =
    (ω ^ a0.repr * ↑↑n + a'.repr + ↑m) ^ o₂.repr

Tactic:
· simp [r₂, opow_mul, repr_opow_aux₁ a00 al aa, add_assoc]

Goal state after:
case oadd.succ
o₁ o₂ : ONote
inst✝¹ : o₁.NF
inst✝ : o₂.NF
m : ℕ
a0 : ONote
n : ℕ+
a' : ONote
e₁ : o₁.split = (a0.oadd n a', m)
N₁ : (a0.oadd n a').NF
r₁ : o₁.repr = (a0.oadd n a').repr + ↑m
this✝ : a0.NF
this : a'.NF
a00 : a0.repr ≠ 0
ad : ω ∣ a'.repr
al : a'.repr + ↑m < ω ^ a0.repr
aa : (a' + ↑m).repr = a'.repr + ↑m
b' : ONote
left✝ : b'.NF
k : ℕ
e₂ : o₂.split' = (b', k + 1)
r₂ : o₂.repr = ω * b'.repr + ↑(k + 1)
⊢ (match (scale 1 b', k + 1) with
      | (b, 0) => (a0 * b).oadd 1 0
      | (b, k.succ) =>
        (a0 * b + a0.mulNat k).scale (a0.oadd n a') + (a0 * b).opowAux a0 ((a0.oadd n a').mulNat m) k m).repr =
    (ω ^ a0.repr * ↑↑n + a'.repr + ↑m) ^ o₂.repr
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs

Goal state before:
pp: basis_hd : ℝ → ℝ
basis_tl : Basis
basis_hd' : ℝ → ℝ
basis_tl' : Basis
f : ℝ → ℝ
g : MultiseriesExpansion basis_tl → MultiseriesExpansion basis_tl'
⊢ map f g nil = nil

Tactic:
simp [map, nil]

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

Goal state before:
pp: case hb0
a : ℚ
n d : ℕ
hn : ¬IsSquare n
hnd : n.Coprime d
ha : IsNNRat a n d
⊢ 0 < ↑d

Tactic:
contrapose! hnd
    have : n ≠ 1 := by rintro rfl; simp at hn
    simp_all

Goal state after:
Module: Mathlib.Topology.Algebra.Group.SubmonoidClosure

Goal state before:
pp: G : Type u_1
inst✝³ : Group G
inst✝² : TopologicalSpace G
inst✝¹ : CompactSpace G
inst✝ : IsTopologicalGroup G
x : G
⊢ closure[inst✝²] (range fun x_1 ↦ x ^ x_1) = closure[inst✝²] (range fun x_1 ↦ x ^ x_1)

Tactic:
by
  ext y
  exact (mapClusterPt_atTop_pow_tfae y x).out 3 2

Goal state after:
Module: Mathlib.Topology.Baire.BaireMeasurable

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
s : Set α
hs : IsLocallyClosed s
x : α
hx : x ∈ coborder s
⊢ x ∈ closure[inst✝] s ↔ x ∈ s

Tactic:
← closure_inter_coborder (s := s)

Goal state after:
α : Type u_1
inst✝ : TopologicalSpace α
s : Set α
hs : IsLocallyClosed s
x : α
hx : x ∈ coborder s
⊢ x ∈ closure[inst✝] s ↔ x ∈ closure[inst✝] s ∩ coborder s
Module: Mathlib.Topology.Baire.BaireMeasurable

Goal state before:
pp: case iUnion
α : Type u_1
inst✝² : TopologicalSpace α
s : Set α
inst✝¹ : MeasurableSpace α
inst✝ : BorelSpace α
f : ℕ → Set α
a✝ : Pairwise (Function.onFun Disjoint f)
hf✝ : ∀ (i : ℕ), MeasurableSet (f i)
ihf : ∀ (i : ℕ), ∃ u, IsOpen[inst✝²] u ∧ f i =ᶠ[residual α] u
⊢ ∃ u, IsOpen[inst✝²] u ∧ ⋃ i, f i =ᶠ[residual α] u

Tactic:
| iUnion f _ _ ihf =>

Goal state after:
Module: Mathlib.Topology.Baire.BaireMeasurable

Goal state before:
pp: α : Type u_1
inst✝ : TopologicalSpace α
s : Set α
h : BaireMeasurableSet s
this✝¹ : MeasurableSpace α := borel α
this✝ : BorelSpace α
⊢ ∃ u, IsOpen[inst✝] u ∧ s =ᶠ[residual α] u

Tactic:
rcases h with ⟨t, ht, hst⟩

Goal state after:
α : Type u_1
inst✝ : TopologicalSpace α
s : Set α
this✝¹ : MeasurableSpace α := borel α
this✝ : BorelSpace α
t : Set α
ht : MeasurableSet t
hst : s =ᶠ[residual α] t
⊢ ∃ u, IsOpen[inst✝] u ∧ s =ᶠ[residual α] u