harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/CategoryTheory/Limits/Shapes/Pullback/CommSq.lean
theorem zero_right (X : C) : IsPullback (0 : X ⟶ 0) (𝟙 X) (0 : (0 : C) ⟶ 0) (0 : X ⟶ 0) :=
  of_iso_pullback (by simp) ((zeroProdIso X).symm ≪≫ (pullbackZeroZeroIso _ _).symm)
    (by simp [eq_iff_true_of_subsingleton]) (by simp)

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
X : C
⊢ ((zeroProdIso X).symm ≪≫ (pullbackZeroZeroIso 0 X).symm).hom ≫ pullback.snd 0 0 = 𝟙 X

Tactic:
simp

Result:
no goals

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
X : C
⊢ ((zeroProdIso X).symm ≪≫ (pullbackZeroZeroIso 0 X).symm).hom ≫ pullback.fst 0 0 = 0

Tactic:
simp [eq_iff_true_of_subsingleton]

Result:
no goals

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
X : C
⊢ CommSq 0 (𝟙 X) 0 0

Tactic:
simp

Result:
no goals
-- Mathlib/RingTheory/Norm/Basic.lean
theorem _root_.IntermediateField.AdjoinSimple.norm_gen_eq_one {x : L} (hx : ¬IsIntegral K x) :
    norm K (AdjoinSimple.gen K x) = 1

Proof state:
case h.intro.intro
K : Type u_4
L : Type u_5
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
x : L
s : Finset ↥K⟮x⟯
b : Basis { x_1 // x_1 ∈ s } K ↥K⟮x⟯
⊢ IsIntegral K x

Tactic:
refine .of_mem_of_fg K⟮x⟯.toSubalgebra ?_ x ?_

Result:
case h.intro.intro.refine_1
K : Type u_4
L : Type u_5
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
x : L
s : Finset ↥K⟮x⟯
b : Basis { x_1 // x_1 ∈ s } K ↥K⟮x⟯
⊢ (Subalgebra.toSubmodule K⟮x⟯.toSubalgebra).FG

case h.intro.intro.refine_2
K : Type u_4
L : Type u_5
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
x : L
s : Finset ↥K⟮x⟯
b : Basis { x_1 // x_1 ∈ s } K ↥K⟮x⟯
⊢ x ∈ K⟮x⟯.toSubalgebra

Proof state:
K : Type u_4
L : Type u_5
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
x : L
hx : ¬IsIntegral K x
⊢ (norm K) (AdjoinSimple.gen K x) = 1

Tactic:
rw [norm_eq_one_of_not_exists_basis]

Result:
case h
K : Type u_4
L : Type u_5
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
x : L
hx : ¬IsIntegral K x
⊢ ¬∃ s, Nonempty (Basis { x_1 // x_1 ∈ s } K ↥K⟮x⟯)

Proof state:
case h
K : Type u_4
L : Type u_5
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
x : L
hx : ∃ s, Nonempty (Basis { x_1 // x_1 ∈ s } K ↥K⟮x⟯)
⊢ IsIntegral K x

Tactic:
obtain ⟨s, ⟨b⟩⟩ := hx

Result:
case h.intro.intro
K : Type u_4
L : Type u_5
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
x : L
s : Finset ↥K⟮x⟯
b : Basis { x_1 // x_1 ∈ s } K ↥K⟮x⟯
⊢ IsIntegral K x

Proof state:
case h.intro.intro.refine_1
K : Type u_4
L : Type u_5
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
x : L
s : Finset ↥K⟮x⟯
b : Basis { x_1 // x_1 ∈ s } K ↥K⟮x⟯
⊢ (Subalgebra.toSubmodule K⟮x⟯.toSubalgebra).FG

Tactic:
exact (Submodule.fg_iff_finiteDimensional _).mpr (.of_fintype_basis b)

Result:
no goals

Proof state:
case h
K : Type u_4
L : Type u_5
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
x : L
hx : ¬IsIntegral K x
⊢ ¬∃ s, Nonempty (Basis { x_1 // x_1 ∈ s } K ↥K⟮x⟯)

Tactic:
contrapose! hx

Result:
case h
K : Type u_4
L : Type u_5
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
x : L
hx : ∃ s, Nonempty (Basis { x_1 // x_1 ∈ s } K ↥K⟮x⟯)
⊢ IsIntegral K x

Proof state:
case h.intro.intro.refine_2
K : Type u_4
L : Type u_5
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
x : L
s : Finset ↥K⟮x⟯
b : Basis { x_1 // x_1 ∈ s } K ↥K⟮x⟯
⊢ x ∈ K⟮x⟯.toSubalgebra

Tactic:
exact IntermediateField.subset_adjoin K _ (Set.mem_singleton x)

Result:
no goals
-- Mathlib/Data/Rat/Cast/Order.lean
@[simp] lemma one_le_cast : 1 ≤ (p : K) ↔ 1 ≤ p

Proof state:
K : Type u_5
inst✝ : LinearOrderedSemifield K
p : ℚ≥0
⊢ 1 ≤ ↑p ↔ 1 ≤ p

Tactic:
norm_cast

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Range.lean
theorem length_range (n : Nat) : length (range n) = n

Proof state:
n : Nat
⊢ (range n).length = n

Tactic:
simp only [range_eq_range', length_range']

Result:
no goals
-- Mathlib/Order/LiminfLimsup.lean
theorem bliminf_false {f : Filter β} {u : β → α} : (bliminf u f fun _ => False) = ⊤

Proof state:
α : Type u_1
β : Type u_2
inst✝ : CompleteLattice α
f : Filter β
u : β → α
⊢ (bliminf u f fun x => False) = ⊤

Tactic:
simp [bliminf_eq]

Result:
no goals
-- Mathlib/Analysis/Convex/Basic.lean
theorem convex_hyperplane {f : E → β} (h : IsLinearMap 𝕜 f) (r : β) : Convex 𝕜 { w | f w = r }

Proof state:
𝕜 : Type u_1
E : Type u_2
β : Type u_4
inst✝⁵ : OrderedSemiring 𝕜
inst✝⁴ : AddCommMonoid E
inst✝³ : Module 𝕜 E
inst✝² : OrderedAddCommMonoid β
inst✝¹ : Module 𝕜 β
inst✝ : OrderedSMul 𝕜 β
f : E → β
h : IsLinearMap 𝕜 f
r : β
⊢ Convex 𝕜 {w | f w = r}

Tactic:
simp_rw [le_antisymm_iff]

Result:
𝕜 : Type u_1
E : Type u_2
β : Type u_4
inst✝⁵ : OrderedSemiring 𝕜
inst✝⁴ : AddCommMonoid E
inst✝³ : Module 𝕜 E
inst✝² : OrderedAddCommMonoid β
inst✝¹ : Module 𝕜 β
inst✝ : OrderedSMul 𝕜 β
f : E → β
h : IsLinearMap 𝕜 f
r : β
⊢ Convex 𝕜 {w | f w ≤ r ∧ r ≤ f w}

Proof state:
𝕜 : Type u_1
E : Type u_2
β : Type u_4
inst✝⁵ : OrderedSemiring 𝕜
inst✝⁴ : AddCommMonoid E
inst✝³ : Module 𝕜 E
inst✝² : OrderedAddCommMonoid β
inst✝¹ : Module 𝕜 β
inst✝ : OrderedSMul 𝕜 β
f : E → β
h : IsLinearMap 𝕜 f
r : β
⊢ Convex 𝕜 {w | f w ≤ r ∧ r ≤ f w}

Tactic:
exact (convex_halfSpace_le h r).inter (convex_halfSpace_ge h r)

Result:
no goals
-- Mathlib/LinearAlgebra/BilinearForm/Orthogonal.lean
@[simp] lemma orthogonal_bot : B.orthogonal ⊥ = ⊤

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
B : BilinForm R M
⊢ B.orthogonal ⊥ = ⊤

Tactic:
ext

Result:
case h
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
B : BilinForm R M
x✝ : M
⊢ x✝ ∈ B.orthogonal ⊥ ↔ x✝ ∈ ⊤

Proof state:
case h
R : Type u_1
M : Type u_2
inst✝² : CommSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
B : BilinForm R M
x✝ : M
⊢ x✝ ∈ B.orthogonal ⊥ ↔ x✝ ∈ ⊤

Tactic:
simp [IsOrtho]

Result:
no goals
-- Mathlib/CategoryTheory/Functor/KanExtension/Adjunction.lean
@[reassoc (attr := simp)]
lemma ι_leftKanExtensionObjIsoColimit_inv [HasLeftKanExtension L F] (X : D)
    (f : CostructuredArrow L X) :
    colimit.ι _ f ≫ (L.leftKanExtensionObjIsoColimit F X).inv =
    (L.leftKanExtensionUnit F).app f.left ≫ (L.leftKanExtension F).map f.hom

Proof state:
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{u_4, u_1} C
inst✝³ : Category.{u_6, u_2} D
L : C ⥤ D
H : Type u_3
inst✝² : Category.{u_5, u_3} H
F : C ⥤ H
inst✝¹ : L.HasPointwiseLeftKanExtension F
inst✝ : L.HasLeftKanExtension F
X : D
f : CostructuredArrow L X
⊢ colimit.ι (proj L X ⋙ F) f ≫ (L.leftKanExtensionObjIsoColimit F X).inv =
    (L.leftKanExtensionUnit F).app f.left ≫ (L.leftKanExtension F).map f.hom

Tactic:
simp [leftKanExtensionObjIsoColimit, lanUnit]

Result:
no goals
-- Mathlib/RingTheory/GradedAlgebra/HomogeneousLocalization.lean
theorem val_add : ∀ y1 y2 : HomogeneousLocalization 𝒜 x, (y1 + y2).val = y1.val + y2.val :=
  Quotient.ind₂' fun y1 y2 ↦ by rw [← mk_add, val_mk, val_mk, val_mk, Localization.add_mk]; rfl

Proof state:
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
𝒜 : ι → Submodule R A
x : Submonoid A
inst✝² : AddCommMonoid ι
inst✝¹ : DecidableEq ι
inst✝ : GradedAlgebra 𝒜
y1 y2 : NumDenSameDeg 𝒜 x
⊢ (Quotient.mk'' y1 + Quotient.mk'' y2).val = val (Quotient.mk'' y1) + val (Quotient.mk'' y2)

Tactic:
rw [← mk_add, val_mk, val_mk, val_mk, Localization.add_mk]

Result:
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
𝒜 : ι → Submodule R A
x : Submonoid A
inst✝² : AddCommMonoid ι
inst✝¹ : DecidableEq ι
inst✝ : GradedAlgebra 𝒜
y1 y2 : NumDenSameDeg 𝒜 x
⊢ Localization.mk ↑(y1 + y2).num ⟨↑(y1 + y2).den, ⋯⟩ =
    Localization.mk (↑⟨↑y1.den, ⋯⟩ * ↑y2.num + ↑⟨↑y2.den, ⋯⟩ * ↑y1.num) (⟨↑y1.den, ⋯⟩ * ⟨↑y2.den, ⋯⟩)

Proof state:
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
𝒜 : ι → Submodule R A
x : Submonoid A
inst✝² : AddCommMonoid ι
inst✝¹ : DecidableEq ι
inst✝ : GradedAlgebra 𝒜
y1 y2 : NumDenSameDeg 𝒜 x
⊢ Localization.mk ↑(y1 + y2).num ⟨↑(y1 + y2).den, ⋯⟩ =
    Localization.mk (↑⟨↑y1.den, ⋯⟩ * ↑y2.num + ↑⟨↑y2.den, ⋯⟩ * ↑y1.num) (⟨↑y1.den, ⋯⟩ * ⟨↑y2.den, ⋯⟩)

Tactic:
rfl

Result:
no goals
-- Mathlib/RingTheory/PowerSeries/Basic.lean
theorem subsingleton_iff : Subsingleton R⟦X⟧ ↔ Subsingleton R

Proof state:
R : Type u_1
inst✝ : Semiring R
⊢ Subsingleton R⟦X⟧ ↔ Subsingleton R

Tactic:
refine ⟨fun h ↦ ?_, fun _ ↦ inferInstance⟩

Result:
R : Type u_1
inst✝ : Semiring R
h : Subsingleton R⟦X⟧
⊢ Subsingleton R

Proof state:
R : Type u_1
inst✝ : Semiring R
h : Subsingleton R⟦X⟧
⊢ Subsingleton R

Tactic:
rw [subsingleton_iff] at h ⊢

Result:
R : Type u_1
inst✝ : Semiring R
h : ∀ (x y : R⟦X⟧), x = y
⊢ ∀ (x y : R), x = y

Proof state:
R : Type u_1
inst✝ : Semiring R
h : ∀ (x y : R⟦X⟧), x = y
⊢ ∀ (x y : R), x = y

Tactic:
exact fun a b ↦ C_injective (h (C R a) (C R b))

Result:
no goals
-- Mathlib/GroupTheory/PGroup.lean
theorem of_surjective {H : Type*} [Group H] (ϕ : G →* H) (hϕ : Function.Surjective ϕ) :
    IsPGroup p H

Proof state:
p : ℕ
G : Type u_1
inst✝¹ : Group G
hG : IsPGroup p G
H : Type u_2
inst✝ : Group H
ϕ : G →* H
hϕ : Function.Surjective ⇑ϕ
h : H
g : G
hg : ϕ g = h
k : ℕ
hk : g ^ p ^ k = 1
⊢ h ^ p ^ k = 1

Tactic:
rw [← hg, ← ϕ.map_pow, hk, ϕ.map_one]

Result:
no goals

Proof state:
p : ℕ
G : Type u_1
inst✝¹ : Group G
hG : IsPGroup p G
H : Type u_2
inst✝ : Group H
ϕ : G →* H
hϕ : Function.Surjective ⇑ϕ
⊢ IsPGroup p H

Tactic:
refine fun h => Exists.elim (hϕ h) fun g hg => Exists.imp (fun k hk => ?_) (hG g)

Result:
p : ℕ
G : Type u_1
inst✝¹ : Group G
hG : IsPGroup p G
H : Type u_2
inst✝ : Group H
ϕ : G →* H
hϕ : Function.Surjective ⇑ϕ
h : H
g : G
hg : ϕ g = h
k : ℕ
hk : g ^ p ^ k = 1
⊢ h ^ p ^ k = 1
-- Mathlib/GroupTheory/Congruence/Defs.lean
theorem sInf_toSetoid (S : Set (Con M)) : (sInf S).toSetoid = sInf (toSetoid '' S) :=
  Setoid.ext fun x y =>
    ⟨fun h r ⟨c, hS, hr⟩ => by rw [← hr]; exact h c hS, fun h c hS => h c.toSetoid ⟨c, hS, rfl⟩⟩

Proof state:
M : Type u_1
inst✝ : Mul M
S : Set (Con M)
x y : M
h : (sInf S).toSetoid x y
r : Setoid M
x✝ : r ∈ toSetoid '' S
c : Con M
hS : c ∈ S
hr : c.toSetoid = r
⊢ c.toSetoid x y

Tactic:
exact h c hS

Result:
no goals

Proof state:
M : Type u_1
inst✝ : Mul M
S : Set (Con M)
x y : M
h : (sInf S).toSetoid x y
r : Setoid M
x✝ : r ∈ toSetoid '' S
c : Con M
hS : c ∈ S
hr : c.toSetoid = r
⊢ r x y

Tactic:
rw [← hr]

Result:
M : Type u_1
inst✝ : Mul M
S : Set (Con M)
x y : M
h : (sInf S).toSetoid x y
r : Setoid M
x✝ : r ∈ toSetoid '' S
c : Con M
hS : c ∈ S
hr : c.toSetoid = r
⊢ c.toSetoid x y
-- Mathlib/CategoryTheory/Localization/SmallHom.lean
@[simp]
lemma mkInv_comp_mk [HasSmallLocalizedHom.{w} W X X] [HasSmallLocalizedHom.{w} W X Y]
    [HasSmallLocalizedHom.{w} W Y X] (f : Y ⟶ X) (hf : W f) :
    (mkInv f hf).comp (mk W f) = mk W (𝟙 X) :=
  (equiv W W.Q).injective (by simp [equiv_comp])

Proof state:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
W : MorphismProperty C
X Y : C
inst✝² : HasSmallLocalizedHom W X X
inst✝¹ : HasSmallLocalizedHom W X Y
inst✝ : HasSmallLocalizedHom W Y X
f : Y ⟶ X
hf : W f
⊢ (equiv W W.Q) ((mkInv f hf).comp (mk W f)) = (equiv W W.Q) (mk W (𝟙 X))

Tactic:
simp [equiv_comp]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/TakeDrop.lean
theorem set_take {l : List α} {n m : Nat} {a : α} :
    (l.set m a).take n = (l.take n).set m a

Proof state:
α : Type u_1
l : List α
n m : Nat
a : α
⊢ take n (l.set m a) = (take n l).set m a

Tactic:
induction n generalizing l m with
| zero => simp
| succ _ hn =>
  cases l with
  | nil => simp
  | cons hd tl => cases m <;> simp_all

Result:
no goals

Proof state:
case succ.cons
α : Type u_1
a : α
n✝ : Nat
hn : ∀ {l : List α} {m : Nat}, take n✝ (l.set m a) = (take n✝ l).set m a
m : Nat
hd : α
tl : List α
⊢ take (n✝ + 1) ((hd :: tl).set m a) = (take (n✝ + 1) (hd :: tl)).set m a

Tactic:
cases m <;> simp_all

Result:
no goals

Proof state:
case zero
α : Type u_1
a : α
l : List α
m : Nat
⊢ take 0 (l.set m a) = (take 0 l).set m a

Tactic:
simp

Result:
no goals

Proof state:
case succ.nil
α : Type u_1
a : α
n✝ : Nat
hn : ∀ {l : List α} {m : Nat}, take n✝ (l.set m a) = (take n✝ l).set m a
m : Nat
⊢ take (n✝ + 1) ([].set m a) = (take (n✝ + 1) []).set m a

Tactic:
simp

Result:
no goals

Proof state:
case succ
α : Type u_1
a : α
n✝ : Nat
hn : ∀ {l : List α} {m : Nat}, take n✝ (l.set m a) = (take n✝ l).set m a
l : List α
m : Nat
⊢ take (n✝ + 1) (l.set m a) = (take (n✝ + 1) l).set m a

Tactic:
cases l with
| nil => simp
| cons hd tl => cases m <;> simp_all

Result:
no goals
-- Mathlib/Order/Interval/Set/OrdConnected.lean
@[simp]
lemma image_subtype_val_Ioc {s : Set α} [OrdConnected s] (x y : s) :
    Subtype.val '' Ioc x y = Ioc x.1 y :=
  (OrderEmbedding.subtype (· ∈ s)).image_Ioc (by simpa) x y

Proof state:
α : Type u_1
inst✝¹ : Preorder α
s : Set α
inst✝ : s.OrdConnected
x y : ↑s
⊢ (range ⇑(OrderEmbedding.subtype fun x => x ∈ s)).OrdConnected

Tactic:
simpa

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem take_size (a : Vector α n) : a.take n = a.cast (by simp)

Proof state:
α : Type ?u.451589
n : Nat
a : Vector α n
⊢ n = min n n

Tactic:
simp

Result:
no goals

Proof state:
case mk
α : Type u_1
a : Array α
⊢ { toArray := a, size_toArray := ⋯ }.take a.size = Vector.cast ⋯ { toArray := a, size_toArray := ⋯ }

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
n : Nat
a : Vector α n
⊢ a.take n = Vector.cast ⋯ a

Tactic:
rcases a with ⟨a, rfl⟩

Result:
case mk
α : Type u_1
a : Array α
⊢ { toArray := a, size_toArray := ⋯ }.take a.size = Vector.cast ⋯ { toArray := a, size_toArray := ⋯ }
-- Mathlib/SetTheory/ZFC/Basic.lean
theorem pair_eq_singleton (x : ZFSet) : {x, x} = ({x} : ZFSet)

Proof state:
case a
x z✝ : ZFSet.{u_1}
⊢ z✝ ∈ {x, x} ↔ z✝ ∈ {x}

Tactic:
simp

Result:
no goals

Proof state:
x : ZFSet.{u_1}
⊢ {x, x} = {x}

Tactic:
ext

Result:
case a
x z✝ : ZFSet.{u_1}
⊢ z✝ ∈ {x, x} ↔ z✝ ∈ {x}
-- Mathlib/GroupTheory/QuotientGroup/Basic.lean
theorem mk_nat_mul (n : ℕ) (a : R) : ((n * a : R) : R ⧸ N) = n • ↑a

Proof state:
R : Type u_1
inst✝¹ : NonAssocRing R
N : AddSubgroup R
inst✝ : N.Normal
n : ℕ
a : R
⊢ ↑(↑n * a) = n • ↑a

Tactic:
rw [← nsmul_eq_mul, mk_nsmul N a n]

Result:
no goals
-- Mathlib/Logic/Function/Basic.lean
theorem sometimes_spec {p : Prop} {α} [Nonempty α] (P : α → Prop) (f : p → α) (a : p)
    (h : P (f a)) : P (sometimes f)

Proof state:
p : Prop
α : Sort u_1
inst✝ : Nonempty α
P : α → Prop
f : p → α
a : p
h : P (f a)
⊢ P (sometimes f)

Tactic:
rwa [sometimes_eq]

Result:
no goals
-- Mathlib/Topology/MetricSpace/PiNat.lean
theorem dist_le_dist_pi_of_dist_lt {x y : ∀ i, F i} {i : ι} (h : dist x y < (1 / 2) ^ encode i) :
    dist (x i) (y i) ≤ dist x y

Proof state:
ι : Type u_2
inst✝¹ : Encodable ι
F : ι → Type u_3
inst✝ : (i : ι) → MetricSpace (F i)
x y : (i : ι) → F i
i : ι
h : dist x y < (1 / 2) ^ encode i
⊢ dist (x i) (y i) ≤ dist x y

Tactic:
simpa only [not_le.2 h, false_or] using min_le_iff.1 (min_dist_le_dist_pi x y i)

Result:
no goals
-- Mathlib/Probability/Martingale/Convergence.lean
theorem Submartingale.tendsto_eLpNorm_one_limitProcess (hf : Submartingale f ℱ μ)
    (hunif : UniformIntegrable f 1 μ) :
    Tendsto (fun n => eLpNorm (f n - ℱ.limitProcess f μ) 1 μ) atTop (𝓝 0)

Proof state:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hunif : UniformIntegrable f 1 μ
⊢ Tendsto (fun n => eLpNorm (f n - limitProcess f ℱ μ) 1 μ) atTop (𝓝 0)

Tactic:
obtain ⟨R, hR⟩ := hunif.2.2

Result:
case intro
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hunif : UniformIntegrable f 1 μ
R : ℝ≥0
hR : ∀ (i : ℕ), eLpNorm (f i) 1 μ ≤ ↑R
⊢ Tendsto (fun n => eLpNorm (f n - limitProcess f ℱ μ) 1 μ) atTop (𝓝 0)

Proof state:
case intro
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hunif : UniformIntegrable f 1 μ
R : ℝ≥0
hR : ∀ (i : ℕ), eLpNorm (f i) 1 μ ≤ ↑R
⊢ Tendsto (fun n => eLpNorm (f n - limitProcess f ℱ μ) 1 μ) atTop (𝓝 0)

Tactic:
have hmeas : ∀ n, AEStronglyMeasurable (f n) μ := fun n =>
  ((hf.stronglyMeasurable n).mono (ℱ.le _)).aestronglyMeasurable

Result:
case intro
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hunif : UniformIntegrable f 1 μ
R : ℝ≥0
hR : ∀ (i : ℕ), eLpNorm (f i) 1 μ ≤ ↑R
hmeas : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
⊢ Tendsto (fun n => eLpNorm (f n - limitProcess f ℱ μ) 1 μ) atTop (𝓝 0)

Proof state:
case intro
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
ℱ : Filtration ℕ m0
f : ℕ → Ω → ℝ
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
hunif : UniformIntegrable f 1 μ
R : ℝ≥0
hR : ∀ (i : ℕ), eLpNorm (f i) 1 μ ≤ ↑R
hmeas : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
⊢ Tendsto (fun n => eLpNorm (f n - limitProcess f ℱ μ) 1 μ) atTop (𝓝 0)

Tactic:
exact tendsto_Lp_finite_of_tendstoInMeasure le_rfl ENNReal.one_ne_top hmeas
  (memLp_limitProcess_of_eLpNorm_bdd hmeas hR) hunif.2.1
  (tendstoInMeasure_of_tendsto_ae hmeas <| hf.ae_tendsto_limitProcess hR)

Result:
no goals
-- Mathlib/Algebra/Module/LocalizedModule/Basic.lean
theorem mk'_sub {M M' : Type*} [AddCommGroup M] [AddCommGroup M'] [Module R M] [Module R M']
    (f : M →ₗ[R] M') [IsLocalizedModule S f] (m₁ m₂ : M) (s : S) :
    mk' f (m₁ - m₂) s = mk' f m₁ s - mk' f m₂ s

Proof state:
R : Type u_1
inst✝⁵ : CommSemiring R
S : Submonoid R
M : Type u_6
M' : Type u_7
inst✝⁴ : AddCommGroup M
inst✝³ : AddCommGroup M'
inst✝² : Module R M
inst✝¹ : Module R M'
f : M →ₗ[R] M'
inst✝ : IsLocalizedModule S f
m₁ m₂ : M
s : ↥S
⊢ mk' f (m₁ - m₂) s = mk' f m₁ s - mk' f m₂ s

Tactic:
rw [sub_eq_add_neg, sub_eq_add_neg, mk'_add, mk'_neg]

Result:
no goals
-- Mathlib/FieldTheory/Perfect.lean
theorem roots_X_pow_char_pow_sub_C_pow {y : R} {m : ℕ} :
    ((X ^ p ^ n - C y) ^ m).roots = (m * p ^ n) • {(iterateFrobeniusEquiv R p n).symm y}

Proof state:
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsDomain R
p n : ℕ
inst✝¹ : ExpChar R p
inst✝ : PerfectRing R p
y : R
m : ℕ
⊢ ((X ^ p ^ n - C y) ^ m).roots = (m * p ^ n) • {(iterateFrobeniusEquiv R p n).symm y}

Tactic:
rw [roots_pow, roots_X_pow_char_pow_sub_C, mul_smul]

Result:
no goals
-- Mathlib/Topology/Instances/NNReal/Lemmas.lean
theorem _root_.Real.comap_toNNReal_atTop : comap Real.toNNReal atTop = atTop

Proof state:
a : ℝ
ha : 0 < a
⊢ Set.Ioi a ∈ comap Real.toNNReal atTop

Tactic:
filter_upwards [preimage_mem_comap (Ioi_mem_atTop a.toNNReal)] with x hx

Result:
case h
a : ℝ
ha : 0 < a
x : ℝ
hx : x ∈ Real.toNNReal ⁻¹' Set.Ioi a.toNNReal
⊢ x ∈ Set.Ioi a

Proof state:
case h
a : ℝ
ha : 0 < a
x : ℝ
hx : x ∈ Real.toNNReal ⁻¹' Set.Ioi a.toNNReal
⊢ x ∈ Set.Ioi a

Tactic:
exact (Real.toNNReal_lt_toNNReal_iff_of_nonneg ha.le).1 hx

Result:
no goals

Proof state:
⊢ comap Real.toNNReal atTop ≤ atTop

Tactic:
refine (atTop_basis_Ioi' 0).ge_iff.2 fun a ha ↦ ?_

Result:
a : ℝ
ha : 0 < a
⊢ Set.Ioi a ∈ comap Real.toNNReal atTop

Proof state:
⊢ comap Real.toNNReal atTop = atTop

Tactic:
refine le_antisymm ?_ tendsto_real_toNNReal_atTop.le_comap

Result:
⊢ comap Real.toNNReal atTop ≤ atTop
-- Mathlib/Tactic/CategoryTheory/Coherence/Basic.lean
theorem mk_eq_of_cons {C : Type u} [CategoryStruct.{v} C]
    {f₁ f₂ f₃ f₄ : C}
    (α α' : f₁ ⟶ f₂) (η η' : f₂ ⟶ f₃) (ηs ηs' : f₃ ⟶ f₄)
    (e_α : α = α') (e_η : η = η') (e_ηs : ηs = ηs') :
    α ≫ η ≫ ηs = α' ≫ η' ≫ ηs'

Proof state:
C : Type u
inst✝ : CategoryStruct.{v, u} C
f₁ f₂ f₃ f₄ : C
α α' : f₁ ⟶ f₂
η η' : f₂ ⟶ f₃
ηs ηs' : f₃ ⟶ f₄
e_α : α = α'
e_η : η = η'
e_ηs : ηs = ηs'
⊢ α ≫ η ≫ ηs = α' ≫ η' ≫ ηs'

Tactic:
simp [e_α, e_η, e_ηs]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Bool.lean
theorem coe_false_iff_true  : ∀{a b : Bool}, (a = false ↔ b) ↔ (!a) = b

Proof state:
⊢ ∀ {a b : Bool}, (a = false ↔ b = true) ↔ (!a) = b

Tactic:
decide

Result:
no goals
-- Mathlib/Algebra/BigOperators/Group/Multiset/Defs.lean
theorem prod_eq_foldl (s : Multiset α) :
    prod s = foldl (· * ·) 1 s :=
  (foldr_swap _ _ _).trans (by simp [mul_comm])

Proof state:
α : Type u_3
inst✝ : CommMonoid α
s : Multiset α
⊢ foldl (fun x y => y * x) 1 s = foldl (fun x1 x2 => x1 * x2) 1 s

Tactic:
simp [mul_comm]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Omega/Int.lean
theorem natAbs_dichotomy {a : Int} : 0 ≤ a ∧ a.natAbs = a ∨ a < 0 ∧ a.natAbs = -a

Proof state:
case neg.h
a : Int
h : a < 0
⊢ a < 0 ∧ -a = -a

Tactic:
simp_all

Result:
no goals

Proof state:
a : Int
⊢ 0 ≤ a ∧ ↑a.natAbs = a ∨ a < 0 ∧ ↑a.natAbs = -a

Tactic:
by_cases h : 0 ≤ a

Result:
case pos
a : Int
h : 0 ≤ a
⊢ 0 ≤ a ∧ ↑a.natAbs = a ∨ a < 0 ∧ ↑a.natAbs = -a

case neg
a : Int
h : ¬0 ≤ a
⊢ 0 ≤ a ∧ ↑a.natAbs = a ∨ a < 0 ∧ ↑a.natAbs = -a

Proof state:
case neg.h
a : Int
h : a < 0
⊢ a < 0 ∧ ↑a.natAbs = -a

Tactic:
rw [Int.ofNat_natAbs_of_nonpos (Int.le_of_lt h)]

Result:
case neg.h
a : Int
h : a < 0
⊢ a < 0 ∧ -a = -a

Proof state:
case pos.h
a : Int
h : 0 ≤ a
⊢ 0 ≤ a ∧ ↑a.natAbs = a

Tactic:
simp_all [Int.natAbs_of_nonneg]

Result:
no goals

Proof state:
case neg
a : Int
h : ¬0 ≤ a
⊢ 0 ≤ a ∧ ↑a.natAbs = a ∨ a < 0 ∧ ↑a.natAbs = -a

Tactic:
right

Result:
case neg.h
a : Int
h : ¬0 ≤ a
⊢ a < 0 ∧ ↑a.natAbs = -a

Proof state:
case pos
a : Int
h : 0 ≤ a
⊢ 0 ≤ a ∧ ↑a.natAbs = a ∨ a < 0 ∧ ↑a.natAbs = -a

Tactic:
left

Result:
case pos.h
a : Int
h : 0 ≤ a
⊢ 0 ≤ a ∧ ↑a.natAbs = a

Proof state:
case neg.h
a : Int
h : ¬0 ≤ a
⊢ a < 0 ∧ ↑a.natAbs = -a

Tactic:
rw [Int.not_le] at h

Result:
case neg.h
a : Int
h : a < 0
⊢ a < 0 ∧ ↑a.natAbs = -a
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/MapIdx.lean
theorem mapFinIdx_eq_zipIdx_map {l : Array α} {f : (i : Nat) → α → (h : i < l.size) → β} :
    l.mapFinIdx f = l.zipIdx.attach.map
      fun ⟨⟨x, i⟩, m⟩ =>
        f i x (by simp [mk_mem_zipIdx_iff_getElem?, getElem?_eq_some_iff] at m; exact m.1)

Proof state:
α : Type ?u.59452
β : Type ?u.59474
l : Array α
f : (i : Nat) → α → i < l.size → β
x✝ : { x // x ∈ l.zipIdx }
x : α
i : Nat
m : ∃ h, l[i] = x
⊢ i < l.size

Tactic:
exact m.1

Result:
no goals

Proof state:
α : Type ?u.59452
β : Type ?u.59474
l : Array α
f : (i : Nat) → α → i < l.size → β
x✝ : { x // x ∈ l.zipIdx }
x : α
i : Nat
m : (x, i) ∈ l.zipIdx
⊢ i < l.size

Tactic:
simp [mk_mem_zipIdx_iff_getElem?, getElem?_eq_some_iff] at m

Result:
α : Type ?u.59452
β : Type ?u.59474
l : Array α
f : (i : Nat) → α → i < l.size → β
x✝ : { x // x ∈ l.zipIdx }
x : α
i : Nat
m : ∃ h, l[i] = x
⊢ i < l.size

Proof state:
α : Type u_1
β : Type u_2
l : Array α
f : (i : Nat) → α → i < l.size → β
⊢ l.mapFinIdx f =
    map
      (fun x =>
        match x with
        | ⟨(x, i), m⟩ => f i x ⋯)
      l.zipIdx.attach

Tactic:
ext <;> simp

Result:
no goals
-- Mathlib/Data/Matrix/Hadamard.lean
theorem one_hadamard : (1 : Matrix n n α) ⊙ M = diagonal fun i => M i i

Proof state:
case a
α : Type u_1
n : Type u_3
inst✝¹ : DecidableEq n
inst✝ : MulZeroOneClass α
M : Matrix n n α
i j : n
⊢ (1 ⊙ M) i j = diagonal (fun i => M i i) i j

Tactic:
by_cases h : i = j <;> simp [h]

Result:
no goals

Proof state:
α : Type u_1
n : Type u_3
inst✝¹ : DecidableEq n
inst✝ : MulZeroOneClass α
M : Matrix n n α
⊢ 1 ⊙ M = diagonal fun i => M i i

Tactic:
ext i j

Result:
case a
α : Type u_1
n : Type u_3
inst✝¹ : DecidableEq n
inst✝ : MulZeroOneClass α
M : Matrix n n α
i j : n
⊢ (1 ⊙ M) i j = diagonal (fun i => M i i) i j
-- Mathlib/Data/Finset/NAry.lean
theorem mem_image₂_iff (hf : Injective2 f) : f a b ∈ image₂ f s t ↔ a ∈ s ∧ b ∈ t

Proof state:
α : Type u_1
β : Type u_3
γ : Type u_5
inst✝ : DecidableEq γ
f : α → β → γ
s : Finset α
t : Finset β
a : α
b : β
hf : Injective2 f
⊢ f a b ∈ image₂ f s t ↔ a ∈ s ∧ b ∈ t

Tactic:
rw [← mem_coe, coe_image₂, mem_image2_iff hf, mem_coe, mem_coe]

Result:
no goals