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

Goal state before:
pp: g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
⊢ (g = 1 ∨ g = -1) ∨
    (g = T ∨ g = -T) ∧ z.re = -1 / 2 ∨
      (g = T⁻¹ ∨ g = -T⁻¹) ∧ z.re = 1 / 2 ∨
        (g = S ∨ g = -S) ∧ ‖↑z‖ = 1 ∨
          (g = T * S ∨ g = -(T * S)) ∧ z = 1 +ᵥ ρ ∨
            (g = T⁻¹ * S * T⁻¹ ∨ g = -(T⁻¹ * S * T⁻¹)) ∧ z = 1 +ᵥ ρ ∨
              (g = S * T⁻¹ ∨ g = -(S * T⁻¹)) ∧ z = 1 +ᵥ ρ ∨
                (g = S * T ∨ g = -(S * T)) ∧ z = ρ ∨
                  (g = T * S * T ∨ g = -(T * S * T)) ∧ z = ρ ∨ (g = T⁻¹ * S ∨ g = -(T⁻¹ * S)) ∧ z = ρ

Tactic:
by
  have him : (g • z).im = z.im := serreTheorem_im_eq hz hg
  wlog hc : 0 ≤ g 1 0
  · simpa [neg_eq_iff_eq_neg, or_comm] using @this (-g) z hz (by simpa using hg)
      (by simpa using him) (by simpa using (not_le.mp hc).le)
  rw [im_smul_eq_div_normSq, div_eq_iff (normSq_denom_pos _ z.im_ne_zero).ne',
    eq_comm, mul_eq_left₀ z.im_ne_zero, normSq_eq_norm_sq,
    pow_eq_one_iff_of_nonneg (norm_nonneg _) two_ne_zero] at him
  have hc : g 1 0 = 0 ∨ g 1 0 = 1 := by grind [abs_c_le_one hz hg]
  rcases hc with hc | hc
  · grind [cases_c_zero hz hg hc] -- ± T, T⁻¹
  · rcases Int.abs_le_one_iff.mp (cases_d_of_c_eq_one hz him.le hc) with hd | hd | hd
    · grind [cases_c_one_d_zero hz hg him.le hc hd] -- ± S, T⁻¹S, TS
    · grind [case_c_one_d_one hz hg him.le hc hd] -- ± ST, TST
    · grind [case_c_one_d_neg_one hz hg him.le hc hd]

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.OneVariable

Goal state before:
pp: τ : ℍ
h0 : ↑τ ≠ 0
⊢ (-I * ↑τ) ^ (1 / 2) ≠ 0

Tactic:
Ne,

Goal state after:
τ : ℍ
h0 : ↑τ ≠ 0
⊢ ¬(-I * ↑τ) ^ (1 / 2) = 0
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion

Goal state before:
pp: k : ℕ
hk : 3 ≤ k
z : ℍ
hk1 : 1 < k
hk2 : 3 ≤ ↑k
b : ℕ
⊢ Summable fun c ↦ (↑(b, c).1 ^ k)⁻¹ * eisSummand (↑k) (↑(b, c).2) z

Tactic:
simpa using ((summable_norm_eisSummand hk2 z).subtype _).of_norm.mul_left (a := ((b : ℂ) ^ k)⁻¹)

Goal state after:
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: case right
y : ℝ
z : ℂ
hz : z ∈ {z | 0 ≤ z.im ∧ z.im ≤ y ∧ |z.re| ≤ 1 / 2 ∧ 1 ≤ ‖z‖}
⊢ ‖z‖ ^ 2 ≤ (1 / 2) ^ 2 + y ^ 2

Tactic:
Complex.norm_eq_sqrt_sq_add_sq,

Goal state after:
case right
y : ℝ
z : ℂ
hz : z ∈ {z | 0 ≤ z.im ∧ z.im ≤ y ∧ |z.re| ≤ 1 / 2 ∧ 1 ≤ ‖z‖}
⊢ √(z.re ^ 2 + z.im ^ 2) ^ 2 ≤ (1 / 2) ^ 2 + y ^ 2
Module: Mathlib.Topology.Algebra.RestrictedProduct.Basic

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

Tactic:
ext; simp [Pi.mulSingle_div]

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

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

Tactic:
ext; simp [Pi.mulSingle_pow, RestrictedProduct.pow_apply]

Goal state after:
Module: Mathlib.NumberTheory.Multiplicity

Goal state before:
pp: case succ
p : ℕ
hp : Prime ↑p
hp1 : Odd p
x y : ℤ
hxy : ↑p ∣ x - y
hx : ¬↑p ∣ x
n : ℕ
h : FiniteMultiplicity p (n + 1)
hpn : ¬p ^ (multiplicity p (n + 1) + 1) ∣ n + 1
k : ℕ
hk : n + 1 = p ^ multiplicity p (n + 1) * k
⊢ emultiplicity (↑p) ((x ^ p ^ multiplicity p (n + 1)) ^ k - (y ^ p ^ multiplicity p (n + 1)) ^ k) =
    emultiplicity (↑p) (x - y) + emultiplicity p (n + 1)

Tactic:
emultiplicity_pow_sub_pow_of_prime hp,

Goal state after:
case succ
p : ℕ
hp : Prime ↑p
hp1 : Odd p
x y : ℤ
hxy : ↑p ∣ x - y
hx : ¬↑p ∣ x
n : ℕ
h : FiniteMultiplicity p (n + 1)
hpn : ¬p ^ (multiplicity p (n + 1) + 1) ∣ n + 1
k : ℕ
hk : n + 1 = p ^ multiplicity p (n + 1) * k
⊢ emultiplicity (↑p) (x ^ p ^ multiplicity p (n + 1) - y ^ p ^ multiplicity p (n + 1)) =
    emultiplicity (↑p) (x - y) + emultiplicity p (n + 1)

case succ.hxy
p : ℕ
hp : Prime ↑p
hp1 : Odd p
x y : ℤ
hxy : ↑p ∣ x - y
hx : ¬↑p ∣ x
n : ℕ
h : FiniteMultiplicity p (n + 1)
hpn : ¬p ^ (multiplicity p (n + 1) + 1) ∣ n + 1
k : ℕ
hk : n + 1 = p ^ multiplicity p (n + 1) * k
⊢ ↑p ∣ x ^ p ^ multiplicity p (n + 1) - y ^ p ^ multiplicity p (n + 1)

case succ.hx
p : ℕ
hp : Prime ↑p
hp1 : Odd p
x y : ℤ
hxy : ↑p ∣ x - y
hx : ¬↑p ∣ x
n : ℕ
h : FiniteMultiplicity p (n + 1)
hpn : ¬p ^ (multiplicity p (n + 1) + 1) ∣ n + 1
k : ℕ
hk : n + 1 = p ^ multiplicity p (n + 1) * k
⊢ ¬↑p ∣ x ^ p ^ multiplicity p (n + 1)

case succ.hn
p : ℕ
hp : Prime ↑p
hp1 : Odd p
x y : ℤ
hxy : ↑p ∣ x - y
hx : ¬↑p ∣ x
n : ℕ
h : FiniteMultiplicity p (n + 1)
hpn : ¬p ^ (multiplicity p (n + 1) + 1) ∣ n + 1
k : ℕ
hk : n + 1 = p ^ multiplicity p (n + 1) * k
⊢ ¬↑p ∣ ↑k
Module: Mathlib.NumberTheory.NumberField.CMField

Goal state before:
pp: K : Type u_1
inst✝³ : Field K
inst✝² : CharZero K
inst✝¹ : IsCMField K
inst✝ : Algebra.IsIntegral ℚ K
φ : K →+* ℂ
σ : Gal(K/↥K⁺)
hσ : ComplexEmbedding.IsConj φ σ
this : ComplexEmbedding.IsConj (Classical.choice ⋯) ⋯.choose
⊢ ComplexEmbedding.IsConj φ (complexConj K)

Tactic:
isConj_eq_isConj K hσ this

Goal state after:
K : Type u_1
inst✝³ : Field K
inst✝² : CharZero K
inst✝¹ : IsCMField K
inst✝ : Algebra.IsIntegral ℚ K
φ : K →+* ℂ
σ : Gal(K/↥K⁺)
hσ : ComplexEmbedding.IsConj φ ⋯.choose
this : ComplexEmbedding.IsConj (Classical.choice ⋯) ⋯.choose
⊢ ComplexEmbedding.IsConj φ (complexConj K)
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
A : Set (mixedSpace K)
inst✝ : NumberField K
hA : normAtAllPlaces ⁻¹' normAtAllPlaces '' A = A
hm : MeasurableSet A
hA₁ : ∀ (x : mixedSpace K), x ∈ A ↔ (fun w ↦ ‖x.1 w‖, x.2) ∈ A
hA₃ : normAtComplexPlaces ⁻¹' normAtComplexPlaces '' plusPart A = plusPart A
w : { w // w.IsReal }
⊢ volume {x | x ↑w ≠ 0}ᶜ = 0

Tactic:
rw [show {x : realSpace K | x w.1 ≠ 0}ᶜ = {x | x w.1 = 0} by ext; simp]

Goal state after:
K : Type u_1
inst✝¹ : Field K
A : Set (mixedSpace K)
inst✝ : NumberField K
hA : normAtAllPlaces ⁻¹' normAtAllPlaces '' A = A
hm : MeasurableSet A
hA₁ : ∀ (x : mixedSpace K), x ∈ A ↔ (fun w ↦ ‖x.1 w‖, x.2) ∈ A
hA₃ : normAtComplexPlaces ⁻¹' normAtComplexPlaces '' plusPart A = plusPart A
w : { w // w.IsReal }
⊢ volume {x | x ↑w = 0} = 0
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x y : mixedSpace K
c : ℝ
J : ↥(Ideal (𝓞 K))⁰
n : ℕ
x✝ : ↑(integerSet K)
⊢ mixedEmbedding.norm ↑x✝ = ↑n ∧ ↑(preimageOfMemIntegerSet x✝) ∈ ↑J ↔
    ↑(preimageOfMemIntegerSet x✝) ∈ ↑J ∧ mixedEmbedding.norm ↑x✝ = ↑n

Tactic:
simp [and_comm]

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : K
hx : x ≠ 0
⊢ ∑ w, ↑expMap.symm (normAtAllPlaces ((mixedEmbedding K) x)) w = ∑ x_1, ↑x_1.mult * Real.log (x_1 x)

Tactic:
expMap_symm_apply,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : K
hx : x ≠ 0
⊢ ∑ w, ↑w.mult * Real.log (normAtAllPlaces ((mixedEmbedding K) x) w) = ∑ x_1, ↑x_1.mult * Real.log (x_1 x)
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : K
hx : x ≠ 0
w : { w // w ≠ w₀ }
⊢ ↑expMap.symm (normAtAllPlaces ((mixedEmbedding K) x)) ↑w -
      ↑(↑w).mult * Real.log ↑|(Algebra.norm ℚ) x| * (↑(finrank ℚ K))⁻¹ =
    logMap ((mixedEmbedding K) x) w

Tactic:
expMap_symm_apply,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : K
hx : x ≠ 0
w : { w // w ≠ w₀ }
⊢ ↑(↑w).mult * Real.log (normAtAllPlaces ((mixedEmbedding K) x) ↑w) -
      ↑(↑w).mult * Real.log ↑|(Algebra.norm ℚ) x| * (↑(finrank ℚ K))⁻¹ =
    logMap ((mixedEmbedding K) x) w
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne

Goal state before:
pp: case neg
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w i : InfinitePlace K
hw : ¬w = w₀
⊢ ↑expMap.symm (normAtAllPlaces ((mixedEmbedding K) ((algebraMap (𝓞 K) K) ↑(fundSystem K (equivFinRank.symm ⟨w, hw⟩)))))
      i =
    ↑i.mult * Real.log (i ((algebraMap (𝓞 K) K) ↑(fundSystem K (equivFinRank.symm ⟨w, hw⟩))))

Tactic:
expMap_symm_apply,

Goal state after:
case neg
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w i : InfinitePlace K
hw : ¬w = w₀
⊢ ↑i.mult *
      Real.log
        (normAtAllPlaces ((mixedEmbedding K) ((algebraMap (𝓞 K) K) ↑(fundSystem K (equivFinRank.symm ⟨w, hw⟩)))) i) =
    ↑i.mult * Real.log (i ((algebraMap (𝓞 K) K) ↑(fundSystem K (equivFinRank.symm ⟨w, hw⟩))))
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : realSpace K
w : InfinitePlace K
hw : w ≠ w₀
⊢ (∑ x_1,
          x ↑x_1 •
            (Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K)).repr fun i ↦
              ↑expMap.symm
                (normAtAllPlaces ((mixedEmbedding K) ((algebraMap (𝓞 K) K) ↑(fundSystem K (equivFinRank.symm x_1)))))
                ↑i)
        (equivFinRank.symm ⟨w, hw⟩) ∈
      Set.Ico 0 1 ↔
    x w ∈ Set.Ico 0 1

Tactic:
expMap_symm_apply,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : realSpace K
w : InfinitePlace K
hw : w ≠ w₀
⊢ (∑ x_1,
          x ↑x_1 •
            (Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K)).repr fun i ↦
              ↑(↑i).mult *
                Real.log
                  (normAtAllPlaces ((mixedEmbedding K) ((algebraMap (𝓞 K) K) ↑(fundSystem K (equivFinRank.symm x_1))))
                    ↑i))
        (equivFinRank.symm ⟨w, hw⟩) ∈
      Set.Ico 0 1 ↔
    x w ∈ Set.Ico 0 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_1.mult)⁻¹ * (completeBasis K).equivFun.symm x x_1) * (↑x_1.mult)⁻¹ =
    Real.exp (x w₀) ^ finrank ℚ K * (∏ w, ↑expMapBasis x ↑w)⁻¹ * 2⁻¹ ^ nrComplexPlaces K

Tactic:
rw [Finset.prod_mul_distrib]

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : realSpace K
⊢ (∏ x_1, Real.exp ((↑x_1.mult)⁻¹ * (completeBasis K).equivFun.symm x x_1)) * ∏ x, (↑x.mult)⁻¹ =
    Real.exp (x w₀) ^ finrank ℚ K * (∏ w, ↑expMapBasis x ↑w)⁻¹ * 2⁻¹ ^ nrComplexPlaces K
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Galois

Goal state before:
pp: n : ℕ
inst✝² : NeZero n
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
hK : IsCyclotomicExtension {n} ℚ K
σ : Gal(K/ℚ)
x : 𝓞 K
hx : x ^ n = 1
⊢ σ • x = x ^ (↑((galEquivZMod n K) σ)).val

Tactic:
apply FaithfulSMul.algebraMap_injective (𝓞 K) K

Goal state after:
n : ℕ
inst✝² : NeZero n
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
hK : IsCyclotomicExtension {n} ℚ K
σ : Gal(K/ℚ)
x : 𝓞 K
hx : x ^ n = 1
⊢ (algebraMap (𝓞 K) K) (σ • x) = (algebraMap (𝓞 K) K) (x ^ (↑((galEquivZMod n K) σ)).val)
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ closure (normAtAllPlaces ⁻¹' ↑expMapBasis '' paramSet K) ⊆ normAtAllPlaces ⁻¹' compactSet K

Tactic:
refine ((continuous_normAtAllPlaces K).closure_preimage_subset _).trans (Set.preimage_mono ?_)

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ closure (↑expMapBasis '' paramSet K) ⊆ compactSet K
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
hK : IsCyclotomicExtension {p} ℚ K
P : Ideal (𝓞 K)
hP₁ : P.IsPrime
hP₂ : P.LiesOver 𝒑
⊢ (span {⋯.toInteger - 1}).ramificationIdx ℤ = p - 1

Tactic:
ramificationIdx_span_zeta_sub_one'

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
hK : IsCyclotomicExtension {p} ℚ K
P : Ideal (𝓞 K)
hP₁ : P.IsPrime
hP₂ : P.LiesOver 𝒑
⊢ p - 1 = p - 1
Module: Mathlib.NumberTheory.NumberField.DedekindZeta

Goal state before:
pp: case e_a
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
n : ℕ
⊢ Nat.card { I // absNorm I ≤ n } =
    ∑ x ∈ Finset.Ioc 0 n, Nat.card { I // absNorm I = x } + Nat.card { I // absNorm I = 0 }

Tactic:
Finset.sum_Ioc_add_eq_sum_Icc (n.zero_le),

Goal state after:
case e_a
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
n : ℕ
⊢ Nat.card { I // absNorm I ≤ n } = ∑ x ∈ Finset.Icc 0 n, Nat.card { I // absNorm I = x }
Module: Mathlib.NumberTheory.NumberField.ExistsRamified

Goal state before:
pp: case right
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
this✝ : 0 < Module.finrank ℚ K
this : 2 < |discr K|
p : ℤ
hp1 : Prime p
hp2 : p ∣ discr K
⊢ ¬Algebra.IsUnramifiedIn 𝒪 (Ideal.span {↑p.natAbs})

Tactic:
simpa [← not_dvd_discr_iff_isUnramifiedIn K 𝒪 hp1]

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

Goal state before:
pp: K : Type u_1
inst✝² : Field K
inst✝¹ : NumberField K
α : Type u_2
β : Type u_3
a : Matrix α β (𝓞 K)
x : β × (K →+* ℂ) → ℤ
hxl : x ≠ 0
inst✝ : Fintype β
hmulvec0 : asiegel K a *ᵥ x = 0
k : α
u : K →+* ℂ
hξ : ξ K x ≠ 0
⊢ ∑ r, ∑ l, ↑(a' K a k l r u) * ↑(x (l, r)) = 0

Tactic:
Ne,

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 : α
u : K →+* ℂ
hξ : ¬ξ K x = 0
⊢ ∑ r, ∑ l, ↑(a' K a k l r u) * ↑(x (l, r)) = 0
Module: Mathlib.NumberTheory.Ostrowski

Goal state before:
pp: f : AbsoluteValue ℚ ℝ
hf_nontriv : f.IsNontrivial
bdd : ∀ (n : ℕ), f ↑n ≤ 1
n : ℕ
hn1 : n ≠ 0
hn2 : f ↑n ≠ 1
⊢ ∃ p, (0 < f ↑p ∧ f ↑p < 1) ∧ ∀ (m : ℕ), 0 < f ↑m ∧ f ↑m < 1 → p ≤ m

Tactic:
set P := {m : ℕ | 0 < f ↑m ∧ f ↑m < 1}

Goal state after:
f : AbsoluteValue ℚ ℝ
hf_nontriv : f.IsNontrivial
bdd : ∀ (n : ℕ), f ↑n ≤ 1
n : ℕ
hn1 : n ≠ 0
hn2 : f ↑n ≠ 1
P : Set ℕ := {m | 0 < f ↑m ∧ f ↑m < 1}
⊢ ∃ p, (0 < f ↑p ∧ f ↑p < 1) ∧ ∀ (m : ℕ), 0 < f ↑m ∧ f ↑m < 1 → p ≤ m
Module: Mathlib.NumberTheory.SiegelsLemma

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
inst✝³ : Fintype α
inst✝² : Fintype β
A : Matrix α β ℤ
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
hn : m < n
hm : 0 < m
i : α
x✝ : i ∈ univ
h1 : ↑n * max 1 ‖A‖ * ↑B = ∑ x, max 1 ‖A‖ * ↑B
⊢ ∑ x, ↑B * (↑(A i x)⁺ + ↑(A i x)⁻) ≤ ∑ x, ↑B * max 1 ‖A‖

Tactic:
← Int.cast_add

Goal state after:
case refine_2
α : Type u_1
β : Type u_2
inst✝³ : Fintype α
inst✝² : Fintype β
A : Matrix α β ℤ
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
hn : m < n
hm : 0 < m
i : α
x✝ : i ∈ univ
h1 : ↑n * max 1 ‖A‖ * ↑B = ∑ x, max 1 ‖A‖ * ↑B
⊢ ∑ x, ↑B * ↑((A i x)⁺ + (A i x)⁻) ≤ ∑ x, ↑B * max 1 ‖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)
inst✝² : Fintype β
A : ℝ
habs : ∀ (k : α) (l : β), house ((algebraMap (𝓞 K) K) (a k l)) ≤ A
inst✝¹ : DecidableEq (K →+* ℂ)
inst✝ : Fintype α
Apos : 0 ≤ A
⊢ ‖asiegel K a‖ ≤ c₂ K * A

Tactic:
have := c_nonneg K

Goal state after:
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
⊢ ‖asiegel K a‖ ≤ c₂ K * A
Module: Mathlib.NumberTheory.Padics.Complex

Goal state before:
pp: case h
p : ℕ
hp : Fact (Nat.Prime p)
x : PadicAlgCl p
⊢ ‖x‖ = ↑(embedding (Valued.v.restrict ↑x))

Tactic:
embedding_restrict (PadicComplex.valued p).v x,

Goal state after:
case h
p : ℕ
hp : Fact (Nat.Prime p)
x : PadicAlgCl p
⊢ ‖x‖ = ↑(Valued.v ↑x)
Module: Mathlib.NumberTheory.Padics.MahlerBasis

Goal state before:
pp: M : Type u_1
G : Type u_2
inst✝¹ : AddCommMonoidWithOne M
inst✝ : AddCommGroup G
f : M → G
n R : ℕ
hR : 1 ≤ R
aux : Δ_[1]^[n + R] f 0 = R.choose (R - 1 + 1) • Δ_[1]^[n + R] f 0
⊢ Δ_[1]^[n + R] f 0 =
    -∑ j ∈ range (R - 1), R.choose (j + 1) • Δ_[1]^[n + (j + 1)] f 0 +
      ∑ k ∈ range (n + 1), ((-1) ^ (n - k) * ↑(n.choose k)) • (f (↑k + ↑R) - f ↑k)

Tactic:
neg_add_eq_sub,

Goal state after:
M : Type u_1
G : Type u_2
inst✝¹ : AddCommMonoidWithOne M
inst✝ : AddCommGroup G
f : M → G
n R : ℕ
hR : 1 ≤ R
aux : Δ_[1]^[n + R] f 0 = R.choose (R - 1 + 1) • Δ_[1]^[n + R] f 0
⊢ Δ_[1]^[n + R] f 0 =
    ∑ k ∈ range (n + 1), ((-1) ^ (n - k) * ↑(n.choose k)) • (f (↑k + ↑R) - f ↑k) -
      ∑ j ∈ range (R - 1), R.choose (j + 1) • Δ_[1]^[n + (j + 1)] f 0
Module: Mathlib.NumberTheory.Padics.WithVal

Goal state before:
pp: case right
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp0' : 0 < ↑p
hp0 : 0 < (↑p)⁻¹
hp1' : 1 < ↑p
hp1 : (↑p)⁻¹ < 1
⊢ ∀ (j : (MonoidWithZeroHom.ofClass Valued.v).ValueGroup₀ˣ),
    ∃ i,
      ∀ (x y : WithVal (Rat.padicValuation p)),
        ↑(padicNorm p ((WithVal.equiv (Rat.padicValuation p)) (x - y))) ≤ (↑p ^ i)⁻¹ → Valued.v.restrict (y - x) < ↑j

Tactic:
· intro γ
    use (log ((embedding γ.val) * exp (-1))).natAbs
    intro x y h
    set x' := (WithVal.equiv (Rat.padicValuation p)) x with hx
    set y' := (WithVal.equiv (Rat.padicValuation p)) y with hy
    rw [Valuation.map_sub_swap, Valuation.restrict_lt_iff_lt_embedding]
    change Rat.padicValuation p (x' - y') < embedding γ.1
    rw [← Nat.cast_pow, ← Rat.cast_natCast, ← Rat.cast_inv_of_ne_zero, Rat.cast_le] at h
    · change padicNorm p (x' - y') ≤ _ at h
      simp only [Rat.padicValuation, Valuation.coe_mk, MonoidWithZeroHom.coe_mk, ZeroHom.coe_mk,
        padicNorm, zpow_neg, Nat.cast_pow] at h ⊢
      split_ifs with H
      · simp only [exp_neg]
        exact embedding_unit_pos _
      · rw [← lt_log_iff_exp_lt (embedding_unit_ne_zero _)]
        simp_all [← zpow_natCast, zpow_pos, inv_le_inv₀, zpow_le_zpow_iff_right₀ hp1', abs_le,
          Int.lt_iff_add_one_le]
    · simp [Nat.Prime.ne_zero Fact.out]

Goal state after:
Module: Mathlib.Topology.Separation.DisjointCover

Goal state before:
pp: X : Type u_1
inst✝³ : TopologicalSpace X
S : Set (X × X)
inst✝² : CompactSpace X
inst✝¹ : TotallyDisconnectedSpace X
inst✝ : T2Space X
hS : S ∈ 𝓝ˢ (diagonal X)
t : Finset X
U : ↥t → Opens X
hUc : IsOpenCover U
hUS : ∀ (i : ↥t), ↑(U i) ×ˢ ↑(U i) ⊆ S
n : ℕ
W : Fin n → Clopens X
hW₁ : ∀ (j : Fin n), W j ≠ ⊥ ∧ ∃ i, ↑(W j) ⊆ ↑(U i)
hW₂ : univ ⊆ ⋃ j, ↑(W j)
hW₃ : Pairwise (Disjoint on W)
⊢ ∃ n D,
    (∀ (i : Fin n), D i ≠ ⊥) ∧
      (∀ (i : Fin n), ∀ y ∈ D i, ∀ z ∈ D i, (y, z) ∈ S) ∧ univ ⊆ ⋃ i, ↑(D i) ∧ Pairwise (Disjoint on D)

Tactic:
refine ⟨n, W, fun j ↦ (hW₁ j).1, fun j y hy z hz ↦ ?_, hW₂, hW₃⟩

Goal state after:
X : Type u_1
inst✝³ : TopologicalSpace X
S : Set (X × X)
inst✝² : CompactSpace X
inst✝¹ : TotallyDisconnectedSpace X
inst✝ : T2Space X
hS : S ∈ 𝓝ˢ (diagonal X)
t : Finset X
U : ↥t → Opens X
hUc : IsOpenCover U
hUS : ∀ (i : ↥t), ↑(U i) ×ˢ ↑(U i) ⊆ S
n : ℕ
W : Fin n → Clopens X
hW₁ : ∀ (j : Fin n), W j ≠ ⊥ ∧ ∃ i, ↑(W j) ⊆ ↑(U i)
hW₂ : univ ⊆ ⋃ j, ↑(W j)
hW₃ : Pairwise (Disjoint on W)
j : Fin n
y : X
hy : y ∈ W j
z : X
hz : z ∈ W j
⊢ (y, z) ∈ S
Module: Mathlib.NumberTheory.Padics.HeightOneSpectrum

Goal state before:
pp: case refine_2
R : Type u_2
inst✝⁴ : CommRing R
inst✝³ : Algebra R ℚ
inst✝² : IsIntegralClosure R ℤ ℚ
inst✝¹ : IsDedekindDomain R
inst✝ : IsFractionRing R ℚ
v : HeightOneSpectrum R
y : ℚ_[↑(primesEquiv v)]
hy : y ∈ ↑(subring ↑(primesEquiv v))
⊢ y ∈ ⇑(padicEquiv v) '' ↑(HeightOneSpectrum.adicCompletionIntegers ℚ v)

Tactic:
· obtain ⟨x, hx⟩ := (adicCompletionIntegers.padicIntEquiv v).surjective ⟨y, hy⟩
    refine ⟨x, x.2, by rw [← adicCompletionIntegers.coe_padicIntEquiv_apply, hx]⟩

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

Goal state before:
pp: R✝ : Type u_1
inst✝⁷ : CommRing R✝
inst✝⁶ : Algebra R✝ ℚ
inst✝⁵ : IsIntegralClosure R✝ ℤ ℚ
R : Type u_2
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
inst✝² : Algebra R ℚ
inst✝¹ : IsFractionRing R ℚ
inst✝ : IsIntegralClosure R ℤ ℚ
p : Nat.Primes
⊢ ℤ_[↑p] ≃A[ℤ] ↥(HeightOneSpectrum.adicCompletionIntegers ℚ (primesEquiv.symm p))

Tactic:
apply (ContinuousAlgEquiv.cast (primesEquiv.apply_symm_apply p).symm).trans
    (adicCompletionIntegers.padicIntEquiv (primesEquiv.symm p)).symm

Goal state after:
Module: Mathlib.NumberTheory.Pell

Goal state before:
pp: d : ℤ
a : Solution₁ d
hax : 0 < a.x
n : ℤ
⊢ 0 < (a ^ n).x

Tactic:
cases n with
  | ofNat n =>
    rw [Int.ofNat_eq_natCast, zpow_natCast]
    exact x_pow_pos hax n
  | negSucc n =>
    rw [zpow_negSucc]
    exact x_pow_pos hax (n + 1)

Goal state after:
Module: Mathlib.NumberTheory.Pell

Goal state before:
pp: d : ℤ
h₀ : 0 < d
⊢ (∃ x y, x ^ 2 - d * y ^ 2 = 1 ∧ y ≠ 0) ↔ ¬IsSquare d

Tactic:
refine ⟨?_, exists_of_not_isSquare h₀⟩
  rintro ⟨x, y, hxy, hy⟩ ⟨a, rfl⟩
  rw [← sq, ← mul_pow, sq_sub_sq] at hxy
  simpa [hy, mul_self_pos.mp h₀, sub_eq_add_neg, eq_neg_self_iff] using Int.eq_of_mul_eq_one hxy

Goal state after:
Module: Mathlib.NumberTheory.Pell

Goal state before:
pp: d : ℤ
a₁ : Solution₁ d
h : IsFundamental a₁
a : Solution₁ d
hax : 1 < a.x
hay : 0 < a.y
H : d * (a₁.y ^ 2 - a.y ^ 2) = a₁.x ^ 2 - a.x ^ 2
⊢ a₁.y ≤ a.y

Tactic:
rw [← abs_of_pos hay, ← abs_of_pos h.2.1, ← sq_le_sq, ← mul_le_mul_iff_right₀ h.d_pos,
    ← sub_nonpos, ← mul_sub, H, sub_nonpos, sq_le_sq, abs_of_pos (zero_lt_one.trans h.1),
    abs_of_pos (zero_lt_one.trans hax)]

Goal state after:
d : ℤ
a₁ : Solution₁ d
h : IsFundamental a₁
a : Solution₁ d
hax : 1 < a.x
hay : 0 < a.y
H : d * (a₁.y ^ 2 - a.y ^ 2) = a₁.x ^ 2 - a.x ^ 2
⊢ a₁.x ≤ a.x