mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.WittVector.IsPoly

Goal state before:
pp: case e'_3
p : ℕ
inst✝ : Fact (Nat.Prime p)
f g : ⦃R : Type u⦄ → [CommRing R] → 𝕎 R → 𝕎 R
φ : ℕ → MvPolynomial ℕ ℤ
hf : ∀ ⦃R : Type u⦄ [inst : CommRing R] (x : 𝕎 R), (f x).coeff = fun n ↦ (aeval x.coeff) (φ n)
ψ : ℕ → MvPolynomial ℕ ℤ
hg : ∀ ⦃R : Type u⦄ [inst : CommRing R] (x : 𝕎 R), (g x).coeff = fun n ↦ (aeval x.coeff) (ψ n)
R✝ : Type u
_Rcr✝ : CommRing R✝
x✝ : 𝕎 R✝
n k : ℕ
x : ℕ → ℤ
h :
  (eval₂Hom (algebraMap ℤ (ULift.{u, 0} ℤ)) (f (mk p fun i ↦ { down := x i })).coeff) (wittPolynomial p ℤ k) =
    (eval₂Hom (algebraMap ℤ (ULift.{u, 0} ℤ)) (g (mk p fun i ↦ { down := x i })).coeff) (wittPolynomial p ℤ k)
⊢ (eval₂Hom ((↑ULift.ringEquiv.symm).comp ((MvPolynomial.eval x).comp C)) fun i ↦
        ↑ULift.ringEquiv.symm ((MvPolynomial.eval x) (ψ i)))
      (wittPolynomial p ℤ k) =
    (eval₂Hom (algebraMap ℤ (ULift.{u, 0} ℤ)) (g (mk p fun i ↦ { down := x i })).coeff) (wittPolynomial p ℤ k)

Tactic:
simp only [hf, hg, MvPolynomial.eval, map_eval₂Hom]

Goal state after:
case e'_3
p : ℕ
inst✝ : Fact (Nat.Prime p)
f g : ⦃R : Type u⦄ → [CommRing R] → 𝕎 R → 𝕎 R
φ : ℕ → MvPolynomial ℕ ℤ
hf : ∀ ⦃R : Type u⦄ [inst : CommRing R] (x : 𝕎 R), (f x).coeff = fun n ↦ (aeval x.coeff) (φ n)
ψ : ℕ → MvPolynomial ℕ ℤ
hg : ∀ ⦃R : Type u⦄ [inst : CommRing R] (x : 𝕎 R), (g x).coeff = fun n ↦ (aeval x.coeff) (ψ n)
R✝ : Type u
_Rcr✝ : CommRing R✝
x✝ : 𝕎 R✝
n k : ℕ
x : ℕ → ℤ
h :
  (eval₂Hom (algebraMap ℤ (ULift.{u, 0} ℤ)) (f (mk p fun i ↦ { down := x i })).coeff) (wittPolynomial p ℤ k) =
    (eval₂Hom (algebraMap ℤ (ULift.{u, 0} ℤ)) (g (mk p fun i ↦ { down := x i })).coeff) (wittPolynomial p ℤ k)
⊢ (eval₂Hom ((↑ULift.ringEquiv.symm).comp ((eval₂Hom (RingHom.id ℤ) x).comp C)) fun i ↦
        (eval₂Hom ((↑ULift.ringEquiv.symm).comp (RingHom.id ℤ)) fun i ↦ ↑ULift.ringEquiv.symm (x i)) (ψ i))
      (wittPolynomial p ℤ k) =
    (eval₂Hom (algebraMap ℤ (ULift.{u, 0} ℤ)) fun n ↦ (aeval (mk p fun i ↦ { down := x i }).coeff) (ψ n))
      (wittPolynomial p ℤ k)
Module: Mathlib.RingTheory.Perfection

Goal state before:
pp: case refine_1.le_succ_of_le
R : Type u_1
inst✝¹ : CommSemiring R
p : ℕ
hp : Fact (Nat.Prime p)
inst✝ : CharP R p
h : Function.Surjective ⇑(frobenius R p)
n : ℕ
x : R
m k✝ : ℕ
hle : n ≤ k✝
xk : R
⊢ R

Tactic:
| le_succ_of_le hle xk =>

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

Goal state before:
pp: p : ℕ
R : Type u
inst✝¹ : CommRing R
inst✝ : Fact (Nat.Prime p)
n : ℕ
⊢ (aeval 0) (wittPolynomial p R n) = 0

Tactic:
aeval_zero,

Goal state after:
p : ℕ
R : Type u
inst✝¹ : CommRing R
inst✝ : Fact (Nat.Prime p)
n : ℕ
⊢ (algebraMap R (MvPolynomial ℕ R)) (MvPolynomial.constantCoeff (wittPolynomial p R n)) = 0
Module: Mathlib.RingTheory.WittVector.IsPoly

Goal state before:
pp: case e'_2
p : ℕ
inst✝ : Fact (Nat.Prime p)
f g : ⦃R : Type u⦄ → [CommRing R] → 𝕎 R → 𝕎 R → 𝕎 R
φ : ℕ → MvPolynomial (Fin 2 × ℕ) ℤ
hf : ∀ ⦃R : Type u⦄ [inst : CommRing R] (x y : 𝕎 R), (f x y).coeff = fun n ↦ peval (φ n) ![x.coeff, y.coeff]
ψ : ℕ → MvPolynomial (Fin 2 × ℕ) ℤ
hg : ∀ ⦃R : Type u⦄ [inst : CommRing R] (x y : 𝕎 R), (g x y).coeff = fun n ↦ peval (ψ n) ![x.coeff, y.coeff]
R✝ : Type u
_Rcr✝ : CommRing R✝
x✝ y✝ : 𝕎 R✝
n k : ℕ
x : Fin 2 × ℕ → ℤ
h :
  (eval₂Hom (algebraMap ℤ (ULift.{u, 0} ℤ))
        (f (mk p fun i ↦ { down := x (0, i) }) (mk p fun i ↦ { down := x (1, i) })).coeff)
      (wittPolynomial p ℤ k) =
    (eval₂Hom (algebraMap ℤ (ULift.{u, 0} ℤ))
        (g (mk p fun i ↦ { down := x (0, i) }) (mk p fun i ↦ { down := x (1, i) })).coeff)
      (wittPolynomial p ℤ k)
⊢ (eval₂Hom ((↑ULift.ringEquiv.symm).comp ((MvPolynomial.eval x).comp C)) fun i ↦
        ↑ULift.ringEquiv.symm ((MvPolynomial.eval x) (φ i)))
      (wittPolynomial p ℤ k) =
    (eval₂Hom (algebraMap ℤ (ULift.{u, 0} ℤ))
        (f (mk p fun i ↦ { down := x (0, i) }) (mk p fun i ↦ { down := x (1, i) })).coeff)
      (wittPolynomial p ℤ k)

Tactic:
simp only [hf, hg, MvPolynomial.eval, map_eval₂Hom]

Goal state after:
case e'_2
p : ℕ
inst✝ : Fact (Nat.Prime p)
f g : ⦃R : Type u⦄ → [CommRing R] → 𝕎 R → 𝕎 R → 𝕎 R
φ : ℕ → MvPolynomial (Fin 2 × ℕ) ℤ
hf : ∀ ⦃R : Type u⦄ [inst : CommRing R] (x y : 𝕎 R), (f x y).coeff = fun n ↦ peval (φ n) ![x.coeff, y.coeff]
ψ : ℕ → MvPolynomial (Fin 2 × ℕ) ℤ
hg : ∀ ⦃R : Type u⦄ [inst : CommRing R] (x y : 𝕎 R), (g x y).coeff = fun n ↦ peval (ψ n) ![x.coeff, y.coeff]
R✝ : Type u
_Rcr✝ : CommRing R✝
x✝ y✝ : 𝕎 R✝
n k : ℕ
x : Fin 2 × ℕ → ℤ
h :
  (eval₂Hom (algebraMap ℤ (ULift.{u, 0} ℤ))
        (f (mk p fun i ↦ { down := x (0, i) }) (mk p fun i ↦ { down := x (1, i) })).coeff)
      (wittPolynomial p ℤ k) =
    (eval₂Hom (algebraMap ℤ (ULift.{u, 0} ℤ))
        (g (mk p fun i ↦ { down := x (0, i) }) (mk p fun i ↦ { down := x (1, i) })).coeff)
      (wittPolynomial p ℤ k)
⊢ (eval₂Hom ((↑ULift.ringEquiv.symm).comp ((eval₂Hom (RingHom.id ℤ) x).comp C)) fun i ↦
        (eval₂Hom ((↑ULift.ringEquiv.symm).comp (RingHom.id ℤ)) fun i ↦ ↑ULift.ringEquiv.symm (x i)) (φ i))
      (wittPolynomial p ℤ k) =
    (eval₂Hom (algebraMap ℤ (ULift.{u, 0} ℤ)) fun n ↦
        peval (φ n) ![(mk p fun i ↦ { down := x (0, i) }).coeff, (mk p fun i ↦ { down := x (1, i) }).coeff])
      (wittPolynomial p ℤ k)
Module: Mathlib.RingTheory.WittVector.IsPoly

Goal state before:
pp: case e'_3
p : ℕ
inst✝ : Fact (Nat.Prime p)
f g : ⦃R : Type u⦄ → [CommRing R] → 𝕎 R → 𝕎 R → 𝕎 R
φ : ℕ → MvPolynomial (Fin 2 × ℕ) ℤ
hf : ∀ ⦃R : Type u⦄ [inst : CommRing R] (x y : 𝕎 R), (f x y).coeff = fun n ↦ peval (φ n) ![x.coeff, y.coeff]
ψ : ℕ → MvPolynomial (Fin 2 × ℕ) ℤ
hg : ∀ ⦃R : Type u⦄ [inst : CommRing R] (x y : 𝕎 R), (g x y).coeff = fun n ↦ peval (ψ n) ![x.coeff, y.coeff]
R✝ : Type u
_Rcr✝ : CommRing R✝
x✝ y✝ : 𝕎 R✝
n k : ℕ
x : Fin 2 × ℕ → ℤ
h :
  (eval₂Hom (algebraMap ℤ (ULift.{u, 0} ℤ))
        (f (mk p fun i ↦ { down := x (0, i) }) (mk p fun i ↦ { down := x (1, i) })).coeff)
      (wittPolynomial p ℤ k) =
    (eval₂Hom (algebraMap ℤ (ULift.{u, 0} ℤ))
        (g (mk p fun i ↦ { down := x (0, i) }) (mk p fun i ↦ { down := x (1, i) })).coeff)
      (wittPolynomial p ℤ k)
⊢ (eval₂Hom ((↑ULift.ringEquiv.symm).comp ((MvPolynomial.eval x).comp C)) fun i ↦
        ↑ULift.ringEquiv.symm ((MvPolynomial.eval x) (ψ i)))
      (wittPolynomial p ℤ k) =
    (eval₂Hom (algebraMap ℤ (ULift.{u, 0} ℤ))
        (g (mk p fun i ↦ { down := x (0, i) }) (mk p fun i ↦ { down := x (1, i) })).coeff)
      (wittPolynomial p ℤ k)

Tactic:
simp only [hf, hg, MvPolynomial.eval, map_eval₂Hom]

Goal state after:
case e'_3
p : ℕ
inst✝ : Fact (Nat.Prime p)
f g : ⦃R : Type u⦄ → [CommRing R] → 𝕎 R → 𝕎 R → 𝕎 R
φ : ℕ → MvPolynomial (Fin 2 × ℕ) ℤ
hf : ∀ ⦃R : Type u⦄ [inst : CommRing R] (x y : 𝕎 R), (f x y).coeff = fun n ↦ peval (φ n) ![x.coeff, y.coeff]
ψ : ℕ → MvPolynomial (Fin 2 × ℕ) ℤ
hg : ∀ ⦃R : Type u⦄ [inst : CommRing R] (x y : 𝕎 R), (g x y).coeff = fun n ↦ peval (ψ n) ![x.coeff, y.coeff]
R✝ : Type u
_Rcr✝ : CommRing R✝
x✝ y✝ : 𝕎 R✝
n k : ℕ
x : Fin 2 × ℕ → ℤ
h :
  (eval₂Hom (algebraMap ℤ (ULift.{u, 0} ℤ))
        (f (mk p fun i ↦ { down := x (0, i) }) (mk p fun i ↦ { down := x (1, i) })).coeff)
      (wittPolynomial p ℤ k) =
    (eval₂Hom (algebraMap ℤ (ULift.{u, 0} ℤ))
        (g (mk p fun i ↦ { down := x (0, i) }) (mk p fun i ↦ { down := x (1, i) })).coeff)
      (wittPolynomial p ℤ k)
⊢ (eval₂Hom ((↑ULift.ringEquiv.symm).comp ((eval₂Hom (RingHom.id ℤ) x).comp C)) fun i ↦
        (eval₂Hom ((↑ULift.ringEquiv.symm).comp (RingHom.id ℤ)) fun i ↦ ↑ULift.ringEquiv.symm (x i)) (ψ i))
      (wittPolynomial p ℤ k) =
    (eval₂Hom (algebraMap ℤ (ULift.{u, 0} ℤ)) fun n ↦
        peval (ψ n) ![(mk p fun i ↦ { down := x (0, i) }).coeff, (mk p fun i ↦ { down := x (1, i) }).coeff])
      (wittPolynomial p ℤ k)
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
m : M
⊢ _root_.id m = m

Tactic:
id_eq

Goal state after:
R : Type u
inst✝² : CommSemiring R
M : Type u_1
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
m : M
⊢ m = m
Module: Mathlib.RingTheory.Radical.NatInt

Goal state before:
pp: n : ℕ
pp : ∀ p ∈ n.primeFactors, 1 ≤ p
⊢ 1 < ∏ p ∈ n.primeFactors, p ↔ n.primeFactors.Nonempty

Tactic:
Finset.one_lt_prod_iff_of_one_le pp

Goal state after:
n : ℕ
pp : ∀ p ∈ n.primeFactors, 1 ≤ p
⊢ (∃ x ∈ n.primeFactors, 1 < x) ↔ n.primeFactors.Nonempty
Module: Mathlib.RingTheory.PolynomialLaw.Basic

Goal state before:
pp: case h
R : Type u
inst✝⁶ : CommSemiring R
M : Type u_1
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
S : Type v
inst✝³ : CommSemiring S
inst✝² : Algebra R S
T : Type u_3
inst✝¹ : CommSemiring T
inst✝ : Algebra R T
A : Subalgebra R T
φ : S →ₐ[R] T
hφ : A ≤ φ.range
t : T ⊗[R] M
u : ↥A ⊗[R] M
hu : (rTensor M A.val.toLinearMap) u = t
h_surj : Function.Surjective ⇑(rTensor M φ.rangeRestrict.toLinearMap)
p : S ⊗[R] M
hp : (rTensor M φ.rangeRestrict.toLinearMap) p = (rTensor M (Subalgebra.inclusion hφ).toLinearMap) u
⊢ (rTensor M φ.toLinearMap) p = (rTensor M φ.range.val.toLinearMap ∘ₗ rTensor M φ.rangeRestrict.toLinearMap) p

Tactic:
← rTensor_comp,

Goal state after:
case h
R : Type u
inst✝⁶ : CommSemiring R
M : Type u_1
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
S : Type v
inst✝³ : CommSemiring S
inst✝² : Algebra R S
T : Type u_3
inst✝¹ : CommSemiring T
inst✝ : Algebra R T
A : Subalgebra R T
φ : S →ₐ[R] T
hφ : A ≤ φ.range
t : T ⊗[R] M
u : ↥A ⊗[R] M
hu : (rTensor M A.val.toLinearMap) u = t
h_surj : Function.Surjective ⇑(rTensor M φ.rangeRestrict.toLinearMap)
p : S ⊗[R] M
hp : (rTensor M φ.rangeRestrict.toLinearMap) p = (rTensor M (Subalgebra.inclusion hφ).toLinearMap) u
⊢ (rTensor M φ.toLinearMap) p = (rTensor M (φ.range.val.toLinearMap ∘ₗ φ.rangeRestrict.toLinearMap)) p
Module: Mathlib.RingTheory.TensorProduct.DirectLimitFG

Goal state before:
pp: case h.right
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring S
inst✝⁴ : Algebra R S
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
f : M →ₗ[R] N
t : S ⊗[R] M
ht : (LinearMap.baseChange S f) t = 0
A : Subalgebra R S
hA : A.FG
ht_memA : t ∈ (rTensor M A.val.toLinearMap).range
u : ↥A ⊗[R] M
hu : (rTensor M A.val.toLinearMap) u = t
this :
  (rTensor N A.val.toLinearMap) ((LinearMap.baseChange (↥A) f) u) = 0 →
    ∃ B, B.FG ∧ ∃ (x : A ≤ B), (rTensor N (Subalgebra.inclusion ⋯).toLinearMap) ((LinearMap.baseChange (↥A) f) u) = 0
hu'✝ : (rTensor N A.val.toLinearMap) ((LinearMap.baseChange (↥A) f) u) = 0
B : Subalgebra R S
hB : B.FG
hAB : A ≤ B
hu' : (rTensor N (Subalgebra.inclusion ⋯).toLinearMap) ((LinearMap.baseChange (↥A) f) u) = 0
⊢ (rTensor M B.val.toLinearMap ∘ₗ rTensor M (Subalgebra.inclusion hAB).toLinearMap) u = t

Tactic:
← rTensor_comp,

Goal state after:
case h.right
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring S
inst✝⁴ : Algebra R S
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
f : M →ₗ[R] N
t : S ⊗[R] M
ht : (LinearMap.baseChange S f) t = 0
A : Subalgebra R S
hA : A.FG
ht_memA : t ∈ (rTensor M A.val.toLinearMap).range
u : ↥A ⊗[R] M
hu : (rTensor M A.val.toLinearMap) u = t
this :
  (rTensor N A.val.toLinearMap) ((LinearMap.baseChange (↥A) f) u) = 0 →
    ∃ B, B.FG ∧ ∃ (x : A ≤ B), (rTensor N (Subalgebra.inclusion ⋯).toLinearMap) ((LinearMap.baseChange (↥A) f) u) = 0
hu'✝ : (rTensor N A.val.toLinearMap) ((LinearMap.baseChange (↥A) f) u) = 0
B : Subalgebra R S
hB : B.FG
hAB : A ≤ B
hu' : (rTensor N (Subalgebra.inclusion ⋯).toLinearMap) ((LinearMap.baseChange (↥A) f) u) = 0
⊢ (rTensor M (B.val.toLinearMap ∘ₗ (Subalgebra.inclusion hAB).toLinearMap)) u = t
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
T : Type w
inst✝¹ : CommSemiring T
inst✝ : Algebra R T
h : S →ₐ[R] T
t : S ⊗[R] M
s : Finset S
p : MvPolynomial (Fin s.card) R ⊗[R] M
ha : π R M S ⟨s, p⟩ = t
s' : Finset T := Finset.image (⇑h) s
h' : ↥(φ R s).range →ₐ[R] ↥(φ R s').range := (h.comp (φ R s).range.val).codRestrict (φ R s').range ⋯
j : Fin s.card → Fin s'.card :=
  ⇑s'.equivFin ∘
    (fun x ↦
        match x with
        | ⟨x, hx⟩ => ⟨h x, ⋯⟩) ∘
      ⇑s.equivFin.symm
eq_h_comp : (φ R s').comp (rename j) = h.comp (φ R s)
p' : MvPolynomial (Fin s'.card) R ⊗[R] M := (rTensor M (rename j).toLinearMap) p
ha' : π R M T ⟨s', p'⟩ = (rTensor M h.toLinearMap) t
⊢ (rTensor N h.toLinearMap ∘ₗ rTensor N (φ R s).toLinearMap) (f.toFun' (MvPolynomial (Fin s.card) R) p) =
    (rTensor N (φ R s').toLinearMap) (f.toFun' (MvPolynomial (Fin s'.card) R) p')

Tactic:
← rTensor_comp,

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
T : Type w
inst✝¹ : CommSemiring T
inst✝ : Algebra R T
h : S →ₐ[R] T
t : S ⊗[R] M
s : Finset S
p : MvPolynomial (Fin s.card) R ⊗[R] M
ha : π R M S ⟨s, p⟩ = t
s' : Finset T := Finset.image (⇑h) s
h' : ↥(φ R s).range →ₐ[R] ↥(φ R s').range := (h.comp (φ R s).range.val).codRestrict (φ R s').range ⋯
j : Fin s.card → Fin s'.card :=
  ⇑s'.equivFin ∘
    (fun x ↦
        match x with
        | ⟨x, hx⟩ => ⟨h x, ⋯⟩) ∘
      ⇑s.equivFin.symm
eq_h_comp : (φ R s').comp (rename j) = h.comp (φ R s)
p' : MvPolynomial (Fin s'.card) R ⊗[R] M := (rTensor M (rename j).toLinearMap) p
ha' : π R M T ⟨s', p'⟩ = (rTensor M h.toLinearMap) t
⊢ (rTensor N (h.toLinearMap ∘ₗ (φ R s).toLinearMap)) (f.toFun' (MvPolynomial (Fin s.card) R) p) =
    (rTensor N (φ R s').toLinearMap) (f.toFun' (MvPolynomial (Fin s'.card) R) p')
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 ≠ ⊤
⊢ WithBot.unbotD 0 ↑(((map (Ideal.Quotient.mk I)) g).order.lift ⋯) = ((map (Ideal.Quotient.mk I)) g).order.toNat

Tactic:
ENat.lift_eq_toNat_of_lt_top

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 ≠ ⊤
⊢ WithBot.unbotD 0 ↑((map (Ideal.Quotient.mk I)) g).order.toNat = ((map (Ideal.Quotient.mk I)) g).order.toNat
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)}
⊢ p.1 < ((map (IsLocalRing.residue A)) g).order.lift ⋯

Tactic:
ENat.lift_eq_toNat_of_lt_top

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)}
⊢ p.1 < ((map (IsLocalRing.residue A)) g).order.toNat
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.1 = n
⊢ p ∈ {(n, 0)}

Tactic:
rwa [Finset.mem_singleton, Finset.HasAntidiagonal.antidiagonal_congr hp (by simp)]

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

Goal state before:
pp: R : Type u_2
M : Type u
inst✝² : Ring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
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.map N.subtype a)],
      IsIsotypicOfType R ↥N ↥(Submodule.map N.subtype a)

Tactic:
← (e _).isSimpleModule_iff,

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 ↥a], IsIsotypicOfType R ↥N ↥(Submodule.map N.subtype a)
Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation

Goal state before:
pp: case degree_lt.refine_1
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 : ℕ := ((map (IsLocalRing.residue A)) g).order.toNat
hn : n = ((map (IsLocalRing.residue A)) g).order.toNat
⊢ ↑((map (IsLocalRing.residue A)) g).order.toNat = ↑(((map (IsLocalRing.residue A)) g).order.lift ⋯)

Tactic:
ENat.lift_eq_toNat_of_lt_top

Goal state after:
Module: Mathlib.RingTheory.Valuation.ValuativeRel.Trivial

Goal state before:
pp: case inr
R Γ : Type
inst✝⁵ : Ring R
inst✝⁴ : DecidableEq R
inst✝³ : IsDomain R
inst✝² : LinearOrderedCommGroupWithZero Γ
inst✝¹ : ValuativeRel R
inst✝ : Valuation.Compatible 1
this : Subsingleton (ValueGroupWithZero R)ˣ
u : (ValueGroupWithZero R)ˣ
hx : ↑u ≠ 0
hx' : ↑u ≠ 1
⊢ False

Tactic:
simp_all [Subsingleton.elim u 1]

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : CharP R p
i : ℕ
hin : i < n
⊢ ∃ x, ¬coeff x ((WittVector.truncate n) (↑p ^ i)) = coeff x 0

Tactic:
use ⟨i, hin⟩

Goal state after:
case h
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : CharP R p
i : ℕ
hin : i < n
⊢ ¬coeff ⟨i, hin⟩ ((WittVector.truncate n) (↑p ^ i)) = coeff ⟨i, hin⟩ 0
Module: Mathlib.SetTheory.Cardinal.Cofinality.Club

Goal state before:
pp: α : Type v
inst✝ : LinearOrder α
⊢ IsStationary Set.univ ↔ Nonempty α

Tactic:
simp [IsStationary, ← not_imp_not (b := IsClub _), not_nonempty_iff_eq_empty,
    isClub_empty_iff]

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 (CNF b o))

Tactic:
CNF.of_lt ho hob

Goal state after:
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)])
Module: Mathlib.SetTheory.Ordinal.CantorNormalForm

Goal state before:
pp: b e : Ordinal.{u_1}
⊢ (coeff b 0) e = 0

Tactic:
by
  apply coeff_of_notMem_CNF
  simp

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

Goal state before:
pp: case h
α : Type u
inst✝ : CompleteLattice α
f : α →o α
⊢ lfp f = ↑⊥

Tactic:
exact rfl

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

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

Tactic:
exact rfl

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

Goal state before:
pp: x y : ZFSet.{u}
⊢ (insert x y).card ≤ y.card + 1

Tactic:
by
  rw [← lift_le.{u + 1}]
  simpa [← cardinalMk_coe_sort] using! mk_insert_le

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

Goal state before:
pp: x : ZFSet.{u}
hx : ↑x = IsOrdinal
this : x.IsOrdinal
⊢ ↑x ∈ ↑x

Tactic:
rwa [Class.coe_mem, hx]

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

Goal state before:
pp: case neg.inl
x y✝ y : ZFSet.{u}
hy : y.IsOrdinal
m : ZFSet.{u}
hmy : m ∈ y
IH :
  ∀ (a₂ b₂ : ZFSet.{u}),
    Sym2.GameAdd (fun x1 x2 ↦ x1 ∈ x2) s(a₂, b₂) s(m, y) → a₂.IsOrdinal → b₂.IsOrdinal → a₂ ⊆ b₂ → a₂ = b₂ ∨ a₂ ∈ b₂
hx : m.IsOrdinal
hxy : m ⊆ y
hyx : ¬y ⊆ m
hm : m ∈ ↑y \ ↑m
hm' : ∀ x ∈ ↑y \ ↑m, x ∉ m
hmx : m ⊆ m
⊢ m = y ∨ m ∈ y

Tactic:
exact Or.inr hmy

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

Goal state before:
pp: x : ZFSet.{u_1}
⊢ x ⊆ V_ x.rank

Tactic:
by
  simp [subset_vonNeumann]

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

Goal state before:
pp: a b : Ordinal.{u}
⊢ V_ a ⊆ V_ b ↔ a ≤ b

Tactic:
by
  simp [subset_vonNeumann]

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

Goal state before:
pp: o : Ordinal.{u_1}
⊢ o.toZFSet ⊆ V_ o

Tactic:
by
  simp [subset_vonNeumann]

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

Goal state before:
pp: case limit.refine_1
o : Ordinal.{u}
ho : IsSuccLimit o
ih : ∀ o' < o, (V_ o').card = preBeth o'
⊢ lift.{u + 1, u} ℵ₀ ≤ lift.{u + 1, u} o.card

Tactic:
lift_le,

Goal state after:
case limit.refine_1
o : Ordinal.{u}
ho : IsSuccLimit o
ih : ∀ o' < o, (V_ o').card = preBeth o'
⊢ ℵ₀ ≤ o.card
Module: Mathlib.SetTheory.Ordinal.Notation

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

pp: case oadd
o₁ o₂ : ONote
inst✝¹ : o₁.NF
inst✝ : o₂.NF
m : ℕ
b' : ONote
k : ℕ
e₂ : o₂.split' = (b', k)
this : b'.NF
a0 : ONote
n : ℕ+
a' : ONote
e₁ : o₁.split = (a0.oadd n a', m)
na : (a0.oadd n a').NF
⊢ (o₁ ^ o₂).NF

Tactic:
· rcases m with - | m
    · by_cases h : o₂ = 0
      · subst h
        simp only [(· ^ ·), Pow.pow, opow, opowAux2, e₁, OfNat.ofNat, Zero.zero, One.one]
        decide
      · have h' : o₂ ≠ zero := fun he => h (he ▸ zero_def ▸ rfl)
        simp only [(· ^ ·), Pow.pow, opow, opowAux2, e₁, OfNat.ofNat, Zero.zero, One.one,
          h', ite_false]
        exact NF.zero
    · by_cases h : m = 0
      · simp only [(· ^ ·), Pow.pow, opow, opowAux2, OfNat.ofNat, Zero.zero, One.one, *]
        decide
      · simp only [(· ^ ·), Pow.pow, opow, opowAux2, OfNat.ofNat, Zero.zero, *]
        change NF (oadd _ _ 0)
        infer_instance

Goal state after:
case oadd
o₁ o₂ : ONote
inst✝¹ : o₁.NF
inst✝ : o₂.NF
m : ℕ
b' : ONote
k : ℕ
e₂ : o₂.split' = (b', k)
this : b'.NF
a0 : ONote
n : ℕ+
a' : ONote
e₁ : o₁.split = (a0.oadd n a', m)
na : (a0.oadd n a').NF
⊢ (o₁ ^ o₂).NF
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion

Goal state before:
pp: α : Type u_1
s t : Stream'.Seq α
h : s.head ≠ t.head
⊢ dist s t = 1

Tactic:
by
  rw [Subtype.dist_eq, PiNat.dist_eq_of_ne]
  · convert! pow_zero _
    simp only [PiNat.firstDiff, ne_eq, Classical.dite_not, dite_eq_left_iff,
      Nat.find_eq_zero]
    intro h'
    simpa [Stream'.cons]
  · rw [Subtype.coe_ne_coe]
    contrapose h
    simp [h]

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

Goal state before:
pp: basis : Basis
f : ℝ → ℝ
h_basis : WellFormedBasis basis
hf_tendsto : Tendsto f atTop atTop
hf : ∀ g ∈ basis, (Real.log ∘ g) =o[atTop] (Real.log ∘ f)
⊢ WellFormedBasis (f :: basis)

Tactic:
change WellFormedBasis ([f] ++ basis)
  exact append (by simpa [WellFormedBasis]) h_basis (by simpa)

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

Goal state before:
pp: case cons.nil.cons
α : Type u_1
op : Stream'.Seq α → Stream'.Seq α
h : FriendlyOperation op
s_hd : α
s_tl : Stream'.Seq α
ht0 : op (Seq.cons s_hd nil) = nil
x✝ : α
s✝ : Stream'.Seq α
ht : op (Seq.cons s_hd s_tl) = Seq.cons x✝ s✝
this : nil.head = (Seq.cons x✝ s✝).head
⊢ (Seq.cons x✝ s✝).destruct =
    Option.map (fun x ↦ (x.1, ↑x.2 s_tl))
      (match nil.destruct with
      | none => none
      | some (t_hd, snd) => some (t_hd, ⟨fun s_tl ↦ (op (Seq.cons s_hd s_tl)).tail, ⋯⟩))

Tactic:
| cons =>

Goal state after: