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

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
hp0' : 0 < ↑p
hp0 : 0 < (↑p)⁻¹
hp1' : 1 < ↑p
hp1 : (↑p)⁻¹ < 1
⊢ IsUniformInducing ⇑((Rat.castHom ℚ_[p]).comp (WithVal.equiv (Rat.padicValuation p)).toRingHom)

Tactic:
rw [Filter.HasBasis.isUniformInducing_iff (Valued.hasBasis_uniformity _ _)
    (Metric.uniformity_basis_dist_le_pow hp0 hp1)]

Goal state after:
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp0' : 0 < ↑p
hp0 : 0 < (↑p)⁻¹
hp1' : 1 < ↑p
hp1 : (↑p)⁻¹ < 1
⊢ (∀ (i : ℕ),
      True →
        ∃ j,
          True ∧
            ∀ (x y : WithVal (Rat.padicValuation p)),
              (x, y) ∈ {p_1 | Valued.v.restrict (p_1.2 - p_1.1) < ↑j} →
                (((Rat.castHom ℚ_[p]).comp (WithVal.equiv (Rat.padicValuation p)).toRingHom) x,
                    ((Rat.castHom ℚ_[p]).comp (WithVal.equiv (Rat.padicValuation p)).toRingHom) y) ∈
                  {p_1 | dist p_1.1 p_1.2 ≤ (↑p)⁻¹ ^ i}) ∧
    ∀ (j : (MonoidWithZeroHom.ofClass Valued.v).ValueGroup₀ˣ),
      True →
        ∃ i,
          True ∧
            ∀ (x y : WithVal (Rat.padicValuation p)),
              (((Rat.castHom ℚ_[p]).comp (WithVal.equiv (Rat.padicValuation p)).toRingHom) x,
                    ((Rat.castHom ℚ_[p]).comp (WithVal.equiv (Rat.padicValuation p)).toRingHom) y) ∈
                  {p_1 | dist p_1.1 p_1.2 ≤ (↑p)⁻¹ ^ i} →
                (x, y) ∈ {p_1 | Valued.v.restrict (p_1.2 - p_1.1) < ↑j}
Module: Mathlib.NumberTheory.Padics.MahlerBasis

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : Module ℤ_[p] E
inst✝² : IsBoundedSMul ℤ_[p] E
inst✝¹ : IsUltrametricDist E
inst✝ : CompleteSpace E
a : ℕ → E
ha : Tendsto a atTop (𝓝 0)
⊢ HasSum (fun n ↦ mahlerTerm (a n) n) (mahlerSeries a)

Tactic:
refine (NonarchimedeanAddGroup.summable_of_tendsto_cofinite_zero ?_).hasSum

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : Module ℤ_[p] E
inst✝² : IsBoundedSMul ℤ_[p] E
inst✝¹ : IsUltrametricDist E
inst✝ : CompleteSpace E
a : ℕ → E
ha : Tendsto a atTop (𝓝 0)
⊢ Tendsto (fun n ↦ mahlerTerm (a n) n) cofinite (𝓝 0)
Module: Mathlib.NumberTheory.Padics.MahlerBasis

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : Module ℤ_[p] E
inst✝² : IsBoundedSMul ℤ_[p] E
inst✝¹ : IsUltrametricDist E
inst✝ : CompleteSpace E
a : ℕ → E
ha : Tendsto a atTop (𝓝 0)
⊢ HasSum (fun n ↦ mahlerTerm (a n) n) (mahlerSeries a)

Tactic:
by
  refine (NonarchimedeanAddGroup.summable_of_tendsto_cofinite_zero ?_).hasSum
  rw [tendsto_zero_iff_norm_tendsto_zero] at ha ⊢
  simpa only [norm_mahlerTerm, Nat.cofinite_eq_atTop] using ha

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

Goal state before:
pp: x : 𝓞 ℚ
⊢ (intEquiv (𝓞 ℚ)) x = ringOfIntegersEquiv x

Tactic:
by
  simp [intEquiv, RingOfIntegers.equiv, IsIntegralClosure.equiv, IsIntegralClosure.lift,
    IsIntegralClosure.mk']

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

Goal state before:
pp: X : Type u_1
V : Type u_2
inst✝⁴ : TopologicalSpace X
inst✝³ : TopologicalSpace V
inst✝² : TotallyDisconnectedSpace X
inst✝¹ : T2Space X
inst✝ : CompactSpace X
S : Set (V × V)
f : C(X, V)
hS : S ∈ 𝓝ˢ (diagonal V)
n : ℕ
E : Fin n → Clopens X
hEne : ∀ (i : Fin n), E i ≠ ⊥
hES : ∀ (i : Fin n), ∀ y ∈ E i, ∀ z ∈ E i, (f y, f z) ∈ S
hEuniv : univ ⊆ ⋃ i, ↑(E i)
hEdis : Pairwise (Disjoint on E)
g : X → Fin n
hg : ∀ (x : X), (fun i ↦ x ∈ E i) (g x)
hg' : ∀ (x : X) (y : Fin n), (fun i ↦ x ∈ E i) y → y = g x
r : Fin n → X
hr : ∀ (i : Fin n), r i ∈ E i
⊢ ∃ n g h, Continuous[inst✝⁴, _] g ∧ ∀ (x : X), (f x, h (g x)) ∈ S

Tactic:
refine ⟨n, g, f ∘ r, continuous_discrete_rng.mpr fun j ↦ ?_, fun x ↦ (hES _) _ (hg _) _ (hr _)⟩

Goal state after:
X : Type u_1
V : Type u_2
inst✝⁴ : TopologicalSpace X
inst✝³ : TopologicalSpace V
inst✝² : TotallyDisconnectedSpace X
inst✝¹ : T2Space X
inst✝ : CompactSpace X
S : Set (V × V)
f : C(X, V)
hS : S ∈ 𝓝ˢ (diagonal V)
n : ℕ
E : Fin n → Clopens X
hEne : ∀ (i : Fin n), E i ≠ ⊥
hES : ∀ (i : Fin n), ∀ y ∈ E i, ∀ z ∈ E i, (f y, f z) ∈ S
hEuniv : univ ⊆ ⋃ i, ↑(E i)
hEdis : Pairwise (Disjoint on E)
g : X → Fin n
hg : ∀ (x : X), (fun i ↦ x ∈ E i) (g x)
hg' : ∀ (x : X) (y : Fin n), (fun i ↦ x ∈ E i) y → y = g x
r : Fin n → X
hr : ∀ (i : Fin n), r i ∈ E i
j : Fin n
⊢ IsOpen[inst✝⁴] (g ⁻¹' {j})
Module: Mathlib.NumberTheory.Pell

Goal state before:
pp: d : ℤ
a : Solution₁ d
hax : 0 < a.x
hay : 0 < a.y
n : ℤ
hn : 0 < n
⊢ 0 < (a ^ n).y

Tactic:
by
  lift n to ℕ using hn.le
  norm_cast at hn ⊢
  rw [← Nat.succ_pred_eq_of_pos hn]
  exact y_pow_succ_pos hax hay _

Goal state after:
Module: Mathlib.NumberTheory.Pell

Goal state before:
pp: d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
x y : ℤ
prop : x ^ 2 - d * y ^ 2 = 1
hy : y ≠ 0
⊢ ∃ a, a ≠ 1 ∧ a ≠ -1

Tactic:
refine ⟨mk x y prop, fun H => ?_, fun H => ?_⟩ <;> apply_fun Solution₁.y at H

Goal state after:
case refine_1
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
x y : ℤ
prop : x ^ 2 - d * y ^ 2 = 1
hy : y ≠ 0
H : (mk x y prop).y = Solution₁.y 1
⊢ False

case refine_2
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
x y : ℤ
prop : x ^ 2 - d * y ^ 2 = 1
hy : y ≠ 0
H : (mk x y prop).y = (-1).y
⊢ False
Module: Mathlib.NumberTheory.Pell

Goal state before:
pp: case h.inr
d : ℤ
a₁ : Solution₁ d
h : IsFundamental a₁
x : ℕ
ih : ∀ m < x, ∀ {a : Solution₁ d}, 0 ≤ a.y → ↑m = a.x → 0 < ↑m → ∃ n, a = a₁ ^ n
a : Solution₁ d
hay : 0 ≤ a.y
hax' : ↑x = a.x
hax : 0 < ↑x
hy : 0 < a.y
hx₁ : 1 < a.x
⊢ ∃ n, a = a₁ ^ n

Tactic:
have hxx₁ := h.mul_inv_x_pos hx₁ hy

Goal state after:
case h.inr
d : ℤ
a₁ : Solution₁ d
h : IsFundamental a₁
x : ℕ
ih : ∀ m < x, ∀ {a : Solution₁ d}, 0 ≤ a.y → ↑m = a.x → 0 < ↑m → ∃ n, a = a₁ ^ n
a : Solution₁ d
hay : 0 ≤ a.y
hax' : ↑x = a.x
hax : 0 < ↑x
hy : 0 < a.y
hx₁ : 1 < a.x
hxx₁ : 0 < (a * a₁⁻¹).x
⊢ ∃ n, a = a₁ ^ n
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 : ℕ
⊢ 2 ≤ 2 ^ (n + 1)

Tactic:
have := pow_right_mono₀ (by simp : 1 ≤ 2) (Nat.le_add_left _ _ : 1 ≤ n + 1)
    simpa using this

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

Goal state before:
pp: case refine_4
A : Type u_1
K : Type u_2
L : Type u_3
B : Type u_4
inst✝³⁹ : Field K
inst✝³⁸ : Field L
inst✝³⁷ : Algebra K L
inst✝³⁶ : CommRing A
inst✝³⁵ : CommRing B
inst✝³⁴ : Algebra A B
p : Ideal A
P : Ideal B
inst✝³³ : P.LiesOver p
inst✝³² : Algebra A K
inst✝³¹ : IsFractionRing A K
inst✝³⁰ : Algebra A L
inst✝²⁹ : IsScalarTower A K L
inst✝²⁸ : Algebra B L
inst✝²⁷ : IsScalarTower A B L
inst✝²⁶ : IsFractionRing B L
inst✝²⁵ : MulSemiringAction Gal(L/K) B
inst✝²⁴ : SMulDistribClass Gal(L/K) B L
D : Type u_5
𝓞D : Type u_6
inst✝²³ : Field D
inst✝²² : Algebra D L
inst✝²¹ : IsDecompositionField K L P D
inst✝²⁰ : CommRing 𝓞D
inst✝¹⁹ : Algebra 𝓞D D
inst✝¹⁸ : IsFractionRing 𝓞D D
inst✝¹⁷ : Algebra 𝓞D B
inst✝¹⁶ : Algebra 𝓞D L
inst✝¹⁵ : IsScalarTower 𝓞D D L
inst✝¹⁴ : IsScalarTower 𝓞D B L
𝓟D : Ideal 𝓞D
hD : P.LiesOver 𝓟D
inst✝¹³ : IsGalois K L
inst✝¹² : IsDedekindDomain A
inst✝¹¹ : IsDedekindDomain B
inst✝¹⁰ : Module.Finite A B
inst✝⁹ : Module.IsTorsionFree A B
inst✝⁸ : Algebra A 𝓞D
inst✝⁷ : Module.Finite A 𝓞D
inst✝⁶ : IsScalarTower A 𝓞D B
inst✝⁵ : IsDedekindDomain 𝓞D
inst✝⁴ : 𝓟D.LiesOver p
inst✝³ : FiniteDimensional K L
inst✝² : Ring.HasFiniteQuotients A
inst✝¹ : 𝓟D.IsMaximal
inst✝ : P.IsMaximal
hp : p ≠ ⊥
left✝⁴ : Module.Finite 𝓞D B
left✝³ : Module.IsTorsionFree 𝓞D B
left✝² : Module.IsTorsionFree A 𝓞D
left✝¹ : IsGaloisGroup Gal(L/K) A B
left✝ : IsGaloisGroup (↥(stabilizer Gal(L/K) P)) 𝓞D B
h𝓟 : 𝓟D ≠ ⊥
⊢ 𝓟D.inertiaDegIn B ≤ p.inertiaDegIn B

Tactic:
rw [inertiaDegIn_eq_inertiaDeg p P Gal(L/K),
      inertiaDegIn_eq_inertiaDeg _ P (stabilizer Gal(L/K) P)]

Goal state after:
case refine_4
A : Type u_1
K : Type u_2
L : Type u_3
B : Type u_4
inst✝³⁹ : Field K
inst✝³⁸ : Field L
inst✝³⁷ : Algebra K L
inst✝³⁶ : CommRing A
inst✝³⁵ : CommRing B
inst✝³⁴ : Algebra A B
p : Ideal A
P : Ideal B
inst✝³³ : P.LiesOver p
inst✝³² : Algebra A K
inst✝³¹ : IsFractionRing A K
inst✝³⁰ : Algebra A L
inst✝²⁹ : IsScalarTower A K L
inst✝²⁸ : Algebra B L
inst✝²⁷ : IsScalarTower A B L
inst✝²⁶ : IsFractionRing B L
inst✝²⁵ : MulSemiringAction Gal(L/K) B
inst✝²⁴ : SMulDistribClass Gal(L/K) B L
D : Type u_5
𝓞D : Type u_6
inst✝²³ : Field D
inst✝²² : Algebra D L
inst✝²¹ : IsDecompositionField K L P D
inst✝²⁰ : CommRing 𝓞D
inst✝¹⁹ : Algebra 𝓞D D
inst✝¹⁸ : IsFractionRing 𝓞D D
inst✝¹⁷ : Algebra 𝓞D B
inst✝¹⁶ : Algebra 𝓞D L
inst✝¹⁵ : IsScalarTower 𝓞D D L
inst✝¹⁴ : IsScalarTower 𝓞D B L
𝓟D : Ideal 𝓞D
hD : P.LiesOver 𝓟D
inst✝¹³ : IsGalois K L
inst✝¹² : IsDedekindDomain A
inst✝¹¹ : IsDedekindDomain B
inst✝¹⁰ : Module.Finite A B
inst✝⁹ : Module.IsTorsionFree A B
inst✝⁸ : Algebra A 𝓞D
inst✝⁷ : Module.Finite A 𝓞D
inst✝⁶ : IsScalarTower A 𝓞D B
inst✝⁵ : IsDedekindDomain 𝓞D
inst✝⁴ : 𝓟D.LiesOver p
inst✝³ : FiniteDimensional K L
inst✝² : Ring.HasFiniteQuotients A
inst✝¹ : 𝓟D.IsMaximal
inst✝ : P.IsMaximal
hp : p ≠ ⊥
left✝⁴ : Module.Finite 𝓞D B
left✝³ : Module.IsTorsionFree 𝓞D B
left✝² : Module.IsTorsionFree A 𝓞D
left✝¹ : IsGaloisGroup Gal(L/K) A B
left✝ : IsGaloisGroup (↥(stabilizer Gal(L/K) P)) 𝓞D B
h𝓟 : 𝓟D ≠ ⊥
⊢ P.inertiaDeg 𝓞D ≤ P.inertiaDeg A
Module: Mathlib.NumberTheory.Rayleigh

Goal state before:
pp: case a.inl
r s : ℝ
hrs : r.HolderConjugate s
j k : ℤ
hk : k > 0
hjk : beattySeq r k = j
⊢ 0 < ⌊↑k * r⌋

Tactic:
Int.floor_pos

Goal state after:
case a.inl
r s : ℝ
hrs : r.HolderConjugate s
j k : ℤ
hk : k > 0
hjk : beattySeq r k = j
⊢ 1 ≤ ↑k * r
Module: Mathlib.NumberTheory.Rayleigh

Goal state before:
pp: r s : ℝ
hrs : r.HolderConjugate s
j : ℤ
s✝ : ℝ
hs : s✝ ≥ 0
x✝ : j ∈ {x | ∃ k, beattySeq s✝ k = x}
k : ℤ
hj : 0 < ⌊↑k * s✝⌋
hk : beattySeq s✝ k = j
⊢ k > 0

Tactic:
Int.floor_pos

Goal state after:
r s : ℝ
hrs : r.HolderConjugate s
j : ℤ
s✝ : ℝ
hs : s✝ ≥ 0
x✝ : j ∈ {x | ∃ k, beattySeq s✝ k = x}
k : ℤ
hj : 1 ≤ ↑k * s✝
hk : beattySeq s✝ k = j
⊢ k > 0
Module: Mathlib.NumberTheory.RatFunc.Ostrowski

Goal state before:
pp: case inr.f
K : Type u_1
Γ : Type u_2
inst✝⁴ : Field K
inst✝³ : LinearOrderedCommGroupWithZero Γ
v : Valuation K⟮X⟯ Γ
inst✝² : v.IsNontrivial
inst✝¹ : IsTrivialOn K v
hle : v X ≤ 1
inst✝ : v.IsRankOneDiscrete
p q : K[X]
hq0 : q ≠ 0
hf0 : (algebraMap K[X] K⟮X⟯) p / (algebraMap K[X] K⟮X⟯) q ≠ 0
hp0 : p ≠ 0
pi : K[X] := πᵥ
hpi_def : pi = πᵥ
hpi : v.IsUniformizer ↑pi
⊢ v ((algebraMap K[X] K⟮X⟯) p) / v ((algebraMap K[X] K⟮X⟯) q) ≤ 1 ↔
    (exp ↑((Associates.mk Pᵥ.asIdeal).count (Associates.mk (Ideal.span {p})).factors))⁻¹ *
        exp ↑((Associates.mk Pᵥ.asIdeal).count (Associates.mk (Ideal.span {q})).factors) ≤
      1

Tactic:
rw [valuation_eq_valuation_uniformizingPolynomial_pow_of_valuation_X_le_one hle hp0,
        valuation_eq_valuation_uniformizingPolynomial_pow_of_valuation_X_le_one hle hq0]

Goal state after:
case inr.f
K : Type u_1
Γ : Type u_2
inst✝⁴ : Field K
inst✝³ : LinearOrderedCommGroupWithZero Γ
v : Valuation K⟮X⟯ Γ
inst✝² : v.IsNontrivial
inst✝¹ : IsTrivialOn K v
hle : v X ≤ 1
inst✝ : v.IsRankOneDiscrete
p q : K[X]
hq0 : q ≠ 0
hf0 : (algebraMap K[X] K⟮X⟯) p / (algebraMap K[X] K⟮X⟯) q ≠ 0
hp0 : p ≠ 0
pi : K[X] := πᵥ
hpi_def : pi = πᵥ
hpi : v.IsUniformizer ↑pi
⊢ v (↑πᵥ ^ (Associates.mk Pᵥ.asIdeal).count (Associates.mk (Ideal.span {p})).factors) /
        v (↑πᵥ ^ (Associates.mk Pᵥ.asIdeal).count (Associates.mk (Ideal.span {q})).factors) ≤
      1 ↔
    (exp ↑((Associates.mk Pᵥ.asIdeal).count (Associates.mk (Ideal.span {p})).factors))⁻¹ *
        exp ↑((Associates.mk Pᵥ.asIdeal).count (Associates.mk (Ideal.span {q})).factors) ≤
      1
Module: Mathlib.NumberTheory.Zsqrtd.GaussianInt

Goal state before:
pp: x : ℤ[i]
⊢ toComplex x = { re := ↑x.re, im := ↑x.im }

Tactic:
apply Complex.ext

Goal state after:
case a
x : ℤ[i]
⊢ (toComplex x).re = { re := ↑x.re, im := ↑x.im }.re

case a
x : ℤ[i]
⊢ (toComplex x).im = { re := ↑x.re, im := ↑x.im }.im
Module: Mathlib.NumberTheory.Zsqrtd.GaussianInt

Goal state before:
pp: α : Type u_1
inst✝ : AddGroupWithOne α
x : ℤ[i]
⊢ ↑(norm x).natAbs = ↑(norm x)

Tactic:
by
  simp

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

Goal state before:
pp: x y : ℤ[i]
⊢ toComplex x / toComplex y - toComplex (x / y) =
    ↑(toComplex x / toComplex y).re - ↑(toComplex (x / y)).re +
      (↑(toComplex x / toComplex y).im - ↑(toComplex (x / y)).im) * I

Tactic:
apply Complex.ext

Goal state after:
case a
x y : ℤ[i]
⊢ (toComplex x / toComplex y - toComplex (x / y)).re =
    (↑(toComplex x / toComplex y).re - ↑(toComplex (x / y)).re +
        (↑(toComplex x / toComplex y).im - ↑(toComplex (x / y)).im) * I).re

case a
x y : ℤ[i]
⊢ (toComplex x / toComplex y - toComplex (x / y)).im =
    (↑(toComplex x / toComplex y).re - ↑(toComplex (x / y)).re +
        (↑(toComplex x / toComplex y).im - ↑(toComplex (x / y)).im) * I).im
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

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

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.Liouville.Basic

Goal state before:
pp: a : ℤ
b : ℕ
bN0 : b ≠ 0
cop : a.natAbs.Coprime b
h : Liouville (↑a / ↑b)
p q : ℤ
q1 : 1 < q
a0 : ↑a / ↑b ≠ ↑p / ↑q
a1 : |↑a / ↑b - ↑p / ↑q| < 1 / ↑q ^ (b + 1)
qR0 : 0 < ↑q
b0 : ↑b ≠ 0
bq0 : 0 < ↑b * ↑q
⊢ |a * q - ↑b * p| * q ^ (b + 1) < ↑b * q

Tactic:
rw [div_sub_div _ _ b0 qR0.ne', abs_div, div_lt_div_iff₀ (abs_pos.mpr bq0.ne') (pow_pos qR0 _),
      abs_of_pos bq0, one_mul] at a1

Goal state after:
a : ℤ
b : ℕ
bN0 : b ≠ 0
cop : a.natAbs.Coprime b
h : Liouville (↑a / ↑b)
p q : ℤ
q1 : 1 < q
a0 : ↑a / ↑b ≠ ↑p / ↑q
a1 : |↑a * ↑q - ↑b * ↑p| * ↑q ^ (b + 1) < ↑b * ↑q
qR0 : 0 < ↑q
b0 : ↑b ≠ 0
bq0 : 0 < ↑b * ↑q
⊢ |a * q - ↑b * p| * q ^ (b + 1) < ↑b * q
Module: Mathlib.NumberTheory.RamificationInertia.Basic

Goal state before:
pp: case mk.mk
R : Type u
inst✝³ : CommRing R
S : Type v
inst✝² : CommRing S
inst✝¹ : Algebra R S
p : Ideal R
P : Ideal S
hfp : NeZero e
inst✝ : IsDedekindDomain S
hP0 : P ≠ ⊥
hP : P.IsPrime
i : ℕ
hi : i < e
a : S
a_mem : span {a} ≤ P ^ i
a_notMem : ¬span {a} ≤ P ^ (i + 1)
b✝ : ↥(map (Quotient.mk (P ^ e)) (P ^ i)) ⧸ (p.powQuotSuccInclusion P i).range
val✝ : S ⧸ P ^ e
x : S
hx✝ : Quot.mk (⇑(Submodule.quotientRel (P ^ e))) x ∈ map (Quotient.mk (P ^ e)) (P ^ i)
hx : x ∈ P ^ i
Pe_le_Pi : P ^ e ≤ P ^ i
hspan0 : span {a} ≠ ⊥
⊢ x ∈ P ^ (i + 1) ⊔ span {a}

Tactic:
irreducible_pow_sup hspan0 ((prime_iff_isPrime hP0).mpr hP).irreducible,

Goal state after:
case mk.mk
R : Type u
inst✝³ : CommRing R
S : Type v
inst✝² : CommRing S
inst✝¹ : Algebra R S
p : Ideal R
P : Ideal S
hfp : NeZero e
inst✝ : IsDedekindDomain S
hP0 : P ≠ ⊥
hP : P.IsPrime
i : ℕ
hi : i < e
a : S
a_mem : span {a} ≤ P ^ i
a_notMem : ¬span {a} ≤ P ^ (i + 1)
b✝ : ↥(map (Quotient.mk (P ^ e)) (P ^ i)) ⧸ (p.powQuotSuccInclusion P i).range
val✝ : S ⧸ P ^ e
x : S
hx✝ : Quot.mk (⇑(Submodule.quotientRel (P ^ e))) x ∈ map (Quotient.mk (P ^ e)) (P ^ i)
hx : x ∈ P ^ i
Pe_le_Pi : P ^ e ≤ P ^ i
hspan0 : span {a} ≠ ⊥
⊢ x ∈ P ^ min (Multiset.count P (normalizedFactors (span {a}))) (i + 1)
Module: Mathlib.NumberTheory.Transcendental.Lindemann.AnalyticalPart

Goal state before:
pp: case h.right.refine_1
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' : eval 0 (sumIDeriv (X ^ (p - 1) * f ^ p)) = (p - 1)! • eval 0 (f ^ p) + p ! • eval 0 gp'
gp : ℤ[X]
gp'_le : gp.natDegree ≤ (X ^ (p - 1) * f ^ p).natDegree - p
h :
  ∀ (r : ℂ),
    (X - C r) ^ p ∣ map (algebraMap ℤ ℂ) (X ^ (p - 1) * f ^ p) →
      (aeval r) (sumIDeriv (X ^ (p - 1) * f ^ p)) = p ! • (aeval r) gp
⊢ gp.natDegree ≤ p * f.natDegree - 1

Tactic:
refine gp'_le.trans ((tsub_le_tsub_right natDegree_mul_le p).trans ?_)
    rw [natDegree_X_pow, natDegree_pow, tsub_add_eq_add_tsub prime_p.one_le, tsub_right_comm,
      add_tsub_cancel_left]

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

Goal state before:
pp: m : ℤ
⊢ volume
      ((fun x ↦ x + ↑m) ⁻¹'
        ⋃ n, ⋃ (_ : n > 0), {x | ∃ᶠ (b : ℕ) in atTop, ∃ a ∈ Finset.Icc 0 ↑b, |x - ↑a / ↑b| < 1 / ↑b ^ (2 + 1 / ↑n)}) =
    0

Tactic:
rw [measure_preimage_add_right]

Goal state after:
m : ℤ
⊢ volume (⋃ n, ⋃ (_ : n > 0), {x | ∃ᶠ (b : ℕ) in atTop, ∃ a ∈ Finset.Icc 0 ↑b, |x - ↑a / ↑b| < 1 / ↑b ^ (2 + 1 / ↑n)}) =
    0
Module: Mathlib.Order.Category.Frm

Goal state before:
pp: X Y : Frm
e : X ≅ Y
x : ↑X
⊢ (ConcreteCategory.hom e.inv) ((ConcreteCategory.hom e.hom) x) = x

Tactic:
by
  simp

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

Goal state before:
pp: X Y : Frm
e : X ≅ Y
s : ↑Y
⊢ (ConcreteCategory.hom e.hom) ((ConcreteCategory.hom e.inv) s) = s

Tactic:
by
  simp

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

Goal state before:
pp: X Y : FinBddDistLat
e : X ≅ Y
x : ↑X.toDistLat
⊢ (ConcreteCategory.hom e.inv) ((ConcreteCategory.hom e.hom) x) = x

Tactic:
by
  simp

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

Goal state before:
pp: X Y : FinBddDistLat
e : X ≅ Y
s : ↑Y.toDistLat
⊢ (ConcreteCategory.hom e.hom) ((ConcreteCategory.hom e.inv) s) = s

Tactic:
by
  simp

Goal state after:
Module: Mathlib.Order.Comparable

Goal state before:
pp: α : Type u_1
a b : α
r : α → α → Prop
⊢ IncompRel rᶜ a b ↔ AntisymmRel r a b

Tactic:
by
  simp

Goal state after:
Module: Mathlib.Order.CompleteLattice.PiLex

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝² : LinearOrder ι
inst✝¹ : (i : ι) → CompleteLinearOrder (α i)
inst✝ : WellFoundedGT ι
x✝ : Set (Colex ((i : ι) → α i))
⊢ IsGLB x✝ (sInf x✝)

Tactic:
by exact Lex.isGLB_sInf (ι := ιᵒᵈ)

Goal state after:
Module: Mathlib.Order.CompleteSublattice

Goal state before:
pp: α : Type u_1
inst✝ : CompleteLattice α
L : CompleteSublattice α
ι : Sort u_3
f : ι → ↥L
⊢ ⨅ N ∈ range f, ↑N = ⨅ i, ↑(f i)

Tactic:
iInf_range

Goal state after:
α : Type u_1
inst✝ : CompleteLattice α
L : CompleteSublattice α
ι : Sort u_3
f : ι → ↥L
⊢ ⨅ i, ↑(f i) = ⨅ i, ↑(f i)
Module: Mathlib.Order.Completion

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

Tactic:
rw [right_principal, mem_Ici, sSup_le_iff, ← upperBounds_left, mem_upperBounds]

Goal state after:
Module: Mathlib.Order.Concept

Goal state before:
pp: α : Type u_2
β : Type u_3
r : α → β → Prop
a : α
b : β
⊢ ofObject r a ≤ ofAttribute r b ↔ r a b

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
⊢ range A ⊆ s

Tactic:
simp [range]

Goal state after:
ι : 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
⊢ {x | ∃ y, A y = x} ⊆ s
Module: Mathlib.Order.Concept

Goal state before:
pp: ι : Sort u_1
α : Type u_2
β : Type u_3
r : α → β → Prop
f : ι → Concept α β r
⊢ lowerPolar r (⨅ i ∈ range fun i ↦ f i, i.intent) = lowerPolar r (⨅ i, (f i).intent)

Tactic:
iInf_range

Goal state after:
Module: Mathlib.Order.Concept

Goal state before:
pp: ι : Sort u_1
α : Type u_2
β : Type u_3
r : α → β → Prop
f : ι → Concept α β r
⊢ ⨅ i ∈ range fun i ↦ f i, i.intent = ⨅ i, (f i).intent

Tactic:
iInf_range

Goal state after:
Module: Mathlib.Order.Concept

Goal state before:
pp: ι : Sort u_1
α : Type u_2
β : Type u_3
r : α → β → Prop
f : ι → Concept α β r
⊢ ⨅ i ∈ range fun i ↦ f i, i.extent = ⨅ i, (f i).extent

Tactic:
iInf_range

Goal state after:
Module: Mathlib.Order.Concept

Goal state before:
pp: ι : Sort u_1
α : Type u_2
β : Type u_3
r : α → β → Prop
f : ι → Concept α β r
⊢ upperPolar r (⨅ i ∈ range fun i ↦ f i, i.extent) = upperPolar r (⨅ i, (f i).extent)

Tactic:
iInf_range

Goal state after:
Module: Mathlib.Order.Filter.CardinalInter

Goal state before:
pp: ι α β : Type u
c : Cardinal.{u}
l✝ l : Filter α
inst✝ : CountableInterFilter l
S : Set (Set α)
hS : #↑S < ℵ_ 1
a : ∀ s ∈ S, s ∈ l
⊢ ⋂₀ S ∈ l

Tactic:
by
    apply CountableInterFilter.countable_sInter_mem S _ a
    rwa [← le_aleph0_iff_set_countable, ← lt_aleph_one_iff]

Goal state after:
Module: Mathlib.Order.Filter.Partial

Goal state before:
pp: α : Type u
β : Type v
l₁ : Filter α
l₂ : Filter β
f : α → β
⊢ Tendsto f l₁ l₂ ↔ RTendsto' (Function.graph f) l₁ l₂

Tactic:
by
  simp [tendsto_def, Function.graph, rtendsto'_def, SetRel.preimage, Set.preimage]

Goal state after:
Module: Mathlib.Order.Nucleus

Goal state before:
pp: X : Type u_1
inst✝ : CompleteLattice X
ι : Type u_2
f : ι → Nucleus X
x : X
⊢ ⨅ j ∈ range f, j x = ⨅ j, (f j) x

Tactic:
iInf_range

Goal state after:
X : Type u_1
inst✝ : CompleteLattice X
ι : Type u_2
f : ι → Nucleus X
x : X
⊢ ⨅ i, (f i) x = ⨅ j, (f j) x
Module: Mathlib.Order.Sublocale

Goal state before:
pp: X : Type u_1
inst✝ : Order.Frame X
ι : Sort u_2
S T : Sublocale X
s : Set X
f : ι → X
a b : X
s1 s2 : Sublocale X
h : (fun x ↦ x.carrier) s1 = (fun x ↦ x.carrier) s2
⊢ s1 = s2

Tactic:
by cases s1; congr

Goal state after:
Module: Mathlib.Order.Sublocale

Goal state before:
pp: X : Type u_1
inst✝ : Order.Frame X
n : Nucleus X
a : Set X
h : a ⊆ range ⇑n
b : X
h1 : b ∈ a
⊢ n (sInf a) ≤ b

Tactic:
simp_rw [subset_def, mem_range] at h

Goal state after:
X : Type u_1
inst✝ : Order.Frame X
n : Nucleus X
a : Set X
b : X
h1 : b ∈ a
h : ∀ x ∈ a, n x = x
⊢ n (sInf a) ≤ b
Module: Mathlib.Probability.Process.HittingTime

Goal state before:
pp: Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n : ι
ω : Ω
m : ι
h_exists : ∃ j ∈ Set.Icc n m, u j ω ∈ s
⊢ n ≤ hittingBtwn u s n m ω

Tactic:
by
  refine le_hittingBtwn ?_ ω
  by_contra h
  rw [Set.Icc_eq_empty_of_lt (not_le.mp h)] at h_exists
  simp at h_exists

Goal state after: