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

Goal state before:
pp: s : BoundingSieve
w : ℕ → ℝ
d1 : ℕ
hd1 : d1 ∈ s.prodPrimes.divisors
⊢ ∀ x ∈ s.prodPrimes.divisors,
    (∑ x_1 ∈ s.prodPrimes.divisors, if x_1 = d1.lcm x then w d1 * w x * s.nu x_1 else 0) =
      s.nu d1 * w d1 * s.nu x * w x * (s.nu (d1.gcd x))⁻¹

Tactic:
intro d2

Goal state after:
s : BoundingSieve
w : ℕ → ℝ
d1 : ℕ
hd1 : d1 ∈ s.prodPrimes.divisors
d2 : ℕ
⊢ d2 ∈ s.prodPrimes.divisors →
    (∑ x ∈ s.prodPrimes.divisors, if x = d1.lcm d2 then w d1 * w d2 * s.nu x else 0) =
      s.nu d1 * w d1 * s.nu d2 * w d2 * (s.nu (d1.gcd d2))⁻¹
Module: Mathlib.NumberTheory.SumTwoSquares

Goal state before:
pp: m n : ℕ
hd : m ∣ n
hs : IsSquare (-1)
f : ZMod n →+* ZMod m := castHom hd (ZMod m)
⊢ IsSquare (f (-1))

Tactic:
exact hs.map f

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 ℂ
⊢ ‖↑(eval 0 f ^ p + ↑p * eval 0 gp') * cexp r - ↑p * (aeval r) gp‖ ≤
    (if h : (Multiset.map c' (f.aroots ℂ)).toFinset.Nonempty then (Multiset.map c' (f.aroots ℂ)).toFinset.max' h
        else 0) ^
        p /
      ↑(p - 1)!

Tactic:
specialize h r _

Goal state after:
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)

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
r : ℂ
h : (aeval r) (sumIDeriv (X ^ (p - 1) * f ^ p)) = p ! • (aeval r) gp
hr : r ∈ f.aroots ℂ
⊢ ‖↑(eval 0 f ^ p + ↑p * eval 0 gp') * cexp r - ↑p * (aeval r) gp‖ ≤
    (if h : (Multiset.map c' (f.aroots ℂ)).toFinset.Nonempty then (Multiset.map c' (f.aroots ℂ)).toFinset.max' h
        else 0) ^
        p /
      ↑(p - 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
inst✝¹ : IsDedekindDomain S
inst✝ : p.IsMaximal
P : ↥(factors (map f p)).toFinset
⊢ finrank (R ⧸ p) (S ⧸ ↑P ^ p.ramificationIdx' ↑P) = p.ramificationIdx' ↑P * p.inertiaDeg' ↑P

Tactic:
by
  rw [finrank_prime_pow_ramificationIdx, inertiaDeg'_algebraMap]
  exacts [Factors.ne_bot p P, NeZero.ne _]

Goal state after:
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 * ↑r - ↑(r.num * m) / ↑(r.den • id n)| < ↑r.den ^ p * (↑|r| * C) / ↑(r.den • id n) ^ p

Tactic:
A,

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 * ↑r - ↑m / ↑n * ↑r| < ↑r.den ^ p * (↑|r| * C) / ↑(r.den • id n) ^ p
Module: Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith

Goal state before:
pp: p x : ℝ
m : ℤ
hm : m ≠ 0
⊢ LiouvilleWith p (↑m * x) ↔ LiouvilleWith p x

Tactic:
by
  rw [mul_comm, mul_int_iff hm]

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

Goal state before:
pp: p x : ℝ
n : ℕ
⊢ LiouvilleWith p (↑n + x) ↔ LiouvilleWith p x

Tactic:
by rw [add_comm, add_nat_iff]

Goal state after:
Module: Mathlib.NumberTheory.WellApproximable

Goal state before:
pp: T : ℝ
hT : Fact (0 < T)
δ : ℕ → ℝ
hδ : Tendsto δ atTop (𝓝 0)
this : SemilatticeSup Nat.Primes := Nat.Subtype.semilatticeSup fun p ↦ Nat.Prime p
⊢ (∀ᵐ (x : 𝕊), x ∉ addWellApproximable 𝕊 δ) ∨ ∀ᵐ (x : 𝕊), x ∈ addWellApproximable 𝕊 δ

Tactic:
set μ : Measure 𝕊 := volume

Goal state after:
T : ℝ
hT : Fact (0 < T)
δ : ℕ → ℝ
hδ : Tendsto δ atTop (𝓝 0)
this : SemilatticeSup Nat.Primes := Nat.Subtype.semilatticeSup fun p ↦ Nat.Prime p
μ : Measure 𝕊 := volume
⊢ (∀ᵐ (x : 𝕊) ∂μ, x ∉ addWellApproximable 𝕊 δ) ∨ ∀ᵐ (x : 𝕊) ∂μ, x ∈ addWellApproximable 𝕊 δ
Module: Mathlib.NumberTheory.WellApproximable

Goal state before:
pp: T : ℝ
hT : Fact (0 < T)
δ : ℕ → ℝ
hδ : Tendsto δ atTop (𝓝 0)
this : SemilatticeSup Nat.Primes := Nat.Subtype.semilatticeSup fun p ↦ Nat.Prime p
μ : Measure 𝕊 := volume
u : Nat.Primes → 𝕊 := fun p ↦ ↑(↑1 / ↑↑p * T)
hu₀ : ∀ (p : Nat.Primes), addOrderOf (u p) = ↑p
hu : Tendsto (addOrderOf ∘ u) atTop atTop
E : Set 𝕊 := addWellApproximable 𝕊 δ
X : ℕ → Set 𝕊 := fun n ↦ approxAddOrderOf 𝕊 n (δ n)
A : ℕ → Set 𝕊 := fun p ↦ blimsup X atTop fun n ↦ 0 < n ∧ ¬p ∣ n
B : ℕ → Set 𝕊 := fun p ↦ blimsup X atTop fun n ↦ 0 < n ∧ p ∣ n ∧ ¬p * p ∣ n
C : ℕ → Set 𝕊 := fun p ↦ blimsup X atTop fun n ↦ 0 < n ∧ p ^ 2 ∣ n
hA₀ : ∀ (p : ℕ), MeasurableSet (A p)
hB₀ : ∀ (p : ℕ), MeasurableSet (B p)
hE₀ : NullMeasurableSet E μ
hE₁ : ∀ (p : ℕ), E = A p ∪ B p ∪ C p
hE₂ : ∀ (p : Nat.Primes), A ↑p =ᵐ[μ] ∅ ∧ B ↑p =ᵐ[μ] ∅ → E =ᵐ[μ] C ↑p
p : ℕ
hp : Nat.Prime p
f : 𝕊 → 𝕊 := fun y ↦ p • y
n : ℕ
hn : 0 < n ∧ ¬p ∣ n
⊢ (⇑(sSupHom.setImage f) ∘ X) n ⊆ approxAddOrderOf 𝕊 n (↑p * δ n)

Tactic:
replace hn := Nat.coprime_comm.mp (hp.coprime_iff_not_dvd.2 hn.2)

Goal state after:
T : ℝ
hT : Fact (0 < T)
δ : ℕ → ℝ
hδ : Tendsto δ atTop (𝓝 0)
this : SemilatticeSup Nat.Primes := Nat.Subtype.semilatticeSup fun p ↦ Nat.Prime p
μ : Measure 𝕊 := volume
u : Nat.Primes → 𝕊 := fun p ↦ ↑(↑1 / ↑↑p * T)
hu₀ : ∀ (p : Nat.Primes), addOrderOf (u p) = ↑p
hu : Tendsto (addOrderOf ∘ u) atTop atTop
E : Set 𝕊 := addWellApproximable 𝕊 δ
X : ℕ → Set 𝕊 := fun n ↦ approxAddOrderOf 𝕊 n (δ n)
A : ℕ → Set 𝕊 := fun p ↦ blimsup X atTop fun n ↦ 0 < n ∧ ¬p ∣ n
B : ℕ → Set 𝕊 := fun p ↦ blimsup X atTop fun n ↦ 0 < n ∧ p ∣ n ∧ ¬p * p ∣ n
C : ℕ → Set 𝕊 := fun p ↦ blimsup X atTop fun n ↦ 0 < n ∧ p ^ 2 ∣ n
hA₀ : ∀ (p : ℕ), MeasurableSet (A p)
hB₀ : ∀ (p : ℕ), MeasurableSet (B p)
hE₀ : NullMeasurableSet E μ
hE₁ : ∀ (p : ℕ), E = A p ∪ B p ∪ C p
hE₂ : ∀ (p : Nat.Primes), A ↑p =ᵐ[μ] ∅ ∧ B ↑p =ᵐ[μ] ∅ → E =ᵐ[μ] C ↑p
p : ℕ
hp : Nat.Prime p
f : 𝕊 → 𝕊 := fun y ↦ p • y
n : ℕ
hn : n.Coprime p
⊢ (⇑(sSupHom.setImage f) ∘ X) n ⊆ approxAddOrderOf 𝕊 n (↑p * δ n)
Module: Mathlib.Order.Concept

Goal state before:
pp: α : Type u_2
β : Type u_3
r : α → β → Prop
c : Concept α β r
e : Set α
i : Set β
he : e = c.extent
hi : i = c.intent
⊢ c.copy e i he hi = c

Tactic:
by
  ext; simp_all

Goal state after:
Module: Mathlib.NumberTheory.WellApproximable

Goal state before:
pp: T : ℝ
hT : Fact (0 < T)
δ : ℕ → ℝ
hδ : Tendsto δ atTop (𝓝 0)
this : SemilatticeSup Nat.Primes := Nat.Subtype.semilatticeSup fun p ↦ Nat.Prime p
μ : Measure 𝕊 := volume
u : Nat.Primes → 𝕊 := fun p ↦ ↑(↑1 / ↑↑p * T)
hu₀ : ∀ (p : Nat.Primes), addOrderOf (u p) = ↑p
hu : Tendsto (addOrderOf ∘ u) atTop atTop
E : Set 𝕊 := addWellApproximable 𝕊 δ
X : ℕ → Set 𝕊 := fun n ↦ approxAddOrderOf 𝕊 n (δ n)
A : ℕ → Set 𝕊 := fun p ↦ blimsup X atTop fun n ↦ 0 < n ∧ ¬p ∣ n
B : ℕ → Set 𝕊 := fun p ↦ blimsup X atTop fun n ↦ 0 < n ∧ p ∣ n ∧ ¬p * p ∣ n
C : ℕ → Set 𝕊 := fun p ↦ blimsup X atTop fun n ↦ 0 < n ∧ p ^ 2 ∣ n
hA₀ : ∀ (p : ℕ), MeasurableSet (A p)
hB₀ : ∀ (p : ℕ), MeasurableSet (B p)
hE₀ : NullMeasurableSet E μ
hE₁ : ∀ (p : ℕ), E = A p ∪ B p ∪ C p
hE₂ : ∀ (p : Nat.Primes), A ↑p =ᵐ[μ] ∅ ∧ B ↑p =ᵐ[μ] ∅ → E =ᵐ[μ] C ↑p
hA : ∀ (p : Nat.Primes), A ↑p =ᵐ[μ] ∅ ∨ A ↑p =ᵐ[μ] univ
hB : ∀ (p : Nat.Primes), B ↑p =ᵐ[μ] ∅ ∨ B ↑p =ᵐ[μ] univ
p : Nat.Primes
e : Set 𝕊 ≃o Set 𝕊 := Equiv.toOrderIsoSet (AddAction.toPerm (u p))
⊢ (blimsup (⇑e ∘ X) atTop fun n ↦ 0 < n ∧ ↑p ^ 2 ∣ n) = C ↑p

Tactic:
← hu₀ p

Goal state after:
T : ℝ
hT : Fact (0 < T)
δ : ℕ → ℝ
hδ : Tendsto δ atTop (𝓝 0)
this : SemilatticeSup Nat.Primes := Nat.Subtype.semilatticeSup fun p ↦ Nat.Prime p
μ : Measure 𝕊 := volume
u : Nat.Primes → 𝕊 := fun p ↦ ↑(↑1 / ↑↑p * T)
hu₀ : ∀ (p : Nat.Primes), addOrderOf (u p) = ↑p
hu : Tendsto (addOrderOf ∘ u) atTop atTop
E : Set 𝕊 := addWellApproximable 𝕊 δ
X : ℕ → Set 𝕊 := fun n ↦ approxAddOrderOf 𝕊 n (δ n)
A : ℕ → Set 𝕊 := fun p ↦ blimsup X atTop fun n ↦ 0 < n ∧ ¬p ∣ n
B : ℕ → Set 𝕊 := fun p ↦ blimsup X atTop fun n ↦ 0 < n ∧ p ∣ n ∧ ¬p * p ∣ n
C : ℕ → Set 𝕊 := fun p ↦ blimsup X atTop fun n ↦ 0 < n ∧ p ^ 2 ∣ n
hA₀ : ∀ (p : ℕ), MeasurableSet (A p)
hB₀ : ∀ (p : ℕ), MeasurableSet (B p)
hE₀ : NullMeasurableSet E μ
hE₁ : ∀ (p : ℕ), E = A p ∪ B p ∪ C p
hE₂ : ∀ (p : Nat.Primes), A ↑p =ᵐ[μ] ∅ ∧ B ↑p =ᵐ[μ] ∅ → E =ᵐ[μ] C ↑p
hA : ∀ (p : Nat.Primes), A ↑p =ᵐ[μ] ∅ ∨ A ↑p =ᵐ[μ] univ
hB : ∀ (p : Nat.Primes), B ↑p =ᵐ[μ] ∅ ∨ B ↑p =ᵐ[μ] univ
p : Nat.Primes
e : Set 𝕊 ≃o Set 𝕊 := Equiv.toOrderIsoSet (AddAction.toPerm (u p))
⊢ (blimsup (⇑e ∘ X) atTop fun n ↦ 0 < n ∧ addOrderOf (u p) ^ 2 ∣ n) = C (addOrderOf (u p))
Module: Mathlib.Order.Height

Goal state before:
pp: α : Type u_1
s : Set α
r : α → α → Prop
⊢ s.chainHeight r = ⊤ ↔ ∀ (n : ℕ), ∃ t ⊆ s, t.encard = ↑n ∧ IsChain r t

Tactic:
refine ⟨fun h _ ↦ exists_isChain_of_le_chainHeight _ (le_top.trans_eq h.symm), fun h ↦ ?_⟩
  contrapose! h
  obtain ⟨n, hn⟩ := ENat.ne_top_iff_exists.mp h
  refine ⟨n + 1, fun l hl he ↦ not_isChain_of_chainHeight_lt_encard r s l hl ?_⟩
  rw [← hn, he]
  exact_mod_cast lt_add_one _

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 t : α⦄, x ≤ y → r x y → r (x ⊓ t) (y ⊓ t) ∧ r (x ⊔ t) (y ⊔ t)
a b c d : α
hab : a ≤ b
hbd : b ≤ d
hac : a ≤ c
hcd : c ≤ d
had : r a d
this : r (b ⊓ c ⊓ (b ⊔ c)) (d ⊓ (b ⊔ c))
⊢ r b c

Tactic:
simpa [h₂, inf_eq_right.mpr (sup_le hbd hcd)] using this

Goal state after:
Module: Mathlib.Order.Lattice.Congruence

Goal state before:
pp: F : Type u_1
α : Type u_2
β : Type u_3
inst✝¹ : Lattice α
inst✝ : Lattice β
r : α → α → Prop
h₁ : Std.Refl r
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)
⊢ ∀ {w x y z : α}, r w x → r y z → r (w ⊓ y) (x ⊓ z)

Tactic:
by
    intro w _ _ _ h1 h2
    have compatible_left_inf {x y t : α} (hh : r x y) : r (x ⊓ t) (y ⊓ t) :=
      closed_interval h₂ h₄ ((x ⊓ y) ⊓ t) _ _ ((x ⊔ y) ⊓ t)
            (inf_le_inf_right _ inf_le_left) (inf_le_inf_right _ le_sup_left)
            (inf_le_inf_right _ inf_le_right) (inf_le_inf_right _ le_sup_right)
            (h₄ inf_le_sup (h₂.mp hh)).1
    exact transitive h₂ h₃ h₄ (by
          simpa [inf_comm w] using compatible_left_inf h2) (compatible_left_inf h1)

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

Goal state before:
pp: α✝ : Type u_1
s✝ t x y z : α✝
S : Set α✝
inst✝¹ : CompleteLattice α✝
P✝ Q✝ : Partition s✝
α : Type u_2
inst✝ : Order.Frame α
s : α
P Q : Partition s
a : α
ha : a ∈ {a | ∃ p ∈ P, ∃ q ∈ Q, a = p ⊓ q}
a' : α
⊢ a' ∈ {a | ∃ p ∈ P, ∃ q ∈ Q, a = p ⊓ q} → a ≠ a' → Function.onFun Disjoint id a a'

Tactic:
ha'

Goal state after:
α✝ : Type u_1
s✝ t x y z : α✝
S : Set α✝
inst✝¹ : CompleteLattice α✝
P✝ Q✝ : Partition s✝
α : Type u_2
inst✝ : Order.Frame α
s : α
P Q : Partition s
a : α
ha : a ∈ {a | ∃ p ∈ P, ∃ q ∈ Q, a = p ⊓ q}
a' : α
ha' : a' ∈ {a | ∃ p ∈ P, ∃ q ∈ Q, a = p ⊓ q}
⊢ a ≠ a' → Function.onFun Disjoint id a a'
Module: Mathlib.Order.Partition.Basic

Goal state before:
pp: α✝ : Type u_1
s✝ t x y z : α✝
S : Set α✝
inst✝¹ : CompleteLattice α✝
P✝ Q✝ : Partition s✝
α : Type u_2
inst✝ : Order.Frame α
s : α
P Q : Partition s
a : α
ha : a ∈ removeBot {a | ∃ p ∈ P, ∃ q ∈ Q, a = p ⊓ q} ⋯ ⋯
⊢ ∃ y ∈ P, a ≤ y

Tactic:
obtain ⟨⟨p, hp, q, hq, rfl⟩, h⟩ := ha
    grind [inf_le_left]

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

Goal state before:
pp: t : RootedTree
t₁ t₂ : SubRootedTree t
ht₁ : t₁ ∈ t.subtrees
ht₂ : t₂ ∈ t.subtrees
v₁ v₂ : ↑t
h₁ : t₁.root ≤ v₁
h₂ : t₂.root ≤ v₂
h : ⊥ < v₁ ⊓ v₂
⊢ t₁ = t₂

Tactic:
rcases lt_or_le_of_directed (by simp : v₁ ⊓ v₂ ≤ v₁) h₁ with oh | oh

Goal state after:
case inl
t : RootedTree
t₁ t₂ : SubRootedTree t
ht₁ : t₁ ∈ t.subtrees
ht₂ : t₂ ∈ t.subtrees
v₁ v₂ : ↑t
h₁ : t₁.root ≤ v₁
h₂ : t₂.root ≤ v₂
h : ⊥ < v₁ ⊓ v₂
oh : v₁ ⊓ v₂ < t₁.root
⊢ t₁ = t₂

case inr
t : RootedTree
t₁ t₂ : SubRootedTree t
ht₁ : t₁ ∈ t.subtrees
ht₂ : t₂ ∈ t.subtrees
v₁ v₂ : ↑t
h₁ : t₁.root ≤ v₁
h₂ : t₂.root ≤ v₂
h : ⊥ < v₁ ⊓ v₂
oh : t₁.root ≤ v₁ ⊓ v₂
⊢ t₁ = t₂
Module: Mathlib.Order.Types.Arithmetic

Goal state before:
pp: o₁ o₂ o₃ : OrderType.{u}
α : Type u
x✝² : LinearOrder α
β : Type u
x✝¹ : LinearOrder β
γ : Type u
x✝ : LinearOrder γ
⊢ type α + type β + type γ = type α + (type β + type γ)

Tactic:
by
      simp only [← type_lex_sum, (OrderIso.sumLexAssoc α β γ).type_congr]

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
ℱ : Filtration ι m0
inst✝² : CompleteSpace E
inst✝¹ : PartialOrder E
inst✝ : IsOrderedAddMonoid E
f : ι → Ω → E
hf : Submartingale f ℱ μ
i j : ι
hij : i ≤ j
⊢ 0 ≤ᵐ[μ] μ[f j - f i | ↑ℱ i]

Tactic:
by_cases h : SigmaFinite (μ.trim (ℱ.le i))

Goal state after:
case pos
Ω : Type u_1
E : Type u_2
ι : Type u_3
inst✝⁵ : Preorder ι
m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
ℱ : Filtration ι m0
inst✝² : CompleteSpace E
inst✝¹ : PartialOrder E
inst✝ : IsOrderedAddMonoid E
f : ι → Ω → E
hf : Submartingale f ℱ μ
i j : ι
hij : i ≤ j
h : SigmaFinite (μ.trim ⋯)
⊢ 0 ≤ᵐ[μ] μ[f j - f i | ↑ℱ i]

case neg
Ω : Type u_1
E : Type u_2
ι : Type u_3
inst✝⁵ : Preorder ι
m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
ℱ : Filtration ι m0
inst✝² : CompleteSpace E
inst✝¹ : PartialOrder E
inst✝ : IsOrderedAddMonoid E
f : ι → Ω → E
hf : Submartingale f ℱ μ
i j : ι
hij : i ≤ j
h : ¬SigmaFinite (μ.trim ⋯)
⊢ 0 ≤ᵐ[μ] μ[f j - f i | ↑ℱ i]
Module: Mathlib.Probability.Martingale.Basic

Goal state before:
pp: case base
Ω : Type u_1
E : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
𝒢 : Filtration ℕ m0
inst✝⁵ : CompleteSpace E
inst✝⁴ : PartialOrder E
inst✝³ : IsOrderedAddMonoid E
inst✝² : ClosedIciTopology E
inst✝¹ : IsOrderedModule ℝ E
inst✝ : IsFiniteMeasure μ
f : ℕ → Ω → E
hadp : StronglyAdapted 𝒢 f
hint : ∀ (i : ℕ), Integrable (f i) μ
hf : ∀ (i : ℕ), f i ≤ᵐ[μ] μ[f (i + 1) | ↑𝒢 i]
i j : ℕ
⊢ f i ≤ᵐ[μ] μ[f i | ↑𝒢 i]

Tactic:
refine ae_of_all _ fun _ ↦ ?_
    rw [condExp_of_stronglyMeasurable (𝒢.le i) (hadp i) (hint i)]

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

Goal state before:
pp: case base
Ω : Type u_1
E : Type u_2
m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
𝒢 : Filtration ℕ m0
inst✝¹ : CompleteSpace E
inst✝ : IsFiniteMeasure μ
f : ℕ → Ω → E
hadp : StronglyAdapted 𝒢 f
hint : ∀ (i : ℕ), Integrable (f i) μ
hf : ∀ (i : ℕ), f i =ᵐ[μ] μ[f (i + 1) | ↑𝒢 i]
i j : ℕ
⊢ μ[f i | ↑𝒢 i] =ᵐ[μ] f i

Tactic:
refine ae_of_all _ fun _ ↦ ?_
    rw [condExp_of_stronglyMeasurable (𝒢.le i) (hadp i) (hint i)]

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

Goal state before:
pp: Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N n : ℕ
ω : Ω
M : ℕ
hNM : N ≤ M
h : upperCrossingTime a b f N (n + 1) ω < N
⊢ upperCrossingTime a b f M (n + 1) ω = upperCrossingTime a b f N (n + 1) ω ∧
    lowerCrossingTime a b f M n ω = lowerCrossingTime a b f N n ω

Tactic:
by
  have := (crossing_eq_crossing_of_lowerCrossingTime_lt hNM
    (lt_of_le_of_lt lowerCrossingTime_le_upperCrossingTime_succ h)).2
  refine ⟨?_, this⟩
  rw [upperCrossingTime_succ_eq, upperCrossingTime_succ_eq, eq_comm, this]
  refine hittingBtwn_eq_hittingBtwn_of_exists hNM ?_
  rw [upperCrossingTime_succ_eq, hittingBtwn_lt_iff] at h
  · obtain ⟨j, hj₁, hj₂⟩ := h
    exact ⟨j, ⟨hj₁.1, hj₁.2.le⟩, hj₂⟩
  · exact le_rfl

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

Goal state before:
pp: case refine_1
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
a b : ℝ
f : ℕ → Ω → ℝ
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hab : a < b
this : ∫⁻ (ω : Ω), upcrossings a b f ω ∂μ ≤ (⨆ N, ∫⁻ (ω : Ω), ENNReal.ofReal (f N ω - a)⁺ ∂μ) / ENNReal.ofReal (b - a)
hbdd : ∀ (n : ℕ), ∫⁻ (x : Ω), ‖f n x‖ₑ ∂μ ≤ ↑R
n : ℕ
ω : Ω
⊢ ↑‖f n ω + -a‖₊ ≤ ↑(‖f n ω‖₊ + ‖-a‖₊)

Tactic:
ENNReal.coe_le_coe

Goal state after:
case refine_1
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
a b : ℝ
f : ℕ → Ω → ℝ
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hab : a < b
this : ∫⁻ (ω : Ω), upcrossings a b f ω ∂μ ≤ (⨆ N, ∫⁻ (ω : Ω), ENNReal.ofReal (f N ω - a)⁺ ∂μ) / ENNReal.ofReal (b - a)
hbdd : ∀ (n : ℕ), ∫⁻ (x : Ω), ‖f n x‖ₑ ∂μ ≤ ↑R
n : ℕ
ω : Ω
⊢ ‖f n ω + -a‖₊ ≤ ‖f n ω‖₊ + ‖-a‖₊
Module: Mathlib.Probability.Martingale.Convergence

Goal state before:
pp: case pos
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
a b : ℝ
f : ℕ → Ω → ℝ
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hbdd : ∀ (n : ℕ), eLpNorm (f n) 1 μ ≤ ↑R
hab : a < b
this : ∫⁻ (ω : Ω), upcrossings a b f ω ∂μ ≤ (⨆ N, ∫⁻ (ω : Ω), ENNReal.ofReal (f N ω - a)⁺ ∂μ) / ENNReal.ofReal (b - a)
hR' : ∀ (n : ℕ), ∫⁻ (ω : Ω), ↑‖f n ω - a‖₊ ∂μ ≤ ↑R + ↑‖a‖₊ * μ Set.univ
n : ℕ
ω : Ω
hnonneg : 0 ≤ f n ω - a
⊢ f n ω - a ≤ |f n ω - a|

Tactic:
abs_of_nonneg hnonneg

Goal state after:
case pos
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
a b : ℝ
f : ℕ → Ω → ℝ
R : ℝ≥0
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hbdd : ∀ (n : ℕ), eLpNorm (f n) 1 μ ≤ ↑R
hab : a < b
this : ∫⁻ (ω : Ω), upcrossings a b f ω ∂μ ≤ (⨆ N, ∫⁻ (ω : Ω), ENNReal.ofReal (f N ω - a)⁺ ∂μ) / ENNReal.ofReal (b - a)
hR' : ∀ (n : ℕ), ∫⁻ (ω : Ω), ↑‖f n ω - a‖₊ ∂μ ≤ ↑R + ↑‖a‖₊ * μ Set.univ
n : ℕ
ω : Ω
hnonneg : 0 ≤ f n ω - a
⊢ f n ω - a ≤ f n ω - a
Module: Mathlib.Probability.Martingale.Upcrossing

Goal state before:
pp: case mp
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
ω : Ω
this : upcrossings a b f ω < ∞ ↔ ∃ k, upcrossings a b f ω ≤ ↑k
k : ℝ≥0
hk : ∀ (i : ℕ), ↑(upcrossingsBefore a b f i ω) ≤ ↑k
m : ℕ
hm : k ≤ ↑m
N : ℕ
⊢ ↑k ≤ ↑↑m

Tactic:
ENNReal.coe_le_coe

Goal state after:
case mp
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
ω : Ω
this : upcrossings a b f ω < ∞ ↔ ∃ k, upcrossings a b f ω ≤ ↑k
k : ℝ≥0
hk : ∀ (i : ℕ), ↑(upcrossingsBefore a b f i ω) ≤ ↑k
m : ℕ
hm : k ≤ ↑m
N : ℕ
⊢ k ≤ ↑m
Module: Mathlib.Probability.Martingale.Convergence

Goal state before:
pp: case iUnion
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
inst✝ : IsFiniteMeasure μ
g : Ω → ℝ
hg : Integrable g μ
hgmeas : StronglyMeasurable g
hle : ⨆ n, ↑ℱ n ≤ m0
hunif : UniformIntegrable (fun n ↦ μ[g | ↑ℱ n]) 1 μ
R : ℝ≥0
hR : ∀ (i : ℕ), eLpNorm ((fun n ↦ μ[g | ↑ℱ n]) i) 1 μ ≤ ↑R
hlimint : Integrable (limitProcess (fun n ↦ μ[g | ↑ℱ n]) ℱ μ) μ
this :
  ∀ (n : ℕ) (s : Set Ω),
    MeasurableSet s → ∫ (x : Ω) in s, g x ∂μ = ∫ (x : Ω) in s, limitProcess (fun n x ↦ μ[g | ↑ℱ n] x) ℱ μ x ∂μ
s : Set Ω
hpi : IsPiSystem {s | ∃ n, MeasurableSet s}
f : ℕ → Set Ω
hf : Pairwise (Function.onFun Disjoint f)
hfmeas : ∀ (i : ℕ), MeasurableSet (f i)
heq :
  ∀ (i : ℕ), μ (f i) < ∞ → ∫ (x : Ω) in f i, g x ∂μ = ∫ (x : Ω) in f i, limitProcess (fun n x ↦ μ[g | ↑ℱ n] x) ℱ μ x ∂μ
x✝ : μ (⋃ i, f i) < ∞
⊢ ∫ (x : Ω) in ⋃ i, f i, g x ∂μ = ∫ (x : Ω) in ⋃ i, f i, limitProcess (fun n x ↦ μ[g | ↑ℱ n] x) ℱ μ x ∂μ

Tactic:
| iUnion f hf hfmeas heq =>

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

Goal state before:
pp: case h
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
inst✝ : IsFiniteMeasure μ
hsub : Submartingale f 𝒢 μ
hnonneg : 0 ≤ f
ε : ℝ≥0
n : ℕ
ω : Ω
hω : ((range (n + 1)).sup' ⋯ fun k ↦ f k ω) < ↑ε
⊢ f n ω ≤ stoppedValue f (fun ω ↦ ↑(hittingBtwn f {y | ↑ε ≤ y} 0 n ω)) ω

Tactic:
have : hittingBtwn f {y : ℝ | ε ≤ y} 0 n ω = n := by
        simp only [hittingBtwn, Set.mem_ofPred_eq, ite_eq_right_iff, forall_exists_index, and_imp]
        intro m hm hεm
        exact False.elim
          ((not_le.2 hω) ((le_sup'_iff _).2 ⟨m, mem_range.2 (Nat.lt_succ_of_le hm.2), hεm⟩))

Goal state after:
case h
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
f : ℕ → Ω → ℝ
inst✝ : IsFiniteMeasure μ
hsub : Submartingale f 𝒢 μ
hnonneg : 0 ≤ f
ε : ℝ≥0
n : ℕ
ω : Ω
hω : ((range (n + 1)).sup' ⋯ fun k ↦ f k ω) < ↑ε
this : hittingBtwn f {y | ↑ε ≤ y} 0 n ω = n
⊢ f n ω ≤ stoppedValue f (fun ω ↦ ↑(hittingBtwn f {y | ↑ε ≤ y} 0 n ω)) ω
Module: Mathlib.Probability.Moments.Basic

Goal state before:
pp: Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t α : ℝ
⊢ mgf (fun ω ↦ α + X ω) μ t = rexp (t * α) * mgf X μ t

Tactic:
rw [mgf, mgf, ← integral_const_mul]

Goal state after:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t α : ℝ
⊢ ∫ (x : Ω), (fun ω ↦ rexp (t * (α + X ω))) x ∂μ = ∫ (a : Ω), rexp (t * α) * rexp (t * X a) ∂μ
Module: Mathlib.Probability.Moments.Basic

Goal state before:
pp: Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
X Y : Ω → ℝ
h_indep : X ⟂ᵢ[μ] Y
s t : ℝ
⊢ (fun ω ↦ rexp (s * X ω)) ⟂ᵢ[μ] fun ω ↦ rexp (t * Y ω)

Tactic:
have h_meas : ∀ t, Measurable fun x => exp (t * x) := fun t => (measurable_id'.const_mul t).exp

Goal state after:
Ω : Type u_1
m : MeasurableSpace Ω
μ : Measure Ω
X Y : Ω → ℝ
h_indep : X ⟂ᵢ[μ] Y
s t : ℝ
h_meas : ∀ (t : ℝ), Measurable fun x ↦ rexp (t * x)
⊢ (fun ω ↦ rexp (s * X ω)) ⟂ᵢ[μ] fun ω ↦ rexp (t * Y ω)
Module: Mathlib.Probability.Process.Stopping

Goal state before:
pp: case inr
Ω : Type u_1
ι : Type u_3
inst✝² : Nonempty ι
τ : Ω → WithTop ι
E : Type u_4
u : ι → Ω → E
inst✝¹ : LinearOrder ι
inst✝ : AddCommMonoid E
s : Finset ι
n : ι
ω : Ω
i : ι
hi : ↑i = τ ω
hbdd : ↑i ∈ WithTop.some '' ↑s
h : ↑i < ↑n
⊢ u i ω = 0 + {ω | τ ω = ↑i}.indicator (u i) ω

pp: case inr.h
Ω : Type u_1
ι : Type u_3
inst✝² : Nonempty ι
τ : Ω → WithTop ι
E : Type u_4
u : ι → Ω → E
inst✝¹ : LinearOrder ι
inst✝ : AddCommMonoid E
s : Finset ι
n : ι
ω : Ω
i : ι
hi : ↑i = τ ω
hbdd : ↑i ∈ WithTop.some '' ↑s
h : ↑i < ↑n
⊢ ω ∉ {a | ↑n ≤ τ a}

Tactic:
zero_add,

Goal state after:
case inr
Ω : Type u_1
ι : Type u_3
inst✝² : Nonempty ι
τ : Ω → WithTop ι
E : Type u_4
u : ι → Ω → E
inst✝¹ : LinearOrder ι
inst✝ : AddCommMonoid E
s : Finset ι
n : ι
ω : Ω
i : ι
hi : ↑i = τ ω
hbdd : ↑i ∈ WithTop.some '' ↑s
h : ↑i < ↑n
⊢ u i ω = {ω | τ ω = ↑i}.indicator (u i) ω

case inr.h
Ω : Type u_1
ι : Type u_3
inst✝² : Nonempty ι
τ : Ω → WithTop ι
E : Type u_4
u : ι → Ω → E
inst✝¹ : LinearOrder ι
inst✝ : AddCommMonoid E
s : Finset ι
n : ι
ω : Ω
i : ι
hi : ↑i = τ ω
hbdd : ↑i ∈ WithTop.some '' ↑s
h : ↑i < ↑n
⊢ ω ∉ {a | ↑n ≤ τ a}