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

Goal state before:
pp: case refine_2
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
n i : ℕ
x✝ : i ∈ range (n + 1)
⊢ ‖((-1) ^ (n - i) * ↑(n.choose i)) • (f (↑i + ↑(p ^ t)) - f ↑i)‖ ≤ ‖f‖ / ↑p ^ s

Tactic:
calc ‖((-1 : ℤ) ^ (n - i) * n.choose i) • (f (i + ↑(p ^ t)) - f i)‖
    _ ≤ ‖((-1 : ℤ) ^ (n - i) * n.choose i : ℤ_[p])‖ * ‖(f (i + ↑(p ^ t)) - f i)‖ := by
      rw [← Int.cast_smul_eq_zsmul ℤ_[p]]
      exact (norm_smul_le ..).trans (by norm_cast)
    _ ≤ ‖f (i + ↑(p ^ t)) - f i‖ := by
      apply mul_le_of_le_one_left (norm_nonneg _)
      simpa only [← coe_intCast] using norm_le_one _
    _ ≤ ‖f‖ / p ^ s := by
      apply hst
      rw [Nat.cast_pow, add_sub_cancel_left, norm_pow, norm_p, inv_pow, zpow_neg, zpow_natCast]

Goal state after:
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)
U : Set C(X × Y, R)
hUo : IsOpen U
hUf : f ∈ U
this : {p | p.1 = f → p.2 ∈ U} ∈ 𝓤 C(X × Y, R)
J : Set (R × R)
hJu : J ∈ 𝓤 R
hJ' : {fg | ∀ (x : X × Y), (fg.1 x, fg.2 x) ∈ J} ⊆ {p | p.1 = f → p.2 ∈ U}
n : ℕ
g : Fin n → C(X, R)
h : Fin n → C(Y, R)
hgh : ∀ (x : X) (y : Y), (f (x, y), ∑ i, (g i) x * (h i) y) ∈ J
hG : (∀ (a : X) (b : Y), (f (a, b), (tensorHom (∑ i, g i ⊗ₜ[R] h i)) (a, b)) ∈ J) → tensorHom (∑ i, g i ⊗ₜ[R] h i) ∈ U
⊢ ∀ (a : X) (b : Y), (f (a, b), (tensorHom (∑ i, g i ⊗ₜ[R] h i)) (a, b)) ∈ J

Tactic:
by simpa [tensorHom] using hgh

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
⊢ Tendsto
    (fun n ↦
      ‖(Polynomial.aeval a) (Polynomial.derivative F)‖ * ‖(Polynomial.aeval a) (Polynomial.derivative F)‖ *
        T_gen p F a ^ 2 ^ n)
    atTop (𝓝 (‖(Polynomial.aeval a) (Polynomial.derivative F)‖ * 0))

Tactic:
simp only [mul_assoc]

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
⊢ Tendsto
    (fun n ↦
      ‖(Polynomial.aeval a) (Polynomial.derivative F)‖ *
        (‖(Polynomial.aeval a) (Polynomial.derivative F)‖ * T_gen p F a ^ 2 ^ n))
    atTop (𝓝 (‖(Polynomial.aeval a) (Polynomial.derivative F)‖ * 0))
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''
s : Finset ι
g : ι → K
eq : ∑ i ∈ s, g i • (⇑F ∘ b) i = 0
j' : ι
hj's : j' ∈ s
hj'g : ¬g j' = 0
a : K
j : ι
hjs : j ∈ s
hgI✝ : a * g j ∉ ↑(RingHom.ker f)
g'' : (i : ι) → i ∈ s → R
hg'' : ∀ (i : ι) (a_1 : i ∈ s), (algebraMap R K) (g'' i a_1) = a * g i
this : (a : Prop) → Decidable a := Classical.propDecidable
g' : ι → R := fun i ↦ if h : i ∈ s then g'' i h else 0
hg' : ∀ i ∈ s, (algebraMap R K) (g' i) = a * g i
hgI : f (g' j) ≠ 0
i : ι
hi : i ∈ s
⊢ F (g' i • b i) = a • g i • (⇑F ∘ b) i

Tactic:
rw [map_smul, ← IsScalarTower.algebraMap_smul K, hg' i hi, ← smul_assoc,
      smul_eq_mul, Function.comp_apply]

Goal state after:
Module: Mathlib.NumberTheory.SelbergSieve

Goal state before:
pp: s : BoundingSieve
⊢ ∀ n > 0,
    (n ∈ fun x ↦ ∃ c, s.prodPrimes = x * c) → ∑ x ∈ n.divisorsAntidiagonal, ↑(μ x.1) * (s.nu x.2)⁻¹ = (selbergTerms n)⁻¹

Tactic:
intro l

Goal state after:
s : BoundingSieve
l : ℕ
⊢ l > 0 →
    (l ∈ fun x ↦ ∃ c, s.prodPrimes = x * c) → ∑ x ∈ l.divisorsAntidiagonal, ↑(μ x.1) * (s.nu x.2)⁻¹ = (selbergTerms l)⁻¹
Module: Mathlib.NumberTheory.Zsqrtd.QuadraticReciprocity

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
hpi : Prime ↑p
hp1 : p % 2 = 1
hp3 : p % 4 ≠ 3
k : ℕ
k_lt_p : k < p
hk : -1 = ↑k * ↑k
⊢ ↑k * ↑k + ↑1 = 0

Tactic:
Nat.cast_one,

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
hpi : Prime ↑p
hp1 : p % 2 = 1
hp3 : p % 4 ≠ 3
k : ℕ
k_lt_p : k < p
hk : -1 = ↑k * ↑k
⊢ ↑k * ↑k + 1 = 0
Module: Mathlib.NumberTheory.SumFourSquares

Goal state before:
pp: case pos
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
hm : ∃ m < p, 0 < m ∧ ∃ a b c d, a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = m * p
a b c d m : ℕ
hmin : ∀ m_1 < 2 * m, ¬(m_1 < p ∧ 0 < m_1 ∧ ∃ a b c d, a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = m_1 * p)
hmp : 2 * m < p
hm₀ : 0 < m
hm₁ : 1 < 2 * m
this : NeZero (2 * m)
hm₂ : m < 2 * m
habcd : ↑(a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2) = ↑(2 * m * p)
⊢ False

Tactic:
push_cast [mul_assoc] at habcd

Goal state after:
case pos
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
hm : ∃ m < p, 0 < m ∧ ∃ a b c d, a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = m * p
a b c d m : ℕ
hmin : ∀ m_1 < 2 * m, ¬(m_1 < p ∧ 0 < m_1 ∧ ∃ a b c d, a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 = m_1 * p)
hmp : 2 * m < p
hm₀ : 0 < m
hm₁ : 1 < 2 * m
this : NeZero (2 * m)
hm₂ : m < 2 * m
habcd : ↑a ^ 2 + ↑b ^ 2 + ↑c ^ 2 + ↑d ^ 2 = 2 * (↑m * ↑p)
⊢ False
Module: Mathlib.NumberTheory.SumTwoSquares

Goal state before:
pp: case mpr
n a b : ℕ
h₁ : n = a ^ 2 * b
h₂ : IsSquare (-1)
⊢ ∃ x y, n = x ^ 2 + y ^ 2

Tactic:
obtain ⟨x', y', h⟩ := Nat.eq_sq_add_sq_of_isSquare_mod_neg_one h₂

Goal state after:
case mpr
n a b : ℕ
h₁ : n = a ^ 2 * b
h₂ : IsSquare (-1)
x' y' : ℕ
h : b = x' ^ 2 + y' ^ 2
⊢ ∃ x y, n = x ^ 2 + y ^ 2
Module: Mathlib.NumberTheory.SumTwoSquares

Goal state before:
pp: case inl
⊢ (∃ x y, 0 = x ^ 2 + y ^ 2) ↔ ∀ q ∈ primeFactors 0, q % 4 = 3 → Even (padicValNat q 0)

pp: case inr
n : ℕ
hn₀ : n > 0
⊢ (∃ x y, n = x ^ 2 + y ^ 2) ↔ ∀ q ∈ n.primeFactors, q % 4 = 3 → Even (padicValNat q n)

Tactic:
· exact ⟨fun _ q _ _ ↦ (padicValNat_zero_right _).symm ▸ Even.zero, fun _ ↦ ⟨0, 0, rfl⟩⟩

Goal state after:
case inr
n : ℕ
hn₀ : n > 0
⊢ (∃ x y, n = x ^ 2 + y ^ 2) ↔ ∀ q ∈ n.primeFactors, q % 4 = 3 → Even (padicValNat q n)
Module: Mathlib.NumberTheory.Transcendental.Lindemann.AnalyticalPart

Goal state before:
pp: case h₁
f : ℕ → ℂ[X]
s : ℂ
c' : ℝ
hc' : c' ≥ 0
h' : ∀ (p : ℕ), ‖P (f p) s‖ ≤ Real.exp s.re * (Real.exp ‖s‖ * c' ^ p * ‖s‖)
c₁ : ℝ := ⋯
c₂ : ℝ := ⋯
c₃ : ℝ := ⋯
p : ℕ
hp : p ≠ 0
le_max_one_pow : ∀ {x : ℝ}, x ≤ max x 1 ^ p
⊢ Real.exp s.re ≤ c₁ ^ p

Tactic:
exact le_max_one_pow

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

Goal state before:
pp: case hbc
f : ℕ → ℂ[X]
s : ℂ
c' : ℝ
hc' : c' ≥ 0
h' : ∀ (p : ℕ), ‖P (f p) s‖ ≤ Real.exp s.re * (Real.exp ‖s‖ * c' ^ p * ‖s‖)
c₁ : ℝ := ⋯
c₂ : ℝ := ⋯
c₃ : ℝ := ⋯
p : ℕ
hp : p ≠ 0
le_max_one_pow : ∀ {x : ℝ}, x ≤ max x 1 ^ p
⊢ Real.exp ‖s‖ ≤ c₂ ^ p

Tactic:
exact le_max_one_pow

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

Goal state before:
pp: case h₂
f : ℕ → ℂ[X]
s : ℂ
c' : ℝ
hc' : c' ≥ 0
h' : ∀ (p : ℕ), ‖P (f p) s‖ ≤ Real.exp s.re * (Real.exp ‖s‖ * c' ^ p * ‖s‖)
c₁ : ℝ := ⋯
c₂ : ℝ := ⋯
c₃ : ℝ := ⋯
p : ℕ
hp : p ≠ 0
le_max_one_pow : ∀ {x : ℝ}, x ≤ max x 1 ^ p
⊢ ‖s‖ ≤ c₃ ^ p

Tactic:
exact le_max_one_pow

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

Goal state before:
pp: case h.right.refine_1
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
⊢ p - 1 + p * f.natDegree - p ≤ p * f.natDegree - 1

Tactic:
tsub_add_eq_add_tsub prime_p.one_le,

Goal state after:
case h.right.refine_1
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
⊢ p + p * f.natDegree - 1 - p ≤ p * f.natDegree - 1
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✝¹ : p.IsMaximal
inst✝ : P.IsPrime
hP0 : P ≠ ⊥
he : e ≠ 0
this✝ : NeZero e := { out := he }
this : Module.rank (R ⧸ p) ↥⊤ = e • Module.rank (R ⧸ p) (S ⧸ P)
⊢ Module.rank (R ⧸ p) (S ⧸ P ^ e) = e • Module.rank (R ⧸ p) (S ⧸ P)

Tactic:
exact (rank_top (R ⧸ p) _).symm.trans this

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

Goal state before:
pp: m : ℕ
hm : 0 < m
⊢ 1 / ↑m ^ 0! = ↑1 / ↑(m ^ 0!)

Tactic:
Nat.cast_one,

Goal state after:
m : ℕ
hm : 0 < m
⊢ 1 / ↑m ^ 0! = 1 / ↑(m ^ 0!)
Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith

Goal state before:
pp: case refine_2
p x : ℝ
r : ℚ
h : LiouvilleWith p x
hr : r ≠ 0
C : ℝ
_hC₀ : 0 < C
hC : ∃ᶠ (n : ℕ) in atTop, 1 ≤ n ∧ ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < C / ↑n ^ p
n : ℕ
_hn : 1 ≤ n
m : ℤ
hne : x ≠ ↑m / ↑n
hlt : |x - ↑m / ↑n| < C / ↑n ^ p
A : ↑(r.num * m) / ↑(r.den • id n) = ↑m / ↑n * ↑r
⊢ |x - ↑m / ↑n| * |↑r| < ↑r.den ^ p * (↑|r| * C) / ↑(r.den • id n) ^ p

Tactic:
simp only [smul_eq_mul, id, Nat.cast_mul]

Goal state after:
case refine_2
p x : ℝ
r : ℚ
h : LiouvilleWith p x
hr : r ≠ 0
C : ℝ
_hC₀ : 0 < C
hC : ∃ᶠ (n : ℕ) in atTop, 1 ≤ n ∧ ∃ m, x ≠ ↑m / ↑n ∧ |x - ↑m / ↑n| < C / ↑n ^ p
n : ℕ
_hn : 1 ≤ n
m : ℤ
hne : x ≠ ↑m / ↑n
hlt : |x - ↑m / ↑n| < C / ↑n ^ p
A : ↑(r.num * m) / ↑(r.den • id n) = ↑m / ↑n * ↑r
⊢ |x - ↑m / ↑n| * |↑r| < ↑r.den ^ p * (↑|r| * C) / (↑r.den * ↑n) ^ p
Module: Mathlib.Order.Comparable

Goal state before:
pp: α : Type u_1
r : α → α → Prop
inst✝ : Std.Total r
a b : α
⊢ ¬IncompRel r a b

Tactic:
by
  rw [not_incompRel_iff_symmGen]
  exact symmGen_of_total a b

Goal state after:
Module: Mathlib.Order.Concept

Goal state before:
pp: ι : Sort u_1
α : Type u_2
β : Type u_3
r : α → β → Prop
f : ι → Concept α β r
⊢ (⨅ i, f i).intent = upperPolar r (⋂ i, (f i).extent)

Tactic:
simp_rw [iInf, intent_sInf, ← Set.iInf_eq_iInter, iInf_range]

Goal state after:
Module: Mathlib.Order.Extension.Linear

Goal state before:
pp: α : Type u
r : α → α → Prop
inst✝ : IsPartialOrder α r
S : Set (α → α → Prop) := {s | IsPartialOrder α s}
c : Set (α → α → Prop)
hc₁ : c ⊆ S
hc₂ : IsChain (fun x1 x2 ↦ x1 ≤ x2) c
s : α → α → Prop
hs : s ∈ c
⊢ ∃ ub ∈ S, ∀ z ∈ c, z ≤ ub

Tactic:
have := (hc₁ hs).1

Goal state after:
α : Type u
r : α → α → Prop
inst✝ : IsPartialOrder α r
S : Set (α → α → Prop) := {s | IsPartialOrder α s}
c : Set (α → α → Prop)
hc₁ : c ⊆ S
hc₂ : IsChain (fun x1 x2 ↦ x1 ≤ x2) c
s : α → α → Prop
hs : s ∈ c
this : IsPreorder α s
⊢ ∃ ub ∈ S, ∀ z ∈ c, z ≤ ub
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 α)
⊢ t ∈ traverse f (b :: fs) → ∃ us, Forall₂ (fun b s ↦ s ∈ f b) (b :: fs) us ∧ sequence us ⊆ t

Tactic:
intro ht

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)
⊢ ∃ us, Forall₂ (fun b s ↦ s ∈ f b) (b :: fs) us ∧ sequence us ⊆ t
Module: Mathlib.Order.Fin.InsertNth

Goal state before:
pp: case inr.inr
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
j : Fin n
hj : i.castSucc < j.succ
⊢ i.castSucc.succ.insertNth x f j.succ.castSucc < i.castSucc.succ.insertNth x f j.succ.succ

Tactic:
grind [insertNth_apply_same, insertNth_apply_above]

Goal state after:
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 : α
hxy : r x y
hyz : r y z
⊢ x ⊓ y ⊓ z ≤ x

Tactic:
simp [inf_assoc, inf_le_left]

Goal state after:
Module: Mathlib.Order.PrimeIdeal

Goal state before:
pp: P : Type u_1
inst✝¹ : DistribLattice P
I : Ideal P
inst✝ : I.IsMaximal
x y : P
hx : x ∉ I
hynI : y ∉ I
hxy : x ⊓ y ∈ I
J : Ideal P := I ⊔ principal x
hJuniv : ↑J = Set.univ
a : P
ha : a ∈ I
b : P
hb : b ∈ principal x
hy : y = a ⊔ b
⊢ a ⊔ b ∈ I

Tactic:
refine sup_mem ha (I.lower (le_inf hb ?_) hxy)

Goal state after:
P : Type u_1
inst✝¹ : DistribLattice P
I : Ideal P
inst✝ : I.IsMaximal
x y : P
hx : x ∉ I
hynI : y ∉ I
hxy : x ⊓ y ∈ I
J : Ideal P := I ⊔ principal x
hJuniv : ↑J = Set.univ
a : P
ha : a ∈ I
b : P
hb : b ∈ principal x
hy : y = a ⊔ b
⊢ b ≤ y
Module: Mathlib.Order.Nucleus

Goal state before:
pp: X : Type u_1
inst✝ : Frame X
n m : Nucleus X
x y : X
a : ↑(range ⇑n)
s : Set ↑(range ⇑n)
⊢ ⨆ b ∈ Subtype.val '' s, ↑a ⊓ b ≤ ⨆ a_1 ∈ range fun x ↦ a ⊓ ↑x, ↑a_1

Tactic:
iSup_range,

Goal state after:
X : Type u_1
inst✝ : Frame X
n m : Nucleus X
x y : X
a : ↑(range ⇑n)
s : Set ↑(range ⇑n)
⊢ ⨆ b ∈ Subtype.val '' s, ↑a ⊓ b ≤ ⨆ i, ↑(a ⊓ ↑i)
Module: Mathlib.Order.PrimeSeparator

Goal state before:
pp: case h
α : Type u_1
inst✝ : DistribLattice α
F : PFilter α
I : Ideal α
hFI : Disjoint ↑F ↑I
S : Set (Set α) := ⋯
Jset : Set α
left✝ : ↑I ⊆ Jset
hmax : Maximal (fun x ↦ x ∈ S) Jset
Jidl : IsIdeal Jset
IJ : ↑I ⊆ Jset
J : Ideal α := ⋯
IJ' : I ≤ J
Jpr : J.IsProper
a₁ a₂ : α
ha₁ : a₁ ∉ J
ha₂ : a₂ ∉ J
J₁ : Ideal α := ⋯
J₂ : Ideal α := ⋯
a₁J₁ : a₁ ∈ J₁
a₂J₂ : a₂ ∈ J₂
J₁J : ↑J₁ ≠ Jset
J₂J : ↑J₂ ≠ Jset
J₁S : ↑J₁ ∉ S
J₂S : ↑J₂ ∉ S
J₁F : ¬Disjoint ↑F ↑J₁
J₂F : ¬Disjoint ↑F ↑J₂
c₁ : α
c₁F : c₁ ∈ ↑F
c₁J₁ : c₁ ∈ ↑J₁
c₂ : α
c₂F : c₂ ∈ ↑F
c₂J₂ : c₂ ∈ ↑J₂
b₁ : α
b₁J : b₁ ∈ J
cba₁ : c₁ ≤ b₁ ⊔ a₁
b₂ : α
b₂J : b₂ ∈ J
cba₂ : c₂ ≤ b₂ ⊔ a₂
b : α := ⋯
bJ : b ∈ J
ineq : c₁ ⊓ c₂ ≤ b ⊔ a₁ ⊓ a₂
ba₁a₂F : b ⊔ a₁ ⊓ a₂ ∈ F
ha₁a₂ : a₁ ⊓ a₂ ∈ J
⊢ b ⊔ a₁ ⊓ a₂ ∈ ↑F ∧ b ⊔ a₁ ⊓ a₂ ∈ Jset

Tactic:
exact ⟨ba₁a₂F, sup_mem bJ ha₁a₂⟩

Goal state after:
Module: Mathlib.Order.SuccPred.Tree

Goal state before:
pp: α : Type u_1
inst✝³ : PartialOrder α
inst✝² : PredOrder α
inst✝¹ : IsPredArchimedean α
inst✝ : OrderBot α
b : α
⊢ b = ⊥ ∨ ∃ a, IsAtom a ∧ a ≤ b

Tactic:
rw [or_iff_not_imp_left]
    intro hb
    use findAtom b, isAtom_findAtom hb, findAtom_le b

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

Tactic:
rw [Function.onFun_apply, Set.disjoint_left]

Goal state after:
t : RootedTree
t₁ : SubRootedTree t
ht₁ : t₁ ∈ t.subtrees
t₂ : SubRootedTree t
ht₂ : t₂ ∈ t.subtrees
h : t₁ ≠ t₂
⊢ ∀ ⦃a : ↑t⦄, a ∈ ↑t₁ → a ∉ ↑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
hf : Martingale f ℱ μ
n : ℕ
⊢ ∑ i ∈ Finset.range n, μ[f (i + 1) - f i | ↑ℱ i] =ᵐ[μ] 0

Tactic:
← Finset.sum_const_zero (s := Finset.range n)

Goal state after:
Ω : Type u_1
E : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
f : ℕ → Ω → E
ℱ : Filtration ℕ m0
inst✝ : CompleteSpace E
hf : Martingale f ℱ μ
n : ℕ
⊢ ∑ i ∈ Finset.range n, μ[f (i + 1) - f i | ↑ℱ i] =ᵐ[μ] ∑ _x ∈ Finset.range n, 0
Module: Mathlib.Probability.Martingale.Centering

Goal state before:
pp: Ω : Type u_1
E : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
f : ℕ → Ω → E
ℱ : Filtration ℕ m0
inst✝ : CompleteSpace E
hf : Martingale f ℱ μ
n i : ℕ
hi : i ∈ Finset.range n
⊢ μ[f (i + 1) - f i | ↑ℱ i] =ᵐ[μ] μ[f (i + 1) | ↑ℱ i] - μ[f i | ↑ℱ i]

Tactic:
by
    simp [condExp_sub (hf.integrable (i + 1)) (hf.integrable i) (ℱ i)]

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

Goal state before:
pp: case refine_1.zero
Ω : Type u_1
m✝ : MeasurableSpace Ω
E : Type u_3
inst✝ : TopologicalSpace E
𝓕 : Filtration ℕ m✝
u : ℕ → Ω → E
h₀ : StronglyMeasurable (u 0)
h : ∀ (n : ℕ), StronglyMeasurable (u (n + 1))
this : MeasurableSpace (ℕ × Ω) := 𝓕.predictable
X : ℕ → ℕ × Ω → E :=
  fun m x ↦
    match x.1 with
    | 0 => (h₀.approx m) x.2
    | n.succ => (⋯.approx m) x.2
Y : ℕ → ℕ × Ω → E := fun m x ↦ if x.1 ≤ m then X m x else X m (0, x.2)
m : ℕ
s : E
⊢ MeasurableSet ({0} ×ˢ (Function.curry (Y m) 0 ⁻¹' {s}))

Tactic:
apply measurableSet_predictable_singleton_bot_prod
      let : MeasurableSpace Ω := 𝓕 0
      exact (h₀.approx m).measurableSet_fiber s

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 : ι
⊢ Monotone fun x ↦ hittingBtwn u s n x ω

Tactic:
intro m₁ m₂ hm

Goal state after:
Ω : Type u_1
β : Type u_2
ι : Type u_3
inst✝ : ConditionallyCompleteLinearOrder ι
ω : Ω
u : ι → Ω → β
s : Set β
n m₁ m₂ : ι
hm : m₁ ≤ m₂
⊢ (fun x ↦ hittingBtwn u s n x ω) m₁ ≤ (fun x ↦ hittingBtwn u s n x ω) m₂
Module: Mathlib.Probability.Martingale.Convergence

Goal state before:
pp: Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
ω : Ω
hab : a < b
hω : ∃ k, ∀ (N : ℕ), upcrossingsBefore a b f N ω < k
h₁ : ∀ (a_1 : ℕ), ∃ b, a_1 ≤ b ∧ f b ω < a
h₂ : ∀ (a : ℕ), ∃ b_1, a ≤ b_1 ∧ b < f b_1 ω
k : ℕ
⊢ ∃ N, k ≤ upcrossingsBefore a b f N ω

Tactic:
induction k with
  | zero => simp only [zero_le, exists_const]
  | succ k ih =>
    obtain ⟨N, hN⟩ := ih
    obtain ⟨N₁, hN₁, hN₁'⟩ := h₁ N
    obtain ⟨N₂, hN₂, hN₂'⟩ := h₂ N₁
    exact ⟨N₂ + 1, Nat.succ_le_of_lt <|
      lt_of_le_of_lt hN (upcrossingsBefore_lt_of_exists_upcrossing hab hN₁ hN₁' hN₂ hN₂')⟩

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

Goal state before:
pp: Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝³ : AddGroup ι
inst✝² : Preorder ι
inst✝¹ : AddRightMono ι
inst✝ : AddLeftMono ι
f : Filtration ι m
τ : Ω → WithTop ι
hτ : IsStoppingTime f τ
i : ι
hi : 0 ≤ i
j : ι
⊢ MeasurableSet {ω | τ ω + ↑i ≤ ↑j}

Tactic:
have h_eq : {ω | τ ω + i ≤ j} = {ω | τ ω ≤ j - i} := by
    ext ω
    simp only [Set.mem_ofPred_eq, coe_sub]
    cases τ ω with
    | top => simp
    | coe a => norm_cast; simp_rw [← le_sub_iff_add_le]

Goal state after:
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝³ : AddGroup ι
inst✝² : Preorder ι
inst✝¹ : AddRightMono ι
inst✝ : AddLeftMono ι
f : Filtration ι m
τ : Ω → WithTop ι
hτ : IsStoppingTime f τ
i : ι
hi : 0 ≤ i
j : ι
h_eq : {ω | τ ω + ↑i ≤ ↑j} = {ω | τ ω ≤ ↑(j - i)}
⊢ MeasurableSet {ω | τ ω + ↑i ≤ ↑j}
Module: Mathlib.Probability.Process.Stopping

Goal state before:
pp: Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : LinearOrder ι
f : Filtration ι m
τ : Ω → WithTop ι
hτ : IsStoppingTime f τ
h_countable : (Set.range τ).Countable
i : ι
⊢ MeasurableSet {ω | τ ω < ↑i}

Tactic:
have : {ω | τ ω < i} = {ω | τ ω ≤ i} \ {ω | τ ω = i} := by
    ext1 ω
    simp only [lt_iff_le_and_ne, Set.mem_ofPred_eq, Set.mem_sdiff]
  rw [this]
  exact (hτ.measurableSet_le' i).diff (hτ.measurableSet_eq_of_countable_range' h_countable i)

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

Goal state before:
pp: case refine_1
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : LinearOrder ι
f : Filtration ι m
τ π : Ω → WithTop ι
hτ : IsStoppingTime f τ
hπ : IsStoppingTime f π
⊢ ⋯.measurableSpace ≤ hτ.measurableSpace ⊓ hπ.measurableSpace

pp: case refine_2
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : LinearOrder ι
f : Filtration ι m
τ π : Ω → WithTop ι
hτ : IsStoppingTime f τ
hπ : IsStoppingTime f π
⊢ hτ.measurableSpace ⊓ hπ.measurableSpace ≤ ⋯.measurableSpace

Tactic:
· exact le_inf (measurableSpace_mono _ hτ fun _ => min_le_left _ _)
      (measurableSpace_mono _ hπ fun _ => min_le_right _ _)

Goal state after:
case refine_2
Ω : Type u_1
ι : Type u_3
m : MeasurableSpace Ω
inst✝ : LinearOrder ι
f : Filtration ι m
τ π : Ω → WithTop ι
hτ : IsStoppingTime f τ
hπ : IsStoppingTime f π
⊢ hτ.measurableSpace ⊓ hπ.measurableSpace ≤ ⋯.measurableSpace
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 ι
μ : Measure Ω
hσ✝ : ∀ᵐ (ω : Ω) ∂μ, σ ω ≠ ⊤
ω : Ω
hσ : σ ω ≠ ⊤
⊢ stoppedValue (stoppedProcess u τ) σ ω = stoppedValue u (fun ω ↦ min (σ ω) (τ ω)) ω

Tactic:
by simp [stoppedValue_stoppedProcess, hσ]

Goal state after:
Module: Mathlib.Probability.ConditionalExpectation

Goal state before:
pp: case pos.refine_2
Ω : Type u_1
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
m₁ m₂ m : MeasurableSpace Ω
μ : Measure Ω
f : Ω → E
hle₁ : m₁ ≤ m
hle₂ : m₂ ≤ m
inst✝ : SigmaFinite (μ.trim hle₂)
hf : StronglyMeasurable f
hindp : Indep m₁ m₂ μ
hfint : MemLp f 1 μ
s : Set Ω
hms : MeasurableSet s
hs : μ s < ∞
c : E
t : Set Ω
hmt : MeasurableSet t
a✝ : μ t < ∞
⊢ μ.real s • ∫ (x : Ω), t.indicator (fun x ↦ c) x ∂μ = ∫ (x : Ω) in s, t.indicator (fun x ↦ c) x ∂μ

Tactic:
rw [Indep_iff] at hindp

Goal state after:
case pos.refine_2
Ω : Type u_1
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
m₁ m₂ m : MeasurableSpace Ω
μ : Measure Ω
f : Ω → E
hle₁ : m₁ ≤ m
hle₂ : m₂ ≤ m
inst✝ : SigmaFinite (μ.trim hle₂)
hf : StronglyMeasurable f
hindp : ∀ (t1 t2 : Set Ω), MeasurableSet t1 → MeasurableSet t2 → μ (t1 ∩ t2) = μ t1 * μ t2
hfint : MemLp f 1 μ
s : Set Ω
hms : MeasurableSet s
hs : μ s < ∞
c : E
t : Set Ω
hmt : MeasurableSet t
a✝ : μ t < ∞
⊢ μ.real s • ∫ (x : Ω), t.indicator (fun x ↦ c) x ∂μ = ∫ (x : Ω) in s, t.indicator (fun x ↦ c) x ∂μ
Module: Mathlib.Probability.Moments.Basic

Goal state before:
pp: Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
t : ℝ
⊢ cgf 0 μ t = log (μ.real Set.univ)

Tactic:
by simp only [cgf, mgf_zero_fun]

Goal state after: