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

Goal state before:
pp: K : Type u_2
inst✝⁵ : Field K
inst✝⁴ : CharZero K
inst✝³ : Algebra.IsIntegral ℚ K
inst✝² : IsTotallyComplex K
E : Subfield K
inst✝¹ : IsTotallyReal ↥E
inst✝ : IsQuadraticExtension (↥E) K
h : ¬maximalRealSubfield K ≤ E
L : IntermediateField (↥E) K := (E ⊔ maximalRealSubfield K).toIntermediateField ⋯
⊢ E ⊔ maximalRealSubfield K = ⊤

Tactic:
have := ((IntermediateField.isSimpleOrder_of_finrank_prime E K
      (IsQuadraticExtension.finrank_eq_two E K ▸ Nat.prime_two)).eq_bot_or_eq_top L).resolve_left ?_

Goal state after:
case refine_2
K : Type u_2
inst✝⁵ : Field K
inst✝⁴ : CharZero K
inst✝³ : Algebra.IsIntegral ℚ K
inst✝² : IsTotallyComplex K
E : Subfield K
inst✝¹ : IsTotallyReal ↥E
inst✝ : IsQuadraticExtension (↥E) K
h : ¬maximalRealSubfield K ≤ E
L : IntermediateField (↥E) K := (E ⊔ maximalRealSubfield K).toIntermediateField ⋯
this : L = ⊤
⊢ E ⊔ maximalRealSubfield K = ⊤

case refine_1
K : Type u_2
inst✝⁵ : Field K
inst✝⁴ : CharZero K
inst✝³ : Algebra.IsIntegral ℚ K
inst✝² : IsTotallyComplex K
E : Subfield K
inst✝¹ : IsTotallyReal ↥E
inst✝ : IsQuadraticExtension (↥E) K
h : ¬maximalRealSubfield K ≤ E
L : IntermediateField (↥E) K := (E ⊔ maximalRealSubfield K).toIntermediateField ⋯
⊢ ¬L = ⊥
Module: Mathlib.NumberTheory.NumberField.CMField

Goal state before:
pp: F : Type u_1
K : Type u_2
inst✝⁷ : Field F
inst✝⁶ : IsTotallyReal F
inst✝⁵ : Field K
inst✝⁴ : CharZero K
inst✝³ : Algebra.IsIntegral ℚ K
inst✝² : IsTotallyComplex K
inst✝¹ : Algebra F K
inst✝ : IsQuadraticExtension F K
this : IsTotallyReal ↥(algebraMap F K).fieldRange
x✝ : ↥(algebraMap F K).fieldRange
⊢ ↑x✝ = (algebraMap (↥(algebraMap F K).fieldRange) K) x✝

Tactic:
rfl

Goal state after:
Module: Mathlib.NumberTheory.NumberField.Units.Regulator

Goal state before:
pp: case e_a
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
u : Fin (rank K) → (𝓞 K)ˣ
w' : InfinitePlace K
e : { w // w ≠ w' } ≃ Fin (rank K)
f : Fin (rank K + 1) ≃ InfinitePlace K := (finSuccEquiv (rank K)).trans ↑((Equiv.optionSubtype w').symm e.symm)
g : { w // w ≠ w' } ≃ Fin (rank K) := (f.symm.subtypeEquiv ⋯).trans (finSuccAboveEquiv (f.symm w')).symm
i j : Fin (rank K)
⊢ ↑(↑(g.symm j)).mult * Real.log (↑(g.symm j) ((algebraMap (𝓞 K) K) ↑(u (e (g.symm i))))) =
    ↑(f ((f.symm w').succAbove j)).mult *
      Real.log ((f ((f.symm w').succAbove j)) ((algebraMap (𝓞 K) K) ↑(u (e ⟨f ((f.symm w').succAbove i), ?e_a.hnc✝⟩))))

pp: case e_a.hnc
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
u : Fin (rank K) → (𝓞 K)ˣ
w' : InfinitePlace K
e : { w // w ≠ w' } ≃ Fin (rank K)
f : Fin (rank K + 1) ≃ InfinitePlace K := (finSuccEquiv (rank K)).trans ↑((Equiv.optionSubtype w').symm e.symm)
g : { w // w ≠ w' } ≃ Fin (rank K) := (f.symm.subtypeEquiv ⋯).trans (finSuccAboveEquiv (f.symm w')).symm
i j : Fin (rank K)
⊢ ¬f ((f.symm w').succAbove i) = w'

Tactic:
rfl

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

Goal state before:
pp: K : Type u_1
inst✝² : Field K
inst✝¹ : CharZero K
S : Set ℕ
inst✝ : IsCyclotomicExtension S ℚ K
this✝ : Algebra.IsIntegral ℚ K
n : ℕ
hn₁ : n ∈ S
hn₂ : 2 < n
this : NeZero n
⊢ n ≠ 0

Tactic:
grind

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

Goal state before:
pp: p✝ : ℕ
A✝ : Type u_1
ζ✝ : A✝
inst✝³ : CommRing A✝
inst✝² : IsDomain A✝
p : ℕ
A : Type u_1
ζ : A
inst✝¹ : CommRing A
inst✝ : IsDomain A
hζ : IsPrimitiveRoot ζ p
hp : Nat.Prime p
this : NeZero p
i : ℕ
hi : i < p
hη₁ : ζ ^ i ∈ ↑(nthRootsFinset p 1)
j : ℕ
hj : j < p
hη₂ : ζ ^ j ∈ ↑(nthRootsFinset p 1)
e : ζ ^ i ≠ ζ ^ j
hij : j ≤ i
⊢ i - j ≠ 0

Tactic:
grind

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

Goal state before:
pp: p✝ : ℕ
A✝ : Type u_1
ζ✝ : A✝
inst✝³ : CommRing A✝
inst✝² : IsDomain A✝
p : ℕ
A : Type u_1
ζ : A
inst✝¹ : CommRing A
inst✝ : IsDomain A
hζ : IsPrimitiveRoot ζ p
hp : Nat.Prime p
this : NeZero p
i : ℕ
hi : i < p
hη₁ : ζ ^ i ∈ ↑(nthRootsFinset p 1)
j : ℕ
hj : j < p
hη₂ : ζ ^ j ∈ ↑(nthRootsFinset p 1)
e : ζ ^ i ≠ ζ ^ j
hij : j ≤ i
⊢ i - j < p

Tactic:
grind

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

Goal state before:
pp: K : Type u_1
inst✝² : Field K
I : Ideal (𝓞 K)
inst✝¹ : NumberField K
n : ℕ
inst✝ : NeZero n
hI₁ : absNorm I ≠ 1
hI₂ : (absNorm I).Coprime n
x✝ : ↥(rootsOfUnity n (𝓞 K))
ζ : (𝓞 K)ˣ
hζ✝ : ζ ∈ rootsOfUnity n (𝓞 K)
h : (I.rootsOfUnityMapQuot n) ⟨ζ, hζ✝⟩ = 1
t : ℕ
ht₀ : t ≠ 0
ht : t ∣ n
hζ : IsPrimitiveRoot ζ t
this : ¬2 ≤ t
⊢ t = 1

Tactic:
grind

Goal state after:
Module: Mathlib.NumberTheory.NumberField.Units.Regulator

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
u : Fin (rank K) → (𝓞 K)ˣ
⊢ Subgroup.closure (Set.range u) ⊔ torsion K ≤ Subgroup.closure (Set.range (fundSystem K)) ⊔ torsion K

Tactic:
simp only [closure_fundSystem_sup_torsion_eq_top, le_top]

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

Goal state before:
pp: case neg
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
hc' : 0 < c
w : InfinitePlace K
h : ¬w = w₀
⊢ y w = y w

Tactic:
rfl

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

Goal state before:
pp: case pos
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
y : realSpace K
hy : y ∈ Set.univ.pi fun w ↦ if w = w₀ then Set.Iic 0 else Set.Icc 0 1
hx₀ : ↑expMapBasis y ≠ 0
w : InfinitePlace K
h : w = w₀
⊢ 0 ∈ {0}

Tactic:
rfl

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 : ℝ
⊢ primeIdealZetaSum S s = ∑' (𝔭 : ↑S), ↑(Ideal.absNorm (↑𝔭).asIdeal) ^ (-s)

Tactic:
rfl

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 ((subgroupOrderIsoSubgroupMulChar (ZMod n) R) ((galEquivZMod n K).mapSubgroup H))) =
    Nat.card (Gal(K/ℚ) ⧸ H)

Tactic:
card_subgroupOrderIsoSubgroupMulChar

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 ((ZMod n)ˣ ⧸ (galEquivZMod n K).mapSubgroup H) = Nat.card (Gal(K/ℚ) ⧸ H)
Module: Mathlib.NumberTheory.NumberField.Ideal.Asymptotics

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
C : ClassGroup (𝓞 K)
J : ↥(Ideal (𝓞 K))⁰
s : ℝ
hJ : ClassGroup.mk0 J = C⁻¹
I : ↥(Ideal (𝓞 K))⁰
⊢ C = ClassGroup.mk0 I → (↑(absNorm ↑I) ≤ s ↔ ↑(absNorm ↑J) * ↑(absNorm ↑I) ≤ ↑(absNorm ↑J) * s)

Tactic:
exact fun _ ↦
    (mul_le_mul_iff_of_pos_left (Nat.cast_pos.mpr (absNorm_pos_of_nonZeroDivisors J))).symm

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
s : Finset ι
α : ι → K
b✝ : ι
a✝ : b✝ ∈ s
⊢ ‖(canonicalEmbedding K) (α b✝)‖ ≤ ‖(canonicalEmbedding K) (α b✝)‖

Tactic:
rfl

Goal state after:
Module: Mathlib.NumberTheory.Ostrowski

Goal state before:
pp: f : AbsoluteValue ℚ ℝ
hf_nontriv : f.IsNontrivial
bdd : ∀ (n : ℕ), f ↑n ≤ 1
⊢ ∃ p, (0 < f ↑p ∧ f ↑p < 1) ∧ ∀ (m : ℕ), 0 < f ↑m ∧ f ↑m < 1 → p ≤ m

Tactic:
by
  -- There is a positive integer with absolute value different from one.
  obtain ⟨n, hn1, hn2⟩ : ∃ n : ℕ, n ≠ 0 ∧ f n ≠ 1 := by
    contrapose! hf_nontriv
    refine (isNontrivial_iff_ne_trivial f).not_left.mpr <| eq_on_nat_iff_eq.mp fun n ↦ ?_
    rcases eq_or_ne n 0 with rfl | hn
    · simp
    · simp [hf_nontriv, hn]
  set P := {m : ℕ | 0 < f ↑m ∧ f ↑m < 1} -- p is going to be the minimum of this set.
  have hP : P.Nonempty :=
    ⟨n, map_pos_of_ne_zero f (Nat.cast_ne_zero.mpr hn1), lt_of_le_of_ne (bdd n) hn2⟩
  exact ⟨sInf P, Nat.sInf_mem hP, fun _ hm ↦ Nat.sInf_le hm⟩

Goal state after:
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

Tactic:
grind

Goal state after:
Module: Mathlib.NumberTheory.Ostrowski

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

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

Goal state before:
pp: case calc_1
K : Type u_1
inst✝⁴ : Field K
inst✝³ : NumberField K
α : Type u_2
β : Type u_3
a : Matrix α β (𝓞 K)
inst✝² : Fintype β
A : ℝ
habs : ∀ (k : α) (l : β), house ((algebraMap (𝓞 K) K) (a k l)) ≤ A
inst✝¹ : DecidableEq (K →+* ℂ)
inst✝ : Fintype α
Apos : 0 ≤ A
this : 0 ≤ c K
kr : α × (K →+* ℂ)
lu : β × (K →+* ℂ)
⊢ ‖asiegel K a kr lu‖ = ‖↑(asiegel K a kr lu)‖

Tactic:
rfl

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

Goal state before:
pp: case calc_2
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, house ((algebraMap (𝓞 K) K) ↑(x (l, r)) * (algebraMap (𝓞 K) K) ((newBasis K) r)) ≤
    ∑ r, ‖x (l, r)‖ * house ((algebraMap (𝓞 K) K) ((newBasis K) r))

Tactic:
gcongr with r _

Goal state after:
case h
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 : K →+* ℂ
a✝ : r ∈ univ
⊢ house ((algebraMap (𝓞 K) K) ↑(x (l, r)) * (algebraMap (𝓞 K) K) ((newBasis K) r)) ≤
    ‖x (l, r)‖ * house ((algebraMap (𝓞 K) K) ((newBasis K) r))
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)‖ * univ.sup' ⋯ fun r ↦ house ((algebraMap (𝓞 K) K) ((newBasis K) r))

Tactic:
gcongr with r _

Goal state after:
case hbc
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 : ℕ := ⋯
l : β
H₀ : 0 ≤ supOfBasis K
H₁ : 0 < ↑q - ↑p
r : K →+* ℂ
a✝ : r ∈ univ
⊢ house ((algebraMap (𝓞 K) K) ((newBasis K) r)) ≤ univ.sup' ⋯ fun r ↦ house ((algebraMap (𝓞 K) K) ((newBasis K) r))
Module: Mathlib.NumberTheory.NumberField.House

Goal state before:
pp: case calc_4
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)‖ * supOfBasis K ≤ ∑ _r, (↑q * ↑h * ‖asiegel K a‖) ^ (↑p / (↑q - ↑p)) * supOfBasis K

Tactic:
gcongr with r _

Goal state after:
case hbc
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 : ℕ := ⋯
l : β
H₀ : 0 ≤ supOfBasis K
H₁ : 0 < ↑q - ↑p
r : K →+* ℂ
a✝ : r ∈ univ
⊢ ‖x (l, r)‖ ≤ (↑q * ↑h * ‖asiegel K a‖) ^ (↑p / (↑q - ↑p))
Module: Mathlib.NumberTheory.NumberField.House

Goal state before:
pp: case calc_6
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
⊢ ↑h * c₂ K * (c₁ K * ↑q * A) ^ (↑p / (↑q - ↑p)) ≤ c₁ K * (c₁ K * ↑q * A) ^ (↑p / (↑q - ↑p))

Tactic:
rfl

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
⊢ (fun x ↦ ‖x‖) = Norm.norm

Tactic:
rfl

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
k : ℕ
x : ℤ_[p]
f : ℤ_[p] → ℤ_[p] := fun x ↦ Polynomial.eval x (ascPochhammer ℤ_[p] k)
hC : ↑k.factorial ≠ 0
hf : ContinuousAt f x
n : ℕ
hn : ‖f x - f ↑n‖ ≤ ‖↑k.factorial‖
⊢ ‖↑(Polynomial.eval n (ascPochhammer ℕ k))‖ ≤ ‖↑k.factorial‖

Tactic:
Polynomial.eval_eq_smeval,

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
k : ℕ
x : ℤ_[p]
f : ℤ_[p] → ℤ_[p] := fun x ↦ Polynomial.eval x (ascPochhammer ℤ_[p] k)
hC : ↑k.factorial ≠ 0
hf : ContinuousAt f x
n : ℕ
hn : ‖f x - f ↑n‖ ≤ ‖↑k.factorial‖
⊢ ‖↑((ascPochhammer ℕ k).smeval n)‖ ≤ ‖↑k.factorial‖
Module: Mathlib.NumberTheory.Padics.MahlerBasis

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
k : ℕ
⊢ ‖↑(Polynomial.eval x (ascPochhammer ℤ_[p] k)) / ↑k.factorial‖ ≤ 1

Tactic:
rw [norm_div, div_le_one (by simpa using k.factorial_ne_zero)]

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
x : ℤ_[p]
k : ℕ
⊢ Polynomial.eval x (ascPochhammer ℤ_[p] k) = (ascPochhammer ℕ k).smeval x

Tactic:
Polynomial.eval_eq_smeval,

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

Goal state before:
pp: R✝ : Type u_1
inst✝⁷ : CommRing R✝
inst✝⁶ : Algebra R✝ ℚ
inst✝⁵ : IsIntegralClosure R✝ ℤ ℚ
R : Type u_2
inst✝⁴ : CommRing R
inst✝³ : Algebra R ℚ
inst✝² : IsIntegralClosure R ℤ ℚ
inst✝¹ : IsDedekindDomain R
inst✝ : IsFractionRing R ℚ
v : HeightOneSpectrum R
x✝ : HeightOneSpectrum.adicCompletion ℚ v
⊢ Valued.v x✝ ≤ 1 ↔ (HeightOneSpectrum.adicCompletion.equiv ℚ v) x✝ ∈ Valued.v.valuationSubring

Tactic:
rfl

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

Goal state before:
pp: R✝ : Type u_1
inst✝⁷ : CommRing R✝
inst✝⁶ : Algebra R✝ ℚ
inst✝⁵ : IsIntegralClosure R✝ ℤ ℚ
R : Type u_2
inst✝⁴ : CommRing R
inst✝³ : Algebra R ℚ
inst✝² : IsIntegralClosure R ℤ ℚ
inst✝¹ : IsDedekindDomain R
inst✝ : IsFractionRing R ℚ
v : HeightOneSpectrum R
x✝ : HeightOneSpectrum.adicCompletion ℚ v
⊢ Valued.v x✝ ≤ 1 ↔ (HeightOneSpectrum.adicCompletion.uniformEquiv ℚ v) x✝ ∈ Valued.v.valuationSubring

Tactic:
rfl

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 : ∀ x ∈ diagonal V, S ∈ 𝓝 x
⊢ ∀ x ∈ diagonal X, ⇑(f.prodMap f) ⁻¹' S ∈ 𝓝 x

Tactic:
rintro ⟨x, y⟩ (rfl : x = y)

Goal state after:
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 : ∀ x ∈ diagonal V, S ∈ 𝓝 x
x : X
⊢ ⇑(f.prodMap f) ⁻¹' S ∈ 𝓝 (x, x)
Module: Mathlib.NumberTheory.Padics.Measure.Basic

Goal state before:
pp: case e_6.e_6
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)
y : Y
x : X
⊢ { toFun := fun x ↦ (f.comp fst * g.comp snd) (x, y), continuous_toFun := ⋯ } x = f x * g y

Tactic:
rfl

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

Goal state before:
pp: case e_6
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)
x : X
⊢ ν { toFun := fun y ↦ (f.comp fst • g.comp snd) (x, y), continuous_toFun := ⋯ } = ν (f x • g)

Tactic:
rfl

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

Goal state before:
pp: case add
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✝⁵ : CompactSpace X
inst✝⁴ : CompactSpace Y
inst✝³ : T2Space X
inst✝² : T2Space Y
inst✝¹ : TotallyDisconnectedSpace X
inst✝ : T0Space R
x✝ y✝ : TensorProduct R C(X, R) C(Y, R)
a✝¹ : (⇑((prodMk μ) ν) ∘ ⇑tensorHom) x✝ = (⇑((prodMk' μ) ν) ∘ ⇑tensorHom) x✝
a✝ : (⇑((prodMk μ) ν) ∘ ⇑tensorHom) y✝ = (⇑((prodMk' μ) ν) ∘ ⇑tensorHom) y✝
⊢ (⇑((prodMk μ) ν) ∘ ⇑tensorHom) (x✝ + y✝) = (⇑((prodMk' μ) ν) ∘ ⇑tensorHom) (x✝ + y✝)

Tactic:
grind

Goal state after:
Module: Mathlib.NumberTheory.PrimesCongruentOne

Goal state before:
pp: k n : ℕ
hk0 : k ≠ 0
hk1 : 1 < k
b : ℕ := k * n !
hgt : 1 < (eval (↑b) (cyclotomic k ℤ)).natAbs
p : ℕ := (eval (↑b) (cyclotomic k ℤ)).natAbs.minFac
hprime : Fact (Prime p)
this : ↑↑b = (Int.castRingHom (ZMod p)) ↑b
⊢ eval₂ (Int.castRingHom (ZMod p)) (↑b) (cyclotomic k ℤ) = 0

Tactic:
← Int.cast_natCast,

Goal state after:
k n : ℕ
hk0 : k ≠ 0
hk1 : 1 < k
b : ℕ := k * n !
hgt : 1 < (eval (↑b) (cyclotomic k ℤ)).natAbs
p : ℕ := (eval (↑b) (cyclotomic k ℤ)).natAbs.minFac
hprime : Fact (Prime p)
this : ↑↑b = (Int.castRingHom (ZMod p)) ↑b
⊢ eval₂ (Int.castRingHom (ZMod p)) (↑↑b) (cyclotomic k ℤ) = 0
Module: Mathlib.NumberTheory.Pell

Goal state before:
pp: d : ℤ
a b : Solution₁ d
⊢ (a * b).x = a.x * b.x + d * a.y * b.y

Tactic:
rfl

Goal state after:
Module: Mathlib.NumberTheory.Pell

Goal state before:
pp: case ofNat.zero
d : ℤ
a : Solution₁ d
hax : 0 < a.x
hay : 0 < a.y
⊢ (a ^ Int.ofNat 0).y.sign = (Int.ofNat 0).sign

Tactic:
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 ∈ {q | |ξ - ↑q| < 1 / ↑q.den ^ 2}
h0 : 0 < ↑q.den ^ 2
h1 : ↑q.num / ↑q.den = ↑q
⊢ q ∈ {q | |q.num ^ 2 - d * ↑q.den ^ 2| < M}

Tactic:
mem_ofPred,

Goal state after:
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
ξ : ℝ := √↑d
hξ : Irrational ξ
M : ℤ
hM₁ : 2 * |ξ| + 1 < ↑M
q : ℚ
h : q ∈ {q | |ξ - ↑q| < 1 / ↑q.den ^ 2}
h0 : 0 < ↑q.den ^ 2
h1 : ↑q.num / ↑q.den = ↑q
⊢ |q.num ^ 2 - d * ↑q.den ^ 2| < M
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 ∈ {q | |ξ - ↑q| < 1 / ↑q.den ^ 2}
h0 : 0 < ↑q.den ^ 2
h1 : ↑q.num / ↑q.den = ↑q
⊢ |↑q| - |ξ| ≤ 1

Tactic:
mem_ofPred,

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
⊢ |↑q| - |ξ| ≤ 1
Module: Mathlib.NumberTheory.Pell

Goal state before:
pp: d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
ξ : ℝ := √↑d
hξ : Irrational ξ
M : ℤ
hM₁ : 2 * |ξ| + 1 < ↑M
hM : {q | |q.num ^ 2 - d * ↑q.den ^ 2| < M}.Infinite
hm : {q | q.num ^ 2 - d * ↑q.den ^ 2 = 0}.Infinite
q : ℚ
hq : q ∈ {q | q.num ^ 2 - d * ↑q.den ^ 2 = 0}
⊢ False

Tactic:
mem_ofPred,

Goal state after:
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
ξ : ℝ := √↑d
hξ : Irrational ξ
M : ℤ
hM₁ : 2 * |ξ| + 1 < ↑M
hM : {q | |q.num ^ 2 - d * ↑q.den ^ 2| < M}.Infinite
hm : {q | q.num ^ 2 - d * ↑q.den ^ 2 = 0}.Infinite
q : ℚ
hq : q.num ^ 2 - d * ↑q.den ^ 2 = 0
⊢ False
Module: Mathlib.NumberTheory.Pell

Goal state before:
pp: case refine_1
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
ξ : ℝ := √↑d
hξ : Irrational ξ
M : ℤ
hM₁ : 2 * |ξ| + 1 < ↑M
hM : {q | |q.num ^ 2 - d * ↑q.den ^ 2| < M}.Infinite
m : ℤ
hm : {q | q.num ^ 2 - d * ↑q.den ^ 2 = m}.Infinite
this : NeZero m.natAbs
f : ℚ → ZMod m.natAbs × ZMod m.natAbs := fun q ↦ (↑q.num, ↑q.den)
q₁ : ℚ
h₁ : q₁.num ^ 2 - d * ↑q₁.den ^ 2 = m
q₂ : ℚ
h₂ : q₂.num ^ 2 - d * ↑q₂.den ^ 2 = m
hne : q₁ ≠ q₂
hqf : f q₁ = f q₂
hq1 : ↑q₁.num = ↑q₂.num
hq2 : ↑q₁.den = ↑q₂.den
hd₁ : m ∣ q₁.num * q₂.num - d * (↑q₁.den * ↑q₂.den)
hd₂ : m ∣ q₁.num * ↑q₂.den - q₂.num * ↑q₁.den
hm₀ : ↑m ≠ 0
⊢ (q₁.num * q₂.num - d * ↑q₁.den * ↑q₂.den) ^ 2 - d * (q₁.num * ↑q₂.den - q₂.num * ↑q₁.den) ^ 2 = m ^ 2

Tactic:
grind

Goal state after:
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✝¹ : DecidableEq K⟮X⟯
inst✝ : IsTrivialOn K v
hlt : 1 < v X
f : K⟮X⟯
hf : f ≠ 0
hlt' : 1 < (inftyValuation K) X
⊢ v X ^ f.intDegree < 1 ↔ (inftyValuation K) X ^ f.intDegree < 1

Tactic:
grind [one_le_zpow_iff_right₀]

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

Goal state before:
pp: K : Type u_1
Γ : Type u_2
inst✝¹ : Field K
inst✝ : LinearOrderedCommGroupWithZero Γ
v : Valuation K⟮X⟯ Γ
hne : {p | v ↑p < 1 ∧ p ≠ 0}.Nonempty
a b : K[X]
hab : v ↑(a * b) < 1 ∧ a ≠ 0 ∧ b ≠ 0
hb : ¬IsUnit b
πᵥ : K[X] := ⋯.min {p | v ↑p < 1 ∧ p ≠ 0} hne
hπᵥ : πᵥ = a * b
hda : a.degree < πᵥ.degree
hlea : a ∉ {p | v ↑p < 1 ∧ p ≠ 0}
⊢ 1 ≤ v ↑a

Tactic:
grind

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

Goal state before:
pp: case refine_1
K : Type u_1
Γ : Type u_2
inst✝² : Field K
inst✝¹ : LinearOrderedCommGroupWithZero Γ
v : Valuation K⟮X⟯ Γ
inst✝ : IsTrivialOn K v
hne : {p | v ↑p < 1 ∧ p ≠ 0}.Nonempty
πᵥ : K[X] := ⋯.min {p | v ↑p < 1 ∧ p ≠ 0} hne
a : K
hπᵥ : v ((algebraMap K K⟮X⟯) a) < 1 ∧ Polynomial.C a ≠ 0
ha0 : a ≠ 0
ha : Polynomial.C a = πᵥ
⊢ False

Tactic:
grind

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

Goal state before:
pp: case refine_2
K : Type u_1
Γ : Type u_2
inst✝² : Field K
inst✝¹ : LinearOrderedCommGroupWithZero Γ
v : Valuation K⟮X⟯ Γ
inst✝ : IsTrivialOn K v
hne : {p | v ↑p < 1 ∧ p ≠ 0}.Nonempty
πᵥ : K[X] := ⋯.min {p | v ↑p < 1 ∧ p ≠ 0} hne
a b : K[X]
H : ¬IsUnit a ∧ ¬IsUnit b
hva : 1 ≤ v ↑a
hab : πᵥ = b * a
this : 1 ≤ v ((algebraMap K[X] K⟮X⟯) b) * v ((algebraMap K[X] K⟮X⟯) a)
hπᵥ : v ((algebraMap K[X] K⟮X⟯) b) * v ((algebraMap K[X] K⟮X⟯) a) < 1 ∧ ¬b = 0 ∧ ¬a = 0
⊢ False

Tactic:
grind

Goal state after: