mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.NumberTheory.NumberField.Ideal.KummerDedekind

Goal state before:
pp: K : Type u_1
inst✝² : Field K
θ✝ : 𝓞 K
inst✝¹ : NumberField K
θ : 𝓞 K
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : ¬p ∣ exponent θ
Q : ℤ[X]
hQ : Polynomial.map (Int.castRingHom (ZMod p)) Q ∈ monicFactorsMod θ p
h₀ : Polynomial.map (Int.castRingHom (ZMod p)) (minpoly ℤ θ) ≠ 0
⊢ span {Polynomial.map (Int.castRingHom (ZMod p)) Q} =
    span {Polynomial.map (Int.castRingHom (ZMod p)) (minpoly ℤ θ)} ⊔ span {Polynomial.map (Int.castRingHom (ZMod p)) Q}

Tactic:
rw [← span_insert, span_pair_comm, span_pair_eq_span_left_iff_dvd.mpr]

Goal state after:
K : Type u_1
inst✝² : Field K
θ✝ : 𝓞 K
inst✝¹ : NumberField K
θ : 𝓞 K
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : ¬p ∣ exponent θ
Q : ℤ[X]
hQ : Polynomial.map (Int.castRingHom (ZMod p)) Q ∈ monicFactorsMod θ p
h₀ : Polynomial.map (Int.castRingHom (ZMod p)) (minpoly ℤ θ) ≠ 0
⊢ Polynomial.map (Int.castRingHom (ZMod p)) Q ∣ Polynomial.map (Int.castRingHom (ZMod p)) (minpoly ℤ θ)
Module: Mathlib.RingTheory.RootsOfUnity.CyclotomicUnits

Goal state before:
pp: A : Type u_1
ζ : A
inst✝⁴ : CommRing A
inst✝³ : IsDomain A
R : Type u_3
inst✝² : CommRing R
inst✝¹ : Algebra R A
n : ℕ
inst✝ : NeZero n
hζ : IsPrimitiveRoot ζ n
σ : A ≃ₐ[R] A
⊢ Associated (ζ - 1) (σ (ζ - 1))

Tactic:
rw [map_sub, map_one, ← hζ.autToPow_spec R σ]

Goal state after:
A : Type u_1
ζ : A
inst✝⁴ : CommRing A
inst✝³ : IsDomain A
R : Type u_3
inst✝² : CommRing R
inst✝¹ : Algebra R A
n : ℕ
inst✝ : NeZero n
hζ : IsPrimitiveRoot ζ n
σ : A ≃ₐ[R] A
⊢ Associated (ζ - 1) (ζ ^ (↑((autToPow R hζ) σ)).val - 1)
Module: Mathlib.RingTheory.RootsOfUnity.CyclotomicUnits

Goal state before:
pp: case hi
A : Type u_1
ζ : A
inst✝⁴ : CommRing A
inst✝³ : IsDomain A
R : Type u_3
inst✝² : CommRing R
inst✝¹ : Algebra R A
n : ℕ
inst✝ : NeZero n
hζ : IsPrimitiveRoot ζ n
σ τ : A ≃ₐ[R] A
⊢ (↑((autToPow R hζ) τ)).val.Coprime n

pp: case hj
A : Type u_1
ζ : A
inst✝⁴ : CommRing A
inst✝³ : IsDomain A
R : Type u_3
inst✝² : CommRing R
inst✝¹ : Algebra R A
n : ℕ
inst✝ : NeZero n
hζ : IsPrimitiveRoot ζ n
σ τ : A ≃ₐ[R] A
⊢ (↑((autToPow R hζ) σ)).val.Coprime n

Tactic:
<;>

Goal state after:
case hi
A : Type u_1
ζ : A
inst✝⁴ : CommRing A
inst✝³ : IsDomain A
R : Type u_3
inst✝² : CommRing R
inst✝¹ : Algebra R A
n : ℕ
inst✝ : NeZero n
hζ : IsPrimitiveRoot ζ n
σ τ : A ≃ₐ[R] A
⊢ (↑((autToPow R hζ) τ)).val.Coprime n

case hj
A : Type u_1
ζ : A
inst✝⁴ : CommRing A
inst✝³ : IsDomain A
R : Type u_3
inst✝² : CommRing R
inst✝¹ : Algebra R A
n : ℕ
inst✝ : NeZero n
hζ : IsPrimitiveRoot ζ n
σ τ : A ≃ₐ[R] A
⊢ (↑((autToPow R hζ) σ)).val.Coprime n
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal

Goal state before:
pp: n m p k : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
P : Ideal (𝓞 K)
hP₁ : P.IsPrime
hP₂ : P.LiesOver 𝒑
hK : IsCyclotomicExtension {p ^ (k + 1)} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
⊢ Prime (hζ.toInteger - 1)

pp: n m p k : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
P : Ideal (𝓞 K)
hP₁ : P.IsPrime
hP₂ : P.LiesOver 𝒑
hK : IsCyclotomicExtension {p ^ (k + 1)} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
⊢ hζ.toInteger - 1 ≠ 0

Tactic:
· exact hζ.zeta_sub_one_prime

Goal state after:
n m p k : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
P : Ideal (𝓞 K)
hP₁ : P.IsPrime
hP₂ : P.LiesOver 𝒑
hK : IsCyclotomicExtension {p ^ (k + 1)} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
⊢ hζ.toInteger - 1 ≠ 0
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal

Goal state before:
pp: p k : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
hK : IsCyclotomicExtension {p ^ (k + 1)} ℚ K
this✝ : IsGalois ℚ K
hζ : IsPrimitiveRoot (zeta (p ^ (k + 1)) ℚ K) (p ^ (k + 1))
h_main : (𝒑.primesOver (𝓞 K)).ncard * ((span {hζ.toInteger - 1}).ramificationIdx ℤ * 1) = Nat.card Gal(K/ℚ)
this : (span {hζ.toInteger - 1}).LiesOver 𝒑
⊢ (𝒑.primesOver (𝓞 K)).ncard = 1

Tactic:
ramificationIdx_span_zeta_sub_one,

Goal state after:
p k : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
hK : IsCyclotomicExtension {p ^ (k + 1)} ℚ K
this✝ : IsGalois ℚ K
hζ : IsPrimitiveRoot (zeta (p ^ (k + 1)) ℚ K) (p ^ (k + 1))
h_main : (𝒑.primesOver (𝓞 K)).ncard * (p ^ k * (p - 1) * 1) = Nat.card Gal(K/ℚ)
this : (span {hζ.toInteger - 1}).LiesOver 𝒑
⊢ (𝒑.primesOver (𝓞 K)).ncard = 1
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal

Goal state before:
pp: n m p k : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
P : Ideal (𝓞 K)
hP₁ : P.IsPrime
hP₂ : P.LiesOver 𝒑
hK : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ p
⊢ (span {hζ.toInteger - 1}).IsPrime

Tactic:
← pow_one p

Goal state after:
n m p k : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
P : Ideal (𝓞 K)
hP₁ : P.IsPrime
hP₂ : P.LiesOver 𝒑
hK : IsCyclotomicExtension {p ^ 1} ℚ K
ζ : K
hζ✝ : IsPrimitiveRoot ζ p
hζ : IsPrimitiveRoot ζ (p ^ 1)
⊢ (span {hζ✝.toInteger - 1}).IsPrime
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
hK : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ p
h : 2 < p
⊢ ¬hζ.toInteger - 1 ∣ 2

Tactic:
← pow_one p

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
hK : IsCyclotomicExtension {p ^ 1} ℚ K
ζ : K
hζ✝ : IsPrimitiveRoot ζ p
hζ : IsPrimitiveRoot ζ (p ^ 1)
h : 2 < p
⊢ ¬hζ✝.toInteger - 1 ∣ 2
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
hK : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ p
x : 𝓞 K
hx : ¬hζ.toInteger - 1 ∣ x
⊢ 0 < p - 1

Tactic:
by grind [hp.out.one_lt]

Goal state after:
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
hK : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ p
⊢ (span {hζ.toInteger - 1}).inertiaDeg ℤ = 1

Tactic:
← pow_one p

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
hK : IsCyclotomicExtension {p ^ 1} ℚ K
ζ : K
hζ✝ : IsPrimitiveRoot ζ p
hζ : IsPrimitiveRoot ζ (p ^ 1)
⊢ (span {hζ✝.toInteger - 1}).inertiaDeg ℤ = 1
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : realSpace K
⊢ x ∈ compactSet K ↔ x ∈ ↑expMapBasis '' closure (paramSet K) ∪ {0}

Tactic:
by_cases hx₀ : x = 0

Goal state after:
case pos
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : realSpace K
hx₀ : x = 0
⊢ x ∈ compactSet K ↔ x ∈ ↑expMapBasis '' closure (paramSet K) ∪ {0}

case neg
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : realSpace K
hx₀ : ¬x = 0
⊢ x ∈ compactSet K ↔ x ∈ ↑expMapBasis '' closure (paramSet K) ∪ {0}
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
hK : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ p
⊢ (span {hζ.toInteger - 1}).ramificationIdx ℤ = p - 1

Tactic:
← pow_one p

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
hK : IsCyclotomicExtension {p ^ 1} ℚ K
ζ : K
hζ✝ : IsPrimitiveRoot ζ p
hζ : IsPrimitiveRoot ζ (p ^ 1)
⊢ (span {hζ✝.toInteger - 1}).ramificationIdx ℤ = p - 1
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
hK : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ p
n : ℤ
⊢ hζ.toInteger - 1 ∣ ↑n ↔ ↑p ∣ n

Tactic:
← pow_one p

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
hK : IsCyclotomicExtension {p ^ 1} ℚ K
ζ : K
hζ✝ : IsPrimitiveRoot ζ p
hζ : IsPrimitiveRoot ζ (p ^ 1)
n : ℤ
⊢ hζ✝.toInteger - 1 ∣ ↑n ↔ ↑p ∣ n
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
hK : IsCyclotomicExtension {p} ℚ K
⊢ (𝒑.primesOver (𝓞 K)).ncard = 1

Tactic:
← pow_one p

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
hK : IsCyclotomicExtension {p ^ 1} ℚ K
⊢ (𝒑.primesOver (𝓞 K)).ncard = 1
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
hK : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ p
P : Ideal (𝓞 K)
hP₁ : P.IsPrime
hP₂ : P.LiesOver 𝒑
⊢ P = span {hζ.toInteger - 1}

Tactic:
← pow_one p

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
hK : IsCyclotomicExtension {p ^ 1} ℚ K
ζ : K
hζ✝ : IsPrimitiveRoot ζ p
hζ : IsPrimitiveRoot ζ (p ^ 1)
P : Ideal (𝓞 K)
hP₁ : P.IsPrime
hP₂ : P.LiesOver 𝒑
⊢ P = span {hζ✝.toInteger - 1}
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
hK : IsCyclotomicExtension {p} ℚ K
⊢ 𝒑.inertiaDegIn (𝓞 K) = 1

Tactic:
← pow_one p

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
hK : IsCyclotomicExtension {p ^ 1} ℚ K
⊢ 𝒑.inertiaDegIn (𝓞 K) = 1
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
hK : IsCyclotomicExtension {p} ℚ K
⊢ 𝒑.ramificationIdxIn (𝓞 K) = p - 1

Tactic:
← pow_one p

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
hK : IsCyclotomicExtension {p ^ 1} ℚ K
⊢ 𝒑.ramificationIdxIn (𝓞 K) = p - 1
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ volume (normLeOne K) = 2 ^ nrRealPlaces K * ↑NNReal.pi ^ nrComplexPlaces K * ENNReal.ofReal (regulator K)

Tactic:
by
  rw [volume_eq_two_pow_mul_two_pi_pow_mul_integral (normLeOne_eq_preimage_image K).symm
    (measurableSet_normLeOne K), normLeOne_eq_preimage,
    normAtAllPlaces_image_preimage_expMapBasis,
    setLIntegral_expMapBasis_image (measurableSet_paramSet K) (by fun_prop)]
  simp_rw [ENNReal.inv_mul_cancel_right
    (Finset.prod_ne_zero_iff.mpr fun _ _ ↦ ofReal_ne_zero_iff.mpr (expMapBasis_pos _ _))
    (prod_ne_top fun _ _ ↦ ofReal_ne_top)]
  rw [setLIntegral_paramSet_exp K Module.finrank_pos, ofReal_mul zero_le_two, mul_pow,
    ofReal_ofNat, ENNReal.mul_inv_cancel_right (Nat.cast_ne_zero.mpr Module.finrank_pos.ne')
    (natCast_ne_top _), coe_nnreal_eq, NNReal.coe_real_pi, mul_mul_mul_comm, ← ENNReal.inv_pow,
    ← mul_assoc, ← mul_assoc, ENNReal.inv_mul_cancel_right (pow_ne_zero _ two_ne_zero)
    (pow_ne_top ENNReal.ofNat_ne_top)]

Goal state after:
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal

Goal state before:
pp: m p : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst✝² : Field K
inst✝¹ : NumberField K
inst✝ : NeZero m
hK : IsCyclotomicExtension {m} ℚ K
hm : ¬p ∣ m
⊢ 𝒑.ramificationIdxIn (𝓞 K) = 1

Tactic:
have : IsGalois ℚ K := isGalois {m} ℚ K
  obtain ⟨⟨P, _, _⟩⟩ := 𝒑.nonempty_primesOver (S := 𝓞 K)
  rw [ramificationIdxIn_eq_ramificationIdx 𝒑 P Gal(K/ℚ), ramificationIdx_eq_of_not_dvd p K P hm]

Goal state after:
Module: Mathlib.NumberTheory.NumberField.DirichletDensity

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
S : Set (HeightOneSpectrum (𝓞 K))
s : ℝ
hs : 0 ≤ s
hS : Finite ↑S
⊢ ∑' (𝔭 : ↑S), 1 ≤ ↑S.ncard

pp: case hf
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
S : Set (HeightOneSpectrum (𝓞 K))
s : ℝ
hs : 0 ≤ s
hS : Finite ↑S
⊢ Summable fun 𝔭 ↦ ↑(Ideal.absNorm (↑𝔭).asIdeal) ^ (-s)

pp: case hg
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
S : Set (HeightOneSpectrum (𝓞 K))
s : ℝ
hs : 0 ≤ s
hS : Finite ↑S
⊢ Summable fun 𝔭 ↦ 1

pp: case hx
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
S : Set (HeightOneSpectrum (𝓞 K))
s : ℝ
hs : 0 ≤ s
hS : Finite ↑S
𝔭 : ↑S
⊢ 1 ≤ ↑(Ideal.absNorm (↑𝔭).asIdeal)

pp: case hz
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
S : Set (HeightOneSpectrum (𝓞 K))
s : ℝ
hs : 0 ≤ s
hS : Finite ↑S
𝔭 : ↑S
⊢ -s ≤ 0

Tactic:
<;>

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
S : Set (HeightOneSpectrum (𝓞 K))
s : ℝ
hs : 0 ≤ s
hS : Finite ↑S
⊢ ∑' (𝔭 : ↑S), 1 ≤ ↑S.ncard

case hf
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
S : Set (HeightOneSpectrum (𝓞 K))
s : ℝ
hs : 0 ≤ s
hS : Finite ↑S
⊢ Summable fun 𝔭 ↦ ↑(Ideal.absNorm (↑𝔭).asIdeal) ^ (-s)

case hg
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
S : Set (HeightOneSpectrum (𝓞 K))
s : ℝ
hs : 0 ≤ s
hS : Finite ↑S
⊢ Summable fun 𝔭 ↦ 1

case hx
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
S : Set (HeightOneSpectrum (𝓞 K))
s : ℝ
hs : 0 ≤ s
hS : Finite ↑S
𝔭 : ↑S
⊢ 1 ≤ ↑(Ideal.absNorm (↑𝔭).asIdeal)

case hz
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
S : Set (HeightOneSpectrum (𝓞 K))
s : ℝ
hs : 0 ≤ s
hS : Finite ↑S
𝔭 : ↑S
⊢ -s ≤ 0
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Galois

Goal state before:
pp: case refine_2
n : ℕ
inst✝⁴ : NeZero n
K : Type u_1
inst✝³ : Field K
inst✝² : NumberField K
hK : IsCyclotomicExtension {n} ℚ K
p : ℕ
hp : Fact (Nat.Prime p)
P : Ideal (𝓞 K)
inst✝¹ : P.IsMaximal
inst✝ : P.LiesOver (span {↑p})
hn✝ : p.Coprime n
this : IsGalois ℚ K
hn : ¬p ∣ n
⊢ orderOf ((Units.coeHom (ZMod n)) (ZMod.unitOfCoprime p hn✝)) ≤ (span {↑p}).inertiaDegIn (𝓞 K)

Tactic:
Units.coeHom_apply,

Goal state after:
case refine_2
n : ℕ
inst✝⁴ : NeZero n
K : Type u_1
inst✝³ : Field K
inst✝² : NumberField K
hK : IsCyclotomicExtension {n} ℚ K
p : ℕ
hp : Fact (Nat.Prime p)
P : Ideal (𝓞 K)
inst✝¹ : P.IsMaximal
inst✝ : P.LiesOver (span {↑p})
hn✝ : p.Coprime n
this : IsGalois ℚ K
hn : ¬p ∣ n
⊢ orderOf ↑(ZMod.unitOfCoprime p hn✝) ≤ (span {↑p}).inertiaDegIn (𝓞 K)
Module: Mathlib.NumberTheory.Ostrowski

Goal state before:
pp: case «0»
f : AbsoluteValue ℚ ℝ
p : ℕ
hp0 : 0 < f ↑0
hp1 : f ↑0 < 1
hmin : ∀ (m : ℕ), 0 < f ↑m ∧ f ↑m < 1 → 0 ≤ m
hp : 0 < 2
⊢ False

pp: case «1»
f : AbsoluteValue ℚ ℝ
p : ℕ
hp0 : 0 < f ↑1
hp1 : f ↑1 < 1
hmin : ∀ (m : ℕ), 0 < f ↑m ∧ f ↑m < 1 → 1 ≤ m
hp : 1 < 2
⊢ False

Tactic:
<;>

Goal state after:
case «0»
f : AbsoluteValue ℚ ℝ
p : ℕ
hp0 : 0 < f ↑0
hp1 : f ↑0 < 1
hmin : ∀ (m : ℕ), 0 < f ↑m ∧ f ↑m < 1 → 0 ≤ m
hp : 0 < 2
⊢ False

case «1»
f : AbsoluteValue ℚ ℝ
p : ℕ
hp0 : 0 < f ↑1
hp1 : f ↑1 < 1
hmin : ∀ (m : ℕ), 0 < f ↑m ∧ f ↑m < 1 → 1 ≤ m
hp : 1 < 2
⊢ False
Module: Mathlib.NumberTheory.NumberField.Ideal.Asymptotics

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
s : ℝ
hs : 0 ≤ s
this : Fintype { I // ↑(absNorm ↑I) ≤ s }
e : (C : ClassGroup (𝓞 K)) → { x // ClassGroup.mk0 ↑x = C } ≃ { x // ↑(absNorm ↑x) ≤ s ∧ ClassGroup.mk0 x = C } :=
  fun C ↦ Equiv.subtypeSubtypeEquivSubtypeInter (fun I ↦ ↑(absNorm ↑I) ≤ s) fun I ↦ ClassGroup.mk0 I = C
⊢ ∑ x, ↑{x_1 | ClassGroup.mk0 ↑x_1 = x}.card / s = ↑(Fintype.card { I // ↑(absNorm ↑I) ≤ s }) / s

Tactic:
rw [Fintype.card, Finset.card_eq_sum_card_fiberwise (f := fun I ↦ ClassGroup.mk0 I.1)
      (t := Finset.univ) (fun _ _ ↦ Finset.mem_univ _), Nat.cast_sum, Finset.sum_div]

Goal state after:
Module: Mathlib.NumberTheory.Ostrowski

Goal state before:
pp: case hbc
f : AbsoluteValue ℚ ℝ
bdd : ∀ (n : ℕ), f ↑n ≤ 1
p : ℕ
hp0 : 0 < f ↑p
hp1 : f ↑p < 1
hmin : ∀ (m : ℕ), 0 < f ↑m ∧ f ↑m < 1 → p ≤ m
m : ℕ
hpm : ¬p ∣ m
hm : f ↑m < 1
M : ℝ := ⋯
hM : M = max (f ↑p) (f ↑m)
k : ℕ := ⋯
hk : k = ⌈logb M (1 / 2)⌉₊ + 1
a b : ℤ
bezout : a * ↑p ^ k + b * ↑m ^ k = 1
le_half : ∀ {x : ℝ}, 0 < x → x < 1 → x ≤ M → x ^ k < 1 / 2
⊢ f ↑a ≤ 1

pp: case hbc
f : AbsoluteValue ℚ ℝ
bdd : ∀ (n : ℕ), f ↑n ≤ 1
p : ℕ
hp0 : 0 < f ↑p
hp1 : f ↑p < 1
hmin : ∀ (m : ℕ), 0 < f ↑m ∧ f ↑m < 1 → p ≤ m
m : ℕ
hpm : ¬p ∣ m
hm : f ↑m < 1
M : ℝ := ⋯
hM : M = max (f ↑p) (f ↑m)
k : ℕ := ⋯
hk : k = ⌈logb M (1 / 2)⌉₊ + 1
a b : ℤ
bezout : a * ↑p ^ k + b * ↑m ^ k = 1
le_half : ∀ {x : ℝ}, 0 < x → x < 1 → x ≤ M → x ^ k < 1 / 2
⊢ f ↑b ≤ 1

Tactic:
<;>

Goal state after:
case hbc
f : AbsoluteValue ℚ ℝ
bdd : ∀ (n : ℕ), f ↑n ≤ 1
p : ℕ
hp0 : 0 < f ↑p
hp1 : f ↑p < 1
hmin : ∀ (m : ℕ), 0 < f ↑m ∧ f ↑m < 1 → p ≤ m
m : ℕ
hpm : ¬p ∣ m
hm : f ↑m < 1
M : ℝ := ⋯
hM : M = max (f ↑p) (f ↑m)
k : ℕ := ⋯
hk : k = ⌈logb M (1 / 2)⌉₊ + 1
a b : ℤ
bezout : a * ↑p ^ k + b * ↑m ^ k = 1
le_half : ∀ {x : ℝ}, 0 < x → x < 1 → x ≤ M → x ^ k < 1 / 2
⊢ f ↑a ≤ 1

case hbc
f : AbsoluteValue ℚ ℝ
bdd : ∀ (n : ℕ), f ↑n ≤ 1
p : ℕ
hp0 : 0 < f ↑p
hp1 : f ↑p < 1
hmin : ∀ (m : ℕ), 0 < f ↑m ∧ f ↑m < 1 → p ≤ m
m : ℕ
hpm : ¬p ∣ m
hm : f ↑m < 1
M : ℝ := ⋯
hM : M = max (f ↑p) (f ↑m)
k : ℕ := ⋯
hk : k = ⌈logb M (1 / 2)⌉₊ + 1
a b : ℤ
bezout : a * ↑p ^ k + b * ↑m ^ k = 1
le_half : ∀ {x : ℝ}, 0 < x → x < 1 → x ≤ M → x ^ k < 1 / 2
⊢ f ↑b ≤ 1
Module: Mathlib.Topology.MetricSpace.Ultra.ContinuousMaps

Goal state before:
pp: case refine_1
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : CompactSpace X
inst✝¹ : MetricSpace Y
inst✝ : IsUltrametricDist Y
f g h : C(X, Y)
x : X
⊢ dist (f x) (g x) ≤ dist f g

pp: case refine_2
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : CompactSpace X
inst✝¹ : MetricSpace Y
inst✝ : IsUltrametricDist Y
f g h : C(X, Y)
x : X
⊢ dist (g x) (h x) ≤ dist g h

Tactic:
<;>

Goal state after:
case refine_1
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : CompactSpace X
inst✝¹ : MetricSpace Y
inst✝ : IsUltrametricDist Y
f g h : C(X, Y)
x : X
⊢ dist (f x) (g x) ≤ dist f g

case refine_2
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : CompactSpace X
inst✝¹ : MetricSpace Y
inst✝ : IsUltrametricDist Y
f g h : C(X, Y)
x : X
⊢ dist (g x) (h x) ≤ dist g h
Module: Mathlib.NumberTheory.NumberField.House

Goal state before:
pp: case calc_3
K : Type u_1
inst✝⁴ : Field K
inst✝³ : NumberField K
α : Type u_2
β : Type u_3
a : Matrix α β (𝓞 K)
p q : ℕ
hpq : p < q
x : β × (K →+* ℂ) → ℤ
inst✝² : Fintype β
A : ℝ
habs : ∀ (k : α) (l : β), house ((algebraMap (𝓞 K) K) (a k l)) ≤ A
inst✝¹ : DecidableEq (K →+* ℂ)
inst✝ : Fintype α
Apos : 0 ≤ A
hxbound : ‖x‖ ≤ (↑q * ↑(finrank ℚ K) * ‖asiegel K a‖) ^ (↑p / (↑q - ↑p))
h : ℕ := finrank ℚ K
l : β
H₀ : 0 ≤ supOfBasis K
H₁ : 0 < ↑q - ↑p
⊢ ∑ r, ‖x (l, r)‖ * house ((algebraMap (𝓞 K) K) ((newBasis K) r)) ≤ ∑ r, ‖x (l, r)‖ * supOfBasis K

Tactic:
unfold supOfBasis

Goal state after:
case calc_3
K : Type u_1
inst✝⁴ : Field K
inst✝³ : NumberField K
α : Type u_2
β : Type u_3
a : Matrix α β (𝓞 K)
p q : ℕ
hpq : p < q
x : β × (K →+* ℂ) → ℤ
inst✝² : Fintype β
A : ℝ
habs : ∀ (k : α) (l : β), house ((algebraMap (𝓞 K) K) (a k l)) ≤ A
inst✝¹ : DecidableEq (K →+* ℂ)
inst✝ : Fintype α
Apos : 0 ≤ A
hxbound : ‖x‖ ≤ (↑q * ↑(finrank ℚ K) * ‖asiegel K a‖) ^ (↑p / (↑q - ↑p))
h : ℕ := finrank ℚ K
l : β
H₀ : 0 ≤ supOfBasis K
H₁ : 0 < ↑q - ↑p
⊢ ∑ r, ‖x (l, r)‖ * house ((algebraMap (𝓞 K) K) ((newBasis K) r)) ≤
    ∑ r, ‖x (l, r)‖ * univ.sup' ⋯ fun r ↦ house ((algebraMap (𝓞 K) K) ((newBasis K) r))
Module: Mathlib.NumberTheory.Ostrowski

Goal state before:
pp: case inl
f : AbsoluteValue ℚ ℝ
notbdd : ¬∀ (n : ℕ), f ↑n ≤ 1
hfm1 : 1 < f ↑0
hm : 0 ≤ 1
⊢ f ↑0 ≤ 1

pp: case inr
f : AbsoluteValue ℚ ℝ
notbdd : ¬∀ (n : ℕ), f ↑n ≤ 1
hfm1 : 1 < f ↑1
hm : 1 ≤ 1
⊢ f ↑1 ≤ 1

Tactic:
<;>

Goal state after:
case inl
f : AbsoluteValue ℚ ℝ
notbdd : ¬∀ (n : ℕ), f ↑n ≤ 1
hfm1 : 1 < f ↑0
hm : 0 ≤ 1
⊢ f ↑0 ≤ 1

case inr
f : AbsoluteValue ℚ ℝ
notbdd : ¬∀ (n : ℕ), f ↑n ≤ 1
hfm1 : 1 < f ↑1
hm : 1 ≤ 1
⊢ f ↑1 ≤ 1
Module: Mathlib.Topology.Separation.DisjointCover

Goal state before:
pp: ι : Type u_1
X : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TotallyDisconnectedSpace X
inst✝¹ : T2Space X
inst✝ : CompactSpace X
U : ι → Opens X
hU : IsOpenCover U
r : X → ι
hr : ∀ (a : X), a ∈ U (r a)
V : X → Set X
hV : ∀ (x : X), IsClopen (V x)
hVx : ∀ (x : X), x ∈ V x
hVU : ∀ (x : X), V x ⊆ ↑(U (r x))
⊢ ∃ n V, (∀ (j : Fin n), ∃ i, ↑(V j) ⊆ ↑(U i)) ∧ univ ⊆ ⋃ j, ↑(V j)

Tactic:
obtain ⟨t, ht⟩ : ∃ t, univ ⊆ ⋃ i ∈ t, V i :=
    isCompact_univ.elim_finite_subcover V (fun x ↦ (hV x).2) (fun x _ ↦ mem_iUnion.mpr ⟨x, hVx x⟩)

Goal state after:
ι : Type u_1
X : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TotallyDisconnectedSpace X
inst✝¹ : T2Space X
inst✝ : CompactSpace X
U : ι → Opens X
hU : IsOpenCover U
r : X → ι
hr : ∀ (a : X), a ∈ U (r a)
V : X → Set X
hV : ∀ (x : X), IsClopen (V x)
hVx : ∀ (x : X), x ∈ V x
hVU : ∀ (x : X), V x ⊆ ↑(U (r x))
t : Finset X
ht : univ ⊆ ⋃ i ∈ t, V i
⊢ ∃ n V, (∀ (j : Fin n), ∃ i, ↑(V j) ⊆ ↑(U i)) ∧ univ ⊆ ⋃ j, ↑(V j)
Module: Mathlib.Topology.UniformSpace.ProdApproximation

Goal state before:
pp: X : Type u_5
Y : Type u_6
R : Type u_7
inst✝⁴ : TopologicalSpace X
inst✝³ : TopologicalSpace Y
inst✝² : CommRing R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalRing R
f : C(X, R)
g : C(Y, R)
⊢ tensorHom (f ⊗ₜ[R] g) = (prodMul f) g

Tactic:
tensorHom,

Goal state after:
X : Type u_5
Y : Type u_6
R : Type u_7
inst✝⁴ : TopologicalSpace X
inst✝³ : TopologicalSpace Y
inst✝² : CommRing R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalRing R
f : C(X, R)
g : C(Y, R)
⊢ (TensorProduct.lift prodMul) (f ⊗ₜ[R] g) = (prodMul f) g
Module: Mathlib.Topology.UniformSpace.ProdApproximation

Goal state before:
pp: X : Type u_5
Y : Type u_6
R : Type u_7
inst✝⁸ : TopologicalSpace X
inst✝⁷ : TopologicalSpace Y
inst✝⁶ : CommRing R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : IsTopologicalRing R
inst✝³ : CompactSpace X
inst✝² : T2Space X
inst✝¹ : CompactSpace Y
inst✝ : TotallyDisconnectedSpace X
⊢ DenseRange ⇑tensorHom

Tactic:
let : UniformSpace R := IsTopologicalAddGroup.rightUniformSpace R
  let : IsUniformAddGroup R := isUniformAddGroup_of_addCommGroup
  intro f
  simp_rw [mem_closure_iff, Set.nonempty_def]
  intro U hUo hUf
  have := mem_nhds_uniformity_iff_right.mp (hUo.mem_nhds hUf)
  obtain ⟨J, hJu, hJ'⟩ := (hasBasis_compactConvergenceUniformity_of_compact).mem_iff.mp this
  obtain ⟨n, g, h, hgh⟩ := exists_finite_sum_mul_approximation_of_mem_uniformity f hJu
  have hG := Set.mem_of_subset_of_mem hJ' (a := (f, tensorHom <| ∑ i, g i ⊗ₜ h i))
  simp only [Prod.forall, Set.mem_ofPred_eq, forall_const] at hG
  simpa using ⟨_, hG <| by simpa [tensorHom] using hgh⟩

Goal state after:
Module: Mathlib.NumberTheory.Pell

Goal state before:
pp: case refine_1
d : ℤ
h₀ : 0 < d
a : Solution₁ d
hy : 0 ≤ a.y
hx : a.x < 0
⊢ 0 < (-a⁻¹).x

pp: case refine_2
d : ℤ
h₀ : 0 < d
a : Solution₁ d
hy : 0 ≤ a.y
hx : a.x < 0
⊢ 0 ≤ (-a⁻¹).y

pp: case refine_3
d : ℤ
h₀ : 0 < d
a : Solution₁ d
hy : 0 ≤ a.y
hx : a.x < 0
⊢ a ∈ {-a⁻¹, (-a⁻¹)⁻¹, - -a⁻¹, -(-a⁻¹)⁻¹}

pp: case refine_4
d : ℤ
h₀ : 0 < d
a : Solution₁ d
hy : a.y ≤ 0
hx : a.x < 0
⊢ 0 < (-a).x

pp: case refine_5
d : ℤ
h₀ : 0 < d
a : Solution₁ d
hy : a.y ≤ 0
hx : a.x < 0
⊢ 0 ≤ (-a).y

pp: case refine_6
d : ℤ
h₀ : 0 < d
a : Solution₁ d
hy : a.y ≤ 0
hx : a.x < 0
⊢ a ∈ {-a, (-a)⁻¹, - -a, -(-a)⁻¹}

pp: case refine_7
d : ℤ
h₀ : 0 < d
a : Solution₁ d
hy : 0 ≤ a.y
hx : 0 < a.x
⊢ a ∈ {a, a⁻¹, -a, -a⁻¹}

pp: case refine_8
d : ℤ
h₀ : 0 < d
a : Solution₁ d
hy : a.y ≤ 0
hx : 0 < a.x
⊢ 0 ≤ a⁻¹.y

pp: case refine_9
d : ℤ
h₀ : 0 < d
a : Solution₁ d
hy : a.y ≤ 0
hx : 0 < a.x
⊢ a ∈ {a⁻¹, a⁻¹⁻¹, -a⁻¹, -a⁻¹⁻¹}

Tactic:
<;>

Goal state after:
case refine_1
d : ℤ
h₀ : 0 < d
a : Solution₁ d
hy : 0 ≤ a.y
hx : a.x < 0
⊢ 0 < (-a⁻¹).x

case refine_2
d : ℤ
h₀ : 0 < d
a : Solution₁ d
hy : 0 ≤ a.y
hx : a.x < 0
⊢ 0 ≤ (-a⁻¹).y

case refine_3
d : ℤ
h₀ : 0 < d
a : Solution₁ d
hy : 0 ≤ a.y
hx : a.x < 0
⊢ a ∈ {-a⁻¹, (-a⁻¹)⁻¹, - -a⁻¹, -(-a⁻¹)⁻¹}

case refine_4
d : ℤ
h₀ : 0 < d
a : Solution₁ d
hy : a.y ≤ 0
hx : a.x < 0
⊢ 0 < (-a).x

case refine_5
d : ℤ
h₀ : 0 < d
a : Solution₁ d
hy : a.y ≤ 0
hx : a.x < 0
⊢ 0 ≤ (-a).y

case refine_6
d : ℤ
h₀ : 0 < d
a : Solution₁ d
hy : a.y ≤ 0
hx : a.x < 0
⊢ a ∈ {-a, (-a)⁻¹, - -a, -(-a)⁻¹}

case refine_7
d : ℤ
h₀ : 0 < d
a : Solution₁ d
hy : 0 ≤ a.y
hx : 0 < a.x
⊢ a ∈ {a, a⁻¹, -a, -a⁻¹}

case refine_8
d : ℤ
h₀ : 0 < d
a : Solution₁ d
hy : a.y ≤ 0
hx : 0 < a.x
⊢ 0 ≤ a⁻¹.y

case refine_9
d : ℤ
h₀ : 0 < d
a : Solution₁ d
hy : a.y ≤ 0
hx : 0 < a.x
⊢ a ∈ {a⁻¹, a⁻¹⁻¹, -a⁻¹, -a⁻¹⁻¹}