mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.NumberTheory.NumberField.House

Goal state before:
pp: K : Type u_1
inst✝⁴ : Field K
inst✝³ : NumberField K
α : Type u_2
β : Type u_3
a : Matrix α β (𝓞 K)
ha : a ≠ 0
p q : ℕ
h0p : 0 < p
hpq : p < q
inst✝² : Fintype β
cardβ : Fintype.card β = q
A : ℝ
habs : ∀ (k : α) (l : β), house ((algebraMap (𝓞 K) K) (a k l)) ≤ A
inst✝¹ : DecidableEq (K →+* ℂ)
inst✝ : Fintype α
cardα : Fintype.card α = p
h : ℕ := finrank ℚ K
hphqh : p * h < q * h
h0ph : 0 < p * h
hfinp : Fintype.card (α × (K →+* ℂ)) = p * h
hfinq : Fintype.card (β × (K →+* ℂ)) = q * h
x : β × (K →+* ℂ) → ℤ
hxl : x ≠ 0
hmulvec0 : asiegel K a *ᵥ x = 0
hxbound : ‖x‖ ≤ (↑q * ↑h * ‖asiegel K a‖) ^ (↑p / (↑q - ↑p))
Apos : 0 ≤ A
⊢ ∃ ξ, ξ ≠ 0 ∧ a *ᵥ ξ = 0 ∧ ∀ (l : β), house ↑(ξ l) ≤ c₁ K * (c₁ K * ↑q * A) ^ (↑p / (↑q - ↑p))

Tactic:
use ξ K x, ξ_ne_0 K x hxl, ξ_mulVec_eq_0 K a x hxl hmulvec0,
    house_le_bound K a hpq x habs Apos hxbound

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

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : Module ℤ_[p] E
inst✝² : IsBoundedSMul ℤ_[p] E
inst✝¹ : IsUltrametricDist E
inst✝ : CompleteSpace E
a : ℕ → E
ha : Tendsto a atTop (𝓝 0)
n : ℕ
⊢ Δ_[1]^[n] (fun k ↦ ∑ j ∈ range (n + 1), k.choose j • a j) 0 =
    ∑ j ∈ range (n + 1), Δ_[1]^[n] (fun k ↦ k.choose j • a j) 0

Tactic:
by
    simp only [fwdDiff_iter_eq_sum_shift, smul_sum]
    rw [sum_comm]

Goal state after:
Module: Mathlib.Topology.Separation.DisjointCover

Goal state before:
pp: ι : Type u_1
X : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TotallyDisconnectedSpace X
inst✝¹ : T2Space X
inst✝ : CompactSpace X
U : ι → Opens X
hU : IsOpenCover U
⊢ ∃ n W, (∀ (j : Fin n), W j ≠ ⊥ ∧ ∃ i, ↑(W j) ⊆ ↑(U i)) ∧ univ ⊆ ⋃ j, ↑(W j) ∧ Pairwise (Disjoint on W)

Tactic:
classical
  obtain ⟨n, V, hVle, hVun⟩ := hU.exists_finite_clopen_cover
  obtain ⟨W, hWle, hWun, hWd⟩ := Fintype.exists_disjointed_le V
  simp only [← SetLike.coe_set_eq, Clopens.coe_finset_sup, Finset.mem_univ, iUnion_true] at hWun
  let t : Finset (Fin n) := {j | W j ≠ ⊥}
  refine ⟨#t, fun k ↦ W (t.equivFin.symm k), fun k ↦ ⟨?_, ?_⟩, fun x hx ↦ ?_, ?_⟩
  · exact (Finset.mem_filter.mp (t.equivFin.symm k).2).2
  · exact match hVle (t.equivFin.symm k) with | ⟨i, hi⟩ => ⟨i, subset_trans (hWle _) hi⟩
  · obtain ⟨j, hj⟩ := mem_iUnion.mp <| (hWun ▸ hVun) hx
    have : W j ≠ ⊥ := by simpa [← SetLike.coe_ne_coe, ← Set.nonempty_iff_ne_empty] using ⟨x, hj⟩
    exact mem_iUnion.mpr ⟨t.equivFin ⟨j, Finset.mem_filter.mpr ⟨Finset.mem_univ _, this⟩⟩, by simpa⟩
  · exact hWd.comp_of_injective <| Subtype.val_injective.comp t.equivFin.symm.injective

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

Goal state before:
pp: case refine_1
R : Type u_2
inst✝⁴ : CommRing R
inst✝³ : Algebra R ℚ
inst✝² : IsIntegralClosure R ℤ ℚ
inst✝¹ : IsDedekindDomain R
inst✝ : IsFractionRing R ℚ
v : HeightOneSpectrum R
x : HeightOneSpectrum.adicCompletion ℚ v
hx : x ∈ ↑(HeightOneSpectrum.adicCompletionIntegers ℚ v)
⊢ (padicEquiv v) x ∈ ↑(subring ↑(primesEquiv v))

pp: case refine_2
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))
⊢ y ∈ ⇑(padicEquiv v) '' ↑(HeightOneSpectrum.adicCompletionIntegers ℚ v)

Tactic:
· rw [← adicCompletionIntegers.coe_padicIntEquiv_apply v ⟨x, hx⟩]
    exact norm_le_one ((adicCompletionIntegers.padicIntEquiv v) ⟨x, hx⟩)

Goal state after:
case refine_2
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))
⊢ y ∈ ⇑(padicEquiv v) '' ↑(HeightOneSpectrum.adicCompletionIntegers ℚ v)
Module: Mathlib.Topology.UniformSpace.ProdApproximation

Goal state before:
pp: X : Type u_5
Y : Type u_6
R : Type u_7
inst✝⁸ : TopologicalSpace X
inst✝⁷ : TopologicalSpace Y
inst✝⁶ : CommRing R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : IsTopologicalRing R
inst✝³ : CompactSpace X
inst✝² : T2Space X
inst✝¹ : CompactSpace Y
inst✝ : TotallyDisconnectedSpace X
this✝ : UniformSpace R := IsTopologicalAddGroup.rightUniformSpace R
this : IsUniformAddGroup R := isUniformAddGroup_of_addCommGroup
f : C(X × Y, R)
⊢ ∀ (o : Set C(X × Y, R)), IsOpen o → f ∈ o → ∃ x, x ∈ o ∩ Set.range ⇑tensorHom

Tactic:
intro U hUo hUf

Goal state after:
X : Type u_5
Y : Type u_6
R : Type u_7
inst✝⁸ : TopologicalSpace X
inst✝⁷ : TopologicalSpace Y
inst✝⁶ : CommRing R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : IsTopologicalRing R
inst✝³ : CompactSpace X
inst✝² : T2Space X
inst✝¹ : CompactSpace Y
inst✝ : TotallyDisconnectedSpace X
this✝ : UniformSpace R := IsTopologicalAddGroup.rightUniformSpace R
this : IsUniformAddGroup R := isUniformAddGroup_of_addCommGroup
f : C(X × Y, R)
U : Set C(X × Y, R)
hUo : IsOpen U
hUf : f ∈ U
⊢ ∃ x, x ∈ U ∩ Set.range ⇑tensorHom
Module: Mathlib.NumberTheory.PowModTotient

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

Tactic:
by
  induction l with
  | zero => simp
  | succ l ih =>
    rw [add_mul, one_mul, ← add_assoc, pow_add_totient_mod_eq hn h, ih]

Goal state after:
Module: Mathlib.NumberTheory.PrimesCongruentOne

Goal state before:
pp: case inr.refine_2
k n : ℕ
hk0 : k ≠ 0
hk1 : 1 < k
b : ℕ := k * n !
hgt : 1 < (eval (↑b) (cyclotomic k ℤ)).natAbs
p : ℕ := (eval (↑b) (cyclotomic k ℤ)).natAbs.minFac
hprime : Fact (Prime p)
hroot : (cyclotomic k (ZMod p)).IsRoot ((castRingHom (ZMod p)) b)
hpb : ¬p ∣ b
hdiv : orderOf ↑b ∣ p - 1
⊢ p ≡ 1 [MOD k]

Tactic:
have : NeZero (k : ZMod p) :=
      NeZero.of_not_dvd (ZMod p) fun hpk => hpb (dvd_mul_of_dvd_left hpk _)

Goal state after:
case inr.refine_2
k n : ℕ
hk0 : k ≠ 0
hk1 : 1 < k
b : ℕ := k * n !
hgt : 1 < (eval (↑b) (cyclotomic k ℤ)).natAbs
p : ℕ := (eval (↑b) (cyclotomic k ℤ)).natAbs.minFac
hprime : Fact (Prime p)
hroot : (cyclotomic k (ZMod p)).IsRoot ((castRingHom (ZMod p)) b)
hpb : ¬p ∣ b
hdiv : orderOf ↑b ∣ p - 1
this : NeZero ↑k
⊢ p ≡ 1 [MOD k]
Module: Mathlib.NumberTheory.Pell

Goal state before:
pp: d : ℤ
a₁ : Solution₁ d
h : IsFundamental a₁
a : Solution₁ d
hax : 1 < a.x
hay : 0 < a.y
⊢ a.x * a₁.x < d * (a.y * a₁.y) + a.x

Tactic:
refine lt_of_mul_lt_mul_left ?_ h.2.1.le

Goal state after:
d : ℤ
a₁ : Solution₁ d
h : IsFundamental a₁
a : Solution₁ d
hax : 1 < a.x
hay : 0 < a.y
⊢ a₁.y * (a.x * a₁.x) < a₁.y * (d * (a.y * a₁.y) + a.x)
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
k : ℕ
_h : 0 < k + 2
⊢ ‖newton_seq (k + 2) - newton_seq (k + 1)‖ < ‖newton_seq (k + 1) - a‖

Tactic:
newton_seq_dist_to_a (k + 1) (succ_pos _)

Goal state after:
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
k : ℕ
_h : 0 < k + 2
⊢ ‖newton_seq (k + 2) - newton_seq (k + 1)‖ <
    ‖(Polynomial.aeval a) F‖ / ‖(Polynomial.aeval a) (Polynomial.derivative F)‖
Module: Mathlib.NumberTheory.Rayleigh

Goal state before:
pp: case pos
r s : ℝ
hrs : r.HolderConjugate s
j : ℤ
h₁ : j ∉ {x | ∃ k, beattySeq r k = x}
h₂ : j ∈ {x | ∃ k, beattySeq' s k = x}
⊢ j ∈ {x | ∃ k, beattySeq r k = x}ᶜ ↔ j ∈ {x | ∃ k, beattySeq' s k = x}

pp: case neg
r s : ℝ
hrs : r.HolderConjugate s
j : ℤ
h₁ : j ∉ {x | ∃ k, beattySeq r k = x}
h₂ : j ∉ {x | ∃ k, beattySeq' s k = x}
⊢ j ∈ {x | ∃ k, beattySeq r k = x}ᶜ ↔ j ∈ {x | ∃ k, beattySeq' s k = x}

Tactic:
· simp only [Set.mem_compl_iff, h₁, h₂, not_false_eq_true]

Goal state after:
case neg
r s : ℝ
hrs : r.HolderConjugate s
j : ℤ
h₁ : j ∉ {x | ∃ k, beattySeq r k = x}
h₂ : j ∉ {x | ∃ k, beattySeq' s k = x}
⊢ j ∈ {x | ∃ k, beattySeq r k = x}ᶜ ↔ j ∈ {x | ∃ k, beattySeq' s k = x}
Module: Mathlib.NumberTheory.SelbergSieve

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

Tactic:
apply _root_.ne_of_gt
  exact nu_pos_of_dvd_prodPrimes hd

Goal state after:
Module: Mathlib.NumberTheory.SelbergSieve

Goal state before:
pp: case caseB
s : BoundingSieve
w : ℕ → ℝ
⊢ (∑ d1 ∈ s.prodPrimes.divisors,
      ∑ d2 ∈ s.prodPrimes.divisors,
        ∑ l ∈ s.prodPrimes.divisors,
          if l ∣ d1.gcd d2 then (selbergTerms l)⁻¹ * (s.nu d1 * w d1) * (s.nu d2 * w d2) else 0) =
    ∑ l ∈ s.prodPrimes.divisors,
      ∑ d1 ∈ s.prodPrimes.divisors,
        ∑ d2 ∈ s.prodPrimes.divisors,
          if l ∣ d1.gcd d2 then (selbergTerms l)⁻¹ * (s.nu d1 * w d1) * (s.nu d2 * w d2) else 0

pp: case caseC
s : BoundingSieve
w : ℕ → ℝ
⊢ (∑ l ∈ s.prodPrimes.divisors,
      ∑ d1 ∈ s.prodPrimes.divisors,
        ∑ d2 ∈ s.prodPrimes.divisors,
          if l ∣ d1.gcd d2 then (selbergTerms l)⁻¹ * (s.nu d1 * w d1) * (s.nu d2 * w d2) else 0) =
    ∑ l ∈ s.prodPrimes.divisors,
      (selbergTerms l)⁻¹ * (∑ d ∈ s.prodPrimes.divisors, if l ∣ d then s.nu d * w d else 0) ^ 2

Tactic:
case caseB =>
    rw [eq_comm, sum_comm, sum_congr rfl fun _ _ ↦ sum_comm]

Goal state after:
case caseC
s : BoundingSieve
w : ℕ → ℝ
⊢ (∑ l ∈ s.prodPrimes.divisors,
      ∑ d1 ∈ s.prodPrimes.divisors,
        ∑ d2 ∈ s.prodPrimes.divisors,
          if l ∣ d1.gcd d2 then (selbergTerms l)⁻¹ * (s.nu d1 * w d1) * (s.nu d2 * w d2) else 0) =
    ∑ l ∈ s.prodPrimes.divisors,
      (selbergTerms l)⁻¹ * (∑ d ∈ s.prodPrimes.divisors, if l ∣ d then s.nu d * w d else 0) ^ 2
Module: Mathlib.NumberTheory.Zsqrtd.QuadraticReciprocity

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
hp3 : p % 4 = 3
hpi : ¬Irreducible ↑p
a b : ℕ
hab : a ^ 2 + b ^ 2 = p
⊢ ∀ (a b : ZMod 4), a ^ 2 + b ^ 2 ≠ ↑p

Tactic:
by
        rw [← ZMod.natCast_mod p 4, hp3]; decide

Goal state after:
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
p : Ideal R
P✝ : Ideal S
inst✝² : IsDedekindDomain S
inst✝¹ : Module.Finite R S
inst✝ : p.IsMaximal
P : ↥(factors (map f p)).toFinset
⊢ FiniteDimensional (R ⧸ p) (S ⧸ ↑P ^ p.ramificationIdx' ↑P)

Tactic:
refine .of_finrank_pos ?_

Goal state after:
R : Type u
inst✝⁵ : CommRing R
S : Type v
inst✝⁴ : CommRing S
inst✝³ : Algebra R S
p : Ideal R
P✝ : Ideal S
inst✝² : IsDedekindDomain S
inst✝¹ : Module.Finite R S
inst✝ : p.IsMaximal
P : ↥(factors (map f p)).toFinset
⊢ 0 < finrank (R ⧸ p) (S ⧸ ↑P ^ p.ramificationIdx' ↑P)
Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith

Goal state before:
pp: p x : ℝ
h : LiouvilleWith p x
hp : 1 < p
m : ℤ
⊢ x ≠ ↑m

Tactic:
by
  rintro rfl; rename' m => M
  rcases ((eventually_gt_atTop 0).and_frequently (h.frequently_lt_rpow_neg hp)).exists with
    ⟨n : ℕ, hn : 0 < n, m : ℤ, hne : (M : ℝ) ≠ m / n, hlt : |(M - m / n : ℝ)| < n ^ (-1 : ℝ)⟩
  refine hlt.not_ge ?_
  have hn' : (0 : ℝ) < n := by simpa
  rw [rpow_neg_one, ← one_div, sub_div' hn'.ne', abs_div, Nat.abs_cast]
  gcongr
  norm_cast
  rw [← zero_add (1 : ℤ), Int.add_one_le_iff, abs_pos, sub_ne_zero]
  rw [Ne, eq_div_iff hn'.ne'] at hne
  exact mod_cast hne

Goal state after:
Module: Mathlib.Order.Comparable

Goal state before:
pp: α : Type u_1
r : α → α → Prop
⊢ IncompRel rᶜ = AntisymmRel r

Tactic:
by
  simp [← antisymmRel_compl, compl]

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

Goal state before:
pp: ι α β : Type u
c : Cardinal.{u}
l✝ : Filter α
inst✝ : CardinalInterFilter l✝ c
l : Set (Set α)
hc : 2 < c
hl : ∀ (S : Set (Set α)), #↑S < c → S ⊆ l → ⋂₀ S ∈ l
h_mono : ∀ (s t : Set α), s ∈ l → s ⊆ t → t ∈ l
s t : Set α
hs : s ∈ l
ht : t ∈ l
⊢ ⋂₀ {s, t} ∈ l

Tactic:
apply hl _ (?_) (insert_subset_iff.2 ⟨hs, singleton_subset_iff.2 ht⟩)
    have : #({s, t} : Set (Set α)) ≤ 2 := by
      calc
      _ ≤ #({t} : Set (Set α)) + 1 := Cardinal.mk_insert_le
      _ = 2 := by norm_num
    exact lt_of_le_of_lt this hc

Goal state after:
Module: Mathlib.Order.Fin.InsertNth

Goal state before:
pp: case inr.inl
n : ℕ
α : Type u_1
inst✝ : Preorder α
f : Fin (n + 1) → α
hf : Monotone f
i : Fin n
x : α
hx₁ : f i.castSucc ≤ x
hx₂ : x ≤ f i.succ
⊢ i.castSucc.succ.insertNth x f (i.castSucc.succ.succAbove i.castSucc) ≤ i.castSucc.succ.insertNth x f i.castSucc.succ

Tactic:
insertNth_apply_succAbove,

Goal state after:
case inr.inl
n : ℕ
α : Type u_1
inst✝ : Preorder α
f : Fin (n + 1) → α
hf : Monotone f
i : Fin n
x : α
hx₁ : f i.castSucc ≤ x
hx₂ : x ≤ f i.succ
⊢ f i.castSucc ≤ i.castSucc.succ.insertNth x f i.castSucc.succ
Module: Mathlib.Order.Height

Goal state before:
pp: α : Type u_1
s : Set α
r : α → α → Prop
h : s.chainHeight r ≠ ⊤
⊢ ∃ t ⊆ s, t.encard = s.chainHeight r ∧ IsChain r t

Tactic:
have : Nonempty { t // t ⊆ s ∧ IsChain r t } := ⟨∅, by simp⟩
  obtain ⟨t, ht⟩ := exists_eq_iSup_of_lt_top (by rwa [← chainHeight_eq_iSup, lt_top_iff_ne_top])
  exact ⟨t.1, t.2.1, ht, t.2.2⟩

Goal state after:
Module: Mathlib.Order.Fin.InsertNth

Goal state before:
pp: case inr.inl
n : ℕ
α : Type u_1
inst✝ : Preorder α
f : Fin (n + 1) → α
hf : ∀ (i : Fin n), f i.castSucc < f i.succ
i : Fin n
x : α
hx₁ : f i.castSucc < x
hx₂ : x < f i.succ
⊢ i.castSucc.succ.insertNth x f (i.castSucc.succ.succAbove i.castSucc) < i.castSucc.succ.insertNth x f i.castSucc.succ

Tactic:
insertNth_apply_succAbove,

Goal state after:
case inr.inl
n : ℕ
α : Type u_1
inst✝ : Preorder α
f : Fin (n + 1) → α
hf : ∀ (i : Fin n), f i.castSucc < f i.succ
i : Fin n
x : α
hx₁ : f i.castSucc < x
hx₂ : x < f i.succ
⊢ f i.castSucc < i.castSucc.succ.insertNth x f i.castSucc.succ
Module: Mathlib.Order.Heyting.Regular

Goal state before:
pp: α : Type u_1
inst✝ : HeytingAlgebra α
a✝ b✝ : α
a b c : Regular α
⊢ (↑a ⊔ ↑b)ᶜᶜ ⊓ (↑a ⊔ ↑c)ᶜᶜ ≤ (↑a ⊔ ↑b ⊓ ↑c)ᶜᶜ

Tactic:
rw [sup_inf_left, compl_compl_inf_distrib]

Goal state after:
Module: Mathlib.Order.PrimeIdeal

Goal state before:
pp: P : Type u_1
inst✝ : BooleanAlgebra P
x : P
I : Ideal P
hI : I.IsPrime
⊢ x ∈ I ∨ xᶜ ∈ I

Tactic:
by
  apply hI.mem_or_mem
  rw [inf_compl_eq_bot]
  exact I.bot_mem

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
n : Nucleus X
s : Set X
⊢ rangeFactorization (⇑n) (sSup s) = sSup (rangeFactorization ⇑n '' s)

Tactic:
rw [n.giAux.gc.l_sSup, sSup_image]

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

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

Tactic:
obtain (hx | hx) := em (x ∈ u)
  · exact hf.apply_eq_apply (hg.rel_apply hx).symm
  rw [hg.apply_of_notMem hx, hf.apply_of_notMem hx]

Goal state after:
Module: Mathlib.Order.Types.Defs

Goal state before:
pp: α β : Type u
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
h : lift.{u_1, u} (type α) = lift.{u_1, u} (type β)
⊢ Nonempty (α ≃o β)

Tactic:
rw [← type_ulift, ← type_ulift, type_eq_type] at h

Goal state after:
α β : Type u
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
h : Nonempty (ULift α ≃o ULift β)
⊢ Nonempty (α ≃o β)
Module: Mathlib.Order.Sublocale

Goal state before:
pp: X : Type u_1
inst✝ : Order.Frame X
ι : Sort u_2
S✝ T : Sublocale X
s : Set X
f : ι → X
a b : X
S : Sublocale X
x✝ : X
⊢ ↑(S.restrict ↑(S.restrict x✝)) ≤ ↑(S.restrict x✝)

Tactic:
S.giRestrict.gc.l_u_l_eq_l

Goal state after:
X : Type u_1
inst✝ : Order.Frame X
ι : Sort u_2
S✝ T : Sublocale X
s : Set X
f : ι → X
a b : X
S : Sublocale X
x✝ : X
⊢ ↑(S.restrict x✝) ≤ ↑(S.restrict x✝)
Module: Mathlib.Probability.Process.Predictable

Goal state before:
pp: case inr
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst✝¹ : LinearOrder ι
inst✝ : OrderBot ι
𝓕 : Filtration ι m
i j : ι
s : Set Ω
hs : MeasurableSet s
hij : i ≤ j
⊢ MeasurableSet (Set.Ioi i ×ˢ s \ Set.Ioi j ×ˢ s)

Tactic:
exact (measurableSet_predictable_Ioi_prod hs).diff
      (measurableSet_predictable_Ioi_prod <| 𝓕.mono hij _ hs)

Goal state after:
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
⊢ IsStronglyProgressive 𝓕 u

Tactic:
by
  intro i
  let : MeasurableSpace (ι × Ω) := 𝓕.predictable
  let : MeasurableSpace (Set.Iic i × Ω) := Subtype.instMeasurableSpace.prod (𝓕 i)
  let X m (x : Set.Iic i × Ω) := h𝓕.approx m ⟨x.1, x.2⟩
  refine ⟨fun m ↦ SimpleFunc.mk (X m) ?_ ?_, ?_⟩
  · exact fun e ↦ measurable_inclusion_predictable <| (h𝓕.approx m).measurableSet_fiber e
  · exact Set.Finite.subset (h𝓕.approx m).finite_range (by grind)
  · exact fun n ↦ by apply h𝓕.tendsto_approx

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 g : ι → Ω → E
ℱ : Filtration ι m0
inst✝ : CompleteSpace E
hf : Martingale f ℱ μ
hg : StronglyAdapted ℱ g
h_eq : ∀ (t : ι), f t =ᵐ[μ] g t
i j : ι
hij : i ≤ j
⊢ μ[g j | ↑ℱ i] =ᵐ[μ] g i

Tactic:
calc μ[g j | ℱ i] =ᵐ[μ] μ[f j | ℱ i] := (condExp_congr_ae (h_eq j)).symm
    _ =ᵐ[μ] g i := (hf.2 i j hij).trans (h_eq i)

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

Goal state before:
pp: Ω : Type u_1
ι : Type u_3
inst✝¹ : Preorder ι
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ι m0
inst✝ : SigmaFiniteFiltration μ ℱ
f : ι → Ω → ℝ
hadp : StronglyAdapted ℱ f
hint : ∀ (i : ι), Integrable (f i) μ
i j : ι
hij : i ≤ j
s : Set Ω
hf : ∫ (ω : Ω) in s, f i ω ∂μ ≤ ∫ (ω : Ω) in s, f j ω ∂μ
hs : MeasurableSet s
x✝ : (μ.trim ⋯) s < ∞
⊢ 0 ≤ ∫ (x : Ω) in s, (μ[f j | ↑ℱ i] - f i) x ∂μ.trim ⋯

Tactic:
rwa [← setIntegral_trim _ (stronglyMeasurable_condExp.sub <| hadp i) hs,
    integral_sub' integrable_condExp.integrableOn (hint i).integrableOn, sub_nonneg,
    setIntegral_condExp (ℱ.le i) (hint j) hs]

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

Goal state before:
pp: Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
inst✝ : IsFiniteMeasure μ
f : ℕ → Ω → ℝ
hadp : StronglyAdapted 𝒢 f
hint : ∀ (i : ℕ), Integrable (f i) μ
hf : ∀ (i : ℕ) (s : Set Ω), MeasurableSet s → ∫ (ω : Ω) in s, f i ω ∂μ ≤ ∫ (ω : Ω) in s, f (i + 1) ω ∂μ
⊢ Submartingale f 𝒢 μ

Tactic:
refine submartingale_of_setIntegral_le hadp hint fun i j hij s hs => ?_

Goal state after:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
inst✝ : IsFiniteMeasure μ
f : ℕ → Ω → ℝ
hadp : StronglyAdapted 𝒢 f
hint : ∀ (i : ℕ), Integrable (f i) μ
hf : ∀ (i : ℕ) (s : Set Ω), MeasurableSet s → ∫ (ω : Ω) in s, f i ω ∂μ ≤ ∫ (ω : Ω) in s, f (i + 1) ω ∂μ
i j : ℕ
hij : i ≤ j
s : Set Ω
hs : MeasurableSet s
⊢ ∫ (ω : Ω) in s, f i ω ∂μ ≤ ∫ (ω : Ω) in s, f j ω ∂μ
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
inst✝ : CompleteSpace E
R : ℝ
f : ℕ → Ω → E
ℱ : Filtration ℕ m0
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), ‖f (i + 1) ω - f i ω‖ ≤ R
⊢ ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), ‖martingalePart f ℱ μ (i + 1) ω - martingalePart f ℱ μ i ω‖ ≤ 2 * R

Tactic:
filter_upwards [hbdd, predictablePart_bdd_difference ℱ hbdd] with ω hω₁ hω₂ i

Goal state after:
Ω : Type u_1
E : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
R : ℝ
f : ℕ → Ω → E
ℱ : Filtration ℕ m0
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), ‖f (i + 1) ω - f i ω‖ ≤ R
ω : Ω
hω₁ : ∀ (i : ℕ), ‖f (i + 1) ω - f i ω‖ ≤ R
hω₂ : ∀ (i : ℕ), ‖predictablePart f ℱ μ (i + 1) ω - predictablePart f ℱ μ i ω‖ ≤ R
i : ℕ
⊢ ‖martingalePart f ℱ μ (i + 1) ω - martingalePart f ℱ μ i ω‖ ≤ 2 * R
Module: Mathlib.Probability.Martingale.Upcrossing

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

Tactic:
rw [upperCrossingTime_succ]

Goal state after:
Ω : Type u_1
ι : Type u_2
inst✝ : ConditionallyCompleteLinearOrderBot ι
a b : ℝ
f : ι → Ω → ℝ
N : ι
n : ℕ
ω : Ω
⊢ lowerCrossingTime a b f N n ω ≤
    hittingBtwn f (Set.Ici b) (lowerCrossingTimeAux a f (upperCrossingTime a b f N n ω) N ω) N ω
Module: Mathlib.Probability.Martingale.Upcrossing

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

Tactic:
rw [upperCrossingTime_succ]
  exact le_hittingBtwn lowerCrossingTime_le ω

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

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

Tactic:
refine lt_of_le_of_ne upperCrossingTime_le_lowerCrossingTime fun h =>
    not_le.2 hab <| le_trans ?_ (stoppedValue_lowerCrossingTime hn)
  simp only [stoppedValue]
  rw [← h]
  exact stoppedValue_upperCrossingTime (h.symm ▸ hn)

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

Goal state before:
pp: Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n i : ι
ω : Ω
h' : hittingAfter u s n ω < ↑i
h_top : ¬∀ (j : ι), n ≤ j → u j ω ∉ s
⊢ ∃ j, n ≤ j ∧ u j ω ∈ s

Tactic:
push Not at h_top

Goal state after:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
n i : ι
ω : Ω
h' : hittingAfter u s n ω < ↑i
h_top : ∃ j, n ≤ j ∧ u j ω ∈ s
⊢ ∃ j, n ≤ j ∧ u j ω ∈ s
Module: Mathlib.Probability.Process.Stopping

Goal state before:
pp: case refine_2
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝³ : ConditionallyCompleteLinearOrder ι
inst✝² : TopologicalSpace ι
inst✝¹ : OrderTopology ι
inst✝ : FirstCountableTopology ι
f : Filtration ι m
τ : Ω → WithTop ι
hf : f.IsRightContinuous
hτ1 : ∀ (i : ι), MeasurableSet {ω | τ ω < ↑i}
hτ2 : ∀ (i : ι), 𝓝[>] i = ⊥ → MeasurableSet {ω | τ ω = ↑i}
t : ι
ht : ¬𝓝[>] t = ⊥
this : (𝓝[>] t).NeBot
s : ℕ → ι
hs_gt : ∀ (n : ℕ), t < s n
hs_tendsto : Tendsto s atTop (𝓝 t)
h_exists_lt : ∀ (u : ι), t < u → ∃ i, s i < u
h_exists_lt' : ∀ (u : WithTop ι), ↑t < u → ∃ i, ↑(s i) < u
h_eq_iInter : {ω | τ ω ≤ ↑t} = ⋂ m, {ω | τ ω < ↑(s m)}
⊢ ⨅ m_1, ↑f (s m_1) ≤ ⨅ j, ⨅ (_ : j > t), ↑f j

Tactic:
simp only [gt_iff_lt, le_iInf_iff]
      intro i hti
      obtain ⟨m, hm⟩ := h_exists_lt i hti
      exact (iInf_le _ m).trans (f.mono hm.le)

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

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

Tactic:
have h_le : ∀ ω, hittingBtwn u s n n' ω ≤ i := fun x => (hittingBtwn_le x).trans hi
    simp [h_le]

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

Goal state before:
pp: Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
hf : a ≤ f N ω
hab : a < b
hN : ¬N = 0
k : ℕ
⊢ {i ∈ Finset.range N | i ∈ Set.Ico (lowerCrossingTime a b f N k ω) (upperCrossingTime a b f N (k + 1) ω)} =
    Finset.Ico (lowerCrossingTime a b f N k ω) (upperCrossingTime a b f N (k + 1) ω)

Tactic:
· ext i
      simp only [Set.mem_Ico, Finset.mem_filter, Finset.mem_range, Finset.mem_Ico,
        and_iff_right_iff_imp, and_imp]
      exact fun _ h => lt_of_lt_of_le h upperCrossingTime_le

Goal state after: