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

Goal state before:
pp: ι : Type u_1
R : ι → Type u_2
A : (i : ι) → Set (R i)
inst✝ : (i : ι) → TopologicalSpace (R i)
S : Set ι
⊢ TopologicalSpace.induced DFunLike.coe inferInstance ≤
    TopologicalSpace.coinduced (inclusion R A ⋯) (TopologicalSpace.induced DFunLike.coe inferInstance)

Tactic:
by rw [inclusion_eq_id R A (𝓟 S), @coinduced_id]

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

Goal state before:
pp: ι : Type u_1
R : ι → Type u_2
A : (i : ι) → Set (R i)
inst✝¹ : (i : ι) → TopologicalSpace (R i)
S : Set ι
inst✝ : ∀ (i : ι), WeaklyLocallyCompactSpace (R i)
hS : cofinite ≤ 𝓟 S
hAcompact : ∀ i ∈ S, IsCompact (A i)
x : Πʳ (i : ι), [R i, A i]_[𝓟 S]
⊢ ∃ s, IsCompact s ∧ s ∈ 𝓝 x

Tactic:
rw [le_principal_iff, mem_cofinite] at hS

Goal state after:
ι : Type u_1
R : ι → Type u_2
A : (i : ι) → Set (R i)
inst✝¹ : (i : ι) → TopologicalSpace (R i)
S : Set ι
inst✝ : ∀ (i : ι), WeaklyLocallyCompactSpace (R i)
hS : Sᶜ.Finite
hAcompact : ∀ i ∈ S, IsCompact (A i)
x : Πʳ (i : ι), [R i, A i]_[𝓟 S]
⊢ ∃ s, IsCompact s ∧ s ∈ 𝓝 x
Module: Mathlib.Topology.Algebra.RestrictedProduct.Basic

Goal state before:
pp: ι : Type u_1
S : ι → Type u_3
G : ι → Type u_4
inst✝³ : (i : ι) → SetLike (S i) (G i)
A : (i : ι) → S i
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Group (G i)
inst✝ : ∀ (i : ι), SubgroupClass (S i) (G i)
i : ι
r : G i
n : ℤ
i✝ : ι
⊢ (mulSingle A i (r ^ n)) i✝ = (mulSingle A i r ^ n) i✝

Tactic:
simp [Pi.mulSingle_zpow, RestrictedProduct.zpow_apply]

Goal state after:
Module: Mathlib.NumberTheory.Multiplicity

Goal state before:
pp: case inl
p : ℕ
hp : Prime p
hp1 : Odd p
x y : ℕ
hxy : p ∣ x - y
hx : ¬p ∣ x
n : ℕ
hyx : y ≤ x
⊢ emultiplicity p (x ^ n - y ^ n) = emultiplicity p (x - y) + emultiplicity p n

Tactic:
iterate 2 rw [← Int.natCast_emultiplicity]
    rw [Int.ofNat_sub (Nat.pow_le_pow_left hyx n)]
    rw [← Int.natCast_dvd_natCast] at hxy hx
    rw [Int.natCast_sub hyx] at *
    push_cast at *
    exact Int.emultiplicity_pow_sub_pow hp hp1 hxy hx n

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

Goal state before:
pp: ι : Type u_1
R : ι → Type u_2
A : (i : ι) → Set (R i)
𝓕 : Filter ι
inst✝ : (i : ι) → TopologicalSpace (R i)
⊢ topologicalSpace R A 𝓕 =
    ⨆ S, ⨆ (hS : 𝓕 ≤ 𝓟 S), TopologicalSpace.coinduced (inclusion R A hS) (topologicalSpace R A (𝓟 S))

Tactic:
topologicalSpace_eq_of_principal,

Goal state after:
ι : Type u_1
R : ι → Type u_2
A : (i : ι) → Set (R i)
𝓕 : Filter ι
inst✝ : (i : ι) → TopologicalSpace (R i)
⊢ topologicalSpace R A 𝓕 =
    ⨆ S,
      ⨆ (x : 𝓕 ≤ 𝓟 S),
        TopologicalSpace.coinduced (inclusion R A ⋯) (TopologicalSpace.induced DFunLike.coe inferInstance)
Module: Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace

Goal state before:
pp: ι : Type u_1
R : ι → Type u_2
A : (i : ι) → Set (R i)
𝓕 : Filter ι
inst✝¹ : (i : ι) → TopologicalSpace (R i)
X : Type u_3
inst✝ : TopologicalSpace X
f : Πʳ (i : ι), [R i, A i]_[𝓕] → X
⊢ Continuous[topologicalSpace R A 𝓕, inst✝] f ↔
    ∀ (S : Set ι) (hS : 𝓕 ≤ 𝓟 S), Continuous[topologicalSpace R A (𝓟 S), inst✝] (f ∘ inclusion R A hS)

Tactic:
topologicalSpace_eq_of_principal,

Goal state after:
ι : Type u_1
R : ι → Type u_2
A : (i : ι) → Set (R i)
𝓕 : Filter ι
inst✝¹ : (i : ι) → TopologicalSpace (R i)
X : Type u_3
inst✝ : TopologicalSpace X
f : Πʳ (i : ι), [R i, A i]_[𝓕] → X
⊢ Continuous[topologicalSpace R A 𝓕, inst✝] f ↔
    ∀ (S : Set ι) (hS : 𝓕 ≤ 𝓟 S),
      Continuous[TopologicalSpace.induced DFunLike.coe inferInstance, inst✝] (f ∘ 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 : 𝓞 K
u : (𝓞 K)ˣ
⊢ (mixedEmbedding K) ((algebraMap (𝓞 K) K) ↑u) * (mixedEmbedding K) ↑x = (mixedEmbedding K) ↑y ↔ ↑u * x = y

Tactic:
← map_mul,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x y : 𝓞 K
u : (𝓞 K)ˣ
⊢ (mixedEmbedding K) ((algebraMap (𝓞 K) K) ↑u * ↑x) = (mixedEmbedding K) ↑y ↔ ↑u * x = y
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x y : 𝓞 K
u : (𝓞 K)ˣ
⊢ ↑↑u * ↑x = ↑y ↔ ↑u * x = y

pp: case I
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x y : 𝓞 K
u : (𝓞 K)ˣ
⊢ Function.Injective ⇑(mixedEmbedding K)

Tactic:
← map_mul,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x y : 𝓞 K
u : (𝓞 K)ˣ
⊢ (algebraMap (𝓞 K) K) (↑u * x) = ↑y ↔ ↑u * x = y

case I
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x y : 𝓞 K
u : (𝓞 K)ˣ
⊢ Function.Injective ⇑(mixedEmbedding K)
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone

Goal state before:
pp: case mk
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
b✝ : Associates ↥(𝓞 K)⁰
x : ↥(𝓞 K)⁰
u : (𝓞 K)ˣ
hu : u • (mixedEmbedding K) ↑↑x ∈ integerSet K
⊢ (mixedEmbedding K) ((algebraMap (𝓞 K) K) ↑u) * (mixedEmbedding K) ↑↑x *
      (mixedEmbedding K) ((algebraMap (𝓞 K) K) ↑↑(unitsNonZeroDivisorsEquiv.symm u⁻¹)) =
    (mixedEmbedding K) ↑↑x

Tactic:
← map_mul,

Goal state after:
case mk
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
b✝ : Associates ↥(𝓞 K)⁰
x : ↥(𝓞 K)⁰
u : (𝓞 K)ˣ
hu : u • (mixedEmbedding K) ↑↑x ∈ integerSet K
⊢ (mixedEmbedding K) ((algebraMap (𝓞 K) K) (↑u * ↑x * ↑↑(unitsNonZeroDivisorsEquiv.symm u⁻¹))) = (mixedEmbedding K) ↑↑x
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
a : ↑(integerSet K)
ζ : ↥(torsion K)
hζ :
  (mixedEmbedding K) ((algebraMap (𝓞 K) K) ↑↑ζ) * (mixedEmbedding K) ↑↑(preimageOfMemIntegerSet a) =
    (mixedEmbedding K) ↑↑(preimageOfMemIntegerSet a)
⊢ ζ = 1

Tactic:
← map_mul,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
a : ↑(integerSet K)
ζ : ↥(torsion K)
hζ :
  (mixedEmbedding K) ((algebraMap (𝓞 K) K) ↑↑ζ * ↑↑(preimageOfMemIntegerSet a)) =
    (mixedEmbedding K) ↑↑(preimageOfMemIntegerSet a)
⊢ ζ = 1
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
a : ↑(integerSet K)
ζ : ↥(torsion K)
hζ : (algebraMap (𝓞 K) K) ↑↑ζ * ↑↑(preimageOfMemIntegerSet a) = ↑↑(preimageOfMemIntegerSet a)
⊢ ζ = 1

Tactic:
← map_mul,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
a : ↑(integerSet K)
ζ : ↥(torsion K)
hζ : (algebraMap (𝓞 K) K) (↑↑ζ * ↑(preimageOfMemIntegerSet a)) = ↑↑(preimageOfMemIntegerSet a)
⊢ ζ = 1
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
this : Subgroup.map (Units.map ↑(algebraMap (𝓞 ↥K⁺) (𝓞 K))) (torsion ↥K⁺) ≤ torsion K
⊢ Subgroup.closure (Set.range (realFundSystem K)) ⊔ torsion K =
    Subgroup.map (Units.map ↑(algebraMap (𝓞 ↥K⁺) (𝓞 K))) (Subgroup.closure (Set.range (fundSystem ↥K⁺))) ⊔
        Subgroup.map (Units.map ↑(algebraMap (𝓞 ↥K⁺) (𝓞 K))) (torsion ↥K⁺) ⊔
      torsion K

Tactic:
sup_assoc,

Goal state after:
K : Type u_1
inst✝³ : Field K
inst✝² : CharZero K
inst✝¹ : IsCMField K
inst✝ : NumberField K
this : Subgroup.map (Units.map ↑(algebraMap (𝓞 ↥K⁺) (𝓞 K))) (torsion ↥K⁺) ≤ torsion K
⊢ Subgroup.closure (Set.range (realFundSystem K)) ⊔ torsion K =
    Subgroup.map (Units.map ↑(algebraMap (𝓞 ↥K⁺) (𝓞 K))) (Subgroup.closure (Set.range (fundSystem ↥K⁺))) ⊔
      (Subgroup.map (Units.map ↑(algebraMap (𝓞 ↥K⁺) (𝓞 K))) (torsion ↥K⁺) ⊔ torsion K)
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, (smulRight 1 (deriv_expMap_single x_1 ((completeBasis K).equivFun.symm x x_1))) 1) *
        LinearMap.det ↑↑(completeBasis K).equivFunL.symm| =
    Real.exp (x w₀ * ↑(finrank ℚ K)) * (∏ w, ↑expMapBasis x ↑w)⁻¹ * 2⁻¹ ^ nrComplexPlaces K * ↑(finrank ℚ K) *
      regulator K

Tactic:
smulRight_apply,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : realSpace K
⊢ |(∏ x_1, 1 1 • deriv_expMap_single x_1 ((completeBasis K).equivFun.symm x x_1)) *
        LinearMap.det ↑↑(completeBasis K).equivFunL.symm| =
    Real.exp (x w₀ * ↑(finrank ℚ K)) * (∏ w, ↑expMapBasis x ↑w)⁻¹ * 2⁻¹ ^ nrComplexPlaces K * ↑(finrank ℚ K) *
      regulator K
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne

Goal state before:
pp: case neg.refine_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : realSpace K
hx : ¬∀ (w : InfinitePlace K), 0 < x w
⊢ x ∈ ↑expMapBasis '' paramSet K → x ∈ normAtAllPlaces '' normLeOne K

Tactic:
rintro ⟨a, _, rfl⟩

Goal state after:
case neg.refine_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
a : realSpace K
left✝ : a ∈ paramSet K
hx : ¬∀ (w : InfinitePlace K), 0 < ↑expMapBasis a w
⊢ ↑expMapBasis a ∈ normAtAllPlaces '' normLeOne K
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst✝ : Field K
ζ : K
hζ : IsPrimitiveRoot ζ p
η : 𝓞 K
hη : η ∈ primitiveRoots p (𝓞 K)
hη' : IsPrimitiveRoot (↑η) p
⊢ Associated (hζ.toInteger - 1) (1 - η)

Tactic:
simpa using (associated_sub_one_of_isPrimitiveRoot p hζ hη').neg_right

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
hK : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ p
x : 𝓞 K
hx : ¬hζ.toInteger - 1 ∣ x
⊢ IsCoprime (↑p) x

Tactic:
by
  rwa [← isCoprime_span_singleton_iff,  ← span_singleton_eq_span_singleton.mpr
    (associated_zeta_sub_one_pow_prime p hζ), ← span_singleton_pow,
    IsCoprime.pow_left_iff (by grind [hp.out.one_lt]), isCoprime_iff_gcd,
    (prime_span_singleton_iff.mpr
    hζ.zeta_sub_one_prime').irreducible.gcd_eq_one_iff, dvd_span_singleton, mem_span_singleton]

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 : ℝ
hs : 0 ≤ s
hS : Finite ↑S
⊢ ∑' (𝔭 : ↑S), 1 ≤ ↑S.ncard

Tactic:
simp [Summable.of_finite, Nat.one_le_iff_ne_zero,
    Ideal.absNorm_eq_zero_iff, hs, HeightOneSpectrum.ne_bot]

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

Goal state before:
pp: case hf
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
S : Set (HeightOneSpectrum (𝓞 K))
s : ℝ
hs : 0 ≤ s
hS : Finite ↑S
⊢ Summable fun 𝔭 ↦ ↑(Ideal.absNorm (↑𝔭).asIdeal) ^ (-s)

Tactic:
simp [Summable.of_finite, Nat.one_le_iff_ne_zero,
    Ideal.absNorm_eq_zero_iff, hs, HeightOneSpectrum.ne_bot]

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

Goal state before:
pp: case hg
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
S : Set (HeightOneSpectrum (𝓞 K))
s : ℝ
hs : 0 ≤ s
hS : Finite ↑S
⊢ Summable fun 𝔭 ↦ 1

Tactic:
simp [Summable.of_finite, Nat.one_le_iff_ne_zero,
    Ideal.absNorm_eq_zero_iff, hs, HeightOneSpectrum.ne_bot]

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

Goal state before:
pp: case hx
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
S : Set (HeightOneSpectrum (𝓞 K))
s : ℝ
hs : 0 ≤ s
hS : Finite ↑S
𝔭 : ↑S
⊢ 1 ≤ ↑(Ideal.absNorm (↑𝔭).asIdeal)

Tactic:
simp [Summable.of_finite, Nat.one_le_iff_ne_zero,
    Ideal.absNorm_eq_zero_iff, hs, HeightOneSpectrum.ne_bot]

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

Goal state before:
pp: case hz
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
S : Set (HeightOneSpectrum (𝓞 K))
s : ℝ
hs : 0 ≤ s
hS : Finite ↑S
𝔭 : ↑S
⊢ -s ≤ 0

Tactic:
simp [Summable.of_finite, Nat.one_le_iff_ne_zero,
    Ideal.absNorm_eq_zero_iff, hs, HeightOneSpectrum.ne_bot]

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
⊢ asiegel K a ≠ 0

Tactic:
simp +unfoldPartialApp only [asiegel, a']
  simp only [ne_eq]
  rw [funext_iff]; intro hs
  simp only [Prod.forall] at hs
  apply ha
  rw [← Matrix.ext_iff]; intro k' l
  specialize hs k'
  let ⟨b⟩ := Fintype.card_pos_iff.1 (Fintype.card_pos (α := (K →+* ℂ)))
  have := ((newBasis K).repr.map_eq_zero_iff (x := (a k' l * (newBasis K) b))).1 <| by
    ext b'
    specialize hs b'
    rw [funext_iff] at hs
    simp only [Prod.forall] at hs
    apply hs
  simp only [mul_eq_zero] at this
  exact this.resolve_right (Basis.ne_zero (newBasis K) b)

Goal state after:
Module: Mathlib.NumberTheory.SiegelsLemma

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

Tactic:
rw [norm_lt_iff Real.zero_lt_one] at h

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

Goal state before:
pp: f : AbsoluteValue ℚ ℝ
p : ℕ
hp0 : 0 < f ↑p
hp1 : f ↑p < 1
hmin : ∀ (m : ℕ), 0 < f ↑m ∧ f ↑m < 1 → p ≤ m
⊢ Nat.Prime p

Tactic:
have hp2 : 2 ≤ p := by
    by_contra! hp
    interval_cases p <;> grind
  rw [Nat.prime_iff_not_exists_mul_eq]
  refine ⟨hp2, ?_⟩
  rintro ⟨a, b, ha, hb, rfl⟩
  obtain ⟨ha₀, hb₀⟩ := mul_ne_zero_iff.mp (by omega : a * b ≠ 0)
  have h {n : ℕ} (hn₀ : n ≠ 0) (hn : n < a * b) : 1 ≤ f n := by
    by_contra! hn₁
    exact (not_le_of_gt hn) <| hmin n ⟨map_pos_of_ne_zero f (mod_cast hn₀), hn₁⟩
  rw [Nat.cast_mul, map_mul] at hp1
  exact not_le_of_gt hp1 <| one_le_mul_of_one_le_of_one_le (h ha₀ ha) (h hb₀ hb)

Goal state after:
Module: Mathlib.NumberTheory.Ostrowski

Goal state before:
pp: case refine_1.inr
f : AbsoluteValue ℚ ℝ
hf_nontriv : f.IsNontrivial
bdd : ∀ (n : ℕ), f ↑n ≤ 1
p : ℕ
hmin : ∀ (m : ℕ), 0 < f ↑m ∧ f ↑m < 1 → p ≤ m
hp0 : 0 < f ↑p
hp1 : f ↑p < 1
hp : Nat.Prime p
this : Fact (Nat.Prime p)
t : ℝ
ht : 0 < t
hpt : f ↑p = ↑p ^ (-t)
n : ℕ
hn : n ≠ 0
⊢ f ↑n ^ t⁻¹ = (padic p) ↑n

Tactic:
rcases Nat.exists_eq_pow_mul_and_not_dvd hn p hp.ne_one with ⟨_, m, hpm, rfl⟩
      have := (padicNorm.nat_eq_one_iff m).mpr hpm
      simp_all [← rpow_natCast, ← rpow_mul, mul_comm t, mul_inv_cancel_right₀ ht.ne',
        eq_one_of_not_dvd bdd hp0 hp1 hmin hpm]

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)
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
⊢ house ((algebraMap (𝓞 K) K) (∑ r, ↑(x (l, r)) * (newBasis K) r)) ≤
    ∑ r, house ((algebraMap (𝓞 K) K) ↑(x (l, r)) * (algebraMap (𝓞 K) K) ((newBasis K) r))

Tactic:
← map_mul,

Goal state after:
case calc_1
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
⊢ house ((algebraMap (𝓞 K) K) (∑ r, ↑(x (l, r)) * (newBasis K) r)) ≤
    ∑ x_1, house ((algebraMap (𝓞 K) K) (↑(x (l, x_1)) * (newBasis K) x_1))
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
h_ineq1 : ∀ {m n : ℕ}, 1 < m → 1 < n → f ↑n ≤ ↑m * f ↑m / (f ↑m - 1) * f ↑m ^ logb ↑m ↑n
he : 0 < ↑m * f ↑m / (f ↑m - 1)
⊢ f ↑n ^ k ≤ ((↑m * f ↑m / (f ↑m - 1)) ^ (↑k)⁻¹) ^ ↑k * (f ↑m ^ logb ↑m ↑n) ^ ↑k

Tactic:
← rpow_mul he.le,

Goal state after:
f : AbsoluteValue ℚ ℝ
m n : ℕ
hm : 1 < m
hn : 1 < n
notbdd : ¬∀ (n : ℕ), f ↑n ≤ 1
k : ℕ
hk : k ≠ 0
h_ineq1 : ∀ {m n : ℕ}, 1 < m → 1 < n → f ↑n ≤ ↑m * f ↑m / (f ↑m - 1) * f ↑m ^ logb ↑m ↑n
he : 0 < ↑m * f ↑m / (f ↑m - 1)
⊢ f ↑n ^ k ≤ (↑m * f ↑m / (f ↑m - 1)) ^ ((↑k)⁻¹ * ↑k) * (f ↑m ^ logb ↑m ↑n) ^ ↑k
Module: Mathlib.NumberTheory.Ostrowski

Goal state before:
pp: case inl
f : AbsoluteValue ℚ ℝ
notbdd : ¬∀ (n : ℕ), f ↑n ≤ 1
m : ℕ
hm : ¬f ↑m ≤ 1
hfm1 : 1 < f ↑m
oneltm : 1 < m
s : ℝ := logb (↑m) (f ↑m)
hs : s = logb (↑m) (f ↑m)
hs0 : 0 < s
n : ℕ
h : n < 1
⊢ f ↑n ^ s⁻¹ = real ↑n

Tactic:
obtain rfl : n = 0 := by lia
    simp [hs0.ne']

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
k n : ℕ
⊢ (mahler k) ↑n = ↑(n.choose k)

Tactic:
simp only [mahler_apply, Ring.choose_natCast]

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
E : Type u_4
inst✝¹¹ : TopologicalSpace X
inst✝¹⁰ : TopologicalSpace Y
inst✝⁹ : AddCommGroup E
inst✝⁸ : TopologicalSpace E
inst✝⁷ : IsTopologicalAddGroup E
inst✝⁶ : CommRing R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : IsTopologicalRing R
inst✝³ : Module R E
inst✝² : ContinuousSMul R E
μ : AbstractMeasure X R R
ν✝ : AbstractMeasure Y R R
inst✝¹ : LocallyCompactSpace X
inst✝ : LocallyCompactSpace Y
ν : AbstractMeasure Y R R
⊢ Continuous (Function.uncurry fun x y ↦ (x.1.curry x.2) y)

Tactic:
← (Homeomorph.prodAssoc C(X × Y, R) X Y).symm.comp_continuous_iff'

Goal state after:
X : Type u_1
Y : Type u_2
R : Type u_3
E : Type u_4
inst✝¹¹ : TopologicalSpace X
inst✝¹⁰ : TopologicalSpace Y
inst✝⁹ : AddCommGroup E
inst✝⁸ : TopologicalSpace E
inst✝⁷ : IsTopologicalAddGroup E
inst✝⁶ : CommRing R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : IsTopologicalRing R
inst✝³ : Module R E
inst✝² : ContinuousSMul R E
μ : AbstractMeasure X R R
ν✝ : AbstractMeasure Y R R
inst✝¹ : LocallyCompactSpace X
inst✝ : LocallyCompactSpace Y
ν : AbstractMeasure Y R R
⊢ Continuous ((Function.uncurry fun x y ↦ (x.1.curry x.2) y) ∘ ⇑(Homeomorph.prodAssoc C(X × Y, R) X Y).symm)
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)
y : Y
⊢ ((contractFst μ) (f.comp fst • g.comp snd)) y = (μ f • g) y

Tactic:
contractFst_apply,

Goal state after:
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)
y : Y
⊢ μ { toFun := fun x ↦ (f.comp fst • g.comp snd) (x, y), continuous_toFun := ⋯ } = (μ f • g) y
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:
rw [mem_ofPred, abs_sub_comm, ← @Int.cast_lt ℝ,
      ← div_lt_div_iff_of_pos_right (abs_pos_of_pos h0)]

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
⊢ ↑|d * ↑q.den ^ 2 - q.num ^ 2| / |↑q.den ^ 2| < ↑M / |↑q.den ^ 2|
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
z z' z1 : ℤ_[p]
hz' : z' = z - z1
n : ℕ
hz : ih_gen n z
h1 : ‖↑((Polynomial.aeval z) F) / ↑((Polynomial.aeval z) (Polynomial.derivative F))‖ ≤ 1
hzeq : z1 = ⟨↑((Polynomial.aeval z) F) / ↑((Polynomial.aeval z) (Polynomial.derivative F)), h1⟩
hdzne : (Polynomial.aeval z) (Polynomial.derivative F) ≠ 0
hdzne' : ↑((Polynomial.aeval z) (Polynomial.derivative F)) ≠ 0
q : ℤ_[p]
hq :
  Polynomial.eval (z + -z1) (Polynomial.map (algebraMap R ℤ_[p]) F) =
    Polynomial.eval z (Polynomial.map (algebraMap R ℤ_[p]) F) +
        Polynomial.eval z (Polynomial.derivative (Polynomial.map (algebraMap R ℤ_[p]) F)) * -z1 +
      q * (-z1) ^ 2
this :
  ‖↑((Polynomial.aeval z) (Polynomial.derivative F)) *
        (↑((Polynomial.aeval z) F) / ↑((Polynomial.aeval z) (Polynomial.derivative F)))‖ ≤
    1
⊢ (Polynomial.aeval z) (Polynomial.derivative F) * -z1 =
    (Polynomial.aeval z) (Polynomial.derivative F) *
      -⟨↑((Polynomial.aeval z) F) / ↑((Polynomial.aeval z) (Polynomial.derivative F)), h1⟩

Tactic:
rw [hzeq]

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
z z' z1 : ℤ_[p]
n : ℕ
hz : ih_gen n z
q : ℤ_[p]
heq : (Polynomial.aeval z') F = q * z1 ^ 2
h1 : ‖↑((Polynomial.aeval z) F) / ↑((Polynomial.aeval z) (Polynomial.derivative F))‖ ≤ 1
hzeq : z1 = ⟨↑((Polynomial.aeval z) F) / ↑((Polynomial.aeval z) (Polynomial.derivative F)), h1⟩
⊢ ‖(Polynomial.aeval z') F‖ = ‖q‖ * ‖z1‖ ^ 2

Tactic:
simp [heq]

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:
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.RatFunc.Ostrowski

Goal state before:
pp: case inl
K : Type u_1
Γ : Type u_2
inst✝⁴ : Field K
inst✝³ : LinearOrderedCommGroupWithZero Γ
v : Valuation K⟮X⟯ Γ
inst✝² : v.IsRankOneDiscrete
inst✝¹ : IsTrivialOn K v
inst✝ : DecidableEq K⟮X⟯
hlt : 1 < v X
hv : v.IsEquiv (inftyValuation K)
pw : HeightOneSpectrum K[X]
hw : v.IsEquiv (valuation K⟮X⟯ pw)
⊢ ∃ x, ∃ (_ : v.IsEquiv (valuation K⟮X⟯ x)), ¬x = pw

Tactic:
exact absurd (hw.symm.trans hv) (adicValuation_not_isEquiv_infty_valuation pw)

Goal state after:
Module: Mathlib.NumberTheory.Zsqrtd.QuadraticReciprocity

Goal state before:
pp: case re
p : ℕ
hp : Fact (Nat.Prime p)
hpi : Prime ↑p
hp1 : p % 2 = 1
hp3 : p % 4 ≠ 3
k : ℕ
k_lt_p : k < p
hk : -1 = ↑k * ↑k
hpk : p ∣ k ^ 2 + 1
⊢ (↑k ^ 2 + 1).re = ({ re := ↑k, im := 1 } * { re := ↑k, im := -1 }).re

Tactic:
simp [sq]

Goal state after:
Module: Mathlib.NumberTheory.Zsqrtd.QuadraticReciprocity

Goal state before:
pp: case im
p : ℕ
hp : Fact (Nat.Prime p)
hpi : Prime ↑p
hp1 : p % 2 = 1
hp3 : p % 4 ≠ 3
k : ℕ
k_lt_p : k < p
hk : -1 = ↑k * ↑k
hpk : p ∣ k ^ 2 + 1
⊢ (↑k ^ 2 + 1).im = ({ re := ↑k, im := 1 } * { re := ↑k, im := -1 }).im

Tactic:
simp [sq]

Goal state after:
Module: Mathlib.NumberTheory.SumTwoSquares

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
a b x y u v : R
ha : a = x ^ 2 + y ^ 2
hb : b = u ^ 2 + v ^ 2
⊢ (x ^ 2 + y ^ 2) * b = (x * u - y * v) ^ 2 + (x * v + y * u) ^ 2

Tactic:
hb

Goal state after:
R : Type u_1
inst✝ : CommRing R
a b x y u v : R
ha : a = x ^ 2 + y ^ 2
hb : b = u ^ 2 + v ^ 2
⊢ (x ^ 2 + y ^ 2) * (u ^ 2 + v ^ 2) = (x * u - y * v) ^ 2 + (x * v + y * u) ^ 2