mathlib-initiative/mathlib-tactics huggingface dataset:
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) * ‖(aeval (↑x * s)) f‖ ^ p ≤ (|max (x * ‖s‖) 1| * ‖(aeval (↑x * s)) f‖) ^ p

Tactic:
mul_pow,

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‖ ^ (p - 1) * ‖s‖ ^ (p - 1) * ‖(aeval (↑x * s)) f‖ ^ p ≤ |max (x * ‖s‖) 1| ^ p * ‖(aeval (↑x * s)) f‖ ^ p
Module: Mathlib.NumberTheory.Transcendental.Liouville.Basic

Goal state before:
pp: a : ℤ
b : ℕ
bN0 : b ≠ 0
cop : a.natAbs.Coprime b
h : Liouville (↑a / ↑b)
p q : ℤ
q1 : 1 < q
a0 : ¬↑a * ↑q = ↑p * ↑b
qR0 : 0 < ↑q
b0 : ↑b ≠ 0
bq0 : 0 < ↑b * ↑q
a1 : |a * q - ↑b * p| * q ^ (b + 1) < ↑b * q
⊢ a * q - ↑b * p ≠ 0

Tactic:
mul_comm (p : ℝ),

Goal state after:
a : ℤ
b : ℕ
bN0 : b ≠ 0
cop : a.natAbs.Coprime b
h : Liouville (↑a / ↑b)
p q : ℤ
q1 : 1 < q
a0 : ¬↑a * ↑q = ↑b * ↑p
qR0 : 0 < ↑q
b0 : ↑b ≠ 0
bq0 : 0 < ↑b * ↑q
a1 : |a * q - ↑b * p| * q ^ (b + 1) < ↑b * q
⊢ a * q - ↑b * p ≠ 0
Module: Mathlib.NumberTheory.RamificationInertia.Basic

Goal state before:
pp: case refine_1
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)
j : ℕ
lt_e : j < e
_le_j : i ≤ j
ih : Q (j + 1)
⊢ (e - (j + 1) + 1) • Module.rank (R ⧸ p) (S ⧸ P) = (e - j) • Module.rank (R ⧸ p) (S ⧸ P)

pp: 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)
j : ℕ
lt_e : j < e
_le_j : i ≤ j
ih : Q (j + 1)
⊢ P ≠ ⊥

Tactic:
Nat.sub_succ,

Goal state after:
case refine_1
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)
j : ℕ
lt_e : j < e
_le_j : i ≤ j
ih : Q (j + 1)
⊢ ((e - j).pred + 1) • Module.rank (R ⧸ p) (S ⧸ P) = (e - j) • Module.rank (R ⧸ p) (S ⧸ P)

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)
j : ℕ
lt_e : j < e
_le_j : i ≤ j
ih : Q (j + 1)
⊢ P ≠ ⊥
Module: Mathlib.NumberTheory.Transcendental.Liouville.Basic

Goal state before:
pp: case refine_1
x : ℝ
lx : Liouville x
f : ℤ[X]
f0 : f ≠ 0
ef0 : eval x (map (algebraMap ℤ ℝ) f) = 0
A : ℝ
hA : 0 < A
h : ∀ (a : ℤ) (b : ℕ), 1 ≤ (↑b + 1) ^ f.natDegree * (|x - ↑a / (↑b + 1)| * A)
r : ℕ
hn : A < (1 + 1) ^ r
a b : ℤ
b1 : 1 < b
a1 : ↑b ^ r * (↑b ^ f.natDegree * |x - ↑a / ↑b|) < 1
b0 : 0 < ↑b
⊢ A * (↑b ^ f.natDegree * |x - ↑a / ↑b|) < 1

Tactic:
refine lt_of_le_of_lt ?_ a1

Goal state after:
case refine_1
x : ℝ
lx : Liouville x
f : ℤ[X]
f0 : f ≠ 0
ef0 : eval x (map (algebraMap ℤ ℝ) f) = 0
A : ℝ
hA : 0 < A
h : ∀ (a : ℤ) (b : ℕ), 1 ≤ (↑b + 1) ^ f.natDegree * (|x - ↑a / (↑b + 1)| * A)
r : ℕ
hn : A < (1 + 1) ^ r
a b : ℤ
b1 : 1 < b
a1 : ↑b ^ r * (↑b ^ f.natDegree * |x - ↑a / ↑b|) < 1
b0 : 0 < ↑b
⊢ A * (↑b ^ f.natDegree * |x - ↑a / ↑b|) ≤ ↑b ^ r * (↑b ^ f.natDegree * |x - ↑a / ↑b|)
Module: Mathlib.NumberTheory.Wilson

Goal state before:
pp: case refine_2
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : 0 < p
a₁✝ : (ZMod p)ˣ
ha₁✝ : a₁✝ ∈ univ
a₂✝ : (ZMod p)ˣ
ha₂✝ : a₂✝ ∈ univ
⊢ (↑a₁✝).val = (↑a₂✝).val → a₁✝ = a₂✝

Tactic:
h

Goal state after:
case refine_2
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : 0 < p
a₁✝ : (ZMod p)ˣ
ha₁✝ : a₁✝ ∈ univ
a₂✝ : (ZMod p)ˣ
ha₂✝ : a₂✝ ∈ univ
h : (↑a₁✝).val = (↑a₂✝).val
⊢ a₁✝ = a₂✝
Module: Mathlib.NumberTheory.Wilson

Goal state before:
pp: case refine_3.refine_2
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : 0 < p
b : ℕ
hb : b ≠ 0 ∧ b < p
⊢ (↑(Units.mk0 ↑b ⋯)).val = b

Tactic:
· simp only [val_cast_of_lt hb.right, Units.val_mk0]

Goal state after:
Module: Mathlib.Order.Bounded

Goal state before:
pp: α : Type u_1
s : Set α
inst✝ : LinearOrder α
a : α
⊢ Unbounded (fun x1 x2 ↦ x1 < x2) (s ∩ {b | a ≤ b}) ↔ Unbounded (fun x1 x2 ↦ x1 < x2) s

Tactic:
by
  convert! @unbounded_lt_inter_not_lt _ s _ a
  exact not_lt.symm

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

Goal state before:
pp: case hab
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
⊢ 0 < |M * ↑n - m|

Tactic:
abs_pos,

Goal state after:
case hab
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
⊢ M * ↑n - m ≠ 0
Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith

Goal state before:
pp: case inl
p : ℝ
hp : 1 < p
h : LiouvilleWith p ↑0
⊢ ↑0 = ↑0

Tactic:
Rat.cast_zero,

Goal state after:
case inl
p : ℝ
hp : 1 < p
h : LiouvilleWith p ↑0
⊢ 0 = ↑0
Module: Mathlib.NumberTheory.WellApproximable

Goal state before:
pp: A : Type u_1
inst✝ : SeminormedCommGroup A
a : A
n : ℕ
δ : ℝ
hn : 0 < n
han : orderOf a ^ 2 ∣ n
b : A
hb : orderOf b = n
⊢ orderOf (a * b) = n

Tactic:
rw [← hb] at han hn

Goal state after:
A : Type u_1
inst✝ : SeminormedCommGroup A
a : A
n : ℕ
δ : ℝ
b : A
hn : 0 < orderOf b
han : orderOf a ^ 2 ∣ orderOf b
hb : orderOf b = n
⊢ orderOf (a * b) = 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
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)
⊢ (∀ᵐ (x : 𝕊) ∂μ, x ∉ E) ∨ ∀ᵐ (x : 𝕊) ∂μ, x ∈ E

Tactic:
have hE₀ : NullMeasurableSet E μ := by
    refine (MeasurableSet.measurableSet_blimsup fun n hn =>
      IsOpen.measurableSet ?_).nullMeasurableSet
    exact isOpen_thickening

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

Goal state before:
pp: case refine_1
ι : Type u_1
α : ι → Type u_2
inst✝² : LinearOrder ι
inst✝¹ : (i : ι) → CompleteLinearOrder (α i)
inst✝ : WellFoundedLT ι
s : Set (Lex ((i : ι) → (fun i ↦ α i) i))
e : Lex ((i : ι) → (fun i ↦ α i) i)
he : e ∈ s
⊢ e ≤ sSup s

Tactic:
by_contra! hs
    obtain ⟨a, ha⟩ := hs
    exact ha.2.not_ge (le_sSup_apply he fun j hj ↦ (ha.1 j hj).symm)

Goal state after:
Module: Mathlib.Order.Completion

Goal state before:
pp: α : Type u_1
inst✝ : Preorder α
a : α
c : DedekindCut α
⊢ c ≤ principal a ↔ a ∈ c.right

Tactic:
simp only [← intent_subset_intent_iff, right_principal]
  exact ⟨fun h ↦ h self_mem_Ici, fun h _y hy ↦ mem_intent_of_intent_rel hy h⟩

Goal state after:
Module: Mathlib.Order.CountableSupClosed

Goal state before:
pp: α : Type u_2
s : Set α
inst✝ : CompleteLattice α
hs : ∀ (A : ℕ → α), (∀ (n : ℕ), A n ∈ s) → ⨆ n, A n ∈ s
x : α
f : ℕ → α
hAs : range f ⊆ s
hA_ne : (range f).Nonempty
hAc : (range f).Countable
hx : IsLUB (range f) x
⊢ x ∈ s

Tactic:
rw [(IsLUB.unique hx isLUB_iSup : x = ⨆ n, f n)]

Goal state after:
α : Type u_2
s : Set α
inst✝ : CompleteLattice α
hs : ∀ (A : ℕ → α), (∀ (n : ℕ), A n ∈ s) → ⨆ n, A n ∈ s
x : α
f : ℕ → α
hAs : range f ⊆ s
hA_ne : (range f).Nonempty
hAc : (range f).Countable
hx : IsLUB (range f) x
⊢ ⨆ n, f n ∈ s
Module: Mathlib.Order.CountableSupClosed

Goal state before:
pp: ι : Sort u_1
α : Type u_2
β : Type u_3
S : Set (Set α)
s✝ t : Set α
a b : α
inst✝ : Preorder α
s A : Set α
hA : A ⊆ {a | ∃ A, ∃ (_ : A ⊆ s) (_ : A.Nonempty) (_ : A.Countable), IsLUB A a}
hA_ne : A.Nonempty
hAc : A.Countable
x : α
hx : IsLUB A x
⊢ x ∈ {a | ∃ A, ∃ (_ : A ⊆ s) (_ : A.Nonempty) (_ : A.Countable), IsLUB A a}

Tactic:
choose B hB hB_ne hBc hB_lub using hA

Goal state after:
ι : Sort u_1
α : Type u_2
β : Type u_3
S : Set (Set α)
s✝ t : Set α
a b : α
inst✝ : Preorder α
s A : Set α
hA_ne : A.Nonempty
hAc : A.Countable
x : α
hx : IsLUB A x
B : ⦃a : α⦄ → a ∈ A → Set α
hB : ∀ ⦃a : α⦄ (a_1 : a ∈ A), B a_1 ⊆ s
hB_ne : ∀ ⦃a : α⦄ (a_1 : a ∈ A), (B a_1).Nonempty
hBc : ∀ ⦃a : α⦄ (a_1 : a ∈ A), (B a_1).Countable
hB_lub : ∀ ⦃a : α⦄ (a_1 : a ∈ A), IsLUB (B a_1) a
⊢ x ∈ {a | ∃ A, ∃ (_ : A ⊆ s) (_ : A.Nonempty) (_ : A.Countable), IsLUB A a}
Module: Mathlib.Order.Filter.ListTraverse

Goal state before:
pp: case mp.cons
α β : Type u
f : β → Filter α
b : β
fs : List β
ih : ∀ t ∈ traverse f fs, ∃ us, Forall₂ (fun b s ↦ s ∈ f b) fs us ∧ sequence us ⊆ t
t : Set (List α)
ht✝ : t ∈ traverse f (b :: fs)
u : Set (List α → List α)
hu : u ∈ cons <$> f b
v : Set (List α)
hv : v ∈ (fun x ↦ List.traverse f fs) ()
ht : u.seq v ⊆ t
w : Set α
hw : w ∈ f b
hwu : cons '' w ⊆ u
⊢ ∃ us, Forall₂ (fun b s ↦ s ∈ f b) (b :: fs) us ∧ sequence us ⊆ t

Tactic:
rcases ih v hv with ⟨us, hus, hu⟩

Goal state after:
case mp.cons
α β : Type u
f : β → Filter α
b : β
fs : List β
ih : ∀ t ∈ traverse f fs, ∃ us, Forall₂ (fun b s ↦ s ∈ f b) fs us ∧ sequence us ⊆ t
t : Set (List α)
ht✝ : t ∈ traverse f (b :: fs)
u : Set (List α → List α)
hu✝ : u ∈ cons <$> f b
v : Set (List α)
hv : v ∈ (fun x ↦ List.traverse f fs) ()
ht : u.seq v ⊆ t
w : Set α
hw : w ∈ f b
hwu : cons '' w ⊆ u
us : List (Set α)
hus : Forall₂ (fun b s ↦ s ∈ f b) fs us
hu : sequence us ⊆ v
⊢ ∃ us, Forall₂ (fun b s ↦ s ∈ f b) (b :: fs) us ∧ sequence us ⊆ t
Module: Mathlib.Order.Filter.CardinalInter

Goal state before:
pp: case mp.sInter
α : Type u
c : Cardinal.{u}
g : Set (Set α)
s : Set α
hreg : c.IsRegular
S : Set (Set α)
Sct : #↑S < c
a✝ : ∀ s ∈ S, CardinalGenerateSets g s
ih : ∀ s ∈ S, ∃ S ⊆ g, #↑S < c ∧ ⋂₀ S ⊆ s
⊢ ∃ S_1 ⊆ g, #↑S_1 < c ∧ ⋂₀ S_1 ⊆ ⋂₀ S

Tactic:
choose T Tg Tct hT using ih
      refine ⟨⋃ (s) (H : s ∈ S), T s H, by simpa,
        (Cardinal.card_biUnion_lt_iff_forall_of_isRegular hreg Sct).2 Tct, ?_⟩
      apply subset_sInter
      apply fun s H => subset_trans (sInter_subset_sInter (subset_iUnion₂ s H)) (hT s H)

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

Goal state before:
pp: case mp
α : Type u
c : Cardinal.{u}
g : Set (Set α)
s : Set α
hreg : c.IsRegular
h : s ∈ cardinalGenerate g ⋯
⊢ ∃ S ⊆ g, #↑S < c ∧ ⋂₀ S ⊆ s

Tactic:
induction h with

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

Goal state before:
pp: case mp
α : Type u
c : Cardinal.{u}
g : Set (Set α)
f : Filter α
inst✝ : CardinalInterFilter f c
hc : 2 < c
h : f ≤ cardinalGenerate g hc
⊢ g ⊆ f.sets

Tactic:
exact subset_trans (fun s => CardinalGenerateSets.basic) h

Goal state after:
Module: Mathlib.Order.Height

Goal state before:
pp: α : Type u_1
s : Set α
r : α → α → Prop
⊢ s.chainHeight (flip r) = s.chainHeight r

Tactic:
refine eq_of_forall_natCast_le_iff fun n ↦ ⟨fun hn ↦ ?_, fun hn ↦ ?_⟩

Goal state after:
case refine_1
α : Type u_1
s : Set α
r : α → α → Prop
n : ℕ
hn : ↑n ≤ s.chainHeight (flip r)
⊢ ↑n ≤ s.chainHeight r

case refine_2
α : Type u_1
s : Set α
r : α → α → Prop
n : ℕ
hn : ↑n ≤ s.chainHeight r
⊢ ↑n ≤ s.chainHeight (flip r)
Module: Mathlib.Order.Height

Goal state before:
pp: α : Type u_1
β : Type u_2
r : α → α → Prop
r' : β → β → Prop
s : Set α
e : r ↪r r'
⊢ (⇑e '' s).chainHeight r' = s.chainHeight r

Tactic:
refine eq_of_forall_natCast_le_iff fun n ↦ ⟨fun hn ↦ ?_, fun hn ↦ ?_⟩

Goal state after:
case refine_1
α : Type u_1
β : Type u_2
r : α → α → Prop
r' : β → β → Prop
s : Set α
e : r ↪r r'
n : ℕ
hn : ↑n ≤ (⇑e '' s).chainHeight r'
⊢ ↑n ≤ s.chainHeight r

case refine_2
α : Type u_1
β : Type u_2
r : α → α → Prop
r' : β → β → Prop
s : Set α
e : r ↪r r'
n : ℕ
hn : ↑n ≤ s.chainHeight r
⊢ ↑n ≤ (⇑e '' s).chainHeight r'
Module: Mathlib.Order.Lattice.Congruence

Goal state before:
pp: α : Type u_2
inst✝ : Lattice α
r : α → α → Prop
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)
x y : α
⊢ ∀ {z : α}, r x y → r y z → r x z

Tactic:
z

Goal state after:
α : Type u_2
inst✝ : Lattice α
r : α → α → Prop
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)
x y z : α
⊢ r x y → r y z → r x z
Module: Mathlib.Order.Monotone.MonovaryOrder

Goal state before:
pp: ι : Type u_1
α : Type u_3
β : Type u_4
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
f : ι → α
g : ι → β
s : Set ι
⊢ MonovaryOn f g s ↔ ∃ x, MonotoneOn f s ∧ MonotoneOn g s

Tactic:
by
  classical
  let := linearOrderOfSTO (MonovaryOrder f g)
  refine ⟨fun hfg => ⟨‹_›, monotoneOn_iff_forall_lt.2 fun i hi j hj hij => ?_,
    monotoneOn_iff_forall_lt.2 fun i hi j hj hij => ?_⟩, ?_⟩
  · obtain h | ⟨h, -⟩ := Prod.lex_iff.1 hij <;> exact h.le
  · obtain h | ⟨-, h⟩ := Prod.lex_iff.1 hij
    · exact hfg.symm hi hj h
    obtain h | ⟨h, -⟩ := Prod.lex_iff.1 h <;> exact h.le
  · rintro ⟨_, hf, hg⟩
    exact hf.monovaryOn hg

Goal state after:
Module: Mathlib.Order.PrimeIdeal

Goal state before:
pp: P : Type u_1
inst✝¹ : BooleanAlgebra P
I : Ideal P
inst✝ : I.IsProper
h : ∀ {x : P}, x ∈ I ∨ xᶜ ∈ I
⊢ ∀ {x y : P}, x ⊓ y ∈ I → x ∉ I → y ∈ I

Tactic:
intro x y hxy hxI

Goal state after:
P : Type u_1
inst✝¹ : BooleanAlgebra P
I : Ideal P
inst✝ : I.IsProper
h : ∀ {x : P}, x ∈ I ∨ xᶜ ∈ I
x y : P
hxy : x ⊓ y ∈ I
hxI : x ∉ I
⊢ y ∈ I
Module: Mathlib.Order.PrimeIdeal

Goal state before:
pp: P : Type u_1
inst✝¹ : BooleanAlgebra P
x : P
I : Ideal P
inst✝ : I.IsPrime
⊢ I.IsMaximal

Tactic:
by
  simp only [isMaximal_iff, Set.eq_univ_iff_forall, IsPrime.toIsProper, true_and]
  intro J hIJ x
  rcases Set.exists_of_ssubset hIJ with ⟨y, hyJ, hyI⟩
  suffices ass : x ⊓ y ⊔ x ⊓ yᶜ ∈ J by rwa [sup_inf_inf_compl] at ass
  exact
    sup_mem (J.lower inf_le_right hyJ)
      (hIJ.le <| I.lower inf_le_right <| IsPrime.compl_mem_of_notMem ‹_› hyI)

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 : α
ha : a ∈ {a | ∃ p ∈ P, ∃ q ∈ Q, a = p ⊓ q}
a' : α
ha' : a' ∈ {a | ∃ p ∈ P, ∃ q ∈ Q, a = p ⊓ q}
⊢ a ≠ a' → Function.onFun Disjoint id a a'

Tactic:
h

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 : α
ha : a ∈ {a | ∃ p ∈ P, ∃ q ∈ Q, a = p ⊓ q}
a' : α
ha' : a' ∈ {a | ∃ p ∈ P, ∃ q ∈ Q, a = p ⊓ q}
h : a ≠ a'
⊢ Function.onFun Disjoint id a a'
Module: Mathlib.Order.Partition.Basic

Goal state before:
pp: case refine_1.inr.inl
α : Type u_1
u : Set α
P : Partition u
f : α → α
a b : α
hf : P.IsRepFun f
hab : f a = f b
hne : a ≠ b
ha : a ∉ u
hb : b ∈ u
⊢ P.Rel a b

pp: case refine_1.inr.inr
α : Type u_1
u : Set α
P : Partition u
f : α → α
a b : α
hf : P.IsRepFun f
hab : f a = f b
hne : a ≠ b
ha : a ∉ u
hb : b ∉ u
⊢ P.Rel a b

Tactic:
· exact (hf.apply_eq_apply_iff_rel hb |>.mp hab.symm).symm

Goal state after:
case refine_1.inr.inr
α : Type u_1
u : Set α
P : Partition u
f : α → α
a b : α
hf : P.IsRepFun f
hab : f a = f b
hne : a ≠ b
ha : a ∉ u
hb : b ∉ u
⊢ P.Rel a b
Module: Mathlib.Order.Partition.Basic

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

Tactic:
rw [eq_comm, hf.apply_eq_apply_iff_rel ha]

Goal state after:
case inl
α : Type u_1
u : Set α
P : Partition u
f : α → α
a : α
hf : P.IsRepFun f
ha : a ∈ u
⊢ P.Rel 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
a b c : ↥S
⊢ a ≤ b ⇨ c ↔ a ⊓ b ≤ c

Tactic:
by simp [← Subtype.coe_le_coe, ← @Sublocale.coe_inf, himp]

Goal state after:
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
⊢ t₁ ≠ t₂ → Function.onFun Disjoint SetLike.coe t₁ t₂

Tactic:
h

Goal state after:
t : RootedTree
t₁ : SubRootedTree t
ht₁ : t₁ ∈ t.subtrees
t₂ : SubRootedTree t
ht₂ : t₂ ∈ t.subtrees
h : t₁ ≠ t₂
⊢ Function.onFun Disjoint SetLike.coe t₁ t₂
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 ℱ μ
this : ∀ᵐ (a : Ω) ∂μ, ∀ (i : ℕ), 0 a ≤ μ[f i.succ - f i | ↑ℱ i] a
ω : Ω
⊢ (∀ (i : ℕ), 0 ω ≤ μ[f i.succ - f i | ↑ℱ i] ω) → Monotone fun x ↦ predictablePart f ℱ μ x ω

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 ℱ μ
this : ∀ᵐ (a : Ω) ∂μ, ∀ (i : ℕ), 0 a ≤ μ[f i.succ - f i | ↑ℱ i] a
ω : Ω
h : ∀ (i : ℕ), 0 ω ≤ μ[f i.succ - f i | ↑ℱ i] ω
⊢ Monotone fun x ↦ predictablePart f ℱ μ x ω
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✝ : Ω
⊢ μ[f j | ↑ℱ i] a✝ = f i a✝ → a✝ ∈ s → f i a✝ = μ[f j | ↑ℱ i] a✝

Tactic:
heq

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✝ ∈ s → 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
ℱ : Filtration ι m0
inst✝⁵ : CompleteSpace E
inst✝⁴ : PartialOrder E
inst✝³ : IsOrderedAddMonoid E
inst✝² : IsOrderedModule ℝ E
inst✝¹ : ClosedIciTopology E
inst✝ : SigmaFiniteFiltration μ ℱ
f : ι → Ω → E
hf : Supermartingale f ℱ μ
i j : ι
hij : i ≤ j
s : Set Ω
hs : MeasurableSet s
a✝ : Ω
⊢ μ[f j | ↑ℱ i] a✝ ≤ f i a✝ → μ[f j | ↑ℱ i] a✝ ≤ f i a✝

Tactic:
heq

Goal state after:
Ω : 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
inst✝² : IsOrderedModule ℝ E
inst✝¹ : ClosedIciTopology E
inst✝ : SigmaFiniteFiltration μ ℱ
f : ι → Ω → E
hf : Supermartingale f ℱ μ
i j : ι
hij : i ≤ j
s : Set Ω
hs : MeasurableSet s
a✝ : Ω
heq : μ[f j | ↑ℱ i] a✝ ≤ f i a✝
⊢ μ[f j | ↑ℱ i] a✝ ≤ f i a✝
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
ℱ : Filtration ℕ m0
inst✝¹ : CompleteSpace E
inst✝ : SigmaFiniteFiltration μ ℱ
f g : ℕ → Ω → E
hf : Martingale f ℱ μ
hg : StronglyAdapted ℱ fun n ↦ g (n + 1)
hg0 : g 0 = 0
hgint : ∀ (n : ℕ), Integrable (g n) μ
n : ℕ
⊢ martingalePart (f + g) ℱ μ n =ᵐ[μ] f n

Tactic:
set h := f - martingalePart (f + g) ℱ μ with hhdef

Goal state after:
Ω : Type u_1
E : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
ℱ : Filtration ℕ m0
inst✝¹ : CompleteSpace E
inst✝ : SigmaFiniteFiltration μ ℱ
f g : ℕ → Ω → E
hf : Martingale f ℱ μ
hg : StronglyAdapted ℱ fun n ↦ g (n + 1)
hg0 : g 0 = 0
hgint : ∀ (n : ℕ), Integrable (g n) μ
n : ℕ
h : ℕ → Ω → E := f - martingalePart (f + g) ℱ μ
hhdef : h = f - martingalePart (f + g) ℱ μ
⊢ martingalePart (f + g) ℱ μ 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
ℱ : Filtration ℕ m0
inst✝¹ : CompleteSpace E
inst✝ : SigmaFiniteFiltration μ ℱ
f g : ℕ → Ω → E
hf : Martingale f ℱ μ
hg : StronglyAdapted ℱ fun n ↦ g (n + 1)
hg0 : g 0 = 0
hgint : ∀ (n : ℕ), Integrable (g n) μ
n : ℕ
h : ℕ → Ω → E := f - martingalePart (f + g) ℱ μ
hhdef : h = f - martingalePart (f + g) ℱ μ
⊢ f - martingalePart (f + g) ℱ μ = predictablePart (f + g) ℱ μ - g

Tactic:
sub_eq_sub_iff_add_eq_add,

Goal state after:
Ω : Type u_1
E : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
ℱ : Filtration ℕ m0
inst✝¹ : CompleteSpace E
inst✝ : SigmaFiniteFiltration μ ℱ
f g : ℕ → Ω → E
hf : Martingale f ℱ μ
hg : StronglyAdapted ℱ fun n ↦ g (n + 1)
hg0 : g 0 = 0
hgint : ∀ (n : ℕ), Integrable (g n) μ
n : ℕ
h : ℕ → Ω → E := f - martingalePart (f + g) ℱ μ
hhdef : h = f - martingalePart (f + g) ℱ μ
⊢ f + g = predictablePart (f + g) ℱ μ + martingalePart (f + g) ℱ μ
Module: Mathlib.Probability.Process.Stopping

Goal state before:
pp: case mp
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : PartialOrder ι
τ : Ω → WithTop ι
f : Filtration ι m
hτ : IsStoppingTime f τ
h_countable : (Set.range τ).Countable
i : ι
a : Ω
h : τ a = ↑i
⊢ τ a ≤ ↑i ∧ ∀ (x : Ω), τ x < ↑i → ¬τ a ≤ τ x

Tactic:
simp only [h, lt_iff_le_not_ge, le_refl, and_imp, imp_self, imp_true_iff, and_self_iff]

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

Goal state before:
pp: case mpr
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝¹ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n i : ι
ω : Ω
inst✝ : WellFoundedLT ι
j : ι
hj₁ : j ∈ Set.Icc n i
hj₂ : u j ω ∈ s
⊢ hittingAfter u s n ω ≤ ↑j

Tactic:
exact hittingAfter_le_of_mem hj₁.1 hj₂

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

Goal state before:
pp: case mpr
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝¹ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n i : ι
ω : Ω
inst✝ : WellFoundedLT ι
h' : ∃ j ∈ Set.Icc n i, u j ω ∈ s
⊢ hittingAfter u s n ω ≤ ↑i

Tactic:
obtain ⟨j, hj₁, hj₂⟩ := h'
    refine le_trans ?_ (mod_cast hj₁.2 : (j : WithTop ι) ≤ i)
    exact hittingAfter_le_of_mem hj₁.1 hj₂

Goal state after: