harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/RingTheory/Filtration.lean
theorem Stable.exists_pow_smul_eq_of_ge (h : F.Stable) :
    ∃ n₀, ∀ n ≥ n₀, F.N n = I ^ (n - n₀) • F.N n₀

Proof state:
case h.e'_2.h.e'_8
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F : I.Filtration M
h : F.Stable
n₀ : ℕ
hn₀ : ∀ (k : ℕ), F.N (n₀ + k) = I ^ k • F.N n₀
n : ℕ
hn : n ≥ n₀
⊢ n = n₀ + (n - n₀)

Tactic:
rw [add_comm, tsub_add_cancel_of_le hn]

Result:
no goals

Proof state:
case intro
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F : I.Filtration M
h : F.Stable
n₀ : ℕ
hn₀ : ∀ (k : ℕ), F.N (n₀ + k) = I ^ k • F.N n₀
⊢ ∃ n₀, ∀ n ≥ n₀, F.N n = I ^ (n - n₀) • F.N n₀

Tactic:
use n₀

Result:
case h
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F : I.Filtration M
h : F.Stable
n₀ : ℕ
hn₀ : ∀ (k : ℕ), F.N (n₀ + k) = I ^ k • F.N n₀
⊢ ∀ n ≥ n₀, F.N n = I ^ (n - n₀) • F.N n₀

Proof state:
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F : I.Filtration M
h : F.Stable
⊢ ∃ n₀, ∀ n ≥ n₀, F.N n = I ^ (n - n₀) • F.N n₀

Tactic:
obtain ⟨n₀, hn₀⟩ := h.exists_pow_smul_eq

Result:
case intro
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F : I.Filtration M
h : F.Stable
n₀ : ℕ
hn₀ : ∀ (k : ℕ), F.N (n₀ + k) = I ^ k • F.N n₀
⊢ ∃ n₀, ∀ n ≥ n₀, F.N n = I ^ (n - n₀) • F.N n₀

Proof state:
case h
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F : I.Filtration M
h : F.Stable
n₀ : ℕ
hn₀ : ∀ (k : ℕ), F.N (n₀ + k) = I ^ k • F.N n₀
n : ℕ
hn : n ≥ n₀
⊢ F.N n = I ^ (n - n₀) • F.N n₀

Tactic:
convert hn₀ (n - n₀)

Result:
case h.e'_2.h.e'_8
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F : I.Filtration M
h : F.Stable
n₀ : ℕ
hn₀ : ∀ (k : ℕ), F.N (n₀ + k) = I ^ k • F.N n₀
n : ℕ
hn : n ≥ n₀
⊢ n = n₀ + (n - n₀)

Proof state:
case h
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F : I.Filtration M
h : F.Stable
n₀ : ℕ
hn₀ : ∀ (k : ℕ), F.N (n₀ + k) = I ^ k • F.N n₀
⊢ ∀ n ≥ n₀, F.N n = I ^ (n - n₀) • F.N n₀

Tactic:
intro n hn

Result:
case h
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
F : I.Filtration M
h : F.Stable
n₀ : ℕ
hn₀ : ∀ (k : ℕ), F.N (n₀ + k) = I ^ k • F.N n₀
n : ℕ
hn : n ≥ n₀
⊢ F.N n = I ^ (n - n₀) • F.N n₀
-- Mathlib/SetTheory/Cardinal/Finsupp.lean
theorem mk_finsupp_lift_of_infinite (α : Type u) (β : Type v) [Infinite α] [Zero β] [Nontrivial β] :
    #(α →₀ β) = max (lift.{v} #α) (lift.{u} #β)

Proof state:
case a.h₁
α : Type u
β : Type v
inst✝² : Infinite α
inst✝¹ : Zero β
inst✝ : Nontrivial β
⊢ lift.{max u v, u} #α ≤ lift.{max v u, max v u} #(α →₀ β)

Tactic:
obtain ⟨b, hb⟩ := exists_ne (0 : β)

Result:
case a.h₁.intro
α : Type u
β : Type v
inst✝² : Infinite α
inst✝¹ : Zero β
inst✝ : Nontrivial β
b : β
hb : b ≠ 0
⊢ lift.{max u v, u} #α ≤ lift.{max v u, max v u} #(α →₀ β)

Proof state:
α : Type u
β : Type v
inst✝² : Infinite α
inst✝¹ : Zero β
inst✝ : Nontrivial β
⊢ #(α →₀ β) = lift.{v, u} #α ⊔ lift.{u, v} #β

Tactic:
apply le_antisymm

Result:
case a
α : Type u
β : Type v
inst✝² : Infinite α
inst✝¹ : Zero β
inst✝ : Nontrivial β
⊢ #(α →₀ β) ≤ lift.{v, u} #α ⊔ lift.{u, v} #β

case a
α : Type u
β : Type v
inst✝² : Infinite α
inst✝¹ : Zero β
inst✝ : Nontrivial β
⊢ lift.{v, u} #α ⊔ lift.{u, v} #β ≤ #(α →₀ β)

Proof state:
case a.h₁.intro
α : Type u
β : Type v
inst✝² : Infinite α
inst✝¹ : Zero β
inst✝ : Nontrivial β
b : β
hb : b ≠ 0
⊢ lift.{max u v, u} #α ≤ lift.{max v u, max v u} #(α →₀ β)

Tactic:
exact lift_mk_le.{v}.2 ⟨⟨_, Finsupp.single_left_injective hb⟩⟩

Result:
no goals

Proof state:
α : Type u
β : Type v
inst✝² : Infinite α
inst✝¹ : Zero β
inst✝ : Nontrivial β
⊢ #(α × β) = lift.{v, u} #α ⊔ lift.{u, v} #β

Tactic:
rw [mk_prod, mul_eq_max_of_aleph0_le_left] <;> simp

Result:
no goals

Proof state:
case a
α : Type u
β : Type v
inst✝² : Infinite α
inst✝¹ : Zero β
inst✝ : Nontrivial β
⊢ lift.{v, u} #α ⊔ lift.{u, v} #β ≤ #(α →₀ β)

Tactic:
apply max_le <;> rw [← lift_id #(α →₀ β), ← lift_umax]

Result:
case a.h₁
α : Type u
β : Type v
inst✝² : Infinite α
inst✝¹ : Zero β
inst✝ : Nontrivial β
⊢ lift.{max u v, u} #α ≤ lift.{max v u, max v u} #(α →₀ β)

case a.h₂
α : Type u
β : Type v
inst✝² : Infinite α
inst✝¹ : Zero β
inst✝ : Nontrivial β
⊢ lift.{max v u, v} #β ≤ lift.{max v u, max v u} #(α →₀ β)

Proof state:
case a
α : Type u
β : Type v
inst✝² : Infinite α
inst✝¹ : Zero β
inst✝ : Nontrivial β
⊢ #(α →₀ β) ≤ lift.{v, u} #α ⊔ lift.{u, v} #β

Tactic:
calc
  #(α →₀ β) ≤ #(Finset (α × β)) := mk_le_of_injective (Finsupp.graph_injective α β)
  _ = #(α × β) := mk_finset_of_infinite _
  _ = max (lift.{v} #α) (lift.{u} #β) := by
    rw [mk_prod, mul_eq_max_of_aleph0_le_left] <;> simp

Result:
no goals

Proof state:
case a.h₂
α : Type u
β : Type v
inst✝² : Infinite α
inst✝¹ : Zero β
inst✝ : Nontrivial β
⊢ lift.{max v u, v} #β ≤ lift.{max v u, max v u} #(α →₀ β)

Tactic:
inhabit α

Result:
case a.h₂
α : Type u
β : Type v
inst✝² : Infinite α
inst✝¹ : Zero β
inst✝ : Nontrivial β
inhabited_h : Inhabited α
⊢ lift.{max v u, v} #β ≤ lift.{max v u, max v u} #(α →₀ β)

Proof state:
case a.h₂
α : Type u
β : Type v
inst✝² : Infinite α
inst✝¹ : Zero β
inst✝ : Nontrivial β
inhabited_h : Inhabited α
⊢ lift.{max v u, v} #β ≤ lift.{max v u, max v u} #(α →₀ β)

Tactic:
exact lift_mk_le.{u}.2 ⟨⟨_, Finsupp.single_injective default⟩⟩

Result:
no goals
-- Mathlib/Analysis/Analytic/OfScalars.lean
theorem ofScalarsSum_op [T2Space E] (x : E) :
    ofScalarsSum c (MulOpposite.op x) = MulOpposite.op (ofScalarsSum c x)

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝⁵ : Field 𝕜
inst✝⁴ : Ring E
inst✝³ : Algebra 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : IsTopologicalRing E
c : ℕ → 𝕜
inst✝ : T2Space E
x : E
⊢ ofScalarsSum c (MulOpposite.op x) = MulOpposite.op (ofScalarsSum c x)

Tactic:
simp [ofScalars, ofScalars_sum_eq, ← MulOpposite.op_pow, ← MulOpposite.op_smul, tsum_op]

Result:
no goals
-- Mathlib/Analysis/LocallyConvex/Polar.lean
theorem polar_weak_closed (s : Set E) : IsClosed[WeakBilin.instTopologicalSpace B.flip]
    (B.polar s)

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NormedCommRing 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
s : Set E
⊢ IsClosed (B.polar s)

Tactic:
rw [polar_eq_iInter]

Result:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NormedCommRing 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
s : Set E
⊢ IsClosed (⋂ x ∈ s, {y | ‖(B x) y‖ ≤ 1})

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NormedCommRing 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
s : Set E
⊢ IsClosed (⋂ x ∈ s, {y | ‖(B x) y‖ ≤ 1})

Tactic:
refine isClosed_iInter fun x => isClosed_iInter fun _ => ?_

Result:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NormedCommRing 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
s : Set E
x : E
x✝ : x ∈ s
⊢ IsClosed {y | ‖(B x) y‖ ≤ 1}

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NormedCommRing 𝕜
inst✝³ : AddCommMonoid E
inst✝² : AddCommMonoid F
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 F
B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜
s : Set E
x : E
x✝ : x ∈ s
⊢ IsClosed {y | ‖(B x) y‖ ≤ 1}

Tactic:
exact isClosed_le (WeakBilin.eval_continuous B.flip x).norm continuous_const

Result:
no goals
-- Mathlib/AlgebraicTopology/SimplexCategory/GeneratorsRelations/EpiMono.lean
/-- All `P_δ` are split monos as composition of such. -/
lemma isSplitMono_P_δ {x y : SimplexCategoryGenRel} {m : x ⟶ y} (hm : P_δ m) :
    IsSplitMono m

Proof state:
case comp_of
x y : SimplexCategoryGenRel
m : x ⟶ y
x✝ y✝ z✝ : SimplexCategoryGenRel
f✝ : x✝ ⟶ y✝
g✝ : y✝ ⟶ z✝
hf✝ : faces.multiplicativeClosure f✝
h : faces g✝
hf_ih✝ : IsSplitMono f✝
⊢ IsSplitMono (f✝ ≫ g✝)

Tactic:
cases h

Result:
case comp_of.δ
x y : SimplexCategoryGenRel
m : x ⟶ y
x✝ : SimplexCategoryGenRel
n✝ : ℕ
i✝ : Fin (n✝ + 2)
f✝ : x✝ ⟶ mk n✝
hf✝ : faces.multiplicativeClosure f✝
hf_ih✝ : IsSplitMono f✝
⊢ IsSplitMono (f✝ ≫ δ i✝)

Proof state:
case id
x y : SimplexCategoryGenRel
m : x ⟶ y
x✝ : SimplexCategoryGenRel
⊢ IsSplitMono (𝟙 x✝)

Tactic:
infer_instance

Result:
no goals

Proof state:
x y : SimplexCategoryGenRel
m : x ⟶ y
hm : P_δ m
⊢ IsSplitMono m

Tactic:
induction hm with
| of x hx => cases hx; infer_instance
| id => infer_instance
| comp_of _ _ _ h => cases h; infer_instance

Result:
no goals

Proof state:
case of
x✝¹ y : SimplexCategoryGenRel
m : x✝¹ ⟶ y
x✝ y✝ : SimplexCategoryGenRel
x : x✝ ⟶ y✝
hx : faces x
⊢ IsSplitMono x

Tactic:
cases hx

Result:
case of.δ
x y : SimplexCategoryGenRel
m : x ⟶ y
n✝ : ℕ
i✝ : Fin (n✝ + 2)
⊢ IsSplitMono (δ i✝)

Proof state:
case comp_of.δ
x y : SimplexCategoryGenRel
m : x ⟶ y
x✝ : SimplexCategoryGenRel
n✝ : ℕ
i✝ : Fin (n✝ + 2)
f✝ : x✝ ⟶ mk n✝
hf✝ : faces.multiplicativeClosure f✝
hf_ih✝ : IsSplitMono f✝
⊢ IsSplitMono (f✝ ≫ δ i✝)

Tactic:
infer_instance

Result:
no goals

Proof state:
case of.δ
x y : SimplexCategoryGenRel
m : x ⟶ y
n✝ : ℕ
i✝ : Fin (n✝ + 2)
⊢ IsSplitMono (δ i✝)

Tactic:
infer_instance

Result:
no goals
-- Mathlib/Topology/Baire/BaireMeasurable.lean
theorem Homeomorph.residual_map_eq (h : α ≃ₜ β) : (residual α).map h = residual β

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
h : α ≃ₜ β
⊢ ∀ s ∈ residual α, ⇑h.symm ⁻¹' s ∈ residual β

Tactic:
exact tendsto_residual_of_isOpenMap h.symm.continuous h.symm.isOpenMap

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
h : α ≃ₜ β
⊢ map (⇑h) (residual α) = residual β

Tactic:
refine le_antisymm (tendsto_residual_of_isOpenMap h.continuous h.isOpenMap) (le_map ?_)

Result:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
h : α ≃ₜ β
⊢ ∀ s ∈ residual α, ⇑h '' s ∈ residual β

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
h : α ≃ₜ β
⊢ ∀ s ∈ residual α, ⇑h '' s ∈ residual β

Tactic:
simp_rw [← preimage_symm]

Result:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
h : α ≃ₜ β
⊢ ∀ s ∈ residual α, ⇑h.symm ⁻¹' s ∈ residual β
-- Mathlib/Data/Matrix/Notation.lean
theorem cons_mul [Fintype n'] (v : n' → α) (A : Fin m → n' → α) (B : Matrix n' o' α) :
    of (vecCons v A) * B = of (vecCons (v ᵥ* B) (of.symm (of A * B)))

Proof state:
case a
α : Type u
m : ℕ
n' : Type uₙ
o' : Type uₒ
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : Fintype n'
v : n' → α
A : Fin m → n' → α
B : Matrix n' o' α
i : Fin m.succ
j : o'
⊢ (of (vecCons v A) * B) i j = of (vecCons (v ᵥ* B) (of.symm (of A * B))) i j

Tactic:
refine Fin.cases ?_ ?_ i

Result:
case a.refine_1
α : Type u
m : ℕ
n' : Type uₙ
o' : Type uₒ
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : Fintype n'
v : n' → α
A : Fin m → n' → α
B : Matrix n' o' α
i : Fin m.succ
j : o'
⊢ (of (vecCons v A) * B) 0 j = of (vecCons (v ᵥ* B) (of.symm (of A * B))) 0 j

case a.refine_2
α : Type u
m : ℕ
n' : Type uₙ
o' : Type uₒ
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : Fintype n'
v : n' → α
A : Fin m → n' → α
B : Matrix n' o' α
i : Fin m.succ
j : o'
⊢ ∀ (i : Fin m), (of (vecCons v A) * B) i.succ j = of (vecCons (v ᵥ* B) (of.symm (of A * B))) i.succ j

Proof state:
case a.refine_2
α : Type u
m : ℕ
n' : Type uₙ
o' : Type uₒ
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : Fintype n'
v : n' → α
A : Fin m → n' → α
B : Matrix n' o' α
i : Fin m.succ
j : o'
⊢ ∀ (i : Fin m), (of (vecCons v A) * B) i.succ j = of (vecCons (v ᵥ* B) (of.symm (of A * B))) i.succ j

Tactic:
simp [mul_val_succ]

Result:
no goals

Proof state:
α : Type u
m : ℕ
n' : Type uₙ
o' : Type uₒ
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : Fintype n'
v : n' → α
A : Fin m → n' → α
B : Matrix n' o' α
⊢ of (vecCons v A) * B = of (vecCons (v ᵥ* B) (of.symm (of A * B)))

Tactic:
ext i j

Result:
case a
α : Type u
m : ℕ
n' : Type uₙ
o' : Type uₒ
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : Fintype n'
v : n' → α
A : Fin m → n' → α
B : Matrix n' o' α
i : Fin m.succ
j : o'
⊢ (of (vecCons v A) * B) i j = of (vecCons (v ᵥ* B) (of.symm (of A * B))) i j

Proof state:
case a.refine_1
α : Type u
m : ℕ
n' : Type uₙ
o' : Type uₒ
inst✝¹ : NonUnitalNonAssocSemiring α
inst✝ : Fintype n'
v : n' → α
A : Fin m → n' → α
B : Matrix n' o' α
i : Fin m.succ
j : o'
⊢ (of (vecCons v A) * B) 0 j = of (vecCons (v ᵥ* B) (of.symm (of A * B))) 0 j

Tactic:
rfl

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem not_mem_of_not_mem_push {a b : α} {l : Vector α n} (h : a ∉ l.push b) : a ∉ l

Proof state:
α : Type u_1
n : Nat
a b : α
l : Vector α n
h : ¬a ∈ l.push b
⊢ ¬a ∈ l

Tactic:
simp only [mem_push, not_or] at h

Result:
α : Type u_1
n : Nat
a b : α
l : Vector α n
h : ¬a ∈ l ∧ ¬a = b
⊢ ¬a ∈ l

Proof state:
α : Type u_1
n : Nat
a b : α
l : Vector α n
h : ¬a ∈ l ∧ ¬a = b
⊢ ¬a ∈ l

Tactic:
exact h.1

Result:
no goals
-- Mathlib/Topology/ShrinkingLemma.lean
theorem exists_gt_t2space (v : PartialRefinement u s (fun w => IsCompact (closure w)))
    (hs : IsCompact s) (i : ι) (hi : i ∉ v.carrier) :
    ∃ v' : PartialRefinement u s (fun w => IsCompact (closure w)),
      v < v' ∧ IsCompact (closure (v' i))

Proof state:
case h.a
ι : Type u_1
X : Type u_2
inst✝² : TopologicalSpace X
u : ι → Set X
s : Set X
inst✝¹ : T2Space X
inst✝ : LocallyCompactSpace X
v : PartialRefinement u s fun w => IsCompact (closure w)
hs : IsCompact s
i : ι
hi : i ∉ v.carrier
si : Set X := s ∩ (⋃ j, ⋃ (_ : j ≠ i), v.toFun j)ᶜ
hsi : si = s ∩ ⋂ i_1, ⋂ (_ : ¬i_1 = i), (v.toFun i_1)ᶜ
hsic : IsCompact si
this : si ⊆ v.toFun i
vi : Set X
hvi : IsOpen vi ∧ si ⊆ vi ∧ closure vi ⊆ v.toFun i ∧ IsCompact (closure vi)
x : X
hx : x ∈ s
h : ∀ (j : ι), j ≠ i → x ∉ v.toFun j
⊢ x ∈ s ∩ ⋂ i_1, ⋂ (_ : ¬i_1 = i), (v.toFun i_1)ᶜ

Tactic:
exact ⟨hx, mem_iInter₂_of_mem h⟩

Result:
no goals

Proof state:
case pos
ι : Type u_1
X : Type u_2
inst✝² : TopologicalSpace X
u : ι → Set X
s : Set X
inst✝¹ : T2Space X
inst✝ : LocallyCompactSpace X
v : PartialRefinement u s fun w => IsCompact (closure w)
hs : IsCompact s
i : ι
hi : i ∉ v.carrier
si : Set X := s ∩ (⋃ j, ⋃ (_ : j ≠ i), v.toFun j)ᶜ
hsi : si = s ∩ ⋂ i_1, ⋂ (_ : ¬i_1 = i), (v.toFun i_1)ᶜ
hsic : IsCompact si
this : si ⊆ v.toFun i
vi : Set X
hvi : IsOpen vi ∧ si ⊆ vi ∧ closure vi ⊆ v.toFun i ∧ IsCompact (closure vi)
j : ι
hj : j = i ∨ j ∈ v.carrier
h : j = i
⊢ IsCompact (closure (update v.toFun j vi j))

Tactic:
simp only [update_self]

Result:
case pos
ι : Type u_1
X : Type u_2
inst✝² : TopologicalSpace X
u : ι → Set X
s : Set X
inst✝¹ : T2Space X
inst✝ : LocallyCompactSpace X
v : PartialRefinement u s fun w => IsCompact (closure w)
hs : IsCompact s
i : ι
hi : i ∉ v.carrier
si : Set X := s ∩ (⋃ j, ⋃ (_ : j ≠ i), v.toFun j)ᶜ
hsi : si = s ∩ ⋂ i_1, ⋂ (_ : ¬i_1 = i), (v.toFun i_1)ᶜ
hsic : IsCompact si
this : si ⊆ v.toFun i
vi : Set X
hvi : IsOpen vi ∧ si ⊆ vi ∧ closure vi ⊆ v.toFun i ∧ IsCompact (closure vi)
j : ι
hj : j = i ∨ j ∈ v.carrier
h : j = i
⊢ IsCompact (closure vi)

Proof state:
case h
ι : Type u_1
X : Type u_2
inst✝² : TopologicalSpace X
u : ι → Set X
s : Set X
inst✝¹ : T2Space X
inst✝ : LocallyCompactSpace X
v : PartialRefinement u s fun w => IsCompact (closure w)
hs : IsCompact s
i : ι
hi : i ∉ v.carrier
si : Set X := s ∩ (⋃ j, ⋃ (_ : j ≠ i), v.toFun j)ᶜ
hsi : si = s ∩ ⋂ i_1, ⋂ (_ : ¬i_1 = i), (v.toFun i_1)ᶜ
hsic : IsCompact si
x : X
hx : x ∈ s ∩ ⋂ i_1, ⋂ (_ : ¬i_1 = i), (v.toFun i_1)ᶜ
j : ι
hj : ¬j = i
hsi' : ∀ (i_1 : ι), ¬i_1 = i → x ∈ (v.toFun i_1)ᶜ
⊢ x ∈ (v.toFun j)ᶜ

Tactic:
exact hsi' j hj

Result:
no goals

Proof state:
case h
ι : Type u_1
X : Type u_2
inst✝² : TopologicalSpace X
u : ι → Set X
s : Set X
inst✝¹ : T2Space X
inst✝ : LocallyCompactSpace X
v : PartialRefinement u s fun w => IsCompact (closure w)
hs : IsCompact s
i : ι
hi : i ∉ v.carrier
si : Set X := s ∩ (⋃ j, ⋃ (_ : j ≠ i), v.toFun j)ᶜ
hsi : si = s ∩ ⋂ i_1, ⋂ (_ : ¬i_1 = i), (v.toFun i_1)ᶜ
j : ι
a✝ : j ∈ fun i_1 => i_1 = i → False
⊢ IsOpen (v.toFun j)

Tactic:
exact v.isOpen j

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Impl.lean
theorem intercalate_eq_intercalateTR : @intercalate = @intercalateTR

Proof state:
α : Type u_1
sep : List α
l : List (List α)
x✝ y : List α
xs : List (List α)
acc : Array α
x : List α
⊢ intercalateTR.go sep.toArray x [] acc = acc.toList ++ (intersperse sep [x]).flatten

Tactic:
simp [intercalateTR.go]

Result:
no goals

Proof state:
case h.h.h
α : Type u_1
sep : List α
l : List (List α)
⊢ (intersperse sep l).flatten =
    match l with
    | [] => []
    | [x] => x
    | x :: xs => intercalateTR.go sep.toArray x xs #[]

Tactic:
match l with
| [] => rfl
| [_] => simp
| x::y::xs =>
  let rec go {acc x} : ∀ xs,
    intercalateTR.go sep.toArray x xs acc = acc.toList ++ flatten (intersperse sep (x::xs))
  | [] => by simp [intercalateTR.go]
  | _::_ => by simp [intercalateTR.go, go]
  simp [intersperse, go]

Result:
no goals

Proof state:
α : Type u_1
sep : List α
l : List (List α)
x y : List α
xs : List (List α)
⊢ (intersperse sep (x :: y :: xs)).flatten =
    match x :: y :: xs with
    | [] => []
    | [x] => x
    | x :: xs => intercalateTR.go sep.toArray x xs #[]

Tactic:
simp [intersperse, go]

Result:
no goals

Proof state:
α : Type u_1
sep : List α
l : List (List α)
x✝ y : List α
xs : List (List α)
acc : Array α
x head✝ : List α
tail✝ : List (List α)
⊢ intercalateTR.go sep.toArray x (head✝ :: tail✝) acc = acc.toList ++ (intersperse sep (x :: head✝ :: tail✝)).flatten

Tactic:
simp [intercalateTR.go, go]

Result:
no goals

Proof state:
α : Type u_1
sep : List α
l : List (List α)
⊢ (intersperse sep []).flatten =
    match [] with
    | [] => []
    | [x] => x
    | x :: xs => intercalateTR.go sep.toArray x xs #[]

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
sep : List α
l : List (List α)
head✝ : List α
⊢ (intersperse sep [head✝]).flatten =
    match [head✝] with
    | [] => []
    | [x] => x
    | x :: xs => intercalateTR.go sep.toArray x xs #[]

Tactic:
simp

Result:
no goals

Proof state:
case h.h.h
α : Type u_1
sep : List α
l : List (List α)
⊢ sep.intercalate l = sep.intercalateTR l

Tactic:
simp [intercalate, intercalateTR]

Result:
case h.h.h
α : Type u_1
sep : List α
l : List (List α)
⊢ (intersperse sep l).flatten =
    match l with
    | [] => []
    | [x] => x
    | x :: xs => intercalateTR.go sep.toArray x xs #[]

Proof state:
⊢ @intercalate = @intercalateTR

Tactic:
funext α sep l

Result:
case h.h.h
α : Type u_1
sep : List α
l : List (List α)
⊢ sep.intercalate l = sep.intercalateTR l
-- Mathlib/Order/Filter/Map.lean
theorem map_neBot_iff (f : α → β) {F : Filter α} : NeBot (map f F) ↔ NeBot F

Proof state:
α : Type u_1
β : Type u_2
f : α → β
F : Filter α
⊢ (map f F).NeBot ↔ F.NeBot

Tactic:
simp only [neBot_iff, Ne, map_eq_bot_iff]

Result:
no goals
-- Mathlib/Algebra/Order/Ring/Idempotent.lean
lemma mul_eq_zero_add_eq_one_ext_right (eq : a.1.2 = b.1.2) : a = b

Proof state:
α : Type u_1
inst✝ : CommSemiring α
a b : { a // a.1 * a.2 = 0 ∧ a.1 + a.2 = 1 }
eq : (↑a).2 = (↑b).2
⊢ a = b

Tactic:
refine Subtype.ext <| Prod.ext_iff.mpr ⟨eq_of_mul_eq_add_eq_one a.1.2 ?_ ?_ ?_, eq⟩

Result:
case refine_1
α : Type u_1
inst✝ : CommSemiring α
a b : { a // a.1 * a.2 = 0 ∧ a.1 + a.2 = 1 }
eq : (↑a).2 = (↑b).2
⊢ (↑a).2 * (↑a).1 = (↑b).1 * (↑a).2

case refine_2
α : Type u_1
inst✝ : CommSemiring α
a b : { a // a.1 * a.2 = 0 ∧ a.1 + a.2 = 1 }
eq : (↑a).2 = (↑b).2
⊢ (↑a).2 + (↑a).1 = 1

case refine_3
α : Type u_1
inst✝ : CommSemiring α
a b : { a // a.1 * a.2 = 0 ∧ a.1 + a.2 = 1 }
eq : (↑a).2 = (↑b).2
⊢ (↑a).2 + (↑b).1 = 1

Proof state:
case refine_2
α : Type u_1
inst✝ : CommSemiring α
a b : { a // a.1 * a.2 = 0 ∧ a.1 + a.2 = 1 }
eq : (↑a).2 = (↑b).2
⊢ (↑a).2 + (↑a).1 = 1

Tactic:
rw [add_comm, a.2.2]

Result:
no goals

Proof state:
case refine_1
α : Type u_1
inst✝ : CommSemiring α
a b : { a // a.1 * a.2 = 0 ∧ a.1 + a.2 = 1 }
eq : (↑a).2 = (↑b).2
⊢ (↑a).2 * (↑a).1 = (↑b).1 * (↑a).2

Tactic:
rw [mul_comm, a.2.1, eq, b.2.1]

Result:
no goals

Proof state:
case refine_3
α : Type u_1
inst✝ : CommSemiring α
a b : { a // a.1 * a.2 = 0 ∧ a.1 + a.2 = 1 }
eq : (↑a).2 = (↑b).2
⊢ (↑a).2 + (↑b).1 = 1

Tactic:
rw [add_comm, eq, b.2.2]

Result:
no goals
-- Mathlib/AlgebraicGeometry/AffineScheme.lean
theorem basicOpen_union_eq_self_iff (s : Set Γ(X, U)) :
    ⨆ f : s, X.basicOpen (f : Γ(X, U)) = U ↔ Ideal.span s = ⊤

Proof state:
case h
X : Scheme
U : X.Opens
hU : IsAffineOpen U
s : Set ↑Γ(X, U)
h : ↑U ⊆ ↑(⨆ f, X.basicOpen ↑f)
x : ↑Γ(X, U)
h✝ : x ∈ s
⊢ ↑(X.basicOpen x) ⊆ ↑U

Tactic:
exact X.basicOpen_le x

Result:
no goals

Proof state:
case h
X : Scheme
U : X.Opens
hU : IsAffineOpen U
s : Set ↑Γ(X, U)
h : ↑U ⊆ ↑(⨆ f, X.basicOpen ↑f)
⊢ ∀ x ∈ s, ↑(X.basicOpen x) ⊆ ↑U

Tactic:
intro x _

Result:
case h
X : Scheme
U : X.Opens
hU : IsAffineOpen U
s : Set ↑Γ(X, U)
h : ↑U ⊆ ↑(⨆ f, X.basicOpen ↑f)
x : ↑Γ(X, U)
h✝ : x ∈ s
⊢ ↑(X.basicOpen x) ⊆ ↑U

Proof state:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
s : Set ↑Γ(X, U)
h :
  ⇑(ConcreteCategory.hom hU.fromSpec.base) ⁻¹' (⨆ f, X.basicOpen ↑f).carrier =
    ⇑(ConcreteCategory.hom hU.fromSpec.base) ⁻¹' U.carrier
⊢ ⨆ f, X.basicOpen ↑f = U

Tactic:
apply_fun Set.image hU.fromSpec.base at h

Result:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
s : Set ↑Γ(X, U)
h :
  ⇑(ConcreteCategory.hom hU.fromSpec.base) ''
      (⇑(ConcreteCategory.hom hU.fromSpec.base) ⁻¹' (⨆ f, X.basicOpen ↑f).carrier) =
    ⇑(ConcreteCategory.hom hU.fromSpec.base) '' (⇑(ConcreteCategory.hom hU.fromSpec.base) ⁻¹' U.carrier)
⊢ ⨆ f, X.basicOpen ↑f = U

Proof state:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
s : Set ↑Γ(X, U)
h : ↑U ⊆ ↑(⨆ f, X.basicOpen ↑f)
⊢ ⨆ f, X.basicOpen ↑f = U

Tactic:
ext1

Result:
case h
X : Scheme
U : X.Opens
hU : IsAffineOpen U
s : Set ↑Γ(X, U)
h : ↑U ⊆ ↑(⨆ f, X.basicOpen ↑f)
⊢ ↑(⨆ f, X.basicOpen ↑f) = ↑U

Proof state:
X : Scheme
U : X.Opens
hU : IsAffineOpen U
s : Set ↑Γ(X, U)
⊢ PrimeSpectrum.zeroLocus (⋃ i, {↑i}) = ∅ ↔ PrimeSpectrum.zeroLocus s = ∅

Tactic:
simp only [Set.iUnion_singleton_eq_range, Subtype.range_val_subtype, Set.setOf_mem_eq]

Result:
no goals
-- Mathlib/Computability/AkraBazzi/AkraBazzi.lean
lemma dist_r_b' : ∀ᶠ n in atTop, ∀ i, ‖(r i n : ℝ) - b i * n‖ ≤ n / log n ^ 2

Proof state:
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
i : α
⊢ ∀ᶠ (x : ℕ) in atTop, ‖↑(r i x) - b i * ↑x‖ ≤ ↑x / log ↑x ^ 2

Tactic:
simpa using IsLittleO.eventuallyLE (R.dist_r_b i)

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
⊢ ∀ᶠ (n : ℕ) in atTop, ∀ (i : α), ‖↑(r i n) - b i * ↑n‖ ≤ ↑n / log ↑n ^ 2

Tactic:
rw [Filter.eventually_all]

Result:
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
⊢ ∀ (i : α), ∀ᶠ (x : ℕ) in atTop, ‖↑(r i x) - b i * ↑x‖ ≤ ↑x / log ↑x ^ 2

Proof state:
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
⊢ ∀ (i : α), ∀ᶠ (x : ℕ) in atTop, ‖↑(r i x) - b i * ↑x‖ ≤ ↑x / log ↑x ^ 2

Tactic:
intro i

Result:
α : Type u_1
inst✝¹ : Fintype α
T : ℕ → ℝ
g : ℝ → ℝ
a b : α → ℝ
r : α → ℕ → ℕ
inst✝ : Nonempty α
R : AkraBazziRecurrence T g a b r
i : α
⊢ ∀ᶠ (x : ℕ) in atTop, ‖↑(r i x) - b i * ↑x‖ ≤ ↑x / log ↑x ^ 2