harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/NumberTheory/LSeries/DirichletContinuation.lean
/--
The L-function of the (unique) Dirichlet character mod 1 is the Riemann zeta function.
(Compare `DirichletCharacter.LSeries_modOne_eq`.)
-/
@[simp] lemma LFunction_modOne_eq {χ : DirichletCharacter ℂ 1} :
    LFunction χ = riemannZeta

Proof state:
χ : DirichletCharacter ℂ 1
x✝ : ℂ
⊢ 0 = 1

Tactic:
rfl

Result:
no goals

Proof state:
χ : DirichletCharacter ℂ 1
⊢ LFunction χ = riemannZeta

Tactic:
ext

Result:
case h
χ : DirichletCharacter ℂ 1
x✝ : ℂ
⊢ LFunction χ x✝ = riemannZeta x✝

Proof state:
case h
χ : DirichletCharacter ℂ 1
x✝ : ℂ
⊢ LFunction χ x✝ = riemannZeta x✝

Tactic:
rw [LFunction, ZMod.LFunction_modOne_eq, (by rfl : (0 : ZMod 1) = 1), map_one, one_mul]

Result:
no goals
-- Mathlib/Algebra/GCDMonoid/Nat.lean
theorem Int.associated_iff_natAbs {a b : ℤ} : Associated a b ↔ a.natAbs = b.natAbs

Proof state:
a b : ℤ
⊢ Associated a.natAbs b.natAbs ↔ a.natAbs = b.natAbs

Tactic:
exact associated_iff_eq

Result:
no goals

Proof state:
a b : ℤ
⊢ Associated a b ↔ a.natAbs = b.natAbs

Tactic:
rw [← dvd_dvd_iff_associated, ← Int.natAbs_dvd_natAbs, ← Int.natAbs_dvd_natAbs,
  dvd_dvd_iff_associated]

Result:
a b : ℤ
⊢ Associated a.natAbs b.natAbs ↔ a.natAbs = b.natAbs
-- Mathlib/Data/Matroid/IndepAxioms.lean
theorem ofFinset_indep [DecidableEq α] (E : Set α) Indep indep_empty indep_subset indep_aug
    subset_ground {I : Finset α} : (IndepMatroid.ofFinset
      E Indep indep_empty indep_subset indep_aug subset_ground).Indep I ↔ Indep I

Proof state:
α : Type u_1
inst✝ : DecidableEq α
E : Set α
Indep : Finset α → Prop
indep_empty : Indep ∅
indep_subset : ∀ ⦃I J : Finset α⦄, Indep J → I ⊆ J → Indep I
indep_aug : ∀ ⦃I J : Finset α⦄, Indep I → Indep J → I.card < J.card → ∃ e ∈ J, e ∉ I ∧ Indep (insert e I)
subset_ground : ∀ ⦃I : Finset α⦄, Indep I → ↑I ⊆ E
I : Finset α
⊢ (IndepMatroid.ofFinset E Indep indep_empty indep_subset indep_aug subset_ground).Indep ↑I ↔ Indep I

Tactic:
simp only [IndepMatroid.ofFinset, ofFinitaryCardAugment_indep, Finset.coe_subset]

Result:
α : Type u_1
inst✝ : DecidableEq α
E : Set α
Indep : Finset α → Prop
indep_empty : Indep ∅
indep_subset : ∀ ⦃I J : Finset α⦄, Indep J → I ⊆ J → Indep I
indep_aug : ∀ ⦃I J : Finset α⦄, Indep I → Indep J → I.card < J.card → ∃ e ∈ J, e ∉ I ∧ Indep (insert e I)
subset_ground : ∀ ⦃I : Finset α⦄, Indep I → ↑I ⊆ E
I : Finset α
⊢ (∀ J ⊆ I, Indep J) ↔ Indep I

Proof state:
α : Type u_1
inst✝ : DecidableEq α
E : Set α
Indep : Finset α → Prop
indep_empty : Indep ∅
indep_subset : ∀ ⦃I J : Finset α⦄, Indep J → I ⊆ J → Indep I
indep_aug : ∀ ⦃I J : Finset α⦄, Indep I → Indep J → I.card < J.card → ∃ e ∈ J, e ∉ I ∧ Indep (insert e I)
subset_ground : ∀ ⦃I : Finset α⦄, Indep I → ↑I ⊆ E
I : Finset α
⊢ (∀ J ⊆ I, Indep J) ↔ Indep I

Tactic:
exact ⟨fun h ↦ h _ Subset.rfl, fun h J hJI ↦ indep_subset h hJI⟩

Result:
no goals
-- Mathlib/RingTheory/Spectrum/Maximal/Localization.lean
theorem mapPiLocalization_naturality :
    (mapPiLocalization f hf).comp (toPiLocalization R) =
      (toPiLocalization S).comp f

Proof state:
case a.h
R : Type u_1
S : Type u_2
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
hf : Function.Bijective ⇑f
r : R
I : MaximalSpectrum S
⊢ IsLocalization.mk' (Localization.AtPrime I.asIdeal) (f r) ⟨1, ⋯⟩ =
    IsLocalization.mk' (Localization.AtPrime I.asIdeal) (f r) 1

Tactic:
rfl

Result:
no goals

Proof state:
case a.h
R : Type u_1
S : Type u_2
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
hf : Function.Bijective ⇑f
r : R
I : MaximalSpectrum S
⊢ (Localization.localRingHom (Ideal.comap f I.asIdeal) I.asIdeal f ⋯)
      ((algebraMap R (Localization.AtPrime (Ideal.comap f I.asIdeal))) r) =
    (algebraMap S (Localization.AtPrime I.asIdeal)) (f r)

Tactic:
simp_rw [← IsLocalization.mk'_one (M := (I.1.comap f).primeCompl), Localization.localRingHom_mk',
  ← IsLocalization.mk'_one (M := I.1.primeCompl), Submonoid.coe_one, map_one f]

Result:
case a.h
R : Type u_1
S : Type u_2
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
hf : Function.Bijective ⇑f
r : R
I : MaximalSpectrum S
⊢ IsLocalization.mk' (Localization.AtPrime I.asIdeal) (f r) ⟨1, ⋯⟩ =
    IsLocalization.mk' (Localization.AtPrime I.asIdeal) (f r) 1

Proof state:
R : Type u_1
S : Type u_2
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
hf : Function.Bijective ⇑f
⊢ (mapPiLocalization f hf).comp (toPiLocalization R) = (toPiLocalization S).comp f

Tactic:
ext r I

Result:
case a.h
R : Type u_1
S : Type u_2
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
hf : Function.Bijective ⇑f
r : R
I : MaximalSpectrum S
⊢ ((mapPiLocalization f hf).comp (toPiLocalization R)) r I = ((toPiLocalization S).comp f) r I

Proof state:
case a.h
R : Type u_1
S : Type u_2
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
hf : Function.Bijective ⇑f
r : R
I : MaximalSpectrum S
⊢ ((mapPiLocalization f hf).comp (toPiLocalization R)) r I = ((toPiLocalization S).comp f) r I

Tactic:
show Localization.localRingHom _ _ _ rfl (algebraMap _ _ r) = algebraMap _ _ (f r)

Result:
case a.h
R : Type u_1
S : Type u_2
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
hf : Function.Bijective ⇑f
r : R
I : MaximalSpectrum S
⊢ (Localization.localRingHom (Ideal.comap f I.asIdeal) I.asIdeal f ⋯)
      ((algebraMap R (Localization.AtPrime (Ideal.comap f I.asIdeal))) r) =
    (algebraMap S (Localization.AtPrime I.asIdeal)) (f r)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lex.lean
theorem not_nil_lex_iff : ¬Lex r [] l ↔ l = []

Proof state:
case mp
α✝ : Type u_1
r : α✝ → α✝ → Prop
l : List α✝
⊢ ¬Lex r [] l → l = []

Tactic:
rintro h

Result:
case mp
α✝ : Type u_1
r : α✝ → α✝ → Prop
l : List α✝
h : ¬Lex r [] l
⊢ l = []

Proof state:
α✝ : Type u_1
r : α✝ → α✝ → Prop
l : List α✝
⊢ ¬Lex r [] l ↔ l = []

Tactic:
constructor

Result:
case mp
α✝ : Type u_1
r : α✝ → α✝ → Prop
l : List α✝
⊢ ¬Lex r [] l → l = []

case mpr
α✝ : Type u_1
r : α✝ → α✝ → Prop
l : List α✝
⊢ l = [] → ¬Lex r [] l

Proof state:
α✝ : Type u_1
r : α✝ → α✝ → Prop
l : List α✝
h✝ : ¬Lex r [] l
h : ¬Lex r [] []
⊢ [] = []

Tactic:
rfl

Result:
no goals

Proof state:
case mpr
α✝ : Type u_1
r : α✝ → α✝ → Prop
l : List α✝
⊢ l = [] → ¬Lex r [] l

Tactic:
rintro rfl

Result:
case mpr
α✝ : Type u_1
r : α✝ → α✝ → Prop
⊢ ¬Lex r [] []

Proof state:
case mpr
α✝ : Type u_1
r : α✝ → α✝ → Prop
⊢ ¬Lex r [] []

Tactic:
exact not_lex_nil

Result:
no goals

Proof state:
α✝ : Type u_1
r : α✝ → α✝ → Prop
l : List α✝
h✝ : ¬Lex r [] l
a : α✝
tail✝ : List α✝
h : ¬Lex r [] (a :: tail✝)
⊢ a :: tail✝ = []

Tactic:
exact False.elim (h Lex.nil)

Result:
no goals

Proof state:
case mp
α✝ : Type u_1
r : α✝ → α✝ → Prop
l : List α✝
h : ¬Lex r [] l
⊢ l = []

Tactic:
match l, h with
| [], h => rfl
| a :: _, h => exact False.elim (h Lex.nil)

Result:
no goals
-- Mathlib/Geometry/Euclidean/Angle/Oriented/Affine.lean
theorem oangle_ne_zero_and_ne_pi_iff_affineIndependent {p₁ p₂ p₃ : P} :
    ∡ p₁ p₂ p₃ ≠ 0 ∧ ∡ p₁ p₂ p₃ ≠ π ↔ AffineIndependent ℝ ![p₁, p₂, p₃]

Proof state:
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
⊢ ∡ p₁ p₂ p₃ ≠ 0 ∧ ∡ p₁ p₂ p₃ ≠ ↑π ↔ AffineIndependent ℝ ![p₁, p₂, p₃]

Tactic:
rw [oangle, o.oangle_ne_zero_and_ne_pi_iff_linearIndependent,
  affineIndependent_iff_linearIndependent_vsub ℝ _ (1 : Fin 3), ←
  linearIndependent_equiv (finSuccAboveEquiv (1 : Fin 3))]

Result:
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
⊢ LinearIndependent ℝ ![p₁ -ᵥ p₂, p₃ -ᵥ p₂] ↔
    LinearIndependent ℝ ((fun i => ![p₁, p₂, p₃] ↑i -ᵥ ![p₁, p₂, p₃] 1) ∘ ⇑(finSuccAboveEquiv 1))

Proof state:
case h.e'_2.h.e'_4.h
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
i : Fin 2
⊢ ((fun i => ![p₁, p₂, p₃] ↑i -ᵥ ![p₁, p₂, p₃] 1) ∘ ⇑(finSuccAboveEquiv 1)) i = ![p₁ -ᵥ p₂, p₃ -ᵥ p₂] i

Tactic:
fin_cases i <;> rfl

Result:
no goals

Proof state:
case h.e'_2.h.e'_4
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
⊢ (fun i => ![p₁, p₂, p₃] ↑i -ᵥ ![p₁, p₂, p₃] 1) ∘ ⇑(finSuccAboveEquiv 1) = ![p₁ -ᵥ p₂, p₃ -ᵥ p₂]

Tactic:
ext i

Result:
case h.e'_2.h.e'_4.h
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
i : Fin 2
⊢ ((fun i => ![p₁, p₂, p₃] ↑i -ᵥ ![p₁, p₂, p₃] 1) ∘ ⇑(finSuccAboveEquiv 1)) i = ![p₁ -ᵥ p₂, p₃ -ᵥ p₂] i

Proof state:
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
⊢ LinearIndependent ℝ ![p₁ -ᵥ p₂, p₃ -ᵥ p₂] ↔
    LinearIndependent ℝ ((fun i => ![p₁, p₂, p₃] ↑i -ᵥ ![p₁, p₂, p₃] 1) ∘ ⇑(finSuccAboveEquiv 1))

Tactic:
convert Iff.rfl

Result:
case h.e'_2.h.e'_4
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
⊢ (fun i => ![p₁, p₂, p₃] ↑i -ᵥ ![p₁, p₂, p₃] 1) ∘ ⇑(finSuccAboveEquiv 1) = ![p₁ -ᵥ p₂, p₃ -ᵥ p₂]
-- Mathlib/CategoryTheory/Triangulated/Pretriangulated.lean
lemma exists_iso_binaryBiproduct_of_distTriang (T : Triangle C) (hT : T ∈ distTriang C)
    (zero : T.mor₃ = 0) :
    ∃ (e : T.obj₂ ≅ T.obj₁ ⊞ T.obj₃), T.mor₁ ≫ e.hom = biprod.inl ∧
      T.mor₂ = e.hom ≫ biprod.snd

Proof state:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), (shiftFunctor C n).Additive
hC : Pretriangulated C
T : Triangle C
hT : T ∈ distinguishedTriangles
zero : T.mor₃ = 0
this : Epi T.mor₂
⊢ ∃ e, T.mor₁ ≫ e.hom = biprod.inl ∧ T.mor₂ = e.hom ≫ biprod.snd

Tactic:
have := isSplitEpi_of_epi T.mor₂

Result:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), (shiftFunctor C n).Additive
hC : Pretriangulated C
T : Triangle C
hT : T ∈ distinguishedTriangles
zero : T.mor₃ = 0
this✝ : Epi T.mor₂
this : IsSplitEpi T.mor₂
⊢ ∃ e, T.mor₁ ≫ e.hom = biprod.inl ∧ T.mor₂ = e.hom ≫ biprod.snd

Proof state:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), (shiftFunctor C n).Additive
hC : Pretriangulated C
T : Triangle C
hT : T ∈ distinguishedTriangles
zero : T.mor₃ = 0
this✝ : Epi T.mor₂
this : IsSplitEpi T.mor₂
⊢ ∃ e, T.mor₁ ≫ e.hom = biprod.inl ∧ T.mor₂ = e.hom ≫ biprod.snd

Tactic:
obtain ⟨fst, hfst⟩ := T.coyoneda_exact₂ hT (𝟙 T.obj₂ - T.mor₂ ≫ section_ T.mor₂) (by simp)

Result:
case intro
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), (shiftFunctor C n).Additive
hC : Pretriangulated C
T : Triangle C
hT : T ∈ distinguishedTriangles
zero : T.mor₃ = 0
this✝ : Epi T.mor₂
this : IsSplitEpi T.mor₂
fst : T.obj₂ ⟶ T.obj₁
hfst : 𝟙 T.obj₂ - T.mor₂ ≫ section_ T.mor₂ = fst ≫ T.mor₁
⊢ ∃ e, T.mor₁ ≫ e.hom = biprod.inl ∧ T.mor₂ = e.hom ≫ biprod.snd

Proof state:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), (shiftFunctor C n).Additive
hC : Pretriangulated C
T : Triangle C
hT : T ∈ distinguishedTriangles
zero : T.mor₃ = 0
this✝ : Epi T.mor₂
this : IsSplitEpi T.mor₂
fst : T.obj₂ ⟶ T.obj₁
hfst : 𝟙 T.obj₂ - T.mor₂ ≫ section_ T.mor₂ = fst ≫ T.mor₁
⊢ section_ T.mor₂ ≫ T.mor₂ = 𝟙 T.obj₃

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Set/Function.lean
theorem image_restrictPreimage :
    t.restrictPreimage f '' (Subtype.val ⁻¹' s) = Subtype.val ⁻¹' (f '' s)

Proof state:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
⊢ t.restrictPreimage f '' (Subtype.val ⁻¹' s) = Subtype.val ⁻¹' (f '' s)

Tactic:
delta Set.restrictPreimage

Result:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
⊢ MapsTo.restrict f (f ⁻¹' t) t ⋯ '' (Subtype.val ⁻¹' s) = Subtype.val ⁻¹' (f '' s)

Proof state:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
⊢ MapsTo.restrict f (f ⁻¹' t) t ⋯ '' (Subtype.val ⁻¹' s) = Subtype.val ⁻¹' (f '' s)

Tactic:
rw [← (Subtype.coe_injective).image_injective.eq_iff, ← image_comp, MapsTo.restrict_commutes,
  image_comp, Subtype.image_preimage_coe, Subtype.image_preimage_coe, image_preimage_inter]

Result:
no goals
-- Mathlib/Topology/Category/CompHausLike/EffectiveEpi.lean
theorem precoherent [HasExplicitPullbacks P] [HasExplicitFiniteCoproducts.{0} P]
    (hs : ∀ ⦃X Y : CompHausLike P⦄ (f : X ⟶ Y), EffectiveEpi f → Function.Surjective f) :
    Precoherent (CompHausLike P)

Proof state:
P : TopCat → Prop
inst✝¹ : HasExplicitPullbacks P
inst✝ : HasExplicitFiniteCoproducts P
hs : ∀ ⦃X Y : CompHausLike P⦄ (f : X ⟶ Y), EffectiveEpi f → Function.Surjective ⇑(ConcreteCategory.hom f)
this : Preregular (CompHausLike P)
⊢ Precoherent (CompHausLike P)

Tactic:
infer_instance

Result:
no goals

Proof state:
P : TopCat → Prop
inst✝¹ : HasExplicitPullbacks P
inst✝ : HasExplicitFiniteCoproducts P
hs : ∀ ⦃X Y : CompHausLike P⦄ (f : X ⟶ Y), EffectiveEpi f → Function.Surjective ⇑(ConcreteCategory.hom f)
⊢ Precoherent (CompHausLike P)

Tactic:
have : Preregular (CompHausLike P) := preregular hs

Result:
P : TopCat → Prop
inst✝¹ : HasExplicitPullbacks P
inst✝ : HasExplicitFiniteCoproducts P
hs : ∀ ⦃X Y : CompHausLike P⦄ (f : X ⟶ Y), EffectiveEpi f → Function.Surjective ⇑(ConcreteCategory.hom f)
this : Preregular (CompHausLike P)
⊢ Precoherent (CompHausLike P)
-- Mathlib/NumberTheory/LSeries/ZMod.lean
/--
The `LFunction` of the function `x ↦ e (j * x)`, where `e : ZMod N → ℂ` is the standard additive
character, agrees with `expZeta (j / N)` on `1 < re s`. Private since it is a stepping-stone to
the more general result `LFunction_stdAddChar_eq_expZeta` below.
-/
private lemma LFunction_stdAddChar_eq_expZeta_of_one_lt_re (j : ZMod N) {s : ℂ} (hs : 1 < s.re) :
    LFunction (fun k ↦ 𝕖 (j * k)) s = expZeta (ZMod.toAddCircle j) s

Proof state:
N : ℕ
inst✝ : NeZero N
j : ZMod N
s : ℂ
hs : 1 < s.re
⊢ ∑' (n : ℕ), LSeries.term (fun x => 𝕖 (j * ↑x)) s n = ∑' (b : ℕ), cexp (2 * ↑π * I * ↑(↑j.val / ↑N) * ↑b) / ↑b ^ s

Tactic:
congr 1 with n

Result:
case e_f.h
N : ℕ
inst✝ : NeZero N
j : ZMod N
s : ℂ
hs : 1 < s.re
n : ℕ
⊢ LSeries.term (fun x => 𝕖 (j * ↑x)) s n = cexp (2 * ↑π * I * ↑(↑j.val / ↑N) * ↑n) / ↑n ^ s

Proof state:
case e_f.h
N : ℕ
inst✝ : NeZero N
j : ZMod N
s : ℂ
hs : 1 < s.re
n : ℕ
⊢ LSeries.term (fun x => 𝕖 (j * ↑x)) s n = cexp (2 * ↑π * I * ↑(↑j.val / ↑N) * ↑n) / ↑n ^ s

Tactic:
rw [LSeries.term_of_ne_zero' (ne_zero_of_one_lt_re hs), ofReal_div, ofReal_natCast,
  ofReal_natCast, mul_assoc, div_mul_eq_mul_div, stdAddChar_apply]

Result:
case e_f.h
N : ℕ
inst✝ : NeZero N
j : ZMod N
s : ℂ
hs : 1 < s.re
n : ℕ
⊢ ↑(toCircle (j * ↑n)) / ↑n ^ s = cexp (2 * ↑π * I * (↑j.val * ↑n / ↑N)) / ↑n ^ s

Proof state:
case e_f.h
N : ℕ
inst✝ : NeZero N
j : ZMod N
s : ℂ
hs : 1 < s.re
n : ℕ
this : ↑(toCircle ↑(↑j.val * ↑n)) = cexp (2 * ↑π * I * ↑(↑j.val * ↑n) / ↑N)
⊢ ↑(toCircle (j * ↑n)) / ↑n ^ s = cexp (2 * ↑π * I * (↑j.val * ↑n / ↑N)) / ↑n ^ s

Tactic:
conv_rhs at this => rw [Int.cast_mul, Int.cast_natCast, Int.cast_natCast, mul_div_assoc]

Result:
case e_f.h
N : ℕ
inst✝ : NeZero N
j : ZMod N
s : ℂ
hs : 1 < s.re
n : ℕ
this : ↑(toCircle ↑(↑j.val * ↑n)) = cexp (2 * ↑π * I * (↑j.val * ↑n / ↑N))
⊢ ↑(toCircle (j * ↑n)) / ↑n ^ s = cexp (2 * ↑π * I * (↑j.val * ↑n / ↑N)) / ↑n ^ s

Proof state:
case e_f.h
N : ℕ
inst✝ : NeZero N
j : ZMod N
s : ℂ
hs : 1 < s.re
n : ℕ
this : ↑(toCircle ↑(↑j.val * ↑n)) = cexp (2 * ↑π * I * (↑j.val * ↑n / ↑N))
⊢ ↑(toCircle (j * ↑n)) / ↑n ^ s = cexp (2 * ↑π * I * (↑j.val * ↑n / ↑N)) / ↑n ^ s

Tactic:
rw [← this, Int.cast_mul, Int.cast_natCast, Int.cast_natCast, natCast_zmod_val]

Result:
no goals

Proof state:
N : ℕ
inst✝ : NeZero N
j : ZMod N
s : ℂ
hs : 1 < s.re
⊢ LFunction (fun k => 𝕖 (j * k)) s = expZeta (toAddCircle j) s

Tactic:
rw [toAddCircle_apply, ← (hasSum_expZeta_of_one_lt_re (j.val / N) hs).tsum_eq,
  LFunction_eq_LSeries _ hs, LSeries]

Result:
N : ℕ
inst✝ : NeZero N
j : ZMod N
s : ℂ
hs : 1 < s.re
⊢ ∑' (n : ℕ), LSeries.term (fun x => 𝕖 (j * ↑x)) s n = ∑' (b : ℕ), cexp (2 * ↑π * I * ↑(↑j.val / ↑N) * ↑b) / ↑b ^ s

Proof state:
case e_f.h
N : ℕ
inst✝ : NeZero N
j : ZMod N
s : ℂ
hs : 1 < s.re
n : ℕ
⊢ ↑(toCircle (j * ↑n)) / ↑n ^ s = cexp (2 * ↑π * I * (↑j.val * ↑n / ↑N)) / ↑n ^ s

Tactic:
have := ZMod.toCircle_intCast (N := N) (j.val * n)

Result:
case e_f.h
N : ℕ
inst✝ : NeZero N
j : ZMod N
s : ℂ
hs : 1 < s.re
n : ℕ
this : ↑(toCircle ↑(↑j.val * ↑n)) = cexp (2 * ↑π * I * ↑(↑j.val * ↑n) / ↑N)
⊢ ↑(toCircle (j * ↑n)) / ↑n ^ s = cexp (2 * ↑π * I * (↑j.val * ↑n / ↑N)) / ↑n ^ s
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem getKey!_unitOfList_of_contains_eq_false [EquivBEq α] [LawfulHashable α]
    [Inhabited α] {l : List α} {k : α}
    (contains_eq_false : l.contains k = false) :
    getKey! (unitOfList l) k = default

Proof state:
α : Type u
inst✝⁴ : BEq α
inst✝³ : Hashable α
inst✝² : EquivBEq α
inst✝¹ : LawfulHashable α
inst✝ : Inhabited α
l : List α
k : α
contains_eq_false : l.contains k = false
⊢ (unitOfList l).getKey! k = default

Tactic:
simp_to_raw using Raw₀.Const.getKey!_insertManyIfNewUnit_empty_list_of_contains_eq_false

Result:
no goals
-- Mathlib/Topology/UnitInterval.lean
@[simp]
lemma symm_eq_zero {i : I} : σ i = 0 ↔ i = 1

Proof state:
i : ↑I
⊢ σ i = 0 ↔ i = 1

Tactic:
rw [← symm_one, symm_inj]

Result:
no goals
-- Mathlib/Analysis/Normed/Group/Hom.lean
theorem norm_id {V : Type*} [NormedAddCommGroup V] [Nontrivial V] : ‖id V‖ = 1

Proof state:
V : Type u_5
inst✝¹ : NormedAddCommGroup V
inst✝ : Nontrivial V
⊢ ‖id V‖ = 1

Tactic:
refine norm_id_of_nontrivial_seminorm V ?_

Result:
V : Type u_5
inst✝¹ : NormedAddCommGroup V
inst✝ : Nontrivial V
⊢ ∃ x, ‖x‖ ≠ 0

Proof state:
case intro
V : Type u_5
inst✝¹ : NormedAddCommGroup V
inst✝ : Nontrivial V
x : V
hx : x ≠ 0
⊢ ∃ x, ‖x‖ ≠ 0

Tactic:
exact ⟨x, ne_of_gt (norm_pos_iff.2 hx)⟩

Result:
no goals

Proof state:
V : Type u_5
inst✝¹ : NormedAddCommGroup V
inst✝ : Nontrivial V
⊢ ∃ x, ‖x‖ ≠ 0

Tactic:
obtain ⟨x, hx⟩ := exists_ne (0 : V)

Result:
case intro
V : Type u_5
inst✝¹ : NormedAddCommGroup V
inst✝ : Nontrivial V
x : V
hx : x ≠ 0
⊢ ∃ x, ‖x‖ ≠ 0
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Zip.lean
theorem unzip_zip_right {l₁ : Vector α n} {l₂ : Vector β n} :
    (unzip (zip l₁ l₂)).2 = l₂

Proof state:
α : Type u_1
n : Nat
β : Type u_2
l₁ : Vector α n
l₂ : Vector β n
⊢ (l₁.zip l₂).unzip.snd = l₂

Tactic:
rcases l₁ with ⟨l₁, rfl⟩

Result:
case mk
α : Type u_1
β : Type u_2
l₁ : Array α
l₂ : Vector β l₁.size
⊢ ({ toArray := l₁, size_toArray := ⋯ }.zip l₂).unzip.snd = l₂

Proof state:
case mk
α : Type u_1
β : Type u_2
l₁ : Array α
l₂ : Vector β l₁.size
⊢ ({ toArray := l₁, size_toArray := ⋯ }.zip l₂).unzip.snd = l₂

Tactic:
rcases l₂ with ⟨l₂, h⟩

Result:
case mk.mk
α : Type u_1
β : Type u_2
l₁ : Array α
l₂ : Array β
h : l₂.size = l₁.size
⊢ ({ toArray := l₁, size_toArray := ⋯ }.zip { toArray := l₂, size_toArray := h }).unzip.snd =
    { toArray := l₂, size_toArray := h }

Proof state:
case mk.mk
α : Type u_1
β : Type u_2
l₁ : Array α
l₂ : Array β
h : l₂.size = l₁.size
⊢ ({ toArray := l₁, size_toArray := ⋯ }.zip { toArray := l₂, size_toArray := h }).unzip.snd =
    { toArray := l₂, size_toArray := h }

Tactic:
simp [Array.unzip_zip_right, h, Array.map_snd_zip]

Result:
no goals
-- Mathlib/Algebra/Order/Monoid/Unbundled/WithTop.lean
protected lemma add_lt_add_right [LT α] [AddRightStrictMono α] (hz : z ≠ ⊤) :
    x < y → x + z < y + z

Proof state:
α : Type u
inst✝² : Add α
x y z : WithTop α
inst✝¹ : LT α
inst✝ : AddRightStrictMono α
hz : z ≠ ⊤
⊢ x < y → x + z < y + z

Tactic:
lift z to α using hz

Result:
case intro
α : Type u
inst✝² : Add α
x y : WithTop α
inst✝¹ : LT α
inst✝ : AddRightStrictMono α
z : α
⊢ x < y → x + ↑z < y + ↑z

Proof state:
case intro
α : Type u
inst✝² : Add α
x y : WithTop α
inst✝¹ : LT α
inst✝ : AddRightStrictMono α
z : α
⊢ x < y → x + ↑z < y + ↑z

Tactic:
cases x <;> cases y <;> simp [← coe_add]

Result:
case intro.coe.coe
α : Type u
inst✝² : Add α
inst✝¹ : LT α
inst✝ : AddRightStrictMono α
z a✝¹ a✝ : α
⊢ a✝¹ < a✝ → a✝¹ + z < a✝ + z
-- Mathlib/Algebra/Ring/Parity.lean
@[deprecated not_odd_iff_even (since := "2024-08-21")]
lemma even_iff_not_odd : Even n ↔ ¬Odd n

Proof state:
n : ℕ
⊢ Even n ↔ ¬Odd n

Tactic:
rw [not_odd_iff, even_iff]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/MeasureSpace.lean
theorem sum_measure_preimage_singleton (s : Finset β) {f : α → β}
    (hf : ∀ y ∈ s, MeasurableSet (f ⁻¹' {y})) : (∑ b ∈ s, μ (f ⁻¹' {b})) = μ (f ⁻¹' ↑s)

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
s : Finset β
f : α → β
hf : ∀ y ∈ s, MeasurableSet (f ⁻¹' {y})
⊢ ∑ b ∈ s, μ (f ⁻¹' {b}) = μ (f ⁻¹' ↑s)

Tactic:
simp only [← measure_biUnion_finset (pairwiseDisjoint_fiber f s) hf,
  Finset.set_biUnion_preimage_singleton]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Smeval.lean
theorem smeval_neg_nat (S : Type*) [NonAssocRing S] [Pow S ℕ] [NatPowAssoc S] (q : ℕ[X])
    (n : ℕ) : q.smeval (-(n : S)) = q.smeval (-n : ℤ)

Proof state:
S : Type u_3
inst✝² : NonAssocRing S
inst✝¹ : Pow S ℕ
inst✝ : NatPowAssoc S
q : ℕ[X]
n : ℕ
⊢ q.smeval (-↑n) = ↑(q.smeval (-↑n))

Tactic:
rw [smeval_eq_sum, smeval_eq_sum]

Result:
S : Type u_3
inst✝² : NonAssocRing S
inst✝¹ : Pow S ℕ
inst✝ : NatPowAssoc S
q : ℕ[X]
n : ℕ
⊢ q.sum (smul_pow (-↑n)) = ↑(q.sum (smul_pow (-↑n)))

Proof state:
S : Type u_3
inst✝² : NonAssocRing S
inst✝¹ : Pow S ℕ
inst✝ : NatPowAssoc S
q : ℕ[X]
n : ℕ
⊢ ∑ x ∈ q.support, q.coeff x • (-↑n) ^ x = ∑ x ∈ q.support, ↑(q.coeff x • (-↑n) ^ x)

Tactic:
refine Finset.sum_congr rfl ?_

Result:
S : Type u_3
inst✝² : NonAssocRing S
inst✝¹ : Pow S ℕ
inst✝ : NatPowAssoc S
q : ℕ[X]
n : ℕ
⊢ ∀ x ∈ q.support, q.coeff x • (-↑n) ^ x = ↑(q.coeff x • (-↑n) ^ x)

Proof state:
S : Type u_3
inst✝² : NonAssocRing S
inst✝¹ : Pow S ℕ
inst✝ : NatPowAssoc S
q : ℕ[X]
n : ℕ
⊢ ∀ x ∈ q.support, q.coeff x • (-↑n) ^ x = ↑(q.coeff x • (-↑n) ^ x)

Tactic:
intro k _

Result:
S : Type u_3
inst✝² : NonAssocRing S
inst✝¹ : Pow S ℕ
inst✝ : NatPowAssoc S
q : ℕ[X]
n k : ℕ
a✝ : k ∈ q.support
⊢ q.coeff k • (-↑n) ^ k = ↑(q.coeff k • (-↑n) ^ k)

Proof state:
S : Type u_3
inst✝² : NonAssocRing S
inst✝¹ : Pow S ℕ
inst✝ : NatPowAssoc S
q : ℕ[X]
n k : ℕ
a✝ : k ∈ q.support
⊢ q.coeff k • (-↑n) ^ k = ↑(q.coeff k • (-↑n) ^ k)

Tactic:
rw [show -(n : S) = (-n : ℤ) by simp only [Int.cast_neg, Int.cast_natCast], nsmul_eq_mul,
  ← AddGroupWithOne.intCast_ofNat, ← Int.cast_npow, ← Int.cast_mul, ← nsmul_eq_mul]

Result:
no goals

Proof state:
S : Type u_3
inst✝² : NonAssocRing S
inst✝¹ : Pow S ℕ
inst✝ : NatPowAssoc S
q : ℕ[X]
n k : ℕ
a✝ : k ∈ q.support
⊢ -↑n = ↑(-↑n)

Tactic:
simp only [Int.cast_neg, Int.cast_natCast]

Result:
no goals

Proof state:
S : Type u_3
inst✝² : NonAssocRing S
inst✝¹ : Pow S ℕ
inst✝ : NatPowAssoc S
q : ℕ[X]
n : ℕ
⊢ q.sum (smul_pow (-↑n)) = ↑(q.sum (smul_pow (-↑n)))

Tactic:
simp only [Polynomial.smul_pow, sum_def, Int.cast_sum, Int.cast_mul, Int.cast_npow]

Result:
S : Type u_3
inst✝² : NonAssocRing S
inst✝¹ : Pow S ℕ
inst✝ : NatPowAssoc S
q : ℕ[X]
n : ℕ
⊢ ∑ x ∈ q.support, q.coeff x • (-↑n) ^ x = ∑ x ∈ q.support, ↑(q.coeff x • (-↑n) ^ x)