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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
IH :
  ∀ m < n,
    X m ^ p + C ↑p * (MvPolynomial.map (Int.castRingHom ℚ)) (frobeniusPolyAux p m) =
      (bind₁ (wittPolynomial p ℚ ∘ fun n ↦ n + 1)) (xInTermsOfW p ℚ m)
h1 : ↑p ^ n * ⅟↑p ^ n = 1
⊢ C ↑p *
      (MvPolynomial.map (Int.castRingHom ℚ))
        (∑ i ∈ range n,
          ∑ j ∈ range (p ^ (n - i)),
            (X i ^ p) ^ (p ^ (n - i) - (j + 1)) * frobeniusPolyAux p i ^ (j + 1) *
              C ↑((p ^ (n - i)).choose (j + 1) / p ^ (n - i - v p (j + 1)) * p ^ (j - v p (j + 1)))) =
    -((∑ x ∈ range n, C (↑p ^ x) * X x ^ p ^ (n + 1 - x)) * C (⅟↑p ^ n) -
        (∑ x ∈ range n, C (↑p ^ x) * (bind₁ (wittPolynomial p ℚ ∘ fun n ↦ n + 1)) (xInTermsOfW p ℚ x) ^ p ^ (n - x)) *
          C (⅟↑p ^ n))

Tactic:
neg_sub,

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
IH :
  ∀ m < n,
    X m ^ p + C ↑p * (MvPolynomial.map (Int.castRingHom ℚ)) (frobeniusPolyAux p m) =
      (bind₁ (wittPolynomial p ℚ ∘ fun n ↦ n + 1)) (xInTermsOfW p ℚ m)
h1 : ↑p ^ n * ⅟↑p ^ n = 1
⊢ C ↑p *
      (MvPolynomial.map (Int.castRingHom ℚ))
        (∑ i ∈ range n,
          ∑ j ∈ range (p ^ (n - i)),
            (X i ^ p) ^ (p ^ (n - i) - (j + 1)) * frobeniusPolyAux p i ^ (j + 1) *
              C ↑((p ^ (n - i)).choose (j + 1) / p ^ (n - i - v p (j + 1)) * p ^ (j - v p (j + 1)))) =
    (∑ x ∈ range n, C (↑p ^ x) * (bind₁ (wittPolynomial p ℚ ∘ fun n ↦ n + 1)) (xInTermsOfW p ℚ x) ^ p ^ (n - x)) *
        C (⅟↑p ^ n) -
      (∑ x ∈ range n, C (↑p ^ x) * X x ^ p ^ (n + 1 - x)) * C (⅟↑p ^ n)
Module: Mathlib.RingTheory.WittVector.Verschiebung

Goal state before:
pp: p : ℕ
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
hp : Fact (Nat.Prime p)
f : R →+* S
x : 𝕎 R
⊢ (map f) (verschiebung x) = verschiebung ((map f) x)

Tactic:
ext ⟨-, -⟩
  · exact f.map_zero
  · rfl

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

Goal state before:
pp: case succ
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CharP R p
x : 𝕎 R
n : ℕ
ih : ∀ {m : ℕ}, (x * ↑p ^ n).coeff (m + n) = x.coeff m ^ p ^ n
m : ℕ
⊢ (x * ↑p ^ n * ↑p).coeff (m + (n + 1)) = x.coeff m ^ p ^ (n + 1)

Tactic:
← add_assoc,

Goal state after:
case succ
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CharP R p
x : 𝕎 R
n : ℕ
ih : ∀ {m : ℕ}, (x * ↑p ^ n).coeff (m + n) = x.coeff m ^ p ^ n
m : ℕ
⊢ (x * ↑p ^ n * ↑p).coeff (m + n + 1) = x.coeff m ^ p ^ (n + 1)
Module: Mathlib.RingTheory.Perfection

Goal state before:
pp: case succ
K : Type u₁
inst✝⁴ : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝³ : CommRing O
inst✝² : Algebra O K
hv : v.Integers O
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fact ¬IsUnit ↑p
f : PreTilt O p
h : ∃ n, (coeff n) f ≠ 0
k : ℕ
ih :
  (coeff (Nat.find h + k)) f ≠ 0 →
    ModP.preVal K v O p ((coeff (Nat.find h)) f) ^ p ^ Nat.find h =
      ModP.preVal K v O p ((coeff (Nat.find h + k)) f) ^ p ^ (Nat.find h + k)
hfn : (coeff (Nat.find h + (k + 1))) f ≠ 0
x : O
hx : (Ideal.Quotient.mk (Ideal.span {↑p})) x = (coeff (Nat.find h + k + 1)) f
h1 : (Ideal.Quotient.mk (Ideal.span {↑p})) x ≠ 0
h2 : (Ideal.Quotient.mk (Ideal.span {↑p})) (x ^ p) ≠ 0
⊢ ModP.preVal K v O p ((coeff (Nat.find h + k)) f) ^ p ^ (Nat.find h + k) =
    ModP.preVal K v O p ((coeff (Nat.find h + (k + 1))) f) ^ p ^ (Nat.find h + (k + 1))

Tactic:
← add_assoc,

Goal state after:
case succ
K : Type u₁
inst✝⁴ : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝³ : CommRing O
inst✝² : Algebra O K
hv : v.Integers O
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fact ¬IsUnit ↑p
f : PreTilt O p
h : ∃ n, (coeff n) f ≠ 0
k : ℕ
ih :
  (coeff (Nat.find h + k)) f ≠ 0 →
    ModP.preVal K v O p ((coeff (Nat.find h)) f) ^ p ^ Nat.find h =
      ModP.preVal K v O p ((coeff (Nat.find h + k)) f) ^ p ^ (Nat.find h + k)
hfn : (coeff (Nat.find h + (k + 1))) f ≠ 0
x : O
hx : (Ideal.Quotient.mk (Ideal.span {↑p})) x = (coeff (Nat.find h + k + 1)) f
h1 : (Ideal.Quotient.mk (Ideal.span {↑p})) x ≠ 0
h2 : (Ideal.Quotient.mk (Ideal.span {↑p})) (x ^ p) ≠ 0
⊢ ModP.preVal K v O p ((coeff (Nat.find h + k)) f) ^ p ^ (Nat.find h + k) =
    ModP.preVal K v O p ((coeff (Nat.find h + k + 1)) f) ^ p ^ (Nat.find h + k + 1)
Module: Mathlib.RingTheory.Perfection

Goal state before:
pp: case succ
K : Type u₁
inst✝⁴ : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝³ : CommRing O
inst✝² : Algebra O K
hv : v.Integers O
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fact ¬IsUnit ↑p
f : PreTilt O p
h : ∃ n, (coeff n) f ≠ 0
k : ℕ
ih :
  (coeff (Nat.find h + k)) f ≠ 0 →
    ModP.preVal K v O p ((coeff (Nat.find h)) f) ^ p ^ Nat.find h =
      ModP.preVal K v O p ((coeff (Nat.find h + k)) f) ^ p ^ (Nat.find h + k)
hfn : (coeff (Nat.find h + (k + 1))) f ≠ 0
x : O
hx : (Ideal.Quotient.mk (Ideal.span {↑p})) x = (coeff (Nat.find h + k + 1)) f
h1 : (Ideal.Quotient.mk (Ideal.span {↑p})) x ≠ 0
h2 : (Ideal.Quotient.mk (Ideal.span {↑p})) (x ^ p) ≠ 0
⊢ ModP.preVal K v O p ((Ideal.Quotient.mk (Ideal.span {↑p})) (x ^ p)) ^ p ^ (Nat.find h + k) =
    v ((algebraMap O K) x) ^ p ^ (Nat.find h + k + 1)

Tactic:
ModP.preVal_mk hv h2,

Goal state after:
case succ
K : Type u₁
inst✝⁴ : Field K
v : Valuation K ℝ≥0
O : Type u₂
inst✝³ : CommRing O
inst✝² : Algebra O K
hv : v.Integers O
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : Fact ¬IsUnit ↑p
f : PreTilt O p
h : ∃ n, (coeff n) f ≠ 0
k : ℕ
ih :
  (coeff (Nat.find h + k)) f ≠ 0 →
    ModP.preVal K v O p ((coeff (Nat.find h)) f) ^ p ^ Nat.find h =
      ModP.preVal K v O p ((coeff (Nat.find h + k)) f) ^ p ^ (Nat.find h + k)
hfn : (coeff (Nat.find h + (k + 1))) f ≠ 0
x : O
hx : (Ideal.Quotient.mk (Ideal.span {↑p})) x = (coeff (Nat.find h + k + 1)) f
h1 : (Ideal.Quotient.mk (Ideal.span {↑p})) x ≠ 0
h2 : (Ideal.Quotient.mk (Ideal.span {↑p})) (x ^ p) ≠ 0
⊢ v ((algebraMap O K) (x ^ p)) ^ p ^ (Nat.find h + k) = v ((algebraMap O K) x) ^ p ^ (Nat.find h + k + 1)
Module: Mathlib.RingTheory.WittVector.Truncated

Goal state before:
pp: p n : ℕ
R : Type u_1
inst✝ : CommRing R
x : TruncatedWittVector p n R
i : Fin n
⊢ (if h : ↑i < n then coeff ⟨↑i, h⟩ x else 0) = coeff i x

Tactic:
rw [dif_pos i.is_lt, Fin.eta]

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
R : Type u_3
x y : MvPolynomial R ℚ
n : ℕ
⊢ ghostMap (teichmullerFun p (x * y)) n = (ghostMap (teichmullerFun p x) * ghostMap (teichmullerFun p y)) n

Tactic:
simp only [Pi.mul_apply, ghostMap_apply, ghostComponent_teichmullerFun, mul_pow]

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Hermite.Gaussian

Goal state before:
pp: case succ
n : ℕ
x : ℝ
ih : (deriv^[n] fun y ↦ Real.exp (-(y ^ 2 / 2))) = fun x ↦ (-1) ^ n * ((aeval x) (hermite n) * Real.exp (-(x ^ 2 / 2)))
deriv_gaussian : deriv (fun y ↦ Real.exp (-(y ^ 2 / 2))) x = -x * Real.exp (-(x ^ 2 / 2))
⊢ (-1) ^ n *
      ((aeval x) (derivative (hermite n)) * Real.exp (-(x ^ 2 / 2)) +
        (aeval x) (hermite n) * (-x * Real.exp (-(x ^ 2 / 2)))) =
    (-1) ^ n * -1 * ((x * (aeval x) (hermite n) - (aeval x) (derivative (hermite n))) * Real.exp (-(x ^ 2 / 2)))

pp: case succ.hc
n : ℕ
x : ℝ
ih : (deriv^[n] fun y ↦ Real.exp (-(y ^ 2 / 2))) = fun x ↦ (-1) ^ n * ((aeval x) (hermite n) * Real.exp (-(x ^ 2 / 2)))
deriv_gaussian : deriv (fun y ↦ Real.exp (-(y ^ 2 / 2))) x = -x * Real.exp (-(x ^ 2 / 2))
⊢ DifferentiableAt ℝ (fun x ↦ (aeval x) (hermite n)) x

pp: case succ.hd
n : ℕ
x : ℝ
ih : (deriv^[n] fun y ↦ Real.exp (-(y ^ 2 / 2))) = fun x ↦ (-1) ^ n * ((aeval x) (hermite n) * Real.exp (-(x ^ 2 / 2)))
deriv_gaussian : deriv (fun y ↦ Real.exp (-(y ^ 2 / 2))) x = -x * Real.exp (-(x ^ 2 / 2))
⊢ DifferentiableAt ℝ (fun x ↦ Real.exp (-(x ^ 2 / 2))) x

Tactic:
· ring

Goal state after:
case succ.hc
n : ℕ
x : ℝ
ih : (deriv^[n] fun y ↦ Real.exp (-(y ^ 2 / 2))) = fun x ↦ (-1) ^ n * ((aeval x) (hermite n) * Real.exp (-(x ^ 2 / 2)))
deriv_gaussian : deriv (fun y ↦ Real.exp (-(y ^ 2 / 2))) x = -x * Real.exp (-(x ^ 2 / 2))
⊢ DifferentiableAt ℝ (fun x ↦ (aeval x) (hermite n)) x

case succ.hd
n : ℕ
x : ℝ
ih : (deriv^[n] fun y ↦ Real.exp (-(y ^ 2 / 2))) = fun x ↦ (-1) ^ n * ((aeval x) (hermite n) * Real.exp (-(x ^ 2 / 2)))
deriv_gaussian : deriv (fun y ↦ Real.exp (-(y ^ 2 / 2))) x = -x * Real.exp (-(x ^ 2 / 2))
⊢ DifferentiableAt ℝ (fun x ↦ Real.exp (-(x ^ 2 / 2))) x
Module: Mathlib.RingTheory.Polynomial.Hermite.Basic

Goal state before:
pp: n k : ℕ
hermite_explicit : ℕ → ℕ → ℤ := fun n k ↦ (-1) ^ n * ↑(2 * n - 1)‼ * ↑((2 * n + k).choose k)
hermite_explicit_recur :
  ∀ (n k : ℕ), hermite_explicit (n + 1) (k + 1) = hermite_explicit (n + 1) k - (↑k + 2) * hermite_explicit n (k + 2)
⊢ (hermite (2 * (n + 1) + (k + 1))).coeff (k + 1) = hermite_explicit (n + 1) (k + 1)

Tactic:
← add_assoc,

Goal state after:
n k : ℕ
hermite_explicit : ℕ → ℕ → ℤ := fun n k ↦ (-1) ^ n * ↑(2 * n - 1)‼ * ↑((2 * n + k).choose k)
hermite_explicit_recur :
  ∀ (n k : ℕ), hermite_explicit (n + 1) (k + 1) = hermite_explicit (n + 1) k - (↑k + 2) * hermite_explicit n (k + 2)
⊢ (hermite (2 * (n + 1) + k + 1)).coeff (k + 1) = hermite_explicit (n + 1) (k + 1)
Module: Mathlib.RingTheory.Polynomial.Dickson

Goal state before:
pp: case pos
p : ℕ
inst✝ : Fact (Nat.Prime p)
K : Type
w✝¹ : Field K
w✝ : CharP K p
H : Set.univ.Infinite
h : {x | ∃ y, x = y + y⁻¹ ∧ y ≠ 0}.Finite
x : K
hx : x = 0
⊢ ∃ i, (∃ y, i = y + y⁻¹ ∧ ¬y = 0) ∧ (i = x + x⁻¹ ∨ x = 0)

Tactic:
simp only [hx, and_true, inv_zero, or_true]
      exact ⟨_, 1, rfl, one_ne_zero⟩

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
n : ℕ
r : R
⊢ (opRingEquiv R) (op ((monomial n) r)) = (monomial n) (op r)

Tactic:
by
  ext; simp [opRingEquiv, ← ofFinsupp_single]

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

Goal state before:
pp: case succ
F : Type u_1
inst✝¹ : Field F
inst✝ : CharZero F
p : F[X]
d e : ℕ
he : (p * (1 - X) ^ e).hilbertPoly (d + e) = p.hilbertPoly d
⊢ (p * (1 - X) ^ e * (1 - X)).hilbertPoly (d + (e + 1)) = p.hilbertPoly d

Tactic:
← add_assoc,

Goal state after:
case succ
F : Type u_1
inst✝¹ : Field F
inst✝ : CharZero F
p : F[X]
d e : ℕ
he : (p * (1 - X) ^ e).hilbertPoly (d + e) = p.hilbertPoly d
⊢ (p * (1 - X) ^ e * (1 - X)).hilbertPoly (d + e + 1) = p.hilbertPoly d
Module: Mathlib.RingTheory.Polynomial.Selmer

Goal state before:
pp: n : ℕ
z : ℂ
h1 : z ^ n = z + 1
h2 : z ^ n + z ^ 2 = 0
h3 : z ^ 3 = 1
⊢ False

Tactic:
have key : z ^ n = 1 ∨ z ^ n = z ∨ z ^ n = z ^ 2 := by
    rw [← Nat.mod_add_div n 3, pow_add, pow_mul, h3, one_pow, mul_one]
    have : n % 3 < 3 := Nat.mod_lt n zero_lt_three
    interval_cases n % 3 <;>
    simp only [pow_zero, pow_one, or_true, true_or]

Goal state after:
n : ℕ
z : ℂ
h1 : z ^ n = z + 1
h2 : z ^ n + z ^ 2 = 0
h3 : z ^ 3 = 1
key : z ^ n = 1 ∨ z ^ n = z ∨ z ^ n = z ^ 2
⊢ False
Module: Mathlib.RingTheory.PowerSeries.Catalan

Goal state before:
pp: n : ℕ
⊢ (coeff n) (catalanSeries ^ 2 * X + 1) = (coeff n) catalanSeries

Tactic:
cases n with

Goal state after:
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
inst✝ : IsHausdorff I A
q : A⟦X⟧
r : A[X]
hdeg : r.degree < ↑((map (Ideal.Quotient.mk I)) g).order.toNat
heq : g * q = ↑r
this : ∀ (k i : ℕ), (coeff i) q ∈ I ^ k
⊢ q = 0 ∧ r = 0

Tactic:
by
    have hq : q = 0 := by
      ext i
      refine IsHausdorff.haus' (I := I) _ fun k ↦ ?_
      rw [SModEq.zero, smul_eq_mul, Ideal.mul_top]
      exact this _ _
    rw [hq, mul_zero, Eq.comm, Polynomial.coe_eq_zero_iff] at heq
    exact ⟨hq, heq⟩

Goal state after:
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
a✝ : A
f✝ f'✝ : A⟦X⟧
inst✝ : IsAdicComplete I A
f f' : A⟦X⟧
hf : f ≈ f'
a : A⟦X⟧
ha : a * g + (g * H.div f' + ↑(H.mod f')) = g * H.div f + ↑(H.mod f)
hf1 : (H.mod f).degree < ↑((map (Ideal.Quotient.mk I)) g).order.toNat
hf2 : f = g * H.div f + ↑(H.mod f)
hf'1 : (H.mod f').degree < ↑((map (Ideal.Quotient.mk I)) g).order.toNat
hf'2 : f' = g * H.div f' + ↑(H.mod f')
⊢ H.mod f = H.mod f'

Tactic:
← add_assoc,

Goal state after:
A : Type u_1
inst✝¹ : CommRing A
g : A⟦X⟧
I : Ideal A
H : g.IsWeierstrassDivisorAt I
a✝ : A
f✝ f'✝ : A⟦X⟧
inst✝ : IsAdicComplete I A
f f' : A⟦X⟧
hf : f ≈ f'
a : A⟦X⟧
ha : a * g + g * H.div f' + ↑(H.mod f') = g * H.div f + ↑(H.mod f)
hf1 : (H.mod f).degree < ↑((map (Ideal.Quotient.mk I)) g).order.toNat
hf2 : f = g * H.div f + ↑(H.mod f)
hf'1 : (H.mod f').degree < ↑((map (Ideal.Quotient.mk I)) g).order.toNat
hf'2 : f' = g * H.div f' + ↑(H.mod f')
⊢ H.mod f = H.mod f'
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
mem : x ∈ maximalIdeal R ∧ ∀ a ∈ rs', a ∈ maximalIdeal R
reg : IsSMulRegular (↑M) x ∧ IsWeaklyRegular (QuotSMulTop x ↑M) rs'
this : Nontrivial (QuotSMulTop x ↑M)
len : rs'.length = n
⊢ projectiveDimension (of R (QuotSMulTop x ↑M ⧸ Ideal.ofList rs' • ⊤)) = projectiveDimension M + (1 + ↑n)

Tactic:
← add_assoc,

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
mem : x ∈ maximalIdeal R ∧ ∀ a ∈ rs', a ∈ maximalIdeal R
reg : IsSMulRegular (↑M) x ∧ IsWeaklyRegular (QuotSMulTop x ↑M) rs'
this : Nontrivial (QuotSMulTop x ↑M)
len : rs'.length = n
⊢ projectiveDimension (of R (QuotSMulTop x ↑M ⧸ Ideal.ofList rs' • ⊤)) = projectiveDimension M + 1 + ↑n
Module: Mathlib.RingTheory.SimpleModule.WedderburnArtin

Goal state before:
pp: R : Type u
inst✝¹ : Ring R
inst✝ : IsSimpleRing R
⊢ [IsSemisimpleRing R, IsArtinianRing R, ∃ I, IsAtom I].TFAE

Tactic:
by
  tfae_have 1 → 2 := fun _ ↦ inferInstance
  tfae_have 2 → 3 := fun _ ↦ IsAtomic.exists_atom _
  tfae_have 3 → 1 := fun ⟨I, hI⟩ ↦ by
    have ⟨_, h⟩ := isSimpleRing_iff_isTwoSided_imp.mp ‹IsSimpleRing R›
    simp_rw [← isFullyInvariant_iff_isTwoSided] at h
    have := isSimpleModule_iff_isAtom.mpr hI
    obtain eq | eq := h _ (.isotypicComponent R R I)
    · exact (hI.bot_lt.not_ge <| (le_sSup <| by exact ⟨.refl ..⟩).trans_eq eq).elim
    exact .congr (.symm <| .trans (.ofEq _ _ eq) Submodule.topEquiv)
  tfae_finish

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)ˣ
⊢ ↑u < 1 → ↑u ≤ 0

Tactic:
· rw [← Units.val_one, Units.val_lt_val]
    simp

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)^[m] ((⇑frobenius)^[m] b)
⊢ ∃ m b, b.coeff 0 ≠ 0 ∧ a = ↑p ^ m * b

Tactic:
have := congr_fun (WittVector.verschiebung_frobenius_comm.comp_iterate m) b

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)^[m] ((⇑frobenius)^[m] b)
this : (⇑verschiebung ∘ ⇑frobenius)^[m] b = ((⇑verschiebung)^[m] ∘ (⇑frobenius)^[m]) b
⊢ ∃ m b, b.coeff 0 ≠ 0 ∧ a = ↑p ^ m * b
Module: Mathlib.RingTheory.WittVector.MulCoeff

Goal state before:
pp: p n : ℕ
mvpz : ↑p ^ (n + 1) = C (↑p ^ (n + 1))
| -(↑p ^ (n + 1) * X (0, n + 1)) * (↑p ^ (n + 1) * X (1, n + 1)) +
        ↑p ^ (n + 1) * X (0, n + 1) *
          (∑ x ∈ range (n + 1), (rename (Prod.mk 1)) ((monomial (Finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x)) +
            ↑p ^ (n + 1) * X (1, n + 1)) +
      ↑p ^ (n + 1) * X (1, n + 1) *
        ∑ x ∈ range (n + 1 + 1), (rename (Prod.mk 0)) ((monomial (Finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x)) +
    remainder p n

Tactic:
enter [1, 2, 2]
    rw [sum_range_succ, ← C_mul_X_pow_eq_monomial, tsub_self, pow_zero, pow_one, map_mul,
      rename_C, rename_X, ← mvpz]

Goal state after:
p n : ℕ
mvpz : ↑p ^ (n + 1) = C (↑p ^ (n + 1))
| ∑ x ∈ range (n + 1), (rename (Prod.mk 0)) ((monomial (Finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x)) +
    ↑p ^ (n + 1) * X (0, n + 1)
Module: Mathlib.SetTheory.Cardinal.Cofinality.Club

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

Tactic:
isClub_iff,

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

Goal state before:
pp: case refine_2
b o✝ : Ordinal.{u}
hb : 1 < b
x : Ordinal.{u} × Ordinal.{u}
o : Ordinal.{u}
ho : o ≠ 0
IH : x ∈ CNF b (o % b ^ log b o) → x.2 < b
⊢ x ∈ CNF b o → x.2 < b

Tactic:
· rw [CNF.ne_zero ho]
    intro h
    obtain rfl | h := mem_cons.mp h
    · exact div_opow_log_lt o hb
    · exact IH h

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

Goal state before:
pp: case a
α : Type u
inst✝ : CompleteLattice α
f : α →o α
h_fix : ∃ y, lfpApprox f ⊥ (succ #α).ord = ↑y
x : ↑(fixedPoints ⇑f)
h_x : lfpApprox f ⊥ (succ #α).ord = ↑x
⊢ lfp f ≤ lfpApprox f ⊥ (succ #α).ord

Tactic:
h_x

Goal state after:
case a
α : Type u
inst✝ : CompleteLattice α
f : α →o α
h_fix : ∃ y, lfpApprox f ⊥ (succ #α).ord = ↑y
x : ↑(fixedPoints ⇑f)
h_x : lfpApprox f ⊥ (succ #α).ord = ↑x
⊢ lfp f ≤ ↑x
Module: Mathlib.SetTheory.Ordinal.CantorNormalForm

Goal state before:
pp: case inl
b e x y : Ordinal.{u_1}
hb : 1 < b
hx : x ≠ 0
hxb : x < b
hy : y < b ^ e
⊢ (e, x) ∈ CNF b (b ^ e * x + y)

Tactic:
CNF.opow_mul_add hb hx hxb hy

Goal state after:
case inl
b e x y : Ordinal.{u_1}
hb : 1 < b
hx : x ≠ 0
hxb : x < b
hy : y < b ^ e
⊢ (e, x) ∈ (e, x) :: CNF b y
Module: Mathlib.SetTheory.Ordinal.CantorNormalForm

Goal state before:
pp: case pos
b e x y : Ordinal.{u_1}
hb : 1 < b
hx : x ≠ 0
hxb : x < b
hy : y < b ^ e
f c : Ordinal.{u_1}
hf : (f, c) ∈ CNF b y
he : e ≠ (f, c).1
⊢ (coeff b (b ^ e * x + y)) (f, c).1 = (coeff b y) (f, c).1

Tactic:
rw [coeff_of_mem_CNF hf]

Goal state after:
case pos
b e x y : Ordinal.{u_1}
hb : 1 < b
hx : x ≠ 0
hxb : x < b
hy : y < b ^ e
f c : Ordinal.{u_1}
hf : (f, c) ∈ CNF b y
he : e ≠ (f, c).1
⊢ (coeff b (b ^ e * x + y)) (f, c).1 = c
Module: Mathlib.SetTheory.Ordinal.CantorNormalForm

Goal state before:
pp: case pos
b e x y : Ordinal.{u_1}
hb : 1 < b
hx : x ≠ 0
hxb : x < b
hy : y < b ^ e
f c : Ordinal.{u_1}
hf : (f, c) ∈ CNF b y
he : e ≠ (f, c).1
⊢ ((f, c).1, c) ∈ CNF b (b ^ e * x + y)

Tactic:
CNF.opow_mul_add hb hx hxb hy

Goal state after:
case pos
b e x y : Ordinal.{u_1}
hb : 1 < b
hx : x ≠ 0
hxb : x < b
hy : y < b ^ e
f c : Ordinal.{u_1}
hf : (f, c) ∈ CNF b y
he : e ≠ (f, c).1
⊢ ((f, c).1, c) ∈ (e, x) :: CNF b y
Module: Mathlib.SetTheory.Ordinal.CantorNormalForm

Goal state before:
pp: case neg
b e x y : Ordinal.{u_1}
hb : 1 < b
hx : x ≠ 0
hxb : x < b
hy : y < b ^ e
e' : Ordinal.{u_1}
he : e ≠ e'
h : ¬∃ a ∈ CNF b y, a.1 = e'
⊢ ¬∃ a ∈ CNF b (b ^ e * x + y), a.1 = e'

Tactic:
CNF.opow_mul_add hb hx hxb hy

Goal state after:
case neg
b e x y : Ordinal.{u_1}
hb : 1 < b
hx : x ≠ 0
hxb : x < b
hy : y < b ^ e
e' : Ordinal.{u_1}
he : e ≠ e'
h : ¬∃ a ∈ CNF b y, a.1 = e'
⊢ ¬∃ a ∈ (e, x) :: CNF b y, a.1 = e'
Module: Mathlib.SetTheory.Ordinal.Topology

Goal state before:
pp: s : Set Ordinal.{u}
⊢ IsClosed s ↔
    ∀ {o : Ordinal.{u}},
      o ≠ 0 →
        ∀ (f : (a : Ordinal.{u}) → a < o → Ordinal.{u}), (∀ (i : Ordinal.{u}) (hi : i < o), f i hi ∈ s) → o.bsup f ∈ s

Tactic:
rw [isClosed_iff_iSup]

Goal state after:
s : Set Ordinal.{u}
⊢ (∀ {ι : Type u}, Nonempty ι → ∀ (f : ι → Ordinal.{u}), (∀ (i : ι), f i ∈ s) → ⨆ i, f i ∈ s) ↔
    ∀ {o : Ordinal.{u}},
      o ≠ 0 →
        ∀ (f : (a : Ordinal.{u}) → a < o → Ordinal.{u}), (∀ (i : Ordinal.{u}) (hi : i < o), f i hi ∈ s) → o.bsup f ∈ s
Module: Mathlib.SetTheory.Ordinal.Topology

Goal state before:
pp: case refine_1
s : Set Ordinal.{u}
H : ∀ {ι : Type u}, Nonempty ι → ∀ (f : ι → Ordinal.{u}), (∀ (i : ι), f i ∈ s) → ⨆ i, f i ∈ s
o : Ordinal.{u}
ho : o ≠ 0
f : (a : Ordinal.{u}) → a < o → Ordinal.{u}
hf : ∀ (i : Ordinal.{u}) (hi : i < o), f i hi ∈ s
⊢ ∀ (i : o.ToType), o.familyOfBFamily f i ∈ s

pp: case refine_2
s : Set Ordinal.{u}
H :
  ∀ {o : Ordinal.{u}},
    o ≠ 0 →
      ∀ (f : (a : Ordinal.{u}) → a < o → Ordinal.{u}), (∀ (i : Ordinal.{u}) (hi : i < o), f i hi ∈ s) → o.bsup f ∈ s
ι : Type u
hι : Nonempty ι
f : ι → Ordinal.{u}
hf : ∀ (i : ι), f i ∈ s
⊢ ⨆ i, f i ∈ s

Tactic:
· exact fun i => hf _ _

Goal state after:
case refine_2
s : Set Ordinal.{u}
H :
  ∀ {o : Ordinal.{u}},
    o ≠ 0 →
      ∀ (f : (a : Ordinal.{u}) → a < o → Ordinal.{u}), (∀ (i : Ordinal.{u}) (hi : i < o), f i hi ∈ s) → o.bsup f ∈ s
ι : Type u
hι : Nonempty ι
f : ι → Ordinal.{u}
hf : ∀ (i : ι), f i ∈ s
⊢ ⨆ i, f i ∈ s
Module: Mathlib.SetTheory.ZFC.Cardinal

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

Tactic:
← lift_inj.{u, u + 1}

Goal state after:
x y : ZFSet.{u}
h : x ∉ y
⊢ lift.{u + 1, u} (insert x y).card = lift.{u + 1, u} (y.card + 1)
Module: Mathlib.SetTheory.ZFC.Cardinal

Goal state before:
pp: x : ZFSet.{u}
⊢ x.powerset.card = 2 ^ x.card

Tactic:
← lift_inj.{u, u + 1}

Goal state after:
x : ZFSet.{u}
⊢ lift.{u + 1, u} x.powerset.card = lift.{u + 1, u} (2 ^ x.card)
Module: Mathlib.SetTheory.ZFC.Cardinal

Goal state before:
pp: α : Type u
inst✝ : Small.{v, u} α
f : α → ZFSet.{v}
⊢ lift.{max u (v + 1), max u v} (lift.{u, v} (⋃ (i : α), f i).card) ≤
    lift.{max u (v + 1), max u v} (sum fun i ↦ (f i).card)

Tactic:
lift_umax.{max u v, v + 1}

Goal state after:
α : Type u
inst✝ : Small.{v, u} α
f : α → ZFSet.{v}
⊢ lift.{v + 1, max u v} (lift.{u, v} (⋃ (i : α), f i).card) ≤ lift.{v + 1, max u v} (sum fun i ↦ (f i).card)
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: case oadd.lt
e : ONote
n : ℕ+
a o : ONote
h₁ : (e.oadd n a).NF
h₂ : o.NF
this✝¹ : a.NF
h' : (a.add o).repr = a.repr + o.repr
e' : ONote
n' : ℕ+
a' : ONote
h : a.add o = e'.oadd n' a'
nf : (e'.oadd n' a').NF
this✝ : e.NF
this : e'.NF
he : e.cmp e' = Ordering.lt
ee : e < e'
⊢ ω ^ e'.repr * ↑↑n' + a'.repr = ω ^ e.repr * ↑↑n + (ω ^ e'.repr * ↑↑n' + a'.repr)

Tactic:
← add_assoc,

Goal state after:
case oadd.lt
e : ONote
n : ℕ+
a o : ONote
h₁ : (e.oadd n a).NF
h₂ : o.NF
this✝¹ : a.NF
h' : (a.add o).repr = a.repr + o.repr
e' : ONote
n' : ℕ+
a' : ONote
h : a.add o = e'.oadd n' a'
nf : (e'.oadd n' a').NF
this✝ : e.NF
this : e'.NF
he : e.cmp e' = Ordering.lt
ee : e < e'
⊢ ω ^ e'.repr * ↑↑n' + a'.repr = ω ^ e.repr * ↑↑n + ω ^ e'.repr * ↑↑n' + a'.repr