harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/MeasureTheory/Integral/IntervalIntegral.lean
theorem _root_.MeasureTheory.Integrable.hasSum_intervalIntegral (hfi : Integrable f μ) (y : ℝ) :
    HasSum (fun n : ℤ => ∫ x in y + n..y + n + 1, f x ∂μ) (∫ x, f x ∂μ)

Proof state:
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
μ : Measure ℝ
f : ℝ → E
hfi : Integrable f μ
y : ℝ
⊢ HasSum (fun n => ∫ (x : ℝ) in Ioc (y + ↑n) (y + ↑n + 1), f x ∂μ) (∫ (x : ℝ) in ⋃ n, Ioc (y + ↑n) (y + ↑n + 1), f x ∂μ)

Tactic:
exact
  hasSum_integral_iUnion (fun i => measurableSet_Ioc) (pairwise_disjoint_Ioc_add_intCast y)
    hfi.integrableOn

Result:
no goals

Proof state:
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
μ : Measure ℝ
f : ℝ → E
hfi : Integrable f μ
y : ℝ
⊢ HasSum (fun n => ∫ (x : ℝ) in Ioc (y + ↑n) (y + ↑n + 1), f x ∂μ) (∫ (x : ℝ), f x ∂μ)

Tactic:
rw [← setIntegral_univ, ← iUnion_Ioc_add_intCast y]

Result:
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
μ : Measure ℝ
f : ℝ → E
hfi : Integrable f μ
y : ℝ
⊢ HasSum (fun n => ∫ (x : ℝ) in Ioc (y + ↑n) (y + ↑n + 1), f x ∂μ) (∫ (x : ℝ) in ⋃ n, Ioc (y + ↑n) (y + ↑n + 1), f x ∂μ)

Proof state:
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
μ : Measure ℝ
f : ℝ → E
hfi : Integrable f μ
y : ℝ
⊢ HasSum (fun n => ∫ (x : ℝ) in y + ↑n..y + ↑n + 1, f x ∂μ) (∫ (x : ℝ), f x ∂μ)

Tactic:
simp_rw [integral_of_le (le_add_of_nonneg_right zero_le_one)]

Result:
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
μ : Measure ℝ
f : ℝ → E
hfi : Integrable f μ
y : ℝ
⊢ HasSum (fun n => ∫ (x : ℝ) in Ioc (y + ↑n) (y + ↑n + 1), f x ∂μ) (∫ (x : ℝ), f x ∂μ)
-- Mathlib/MeasureTheory/Constructions/Cylinders.lean
theorem diff_mem_measurableCylinders (hs : s ∈ measurableCylinders α)
    (ht : t ∈ measurableCylinders α) :
    s \ t ∈ measurableCylinders α

Proof state:
ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → MeasurableSpace (α i)
s t : Set ((i : ι) → α i)
hs : s ∈ measurableCylinders α
ht : t ∈ measurableCylinders α
⊢ s \ t ∈ measurableCylinders α

Tactic:
rw [diff_eq_compl_inter]

Result:
ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → MeasurableSpace (α i)
s t : Set ((i : ι) → α i)
hs : s ∈ measurableCylinders α
ht : t ∈ measurableCylinders α
⊢ tᶜ ∩ s ∈ measurableCylinders α

Proof state:
ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → MeasurableSpace (α i)
s t : Set ((i : ι) → α i)
hs : s ∈ measurableCylinders α
ht : t ∈ measurableCylinders α
⊢ tᶜ ∩ s ∈ measurableCylinders α

Tactic:
exact inter_mem_measurableCylinders (compl_mem_measurableCylinders ht) hs

Result:
no goals
-- Mathlib/Analysis/Normed/Field/Basic.lean
theorem NormedAddCommGroup.tendsto_atTop [Nonempty α] [Preorder α] [IsDirected α (· ≤ ·)]
    {β : Type*} [SeminormedAddCommGroup β] {f : α → β} {b : β} :
    Tendsto f atTop (𝓝 b) ↔ ∀ ε, 0 < ε → ∃ N, ∀ n, N ≤ n → ‖f n - b‖ < ε :=
  (atTop_basis.tendsto_iff Metric.nhds_basis_ball).trans (by simp [dist_eq_norm])

Proof state:
α : Type u_2
inst✝³ : Nonempty α
inst✝² : Preorder α
inst✝¹ : IsDirected α fun x1 x2 => x1 ≤ x2
β : Type u_5
inst✝ : SeminormedAddCommGroup β
f : α → β
b : β
⊢ (∀ (ib : ℝ), 0 < ib → ∃ ia, True ∧ ∀ x ∈ Set.Ici ia, f x ∈ Metric.ball b ib) ↔
    ∀ (ε : ℝ), 0 < ε → ∃ N, ∀ (n : α), N ≤ n → ‖f n - b‖ < ε

Tactic:
simp [dist_eq_norm]

Result:
no goals
-- Mathlib/GroupTheory/Index.lean
@[to_additive]
lemma index_eq_zero_iff_infinite : H.index = 0 ↔ Infinite (G ⧸ H)

Proof state:
G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ H.index = 0 ↔ Infinite (G ⧸ H)

Tactic:
simp [index_eq_card, Nat.card_eq_zero]

Result:
no goals
-- Mathlib/Data/Matroid/Basic.lean
theorem Indep.isBase_of_forall_insert (hB : M.Indep B)
    (hBmax : ∀ e ∈ M.E \ B, ¬ M.Indep (insert e B)) : M.IsBase B

Proof state:
α : Type u_1
M : Matroid α
B : Set α
hB : M.Indep B
hBmax : ∀ e ∈ M.E \ B, ¬M.Indep (insert e B)
⊢ M.IsBase B

Tactic:
refine by_contra fun hnb ↦ ?_

Result:
α : Type u_1
M : Matroid α
B : Set α
hB : M.Indep B
hBmax : ∀ e ∈ M.E \ B, ¬M.Indep (insert e B)
hnb : ¬M.IsBase B
⊢ False

Proof state:
case intro
α : Type u_1
M : Matroid α
B : Set α
hB : M.Indep B
hBmax : ∀ e ∈ M.E \ B, ¬M.Indep (insert e B)
hnb : ¬M.IsBase B
B' : Set α
hB' : M.IsBase B'
⊢ False

Tactic:
obtain ⟨e, he, h⟩ := hB.exists_insert_of_not_isBase hnb hB'

Result:
case intro.intro.intro
α : Type u_1
M : Matroid α
B : Set α
hB : M.Indep B
hBmax : ∀ e ∈ M.E \ B, ¬M.Indep (insert e B)
hnb : ¬M.IsBase B
B' : Set α
hB' : M.IsBase B'
e : α
he : e ∈ B' \ B
h : M.Indep (insert e B)
⊢ False

Proof state:
α : Type u_1
M : Matroid α
B : Set α
hB : M.Indep B
hBmax : ∀ e ∈ M.E \ B, ¬M.Indep (insert e B)
hnb : ¬M.IsBase B
⊢ False

Tactic:
obtain ⟨B', hB'⟩ := M.exists_isBase

Result:
case intro
α : Type u_1
M : Matroid α
B : Set α
hB : M.Indep B
hBmax : ∀ e ∈ M.E \ B, ¬M.Indep (insert e B)
hnb : ¬M.IsBase B
B' : Set α
hB' : M.IsBase B'
⊢ False

Proof state:
case intro.intro.intro
α : Type u_1
M : Matroid α
B : Set α
hB : M.Indep B
hBmax : ∀ e ∈ M.E \ B, ¬M.Indep (insert e B)
hnb : ¬M.IsBase B
B' : Set α
hB' : M.IsBase B'
e : α
he : e ∈ B' \ B
h : M.Indep (insert e B)
⊢ False

Tactic:
exact hBmax e ⟨hB'.subset_ground he.1, he.2⟩ h

Result:
no goals
-- Mathlib/Order/Filter/AtTopBot/Archimedean.lean
theorem tendsto_ratCast_atTop_iff [LinearOrderedField R] [Archimedean R] {f : α → ℚ}
    {l : Filter α} : Tendsto (fun n => (f n : R)) l atTop ↔ Tendsto f l atTop

Proof state:
α : Type u_1
R : Type u_2
inst✝¹ : LinearOrderedField R
inst✝ : Archimedean R
f : α → ℚ
l : Filter α
⊢ Tendsto (fun n => ↑(f n)) l atTop ↔ Tendsto f l atTop

Tactic:
rw [← @Rat.comap_cast_atTop R, tendsto_comap_iff]

Result:
α : Type u_1
R : Type u_2
inst✝¹ : LinearOrderedField R
inst✝ : Archimedean R
f : α → ℚ
l : Filter α
⊢ Tendsto (fun n => ↑(f n)) l atTop ↔ Tendsto (Rat.cast ∘ f) l atTop

Proof state:
α : Type u_1
R : Type u_2
inst✝¹ : LinearOrderedField R
inst✝ : Archimedean R
f : α → ℚ
l : Filter α
⊢ Tendsto (fun n => ↑(f n)) l atTop ↔ Tendsto (Rat.cast ∘ f) l atTop

Tactic:
rfl

Result:
no goals
-- Mathlib/Analysis/BoxIntegral/Partition/Basic.lean
theorem mem_iUnion : x ∈ π.iUnion ↔ ∃ J ∈ π, x ∈ J

Proof state:
case h.e'_2.h.e'_2.h.a
ι : Type u_1
I : Box ι
π : Prepartition I
x : ι → ℝ
x✝ : Box ι
⊢ x✝ ∈ π ∧ x ∈ x✝ ↔ ∃ (_ : x✝ ∈ π), x ∈ ↑x✝

Tactic:
rw [Box.mem_coe, exists_prop]

Result:
no goals

Proof state:
ι : Type u_1
I : Box ι
π : Prepartition I
x : ι → ℝ
⊢ x ∈ π.iUnion ↔ ∃ J ∈ π, x ∈ J

Tactic:
convert Set.mem_iUnion₂

Result:
case h.e'_2.h.e'_2.h.a
ι : Type u_1
I : Box ι
π : Prepartition I
x : ι → ℝ
x✝ : Box ι
⊢ x✝ ∈ π ∧ x ∈ x✝ ↔ ∃ (_ : x✝ ∈ π), x ∈ ↑x✝
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Lemmas.lean
theorem mul_mul_mul_comm (a b c d : Nat) : (a * b) * (c * d) = (a * c) * (b * d)

Proof state:
a b c d : Nat
⊢ a * b * (c * d) = a * c * (b * d)

Tactic:
rw [Nat.mul_assoc, Nat.mul_assoc, Nat.mul_left_comm b]

Result:
no goals
-- Mathlib/MeasureTheory/MeasurableSpace/Defs.lean
theorem generateFrom_singleton_empty : generateFrom {∅} = (⊥ : MeasurableSpace α) :=
  bot_unique <| generateFrom_le <| by simp [@MeasurableSet.empty α ⊥]

Proof state:
α : Type u_1
⊢ ∀ t ∈ {∅}, MeasurableSet t

Tactic:
simp [@MeasurableSet.empty α ⊥]

Result:
no goals
-- Mathlib/MeasureTheory/Group/Measure.lean
theorem eventually_mul_right_iff (μ : Measure G) [IsMulRightInvariant μ] (t : G) {p : G → Prop} :
    (∀ᵐ x ∂μ, p (x * t)) ↔ ∀ᵐ x ∂μ, p x

Proof state:
G : Type u_1
inst✝³ : MeasurableSpace G
inst✝² : Group G
inst✝¹ : MeasurableMul G
μ : Measure G
inst✝ : μ.IsMulRightInvariant
t : G
p : G → Prop
⊢ (∀ᵐ (x : G) ∂μ, p (x * t)) ↔ {x | p x} ∈ Filter.map (fun h => h * t) (ae μ)

Tactic:
rfl

Result:
no goals

Proof state:
G : Type u_1
inst✝³ : MeasurableSpace G
inst✝² : Group G
inst✝¹ : MeasurableMul G
μ : Measure G
inst✝ : μ.IsMulRightInvariant
t : G
p : G → Prop
⊢ (∀ᵐ (x : G) ∂μ, p (x * t)) ↔ ∀ᵐ (x : G) ∂μ, p x

Tactic:
conv_rhs => rw [Filter.Eventually, ← map_mul_right_ae μ t]

Result:
G : Type u_1
inst✝³ : MeasurableSpace G
inst✝² : Group G
inst✝¹ : MeasurableMul G
μ : Measure G
inst✝ : μ.IsMulRightInvariant
t : G
p : G → Prop
⊢ (∀ᵐ (x : G) ∂μ, p (x * t)) ↔ {x | p x} ∈ Filter.map (fun h => h * t) (ae μ)
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/Raw.lean
theorem Const.insertMany_val [BEq α][Hashable α] {m : Raw₀ α (fun _ => β)} {ρ : Type w} [ForIn Id ρ (α × β)] {l : ρ} :
    Raw.Const.insertMany m.val l = Raw₀.Const.insertMany m l

Proof state:
α : Type u
β : Type v
inst✝² : BEq α
inst✝¹ : Hashable α
m : Raw₀ α fun x => β
ρ : Type w
inst✝ : ForIn Id ρ (α × β)
l : ρ
⊢ Raw.Const.insertMany m.val l = (Raw₀.Const.insertMany m l).val.val

Tactic:
simp [Raw.Const.insertMany, m.2]

Result:
no goals
-- Mathlib/Algebra/GCDMonoid/Basic.lean
theorem gcd_eq_zero_iff [GCDMonoid α] (a b : α) : gcd a b = 0 ↔ a = 0 ∧ b = 0 :=
  Iff.intro
    (fun h => by
      let ⟨ca, ha⟩ := gcd_dvd_left a b
      let ⟨cb, hb⟩ := gcd_dvd_right a b
      rw [h, zero_mul] at ha hb
      exact ⟨ha, hb⟩)
    fun ⟨ha, hb⟩ => by
    rw [ha, hb, ← zero_dvd_iff]
    apply dvd_gcd <;> rfl

Proof state:
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : GCDMonoid α
a b : α
h : gcd a b = 0
ca : α
ha : a = gcd a b * ca
⊢ a = 0 ∧ b = 0

Tactic:
let ⟨cb, hb⟩ := gcd_dvd_right a b

Result:
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : GCDMonoid α
a b : α
h : gcd a b = 0
ca : α
ha : a = gcd a b * ca
cb : α
hb : b = gcd a b * cb
⊢ a = 0 ∧ b = 0

Proof state:
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : GCDMonoid α
a b : α
x✝ : a = 0 ∧ b = 0
ha : a = 0
hb : b = 0
⊢ 0 ∣ gcd 0 0

Tactic:
apply dvd_gcd <;> rfl

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : GCDMonoid α
a b : α
h : gcd a b = 0
⊢ a = 0 ∧ b = 0

Tactic:
let ⟨ca, ha⟩ := gcd_dvd_left a b

Result:
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : GCDMonoid α
a b : α
h : gcd a b = 0
ca : α
ha : a = gcd a b * ca
⊢ a = 0 ∧ b = 0

Proof state:
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : GCDMonoid α
a b : α
x✝ : a = 0 ∧ b = 0
ha : a = 0
hb : b = 0
⊢ gcd a b = 0

Tactic:
rw [ha, hb, ← zero_dvd_iff]

Result:
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : GCDMonoid α
a b : α
x✝ : a = 0 ∧ b = 0
ha : a = 0
hb : b = 0
⊢ 0 ∣ gcd 0 0

Proof state:
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : GCDMonoid α
a b : α
h : gcd a b = 0
ca : α
ha : a = gcd a b * ca
cb : α
hb : b = gcd a b * cb
⊢ a = 0 ∧ b = 0

Tactic:
rw [h, zero_mul] at ha hb

Result:
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : GCDMonoid α
a b : α
h : gcd a b = 0
ca : α
ha : a = 0
cb : α
hb : b = 0
⊢ a = 0 ∧ b = 0

Proof state:
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : GCDMonoid α
a b : α
h : gcd a b = 0
ca : α
ha : a = 0
cb : α
hb : b = 0
⊢ a = 0 ∧ b = 0

Tactic:
exact ⟨ha, hb⟩

Result:
no goals
-- Mathlib/Algebra/Vertex/HVertexOperator.lean
theorem compHahnSeries_add (u v : U) :
    compHahnSeries A B (u + v) = compHahnSeries A B u + compHahnSeries A B v

Proof state:
case coeff.h.coeff.h
Γ : Type u_5
Γ' : Type u_6
inst✝⁸ : OrderedCancelAddCommMonoid Γ
inst✝⁷ : OrderedCancelAddCommMonoid Γ'
R : Type u_7
inst✝⁶ : CommRing R
U : Type u_8
V : Type u_9
W : Type u_10
inst✝⁵ : AddCommGroup U
inst✝⁴ : Module R U
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : AddCommGroup W
inst✝ : Module R W
A : HVertexOperator Γ R V W
B : HVertexOperator Γ' R U V
u v : U
x✝¹ : Γ'
x✝ : Γ
⊢ (A (((of R).symm (B u)).coeff x✝¹) + A (((of R).symm (B v)).coeff x✝¹)).coeff x✝ =
    (A (((of R).symm (B u)).coeff x✝¹)).coeff x✝ + (A (((of R).symm (B v)).coeff x✝¹)).coeff x✝

Tactic:
rw [← HahnSeries.coeff_add]

Result:
no goals

Proof state:
Γ : Type u_5
Γ' : Type u_6
inst✝⁸ : OrderedCancelAddCommMonoid Γ
inst✝⁷ : OrderedCancelAddCommMonoid Γ'
R : Type u_7
inst✝⁶ : CommRing R
U : Type u_8
V : Type u_9
W : Type u_10
inst✝⁵ : AddCommGroup U
inst✝⁴ : Module R U
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : AddCommGroup W
inst✝ : Module R W
A : HVertexOperator Γ R V W
B : HVertexOperator Γ' R U V
u v : U
⊢ A.compHahnSeries B (u + v) = A.compHahnSeries B u + A.compHahnSeries B v

Tactic:
ext

Result:
case coeff.h.coeff.h
Γ : Type u_5
Γ' : Type u_6
inst✝⁸ : OrderedCancelAddCommMonoid Γ
inst✝⁷ : OrderedCancelAddCommMonoid Γ'
R : Type u_7
inst✝⁶ : CommRing R
U : Type u_8
V : Type u_9
W : Type u_10
inst✝⁵ : AddCommGroup U
inst✝⁴ : Module R U
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : AddCommGroup W
inst✝ : Module R W
A : HVertexOperator Γ R V W
B : HVertexOperator Γ' R U V
u v : U
x✝¹ : Γ'
x✝ : Γ
⊢ ((A.compHahnSeries B (u + v)).coeff x✝¹).coeff x✝ = ((A.compHahnSeries B u + A.compHahnSeries B v).coeff x✝¹).coeff x✝

Proof state:
case coeff.h.coeff.h
Γ : Type u_5
Γ' : Type u_6
inst✝⁸ : OrderedCancelAddCommMonoid Γ
inst✝⁷ : OrderedCancelAddCommMonoid Γ'
R : Type u_7
inst✝⁶ : CommRing R
U : Type u_8
V : Type u_9
W : Type u_10
inst✝⁵ : AddCommGroup U
inst✝⁴ : Module R U
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : AddCommGroup W
inst✝ : Module R W
A : HVertexOperator Γ R V W
B : HVertexOperator Γ' R U V
u v : U
x✝¹ : Γ'
x✝ : Γ
⊢ ((A.compHahnSeries B (u + v)).coeff x✝¹).coeff x✝ = ((A.compHahnSeries B u + A.compHahnSeries B v).coeff x✝¹).coeff x✝

Tactic:
simp only [compHahnSeries_coeff, map_add, coeff_apply, HahnSeries.coeff_add', Pi.add_apply]

Result:
case coeff.h.coeff.h
Γ : Type u_5
Γ' : Type u_6
inst✝⁸ : OrderedCancelAddCommMonoid Γ
inst✝⁷ : OrderedCancelAddCommMonoid Γ'
R : Type u_7
inst✝⁶ : CommRing R
U : Type u_8
V : Type u_9
W : Type u_10
inst✝⁵ : AddCommGroup U
inst✝⁴ : Module R U
inst✝³ : AddCommGroup V
inst✝² : Module R V
inst✝¹ : AddCommGroup W
inst✝ : Module R W
A : HVertexOperator Γ R V W
B : HVertexOperator Γ' R U V
u v : U
x✝¹ : Γ'
x✝ : Γ
⊢ (A (((of R).symm (B u)).coeff x✝¹) + A (((of R).symm (B v)).coeff x✝¹)).coeff x✝ =
    (A (((of R).symm (B u)).coeff x✝¹)).coeff x✝ + (A (((of R).symm (B v)).coeff x✝¹)).coeff x✝
-- Mathlib/NumberTheory/LSeries/HurwitzZetaOdd.lean
/-- If `s` is not in `-ℕ`, then `sinZeta a (1 - s)` is an explicit multiple of
`hurwitzZetaOdd s`. -/
lemma sinZeta_one_sub (a : UnitAddCircle) {s : ℂ} (hs : ∀ (n : ℕ), s ≠ -n) :
    sinZeta a (1 - s) = 2 * (2 * π) ^ (-s) * Gamma s * sin (π * s / 2) * hurwitzZetaOdd a s

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

Tactic:
rw [← Gammaℂ, sinZeta, (by ring : 1 - s + 1 = 2 - s), div_eq_mul_inv, inv_Gammaℝ_two_sub hs,
  completedSinZeta_one_sub, hurwitzZetaOdd, ← div_eq_mul_inv, ← mul_div_assoc, ← mul_div_assoc,
  mul_comm]

Result:
no goals

Proof state:
a : UnitAddCircle
s : ℂ
hs : ∀ (n : ℕ), s ≠ -↑n
⊢ 1 - s + 1 = 2 - s

Tactic:
ring

Result:
no goals
-- Mathlib/Topology/Algebra/InfiniteSum/Real.lean
theorem summable_sigma_of_nonneg {α} {β : α → Type*} {f : (Σ x, β x) → ℝ} (hf : ∀ x, 0 ≤ f x) :
    Summable f ↔ (∀ x, Summable fun y => f ⟨x, y⟩) ∧ Summable fun x => ∑' y, f ⟨x, y⟩

Proof state:
case intro
α : Type u_4
β : α → Type u_3
f : (x : α) × β x → ℝ≥0
⊢ (Summable fun i => ↑(f i)) ↔
    (∀ (x : α), Summable fun y => (fun i => ↑(f i)) ⟨x, y⟩) ∧ Summable fun x => ∑' (y : β x), (fun i => ↑(f i)) ⟨x, y⟩

Tactic:
simpa using mod_cast NNReal.summable_sigma

Result:
no goals

Proof state:
α : Type u_4
β : α → Type u_3
f : (x : α) × β x → ℝ
hf : ∀ (x : (x : α) × β x), 0 ≤ f x
⊢ Summable f ↔ (∀ (x : α), Summable fun y => f ⟨x, y⟩) ∧ Summable fun x => ∑' (y : β x), f ⟨x, y⟩

Tactic:
lift f to (Σx, β x) → ℝ≥0 using hf

Result:
case intro
α : Type u_4
β : α → Type u_3
f : (x : α) × β x → ℝ≥0
⊢ (Summable fun i => ↑(f i)) ↔
    (∀ (x : α), Summable fun y => (fun i => ↑(f i)) ⟨x, y⟩) ∧ Summable fun x => ∑' (y : β x), (fun i => ↑(f i)) ⟨x, y⟩
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem sub_self (x : BitVec n) : x - x = 0#n

Proof state:
n : Nat
x : BitVec n
⊢ x - x = 0#n

Tactic:
apply eq_of_toNat_eq

Result:
case a
n : Nat
x : BitVec n
⊢ (x - x).toNat = (0#n).toNat

Proof state:
case a
n : Nat
x : BitVec n
⊢ (x - x).toNat = (0#n).toNat

Tactic:
simp only [toNat_sub]

Result:
case a
n : Nat
x : BitVec n
⊢ (2 ^ n - x.toNat + x.toNat) % 2 ^ n = (0#n).toNat

Proof state:
case a
n : Nat
x : BitVec n
⊢ 2 ^ n % 2 ^ n = (0#n).toNat

Tactic:
simp

Result:
no goals

Proof state:
case a
n : Nat
x : BitVec n
⊢ (2 ^ n - x.toNat + x.toNat) % 2 ^ n = (0#n).toNat

Tactic:
rw [Nat.add_comm, Nat.add_sub_of_le]

Result:
case a
n : Nat
x : BitVec n
⊢ 2 ^ n % 2 ^ n = (0#n).toNat

case a
n : Nat
x : BitVec n
⊢ x.toNat ≤ 2 ^ n

Proof state:
case a
n : Nat
x : BitVec n
⊢ x.toNat ≤ 2 ^ n

Tactic:
exact Nat.le_of_lt x.isLt

Result:
no goals
-- Mathlib/Probability/Martingale/Basic.lean
theorem supermartingale_of_condExp_sub_nonneg_nat [IsFiniteMeasure μ] {f : ℕ → Ω → ℝ}
    (hadp : Adapted 𝒢 f) (hint : ∀ i, Integrable (f i) μ)
    (hf : ∀ i, 0 ≤ᵐ[μ] μ[f i - f (i + 1)|𝒢 i]) : Supermartingale f 𝒢 μ

Proof state:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
inst✝ : IsFiniteMeasure μ
f : ℕ → Ω → ℝ
hadp : Adapted 𝒢 f
hint : ∀ (i : ℕ), Integrable (f i) μ
hf : ∀ (i : ℕ), 0 ≤ᶠ[ae μ] μ[f i - f (i + 1)|↑𝒢 i]
⊢ Supermartingale (- -f) 𝒢 μ

Tactic:
refine (submartingale_of_condExp_sub_nonneg_nat hadp.neg (fun i => (hint i).neg) ?_).neg

Result:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
inst✝ : IsFiniteMeasure μ
f : ℕ → Ω → ℝ
hadp : Adapted 𝒢 f
hint : ∀ (i : ℕ), Integrable (f i) μ
hf : ∀ (i : ℕ), 0 ≤ᶠ[ae μ] μ[f i - f (i + 1)|↑𝒢 i]
⊢ ∀ (i : ℕ), 0 ≤ᶠ[ae μ] μ[(-f) (i + 1) - (-f) i|↑𝒢 i]

Proof state:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
inst✝ : IsFiniteMeasure μ
f : ℕ → Ω → ℝ
hadp : Adapted 𝒢 f
hint : ∀ (i : ℕ), Integrable (f i) μ
hf : ∀ (i : ℕ), 0 ≤ᶠ[ae μ] μ[f i - f (i + 1)|↑𝒢 i]
⊢ ∀ (i : ℕ), 0 ≤ᶠ[ae μ] μ[(-f) (i + 1) - (-f) i|↑𝒢 i]

Tactic:
simpa only [Pi.zero_apply, Pi.neg_apply, neg_sub_neg]

Result:
no goals

Proof state:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
inst✝ : IsFiniteMeasure μ
f : ℕ → Ω → ℝ
hadp : Adapted 𝒢 f
hint : ∀ (i : ℕ), Integrable (f i) μ
hf : ∀ (i : ℕ), 0 ≤ᶠ[ae μ] μ[f i - f (i + 1)|↑𝒢 i]
⊢ Supermartingale f 𝒢 μ

Tactic:
rw [← neg_neg f]

Result:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
inst✝ : IsFiniteMeasure μ
f : ℕ → Ω → ℝ
hadp : Adapted 𝒢 f
hint : ∀ (i : ℕ), Integrable (f i) μ
hf : ∀ (i : ℕ), 0 ≤ᶠ[ae μ] μ[f i - f (i + 1)|↑𝒢 i]
⊢ Supermartingale (- -f) 𝒢 μ
-- Mathlib/LinearAlgebra/Ray.lean
theorem sameRay_of_mem_orbit {v₁ v₂ : M} (h : v₁ ∈ MulAction.orbit ↥(Units.posSubgroup R) v₂) :
    SameRay R v₁ v₂

Proof state:
case intro.mk
R : Type u_1
inst✝² : LinearOrderedCommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v₂ : M
r : Rˣ
hr : 0 < ↑r
⊢ SameRay R (r • v₂) v₂

Tactic:
exact SameRay.sameRay_pos_smul_left _ hr

Result:
no goals

Proof state:
R : Type u_1
inst✝² : LinearOrderedCommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v₁ v₂ : M
h : v₁ ∈ MulAction.orbit (↥(Units.posSubgroup R)) v₂
⊢ SameRay R v₁ v₂

Tactic:
rcases h with ⟨⟨r, hr : 0 < r.1⟩, rfl : r • v₂ = v₁⟩

Result:
case intro.mk
R : Type u_1
inst✝² : LinearOrderedCommRing R
M : Type u_2
inst✝¹ : AddCommGroup M
inst✝ : Module R M
v₂ : M
r : Rˣ
hr : 0 < ↑r
⊢ SameRay R (r • v₂) v₂
-- Mathlib/Topology/Algebra/Order/Floor.lean
theorem tendsto_pow_div_factorial_atTop (c : K) :
    Tendsto (fun n ↦ c ^ n / n !) atTop (𝓝 0)

Proof state:
case h.e'_3.h.h.e'_5
K : Type u_1
inst✝³ : LinearOrderedField K
inst✝² : FloorSemiring K
inst✝¹ : TopologicalSpace K
inst✝ : OrderTopology K
c : K
x✝ : ℕ
⊢ c ^ x✝ = 1 * c ^ x✝

Tactic:
rw [one_mul]

Result:
no goals

Proof state:
K : Type u_1
inst✝³ : LinearOrderedField K
inst✝² : FloorSemiring K
inst✝¹ : TopologicalSpace K
inst✝ : OrderTopology K
c : K
⊢ Tendsto (fun n => c ^ n / ↑n !) atTop (𝓝 0)

Tactic:
convert tendsto_mul_pow_div_factorial_sub_atTop 1 c 0

Result:
case h.e'_3.h.h.e'_5
K : Type u_1
inst✝³ : LinearOrderedField K
inst✝² : FloorSemiring K
inst✝¹ : TopologicalSpace K
inst✝ : OrderTopology K
c : K
x✝ : ℕ
⊢ c ^ x✝ = 1 * c ^ x✝
-- Mathlib/CategoryTheory/Adjunction/Unique.lean
theorem leftAdjointUniq_trans {F F' F'' : C ⥤ D} {G : D ⥤ C} (adj1 : F ⊣ G) (adj2 : F' ⊣ G)
    (adj3 : F'' ⊣ G) :
    (leftAdjointUniq adj1 adj2).hom ≫ (leftAdjointUniq adj2 adj3).hom =
      (leftAdjointUniq adj1 adj3).hom

Proof state:
C : Type u_1
D : Type u_2
inst✝¹ : Category.{u_3, u_1} C
inst✝ : Category.{u_4, u_2} D
F F' F'' : C ⥤ D
G : D ⥤ C
adj1 : F ⊣ G
adj2 : F' ⊣ G
adj3 : F'' ⊣ G
⊢ (adj1.leftAdjointUniq adj2).hom ≫ (adj2.leftAdjointUniq adj3).hom = (adj1.leftAdjointUniq adj3).hom

Tactic:
simp [leftAdjointUniq]

Result:
no goals
-- Mathlib/LinearAlgebra/Basis/Flag.lean
theorem flag_zero (b : Basis (Fin n) R M) : b.flag 0 = ⊥

Proof state:
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
b : Basis (Fin n) R M
⊢ b.flag 0 = ⊥

Tactic:
simp [flag]

Result:
no goals
-- Mathlib/Algebra/ContinuedFractions/Computation/TerminatesIffRat.lean
theorem coe_of_rat_eq (v_eq_q : v = (↑q : K)) :
    (⟨(of q).h, (of q).s.map (Pair.map (↑))⟩ : GenContFract K) = of v

Proof state:
case mk
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
q : ℚ
v_eq_q : v = ↑q
h : K
s : Stream'.Seq (Pair K)
gcf_v_eq : of v = { h := h, s := s }
⊢ { h := ↑(of q).h, s := Stream'.Seq.map (Pair.map Rat.cast) (of q).s } = { h := h, s := s }

Tactic:
subst v

Result:
case mk
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
q : ℚ
h : K
s : Stream'.Seq (Pair K)
gcf_v_eq : of ↑q = { h := h, s := s }
⊢ { h := ↑(of q).h, s := Stream'.Seq.map (Pair.map Rat.cast) (of q).s } = { h := h, s := s }

Proof state:
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
q : ℚ
v_eq_q : v = ↑q
⊢ { h := ↑(of q).h, s := Stream'.Seq.map (Pair.map Rat.cast) (of q).s } = of v

Tactic:
rcases gcf_v_eq : of v with ⟨h, s⟩

Result:
case mk
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
q : ℚ
v_eq_q : v = ↑q
h : K
s : Stream'.Seq (Pair K)
gcf_v_eq : of v = { h := h, s := s }
⊢ { h := ↑(of q).h, s := Stream'.Seq.map (Pair.map Rat.cast) (of q).s } = { h := h, s := s }

Proof state:
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
q : ℚ
h : K
s : Stream'.Seq (Pair K)
gcf_v_eq : of ↑q = { h := h, s := s }
⊢ ↑⌊↑q⌋ = h

Tactic:
injection gcf_v_eq

Result:
no goals

Proof state:
case mk
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
q : ℚ
h : K
s : Stream'.Seq (Pair K)
gcf_v_eq : of ↑q = { h := h, s := s }
⊢ { h := ↑(of q).h, s := Stream'.Seq.map (Pair.map Rat.cast) (of q).s } = { h := h, s := s }

Tactic:
obtain rfl : ↑⌊(q : K)⌋ = h := by injection gcf_v_eq

Result:
case mk
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
q : ℚ
s : Stream'.Seq (Pair K)
gcf_v_eq : of ↑q = { h := ↑⌊↑q⌋, s := s }
⊢ { h := ↑(of q).h, s := Stream'.Seq.map (Pair.map Rat.cast) (of q).s } = { h := ↑⌊↑q⌋, s := s }

Proof state:
case mk
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
q : ℚ
s : Stream'.Seq (Pair K)
gcf_v_eq : of ↑q = { h := ↑⌊↑q⌋, s := s }
⊢ { h := ↑(of q).h, s := Stream'.Seq.map (Pair.map Rat.cast) (of q).s } = { h := ↑⌊↑q⌋, s := s }

Tactic:
simp [coe_of_h_rat_eq rfl, coe_of_s_rat_eq rfl, gcf_v_eq]

Result:
no goals