mathlib-initiative/mathlib-tactics huggingface dataset:
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
m : ℕ
inst✝² : NeZero m
inst✝¹ : IsGalois ℚ ↥F
inst✝ : IsCyclotomicExtension {m} ℚ ↥F
hdiv : m ∣ n
χ : DirichletCharacter R n
⊢ (∀ σ ∈ F.fixingSubgroup, χ ↑((galEquivZMod n K) σ) = 1) ↔
    ∀ ⦃x : (ZMod n)ˣ⦄, x ∈ (ZMod.unitsMap hdiv).ker → x ∈ (toUnitHom χ).ker

Tactic:
← (galEquivZMod n K).forall_congr_right,

Goal state after:
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
m : ℕ
inst✝² : NeZero m
inst✝¹ : IsGalois ℚ ↥F
inst✝ : IsCyclotomicExtension {m} ℚ ↥F
hdiv : m ∣ n
χ : DirichletCharacter R n
⊢ (∀ σ ∈ F.fixingSubgroup, χ ↑((galEquivZMod n K) σ) = 1) ↔
    ∀ (a : Gal(K/ℚ)),
      (galEquivZMod n K).toEquiv a ∈ (ZMod.unitsMap hdiv).ker → (galEquivZMod n K).toEquiv a ∈ (toUnitHom χ).ker
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)
p : Ideal A := Ideal.under A q
this✝² : Algebra (Localization.AtPrime p) (Localization.AtPrime q) := Localization.AtPrime.algebraOfLiesOver p q
this✝¹ : p.IsMaximal
this✝ : Field (A ⧸ p) := Ideal.Quotient.field p
this : IsArtinianRing (B ⧸ Ideal.map (algebraMap A B) p)
⊢ q' = Ideal.map (algebraMap B (Localization.AtPrime q)) (Ideal.map (algebraMap A B) p)

Tactic:
← (Algebra.FormallyUnramified.isRadical_map_isMaximal A B p).radical,

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)
p : Ideal A := Ideal.under A q
this✝² : Algebra (Localization.AtPrime p) (Localization.AtPrime q) := Localization.AtPrime.algebraOfLiesOver p q
this✝¹ : p.IsMaximal
this✝ : Field (A ⧸ p) := Ideal.Quotient.field p
this : IsArtinianRing (B ⧸ Ideal.map (algebraMap A B) p)
⊢ q' = Ideal.map (algebraMap B (Localization.AtPrime q)) (Ideal.map (algebraMap A B) p).radical
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal

Goal state before:
pp: n m p k : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst✝² : Field K
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {n} ℚ K
hn : n = p ^ (k + 1) * m
hm : ¬p ∣ m
this✝³ : IsAbelianGalois ℚ K
this✝² : NeZero m
this✝¹ : NeZero n
ζ : K := zeta n ℚ K
hζ : IsPrimitiveRoot (zeta n ℚ K) n
ζₘ : K := ζ ^ p ^ (k + 1)
hζₘ : IsPrimitiveRoot (zeta n ℚ K ^ p ^ (k + 1)) m
Fₘ : IntermediateField ℚ K := ℚ⟮ζₘ⟯
this✝ : IsCyclotomicExtension {m} ℚ ↥Fₘ
Pₘ : Ideal (𝓞 ↥Fₘ)
left✝ : Pₘ.IsMaximal
right✝¹ : Pₘ.LiesOver 𝒑
ζₚ : K := ζ ^ m
hζₚ : IsPrimitiveRoot (zeta n ℚ K ^ m) (p ^ (k + 1))
Fₚ : IntermediateField ℚ K := ℚ⟮ζₚ⟯
this : IsCyclotomicExtension {p ^ (k + 1)} ℚ ↥Fₚ
Pₚ : Ideal (𝓞 ↥Fₚ)
hP₁ : Pₚ.IsMaximal
right✝ : Pₚ.LiesOver 𝒑
h_main : 𝒑.ramificationIdxIn (𝓞 ↥Fₚ) = Pₘ.inertiaDegIn (𝓞 K) * ((Pₘ.primesOver (𝓞 K)).ncard * 𝒑.ramificationIdxIn (𝓞 K))
⊢ Pₚ.ramificationIdxIn (𝓞 K) * Pₘ.inertiaDegIn (𝓞 K) * (Pₘ.primesOver (𝓞 K)).ncard = 1

Tactic:
← mul_rotate',

Goal state after:
n m p k : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst✝² : Field K
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {n} ℚ K
hn : n = p ^ (k + 1) * m
hm : ¬p ∣ m
this✝³ : IsAbelianGalois ℚ K
this✝² : NeZero m
this✝¹ : NeZero n
ζ : K := zeta n ℚ K
hζ : IsPrimitiveRoot (zeta n ℚ K) n
ζₘ : K := ζ ^ p ^ (k + 1)
hζₘ : IsPrimitiveRoot (zeta n ℚ K ^ p ^ (k + 1)) m
Fₘ : IntermediateField ℚ K := ℚ⟮ζₘ⟯
this✝ : IsCyclotomicExtension {m} ℚ ↥Fₘ
Pₘ : Ideal (𝓞 ↥Fₘ)
left✝ : Pₘ.IsMaximal
right✝¹ : Pₘ.LiesOver 𝒑
ζₚ : K := ζ ^ m
hζₚ : IsPrimitiveRoot (zeta n ℚ K ^ m) (p ^ (k + 1))
Fₚ : IntermediateField ℚ K := ℚ⟮ζₚ⟯
this : IsCyclotomicExtension {p ^ (k + 1)} ℚ ↥Fₚ
Pₚ : Ideal (𝓞 ↥Fₚ)
hP₁ : Pₚ.IsMaximal
right✝ : Pₚ.LiesOver 𝒑
h_main : 𝒑.ramificationIdxIn (𝓞 ↥Fₚ) = 𝒑.ramificationIdxIn (𝓞 K) * (Pₘ.inertiaDegIn (𝓞 K) * (Pₘ.primesOver (𝓞 K)).ncard)
⊢ Pₚ.ramificationIdxIn (𝓞 K) * Pₘ.inertiaDegIn (𝓞 K) * (Pₘ.primesOver (𝓞 K)).ncard = 1
Module: Mathlib.NumberTheory.SiegelsLemma

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : Fintype β
A : Matrix α β ℤ
hA : A ≠ 0
⊢ 1 ≤ ‖A‖

Tactic:
by_contra! h

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : Fintype β
A : Matrix α β ℤ
hA : A ≠ 0
h : ‖A‖ < 1
⊢ False
Module: Mathlib.NumberTheory.SiegelsLemma

Goal state before:
pp: case refine_1
α : 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
⊢ 0 ≤ ∑ x_1, ↑B * ↑(A i x_1)⁺ - ∑ x_1, ↑B * -↑(A i x_1)⁻ + 1

Tactic:
have h := N_le_P_add_one A i
        rify at h
        linarith only [h]

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

Goal state before:
pp: case hbc
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 →+* ℂ)
⊢ house ((algebraMap (𝓞 K) K) ((newBasis K) lu.2)) ≤ supOfBasis K

Tactic:
simp only [supOfBasis, le_sup'_iff, mem_univ]

Goal state after:
case hbc
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 →+* ℂ)
⊢ ∃ b, True ∧ house ((algebraMap (𝓞 K) K) ((newBasis K) lu.2)) ≤ house ((algebraMap (𝓞 K) K) ((newBasis K) b))
Module: Mathlib.NumberTheory.Padics.MahlerBasis

Goal state before:
pp: case refine_1
p : ℕ
hp : Fact (Nat.Prime p)
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : Module ℤ_[p] E
inst✝¹ : IsBoundedSMul ℤ_[p] E
inst✝ : IsUltrametricDist E
f : C(ℤ_[p], E)
s t : ℕ
hst : ∀ (x y : ℤ_[p]), ‖x - y‖ ≤ ↑p ^ (-↑t) → ‖f x - f y‖ ≤ ‖f‖ / ↑p ^ s
n i : ℕ
hi : i < p ^ t - 1
this : 0 < (p ^ t).choose (i + 1)
⊢ ‖↑((p ^ t).choose (i + 1))‖₊ ≤ ↑p ^ (-1)

Tactic:
← coe_le_coe,

Goal state after:
case refine_1
p : ℕ
hp : Fact (Nat.Prime p)
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : Module ℤ_[p] E
inst✝¹ : IsBoundedSMul ℤ_[p] E
inst✝ : IsUltrametricDist E
f : C(ℤ_[p], E)
s t : ℕ
hst : ∀ (x y : ℤ_[p]), ‖x - y‖ ≤ ↑p ^ (-↑t) → ‖f x - f y‖ ≤ ‖f‖ / ↑p ^ s
n i : ℕ
hi : i < p ^ t - 1
this : 0 < (p ^ t).choose (i + 1)
⊢ ↑‖↑((p ^ t).choose (i + 1))‖₊ ≤ ↑(↑p ^ (-1))
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:
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.Pell

Goal state before:
pp: d : ℤ
a : Solution₁ d
ha : 1 < a.x
⊢ 0 < d * a.y ^ 2

Tactic:
rw [a.prop_y, sub_pos]

Goal state after:
d : ℤ
a : Solution₁ d
ha : 1 < a.x
⊢ 1 < a.x ^ 2
Module: Mathlib.NumberTheory.Pell

Goal state before:
pp: b : ℤ
a : Solution₁ (b * b)
ha : 1 < a.x
hp : a.x ^ 2 - b * b * a.y ^ 2 = 1
⊢ False

Tactic:
simp_rw [← sq, ← mul_pow, sq_sub_sq, Int.mul_eq_one_iff_eq_one_or_neg_one] at hp

Goal state after:
b : ℤ
a : Solution₁ (b * b)
ha : 1 < a.x
hp : a.x + b * a.y = 1 ∧ a.x - b * a.y = 1 ∨ a.x + b * a.y = -1 ∧ a.x - b * a.y = -1
⊢ False
Module: Mathlib.NumberTheory.Rayleigh

Goal state before:
pp: r s : ℝ
hrs : r.HolderConjugate s
hr : Irrational r
⊢ {x | ∃ k > 0, beattySeq' r k = x} ∆ {x | ∃ k > 0, beattySeq s k = x} = {n | 0 < n}

Tactic:
beattySeq'_symmDiff_beattySeq_pos hrs

Goal state after:
r s : ℝ
hrs : r.HolderConjugate s
hr : Irrational r
⊢ {n | 0 < n} = {n | 0 < n}
Module: Mathlib.NumberTheory.SelbergSieve

Goal state before:
pp: s : BoundingSieve
⊢ ∀ {d : ℕ}, 0 < d → d ∣ s.prodPrimes → ∑ a ∈ d.divisors, (selbergTerms a)⁻¹ = (s.nu d)⁻¹

Tactic:
apply (ArithmeticFunction.sum_eq_iff_sum_mul_moebius_eq_on _ (fun _ _ ↦ Nat.dvd_trans)).mpr

Goal state after:
s : BoundingSieve
⊢ ∀ n > 0,
    (n ∈ fun x ↦ ∃ c, s.prodPrimes = x * c) → ∑ x ∈ n.divisorsAntidiagonal, ↑(μ x.1) * (s.nu x.2)⁻¹ = (selbergTerms n)⁻¹
Module: Mathlib.NumberTheory.SelbergSieve

Goal state before:
pp: s : BoundingSieve
w : ℕ → ℝ
d1 : ℕ
hd1 : d1 ∈ s.prodPrimes.divisors
d2 : ℕ
hd2 : d2 ∈ s.prodPrimes.divisors
h : d1.lcm d2 ∣ s.prodPrimes
⊢ (∑ x ∈ s.prodPrimes.divisors, if x = d1.lcm d2 then w d1 * w d2 * s.nu x else 0) =
    s.nu d1 * w d1 * s.nu d2 * w d2 * (s.nu (d1.gcd d2))⁻¹

Tactic:
rw [sum_ite_eq_of_mem' (divisors s.prodPrimes) (d1.lcm d2) _
      (mem_divisors.mpr ⟨h, prodPrimes_ne_zero⟩), s.nu_mult.map_lcm]

Goal state after:
s : BoundingSieve
w : ℕ → ℝ
d1 : ℕ
hd1 : d1 ∈ s.prodPrimes.divisors
d2 : ℕ
hd2 : d2 ∈ s.prodPrimes.divisors
h : d1.lcm d2 ∣ s.prodPrimes
⊢ w d1 * w d2 * (s.nu d1 * s.nu d2 / s.nu (d1.gcd d2)) = s.nu d1 * w d1 * s.nu d2 * w d2 * (s.nu (d1.gcd d2))⁻¹

s : BoundingSieve
w : ℕ → ℝ
d1 : ℕ
hd1 : d1 ∈ s.prodPrimes.divisors
d2 : ℕ
hd2 : d2 ∈ s.prodPrimes.divisors
h : d1.lcm d2 ∣ s.prodPrimes
⊢ s.nu (d1.gcd d2) ≠ 0
Module: Mathlib.NumberTheory.Transcendental.Lindemann.AnalyticalPart

Goal state before:
pp: f : ℤ[X]
s : ℂ
this : Bornology.IsBounded ((fun x ↦ max (x * ‖s‖) 1 * ‖(aeval (↑x * s)) f‖) '' Set.Ioc 0 1)
c : ℝ
h : ∀ x ∈ (fun x ↦ max (x * ‖s‖) 1 * ‖(aeval (↑x * s)) f‖) '' Set.Ioc 0 1, |x| ≤ c
p : ℕ
x : ℝ
hx : x ∈ Set.Ioc 0 1
⊢ ‖eval (x • s) (map (algebraMap ℤ ℂ) (X ^ (p - 1) * f ^ p))‖ ≤ c ^ p

Tactic:
specialize h (max (x * ‖s‖) 1 * ‖aeval (x * s) f‖) (Set.mem_image_of_mem _ hx)

Goal state after:
f : ℤ[X]
s : ℂ
this : Bornology.IsBounded ((fun x ↦ max (x * ‖s‖) 1 * ‖(aeval (↑x * s)) f‖) '' Set.Ioc 0 1)
c : ℝ
p : ℕ
x : ℝ
h : |max (x * ‖s‖) 1 * ‖(aeval (↑x * s)) f‖| ≤ c
hx : x ∈ Set.Ioc 0 1
⊢ ‖eval (x • s) (map (algebraMap ℤ ℂ) (X ^ (p - 1) * f ^ p))‖ ≤ c ^ p
Module: Mathlib.NumberTheory.Transcendental.Lindemann.AnalyticalPart

Goal state before:
pp: f : ℤ[X]
s : ℂ
this : Bornology.IsBounded ((fun x ↦ max (x * ‖s‖) 1 * ‖(aeval (↑x * s)) f‖) '' Set.Ioc 0 1)
c : ℝ
p : ℕ
x : ℝ
h : |max (x * ‖s‖) 1 * ‖(aeval (↑x * s)) f‖| ≤ c
hx : x ∈ Set.Ioc 0 1
⊢ (x * ‖s‖) ^ (p - 1) ≤ |max (x * ‖s‖) 1| ^ p

Tactic:
abs_of_nonneg (by positivity),

Goal state after:
f : ℤ[X]
s : ℂ
this : Bornology.IsBounded ((fun x ↦ max (x * ‖s‖) 1 * ‖(aeval (↑x * s)) f‖) '' Set.Ioc 0 1)
c : ℝ
p : ℕ
x : ℝ
h : |max (x * ‖s‖) 1 * ‖(aeval (↑x * s)) f‖| ≤ c
hx : x ∈ Set.Ioc 0 1
⊢ (x * ‖s‖) ^ (p - 1) ≤ max (x * ‖s‖) 1 ^ p
Module: Mathlib.NumberTheory.RamificationInertia.Basic

Goal state before:
pp: case refine_2
R : Type u
inst✝⁵ : CommRing R
S : Type v
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
p : Ideal R
P : Ideal S
hfp : NeZero e
inst✝² : IsDedekindDomain S
inst✝¹ : p.IsMaximal
inst✝ : P.IsPrime
hP0 : P ≠ ⊥
i : ℕ
hi : i ≤ e
Q : ℕ → Prop := fun i ↦ Module.rank (R ⧸ p) ↥(map (Quotient.mk (P ^ e)) (P ^ i)) = (e - i) • Module.rank (R ⧸ p) (S ⧸ P)
⊢ Module.rank (R ⧸ p) ↥(map (Quotient.mk (P ^ e)) (P ^ e)) = (e - e) • Module.rank (R ⧸ p) (S ⧸ P)

Tactic:
rw [Nat.sub_self, zero_nsmul, map_quotient_self]

Goal state after:
case refine_2
R : Type u
inst✝⁵ : CommRing R
S : Type v
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
p : Ideal R
P : Ideal S
hfp : NeZero e
inst✝² : IsDedekindDomain S
inst✝¹ : p.IsMaximal
inst✝ : P.IsPrime
hP0 : P ≠ ⊥
i : ℕ
hi : i ≤ e
Q : ℕ → Prop := fun i ↦ Module.rank (R ⧸ p) ↥(map (Quotient.mk (P ^ e)) (P ^ i)) = (e - i) • Module.rank (R ⧸ p) (S ⧸ P)
⊢ Module.rank (R ⧸ p) ↥⊥ = 0
Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith

Goal state before:
pp: p x : ℝ
m : ℤ
⊢ LiouvilleWith p (x + ↑m) ↔ LiouvilleWith p x

Tactic:
rw [← Rat.cast_intCast m, add_rat_iff]

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)
p : ℕ
hp : Nat.Prime p
⊢ addOrderOf (u ⟨p, hp⟩) = ↑⟨p, hp⟩

Tactic:
exact addOrderOf_div_of_gcd_eq_one hp.pos (gcd_one_left p)

Goal state after:
Module: Mathlib.Order.CompleteSublattice

Goal state before:
pp: case refine_1
α : Type u_1
inst✝ : CompleteLattice α
L : CompleteSublattice α
x✝ : ComplementedLattice ↥L
a : α
ha : a ∈ L
h : ∀ (a : ↥L), ∃ b, IsCompl a b
⊢ ∃ b ∈ L, IsCompl a b

pp: case refine_2
α : Type u_1
inst✝ : CompleteLattice α
L : CompleteSublattice α
h : ∀ a ∈ L, ∃ b ∈ L, IsCompl a b
x✝ : ↥L
a : α
ha : a ∈ L
⊢ ∃ b, IsCompl ⟨a, ha⟩ b

Tactic:
· obtain ⟨b, hb⟩ := h ⟨a, ha⟩
    exact ⟨b, b.property, CompleteSublattice.isCompl_iff.mp hb⟩

Goal state after:
case refine_2
α : Type u_1
inst✝ : CompleteLattice α
L : CompleteSublattice α
h : ∀ a ∈ L, ∃ b ∈ L, IsCompl a b
x✝ : ↥L
a : α
ha : a ∈ L
⊢ ∃ b, IsCompl ⟨a, ha⟩ b
Module: Mathlib.Order.Completion

Goal state before:
pp: α : Type u_1
inst✝ : LinearOrder α
a : α
c : DedekindCut α
⊢ c < principal a ↔ ∃ b ∈ c.right, b < a

Tactic:
rw [← not_le, principal_le_iff]
  rw [not_iff_comm, not_exists, ← principal_le_iff]
  rw [← intent_subset_intent_iff]
  simp_rw [← not_le, not_and, not_not]
  rfl

Goal state after:
Module: Mathlib.Order.Extension.Linear

Goal state before:
pp: α : Type u
r : α → α → Prop
inst✝ : IsPartialOrder α r
S : Set (α → α → Prop) := {s | IsPartialOrder α s}
hS : ∀ c ⊆ S, IsChain (fun x1 x2 ↦ x1 ≤ x2) c → ∀ y ∈ c, ∃ ub ∈ S, ∀ z ∈ c, z ≤ ub
s : α → α → Prop
hrs : r ≤ s
hs : Maximal (fun x ↦ x ∈ S) s
this : IsPartialOrder α s
x y : α
⊢ s x y ∨ s y x

Tactic:
by_contra! h

Goal state after:
α : Type u
r : α → α → Prop
inst✝ : IsPartialOrder α r
S : Set (α → α → Prop) := {s | IsPartialOrder α s}
hS : ∀ c ⊆ S, IsChain (fun x1 x2 ↦ x1 ≤ x2) c → ∀ y ∈ c, ∃ ub ∈ S, ∀ z ∈ c, z ≤ ub
s : α → α → Prop
hrs : r ≤ s
hs : Maximal (fun x ↦ x ∈ S) s
this : IsPartialOrder α s
x y : α
h : ¬s x y ∧ ¬s y x
⊢ False
Module: Mathlib.Order.Height

Goal state before:
pp: α : Type u_1
s : Set α
r : α → α → Prop
⊢ s.chainHeight r ≤ s.encard

Tactic:
by
  simp_all [chainHeight, encard_le_encard]

Goal state after:
Module: Mathlib.Order.KonigLemma

Goal state before:
pp: case succ
α : Type u_1
inst✝⁴ : PartialOrder α
inst✝³ : IsStronglyAtomic α
inst✝² : GradeMinOrder ℕ α
inst✝¹ : OrderBot α
inst✝ : Infinite α
hfin : ∀ (a : α), {x | a ⋖ x}.Finite
f : ℕ ↪o α
h0 : f 0 = ⊥
hf : ∀ (i : ℕ), f i ⋖ f (i + 1)
i : ℕ
ih : grade ℕ (f i) = i
⊢ grade ℕ (f (i + 1)) = i + 1

Tactic:
| succ i ih =>

Goal state after:
Module: Mathlib.Order.Monotone.MonovaryOrder

Goal state before:
pp: case e'_2.e'_1
ι : Type u_1
ι' : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : ι → α
g : ι → β
s : Set ι
a b : ι
⊢ a = b ↔ (f a, g a, a) = (f b, g b, b)

Tactic:
simp only [Prod.ext_iff, ← and_assoc, imp_and, iff_and_self]
      exact ⟨congr_arg _, congr_arg _⟩

Goal state after:
Module: Mathlib.Order.Lattice.Congruence

Goal state before:
pp: α : Type u_2
inst✝ : Lattice α
c : LatticeCon α
x y : α
h : c.toSetoid (x ⊓ y) (x ⊔ y)
⊢ x ≈ ?m.17 h

Tactic:
simpa using c.inf (c.refl x) (c.symm h)

Goal state after:
Module: Mathlib.Order.Nucleus

Goal state before:
pp: X : Type u_1
inst✝ : SemilatticeInf X
n✝ m✝ : Nucleus X
x✝ y✝ : X
m n : Nucleus X
x y : X
⊢ (⇑m ⊓ ⇑n) (x ⊓ y) = (⇑m ⊓ ⇑n) x ⊓ (⇑m ⊓ ⇑n) y

Tactic:
simp [inf_inf_inf_comm]

Goal state after:
Module: Mathlib.Order.Nucleus

Goal state before:
pp: case refine_3
X : Type u_1
inst✝ : CompleteLattice X
s : Set (Nucleus X)
x y : X
f : Nucleus X
hf : f ∈ s
⊢ (⨅ f ∈ s, f x) ⊓ ⨅ f ∈ s, f y ≤ f x ∧ (⨅ f ∈ s, f x) ⊓ ⨅ f ∈ s, f y ≤ f y

Tactic:
· exact ⟨inf_le_of_left_le <| iInf₂_le f hf, inf_le_of_right_le <| iInf₂_le f hf⟩

Goal state after:
Module: Mathlib.Order.Nucleus

Goal state before:
pp: X : Type u_1
inst✝ : Frame X
n✝ m : Nucleus X
x y : X
x✝¹ n x✝ : Nucleus X
⊢ x✝¹ ≤ n ⇨ x✝ ↔ x✝¹ ⊓ n ≤ x✝

Tactic:
by
    simpa [← coe_le_coe, Pi.le_def]
      using ⟨fun h i ↦ h i i le_rfl, fun h i j _ ↦ (h j).trans' <| by gcongr⟩

Goal state after:
Module: Mathlib.Order.Nucleus

Goal state before:
pp: X : Type u_1
inst✝ : Frame X
n m : Nucleus X
h : ⇑n ∘ ⇑m = ⇑m
⊢ n ≤ m

Tactic:
← coe_le_coe,

Goal state after:
X : Type u_1
inst✝ : Frame X
n m : Nucleus X
h : ⇑n ∘ ⇑m = ⇑m
⊢ ⇑n ≤ ⇑m
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✝
α : Type u_2
inst✝ : Order.Frame α
s : α
P Q R : Partition s
hQ : P ≤ Q
hR : P ≤ R
a : α
ha : a ∈ P
⊢ ∃ y ∈ removeBot {a | ∃ p ∈ Q, ∃ q ∈ R, a = p ⊓ q} ⋯ ⋯, a ≤ y

Tactic:
have ⟨q, hq⟩ := hQ ha
    have ⟨r, hr⟩ := hR ha
    refine ⟨q ⊓ r, ⟨?_, ?_⟩, ?_⟩ <;> grind [le_inf_iff, P.ne_bot_of_mem ha]

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

Goal state before:
pp: α : Type u_1
x y : α
u t✝ : Set α
P : Partition u
ht : t✝ ∈ P
t : Set α
ht' : t ∈ P
hx : x ∈ t
hy : y ∈ t
h : x ∈ t✝
⊢ y ∈ t✝

Tactic:
by rwa [P.eq_of_mem_of_mem ht ht' h hx]

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

Goal state before:
pp: α : Type u_1
u : Set α
P : Partition u
f : α → α
a : α
hf : P.IsRepFun f
⊢ f (f a) = f a

Tactic:
obtain (ha | ha) := em (a ∈ u)
  · rw [eq_comm, hf.apply_eq_apply_iff_rel ha]
    exact hf.rel_apply ha
  simp_rw [hf.apply_of_notMem ha]

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

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

Tactic:
have : Order.pred^[0] r = ⊥ := by
      rw [← h]
      apply Nat.find_spec (bot_le (a := r)).exists_pred_iterate
    simp only [Function.iterate_zero, id_eq] at this
    simp [this]

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 ⋯ = 0
⊢ r = ⊥

Tactic:
simpa [this] using h

Goal state after:
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 : Set ↥S), IsGLB s (sInf s)

Tactic:
simp [isGLB_iff_le_iff, lowerBounds, ← Subtype.coe_le_coe]

Goal state after:
Module: Mathlib.Order.Sublocale

Goal state before:
pp: X : Type u_1
inst✝ : Order.Frame X
n : Nucleus X
x : X
⊢ n.toSublocale.restrict x = ⟨n x, ⋯⟩

Tactic:
by
  ext
  simpa [Sublocale.restrict, sInf_image, le_antisymm_iff (a := iInf _)] using
    ⟨iInf₂_le_of_le ⟨n x, x, rfl⟩ n.le_apply le_rfl, fun y hxy ↦ by simpa using n.monotone hxy⟩

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

Goal state before:
pp: case succ
Ω : Type u_1
ι : Type u_2
inst✝ : ConditionallyCompleteLinearOrderBot ι
a b : ℝ
f : ι → Ω → ℝ
N : ι
ω : Ω
n✝ : ℕ
⊢ upperCrossingTime a b f N (n✝ + 1) ω ≤ N

Tactic:
simp only [upperCrossingTime_succ, hittingBtwn_le]

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

Goal state before:
pp: Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ω : Ω
hab : a < b
hn : lowerCrossingTime a b f N (n + 1) ω ≠ N
h : upperCrossingTime a b f N (n + 1) ω = lowerCrossingTime a b f N (n + 1) ω
⊢ b ≤ f (↑(upperCrossingTime a b f N (n + 1) ω)).untopA ω

Tactic:
exact stoppedValue_upperCrossingTime (h.symm ▸ hn)

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

Goal state before:
pp: Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
hab : a < b
⊢ ∃ n, upperCrossingTime a b f N n ω = N

Tactic:
by_contra! h

Goal state after:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
hab : a < b
h : ∀ (n : ℕ), upperCrossingTime a b f N n ω ≠ N
⊢ False
Module: Mathlib.Probability.Process.HittingTime

Goal state before:
pp: Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
n m : ι
⊢ Antitone fun x ↦ hittingBtwn u x n m

Tactic:
by
  intro E F hEF ω
  simp only [hittingBtwn_def]
  split_ifs with hF hE hE
  · gcongr
    exact ⟨n, by simp [mem_lowerBounds]; grind⟩
  · obtain ⟨t, ht⟩ := hF
    exact csInf_le_of_le ⟨n, by simp [mem_lowerBounds]; grind⟩ ht ht.1.2
  · obtain ⟨t, ht⟩ := hE
    exact absurd ⟨t, ht.1, hEF ht.2⟩ hF
  · simp

Goal state after:
Module: Mathlib.Probability.Process.HittingTime

Goal state before:
pp: case inr
Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝² : ConditionallyCompleteLinearOrder ι
inst✝¹ : WellFoundedLT ι
inst✝ : Countable ι
x✝ : MeasurableSpace β
f : Filtration ι m
u : ι → Ω → β
s : Set β
n n' : ι
hu : Adapted f u
hs : MeasurableSet s
i : ι
hi : i < n'
⊢ MeasurableSet {ω | (fun ω ↦ ↑(hittingBtwn u s n n' ω)) ω ≤ ↑i}

Tactic:
have h_set_eq_Union : {ω | hittingBtwn u s n n' ω ≤ i} = ⋃ j ∈ Set.Icc n i, u j ⁻¹' s := by
      ext; simp [hittingBtwn_le_iff_of_lt _ hi]
    simpa [h_set_eq_Union] using MeasurableSet.iUnion fun j =>
      MeasurableSet.iUnion fun hj => f.mono hj.2 _ ((hu j) hs)

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

Goal state before:
pp: Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
inst✝ : IsFiniteMeasure μ
hsub : Submartingale f 𝒢 μ
ε : ℝ≥0
n : ℕ
x : Ω
hx : ∃ b ≤ n, ↑ε ≤ f b x
⊢ ∃ j ≤ n, ↑ε ≤ f j x

Tactic:
exact
      let ⟨j, hj₁, hj₂⟩ := hx
      ⟨j, hj₁, hj₂⟩

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

Goal state before:
pp: case neg
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
f : ℕ → Ω → ℝ
ℱ : Filtration ℕ m0
inst✝ : IsFiniteMeasure μ
a b : ℝ
hf : Submartingale f ℱ μ
N : ℕ
hab : b ≤ a
⊢ (b - a) * ∫ (x : Ω), ↑(upcrossingsBefore a b f N x) ∂μ ≤ ∫ (x : Ω), (fun ω ↦ (f N ω - a)⁺) x ∂μ

Tactic:
← sub_nonpos

Goal state after:
case neg
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
f : ℕ → Ω → ℝ
ℱ : Filtration ℕ m0
inst✝ : IsFiniteMeasure μ
a b : ℝ
hf : Submartingale f ℱ μ
N : ℕ
hab : b - a ≤ 0
⊢ (b - a) * ∫ (x : Ω), ↑(upcrossingsBefore a b f N x) ∂μ ≤ ∫ (x : Ω), (fun ω ↦ (f N ω - a)⁺) x ∂μ
Module: Mathlib.Probability.Martingale.Upcrossing

Goal state before:
pp: case neg
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
f : ℕ → Ω → ℝ
ℱ : Filtration ℕ m0
inst✝ : IsFiniteMeasure μ
a b : ℝ
hf : Submartingale f ℱ μ
hab : b ≤ a
⊢ ENNReal.ofReal (b - a) * ∫⁻ (ω : Ω), upcrossings a b f ω ∂μ ≤ ⨆ N, ∫⁻ (ω : Ω), ENNReal.ofReal (f N ω - a)⁺ ∂μ

Tactic:
← sub_nonpos

Goal state after:
case neg
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
f : ℕ → Ω → ℝ
ℱ : Filtration ℕ m0
inst✝ : IsFiniteMeasure μ
a b : ℝ
hf : Submartingale f ℱ μ
hab : b - a ≤ 0
⊢ ENNReal.ofReal (b - a) * ∫⁻ (ω : Ω), upcrossings a b f ω ∂μ ≤ ⨆ N, ∫⁻ (ω : Ω), ENNReal.ofReal (f N ω - a)⁺ ∂μ