harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Zip.lean
theorem map_zip_eq_zipWith (f : α × β → γ) (l : Array α) (l' : Array β) :
    map f (l.zip l') = zipWith (Function.curry f) l l'

Proof state:
case mk
α : Type u_1
β : Type u_2
γ : Type u_3
f : α × β → γ
l' : Array β
toList✝ : List α
⊢ map f ({ toList := toList✝ }.zip l') = zipWith (Function.curry f) { toList := toList✝ } l'

Tactic:
cases l'

Result:
case mk.mk
α : Type u_1
β : Type u_2
γ : Type u_3
f : α × β → γ
toList✝¹ : List α
toList✝ : List β
⊢ map f ({ toList := toList✝¹ }.zip { toList := toList✝ }) =
    zipWith (Function.curry f) { toList := toList✝¹ } { toList := toList✝ }

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α × β → γ
l : Array α
l' : Array β
⊢ map f (l.zip l') = zipWith (Function.curry f) l l'

Tactic:
cases l

Result:
case mk
α : Type u_1
β : Type u_2
γ : Type u_3
f : α × β → γ
l' : Array β
toList✝ : List α
⊢ map f ({ toList := toList✝ }.zip l') = zipWith (Function.curry f) { toList := toList✝ } l'

Proof state:
case mk.mk
α : Type u_1
β : Type u_2
γ : Type u_3
f : α × β → γ
toList✝¹ : List α
toList✝ : List β
⊢ map f ({ toList := toList✝¹ }.zip { toList := toList✝ }) =
    zipWith (Function.curry f) { toList := toList✝¹ } { toList := toList✝ }

Tactic:
simp [List.map_zip_eq_zipWith]

Result:
no goals
-- Mathlib/Topology/Order/LeftRightNhds.lean
theorem nhds_basis_Ioo_pos [NoMaxOrder α] (a : α) :
    (𝓝 a).HasBasis (fun ε : α => (0 : α) < ε) fun ε => Ioo (a - ε) (a + ε)

Proof state:
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrderedAddCommGroup α
inst✝¹ : OrderTopology α
inst✝ : NoMaxOrder α
a : α
⊢ (𝓝 a).HasBasis (fun ε => 0 < ε) fun ε => Ioo (a - ε) (a + ε)

Tactic:
convert nhds_basis_abs_sub_lt a

Result:
case h.e'_5.h
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrderedAddCommGroup α
inst✝¹ : OrderTopology α
inst✝ : NoMaxOrder α
a x✝ : α
⊢ Ioo (a - x✝) (a + x✝) = {b | |b - a| < x✝}

Proof state:
case h.e'_5.h
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrderedAddCommGroup α
inst✝¹ : OrderTopology α
inst✝ : NoMaxOrder α
a x✝ : α
⊢ Ioo (a - x✝) (a + x✝) = {b | |b - a| < x✝}

Tactic:
simp only [Ioo, abs_lt, ← sub_lt_iff_lt_add, neg_lt_sub_iff_lt_add, sub_lt_comm]

Result:
no goals
-- Mathlib/Topology/Algebra/InfiniteSum/Module.lean
theorem ContinuousLinearEquiv.tsum_eq_iff [T2Space M] [T2Space M₂] {f : ι → M} (e : M ≃SL[σ] M₂)
    {y : M₂} : (∑' z, e (f z)) = y ↔ ∑' z, f z = e.symm y

Proof state:
case neg
ι : Type u_5
R : Type u_7
R₂ : Type u_8
M : Type u_9
M₂ : Type u_10
inst✝¹¹ : Semiring R
inst✝¹⁰ : Semiring R₂
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module R M
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : Module R₂ M₂
inst✝⁵ : TopologicalSpace M
inst✝⁴ : TopologicalSpace M₂
σ : R →+* R₂
σ' : R₂ →+* R
inst✝³ : RingHomInvPair σ σ'
inst✝² : RingHomInvPair σ' σ
inst✝¹ : T2Space M
inst✝ : T2Space M₂
f : ι → M
e : M ≃SL[σ] M₂
y : M₂
hf : ¬Summable f
hf' : ¬Summable fun z => e (f z)
⊢ ∑' (z : ι), e (f z) = y ↔ ∑' (z : ι), f z = e.symm y

Tactic:
rw [tsum_eq_zero_of_not_summable hf, tsum_eq_zero_of_not_summable hf']

Result:
case neg
ι : Type u_5
R : Type u_7
R₂ : Type u_8
M : Type u_9
M₂ : Type u_10
inst✝¹¹ : Semiring R
inst✝¹⁰ : Semiring R₂
inst✝⁹ : AddCommMonoid M
inst✝⁸ : Module R M
inst✝⁷ : AddCommMonoid M₂
inst✝⁶ : Module R₂ M₂
inst✝⁵ : TopologicalSpace M
inst✝⁴ : TopologicalSpace M₂
σ : R →+* R₂
σ' : R₂ →+* R
inst✝³ : RingHomInvPair σ σ'
inst✝² : RingHomInvPair σ' σ
inst✝¹ : T2Space M
inst✝ : T2Space M₂
f : ι → M
e : M ≃SL[σ] M₂
y : M₂
hf : ¬Summable f
hf' : ¬Summable fun z => e (f z)
⊢ 0 = y ↔ 0 = e.symm y
-- Mathlib/Algebra/Module/Submodule/Pointwise.lean
lemma set_smul_eq_iSup [SMulCommClass S R M] (s : Set S) (N : Submodule R M) :
    s • N = ⨆ (a ∈ s), a • N

Proof state:
R : Type u_2
M : Type u_3
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
S : Type u_4
inst✝² : Monoid S
inst✝¹ : DistribMulAction S M
inst✝ : SMulCommClass S R M
s : Set S
N : Submodule R M
⊢ s • N = ⨆ a ∈ s, a • N

Tactic:
refine Eq.trans (congrArg sInf ?_) csInf_Ici

Result:
R : Type u_2
M : Type u_3
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
S : Type u_4
inst✝² : Monoid S
inst✝¹ : DistribMulAction S M
inst✝ : SMulCommClass S R M
s : Set S
N : Submodule R M
⊢ {p | ∀ ⦃r : S⦄ ⦃n : M⦄, r ∈ s → n ∈ N → r • n ∈ p} = Set.Ici (⨆ a ∈ s, a • N)

Proof state:
R : Type u_2
M : Type u_3
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
S : Type u_4
inst✝² : Monoid S
inst✝¹ : DistribMulAction S M
inst✝ : SMulCommClass S R M
s : Set S
N : Submodule R M
⊢ {p | ∀ ⦃r : S⦄, r ∈ s → ∀ a ∈ N, r • a ∈ p} = {x | ∀ i ∈ s, i • N ≤ x}

Tactic:
exact Set.ext fun _ => forall₂_congr (fun _ _ => Iff.symm map_le_iff_le_comap)

Result:
no goals

Proof state:
R : Type u_2
M : Type u_3
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
S : Type u_4
inst✝² : Monoid S
inst✝¹ : DistribMulAction S M
inst✝ : SMulCommClass S R M
s : Set S
N : Submodule R M
⊢ {p | ∀ ⦃r : S⦄ ⦃n : M⦄, r ∈ s → n ∈ N → r • n ∈ p} = Set.Ici (⨆ a ∈ s, a • N)

Tactic:
simp_rw [← Set.Ici_def, iSup_le_iff, @forall_comm M]

Result:
R : Type u_2
M : Type u_3
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid M
inst✝³ : Module R M
S : Type u_4
inst✝² : Monoid S
inst✝¹ : DistribMulAction S M
inst✝ : SMulCommClass S R M
s : Set S
N : Submodule R M
⊢ {p | ∀ ⦃r : S⦄, r ∈ s → ∀ a ∈ N, r • a ∈ p} = {x | ∀ i ∈ s, i • N ≤ x}
-- Mathlib/AlgebraicGeometry/EllipticCurve/DivisionPolynomial/Degree.lean
lemma preΨ'_ne_zero [Nontrivial R] {n : ℕ} (h : (n : R) ≠ 0) : W.preΨ' n ≠ 0

Proof state:
case pos
R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : Nontrivial R
n : ℕ
h : ↑n ≠ 0
hn : 2 < n
⊢ W.preΨ' n ≠ 0

Tactic:
exact ne_zero_of_natDegree_gt <| W.natDegree_preΨ'_pos hn h

Result:
no goals

Proof state:
R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : Nontrivial R
n : ℕ
h : ↑n ≠ 0
⊢ W.preΨ' n ≠ 0

Tactic:
by_cases hn : 2 < n

Result:
case pos
R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : Nontrivial R
n : ℕ
h : ↑n ≠ 0
hn : 2 < n
⊢ W.preΨ' n ≠ 0

case neg
R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : Nontrivial R
n : ℕ
h : ↑n ≠ 0
hn : ¬2 < n
⊢ W.preΨ' n ≠ 0

Proof state:
case neg
R : Type u
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : Nontrivial R
n : ℕ
h : ↑n ≠ 0
hn : ¬2 < n
⊢ W.preΨ' n ≠ 0

Tactic:
rcases n with _ | _ | _ <;> aesop

Result:
no goals
-- Mathlib/RingTheory/DedekindDomain/Ideal.lean
theorem integrallyClosed : IsIntegrallyClosed A

Proof state:
A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDomain A
h : IsDedekindDomainInv A
⊢ IsIntegrallyClosed A

Tactic:
refine (isIntegrallyClosed_iff (FractionRing A)).mpr (fun {x hx} => ?_)

Result:
A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDomain A
h : IsDedekindDomainInv A
x : FractionRing A
hx : IsIntegral A x
⊢ ∃ y, (algebraMap A (FractionRing A)) y = x

Proof state:
A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDomain A
h : IsDedekindDomainInv A
x : FractionRing A
hx : IsIntegral A x
⊢ adjoinIntegral A⁰ x hx ≠ 0

Tactic:
exact fun h => one_ne_zero (eq_zero_iff.mp h 1 (Algebra.adjoin A {x}).one_mem)

Result:
no goals

Proof state:
A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDomain A
h : IsDedekindDomainInv A
x : FractionRing A
hx : IsIntegral A x
⊢ ∃ y, (algebraMap A (FractionRing A)) y = x

Tactic:
rw [← Set.mem_range, ← Algebra.mem_bot, ← Subalgebra.mem_toSubmodule, Algebra.toSubmodule_bot,
  Submodule.one_eq_span, ← coe_spanSingleton A⁰ (1 : FractionRing A), spanSingleton_one, ←
  FractionalIdeal.adjoinIntegral_eq_one_of_isUnit x hx (h.isUnit _)]

Result:
A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDomain A
h : IsDedekindDomainInv A
x : FractionRing A
hx : IsIntegral A x
⊢ x ∈ ↑(adjoinIntegral A⁰ x hx)

A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDomain A
h : IsDedekindDomainInv A
x : FractionRing A
hx : IsIntegral A x
⊢ adjoinIntegral A⁰ x hx ≠ 0

Proof state:
A : Type u_2
inst✝¹ : CommRing A
inst✝ : IsDomain A
h : IsDedekindDomainInv A
x : FractionRing A
hx : IsIntegral A x
⊢ x ∈ ↑(adjoinIntegral A⁰ x hx)

Tactic:
exact mem_adjoinIntegral_self A⁰ x hx

Result:
no goals
-- Mathlib/Algebra/Homology/Embedding/Boundary.lean
@[simp] lemma op_boundaryGE_iff {j : ι} : e.op.BoundaryGE j ↔ e.BoundaryLE j

Proof state:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
e : c.Embedding c'
j : ι
⊢ e.op.BoundaryGE j ↔ e.BoundaryLE j

Tactic:
rfl

Result:
no goals
-- Mathlib/Geometry/Euclidean/Angle/Oriented/RightAngle.lean
theorem oangle_add_left_eq_arctan_of_oangle_eq_pi_div_two {x y : V} (h : o.oangle x y = ↑(π / 2)) :
    o.oangle (x + y) y = Real.arctan (‖x‖ / ‖y‖)

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : (-o).oangle y x = ↑(π / 2)
⊢ (-o).oangle y (y + x) = ↑(Real.arctan (‖x‖ / ‖y‖))

Tactic:
exact (-o).oangle_add_right_eq_arctan_of_oangle_eq_pi_div_two h

Result:
no goals

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : o.oangle x y = ↑(π / 2)
⊢ o.oangle (x + y) y = ↑(Real.arctan (‖x‖ / ‖y‖))

Tactic:
rw [← neg_inj, oangle_rev, ← oangle_neg_orientation_eq_neg, neg_inj] at h ⊢

Result:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : (-o).oangle y x = ↑(π / 2)
⊢ (-o).oangle y (x + y) = ↑(Real.arctan (‖x‖ / ‖y‖))

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : (-o).oangle y x = ↑(π / 2)
⊢ (-o).oangle y (x + y) = ↑(Real.arctan (‖x‖ / ‖y‖))

Tactic:
rw [add_comm]

Result:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : (-o).oangle y x = ↑(π / 2)
⊢ (-o).oangle y (y + x) = ↑(Real.arctan (‖x‖ / ‖y‖))
-- Mathlib/Analysis/Calculus/MeanValue.lean
theorem antitoneOn_of_deriv_nonpos {D : Set ℝ} (hD : Convex ℝ D) {f : ℝ → ℝ}
    (hf : ContinuousOn f D) (hf' : DifferentiableOn ℝ f (interior D))
    (hf'_nonpos : ∀ x ∈ interior D, deriv f x ≤ 0) : AntitoneOn f D := fun x hx y hy hxy => by
  simpa only [zero_mul, sub_nonpos] using
    hD.image_sub_le_mul_sub_of_deriv_le hf hf' hf'_nonpos x hx y hy hxy

Proof state:
D : Set ℝ
hD : Convex ℝ D
f : ℝ → ℝ
hf : ContinuousOn f D
hf' : DifferentiableOn ℝ f (interior D)
hf'_nonpos : ∀ x ∈ interior D, deriv f x ≤ 0
x : ℝ
hx : x ∈ D
y : ℝ
hy : y ∈ D
hxy : x ≤ y
⊢ f y ≤ f x

Tactic:
simpa only [zero_mul, sub_nonpos] using
  hD.image_sub_le_mul_sub_of_deriv_le hf hf' hf'_nonpos x hx y hy hxy

Result:
no goals
-- Mathlib/Combinatorics/SetFamily/Compression/UV.lean
theorem compress_self (u a : α) : compress u u a = a

Proof state:
α : Type u_1
inst✝² : GeneralizedBooleanAlgebra α
inst✝¹ : DecidableRel Disjoint
inst✝ : DecidableRel fun x1 x2 => x1 ≤ x2
u a : α
⊢ (if Disjoint u a ∧ u ≤ a then (a ⊔ u) \ u else a) = a

Tactic:
split_ifs with h

Result:
case pos
α : Type u_1
inst✝² : GeneralizedBooleanAlgebra α
inst✝¹ : DecidableRel Disjoint
inst✝ : DecidableRel fun x1 x2 => x1 ≤ x2
u a : α
h : Disjoint u a ∧ u ≤ a
⊢ (a ⊔ u) \ u = a

case neg
α : Type u_1
inst✝² : GeneralizedBooleanAlgebra α
inst✝¹ : DecidableRel Disjoint
inst✝ : DecidableRel fun x1 x2 => x1 ≤ x2
u a : α
h : ¬(Disjoint u a ∧ u ≤ a)
⊢ a = a

Proof state:
case neg
α : Type u_1
inst✝² : GeneralizedBooleanAlgebra α
inst✝¹ : DecidableRel Disjoint
inst✝ : DecidableRel fun x1 x2 => x1 ≤ x2
u a : α
h : ¬(Disjoint u a ∧ u ≤ a)
⊢ a = a

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
inst✝² : GeneralizedBooleanAlgebra α
inst✝¹ : DecidableRel Disjoint
inst✝ : DecidableRel fun x1 x2 => x1 ≤ x2
u a : α
⊢ compress u u a = a

Tactic:
unfold compress

Result:
α : Type u_1
inst✝² : GeneralizedBooleanAlgebra α
inst✝¹ : DecidableRel Disjoint
inst✝ : DecidableRel fun x1 x2 => x1 ≤ x2
u a : α
⊢ (if Disjoint u a ∧ u ≤ a then (a ⊔ u) \ u else a) = a

Proof state:
case pos
α : Type u_1
inst✝² : GeneralizedBooleanAlgebra α
inst✝¹ : DecidableRel Disjoint
inst✝ : DecidableRel fun x1 x2 => x1 ≤ x2
u a : α
h : Disjoint u a ∧ u ≤ a
⊢ (a ⊔ u) \ u = a

Tactic:
exact h.1.symm.sup_sdiff_cancel_right

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/Symmetric.lean
theorem IsSymmetric.sub {T S : E →ₗ[𝕜] E} (hT : T.IsSymmetric) (hS : S.IsSymmetric) :
    (T - S).IsSymmetric

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T S : E →ₗ[𝕜] E
hT : T.IsSymmetric
hS : S.IsSymmetric
x y : E
⊢ inner ((T - S) x) y = inner x ((T - S) y)

Tactic:
rw [sub_apply, inner_sub_left, hT x y, hS x y, ← inner_sub_right, sub_apply]

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T S : E →ₗ[𝕜] E
hT : T.IsSymmetric
hS : S.IsSymmetric
⊢ (T - S).IsSymmetric

Tactic:
intro x y

Result:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T S : E →ₗ[𝕜] E
hT : T.IsSymmetric
hS : S.IsSymmetric
x y : E
⊢ inner ((T - S) x) y = inner x ((T - S) y)
-- Mathlib/Topology/Compactness/Compact.lean
theorem IsCompact.compl_mem_sets_of_nhdsWithin (hs : IsCompact s) {f : Filter X}
    (hf : ∀ x ∈ s, ∃ t ∈ 𝓝[s] x, tᶜ ∈ f) : sᶜ ∈ f

Proof state:
case intro.intro
X : Type u
inst✝ : TopologicalSpace X
s : Set X
hs : IsCompact s
f : Filter X
hf : ∀ x ∈ s, ∃ t ∈ 𝓝[s] x, tᶜ ∈ f
x : X
hx : x ∈ s
t : Set X
ht : t ∈ 𝓝[s] x
hst : tᶜ ∈ f
⊢ sᶜ ∈ 𝓝 x ⊓ f

Tactic:
replace ht := mem_inf_principal.1 ht

Result:
case intro.intro
X : Type u
inst✝ : TopologicalSpace X
s : Set X
hs : IsCompact s
f : Filter X
hf : ∀ x ∈ s, ∃ t ∈ 𝓝[s] x, tᶜ ∈ f
x : X
hx : x ∈ s
t : Set X
hst : tᶜ ∈ f
ht : {x | x ∈ s → x ∈ t} ∈ 𝓝 x
⊢ sᶜ ∈ 𝓝 x ⊓ f

Proof state:
case intro.intro
X : Type u
inst✝ : TopologicalSpace X
s : Set X
hs : IsCompact s
f : Filter X
hf : ∀ x ∈ s, ∃ t ∈ 𝓝[s] x, tᶜ ∈ f
x : X
hx : x ∈ s
t : Set X
hst : tᶜ ∈ f
ht : {x | x ∈ s → x ∈ t} ∈ 𝓝 x
⊢ {x | x ∈ s → x ∈ t} ∩ tᶜ ⊆ sᶜ

Tactic:
rintro x ⟨h₁, h₂⟩ hs

Result:
case intro.intro.intro
X : Type u
inst✝ : TopologicalSpace X
s : Set X
hs✝ : IsCompact s
f : Filter X
hf : ∀ x ∈ s, ∃ t ∈ 𝓝[s] x, tᶜ ∈ f
x✝ : X
hx : x✝ ∈ s
t : Set X
hst : tᶜ ∈ f
ht : {x | x ∈ s → x ∈ t} ∈ 𝓝 x✝
x : X
h₁ : x ∈ {x | x ∈ s → x ∈ t}
h₂ : x ∈ tᶜ
hs : x ∈ s
⊢ False

Proof state:
case intro.intro.intro
X : Type u
inst✝ : TopologicalSpace X
s : Set X
hs✝ : IsCompact s
f : Filter X
hf : ∀ x ∈ s, ∃ t ∈ 𝓝[s] x, tᶜ ∈ f
x✝ : X
hx : x✝ ∈ s
t : Set X
hst : tᶜ ∈ f
ht : {x | x ∈ s → x ∈ t} ∈ 𝓝 x✝
x : X
h₁ : x ∈ {x | x ∈ s → x ∈ t}
h₂ : x ∈ tᶜ
hs : x ∈ s
⊢ False

Tactic:
exact h₂ (h₁ hs)

Result:
no goals

Proof state:
X : Type u
inst✝ : TopologicalSpace X
s : Set X
hs : IsCompact s
f : Filter X
hf : ∀ x ∈ s, ∃ t ∈ 𝓝[s] x, tᶜ ∈ f
⊢ sᶜ ∈ f

Tactic:
refine hs.compl_mem_sets fun x hx => ?_

Result:
X : Type u
inst✝ : TopologicalSpace X
s : Set X
hs : IsCompact s
f : Filter X
hf : ∀ x ∈ s, ∃ t ∈ 𝓝[s] x, tᶜ ∈ f
x : X
hx : x ∈ s
⊢ sᶜ ∈ 𝓝 x ⊓ f

Proof state:
X : Type u
inst✝ : TopologicalSpace X
s : Set X
hs : IsCompact s
f : Filter X
hf : ∀ x ∈ s, ∃ t ∈ 𝓝[s] x, tᶜ ∈ f
x : X
hx : x ∈ s
⊢ sᶜ ∈ 𝓝 x ⊓ f

Tactic:
rcases hf x hx with ⟨t, ht, hst⟩

Result:
case intro.intro
X : Type u
inst✝ : TopologicalSpace X
s : Set X
hs : IsCompact s
f : Filter X
hf : ∀ x ∈ s, ∃ t ∈ 𝓝[s] x, tᶜ ∈ f
x : X
hx : x ∈ s
t : Set X
ht : t ∈ 𝓝[s] x
hst : tᶜ ∈ f
⊢ sᶜ ∈ 𝓝 x ⊓ f

Proof state:
case intro.intro
X : Type u
inst✝ : TopologicalSpace X
s : Set X
hs : IsCompact s
f : Filter X
hf : ∀ x ∈ s, ∃ t ∈ 𝓝[s] x, tᶜ ∈ f
x : X
hx : x ∈ s
t : Set X
hst : tᶜ ∈ f
ht : {x | x ∈ s → x ∈ t} ∈ 𝓝 x
⊢ sᶜ ∈ 𝓝 x ⊓ f

Tactic:
apply mem_inf_of_inter ht hst

Result:
case intro.intro
X : Type u
inst✝ : TopologicalSpace X
s : Set X
hs : IsCompact s
f : Filter X
hf : ∀ x ∈ s, ∃ t ∈ 𝓝[s] x, tᶜ ∈ f
x : X
hx : x ∈ s
t : Set X
hst : tᶜ ∈ f
ht : {x | x ∈ s → x ∈ t} ∈ 𝓝 x
⊢ {x | x ∈ s → x ∈ t} ∩ tᶜ ⊆ sᶜ
-- Mathlib/NumberTheory/Harmonic/ZetaAsymp.lean
lemma tendsto_riemannZeta_sub_one_div_Gammaℝ :
    Tendsto (fun s ↦ riemannZeta s - 1 / Gammaℝ s / (s - 1)) (𝓝[≠] 1)
    (𝓝 ((γ - Complex.log (4 * ↑π)) / 2))

Proof state:
this :
  Tendsto (fun x => riemannZeta x - 1 / (x - 1) + (1 / (x - 1) - 1 / x.Gammaℝ / (x - 1))) (𝓝[≠] 1)
    (𝓝 (↑γ + -(↑γ + Complex.log (4 * ↑π)) / 2))
⊢ Tendsto (fun s => riemannZeta s - 1 / s.Gammaℝ / (s - 1)) (𝓝[≠] 1) (𝓝 ((↑γ - Complex.log (4 * ↑π)) / 2))

Tactic:
simp_rw [sub_add_sub_cancel] at this

Result:
this : Tendsto (fun x => riemannZeta x - 1 / x.Gammaℝ / (x - 1)) (𝓝[≠] 1) (𝓝 (↑γ + -(↑γ + Complex.log (4 * ↑π)) / 2))
⊢ Tendsto (fun s => riemannZeta s - 1 / s.Gammaℝ / (s - 1)) (𝓝[≠] 1) (𝓝 ((↑γ - Complex.log (4 * ↑π)) / 2))

Proof state:
this : Tendsto (fun x => riemannZeta x - 1 / x.Gammaℝ / (x - 1)) (𝓝[≠] 1) (𝓝 (↑γ + -(↑γ + Complex.log (4 * ↑π)) / 2))
⊢ Tendsto (fun s => riemannZeta s - 1 / s.Gammaℝ / (s - 1)) (𝓝[≠] 1) (𝓝 ((↑γ - Complex.log (4 * ↑π)) / 2))

Tactic:
convert this using 2

Result:
case h.e'_5.h.e'_3
this : Tendsto (fun x => riemannZeta x - 1 / x.Gammaℝ / (x - 1)) (𝓝[≠] 1) (𝓝 (↑γ + -(↑γ + Complex.log (4 * ↑π)) / 2))
⊢ (↑γ - Complex.log (4 * ↑π)) / 2 = ↑γ + -(↑γ + Complex.log (4 * ↑π)) / 2

Proof state:
⊢ Tendsto (fun s => riemannZeta s - 1 / s.Gammaℝ / (s - 1)) (𝓝[≠] 1) (𝓝 ((↑γ - Complex.log (4 * ↑π)) / 2))

Tactic:
have := tendsto_riemannZeta_sub_one_div.add tendsto_Gamma_term_aux

Result:
this :
  Tendsto (fun x => riemannZeta x - 1 / (x - 1) + (1 / (x - 1) - 1 / x.Gammaℝ / (x - 1))) (𝓝[≠] 1)
    (𝓝 (↑γ + -(↑γ + Complex.log (4 * ↑π)) / 2))
⊢ Tendsto (fun s => riemannZeta s - 1 / s.Gammaℝ / (s - 1)) (𝓝[≠] 1) (𝓝 ((↑γ - Complex.log (4 * ↑π)) / 2))

Proof state:
case h.e'_5.h.e'_3
this : Tendsto (fun x => riemannZeta x - 1 / x.Gammaℝ / (x - 1)) (𝓝[≠] 1) (𝓝 (↑γ + -(↑γ + Complex.log (4 * ↑π)) / 2))
⊢ (↑γ - Complex.log (4 * ↑π)) / 2 = ↑γ + -(↑γ + Complex.log (4 * ↑π)) / 2

Tactic:
ring_nf

Result:
no goals
-- Mathlib/Analysis/Calculus/FDeriv/Add.lean
theorem HasStrictFDerivAt.add (hf : HasStrictFDerivAt f f' x)
    (hg : HasStrictFDerivAt g g' x) : HasStrictFDerivAt (fun y => f y + g y) (f' + g') x :=
   .of_isLittleO <| (hf.isLittleO.add hg.isLittleO).congr_left fun y => by
    simp only [LinearMap.sub_apply, LinearMap.add_apply, map_sub, map_add, add_apply]
    abel

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f g : E → F
f' g' : E →L[𝕜] F
x : E
hf : HasStrictFDerivAt f f' x
hg : HasStrictFDerivAt g g' x
y : E × E
⊢ f y.1 - f y.2 - (f' y.1 - f' y.2) + (g y.1 - g y.2 - (g' y.1 - g' y.2)) =
    f y.1 + g y.1 - (f y.2 + g y.2) - (f' y.1 + g' y.1 - (f' y.2 + g' y.2))

Tactic:
abel

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f g : E → F
f' g' : E →L[𝕜] F
x : E
hf : HasStrictFDerivAt f f' x
hg : HasStrictFDerivAt g g' x
y : E × E
⊢ f y.1 - f y.2 - f' (y.1 - y.2) + (g y.1 - g y.2 - g' (y.1 - y.2)) =
    f y.1 + g y.1 - (f y.2 + g y.2) - (f' + g') (y.1 - y.2)

Tactic:
simp only [LinearMap.sub_apply, LinearMap.add_apply, map_sub, map_add, add_apply]

Result:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f g : E → F
f' g' : E →L[𝕜] F
x : E
hf : HasStrictFDerivAt f f' x
hg : HasStrictFDerivAt g g' x
y : E × E
⊢ f y.1 - f y.2 - (f' y.1 - f' y.2) + (g y.1 - g y.2 - (g' y.1 - g' y.2)) =
    f y.1 + g y.1 - (f y.2 + g y.2) - (f' y.1 + g' y.1 - (f' y.2 + g' y.2))
-- Mathlib/Geometry/Euclidean/Angle/Unoriented/RightAngle.lean
theorem angle_add_eq_arccos_of_inner_eq_zero {x y : V} (h : ⟪x, y⟫ = 0) :
    angle x (x + y) = Real.arccos (‖x‖ / ‖x + y‖)

Proof state:
case pos
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x y = 0
hx : ‖x‖ = 0
⊢ Real.arccos (‖x‖ * ‖x‖ / (‖x‖ * ‖x + y‖)) = Real.arccos (‖x‖ / ‖x + y‖)

Tactic:
simp [hx]

Result:
no goals

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x y = 0
⊢ Real.arccos (‖x‖ * ‖x‖ / (‖x‖ * ‖x + y‖)) = Real.arccos (‖x‖ / ‖x + y‖)

Tactic:
by_cases hx : ‖x‖ = 0

Result:
case pos
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x y = 0
hx : ‖x‖ = 0
⊢ Real.arccos (‖x‖ * ‖x‖ / (‖x‖ * ‖x + y‖)) = Real.arccos (‖x‖ / ‖x + y‖)

case neg
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x y = 0
hx : ¬‖x‖ = 0
⊢ Real.arccos (‖x‖ * ‖x‖ / (‖x‖ * ‖x + y‖)) = Real.arccos (‖x‖ / ‖x + y‖)

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x y = 0
⊢ angle x (x + y) = Real.arccos (‖x‖ / ‖x + y‖)

Tactic:
rw [angle, inner_add_right, h, add_zero, real_inner_self_eq_norm_mul_norm]

Result:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x y = 0
⊢ Real.arccos (‖x‖ * ‖x‖ / (‖x‖ * ‖x + y‖)) = Real.arccos (‖x‖ / ‖x + y‖)

Proof state:
case neg
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
h : inner x y = 0
hx : ¬‖x‖ = 0
⊢ Real.arccos (‖x‖ * ‖x‖ / (‖x‖ * ‖x + y‖)) = Real.arccos (‖x‖ / ‖x + y‖)

Tactic:
rw [div_mul_eq_div_div, mul_self_div_self]

Result:
no goals
-- Mathlib/Data/Nat/Digits.lean
theorem head!_digits {b n : ℕ} (h : b ≠ 1) : (Nat.digits b n).head! = n % b

Proof state:
case pos.zero
b : ℕ
h : b ≠ 1
hb : 1 < b
⊢ (b.digits 0).head! = 0 % b

Tactic:
simp

Result:
no goals

Proof state:
case pos.succ
b : ℕ
h : b ≠ 1
hb : 1 < b
n : ℕ
⊢ (b.digits (n + 1)).head! = (b.digits (n + 1)).head! % b

Tactic:
exact (Nat.mod_eq_of_lt (Nat.digits_lt_base hb <| List.head!_mem_self <|
    Nat.digits_ne_nil_iff_ne_zero.mpr <| Nat.succ_ne_zero n)).symm

Result:
no goals

Proof state:
b n : ℕ
h : b ≠ 1
⊢ (b.digits n).head! = n % b

Tactic:
by_cases hb : 1 < b

Result:
case pos
b n : ℕ
h : b ≠ 1
hb : 1 < b
⊢ (b.digits n).head! = n % b

case neg
b n : ℕ
h : b ≠ 1
hb : ¬1 < b
⊢ (b.digits n).head! = n % b

Proof state:
case pos.succ
b : ℕ
h : b ≠ 1
hb : 1 < b
n : ℕ
⊢ (b.digits (n + 1)).head! = ofDigits b (b.digits (n + 1)) % b

Tactic:
rw [Nat.ofDigits_mod_eq_head! _ _]

Result:
case pos.succ
b : ℕ
h : b ≠ 1
hb : 1 < b
n : ℕ
⊢ (b.digits (n + 1)).head! = (b.digits (n + 1)).head! % b

Proof state:
b : ℕ
h : b ≠ 1
hb : ¬1 < b
n✝ : ℕ
⊢ b = 0

Tactic:
omega

Result:
no goals

Proof state:
case pos.succ
b : ℕ
h : b ≠ 1
hb : 1 < b
n : ℕ
⊢ (b.digits (n + 1)).head! = (n + 1) % b

Tactic:
nth_rw 2 [← Nat.ofDigits_digits b (n + 1)]

Result:
case pos.succ
b : ℕ
h : b ≠ 1
hb : 1 < b
n : ℕ
⊢ (b.digits (n + 1)).head! = ofDigits b (b.digits (n + 1)) % b

Proof state:
case neg
b n : ℕ
h : b ≠ 1
hb : ¬1 < b
⊢ (b.digits n).head! = n % b

Tactic:
rcases n with _ | _ <;> simp_all [show b = 0 by omega]

Result:
no goals

Proof state:
case pos
b n : ℕ
h : b ≠ 1
hb : 1 < b
⊢ (b.digits n).head! = n % b

Tactic:
rcases n with _ | n

Result:
case pos.zero
b : ℕ
h : b ≠ 1
hb : 1 < b
⊢ (b.digits 0).head! = 0 % b

case pos.succ
b : ℕ
h : b ≠ 1
hb : 1 < b
n : ℕ
⊢ (b.digits (n + 1)).head! = (n + 1) % b
-- Mathlib/Topology/MetricSpace/Infsep.lean
theorem einfsep_of_fintype [DecidableEq α] [Fintype s] :
    s.einfsep = s.offDiag.toFinset.inf (uncurry edist)

Proof state:
α : Type u_1
inst✝² : EDist α
s : Set α
inst✝¹ : DecidableEq α
inst✝ : Fintype ↑s
⊢ s.einfsep = s.offDiag.toFinset.inf (uncurry edist)

Tactic:
refine eq_of_forall_le_iff fun _ => ?_

Result:
α : Type u_1
inst✝² : EDist α
s : Set α
inst✝¹ : DecidableEq α
inst✝ : Fintype ↑s
x✝ : ℝ≥0∞
⊢ x✝ ≤ s.einfsep ↔ x✝ ≤ s.offDiag.toFinset.inf (uncurry edist)

Proof state:
α : Type u_1
inst✝² : EDist α
s : Set α
inst✝¹ : DecidableEq α
inst✝ : Fintype ↑s
x✝ : ℝ≥0∞
⊢ x✝ ≤ s.einfsep ↔ x✝ ≤ s.offDiag.toFinset.inf (uncurry edist)

Tactic:
simp_rw [le_einfsep_iff, imp_forall_iff, Finset.le_inf_iff, mem_toFinset, mem_offDiag,
  Prod.forall, uncurry_apply_pair, and_imp]

Result:
no goals