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

Goal state before:
pp: x y : ℤ
n : ℕ
hxy : 4 ∣ x - y
hx : ¬2 ∣ x
hx_odd : Odd x
hxy_even : Even (x - y)
hy_odd : Odd y
⊢ emultiplicity 2 (x ^ n - y ^ n) = emultiplicity 2 (x - y) + emultiplicity 2 ↑n

Tactic:
rcases n with - | n

Goal state after:
case zero
x y : ℤ
hxy : 4 ∣ x - y
hx : ¬2 ∣ x
hx_odd : Odd x
hxy_even : Even (x - y)
hy_odd : Odd y
⊢ emultiplicity 2 (x ^ 0 - y ^ 0) = emultiplicity 2 (x - y) + emultiplicity 2 ↑0

case succ
x y : ℤ
hxy : 4 ∣ x - y
hx : ¬2 ∣ x
hx_odd : Odd x
hxy_even : Even (x - y)
hy_odd : Odd y
n : ℕ
⊢ emultiplicity 2 (x ^ (n + 1) - y ^ (n + 1)) = emultiplicity 2 (x - y) + emultiplicity 2 ↑(n + 1)
Module: Mathlib.NumberTheory.Multiplicity

Goal state before:
pp: n x : ℕ
h1x : 1 < x
hx : ¬2 ∣ x
hn : n ≠ 0
hneven : Even n
this✝ : padicValNat 2 ((x + 1) * (x - 1)) ≥ 3
this : padicValNat 2 (x ^ n - 1) + 1 = padicValNat 2 (x + 1) + padicValNat 2 (x - 1) + padicValNat 2 n
⊢ padicValNat 2 n + 2 ≤ padicValNat 2 (x ^ n - 1)

Tactic:
grind [← padicValNat.mul]

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

Goal state before:
pp: ι : Type u_1
n : Type u_3
inst✝² : Finite n
X : Type u_4
inst✝¹ : TopologicalSpace X
A : n → ι → Type u_5
inst✝ : (j : n) → (i : ι) → TopologicalSpace (A j i)
C : (j : n) → (i : ι) → Set (A j i)
hCopen : ∀ (j : n) (i : ι), IsOpen[inst✝ j i] (C j i)
f : ((j : n) → Πʳ (i : ι), [A j i, C j i]) → X
H :
  ∀ (S : Set ι) (hS : cofinite ≤ 𝓟 S),
    Continuous[Pi.topologicalSpace, inst✝¹] (f ∘ Pi.map fun x ↦ inclusion (A x) (C x) hS)
x : (j : n) → Πʳ (i : ι), [A j i, C j i]
S : Set ι := {i | ∀ (j : n), (x j) i ∈ C j i}
hS : cofinite ≤ 𝓟 S
x' : (j : n) → Πʳ (i : ι), [A j i, C j i]_[𝓟 S] := fun j ↦ mk (fun i ↦ (x j) i) ⋯
hxx' : Pi.map (fun j ↦ inclusion (A j) (C j) hS) x' = x
⊢ Tendsto f (Filter.map (Pi.map fun i ↦ inclusion (A i) (C i) hS) (Filter.pi fun i ↦ 𝓝 (x' i)))
    (𝓝 (f (Pi.map (fun i ↦ inclusion (A i) (C i) hS) x')))

Tactic:
tendsto_map'_iff,

Goal state after:
ι : Type u_1
n : Type u_3
inst✝² : Finite n
X : Type u_4
inst✝¹ : TopologicalSpace X
A : n → ι → Type u_5
inst✝ : (j : n) → (i : ι) → TopologicalSpace (A j i)
C : (j : n) → (i : ι) → Set (A j i)
hCopen : ∀ (j : n) (i : ι), IsOpen[inst✝ j i] (C j i)
f : ((j : n) → Πʳ (i : ι), [A j i, C j i]) → X
H :
  ∀ (S : Set ι) (hS : cofinite ≤ 𝓟 S),
    Continuous[Pi.topologicalSpace, inst✝¹] (f ∘ Pi.map fun x ↦ inclusion (A x) (C x) hS)
x : (j : n) → Πʳ (i : ι), [A j i, C j i]
S : Set ι := {i | ∀ (j : n), (x j) i ∈ C j i}
hS : cofinite ≤ 𝓟 S
x' : (j : n) → Πʳ (i : ι), [A j i, C j i]_[𝓟 S] := fun j ↦ mk (fun i ↦ (x j) i) ⋯
hxx' : Pi.map (fun j ↦ inclusion (A j) (C j) hS) x' = x
⊢ Tendsto (f ∘ Pi.map fun i ↦ inclusion (A i) (C i) hS) (Filter.pi fun i ↦ 𝓝 (x' i))
    (𝓝 (f (Pi.map (fun i ↦ inclusion (A i) (C i) hS) x')))
Module: Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace

Goal state before:
pp: ι : Type u_1
R : ι → Type u_2
A : (i : ι) → Set (R i)
𝓕✝ 𝓖 : Filter ι
S : ι → Type u_3
inst✝⁴ : (i : ι) → SetLike (S i) (R i)
B : (i : ι) → S i
T : Set ι
𝓕 : Filter ι
inst✝³ : (i : ι) → TopologicalSpace (R i)
inst✝² : (i : ι) → Inv (R i)
inst✝¹ : ∀ (i : ι), InvMemClass (S i) (R i)
inst✝ : ∀ (i : ι), ContinuousInv (R i)
⊢ Continuous[topologicalSpace R (fun i ↦ ↑(B i)) 𝓕, topologicalSpace R (fun i ↦ ↑(B i)) 𝓕] fun a ↦ a⁻¹

Tactic:
continuous_dom

Goal state after:
ι : Type u_1
R : ι → Type u_2
A : (i : ι) → Set (R i)
𝓕✝ 𝓖 : Filter ι
S : ι → Type u_3
inst✝⁴ : (i : ι) → SetLike (S i) (R i)
B : (i : ι) → S i
T : Set ι
𝓕 : Filter ι
inst✝³ : (i : ι) → TopologicalSpace (R i)
inst✝² : (i : ι) → Inv (R i)
inst✝¹ : ∀ (i : ι), InvMemClass (S i) (R i)
inst✝ : ∀ (i : ι), ContinuousInv (R i)
⊢ ∀ (S_1 : Set ι) (hS : 𝓕 ≤ 𝓟 S_1),
    Continuous[topologicalSpace R (fun i ↦ ↑(B i)) (𝓟 S_1), topologicalSpace R (fun i ↦ ↑(B i)) 𝓕]
      ((fun a ↦ a⁻¹) ∘ inclusion R (fun i ↦ ↑(B i)) hS)
Module: Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace

Goal state before:
pp: ι : Type u_1
R : ι → Type u_2
A : (i : ι) → Set (R i)
𝓕✝ 𝓖 : Filter ι
S : ι → Type u_3
inst✝⁴ : (i : ι) → SetLike (S i) (R i)
B : (i : ι) → S i
T : Set ι
𝓕 : Filter ι
inst✝³ : (i : ι) → TopologicalSpace (R i)
G : Type u_4
inst✝² : (i : ι) → SMul G (R i)
inst✝¹ : ∀ (i : ι), SMulMemClass (S i) G (R i)
inst✝ : ∀ (i : ι), ContinuousConstSMul G (R i)
g : G
⊢ Continuous[topologicalSpace R (fun i ↦ ↑(B i)) 𝓕, topologicalSpace R (fun i ↦ ↑(B i)) 𝓕] fun x ↦ g • x

Tactic:
continuous_dom

Goal state after:
ι : Type u_1
R : ι → Type u_2
A : (i : ι) → Set (R i)
𝓕✝ 𝓖 : Filter ι
S : ι → Type u_3
inst✝⁴ : (i : ι) → SetLike (S i) (R i)
B : (i : ι) → S i
T : Set ι
𝓕 : Filter ι
inst✝³ : (i : ι) → TopologicalSpace (R i)
G : Type u_4
inst✝² : (i : ι) → SMul G (R i)
inst✝¹ : ∀ (i : ι), SMulMemClass (S i) G (R i)
inst✝ : ∀ (i : ι), ContinuousConstSMul G (R i)
g : G
⊢ ∀ (S_1 : Set ι) (hS : 𝓕 ≤ 𝓟 S_1),
    Continuous[topologicalSpace R (fun i ↦ ↑(B i)) (𝓟 S_1), topologicalSpace R (fun i ↦ ↑(B i)) 𝓕]
      ((fun x ↦ g • x) ∘ inclusion R (fun i ↦ ↑(B i)) hS)
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)
⊢ Continuous[topologicalSpace R₁ A₁ 𝓕₁, topologicalSpace R₂ A₂ 𝓕₂] (mapAlong R₁ R₂ f hf φ hφ)

Tactic:
continuous_dom

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
c : ℝ
⊢ logMap (c • 1) = 0

Tactic:
by
  ext
  rw [logMap_apply, normAtPlace_smul, norm_smul, map_one, map_one, mul_one, mul_one, Real.log_pow,
    mul_comm (finrank ℚ K : ℝ) _, mul_assoc, mul_inv_cancel₀ (Nat.cast_ne_zero.mpr finrank_pos.ne'),
    mul_one, sub_self, mul_zero, Pi.zero_apply]

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

Goal state before:
pp: case refine_1
K : Type u_1
inst✝ : Field K
A : Set (mixedSpace K)
hA : normAtAllPlaces ⁻¹' normAtAllPlaces '' A = A
x : realSpace K
⊢ x ∈ normAtAllPlaces '' A ∩ ⋂ w, {x | x ↑w ≠ 0} → x ∈ normAtComplexPlaces '' plusPart A

pp: case refine_2
K : Type u_1
inst✝ : Field K
A : Set (mixedSpace K)
hA : normAtAllPlaces ⁻¹' normAtAllPlaces '' A = A
x : realSpace K
⊢ x ∈ normAtComplexPlaces '' plusPart A → x ∈ normAtAllPlaces '' A ∩ ⋂ w, {x | x ↑w ≠ 0}

Tactic:
· rintro ⟨⟨a, ha, rfl⟩, ha₂⟩
    refine ⟨mixedSpaceOfRealSpace (normAtAllPlaces a), ⟨?_, ?_⟩, ?_⟩
    · rw [← hA, Set.mem_preimage, normAtAllPlaces_normAtAllPlaces]
      exact Set.mem_image_of_mem normAtAllPlaces ha
    · intro w
      refine lt_of_le_of_ne' (normAtPlace_nonneg _ _) (Set.mem_iInter.mp ha₂ w)
    · rw [normAtComplexPlaces_normAtAllPlaces]

Goal state after:
case refine_2
K : Type u_1
inst✝ : Field K
A : Set (mixedSpace K)
hA : normAtAllPlaces ⁻¹' normAtAllPlaces '' A = A
x : realSpace K
⊢ x ∈ normAtComplexPlaces '' plusPart A → x ∈ normAtAllPlaces '' A ∩ ⋂ w, {x | x ↑w ≠ 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
h₁ : indexRealUnits K * (unitsMulComplexConjInv K).range.index = 2
h₂ : (unitsMulComplexConjInv K).range.index = 1
⊢ indexRealUnits K = 2

Tactic:
by rwa [h₂, mul_one] at h₁

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
n : ℕ
a : { a // mixedEmbedding.norm ↑a = ↑n }
⊢ ↑↑((integerSetEquiv K) ↑a).1 = Ideal.span {↑(preimageOfMemIntegerSet ↑a)}

Tactic:
integerSetEquiv_apply_fst

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
n : ℕ
⊢ Nat.card ↑{I | IsPrincipal ↑I ∧ absNorm ↑I = n} * torsionOrder K = Nat.card ↑{a | mixedEmbedding.norm ↑a = ↑n}

Tactic:
by
  rw [torsionOrder, ← Nat.card_prod]
  exact Nat.card_congr (integerSetEquivNorm K n).symm

Goal state after:
Module: Mathlib.NumberTheory.NumberField.Completion.Ramification

Goal state before:
pp: K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
v : InfinitePlace K
w : InfinitePlace L
inst✝ : w.LiesOver v
h : IsRamified K w
H : w.IsComplex ∧ v.IsReal
this : ComplexEmbedding.LiesOver (extensionEmbedding w) (extensionEmbedding v)
⊢ Module.finrank v.Completion w.Completion = 2

Tactic:
Algebra.finrank_eq_of_equiv_equiv (ringEquivRealOfIsReal H.2)
      (ringEquivComplexOfIsComplex H.1) (by ext; simp),

Goal state after:
K : Type u_1
L : Type u_2
inst✝³ : Field K
inst✝² : Field L
inst✝¹ : Algebra K L
v : InfinitePlace K
w : InfinitePlace L
inst✝ : w.LiesOver v
h : IsRamified K w
H : w.IsComplex ∧ v.IsReal
this : ComplexEmbedding.LiesOver (extensionEmbedding w) (extensionEmbedding v)
⊢ Module.finrank ℝ ℂ = 2
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : realSpace K
⊢ HasFDerivAt (↑expMap) (fderiv_expMap x) x

Tactic:
by
  simpa [expMap, fderiv_expMap, hasFDerivAt_pi', OpenPartialHomeomorph.pi_apply,
    ContinuousLinearMap.proj_pi] using!
    fun w ↦ (hasDerivAt_expMap_single w _).hasFDerivAt.comp x (hasFDerivAt_apply w x)

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
h₁ : LinearIndependent ℝ fun w ↦ completeFamily K ↑w
h₂ : completeFamily K w₀ ∉ Submodule.span ℝ (Set.range fun w ↦ completeFamily K ↑w)
⊢ LinearIndependent ℝ (completeFamily K ∘ ⇑(Equiv.optionSubtypeNe w₀))

Tactic:
linearIndependent_option

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
h₁ : LinearIndependent ℝ fun w ↦ completeFamily K ↑w
h₂ : completeFamily K w₀ ∉ Submodule.span ℝ (Set.range fun w ↦ completeFamily K ↑w)
⊢ LinearIndependent ℝ ((completeFamily K ∘ ⇑(Equiv.optionSubtypeNe w₀)) ∘ some) ∧
    (completeFamily K ∘ ⇑(Equiv.optionSubtypeNe w₀)) none ∉
      Submodule.span ℝ (Set.range ((completeFamily K ∘ ⇑(Equiv.optionSubtypeNe w₀)) ∘ some))
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne

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

Tactic:
Pi.smul_def,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : realSpace K
⊢ (fun i ↦
      Real.exp (x w₀) *
        (∏ x_1,
            normAtAllPlaces ((mixedEmbedding K) ((algebraMap (𝓞 K) K) ↑(fundSystem K (equivFinRank.symm x_1)))) ^
              x ↑x_1)
          i) =
    fun i ↦ Real.exp (x w₀) • ∏ i_1, i ((algebraMap (𝓞 K) K) ↑(fundSystem K (equivFinRank.symm i_1))) ^ x ↑i_1
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₀) • fun w ↦ ∏ i, w ((algebraMap (𝓞 K) K) ↑(fundSystem K (equivFinRank.symm i))) ^ x ↑i) x_1 ^
        x_1.mult =
    Real.exp (x w₀) ^ finrank ℚ K

Tactic:
Pi.smul_def,

Goal state after:
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
Module: Mathlib.RingTheory.Polynomial.Cyclotomic.Factorization

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : Fintype K
p f n : ℕ
P : K[X]
hK : Fintype.card K = p ^ f
hn : p.Coprime n
hp : Fact (Nat.Prime p)
hP : P ∣ cyclotomic n K
hPirr : Irreducible P
hPmo : P.Monic
this✝² : Fact (Irreducible P)
this✝¹ : Module.Finite K (AdjoinRoot P)
this✝ : Finite (AdjoinRoot P)
this : NeZero ↑n
⊢ map (of P) P ∣ cyclotomic n (AdjoinRoot P)

Tactic:
by simpa using! map_dvd (algebraMap K (AdjoinRoot P)) hP

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

Goal state before:
pp: case pos
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
u v : Fin (rank K) → (𝓞 K)ˣ
hv : IsMaxRank v
h : Subgroup.closure (Set.range u) ⊔ torsion K ≤ Subgroup.closure (Set.range v) ⊔ torsion K
hu : IsMaxRank u
this : span ℤ (Set.range ⇑(basisOfIsMaxRank hu)) ≤ span ℤ (Set.range ⇑(basisOfIsMaxRank hv))
⊢ ↑((AddSubgroup.map (logEmbedding K) (Subgroup.toAddSubgroup (Subgroup.closure (Set.range u)))).relIndex
        (AddSubgroup.map (logEmbedding K) (Subgroup.toAddSubgroup (Subgroup.closure (Set.range v))))) =
    ↑((Subgroup.closure (Set.range u) ⊔ torsion K).relIndex (Subgroup.closure (Set.range v) ⊔ torsion K))

Tactic:
AddSubgroup.relIndex_map_map,

Goal state after:
case pos
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
u v : Fin (rank K) → (𝓞 K)ˣ
hv : IsMaxRank v
h : Subgroup.closure (Set.range u) ⊔ torsion K ≤ Subgroup.closure (Set.range v) ⊔ torsion K
hu : IsMaxRank u
this : span ℤ (Set.range ⇑(basisOfIsMaxRank hu)) ≤ span ℤ (Set.range ⇑(basisOfIsMaxRank hv))
⊢ ↑((Subgroup.toAddSubgroup (Subgroup.closure (Set.range u)) ⊔ (logEmbedding K).ker).relIndex
        (Subgroup.toAddSubgroup (Subgroup.closure (Set.range v)) ⊔ (logEmbedding K).ker)) =
    ↑((Subgroup.closure (Set.range u) ⊔ torsion K).relIndex (Subgroup.closure (Set.range v) ⊔ torsion K))
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
n : ℕ
hn✝ : 0 < n
hn : 0 < ↑n
⊢ ∫⁻ (x : realSpace K) in paramSet K, ENNReal.ofReal (Real.exp (x w₀ * ↑n)) = (↑n)⁻¹

Tactic:
rw [volume_pi, paramSet, Measure.restrict_pi_pi, lintegral_eq_lmarginal_univ 0,
    lmarginal_erase' _ (by fun_prop) (Finset.mem_univ w₀), if_pos rfl]

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
n : ℕ
hn✝ : 0 < n
hn : 0 < ↑n
⊢ (∫⋯∫⁻_univ.erase w₀, fun x ↦
        ∫⁻ (xᵢ : ℝ) in Set.Iic 0, ENNReal.ofReal (Real.exp (Function.update x w₀ xᵢ w₀ * ↑n)) ∂fun i ↦
        volume.restrict (if i = w₀ then Set.Iic 0 else Set.Ico 0 1))
      0 =
    (↑n)⁻¹
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
h₁ : MeasurableSet (normAtAllPlaces ⁻¹' compactSet K)
h₂ : MeasurableSet (normAtAllPlaces ⁻¹' ↑expMapBasis '' interior (paramSet K))
⊢ 2 ^ nrRealPlaces K * ENNReal.ofReal (2 * Real.pi) ^ nrComplexPlaces K *
      ∫⁻ (x : realSpace K) in normAtAllPlaces '' normAtAllPlaces ⁻¹' compactSet K, ∏ w, ENNReal.ofReal (x ↑w) =
    volume (normAtAllPlaces ⁻¹' ↑expMapBasis '' interior (paramSet K))

Tactic:
normAtAllPlaces_image_preimage_of_nonneg (fun x a w ↦ nonneg_of_mem_compactSet K a w),

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
h₁ : MeasurableSet (normAtAllPlaces ⁻¹' compactSet K)
h₂ : MeasurableSet (normAtAllPlaces ⁻¹' ↑expMapBasis '' interior (paramSet K))
⊢ 2 ^ nrRealPlaces K * ENNReal.ofReal (2 * Real.pi) ^ nrComplexPlaces K *
      ∫⁻ (x : realSpace K) in compactSet K, ∏ w, ENNReal.ofReal (x ↑w) =
    volume (normAtAllPlaces ⁻¹' ↑expMapBasis '' interior (paramSet K))
Module: Mathlib.NumberTheory.NumberField.House

Goal state before:
pp: K : Type u_1
inst✝² : Field K
inst✝¹ : NumberField K
inst✝ : DecidableEq (K →+* ℂ)
α : 𝓞 K
i : K →+* ℂ
σ : K →+* (K →+* ℂ) → ℂ := canonicalEmbedding K
⊢ ∑ x, ‖fun i j ↦ (basisMatrix K)ᵀ⁻¹ i j‖ * house ((algebraMap (𝓞 K) K) α) =
    ↑(finrank ℚ K) * ‖(basisMatrix K)ᵀ⁻¹‖ * house ((algebraMap (𝓞 K) K) α)

Tactic:
simp [Embeddings.card, mul_assoc]

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:
← Nat.card_congr (e _),

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, ↑(Nat.card { x_1 // ClassGroup.mk0 ↑x_1 = x }) / s = ↑(Nat.card { I // ↑(absNorm ↑I) ≤ s }) / s
Module: Mathlib.Topology.Algebra.Nonarchimedean.Completion

Goal state before:
pp: case h
G : Type u_1
inst✝³ : AddGroup G
inst✝² : UniformSpace G
inst✝¹ : IsUniformAddGroup G
inst✝ : NonarchimedeanAddGroup G
U : Set (Completion G)
hU : U ∈ 𝓝 0
C : Set (Completion G)
C_subset_U : id C ⊆ U
hC : C ∈ 𝓝 0
C_closed : IsClosed C
this✝ : ⇑toCompl ⁻¹' C ∈ 𝓝 0
W : OpenAddSubgroup G
hCW : ↑W ⊆ ⇑toCompl ⁻¹' C
V : Set (Completion G) := ⋯
this : IsOpen V
⊢ ↑{ toAddSubgroup := (map toCompl ↑W).topologicalClosure, isOpen' := this } ⊆ U

Tactic:
suffices V ⊆ C from this.trans C_subset_U

Goal state after:
case h
G : Type u_1
inst✝³ : AddGroup G
inst✝² : UniformSpace G
inst✝¹ : IsUniformAddGroup G
inst✝ : NonarchimedeanAddGroup G
U : Set (Completion G)
hU : U ∈ 𝓝 0
C : Set (Completion G)
C_subset_U : id C ⊆ U
hC : C ∈ 𝓝 0
C_closed : IsClosed C
this✝ : ⇑toCompl ⁻¹' C ∈ 𝓝 0
W : OpenAddSubgroup G
hCW : ↑W ⊆ ⇑toCompl ⁻¹' C
V : Set (Completion G) := ↑(map toCompl ↑W).topologicalClosure
this : IsOpen V
⊢ V ⊆ C
Module: Mathlib.NumberTheory.Padics.MahlerBasis

Goal state before:
pp: case refine_1
p : ℕ
hp : Fact (Nat.Prime p)
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : Module ℤ_[p] E
inst✝¹ : IsBoundedSMul ℤ_[p] E
inst✝ : IsUltrametricDist E
f : C(ℤ_[p], E)
s t : ℕ
hst : ∀ (x y : ℤ_[p]), ‖x - y‖ ≤ ↑p ^ (-↑t) → ‖f x - f y‖ ≤ ‖f‖ / ↑p ^ s
n i : ℕ
hi : i < p ^ t - 1
this : 0 < (p ^ t).choose (i + 1)
⊢ 1 ≤ padicValNat p ((p ^ t).choose (i + 1))

Tactic:
exact one_le_padicValNat_of_dvd this.ne' <| hp.out.dvd_choose_pow (by lia) (by omega)

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : Module ℤ_[p] E
inst✝¹ : IsBoundedSMul ℤ_[p] E
inst✝ : IsUltrametricDist E
f : C(ℤ_[p], E)
s t : ℕ
hst : ∀ (x y : ℤ_[p]), ‖x - y‖ ≤ ↑p ^ (-↑t) → ‖f x - f y‖ ≤ ‖f‖ / ↑p ^ s
n : ℕ
⊢ ‖Δ_[1]^[n + s * p ^ t] (⇑f) 0‖ ≤ ‖f‖ / ↑p ^ s

Tactic:
suffices ∀ {k : ℕ}, k ≤ s → ‖Δ_[1]^[n + k * p ^ t] f 0‖ ≤ ‖f‖ / p ^ k from this le_rfl

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : Module ℤ_[p] E
inst✝¹ : IsBoundedSMul ℤ_[p] E
inst✝ : IsUltrametricDist E
f : C(ℤ_[p], E)
s t : ℕ
hst : ∀ (x y : ℤ_[p]), ‖x - y‖ ≤ ↑p ^ (-↑t) → ‖f x - f y‖ ≤ ‖f‖ / ↑p ^ s
n : ℕ
⊢ ∀ {k : ℕ}, k ≤ s → ‖Δ_[1]^[n + k * p ^ t] (⇑f) 0‖ ≤ ‖f‖ / ↑p ^ k
Module: Mathlib.NumberTheory.Padics.MahlerBasis

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : Module ℤ_[p] E
inst✝¹ : IsBoundedSMul ℤ_[p] E
inst✝ : IsUltrametricDist E
f : C(ℤ_[p], E)
s t : ℕ
hst : ∀ (x y : ℤ_[p]), ‖x - y‖ ≤ ↑p ^ (-↑t) → ‖f x - f y‖ ≤ ‖f‖ / ↑p ^ s
n : ℕ
⊢ ‖Δ_[1]^[n + s * p ^ t] (⇑f) 0‖ ≤ ‖f‖ / ↑p ^ s

Tactic:
suffices ∀ {k : ℕ}, k ≤ s → ‖Δ_[1]^[n + k * p ^ t] f 0‖ ≤ ‖f‖ / p ^ k from this le_rfl
  intro k hk
  induction k generalizing n with
  | zero => -- base case just says that `‖Δ^[·] (⇑f) 0‖` is bounded by `‖f‖`
    simpa only [zero_mul, pow_zero, add_zero, div_one] using norm_fwdDiff_iter_apply_le 1 f 0 n
  | succ k IH => -- induction is the "step 2" lemma above
    rw [add_mul, one_mul, ← add_assoc]
    refine (bojanic_mahler_step2 hst (n + k * p ^ t)).trans (max_le ?_ ?_)
    · rw [← coe_nnnorm, ← NNReal.coe_natCast, ← NNReal.coe_pow, ← NNReal.coe_div, NNReal.coe_le_coe]
      refine Finset.sup_le fun j _ ↦ ?_
      rw [pow_succ, ← div_div, div_le_div_iff_of_pos_right (mod_cast hp.out.pos), add_right_comm]
      exact_mod_cast IH (n + (j + 1)) (by lia)
    · exact div_le_div_of_nonneg_left (norm_nonneg _)
        (mod_cast pow_pos hp.out.pos _) (mod_cast pow_le_pow_right₀ hp.out.one_le hk)

Goal state after:
Module: Mathlib.Topology.UniformSpace.ProdApproximation

Goal state before:
pp: X✝ : Type u_1
Y✝ : Type u_2
R✝ : Type u_3
V : Type u_4
inst✝¹³ : TopologicalSpace X✝
inst✝¹² : TotallyDisconnectedSpace X✝
inst✝¹¹ : T2Space X✝
inst✝¹⁰ : CompactSpace X✝
inst✝⁹ : TopologicalSpace Y✝
inst✝⁸ : CompactSpace Y✝
inst✝⁷ : AddCommGroup V
inst✝⁶ : UniformSpace V
inst✝⁵ : IsUniformAddGroup V
S : Set (V × V)
X : Type u_5
Y : Type u_6
R : Type u_7
inst✝⁴ : TopologicalSpace X
inst✝³ : TopologicalSpace Y
inst✝² : CommRing R
inst✝¹ : TopologicalSpace R
inst✝ : IsTopologicalRing R
f : C(X, R)
g g' : C(Y, R)
⊢ f.comp fst * (g + g').comp snd = f.comp fst * g.comp snd + f.comp fst * g'.comp snd

Tactic:
ext; simp [mul_add]

Goal state after:
Module: Mathlib.NumberTheory.Pell

Goal state before:
pp: d : ℤ
a : Solution₁ d
⊢ a.x ^ 2 = 1 + d * a.y ^ 2

Tactic:
rw [← a.prop]; ring

Goal state after:
Module: Mathlib.NumberTheory.Pell

Goal state before:
pp: d : ℤ
a : Solution₁ d
⊢ d * a.y ^ 2 = a.x ^ 2 - 1

Tactic:
rw [← a.prop]; ring

Goal state after:
Module: Mathlib.NumberTheory.Pell

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

Tactic:
obtain ⟨n, hn⟩ := h.eq_pow_of_nonneg hbx hby

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