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

Goal state before:
pp: case hH.refine_2
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
⊢ ∃ k, ⋯.unit ^ k = γ

Tactic:
·

Goal state after:
case hH.refine_2
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
⊢ ∃ k, ⋯.unit ^ k = γ
Module: Mathlib.NumberTheory.SelbergSieve

Goal state before:
pp: case pos
weights : ℕ → ℝ
hw : weights 1 = 1
n : ℕ
h✝ : n = 1
⊢ 1 ≤ ∑ d ∈ n.divisors, ∑ d1 ∈ d.divisors, ∑ d2 ∈ d.divisors, if d = d1.lcm d2 then weights d1 * weights d2 else 0

pp: case neg
weights : ℕ → ℝ
hw : weights 1 = 1
n : ℕ
h✝ : ¬n = 1
⊢ 0 ≤ ∑ d ∈ n.divisors, ∑ d1 ∈ d.divisors, ∑ d2 ∈ d.divisors, if d = d1.lcm d2 then weights d1 * weights d2 else 0

Tactic:
·

Goal state after:
case pos
weights : ℕ → ℝ
hw : weights 1 = 1
n : ℕ
h✝ : n = 1
⊢ 1 ≤ ∑ d ∈ n.divisors, ∑ d1 ∈ d.divisors, ∑ d2 ∈ d.divisors, if d = d1.lcm d2 then weights d1 * weights d2 else 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.IsNontrivial
inst✝¹ : IsTrivialOn K v
hle : v X ≤ 1
inst✝ : v.IsRankOneDiscrete
⊢ v 0 ≤ 1 ↔ (valuation K⟮X⟯ Pᵥ) 0 ≤ 1

pp: case inr
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
f : K⟮X⟯
hf0 : f ≠ 0
⊢ v f ≤ 1 ↔ (valuation K⟮X⟯ Pᵥ) f ≤ 1

Tactic:
·

Goal state after:
case inl
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
⊢ v 0 ≤ 1 ↔ (valuation K⟮X⟯ Pᵥ) 0 ≤ 1
Module: Mathlib.NumberTheory.RatFunc.Ostrowski

Goal state before:
pp: case inr
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
f : K⟮X⟯
hf0 : f ≠ 0
⊢ v f ≤ 1 ↔ (valuation K⟮X⟯ Pᵥ) f ≤ 1

Tactic:
·

Goal state after:
case inr
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
f : K⟮X⟯
hf0 : f ≠ 0
⊢ v f ≤ 1 ↔ (valuation K⟮X⟯ Pᵥ) f ≤ 1
Module: Mathlib.NumberTheory.SumFourSquares

Goal state before:
pp: case inl
hp : Fact (Nat.Prime 2)
⊢ ∃ a b k, 0 < k ∧ k < 2 ∧ a ^ 2 + b ^ 2 + 1 = k * 2

pp: case inr
p : ℕ
hp : Fact (Nat.Prime p)
hodd : Odd p
⊢ ∃ a b k, 0 < k ∧ k < p ∧ a ^ 2 + b ^ 2 + 1 = k * p

Tactic:
·

Goal state after:
case inl
hp : Fact (Nat.Prime 2)
⊢ ∃ a b k, 0 < k ∧ k < 2 ∧ a ^ 2 + b ^ 2 + 1 = k * 2
Module: Mathlib.NumberTheory.SelbergSieve

Goal state before:
pp: case pos
s : BoundingSieve
d : ℕ
h : d = 0
⊢ (s.nu.pmul (prodPrimeFactors fun p ↦ (1 - s.nu p)⁻¹)) d = s.nu d * ∏ p ∈ d.primeFactors, (1 - s.nu p)⁻¹

pp: case neg
s : BoundingSieve
d : ℕ
h : ¬d = 0
⊢ (s.nu.pmul (prodPrimeFactors fun p ↦ (1 - s.nu p)⁻¹)) d = s.nu d * ∏ p ∈ d.primeFactors, (1 - s.nu p)⁻¹

Tactic:
·

Goal state after:
case pos
s : BoundingSieve
d : ℕ
h : d = 0
⊢ (s.nu.pmul (prodPrimeFactors fun p ↦ (1 - s.nu p)⁻¹)) d = s.nu d * ∏ p ∈ d.primeFactors, (1 - s.nu p)⁻¹
Module: Mathlib.NumberTheory.SumFourSquares

Goal state before:
pp: case inr.refine_1
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₀ : 0 < ↑k
hk : a ^ 2 + b ^ 2 + 1 ^ 2 + 0 ^ 2 = k * p
⊢ 2 * a < p

pp: case inr.refine_2
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₀ : 0 < ↑k
hk : a ^ 2 + b ^ 2 + 1 ^ 2 + 0 ^ 2 = k * p
⊢ 2 * b < p

pp: case inr.refine_3
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₀ : 0 < ↑k
hk : a ^ 2 + b ^ 2 + 1 ^ 2 + 0 ^ 2 = k * p
⊢ 2 * 1 < p

pp: case inr.refine_4
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₀ : 0 < ↑k
hk : a ^ 2 + b ^ 2 + 1 ^ 2 + 0 ^ 2 = k * p
⊢ 2 * 0 < p

Tactic:
·

Goal state after:
case inr.refine_1
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₀ : 0 < ↑k
hk : a ^ 2 + b ^ 2 + 1 ^ 2 + 0 ^ 2 = k * p
⊢ 2 * a < p
Module: Mathlib.NumberTheory.SumFourSquares

Goal state before:
pp: case inr.refine_2
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₀ : 0 < ↑k
hk : a ^ 2 + b ^ 2 + 1 ^ 2 + 0 ^ 2 = k * p
⊢ 2 * b < p

pp: case inr.refine_3
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₀ : 0 < ↑k
hk : a ^ 2 + b ^ 2 + 1 ^ 2 + 0 ^ 2 = k * p
⊢ 2 * 1 < p

pp: case inr.refine_4
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₀ : 0 < ↑k
hk : a ^ 2 + b ^ 2 + 1 ^ 2 + 0 ^ 2 = k * p
⊢ 2 * 0 < p

Tactic:
·

Goal state after:
case inr.refine_2
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₀ : 0 < ↑k
hk : a ^ 2 + b ^ 2 + 1 ^ 2 + 0 ^ 2 = k * p
⊢ 2 * b < p
Module: Mathlib.NumberTheory.SumFourSquares

Goal state before:
pp: case inr.refine_3
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₀ : 0 < ↑k
hk : a ^ 2 + b ^ 2 + 1 ^ 2 + 0 ^ 2 = k * p
⊢ 2 * 1 < p

pp: case inr.refine_4
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₀ : 0 < ↑k
hk : a ^ 2 + b ^ 2 + 1 ^ 2 + 0 ^ 2 = k * p
⊢ 2 * 0 < p

Tactic:
·

Goal state after:
case inr.refine_3
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₀ : 0 < ↑k
hk : a ^ 2 + b ^ 2 + 1 ^ 2 + 0 ^ 2 = k * p
⊢ 2 * 1 < p
Module: Mathlib.NumberTheory.SumFourSquares

Goal state before:
pp: case inr.refine_4
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₀ : 0 < ↑k
hk : a ^ 2 + b ^ 2 + 1 ^ 2 + 0 ^ 2 = k * p
⊢ 2 * 0 < p

Tactic:
·

Goal state after:
case inr.refine_4
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₀ : 0 < ↑k
hk : a ^ 2 + b ^ 2 + 1 ^ 2 + 0 ^ 2 = k * p
⊢ 2 * 0 < p
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
⊢ Xor (v.IsEquiv (inftyValuation K)) (∃! u, v.IsEquiv (valuation K⟮X⟯ u))

pp: case inr
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⟯
hge : v X ≤ 1
⊢ Xor (v.IsEquiv (inftyValuation K)) (∃! u, v.IsEquiv (valuation K⟮X⟯ u))

Tactic:
·

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
⊢ Xor (v.IsEquiv (inftyValuation K)) (∃! u, v.IsEquiv (valuation K⟮X⟯ u))
Module: Mathlib.NumberTheory.RatFunc.Ostrowski

Goal state before:
pp: case inr
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⟯
hge : v X ≤ 1
⊢ Xor (v.IsEquiv (inftyValuation K)) (∃! u, v.IsEquiv (valuation K⟮X⟯ u))

Tactic:
·

Goal state after:
case inr
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⟯
hge : v X ≤ 1
⊢ Xor (v.IsEquiv (inftyValuation K)) (∃! u, v.IsEquiv (valuation K⟮X⟯ u))
Module: Mathlib.NumberTheory.SelbergSieve

Goal state before:
pp: 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)

Tactic:
Nat.divisors_filter_dvd_of_dvd prodPrimes_ne_zero hd,

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

Goal state before:
pp: case a
s : BoundingSieve
d : ℕ
hd : d ∣ s.prodPrimes
l : ℕ
hl : (l ∣ s.prodPrimes ∧ ¬s.prodPrimes = 0) ∧ l ∣ d
⊢ selbergTerms d / selbergTerms l = selbergTerms d * (selbergTerms l)⁻¹

pp: case a.hl
s : BoundingSieve
d : ℕ
hd : d ∣ s.prodPrimes
l : ℕ
hl : (l ∣ s.prodPrimes ∧ ¬s.prodPrimes = 0) ∧ l ∣ d
⊢ (d / l).Coprime l

pp: case a.hd
s : BoundingSieve
d : ℕ
hd : d ∣ s.prodPrimes
l : ℕ
hl : (l ∣ s.prodPrimes ∧ ¬s.prodPrimes = 0) ∧ l ∣ d
⊢ selbergTerms l ≠ 0

Tactic:
·

Goal state after:
case a
s : BoundingSieve
d : ℕ
hd : d ∣ s.prodPrimes
l : ℕ
hl : (l ∣ s.prodPrimes ∧ ¬s.prodPrimes = 0) ∧ l ∣ d
⊢ selbergTerms d / selbergTerms l = selbergTerms d * (selbergTerms l)⁻¹
Module: Mathlib.NumberTheory.SelbergSieve

Goal state before:
pp: case a.hl
s : BoundingSieve
d : ℕ
hd : d ∣ s.prodPrimes
l : ℕ
hl : (l ∣ s.prodPrimes ∧ ¬s.prodPrimes = 0) ∧ l ∣ d
⊢ (d / l).Coprime l

pp: case a.hd
s : BoundingSieve
d : ℕ
hd : d ∣ s.prodPrimes
l : ℕ
hl : (l ∣ s.prodPrimes ∧ ¬s.prodPrimes = 0) ∧ l ∣ d
⊢ selbergTerms l ≠ 0

Tactic:
·

Goal state after:
case a.hl
s : BoundingSieve
d : ℕ
hd : d ∣ s.prodPrimes
l : ℕ
hl : (l ∣ s.prodPrimes ∧ ¬s.prodPrimes = 0) ∧ l ∣ d
⊢ (d / l).Coprime l
Module: Mathlib.NumberTheory.SelbergSieve

Goal state before:
pp: case a.hd
s : BoundingSieve
d : ℕ
hd : d ∣ s.prodPrimes
l : ℕ
hl : (l ∣ s.prodPrimes ∧ ¬s.prodPrimes = 0) ∧ l ∣ d
⊢ selbergTerms l ≠ 0

Tactic:
·

Goal state after:
case a.hd
s : BoundingSieve
d : ℕ
hd : d ∣ s.prodPrimes
l : ℕ
hl : (l ∣ s.prodPrimes ∧ ¬s.prodPrimes = 0) ∧ l ∣ d
⊢ selbergTerms l ≠ 0
Module: Mathlib.NumberTheory.RamificationInertia.Basic

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

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

Tactic:
·

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

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

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

Tactic:
·

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

Goal state before:
pp: s : BoundingSieve
w : ℕ → ℝ
d1 : ℕ
hd1 : d1 ∈ s.prodPrimes.divisors
d2 : ℕ
hd2 : d2 ∈ s.prodPrimes.divisors
h : d1.lcm d2 ∣ s.prodPrimes
⊢ w d1 * w d2 * (s.nu d1 * s.nu d2 / s.nu (d1.gcd d2)) = s.nu d1 * w d1 * s.nu d2 * w d2 * (s.nu (d1.gcd d2))⁻¹

pp: s : BoundingSieve
w : ℕ → ℝ
d1 : ℕ
hd1 : d1 ∈ s.prodPrimes.divisors
d2 : ℕ
hd2 : d2 ∈ s.prodPrimes.divisors
h : d1.lcm d2 ∣ s.prodPrimes
⊢ s.nu (d1.gcd d2) ≠ 0

Tactic:
·

Goal state after:
s : BoundingSieve
w : ℕ → ℝ
d1 : ℕ
hd1 : d1 ∈ s.prodPrimes.divisors
d2 : ℕ
hd2 : d2 ∈ s.prodPrimes.divisors
h : d1.lcm d2 ∣ s.prodPrimes
⊢ w d1 * w d2 * (s.nu d1 * s.nu d2 / s.nu (d1.gcd d2)) = s.nu d1 * w d1 * s.nu d2 * w d2 * (s.nu (d1.gcd d2))⁻¹
Module: Mathlib.NumberTheory.RamificationInertia.Basic

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

Tactic:
·

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

Goal state before:
pp: case inl
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
a b c d : ℕ
hmin : ∀ m < 1, ¬(m < p ∧ 0 < m ∧ ∃ a b c d, a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = m * p)
hmp : 1 < p
hm₀ : 0 < 1
habcd : a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = 1 * p
⊢ ∃ a b c d, a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = p

pp: case 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
⊢ ∃ a b c d, a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = p

Tactic:
·

Goal state after:
case inl
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
a b c d : ℕ
hmin : ∀ m < 1, ¬(m < p ∧ 0 < m ∧ ∃ a b c d, a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = m * p)
hmp : 1 < p
hm₀ : 0 < 1
habcd : a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = 1 * p
⊢ ∃ a b c d, a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = p
Module: Mathlib.NumberTheory.Zsqrtd.GaussianInt

Goal state before:
pp: x y : ℤ[i]
hy : y ≠ 0
⊢ (norm x).natAbs ≤ (norm (x * y)).natAbs

Tactic:
rw [Zsqrtd.norm_mul, Int.natAbs_mul]
  exact le_mul_of_one_le_right (Nat.zero_le _) (Int.ofNat_le.1 (by
    rw [abs_natCast_norm]
    exact Int.add_one_le_of_lt (norm_pos.2 hy)))

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
hpi : Prime ↑p
hp1 : p % 2 = 1
hp3 : p % 4 ≠ 3
k : ℕ
k_lt_p : k < p
hk : -1 = ↑k * ↑k
hpk : p ∣ k ^ 2 + 1
hkmul : ↑k ^ 2 + 1 = { re := ↑k, im := 1 } * { re := ↑k, im := -1 }
hk₀ : k ≠ 0
⊢ 1 + k * k ≤ k * (k + 1)

Tactic:
by lia

Goal state after:
Module: Mathlib.NumberTheory.SumFourSquares

Goal state before:
pp: case pos
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
⊢ False

pp: case neg
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
⊢ False

Tactic:
·

Goal state after:
case pos
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
⊢ False
Module: Mathlib.NumberTheory.SumFourSquares

Goal state before:
pp: case pos
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
a b c d m : ℕ
hmin : ∀ m_1 < 2 * m, ¬(m_1 < p ∧ 0 < m_1 ∧ ∃ a b c d, a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = m_1 * p)
hmp : 2 * m < p
hm₀ : 0 < 2 * m
habcd : a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = 2 * m * p
hm₁ : 1 < 2 * m
this : NeZero (2 * m)
⊢ False

Tactic:
mul_pos_iff_of_pos_left two_pos

Goal state after:
case pos
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
a b c d m : ℕ
hmin : ∀ m_1 < 2 * m, ¬(m_1 < p ∧ 0 < m_1 ∧ ∃ a b c d, a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = m_1 * p)
hmp : 2 * m < p
hm₀ : 0 < m
habcd : a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = 2 * m * p
hm₁ : 1 < 2 * m
this : NeZero (2 * m)
⊢ False
Module: Mathlib.NumberTheory.SumTwoSquares

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

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

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 : ℕ
hp : Nat.Prime p
hq : q ∣ n → q % 4 ≠ 3
hpq : p * q ∣ n
⊢ p * q % 4 ≠ 3

Tactic:
·

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