mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.NumberTheory.Padics.WithVal

Goal state before:
pp: case h
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp0' : 0 < ↑p
hp0 : 0 < (↑p)⁻¹
hp1' : 1 < ↑p
hp1 : (↑p)⁻¹ < 1
γ : (MonoidWithZeroHom.ofClass Valued.v).ValueGroup₀ˣ
x y : WithVal (Rat.padicValuation p)
h : ↑(padicNorm p ((WithVal.equiv (Rat.padicValuation p)) (x - y))) ≤ (↑p ^ (embedding ↑γ * exp (-1)).log.natAbs)⁻¹
x' : ℚ := (WithVal.equiv (Rat.padicValuation p)) x
hx : x' = (WithVal.equiv (Rat.padicValuation p)) x
y' : ℚ := (WithVal.equiv (Rat.padicValuation p)) y
hy : y' = (WithVal.equiv (Rat.padicValuation p)) y
⊢ Valued.v.restrict (x - y) < ↑γ

Tactic:
Valuation.restrict_lt_iff_lt_embedding

Goal state after:
case h
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp0' : 0 < ↑p
hp0 : 0 < (↑p)⁻¹
hp1' : 1 < ↑p
hp1 : (↑p)⁻¹ < 1
γ : (MonoidWithZeroHom.ofClass Valued.v).ValueGroup₀ˣ
x y : WithVal (Rat.padicValuation p)
h : ↑(padicNorm p ((WithVal.equiv (Rat.padicValuation p)) (x - y))) ≤ (↑p ^ (embedding ↑γ * exp (-1)).log.natAbs)⁻¹
x' : ℚ := (WithVal.equiv (Rat.padicValuation p)) x
hx : x' = (WithVal.equiv (Rat.padicValuation p)) x
y' : ℚ := (WithVal.equiv (Rat.padicValuation p)) y
hy : y' = (WithVal.equiv (Rat.padicValuation p)) y
⊢ Valued.v (x - y) < embedding ↑γ
Module: Mathlib.NumberTheory.Pell

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

Tactic:
intro hy
  have prop := a.prop
  rw [hy, sq (0 : ℤ), zero_mul, mul_zero, sub_zero] at prop
  exact lt_irrefl _ (((one_lt_sq_iff₀ <| zero_le_one.trans ha.le).mpr ha).trans_eq prop)

Goal state after:
Module: Mathlib.NumberTheory.Pell

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

Tactic:
induction n with
  | zero => simp only [pow_zero, x_one, zero_lt_one]
  | succ n ih => rw [pow_succ]; exact x_mul_pos ih hax

Goal state after:
Module: Mathlib.NumberTheory.Pell

Goal state before:
pp: case inr.inr.inr
d : ℤ
a₁ : Solution₁ d
h : IsFundamental a₁
a b : Solution₁ d
hbx : 0 < b.x
hby : 0 ≤ b.y
n : ℕ
hn : b = a₁ ^ n
hb : a ∈ {-b⁻¹}
⊢ ∃ n, a = a₁ ^ n ∨ a = -a₁ ^ n

Tactic:
rw [Set.mem_singleton_iff] at hb
    rw [hb]
    exact ⟨-n, Or.inr (by simp [hn])⟩

Goal state after:
Module: Mathlib.NumberTheory.Padics.Hensel

Goal state before:
pp: p : ℕ
inst✝² : Fact (Nat.Prime p)
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Algebra R ℤ_[p]
F : Polynomial R
a : ℤ_[p]
hnorm : ‖(Polynomial.aeval a) F‖ < ‖(Polynomial.aeval a) (Polynomial.derivative F)‖ ^ 2
hnsol : (Polynomial.aeval a) F ≠ 0
⊢ ‖soln - a‖ < ‖(Polynomial.aeval a) (Polynomial.derivative F)‖

Tactic:
by
  rw [soln_dist_to_a, div_lt_iff₀ (deriv_norm_pos _), ← sq] <;> assumption

Goal state after:
Module: Mathlib.NumberTheory.SelbergSieve

Goal state before:
pp: case hfg
s : BoundingSieve
d : ℕ
hdP : d ∣ s.prodPrimes
hd_ne_one : d ≠ 1
hd_sq : Squarefree d
this : d ≠ 0
⊢ ∀ i ∈ d.primeFactors, s.nu i < 1

Tactic:
intro p hpd; rw [mem_primeFactors_of_ne_zero hd_sq.ne_zero] at hpd
        apply s.nu_lt_one_of_prime p hpd.left (hpd.2.trans hdP)

Goal state after:
Module: Mathlib.NumberTheory.RatFunc.Ostrowski

Goal state before:
pp: K : Type u_1
Γ : Type u_2
inst✝³ : Field K
inst✝² : LinearOrderedCommGroupWithZero Γ
v : Valuation K⟮X⟯ Γ
inst✝¹ : v.IsNontrivial
inst✝ : IsTrivialOn K v
hle : v X ≤ 1
hv : v.IsRankOneDiscrete
h0 : v ↑πᵥ ≠ 0
⊢ v ↑πᵥ = ↑(IsRankOneDiscrete.generator v)

Tactic:
← hv.valueGroup_genLTOne_eq_generator,

Goal state after:
K : Type u_1
Γ : Type u_2
inst✝³ : Field K
inst✝² : LinearOrderedCommGroupWithZero Γ
v : Valuation K⟮X⟯ Γ
inst✝¹ : v.IsNontrivial
inst✝ : IsTrivialOn K v
hle : v X ≤ 1
hv : v.IsRankOneDiscrete
h0 : v ↑πᵥ ≠ 0
⊢ v ↑πᵥ = ↑(LinearOrderedCommGroup.Subgroup.genLTOne (MonoidWithZeroHom.ofClass v).valueGroup)
Module: Mathlib.NumberTheory.RamificationInertia.Basic

Goal state before:
pp: R : Type u
inst✝¹⁵ : CommRing R
S : Type v
inst✝¹⁴ : CommRing S
inst✝¹³ : Algebra R S
K : Type u_1
inst✝¹² : Field K
inst✝¹¹ : Algebra R K
V : Type u_3
V' : Type u_4
V'' : Type u_5
inst✝¹⁰ : AddCommGroup V
inst✝⁹ : Module R V
inst✝⁸ : Module K V
inst✝⁷ : IsScalarTower R K V
inst✝⁶ : AddCommGroup V'
inst✝⁵ : Module R V'
inst✝⁴ : Module S V'
inst✝³ : IsScalarTower R S V'
inst✝² : AddCommGroup V''
inst✝¹ : Module R V''
hRK : IsFractionRing R K
inst✝ : IsDedekindDomain R
hRS : RingHom.ker f ≠ ⊤
F : V'' →ₗ[R] V
hf : Function.Injective ⇑F
f' : V'' →ₗ[R] V'
ι : Type u_6
b : ι → V''
hb : ¬LinearIndependent K (⇑F ∘ b)
⊢ ¬LinearIndependent S (⇑f' ∘ b)

Tactic:
simp only [linearIndependent_iff', not_forall] at hb ⊢

Goal state after:
R : Type u
inst✝¹⁵ : CommRing R
S : Type v
inst✝¹⁴ : CommRing S
inst✝¹³ : Algebra R S
K : Type u_1
inst✝¹² : Field K
inst✝¹¹ : Algebra R K
V : Type u_3
V' : Type u_4
V'' : Type u_5
inst✝¹⁰ : AddCommGroup V
inst✝⁹ : Module R V
inst✝⁸ : Module K V
inst✝⁷ : IsScalarTower R K V
inst✝⁶ : AddCommGroup V'
inst✝⁵ : Module R V'
inst✝⁴ : Module S V'
inst✝³ : IsScalarTower R S V'
inst✝² : AddCommGroup V''
inst✝¹ : Module R V''
hRK : IsFractionRing R K
inst✝ : IsDedekindDomain R
hRS : RingHom.ker f ≠ ⊤
F : V'' →ₗ[R] V
hf : Function.Injective ⇑F
f' : V'' →ₗ[R] V'
ι : Type u_6
b : ι → V''
hb : ∃ x x_1, ∃ (_ : ∑ i ∈ x, x_1 i • (⇑F ∘ b) i = 0), ∃ x_2, ∃ (_ : x_2 ∈ x), ¬x_1 x_2 = 0
⊢ ∃ x x_1, ∃ (_ : ∑ i ∈ x, x_1 i • (⇑f' ∘ b) i = 0), ∃ x_2, ∃ (_ : x_2 ∈ x), ¬x_1 x_2 = 0
Module: Mathlib.NumberTheory.Transcendental.Lindemann.AnalyticalPart

Goal state before:
pp: case hbc.convert_10
f : ℕ → ℂ[X]
s : ℂ
c : ℝ
hc : ∀ (p : ℕ), ∀ x ∈ Set.Ioc 0 1, ‖eval (x • s) (f p)‖ ≤ c ^ p
p : ℕ
⊢ MeasureTheory.volume (Set.Ioc 0 1) < ⊤

Tactic:
Real.volume_Ioc,

Goal state after:
case hbc.convert_10
f : ℕ → ℂ[X]
s : ℂ
c : ℝ
hc : ∀ (p : ℕ), ∀ x ∈ Set.Ioc 0 1, ‖eval (x • s) (f p)‖ ≤ c ^ p
p : ℕ
⊢ ENNReal.ofReal (1 - 0) < ⊤
Module: Mathlib.NumberTheory.Transcendental.Liouville.Basic

Goal state before:
pp: x : ℝ
h : Liouville x
⊢ Irrational x

Tactic:
by
  -- By contradiction, `x = a / b`, with `a ∈ ℤ`, `0 < b ∈ ℕ` is a Liouville number,
  rintro ⟨⟨a, b, bN0, cop⟩, rfl⟩
  -- clear up the mess of constructions of rationals
  rw [Rat.cast_mk'] at h
  -- Since `a / b` is a Liouville number, there are `p, q ∈ ℤ`, with `q1 : 1 < q`,∈
  -- `a0 : a / b ≠ p / q` and `a1 : |a / b - p / q| < 1 / q ^ (b + 1)`
  rcases h (b + 1) with ⟨p, q, q1, a0, a1⟩
  -- A few useful inequalities
  have qR0 : (0 : ℝ) < q := Int.cast_pos.mpr (zero_lt_one.trans q1)
  have b0 : (b : ℝ) ≠ 0 := Nat.cast_ne_zero.mpr bN0
  have bq0 : (0 : ℝ) < b * q := mul_pos (Nat.cast_pos.mpr bN0.bot_lt) qR0
  -- At a1, clear denominators...
  replace a1 : |a * q - b * p| * q ^ (b + 1) < b * q := by
    rw [div_sub_div _ _ b0 qR0.ne', abs_div, div_lt_div_iff₀ (abs_pos.mpr bq0.ne') (pow_pos qR0 _),
      abs_of_pos bq0, one_mul] at a1
    exact mod_cast a1
  -- At a0, clear denominators...
  replace a0 : a * q - ↑b * p ≠ 0 := by
    rw [Ne, div_eq_div_iff b0 qR0.ne', mul_comm (p : ℝ), ← sub_eq_zero] at a0
    exact mod_cast a0
  -- Actually, `q` is a natural number
  lift q to ℕ using (zero_lt_one.trans q1).le
  -- Looks innocuous, but we now have an integer with non-zero absolute value: this is at
  -- least one away from zero.  The gain here is what gets the proof going.
  have ap : 0 < |a * ↑q - ↑b * p| := abs_pos.mpr a0
  -- Actually, the absolute value of an integer is a natural number
  -- FIXME: This `lift` call duplicates the hypotheses `a1` and `ap`
  lift |a * ↑q - ↑b * p| to ℕ using abs_nonneg (a * ↑q - ↑b * p) with e he
  norm_cast at a1 ap q1
  -- Recall this is by contradiction: we obtained the inequality `b * q ≤ x * q ^ (b + 1)`, so
  -- we are done.
  exact not_le.mpr a1 (Nat.mul_lt_mul_pow_succ ap q1).le

Goal state after:
Module: Mathlib.NumberTheory.RamificationInertia.Basic

Goal state before:
pp: case hP0
R : Type u
inst✝⁴ : CommRing R
S : Type v
inst✝³ : CommRing S
inst✝² : Algebra R S
p : Ideal R
inst✝¹ : IsDedekindDomain S
inst✝ : p.IsMaximal
P : ↥(factors (map f p)).toFinset
⊢ ↑P ≠ ⊥

pp: case he
R : Type u
inst✝⁴ : CommRing R
S : Type v
inst✝³ : CommRing S
inst✝² : Algebra R S
p : Ideal R
inst✝¹ : IsDedekindDomain S
inst✝ : p.IsMaximal
P : ↥(factors (map f p)).toFinset
⊢ p.ramificationIdx' ↑P ≠ 0

Tactic:
exacts [Factors.ne_bot p P, NeZero.ne _]

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

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

Tactic:
rw [mem_roots'] at hr
    rw [Polynomial.map_mul, f.map_pow]
    exact dvd_mul_of_dvd_right (pow_dvd_pow_of_dvd (dvd_iff_isRoot.mpr hr.2) _) _

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

Goal state before:
pp: case refine_1
⊢ {x | Liouville x} ⊆ {x | Irrational x} ∩ ⋂ n, ⋃ a, ⋃ b, ⋃ (_ : 1 < b), ball (↑a / ↑b) (1 / ↑b ^ n)

pp: case refine_2
⊢ {x | Irrational x} ∩ ⋂ n, ⋃ a, ⋃ b, ⋃ (_ : 1 < b), ball (↑a / ↑b) (1 / ↑b ^ n) ⊆ {x | Liouville x}

Tactic:
· refine subset_inter (fun x hx => hx.irrational) ?_
    rw [setOfPred_liouville_eq_iInter_iUnion]
    exact iInter_mono fun n => iUnion₂_mono fun a b => iUnion_mono fun _hb => sdiff_subset

Goal state after:
case refine_2
⊢ {x | Irrational x} ∩ ⋂ n, ⋃ a, ⋃ b, ⋃ (_ : 1 < b), ball (↑a / ↑b) (1 / ↑b ^ n) ⊆ {x | Liouville x}
Module: Mathlib.NumberTheory.Wilson

Goal state before:
pp: case inr
n : ℕ
h : ↑(n - 1)! = -1
h0 : n ≠ 0
h1 : 1 < n
⊢ Prime n

Tactic:
by_contra h2

Goal state after:
case inr
n : ℕ
h : ↑(n - 1)! = -1
h0 : n ≠ 0
h1 : 1 < n
h2 : ¬Prime n
⊢ False
Module: Mathlib.Order.Bounded

Goal state before:
pp: α : Type u_1
s : Set α
inst✝¹ : Preorder α
inst✝ : NoMaxOrder α
a : α
ha : ∀ (b : α), b ∈ s → (fun x1 x2 ↦ x1 ≤ x2) b a
b : α
hb : a < b
⊢ Bounded (fun x1 x2 ↦ x1 < x2) s

Tactic:
exact ⟨b, fun c hc => lt_of_le_of_lt (ha c hc) hb⟩

Goal state after:
Module: Mathlib.NumberTheory.WellApproximable

Goal state before:
pp: A : Type u_1
inst✝ : SeminormedCommGroup A
m : ℕ
δ : ℝ
n : ℕ
hm : 0 < m
⊢ (fun y ↦ y ^ m) '' approxOrderOf A (n * m) δ ⊆ approxOrderOf A n (↑m * δ)

Tactic:
by
  rintro - ⟨a, ha, rfl⟩
  obtain ⟨b, hb : orderOf b = n * m, hab : a ∈ ball b δ⟩ := mem_approxOrderOf_iff.mp ha
  replace hb : b ^ m ∈ {y : A | orderOf y = n} := by
    rw [mem_ofPred_eq, orderOf_pow' b hm.ne', hb, Nat.gcd_mul_left_left, n.mul_div_cancel hm]
  apply ball_subset_thickening hb (m * δ)
  convert! pow_mem_ball hm hab using 1
  simp only [nsmul_eq_mul]

Goal state after:
Module: Mathlib.Order.CountableSupClosed

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

Tactic:
intro a ha b hb

Goal state after:
α : Type u_2
inst✝ : Preorder α
s : Set α
a : α
ha : a ∈ upperBounds s
b : α
hb : b ∈ countableSupClosure s
⊢ b ≤ a
Module: Mathlib.Order.Filter.CardinalInter

Goal state before:
pp: ι α : Type u
c : Cardinal.{u}
l : Filter α
inst✝ : CardinalInterFilter l c
S : Set ι
hS : #↑S < c
s t : (i : ι) → i ∈ S → Set α
h : ∀ (i : ι) (hi : i ∈ S), s i hi ≤ᶠ[l] t i hi
⊢ ⋂ i, ⋂ (h : i ∈ S), s i h ≤ᶠ[l] ⋂ i, ⋂ (h : i ∈ S), t i h

Tactic:
simp only [biInter_eq_iInter]
  exact EventuallyLE.cardinal_iInter hS fun i => h i i.2

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

Goal state before:
pp: case mp
α : Type u
β : Type v
γ : Type w
r : SetRel α β
s : SetRel β γ
l : Filter γ
t : Set α
u : Set β
h : r.core u ⊆ t
v : Set γ
vsets : v ∈ l
hv : s.core v ⊆ u
⊢ ∃ a ∈ l, r.core (s.core a) ⊆ t

Tactic:
exact ⟨v, vsets, Set.Subset.trans (SetRel.core_mono hv) h⟩

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

Goal state before:
pp: case mpr.superset
α : Type u
c : Cardinal.{u}
g : Set (Set α)
f : Filter α
inst✝ : CardinalInterFilter f c
hc : 2 < c
h : g ⊆ f.sets
s s✝ t✝ : Set α
a✝ : CardinalGenerateSets g s✝
st : s✝ ⊆ t✝
ih : s✝ ∈ f
⊢ t✝ ∈ f

Tactic:
| superset _ st ih =>

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

Goal state before:
pp: case mpr.sInter
α : Type u
c : Cardinal.{u}
g : Set (Set α)
f : Filter α
inst✝ : CardinalInterFilter f c
hc : 2 < c
h : g ⊆ f.sets
s : Set α
S✝ : Set (Set α)
Sct : #↑S✝ < c
a✝ : ∀ s ∈ S✝, CardinalGenerateSets g s
ih : ∀ s ∈ S✝, s ∈ f
⊢ ⋂₀ S✝ ∈ f

Tactic:
| sInter Sct _ ih =>

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

Goal state before:
pp: α : Type u_1
inst✝² : Semiring α
inst✝¹ : LinearOrder α
inst✝ : FloorSemiring α
a b : α
n : ℕ
ha : 0 ≤ a
⊢ ↑n ∈ Set.Ioo a b ↔ n ∈ Finset.Ioo ⌊a⌋₊ ⌈b⌉₊

Tactic:
by
  simp [floor_lt ha, lt_ceil]

Goal state after:
Module: Mathlib.Order.KonigLemma

Goal state before:
pp: α : ℕ → Type u_1
inst✝¹ : Finite (α 0)
inst✝ : ∀ (i : ℕ), Nonempty (α i)
π : {i j : ℕ} → i ≤ j → α j → α i
π_refl : ∀ ⦃i : ℕ⦄ (a : α i), π ⋯ a = a
π_trans : ∀ ⦃i j k : ℕ⦄ (hij : i ≤ j) (hjk : j ≤ k) (a : α k), π hij (π hjk a) = π ⋯ a
hfin : ∀ (i : ℕ) (a : α i), {b | π ⋯ b = a}.Finite
αs : Type u_1 := (i : ℕ) × α i
x✝ : PartialOrder αs :=
  { le := fun a b ↦ ∃ (h : a.fst ≤ b.fst), π h b.snd = a.snd, le_refl := ⋯, le_trans := ⋯, lt_iff_le_not_ge := ⋯,
    le_antisymm := ⋯ }
hcovby : ∀ {a b : αs}, a ⋖ b ↔ a ≤ b ∧ a.fst + 1 = b.fst
this : IsStronglyAtomic αs
a₀ : α 0
ha₀ : Infinite ↑((fun a ↦ π ⋯ a.snd) ⁻¹' {a₀})
⊢ ∃ a₀, a₀.fst = 0 ∧ (Ici a₀).Infinite

Tactic:
refine ⟨⟨0, a₀⟩, rfl, (infinite_coe_iff.1 ha₀).mono ?_⟩

Goal state after:
α : ℕ → Type u_1
inst✝¹ : Finite (α 0)
inst✝ : ∀ (i : ℕ), Nonempty (α i)
π : {i j : ℕ} → i ≤ j → α j → α i
π_refl : ∀ ⦃i : ℕ⦄ (a : α i), π ⋯ a = a
π_trans : ∀ ⦃i j k : ℕ⦄ (hij : i ≤ j) (hjk : j ≤ k) (a : α k), π hij (π hjk a) = π ⋯ a
hfin : ∀ (i : ℕ) (a : α i), {b | π ⋯ b = a}.Finite
αs : Type u_1 := (i : ℕ) × α i
x✝ : PartialOrder αs :=
  { le := fun a b ↦ ∃ (h : a.fst ≤ b.fst), π h b.snd = a.snd, le_refl := ⋯, le_trans := ⋯, lt_iff_le_not_ge := ⋯,
    le_antisymm := ⋯ }
hcovby : ∀ {a b : αs}, a ⋖ b ↔ a ≤ b ∧ a.fst + 1 = b.fst
this : IsStronglyAtomic αs
a₀ : α 0
ha₀ : Infinite ↑((fun a ↦ π ⋯ a.snd) ⁻¹' {a₀})
⊢ (fun a ↦ π ⋯ a.snd) ⁻¹' {a₀} ⊆ Ici ⟨0, a₀⟩
Module: Mathlib.Order.SaddlePoint

Goal state before:
pp: E : Type u_1
F : Type u_2
β : Type u_3
X : Set E
Y : Set F
f : E → F → β
inst✝ : CompleteLinearOrder β
y : F
hy : y ∈ Y
⊢ ⨅ x ∈ X, f x y ≤ ⨅ x ∈ X, ⨆ y ∈ Y, f x y

Tactic:
le_iInf₂_iff

Goal state after:
E : Type u_1
F : Type u_2
β : Type u_3
X : Set E
Y : Set F
f : E → F → β
inst✝ : CompleteLinearOrder β
y : F
hy : y ∈ Y
⊢ ∀ i ∈ X, ⨅ x ∈ X, f x y ≤ ⨆ y ∈ Y, f i y
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
⊢ f a b ≤ ⨅ x ∈ X, ⨆ y ∈ Y, f x y

Tactic:
← h.2

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 ∈ X, f x b ≤ ⨅ x ∈ X, ⨆ y ∈ Y, f x y
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
⊢ f a b ≤ ⨅ x ∈ X, ⨆ y ∈ Y, f x y

Tactic:
rw [← h.2]
      apply iInf₂_mono
      intro x _
      apply le_iSup₂ b hb

Goal state after:
Module: Mathlib.Order.ScottContinuity.Prod

Goal state before:
pp: case refine_1
α : Type u_1
β : Type u_2
α' : Type u_4
β' : Type u_5
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : Preorder α'
inst✝ : Preorder β'
f : α → α'
g : β → β'
hf : ScottContinuous f
hg : ScottContinuous g
a : α
d : Set β
hd₁ : d.Nonempty
hd₂ : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) d
c : β
hdc : IsLUB d c
e1 : (fun b ↦ (f a, g b)) '' d = {f a} ×ˢ (g '' d)
⊢ IsLUB ((fun b ↦ Prod.map f g (a, b)) '' d) (Prod.map f g (a, c))

Tactic:
Prod.map_apply,

Goal state after:
case refine_1
α : Type u_1
β : Type u_2
α' : Type u_4
β' : Type u_5
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : Preorder α'
inst✝ : Preorder β'
f : α → α'
g : β → β'
hf : ScottContinuous f
hg : ScottContinuous g
a : α
d : Set β
hd₁ : d.Nonempty
hd₂ : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) d
c : β
hdc : IsLUB d c
e1 : (fun b ↦ (f a, g b)) '' d = {f a} ×ˢ (g '' d)
⊢ IsLUB ((fun a_1 ↦ (f a, g a_1)) '' d) (f a, g c)
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
⊢ f a b ≤ ⨆ y ∈ Y, ⨅ x ∈ X, f x y

Tactic:
← h.2

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 ∈ X, f x b ≤ ⨆ y ∈ Y, ⨅ x ∈ X, f x y
Module: Mathlib.Order.ScottContinuity.Prod

Goal state before:
pp: case refine_2
α : Type u_1
β : Type u_2
α' : Type u_4
β' : Type u_5
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : Preorder α'
inst✝ : Preorder β'
f : α → α'
g : β → β'
hf : ScottContinuous f
hg : ScottContinuous g
b : β
d : Set α
hd₁ : d.Nonempty
hd₂ : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) d
c : α
hdc : IsLUB d c
e2 : (fun a ↦ (f a, g b)) '' d = (f '' d) ×ˢ {g b}
⊢ IsLUB ((fun a ↦ Prod.map f g (a, b)) '' d) (Prod.map f g (c, b))

Tactic:
Prod.map_apply,

Goal state after:
case refine_2
α : Type u_1
β : Type u_2
α' : Type u_4
β' : Type u_5
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : Preorder α'
inst✝ : Preorder β'
f : α → α'
g : β → β'
hf : ScottContinuous f
hg : ScottContinuous g
b : β
d : Set α
hd₁ : d.Nonempty
hd₂ : DirectedOn (fun x1 x2 ↦ x1 ≤ x2) d
c : α
hdc : IsLUB d c
e2 : (fun a ↦ (f a, g b)) '' d = (f '' d) ×ˢ {g b}
⊢ IsLUB ((fun a ↦ (f a, g b)) '' d) (f c, g b)
Module: Mathlib.Order.Std

Goal state before:
pp: α : Type u_1
args : OfStdArgs α
this✝⁷ : LE α := args.le
this✝⁶ : LT α := args.lt
this✝⁵ :
  let this := args.le;
  let this_1 := args.lt;
  Std.LawfulOrderLT α
this✝⁴ :
  let this := args.le;
  Std.IsLinearOrder α
this✝³ : DecidableLE α := args.decidableLE
this✝² : Std.LawfulOrderLeftLeaningMin α
this✝¹ : Std.LawfulOrderLeftLeaningMax α
a b : α
this✝ : Ord α := args.ord
this :
  let this := args.le;
  let this_1 := args.lt;
  let this_2 := ⋯;
  let this_3 := ⋯;
  let this_4 := args.decidableEq;
  let this_5 := args.decidableLT;
  Std.LawfulOrderOrd α
h : ¬a < b
h' : ¬a = b
⊢ compare a b = Ordering.gt

Tactic:
exact Std.compare_eq_gt.mpr <| Std.lt_of_le_of_ne (Std.not_lt.mp h) (Ne.symm h')

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

Goal state before:
pp: Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst✝⁴ : Preorder ι
f : Filtration ι m
β : Type u_3
inst✝³ : TopologicalSpace β
inst✝² : MeasurableSpace ι
γ : Type u_4
inst✝¹ : CommMonoid β
inst✝ : ContinuousMul β
U : γ → ι → Ω → β
s : Finset γ
h : ∀ c ∈ s, IsStronglyProgressive f (U c)
⊢ IsStronglyProgressive f fun i a ↦ ∏ c ∈ s, U c i a

Tactic:
convert! IsStronglyProgressive.finsetProd' h using 1

Goal state after:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst✝⁴ : Preorder ι
f : Filtration ι m
β : Type u_3
inst✝³ : TopologicalSpace β
inst✝² : MeasurableSpace ι
γ : Type u_4
inst✝¹ : CommMonoid β
inst✝ : ContinuousMul β
U : γ → ι → Ω → β
s : Finset γ
h : ∀ c ∈ s, IsStronglyProgressive f (U c)
⊢ (fun i a ↦ ∏ c ∈ s, U c i a) = ∏ c ∈ s, U c
Module: Mathlib.Probability.Process.Predictable

Goal state before:
pp: case inr.inr
Ω : Type u_1
m : MeasurableSpace Ω
𝓕 : Filtration ℕ m
s : Set (ℕ × Ω)
hs : MeasurableSet s
n i : ℕ
A : Set Ω
hA : MeasurableSet A
hin : i ≤ n
⊢ MeasurableSet ({⟨n + 1, ⋯⟩} ×ˢ A)

pp: Ω : Type u_1
m : MeasurableSpace Ω
𝓕 : Filtration ℕ m
s : Set (ℕ × Ω)
hs : MeasurableSet s
n i : ℕ
A : Set Ω
hA : MeasurableSet A
hin : i ≤ n
⊢ (fun p ↦ (↑p.1, p.2)) ⁻¹' Set.Ioi i ×ˢ A = {⟨n + 1, ⋯⟩} ×ˢ A

Tactic:
· exact MeasurableSet.prod (MeasurableSet.of_subtype_image trivial) (𝓕.mono hin _ hA)

Goal state after:
Ω : Type u_1
m : MeasurableSpace Ω
𝓕 : Filtration ℕ m
s : Set (ℕ × Ω)
hs : MeasurableSet s
n i : ℕ
A : Set Ω
hA : MeasurableSet A
hin : i ≤ n
⊢ (fun p ↦ (↑p.1, p.2)) ⁻¹' Set.Ioi i ×ˢ A = {⟨n + 1, ⋯⟩} ×ˢ A
Module: Mathlib.Probability.Process.Predictable

Goal state before:
pp: Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
E : Type u_3
inst✝⁶ : TopologicalSpace E
inst✝⁵ : LinearOrder ι
inst✝⁴ : OrderBot ι
inst✝³ : MeasurableSpace ι
inst✝² : TopologicalSpace ι
inst✝¹ : OpensMeasurableSpace ι
inst✝ : OrderClosedTopology ι
𝓕 : Filtration ι m
u : ι → Ω → E
h𝓕 : IsStronglyPredictable 𝓕 u
i : ι
⊢ StronglyMeasurable fun p ↦ u (↑p.1) p.2

Tactic:
let : MeasurableSpace (ι × Ω) := 𝓕.predictable

Goal state after:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
E : Type u_3
inst✝⁶ : TopologicalSpace E
inst✝⁵ : LinearOrder ι
inst✝⁴ : OrderBot ι
inst✝³ : MeasurableSpace ι
inst✝² : TopologicalSpace ι
inst✝¹ : OpensMeasurableSpace ι
inst✝ : OrderClosedTopology ι
𝓕 : Filtration ι m
u : ι → Ω → E
h𝓕 : IsStronglyPredictable 𝓕 u
i : ι
this : MeasurableSpace (ι × Ω) := 𝓕.predictable
⊢ StronglyMeasurable fun p ↦ u (↑p.1) p.2
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 ℱ μ
⊢ ∀ᵐ (ω : Ω) ∂μ, ∀ (n : ℕ), 0 ≤ predictablePart f ℱ μ n ω

Tactic:
filter_upwards [hf.monotone_predictablePart] with ω hω n
  simpa [predictablePart_zero] using hω (Nat.zero_le n)

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 : Submartingale f ℱ μ
⊢ Supermartingale (-f) ℱ μ

Tactic:
by
  refine ⟨hf.1.neg, fun i j hij => (condExp_neg ..).le.trans ?_, fun i => (hf.2.2 i).neg⟩
  filter_upwards [hf.2.1 i j hij] with _ _
  simpa

Goal state after: