harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/GroupWithZero/Associated.lean
theorem Irreducible.dvd_iff [Monoid M] {x y : M} (hx : Irreducible x) :
    y ∣ x ↔ IsUnit y ∨ Associated x y

Proof state:
case mp.intro.inr
M : Type u_1
inst✝ : Monoid M
x y : M
hx : Irreducible x
z : M
hz : x = y * z
h : IsUnit z
⊢ IsUnit y ∨ y * z ~ᵤ y

Tactic:
exact Or.inr (associated_mul_unit_left _ _ h)

Result:
no goals

Proof state:
case mp
M : Type u_1
inst✝ : Monoid M
x y : M
hx : Irreducible x
⊢ y ∣ x → IsUnit y ∨ x ~ᵤ y

Tactic:
rintro ⟨z, hz⟩

Result:
case mp.intro
M : Type u_1
inst✝ : Monoid M
x y : M
hx : Irreducible x
z : M
hz : x = y * z
⊢ IsUnit y ∨ x ~ᵤ y

Proof state:
case mp.intro
M : Type u_1
inst✝ : Monoid M
x y : M
hx : Irreducible x
z : M
hz : x = y * z
⊢ IsUnit y ∨ x ~ᵤ y

Tactic:
obtain (h|h) := hx.isUnit_or_isUnit hz

Result:
case mp.intro.inl
M : Type u_1
inst✝ : Monoid M
x y : M
hx : Irreducible x
z : M
hz : x = y * z
h : IsUnit y
⊢ IsUnit y ∨ x ~ᵤ y

case mp.intro.inr
M : Type u_1
inst✝ : Monoid M
x y : M
hx : Irreducible x
z : M
hz : x = y * z
h : IsUnit z
⊢ IsUnit y ∨ x ~ᵤ y

Proof state:
case mpr
M : Type u_1
inst✝ : Monoid M
x y : M
hx : Irreducible x
⊢ IsUnit y ∨ x ~ᵤ y → y ∣ x

Tactic:
rintro (hy|h)

Result:
case mpr.inl
M : Type u_1
inst✝ : Monoid M
x y : M
hx : Irreducible x
hy : IsUnit y
⊢ y ∣ x

case mpr.inr
M : Type u_1
inst✝ : Monoid M
x y : M
hx : Irreducible x
h : x ~ᵤ y
⊢ y ∣ x

Proof state:
M : Type u_1
inst✝ : Monoid M
x y : M
hx : Irreducible x
⊢ y ∣ x ↔ IsUnit y ∨ x ~ᵤ y

Tactic:
constructor

Result:
case mp
M : Type u_1
inst✝ : Monoid M
x y : M
hx : Irreducible x
⊢ y ∣ x → IsUnit y ∨ x ~ᵤ y

case mpr
M : Type u_1
inst✝ : Monoid M
x y : M
hx : Irreducible x
⊢ IsUnit y ∨ x ~ᵤ y → y ∣ x

Proof state:
case mpr.inr
M : Type u_1
inst✝ : Monoid M
x y : M
hx : Irreducible x
h : x ~ᵤ y
⊢ y ∣ x

Tactic:
exact h.symm.dvd

Result:
no goals

Proof state:
case mp.intro.inr
M : Type u_1
inst✝ : Monoid M
x y : M
hx : Irreducible x
z : M
hz : x = y * z
h : IsUnit z
⊢ IsUnit y ∨ x ~ᵤ y

Tactic:
rw [hz]

Result:
case mp.intro.inr
M : Type u_1
inst✝ : Monoid M
x y : M
hx : Irreducible x
z : M
hz : x = y * z
h : IsUnit z
⊢ IsUnit y ∨ y * z ~ᵤ y

Proof state:
case mpr.inl
M : Type u_1
inst✝ : Monoid M
x y : M
hx : Irreducible x
hy : IsUnit y
⊢ y ∣ x

Tactic:
exact hy.dvd

Result:
no goals

Proof state:
case mp.intro.inl
M : Type u_1
inst✝ : Monoid M
x y : M
hx : Irreducible x
z : M
hz : x = y * z
h : IsUnit y
⊢ IsUnit y ∨ x ~ᵤ y

Tactic:
exact Or.inl h

Result:
no goals
-- Mathlib/Algebra/Homology/DerivedCategory/Ext/ExactSequences.lean
lemma contravariant_sequence_exact₂ {n : ℕ} (x₂ : Ext S.X₂ Y n)
    (hx₂ : (mk₀ S.f).comp x₂ (zero_add n) = 0) :
    ∃ (x₁ : Ext S.X₃ Y n), (mk₀ S.g).comp x₁ (zero_add n) = x₂

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
S : ShortComplex C
hS : S.ShortExact
Y : C
n : ℕ
x₂ : Ext S.X₂ Y n
hx₂ : (mk₀ S.f).comp x₂ ⋯ = 0
this : (ShortComplex.mk (AddCommGrp.ofHom ((mk₀ S.g).precomp Y ⋯)) (AddCommGrp.ofHom ((mk₀ S.f).precomp Y ⋯)) ⋯).Exact
⊢ ∃ x₁, (mk₀ S.g).comp x₁ ⋯ = x₂

Tactic:
rw [ShortComplex.ab_exact_iff] at this

Result:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
S : ShortComplex C
hS : S.ShortExact
Y : C
n : ℕ
x₂ : Ext S.X₂ Y n
hx₂ : (mk₀ S.f).comp x₂ ⋯ = 0
this :
  ∀
    (x₂ :
      ↑(ShortComplex.mk (AddCommGrp.ofHom ((mk₀ S.g).precomp Y ⋯)) (AddCommGrp.ofHom ((mk₀ S.f).precomp Y ⋯)) ⋯).X₂),
    (ConcreteCategory.hom
            (ShortComplex.mk (AddCommGrp.ofHom ((mk₀ S.g).precomp Y ⋯)) (AddCommGrp.ofHom ((mk₀ S.f).precomp Y ⋯)) ⋯).g)
          x₂ =
        0 →
      ∃ x₁,
        (ConcreteCategory.hom
              (ShortComplex.mk (AddCommGrp.ofHom ((mk₀ S.g).precomp Y ⋯)) (AddCommGrp.ofHom ((mk₀ S.f).precomp Y ⋯))
                  ⋯).f)
            x₁ =
          x₂
⊢ ∃ x₁, (mk₀ S.g).comp x₁ ⋯ = x₂

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
S : ShortComplex C
hS : S.ShortExact
Y : C
n : ℕ
x₂ : Ext S.X₂ Y n
hx₂ : (mk₀ S.f).comp x₂ ⋯ = 0
⊢ ∃ x₁, (mk₀ S.g).comp x₁ ⋯ = x₂

Tactic:
have := contravariant_sequence_exact₂' hS Y n

Result:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
S : ShortComplex C
hS : S.ShortExact
Y : C
n : ℕ
x₂ : Ext S.X₂ Y n
hx₂ : (mk₀ S.f).comp x₂ ⋯ = 0
this : (ShortComplex.mk (AddCommGrp.ofHom ((mk₀ S.g).precomp Y ⋯)) (AddCommGrp.ofHom ((mk₀ S.f).precomp Y ⋯)) ⋯).Exact
⊢ ∃ x₁, (mk₀ S.g).comp x₁ ⋯ = x₂

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Abelian C
inst✝ : HasExt C
S : ShortComplex C
hS : S.ShortExact
Y : C
n : ℕ
x₂ : Ext S.X₂ Y n
hx₂ : (mk₀ S.f).comp x₂ ⋯ = 0
this :
  ∀
    (x₂ :
      ↑(ShortComplex.mk (AddCommGrp.ofHom ((mk₀ S.g).precomp Y ⋯)) (AddCommGrp.ofHom ((mk₀ S.f).precomp Y ⋯)) ⋯).X₂),
    (ConcreteCategory.hom
            (ShortComplex.mk (AddCommGrp.ofHom ((mk₀ S.g).precomp Y ⋯)) (AddCommGrp.ofHom ((mk₀ S.f).precomp Y ⋯)) ⋯).g)
          x₂ =
        0 →
      ∃ x₁,
        (ConcreteCategory.hom
              (ShortComplex.mk (AddCommGrp.ofHom ((mk₀ S.g).precomp Y ⋯)) (AddCommGrp.ofHom ((mk₀ S.f).precomp Y ⋯))
                  ⋯).f)
            x₁ =
          x₂
⊢ ∃ x₁, (mk₀ S.g).comp x₁ ⋯ = x₂

Tactic:
exact this x₂ hx₂

Result:
no goals
-- Mathlib/LinearAlgebra/PiTensorProduct.lean
theorem map_range_eq_span_tprod :
    LinearMap.range (map f) =
      Submodule.span R {t | ∃ (m : Π i, s i), tprod R (fun i ↦ f i (m i)) = t}

Proof state:
ι : Type u_1
R : Type u_4
inst✝⁴ : CommSemiring R
s : ι → Type u_7
inst✝³ : (i : ι) → AddCommMonoid (s i)
inst✝² : (i : ι) → Module R (s i)
t : ι → Type u_11
inst✝¹ : (i : ι) → AddCommMonoid (t i)
inst✝ : (i : ι) → Module R (t i)
f : (i : ι) → s i →ₗ[R] t i
⊢ Submodule.span R (Set.range (⇑(map f) ∘ ⇑(tprod R))) =
    Submodule.span R {t_1 | ∃ m, (⨂ₜ[R] (i : ι), (f i) (m i)) = t_1}

Tactic:
apply congrArg

Result:
case h
ι : Type u_1
R : Type u_4
inst✝⁴ : CommSemiring R
s : ι → Type u_7
inst✝³ : (i : ι) → AddCommMonoid (s i)
inst✝² : (i : ι) → Module R (s i)
t : ι → Type u_11
inst✝¹ : (i : ι) → AddCommMonoid (t i)
inst✝ : (i : ι) → Module R (t i)
f : (i : ι) → s i →ₗ[R] t i
⊢ Set.range (⇑(map f) ∘ ⇑(tprod R)) = {t_1 | ∃ m, (⨂ₜ[R] (i : ι), (f i) (m i)) = t_1}

Proof state:
case h.h
ι : Type u_1
R : Type u_4
inst✝⁴ : CommSemiring R
s : ι → Type u_7
inst✝³ : (i : ι) → AddCommMonoid (s i)
inst✝² : (i : ι) → Module R (s i)
t : ι → Type u_11
inst✝¹ : (i : ι) → AddCommMonoid (t i)
inst✝ : (i : ι) → Module R (t i)
f : (i : ι) → s i →ₗ[R] t i
x : ⨂[R] (i : ι), t i
⊢ x ∈ Set.range (⇑(map f) ∘ ⇑(tprod R)) ↔ x ∈ {t_1 | ∃ m, (⨂ₜ[R] (i : ι), (f i) (m i)) = t_1}

Tactic:
simp only [Set.mem_range, comp_apply, map_tprod, Set.mem_setOf_eq]

Result:
no goals

Proof state:
ι : Type u_1
R : Type u_4
inst✝⁴ : CommSemiring R
s : ι → Type u_7
inst✝³ : (i : ι) → AddCommMonoid (s i)
inst✝² : (i : ι) → Module R (s i)
t : ι → Type u_11
inst✝¹ : (i : ι) → AddCommMonoid (t i)
inst✝ : (i : ι) → Module R (t i)
f : (i : ι) → s i →ₗ[R] t i
⊢ LinearMap.range (map f) = Submodule.span R {t_1 | ∃ m, (⨂ₜ[R] (i : ι), (f i) (m i)) = t_1}

Tactic:
rw [← Submodule.map_top, ← span_tprod_eq_top, Submodule.map_span, ← Set.range_comp]

Result:
ι : Type u_1
R : Type u_4
inst✝⁴ : CommSemiring R
s : ι → Type u_7
inst✝³ : (i : ι) → AddCommMonoid (s i)
inst✝² : (i : ι) → Module R (s i)
t : ι → Type u_11
inst✝¹ : (i : ι) → AddCommMonoid (t i)
inst✝ : (i : ι) → Module R (t i)
f : (i : ι) → s i →ₗ[R] t i
⊢ Submodule.span R (Set.range (⇑(map f) ∘ ⇑(tprod R))) =
    Submodule.span R {t_1 | ∃ m, (⨂ₜ[R] (i : ι), (f i) (m i)) = t_1}

Proof state:
case h
ι : Type u_1
R : Type u_4
inst✝⁴ : CommSemiring R
s : ι → Type u_7
inst✝³ : (i : ι) → AddCommMonoid (s i)
inst✝² : (i : ι) → Module R (s i)
t : ι → Type u_11
inst✝¹ : (i : ι) → AddCommMonoid (t i)
inst✝ : (i : ι) → Module R (t i)
f : (i : ι) → s i →ₗ[R] t i
⊢ Set.range (⇑(map f) ∘ ⇑(tprod R)) = {t_1 | ∃ m, (⨂ₜ[R] (i : ι), (f i) (m i)) = t_1}

Tactic:
ext x

Result:
case h.h
ι : Type u_1
R : Type u_4
inst✝⁴ : CommSemiring R
s : ι → Type u_7
inst✝³ : (i : ι) → AddCommMonoid (s i)
inst✝² : (i : ι) → Module R (s i)
t : ι → Type u_11
inst✝¹ : (i : ι) → AddCommMonoid (t i)
inst✝ : (i : ι) → Module R (t i)
f : (i : ι) → s i →ₗ[R] t i
x : ⨂[R] (i : ι), t i
⊢ x ∈ Set.range (⇑(map f) ∘ ⇑(tprod R)) ↔ x ∈ {t_1 | ∃ m, (⨂ₜ[R] (i : ι), (f i) (m i)) = t_1}
-- Mathlib/Algebra/Polynomial/Roots.lean
theorem zero_of_eval_zero [Infinite R] (p : R[X]) (h : ∀ x, p.eval x = 0) : p = 0

Proof state:
R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : Infinite R
p : R[X]
h : ∀ (x : R), eval x p = 0
⊢ p = 0

Tactic:
classical
by_contra hp
refine @Fintype.false R _ ?_
exact ⟨p.roots.toFinset, fun x => Multiset.mem_toFinset.mpr ((mem_roots hp).mpr (h _))⟩

Result:
no goals

Proof state:
R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : Infinite R
p : R[X]
h : ∀ (x : R), eval x p = 0
hp : ¬p = 0
⊢ False

Tactic:
refine @Fintype.false R _ ?_

Result:
R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : Infinite R
p : R[X]
h : ∀ (x : R), eval x p = 0
hp : ¬p = 0
⊢ Fintype R

Proof state:
R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : Infinite R
p : R[X]
h : ∀ (x : R), eval x p = 0
⊢ p = 0

Tactic:
by_contra hp

Result:
R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : Infinite R
p : R[X]
h : ∀ (x : R), eval x p = 0
hp : ¬p = 0
⊢ False

Proof state:
R : Type u
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : Infinite R
p : R[X]
h : ∀ (x : R), eval x p = 0
hp : ¬p = 0
⊢ Fintype R

Tactic:
exact ⟨p.roots.toFinset, fun x => Multiset.mem_toFinset.mpr ((mem_roots hp).mpr (h _))⟩

Result:
no goals
-- Mathlib/Algebra/Module/Submodule/Map.lean
theorem map_zero : map (0 : M →ₛₗ[σ₁₂] M₂) p = ⊥ :=
  have : ∃ x : M, x ∈ p := ⟨0, p.zero_mem⟩
  ext <| by simp [this, eq_comm]

Proof state:
R : Type u_1
R₂ : Type u_3
M : Type u_5
M₂ : Type u_7
inst✝⁶ : Semiring R
inst✝⁵ : Semiring R₂
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M₂
inst✝² : Module R M
inst✝¹ : Module R₂ M₂
σ₁₂ : R →+* R₂
p : Submodule R M
inst✝ : RingHomSurjective σ₁₂
this : ∃ x, x ∈ p
⊢ ∀ (x : M₂), x ∈ map 0 p ↔ x ∈ ⊥

Tactic:
simp [this, eq_comm]

Result:
no goals
-- Mathlib/Geometry/Manifold/MFDeriv/SpecificFunctions.lean
theorem tangentMap_prod_fst {p : TangentBundle (I.prod I') (M × M')} :
    tangentMap (I.prod I') I Prod.fst p = ⟨p.proj.1, p.2.1⟩

Proof state:
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
E' : Type u_5
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝² : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
p : TangentBundle (I.prod I') (M × M')
⊢ tangentMap (I.prod I') I Prod.fst p = { proj := p.proj.1, snd := p.snd.1 }

Tactic:
simp [tangentMap]

Result:
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
E' : Type u_5
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝² : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
p : TangentBundle (I.prod I') (M × M')
⊢ (ContinuousLinearMap.fst 𝕜 (TangentSpace I p.proj.1) (TangentSpace I' p.proj.2)) p.snd = p.snd.1

Proof state:
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁷ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
E' : Type u_5
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝² : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
p : TangentBundle (I.prod I') (M × M')
⊢ (ContinuousLinearMap.fst 𝕜 (TangentSpace I p.proj.1) (TangentSpace I' p.proj.2)) p.snd = p.snd.1

Tactic:
rfl

Result:
no goals
-- Mathlib/Algebra/BigOperators/Associated.lean
theorem prod_le_prod {p q : Multiset (Associates α)} (h : p ≤ q) : p.prod ≤ q.prod

Proof state:
α : Type u_1
inst✝ : CommMonoid α
p q : Multiset (Associates α)
h : p ≤ q
this : DecidableEq (Associates α)
⊢ p.prod ≤ q.prod

Tactic:
haveI := Classical.decEq α

Result:
α : Type u_1
inst✝ : CommMonoid α
p q : Multiset (Associates α)
h : p ≤ q
this✝ : DecidableEq (Associates α)
this : DecidableEq α
⊢ p.prod ≤ q.prod

Proof state:
α : Type u_1
inst✝ : CommMonoid α
p q : Multiset (Associates α)
h : p ≤ q
this✝¹ : DecidableEq (Associates α)
this✝ : DecidableEq α
this : p.prod * 1 ≤ p.prod * (q - p).prod
⊢ p.prod ≤ (p + (q - p)).prod

Tactic:
simpa

Result:
no goals

Proof state:
α : Type u_1
inst✝ : CommMonoid α
p q : Multiset (Associates α)
h : p ≤ q
⊢ p.prod ≤ q.prod

Tactic:
haveI := Classical.decEq (Associates α)

Result:
α : Type u_1
inst✝ : CommMonoid α
p q : Multiset (Associates α)
h : p ≤ q
this : DecidableEq (Associates α)
⊢ p.prod ≤ q.prod

Proof state:
α : Type u_1
inst✝ : CommMonoid α
p q : Multiset (Associates α)
h : p ≤ q
this✝¹ : DecidableEq (Associates α)
this✝ : DecidableEq α
this : p.prod ≤ (p + (q - p)).prod
⊢ p.prod ≤ q.prod

Tactic:
rwa [add_tsub_cancel_of_le h] at this

Result:
no goals

Proof state:
α : Type u_1
inst✝ : CommMonoid α
p q : Multiset (Associates α)
h : p ≤ q
this✝ : DecidableEq (Associates α)
this : DecidableEq α
⊢ p.prod * 1 ≤ p.prod * (q - p).prod

Tactic:
exact mul_mono (le_refl p.prod) one_le

Result:
no goals

Proof state:
α : Type u_1
inst✝ : CommMonoid α
p q : Multiset (Associates α)
h : p ≤ q
this✝ : DecidableEq (Associates α)
this : DecidableEq α
⊢ p.prod ≤ q.prod

Tactic:
suffices p.prod ≤ (p + (q - p)).prod by rwa [add_tsub_cancel_of_le h] at this

Result:
α : Type u_1
inst✝ : CommMonoid α
p q : Multiset (Associates α)
h : p ≤ q
this✝ : DecidableEq (Associates α)
this : DecidableEq α
⊢ p.prod ≤ (p + (q - p)).prod

Proof state:
α : Type u_1
inst✝ : CommMonoid α
p q : Multiset (Associates α)
h : p ≤ q
this✝ : DecidableEq (Associates α)
this : DecidableEq α
⊢ p.prod ≤ (p + (q - p)).prod

Tactic:
suffices p.prod * 1 ≤ p.prod * (q - p).prod by simpa

Result:
α : Type u_1
inst✝ : CommMonoid α
p q : Multiset (Associates α)
h : p ≤ q
this✝ : DecidableEq (Associates α)
this : DecidableEq α
⊢ p.prod * 1 ≤ p.prod * (q - p).prod
-- Mathlib/NumberTheory/LSeries/HurwitzZetaEven.lean
/-- Formula for `hurwitzZetaEven` as a Dirichlet series in the convergence range, with sum over `ℕ`
(version without absolute values, assuming `a ∈ Icc 0 1`) -/
lemma hasSum_nat_hurwitzZetaEven_of_mem_Icc {a : ℝ} (ha : a ∈ Icc 0 1) {s : ℂ} (hs : 1 < re s) :
    HasSum (fun n : ℕ ↦ (1 / (n + a : ℂ) ^ s + 1 / (n + 1 - a : ℂ) ^ s) / 2)
    (hurwitzZetaEven a s)

Proof state:
a : ℝ
ha : a ∈ Icc 0 1
s : ℂ
hs : 1 < s.re
⊢ HasSum (fun n => (1 / (↑n + ↑a) ^ s + 1 / (↑n + 1 - ↑a) ^ s) / 2) (hurwitzZetaEven (↑a) s)

Tactic:
refine (hasSum_nat_hurwitzZetaEven a hs).congr_fun fun n ↦ ?_

Result:
a : ℝ
ha : a ∈ Icc 0 1
s : ℂ
hs : 1 < s.re
n : ℕ
⊢ (1 / (↑n + ↑a) ^ s + 1 / (↑n + 1 - ↑a) ^ s) / 2 = (1 / ↑|↑n + a| ^ s + 1 / ↑|↑n + 1 - a| ^ s) / 2

Proof state:
a : ℝ
ha : a ∈ Icc 0 1
s : ℂ
hs : 1 < s.re
n : ℕ
⊢ 0 ≤ ↑n + 1 - a

Tactic:
linarith [ha.1, ha.2]

Result:
no goals

Proof state:
a : ℝ
ha : a ∈ Icc 0 1
s : ℂ
hs : 1 < s.re
n : ℕ
⊢ (1 / (↑n + ↑a) ^ s + 1 / (↑n + 1 - ↑a) ^ s) / 2 = (1 / ↑|↑n + a| ^ s + 1 / ↑|↑n + 1 - a| ^ s) / 2

Tactic:
congr 2 <;>
rw [abs_of_nonneg (by linarith [ha.1, ha.2])] <;>
simp

Result:
no goals
-- Mathlib/Data/Real/EReal.lean
@[simp]
lemma preimage_coe_Ioo_bot (y : ℝ) : Real.toEReal ⁻¹' Ioo ⊥ y = Iio y

Proof state:
y : ℝ
⊢ Real.toEReal ⁻¹' Ioo ⊥ ↑y = Iio y

Tactic:
rw [← Ioi_inter_Iio]

Result:
y : ℝ
⊢ Real.toEReal ⁻¹' (Ioi ⊥ ∩ Iio ↑y) = Iio y

Proof state:
y : ℝ
⊢ Real.toEReal ⁻¹' (Ioi ⊥ ∩ Iio ↑y) = Iio y

Tactic:
simp

Result:
no goals
-- Mathlib/Order/Filter/Map.lean
theorem Filter.map_surjOn_Iic_iff_surjOn {s : Set α} {t : Set β} {m : α → β} :
    SurjOn (map m) (Iic <| 𝓟 s) (Iic <| 𝓟 t) ↔ SurjOn m s t

Proof state:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
m : α → β
⊢ SurjOn (map m) (Iic (𝓟 s)) (Iic (𝓟 t)) ↔ SurjOn m s t

Tactic:
rw [map_surjOn_Iic_iff_le_map, map_principal, principal_mono, SurjOn]

Result:
no goals
-- Mathlib/Data/Set/Lattice.lean
theorem biUnion_iUnion (s : ι → Set α) (t : α → Set β) :
    ⋃ x ∈ ⋃ i, s i, t x = ⋃ (i) (x ∈ s i), t x

Proof state:
α : Type u_1
β : Type u_2
ι : Sort u_5
s : ι → Set α
t : α → Set β
⊢ ⋃ x ∈ ⋃ i, s i, t x = ⋃ i, ⋃ x ∈ s i, t x

Tactic:
simp [@iUnion_comm _ ι]

Result:
no goals
-- Mathlib/MeasureTheory/Constructions/BorelSpace/Order.lean
theorem AEMeasurable.iSup {ι} {μ : Measure δ} [Countable ι] {f : ι → δ → α}
    (hf : ∀ i, AEMeasurable (f i) μ) : AEMeasurable (fun b => ⨆ i, f i b) μ

Proof state:
α : Type u_1
δ : Type u_4
inst✝⁵ : TopologicalSpace α
mα : MeasurableSpace α
inst✝⁴ : BorelSpace α
mδ : MeasurableSpace δ
inst✝³ : ConditionallyCompleteLinearOrder α
inst✝² : OrderTopology α
inst✝¹ : SecondCountableTopology α
ι : Sort u_5
μ : Measure δ
inst✝ : Countable ι
f : ι → δ → α
hf : ∀ (i : ι), AEMeasurable (f i) μ
b : δ
hb : ∀ (i : ι), f i b = mk (f i) ⋯ b
⊢ ⨆ i, f i b = ⨆ i, mk (f i) ⋯ b

Tactic:
simp [hb]

Result:
no goals

Proof state:
α : Type u_1
δ : Type u_4
inst✝⁵ : TopologicalSpace α
mα : MeasurableSpace α
inst✝⁴ : BorelSpace α
mδ : MeasurableSpace δ
inst✝³ : ConditionallyCompleteLinearOrder α
inst✝² : OrderTopology α
inst✝¹ : SecondCountableTopology α
ι : Sort u_5
μ : Measure δ
inst✝ : Countable ι
f : ι → δ → α
hf : ∀ (i : ι), AEMeasurable (f i) μ
⊢ (fun b => ⨆ i, f i b) =ᶠ[ae μ] fun b => ⨆ i, mk (f i) ⋯ b

Tactic:
filter_upwards [ae_all_iff.2 (fun i ↦ (hf i).ae_eq_mk)] with b hb using by simp [hb]

Result:
no goals

Proof state:
α : Type u_1
δ : Type u_4
inst✝⁵ : TopologicalSpace α
mα : MeasurableSpace α
inst✝⁴ : BorelSpace α
mδ : MeasurableSpace δ
inst✝³ : ConditionallyCompleteLinearOrder α
inst✝² : OrderTopology α
inst✝¹ : SecondCountableTopology α
ι : Sort u_5
μ : Measure δ
inst✝ : Countable ι
f : ι → δ → α
hf : ∀ (i : ι), AEMeasurable (f i) μ
⊢ AEMeasurable (fun b => ⨆ i, f i b) μ

Tactic:
refine ⟨fun b ↦ ⨆ i, (hf i).mk (f i) b, .iSup (fun i ↦ (hf i).measurable_mk), ?_⟩

Result:
α : Type u_1
δ : Type u_4
inst✝⁵ : TopologicalSpace α
mα : MeasurableSpace α
inst✝⁴ : BorelSpace α
mδ : MeasurableSpace δ
inst✝³ : ConditionallyCompleteLinearOrder α
inst✝² : OrderTopology α
inst✝¹ : SecondCountableTopology α
ι : Sort u_5
μ : Measure δ
inst✝ : Countable ι
f : ι → δ → α
hf : ∀ (i : ι), AEMeasurable (f i) μ
⊢ (fun b => ⨆ i, f i b) =ᶠ[ae μ] fun b => ⨆ i, mk (f i) ⋯ b
-- Mathlib/AlgebraicGeometry/Sites/SmallAffineZariski.lean
lemma mem_grothendieckTopology {U : X.AffineZariskiSite} {S : Sieve U} :
    S ∈ grothendieckTopology X U ↔
      ∀ x ∈ U.toOpens, ∃ (V : _) (f : V ⟶ U), S.arrows f ∧ x ∈ V.toOpens

Proof state:
X : Scheme
U : X.AffineZariskiSite
S : Sieve U
x : ↑↑X.toPresheafedSpace
hxU : x ∈ (toOpensFunctor X).obj U
⊢ (∃ V f, S.arrows f ∧ x ∈ V.toOpens) → ∃ U_1 f, (Sieve.functorPushforward (toOpensFunctor X) S).arrows f ∧ x ∈ U_1

Tactic:
rintro ⟨W, g, hg, hxW⟩

Result:
case intro.intro.intro
X : Scheme
U : X.AffineZariskiSite
S : Sieve U
x : ↑↑X.toPresheafedSpace
hxU : x ∈ (toOpensFunctor X).obj U
W : X.AffineZariskiSite
g : W ⟶ U
hg : S.arrows g
hxW : x ∈ W.toOpens
⊢ ∃ U_1 f, (Sieve.functorPushforward (toOpensFunctor X) S).arrows f ∧ x ∈ U_1

Proof state:
X : Scheme
U : X.AffineZariskiSite
S : Sieve U
⊢ S ∈ (grothendieckTopology X) U ↔ ∀ x ∈ U.toOpens, ∃ V f, S.arrows f ∧ x ∈ V.toOpens

Tactic:
apply forall₂_congr fun x hxU ↦ ⟨?_, ?_⟩

Result:
X : Scheme
U : X.AffineZariskiSite
S : Sieve U
x : ↑↑X.toPresheafedSpace
hxU : x ∈ (toOpensFunctor X).obj U
⊢ (∃ U_1 f, (Sieve.functorPushforward (toOpensFunctor X) S).arrows f ∧ x ∈ U_1) → ∃ V f, S.arrows f ∧ x ∈ V.toOpens

X : Scheme
U : X.AffineZariskiSite
S : Sieve U
x : ↑↑X.toPresheafedSpace
hxU : x ∈ (toOpensFunctor X).obj U
⊢ (∃ V f, S.arrows f ∧ x ∈ V.toOpens) → ∃ U_1 f, (Sieve.functorPushforward (toOpensFunctor X) S).arrows f ∧ x ∈ U_1

Proof state:
case intro.intro.intro
X : Scheme
U : X.AffineZariskiSite
S : Sieve U
x : ↑↑X.toPresheafedSpace
hxU : x ∈ (toOpensFunctor X).obj U
W : X.AffineZariskiSite
g : W ⟶ U
hg : S.arrows g
hxW : x ∈ W.toOpens
⊢ ∃ U_1 f, (Sieve.functorPushforward (toOpensFunctor X) S).arrows f ∧ x ∈ U_1

Tactic:
exact ⟨W.toOpens, homOfLE (toOpens_mono g.le), ⟨W, g, 𝟙 _, hg, rfl⟩, hxW⟩

Result:
no goals

Proof state:
case intro.intro.intro.intro.intro.intro.intro
X : Scheme
U : X.AffineZariskiSite
S : Sieve U
x : ↑↑X.toPresheafedSpace
hxU : x ∈ (toOpensFunctor X).obj U
V : TopologicalSpace.Opens ↑↑X.toPresheafedSpace
hxV : x ∈ V
W : X.AffineZariskiSite
g : W ⟶ U
h : V ⟶ (toOpensFunctor X).obj W
hg : S.arrows g
⊢ ∃ V f, S.arrows f ∧ x ∈ V.toOpens

Tactic:
exact ⟨W, g, hg, h.le hxV⟩

Result:
no goals

Proof state:
X : Scheme
U : X.AffineZariskiSite
S : Sieve U
x : ↑↑X.toPresheafedSpace
hxU : x ∈ (toOpensFunctor X).obj U
⊢ (∃ U_1 f, (Sieve.functorPushforward (toOpensFunctor X) S).arrows f ∧ x ∈ U_1) → ∃ V f, S.arrows f ∧ x ∈ V.toOpens

Tactic:
rintro ⟨V, f, ⟨W, g, h, hg, rfl⟩, hxV⟩

Result:
case intro.intro.intro.intro.intro.intro.intro
X : Scheme
U : X.AffineZariskiSite
S : Sieve U
x : ↑↑X.toPresheafedSpace
hxU : x ∈ (toOpensFunctor X).obj U
V : TopologicalSpace.Opens ↑↑X.toPresheafedSpace
hxV : x ∈ V
W : X.AffineZariskiSite
g : W ⟶ U
h : V ⟶ (toOpensFunctor X).obj W
hg : S.arrows g
⊢ ∃ V f, S.arrows f ∧ x ∈ V.toOpens
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Count.lean
theorem size_eq_countP_add_countP (l) : l.size = countP p l + countP (fun a => ¬p a) l

Proof state:
case mk
α : Type u_1
p : α → Bool
toList✝ : List α
⊢ { toList := toList✝ }.size =
    countP p { toList := toList✝ } + countP (fun a => decide ¬p a = true) { toList := toList✝ }

Tactic:
simp [List.length_eq_countP_add_countP (p := p)]

Result:
no goals

Proof state:
α : Type u_1
p : α → Bool
l : Array α
⊢ l.size = countP p l + countP (fun a => decide ¬p a = true) l

Tactic:
cases l

Result:
case mk
α : Type u_1
p : α → Bool
toList✝ : List α
⊢ { toList := toList✝ }.size =
    countP p { toList := toList✝ } + countP (fun a => decide ¬p a = true) { toList := toList✝ }
-- Mathlib/Order/PartialSups.lean
theorem partialSups_eq_sup'_range (f : ℕ → α) (n : ℕ) :
    partialSups f n = (Finset.range (n + 1)).sup' nonempty_range_succ f :=
  eq_of_forall_ge_iff fun _ ↦ by simp [Nat.lt_succ_iff]

Proof state:
α : Type u_1
inst✝ : SemilatticeSup α
f : ℕ → α
n : ℕ
x✝ : α
⊢ (partialSups f) n ≤ x✝ ↔ (range (n + 1)).sup' ⋯ f ≤ x✝

Tactic:
simp [Nat.lt_succ_iff]

Result:
no goals
-- Mathlib/Geometry/Euclidean/Angle/Oriented/Basic.lean
theorem oangle_neg_right {x y : V} (hx : x ≠ 0) (hy : y ≠ 0) :
    o.oangle x (-y) = o.oangle x y + π

Proof state:
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
hx : x ≠ 0
hy : y ≠ 0
⊢ ↑(-(o.kahler x) y).arg = ↑((o.kahler x) y).arg + ↑π

Tactic:
convert Complex.arg_neg_coe_angle _

Result:
case convert_2
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
hx : x ≠ 0
hy : y ≠ 0
⊢ (o.kahler x) y ≠ 0

Proof state:
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
hx : x ≠ 0
hy : y ≠ 0
⊢ o.oangle x (-y) = o.oangle x y + ↑π

Tactic:
simp only [oangle, map_neg]

Result:
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
hx : x ≠ 0
hy : y ≠ 0
⊢ ↑(-(o.kahler x) y).arg = ↑((o.kahler x) y).arg + ↑π

Proof state:
case convert_2
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
hx : x ≠ 0
hy : y ≠ 0
⊢ (o.kahler x) y ≠ 0

Tactic:
exact o.kahler_ne_zero hx hy

Result:
no goals