harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem toList_beq_toList [BEq α] (a : Vector α n) (b : Vector α n) :
    (a.toList == b.toList) = (a == b)

Proof state:
α : Type u_1
n : Nat
inst✝ : BEq α
a b : Vector α n
⊢ (a.toList == b.toList) = (a == b)

Tactic:
simp [instBEq, isEqv, Array.instBEq, Array.isEqv, a.2, b.2]

Result:
no goals
-- Mathlib/Data/Multiset/AddSub.lean
protected lemma add_left_inj : s + u = t + u ↔ s = t

Proof state:
α : Type u_1
s t u : Multiset α
⊢ s + u = t + u ↔ s = t

Tactic:
classical simp [Multiset.ext]

Result:
no goals

Proof state:
α : Type u_1
s t u : Multiset α
⊢ s + u = t + u ↔ s = t

Tactic:
simp [Multiset.ext]

Result:
no goals
-- Mathlib/Data/Seq/Seq.lean
theorem map_comp (f : α → β) (g : β → γ) : ∀ s : Seq α, map (g ∘ f) s = map g (map f s)
  | ⟨s, al⟩ => by
    apply Subtype.eq; dsimp [map]
    apply congr_arg fun f : _ → Option γ => Stream'.map f s
    ext ⟨⟩ <;> rfl

Proof state:
case a
α : Type u
β : Type v
γ : Type w
f : α → β
g : β → γ
s : Stream' (Option α)
al : s.IsSeq
⊢ Option.map (g ∘ f) = Option.map g ∘ Option.map f

Tactic:
ext ⟨⟩ <;> rfl

Result:
no goals

Proof state:
α : Type u
β : Type v
γ : Type w
f : α → β
g : β → γ
s : Stream' (Option α)
al : s.IsSeq
⊢ map (g ∘ f) ⟨s, al⟩ = map g (map f ⟨s, al⟩)

Tactic:
apply Subtype.eq

Result:
case a
α : Type u
β : Type v
γ : Type w
f : α → β
g : β → γ
s : Stream' (Option α)
al : s.IsSeq
⊢ ↑(map (g ∘ f) ⟨s, al⟩) = ↑(map g (map f ⟨s, al⟩))

Proof state:
case a
α : Type u
β : Type v
γ : Type w
f : α → β
g : β → γ
s : Stream' (Option α)
al : s.IsSeq
⊢ Stream'.map (Option.map (g ∘ f)) s = Stream'.map (Option.map g ∘ Option.map f) s

Tactic:
apply congr_arg fun f : _ → Option γ => Stream'.map f s

Result:
case a
α : Type u
β : Type v
γ : Type w
f : α → β
g : β → γ
s : Stream' (Option α)
al : s.IsSeq
⊢ Option.map (g ∘ f) = Option.map g ∘ Option.map f

Proof state:
case a
α : Type u
β : Type v
γ : Type w
f : α → β
g : β → γ
s : Stream' (Option α)
al : s.IsSeq
⊢ ↑(map (g ∘ f) ⟨s, al⟩) = ↑(map g (map f ⟨s, al⟩))

Tactic:
dsimp [map]

Result:
case a
α : Type u
β : Type v
γ : Type w
f : α → β
g : β → γ
s : Stream' (Option α)
al : s.IsSeq
⊢ Stream'.map (Option.map (g ∘ f)) s = Stream'.map (Option.map g ∘ Option.map f) s
-- Mathlib/.lake/packages/lean4/src/lean/Init/Omega/Int.lean
theorem not_lt {i j : Fin n} : ¬ i < j ↔ j ≤ i

Proof state:
case mk.mk
n val✝¹ : Nat
isLt✝¹ : val✝¹ < n
val✝ : Nat
isLt✝ : val✝ < n
⊢ ¬⟨val✝¹, isLt✝¹⟩ < ⟨val✝, isLt✝⟩ ↔ ⟨val✝, isLt✝⟩ ≤ ⟨val✝¹, isLt✝¹⟩

Tactic:
exact Nat.not_lt

Result:
no goals

Proof state:
case mk
n : Nat
j : Fin n
val✝ : Nat
isLt✝ : val✝ < n
⊢ ¬⟨val✝, isLt✝⟩ < j ↔ j ≤ ⟨val✝, isLt✝⟩

Tactic:
cases j

Result:
case mk.mk
n val✝¹ : Nat
isLt✝¹ : val✝¹ < n
val✝ : Nat
isLt✝ : val✝ < n
⊢ ¬⟨val✝¹, isLt✝¹⟩ < ⟨val✝, isLt✝⟩ ↔ ⟨val✝, isLt✝⟩ ≤ ⟨val✝¹, isLt✝¹⟩

Proof state:
n : Nat
i j : Fin n
⊢ ¬i < j ↔ j ≤ i

Tactic:
cases i

Result:
case mk
n : Nat
j : Fin n
val✝ : Nat
isLt✝ : val✝ < n
⊢ ¬⟨val✝, isLt✝⟩ < j ↔ j ≤ ⟨val✝, isLt✝⟩
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/Reflect.lean
theorem false_of_eq_true_of_eq_false (h₁ : x = true) (h₂ : x = false) : False

Proof state:
x : Bool
h₁ : x = true
h₂ : x = false
⊢ False

Tactic:
cases h₁

Result:
case refl
h₂ : true = false
⊢ False

Proof state:
case refl
h₂ : true = false
⊢ False

Tactic:
cases h₂

Result:
no goals
-- Mathlib/CategoryTheory/Shift/Induced.lean
@[simp]
lemma shiftFunctorAdd_inv_app_obj_of_induced (a b : A) (X : C) :
    letI := HasShift.induced F A s i
    (shiftFunctorAdd D a b).inv.app (F.obj X) =
      (s b).map ((i a).hom.app X) ≫
      (i b).hom.app ((shiftFunctor C a).obj X) ≫
      F.map ((shiftFunctorAdd C a b).inv.app X) ≫
      (i (a + b)).inv.app X

Proof state:
C : Type u_4
D : Type u_2
inst✝⁵ : Category.{u_5, u_4} C
inst✝⁴ : Category.{u_1, u_2} D
F : C ⥤ D
A : Type u_3
inst✝³ : AddMonoid A
inst✝² : HasShift C A
s : A → D ⥤ D
i : (a : A) → F ⋙ s a ≅ shiftFunctor C a ⋙ F
inst✝¹ : ((whiskeringLeft C D D).obj F).Full
inst✝ : ((whiskeringLeft C D D).obj F).Faithful
a b : A
X : C
this : HasShift D A := HasShift.induced F A s i
⊢ (shiftFunctorAdd D a b).inv.app (F.obj X) =
    (s b).map ((i a).hom.app X) ≫
      (i b).hom.app ((shiftFunctor C a).obj X) ≫ F.map ((shiftFunctorAdd C a b).inv.app X) ≫ (i (a + b)).inv.app X

Tactic:
simp only [ShiftMkCore.shiftFunctorAdd_eq, HasShift.Induced.add_inv_app_obj]

Result:
no goals

Proof state:
C : Type u_4
D : Type u_2
inst✝⁵ : Category.{u_5, u_4} C
inst✝⁴ : Category.{u_1, u_2} D
F : C ⥤ D
A : Type u_3
inst✝³ : AddMonoid A
inst✝² : HasShift C A
s : A → D ⥤ D
i : (a : A) → F ⋙ s a ≅ shiftFunctor C a ⋙ F
inst✝¹ : ((whiskeringLeft C D D).obj F).Full
inst✝ : ((whiskeringLeft C D D).obj F).Faithful
a b : A
X : C
⊢ (shiftFunctorAdd D a b).inv.app (F.obj X) =
    (s b).map ((i a).hom.app X) ≫
      (i b).hom.app ((shiftFunctor C a).obj X) ≫ F.map ((shiftFunctorAdd C a b).inv.app X) ≫ (i (a + b)).inv.app X

Tactic:
letI := HasShift.induced F A s i

Result:
C : Type u_4
D : Type u_2
inst✝⁵ : Category.{u_5, u_4} C
inst✝⁴ : Category.{u_1, u_2} D
F : C ⥤ D
A : Type u_3
inst✝³ : AddMonoid A
inst✝² : HasShift C A
s : A → D ⥤ D
i : (a : A) → F ⋙ s a ≅ shiftFunctor C a ⋙ F
inst✝¹ : ((whiskeringLeft C D D).obj F).Full
inst✝ : ((whiskeringLeft C D D).obj F).Faithful
a b : A
X : C
this : HasShift D A := HasShift.induced F A s i
⊢ (shiftFunctorAdd D a b).inv.app (F.obj X) =
    (s b).map ((i a).hom.app X) ≫
      (i b).hom.app ((shiftFunctor C a).obj X) ≫ F.map ((shiftFunctorAdd C a b).inv.app X) ≫ (i (a + b)).inv.app X
-- Mathlib/MeasureTheory/Group/Action.lean
theorem measure_smul (c : G) (s : Set α) : μ (c • s) = μ s

Proof state:
G : Type u
α : Type w
m : MeasurableSpace α
inst✝² : Group G
inst✝¹ : MulAction G α
μ : Measure α
inst✝ : SMulInvariantMeasure G α μ
c : G
s : Set α
⊢ μ (c • s) = μ s

Tactic:
simpa only [preimage_smul_inv] using measure_preimage_smul μ c⁻¹ s

Result:
no goals
-- Mathlib/LinearAlgebra/RootSystem/Defs.lean
lemma coroot_root_eq_pairing : P.toLin.flip (P.coroot i) (P.root j) = P.pairing j i

Proof state:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
P : RootPairing ι R M N
i j : ι
⊢ (P.toLin.flip (P.coroot i)) (P.root j) = P.pairing j i

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Set/Image.lean
theorem range_coe {s : Set α} : range ((↑) : s → α) = s

Proof state:
α : Type u_1
s : Set α
⊢ range val = s

Tactic:
rw [← image_univ]

Result:
α : Type u_1
s : Set α
⊢ val '' univ = s

Proof state:
α : Type u_1
s : Set α
⊢ val '' univ = s

Tactic:
simp [-image_univ, coe_image]

Result:
no goals
-- Mathlib/Combinatorics/Quiver/Path.lean
lemma nil_ne_cons (p : Path a b) (e : b ⟶ a) : Path.nil ≠ p.cons e :=
  fun h => by injection h

Proof state:
V : Type u
inst✝ : Quiver V
a b : V
p : Path a b
e : b ⟶ a
h : nil = p.cons e
⊢ False

Tactic:
injection h

Result:
no goals
-- Mathlib/Algebra/Algebra/Spectrum.lean
lemma inv₀_mem_inv_iff {r : R} {a : Aˣ} :
    r⁻¹ ∈ spectrum R (↑a⁻¹ : A) ↔ r ∈ spectrum R (a : A)

Proof state:
R : Type u
A : Type v
inst✝² : Semifield R
inst✝¹ : Ring A
inst✝ : Algebra R A
r : R
a : Aˣ
⊢ r⁻¹ ∈ spectrum R ↑a⁻¹ ↔ r ∈ spectrum R ↑a

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Inverse.lean
lemma arccos_eq_of_eq_cos (hy₀ : 0 ≤ y) (hy₁ : y ≤ π) (hxy : x = cos y) : arccos x = y

Proof state:
x y : ℝ
hy₀ : 0 ≤ y
hy₁ : y ≤ π
hxy : x = cos y
⊢ arccos x = y

Tactic:
rw [hxy, arccos_cos hy₀ hy₁]

Result:
no goals
-- Mathlib/Algebra/Lie/Nilpotent.lean
theorem isNilpotent_quotient_iff :
    IsNilpotent L (M ⧸ N) ↔ ∃ k, lowerCentralSeries R L M k ≤ N

Proof state:
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
N : LieSubmodule R L M
inst✝ : LieModule R L M
k : ℕ
⊢ lowerCentralSeries R L (M ⧸ N) k = ⊥ ↔ lowerCentralSeries R L M k ≤ N

Tactic:
rw [← LieSubmodule.Quotient.map_mk'_eq_bot_le, map_lowerCentralSeries_eq k
  (LieSubmodule.Quotient.surjective_mk' N)]

Result:
no goals

Proof state:
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
N : LieSubmodule R L M
inst✝ : LieModule R L M
⊢ (∃ k, lowerCentralSeries R L (M ⧸ N) k = ⊥) ↔ ∃ k, lowerCentralSeries R L M k ≤ N

Tactic:
refine exists_congr fun k ↦ ?_

Result:
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
N : LieSubmodule R L M
inst✝ : LieModule R L M
k : ℕ
⊢ lowerCentralSeries R L (M ⧸ N) k = ⊥ ↔ lowerCentralSeries R L M k ≤ N

Proof state:
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
N : LieSubmodule R L M
inst✝ : LieModule R L M
⊢ IsNilpotent L (M ⧸ N) ↔ ∃ k, lowerCentralSeries R L M k ≤ N

Tactic:
rw [isNilpotent_iff R L]

Result:
R : Type u
L : Type v
M : Type w
inst✝⁶ : CommRing R
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra R L
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : LieRingModule L M
N : LieSubmodule R L M
inst✝ : LieModule R L M
⊢ (∃ k, lowerCentralSeries R L (M ⧸ N) k = ⊥) ↔ ∃ k, lowerCentralSeries R L M k ≤ N
-- Mathlib/Algebra/BigOperators/Group/Finset/Basic.lean
theorem prod_subtype_map_embedding {p : α → Prop} {s : Finset { x // p x }} {f : { x // p x } → β}
    {g : α → β} (h : ∀ x : { x // p x }, x ∈ s → g x = f x) :
    (∏ x ∈ s.map (Function.Embedding.subtype _), g x) = ∏ x ∈ s, f x

Proof state:
α : Type u_3
β : Type u_4
inst✝ : CommMonoid β
p : α → Prop
s : Finset { x // p x }
f : { x // p x } → β
g : α → β
h : ∀ x ∈ s, g ↑x = f x
⊢ ∏ x ∈ s, g ((Embedding.subtype fun x => p x) x) = ∏ x ∈ s, f x

Tactic:
exact Finset.prod_congr rfl h

Result:
no goals

Proof state:
α : Type u_3
β : Type u_4
inst✝ : CommMonoid β
p : α → Prop
s : Finset { x // p x }
f : { x // p x } → β
g : α → β
h : ∀ x ∈ s, g ↑x = f x
⊢ ∏ x ∈ map (Embedding.subtype fun x => p x) s, g x = ∏ x ∈ s, f x

Tactic:
rw [Finset.prod_map]

Result:
α : Type u_3
β : Type u_4
inst✝ : CommMonoid β
p : α → Prop
s : Finset { x // p x }
f : { x // p x } → β
g : α → β
h : ∀ x ∈ s, g ↑x = f x
⊢ ∏ x ∈ s, g ((Embedding.subtype fun x => p x) x) = ∏ x ∈ s, f x
-- Mathlib/Algebra/BigOperators/Finprod.lean
theorem finprod_curry (f : α × β → M) (hf : (mulSupport f).Finite) :
    ∏ᶠ ab, f ab = ∏ᶠ (a) (b), f (a, b)

Proof state:
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : CommMonoid M
f : α × β → M
hf : (mulSupport f).Finite
⊢ ∀ (a : α × β), ∏ᶠ (_ : a ∈ hf.toFinset), f a = f a

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : CommMonoid M
f : α × β → M
hf : (mulSupport f).Finite
h₁ : ∀ (a : α × β), ∏ᶠ (_ : a ∈ hf.toFinset), f a = f a
h₂ : ∏ᶠ (a : α × β), f a = ∏ᶠ (a : α × β) (_ : a ∈ hf.toFinset), f a
⊢ ∏ᶠ (ab : α × β), f ab = ∏ᶠ (a : α) (b : β), f (a, b)

Tactic:
simp_rw [h₂, finprod_mem_finset_product, h₁]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : CommMonoid M
f : α × β → M
hf : (mulSupport f).Finite
⊢ ∏ᶠ (ab : α × β), f ab = ∏ᶠ (a : α) (b : β), f (a, b)

Tactic:
have h₁ : ∀ a, ∏ᶠ _ : a ∈ hf.toFinset, f a = f a := by simp

Result:
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : CommMonoid M
f : α × β → M
hf : (mulSupport f).Finite
h₁ : ∀ (a : α × β), ∏ᶠ (_ : a ∈ hf.toFinset), f a = f a
⊢ ∏ᶠ (ab : α × β), f ab = ∏ᶠ (a : α) (b : β), f (a, b)

Proof state:
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : CommMonoid M
f : α × β → M
hf : (mulSupport f).Finite
h₁ : ∀ (a : α × β), ∏ᶠ (_ : a ∈ hf.toFinset), f a = f a
⊢ ∏ᶠ (ab : α × β), f ab = ∏ᶠ (a : α) (b : β), f (a, b)

Tactic:
have h₂ : ∏ᶠ a, f a = ∏ᶠ (a) (_ : a ∈ hf.toFinset), f a := by simp

Result:
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : CommMonoid M
f : α × β → M
hf : (mulSupport f).Finite
h₁ : ∀ (a : α × β), ∏ᶠ (_ : a ∈ hf.toFinset), f a = f a
h₂ : ∏ᶠ (a : α × β), f a = ∏ᶠ (a : α × β) (_ : a ∈ hf.toFinset), f a
⊢ ∏ᶠ (ab : α × β), f ab = ∏ᶠ (a : α) (b : β), f (a, b)

Proof state:
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : CommMonoid M
f : α × β → M
hf : (mulSupport f).Finite
h₁ : ∀ (a : α × β), ∏ᶠ (_ : a ∈ hf.toFinset), f a = f a
⊢ ∏ᶠ (a : α × β), f a = ∏ᶠ (a : α × β) (_ : a ∈ hf.toFinset), f a

Tactic:
simp

Result:
no goals
-- Mathlib/SetTheory/Lists.lean
theorem mem_cons {a y l} : a ∈ @cons α y l ↔ a ~ y ∨ a ∈ l

Proof state:
α : Type u_1
a y : Lists α
l : Lists' α true
⊢ a ∈ cons y l ↔ a ~ y ∨ a ∈ l

Tactic:
simp [mem_def, or_and_right, exists_or]

Result:
no goals
-- Mathlib/Algebra/QuaternionBasis.lean
theorem i_mul_k : q.i * q.k = c₁ • q.j + c₂ • q.k

Proof state:
R : Type u_1
A : Type u_2
inst✝² : CommRing R
inst✝¹ : Ring A
inst✝ : Algebra R A
c₁ c₂ c₃ : R
q : Basis A c₁ c₂ c₃
⊢ q.i * q.k = c₁ • q.j + c₂ • q.k

Tactic:
rw [← i_mul_j, ← mul_assoc, i_mul_i, add_mul, smul_mul_assoc, one_mul, smul_mul_assoc]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Attach.lean
theorem back?_attachWith {P : α → Prop} {xs : Array α}
    {H : ∀ (a : α), a ∈ xs → P a} :
    (xs.attachWith P H).back? = xs.back?.pbind (fun a h => some ⟨a, H _ (mem_of_back? h)⟩)

Proof state:
α : Type u_1
P : α → Prop
xs : Array α
H : ∀ (a : α), a ∈ xs → P a
⊢ (xs.attachWith P H).back? = xs.back?.pbind fun a h => some ⟨a, ⋯⟩

Tactic:
cases xs

Result:
case mk
α : Type u_1
P : α → Prop
toList✝ : List α
H : ∀ (a : α), a ∈ { toList := toList✝ } → P a
⊢ ({ toList := toList✝ }.attachWith P H).back? = { toList := toList✝ }.back?.pbind fun a h => some ⟨a, ⋯⟩

Proof state:
case mk
α : Type u_1
P : α → Prop
toList✝ : List α
H : ∀ (a : α), a ∈ { toList := toList✝ } → P a
⊢ ({ toList := toList✝ }.attachWith P H).back? = { toList := toList✝ }.back?.pbind fun a h => some ⟨a, ⋯⟩

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Find.lean
theorem find?_mkVector_eq_some_iff {n : Nat} {a b : α} {p : α → Bool} :
    (mkVector n a).find? p = some b ↔ n ≠ 0 ∧ p a ∧ a = b

Proof state:
α : Type
n : Nat
a b : α
p : α → Bool
⊢ Array.find? p (mkArray n a) = some b ↔ n ≠ 0 ∧ p a = true ∧ a = b

Tactic:
simp

Result:
no goals

Proof state:
α : Type
n : Nat
a b : α
p : α → Bool
⊢ find? p (mkVector n a) = some b ↔ n ≠ 0 ∧ p a = true ∧ a = b

Tactic:
rw [mkVector_eq_mk_mkArray, find?_mk]

Result:
α : Type
n : Nat
a b : α
p : α → Bool
⊢ Array.find? p (mkArray n a) = some b ↔ n ≠ 0 ∧ p a = true ∧ a = b
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Find.lean
theorem find?_singleton (a : α) (p : α → Bool) : [a].find? p = if p a then some a else none

Proof state:
α : Type u_1
a : α
p : α → Bool
⊢ (match p a with
    | true => some a
    | false => none) =
    if p a = true then some a else none

Tactic:
split <;> simp_all

Result:
no goals

Proof state:
α : Type u_1
a : α
p : α → Bool
⊢ find? p [a] = if p a = true then some a else none

Tactic:
simp only [find?]

Result:
α : Type u_1
a : α
p : α → Bool
⊢ (match p a with
    | true => some a
    | false => none) =
    if p a = true then some a else none
-- Mathlib/NumberTheory/LSeries/HurwitzZetaEven.lean
/-- Formula for `hurwitzZetaEven` as a Dirichlet series in the convergence range, with sum over `ℕ`
(version with absolute values) -/
lemma hasSum_nat_hurwitzZetaEven (a : ℝ) {s : ℂ} (hs : 1 < re s) :
    HasSum (fun n : ℕ ↦ (1 / (↑|n + a| : ℂ) ^ s + 1 / (↑|n + 1 - a| : ℂ) ^ s) / 2)
    (hurwitzZetaEven a s)

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

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

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

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

Tactic:
simp [← abs_neg (n + 1 - a), -neg_sub, neg_sub', add_div]

Result:
no goals
-- Mathlib/Algebra/Ring/NegOnePow.lean
lemma negOnePow_eq_iff (n₁ n₂ : ℤ) :
    n₁.negOnePow = n₂.negOnePow ↔ Even (n₁ - n₂)

Proof state:
case pos
n₁ n₂ : ℤ
h₂ : Even n₂
⊢ Even n₁ ↔ (Even n₁ ↔ Even n₂)

Tactic:
tauto

Result:
no goals

Proof state:
case pos
n₁ n₂ : ℤ
h₂ : Even n₂
⊢ n₁.negOnePow = n₂.negOnePow ↔ Even (n₁ - n₂)

Tactic:
rw [negOnePow_even _ h₂, Int.even_sub, negOnePow_eq_one_iff]

Result:
case pos
n₁ n₂ : ℤ
h₂ : Even n₂
⊢ Even n₁ ↔ (Even n₁ ↔ Even n₂)

Proof state:
case neg
n₁ n₂ : ℤ
h₂ : ¬Even n₂
⊢ n₁.negOnePow = n₂.negOnePow ↔ Even (n₁ - n₂)

Tactic:
rw [Int.not_even_iff_odd] at h₂

Result:
case neg
n₁ n₂ : ℤ
h₂ : Odd n₂
⊢ n₁.negOnePow = n₂.negOnePow ↔ Even (n₁ - n₂)

Proof state:
n₁ n₂ : ℤ
⊢ n₁.negOnePow = n₂.negOnePow ↔ Even (n₁ - n₂)

Tactic:
by_cases h₂ : Even n₂

Result:
case pos
n₁ n₂ : ℤ
h₂ : Even n₂
⊢ n₁.negOnePow = n₂.negOnePow ↔ Even (n₁ - n₂)

case neg
n₁ n₂ : ℤ
h₂ : ¬Even n₂
⊢ n₁.negOnePow = n₂.negOnePow ↔ Even (n₁ - n₂)

Proof state:
case neg
n₁ n₂ : ℤ
h₂ : Odd n₂
⊢ n₁.negOnePow = n₂.negOnePow ↔ Even (n₁ - n₂)

Tactic:
rw [negOnePow_odd _ h₂, Int.even_sub, negOnePow_eq_neg_one_iff,
  ← Int.not_odd_iff_even, ← Int.not_odd_iff_even]

Result:
case neg
n₁ n₂ : ℤ
h₂ : Odd n₂
⊢ Odd n₁ ↔ (¬Odd n₁ ↔ ¬Odd n₂)

Proof state:
case neg
n₁ n₂ : ℤ
h₂ : Odd n₂
⊢ Odd n₁ ↔ (¬Odd n₁ ↔ ¬Odd n₂)

Tactic:
tauto

Result:
no goals
-- Mathlib/Data/Nat/Factorization/Defs.lean
theorem Prime.factorization_pow {p k : ℕ} (hp : Prime p) : (p ^ k).factorization = single p k

Proof state:
p k : ℕ
hp : Prime p
⊢ (p ^ k).factorization = single p k

Tactic:
simp [hp]

Result:
no goals
-- Mathlib/Topology/UnitInterval.lean
theorem affineHomeomorph_image_I (a b : 𝕜) (h : 0 < a) :
    affineHomeomorph a b h.ne.symm '' Set.Icc 0 1 = Set.Icc b (a + b)

Proof state:
𝕜 : Type u_1
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : IsTopologicalRing 𝕜
a b : 𝕜
h : 0 < a
⊢ ⇑(affineHomeomorph a b ⋯) '' Icc 0 1 = Icc b (a + b)

Tactic:
simp [h]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/Images.lean
theorem e_isoExt_inv : F'.e ≫ (isoExt hF hF').inv = F.e

Proof state:
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : X ⟶ Y
F F' : MonoFactorisation f
hF : IsImage F
hF' : IsImage F'
⊢ F'.e ≫ (hF.isoExt hF').inv = F.e

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Nat/Choose/Sum.lean
theorem choose_middle_le_pow (n : ℕ) : (2 * n + 1).choose n ≤ 4 ^ n

Proof state:
n : ℕ
⊢ (2 * n + 1).choose n ≤ 4 ^ n

Tactic:
have t : (2 * n + 1).choose n ≤ ∑ i ∈ range (n + 1), (2 * n + 1).choose i :=
  single_le_sum (fun x _ ↦ by omega) (self_mem_range_succ n)

Result:
n : ℕ
t : (2 * n + 1).choose n ≤ ∑ i ∈ range (n + 1), (2 * n + 1).choose i
⊢ (2 * n + 1).choose n ≤ 4 ^ n

Proof state:
n : ℕ
t : (2 * n + 1).choose n ≤ ∑ i ∈ range (n + 1), (2 * n + 1).choose i
⊢ (2 * n + 1).choose n ≤ 4 ^ n

Tactic:
simpa [sum_range_choose_halfway n] using t

Result:
no goals

Proof state:
n x : ℕ
x✝ : x ∈ range (n + 1)
⊢ 0 ≤ (2 * n + 1).choose x

Tactic:
omega

Result:
no goals
-- Mathlib/Data/Nat/Factorization/Defs.lean
theorem factorization_eq_zero_of_remainder {p r : ℕ} (i : ℕ) (hr : ¬p ∣ r) :
    (p * i + r).factorization p = 0

Proof state:
p r i : ℕ
hr : ¬p ∣ r
⊢ (p * i + r).factorization p = 0

Tactic:
apply factorization_eq_zero_of_not_dvd

Result:
case h
p r i : ℕ
hr : ¬p ∣ r
⊢ ¬p ∣ p * i + r

Proof state:
case h
p r i : ℕ
hr : ¬p ∣ r
⊢ ¬p ∣ p * i + r

Tactic:
rwa [← Nat.dvd_add_iff_right (Dvd.intro i rfl)]

Result:
no goals
-- Mathlib/Algebra/Order/GroupWithZero/Unbundled.lean
/-- See `inv_le_iff_one_le_mul₀'` for a version with multiplication on the other side. -/
lemma inv_le_iff_one_le_mul₀ (ha : 0 < a) : a⁻¹ ≤ b ↔ 1 ≤ b * a

Proof state:
G₀ : Type u_2
inst✝⁴ : GroupWithZero G₀
inst✝³ : PartialOrder G₀
inst✝² : ZeroLEOneClass G₀
inst✝¹ : PosMulReflectLT G₀
a b : G₀
inst✝ : MulPosMono G₀
ha : 0 < a
⊢ a⁻¹ ≤ b ↔ 1 ≤ b * a

Tactic:
rw [← mul_inv_le_iff₀ ha, one_mul]

Result:
no goals
-- Mathlib/Algebra/Field/Basic.lean
theorem Commute.div_add_div (hbc : Commute b c) (hbd : Commute b d) (hb : b ≠ 0)
    (hd : d ≠ 0) : a / b + c / d = (a * d + b * c) / (b * d)

Proof state:
K : Type u_1
inst✝ : DivisionSemiring K
a b c d : K
hbc : Commute b c
hbd : Commute b d
hb : b ≠ 0
hd : d ≠ 0
⊢ a / b + c / d = (a * d + b * c) / (b * d)

Tactic:
rw [add_div, mul_div_mul_right _ b hd, hbc.eq, hbd.eq, mul_div_mul_right c d hb]

Result:
no goals
-- Mathlib/Analysis/Complex/CauchyIntegral.lean
theorem _root_.DifferentiableOn.analyticAt {s : Set ℂ} {f : ℂ → E} {z : ℂ}
    (hd : DifferentiableOn ℂ f s) (hz : s ∈ 𝓝 z) : AnalyticAt ℂ f z

Proof state:
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
s : Set ℂ
f : ℂ → E
z : ℂ
hd : DifferentiableOn ℂ f s
hz : s ∈ 𝓝 z
⊢ AnalyticAt ℂ f z

Tactic:
rcases nhds_basis_closedBall.mem_iff.1 hz with ⟨R, hR0, hRs⟩

Result:
case intro.intro
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
s : Set ℂ
f : ℂ → E
z : ℂ
hd : DifferentiableOn ℂ f s
hz : s ∈ 𝓝 z
R : ℝ
hR0 : 0 < R
hRs : closedBall z R ⊆ s
⊢ AnalyticAt ℂ f z

Proof state:
case intro.intro
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
s : Set ℂ
f : ℂ → E
z : ℂ
hd : DifferentiableOn ℂ f s
hz : s ∈ 𝓝 z
R : ℝ
hR0 : 0 < R
hRs : closedBall z R ⊆ s
⊢ AnalyticAt ℂ f z

Tactic:
lift R to ℝ≥0 using hR0.le

Result:
case intro.intro.intro
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
s : Set ℂ
f : ℂ → E
z : ℂ
hd : DifferentiableOn ℂ f s
hz : s ∈ 𝓝 z
R : ℝ≥0
hR0 : 0 < ↑R
hRs : closedBall z ↑R ⊆ s
⊢ AnalyticAt ℂ f z

Proof state:
case intro.intro.intro
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
s : Set ℂ
f : ℂ → E
z : ℂ
hd : DifferentiableOn ℂ f s
hz : s ∈ 𝓝 z
R : ℝ≥0
hR0 : 0 < ↑R
hRs : closedBall z ↑R ⊆ s
⊢ AnalyticAt ℂ f z

Tactic:
exact ((hd.mono hRs).hasFPowerSeriesOnBall hR0).analyticAt

Result:
no goals
-- Mathlib/MeasureTheory/Constructions/Projective.lean
lemma measure_univ_eq (hP : IsProjectiveMeasureFamily P) (I J : Finset ι) :
    P I univ = P J univ

Proof state:
ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → MeasurableSpace (α i)
P : (J : Finset ι) → Measure ((j : { x // x ∈ J }) → α ↑j)
hP : IsProjectiveMeasureFamily P
I J : Finset ι
⊢ (P I) univ = (P J) univ

Tactic:
classical
rw [← hP.measure_univ_eq_of_subset I.subset_union_left,
  ← hP.measure_univ_eq_of_subset (I.subset_union_right (s₂ := J))]

Result:
no goals

Proof state:
ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → MeasurableSpace (α i)
P : (J : Finset ι) → Measure ((j : { x // x ∈ J }) → α ↑j)
hP : IsProjectiveMeasureFamily P
I J : Finset ι
⊢ (P I) univ = (P J) univ

Tactic:
rw [← hP.measure_univ_eq_of_subset I.subset_union_left,
  ← hP.measure_univ_eq_of_subset (I.subset_union_right (s₂ := J))]

Result:
no goals
-- Mathlib/Analysis/Normed/Group/Bounded.lean
@[to_additive (attr := simp) tendsto_norm_atTop_iff_cobounded]
lemma tendsto_norm_atTop_iff_cobounded' {f : α → E} {l : Filter α} :
    Tendsto (‖f ·‖) l atTop ↔ Tendsto f l (cobounded E)

Proof state:
α : Type u_1
E : Type u_2
inst✝ : SeminormedGroup E
f : α → E
l : Filter α
⊢ Tendsto (fun x => ‖f x‖) l atTop ↔ Tendsto (norm ∘ f) l atTop

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
E : Type u_2
inst✝ : SeminormedGroup E
f : α → E
l : Filter α
⊢ Tendsto (fun x => ‖f x‖) l atTop ↔ Tendsto f l (cobounded E)

Tactic:
rw [← comap_norm_atTop', tendsto_comap_iff]

Result:
α : Type u_1
E : Type u_2
inst✝ : SeminormedGroup E
f : α → E
l : Filter α
⊢ Tendsto (fun x => ‖f x‖) l atTop ↔ Tendsto (norm ∘ f) l atTop
-- Mathlib/Data/Real/Sqrt.lean
theorem sq_lt : x ^ 2 < y ↔ -√y < x ∧ x < √y

Proof state:
x y : ℝ
⊢ x ^ 2 < y ↔ -√y < x ∧ x < √y

Tactic:
rw [← abs_lt, ← sq_abs, lt_sqrt (abs_nonneg _)]

Result:
no goals