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

Goal state before:
pp: case ind.ha
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
ih : ∀ m < n, m ∈ (xInTermsOfW p ℚ m).vars ∧ (xInTermsOfW p ℚ m).vars ⊆ range (m + 1)
i j : ℕ
hj : j ∈ range n
H : i ∈ (C (↑p ^ j) * xInTermsOfW p ℚ j ^ p ^ (n - j)).vars
⊢ ↑p ^ j ≠ 0

pp: case ind
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
ih : ∀ m < n, m ∈ (xInTermsOfW p ℚ m).vars ∧ (xInTermsOfW p ℚ m).vars ⊆ range (m + 1)
i j : ℕ
hj : j ∈ range n
H : i ∈ (xInTermsOfW p ℚ j ^ p ^ (n - j)).vars
⊢ i ∈ range n

Tactic:
· apply pow_ne_zero
      exact mod_cast hp.1.ne_zero

Goal state after:
case ind
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
ih : ∀ m < n, m ∈ (xInTermsOfW p ℚ m).vars ∧ (xInTermsOfW p ℚ m).vars ⊆ range (m + 1)
i j : ℕ
hj : j ∈ range n
H : i ∈ (xInTermsOfW p ℚ j ^ p ^ (n - j)).vars
⊢ i ∈ range n
Module: Mathlib.RingTheory.WittVector.WittPolynomial

Goal state before:
pp: case ind.hpq.ha
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
ih : ∀ m < n, m ∈ (xInTermsOfW p ℚ m).vars ∧ (xInTermsOfW p ℚ m).vars ⊆ range (m + 1)
j : ℕ
hj : j ∈ range n
H : n ∈ (C (↑p ^ j) * xInTermsOfW p ℚ j ^ p ^ (n - j)).vars
⊢ ↑p ^ j ≠ 0

pp: case ind.hpq
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
ih : ∀ m < n, m ∈ (xInTermsOfW p ℚ m).vars ∧ (xInTermsOfW p ℚ m).vars ⊆ range (m + 1)
j : ℕ
hj : j ∈ range n
H : n ∈ (xInTermsOfW p ℚ j ^ p ^ (n - j)).vars
⊢ False

Tactic:
· apply pow_ne_zero
      exact mod_cast hp.1.ne_zero

Goal state after:
case ind.hpq
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
ih : ∀ m < n, m ∈ (xInTermsOfW p ℚ m).vars ∧ (xInTermsOfW p ℚ m).vars ⊆ range (m + 1)
j : ℕ
hj : j ∈ range n
H : n ∈ (xInTermsOfW p ℚ j ^ p ^ (n - j)).vars
⊢ False
Module: Mathlib.RingTheory.WittVector.Defs

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ constantCoeff (wittAdd p n) = 0

Tactic:
by
  apply constantCoeff_wittStructureInt p _ _ n
  simp only [add_zero, map_add, constantCoeff_X]

Goal state after:
Module: Mathlib.RingTheory.Perfection

Goal state before:
pp: M : Type u_1
inst✝ : CommMonoid M
p : ℕ
f : Perfection M p
m n : ℕ
⊢ (coeffMonoidHom M p (m + n)) f ^ p ^ n = (coeffMonoidHom M p m) f

Tactic:
← map_pow,

Goal state after:
M : Type u_1
inst✝ : CommMonoid M
p : ℕ
f : Perfection M p
m n : ℕ
⊢ (coeffMonoidHom M p (m + n)) (f ^ p ^ n) = (coeffMonoidHom M p m) f
Module: Mathlib.RingTheory.Perfection

Goal state before:
pp: M✝ : Type u_1
inst✝³ : CommMonoid M✝
p✝ p : ℕ
M : Type u_2
inst✝² : CommMonoid M
inst✝¹ : PerfectRing M p
N : Type u_3
inst✝ : CommMonoid N
f : M →* N
r : M
n : ℕ
⊢ (fun n ↦ f ((powMulEquiv M (p ^ n)).symm r)) (n + 1) ^ p = (fun n ↦ f ((powMulEquiv M (p ^ n)).symm r)) n

Tactic:
← map_pow,

Goal state after:
M✝ : Type u_1
inst✝³ : CommMonoid M✝
p✝ p : ℕ
M : Type u_2
inst✝² : CommMonoid M
inst✝¹ : PerfectRing M p
N : Type u_3
inst✝ : CommMonoid N
f : M →* N
r : M
n : ℕ
⊢ f ((powMulEquiv M (p ^ (n + 1))).symm r ^ p) = (fun n ↦ f ((powMulEquiv M (p ^ n)).symm r)) n
Module: Mathlib.RingTheory.Perfection

Goal state before:
pp: M✝ : Type u_1
inst✝³ : CommMonoid M✝
p✝ p : ℕ
M : Type u_2
inst✝² : CommMonoid M
inst✝¹ : PerfectRing M p
N : Type u_3
inst✝ : CommMonoid N
f : M →* Perfection N p
m : M
n : ℕ
⊢ (coeffMonoidHom N p (0 + n)) (f ((powMulEquiv M (p ^ n)).symm m) ^ p ^ n) = (coeffMonoidHom N p n) (f m)

Tactic:
← map_pow,

Goal state after:
M✝ : Type u_1
inst✝³ : CommMonoid M✝
p✝ p : ℕ
M : Type u_2
inst✝² : CommMonoid M
inst✝¹ : PerfectRing M p
N : Type u_3
inst✝ : CommMonoid N
f : M →* Perfection N p
m : M
n : ℕ
⊢ (coeffMonoidHom N p (0 + n)) (f ((powMulEquiv M (p ^ n)).symm m ^ p ^ n)) = (coeffMonoidHom N p n) (f m)
Module: Mathlib.RingTheory.Perfection

Goal state before:
pp: M✝ : Type u_1
inst✝² : CommMonoid M✝
p✝ p : ℕ
M : Type u_2
N : Type u_3
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
φ : M →* N
f : Perfection M p
n : ℕ
⊢ (fun n ↦ φ ((coeffMonoidHom M p n) f)) (n + 1) ^ p = (fun n ↦ φ ((coeffMonoidHom M p n) f)) n

Tactic:
← map_pow,

Goal state after:
M✝ : Type u_1
inst✝² : CommMonoid M✝
p✝ p : ℕ
M : Type u_2
N : Type u_3
inst✝¹ : CommMonoid M
inst✝ : CommMonoid N
φ : M →* N
f : Perfection M p
n : ℕ
⊢ φ ((coeffMonoidHom M p (n + 1)) f ^ p) = (fun n ↦ φ ((coeffMonoidHom M p n) f)) n
Module: Mathlib.RingTheory.WittVector.Verschiebung

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
x : ℕ → ℤ
n : ℕ
hn : ¬n.succ = 0
⊢ (ghostComponent (n + 1)) (verschiebung (mk p x)) = ↑p * (MvPolynomial.eval x) (wittPolynomial p ℤ n)

Tactic:
ghostComponent_verschiebung

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
x : ℕ → ℤ
n : ℕ
hn : ¬n.succ = 0
⊢ ↑p * (ghostComponent n) (mk p x) = ↑p * (MvPolynomial.eval x) (wittPolynomial p ℤ n)
Module: Mathlib.RingTheory.WittVector.IsPoly

Goal state before:
pp: case h
p : ℕ
R S : Type u
idx : Type u_1
inst✝² : CommRing R
inst✝¹ : CommRing S
g : ⦃R : Type u_2⦄ → [CommRing R] → 𝕎 R → 𝕎 R
f : ⦃R : Type u_2⦄ → [CommRing R] → 𝕎 R → 𝕎 R → 𝕎 R
φ : ℕ → MvPolynomial (Fin 2 × ℕ) ℤ
hf : ∀ ⦃R : Type u_2⦄ [inst : CommRing R] (x y : 𝕎 R), (f x y).coeff = fun n ↦ peval (φ n) ![x.coeff, y.coeff]
ψ : ℕ → MvPolynomial ℕ ℤ
hg : ∀ ⦃R : Type u_2⦄ [inst : CommRing R] (x : 𝕎 R), (g x).coeff = fun n ↦ (aeval x.coeff) (ψ n)
R✝ : Type u_2
inst✝ : CommRing R✝
x✝ y✝ : 𝕎 R✝
⊢ (g (f x✝ y✝)).coeff = fun n ↦ peval ((fun n ↦ (bind₁ φ) (ψ n)) n) ![x✝.coeff, y✝.coeff]

Tactic:
simp only [peval, aeval_bind₁, hg, hf]

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

Goal state before:
pp: case zero
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CharP R p
x : 𝕎 R
⊢ (verschiebung (frobenius x)).coeff 0 = 0

Tactic:
verschiebung_coeff_zero

Goal state after:
case zero
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CharP R p
x : 𝕎 R
⊢ 0 = 0
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) =
    ModP.preVal K v O p ((Ideal.Quotient.mk (Ideal.span {↑p})) x) ^ p ^ (Nat.find h + k + 1)

Tactic:
← map_pow,

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 ((Ideal.Quotient.mk (Ideal.span {↑p})) (x ^ p)) ^ p ^ (Nat.find h + k) =
    ModP.preVal K v O p ((Ideal.Quotient.mk (Ideal.span {↑p})) 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
inst✝ : Fact (Nat.Prime p)
m : ℕ
hm : n ≤ m
i : Fin n
x : TruncatedWittVector p m R
⊢ coeff i ((truncate hm) x) = coeff (Fin.castLE hm i) x

Tactic:
obtain ⟨y, rfl⟩ := @WittVector.truncate_surjective p _ _ _ _ x

Goal state after:
p n : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Fact (Nat.Prime p)
m : ℕ
hm : n ≤ m
i : Fin n
y : 𝕎 R
⊢ coeff i ((truncate hm) ((WittVector.truncate m) y)) = coeff (Fin.castLE hm i) ((WittVector.truncate m) y)
Module: Mathlib.RingTheory.Perfectoid.FontaineTheta

Goal state before:
pp: case h
R : Type u
inst✝³ : CommRing R
p : ℕ
inst✝² : Fact (Nat.Prime p)
inst✝¹ : Fact ¬IsUnit ↑p
inst✝ : IsAdicComplete 𝔭 R
n : ℕ
this : ↑p = (Ideal.Quotient.mk (𝔭 ^ (n + 1))) ↑p
⊢ (Ideal.Quotient.mk (𝔭 ^ (n + 1))) ↑p ^ (n + 1) = 0

Tactic:
← map_pow,

Goal state after:
case h
R : Type u
inst✝³ : CommRing R
p : ℕ
inst✝² : Fact (Nat.Prime p)
inst✝¹ : Fact ¬IsUnit ↑p
inst✝ : IsAdicComplete 𝔭 R
n : ℕ
this : ↑p = (Ideal.Quotient.mk (𝔭 ^ (n + 1))) ↑p
⊢ (Ideal.Quotient.mk (𝔭 ^ (n + 1))) (↑p ^ (n + 1)) = 0
Module: Mathlib.RingTheory.Polynomial.Hermite.Basic

Goal state before:
pp: case succ.succ
n : ℕ
ih : ∀ {k : ℕ}, Odd (n + k) → (hermite n).coeff k = 0
k : ℕ
hnk : Odd (n + 1 + (k + 1))
⊢ Odd (n + k)

Tactic:
rw [(by rw [Nat.succ_add, Nat.add_succ] : n.succ + k.succ = n + k + 2)] at hnk

Goal state after:
case succ.succ
n : ℕ
ih : ∀ {k : ℕ}, Odd (n + k) → (hermite n).coeff k = 0
k : ℕ
hnk : Odd (n + k + 2)
⊢ Odd (n + k)
Module: Mathlib.RingTheory.Polynomial.SmallDegreeVieta

Goal state before:
pp: T : Type u_2
S : Type u_3
inst✝³ : CommRing T
inst✝² : CommRing S
inst✝¹ : IsDomain S
inst✝ : Algebra T S
a b c : T
x1 x2 : S
ha : (algebraMap T S) a ≠ 0
⊢ (C a * X ^ 2 + C b * X + C c).aroots S = {x1, x2} ↔
    (algebraMap T S) b = -(algebraMap T S) a * (x1 + x2) ∧ (algebraMap T S) c = (algebraMap T S) a * x1 * x2

Tactic:
rw [aroots_def, show map (algebraMap T S) (C a * X ^ 2 + C b * X + C c) = C ((algebraMap T S) a) *
    X ^ 2 + C ((algebraMap T S) b) * X + C ((algebraMap T S) c) by simp]
  exact roots_quadratic_eq_pair_iff_of_ne_zero ha

Goal state after:
Module: Mathlib.RingTheory.Radical.NatInt

Goal state before:
pp: z : ℤ
⊢ primeFactors z = Finset.map Nat.castEmbedding z.natAbs.primeFactors

Tactic:
obtain rfl | hz := eq_or_ne z 0

Goal state after:
case inl
⊢ primeFactors 0 = Finset.map Nat.castEmbedding (Int.natAbs 0).primeFactors

case inr
z : ℤ
hz : z ≠ 0
⊢ primeFactors z = Finset.map Nat.castEmbedding z.natAbs.primeFactors
Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation

Goal state before:
pp: case degree_lt
A : Type u_1
inst✝ : CommRing A
g : A⟦X⟧
I : Ideal A
⊢ Polynomial.degree 0 < ↑((map (Ideal.Quotient.mk I)) g).order.toNat

pp: case eq_mul_add
A : Type u_1
inst✝ : CommRing A
g : A⟦X⟧
I : Ideal A
⊢ 0 = g * 0 + ↑0

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

Goal state after:
case eq_mul_add
A : Type u_1
inst✝ : CommRing A
g : A⟦X⟧
I : Ideal A
⊢ 0 = g * 0 + ↑0
Module: Mathlib.RingTheory.Regular.ProjectiveDimension

Goal state before:
pp: case coe.top
R : Type u
inst✝⁴ : CommRing R
inst✝³ : Small.{v, u} R
inst✝² : IsLocalRing R
inst✝¹ : IsNoetherianRing R
M : ModuleCat R
inst✝ : Module.Finite R ↑M
x : R
reg : IsSMulRegular (↑M) x
mem : x ∈ maximalIdeal R
sub : Subsingleton ↑M ↔ Subsingleton (QuotSMulTop x ↑M)
aux : ∀ (n : ℕ), projectiveDimension (of R (QuotSMulTop x ↑M)) ≤ ↑n ↔ projectiveDimension M + 1 ≤ ↑n
⊢ projectiveDimension (of R (QuotSMulTop x ↑M)) ≤ ↑⊤ ↔ projectiveDimension M + 1 ≤ ↑⊤

Tactic:
| top =>

Goal state after:
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
H : (X ^ ((map (IsLocalRing.residue A)) g).order.toNat).IsWeierstrassDivision g q r
⊢ IsUnit q

Tactic:
by
  obtain ⟨H1 : r.degree < (g.map (IsLocalRing.residue A)).order.toNat, H2⟩ := H
  set n := (g.map (IsLocalRing.residue A)).order.toNat
  replace H2 := congr(coeff n (($H2).map (IsLocalRing.residue A)))
  simp_rw [map_pow, map_X, coeff_X_pow_self, map_add, map_mul, coeff_map,
    Polynomial.coeff_coe, Polynomial.coeff_eq_zero_of_degree_lt H1, map_zero, add_zero] at H2
  rw [isUnit_iff_constantCoeff, ← isUnit_map_iff (IsLocalRing.residue A)]
  rw [coeff_mul, ← Finset.sum_subset (s₁ := {(n, 0)}) (by simp) (fun p hp hnotMem ↦ ?_),
    Finset.sum_singleton, coeff_map, coeff_map, coeff_zero_eq_constantCoeff, mul_comm] at H2
  · exact .of_mul_eq_one _ H2.symm
  · rw [coeff_of_lt_order p.1 ?_]
    · rw [zero_mul]
    · rw [← ENat.lt_lift_iff (h := order_finite_iff_ne_zero.2 hg), ENat.lift_eq_toNat_of_lt_top]
      refine (Finset.HasAntidiagonal.antidiagonal.fst_le hp).lt_of_ne ?_
      contrapose hnotMem
      rwa [Finset.mem_singleton, Finset.HasAntidiagonal.antidiagonal_congr hp (by simp)]

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

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

Tactic:
IsLocalization.under_map_of_isPrime_disjoint pc _ ‹_› disj

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

Goal state before:
pp: R : Type u_2
M : Type u
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsSemisimpleModule R M
m : Submodule R M
h : m.IsFullyInvariant
S : Submodule R M
le : S ≤ m
x✝¹ : IsSimpleModule R ↥S
S' : Submodule R M
x✝ : S' ∈ {m | Nonempty (↥m ≃ₗ[R] ↥S)}
e : ↥S' ≃ₗ[R] ↥S
⊢ S' ≤ m

Tactic:
have ⟨p, eq⟩ := extension_property _ S.subtype_injective (S'.subtype ∘ₗ e.symm)

Goal state after:
R : Type u_2
M : Type u
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsSemisimpleModule R M
m : Submodule R M
h : m.IsFullyInvariant
S : Submodule R M
le : S ≤ m
x✝¹ : IsSimpleModule R ↥S
S' : Submodule R M
x✝ : S' ∈ {m | Nonempty (↥m ≃ₗ[R] ↥S)}
e : ↥S' ≃ₗ[R] ↥S
p : M →ₗ[R] M
eq : p ∘ₗ S.subtype = S'.subtype ∘ₗ ↑e.symm
⊢ S' ≤ m
Module: Mathlib.RingTheory.SimpleModule.WedderburnArtin

Goal state before:
pp: R₀ : Type u_1
R : Type u
inst✝⁴ : CommSemiring R₀
inst✝³ : Ring R
inst✝² : Algebra R₀ R
inst✝¹ : IsSimpleRing R
inst✝ : IsArtinianRing R
n : ℕ
hn : NeZero n
S : Submodule R R
hS : IsSimpleModule R ↥S
e : R ≃ₗ[R] Fin n → ↥S
⊢ ∃ n,
    ∃ (_ : NeZero n), ∃ I, ∃ (_ : IsSimpleModule R ↥I), Nonempty (R ≃ₐ[R₀] Matrix (Fin n) (Fin n) (Module.End R ↥I)ᵐᵒᵖ)

Tactic:
refine ⟨n, hn, S, hS, ⟨.trans (.opOp R₀ R) <| .trans (.op ?_) (.symm .mopMatrix)⟩⟩

Goal state after:
R₀ : Type u_1
R : Type u
inst✝⁴ : CommSemiring R₀
inst✝³ : Ring R
inst✝² : Algebra R₀ R
inst✝¹ : IsSimpleRing R
inst✝ : IsArtinianRing R
n : ℕ
hn : NeZero n
S : Submodule R R
hS : IsSimpleModule R ↥S
e : R ≃ₗ[R] Fin n → ↥S
⊢ Rᵐᵒᵖ ≃ₐ[R₀] Matrix (Fin n) (Fin n) (Module.End R ↥S)
Module: Mathlib.RingTheory.WittVector.Compare

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

Tactic:
WittVector.coeff_truncate,

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
⊢ ¬(↑p ^ i).coeff ↑⟨i, hin⟩ = coeff ⟨i, hin⟩ 0
Module: Mathlib.RingTheory.WittVector.DiscreteValuationRing

Goal state before:
pp: case succ.succ
p : ℕ
hp✝ : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : Field k
inst✝ : CharP k p
hp : ¬IsUnit ↑p
a : 𝕎 k
ha : a.coeff 0 ≠ 0
b : 𝕎 k
hb : b.coeff 0 ≠ 0
n✝ : ℕ
ha0 : (⇑verschiebung)^[n✝ + 1] a ≠ 0
n : ℕ
hb0 : (⇑verschiebung)^[n + 1] b ≠ 0
hab : ↑p = (⇑verschiebung)^[n✝ + 1] a * (⇑verschiebung)^[n + 1] b
⊢ IsUnit ((⇑verschiebung)^[n✝ + 1] a) ∨ IsUnit ((⇑verschiebung)^[n + 1] b)

Tactic:
rw [iterate_verschiebung_mul] at hab

Goal state after:
case succ.succ
p : ℕ
hp✝ : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : Field k
inst✝ : CharP k p
hp : ¬IsUnit ↑p
a : 𝕎 k
ha : a.coeff 0 ≠ 0
b : 𝕎 k
hb : b.coeff 0 ≠ 0
n✝ : ℕ
ha0 : (⇑verschiebung)^[n✝ + 1] a ≠ 0
n : ℕ
hb0 : (⇑verschiebung)^[n + 1] b ≠ 0
hab : ↑p = (⇑verschiebung)^[n✝ + 1 + (n + 1)] ((⇑frobenius)^[n + 1] a * (⇑frobenius)^[n✝ + 1] b)
⊢ IsUnit ((⇑verschiebung)^[n✝ + 1] a) ∨ IsUnit ((⇑verschiebung)^[n + 1] b)
Module: Mathlib.RingTheory.WittVector.MulCoeff

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ (∑ i ∈ range n, ↑p ^ i * wittMul p i ^ p ^ (n - i)).vars ⊆ univ ×ˢ range n

Tactic:
refine Subset.trans (vars_sum_subset _ _) ?_

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ ((range n).biUnion fun i ↦ (↑p ^ i * wittMul p i ^ p ^ (n - i)).vars) ⊆ univ ×ˢ range n
Module: Mathlib.RingTheory.WittVector.MulCoeff

Goal state before:
pp: case refine_1
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ (∑ x ∈ range (n + 1), (rename (Prod.mk 0)) ((monomial (Finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x))).vars ⊆
    univ ×ˢ range (n + 1)

Tactic:
refine Subset.trans (vars_sum_subset _ _) ?_

Goal state after:
case refine_1
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ ((range (n + 1)).biUnion fun i ↦
      ((rename (Prod.mk 0)) ((monomial (Finsupp.single i (p ^ (n + 1 - i)))) (↑p ^ i))).vars) ⊆
    univ ×ˢ range (n + 1)
Module: Mathlib.RingTheory.WittVector.MulCoeff

Goal state before:
pp: case refine_2
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ (∑ x ∈ range (n + 1), (rename (Prod.mk 1)) ((monomial (Finsupp.single x (p ^ (n + 1 - x)))) (↑p ^ x))).vars ⊆
    univ ×ˢ range (n + 1)

Tactic:
refine Subset.trans (vars_sum_subset _ _) ?_

Goal state after:
case refine_2
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ ((range (n + 1)).biUnion fun i ↦
      ((rename (Prod.mk 1)) ((monomial (Finsupp.single i (p ^ (n + 1 - i)))) (↑p ^ i))).vars) ⊆
    univ ×ˢ range (n + 1)
Module: Mathlib.SetTheory.Ordinal.FixedPointApproximants

Goal state before:
pp: α : Type u
inst✝ : CompleteLattice α
f g : α →o α
h : f ≤ g
x : α
a : Ordinal.{u}
⊢ lfpApprox f x a ≤ lfpApprox g x a

Tactic:
induction a using WellFoundedLT.induction with

Goal state after:
case ind
α : Type u
inst✝ : CompleteLattice α
f g : α →o α
h : f ≤ g
x : α
i : Ordinal.{u}
IH : ∀ y < i, lfpApprox f x y ≤ lfpApprox g x y
⊢ lfpApprox f x i ≤ lfpApprox g x i
Module: Mathlib.SetTheory.Ordinal.FixedPointApproximants

Goal state before:
pp: α : Type u
inst✝ : CompleteLattice α
f : α →o α
x₁ x₂ : α
h : x₁ ≤ x₂
a : Ordinal.{u}
⊢ lfpApprox f x₁ a ≤ lfpApprox f x₂ a

Tactic:
induction a using WellFoundedLT.induction with

Goal state after:
case ind
α : Type u
inst✝ : CompleteLattice α
f : α →o α
x₁ x₂ : α
h : x₁ ≤ x₂
i : Ordinal.{u}
IH : ∀ y < i, lfpApprox f x₁ y ≤ lfpApprox f x₂ y
⊢ lfpApprox f x₁ i ≤ lfpApprox f x₂ i
Module: Mathlib.SetTheory.Lists

Goal state before:
pp: α : Type u_1
l : Lists' α true
x✝ : IsList ⟨true, l⟩
⊢ ofList (toList ⟨true, l⟩) = ⟨true, l⟩

Tactic:
by simp_all [ofList, of']

Goal state after:
Module: Mathlib.SetTheory.Lists

Goal state before:
pp: α : Type u_1
inst✝ : DecidableEq α
l₁ l₂ : Lists' α true
this✝ : Decidable (l₁ ⊆ l₂)
this : Decidable (l₂ ⊆ l₁)
⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
exact decidable_of_iff' _ Equiv.antisymm_iff

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

Goal state before:
pp: case single_add
b : Ordinal.{u_1}
f₂ : Ordinal.{u_1} →₀ Ordinal.{u_1}
e₁ x : Ordinal.{u_1}
f₁ : Ordinal.{u_1} →₀ Ordinal.{u_1}
hf₁ : ∀ c ∈ f₁.support, c < e₁
hx : x ≠ 0
IH : (∀ e₁ ∈ f₁.support, ∀ e₂ ∈ f₂.support, e₂ ≤ e₁) → eval b (f₁ + f₂) = eval b f₁ + eval b f₂
h : ∀ e₁_1 ∈ (single e₁ x + f₁).support, ∀ e₂ ∈ f₂.support, e₂ ≤ e₁_1
⊢ b ^ e₁ * x + (eval b f₁ + eval b f₂) = b ^ e₁ * x + eval b f₁ + eval b f₂

pp: case single_add
b : Ordinal.{u_1}
f₂ : Ordinal.{u_1} →₀ Ordinal.{u_1}
e₁ x : Ordinal.{u_1}
f₁ : Ordinal.{u_1} →₀ Ordinal.{u_1}
hf₁ : ∀ c ∈ f₁.support, c < e₁
hx : x ≠ 0
IH : (∀ e₁ ∈ f₁.support, ∀ e₂ ∈ f₂.support, e₂ ≤ e₁) → eval b (f₁ + f₂) = eval b f₁ + eval b f₂
h : ∀ e₁_1 ∈ (single e₁ x + f₁).support, ∀ e₂ ∈ f₂.support, e₂ ≤ e₁_1
⊢ ∀ e₁ ∈ f₁.support, ∀ e₂ ∈ f₂.support, e₂ ≤ e₁

pp: case single_add.h
b : Ordinal.{u_1}
f₂ : Ordinal.{u_1} →₀ Ordinal.{u_1}
e₁ x : Ordinal.{u_1}
f₁ : Ordinal.{u_1} →₀ Ordinal.{u_1}
hf₁ : ∀ c ∈ f₁.support, c < e₁
hx : x ≠ 0
IH : (∀ e₁ ∈ f₁.support, ∀ e₂ ∈ f₂.support, e₂ ≤ e₁) → eval b (f₁ + f₂) = eval b f₁ + eval b f₂
h : ∀ e₁_1 ∈ (single e₁ x + f₁).support, ∀ e₂ ∈ f₂.support, e₂ ≤ e₁_1
⊢ ∀ e' ∈ (f₁ + f₂).support, e' ≤ e₁

Tactic:
add_assoc

Goal state after:
case single_add
b : Ordinal.{u_1}
f₂ : Ordinal.{u_1} →₀ Ordinal.{u_1}
e₁ x : Ordinal.{u_1}
f₁ : Ordinal.{u_1} →₀ Ordinal.{u_1}
hf₁ : ∀ c ∈ f₁.support, c < e₁
hx : x ≠ 0
IH : (∀ e₁ ∈ f₁.support, ∀ e₂ ∈ f₂.support, e₂ ≤ e₁) → eval b (f₁ + f₂) = eval b f₁ + eval b f₂
h : ∀ e₁_1 ∈ (single e₁ x + f₁).support, ∀ e₂ ∈ f₂.support, e₂ ≤ e₁_1
⊢ b ^ e₁ * x + (eval b f₁ + eval b f₂) = b ^ e₁ * x + (eval b f₁ + eval b f₂)

case single_add
b : Ordinal.{u_1}
f₂ : Ordinal.{u_1} →₀ Ordinal.{u_1}
e₁ x : Ordinal.{u_1}
f₁ : Ordinal.{u_1} →₀ Ordinal.{u_1}
hf₁ : ∀ c ∈ f₁.support, c < e₁
hx : x ≠ 0
IH : (∀ e₁ ∈ f₁.support, ∀ e₂ ∈ f₂.support, e₂ ≤ e₁) → eval b (f₁ + f₂) = eval b f₁ + eval b f₂
h : ∀ e₁_1 ∈ (single e₁ x + f₁).support, ∀ e₂ ∈ f₂.support, e₂ ≤ e₁_1
⊢ ∀ e₁ ∈ f₁.support, ∀ e₂ ∈ f₂.support, e₂ ≤ e₁

case single_add.h
b : Ordinal.{u_1}
f₂ : Ordinal.{u_1} →₀ Ordinal.{u_1}
e₁ x : Ordinal.{u_1}
f₁ : Ordinal.{u_1} →₀ Ordinal.{u_1}
hf₁ : ∀ c ∈ f₁.support, c < e₁
hx : x ≠ 0
IH : (∀ e₁ ∈ f₁.support, ∀ e₂ ∈ f₂.support, e₂ ≤ e₁) → eval b (f₁ + f₂) = eval b f₁ + eval b f₂
h : ∀ e₁_1 ∈ (single e₁ x + f₁).support, ∀ e₂ ∈ f₂.support, e₂ ≤ e₁_1
⊢ ∀ e' ∈ (f₁ + f₂).support, e' ≤ e₁
Module: Mathlib.SetTheory.Ordinal.CantorNormalForm

Goal state before:
pp: case single_add
b e' x : Ordinal.{u_1}
f : Ordinal.{u_1} →₀ Ordinal.{u_1}
hf : ∀ c ∈ f.support, c < e'
hx : x ≠ 0
IH : ∀ {e : Ordinal.{u_1}}, (∀ (e' : Ordinal.{u_1}), f e' < b) → (∀ e' ∈ f.support, e' < e) → eval b f < b ^ e
e : Ordinal.{u_1}
hb : ∀ (e'_1 : Ordinal.{u_1}), (single e' x + f) e'_1 < b
he : ∀ e'_1 ∈ (single e' x + f).support, e'_1 < e
he' : e' ∉ f.support
⊢ eval b (single e' x + f) < b ^ e

Tactic:
rw [eval_single_add' _ hf]

Goal state after:
case single_add
b e' x : Ordinal.{u_1}
f : Ordinal.{u_1} →₀ Ordinal.{u_1}
hf : ∀ c ∈ f.support, c < e'
hx : x ≠ 0
IH : ∀ {e : Ordinal.{u_1}}, (∀ (e' : Ordinal.{u_1}), f e' < b) → (∀ e' ∈ f.support, e' < e) → eval b f < b ^ e
e : Ordinal.{u_1}
hb : ∀ (e'_1 : Ordinal.{u_1}), (single e' x + f) e'_1 < b
he : ∀ e'_1 ∈ (single e' x + f).support, e'_1 < e
he' : e' ∉ f.support
⊢ b ^ e' * x + eval b f < b ^ e
Module: Mathlib.SetTheory.Ordinal.Notation

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

Tactic:
exact oadd_lt_oadd_2 h₂ nh.left

Goal state after: