mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
⊢ mixedSpaceOfRealSpace (normAtAllPlaces x) ∈ fundamentalCone K ↔ x ∈ fundamentalCone K

Tactic:
fundamentalCone,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
⊢ mixedSpaceOfRealSpace (normAtAllPlaces x) ∈
      logMap ⁻¹' ZSpan.fundamentalDomain (Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K)) \
        {x | mixedEmbedding.norm x = 0} ↔
    x ∈
      logMap ⁻¹' ZSpan.fundamentalDomain (Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K)) \
        {x | mixedEmbedding.norm x = 0}
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
J : ↥(Ideal (𝓞 K))⁰
a : { a // ↑(preimageOfMemIntegerSet a) ∈ ↑↑J }
⊢ ↑((idealSetEquiv K J).symm a) = ↑↑a

Tactic:
rw [← (idealSetEquiv_apply ((idealSetEquiv K J).symm a)), Equiv.apply_symm_apply]

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

Goal state before:
pp: K : Type u_1
inst✝³ : Field K
inst✝² : CharZero K
inst✝¹ : IsCMField K
inst✝ : NumberField K
W₀ : InfinitePlace K := (equivInfinitePlace K).symm w₀
f : { w // w ≠ W₀ } ≃ { w // w ≠ w₀ } := (equivInfinitePlace K).subtypeEquiv ⋯
g : Fin (rank K) ≃ { w // w ≠ W₀ } := ((finCongr ⋯).trans (equivFinRank ↥K⁺)).trans f.symm
⊢ regOfFamily (realFundSystem K) = 2 ^ rank K * regulator ↥K⁺

Tactic:
show (2 : ℝ) ^ rank K = |∏ w : {w : InfinitePlace K⁺ // w ≠ w₀}, 2| by
    rw [Finset.prod_const, abs_pow, abs_of_pos zero_lt_two, ← units_rank_eq_units_rank K, rank]
    simp

Goal state after:
K : Type u_1
inst✝³ : Field K
inst✝² : CharZero K
inst✝¹ : IsCMField K
inst✝ : NumberField K
W₀ : InfinitePlace K := (equivInfinitePlace K).symm w₀
f : { w // w ≠ W₀ } ≃ { w // w ≠ w₀ } := (equivInfinitePlace K).subtypeEquiv ⋯
g : Fin (rank K) ≃ { w // w ≠ W₀ } := ((finCongr ⋯).trans (equivFinRank ↥K⁺)).trans f.symm
⊢ regOfFamily (realFundSystem K) = |∏ w, 2| * regulator ↥K⁺
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
⊢ ↑((primesOverSpanEquivMonicFactorsMod hp).symm ⟨Polynomial.map (Int.castRingHom (ZMod p)) Q, hQ⟩) =
    span {↑p, (aeval θ) Q}

Tactic:
simp only [primesOverSpanEquivMonicFactorsMod_symm_apply, Polynomial.map_map,
    Int.quotientSpanNatEquivZMod_comp_castRingHom]

Goal state after:
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
⊢ ↑((normalizedFactorsMapEquivNormalizedFactorsMinPolyMk ⋯ ⋯ ⋯ ⋯).symm
        ⟨Polynomial.map (Ideal.Quotient.mk (span {↑p})) Q, ⋯⟩) =
    span {↑p, (aeval θ) Q}
Module: Mathlib.RingTheory.RootsOfUnity.CyclotomicUnits

Goal state before:
pp: n : ℕ
A : Type u_1
ζ : A
inst✝¹ : CommRing A
inst✝ : IsDomain A
hζ : ζ ^ n = 1
hζ1 : ζ ≠ 1
key : ↑n = ∑ i ∈ range n, (1 - ζ ^ i)
i : ℕ
x✝ : i ∈ range n
h : ζ - 1 ∣ ζ ^ i - 1
⊢ ζ - 1 ∣ 1 - ζ ^ i

Tactic:
rwa [← dvd_neg, neg_sub] at h

Goal state after:
Module: Mathlib.RingTheory.RootsOfUnity.CyclotomicUnits

Goal state before:
pp: n j : ℕ
A : Type u_1
ζ : A
inst✝¹ : CommRing A
inst✝ : IsDomain A
hζ : IsPrimitiveRoot ζ n
hj : j.Coprime n
hj_Unit : IsUnit ↑j
⊢ IsUnit (∑ i ∈ range j, ζ ^ i)

Tactic:
by
  match n with
  | 0 => simp_all
  | 1 => simp_all
  | n + 2 => exact geom_sum_isUnit hζ (by linarith) hj

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ closure (paramSet K) = Set.univ.pi fun w ↦ if w = w₀ then Set.Iic 0 else Set.Icc 0 1

Tactic:
by
  simp [closure_pi_set, apply_ite]

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : realSpace K
hx : x ∈ compactSet K
w : InfinitePlace K
⊢ 0 ≤ x w

Tactic:
obtain ⟨c, hc, ⟨_, ⟨⟨a, ha, rfl⟩, _, rfl⟩⟩⟩ := hx

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w : InfinitePlace K
c : ℝ
hc : c ∈ Set.Icc 0 1
a : realSpace K
ha : a ∈ Set.univ.pi fun w ↦ if w = w₀ then {0} else Set.Icc 0 1
⊢ 0 ≤ (fun x1 x2 ↦ x1 • x2) c (↑expMapBasis a) w
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
this : IsBounded (↑expMapBasis '' paramSet K)
⊢ IsBounded (normAtAllPlaces ⁻¹' ↑expMapBasis '' paramSet K)

Tactic:
by
    obtain ⟨C, hC⟩ := isBounded_iff_forall_norm_le.mp this
    refine isBounded_iff_forall_norm_le.mpr ⟨C, fun x hx ↦ ?_⟩
    rw [norm_eq_sup'_normAtPlace]
    refine sup'_le _ _ fun w _ ↦ ?_
    simpa [normAtAllPlaces_apply, Real.norm_of_nonneg (normAtPlace_nonneg w x)]
      using (pi_norm_le_iff_of_nonempty _).mp (hC _ hx) w

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

Goal state before:
pp: n : ℕ
inst✝⁵ : NeZero n
K : Type u_1
inst✝⁴ : Field K
inst✝³ : NumberField K
hK : IsCyclotomicExtension {n} ℚ K
R : Type u_2
inst✝² : CommRing R
inst✝¹ : HasEnoughRootsOfUnity R (Monoid.exponent (ZMod n)ˣ)
inst✝ : IsMulCommutative Gal(K/ℚ)
H : Subgroup Gal(K/ℚ)
⊢ Nat.card ↥(OrderDual.ofDual (((galEquivZMod n K).mapSubgroup.trans (subgroupOrderIsoSubgroupMulChar (ZMod n) R)) H)) =
    Nat.card (Gal(K/ℚ) ⧸ H)

Tactic:
OrderIso.trans_apply,

Goal state after:
n : ℕ
inst✝⁵ : NeZero n
K : Type u_1
inst✝⁴ : Field K
inst✝³ : NumberField K
hK : IsCyclotomicExtension {n} ℚ K
R : Type u_2
inst✝² : CommRing R
inst✝¹ : HasEnoughRootsOfUnity R (Monoid.exponent (ZMod n)ˣ)
inst✝ : IsMulCommutative Gal(K/ℚ)
H : Subgroup Gal(K/ℚ)
⊢ Nat.card ↥(OrderDual.ofDual ((subgroupOrderIsoSubgroupMulChar (ZMod n) R) ((galEquivZMod n K).mapSubgroup H))) =
    Nat.card (Gal(K/ℚ) ⧸ H)
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Galois

Goal state before:
pp: n : ℕ
inst✝⁵ : NeZero n
K : Type u_1
inst✝⁴ : Field K
inst✝³ : NumberField K
hK : IsCyclotomicExtension {n} ℚ K
R : Type u_2
inst✝² : CommRing R
inst✝¹ : HasEnoughRootsOfUnity R (Monoid.exponent (ZMod n)ˣ)
inst✝ : IsAbelianGalois ℚ K
F : IntermediateField ℚ K
⊢ Nat.card
      ↥((IsGalois.intermediateFieldEquivSubgroup.trans
            ((subgroupGalEquivSubgroupChar n K R).dual.trans
              (OrderIso.dualDual (Subgroup (DirichletCharacter R n))).symm))
          F) =
    Module.finrank ℚ ↥F

Tactic:
OrderIso.trans_apply,

Goal state after:
n : ℕ
inst✝⁵ : NeZero n
K : Type u_1
inst✝⁴ : Field K
inst✝³ : NumberField K
hK : IsCyclotomicExtension {n} ℚ K
R : Type u_2
inst✝² : CommRing R
inst✝¹ : HasEnoughRootsOfUnity R (Monoid.exponent (ZMod n)ˣ)
inst✝ : IsAbelianGalois ℚ K
F : IntermediateField ℚ K
⊢ Nat.card
      ↥(((subgroupGalEquivSubgroupChar n K R).dual.trans (OrderIso.dualDual (Subgroup (DirichletCharacter R n))).symm)
          (IsGalois.intermediateFieldEquivSubgroup F)) =
    Module.finrank ℚ ↥F
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Galois

Goal state before:
pp: n : ℕ
inst✝⁵ : NeZero n
K : Type u_1
inst✝⁴ : Field K
inst✝³ : NumberField K
hK : IsCyclotomicExtension {n} ℚ K
R : Type u_2
inst✝² : CommRing R
inst✝¹ : HasEnoughRootsOfUnity R (Monoid.exponent (ZMod n)ˣ)
inst✝ : IsAbelianGalois ℚ K
F : IntermediateField ℚ K
⊢ Nat.card
      ↥(((subgroupGalEquivSubgroupChar n K R).dual.trans (OrderIso.dualDual (Subgroup (DirichletCharacter R n))).symm)
          (IsGalois.intermediateFieldEquivSubgroup F)) =
    Module.finrank ℚ ↥F

Tactic:
OrderIso.trans_apply,

Goal state after:
n : ℕ
inst✝⁵ : NeZero n
K : Type u_1
inst✝⁴ : Field K
inst✝³ : NumberField K
hK : IsCyclotomicExtension {n} ℚ K
R : Type u_2
inst✝² : CommRing R
inst✝¹ : HasEnoughRootsOfUnity R (Monoid.exponent (ZMod n)ˣ)
inst✝ : IsAbelianGalois ℚ K
F : IntermediateField ℚ K
⊢ Nat.card
      ↥((OrderIso.dualDual (Subgroup (DirichletCharacter R n))).symm
          ((subgroupGalEquivSubgroupChar n K R).dual (IsGalois.intermediateFieldEquivSubgroup F))) =
    Module.finrank ℚ ↥F
Module: Mathlib.NumberTheory.Ostrowski

Goal state before:
pp: ⊢ Tendsto (fun k ↦ ↑k ^ (↑k)⁻¹) atTop (𝓝 1)

Tactic:
simp_rw [← one_div]

Goal state after:
⊢ Tendsto (fun k ↦ ↑k ^ (1 / ↑k)) atTop (𝓝 1)
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
⊢ #S < #T

Tactic:
zify -- This is necessary to use card_S_eq
  rw [card_T_eq A, card_S_eq]
  rify -- This is necessary because ‖A‖ is a real number
  calc
  ∏ x : α, (∑ x_1 : β, ↑B * ↑(A x x_1)⁺ - ∑ x_1 : β, ↑B * -↑(A x x_1)⁻ + 1)
    ≤ ∏ x : α, (n * max 1 ‖A‖ * B + 1) := by
      refine Finset.prod_le_prod (fun i _ ↦ ?_) (fun i _ ↦ ?_)
      · have h := N_le_P_add_one A i
        rify at h
        linarith only [h]
      · simp only [mul_neg, sum_neg_distrib, sub_neg_eq_add, add_le_add_iff_right]
        have h1 : n * max 1 ‖A‖ * B = ∑ _ : β, max 1 ‖A‖ * B := by
          simp
          ring
        simp_rw [h1, ← Finset.sum_add_distrib, ← mul_add, mul_comm (max 1 ‖A‖), ← Int.cast_add]
        gcongr with j _
        rw [posPart_add_negPart (A i j), Int.cast_abs]
        exact le_trans (norm_entry_le_entrywise_sup_norm A) (le_max_right ..)
  _ = (n * max 1 ‖A‖ * B + 1) ^ m := by simp
  _ ≤ (n * max 1 ‖A‖) ^ m * (B + 1) ^ m := by
        rw [← mul_pow, mul_add, mul_one]
        gcongr
        have H : 1 ≤ (n : ℝ) := mod_cast (hm.trans hn)
        exact one_le_mul_of_one_le_of_one_le H <| le_max_left ..
  _ = ((n * max 1 ‖A‖) ^ (m / ((n : ℝ) - m))) ^ ((n : ℝ) - m) * (B + 1) ^ m := by
        congr 1
        rw [← rpow_mul (mul_nonneg (Nat.cast_nonneg' n) (le_trans zero_le_one (le_max_left ..))),
          ← Real.rpow_natCast, div_mul_cancel₀]
        exact sub_ne_zero_of_ne (mod_cast hn.ne')
  _ < (B + 1) ^ ((n : ℝ) - m) * (B + 1) ^ m := by
        gcongr
        · exact sub_pos.mpr (mod_cast hn)
        · exact Nat.lt_floor_add_one ((n * max 1 ‖A‖) ^ e)
  _ = (B + 1) ^ n := by
        rw [← rpow_natCast, ← rpow_add (Nat.cast_add_one_pos B), ← rpow_natCast, sub_add_cancel]

Goal state after:
Module: Mathlib.NumberTheory.Ostrowski

Goal state before:
pp: f : AbsoluteValue ℚ ℝ
n m : ℕ
hm : 1 < m
L : List ℕ := m.digits n
L' : List ℚ := List.map Nat.cast (List.mapIdx (fun i a ↦ a * m ^ i) L)
hcoef : ∀ {c : ℕ}, c ∈ m.digits n → f ↑c < ↑m
⊢ f ↑n ≤ (List.mapIdx (fun i x ↦ ↑m * f ↑m ^ i) L).sum

Tactic:
calc
  f n = f ((Nat.ofDigits m L : ℕ) : ℚ) := by rw [Nat.ofDigits_digits m n]
    _ = f L'.sum := by simp [L', Nat.ofDigits_eq_sum_mapIdx]
    _ ≤ (L'.map f).sum := listSum_le f L'
    _ ≤ (L.mapIdx fun i _ ↦ m * (f m) ^ i).sum := ?_

Goal state after:
f : AbsoluteValue ℚ ℝ
n m : ℕ
hm : 1 < m
L : List ℕ := m.digits n
L' : List ℚ := List.map Nat.cast (List.mapIdx (fun i a ↦ a * m ^ i) L)
hcoef : ∀ {c : ℕ}, c ∈ m.digits n → f ↑c < ↑m
⊢ (List.map (⇑f) L').sum ≤ (List.mapIdx (fun i x ↦ ↑m * f ↑m ^ i) L).sum
Module: Mathlib.NumberTheory.Ostrowski

Goal state before:
pp: f : AbsoluteValue ℚ ℝ
n m : ℕ
hm : 1 < m
L : List ℕ := m.digits n
L' : List ℚ := List.map Nat.cast (List.mapIdx (fun i a ↦ a * m ^ i) L)
hcoef : ∀ {c : ℕ}, c ∈ m.digits n → f ↑c < ↑m
x✝ : ℕ × ℕ
a i : ℕ
hia✝ : (a, i) ∈ L.zipIdx
hia : 0 ≤ i ∧ i < 0 + L.length ∧ a = L[i - 0]
⊢ f ↑a * f ↑m ^ i ≤ ↑m * f ↑m ^ i

Tactic:
refine mul_le_mul_of_nonneg_right ?_ <| pow_nonneg (f.nonneg _) i

Goal state after:
f : AbsoluteValue ℚ ℝ
n m : ℕ
hm : 1 < m
L : List ℕ := m.digits n
L' : List ℚ := List.map Nat.cast (List.mapIdx (fun i a ↦ a * m ^ i) L)
hcoef : ∀ {c : ℕ}, c ∈ m.digits n → f ↑c < ↑m
x✝ : ℕ × ℕ
a i : ℕ
hia✝ : (a, i) ∈ L.zipIdx
hia : 0 ≤ i ∧ i < 0 + L.length ∧ a = L[i - 0]
⊢ f ↑a ≤ ↑m
Module: Mathlib.NumberTheory.Ostrowski

Goal state before:
pp: f : AbsoluteValue ℚ ℝ
n m : ℕ
hm : 1 < m
L : List ℕ := m.digits n
L' : List ℚ := List.map Nat.cast (List.mapIdx (fun i a ↦ a * m ^ i) L)
hcoef : ∀ {c : ℕ}, c ∈ m.digits n → f ↑c < ↑m
x✝ : ℕ × ℕ
a i : ℕ
hia✝ : (a, i) ∈ L.zipIdx
hia : i < L.length ∧ a = L[i - 0]
⊢ f ↑a ≤ ↑m

Tactic:
exact (hcoef (List.mem_iff_get.mpr ⟨⟨i, hia.1⟩, hia.2.symm⟩)).le

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

Goal state before:
pp: p : ℕ
inst✝⁶ : Fact (Nat.Prime p)
R : Type u_1
inst✝⁵ : NormedRing R
inst✝⁴ : Algebra ℤ_[p] R
inst✝³ : IsBoundedSMul ℤ_[p] R
inst✝² : IsUltrametricDist R
inst✝¹ : CompleteSpace R
inst✝ : NormMulClass R
⊢ (fun r ↦ Tendsto (fun x ↦ r ^ x) atTop (𝓝 0)) = fun r ↦ ‖r‖ < 1

Tactic:
by simp only [tendsto_pow_atTop_nhds_zero_iff_norm_lt_one]

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)
ha : a ≠ 0
p q : ℕ
h0p : 0 < p
hpq : p < q
inst✝² : Fintype β
cardβ : Fintype.card β = q
A : ℝ
habs : ∀ (k : α) (l : β), house ((algebraMap (𝓞 K) K) (a k l)) ≤ A
inst✝¹ : DecidableEq (K →+* ℂ)
inst✝ : Fintype α
cardα : Fintype.card α = p
h : ℕ := finrank ℚ K
hphqh : p * h < q * h
h0ph : 0 < p * h
hfinp : Fintype.card (α × (K →+* ℂ)) = p * h
hfinq : Fintype.card (β × (K →+* ℂ)) = q * h
x : β × (K →+* ℂ) → ℤ
hxl : x ≠ 0
hmulvec0 : asiegel K a *ᵥ x = 0
hxbound :
  ‖x‖ ≤
    (↑(Fintype.card (β × (K →+* ℂ))) * ‖asiegel K a‖) ^
      (↑(Fintype.card (α × (K →+* ℂ))) / (↑(Fintype.card (β × (K →+* ℂ))) - ↑(Fintype.card (α × (K →+* ℂ)))))
⊢ ∃ ξ, ξ ≠ 0 ∧ a *ᵥ ξ = 0 ∧ ∀ (l : β), house ↑(ξ l) ≤ c₁ K * (c₁ K * ↑q * A) ^ (↑p / (↑q - ↑p))

Tactic:
simp only [hfinp, hfinq, Nat.cast_mul] at hmulvec0 hxbound

Goal state after:
K : Type u_1
inst✝⁴ : Field K
inst✝³ : NumberField K
α : Type u_2
β : Type u_3
a : Matrix α β (𝓞 K)
ha : a ≠ 0
p q : ℕ
h0p : 0 < p
hpq : p < q
inst✝² : Fintype β
cardβ : Fintype.card β = q
A : ℝ
habs : ∀ (k : α) (l : β), house ((algebraMap (𝓞 K) K) (a k l)) ≤ A
inst✝¹ : DecidableEq (K →+* ℂ)
inst✝ : Fintype α
cardα : Fintype.card α = p
h : ℕ := finrank ℚ K
hphqh : p * h < q * h
h0ph : 0 < p * h
hfinp : Fintype.card (α × (K →+* ℂ)) = p * h
hfinq : Fintype.card (β × (K →+* ℂ)) = q * h
x : β × (K →+* ℂ) → ℤ
hxl : x ≠ 0
hmulvec0 : asiegel K a *ᵥ x = 0
hxbound : ‖x‖ ≤ (↑q * ↑h * ‖asiegel K a‖) ^ (↑p * ↑h / (↑q * ↑h - ↑p * ↑h))
⊢ ∃ ξ, ξ ≠ 0 ∧ a *ᵥ ξ = 0 ∧ ∀ (l : β), house ↑(ξ l) ≤ c₁ K * (c₁ K * ↑q * A) ^ (↑p / (↑q - ↑p))
Module: Mathlib.NumberTheory.Padics.Complex

Goal state before:
pp: case hg
p : ℕ
hp : Fact (Nat.Prime p)
⊢ UniformContinuous Valued.v.norm

Tactic:
let S := (Valued.toNormedField ℂ_[p] NNReal).toNormedCommRing.toNormedRing.toSeminormedRing
    let := S.toNonUnitalSeminormedRing.toSeminormedAddCommGroup.toSeminormedAddGroup
    exact @uniformContinuous_norm ℂ_[p] this

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)
ha : a ≠ 0
p q : ℕ
h0p : 0 < p
hpq : p < q
inst✝² : Fintype β
cardβ : Fintype.card β = q
A : ℝ
habs : ∀ (k : α) (l : β), house ((algebraMap (𝓞 K) K) (a k l)) ≤ A
inst✝¹ : DecidableEq (K →+* ℂ)
inst✝ : Fintype α
cardα : Fintype.card α = p
h : ℕ := finrank ℚ K
hphqh : p * h < q * h
h0ph : 0 < p * h
hfinp : Fintype.card (α × (K →+* ℂ)) = p * h
hfinq : Fintype.card (β × (K →+* ℂ)) = q * h
x : β × (K →+* ℂ) → ℤ
hxl : x ≠ 0
hmulvec0 : asiegel K a *ᵥ x = 0
hxbound : ‖x‖ ≤ (↑q * ↑h * ‖asiegel K a‖) ^ (↑p / (↑q - ↑p))
⊢ 0 ≤ A

Tactic:
have ⟨k⟩ := Fintype.card_pos_iff.1 (cardα ▸ h0p)

Goal state after:
K : Type u_1
inst✝⁴ : Field K
inst✝³ : NumberField K
α : Type u_2
β : Type u_3
a : Matrix α β (𝓞 K)
ha : a ≠ 0
p q : ℕ
h0p : 0 < p
hpq : p < q
inst✝² : Fintype β
cardβ : Fintype.card β = q
A : ℝ
habs : ∀ (k : α) (l : β), house ((algebraMap (𝓞 K) K) (a k l)) ≤ A
inst✝¹ : DecidableEq (K →+* ℂ)
inst✝ : Fintype α
cardα : Fintype.card α = p
h : ℕ := finrank ℚ K
hphqh : p * h < q * h
h0ph : 0 < p * h
hfinp : Fintype.card (α × (K →+* ℂ)) = p * h
hfinq : Fintype.card (β × (K →+* ℂ)) = q * h
x : β × (K →+* ℂ) → ℤ
hxl : x ≠ 0
hmulvec0 : asiegel K a *ᵥ x = 0
hxbound : ‖x‖ ≤ (↑q * ↑h * ‖asiegel K a‖) ^ (↑p / (↑q - ↑p))
k : α
⊢ 0 ≤ A
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:
mul_div_cancel₀ _ (mod_cast k.factorial_ne_zero),

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

Goal state before:
pp: case refine_1
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)
s t : ℕ
hst : ∀ (x y : ℤ_[p]), ‖x - y‖ ≤ ↑p ^ (-↑t) → ‖f x - f y‖ ≤ ‖f‖ / ↑p ^ s
n i : ℕ
hi : i < p ^ t - 1
this : 0 < (p ^ t).choose (i + 1)
⊢ ↑p ^ (-↑(↑((p ^ t).choose (i + 1))).valuation) ≤ ↑(↑p ^ (-1))

Tactic:
coe_zpow,

Goal state after:
case refine_1
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)
s t : ℕ
hst : ∀ (x y : ℤ_[p]), ‖x - y‖ ≤ ↑p ^ (-↑t) → ‖f x - f y‖ ≤ ‖f‖ / ↑p ^ s
n i : ℕ
hi : i < p ^ t - 1
this : 0 < (p ^ t).choose (i + 1)
⊢ ↑p ^ (-↑(↑((p ^ t).choose (i + 1))).valuation) ≤ ↑↑p ^ (-1)
Module: Mathlib.NumberTheory.Padics.WithVal

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
hp0' : 0 < ↑p
⊢ IsUniformInducing ⇑((Rat.castHom ℚ_[p]).comp (WithVal.equiv (Rat.padicValuation p)).toRingHom)

Tactic:
have hp0 : 0 < (p : ℝ)⁻¹ := by simp [Nat.Prime.pos Fact.out]

Goal state after:
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp0' : 0 < ↑p
hp0 : 0 < (↑p)⁻¹
⊢ IsUniformInducing ⇑((Rat.castHom ℚ_[p]).comp (WithVal.equiv (Rat.padicValuation p)).toRingHom)
Module: Mathlib.NumberTheory.Padics.WithVal

Goal state before:
pp: case hp
p : ℕ
inst✝ : Fact (Nat.Prime p)
⊢ IsClosed
    {a |
      ⋯.extend coe' ((extensionHom ((Rat.castHom ℚ_[p]).comp (WithVal.equiv (Rat.padicValuation p)).toRingHom) ⋯) a) =
        a}

Tactic:
generalize_proofs _ _ _ H
      refine isClosed_eq ?_ continuous_id
      exact (uniformContinuous_uniformly_extend Padic.isUniformInducing_cast_withVal
        Padic.isDenseInducing_cast_withVal.dense (uniformContinuous_coe _)).continuous.comp
        (continuous_extension)

Goal state after:
Module: Mathlib.NumberTheory.Padics.Measure.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
R : Type u_3
inst✝⁶ : TopologicalSpace X
inst✝⁵ : TopologicalSpace Y
inst✝⁴ : CommRing R
inst✝³ : TopologicalSpace R
inst✝² : IsTopologicalRing R
μ : AbstractMeasure X R R
ν : AbstractMeasure Y R R
inst✝¹ : LocallyCompactSpace X
inst✝ : LocallyCompactSpace Y
f : C(X, R)
g : C(Y, R)
⊢ ((prodMk μ) ν) (f.comp fst * g.comp snd) = μ f * ν g

Tactic:
by
  simp only [← smul_eq_mul, prodMk_apply, ← map_smul]
  congr 1 with y
  simp_rw [contractFst_apply, ContinuousMap.smul_apply, smul_eq_mul, mul_comm (μ f) (g y),
    ← smul_eq_mul, ← map_smul]
  congr 1 with x
  simp_rw [ContinuousMap.smul_apply, smul_eq_mul, mul_comm (g y) (f x)]
  rfl

Goal state after:
Module: Mathlib.NumberTheory.Pell

Goal state before:
pp: d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
ξ : ℝ := √↑d
hξ : Irrational ξ
M : ℤ
hM₁ : 2 * |ξ| + 1 < ↑M
q : ℚ
h : |↑q - ξ| < 1 / ↑q.den ^ 2
h0 : 0 < ↑q.den ^ 2
h1 : ↑q.num / ↑q.den = ↑q
⊢ 1 ≤ ↑q.den ^ 2

Tactic:
one_le_sq_iff_one_le_abs,

Goal state after:
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
ξ : ℝ := √↑d
hξ : Irrational ξ
M : ℤ
hM₁ : 2 * |ξ| + 1 < ↑M
q : ℚ
h : |↑q - ξ| < 1 / ↑q.den ^ 2
h0 : 0 < ↑q.den ^ 2
h1 : ↑q.num / ↑q.den = ↑q
⊢ 1 ≤ |↑q.den|
Module: Mathlib.NumberTheory.Pell

Goal state before:
pp: d : ℤ
a : Solution₁ d
h : IsFundamental a
n : ℤ
⊢ a ^ n = 1 ↔ n = 0

Tactic:
rw [← zpow_zero a]
  exact ⟨fun H => h.y_strictMono.injective (congr_arg Solution₁.y H), fun H => H ▸ rfl⟩

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

Goal state before:
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
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
span_d : Submodule.restrictScalars R (S ∙ f A.det) ≤ M
⊢ ⊤ = Submodule.restrictScalars K (span {(algebraMap R L) A.det})

Tactic:
rw [eq_comm, Submodule.restrictScalars_eq_top_iff, Ideal.span_singleton_eq_top]
    refine IsUnit.mk0 _ ((map_ne_zero_iff (algebraMap R L) hRL).mpr ?_)
    refine ne_zero_of_map («f» := Ideal.Quotient.mk p) ?_
    have := Ideal.Quotient.nontrivial_iff.mpr hp
    calc
      Ideal.Quotient.mk p A.det = Matrix.det ((Ideal.Quotient.mk p).mapMatrix A) := by
        rw [RingHom.map_det]
      _ = Matrix.det ((Ideal.Quotient.mk p).mapMatrix (Matrix.of A' - 1)) := rfl
      _ = Matrix.det fun i j =>
          (Ideal.Quotient.mk p) (A' i j) - (1 : Matrix (Fin n) (Fin n) (R ⧸ p)) i j := ?_
      _ = Matrix.det (-1 : Matrix (Fin n) (Fin n) (R ⧸ p)) := ?_
      _ = (-1 : R ⧸ p) ^ n := by rw [Matrix.det_neg, Fintype.card_fin, Matrix.det_one, mul_one]
      _ ≠ 0 := IsUnit.ne_zero (isUnit_one.neg.pow _)
    · refine congr_arg Matrix.det (Matrix.ext fun i j => ?_)
      rw [map_sub, RingHom.mapMatrix_apply, map_one]
      simp
    · refine congr_arg Matrix.det (Matrix.ext fun i j => ?_)
      rw [Ideal.Quotient.eq_zero_iff_mem.mpr (hA'p i j), zero_sub, Matrix.neg_apply]

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

Goal state before:
pp: case hH
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
⊢ Subgroup.zpowers ⋯.unit = (MonoidWithZeroHom.ofClass v).valueGroup

Tactic:
ext γ
    simp only [coePolynomial_eq_algebraMap, MonoidWithZeroHom.mem_valueGroup_iff_of_comm, ne_eq,
      map_eq_zero, Subgroup.mem_zpowers_iff]
    refine ⟨fun ⟨k, hk⟩ ↦ ?_, fun ⟨a, ha, b, hab⟩ ↦ ?_⟩
    · use 1, one_ne_zero, πᵥ ^ k
      simp only [← Units.val_inj, Units.val_zpow_eq_zpow_val] at hk
      simp [← hk]
    · obtain ⟨ka, hka⟩ := exists_zpow_uniformizingPolynomial hle ha
      obtain ⟨kb, hkb⟩ := exists_zpow_uniformizingPolynomial hle (f := b) (by aesop)
      rw [MonoidWithZeroHom.coe_ofClass, hka, hkb] at hab
      use kb - ka
      have : v ↑πᵥ ^ ka ≠ 0 := zpow_ne_zero _ h0
      simp [zpow_sub, ← Units.val_inj, ← coePolynomial_eq_algebraMap, field, ← hab]

Goal state after: