harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/Normed/Group/SemiNormedGrp/Kernels.lean
theorem explicitCokernelDesc_unique {X Y Z : SemiNormedGrp.{u}} {f : X ⟶ Y} {g : Y ⟶ Z}
    (w : f ≫ g = 0) (e : explicitCokernel f ⟶ Z) (he : explicitCokernelπ f ≫ e = g) :
    e = explicitCokernelDesc w

Proof state:
X Y Z : SemiNormedGrp
f : X ⟶ Y
g : Y ⟶ Z
w : f ≫ g = 0
e : explicitCokernel f ⟶ Z
he : explicitCokernelπ f ≫ e = g
⊢ e = explicitCokernelDesc w

Tactic:
apply (isColimitCokernelCocone f).uniq (Cofork.ofπ g (by simp [w]))

Result:
case x
X Y Z : SemiNormedGrp
f : X ⟶ Y
g : Y ⟶ Z
w : f ≫ g = 0
e : explicitCokernel f ⟶ Z
he : explicitCokernelπ f ≫ e = g
⊢ ∀ (j : WalkingParallelPair), (cokernelCocone f).ι.app j ≫ e = (Cofork.ofπ g ⋯).ι.app j

Proof state:
case x
X Y Z : SemiNormedGrp
f : X ⟶ Y
g : Y ⟶ Z
w : f ≫ g = 0
e : explicitCokernel f ⟶ Z
he : explicitCokernelπ f ≫ e = g
⊢ ∀ (j : WalkingParallelPair), (cokernelCocone f).ι.app j ≫ e = (Cofork.ofπ g ⋯).ι.app j

Tactic:
rintro (_ | _)

Result:
case x.zero
X Y Z : SemiNormedGrp
f : X ⟶ Y
g : Y ⟶ Z
w : f ≫ g = 0
e : explicitCokernel f ⟶ Z
he : explicitCokernelπ f ≫ e = g
⊢ (cokernelCocone f).ι.app WalkingParallelPair.zero ≫ e = (Cofork.ofπ g ⋯).ι.app WalkingParallelPair.zero

case x.one
X Y Z : SemiNormedGrp
f : X ⟶ Y
g : Y ⟶ Z
w : f ≫ g = 0
e : explicitCokernel f ⟶ Z
he : explicitCokernelπ f ≫ e = g
⊢ (cokernelCocone f).ι.app WalkingParallelPair.one ≫ e = (Cofork.ofπ g ⋯).ι.app WalkingParallelPair.one

Proof state:
X Y Z : SemiNormedGrp
f : X ⟶ Y
g : Y ⟶ Z
w : f ≫ g = 0
e : explicitCokernel f ⟶ Z
he : explicitCokernelπ f ≫ e = g
⊢ f ≫ g = 0 ≫ g

Tactic:
simp [w]

Result:
no goals

Proof state:
case h.e'_2.h
X Y Z : SemiNormedGrp
f : X ⟶ Y
g : Y ⟶ Z
w : f ≫ g = 0
e : explicitCokernel f ⟶ Z
he : explicitCokernelπ f ≫ e = g
e_1✝ : ((parallelPair f 0).obj WalkingParallelPair.zero ⟶ (Cofork.ofπ g ⋯).pt) = (X ⟶ Z)
⊢ (cokernelCocone f).ι.app WalkingParallelPair.zero ≫ e = 0

Tactic:
simp

Result:
no goals

Proof state:
case x.zero
X Y Z : SemiNormedGrp
f : X ⟶ Y
g : Y ⟶ Z
w : f ≫ g = 0
e : explicitCokernel f ⟶ Z
he : explicitCokernelπ f ≫ e = g
⊢ (cokernelCocone f).ι.app WalkingParallelPair.zero ≫ e = (Cofork.ofπ g ⋯).ι.app WalkingParallelPair.zero

Tactic:
convert w.symm

Result:
case h.e'_2.h
X Y Z : SemiNormedGrp
f : X ⟶ Y
g : Y ⟶ Z
w : f ≫ g = 0
e : explicitCokernel f ⟶ Z
he : explicitCokernelπ f ≫ e = g
e_1✝ : ((parallelPair f 0).obj WalkingParallelPair.zero ⟶ (Cofork.ofπ g ⋯).pt) = (X ⟶ Z)
⊢ (cokernelCocone f).ι.app WalkingParallelPair.zero ≫ e = 0

Proof state:
case x.one
X Y Z : SemiNormedGrp
f : X ⟶ Y
g : Y ⟶ Z
w : f ≫ g = 0
e : explicitCokernel f ⟶ Z
he : explicitCokernelπ f ≫ e = g
⊢ (cokernelCocone f).ι.app WalkingParallelPair.one ≫ e = (Cofork.ofπ g ⋯).ι.app WalkingParallelPair.one

Tactic:
exact he

Result:
no goals
-- Mathlib/Data/Finset/Card.lean
theorem card_image_le [DecidableEq β] : #(s.image f) ≤ #s

Proof state:
α : Type u_1
β : Type u_2
s : Finset α
f : α → β
inst✝ : DecidableEq β
⊢ #(image f s) ≤ #s

Tactic:
simpa only [card_map] using (s.1.map f).toFinset_card_le

Result:
no goals
-- Mathlib/Topology/Order/ScottTopology.lean
lemma isOpen_iff_isUpperSet_and_scottHausdorff_open [IsScott α D] :
    IsOpen s ↔ IsUpperSet s ∧ IsOpen[scottHausdorff α D] s

Proof state:
α : Type u_1
D : Set (Set α)
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
s : Set α
inst✝ : IsScott α D
⊢ IsOpen s ↔ IsUpperSet s ∧ IsOpen s

Tactic:
rfl

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Monadic.lean
theorem foldlM_filter [Monad m] [LawfulMonad m] (p : α → Bool) (g : β → α → m β) (l : List α) (init : β) :
    (l.filter p).foldlM g init =
      l.foldlM (fun x y => if p y then g x y else pure x) init

Proof state:
case cons
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
p : α → Bool
g : β → α → m β
a : α
l : List α
ih :
  ∀ (init : β), List.foldlM g init (filter p l) = List.foldlM (fun x y => if p y = true then g x y else pure x) init l
init : β
⊢ List.foldlM g init (if p a = true then a :: filter p l else filter p l) = do
    let init ← if p a = true then g init a else pure init
    List.foldlM (fun x y => if p y = true then g x y else pure x) init l

Tactic:
split <;> simp [ih]

Result:
no goals

Proof state:
case nil
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
p : α → Bool
g : β → α → m β
init : β
⊢ List.foldlM g init (filter p []) = List.foldlM (fun x y => if p y = true then g x y else pure x) init []

Tactic:
rfl

Result:
no goals

Proof state:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
p : α → Bool
g : β → α → m β
l : List α
init : β
⊢ List.foldlM g init (filter p l) = List.foldlM (fun x y => if p y = true then g x y else pure x) init l

Tactic:
induction l generalizing init with
| nil => rfl
| cons a l ih =>
  simp only [filter_cons, foldlM_cons]
  split <;> simp [ih]

Result:
no goals

Proof state:
case cons
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
p : α → Bool
g : β → α → m β
a : α
l : List α
ih :
  ∀ (init : β), List.foldlM g init (filter p l) = List.foldlM (fun x y => if p y = true then g x y else pure x) init l
init : β
⊢ List.foldlM g init (filter p (a :: l)) = List.foldlM (fun x y => if p y = true then g x y else pure x) init (a :: l)

Tactic:
simp only [filter_cons, foldlM_cons]

Result:
case cons
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
p : α → Bool
g : β → α → m β
a : α
l : List α
ih :
  ∀ (init : β), List.foldlM g init (filter p l) = List.foldlM (fun x y => if p y = true then g x y else pure x) init l
init : β
⊢ List.foldlM g init (if p a = true then a :: filter p l else filter p l) = do
    let init ← if p a = true then g init a else pure init
    List.foldlM (fun x y => if p y = true then g x y else pure x) init l
-- Mathlib/CategoryTheory/Shift/ShiftSequence.lean
@[simp]
lemma shiftIso_zero_inv_app (a : M) (X : C) :
    (F.shiftIso 0 a a (zero_add a)).inv.app X =
      (shift F a).map ((shiftFunctorZero C M).inv.app X)

Proof state:
C : Type u_1
A : Type u_2
inst✝⁴ : Category.{u_6, u_1} C
inst✝³ : Category.{u_5, u_2} A
F : C ⥤ A
M : Type u_3
inst✝² : AddMonoid M
inst✝¹ : HasShift C M
inst✝ : F.ShiftSequence M
a : M
X : C
⊢ (F.shiftIso 0 a a ⋯).inv.app X = (F.shift a).map ((shiftFunctorZero C M).inv.app X)

Tactic:
simp [F.shiftIso_zero a]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/Lemmas.lean
theorem sub_sub (a b c : Int) : a - b - c = a - (b + c)

Proof state:
a b c : Int
⊢ a - b - c = a - (b + c)

Tactic:
simp [Int.sub_eq_add_neg, Int.add_assoc]

Result:
no goals
-- Mathlib/Order/LiminfLimsup.lean
/-- In linear orders, frequent boundedness from below implies coboundedness for `≤`. -/
lemma IsCobounded.of_frequently_ge [LinearOrder α] {l : α} (freq_ge : ∃ᶠ x in f, l ≤ x) :
    IsCobounded (· ≤ ·) f

Proof state:
case inr.intro.intro.intro
α : Type u_1
f : Filter α
inst✝ : LinearOrder α
l : α
freq_ge : ∃ᶠ (x : α) in f, l ≤ x
l' : α
hl' : l' < l
u : α
hu : ∀ᶠ (x : α) in f, (fun x1 x2 => x1 ≤ x2) x u
w : α
l_le_w : l ≤ w
w_le_u : w ≤ u
⊢ l' ≤ u

Tactic:
exact hl'.le.trans (l_le_w.trans w_le_u)

Result:
no goals

Proof state:
α : Type u_1
f : Filter α
inst✝ : LinearOrder α
l : α
freq_ge : ∃ᶠ (x : α) in f, l ≤ x
⊢ IsCobounded (fun x1 x2 => x1 ≤ x2) f

Tactic:
rcases isBot_or_exists_lt l with lbot | ⟨l', hl'⟩

Result:
case inl
α : Type u_1
f : Filter α
inst✝ : LinearOrder α
l : α
freq_ge : ∃ᶠ (x : α) in f, l ≤ x
lbot : IsBot l
⊢ IsCobounded (fun x1 x2 => x1 ≤ x2) f

case inr.intro
α : Type u_1
f : Filter α
inst✝ : LinearOrder α
l : α
freq_ge : ∃ᶠ (x : α) in f, l ≤ x
l' : α
hl' : l' < l
⊢ IsCobounded (fun x1 x2 => x1 ≤ x2) f

Proof state:
case inr.intro
α : Type u_1
f : Filter α
inst✝ : LinearOrder α
l : α
freq_ge : ∃ᶠ (x : α) in f, l ≤ x
l' : α
hl' : l' < l
⊢ IsCobounded (fun x1 x2 => x1 ≤ x2) f

Tactic:
refine ⟨l', fun u hu ↦ ?_⟩

Result:
case inr.intro
α : Type u_1
f : Filter α
inst✝ : LinearOrder α
l : α
freq_ge : ∃ᶠ (x : α) in f, l ≤ x
l' : α
hl' : l' < l
u : α
hu : ∀ᶠ (x : α) in f, (fun x1 x2 => x1 ≤ x2) x u
⊢ (fun x1 x2 => x1 ≤ x2) l' u

Proof state:
case inr.intro
α : Type u_1
f : Filter α
inst✝ : LinearOrder α
l : α
freq_ge : ∃ᶠ (x : α) in f, l ≤ x
l' : α
hl' : l' < l
u : α
hu : ∀ᶠ (x : α) in f, (fun x1 x2 => x1 ≤ x2) x u
⊢ (fun x1 x2 => x1 ≤ x2) l' u

Tactic:
obtain ⟨w, l_le_w, w_le_u⟩ := (freq_ge.and_eventually hu).exists

Result:
case inr.intro.intro.intro
α : Type u_1
f : Filter α
inst✝ : LinearOrder α
l : α
freq_ge : ∃ᶠ (x : α) in f, l ≤ x
l' : α
hl' : l' < l
u : α
hu : ∀ᶠ (x : α) in f, (fun x1 x2 => x1 ≤ x2) x u
w : α
l_le_w : l ≤ w
w_le_u : w ≤ u
⊢ l' ≤ u

Proof state:
case inl
α : Type u_1
f : Filter α
inst✝ : LinearOrder α
l : α
freq_ge : ∃ᶠ (x : α) in f, l ≤ x
lbot : IsBot l
⊢ IsCobounded (fun x1 x2 => x1 ≤ x2) f

Tactic:
exact ⟨l, fun x _ ↦ lbot x⟩

Result:
no goals
-- Mathlib/RingTheory/KrullDimension/Basic.lean
theorem Ring.jacobson_eq_nilradical_of_krullDimLE_zero (R) [CommRing R] [KrullDimLE 0 R] :
    jacobson R = nilradical R

Proof state:
R : Type u_3
inst✝¹ : CommRing R
inst✝ : KrullDimLE 0 R
I : Ideal R
hI : I ∈ {J | J.IsPrime}
⊢ I ∈ {m | IsCoatom m}

Tactic:
rw [Set.mem_def, Set.setOf_app_iff] at hI

Result:
R : Type u_3
inst✝¹ : CommRing R
inst✝ : KrullDimLE 0 R
I : Ideal R
hI : I.IsPrime
⊢ I ∈ {m | IsCoatom m}

Proof state:
R : Type u_3
inst✝¹ : CommRing R
inst✝ : KrullDimLE 0 R
⊢ jacobson R = nilradical R

Tactic:
refine (nilradical_le_jacobson R).antisymm' (nilradical_eq_sInf R ▸ le_sInf fun I hI ↦ sInf_le ?_)

Result:
R : Type u_3
inst✝¹ : CommRing R
inst✝ : KrullDimLE 0 R
I : Ideal R
hI : I ∈ {J | J.IsPrime}
⊢ I ∈ {m | IsCoatom m}

Proof state:
R : Type u_3
inst✝¹ : CommRing R
inst✝ : KrullDimLE 0 R
I : Ideal R
hI : I.IsPrime
⊢ I ∈ {m | IsCoatom m}

Tactic:
exact Ideal.IsMaximal.out

Result:
no goals
-- Mathlib/Topology/Algebra/Module/Basic.lean
theorem Submodule.closure_subset_topologicalClosure_span (s : Set M) :
    closure s ⊆ (span R s).topologicalClosure

Proof state:
R : Type u
M : Type v
inst✝⁵ : Semiring R
inst✝⁴ : TopologicalSpace M
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : ContinuousConstSMul R M
inst✝ : ContinuousAdd M
s : Set M
⊢ closure s ⊆ ↑(span R s).topologicalClosure

Tactic:
rw [Submodule.topologicalClosure_coe]

Result:
R : Type u
M : Type v
inst✝⁵ : Semiring R
inst✝⁴ : TopologicalSpace M
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : ContinuousConstSMul R M
inst✝ : ContinuousAdd M
s : Set M
⊢ closure s ⊆ closure ↑(span R s)

Proof state:
R : Type u
M : Type v
inst✝⁵ : Semiring R
inst✝⁴ : TopologicalSpace M
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : ContinuousConstSMul R M
inst✝ : ContinuousAdd M
s : Set M
⊢ closure s ⊆ closure ↑(span R s)

Tactic:
exact closure_mono subset_span

Result:
no goals
-- Mathlib/Topology/Separation/Basic.lean
theorem IsCompact.closure {K : Set X} (hK : IsCompact K) : IsCompact (closure K)

Proof state:
case intro
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : R1Space X
K : Set X
hK : IsCompact K
ι✝ : Type u_1
U : ι✝ → Set X
hUo : ∀ (i : ι✝), IsOpen (U i)
hKU : closure K ⊆ ⋃ i, U i
t : Finset ι✝
ht : K ⊆ ⋃ i ∈ t, U i
⊢ ∃ t, closure K ⊆ ⋃ i ∈ t, U i

Tactic:
exact ⟨t, hK.closure_subset_of_isOpen (isOpen_biUnion fun _ _ ↦ hUo _) ht⟩

Result:
no goals

Proof state:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : R1Space X
K : Set X
hK : IsCompact K
ι✝ : Type u_1
U : ι✝ → Set X
hUo : ∀ (i : ι✝), IsOpen (U i)
hKU : closure K ⊆ ⋃ i, U i
⊢ ∃ t, closure K ⊆ ⋃ i ∈ t, U i

Tactic:
rcases hK.elim_finite_subcover U hUo (subset_closure.trans hKU) with ⟨t, ht⟩

Result:
case intro
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : R1Space X
K : Set X
hK : IsCompact K
ι✝ : Type u_1
U : ι✝ → Set X
hUo : ∀ (i : ι✝), IsOpen (U i)
hKU : closure K ⊆ ⋃ i, U i
t : Finset ι✝
ht : K ⊆ ⋃ i ∈ t, U i
⊢ ∃ t, closure K ⊆ ⋃ i ∈ t, U i

Proof state:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : R1Space X
K : Set X
hK : IsCompact K
⊢ IsCompact (closure K)

Tactic:
refine isCompact_of_finite_subcover fun U hUo hKU ↦ ?_

Result:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : R1Space X
K : Set X
hK : IsCompact K
ι✝ : Type u_1
U : ι✝ → Set X
hUo : ∀ (i : ι✝), IsOpen (U i)
hKU : closure K ⊆ ⋃ i, U i
⊢ ∃ t, closure K ⊆ ⋃ i ∈ t, U i
-- Mathlib/NumberTheory/Pell.lean
theorem x_pow_pos {a : Solution₁ d} (hax : 0 < a.x) (n : ℕ) : 0 < (a ^ n).x

Proof state:
d : ℤ
a : Solution₁ d
hax : 0 < a.x
n : ℕ
⊢ 0 < (a ^ n).x

Tactic:
induction n with
| zero => simp only [pow_zero, x_one, zero_lt_one]
| succ n ih => rw [pow_succ]; exact x_mul_pos ih hax

Result:
no goals

Proof state:
case succ
d : ℤ
a : Solution₁ d
hax : 0 < a.x
n : ℕ
ih : 0 < (a ^ n).x
⊢ 0 < (a ^ (n + 1)).x

Tactic:
rw [pow_succ]

Result:
case succ
d : ℤ
a : Solution₁ d
hax : 0 < a.x
n : ℕ
ih : 0 < (a ^ n).x
⊢ 0 < (a ^ n * a).x

Proof state:
case zero
d : ℤ
a : Solution₁ d
hax : 0 < a.x
⊢ 0 < (a ^ 0).x

Tactic:
simp only [pow_zero, x_one, zero_lt_one]

Result:
no goals

Proof state:
case succ
d : ℤ
a : Solution₁ d
hax : 0 < a.x
n : ℕ
ih : 0 < (a ^ n).x
⊢ 0 < (a ^ n * a).x

Tactic:
exact x_mul_pos ih hax

Result:
no goals
-- Mathlib/Tactic/CategoryTheory/Bicategory/Datatypes.lean
theorem structuralIso_inv {f g : a ⟶ b} (η : f ≅ g) :
    η.symm.hom = η.inv

Proof state:
B : Type u
inst✝ : Bicategory B
a b : B
f g : a ⟶ b
η : f ≅ g
⊢ η.symm.hom = η.inv

Tactic:
simp only [Iso.symm_hom]

Result:
no goals
-- Mathlib/Algebra/Homology/ShortComplex/Homology.lean
lemma liftCycles_homologyπ_eq_zero_of_boundary [S.HasHomology]
    (k : A ⟶ S.X₂) (x : A ⟶ S.X₁) (hx : k = x ≫ S.f) :
    S.liftCycles k (by rw [hx, assoc, S.zero, comp_zero]) ≫ S.homologyπ = 0

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
S S₁ S₂ S₃ S₄ : ShortComplex C
φ : S₁ ⟶ S₂
h₁ : S₁.HomologyData
h₂ : S₂.HomologyData
A : C
inst✝ : S.HasHomology
k : A ⟶ S.X₂
x : A ⟶ S.X₁
hx : k = x ≫ S.f
⊢ k ≫ S.g = 0

Tactic:
rw [hx, assoc, S.zero, comp_zero]

Result:
no goals

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
S : ShortComplex C
A : C
inst✝ : S.HasHomology
k : A ⟶ S.X₂
x : A ⟶ S.X₁
hx : k = x ≫ S.f
⊢ S.liftCycles k ⋯ ≫ S.leftHomologyπ ≫ S.leftHomologyIso.hom = 0

Tactic:
rw [S.liftCycles_leftHomologyπ_eq_zero_of_boundary_assoc k x hx, zero_comp]

Result:
no goals

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
S : ShortComplex C
A : C
inst✝ : S.HasHomology
k : A ⟶ S.X₂
x : A ⟶ S.X₁
hx : k = x ≫ S.f
⊢ S.liftCycles k ⋯ ≫ S.homologyπ = 0

Tactic:
dsimp only [homologyπ]

Result:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
S : ShortComplex C
A : C
inst✝ : S.HasHomology
k : A ⟶ S.X₂
x : A ⟶ S.X₁
hx : k = x ≫ S.f
⊢ S.liftCycles k ⋯ ≫ S.leftHomologyπ ≫ S.leftHomologyIso.hom = 0
-- Mathlib/Algebra/BigOperators/Finprod.lean
theorem finsum_smul {R M : Type*} [Ring R] [AddCommGroup M] [Module R M] [NoZeroSMulDivisors R M]
    (f : ι → R) (x : M) : (∑ᶠ i, f i) • x = ∑ᶠ i, f i • x

Proof state:
case inr
ι : Sort u_6
R : Type u_7
M : Type u_8
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
f : ι → R
x : M
hx : x ≠ 0
⊢ (∑ᶠ (i : ι), f i) • x = ∑ᶠ (i : ι), f i • x

Tactic:
exact ((smulAddHom R M).flip x).map_finsum_of_injective (smul_left_injective R hx) _

Result:
no goals

Proof state:
case inl
ι : Sort u_6
R : Type u_7
M : Type u_8
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
f : ι → R
⊢ (∑ᶠ (i : ι), f i) • 0 = ∑ᶠ (i : ι), f i • 0

Tactic:
simp

Result:
no goals

Proof state:
ι : Sort u_6
R : Type u_7
M : Type u_8
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
f : ι → R
x : M
⊢ (∑ᶠ (i : ι), f i) • x = ∑ᶠ (i : ι), f i • x

Tactic:
rcases eq_or_ne x 0 with (rfl | hx)

Result:
case inl
ι : Sort u_6
R : Type u_7
M : Type u_8
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
f : ι → R
⊢ (∑ᶠ (i : ι), f i) • 0 = ∑ᶠ (i : ι), f i • 0

case inr
ι : Sort u_6
R : Type u_7
M : Type u_8
inst✝³ : Ring R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
f : ι → R
x : M
hx : x ≠ 0
⊢ (∑ᶠ (i : ι), f i) • x = ∑ᶠ (i : ι), f i • x
-- Mathlib/Analysis/LocallyConvex/BalancedCoreHull.lean
theorem Balanced.balancedHull_subset_of_subset (ht : Balanced 𝕜 t) (h : s ⊆ t) :
    balancedHull 𝕜 s ⊆ t

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝¹ : SeminormedRing 𝕜
inst✝ : SMul 𝕜 E
s t : Set E
ht : Balanced 𝕜 t
h : s ⊆ t
x : E
hx : x ∈ balancedHull 𝕜 s
⊢ x ∈ t

Tactic:
obtain ⟨r, hr, y, hy, rfl⟩ := mem_balancedHull_iff.1 hx

Result:
case intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝¹ : SeminormedRing 𝕜
inst✝ : SMul 𝕜 E
s t : Set E
ht : Balanced 𝕜 t
h : s ⊆ t
r : 𝕜
hr : ‖r‖ ≤ 1
y : E
hy : y ∈ s
hx : (fun x => r • x) y ∈ balancedHull 𝕜 s
⊢ (fun x => r • x) y ∈ t

Proof state:
case intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝¹ : SeminormedRing 𝕜
inst✝ : SMul 𝕜 E
s t : Set E
ht : Balanced 𝕜 t
h : s ⊆ t
r : 𝕜
hr : ‖r‖ ≤ 1
y : E
hy : y ∈ s
hx : (fun x => r • x) y ∈ balancedHull 𝕜 s
⊢ (fun x => r • x) y ∈ t

Tactic:
exact ht.smul_mem hr (h hy)

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝¹ : SeminormedRing 𝕜
inst✝ : SMul 𝕜 E
s t : Set E
ht : Balanced 𝕜 t
h : s ⊆ t
⊢ balancedHull 𝕜 s ⊆ t

Tactic:
intros x hx

Result:
𝕜 : Type u_1
E : Type u_2
inst✝¹ : SeminormedRing 𝕜
inst✝ : SMul 𝕜 E
s t : Set E
ht : Balanced 𝕜 t
h : s ⊆ t
x : E
hx : x ∈ balancedHull 𝕜 s
⊢ x ∈ t
-- Mathlib/MeasureTheory/Integral/Lebesgue.lean
theorem lintegral_iSup_ae {f : ℕ → α → ℝ≥0∞} (hf : ∀ n, Measurable (f n))
    (h_mono : ∀ n, ∀ᵐ a ∂μ, f n a ≤ f n.succ a) : ∫⁻ a, ⨆ n, f n a ∂μ = ⨆ n, ∫⁻ a, f n a ∂μ

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), Measurable (f n)
h_mono : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, f n a ≤ f n.succ a
s : Set α
hs : {a | ¬∀ (i : ℕ), f i a ≤ f i.succ a} ⊆ s ∧ MeasurableSet s ∧ μ s = 0
⊢ ∫⁻ (a : α), ⨆ n, f n a ∂μ = ⨆ n, ∫⁻ (a : α), f n a ∂μ

Tactic:
let g n a := if a ∈ s then 0 else f n a

Result:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), Measurable (f n)
h_mono : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, f n a ≤ f n.succ a
s : Set α
hs : {a | ¬∀ (i : ℕ), f i a ≤ f i.succ a} ⊆ s ∧ MeasurableSet s ∧ μ s = 0
g : ℕ → α → ℝ≥0∞ := fun n a => if a ∈ s then 0 else f n a
⊢ ∫⁻ (a : α), ⨆ n, f n a ∂μ = ⨆ n, ∫⁻ (a : α), f n a ∂μ

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), Measurable (f n)
h_mono : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, f n a ≤ f n.succ a
s : Set α
hs : {a | ¬∀ (i : ℕ), f i a ≤ f i.succ a} ⊆ s ∧ MeasurableSet s ∧ μ s = 0
g : ℕ → α → ℝ≥0∞ := fun n a => if a ∈ s then 0 else f n a
g_eq_f : ∀ᵐ (a : α) ∂μ, ∀ (n : ℕ), g n a = f n a
n : ℕ
a : α
⊢ (if a ∈ s then 0 else f n a) ≤ if a ∈ s then 0 else f (n + 1) a

Tactic:
split_ifs with h

Result:
case pos
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), Measurable (f n)
h_mono : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, f n a ≤ f n.succ a
s : Set α
hs : {a | ¬∀ (i : ℕ), f i a ≤ f i.succ a} ⊆ s ∧ MeasurableSet s ∧ μ s = 0
g : ℕ → α → ℝ≥0∞ := fun n a => if a ∈ s then 0 else f n a
g_eq_f : ∀ᵐ (a : α) ∂μ, ∀ (n : ℕ), g n a = f n a
n : ℕ
a : α
h : a ∈ s
⊢ 0 ≤ 0

case neg
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), Measurable (f n)
h_mono : ∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, f n a ≤ f n.succ a
s : Set α
hs : {a | ¬∀ (i : ℕ), f i a ≤ f i.succ a} ⊆ s ∧ MeasurableSet s ∧ μ s = 0
g : ℕ → α → ℝ≥0∞ := fun n a => if a ∈ s then 0 else f n a
g_eq_f : ∀ᵐ (a : α) ∂μ, ∀ (n : ℕ), g n a = f n a
n : ℕ
a : α
h : a ∉ s
⊢ f n a ≤ f (n + 1) a
-- Mathlib/NumberTheory/Pell.lean
theorem prop_x (a : Solution₁ d) : a.x ^ 2 = 1 + d * a.y ^ 2

Proof state:
d : ℤ
a : Solution₁ d
⊢ a.x ^ 2 = a.x ^ 2 - d * a.y ^ 2 + d * a.y ^ 2

Tactic:
ring

Result:
no goals

Proof state:
d : ℤ
a : Solution₁ d
⊢ a.x ^ 2 = 1 + d * a.y ^ 2

Tactic:
rw [← a.prop]

Result:
d : ℤ
a : Solution₁ d
⊢ a.x ^ 2 = a.x ^ 2 - d * a.y ^ 2 + d * a.y ^ 2
-- Mathlib/RingTheory/Spectrum/Prime/Polynomial.lean
lemma isOpen_image_comap_of_monic (f g : R[X]) (hg : g.Monic) :
    IsOpen (comap C '' (zeroLocus {g} \ zeroLocus {f}))

Proof state:
R : Type u_1
inst✝ : CommRing R
f g : R[X]
hg : g.Monic
⊢ IsOpen (⇑(comap C) '' (zeroLocus {g} \ zeroLocus {f}))

Tactic:
obtain ⟨t, ht⟩ := exists_image_comap_of_monic f g hg

Result:
case intro
R : Type u_1
inst✝ : CommRing R
f g : R[X]
hg : g.Monic
t : Finset R
ht : ⇑(comap C) '' (zeroLocus {g} \ zeroLocus {f}) = (zeroLocus ↑t)ᶜ
⊢ IsOpen (⇑(comap C) '' (zeroLocus {g} \ zeroLocus {f}))

Proof state:
case intro
R : Type u_1
inst✝ : CommRing R
f g : R[X]
hg : g.Monic
t : Finset R
ht : ⇑(comap C) '' (zeroLocus {g} \ zeroLocus {f}) = (zeroLocus ↑t)ᶜ
⊢ IsOpen (⇑(comap C) '' (zeroLocus {g} \ zeroLocus {f}))

Tactic:
rw [ht]

Result:
case intro
R : Type u_1
inst✝ : CommRing R
f g : R[X]
hg : g.Monic
t : Finset R
ht : ⇑(comap C) '' (zeroLocus {g} \ zeroLocus {f}) = (zeroLocus ↑t)ᶜ
⊢ IsOpen (zeroLocus ↑t)ᶜ

Proof state:
case intro
R : Type u_1
inst✝ : CommRing R
f g : R[X]
hg : g.Monic
t : Finset R
ht : ⇑(comap C) '' (zeroLocus {g} \ zeroLocus {f}) = (zeroLocus ↑t)ᶜ
⊢ IsOpen (zeroLocus ↑t)ᶜ

Tactic:
exact (isClosed_zeroLocus (R := R) t).isOpen_compl

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/DivisionPolynomial/Degree.lean
lemma natDegree_preΨ_pos {n : ℤ} (hn : 2 < n.natAbs) (h : (n : R) ≠ 0) :
    0 < (W.preΨ n).natDegree

Proof state:
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
ih : ∀ (n : ℕ), 2 < (↑n).natAbs → ↑↑n ≠ 0 → 0 < (W.preΨ ↑n).natDegree
n : ℕ
hn : 2 < (-↑n).natAbs
h : ↑(-↑n) ≠ 0
⊢ 2 < (↑n).natAbs

Tactic:
rwa [← Int.natAbs_neg]

Result:
no goals

Proof state:
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
n : ℤ
hn : 2 < n.natAbs
h : ↑n ≠ 0
⊢ 0 < (W.preΨ n).natDegree

Tactic:
induction n using Int.negInduction with
| nat n => simpa only [preΨ_ofNat] using W.natDegree_preΨ'_pos hn <| by exact_mod_cast h
| neg ih n => simpa only [preΨ_neg, natDegree_neg]
      using ih n (by rwa [← Int.natAbs_neg]) <| neg_ne_zero.mp <| by exact_mod_cast h

Result:
no goals

Proof state:
case neg
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
ih : ∀ (n : ℕ), 2 < (↑n).natAbs → ↑↑n ≠ 0 → 0 < (W.preΨ ↑n).natDegree
n : ℕ
hn : 2 < (-↑n).natAbs
h : ↑(-↑n) ≠ 0
⊢ 0 < (W.preΨ (-↑n)).natDegree

Tactic:
simpa only [preΨ_neg, natDegree_neg]
using ih n (by rwa [← Int.natAbs_neg]) <| neg_ne_zero.mp <| by exact_mod_cast h

Result:
no goals

Proof state:
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
ih : ∀ (n : ℕ), 2 < (↑n).natAbs → ↑↑n ≠ 0 → 0 < (W.preΨ ↑n).natDegree
n : ℕ
hn : 2 < (-↑n).natAbs
h : ↑(-↑n) ≠ 0
⊢ -↑↑n ≠ 0

Tactic:
exact_mod_cast h

Result:
no goals

Proof state:
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
n : ℕ
hn : 2 < (↑n).natAbs
h : ↑↑n ≠ 0
⊢ ↑(↑n).natAbs ≠ 0

Tactic:
exact_mod_cast h

Result:
no goals

Proof state:
case nat
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
n : ℕ
hn : 2 < (↑n).natAbs
h : ↑↑n ≠ 0
⊢ 0 < (W.preΨ ↑n).natDegree

Tactic:
simpa only [preΨ_ofNat] using W.natDegree_preΨ'_pos hn <| by exact_mod_cast h

Result:
no goals