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

Goal state before:
pp: K : Type u_2
inst✝⁵ : Field K
inst✝⁴ : CharZero K
inst✝³ : Algebra.IsIntegral ℚ K
inst✝² : IsTotallyComplex K
E : Subfield K
inst✝¹ : IsTotallyReal ↥E
inst✝ : IsQuadraticExtension (↥E) K
⊢ E = maximalRealSubfield K

Tactic:
by
  refine le_antisymm (IsTotallyReal.le_maximalRealSubfield E) ?_
  by_contra! h
  have h' : E ⊔ (maximalRealSubfield K) = ⊤ := by
    let L : IntermediateField E K := (E ⊔ (maximalRealSubfield K)).toIntermediateField
      (fun x ↦ (le_sup_left (a := E)) x.prop)
    have := ((IntermediateField.isSimpleOrder_of_finrank_prime E K
      (IsQuadraticExtension.finrank_eq_two E K ▸ Nat.prime_two)).eq_bot_or_eq_top L).resolve_left ?_
    · simpa [L] using congr_arg IntermediateField.toSubfield this
    · contrapose h
      rw [← SetLike.coe_set_eq, Subfield.coe_toIntermediateField] at h
      rw [← sup_eq_left, ← SetLike.coe_set_eq, h, IntermediateField.coe_bot]
      aesop
  have : Algebra.IsAlgebraic (maximalRealSubfield K) K :=
    Algebra.IsAlgebraic.tower_top (K := ℚ) (maximalRealSubfield K)
  have : IsTotallyReal K := (h' ▸ isTotallyReal_sup).ofRingEquiv Subring.topEquiv
  obtain w : InfinitePlace K := Classical.choice (inferInstance : Nonempty _)
  exact (not_isReal_iff_isComplex.mpr (IsTotallyComplex.isComplex w)) (IsTotallyReal.isReal w)

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

Goal state before:
pp: F : Type u_1
K : Type u_2
inst✝⁸ : Field F
inst✝⁷ : IsTotallyReal F
inst✝⁶ : Field K
inst✝⁵ : CharZero K
inst✝⁴ : Algebra.IsIntegral ℚ K
inst✝³ : IsTotallyComplex K
inst✝² : Algebra F K
inst✝¹ : IsQuadraticExtension F K
inst✝ : IsAbelianGalois ℚ K
φ : K →+* ℂ := Classical.choice ⋯
σ : Gal(K/ℚ)
hσ₁ : ComplexEmbedding.IsConj φ σ
ν : Gal(K/ℚ)
⊢ ComplexEmbedding.IsConj (φ.comp ↑ν.symm) σ

Tactic:
show σ = ν.symm⁻¹ * σ * ν.symm by simp

Goal state after:
F : Type u_1
K : Type u_2
inst✝⁸ : Field F
inst✝⁷ : IsTotallyReal F
inst✝⁶ : Field K
inst✝⁵ : CharZero K
inst✝⁴ : Algebra.IsIntegral ℚ K
inst✝³ : IsTotallyComplex K
inst✝² : Algebra F K
inst✝¹ : IsQuadraticExtension F K
inst✝ : IsAbelianGalois ℚ K
φ : K →+* ℂ := Classical.choice ⋯
σ : Gal(K/ℚ)
hσ₁ : ComplexEmbedding.IsConj φ σ
ν : Gal(K/ℚ)
⊢ ComplexEmbedding.IsConj (φ.comp ↑ν.symm) (ν.symm⁻¹ * σ * ν.symm)
Module: Mathlib.RingTheory.RootsOfUnity.CyclotomicUnits

Goal state before:
pp: A : Type u_1
ζ : A
inst✝⁴ : CommRing A
inst✝³ : IsDomain A
R : Type u_3
inst✝² : CommRing R
inst✝¹ : Algebra R A
n : ℕ
inst✝ : NeZero n
hζ : IsPrimitiveRoot ζ n
σ τ : A ≃ₐ[R] A
⊢ Associated (ζ ^ (↑((autToPow R hζ) σ)).val - 1) (τ ζ - 1)

Tactic:
← hζ.autToPow_spec R τ

Goal state after:
A : Type u_1
ζ : A
inst✝⁴ : CommRing A
inst✝³ : IsDomain A
R : Type u_3
inst✝² : CommRing R
inst✝¹ : Algebra R A
n : ℕ
inst✝ : NeZero n
hζ : IsPrimitiveRoot ζ n
σ τ : A ≃ₐ[R] A
⊢ Associated (ζ ^ (↑((autToPow R hζ) σ)).val - 1) (ζ ^ (↑((autToPow R hζ) τ)).val - 1)
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
hj : j.Coprime n
⊢ IsUnit (∑ i ∈ range j, ζ ^ i)

Tactic:
obtain ⟨u, hu⟩ := hζ.associated_pow_sub_one_pow_of_coprime hj (coprime_one_left n)
  convert! u.isUnit
  apply mul_right_injective₀ (show 1 - ζ ≠ 0 by grind [sub_one_ne_zero])
  grind [mul_neg_geom_sum]

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))
⊢ map (algebraMap ℤ (𝓞 K)) 𝒑 = span {hζ.toInteger - 1} ^ Module.finrank ℚ K

Tactic:
by
  have : IsGalois ℚ K := isGalois {p ^ (k + 1)} ℚ K
  have : IsGalois (FractionRing ℤ) (FractionRing (𝓞 K)) := by
    refine IsGalois.of_equiv_equiv (f := (FractionRing.algEquiv ℤ ℚ).toRingEquiv.symm)
      (g := (FractionRing.algEquiv (𝓞 K) K).toRingEquiv.symm) <|
        RingHom.ext fun x ↦ IsFractionRing.algEquiv_commutes (FractionRing.algEquiv ℤ ℚ).symm
          (FractionRing.algEquiv (𝓞 K) K).symm _
  rw [map_span, Set.image_singleton, span_singleton_eq_span_singleton.mpr
    ((associated_norm_zeta_sub_one p k hζ).symm.map (algebraMap ℤ (𝓞 K))),
    ← Algebra.intNorm_eq_norm, Algebra.algebraMap_intNorm_of_isGalois, ← prod_span_singleton]
  conv_lhs =>
    enter [2, σ]
    rw [span_singleton_eq_span_singleton.mpr
      (hζ.toInteger_isPrimitiveRoot.associated_sub_one_map_sub_one σ).symm]
  rw [Finset.prod_const, Finset.card_univ, ← Fintype.card_congr (galRestrict ℤ ℚ K (𝓞 K)).toEquiv,
    ← Nat.card_eq_fintype_card, IsGalois.card_aut_eq_finrank]

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

Goal state before:
pp: case e'_5
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
⊢ 2 ^ nrRealPlaces K * (2 * π) ^ nrComplexPlaces K * regulator K / (↑(torsionOrder K) * √|↑(discr K)|) =
    (MeasureTheory.volume (normLeOne K)).toReal /
        ZLattice.covolume (ZLattice.comap ℝ (idealLattice K ((FractionalIdeal.mk0 K) J)) ↑↑(toMixed K))
          MeasureTheory.volume *
      (↑(absNorm ↑J) * (↑(torsionOrder K))⁻¹)

Tactic:
volume_normLeOne,

Goal state after:
case e'_5
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
⊢ 2 ^ nrRealPlaces K * (2 * π) ^ nrComplexPlaces K * regulator K / (↑(torsionOrder K) * √|↑(discr K)|) =
    (2 ^ nrRealPlaces K * ↑NNReal.pi ^ nrComplexPlaces K * ENNReal.ofReal (regulator K)).toReal /
        ZLattice.covolume (ZLattice.comap ℝ (idealLattice K ((FractionalIdeal.mk0 K) J)) ↑↑(toMixed K))
          MeasureTheory.volume *
      (↑(absNorm ↑J) * (↑(torsionOrder K))⁻¹)
Module: Mathlib.NumberTheory.NumberField.House

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
α : Type u_2
β : Type u_3
a : Matrix α β (𝓞 K)
ha : a ≠ 0
k' : α
hs : ∀ (b : K →+* ℂ), (fun l ↦ ((newBasis K).repr (a k' l.1 * (newBasis K) l.2)) b) = 0 (k', b)
l : β
⊢ a k' l = 0 k' l

Tactic:
let ⟨b⟩ := Fintype.card_pos_iff.1 (Fintype.card_pos (α := (K →+* ℂ)))

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
k' : α
hs : ∀ (b : K →+* ℂ), (fun l ↦ ((newBasis K).repr (a k' l.1 * (newBasis K) l.2)) b) = 0 (k', b)
l : β
b : K →+* ℂ
⊢ a k' l = 0 k' l
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
⊢ ∃ t, 0 < t ∧ f ↑p = ↑p ^ (-t)

Tactic:
have hp : (1 : ℝ) < p :=
    mod_cast (is_prime_of_minimal_nat_zero_lt_and_lt_one hp0 hp1 hmin).one_lt
  exact ⟨-logb p (f p), neg_pos.mpr <| logb_neg hp hp0 hp1, by
    simpa using (rpow_logb (zero_lt_one.trans hp) hp.ne' hp0).symm⟩

Goal state after:
Module: Mathlib.NumberTheory.Padics.Measure.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
R : Type u_3
inst✝¹⁰ : TopologicalSpace X
inst✝⁹ : TopologicalSpace Y
inst✝⁸ : CommRing R
inst✝⁷ : TopologicalSpace R
inst✝⁶ : IsTopologicalRing R
μ : AbstractMeasure X R R
ν : AbstractMeasure Y R R
inst✝⁵ : CompactSpace X
inst✝⁴ : CompactSpace Y
inst✝³ : T2Space X
inst✝² : T2Space Y
inst✝¹ : TotallyDisconnectedSpace X
inst✝ : T0Space R
⊢ ⇑((prodMk μ) ν) = ⇑((prodMk' μ) ν)

Tactic:
apply denseRange_tensorHom.equalizer (by fun_prop) (by fun_prop) (funext fun h ↦ ?_)

Goal state after:
X : Type u_1
Y : Type u_2
R : Type u_3
inst✝¹⁰ : TopologicalSpace X
inst✝⁹ : TopologicalSpace Y
inst✝⁸ : CommRing R
inst✝⁷ : TopologicalSpace R
inst✝⁶ : IsTopologicalRing R
μ : AbstractMeasure X R R
ν : AbstractMeasure Y R R
inst✝⁵ : CompactSpace X
inst✝⁴ : CompactSpace Y
inst✝³ : T2Space X
inst✝² : T2Space Y
inst✝¹ : TotallyDisconnectedSpace X
inst✝ : T0Space R
h : TensorProduct R C(X, R) C(Y, R)
⊢ (⇑((prodMk μ) ν) ∘ ⇑tensorHom) h = (⇑((prodMk' μ) ν) ∘ ⇑tensorHom) h
Module: Mathlib.NumberTheory.PrimesCongruentOne

Goal state before:
pp: case inr
k n : ℕ
hk0 : k ≠ 0
hk1 : 1 < k
b : ℕ := k * n !
hgt : 1 < (eval (↑b) (cyclotomic k ℤ)).natAbs
p : ℕ := (eval (↑b) (cyclotomic k ℤ)).natAbs.minFac
hprime : Fact (Prime p)
hroot : (cyclotomic k (ZMod p)).IsRoot ((castRingHom (ZMod p)) b)
⊢ ∃ p, Prime p ∧ n < p ∧ p ≡ 1 [MOD k]

Tactic:
have hpb : ¬p ∣ b :=
    hprime.1.coprime_iff_not_dvd.1 (coprime_of_root_cyclotomic hk0.bot_lt hroot).symm

Goal state after:
case inr
k n : ℕ
hk0 : k ≠ 0
hk1 : 1 < k
b : ℕ := k * n !
hgt : 1 < (eval (↑b) (cyclotomic k ℤ)).natAbs
p : ℕ := (eval (↑b) (cyclotomic k ℤ)).natAbs.minFac
hprime : Fact (Prime p)
hroot : (cyclotomic k (ZMod p)).IsRoot ((castRingHom (ZMod p)) b)
hpb : ¬p ∣ b
⊢ ∃ p, Prime p ∧ n < p ∧ p ≡ 1 [MOD k]
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✝¹¹ : FiniteDimensional K L
inst✝¹⁰ : MulSemiringAction Gal(L/K) B
inst✝⁹ : IsGaloisGroup Gal(L/K) A B
inst✝⁸ : IsDedekindDomain A
inst✝⁷ : IsDedekindDomain B
inst✝⁶ : Module.Finite A B
inst✝⁵ : Module.IsTorsionFree A B
inst✝⁴ : Ring.HasFiniteQuotients A
inst✝³ : P.IsMaximal
E : Type u_6
inst✝² : Field E
inst✝¹ : Algebra E L
inst✝ : IsInertiaField K L P E
hp : p ≠ ⊥
this✝ : p.IsMaximal
this : Finite (A ⧸ p)
⊢ Module.finrank E L = p.ramificationIdxIn B

Tactic:
rw [← IsGaloisGroup.card_eq_finrank (inertia Gal(L/K) P) E L, card_inertia_eq_ramificationIdxIn p]

Goal state after:
Module: Mathlib.NumberTheory.Pell

Goal state before:
pp: d : ℤ
a₁ : Solution₁ d
h : IsFundamental a₁
x : ℕ
ih : ∀ m < x, ∀ {a : Solution₁ d}, 0 ≤ a.y → ↑m = a.x → 0 < ↑m → ∃ n, a = a₁ ^ n
a : Solution₁ d
hay : 0 ≤ a.y
hax' : ↑x = a.x
hax : 0 < ↑x
hy : 0 < a.y
⊢ 1 < a.x

Tactic:
nlinarith [a.prop, h.d_pos]

Goal state after:
Module: Mathlib.NumberTheory.SelbergSieve

Goal state before:
pp: s : BoundingSieve
d : ℕ
hd : d ∣ s.prodPrimes
⊢ ∏ p ∈ d.primeFactors, s.nu p = s.nu d

Tactic:
← s.nu_mult.map_prod_of_subset_primeFactors _ _ subset_rfl,

Goal state after:
s : BoundingSieve
d : ℕ
hd : d ∣ s.prodPrimes
⊢ s.nu (∏ a ∈ d.primeFactors, a) = s.nu d
Module: Mathlib.NumberTheory.RatFunc.Ostrowski

Goal state before:
pp: case h
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
hv : v.IsRankOneDiscrete
h0 : v ↑πᵥ ≠ 0
γ : Γˣ
x✝ : ∃ a, ¬a = 0 ∧ ∃ x, (MonoidWithZeroHom.ofClass v) a * ↑γ = (MonoidWithZeroHom.ofClass v) x
a : K⟮X⟯
ha : ¬a = 0
b : K⟮X⟯
ka : ℤ
hka : v a = v ↑πᵥ ^ ka
kb : ℤ
hab : v ↑πᵥ ^ ka * ↑γ = v ↑πᵥ ^ kb
hkb : v b = v ↑πᵥ ^ kb
this : v ↑πᵥ ^ ka ≠ 0
⊢ ⋯.unit ^ (kb - ka) = γ

Tactic:
simp [zpow_sub, ← Units.val_inj, ← coePolynomial_eq_algebraMap, field, ← hab]

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

Goal state before:
pp: x y : ℤ
⊢ toComplex { re := x, im := y } = ↑x + ↑y * I

Tactic:
simp [toComplex_def]

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

Goal state before:
pp: case a
x : ℤ[i]
⊢ (toComplex x).re = { re := ↑x.re, im := ↑x.im }.re

Tactic:
simp [toComplex_def]

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

Goal state before:
pp: case a
x : ℤ[i]
⊢ (toComplex x).im = { re := ↑x.re, im := ↑x.im }.im

Tactic:
simp [toComplex_def]

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

Goal state before:
pp: x : ℤ[i]
⊢ ↑x.re = (toComplex x).re

Tactic:
simp [toComplex_def]

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

Goal state before:
pp: x : ℤ[i]
⊢ ↑x.im = (toComplex x).im

Tactic:
simp [toComplex_def]

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

Goal state before:
pp: x y : ℤ
⊢ (toComplex { re := x, im := y }).re = ↑x

Tactic:
simp [toComplex_def]

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

Goal state before:
pp: x y : ℤ
⊢ (toComplex { re := x, im := y }).im = ↑y

Tactic:
simp [toComplex_def]

Goal state after:
Module: Mathlib.NumberTheory.SumFourSquares

Goal state before:
pp: p : ℕ
hp : Prime p
this✝ : Fact (Prime p)
natAbs_iff :
  ∀ {a b c d : ℤ} {k : ℕ},
    a.natAbs ^ 2 + b.natAbs ^ 2 + c.natAbs ^ 2 + d.natAbs ^ 2 = k ↔ a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = ↑k
hm✝ : ∃ m < p, 0 < m ∧ ∃ a b c d, a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = m * p
m : ℕ
hmin : ∀ m_1 < m, ¬(m_1 < p ∧ 0 < m_1 ∧ ∃ a b c d, a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = m_1 * p)
hmp : m < p
hm₀ : 0 < m
a b c d : ℕ
habcd : a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = m * p
hm₁ : 1 < m
this : NeZero m
hm : ¬2 ∣ m
f : ℕ → ℤ
hf_lt : ∀ (x : ℕ), 2 * (f x).natAbs < m
hf_mod : ∀ (x : ℕ), ↑(f x) = ↑x
r : ℕ
hr₀ : 0 < r
hrm : r < m
hr : f b ^ 2 + f a ^ 2 + f d ^ 2 + (-f c) ^ 2 = ↑(m * r)
⊢ ∃ w x y z, ↑m ∣ w ∧ ↑m ∣ x ∧ ↑m ∣ y ∧ ↑m ∣ z ∧ w ^ 2 + x ^ 2 + y ^ 2 + z ^ 2 = ↑(m * r) * ↑(m * p)

Tactic:
have := congr_arg₂ (· * Nat.cast ·) hr habcd

Goal state after:
p : ℕ
hp : Prime p
this✝¹ : Fact (Prime p)
natAbs_iff :
  ∀ {a b c d : ℤ} {k : ℕ},
    a.natAbs ^ 2 + b.natAbs ^ 2 + c.natAbs ^ 2 + d.natAbs ^ 2 = k ↔ a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = ↑k
hm✝ : ∃ m < p, 0 < m ∧ ∃ a b c d, a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = m * p
m : ℕ
hmin : ∀ m_1 < m, ¬(m_1 < p ∧ 0 < m_1 ∧ ∃ a b c d, a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = m_1 * p)
hmp : m < p
hm₀ : 0 < m
a b c d : ℕ
habcd : a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = m * p
hm₁ : 1 < m
this✝ : NeZero m
hm : ¬2 ∣ m
f : ℕ → ℤ
hf_lt : ∀ (x : ℕ), 2 * (f x).natAbs < m
hf_mod : ∀ (x : ℕ), ↑(f x) = ↑x
r : ℕ
hr₀ : 0 < r
hrm : r < m
hr : f b ^ 2 + f a ^ 2 + f d ^ 2 + (-f c) ^ 2 = ↑(m * r)
this : (f b ^ 2 + f a ^ 2 + f d ^ 2 + (-f c) ^ 2) * ↑(a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2) = ↑(m * r) * ↑(m * p)
⊢ ∃ w x y z, ↑m ∣ w ∧ ↑m ∣ x ∧ ↑m ∣ y ∧ ↑m ∣ z ∧ w ^ 2 + x ^ 2 + y ^ 2 + z ^ 2 = ↑(m * r) * ↑(m * p)
Module: Mathlib.NumberTheory.Transcendental.Lindemann.AnalyticalPart

Goal state before:
pp: f : ℤ[X]
hf : eval 0 f ≠ 0
c' : ℂ → ℝ
c'0 : ∀ (s : ℂ), c' s ≥ 0
Pp'_le : ∀ (s : ℂ) (p : ℕ), p ≠ 0 → ‖P (map (algebraMap ℤ ℂ) (X ^ (p - 1) * f ^ p)) s‖ ≤ c' s ^ p
p : ℕ
p_gt : p > (eval 0 f).natAbs
prime_p : Nat.Prime p
gp' : ℤ[X]
h' : eval 0 (sumIDeriv (X ^ (p - 1) * f ^ p)) = (p - 1)! • eval 0 (f ^ p) + p ! • eval 0 gp'
gp : ℤ[X]
gp'_le : gp.natDegree ≤ (X ^ (p - 1) * f ^ p).natDegree - p
r : ℂ
h : (aeval r) (sumIDeriv (X ^ (p - 1) * f ^ p)) = ↑p ! * (aeval r) gp
hr : r ∈ f.aroots ℂ
this✝ :
  (↑(eval 0 f ^ p + ↑p * eval 0 gp') * cexp r - ↑p * (aeval r) gp) * ↑(p - 1)! =
    ↑(eval 0 f) ^ p * cexp r * ↑(p - 1)! + ↑(p * (p - 1)!) * (↑(eval 0 gp') * cexp r - (aeval r) gp)
this :
  ↑(eval 0 f) ^ p * cexp r * ↑(p - 1)! +
      (↑p ! * (↑(eval 0 gp') * cexp r) - (aeval r) (sumIDeriv (X ^ (p - 1) * f ^ p))) =
    ↑((p - 1)! • eval 0 (f ^ p) + p ! • eval 0 gp') * cexp r - (aeval r) (sumIDeriv (X ^ (p - 1) * f ^ p))
⊢ c' r ∈ (Multiset.map c' (f.aroots ℂ)).toFinset

Tactic:
simpa only [Multiset.mem_toFinset] using Multiset.mem_map_of_mem _ hr

Goal state after:
Module: Mathlib.Order.Completion

Goal state before:
pp: α : Type u_1
inst✝ : CompleteLattice α
A : DedekindCut α
x✝ : α
⊢ x✝ ∈ Ici (sSup A.left) ↔ x✝ ∈ A.right

Tactic:
mem_Ici,

Goal state after:
α : Type u_1
inst✝ : CompleteLattice α
A : DedekindCut α
x✝ : α
⊢ sSup A.left ≤ x✝ ↔ x✝ ∈ A.right
Module: Mathlib.Order.CountableSupClosed

Goal state before:
pp: α : Type u_2
β : Type u_3
s : Set α
inst✝¹ : Preorder α
inst✝ : Preorder β
t : Set β
hs : CountableSupClosed s
ht : CountableSupClosed t
A : Set (α × β)
hAst : A ⊆ s ×ˢ t
hA_ne : A.Nonempty
hAc : A.Countable
⊢ ∀ (x : α × β), IsLUB A x → x ∈ s ×ˢ t

Tactic:
intro (x, y)

Goal state after:
α : Type u_2
β : Type u_3
s : Set α
inst✝¹ : Preorder α
inst✝ : Preorder β
t : Set β
hs : CountableSupClosed s
ht : CountableSupClosed t
A : Set (α × β)
hAst : A ⊆ s ×ˢ t
hA_ne : A.Nonempty
hAc : A.Countable
x : α
y : β
⊢ IsLUB A (x, y) → (x, y) ∈ s ×ˢ t
Module: Mathlib.SetTheory.Ordinal.Rank

Goal state before:
pp: α : Type u
a : α
r : α → α → Prop
h : Acc r a
⊢ h.rank = ⨆ b, Order.succ ⋯.rank

Tactic:
change (Acc.intro a fun _ => h.inv).rank = _
  rfl

Goal state after:
Module: Mathlib.Order.Height

Goal state before:
pp: α : Type u_1
s : Set α
r : α → α → Prop
h : s.chainHeight r ≠ ⊤
n : ℕ
hn : ↑n = s.chainHeight r
l : Set α
hl : l ⊆ s
he : l.encard = ↑(n + 1)
⊢ s.chainHeight r < l.encard

Tactic:
rw [← hn, he]

Goal state after:
α : Type u_1
s : Set α
r : α → α → Prop
h : s.chainHeight r ≠ ⊤
n : ℕ
hn : ↑n = s.chainHeight r
l : Set α
hl : l ⊆ s
he : l.encard = ↑(n + 1)
⊢ ↑n < ↑(n + 1)
Module: Mathlib.Order.Interval.Finset.Floor

Goal state before:
pp: α : Type u_1
inst✝² : Ring α
inst✝¹ : LinearOrder α
inst✝ : FloorRing α
a : α
n : ℤ
⊢ ↑n ∈ Set.Ici a ↔ n ∈ Set.Ici ⌈a⌉

Tactic:
by simp [ceil_le]

Goal state after:
Module: Mathlib.Order.Interval.Finset.Floor

Goal state before:
pp: α : Type u_1
inst✝² : Semiring α
inst✝¹ : LinearOrder α
inst✝ : FloorSemiring α
a : α
n : ℕ
⊢ ↑n ∈ Set.Ici a ↔ n ∈ Set.Ici ⌈a⌉₊

Tactic:
by simp [ceil_le]

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

Goal state before:
pp: α : Type u_1
s✝ t x y z : α
S : Set α
inst✝ : CompleteLattice α
P Q : Partition s✝
s : α
p p' : Partition s
h : p.parts = p'.parts
⊢ p = p'

Tactic:
cases p

Goal state after:
case mk
α : Type u_1
s✝ t x y z : α
S : Set α
inst✝ : CompleteLattice α
P Q : Partition s✝
s : α
p' : Partition s
parts✝ : Set α
sSupIndep'✝ : sSupIndep parts✝
bot_notMem'✝ : ⊥ ∉ parts✝
sSup_eq'✝ : sSup parts✝ = s
h : { parts := parts✝, sSupIndep' := sSupIndep'✝, bot_notMem' := bot_notMem'✝, sSup_eq' := sSup_eq'✝ }.parts = p'.parts
⊢ { parts := parts✝, sSupIndep' := sSupIndep'✝, bot_notMem' := bot_notMem'✝, sSup_eq' := sSup_eq'✝ } = p'
Module: Mathlib.Order.Partition.Basic

Goal state before:
pp: α : Type u_1
x : α
u t : Set α
P : Partition u
ht : t ∈ P
hxt : x ∈ t
⊢ t = P.partOf x

Tactic:
ext y
  exact ⟨(⟨t, ht, hxt, ·⟩), fun ⟨s, hsP, hxs, hys⟩ ↦ (P.eq_of_mem_of_mem ht hsP hxt hxs) ▸ hys⟩

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

Goal state before:
pp: case refine_2
α : Type u_1
t u : Set α
P : Partition u
f₀ : ↑t → α
h_notMem : ∀ (x : ↑t), ↑x ∉ u → f₀ x = ↑x
h_mem : ∀ (x : ↑t), ↑x ∈ u → P.Rel (↑x) (f₀ x)
h_eq : ∀ (x y : ↑t), P.Rel ↑x ↑y → f₀ x = f₀ y
f : α → α := fun a ↦ if ha : a ∈ u then if hb : ∃ b, P.Rel a ↑b then f₀ hb.choose else P.rep ⋯ else a
hfdef : f = fun a ↦ if ha : a ∈ u then if hb : ∃ b, P.Rel a ↑b then f₀ hb.choose else P.rep ⋯ else a
a b : α
hab : P.Rel a b
⊢ f a = f b

pp: case refine_3
α : Type u_1
t u : Set α
P : Partition u
f₀ : ↑t → α
h_notMem : ∀ (x : ↑t), ↑x ∉ u → f₀ x = ↑x
h_mem : ∀ (x : ↑t), ↑x ∈ u → P.Rel (↑x) (f₀ x)
h_eq : ∀ (x y : ↑t), P.Rel ↑x ↑y → f₀ x = f₀ y
f : α → α := fun a ↦ if ha : a ∈ u then if hb : ∃ b, P.Rel a ↑b then f₀ hb.choose else P.rep ⋯ else a
hfdef : f = fun a ↦ if ha : a ∈ u then if hb : ∃ b, P.Rel a ↑b then f₀ hb.choose else P.rep ⋯ else a
a : ↑t
⊢ f ↑a = f₀ a

Tactic:
· simp_rw [hfdef, dif_pos hab.left_mem, dif_pos hab.right_mem]
    split_ifs with h₁ h₂ h₂
    · exact h_eq _ _ <| (hab.symm.trans h₁.choose_spec).symm.trans h₂.choose_spec
    · exact h₂ ⟨_, hab.symm.trans h₁.choose_spec⟩ |>.elim
    · exact h₁ ⟨_, hab.trans h₂.choose_spec⟩ |>.elim
    congr 1
    rwa [← rel_iff_partOf_eq_partOf_of_mem _ hab.left_mem hab.right_mem]

Goal state after:
case refine_3
α : Type u_1
t u : Set α
P : Partition u
f₀ : ↑t → α
h_notMem : ∀ (x : ↑t), ↑x ∉ u → f₀ x = ↑x
h_mem : ∀ (x : ↑t), ↑x ∈ u → P.Rel (↑x) (f₀ x)
h_eq : ∀ (x y : ↑t), P.Rel ↑x ↑y → f₀ x = f₀ y
f : α → α := fun a ↦ if ha : a ∈ u then if hb : ∃ b, P.Rel a ↑b then f₀ hb.choose else P.rep ⋯ else a
hfdef : f = fun a ↦ if ha : a ∈ u then if hb : ∃ b, P.Rel a ↑b then f₀ hb.choose else P.rep ⋯ else a
a : ↑t
⊢ f ↑a = f₀ a
Module: Mathlib.Order.Sublocale

Goal state before:
pp: X : Type u_1
inst✝ : Order.Frame X
ι : Sort u_2
S✝ T : Sublocale X
s : Set X
f : ι → X
a b : X
S : Sublocale X
x : X
hx : ↑(S.restrictAux x) ≤ x
⊢ ↑(S.restrictAux x) ∈ S

Tactic:
exact S.sInf_mem <| by simp +contextual [Set.subset_def]

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

Goal state before:
pp: case inl
t : RootedTree
t₁ t₂ : SubRootedTree t
ht₁ : t₁ ∈ t.subtrees
ht₂ : t₂ ∈ t.subtrees
v₁ v₂ : ↑t
h₁ : t₁.root ≤ v₁
h₂ : t₂.root ≤ v₂
h : ⊥ < v₁ ⊓ v₂
oh : v₁ ⊓ v₂ < t₁.root
⊢ t₁ = t₂

Tactic:
simp_all [RootedTree.subtrees, IsAtom.lt_iff]

Goal state after:
Module: Mathlib.Probability.Martingale.Centering

Goal state before:
pp: Ω : Type u_1
E : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℕ → Ω → E
ℱ : Filtration ℕ m0
⊢ martingalePart f ℱ μ 0 = f 0

Tactic:
by
  simp [martingalePart]

Goal state after:
Module: Mathlib.Probability.Martingale.Centering

Goal state before:
pp: Ω : Type u_1
E : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
f g : ℕ → Ω → E
ℱ : Filtration ℕ m0
inst✝ : CompleteSpace E
hfint : ∀ (n : ℕ), Integrable (f n) μ
hgint : ∀ (n : ℕ), Integrable (g n) μ
n : ℕ
⊢ martingalePart (f + g) ℱ μ n =ᵐ[μ] martingalePart f ℱ μ n + martingalePart g ℱ μ n

Tactic:
filter_upwards [predictablePart_add (ℱ := ℱ) hfint hgint n] with ω hω
  simp_all [martingalePart]
  abel

Goal state after:
Module: Mathlib.Probability.Martingale.Basic

Goal state before:
pp: Ω : Type u_1
E : Type u_2
ι : Type u_3
inst✝⁴ : Preorder ι
m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
f g : ι → Ω → E
ℱ : Filtration ι m0
inst✝¹ : CompleteSpace E
inst✝ : LE E
hf : Submartingale f ℱ μ
hg : StronglyAdapted ℱ g
h_eq : ∀ (t : ι), f t =ᵐ[μ] g t
⊢ Submartingale g ℱ μ

Tactic:
refine ⟨hg, fun i j hij ↦ ?_, fun i ↦ (integrable_congr (h_eq i)).mp (hf.integrable i)⟩
  exact (Filter.eventuallyLE_congr (h_eq i) (condExp_congr_ae (h_eq j))).mp (ae_le_condExp hf hij)

Goal state after:
Module: Mathlib.Probability.Martingale.Basic

Goal state before:
pp: Ω : Type u_1
ι : Type u_3
inst✝¹ : Preorder ι
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ι m0
inst✝ : SigmaFiniteFiltration μ ℱ
f : ι → Ω → ℝ
hadp : StronglyAdapted ℱ f
hint : ∀ (i : ι), Integrable (f i) μ
i j : ι
hij : i ≤ j
s : Set Ω
hf : ∫ (ω : Ω) in s, f i ω ∂μ ≤ ∫ (ω : Ω) in s, f j ω ∂μ
hs : MeasurableSet s
x✝ : (μ.trim ⋯) s < ∞
⊢ ∫ (a : Ω) in s, f i a ∂μ ≤ ∫ (a : Ω) in s, μ[f j | ↑ℱ i] a ∂μ

Tactic:
setIntegral_condExp (ℱ.le i) (hint j) hs

Goal state after:
Ω : Type u_1
ι : Type u_3
inst✝¹ : Preorder ι
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ι m0
inst✝ : SigmaFiniteFiltration μ ℱ
f : ι → Ω → ℝ
hadp : StronglyAdapted ℱ f
hint : ∀ (i : ι), Integrable (f i) μ
i j : ι
hij : i ≤ j
s : Set Ω
hf : ∫ (ω : Ω) in s, f i ω ∂μ ≤ ∫ (ω : Ω) in s, f j ω ∂μ
hs : MeasurableSet s
x✝ : (μ.trim ⋯) s < ∞
⊢ ∫ (a : Ω) in s, f i a ∂μ ≤ ∫ (x : Ω) in s, f j x ∂μ
Module: Mathlib.Probability.Martingale.Basic

Goal state before:
pp: case pos
Ω : Type u_1
E : Type u_2
ι : Type u_3
inst✝⁵ : Preorder ι
m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
ℱ : Filtration ι m0
inst✝² : CompleteSpace E
inst✝¹ : PartialOrder E
inst✝ : IsOrderedAddMonoid E
f : ι → Ω → E
hf : Submartingale f ℱ μ
i j : ι
hij : i ≤ j
h : SigmaFinite (μ.trim ⋯)
⊢ f i ≤ᵐ[μ] μ[f j | ↑ℱ i]

Tactic:
exact hf.2.1 i j hij

Goal state after: