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

Goal state before:
pp: R : Type u
inst✝⁶ : CommSemiring R
M : Type u_1
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
N : Type u_2
inst✝³ : AddCommMonoid N
inst✝² : Module R N
S : Type v
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
f : M →ₚₗ[R] N
s : Finset S
p : MvPolynomial (Fin s.card) R ⊗[R] M
s' : Finset S
p' : MvPolynomial (Fin s'.card) R ⊗[R] M
h✝ : π R M S ⟨s, p⟩ = π R M S ⟨s', p'⟩
u : ↥(φ R s).range ⊗[R] M := (rTensor M (φ R s).rangeRestrict.toLinearMap) p
hu : u = (rTensor M (φ R s).rangeRestrict.toLinearMap) p
uFG : (φ R s).range.FG
u' : ↥(φ R s').range ⊗[R] M := (rTensor M (φ R s').rangeRestrict.toLinearMap) p'
hu' : u' = (rTensor M (φ R s').rangeRestrict.toLinearMap) p'
u'FG : (φ R s').range.FG
huu' : (rTensor M (φ R s).range.val.toLinearMap) u = (rTensor M (φ R s').range.val.toLinearMap) u'
B : Subalgebra R S
hAB : (φ R s).range ≤ B
hA'B : (φ R s').range ≤ B
h : (rTensor M (Subalgebra.inclusion hAB).toLinearMap) u = (rTensor M (Subalgebra.inclusion hA'B).toLinearMap) u'
t : Finset S
hB : B = (φ R t).range
hAB' : (φ R s).range ≤ (φ R t).range
hA'B' : (φ R s').range ≤ (φ R t).range
q : MvPolynomial (Fin t.card) R ⊗[R] M
hq :
  (rTensor M (φ R t).rangeRestrict.toLinearMap) q =
    (rTensor M ((Subalgebra.inclusion ⋯).comp (Subalgebra.inclusion hAB)).toLinearMap) u
⊢ (rTensor M ((Subalgebra.inclusion hA'B').comp (φ R s').rangeRestrict).toLinearMap) p' =
    (rTensor M (φ R t).rangeRestrict.toLinearMap) q

Tactic:
simp only [hq, comp_toLinearMap, rTensor_comp, LinearMap.comp_apply]

Goal state after:
R : Type u
inst✝⁶ : CommSemiring R
M : Type u_1
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
N : Type u_2
inst✝³ : AddCommMonoid N
inst✝² : Module R N
S : Type v
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
f : M →ₚₗ[R] N
s : Finset S
p : MvPolynomial (Fin s.card) R ⊗[R] M
s' : Finset S
p' : MvPolynomial (Fin s'.card) R ⊗[R] M
h✝ : π R M S ⟨s, p⟩ = π R M S ⟨s', p'⟩
u : ↥(φ R s).range ⊗[R] M := (rTensor M (φ R s).rangeRestrict.toLinearMap) p
hu : u = (rTensor M (φ R s).rangeRestrict.toLinearMap) p
uFG : (φ R s).range.FG
u' : ↥(φ R s').range ⊗[R] M := (rTensor M (φ R s').rangeRestrict.toLinearMap) p'
hu' : u' = (rTensor M (φ R s').rangeRestrict.toLinearMap) p'
u'FG : (φ R s').range.FG
huu' : (rTensor M (φ R s).range.val.toLinearMap) u = (rTensor M (φ R s').range.val.toLinearMap) u'
B : Subalgebra R S
hAB : (φ R s).range ≤ B
hA'B : (φ R s').range ≤ B
h : (rTensor M (Subalgebra.inclusion hAB).toLinearMap) u = (rTensor M (Subalgebra.inclusion hA'B).toLinearMap) u'
t : Finset S
hB : B = (φ R t).range
hAB' : (φ R s).range ≤ (φ R t).range
hA'B' : (φ R s').range ≤ (φ R t).range
q : MvPolynomial (Fin t.card) R ⊗[R] M
hq :
  (rTensor M (φ R t).rangeRestrict.toLinearMap) q =
    (rTensor M ((Subalgebra.inclusion ⋯).comp (Subalgebra.inclusion hAB)).toLinearMap) u
⊢ (rTensor M (Subalgebra.inclusion hA'B').toLinearMap) ((rTensor M (φ R s').rangeRestrict.toLinearMap) p') =
    (rTensor M (Subalgebra.inclusion ⋯).toLinearMap) ((rTensor M (Subalgebra.inclusion hAB).toLinearMap) u)
Module: Mathlib.RingTheory.Regular.Free

Goal state before:
pp: R : Type u_1
inst✝³ : CommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : FinitePresentation R M
x : R
mem : x ∈ ⊥.jacobson
reg : IsSMulRegular M x
free : Free (R ⧸ Ideal.span {x}) (QuotSMulTop x M)
this : Module.Finite (R ⧸ Ideal.span {x}) (QuotSMulTop x M)
I : Type u_2 := Free.ChooseBasisIndex (R ⧸ Ideal.span {x}) (QuotSMulTop x M)
b : Basis (Free.ChooseBasisIndex (R ⧸ Ideal.span {x}) (QuotSMulTop x M)) (R ⧸ Ideal.span {x}) (QuotSMulTop x M) :=
  Free.chooseBasis (R ⧸ Ideal.span {x}) (QuotSMulTop x M)
b' : QuotSMulTop x M ≃ₗ[R] I →₀ R ⧸ Ideal.span {x} := LinearEquiv.restrictScalars R b.repr
f : (I →₀ R) →ₗ[R] QuotSMulTop x M := ↑b'.symm ∘ₗ Finsupp.mapRange.linearMap (Submodule.mkQ (Ideal.span {x}))
g : (I →₀ R) →ₗ[R] M
hg : (x • ⊤).mkQ ∘ₗ g = f
surjf : Function.Surjective ⇑f
lejac : Ideal.span {x} ≤ ⊥.jacobson
surjg : Function.Surjective ⇑g
⊢ (Finsupp.submodule fun x_1 ↦ Ideal.span {x}) = x • ⊤

Tactic:
← (Ideal.span {x}).mul_top,

Goal state after:
R : Type u_1
inst✝³ : CommRing R
M : Type u_2
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : FinitePresentation R M
x : R
mem : x ∈ ⊥.jacobson
reg : IsSMulRegular M x
free : Free (R ⧸ Ideal.span {x}) (QuotSMulTop x M)
this : Module.Finite (R ⧸ Ideal.span {x}) (QuotSMulTop x M)
I : Type u_2 := Free.ChooseBasisIndex (R ⧸ Ideal.span {x}) (QuotSMulTop x M)
b : Basis (Free.ChooseBasisIndex (R ⧸ Ideal.span {x}) (QuotSMulTop x M)) (R ⧸ Ideal.span {x}) (QuotSMulTop x M) :=
  Free.chooseBasis (R ⧸ Ideal.span {x}) (QuotSMulTop x M)
b' : QuotSMulTop x M ≃ₗ[R] I →₀ R ⧸ Ideal.span {x} := LinearEquiv.restrictScalars R b.repr
f : (I →₀ R) →ₗ[R] QuotSMulTop x M := ↑b'.symm ∘ₗ Finsupp.mapRange.linearMap (Submodule.mkQ (Ideal.span {x}))
g : (I →₀ R) →ₗ[R] M
hg : (x • ⊤).mkQ ∘ₗ g = f
surjf : Function.Surjective ⇑f
lejac : Ideal.span {x} ≤ ⊥.jacobson
surjg : Function.Surjective ⇑g
⊢ (Finsupp.submodule fun x_1 ↦ Ideal.span {x} * ⊤) = x • ⊤
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)
⊢ ↑(Submodule.spanFinrank (maximalIdeal (Localization.AtPrime p))) ≤ ringKrullDim (Localization.AtPrime p)

Tactic:
have qle : q ≤ p := by simpa [q, ← max] using map_comap_le

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
⊢ ↑(Submodule.spanFinrank (maximalIdeal (Localization.AtPrime p))) ≤ ringKrullDim (Localization.AtPrime p)
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
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}
⊢ p = span (⇑(algebraMap R R[X]) '' Submodule.generators (maximalIdeal R) ∪ {y})

Tactic:
simp only [Set.union_comm, Ideal.span_union, ← Ideal.map_span, algebraMap_eq, sup_comm]

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}
⊢ p = Ideal.map C (span (Submodule.generators (maximalIdeal R))) ⊔ span {y}
Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation

Goal state before:
pp: case neg
A : Type u_1
inst✝² : CommRing A
inst✝¹ : IsLocalRing A
f g : A⟦X⟧
inst✝ : IsPrecomplete (IsLocalRing.maximalIdeal A) A
hg : ¬(map (IsLocalRing.residue A)) g ≠ 0
⊢ Polynomial.degree 0 < ↑((map (IsLocalRing.residue A)) g).order.toNat

Tactic:
· nontriviality A
    rw [Polynomial.degree_zero]
    exact WithBot.bot_lt_coe _

Goal state after:
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
n : ℕ
hn :
  ∀ (M : ModuleCat R) [Nontrivial ↑M] [Module.Finite R ↑M] (rs : List R),
    IsWeaklyRegular (↑M) rs →
      (∀ r ∈ rs, r ∈ maximalIdeal R) →
        rs.length = n → projectiveDimension (of R (↑M ⧸ Ideal.ofList rs • ⊤)) = projectiveDimension M + ↑n
M : ModuleCat R
inst✝¹ : Nontrivial ↑M
inst✝ : Module.Finite R ↑M
rs : List R
x : R
rs' : List R
reg : IsWeaklyRegular (↑M) (x :: rs')
len : (x :: rs').length = n + 1
mem : x ∈ maximalIdeal R ∧ ∀ a ∈ rs', a ∈ maximalIdeal R
⊢ projectiveDimension (of R (↑M ⧸ Ideal.ofList (x :: rs') • ⊤)) = projectiveDimension M + ↑(n + 1)

Tactic:
simp only [isWeaklyRegular_cons_iff] at reg

Goal state after:
R : Type u
inst✝⁵ : CommRing R
inst✝⁴ : Small.{v, u} R
inst✝³ : IsLocalRing R
inst✝² : IsNoetherianRing R
n : ℕ
hn :
  ∀ (M : ModuleCat R) [Nontrivial ↑M] [Module.Finite R ↑M] (rs : List R),
    IsWeaklyRegular (↑M) rs →
      (∀ r ∈ rs, r ∈ maximalIdeal R) →
        rs.length = n → projectiveDimension (of R (↑M ⧸ Ideal.ofList rs • ⊤)) = projectiveDimension M + ↑n
M : ModuleCat R
inst✝¹ : Nontrivial ↑M
inst✝ : Module.Finite R ↑M
rs : List R
x : R
rs' : List R
len : (x :: rs').length = n + 1
mem : x ∈ maximalIdeal R ∧ ∀ a ∈ rs', a ∈ maximalIdeal R
reg : IsSMulRegular (↑M) x ∧ IsWeaklyRegular (QuotSMulTop x ↑M) rs'
⊢ projectiveDimension (of R (↑M ⧸ Ideal.ofList (x :: rs') • ⊤)) = projectiveDimension M + ↑(n + 1)
Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation

Goal state before:
pp: 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)

Tactic:
rw [Algebra.smul_def]

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 ((algebraMap A A⟦X⟧) a * h)
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
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
⊢ Submodule.spanFinrank
      (span
        (⇑(algebraMap R[X] (Localization.AtPrime p)) ''
          (⇑(algebraMap R R[X]) '' Submodule.generators (maximalIdeal R) ∪ {y}))) ≤
    Submodule.spanFinrank (maximalIdeal R) + 1

Tactic:
apply le_trans (Submodule.spanFinrank_span_le_ncard_of_finite (fin.image _))

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
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[X] (Localization.AtPrime p)) ''
        (⇑(algebraMap R R[X]) '' Submodule.generators (maximalIdeal R) ∪ {y})).ncard ≤
    Submodule.spanFinrank (maximalIdeal R) + 1
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
inst✝² : IsSemisimpleModule R M
inst✝¹ : Module.Finite R M
inst✝ : Nontrivial M
h : IsIsotypic R M
S : Submodule R M
hS : IsSimpleModule R ↥S
e : Nonempty (M ≃ₗ[R] Fin 0 → ↥S)
⊢ False

Tactic:
exact not_subsingleton _ (e.some.subsingleton)

Goal state after:
Module: Mathlib.RingTheory.TwoSidedIdeal.BigOperators

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
I : TwoSidedIdeal R
ι : Type u_2
s : Finset ι
f : ι → R
hs : ∃ x ∈ s, f x ∈ I
⊢ s.prod f ∈ I

Tactic:
by
  rcases s
  simpa using multiSetProd_mem (hs := hs)

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

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

Tactic:
rw [ha.squarefree.moebius_eq, card_factors_of_irreducible ha, pow_one]

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : CommRing k
inst✝¹ : CharP k p
inst✝ : PerfectRing k p
a : 𝕎 k
ha : a ≠ 0
m : ℕ
b : 𝕎 k
hc : b.coeff 0 ^ p ^ m ≠ 0
hcm : a = (⇑verschiebung ∘ ⇑frobenius)^[m] b
this : (⇑verschiebung ∘ ⇑frobenius)^[m] b = (⇑verschiebung)^[m] ((⇑frobenius)^[m] b)
x : 𝕎 k
⊢ ↑p * x = (⇑verschiebung ∘ ⇑frobenius) x

Tactic:
rw [mul_comm, ← WittVector.verschiebung_frobenius x]

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : CommRing k
inst✝¹ : CharP k p
inst✝ : PerfectRing k p
a : 𝕎 k
ha : a ≠ 0
m : ℕ
b : 𝕎 k
hc : b.coeff 0 ^ p ^ m ≠ 0
hcm : a = (⇑verschiebung ∘ ⇑frobenius)^[m] b
this : (⇑verschiebung ∘ ⇑frobenius)^[m] b = (⇑verschiebung)^[m] ((⇑frobenius)^[m] b)
x : 𝕎 k
⊢ verschiebung (frobenius x) = (⇑verschiebung ∘ ⇑frobenius) x
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
⊢ a₁.coeff 0 ^ p ^ (n + 1) ≠ 0

Tactic:
exact pow_ne_zero _ ha₁

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

Goal state before:
pp: 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
⊢ ∃ m, Nonempty (StandardOneDimIsocrystal p k m ≃ᶠⁱ[p, k] V)

Tactic:
obtain ⟨b, hb, m, hmb⟩ := WittVector.exists_frobenius_solution_fractionRing p ha

Goal state after:
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 : (IsFractionRing.ringEquivOfRingEquiv (frobeniusEquiv p k)) b * a = ↑p ^ m * b
⊢ ∃ m, Nonempty (StandardOneDimIsocrystal p k m ≃ᶠⁱ[p, k] V)
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:
rw [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.Ordinal.FixedPointApproximants

Goal state before:
pp: case neg
α : 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 : Ordinal.{u}
hi : i < b
hi' : a ≤ i
⊢ f (lfpApprox f x i) ≤ lfpApprox f x a

Tactic:
· simp [IH i hi hi', hf]

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

Goal state before:
pp: o x : Ordinal.{u}
h : x.invVeblen₁ < o
z : Ordinal.{u}
hz hz' : veblen o z = ω ^ x
⊢ False

Tactic:
← veblen_veblen_of_lt h,

Goal state after:
o x : Ordinal.{u}
h : x.invVeblen₁ < o
z : Ordinal.{u}
hz : veblen x.invVeblen₁ (veblen o z) = ω ^ x
hz' : veblen o z = ω ^ x
⊢ False
Module: Mathlib.SetTheory.ZFC.Class

Goal state before:
pp: case mp
x y : Class.{u}
⊢ y ∈ ⋃₀ x → ∃ z ∈ x, y ∈ z

Tactic:
rintro ⟨w, rfl, z, hzx, hwz⟩

Goal state after:
case mp
x : Class.{u}
w : ZFSet.{u}
z : Set ZFSet.{u}
hzx : z ∈ x.classToCong
hwz : w ∈ z
⊢ ∃ z ∈ x, ↑w ∈ z
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: e a : ONote
Ne : e.NF
Na : a.NF
e0 : e.repr ≠ 0
n : ℕ+
h : a.repr < ω ^ e.repr
No : (e.oadd n a).NF
this : ω ^ e.repr ≤ (e.oadd n a).repr
⊢ (ω ^ e.repr * ↑↑n + a.repr) ^ ω = (ω ^ e.repr) ^ ω

Tactic:
rw [repr] at this

Goal state after:
e a : ONote
Ne : e.NF
Na : a.NF
e0 : e.repr ≠ 0
n : ℕ+
h : a.repr < ω ^ e.repr
No : (e.oadd n a).NF
this : ω ^ e.repr ≤ ω ^ e.repr * ↑↑n + a.repr
⊢ (ω ^ e.repr * ↑↑n + a.repr) ^ ω = (ω ^ e.repr) ^ ω
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: e a : ONote
Ne : e.NF
Na : a.NF
e0 : e.repr ≠ 0
n : ℕ+
h : a.repr < ω ^ e.repr
No : (e.oadd n a).NF
this✝ : ω ^ e.repr ≤ ω ^ e.repr * ↑↑n + a.repr
b : Ordinal.{0}
l : b < ω
this : (e.oadd n a).repr < ω ^ succ e.repr
⊢ (ω ^ e.repr * ↑↑n + a.repr) ^ b ≤ (ω ^ e.repr) ^ ω

Tactic:
rw [repr] at this

Goal state after:
e a : ONote
Ne : e.NF
Na : a.NF
e0 : e.repr ≠ 0
n : ℕ+
h : a.repr < ω ^ e.repr
No : (e.oadd n a).NF
this✝ : ω ^ e.repr ≤ ω ^ e.repr * ↑↑n + a.repr
b : Ordinal.{0}
l : b < ω
this : ω ^ e.repr * ↑↑n + a.repr < ω ^ succ e.repr
⊢ (ω ^ e.repr * ↑↑n + a.repr) ^ b ≤ (ω ^ e.repr) ^ ω
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.Defs

Goal state before:
pp: case h_coef.step
basis_hd : ℝ → ℝ
basis_tl : Basis
s : Multiseries basis_hd basis_tl
motive : Multiseries basis_hd basis_tl → Prop
h_base : motive s
h_step :
  ∀ (exp : ℝ) (coef : MultiseriesExpansion basis_tl) (tl : Multiseries basis_hd basis_tl),
    motive (Multiseries.cons exp coef tl) → coef.Sorted ∧ tl.leadingExp < ↑exp ∧ motive tl
exp : ℝ
coef : MultiseriesExpansion basis_tl
⊢ ∀ (tl : Stream'.Seq (ℝ × MultiseriesExpansion basis_tl)),
    motive (Seq.cons (exp, coef) tl) → (exp, coef).2.Sorted ∧ motive tl

Tactic:
tl

Goal state after:
case h_coef.step
basis_hd : ℝ → ℝ
basis_tl : Basis
s : Multiseries basis_hd basis_tl
motive : Multiseries basis_hd basis_tl → Prop
h_base : motive s
h_step :
  ∀ (exp : ℝ) (coef : MultiseriesExpansion basis_tl) (tl : Multiseries basis_hd basis_tl),
    motive (Multiseries.cons exp coef tl) → coef.Sorted ∧ tl.leadingExp < ↑exp ∧ motive tl
exp : ℝ
coef : MultiseriesExpansion basis_tl
tl : Stream'.Seq (ℝ × MultiseriesExpansion basis_tl)
⊢ motive (Seq.cons (exp, coef) tl) → (exp, coef).2.Sorted ∧ motive tl
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs

Goal state before:
pp: case step
basis_hd : ℝ → ℝ
basis_tl : Basis
s : Multiseries basis_hd basis_tl
motive : Multiseries basis_hd basis_tl → Prop
h_base : motive s
h_step :
  ∀ (exp : ℝ) (coef : MultiseriesExpansion basis_tl) (tl : Multiseries basis_hd basis_tl),
    motive (Multiseries.cons exp coef tl) → coef.Sorted ∧ tl.leadingExp < ↑exp ∧ motive tl
exp : ℝ
coef : MultiseriesExpansion basis_tl
⊢ ∀ (tl : Stream'.Seq (ℝ × MultiseriesExpansion basis_tl)),
    motive (Seq.cons (exp, coef) tl) → (∀ x ∈ tl.head, (exp, coef) > x) ∧ motive tl

Tactic:
tl

Goal state after:
case step
basis_hd : ℝ → ℝ
basis_tl : Basis
s : Multiseries basis_hd basis_tl
motive : Multiseries basis_hd basis_tl → Prop
h_base : motive s
h_step :
  ∀ (exp : ℝ) (coef : MultiseriesExpansion basis_tl) (tl : Multiseries basis_hd basis_tl),
    motive (Multiseries.cons exp coef tl) → coef.Sorted ∧ tl.leadingExp < ↑exp ∧ motive tl
exp : ℝ
coef : MultiseriesExpansion basis_tl
tl : Stream'.Seq (ℝ × MultiseriesExpansion basis_tl)
⊢ motive (Seq.cons (exp, coef) tl) → (∀ x ∈ tl.head, (exp, coef) > x) ∧ motive tl
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs

Goal state before:
pp: case step.left
basis_hd : ℝ → ℝ
basis_tl : Basis
s : Multiseries basis_hd basis_tl
motive : Multiseries basis_hd basis_tl → Prop
h_base : motive s
h_step :
  ∀ (exp : ℝ) (coef : MultiseriesExpansion basis_tl) (tl : Multiseries basis_hd basis_tl),
    motive (Multiseries.cons exp coef tl) → coef.Sorted ∧ tl.leadingExp < ↑exp ∧ motive tl
exp : ℝ
coef : MultiseriesExpansion basis_tl
tl : Stream'.Seq (ℝ × MultiseriesExpansion basis_tl)
h : motive (Seq.cons (exp, coef) tl)
⊢ ∀ x ∈ tl.head, (exp, coef) > x

Tactic:
intro (tl_exp, tl_coef) h_tl
        rw [gt_iff_lt, lt_iff_lt]
        replace h_step := (h_step exp coef tl h).right.left
        cases tl <;> simp [leadingExp, head] at h_tl h_step
        grind

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

Goal state before:
pp: x✝ : ONote
o : ONote := x✝
a : ONote
h : o.FundamentalSequenceProp (Sum.inl (some a))
⊢ a < o

Tactic:
rw [lt_def, h.1]; apply lt_succ

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

Goal state before:
pp: a : ℕ
⊢ (a.pow 0).mod 0 = 1

Tactic:
simp [Nat.mod, Nat.modCore]

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

Goal state before:
pp: x : ℝ
num den num_k : ℕ
hx_isNNRat : IsNNRat x num den
hx_coprime : num.Coprime den
hn1 : num_k ^ 2 < num
hn2 : num < (num_k + 1) ^ 2
⊢ Irrational √x

Tactic:
Real.sqrt_eq_rpow

Goal state after:
x : ℝ
num den num_k : ℕ
hx_isNNRat : IsNNRat x num den
hx_coprime : num.Coprime den
hn1 : num_k ^ 2 < num
hn2 : num < (num_k + 1) ^ 2
⊢ Irrational (x ^ (1 / 2))
Module: Mathlib.Tactic.NormNum.Irrational

Goal state before:
pp: x : ℝ
num den den_k : ℕ
hx_isNNRat : IsNNRat x num den
hx_coprime : num.Coprime den
hd1 : den_k ^ 2 < den
hd2 : den < (den_k + 1) ^ 2
⊢ Irrational √x

Tactic:
Real.sqrt_eq_rpow

Goal state after:
x : ℝ
num den den_k : ℕ
hx_isNNRat : IsNNRat x num den
hx_coprime : num.Coprime den
hd1 : den_k ^ 2 < den
hd2 : den < (den_k + 1) ^ 2
⊢ Irrational (x ^ (1 / 2))
Module: Mathlib.Tactic.NormNum.RealSqrt

Goal state before:
pp: case out
n sn d sd : ℕ
hn : sn * sn = n
hd : sd * sd = d
inv✝ : Invertible ↑d
⊢ sqrt (↑n * ⅟↑d) = ↑sn * ⅟↑sd

Tactic:
simp [← hn, ← hd, NNReal.sqrt_mul]

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

Goal state before:
pp: case cons.succ.cons.cons.hnc
α : Type u
inst✝ : DecidableEq α
x y x' : α
xs : List α
xs_ih :
  ∀ {ys : List α},
    xs.Nodup → xs.length = ys.length → ∀ (i : ℕ), xs[i]? = some x → (applyId (xs.zip ys) x = y ↔ ys[i]? = some y)
n✝ : ℕ
h₂ : xs[n✝]? = some x
head✝ : α
tail✝ : List α
h₁✝ : (x' :: xs).length = (head✝ :: tail✝).length
h₁ : List.Pairwise (fun x1 x2 ↦ x1 ≠ x2) xs
h₀ : ∀ a' ∈ xs, x' ≠ a'
⊢ ¬x' = x

Tactic:
· apply h₀; apply List.mem_of_getElem? h₂

Goal state after:
Module: Mathlib.Topology.Algebra.InfiniteSum.DiscreteConvolution

Goal state before:
pp: M : Type u_1
S : Type u_2
E : Type u_3
E' : Type u_4
F : Type u_6
inst✝¹⁰ : Monoid M
inst✝⁹ : CommSemiring S
inst✝⁸ : AddCommMonoid E
inst✝⁷ : AddCommMonoid E'
inst✝⁶ : AddCommMonoid F
inst✝⁵ : Module S E
inst✝⁴ : Module S E'
inst✝³ : Module S F
inst✝² : TopologicalSpace F
inst✝¹ : T2Space F
inst✝ : ContinuousAdd F
f : M → E
g g' : M → E'
L : E →ₗ[S] E' →ₗ[S] F
hfg : ConvolutionExists L f g
hfg' : ConvolutionExists L f g'
x : M
⊢ (f ⋆[L] (g + g')) x = (f ⋆[L] g + f ⋆[L] g') x

Tactic:
exact (hfg x).distrib_add L (hfg' x)

Goal state after: