harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/Star/Subalgebra.lean
theorem coe_iInf {ι : Sort*} {S : ι → StarSubalgebra R A} : (↑(⨅ i, S i) : Set A) = ⋂ i, S i

Proof state:
R : Type u_2
A : Type u_3
inst✝⁵ : CommSemiring R
inst✝⁴ : StarRing R
inst✝³ : Semiring A
inst✝² : Algebra R A
inst✝¹ : StarRing A
inst✝ : StarModule R A
ι : Sort u_5
S : ι → StarSubalgebra R A
⊢ ↑(⨅ i, S i) = ⋂ i, ↑(S i)

Tactic:
simp [iInf]

Result:
no goals
-- Mathlib/LinearAlgebra/TensorProduct/RightExactness.lean
theorem TensorProduct.mk_surjective (S) [Semiring S] [Algebra R S]
    (h : Function.Surjective (algebraMap R S)) :
    Function.Surjective (TensorProduct.mk R S M 1)

Proof state:
case intro.intro
R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : Module R M
S : Type u_8
inst✝¹ : Semiring S
inst✝ : Algebra R S
h : Function.Surjective ⇑(algebraMap R S)
x : S
y : M
⊢ x ⊗ₜ[R] y ∈ ↑(range ((mk R S M) 1))

Tactic:
obtain ⟨x, rfl⟩ := h x

Result:
case intro.intro.intro
R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : Module R M
S : Type u_8
inst✝¹ : Semiring S
inst✝ : Algebra R S
h : Function.Surjective ⇑(algebraMap R S)
y : M
x : R
⊢ (algebraMap R S) x ⊗ₜ[R] y ∈ ↑(range ((mk R S M) 1))

Proof state:
R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : Module R M
S : Type u_8
inst✝¹ : Semiring S
inst✝ : Algebra R S
h : Function.Surjective ⇑(algebraMap R S)
⊢ {t | ∃ m n, m ⊗ₜ[R] n = t} ⊆ ↑(range ((mk R S M) 1))

Tactic:
rintro _ ⟨x, y, rfl⟩

Result:
case intro.intro
R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : Module R M
S : Type u_8
inst✝¹ : Semiring S
inst✝ : Algebra R S
h : Function.Surjective ⇑(algebraMap R S)
x : S
y : M
⊢ x ⊗ₜ[R] y ∈ ↑(range ((mk R S M) 1))

Proof state:
case intro.intro.intro
R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : Module R M
S : Type u_8
inst✝¹ : Semiring S
inst✝ : Algebra R S
h : Function.Surjective ⇑(algebraMap R S)
y : M
x : R
⊢ 1 ⊗ₜ[R] (x • y) ∈ ↑(range ((mk R S M) 1))

Tactic:
exact ⟨x • y, rfl⟩

Result:
no goals

Proof state:
R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : Module R M
S : Type u_8
inst✝¹ : Semiring S
inst✝ : Algebra R S
h : Function.Surjective ⇑(algebraMap R S)
⊢ Function.Surjective ⇑((mk R S M) 1)

Tactic:
rw [← LinearMap.range_eq_top, ← top_le_iff, ← span_tmul_eq_top, Submodule.span_le]

Result:
R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : Module R M
S : Type u_8
inst✝¹ : Semiring S
inst✝ : Algebra R S
h : Function.Surjective ⇑(algebraMap R S)
⊢ {t | ∃ m n, m ⊗ₜ[R] n = t} ⊆ ↑(range ((mk R S M) 1))

Proof state:
case intro.intro.intro
R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : Module R M
S : Type u_8
inst✝¹ : Semiring S
inst✝ : Algebra R S
h : Function.Surjective ⇑(algebraMap R S)
y : M
x : R
⊢ (algebraMap R S) x ⊗ₜ[R] y ∈ ↑(range ((mk R S M) 1))

Tactic:
rw [Algebra.algebraMap_eq_smul_one, smul_tmul]

Result:
case intro.intro.intro
R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : Module R M
S : Type u_8
inst✝¹ : Semiring S
inst✝ : Algebra R S
h : Function.Surjective ⇑(algebraMap R S)
y : M
x : R
⊢ 1 ⊗ₜ[R] (x • y) ∈ ↑(range ((mk R S M) 1))
-- Mathlib/CategoryTheory/CofilteredSystem.lean
theorem IsMittagLeffler.subset_image_eventualRange (h : F.IsMittagLeffler) (f : j ⟶ i) :
    F.eventualRange i ⊆ F.map f '' F.eventualRange j

Proof state:
case intro.intro
J : Type u
inst✝ : Category.{u_1, u} J
F : J ⥤ Type v
i j : J
h : F.IsMittagLeffler
f : j ⟶ i
k : J
g : k ⟶ j
hg : F.eventualRange j = range (F.map g)
⊢ F.eventualRange i ⊆ F.map f '' range (F.map g)

Tactic:
intro x hx

Result:
case intro.intro
J : Type u
inst✝ : Category.{u_1, u} J
F : J ⥤ Type v
i j : J
h : F.IsMittagLeffler
f : j ⟶ i
k : J
g : k ⟶ j
hg : F.eventualRange j = range (F.map g)
x : F.obj i
hx : x ∈ F.eventualRange i
⊢ x ∈ F.map f '' range (F.map g)

Proof state:
case intro.intro.intro
J : Type u
inst✝ : Category.{u_1, u} J
F : J ⥤ Type v
i j : J
h : F.IsMittagLeffler
f : j ⟶ i
k : J
g : k ⟶ j
hg : F.eventualRange j = range (F.map g)
x : F.obj k
hx : F.map (g ≫ f) x ∈ F.eventualRange i
⊢ F.map (g ≫ f) x ∈ F.map f '' range (F.map g)

Tactic:
exact ⟨_, ⟨x, rfl⟩, by rw [map_comp_apply]⟩

Result:
no goals

Proof state:
J : Type u
inst✝ : Category.{u_1, u} J
F : J ⥤ Type v
i j : J
h : F.IsMittagLeffler
f : j ⟶ i
⊢ F.eventualRange i ⊆ F.map f '' F.eventualRange j

Tactic:
obtain ⟨k, g, hg⟩ := F.isMittagLeffler_iff_eventualRange.1 h j

Result:
case intro.intro
J : Type u
inst✝ : Category.{u_1, u} J
F : J ⥤ Type v
i j : J
h : F.IsMittagLeffler
f : j ⟶ i
k : J
g : k ⟶ j
hg : F.eventualRange j = range (F.map g)
⊢ F.eventualRange i ⊆ F.map f '' F.eventualRange j

Proof state:
case intro.intro
J : Type u
inst✝ : Category.{u_1, u} J
F : J ⥤ Type v
i j : J
h : F.IsMittagLeffler
f : j ⟶ i
k : J
g : k ⟶ j
hg : F.eventualRange j = range (F.map g)
⊢ F.eventualRange i ⊆ F.map f '' F.eventualRange j

Tactic:
rw [hg]

Result:
case intro.intro
J : Type u
inst✝ : Category.{u_1, u} J
F : J ⥤ Type v
i j : J
h : F.IsMittagLeffler
f : j ⟶ i
k : J
g : k ⟶ j
hg : F.eventualRange j = range (F.map g)
⊢ F.eventualRange i ⊆ F.map f '' range (F.map g)

Proof state:
case intro.intro
J : Type u
inst✝ : Category.{u_1, u} J
F : J ⥤ Type v
i j : J
h : F.IsMittagLeffler
f : j ⟶ i
k : J
g : k ⟶ j
hg : F.eventualRange j = range (F.map g)
x : F.obj i
hx : x ∈ F.eventualRange i
⊢ x ∈ F.map f '' range (F.map g)

Tactic:
obtain ⟨x, rfl⟩ := F.mem_eventualRange_iff.1 hx (g ≫ f)

Result:
case intro.intro.intro
J : Type u
inst✝ : Category.{u_1, u} J
F : J ⥤ Type v
i j : J
h : F.IsMittagLeffler
f : j ⟶ i
k : J
g : k ⟶ j
hg : F.eventualRange j = range (F.map g)
x : F.obj k
hx : F.map (g ≫ f) x ∈ F.eventualRange i
⊢ F.map (g ≫ f) x ∈ F.map f '' range (F.map g)

Proof state:
J : Type u
inst✝ : Category.{u_1, u} J
F : J ⥤ Type v
i j : J
h : F.IsMittagLeffler
f : j ⟶ i
k : J
g : k ⟶ j
hg : F.eventualRange j = range (F.map g)
x : F.obj k
hx : F.map (g ≫ f) x ∈ F.eventualRange i
⊢ F.map f (F.map g x) = F.map (g ≫ f) x

Tactic:
rw [map_comp_apply]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/VitaliCaratheodory.lean
theorem exists_le_lowerSemicontinuous_lintegral_ge (f : α → ℝ≥0∞) (hf : Measurable f) {ε : ℝ≥0∞}
    (εpos : ε ≠ 0) :
    ∃ g : α → ℝ≥0∞,
      (∀ x, f x ≤ g x) ∧ LowerSemicontinuous g ∧ (∫⁻ x, g x ∂μ) ≤ (∫⁻ x, f x ∂μ) + ε

Proof state:
case intro.intro.refine_2
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : MeasurableSpace α
inst✝¹ : BorelSpace α
μ : Measure α
inst✝ : μ.WeaklyRegular
f : α → ℝ≥0∞
hf : Measurable f
ε : ℝ≥0∞
εpos : ε ≠ 0
δ : ℕ → ℝ≥0∞
δpos : ∀ (i : ℕ), 0 < δ i
hδ : ∑' (i : ℕ), δ i < ε
g : ℕ → α → ℝ≥0
f_le_g : ∀ (n : ℕ) (x : α), (SimpleFunc.eapproxDiff f n) x ≤ g n x
gcont : ∀ (n : ℕ), LowerSemicontinuous (g n)
hg : ∀ (n : ℕ), ∫⁻ (x : α), ↑(g n x) ∂μ ≤ ∫⁻ (x : α), ↑((SimpleFunc.eapproxDiff f n) x) ∂μ + δ n
n : ℕ
⊢ LowerSemicontinuous fun x => ↑(g n x)

Tactic:
exact
  ENNReal.continuous_coe.comp_lowerSemicontinuous (gcont n) fun x y hxy =>
    ENNReal.coe_le_coe.2 hxy

Result:
no goals
-- Mathlib/Topology/Separation/Profinite.lean
theorem loc_compact_Haus_tot_disc_of_zero_dim [TotallyDisconnectedSpace H] :
    IsTopologicalBasis { s : Set H | IsClopen s }

Proof state:
H : Type u_3
inst✝³ : TopologicalSpace H
inst✝² : LocallyCompactSpace H
inst✝¹ : T2Space H
inst✝ : TotallyDisconnectedSpace H
U : Set H
hU : IsOpen U
s : Set H
comp : IsCompact s
sU : s ⊆ U
u : Set ↑s := Subtype.val ⁻¹' interior s
u_open_in_s : IsOpen u
x : { x // x ∈ s }
memU : ↑x ∈ U
xs : ↑x ∈ interior s
this : CompactSpace ↑s
V : Set ↑s
VisClopen : IsClopen V
Vx : x ∈ V
V_sub : V ⊆ u
⊢ IsClopen (Subtype.val '' V)

Tactic:
refine ⟨comp.isClosed.isClosedEmbedding_subtypeVal.isClosed_iff_image_isClosed.1 VisClopen.1,
  ?_⟩

Result:
H : Type u_3
inst✝³ : TopologicalSpace H
inst✝² : LocallyCompactSpace H
inst✝¹ : T2Space H
inst✝ : TotallyDisconnectedSpace H
U : Set H
hU : IsOpen U
s : Set H
comp : IsCompact s
sU : s ⊆ U
u : Set ↑s := Subtype.val ⁻¹' interior s
u_open_in_s : IsOpen u
x : { x // x ∈ s }
memU : ↑x ∈ U
xs : ↑x ∈ interior s
this : CompactSpace ↑s
V : Set ↑s
VisClopen : IsClopen V
Vx : x ∈ V
V_sub : V ⊆ u
⊢ IsOpen (Subtype.val '' V)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Find.lean
theorem Sublist.findSome?_isSome {l₁ l₂ : List α} (h : l₁ <+ l₂) :
    (l₁.findSome? f).isSome → (l₂.findSome? f).isSome

Proof state:
case cons₂.h_1
α : Type u_1
α✝ : Type u_2
f : α → Option α✝
l₁ l₂ l₁✝ l₂✝ : List α
a : α
h : l₁✝ <+ l₂✝
ih : (findSome? f l₁✝).isSome = true → (findSome? f l₂✝).isSome = true
x✝ : Option α✝
b✝ : α✝
heq✝ : f a = some b✝
⊢ (some b✝).isSome = true → (some b✝).isSome = true

Tactic:
simp_all

Result:
no goals

Proof state:
case cons₂
α : Type u_1
α✝ : Type u_2
f : α → Option α✝
l₁ l₂ l₁✝ l₂✝ : List α
a : α
h : l₁✝ <+ l₂✝
ih : (findSome? f l₁✝).isSome = true → (findSome? f l₂✝).isSome = true
⊢ (match f a with
        | some b => some b
        | none => findSome? f l₁✝).isSome =
      true →
    (match f a with
        | some b => some b
        | none => findSome? f l₂✝).isSome =
      true

Tactic:
split

Result:
case cons₂.h_1
α : Type u_1
α✝ : Type u_2
f : α → Option α✝
l₁ l₂ l₁✝ l₂✝ : List α
a : α
h : l₁✝ <+ l₂✝
ih : (findSome? f l₁✝).isSome = true → (findSome? f l₂✝).isSome = true
x✝ : Option α✝
b✝ : α✝
heq✝ : f a = some b✝
⊢ (some b✝).isSome = true → (some b✝).isSome = true

case cons₂.h_2
α : Type u_1
α✝ : Type u_2
f : α → Option α✝
l₁ l₂ l₁✝ l₂✝ : List α
a : α
h : l₁✝ <+ l₂✝
ih : (findSome? f l₁✝).isSome = true → (findSome? f l₂✝).isSome = true
x✝ : Option α✝
heq✝ : f a = none
⊢ (findSome? f l₁✝).isSome = true → (findSome? f l₂✝).isSome = true

Proof state:
case cons₂.h_2
α : Type u_1
α✝ : Type u_2
f : α → Option α✝
l₁ l₂ l₁✝ l₂✝ : List α
a : α
h : l₁✝ <+ l₂✝
ih : (findSome? f l₁✝).isSome = true → (findSome? f l₂✝).isSome = true
x✝ : Option α✝
heq✝ : f a = none
⊢ (findSome? f l₁✝).isSome = true → (findSome? f l₂✝).isSome = true

Tactic:
exact ih

Result:
no goals

Proof state:
case cons₂
α : Type u_1
α✝ : Type u_2
f : α → Option α✝
l₁ l₂ l₁✝ l₂✝ : List α
a : α
h : l₁✝ <+ l₂✝
ih : (findSome? f l₁✝).isSome = true → (findSome? f l₂✝).isSome = true
⊢ (findSome? f (a :: l₁✝)).isSome = true → (findSome? f (a :: l₂✝)).isSome = true

Tactic:
simp only [findSome?]

Result:
case cons₂
α : Type u_1
α✝ : Type u_2
f : α → Option α✝
l₁ l₂ l₁✝ l₂✝ : List α
a : α
h : l₁✝ <+ l₂✝
ih : (findSome? f l₁✝).isSome = true → (findSome? f l₂✝).isSome = true
⊢ (match f a with
        | some b => some b
        | none => findSome? f l₁✝).isSome =
      true →
    (match f a with
        | some b => some b
        | none => findSome? f l₂✝).isSome =
      true

Proof state:
case slnil
α : Type u_1
α✝ : Type u_2
f : α → Option α✝
l₁ l₂ : List α
⊢ (findSome? f []).isSome = true → (findSome? f []).isSome = true

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Homology/HomologicalComplex.lean
theorem image_to_eq_image [HasImages V] [HasEqualizers V] {i j : ι} (r : c.Rel i j) :
    imageSubobject (C.dTo j) = imageSubobject (C.d i j)

Proof state:
ι : Type u_1
V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasZeroMorphisms V
c : ComplexShape ι
C : HomologicalComplex V c
inst✝¹ : HasImages V
inst✝ : HasEqualizers V
i j : ι
r : c.Rel i j
⊢ imageSubobject (C.dTo j) = imageSubobject (C.d i j)

Tactic:
rw [C.dTo_eq r]

Result:
ι : Type u_1
V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasZeroMorphisms V
c : ComplexShape ι
C : HomologicalComplex V c
inst✝¹ : HasImages V
inst✝ : HasEqualizers V
i j : ι
r : c.Rel i j
⊢ imageSubobject ((C.xPrevIso r).hom ≫ C.d i j) = imageSubobject (C.d i j)

Proof state:
ι : Type u_1
V : Type u
inst✝³ : Category.{v, u} V
inst✝² : HasZeroMorphisms V
c : ComplexShape ι
C : HomologicalComplex V c
inst✝¹ : HasImages V
inst✝ : HasEqualizers V
i j : ι
r : c.Rel i j
⊢ imageSubobject ((C.xPrevIso r).hom ≫ C.d i j) = imageSubobject (C.d i j)

Tactic:
apply imageSubobject_iso_comp

Result:
no goals
-- Mathlib/Condensed/Discrete/Colimit.lean
@[simp]
lemma lanPresheafExt_hom {F G : Profinite.{u}ᵒᵖ ⥤ Type (u+1)} (S : Profinite.{u}ᵒᵖ)
    (i : toProfinite.op ⋙ F ≅ toProfinite.op ⋙ G) : (lanPresheafExt i).hom.app S =
      colimMap (whiskerLeft (CostructuredArrow.proj toProfinite.op S) i.hom)

Proof state:
case w
F G : Profiniteᵒᵖ ⥤ Type (u + 1)
S : Profiniteᵒᵖ
i : toProfinite.op ⋙ F ≅ toProfinite.op ⋙ G
⊢ ∀ (j : CostructuredArrow toProfinite.op S),
    colimit.ι (CostructuredArrow.proj toProfinite.op S ⋙ toProfinite.op ⋙ F) j ≫
        colimit.desc (CostructuredArrow.proj toProfinite.op S ⋙ toProfinite.op ⋙ F)
          (toProfinite.op.costructuredArrowMapCocone (toProfinite.op ⋙ F)
            (toProfinite.op.pointwiseLeftKanExtension (toProfinite.op ⋙ G))
            (i.hom ≫ toProfinite.op.pointwiseLeftKanExtensionUnit (toProfinite.op ⋙ G)) S) =
      colimit.ι (CostructuredArrow.proj toProfinite.op S ⋙ toProfinite.op ⋙ F) j ≫
        colimMap (whiskerLeft (CostructuredArrow.proj toProfinite.op S) i.hom)

Tactic:
aesop

Result:
no goals

Proof state:
F G : Profiniteᵒᵖ ⥤ Type (u + 1)
S : Profiniteᵒᵖ
i : toProfinite.op ⋙ F ≅ toProfinite.op ⋙ G
⊢ colimit.desc (CostructuredArrow.proj toProfinite.op S ⋙ toProfinite.op ⋙ F)
      (toProfinite.op.costructuredArrowMapCocone (toProfinite.op ⋙ F)
        (toProfinite.op.pointwiseLeftKanExtension (toProfinite.op ⋙ G))
        (i.hom ≫ toProfinite.op.pointwiseLeftKanExtensionUnit (toProfinite.op ⋙ G)) S) =
    colimMap (whiskerLeft (CostructuredArrow.proj toProfinite.op S) i.hom)

Tactic:
apply colimit.hom_ext

Result:
case w
F G : Profiniteᵒᵖ ⥤ Type (u + 1)
S : Profiniteᵒᵖ
i : toProfinite.op ⋙ F ≅ toProfinite.op ⋙ G
⊢ ∀ (j : CostructuredArrow toProfinite.op S),
    colimit.ι (CostructuredArrow.proj toProfinite.op S ⋙ toProfinite.op ⋙ F) j ≫
        colimit.desc (CostructuredArrow.proj toProfinite.op S ⋙ toProfinite.op ⋙ F)
          (toProfinite.op.costructuredArrowMapCocone (toProfinite.op ⋙ F)
            (toProfinite.op.pointwiseLeftKanExtension (toProfinite.op ⋙ G))
            (i.hom ≫ toProfinite.op.pointwiseLeftKanExtensionUnit (toProfinite.op ⋙ G)) S) =
      colimit.ι (CostructuredArrow.proj toProfinite.op S ⋙ toProfinite.op ⋙ F) j ≫
        colimMap (whiskerLeft (CostructuredArrow.proj toProfinite.op S) i.hom)

Proof state:
F G : Profiniteᵒᵖ ⥤ Type (u + 1)
S : Profiniteᵒᵖ
i : toProfinite.op ⋙ F ≅ toProfinite.op ⋙ G
⊢ (lanPresheafExt i).hom.app S = colimMap (whiskerLeft (CostructuredArrow.proj toProfinite.op S) i.hom)

Tactic:
simp only [lanPresheaf, pointwiseLeftKanExtension_obj, lanPresheafExt,
  leftKanExtensionUniqueOfIso_hom, pointwiseLeftKanExtension_desc_app]

Result:
F G : Profiniteᵒᵖ ⥤ Type (u + 1)
S : Profiniteᵒᵖ
i : toProfinite.op ⋙ F ≅ toProfinite.op ⋙ G
⊢ colimit.desc (CostructuredArrow.proj toProfinite.op S ⋙ toProfinite.op ⋙ F)
      (toProfinite.op.costructuredArrowMapCocone (toProfinite.op ⋙ F)
        (toProfinite.op.pointwiseLeftKanExtension (toProfinite.op ⋙ G))
        (i.hom ≫ toProfinite.op.pointwiseLeftKanExtensionUnit (toProfinite.op ⋙ G)) S) =
    colimMap (whiskerLeft (CostructuredArrow.proj toProfinite.op S) i.hom)
-- Mathlib/MeasureTheory/Integral/DominatedConvergence.lean
lemma hasSum_integral_of_summable_integral_norm {ι} [Countable ι] {F : ι → α → E}
    (hF_int : ∀ i : ι, Integrable (F i) μ) (hF_sum : Summable fun i ↦ ∫ a, ‖F i a‖ ∂μ) :
    HasSum (∫ a, F · a ∂μ) (∫ a, (∑' i, F i a) ∂μ)

Proof state:
case pos
α : Type u_1
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
ι : Type u_4
inst✝ : Countable ι
F : ι → α → E
hF_int : ∀ (i : ι), Integrable (F i) μ
hF_sum : Summable fun i => ∫ (a : α), ‖F i a‖ ∂μ
hE : CompleteSpace E
⊢ HasSum (fun x => ∫ (a : α), F x a ∂μ) (∫ (a : α), ∑' (i : ι), F i a ∂μ)

Tactic:
rw [integral_tsum (fun i ↦ (hF_int i).1)]

Result:
case pos
α : Type u_1
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
ι : Type u_4
inst✝ : Countable ι
F : ι → α → E
hF_int : ∀ (i : ι), Integrable (F i) μ
hF_sum : Summable fun i => ∫ (a : α), ‖F i a‖ ∂μ
hE : CompleteSpace E
⊢ HasSum (fun x => ∫ (a : α), F x a ∂μ) (∑' (i : ι), ∫ (a : α), F i a ∂μ)

case pos
α : Type u_1
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
ι : Type u_4
inst✝ : Countable ι
F : ι → α → E
hF_int : ∀ (i : ι), Integrable (F i) μ
hF_sum : Summable fun i => ∫ (a : α), ‖F i a‖ ∂μ
hE : CompleteSpace E
⊢ ∑' (i : ι), ∫⁻ (a : α), ‖F i a‖ₑ ∂μ ≠ ⊤

Proof state:
α : Type u_1
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
ι : Type u_4
inst✝ : Countable ι
F : ι → α → E
hF_int : ∀ (i : ι), Integrable (F i) μ
hF_sum : Summable fun i => ∫ (a : α), ‖F i a‖ ∂μ
hE : CompleteSpace E
i : ι
⊢ ENNReal.ofReal (∫ (a : α), ↑‖F i a‖₊ ∂μ) = ENNReal.ofReal (∫ (a : α), ‖F i a‖ ∂μ)

Tactic:
simp only [coe_nnnorm]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/DivModLemmas.lean
theorem ediv_nonneg_of_nonpos_of_nonpos {a b : Int} (Ha : a ≤ 0) (Hb : b ≤ 0) : 0 ≤ a / b

Proof state:
a b : Int
Ha : a ≤ 0
Hb : b ≤ 0
⊢ 0 ≤ a / b

Tactic:
match a, b with
| ofNat a, b =>
  match Int.le_antisymm Ha (ofNat_zero_le a) with
  | h1 =>
    rw [h1, zero_ediv]
    exact Int.le_refl 0
| a, ofNat b =>
  match Int.le_antisymm Hb (ofNat_zero_le  b) with
  | h1 =>
    rw [h1, Int.ediv_zero]
    exact Int.le_refl 0
| negSucc a, negSucc b =>
  rw [Int.div_def, ediv]
  exact le_add_one (ediv_nonneg (ofNat_zero_le a) (Int.le_trans (ofNat_zero_le b) (le.intro 1 rfl)))

Result:
no goals

Proof state:
a✝ b✝ : Int
a b : Nat
Ha : -[a+1] ≤ 0
Hb : -[b+1] ≤ 0
⊢ 0 ≤ -[a+1] / -[b+1]

Tactic:
rw [Int.div_def, ediv]

Result:
a✝ b✝ : Int
a b : Nat
Ha : -[a+1] ≤ 0
Hb : -[b+1] ≤ 0
⊢ 0 ≤ ofNat (a / b.succ).succ

Proof state:
a✝ b✝ a : Int
b : Nat
Ha : a ≤ 0
Hb : ofNat b ≤ 0
h1 : ofNat b = 0 := Int.le_antisymm Hb (ofNat_zero_le b)
⊢ 0 ≤ 0

Tactic:
exact Int.le_refl 0

Result:
no goals

Proof state:
a✝ b✝ : Int
a : Nat
b : Int
Ha : ofNat a ≤ 0
Hb : b ≤ 0
⊢ 0 ≤ ofNat a / b

Tactic:
match Int.le_antisymm Ha (ofNat_zero_le a) with
| h1 =>
  rw [h1, zero_ediv]
  exact Int.le_refl 0

Result:
no goals

Proof state:
a✝ b✝ : Int
a b : Nat
Ha : -[a+1] ≤ 0
Hb : -[b+1] ≤ 0
⊢ 0 ≤ ofNat (a / b.succ).succ

Tactic:
exact le_add_one (ediv_nonneg (ofNat_zero_le a) (Int.le_trans (ofNat_zero_le b) (le.intro 1 rfl)))

Result:
no goals

Proof state:
a✝ b✝ : Int
a : Nat
b : Int
Ha : ofNat a ≤ 0
Hb : b ≤ 0
h1 : ofNat a = 0 := Int.le_antisymm Ha (ofNat_zero_le a)
⊢ 0 ≤ ofNat a / b

Tactic:
rw [h1, zero_ediv]

Result:
a✝ b✝ : Int
a : Nat
b : Int
Ha : ofNat a ≤ 0
Hb : b ≤ 0
h1 : ofNat a = 0 := Int.le_antisymm Ha (ofNat_zero_le a)
⊢ 0 ≤ 0

Proof state:
a✝ b✝ a : Int
b : Nat
Ha : a ≤ 0
Hb : ofNat b ≤ 0
h1 : ofNat b = 0 := Int.le_antisymm Hb (ofNat_zero_le b)
⊢ 0 ≤ a / ofNat b

Tactic:
rw [h1, Int.ediv_zero]

Result:
a✝ b✝ a : Int
b : Nat
Ha : a ≤ 0
Hb : ofNat b ≤ 0
h1 : ofNat b = 0 := Int.le_antisymm Hb (ofNat_zero_le b)
⊢ 0 ≤ 0

Proof state:
a✝ b✝ : Int
a : Nat
b : Int
Ha : ofNat a ≤ 0
Hb : b ≤ 0
h1 : ofNat a = 0 := Int.le_antisymm Ha (ofNat_zero_le a)
⊢ 0 ≤ 0

Tactic:
exact Int.le_refl 0

Result:
no goals

Proof state:
a✝ b✝ a : Int
b : Nat
Ha : a ≤ 0
Hb : ofNat b ≤ 0
⊢ 0 ≤ a / ofNat b

Tactic:
match Int.le_antisymm Hb (ofNat_zero_le  b) with
| h1 =>
  rw [h1, Int.ediv_zero]
  exact Int.le_refl 0

Result:
no goals
-- Mathlib/Analysis/Calculus/Taylor.lean
theorem taylorWithinEval_self (f : ℝ → E) (n : ℕ) (s : Set ℝ) (x₀ : ℝ) :
    taylorWithinEval f n s x₀ x₀ = f x₀

Proof state:
case zero
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
s : Set ℝ
x₀ : ℝ
⊢ taylorWithinEval f 0 s x₀ x₀ = f x₀

Tactic:
exact taylor_within_zero_eval _ _ _ _

Result:
no goals

Proof state:
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
n : ℕ
s : Set ℝ
x₀ : ℝ
⊢ taylorWithinEval f n s x₀ x₀ = f x₀

Tactic:
induction n with
| zero => exact taylor_within_zero_eval _ _ _ _
| succ k hk => simp [hk]

Result:
no goals

Proof state:
case succ
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
s : Set ℝ
x₀ : ℝ
k : ℕ
hk : taylorWithinEval f k s x₀ x₀ = f x₀
⊢ taylorWithinEval f (k + 1) s x₀ x₀ = f x₀

Tactic:
simp [hk]

Result:
no goals
-- Mathlib/Algebra/Order/Antidiag/Pi.lean
lemma piAntidiag_univ_fin_eq_antidiagonalTuple (n k : ℕ) :
    piAntidiag univ n = Nat.antidiagonalTuple k n

Proof state:
n k : ℕ
⊢ univ.piAntidiag n = Nat.antidiagonalTuple k n

Tactic:
ext

Result:
case h
n k : ℕ
a✝ : Fin k → ℕ
⊢ a✝ ∈ univ.piAntidiag n ↔ a✝ ∈ Nat.antidiagonalTuple k n

Proof state:
case h
n k : ℕ
a✝ : Fin k → ℕ
⊢ a✝ ∈ univ.piAntidiag n ↔ a✝ ∈ Nat.antidiagonalTuple k n

Tactic:
simp [Nat.mem_antidiagonalTuple]

Result:
no goals
-- Mathlib/RingTheory/FractionalIdeal/Extended.lean
theorem extended_zero : extended L hf (0 : FractionalIdeal M K) = 0 :=
  have : ((0 : FractionalIdeal M K) : Set K) = {0}

Proof state:
A : Type u_1
inst✝⁷ : CommRing A
B : Type u_2
inst✝⁶ : CommRing B
f : A →+* B
K : Type u_3
M : Submonoid A
inst✝⁵ : CommRing K
inst✝⁴ : Algebra A K
inst✝³ : IsLocalization M K
L : Type u_4
N : Submonoid B
inst✝² : CommRing L
inst✝¹ : Algebra B L
inst✝ : IsLocalization N L
hf : M ≤ Submonoid.comap f N
⊢ ↑0 = {0}

Tactic:
ext

Result:
case h
A : Type u_1
inst✝⁷ : CommRing A
B : Type u_2
inst✝⁶ : CommRing B
f : A →+* B
K : Type u_3
M : Submonoid A
inst✝⁵ : CommRing K
inst✝⁴ : Algebra A K
inst✝³ : IsLocalization M K
L : Type u_4
N : Submonoid B
inst✝² : CommRing L
inst✝¹ : Algebra B L
inst✝ : IsLocalization N L
hf : M ≤ Submonoid.comap f N
x✝ : K
⊢ x✝ ∈ ↑0 ↔ x✝ ∈ {0}

Proof state:
A : Type u_1
inst✝⁷ : CommRing A
B : Type u_2
inst✝⁶ : CommRing B
f : A →+* B
K : Type u_3
M : Submonoid A
inst✝⁵ : CommRing K
inst✝⁴ : Algebra A K
inst✝³ : IsLocalization M K
L : Type u_4
N : Submonoid B
inst✝² : CommRing L
inst✝¹ : Algebra B L
inst✝ : IsLocalization N L
hf : M ≤ Submonoid.comap f N
this : ↑0 = {0}
⊢ (fun I => ↑I) (extended L hf 0) = (fun I => ↑I) 0

Tactic:
simp [this]

Result:
no goals

Proof state:
case h
A : Type u_1
inst✝⁷ : CommRing A
B : Type u_2
inst✝⁶ : CommRing B
f : A →+* B
K : Type u_3
M : Submonoid A
inst✝⁵ : CommRing K
inst✝⁴ : Algebra A K
inst✝³ : IsLocalization M K
L : Type u_4
N : Submonoid B
inst✝² : CommRing L
inst✝¹ : Algebra B L
inst✝ : IsLocalization N L
hf : M ≤ Submonoid.comap f N
x✝ : K
⊢ x✝ ∈ ↑0 ↔ x✝ ∈ {0}

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Seq/Seq.lean
theorem toList_ofList (l : List α) : toList (ofList l) (terminates_ofList l) = l :=
  ofList_injective (by simp)

Proof state:
α : Type u
l : List α
⊢ ↑((↑l).toList ⋯) = ↑l

Tactic:
simp

Result:
no goals
-- Mathlib/RingTheory/Spectrum/Prime/RingHom.lean
theorem range_specComap_of_surjective (hf : Surjective f) :
    Set.range f.specComap = zeroLocus (ker f)

Proof state:
case h.e'_2.h.e'_4
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : Surjective ⇑f
⊢ Set.univ = zeroLocus ↑⊥

Tactic:
rw [zeroLocus_bot]

Result:
no goals

Proof state:
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : Surjective ⇑f
⊢ f.specComap '' Set.univ = zeroLocus ↑(ker f)

Tactic:
convert image_specComap_zeroLocus_eq_zeroLocus_comap _ _ hf _

Result:
case h.e'_2.h.e'_4
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : Surjective ⇑f
⊢ Set.univ = zeroLocus ↑⊥

Proof state:
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : Surjective ⇑f
⊢ Set.range f.specComap = zeroLocus ↑(ker f)

Tactic:
rw [← Set.image_univ]

Result:
R : Type u
S : Type v
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
hf : Surjective ⇑f
⊢ f.specComap '' Set.univ = zeroLocus ↑(ker f)
-- Mathlib/Data/List/MinMax.lean
theorem not_lt_minimum_of_mem' (ha : a ∈ l) : ¬(a : WithTop α) < minimum l

Proof state:
α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x1 x2 => x1 < x2
l : List α
a : α
ha : a ∈ l
⊢ ¬↑a < l.minimum

Tactic:
cases h : l.minimum <;> simp_all [not_lt_minimum_of_mem ha]

Result:
no goals