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

Goal state before:
pp: 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)
x✝ : ℕ
⊢ (fun i ↦ ↑ULift.ringEquiv.symm (x i)) = (mk p fun i ↦ { down := x i }).coeff

Tactic:
simp only [coeff_mk]

Goal state after:
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)
x✝ : ℕ
⊢ (fun i ↦ ↑ULift.ringEquiv.symm (x i)) = fun i ↦ { down := x i }
Module: Mathlib.RingTheory.WittVector.IsPoly

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
f g : ⦃R : Type u⦄ → [CommRing R] → 𝕎 R → 𝕎 R
hf : IsPoly p f
hg : IsPoly p g
h : ∀ (R : Type u) [_Rcr : CommRing R] (x : 𝕎 R) (n : ℕ), (ghostComponent n) (f x) = (ghostComponent n) (g x)
⊢ ∀ (R : Type u) [_Rcr : CommRing R] (x : 𝕎 R), f x = g x

Tactic:
obtain ⟨φ, hf⟩ := hf
  obtain ⟨ψ, hg⟩ := hg
  intros
  ext n
  rw [hf, hg, poly_eq_of_wittPolynomial_bind_eq p φ ψ]
  intro k
  apply MvPolynomial.funext
  intro x
  simp only [hom_bind₁]
  specialize h (ULift ℤ) (mk p fun i => ⟨x i⟩) k
  simp only [ghostComponent_apply, aeval_eq_eval₂Hom] at h
  apply (ULift.ringEquiv.symm : ℤ ≃+* _).injective
  simp only [← RingEquiv.coe_toRingHom, map_eval₂Hom]
  convert! h using 1
  all_goals
    simp only [hf, hg, MvPolynomial.eval, map_eval₂Hom]
    apply eval₂Hom_congr (RingHom.ext_int _ _) _ rfl
    ext1
    apply eval₂Hom_congr (RingHom.ext_int _ _) _ rfl
    simp only [coeff_mk]; rfl

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

Goal state before:
pp: case h₀
p : ℕ
hp : Fact (Nat.Prime p)
n i : ℕ
_hi : i ∈ Finset.range (n + 1)
hi0 : i ≠ 0
⊢ (bind₁ onePoly) (C (↑p ^ i) * X i ^ p ^ (n - i)) = 0

Tactic:
simp only [onePoly, if_neg hi0, zero_pow (pow_ne_zero _ hp.1.ne_zero), mul_zero, map_pow,
      bind₁_X_right, map_mul]

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
i : ℕ
h : (↑p ^ i).coeff i = 1
⊢ (↑p ^ (i + 1)).coeff (i + 1) = 1

Tactic:
pow_succ,

Goal state after:
case succ
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CharP R p
i : ℕ
h : (↑p ^ i).coeff i = 1
⊢ (↑p ^ i * ↑p).coeff (i + 1) = 1
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
i : ℕ
hi : ∀ {j : ℕ}, j ≠ i → (↑p ^ i).coeff j = 0
j : ℕ
hj : j ≠ i + 1
⊢ (↑p ^ (i + 1)).coeff j = 0

Tactic:
pow_succ,

Goal state after:
case succ
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CharP R p
i : ℕ
hi : ∀ {j : ℕ}, j ≠ i → (↑p ^ i).coeff j = 0
j : ℕ
hj : j ≠ i + 1
⊢ (↑p ^ i * ↑p).coeff j = 0
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 : ℕ}, m < n → (x * ↑p ^ n).coeff m = 0
m : ℕ
h : m < n + 1
⊢ (x * ↑p ^ (n + 1)).coeff m = 0

Tactic:
pow_succ,

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 : ℕ}, m < n → (x * ↑p ^ n).coeff m = 0
m : ℕ
h : m < n + 1
⊢ (x * (↑p ^ n * ↑p)).coeff m = 0
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 + 1)).coeff (m + (n + 1)) = x.coeff m ^ p ^ (n + 1)

Tactic:
pow_succ,

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.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).coeff (m + n) ^ p = x.coeff m ^ p ^ (n + 1)

Tactic:
pow_succ,

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).coeff (m + n) ^ p = x.coeff m ^ (p ^ n * p)
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
⊢ 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 + 1))) f) ^ p ^ (Nat.find h + (k + 1))

Tactic:
obtain ⟨x, hx⟩ := Ideal.Quotient.mk_surjective (coeff (Nat.find h + k + 1) f)

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
⊢ 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 + 1))) f) ^ p ^ (Nat.find h + (k + 1))
Module: Mathlib.RingTheory.WittVector.Frobenius

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
x : 𝕎 (ZMod p)
⊢ frobenius x = x

Tactic:
simp only [WittVector.ext_iff, coeff_frobenius_charP, ZMod.pow_card,
    forall_const]

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 : (⇑verschiebung ∘ ⇑frobenius)^[n] x = x * ↑p ^ n
⊢ (⇑verschiebung ∘ ⇑frobenius) (x * ↑p ^ n) = x * ↑p ^ (n + 1)

Tactic:
pow_succ,

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 : (⇑verschiebung ∘ ⇑frobenius)^[n] x = x * ↑p ^ n
⊢ (⇑verschiebung ∘ ⇑frobenius) (x * ↑p ^ n) = x * (↑p ^ n * ↑p)
Module: Mathlib.RingTheory.WittVector.Identities

Goal state before:
pp: p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CharP R p
x : 𝕎 R
n : ℕ
⊢ (⇑verschiebung ∘ ⇑frobenius)^[n] x = x * ↑p ^ n

Tactic:
induction n with
  | zero => simp
  | succ n ih =>
    rw [iterate_succ_apply', ih, pow_succ, comp_apply, verschiebung_frobenius, mul_assoc]

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

Goal state before:
pp: p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
x y : MvPolynomial R ℤ
⊢ teichmullerFun p ((counit R) x * (counit R) y) = teichmullerFun p ((counit R) x) * teichmullerFun p ((counit R) y)

Tactic:
simp only [← map_teichmullerFun, ← map_mul, teichmuller_mul_aux₂]

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝ : CommRing k
x y : 𝕎 k
n : ℕ
⊢ (truncate n) (x - y) = 0 ↔ ∀ i < n, (x - y).coeff i = 0

Tactic:
simp only [← mem_ker_truncate, RingHom.mem_ker]

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

Goal state before:
pp: case refine_1
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : CommRing k
inst✝¹ : CharP k p
inst✝ : PerfectRing k p
x : 𝕎 k
x✝ : ∃ c, x = c * ↑p
u : 𝕎 k
hu : x = u * ↑p
⊢ x.coeff 0 = 0

Tactic:
rw [hu, mul_charP_coeff_zero]

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

Goal state before:
pp: case e_a
R : Type u_1
inst✝ : CommRing R
m n : ℕ
h : 1 = (Int.castRingHom R) 1
⊢ (2 * Chebyshev.T ℚ ↑m).comp (Chebyshev.T ℚ ↑n) = (2 * Chebyshev.T ℚ ↑m).comp ((C ⅟2 * X).comp (2 * Chebyshev.T ℚ ↑n))

Tactic:
apply eval₂_congr rfl _ rfl

Goal state after:
R : Type u_1
inst✝ : CommRing R
m n : ℕ
h : 1 = (Int.castRingHom R) 1
⊢ Chebyshev.T ℚ ↑n = (C ⅟2 * X).comp (2 * Chebyshev.T ℚ ↑n)
Module: Mathlib.RingTheory.Polynomial.Opposites

Goal state before:
pp: case pos
R : Type u_1
inst✝ : Semiring R
p : R[X]ᵐᵒᵖ
p0 : p = 0
⊢ ((opRingEquiv R) p).natDegree = (unop p).natDegree

pp: case neg
R : Type u_1
inst✝ : Semiring R
p : R[X]ᵐᵒᵖ
p0 : ¬p = 0
⊢ ((opRingEquiv R) p).natDegree = (unop p).natDegree

Tactic:
· simp only [p0, map_zero, natDegree_zero, unop_zero]

Goal state after:
case neg
R : Type u_1
inst✝ : Semiring R
p : R[X]ᵐᵒᵖ
p0 : ¬p = 0
⊢ ((opRingEquiv R) p).natDegree = (unop p).natDegree
Module: Mathlib.RingTheory.Polynomial.HilbertPoly

Goal state before:
pp: F : Type u_1
inst✝¹ : Field F
inst✝ : CharZero F
p : F[X]
d : ℕ
hh : p.hilbertPoly d ≠ 0
hp : p ≠ 0
h : ¬rootMultiplicity 1 p < d
⊢ False

Tactic:
exact hh (hilbertPoly_eq_zero_of_le_rootMultiplicity_one <| not_lt.1 h)

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

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

Tactic:
exact roots_quadratic_eq_pair_iff_of_ne_zero' ha

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

Goal state before:
pp: A : Type u_1
inst✝ : Semiring A
I : Ideal A
f g : A⟦X⟧
hg : ∀ (i : ℕ), (coeff i) g ∈ I
⊢ ∀ (i : ℕ), (coeff i) (f * g) ∈ I

Tactic:
by
  simpa using coeff_mul_mem_ideal_mul_ideal_of_coeff_mem_ideal' (I := ⊤) (f := f) (by simp) hg

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

Goal state before:
pp: R : Type u_2
inst✝ : CommRing R
p : ℕ
hp : p ≠ 0
r : R
| (expand p hp) (r • 1)

Tactic:
expand,

Goal state after:
R : Type u_2
inst✝ : CommRing R
p : ℕ
hp : p ≠ 0
r : R
| (MvPowerSeries.expand p hp) (r • 1)
Module: Mathlib.RingTheory.PowerSeries.Expand

Goal state before:
pp: R : Type u_2
inst✝ : CommRing R
p : ℕ
hp : p ≠ 0
φ : R⟦X⟧
m : ℕ
⊢ (MvPowerSeries.coeff (Finsupp.single () (p * m))) ((expand p hp) φ) = (MvPowerSeries.coeff (Finsupp.single () m)) φ

Tactic:
expand,

Goal state after:
R : Type u_2
inst✝ : CommRing R
p : ℕ
hp : p ≠ 0
φ : R⟦X⟧
m : ℕ
⊢ (MvPowerSeries.coeff (Finsupp.single () (p * m))) ((MvPowerSeries.expand p hp) φ) =
    (MvPowerSeries.coeff (Finsupp.single () m)) φ
Module: Mathlib.RingTheory.PowerSeries.Expand

Goal state before:
pp: R : Type u_2
inst✝ : CommRing R
p : ℕ
hp : p ≠ 0
φ : R⟦X⟧
m : ℕ
h : ¬p ∣ m
⊢ (MvPowerSeries.coeff (Finsupp.single () m)) ((expand p hp) φ) = 0

Tactic:
expand,

Goal state after:
R : Type u_2
inst✝ : CommRing R
p : ℕ
hp : p ≠ 0
φ : R⟦X⟧
m : ℕ
h : ¬p ∣ m
⊢ (MvPowerSeries.coeff (Finsupp.single () m)) ((MvPowerSeries.expand p hp) φ) = 0
Module: Mathlib.RingTheory.PowerSeries.Expand

Goal state before:
pp: R : Type u_2
inst✝ : CommRing R
p : ℕ
hp : p ≠ 0
φ : R⟦X⟧
⊢ Function.support ((expand p hp) φ) ⊆ (fun x ↦ p • x) '' Function.support φ

Tactic:
expand,

Goal state after:
R : Type u_2
inst✝ : CommRing R
p : ℕ
hp : p ≠ 0
φ : R⟦X⟧
⊢ Function.support ((MvPowerSeries.expand p hp) φ) ⊆ (fun x ↦ p • x) '' Function.support φ
Module: Mathlib.RingTheory.PowerSeries.Expand

Goal state before:
pp: R : Type u_2
inst✝ : CommRing R
p : ℕ
hp : p ≠ 0
φ : R⟦X⟧
⊢ Function.support ((expand p hp) φ) = (fun x ↦ p • x) '' Function.support φ

Tactic:
expand,

Goal state after:
R : Type u_2
inst✝ : CommRing R
p : ℕ
hp : p ≠ 0
φ : R⟦X⟧
⊢ Function.support ((MvPowerSeries.expand p hp) φ) = (fun x ↦ p • x) '' Function.support φ
Module: Mathlib.RingTheory.PowerSeries.Expand

Goal state before:
pp: R : Type u_2
inst✝ : CommRing R
p : ℕ
hp : p ≠ 0
φ : R⟦X⟧
⊢ ((expand p hp) φ).order = p • φ.order

Tactic:
expand,

Goal state after:
R : Type u_2
inst✝ : CommRing R
p : ℕ
hp : p ≠ 0
φ : R⟦X⟧
⊢ ((MvPowerSeries.expand p hp) φ).order = p • φ.order
Module: Mathlib.RingTheory.UniqueFactorizationDomain.Moebius

Goal state before:
pp: α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a b : α
h : Associated a b
⊢ moebius a = moebius b

Tactic:
by
  rw [moebius, moebius, h.squarefree_iff, h.card_factors_eq]

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

Goal state before:
pp: R Γ : Type
inst✝⁵ : Ring R
inst✝⁴ : DecidableEq R
inst✝³ : IsDomain R
inst✝² : LinearOrderedCommGroupWithZero Γ
inst✝¹ : ValuativeRel R
inst✝ : Valuation.Compatible 1
a b : (ValueGroupWithZero R)ˣ
this : (valuation R).IsEquiv 1
r s : ↥(posSubmonoid R)
hr : (valuation R) ↑r / (valuation R) ↑s = ↑a
t u : ↥(posSubmonoid R)
ht : (valuation R) ↑t / (valuation R) ↑u = ↑b
⊢ a = b

Tactic:
rw [Units.ext_iff, ← hr, ← ht, div_eq_div_iff, ← map_mul, ← map_mul, this.eq_iff] <;>
  simp [one_apply_posSubmonoid]

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

Goal state before:
pp: case refine_1
p : ℕ
hp : Fact (Nat.Prime p)
n x : ℕ
hx : x ∈ range n
⊢ (↑p ^ x).vars ⊆ univ ×ˢ range n

Tactic:
apply Subset.trans (vars_pow _ _)
    have : (p : 𝕄) = C (p : ℤ) := by simp only [Int.cast_natCast, eq_intCast]
    rw [this, vars_C]
    apply empty_subset

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

Goal state before:
pp: β : Type v
inst✝¹ : PartialOrder β
f : Cardinal.{v} → β
inst✝ : Small.{v, v} β
hf : Monotone f
⊢ EventuallyConst f atTop

Tactic:
refine .of_monotone_of_lt_cof hf ?_

Goal state after:
β : Type v
inst✝¹ : PartialOrder β
f : Cardinal.{v} → β
inst✝ : Small.{v, v} β
hf : Monotone f
⊢ lift.{v + 1, v} #β < lift.{v, v + 1} (cof Cardinal.{v})
Module: Mathlib.SetTheory.Cardinal.EventuallyConst

Goal state before:
pp: β : Type v
inst✝¹ : PartialOrder β
f : Ordinal.{v} → β
inst✝ : Small.{v, v} β
hf : Monotone f
⊢ EventuallyConst f atTop

Tactic:
refine .of_monotone_of_lt_cof hf ?_

Goal state after:
β : Type v
inst✝¹ : PartialOrder β
f : Ordinal.{v} → β
inst✝ : Small.{v, v} β
hf : Monotone f
⊢ Cardinal.lift.{v + 1, v} #β < Cardinal.lift.{v, v + 1} (cof Ordinal.{v})
Module: Mathlib.SetTheory.Lists

Goal state before:
pp: case C1.antisymm.antisymm.left
α : Type u_1
trans : Lists α → Prop := ⋯
l₁ : Lists' α true
IH : ∀ (l' : Lists α), l' ∈ l₁.toList → trans l'
l₂✝¹ : Lists' α true
l₂ : l₁.Subset l₂✝¹
a✝¹ : l₂✝¹.Subset l₁
h₁ : of' l₁ ~ ⟨true, l₂✝¹⟩
l₂✝ : Lists' α true
l₃ : l₂✝¹.Subset l₂✝
a✝ : l₂✝.Subset l₂✝¹
h₂ : ⟨true, l₂✝¹⟩ ~ ⟨true, l₂✝⟩
hl₁ : l₁ ⊆ l₂✝¹
hr₁ : l₂✝¹ ⊆ l₁
hl₂ : l₂✝¹ ⊆ l₂✝
hr₂ : l₂✝ ⊆ l₂✝¹
⊢ ∀ (a : Lists α), a ∈ l₁.toList → a ∈ l₂✝

Tactic:
intro a₁

Goal state after:
case C1.antisymm.antisymm.left
α : Type u_1
trans : Lists α → Prop := fun l₁ ↦ ∀ ⦃l₂ l₃ : Lists α⦄, l₁ ~ l₂ → l₂ ~ l₃ → l₁ ~ l₃
l₁ : Lists' α true
IH : ∀ (l' : Lists α), l' ∈ l₁.toList → trans l'
l₂✝¹ : Lists' α true
l₂ : l₁.Subset l₂✝¹
a✝¹ : l₂✝¹.Subset l₁
h₁ : of' l₁ ~ ⟨true, l₂✝¹⟩
l₂✝ : Lists' α true
l₃ : l₂✝¹.Subset l₂✝
a✝ : l₂✝.Subset l₂✝¹
h₂ : ⟨true, l₂✝¹⟩ ~ ⟨true, l₂✝⟩
hl₁ : l₁ ⊆ l₂✝¹
hr₁ : l₂✝¹ ⊆ l₁
hl₂ : l₂✝¹ ⊆ l₂✝
hr₂ : l₂✝ ⊆ l₂✝¹
a₁ : Lists α
⊢ a₁ ∈ l₁.toList → a₁ ∈ l₂✝
Module: Mathlib.Topology.Order.SuccPred

Goal state before:
pp: α : Type u_1
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
inst✝¹ : SuccOrder α
inst✝ : NoMaxOrder α
a : α
s : Set α
h : AccPt a (𝓟 s)
⊢ ¬IsMin a ∧ ∀ (b : α), ¬b ⋖ a

Tactic:
simp_rw [accPt_principal, Set.Nonempty] at h

Goal state after:
α : Type u_1
inst✝⁴ : LinearOrder α
inst✝³ : TopologicalSpace α
inst✝² : OrderTopology α
inst✝¹ : SuccOrder α
inst✝ : NoMaxOrder α
a : α
s : Set α
h : ¬IsMin a ∧ ∀ b < a, ∃ x, x ∈ s ∩ Ioo b a
⊢ ¬IsMin a ∧ ∀ (b : α), ¬b ⋖ a
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: case inr
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
nh : ↑n₂ ≤ ↑n₁ ∧ (if ↑n₂ < ↑n₁ then Ordering.gt else Ordering.eq) = Ordering.lt
⊢ (Ordering.eq.then (Ordering.lt.then (a₁.cmp a₂))).Compares (namedPattern o₁ (e₁.oadd n₁ a₁) h✝¹)
    (namedPattern o₂ (e₁.oadd n₂ a₂) h✝)

Tactic:
· rw [ite_eq_iff] at nh; rcases nh.right with nh | nh <;> cases nh <;> contradiction

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

Goal state before:
pp: case oadd
b : Ordinal.{0}
e : ONote
n : ℕ+
a o : ONote
h₁ : (e.oadd n a).NFBelow b
h₂ : o.NFBelow b
e' : ONote
n' : ℕ+
a' : ONote
h' : (e'.oadd n' a').NFBelow b
this : (e.cmp e').Compares e e'
⊢ (e.addAux n (e'.oadd n' a')).NFBelow b

Tactic:
cases h : cmp e e' <;> dsimp [addAux] <;> simp only [h]

Goal state after:
case oadd.lt
b : Ordinal.{0}
e : ONote
n : ℕ+
a o : ONote
h₁ : (e.oadd n a).NFBelow b
h₂ : o.NFBelow b
e' : ONote
n' : ℕ+
a' : ONote
h' : (e'.oadd n' a').NFBelow b
this : (e.cmp e').Compares e e'
h : e.cmp e' = Ordering.lt
⊢ (e'.oadd n' a').NFBelow b

case oadd.eq
b : Ordinal.{0}
e : ONote
n : ℕ+
a o : ONote
h₁ : (e.oadd n a).NFBelow b
h₂ : o.NFBelow b
e' : ONote
n' : ℕ+
a' : ONote
h' : (e'.oadd n' a').NFBelow b
this : (e.cmp e').Compares e e'
h : e.cmp e' = Ordering.eq
⊢ (e.oadd (n + n') a').NFBelow b

case oadd.gt
b : Ordinal.{0}
e : ONote
n : ℕ+
a o : ONote
h₁ : (e.oadd n a).NFBelow b
h₂ : o.NFBelow b
e' : ONote
n' : ℕ+
a' : ONote
h' : (e'.oadd n' a').NFBelow b
this : (e.cmp e').Compares e e'
h : e.cmp e' = Ordering.gt
⊢ (e.oadd n (e'.oadd n' a')).NFBelow b
Module: Mathlib.SetTheory.ZFC.Basic

Goal state before:
pp: x✝ y z x : ZFSet.{u}
⊢ Function.LeftInverse (fun s ↦ ⟨ZFSet.sep (fun x_1 ↦ x_1 ∈ ↑s) x, ⋯⟩) fun y ↦ ⟨↑↑y, ⋯⟩

Tactic:
simp +contextual [Function.LeftInverse]

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

Goal state before:
pp: α✝¹ : Type u_1
A✝¹ : α✝¹ → PSet.{u_1}
α✝ : Type u_1
A✝ : α✝ → PSet.{u_1}
αβ : ∀ (a : α✝¹), ∃ b, (A✝¹ a).Equiv (A✝ b)
βα : ∀ (b : α✝), ∃ a, (A✝¹ a).Equiv (A✝ b)
⊢ (mk α✝¹ A✝¹).rank = (mk α✝ A✝).rank

Tactic:
apply congr_arg sSup
    ext
    constructor <;> simp only [Set.mem_range, forall_exists_index] <;> intro a h
    · obtain ⟨b, h'⟩ := αβ a
      exists b
      rw [← h, rank_congr h']
    · obtain ⟨b, h'⟩ := βα a
      exists b
      rw [← h, rank_congr h']

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

Goal state before:
pp: o : Ordinal.{u_1}
x : PSet.{u_1}
⊢ o < x.rank ↔ ∃ y ∈ x, o ≤ y.rank

Tactic:
contrapose!; exact rank_le_iff

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

Goal state before:
pp: x : ZFSet.{u}
o : Ordinal.{u}
⊢ o < x.rank ↔ ∃ y ∈ x, o ≤ y.rank

Tactic:
contrapose!; exact rank_le_iff

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

Goal state before:
pp: x : ZFSet.{u}
h : ∅ ∉ x
y : ZFSet.{u}
yx : y ∈ x
⊢ ↑(map (fun y ↦ Classical.epsilon fun z ↦ z ∈ y) x) ′ ↑y ∈ ↑y

Tactic:
@map_fval _ (Classical.allZFSetDefinable _) x y yx,

Goal state after:
x : ZFSet.{u}
h : ∅ ∉ x
y : ZFSet.{u}
yx : y ∈ x
⊢ ↑(Classical.epsilon fun z ↦ z ∈ y) ∈ ↑y
Module: Mathlib.SetTheory.ZFC.Class

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

Tactic:
refine ⟨fun y hy z hz ↦ ?_, fun hyz hzw hwx ↦ ?_⟩

Goal state after:
case refine_1
x : ZFSet.{u}
hx : ↑x = IsOrdinal
y : ZFSet.{u}
hy : y ∈ x
z : ZFSet.{u}
hz : z ∈ y
⊢ z ∈ x

case refine_2
x : ZFSet.{u}
hx : ↑x = IsOrdinal
y✝ z✝ w✝ : ZFSet.{u}
hyz : y✝ ∈ z✝
hzw : z✝ ∈ w✝
hwx : w✝ ∈ x
⊢ y✝ ∈ w✝
Module: Mathlib.SetTheory.ZFC.Rank

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

Tactic:
induction x using inductionOn with

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 = IsWellFounded.rank (fun x1 x2 ↦ x1 ∈ x2) x
Module: Mathlib.SetTheory.ZFC.VonNeumann

Goal state before:
pp: case mp
o : Ordinal.{u_1}
x : ZFSet.{u_1}
hx : x ⊆ V_ o
y : ZFSet.{u_1}
hy : y ∈ x
⊢ y.rank < o

pp: case mpr
o : Ordinal.{u_1}
x : ZFSet.{u_1}
hx : ∀ ⦃y : ZFSet.{u_1}⦄, y ∈ x → y.rank < o
y : ZFSet.{u_1}
hy : y ∈ x
⊢ y ∈ V_ o

Tactic:
· apply (rank_lt_of_mem (hx hy)).trans_le
    simp_rw [rank_le_iff, mem_vonNeumann']
    rintro z ⟨a, ha, hz⟩
    exact (subset_vonNeumann.1 hz).trans_lt ha

Goal state after:
case mpr
o : Ordinal.{u_1}
x : ZFSet.{u_1}
hx : ∀ ⦃y : ZFSet.{u_1}⦄, y ∈ x → y.rank < o
y : ZFSet.{u_1}
hy : y ∈ x
⊢ y ∈ V_ o
Module: Mathlib.SetTheory.ZFC.VonNeumann

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

Tactic:
simp [subset_vonNeumann]

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

Goal state before:
pp: x y : ZFSet.{u_1}
hx : x.IsOrdinal
hy : y.IsOrdinal
⊢ x.rank ≤ y.rank ↔ x ⊆ y

Tactic:
by
  rw [← notMem_iff_subset hy hx, ← rank_lt_iff_mem hy hx, not_lt]

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

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

Tactic:
simp [subset_vonNeumann]

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

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

Tactic:
simp [subset_vonNeumann]

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

Goal state before:
pp: x✝¹ x✝ : Ordinal.{u_1}
h : x✝¹ < x✝
⊢ x✝¹.toZFSet ⊂ x✝.toZFSet

Tactic:
ssubset_iff_subset_not_subset

Goal state after:
x✝¹ x✝ : Ordinal.{u_1}
h : x✝¹ < x✝
⊢ x✝¹.toZFSet ⊆ x✝.toZFSet ∧ ¬x✝.toZFSet ⊆ x✝¹.toZFSet
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs

Goal state before:
pp: basis_hd : ℝ → ℝ
basis_tl : Basis
s : Stream'.Seq (ℝ × MultiseriesExpansion basis_tl)
⊢ s.destruct =
    Option.map
      ((fun x ↦ ((x.1, x.2.1), x.2.2)) ∘ fun x ↦
        match x with
        | ((exp, coef), tl) => (exp, coef, tl))
      s.destruct

Tactic:
exact Option.map_id_apply.symm

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

Goal state before:
pp: basis : Basis
n : ℕ
h : n < List.length basis
n' : Fin (List.length basis) := ⟨n, h⟩
| (monomial basis n).toFun

Tactic:
show n = n'.val by simp [n']

Goal state after:
basis : Basis
n : ℕ
h : n < List.length basis
n' : Fin (List.length basis) := ⟨n, h⟩
| (monomial basis ↑n').toFun
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Predicates

Goal state before:
pp: hd : ℝ
tl : UnitMonomial
⊢ FirstNonzeroIsNeg (hd :: tl) ↔ hd < 0 ∨ hd = 0 ∧ tl.FirstNonzeroIsNeg

Tactic:
grind [FirstNonzeroIsNeg, sign]

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

Goal state before:
pp: o a : Ordinal.{u_1}
h : a < o * ω
⊢ ∃ i, a < o * ↑i + o

Tactic:
obtain ⟨i, hi, h'⟩ := (lt_mul_iff_of_isSuccLimit isSuccLimit_omega0).1 h

Goal state after:
o a : Ordinal.{u_1}
h : a < o * ω
i : Ordinal.{u_1}
hi : i < ω
h' : a < o * i
⊢ ∃ i, a < o * ↑i + o