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

Goal state before:
pp: p k : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
hK : IsCyclotomicExtension {p ^ (k + 1)} ℚ K
this : IsGalois ℚ K
⊢ 𝒑.ramificationIdxIn (𝓞 K) = p ^ k * (p - 1)

Tactic:
ramificationIdxIn_eq_ramificationIdx 𝒑 (span {hK.zeta_spec.toInteger - 1}) Gal(K/ℚ),

Goal state after:
p k : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
hK : IsCyclotomicExtension {p ^ (k + 1)} ℚ K
this : IsGalois ℚ K
⊢ (span {⋯.toInteger - 1}).ramificationIdx ℤ = p ^ k * (p - 1)
Module: Mathlib.NumberTheory.NumberField.ExistsRamified

Goal state before:
pp: K : Type u_1
𝒪 : Type u_2
inst✝⁴ : Field K
inst✝³ : NumberField K
inst✝² : CommRing 𝒪
inst✝¹ : Algebra 𝒪 K
inst✝ : IsIntegralClosure 𝒪 ℤ K
H : Module.finrank ℚ K ≠ 1
this✝ : 0 < Module.finrank ℚ K
this : 2 < |discr K|
⊢ (discr K).natAbs ≠ 1

Tactic:
by linarith

Goal state after:
Module: Mathlib.NumberTheory.NumberField.House

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
α : K
⊢ house α = ↑(univ.sup' ⋯ fun φ ↦ ‖φ α‖₊)

Tactic:
rw [house, ← coe_nnnorm, nnnorm_eq, ← sup'_eq_sup univ_nonempty]

Goal state after:
Module: Mathlib.NumberTheory.NumberField.House

Goal state before:
pp: case calc_1
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
α : K
σ : K →+* ℂ
σ' : K →ₐ[ℚ] ℂ := σ.toRatAlgHom
⊢ ‖(Algebra.norm ℚ) α‖ = ‖∏ τ, τ α‖

Tactic:
rw [← Algebra.norm_eq_prod_embeddings, ← Rat.norm_cast_real,
      Real.norm_eq_abs, eq_ratCast, Complex.norm_ratCast]

Goal state after:
Module: Mathlib.NumberTheory.NumberField.Ideal.Asymptotics

Goal state before:
pp: case convert_3
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
C : ClassGroup (𝓞 K)
h₁ :
  ∀ (s : ℝ),
    {x | x ∈ ⇑(toMixed K) ⁻¹' fundamentalCone K ∧ mixedEmbedding.norm ((toMixed K) x) ≤ s} =
      ⇑(toMixed K) ⁻¹' {x | x ∈ fundamentalCone K ∧ mixedEmbedding.norm x ≤ s}
h₂ : {x | x ∈ fundamentalCone K ∧ mixedEmbedding.norm x ≤ 1} = normLeOne K
J : ↥(Ideal (𝓞 K))⁰
hJ : ClassGroup.mk0 J = C⁻¹
h₃ : ↑(absNorm ↑J) ≠ 0
⊢ MeasurableSet {x | x ∈ ⇑(toMixed K) ⁻¹' fundamentalCone K ∧ mixedEmbedding.norm ((toMixed K) x) ≤ 1}

Tactic:
exact (toMixed K).continuous.measurable (measurableSet_normLeOne K)

Goal state after:
Module: Mathlib.NumberTheory.SiegelsLemma

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : Fintype β
A : Matrix α β ℤ
hA : A ≠ 0
⊢ 1 ≤ ‖A‖

Tactic:
by_contra! h
  apply hA
  ext i j
  simp only [Matrix.zero_apply]
  rw [norm_lt_iff Real.zero_lt_one] at h
  specialize h i j
  rw [Int.norm_eq_abs] at h
  norm_cast at h
  exact Int.abs_lt_one_iff.1 h

Goal state after:
Module: Mathlib.NumberTheory.NumberField.House

Goal state before:
pp: case calc_4
K : Type u_1
inst✝⁴ : Field K
inst✝³ : NumberField K
α : Type u_2
β : Type u_3
a : Matrix α β (𝓞 K)
inst✝² : Fintype β
A : ℝ
habs : ∀ (k : α) (l : β), house ((algebraMap (𝓞 K) K) (a k l)) ≤ A
inst✝¹ : DecidableEq (K →+* ℂ)
inst✝ : Fintype α
Apos : 0 ≤ A
this : 0 ≤ c K
kr : α × (K →+* ℂ)
lu : β × (K →+* ℂ)
⊢ c K * (house ((algebraMap (𝓞 K) K) (a kr.1 lu.1)) * house ((algebraMap (𝓞 K) K) ((newBasis K) lu.2))) ≤
    c K * (A * house ((algebraMap (𝓞 K) K) ((newBasis K) lu.2)))

Tactic:
gcongr _ * (?_ * _)

Goal state after:
case ha
K : Type u_1
inst✝⁴ : Field K
inst✝³ : NumberField K
α : Type u_2
β : Type u_3
a : Matrix α β (𝓞 K)
inst✝² : Fintype β
A : ℝ
habs : ∀ (k : α) (l : β), house ((algebraMap (𝓞 K) K) (a k l)) ≤ A
inst✝¹ : DecidableEq (K →+* ℂ)
inst✝ : Fintype α
Apos : 0 ≤ A
this : 0 ≤ c K
kr : α × (K →+* ℂ)
lu : β × (K →+* ℂ)
⊢ 0 ≤ house ((algebraMap (𝓞 K) K) ((newBasis K) lu.2))

case hbc
K : Type u_1
inst✝⁴ : Field K
inst✝³ : NumberField K
α : Type u_2
β : Type u_3
a : Matrix α β (𝓞 K)
inst✝² : Fintype β
A : ℝ
habs : ∀ (k : α) (l : β), house ((algebraMap (𝓞 K) K) (a k l)) ≤ A
inst✝¹ : DecidableEq (K →+* ℂ)
inst✝ : Fintype α
Apos : 0 ≤ A
this : 0 ≤ c K
kr : α × (K →+* ℂ)
lu : β × (K →+* ℂ)
⊢ house ((algebraMap (𝓞 K) K) (a kr.1 lu.1)) ≤ A
Module: Mathlib.NumberTheory.Padics.MahlerBasis

Goal state before:
pp: case succ.refine_1
p : ℕ
hp : Fact (Nat.Prime p)
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : Module ℤ_[p] E
inst✝¹ : IsBoundedSMul ℤ_[p] E
inst✝ : IsUltrametricDist E
f : C(ℤ_[p], E)
s t : ℕ
hst : ∀ (x y : ℤ_[p]), ‖x - y‖ ≤ ↑p ^ (-↑t) → ‖f x - f y‖ ≤ ‖f‖ / ↑p ^ s
k : ℕ
IH : ∀ (n : ℕ), k ≤ s → ‖Δ_[1]^[n + k * p ^ t] (⇑f) 0‖ ≤ ‖f‖ / ↑p ^ k
n : ℕ
hk : k + 1 ≤ s
⊢ ↑((range (p ^ t - 1)).sup fun j ↦ ‖Δ_[1]^[n + k * p ^ t + (j + 1)] (⇑f) 0‖₊ / ↑p) ≤ ↑‖f‖₊ / ↑↑p ^ (k + 1)

Tactic:
← NNReal.coe_pow,

Goal state after:
case succ.refine_1
p : ℕ
hp : Fact (Nat.Prime p)
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : Module ℤ_[p] E
inst✝¹ : IsBoundedSMul ℤ_[p] E
inst✝ : IsUltrametricDist E
f : C(ℤ_[p], E)
s t : ℕ
hst : ∀ (x y : ℤ_[p]), ‖x - y‖ ≤ ↑p ^ (-↑t) → ‖f x - f y‖ ≤ ‖f‖ / ↑p ^ s
k : ℕ
IH : ∀ (n : ℕ), k ≤ s → ‖Δ_[1]^[n + k * p ^ t] (⇑f) 0‖ ≤ ‖f‖ / ↑p ^ k
n : ℕ
hk : k + 1 ≤ s
⊢ ↑((range (p ^ t - 1)).sup fun j ↦ ‖Δ_[1]^[n + k * p ^ t + (j + 1)] (⇑f) 0‖₊ / ↑p) ≤ ↑‖f‖₊ / ↑(↑p ^ (k + 1))
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
f : C(ℤ_[p], E)
ε : ℝ
hε : ε > 0
this : Tendsto (fun s ↦ ‖f‖ / ↑p ^ s) atTop (𝓝 0)
⊢ ∀ᶠ (x : ℕ) in atTop, ‖Δ_[1]^[x] (⇑f) 0‖ < ε

Tactic:
obtain ⟨s, hs⟩ := (this.eventually_lt_const hε).exists

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : Module ℤ_[p] E
inst✝¹ : IsBoundedSMul ℤ_[p] E
inst✝ : IsUltrametricDist E
f : C(ℤ_[p], E)
ε : ℝ
hε : ε > 0
this : Tendsto (fun s ↦ ‖f‖ / ↑p ^ s) atTop (𝓝 0)
s : ℕ
hs : ‖f‖ / ↑p ^ s < ε
⊢ ∀ᶠ (x : ℕ) in atTop, ‖Δ_[1]^[x] (⇑f) 0‖ < ε
Module: Mathlib.Topology.Separation.DisjointCover

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
S : Set (X × X)
inst✝ : CompactSpace X
hS : S ∈ 𝓝ˢ (diagonal X)
⊢ ∃ t U, IsOpenCover U ∧ ∀ (i : ↥t), ↑(U i) ×ˢ ↑(U i) ⊆ S

Tactic:
by
  choose U hUo hUx hUp using exists_open_prod_subset_of_mem_nhds_diagonal hS
  obtain ⟨t, ht⟩ := isCompact_univ.elim_finite_subcover _ hUo (fun x _ ↦ mem_iUnion.mpr ⟨_, hUx x⟩)
  refine ⟨t, fun i ↦ ⟨_, hUo i⟩, .of_sets _ ?_, (hUp ·)⟩
  simpa [iUnion_subtype, ← univ_subset_iff] using ht

Goal state after:
Module: Mathlib.NumberTheory.Pell

Goal state before:
pp: d : ℤ
h₀ : d ≠ 0
a : Solution₁ d
ha : a.x = 1
⊢ a = 1

Tactic:
have prop := a.prop_y
  rw [ha, one_pow, sub_self, mul_eq_zero, or_iff_right h₀, sq_eq_zero_iff] at prop
  exact ext ha prop

Goal state after:
Module: Mathlib.NumberTheory.Pell

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

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

Goal state after:
Module: Mathlib.NumberTheory.Rayleigh

Goal state before:
pp: r : ℝ
hr : Irrational r
x✝ k : ℤ
hk : k > 0
⊢ ↑⌊↑k * r⌋ < ↑k * r ∧ ↑k * r ≤ ↑⌊↑k * r⌋ + 1

Tactic:
refine ⟨(Int.floor_le _).lt_of_ne fun h ↦ ?_, (Int.lt_floor_add_one _).le⟩

Goal state after:
r : ℝ
hr : Irrational r
x✝ k : ℤ
hk : k > 0
h : ↑⌊↑k * r⌋ = ↑k * r
⊢ False
Module: Mathlib.NumberTheory.SumFourSquares

Goal state before:
pp: p : ℕ
hp : Prime p
this : Fact (Prime p)
natAbs_iff :
  ∀ {a b c d : ℤ} {k : ℕ},
    a.natAbs ^ 2 + b.natAbs ^ 2 + c.natAbs ^ 2 + d.natAbs ^ 2 = k ↔ a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = ↑k
⊢ ∃ m < p, 0 < m ∧ ∃ a b c d, a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = m * p

Tactic:
obtain ⟨a, b, k, hk₀, hkp, hk⟩ := exists_sq_add_sq_add_one_eq_mul p

Goal state after:
p : ℕ
hp : Prime p
this : Fact (Prime p)
natAbs_iff :
  ∀ {a b c d : ℤ} {k : ℕ},
    a.natAbs ^ 2 + b.natAbs ^ 2 + c.natAbs ^ 2 + d.natAbs ^ 2 = k ↔ a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = ↑k
a b k : ℕ
hk₀ : 0 < k
hkp : k < p
hk : a ^ 2 + b ^ 2 + 1 = k * p
⊢ ∃ m < p, 0 < m ∧ ∃ a b c d, a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = m * p
Module: Mathlib.NumberTheory.Zsqrtd.GaussianInt

Goal state before:
pp: x y : ℤ[i]
this : |2⁻¹| = 2⁻¹
⊢ |(toComplex x / toComplex y).re - ↑(round (toComplex x / toComplex y).re)| ≤ 2⁻¹

Tactic:
simpa using abs_sub_round (x / y : ℂ).re

Goal state after:
Module: Mathlib.NumberTheory.SumTwoSquares

Goal state before:
pp: p n : ℕ
hp : p ∈ n.primeFactors
hs : IsSquare (-1)
y : ZMod p
h : y ^ 2 = -1
⊢ p % 4 ≠ 3

Tactic:
show (-1 : ZMod p) = -1 ^ 2 by ring

Goal state after:
p n : ℕ
hp : p ∈ n.primeFactors
hs : IsSquare (-1)
y : ZMod p
h : y ^ 2 = -1 ^ 2
⊢ p % 4 ≠ 3
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)
⊢ Module.rank (R ⧸ p) (S ⧸ P) + (e - (j + 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:
← succ_nsmul',

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 + 1) + 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.LiouvilleNumber

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

Tactic:
by
  induction k with
  | zero => exact ⟨1, by rw [partialSum, range_one, sum_singleton, Nat.cast_one, Nat.factorial,
      pow_one, pow_one]⟩
  | succ k h =>
    rcases h with ⟨p_k, h_k⟩
    use p_k * m ^ ((k + 1)! - k !) + 1
    rw [partialSum_succ, h_k, div_add_div, div_eq_div_iff, add_mul]
    · norm_cast
      rw [add_mul, one_mul, Nat.factorial_succ, add_mul, one_mul, add_tsub_cancel_right, pow_add]
      simp [mul_assoc]
    all_goals positivity

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

Goal state before:
pp: x : ℝ
n : ℕ
hn : 0 < n
hn' : 0 < ↑n
this : x < ↑(⌊x * ↑n⌋ + 1) / ↑n
⊢ x * ↑n + 1 < x * ↑n + 2

Tactic:
by linarith

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

Goal state before:
pp: p x : ℝ
r : ℚ
hr : r ≠ 0
⊢ LiouvilleWith p (↑r * x) ↔ LiouvilleWith p x

Tactic:
by
  rw [mul_comm, mul_rat_iff hr]

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

Goal state before:
pp: p : ℝ
hp : p > 2
n : ℕ
hn : 2 + 1 / (↑n + 1) < p
x : ℝ
hxp : LiouvilleWith p x
hx01 : x ∈ Ico 0 1
b : ℕ
a : ℤ
hb : 1 ≤ ↑b
hb0 : 0 < ↑b
hlt : |x * ↑b - ↑a| / ↑b < 1 / ↑b
⊢ a ∈ Finset.Icc 0 ↑b

Tactic:
div_lt_div_iff_of_pos_right hb0,

Goal state after:
p : ℝ
hp : p > 2
n : ℕ
hn : 2 + 1 / (↑n + 1) < p
x : ℝ
hxp : LiouvilleWith p x
hx01 : x ∈ Ico 0 1
b : ℕ
a : ℤ
hb : 1 ≤ ↑b
hb0 : 0 < ↑b
hlt : |x * ↑b - ↑a| < 1
⊢ a ∈ Finset.Icc 0 ↑b
Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith

Goal state before:
pp: p : ℝ
hp : 1 < p
r : ℚ
h : LiouvilleWith p ↑r
⊢ False

Tactic:
rcases eq_or_ne r 0 with (rfl | h0)

Goal state after:
case inl
p : ℝ
hp : 1 < p
h : LiouvilleWith p ↑0
⊢ False

case inr
p : ℝ
hp : 1 < p
r : ℚ
h : LiouvilleWith p ↑r
h0 : r ≠ 0
⊢ False
Module: Mathlib.Order.CountableSupClosed

Goal state before:
pp: case refine_3
ι : 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
this : Nonempty ↑A
⊢ IsLUB (⋃ a, B ⋯) x

Tactic:
← isLUB_iUnion_iff_of_isLUB (u := fun a : A ↦ a.1) (fun a ↦ hB_lub a.2)

Goal state after:
case refine_3
ι : 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
this : Nonempty ↑A
⊢ IsLUB (Set.range fun a ↦ ↑a) x
Module: Mathlib.Order.Lattice.Congruence

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : Lattice α
inst✝² : Lattice β
inst✝¹ : FunLike F α β
inst✝ : LatticeHomClass F α β
f : F
w✝ x✝² y✝ z✝ : α
x✝¹ : (Setoid.ker ⇑f) w✝ x✝²
x✝ : (Setoid.ker ⇑f) y✝ z✝
⊢ (Setoid.ker ⇑f) (w✝ ⊔ y✝) (x✝² ⊔ z✝)

Tactic:
by simp_all +instances only [Setoid.ker, onFun, map_sup]

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

Goal state before:
pp: α : Type u_1
s✝ t✝¹ x y z : α
S✝ : Set α
S : Set (Set α)
u s t✝ : Set α
a b c : α
P✝ Q P : Partition u
x✝⁴ x✝³ x✝² : α
x✝¹ : P.Rel x✝⁴ x✝³
x✝ : P.Rel x✝³ x✝²
t : Set α
ht : t ∈ P
ha : x✝⁴ ∈ t
hb : x✝³ ∈ t
t' : Set α
ht' : t' ∈ P
hb' : x✝³ ∈ t'
hc : x✝² ∈ t'
⊢ x✝² ∈ t

Tactic:
by rwa [eq_of_mem_of_mem ht ht' hb hb']

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

Goal state before:
pp: α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
⊢ type (Lex (α × β)) = type β * type α

Tactic:
simp [HMul.hMul]

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 β
u : ι → Ω → β
γ : Type u_4
inst✝³ : MeasurableSpace ι
inst✝² : PseudoMetrizableSpace β
fltr : Filter γ
inst✝¹ : fltr.NeBot
inst✝ : fltr.IsCountablyGenerated
U : γ → ι → Ω → β
h : ∀ (l : γ), IsStronglyProgressive f (U l)
h_tendsto : Tendsto U fltr (𝓝 u)
i : ι
⊢ StronglyMeasurable fun p ↦ u (↑p.1) p.2

Tactic:
apply @stronglyMeasurable_of_tendsto (Set.Iic i × Ω) β γ
    (MeasurableSpace.prod _ (f i)) _ _ fltr _ _ _ _ fun l => h l i

Goal state after:
Ω : Type u_1
ι : Type u_2
m : MeasurableSpace Ω
inst✝⁵ : Preorder ι
f : Filtration ι m
β : Type u_3
inst✝⁴ : TopologicalSpace β
u : ι → Ω → β
γ : Type u_4
inst✝³ : MeasurableSpace ι
inst✝² : PseudoMetrizableSpace β
fltr : Filter γ
inst✝¹ : fltr.NeBot
inst✝ : fltr.IsCountablyGenerated
U : γ → ι → Ω → β
h : ∀ (l : γ), IsStronglyProgressive f (U l)
h_tendsto : Tendsto U fltr (𝓝 u)
i : ι
⊢ Tendsto (fun l p ↦ U l (↑p.1) p.2) fltr (𝓝 fun p ↦ u (↑p.1) p.2)
Module: Mathlib.Probability.Process.HittingTime

Goal state before:
pp: Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
ω : Ω
m : ι
hmn : m ≤ m
x✝ : ι
| (m ≤ x✝ ∧ x✝ ≤ m) ∧ u x✝ ω ∈ s → sInf ({m} ∩ {i | u i ω ∈ s}) = m

Tactic:
and_imp,

Goal state after:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
s : Set β
ω : Ω
m : ι
hmn : m ≤ m
x✝ : ι
| m ≤ x✝ ∧ x✝ ≤ m → u x✝ ω ∈ s → sInf ({m} ∩ {i | u i ω ∈ s}) = m
Module: Mathlib.Probability.Process.HittingTime

Goal state before:
pp: case pos
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
n m : ι
E F : Set β
hEF : E ⊆ F
ω : Ω
hF : ¬∃ j ∈ Set.Icc n m, u j ω ∈ F
hE : ∃ j ∈ Set.Icc n m, u j ω ∈ E
⊢ m ≤ sInf (Set.Icc n m ∩ {i | u i ω ∈ E})

pp: case neg
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
n m : ι
E F : Set β
hEF : E ⊆ F
ω : Ω
hF : ¬∃ j ∈ Set.Icc n m, u j ω ∈ F
hE : ¬∃ j ∈ Set.Icc n m, u j ω ∈ E
⊢ m ≤ m

Tactic:
· obtain ⟨t, ht⟩ := hE
    exact absurd ⟨t, ht.1, hEF ht.2⟩ hF

Goal state after:
case neg
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
n m : ι
E F : Set β
hEF : E ⊆ F
ω : Ω
hF : ¬∃ j ∈ Set.Icc n m, u j ω ∈ F
hE : ¬∃ j ∈ Set.Icc n m, u j ω ∈ E
⊢ m ≤ m
Module: Mathlib.Probability.Process.HittingTime

Goal state before:
pp: case pos
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
n : ι
E F : Set β
hEF : E ⊆ F
ω : Ω
hF : ¬∃ j, n ≤ j ∧ u j ω ∈ F
hE : ∃ j, n ≤ j ∧ u j ω ∈ E
⊢ ⊤ ≤ ↑(sInf {j | n ≤ j ∧ u j ω ∈ E})

pp: case neg
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
n : ι
E F : Set β
hEF : E ⊆ F
ω : Ω
hF : ¬∃ j, n ≤ j ∧ u j ω ∈ F
hE : ¬∃ j, n ≤ j ∧ u j ω ∈ E
⊢ ⊤ ≤ ⊤

Tactic:
· obtain ⟨t, ht⟩ := hE
    exact absurd ⟨t, ht.1, hEF ht.2⟩ hF

Goal state after:
case neg
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : ConditionallyCompleteLinearOrder ι
u : ι → Ω → β
n : ι
E F : Set β
hEF : E ⊆ F
ω : Ω
hF : ¬∃ j, n ≤ j ∧ u j ω ∈ F
hE : ¬∃ j, n ≤ j ∧ u j ω ∈ E
⊢ ⊤ ≤ ⊤
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
h₁ :
  ∀ (k : ℕ),
    ∑ n ∈ Finset.range N,
        (Set.Ico (lowerCrossingTime a b f N k ω) (upperCrossingTime a b f N (k + 1) ω)).indicator
          (fun m ↦ f (m + 1) ω - f m ω) n =
      stoppedValue f (fun ω ↦ ↑(upperCrossingTime a b f N (k + 1) ω)) ω -
        stoppedValue f (fun ω ↦ ↑(lowerCrossingTime a b f N k ω)) ω
⊢ ∑ _k ∈ Finset.range (upcrossingsBefore a b f N ω), (b - a) ≤
    ∑ k ∈ Finset.range (upcrossingsBefore a b f N ω),
      (stoppedValue f (fun ω ↦ ↑(upperCrossingTime a b f N (k + 1) ω)) ω -
        stoppedValue f (fun ω ↦ ↑(lowerCrossingTime a b f N k ω)) ω)

Tactic:
by
        gcongr ∑ k ∈ _, ?_ with i hi
        refine le_sub_of_le_upcrossingsBefore (zero_lt_iff.2 hN) hab ?_
        rwa [Finset.mem_range] at hi

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

Goal state before:
pp: case coe
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝⁵ : Add ι
inst✝⁴ : LinearOrder ι
inst✝³ : CanonicallyOrderedAdd ι
inst✝² : Countable ι
inst✝¹ : TopologicalSpace ι
inst✝ : OrderTopology ι
f : Filtration ι m
τ : Ω → WithTop ι
hτ : IsStoppingTime f τ
i j : ι
ω : Ω
a : ι
⊢ ↑a + ↑i ≤ ↑j ↔ ∃ i_1, ↑a = ↑↑i_1

Tactic:
simp; norm_cast

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

Goal state before:
pp: Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
τ : Ω → ℕ∞
inst✝ : SigmaFiniteFiltration μ 𝒢
h : Submartingale f 𝒢 μ
hτ : IsStoppingTime 𝒢 τ
⊢ ∀ (τ_1 π : Ω → ℕ∞),
    IsStoppingTime 𝒢 τ_1 →
      IsStoppingTime 𝒢 π →
        τ_1 ≤ π →
          (∃ N, ∀ (x : Ω), π x ≤ ↑N) →
            ∫ (x : Ω), stoppedValue (stoppedProcess f τ) τ_1 x ∂μ ≤ ∫ (x : Ω), stoppedValue (stoppedProcess f τ) π x ∂μ

Tactic:
intro σ π hσ hπ hσ_le_π hπ_bdd

Goal state after:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
τ : Ω → ℕ∞
inst✝ : SigmaFiniteFiltration μ 𝒢
h : Submartingale f 𝒢 μ
hτ : IsStoppingTime 𝒢 τ
σ π : Ω → ℕ∞
hσ : IsStoppingTime 𝒢 σ
hπ : IsStoppingTime 𝒢 π
hσ_le_π : σ ≤ π
hπ_bdd : ∃ N, ∀ (x : Ω), π x ≤ ↑N
⊢ ∫ (x : Ω), stoppedValue (stoppedProcess f τ) σ x ∂μ ≤ ∫ (x : Ω), stoppedValue (stoppedProcess f τ) π x ∂μ
Module: Mathlib.Probability.Martingale.BorelCantelli

Goal state before:
pp: Ω : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hf0 : f 0 = 0
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R
ht : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), ∃ c, Tendsto (fun n ↦ stoppedAbove f (↑i) n ω) atTop (𝓝 c)
ω : Ω
hω : ∀ (i : ℕ), ∃ c, Tendsto (fun n ↦ stoppedAbove f (↑i) n ω) atTop (𝓝 c)
hωb : (upperBounds (Set.range fun n ↦ f n ω)).Nonempty
i : ℕ
hi : hωb.some < ↑i
hib : ∀ (n : ℕ), f n ω < ↑i
⊢ ∃ c, Tendsto (fun n ↦ f n ω) atTop (𝓝 c)

Tactic:
have heq : ∀ n, stoppedAbove f i n ω = f n ω := by
    intro n
    rw [stoppedAbove, stoppedProcess, leastGE, hittingAfter_eq_top_iff.mpr]
    · simp only [le_top, inf_of_le_left]
      congr
    · simp [hib]

Goal state after:
Ω : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hf0 : f 0 = 0
hbdd : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), |f (i + 1) ω - f i ω| ≤ ↑R
ht : ∀ᵐ (ω : Ω) ∂μ, ∀ (i : ℕ), ∃ c, Tendsto (fun n ↦ stoppedAbove f (↑i) n ω) atTop (𝓝 c)
ω : Ω
hω : ∀ (i : ℕ), ∃ c, Tendsto (fun n ↦ stoppedAbove f (↑i) n ω) atTop (𝓝 c)
hωb : (upperBounds (Set.range fun n ↦ f n ω)).Nonempty
i : ℕ
hi : hωb.some < ↑i
hib : ∀ (n : ℕ), f n ω < ↑i
heq : ∀ (n : ℕ), stoppedAbove f (↑i) n ω = f n ω
⊢ ∃ c, Tendsto (fun n ↦ f n ω) atTop (𝓝 c)
Module: Mathlib.Probability.BorelCantelli

Goal state before:
pp: Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ι : Type u_2
β : Type u_3
inst✝² : LinearOrder ι
mβ : MeasurableSpace β
inst✝¹ : NormedAddCommGroup β
inst✝ : BorelSpace β
f : ι → Ω → β
i j : ι
hf : ∀ (i : ι), StronglyMeasurable (f i)
hfi : iIndepFun f μ
hij : i < j
this : Indep (⨆ k ∈ {j}, MeasurableSpace.comap (f k) mβ) (⨆ k ∈ {k | k ≤ i}, MeasurableSpace.comap (f k) mβ) μ
⊢ Indep (MeasurableSpace.comap (f j) mβ) (↑(Filtration.natural f hf) i) μ

Tactic:
iSup_singleton

Goal state after:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ι : Type u_2
β : Type u_3
inst✝² : LinearOrder ι
mβ : MeasurableSpace β
inst✝¹ : NormedAddCommGroup β
inst✝ : BorelSpace β
f : ι → Ω → β
i j : ι
hf : ∀ (i : ι), StronglyMeasurable (f i)
hfi : iIndepFun f μ
hij : i < j
this : Indep (MeasurableSpace.comap (f j) mβ) (⨆ k ∈ {k | k ≤ i}, MeasurableSpace.comap (f k) mβ) μ
⊢ Indep (MeasurableSpace.comap (f j) mβ) (↑(Filtration.natural f hf) i) μ
Module: Mathlib.Probability.Moments.Basic

Goal state before:
pp: Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
t : ℝ
inst✝ : IsFiniteMeasure μ
hμ : μ ≠ 0
c : ℝ
⊢ μ.real Set.univ ≠ 0

Tactic:
rw [Ne, measureReal_eq_zero_iff, Measure.measure_univ_eq_zero]
    simp only [hμ, not_false_iff]

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

Goal state before:
pp: Ω : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace Ω
inst✝¹⁰ : Nonempty ι
u : ι → Ω → β
τ : Ω → WithTop ι
inst✝⁹ : LinearOrder ι
inst✝⁸ : MeasurableSpace ι
inst✝⁷ : TopologicalSpace ι
inst✝⁶ : OrderTopology ι
inst✝⁵ : SecondCountableTopology ι
inst✝⁴ : BorelSpace ι
inst✝³ : TopologicalSpace β
f : Filtration ι m
inst✝² : PseudoMetrizableSpace β
inst✝¹ : MeasurableSpace β
inst✝ : BorelSpace β
hf_prog : IsStronglyProgressive f u
hτ : IsStoppingTime f τ
t : Set β
ht : MeasurableSet t
i : ι
h_str_meas : ∀ (i : ι), StronglyMeasurable (stoppedValue u fun ω ↦ min (τ ω) ↑i)
this : stoppedValue u τ ⁻¹' t ∩ {ω | τ ω ≤ ↑i} = (stoppedValue u fun ω ↦ min (τ ω) ↑i) ⁻¹' t ∩ {ω | τ ω ≤ ↑i}
⊢ MeasurableSet (stoppedValue u τ ⁻¹' t ∩ {ω | τ ω ≤ ↑i})

Tactic:
rw [this]; exact ((h_str_meas i).measurable ht).inter (hτ.measurableSet_le i)

Goal state after: