harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/CategoryTheory/Limits/Preserves/Shapes/AbelianImages.lean
theorem PreservesImage.factorThruImage_iso_inv :
    Abelian.factorThruImage (F.map f) ≫ (PreservesImage.iso F f).inv =
      F.map (Abelian.factorThruImage f)

Proof state:
C : Type u₁
inst✝¹⁰ : Category.{v₁, u₁} C
inst✝⁹ : HasZeroMorphisms C
inst✝⁸ : HasKernels C
inst✝⁷ : HasCokernels C
D : Type u₂
inst✝⁶ : Category.{v₂, u₂} D
inst✝⁵ : HasZeroMorphisms D
inst✝⁴ : HasKernels D
inst✝³ : HasCokernels D
F : C ⥤ D
inst✝² : F.PreservesZeroMorphisms
inst✝¹ : PreservesLimitsOfShape WalkingParallelPair F
inst✝ : PreservesColimitsOfShape WalkingParallelPair F
X Y : C
f : X ⟶ Y
⊢ Abelian.factorThruImage (F.map f) ≫ (iso F f).inv = F.map (Abelian.factorThruImage f)

Tactic:
simp [Iso.comp_inv_eq]

Result:
no goals
-- Mathlib/NumberTheory/Harmonic/ZetaAsymp.lean
lemma term_sum_of_lt (N : ℕ) {s : ℝ} (hs : 1 < s) :
    term_sum s N = 1 / (s - 1) * (1 - 1 / (N + 1) ^ (s - 1))
    - 1 / s * ((∑ n ∈ Finset.range N, 1 / (n + 1 : ℝ) ^ s) - N / (N + 1) ^ s)

Proof state:
N : ℕ
s : ℝ
hs : 1 < s
⊢ term_sum s N =
    1 / (s - 1) * (1 - 1 / (↑N + 1) ^ (s - 1)) - 1 / s * (∑ n ∈ Finset.range N, 1 / (↑n + 1) ^ s - ↑N / (↑N + 1) ^ s)

Tactic:
simp only [term_sum]

Result:
N : ℕ
s : ℝ
hs : 1 < s
⊢ ∑ n ∈ Finset.range N, term (n + 1) s =
    1 / (s - 1) * (1 - 1 / (↑N + 1) ^ (s - 1)) - 1 / s * (∑ n ∈ Finset.range N, 1 / (↑n + 1) ^ s - ↑N / (↑N + 1) ^ s)
-- Mathlib/Algebra/Polynomial/Roots.lean
theorem rootSet_zero (S) [CommRing S] [IsDomain S] [Algebra T S] : (0 : T[X]).rootSet S = ∅

Proof state:
T : Type w
inst✝³ : CommRing T
S : Type u_1
inst✝² : CommRing S
inst✝¹ : IsDomain S
inst✝ : Algebra T S
⊢ rootSet 0 S = ∅

Tactic:
rw [← C_0, rootSet_C]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/Kernels.lean
lemma CokernelCofork.IsColimit.isIso_π {X Y : C} {f : X ⟶ Y} (c : CokernelCofork f)
    (hc : IsColimit c) (hf : f = 0) : IsIso c.π

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
c : CokernelCofork f
hc : IsColimit c
hf : f = 0
e : c.pt ≅ Y := hc.coconePointUniqueUpToIso (ofId f hf)
eq : Cofork.π c ≫ e.hom = 𝟙 Y
⊢ IsIso (𝟙 Y)

Tactic:
infer_instance

Result:
no goals

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
c : CokernelCofork f
hc : IsColimit c
hf : f = 0
⊢ IsIso (Cofork.π c)

Tactic:
let e : c.pt ≅ Y := IsColimit.coconePointUniqueUpToIso hc
  (CokernelCofork.IsColimit.ofId (f : X ⟶ Y) hf)

Result:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
c : CokernelCofork f
hc : IsColimit c
hf : f = 0
e : c.pt ≅ Y := hc.coconePointUniqueUpToIso (ofId f hf)
⊢ IsIso (Cofork.π c)

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
c : CokernelCofork f
hc : IsColimit c
hf : f = 0
e : c.pt ≅ Y := hc.coconePointUniqueUpToIso (ofId f hf)
eq : Cofork.π c ≫ e.hom = 𝟙 Y
this : IsIso (Cofork.π c ≫ e.hom)
⊢ IsIso (Cofork.π c)

Tactic:
exact IsIso.of_isIso_comp_right c.π e.hom

Result:
no goals

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
c : CokernelCofork f
hc : IsColimit c
hf : f = 0
e : c.pt ≅ Y := hc.coconePointUniqueUpToIso (ofId f hf)
eq : Cofork.π c ≫ e.hom = 𝟙 Y
⊢ IsIso (Cofork.π c)

Tactic:
haveI : IsIso (c.π ≫ e.hom) := by
  rw [eq]
  dsimp
  infer_instance

Result:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
c : CokernelCofork f
hc : IsColimit c
hf : f = 0
e : c.pt ≅ Y := hc.coconePointUniqueUpToIso (ofId f hf)
eq : Cofork.π c ≫ e.hom = 𝟙 Y
this : IsIso (Cofork.π c ≫ e.hom)
⊢ IsIso (Cofork.π c)

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
c : CokernelCofork f
hc : IsColimit c
hf : f = 0
e : c.pt ≅ Y := hc.coconePointUniqueUpToIso (ofId f hf)
⊢ IsIso (Cofork.π c)

Tactic:
have eq : c.π ≫ e.hom = 𝟙 Y := Cofork.IsColimit.π_desc hc

Result:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
c : CokernelCofork f
hc : IsColimit c
hf : f = 0
e : c.pt ≅ Y := hc.coconePointUniqueUpToIso (ofId f hf)
eq : Cofork.π c ≫ e.hom = 𝟙 Y
⊢ IsIso (Cofork.π c)

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
c : CokernelCofork f
hc : IsColimit c
hf : f = 0
e : c.pt ≅ Y := hc.coconePointUniqueUpToIso (ofId f hf)
eq : Cofork.π c ≫ e.hom = 𝟙 Y
⊢ IsIso (Cofork.π c ≫ e.hom)

Tactic:
rw [eq]

Result:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
c : CokernelCofork f
hc : IsColimit c
hf : f = 0
e : c.pt ≅ Y := hc.coconePointUniqueUpToIso (ofId f hf)
eq : Cofork.π c ≫ e.hom = 𝟙 Y
⊢ IsIso (𝟙 Y)
-- Mathlib/Geometry/RingedSpace/PresheafedSpace/Gluing.lean
theorem f_invApp_f_app (i j k : D.J) (U : Opens (D.V (i, j)).carrier) :
    (D.f_open i j).invApp _ U ≫ (D.f i k).c.app _ =
      (π₁ i, j, k).c.app (op U) ≫
        (π₂⁻¹ i, j, k) (unop _) ≫
          (D.V _).presheaf.map
            (eqToHom
              (by
                delta IsOpenImmersion.opensFunctor
                dsimp only [Functor.op, IsOpenMap.functor, Opens.map, unop_op]
                congr
                apply pullback_base))

Proof state:
C : Type u
inst✝ : Category.{v, u} C
D : GlueData C
i j k : D.J
U : Opens ↑↑(D.V (i, j))
this :
  ∀ (U : (Opens ↑↑(D.U i))ᵒᵖ),
    (pullback.fst (D.f i j) (D.f i k) ≫ D.f i j).c.app U =
      (pullback.snd (D.f i j) (D.f i k) ≫ D.f i k).c.app U ≫ (pullback (D.f i j) (D.f i k)).presheaf.map (eqToHom ⋯)
⊢ invApp (D.f i j) U ≫ (D.f i k).c.app (op ((opensFunctor (D.f i j)).obj U)) =
    (pullback.fst (D.f i j) (D.f i k)).c.app (op U) ≫
      invApp (pullback.snd (D.f i j) (D.f i k))
          (unop (op ((Opens.map (pullback.fst (D.f i j) (D.f i k)).base).toPrefunctor.1 (unop (op U))))) ≫
        (D.V (i, k)).presheaf.map (eqToHom ⋯)

Tactic:
dsimp only [comp_c_app] at this

Result:
C : Type u
inst✝ : Category.{v, u} C
D : GlueData C
i j k : D.J
U : Opens ↑↑(D.V (i, j))
this :
  ∀ (U : (Opens ↑↑(D.U i))ᵒᵖ),
    (D.f i j).c.app U ≫ (pullback.fst (D.f i j) (D.f i k)).c.app (op ((Opens.map (D.f i j).base).obj (unop U))) =
      ((D.f i k).c.app U ≫ (pullback.snd (D.f i j) (D.f i k)).c.app (op ((Opens.map (D.f i k).base).obj (unop U)))) ≫
        (pullback (D.f i j) (D.f i k)).presheaf.map (eqToHom ⋯)
⊢ invApp (D.f i j) U ≫ (D.f i k).c.app (op ((opensFunctor (D.f i j)).obj U)) =
    (pullback.fst (D.f i j) (D.f i k)).c.app (op U) ≫
      invApp (pullback.snd (D.f i j) (D.f i k))
          (unop (op ((Opens.map (pullback.fst (D.f i j) (D.f i k)).base).toPrefunctor.1 (unop (op U))))) ≫
        (D.V (i, k)).presheaf.map (eqToHom ⋯)
-- Mathlib/Data/Nat/Factorization/Basic.lean
theorem factorization_le_factorization_mul_left {a b : ℕ} (hb : b ≠ 0) :
    a.factorization ≤ (a * b).factorization

Proof state:
case inr
a b : ℕ
hb : b ≠ 0
ha : a ≠ 0
⊢ a.factorization ≤ (a * b).factorization

Tactic:
rw [factorization_le_iff_dvd ha <| mul_ne_zero ha hb]

Result:
case inr
a b : ℕ
hb : b ≠ 0
ha : a ≠ 0
⊢ a ∣ a * b

Proof state:
a b : ℕ
hb : b ≠ 0
⊢ a.factorization ≤ (a * b).factorization

Tactic:
rcases eq_or_ne a 0 with (rfl | ha)

Result:
case inl
b : ℕ
hb : b ≠ 0
⊢ factorization 0 ≤ (0 * b).factorization

case inr
a b : ℕ
hb : b ≠ 0
ha : a ≠ 0
⊢ a.factorization ≤ (a * b).factorization

Proof state:
case inr
a b : ℕ
hb : b ≠ 0
ha : a ≠ 0
⊢ a ∣ a * b

Tactic:
exact Dvd.intro b rfl

Result:
no goals

Proof state:
case inl
b : ℕ
hb : b ≠ 0
⊢ factorization 0 ≤ (0 * b).factorization

Tactic:
simp

Result:
no goals
-- Mathlib/NumberTheory/Harmonic/ZetaAsymp.lean
theorem _root_.tendsto_riemannZeta_sub_one_div :
    Tendsto (fun s : ℂ ↦ riemannZeta s - 1 / (s - 1)) (𝓝[≠] 1) (𝓝 γ)

Proof state:
f : ℂ → ℂ := fun s => riemannZeta s - 1 / (s - 1)
this : ∃ C, Tendsto f (𝓝[≠] 1) (𝓝 C)
⊢ Tendsto (fun s => riemannZeta s - 1 / (s - 1)) (𝓝[≠] 1) (𝓝 ↑γ)

Tactic:
obtain ⟨C, hC⟩ := this

Result:
case intro
f : ℂ → ℂ := fun s => riemannZeta s - 1 / (s - 1)
C : ℂ
hC : Tendsto f (𝓝[≠] 1) (𝓝 C)
⊢ Tendsto (fun s => riemannZeta s - 1 / (s - 1)) (𝓝[≠] 1) (𝓝 ↑γ)

Proof state:
case refine_1
f : ℂ → ℂ := fun s => riemannZeta s - 1 / (s - 1)
⊢ ∀ᶠ (z : ℂ) in 𝓝[≠] 1, DifferentiableAt ℂ f z

Tactic:
filter_upwards [self_mem_nhdsWithin] with s hs

Result:
case h
f : ℂ → ℂ := fun s => riemannZeta s - 1 / (s - 1)
s : ℂ
hs : s ∈ {1}ᶜ
⊢ DifferentiableAt ℂ f s
-- Mathlib/AlgebraicGeometry/Properties.lean
theorem isReduced_of_isOpenImmersion {X Y : Scheme} (f : X ⟶ Y) [H : IsOpenImmersion f]
    [IsReduced Y] : IsReduced X

Proof state:
case component_reduced
X Y : Scheme
f : X ⟶ Y
H : IsOpenImmersion f
inst✝ : IsReduced Y
U : X.Opens
this : U = f ⁻¹ᵁ f ''ᵁ U
⊢ _root_.IsReduced ↑Γ(X, f ⁻¹ᵁ f ''ᵁ U)

Tactic:
exact isReduced_of_injective (inv <| f.app (f ''ᵁ U)).hom
  (asIso <| f.app (f ''ᵁ U) : Γ(Y, f ''ᵁ U) ≅ _).symm.commRingCatIsoToRingEquiv.injective

Result:
no goals

Proof state:
case component_reduced
X Y : Scheme
f : X ⟶ Y
H : IsOpenImmersion f
inst✝ : IsReduced Y
⊢ autoParam (∀ (U : X.Opens), _root_.IsReduced ↑Γ(X, U)) _auto✝

Tactic:
intro U

Result:
case component_reduced
X Y : Scheme
f : X ⟶ Y
H : IsOpenImmersion f
inst✝ : IsReduced Y
U : X.Opens
⊢ _root_.IsReduced ↑Γ(X, U)

Proof state:
X Y : Scheme
f : X ⟶ Y
H : IsOpenImmersion f
inst✝ : IsReduced Y
⊢ IsReduced X

Tactic:
constructor

Result:
case component_reduced
X Y : Scheme
f : X ⟶ Y
H : IsOpenImmersion f
inst✝ : IsReduced Y
⊢ autoParam (∀ (U : X.Opens), _root_.IsReduced ↑Γ(X, U)) _auto✝

Proof state:
case component_reduced
X Y : Scheme
f : X ⟶ Y
H : IsOpenImmersion f
inst✝ : IsReduced Y
U : X.Opens
⊢ _root_.IsReduced ↑Γ(X, U)

Tactic:
have : U = f ⁻¹ᵁ f ''ᵁ U := by
  ext1; exact (Set.preimage_image_eq _ H.base_open.injective).symm

Result:
case component_reduced
X Y : Scheme
f : X ⟶ Y
H : IsOpenImmersion f
inst✝ : IsReduced Y
U : X.Opens
this : U = f ⁻¹ᵁ f ''ᵁ U
⊢ _root_.IsReduced ↑Γ(X, U)

Proof state:
case component_reduced
X Y : Scheme
f : X ⟶ Y
H : IsOpenImmersion f
inst✝ : IsReduced Y
U : X.Opens
this : U = f ⁻¹ᵁ f ''ᵁ U
⊢ _root_.IsReduced ↑Γ(X, U)

Tactic:
rw [this]

Result:
case component_reduced
X Y : Scheme
f : X ⟶ Y
H : IsOpenImmersion f
inst✝ : IsReduced Y
U : X.Opens
this : U = f ⁻¹ᵁ f ''ᵁ U
⊢ _root_.IsReduced ↑Γ(X, f ⁻¹ᵁ f ''ᵁ U)

Proof state:
case h
X Y : Scheme
f : X ⟶ Y
H : IsOpenImmersion f
inst✝ : IsReduced Y
U : X.Opens
⊢ ↑U = ↑(f ⁻¹ᵁ f ''ᵁ U)

Tactic:
exact (Set.preimage_image_eq _ H.base_open.injective).symm

Result:
no goals

Proof state:
X Y : Scheme
f : X ⟶ Y
H : IsOpenImmersion f
inst✝ : IsReduced Y
U : X.Opens
⊢ U = f ⁻¹ᵁ f ''ᵁ U

Tactic:
ext1

Result:
case h
X Y : Scheme
f : X ⟶ Y
H : IsOpenImmersion f
inst✝ : IsReduced Y
U : X.Opens
⊢ ↑U = ↑(f ⁻¹ᵁ f ''ᵁ U)
-- Mathlib/Analysis/Calculus/ContDiff/Bounds.lean
theorem norm_iteratedFDerivWithin_clm_apply_const {f : E → F →L[𝕜] G} {c : F} {s : Set E} {x : E}
    {N : WithTop ℕ∞} {n : ℕ} (hf : ContDiffWithinAt 𝕜 N f s x) (hs : UniqueDiffOn 𝕜 s)
    (hx : x ∈ s) (hn : n ≤ N) :
    ‖iteratedFDerivWithin 𝕜 n (fun y : E => (f y) c) s x‖ ≤
      ‖c‖ * ‖iteratedFDerivWithin 𝕜 n f s x‖

Proof state:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type uF
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type uG
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : E → F →L[𝕜] G
c : F
s : Set E
x : E
N : WithTop ℕ∞
n : ℕ
hf : ContDiffWithinAt 𝕜 N f s x
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
hn : ↑n ≤ N
g : (F →L[𝕜] G) →L[𝕜] G := (ContinuousLinearMap.apply 𝕜 G) c
h : ‖iteratedFDerivWithin 𝕜 n (⇑g ∘ f) s x‖ ≤ ‖g‖ * ‖iteratedFDerivWithin 𝕜 n f s x‖
⊢ ‖iteratedFDerivWithin 𝕜 n (fun y => (f y) c) s x‖ ≤ ‖c‖ * ‖iteratedFDerivWithin 𝕜 n f s x‖

Tactic:
refine h.trans (mul_le_mul_of_nonneg_right ?_ (norm_nonneg _))

Result:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type uF
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type uG
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : E → F →L[𝕜] G
c : F
s : Set E
x : E
N : WithTop ℕ∞
n : ℕ
hf : ContDiffWithinAt 𝕜 N f s x
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
hn : ↑n ≤ N
g : (F →L[𝕜] G) →L[𝕜] G := (ContinuousLinearMap.apply 𝕜 G) c
h : ‖iteratedFDerivWithin 𝕜 n (⇑g ∘ f) s x‖ ≤ ‖g‖ * ‖iteratedFDerivWithin 𝕜 n f s x‖
⊢ ‖g‖ ≤ ‖c‖
-- Mathlib/Topology/Algebra/Field.lean
theorem IsPreconnected.eq_or_eq_neg_of_sq_eq [Field 𝕜] [HasContinuousInv₀ 𝕜] [ContinuousMul 𝕜]
    (hS : IsPreconnected S) (hf : ContinuousOn f S) (hg : ContinuousOn g S)
    (hsq : EqOn (f ^ 2) (g ^ 2) S) (hg_ne : ∀ {x : α}, x ∈ S → g x ≠ 0) :
    EqOn f g S ∨ EqOn f (-g) S

Proof state:
α : Type u_2
𝕜 : Type u_3
f g : α → 𝕜
S : Set α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : T1Space 𝕜
inst✝² : Field 𝕜
inst✝¹ : HasContinuousInv₀ 𝕜
inst✝ : ContinuousMul 𝕜
hS : IsPreconnected S
hf : ContinuousOn f S
hg : ContinuousOn g S
hsq : EqOn (f ^ 2) (g ^ 2) S
hg_ne : ∀ {x : α}, x ∈ S → g x ≠ 0
x : α
hx : x ∈ S
⊢ ((f / g) ^ 2) x = 1 x

Tactic:
simpa [div_eq_one_iff_eq (pow_ne_zero _ (hg_ne hx)), div_pow] using hsq hx

Result:
no goals

Proof state:
α : Type u_2
𝕜 : Type u_3
f g : α → 𝕜
S : Set α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : T1Space 𝕜
inst✝² : Field 𝕜
inst✝¹ : HasContinuousInv₀ 𝕜
inst✝ : ContinuousMul 𝕜
hS : IsPreconnected S
hf : ContinuousOn f S
hg : ContinuousOn g S
hsq✝ : EqOn (f ^ 2) (g ^ 2) S
hg_ne : ∀ {x : α}, x ∈ S → g x ≠ 0
hsq : EqOn ((f / g) ^ 2) 1 S
⊢ EqOn f g S ∨ EqOn f (-g) S

Tactic:
simpa (config := { contextual := true }) [EqOn, div_eq_iff (hg_ne _)]
  using hS.eq_one_or_eq_neg_one_of_sq_eq (hf.div hg fun z => hg_ne) hsq

Result:
no goals

Proof state:
α : Type u_2
𝕜 : Type u_3
f g : α → 𝕜
S : Set α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : T1Space 𝕜
inst✝² : Field 𝕜
inst✝¹ : HasContinuousInv₀ 𝕜
inst✝ : ContinuousMul 𝕜
hS : IsPreconnected S
hf : ContinuousOn f S
hg : ContinuousOn g S
hsq : EqOn (f ^ 2) (g ^ 2) S
hg_ne : ∀ {x : α}, x ∈ S → g x ≠ 0
⊢ EqOn f g S ∨ EqOn f (-g) S

Tactic:
have hsq : EqOn ((f / g) ^ 2) 1 S := fun x hx => by
  simpa [div_eq_one_iff_eq (pow_ne_zero _ (hg_ne hx)), div_pow] using hsq hx

Result:
α : Type u_2
𝕜 : Type u_3
f g : α → 𝕜
S : Set α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace 𝕜
inst✝³ : T1Space 𝕜
inst✝² : Field 𝕜
inst✝¹ : HasContinuousInv₀ 𝕜
inst✝ : ContinuousMul 𝕜
hS : IsPreconnected S
hf : ContinuousOn f S
hg : ContinuousOn g S
hsq✝ : EqOn (f ^ 2) (g ^ 2) S
hg_ne : ∀ {x : α}, x ∈ S → g x ≠ 0
hsq : EqOn ((f / g) ^ 2) 1 S
⊢ EqOn f g S ∨ EqOn f (-g) S
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Zip.lean
theorem map_snd_zip (l₁ : Vector α n) (l₂ : Vector β n) :
    map Prod.snd (zip l₁ l₂) = l₂

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

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

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

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

Tactic:
simp [Array.map_snd_zip, h]

Result:
no goals

Proof state:
case mk
α : Type u_1
β : Type u_2
l₁ : Array α
l₂ : Vector β l₁.size
⊢ map Prod.snd ({ toArray := l₁, size_toArray := ⋯ }.zip l₂) = 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
⊢ map Prod.snd ({ toArray := l₁, size_toArray := ⋯ }.zip { toArray := l₂, size_toArray := h }) =
    { toArray := l₂, size_toArray := h }
-- Mathlib/Algebra/Homology/HomotopyCategory/ShiftSequence.lean
lemma shiftShortComplexFunctorIso_add'_hom_app
    (n m mn : ℤ) (hmn : m + n = mn) (a a' a'' : ℤ) (ha' : n + a = a') (ha'' : m + a' = a'')
    (K : CochainComplex C ℤ) :
    (shiftShortComplexFunctorIso C mn a a'' (by rw [← ha'', ← ha', ← add_assoc, hmn])).hom.app K =
      (shortComplexFunctor C (ComplexShape.up ℤ) a).map
        ((CategoryTheory.shiftFunctorAdd' (CochainComplex C ℤ) m n mn hmn).hom.app K) ≫
        (shiftShortComplexFunctorIso C n a a' ha').hom.app (K⟦m⟧) ≫
        (shiftShortComplexFunctorIso C m a' a'' ha'' ).hom.app K

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
n m mn : ℤ
hmn : m + n = mn
a a' a'' : ℤ
ha' : n + a = a'
ha'' : m + a' = a''
K : CochainComplex C ℤ
⊢ (shiftShortComplexFunctorIso C mn a a'' ⋯).hom.app K =
    (shortComplexFunctor C (up ℤ) a).map ((CategoryTheory.shiftFunctorAdd' (CochainComplex C ℤ) m n mn hmn).hom.app K) ≫
      (shiftShortComplexFunctorIso C n a a' ha').hom.app ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) m).obj K) ≫
        (shiftShortComplexFunctorIso C m a' a'' ha'').hom.app K

Tactic:
ext <;> dsimp <;> simp only [← hmn, Int.negOnePow_add, shiftFunctorAdd'_hom_app_f',
  XIsoOfEq_shift, Linear.comp_units_smul, Linear.units_smul_comp,
  XIsoOfEq_hom_comp_XIsoOfEq_hom, smul_smul]

Result:
no goals

Proof state:
C : Type u_1
inst✝¹ : Category.{?u.45022, u_1} C
inst✝ : Preadditive C
n m mn : ℤ
hmn : m + n = mn
a a' a'' : ℤ
ha' : n + a = a'
ha'' : m + a' = a''
K : CochainComplex C ℤ
⊢ mn + a = a''

Tactic:
rw [← ha'', ← ha', ← add_assoc, hmn]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Typeclasses.lean
theorem exists_isFiniteMeasure_absolutelyContinuous [SFinite μ] :
    ∃ ν : Measure α, IsFiniteMeasure ν ∧ μ ≪ ν ∧ ν ≪ μ

Proof state:
case intro.intro
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : SFinite μ
c : ℕ → ℝ≥0
hc₀ : ∀ (i : ℕ), 0 < c i
hc : ∑' (i : ℕ), (sfiniteSeq μ i) univ * ↑(c i) < ⊤
⊢ ∃ ν, IsFiniteMeasure ν ∧ μ ≪ ν ∧ ν ≪ μ

Tactic:
have {s : Set α} : sum (fun n ↦ c n • sfiniteSeq μ n) s = 0 ↔ μ s = 0 := by
  conv_rhs => rw [← sum_sfiniteSeq μ, sum_apply_of_countable]
  simp [(hc₀ _).ne']

Result:
case intro.intro
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : SFinite μ
c : ℕ → ℝ≥0
hc₀ : ∀ (i : ℕ), 0 < c i
hc : ∑' (i : ℕ), (sfiniteSeq μ i) univ * ↑(c i) < ⊤
this : ∀ {s : Set α}, (sum fun n => c n • sfiniteSeq μ n) s = 0 ↔ μ s = 0
⊢ ∃ ν, IsFiniteMeasure ν ∧ μ ≪ ν ∧ ν ≪ μ

Proof state:
case intro.intro
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : SFinite μ
c : ℕ → ℝ≥0
hc₀ : ∀ (i : ℕ), 0 < c i
hc : ∑' (i : ℕ), (sfiniteSeq μ i) univ * ↑(c i) < ⊤
this : ∀ {s : Set α}, (sum fun n => c n • sfiniteSeq μ n) s = 0 ↔ μ s = 0
⊢ ∃ ν, IsFiniteMeasure ν ∧ μ ≪ ν ∧ ν ≪ μ

Tactic:
refine ⟨.sum fun n ↦ c n • sfiniteSeq μ n, ⟨?_⟩, fun _ ↦ this.1, fun _ ↦ this.2⟩

Result:
case intro.intro
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : SFinite μ
c : ℕ → ℝ≥0
hc₀ : ∀ (i : ℕ), 0 < c i
hc : ∑' (i : ℕ), (sfiniteSeq μ i) univ * ↑(c i) < ⊤
this : ∀ {s : Set α}, (sum fun n => c n • sfiniteSeq μ n) s = 0 ↔ μ s = 0
⊢ (sum fun n => c n • sfiniteSeq μ n) univ < ⊤

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : SFinite μ
c : ℕ → ℝ≥0
hc₀ : ∀ (i : ℕ), 0 < c i
hc : ∑' (i : ℕ), (sfiniteSeq μ i) univ * ↑(c i) < ⊤
s : Set α
⊢ (sum fun n => c n • sfiniteSeq μ n) s = 0 ↔ μ s = 0

Tactic:
conv_rhs => rw [← sum_sfiniteSeq μ, sum_apply_of_countable]

Result:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : SFinite μ
c : ℕ → ℝ≥0
hc₀ : ∀ (i : ℕ), 0 < c i
hc : ∑' (i : ℕ), (sfiniteSeq μ i) univ * ↑(c i) < ⊤
s : Set α
⊢ (sum fun n => c n • sfiniteSeq μ n) s = 0 ↔ ∑' (i : ℕ), (sfiniteSeq μ i) s = 0

Proof state:
case intro.intro
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : SFinite μ
c : ℕ → ℝ≥0
hc₀ : ∀ (i : ℕ), 0 < c i
hc : ∑' (i : ℕ), (sfiniteSeq μ i) univ * ↑(c i) < ⊤
this : ∀ {s : Set α}, (sum fun n => c n • sfiniteSeq μ n) s = 0 ↔ μ s = 0
⊢ (sum fun n => c n • sfiniteSeq μ n) univ < ⊤

Tactic:
simpa [mul_comm] using hc

Result:
no goals

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : SFinite μ
c : ℕ → ℝ≥0
hc₀ : ∀ (i : ℕ), 0 < c i
hc : ∑' (i : ℕ), (sfiniteSeq μ i) univ * ↑(c i) < ⊤
s : Set α
⊢ (sum fun n => c n • sfiniteSeq μ n) s = 0 ↔ ∑' (i : ℕ), (sfiniteSeq μ i) s = 0

Tactic:
simp [(hc₀ _).ne']

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Ord.lean
theorem isLE_of_eq_eq {o : Ordering} : o = .eq → o.isLE

Proof state:
⊢ eq.isLE = true

Tactic:
rfl

Result:
no goals

Proof state:
o : Ordering
⊢ o = eq → o.isLE = true

Tactic:
rintro rfl

Result:
⊢ eq.isLE = true
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Fin/Lemmas.lean
theorem fin_two_eq_of_eq_zero_iff : ∀ {a b : Fin 2}, (a = 0 ↔ b = 0) → a = b

Proof state:
⊢ ∀ {a b : Fin 2}, (a = 0 ↔ b = 0) → a = b

Tactic:
simp only [forall_fin_two]

Result:
⊢ ((True → True) ∧ ((True ↔ 1 = 0) → 0 = 1)) ∧ ((1 = 0 ↔ True) → 1 = 0) ∧ (True → True)

Proof state:
⊢ ((True → True) ∧ ((True ↔ 1 = 0) → 0 = 1)) ∧ ((1 = 0 ↔ True) → 1 = 0) ∧ (True → True)

Tactic:
decide

Result:
no goals
-- Mathlib/GroupTheory/FreeGroup/Basic.lean
theorem inv_of_red_of_ne {x1 b1 x2 b2} (H1 : (x1, b1) ≠ (x2, b2))
    (H2 : Red ((x1, b1) :: L₁) ((x2, b2) :: L₂)) : Red L₁ ((x1, not b1) :: (x2, b2) :: L₂)

Proof state:
case intro.cons.intro.intro.intro
α : Type u
L₁ L₂ : List (α × Bool)
x1 : α
b1 : Bool
x2 : α
b2 : Bool
H1 : (x1, b1) ≠ (x2, b2)
H2 : Red ((x1, b1) :: L₁) ((x2, b2) :: L₂)
this : Red ((x1, b1) :: L₁) ([(x2, b2)] ++ L₂)
p : α × Bool
L₃ L₄ : List (α × Bool)
eq : (x1, b1) :: L₁ = p :: L₃ ++ L₄
h₁ : Red (p :: L₃) [(x2, b2)]
h₂ : Red L₄ L₂
⊢ Red L₁ ((x1, !b1) :: (x2, b2) :: L₂)

Tactic:
cases eq

Result:
case intro.cons.intro.intro.intro.refl
α : Type u
L₂ : List (α × Bool)
x1 : α
b1 : Bool
x2 : α
b2 : Bool
H1 : (x1, b1) ≠ (x2, b2)
L₃ L₄ : List (α × Bool)
h₂ : Red L₄ L₂
h₁ : Red ((x1, b1) :: L₃) [(x2, b2)]
H2 : Red ((x1, b1) :: L₃.append L₄) ((x2, b2) :: L₂)
this : Red ((x1, b1) :: L₃.append L₄) ([(x2, b2)] ++ L₂)
⊢ Red (L₃.append L₄) ((x1, !b1) :: (x2, b2) :: L₂)
-- Mathlib/NumberTheory/EulerProduct/DirichletLSeries.lean
/-- When `s.re > 1`, the map `n ↦ χ(n) * n^(-s)` is norm-summable. -/
lemma summable_dirichletSummand {N : ℕ} (χ : DirichletCharacter ℂ N) (hs : 1 < s.re) :
    Summable (fun n ↦ ‖dirichletSummandHom χ (ne_zero_of_one_lt_re hs) n‖)

Proof state:
s : ℂ
N : ℕ
χ : DirichletCharacter ℂ N
hs : 1 < s.re
⊢ Summable fun n => ‖(dirichletSummandHom χ ⋯) n‖

Tactic:
simp only [dirichletSummandHom, MonoidWithZeroHom.coe_mk, ZeroHom.coe_mk, norm_mul]

Result:
s : ℂ
N : ℕ
χ : DirichletCharacter ℂ N
hs : 1 < s.re
⊢ Summable fun n => ‖χ ↑n‖ * ‖↑n ^ (-s)‖

Proof state:
s : ℂ
N : ℕ
χ : DirichletCharacter ℂ N
hs : 1 < s.re
⊢ Summable fun n => ‖χ ↑n‖ * ‖↑n ^ (-s)‖

Tactic:
exact (summable_riemannZetaSummand hs).of_nonneg_of_le (fun _ ↦ by positivity)
  (fun n ↦ mul_le_of_le_one_left (norm_nonneg _) <| χ.norm_le_one n)

Result:
no goals

Proof state:
s : ℂ
N : ℕ
χ : DirichletCharacter ℂ N
hs : 1 < s.re
x✝ : ℕ
⊢ 0 ≤ ‖χ ↑x✝‖ * ‖↑x✝ ^ (-s)‖

Tactic:
positivity

Result:
no goals