mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace

Goal state before:
pp: ι₁ : Type u_3
ι₂ : Type u_4
R₁ : ι₁ → Type u_5
R₂ : ι₂ → Type u_6
inst✝¹ : (i : ι₁) → TopologicalSpace (R₁ i)
inst✝ : (i : ι₂) → TopologicalSpace (R₂ i)
𝓕₁ : Filter ι₁
𝓕₂ : Filter ι₂
A₁ : (i : ι₁) → Set (R₁ i)
A₂ : (i : ι₂) → Set (R₂ i)
f : ι₂ → ι₁
hf : Tendsto f 𝓕₂ 𝓕₁
φ : (j : ι₂) → R₁ (f j) → R₂ j
hφ : ∀ᶠ (j : ι₂) in 𝓕₂, MapsTo (φ j) (A₁ (f j)) (A₂ j)
φ_cont : ∀ (j : ι₂), Continuous[inst✝¹ (f j), inst✝ j] (φ j)
⊢ ∀ (S : Set ι₁) (hS : 𝓕₁ ≤ 𝓟 S),
    Continuous[topologicalSpace R₁ A₁ (𝓟 S), topologicalSpace R₂ A₂ 𝓕₂] (mapAlong R₁ R₂ f hf φ hφ ∘ inclusion R₁ A₁ hS)

Tactic:
intro S hS

Goal state after:
ι₁ : Type u_3
ι₂ : Type u_4
R₁ : ι₁ → Type u_5
R₂ : ι₂ → Type u_6
inst✝¹ : (i : ι₁) → TopologicalSpace (R₁ i)
inst✝ : (i : ι₂) → TopologicalSpace (R₂ i)
𝓕₁ : Filter ι₁
𝓕₂ : Filter ι₂
A₁ : (i : ι₁) → Set (R₁ i)
A₂ : (i : ι₂) → Set (R₂ i)
f : ι₂ → ι₁
hf : Tendsto f 𝓕₂ 𝓕₁
φ : (j : ι₂) → R₁ (f j) → R₂ j
hφ : ∀ᶠ (j : ι₂) in 𝓕₂, MapsTo (φ j) (A₁ (f j)) (A₂ j)
φ_cont : ∀ (j : ι₂), Continuous[inst✝¹ (f j), inst✝ j] (φ j)
S : Set ι₁
hS : 𝓕₁ ≤ 𝓟 S
⊢ Continuous[topologicalSpace R₁ A₁ (𝓟 S), topologicalSpace R₂ A₂ 𝓕₂] (mapAlong R₁ R₂ f hf φ hφ ∘ inclusion R₁ A₁ hS)
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x y : mixedSpace K
hx : mixedEmbedding.norm x ≠ 0
hy : mixedEmbedding.norm y ≠ 0
⊢ logMap (x * y) = logMap x + logMap y

Tactic:
ext w
  simp_rw [Pi.add_apply, logMap_apply]
  rw [map_mul, map_mul, Real.log_mul, Real.log_mul hx hy, add_mul]
  · ring
  · exact mixedEmbedding.norm_ne_zero_iff.mp hx w
  · exact mixedEmbedding.norm_ne_zero_iff.mp hy w

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
A : Set (mixedSpace K)
inst✝ : NumberField K
hA : normAtComplexPlaces ⁻¹' normAtComplexPlaces '' A = A
hm : MeasurableSet A
hA' : ∀ {x : mixedSpace K}, A.indicator 1 x = (normAtComplexPlaces '' A).indicator 1 (normAtComplexPlaces x)
⊢ ∫⁻ (x : InfinitePlace K → ℝ) in Set.univ.pi fun w ↦ if w.IsReal then Set.univ else Set.Ioi 0,
      (∏ x_1, ENNReal.ofReal (x ↑x_1)) *
          (normAtComplexPlaces '' A).indicator 1 (normAtComplexPlaces (mixedSpaceOfRealSpace x)) *
        (volume.restrict (Set.univ.pi fun x ↦ Set.Ioo (-π) π)) Set.univ =
    ENNReal.ofReal (2 * π) ^ nrComplexPlaces K *
      ∫⁻ (x : realSpace K) in normAtComplexPlaces '' A, ∏ w, ENNReal.ofReal (x ↑w)

Tactic:
restrict_apply
      MeasurableSet.univ,

Goal state after:
K : Type u_1
inst✝¹ : Field K
A : Set (mixedSpace K)
inst✝ : NumberField K
hA : normAtComplexPlaces ⁻¹' normAtComplexPlaces '' A = A
hm : MeasurableSet A
hA' : ∀ {x : mixedSpace K}, A.indicator 1 x = (normAtComplexPlaces '' A).indicator 1 (normAtComplexPlaces x)
⊢ ∫⁻ (x : InfinitePlace K → ℝ) in Set.univ.pi fun w ↦ if w.IsReal then Set.univ else Set.Ioi 0,
      (∏ x_1, ENNReal.ofReal (x ↑x_1)) *
          (normAtComplexPlaces '' A).indicator 1 (normAtComplexPlaces (mixedSpaceOfRealSpace x)) *
        volume (Set.univ ∩ Set.univ.pi fun x ↦ Set.Ioo (-π) π) =
    ENNReal.ofReal (2 * π) ^ nrComplexPlaces K *
      ∫⁻ (x : realSpace K) in normAtComplexPlaces '' A, ∏ w, ENNReal.ofReal (x ↑w)
Module: Mathlib.NumberTheory.NumberField.CMField

Goal state before:
pp: K : Type u_1
inst✝³ : Field K
inst✝² : CharZero K
inst✝¹ : IsCMField K
inst✝ : Algebra.IsIntegral ℚ K
φ : K →+* ℂ
x : K
⊢ φ ((complexConj K) x) = (starRingEnd ℂ) (φ x)

Tactic:
IsConj.eq (isConj_complexConj K φ),

Goal state after:
K : Type u_1
inst✝³ : Field K
inst✝² : CharZero K
inst✝¹ : IsCMField K
inst✝ : Algebra.IsIntegral ℚ K
φ : K →+* ℂ
x : K
⊢ star (φ x) = (starRingEnd ℂ) (φ x)
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x y : mixedSpace K
c : ℝ
n : ℕ
x✝ : ↑(integerSet K)
⊢ ((Algebra.norm ℤ) ↑(preimageOfMemIntegerSet x✝)).natAbs = n ↔ absNorm (Ideal.span {↑(preimageOfMemIntegerSet x✝)}) = n

Tactic:
absNorm_span_singleton

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)ˣ
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
b✝ : InfinitePlace K
⊢ ¬b✝ = w' →
    (if h : b✝ = w' then ∑ x, ↑x.mult else ∑ x, ↑x.mult * Real.log (x ((algebraMap (𝓞 K) K) ↑(u (e ⟨b✝, ⋯⟩))))) = 0

Tactic:
h

Goal state after:
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
b✝ : InfinitePlace K
h : ¬b✝ = w'
⊢ (if h : b✝ = w' then ∑ x, ↑x.mult else ∑ x, ↑x.mult * Real.log (x ((algebraMap (𝓞 K) K) ↑(u (e ⟨b✝, ⋯⟩))))) = 0
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : realSpace K
⊢ ∏ x_1, (Real.exp (x w₀) * ∏ i, x_1 ((algebraMap (𝓞 K) K) ↑(fundSystem K (equivFinRank.symm i))) ^ x ↑i) ^ x_1.mult =
    Real.exp (x w₀) ^ finrank ℚ K

Tactic:
mul_pow,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : realSpace K
⊢ ∏ x_1,
      Real.exp (x w₀) ^ x_1.mult *
        (∏ i, x_1 ((algebraMap (𝓞 K) K) ↑(fundSystem K (equivFinRank.symm i))) ^ x ↑i) ^ x_1.mult =
    Real.exp (x w₀) ^ finrank ℚ K
Module: Mathlib.RingTheory.RootsOfUnity.CyclotomicUnits

Goal state before:
pp: case inr
p : ℕ
A : Type u_1
ζ : A
inst✝¹ : CommRing A
inst✝ : IsDomain A
hζ : IsPrimitiveRoot ζ p
hp : Nat.Prime p
η₁ : A
hη₁ : η₁ ∈ nthRootsFinset p 1
η₂ : A
hη₂ : η₂ ∈ nthRootsFinset p 1
h : η₁ ≠ η₂
⊢ ζ - 1 ∣ η₁ - η₂

Tactic:
· exact (hζ.nthRootsFinset_pairwise_associated_sub_one_sub_of_prime hp hη₁ hη₂ h).dvd

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
hI₁ : absNorm I ≠ 1
hI₂ : (absNorm I).Coprime (torsionOrder K)
x : (𝓞 K)ˣ
hx : x ∈ torsion K
y : (𝓞 K)ˣ
hy : y ∈ torsion K
⊢ I.torsionMapQuot ⟨x, hx⟩ = I.torsionMapQuot ⟨y, hy⟩ → ⟨x, hx⟩ = ⟨y, hy⟩

Tactic:
h

Goal state after:
K : Type u_1
inst✝¹ : Field K
I : Ideal (𝓞 K)
inst✝ : NumberField K
hI₁ : absNorm I ≠ 1
hI₂ : (absNorm I).Coprime (torsionOrder K)
x : (𝓞 K)ˣ
hx : x ∈ torsion K
y : (𝓞 K)ˣ
hy : y ∈ torsion K
h : I.torsionMapQuot ⟨x, hx⟩ = I.torsionMapQuot ⟨y, hy⟩
⊢ ⟨x, hx⟩ = ⟨y, hy⟩
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
⊢ (𝒑.primesOver (𝓞 K)).ncard = 1

Tactic:
have h_main := ncard_primesOver_mul_ramificationIdxIn_mul_inertiaDegIn 𝒑 (𝓞 K) Gal(K/ℚ)

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_main : (𝒑.primesOver (𝓞 K)).ncard * (𝒑.ramificationIdxIn (𝓞 K) * 𝒑.inertiaDegIn (𝓞 K)) = Nat.card Gal(K/ℚ)
⊢ (𝒑.primesOver (𝓞 K)).ncard = 1
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne

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

Tactic:
mul_pow,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ 2 ^ nrRealPlaces K * (ENNReal.ofReal 2 ^ nrComplexPlaces K * ENNReal.ofReal Real.pi ^ nrComplexPlaces K) *
      (2⁻¹ ^ nrComplexPlaces K * ENNReal.ofReal (regulator K) * ↑(finrank ℚ K) * (↑(finrank ℚ K))⁻¹) =
    2 ^ nrRealPlaces K * ↑NNReal.pi ^ nrComplexPlaces K * ENNReal.ofReal (regulator K)
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:
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.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
⊢ ∑ c, ↑(Nat.card { I // ↑(absNorm ↑I) ≤ s ∧ ClassGroup.mk0 I = c }) / s = ↑(Nat.card { I // ↑(absNorm ↑I) ≤ s }) / s

Tactic:
simp_rw [← Nat.card_congr (e _), Nat.card_eq_fintype_card, Fintype.subtype_card]

Goal state after:
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
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
x : ℝ
hx0 : 0 < x
hx1 : x < 1
hxM : x ≤ M
⊢ x ^ logb M (1 / 2) ≤ x ^ logb x (1 / 2)

Tactic:
apply rpow_le_rpow_of_exponent_ge hx0 hx1.le
      simp only [one_div, ← log_div_log, log_inv, neg_div, ← div_neg, hM]
      gcongr
      simp only [Left.neg_pos_iff]
      exact log_neg (lt_sup_iff.mpr <| .inl hp0) (sup_lt_iff.mpr ⟨hp1, hm⟩)

Goal state after:
Module: Mathlib.Topology.MetricSpace.Ultra.ContinuousMaps

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

Tactic:
h

Goal state after:
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)
⊢ dist f h ≤ max (dist f g) (dist g h)
Module: Mathlib.NumberTheory.Padics.WithVal

Goal state before:
pp: case h
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp0' : 0 < ↑p
hp0 : 0 < (↑p)⁻¹
hp1' : 1 < ↑p
hp1 : (↑p)⁻¹ < 1
n : ℕ
hn : Valued.v (↑p ^ n) = exp (-↑n)
x y : WithVal (Rat.padicValuation p)
⊢ Valued.v.restrict (y - x) < ↑(Units.mk0 (Valued.v.restrict (↑p ^ n)) ⋯) →
    ↑(padicNorm p ((WithVal.equiv (Rat.padicValuation p)) (x - y))) ≤ (↑p ^ n)⁻¹

Tactic:
h

Goal state after:
case h
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp0' : 0 < ↑p
hp0 : 0 < (↑p)⁻¹
hp1' : 1 < ↑p
hp1 : (↑p)⁻¹ < 1
n : ℕ
hn : Valued.v (↑p ^ n) = exp (-↑n)
x y : WithVal (Rat.padicValuation p)
h : Valued.v.restrict (y - x) < ↑(Units.mk0 (Valued.v.restrict (↑p ^ n)) ⋯)
⊢ ↑(padicNorm p ((WithVal.equiv (Rat.padicValuation p)) (x - y))) ≤ (↑p ^ n)⁻¹
Module: Mathlib.NumberTheory.Padics.WithVal

Goal state before:
pp: case right
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp0' : 0 < ↑p
hp0 : 0 < (↑p)⁻¹
hp1' : 1 < ↑p
hp1 : (↑p)⁻¹ < 1
⊢ ∀ (j : (MonoidWithZeroHom.ofClass Valued.v).ValueGroup₀ˣ),
    ∃ i,
      ∀ (x y : WithVal (Rat.padicValuation p)),
        ↑(padicNorm p ((WithVal.equiv (Rat.padicValuation p)) (x - y))) ≤ (↑p ^ i)⁻¹ → Valued.v.restrict (y - x) < ↑j

Tactic:
intro γ

Goal state after:
case right
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp0' : 0 < ↑p
hp0 : 0 < (↑p)⁻¹
hp1' : 1 < ↑p
hp1 : (↑p)⁻¹ < 1
γ : (MonoidWithZeroHom.ofClass Valued.v).ValueGroup₀ˣ
⊢ ∃ i,
    ∀ (x y : WithVal (Rat.padicValuation p)),
      ↑(padicNorm p ((WithVal.equiv (Rat.padicValuation p)) (x - y))) ≤ (↑p ^ i)⁻¹ → Valued.v.restrict (y - x) < ↑γ
Module: Mathlib.NumberTheory.Padics.WithVal

Goal state before:
pp: case h
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp0' : 0 < ↑p
hp0 : 0 < (↑p)⁻¹
hp1' : 1 < ↑p
hp1 : (↑p)⁻¹ < 1
γ : (MonoidWithZeroHom.ofClass Valued.v).ValueGroup₀ˣ
x y : WithVal (Rat.padicValuation p)
⊢ ↑(padicNorm p ((WithVal.equiv (Rat.padicValuation p)) (x - y))) ≤ (↑p ^ (embedding ↑γ * exp (-1)).log.natAbs)⁻¹ →
    Valued.v.restrict (y - x) < ↑γ

Tactic:
h

Goal state after:
case h
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp0' : 0 < ↑p
hp0 : 0 < (↑p)⁻¹
hp1' : 1 < ↑p
hp1 : (↑p)⁻¹ < 1
γ : (MonoidWithZeroHom.ofClass Valued.v).ValueGroup₀ˣ
x y : WithVal (Rat.padicValuation p)
h : ↑(padicNorm p ((WithVal.equiv (Rat.padicValuation p)) (x - y))) ≤ (↑p ^ (embedding ↑γ * exp (-1)).log.natAbs)⁻¹
⊢ Valued.v.restrict (y - x) < ↑γ
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✝⁵ : CompactSpace X
inst✝⁴ : CompactSpace Y
inst✝³ : T2Space X
inst✝² : T2Space Y
inst✝¹ : TotallyDisconnectedSpace X
inst✝ : T0Space R
h : TensorProduct R C(X, R) C(Y, R)
⊢ (⇑((prodMk μ) ν) ∘ ⇑tensorHom) h = (⇑((prodMk' μ) ν) ∘ ⇑tensorHom) h

Tactic:
induction h with

Goal state after:
Module: Mathlib.NumberTheory.Pell

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

pp: case negSucc
d : ℤ
a : Solution₁ d
hax : 0 < a.x
hay : 0 < a.y
n : ℕ
⊢ (a ^ Int.negSucc n).y.sign = (Int.negSucc n).sign

Tactic:
· rw [Int.ofNat_eq_natCast, zpow_natCast]
    exact Int.sign_eq_one_of_pos (y_pow_succ_pos hax hay n)

Goal state after:
case negSucc
d : ℤ
a : Solution₁ d
hax : 0 < a.x
hay : 0 < a.y
n : ℕ
⊢ (a ^ Int.negSucc n).y.sign = (Int.negSucc n).sign
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 : ℚ
a : ℤ
hq : (↑q.den * a) ^ 2 = ↑q.den ^ 2 * d
ha : q.num = ↑q.den * a
⊢ False

Tactic:
mul_pow,

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 : ℚ
a : ℤ
hq : ↑q.den ^ 2 * a ^ 2 = ↑q.den ^ 2 * d
ha : q.num = ↑q.den * a
⊢ False
Module: Mathlib.NumberTheory.RamificationInertia.Basic

Goal state before:
pp: case h
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 • ⊤ = ⊤
x : S ⧸ M
a'' : Fin n →₀ R
ha'' : ∀ (i : Fin n), a'' i ∈ p
hx : (a''.sum fun i c ↦ c • a i) = x
⊢ ∀ (i : Fin n), 0 • a i = 0

Tactic:
exact fun _ => zero_smul _ _

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 * a₁.y) ^ 2 ≤ (a.y * a₁.x) ^ 2

Tactic:
mul_pow,

Goal state after:
d : ℤ
a₁ : Solution₁ d
h : IsFundamental a₁
a : Solution₁ d
hax : 1 < a.x
hay : 0 < a.y
⊢ a.x ^ 2 * a₁.y ^ 2 ≤ (a.y * a₁.x) ^ 2
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 ^ 2 * a₁.y ^ 2 ≤ (a.y * a₁.x) ^ 2

Tactic:
mul_pow,

Goal state after:
d : ℤ
a₁ : Solution₁ d
h : IsFundamental a₁
a : Solution₁ d
hax : 1 < a.x
hay : 0 < a.y
⊢ a.x ^ 2 * a₁.y ^ 2 ≤ a.y ^ 2 * a₁.x ^ 2
Module: Mathlib.NumberTheory.Pell

Goal state before:
pp: case calc.step
d : ℤ
a₁ : Solution₁ d
h : IsFundamental a₁
a : Solution₁ d
hax : 1 < a.x
hay : 0 < a.y
⊢ a.y - a.x * a₁.y < 0

Tactic:
sub_neg,

Goal state after:
case calc.step
d : ℤ
a₁ : Solution₁ d
h : IsFundamental a₁
a : Solution₁ d
hax : 1 < a.x
hay : 0 < a.y
⊢ a.y < a.x * a₁.y
Module: Mathlib.NumberTheory.Pell

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

Tactic:
mul_pow,

Goal state after:
case calc.step
d : ℤ
a₁ : Solution₁ d
h : IsFundamental a₁
a : Solution₁ d
hax : 1 < a.x
hay : 0 < a.y
⊢ a.y ^ 2 < a.x ^ 2 * a₁.y ^ 2
Module: Mathlib.NumberTheory.Padics.Hensel

Goal state before:
pp: case hf
p : ℕ
inst✝² : Fact (Nat.Prime p)
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Algebra R ℤ_[p]
F : Polynomial R
a : ℤ_[p]
hnorm : ‖(Polynomial.aeval a) F‖ < ‖(Polynomial.aeval a) (Polynomial.derivative F)‖ ^ 2
⊢ Tendsto (fun x ↦ ‖(Polynomial.aeval a) (Polynomial.derivative F)‖) atTop
    (𝓝 ‖(Polynomial.aeval a) (Polynomial.derivative F)‖)

Tactic:
apply tendsto_const_nhds

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⟯ Γ
inst✝¹ : v.IsNontrivial
inst✝ : IsTrivialOn K v
hle : v X ≤ 1
p : K[X]
hp : p ≠ 0
π : K[X] := πᵥ
hne : {p | v ↑p < 1 ∧ p ≠ 0}.Nonempty
hπirr : Irreducible π
k : ℕ
q : K[X]
hnq : ¬π ∣ q
heq : p = π ^ k * q
hπ : v ↑π < 1 ∧ ¬π = 0
⊢ v ((algebraMap K[X] K⟮X⟯) p) = v (↑π ^ (Associates.mk Pᵥ.asIdeal).count (Associates.mk (Ideal.span {p})).factors)

Tactic:
heq

Goal state after:
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
p : K[X]
hp : p ≠ 0
π : K[X] := πᵥ
hne : {p | v ↑p < 1 ∧ p ≠ 0}.Nonempty
hπirr : Irreducible π
k : ℕ
q : K[X]
hnq : ¬π ∣ q
heq : p = π ^ k * q
hπ : v ↑π < 1 ∧ ¬π = 0
⊢ v ((algebraMap K[X] K⟮X⟯) (π ^ k * q)) =
    v (↑π ^ (Associates.mk Pᵥ.asIdeal).count (Associates.mk (Ideal.span {p})).factors)
Module: Mathlib.NumberTheory.Rayleigh

Goal state before:
pp: case a
r s : ℝ
hrs : r.HolderConjugate s
j : ℤ
hj : 0 < j
hb₁ : ∀ s ≥ 0, j ∈ {x | ∃ k > 0, beattySeq s k = x} ↔ j ∈ {x | ∃ k, beattySeq s k = x}
hb₂ : ∀ s ≥ 0, j ∈ {x | ∃ k > 0, beattySeq' s k = x} ↔ j ∈ {x | ∃ k, beattySeq' s k = x}
⊢ j ∈ {x | ∃ k, beattySeq r k = x} ∧ j ∉ {x | ∃ k, beattySeq r k = x}ᶜ ∨
    j ∈ {x | ∃ k, beattySeq r k = x}ᶜ ∧ j ∉ {x | ∃ k, beattySeq r k = x}

Tactic:
Set.notMem_compl_iff,

Goal state after:
case a
r s : ℝ
hrs : r.HolderConjugate s
j : ℤ
hj : 0 < j
hb₁ : ∀ s ≥ 0, j ∈ {x | ∃ k > 0, beattySeq s k = x} ↔ j ∈ {x | ∃ k, beattySeq s k = x}
hb₂ : ∀ s ≥ 0, j ∈ {x | ∃ k > 0, beattySeq' s k = x} ↔ j ∈ {x | ∃ k, beattySeq' s k = x}
⊢ j ∈ {x | ∃ k, beattySeq r k = x} ∧ j ∈ {x | ∃ k, beattySeq r k = x} ∨
    j ∈ {x | ∃ k, beattySeq r k = x}ᶜ ∧ j ∉ {x | ∃ k, beattySeq r k = x}
Module: Mathlib.NumberTheory.RatFunc.Ostrowski

Goal state before:
pp: case hH.refine_2
K : Type u_1
Γ : Type u_2
inst✝³ : Field K
inst✝² : LinearOrderedCommGroupWithZero Γ
v : Valuation K⟮X⟯ Γ
inst✝¹ : v.IsNontrivial
inst✝ : IsTrivialOn K v
hle : v X ≤ 1
hv : v.IsRankOneDiscrete
h0 : v ↑πᵥ ≠ 0
γ : Γˣ
x✝ : ∃ a, ¬a = 0 ∧ ∃ x, (MonoidWithZeroHom.ofClass v) a * ↑γ = (MonoidWithZeroHom.ofClass v) x
a : K⟮X⟯
ha : ¬a = 0
b : K⟮X⟯
hab : (MonoidWithZeroHom.ofClass v) a * ↑γ = (MonoidWithZeroHom.ofClass v) b
⊢ ∃ k, ⋯.unit ^ k = γ

Tactic:
obtain ⟨ka, hka⟩ := exists_zpow_uniformizingPolynomial hle ha

Goal state after:
case hH.refine_2
K : Type u_1
Γ : Type u_2
inst✝³ : Field K
inst✝² : LinearOrderedCommGroupWithZero Γ
v : Valuation K⟮X⟯ Γ
inst✝¹ : v.IsNontrivial
inst✝ : IsTrivialOn K v
hle : v X ≤ 1
hv : v.IsRankOneDiscrete
h0 : v ↑πᵥ ≠ 0
γ : Γˣ
x✝ : ∃ a, ¬a = 0 ∧ ∃ x, (MonoidWithZeroHom.ofClass v) a * ↑γ = (MonoidWithZeroHom.ofClass v) x
a : K⟮X⟯
ha : ¬a = 0
b : K⟮X⟯
hab : (MonoidWithZeroHom.ofClass v) a * ↑γ = (MonoidWithZeroHom.ofClass v) b
ka : ℤ
hka : v a = v ↑πᵥ ^ ka
⊢ ∃ k, ⋯.unit ^ k = γ
Module: Mathlib.NumberTheory.SumFourSquares

Goal state before:
pp: m x y : ℤ
h : 2 * m = x ^ 2 + y ^ 2
⊢ Even (x ^ 2 + y ^ 2)

Tactic:
by simp [← h]

Goal state after:
Module: Mathlib.NumberTheory.SumFourSquares

Goal state before:
pp: m x y : ℤ
h : 2 * m = x ^ 2 + y ^ 2
this : Even (x ^ 2 + y ^ 2)
⊢ 2 * (2 * m) = (x - y) ^ 2 + (x + y) ^ 2

Tactic:
h

Goal state after:
m x y : ℤ
h : 2 * m = x ^ 2 + y ^ 2
this : Even (x ^ 2 + y ^ 2)
⊢ 2 * (x ^ 2 + y ^ 2) = (x - y) ^ 2 + (x + y) ^ 2
Module: Mathlib.NumberTheory.RatFunc.Ostrowski

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : DecidableEq K⟮X⟯
p : HeightOneSpectrum K[X]
⊢ ¬(valuation K⟮X⟯ p).IsEquiv (inftyValuation K)

Tactic:
simp only [isEquiv_iff_val_le_one]

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : DecidableEq K⟮X⟯
p : HeightOneSpectrum K[X]
⊢ ¬∀ {x : K⟮X⟯}, (valuation K⟮X⟯ p) x ≤ 1 ↔ (inftyValuation K) x ≤ 1
Module: Mathlib.NumberTheory.Zsqrtd.GaussianInt

Goal state before:
pp: x : ℤ[i]
⊢ toComplex x = { re := ↑x.re, im := ↑x.im }

Tactic:
apply Complex.ext <;> simp [toComplex_def]

Goal state after:
Module: Mathlib.NumberTheory.SumTwoSquares

Goal state before:
pp: n a b : ℕ
h₁ : n = a ^ 2 * b
h₂ : IsSquare (-1)
x' y' : ℕ
h : b = x' ^ 2 + y' ^ 2
⊢ a ^ 2 * b = (a * x') ^ 2 + (a * y') ^ 2

Tactic:
h

Goal state after:
n a b : ℕ
h₁ : n = a ^ 2 * b
h₂ : IsSquare (-1)
x' y' : ℕ
h : b = x' ^ 2 + y' ^ 2
⊢ a ^ 2 * (x' ^ 2 + y' ^ 2) = (a * x') ^ 2 + (a * y') ^ 2
Module: Mathlib.NumberTheory.SumFourSquares

Goal state before:
pp: case neg.inl
p : ℕ
hp : Prime p
this✝ : Fact (Prime p)
natAbs_iff :
  ∀ {a b c d : ℤ} {k : ℕ},
    a.natAbs ^ 2 + b.natAbs ^ 2 + c.natAbs ^ 2 + d.natAbs ^ 2 = k ↔ a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = ↑k
hm✝ : ∃ m < p, 0 < m ∧ ∃ a b c d, a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = m * p
m : ℕ
hmin : ∀ m_1 < m, ¬(m_1 < p ∧ 0 < m_1 ∧ ∃ a b c d, a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = m_1 * p)
hmp : m < p
hm₀ : 0 < m
a b c d : ℕ
habcd : a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = m * p
hm₁ : 1 < m
this : NeZero m
hm : ¬2 ∣ m
f : ℕ → ℤ
hf_lt : ∀ (x : ℕ), 2 * (f x).natAbs < m
hf_mod : ∀ (x : ℕ), ↑(f x) = ↑x
hr : (f a).natAbs ^ 2 + (f b).natAbs ^ 2 + (f c).natAbs ^ 2 + (f d).natAbs ^ 2 = m * 0
⊢ False

Tactic:
replace hr : f a = 0 ∧ f b = 0 ∧ f c = 0 ∧ f d = 0 := by simpa [and_assoc] using hr

Goal state after:
case neg.inl
p : ℕ
hp : Prime p
this✝ : Fact (Prime p)
natAbs_iff :
  ∀ {a b c d : ℤ} {k : ℕ},
    a.natAbs ^ 2 + b.natAbs ^ 2 + c.natAbs ^ 2 + d.natAbs ^ 2 = k ↔ a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = ↑k
hm✝ : ∃ m < p, 0 < m ∧ ∃ a b c d, a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = m * p
m : ℕ
hmin : ∀ m_1 < m, ¬(m_1 < p ∧ 0 < m_1 ∧ ∃ a b c d, a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = m_1 * p)
hmp : m < p
hm₀ : 0 < m
a b c d : ℕ
habcd : a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = m * p
hm₁ : 1 < m
this : NeZero m
hm : ¬2 ∣ m
f : ℕ → ℤ
hf_lt : ∀ (x : ℕ), 2 * (f x).natAbs < m
hf_mod : ∀ (x : ℕ), ↑(f x) = ↑x
hr : f a = 0 ∧ f b = 0 ∧ f c = 0 ∧ f d = 0
⊢ False