mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith

Goal state before:
pp: p : ℝ
hp : 1 < p
M : ℤ
h : LiouvilleWith p ↑M
n : ℕ
hn : 0 < n
m : ℤ
hne : ↑M ≠ ↑m / ↑n
hlt : |↑M - ↑m / ↑n| < ↑n ^ (-1)
hn' : 0 < ↑n
⊢ 1 / ↑n ≤ |↑M * ↑n - ↑m| / |↑n|

Tactic:
Nat.abs_cast

Goal state after:
p : ℝ
hp : 1 < p
M : ℤ
h : LiouvilleWith p ↑M
n : ℕ
hn : 0 < n
m : ℤ
hne : ↑M ≠ ↑m / ↑n
hlt : |↑M - ↑m / ↑n| < ↑n ^ (-1)
hn' : 0 < ↑n
⊢ 1 / ↑n ≤ |↑M * ↑n - ↑m| / ↑n
Module: Mathlib.NumberTheory.WellApproximable

Goal state before:
pp: case refine_1
A : Type u_1
inst✝ : SeminormedCommGroup A
a : A
n : ℕ
δ : ℝ
hn : 0 < n
han : ∀ {b : A}, orderOf b = n → orderOf (a * b) = n
f : ↑{b | orderOf b = n} → ↑{b | orderOf b = n} := fun b ↦ ⟨a * ↑b, ⋯⟩
b : A
hb : b ∈ {b | orderOf b = n}
⊢ orderOf (b⁻¹ * a⁻¹⁻¹) = n

Tactic:
inv_inv,

Goal state after:
case refine_1
A : Type u_1
inst✝ : SeminormedCommGroup A
a : A
n : ℕ
δ : ℝ
hn : 0 < n
han : ∀ {b : A}, orderOf b = n → orderOf (a * b) = n
f : ↑{b | orderOf b = n} → ↑{b | orderOf b = n} := fun b ↦ ⟨a * ↑b, ⋯⟩
b : A
hb : b ∈ {b | orderOf b = n}
⊢ orderOf (b⁻¹ * a) = n
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
⊢ (∀ᵐ (x : 𝕊) ∂μ, x ∉ addWellApproximable 𝕊 δ) ∨ ∀ᵐ (x : 𝕊) ∂μ, x ∈ addWellApproximable 𝕊 δ

Tactic:
set E := addWellApproximable 𝕊 δ

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 : 𝕊) ∂μ, x ∉ E) ∨ ∀ᵐ (x : 𝕊) ∂μ, x ∈ E
Module: Mathlib.Order.Concept

Goal state before:
pp: case inr
α : Type u_6
inst✝ : PartialOrder α
c : Concept α α fun x1 x2 ↦ x1 < x2
a b : α
hb✝ : a ≤ b
ha : a ∈ c.intent
hb : a < b
⊢ b ∈ c.intent

Tactic:
· exact mem_intent_of_intent_rel hb ha

Goal state after:
Module: Mathlib.Order.Completion

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

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

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
hA : ∀ (p : Nat.Primes), A ↑p =ᵐ[μ] ∅ ∨ A ↑p =ᵐ[μ] univ
hB : ∀ (p : Nat.Primes), B ↑p =ᵐ[μ] ∅ ∨ B ↑p =ᵐ[μ] univ
hC : ∀ (p : Nat.Primes), u p +ᵥ C ↑p = C ↑p
h : ∀ (p : Nat.Primes), A ↑p =ᵐ[μ] ∅ ∧ B ↑p =ᵐ[μ] ∅
p : Nat.Primes
hE₂ : E =ᵐ[μ] C ↑p
h_qmp : Measure.QuasiMeasurePreserving (fun x ↦ -u p +ᵥ x) μ μ
⊢ u p +ᵥ E =ᵐ[μ] E

Tactic:
refine (h_qmp.vadd_ae_eq_of_ae_eq (u p) hE₂).trans (ae_eq_trans ?_ hE₂.symm)

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
hA : ∀ (p : Nat.Primes), A ↑p =ᵐ[μ] ∅ ∨ A ↑p =ᵐ[μ] univ
hB : ∀ (p : Nat.Primes), B ↑p =ᵐ[μ] ∅ ∨ B ↑p =ᵐ[μ] univ
hC : ∀ (p : Nat.Primes), u p +ᵥ C ↑p = C ↑p
h : ∀ (p : Nat.Primes), A ↑p =ᵐ[μ] ∅ ∧ B ↑p =ᵐ[μ] ∅
p : Nat.Primes
hE₂ : E =ᵐ[μ] C ↑p
h_qmp : Measure.QuasiMeasurePreserving (fun x ↦ -u p +ᵥ x) μ μ
⊢ u p +ᵥ C ↑p =ᵐ[μ] C ↑p
Module: Mathlib.Order.Monotone.MonovaryOrder

Goal state before:
pp: case refine_2.inl
ι : Type u_1
α : Type u_3
β : Type u_4
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : ι → α
g : ι → β
s : Set ι
this : LinearOrder ι := linearOrderOfSTO (MonovaryOrder f g)
hfg : MonovaryOn f g s
i : ι
hi : i ∈ s
j : ι
hj : j ∈ s
hij : i < j
h : (f i, g i, i).1 < (f j, g j, j).1
⊢ g i ≤ g j

pp: case refine_2.inr
ι : Type u_1
α : Type u_3
β : Type u_4
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : ι → α
g : ι → β
s : Set ι
this : LinearOrder ι := linearOrderOfSTO (MonovaryOrder f g)
hfg : MonovaryOn f g s
i : ι
hi : i ∈ s
j : ι
hj : j ∈ s
hij : i < j
h : Prod.Lex (fun x1 x2 ↦ x1 < x2) WellOrderingRel (f i, g i, i).2 (f j, g j, j).2
⊢ g i ≤ g j

Tactic:
· exact hfg.symm hi hj h

Goal state after:
case refine_2.inr
ι : Type u_1
α : Type u_3
β : Type u_4
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : ι → α
g : ι → β
s : Set ι
this : LinearOrder ι := linearOrderOfSTO (MonovaryOrder f g)
hfg : MonovaryOn f g s
i : ι
hi : i ∈ s
j : ι
hj : j ∈ s
hij : i < j
h : Prod.Lex (fun x1 x2 ↦ x1 < x2) WellOrderingRel (f i, g i, i).2 (f j, g j, j).2
⊢ g i ≤ g j
Module: Mathlib.Order.Lattice.Congruence

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : Lattice α
inst✝ : Lattice β
r : α → α → Prop
h₁ : Std.Refl r
h₂ : ∀ ⦃x y : α⦄, r x y ↔ r (x ⊓ y) (x ⊔ y)
h₃ : ∀ ⦃x y z : α⦄, x ≤ y → y ≤ z → r x y → r y z → r x z
h₄ : ∀ ⦃x y t : α⦄, x ≤ y → r x y → r (x ⊓ t) (y ⊓ t) ∧ r (x ⊔ t) (y ⊔ t)
w : α
⊢ ∀ {x y z : α}, r w x → r y z → r (w ⊓ y) (x ⊓ z)

Tactic:
_

Goal state after:
F : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : Lattice α
inst✝ : Lattice β
r : α → α → Prop
h₁ : Std.Refl r
h₂ : ∀ ⦃x y : α⦄, r x y ↔ r (x ⊓ y) (x ⊔ y)
h₃ : ∀ ⦃x y z : α⦄, x ≤ y → y ≤ z → r x y → r y z → r x z
h₄ : ∀ ⦃x y t : α⦄, x ≤ y → r x y → r (x ⊓ t) (y ⊓ t) ∧ r (x ⊔ t) (y ⊔ t)
w x✝ : α
⊢ ∀ {y z : α}, r w x✝ → r y z → r (w ⊓ y) (x✝ ⊓ z)
Module: Mathlib.Order.Lattice.Congruence

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : Lattice α
inst✝ : Lattice β
r : α → α → Prop
h₁ : Std.Refl r
h₂ : ∀ ⦃x y : α⦄, r x y ↔ r (x ⊓ y) (x ⊔ y)
h₃ : ∀ ⦃x y z : α⦄, x ≤ y → y ≤ z → r x y → r y z → r x z
h₄ : ∀ ⦃x y t : α⦄, x ≤ y → r x y → r (x ⊓ t) (y ⊓ t) ∧ r (x ⊔ t) (y ⊔ t)
w x✝ : α
⊢ ∀ {y z : α}, r w x✝ → r y z → r (w ⊓ y) (x✝ ⊓ z)

Tactic:
_

Goal state after:
F : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : Lattice α
inst✝ : Lattice β
r : α → α → Prop
h₁ : Std.Refl r
h₂ : ∀ ⦃x y : α⦄, r x y ↔ r (x ⊓ y) (x ⊔ y)
h₃ : ∀ ⦃x y z : α⦄, x ≤ y → y ≤ z → r x y → r y z → r x z
h₄ : ∀ ⦃x y t : α⦄, x ≤ y → r x y → r (x ⊓ t) (y ⊓ t) ∧ r (x ⊔ t) (y ⊔ t)
w x✝ y✝ : α
⊢ ∀ {z : α}, r w x✝ → r y✝ z → r (w ⊓ y✝) (x✝ ⊓ z)
Module: Mathlib.Order.Lattice.Congruence

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : Lattice α
inst✝ : Lattice β
r : α → α → Prop
h₁ : Std.Refl r
h₂ : ∀ ⦃x y : α⦄, r x y ↔ r (x ⊓ y) (x ⊔ y)
h₃ : ∀ ⦃x y z : α⦄, x ≤ y → y ≤ z → r x y → r y z → r x z
h₄ : ∀ ⦃x y t : α⦄, x ≤ y → r x y → r (x ⊓ t) (y ⊓ t) ∧ r (x ⊔ t) (y ⊔ t)
w x✝ y✝ : α
⊢ ∀ {z : α}, r w x✝ → r y✝ z → r (w ⊓ y✝) (x✝ ⊓ z)

Tactic:
_

Goal state after:
F : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : Lattice α
inst✝ : Lattice β
r : α → α → Prop
h₁ : Std.Refl r
h₂ : ∀ ⦃x y : α⦄, r x y ↔ r (x ⊓ y) (x ⊔ y)
h₃ : ∀ ⦃x y z : α⦄, x ≤ y → y ≤ z → r x y → r y z → r x z
h₄ : ∀ ⦃x y t : α⦄, x ≤ y → r x y → r (x ⊓ t) (y ⊓ t) ∧ r (x ⊔ t) (y ⊔ t)
w x✝ y✝ z✝ : α
⊢ r w x✝ → r y✝ z✝ → r (w ⊓ y✝) (x✝ ⊓ z✝)
Module: Mathlib.Order.Lattice.Congruence

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : Lattice α
inst✝ : Lattice β
r : α → α → Prop
h₁ : Std.Refl r
h₂ : ∀ ⦃x y : α⦄, r x y ↔ r (x ⊓ y) (x ⊔ y)
h₃ : ∀ ⦃x y z : α⦄, x ≤ y → y ≤ z → r x y → r y z → r x z
h₄ : ∀ ⦃x y t : α⦄, x ≤ y → r x y → r (x ⊓ t) (y ⊓ t) ∧ r (x ⊔ t) (y ⊔ t)
w : α
⊢ ∀ {x y z : α}, r w x → r y z → r (w ⊔ y) (x ⊔ z)

Tactic:
_

Goal state after:
F : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : Lattice α
inst✝ : Lattice β
r : α → α → Prop
h₁ : Std.Refl r
h₂ : ∀ ⦃x y : α⦄, r x y ↔ r (x ⊓ y) (x ⊔ y)
h₃ : ∀ ⦃x y z : α⦄, x ≤ y → y ≤ z → r x y → r y z → r x z
h₄ : ∀ ⦃x y t : α⦄, x ≤ y → r x y → r (x ⊓ t) (y ⊓ t) ∧ r (x ⊔ t) (y ⊔ t)
w x✝ : α
⊢ ∀ {y z : α}, r w x✝ → r y z → r (w ⊔ y) (x✝ ⊔ z)
Module: Mathlib.Order.Lattice.Congruence

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : Lattice α
inst✝ : Lattice β
r : α → α → Prop
h₁ : Std.Refl r
h₂ : ∀ ⦃x y : α⦄, r x y ↔ r (x ⊓ y) (x ⊔ y)
h₃ : ∀ ⦃x y z : α⦄, x ≤ y → y ≤ z → r x y → r y z → r x z
h₄ : ∀ ⦃x y t : α⦄, x ≤ y → r x y → r (x ⊓ t) (y ⊓ t) ∧ r (x ⊔ t) (y ⊔ t)
w x✝ : α
⊢ ∀ {y z : α}, r w x✝ → r y z → r (w ⊔ y) (x✝ ⊔ z)

Tactic:
_

Goal state after:
F : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : Lattice α
inst✝ : Lattice β
r : α → α → Prop
h₁ : Std.Refl r
h₂ : ∀ ⦃x y : α⦄, r x y ↔ r (x ⊓ y) (x ⊔ y)
h₃ : ∀ ⦃x y z : α⦄, x ≤ y → y ≤ z → r x y → r y z → r x z
h₄ : ∀ ⦃x y t : α⦄, x ≤ y → r x y → r (x ⊓ t) (y ⊓ t) ∧ r (x ⊔ t) (y ⊔ t)
w x✝ y✝ : α
⊢ ∀ {z : α}, r w x✝ → r y✝ z → r (w ⊔ y✝) (x✝ ⊔ z)
Module: Mathlib.Order.Lattice.Congruence

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : Lattice α
inst✝ : Lattice β
r : α → α → Prop
h₁ : Std.Refl r
h₂ : ∀ ⦃x y : α⦄, r x y ↔ r (x ⊓ y) (x ⊔ y)
h₃ : ∀ ⦃x y z : α⦄, x ≤ y → y ≤ z → r x y → r y z → r x z
h₄ : ∀ ⦃x y t : α⦄, x ≤ y → r x y → r (x ⊓ t) (y ⊓ t) ∧ r (x ⊔ t) (y ⊔ t)
w x✝ y✝ : α
⊢ ∀ {z : α}, r w x✝ → r y✝ z → r (w ⊔ y✝) (x✝ ⊔ z)

Tactic:
_

Goal state after:
F : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : Lattice α
inst✝ : Lattice β
r : α → α → Prop
h₁ : Std.Refl r
h₂ : ∀ ⦃x y : α⦄, r x y ↔ r (x ⊓ y) (x ⊔ y)
h₃ : ∀ ⦃x y z : α⦄, x ≤ y → y ≤ z → r x y → r y z → r x z
h₄ : ∀ ⦃x y t : α⦄, x ≤ y → r x y → r (x ⊓ t) (y ⊓ t) ∧ r (x ⊔ t) (y ⊔ t)
w x✝ y✝ z✝ : α
⊢ r w x✝ → r y✝ z✝ → r (w ⊔ y✝) (x✝ ⊔ z✝)
Module: Mathlib.Order.PrimeIdeal

Goal state before:
pp: P : Type u_1
inst✝ : Preorder P
IF : PrimePair P
⊢ IsPFilter (↑IF.I)ᶜ

Tactic:
rw [IF.compl_I_eq_F]
      exact IF.F.isPFilter

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

Goal state before:
pp: α : Type u_1
β : Type u_2
R : SetRel α β
J : ↑R.leftFixedPoints
⊢ (fun x ↦
        match x with
        | ⟨I, property⟩ => ⟨R.rightDual I, ⋯⟩)
      ((fun x ↦
          match x with
          | ⟨J, property⟩ => ⟨R.leftDual J, ⋯⟩)
        J) =
    J

Tactic:
by obtain ⟨J, hJ⟩ := J; rw [Subtype.mk.injEq, hJ]

Goal state after:
Module: Mathlib.Order.SaddlePoint

Goal state before:
pp: case a
E : Type u_1
F : Type u_2
β : Type u_3
X : Set E
Y : Set F
f : E → F → β
inst✝ : CompleteLinearOrder β
a : E
ha : a ∈ X
b : F
hb : b ∈ Y
h : ⨆ y ∈ Y, f a y = f a b ∧ ⨅ x ∈ X, f x b = f a b
x : E
⊢ x ∈ X → f x b ≤ ⨆ y ∈ Y, f x y

Tactic:
_

Goal state after:
case a
E : Type u_1
F : Type u_2
β : Type u_3
X : Set E
Y : Set F
f : E → F → β
inst✝ : CompleteLinearOrder β
a : E
ha : a ∈ X
b : F
hb : b ∈ Y
h : ⨆ y ∈ Y, f a y = f a b ∧ ⨅ x ∈ X, f x b = f a b
x : E
j✝ : x ∈ X
⊢ f x b ≤ ⨆ y ∈ Y, f x y
Module: Mathlib.Order.ScottContinuity.Prod

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
f : α × β → γ
D : Set (Set (α × β))
h₁ : ∀ (a : α), ScottContinuousOn ((fun d ↦ Prod.snd '' d) '' D) fun b ↦ f (a, b)
h₂ : ∀ (b : β), ScottContinuousOn ((fun d ↦ Prod.fst '' d) '' D) fun a ↦ f (a, b)
h₁' : ∀ (a : α), Monotone fun b ↦ f (a, b)
h₂' : ∀ (b : β), Monotone fun a ↦ f (a, b)
d : Set (α × β)
hX : d ∈ D
hd₁ : d.Nonempty
hd₂ : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) d
x✝ : α × β
p1 : α
p2 : β
hdp : IsLUB d (p1, p2)
⊢ IsLUB (f '' d) (f (p1, p2))

Tactic:
by
  rw [isLUB_congr ((monotone_prod_iff.mpr ⟨h₁', h₂'⟩).upperBounds_image_of_directedOn_prod hd₂),
    ← iUnion_of_singleton_coe (Prod.fst '' d), iUnion_prod_const, image_iUnion,
    ← isLUB_iUnion_iff_of_isLUB (fun a => by
      rw [singleton_prod, image_image f (fun b ↦ (a, b))]
      exact h₁ _ (mem_image_of_mem (fun d ↦ Prod.snd '' d) hX) (Nonempty.image Prod.snd hd₁)
        (DirectedOn.snd hd₂) (isLUB_prod.mp hdp).2) _, Set.range]
  convert!
    (h₂ _ (mem_image_of_mem (fun d ↦ Prod.fst '' d) hX) (Nonempty.image Prod.fst hd₁)
      (DirectedOn.fst hd₂) (isLUB_prod.mp hdp).1)
  ext : 1
  simp_all only [Subtype.exists, mem_image, Prod.exists,
    exists_and_right, exists_eq_right, exists_prop, mem_ofPred_eq]

Goal state after:
Module: Mathlib.Order.SaddlePoint

Goal state before:
pp: case right.a
E : Type u_1
F : Type u_2
β : Type u_3
X : Set E
Y : Set F
f : E → F → β
inst✝ : CompleteLinearOrder β
a : E
ha : a ∈ X
b : F
hb : b ∈ Y
h : ⨆ y ∈ Y, f a y = f a b ∧ ⨅ x ∈ X, f x b = f a b
y : F
⊢ y ∈ Y → ⨅ x ∈ X, f x y ≤ f a y

Tactic:
_

Goal state after:
case right.a
E : Type u_1
F : Type u_2
β : Type u_3
X : Set E
Y : Set F
f : E → F → β
inst✝ : CompleteLinearOrder β
a : E
ha : a ∈ X
b : F
hb : b ∈ Y
h : ⨆ y ∈ Y, f a y = f a b ∧ ⨅ x ∈ X, f x b = f a b
y : F
j✝ : y ∈ Y
⊢ ⨅ x ∈ X, f x y ≤ f a y
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
inst✝¹ : PartialOrder E
inst✝ : IsOrderedAddMonoid E
hf : Submartingale f ℱ μ
ω : Ω
⊢ (Monotone fun x ↦ predictablePart f ℱ μ x ω) → ∀ (n : ℕ), 0 ≤ predictablePart f ℱ μ n ω

Tactic:
hω

Goal state after:
Ω : Type u_1
E : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
f : ℕ → Ω → E
ℱ : Filtration ℕ m0
inst✝² : CompleteSpace E
inst✝¹ : PartialOrder E
inst✝ : IsOrderedAddMonoid E
hf : Submartingale f ℱ μ
ω : Ω
hω : Monotone fun x ↦ predictablePart f ℱ μ x ω
⊢ ∀ (n : ℕ), 0 ≤ predictablePart f ℱ μ n ω
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
c : ℝ
n : ℕ
ω : Ω
⊢ predictablePart (c • f) ?m.45 μ n ω = (c • predictablePart f ?m.45 μ n) ω →
    martingalePart (c • f) ℱ μ n ω = (c • martingalePart f ℱ μ n) ω

Tactic:
hω

Goal state after:
Ω : Type u_1
E : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
f : ℕ → Ω → E
ℱ : Filtration ℕ m0
inst✝ : CompleteSpace E
c : ℝ
n : ℕ
ω : Ω
hω : predictablePart (c • f) ?m.45 μ n ω = (c • predictablePart f ?m.45 μ n) ω
⊢ martingalePart (c • f) ℱ μ n ω = (c • martingalePart f ℱ μ n) ω
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 : ℕ
ω : Ω
⊢ predictablePart (f + g) ℱ μ n ω = (predictablePart f ℱ μ n + predictablePart g ℱ μ n) ω →
    martingalePart (f + g) ℱ μ n ω = (martingalePart f ℱ μ n + martingalePart g ℱ μ n) ω

Tactic:
hω

Goal state after:
Ω : 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 : ℕ
ω : Ω
hω : predictablePart (f + g) ℱ μ n ω = (predictablePart f ℱ μ n + predictablePart g ℱ μ n) ω
⊢ martingalePart (f + g) ℱ μ n ω = (martingalePart f ℱ μ n + martingalePart g ℱ μ n) ω
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 : Martingale f ℱ μ
n : ℕ
ω : Ω
⊢ predictablePart f ℱ μ n ω = 0 ω → martingalePart f ℱ μ n ω = f n ω

Tactic:
hω

Goal state after:
Ω : Type u_1
E : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
f : ℕ → Ω → E
ℱ : Filtration ℕ m0
inst✝ : CompleteSpace E
hf : Martingale f ℱ μ
n : ℕ
ω : Ω
hω : predictablePart f ℱ μ n ω = 0 ω
⊢ martingalePart f ℱ μ n ω = f n ω
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✝ : SigmaFiniteFiltration μ ℱ
hf : IsStronglyPredictable ℱ f
hfint : ∀ (n : ℕ), Integrable (f n) μ
n : ℕ
ω : Ω
⊢ predictablePart f ℱ μ n ω = (f n - f 0) ω → martingalePart f ℱ μ n ω = f 0 ω

Tactic:
hω

Goal state after:
Ω : Type u_1
E : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
f : ℕ → Ω → E
ℱ : Filtration ℕ m0
inst✝ : SigmaFiniteFiltration μ ℱ
hf : IsStronglyPredictable ℱ f
hfint : ∀ (n : ℕ), Integrable (f n) μ
n : ℕ
ω : Ω
hω : predictablePart f ℱ μ n ω = (f n - f 0) ω
⊢ martingalePart f ℱ μ n ω = f 0 ω
Module: Mathlib.Probability.Process.Predictable

Goal state before:
pp: case refine_1.zero
Ω : 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 : ℕ
s : E
this : MeasurableSpace Ω := ↑𝓕 0
⊢ MeasurableSet (Function.curry (Y m) 0 ⁻¹' {s})

Tactic:
exact (h₀.approx m).measurableSet_fiber s

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 : ι → Ω → E
ℱ : Filtration ι m0
inst✝¹ : CompleteSpace E
inst✝ : SigmaFiniteFiltration μ ℱ
hf : Martingale f ℱ μ
i j : ι
hij : i ≤ j
s : Set Ω
hs : MeasurableSet s
a✝ : Ω
heq : μ[f j | ↑ℱ i] a✝ = f i a✝
⊢ a✝ ∈ s → f i a✝ = μ[f j | ↑ℱ i] a✝

Tactic:
_

Goal state after:
Ω : Type u_1
E : Type u_2
ι : Type u_3
inst✝⁴ : Preorder ι
m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
f : ι → Ω → E
ℱ : Filtration ι m0
inst✝¹ : CompleteSpace E
inst✝ : SigmaFiniteFiltration μ ℱ
hf : Martingale f ℱ μ
i j : ι
hij : i ≤ j
s : Set Ω
hs : MeasurableSet s
a✝¹ : Ω
heq : μ[f j | ↑ℱ i] a✝¹ = f i a✝¹
a✝ : a✝¹ ∈ s
⊢ f i a✝¹ = μ[f j | ↑ℱ i] a✝¹
Module: Mathlib.Probability.Process.Predictable

Goal state before:
pp: case neg
Ω : 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 : ℕ
s : E
n : ℕ
hmk : m < n + 1
this : MeasurableSpace Ω := ↑𝓕 0
⊢ MeasurableSet (Function.curry (X m) 0 ⁻¹' {s})

Tactic:
exact (h₀.approx m).measurableSet_fiber s

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 : ι → Ω → E
ℱ : Filtration ι m0
inst✝² : CompleteSpace E
inst✝¹ : Preorder E
inst✝ : AddLeftMono E
hf : Supermartingale f ℱ μ
i j : ι
hij : i ≤ j
a✝ : Ω
⊢ μ[f j | ↑ℱ i] a✝ ≤ f i a✝ → (-f) i a✝ ≤ (-μ[f j | ↑ℱ i]) a✝

Tactic:
_

Goal state after:
Ω : Type u_1
E : Type u_2
ι : Type u_3
inst✝⁵ : Preorder ι
m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
f : ι → Ω → E
ℱ : Filtration ι m0
inst✝² : CompleteSpace E
inst✝¹ : Preorder E
inst✝ : AddLeftMono E
hf : Supermartingale f ℱ μ
i j : ι
hij : i ≤ j
a✝¹ : Ω
a✝ : μ[f j | ↑ℱ i] a✝¹ ≤ f i a✝¹
⊢ (-f) i a✝¹ ≤ (-μ[f j | ↑ℱ i]) a✝¹
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 : ι → Ω → E
ℱ : Filtration ι m0
inst✝² : CompleteSpace E
inst✝¹ : Preorder E
inst✝ : AddLeftMono E
hf : Submartingale f ℱ μ
i j : ι
hij : i ≤ j
a✝ : Ω
⊢ f i a✝ ≤ μ[f j | ↑ℱ i] a✝ → (-μ[f j | ↑ℱ i]) a✝ ≤ (-f) i a✝

Tactic:
_

Goal state after:
Ω : Type u_1
E : Type u_2
ι : Type u_3
inst✝⁵ : Preorder ι
m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
f : ι → Ω → E
ℱ : Filtration ι m0
inst✝² : CompleteSpace E
inst✝¹ : Preorder E
inst✝ : AddLeftMono E
hf : Submartingale f ℱ μ
i j : ι
hij : i ≤ j
a✝¹ : Ω
a✝ : f i a✝¹ ≤ μ[f j | ↑ℱ i] a✝¹
⊢ (-μ[f j | ↑ℱ i]) a✝¹ ≤ (-f) i a✝¹
Module: Mathlib.Probability.Martingale.Centering

Goal state before:
pp: 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
h_eq_sum :
  μ[martingalePart f ℱ μ j | ↑ℱ i] =ᵐ[μ]
    f 0 + ∑ k ∈ Finset.range j, (μ[f (k + 1) - f k | ↑ℱ i] - μ[μ[f (k + 1) - f k | ↑ℱ k] | ↑ℱ i])
h_ge : ∀ (k : ℕ), i ≤ k → μ[f (k + 1) - f k | ↑ℱ i] - μ[μ[f (k + 1) - f k | ↑ℱ k] | ↑ℱ i] =ᵐ[μ] 0
k : ℕ
hk : k < i
⊢ μ[f (k + 1) - f k | ↑ℱ i] =ᵐ[μ] f (k + 1) - f k

Tactic:
rw [condExp_of_stronglyMeasurable]

Goal state after:
case refine_1.hf
Ω : 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
h_eq_sum :
  μ[martingalePart f ℱ μ j | ↑ℱ i] =ᵐ[μ]
    f 0 + ∑ k ∈ Finset.range j, (μ[f (k + 1) - f k | ↑ℱ i] - μ[μ[f (k + 1) - f k | ↑ℱ k] | ↑ℱ i])
h_ge : ∀ (k : ℕ), i ≤ k → μ[f (k + 1) - f k | ↑ℱ i] - μ[μ[f (k + 1) - f k | ↑ℱ k] | ↑ℱ i] =ᵐ[μ] 0
k : ℕ
hk : k < i
⊢ StronglyMeasurable (f (k + 1) - f k)

case refine_1.hfi
Ω : 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
h_eq_sum :
  μ[martingalePart f ℱ μ j | ↑ℱ i] =ᵐ[μ]
    f 0 + ∑ k ∈ Finset.range j, (μ[f (k + 1) - f k | ↑ℱ i] - μ[μ[f (k + 1) - f k | ↑ℱ k] | ↑ℱ i])
h_ge : ∀ (k : ℕ), i ≤ k → μ[f (k + 1) - f k | ↑ℱ i] - μ[μ[f (k + 1) - f k | ↑ℱ k] | ↑ℱ i] =ᵐ[μ] 0
k : ℕ
hk : k < i
⊢ Integrable (f (k + 1) - f k) μ