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
⊢ X n ^ p + C ↑p * (MvPolynomial.map (Int.castRingHom ℚ)) (frobeniusPolyAux p n) =
    (∑ x ∈ range n, C (↑p ^ x) * X x ^ p ^ (n + 1 - x)) * C (⅟↑p ^ n) + C (↑p ^ n) * C (⅟↑p ^ n) * X n ^ p +
        C (↑p ^ (n + 1)) * C (⅟↑p ^ n) * X (n + 1) -
      (∑ x ∈ range n, C (↑p ^ x) * (bind₁ (wittPolynomial p ℚ ∘ fun n ↦ n + 1)) (xInTermsOfW p ℚ x) ^ p ^ (n - x)) *
        C (⅟↑p ^ n)

Tactic:
← C_mul,

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
⊢ X n ^ p + C ↑p * (MvPolynomial.map (Int.castRingHom ℚ)) (frobeniusPolyAux p n) =
    (∑ x ∈ range n, C (↑p ^ x) * X x ^ p ^ (n + 1 - x)) * C (⅟↑p ^ n) + C (↑p ^ n * ⅟↑p ^ n) * X n ^ p +
        C (↑p ^ (n + 1)) * C (⅟↑p ^ n) * X (n + 1) -
      (∑ x ∈ range n, C (↑p ^ x) * (bind₁ (wittPolynomial p ℚ ∘ fun n ↦ n + 1)) (xInTermsOfW p ℚ x) ^ p ^ (n - x)) *
        C (⅟↑p ^ n)
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
⊢ X n ^ p + C ↑p * (MvPolynomial.map (Int.castRingHom ℚ)) (frobeniusPolyAux p n) =
    (∑ x ∈ range n, C (↑p ^ x) * X x ^ p ^ (n + 1 - x)) * C (⅟↑p ^ n) + C (↑p ^ n * ⅟↑p ^ n) * X n ^ p +
        C (↑p ^ (n + 1)) * C (⅟↑p ^ n) * X (n + 1) -
      (∑ x ∈ range n, C (↑p ^ x) * (bind₁ (wittPolynomial p ℚ ∘ fun n ↦ n + 1)) (xInTermsOfW p ℚ x) ^ p ^ (n - x)) *
        C (⅟↑p ^ n)

Tactic:
← C_mul,

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
⊢ X n ^ p + C ↑p * (MvPolynomial.map (Int.castRingHom ℚ)) (frobeniusPolyAux p n) =
    (∑ x ∈ range n, C (↑p ^ x) * X x ^ p ^ (n + 1 - x)) * C (⅟↑p ^ n) + C (↑p ^ n * ⅟↑p ^ n) * X n ^ p +
        C (↑p ^ (n + 1) * ⅟↑p ^ n) * X (n + 1) -
      (∑ x ∈ range n, C (↑p ^ x) * (bind₁ (wittPolynomial p ℚ ∘ fun n ↦ n + 1)) (xInTermsOfW p ℚ x) ^ p ^ (n - x)) *
        C (⅟↑p ^ n)
Module: Mathlib.RingTheory.WittVector.IsPoly

Goal state before:
pp: p : ℕ
R S : Type u
idx : Type u_1
inst✝² : CommRing R
inst✝¹ : CommRing S
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]
R✝ : Type u_2
inst✝ : CommRing R✝
x✝ : 𝕎 R✝
n : ℕ
⊢ (fun a ↦ ![x✝.coeff, x✝.coeff] a.1 a.2) = fun i ↦ (aeval x✝.coeff) (![X, X] i.1 i.2)

Tactic:
ext ⟨i, k⟩

Goal state after:
p : ℕ
R S : Type u
idx : Type u_1
inst✝² : CommRing R
inst✝¹ : CommRing S
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]
R✝ : Type u_2
inst✝ : CommRing R✝
x✝ : 𝕎 R✝
n : ℕ
i : Fin 2
k : ℕ
⊢ ![x✝.coeff, x✝.coeff] (i, k).1 (i, k).2 = (aeval x✝.coeff) (![X, X] (i, k).1 (i, k).2)
Module: Mathlib.RingTheory.WittVector.IsPoly

Goal state before:
pp: p : ℕ
R S : Type u
idx : Type u_1
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Fact (Nat.Prime p)
R✝ : Type u_2
inst✝ : CommRing R✝
x✝ : 𝕎 R✝
n : ℕ
⊢ uncurry ![x✝.coeff] = x✝.coeff ∘ Prod.snd

Tactic:
ext ⟨i, k⟩

Goal state after:
p : ℕ
R S : Type u
idx : Type u_1
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Fact (Nat.Prime p)
R✝ : Type u_2
inst✝ : CommRing R✝
x✝ : 𝕎 R✝
n : ℕ
i : Fin 1
k : ℕ
⊢ uncurry ![x✝.coeff] (i, k) = (x✝.coeff ∘ Prod.snd) (i, k)
Module: Mathlib.RingTheory.WittVector.IsPoly

Goal state before:
pp: p : ℕ
R S : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Fact (Nat.Prime p)
f : ⦃R : Type u⦄ → [CommRing R] → 𝕎 R → 𝕎 R → 𝕎 R
g : R →+* S
x y : 𝕎 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]
n : ℕ
⊢ (fun i ↦ g (![x.coeff, y.coeff] i.1 i.2)) = fun a ↦
    ![((WittVector.map g) x).coeff, ((WittVector.map g) y).coeff] a.1 a.2

Tactic:
ext ⟨i, k⟩

Goal state after:
p : ℕ
R S : Type u
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Fact (Nat.Prime p)
f : ⦃R : Type u⦄ → [CommRing R] → 𝕎 R → 𝕎 R → 𝕎 R
g : R →+* S
x y : 𝕎 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]
n : ℕ
i : Fin 2
k : ℕ
⊢ g (![x.coeff, y.coeff] (i, k).1 (i, k).2) =
    ![((WittVector.map g) x).coeff, ((WittVector.map g) y).coeff] (i, k).1 (i, k).2
Module: Mathlib.RingTheory.Perfection

Goal state before:
pp: case neg
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
hf0 : ¬f = 0
n : ℕ
hn : (coeff n) f ≠ 0
hvf : ModP.preVal K v O p ((coeff n) f) = 0
⊢ (coeff n) f = 0

Tactic:
rwa [ModP.preVal_eq_zero hv] at hvf

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : Invertible 2
⊢ C ⅟2 * 2 = 1

Tactic:
rw [mul_comm, two_mul_C_half_eq_one]

Goal state after:
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 (2 * (n + 1) + (k + 1))).coeff (k + 1) =
    (-1) ^ (n + 1) * ↑(2 * (n + 1) - 1)‼ * ↑((2 * (n + 1) + (k + 1)).choose (k + 1))

Tactic:
have hermite_explicit_recur :
      ∀ n k : ℕ,
        hermite_explicit (n + 1) (k + 1) =
          hermite_explicit (n + 1) k - (k + 2) * hermite_explicit n (k + 2) := by
      intro n k
      simp only [hermite_explicit]
      -- Factor out (-1)'s.
      rw [mul_comm (↑k + _ : ℤ), sub_eq_add_neg]
      nth_rw 3 [neg_eq_neg_one_mul]
      simp only [mul_assoc, ← mul_add, pow_succ']
      congr 2
      -- Factor out double factorials.
      norm_cast
      rw [(by grind : 2 * (n + 1) - 1 = 2 * n + 1),
        Nat.doubleFactorial_add_one, mul_comm (2 * n + 1)]
      simp only [mul_assoc, ← mul_add]
      congr 1
      -- Match up binomial coefficients using `Nat.choose_succ_right_eq`.
      rw [(by ring : 2 * (n + 1) + (k + 1) = 2 * n + 1 + (k + 1) + 1),
        (by ring : 2 * (n + 1) + k = 2 * n + 1 + (k + 1)),
        (by ring : 2 * n + (k + 2) = 2 * n + 1 + (k + 1))]
      rw [Nat.choose, Nat.choose_succ_right_eq (2 * n + 1 + (k + 1)) (k + 1), Nat.add_sub_cancel]
      ring

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) =
    (-1) ^ (n + 1) * ↑(2 * (n + 1) - 1)‼ * ↑((2 * (n + 1) + (k + 1)).choose (k + 1))
Module: Mathlib.RingTheory.Polynomial.HilbertPoly

Goal state before:
pp: case succ
F : Type u_1
inst✝ : Field F
a : F
p : F[X]
d : ℕ
a✝ :
  (match d with
    | 0 => 0
    | d.succ => ∑ i ∈ (a • p).support, (a • p).coeff i • preHilbertPoly F d i) =
    a •
      match d with
      | 0 => 0
      | d.succ => ∑ i ∈ p.support, p.coeff i • preHilbertPoly F d i
⊢ ((a • p).sum fun x r ↦ r • preHilbertPoly F d x) = a • p.sum fun x r ↦ r • preHilbertPoly F d x

Tactic:
Polynomial.smul_sum,

Goal state after:
case succ
F : Type u_1
inst✝ : Field F
a : F
p : F[X]
d : ℕ
a✝ :
  (match d with
    | 0 => 0
    | d.succ => ∑ i ∈ (a • p).support, (a • p).coeff i • preHilbertPoly F d i) =
    a •
      match d with
      | 0 => 0
      | d.succ => ∑ i ∈ p.support, p.coeff i • preHilbertPoly F d i
⊢ ((a • p).sum fun x r ↦ r • preHilbertPoly F d x) = p.sum fun n a_1 ↦ a • a_1 • preHilbertPoly F d n
Module: Mathlib.RingTheory.Polynomial.IrreducibleRing

Goal state before:
pp: R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : (nilradical R).IsPrime
inst✝¹ : CommRing S
inst✝ : IsDomain S
φ : R →+* S
f : R[X]
hm : f.Monic
hi : Irreducible (Polynomial.map φ f)
R' : Type u_1 := R ⧸ nilradical R
ψ : R' →+* S := Ideal.Quotient.lift (nilradical R) φ ⋯
ι : R →+* R' := algebraMap R R'
⊢ Irreducible f

Tactic:
show φ = ψ.comp ι from rfl,

Goal state after:
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : (nilradical R).IsPrime
inst✝¹ : CommRing S
inst✝ : IsDomain S
φ : R →+* S
f : R[X]
hm : f.Monic
R' : Type u_1 := R ⧸ nilradical R
ψ : R' →+* S := Ideal.Quotient.lift (nilradical R) φ ⋯
ι : R →+* R' := algebraMap R R'
hi : Irreducible (Polynomial.map (ψ.comp ι) f)
⊢ Irreducible f
Module: Mathlib.RingTheory.Polynomial.Dickson

Goal state before:
pp: case neg
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
⊢ ∃ y, x + x⁻¹ = y + y⁻¹ ∧ ¬y = 0

Tactic:
exact ⟨_, rfl, hx⟩

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:
ext; simp [opRingEquiv, ← ofFinsupp_single]

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
⊢ IsDomain R[X] ↔ IsDomain R ∧ IsCancelAdd R

Tactic:
isDomain_iff_cancelMulZero_and_nontrivial,

Goal state after:
R : Type u_1
inst✝ : Semiring R
⊢ IsCancelMulZero R[X] ∧ Nontrivial R[X] ↔ (IsCancelMulZero R ∧ Nontrivial R) ∧ IsCancelAdd R
Module: Mathlib.RingTheory.PowerSeries.Schroder

Goal state before:
pp: case isFalse
n : ℕ
hn : 0 < n
x : ℕ
a : x < n
h✝ : ¬0 < x
⊢ (coeff x) (X * largeSchroderSeries) * (n - x).largeSchroder = 0

Tactic:
next h =>
      simp_all only [not_lt, nonpos_iff_eq_zero, coeff_zero_eq_constantCoeff, map_mul,
      constantCoeff_X, constantCoeff_largeSchroderSeries, mul_one, tsub_zero, zero_mul]

Goal state after:
Module: Mathlib.RingTheory.PowerSeries.Log

Goal state before:
pp: A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n : ℕ
this : ↑n + 1 = (algebraMap ℚ A) (↑n + 1)
⊢ (coeff n) ((d⁄dX A) (log A)) = (coeff n) (mk fun n ↦ (algebraMap ℚ A) ((-1) ^ n))

Tactic:
rw [coeff_derivative, coeff_log, coeff_mk]

Goal state after:
A : Type u_1
inst✝¹ : CommRing A
inst✝ : Algebra ℚ A
n : ℕ
this : ↑n + 1 = (algebraMap ℚ A) (↑n + 1)
⊢ (if n + 1 = 0 then 0 else (algebraMap ℚ A) ((-1) ^ (n + 1 + 1) / ↑(n + 1))) * (↑n + 1) = (algebraMap ℚ A) ((-1) ^ n)
Module: Mathlib.RingTheory.Radical.NatInt

Goal state before:
pp: n : ℕ
pp : ∀ p ∈ n.primeFactors, 1 ≤ p
⊢ (∃ x ∈ n.primeFactors, 1 < x) ↔ n.primeFactors.Nonempty

Tactic:
exact ⟨fun ⟨p, h⟩ ↦ ⟨p, h.1⟩, fun ⟨p, h⟩ ↦ ⟨p, h, (mem_primeFactors.mp h).1.one_lt⟩⟩

Goal state after:
Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation

Goal state before:
pp: A : Type u_1
inst✝ : CommRing A
f g q : A⟦X⟧
r : A[X]
I : Ideal A
f' q' : A⟦X⟧
r' : A[X]
H : f.IsWeierstrassDivisionAt g q r I
H' : f'.IsWeierstrassDivisionAt g q' r' I
⊢ f + f' = g * (q + q') + ↑(r + r')

Tactic:
rw [H.eq_mul_add, H'.eq_mul_add, Polynomial.coe_add]

Goal state after:
A : Type u_1
inst✝ : CommRing A
f g q : A⟦X⟧
r : A[X]
I : Ideal A
f' q' : A⟦X⟧
r' : A[X]
H : f.IsWeierstrassDivisionAt g q r I
H' : f'.IsWeierstrassDivisionAt g q' r' I
⊢ g * q + ↑r + (g * q' + ↑r') = g * (q + q') + (↑r + ↑r')
Module: Mathlib.RingTheory.PolynomialLaw.Basic

Goal state before:
pp: case e'_3
R : Type u
inst✝⁶ : CommSemiring R
M : Type u_3
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
N : Type u_4
inst✝³ : AddCommMonoid N
inst✝² : Module R N
f : M →ₚₗ[R] N
S : Type u_5
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
x : M
⊢ 1 ⊗ₜ[R] x = (rTensor M (Algebra.ofId R S).toLinearMap) (1 ⊗ₜ[R] x)

Tactic:
· rw [rTensor_tmul, toLinearMap_apply, _root_.map_one]

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

Goal state before:
pp: R : Type u_2
M : Type u
N : Type u_3
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup N
inst✝² : Module R M
inst✝¹ : Module R N
S : Submodule R M
inst✝ : IsSimpleModule R ↥S
f : M →ₗ[R] N
⊢ map f S ≤ isotypicComponent R N ↥S

Tactic:
by
  conv_lhs => rw [← S.range_subtype, ← LinearMap.range_comp]
  obtain inj | eq := (f ∘ₗ S.subtype).injective_or_eq_zero
  · exact le_sSup ⟨.symm <| .ofInjective _ inj⟩
  · simp_rw [eq, LinearMap.range_zero, bot_le]

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

Goal state before:
pp: R : Type u_2
M : Type u
S : Type u_4
inst✝⁶ : Ring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup S
inst✝³ : Module R M
inst✝² : Module R S
inst✝¹ : IsSimpleModule R S
inst✝ : IsSemisimpleModule R M
ne : isotypicComponent R M S ≠ ⊥
⊢ IsIsotypicOfType R (↥(isotypicComponent R M S)) S ∧ (isotypicComponent R M S).IsFullyInvariant

Tactic:
exact ⟨.isotypicComponent R M S, .isotypicComponent R M S⟩

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:
Units.val_lt_val

Goal state after:
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
Module: Mathlib.RingTheory.WittVector.DiscreteValuationRing

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

Tactic:
cases m

Goal state after:
case zero
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
n : ℕ
b : 𝕎 k
hb : b.coeff 0 ≠ 0
hb0 : (⇑verschiebung)^[n] b ≠ 0
ha0 : (⇑verschiebung)^[0] a ≠ 0
hab : ↑p = (⇑verschiebung)^[0] a * (⇑verschiebung)^[n] b
⊢ IsUnit ((⇑verschiebung)^[0] a) ∨ IsUnit ((⇑verschiebung)^[n] b)

case 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
n : ℕ
b : 𝕎 k
hb : b.coeff 0 ≠ 0
hb0 : (⇑verschiebung)^[n] b ≠ 0
n✝ : ℕ
ha0 : (⇑verschiebung)^[n✝ + 1] a ≠ 0
hab : ↑p = (⇑verschiebung)^[n✝ + 1] a * (⇑verschiebung)^[n] b
⊢ IsUnit ((⇑verschiebung)^[n✝ + 1] a) ∨ IsUnit ((⇑verschiebung)^[n] b)
Module: Mathlib.SetTheory.Ordinal.FixedPointApproximants

Goal state before:
pp: α : Type u
inst✝ : CompleteLattice α
f : α →o α
x : α
hx : x ≤ f x
o : Ordinal.{u}
h : lfpApprox f x o = x
ho : o ≠ 0
hpos : 0 < o
hmem : lfpApprox f x 0 ∈ fixedPoints ⇑f
⊢ x ∈ fixedPoints ⇑f

Tactic:
simpa [lfpApprox_zero] using hmem

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

Goal state before:
pp: case h
α : Type u
inst✝ : CompleteLattice α
f : α →o α
x : α
h_ninj :
  ∃ a b,
    (Set.Iio (SuccOrder.succ #α).ord).domRestrict (lfpApprox f x) a =
        (Set.Iio (SuccOrder.succ #α).ord).domRestrict (lfpApprox f x) b ∧
      a ≠ b
a b : ↑(Set.Iio (SuccOrder.succ #α).ord)
h_fab :
  (Set.Iio (SuccOrder.succ #α).ord).domRestrict (lfpApprox f x) a =
    (Set.Iio (SuccOrder.succ #α).ord).domRestrict (lfpApprox f x) b
h_nab : a ≠ b
⊢ ↑a < (succ #α).ord ∧ ∃ b < (succ #α).ord, ↑a ≠ b ∧ lfpApprox f x ↑a = lfpApprox f x b

Tactic:
apply And.intro a.prop

Goal state after:
case h
α : Type u
inst✝ : CompleteLattice α
f : α →o α
x : α
h_ninj :
  ∃ a b,
    (Set.Iio (SuccOrder.succ #α).ord).domRestrict (lfpApprox f x) a =
        (Set.Iio (SuccOrder.succ #α).ord).domRestrict (lfpApprox f x) b ∧
      a ≠ b
a b : ↑(Set.Iio (SuccOrder.succ #α).ord)
h_fab :
  (Set.Iio (SuccOrder.succ #α).ord).domRestrict (lfpApprox f x) a =
    (Set.Iio (SuccOrder.succ #α).ord).domRestrict (lfpApprox f x) b
h_nab : a ≠ b
⊢ ∃ b < (succ #α).ord, ↑a ≠ b ∧ lfpApprox f x ↑a = lfpApprox f x b
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: e₁ : ONote
n₁ : ℕ+
a₁ e₂ : ONote
n₂ : ℕ+
a₂ : ONote
⊢ (e₁.cmp e₂).then ((_root_.cmp ↑n₁ ↑n₂).then (a₁.cmp a₂)) = Ordering.eq → e₁.oadd n₁ a₁ = e₂.oadd n₂ a₂

Tactic:
cases h₁ : cmp e₁ e₂

Goal state after:
case lt
e₁ : ONote
n₁ : ℕ+
a₁ e₂ : ONote
n₂ : ℕ+
a₂ : ONote
h₁ : e₁.cmp e₂ = Ordering.lt
⊢ Ordering.lt.then ((_root_.cmp ↑n₁ ↑n₂).then (a₁.cmp a₂)) = Ordering.eq → e₁.oadd n₁ a₁ = e₂.oadd n₂ a₂

case eq
e₁ : ONote
n₁ : ℕ+
a₁ e₂ : ONote
n₂ : ℕ+
a₂ : ONote
h₁ : e₁.cmp e₂ = Ordering.eq
⊢ Ordering.eq.then ((_root_.cmp ↑n₁ ↑n₂).then (a₁.cmp a₂)) = Ordering.eq → e₁.oadd n₁ a₁ = e₂.oadd n₂ a₂

case gt
e₁ : ONote
n₁ : ℕ+
a₁ e₂ : ONote
n₂ : ℕ+
a₂ : ONote
h₁ : e₁.cmp e₂ = Ordering.gt
⊢ Ordering.gt.then ((_root_.cmp ↑n₁ ↑n₂).then (a₁.cmp a₂)) = Ordering.eq → e₁.oadd n₁ a₁ = e₂.oadd n₂ a₂
Module: Mathlib.SetTheory.Ordinal.Topology

Goal state before:
pp: case refine_2.refine_1
s : Set Ordinal.{u}
hs : ¬BddAbove s
Hs : StrictMono (enumOrd s)
h : IsClosed s
a : Ordinal.{u}
ha : IsSuccLimit a
o : Ordinal.{u}
H : ∀ b < a, enumOrd s b ≤ o
this✝ : sSup (enumOrd s '' Set.Iio a) ∈ closure (enumOrd s '' Set.Iio a)
this : sSup (enumOrd s '' Set.Iio a) ∈ s
⊢ o ∈ upperBounds (enumOrd s '' Set.Iio a)

Tactic:
grind [upperBounds]

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

Goal state before:
pp: x y : ZFSet.{u}
h : x ≠ y
⊢ 2 = {y}.card + 1

Tactic:
card_singleton,

Goal state after:
x y : ZFSet.{u}
h : x ≠ y
⊢ 2 = 1 + 1
Module: Mathlib.SetTheory.Ordinal.Veblen

Goal state before:
pp: o a : Ordinal.{u}
h : a < veblen o a
⊢ (veblen o a).invVeblen₁ = o

Tactic:
apply le_antisymm
  · rwa [← lt_veblen_iff_invVeblen₁_le, veblen_lt_veblen_iff_right]
  · rw [← mem_range_veblen_iff_le_invVeblen₁]
    obtain rfl | ho := eq_zero_or_pos o
    · simp
    · rw [← veblen_zero_apply, veblen_veblen_of_lt ho]
      simp

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

Goal state before:
pp: case h
x✝ x : PSet.{u}
ih : ∀ y ∈ x, lift.{u + 1, u} y.rank = IsWellFounded.rank (fun x1 x2 ↦ x1 ∈ x2) y
⊢ lift.{u + 1, u} x.rank = IsWellFounded.rank (fun x1 x2 ↦ x1 ∈ x2) x

Tactic:
rw [IsWellFounded.rank_eq]

Goal state after:
case h
x✝ x : PSet.{u}
ih : ∀ y ∈ x, lift.{u + 1, u} y.rank = IsWellFounded.rank (fun x1 x2 ↦ x1 ∈ x2) y
⊢ lift.{u + 1, u} x.rank = ⨆ b, succ (IsWellFounded.rank (fun x1 x2 ↦ x1 ∈ x2) ↑b)
Module: Mathlib.SetTheory.ZFC.Class

Goal state before:
pp: x : Class.{u_1}
y : ZFSet.{u_1}
⊢ (⋃₀ x) y ↔ ∃ z, x z ∧ y ∈ z

Tactic:
constructor
  · rintro ⟨-, ⟨z, rfl, hxz⟩, hyz⟩
    exact ⟨z, hxz, hyz⟩
  · exact fun ⟨z, hxz, hyz⟩ => ⟨_, coe_mem.2 hxz, hyz⟩

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

Goal state before:
pp: case h
x✝ x : ZFSet.{u}
ih : ∀ y ∈ x, lift.{u + 1, u} y.rank = IsWellFounded.rank (fun x1 x2 ↦ x1 ∈ x2) y
⊢ lift.{u + 1, u} x.rank = IsWellFounded.rank (fun x1 x2 ↦ x1 ∈ x2) x

Tactic:
rw [IsWellFounded.rank_eq]

Goal state after:
case h
x✝ x : ZFSet.{u}
ih : ∀ y ∈ x, lift.{u + 1, u} y.rank = IsWellFounded.rank (fun x1 x2 ↦ x1 ∈ x2) y
⊢ lift.{u + 1, u} x.rank = ⨆ b, succ (IsWellFounded.rank (fun x1 x2 ↦ x1 ∈ x2) ↑b)
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: case lt
e₁ : ONote
n₁ : ℕ+
a₁ e₂ : ONote
n₂ : ℕ+
a₂ : ONote
h₁ : (e₁.oadd n₁ a₁).NF
h₂ : (e₂.oadd n₂ a₂).NF
this✝ : a₁.NF
this : a₂.NF
h' : (a₁.sub a₂).repr = a₁.repr - a₂.repr
h : e₁.cmp e₂ = Ordering.lt
ee : Ordering.lt.Compares e₁ e₂
⊢ (e₁.oadd n₁ a₁).repr ≤ (e₂.oadd n₂ a₂).repr

Tactic:
exact le_of_lt (oadd_lt_oadd_1 h₁ ee)

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

Goal state before:
pp: case eq.succ
e₁ : ONote
n₁ : ℕ+
a₁ : ONote
n₂ : ℕ+
a₂ : ONote
h₁ : (e₁.oadd n₁ a₁).NF
this✝ : a₁.NF
this : a₂.NF
h' : (a₁.sub a₂).repr = a₁.repr - a₂.repr
h₂ : (e₁.oadd n₂ a₂).NF
h : e₁.cmp e₁ = Ordering.eq
n✝ : ℕ
mn : ↑n₁ - ↑n₂ = n✝ + 1
⊢ (e₁.oadd n✝.succPNat a₁).repr = (e₁.oadd n₁ a₁).repr - (e₁.oadd n₂ a₂).repr

Tactic:
simp only [Nat.succPNat, Nat.succ_eq_add_one, repr, PNat.mk_coe, ← succ_eq_add_one]
        rw [(tsub_eq_iff_eq_add_of_le <| le_of_lt <| Nat.lt_of_sub_eq_succ mn).1 mn, add_comm,
          Nat.cast_add, mul_add, add_assoc, add_sub_add_cancel]
        refine
          (Ordinal.sub_eq_of_add_eq <|
              add_of_omega0_opow_le h₂.snd'.repr_lt <| le_trans ?_ le_self_add).symm
        exact Ordinal.le_mul_left _ (Nat.cast_lt.2 <| Nat.succ_pos _)

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

Goal state before:
pp: e₁ : ONote
n₁ : ℕ+
a₁ : ONote
b₁ : Ordinal.{0}
h₁ : (e₁.oadd n₁ a₁).NFBelow b₁
e₂ : ONote
n₂ : ℕ+
a₂ : ONote
b₂ : Ordinal.{0}
h₂ : (e₂.oadd n₂ a₂).NFBelow b₂
⊢ (e₁.oadd n₁ a₁ * e₂.oadd n₂ a₂).NFBelow (e₁.repr + b₂)

Tactic:
by
    have IH := oadd_mul_nfBelow h₁ h₂.snd
    by_cases e0 : e₂ = 0 <;> simp only [e0, oadd_mul, ↓reduceIte]
    · apply NFBelow.oadd h₁.fst h₁.snd
      grw [← h₂.lt.pos, add_zero]
    · have := h₁.fst
      have := h₂.fst
      apply NFBelow.oadd
      · infer_instance
      · rwa [repr_add]
      · grw [repr_add, h₂.lt]

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

Goal state before:
pp: case oadd.succ.zero
o₁ o₂ : ONote
inst✝¹ : o₁.NF
inst✝ : o₂.NF
m : ℕ
b' : ONote
this✝ : b'.NF
a0 : ONote
n : ℕ+
a' : ONote
e₁ : o₁.split = (a0.oadd n a', m)
na : (a0.oadd n a').NF
this : a0.NF
e₂ : o₂.split' = (b', 0 + 1)
⊢ (match (scale 1 b', 0 + 1) with
    | (b, 0) => (a0 * b).oadd 1 0
    | (b, k.succ) => (a0 * b + a0 * ↑k).scale (a0.oadd n a') + (a0 * b).opowAux a0 (a0.oadd n a' * ↑m) k m).NF

Tactic:
cases m

Goal state after:
case oadd.succ.zero.zero
o₁ o₂ : ONote
inst✝¹ : o₁.NF
inst✝ : o₂.NF
b' : ONote
this✝ : b'.NF
a0 : ONote
n : ℕ+
a' : ONote
na : (a0.oadd n a').NF
this : a0.NF
e₂ : o₂.split' = (b', 0 + 1)
e₁ : o₁.split = (a0.oadd n a', 0)
⊢ (match (scale 1 b', 0 + 1) with
    | (b, 0) => (a0 * b).oadd 1 0
    | (b, k.succ) => (a0 * b + a0 * ↑k).scale (a0.oadd n a') + (a0 * b).opowAux a0 (a0.oadd n a' * ↑0) k 0).NF

case oadd.succ.zero.succ
o₁ o₂ : ONote
inst✝¹ : o₁.NF
inst✝ : o₂.NF
b' : ONote
this✝ : b'.NF
a0 : ONote
n : ℕ+
a' : ONote
na : (a0.oadd n a').NF
this : a0.NF
e₂ : o₂.split' = (b', 0 + 1)
n✝ : ℕ
e₁ : o₁.split = (a0.oadd n a', n✝ + 1)
⊢ (match (scale 1 b', 0 + 1) with
    | (b, 0) => (a0 * b).oadd 1 0
    | (b, k.succ) =>
      (a0 * b + a0 * ↑k).scale (a0.oadd n a') + (a0 * b).opowAux a0 (a0.oadd n a' * ↑(n✝ + 1)) k (n✝ + 1)).NF