mathlib-initiative/mathlib-tactics huggingface dataset:
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, Nat.Prime p ∧ ∀ (P : Ideal 𝒪) (x : P.IsPrime), ↑p ∈ P → ¬Algebra.IsUnramifiedAt ℤ P

Tactic:
obtain ⟨P, _, hP'⟩ := NumberField.exists_not_isUnramifiedAt_int (𝒪 := 𝒪) H.ne'

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 𝒪
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, Nat.Prime p ∧ ∀ (P : Ideal 𝒪) (x : P.IsPrime), ↑p ∈ P → ¬Algebra.IsUnramifiedAt ℤ P
Module: Mathlib.NumberTheory.Ostrowski

Goal state before:
pp: f g : AbsoluteValue ℚ ℝ
x✝ : ∃ c, 0 < c ∧ ∀ (n : ℕ), f ↑n ^ c = g ↑n
c : ℝ
hc : 0 < c
h : ∀ (n : ℕ), f ↑n ^ c = g ↑n
x : ℚ
⊢ f x ^ c = g x

Tactic:
← Rat.num_div_den x,

Goal state after:
f g : AbsoluteValue ℚ ℝ
x✝ : ∃ c, 0 < c ∧ ∀ (n : ℕ), f ↑n ^ c = g ↑n
c : ℝ
hc : 0 < c
h : ∀ (n : ℕ), f ↑n ^ c = g ↑n
x : ℚ
⊢ f (↑x.num / ↑x.den) ^ c = g (↑x.num / ↑x.den)
Module: Mathlib.NumberTheory.NumberField.Ideal.Asymptotics

Goal state before:
pp: case convert_4
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
C : ClassGroup (𝓞 K)
h₁ :
  ∀ (s : ℝ),
    {x | x ∈ ⇑(toMixed K) ⁻¹' fundamentalCone K ∧ mixedEmbedding.norm ((toMixed K) x) ≤ s} =
      ⇑(toMixed K) ⁻¹' {x | x ∈ fundamentalCone K ∧ mixedEmbedding.norm x ≤ s}
h₂ : {x | x ∈ fundamentalCone K ∧ mixedEmbedding.norm x ≤ 1} = normLeOne K
J : ↥(Ideal (𝓞 K))⁰
hJ : ClassGroup.mk0 J = C⁻¹
h₃ : ↑(absNorm ↑J) ≠ 0
⊢ MeasureTheory.volume (frontier (normLeOne K)) = 0

Tactic:
volume_frontier_normLeOne

Goal state after:
case convert_4
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
C : ClassGroup (𝓞 K)
h₁ :
  ∀ (s : ℝ),
    {x | x ∈ ⇑(toMixed K) ⁻¹' fundamentalCone K ∧ mixedEmbedding.norm ((toMixed K) x) ≤ s} =
      ⇑(toMixed K) ⁻¹' {x | x ∈ fundamentalCone K ∧ mixedEmbedding.norm x ≤ s}
h₂ : {x | x ∈ fundamentalCone K ∧ mixedEmbedding.norm x ≤ 1} = normLeOne K
J : ↥(Ideal (𝓞 K))⁰
hJ : ClassGroup.mk0 J = C⁻¹
h₃ : ↑(absNorm ↑J) ≠ 0
⊢ 0 = 0
Module: Mathlib.NumberTheory.NumberField.Ideal.Asymptotics

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

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

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

Goal state before:

Tactic:
‖asiegel K a kr lu‖ = |asiegel K a kr lu| := ?_
      _ ≤ c K * house ((algebraMap (𝓞 K) K) (a kr.1 lu.1 * ((newBasis K) lu.2))) := ?_
      _ ≤ c K * house ((algebraMap (𝓞 K) K) (a kr.1 lu.1)) *
        house ((algebraMap (𝓞 K) K) ((newBasis K) lu.2)) := ?_
      _ ≤ c K * A * house ((algebraMap (𝓞 K) K) ((newBasis K) lu.2)) := ?_
      _ ≤ c K * A * supOfBasis K := ?_
      _ ≤ c₂ K * A := ?_

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)
inst✝² : Fintype β
A : ℝ
habs : ∀ (k : α) (l : β), house ((algebraMap (𝓞 K) K) (a k l)) ≤ A
inst✝¹ : DecidableEq (K →+* ℂ)
inst✝ : Fintype α
Apos : 0 ≤ A
this : 0 ≤ c K
kr : α × (K →+* ℂ)
lu : β × (K →+* ℂ)
⊢ ‖asiegel K a kr lu‖ = ↑|asiegel K a kr lu|

case calc_2
K : Type u_1
inst✝⁴ : Field K
inst✝³ : NumberField K
α : Type u_2
β : Type u_3
a : Matrix α β (𝓞 K)
inst✝² : Fintype β
A : ℝ
habs : ∀ (k : α) (l : β), house ((algebraMap (𝓞 K) K) (a k l)) ≤ A
inst✝¹ : DecidableEq (K →+* ℂ)
inst✝ : Fintype α
Apos : 0 ≤ A
this : 0 ≤ c K
kr : α × (K →+* ℂ)
lu : β × (K →+* ℂ)
⊢ ↑|asiegel K a kr lu| ≤ c K * house ((algebraMap (𝓞 K) K) (a kr.1 lu.1 * (newBasis K) lu.2))

case calc_3
K : Type u_1
inst✝⁴ : Field K
inst✝³ : NumberField K
α : Type u_2
β : Type u_3
a : Matrix α β (𝓞 K)
inst✝² : Fintype β
A : ℝ
habs : ∀ (k : α) (l : β), house ((algebraMap (𝓞 K) K) (a k l)) ≤ A
inst✝¹ : DecidableEq (K →+* ℂ)
inst✝ : Fintype α
Apos : 0 ≤ A
this : 0 ≤ c K
kr : α × (K →+* ℂ)
lu : β × (K →+* ℂ)
⊢ c K * house ((algebraMap (𝓞 K) K) (a kr.1 lu.1 * (newBasis K) lu.2)) ≤
    c K * house ((algebraMap (𝓞 K) K) (a kr.1 lu.1)) * house ((algebraMap (𝓞 K) K) ((newBasis K) lu.2))

case calc_4
K : Type u_1
inst✝⁴ : Field K
inst✝³ : NumberField K
α : Type u_2
β : Type u_3
a : Matrix α β (𝓞 K)
inst✝² : Fintype β
A : ℝ
habs : ∀ (k : α) (l : β), house ((algebraMap (𝓞 K) K) (a k l)) ≤ A
inst✝¹ : DecidableEq (K →+* ℂ)
inst✝ : Fintype α
Apos : 0 ≤ A
this : 0 ≤ c K
kr : α × (K →+* ℂ)
lu : β × (K →+* ℂ)
⊢ c K * house ((algebraMap (𝓞 K) K) (a kr.1 lu.1)) * house ((algebraMap (𝓞 K) K) ((newBasis K) lu.2)) ≤
    c K * A * house ((algebraMap (𝓞 K) K) ((newBasis K) lu.2))

case calc_5
K : Type u_1
inst✝⁴ : Field K
inst✝³ : NumberField K
α : Type u_2
β : Type u_3
a : Matrix α β (𝓞 K)
inst✝² : Fintype β
A : ℝ
habs : ∀ (k : α) (l : β), house ((algebraMap (𝓞 K) K) (a k l)) ≤ A
inst✝¹ : DecidableEq (K →+* ℂ)
inst✝ : Fintype α
Apos : 0 ≤ A
this : 0 ≤ c K
kr : α × (K →+* ℂ)
lu : β × (K →+* ℂ)
⊢ c K * A * house ((algebraMap (𝓞 K) K) ((newBasis K) lu.2)) ≤ c K * A * supOfBasis K

case calc_6
K : Type u_1
inst✝⁴ : Field K
inst✝³ : NumberField K
α : Type u_2
β : Type u_3
a : Matrix α β (𝓞 K)
inst✝² : Fintype β
A : ℝ
habs : ∀ (k : α) (l : β), house ((algebraMap (𝓞 K) K) (a k l)) ≤ A
inst✝¹ : DecidableEq (K →+* ℂ)
inst✝ : Fintype α
Apos : 0 ≤ A
this : 0 ≤ c K
kr : α × (K →+* ℂ)
lu : β × (K →+* ℂ)
⊢ c K * A * supOfBasis K ≤ c₂ K * A
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
p q : ℕ
h0p : 0 < p
hpq : p < q
inst✝² : Fintype β
cardβ : Fintype.card β = q
A : ℝ
habs : ∀ (k : α) (l : β), house ((algebraMap (𝓞 K) K) (a k l)) ≤ A
inst✝¹ : DecidableEq (K →+* ℂ)
inst✝ : Fintype α
cardα : Fintype.card α = p
h : ℕ := finrank ℚ K
hphqh : p * h < q * h
⊢ ∃ ξ, ξ ≠ 0 ∧ a *ᵥ ξ = 0 ∧ ∀ (l : β), house ↑(ξ l) ≤ c₁ K * (c₁ K * ↑q * A) ^ (↑p / (↑q - ↑p))

Tactic:
have h0ph : 0 < p * h := by rw [mul_pos_iff]; constructor; exact ⟨h0p, finrank_pos⟩

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
p q : ℕ
h0p : 0 < p
hpq : p < q
inst✝² : Fintype β
cardβ : Fintype.card β = q
A : ℝ
habs : ∀ (k : α) (l : β), house ((algebraMap (𝓞 K) K) (a k l)) ≤ A
inst✝¹ : DecidableEq (K →+* ℂ)
inst✝ : Fintype α
cardα : Fintype.card α = p
h : ℕ := finrank ℚ K
hphqh : p * h < q * h
h0ph : 0 < p * h
⊢ ∃ ξ, ξ ≠ 0 ∧ a *ᵥ ξ = 0 ∧ ∀ (l : β), house ↑(ξ l) ≤ c₁ K * (c₁ K * ↑q * A) ^ (↑p / (↑q - ↑p))
Module: Mathlib.NumberTheory.Padics.Complex

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
⊢ Valued.v ↑p = 1 / ↑p

Tactic:
← map_natCast (algebraMap (PadicAlgCl p) ℂ_[p]),

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
⊢ Valued.v ((algebraMap (PadicAlgCl p) ℂ_[p]) ↑p) = 1 / ↑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) = ⊤
⊢ Submodule.map M.mkQ (p • ⊤) = ⊤

Tactic:
by rw [Ideal.smul_top_eq_map, (Submodule.map_mkQ_eq_top M _).mpr hb']

Goal state after:
Module: Mathlib.NumberTheory.Pell

Goal state before:
pp: d : ℤ
a : Solution₁ d
h : IsFundamental a
⊢ ∀ (n : ℤ), 0 ≤ n → (a ^ n).y < (a ^ (n + 1)).y

Tactic:
intro n hn

Goal state after:
d : ℤ
a : Solution₁ d
h : IsFundamental a
n : ℤ
hn : 0 ≤ n
⊢ (a ^ n).y < (a ^ (n + 1)).y
Module: Mathlib.NumberTheory.Pell

Goal state before:
pp: case calc.step
d : ℤ
a₁ : Solution₁ d
h : IsFundamental a₁
a : Solution₁ d
hax : 1 < a.x
hay : 0 < a.y
⊢ a.y * (1 + d * a₁.y ^ 2) - a₁.y * (d * (a.y * a₁.y) + a.x) < 0

Tactic:
suffices a.y - a.x * a₁.y < 0 by convert! this using 1; ring

Goal state after:
case calc.step
d : ℤ
a₁ : Solution₁ d
h : IsFundamental a₁
a : Solution₁ d
hax : 1 < a.x
hay : 0 < a.y
⊢ a.y - a.x * a₁.y < 0
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 | v ↑p < 1 ∧ p ≠ 0}.Nonempty

Tactic:
by
  obtain ⟨w, h0, h1⟩ := IsNontrivial.exists_lt_one (v := v)
  induction w using RatFunc.induction_on with
  | f p q =>
    simp only [ne_eq, _root_.div_eq_zero_iff, FaithfulSMul.algebraMap_eq_zero_iff, not_or,
      map_div₀] at *
    have hor : ¬v ↑p = 1 ∨ ¬v ↑q = 1 := by rw [← not_and_or]; aesop
    suffices ∀ r : K[X], v (↑r) ≠ 1 → r ≠ 0 → {p : K[X] | v ↑p < 1 ∧ ¬p = 0}.Nonempty by
      exact Or.elim hor (fun hp ↦ this p hp h0.1) (fun hq ↦ this q hq h0.2)
    exact fun r hr hr0 ↦ ⟨r, lt_iff_le_and_ne.mpr
      ⟨Polynomial.valuation_le_one_of_valuation_X_le_one _ hle r, hr⟩, hr0⟩

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
heq : p = π ^ k * q
hπ : v ↑π < 1 ∧ ¬π = 0
this : v ((algebraMap K[X] K⟮X⟯) q) = 1
⊢ v ((algebraMap K[X] K⟮X⟯) π) ^ k * v ((algebraMap K[X] K⟮X⟯) q) =
    v ↑π ^ (Associates.mk Pᵥ.asIdeal).count (Associates.mk (Ideal.span {p})).factors

Tactic:
simp only [this, mul_one]

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
heq : p = π ^ k * q
hπ : v ↑π < 1 ∧ ¬π = 0
this : v ((algebraMap K[X] K⟮X⟯) q) = 1
⊢ v ((algebraMap K[X] K⟮X⟯) π) ^ k = v ↑π ^ (Associates.mk Pᵥ.asIdeal).count (Associates.mk (Ideal.span {p})).factors
Module: Mathlib.NumberTheory.SumFourSquares

Goal state before:
pp: case inr
p : ℕ
hp : Fact (Nat.Prime p)
hodd : Odd p
⊢ ∃ a b k, 0 < k ∧ k < p ∧ a ^ 2 + b ^ 2 + 1 = k * p

Tactic:
rcases Nat.sq_add_sq_zmodEq p (-1) with ⟨a, b, ha, hb, hab⟩

Goal state after:
case inr
p : ℕ
hp : Fact (Nat.Prime p)
hodd : Odd p
a b : ℕ
ha : a ≤ p / 2
hb : b ≤ p / 2
hab : ↑a ^ 2 + ↑b ^ 2 ≡ -1 [ZMOD ↑p]
⊢ ∃ a b k, 0 < k ∧ k < p ∧ a ^ 2 + b ^ 2 + 1 = k * p
Module: Mathlib.NumberTheory.SumFourSquares

Goal state before:
pp: case inr
p : ℕ
hp : Fact (Nat.Prime p)
hodd : Odd p
a b : ℕ
ha : a ≤ p / 2
hb : b ≤ p / 2
hab : ↑a ^ 2 + ↑b ^ 2 ≡ -1 [ZMOD ↑p]
k : ℤ
hk : ↑a ^ 2 + ↑b ^ 2 + 1 = k * ↑p
hk₀ : 0 < k
⊢ ∃ a b k, 0 < k ∧ k < p ∧ a ^ 2 + b ^ 2 + 1 = k * p

Tactic:
lift k to ℕ using hk₀.le

Goal state after:
case inr
p : ℕ
hp : Fact (Nat.Prime p)
hodd : Odd p
a b : ℕ
ha : a ≤ p / 2
hb : b ≤ p / 2
hab : ↑a ^ 2 + ↑b ^ 2 ≡ -1 [ZMOD ↑p]
k : ℕ
hk : ↑a ^ 2 + ↑b ^ 2 + 1 = ↑k * ↑p
hk₀ : 0 < ↑k
⊢ ∃ a b k, 0 < k ∧ k < p ∧ a ^ 2 + b ^ 2 + 1 = k * p
Module: Mathlib.NumberTheory.Zsqrtd.GaussianInt

Goal state before:
pp: x y : ℂ
hre : |x.re| ≤ |y.re|
him : |x.im| ≤ |y.im|
⊢ x.re * x.re + x.im * x.im ≤ y.re * y.re + y.im * y.im

Tactic:
nlinarith [sq_le_sq.mpr hre, sq_le_sq.mpr him]

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

Goal state before:
pp: ⊢ failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)

Tactic:
simp [div_def]; rfl

Goal state after:
Module: Mathlib.NumberTheory.SumTwoSquares

Goal state before:
pp: case prime_mul
p n : ℕ
hpp : Prime p
ih : IsSquare (-1) → ∃ x y, n = x ^ 2 + y ^ 2
h : IsSquare (-1)
this : Fact (Prime p)
⊢ ∃ x y, p * n = x ^ 2 + y ^ 2

Tactic:
have hp : IsSquare (-1 : ZMod p) := ZMod.isSquare_neg_one_of_dvd ⟨n, rfl⟩ h

Goal state after:
case prime_mul
p n : ℕ
hpp : Prime p
ih : IsSquare (-1) → ∃ x y, n = x ^ 2 + y ^ 2
h : IsSquare (-1)
this : Fact (Prime p)
hp : IsSquare (-1)
⊢ ∃ x y, p * n = x ^ 2 + y ^ 2
Module: Mathlib.NumberTheory.SumTwoSquares

Goal state before:
pp: n x y : ℕ
h : n = x ^ 2 + y ^ 2
hxy : x = 0 ∧ y = 0
⊢ -1 = 0 * 0

Tactic:
rw [zero_mul, neg_eq_zero, Fin.one_eq_zero_iff]

Goal state after:
Module: Mathlib.NumberTheory.Transcendental.Lindemann.AnalyticalPart

Goal state before:
pp: case e'_9
p : ℂ[X]
s : ℂ
x : ℝ
h₀ : HasDerivAt (fun y ↦ y • s) (1 • s) x
h₁ : HasDerivAt (fun x ↦ cexp (-(x • s))) (cexp (-(x • s)) * -(1 • s)) x
h₂ : HasDerivAt ((fun x ↦ eval x (sumIDeriv p)) ∘ fun y ↦ y • s) (eval (x • s) (derivative (sumIDeriv p)) * 1 • s) x
⊢ s * (cexp (-(x • s)) * eval (x • s) p) =
    -(cexp (-(x • s)) * -(1 • s) * ((fun x ↦ eval x (p + derivative (sumIDeriv p))) ∘ fun y ↦ y • s) x +
        cexp (-(x • s)) * (eval (x • s) (derivative (sumIDeriv p)) * 1 • s))

Tactic:
simp only [one_smul, eval_add, Function.comp_apply]

Goal state after:
case e'_9
p : ℂ[X]
s : ℂ
x : ℝ
h₀ : HasDerivAt (fun y ↦ y • s) (1 • s) x
h₁ : HasDerivAt (fun x ↦ cexp (-(x • s))) (cexp (-(x • s)) * -(1 • s)) x
h₂ : HasDerivAt ((fun x ↦ eval x (sumIDeriv p)) ∘ fun y ↦ y • s) (eval (x • s) (derivative (sumIDeriv p)) * 1 • s) x
⊢ s * (cexp (-(x • s)) * eval (x • s) p) =
    -(cexp (-(x • s)) * -s * (eval (x • s) p + eval (x • s) (derivative (sumIDeriv p))) +
        cexp (-(x • s)) * (eval (x • s) (derivative (sumIDeriv p)) * s))
Module: Mathlib.NumberTheory.Transcendental.Lindemann.AnalyticalPart

Goal state before:
pp: f : ℕ → ℂ[X]
s : ℂ
c' : ℝ
hc' : c' ≥ 0
h' : ∀ (p : ℕ), ‖P (f p) s‖ ≤ Real.exp s.re * (Real.exp ‖s‖ * c' ^ p * ‖s‖)
c₁ : ℝ := max (Real.exp s.re) 1
c₂ : ℝ := max (Real.exp ‖s‖) 1
c₃ : ℝ := max ‖s‖ 1
p : ℕ
hp : p ≠ 0
x : ℝ
h : max x 1 = 1 ∧ x < 1
⊢ x ≤ 1

Tactic:
exact h.2.le

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

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

Tactic:
have bq0 : (0 : ℝ) < b * q := mul_pos (Nat.cast_pos.mpr bN0.bot_lt) qR0

Goal state after:
a : ℤ
b : ℕ
bN0 : b ≠ 0
cop : a.natAbs.Coprime b
h : Liouville (↑a / ↑b)
p q : ℤ
q1 : 1 < q
a0 : ↑a / ↑b ≠ ↑p / ↑q
a1 : |↑a / ↑b - ↑p / ↑q| < 1 / ↑q ^ (b + 1)
qR0 : 0 < ↑q
b0 : ↑b ≠ 0
bq0 : 0 < ↑b * ↑q
⊢ 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
P : Ideal S
inst✝² : IsDedekindDomain S
inst✝¹ : p.IsMaximal
inst✝ : P.IsPrime
hP0 : P ≠ ⊥
he : e ≠ 0
this✝ : NeZero e := { out := he }
this : Module.rank (R ⧸ p) ↥(map (Quotient.mk (P ^ e)) 1) = (e - 0) • Module.rank (R ⧸ p) (S ⧸ P)
⊢ Module.rank (R ⧸ p) (S ⧸ P ^ e) = e • Module.rank (R ⧸ p) (S ⧸ P)

Tactic:
Nat.sub_zero,

Goal state after:
R : Type u
inst✝⁵ : CommRing R
S : Type v
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
p : Ideal R
P : Ideal S
inst✝² : IsDedekindDomain S
inst✝¹ : p.IsMaximal
inst✝ : P.IsPrime
hP0 : P ≠ ⊥
he : e ≠ 0
this✝ : NeZero e := { out := he }
this : Module.rank (R ⧸ p) ↥(map (Quotient.mk (P ^ e)) 1) = e • Module.rank (R ⧸ p) (S ⧸ P)
⊢ Module.rank (R ⧸ p) (S ⧸ P ^ e) = e • Module.rank (R ⧸ p) (S ⧸ P)
Module: Mathlib.NumberTheory.Transcendental.Liouville.Residual

Goal state before:
pp: case refine_2.refine_2.convert_2
r : ℚ
n : ℕ
⊢ 0 < 1 / ↑(↑r.den * 2) ^ n

Tactic:
refine one_div_pos.2 (pow_pos (Int.cast_pos.2 ?_) _)
        exact mul_pos (Int.natCast_pos.2 r.pos) zero_lt_two

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

Goal state before:
pp: p x : ℝ
h : LiouvilleWith p x
r : ℚ
⊢ LiouvilleWith p (x + ↑r)

Tactic:
by
  rcases h.exists_pos with ⟨C, _hC₀, hC⟩
  refine ⟨r.den ^ p * C, (tendsto_id.nsmul_atTop r.pos).frequently (hC.mono ?_)⟩
  rintro n ⟨hn, m, hne, hlt⟩
  have : (↑(r.den * m + r.num * n : ℤ) / ↑(r.den • id n) : ℝ) = m / n + r := by
    rw [smul_eq_mul, id]
    nth_rewrite 4 [← Rat.num_div_den r]
    push_cast
    rw [add_div, mul_div_mul_left _ _ (by positivity), mul_div_mul_right _ _ (by positivity)]
  refine ⟨r.den * m + r.num * n, ?_⟩; rw [this, add_sub_add_right_eq_sub]
  refine ⟨by simpa, hlt.trans_le (le_of_eq ?_)⟩
  have : (r.den ^ p : ℝ) ≠ 0 := by positivity
  simp [mul_rpow, mul_div_mul_left, this]

Goal state after:
Module: Mathlib.Order.CompleteLattice.PiLex

Goal state before:
pp: ι : Type u_1
α : ι → Type u_2
inst✝² : LinearOrder ι
inst✝¹ : (i : ι) → CompleteLinearOrder (α i)
inst✝ : WellFoundedLT ι
x✝ : Set (Lex ((i : ι) → (fun i ↦ α i) i))
⊢ IsLUB x✝ (sSup x✝)

Tactic:
by exact isLUB_sSup

Goal state after:
Module: Mathlib.Order.Concept

Goal state before:
pp: α : Type u_2
r' : α → α → Prop
c' : Concept α α r'
inst✝¹ : Std.Trichotomous r'
inst✝ : IsTrans α r'
⊢ ⊤ ⊆ c'.extent ⊔ c'.intent

Tactic:
refine fun x _ ↦ or_iff_not_imp_left.2 fun hx ↦ ?_

Goal state after:
α : Type u_2
r' : α → α → Prop
c' : Concept α α r'
inst✝¹ : Std.Trichotomous r'
inst✝ : IsTrans α r'
x : α
x✝ : x ∈ ⊤
hx : x ∉ c'.extent
⊢ x ∈ c'.intent
Module: Mathlib.Order.Completion

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a b : DedekindCut α
h : a.extent ⊂ b.extent
⊢ ∃ c, a < principal c ∧ principal c ≤ b

Tactic:
Set.ssubset_iff_exists

Goal state after:
α : Type u_1
inst✝ : LinearOrder α
a b : DedekindCut α
h : a.extent ⊆ b.extent ∧ ∃ x ∈ b.extent, x ∉ a.extent
⊢ ∃ c, a < principal c ∧ principal c ≤ b
Module: Mathlib.Order.Completion

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a b : DedekindCut α
h : b.intent ⊂ a.intent
⊢ ∃ c, a ≤ principal c ∧ principal c < b

Tactic:
Set.ssubset_iff_exists

Goal state after:
α : Type u_1
inst✝ : LinearOrder α
a b : DedekindCut α
h : b.intent ⊆ a.intent ∧ ∃ x ∈ a.intent, x ∉ b.intent
⊢ ∃ c, a ≤ principal c ∧ principal c < b
Module: Mathlib.SetTheory.Ordinal.Rank

Goal state before:
pp: α : Type u
a : α
r : α → α → Prop
hwf : IsWellFounded α r
b : α
hb : Acc r b
h : hb.rank ≤ rank r a
⊢ hb.rank ∈ Set.range (rank r)

Tactic:
exact ⟨b, rfl⟩

Goal state after:
Module: Mathlib.Order.CountableSupClosed

Goal state before:
pp: α : Type u_2
β : Type u_3
inst✝¹ : Preorder α
inst✝ : Preorder β
s : Set α
t : Set β
a : α
b : β
hb : ∃ A, ∃ (_ : A ⊆ t) (_ : A.Nonempty) (_ : A.Countable), IsLUB A b
u : Set α
hu : u ⊆ s
hu_ne : u.Nonempty
hu_c : u.Countable
hu_lub : IsLUB u a
⊢ ∃ A, ∃ (_ : A ⊆ s ×ˢ t) (_ : A.Nonempty) (_ : A.Countable), IsLUB A (a, b)

Tactic:
obtain ⟨v, hv, hv_ne, hv_c, hv_lub⟩ := hb

Goal state after:
α : Type u_2
β : Type u_3
inst✝¹ : Preorder α
inst✝ : Preorder β
s : Set α
t : Set β
a : α
b : β
u : Set α
hu : u ⊆ s
hu_ne : u.Nonempty
hu_c : u.Countable
hu_lub : IsLUB u a
v : Set β
hv : v ⊆ t
hv_ne : v.Nonempty
hv_c : v.Countable
hv_lub : IsLUB v b
⊢ ∃ A, ∃ (_ : A ⊆ s ×ˢ t) (_ : A.Nonempty) (_ : A.Countable), IsLUB A (a, b)
Module: Mathlib.Order.Filter.Cocardinal

Goal state before:
pp: α : Type u
c : Cardinal.{u}
hreg : c.IsRegular
S : Set (Set α)
hS : #↑S < c
hSs : ∀ s ∈ S, s ∈ cocardinal α hreg
⊢ #↑(compl '' S) < c.ord.cof

Tactic:
rw [hreg.cof_ord]
      exact mk_image_le.trans_lt hS

Goal state after:
Module: Mathlib.Order.KonigLemma

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

Tactic:
exact congr_arg Sigma.fst <| h' (i + 1) (π hle' b) ⟨by simp, by rw [π_trans]⟩ ⟨hle', by simp⟩
        (fun h ↦ by simp at h)

Goal state after: