harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/MeasureTheory/Integral/FundThmCalculus.lean
theorem integral_hasDerivWithinAt_of_tendsto_ae_left (hf : IntervalIntegrable f volume a b)
    {s t : Set ℝ} [FTCFilter a (𝓝[s] a) (𝓝[t] a)] (hmeas : StronglyMeasurableAtFilter f (𝓝[t] a))
    (ha : Tendsto f (𝓝[t] a ⊓ ae volume) (𝓝 c)) :
    HasDerivWithinAt (fun u => ∫ x in u..b, f x) (-c) s a

Proof state:
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
f : ℝ → E
c : E
a b : ℝ
hf : IntervalIntegrable f volume a b
s t : Set ℝ
inst✝ : FTCFilter a (𝓝[s] a) (𝓝[t] a)
hmeas : StronglyMeasurableAtFilter f (𝓝[t] a) volume
ha : Tendsto f (𝓝[t] a ⊓ ae volume) (𝓝 c)
⊢ HasDerivWithinAt (fun u => ∫ (x : ℝ) in u..b, f x) (-c) s a

Tactic:
simp only [integral_symm b]

Result:
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
f : ℝ → E
c : E
a b : ℝ
hf : IntervalIntegrable f volume a b
s t : Set ℝ
inst✝ : FTCFilter a (𝓝[s] a) (𝓝[t] a)
hmeas : StronglyMeasurableAtFilter f (𝓝[t] a) volume
ha : Tendsto f (𝓝[t] a ⊓ ae volume) (𝓝 c)
⊢ HasDerivWithinAt (fun u => -∫ (x : ℝ) in b..u, f x) (-c) s a

Proof state:
E : Type u_3
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
f : ℝ → E
c : E
a b : ℝ
hf : IntervalIntegrable f volume a b
s t : Set ℝ
inst✝ : FTCFilter a (𝓝[s] a) (𝓝[t] a)
hmeas : StronglyMeasurableAtFilter f (𝓝[t] a) volume
ha : Tendsto f (𝓝[t] a ⊓ ae volume) (𝓝 c)
⊢ HasDerivWithinAt (fun u => -∫ (x : ℝ) in b..u, f x) (-c) s a

Tactic:
exact (integral_hasDerivWithinAt_of_tendsto_ae_right hf.symm hmeas ha).neg

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Arithmetic.lean
theorem bsup_congr {o₁ o₂ : Ordinal.{u}} (f : ∀ a < o₁, Ordinal.{max u v}) (ho : o₁ = o₂) :
    bsup.{_, v} o₁ f = bsup.{_, v} o₂ fun a h => f a (h.trans_eq ho.symm)

Proof state:
o₁ o₂ : Ordinal.{u}
f : (a : Ordinal.{u}) → a < o₁ → Ordinal.{max u v}
ho : o₁ = o₂
⊢ o₁.bsup f = o₂.bsup fun a h => f a ⋯

Tactic:
subst ho

Result:
o₁ : Ordinal.{u}
f : (a : Ordinal.{u}) → a < o₁ → Ordinal.{max u v}
⊢ o₁.bsup f = o₁.bsup fun a h => f a ⋯

Proof state:
o₁ : Ordinal.{u}
f : (a : Ordinal.{u}) → a < o₁ → Ordinal.{max u v}
⊢ o₁.bsup f = o₁.bsup fun a h => f a ⋯

Tactic:
rfl

Result:
no goals
-- Mathlib/LinearAlgebra/FiniteDimensional.lean
theorem finrank_add_finrank_le_of_disjoint [FiniteDimensional K V]
    {s t : Submodule K V} (hdisjoint : Disjoint s t) :
    finrank K s + finrank K t ≤ finrank K V

Proof state:
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
s t : Submodule K V
hdisjoint : Disjoint s t
⊢ finrank K ↥s + finrank K ↥t ≤ finrank K V

Tactic:
rw [← Submodule.finrank_sup_add_finrank_inf_eq s t, hdisjoint.eq_bot, finrank_bot, add_zero]

Result:
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
s t : Submodule K V
hdisjoint : Disjoint s t
⊢ finrank K ↥(s ⊔ t) ≤ finrank K V

Proof state:
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
s t : Submodule K V
hdisjoint : Disjoint s t
⊢ finrank K ↥(s ⊔ t) ≤ finrank K V

Tactic:
exact Submodule.finrank_le _

Result:
no goals
-- Mathlib/AlgebraicTopology/SimplexCategory/Basic.lean
theorem epi_iff_surjective {n m : SimplexCategory} {f : n ⟶ m} :
    Epi f ↔ Function.Surjective f.toOrderHom

Proof state:
n m : SimplexCategory
f : n ⟶ m
⊢ Epi (skeletalFunctor.map f) ↔ Function.Surjective ⇑(Hom.toOrderHom f)

Tactic:
simp only [skeletalFunctor_obj, skeletalFunctor_map,
  NonemptyFinLinOrd.epi_iff_surjective, NonemptyFinLinOrd.coe_of, ConcreteCategory.hom_ofHom]

Result:
no goals

Proof state:
n m : SimplexCategory
f : n ⟶ m
⊢ Epi f ↔ Function.Surjective ⇑(Hom.toOrderHom f)

Tactic:
rw [← Functor.epi_map_iff_epi skeletalEquivalence.functor]

Result:
n m : SimplexCategory
f : n ⟶ m
⊢ Epi (skeletalEquivalence.functor.map f) ↔ Function.Surjective ⇑(Hom.toOrderHom f)

Proof state:
n m : SimplexCategory
f : n ⟶ m
⊢ Epi (skeletalEquivalence.functor.map f) ↔ Function.Surjective ⇑(Hom.toOrderHom f)

Tactic:
dsimp only [skeletalEquivalence, Functor.asEquivalence_functor]

Result:
n m : SimplexCategory
f : n ⟶ m
⊢ Epi (skeletalFunctor.map f) ↔ Function.Surjective ⇑(Hom.toOrderHom f)
-- Mathlib/Algebra/Ring/Periodic.lean
theorem Periodic.nat_mul_sub_eq [Ring α] (h : Periodic f c) (n : ℕ) : f (n * c - x) = f (-x)

Proof state:
α : Type u_1
β : Type u_2
f : α → β
c x : α
inst✝ : Ring α
h : Periodic f c
n : ℕ
⊢ f (↑n * c - x) = f (-x)

Tactic:
simpa only [sub_eq_neg_add] using h.nat_mul n (-x)

Result:
no goals
-- Mathlib/Order/CompleteLattice.lean
theorem sup_iSup_nat_succ (u : ℕ → α) : (u 0 ⊔ ⨆ i, u (i + 1)) = ⨆ i, u i :=
  calc
    (u 0 ⊔ ⨆ i, u (i + 1)) = ⨆ x ∈ {0} ∪ range Nat.succ, u x

Proof state:
α : Type u_1
inst✝ : CompleteLattice α
u : ℕ → α
⊢ u 0 ⊔ ⨆ i, u (i + 1) = ⨆ x ∈ {0} ∪ range Nat.succ, u x

Tactic:
rw [iSup_union, iSup_singleton, iSup_range]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : CompleteLattice α
u : ℕ → α
⊢ ⨆ x ∈ {0} ∪ range Nat.succ, u x = ⨆ i, u i

Tactic:
rw [Nat.zero_union_range_succ, iSup_univ]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/DivModLemmas.lean
theorem fmod_self {a : Int} : a.fmod a = 0

Proof state:
a : Int
⊢ a.fmod a = 0

Tactic:
have := mul_fmod_left 1 a

Result:
a : Int
this : (1 * a).fmod a = 0
⊢ a.fmod a = 0

Proof state:
a : Int
this : (1 * a).fmod a = 0
⊢ a.fmod a = 0

Tactic:
rwa [Int.one_mul] at this

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Bounds.lean
/-- Half of **Jordan's inequality** for absolute values. -/
lemma mul_abs_le_abs_sin (hx : |x| ≤ π / 2) : 2 / π * |x| ≤ |sin x|

Proof state:
x : ℝ
hx : |x| ≤ π / 2
⊢ 2 / π * |x| ≤ |sin x|

Tactic:
wlog hx₀ : 0 ≤ x

Result:
case inr
x : ℝ
hx : |x| ≤ π / 2
this : ∀ {x : ℝ}, |x| ≤ π / 2 → 0 ≤ x → 2 / π * |x| ≤ |sin x|
hx₀ : ¬0 ≤ x
⊢ 2 / π * |x| ≤ |sin x|

x✝ x : ℝ
hx : |x| ≤ π / 2
hx₀ : 0 ≤ x
⊢ 2 / π * |x| ≤ |sin x|

Proof state:
x : ℝ
hx : |x| ≤ π / 2
this : ∀ {x : ℝ}, |x| ≤ π / 2 → 0 ≤ x → 2 / π * |x| ≤ |sin x|
hx₀ : ¬0 ≤ x
⊢ |(-x)| ≤ π / 2

Tactic:
rwa [abs_neg]

Result:
no goals

Proof state:
x : ℝ
hx : |x| ≤ π / 2
this : ∀ {x : ℝ}, |x| ≤ π / 2 → 0 ≤ x → 2 / π * |x| ≤ |sin x|
hx₀ : ¬0 ≤ x
⊢ 2 / π * |x| ≤ |sin x|

Tactic:
simpa using this (by rwa [abs_neg]) <| neg_nonneg.2 <| le_of_not_le hx₀

Result:
no goals

Proof state:
x✝ x : ℝ
hx : x ≤ π / 2
hx₀ : 0 ≤ x
⊢ 2 / π * x ≤ |sin x|

Tactic:
exact (mul_le_sin hx₀ hx).trans (le_abs_self _)

Result:
no goals

Proof state:
x✝ x : ℝ
hx : |x| ≤ π / 2
hx₀ : 0 ≤ x
⊢ 2 / π * |x| ≤ |sin x|

Tactic:
rw [abs_of_nonneg hx₀] at hx ⊢

Result:
x✝ x : ℝ
hx : x ≤ π / 2
hx₀ : 0 ≤ x
⊢ 2 / π * x ≤ |sin x|

Proof state:
case inr
x : ℝ
hx : |x| ≤ π / 2
this : ∀ {x : ℝ}, |x| ≤ π / 2 → 0 ≤ x → 2 / π * |x| ≤ |sin x|
hx₀ : ¬0 ≤ x
⊢ 2 / π * |x| ≤ |sin x|

x✝ x : ℝ
hx : |x| ≤ π / 2
hx₀ : 0 ≤ x
⊢ 2 / π * |x| ≤ |sin x|

Tactic:
case inr => simpa using this (by rwa [abs_neg]) <| neg_nonneg.2 <| le_of_not_le hx₀

Result:
x✝ x : ℝ
hx : |x| ≤ π / 2
hx₀ : 0 ≤ x
⊢ 2 / π * |x| ≤ |sin x|
-- Mathlib/Analysis/Convex/Function.lean
theorem ConvexOn.openSegment_subset_strict_epigraph (hf : ConvexOn 𝕜 s f) (p q : E × β)
    (hp : p.1 ∈ s ∧ f p.1 < p.2) (hq : q.1 ∈ s ∧ f q.1 ≤ q.2) :
    openSegment 𝕜 p q ⊆ { p : E × β | p.1 ∈ s ∧ f p.1 < p.2 }

Proof state:
𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst✝⁵ : OrderedSemiring 𝕜
inst✝⁴ : AddCommMonoid E
inst✝³ : OrderedCancelAddCommMonoid β
inst✝² : Module 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : OrderedSMul 𝕜 β
s : Set E
f : E → β
hf : ConvexOn 𝕜 s f
p q : E × β
hp : p.1 ∈ s ∧ f p.1 < p.2
hq : q.1 ∈ s ∧ f q.1 ≤ q.2
⊢ openSegment 𝕜 p q ⊆ {p | p.1 ∈ s ∧ f p.1 < p.2}

Tactic:
rintro _ ⟨a, b, ha, hb, hab, rfl⟩

Result:
case intro.intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst✝⁵ : OrderedSemiring 𝕜
inst✝⁴ : AddCommMonoid E
inst✝³ : OrderedCancelAddCommMonoid β
inst✝² : Module 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : OrderedSMul 𝕜 β
s : Set E
f : E → β
hf : ConvexOn 𝕜 s f
p q : E × β
hp : p.1 ∈ s ∧ f p.1 < p.2
hq : q.1 ∈ s ∧ f q.1 ≤ q.2
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ a • p + b • q ∈ {p | p.1 ∈ s ∧ f p.1 < p.2}

Proof state:
case intro.intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst✝⁵ : OrderedSemiring 𝕜
inst✝⁴ : AddCommMonoid E
inst✝³ : OrderedCancelAddCommMonoid β
inst✝² : Module 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : OrderedSMul 𝕜 β
s : Set E
f : E → β
hf : ConvexOn 𝕜 s f
p q : E × β
hp : p.1 ∈ s ∧ f p.1 < p.2
hq : q.1 ∈ s ∧ f q.1 ≤ q.2
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ f (a • p + b • q).1 < (a • p + b • q).2

Tactic:
calc
  f (a • p.1 + b • q.1) ≤ a • f p.1 + b • f q.1 := hf.2 hp.1 hq.1 ha.le hb.le hab
  _ < a • p.2 + b • q.2 := add_lt_add_of_lt_of_le
     (smul_lt_smul_of_pos_left hp.2 ha) (smul_le_smul_of_nonneg_left hq.2 hb.le)

Result:
no goals

Proof state:
case intro.intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst✝⁵ : OrderedSemiring 𝕜
inst✝⁴ : AddCommMonoid E
inst✝³ : OrderedCancelAddCommMonoid β
inst✝² : Module 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : OrderedSMul 𝕜 β
s : Set E
f : E → β
hf : ConvexOn 𝕜 s f
p q : E × β
hp : p.1 ∈ s ∧ f p.1 < p.2
hq : q.1 ∈ s ∧ f q.1 ≤ q.2
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ a • p + b • q ∈ {p | p.1 ∈ s ∧ f p.1 < p.2}

Tactic:
refine ⟨hf.1 hp.1 hq.1 ha.le hb.le hab, ?_⟩

Result:
case intro.intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst✝⁵ : OrderedSemiring 𝕜
inst✝⁴ : AddCommMonoid E
inst✝³ : OrderedCancelAddCommMonoid β
inst✝² : Module 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : OrderedSMul 𝕜 β
s : Set E
f : E → β
hf : ConvexOn 𝕜 s f
p q : E × β
hp : p.1 ∈ s ∧ f p.1 < p.2
hq : q.1 ∈ s ∧ f q.1 ≤ q.2
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ f (a • p + b • q).1 < (a • p + b • q).2
-- Mathlib/Data/Nat/PartENat.lean
theorem toWithTop_add {x y : PartENat} : toWithTop (x + y) = toWithTop x + toWithTop y

Proof state:
case refine_1.refine_1
x y : PartENat
⊢ (⊤ + ⊤).toWithTop = ⊤.toWithTop + ⊤.toWithTop

Tactic:
simp only [add_top, toWithTop_top', _root_.add_top]

Result:
no goals

Proof state:
x y : PartENat
⊢ (x + y).toWithTop = x.toWithTop + y.toWithTop

Tactic:
refine PartENat.casesOn y ?_ ?_ <;> refine PartENat.casesOn x ?_ ?_

Result:
case refine_1.refine_1
x y : PartENat
⊢ (⊤ + ⊤).toWithTop = ⊤.toWithTop + ⊤.toWithTop

case refine_1.refine_2
x y : PartENat
⊢ ∀ (n : ℕ), (↑n + ⊤).toWithTop = (↑n).toWithTop + ⊤.toWithTop

case refine_2.refine_1
x y : PartENat
⊢ ∀ (n : ℕ), (⊤ + ↑n).toWithTop = ⊤.toWithTop + (↑n).toWithTop

case refine_2.refine_2
x y : PartENat
⊢ ∀ (n n_1 : ℕ), (↑n + ↑n_1).toWithTop = (↑n).toWithTop + (↑n_1).toWithTop

Proof state:
case refine_2.refine_1
x y : PartENat
⊢ ∀ (n : ℕ), (⊤ + ↑n).toWithTop = ⊤.toWithTop + (↑n).toWithTop

Tactic:
simp only [top_add, toWithTop_top', toWithTop_natCast', _root_.top_add, forall_const]

Result:
no goals

Proof state:
case refine_1.refine_2
x y : PartENat
⊢ ∀ (n : ℕ), (↑n + ⊤).toWithTop = (↑n).toWithTop + ⊤.toWithTop

Tactic:
simp only [add_top, toWithTop_top', toWithTop_natCast', _root_.add_top, forall_const]

Result:
no goals

Proof state:
case refine_2.refine_2
x y : PartENat
⊢ ∀ (n n_1 : ℕ), (↑n + ↑n_1).toWithTop = (↑n).toWithTop + (↑n_1).toWithTop

Tactic:
simp_rw [toWithTop_natCast', ← Nat.cast_add, toWithTop_natCast', forall_const]

Result:
no goals
-- Mathlib/Data/Matroid/Circuit.lean
/-- A cocircuit is a minimal set that intersects every base. -/
lemma isCocircuit_iff_minimal :
    M.IsCocircuit K ↔ Minimal (fun X ↦ ∀ B, M.IsBase B → (X ∩ B).Nonempty) K

Proof state:
α : Type u_1
M : Matroid α
K : Set α
aux : M✶.Dep = fun X => (∀ (B : Set α), M.IsBase B → (X ∩ B).Nonempty) ∧ X ⊆ M.E
⊢ M.IsCocircuit K ↔ Minimal (fun X => ∀ (B : Set α), M.IsBase B → (X ∩ B).Nonempty) K

Tactic:
rw [isCocircuit_def, isCircuit_def, aux, iff_comm]

Result:
α : Type u_1
M : Matroid α
K : Set α
aux : M✶.Dep = fun X => (∀ (B : Set α), M.IsBase B → (X ∩ B).Nonempty) ∧ X ⊆ M.E
⊢ Minimal (fun X => ∀ (B : Set α), M.IsBase B → (X ∩ B).Nonempty) K ↔
    Minimal (fun X => (∀ (B : Set α), M.IsBase B → (X ∩ B).Nonempty) ∧ X ⊆ M.E) K

Proof state:
α : Type u_1
M : Matroid α
K : Set α
⊢ M.IsCocircuit K ↔ Minimal (fun X => ∀ (B : Set α), M.IsBase B → (X ∩ B).Nonempty) K

Tactic:
have aux : M✶.Dep = fun X ↦ (∀ B, M.IsBase B → (X ∩ B).Nonempty) ∧ X ⊆ M.E := by
  ext; apply dual_dep_iff_forall

Result:
α : Type u_1
M : Matroid α
K : Set α
aux : M✶.Dep = fun X => (∀ (B : Set α), M.IsBase B → (X ∩ B).Nonempty) ∧ X ⊆ M.E
⊢ M.IsCocircuit K ↔ Minimal (fun X => ∀ (B : Set α), M.IsBase B → (X ∩ B).Nonempty) K

Proof state:
α : Type u_1
M : Matroid α
K : Set α
⊢ M✶.Dep = fun X => (∀ (B : Set α), M.IsBase B → (X ∩ B).Nonempty) ∧ X ⊆ M.E

Tactic:
ext

Result:
case h.a
α : Type u_1
M : Matroid α
K x✝ : Set α
⊢ M✶.Dep x✝ ↔ (∀ (B : Set α), M.IsBase B → (x✝ ∩ B).Nonempty) ∧ x✝ ⊆ M.E

Proof state:
case h.a
α : Type u_1
M : Matroid α
K x✝ : Set α
⊢ M✶.Dep x✝ ↔ (∀ (B : Set α), M.IsBase B → (x✝ ∩ B).Nonempty) ∧ x✝ ⊆ M.E

Tactic:
apply dual_dep_iff_forall

Result:
no goals

Proof state:
α : Type u_1
M : Matroid α
K : Set α
aux : M✶.Dep = fun X => (∀ (B : Set α), M.IsBase B → (X ∩ B).Nonempty) ∧ X ⊆ M.E
X : Set α
hX : ∀ (B : Set α), M.IsBase B → (X ∩ B).Nonempty
B : Set α
hB : M.IsBase B
⊢ (X ∩ M.E ∩ B).Nonempty

Tactic:
rw [inter_assoc, inter_eq_self_of_subset_right hB.subset_ground]

Result:
α : Type u_1
M : Matroid α
K : Set α
aux : M✶.Dep = fun X => (∀ (B : Set α), M.IsBase B → (X ∩ B).Nonempty) ∧ X ⊆ M.E
X : Set α
hX : ∀ (B : Set α), M.IsBase B → (X ∩ B).Nonempty
B : Set α
hB : M.IsBase B
⊢ (X ∩ B).Nonempty

Proof state:
α : Type u_1
M : Matroid α
K : Set α
aux : M✶.Dep = fun X => (∀ (B : Set α), M.IsBase B → (X ∩ B).Nonempty) ∧ X ⊆ M.E
X : Set α
hX : ∀ (B : Set α), M.IsBase B → (X ∩ B).Nonempty
B : Set α
hB : M.IsBase B
⊢ (X ∩ B).Nonempty

Tactic:
exact hX B hB

Result:
no goals

Proof state:
α : Type u_1
M : Matroid α
K : Set α
aux : M✶.Dep = fun X => (∀ (B : Set α), M.IsBase B → (X ∩ B).Nonempty) ∧ X ⊆ M.E
⊢ Minimal (fun X => ∀ (B : Set α), M.IsBase B → (X ∩ B).Nonempty) K ↔
    Minimal (fun X => (∀ (B : Set α), M.IsBase B → (X ∩ B).Nonempty) ∧ X ⊆ M.E) K

Tactic:
refine minimal_iff_minimal_of_imp_of_forall (fun _ h ↦ h.1) fun X hX ↦
  ⟨X ∩ M.E, inter_subset_left, fun B hB ↦ ?_, inter_subset_right⟩

Result:
α : Type u_1
M : Matroid α
K : Set α
aux : M✶.Dep = fun X => (∀ (B : Set α), M.IsBase B → (X ∩ B).Nonempty) ∧ X ⊆ M.E
X : Set α
hX : ∀ (B : Set α), M.IsBase B → (X ∩ B).Nonempty
B : Set α
hB : M.IsBase B
⊢ (X ∩ M.E ∩ B).Nonempty
-- Mathlib/Topology/Instances/ENNReal/Lemmas.lean
theorem tendsto_tsum_compl_atTop_zero {α : Type*} {f : α → ℝ≥0∞} (hf : ∑' x, f x ≠ ∞) :
    Tendsto (fun s : Finset α => ∑' b : { x // x ∉ s }, f b) atTop (𝓝 0)

Proof state:
case h.e'_3.h
α : Type u_4
f : α → ℝ≥0
hf : ∑' (x : α), (fun i => ↑(f i)) x ≠ ⊤
x✝ : Finset α
⊢ Summable fun b => f ↑b

Tactic:
exact NNReal.summable_comp_injective (tsum_coe_ne_top_iff_summable.1 hf) Subtype.coe_injective

Result:
no goals

Proof state:
α : Type u_4
f : α → ℝ≥0∞
hf : ∑' (x : α), f x ≠ ⊤
⊢ Tendsto (fun s => ∑' (b : { x // x ∉ s }), f ↑b) atTop (𝓝 0)

Tactic:
lift f to α → ℝ≥0 using ENNReal.ne_top_of_tsum_ne_top hf

Result:
case intro
α : Type u_4
f : α → ℝ≥0
hf : ∑' (x : α), (fun i => ↑(f i)) x ≠ ⊤
⊢ Tendsto (fun s => ∑' (b : { x // x ∉ s }), (fun i => ↑(f i)) ↑b) atTop (𝓝 0)

Proof state:
case intro
α : Type u_4
f : α → ℝ≥0
hf : ∑' (x : α), (fun i => ↑(f i)) x ≠ ⊤
⊢ Tendsto (fun s => ∑' (b : { x // x ∉ s }), (fun i => ↑(f i)) ↑b) atTop (𝓝 0)

Tactic:
convert ENNReal.tendsto_coe.2 (NNReal.tendsto_tsum_compl_atTop_zero f)

Result:
case h.e'_3.h
α : Type u_4
f : α → ℝ≥0
hf : ∑' (x : α), (fun i => ↑(f i)) x ≠ ⊤
x✝ : Finset α
⊢ ∑' (b : { x // x ∉ x✝ }), (fun i => ↑(f i)) ↑b = ↑(∑' (b : { x // x ∉ x✝ }), f ↑b)

Proof state:
case h.e'_3.h
α : Type u_4
f : α → ℝ≥0
hf : ∑' (x : α), (fun i => ↑(f i)) x ≠ ⊤
x✝ : Finset α
⊢ ∑' (b : { x // x ∉ x✝ }), (fun i => ↑(f i)) ↑b = ↑(∑' (b : { x // x ∉ x✝ }), f ↑b)

Tactic:
rw [ENNReal.coe_tsum]

Result:
case h.e'_3.h
α : Type u_4
f : α → ℝ≥0
hf : ∑' (x : α), (fun i => ↑(f i)) x ≠ ⊤
x✝ : Finset α
⊢ Summable fun b => f ↑b
-- Mathlib/Data/List/Forall2.lean
theorem rel_filterMap : ((R ⇒ Option.Rel P) ⇒ Forall₂ R ⇒ Forall₂ P) filterMap filterMap
  | _, _, _, _, _, Forall₂.nil => Forall₂.nil
  | f, g, hfg, a :: as, b :: bs, Forall₂.cons h₁ h₂ => by
    rw [filterMap_cons, filterMap_cons]
    exact
      match f a, g b, hfg h₁ with
      | _, _, Option.Rel.none => rel_filterMap (@hfg) h₂
      | _, _, Option.Rel.some h => Forall₂.cons h (rel_filterMap (@hfg) h₂)

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R : α → β → Prop
P : γ → δ → Prop
f : α → Option γ
g : β → Option δ
hfg : (R ⇒ Option.Rel P) f g
a : α
as : List α
b : β
bs : List β
h₁ : R a b
h₂ : Forall₂ R as bs
⊢ Forall₂ P (filterMap f (a :: as)) (filterMap g (b :: bs))

Tactic:
rw [filterMap_cons, filterMap_cons]

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R : α → β → Prop
P : γ → δ → Prop
f : α → Option γ
g : β → Option δ
hfg : (R ⇒ Option.Rel P) f g
a : α
as : List α
b : β
bs : List β
h₁ : R a b
h₂ : Forall₂ R as bs
⊢ Forall₂ P
    (match f a with
    | none => filterMap f as
    | some b => b :: filterMap f as)
    (match g b with
    | none => filterMap g bs
    | some b => b :: filterMap g bs)

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
R : α → β → Prop
P : γ → δ → Prop
f : α → Option γ
g : β → Option δ
hfg : (R ⇒ Option.Rel P) f g
a : α
as : List α
b : β
bs : List β
h₁ : R a b
h₂ : Forall₂ R as bs
⊢ Forall₂ P
    (match f a with
    | none => filterMap f as
    | some b => b :: filterMap f as)
    (match g b with
    | none => filterMap g bs
    | some b => b :: filterMap g bs)

Tactic:
exact
  match f a, g b, hfg h₁ with
  | _, _, Option.Rel.none => rel_filterMap (@hfg) h₂
  | _, _, Option.Rel.some h => Forall₂.cons h (rel_filterMap (@hfg) h₂)

Result:
no goals
-- Mathlib/Algebra/MvPolynomial/Variables.lean
theorem mem_vars (i : σ) : i ∈ p.vars ↔ ∃ d ∈ p.support, i ∈ d.support

Proof state:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial σ R
i : σ
⊢ i ∈ p.vars ↔ ∃ d ∈ p.support, i ∈ d.support

Tactic:
simp only [vars_def, Multiset.mem_toFinset, mem_degrees, mem_support_iff, exists_prop]

Result:
no goals

Proof state:
R : Type u
σ : Type u_1
inst✝ : CommSemiring R
p : MvPolynomial σ R
i : σ
⊢ i ∈ p.vars ↔ ∃ d ∈ p.support, i ∈ d.support

Tactic:
classical simp only [vars_def, Multiset.mem_toFinset, mem_degrees, mem_support_iff, exists_prop]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Derivative.lean
theorem derivative_pow_eq_zero {n : ℕ} (chn : (n : R) ≠ 0) {a : R[X]} :
    derivative (a ^ n) = 0 ↔ derivative a = 0

Proof state:
R : Type u
inst✝² : CommSemiring R
inst✝¹ : NoZeroDivisors R
n : ℕ
chn : ↑n ≠ 0
a : R[X]
inst✝ : Nontrivial R
⊢ derivative (a ^ n) = 0 ↔ derivative a = 0

Tactic:
simp +contextual [derivative_pow, or_imp, chn]

Result:
no goals

Proof state:
R : Type u
inst✝¹ : CommSemiring R
inst✝ : NoZeroDivisors R
n : ℕ
chn : ↑n ≠ 0
a : R[X]
⊢ derivative (a ^ n) = 0 ↔ derivative a = 0

Tactic:
nontriviality R

Result:
R : Type u
inst✝² : CommSemiring R
inst✝¹ : NoZeroDivisors R
n : ℕ
chn : ↑n ≠ 0
a : R[X]
inst✝ : Nontrivial R
⊢ derivative (a ^ n) = 0 ↔ derivative a = 0
-- Mathlib/MeasureTheory/Measure/Regular.lean
theorem map [BorelSpace α] [MeasurableSpace β] [TopologicalSpace β]
    [BorelSpace β] [Regular μ] (f : α ≃ₜ β) : (Measure.map f μ).Regular

Proof state:
α : Type u_1
β : Type u_2
inst✝⁶ : MeasurableSpace α
μ : Measure α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : BorelSpace α
inst✝³ : MeasurableSpace β
inst✝² : TopologicalSpace β
inst✝¹ : BorelSpace β
inst✝ : μ.Regular
f : α ≃ₜ β
⊢ (map (⇑f) μ).Regular

Tactic:
haveI := OuterRegular.map f μ

Result:
α : Type u_1
β : Type u_2
inst✝⁶ : MeasurableSpace α
μ : Measure α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : BorelSpace α
inst✝³ : MeasurableSpace β
inst✝² : TopologicalSpace β
inst✝¹ : BorelSpace β
inst✝ : μ.Regular
f : α ≃ₜ β
this : (map (⇑f) μ).OuterRegular
⊢ (map (⇑f) μ).Regular

Proof state:
α : Type u_1
β : Type u_2
inst✝⁶ : MeasurableSpace α
μ : Measure α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : BorelSpace α
inst✝³ : MeasurableSpace β
inst✝² : TopologicalSpace β
inst✝¹ : BorelSpace β
inst✝ : μ.Regular
f : α ≃ₜ β
this✝ : (map (⇑f) μ).OuterRegular
this : IsFiniteMeasureOnCompacts (map (⇑f) μ)
⊢ (map (⇑f) μ).Regular

Tactic:
exact
  ⟨Regular.innerRegular.map' f.toMeasurableEquiv
      (fun U hU => hU.preimage f.continuous)
      (fun K hK => hK.image f.continuous)⟩

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝⁶ : MeasurableSpace α
μ : Measure α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : BorelSpace α
inst✝³ : MeasurableSpace β
inst✝² : TopologicalSpace β
inst✝¹ : BorelSpace β
inst✝ : μ.Regular
f : α ≃ₜ β
this : (map (⇑f) μ).OuterRegular
⊢ (map (⇑f) μ).Regular

Tactic:
haveI := IsFiniteMeasureOnCompacts.map μ f

Result:
α : Type u_1
β : Type u_2
inst✝⁶ : MeasurableSpace α
μ : Measure α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : BorelSpace α
inst✝³ : MeasurableSpace β
inst✝² : TopologicalSpace β
inst✝¹ : BorelSpace β
inst✝ : μ.Regular
f : α ≃ₜ β
this✝ : (map (⇑f) μ).OuterRegular
this : IsFiniteMeasureOnCompacts (map (⇑f) μ)
⊢ (map (⇑f) μ).Regular
-- Mathlib/Topology/UrysohnsLemma.lean
theorem approx_of_nmem_U (c : CU P) (n : ℕ) {x : X} (hx : x ∉ c.U) : c.approx n x = 1

Proof state:
case succ
X : Type u_1
inst✝ : TopologicalSpace X
P : Set X → Prop
x : X
n : ℕ
ihn : ∀ (c : CU P), x ∉ c.U → approx n c x = 1
c : CU P
hx : x ∉ c.U
⊢ approx (n + 1) c x = 1

Tactic:
simp only [approx]

Result:
case succ
X : Type u_1
inst✝ : TopologicalSpace X
P : Set X → Prop
x : X
n : ℕ
ihn : ∀ (c : CU P), x ∉ c.U → approx n c x = 1
c : CU P
hx : x ∉ c.U
⊢ midpoint ℝ (approx n c.left x) (approx n c.right x) = 1

Proof state:
case succ
X : Type u_1
inst✝ : TopologicalSpace X
P : Set X → Prop
x : X
n : ℕ
ihn : ∀ (c : CU P), x ∉ c.U → approx n c x = 1
c : CU P
hx : x ∉ c.U
⊢ midpoint ℝ (approx n c.left x) (approx n c.right x) = 1

Tactic:
rw [ihn, ihn, midpoint_self]

Result:
case succ.hx
X : Type u_1
inst✝ : TopologicalSpace X
P : Set X → Prop
x : X
n : ℕ
ihn : ∀ (c : CU P), x ∉ c.U → approx n c x = 1
c : CU P
hx : x ∉ c.U
⊢ x ∉ c.right.U

case succ.hx
X : Type u_1
inst✝ : TopologicalSpace X
P : Set X → Prop
x : X
n : ℕ
ihn : ∀ (c : CU P), x ∉ c.U → approx n c x = 1
c : CU P
hx : x ∉ c.U
⊢ x ∉ c.left.U

Proof state:
case succ.hx
X : Type u_1
inst✝ : TopologicalSpace X
P : Set X → Prop
x : X
n : ℕ
ihn : ∀ (c : CU P), x ∉ c.U → approx n c x = 1
c : CU P
hx : x ∉ c.U
⊢ x ∉ c.right.U

case succ.hx
X : Type u_1
inst✝ : TopologicalSpace X
P : Set X → Prop
x : X
n : ℕ
ihn : ∀ (c : CU P), x ∉ c.U → approx n c x = 1
c : CU P
hx : x ∉ c.U
⊢ x ∉ c.left.U

Tactic:
exacts [hx, fun hU => hx <| c.left_U_subset hU]

Result:
no goals

Proof state:
case zero
X : Type u_1
inst✝ : TopologicalSpace X
P : Set X → Prop
x : X
c : CU P
hx : x ∉ c.U
⊢ approx 0 c x = 1

Tactic:
rw [← mem_compl_iff] at hx

Result:
case zero
X : Type u_1
inst✝ : TopologicalSpace X
P : Set X → Prop
x : X
c : CU P
hx : x ∈ c.Uᶜ
⊢ approx 0 c x = 1

Proof state:
case zero
X : Type u_1
inst✝ : TopologicalSpace X
P : Set X → Prop
x : X
c : CU P
hx : x ∈ c.Uᶜ
⊢ approx 0 c x = 1

Tactic:
exact indicator_of_mem hx _

Result:
no goals

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
P : Set X → Prop
c : CU P
n : ℕ
x : X
hx : x ∉ c.U
⊢ approx n c x = 1

Tactic:
induction n generalizing c with
| zero =>
  rw [← mem_compl_iff] at hx
  exact indicator_of_mem hx _
| succ n ihn =>
  simp only [approx]
  rw [ihn, ihn, midpoint_self]
  exacts [hx, fun hU => hx <| c.left_U_subset hU]

Result:
no goals
-- Mathlib/Analysis/Complex/Basic.lean
@[simp 1100, norm_cast] lemma nnnorm_intCast (n : ℤ) : ‖(n : ℂ)‖₊ = ‖n‖₊

Proof state:
case a
n : ℤ
⊢ ↑‖↑n‖₊ = ↑‖n‖₊

Tactic:
exact norm_intCast n

Result:
no goals

Proof state:
n : ℤ
⊢ ‖↑n‖₊ = ‖n‖₊

Tactic:
ext

Result:
case a
n : ℤ
⊢ ↑‖↑n‖₊ = ↑‖n‖₊