mathlib-initiative/mathlib-tactics huggingface dataset:
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
y : ℚ_[↑(primesEquiv v)]
hy : y ∈ ↑(subring ↑(primesEquiv v))
x : ↥(HeightOneSpectrum.adicCompletionIntegers ℚ v)
hx : (adicCompletionIntegers.padicIntEquiv v) x = ⟨y, hy⟩
⊢ (padicEquiv v) ↑x = y

Tactic:
← adicCompletionIntegers.coe_padicIntEquiv_apply,

Goal state after:
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))
x : ↥(HeightOneSpectrum.adicCompletionIntegers ℚ v)
hx : (adicCompletionIntegers.padicIntEquiv v) x = ⟨y, hy⟩
⊢ ↑((adicCompletionIntegers.padicIntEquiv v) x) = y
Module: Mathlib.NumberTheory.Padics.Measure.Basic

Goal state before:
pp: case zero
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 μ) ν) ∘ ⇑tensorHom) 0 = (⇑((prodMk' μ) ν) ∘ ⇑tensorHom) 0

Tactic:
| zero =>

Goal state after:
Module: Mathlib.NumberTheory.PowModTotient

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

Tactic:
| zero =>

Goal state after:
Module: Mathlib.NumberTheory.Pell

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

Tactic:
| zero =>

Goal state after:
Module: Mathlib.NumberTheory.Pell

Goal state before:
pp: case zero
d : ℤ
a : Solution₁ d
hax : 0 < a.x
hay : 0 < a.y
⊢ 0 < (a ^ Nat.succ 0).y

Tactic:
| zero =>

Goal state after:
Module: Mathlib.NumberTheory.Pell

Goal state before:
pp: d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
a : Solution₁ d
ha₁ : 1 < a.x
ha₂ : 0 < a.y
P : ∃ x', 1 < x' ∧ ∃ y', 0 < y' ∧ ↑x' ^ 2 - d * y' ^ 2 = 1
x₁ : ℕ := Nat.find P
hx : 1 < Nat.find P
y₁ : ℤ
hy₀ : 0 < y₁
hy₁ : ↑(Nat.find P) ^ 2 - d * y₁ ^ 2 = 1
b : Solution₁ d
hb : 1 < b.x
⊢ ↑x₁ ≤ b.x

Tactic:
have hb' := (Int.toNat_of_nonneg <| zero_le_one.trans hb.le).symm

Goal state after:
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
a : Solution₁ d
ha₁ : 1 < a.x
ha₂ : 0 < a.y
P : ∃ x', 1 < x' ∧ ∃ y', 0 < y' ∧ ↑x' ^ 2 - d * y' ^ 2 = 1
x₁ : ℕ := Nat.find P
hx : 1 < Nat.find P
y₁ : ℤ
hy₀ : 0 < y₁
hy₁ : ↑(Nat.find P) ^ 2 - d * y₁ ^ 2 = 1
b : Solution₁ d
hb : 1 < b.x
hb' : b.x = ↑b.x.toNat
⊢ ↑x₁ ≤ b.x
Module: Mathlib.NumberTheory.Pell

Goal state before:
pp: d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
a : Solution₁ d
ha₁ : 1 < a.x
ha₂ : 0 < a.y
P : ∃ x', 1 < x' ∧ ∃ y', 0 < y' ∧ ↑x' ^ 2 - d * y' ^ 2 = 1
x₁ : ℕ := Nat.find P
hx : 1 < Nat.find P
y₁ : ℤ
hy₀ : 0 < y₁
hy₁ : ↑(Nat.find P) ^ 2 - d * y₁ ^ 2 = 1
b : Solution₁ d
hb : 1 < b.x
hb' : b.x = ↑b.x.toNat
hb'' : 1 < b.x
⊢ ↑x₁ ≤ b.x

Tactic:
hb'

Goal state after:
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
a : Solution₁ d
ha₁ : 1 < a.x
ha₂ : 0 < a.y
P : ∃ x', 1 < x' ∧ ∃ y', 0 < y' ∧ ↑x' ^ 2 - d * y' ^ 2 = 1
x₁ : ℕ := Nat.find P
hx : 1 < Nat.find P
y₁ : ℤ
hy₀ : 0 < y₁
hy₁ : ↑(Nat.find P) ^ 2 - d * y₁ ^ 2 = 1
b : Solution₁ d
hb : 1 < ↑b.x.toNat
hb' : b.x = ↑b.x.toNat
hb'' : 1 < b.x
⊢ ↑x₁ ≤ ↑b.x.toNat
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✝²⁸ : Algebra A K
inst✝²⁷ : IsFractionRing A K
inst✝²⁶ : Algebra A L
inst✝²⁵ : IsScalarTower A K L
inst✝²⁴ : Algebra B L
inst✝²³ : IsScalarTower A B L
inst✝²² : IsFractionRing B L
inst✝²¹ : MulSemiringAction Gal(L/K) B
inst✝²⁰ : SMulDistribClass Gal(L/K) B L
D : Type u_5
𝓞D : Type u_6
inst✝¹⁹ : Field D
inst✝¹⁸ : Algebra D L
inst✝¹⁷ : IsDecompositionField K L P D
inst✝¹⁶ : CommRing 𝓞D
inst✝¹⁵ : Algebra 𝓞D D
inst✝¹⁴ : IsFractionRing 𝓞D D
inst✝¹³ : Algebra 𝓞D B
inst✝¹² : Algebra 𝓞D L
inst✝¹¹ : IsScalarTower 𝓞D D L
inst✝¹⁰ : IsScalarTower 𝓞D B L
𝓟D : Ideal 𝓞D
inst✝⁹ : IsGalois K L
inst✝⁸ : IsDedekindDomain A
inst✝⁷ : IsDedekindDomain B
inst✝⁶ : Module.Finite A B
inst✝⁵ : Module.IsTorsionFree A B
inst✝⁴ : Algebra A 𝓞D
inst✝³ : Module.Finite A 𝓞D
inst✝² : IsScalarTower A 𝓞D B
inst✝¹ : IsDedekindDomain 𝓞D
inst✝ : 𝓟D.LiesOver p
hp : p ≠ ⊥
inst₁ : Module.Finite 𝓞D B
⊢ FaithfulSMul 𝓞D B

Tactic:
apply Algebra.IsAlgebraic.faithfulSMul_tower_top A

Goal state after:
Module: Mathlib.NumberTheory.Pell

Goal state before:
pp: d : ℤ
a₁ : Solution₁ d
h : IsFundamental a₁
a : Solution₁ d
⊢ ∃ n, a = a₁ ^ n ∨ a = -a₁ ^ n

Tactic:
by
  obtain ⟨b, hbx, hby, hb⟩ := exists_pos_variant h.d_pos a
  obtain ⟨n, hn⟩ := h.eq_pow_of_nonneg hbx hby
  rcases hb with (rfl | rfl | rfl | hb)
  · exact ⟨n, Or.inl (mod_cast hn)⟩
  · exact ⟨-n, Or.inl (by simp [hn])⟩
  · exact ⟨n, Or.inr (by simp [hn])⟩
  · rw [Set.mem_singleton_iff] at hb
    rw [hb]
    exact ⟨-n, Or.inr (by simp [hn])⟩

Goal state after:
Module: Mathlib.NumberTheory.Pell

Goal state before:
pp: case inl.inr
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
a₁ : Solution₁ d
ha₁ : IsFundamental a₁
n₁ n₂ : ℤ
Hx : 1 < (a₁ ^ n₂).x
Hy : 0 < (a₁ ^ n₂).y
H : ∀ (a : Solution₁ d), ∃ n, a = (a₁ ^ n₂) ^ n ∨ a = -(a₁ ^ n₂) ^ n
hn₁ : -a₁ ^ (n₂ * n₁ - 1) = 1
⊢ a₁ ^ n₂ = a₁

Tactic:
← zpow_zero a₁,

Goal state after:
case inl.inr
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
a₁ : Solution₁ d
ha₁ : IsFundamental a₁
n₁ n₂ : ℤ
Hx : 1 < (a₁ ^ n₂).x
Hy : 0 < (a₁ ^ n₂).y
H : ∀ (a : Solution₁ d), ∃ n, a = (a₁ ^ n₂) ^ n ∨ a = -(a₁ ^ n₂) ^ n
hn₁ : -a₁ ^ (n₂ * n₁ - 1) = a₁ ^ 0
⊢ a₁ ^ n₂ = a₁
Module: Mathlib.NumberTheory.Pell

Goal state before:
pp: d : ℤ
a : Solution₁ d
h : 1 < a.x ∧ 0 < a.y ∧ ∀ (b : Solution₁ d), ∃ n, b = a ^ n ∨ b = -a ^ n
h₀ : 0 < d
hd : ¬IsSquare d
a₁ : Solution₁ d
ha₁ : IsFundamental a₁
⊢ IsFundamental a

Tactic:
obtain ⟨b, -, hb₂⟩ := existsUnique_pos_generator h₀ hd

Goal state after:
d : ℤ
a : Solution₁ d
h : 1 < a.x ∧ 0 < a.y ∧ ∀ (b : Solution₁ d), ∃ n, b = a ^ n ∨ b = -a ^ n
h₀ : 0 < d
hd : ¬IsSquare d
a₁ : Solution₁ d
ha₁ : IsFundamental a₁
b : Solution₁ d
hb₂ : ∀ (y : Solution₁ d), (fun a₁ ↦ 1 < a₁.x ∧ 0 < a₁.y ∧ ∀ (a : Solution₁ d), ∃ n, a = a₁ ^ n ∨ a = -a₁ ^ n) y → y = b
⊢ IsFundamental a
Module: Mathlib.NumberTheory.Pell

Goal state before:
pp: d : ℤ
a : Solution₁ d
h : 1 < a.x ∧ 0 < a.y ∧ ∀ (b : Solution₁ d), ∃ n, b = a ^ n ∨ b = -a ^ n
h₀ : 0 < d
hd : ¬IsSquare d
a₁ : Solution₁ d
ha₁ : IsFundamental a₁
b : Solution₁ d
hb₂ : ∀ (y : Solution₁ d), (fun a₁ ↦ 1 < a₁.x ∧ 0 < a₁.y ∧ ∀ (a : Solution₁ d), ∃ n, a = a₁ ^ n ∨ a = -a₁ ^ n) y → y = b
⊢ IsFundamental b

Tactic:
← hb₂ a₁ ⟨ha₁.1, ha₁.2.1, ha₁.eq_zpow_or_neg_zpow⟩

Goal state after:
d : ℤ
a : Solution₁ d
h : 1 < a.x ∧ 0 < a.y ∧ ∀ (b : Solution₁ d), ∃ n, b = a ^ n ∨ b = -a ^ n
h₀ : 0 < d
hd : ¬IsSquare d
a₁ : Solution₁ d
ha₁ : IsFundamental a₁
b : Solution₁ d
hb₂ : ∀ (y : Solution₁ d), (fun a₁ ↦ 1 < a₁.x ∧ 0 < a₁.y ∧ ∀ (a : Solution₁ d), ∃ n, a = a₁ ^ n ∨ a = -a₁ ^ n) y → y = b
⊢ IsFundamental a₁
Module: Mathlib.NumberTheory.RatFunc.Ostrowski

Goal state before:
pp: case f
K : Type u_1
Γ : Type u_2
inst✝² : Field K
inst✝¹ : LinearOrderedCommGroupWithZero Γ
v : Valuation K⟮X⟯ Γ
inst✝ : IsTrivialOn K v
hlt : 1 < v X
p q : K[X]
hq : q ≠ 0
hf : (algebraMap K[X] K⟮X⟯) p / (algebraMap K[X] K⟮X⟯) q ≠ 0
⊢ v ((algebraMap K[X] K⟮X⟯) p / (algebraMap K[X] K⟮X⟯) q) =
    v X ^ ((algebraMap K[X] K⟮X⟯) p / (algebraMap K[X] K⟮X⟯) q).intDegree

Tactic:
rw [intDegree_div (by grind only) (by grind only), v.map_div, zpow_sub₀ (ne_zero_of_lt hlt)]

Goal state after:
case f
K : Type u_1
Γ : Type u_2
inst✝² : Field K
inst✝¹ : LinearOrderedCommGroupWithZero Γ
v : Valuation K⟮X⟯ Γ
inst✝ : IsTrivialOn K v
hlt : 1 < v X
p q : K[X]
hq : q ≠ 0
hf : (algebraMap K[X] K⟮X⟯) p / (algebraMap K[X] K⟮X⟯) q ≠ 0
⊢ v ((algebraMap K[X] K⟮X⟯) p) / v ((algebraMap K[X] K⟮X⟯) q) =
    v X ^ ((algebraMap K[X] K⟮X⟯) p).intDegree / v X ^ ((algebraMap K[X] K⟮X⟯) q).intDegree
Module: Mathlib.NumberTheory.SelbergSieve

Goal state before:
pp: s : BoundingSieve
d : ℕ
hd : d ∣ s.prodPrimes
⊢ 0 < s.nu d

Tactic:
exact nu_pos_of_dvd_prodPrimes hd

Goal state after:
Module: Mathlib.NumberTheory.SumTwoSquares

Goal state before:
pp: case zero
hn : Squarefree 0
H : ∀ q ∈ Nat.primeFactors 0, q % 4 ≠ 3
⊢ IsSquare (-1)

Tactic:
| zero =>

Goal state after:
Module: Mathlib.NumberTheory.SumTwoSquares

Goal state before:
pp: case zero
h : IsSquare (-1)
⊢ ∃ x y, 0 = x ^ 2 + y ^ 2

Tactic:
| zero =>

Goal state after:
Module: Mathlib.NumberTheory.SumTwoSquares

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

Tactic:
exact Nat.sq_add_sq_mul huv.symm hxy

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

Goal state before:
pp: case a
f : ℕ → ℂ[X]
s : ℂ
c : ℝ
hc : ∀ (p : ℕ), ∀ x ∈ Set.Ioc 0 1, ‖eval (x • s) (f p)‖ ≤ c ^ p
p : ℕ
x : ℝ
hx : x ∈ Set.Ioc 0 1
⊢ (-(x • s)).re ≤ ‖s‖

pp: case h₂
f : ℕ → ℂ[X]
s : ℂ
c : ℝ
hc : ∀ (p : ℕ), ∀ x ∈ Set.Ioc 0 1, ‖eval (x • s) (f p)‖ ≤ c ^ p
p : ℕ
x : ℝ
hx : x ∈ Set.Ioc 0 1
⊢ ‖eval (x • s) (f p)‖ ≤ |c| ^ p

Tactic:
· simp only [Set.mem_Ioc] at hx
    apply (re_le_norm _).trans
    rw [norm_neg, norm_smul, Real.norm_of_nonneg hx.1.le]
    exact mul_le_of_le_one_left (norm_nonneg _) hx.2

Goal state after:
case h₂
f : ℕ → ℂ[X]
s : ℂ
c : ℝ
hc : ∀ (p : ℕ), ∀ x ∈ Set.Ioc 0 1, ‖eval (x • s) (f p)‖ ≤ c ^ p
p : ℕ
x : ℝ
hx : x ∈ Set.Ioc 0 1
⊢ ‖eval (x • s) (f p)‖ ≤ |c| ^ p
Module: Mathlib.NumberTheory.Transcendental.Liouville.Basic

Goal state before:
pp: α : ℝ
ha : Irrational α
f : ℤ[X]
f0 : f ≠ 0
fR : ℝ[X] := map (algebraMap ℤ ℝ) f
fa : eval α fR = 0
fR0 : fR ≠ 0
ar : α ∈ ↑fR.roots.toFinset
ζ : ℝ
z0 : ζ > 0
U : closedBall α ζ ∩ ↑fR.roots.toFinset = {α}
xm : ℝ
hM : IsMaxOn (fun x ↦ |eval x (derivative fR)|) (Icc (α - ζ) (α + ζ)) xm
⊢ ∃ A, 0 < A ∧ ∀ (a : ℤ) (b : ℕ), 1 ≤ (↑b + 1) ^ f.natDegree * (|α - ↑a / (↑b + 1)| * A)

Tactic:
refine
    @exists_one_le_pow_mul_dist ℤ ℕ ℝ _ _ _ (fun y => fR.eval y) α ζ |fR.derivative.eval xm| ?_ z0
      (fun y hy => ?_) fun z a hq => ?_

Goal state after:
case refine_1
α : ℝ
ha : Irrational α
f : ℤ[X]
f0 : f ≠ 0
fR : ℝ[X] := map (algebraMap ℤ ℝ) f
fa : eval α fR = 0
fR0 : fR ≠ 0
ar : α ∈ ↑fR.roots.toFinset
ζ : ℝ
z0 : ζ > 0
U : closedBall α ζ ∩ ↑fR.roots.toFinset = {α}
xm : ℝ
hM : IsMaxOn (fun x ↦ |eval x (derivative fR)|) (Icc (α - ζ) (α + ζ)) xm
⊢ ∀ (a : ℕ), 1 ≤ (↑a + 1) ^ f.natDegree

case refine_2
α : ℝ
ha : Irrational α
f : ℤ[X]
f0 : f ≠ 0
fR : ℝ[X] := map (algebraMap ℤ ℝ) f
fa : eval α fR = 0
fR0 : fR ≠ 0
ar : α ∈ ↑fR.roots.toFinset
ζ : ℝ
z0 : ζ > 0
U : closedBall α ζ ∩ ↑fR.roots.toFinset = {α}
xm : ℝ
hM : IsMaxOn (fun x ↦ |eval x (derivative fR)|) (Icc (α - ζ) (α + ζ)) xm
y : ℝ
hy : y ∈ closedBall α ζ
⊢ dist (eval α fR) (eval y fR) ≤ dist α y * |eval xm (derivative fR)|

case refine_3
α : ℝ
ha : Irrational α
f : ℤ[X]
f0 : f ≠ 0
fR : ℝ[X] := map (algebraMap ℤ ℝ) f
fa : eval α fR = 0
fR0 : fR ≠ 0
ar : α ∈ ↑fR.roots.toFinset
ζ : ℝ
z0 : ζ > 0
U : closedBall α ζ ∩ ↑fR.roots.toFinset = {α}
xm : ℝ
hM : IsMaxOn (fun x ↦ |eval x (derivative fR)|) (Icc (α - ζ) (α + ζ)) xm
z : ℤ
a : ℕ
hq : ↑z / (↑a + 1) ∈ closedBall α ζ
⊢ 1 ≤ (↑a + 1) ^ f.natDegree * dist (eval α fR) (eval (↑z / (↑a + 1)) fR)
Module: Mathlib.NumberTheory.SumFourSquares

Goal state before:
pp: case zero
⊢ ∃ a b c d, a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = 0

Tactic:
| zero =>

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

Goal state before:
pp: x : ℝ
lx : Liouville x
f : ℤ[X]
f0 : f ≠ 0
ef0 : (aeval x) f = 0
⊢ eval x (map (algebraMap ℤ ℝ) f) = 0

Tactic:
rwa [← eval_map_algebraMap] at ef0

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

Goal state before:
pp: case zero
m : ℕ
hm : 0 < m
⊢ ∃ p, partialSum (↑m) 0 = ↑p / ↑(m ^ 0!)

Tactic:
| zero =>

Goal state after:
Module: Mathlib.NumberTheory.Wilson

Goal state before:
pp: case refine_1
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : 0 < p
⊢ ∀ a ∈ univ, (↑a).val ∈ Ico 1 (p - 1).succ

Tactic:
intro a

Goal state after:
case refine_1
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : 0 < p
a : (ZMod p)ˣ
⊢ a ∈ univ → (↑a).val ∈ Ico 1 (p - 1).succ
Module: Mathlib.Order.Concept

Goal state before:
pp: α : Type u_2
r' : α → α → Prop
c' : Concept α α r'
inst✝ : Std.Irrefl r'
⊢ Disjoint c'.extent c'.intent

Tactic:
disjoint_iff_forall_ne

Goal state after:
α : Type u_2
r' : α → α → Prop
c' : Concept α α r'
inst✝ : Std.Irrefl r'
⊢ ∀ ⦃a : α⦄, a ∈ c'.extent → ∀ ⦃b : α⦄, b ∈ c'.intent → a ≠ b
Module: Mathlib.Order.Concept

Goal state before:
pp: α : Type u_6
inst✝ : PartialOrder α
c : Concept α α fun x1 x2 ↦ x1 < x2
⊢ IsLowerSet c.extent

Tactic:
intro a

Goal state after:
α : Type u_6
inst✝ : PartialOrder α
c : Concept α α fun x1 x2 ↦ x1 < x2
a : α
⊢ ∀ ⦃b : α⦄, b ≤ a → a ∈ c.extent → b ∈ c.extent
Module: Mathlib.Order.Concept

Goal state before:
pp: α : Type u_6
inst✝ : PartialOrder α
c : Concept α α fun x1 x2 ↦ x1 < x2
⊢ IsUpperSet c.intent

Tactic:
intro a

Goal state after:
α : Type u_6
inst✝ : PartialOrder α
c : Concept α α fun x1 x2 ↦ x1 < x2
a : α
⊢ ∀ ⦃b : α⦄, a ≤ b → a ∈ c.intent → b ∈ c.intent
Module: Mathlib.Order.CountableSupClosed

Goal state before:
pp: α : Type u_2
inst✝ : Preorder α
s : Set α
⊢ upperBounds s ⊆ upperBounds (countableSupClosure s)

Tactic:
intro a

Goal state after:
α : Type u_2
inst✝ : Preorder α
s : Set α
a : α
⊢ a ∈ upperBounds s → a ∈ upperBounds (countableSupClosure s)
Module: Mathlib.Order.Heyting.Regular

Goal state before:
pp: α : Type u_1
inst✝ : HeytingAlgebra α
a b : α
hb : IsRegular b
⊢ Disjoint a bᶜ ↔ a ≤ b

Tactic:
by rw [← le_compl_iff_disjoint_right, hb.eq]

Goal state after:
Module: Mathlib.Order.KonigLemma

Goal state before:
pp: case zero
α : 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)
⊢ grade ℕ (f 0) = 0

Tactic:
| zero =>

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
m n : Nucleus X
⊢ ∀ (x : X), x ≤ ⨅ y, ⨅ (_ : y ≥ x), m y ⇨ n y

Tactic:
simpa using fun _ _ h ↦ inf_le_of_left_le <| h.trans n.le_apply

Goal state after:
Module: Mathlib.Order.Rel.GaloisConnection

Goal state before:
pp: α : Type u_1
β : Type u_2
R : SetRel α β
J : Set α
⊢ R.leftDual J ∈ R.rightFixedPoints

Tactic:
by
  apply le_antisymm
  · apply R.gc_leftDual_rightDual.monotone_l; exact R.gc_leftDual_rightDual.le_u_l J
  · exact R.gc_leftDual_rightDual.l_u_le (R.leftDual J)

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

Goal state before:
pp: α : Type u_1
inst✝ : CompleteLattice α
P : Partition ⊥
hxP : ⊥ ∈ P
⊢ False

Tactic:
exact P.bot_notMem hxP

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✝
α : Type u_2
inst✝ : Order.Frame α
s : α
P Q : Partition s
⊢ {a | ∃ p ∈ P, ∃ q ∈ Q, a = p ⊓ q}.PairwiseDisjoint id

Tactic:
intro a

Goal state after:
α✝ : 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 : Partition s
a : α
⊢ a ∈ {a | ∃ p ∈ P, ∃ q ∈ Q, a = p ⊓ q} →
    ∀ ⦃y : α⦄, y ∈ {a | ∃ p ∈ P, ∃ q ∈ Q, a = p ⊓ q} → a ≠ y → Function.onFun Disjoint id a y
Module: Mathlib.Order.Partition.Basic

Goal state before:
pp: α : Type u_1
u : Set α
P : Partition u
f : α → α
hf : P.IsRepFun f
a : α
⊢ (∀ (x : α), f a = f x ↔ a = x) ∨ ∀ (x : α), f a = f x ↔ P.Rel a x

Tactic:
refine (em (a ∈ u)).elim (fun ha ↦ Or.inr fun b ↦ ?_) (fun ha ↦ Or.inl fun b ↦ ?_)

Goal state after:
case refine_1
α : Type u_1
u : Set α
P : Partition u
f : α → α
hf : P.IsRepFun f
a : α
ha : a ∈ u
b : α
⊢ f a = f b ↔ P.Rel a b

case refine_2
α : Type u_1
u : Set α
P : Partition u
f : α → α
hf : P.IsRepFun f
a : α
ha : a ∉ u
b : α
⊢ f a = f b ↔ a = b
Module: Mathlib.Order.SuccPred.Tree

Goal state before:
pp: case inr
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 : t₁.root ≤ v₁ ⊓ v₂
⊢ t₁ = t₂

Tactic:
rw [le_inf_iff] at oh

Goal state after:
case inr
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 : t₁.root ≤ v₁ ∧ t₁.root ≤ v₂
⊢ t₁ = t₂
Module: Mathlib.Order.SuccPred.Tree

Goal state before:
pp: t : RootedTree
t₁ : SubRootedTree t
ht₁ : t₁ ∈ t.subtrees
t₂ : SubRootedTree t
ht₂ : t₂ ∈ t.subtrees
h : t₁ ≠ t₂
⊢ ∀ ⦃a : ↑t⦄, a ∈ ↑t₁ → a ∉ ↑t₂

Tactic:
intro a

Goal state after:
t : RootedTree
t₁ : SubRootedTree t
ht₁ : t₁ ∈ t.subtrees
t₂ : SubRootedTree t
ht₂ : t₂ ∈ t.subtrees
h : t₁ ≠ t₂
a : ↑t
⊢ a ∈ ↑t₁ → a ∉ ↑t₂
Module: Mathlib.Order.SuccPred.Tree

Goal state before:
pp: t : RootedTree
inst✝ : DecidableEq ↑t
v : ↑t
hr : v ≠ ⊥
⊢ t.subtreeOf v ∈ t.subtrees

Tactic:
simpa [RootedTree.subtrees, RootedTree.subtreeOf]

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
inst✝¹ : CompleteSpace E
hf : StronglyAdapted ℱ f
hf_int : ∀ (n : ℕ), Integrable (f n) μ
inst✝ : SigmaFiniteFiltration μ ℱ
i j : ℕ
hij : i ≤ j
⊢ μ[f 0 | ↑ℱ i] + ∑ i_1 ∈ Finset.range j, μ[f (i_1 + 1) - f i_1 - μ[f (i_1 + 1) - f i_1 | ↑ℱ i_1] | ↑ℱ i] =ᵐ[μ]
    f 0 + ∑ k ∈ Finset.range j, (μ[f (k + 1) - f k | ↑ℱ i] - μ[μ[f (k + 1) - f k | ↑ℱ k] | ↑ℱ i])

Tactic:
refine EventuallyEq.add ?_ ?_

Goal state after:
case refine_1
Ω : Type u_1
E : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
f : ℕ → Ω → E
ℱ : Filtration ℕ m0
inst✝¹ : CompleteSpace E
hf : StronglyAdapted ℱ f
hf_int : ∀ (n : ℕ), Integrable (f n) μ
inst✝ : SigmaFiniteFiltration μ ℱ
i j : ℕ
hij : i ≤ j
⊢ μ[f 0 | ↑ℱ i] =ᵐ[μ] f 0

case refine_2
Ω : Type u_1
E : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
f : ℕ → Ω → E
ℱ : Filtration ℕ m0
inst✝¹ : CompleteSpace E
hf : StronglyAdapted ℱ f
hf_int : ∀ (n : ℕ), Integrable (f n) μ
inst✝ : SigmaFiniteFiltration μ ℱ
i j : ℕ
hij : i ≤ j
⊢ ∑ i_1 ∈ Finset.range j, μ[f (i_1 + 1) - f i_1 - μ[f (i_1 + 1) - f i_1 | ↑ℱ i_1] | ↑ℱ i] =ᵐ[μ]
    ∑ k ∈ Finset.range j, (μ[f (k + 1) - f k | ↑ℱ i] - μ[μ[f (k + 1) - f k | ↑ℱ k] | ↑ℱ i])
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
inst✝¹ : CompleteSpace E
hf : StronglyAdapted ℱ f
hf_int : ∀ (n : ℕ), Integrable (f n) μ
inst✝ : SigmaFiniteFiltration μ ℱ
i j : ℕ
hij : i ≤ j
⊢ StronglyMeasurable (f 0)

Tactic:
· exact (hf 0).mono (ℱ.mono zero_le)

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

Goal state before:
pp: case refine_2.hs.succ
Ω : Type u_1
m✝ : MeasurableSpace Ω
E : Type u_3
inst✝ : TopologicalSpace E
𝓕 : Filtration ℕ m✝
u : ℕ → Ω → E
h₀ : StronglyMeasurable (u 0)
h : ∀ (n : ℕ), StronglyMeasurable (u (n + 1))
this : MeasurableSpace (ℕ × Ω) := 𝓕.predictable
X : ℕ → ℕ × Ω → E :=
  fun m x ↦
    match x.1 with
    | 0 => (h₀.approx m) x.2
    | n.succ => (⋯.approx m) x.2
Y : ℕ → ℕ × Ω → E := fun m x ↦ if x.1 ≤ m then X m x else X m (0, x.2)
m n : ℕ
hn : n + 1 ∈ ↑(Finset.range (m + 1))
⊢ (Set.range (Function.curry (X m) (n + 1))).Finite

Tactic:
exact @((h n).approx m).finite_range

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
ℱ : Filtration ι m0
inst✝⁵ : CompleteSpace E
inst✝⁴ : Lattice E
inst✝³ : ContinuousSup E
inst✝² : HasSolidNorm E
inst✝¹ : IsOrderedAddMonoid E
inst✝ : IsOrderedModule ℝ E
f g : ι → Ω → E
hf : Submartingale f ℱ μ
hg : Submartingale g ℱ μ
⊢ Submartingale (f ⊔ g) ℱ μ

Tactic:
refine ⟨fun i =>
    @StronglyMeasurable.sup _ _ _ _ (ℱ i) _ _ _ (hf.stronglyAdapted i) (hg.stronglyAdapted i),
    fun i j hij => ?_, fun i => Integrable.sup (hf.integrable _) (hg.integrable _)⟩
  refine EventuallyLE.sup_le ?_ ?_
  · exact EventuallyLE.trans (hf.2.1 i j hij)
      (condExp_mono (hf.integrable _) (Integrable.sup (hf.integrable j) (hg.integrable j))
        (Eventually.of_forall fun x => le_sup_left))
  · exact EventuallyLE.trans (hg.2.1 i j hij)
      (condExp_mono (hg.integrable _) (Integrable.sup (hf.integrable j) (hg.integrable j))
        (Eventually.of_forall fun x => le_sup_right))

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

Goal state before:
pp: case pos
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝¹ : Preorder ι
f : Filtration ι m
τ : Ω → WithTop ι
inst✝ : PredOrder ι
hτ : IsStoppingTime f τ
i : ι
hi_min : ∀ (b : ι), ¬b < i
ω : Ω
⊢ ¬τ ω < ↑i

Tactic:
cases τ ω with
    | top => simp
    | coe t => exact mod_cast hi_min t

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

Goal state before:
pp: Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : PartialOrder ι
τ : Ω → WithTop ι
f : Filtration ι m
hτ : IsStoppingTime f τ
h_countable : (Set.range τ).Countable
i : ι
⊢ MeasurableSet {ω | τ ω < ↑i}

Tactic:
by
  have : {ω | τ ω < i} = {ω | τ ω ≤ i} \ {ω | τ ω = i} := by ext1 ω; simp [lt_iff_le_and_ne]
  rw [this]
  exact (hτ.measurableSet_le i).diff (hτ.measurableSet_eq_of_countable_range h_countable i)

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

Goal state before:
pp: case zero
Ω : Type u_1
E : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
𝒢 : Filtration ℕ m0
inst✝¹ : Preorder E
inst✝ : SigmaFiniteFiltration μ 𝒢
f : ℕ → Ω → E
hfmgle : Submartingale f 𝒢 μ
hfadp : StronglyAdapted 𝒢 fun n ↦ f (n + 1)
⊢ f 0 ≤ᵐ[μ] f 0

Tactic:
| zero =>

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

Goal state before:
pp: case zero
Ω : Type u_1
E : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
𝒢 : Filtration ℕ m0
inst✝¹ : Preorder E
inst✝ : SigmaFiniteFiltration μ 𝒢
f : ℕ → Ω → E
hfmgle : Supermartingale f 𝒢 μ
hfadp : StronglyAdapted 𝒢 fun n ↦ f (n + 1)
⊢ f 0 ≤ᵐ[μ] f 0

Tactic:
| zero =>

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

Goal state before:
pp: case zero
Ω : Type u_1
m0 : MeasurableSpace Ω
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ℱ : Filtration ℕ m0
hf : StronglyAdapted ℱ f
⊢ (IsStoppingTime ℱ fun ω ↦ ↑(upperCrossingTime a b f N 0 ω)) ∧
    IsStoppingTime ℱ fun ω ↦ ↑(lowerCrossingTime a b f N 0 ω)

Tactic:
| zero =>

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

Goal state before:
pp: case zero
Ω : Type u_1
E : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
𝒢 : Filtration ℕ m0
inst✝¹ : CompleteSpace E
inst✝ : SigmaFiniteFiltration μ 𝒢
f : ℕ → Ω → E
hfmgle : Martingale f 𝒢 μ
hfadp : StronglyAdapted 𝒢 fun n ↦ f (n + 1)
⊢ f 0 =ᵐ[μ] f 0

Tactic:
| zero =>

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

Goal state before:
pp: case zero
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ω : Ω
M : ℕ
hNM : N ≤ M
h : lowerCrossingTime a b f N 0 ω < N
h' : upperCrossingTime a b f N 0 ω < N
⊢ upperCrossingTime a b f M 0 ω = upperCrossingTime a b f N 0 ω ∧
    lowerCrossingTime a b f M 0 ω = lowerCrossingTime a b f N 0 ω

Tactic:
| zero =>

Goal state after: