mathlib-initiative/mathlib-tactics huggingface dataset:
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 compactSet K, ∏ w, ENNReal.ofReal (x ↑w) =
    2 ^ nrRealPlaces K * ENNReal.ofReal (2 * Real.pi) ^ nrComplexPlaces K *
      ∫⁻ (x : realSpace K) in normAtAllPlaces '' normAtAllPlaces ⁻¹' ↑expMapBasis '' interior (paramSet K),
        ∏ w, ENNReal.ofReal (x ↑w)

Tactic:
normAtAllPlaces_image_preimage_expMapBasis,

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) =
    2 ^ nrRealPlaces K * ENNReal.ofReal (2 * Real.pi) ^ nrComplexPlaces K *
      ∫⁻ (x : realSpace K) in ↑expMapBasis '' interior (paramSet K), ∏ w, ENNReal.ofReal (x ↑w)
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal

Goal state before:
pp: case refine_2
m p : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst✝² : Field K
inst✝¹ : NumberField K
P : Ideal (𝓞 K)
hP₁ : P.IsPrime
hP₂ : P.LiesOver 𝒑
inst✝ : NeZero m
hK : IsCyclotomicExtension {m} ℚ K
hm : ¬p ∣ m
ζ : 𝓞 K := ⋯.toInteger
h₁ : ¬p ∣ exponent ζ
h₂ :
  Irreducible ↑((primesOverSpanEquivMonicFactorsMod h₁) ⟨P, ⋯⟩) ∧
    (↑((primesOverSpanEquivMonicFactorsMod h₁) ⟨P, ⋯⟩)).Monic ∧
      ↑((primesOverSpanEquivMonicFactorsMod h₁) ⟨P, ⋯⟩) ∣ Polynomial.map (Int.castRingHom (ZMod p)) (minpoly ℤ ζ)
h₃ :
  P.ramificationIdx ℤ =
    multiplicity (↑((primesOverSpanEquivMonicFactorsMod h₁) ⟨P, ⋯⟩))
      (Polynomial.map (Int.castRingHom (ZMod p)) (minpoly ℤ ζ))
⊢ ↑1 ≤
    emultiplicity (↑((primesOverSpanEquivMonicFactorsMod h₁) ⟨P, ⋯⟩))
      (Polynomial.map (Int.castRingHom (ZMod p)) (minpoly ℤ ζ))

Tactic:
· rw [ENat.natCast_one]
    exact Order.one_le_iff_pos.mpr <| emultiplicity_pos_of_dvd h₂.2.2

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

Goal state before:
pp: K : Type u_1
𝒪 : Type u_2
inst✝⁴ : Field K
inst✝³ : NumberField K
inst✝² : CommRing 𝒪
inst✝¹ : Algebra 𝒪 K
inst✝ : IsIntegralClosure 𝒪 ℤ K
H : Module.finrank ℚ K ≠ 1
p : ℕ
hp1 : Nat.Prime p
hp2 : ¬Algebra.IsUnramifiedIn 𝒪 (Ideal.span {↑p})
⊢ ∃ P, ∃ (x : P.IsMaximal), ¬Algebra.IsUnramifiedAt ℤ P

Tactic:
have := (IsIntegralClosure.algebraMap_injective 𝒪 ℤ K).isDomain

Goal state after:
K : Type u_1
𝒪 : Type u_2
inst✝⁴ : Field K
inst✝³ : NumberField K
inst✝² : CommRing 𝒪
inst✝¹ : Algebra 𝒪 K
inst✝ : IsIntegralClosure 𝒪 ℤ K
H : Module.finrank ℚ K ≠ 1
p : ℕ
hp1 : Nat.Prime p
hp2 : ¬Algebra.IsUnramifiedIn 𝒪 (Ideal.span {↑p})
this : IsDomain 𝒪
⊢ ∃ P, ∃ (x : P.IsMaximal), ¬Algebra.IsUnramifiedAt ℤ P
Module: Mathlib.NumberTheory.NumberField.ExistsRamified

Goal state before:
pp: K : Type u_1
𝒪 : Type u_2
inst✝⁴ : Field K
inst✝³ : NumberField K
inst✝² : CommRing 𝒪
inst✝¹ : Algebra 𝒪 K
inst✝ : IsIntegralClosure 𝒪 ℤ K
H : Module.finrank ℚ K ≠ 1
p : ℕ
hp1 : Nat.Prime p
hp2 : ¬Algebra.IsUnramifiedIn 𝒪 (Ideal.span {↑p})
this✝¹ : IsDomain 𝒪
this✝ : IsDedekindDomain 𝒪
this : Module.IsTorsionFree ℤ 𝒪
⊢ ∃ P, ∃ (x : P.IsMaximal), ¬Algebra.IsUnramifiedAt ℤ P

Tactic:
have := IsIntegralClosure.isIntegral_algebra ℤ (A := 𝒪) K

Goal state after:
K : Type u_1
𝒪 : Type u_2
inst✝⁴ : Field K
inst✝³ : NumberField K
inst✝² : CommRing 𝒪
inst✝¹ : Algebra 𝒪 K
inst✝ : IsIntegralClosure 𝒪 ℤ K
H : Module.finrank ℚ K ≠ 1
p : ℕ
hp1 : Nat.Prime p
hp2 : ¬Algebra.IsUnramifiedIn 𝒪 (Ideal.span {↑p})
this✝² : IsDomain 𝒪
this✝¹ : IsDedekindDomain 𝒪
this✝ : Module.IsTorsionFree ℤ 𝒪
this : Algebra.IsIntegral ℤ 𝒪
⊢ ∃ P, ∃ (x : P.IsMaximal), ¬Algebra.IsUnramifiedAt ℤ P
Module: Mathlib.NumberTheory.NumberField.ExistsRamified

Goal state before:
pp: K : Type u_1
𝒪 : Type u_2
inst✝⁵ : Field K
inst✝⁴ : NumberField K
inst✝³ : CommRing 𝒪
inst✝² : Algebra 𝒪 K
inst✝¹ : IsIntegralClosure 𝒪 ℤ K
inst✝ : IsGalois ℚ K
H : 1 < Module.finrank ℚ K
⊢ ∃ p, Nat.Prime p ∧ ∀ (P : Ideal 𝒪) (x : P.IsPrime), ↑p ∈ P → ¬Algebra.IsUnramifiedAt ℤ P

Tactic:
have := (IsIntegralClosure.algebraMap_injective 𝒪 ℤ K).isDomain

Goal state after:
K : Type u_1
𝒪 : Type u_2
inst✝⁵ : Field K
inst✝⁴ : NumberField K
inst✝³ : CommRing 𝒪
inst✝² : Algebra 𝒪 K
inst✝¹ : IsIntegralClosure 𝒪 ℤ K
inst✝ : IsGalois ℚ K
H : 1 < Module.finrank ℚ K
this : IsDomain 𝒪
⊢ ∃ p, Nat.Prime p ∧ ∀ (P : Ideal 𝒪) (x : P.IsPrime), ↑p ∈ P → ¬Algebra.IsUnramifiedAt ℤ P
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal

Goal state before:
pp: n m p k : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst✝² : Field K
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {n} ℚ K
hn : n = p ^ (k + 1) * m
hm : ¬p ∣ m
this✝³ : IsAbelianGalois ℚ K
this✝² : NeZero m
this✝¹ : NeZero n
ζ : K := zeta n ℚ K
hζ : IsPrimitiveRoot (zeta n ℚ K) n
ζₘ : K := ζ ^ p ^ (k + 1)
hζₘ : IsPrimitiveRoot (zeta n ℚ K ^ p ^ (k + 1)) m
Fₘ : IntermediateField ℚ K := ℚ⟮ζₘ⟯
this✝ : IsCyclotomicExtension {m} ℚ ↥Fₘ
Pₘ : Ideal (𝓞 ↥Fₘ)
left✝ : Pₘ.IsMaximal
right✝¹ : Pₘ.LiesOver 𝒑
ζₚ : K := ζ ^ m
hζₚ : IsPrimitiveRoot (zeta n ℚ K ^ m) (p ^ (k + 1))
Fₚ : IntermediateField ℚ K := ℚ⟮ζₚ⟯
this : IsCyclotomicExtension {p ^ (k + 1)} ℚ ↥Fₚ
Pₚ : Ideal (𝓞 ↥Fₚ)
hP₁ : Pₚ.IsMaximal
right✝ : Pₚ.LiesOver 𝒑
⊢ Pₚ.ramificationIdxIn (𝓞 K) * Pₘ.inertiaDegIn (𝓞 K) * (Pₘ.primesOver (𝓞 K)).ncard = 1

Tactic:
have h_main : Module.finrank ℚ Fₘ * Module.finrank ℚ Fₚ = Module.finrank ℚ K := by
    rw [finrank m, finrank (p ^ (k + 1)), finrank n, hn, mul_comm, Nat.totient_mul]
    exact Nat.Coprime.pow_left (k + 1) (by rwa [hp.out.coprime_iff_not_dvd])

Goal state after:
n m p k : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst✝² : Field K
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {n} ℚ K
hn : n = p ^ (k + 1) * m
hm : ¬p ∣ m
this✝³ : IsAbelianGalois ℚ K
this✝² : NeZero m
this✝¹ : NeZero n
ζ : K := zeta n ℚ K
hζ : IsPrimitiveRoot (zeta n ℚ K) n
ζₘ : K := ζ ^ p ^ (k + 1)
hζₘ : IsPrimitiveRoot (zeta n ℚ K ^ p ^ (k + 1)) m
Fₘ : IntermediateField ℚ K := ℚ⟮ζₘ⟯
this✝ : IsCyclotomicExtension {m} ℚ ↥Fₘ
Pₘ : Ideal (𝓞 ↥Fₘ)
left✝ : Pₘ.IsMaximal
right✝¹ : Pₘ.LiesOver 𝒑
ζₚ : K := ζ ^ m
hζₚ : IsPrimitiveRoot (zeta n ℚ K ^ m) (p ^ (k + 1))
Fₚ : IntermediateField ℚ K := ℚ⟮ζₚ⟯
this : IsCyclotomicExtension {p ^ (k + 1)} ℚ ↥Fₚ
Pₚ : Ideal (𝓞 ↥Fₚ)
hP₁ : Pₚ.IsMaximal
right✝ : Pₚ.LiesOver 𝒑
h_main : Module.finrank ℚ ↥Fₘ * Module.finrank ℚ ↥Fₚ = Module.finrank ℚ K
⊢ Pₚ.ramificationIdxIn (𝓞 K) * Pₘ.inertiaDegIn (𝓞 K) * (Pₘ.primesOver (𝓞 K)).ncard = 1
Module: Mathlib.NumberTheory.NumberField.ExistsRamified

Goal state before:
pp: K : Type u_1
𝒪 : Type u_2
inst✝⁵ : Field K
inst✝⁴ : NumberField K
inst✝³ : CommRing 𝒪
inst✝² : Algebra 𝒪 K
inst✝¹ : IsIntegralClosure 𝒪 ℤ K
inst✝ : IsGalois ℚ K
H : 1 < Module.finrank ℚ K
this✝⁶ : IsDomain 𝒪
this✝⁵ : IsDedekindDomain 𝒪
this✝⁴ : IsFractionRing 𝒪 K
this✝³ : Module.Finite ℤ 𝒪
this✝² : CharZero 𝒪
this✝¹ : MulSemiringAction Gal(K/ℚ) 𝒪 := IsIntegralClosure.MulSemiringAction ℤ ℚ K 𝒪
this✝ : IsGaloisGroup Gal(K/ℚ) ℤ 𝒪
P : Ideal 𝒪
w✝ : P.IsMaximal
hP' : ¬Algebra.IsUnramifiedAt ℤ P
p : ℤ
hp : Ideal.under ℤ P = Ideal.span {p}
hp0 : p ≠ 0
this : Prime p
Q : Ideal 𝒪
x✝ : Q.IsPrime
hQ : ↑p.natAbs ∈ Q
⊢ (algebraMap ℤ 𝒪) ↑p.natAbs ∈ Q

Tactic:
simpa using hQ

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
α β : K
⊢ house (α + β) ≤ house α + house β

Tactic:
simp only [house, map_add]

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
α β : K
⊢ ‖(canonicalEmbedding K) α + (canonicalEmbedding K) β‖ ≤ ‖(canonicalEmbedding K) α‖ + ‖(canonicalEmbedding K) β‖
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 : α
lin_0 : ∀ (u : K →+* ℂ), ∑ r, ∑ l, ↑(a' K a k l r u) * ↑(x (l, r)) = 0
this : 0 = ∑ u, (∑ r, ∑ l, ↑(a' K a k l r u) * ↑(x (l, r))) * (newBasis K) u
| 0 = ∑ u, (∑ r, ∑ l, ↑(a' K a k l r u) * ↑(x (l, r))) * (newBasis K) u

Tactic:
enter [

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 : asiegel K a *ᵥ x = 0
k : α
lin_0 : ∀ (u : K →+* ℂ), ∑ r, ∑ l, ↑(a' K a k l r u) * ↑(x (l, r)) = 0
this : 0 = ∑ u, (∑ r, ∑ l, ↑(a' K a k l r u) * ↑(x (l, r))) * (newBasis K) u
| 0 = ∑ u, (∑ r, ∑ l, ↑(a' K a k l r u) * ↑(x (l, r))) * (newBasis K) u
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 : α
lin_0 : ∀ (u : K →+* ℂ), ∑ r, ∑ l, ↑(a' K a k l r u) * ↑(x (l, r)) = 0
this : 0 = ∑ y, ∑ x_1, (∑ l, ↑(a' K a k l y x_1) * ↑(x (l, y))) * (newBasis K) x_1
r : K →+* ℂ
| ∑ x_1, (∑ l, ↑(a' K a k l r x_1) * ↑(x (l, r))) * (newBasis K) x_1 =
    ∑ l, ↑(x (l, r)) * ∑ u, ↑(a' K a k l r u) * (newBasis K) u

Tactic:
enter [

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 : asiegel K a *ᵥ x = 0
k : α
lin_0 : ∀ (u : K →+* ℂ), ∑ r, ∑ l, ↑(a' K a k l r u) * ↑(x (l, r)) = 0
this : 0 = ∑ y, ∑ x_1, (∑ l, ↑(a' K a k l y x_1) * ↑(x (l, y))) * (newBasis K) x_1
r : K →+* ℂ
| ∑ x_1, (∑ l, ↑(a' K a k l r x_1) * ↑(x (l, r))) * (newBasis K) x_1 =
    ∑ l, ↑(x (l, r)) * ∑ u, ↑(a' K a k l r u) * (newBasis K) u
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
⊢ ‖x - y‖ ≤ (↑n * max 1 ‖A‖) ^ e

Tactic:
have n_mul_norm_A_pow_e_nonneg : 0 ≤ (n * max 1 ‖A‖) ^ e := by positivity

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
⊢ ‖x - y‖ ≤ (↑n * max 1 ‖A‖) ^ e
Module: Mathlib.NumberTheory.SiegelsLemma

Goal state before:
pp: case left
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : Fintype β
A : Matrix α β ℤ
hn : m < n
hm : 0 < m
x : β → ℤ
hxT : 0 ≤ x ∧ x ≤ B'
y : β → ℤ
hyT : 0 ≤ y ∧ y ≤ B'
hneq : x ≠ y
hfeq : A *ᵥ x = A *ᵥ y
n_mul_norm_A_pow_e_nonneg : 0 ≤ (↑n * max 1 ‖A‖) ^ e
i : β
j : Unit
⊢ (fun x ↦ ↑⌊(↑n * max 1 ‖A‖) ^ ↑(Rat.divInt (↑m) (subNatNat n m))⌋₊) i ≤
    x i + ↑⌊(↑n * max 1 ‖A‖) ^ ↑(Rat.divInt (↑m) (subNatNat n m))⌋₊

Tactic:
simp only [le_add_iff_nonneg_left]

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

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

Tactic:
← Ring.factorial_nsmul_multichoose_eq_ascPochhammer,

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

Goal state before:
pp: case hg
p : ℕ
hp : Fact (Nat.Prime p)
S : SeminormedRing ℂ_[p] := NormedRing.toSeminormedRing
⊢ UniformContinuous Valued.v.norm

Tactic:
let := S.toNonUnitalSeminormedRing.toSeminormedAddCommGroup.toSeminormedAddGroup

Goal state after:
case hg
p : ℕ
hp : Fact (Nat.Prime p)
S : SeminormedRing ℂ_[p] := NormedRing.toSeminormedRing
this : SeminormedAddGroup ℂ_[p] := SeminormedAddCommGroup.toSeminormedAddGroup
⊢ UniformContinuous Valued.v.norm
Module: Mathlib.NumberTheory.Padics.HeightOneSpectrum

Goal state before:
pp: case refine_1
R : Type u_2
inst✝⁴ : CommRing R
inst✝³ : Algebra R ℚ
inst✝² : IsIntegralClosure R ℤ ℚ
inst✝¹ : IsDedekindDomain R
inst✝ : IsFractionRing R ℚ
v : HeightOneSpectrum R
x : HeightOneSpectrum.adicCompletion ℚ v
hx : x ∈ ↑(HeightOneSpectrum.adicCompletionIntegers ℚ v)
⊢ (padicEquiv v) x ∈ ↑(subring ↑(primesEquiv v))

Tactic:
← adicCompletionIntegers.coe_padicIntEquiv_apply v ⟨x, hx⟩

Goal state after:
case refine_1
R : Type u_2
inst✝⁴ : CommRing R
inst✝³ : Algebra R ℚ
inst✝² : IsIntegralClosure R ℤ ℚ
inst✝¹ : IsDedekindDomain R
inst✝ : IsFractionRing R ℚ
v : HeightOneSpectrum R
x : HeightOneSpectrum.adicCompletion ℚ v
hx : x ∈ ↑(HeightOneSpectrum.adicCompletionIntegers ℚ v)
⊢ ↑((adicCompletionIntegers.padicIntEquiv v) ⟨x, hx⟩) ∈ ↑(subring ↑(primesEquiv v))
Module: Mathlib.NumberTheory.RamificationInertia.HilbertTheory

Goal state before:
pp: case refine_1
K : Type u_2
L : Type u_3
B : Type u_4
inst✝¹⁵ : Field K
inst✝¹⁴ : Field L
inst✝¹³ : Algebra K L
inst✝¹² : CommRing B
P : Ideal B
D : Type u_5
inst✝¹¹ : Field D
inst✝¹⁰ : Algebra D L
inst✝⁹ : MulSemiringAction Gal(L/K) B
G : Type u_7
inst✝⁸ : Group G
inst✝⁷ : Finite G
inst✝⁶ : MulSemiringAction G L
inst✝⁵ : IsGaloisGroup G K L
inst✝⁴ : MulSemiringAction G B
inst✝³ : Algebra B L
inst✝² : IsFractionRing B L
inst✝¹ : SMulDistribClass Gal(L/K) B L
inst✝ : SMulDistribClass G B L
h : IsGaloisGroup (↥(stabilizer G P)) D L
x✝¹ : G
x✝ : B
⊢ (algebraMap B L) ((IsGaloisGroup.mulEquivAlgEquiv G K L) x✝¹ • x✝) = (algebraMap B L) (x✝¹ • x✝)

Tactic:
simp [algebraMap.smul']

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

Goal state before:
pp: case refine_1
K : Type u_2
L : Type u_3
B : Type u_4
inst✝¹⁵ : Field K
inst✝¹⁴ : Field L
inst✝¹³ : Algebra K L
inst✝¹² : CommRing B
P : Ideal B
E : Type u_6
inst✝¹¹ : Field E
inst✝¹⁰ : Algebra E L
inst✝⁹ : MulSemiringAction Gal(L/K) B
G : Type u_7
inst✝⁸ : Group G
inst✝⁷ : Finite G
inst✝⁶ : MulSemiringAction G L
inst✝⁵ : IsGaloisGroup G K L
inst✝⁴ : MulSemiringAction G B
inst✝³ : Algebra B L
inst✝² : IsFractionRing B L
inst✝¹ : SMulDistribClass Gal(L/K) B L
inst✝ : SMulDistribClass G B L
h : IsGaloisGroup (↥(inertia G P)) E L
x✝¹ : G
x✝ : B
⊢ (algebraMap B L) ((IsGaloisGroup.mulEquivAlgEquiv G K L) x✝¹ • x✝) = (algebraMap B L) (x✝¹ • x✝)

Tactic:
simp [algebraMap.smul']

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 % π = 0
heq : p = π ^ k * q
hπ : v ↑π < 1 ∧ ¬π = 0
this : v ((algebraMap K[X] K⟮X⟯) (q % π)) = 1 ∧ v ((algebraMap K[X] K⟮X⟯) (π * (q / π))) < 1
⊢ v ((algebraMap K[X] K⟮X⟯) (q % π) + (algebraMap K[X] K⟮X⟯) (π * (q / π))) = 1

Tactic:
obtain ⟨h₁, h₂⟩ := this

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 % π = 0
heq : p = π ^ k * q
hπ : v ↑π < 1 ∧ ¬π = 0
h₁ : v ((algebraMap K[X] K⟮X⟯) (q % π)) = 1
h₂ : v ((algebraMap K[X] K⟮X⟯) (π * (q / π))) < 1
⊢ v ((algebraMap K[X] K⟮X⟯) (q % π) + (algebraMap K[X] K⟮X⟯) (π * (q / π))) = 1
Module: Mathlib.NumberTheory.SelbergSieve

Goal state before:
pp: s : BoundingSieve
muPlus : ℕ → ℝ
h : IsUpperMoebius muPlus
hμ : ∀ (n : ℕ), (if n = 1 then 1 else 0) ≤ ∑ d ∈ n.divisors, muPlus d
⊢ (∑ d ∈ s.support, s.weights d * if s.prodPrimes.gcd d = 1 then 1 else 0) ≤
    ∑ n ∈ s.support, s.weights n * ∑ d ∈ (s.prodPrimes.gcd n).divisors, muPlus d

Tactic:
gcongr with n

Goal state after:
case hbc
s : BoundingSieve
muPlus : ℕ → ℝ
h : IsUpperMoebius muPlus
hμ : ∀ (n : ℕ), (if n = 1 then 1 else 0) ≤ ∑ d ∈ n.divisors, muPlus d
n : ℕ
a✝ : n ∈ s.support
⊢ (if s.prodPrimes.gcd n = 1 then 1 else 0) ≤ ∑ d ∈ (s.prodPrimes.gcd n).divisors, muPlus d
Module: Mathlib.NumberTheory.RamificationInertia.Basic

Goal state before:
pp: 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)
⊢ finrank (R ⧸ p) (S ⧸ map f p) = finrank K L

Tactic:
let b' : ι → S := fun i => (Ideal.Quotient.mk_surjective (b i)).choose

Goal state after:
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
⊢ finrank (R ⧸ p) (S ⧸ map f p) = finrank K L
Module: Mathlib.NumberTheory.SumFourSquares

Goal state before:
pp: m a b c d : ℤ
h : a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = 2 * m
this :
  ∀ (f : Fin 4 → ZMod 2),
    f 0 ^ 2 + f 1 ^ 2 + f 2 ^ 2 + f 3 ^ 2 = 0 →
      ∃ i, f i ^ 2 + f ((swap i 0) 1) ^ 2 = 0 ∧ f ((swap i 0) 2) ^ 2 + f ((swap i 0) 3) ^ 2 = 0
f : Fin 4 → ℤ := ![a, b, c, d]
i : Fin 4
σ : Perm (Fin 4) := swap i 0
hσ : ↑(f i) ^ 2 + ↑(f (σ 1)) ^ 2 = 0 ∧ ↑(f (σ 2)) ^ 2 + ↑(f (σ 3)) ^ 2 = 0
x : ℤ
hx : f (σ 0) ^ 2 + f (σ 1) ^ 2 = 2 * x
y : ℤ
hy : f (σ 2) ^ 2 + f (σ 3) ^ 2 = 2 * y
⊢ 2 * (x + y) = a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2

Tactic:
mul_add

Goal state after:
m a b c d : ℤ
h : a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = 2 * m
this :
  ∀ (f : Fin 4 → ZMod 2),
    f 0 ^ 2 + f 1 ^ 2 + f 2 ^ 2 + f 3 ^ 2 = 0 →
      ∃ i, f i ^ 2 + f ((swap i 0) 1) ^ 2 = 0 ∧ f ((swap i 0) 2) ^ 2 + f ((swap i 0) 3) ^ 2 = 0
f : Fin 4 → ℤ := ![a, b, c, d]
i : Fin 4
σ : Perm (Fin 4) := swap i 0
hσ : ↑(f i) ^ 2 + ↑(f (σ 1)) ^ 2 = 0 ∧ ↑(f (σ 2)) ^ 2 + ↑(f (σ 3)) ^ 2 = 0
x : ℤ
hx : f (σ 0) ^ 2 + f (σ 1) ^ 2 = 2 * x
y : ℤ
hy : f (σ 2) ^ 2 + f (σ 3) ^ 2 = 2 * y
⊢ 2 * x + 2 * y = a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2
Module: Mathlib.NumberTheory.SumFourSquares

Goal state before:
pp: 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
⊢ ∃ a b c d, a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = p

Tactic:
have hm : ∃ m < p, 0 < m ∧ ∃ a b c d : ℕ, a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = m * p := by
    obtain ⟨a, b, k, hk₀, hkp, hk⟩ := exists_sq_add_sq_add_one_eq_mul p
    refine ⟨k, hkp, hk₀, a, b, 1, 0, ?_⟩
    simpa

Goal state after:
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
⊢ ∃ a b c d, a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = p
Module: Mathlib.NumberTheory.SumTwoSquares

Goal state before:
pp: m n : ℕ
hd : m ∣ n
hs : IsSquare (-1)
f : ZMod n →+* ZMod m := castHom hd (ZMod m)
⊢ IsSquare (-1)

Tactic:
← map_one f,

Goal state after:
m n : ℕ
hd : m ∣ n
hs : IsSquare (-1)
f : ZMod n →+* ZMod m := castHom hd (ZMod m)
⊢ IsSquare (-f 1)
Module: Mathlib.NumberTheory.RamificationInertia.Basic

Goal state before:
pp: R : Type u
inst✝² : CommRing R
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
p : Ideal R
P : Ideal S
hfp : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
i : ℕ
a : S
a_mem : a ∈ P ^ i
x : R ⧸ p
y : S ⧸ P
⊢ p.quotientToQuotientRangePowQuotSuccAux P a_mem (x • y) =
    (RingHom.id (R ⧸ p)) x • p.quotientToQuotientRangePowQuotSuccAux P a_mem y

Tactic:
induction x, y using Quotient.inductionOn₂' with | _ x y
    simp only [Submodule.Quotient.mk''_eq_mk, RingHom.id_apply,
      quotientToQuotientRangePowQuotSuccAux_mk]
    refine congr_arg Submodule.Quotient.mk ?_
    ext
    simp only [map_mul, Quotient.mk_eq_mk, Submodule.coe_smul_of_tower,
      Algebra.smul_def, Quotient.algebraMap_quotient_pow_ramificationIdx]
    ring

Goal state after:
Module: Mathlib.NumberTheory.SumFourSquares

Goal state before:
pp: n : ℕ
⊢ ∃ a b c d, a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = n

Tactic:
induction n using Nat.recOnMul with

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

Goal state before:
pp: n : ℕ
m : ℝ
hm : 2 ≤ m
⊢ (1 - 1 / m)⁻¹ * (1 / m ^ (n + 1)!) ≤ 2 * (1 / m ^ (n + 1)!)

Tactic:
by
      -- the second factors coincide (and are non-negative),
      -- the first factors satisfy the inequality `sub_one_div_inv_le_two`
      gcongr; exact sub_one_div_inv_le_two hm

Goal state after:
Module: Mathlib.NumberTheory.WellApproximable

Goal state before:
pp: A : Type u_1
inst✝ : SeminormedCommGroup A
a : A
n : ℕ
δ : ℝ
han : (orderOf a).Coprime n
⊢ (fun x ↦ a • x) '' ⋃ x ∈ {y | orderOf y = n}, ball x δ ⊆ ⋃ x ∈ {y | orderOf y = orderOf a * n}, ball x δ

Tactic:
image_iUnion₂,

Goal state after:
A : Type u_1
inst✝ : SeminormedCommGroup A
a : A
n : ℕ
δ : ℝ
han : (orderOf a).Coprime n
⊢ ⋃ i ∈ {y | orderOf y = n}, (fun x ↦ a • x) '' ball i δ ⊆ ⋃ x ∈ {y | orderOf y = orderOf a * n}, ball x δ
Module: Mathlib.NumberTheory.WellApproximable

Goal state before:
pp: A : Type u_1
inst✝ : SeminormedCommGroup A
a : A
n : ℕ
δ : ℝ
hn : 0 < n
han : orderOf a ^ 2 ∣ n
⊢ (fun x ↦ a • x) '' ⋃ x ∈ {y | orderOf y = n}, ball x δ = ⋃ x ∈ {y | orderOf y = n}, ball x δ

Tactic:
image_iUnion₂,

Goal state after:
A : Type u_1
inst✝ : SeminormedCommGroup A
a : A
n : ℕ
δ : ℝ
hn : 0 < n
han : orderOf a ^ 2 ∣ n
⊢ ⋃ i ∈ {y | orderOf y = n}, (fun x ↦ a • x) '' ball i δ = ⋃ x ∈ {y | orderOf y = n}, ball x δ
Module: Mathlib.NumberTheory.WellApproximable

Goal state before:
pp: A : Type u_1
inst✝ : SeminormedCommGroup A
a : A
n : ℕ
δ : ℝ
hn : 0 < n
han : orderOf a ^ 2 ∣ n
⊢ a • approxOrderOf A n δ = approxOrderOf A n δ

Tactic:
by
  simp_rw [approxOrderOf, thickening_eq_biUnion_ball, ← image_smul, image_iUnion₂, image_smul,
    smul_ball'', smul_eq_mul, mem_ofPred_eq]
  replace han : ∀ {b : A}, orderOf b = n → orderOf (a * b) = n := by
    intro b hb
    rw [← hb] at han hn
    rw [sq] at han
    rwa [(Commute.all a b).orderOf_mul_eq_right_of_forall_prime_mul_dvd (orderOf_pos_iff.mp hn)
      fun p _ hp' => dvd_trans (mul_dvd_mul_right hp' <| orderOf a) han]
  let f : {b : A | orderOf b = n} → {b : A | orderOf b = n} := fun b => ⟨a * b, han b.property⟩
  have hf : Surjective f := by
    rintro ⟨b, hb⟩
    refine ⟨⟨a⁻¹ * b, ?_⟩, ?_⟩
    · rw [mem_ofPred_eq, ← orderOf_inv, mul_inv_rev, inv_inv, mul_comm]
      apply han
      simpa
    · simp only [f, mul_inv_cancel_left]
  simpa only [mem_ofPred_eq, Subtype.coe_mk, iUnion_coe_set] using
    hf.iUnion_comp fun b => ball (b : A) δ

Goal state after:
Module: Mathlib.Order.Category.FinBoolAlg

Goal state before:
pp: X✝ Y✝ : FinBoolAlg
a₁✝ a₂✝ : X✝ ⟶ Y✝
h : (forget₂ FinBoolAlg FinPartOrd).map a₁✝ = (forget₂ FinBoolAlg FinPartOrd).map a₂✝
x : ↑X✝.toBoolAlg
⊢ (ConcreteCategory.hom a₁✝) x = (ConcreteCategory.hom a₂✝) x

Tactic:
exact CategoryTheory.congr_fun h x

Goal state after: