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

Goal state before:
pp: case neg
R : Type u_1
S : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
inst✝⁵ : IsDomain S
G : Type u_3
inst✝⁴ : Group G
inst✝³ : MulSemiringAction G S
inst✝² : SMulCommClass G R S
f : R[X]
inst✝¹ : DecidableEq ↑(f.rootSet S)
hf : (map (algebraMap R S) f).Splits
p : Ideal S
inst✝ : p.IsPrime
g : G
hg : g ∈ Ideal.inertia G p
hfp : ¬map (algebraMap R (S ⧸ p)) f = 0
π : S →ₐ[R] S ⧸ p := Ideal.Quotient.mkₐ R p
hp :
  ∀ a ∈ f.rootSet S,
    ∀ b ∈ f.rootSet S, ∀ c ∈ f.rootSet S, ∀ d ∈ f.rootSet S, π a = π b → π c = π d → a ≠ b → c ≠ d → {a, b} = {c, d}
hπ : ∀ (x : S), π (g • x) = π x
x : ↑(f.rootSet S)
hx : g • x ≠ x
z : ↑(f.rootSet S)
⊢ ↑(g • z) = ↑(if z = g • x then x else if z = x then g • x else z)

Tactic:
split_ifs with hz hz'

Goal state after:
case pos
R : Type u_1
S : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
inst✝⁵ : IsDomain S
G : Type u_3
inst✝⁴ : Group G
inst✝³ : MulSemiringAction G S
inst✝² : SMulCommClass G R S
f : R[X]
inst✝¹ : DecidableEq ↑(f.rootSet S)
hf : (map (algebraMap R S) f).Splits
p : Ideal S
inst✝ : p.IsPrime
g : G
hg : g ∈ Ideal.inertia G p
hfp : ¬map (algebraMap R (S ⧸ p)) f = 0
π : S →ₐ[R] S ⧸ p := Ideal.Quotient.mkₐ R p
hp :
  ∀ a ∈ f.rootSet S,
    ∀ b ∈ f.rootSet S, ∀ c ∈ f.rootSet S, ∀ d ∈ f.rootSet S, π a = π b → π c = π d → a ≠ b → c ≠ d → {a, b} = {c, d}
hπ : ∀ (x : S), π (g • x) = π x
x : ↑(f.rootSet S)
hx : g • x ≠ x
z : ↑(f.rootSet S)
hz : z = g • x
⊢ ↑(g • z) = ↑x

case pos
R : Type u_1
S : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
inst✝⁵ : IsDomain S
G : Type u_3
inst✝⁴ : Group G
inst✝³ : MulSemiringAction G S
inst✝² : SMulCommClass G R S
f : R[X]
inst✝¹ : DecidableEq ↑(f.rootSet S)
hf : (map (algebraMap R S) f).Splits
p : Ideal S
inst✝ : p.IsPrime
g : G
hg : g ∈ Ideal.inertia G p
hfp : ¬map (algebraMap R (S ⧸ p)) f = 0
π : S →ₐ[R] S ⧸ p := Ideal.Quotient.mkₐ R p
hp :
  ∀ a ∈ f.rootSet S,
    ∀ b ∈ f.rootSet S, ∀ c ∈ f.rootSet S, ∀ d ∈ f.rootSet S, π a = π b → π c = π d → a ≠ b → c ≠ d → {a, b} = {c, d}
hπ : ∀ (x : S), π (g • x) = π x
x : ↑(f.rootSet S)
hx : g • x ≠ x
z : ↑(f.rootSet S)
hz : ¬z = g • x
hz' : z = x
⊢ ↑(g • z) = ↑(g • x)

case neg
R : Type u_1
S : Type u_2
inst✝⁸ : CommRing R
inst✝⁷ : CommRing S
inst✝⁶ : Algebra R S
inst✝⁵ : IsDomain S
G : Type u_3
inst✝⁴ : Group G
inst✝³ : MulSemiringAction G S
inst✝² : SMulCommClass G R S
f : R[X]
inst✝¹ : DecidableEq ↑(f.rootSet S)
hf : (map (algebraMap R S) f).Splits
p : Ideal S
inst✝ : p.IsPrime
g : G
hg : g ∈ Ideal.inertia G p
hfp : ¬map (algebraMap R (S ⧸ p)) f = 0
π : S →ₐ[R] S ⧸ p := Ideal.Quotient.mkₐ R p
hp :
  ∀ a ∈ f.rootSet S,
    ∀ b ∈ f.rootSet S, ∀ c ∈ f.rootSet S, ∀ d ∈ f.rootSet S, π a = π b → π c = π d → a ≠ b → c ≠ d → {a, b} = {c, d}
hπ : ∀ (x : S), π (g • x) = π x
x : ↑(f.rootSet S)
hx : g • x ≠ x
z : ↑(f.rootSet S)
hz : ¬z = g • x
hz' : ¬z = x
⊢ ↑(g • z) = ↑z
Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation

Goal state before:
pp: case succ
A : Type u_1
inst✝ : CommRing A
g : A⟦X⟧
I : Ideal A
H : g.IsWeierstrassDivisorAt I
f : A⟦X⟧
k : ℕ
hq : ∀ {i : ℕ}, i ≥ ((map (Ideal.Quotient.mk I)) g).order.toNat → (coeff i) (f - g * H.seq f k) ∈ I ^ k
i : ℕ
hi : i ≥ ((map (Ideal.Quotient.mk I)) g).order.toNat
⊢ (coeff i) (f - g * H.seq f (k + 1)) ∈ I ^ (k + 1)

Tactic:
rw [seq]

Goal state after:
case succ
A : Type u_1
inst✝ : CommRing A
g : A⟦X⟧
I : Ideal A
H : g.IsWeierstrassDivisorAt I
f : A⟦X⟧
k : ℕ
hq : ∀ {i : ℕ}, i ≥ ((map (Ideal.Quotient.mk I)) g).order.toNat → (coeff i) (f - g * H.seq f k) ∈ I ^ k
i : ℕ
hi : i ≥ ((map (Ideal.Quotient.mk I)) g).order.toNat
⊢ (coeff i)
      (f -
        g *
          (H.seq f k +
            (mk fun i ↦ (coeff (i + ((map (Ideal.Quotient.mk I)) g).order.toNat)) (f - g * H.seq f k)) * ↑⋯.unit⁻¹)) ∈
    I ^ (k + 1)
Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation

Goal state before:
pp: A : Type u_1
inst✝ : CommRing A
g : A⟦X⟧
I : Ideal A
H : g.IsWeierstrassDivisorAt I
f : A⟦X⟧
k i : ℕ
⊢ (coeff i) (H.seq f (k + 1) - H.seq f k) ∈ I ^ k

Tactic:
rw [seq, add_sub_cancel_left]

Goal state after:
A : Type u_1
inst✝ : CommRing A
g : A⟦X⟧
I : Ideal A
H : g.IsWeierstrassDivisorAt I
f : A⟦X⟧
k i : ℕ
⊢ (coeff i) ((mk fun i ↦ (coeff (i + ((map (Ideal.Quotient.mk I)) g).order.toNat)) (f - g * H.seq f k)) * ↑⋯.unit⁻¹) ∈
    I ^ k
Module: Mathlib.RingTheory.RegularLocalRing.Polynomial

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

Tactic:
have fg := Submodule.FG.finite_generators fg'

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
⊢ ↑(Submodule.spanFinrank (maximalIdeal (Localization.AtPrime p))) ≤ ringKrullDim (Localization.AtPrime p)
Module: Mathlib.RingTheory.RingInvo

Goal state before:
pp: F : Type u_1
R : Type u_2
inst✝¹ : Semiring R
inst✝ : EquivLike F R Rᵐᵒᵖ
e f : RingInvo R
h₁ : e.toFun = f.toFun
h₂ : e.invFun = f.invFun
⊢ e = f

Tactic:
rcases e with ⟨⟨tE, _⟩, _⟩

Goal state after:
F : Type u_1
R : Type u_2
inst✝¹ : Semiring R
inst✝ : EquivLike F R Rᵐᵒᵖ
f : RingInvo R
tE : R ≃ Rᵐᵒᵖ
map_mul'✝ : ∀ (x y : R), tE.toFun (x * y) = tE.toFun x * tE.toFun y
map_add'✝ : ∀ (x y : R), tE.toFun (x + y) = tE.toFun x + tE.toFun y
involution'✝ :
  ∀ (x : R),
    MulOpposite.unop
        ({ toEquiv := tE, map_mul' := map_mul'✝, map_add' := map_add'✝ }.toFun
          (MulOpposite.unop ({ toEquiv := tE, map_mul' := map_mul'✝, map_add' := map_add'✝ }.toFun x))) =
      x
h₁ : { toEquiv := tE, map_mul' := map_mul'✝, map_add' := map_add'✝, involution' := involution'✝ }.toFun = f.toFun
h₂ : { toEquiv := tE, map_mul' := map_mul'✝, map_add' := map_add'✝, involution' := involution'✝ }.invFun = f.invFun
⊢ { toEquiv := tE, map_mul' := map_mul'✝, map_add' := map_add'✝, involution' := involution'✝ } = f
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
hI : I ≠ ⊤
this : Nontrivial (A ⧸ I)
⊢ (map (Ideal.Quotient.mk I)) g ≠ 0

Tactic:
congr(map (Ideal.Quotient.mk I) $(H.eq_mul)),

Goal state after:
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
hI : I ≠ ⊤
this : Nontrivial (A ⧸ I)
⊢ (map (Ideal.Quotient.mk I)) (↑f * h) ≠ 0
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)}
⊢ 0 * (coeff p.2) ((map (IsLocalRing.residue A)) q) = 0

Tactic:
rw [zero_mul]

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

Goal state before:
pp: R : Type u_2
M : Type u
S : Type u_4
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup S
inst✝¹ : Module R M
inst✝ : Module R S
N : Submodule R M
⊢ IsIsotypicOfType R (↥N) S ↔
    ∀ (a : Submodule R ↥N) [IsSimpleModule R ↥↑((Submodule.MapSubtype.orderIso N).toEquiv a)],
      Nonempty (↥↑((Submodule.MapSubtype.orderIso N).toEquiv a) ≃ₗ[R] S)

Tactic:
have e := Submodule.equivMapOfInjective _ N.subtype_injective

Goal state after:
R : Type u_2
M : Type u
S : Type u_4
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup S
inst✝¹ : Module R M
inst✝ : Module R S
N : Submodule R M
e : (p : Submodule R ↥N) → ↥p ≃ₗ[R] ↥(Submodule.map N.subtype p)
⊢ IsIsotypicOfType R (↥N) S ↔
    ∀ (a : Submodule R ↥N) [IsSimpleModule R ↥↑((Submodule.MapSubtype.orderIso N).toEquiv a)],
      Nonempty (↥↑((Submodule.MapSubtype.orderIso N).toEquiv a) ≃ₗ[R] S)
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
⊢ IsIsotypic R ↥N ↔
    ∀ (a : Submodule R ↥N) [IsSimpleModule R ↥↑((Submodule.MapSubtype.orderIso N).toEquiv a)],
      IsIsotypicOfType R ↥N ↥↑((Submodule.MapSubtype.orderIso N).toEquiv a)

Tactic:
have e := Submodule.equivMapOfInjective _ N.subtype_injective

Goal state after:
R : Type u_2
M : Type u
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
N : Submodule R M
e : (p : Submodule R ↥N) → ↥p ≃ₗ[R] ↥(Submodule.map N.subtype p)
⊢ IsIsotypic R ↥N ↔
    ∀ (a : Submodule R ↥N) [IsSimpleModule R ↥↑((Submodule.MapSubtype.orderIso N).toEquiv a)],
      IsIsotypicOfType R ↥N ↥↑((Submodule.MapSubtype.orderIso N).toEquiv a)
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✝ : IsSemisimpleModule R S
⊢ IsSemisimpleModule R ↥(isotypicComponent R M S)

Tactic:
by
  rw [isotypicComponent, sSup_eq_iSup]
  refine isSemisimpleModule_biSup_of_isSemisimpleModule_submodule fun m ⟨e⟩ ↦ ?_
  have := IsSemisimpleModule.congr e
  infer_instance

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
c : ↑(isotypicComponents R M)
⊢ IsSemisimpleModule R ↥↑c

Tactic:
obtain ⟨c, S, _, rfl⟩ := c; infer_instance

Goal state after:
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
a : A
g : A⟦X⟧
hg : (map (IsLocalRing.residue A)) (a • g) ≠ 0
H : g.IsWeierstrassFactorization (g.weierstrassDistinguished ⋯) (g.weierstrassUnit ⋯)
H' : (a • g).IsWeierstrassFactorization ((a • g).weierstrassDistinguished hg) ((a • g).weierstrassUnit hg)
⊢ (a • g).weierstrassDistinguished hg = g.weierstrassDistinguished ⋯

Tactic:
have ha : IsLocalRing.residue A a ≠ 0 := fun h ↦ hg (by simp [Algebra.smul_def, h])

Goal state after:
A : Type u_1
inst✝² : CommRing A
inst✝¹ : IsLocalRing A
inst✝ : IsAdicComplete (IsLocalRing.maximalIdeal A) A
a : A
g : A⟦X⟧
hg : (map (IsLocalRing.residue A)) (a • g) ≠ 0
H : g.IsWeierstrassFactorization (g.weierstrassDistinguished ⋯) (g.weierstrassUnit ⋯)
H' : (a • g).IsWeierstrassFactorization ((a • g).weierstrassDistinguished hg) ((a • g).weierstrassUnit hg)
ha : (IsLocalRing.residue A) a ≠ 0
⊢ (a • g).weierstrassDistinguished hg = g.weierstrassDistinguished ⋯
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
a : A
g : A⟦X⟧
hg : (map (IsLocalRing.residue A)) (a • g) ≠ 0
H : g.IsWeierstrassFactorization (g.weierstrassDistinguished ⋯) (g.weierstrassUnit ⋯)
H' : (a • g).IsWeierstrassFactorization ((a • g).weierstrassDistinguished hg) ((a • g).weierstrassUnit hg)
⊢ (a • g).weierstrassUnit hg = a • g.weierstrassUnit ⋯

Tactic:
have ha : IsLocalRing.residue A a ≠ 0 := fun h ↦ hg (by simp [Algebra.smul_def, h])

Goal state after:
A : Type u_1
inst✝² : CommRing A
inst✝¹ : IsLocalRing A
inst✝ : IsAdicComplete (IsLocalRing.maximalIdeal A) A
a : A
g : A⟦X⟧
hg : (map (IsLocalRing.residue A)) (a • g) ≠ 0
H : g.IsWeierstrassFactorization (g.weierstrassDistinguished ⋯) (g.weierstrassUnit ⋯)
H' : (a • g).IsWeierstrassFactorization ((a • g).weierstrassDistinguished hg) ((a • g).weierstrassUnit hg)
ha : (IsLocalRing.residue A) a ≠ 0
⊢ (a • g).weierstrassUnit hg = a • g.weierstrassUnit ⋯
Module: Mathlib.RingTheory.SimpleRing.DivisionRing

Goal state before:
pp: R : Type u_3
S : Type u_4
inst✝³ : Ring R
inst✝² : Ring S
e : ModuleCat R ⥤ ModuleCat S
inst✝¹ : e.IsEquivalence
M : ModuleCat R
inst✝ : IsSimpleModule R ↑M
⊢ IsSimpleModule S ↑(e.obj M)

Tactic:
rw [← simple_iff_isSimpleModule'] at *

Goal state after:
R : Type u_3
S : Type u_4
inst✝³ : Ring R
inst✝² : Ring S
e : ModuleCat R ⥤ ModuleCat S
inst✝¹ : e.IsEquivalence
M : ModuleCat R
inst✝ : Simple M
⊢ Simple (e.obj M)
Module: Mathlib.RingTheory.SimpleModule.Isotypic

Goal state before:
pp: R : Type u_5
inst✝ : Semiring R
I : Ideal R
⊢ Submodule.IsFullyInvariant I ↔ I.IsTwoSided

Tactic:
simpa only [Submodule.IsFullyInvariant, ← MulOpposite.opEquiv.trans (RingEquiv.moduleEndSelf R
    |>.toEquiv) |>.forall_congr_right, SetLike.le_def, I.isTwoSided_iff] using! forall_comm

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

Goal state before:
pp: case a.mk
R : Type u_1
Γ₀ : Type u_2
inst✝¹ : CommRing R
inst✝ : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
J : Ideal R
hJ : J ≤ v.supp
x✝ : R ⧸ J
x : R
hx : Quot.mk (⇑(Submodule.quotientRel J)) x ∈ (v.onQuot hJ).supp
⊢ Quot.mk (⇑(Submodule.quotientRel J)) x ∈ Ideal.map (Ideal.Quotient.mk J) v.supp

Tactic:
apply Ideal.subset_span

Goal state after:
case a.mk
R : Type u_1
Γ₀ : Type u_2
inst✝¹ : CommRing R
inst✝ : LinearOrderedCommMonoidWithZero Γ₀
v : Valuation R Γ₀
J : Ideal R
hJ : J ≤ v.supp
x✝ : R ⧸ J
x : R
hx : Quot.mk (⇑(Submodule.quotientRel J)) x ∈ (v.onQuot hJ).supp
⊢ Quot.mk (⇑(Submodule.quotientRel J)) x ∈ ⇑(Ideal.Quotient.mk J) '' ↑v.supp
Module: Mathlib.RingTheory.Smooth.Quotient

Goal state before:
pp: case mem_mul_mem
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
hy : y ∈ I
z : R
hz : z ∈ J
w : ↥J
hw : w ∈ Submodule.comap (Submodule.subtype J) (I * J)
eqz : J.toCotangent w = f (J.toCotangent ⟨z, hz⟩)
mem_bot : y * (Submodule.subtype J) w ∈ I * (I * J)
⊢ f (J.toCotangent ⟨y * z, ⋯⟩) = 0

Tactic:
simp only [← mul_assoc, sq, Submodule.bot_mul, Submodule.mem_bot] at mem_bot

Goal state after:
case mem_mul_mem
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
hy : y ∈ I
z : R
hz : z ∈ J
w : ↥J
hw : w ∈ Submodule.comap (Submodule.subtype J) (I * J)
eqz : J.toCotangent w = f (J.toCotangent ⟨z, hz⟩)
mem_bot : y * (Submodule.subtype J) w = 0
⊢ f (J.toCotangent ⟨y * z, ⋯⟩) = 0
Module: Mathlib.SetTheory.Cardinal.UnivLE

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

Tactic:
rw [univLE_iff_cardinal_le]

Goal state after:
⊢ univ.{u, v + 1} ≤ univ.{v, u + 1} ↔ Nonempty (Ordinal.{u} ↪ Ordinal.{v})
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:
cases hp <| List.prefix_iff_eq_take.mpr (h.eq_of_length (by simpa)).symm

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

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

Tactic:
cases hp <| List.prefix_iff_eq_take.mpr (h.eq_of_length (by simpa)).symm

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

Goal state before:
pp: case refine_2.inl
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 : b ≤ 1
⊢ List.Pairwise (fun x1 x2 ↦ x1 > x2) (map Prod.fst [(0, o)])

Tactic:
exact pairwise_singleton _ _

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

Goal state before:
pp: case refine_2.inr.inl
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
hob : o < b
⊢ List.Pairwise (fun x1 x2 ↦ x1 > x2) (map Prod.fst [(0, o)])

Tactic:
exact pairwise_singleton _ _

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

Goal state before:
pp: α : Type u
inst✝ : CompleteLattice α
⊢ Monotone gfpApprox

Tactic:
intro f g h

Goal state after:
α : Type u
inst✝ : CompleteLattice α
f g : α →o α
h : f ≤ g
⊢ gfpApprox f ≤ gfpApprox g
Module: Mathlib.SetTheory.Ordinal.Veblen

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

Tactic:
if_pos rfl

Goal state after:
f : Ordinal.{u_1} → Ordinal.{u_1}
⊢ f = f
Module: Mathlib.SetTheory.ZFC.Basic

Goal state before:
pp: ⊢ ⋂₀ ∅ = ∅

Tactic:
simp [sInter]

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

Goal state before:
pp: case a.inl
x y y✝ : PSet.{u_1}
h : y✝.Equiv x
⊢ y✝.rank < max (succ x.rank) y.rank

pp: case a.inr
x y y✝ : PSet.{u_1}
h : y✝ ∈ y
⊢ y✝.rank < max (succ x.rank) y.rank

Tactic:
· simp [rank_congr h]

Goal state after:
case a.inr
x y y✝ : PSet.{u_1}
h : y✝ ∈ y
⊢ y✝.rank < max (succ x.rank) y.rank
Module: Mathlib.SetTheory.Ordinal.Veblen

Goal state before:
pp: o : Ordinal.{u}
h : o.invVeblen₁ = o
ho : ¬o = 0
| veblen ⊥ o

Tactic:
bot_eq_zero,

Goal state after:
o : Ordinal.{u}
h : o.invVeblen₁ = o
ho : ¬o = 0
| veblen 0 o
Module: Mathlib.Tactic.AddGroup

Goal state before:
pp: G : Type u_1
inst✝ : AddGroup G
a b : G
n : ℤ
⊢ a + n • b + -b = a + (n + -1) • b

Tactic:
by
  rw [add_assoc, _zsmul_neg_trick]

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

Goal state before:
pp: case refine_1
x : ZFSet.{u_1}
h : x.IsOrdinal
y : ZFSet.{u_1}
hy : y ∈ insert x x
⊢ y ⊆ insert x x

Tactic:
obtain rfl | hy := mem_insert_iff.1 hy
    on_goal 2 => apply (h.subset_of_mem hy).trans
    all_goals simp_all [subset_def]

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

Goal state before:
pp: f g b : ℝ → ℝ
f_exp g_exp : ℝ
hf : Majorized f b f_exp
hg : Majorized g b g_exp
h_pos : ∀ᶠ (t : ℝ) in atTop, 0 < b t
⊢ Majorized (f * g) b (f_exp + g_exp)

Tactic:
by
  simp only [Majorized] at *
  intro exp h_exp
  let ε := (exp - f_exp - g_exp) / 2
  specialize hf (f_exp + ε) (by dsimp [ε]; linarith)
  specialize hg (g_exp + ε) (by dsimp [ε]; linarith)
  apply (hf.mul hg).trans_eventuallyEq (g₁ := fun t ↦ b t ^ (f_exp + ε) * b t ^ (g_exp + ε))
  apply h_pos.mono
  intro t hx
  simp only [Pi.pow_apply]
  conv_rhs => rw [show exp = (f_exp + ε) + (g_exp + ε) by dsimp [ε]; ring_nf, Real.rpow_add hx]

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

Goal state before:
pp: basis_hd : ℝ → ℝ
basis_tl : Basis
exp : ℝ
coef : MultiseriesExpansion basis_tl
tl : Multiseries basis_hd basis_tl
⊢ (cons exp coef tl).head = some (exp, coef)

Tactic:
by
  simp [head, cons]

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

Goal state before:
pp: α : Type u_1
γ : Type u_3
s t : Stream'.Seq α
op : γ → Stream'.Seq α → Stream'.Seq α
inst✝ : FriendlyOperationClass op
motive : Stream'.Seq α → Stream'.Seq α → Prop
base : motive s t
step :
  ∀ (u v : Stream'.Seq α),
    motive u v → u = v ∨ ∃ hd u' v' c, u = Seq.cons hd (op c u') ∧ v = Seq.cons hd (op c v') ∧ motive u' v'
this : ∀ (n : ℕ), dist s t ≤ 2⁻¹ ^ n
⊢ dist s t = 0

Tactic:
apply eq_of_le_of_ge
    · apply ge_of_tendsto' (x := Filter.atTop) _ this
      rw [tendsto_pow_atTop_nhds_zero_iff]
      norm_num
    · simp

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

Goal state before:
pp: x y : ℝ
x_num x_den y_num y_den k_num : ℕ
hx_coprime : x_num.Coprime x_den
hy_coprime : y_num.Coprime y_den
hn1 : k_num ^ y_den < x_num
hn2 : x_num < (k_num + 1) ^ y_den
hy_den_pos : 0 < y_den
hx_inv : Invertible ↑x_den
hx_eq : x = ↑x_num * ⅟↑x_den
hy_inv : Invertible ↑y_den
hy_eq : y = ↑y_num * ⅟↑y_den
⊢ Irrational (x ^ y)

Tactic:
hy_eq,

Goal state after:
x y : ℝ
x_num x_den y_num y_den k_num : ℕ
hx_coprime : x_num.Coprime x_den
hy_coprime : y_num.Coprime y_den
hn1 : k_num ^ y_den < x_num
hn2 : x_num < (k_num + 1) ^ y_den
hy_den_pos : 0 < y_den
hx_inv : Invertible ↑x_den
hx_eq : x = ↑x_num * ⅟↑x_den
hy_inv : Invertible ↑y_den
hy_eq : y = ↑y_num * ⅟↑y_den
⊢ Irrational (x ^ (↑y_num * ⅟↑y_den))
Module: Mathlib.Tactic.Simproc.FinsetInterval

Goal state before:
pp: n : ℕ
s : Finset ℕ
hs : Icc 0 n = s
⊢ Icc ⊥ n = s

Tactic:
bot_eq_zero,

Goal state after:
n : ℕ
s : Finset ℕ
hs : Icc 0 n = s
⊢ Icc 0 n = s
Module: Mathlib.Topology.UniformSpace.Ascoli

Goal state before:
pp: ι : Type u_1
X : Type u_2
α : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : UniformSpace α
F : ι → X → α
𝔖 : Set (Set X)
𝔖_compact : ∀ K ∈ 𝔖, IsCompact K
F_eqcont : ∀ K ∈ 𝔖, EquicontinuousOn F K
H1 :
  UniformSpace.comap F (UniformOnFun.uniformSpace X α 𝔖) =
    ⨅ K ∈ 𝔖, UniformSpace.comap (K.domRestrict ∘ F) (UniformFun.uniformSpace (↑K) α)
H2 :
  UniformSpace.comap ((⋃₀ 𝔖).domRestrict ∘ F) (Pi.uniformSpace fun i ↦ α) =
    ⨅ K ∈ 𝔖, UniformSpace.comap (K.domRestrict ∘ F) (Pi.uniformSpace fun i ↦ α)
K : Set X
hK : K ∈ 𝔖
⊢ UniformSpace.comap (K.domRestrict ∘ F) (UniformFun.uniformSpace (↑K) α) =
    UniformSpace.comap (K.domRestrict ∘ F) (Pi.uniformSpace fun i ↦ α)

Tactic:
have : CompactSpace K := isCompact_iff_compactSpace.mp (𝔖_compact K hK)
    exact (equicontinuous_restrict_iff _ |>.mpr <| F_eqcont K hK).comap_uniformFun_eq

Goal state after:
Module: Mathlib.Topology.UniformSpace.Ascoli

Goal state before:
pp: ι : Type u_1
X : Type u_2
α : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : UniformSpace α
F : ι → X → α
𝔖 : Set (Set X)
𝔖_compact : ∀ K ∈ 𝔖, IsCompact K
F_eqcont : ∀ K ∈ 𝔖, EquicontinuousOn F K
ℱ : Filter ι
f : X → α
K : Set X
hK : K ∈ 𝔖
this : CompactSpace ↑K
⊢ Tendsto ((⇑UniformFun.ofFun ∘ K.domRestrict ∘ ⇑(UniformOnFun.toFun 𝔖)) ∘ ⇑(UniformOnFun.ofFun 𝔖) ∘ F) ℱ
      (𝓝 ((⇑UniformFun.ofFun ∘ K.domRestrict ∘ ⇑(UniformOnFun.toFun 𝔖)) ((UniformOnFun.ofFun 𝔖) f))) ↔
    Tendsto (K.domRestrict ∘ F) ℱ (𝓝 (K.domRestrict f))

Tactic:
rw [← (equicontinuous_restrict_iff _ |>.mpr <| F_eqcont K hK).tendsto_uniformFun_iff_pi]

Goal state after:
ι : Type u_1
X : Type u_2
α : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : UniformSpace α
F : ι → X → α
𝔖 : Set (Set X)
𝔖_compact : ∀ K ∈ 𝔖, IsCompact K
F_eqcont : ∀ K ∈ 𝔖, EquicontinuousOn F K
ℱ : Filter ι
f : X → α
K : Set X
hK : K ∈ 𝔖
this : CompactSpace ↑K
⊢ Tendsto ((⇑UniformFun.ofFun ∘ K.domRestrict ∘ ⇑(UniformOnFun.toFun 𝔖)) ∘ ⇑(UniformOnFun.ofFun 𝔖) ∘ F) ℱ
      (𝓝 ((⇑UniformFun.ofFun ∘ K.domRestrict ∘ ⇑(UniformOnFun.toFun 𝔖)) ((UniformOnFun.ofFun 𝔖) f))) ↔
    Tendsto (⇑UniformFun.ofFun ∘ K.domRestrict ∘ F) ℱ (𝓝 (UniformFun.ofFun (K.domRestrict f)))