harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/RingTheory/TwoSidedIdeal/Lattice.lean
lemma mem_sup {I J : TwoSidedIdeal R} {x : R} :
    x ∈ I ⊔ J ↔ ∃ y ∈ I, ∃ z ∈ J, y + z = x

Proof state:
R : Type u_1
inst✝ : NonUnitalNonAssocRing R
I J : TwoSidedIdeal R
x : R
⊢ x ∈ I ⊔ J ↔ ∃ y ∈ I, ∃ z ∈ J, y + z = x

Tactic:
constructor

Result:
case mp
R : Type u_1
inst✝ : NonUnitalNonAssocRing R
I J : TwoSidedIdeal R
x : R
⊢ x ∈ I ⊔ J → ∃ y ∈ I, ∃ z ∈ J, y + z = x

case mpr
R : Type u_1
inst✝ : NonUnitalNonAssocRing R
I J : TwoSidedIdeal R
x : R
⊢ (∃ y ∈ I, ∃ z ∈ J, y + z = x) → x ∈ I ⊔ J

Proof state:
R : Type u_1
inst✝ : NonUnitalNonAssocRing R
I J : TwoSidedIdeal R
x✝ x : R
hx : x ∈ I
y : R
hy : y ∈ J
⊢ -x + -y = -(x + y)

Tactic:
abel

Result:
no goals

Proof state:
R : Type u_1
inst✝ : NonUnitalNonAssocRing R
I J : TwoSidedIdeal R
x : R
⊢ ∀ {x y : R}, x ∈ {x | ∃ y ∈ I, ∃ z ∈ J, y + z = x} → x * y ∈ {x | ∃ y ∈ I, ∃ z ∈ J, y + z = x}

Tactic:
rintro r _ ⟨x, ⟨hx, ⟨y, ⟨hy, rfl⟩⟩⟩⟩

Result:
case intro.intro.intro.intro
R : Type u_1
inst✝ : NonUnitalNonAssocRing R
I J : TwoSidedIdeal R
x✝ y✝ x : R
hx : x ∈ I
y : R
hy : y ∈ J
⊢ (x + y) * y✝ ∈ {x | ∃ y ∈ I, ∃ z ∈ J, y + z = x}

Proof state:
case mpr.intro.intro.intro.intro
R : Type u_1
inst✝ : NonUnitalNonAssocRing R
I J : TwoSidedIdeal R
y : R
hy : y ∈ I
z : R
hz : z ∈ J
⊢ y + z ∈ I ⊔ J

Tactic:
exact add_mem _ (mem_sup_left hy) (mem_sup_right hz)

Result:
no goals

Proof state:
R : Type u_1
inst✝ : NonUnitalNonAssocRing R
I J : TwoSidedIdeal R
x : R
⊢ ∀ {x : R}, x ∈ {x | ∃ y ∈ I, ∃ z ∈ J, y + z = x} → -x ∈ {x | ∃ y ∈ I, ∃ z ∈ J, y + z = x}

Tactic:
rintro _ ⟨x, ⟨hx, ⟨y, ⟨hy, rfl⟩⟩⟩⟩

Result:
case intro.intro.intro.intro
R : Type u_1
inst✝ : NonUnitalNonAssocRing R
I J : TwoSidedIdeal R
x✝ x : R
hx : x ∈ I
y : R
hy : y ∈ J
⊢ -(x + y) ∈ {x | ∃ y ∈ I, ∃ z ∈ J, y + z = x}
-- Mathlib/Analysis/SpecificLimits/Basic.lean
theorem edist_le_of_edist_le_geometric_of_tendsto {a : α} (ha : Tendsto f atTop (𝓝 a)) (n : ℕ) :
    edist (f n) a ≤ C * r ^ n / (1 - r)

Proof state:
case h.e'_4
α : Type u_1
inst✝ : PseudoEMetricSpace α
r C : ℝ≥0∞
f : ℕ → α
hu : ∀ (n : ℕ), edist (f n) (f (n + 1)) ≤ C * r ^ n
a : α
ha : Tendsto f atTop (𝓝 a)
n : ℕ
⊢ C * r ^ n / (1 - r) = ∑' (m : ℕ), C * r ^ (n + m)

Tactic:
simp only [pow_add, ENNReal.tsum_mul_left, ENNReal.tsum_geometric, div_eq_mul_inv, mul_assoc]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : PseudoEMetricSpace α
r C : ℝ≥0∞
f : ℕ → α
hu : ∀ (n : ℕ), edist (f n) (f (n + 1)) ≤ C * r ^ n
a : α
ha : Tendsto f atTop (𝓝 a)
n : ℕ
⊢ edist (f n) a ≤ C * r ^ n / (1 - r)

Tactic:
convert edist_le_tsum_of_edist_le_of_tendsto _ hu ha _

Result:
case h.e'_4
α : Type u_1
inst✝ : PseudoEMetricSpace α
r C : ℝ≥0∞
f : ℕ → α
hu : ∀ (n : ℕ), edist (f n) (f (n + 1)) ≤ C * r ^ n
a : α
ha : Tendsto f atTop (𝓝 a)
n : ℕ
⊢ C * r ^ n / (1 - r) = ∑' (m : ℕ), C * r ^ (n + m)
-- Mathlib/Order/Filter/Bases.lean
theorem HasBasis.to_hasBasis' (hl : l.HasBasis p s) (h : ∀ i, p i → ∃ i', p' i' ∧ s' i' ⊆ s i)
    (h' : ∀ i', p' i' → s' i' ∈ l) : l.HasBasis p' s'

Proof state:
case intro.intro.intro.intro
α : Type u_1
ι : Sort u_4
ι' : Sort u_5
l : Filter α
p : ι → Prop
s : ι → Set α
p' : ι' → Prop
s' : ι' → Set α
hl : l.HasBasis p s
h : ∀ (i : ι), p i → ∃ i', p' i' ∧ s' i' ⊆ s i
h' : ∀ (i' : ι'), p' i' → s' i' ∈ l
t : Set α
ht✝ : t ∈ l
i : ι
hi : p i
ht : s i ⊆ t
i' : ι'
hi' : p' i'
hs's : s' i' ⊆ s i
⊢ ∃ i, p' i ∧ s' i ⊆ t

Tactic:
exact ⟨i', hi', hs's.trans ht⟩

Result:
no goals

Proof state:
α : Type u_1
ι : Sort u_4
ι' : Sort u_5
l : Filter α
p : ι → Prop
s : ι → Set α
p' : ι' → Prop
s' : ι' → Set α
hl : l.HasBasis p s
h : ∀ (i : ι), p i → ∃ i', p' i' ∧ s' i' ⊆ s i
h' : ∀ (i' : ι'), p' i' → s' i' ∈ l
t : Set α
ht : t ∈ l
⊢ ∃ i, p' i ∧ s' i ⊆ t

Tactic:
rcases hl.mem_iff.1 ht with ⟨i, hi, ht⟩

Result:
case intro.intro
α : Type u_1
ι : Sort u_4
ι' : Sort u_5
l : Filter α
p : ι → Prop
s : ι → Set α
p' : ι' → Prop
s' : ι' → Set α
hl : l.HasBasis p s
h : ∀ (i : ι), p i → ∃ i', p' i' ∧ s' i' ⊆ s i
h' : ∀ (i' : ι'), p' i' → s' i' ∈ l
t : Set α
ht✝ : t ∈ l
i : ι
hi : p i
ht : s i ⊆ t
⊢ ∃ i, p' i ∧ s' i ⊆ t

Proof state:
case intro.intro
α : Type u_1
ι : Sort u_4
ι' : Sort u_5
l : Filter α
p : ι → Prop
s : ι → Set α
p' : ι' → Prop
s' : ι' → Set α
hl : l.HasBasis p s
h : ∀ (i : ι), p i → ∃ i', p' i' ∧ s' i' ⊆ s i
h' : ∀ (i' : ι'), p' i' → s' i' ∈ l
t : Set α
ht✝ : t ∈ l
i : ι
hi : p i
ht : s i ⊆ t
⊢ ∃ i, p' i ∧ s' i ⊆ t

Tactic:
rcases h i hi with ⟨i', hi', hs's⟩

Result:
case intro.intro.intro.intro
α : Type u_1
ι : Sort u_4
ι' : Sort u_5
l : Filter α
p : ι → Prop
s : ι → Set α
p' : ι' → Prop
s' : ι' → Set α
hl : l.HasBasis p s
h : ∀ (i : ι), p i → ∃ i', p' i' ∧ s' i' ⊆ s i
h' : ∀ (i' : ι'), p' i' → s' i' ∈ l
t : Set α
ht✝ : t ∈ l
i : ι
hi : p i
ht : s i ⊆ t
i' : ι'
hi' : p' i'
hs's : s' i' ⊆ s i
⊢ ∃ i, p' i ∧ s' i ⊆ t

Proof state:
α : Type u_1
ι : Sort u_4
ι' : Sort u_5
l : Filter α
p : ι → Prop
s : ι → Set α
p' : ι' → Prop
s' : ι' → Set α
hl : l.HasBasis p s
h : ∀ (i : ι), p i → ∃ i', p' i' ∧ s' i' ⊆ s i
h' : ∀ (i' : ι'), p' i' → s' i' ∈ l
⊢ l.HasBasis p' s'

Tactic:
refine ⟨fun t => ⟨fun ht => ?_, fun ⟨i', hi', ht⟩ => mem_of_superset (h' i' hi') ht⟩⟩

Result:
α : Type u_1
ι : Sort u_4
ι' : Sort u_5
l : Filter α
p : ι → Prop
s : ι → Set α
p' : ι' → Prop
s' : ι' → Set α
hl : l.HasBasis p s
h : ∀ (i : ι), p i → ∃ i', p' i' ∧ s' i' ⊆ s i
h' : ∀ (i' : ι'), p' i' → s' i' ∈ l
t : Set α
ht : t ∈ l
⊢ ∃ i, p' i ∧ s' i ⊆ t
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Angle.lean
theorem sin_zero : sin (0 : Angle) = 0

Proof state:
⊢ sin 0 = 0

Tactic:
rw [← coe_zero, sin_coe, Real.sin_zero]

Result:
no goals
-- Mathlib/NumberTheory/LSeries/HurwitzZeta.lean
/-- Functional equation for the exponential zeta function. -/
lemma expZeta_one_sub (a : UnitAddCircle) {s : ℂ} (hs : ∀ (n : ℕ), s ≠ 1 - n) :
    expZeta a (1 - s) = (2 * π) ^ (-s) * Gamma s *
    (exp (π * I * s / 2) * hurwitzZeta a s + exp (-π * I * s / 2) * hurwitzZeta (-a) s)

Proof state:
a : UnitAddCircle
s : ℂ
hs : ∀ (n : ℕ), s ≠ 1 - ↑n
hs' : ∀ (n : ℕ), s ≠ -↑n
⊢ 2 * (2 * ↑π) ^ (-s) * Complex.Gamma s * ((cexp (↑π * s / 2 * I) + cexp (-(↑π * s / 2) * I)) / 2) *
        hurwitzZetaEven a s +
      I *
        (2 * (2 * ↑π) ^ (-s) * Complex.Gamma s * ((cexp (-(↑π * s / 2) * I) - cexp (↑π * s / 2 * I)) * I / 2) *
          hurwitzZetaOdd a s) =
    (2 * ↑π) ^ (-s) * Complex.Gamma s *
      (cexp (↑π * s / 2 * I) * (hurwitzZetaEven a s + hurwitzZetaOdd a s) +
        cexp (-(↑π * s / 2) * I) * (hurwitzZetaEven a s + -hurwitzZetaOdd a s))

Tactic:
generalize (2 * π : ℂ) ^ (-s) = x

Result:
a : UnitAddCircle
s : ℂ
hs : ∀ (n : ℕ), s ≠ 1 - ↑n
hs' : ∀ (n : ℕ), s ≠ -↑n
x : ℂ
⊢ 2 * x * Complex.Gamma s * ((cexp (↑π * s / 2 * I) + cexp (-(↑π * s / 2) * I)) / 2) * hurwitzZetaEven a s +
      I *
        (2 * x * Complex.Gamma s * ((cexp (-(↑π * s / 2) * I) - cexp (↑π * s / 2 * I)) * I / 2) * hurwitzZetaOdd a s) =
    x * Complex.Gamma s *
      (cexp (↑π * s / 2 * I) * (hurwitzZetaEven a s + hurwitzZetaOdd a s) +
        cexp (-(↑π * s / 2) * I) * (hurwitzZetaEven a s + -hurwitzZetaOdd a s))

Proof state:
case h.e'_3
a : UnitAddCircle
s : ℂ
hs : ∀ (n : ℕ), s ≠ 1 - ↑n
n : ℕ
⊢ -↑n = 1 - (↑n + 1)

Tactic:
ring

Result:
no goals

Proof state:
a : UnitAddCircle
s : ℂ
hs : ∀ (n : ℕ), s ≠ 1 - ↑n
hs' : ∀ (n : ℕ), s ≠ -↑n
⊢ 2 * (2 * ↑π) ^ (-s) * Complex.Gamma s * ((cexp (↑π * s / 2 * I) + cexp (-(↑π * s / 2) * I)) / 2) *
        hurwitzZetaEven a s +
      I *
        (2 * (2 * ↑π) ^ (-s) * Complex.Gamma s * ((cexp (-(↑π * s / 2) * I) - cexp (↑π * s / 2 * I)) * I / 2) *
          hurwitzZetaOdd a s) =
    (2 * ↑π) ^ (-s) * Complex.Gamma s *
      (cexp (↑π * I * s / 2) * (hurwitzZetaEven a s + hurwitzZetaOdd a s) +
        cexp (-↑π * I * s / 2) * (hurwitzZetaEven a s + -hurwitzZetaOdd a s))

Tactic:
rw [show ↑π * I * s / 2 = ↑π * s / 2 * I by ring,
  show -↑π * I * s / 2 = -(↑π * s / 2) * I by ring]

Result:
a : UnitAddCircle
s : ℂ
hs : ∀ (n : ℕ), s ≠ 1 - ↑n
hs' : ∀ (n : ℕ), s ≠ -↑n
⊢ 2 * (2 * ↑π) ^ (-s) * Complex.Gamma s * ((cexp (↑π * s / 2 * I) + cexp (-(↑π * s / 2) * I)) / 2) *
        hurwitzZetaEven a s +
      I *
        (2 * (2 * ↑π) ^ (-s) * Complex.Gamma s * ((cexp (-(↑π * s / 2) * I) - cexp (↑π * s / 2 * I)) * I / 2) *
          hurwitzZetaOdd a s) =
    (2 * ↑π) ^ (-s) * Complex.Gamma s *
      (cexp (↑π * s / 2 * I) * (hurwitzZetaEven a s + hurwitzZetaOdd a s) +
        cexp (-(↑π * s / 2) * I) * (hurwitzZetaEven a s + -hurwitzZetaOdd a s))
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Erase.lean
theorem erase_eq_eraseP' (a : α) (l : List α) : l.erase a = l.eraseP (· == a)

Proof state:
case nil
α : Type u_1
inst✝ : BEq α
a : α
⊢ [].erase a = eraseP (fun x => x == a) []

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
inst✝ : BEq α
a b : α
t : List α
ih : t.erase a = eraseP (fun x => x == a) t
⊢ (b :: t).erase a = eraseP (fun x => x == a) (b :: t)

Tactic:
rw [erase_cons, eraseP_cons, ih]

Result:
α : Type u_1
inst✝ : BEq α
a b : α
t : List α
ih : t.erase a = eraseP (fun x => x == a) t
⊢ (if (b == a) = true then t else b :: eraseP (fun x => x == a) t) =
    bif b == a then t else b :: eraseP (fun x => x == a) t

Proof state:
case cons
α : Type u_1
inst✝ : BEq α
a head✝ : α
tail✝ : List α
tail_ih✝ : tail✝.erase a = eraseP (fun x => x == a) tail✝
⊢ (head✝ :: tail✝).erase a = eraseP (fun x => x == a) (head✝ :: tail✝)

Tactic:
next b t ih =>
rw [erase_cons, eraseP_cons, ih]
if h : b == a then simp [h] else simp [h]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : BEq α
a b : α
t : List α
ih : t.erase a = eraseP (fun x => x == a) t
h : (b == a) = true
⊢ (if (b == a) = true then t else b :: eraseP (fun x => x == a) t) =
    bif b == a then t else b :: eraseP (fun x => x == a) t

Tactic:
simp [h]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : BEq α
a b : α
t : List α
ih : t.erase a = eraseP (fun x => x == a) t
h : ¬(b == a) = true
⊢ (if (b == a) = true then t else b :: eraseP (fun x => x == a) t) =
    bif b == a then t else b :: eraseP (fun x => x == a) t

Tactic:
simp [h]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : BEq α
a : α
l : List α
⊢ l.erase a = eraseP (fun x => x == a) l

Tactic:
induction l

Result:
case nil
α : Type u_1
inst✝ : BEq α
a : α
⊢ [].erase a = eraseP (fun x => x == a) []

case cons
α : Type u_1
inst✝ : BEq α
a head✝ : α
tail✝ : List α
tail_ih✝ : tail✝.erase a = eraseP (fun x => x == a) tail✝
⊢ (head✝ :: tail✝).erase a = eraseP (fun x => x == a) (head✝ :: tail✝)

Proof state:
α : Type u_1
inst✝ : BEq α
a b : α
t : List α
ih : t.erase a = eraseP (fun x => x == a) t
⊢ (if (b == a) = true then t else b :: eraseP (fun x => x == a) t) =
    bif b == a then t else b :: eraseP (fun x => x == a) t

Tactic:
if h : b == a then simp [h] else simp [h]

Result:
no goals
-- Mathlib/NumberTheory/ArithmeticFunction.lean
theorem zeta_mul_pow_eq_sigma {k : ℕ} : ζ * pow k = σ k

Proof state:
k : ℕ
⊢ ζ * pow k = σ k

Tactic:
ext

Result:
case h
k x✝ : ℕ
⊢ (ζ * pow k) x✝ = (σ k) x✝

Proof state:
case h
k x✝ : ℕ
⊢ ∑ i ∈ x✝.divisors, (pow k) i = { toFun := fun n => ∑ d ∈ n.divisors, d ^ k, map_zero' := ⋯ } x✝

Tactic:
apply sum_congr rfl

Result:
case h
k x✝ : ℕ
⊢ ∀ x ∈ x✝.divisors, (pow k) x = x ^ k

Proof state:
case h
k x✝ : ℕ
⊢ ∀ x ∈ x✝.divisors, (pow k) x = x ^ k

Tactic:
intro x hx

Result:
case h
k x✝ x : ℕ
hx : x ∈ x✝.divisors
⊢ (pow k) x = x ^ k

Proof state:
case h
k x✝ : ℕ
⊢ (ζ * pow k) x✝ = (σ k) x✝

Tactic:
rw [sigma, zeta_mul_apply]

Result:
case h
k x✝ : ℕ
⊢ ∑ i ∈ x✝.divisors, (pow k) i = { toFun := fun n => ∑ d ∈ n.divisors, d ^ k, map_zero' := ⋯ } x✝

Proof state:
k x✝ x : ℕ
hx : x = 0
⊢ x ∉ x✝.divisors

Tactic:
simp [hx]

Result:
no goals

Proof state:
k x✝ x : ℕ
hx : x ∈ x✝.divisors
⊢ ¬x = 0

Tactic:
contrapose! hx

Result:
k x✝ x : ℕ
hx : x = 0
⊢ x ∉ x✝.divisors

Proof state:
case h
k x✝ x : ℕ
hx : x ∈ x✝.divisors
⊢ (pow k) x = x ^ k

Tactic:
rw [pow_apply, if_neg (not_and_of_not_right _ _)]

Result:
k x✝ x : ℕ
hx : x ∈ x✝.divisors
⊢ ¬x = 0
-- Mathlib/Data/Bool/Count.lean
theorem two_mul_count_bool_le_length_add_one (hl : Chain' (· ≠ ·) l) (b : Bool) :
    2 * count b l ≤ length l + 1

Proof state:
l : List Bool
hl : Chain' (fun x1 x2 => x1 ≠ x2) l
b : Bool
⊢ (if Even l.length then l.length else if (some b == l.head?) = true then l.length + 1 else l.length - 1) ≤ l.length + 1

Tactic:
split_ifs <;> simp [Nat.le_succ_of_le]

Result:
no goals

Proof state:
l : List Bool
hl : Chain' (fun x1 x2 => x1 ≠ x2) l
b : Bool
⊢ 2 * count b l ≤ l.length + 1

Tactic:
rw [hl.two_mul_count_bool_eq_ite]

Result:
l : List Bool
hl : Chain' (fun x1 x2 => x1 ≠ x2) l
b : Bool
⊢ (if Even l.length then l.length else if (some b == l.head?) = true then l.length + 1 else l.length - 1) ≤ l.length + 1
-- Mathlib/Algebra/Polynomial/Degree/Operations.lean
@[simp] lemma natDegree_mul_X (hp : p ≠ 0) : natDegree (p * X) = natDegree p + 1

Proof state:
R : Type u
inst✝¹ : Semiring R
inst✝ : Nontrivial R
p : R[X]
hp : p ≠ 0
⊢ (p * X).natDegree = p.natDegree + 1

Tactic:
rw [natDegree_mul' (by simpa), natDegree_X]

Result:
no goals

Proof state:
R : Type u
inst✝¹ : Semiring R
inst✝ : Nontrivial R
p : R[X]
hp : p ≠ 0
⊢ p.leadingCoeff * X.leadingCoeff ≠ 0

Tactic:
simpa

Result:
no goals
-- Mathlib/Algebra/MvPolynomial/Rename.lean
theorem eval₂_cast_comp (f : σ → τ) (c : ℤ →+* R) (g : τ → R) (p : MvPolynomial σ ℤ) :
    eval₂ c (g ∘ f) p = eval₂ c g (rename f p)

Proof state:
σ : Type u_1
τ : Type u_2
R : Type u_4
inst✝ : CommSemiring R
f : σ → τ
c : ℤ →+* R
g : τ → R
p✝ p : MvPolynomial σ ℤ
n : σ
hp : eval₂ c (g ∘ f) p = eval₂ c g ((rename f) p)
⊢ eval₂ c (g ∘ f) (p * X n) = eval₂ c g ((rename f) (p * X n))

Tactic:
simp only [eval₂_mul, hp, eval₂_X, comp_apply, map_mul, rename_X, eval₂_mul]

Result:
no goals

Proof state:
σ : Type u_1
τ : Type u_2
R : Type u_4
inst✝ : CommSemiring R
f : σ → τ
c : ℤ →+* R
g : τ → R
p : MvPolynomial σ ℤ
n : ℤ
⊢ eval₂ c (g ∘ f) (C n) = eval₂ c g ((rename f) (C n))

Tactic:
simp only [eval₂_C, rename_C]

Result:
no goals

Proof state:
σ : Type u_1
τ : Type u_2
R : Type u_4
inst✝ : CommSemiring R
f : σ → τ
c : ℤ →+* R
g : τ → R
p : MvPolynomial σ ℤ
⊢ eval₂ c (g ∘ f) p = eval₂ c g ((rename f) p)

Tactic:
apply MvPolynomial.induction_on p (fun n => by simp only [eval₂_C, rename_C])
  (fun p q hp hq => by simp only [hp, hq, rename, eval₂_add, map_add])
  fun p n hp => by simp only [eval₂_mul, hp, eval₂_X, comp_apply, map_mul, rename_X, eval₂_mul]

Result:
no goals

Proof state:
σ : Type u_1
τ : Type u_2
R : Type u_4
inst✝ : CommSemiring R
f : σ → τ
c : ℤ →+* R
g : τ → R
p✝ p q : MvPolynomial σ ℤ
hp : eval₂ c (g ∘ f) p = eval₂ c g ((rename f) p)
hq : eval₂ c (g ∘ f) q = eval₂ c g ((rename f) q)
⊢ eval₂ c (g ∘ f) (p + q) = eval₂ c g ((rename f) (p + q))

Tactic:
simp only [hp, hq, rename, eval₂_add, map_add]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Stieltjes.lean
theorem measure_Iic {l : ℝ} (hf : Tendsto f atBot (𝓝 l)) (x : ℝ) :
    f.measure (Iic x) = ofReal (f x - l)

Proof state:
f : StieltjesFunction
l : ℝ
hf : Tendsto (↑f) atBot (𝓝 l)
x : ℝ
⊢ Tendsto (fun x_1 => ofReal (↑f x - ↑f x_1)) atBot (𝓝 (ofReal (↑f x - l)))

Tactic:
exact ENNReal.tendsto_ofReal (Tendsto.const_sub _ hf)

Result:
no goals

Proof state:
f : StieltjesFunction
l : ℝ
hf : Tendsto (↑f) atBot (𝓝 l)
x : ℝ
⊢ f.measure (Iic x) = ofReal (↑f x - l)

Tactic:
refine tendsto_nhds_unique (tendsto_measure_Ioc_atBot _ _) ?_

Result:
f : StieltjesFunction
l : ℝ
hf : Tendsto (↑f) atBot (𝓝 l)
x : ℝ
⊢ Tendsto (fun x_1 => f.measure (Ioc x_1 x)) atBot (𝓝 (ofReal (↑f x - l)))

Proof state:
f : StieltjesFunction
l : ℝ
hf : Tendsto (↑f) atBot (𝓝 l)
x : ℝ
⊢ Tendsto (fun x_1 => f.measure (Ioc x_1 x)) atBot (𝓝 (ofReal (↑f x - l)))

Tactic:
simp_rw [measure_Ioc]

Result:
f : StieltjesFunction
l : ℝ
hf : Tendsto (↑f) atBot (𝓝 l)
x : ℝ
⊢ Tendsto (fun x_1 => ofReal (↑f x - ↑f x_1)) atBot (𝓝 (ofReal (↑f x - l)))
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/LRAT/Internal/Entails.lean
theorem limplies_unsat {α : Type u} {σ1 : Type v} {σ2 : Type w} [Entails α σ1] [Entails α σ2]
    (f1 : σ1) (f2 : σ2) (h : Limplies α f2 f1) :
    Unsatisfiable α f1 → Unsatisfiable α f2

Proof state:
α : Type u
σ1 : Type v
σ2 : Type w
inst✝¹ : Entails α σ1
inst✝ : Entails α σ2
f1 : σ1
f2 : σ2
h : Limplies α f2 f1
⊢ Unsatisfiable α f1 → Unsatisfiable α f2

Tactic:
intros f1_unsat a a_entails_f2

Result:
α : Type u
σ1 : Type v
σ2 : Type w
inst✝¹ : Entails α σ1
inst✝ : Entails α σ2
f1 : σ1
f2 : σ2
h : Limplies α f2 f1
f1_unsat : Unsatisfiable α f1
a : α → Bool
a_entails_f2 : a ⊨ f2
⊢ False

Proof state:
α : Type u
σ1 : Type v
σ2 : Type w
inst✝¹ : Entails α σ1
inst✝ : Entails α σ2
f1 : σ1
f2 : σ2
h : Limplies α f2 f1
f1_unsat : Unsatisfiable α f1
a : α → Bool
a_entails_f2 : a ⊨ f2
⊢ False

Tactic:
exact f1_unsat a <| h a a_entails_f2

Result:
no goals
-- Mathlib/Algebra/Polynomial/Laurent.lean
theorem leftInverse_trunc_toLaurent :
    Function.LeftInverse (trunc : R[T;T⁻¹] → R[X]) Polynomial.toLaurent

Proof state:
case refine_1
R : Type u_1
inst✝ : Semiring R
f✝ f g : R[X]
hf : trunc (toLaurent f) = f
hg : trunc (toLaurent g) = g
⊢ trunc (toLaurent (f + g)) = f + g

Tactic:
simp only [hf, hg, _root_.map_add]

Result:
no goals

Proof state:
R : Type u_1
inst✝ : Semiring R
⊢ LeftInverse ⇑trunc ⇑toLaurent

Tactic:
refine fun f => f.induction_on' ?_ ?_

Result:
case refine_1
R : Type u_1
inst✝ : Semiring R
f : R[X]
⊢ ∀ (p q : R[X]), trunc (toLaurent p) = p → trunc (toLaurent q) = q → trunc (toLaurent (p + q)) = p + q

case refine_2
R : Type u_1
inst✝ : Semiring R
f : R[X]
⊢ ∀ (n : ℕ) (a : R), trunc (toLaurent ((monomial n) a)) = (monomial n) a

Proof state:
case refine_1
R : Type u_1
inst✝ : Semiring R
f : R[X]
⊢ ∀ (p q : R[X]), trunc (toLaurent p) = p → trunc (toLaurent q) = q → trunc (toLaurent (p + q)) = p + q

Tactic:
intro f g hf hg

Result:
case refine_1
R : Type u_1
inst✝ : Semiring R
f✝ f g : R[X]
hf : trunc (toLaurent f) = f
hg : trunc (toLaurent g) = g
⊢ trunc (toLaurent (f + g)) = f + g

Proof state:
case refine_2
R : Type u_1
inst✝ : Semiring R
f : R[X]
n : ℕ
r : R
⊢ trunc (toLaurent ((monomial n) r)) = (monomial n) r

Tactic:
simp only [Polynomial.toLaurent_C_mul_T, trunc_C_mul_T, Int.natCast_nonneg, Int.toNat_natCast,
  if_true]

Result:
no goals

Proof state:
case refine_2
R : Type u_1
inst✝ : Semiring R
f : R[X]
⊢ ∀ (n : ℕ) (a : R), trunc (toLaurent ((monomial n) a)) = (monomial n) a

Tactic:
intro n r

Result:
case refine_2
R : Type u_1
inst✝ : Semiring R
f : R[X]
n : ℕ
r : R
⊢ trunc (toLaurent ((monomial n) r)) = (monomial n) r
-- Mathlib/Probability/Kernel/Disintegration/MeasurableStieltjes.lean
lemma IsMeasurableRatCDF.stieltjesFunction_le_one (a : α) (x : ℝ) :
    hf.stieltjesFunction a x ≤ 1

Proof state:
case intro
α : Type u_1
f : α → ℚ → ℝ
inst✝ : MeasurableSpace α
hf : IsMeasurableRatCDF f
a : α
x : ℝ
r : ℚ
hrx : x < ↑r
⊢ ⨅ r, ↑(hf.stieltjesFunction a) ↑↑r ≤ 1

Tactic:
simp_rw [IsMeasurableRatCDF.stieltjesFunction_eq]

Result:
case intro
α : Type u_1
f : α → ℚ → ℝ
inst✝ : MeasurableSpace α
hf : IsMeasurableRatCDF f
a : α
x : ℝ
r : ℚ
hrx : x < ↑r
⊢ ⨅ r, f a ↑r ≤ 1

Proof state:
case intro
α : Type u_1
f : α → ℚ → ℝ
inst✝ : MeasurableSpace α
hf : IsMeasurableRatCDF f
a : α
x : ℝ
r : ℚ
hrx : x < ↑r
⊢ ⨅ r, f a ↑r ≤ 1

Tactic:
refine ciInf_le_of_le ?_ ?_ (hf.le_one _ _)

Result:
case intro.refine_1
α : Type u_1
f : α → ℚ → ℝ
inst✝ : MeasurableSpace α
hf : IsMeasurableRatCDF f
a : α
x : ℝ
r : ℚ
hrx : x < ↑r
⊢ BddBelow (range fun r => f a ↑r)

case intro.refine_2
α : Type u_1
f : α → ℚ → ℝ
inst✝ : MeasurableSpace α
hf : IsMeasurableRatCDF f
a : α
x : ℝ
r : ℚ
hrx : x < ↑r
⊢ { r' // x < ↑r' }

Proof state:
case intro.refine_1.intro
α : Type u_1
f : α → ℚ → ℝ
inst✝ : MeasurableSpace α
hf : IsMeasurableRatCDF f
a : α
x : ℝ
r : ℚ
hrx : x < ↑r
u : { r' // x < ↑r' }
⊢ 0 ≤ (fun r => f a ↑r) u

Tactic:
exact hf.nonneg a _

Result:
no goals

Proof state:
case intro.refine_1
α : Type u_1
f : α → ℚ → ℝ
inst✝ : MeasurableSpace α
hf : IsMeasurableRatCDF f
a : α
x : ℝ
r : ℚ
hrx : x < ↑r
z : ℝ
⊢ (z ∈ range fun r => f a ↑r) → 0 ≤ z

Tactic:
rintro ⟨u, rfl⟩

Result:
case intro.refine_1.intro
α : Type u_1
f : α → ℚ → ℝ
inst✝ : MeasurableSpace α
hf : IsMeasurableRatCDF f
a : α
x : ℝ
r : ℚ
hrx : x < ↑r
u : { r' // x < ↑r' }
⊢ 0 ≤ (fun r => f a ↑r) u

Proof state:
case intro.refine_2
α : Type u_1
f : α → ℚ → ℝ
inst✝ : MeasurableSpace α
hf : IsMeasurableRatCDF f
a : α
x : ℝ
r : ℚ
hrx : x < ↑r
⊢ { r' // x < ↑r' }

Tactic:
exact ⟨r, hrx⟩

Result:
no goals

Proof state:
case intro.refine_1
α : Type u_1
f : α → ℚ → ℝ
inst✝ : MeasurableSpace α
hf : IsMeasurableRatCDF f
a : α
x : ℝ
r : ℚ
hrx : x < ↑r
⊢ BddBelow (range fun r => f a ↑r)

Tactic:
refine ⟨0, fun z ↦ ?_⟩

Result:
case intro.refine_1
α : Type u_1
f : α → ℚ → ℝ
inst✝ : MeasurableSpace α
hf : IsMeasurableRatCDF f
a : α
x : ℝ
r : ℚ
hrx : x < ↑r
z : ℝ
⊢ (z ∈ range fun r => f a ↑r) → 0 ≤ z

Proof state:
α : Type u_1
f : α → ℚ → ℝ
inst✝ : MeasurableSpace α
hf : IsMeasurableRatCDF f
a : α
x : ℝ
⊢ ↑(hf.stieltjesFunction a) x ≤ 1

Tactic:
obtain ⟨r, hrx⟩ := exists_rat_gt x

Result:
case intro
α : Type u_1
f : α → ℚ → ℝ
inst✝ : MeasurableSpace α
hf : IsMeasurableRatCDF f
a : α
x : ℝ
r : ℚ
hrx : x < ↑r
⊢ ↑(hf.stieltjesFunction a) x ≤ 1

Proof state:
case intro
α : Type u_1
f : α → ℚ → ℝ
inst✝ : MeasurableSpace α
hf : IsMeasurableRatCDF f
a : α
x : ℝ
r : ℚ
hrx : x < ↑r
⊢ ↑(hf.stieltjesFunction a) x ≤ 1

Tactic:
rw [← StieltjesFunction.iInf_rat_gt_eq]

Result:
case intro
α : Type u_1
f : α → ℚ → ℝ
inst✝ : MeasurableSpace α
hf : IsMeasurableRatCDF f
a : α
x : ℝ
r : ℚ
hrx : x < ↑r
⊢ ⨅ r, ↑(hf.stieltjesFunction a) ↑↑r ≤ 1
-- Mathlib/Combinatorics/SetFamily/FourFunctions.lean
private lemma erase_eq_iff (hs : a ∉ s) : t.erase a = s ↔ t = s ∨ t = insert a s

Proof state:
case neg
α : Type u_1
inst✝ : DecidableEq α
a : α
s t : Finset α
hs : a ∉ s
ht : a ∉ t
⊢ t = insert a s → t = s

Tactic:
aesop

Result:
no goals

Proof state:
case neg
α : Type u_1
inst✝ : DecidableEq α
a : α
s t : Finset α
hs : a ∉ s
ht : a ∉ t
⊢ t.erase a = s ↔ t = s ∨ t = insert a s

Tactic:
simp [ne_of_mem_of_not_mem', erase_eq_iff_eq_insert, *]

Result:
case neg
α : Type u_1
inst✝ : DecidableEq α
a : α
s t : Finset α
hs : a ∉ s
ht : a ∉ t
⊢ t = insert a s → t = s
-- Mathlib/RingTheory/HahnSeries/Basic.lean
theorem coeff_orderTop_ne {x : HahnSeries Γ R} {g : Γ} (hg : x.orderTop = g) :
    x.coeff g ≠ 0

Proof state:
Γ : Type u_1
R : Type u_3
inst✝¹ : PartialOrder Γ
inst✝ : Zero R
x : HahnSeries Γ R
g : Γ
h : x.orderTop ≠ ⊤
hx : x ≠ 0
hg : ⋯.min ⋯ = g
⊢ x.coeff g ≠ 0

Tactic:
rw [← hg]

Result:
Γ : Type u_1
R : Type u_3
inst✝¹ : PartialOrder Γ
inst✝ : Zero R
x : HahnSeries Γ R
g : Γ
h : x.orderTop ≠ ⊤
hx : x ≠ 0
hg : ⋯.min ⋯ = g
⊢ x.coeff (⋯.min ⋯) ≠ 0

Proof state:
Γ : Type u_1
R : Type u_3
inst✝¹ : PartialOrder Γ
inst✝ : Zero R
x : HahnSeries Γ R
g : Γ
hg : x.orderTop = ↑g
h : x.orderTop ≠ ⊤
hx : x ≠ 0
⊢ x.coeff g ≠ 0

Tactic:
rw [orderTop_of_ne hx, WithTop.coe_eq_coe] at hg

Result:
Γ : Type u_1
R : Type u_3
inst✝¹ : PartialOrder Γ
inst✝ : Zero R
x : HahnSeries Γ R
g : Γ
h : x.orderTop ≠ ⊤
hx : x ≠ 0
hg : ⋯.min ⋯ = g
⊢ x.coeff g ≠ 0

Proof state:
Γ : Type u_1
R : Type u_3
inst✝¹ : PartialOrder Γ
inst✝ : Zero R
x : HahnSeries Γ R
g : Γ
hg : x.orderTop = ↑g
h : x.orderTop ≠ ⊤
⊢ x.coeff g ≠ 0

Tactic:
have hx : x ≠ 0 := ne_zero_iff_orderTop.mpr h

Result:
Γ : Type u_1
R : Type u_3
inst✝¹ : PartialOrder Γ
inst✝ : Zero R
x : HahnSeries Γ R
g : Γ
hg : x.orderTop = ↑g
h : x.orderTop ≠ ⊤
hx : x ≠ 0
⊢ x.coeff g ≠ 0

Proof state:
Γ : Type u_1
R : Type u_3
inst✝¹ : PartialOrder Γ
inst✝ : Zero R
x : HahnSeries Γ R
g : Γ
hg : x.orderTop = ↑g
⊢ x.coeff g ≠ 0

Tactic:
have h : orderTop x ≠ ⊤ := by simp_all only [ne_eq, WithTop.coe_ne_top, not_false_eq_true]

Result:
Γ : Type u_1
R : Type u_3
inst✝¹ : PartialOrder Γ
inst✝ : Zero R
x : HahnSeries Γ R
g : Γ
hg : x.orderTop = ↑g
h : x.orderTop ≠ ⊤
⊢ x.coeff g ≠ 0

Proof state:
Γ : Type u_1
R : Type u_3
inst✝¹ : PartialOrder Γ
inst✝ : Zero R
x : HahnSeries Γ R
g : Γ
h : x.orderTop ≠ ⊤
hx : x ≠ 0
hg : ⋯.min ⋯ = g
⊢ x.coeff (⋯.min ⋯) ≠ 0

Tactic:
exact x.isWF_support.min_mem (support_nonempty_iff.2 hx)

Result:
no goals

Proof state:
Γ : Type u_1
R : Type u_3
inst✝¹ : PartialOrder Γ
inst✝ : Zero R
x : HahnSeries Γ R
g : Γ
hg : x.orderTop = ↑g
⊢ x.orderTop ≠ ⊤

Tactic:
simp_all only [ne_eq, WithTop.coe_ne_top, not_false_eq_true]

Result:
no goals