mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Factorization

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : Fintype K
p f n : ℕ
P : K[X]
hK : Fintype.card K = p ^ f
hn : p.Coprime n
hp : Fact (Nat.Prime p)
hPirr : Irreducible P
A : K[X]
hA : cyclotomic n K = P * A
⊢ P * (C P.leadingCoeff⁻¹ * C P.leadingCoeff) * A = P * C P.leadingCoeff⁻¹ * (A * C P.leadingCoeff)

Tactic:
ring

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

Goal state before:
pp: K : Type u_1
inst✝² : Field K
θ : 𝓞 K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : NumberField K
hp : ¬p ∣ exponent θ
Q : ℤ[X]
hQ : Polynomial.map (Int.castRingHom (ZMod p)) Q ∈ monicFactorsMod θ p
⊢ multiplicity (↑((primesOverSpanEquivMonicFactorsMod hp).symm ⟨Polynomial.map (Int.castRingHom (ZMod p)) Q, hQ⟩))
      (Ideal.map (algebraMap ℤ (𝓞 K)) (span {↑p})) =
    multiplicity (Polynomial.map (Int.castRingHom (ZMod p)) Q) (Polynomial.map (Int.castRingHom (ZMod p)) (minpoly ℤ θ))

Tactic:
· apply multiplicity_eq_of_emultiplicity_eq
    rw [← emultiplicity_map_eq (mapEquiv (Int.quotientSpanNatEquivZMod p).symm),
      emultiplicity_factors_map_eq_emultiplicity inferInstance (by simp [NeZero.ne p])
      (not_dvd_exponent_iff.mp hp).eq_top θ.isIntegral]
    · simp only [primesOverSpanEquivMonicFactorsMod_symm_apply,
        Equiv.apply_symm_apply (normalizedFactorsMapEquivNormalizedFactorsMinPolyMk _ _ _ _),
        Polynomial.map_map, Int.quotientSpanNatEquivZMod_comp_castRingHom, mapEquiv_apply]
    · rw [← mem_primesOver_iff_mem_normalizedFactors _ (by simp [NeZero.ne p])]
      exact ((primesOverSpanEquivMonicFactorsMod hp).symm ⟨_, hQ⟩).coe_prop

Goal state after:
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Factorization

Goal state before:
pp: K : Type u_1
inst✝² : Field K
inst✝¹ : Fintype K
p f n : ℕ
hK : Fintype.card K = p ^ f
hn : p.Coprime n
hp : Fact (Nat.Prime p)
inst✝ : DecidableEq K
h : Associated (normalizedFactors (cyclotomic n K)).prod (cyclotomic n K)
this : ∀ P ∈ normalizedFactors (cyclotomic n K), P.natDegree = orderOf (unitOfCoprime (p ^ f) ⋯)
H : (Multiset.map (fun x ↦ orderOf (unitOfCoprime (p ^ f) ⋯)) (normalizedFactors (cyclotomic n K))).sum = φ n
⊢ (normalizedFactors (cyclotomic n K)).toFinset.card = φ n / orderOf (unitOfCoprime (p ^ f) ⋯)

Tactic:
simp only [map_const', sum_replicate, smul_eq_mul] at H

Goal state after:
K : Type u_1
inst✝² : Field K
inst✝¹ : Fintype K
p f n : ℕ
hK : Fintype.card K = p ^ f
hn : p.Coprime n
hp : Fact (Nat.Prime p)
inst✝ : DecidableEq K
h : Associated (normalizedFactors (cyclotomic n K)).prod (cyclotomic n K)
this : ∀ P ∈ normalizedFactors (cyclotomic n K), P.natDegree = orderOf (unitOfCoprime (p ^ f) ⋯)
H : (normalizedFactors (cyclotomic n K)).card * orderOf (unitOfCoprime (p ^ f) ⋯) = φ n
⊢ (normalizedFactors (cyclotomic n K)).toFinset.card = φ n / orderOf (unitOfCoprime (p ^ f) ⋯)
Module: Mathlib.NumberTheory.NumberField.Ideal.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
I : Ideal (𝓞 K)
inst✝ : NumberField K
hI : absNorm I ≠ 1
n : ℕ
ζ : K
hn : 2 ≤ n
hζ : IsPrimitiveRoot ζ n
h : (Ideal.Quotient.mk I) hζ.toInteger = (Ideal.Quotient.mk I) 1
h₁ : (absNorm I).Coprime n
⊢ False

Tactic:
Ideal.Quotient.eq

Goal state after:
K : Type u_1
inst✝¹ : Field K
I : Ideal (𝓞 K)
inst✝ : NumberField K
hI : absNorm I ≠ 1
n : ℕ
ζ : K
hn : 2 ≤ n
hζ : IsPrimitiveRoot ζ n
h : hζ.toInteger - 1 ∈ I
h₁ : (absNorm I).Coprime n
⊢ False
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : realSpace K
⊢ Real.exp (x w₀) ^ finrank ℚ K * (∏ x_1, ↑expMapBasis x ↑x_1)⁻¹ * 2⁻¹ ^ nrComplexPlaces K *
      (↑(finrank ℚ K) * regulator K) =
    Real.exp (x w₀) ^ finrank ℚ K * (∏ x_1, ↑expMapBasis x ↑x_1)⁻¹ * 2⁻¹ ^ nrComplexPlaces K * ↑(finrank ℚ K) *
      regulator K

Tactic:
ring

Goal state after:
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne

Goal state before:
pp: case e_f
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
s : Set (realSpace K)
hs : MeasurableSet s
f : (InfinitePlace K → ℝ) → ℝ≥0∞
hf : Measurable f
this✝ : Measurable ↑expMapBasis
x : realSpace K
this : 0 ≤ (∏ w, ↑expMapBasis x ↑w)⁻¹
⊢ ENNReal.ofReal (Real.exp (x w₀ * ↑(finrank ℚ K))) * (∏ i, ENNReal.ofReal (↑expMapBasis x ↑i))⁻¹ *
            2⁻¹ ^ nrComplexPlaces K *
          ↑(finrank ℚ K) *
        ENNReal.ofReal (regulator K) *
      f (↑expMapBasis x) =
    2⁻¹ ^ nrComplexPlaces K * ENNReal.ofReal (regulator K) * ↑(finrank ℚ K) *
      (ENNReal.ofReal (Real.exp (x w₀ * ↑(finrank ℚ K))) * (∏ i, ENNReal.ofReal (↑expMapBasis (fun w ↦ x w) ↑i))⁻¹ *
        f (↑expMapBasis x))

Tactic:
ring

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

Goal state before:
pp: case pos.zero
p : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
ζ : K
h : p = 2
hK : IsCyclotomicExtension {2} ℚ K
hζ✝ : IsPrimitiveRoot ζ (p ^ (0 + 1))
hζ : IsPrimitiveRoot ζ 2
⊢ Associated (-2) ↑2

Tactic:
Int.ofNat_two,

Goal state after:
case pos.zero
p : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
ζ : K
h : p = 2
hK : IsCyclotomicExtension {2} ℚ K
hζ✝ : IsPrimitiveRoot ζ (p ^ (0 + 1))
hζ : IsPrimitiveRoot ζ 2
⊢ Associated (-2) 2
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal

Goal state before:
pp: case pos.succ
p : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
ζ : K
h : p = 2
n : ℕ
hK : IsCyclotomicExtension {2 ^ (n + (1 + 1))} ℚ K
hζ✝ : IsPrimitiveRoot ζ (p ^ (n + 1 + 1))
hζ : IsPrimitiveRoot ζ (2 ^ (n + (1 + 1)))
⊢ Associated ((Algebra.norm ℤ) (hζ✝.toInteger - 1)) ↑p

Tactic:
one_add_one_eq_two

Goal state after:
case pos.succ
p : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
ζ : K
h : p = 2
n : ℕ
hK : IsCyclotomicExtension {2 ^ (n + 2)} ℚ K
hζ✝ : IsPrimitiveRoot ζ (p ^ (n + 1 + 1))
hζ : IsPrimitiveRoot ζ (2 ^ (n + 2))
⊢ Associated ((Algebra.norm ℤ) (hζ✝.toInteger - 1)) ↑p
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne

Goal state before:
pp: case refine_1
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
c : ℝ
hc : c ∈ Set.Icc 0 1
y : realSpace K
hy : y ∈ Set.univ.pi fun w ↦ if w = w₀ then {0} else Set.Icc 0 1
hx₀ : (fun x1 x2 ↦ x1 • x2) c (↑expMapBasis y) ≠ 0
⊢ (fun w ↦ if w = w₀ then Real.log c else y w) ∈ closure (paramSet K)

pp: case refine_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
c : ℝ
hc : c ∈ Set.Icc 0 1
y : realSpace K
hy : y ∈ Set.univ.pi fun w ↦ if w = w₀ then {0} else Set.Icc 0 1
hx₀ : (fun x1 x2 ↦ x1 • x2) c (↑expMapBasis y) ≠ 0
⊢ (↑expMapBasis fun w ↦ if w = w₀ then Real.log c else y w) = (fun x1 x2 ↦ x1 • x2) c (↑expMapBasis y)

Tactic:
· rw [closure_paramSet, Set.mem_univ_pi]
    intro w
    split_ifs with h
    · refine Real.log_nonpos hc.1 hc.2
    · simpa [h] using hy w (Set.mem_univ _)

Goal state after:
case refine_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
c : ℝ
hc : c ∈ Set.Icc 0 1
y : realSpace K
hy : y ∈ Set.univ.pi fun w ↦ if w = w₀ then {0} else Set.Icc 0 1
hx₀ : (fun x1 x2 ↦ x1 • x2) c (↑expMapBasis y) ≠ 0
⊢ (↑expMapBasis fun w ↦ if w = w₀ then Real.log c else y w) = (fun x1 x2 ↦ x1 • x2) c (↑expMapBasis y)
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:
rw [← pow_one p] at hK hζ
  exact isPrime_span_zeta_sub_one p 0 hζ

Goal state after:
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ closure (normLeOne K) ⊆ normAtAllPlaces ⁻¹' compactSet K

Tactic:
by
  rw [normLeOne_eq_preimage]
  refine ((continuous_normAtAllPlaces K).closure_preimage_subset _).trans (Set.preimage_mono ?_)
  refine (isCompact_compactSet K).isClosed.closure_subset_iff.mpr ?_
  exact (Set.image_mono subset_closure).trans (expMapBasis_closure_subset_compactSet _)

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
P : Ideal (𝓞 K)
hP₁ : P.IsPrime
hP₂ : P.LiesOver 𝒑
⊢ P = span {hζ.toInteger - 1}

Tactic:
by
  rw [← pow_one p] at hK hζ
  exact eq_span_zeta_sub_one_of_liesOver p 0 K hζ P

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

Goal state before:
pp: K : Type u_1
inst✝² : Field K
inst✝¹ : NumberField K
inst✝ : DecidableEq (K →+* ℂ)
α : 𝓞 K
i : K →+* ℂ
σ : K →+* (K →+* ℂ) → ℂ := canonicalEmbedding K
⊢ ‖↑((((integralBasis K).reindex (equivReindex K).symm).repr ↑α) i)‖ ≤ c K * house ((algebraMap (𝓞 K) K) α)

Tactic:
calc
    _ ≤ ∑ j, ‖(basisMatrix K)ᵀ⁻¹ i j‖ * ‖σ (algebraMap (𝓞 K) K α) j‖ := by
      rw [← inverse_basisMatrix_mulVec_eq_repr]
      exact norm_sum_le_of_le _ fun _ _ ↦ (norm_mul _ _).le
    _ ≤ ∑ j, ‖((basisMatrix K).transpose)⁻¹‖ * ‖σ (algebraMap (𝓞 K) K α) j‖ := by
      gcongr
      exact norm_entry_le_entrywise_sup_norm ((basisMatrix K).transpose)⁻¹
    _ ≤ ∑ _ : K →+* ℂ, ‖fun i j => ((basisMatrix K).transpose)⁻¹ i j‖
        * house (algebraMap (𝓞 K) K α) := by
      gcongr with j
      exact norm_le_pi_norm (σ ((algebraMap (𝓞 K) K) α)) j
    _ = ↑(finrank ℚ K) * ‖((basisMatrix K).transpose)⁻¹‖ * house (algebraMap (𝓞 K) K α) := by
      simp [Embeddings.card, mul_assoc]

Goal state after:
Module: Mathlib.NumberTheory.SiegelsLemma

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : Fintype α
inst✝² : Fintype β
A : Matrix α β ℤ
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
v : β → ℤ
hv : 0 ≤ v ∧ v ≤ B'
mulVec_def : A *ᵥ v = fun i ↦ ∑ j, A i j * v j
⊢ N ≤ A *ᵥ v ∧ A *ᵥ v ≤ P

Tactic:
mulVec_def

Goal state after:
α : Type u_1
β : Type u_2
inst✝³ : Fintype α
inst✝² : Fintype β
A : Matrix α β ℤ
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
v : β → ℤ
hv : 0 ≤ v ∧ v ≤ B'
mulVec_def : A *ᵥ v = fun i ↦ ∑ j, A i j * v j
⊢ (N ≤ fun i ↦ ∑ j, A i j * v j) ∧ (fun i ↦ ∑ j, A i j * v j) ≤ P
Module: Mathlib.NumberTheory.SiegelsLemma

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : Fintype β
A : Matrix α β ℤ
hA : A ≠ 0
h : ‖A‖ < 1
i : α
j : β
⊢ A i j = 0

Tactic:
norm_lt_iff Real.zero_lt_one

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : Fintype β
A : Matrix α β ℤ
hA : A ≠ 0
h : ∀ (i : α) (j : β), ‖A i j‖ < 1
i : α
j : β
⊢ A i j = 0
Module: Mathlib.NumberTheory.NumberField.Ideal.Asymptotics

Goal state before:
pp: case e'_5
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ 2 ^ nrRealPlaces K * (2 * π) ^ nrComplexPlaces K * regulator K * ↑(Fintype.card (ClassGroup (𝓞 K))) /
      (↑(torsionOrder K) * √|↑(discr K)|) =
    ↑(Fintype.card (ClassGroup (𝓞 K))) *
      (2 ^ nrRealPlaces K * (2 * π) ^ nrComplexPlaces K * regulator K / (↑(torsionOrder K) * √|↑(discr K)|))

Tactic:
ring

Goal state after:
Module: Mathlib.NumberTheory.SiegelsLemma

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : Fintype α
inst✝² : Fintype β
A : Matrix α β ℤ
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
hn : m < n
hm : 0 < m
i : α
x✝ : i ∈ univ
⊢ ↑n * max 1 ‖A‖ * ↑B = ↑n * (max 1 ‖A‖ * ↑B)

Tactic:
ring

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

Goal state before:
pp: case e_f.e_f.e_f
K : Type u_1
inst✝² : Field K
inst✝¹ : NumberField K
α : Type u_2
β : Type u_3
a : Matrix α β (𝓞 K)
x : β × (K →+* ℂ) → ℤ
hxl : x ≠ 0
inst✝ : Fintype β
hmulvec0 : asiegel K a *ᵥ x = 0
k : α
lin_0 : ∀ (u : K →+* ℂ), ∑ r, ∑ l, ↑(a' K a k l r u) * ↑(x (l, r)) = 0
this : 0 = ∑ y, ∑ x_1, (∑ l, ↑(a' K a k l y x_1) * ↑(x (l, y))) * (newBasis K) x_1
r✝¹ : K →+* ℂ
r✝ : β
r : K →+* ℂ
⊢ ↑(a' K a k r✝ r✝¹ r) * ↑(x (r✝, r✝¹)) * (newBasis K) r = ↑(x (r✝, r✝¹)) * (↑(a' K a k r✝ r✝¹ r) * (newBasis K) r)

Tactic:
ring

Goal state after:
Module: Mathlib.NumberTheory.Ostrowski

Goal state before:
pp: 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 : ℝ := max (f ↑p) (f ↑m)
hM : M = max (f ↑p) (f ↑m)
k : ℕ := ⌈logb M (1 / 2)⌉₊ + 1
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 * ↑p ^ k) + f (↑b * ↑m ^ k) ≤ 1 * f ↑p ^ k + 1 * f ↑m ^ k

Tactic:
by
    simp only [map_mul, map_pow]
    gcongr <;> simpa only [← apply_natAbs_eq] using bdd _

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

Goal state before:
pp: case e_f.e_f
K : Type u_1
inst✝² : Field K
inst✝¹ : NumberField K
α : Type u_2
β : Type u_3
a : Matrix α β (𝓞 K)
x : β × (K →+* ℂ) → ℤ
hxl : x ≠ 0
inst✝ : Fintype β
hmulvec0 : asiegel K a *ᵥ x = 0
k : α
lin_0 : ∀ (u : K →+* ℂ), ∑ r, ∑ l, ↑(a' K a k l r u) * ↑(x (l, r)) = 0
this✝ : 0 = ∑ u, (∑ r, ∑ l, ↑(a' K a k l r u) * ↑(x (l, r))) * (newBasis K) u
this : 0 = ∑ y, ∑ x_1, ↑(x (y, x_1)) * ∑ u, ↑(a' K a k y x_1 u) * (newBasis K) u
l✝ : β
l : K →+* ℂ
⊢ ↑(x (l✝, l)) * (a k l✝ * (newBasis K) l) = (fun j ↦ a k j) l✝ * (↑(x (l✝, l)) * (newBasis K) l)

Tactic:
ring

Goal state after:
Module: Mathlib.NumberTheory.Ostrowski

Goal state before:
pp: f : AbsoluteValue ℚ ℝ
m✝ n✝ : ℕ
hm✝ : 1 < m✝
hn✝ : 1 < n✝
notbdd : ¬∀ (n : ℕ), f ↑n ≤ 1
k : ℕ
hk : k ≠ 0
m n : ℕ
hm : 1 < m
hn : 1 < n
d : ℕ := Nat.log m n
hfm : 1 < f ↑m
⊢ ↑m * (f ↑m ^ (d + 1) / (f ↑m - 1)) = ↑m * f ↑m / (f ↑m - 1) * f ↑m ^ d

Tactic:
ring

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

Goal state before:
pp: 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))
⊢ ∀ (l : β), house ↑(ξ K x l) ≤ c₁ K * (c₁ K * ↑q * A) ^ (↑p / (↑q - ↑p))

Tactic:
by
  let h := finrank ℚ K
  intro l
  have H₀ : 0 ≤ NumberField.house.supOfBasis K := supOfBasis_nonneg _
  have H₁ : 0 < (q - p : ℝ) := sub_pos.mpr <| mod_cast hpq
  calc _ = house (algebraMap (𝓞 K) K (∑ r, (x (l, r)) * ((newBasis K) r))) := rfl
       _ ≤ ∑ r, house (((algebraMap (𝓞 K) K) (x (l, r))) *
        ((algebraMap (𝓞 K) K) ((newBasis K) r))) := ?_
       _ ≤ ∑ r, ‖x (l, r)‖ * house ((algebraMap (𝓞 K) K) ((newBasis K) r)) := ?_
       _ ≤ ∑ r, ‖x (l, r)‖ * (supOfBasis K) := ?_
       _ ≤ ∑ _r : K →+* ℂ, ((↑q * h * ‖asiegel K a‖) ^ ((p : ℝ) / (q - p))) * supOfBasis K := ?_
       _ ≤ h * (c₂ K) * ((q * c₁ K * A) ^ ((p : ℝ) / (q - p))) := ?_
       _ ≤ c₁ K * ((c₁ K * ↑q * A) ^ ((p : ℝ) / (q - p))) := ?_
  · simp_rw [← map_mul, map_sum]; apply house_sum_le_sum_house
  · gcongr with r _; convert! house_mul_le ..
    simp only [map_intCast, house_intCast, Int.cast_abs, Int.norm_eq_abs]
  · unfold supOfBasis
    gcongr with r _
    simp only [le_sup'_iff, mem_univ, true_and]; use r
  · gcongr with r _
    exact le_trans (norm_le_pi_norm x ⟨l, r⟩) hxbound
  · simp only [sum_const, card_univ, nsmul_eq_mul]
    rw [Embeddings.card, mul_comm _ (supOfBasis K), c₂, c₁, ← mul_assoc,
      ← mul_assoc (q : ℝ), mul_assoc (q * _ : ℝ)]
    gcongr
    · exact le_mul_of_one_le_left (supOfBasis_nonneg K) (le_max_left ..)
    · exact asiegel_remark K a habs Apos
  · rw [mul_comm (q : ℝ) (c₁ K)]; rfl

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
k : ℕ
⊢ ↑(↑k.factorial * ⟨↑(Polynomial.eval x (ascPochhammer ℤ_[p] k)) / ↑k.factorial, ⋯⟩) = ↑((ascPochhammer ℕ k).smeval x)

Tactic:
PadicInt.coe_mul,

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
k : ℕ
⊢ ↑↑k.factorial * ↑⟨↑(Polynomial.eval x (ascPochhammer ℤ_[p] k)) / ↑k.factorial, ⋯⟩ = ↑((ascPochhammer ℕ k).smeval x)
Module: Mathlib.NumberTheory.Padics.MahlerBasis

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : Module ℤ_[p] E
inst✝¹ : IsBoundedSMul ℤ_[p] E
inst✝ : IsUltrametricDist E
f : C(ℤ_[p], E)
ε : ℝ
hε : ε > 0
this✝ : Tendsto (fun s ↦ ‖f‖ / ↑p ^ s) atTop (𝓝 0)
s : ℕ
hs : ‖f‖ / ↑p ^ s < ε
hf : f ≠ 0
this : 0 < ‖f‖ / ↑p ^ s
δ : ℝ
hδpos : δ > 0
hδf : ∀ {x y : ℤ_[p]}, dist x y < δ → dist (f x) (f y) < ‖f‖ / ↑p ^ s
t : ℕ
ht : ↑p ^ (-↑t) < δ
x y : ℤ_[p]
hxy : ‖x - y‖ ≤ ↑p ^ (-↑t)
⊢ ‖f x - f y‖ ≤ ‖f‖ / ↑p ^ s

Tactic:
by simpa only [dist_eq_norm_sub] using (hδf (hxy.trans_lt ht)).le

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

Goal state before:
pp: X : Type u_1
V : Type u_2
inst✝⁴ : TopologicalSpace X
inst✝³ : TopologicalSpace V
inst✝² : TotallyDisconnectedSpace X
inst✝¹ : T2Space X
inst✝ : CompactSpace X
S : Set (V × V)
f : C(X, V)
hS : S ∈ 𝓝ˢ (diagonal V)
⊢ ∃ n g h, Continuous[inst✝⁴, _] g ∧ ∀ (x : X), (f x, h (g x)) ∈ S

Tactic:
obtain ⟨n, E, hEne, hES, hEuniv, hEdis⟩ :=
    exists_disjoint_nonempty_clopen_cover_of_mem_nhds_diagonal f hS
  have h_uniq (x) : ∃! i, x ∈ E i := by
    refine match mem_iUnion.mp (hEuniv <| mem_univ x) with
      | ⟨i, hi⟩ => ⟨i, hi, fun j hj ↦ hEdis.eq ?_⟩
    simpa [← Clopens.coe_disjoint, not_disjoint_iff] using! ⟨x, hj, hi⟩
  choose g hg hg' using h_uniq -- for each `x`, `g x` is the unique `i` such that `x ∈ E i`
  have h_ex (i) : ∃ x, x ∈ E i := by
    simpa [← SetLike.coe_set_eq, ← nonempty_iff_ne_empty] using! hEne i
  choose r hr using h_ex -- for each `i`, choose an `r i ∈ E i`
  refine ⟨n, g, f ∘ r, continuous_discrete_rng.mpr fun j ↦ ?_, fun x ↦ (hES _) _ (hg _) _ (hr _)⟩
  convert! (E j).isOpen
  exact Set.ext fun x ↦ ⟨fun hj ↦ hj ▸ hg x, fun hx ↦ (hg' _ _ hx).symm⟩

Goal state after:
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
this✝¹ : UniformSpace R := IsTopologicalAddGroup.rightUniformSpace R
this✝ : IsUniformAddGroup R := isUniformAddGroup_of_addCommGroup
f : C(X × Y, R)
U : Set C(X × Y, R)
hUo : IsOpen U
hUf : f ∈ U
this : {p | p.1 = f → p.2 ∈ U} ∈ 𝓤 C(X × Y, R)
J : Set (R × R)
hJu : J ∈ 𝓤 R
hJ' : {fg | ∀ (x : X × Y), (fg.1 x, fg.2 x) ∈ J} ⊆ {p | p.1 = f → p.2 ∈ U}
n : ℕ
g : Fin n → C(X, R)
h : Fin n → C(Y, R)
hgh : ∀ (x : X) (y : Y), (f (x, y), ∑ i, (g i) x * (h i) y) ∈ J
hG : (∀ (a : X) (b : Y), (f (a, b), (tensorHom (∑ i, g i ⊗ₜ[R] h i)) (a, b)) ∈ J) → tensorHom (∑ i, g i ⊗ₜ[R] h i) ∈ U
⊢ ∀ (a : X) (b : Y), (f (a, b), (tensorHom (∑ i, g i ⊗ₜ[R] h i)) (a, b)) ∈ J

Tactic:
simpa [tensorHom] using hgh

Goal state after:
Module: Mathlib.NumberTheory.Pell

Goal state before:
pp: d : ℤ
a : Solution₁ d
⊢ a.x ^ 2 = a.x ^ 2 - d * a.y ^ 2 + d * a.y ^ 2

Tactic:
ring

Goal state after:
Module: Mathlib.NumberTheory.Pell

Goal state before:
pp: d : ℤ
a : Solution₁ d
⊢ d * a.y ^ 2 = a.x ^ 2 - (a.x ^ 2 - d * a.y ^ 2)

Tactic:
ring

Goal state after:
Module: Mathlib.NumberTheory.Pell

Goal state before:
pp: d : ℤ
a : Solution₁ d
h : IsFundamental a
n : ℤ
hn : 0 ≤ n
⊢ (a ^ n).y * a.x - (a ^ n).y = (a ^ n).y * (a.x - 1)

Tactic:
ring

Goal state after:
Module: Mathlib.NumberTheory.Pell

Goal state before:
pp: d : ℤ
a : Solution₁ d
h : IsFundamental a
n : ℤ
hn : 0 ≤ n
⊢ 0 ≤ a.x - 1

Tactic:
rw [sub_nonneg]; exact h.1.le

Goal state after:
Module: Mathlib.NumberTheory.Pell

Goal state before:
pp: d : ℤ
a₁ : Solution₁ d
h : IsFundamental a₁
a : Solution₁ d
hax : 1 < a.x
hay : 0 < a.y
⊢ d * (a₁.y ^ 2 - a.y ^ 2) = 1 + d * a₁.y ^ 2 - (1 + d * a.y ^ 2)

Tactic:
ring

Goal state after:
Module: Mathlib.NumberTheory.Pell

Goal state before:
pp: d : ℤ
a₁ : Solution₁ d
h : IsFundamental a₁
a : Solution₁ d
hax : 1 < a.x
hay : 0 < a.y
⊢ a.x * (d * (a.y * a₁.y)) = d * a.y * (a.x * a₁.y)

Tactic:
ring

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

Goal state before:
pp: case calc_3
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
i k : Fin n
x✝ : k ∈ Finset.univ
⊢ B i k • 0 = 0

Tactic:
smul_zero

Goal state after:
case calc_3
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
i k : Fin n
x✝ : k ∈ Finset.univ
⊢ 0 = 0
Module: Mathlib.NumberTheory.Pell

Goal state before:
pp: d : ℤ
a₁ : Solution₁ d
h : IsFundamental a₁
a : Solution₁ d
hax : 1 < a.x
hay : 0 < a.y
⊢ d * a.y * (a.y * a₁.x) = d * a.y ^ 2 * a₁.x

Tactic:
ring

Goal state after:
Module: Mathlib.NumberTheory.Pell

Goal state before:
pp: d : ℤ
a₁ : Solution₁ d
h : IsFundamental a₁
a : Solution₁ d
hax : 1 < a.x
hay : 0 < a.y
⊢ a₁.y * (a.x * a₁.x) = a.x * a₁.y * a₁.x

Tactic:
ring

Goal state after:
Module: Mathlib.NumberTheory.Pell

Goal state before:
pp: case e'_3
d : ℤ
a₁ : Solution₁ d
h : IsFundamental a₁
a : Solution₁ d
hax : 1 < a.x
hay : 0 < a.y
this : a.y - a.x * a₁.y < 0
⊢ a.y * (1 + d * a₁.y ^ 2) - a₁.y * (d * (a.y * a₁.y) + a.x) = a.y - a.x * a₁.y

Tactic:
ring

Goal state after: