mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone

Goal state before:
pp: case inl
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
J : ↥(Ideal (𝓞 K))⁰
s : ℝ
hs : 0 ≤ s
⊢ Nat.card { I // ↑J ∣ ↑I ∧ IsPrincipal ↑I ∧ ↑(absNorm ↑I) ≤ s } * torsionOrder K =
    Nat.card { a // mixedEmbedding.norm ↑a ≤ s }

pp: case inr
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
J : ↥(Ideal (𝓞 K))⁰
s : ℝ
hs : s < 0
⊢ Nat.card { I // ↑J ∣ ↑I ∧ IsPrincipal ↑I ∧ ↑(absNorm ↑I) ≤ s } * torsionOrder K =
    Nat.card { a // mixedEmbedding.norm ↑a ≤ s }

Tactic:
· simp_rw [← intNorm_idealSetEquiv_apply, ← Nat.le_floor_iff hs]
    rw [torsionOrder, ← Nat.card_prod]
    refine Nat.card_congr <| @Equiv.ofFiberEquiv _ (γ := Finset.Iic ⌊s⌋₊) _
      (fun I ↦ ⟨absNorm I.1.val.1, Finset.mem_Iic.mpr I.1.prop.2.2⟩)
      (fun a ↦ ⟨intNorm (idealSetEquiv K J a.1).1, Finset.mem_Iic.mpr a.prop⟩) fun ⟨i, hi⟩ ↦ ?_
    simp_rw [Subtype.mk.injEq]
    calc _ ≃ {I : {I : (Ideal (𝓞 K))⁰ // _ ∧ _ ∧ _} // absNorm I.1.1 = i} × torsion K :=
        Equiv.prodSubtypeFstEquivSubtypeProd
      _ ≃ {I : (Ideal (𝓞 K))⁰ // (_ ∧ _ ∧ absNorm I.1 ≤ ⌊s⌋₊) ∧ absNorm I.1 = i}
            × torsion K := Equiv.prodCongrLeft fun _ ↦ (Equiv.subtypeSubtypeEquivSubtypeInter
        (p := fun I : (Ideal (𝓞 K))⁰ ↦ J.1 ∣ I.1 ∧ IsPrincipal I.1 ∧ absNorm I.1 ≤ ⌊s⌋₊)
        (q := fun I ↦ absNorm I.1 = i))
      _ ≃ {I : (Ideal (𝓞 K))⁰ // J.1 ∣ I.1 ∧ IsPrincipal I.1 ∧ absNorm I.1 = i}
            × torsion K := Equiv.prodCongrLeft fun _ ↦ Equiv.subtypeEquivRight fun _ ↦ by grind
      _ ≃ {a : idealSet K J // mixedEmbedding.norm (a : mixedSpace K) = i} :=
            (idealSetEquivNorm K J i).symm
      _ ≃ {a : idealSet K J // intNorm (idealSetEquiv K J a).1 = i} := by
        simp_rw [← intNorm_idealSetEquiv_apply, Nat.cast_inj]
        rfl
      _ ≃ {b : {a : idealSet K J // intNorm (idealSetEquiv K J a).1 ≤ ⌊s⌋₊} //
            intNorm (idealSetEquiv K J b).1 = i} :=
        (Equiv.subtypeSubtypeEquivSubtype fun h ↦ Finset.mem_Iic.mp (h ▸ hi)).symm

Goal state after:
case inr
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
J : ↥(Ideal (𝓞 K))⁰
s : ℝ
hs : s < 0
⊢ Nat.card { I // ↑J ∣ ↑I ∧ IsPrincipal ↑I ∧ ↑(absNorm ↑I) ≤ s } * torsionOrder K =
    Nat.card { a // mixedEmbedding.norm ↑a ≤ s }
Module: Mathlib.NumberTheory.NumberField.Completion.LiesOverInstances

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
x : K
h : (algebraMap K v.Completion) x = { toCompletion := ↑(WithAbs.toAbs (↑v) x) }
⊢ (algebraMap K w.Completion) x = { toCompletion := ↑((algebraMap (WithAbs ↑v) (WithAbs ↑w)) (WithAbs.toAbs (↑v) x)) }

Tactic:
apply Completion.ext

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
x : K
h : (algebraMap K v.Completion) x = { toCompletion := ↑(WithAbs.toAbs (↑v) x) }
⊢ ((algebraMap K w.Completion) x).toCompletion =
    { toCompletion := ↑((algebraMap (WithAbs ↑v) (WithAbs ↑w)) (WithAbs.toAbs (↑v) x)) }.toCompletion
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x✝² x✝¹ : realSpace K
x✝ : { w // w ≠ w₀ }
⊢ (x✝² + x✝¹) ↑x✝ - (↑(↑x✝).mult * ∑ w', (x✝² + x✝¹) w') * (↑(finrank ℚ K))⁻¹ =
    ((fun w ↦ x✝² ↑w - (↑(↑w).mult * ∑ w', x✝² w') * (↑(finrank ℚ K))⁻¹) + fun w ↦
        x✝¹ ↑w - (↑(↑w).mult * ∑ w', x✝¹ w') * (↑(finrank ℚ K))⁻¹)
      x✝

Tactic:
simp [sum_add_distrib]

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x✝² x✝¹ : realSpace K
x✝ : { w // w ≠ w₀ }
⊢ x✝² ↑x✝ + x✝¹ ↑x✝ - ↑(↑x✝).mult * (∑ x, x✝² x + ∑ x, x✝¹ x) * (↑(finrank ℚ K))⁻¹ =
    x✝² ↑x✝ - (↑(↑x✝).mult * ∑ x, x✝² x) * (↑(finrank ℚ K))⁻¹ +
      (x✝¹ ↑x✝ - (↑(↑x✝).mult * ∑ x, x✝¹ x) * (↑(finrank ℚ K))⁻¹)
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
inst✝¹ : NumberField K
inst✝ : NumberField L
⊢ ∑ w ∈ (placesOver L v).toFinset, v.inertiaDeg w = Module.finrank K L

Tactic:
rw [← union_ramifiedPlacesOver_unramifiedPlacesOver L v, toFinset_union,
    sum_union (Set.disjoint_toFinset.2 <| disjoint_ramifiedPlacesOver_unramifiedPlacesOver L v),
    sum_congr rfl (fun _ h ↦ inertiaDeg_eq_two (by simpa using h)),
    sum_congr rfl (fun _ h ↦ inertiaDeg_eq_one (by simpa using h)), sum_const, add_comm]
  simp [← unramifedPlacesOver_ncard_add_eq_finrank L v, mul_comm, ncard_eq_toFinset_card']

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

Goal state before:
pp: K : Type u_1
inst✝² : Field K
θ : 𝓞 K
p : ℕ
inst✝¹ : Fact (Nat.Prime p)
inst✝ : NumberField K
hp : ¬p ∣ exponent θ
h : span {↑p} ≠ ⊥
x✝ : Ideal (𝓞 K)
⊢ x✝ ∈ (span {↑p}).primesOver (𝓞 K) ↔ x✝ ∈ {J | J ∈ normalizedFactors (Ideal.map (algebraMap ℤ (𝓞 K)) (span {↑p}))}

Tactic:
simp [mem_primesOver_iff_mem_normalizedFactors _ h]

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

Goal state before:
pp: 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
⊢ AddSubgroup.map (logEmbedding K) (Subgroup.toAddSubgroup (Subgroup.closure (Set.range u) ⊔ torsion K)) ≤
    AddSubgroup.map (logEmbedding K)
      (Subgroup.toAddSubgroup (Subgroup.closure (Set.range v)) ⊔ Subgroup.toAddSubgroup (torsion K))

Tactic:
← SupHomClass.map_sup

Goal state after:
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
⊢ AddSubgroup.map (logEmbedding K) (Subgroup.toAddSubgroup (Subgroup.closure (Set.range u) ⊔ torsion K)) ≤
    AddSubgroup.map (logEmbedding K) (Subgroup.toAddSubgroup (Subgroup.closure (Set.range v) ⊔ torsion K))
Module: Mathlib.RingTheory.RootsOfUnity.CyclotomicUnits

Goal state before:
pp: n j : ℕ
A : Type u_1
ζ : A
inst✝¹ : CommRing A
inst✝ : IsDomain A
hζ : IsPrimitiveRoot ζ n
hn : 2 ≤ n
i : ℕ
hjn : j.Coprime n
this : (ζ - 1) * ζ ^ i * ∑ i ∈ range j, ζ ^ i = ζ ^ (i + j) - ζ ^ i
⊢ (ζ - 1) * ↑(⋯.unit ^ i * ⋯.unit) = ζ ^ (i + j) - ζ ^ i

Tactic:
simp [← this, mul_assoc]

Goal state after:
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
P : Ideal (𝓞 K)
hP₁ : P.IsPrime
hP₂ : P.LiesOver 𝒑
hK : IsCyclotomicExtension {p ^ (k + 1)} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
⊢ 𝒑 = under ℤ (span {hζ.toInteger - 1})

Tactic:
refine IsMaximal.eq_of_le (Int.ideal_span_isMaximal_of_prime p) IsPrime.ne_top' ?_

Goal state after:
n m p k : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
P : Ideal (𝓞 K)
hP₁ : P.IsPrime
hP₂ : P.LiesOver 𝒑
hK : IsCyclotomicExtension {p ^ (k + 1)} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
⊢ 𝒑 ≤ under ℤ (span {hζ.toInteger - 1})
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
ζ : K
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
⊢ (span {hζ.toInteger - 1}).inertiaDeg ℤ = 1

Tactic:
have : IsMaximal (span {hζ.toInteger - 1}) := .of_liesOver_isMaximal _ 𝒑

Goal state after:
p k : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
hK : IsCyclotomicExtension {p ^ (k + 1)} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ (p ^ (k + 1))
this : (span {hζ.toInteger - 1}).IsMaximal
⊢ (span {hζ.toInteger - 1}).inertiaDeg ℤ = 1
Module: Mathlib.NumberTheory.NumberField.DirichletDensity

Goal state before:
pp: case pos
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
S : Set (HeightOneSpectrum (𝓞 K))
δ : ℝ
h : HasDirichletDensity S δ
s : ℝ
hs : Summable fun 𝔭 ↦ ↑(Ideal.absNorm 𝔭.asIdeal) ^ (-s)
⊢ (∑' (𝔭 : ↑S), ↑(Ideal.absNorm (↑𝔭).asIdeal) ^ (-s)) /
      ∑' (x : HeightOneSpectrum (𝓞 K)), ↑(Ideal.absNorm x.asIdeal) ^ (-s) ≤
    1

pp: case neg
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
S : Set (HeightOneSpectrum (𝓞 K))
δ : ℝ
h : HasDirichletDensity S δ
s : ℝ
hs : ¬Summable fun 𝔭 ↦ ↑(Ideal.absNorm 𝔭.asIdeal) ^ (-s)
⊢ (∑' (𝔭 : ↑S), ↑(Ideal.absNorm (↑𝔭).asIdeal) ^ (-s)) /
      ∑' (x : HeightOneSpectrum (𝓞 K)), ↑(Ideal.absNorm x.asIdeal) ^ (-s) ≤
    1

Tactic:
· exact div_le_one_of_le₀ (hs.tsum_subtype_le _ S (fun _ ↦ by positivity))
      (tsum_nonneg fun _ ↦ by positivity)

Goal state after:
case neg
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
S : Set (HeightOneSpectrum (𝓞 K))
δ : ℝ
h : HasDirichletDensity S δ
s : ℝ
hs : ¬Summable fun 𝔭 ↦ ↑(Ideal.absNorm 𝔭.asIdeal) ^ (-s)
⊢ (∑' (𝔭 : ↑S), ↑(Ideal.absNorm (↑𝔭).asIdeal) ^ (-s)) /
      ∑' (x : HeightOneSpectrum (𝓞 K)), ↑(Ideal.absNorm x.asIdeal) ^ (-s) ≤
    1
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
⊢ ¬∀ (x : α × (K →+* ℂ)), (fun l ↦ ((newBasis K).repr (a x.1 l.1 * (newBasis K) l.2)) x.2) = 0 x

Tactic:
intro hs

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

Goal state before:
pp: case calc_6
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
⊢ ↑h * c₂ K * (↑q * c₁ K * A) ^ (↑p / (↑q - ↑p)) ≤ c₁ K * (c₁ K * ↑q * A) ^ (↑p / (↑q - ↑p))

Tactic:
rw [mul_comm (q : ℝ) (c₁ K)]

Goal state after:
case calc_6
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
⊢ ↑h * c₂ K * (c₁ K * ↑q * A) ^ (↑p / (↑q - ↑p)) ≤ c₁ K * (c₁ K * ↑q * A) ^ (↑p / (↑q - ↑p))
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 i : ℕ
x✝ : i ∈ range (n + 1)
⊢ ‖((-1) ^ (n - i) * ↑(n.choose i)) • (f (↑i + ↑(p ^ t)) - f ↑i)‖ ≤
    ‖↑(-1) ^ (n - i) * ↑(n.choose i)‖ * ‖f (↑i + ↑(p ^ t)) - f ↑i‖

Tactic:
← Int.cast_smul_eq_zsmul ℤ_[p]

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 i : ℕ
x✝ : i ∈ range (n + 1)
⊢ ‖↑((-1) ^ (n - i) * ↑(n.choose i)) • (f (↑i + ↑(p ^ t)) - f ↑i)‖ ≤
    ‖↑(-1) ^ (n - i) * ↑(n.choose i)‖ * ‖f (↑i + ↑(p ^ t)) - f ↑i‖
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)
inst✝² : TopologicalSpace R
inst✝¹ : MonoidWithZero R
inst✝ : MulActionWithZero R V
f : C(X × Y, V)
hS : S ∈ 𝓤 V
hS' : {(f, g) | ∀ (y : Y), (f y, g y) ∈ S} ∈ 𝓤 C(Y, V)
n : ℕ
U : Fin n → TopologicalSpace.Clopens X
v : Fin n → C(Y, V)
hv : ∀ (x : X), (f.curry x, ∑ n, (↑(U n)).indicator (fun x ↦ v n) x) ∈ {(f, g) | ∀ (y : Y), (f y, g y) ∈ S}
x : X
y : Y
⊢ (f (x, y), ∑ i, ((fun i ↦ { toFun := (↑(U i)).indicator fun x ↦ 1, continuous_toFun := ⋯ }) i) x • (v i) y) ∈ S

Tactic:
convert! hv x y using 2

Goal state after:
case e'_4
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)
inst✝² : TopologicalSpace R
inst✝¹ : MonoidWithZero R
inst✝ : MulActionWithZero R V
f : C(X × Y, V)
hS : S ∈ 𝓤 V
hS' : {(f, g) | ∀ (y : Y), (f y, g y) ∈ S} ∈ 𝓤 C(Y, V)
n : ℕ
U : Fin n → TopologicalSpace.Clopens X
v : Fin n → C(Y, V)
hv : ∀ (x : X), (f.curry x, ∑ n, (↑(U n)).indicator (fun x ↦ v n) x) ∈ {(f, g) | ∀ (y : Y), (f y, g y) ∈ S}
x : X
y : Y
⊢ ∑ i, ((fun i ↦ { toFun := (↑(U i)).indicator fun x ↦ 1, continuous_toFun := ⋯ }) i) x • (v i) y =
    (∑ n, (↑(U n)).indicator (fun x ↦ v n) x) y
Module: Mathlib.NumberTheory.Pell

Goal state before:
pp: d : ℤ
h₀ : d ≠ 0
a : Solution₁ d
ha : a.x = 1
prop : d * a.y ^ 2 = a.x ^ 2 - 1
⊢ a = 1

Tactic:
ha,

Goal state after:
d : ℤ
h₀ : d ≠ 0
a : Solution₁ d
ha : a.x = 1
prop : d * a.y ^ 2 = 1 ^ 2 - 1
⊢ a = 1
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]
ha : (Polynomial.aeval a) F = 0
z' : ℤ_[p]
hz' : (Polynomial.aeval z') F = 0
hnormz' : ‖z' - a‖ < ‖(Polynomial.aeval a) (Polynomial.derivative F)‖
h : ℤ_[p] := z' - a
q : ℤ_[p]
hq :
  (Polynomial.aeval (a + h)) F = (Polynomial.aeval a) F + (Polynomial.aeval a) (Polynomial.derivative F) * h + q * h ^ 2
⊢ ((Polynomial.aeval a) (Polynomial.derivative F) + q * h) * h =
    (Polynomial.aeval a) F + (Polynomial.aeval a) (Polynomial.derivative F) * h + q * h ^ 2

Tactic:
ha,

Goal state after:
p : ℕ
inst✝² : Fact (Nat.Prime p)
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Algebra R ℤ_[p]
F : Polynomial R
a : ℤ_[p]
ha : (Polynomial.aeval a) F = 0
z' : ℤ_[p]
hz' : (Polynomial.aeval z') F = 0
hnormz' : ‖z' - a‖ < ‖(Polynomial.aeval a) (Polynomial.derivative F)‖
h : ℤ_[p] := z' - a
q : ℤ_[p]
hq :
  (Polynomial.aeval (a + h)) F = (Polynomial.aeval a) F + (Polynomial.aeval a) (Polynomial.derivative F) * h + q * h ^ 2
⊢ ((Polynomial.aeval a) (Polynomial.derivative F) + q * h) * h =
    0 + (Polynomial.aeval a) (Polynomial.derivative F) * h + q * h ^ 2
Module: Mathlib.NumberTheory.Pell

Goal state before:
pp: d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
ξ : ℝ := √↑d
hξ : Irrational ξ
M : ℤ
hM₁ : 2 * |ξ| + 1 < ↑M
hM : {q | |q.num ^ 2 - d * ↑q.den ^ 2| < M}.Infinite
hm : {q | q.num ^ 2 - d * ↑q.den ^ 2 = 0}.Infinite
q : ℚ
hq : q.num ^ 2 = ↑q.den ^ 2 * d
a : ℤ
ha : q.num = ↑q.den * a
⊢ False

Tactic:
ha,

Goal state after:
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
ξ : ℝ := √↑d
hξ : Irrational ξ
M : ℤ
hM₁ : 2 * |ξ| + 1 < ↑M
hM : {q | |q.num ^ 2 - d * ↑q.den ^ 2| < M}.Infinite
hm : {q | q.num ^ 2 - d * ↑q.den ^ 2 = 0}.Infinite
q : ℚ
a : ℤ
hq : (↑q.den * a) ^ 2 = ↑q.den ^ 2 * d
ha : q.num = ↑q.den * a
⊢ False
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
inst✝⁸ : IsDomain R
inst✝⁷ : IsDomain S
inst✝⁶ : Algebra K L
inst✝⁵ : Module.Finite R S
inst✝⁴ : Algebra R L
inst✝³ : IsScalarTower R S L
inst✝² : IsScalarTower R K L
inst✝¹ : Algebra.IsAlgebraic R S
inst✝ : IsTorsionFree R K
hp : p ≠ ⊤
b : Set S
hb' : Submodule.span R b ⊔ Submodule.restrictScalars R (map f p) = ⊤
hRL : Function.Injective ⇑(algebraMap R L)
M : Submodule R S := Submodule.span R b
n : ℕ
a : Fin n → S ⧸ M
ha : Submodule.span R (Set.range a) = ⊤
smul_top_eq : p • ⊤ = ⊤
x : S ⧸ M
⊢ x ∈ p • Submodule.span R (Set.range a)

Tactic:
ha,

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
inst✝⁸ : IsDomain R
inst✝⁷ : IsDomain S
inst✝⁶ : Algebra K L
inst✝⁵ : Module.Finite R S
inst✝⁴ : Algebra R L
inst✝³ : IsScalarTower R S L
inst✝² : IsScalarTower R K L
inst✝¹ : Algebra.IsAlgebraic R S
inst✝ : IsTorsionFree R K
hp : p ≠ ⊤
b : Set S
hb' : Submodule.span R b ⊔ Submodule.restrictScalars R (map f p) = ⊤
hRL : Function.Injective ⇑(algebraMap R L)
M : Submodule R S := Submodule.span R b
n : ℕ
a : Fin n → S ⧸ M
ha : Submodule.span R (Set.range a) = ⊤
smul_top_eq : p • ⊤ = ⊤
x : S ⧸ M
⊢ x ∈ p • ⊤
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
inst✝⁸ : IsDomain R
inst✝⁷ : IsDomain S
inst✝⁶ : Algebra K L
inst✝⁵ : Module.Finite R S
inst✝⁴ : Algebra R L
inst✝³ : IsScalarTower R S L
inst✝² : IsScalarTower R K L
inst✝¹ : Algebra.IsAlgebraic R S
inst✝ : IsTorsionFree R K
hp : p ≠ ⊤
b : Set S
hb' : Submodule.span R b ⊔ Submodule.restrictScalars R (map f p) = ⊤
hRL : Function.Injective ⇑(algebraMap R L)
M : Submodule R S := Submodule.span R b
n : ℕ
a : Fin n → S ⧸ M
ha : Submodule.span R (Set.range a) = ⊤
smul_top_eq : p • ⊤ = ⊤
x : S ⧸ M
a'' : Fin n →₀ R
ha'' : ∀ (i : Fin n), a'' i ∈ p
hx : (a''.sum fun i c ↦ c • a i) = x
⊢ ∃ a', (∀ (i : Fin n), a' i ∈ p) ∧ ∑ i, a' i • a i = x

Tactic:
· refine ⟨fun i => a'' i, fun i => ha'' _, ?_⟩
      rw [← hx, Finsupp.sum_fintype]
      exact fun _ => zero_smul _ _

Goal state after:
Module: Mathlib.NumberTheory.Pell

Goal state before:
pp: case inl.inl.inl
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
a₁ : Solution₁ d
ha₁ : IsFundamental a₁
n₁ : ℤ
Hx : 1 < (a₁ ^ 1).x
Hy : 0 < (a₁ ^ 1).y
H : ∀ (a : Solution₁ d), ∃ n, a = (a₁ ^ 1) ^ n ∨ a = -(a₁ ^ 1) ^ n
hn₁ : a₁ ^ (1 * n₁ - 1) = 1
⊢ a₁ ^ 1 = a₁

Tactic:
zpow_one

Goal state after:
case inl.inl.inl
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
a₁ : Solution₁ d
ha₁ : IsFundamental a₁
n₁ : ℤ
Hx : 1 < (a₁ ^ 1).x
Hy : 0 < (a₁ ^ 1).y
H : ∀ (a : Solution₁ d), ∃ n, a = (a₁ ^ 1) ^ n ∨ a = -(a₁ ^ 1) ^ n
hn₁ : a₁ ^ (1 * n₁ - 1) = 1
⊢ a₁ = a₁
Module: Mathlib.NumberTheory.RamificationInertia.HilbertTheory

Goal state before:
pp: A : Type u_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 A
inst✝³⁵ : CommRing B
inst✝³⁴ : Algebra A B
p : Ideal A
P : Ideal B
inst✝³³ : P.LiesOver p
inst✝³² : Algebra A K
inst✝³¹ : IsFractionRing A K
inst✝³⁰ : Algebra A L
inst✝²⁹ : IsScalarTower A K L
inst✝²⁸ : Algebra B L
inst✝²⁷ : IsScalarTower A B L
inst✝²⁶ : IsFractionRing B L
inst✝²⁵ : MulSemiringAction Gal(L/K) B
inst✝²⁴ : SMulDistribClass Gal(L/K) B L
D : Type u_5
𝓞D : Type u_6
inst✝²³ : Field D
inst✝²² : Algebra D L
inst✝²¹ : IsDecompositionField K L P D
inst✝²⁰ : CommRing 𝓞D
inst✝¹⁹ : Algebra 𝓞D D
inst✝¹⁸ : IsFractionRing 𝓞D D
inst✝¹⁷ : Algebra 𝓞D B
inst✝¹⁶ : Algebra 𝓞D L
inst✝¹⁵ : IsScalarTower 𝓞D D L
inst✝¹⁴ : IsScalarTower 𝓞D B L
𝓟D : Ideal 𝓞D
hD : P.LiesOver 𝓟D
inst✝¹³ : IsGalois K L
inst✝¹² : IsDedekindDomain A
inst✝¹¹ : IsDedekindDomain B
inst✝¹⁰ : Module.Finite A B
inst✝⁹ : Module.IsTorsionFree A B
inst✝⁸ : Algebra A 𝓞D
inst✝⁷ : Module.Finite A 𝓞D
inst✝⁶ : IsScalarTower A 𝓞D B
inst✝⁵ : IsDedekindDomain 𝓞D
inst✝⁴ : 𝓟D.LiesOver p
inst✝³ : FiniteDimensional K L
inst✝² : Ring.HasFiniteQuotients A
inst✝¹ : 𝓟D.IsMaximal
inst✝ : P.IsMaximal
hp : p ≠ ⊥
left✝⁴ : Module.Finite 𝓞D B
left✝³ : Module.IsTorsionFree 𝓞D B
left✝² : Module.IsTorsionFree A 𝓞D
left✝¹ : IsGaloisGroup Gal(L/K) A B
left✝ : IsGaloisGroup (↥(stabilizer Gal(L/K) P)) 𝓞D B
right✝ : 𝓟D ≠ ⊥
this : P.inertiaDeg A = 𝓟D.inertiaDeg A * P.inertiaDeg 𝓞D
⊢ 𝓟D.inertiaDeg A = 1

Tactic:
← inertiaDegIn_eq_inertiaDeg p P Gal(L/K),

Goal state after:
A : Type u_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 A
inst✝³⁵ : CommRing B
inst✝³⁴ : Algebra A B
p : Ideal A
P : Ideal B
inst✝³³ : P.LiesOver p
inst✝³² : Algebra A K
inst✝³¹ : IsFractionRing A K
inst✝³⁰ : Algebra A L
inst✝²⁹ : IsScalarTower A K L
inst✝²⁸ : Algebra B L
inst✝²⁷ : IsScalarTower A B L
inst✝²⁶ : IsFractionRing B L
inst✝²⁵ : MulSemiringAction Gal(L/K) B
inst✝²⁴ : SMulDistribClass Gal(L/K) B L
D : Type u_5
𝓞D : Type u_6
inst✝²³ : Field D
inst✝²² : Algebra D L
inst✝²¹ : IsDecompositionField K L P D
inst✝²⁰ : CommRing 𝓞D
inst✝¹⁹ : Algebra 𝓞D D
inst✝¹⁸ : IsFractionRing 𝓞D D
inst✝¹⁷ : Algebra 𝓞D B
inst✝¹⁶ : Algebra 𝓞D L
inst✝¹⁵ : IsScalarTower 𝓞D D L
inst✝¹⁴ : IsScalarTower 𝓞D B L
𝓟D : Ideal 𝓞D
hD : P.LiesOver 𝓟D
inst✝¹³ : IsGalois K L
inst✝¹² : IsDedekindDomain A
inst✝¹¹ : IsDedekindDomain B
inst✝¹⁰ : Module.Finite A B
inst✝⁹ : Module.IsTorsionFree A B
inst✝⁸ : Algebra A 𝓞D
inst✝⁷ : Module.Finite A 𝓞D
inst✝⁶ : IsScalarTower A 𝓞D B
inst✝⁵ : IsDedekindDomain 𝓞D
inst✝⁴ : 𝓟D.LiesOver p
inst✝³ : FiniteDimensional K L
inst✝² : Ring.HasFiniteQuotients A
inst✝¹ : 𝓟D.IsMaximal
inst✝ : P.IsMaximal
hp : p ≠ ⊥
left✝⁴ : Module.Finite 𝓞D B
left✝³ : Module.IsTorsionFree 𝓞D B
left✝² : Module.IsTorsionFree A 𝓞D
left✝¹ : IsGaloisGroup Gal(L/K) A B
left✝ : IsGaloisGroup (↥(stabilizer Gal(L/K) P)) 𝓞D B
right✝ : 𝓟D ≠ ⊥
this : p.inertiaDegIn B = 𝓟D.inertiaDeg A * P.inertiaDeg 𝓞D
⊢ 𝓟D.inertiaDeg A = 1
Module: Mathlib.NumberTheory.Rayleigh

Goal state before:
pp: r s : ℝ
hrs : r.HolderConjugate s
j k : ℤ
h₁ : ↑j / r ≤ ↑k ∧ ↑k < (↑j + 1) / r
m : ℤ
h₂ : ↑j / s < ↑m ∧ ↑m ≤ (↑j + 1) / s
h₃ : ↑j < ↑k + ↑m
h₄ : ↑k + ↑m < ↑j + 1
⊢ False

Tactic:
← Int.cast_one

Goal state after:
r s : ℝ
hrs : r.HolderConjugate s
j k : ℤ
h₁ : ↑j / r ≤ ↑k ∧ ↑k < (↑j + 1) / r
m : ℤ
h₂ : ↑j / s < ↑m ∧ ↑m ≤ (↑j + 1) / s
h₃ : ↑j < ↑k + ↑m
h₄ : ↑k + ↑m < ↑j + ↑1
⊢ False
Module: Mathlib.NumberTheory.SelbergSieve

Goal state before:
pp: s : BoundingSieve
muPlus : ℕ → ℝ
h : IsUpperMoebius muPlus
⊢ s.totalMass * mainSum muPlus + ∑ d ∈ s.prodPrimes.divisors, muPlus d * rem d ≤
    s.totalMass * mainSum muPlus + errSum muPlus

Tactic:
errSum

Goal state after:
s : BoundingSieve
muPlus : ℕ → ℝ
h : IsUpperMoebius muPlus
⊢ s.totalMass * mainSum muPlus + ∑ d ∈ s.prodPrimes.divisors, muPlus d * rem d ≤
    s.totalMass * mainSum muPlus + ∑ d ∈ s.prodPrimes.divisors, |muPlus d| * |rem d|
Module: Mathlib.NumberTheory.Zsqrtd.QuadraticReciprocity

Goal state before:
pp: 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 := ↑k, im := 1 } * { re := ↑k, im := -1 }

Tactic:
ext <;> 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
⊢ a * b = (x * u - y * v) ^ 2 + (x * v + y * u) ^ 2

Tactic:
ha,

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) * b = (x * u - y * v) ^ 2 + (x * v + y * u) ^ 2