mathlib-initiative/mathlib-tactics huggingface dataset:
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
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
inst✝⁸ : IsDomain R
inst✝⁷ : IsDomain S
inst✝⁶ : Algebra K L
inst✝⁵ : Module.Finite R S
inst✝⁴ : Algebra R L
inst✝³ : IsScalarTower R S L
inst✝² : IsScalarTower R K L
inst✝¹ : Algebra.IsAlgebraic R S
inst✝ : IsTorsionFree R K
hp : p ≠ ⊤
b : Set S
hb' : Submodule.span R b ⊔ Submodule.restrictScalars R (map f p) = ⊤
hRL : Function.Injective ⇑(algebraMap R L)
M : Submodule R S := Submodule.span R b
n : ℕ
a : Fin n → S ⧸ M
ha : Submodule.span R (Set.range a) = ⊤
smul_top_eq : p • ⊤ = ⊤
exists_sum : ∀ (x : S ⧸ M), ∃ a', (∀ (i : Fin n), a' i ∈ p) ∧ ∑ i, a' i • a i = x
A' : Fin n → Fin n → R
hA'p : ∀ (i i_1 : Fin n), A' i i_1 ∈ p
hA' : ∀ (i : Fin n), ∑ i_1, A' i i_1 • a i_1 = a i
A : Matrix (Fin n) (Fin n) R := Matrix.of A' - 1
B : Matrix (Fin n) (Fin n) R := A.adjugate
A_smul : ∀ (i : Fin n), ∑ j, A i j • a j = 0
d_smul : ∀ (i : Fin n), A.det • a i = 0
x : S
hx : x ∈ S ∙ f A.det
⊢ x ∈ M

Tactic:
obtain ⟨x', rfl⟩ := Submodule.mem_span_singleton.mp hx

Goal state after:
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
inst✝⁸ : IsDomain R
inst✝⁷ : IsDomain S
inst✝⁶ : Algebra K L
inst✝⁵ : Module.Finite R S
inst✝⁴ : Algebra R L
inst✝³ : IsScalarTower R S L
inst✝² : IsScalarTower R K L
inst✝¹ : Algebra.IsAlgebraic R S
inst✝ : IsTorsionFree R K
hp : p ≠ ⊤
b : Set S
hb' : Submodule.span R b ⊔ Submodule.restrictScalars R (map f p) = ⊤
hRL : Function.Injective ⇑(algebraMap R L)
M : Submodule R S := Submodule.span R b
n : ℕ
a : Fin n → S ⧸ M
ha : Submodule.span R (Set.range a) = ⊤
smul_top_eq : p • ⊤ = ⊤
exists_sum : ∀ (x : S ⧸ M), ∃ a', (∀ (i : Fin n), a' i ∈ p) ∧ ∑ i, a' i • a i = x
A' : Fin n → Fin n → R
hA'p : ∀ (i i_1 : Fin n), A' i i_1 ∈ p
hA' : ∀ (i : Fin n), ∑ i_1, A' i i_1 • a i_1 = a i
A : Matrix (Fin n) (Fin n) R := Matrix.of A' - 1
B : Matrix (Fin n) (Fin n) R := A.adjugate
A_smul : ∀ (i : Fin n), ∑ j, A i j • a j = 0
d_smul : ∀ (i : Fin n), A.det • a i = 0
x' : S
hx : x' • f A.det ∈ S ∙ f A.det
⊢ x' • f A.det ∈ M
Module: Mathlib.NumberTheory.RamificationInertia.HilbertTheory

Goal state before:
pp: K : Type u_2
L : Type u_3
B : Type u_4
inst✝²⁰ : Field K
inst✝¹⁹ : Field L
inst✝¹⁸ : Algebra K L
inst✝¹⁷ : CommRing B
P : Ideal B
inst✝¹⁶ : Algebra 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
hP : P.IsPrime
inst✝² : Finite ↥(stabilizer Gal(L/K) P)
inst✝¹ : IsIntegrallyClosed 𝓞D
inst✝ : Algebra.IsIntegral 𝓞D B
⊢ 𝓟D.primesOver B = {P}

Tactic:
have := IsGaloisGroup.of_isFractionRing (stabilizer Gal(L/K) P) 𝓞D B D L
  refine Set.eq_singleton_iff_unique_mem.mpr ⟨⟨hP, hD⟩, ?_⟩
  rintro Q ⟨_, _⟩
  obtain ⟨σ, rfl⟩ := exists_smul_eq_of_isGaloisGroup 𝓟D P Q (stabilizer Gal(L/K) P)
  exact σ.prop

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

Goal state before:

Tactic:
‖F.aeval z'‖ = ‖q‖ * ‖z1‖ ^ 2 := by simp [heq]
    _ ≤ 1 * ‖z1‖ ^ 2 := by gcongr; apply PadicInt.norm_le_one
    _ = ‖F.aeval z‖ ^ 2 / ‖F.derivative.aeval a‖ ^ 2 := by simp [hzeq, hz.1, div_pow]
    _ ≤ (‖F.derivative.aeval a‖ ^ 2 * T ^ 2 ^ n) ^ 2 / ‖F.derivative.aeval a‖ ^ 2 := by
      gcongr
      exact hz.2
    _ = (‖F.derivative.aeval a‖ ^ 2) ^ 2 * (T ^ 2 ^ n) ^ 2 / ‖F.derivative.aeval a‖ ^ 2 := by
      simp only [mul_pow]
    _ = ‖F.derivative.aeval a‖ ^ 2 * (T ^ 2 ^ n) ^ 2 := div_sq_cancel _ _
    _ = ‖F.derivative.aeval a‖ ^ 2 * T ^ 2 ^ (n + 1) := by rw [← pow_mul, pow_succ 2]

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

Goal state before:
pp: case hg
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
⊢ ‖(Polynomial.aeval a) F‖ < ‖(Polynomial.aeval a) (Polynomial.derivative F)‖ ^ 2

Tactic:
assumption

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 : ℕ
this : 2 ≤ 2 ^ (n + 1)
⊢ ‖(Polynomial.aeval a) F‖ < ‖(Polynomial.aeval a) (Polynomial.derivative F)‖ ^ 2

Tactic:
assumption

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
k : ℕ
_h : 0 < k + 2
⊢ (Polynomial.aeval a) F ≠ 0

Tactic:
assumption

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

Goal state before:
pp: case refine_5
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.ramificationIdxIn B * p.inertiaDegIn B ≤ 𝓟D.ramificationIdxIn B * 𝓟D.inertiaDegIn B

Tactic:
· have := ncard_primesOver_mul_ramificationIdxIn_mul_inertiaDegIn 𝓟D B (stabilizer Gal(L/K) P)
    rw [primesOver_eq_singleton K L P D 𝓞D, Set.ncard_singleton, one_mul] at this
    rw [this, IsGaloisGroup.card_eq_finrank (stabilizer Gal(L/K) P) D L,
      IsDecompositionField.rank_left A K L P D hp]

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
⊢ ‖(Polynomial.aeval a) F‖ < ‖(Polynomial.aeval a) (Polynomial.derivative F)‖ ^ 2

Tactic:
assumption

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

Goal state before:
pp: case hnsol
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
⊢ (Polynomial.aeval a) F ≠ 0

Tactic:
assumption

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

Goal state before:
pp: 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
right✝ : 𝓟D ≠ ⊥
this : 𝓟D.inertiaDegIn B = 𝓟D.inertiaDeg A * 𝓟D.inertiaDegIn B
⊢ 𝓟D.inertiaDeg A = 1

Tactic:
right_eq_mul₀ <| inertiaDegIn_ne_zero (stabilizer Gal(L/K) P)

Goal state after:
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
right✝ : 𝓟D ≠ ⊥
this : 𝓟D.inertiaDeg A = 1
⊢ 𝓟D.inertiaDeg A = 1
Module: Mathlib.NumberTheory.SelbergSieve

Goal state before:
pp: s : BoundingSieve
muPlus : ℕ → ℝ
h : IsUpperMoebius muPlus
⊢ siftedSum ≤ ∑ d ∈ s.prodPrimes.divisors, muPlus d * multSum d

Tactic:
have hμ : ∀ n, (if n = 1 then 1 else 0) ≤ ∑ d ∈ n.divisors, muPlus d := h

Goal state after:
s : BoundingSieve
muPlus : ℕ → ℝ
h : IsUpperMoebius muPlus
hμ : ∀ (n : ℕ), (if n = 1 then 1 else 0) ≤ ∑ d ∈ n.divisors, muPlus d
⊢ siftedSum ≤ ∑ d ∈ s.prodPrimes.divisors, muPlus d * multSum d
Module: Mathlib.NumberTheory.SelbergSieve

Goal state before:
pp: f : ℕ → ℕ → ℕ → ℝ
n d : ℕ
hd : d ∣ n ∧ n ≠ 0
this : ∀ (d1 d2 : ℕ), (d1 ∣ d ∧ d2 ∣ d ∧ d = d1.lcm d2) = (d = d1.lcm d2)
⊢ (∑ x ∈ n.divisors with x ∣ d, ∑ x_1 ∈ n.divisors with x_1 ∣ d, if d = x.lcm x_1 then f x x_1 d else 0) =
    ∑ d1 ∈ n.divisors, ∑ d2 ∈ n.divisors, if d = d1.lcm d2 then f d1 d2 d else 0

Tactic:
sum_filter,

Goal state after:
f : ℕ → ℕ → ℕ → ℝ
n d : ℕ
hd : d ∣ n ∧ n ≠ 0
this : ∀ (d1 d2 : ℕ), (d1 ∣ d ∧ d2 ∣ d ∧ d = d1.lcm d2) = (d = d1.lcm d2)
⊢ (∑ a ∈ n.divisors,
      if a ∣ d then ∑ a_1 ∈ n.divisors, if a_1 ∣ d then if d = a.lcm a_1 then f a a_1 d else 0 else 0 else 0) =
    ∑ d1 ∈ n.divisors, ∑ d2 ∈ n.divisors, if d = d1.lcm d2 then f d1 d2 d else 0
Module: Mathlib.NumberTheory.RamificationInertia.Basic

Goal state before:
pp: case h
R : Type u
inst✝¹⁵ : CommRing R
S : Type v
inst✝¹⁴ : CommRing S
inst✝¹³ : Algebra R S
K : Type u_1
inst✝¹² : Field K
inst✝¹¹ : Algebra R K
V : Type u_3
V' : Type u_4
V'' : Type u_5
inst✝¹⁰ : AddCommGroup V
inst✝⁹ : Module R V
inst✝⁸ : Module K V
inst✝⁷ : IsScalarTower R K V
inst✝⁶ : AddCommGroup V'
inst✝⁵ : Module R V'
inst✝⁴ : Module S V'
inst✝³ : IsScalarTower R S V'
inst✝² : AddCommGroup V''
inst✝¹ : Module R V''
hRK : IsFractionRing R K
inst✝ : IsDedekindDomain R
hRS : RingHom.ker f ≠ ⊤
F : V'' →ₗ[R] V
hf : Function.Injective ⇑F
f' : V'' →ₗ[R] V'
ι : Type u_6
b : ι → V''
s : Finset ι
g : ι → K
eq✝ : ∑ i ∈ s, g i • (⇑F ∘ b) i = 0
j' : ι
hj's : j' ∈ s
hj'g : ¬g j' = 0
a : K
j : ι
hjs : j ∈ s
hgI✝ : a * g j ∉ ↑(RingHom.ker f)
g'' : (i : ι) → i ∈ s → R
hg'' : ∀ (i : ι) (a_1 : i ∈ s), (algebraMap R K) (g'' i a_1) = a * g i
this : (a : Prop) → Decidable a := Classical.propDecidable
g' : ι → R := fun i ↦ if h : i ∈ s then g'' i h else 0
hg' : ∀ i ∈ s, (algebraMap R K) (g' i) = a * g i
hgI : f (g' j) ≠ 0
eq : F (∑ i ∈ s, g' i • b i) = 0
⊢ ∑ i ∈ s, (fun i ↦ f (g' i)) i • (⇑f' ∘ b) i = 0

Tactic:
simp only [IsScalarTower.algebraMap_smul, ← map_smul, ← map_sum,
    (F.map_eq_zero_iff hf).mp eq, map_zero, (· ∘ ·)]

Goal state after:
Module: Mathlib.NumberTheory.SelbergSieve

Goal state before:
pp: s : BoundingSieve
⊢ ∀ n > 0,
    (n ∈ fun x ↦ ∃ c, s.prodPrimes = x * c) → ∑ x ∈ n.divisorsAntidiagonal, ↑(μ x.1) * (s.nu x.2)⁻¹ = (selbergTerms n)⁻¹

Tactic:
intro l _ hlP

Goal state after:
s : BoundingSieve
l : ℕ
a✝ : l > 0
hlP : l ∈ fun x ↦ ∃ c, s.prodPrimes = x * c
⊢ ∑ x ∈ l.divisorsAntidiagonal, ↑(μ x.1) * (s.nu x.2)⁻¹ = (selbergTerms l)⁻¹
Module: Mathlib.NumberTheory.SelbergSieve

Goal state before:
pp: 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,
      ∑ x_1 ∈ s.prodPrimes.divisors with x ∣ x_1,
        ∑ i ∈ s.prodPrimes.divisors with x ∣ i, (selbergTerms x)⁻¹ * (s.nu x_1 * w x_1 * (s.nu i * w i))

Tactic:
sum_filter,

Goal state after:
s : BoundingSieve
w : ℕ → ℝ
⊢ (∑ x ∈ s.prodPrimes.divisors,
      ∑ x_1 ∈ s.prodPrimes.divisors,
        ∑ a ∈ s.prodPrimes.divisors,
          if x ∣ x_1.gcd a then (selbergTerms x)⁻¹ * (s.nu x_1 * w x_1) * (s.nu a * w a) else 0) =
    ∑ x ∈ s.prodPrimes.divisors,
      ∑ a ∈ s.prodPrimes.divisors,
        if x ∣ a then
          ∑ a_1 ∈ s.prodPrimes.divisors, if x ∣ a_1 then (selbergTerms x)⁻¹ * (s.nu a * w a * (s.nu a_1 * w a_1)) else 0
        else 0
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
inst✝¹ : p.IsMaximal
inst✝ : P.IsPrime
hP0 : P ≠ ⊥
i : ℕ
hi : i ≤ e
Q : ℕ → Prop := fun i ↦ Module.rank (R ⧸ p) ↥(map (Quotient.mk (P ^ e)) (P ^ i)) = (e - i) • Module.rank (R ⧸ p) (S ⧸ P)
j : ℕ
lt_e : j < e
_le_j : i ≤ j
ih : Q (j + 1)
⊢ P ≠ ⊥

Tactic:
assumption

Goal state after:
Module: Mathlib.Order.CompleteSublattice

Goal state before:
pp: α : Type u_1
inst✝ : CompleteLattice α
L : CompleteSublattice α
S : Set ↥L
⊢ ↑(sInf S) = ⨅ N ∈ S, ↑N

Tactic:
coe_sInf,

Goal state after:
α : Type u_1
inst✝ : CompleteLattice α
L : CompleteSublattice α
S : Set ↥L
⊢ sInf {x | ∃ s ∈ S, ↑s = x} = ⨅ N ∈ S, ↑N
Module: Mathlib.Order.Concept

Goal state before:
pp: α : Type u_2
r' : α → α → Prop
c' : Concept α α r'
inst✝ : IsTrans α r'
x y : α
hy : r' x y
hx : x ∈ c'.intent
⊢ y ∈ c'.intent

Tactic:
rw [← upperPolar_extent]

Goal state after:
α : Type u_2
r' : α → α → Prop
c' : Concept α α r'
inst✝ : IsTrans α r'
x y : α
hy : r' x y
hx : x ∈ c'.intent
⊢ y ∈ upperPolar r' c'.extent
Module: Mathlib.Order.Concept

Goal state before:
pp: α : Type u_2
r' : α → α → Prop
c' : Concept α α r'
inst✝¹ : Std.Trichotomous r'
inst✝ : IsTrans α r'
x : α
x✝ : x ∈ ⊤
hx : x ∉ c'.extent
⊢ x ∈ c'.intent

Tactic:
rw [← upperPolar_extent]

Goal state after:
α : Type u_2
r' : α → α → Prop
c' : Concept α α r'
inst✝¹ : Std.Trichotomous r'
inst✝ : IsTrans α r'
x : α
x✝ : x ∈ ⊤
hx : x ∉ c'.extent
⊢ x ∈ upperPolar r' c'.extent
Module: Mathlib.Order.Concept

Goal state before:
pp: case inl
α : Type u_6
inst✝ : PartialOrder α
c : Concept α α fun x1 x2 ↦ x1 < x2
b : α
hb : b ≤ b
ha : b ∈ c.extent
⊢ b ∈ c.extent

Tactic:
assumption

Goal state after:
Module: Mathlib.Order.Concept

Goal state before:
pp: case inl
α : Type u_6
inst✝ : PartialOrder α
c : Concept α α fun x1 x2 ↦ x1 < x2
a : α
ha : a ∈ c.intent
hb : a ≤ a
⊢ a ∈ c.intent

Tactic:
assumption

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 α
⊢ CountableSupClosed {a | ∃ A, ∃ (_ : A ⊆ s) (_ : A.Nonempty) (_ : A.Countable), IsLUB A a}

Tactic:
constructor
    intro A hA hA_ne hAc x hx
    choose B hB hB_ne hBc hB_lub using hA
    refine ⟨⋃ a : A, B a.2, by simp; grind, ?_, ?_, ?_⟩
    · obtain ⟨a, ha⟩ := hA_ne
      simp
      grind
    · have : Countable A := Set.countable_coe_iff.mpr hAc
      exact Set.countable_iUnion fun a ↦ hBc a.2
    · have : Nonempty A := Set.nonempty_coe_sort.mpr hA_ne
      rw [← isLUB_iUnion_iff_of_isLUB (u := fun a : A ↦ a.1) (fun a ↦ hB_lub a.2)]
      simpa

Goal state after:
Module: Mathlib.Order.Height

Goal state before:
pp: α : Type u_1
s : Set α
r : α → α → Prop
⊢ s.chainHeight r = 0 ↔ s = ∅

Tactic:
refine ⟨fun h ↦ ?_, ?_⟩
  · simp only [chainHeight, iSup_eq_zero, encard_eq_zero, Subtype.forall, and_imp] at h
    ext x
    simpa using h {x}
  · simp_all [chainHeight]

Goal state after:
Module: Mathlib.NumberTheory.WellApproximable

Goal state before:
pp: A : Type u_1
inst✝⁵ : NormedAddCommGroup A
inst✝⁴ : CompactSpace A
inst✝³ : PreconnectedSpace A
inst✝² : MeasurableSpace A
inst✝¹ : BorelSpace A
μ : Measure A
inst✝ : μ.IsAddHaarMeasure
ξ : A
n : ℕ
hn : 0 < n
δ : ℝ
hδ : μ univ ≤ (n + 1) • μ (closedBall 0 (δ / 2))
⊢ ∃ j ∈ Icc 1 n, ‖j • ξ‖ ≤ δ

Tactic:
let B : Icc 0 n → Set A := fun j ↦ closedBall ((j : ℕ) • ξ) (δ / 2)
  have hB : ∀ j, IsClosed (B j) := fun j ↦ isClosed_closedBall
  suffices ¬ Pairwise (Disjoint on B) by
    obtain ⟨i, j, hij, x, hx⟩ := exists_lt_mem_inter_of_not_pairwise_disjoint this
    refine ⟨j - i, ⟨le_tsub_of_add_le_left hij, ?_⟩, ?_⟩
    · simpa only [tsub_le_iff_right] using j.property.2.trans le_self_add
    · rw [sub_nsmul _ (Subtype.coe_le_coe.mpr hij.le), ← sub_eq_add_neg, ← dist_eq_norm]
      exact (dist_triangle ((j : ℕ) • ξ) x ((i : ℕ) • ξ)).trans (by
        linarith [mem_closedBall.mp hx.1, mem_closedBall'.mp hx.2])
  by_contra h
  apply hn.ne'
  have h' : ⋃ j, B j = univ := by
    rw [← (isClosed_iUnion_of_finite hB).measure_eq_univ_iff_eq (μ := μ)]
    refine le_antisymm (μ.mono (subset_univ _)) ?_
    simp_rw [measure_iUnion h (fun _ ↦ measurableSet_closedBall), tsum_fintype,
      B, μ.addHaar_closedBall_center, Finset.sum_const, Finset.card_univ, Fintype.card_Icc,
      Nat.card_Icc, tsub_zero]
    exact hδ
  replace hδ : 0 ≤ δ / 2 := by
    by_contra contra
    refine (isOpen_univ.measure_pos μ univ_nonempty).not_ge <| hδ.trans ?_
    suffices μ (closedBall 0 (δ / 2)) = 0 by simp [this]
    rw [not_le, ← closedBall_eq_empty (x := (0 : A))] at contra
    simp [contra]
  have h'' : ∀ j, (B j).Nonempty := by intro j; rwa [nonempty_closedBall]
  simpa using subsingleton_of_disjoint_isClosed_iUnion_eq_univ h'' h hB h'

Goal state after:
Module: Mathlib.Order.KonigLemma

Goal state before:
pp: α : ℕ → Type u_1
inst✝¹ : Finite (α 0)
inst✝ : ∀ (i : ℕ), Nonempty (α i)
π : {i j : ℕ} → i ≤ j → α j → α i
π_refl : ∀ ⦃i : ℕ⦄ (a : α i), π ⋯ a = a
π_trans : ∀ ⦃i j k : ℕ⦄ (hij : i ≤ j) (hjk : j ≤ k) (a : α k), π hij (π hjk a) = π ⋯ a
hfin : ∀ (i : ℕ) (a : α i), {b | π ⋯ b = a}.Finite
αs : Type u_1 := (i : ℕ) × α i
x✝¹ : PartialOrder αs :=
  { le := fun a b ↦ ∃ (h : a.fst ≤ b.fst), π h b.snd = a.snd, le_refl := ⋯, le_trans := ⋯, lt_iff_le_not_ge := ⋯,
    le_antisymm := ⋯ }
i j : ℕ
b : α j
h : i ≤ j
x✝ :
  ¬⟨i, π h b⟩ = ⟨j, b⟩ ∧
    ∀ (a : ℕ) (b_1 : α a), ⟨i, π h b⟩ ≤ ⟨a, b_1⟩ → ⟨a, b_1⟩ ≤ ⟨j, b⟩ → ¬⟨a, b_1⟩ = ⟨i, π h b⟩ → ⟨a, b_1⟩ = ⟨j, b⟩
hne : ¬⟨i, π h b⟩ = ⟨j, b⟩
h' : ∀ (a : ℕ) (b_1 : α a), ⟨i, π h b⟩ ≤ ⟨a, b_1⟩ → ⟨a, b_1⟩ ≤ ⟨j, b⟩ → ¬⟨a, b_1⟩ = ⟨i, π h b⟩ → ⟨a, b_1⟩ = ⟨j, b⟩
hle' : i + 1 ≤ j
⊢ π ⋯ ⟨i + 1, π hle' b⟩.snd = ⟨i, π h b⟩.snd

Tactic:
π_trans

Goal state after:
α : ℕ → Type u_1
inst✝¹ : Finite (α 0)
inst✝ : ∀ (i : ℕ), Nonempty (α i)
π : {i j : ℕ} → i ≤ j → α j → α i
π_refl : ∀ ⦃i : ℕ⦄ (a : α i), π ⋯ a = a
π_trans : ∀ ⦃i j k : ℕ⦄ (hij : i ≤ j) (hjk : j ≤ k) (a : α k), π hij (π hjk a) = π ⋯ a
hfin : ∀ (i : ℕ) (a : α i), {b | π ⋯ b = a}.Finite
αs : Type u_1 := (i : ℕ) × α i
x✝¹ : PartialOrder αs :=
  { le := fun a b ↦ ∃ (h : a.fst ≤ b.fst), π h b.snd = a.snd, le_refl := ⋯, le_trans := ⋯, lt_iff_le_not_ge := ⋯,
    le_antisymm := ⋯ }
i j : ℕ
b : α j
h : i ≤ j
x✝ :
  ¬⟨i, π h b⟩ = ⟨j, b⟩ ∧
    ∀ (a : ℕ) (b_1 : α a), ⟨i, π h b⟩ ≤ ⟨a, b_1⟩ → ⟨a, b_1⟩ ≤ ⟨j, b⟩ → ¬⟨a, b_1⟩ = ⟨i, π h b⟩ → ⟨a, b_1⟩ = ⟨j, b⟩
hne : ¬⟨i, π h b⟩ = ⟨j, b⟩
h' : ∀ (a : ℕ) (b_1 : α a), ⟨i, π h b⟩ ≤ ⟨a, b_1⟩ → ⟨a, b_1⟩ ≤ ⟨j, b⟩ → ¬⟨a, b_1⟩ = ⟨i, π h b⟩ → ⟨a, b_1⟩ = ⟨j, b⟩
hle' : i + 1 ≤ j
⊢ π ⋯ b = ⟨i, π h b⟩.snd
Module: Mathlib.Order.PrimeIdeal

Goal state before:
pp: P : Type u_1
inst✝ : Preorder P
IF : PrimePair P
⊢ IsPFilter ↑IF.F

Tactic:
exact IF.F.isPFilter

Goal state after:
Module: Mathlib.Order.KonigLemma

Goal state before:
pp: α : ℕ → Type u_1
inst✝¹ : Finite (α 0)
inst✝ : ∀ (i : ℕ), Nonempty (α i)
π : {i j : ℕ} → i ≤ j → α j → α i
π_refl : ∀ ⦃i : ℕ⦄ (a : α i), π ⋯ a = a
π_trans : ∀ ⦃i j k : ℕ⦄ (hij : i ≤ j) (hjk : j ≤ k) (a : α k), π hij (π hjk a) = π ⋯ a
hfin : ∀ (i : ℕ) (a : α i), {b | π ⋯ b = a}.Finite
αs : Type u_1 := (i : ℕ) × α i
x✝² : PartialOrder αs :=
  { le := fun a b ↦ ∃ (h : a.fst ≤ b.fst), π h b.snd = a.snd, le_refl := ⋯, le_trans := ⋯, lt_iff_le_not_ge := ⋯,
    le_antisymm := ⋯ }
hcovby : ∀ {a b : αs}, a ⋖ b ↔ a ≤ b ∧ a.fst + 1 = b.fst
this : IsStronglyAtomic αs
a₀ : αs
ha₀ : a₀.fst = 0
ha₀inf : (Ici a₀).Infinite
x✝¹ : αs
i : ℕ
a : α i
j : ℕ
b : α j
x✝ : ⟨i, a⟩ ≤ ⟨j, b⟩
hj : i + 1 = j
w✝ : ⟨i, a⟩.fst ≤ ⟨j, b⟩.fst
h✝ : π w✝ ⟨j, b⟩.snd = ⟨i, a⟩.snd
⊢ π ⋯ (π ⋯ b) = a

Tactic:
π_trans

Goal state after:
α : ℕ → Type u_1
inst✝¹ : Finite (α 0)
inst✝ : ∀ (i : ℕ), Nonempty (α i)
π : {i j : ℕ} → i ≤ j → α j → α i
π_refl : ∀ ⦃i : ℕ⦄ (a : α i), π ⋯ a = a
π_trans : ∀ ⦃i j k : ℕ⦄ (hij : i ≤ j) (hjk : j ≤ k) (a : α k), π hij (π hjk a) = π ⋯ a
hfin : ∀ (i : ℕ) (a : α i), {b | π ⋯ b = a}.Finite
αs : Type u_1 := (i : ℕ) × α i
x✝² : PartialOrder αs :=
  { le := fun a b ↦ ∃ (h : a.fst ≤ b.fst), π h b.snd = a.snd, le_refl := ⋯, le_trans := ⋯, lt_iff_le_not_ge := ⋯,
    le_antisymm := ⋯ }
hcovby : ∀ {a b : αs}, a ⋖ b ↔ a ≤ b ∧ a.fst + 1 = b.fst
this : IsStronglyAtomic αs
a₀ : αs
ha₀ : a₀.fst = 0
ha₀inf : (Ici a₀).Infinite
x✝¹ : αs
i : ℕ
a : α i
j : ℕ
b : α j
x✝ : ⟨i, a⟩ ≤ ⟨j, b⟩
hj : i + 1 = j
w✝ : ⟨i, a⟩.fst ≤ ⟨j, b⟩.fst
h✝ : π w✝ ⟨j, b⟩.snd = ⟨i, a⟩.snd
⊢ π ⋯ b = a