mathlib-initiative/mathlib-tactics huggingface dataset:
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 : (Ideal.Quotient.mk (Ideal.span {↑p})) r ^ p ≠ 0
s : O
hy : (Ideal.Quotient.mk (Ideal.span {↑p})) s ^ p ≠ 0
h1p : 0 < 1 / ↑p
⊢ (Ideal.Quotient.mk (Ideal.span {↑p})) r * (Ideal.Quotient.mk (Ideal.span {↑p})) s ≠ 0

Tactic:
rw [← (Ideal.Quotient.mk (Ideal.span {(p : O)})).map_mul]

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 : (Ideal.Quotient.mk (Ideal.span {↑p})) r ^ p ≠ 0
s : O
hy : (Ideal.Quotient.mk (Ideal.span {↑p})) s ^ p ≠ 0
h1p : 0 < 1 / ↑p
⊢ (Ideal.Quotient.mk (Ideal.span {↑p})) (r * s) ≠ 0
Module: Mathlib.RingTheory.WittVector.TeichmullerSeries

Goal state before:
pp: case inr
p : ℕ
hp : Fact (Nat.Prime p)
R : Type u_1
inst✝¹ : CommRing R
inst✝ : CharP R p
x : R
m n : ℕ
h✝ : m ≠ n
h : n < m
⊢ ((teichmuller p) x * ↑p ^ n).coeff m = 0

Tactic:
| inr h =>

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

Goal state before:
pp: ⊢ hermite 1 = X

Tactic:
rw [hermite_succ, hermite_zero]
  simp only [map_one, mul_one, derivative_one, sub_zero]

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

Goal state before:
pp: case succ
n : ℕ
ih : ∀ (k : ℕ), (hermite n).coeff (n + k + 1) = 0
k : ℕ
this : n + k + 1 + 2 = n + (k + 2) + 1
⊢ (hermite n).coeff (n + 1 + k) - (↑(n + 1 + k) + 2) * (hermite n).coeff (n + 1 + k + 2) = 0

Tactic:
add_right_comm,

Goal state after:
case succ
n : ℕ
ih : ∀ (k : ℕ), (hermite n).coeff (n + k + 1) = 0
k : ℕ
this : n + k + 1 + 2 = n + (k + 2) + 1
⊢ (hermite n).coeff (n + k + 1) - (↑(n + k + 1) + 2) * (hermite n).coeff (n + k + 1 + 2) = 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 + k + 2)
⊢ Odd (n + k)

Tactic:
exact (Nat.odd_add.mp hnk).mpr even_two

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

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

Tactic:
C_comp,

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

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

Tactic:
exact sum_add_index _ _ _ (fun _ => zero_smul ..) (fun _ _ _ => add_smul ..)

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

Goal state before:
pp: case neg
n : ℕ
hn1 : n ≠ 1
hn0 : ¬n = 0
hn : 1 < n
hp : X ^ n - X - 1 = trinomial 0 1 n (-1) (-1) 1
⊢ Irreducible (X ^ n - X - 1)

Tactic:
rw [hp]

Goal state after:
case neg
n : ℕ
hn1 : n ≠ 1
hn0 : ¬n = 0
hn : 1 < n
hp : X ^ n - X - 1 = trinomial 0 1 n (-1) (-1) 1
⊢ Irreducible (trinomial 0 1 n (-1) (-1) 1)
Module: Mathlib.RingTheory.PowerSeries.WeierstrassPreparation

Goal state before:
pp: A : Type u_1
inst✝¹ : CommRing A
g : A⟦X⟧
I : Ideal A
H : g.IsWeierstrassDivisorAt I
a : A
f f' : A⟦X⟧
inst✝ : IsPrecomplete I A
i m n : ℕ
hn : m ≤ n
⊢ (coeff i) (H.seq f m) ≡ (coeff i) (H.seq f n) [SMOD I ^ m • ⊤]

Tactic:
by
      induction n, hn using Nat.le_induction with
      | base => rw [SModEq.def]
      | succ n hn ih =>
        refine ih.trans (SModEq.symm ?_)
        rw [SModEq.sub_mem, smul_eq_mul, Ideal.mul_top, ← map_sub]
        exact Ideal.pow_le_pow_right hn (H.coeff_seq_succ_sub_seq_mem f n i)

Goal state after:
Module: Mathlib.RingTheory.Regular.ProjectiveDimension

Goal state before:
pp: R : Type u
inst✝⁴ : CommRing R
inst✝³ : Small.{v, u} R
inst✝² : IsLocalRing R
inst✝¹ : IsNoetherianRing R
M : ModuleCat R
inst✝ : Module.Finite R ↑M
x : R
reg : IsSMulRegular (↑M) x
mem : x ∈ maximalIdeal R
h : Nontrivial ↑M
⊢ Nontrivial (QuotSMulTop x ↑M)

Tactic:
exact (nontrivial_quotSMulTop_of_mem_maximalIdeal M mem)

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

Goal state before:
pp: R : Type u
inst✝² : Ring R
inst✝¹ : IsSimpleRing R
inst✝ : IsArtinianRing R
⊢ ∃ n, ∃ (_ : NeZero n), ∃ D x, Nonempty (R ≃+* Matrix (Fin n) (Fin n) D)

Tactic:
have ⟨n, hn, I, _, ⟨e⟩⟩ := exists_ringEquiv_matrix_end_mulOpposite R

Goal state after:
R : Type u
inst✝² : Ring R
inst✝¹ : IsSimpleRing R
inst✝ : IsArtinianRing R
n : ℕ
hn : NeZero n
I : Ideal R
w✝ : IsSimpleModule R ↥I
e : R ≃+* Matrix (Fin n) (Fin n) (Module.End R ↥I)ᵐᵒᵖ
⊢ ∃ n, ∃ (_ : NeZero n), ∃ D x, Nonempty (R ≃+* Matrix (Fin n) (Fin n) D)
Module: Mathlib.RingTheory.Spectrum.Prime.IsOpenComapC

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
U : Set (PrimeSpectrum R[X])
s : Set R[X]
z : zeroLocus s = Uᶜ
⊢ IsOpen (PrimeSpectrum.comap C '' (zeroLocus s)ᶜ)

Tactic:
← iUnion_of_singleton_coe s,

Goal state after:
R : Type u_1
inst✝ : CommRing R
U : Set (PrimeSpectrum R[X])
s : Set R[X]
z : zeroLocus s = Uᶜ
⊢ IsOpen (PrimeSpectrum.comap C '' (zeroLocus (⋃ i, {↑i}))ᶜ)
Module: Mathlib.RingTheory.Valuation.ValuativeRel.Trivial

Goal state before:
pp: R✝ Γ : Type
inst✝⁶ : Ring R✝
inst✝⁵ : DecidableEq R✝
inst✝⁴ : IsDomain R✝
inst✝³ : LinearOrderedCommGroupWithZero Γ
R : Type
inst✝² : Semiring R
inst✝¹ : DecidableEq R
inst✝ : IsDomain R
x✝² y✝ : R
x✝¹ : if y✝ = 0 then x✝² = 0 else True
x✝ : R
⊢ if y✝ * x✝ = 0 then x✝² * x✝ = 0 else True

Tactic:
split_ifs at * <;> simp_all

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ Fintype.card (ZMod p) ^ n = p ^ n

Tactic:
ZMod.card

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ p ^ n = p ^ n
Module: Mathlib.RingTheory.WittVector.FrobeniusFractionField

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : Field k
inst✝¹ : CharP k p
inst✝ : IsAlgClosed k
n : ℕ
a₁ a₂ : 𝕎 k
bs : Fin (n + 1) → k
ha₁ : a₁.coeff 0 ≠ 0
ha₂ : a₂.coeff 0 ≠ 0
⊢ succNthVal p n a₁ a₂ bs ha₁ ha₂ ^ p * a₁.coeff 0 ^ p ^ (n + 1) + a₁.coeff (n + 1) * (bs 0 ^ p) ^ p ^ (n + 1) +
      nthRemainder p n (fun v ↦ bs v ^ p) (truncateFun (n + 1) a₁) =
    succNthVal p n a₁ a₂ bs ha₁ ha₂ * a₂.coeff 0 ^ p ^ (n + 1) + a₂.coeff (n + 1) * bs 0 ^ p ^ (n + 1) +
      nthRemainder p n bs (truncateFun (n + 1) a₂)

Tactic:
by
  rw [← sub_eq_zero]
  have := succNthVal_spec p n a₁ a₂ bs ha₁ ha₂
  simp only [Polynomial.eval_X, Polynomial.eval_C,
    Polynomial.eval_pow, succNthDefiningPoly, Polynomial.eval_mul, Polynomial.eval_add,
    Polynomial.eval_sub, Polynomial.IsRoot.def]
    at this
  convert! this using 1
  ring

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

Goal state before:
pp: p : ℕ
inst✝⁵ : Fact (Nat.Prime p)
k : Type u_2
inst✝⁴ : Field k
inst✝³ : IsAlgClosed k
inst✝² : CharP k p
V : Type u_3
inst✝¹ : AddCommGroup V
inst✝ : Isocrystal p k V
h_dim : finrank K(p, k) V = 1
this : Nontrivial V
x : V
hx : x ≠ 0
⊢ ∃ m, Nonempty (StandardOneDimIsocrystal p k m ≃ᶠⁱ[p, k] V)

Tactic:
have : Φ(p, k) x ≠ 0 := by simpa only [map_zero] using Φ(p, k).injective.ne hx

Goal state after:
p : ℕ
inst✝⁵ : Fact (Nat.Prime p)
k : Type u_2
inst✝⁴ : Field k
inst✝³ : IsAlgClosed k
inst✝² : CharP k p
V : Type u_3
inst✝¹ : AddCommGroup V
inst✝ : Isocrystal p k V
h_dim : finrank K(p, k) V = 1
this✝ : Nontrivial V
x : V
hx : x ≠ 0
this : Φ(p, k) x ≠ 0
⊢ ∃ m, Nonempty (StandardOneDimIsocrystal p k m ≃ᶠⁱ[p, k] V)
Module: Mathlib.SetTheory.Cardinal.Cofinality.Club

Goal state before:
pp: case inr.refine_2.inr
α : Type v
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
f : α → α
hα : cof α ≠ ℵ₀
hf : IsNormal f
h✝ : Nonempty α
a : α
h : NoTopOrder α
⊢ ∃ y ∈ Function.fixedPoints f, a ≤ y

Tactic:
| inr h =>

Goal state after:
Module: Mathlib.SetTheory.Cardinal.Cofinality.Club

Goal state before:
pp: α : Type v
inst✝ : LinearOrder α
ι : Sort u_1
f : ι → Set α
hα : cof α ≤ 1
⊢ IsStationary (⋃ i, f i) ↔ ∃ i, IsStationary (f i)

Tactic:
← sUnion_range,

Goal state after:
α : Type v
inst✝ : LinearOrder α
ι : Sort u_1
f : ι → Set α
hα : cof α ≤ 1
⊢ IsStationary (⋃₀ range f) ↔ ∃ i, IsStationary (f i)
Module: Mathlib.SetTheory.Cardinal.Cofinality.Club

Goal state before:
pp: α : Type v
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
ι : Type u
f : ι → Set α
hα : cof α ≠ ℵ₀
hι : lift.{v, u} #ι < lift.{u, v} (cof α)
⊢ IsStationary (⋃ i, f i) ↔ ∃ i, IsStationary (f i)

Tactic:
← sUnion_range,

Goal state after:
α : Type v
inst✝¹ : LinearOrder α
inst✝ : WellFoundedLT α
ι : Type u
f : ι → Set α
hα : cof α ≠ ℵ₀
hι : lift.{v, u} #ι < lift.{u, v} (cof α)
⊢ IsStationary (⋃₀ range f) ↔ ∃ i, IsStationary (f i)
Module: Mathlib.SetTheory.Cardinal.Cofinality.Club

Goal state before:
pp: α : Type v
inst✝² : LinearOrder α
inst✝¹ : WellFoundedLT α
ι : Sort u_1
f : ι → Set α
inst✝ : Countable ι
hα : cof α ≠ ℵ₀
⊢ IsStationary (⋃ i, f i) ↔ ∃ i, IsStationary (f i)

Tactic:
← sUnion_range,

Goal state after:
α : Type v
inst✝² : LinearOrder α
inst✝¹ : WellFoundedLT α
ι : Sort u_1
f : ι → Set α
inst✝ : Countable ι
hα : cof α ≠ ℵ₀
⊢ IsStationary (⋃₀ range f) ↔ ∃ i, IsStationary (f i)
Module: Mathlib.SetTheory.Ordinal.FixedPointApproximants

Goal state before:
pp: case refine_2
α : Type u
inst✝ : CompleteLattice α
f : α →o α
x : α
hx : x ≤ f x
o : Ordinal.{u}
h : f x = x ∨ o = 0
⊢ lfpApprox f x o = x

Tactic:
rcases h with (hf | rfl)
    · exact (lfpApprox_eq_all_of_fixedPoint f hx).mpr hf o
    · exact lfpApprox_zero f

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

Goal state before:
pp: b o : Ordinal.{u_1}
⊢ (coeff b o).support = (map Prod.fst (CNF b o)).toFinset

Tactic:
rw [coeff, lookupFinsupp_support, filter_eq_self.2]
  · simp [List.keys]
  · simp_rw [mem_map]
    rintro _ ⟨a, ⟨ha, rfl⟩⟩
    simpa using (snd_pos ha).ne'

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

Goal state before:
pp: s : Set Ordinal.{u}
a : Ordinal.{u}
⊢ a ∈ closure s ↔ ∃ ι, ∃ (_ : Nonempty ι), ∃ f, (∀ (i : ι), f i ∈ s) ∧ ⨆ i, f i = a

Tactic:
apply ((mem_closure_tfae a s).out 0 4).trans
  simp_rw [exists_prop]

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

Goal state before:
pp: 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
a : Ordinal.{u_1}
⊢ f a < b

Tactic:
by_cases ha : a ∈ f.support

Goal state after:
case pos
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
a : Ordinal.{u_1}
ha : a ∈ f.support
⊢ f a < b

case neg
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
a : Ordinal.{u_1}
ha : a ∉ f.support
⊢ f a < b
Module: Mathlib.SetTheory.Ordinal.Topology

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

Tactic:
· rw [← bsup_eq_iSup]
    apply H (type_ne_zero_iff_nonempty.2 hι)
    exact fun i hi => hf _

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

Goal state before:
pp: case eq.inr.inr.eq
o₁ e₁ a₁ o₂ : ONote
n₂ : ℕ+
a₂ : ONote
h✝¹ : o₂ = e₁.oadd n₂ a₂
h₂ : (namedPattern o₂ (e₁.oadd n₂ a₂) h✝¹).NF
h✝ : o₁ = e₁.oadd n₂ a₁
h₁ : (namedPattern o₁ (e₁.oadd n₂ a₁) h✝).NF
nhl : ↑n₂ ≤ ↑n₂
nhr : ¬↑n₂ < ↑n₂ ∧ Ordering.eq = Ordering.eq
IHa : a₁ = a₂
⊢ (Ordering.eq.then (Ordering.eq.then Ordering.eq)).Compares (namedPattern o₁ (e₁.oadd n₂ a₁) h✝)
    (namedPattern o₂ (e₁.oadd n₂ a₂) h✝¹)

pp: case eq.inr.inr.gt
o₁ e₁ a₁ o₂ : ONote
n₂ : ℕ+
a₂ : ONote
h✝¹ : o₂ = e₁.oadd n₂ a₂
h₂ : (namedPattern o₂ (e₁.oadd n₂ a₂) h✝¹).NF
h✝ : o₁ = e₁.oadd n₂ a₁
h₁ : (namedPattern o₁ (e₁.oadd n₂ a₁) h✝).NF
nhl : ↑n₂ ≤ ↑n₂
nhr : ¬↑n₂ < ↑n₂ ∧ Ordering.eq = Ordering.eq
IHa : a₁ > a₂
⊢ (Ordering.eq.then (Ordering.eq.then Ordering.gt)).Compares (namedPattern o₁ (e₁.oadd n₂ a₁) h✝)
    (namedPattern o₂ (e₁.oadd n₂ a₂) h✝¹)

Tactic:
case gt => exact oadd_lt_oadd_3 IHa

Goal state after:
case eq.inr.inr.eq
o₁ e₁ a₁ o₂ : ONote
n₂ : ℕ+
a₂ : ONote
h✝¹ : o₂ = e₁.oadd n₂ a₂
h₂ : (namedPattern o₂ (e₁.oadd n₂ a₂) h✝¹).NF
h✝ : o₁ = e₁.oadd n₂ a₁
h₁ : (namedPattern o₁ (e₁.oadd n₂ a₁) h✝).NF
nhl : ↑n₂ ≤ ↑n₂
nhr : ¬↑n₂ < ↑n₂ ∧ Ordering.eq = Ordering.eq
IHa : a₁ = a₂
⊢ (Ordering.eq.then (Ordering.eq.then Ordering.eq)).Compares (namedPattern o₁ (e₁.oadd n₂ a₁) h✝)
    (namedPattern o₂ (e₁.oadd n₂ a₂) h✝¹)
Module: Mathlib.SetTheory.Ordinal.Veblen

Goal state before:
pp: f : Ordinal.{u} → Ordinal.{u}
o₁ o₂ : Ordinal.{u}
hf : IsNormal f
h : o₁ < o₂
a : Ordinal.{u}
⊢ veblenWith f o₁ (veblenWith f o₂ a) = veblenWith f o₂ a

Tactic:
apply (mem_range_veblenWith hf h.ne_bot).1 _ _ h
  simp

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

Goal state before:
pp: α✝ : Type u_1
A✝ : α✝ → PSet.{u_1}
x✝ : PSet.{u_1}
w✝ : (mk α✝ A✝).Type
h : x✝.Equiv ((mk α✝ A✝).Func w✝)
⊢ succ ((mk α✝ A✝).Func w✝).rank ≤ (mk α✝ A✝).rank

Tactic:
apply Ordinal.le_iSup

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

Goal state before:
pp: case neg
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
mn : ↑n₁ - ↑n₂ = 0
en : ¬n₁ = n₂
⊢ (if n₁ = n₂ then a₁.sub a₂ else 0).repr = (e₁.oadd n₁ a₁).repr - (e₁.oadd n₂ a₂).repr

Tactic:
simp only [en, ite_false]

Goal state after:
case neg
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
mn : ↑n₁ - ↑n₂ = 0
en : ¬n₁ = n₂
⊢ repr 0 = (e₁.oadd n₁ a₁).repr - (e₁.oadd n₂ a₂).repr
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basis

Goal state before:
pp: case h
f g : ℝ → ℝ
a b : ℝ
hf : ∀ᶠ (x : ℝ) in atTop, 0 < f x
hg : Tendsto g atTop atTop
h : (Real.log ∘ f) =o[atTop] (Real.log ∘ g)
hb : 0 < b
h' : b • Real.log ∘ g - a • Real.log ∘ f ~[atTop] b • Real.log ∘ g
⊢ Tendsto (b • Real.log ∘ g) atTop atTop

Tactic:
apply Filter.Tendsto.const_mul_atTop hb

Goal state after:
case h
f g : ℝ → ℝ
a b : ℝ
hf : ∀ᶠ (x : ℝ) in atTop, 0 < f x
hg : Tendsto g atTop atTop
h : (Real.log ∘ f) =o[atTop] (Real.log ∘ g)
hb : 0 < b
h' : b • Real.log ∘ g - a • Real.log ∘ f ~[atTop] b • Real.log ∘ g
⊢ Tendsto (Real.log ∘ g) atTop atTop
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion

Goal state before:
pp: α : Type u_1
op : Stream'.Seq α → Stream'.Seq α
a : α
s t s' t' : Stream'.Seq α
h : s' = nil ∧ t' = nil ∨ ∃ hd s'_1 t'_1, s' = Seq.cons hd s'_1 ∧ t' = Seq.cons hd t'_1
⊢ s'.head = t'.head

Tactic:
obtain ⟨rfl, rfl⟩ | ⟨hd, s_tl, t_tl, rfl, rfl⟩ := h

Goal state after:
case inl
α : Type u_1
op : Stream'.Seq α → Stream'.Seq α
a : α
s t : Stream'.Seq α
⊢ nil.head = nil.head

case inr
α : Type u_1
op : Stream'.Seq α → Stream'.Seq α
a : α
s t : Stream'.Seq α
hd : α
s_tl t_tl : Stream'.Seq α
⊢ (Seq.cons hd s_tl).head = (Seq.cons hd t_tl).head
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs

Goal state before:
pp: basis_hd : ℝ → ℝ
basis_tl : Basis
x y : Multiseries basis_hd basis_tl
motive : Multiseries basis_hd basis_tl → Multiseries basis_hd basis_tl → Prop
base : motive x y
step :
  ∀ (x y : Multiseries basis_hd basis_tl),
    motive x y → x = nil ∧ y = nil ∨ ∃ exp coef x' y', x = cons exp coef x' ∧ y = cons exp coef y' ∧ motive x' y'
⊢ ∀ (s₁ s₂ : Stream'.Seq (ℝ × MultiseriesExpansion basis_tl)),
    motive s₁ s₂ → s₁ = Seq.nil ∧ s₂ = Seq.nil ∨ ∃ x s₁' s₂', s₁ = Seq.cons x s₁' ∧ s₂ = Seq.cons x s₂' ∧ motive s₁' s₂'

Tactic:
by grind [nil, cons]

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

Goal state before:
pp: basis_hd : ℝ → ℝ
basis_tl : Basis
x y : Multiseries basis_hd basis_tl
motive : Multiseries basis_hd basis_tl → Multiseries basis_hd basis_tl → Prop
base : motive x y
step :
  ∀ (x y : Multiseries basis_hd basis_tl),
    motive x y → x = y ∨ ∃ exp coef x' y', x = cons exp coef x' ∧ y = cons exp coef y' ∧ motive x' y'
⊢ ∀ (s₁ s₂ : Stream'.Seq (ℝ × MultiseriesExpansion basis_tl)),
    motive s₁ s₂ → s₁ = s₂ ∨ ∃ x s₁' s₂', s₁ = Seq.cons x s₁' ∧ s₂ = Seq.cons x s₂' ∧ motive s₁' s₂'

Tactic:
by grind [nil, cons]

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

Goal state before:
pp: t1 t2 : Monomial
basis : Basis
h_basis : WellFormedBasis basis
h_length : List.length t1.unit = List.length t2.unit
t : ℝ
⊢ ((t1.coef * t2.coef) • (t1.unit.toFun basis * t2.unit.toFun basis)) t =
    (t2.coef • t1.coef • (t1.unit.toFun basis * t2.unit.toFun basis)) t

Tactic:
simp [Pi.smul_apply, Pi.mul_apply]

Goal state after:
t1 t2 : Monomial
basis : Basis
h_basis : WellFormedBasis basis
h_length : List.length t1.unit = List.length t2.unit
t : ℝ
⊢ t1.coef * t2.coef * (t1.unit.toFun basis t * t2.unit.toFun basis t) =
    t2.coef * (t1.coef * (t1.unit.toFun basis t * t2.unit.toFun basis t))
Module: Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic

Goal state before:
pp: t : Monomial
basis : Basis
h_basis : WellFormedBasis basis
x : ℝ
⊢ (t.coef⁻¹ • (t.unit.toFun basis)⁻¹) x = (t.coef • t.unit.toFun basis)⁻¹ x

Tactic:
simp [Pi.smul_apply, Pi.inv_apply]

Goal state after:
t : Monomial
basis : Basis
h_basis : WellFormedBasis basis
x : ℝ
⊢ t.coef⁻¹ * (t.unit.toFun basis x)⁻¹ = (t.unit.toFun basis x)⁻¹ * t.coef⁻¹
Module: Mathlib.Tactic.ITauto

Goal state before:
pp: case var.true
a✝ : Nat
⊢ Ordering

pp: case var.false
a✝ : Nat
⊢ Ordering

pp: case var.and'
a✝³ : Nat
a✝² : AndKind
a✝¹ a✝ : IProp
⊢ Ordering

pp: case var.or
a✝² : Nat
a✝¹ a✝ : IProp
⊢ Ordering

pp: case var.imp
a✝² : Nat
a✝¹ a✝ : IProp
⊢ Ordering

pp: case true.var
a✝ : Nat
⊢ Ordering

pp: case true.false
⊢ Ordering

pp: case true.and'
a✝² : AndKind
a✝¹ a✝ : IProp
⊢ Ordering

pp: case true.or
a✝¹ a✝ : IProp
⊢ Ordering

pp: case true.imp
a✝¹ a✝ : IProp
⊢ Ordering

pp: case false.var
a✝ : Nat
⊢ Ordering

pp: case false.true
⊢ Ordering

pp: case false.and'
a✝² : AndKind
a✝¹ a✝ : IProp
⊢ Ordering

pp: case false.or
a✝¹ a✝ : IProp
⊢ Ordering

pp: case false.imp
a✝¹ a✝ : IProp
⊢ Ordering

pp: case and'.var
a✝³ : AndKind
a✝² a✝¹ : IProp
a✝ : Nat
⊢ Ordering

pp: case and'.true
a✝² : AndKind
a✝¹ a✝ : IProp
⊢ Ordering

pp: case and'.false
a✝² : AndKind
a✝¹ a✝ : IProp
⊢ Ordering

pp: case and'.or
a✝⁴ : AndKind
a✝³ a✝² a✝¹ a✝ : IProp
⊢ Ordering

pp: case and'.imp
a✝⁴ : AndKind
a✝³ a✝² a✝¹ a✝ : IProp
⊢ Ordering

pp: case or.var
a✝² a✝¹ : IProp
a✝ : Nat
⊢ Ordering

pp: case or.true
a✝¹ a✝ : IProp
⊢ Ordering

pp: case or.false
a✝¹ a✝ : IProp
⊢ Ordering

pp: case or.and'
a✝⁴ a✝³ : IProp
a✝² : AndKind
a✝¹ a✝ : IProp
⊢ Ordering

pp: case or.imp
a✝³ a✝² a✝¹ a✝ : IProp
⊢ Ordering

pp: case imp.var
a✝² a✝¹ : IProp
a✝ : Nat
⊢ Ordering

pp: case imp.true
a✝¹ a✝ : IProp
⊢ Ordering

pp: case imp.false
a✝¹ a✝ : IProp
⊢ Ordering

pp: case imp.and'
a✝⁴ a✝³ : IProp
a✝² : AndKind
a✝¹ a✝ : IProp
⊢ Ordering

pp: case imp.or
a✝³ a✝² a✝¹ a✝ : IProp
⊢ Ordering

Tactic:
exacts [.lt, .lt, .lt, .lt, .lt,
          .gt, .lt, .lt, .lt, .lt,
          .gt, .gt, .lt, .lt, .lt,
          .gt, .gt, .gt, .lt, .lt,
          .gt, .gt, .gt, .gt, .lt,
          .gt, .gt, .gt, .gt, .gt]

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

Goal state before:
pp: a : ℕ
⊢ jacobiSym (↑a) 0 = 1

Tactic:
jacobiSym.zero_right

Goal state after:
a : ℕ
⊢ 1 = 1
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
⊢ ⨅ i, comap (fun x ↦ ((Prod.map F F x).1 i, (Prod.map F F x).2 i)) (𝓤 α) ≤ 𝓤 ι

Tactic:
refine ((UniformFun.hasBasis_uniformity X α).comap (Prod.map F F)).ge_iff.mpr ?_

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
⊢ ∀ i' ∈ 𝓤 α,
    Prod.map F F ⁻¹' UniformFun.gen X α i' ∈ ⨅ i, comap (fun x ↦ ((Prod.map F F x).1 i, (Prod.map F F x).2 i)) (𝓤 α)
Module: Mathlib.Topology.Algebra.Group.CompactOpen

Goal state before:
pp: case mp
X : Type u_7
Y : Type u_8
inst✝⁷ : TopologicalSpace X
inst✝⁶ : Group X
inst✝⁵ : IsTopologicalGroup X
inst✝⁴ : UniformSpace Y
inst✝³ : CommGroup Y
inst✝² : IsUniformGroup Y
inst✝¹ : T0Space Y
inst✝ : CompactSpace Y
U : Set X
V : Set Y
hU : IsCompact U
hV : V ∈ 𝓝 1
W : Set Y
hWo : W ∈ 𝓝 1
hWV : W ⊆ V
hWc : IsCompact W
S1 : Set (X →* Y) := ⋯
S2 : Set (X →ₜ* Y) := ⋯
S3 : Set C(X, Y) := ⋯
S4 : Set (X → Y) := ⋯
h : Equicontinuous fun x ↦ ⇑↑x
x✝ : X → Y
⊢ x✝ ∈ S4 → x✝ ∈ DFunLike.coe '' S1

Tactic:
rintro ⟨-, ⟨f, hf, rfl⟩, rfl⟩
      exact ⟨f, hf, rfl⟩

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
U : Set G
hU : U ∈ 𝓝 1
x : X
V : Set G
V_mem : V ∈ 𝓝 1
V_closed : IsClosed[inst✝⁹] V
V_symm : V⁻¹ = V
VU : V * V ⊆ U
s : Set G
s_count : s.Countable
hs : ⋃ g ∈ s, g • V = univ
K : ℕ → Set G := compactCovering G
F : ℕ × ↑s → Set X := fun p ↦ (K p.1 ∩ ↑p.2 • V) • {x}
this✝ : Nonempty X
this : Encodable ↑s
n : ℕ
g : G
hg : g ∈ s
⊢ Continuous[inst✝⁹, inst✝⁸] fun g ↦ g • x

Tactic:
fun_prop

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

Goal state before:
pp: X : Type u_7
Y : Type u_8
inst✝⁸ : TopologicalSpace X
inst✝⁷ : Group X
inst✝⁶ : IsTopologicalGroup X
inst✝⁵ : UniformSpace Y
inst✝⁴ : CommGroup Y
inst✝³ : IsUniformGroup Y
inst✝² : T0Space Y
inst✝¹ : CompactSpace Y
inst✝ : LocallyCompactSpace X
V : ℕ → Set Y
hV : ∀ {n : ℕ} {x : Y}, x ∈ V n → x * x ∈ V n → x ∈ V (n + 1)
hVo : (𝓝 1).HasBasis (fun x ↦ True) V
U0 : Set X
hU0c : IsCompact U0
hU0o : U0 ∈ 𝓝 1
⊢ LocallyCompactSpace (X →ₜ* Y)

Tactic:
let U_aux : ℕ → {S : Set X | S ∈ nhds 1} :=
    Nat.rec ⟨U0, hU0o⟩ <| fun _ S ↦ let h := exists_closed_nhds_one_inv_eq_mul_subset S.2
      ⟨Classical.choose h, (Classical.choose_spec h).1⟩

Goal state after:
X : Type u_7
Y : Type u_8
inst✝⁸ : TopologicalSpace X
inst✝⁷ : Group X
inst✝⁶ : IsTopologicalGroup X
inst✝⁵ : UniformSpace Y
inst✝⁴ : CommGroup Y
inst✝³ : IsUniformGroup Y
inst✝² : T0Space Y
inst✝¹ : CompactSpace Y
inst✝ : LocallyCompactSpace X
V : ℕ → Set Y
hV : ∀ {n : ℕ} {x : Y}, x ∈ V n → x * x ∈ V n → x ∈ V (n + 1)
hVo : (𝓝 1).HasBasis (fun x ↦ True) V
U0 : Set X
hU0c : IsCompact U0
hU0o : U0 ∈ 𝓝 1
U_aux : ℕ → ↑{S | S ∈ 𝓝 1} :=
  fun t ↦
    Nat.rec ⟨U0, hU0o⟩
      (fun x S ↦
        let h := ⋯;
        ⟨Classical.choose h, ⋯⟩)
      t
⊢ LocallyCompactSpace (X →ₜ* Y)