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

Goal state before:
pp: case h
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp0' : 0 < ↑p
hp0 : 0 < (↑p)⁻¹
hp1' : 1 < ↑p
hp1 : (↑p)⁻¹ < 1
γ : (MonoidWithZeroHom.ofClass Valued.v).ValueGroup₀ˣ
x y : WithVal (Rat.padicValuation p)
h : padicNorm p ((WithVal.equiv (Rat.padicValuation p)) (x - y)) ≤ (↑(p ^ (embedding ↑γ * exp (-1)).log.natAbs))⁻¹
x' : ℚ := (WithVal.equiv (Rat.padicValuation p)) x
hx : x' = (WithVal.equiv (Rat.padicValuation p)) x
y' : ℚ := (WithVal.equiv (Rat.padicValuation p)) y
hy : y' = (WithVal.equiv (Rat.padicValuation p)) y
⊢ (Rat.padicValuation p) (x' - y') < embedding ↑γ

pp: case h
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp0' : 0 < ↑p
hp0 : 0 < (↑p)⁻¹
hp1' : 1 < ↑p
hp1 : (↑p)⁻¹ < 1
γ : (MonoidWithZeroHom.ofClass Valued.v).ValueGroup₀ˣ
x y : WithVal (Rat.padicValuation p)
h : ↑(padicNorm p ((WithVal.equiv (Rat.padicValuation p)) (x - y))) ≤ (↑↑(p ^ (embedding ↑γ * exp (-1)).log.natAbs))⁻¹
x' : ℚ := (WithVal.equiv (Rat.padicValuation p)) x
hx : x' = (WithVal.equiv (Rat.padicValuation p)) x
y' : ℚ := (WithVal.equiv (Rat.padicValuation p)) y
hy : y' = (WithVal.equiv (Rat.padicValuation p)) y
⊢ ↑(↑(p ^ (embedding ↑γ * exp (-1)).log.natAbs)).num ≠ 0

Tactic:
· change padicNorm p (x' - y') ≤ _ at h
      simp only [Rat.padicValuation, Valuation.coe_mk, MonoidWithZeroHom.coe_mk, ZeroHom.coe_mk,
        padicNorm, zpow_neg, Nat.cast_pow] at h ⊢
      split_ifs with H
      · simp only [exp_neg]
        exact embedding_unit_pos _
      · rw [← lt_log_iff_exp_lt (embedding_unit_ne_zero _)]
        simp_all [← zpow_natCast, zpow_pos, inv_le_inv₀, zpow_le_zpow_iff_right₀ hp1', abs_le,
          Int.lt_iff_add_one_le]

Goal state after:
case h
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp0' : 0 < ↑p
hp0 : 0 < (↑p)⁻¹
hp1' : 1 < ↑p
hp1 : (↑p)⁻¹ < 1
γ : (MonoidWithZeroHom.ofClass Valued.v).ValueGroup₀ˣ
x y : WithVal (Rat.padicValuation p)
h : ↑(padicNorm p ((WithVal.equiv (Rat.padicValuation p)) (x - y))) ≤ (↑↑(p ^ (embedding ↑γ * exp (-1)).log.natAbs))⁻¹
x' : ℚ := (WithVal.equiv (Rat.padicValuation p)) x
hx : x' = (WithVal.equiv (Rat.padicValuation p)) x
y' : ℚ := (WithVal.equiv (Rat.padicValuation p)) y
hy : y' = (WithVal.equiv (Rat.padicValuation p)) y
⊢ ↑(↑(p ^ (embedding ↑γ * exp (-1)).log.natAbs)).num ≠ 0
Module: Mathlib.NumberTheory.Padics.WithVal

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
⊢ IsDenseInducing ⇑((Rat.castHom ℚ_[p]).comp (WithVal.equiv (Rat.padicValuation p)).toRingHom)

Tactic:
refine Padic.isUniformInducing_cast_withVal.isDenseInducing ?_
  intro
  -- nhds_discrete causes timeouts on TC search
  simpa [-nhds_discrete] using Padic.denseRange_ratCast p _

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

Goal state before:
pp: case e'_4.e_f
X : Type u_1
Y : Type u_2
R : Type u_3
V : Type u_4
inst✝¹¹ : TopologicalSpace X
inst✝¹⁰ : TotallyDisconnectedSpace X
inst✝⁹ : T2Space X
inst✝⁸ : CompactSpace X
inst✝⁷ : TopologicalSpace Y
inst✝⁶ : CompactSpace Y
inst✝⁵ : AddCommGroup V
inst✝⁴ : UniformSpace V
inst✝³ : IsUniformAddGroup V
S : Set (V × V)
inst✝² : TopologicalSpace R
inst✝¹ : MonoidWithZero R
inst✝ : MulActionWithZero R V
f : C(X × Y, V)
hS : S ∈ 𝓤 V
hS' : {(f, g) | ∀ (y : Y), (f y, g y) ∈ S} ∈ 𝓤 C(Y, V)
n : ℕ
U : Fin n → TopologicalSpace.Clopens X
v : Fin n → C(Y, V)
hv : ∀ (x : X), (f.curry x, ∑ n, (↑(U n)).indicator (fun x ↦ v n) x) ∈ {(f, g) | ∀ (y : Y), (f y, g y) ∈ S}
x : X
y : Y
i : Fin n
⊢ { toFun := (↑(U i)).indicator fun x ↦ 1, continuous_toFun := ⋯ } x • (v i) y = ((↑(U i)).indicator (fun x ↦ v i) x) y

Tactic:
by_cases hi : x ∈ U i <;> simp [hi]

Goal state after:
Module: Mathlib.Topology.Separation.DisjointCover

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
S : Set (X × X)
inst✝ : CompactSpace X
hS : S ∈ 𝓝ˢ (diagonal X)
U : X → Set X
hUo : ∀ (x : X), IsOpen[inst✝¹] (U x)
hUx : ∀ (x : X), x ∈ U x
hUp : ∀ (x : X), U x ×ˢ U x ⊆ S
⊢ ∃ t U, IsOpenCover U ∧ ∀ (i : ↥t), ↑(U i) ×ˢ ↑(U i) ⊆ S

Tactic:
obtain ⟨t, ht⟩ := isCompact_univ.elim_finite_subcover _ hUo (fun x _ ↦ mem_iUnion.mpr ⟨_, hUx x⟩)

Goal state after:
X : Type u_1
inst✝¹ : TopologicalSpace X
S : Set (X × X)
inst✝ : CompactSpace X
hS : S ∈ 𝓝ˢ (diagonal X)
U : X → Set X
hUo : ∀ (x : X), IsOpen[inst✝¹] (U x)
hUx : ∀ (x : X), x ∈ U x
hUp : ∀ (x : X), U x ×ˢ U x ⊆ S
t : Finset X
ht : univ ⊆ ⋃ i ∈ t, U i
⊢ ∃ t U, IsOpenCover U ∧ ∀ (i : ↥t), ↑(U i) ×ˢ ↑(U i) ⊆ S
Module: Mathlib.NumberTheory.Padics.HeightOneSpectrum

Goal state before:
pp: R : Type u_2
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
inst✝² : Algebra R ℚ
inst✝¹ : IsFractionRing R ℚ
inst✝ : IsIntegralClosure R ℤ ℚ
p : Nat.Primes
x : ℤ_[↑p]
⊢ ↑((adicCompletionIntegersEquiv R p) x) = (adicCompletionEquiv R p) ↑x

Tactic:
by
  simp only [adicCompletionIntegersEquiv, ContinuousAlgEquiv.trans_apply,
    adicCompletionIntegers.coe_padicIntEquiv_symm_apply,
    adicCompletionEquiv, ContinuousAlgEquiv.trans_apply, ContinuousAlgEquiv.cast_apply,
    EmbeddingLike.apply_eq_iff_eq, Equiv.cast_apply, eq_cast_iff_heq]
  rw [← Subtype.heq_iff_coe_heq (by rw [primesEquiv.apply_symm_apply])
    (by rw [primesEquiv.apply_symm_apply])]
  exact cast_heq _ _

Goal state after:
Module: Mathlib.NumberTheory.PrimesCongruentOne

Goal state before:
pp: case inr
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
⊢ ∃ p, Prime p ∧ n < p ∧ p ≡ 1 [MOD k]

Tactic:
have hprime : Fact p.Prime := ⟨minFac_prime (ne_of_lt hgt).symm⟩

Goal state after:
case inr
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)
⊢ ∃ p, Prime p ∧ n < p ∧ p ≡ 1 [MOD k]
Module: Mathlib.NumberTheory.Pell

Goal state before:
pp: d : ℤ
a : Solution₁ d
ha : 1 < a.x
hy : a.y = 0
prop : a.x ^ 2 - 0 = 1
⊢ False

Tactic:
sub_zero

Goal state after:
d : ℤ
a : Solution₁ d
ha : 1 < a.x
hy : a.y = 0
prop : a.x ^ 2 = 1
⊢ False
Module: Mathlib.NumberTheory.Pell

Goal state before:
pp: d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
ξ : ℝ := √↑d
x : ℤ
hx : ξ = ↑x
⊢ √↑d ^ 2 = ξ * ξ

Tactic:
sq

Goal state after:
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
ξ : ℝ := √↑d
x : ℤ
hx : ξ = ↑x
⊢ √↑d * √↑d = ξ * ξ
Module: Mathlib.NumberTheory.Pell

Goal state before:
pp: case refine_1
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
ξ : ℝ := √↑d
hξ : Irrational ξ
M : ℤ
hM₁ : 2 * |ξ| + 1 < ↑M
hM : {q | |q.num ^ 2 - d * ↑q.den ^ 2| < M}.Infinite
m : ℤ
hm : {q | q.num ^ 2 - d * ↑q.den ^ 2 = m}.Infinite
this : NeZero m.natAbs
f : ℚ → ZMod m.natAbs × ZMod m.natAbs := fun q ↦ (↑q.num, ↑q.den)
q₁ : ℚ
h₁ : q₁.num ^ 2 - d * ↑q₁.den ^ 2 = m
q₂ : ℚ
h₂ : q₂.num ^ 2 - d * ↑q₂.den ^ 2 = m
hne : q₁ ≠ q₂
hqf : f q₁ = f q₂
hq1 : ↑q₁.num = ↑q₂.num
hq2 : ↑q₁.den = ↑q₂.den
hd₁ : m ∣ q₁.num * q₂.num - d * (↑q₁.den * ↑q₂.den)
hd₂ : m ∣ q₁.num * ↑q₂.den - q₂.num * ↑q₁.den
hm₀ : ↑m ≠ 0
⊢ ((q₁.num * q₂.num - d * (↑q₁.den * ↑q₂.den)) / m) ^ 2 - d * ((q₁.num * ↑q₂.den - q₂.num * ↑q₁.den) / m) ^ 2 = 1

Tactic:
qify [hd₁, hd₂]
    field_simp
    norm_cast
    grind

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 ∨ -a₁ ^ (n₂ * n₁) * a₁⁻¹ = 1
⊢ a₁ ^ n₂ = a₁

Tactic:
←
      zpow_neg_one,

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
⊢ Tendsto (fun n ↦ ‖(Polynomial.aeval a) (Polynomial.derivative F)‖ ^ 2 * T_gen p F a ^ 2 ^ n) atTop
    (𝓝 (‖(Polynomial.aeval a) (Polynomial.derivative F)‖ * 0))

Tactic:
sq

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
⊢ Tendsto
    (fun n ↦
      ‖(Polynomial.aeval a) (Polynomial.derivative F)‖ * ‖(Polynomial.aeval a) (Polynomial.derivative F)‖ *
        T_gen p F a ^ 2 ^ n)
    atTop (𝓝 (‖(Polynomial.aeval a) (Polynomial.derivative F)‖ * 0))
Module: Mathlib.NumberTheory.RatFunc.Ostrowski

Goal state before:
pp: case inl
K : Type u_1
Γ : Type u_2
inst✝⁴ : Field K
inst✝³ : LinearOrderedCommGroupWithZero Γ
v : Valuation K⟮X⟯ Γ
inst✝² : v.IsRankOneDiscrete
inst✝¹ : IsTrivialOn K v
inst✝ : DecidableEq K⟮X⟯
hlt : 1 < v X
hv : v.IsEquiv (inftyValuation K)
⊢ ¬∃! u, v.IsEquiv (valuation K⟮X⟯ u)

Tactic:
simp only [ExistsUnique, not_exists, not_and, not_forall]

Goal state after:
case inl
K : Type u_1
Γ : Type u_2
inst✝⁴ : Field K
inst✝³ : LinearOrderedCommGroupWithZero Γ
v : Valuation K⟮X⟯ Γ
inst✝² : v.IsRankOneDiscrete
inst✝¹ : IsTrivialOn K v
inst✝ : DecidableEq K⟮X⟯
hlt : 1 < v X
hv : v.IsEquiv (inftyValuation K)
⊢ ∀ (x : HeightOneSpectrum K[X]), v.IsEquiv (valuation K⟮X⟯ x) → ∃ x_1, ∃ (_ : v.IsEquiv (valuation K⟮X⟯ x_1)), ¬x_1 = x
Module: Mathlib.NumberTheory.SumTwoSquares

Goal state before:
pp: n : ℕ
hn : Squarefree n
⊢ IsSquare (-1) ↔ ∀ {q : ℕ}, q ∣ n → q % 4 ≠ 3

Tactic:
have help : ∀ a b : ZMod 4, a ≠ 3 → b ≠ 3 → a * b ≠ 3 := by decide

Goal state after:
n : ℕ
hn : Squarefree n
help : ∀ (a b : ZMod 4), a ≠ 3 → b ≠ 3 → a * b ≠ 3
⊢ IsSquare (-1) ↔ ∀ {q : ℕ}, q ∣ n → q % 4 ≠ 3
Module: Mathlib.NumberTheory.SumTwoSquares

Goal state before:
pp: case refine_3
n : ℕ
hn : Squarefree n
help : ∀ (a b : ZMod 4), a ≠ 3 → b ≠ 3 → a * b ≠ 3
H : ∀ q ∈ n.primeFactors, q % 4 ≠ 3
p q : ℕ
hpq : p * q ∣ n
hp : ¬↑p = ↑3
hq : ¬↑q = ↑3
⊢ ¬↑(p * q) = ↑3

Tactic:
Nat.cast_mul

Goal state after:
case refine_3
n : ℕ
hn : Squarefree n
help : ∀ (a b : ZMod 4), a ≠ 3 → b ≠ 3 → a * b ≠ 3
H : ∀ q ∈ n.primeFactors, q % 4 ≠ 3
p q : ℕ
hpq : p * q ∣ n
hp : ¬↑p = ↑3
hq : ¬↑q = ↑3
⊢ ¬↑p * ↑q = ↑3
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
⊢ ∀ (a b : ZMod 4), a ^ 2 + b ^ 2 ≠ ↑p

Tactic:
rw [← ZMod.natCast_mod p 4, hp3]; decide

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
p : Ideal R
P : Ideal S
hfp : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
i : ℕ
a : S
a_mem : a ∈ P ^ i
x y : S ⧸ P
⊢ p.quotientToQuotientRangePowQuotSuccAux P a_mem (x + y) =
    p.quotientToQuotientRangePowQuotSuccAux P a_mem x + p.quotientToQuotientRangePowQuotSuccAux P a_mem y

Tactic:
induction x, y using Quotient.inductionOn₂' with | _ x y

Goal state after:
case h
R : Type u
inst✝² : CommRing R
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
p : Ideal R
P : Ideal S
hfp : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
i : ℕ
a : S
a_mem : a ∈ P ^ i
x y : S
⊢ p.quotientToQuotientRangePowQuotSuccAux P a_mem (Quotient.mk'' x + Quotient.mk'' y) =
    p.quotientToQuotientRangePowQuotSuccAux P a_mem (Quotient.mk'' x) +
      p.quotientToQuotientRangePowQuotSuccAux P a_mem (Quotient.mk'' y)
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
p : Ideal R
P : Ideal S
hfp : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
i : ℕ
a : S
a_mem : a ∈ P ^ i
x : R ⧸ p
y : S ⧸ P
⊢ p.quotientToQuotientRangePowQuotSuccAux P a_mem (x • y) =
    (RingHom.id (R ⧸ p)) x • p.quotientToQuotientRangePowQuotSuccAux P a_mem y

Tactic:
induction x, y using Quotient.inductionOn₂' with | _ x y

Goal state after:
case h
R : Type u
inst✝² : CommRing R
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
p : Ideal R
P : Ideal S
hfp : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
i : ℕ
a : S
a_mem : a ∈ P ^ i
x : R
y : S
⊢ p.quotientToQuotientRangePowQuotSuccAux P a_mem (Quotient.mk'' x • Quotient.mk'' y) =
    (RingHom.id (R ⧸ p)) (Quotient.mk'' x) • p.quotientToQuotientRangePowQuotSuccAux P a_mem (Quotient.mk'' y)
Module: Mathlib.NumberTheory.Transcendental.Lindemann.AnalyticalPart

Goal state before:
pp: case e'_4.e'_6
f : ℕ → ℂ[X]
s : ℂ
c : ℝ
hc : ∀ (p : ℕ), ∀ x ∈ Set.Ioc 0 1, ‖eval (x • s) (f p)‖ ≤ c ^ p
p : ℕ
⊢ 1 = 1 - 0

Tactic:
sub_zero

Goal state after:
case e'_4.e'_6
f : ℕ → ℂ[X]
s : ℂ
c : ℝ
hc : ∀ (p : ℕ), ∀ x ∈ Set.Ioc 0 1, ‖eval (x • s) (f p)‖ ≤ c ^ p
p : ℕ
⊢ 1 = 1
Module: Mathlib.NumberTheory.Transcendental.Lindemann.AnalyticalPart

Goal state before:
pp: case hbc.convert_10
f : ℕ → ℂ[X]
s : ℂ
c : ℝ
hc : ∀ (p : ℕ), ∀ x ∈ Set.Ioc 0 1, ‖eval (x • s) (f p)‖ ≤ c ^ p
p : ℕ
⊢ ENNReal.ofReal (1 - 0) < ⊤

Tactic:
sub_zero

Goal state after:
case hbc.convert_10
f : ℕ → ℂ[X]
s : ℂ
c : ℝ
hc : ∀ (p : ℕ), ∀ x ∈ Set.Ioc 0 1, ‖eval (x • s) (f p)‖ ≤ c ^ p
p : ℕ
⊢ ENNReal.ofReal 1 < ⊤
Module: Mathlib.NumberTheory.Transcendental.Lindemann.AnalyticalPart

Goal state before:
pp: f : ℤ[X]
hf : eval 0 f ≠ 0
c' : ℂ → ℝ
c'0 : ∀ (s : ℂ), c' s ≥ 0
Pp'_le : ∀ (s : ℂ) (p : ℕ), p ≠ 0 → ‖P (map (algebraMap ℤ ℂ) (X ^ (p - 1) * f ^ p)) s‖ ≤ c' s ^ p
p : ℕ
p_gt : p > (eval 0 f).natAbs
prime_p : Nat.Prime p
gp' : ℤ[X]
h' :
  ∀ (r : ℤ) {p' : ℤ[X]},
    X ^ (p - 1) * f ^ p = (X - C r) ^ (p - 1) * p' →
      eval r (sumIDeriv (X ^ (p - 1) * f ^ p)) = (p - 1)! • eval r p' + p ! • eval r gp'
⊢ X ^ (p - 1) * f ^ p = (X - 0) ^ (p - 1) * ?m.190

Tactic:
sub_zero

Goal state after:
f : ℤ[X]
hf : eval 0 f ≠ 0
c' : ℂ → ℝ
c'0 : ∀ (s : ℂ), c' s ≥ 0
Pp'_le : ∀ (s : ℂ) (p : ℕ), p ≠ 0 → ‖P (map (algebraMap ℤ ℂ) (X ^ (p - 1) * f ^ p)) s‖ ≤ c' s ^ p
p : ℕ
p_gt : p > (eval 0 f).natAbs
prime_p : Nat.Prime p
gp' : ℤ[X]
h' :
  ∀ (r : ℤ) {p' : ℤ[X]},
    X ^ (p - 1) * f ^ p = (X - C r) ^ (p - 1) * p' →
      eval r (sumIDeriv (X ^ (p - 1) * f ^ p)) = (p - 1)! • eval r p' + p ! • eval r gp'
⊢ X ^ (p - 1) * f ^ p = X ^ (p - 1) * ?m.190
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
p : Ideal R
P✝ : Ideal S
inst✝² : IsDedekindDomain S
inst✝¹ : Module.Finite R S
inst✝ : p.IsMaximal
P : ↥(factors (map f p)).toFinset
⊢ FiniteDimensional (R ⧸ p) (S ⧸ ↑P ^ p.ramificationIdx' ↑P)

Tactic:
refine .of_finrank_pos ?_
  rw [pos_iff_ne_zero, Factors.finrank_pow_ramificationIdx]
  exact mul_ne_zero (Factors.ramificationIdx_ne_zero p P) (inertiaDeg'_pos p P.1).ne'

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

Goal state before:
pp: x : ℝ
hx : Irrational x
n : ℕ
A : IsClosed (range fun m ↦ (↑n)⁻¹ * ↑m)
B : x ∉ range fun m ↦ (↑n)⁻¹ * ↑m
ε : ℝ
ε0 : ε > 0
hε : ball x ε ⊆ (range fun m ↦ (↑n)⁻¹ * ↑m)ᶜ
δ : ℝ
hδ : δ ≤ ε
m : ℤ
hlt : dist x (↑m / ↑n) < δ
⊢ False

Tactic:
dist_comm

Goal state after:
x : ℝ
hx : Irrational x
n : ℕ
A : IsClosed (range fun m ↦ (↑n)⁻¹ * ↑m)
B : x ∉ range fun m ↦ (↑n)⁻¹ * ↑m
ε : ℝ
ε0 : ε > 0
hε : ball x ε ⊆ (range fun m ↦ (↑n)⁻¹ * ↑m)ᶜ
δ : ℝ
hδ : δ ≤ ε
m : ℤ
hlt : dist (↑m / ↑n) x < δ
⊢ False
Module: Mathlib.NumberTheory.Transcendental.Liouville.Measure

Goal state before:
pp: ⊢ ∀ᵐ (x : ℝ), ∀ p > 2, ¬LiouvilleWith p x

Tactic:
by
  simpa only [ae_iff, not_forall, Classical.not_not, ofPred_exists] using
    volume_iUnion_setOfPred_liouvilleWith

Goal state after:
Module: Mathlib.NumberTheory.WellApproximable

Goal state before:
pp: A : Type u_1
inst✝ : SeminormedCommGroup A
a : A
n : ℕ
δ : ℝ
b : A
hn : 0 < orderOf b
han : orderOf a ^ 2 ∣ orderOf b
hb : orderOf b = n
⊢ orderOf (a * b) = n

Tactic:
sq

Goal state after:
A : Type u_1
inst✝ : SeminormedCommGroup A
a : A
n : ℕ
δ : ℝ
b : A
hn : 0 < orderOf b
han : orderOf a * orderOf a ∣ orderOf b
hb : orderOf b = n
⊢ orderOf (a * b) = n
Module: Mathlib.Order.Comparable

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
a b : α
⊢ a < b ∨ AntisymmRel (fun x1 x2 ↦ x1 ≤ x2) a b ∨ b < a ∨ IncompRel (fun x1 x2 ↦ x1 ≤ x2) a b

Tactic:
simp_rw [lt_iff_le_not_ge]
  tauto

Goal state after:
Module: Mathlib.Order.CompleteSublattice

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : CompleteLattice β
f : CompleteLatticeHom α β
carrier : Set α
sSupClosed' : ∀ ⦃s : Set α⦄, s ⊆ carrier → sSup s ∈ carrier
sInfClosed' : ∀ ⦃s : Set α⦄, s ⊆ carrier → sInf s ∈ carrier
x : α
hx : x ∈ carrier
y : α
hy : y ∈ carrier
this : x ⊔ y = sSup {x, y}
⊢ x ⊔ y ∈ carrier

Tactic:
exact this ▸ sSupClosed' (fun z hz ↦ by aesop)

Goal state after:
Module: Mathlib.Order.Completion

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
a : α
c : DedekindCut α
⊢ principal a ≤ c ↔ a ∈ c.left

Tactic:
simp only [← extent_subset_extent_iff, left_principal]

Goal state after:
α : Type u_1
inst✝ : Preorder α
a : α
c : DedekindCut α
⊢ Iic a ⊆ c.extent ↔ a ∈ c.left
Module: Mathlib.Order.Extension.Linear

Goal state before:
pp: α : Type u
r : α → α → Prop
inst✝ : IsPartialOrder α r
S : Set (α → α → Prop) := {s | IsPartialOrder α s}
hS : ∀ c ⊆ S, IsChain (fun x1 x2 ↦ x1 ≤ x2) c → ∀ y ∈ c, ∃ ub ∈ S, ∀ z ∈ c, z ≤ ub
s : α → α → Prop
hrs : r ≤ s
hs : Maximal (fun x ↦ x ∈ S) s
⊢ ∃ s, IsLinearOrder α s ∧ r ≤ s

Tactic:
have : IsPartialOrder α s := hs.prop

Goal state after:
α : Type u
r : α → α → Prop
inst✝ : IsPartialOrder α r
S : Set (α → α → Prop) := {s | IsPartialOrder α s}
hS : ∀ c ⊆ S, IsChain (fun x1 x2 ↦ x1 ≤ x2) c → ∀ y ∈ c, ∃ ub ∈ S, ∀ z ∈ c, z ≤ ub
s : α → α → Prop
hrs : r ≤ s
hs : Maximal (fun x ↦ x ∈ S) s
this : IsPartialOrder α s
⊢ ∃ s, IsLinearOrder α s ∧ r ≤ s
Module: Mathlib.NumberTheory.WellApproximable

Goal state before:
pp: T : ℝ
hT : Fact (0 < T)
δ : ℕ → ℝ
hδ : Tendsto δ atTop (𝓝 0)
this : SemilatticeSup Nat.Primes := Nat.Subtype.semilatticeSup fun p ↦ Nat.Prime p
μ : Measure 𝕊 := volume
u : Nat.Primes → 𝕊 := fun p ↦ ↑(↑1 / ↑↑p * T)
hu₀ : ∀ (p : Nat.Primes), addOrderOf (u p) = ↑p
hu : Tendsto (addOrderOf ∘ u) atTop atTop
E : Set 𝕊 := addWellApproximable 𝕊 δ
X : ℕ → Set 𝕊 := fun n ↦ approxAddOrderOf 𝕊 n (δ n)
A : ℕ → Set 𝕊 := fun p ↦ blimsup X atTop fun n ↦ 0 < n ∧ ¬p ∣ n
B : ℕ → Set 𝕊 := fun p ↦ blimsup X atTop fun n ↦ 0 < n ∧ p ∣ n ∧ ¬p * p ∣ n
C : ℕ → Set 𝕊 := fun p ↦ blimsup X atTop fun n ↦ 0 < n ∧ p ^ 2 ∣ n
hA₀ : ∀ (p : ℕ), MeasurableSet (A p)
hB₀ : ∀ (p : ℕ), MeasurableSet (B p)
hE₀ : NullMeasurableSet E μ
hE₁ : ∀ (p : ℕ), E = A p ∪ B p ∪ C p
hE₂ : ∀ (p : Nat.Primes), A ↑p =ᵐ[μ] ∅ ∧ B ↑p =ᵐ[μ] ∅ → E =ᵐ[μ] C ↑p
hA : ∀ (p : Nat.Primes), A ↑p =ᵐ[μ] ∅ ∨ A ↑p =ᵐ[μ] univ
hB : ∀ (p : Nat.Primes), B ↑p =ᵐ[μ] ∅ ∨ B ↑p =ᵐ[μ] univ
hC : ∀ (p : Nat.Primes), u p +ᵥ C ↑p = C ↑p
h : ∀ (p : Nat.Primes), A ↑p =ᵐ[μ] ∅ ∧ B ↑p =ᵐ[μ] ∅
p : Nat.Primes
⊢ u p +ᵥ E =ᵐ[μ] E

Tactic:
replace hE₂ : E =ᵐ[μ] C p := hE₂ p (h p)

Goal state after:
T : ℝ
hT : Fact (0 < T)
δ : ℕ → ℝ
hδ : Tendsto δ atTop (𝓝 0)
this : SemilatticeSup Nat.Primes := Nat.Subtype.semilatticeSup fun p ↦ Nat.Prime p
μ : Measure 𝕊 := volume
u : Nat.Primes → 𝕊 := fun p ↦ ↑(↑1 / ↑↑p * T)
hu₀ : ∀ (p : Nat.Primes), addOrderOf (u p) = ↑p
hu : Tendsto (addOrderOf ∘ u) atTop atTop
E : Set 𝕊 := addWellApproximable 𝕊 δ
X : ℕ → Set 𝕊 := fun n ↦ approxAddOrderOf 𝕊 n (δ n)
A : ℕ → Set 𝕊 := fun p ↦ blimsup X atTop fun n ↦ 0 < n ∧ ¬p ∣ n
B : ℕ → Set 𝕊 := fun p ↦ blimsup X atTop fun n ↦ 0 < n ∧ p ∣ n ∧ ¬p * p ∣ n
C : ℕ → Set 𝕊 := fun p ↦ blimsup X atTop fun n ↦ 0 < n ∧ p ^ 2 ∣ n
hA₀ : ∀ (p : ℕ), MeasurableSet (A p)
hB₀ : ∀ (p : ℕ), MeasurableSet (B p)
hE₀ : NullMeasurableSet E μ
hE₁ : ∀ (p : ℕ), E = A p ∪ B p ∪ C p
hA : ∀ (p : Nat.Primes), A ↑p =ᵐ[μ] ∅ ∨ A ↑p =ᵐ[μ] univ
hB : ∀ (p : Nat.Primes), B ↑p =ᵐ[μ] ∅ ∨ B ↑p =ᵐ[μ] univ
hC : ∀ (p : Nat.Primes), u p +ᵥ C ↑p = C ↑p
h : ∀ (p : Nat.Primes), A ↑p =ᵐ[μ] ∅ ∧ B ↑p =ᵐ[μ] ∅
p : Nat.Primes
hE₂ : E =ᵐ[μ] C ↑p
⊢ u p +ᵥ E =ᵐ[μ] E
Module: Mathlib.Order.PrimeIdeal

Goal state before:
pp: P : Type u_1
inst✝¹ : DistribLattice P
I : Ideal P
inst✝ : I.IsMaximal
x y : P
hx : x ∉ I
hynI : y ∉ I
hxy : x ⊓ y ∈ I
J : Ideal P := I ⊔ principal x
hJuniv : ↑J = Set.univ
a : P
ha : a ∈ I
b : P
hb : b ∈ principal x
hy : y = a ⊔ b
⊢ y ∈ I

Tactic:
rw [hy]

Goal state after:
P : Type u_1
inst✝¹ : DistribLattice P
I : Ideal P
inst✝ : I.IsMaximal
x y : P
hx : x ∉ I
hynI : y ∉ I
hxy : x ⊓ y ∈ I
J : Ideal P := I ⊔ principal x
hJuniv : ↑J = Set.univ
a : P
ha : a ∈ I
b : P
hb : b ∈ principal x
hy : y = a ⊔ b
⊢ a ⊔ b ∈ I
Module: Mathlib.Order.PrimeIdeal

Goal state before:
pp: P : Type u_1
inst✝¹ : DistribLattice P
I : Ideal P
inst✝ : I.IsMaximal
x y : P
hx : x ∉ I
hynI : y ∉ I
hxy : x ⊓ y ∈ I
J : Ideal P := I ⊔ principal x
hJuniv : ↑J = Set.univ
a : P
ha : a ∈ I
b : P
hb : b ∈ principal x
hy : y = a ⊔ b
⊢ b ≤ y

Tactic:
rw [hy]

Goal state after:
P : Type u_1
inst✝¹ : DistribLattice P
I : Ideal P
inst✝ : I.IsMaximal
x y : P
hx : x ∉ I
hynI : y ∉ I
hxy : x ⊓ y ∈ I
J : Ideal P := I ⊔ principal x
hJuniv : ↑J = Set.univ
a : P
ha : a ∈ I
b : P
hb : b ∈ principal x
hy : y = a ⊔ b
⊢ b ≤ a ⊔ b
Module: Mathlib.Order.Nucleus

Goal state before:
pp: X : Type u_1
inst✝ : Frame X
n : Nucleus X
x : X
⊢ x ∈ range ⇑n → n x = x

Tactic:
rintro ⟨x, rfl⟩; exact idempotent _

Goal state after:
Module: Mathlib.Order.SaddlePoint

Goal state before:
pp: E : Type u_1
F : Type u_2
β : Type u_3
X : Set E
Y : Set F
f : E → F → β
inst✝ : CompleteLinearOrder β
a : E
ha : a ∈ X
b : F
hb : b ∈ Y
⊢ IsSaddlePointOn X Y f a b ↔ ⨆ y ∈ Y, f a y = f a b ∧ ⨅ x ∈ X, f x b = f a b

Tactic:
refine ⟨fun h ↦ ⟨?_, ?_⟩, fun ⟨h, h'⟩ x hx y hy ↦ ?_⟩

Goal state after:
case refine_1
E : Type u_1
F : Type u_2
β : Type u_3
X : Set E
Y : Set F
f : E → F → β
inst✝ : CompleteLinearOrder β
a : E
ha : a ∈ X
b : F
hb : b ∈ Y
h : IsSaddlePointOn X Y f a b
⊢ ⨆ y ∈ Y, f a y = f a b

case refine_2
E : Type u_1
F : Type u_2
β : Type u_3
X : Set E
Y : Set F
f : E → F → β
inst✝ : CompleteLinearOrder β
a : E
ha : a ∈ X
b : F
hb : b ∈ Y
h : IsSaddlePointOn X Y f a b
⊢ ⨅ x ∈ X, f x b = f a b

case refine_3
E : Type u_1
F : Type u_2
β : Type u_3
X : Set E
Y : Set F
f : E → F → β
inst✝ : CompleteLinearOrder β
a : E
ha : a ∈ X
b : F
hb : b ∈ Y
x✝ : ⨆ y ∈ Y, f a y = f a b ∧ ⨅ x ∈ X, f x b = f a b
x : E
hx : x ∈ X
y : F
hy : y ∈ Y
h : ⨆ y ∈ Y, f a y = f a b
h' : ⨅ x ∈ X, f x b = f a b
⊢ f a y ≤ f x b
Module: Mathlib.Order.Partition.Basic

Goal state before:
pp: α : Type u_1
x y : α
u : Set α
P : Partition u
hx : x ∈ u
hy : y ∈ u
⊢ P.Rel x y ↔ P.partOf x = P.partOf y

Tactic:
refine ⟨fun ⟨t, htP, hxt, hyt⟩ ↦ eq_partOf_of_mem (P.partOf_mem hx) ?_,
    fun h ↦ ⟨P.partOf x, P.partOf_mem hx, P.mem_partOf hx, h ▸ mem_partOf hy⟩⟩
  rwa [← eq_partOf_of_mem htP hxt]

Goal state after:
Module: Mathlib.Order.SuccPred.Tree

Goal state before:
pp: α : Type u_1
inst✝⁴ : PartialOrder α
inst✝³ : PredOrder α
inst✝² : IsPredArchimedean α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
r : α
hr : r ≠ ⊥
⊢ IsAtom (findAtom r)

Tactic:
by
  constructor
  · simp [hr]
  · intro b hb
    apply Order.le_pred_of_lt at hb
    simpa using hb

Goal state after:
Module: Mathlib.Probability.Process.Adapted

Goal state before:
pp: Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst✝³ : Preorder ι
β : ι → Type u_3
inst✝² : (i : ι) → TopologicalSpace (β i)
u : (i : ι) → Ω → β i
inst✝¹ : ∀ (i : ι), MetrizableSpace (β i)
mβ : (i : ι) → MeasurableSpace (β i)
inst✝ : ∀ (i : ι), BorelSpace (β i)
hum : ∀ (i : ι), StronglyMeasurable (u i)
⊢ StronglyAdapted (natural u hum) u

Tactic:
intro i
  refine StronglyMeasurable.mono ?_ (le_iSup₂_of_le i (le_refl i) le_rfl)
  rw [stronglyMeasurable_iff_measurable_separable]
  exact ⟨measurable_iff_comap_le.2 le_rfl, (hum i).isSeparable_range⟩

Goal state after: