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

Goal state before:
pp: v : InfinitePlace ℚ
x : ℚ
⊢ v ((WithAbs.equiv ↑v) ((WithAbs.equiv ↑v).symm x)) = ↑|(WithAbs.equiv ↑v) ((WithAbs.equiv ↑v).symm x)|

Tactic:
(WithAbs.equiv v.1).apply_symm_apply,

Goal state after:
v : InfinitePlace ℚ
x : ℚ
⊢ v x = ↑|x|
Module: Mathlib.NumberTheory.NumberField.Completion.InfinitePlace

Goal state before:
pp: K : Type u_1
inst✝² : Field K
v : InfinitePlace K
L : Type u_2
inst✝¹ : Field L
inst✝ : Algebra K L
w : InfinitePlace L
x : WithAbs ↑v
⊢ (algebraMap (WithAbs ↑v) (↑w).Completion) x =
    { toCompletion := ↑((algebraMap (WithAbs ↑v) (WithAbs ↑w)) x) }.toCompletion

Tactic:
exact UniformSpace.Completion.algebraMap_def (WithAbs w.1) (WithAbs v.1) x

Goal state after:
Module: Mathlib.RingTheory.DedekindDomain.FiniteAdeleRing

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
a : 𝔸ᶠ[R, K]
⊢ IsUnit a ↔
    (∀ (v : HeightOneSpectrum R), a v ≠ 0) ∧ ∀ᶠ (v : HeightOneSpectrum R) in Filter.cofinite, Valued.v (a v) = 1

Tactic:
rw [RestrictedProduct.isUnit_iff]
  simp only [isUnit_iff_ne_zero, adicCompletionIntegers.isUnit_iff_valued_eq_one, exists_prop,
    Filter.eventually_cofinite, not_and_or, Set.ofPred_or]
  simpa using! fun _ _ ↦ a.2

Goal state after:
Module: Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace

Goal state before:
pp: case pos
ι : Type u_1
R : ι → Type u_2
A : (i : ι) → Set (R i)
inst✝ : (i : ι) → TopologicalSpace (R i)
hAopen : ∀ (i : ι), IsOpen[inst✝ i] (A i)
S : Set ι
hS : S ∈ cofinite
p : ι → Prop
f : Πʳ (i : ι), [R i, A i]_[𝓟 S]
H : f ∈ DFunLike.coe ⁻¹' (Sᶜ ∩ {i | p i}).pi A
i : ι
hiT : p i
hiS : i ∈ S
⊢ ↑f i ∈ A i

Tactic:
exact f.2 hiS

Goal state after:
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
T : Set ι₂ := f ⁻¹' S ∩ {j | MapsTo (φ j) (A₁ (f j)) (A₂ j)}
⊢ 𝓕₂ ≤ 𝓟 T

Tactic:
rw [le_principal_iff] at 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 ∈ 𝓕₁
T : Set ι₂ := f ⁻¹' S ∩ {j | MapsTo (φ j) (A₁ (f j)) (A₂ j)}
⊢ T ∈ 𝓕₂
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
w : InfinitePlace K
x : K
⊢ ‖w.embedding ((complexConj K) x)‖ = w x

Tactic:
complexEmbedding_complexConj,

Goal state after:
K : Type u_1
inst✝³ : Field K
inst✝² : CharZero K
inst✝¹ : IsCMField K
inst✝ : Algebra.IsIntegral ℚ K
w : InfinitePlace K
x : K
⊢ ‖(starRingEnd ℂ) (w.embedding x)‖ = w x
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
b✝ : Associates ↥(𝓞 K)⁰
x : ↥(𝓞 K)⁰
⊢ ∃ u, u • (mixedEmbedding K) ↑↑x ∈ integerSet K

Tactic:
refine exists_unitSMul_mem_integerSet ?_ ⟨(x : 𝓞 K), Set.mem_range_self _, rfl⟩

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
b✝ : Associates ↥(𝓞 K)⁰
x : ↥(𝓞 K)⁰
⊢ (mixedEmbedding K) ↑↑x ≠ 0
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
ζ : ↥(torsion K)
φ : K →+* ℂ := ⋯
⊢ φ ((complexConj K) ((algebraMap (𝓞 K) K) ↑↑ζ)) = φ ((algebraMap (𝓞 K) K) ↑↑ζ)⁻¹

Tactic:
complexEmbedding_complexConj,

Goal state after:
K : Type u_1
inst✝³ : Field K
inst✝² : CharZero K
inst✝¹ : IsCMField K
inst✝ : NumberField K
ζ : ↥(torsion K)
φ : K →+* ℂ := Classical.choice ⋯
⊢ (starRingEnd ℂ) (φ ((algebraMap (𝓞 K) K) ↑↑ζ)) = φ ((algebraMap (𝓞 K) K) ↑↑ζ)⁻¹
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 ((Algebra.norm ℤ) (hζ✝.toInteger - 1)) ↑p

Tactic:
hζ.norm_toInteger_sub_one_of_eq_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) ↑p
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
⊢ 𝒑.ramificationIdxIn (𝓞 K) = p ^ k * (p - 1)

Tactic:
rw [ramificationIdxIn_eq_ramificationIdx 𝒑 (span {hK.zeta_spec.toInteger - 1}) Gal(K/ℚ),
    ramificationIdx_span_zeta_sub_one]

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))
⊢ 0 ≤ dirichletDensity S

Tactic:
rw [dirichletDensity]
  split_ifs with h
  · exact h.choose_spec.nonneg
  · exact le_rfl

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
⊢ ¬(fun k l ↦ ((newBasis K).repr (a k.1 l.1 * (newBasis K) l.2)) k.2) = 0

Tactic:
funext_iff

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
⊢ ¬∀ (x : α × (K →+* ℂ)), (fun l ↦ ((newBasis K).repr (a x.1 l.1 * (newBasis K) l.2)) x.2) = 0 x
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
k' : α
l : β
b b' : K →+* ℂ
hs : (fun l ↦ ((newBasis K).repr (a k' l.1 * (newBasis K) l.2)) b') = 0 (k', b')
⊢ ((newBasis K).repr (a k' l * (newBasis K) b)) b' = 0 b'

Tactic:
funext_iff

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
k' : α
l : β
b b' : K →+* ℂ
hs : ∀ (x : β × (K →+* ℂ)), ((newBasis K).repr (a k' x.1 * (newBasis K) x.2)) b' = 0 (k', b') x
⊢ ((newBasis K).repr (a k' l * (newBasis K) b)) b' = 0 b'
Module: Mathlib.NumberTheory.NumberField.House

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
β : Type u_3
x : β × (K →+* ℂ) → ℤ
hxl : x ≠ 0
H : ξ K x = 0
l : β
r : K →+* ℂ
⊢ x (l, r) = 0 (l, r)

Tactic:
funext_iff

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
β : Type u_3
x : β × (K →+* ℂ) → ℤ
hxl : x ≠ 0
H : ∀ (x_1 : β), ξ K x x_1 = 0 x_1
l : β
r : K →+* ℂ
⊢ x (l, r) = 0 (l, r)
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)
x : β × (K →+* ℂ) → ℤ
hxl : x ≠ 0
inst✝ : Fintype β
hmulvec0 : asiegel K a *ᵥ x = 0
k : α
u : K →+* ℂ
l : β
hξ : ¬ξ K x l = 0 l
⊢ ∑ r, ∑ l, ↑(a' K a k l r u) * ↑(x (l, r)) = 0

Tactic:
funext_iff

Goal state after:
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 : ∀ (x_1 : α × (K →+* ℂ)), (asiegel K a *ᵥ x) x_1 = 0 x_1
k : α
u : K →+* ℂ
l : β
hξ : ¬ξ K x l = 0 l
⊢ ∑ r, ∑ l, ↑(a' K a k l r u) * ↑(x (l, r)) = 0
Module: Mathlib.NumberTheory.SiegelsLemma

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : Fintype α
inst✝¹ : Fintype β
A : Matrix α β ℤ
inst✝ : DecidableEq β
⊢ #T = (B + 1) ^ n

Tactic:
Pi.card_Icc 0 B'

Goal state after:
α : Type u_1
β : Type u_2
inst✝² : Fintype α
inst✝¹ : Fintype β
A : Matrix α β ℤ
inst✝ : DecidableEq β
⊢ ∏ i, #(Icc (0 i) ↑B) = (B + 1) ^ n
Module: Mathlib.NumberTheory.NumberField.Ideal.Asymptotics

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
C : ClassGroup (𝓞 K)
⊢ Tendsto (fun s ↦ ↑(Nat.card { I // ↑(absNorm ↑I) ≤ s ∧ ClassGroup.mk0 I = C }) / s) atTop
    (𝓝 (2 ^ nrRealPlaces K * (2 * π) ^ nrComplexPlaces K * regulator K / (↑(torsionOrder K) * √|↑(discr K)|)))

Tactic:
classical
  have h₁ : ∀ s : ℝ,
    {x | x ∈ toMixed K ⁻¹' fundamentalCone K ∧ mixedEmbedding.norm (toMixed K x) ≤ s} =
      toMixed K ⁻¹' {x | x ∈ fundamentalCone K ∧ mixedEmbedding.norm x ≤ s} := fun _ ↦ rfl
  have h₂ : {x | x ∈ fundamentalCone K ∧ mixedEmbedding.norm x ≤ 1} = normLeOne K := by ext; simp
  obtain ⟨J, hJ⟩ := ClassGroup.mk0_surjective C⁻¹
  have h₃ : (absNorm J.1 : ℝ) ≠ 0 := (Nat.cast_ne_zero.mpr (absNorm_ne_zero_of_nonZeroDivisors J))
  convert!
    ((ZLattice.covolume.tendsto_card_le_div'
              (ZLattice.comap ℝ (mixedEmbedding.idealLattice K (FractionalIdeal.mk0 K J))
                (toMixed K).toLinearMap)
              (F := fun x ↦ mixedEmbedding.norm (toMixed K x)) (X :=
              (toMixed K) ⁻¹' (fundamentalCone K)) (fun _ _ _ h ↦ ?_) (fun _ _ h ↦ ?_)
              ((toMixed K).antilipschitz.isBounded_preimage (isBounded_normLeOne K)) ?_ ?_).mul
          (tendsto_const_nhds (x := (absNorm (J : Ideal (𝓞 K)) : ℝ) * (torsionOrder K : ℝ)⁻¹))).comp
      (tendsto_id.atTop_mul_const' <| Nat.cast_pos.mpr (absNorm_pos_of_nonZeroDivisors J)) using
    2 with s
  · simp_rw [Ideal.tendsto_norm_le_and_mk_eq_div_atTop_aux₁ K hJ, id_eq,
      Nat.card_congr (Ideal.tendsto_norm_le_and_mk_eq_div_atTop_aux₂ K),
      ← card_isPrincipal_dvd_norm_le, Function.comp_def, Nat.cast_mul, div_eq_mul_inv, mul_inv,
      ← mul_assoc, mul_comm _ (torsionOrder K : ℝ)⁻¹, mul_comm _ (torsionOrder K : ℝ), mul_assoc]
    rw [inv_mul_cancel_left₀ (Nat.cast_ne_zero.mpr (torsionOrder_ne_zero K)), inv_mul_cancel₀ h₃,
      mul_one]
  · rw [h₁, h₂, MeasureTheory.measureReal_def, (volumePreserving_toMixed K).measure_preimage
      (measurableSet_normLeOne K).nullMeasurableSet, volume_normLeOne, ZLattice.covolume_comap
      _ _ _ (volumePreserving_toMixed K), covolume_idealLattice, ENNReal.toReal_mul,
      ENNReal.toReal_mul, ENNReal.toReal_pow, ENNReal.toReal_pow, ENNReal.toReal_ofNat,
      ENNReal.coe_toReal, NNReal.coe_real_pi, ENNReal.toReal_ofReal (regulator_pos K).le,
      FractionalIdeal.coe_mk0, FractionalIdeal.coeIdeal_absNorm, Rat.cast_natCast, div_eq_mul_inv,
      div_eq_mul_inv, mul_inv, mul_inv, mul_inv, inv_pow, inv_inv]
    ring_nf
    rw [mul_inv_cancel_right₀ h₃]
  · rwa [Set.mem_preimage, map_smul, smul_mem_iff_mem h.ne']
  · rw [map_smul, mixedEmbedding.norm_smul, euclidean.finrank, abs_of_nonneg h]
  · exact (toMixed K).continuous.measurable (measurableSet_normLeOne K)
  · rw [h₁, ← (toMixed K).coe_toHomeomorph, ← Homeomorph.preimage_frontier,
      (toMixed K).coe_toHomeomorph, (volumePreserving_toMixed K).measure_preimage
      measurableSet_frontier.nullMeasurableSet, h₂, volume_frontier_normLeOne]

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
hm₀ : 0 < f ↑m
⊢ 1 * f ↑p ^ k + 1 * f ↑m ^ k < 1

Tactic:
linarith only [le_half hp0 hp1 le_sup_left, le_half hm₀ hm le_sup_right]

Goal state after:
Module: Mathlib.NumberTheory.SiegelsLemma

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : Fintype β
A : Matrix α β ℤ
hn : m < n
hm : 0 < m
x : β → ℤ
hxT : x ∈ T
y : β → ℤ
hyT : y ∈ T
hneq : x ≠ y
hfeq : A *ᵥ x = A *ᵥ y
n_mul_norm_A_pow_e_nonneg : 0 ≤ (↑n * max 1 ‖A‖) ^ e
i : β
j : Unit
⊢ ‖x i - y i‖ ≤ (↑n * max 1 ‖A‖) ^ e

Tactic:
Int.norm_eq_abs,

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : Fintype β
A : Matrix α β ℤ
hn : m < n
hm : 0 < m
x : β → ℤ
hxT : x ∈ T
y : β → ℤ
hyT : y ∈ T
hneq : x ≠ y
hfeq : A *ᵥ x = A *ᵥ y
n_mul_norm_A_pow_e_nonneg : 0 ≤ (↑n * max 1 ‖A‖) ^ e
i : β
j : Unit
⊢ |↑(x i - y i)| ≤ (↑n * max 1 ‖A‖) ^ e
Module: Mathlib.NumberTheory.Ostrowski

Goal state before:
pp: f : AbsoluteValue ℚ ℝ
n₀ : ℕ
hn₀ : 1 < n₀
h : f ↑n₀ ≤ 1
n m : ℕ
hm : 1 ≤ m
L : List ℕ := n₀.digits m
⊢ (List.mapIdx (fun i x ↦ ↑n₀ * f ↑n₀ ^ i) L).sum ≤ (List.mapIdx (fun x x_1 ↦ ↑n₀) L).sum

Tactic:
simp only [List.mapIdx_eq_zipIdx_map]

Goal state after:
f : AbsoluteValue ℚ ℝ
n₀ : ℕ
hn₀ : 1 < n₀
h : f ↑n₀ ≤ 1
n m : ℕ
hm : 1 ≤ m
L : List ℕ := n₀.digits m
⊢ (List.map (fun x ↦ ↑n₀ * f ↑n₀ ^ x.2) L.zipIdx).sum ≤ (List.map (fun x ↦ ↑n₀) L.zipIdx).sum
Module: Mathlib.NumberTheory.Ostrowski

Goal state before:
pp: f : AbsoluteValue ℚ ℝ
n₀ : ℕ
hn₀ : 1 < n₀
h : f ↑n₀ ≤ 1
n : ℕ
h_ineq1 : ∀ {m : ℕ}, 1 ≤ m → f ↑m ≤ ↑n₀ * (logb ↑n₀ ↑m + 1)
h₀ : n ≠ 0
k : ℕ
hk : 0 < k
this : 0 ≤ logb ↑n₀ ↑n
⊢ (↑n₀ * (↑k * logb ↑n₀ ↑n + 1)) ^ (↑k)⁻¹ ≤ (↑n₀ * (↑k * logb ↑n₀ ↑n + ↑k)) ^ (↑k)⁻¹

Tactic:
gcongr
      exact one_le_cast.mpr hk

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) - 1) / (f ↑m - 1)) ≤ ↑m * (f ↑m ^ (d + 1) / (f ↑m - 1))

Tactic:
gcongr; linarith

Goal state after:
Module: Mathlib.NumberTheory.Ostrowski

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
c : ℝ
hc₀ : 0 < c
hc : (fun x ↦ real x ^ c) 2 = (padic p) 2
⊢ False

Tactic:
simp only [real_eq_abs, abs_ofNat, cast_ofNat] at hc

Goal state after:
p : ℕ
inst✝ : Fact (Nat.Prime p)
c : ℝ
hc₀ : 0 < c
hc : 2 ^ c = (padic p) 2
⊢ False
Module: Mathlib.NumberTheory.PowModTotient

Goal state before:
pp: x k n : ℕ
hn : 1 < n
h : x.Coprime n
⊢ x ^ k % n = x ^ (k % φ n) % n

Tactic:
← div_add_mod' k (φ n),

Goal state after:
x k n : ℕ
hn : 1 < n
h : x.Coprime n
⊢ x ^ (k / φ n * φ n + k % φ n) % n = x ^ ((k / φ n * φ n + k % φ n) % φ n) % n
Module: Mathlib.NumberTheory.Pell

Goal state before:
pp: d : ℤ
h₀ : 0 ≤ d
a : Solution₁ d
hx : a.x = 0
⊢ False

Tactic:
have h : 0 ≤ d * a.y ^ 2 := mul_nonneg h₀ (sq_nonneg _)

Goal state after:
d : ℤ
h₀ : 0 ≤ d
a : Solution₁ d
hx : a.x = 0
h : 0 ≤ d * a.y ^ 2
⊢ False
Module: Mathlib.NumberTheory.Pell

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

Tactic:
← zpow_zero a

Goal state after:
d : ℤ
a : Solution₁ d
h : IsFundamental a
n : ℤ
⊢ a ^ n = a ^ 0 ↔ n = 0
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 • ∑ j, A k j • a j = 0

Tactic:
rw [A_smul, smul_zero]

Goal state after:
Module: Mathlib.NumberTheory.Pell

Goal state before:
pp: case inr.inr.inr
d : ℤ
a₁ : Solution₁ d
h : IsFundamental a₁
a b : Solution₁ d
hbx : 0 < b.x
hby : 0 ≤ b.y
n : ℕ
hn : b = a₁ ^ n
hb : a = -b⁻¹
⊢ ∃ n, a = a₁ ^ n ∨ a = -a₁ ^ n

Tactic:
rw [hb]

Goal state after:
case inr.inr.inr
d : ℤ
a₁ : Solution₁ d
h : IsFundamental a₁
a b : Solution₁ d
hbx : 0 < b.x
hby : 0 ≤ b.y
n : ℕ
hn : b = a₁ ^ n
hb : a = -b⁻¹
⊢ ∃ n, -b⁻¹ = a₁ ^ n ∨ -b⁻¹ = -a₁ ^ n
Module: Mathlib.NumberTheory.Padics.Hensel

Goal state before:
pp: 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
n : ℕ
⊢ ‖(Polynomial.aeval (newton_seq n)) F‖ / ‖(Polynomial.aeval a) (Polynomial.derivative F)‖ ≤
    ‖(Polynomial.aeval a) (Polynomial.derivative F)‖ ^ 2 * T_gen p F a ^ 2 ^ n /
      ‖(Polynomial.aeval a) (Polynomial.derivative F)‖

Tactic:
gcongr
      apply newton_seq_norm_le

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

Goal state before:
pp: 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 n ↦ ‖(Polynomial.aeval a) (Polynomial.derivative F)‖ * T_gen p F a ^ 2 ^ n) atTop
    (𝓝 (‖(Polynomial.aeval a) (Polynomial.derivative F)‖ * 0))

Tactic:
exact
    tendsto_const_nhds.mul
      (Tendsto.comp (tendsto_pow_atTop_nhds_zero_of_lt_one (norm_nonneg _) (T_lt_one hnorm))
        (tendsto_pow_atTop_atTop_of_one_lt (by simp)))

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
⊢ v f < 1 ↔ (inftyValuation K) f < 1

Tactic:
have hlt' : 1 < inftyValuation K X := by simp [← exp_zero]

Goal state after:
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 f < 1 ↔ (inftyValuation K) f < 1
Module: Mathlib.NumberTheory.SelbergSieve

Goal state before:
pp: s : BoundingSieve
d : ℕ
hd : d ∣ s.prodPrimes
⊢ 0 < ∏ p ∈ d.primeFactors, s.nu p

Tactic:
apply prod_pos

Goal state after:
s : BoundingSieve
d : ℕ
hd : d ∣ s.prodPrimes
⊢ ∀ i ∈ d.primeFactors, 0 < s.nu i
Module: Mathlib.NumberTheory.SumTwoSquares

Goal state before:
pp: n : ℕ
⊢ (∃ x y, n = x ^ 2 + y ^ 2) ↔ ∀ q ∈ n.primeFactors, q % 4 = 3 → Even (padicValNat q n)

Tactic:
rcases n.eq_zero_or_pos with (rfl | hn₀)
  · exact ⟨fun _ q _ _ ↦ (padicValNat_zero_right _).symm ▸ Even.zero, fun _ ↦ ⟨0, 0, rfl⟩⟩
  -- now `0 < n`
  refine eq_sq_add_sq_iff_eq_sq_mul.trans ⟨fun ⟨a, b, h₁, h₂⟩ q hq h ↦ ?_, fun H ↦ ?_⟩
  · have : Fact q.Prime := ⟨prime_of_mem_primeFactors hq⟩
    have : q ∣ b → q ∈ b.primeFactors := by grind
    grind (splits := 10) [padicValNat.mul, padicValNat.pow,
      padicValNat.eq_zero_of_not_dvd, mod_four_ne_three_of_mem_primeFactors_of_isSquare_neg_one]
  · obtain ⟨b, a, hb₀, ha₀, hab, hb⟩ := sq_mul_squarefree_of_pos hn₀
    refine ⟨a, b, hab.symm, ZMod.isSquare_neg_one_iff_forall_mem_primeFactors_mod_four_ne_three hb
      |>.mpr fun q hq hq4 ↦ ?_⟩
    have : Fact q.Prime := ⟨prime_of_mem_primeFactors hq⟩
    have := Nat.primeFactors_mono <| Dvd.intro_left _ hab
    have : b.factorization q = 1 := by grind [Squarefree.natFactorization_le_one,
      Prime.dvd_iff_one_le_factorization, prime_of_mem_primeFactors, dvd_of_mem_primeFactors]
    grind [factorization_def, prime_of_mem_primeFactors, padicValNat.mul, padicValNat.pow]

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

Goal state before:
pp: case refine_1.convert_2
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
hRK : IsFractionRing R K
inst✝⁶ : IsDomain S
inst✝⁵ : IsDedekindDomain R
inst✝⁴ : Algebra K L
inst✝³ : Algebra R L
inst✝² : IsScalarTower R K L
inst✝¹ : IsScalarTower R S L
hp : p.IsMaximal
inst✝ : Module.Finite R S
ι : Type v := Free.ChooseBasisIndex (R ⧸ p) (S ⧸ map f p)
b : Basis ι (R ⧸ p) (S ⧸ map f p) := Free.chooseBasis (R ⧸ p) (S ⧸ map f p)
b' : ι → S := fun i ↦ ⋯.choose
b_eq_b' : ⇑b = ⇑(↑R (Submodule.mkQ (map f p))) ∘ b'
b'' : ι → L := ⇑(algebraMap S L) ∘ b'
this : LinearIndependent (R ⧸ p) (⇑(↑R (Submodule.mkQ (map f p))) ∘ b')
⊢ Function.Injective ⇑(↑R (Algebra.linearMap S L))

Tactic:
· exact IsFractionRing.injective S L

Goal state after:
Module: Mathlib.NumberTheory.Transcendental.Liouville.Basic

Goal state before:
pp: a : ℤ
b : ℕ
bN0 : b ≠ 0
cop : a.natAbs.Coprime b
h : Liouville (↑a / ↑b)
p q : ℤ
q1 : 1 < q
qR0 : 0 < ↑q
b0 : ↑b ≠ 0
bq0 : 0 < ↑b * ↑q
a1 : |a * q - ↑b * p| * q ^ (b + 1) < ↑b * q
a0 : a * q - ↑b * p ≠ 0
⊢ False

Tactic:
lift q to ℕ using (zero_lt_one.trans q1).le

Goal state after:
a : ℤ
b : ℕ
bN0 : b ≠ 0
cop : a.natAbs.Coprime b
h : Liouville (↑a / ↑b)
p : ℤ
b0 : ↑b ≠ 0
q : ℕ
q1 : 1 < ↑q
qR0 : 0 < ↑↑q
bq0 : 0 < ↑b * ↑↑q
a1 : |a * ↑q - ↑b * p| * ↑q ^ (b + 1) < ↑b * ↑q
a0 : a * ↑q - ↑b * p ≠ 0
⊢ False
Module: Mathlib.NumberTheory.RamificationInertia.Basic

Goal state before:
pp: case refine_2
R : Type u
inst✝⁵ : CommRing R
S : Type v
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
p : Ideal R
P : Ideal S
hfp : NeZero e
inst✝² : IsDedekindDomain S
inst✝¹ : p.IsMaximal
inst✝ : P.IsPrime
hP0 : P ≠ ⊥
i : ℕ
hi : i ≤ e
Q : ℕ → Prop := fun i ↦ Module.rank (R ⧸ p) ↥(map (Quotient.mk (P ^ e)) (P ^ i)) = (e - i) • Module.rank (R ⧸ p) (S ⧸ P)
⊢ Q e

Tactic:
dsimp only [Q]
    rw [Nat.sub_self, zero_nsmul, map_quotient_self]
    exact rank_bot (R ⧸ p) (S ⧸ P ^ e)

Goal state after:
Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith

Goal state before:
pp: x : ℝ
n : ℕ
hn : 0 < n
hn' : 0 < ↑n
⊢ x < ↑(⌊x * ↑n⌋ + 1) / ↑n

Tactic:
rw [lt_div_iff₀ hn', Int.cast_add, Int.cast_one]

Goal state after:
x : ℝ
n : ℕ
hn : 0 < n
hn' : 0 < ↑n
⊢ x * ↑n < ↑⌊x * ↑n⌋ + 1
Module: Mathlib.NumberTheory.WellApproximable

Goal state before:
pp: A : Type u_1
inst✝ : SeminormedCommGroup A
m : ℕ
δ : ℝ
n : ℕ
hm : 0 < m
a : A
ha : a ∈ approxOrderOf A (n * m) δ
b : A
hb : orderOf b = n * m
hab : a ∈ ball b δ
⊢ orderOf b / (orderOf b).gcd m = n

Tactic:
hb,

Goal state after:
A : Type u_1
inst✝ : SeminormedCommGroup A
m : ℕ
δ : ℝ
n : ℕ
hm : 0 < m
a : A
ha : a ∈ approxOrderOf A (n * m) δ
b : A
hb : orderOf b = n * m
hab : a ∈ ball b δ
⊢ n * m / (n * m).gcd m = n
Module: Mathlib.Order.Interval.Finset.Floor

Goal state before:
pp: α : Type u_1
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : FloorRing α
a b : α
n : ℤ
⊢ ↑n ∈ Set.Ioc a b ↔ n ∈ Finset.Ioc ⌊a⌋ ⌊b⌋

Tactic:
by
  simp [floor_lt, le_floor]

Goal state after:
Module: Mathlib.Order.KonigLemma

Goal state before:
pp: α : ℕ → Type u_1
inst✝¹ : Finite (α 0)
inst✝ : ∀ (i : ℕ), Nonempty (α i)
π : {i j : ℕ} → i ≤ j → α j → α i
π_refl : ∀ ⦃i : ℕ⦄ (a : α i), π ⋯ a = a
π_trans : ∀ ⦃i j k : ℕ⦄ (hij : i ≤ j) (hjk : j ≤ k) (a : α k), π hij (π hjk a) = π ⋯ a
hfin : ∀ (i : ℕ) (a : α i), {b | π ⋯ b = a}.Finite
αs : Type u_1 := (i : ℕ) × α i
x✝ : PartialOrder αs :=
  { le := fun a b ↦ ∃ (h : a.fst ≤ b.fst), π h b.snd = a.snd, le_refl := ⋯, le_trans := ⋯, lt_iff_le_not_ge := ⋯,
    le_antisymm := ⋯ }
hcovby : ∀ {a b : αs}, a ⋖ b ↔ a ≤ b ∧ a.fst + 1 = b.fst
i : ℕ
a : α i
j : ℕ
b : α j
hne : ⟨i, a⟩ ≠ ⟨j, b⟩
hij : i ≤ j
h2 : π hij b = a
⊢ i ≠ j

Tactic:
rintro rfl; simp [← h2, π_refl] at hne

Goal state after: