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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : realMixedSpace K
w : InfinitePlace K
hw : w.IsComplex
⊢ (normAtPlace w) (↑(mixedEmbedding.polarCoord K).symm x) = ‖(x.2 ⟨w, hw⟩).1‖

Tactic:
by
  simp [normAtPlace_apply_of_isComplex hw]

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
ζ : (𝓞 K)ˣ
hζ : ζ ∈ torsion K
x✝ : { w // w ≠ w₀ }
⊢ ↑(↑x✝).mult *
      (Real.log ((normAtPlace ↑x✝) ((mixedEmbedding K) ((algebraMap (𝓞 K) K) ↑ζ)) * (normAtPlace ↑x✝) x) -
        Real.log (mixedEmbedding.norm x) * (↑(finrank ℚ K))⁻¹) =
    ↑(↑x✝).mult * (Real.log ((normAtPlace ↑x✝) x) - Real.log (mixedEmbedding.norm x) * (↑(finrank ℚ K))⁻¹)

Tactic:
normAtPlace_apply,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
ζ : (𝓞 K)ˣ
hζ : ζ ∈ torsion K
x✝ : { w // w ≠ w₀ }
⊢ ↑(↑x✝).mult *
      (Real.log (↑x✝ ((algebraMap (𝓞 K) K) ↑ζ) * (normAtPlace ↑x✝) x) -
        Real.log (mixedEmbedding.norm x) * (↑(finrank ℚ K))⁻¹) =
    ↑(↑x✝).mult * (Real.log ((normAtPlace ↑x✝) x) - Real.log (mixedEmbedding.norm x) * (↑(finrank ℚ K))⁻¹)
Module: Mathlib.NumberTheory.NumberField.CMField

Goal state before:
pp: K : Type u_1
inst✝³ : Field K
inst✝² : CharZero K
inst✝¹ : IsCMField K
inst✝ : NumberField K
⊢ indexRealUnits K = 1 ∨ indexRealUnits K = 2

Tactic:
have h₁ := indexRealUnits_mul_eq K

Goal state after:
K : Type u_1
inst✝³ : Field K
inst✝² : CharZero K
inst✝¹ : IsCMField K
inst✝ : NumberField K
h₁ : indexRealUnits K * (unitsMulComplexConjInv K).range.index = 2
⊢ indexRealUnits K = 1 ∨ indexRealUnits K = 2
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))⁰
x✝¹ x✝ : ↑(idealSet K J)
h : ↑(idealSetMap K J x✝¹) = ↑(idealSetMap K J x✝)
⊢ x✝¹ = x✝

Tactic:
idealSetMap_apply

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x y : mixedSpace K
c : ℝ
J : ↥(Ideal (𝓞 K))⁰
x✝¹ x✝ : ↑(idealSet K J)
h : ↑x✝¹ = ↑x✝
⊢ x✝¹ = x✝
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne

Goal state before:
pp: K : Type u_1
inst✝ : Field K
w : InfinitePlace K
x✝ : ℝ
h : x✝ ∈ Set.Ioi 0
⊢ Real.exp ((↑w.mult)⁻¹ * (↑w.mult * Real.log x✝)) = x✝

Tactic:
simp only [inv_mul_cancel_left₀ mult_coe_ne_zero, Real.exp_log h]

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 : { w // w ≠ w₀ }
⊢ ↑(↑w).mult * Real.log (normAtAllPlaces ((mixedEmbedding K) x) ↑w) -
      ↑(↑w).mult * Real.log ↑|(Algebra.norm ℚ) x| * (↑(finrank ℚ K))⁻¹ =
    ↑(↑w).mult *
      (Real.log ((normAtPlace ↑w) ((mixedEmbedding K) x)) -
        Real.log (mixedEmbedding.norm ((mixedEmbedding K) x)) * (↑(finrank ℚ K))⁻¹)

Tactic:
normAtPlace_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 (↑w x) - ↑(↑w).mult * Real.log ↑|(Algebra.norm ℚ) x| * (↑(finrank ℚ K))⁻¹ =
    ↑(↑w).mult * (Real.log (↑w x) - Real.log (mixedEmbedding.norm ((mixedEmbedding K) x)) * (↑(finrank ℚ K))⁻¹)
Module: Mathlib.NumberTheory.NumberField.Ideal.KummerDedekind

Goal state before:
pp: K : Type u_1
inst✝ : Field K
θ : 𝓞 K
⊢ absNorm (under ℤ (conductor ℤ θ)) = 1 ↔ ℤ[θ] = ⊤

Tactic:
absNorm_eq_one_iff,

Goal state after:
K : Type u_1
inst✝ : Field K
θ : 𝓞 K
⊢ under ℤ (conductor ℤ θ) = ⊤ ↔ ℤ[θ] = ⊤
Module: Mathlib.NumberTheory.NumberField.Ideal.KummerDedekind

Goal state before:
pp: K : Type u_1
inst✝² : Field K
θ✝ : 𝓞 K
inst✝¹ : NumberField K
θ : 𝓞 K
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : ¬p ∣ exponent θ
Q : ℤ[X]
hQ : Polynomial.map (Int.castRingHom (ZMod p)) Q ∈ monicFactorsMod θ p
h₀ : Polynomial.map (Int.castRingHom (ZMod p)) (minpoly ℤ θ) ≠ 0
⊢ span {Polynomial.map (Int.castRingHom (ZMod p)) Q} =
    span {Polynomial.map (Int.castRingHom (ZMod p)) Q, Polynomial.map (Int.castRingHom (ZMod p)) (minpoly ℤ θ)}

Tactic:
span_pair_eq_span_left_iff_dvd.mpr

Goal state after:
K : Type u_1
inst✝² : Field K
θ✝ : 𝓞 K
inst✝¹ : NumberField K
θ : 𝓞 K
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : ¬p ∣ exponent θ
Q : ℤ[X]
hQ : Polynomial.map (Int.castRingHom (ZMod p)) Q ∈ monicFactorsMod θ p
h₀ : Polynomial.map (Int.castRingHom (ZMod p)) (minpoly ℤ θ) ≠ 0
⊢ span {Polynomial.map (Int.castRingHom (ZMod p)) Q} = span {Polynomial.map (Int.castRingHom (ZMod p)) Q}

K : Type u_1
inst✝² : Field K
θ✝ : 𝓞 K
inst✝¹ : NumberField K
θ : 𝓞 K
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : ¬p ∣ exponent θ
Q : ℤ[X]
hQ : Polynomial.map (Int.castRingHom (ZMod p)) Q ∈ monicFactorsMod θ p
h₀ : Polynomial.map (Int.castRingHom (ZMod p)) (minpoly ℤ θ) ≠ 0
⊢ Polynomial.map (Int.castRingHom (ZMod p)) Q ∣ Polynomial.map (Int.castRingHom (ZMod p)) (minpoly ℤ θ)
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : realSpace K
hx : ∀ (w : InfinitePlace K), 0 < x w
h : ∀ (i : InfinitePlace K), ↑expMapBasis.symm x i ∈ if i = w₀ then Set.Iic 0 else Set.Ico 0 1
⊢ ↑expMapBasis.symm x w₀ ≤ 0

Tactic:
simpa using h w₀

Goal state after:
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))
n : ℤ
h : Associated ((Algebra.norm ℤ) (hζ.toInteger - 1)) ↑p
⊢ hζ.toInteger - 1 ∣ ↑n ↔ ↑p ∣ n

Tactic:
rw [← Ideal.norm_dvd_iff (h.symm.prime (Nat.prime_iff_prime_int.mp hp.out))]

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))
n : ℤ
h : Associated ((Algebra.norm ℤ) (hζ.toInteger - 1)) ↑p
⊢ (Algebra.norm ℤ) (hζ.toInteger - 1) ∣ n ↔ ↑p ∣ n
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ interior (paramSet K) ⊆ expMapBasis.source

Tactic:
by simp [expMapBasis_source]

Goal state after:
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
p : ℕ
hp : Fact (Nat.Prime p)
P : Ideal (𝓞 K)
inst✝¹ : P.IsMaximal
inst✝ : P.LiesOver (span {↑p})
hn : p.Coprime n
σ : Gal(K/ℚ)
hσ : σ ∈ stabilizer Gal(K/ℚ) P
hζ : IsPrimitiveRoot (zeta n ℚ K) n
τ : Gal((𝓞 K ⧸ P)/ℤ ⧸ span {↑p}) :=
  (IsFractionRing.stabilizerHom Gal(K/ℚ) (span {↑p}) P (ℤ ⧸ span {↑p}) (𝓞 K ⧸ P)) ⟨σ, hσ⟩
this✝ : CharP (ℤ ⧸ span {↑p}) p
this : Finite (𝓞 K ⧸ P)
i : ℕ
hi : ∀ (x : 𝓞 K ⧸ P), τ x = x ^ Nat.card (ℤ ⧸ span {↑p}) ^ i
⊢ (p ^ P.inertiaDeg ℤ).Coprime n

Tactic:
exact Nat.Coprime.pow_left _ hn

Goal state after:
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
R : Type u_2
inst✝² : CommRing R
inst✝¹ : HasEnoughRootsOfUnity R (Monoid.exponent (ZMod n)ˣ)
inst✝ : IsAbelianGalois ℚ K
F : IntermediateField ℚ K
⊢ Nat.card ↥((intermediateFieldEquivSubgroupChar n K R) F) = Module.finrank ℚ ↥F

Tactic:
by
  unfold intermediateFieldEquivSubgroupChar
  rw [OrderIso.trans_apply, OrderIso.trans_apply, OrderIso.dualDual_symm_apply,
    IsGalois.intermediateFieldEquivSubgroup_apply, OrderIso.dual_apply, OrderDual.ofDual_toDual,
    OrderDual.ofDual_toDual, card_subgroupGalEquivSubgroupChar, finrank_eq_fixingSubgroup_index,
    ← Subgroup.index_eq_card]

Goal state after:
Module: Mathlib.RingTheory.Unramified.Dedekind

Goal state before:
pp: A : Type u_1
B : Type u_2
inst✝⁶ : CommRing A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra A B
inst✝³ : Module.Finite A B
inst✝² : IsDedekindDomain A
inst✝¹ : IsDomain B
inst✝ : Algebra.FormallyUnramified A B
q : Ideal B
hq : q ≠ ⊥
hqp : q.IsPrime
q' : Ideal (Localization.AtPrime q) := IsLocalRing.maximalIdeal (Localization.AtPrime q)
⊢ IsDiscreteValuationRing (Localization.AtPrime q)

Tactic:
suffices q'.IsPrincipal from ((IsDiscreteValuationRing.TFAE (Localization.AtPrime q)
      (IsLocalization.AtPrime.not_isField B hq (Localization.AtPrime q))).out 4 0).mp this

Goal state after:
A : Type u_1
B : Type u_2
inst✝⁶ : CommRing A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra A B
inst✝³ : Module.Finite A B
inst✝² : IsDedekindDomain A
inst✝¹ : IsDomain B
inst✝ : Algebra.FormallyUnramified A B
q : Ideal B
hq : q ≠ ⊥
hqp : q.IsPrime
q' : Ideal (Localization.AtPrime q) := IsLocalRing.maximalIdeal (Localization.AtPrime q)
⊢ Submodule.IsPrincipal q'
Module: Mathlib.NumberTheory.NumberField.House

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
α : K
⊢ house α = ↑(univ.sup' ⋯ fun φ ↦ ‖φ α‖₊)

Tactic:
by
  rw [house, ← coe_nnnorm, nnnorm_eq, ← sup'_eq_sup univ_nonempty]

Goal state after:
Module: Mathlib.NumberTheory.Ostrowski

Goal state before:
pp: f : AbsoluteValue ℚ ℝ
p : ℕ
hp0 : 0 < f ↑p
hp1 : f ↑p < 1
hmin : ∀ (m : ℕ), 0 < f ↑m ∧ f ↑m < 1 → p ≤ m
hp2 : 2 ≤ p
⊢ ¬∃ m n, m < p ∧ n < p ∧ m * n = p

Tactic:
rintro ⟨a, b, ha, hb, rfl⟩

Goal state after:
f : AbsoluteValue ℚ ℝ
a b : ℕ
hp0 : 0 < f ↑(a * b)
hp1 : f ↑(a * b) < 1
hmin : ∀ (m : ℕ), 0 < f ↑m ∧ f ↑m < 1 → a * b ≤ m
hp2 : 2 ≤ a * b
ha : a < a * b
hb : b < a * b
⊢ False
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
⊢ ∑ x_1, ↑B * ↑(A i x_1)⁺ - ∑ x_1, ↑B * -↑(A i x_1)⁻ + 1 ≤ ↑n * max 1 ‖A‖ * ↑B + 1

Tactic:
simp only [mul_neg, sum_neg_distrib, sub_neg_eq_add, add_le_add_iff_right]
        have h1 : n * max 1 ‖A‖ * B = ∑ _ : β, max 1 ‖A‖ * B := by
          simp
          ring
        simp_rw [h1, ← Finset.sum_add_distrib, ← mul_add, mul_comm (max 1 ‖A‖), ← Int.cast_add]
        gcongr with j _
        rw [posPart_add_negPart (A i j), Int.cast_abs]
        exact le_trans (norm_entry_le_entrywise_sup_norm A) (le_max_right ..)

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)
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
⊢ ∀ (i : α × (K →+* ℂ)) (j : β × (K →+* ℂ)), ‖asiegel K a i j‖ ≤ c₂ K * A

Tactic:
intro kr lu
    calc
      ‖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 := ?_
    · simp only [Int.cast_abs, ← Real.norm_eq_abs (asiegel K a kr lu)]; rfl
    · have remark := basis_repr_norm_le_const_mul_house K
      simp only [Basis.repr_reindex, Finsupp.mapDomain_equiv_apply,
        integralBasis_repr_apply, eq_intCast, Rat.cast_intCast,
          Complex.norm_intCast] at remark
      exact mod_cast remark ((a kr.1 lu.1 * ((newBasis K) lu.2))) kr.2
    · simp only [house, map_mul, mul_assoc]
      gcongr
      apply norm_mul_le
    · rw [mul_assoc, mul_assoc]
      gcongr _ * (?_ * _)
      · apply house_nonneg
      · exact habs kr.1 lu.1
    · gcongr
      simp only [supOfBasis, le_sup'_iff, mem_univ]; use lu.2
    · rw [mul_right_comm, c₂]
      gcongr
      exacts [supOfBasis_nonneg _, le_max_right ..]

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

Goal state before:
pp: R : Type u_2
inst✝⁴ : CommRing R
inst✝³ : Algebra R ℚ
inst✝² : IsIntegralClosure R ℤ ℚ
inst✝¹ : IsDedekindDomain R
inst✝ : IsFractionRing R ℚ
v : HeightOneSpectrum R
⊢ Set.BijOn ⇑(padicEquiv v) ↑(HeightOneSpectrum.adicCompletionIntegers ℚ v) ↑(subring ↑(primesEquiv v))

Tactic:
by
  refine ⟨fun x hx ↦ ?_, (padicEquiv v).injective.injOn, fun y hy ↦ ?_⟩
  · rw [← adicCompletionIntegers.coe_padicIntEquiv_apply v ⟨x, hx⟩]
    exact norm_le_one ((adicCompletionIntegers.padicIntEquiv v) ⟨x, hx⟩)
  · 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.PowModTotient

Goal state before:
pp: x k n : ℕ
hn : 1 < n
h : x.Coprime n
⊢ x ^ (k + φ n) % n = x ^ k % n

Tactic:
by
  rw [pow_add, mul_mod, pow_totient_mod_eq_one hn h]
  simp only [mul_one, dvd_refl, mod_mod_of_dvd]

Goal state after:
Module: Mathlib.NumberTheory.Pell

Goal state before:
pp: d : ℤ
h₀ : d < 0
a : Solution₁ d
⊢ a.x = 0 ∨ a.y = 0

Tactic:
by
  have h := a.prop
  contrapose! h
  have h1 := sq_pos_of_ne_zero h.1
  have h2 := sq_pos_of_ne_zero h.2
  nlinarith

Goal state after:
Module: Mathlib.NumberTheory.Pell

Goal state before:
pp: case inr
d : ℤ
a b : Solution₁ d
ha : 0 < a.x
hb : 0 < b.x
h : d < 0
⊢ 0 < 1 + d * a.y ^ 2 + d * b.y ^ 2

Tactic:
rw [(eq_zero_of_d_neg h a).resolve_left ha.ne', (eq_zero_of_d_neg h b).resolve_left hb.ne']
    simp

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
h₁ : v ((algebraMap K[X] K⟮X⟯) (q % π)) = 1
h₂ : v ((algebraMap K[X] K⟮X⟯) (π * (q / π))) < v ((algebraMap K[X] K⟮X⟯) (q % π))
⊢ v ((algebraMap K[X] K⟮X⟯) (q % π) + (algebraMap K[X] K⟮X⟯) (π * (q / π))) = v ((algebraMap K[X] K⟮X⟯) (q % π))

Tactic:
exact Valuation.map_add_eq_of_lt_left _ h₂

Goal state after:
Module: Mathlib.NumberTheory.SelbergSieve

Goal state before:
pp: s : BoundingSieve
muPlus : ℕ → ℝ
h : IsUpperMoebius muPlus
⊢ siftedSum ≤ ∑ d ∈ s.prodPrimes.divisors, muPlus d * multSum d

Tactic:
have hμ : ∀ n, (if n = 1 then 1 else 0) ≤ ∑ d ∈ n.divisors, muPlus d := h
  calc siftedSum ≤
    ∑ n ∈ s.support, s.weights n * ∑ d ∈ (Nat.gcd s.prodPrimes n).divisors, muPlus d := ?caseA
    _ = ∑ n ∈ s.support, ∑ d ∈ divisors s.prodPrimes,
        if d ∣ n then s.weights n * muPlus d else 0 := ?caseB
    _ = ∑ d ∈ divisors s.prodPrimes, muPlus d * multSum d := ?caseC
  case caseA =>
    rw [siftedSum_eq_sum_support_mul_ite]
    gcongr with n
    exact hμ (Nat.gcd s.prodPrimes n)
  case caseB =>
    simp_rw [mul_sum, ← sum_filter]
    congr with n
    congr
    · rw [← divisors_filter_dvd_of_dvd prodPrimes_ne_zero (Nat.gcd_dvd_left _ _)]
      ext x; simp +contextual [dvd_gcd_iff]
  case caseC =>
    rw [sum_comm]
    simp_rw [multSum, ← sum_filter, mul_sum, mul_comm]

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

Goal state before:
pp: m : ℕ
hm : 0 < m
⊢ partialSum (↑m) 0 = ↑1 / ↑(m ^ 0!)

Tactic:
partialSum,

Goal state after:
m : ℕ
hm : 0 < m
⊢ ∑ i ∈ range (0 + 1), 1 / ↑m ^ i ! = ↑1 / ↑(m ^ 0!)
Module: Mathlib.NumberTheory.Transcendental.Liouville.Residual

Goal state before:
pp: case refine_2.refine_1
r : ℚ
n : ℕ
⊢ 1 < ↑r.den * 2

Tactic:
have := r.pos; lia

Goal state after:
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.Order.Bounded

Goal state before:
pp: α : Type u_1
s : Set α
inst✝¹ : Preorder α
inst✝ : NoMaxOrder α
a : α
ha : ∀ (b : α), b ∈ s → (fun x1 x2 ↦ x1 ≤ x2) b a
⊢ Bounded (fun x1 x2 ↦ x1 < x2) s

Tactic:
obtain ⟨b, hb⟩ := exists_gt a

Goal state after:
α : Type u_1
s : Set α
inst✝¹ : Preorder α
inst✝ : NoMaxOrder α
a : α
ha : ∀ (b : α), b ∈ s → (fun x1 x2 ↦ x1 ≤ x2) b a
b : α
hb : a < b
⊢ Bounded (fun x1 x2 ↦ x1 < x2) s
Module: Mathlib.Order.CountableSupClosed

Goal state before:
pp: α : Type u_2
S : Set (Set α)
inst✝ : LE α
hS : ∀ s ∈ S, CountableSupClosed s
A : Set α
hAS : A ⊆ ⋂₀ S
hA_ne : A.Nonempty
hAc : A.Countable
x : α
hx : IsLUB A x
⊢ x ∈ ⋂₀ S

Tactic:
by
    simp only [subset_sInter_iff, mem_sInter] at hAS ⊢
    exact fun s hs ↦ (hS s hs).isLUB_mem A (hAS s hs) hA_ne hAc x hx

Goal state after:
Module: Mathlib.Order.Filter.ListTraverse

Goal state before:
pp: case mpr
α β : Type u
f : β → Filter α
fs : List β
t : Set (List α)
us : List (Set α)
hus : Forall₂ (fun b s ↦ s ∈ f b) fs us
hs : sequence us ⊆ t
⊢ t ∈ traverse f fs

Tactic:
exact mem_of_superset (mem_traverse _ _ hus) hs

Goal state after:
Module: Mathlib.NumberTheory.WellApproximable

Goal state before:
pp: T : ℝ
hT : Fact (0 < T)
δ : ℕ → ℝ
hδ : Tendsto δ atTop (𝓝 0)
this : SemilatticeSup Nat.Primes := Nat.Subtype.semilatticeSup fun p ↦ Nat.Prime p
μ : Measure 𝕊 := volume
u : Nat.Primes → 𝕊 := fun p ↦ ↑(↑1 / ↑↑p * T)
hu₀ : ∀ (p : Nat.Primes), addOrderOf (u p) = ↑p
hu : Tendsto (addOrderOf ∘ u) atTop atTop
E : Set 𝕊 := addWellApproximable 𝕊 δ
X : ℕ → Set 𝕊 := fun n ↦ approxAddOrderOf 𝕊 n (δ n)
A : ℕ → Set 𝕊 := fun p ↦ blimsup X atTop fun n ↦ 0 < n ∧ ¬p ∣ n
B : ℕ → Set 𝕊 := fun p ↦ blimsup X atTop fun n ↦ 0 < n ∧ p ∣ n ∧ ¬p * p ∣ n
C : ℕ → Set 𝕊 := fun p ↦ blimsup X atTop fun n ↦ 0 < n ∧ p ^ 2 ∣ n
hA₀ : ∀ (p : ℕ), MeasurableSet (A p)
hB₀ : ∀ (p : ℕ), MeasurableSet (B p)
hE₀ : NullMeasurableSet E μ
hE₁ : ∀ (p : ℕ), E = A p ∪ B p ∪ C p
hE₂ : ∀ (p : Nat.Primes), A ↑p =ᵐ[μ] ∅ ∧ B ↑p =ᵐ[μ] ∅ → E =ᵐ[μ] C ↑p
hA : ∀ (p : Nat.Primes), A ↑p =ᵐ[μ] ∅ ∨ A ↑p =ᵐ[μ] univ
hB : ∀ (p : Nat.Primes), B ↑p =ᵐ[μ] ∅ ∨ B ↑p =ᵐ[μ] univ
p : Nat.Primes
e : Set 𝕊 ≃o Set 𝕊 := Equiv.toOrderIsoSet (AddAction.toPerm (u p))
⊢ e (C ↑p) = C ↑p

Tactic:
OrderIso.apply_blimsup e,

Goal state after:
T : ℝ
hT : Fact (0 < T)
δ : ℕ → ℝ
hδ : Tendsto δ atTop (𝓝 0)
this : SemilatticeSup Nat.Primes := Nat.Subtype.semilatticeSup fun p ↦ Nat.Prime p
μ : Measure 𝕊 := volume
u : Nat.Primes → 𝕊 := fun p ↦ ↑(↑1 / ↑↑p * T)
hu₀ : ∀ (p : Nat.Primes), addOrderOf (u p) = ↑p
hu : Tendsto (addOrderOf ∘ u) atTop atTop
E : Set 𝕊 := addWellApproximable 𝕊 δ
X : ℕ → Set 𝕊 := fun n ↦ approxAddOrderOf 𝕊 n (δ n)
A : ℕ → Set 𝕊 := fun p ↦ blimsup X atTop fun n ↦ 0 < n ∧ ¬p ∣ n
B : ℕ → Set 𝕊 := fun p ↦ blimsup X atTop fun n ↦ 0 < n ∧ p ∣ n ∧ ¬p * p ∣ n
C : ℕ → Set 𝕊 := fun p ↦ blimsup X atTop fun n ↦ 0 < n ∧ p ^ 2 ∣ n
hA₀ : ∀ (p : ℕ), MeasurableSet (A p)
hB₀ : ∀ (p : ℕ), MeasurableSet (B p)
hE₀ : NullMeasurableSet E μ
hE₁ : ∀ (p : ℕ), E = A p ∪ B p ∪ C p
hE₂ : ∀ (p : Nat.Primes), A ↑p =ᵐ[μ] ∅ ∧ B ↑p =ᵐ[μ] ∅ → E =ᵐ[μ] C ↑p
hA : ∀ (p : Nat.Primes), A ↑p =ᵐ[μ] ∅ ∨ A ↑p =ᵐ[μ] univ
hB : ∀ (p : Nat.Primes), B ↑p =ᵐ[μ] ∅ ∨ B ↑p =ᵐ[μ] univ
p : Nat.Primes
e : Set 𝕊 ≃o Set 𝕊 := Equiv.toOrderIsoSet (AddAction.toPerm (u p))
⊢ (blimsup (⇑e ∘ X) atTop fun n ↦ 0 < n ∧ ↑p ^ 2 ∣ n) = C ↑p
Module: Mathlib.Order.Nucleus

Goal state before:
pp: X : Type u_1
inst✝ : Frame X
n : Nucleus X
x y : X
⊢ x ⇨ n (n y) = x ⇨ n y

Tactic:
rw [n.idempotent]

Goal state after:
Module: Mathlib.Order.PrimeIdeal

Goal state before:
pp: case right.refine_1
P : Type u_1
inst✝¹ : SemilatticeInf P
I : Ideal P
inst✝ : I.IsProper
hI : ∀ {x y : P}, x ⊓ y ∈ I → x ∈ I ∨ y ∈ I
⊢ (↑I)ᶜ.Nonempty

pp: case right.refine_2
P : Type u_1
inst✝¹ : SemilatticeInf P
I : Ideal P
inst✝ : I.IsProper
hI : ∀ {x y : P}, x ⊓ y ∈ I → x ∈ I ∨ y ∈ I
⊢ DirectedOn (fun x1 x2 ↦ x1 ≥ x2) (↑I)ᶜ

pp: case right.refine_3
P : Type u_1
inst✝¹ : SemilatticeInf P
I : Ideal P
inst✝ : I.IsProper
hI : ∀ {x y : P}, x ⊓ y ∈ I → x ∈ I ∨ y ∈ I
⊢ ∀ {x y : P}, x ≤ y → x ∈ (↑I)ᶜ → y ∈ (↑I)ᶜ

Tactic:
· exact Set.nonempty_compl.2 (I.isProper_iff.1 ‹_›)

Goal state after:
case right.refine_2
P : Type u_1
inst✝¹ : SemilatticeInf P
I : Ideal P
inst✝ : I.IsProper
hI : ∀ {x y : P}, x ⊓ y ∈ I → x ∈ I ∨ y ∈ I
⊢ DirectedOn (fun x1 x2 ↦ x1 ≥ x2) (↑I)ᶜ

case right.refine_3
P : Type u_1
inst✝¹ : SemilatticeInf P
I : Ideal P
inst✝ : I.IsProper
hI : ∀ {x y : P}, x ⊓ y ∈ I → x ∈ I ∨ y ∈ I
⊢ ∀ {x y : P}, x ≤ y → x ∈ (↑I)ᶜ → y ∈ (↑I)ᶜ
Module: Mathlib.Order.KonigLemma

Goal state before:
pp: α : ℕ → 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 := ⋯ }
hcovby : ∀ {a b : αs}, a ⋖ b ↔ a ≤ b ∧ a.fst + 1 = b.fst
this : IsStronglyAtomic αs
⊢ ∃ f, ∀ ⦃i j : ℕ⦄ (hij : i ≤ j), π hij (f j) = f i

Tactic:
obtain ⟨a₀, ha₀, ha₀inf⟩ : ∃ a₀ : αs, a₀.1 = 0 ∧ (Ici a₀).Infinite := by
    obtain ⟨a₀, ha₀⟩ := Finite.exists_infinite_fiber (fun (a : αs) ↦ π zero_le a.2)
    refine ⟨⟨0, a₀⟩, rfl, (infinite_coe_iff.1 ha₀).mono ?_⟩
    simp only [αs, subset_def, mem_preimage, mem_singleton_iff, mem_Ici, Sigma.forall]
    exact fun i x h ↦ ⟨zero_le, h⟩

Goal state after:
α : ℕ → 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 := ⋯ }
hcovby : ∀ {a b : αs}, a ⋖ b ↔ a ≤ b ∧ a.fst + 1 = b.fst
this : IsStronglyAtomic αs
a₀ : αs
ha₀ : a₀.fst = 0
ha₀inf : (Ici a₀).Infinite
⊢ ∃ f, ∀ ⦃i j : ℕ⦄ (hij : i ≤ j), π hij (f j) = f i
Module: Mathlib.Order.ScottContinuity.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_4
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
f : α × β → γ
h₁ : ∀ (a : α), ScottContinuous fun b ↦ f (a, b)
h₂ : ∀ (b : β), ScottContinuous fun a ↦ f (a, b)
⊢ ScottContinuous f

Tactic:
simp_rw [← scottContinuousOn_univ] at ⊢
  exact .fromProd (fun a ↦ (h₁ a).scottContinuousOn) (fun b ↦ (h₂ b).scottContinuousOn)
    (fun a ↦ (h₁ a).monotone) (fun b ↦ (h₂ b).monotone)

Goal state after:
Module: Mathlib.Order.Partition.Basic

Goal state before:
pp: α : Type u_1
x : α
u : Set α
P : Partition u
⊢ x ∈ u ↔ x ∈ P.partOf x ∧ P.partOf x ∈ P

Tactic:
by
  refine ⟨fun hx ↦ ?_, fun ⟨hx, hP⟩ ↦ subset_of_mem hP hx⟩
  obtain ⟨t, htP, hxt⟩ := P.mem_iff_exists.mp hx
  exact P.eq_partOf_of_mem htP hxt ▸ ⟨hxt, htP⟩

Goal state after:
Module: Mathlib.Order.SuccPred.Tree

Goal state before:
pp: α : Type u_1
inst✝⁴ : PartialOrder α
inst✝³ : PredOrder α
inst✝² : IsPredArchimedean α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
r : α
h : Order.pred^[Nat.find ⋯ - 1] r = ⊥
this : Nat.find ⋯ ≤ Nat.find ⋯ - 1
⊢ r = ⊥

Tactic:
replace : Nat.find (bot_le (a := r)).exists_pred_iterate = 0 := by lia

Goal state after:
α : Type u_1
inst✝⁴ : PartialOrder α
inst✝³ : PredOrder α
inst✝² : IsPredArchimedean α
inst✝¹ : OrderBot α
inst✝ : DecidableEq α
r : α
h : Order.pred^[Nat.find ⋯ - 1] r = ⊥
this : Nat.find ⋯ = 0
⊢ r = ⊥