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

Goal state before:
pp: case refine_1
p : ℕ
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Fact (Nat.Prime p)
f : R →+* S
x : 𝕎 R
h : (map f) x = 0
n : ℕ
⊢ f (x.coeff n) = 0

Tactic:
apply_fun (·.coeff n) at h
    simpa using h

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

Goal state before:
pp: p n : ℕ
⊢ frobeniusPolyAux p n =
    X (n + 1) -
      ∑ 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)))

Tactic:
rw [frobeniusPolyAux, ← Fin.sum_univ_eq_sum_range]

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ (MvPolynomial.map (Int.castRingHom ℚ)) (frobeniusPoly p n) = frobeniusPolyRat p n

Tactic:
rw [frobeniusPoly, map_add, map_mul, map_pow, map_C, map_X, eq_intCast, Int.cast_natCast,
    frobeniusPolyRat]

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ X n ^ p + C ↑p * (MvPolynomial.map (Int.castRingHom ℚ)) (frobeniusPolyAux p n) =
    (bind₁ (wittPolynomial p ℚ ∘ fun n ↦ n + 1)) (xInTermsOfW p ℚ n)
Module: Mathlib.RingTheory.Perfection

Goal state before:
pp: 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 : ℕ
hp : Fact (Nat.Prime p)
r : O
hx : v ↑p ^ (1 / ↑p) < v ((algebraMap O K) r) ^ 1
s : O
hy : v ↑p ^ (1 / ↑p) < v ((algebraMap O K) s) ^ 1
h1p : 0 < 1 / ↑p
⊢ v ↑p < v ((algebraMap O K) (r * s))

Tactic:
rpow_one

Goal state after:
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 : ℕ
hp : Fact (Nat.Prime p)
r : O
hx : v ↑p ^ (1 / ↑p) < v ((algebraMap O K) r)
s : O
hy : v ↑p ^ (1 / ↑p) < v ((algebraMap O K) s)
h1p : 0 < 1 / ↑p
⊢ v ↑p < v ((algebraMap O K) (r * s))
Module: Mathlib.RingTheory.WittVector.Domain

Goal state before:
pp: case h
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
x : 𝕎 R
hx : x ≠ 0
hex : ∃ k, x.coeff k ≠ 0
n : ℕ := ⋯
⊢ (x.shift n).coeff 0 ≠ 0 ∧ x = (⇑verschiebung)^[n] (x.shift n)

Tactic:
refine ⟨Nat.find_spec hex, eq_iterate_verschiebung fun i hi => not_not.mp ?_⟩

Goal state after:
case h
p : ℕ
R : Type u_1
hp : Fact (Nat.Prime p)
inst✝ : CommRing R
x : 𝕎 R
hx : x ≠ 0
hex : ∃ k, x.coeff k ≠ 0
n : ℕ := Nat.find hex
i : ℕ
hi : i < n
⊢ ¬¬x.coeff i = 0
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
x : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
⊢ (∀ i < m, x.coeff i = 0) → ∀ i < n, x.coeff i = 0

Tactic:
intro h i hi

Goal state after:
p n : ℕ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : Fact (Nat.Prime p)
m : ℕ
hm : n ≤ m
x : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
h : ∀ i < m, x.coeff i = 0
i : ℕ
hi : i < n
⊢ x.coeff i = 0
Module: Mathlib.RingTheory.Polynomial.Hermite.Basic

Goal state before:
pp: case zero
k : ℕ
hnk : Odd (0 + k)
⊢ (hermite 0).coeff k = 0

Tactic:
zero_add k

Goal state after:
case zero
k : ℕ
hnk : Odd k
⊢ (hermite 0).coeff k = 0
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) =
    (-1) ^ (n + 1) * ↑(2 * (n + 1) - 1)‼ * ↑((2 * (n + 1) + (k + 1)).choose (k + 1))

Tactic:
change _ = hermite_explicit _ _

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.Opposites

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
h : IsLeftCancelMulZero R[X]
a b c : R
eq : (fun x ↦ a + x) b = (fun x ↦ a + x) c
a✝ : Nontrivial R
trinomial : R → R[X] := fun r ↦ a • X ^ 2 + r • X + C a
ht : ∀ (r : R), (X + C 1) * trinomial r = a • X ^ 3 + (a + r) • X ^ 2 + (a + r) • X + C a
⊢ a • X ^ 3 + (a + b) • X ^ 2 + (a + b) • X + C a = a • X ^ 3 + (a + c) • X ^ 2 + (a + c) • X + C a

Tactic:
eq

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

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
⊢ (IsLeftCancelMulZero R ∧ IsCancelAdd R) ∧ IsRightCancelMulZero R ∧ IsCancelAdd R ↔
    (IsLeftCancelMulZero R ∧ IsRightCancelMulZero R) ∧ IsCancelAdd R

Tactic:
rw [and_and_and_comm, and_self]

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

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
a b c x1 x2 : R
ha : a ≠ 0
hvieta : b = -a * (x1 + x2) ∧ c = a * x1 * x2
⊢ C a * X ^ 2 + C b * X + C c = C a * (X - C x1) * (X - C x2)

Tactic:
simp [hvieta.1, hvieta.2]

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
a b c x1 x2 : R
ha : a ≠ 0
hvieta : b = -a * (x1 + x2) ∧ c = a * x1 * x2
⊢ C a * X ^ 2 + -(C a * (C x1 + C x2) * X) + C a * C x1 * C x2 = C a * (X - C x1) * (X - C x2)
Module: Mathlib.RingTheory.Polynomial.ShiftedLegendre

Goal state before:
pp: n : ℕ
R : Type u_1
inst✝ : Ring R
x : R
⊢ (aeval x) (shiftedLegendre n) = (-1) ^ n * (aeval (1 - x)) (shiftedLegendre n)

Tactic:
have := congr(aeval x $(neg_one_pow_mul_shiftedLegendre_comp_one_sub_X_eq n))
  simpa [aeval_comp] using this.symm

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⟧
n : ℕ
inst✝ : I.IsTwoSided
hf : ∀ i ≤ n, (coeff i) f ∈ I
⊢ ∀ i ≤ n, (coeff i) (f * g) ∈ I

Tactic:
simpa only [Ideal.IsTwoSided.mul_one] using
    coeff_mul_mem_ideal_mul_ideal_of_coeff_mem_ideal (J := 1) (g := g) n hf (by simp)

Goal state after:
Module: Mathlib.RingTheory.TensorProduct.DirectLimitFG

Goal state before:
pp: R : Type u
M : Type u_1
N : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
P : Submodule R M
hP : P.FG
t t' : ↥P ⊗[R] N
h : (rTensor N P.subtype) t = (rTensor N P.subtype) t'
⊢ ∃ Q, ∃ (hPQ : P ≤ Q), Q.FG ∧ (rTensor N (inclusion hPQ)) t = (rTensor N (inclusion hPQ)) t'

Tactic:
simp only [← Submodule.FG.rTensor.directLimit_apply' R M N hP, EmbeddingLike.apply_eq_iff_eq] at h

Goal state after:
R : Type u
M : Type u_1
N : Type u_2
inst✝⁴ : CommSemiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
P : Submodule R M
hP : P.FG
t t' : ↥P ⊗[R] N
h :
  (Module.DirectLimit.of R { P // P.FG } (fun P ↦ ↥↑P ⊗[R] N) (fun ⦃x x_1⦄ h ↦ rTensor N (inclusion h)) ⟨P, hP⟩) t =
    (Module.DirectLimit.of R { P // P.FG } (fun P ↦ ↥↑P ⊗[R] N) (fun ⦃x x_1⦄ h ↦ rTensor N (inclusion h)) ⟨P, hP⟩) t'
⊢ ∃ Q, ∃ (hPQ : P ≤ Q), Q.FG ∧ (rTensor N (inclusion hPQ)) t = (rTensor N (inclusion hPQ)) t'
Module: Mathlib.RingTheory.Radical.NatInt

Goal state before:
pp: z : ℤ
⊢ 0 < ↑(radical z.natAbs)

Tactic:
natCast_pos

Goal state after:
z : ℤ
⊢ 0 < radical z.natAbs
Module: Mathlib.RingTheory.RegularLocalRing.Defs

Goal state before:
pp: case pos
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsLocalRing R
inst✝¹ : IsDomain R
inst✝ : IsPrincipalIdealRing R
isf : IsField R
⊢ IsRegularLocalRing R

Tactic:
let := isf.toField

Goal state after:
case pos
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsLocalRing R
inst✝¹ : IsDomain R
inst✝ : IsPrincipalIdealRing R
isf : IsField R
this : Field R := isf.toField
⊢ IsRegularLocalRing R
Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation

Goal state before:
pp: case inl
A : Type u_1
inst✝¹ : CommRing A
g✝ : A⟦X⟧
I✝ : Ideal A
g : A[X]
I : Ideal A
H : g.IsDistinguishedAt I
inst✝ : IsAdicComplete I A
f : A[X] ⧸ Ideal.span {g}
h✝ : Subsingleton A
this✝ : Subsingleton A[X]
this : Subsingleton (A[X] ⧸ Ideal.span {g})
⊢ (⇑(Ideal.Quotient.mk (Ideal.span {g})) ∘ ⇑⋯.mod')
      ((↑↑(Ideal.quotientMapₐ (Ideal.span {↑g}) (Polynomial.coeToPowerSeries.algHom A) ⋯).toRingHom).toFun f) =
    f

Tactic:
exact Subsingleton.elim _ _

Goal state after:
Module: Mathlib.RingTheory.Spectrum.Prime.Homeomorph

Goal state before:
pp: R : Type u_3
S : Type u_4
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
H : ∀ (x : S), ∃ n > 0, x ^ n ∈ f.range
hker : RingHom.ker f ≤ nilradical R
q q' : PrimeSpectrum S
hqq' : comap f q = comap f q'
x : S
⊢ x ∈ q.asIdeal ↔ x ∈ q'.asIdeal

Tactic:
obtain ⟨n, hn, y, hy⟩ := H x

Goal state after:
R : Type u_3
S : Type u_4
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
H : ∀ (x : S), ∃ n > 0, x ^ n ∈ f.range
hker : RingHom.ker f ≤ nilradical R
q q' : PrimeSpectrum S
hqq' : comap f q = comap f q'
x : S
n : ℕ
hn : n > 0
y : R
hy : f y = x ^ n
⊢ x ∈ q.asIdeal ↔ x ∈ q'.asIdeal
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
a b : 𝕎 k
hab : ↑p = a * b
⊢ a ≠ 0 ∧ b ≠ 0

Tactic:
by
    rw [← mul_ne_zero_iff]; intro h; rw [h] at hab; exact p_nonzero p k hab

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : CommRing k
inst✝ : CharP k p
n : ℕ
x y✝ : 𝕎 k
this : ↑p = 0
y : 𝕎 k
⊢ ∑ x ∈ range (n + 1 + 1), 0 ^ x * y.coeff x ^ p ^ (n + 1 - x) = y.coeff 0 ^ p ^ (n + 1)

Tactic:
Finset.sum_eq_single_of_mem 0

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : CommRing k
inst✝ : CharP k p
n : ℕ
x y✝ : 𝕎 k
this : ↑p = 0
y : 𝕎 k
⊢ 0 ^ 0 * y.coeff 0 ^ p ^ (n + 1 - 0) = y.coeff 0 ^ p ^ (n + 1)

case h
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : CommRing k
inst✝ : CharP k p
n : ℕ
x y✝ : 𝕎 k
this : ↑p = 0
y : 𝕎 k
⊢ 0 ∈ range (n + 1 + 1)

case h₀
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝¹ : CommRing k
inst✝ : CharP k p
n : ℕ
x y✝ : 𝕎 k
this : ↑p = 0
y : 𝕎 k
⊢ ∀ b ∈ range (n + 1 + 1), b ≠ 0 → 0 ^ b * y.coeff b ^ p ^ (n + 1 - b) = 0
Module: Mathlib.SetTheory.Cardinal.Cofinality.Club

Goal state before:
pp: case inr.inr
α : Type v
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
s : Set (Set α)
hα✝ : cof α ≠ ℵ₀
hsα : #↑s < cof α
hs : ∀ x ∈ s, IsClub x
h✝ : Nonempty α
hα : ℵ₀ < cof α
a : α
f : ↑s → α → α
hf : ∀ (x : ↑s) (x_1 : α), f x x_1 ∈ ↑x ∧ x_1 ≤ f x x_1
g : ℕ → α := fun t ↦ Nat.rec a (fun x IH ↦ sSup (range fun x ↦ f x IH)) t
hg : BddAbove (range g)
⊢ ∃ y ∈ ⋂₀ s, a ≤ y

Tactic:
refine ⟨_, fun t ht ↦ ?_, le_csSup hg ⟨0, rfl⟩⟩

Goal state after:
case inr.inr
α : Type v
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
s : Set (Set α)
hα✝ : cof α ≠ ℵ₀
hsα : #↑s < cof α
hs : ∀ x ∈ s, IsClub x
h✝ : Nonempty α
hα : ℵ₀ < cof α
a : α
f : ↑s → α → α
hf : ∀ (x : ↑s) (x_1 : α), f x x_1 ∈ ↑x ∧ x_1 ≤ f x x_1
g : ℕ → α := fun t ↦ Nat.rec a (fun x IH ↦ sSup (range fun x ↦ f x IH)) t
hg : BddAbove (range g)
t : Set α
ht : t ∈ s
⊢ sSup (range g) ∈ t
Module: Mathlib.SetTheory.Cardinal.EventuallyConst

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : PartialOrder β
f : α → β
hf : Monotone f
hα : lift.{u, v} #β < lift.{v, u} (cof α)
⊢ EventuallyConst f atTop

Tactic:
have : Nonempty α := by by_contra!; simp at hα
  refine .of_not_isCofinal_rangeSplitting hf ?_
  contrapose! hα
  classical let := hf.isChain_range.linearOrder
  rw [← lift_cof_congr_of_strictMono (rangeSplitting_strictMono hf) hα, lift_le]
  exact (cof_le_cardinalMk _).trans (mk_set_le _)

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

Goal state before:
pp: b o : Ordinal.{u_1}
hb : b ≤ 1
ho : o ≠ 0
⊢ CNF b o = [(0, o)]

Tactic:
by
  rcases Order.le_one_iff.1 hb with (rfl | rfl)
  exacts [CNF.zero_left ho, CNF.one_left ho]

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

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

pp: case refine_2.inr
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
h✝ : x ∈ (log b o, o / b ^ log b o) :: CNF b (o % b ^ log b o)
h : x ∈ CNF b (o % b ^ log b o)
⊢ x.2 < b

Tactic:
· exact div_opow_log_lt o hb

Goal state after:
case refine_2.inr
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
h✝ : x ∈ (log b o, o / b ^ log b o) :: CNF b (o % b ^ log b o)
h : x ∈ CNF b (o % b ^ log b o)
⊢ x.2 < b
Module: Mathlib.SetTheory.Ordinal.FixedPointApproximants

Goal state before:
pp: case refine_1
α : Type u
inst✝ : CompleteLattice α
f : α →o α
x : α
hx : x ≤ f x
h : lfpApprox f x 1 = x
⊢ f x = x

Tactic:
← zero_add 1,

Goal state after:
case refine_1
α : Type u
inst✝ : CompleteLattice α
f : α →o α
x : α
hx : x ≤ f x
h : lfpApprox f x (0 + 1) = x
⊢ f x = x
Module: Mathlib.SetTheory.Ordinal.CantorNormalForm

Goal state before:
pp: case zero
b e : Ordinal.{u_1}
hb : ∀ (e' : Ordinal.{u_1}), 0 e' < b
he : ∀ e' ∈ support 0, e' < e
⊢ eval b 0 < b ^ e

Tactic:
rw [eval_zero_right]

Goal state after:
case zero
b e : Ordinal.{u_1}
hb : ∀ (e' : Ordinal.{u_1}), 0 e' < b
he : ∀ e' ∈ support 0, e' < e
⊢ 0 < b ^ e
Module: Mathlib.SetTheory.ZFC.Rank

Goal state before:
pp: case mp
α✝¹ : 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)
x✝ : Ordinal.{u_1}
⊢ (x✝ ∈ Set.range fun a ↦ succ (A✝¹ a).rank) → x✝ ∈ Set.range fun a ↦ succ (A✝ a).rank

Tactic:
simp only [Set.mem_range, forall_exists_index]

Goal state after:
case mp
α✝¹ : 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)
x✝ : Ordinal.{u_1}
⊢ ∀ (x : α✝¹), succ (A✝¹ x).rank = x✝ → ∃ y, succ (A✝ y).rank = x✝
Module: Mathlib.SetTheory.ZFC.Rank

Goal state before:
pp: case mpr
α✝¹ : 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)
x✝ : Ordinal.{u_1}
⊢ (x✝ ∈ Set.range fun a ↦ succ (A✝ a).rank) → x✝ ∈ Set.range fun a ↦ succ (A✝¹ a).rank

Tactic:
simp only [Set.mem_range, forall_exists_index]

Goal state after:
case mpr
α✝¹ : 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)
x✝ : Ordinal.{u_1}
⊢ ∀ (x : α✝), succ (A✝ x).rank = x✝ → ∃ y, succ (A✝¹ y).rank = x✝
Module: Mathlib.SetTheory.Ordinal.Veblen

Goal state before:
pp: o : Ordinal.{u}
h : o.invVeblen₁ = o
ho : ¬o = 0
| ω ^ o

Tactic:
← veblen_invVeblen₁_invVeblen₂,

Goal state after:
o : Ordinal.{u}
h : o.invVeblen₁ = o
ho : ¬o = 0
| veblen o.invVeblen₁ o.invVeblen₂
Module: Mathlib.SetTheory.Ordinal.Veblen

Goal state before:
pp: o : Ordinal.{u}
⊢ ¬o.invVeblen₁ = o ↔ o ≠ 0 ∧ o ∉ range Γ_

Tactic:
invVeblen₁_eq_iff,

Goal state after:
o : Ordinal.{u}
⊢ ¬(o = 0 ∨ o ∈ range Γ_ ) ↔ o ≠ 0 ∧ o ∉ range Γ_
Module: Mathlib.SetTheory.ZFC.Ordinal

Goal state before:
pp: x y : ZFSet.{u}
hx : x.IsTransitive
hy : y.IsTransitive
y✝ : ZFSet.{u}
⊢ y✝ = x ∨ y✝ = y → y✝.IsTransitive

Tactic:
rintro (rfl | rfl)

Goal state after:
case inl
y : ZFSet.{u}
hy : y.IsTransitive
y✝ : ZFSet.{u}
hx : y✝.IsTransitive
⊢ y✝.IsTransitive

case inr
x : ZFSet.{u}
hx : x.IsTransitive
y✝ : ZFSet.{u}
hy : y✝.IsTransitive
⊢ y✝.IsTransitive
Module: Mathlib.SetTheory.ZFC.Ordinal

Goal state before:
pp: x : ZFSet.{u}
⊢ x.IsTransitive ∧ IsTrans (↥x) (Subrel (fun x1 x2 ↦ x1 ∈ x2) fun x_1 ↦ x_1 ∈ x) → x.IsOrdinal

Tactic:
rintro ⟨h₁, ⟨h₂⟩⟩

Goal state after:
x : ZFSet.{u}
h₁ : x.IsTransitive
h₂ :
  ∀ (a b c : ↥x),
    Subrel (fun x1 x2 ↦ x1 ∈ x2) (fun x_1 ↦ x_1 ∈ x) a b →
      Subrel (fun x1 x2 ↦ x1 ∈ x2) (fun x_1 ↦ x_1 ∈ x) b c → Subrel (fun x1 x2 ↦ x1 ∈ x2) (fun x_1 ↦ x_1 ∈ x) a c
⊢ x.IsOrdinal
Module: Mathlib.SetTheory.ZFC.Class

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

Tactic:
by
    apply Class.mem_irrefl x
    rwa [Class.coe_mem, hx]

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

Goal state before:
pp: case a
o : Ordinal.{u_1}
a✝ : PSet.{u_1}
x✝ : Ordinal.{u_1}
⊢ a✝.Equiv x✝.toPSet ↔ x✝.toPSet.Equiv a✝

Tactic:
PSet.Equiv.comm

Goal state after:
case a
o : Ordinal.{u_1}
a✝ : PSet.{u_1}
x✝ : Ordinal.{u_1}
⊢ x✝.toPSet.Equiv a✝ ↔ x✝.toPSet.Equiv a✝
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: case pos
e : ONote
n : ℕ+
a o' : ONote
m : ℕ
h : (e.oadd n a).NF
e0 : e = 0
p : 0 = o' ∧ ↑n = m
⊢ o'.NF ∧ ↑↑n + a.repr = ω * o'.repr + ↑m

pp: case neg
e : ONote
n : ℕ+
a o' : ONote
m : ℕ
h : (e.oadd n a).NF
e0 : ¬e = 0
p : (e - 1).oadd n a.split'.1 = o' ∧ a.split'.2 = m
⊢ o'.NF ∧ ω ^ e.repr * ↑↑n + a.repr = ω * o'.repr + ↑m

Tactic:
· rcases p with ⟨rfl, rfl⟩
      simp [h.zero_of_zero e0, NF.zero]

Goal state after:
case neg
e : ONote
n : ℕ+
a o' : ONote
m : ℕ
h : (e.oadd n a).NF
e0 : ¬e = 0
p : (e - 1).oadd n a.split'.1 = o' ∧ a.split'.2 = m
⊢ o'.NF ∧ ω ^ e.repr * ↑↑n + a.repr = ω * o'.repr + ↑m
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: o o' : ONote
m : ℕ
inst✝ : o.NF
h : o.split = (o', m)
⊢ o'.NF ∧ o.repr = o'.repr + ↑m

Tactic:
rcases e : split' o with ⟨a, n⟩

Goal state after:
o o' : ONote
m : ℕ
inst✝ : o.NF
h : o.split = (o', m)
a : ONote
n : ℕ
e : o.split' = (a, n)
⊢ o'.NF ∧ o.repr = o'.repr + ↑m
Module: Mathlib.SetTheory.Ordinal.Notation

Goal state before:
pp: o o' : ONote
m : ℕ
inst✝ : o.NF
h : o.split = (o', m)
⊢ ω ∣ o'.repr

Tactic:
rcases e : split' o with ⟨a, n⟩

Goal state after:
o o' : ONote
m : ℕ
inst✝ : o.NF
h : o.split = (o', m)
a : ONote
n : ℕ
e : o.split' = (a, n)
⊢ ω ∣ o'.repr
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Majorized

Goal state before:
pp: f : ℝ → ℝ
exp : ℝ
h : Tendsto f atTop atTop
exp' : ℝ
h_exp : exp' > exp
t : ℝ
h1 : 0 < f t
h2 : (f ^ exp') t = 0
⊢ (f ^ exp) t = 0

Tactic:
absurd h2

Goal state after:
f : ℝ → ℝ
exp : ℝ
h : Tendsto f atTop atTop
exp' : ℝ
h_exp : exp' > exp
t : ℝ
h1 : 0 < f t
h2 : (f ^ exp') t = 0
⊢ ¬(f ^ exp') t = 0
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
F : β → Option (α × γ × β)
op : γ → Stream'.Seq α → Stream'.Seq α
h : FriendlyOperationClass op
T : (β →ᵤ Stream'.Seq α) → β →ᵤ Stream'.Seq α :=
  fun f b ↦
    match F b with
    | none => nil
    | some (a, c, b') => Seq.cons a (op c (f b'))
f g : β →ᵤ Stream'.Seq α
b : β
a : α
c : γ
b' : β
⊢ dist (op c (f b')) (op c (g b')) ≤ dist (f b') (g b')

Tactic:
have := h.friend c

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
F : β → Option (α × γ × β)
op : γ → Stream'.Seq α → Stream'.Seq α
h : FriendlyOperationClass op
T : (β →ᵤ Stream'.Seq α) → β →ᵤ Stream'.Seq α :=
  fun f b ↦
    match F b with
    | none => nil
    | some (a, c, b') => Seq.cons a (op c (f b'))
f g : β →ᵤ Stream'.Seq α
b : β
a : α
c : γ
b' : β
this : FriendlyOperation (op c)
⊢ dist (op c (f b')) (op c (g b')) ≤ dist (f b') (g b')
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs

Goal state before:
pp: basis_hd : ℝ → ℝ
basis_tl : Basis
ms : Multiseries basis_hd basis_tl
h : ms.destruct = none
⊢ ms = nil

Tactic:
by
  apply Stream'.Seq.destruct_eq_none
  simpa [destruct] using h

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

Goal state before:
pp: basis_hd : ℝ → ℝ
basis_tl : List (ℝ → ℝ)
h_basis : WellFormedBasis (basis_hd :: basis_tl)
exp1 : ℝ
m1 : List ℝ
exp2 : ℝ
m2 : List ℝ
h : exp1 < exp2
h1 : m1.length = basis_tl.length
h2 : m2.length = basis_tl.length
⊢ m2.length = List.length (inv m1)

Tactic:
grind [inv_length]

Goal state after:
Module: Mathlib.Tactic.NormNum.IsSquare

Goal state before:
pp: a : ℚ
n d : ℕ
hn : n ≠ 0
hd : d ≠ 0
ha : IsRat a (Int.negOfNat n) d
q : ℚ
hq : -(↑n / ↑d) = q * q
⊢ -(↑n / ↑d) < 0

Tactic:
Left.neg_neg_iff

Goal state after:
a : ℚ
n d : ℕ
hn : n ≠ 0
hd : d ≠ 0
ha : IsRat a (Int.negOfNat n) d
q : ℚ
hq : -(↑n / ↑d) = q * q
⊢ 0 < ↑n / ↑d
Module: Mathlib.Tactic.ReduceModChar

Goal state before:
pp: α : Type u_1
inst✝ : Semiring α
a✝ : α
a b n : ℕ
x✝ : CharP α ↑n
h : a✝ = ↑a
⊢ a✝ ^ ↑b = ↑((a.pow b).mod n)

Tactic:
by
    rw [h, Nat.cast_id, Nat.pow_eq, ← Nat.cast_pow, CharP.natCast_eq_natCast_mod α n]
    rfl

Goal state after:
Module: Mathlib.Topology.UniformSpace.Ascoli

Goal state before:
pp: ι : Type u_1
X : Type u_2
α : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : UniformSpace α
F : ι → X → α
inst✝ : CompactSpace X
F_eqcont : Equicontinuous F
U : Set (α × α)
hU : U ∈ 𝓤 α
V : Set (α × α)
hV : V ∈ 𝓤 α
Vsymm : SetRel.IsSymm V
hVU : (SetRel.comp V V).comp V ⊆ U
Ω : X → Set X := fun x ↦ {y | ∀ (i : ι), (F i x, F i y) ∈ V}
A : Finset X
Acover : ⋃ x ∈ A, Ω x = ⊤
i j : ι
hij : (i, j) ∈ ⋂ a ∈ A, {ij | (F ij.1 a, F ij.2 a) ∈ V}
x : X
⊢ (UniformFun.toFun (Prod.map F F (i, j)).1 x, UniformFun.toFun (Prod.map F F (i, j)).2 x) ∈ U

Tactic:
mem_iInter₂

Goal state after:
ι : Type u_1
X : Type u_2
α : Type u_3
inst✝² : TopologicalSpace X
inst✝¹ : UniformSpace α
F : ι → X → α
inst✝ : CompactSpace X
F_eqcont : Equicontinuous F
U : Set (α × α)
hU : U ∈ 𝓤 α
V : Set (α × α)
hV : V ∈ 𝓤 α
Vsymm : SetRel.IsSymm V
hVU : (SetRel.comp V V).comp V ⊆ U
Ω : X → Set X := fun x ↦ {y | ∀ (i : ι), (F i x, F i y) ∈ V}
A : Finset X
Acover : ⋃ x ∈ A, Ω x = ⊤
i j : ι
hij : ∀ i_1 ∈ A, (i, j) ∈ {ij | (F ij.1 i_1, F ij.2 i_1) ∈ V}
x : X
⊢ (UniformFun.toFun (Prod.map F F (i, j)).1 x, UniformFun.toFun (Prod.map F F (i, j)).2 x) ∈ U
Module: Mathlib.Topology.UniformSpace.Ascoli

Goal state before:
pp: ι : Type u_1
X : Type u_2
α : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : UniformSpace α
F : ι → X → α
𝔖 : Set (Set X)
𝔖_compact : ∀ K ∈ 𝔖, IsCompact K
F_eqcont : ∀ K ∈ 𝔖, EquicontinuousOn F K
H1 :
  UniformSpace.comap F (UniformOnFun.uniformSpace X α 𝔖) =
    ⨅ K ∈ 𝔖, UniformSpace.comap (K.domRestrict ∘ F) (UniformFun.uniformSpace (↑K) α)
⊢ UniformSpace.comap ((⋃₀ 𝔖).domRestrict ∘ F) (Pi.uniformSpace fun i ↦ α) =
    ⨅ K ∈ 𝔖, UniformSpace.comap (K.domRestrict ∘ F) (Pi.uniformSpace fun i ↦ α)

Tactic:
simp_rw [UniformSpace.comap_comap, Pi.uniformSpace_comap_restrict_sUnion (fun _ ↦ α) 𝔖,
      UniformSpace.comap_iInf]

Goal state after:
Module: Mathlib.Topology.Algebra.Group.OpenMapping

Goal state before:
pp: G : Type u_1
X : Type u_2
inst✝⁹ : TopologicalSpace G
inst✝⁸ : TopologicalSpace X
inst✝⁷ : Group G
inst✝⁶ : IsTopologicalGroup G
inst✝⁵ : MulAction G X
inst✝⁴ : SigmaCompactSpace G
inst✝³ : BaireSpace X
inst✝² : T2Space X
inst✝¹ : ContinuousSMul G X
inst✝ : IsPretransitive G X
x : X
⊢ IsOpenMap fun g ↦ g • x

Tactic:
isOpenMap_iff_nhds_le,

Goal state after:
G : Type u_1
X : Type u_2
inst✝⁹ : TopologicalSpace G
inst✝⁸ : TopologicalSpace X
inst✝⁷ : Group G
inst✝⁶ : IsTopologicalGroup G
inst✝⁵ : MulAction G X
inst✝⁴ : SigmaCompactSpace G
inst✝³ : BaireSpace X
inst✝² : T2Space X
inst✝¹ : ContinuousSMul G X
inst✝ : IsPretransitive G X
x : X
⊢ ∀ (x_1 : G), 𝓝 (x_1 • x) ≤ Filter.map (fun g ↦ g • x) (𝓝 x_1)
Module: Mathlib.Topology.Algebra.Group.SubmonoidClosure

Goal state before:
pp: G : Type u_1
inst✝³ : Group G
inst✝² : TopologicalSpace G
inst✝¹ : CompactSpace G
inst✝ : IsTopologicalGroup G
x : G
⊢ closure[inst✝²] (range fun x_1 ↦ x ^ x_1) = closure[inst✝²] (range fun x_1 ↦ x ^ x_1)

Tactic:
ext y
  exact (mapClusterPt_atTop_pow_tfae y x).out 3 2

Goal state after:
Module: Mathlib.Topology.DerivedSet

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
A : Set X
h : derivedSet A ⊆ A
a : X
ha : ClusterPt a (𝓟 (A \ {a}))
nh : a ∉ A
this : A = A \ {a}
⊢ False

Tactic:
← accPt_principal_iff_clusterPt

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
A : Set X
h : derivedSet A ⊆ A
a : X
ha : AccPt a (𝓟 A)
nh : a ∉ A
this : A = A \ {a}
⊢ False