mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.NumberTheory.Ostrowski

Goal state before:
pp: f : AbsoluteValue ℚ ℝ
m n : ℕ
hm : 1 < m
hn : 1 < n
notbdd : ¬∀ (n : ℕ), f ↑n ≤ 1
k : ℕ
hk : k ≠ 0
h_ineq1 : ∀ {m n : ℕ}, 1 < m → 1 < n → f ↑n ≤ ↑m * f ↑m / (f ↑m - 1) * f ↑m ^ logb ↑m ↑n
he : 0 < ↑m * f ↑m / (f ↑m - 1)
⊢ f ↑n ^ k = f ↑(n ^ k)

Tactic:
by simp

Goal state after:
Module: Mathlib.NumberTheory.Padics.Complex

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
⊢ Valued.v ↑p = 1 / ↑p

Tactic:
← map_natCast (algebraMap ℚ_[p] (PadicAlgCl p))

Goal state after:
p : ℕ
inst✝ : Fact (Nat.Prime p)
⊢ Valued.v ((algebraMap ℚ_[p] (PadicAlgCl p)) ↑p) = 1 / ↑p
Module: Mathlib.NumberTheory.Padics.Complex

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

Tactic:
← map_natCast (algebraMap (PadicAlgCl p) ℂ_[p]) n,

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
n : ℕ
⊢ ↑↑n = (algebraMap (PadicAlgCl p) ℂ_[p]) ↑n
Module: Mathlib.NumberTheory.Padics.MahlerBasis

Goal state before:
pp: M : Type u_1
G : Type u_2
inst✝¹ : AddCommMonoidWithOne M
inst✝ : AddCommGroup G
f : M → G
n R : ℕ
hR : 1 ≤ R
aux : Δ_[1]^[n + R] f 0 = R.choose (R - 1 + 1) • Δ_[1]^[n + R] f 0
⊢ Δ_[1]^[n + R] f 0 =
    -∑ j ∈ range (R - 1), R.choose (j + 1) • Δ_[1]^[n + (j + 1)] f 0 +
      ∑ k ∈ range (n + 1), ((-1) ^ (n - k) * ↑(n.choose k)) • (f (↑k + ↑R) - f ↑k)

Tactic:
rw [neg_add_eq_sub, eq_sub_iff_add_eq, add_comm, aux, (by lia : n + R = (n + ((R - 1) + 1))),
    ← sum_range_succ, Nat.sub_add_cancel hR,
    ← sub_eq_iff_eq_add.mpr (sum_range_succ' (fun x ↦ R.choose x • Δ_[1]^[n + x] f 0) R), add_zero,
    Nat.choose_zero_right, one_smul]

Goal state after:
M : Type u_1
G : Type u_2
inst✝¹ : AddCommMonoidWithOne M
inst✝ : AddCommGroup G
f : M → G
n R : ℕ
hR : 1 ≤ R
aux : Δ_[1]^[n + R] f 0 = R.choose (R - 1 + 1) • Δ_[1]^[n + R] f 0
⊢ ∑ k ∈ range (R + 1), R.choose k • Δ_[1]^[n + k] f 0 - Δ_[1]^[n] f 0 =
    ∑ k ∈ range (n + 1), ((-1) ^ (n - k) * ↑(n.choose k)) • (f (↑k + ↑R) - f ↑k)
Module: Mathlib.NumberTheory.Padics.HeightOneSpectrum

Goal state before:
pp: R✝ : Type u_1
inst✝⁷ : CommRing R✝
inst✝⁶ : Algebra R✝ ℚ
inst✝⁵ : IsIntegralClosure R✝ ℤ ℚ
R : Type u_2
inst✝⁴ : CommRing R
inst✝³ : Algebra R ℚ
inst✝² : IsIntegralClosure R ℤ ℚ
inst✝¹ : IsDedekindDomain R
inst✝ : IsFractionRing R ℚ
v : HeightOneSpectrum R
⊢ ∀ (r : ℚ),
    ((HeightOneSpectrum.adicCompletion.equiv ℚ v).trans
            ((mapRingEquiv
                  (WithVal.congr (HeightOneSpectrum.valuation ℚ v) (padicValuation ↑(primesEquiv v)) (RingEquiv.refl ℚ))
                  ⋯ ⋯).trans
              Padic.withValRingEquiv)).toFun
        ((algebraMap ℚ (HeightOneSpectrum.adicCompletion ℚ v)) r) =
      (algebraMap ℚ ℚ_[↑(primesEquiv v)]) r

Tactic:
by simp

Goal state after:
Module: Mathlib.NumberTheory.Padics.HeightOneSpectrum

Goal state before:
pp: R✝ : Type u_1
inst✝⁷ : CommRing R✝
inst✝⁶ : Algebra R✝ ℚ
inst✝⁵ : IsIntegralClosure R✝ ℤ ℚ
R : Type u_2
inst✝⁴ : CommRing R
inst✝³ : Algebra R ℚ
inst✝² : IsIntegralClosure R ℤ ℚ
inst✝¹ : IsDedekindDomain R
inst✝ : IsFractionRing R ℚ
v : HeightOneSpectrum R
⊢ ∀ (r : ℤ),
    (let e0 :=
            (HeightOneSpectrum.adicCompletion.equiv ℚ v).restrict (HeightOneSpectrum.adicCompletionIntegers ℚ v)
              Valued.v.valuationSubring ⋯;
          let e :=
            (mapRingEquiv
                  (WithVal.congr (HeightOneSpectrum.valuation ℚ v) (padicValuation ↑(primesEquiv v)) (RingEquiv.refl ℚ))
                  ⋯ ⋯).restrict
              Valued.v.valuationSubring (Valued.integer (padicValuation ↑(primesEquiv v)).Completion) ⋯;
          (e0.trans e).trans withValIntegersRingEquiv).toFun
        ((algebraMap ℤ ↥(HeightOneSpectrum.adicCompletionIntegers ℚ v)) r) =
      (algebraMap ℤ ℤ_[↑(primesEquiv v)]) r

Tactic:
by simp

Goal state after:
Module: Mathlib.NumberTheory.PrimesCongruentOne

Goal state before:
pp: case inr.refine_2
k n : ℕ
hk0 : k ≠ 0
hk1 : 1 < k
b : ℕ := k * n !
hgt : 1 < (eval (↑b) (cyclotomic k ℤ)).natAbs
p : ℕ := (eval (↑b) (cyclotomic k ℤ)).natAbs.minFac
hprime : Fact (Prime p)
hroot : (cyclotomic k (ZMod p)).IsRoot ((castRingHom (ZMod p)) b)
hpb : ¬p ∣ b
hdiv : k ∣ p - 1
this✝ : NeZero ↑k
this : k = orderOf ↑b
⊢ p ≡ 1 [MOD k]

Tactic:
exact ((modEq_iff_dvd' hprime.1.pos).2 hdiv).symm

Goal state after:
Module: Mathlib.NumberTheory.Padics.Hensel

Goal state before:
pp: p : ℕ
inst✝² : Fact (Nat.Prime p)
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Algebra R ℤ_[p]
F : Polynomial R
x y z : ℤ_[p]
hz : (Polynomial.aeval x) F - (Polynomial.aeval y) F = z * (x - y)
⊢ 1 * ‖x - y‖ = ‖x - y‖

Tactic:
by simp

Goal state after:
Module: Mathlib.NumberTheory.Pell

Goal state before:
pp: d : ℤ
a₁ : Solution₁ d
h : IsFundamental a₁
a : Solution₁ d
hax : 1 < a.x
hay : 0 < a.y
⊢ a₁.y ≤ a.y

Tactic:
exact h.y_le_y hax hay

Goal state after:
Module: Mathlib.NumberTheory.Pell

Goal state before:
pp: case inl
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
a₁ : Solution₁ d
ha₁ : IsFundamental a₁
n₁ n₂ : ℤ
Hx : 1 < (a₁ ^ n₂).x
Hy : 0 < (a₁ ^ n₂).y
H : ∀ (a : Solution₁ d), ∃ n, a = (a₁ ^ n₂) ^ n ∨ a = -(a₁ ^ n₂) ^ n
hn₁ : a₁ ^ (n₂ * n₁) * a₁ ^ (-1) = 1 ∨ -a₁ ^ (n₂ * n₁) * a₁ ^ (-1) = 1
⊢ a₁ ^ n₂ = a₁

Tactic:
neg_mul,

Goal state after:
case inl
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
a₁ : Solution₁ d
ha₁ : IsFundamental a₁
n₁ n₂ : ℤ
Hx : 1 < (a₁ ^ n₂).x
Hy : 0 < (a₁ ^ n₂).y
H : ∀ (a : Solution₁ d), ∃ n, a = (a₁ ^ n₂) ^ n ∨ a = -(a₁ ^ n₂) ^ n
hn₁ : a₁ ^ (n₂ * n₁) * a₁ ^ (-1) = 1 ∨ -(a₁ ^ (n₂ * n₁) * a₁ ^ (-1)) = 1
⊢ a₁ ^ n₂ = a₁
Module: Mathlib.NumberTheory.Padics.Hensel

Goal state before:
pp: p : ℕ
inst✝² : Fact (Nat.Prime p)
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Algebra R ℤ_[p]
F : Polynomial R
a : ℤ_[p]
hnorm : ‖(Polynomial.aeval a) F‖ < ‖(Polynomial.aeval a) (Polynomial.derivative F)‖ ^ 2
⊢ 1 < 2

Tactic:
by simp

Goal state after:
Module: Mathlib.NumberTheory.Padics.Hensel

Goal state before:
pp: p : ℕ
inst✝² : Fact (Nat.Prime p)
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Algebra R ℤ_[p]
F : Polynomial R
a : ℤ_[p]
hnorm : ‖(Polynomial.aeval a) F‖ < ‖(Polynomial.aeval a) (Polynomial.derivative F)‖ ^ 2
hnsol : (Polynomial.aeval a) F ≠ 0
n : ℕ
⊢ 1 ≤ 2

Tactic:
by simp

Goal state after:
Module: Mathlib.NumberTheory.Padics.Hensel

Goal state before:
pp: p : ℕ
inst✝² : Fact (Nat.Prime p)
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Algebra R ℤ_[p]
F : Polynomial R
a : ℤ_[p]
hnorm : ‖(Polynomial.aeval a) F‖ < ‖(Polynomial.aeval a) (Polynomial.derivative F)‖ ^ 2
hnsol : (Polynomial.aeval a) F ≠ 0
z : ℤ_[p]
hev : (Polynomial.aeval z) F = 0
hnlt : ‖z - a‖ < ‖(Polynomial.aeval a) (Polynomial.derivative F)‖
⊢ ‖z - soln‖ < ‖(Polynomial.aeval soln) (Polynomial.derivative F)‖

Tactic:
soln_deriv_norm

Goal state after:
p : ℕ
inst✝² : Fact (Nat.Prime p)
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Algebra R ℤ_[p]
F : Polynomial R
a : ℤ_[p]
hnorm : ‖(Polynomial.aeval a) F‖ < ‖(Polynomial.aeval a) (Polynomial.derivative F)‖ ^ 2
hnsol : (Polynomial.aeval a) F ≠ 0
z : ℤ_[p]
hev : (Polynomial.aeval z) F = 0
hnlt : ‖z - a‖ < ‖(Polynomial.aeval a) (Polynomial.derivative F)‖
⊢ ‖z - soln‖ < ‖(Polynomial.aeval a) (Polynomial.derivative F)‖
Module: Mathlib.NumberTheory.RamificationInertia.Valuation

Goal state before:
pp: A : Type u_1
K : Type u_2
L : Type u_3
B : Type u_4
inst✝¹⁶ : CommRing A
inst✝¹⁵ : IsDedekindDomain A
inst✝¹⁴ : CommRing B
inst✝¹³ : IsDedekindDomain B
inst✝¹² : Algebra A B
inst✝¹¹ : Module.IsTorsionFree A B
inst✝¹⁰ : Field K
inst✝⁹ : Field L
inst✝⁸ : Algebra K L
inst✝⁷ : Algebra A K
inst✝⁶ : IsFractionRing A K
inst✝⁵ : Algebra A L
inst✝⁴ : IsScalarTower A K L
inst✝³ : Algebra B L
inst✝² : IsFractionRing B L
inst✝¹ : IsScalarTower A B L
v : HeightOneSpectrum A
w : HeightOneSpectrum B
inst✝ : w.asIdeal.LiesOver v.asIdeal
γL : (ValuativeRel.ValueGroupWithZero (WithVal (valuation L w)))ˣ
a✝ : True
e : ℕ := v.asIdeal.ramificationIdx' w.asIdeal
σL : (MonoidWithZeroHom.ofClass Valued.v).ValueGroup₀ ≃*o (MonoidWithZeroHom.ofClass (valuation L w)).ValueGroup₀ :=
  WithVal.valueGroupOrderIso₀ (valuation L w)
σw : (MonoidWithZeroHom.ofClass (valuation L w)).ValueGroup₀ ≃*o WithZero (Multiplicative ℤ) :=
  valueGroup₀_equiv_withZeroMulInt (valuation L w)
σwV : ValuativeRel.ValueGroupWithZero (WithVal (valuation L w)) ≃*o
  (MonoidWithZeroHom.ofClass (WithVal.valuation (valuation L w))).ValueGroup₀ :=
  ValuativeRel.ValueGroupWithZero.orderMonoidIso (WithVal.valuation (valuation L w))
m : WithZero (Multiplicative ℤ) := σw (σL (σwV ↑γL))
σvV : ValuativeRel.ValueGroupWithZero (WithVal (valuation K v)) ≃*o
  (MonoidWithZeroHom.ofClass (WithVal.valuation (valuation K v))).ValueGroup₀ :=
  ValuativeRel.ValueGroupWithZero.orderMonoidIso (WithVal.valuation (valuation K v))
σv : (MonoidWithZeroHom.ofClass (valuation K v)).ValueGroup₀ ≃*o WithZero (Multiplicative ℤ) :=
  valueGroup₀_equiv_withZeroMulInt (valuation K v)
σK : (MonoidWithZeroHom.ofClass Valued.v).ValueGroup₀ ≃*o (MonoidWithZeroHom.ofClass (valuation K v)).ValueGroup₀ :=
  WithVal.valueGroupOrderIso₀ (valuation K v)
γK : ValuativeRel.ValueGroupWithZero (WithVal (valuation K v)) := σvV.symm (σK.symm (σv.symm (exp (m.log / ↑e))))
hγK : γK ≠ 0
x : WithVal (valuation K v)
hx : (valuation K v) x.ofVal < exp (m.log / ↑e)
hx₀ : x ≠ 0
⊢ exp (m.log / ↑e) ≠ 0

Tactic:
by simp

Goal state after:
Module: Mathlib.NumberTheory.SelbergSieve

Goal state before:
pp: s : BoundingSieve
l : ℕ
hl : l ∣ s.prodPrimes
p : ℕ
hp : p ∈ l.primeFactors
⊢ 0 < 1 - s.nu p

Tactic:
have hp_prime : p.Prime := prime_of_mem_primeFactors hp

Goal state after:
s : BoundingSieve
l : ℕ
hl : l ∣ s.prodPrimes
p : ℕ
hp : p ∈ l.primeFactors
hp_prime : Nat.Prime p
⊢ 0 < 1 - s.nu p
Module: Mathlib.NumberTheory.Zsqrtd.GaussianInt

Goal state before:
pp: ⊢ I * I = ↑(-1)

Tactic:
by simp

Goal state after:
Module: Mathlib.NumberTheory.Zsqrtd.GaussianInt

Goal state before:
pp: x : ℤ[i]
⊢ -1 ≤ 0

Tactic:
by simp

Goal state after:
Module: Mathlib.NumberTheory.Zsqrtd.GaussianInt

Goal state before:
pp: x y : ℤ[i]
⊢ 0 ≤ 2⁻¹

Tactic:
by simp

Goal state after:
Module: Mathlib.NumberTheory.Zsqrtd.GaussianInt

Goal state before:
pp: x y : ℤ[i]
hy : y ≠ 0
this : toComplex y ≠ 0
⊢ normSq (toComplex y) * 1 = ↑(norm y)

Tactic:
by simp

Goal state after:
Module: Mathlib.NumberTheory.SumTwoSquares

Goal state before:
pp: n : ℕ
hn : Squarefree n
help : ∀ (a b : ZMod 4), a ≠ 3 → b ≠ 3 → a * b ≠ 3
H : ∀ q ∈ n.primeFactors, q % 4 ≠ 3
x✝ : 0 ∣ n
⊢ 0 % 4 ≠ 3

Tactic:
by simp

Goal state after:
Module: Mathlib.NumberTheory.SumTwoSquares

Goal state before:
pp: n : ℕ
hn : Squarefree n
help : ∀ (a b : ZMod 4), a ≠ 3 → b ≠ 3 → a * b ≠ 3
H : ∀ q ∈ n.primeFactors, q % 4 ≠ 3
x✝ : 1 ∣ n
⊢ 1 % 4 ≠ 3

Tactic:
by simp

Goal state after:
Module: Mathlib.NumberTheory.Zsqrtd.QuadraticReciprocity

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
hp3 : p % 4 = 3
hpi : ¬Irreducible ↑p
a b : ℕ
hab : a ^ 2 + b ^ 2 = p
this : ∀ (a b : ZMod 4), a ^ 2 + b ^ 2 ≠ ↑p
⊢ ↑a ^ 2 + ↑b ^ 2 = ↑(a ^ 2 + b ^ 2)

Tactic:
by simp

Goal state after:
Module: Mathlib.NumberTheory.RamificationInertia.Basic

Goal state before:
pp: case refine_1
R : Type u
inst✝¹⁴ : CommRing R
S : Type v
inst✝¹³ : CommRing S
inst✝¹² : Algebra R S
p : Ideal R
K : Type u_1
inst✝¹¹ : Field K
inst✝¹⁰ : Algebra R K
L : Type u_2
inst✝⁹ : Field L
inst✝⁸ : Algebra S L
inst✝⁷ : IsFractionRing S L
hRK : IsFractionRing R K
inst✝⁶ : IsDomain S
inst✝⁵ : IsDedekindDomain R
inst✝⁴ : Algebra K L
inst✝³ : Algebra R L
inst✝² : IsScalarTower R K L
inst✝¹ : IsScalarTower R S L
hp : p.IsMaximal
inst✝ : Module.Finite R S
ι : Type v := Free.ChooseBasisIndex (R ⧸ p) (S ⧸ map f p)
b : Basis ι (R ⧸ p) (S ⧸ map f p) := Free.chooseBasis (R ⧸ p) (S ⧸ map f p)
b' : ι → S := fun i ↦ ⋯.choose
b_eq_b' : ⇑b = ⇑(↑R (Submodule.mkQ (map f p))) ∘ b'
b'' : ι → L := ⇑(algebraMap S L) ∘ b'
this : LinearIndependent (R ⧸ p) (⇑(↑R (Submodule.mkQ (map f p))) ∘ b')
⊢ LinearIndependent K b''

Tactic:
convert!
      FinrankQuotientMap.linearIndependent_of_nontrivial K _
        ((Algebra.linearMap S L).restrictScalars R) _ ((Submodule.mkQ _).restrictScalars R) this

Goal state after:
case refine_1.convert_1
R : Type u
inst✝¹⁴ : CommRing R
S : Type v
inst✝¹³ : CommRing S
inst✝¹² : Algebra R S
p : Ideal R
K : Type u_1
inst✝¹¹ : Field K
inst✝¹⁰ : Algebra R K
L : Type u_2
inst✝⁹ : Field L
inst✝⁸ : Algebra S L
inst✝⁷ : IsFractionRing S L
hRK : IsFractionRing R K
inst✝⁶ : IsDomain S
inst✝⁵ : IsDedekindDomain R
inst✝⁴ : Algebra K L
inst✝³ : Algebra R L
inst✝² : IsScalarTower R K L
inst✝¹ : IsScalarTower R S L
hp : p.IsMaximal
inst✝ : Module.Finite R S
ι : Type v := Free.ChooseBasisIndex (R ⧸ p) (S ⧸ map f p)
b : Basis ι (R ⧸ p) (S ⧸ map f p) := Free.chooseBasis (R ⧸ p) (S ⧸ map f p)
b' : ι → S := fun i ↦ ⋯.choose
b_eq_b' : ⇑b = ⇑(↑R (Submodule.mkQ (map f p))) ∘ b'
b'' : ι → L := ⇑(algebraMap S L) ∘ b'
this : LinearIndependent (R ⧸ p) (⇑(↑R (Submodule.mkQ (map f p))) ∘ b')
⊢ RingHom.ker (algebraMap R (R ⧸ p)) ≠ ⊤

case refine_1.convert_2
R : Type u
inst✝¹⁴ : CommRing R
S : Type v
inst✝¹³ : CommRing S
inst✝¹² : Algebra R S
p : Ideal R
K : Type u_1
inst✝¹¹ : Field K
inst✝¹⁰ : Algebra R K
L : Type u_2
inst✝⁹ : Field L
inst✝⁸ : Algebra S L
inst✝⁷ : IsFractionRing S L
hRK : IsFractionRing R K
inst✝⁶ : IsDomain S
inst✝⁵ : IsDedekindDomain R
inst✝⁴ : Algebra K L
inst✝³ : Algebra R L
inst✝² : IsScalarTower R K L
inst✝¹ : IsScalarTower R S L
hp : p.IsMaximal
inst✝ : Module.Finite R S
ι : Type v := Free.ChooseBasisIndex (R ⧸ p) (S ⧸ map f p)
b : Basis ι (R ⧸ p) (S ⧸ map f p) := Free.chooseBasis (R ⧸ p) (S ⧸ map f p)
b' : ι → S := fun i ↦ ⋯.choose
b_eq_b' : ⇑b = ⇑(↑R (Submodule.mkQ (map f p))) ∘ b'
b'' : ι → L := ⇑(algebraMap S L) ∘ b'
this : LinearIndependent (R ⧸ p) (⇑(↑R (Submodule.mkQ (map f p))) ∘ b')
⊢ Function.Injective ⇑(↑R (Algebra.linearMap S L))
Module: Mathlib.NumberTheory.Transcendental.Lindemann.AnalyticalPart

Goal state before:
pp: p : ℂ[X]
s : ℂ
x : ℝ
⊢ HasDerivAt (fun x ↦ -(cexp (-(x • s)) * eval (x • s) (sumIDeriv p))) (s * (cexp (-(x • s)) * eval (x • s) p)) x

Tactic:
have h₀ := (hasDerivAt_id' x).smul_const s
  have h₁ := h₀.fun_neg.cexp
  have h₂ := ((sumIDeriv p).hasDerivAt (x • s)).comp x h₀
  convert! (h₁.mul h₂).fun_neg using 1
  nth_rw 1 [sumIDeriv_eq_self_add p]
  simp only [one_smul, eval_add, Function.comp_apply]
  ring

Goal state after:
Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleNumber

Goal state before:
pp: case h
m : ℕ
hm : 0 < m
k p_k : ℕ
h_k : partialSum (↑m) k = ↑p_k / ↑(m ^ k !)
⊢ (↑p_k * ↑m ^ (k + 1)! + ↑(m ^ k !) * 1) * ↑(m ^ (k + 1)!) =
    ↑(p_k * m ^ ((k + 1)! - k !) + 1) * (↑(m ^ k !) * ↑m ^ (k + 1)!)

pp: case h.hb
m : ℕ
hm : 0 < m
k p_k : ℕ
h_k : partialSum (↑m) k = ↑p_k / ↑(m ^ k !)
⊢ ↑(m ^ k !) * ↑m ^ (k + 1)! ≠ 0

pp: case h.hd
m : ℕ
hm : 0 < m
k p_k : ℕ
h_k : partialSum (↑m) k = ↑p_k / ↑(m ^ k !)
⊢ ↑(m ^ (k + 1)!) ≠ 0

pp: case h.hb
m : ℕ
hm : 0 < m
k p_k : ℕ
h_k : partialSum (↑m) k = ↑p_k / ↑(m ^ k !)
⊢ ↑(m ^ k !) ≠ 0

pp: case h.hd
m : ℕ
hm : 0 < m
k p_k : ℕ
h_k : partialSum (↑m) k = ↑p_k / ↑(m ^ k !)
⊢ ↑m ^ (k + 1)! ≠ 0

Tactic:
add_mul

Goal state after:
case h
m : ℕ
hm : 0 < m
k p_k : ℕ
h_k : partialSum (↑m) k = ↑p_k / ↑(m ^ k !)
⊢ ↑p_k * ↑m ^ (k + 1)! * ↑(m ^ (k + 1)!) + ↑(m ^ k !) * 1 * ↑(m ^ (k + 1)!) =
    ↑(p_k * m ^ ((k + 1)! - k !) + 1) * (↑(m ^ k !) * ↑m ^ (k + 1)!)

case h.hb
m : ℕ
hm : 0 < m
k p_k : ℕ
h_k : partialSum (↑m) k = ↑p_k / ↑(m ^ k !)
⊢ ↑(m ^ k !) * ↑m ^ (k + 1)! ≠ 0

case h.hd
m : ℕ
hm : 0 < m
k p_k : ℕ
h_k : partialSum (↑m) k = ↑p_k / ↑(m ^ k !)
⊢ ↑(m ^ (k + 1)!) ≠ 0

case h.hb
m : ℕ
hm : 0 < m
k p_k : ℕ
h_k : partialSum (↑m) k = ↑p_k / ↑(m ^ k !)
⊢ ↑(m ^ k !) ≠ 0

case h.hd
m : ℕ
hm : 0 < m
k p_k : ℕ
h_k : partialSum (↑m) k = ↑p_k / ↑(m ^ k !)
⊢ ↑m ^ (k + 1)! ≠ 0
Module: Mathlib.Topology.Instances.Irrational

Goal state before:
pp: x✝¹ : ℝ
x✝ : { x // Irrational x }
x : ℝ
hx : Irrational x
⊢ ⟨x, hx⟩ < ⟨x + ↑1, ⋯⟩

Tactic:
by simp

Goal state after:
Module: Mathlib.Topology.Instances.Irrational

Goal state before:
pp: x✝¹ : ℝ
x✝ : { x // Irrational x }
x : ℝ
hx : Irrational x
⊢ ⟨x - ↑1, ⋯⟩ < ⟨x, hx⟩

Tactic:
by simp

Goal state after:
Module: Mathlib.NumberTheory.RamificationInertia.Basic

Goal state before:
pp: R : Type u
inst✝¹⁷ : CommRing R
S : Type v
inst✝¹⁶ : CommRing S
inst✝¹⁵ : Algebra R S
inst✝¹⁴ : IsDedekindDomain S
K : Type u_1
L : Type u_2
inst✝¹³ : Field K
inst✝¹² : Field L
inst✝¹¹ : IsDedekindDomain R
inst✝¹⁰ : Algebra R K
inst✝⁹ : IsFractionRing R K
inst✝⁸ : Algebra S L
inst✝⁷ : IsFractionRing S L
inst✝⁶ : Algebra K L
inst✝⁵ : Algebra R L
inst✝⁴ : IsScalarTower R S L
inst✝³ : IsScalarTower R K L
inst✝² : Module.Finite R S
inst✝¹ : NoZeroSMulDivisors R S
p : Ideal R
inst✝ : p.IsMaximal
P : Ideal S
hP₁ : P.IsPrime
hP₂ : P.LiesOver p
⊢ p.ramificationIdx' P ≤ finrank K L

Tactic:
by_cases hp0 : p = ⊥

Goal state after:
case pos
R : Type u
inst✝¹⁷ : CommRing R
S : Type v
inst✝¹⁶ : CommRing S
inst✝¹⁵ : Algebra R S
inst✝¹⁴ : IsDedekindDomain S
K : Type u_1
L : Type u_2
inst✝¹³ : Field K
inst✝¹² : Field L
inst✝¹¹ : IsDedekindDomain R
inst✝¹⁰ : Algebra R K
inst✝⁹ : IsFractionRing R K
inst✝⁸ : Algebra S L
inst✝⁷ : IsFractionRing S L
inst✝⁶ : Algebra K L
inst✝⁵ : Algebra R L
inst✝⁴ : IsScalarTower R S L
inst✝³ : IsScalarTower R K L
inst✝² : Module.Finite R S
inst✝¹ : NoZeroSMulDivisors R S
p : Ideal R
inst✝ : p.IsMaximal
P : Ideal S
hP₁ : P.IsPrime
hP₂ : P.LiesOver p
hp0 : p = ⊥
⊢ p.ramificationIdx' P ≤ finrank K L

case neg
R : Type u
inst✝¹⁷ : CommRing R
S : Type v
inst✝¹⁶ : CommRing S
inst✝¹⁵ : Algebra R S
inst✝¹⁴ : IsDedekindDomain S
K : Type u_1
L : Type u_2
inst✝¹³ : Field K
inst✝¹² : Field L
inst✝¹¹ : IsDedekindDomain R
inst✝¹⁰ : Algebra R K
inst✝⁹ : IsFractionRing R K
inst✝⁸ : Algebra S L
inst✝⁷ : IsFractionRing S L
inst✝⁶ : Algebra K L
inst✝⁵ : Algebra R L
inst✝⁴ : IsScalarTower R S L
inst✝³ : IsScalarTower R K L
inst✝² : Module.Finite R S
inst✝¹ : NoZeroSMulDivisors R S
p : Ideal R
inst✝ : p.IsMaximal
P : Ideal S
hP₁ : P.IsPrime
hP₂ : P.LiesOver p
hp0 : ¬p = ⊥
⊢ p.ramificationIdx' P ≤ finrank K L
Module: Mathlib.NumberTheory.Wilson

Goal state before:
pp: case refine_1.left
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : 0 < p
a : (ZMod p)ˣ
ha : a ∈ univ
⊢ (↑a).val ≠ 0

Tactic:
rw [← @val_zero p]

Goal state after:
case refine_1.left
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : 0 < p
a : (ZMod p)ˣ
ha : a ∈ univ
⊢ (↑a).val ≠ val 0
Module: Mathlib.NumberTheory.Transcendental.Liouville.Measure

Goal state before:
pp: ⊢ volume (⋃ p, ⋃ (_ : 2 < p), {x | LiouvilleWith p x}) = 0

Tactic:
by
  simp only [← ofPred_exists, exists_prop]
  refine measure_mono_null setOfPred_liouvilleWith_subset_aux ?_
  rw [measure_iUnion_null_iff]; intro m; rw [measure_preimage_add_right]; clear m
  refine (measure_biUnion_null_iff <| to_countable _).2 fun n (hn : 1 ≤ n) => ?_
  generalize hr : (2 + 1 / n : ℝ) = r
  replace hr : 2 < r := by simp [← hr, zero_lt_one.trans_le hn]
  clear hn n
  refine measure_setOfPred_frequently_eq_zero ?_
  simp only [ofPred_exists, ← exists_prop, ← Real.dist_eq, ← mem_ball, ofPred_mem_eq]
  set B : ℤ → ℕ → Set ℝ := fun a b => ball (a / b) (1 / (b : ℝ) ^ r)
  have hB : ∀ a b, volume (B a b) = ↑((2 : ℝ≥0) / (b : ℝ≥0) ^ r) := fun a b ↦ by
    rw [Real.volume_ball, mul_one_div, ← NNReal.coe_two, ← NNReal.coe_natCast, ← NNReal.coe_rpow,
      ← NNReal.coe_div, ENNReal.ofReal_coe_nnreal]
  have : ∀ b : ℕ, volume (⋃ a ∈ Finset.Icc (0 : ℤ) b, B a b) ≤
      ↑(2 * ((b : ℝ≥0) ^ (1 - r) + (b : ℝ≥0) ^ (-r))) := fun b ↦
    calc
      volume (⋃ a ∈ Finset.Icc (0 : ℤ) b, B a b) ≤ ∑ a ∈ Finset.Icc (0 : ℤ) b, volume (B a b) :=
        measure_biUnion_finset_le _ _
      _ = ↑((b + 1) * (2 / (b : ℝ≥0) ^ r)) := by
        simp only [hB, Int.card_Icc, Finset.sum_const, nsmul_eq_mul, sub_zero,
          Int.toNat_natCast, ← Nat.cast_succ, ENNReal.coe_mul, ENNReal.coe_natCast]
      _ = _ := by
        have : 1 - r ≠ 0 := by linarith
        rw [ENNReal.coe_inj]
        simp [add_mul, div_eq_mul_inv, NNReal.rpow_neg, NNReal.rpow_sub' this, mul_add,
          mul_left_comm]
  refine ne_top_of_le_ne_top (ENNReal.tsum_coe_ne_top_iff_summable.2 ?_) (ENNReal.tsum_le_tsum this)
  refine (Summable.add ?_ ?_).mul_left _ <;> simp only [NNReal.summable_rpow] <;> linarith

Goal state after:
Module: Mathlib.Order.Category.Frm

Goal state before:
pp: X : Frm
x : ↑X
⊢ (ConcreteCategory.hom (𝟙 X)) x = x

Tactic:
by simp

Goal state after:
Module: Mathlib.Order.Category.Frm

Goal state before:
pp: X Y Z : Frm
f : X ⟶ Y
g : Y ⟶ Z
x : ↑X
⊢ (ConcreteCategory.hom (f ≫ g)) x = (ConcreteCategory.hom g) ((ConcreteCategory.hom f) x)

Tactic:
by simp

Goal state after:
Module: Mathlib.Order.Category.FinBddDistLat

Goal state before:
pp: X : FinBddDistLat
x : ↑X.toDistLat
⊢ (ConcreteCategory.hom (𝟙 X)) x = x

Tactic:
by simp

Goal state after:
Module: Mathlib.Order.Category.FinBddDistLat

Goal state before:
pp: X Y Z : FinBddDistLat
f : X ⟶ Y
g : Y ⟶ Z
x : ↑X.toDistLat
⊢ (ConcreteCategory.hom (f ≫ g)) x = (ConcreteCategory.hom g) ((ConcreteCategory.hom f) x)

Tactic:
by simp

Goal state after:
Module: Mathlib.Order.CompleteSublattice

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : CompleteLattice β
f : CompleteLatticeHom α β
L✝ : CompleteSublattice α
L : CompleteSublattice β
s : Set α
hs : s ⊆ ⇑f ⁻¹' ↑L
⊢ sInf s ∈ ⇑f ⁻¹' ↑L

Tactic:
by
    simpa only [mem_preimage, map_sInf, SetLike.mem_coe] using sInfClosed
      <| mapsTo_iff_image_subset.mp hs

Goal state after:
Module: Mathlib.Order.Completion

Goal state before:
pp: α : Type u_1
inst✝ : CompleteLattice α
A : DedekindCut α
⊢ principal (sSup A.left) = A

Tactic:
apply ext'

Goal state after:
α : Type u_1
inst✝ : CompleteLattice α
A : DedekindCut α
⊢ (principal (sSup A.left)).right = A.right
Module: Mathlib.Order.Completion

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : PartialOrder β
f : β ↪o α
x : β
⊢ sSup (⇑f '' (principal x).left) ≤ f x

Tactic:
by simp

Goal state after:
Module: Mathlib.Order.Concept

Goal state before:
pp: ι : Sort u_1
α : Type u_2
β : Type u_3
γ : Type u_4
κ : ι → Sort u_5
r : α → β → Prop
s : Set α
t : Set β
a : α
b : β
r' : α → α → Prop
c d : Concept α β r
c' : Concept α α r'
⊢ ∀ {x y : Concept α β r}, (⇑toDual ∘ intent) x ≤ (⇑toDual ∘ intent) y ↔ x ≤ y

Tactic:
by simp

Goal state after:
Module: Mathlib.Order.Concept

Goal state before:
pp: ι : Sort u_1
α : Type u_2
β : Type u_3
γ : Type u_4
κ : ι → Sort u_5
r : α → β → Prop
s : Set α
t : Set β
a : α
b : β
r' : α → α → Prop
c d : Concept α β r
c' : Concept α α r'
⊢ ∀ {x y : Concept α β r}, (⇑toDual ∘ intent) x < (⇑toDual ∘ intent) y ↔ x < y

Tactic:
by simp

Goal state after:
Module: Mathlib.Order.Completion

Goal state before:
pp: α : Type u_1
inst✝ : CompleteLattice α
A : DedekindCut α
⊢ sSup (⇑(RelIso.toRelEmbedding (OrderIso.refl α)) '' A.left) = sSup A.left

Tactic:
by simp

Goal state after:
Module: Mathlib.Order.CountableSupClosed

Goal state before:
pp: ι : Sort u_1
α : Type u_2
s : Set α
inst✝² : CompleteLattice α
inst✝¹ : Countable ι
inst✝ : Nonempty ι
hs : CountableSupClosed s
A : ι → α
hA : ∀ (n : ι), A n ∈ s
i₀ : ι := ⋯.some
⊢ A i₀ ∈ range A

Tactic:
by simp

Goal state after:
Module: Mathlib.Order.CountableSupClosed

Goal state before:
pp: α : Type u_2
s : Set α
inst✝ : SemilatticeSup α
hs : CountableSupClosed s
a : α
ha : a ∈ s
b : α
hb : b ∈ s
⊢ {a, b}.Nonempty

Tactic:
by simp

Goal state after:
Module: Mathlib.Order.CountableSupClosed

Goal state before:
pp: α : Type u_2
s : Set α
inst✝ : SemilatticeSup α
hs : CountableSupClosed s
a : α
ha : a ∈ s
b : α
hb : b ∈ s
⊢ {a, b}.Countable

Tactic:
by simp

Goal state after:
Module: Mathlib.Order.CountableSupClosed

Goal state before:
pp: α : Type u_2
inst✝ : LE α
x✝⁵ : Set α
x✝⁴ : x✝⁵ ⊆ univ
x✝³ : x✝⁵.Nonempty
x✝² : x✝⁵.Countable
x✝¹ : α
x✝ : IsLUB x✝⁵ x✝¹
⊢ x✝¹ ∈ univ

Tactic:
by simp

Goal state after:
Module: Mathlib.Order.CountableSupClosed

Goal state before:
pp: ι : Sort u_1
α : Type u_2
β : Type u_3
S : Set (Set α)
s✝ t : Set α
a b : α
inst✝ : Preorder α
s : Set α
x : α
hxs : x ∈ s
⊢ {x}.Nonempty

Tactic:
by simp

Goal state after:
Module: Mathlib.Order.CountableSupClosed

Goal state before:
pp: ι : Sort u_1
α : Type u_2
β : Type u_3
S : Set (Set α)
s✝ t : Set α
a b : α
inst✝ : Preorder α
s : Set α
x : α
hxs : x ∈ s
⊢ {x}.Countable

Tactic:
by simp

Goal state after: