harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Topology/Algebra/Valued/ValuationTopology.lean
theorem loc_const {x : R} (h : (v x : Γ₀) ≠ 0) : { y : R | v y = v x } ∈ 𝓝 x

Proof state:
case h
R : Type u
inst✝¹ : Ring R
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
_i : Valued R Γ₀
x : R
h : v x ≠ 0
y : R
y_in : y ∈ {y | v (y - x) < v x}
⊢ y ∈ {y | v y = v x}

Tactic:
exact Valuation.map_eq_of_sub_lt _ y_in

Result:
no goals

Proof state:
case h
R : Type u
inst✝¹ : Ring R
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
_i : Valued R Γ₀
x : R
h : v x ≠ 0
⊢ {y | v (y - x) < v x} ⊆ {y | v y = v x}

Tactic:
intro y y_in

Result:
case h
R : Type u
inst✝¹ : Ring R
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
_i : Valued R Γ₀
x : R
h : v x ≠ 0
y : R
y_in : y ∈ {y | v (y - x) < v x}
⊢ y ∈ {y | v y = v x}

Proof state:
R : Type u
inst✝¹ : Ring R
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
_i : Valued R Γ₀
x : R
h : v x ≠ 0
⊢ {y | v y = v x} ∈ 𝓝 x

Tactic:
rw [mem_nhds]

Result:
R : Type u
inst✝¹ : Ring R
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
_i : Valued R Γ₀
x : R
h : v x ≠ 0
⊢ ∃ γ, {y | v (y - x) < ↑γ} ⊆ {y | v y = v x}

Proof state:
R : Type u
inst✝¹ : Ring R
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
_i : Valued R Γ₀
x : R
h : v x ≠ 0
⊢ ∃ γ, {y | v (y - x) < ↑γ} ⊆ {y | v y = v x}

Tactic:
use Units.mk0 _ h

Result:
case h
R : Type u
inst✝¹ : Ring R
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
_i : Valued R Γ₀
x : R
h : v x ≠ 0
⊢ {y | v (y - x) < ↑(Units.mk0 (v x) h)} ⊆ {y | v y = v x}

Proof state:
case h
R : Type u
inst✝¹ : Ring R
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
_i : Valued R Γ₀
x : R
h : v x ≠ 0
⊢ {y | v (y - x) < ↑(Units.mk0 (v x) h)} ⊆ {y | v y = v x}

Tactic:
rw [Units.val_mk0]

Result:
case h
R : Type u
inst✝¹ : Ring R
Γ₀ : Type v
inst✝ : LinearOrderedCommGroupWithZero Γ₀
_i : Valued R Γ₀
x : R
h : v x ≠ 0
⊢ {y | v (y - x) < v x} ⊆ {y | v y = v x}
-- Mathlib/Analysis/NormedSpace/FunctionSeries.lean
theorem continuous_tsum [TopologicalSpace β] {f : α → β → F} (hf : ∀ i, Continuous (f i))
    (hu : Summable u) (hfu : ∀ n x, ‖f n x‖ ≤ u n) : Continuous fun x => ∑' n, f n x

Proof state:
α : Type u_1
β : Type u_2
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : CompleteSpace F
u : α → ℝ
inst✝ : TopologicalSpace β
f : α → β → F
hu : Summable u
hfu : ∀ (n : α) (x : β), ‖f n x‖ ≤ u n
hf : ∀ (i : α), ContinuousOn (f i) univ
⊢ ContinuousOn (fun x => ∑' (n : α), f n x) univ

Tactic:
exact continuousOn_tsum hf hu fun n x _ => hfu n x

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : CompleteSpace F
u : α → ℝ
inst✝ : TopologicalSpace β
f : α → β → F
hf : ∀ (i : α), Continuous (f i)
hu : Summable u
hfu : ∀ (n : α) (x : β), ‖f n x‖ ≤ u n
⊢ Continuous fun x => ∑' (n : α), f n x

Tactic:
simp_rw [continuous_iff_continuousOn_univ] at hf ⊢

Result:
α : Type u_1
β : Type u_2
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : CompleteSpace F
u : α → ℝ
inst✝ : TopologicalSpace β
f : α → β → F
hu : Summable u
hfu : ∀ (n : α) (x : β), ‖f n x‖ ≤ u n
hf : ∀ (i : α), ContinuousOn (f i) univ
⊢ ContinuousOn (fun x => ∑' (n : α), f n x) univ
-- Mathlib/CategoryTheory/EssentiallySmall.lean
theorem essentiallySmall_of_small_of_locallySmall [Small.{w} C] [LocallySmall.{w} C] :
    EssentiallySmall.{w} C :=
  (essentiallySmall_iff C).2 ⟨small_of_surjective Quotient.exists_rep, by infer_instance⟩

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Small.{w, u} C
inst✝ : LocallySmall.{w, v, u} C
⊢ LocallySmall.{w, v, u} C

Tactic:
infer_instance

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Count.lean
theorem countP_cons_of_pos (l) (pa : p a) : countP p (a :: l) = countP p l + 1

Proof state:
α : Type u_1
p : α → Bool
a : α
l : List α
pa : p a = true
⊢ countP p (a :: l) = countP p l + 1

Tactic:
have : countP.go p (a :: l) 0 = countP.go p l 1 := show cond .. = _ by rw [pa]; rfl

Result:
α : Type u_1
p : α → Bool
a : α
l : List α
pa : p a = true
this : countP.go p (a :: l) 0 = countP.go p l 1
⊢ countP p (a :: l) = countP p l + 1

Proof state:
α : Type u_1
p : α → Bool
a : α
l : List α
pa : p a = true
⊢ (bif true then countP.go p l (0 + 1) else countP.go p l 0) = countP.go p l 1

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
p : α → Bool
a : α
l : List α
pa : p a = true
this : countP.go p (a :: l) 0 = countP.go p l 1
⊢ countP.go p (a :: l) 0 = countP.go p l 0 + 1

Tactic:
rw [this, Nat.add_comm, List.countP_go_eq_add]

Result:
no goals

Proof state:
α : Type u_1
p : α → Bool
a : α
l : List α
pa : p a = true
this : countP.go p (a :: l) 0 = countP.go p l 1
⊢ countP p (a :: l) = countP p l + 1

Tactic:
unfold countP

Result:
α : Type u_1
p : α → Bool
a : α
l : List α
pa : p a = true
this : countP.go p (a :: l) 0 = countP.go p l 1
⊢ countP.go p (a :: l) 0 = countP.go p l 0 + 1

Proof state:
α : Type u_1
p : α → Bool
a : α
l : List α
pa : p a = true
⊢ (bif p a then countP.go p l (0 + 1) else countP.go p l 0) = countP.go p l 1

Tactic:
rw [pa]

Result:
α : Type u_1
p : α → Bool
a : α
l : List α
pa : p a = true
⊢ (bif true then countP.go p l (0 + 1) else countP.go p l 0) = countP.go p l 1
-- Mathlib/Data/Int/ConditionallyCompleteOrder.lean
theorem csSup_mem {s : Set ℤ} (h1 : s.Nonempty) (h2 : BddAbove s) : sSup s ∈ s

Proof state:
case h.e'_5
s : Set ℤ
h1 : s.Nonempty
h2 : BddAbove s
⊢ sSup s = ↑((Classical.choose h2).greatestOfBdd ⋯ h1)

s : Set ℤ
h1 : s.Nonempty
h2 : BddAbove s
⊢ DecidablePred (Membership.mem s)

Tactic:
exact dif_pos ⟨h1, h2⟩

Result:
no goals

Proof state:
s : Set ℤ
h1 : s.Nonempty
h2 : BddAbove s
⊢ sSup s ∈ s

Tactic:
convert (greatestOfBdd _ (Classical.choose_spec h2) h1).2.1

Result:
case h.e'_5
s : Set ℤ
h1 : s.Nonempty
h2 : BddAbove s
⊢ sSup s = ↑((Classical.choose h2).greatestOfBdd ⋯ h1)

s : Set ℤ
h1 : s.Nonempty
h2 : BddAbove s
⊢ DecidablePred (Membership.mem s)
-- Mathlib/Data/Fin/Tuple/Take.lean
theorem take_eq_self (v : (i : Fin n) → α i) : take n (le_refl n) v = v

Proof state:
n : ℕ
α : Fin n → Sort u_1
v : (i : Fin n) → α i
⊢ take n ⋯ v = v

Tactic:
ext i

Result:
case h
n : ℕ
α : Fin n → Sort u_1
v : (i : Fin n) → α i
i : Fin n
⊢ take n ⋯ v i = v i

Proof state:
case h
n : ℕ
α : Fin n → Sort u_1
v : (i : Fin n) → α i
i : Fin n
⊢ take n ⋯ v i = v i

Tactic:
simp [take]

Result:
no goals
-- Mathlib/Control/LawfulFix.lean
theorem approx_le_fix (i : ℕ) : approx f i ≤ Part.fix f := fun a b hh ↦ by
  rw [mem_iff f]
  exact ⟨_, hh⟩

Proof state:
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
i : ℕ
a : α
b : β a
hh : b ∈ approx (⇑f) i a
⊢ b ∈ Part.fix (⇑f) a

Tactic:
rw [mem_iff f]

Result:
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
i : ℕ
a : α
b : β a
hh : b ∈ approx (⇑f) i a
⊢ ∃ i, b ∈ approx (⇑f) i a

Proof state:
α : Type u_1
β : α → Type u_2
f : ((a : α) → Part (β a)) →o (a : α) → Part (β a)
i : ℕ
a : α
b : β a
hh : b ∈ approx (⇑f) i a
⊢ ∃ i, b ∈ approx (⇑f) i a

Tactic:
exact ⟨_, hh⟩

Result:
no goals
-- Mathlib/Logic/Equiv/PartialEquiv.lean
theorem trans_assoc (e'' : PartialEquiv γ δ) : (e.trans e').trans e'' = e.trans (e'.trans e'') :=
  PartialEquiv.ext (fun _ => rfl) (fun _ => rfl)
    (by simp [trans_source, @preimage_comp α β γ, inter_assoc])

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
e : PartialEquiv α β
e' : PartialEquiv β γ
e'' : PartialEquiv γ δ
⊢ ((e.trans e').trans e'').source = (e.trans (e'.trans e'')).source

Tactic:
simp [trans_source, @preimage_comp α β γ, inter_assoc]

Result:
no goals
-- Mathlib/CategoryTheory/Adjunction/Basic.lean
lemma unit_comp_map_eq_iff {A : C} {B : D} (f : F.obj A ⟶ B) (g : A ⟶ G.obj B) :
    adj.unit.app A ≫ G.map f = g ↔ f = F.map g ≫ adj.counit.app B :=
  ⟨fun h => by simp [← h], fun h => by simp [h]⟩

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
A : C
B : D
f : F.obj A ⟶ B
g : A ⟶ G.obj B
h : adj.unit.app A ≫ G.map f = g
⊢ f = F.map g ≫ adj.counit.app B

Tactic:
simp [← h]

Result:
no goals

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
adj : F ⊣ G
A : C
B : D
f : F.obj A ⟶ B
g : A ⟶ G.obj B
h : f = F.map g ≫ adj.counit.app B
⊢ adj.unit.app A ≫ G.map f = g

Tactic:
simp [h]

Result:
no goals
-- Mathlib/Computability/EpsilonNFA.lean
theorem evalFrom_empty (x : List α) : M.evalFrom ∅ x = ∅

Proof state:
α : Type u
σ : Type v
M : εNFA α σ
x : List α
⊢ M.evalFrom ∅ x = ∅

Tactic:
induction' x using List.reverseRecOn with x a ih

Result:
case nil
α : Type u
σ : Type v
M : εNFA α σ
⊢ M.evalFrom ∅ [] = ∅

case append_singleton
α : Type u
σ : Type v
M : εNFA α σ
x : List α
a : α
ih : M.evalFrom ∅ x = ∅
⊢ M.evalFrom ∅ (x ++ [a]) = ∅

Proof state:
case append_singleton
α : Type u
σ : Type v
M : εNFA α σ
x : List α
a : α
ih : M.evalFrom ∅ x = ∅
⊢ M.evalFrom ∅ (x ++ [a]) = ∅

Tactic:
rw [evalFrom_append_singleton, ih, stepSet_empty]

Result:
no goals

Proof state:
case nil
α : Type u
σ : Type v
M : εNFA α σ
⊢ M.evalFrom ∅ [] = ∅

Tactic:
rw [evalFrom_nil, εClosure_empty]

Result:
no goals
-- Mathlib/Algebra/Homology/DerivedCategory/Ext/ExtClass.lean
@[simp]
lemma extClass_comp : hS.extClass.comp (Ext.mk₀ S.f) (add_zero 1) = 0

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
S : ShortComplex C
hS : S.ShortExact
this : HasDerivedCategory C := HasDerivedCategory.standard C
⊢ hS.extClass.comp (Ext.mk₀ S.f) ⋯ = 0

Tactic:
ext

Result:
case h
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
S : ShortComplex C
hS : S.ShortExact
this : HasDerivedCategory C := HasDerivedCategory.standard C
⊢ (hS.extClass.comp (Ext.mk₀ S.f) ⋯).hom = Ext.hom 0

Proof state:
case h
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
S : ShortComplex C
hS : S.ShortExact
this : HasDerivedCategory C := HasDerivedCategory.standard C
⊢ hS.singleδ ≫ (shiftFunctor (DerivedCategory C) ↑1).map ((singleFunctor C 0).map S.f) = 0

Tactic:
exact comp_distTriang_mor_zero₃₁ _ hS.singleTriangle_distinguished

Result:
no goals

Proof state:
case h
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
S : ShortComplex C
hS : S.ShortExact
this : HasDerivedCategory C := HasDerivedCategory.standard C
⊢ (hS.extClass.comp (Ext.mk₀ S.f) ⋯).hom = Ext.hom 0

Tactic:
simp only [Ext.comp_hom, Ext.mk₀_hom, extClass_hom, Ext.zero_hom,
  ShiftedHom.comp_mk₀]

Result:
case h
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
S : ShortComplex C
hS : S.ShortExact
this : HasDerivedCategory C := HasDerivedCategory.standard C
⊢ hS.singleδ ≫ (shiftFunctor (DerivedCategory C) ↑1).map ((singleFunctor C 0).map S.f) = 0

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
S : ShortComplex C
hS : S.ShortExact
⊢ hS.extClass.comp (Ext.mk₀ S.f) ⋯ = 0

Tactic:
letI := HasDerivedCategory.standard C

Result:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
S : ShortComplex C
hS : S.ShortExact
this : HasDerivedCategory C := HasDerivedCategory.standard C
⊢ hS.extClass.comp (Ext.mk₀ S.f) ⋯ = 0
-- Mathlib/Order/Bounds/Image.lean
theorem BddAbove.bddBelow_image2_of_bddAbove :
    BddAbove s → BddBelow t → BddBelow (Set.image2 f s t)

Proof state:
case intro.intro
α : Type u
β : Type v
γ : Type w
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
f : α → β → γ
s : Set α
t : Set β
h₀ : ∀ (b : β), Antitone (swap f b)
h₁ : ∀ (a : α), Monotone (f a)
a : α
ha : a ∈ upperBounds s
b : β
hb : b ∈ lowerBounds t
⊢ BddBelow (image2 f s t)

Tactic:
exact ⟨f a b, mem_lowerBounds_image2_of_mem_lowerBounds_of_mem_lowerBounds h₀ h₁ ha hb⟩

Result:
no goals

Proof state:
α : Type u
β : Type v
γ : Type w
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
f : α → β → γ
s : Set α
t : Set β
h₀ : ∀ (b : β), Antitone (swap f b)
h₁ : ∀ (a : α), Monotone (f a)
⊢ BddAbove s → BddBelow t → BddBelow (image2 f s t)

Tactic:
rintro ⟨a, ha⟩ ⟨b, hb⟩

Result:
case intro.intro
α : Type u
β : Type v
γ : Type w
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : Preorder γ
f : α → β → γ
s : Set α
t : Set β
h₀ : ∀ (b : β), Antitone (swap f b)
h₁ : ∀ (a : α), Monotone (f a)
a : α
ha : a ∈ upperBounds s
b : β
hb : b ∈ lowerBounds t
⊢ BddBelow (image2 f s t)
-- Mathlib/CategoryTheory/Triangulated/Pretriangulated.lean
lemma isZero₁_iff : IsZero T.obj₁ ↔ (T.mor₁ = 0 ∧ T.mor₃ = 0)

Proof state:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive
hC : Pretriangulated C
T : Triangle C
hT : T ∈ distinguishedTriangles
⊢ T.invRotate.mor₁ = 0 ∧ T.invRotate.mor₂ = 0 ↔ T.mor₁ = 0 ∧ T.mor₃ = 0

Tactic:
dsimp

Result:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive
hC : Pretriangulated C
T : Triangle C
hT : T ∈ distinguishedTriangles
⊢ -(CategoryTheory.shiftFunctor C (-1)).map T.mor₃ ≫ (shiftFunctorCompIsoId C 1 (-1) ⋯).hom.app T.obj₁ = 0 ∧
      T.mor₁ = 0 ↔
    T.mor₁ = 0 ∧ T.mor₃ = 0

Proof state:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive
hC : Pretriangulated C
T : Triangle C
hT : T ∈ distinguishedTriangles
⊢ IsZero T.obj₁ ↔ T.mor₁ = 0 ∧ T.mor₃ = 0

Tactic:
refine (isZero₂_iff _ (inv_rot_of_distTriang _ hT)).trans ?_

Result:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive
hC : Pretriangulated C
T : Triangle C
hT : T ∈ distinguishedTriangles
⊢ T.invRotate.mor₁ = 0 ∧ T.invRotate.mor₂ = 0 ↔ T.mor₁ = 0 ∧ T.mor₃ = 0

Proof state:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive
hC : Pretriangulated C
T : Triangle C
hT : T ∈ distinguishedTriangles
⊢ T.mor₃ = 0 ∧ T.mor₁ = 0 ↔ T.mor₁ = 0 ∧ T.mor₃ = 0

Tactic:
tauto

Result:
no goals

Proof state:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive
hC : Pretriangulated C
T : Triangle C
hT : T ∈ distinguishedTriangles
⊢ -(CategoryTheory.shiftFunctor C (-1)).map T.mor₃ ≫ (shiftFunctorCompIsoId C 1 (-1) ⋯).hom.app T.obj₁ = 0 ∧
      T.mor₁ = 0 ↔
    T.mor₁ = 0 ∧ T.mor₃ = 0

Tactic:
simp only [neg_eq_zero, IsIso.comp_right_eq_zero, Functor.map_eq_zero_iff]

Result:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive
hC : Pretriangulated C
T : Triangle C
hT : T ∈ distinguishedTriangles
⊢ T.mor₃ = 0 ∧ T.mor₁ = 0 ↔ T.mor₁ = 0 ∧ T.mor₃ = 0
-- Mathlib/Topology/Instances/ENNReal/Lemmas.lean
theorem tsum_const_eq_top_of_ne_zero {α : Type*} [Infinite α] {c : ℝ≥0∞} (hc : c ≠ 0) :
    ∑' _ : α, c = ∞

Proof state:
α : Type u_4
inst✝ : Infinite α
c : ℝ≥0∞
hc : c ≠ 0
A : Tendsto (fun n => ↑n * c) atTop (𝓝 (⊤ * c))
⊢ ∑' (x : α), c = ⊤

Tactic:
have B : ∀ n : ℕ, (n : ℝ≥0∞) * c ≤ ∑' _ : α, c := fun n => by
  rcases Infinite.exists_subset_card_eq α n with ⟨s, hs⟩
  simpa [hs] using @ENNReal.sum_le_tsum α (fun _ => c) s

Result:
α : Type u_4
inst✝ : Infinite α
c : ℝ≥0∞
hc : c ≠ 0
A : Tendsto (fun n => ↑n * c) atTop (𝓝 (⊤ * c))
B : ∀ (n : ℕ), ↑n * c ≤ ∑' (x : α), c
⊢ ∑' (x : α), c = ⊤

Proof state:
case intro
α : Type u_4
inst✝ : Infinite α
c : ℝ≥0∞
hc : c ≠ 0
A : Tendsto (fun n => ↑n * c) atTop (𝓝 (⊤ * c))
n : ℕ
s : Finset α
hs : #s = n
⊢ ↑n * c ≤ ∑' (x : α), c

Tactic:
simpa [hs] using @ENNReal.sum_le_tsum α (fun _ => c) s

Result:
no goals

Proof state:
α : Type u_4
inst✝ : Infinite α
c : ℝ≥0∞
hc : c ≠ 0
⊢ Tendsto (fun n => ↑n * c) atTop (𝓝 (⊤ * c))

Tactic:
apply ENNReal.Tendsto.mul_const tendsto_nat_nhds_top

Result:
α : Type u_4
inst✝ : Infinite α
c : ℝ≥0∞
hc : c ≠ 0
⊢ ⊤ ≠ 0 ∨ c ≠ ⊤

Proof state:
α : Type u_4
inst✝ : Infinite α
c : ℝ≥0∞
hc : c ≠ 0
A : Tendsto (fun n => ↑n * c) atTop (𝓝 (⊤ * c))
n : ℕ
⊢ ↑n * c ≤ ∑' (x : α), c

Tactic:
rcases Infinite.exists_subset_card_eq α n with ⟨s, hs⟩

Result:
case intro
α : Type u_4
inst✝ : Infinite α
c : ℝ≥0∞
hc : c ≠ 0
A : Tendsto (fun n => ↑n * c) atTop (𝓝 (⊤ * c))
n : ℕ
s : Finset α
hs : #s = n
⊢ ↑n * c ≤ ∑' (x : α), c

Proof state:
α : Type u_4
inst✝ : Infinite α
c : ℝ≥0∞
hc : c ≠ 0
A : Tendsto (fun n => ↑n * c) atTop (𝓝 (⊤ * c))
B : ∀ (n : ℕ), ↑n * c ≤ ∑' (x : α), c
⊢ ∑' (x : α), c = ⊤

Tactic:
simpa [hc] using le_of_tendsto' A B

Result:
no goals

Proof state:
α : Type u_4
inst✝ : Infinite α
c : ℝ≥0∞
hc : c ≠ 0
⊢ ⊤ ≠ 0 ∨ c ≠ ⊤

Tactic:
simp only [true_or, top_ne_zero, Ne, not_false_iff]

Result:
no goals

Proof state:
α : Type u_4
inst✝ : Infinite α
c : ℝ≥0∞
hc : c ≠ 0
⊢ ∑' (x : α), c = ⊤

Tactic:
have A : Tendsto (fun n : ℕ => (n : ℝ≥0∞) * c) atTop (𝓝 (∞ * c)) := by
  apply ENNReal.Tendsto.mul_const tendsto_nat_nhds_top
  simp only [true_or, top_ne_zero, Ne, not_false_iff]

Result:
α : Type u_4
inst✝ : Infinite α
c : ℝ≥0∞
hc : c ≠ 0
A : Tendsto (fun n => ↑n * c) atTop (𝓝 (⊤ * c))
⊢ ∑' (x : α), c = ⊤
-- Mathlib/Algebra/BigOperators/Group/Finset/Basic.lean
theorem prod_inter_mul_prod_diff [DecidableEq α] (s t : Finset α) (f : α → β) :
    (∏ x ∈ s ∩ t, f x) * ∏ x ∈ s \ t, f x = ∏ x ∈ s, f x

Proof state:
case h.e'_3.a.h.e
α : Type u_3
β : Type u_4
inst✝¹ : CommMonoid β
inst✝ : DecidableEq α
s t : Finset α
f : α → β
x✝ : α
a✝ : x✝ ∈ s
⊢ f = t.piecewise f f

Tactic:
simp (config := { unfoldPartialApp := true }) [Finset.piecewise]

Result:
no goals

Proof state:
α : Type u_3
β : Type u_4
inst✝¹ : CommMonoid β
inst✝ : DecidableEq α
s t : Finset α
f : α → β
⊢ (∏ x ∈ s ∩ t, f x) * ∏ x ∈ s \ t, f x = ∏ x ∈ s, f x

Tactic:
convert (s.prod_piecewise t f f).symm

Result:
case h.e'_3.a.h.e
α : Type u_3
β : Type u_4
inst✝¹ : CommMonoid β
inst✝ : DecidableEq α
s t : Finset α
f : α → β
x✝ : α
a✝ : x✝ ∈ s
⊢ f = t.piecewise f f
-- Mathlib/RingTheory/DedekindDomain/Ideal.lean
theorem primesOver_ncard_ne_zero : (primesOver p B).ncard ≠ 0

Proof state:
case intro.intro
A : Type u_4
inst✝⁵ : CommRing A
p : Ideal A
hpm : p.IsMaximal
B : Type u_5
inst✝⁴ : CommRing B
inst✝³ : IsDedekindDomain B
inst✝² : Algebra A B
inst✝¹ : NoZeroSMulDivisors A B
inst✝ : Algebra.IsIntegral A B
P : Ideal B
hPm : P.IsMaximal
hp : P.LiesOver p
⊢ (p.primesOver B).ncard ≠ 0

Tactic:
exact Set.ncard_ne_zero_of_mem ⟨hPm.isPrime, hp⟩ (primesOver_finite p B)

Result:
no goals

Proof state:
A : Type u_4
inst✝⁵ : CommRing A
p : Ideal A
hpm : p.IsMaximal
B : Type u_5
inst✝⁴ : CommRing B
inst✝³ : IsDedekindDomain B
inst✝² : Algebra A B
inst✝¹ : NoZeroSMulDivisors A B
inst✝ : Algebra.IsIntegral A B
⊢ (p.primesOver B).ncard ≠ 0

Tactic:
rcases exists_ideal_liesOver_maximal_of_isIntegral p B with ⟨P, hPm, hp⟩

Result:
case intro.intro
A : Type u_4
inst✝⁵ : CommRing A
p : Ideal A
hpm : p.IsMaximal
B : Type u_5
inst✝⁴ : CommRing B
inst✝³ : IsDedekindDomain B
inst✝² : Algebra A B
inst✝¹ : NoZeroSMulDivisors A B
inst✝ : Algebra.IsIntegral A B
P : Ideal B
hPm : P.IsMaximal
hp : P.LiesOver p
⊢ (p.primesOver B).ncard ≠ 0
-- Mathlib/Algebra/Polynomial/Eval/Defs.lean
theorem eval_natCast {n : ℕ} : (n : R[X]).eval x = n

Proof state:
R : Type u
inst✝ : Semiring R
x : R
n : ℕ
⊢ eval x ↑n = ↑n

Tactic:
simp only [← C_eq_natCast, eval_C]

Result:
no goals
-- Mathlib/CategoryTheory/Sites/OneHypercover.lean
lemma preOneHypercover_sieve₁ (f₁ f₂ : S.Arrow) {W : C} (p₁ : W ⟶ f₁.Y) (p₂ : W ⟶ f₂.Y)
    (w : p₁ ≫ f₁.f = p₂ ≫ f₂.f) :
    S.preOneHypercover.sieve₁ p₁ p₂ = ⊤

Proof state:
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
X : C
S : J.Cover X
f₁ f₂ : S.Arrow
W : C
p₁ : W ⟶ f₁.Y
p₂ : W ⟶ f₂.Y
w : p₁ ≫ f₁.f = p₂ ≫ f₂.f
⊢ S.preOneHypercover.sieve₁ p₁ p₂ = ⊤

Tactic:
ext Y f

Result:
case h
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
X : C
S : J.Cover X
f₁ f₂ : S.Arrow
W : C
p₁ : W ⟶ f₁.Y
p₂ : W ⟶ f₂.Y
w : p₁ ≫ f₁.f = p₂ ≫ f₂.f
Y : C
f : Y ⟶ W
⊢ (S.preOneHypercover.sieve₁ p₁ p₂).arrows f ↔ ⊤.arrows f

Proof state:
case h
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
X : C
S : J.Cover X
f₁ f₂ : S.Arrow
W : C
p₁ : W ⟶ f₁.Y
p₂ : W ⟶ f₂.Y
w : p₁ ≫ f₁.f = p₂ ≫ f₂.f
Y : C
f : Y ⟶ W
⊢ (S.preOneHypercover.sieve₁ p₁ p₂).arrows f ↔ ⊤.arrows f

Tactic:
simp only [Sieve.top_apply, iff_true]

Result:
case h
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
X : C
S : J.Cover X
f₁ f₂ : S.Arrow
W : C
p₁ : W ⟶ f₁.Y
p₂ : W ⟶ f₂.Y
w : p₁ ≫ f₁.f = p₂ ≫ f₂.f
Y : C
f : Y ⟶ W
⊢ (S.preOneHypercover.sieve₁ p₁ p₂).arrows f

Proof state:
case h
C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
X : C
S : J.Cover X
f₁ f₂ : S.Arrow
W : C
p₁ : W ⟶ f₁.Y
p₂ : W ⟶ f₂.Y
w : p₁ ≫ f₁.f = p₂ ≫ f₂.f
Y : C
f : Y ⟶ W
⊢ (S.preOneHypercover.sieve₁ p₁ p₂).arrows f

Tactic:
exact ⟨{ w := w}, f, rfl, rfl⟩

Result:
no goals
-- Mathlib/LinearAlgebra/SymplecticGroup.lean
theorem coe_inv' (A : symplecticGroup l R) : (↑A⁻¹ : Matrix (l ⊕ l) (l ⊕ l) R) = (↑A)⁻¹

Proof state:
l : Type u_1
R : Type u_2
inst✝² : DecidableEq l
inst✝¹ : Fintype l
inst✝ : CommRing R
A : ↥(symplecticGroup l R)
⊢ ↑A⁻¹ = (↑A)⁻¹

Tactic:
refine (coe_inv A).trans (inv_eq_left_inv ?_).symm

Result:
l : Type u_1
R : Type u_2
inst✝² : DecidableEq l
inst✝¹ : Fintype l
inst✝ : CommRing R
A : ↥(symplecticGroup l R)
⊢ -J l R * (↑A)ᵀ * J l R * ↑A = 1

Proof state:
l : Type u_1
R : Type u_2
inst✝² : DecidableEq l
inst✝¹ : Fintype l
inst✝ : CommRing R
A : ↥(symplecticGroup l R)
⊢ -J l R * (↑A)ᵀ * J l R * ↑A = 1

Tactic:
simp [inv_left_mul_aux, coe_inv]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/LapMatrix.lean
theorem lapMatrix_mulVec_const_eq_zero [Ring R] : mulVec (G.lapMatrix R) (fun _ ↦ 1) = 0

Proof state:
case h
V : Type u_1
R : Type u_2
inst✝³ : Fintype V
G : SimpleGraph V
inst✝² : DecidableRel G.Adj
inst✝¹ : DecidableEq V
inst✝ : Ring R
i : V
⊢ ↑(G.degree i) * 1 - ∑ u ∈ G.neighborFinset i, 1 = 0 i

Tactic:
simp

Result:
no goals

Proof state:
case h
V : Type u_1
R : Type u_2
inst✝³ : Fintype V
G : SimpleGraph V
inst✝² : DecidableRel G.Adj
inst✝¹ : DecidableEq V
inst✝ : Ring R
i : V
⊢ (lapMatrix R G *ᵥ fun x => 1) i = 0 i

Tactic:
rw [lapMatrix_mulVec_apply]

Result:
case h
V : Type u_1
R : Type u_2
inst✝³ : Fintype V
G : SimpleGraph V
inst✝² : DecidableRel G.Adj
inst✝¹ : DecidableEq V
inst✝ : Ring R
i : V
⊢ ↑(G.degree i) * 1 - ∑ u ∈ G.neighborFinset i, 1 = 0 i

Proof state:
V : Type u_1
R : Type u_2
inst✝³ : Fintype V
G : SimpleGraph V
inst✝² : DecidableRel G.Adj
inst✝¹ : DecidableEq V
inst✝ : Ring R
⊢ (lapMatrix R G *ᵥ fun x => 1) = 0

Tactic:
ext1 i

Result:
case h
V : Type u_1
R : Type u_2
inst✝³ : Fintype V
G : SimpleGraph V
inst✝² : DecidableRel G.Adj
inst✝¹ : DecidableEq V
inst✝ : Ring R
i : V
⊢ (lapMatrix R G *ᵥ fun x => 1) i = 0 i
-- Mathlib/Combinatorics/Quiver/Path.lean
theorem eq_nil_of_length_zero (p : Path a a) (hzero : p.length = 0) : p = nil

Proof state:
case nil
V : Type u
inst✝ : Quiver V
a : V
hzero : nil.length = 0
⊢ nil = nil

Tactic:
rfl

Result:
no goals

Proof state:
V : Type u
inst✝ : Quiver V
a : V
p : Path a a
hzero : p.length = 0
⊢ p = nil

Tactic:
cases p

Result:
case nil
V : Type u
inst✝ : Quiver V
a : V
hzero : nil.length = 0
⊢ nil = nil

case cons
V : Type u
inst✝ : Quiver V
a b✝ : V
a✝¹ : Path a b✝
a✝ : b✝ ⟶ a
hzero : (a✝¹.cons a✝).length = 0
⊢ a✝¹.cons a✝ = nil

Proof state:
case cons
V : Type u
inst✝ : Quiver V
a b✝ : V
a✝¹ : Path a b✝
a✝ : b✝ ⟶ a
hzero : (a✝¹.cons a✝).length = 0
⊢ a✝¹.cons a✝ = nil

Tactic:
simp at hzero

Result:
no goals