mathlib-initiative/mathlib-tactics huggingface dataset:
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₁ = (a₁ ^ n₂) ^ n₁ ∨ a₁ = -(a₁ ^ n₂) ^ n₁
⊢ a₁ ^ n₂ = a₁

pp: case inr
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₁ = (-a₁ ^ n₂) ^ n₁ ∨ a₁ = -(-a₁ ^ n₂) ^ n₁
⊢ -a₁ ^ n₂ = a₁

Tactic:
· rw [← zpow_mul, eq_comm, @eq_comm _ a₁, ← mul_inv_eq_one, ← @mul_inv_eq_one _ _ _ a₁, ←
      zpow_neg_one, neg_mul, ← zpow_add, ← sub_eq_add_neg] at hn₁
    rcases hn₁ with hn₁ | hn₁
    · rcases Int.isUnit_iff.mp
          (.of_mul_eq_one _ <|
            sub_eq_zero.mp <| (ha₁.zpow_eq_one_iff (n₂ * n₁ - 1)).mp hn₁) with
        (rfl | rfl)
      · rw [zpow_one]
      · rw [zpow_neg_one, y_inv, lt_neg, neg_zero] at Hy
        exact False.elim (lt_irrefl _ <| ha₁.2.1.trans Hy)
    · rw [← zpow_zero a₁, eq_comm] at hn₁
      exact False.elim (ha₁.zpow_ne_neg_zpow hn₁)

Goal state after:
case inr
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₁ = (-a₁ ^ n₂) ^ n₁ ∨ a₁ = -(-a₁ ^ n₂) ^ n₁
⊢ -a₁ ^ n₂ = a₁
Module: Mathlib.NumberTheory.RatFunc.Ostrowski

Goal state before:
pp: K : Type u_1
Γ : Type u_2
inst✝³ : Field K
inst✝² : LinearOrderedCommGroupWithZero Γ
v : Valuation K⟮X⟯ Γ
inst✝¹ : DecidableEq K⟮X⟯
inst✝ : IsTrivialOn K v
hlt : 1 < v X
⊢ v.IsEquiv (inftyValuation K)

Tactic:
refine isEquiv_iff_val_lt_one.mpr fun {f} ↦ ?_

Goal state after:
K : Type u_1
Γ : Type u_2
inst✝³ : Field K
inst✝² : LinearOrderedCommGroupWithZero Γ
v : Valuation K⟮X⟯ Γ
inst✝¹ : DecidableEq K⟮X⟯
inst✝ : IsTrivialOn K v
hlt : 1 < v X
f : K⟮X⟯
⊢ v f < 1 ↔ (inftyValuation K) f < 1
Module: Mathlib.NumberTheory.SelbergSieve

Goal state before:
pp: s : BoundingSieve
d : ℕ
hd : d ∣ s.prodPrimes
⊢ s.nu (∏ a ∈ d.primeFactors, a) = s.nu d

Tactic:
Nat.prod_primeFactors_of_squarefree <| Squarefree.squarefree_of_dvd hd s.prodPrimes_squarefree

Goal state after:
s : BoundingSieve
d : ℕ
hd : d ∣ s.prodPrimes
⊢ s.nu d = s.nu d
Module: Mathlib.NumberTheory.SelbergSieve

Goal state before:
pp: s : BoundingSieve
d : ℕ
hdP : d ∣ s.prodPrimes
hd_ne_one : d ≠ 1
hd_sq : Squarefree d
⊢ s.nu d < 1

Tactic:
have := hd_sq.ne_zero

Goal state after:
s : BoundingSieve
d : ℕ
hdP : d ∣ s.prodPrimes
hd_ne_one : d ≠ 1
hd_sq : Squarefree d
this : d ≠ 0
⊢ s.nu d < 1
Module: Mathlib.NumberTheory.SelbergSieve

Goal state before:
pp: s : BoundingSieve
muPlus : ℕ → ℝ
h : IsUpperMoebius muPlus
hμ : ∀ (n : ℕ), (if n = 1 then 1 else 0) ≤ ∑ d ∈ n.divisors, muPlus d
⊢ (∑ y ∈ s.prodPrimes.divisors, ∑ x ∈ s.support, if y ∣ x then s.weights x * muPlus y else 0) =
    ∑ d ∈ s.prodPrimes.divisors, muPlus d * ∑ n ∈ s.support, if d ∣ n then s.weights n else 0

Tactic:
← sum_filter,

Goal state after:
s : BoundingSieve
muPlus : ℕ → ℝ
h : IsUpperMoebius muPlus
hμ : ∀ (n : ℕ), (if n = 1 then 1 else 0) ≤ ∑ d ∈ n.divisors, muPlus d
⊢ ∑ x ∈ s.prodPrimes.divisors, ∑ a ∈ s.support with x ∣ a, s.weights a * muPlus x =
    ∑ x ∈ s.prodPrimes.divisors, muPlus x * ∑ a ∈ s.support with x ∣ a, s.weights a
Module: Mathlib.NumberTheory.RatFunc.Ostrowski

Goal state before:
pp: 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
h0 : v ↑πᵥ ≠ 0
p q : K[X]
hq : q ≠ 0
hf : (algebraMap K[X] K⟮X⟯) p / (algebraMap K[X] K⟮X⟯) q ≠ 0
⊢ p ≠ 0

Tactic:
by aesop

Goal state after:
Module: Mathlib.NumberTheory.RatFunc.Ostrowski

Goal state before:
pp: 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
hv : v.IsRankOneDiscrete
h0 : v ↑πᵥ ≠ 0
γ : Γˣ
x✝ : ∃ a, ¬a = 0 ∧ ∃ x, (MonoidWithZeroHom.ofClass v) a * ↑γ = (MonoidWithZeroHom.ofClass v) x
a : K⟮X⟯
ha : ¬a = 0
b : K⟮X⟯
hab : (MonoidWithZeroHom.ofClass v) a * ↑γ = (MonoidWithZeroHom.ofClass v) b
ka : ℤ
hka : v a = v ↑πᵥ ^ ka
⊢ b ≠ 0

Tactic:
by aesop

Goal state after:
Module: Mathlib.NumberTheory.SumFourSquares

Goal state before:
pp: case inr
p : ℕ
hp : Fact (Nat.Prime p)
hodd : Odd p
a b : ℕ
ha : a ≤ p / 2
hb : b ≤ p / 2
hab : ↑a ^ 2 + ↑b ^ 2 ≡ -1 [ZMOD ↑p]
k : ℤ
hk : ↑a ^ 2 + ↑b ^ 2 - -1 = ↑p * k
⊢ ∃ a b k, 0 < k ∧ k < p ∧ a ^ 2 + b ^ 2 + 1 = k * p

Tactic:
sub_neg_eq_add,

Goal state after:
case inr
p : ℕ
hp : Fact (Nat.Prime p)
hodd : Odd p
a b : ℕ
ha : a ≤ p / 2
hb : b ≤ p / 2
hab : ↑a ^ 2 + ↑b ^ 2 ≡ -1 [ZMOD ↑p]
k : ℤ
hk : ↑a ^ 2 + ↑b ^ 2 + 1 = ↑p * k
⊢ ∃ a b k, 0 < k ∧ k < p ∧ a ^ 2 + b ^ 2 + 1 = k * p
Module: Mathlib.NumberTheory.SelbergSieve

Goal state before:
pp: s : BoundingSieve
d : ℕ
hdP : d ∣ s.prodPrimes
⊢ (∑ l ∈ s.prodPrimes.divisors, if l ∣ d then (selbergTerms l)⁻¹ else 0) = (s.nu d)⁻¹

Tactic:
← sum_filter,

Goal state after:
s : BoundingSieve
d : ℕ
hdP : d ∣ s.prodPrimes
⊢ ∑ a ∈ s.prodPrimes.divisors with a ∣ d, (selbergTerms a)⁻¹ = (s.nu d)⁻¹
Module: Mathlib.NumberTheory.SelbergSieve

Goal state before:
pp: s : BoundingSieve
d : ℕ
hd : d ∣ s.prodPrimes
⊢ (∑ l ∈ s.prodPrimes.divisors, if l ∣ d then selbergTerms l else 0) =
    ∑ l ∈ s.prodPrimes.divisors, if l ∣ d then selbergTerms (d / l) else 0

Tactic:
← sum_filter,

Goal state after:
s : BoundingSieve
d : ℕ
hd : d ∣ s.prodPrimes
⊢ ∑ a ∈ s.prodPrimes.divisors with a ∣ d, selbergTerms a = ∑ a ∈ s.prodPrimes.divisors with a ∣ d, selbergTerms (d / a)
Module: Mathlib.NumberTheory.SelbergSieve

Goal state before:
pp: s : BoundingSieve
d : ℕ
hd : d ∣ s.prodPrimes
⊢ (∑ l ∈ s.prodPrimes.divisors, if l ∣ d then selbergTerms (d / l) else 0) =
    selbergTerms d * ∑ l ∈ s.prodPrimes.divisors, if l ∣ d then (selbergTerms l)⁻¹ else 0

Tactic:
← sum_filter,

Goal state after:
s : BoundingSieve
d : ℕ
hd : d ∣ s.prodPrimes
⊢ ∑ a ∈ s.prodPrimes.divisors with a ∣ d, selbergTerms (d / a) =
    selbergTerms d * ∑ a ∈ s.prodPrimes.divisors with a ∣ d, (selbergTerms a)⁻¹
Module: Mathlib.NumberTheory.SelbergSieve

Goal state before:
pp: case a.a
s : BoundingSieve
w : ℕ → ℝ
d1 : ℕ
hd1 : d1 ∈ s.prodPrimes.divisors
d2 : ℕ
hd2 : d2 ∈ s.prodPrimes.divisors
hgcd_dvd : d1.gcd d2 ∣ s.prodPrimes
⊢ (s.nu d1 * w d1 * s.nu d2 * w d2 * ∑ l ∈ s.prodPrimes.divisors, if l ∣ d1.gcd d2 then (selbergTerms l)⁻¹ else 0) =
    ∑ l ∈ s.prodPrimes.divisors, if l ∣ d1.gcd d2 then (selbergTerms l)⁻¹ * (s.nu d1 * w d1) * (s.nu d2 * w d2) else 0

Tactic:
← sum_filter,

Goal state after:
case a.a
s : BoundingSieve
w : ℕ → ℝ
d1 : ℕ
hd1 : d1 ∈ s.prodPrimes.divisors
d2 : ℕ
hd2 : d2 ∈ s.prodPrimes.divisors
hgcd_dvd : d1.gcd d2 ∣ s.prodPrimes
⊢ s.nu d1 * w d1 * s.nu d2 * w d2 * ∑ a ∈ s.prodPrimes.divisors with a ∣ d1.gcd d2, (selbergTerms a)⁻¹ =
    ∑ a ∈ s.prodPrimes.divisors with a ∣ d1.gcd d2, (selbergTerms a)⁻¹ * (s.nu d1 * w d1) * (s.nu d2 * w d2)
Module: Mathlib.NumberTheory.SelbergSieve

Goal state before:
pp: s : BoundingSieve
w : ℕ → ℝ
⊢ (∑ l ∈ s.prodPrimes.divisors,
      ∑ d1 ∈ s.prodPrimes.divisors,
        ∑ d2 ∈ s.prodPrimes.divisors,
          if l ∣ d1.gcd d2 then (selbergTerms l)⁻¹ * (s.nu d1 * w d1) * (s.nu d2 * w d2) else 0) =
    ∑ l ∈ s.prodPrimes.divisors,
      (selbergTerms l)⁻¹ * (∑ d ∈ s.prodPrimes.divisors, if l ∣ d then s.nu d * w d else 0) ^ 2

Tactic:
← sum_filter,

Goal state after:
s : BoundingSieve
w : ℕ → ℝ
⊢ ∑ x ∈ s.prodPrimes.divisors,
      ∑ x_1 ∈ s.prodPrimes.divisors,
        ∑ a ∈ s.prodPrimes.divisors with x ∣ x_1.gcd a, (selbergTerms x)⁻¹ * (s.nu x_1 * w x_1) * (s.nu a * w a) =
    ∑ x ∈ s.prodPrimes.divisors, (selbergTerms x)⁻¹ * (∑ a ∈ s.prodPrimes.divisors with x ∣ a, s.nu a * w a) ^ 2
Module: Mathlib.NumberTheory.Zsqrtd.GaussianInt

Goal state before:
pp: x y : ℤ[i]
this : |2⁻¹| = 2⁻¹
⊢ |(↑(toComplex x / toComplex y).re - ↑(toComplex (x / y)).re +
          (↑(toComplex x / toComplex y).im - ↑(toComplex (x / y)).im) * I).re| ≤
    |(1 / 2 + 1 / 2 * I).re|

Tactic:
by rw [toComplex_re_div]; simp [normSq, this]; simpa using abs_sub_round (x / y : ℂ).re

Goal state after:
Module: Mathlib.NumberTheory.SelbergSieve

Goal state before:
pp: s : BoundingSieve
w : ℕ → ℝ
⊢ mainSum (lambdaSquared w) =
    ∑ l ∈ s.prodPrimes.divisors,
      (selbergTerms l)⁻¹ * (∑ d ∈ s.prodPrimes.divisors, if l ∣ d then s.nu d * w d else 0) ^ 2

Tactic:
by
  calc mainSum (lambdaSquared w) =
    ∑ d1 ∈ divisors s.prodPrimes, ∑ d2 ∈ divisors s.prodPrimes, (∑ l ∈ divisors s.prodPrimes,
      if l ∣ d1.gcd d2 then (s.selbergTerms l)⁻¹ * (s.nu d1 * w d1) * (s.nu d2 * w d2) else 0)
        := ?caseA
    _ = ∑ l ∈ divisors s.prodPrimes, ∑ d1 ∈ divisors s.prodPrimes, ∑ d2 ∈ divisors s.prodPrimes,
      if l ∣ Nat.gcd d1 d2 then (s.selbergTerms l)⁻¹ * (s.nu d1 * w d1) * (s.nu d2 * w d2) else 0
        := ?caseB
    _ = ∑ l ∈ divisors s.prodPrimes,
      (s.selbergTerms l)⁻¹ * (∑ d ∈ divisors s.prodPrimes, if l ∣ d then s.nu d * w d else 0) ^ 2
        := ?caseC
  case caseA =>
    rw [mainSum_lambdaSquared_eq_sum_sum_mul w]
    congr! 2 with d1 hd1 d2 hd2
    have hgcd_dvd : d1.gcd d2 ∣ s.prodPrimes :=
      (Nat.gcd_dvd_left d1 d2).trans (dvd_of_mem_divisors hd1)
    simp_rw [nu_inv_eq_sum_divisors_inv_selbergTerms hgcd_dvd, ← sum_filter, mul_sum]
    congr with l
    ring
  case caseB =>
    rw [eq_comm, sum_comm, sum_congr rfl fun _ _ ↦ sum_comm]
  case caseC =>
    simp_rw [← sum_filter, sq, sum_mul, mul_sum, sum_filter, ite_sum_zero,
      ← ite_and, dvd_gcd_iff, mul_assoc]

Goal state after:
Module: Mathlib.NumberTheory.SumFourSquares

Goal state before:
pp: case neg.inr
p : ℕ
hp : Prime p
this✝ : Fact (Prime p)
natAbs_iff :
  ∀ {a b c d : ℤ} {k : ℕ},
    a.natAbs ^ 2 + b.natAbs ^ 2 + c.natAbs ^ 2 + d.natAbs ^ 2 = k ↔ a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = ↑k
hm✝ : ∃ m < p, 0 < m ∧ ∃ a b c d, a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = m * p
m : ℕ
hmin : ∀ m_1 < m, ¬(m_1 < p ∧ 0 < m_1 ∧ ∃ a b c d, a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = m_1 * p)
hmp : m < p
hm₀ : 0 < m
a b c d : ℕ
habcd : a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = m * p
hm₁ : 1 < m
this : NeZero m
hm : ¬2 ∣ m
f : ℕ → ℤ
hf_lt : ∀ (x : ℕ), 2 * (f x).natAbs < m
hf_mod : ∀ (x : ℕ), ↑(f x) = ↑x
r : ℕ
hr : (f a).natAbs ^ 2 + (f b).natAbs ^ 2 + (f c).natAbs ^ 2 + (f d).natAbs ^ 2 = m * r
hr₀ : 0 < r
hrm : r < m
w x y z : ℤ
hw : ↑m ∣ w
hx : ↑m ∣ x
hy : ↑m ∣ y
hz : ↑m ∣ z
h : w ^ 2 + x ^ 2 + y ^ 2 + z ^ 2 = ↑(m * r) * ↑(m * p)
⊢ False

Tactic:
have : (w / m) ^ 2 + (x / m) ^ 2 + (y / m) ^ 2 + (z / m) ^ 2 = ↑(r * p) := by
        refine mul_left_cancel₀ (pow_ne_zero 2 (Nat.cast_ne_zero.2 hm₀.ne')) ?_
        conv_rhs => rw [← Nat.cast_pow, ← Nat.cast_mul, sq m, mul_mul_mul_comm, Nat.cast_mul, ← h]
        simp only [mul_add, ← mul_pow, Int.mul_ediv_cancel', *]

Goal state after:
case neg.inr
p : ℕ
hp : Prime p
this✝¹ : Fact (Prime p)
natAbs_iff :
  ∀ {a b c d : ℤ} {k : ℕ},
    a.natAbs ^ 2 + b.natAbs ^ 2 + c.natAbs ^ 2 + d.natAbs ^ 2 = k ↔ a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = ↑k
hm✝ : ∃ m < p, 0 < m ∧ ∃ a b c d, a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = m * p
m : ℕ
hmin : ∀ m_1 < m, ¬(m_1 < p ∧ 0 < m_1 ∧ ∃ a b c d, a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = m_1 * p)
hmp : m < p
hm₀ : 0 < m
a b c d : ℕ
habcd : a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = m * p
hm₁ : 1 < m
this✝ : NeZero m
hm : ¬2 ∣ m
f : ℕ → ℤ
hf_lt : ∀ (x : ℕ), 2 * (f x).natAbs < m
hf_mod : ∀ (x : ℕ), ↑(f x) = ↑x
r : ℕ
hr : (f a).natAbs ^ 2 + (f b).natAbs ^ 2 + (f c).natAbs ^ 2 + (f d).natAbs ^ 2 = m * r
hr₀ : 0 < r
hrm : r < m
w x y z : ℤ
hw : ↑m ∣ w
hx : ↑m ∣ x
hy : ↑m ∣ y
hz : ↑m ∣ z
h : w ^ 2 + x ^ 2 + y ^ 2 + z ^ 2 = ↑(m * r) * ↑(m * p)
this : (w / ↑m) ^ 2 + (x / ↑m) ^ 2 + (y / ↑m) ^ 2 + (z / ↑m) ^ 2 = ↑(r * p)
⊢ False
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 : NeZero e
inst✝ : IsDedekindDomain S
hP0 : P ≠ ⊥
hP : P.IsPrime
i : ℕ
hi : i < e
a : S
a_mem : a ∈ P ^ i
a_notMem : a ∉ P ^ (i + 1)
b✝ : ↥(map (Quotient.mk (P ^ e)) (P ^ i)) ⧸ (p.powQuotSuccInclusion P i).range
val✝ : S ⧸ P ^ e
Pe_le_Pi : P ^ e ≤ P ^ i
z : S
hz : z ∈ P ^ (i + 1)
y : S
hy' : a * y ∈ span {a}
hx✝ : Quot.mk (⇑(Submodule.quotientRel (P ^ e))) (a * y + z) ∈ map (Quotient.mk (P ^ e)) (P ^ i)
hx : a * y + z ∈ P ^ i
hx' : a * y + z ∈ span {a} ⊔ P ^ (i + 1)
⊢ (Quotient.mk (P ^ e)) (-z) = (Quotient.mk (P ^ e)) (a * y) - ((Quotient.mk (P ^ e)) (a * y) + (Quotient.mk (P ^ e)) z)

Tactic:
sub_add_cancel_left,

Goal state after:
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 : a ∈ P ^ i
a_notMem : a ∉ P ^ (i + 1)
b✝ : ↥(map (Quotient.mk (P ^ e)) (P ^ i)) ⧸ (p.powQuotSuccInclusion P i).range
val✝ : S ⧸ P ^ e
Pe_le_Pi : P ^ e ≤ P ^ i
z : S
hz : z ∈ P ^ (i + 1)
y : S
hy' : a * y ∈ span {a}
hx✝ : Quot.mk (⇑(Submodule.quotientRel (P ^ e))) (a * y + z) ∈ map (Quotient.mk (P ^ e)) (P ^ i)
hx : a * y + z ∈ P ^ i
hx' : a * y + z ∈ span {a} ⊔ P ^ (i + 1)
⊢ (Quotient.mk (P ^ e)) (-z) = -(Quotient.mk (P ^ e)) z
Module: Mathlib.NumberTheory.RamificationInertia.Basic

Goal state before:
pp: case pos
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
hP0 : P ≠ ⊥
inst✝¹ : p.IsMaximal
inst✝ : P.IsPrime
he : e ≠ 0
this✝¹ : NeZero e := ⋯
this✝ : Algebra (R ⧸ p) (S ⧸ P) := ⋯
hdim : Module.rank (R ⧸ p) (S ⧸ P ^ e) = e • Module.rank (R ⧸ p) (S ⧸ P)
hP : FiniteDimensional (R ⧸ p) (S ⧸ P)
this : FiniteDimensional (R ⧸ p) (S ⧸ P ^ e)
⊢ ↑(finrank (R ⧸ p) (S ⧸ P ^ e)) = ↑(e * finrank (R ⧸ p) (S ⧸ P))

Tactic:
finrank_eq_rank',

Goal state after:
case pos
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
hP0 : P ≠ ⊥
inst✝¹ : p.IsMaximal
inst✝ : P.IsPrime
he : e ≠ 0
this✝¹ : NeZero e := { out := he }
this✝ : Algebra (R ⧸ p) (S ⧸ P) := Quotient.algebraQuotientOfRamificationIdxNeZero p P
hdim : Module.rank (R ⧸ p) (S ⧸ P ^ e) = e • Module.rank (R ⧸ p) (S ⧸ P)
hP : FiniteDimensional (R ⧸ p) (S ⧸ P)
this : FiniteDimensional (R ⧸ p) (S ⧸ P ^ e)
⊢ Module.rank (R ⧸ p) (S ⧸ P ^ e) = ↑(e * finrank (R ⧸ p) (S ⧸ P))
Module: Mathlib.NumberTheory.RamificationInertia.Basic

Goal state before:
pp: case pos
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
hP0 : P ≠ ⊥
inst✝¹ : p.IsMaximal
inst✝ : P.IsPrime
he : e ≠ 0
this✝¹ : NeZero e := { out := he }
this✝ : Algebra (R ⧸ p) (S ⧸ P) := Quotient.algebraQuotientOfRamificationIdxNeZero p P
hdim : Module.rank (R ⧸ p) (S ⧸ P ^ e) = e • Module.rank (R ⧸ p) (S ⧸ P)
hP : FiniteDimensional (R ⧸ p) (S ⧸ P)
this : FiniteDimensional (R ⧸ p) (S ⧸ P ^ e)
⊢ Module.rank (R ⧸ p) (S ⧸ P ^ e) = ↑e * ↑(finrank (R ⧸ p) (S ⧸ P))

Tactic:
finrank_eq_rank',

Goal state after:
case pos
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
hP0 : P ≠ ⊥
inst✝¹ : p.IsMaximal
inst✝ : P.IsPrime
he : e ≠ 0
this✝¹ : NeZero e := { out := he }
this✝ : Algebra (R ⧸ p) (S ⧸ P) := Quotient.algebraQuotientOfRamificationIdxNeZero p P
hdim : Module.rank (R ⧸ p) (S ⧸ P ^ e) = e • Module.rank (R ⧸ p) (S ⧸ P)
hP : FiniteDimensional (R ⧸ p) (S ⧸ P)
this : FiniteDimensional (R ⧸ p) (S ⧸ P ^ e)
⊢ Module.rank (R ⧸ p) (S ⧸ P ^ e) = ↑e * Module.rank (R ⧸ p) (S ⧸ P)
Module: Mathlib.NumberTheory.RamificationInertia.Basic

Goal state before:
pp: case pos
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
hP0 : P ≠ ⊥
inst✝¹ : p.IsMaximal
inst✝ : P.IsPrime
he : e ≠ 0
this✝ : NeZero e := { out := he }
this : Algebra (R ⧸ p) (S ⧸ P) := Quotient.algebraQuotientOfRamificationIdxNeZero p P
hdim : Module.rank (R ⧸ p) (S ⧸ P ^ e) = e • Module.rank (R ⧸ p) (S ⧸ P)
hP : FiniteDimensional (R ⧸ p) (S ⧸ P)
⊢ finrank (R ⧸ p) (S ⧸ P ^ e) = e * finrank (R ⧸ p) (S ⧸ P)

Tactic:
have := (finiteDimensional_iff_of_rank_eq_nsmul he hdim).mpr hP
    apply @Nat.cast_injective Cardinal
    rw [finrank_eq_rank', Nat.cast_mul, finrank_eq_rank', hdim, nsmul_eq_mul]

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

Goal state before:
pp: ⊢ IsGδ (⋂ n, ⋃ a, ⋃ b, ⋃ (_ : 1 < b), ball (↑a / ↑b) (1 / ↑b ^ n) \ {↑a / ↑b})

Tactic:
refine .iInter fun n => IsOpen.isGδ ?_

Goal state after:
n : ℕ
⊢ IsOpen (⋃ a, ⋃ b, ⋃ (_ : 1 < b), ball (↑a / ↑b) (1 / ↑b ^ n) \ {↑a / ↑b})
Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith

Goal state before:
pp: case refine_1
p x : ℝ
r : ℚ
h : LiouvilleWith p x
hr : r ≠ 0
C : ℝ
_hC₀ : 0 < C
hC : ∃ᶠ (n : ℕ) in atTop, 1 ≤ n ∧ ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < C / ↑n ^ p
n : ℕ
_hn : 1 ≤ n
m : ℤ
hne : x ≠ ↑m / ↑n
hlt : |x - ↑m / ↑n| < C / ↑n ^ p
A : ↑(r.num * m) / ↑(r.den • id n) = ↑m / ↑n * ↑r
⊢ x * ↑r ≠ ↑(r.num * m) / ↑(r.den • id n)

Tactic:
rw [A]

Goal state after:
case refine_1
p x : ℝ
r : ℚ
h : LiouvilleWith p x
hr : r ≠ 0
C : ℝ
_hC₀ : 0 < C
hC : ∃ᶠ (n : ℕ) in atTop, 1 ≤ n ∧ ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < C / ↑n ^ p
n : ℕ
_hn : 1 ≤ n
m : ℤ
hne : x ≠ ↑m / ↑n
hlt : |x - ↑m / ↑n| < C / ↑n ^ p
A : ↑(r.num * m) / ↑(r.den • id n) = ↑m / ↑n * ↑r
⊢ x * ↑r ≠ ↑m / ↑n * ↑r
Module: Mathlib.NumberTheory.Wilson

Goal state before:
pp: case refine_2
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : 0 < p
⊢ ∀ a₁ ∈ univ, ∀ a₂ ∈ univ, (↑a₁).val = (↑a₂).val → a₁ = a₂

Tactic:
intro _ _ _ _ h; rw [Units.ext_iff]; exact val_injective p h

Goal state after:
Module: Mathlib.NumberTheory.WellApproximable

Goal state before:
pp: A : Type u_1
inst✝ : SeminormedCommGroup A
a : A
n : ℕ
δ : ℝ
han : (orderOf a).Coprime n
b : A
hb : orderOf b = n
c : A
hc : c ∈ ball (a * b) δ
⊢ c ∈ ⋃ x, ⋃ (_ : orderOf x = orderOf a * n), ball x δ

Tactic:
simp only [mem_iUnion, exists_prop]

Goal state after:
A : Type u_1
inst✝ : SeminormedCommGroup A
a : A
n : ℕ
δ : ℝ
han : (orderOf a).Coprime n
b : A
hb : orderOf b = n
c : A
hc : c ∈ ball (a * b) δ
⊢ ∃ i, orderOf i = orderOf a * n ∧ c ∈ ball i δ
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}
z : α
hz : z ∈ {x, y}
⊢ z ∈ carrier

Tactic:
by aesop

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 = sInf {x, y}
z : α
hz : z ∈ {x, y}
⊢ z ∈ carrier

Tactic:
by aesop

Goal state after:
Module: Mathlib.Order.CompleteSublattice

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : CompleteLattice β
f : CompleteLatticeHom α β
L✝ L M : CompleteSublattice α
h : (fun L ↦ L.carrier) L = (fun L ↦ L.carrier) M
⊢ L = M

Tactic:
cases L

Goal state after:
case mk
α : Type u_1
β : Type u_2
inst✝¹ : CompleteLattice α
inst✝ : CompleteLattice β
f : CompleteLatticeHom α β
L M : CompleteSublattice α
toSublattice✝ : Sublattice α
sSupClosed'✝ : ∀ ⦃s : Set α⦄, s ⊆ toSublattice✝.carrier → sSup s ∈ toSublattice✝.carrier
sInfClosed'✝ : ∀ ⦃s : Set α⦄, s ⊆ toSublattice✝.carrier → sInf s ∈ toSublattice✝.carrier
h :
  (fun L ↦ L.carrier) { toSublattice := toSublattice✝, sSupClosed' := sSupClosed'✝, sInfClosed' := sInfClosed'✝ } =
    (fun L ↦ L.carrier) M
⊢ { toSublattice := toSublattice✝, sSupClosed' := sSupClosed'✝, sInfClosed' := sInfClosed'✝ } = M
Module: Mathlib.Order.Concept

Goal state before:
pp: α : Type u_2
β : Type u_3
r : α → β → Prop
s s' : Set α
h : IsExtent r s
hs' : s' ⊆ s
⊢ lowerPolar r (upperPolar r s') ⊆ s

Tactic:
by
  rw [← h.eq]
  exact lowerPolar_upperPolar_monotone r hs'

Goal state after:
Module: Mathlib.NumberTheory.WellApproximable

Goal state before:
pp: case pos
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 =ᵐ[μ] ∅
⊢ E =ᵐ[volume] ∅ ∨ E =ᵐ[volume] univ

Tactic:
replace h : ∀ p : Nat.Primes, (u p +ᵥ E : Set _) =ᵐ[μ] E := by
      intro p
      replace hE₂ : E =ᵐ[μ] C p := hE₂ p (h p)
      have h_qmp : Measure.QuasiMeasurePreserving (-u p +ᵥ ·) μ μ :=
        (measurePreserving_vadd _ μ).quasiMeasurePreserving
      refine (h_qmp.vadd_ae_eq_of_ae_eq (u p) hE₂).trans (ae_eq_trans ?_ hE₂.symm)
      rw [hC]
    exact ae_empty_or_univ_of_forall_vadd_ae_eq_self hE₀ h hu

Goal state after:
Module: Mathlib.Order.Nucleus

Goal state before:
pp: X : Type u_1
inst✝ : Frame X
n✝ m✝ : Nucleus X
x✝ y✝ : X
m n : Nucleus X
x y : X
this : Nonempty X
⊢ ∀ i ≥ x ⊓ y, ∀ (b : X), (∀ x_1 ≥ x, b ⊓ m x_1 ≤ n x_1) → (∀ i ≥ y, b ⊓ m i ≤ n i) → b ≤ m i → b ≤ n i

Tactic:
intro k hxyk l hlx hly hlk

Goal state after:
X : Type u_1
inst✝ : Frame X
n✝ m✝ : Nucleus X
x✝ y✝ : X
m n : Nucleus X
x y : X
this : Nonempty X
k : X
hxyk : k ≥ x ⊓ y
l : X
hlx : ∀ x_1 ≥ x, l ⊓ m x_1 ≤ n x_1
hly : ∀ i ≥ y, l ⊓ m i ≤ n i
hlk : l ≤ m k
⊢ l ≤ n k
Module: Mathlib.Order.Std

Goal state before:
pp: α : Type u_1
args : OfStdArgs α
this✝⁷ : LE α := args.le
this✝⁶ : LT α := args.lt
this✝⁵ :
  let this := args.le;
  let this_1 := args.lt;
  Std.LawfulOrderLT α
this✝⁴ :
  let this := args.le;
  Std.IsLinearOrder α
this✝³ : DecidableLE α := args.decidableLE
this✝² : Std.LawfulOrderLeftLeaningMin α
this✝¹ : Std.LawfulOrderLeftLeaningMax α
a b : α
this✝ : Ord α := args.ord
this :
  let this := args.le;
  let this_1 := args.lt;
  let this_2 := ⋯;
  let this_3 := ⋯;
  let this_4 := args.decidableEq;
  let this_5 := args.decidableLT;
  Std.LawfulOrderOrd α
h✝¹ : ¬a < b
h✝ : a = b
⊢ compare a b = Ordering.eq

Tactic:
Std.compare_eq_iff_eq

Goal state after:
α : Type u_1
args : OfStdArgs α
this✝⁷ : LE α := args.le
this✝⁶ : LT α := args.lt
this✝⁵ :
  let this := args.le;
  let this_1 := args.lt;
  Std.LawfulOrderLT α
this✝⁴ :
  let this := args.le;
  Std.IsLinearOrder α
this✝³ : DecidableLE α := args.decidableLE
this✝² : Std.LawfulOrderLeftLeaningMin α
this✝¹ : Std.LawfulOrderLeftLeaningMax α
a b : α
this✝ : Ord α := args.ord
this :
  let this := args.le;
  let this_1 := args.lt;
  let this_2 := ⋯;
  let this_3 := ⋯;
  let this_4 := args.decidableEq;
  let this_5 := args.decidableLT;
  Std.LawfulOrderOrd α
h✝¹ : ¬a < b
h✝ : a = b
⊢ a = b
Module: Mathlib.Order.Sublocale

Goal state before:
pp: case mpr
X : Type u_1
inst✝ : Order.Frame X
ι : Sort u_2
S✝ T : Sublocale X
s : Set X
f : ι → X
a✝ b✝ : X
S : Sublocale X
a : X
b : ↥S
h : a ≤ ↑b
⊢ S.restrictAux a ≤ b

Tactic:
exact sInf_le (by simp [h])

Goal state after: