harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/Homology/ShortComplex/HomologicalComplex.lean
lemma exactAt_iff_isZero_homology [K.HasHomology i] :
    K.ExactAt i ↔ IsZero (K.homology i)

Proof state:
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : HasZeroMorphisms C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex C c
i : ι
inst✝ : K.HasHomology i
⊢ K.ExactAt i ↔ IsZero (K.homology i)

Tactic:
dsimp [homology]

Result:
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : HasZeroMorphisms C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex C c
i : ι
inst✝ : K.HasHomology i
⊢ K.ExactAt i ↔ IsZero (K.sc i).homology

Proof state:
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : HasZeroMorphisms C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex C c
i : ι
inst✝ : K.HasHomology i
⊢ K.ExactAt i ↔ IsZero (K.sc i).homology

Tactic:
rw [exactAt_iff, ShortComplex.exact_iff_isZero_homology]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem getD_insert_self [LawfulBEq α] (h : m.WF) {a : α} {fallback b : β a} :
    (m.insert a b).getD a fallback = b

Proof state:
α : Type u
β : α → Type v
m : Raw α β
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulBEq α
h : m.WF
a : α
fallback b : β a
⊢ (m.insert a b).getD a fallback = b

Tactic:
simp_to_raw using Raw₀.getD_insert_self

Result:
no goals
-- Mathlib/CategoryTheory/Grothendieck.lean
theorem comp_fiber {X Y Z : Grothendieck F} (f : X ⟶ Y) (g : Y ⟶ Z) :
    Hom.fiber (f ≫ g) =
      eqToHom (by simp) ≫ (F.map g.base).map f.fiber ≫ g.fiber :=
  rfl

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₁
inst✝ : Category.{v₁, u₁} D
F : C ⥤ Cat
X Y Z : Grothendieck F
f : X ⟶ Y
g : Y ⟶ Z
⊢ (F.map (f ≫ g).base).obj X.fiber = (F.map g.base).obj ((F.map f.base).obj X.fiber)

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/Complex/Basic.lean
theorem tendsto_normSq_cocompact_atTop : Tendsto normSq (cocompact ℂ) atTop

Proof state:
⊢ Tendsto (⇑normSq) (cocompact ℂ) atTop

Tactic:
simpa [norm_mul_self_eq_normSq]
  using tendsto_norm_cocompact_atTop.atTop_mul_atTop₀ (tendsto_norm_cocompact_atTop (E := ℂ))

Result:
no goals
-- Mathlib/Data/Finset/Defs.lean
theorem coe_ssubset {s₁ s₂ : Finset α} : (s₁ : Set α) ⊂ s₂ ↔ s₁ ⊂ s₂ :=
  show (s₁ : Set α) ⊂ s₂ ↔ s₁ ⊆ s₂ ∧ ¬s₂ ⊆ s₁ by simp only [Set.ssubset_def, Finset.coe_subset]

Proof state:
α : Type u_1
s₁ s₂ : Finset α
⊢ ↑s₁ ⊂ ↑s₂ ↔ s₁ ⊆ s₂ ∧ ¬s₂ ⊆ s₁

Tactic:
simp only [Set.ssubset_def, Finset.coe_subset]

Result:
no goals
-- Mathlib/Algebra/AddTorsor/Basic.lean
theorem injective_pointReflection_left_of_injective_two_nsmul {G P : Type*} [AddCommGroup G]
    [AddTorsor G P] (h : Injective (2 • · : G → G)) (y : P) :
    Injective fun x : P => pointReflection x y :=
  fun x₁ x₂ (hy : pointReflection x₁ y = pointReflection x₂ y) => by
  rwa [pointReflection_apply, pointReflection_apply, vadd_eq_vadd_iff_sub_eq_vsub,
    vsub_sub_vsub_cancel_right, ← neg_vsub_eq_vsub_rev, neg_eq_iff_add_eq_zero,
    ← two_nsmul, ← nsmul_zero 2, h.eq_iff, vsub_eq_zero_iff_eq] at hy

Proof state:
G : Type u_3
P : Type u_4
inst✝¹ : AddCommGroup G
inst✝ : AddTorsor G P
h : Injective fun x => 2 • x
y x₁ x₂ : P
hy : (pointReflection x₁) y = (pointReflection x₂) y
⊢ x₁ = x₂

Tactic:
rwa [pointReflection_apply, pointReflection_apply, vadd_eq_vadd_iff_sub_eq_vsub,
  vsub_sub_vsub_cancel_right, ← neg_vsub_eq_vsub_rev, neg_eq_iff_add_eq_zero,
  ← two_nsmul, ← nsmul_zero 2, h.eq_iff, vsub_eq_zero_iff_eq] at hy

Result:
no goals
-- Mathlib/Condensed/Discrete/Colimit.lean
@[simp]
lemma lanPresheafIso_hom (hF : IsColimit <| F.mapCocone S.asLimitCone.op) :
    (lanPresheafIso hF).hom = colimit.desc _ (Profinite.Extend.cocone _ _)

Proof state:
S : Profinite
F : Profiniteᵒᵖ ⥤ Type (u + 1)
hF : IsColimit (F.mapCocone S.asLimitCone.op)
⊢ ((colimit.isColimit (S.diagram.op ⋙ F)).coconePointUniqueUpToIso hF).hom =
    colimit.desc
      (Profinite.Extend.functorOp S.asLimitCone ⋙
        CostructuredArrow.proj toProfinite.op (Opposite.op S) ⋙ toProfinite.op ⋙ F)
      (Cocone.whisker (Profinite.Extend.functorOp S.asLimitCone) (Profinite.Extend.cocone F S))

Tactic:
rfl

Result:
no goals

Proof state:
S : Profinite
F : Profiniteᵒᵖ ⥤ Type (u + 1)
hF : IsColimit (F.mapCocone S.asLimitCone.op)
⊢ (lanPresheafIso hF).hom =
    colimit.desc (CostructuredArrow.proj toProfinite.op (Opposite.op S) ⋙ toProfinite.op ⋙ F)
      (Profinite.Extend.cocone F S)

Tactic:
simp [lanPresheafIso, Final.colimitIso]

Result:
S : Profinite
F : Profiniteᵒᵖ ⥤ Type (u + 1)
hF : IsColimit (F.mapCocone S.asLimitCone.op)
⊢ ((colimit.isColimit (S.diagram.op ⋙ F)).coconePointUniqueUpToIso hF).hom =
    colimit.desc
      (Profinite.Extend.functorOp S.asLimitCone ⋙
        CostructuredArrow.proj toProfinite.op (Opposite.op S) ⋙ toProfinite.op ⋙ F)
      (Cocone.whisker (Profinite.Extend.functorOp S.asLimitCone) (Profinite.Extend.cocone F S))
-- Mathlib/Order/Heyting/Basic.lean
theorem sdiff_sdiff_self : (a \ b) \ a = ⊥

Proof state:
α : Type u_2
inst✝ : GeneralizedCoheytingAlgebra α
a b : α
⊢ (a \ b) \ a = ⊥

Tactic:
rw [sdiff_sdiff_comm, sdiff_self, bot_sdiff]

Result:
no goals
-- Mathlib/Algebra/BigOperators/Group/List/Basic.lean
theorem prod_flatten {l : List (List M)} : l.flatten.prod = (l.map List.prod).prod

Proof state:
case cons
M : Type u_4
inst✝ : Monoid M
head : List M
tail : List (List M)
ih : tail.flatten.prod = (map prod tail).prod
⊢ (head :: tail).flatten.prod = (map prod (head :: tail)).prod

Tactic:
simp only [*, List.flatten, map, prod_append, prod_cons]

Result:
no goals

Proof state:
case nil
M : Type u_4
inst✝ : Monoid M
⊢ [].flatten.prod = (map prod []).prod

Tactic:
simp

Result:
no goals

Proof state:
M : Type u_4
inst✝ : Monoid M
l : List (List M)
⊢ l.flatten.prod = (map prod l).prod

Tactic:
induction l with
| nil => simp
| cons head tail ih => simp only [*, List.flatten, map, prod_append, prod_cons]

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian.lean
lemma baseChange_add {P Q : Fin 3 → F} (hP : (W'.baseChange F).toJacobian.Nonsingular P)
    (hQ : (W'.baseChange F).toJacobian.Nonsingular Q) :
    (W'.baseChange K).toJacobian.add (f ∘ P) (f ∘ Q) =
      f ∘ (W'.baseChange F).toJacobian.add P Q

Proof state:
F : Type u
inst✝¹⁰ : Field F
R : Type r
inst✝⁹ : CommRing R
W' : Jacobian R
S : Type s
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
inst✝⁶ : Algebra R F
inst✝⁵ : Algebra S F
inst✝⁴ : IsScalarTower R S F
K : Type v
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : Algebra S K
inst✝ : IsScalarTower R S K
f : F →ₐ[S] K
P Q : Fin 3 → F
hP : (baseChange W' F).toJacobian.Nonsingular P
hQ : (baseChange W' F).toJacobian.Nonsingular Q
⊢ (baseChange W' K).toJacobian.add (⇑f ∘ P) (⇑f ∘ Q) = ⇑f ∘ (baseChange W' F).toJacobian.add P Q

Tactic:
rw [← RingHom.coe_coe, ← WeierstrassCurve.Jacobian.map_add f hP hQ (K := K), map_baseChange]

Result:
no goals
-- Mathlib/CategoryTheory/Galois/Decomposition.lean
@[simp]
private lemma mkSelfProdFib_map_π (t : F.obj X) : F.map (Pi.π _ t) (mkSelfProdFib F X) = t

Proof state:
C : Type u₁
inst✝² : Category.{u₂, u₁} C
inst✝¹ : GaloisCategory C
F : C ⥤ FintypeCat
inst✝ : FiberFunctor F
X : C
t : (F.obj X).carrier
⊢ F.map (Pi.π (fun x => X) t) (CategoryTheory.PreGaloisCategory.mkSelfProdFib F X) = t

Tactic:
rw [← congrFun (piComparison_comp_π F _ t), FintypeCat.comp_apply,
  ← PreservesProduct.iso_hom]

Result:
C : Type u₁
inst✝² : Category.{u₂, u₁} C
inst✝¹ : GaloisCategory C
F : C ⥤ FintypeCat
inst✝ : FiberFunctor F
X : C
t : (F.obj X).carrier
⊢ Pi.π (fun b => F.obj X) t
      ((PreservesProduct.iso F fun x => X).hom (CategoryTheory.PreGaloisCategory.mkSelfProdFib F X)) =
    t

Proof state:
C : Type u₁
inst✝² : Category.{u₂, u₁} C
inst✝¹ : GaloisCategory C
F : C ⥤ FintypeCat
inst✝ : FiberFunctor F
X : C
t : (F.obj X).carrier
⊢ Pi.π (fun b => F.obj X) t ((Concrete.productEquiv fun x => F.obj X).symm id) = t

Tactic:
exact Concrete.productEquiv_symm_apply_π.{w, w, w+1} (fun _ : F.obj X ↦ F.obj X) id t

Result:
no goals

Proof state:
C : Type u₁
inst✝² : Category.{u₂, u₁} C
inst✝¹ : GaloisCategory C
F : C ⥤ FintypeCat
inst✝ : FiberFunctor F
X : C
t : (F.obj X).carrier
⊢ Pi.π (fun b => F.obj X) t
      ((PreservesProduct.iso F fun x => X).hom (CategoryTheory.PreGaloisCategory.mkSelfProdFib F X)) =
    t

Tactic:
simp only [mkSelfProdFib, FintypeCat.inv_hom_id_apply]

Result:
C : Type u₁
inst✝² : Category.{u₂, u₁} C
inst✝¹ : GaloisCategory C
F : C ⥤ FintypeCat
inst✝ : FiberFunctor F
X : C
t : (F.obj X).carrier
⊢ Pi.π (fun b => F.obj X) t ((Concrete.productEquiv fun x => F.obj X).symm id) = t
-- Mathlib/Algebra/Polynomial/Mirror.lean
theorem mirror_neg : (-p).mirror = -p.mirror

Proof state:
R : Type u_1
inst✝ : Ring R
p : R[X]
⊢ (-p).mirror = -p.mirror

Tactic:
rw [mirror, mirror, reverse_neg, natTrailingDegree_neg, neg_mul_eq_neg_mul]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/Average.lean
theorem integral_average (μ : Measure α) [IsFiniteMeasure μ] (f : α → E) :
    ∫ _, ⨍ a, f a ∂μ ∂μ = ∫ x, f x ∂μ

Proof state:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace ℝ E
inst✝¹ : CompleteSpace E
μ : Measure α
inst✝ : IsFiniteMeasure μ
f : α → E
⊢ ∫ (x : α), ⨍ (a : α), f a ∂μ ∂μ = ∫ (x : α), f x ∂μ

Tactic:
simp

Result:
no goals
-- Mathlib/MeasureTheory/Integral/SetToL1.lean
theorem setToFun_congr_left' (hT : DominatedFinMeasAdditive μ T C)
    (hT' : DominatedFinMeasAdditive μ T' C') (h : ∀ s, MeasurableSet s → μ s < ∞ → T s = T' s)
    (f : α → E) : setToFun μ T hT f = setToFun μ T' hT' f

Proof state:
α : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
inst✝ : CompleteSpace F
T T' : Set α → E →L[ℝ] F
C C' : ℝ
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive μ T' C'
h : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → T s = T' s
f : α → E
⊢ setToFun μ T hT f = setToFun μ T' hT' f

Tactic:
by_cases hf : Integrable f μ

Result:
case pos
α : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
inst✝ : CompleteSpace F
T T' : Set α → E →L[ℝ] F
C C' : ℝ
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive μ T' C'
h : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → T s = T' s
f : α → E
hf : Integrable f μ
⊢ setToFun μ T hT f = setToFun μ T' hT' f

case neg
α : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
inst✝ : CompleteSpace F
T T' : Set α → E →L[ℝ] F
C C' : ℝ
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive μ T' C'
h : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → T s = T' s
f : α → E
hf : ¬Integrable f μ
⊢ setToFun μ T hT f = setToFun μ T' hT' f

Proof state:
case neg
α : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
inst✝ : CompleteSpace F
T T' : Set α → E →L[ℝ] F
C C' : ℝ
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive μ T' C'
h : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → T s = T' s
f : α → E
hf : ¬Integrable f μ
⊢ setToFun μ T hT f = setToFun μ T' hT' f

Tactic:
simp_rw [setToFun_undef _ hf]

Result:
no goals

Proof state:
case pos
α : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
inst✝ : CompleteSpace F
T T' : Set α → E →L[ℝ] F
C C' : ℝ
hT : DominatedFinMeasAdditive μ T C
hT' : DominatedFinMeasAdditive μ T' C'
h : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → T s = T' s
f : α → E
hf : Integrable f μ
⊢ setToFun μ T hT f = setToFun μ T' hT' f

Tactic:
simp_rw [setToFun_eq _ hf, L1.setToL1_congr_left' T T' hT hT' h]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem self_eq_append_right {x y : List α} : x = x ++ y ↔ y = []

Proof state:
α : Type u_1
x y : List α
⊢ x = x ++ y ↔ y = []

Tactic:
rw [eq_comm, append_right_eq_self]

Result:
no goals
-- Mathlib/Algebra/Order/Hom/Monoid.lean
theorem map_nonpos (ha : a ≤ 0) : f a ≤ 0

Proof state:
F : Type u_1
α : Type u_2
β : Type u_3
inst✝⁶ : FunLike F α β
inst✝⁵ : Preorder α
inst✝⁴ : Zero α
inst✝³ : Preorder β
inst✝² : Zero β
inst✝¹ : OrderHomClass F α β
inst✝ : ZeroHomClass F α β
f : F
a : α
ha : a ≤ 0
⊢ f a ≤ f 0

Tactic:
exact OrderHomClass.mono _ ha

Result:
no goals

Proof state:
F : Type u_1
α : Type u_2
β : Type u_3
inst✝⁶ : FunLike F α β
inst✝⁵ : Preorder α
inst✝⁴ : Zero α
inst✝³ : Preorder β
inst✝² : Zero β
inst✝¹ : OrderHomClass F α β
inst✝ : ZeroHomClass F α β
f : F
a : α
ha : a ≤ 0
⊢ f a ≤ 0

Tactic:
rw [← map_zero f]

Result:
F : Type u_1
α : Type u_2
β : Type u_3
inst✝⁶ : FunLike F α β
inst✝⁵ : Preorder α
inst✝⁴ : Zero α
inst✝³ : Preorder β
inst✝² : Zero β
inst✝¹ : OrderHomClass F α β
inst✝ : ZeroHomClass F α β
f : F
a : α
ha : a ≤ 0
⊢ f a ≤ f 0
-- Mathlib/MeasureTheory/SetSemiring.lean
lemma subset_of_mem_disjointOfDiffUnion (hC : IsSetSemiring C) {I : Finset (Set α)}
    (hs : s ∈ C) (hI : ↑I ⊆ C) (t : Set α)
    (ht : t ∈ (hC.disjointOfDiffUnion hs hI : Set (Set α))) :
    t ⊆ s

Proof state:
α : Type u_1
C : Set (Set α)
s : Set α
hC : IsSetSemiring C
I : Finset (Set α)
hs : s ∈ C
hI : ↑I ⊆ C
t : Set α
ht : t ∈ ↑(hC.disjointOfDiffUnion hs hI)
⊢ s \ ⋃₀ ↑I ≤ s

Tactic:
exact sdiff_le (a := s) (b := ⋃₀ I)

Result:
no goals

Proof state:
α : Type u_1
C : Set (Set α)
s : Set α
hC : IsSetSemiring C
I : Finset (Set α)
hs : s ∈ C
hI : ↑I ⊆ C
t : Set α
ht : t ∈ ↑(hC.disjointOfDiffUnion hs hI)
⊢ t ⊆ s

Tactic:
apply le_trans <| hC.subset_of_diffUnion_disjointOfDiffUnion hs hI t ht

Result:
α : Type u_1
C : Set (Set α)
s : Set α
hC : IsSetSemiring C
I : Finset (Set α)
hs : s ∈ C
hI : ↑I ⊆ C
t : Set α
ht : t ∈ ↑(hC.disjointOfDiffUnion hs hI)
⊢ s \ ⋃₀ ↑I ≤ s
-- Mathlib/Topology/Sets/Opens.lean
theorem mem_iSup {ι} {x : α} {s : ι → Opens α} : x ∈ iSup s ↔ ∃ i, x ∈ s i

Proof state:
α : Type u_2
inst✝ : TopologicalSpace α
ι : Sort u_5
x : α
s : ι → Opens α
⊢ x ∈ ↑(iSup s) ↔ ∃ i, x ∈ s i

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_2
inst✝ : TopologicalSpace α
ι : Sort u_5
x : α
s : ι → Opens α
⊢ x ∈ iSup s ↔ ∃ i, x ∈ s i

Tactic:
rw [← SetLike.mem_coe]

Result:
α : Type u_2
inst✝ : TopologicalSpace α
ι : Sort u_5
x : α
s : ι → Opens α
⊢ x ∈ ↑(iSup s) ↔ ∃ i, x ∈ s i
-- Mathlib/Algebra/Order/GroupWithZero/Unbundled.lean
/-- See `lt_inv_mul_iff₀'` for a version with multiplication on the other side. -/
lemma lt_inv_mul_iff₀ (hc : 0 < c) : a < c⁻¹ * b ↔ c * a < b where
  mp h

Proof state:
G₀ : Type u_2
inst✝⁴ : GroupWithZero G₀
inst✝³ : PartialOrder G₀
inst✝² : ZeroLEOneClass G₀
inst✝¹ : PosMulReflectLT G₀
a b c : G₀
inst✝ : PosMulStrictMono G₀
hc : 0 < c
h : c * a < b
⊢ a < c⁻¹ * b

Tactic:
simpa [hc.ne'] using mul_lt_mul_of_pos_left h (inv_pos.2 hc)

Result:
no goals

Proof state:
G₀ : Type u_2
inst✝⁴ : GroupWithZero G₀
inst✝³ : PartialOrder G₀
inst✝² : ZeroLEOneClass G₀
inst✝¹ : PosMulReflectLT G₀
a b c : G₀
inst✝ : PosMulStrictMono G₀
hc : 0 < c
h : a < c⁻¹ * b
⊢ c * a < b

Tactic:
simpa [hc.ne'] using mul_lt_mul_of_pos_left h hc

Result:
no goals
-- Mathlib/FieldTheory/Relrank.lean
theorem relfinrank_comap_comap_eq_relfinrank_inf (f : L →+* E) :
    relfinrank (A.comap f) (B.comap f) = relfinrank A (B ⊓ f.fieldRange)

Proof state:
E : Type v
inst✝¹ : Field E
L : Type w
inst✝ : Field L
A B : Subfield E
f : L →+* E
⊢ (comap f A).relfinrank (comap f B) = A.relfinrank (B ⊓ f.fieldRange)

Tactic:
simpa using congr(toNat $(lift_relrank_comap_comap_eq_lift_relrank_inf A B f))

Result:
no goals
-- Mathlib/Probability/Kernel/Disintegration/MeasurableStieltjes.lean
lemma isRatStieltjesPoint_unit_prod_iff (f : α → ℚ → ℝ) (a : α) :
    IsRatStieltjesPoint (fun p : Unit × α ↦ f p.2) ((), a)
      ↔ IsRatStieltjesPoint f a

Proof state:
α : Type u_1
f : α → ℚ → ℝ
a : α
⊢ IsRatStieltjesPoint (fun p => f p.2) ((), a) ↔ IsRatStieltjesPoint f a

Tactic:
constructor <;>
  exact fun h ↦ ⟨h.mono, h.tendsto_atTop_one, h.tendsto_atBot_zero, h.iInf_rat_gt_eq⟩

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Find.lean
theorem of_findIdx?_eq_none {xs : Array α} {p : α → Bool} (w : xs.findIdx? p = none) :
    ∀ i : Nat, match xs[i]? with | some a => ¬ p a | none => true

Proof state:
α : Type u_1
xs : Array α
p : α → Bool
w : findIdx? p xs = none
⊢ ∀ (i : Nat),
    match xs[i]? with
    | some a => ¬p a = true
    | none => true = true

Tactic:
rcases xs with ⟨xs⟩

Result:
case mk
α : Type u_1
p : α → Bool
xs : List α
w : findIdx? p { toList := xs } = none
⊢ ∀ (i : Nat),
    match { toList := xs }[i]? with
    | some a => ¬p a = true
    | none => true = true

Proof state:
case mk
α : Type u_1
p : α → Bool
xs : List α
w : findIdx? p { toList := xs } = none
⊢ ∀ (i : Nat),
    match { toList := xs }[i]? with
    | some a => ¬p a = true
    | none => true = true

Tactic:
simpa using List.of_findIdx?_eq_none (by simpa using w)

Result:
no goals

Proof state:
α : Type u_1
p : α → Bool
xs : List α
w : findIdx? p { toList := xs } = none
⊢ List.findIdx? p xs = none

Tactic:
simpa using w

Result:
no goals
-- Mathlib/Data/Finset/Empty.lean
theorem isEmpty_coe_sort {s : Finset α} : IsEmpty (s : Type _) ↔ s = ∅

Proof state:
α : Type u_1
s : Finset α
⊢ IsEmpty { x // x ∈ s } ↔ s = ∅

Tactic:
simpa using @Set.isEmpty_coe_sort α s

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Arithmetic.lean
theorem div_pos {b c : Ordinal} (h : c ≠ 0) : 0 < b / c ↔ c ≤ b

Proof state:
b c : Ordinal.{u_4}
h : c ≠ 0
⊢ 0 < b / c ↔ c ≤ b

Tactic:
simp [lt_div h]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Bool.lean
theorem and_comm : ∀ (x y : Bool), (x && y) = (y && x)

Proof state:
⊢ ∀ (x y : Bool), (x && y) = (y && x)

Tactic:
decide

Result:
no goals
-- Mathlib/MeasureTheory/Group/Measure.lean
theorem forall_measure_preimage_mul_right_iff (μ : Measure G) :
    (∀ (g : G) (A : Set G), MeasurableSet A → μ ((fun h => h * g) ⁻¹' A) = μ A) ↔
      IsMulRightInvariant μ

Proof state:
G : Type u_1
inst✝² : MeasurableSpace G
inst✝¹ : Mul G
inst✝ : MeasurableMul G
μ : Measure G
⊢ (∀ (g : G) (A : Set G), MeasurableSet A → μ ((fun h => h * g) ⁻¹' A) = μ A) ↔
    ∀ (g : G) (s : Set G), MeasurableSet s → (Measure.map (fun x => x * g) μ) s = μ s

Tactic:
refine forall_congr' fun g => forall_congr' fun A => forall_congr' fun hA => ?_

Result:
G : Type u_1
inst✝² : MeasurableSpace G
inst✝¹ : Mul G
inst✝ : MeasurableMul G
μ : Measure G
g : G
A : Set G
hA : MeasurableSet A
⊢ μ ((fun h => h * g) ⁻¹' A) = μ A ↔ (Measure.map (fun x => x * g) μ) A = μ A

Proof state:
G : Type u_1
inst✝² : MeasurableSpace G
inst✝¹ : Mul G
inst✝ : MeasurableMul G
μ : Measure G
⊢ (∀ (g : G) (A : Set G), MeasurableSet A → μ ((fun h => h * g) ⁻¹' A) = μ A) ↔
    ∀ (g : G), Measure.map (fun x => x * g) μ = μ

Tactic:
simp_rw [Measure.ext_iff]

Result:
G : Type u_1
inst✝² : MeasurableSpace G
inst✝¹ : Mul G
inst✝ : MeasurableMul G
μ : Measure G
⊢ (∀ (g : G) (A : Set G), MeasurableSet A → μ ((fun h => h * g) ⁻¹' A) = μ A) ↔
    ∀ (g : G) (s : Set G), MeasurableSet s → (Measure.map (fun x => x * g) μ) s = μ s

Proof state:
G : Type u_1
inst✝² : MeasurableSpace G
inst✝¹ : Mul G
inst✝ : MeasurableMul G
μ : Measure G
⊢ (∀ (g : G), Measure.map (fun x => x * g) μ = μ) ↔ μ.IsMulRightInvariant

Tactic:
exact ⟨fun h => ⟨h⟩, fun h => h.1⟩

Result:
no goals

Proof state:
G : Type u_1
inst✝² : MeasurableSpace G
inst✝¹ : Mul G
inst✝ : MeasurableMul G
μ : Measure G
g : G
A : Set G
hA : MeasurableSet A
⊢ μ ((fun h => h * g) ⁻¹' A) = μ A ↔ (Measure.map (fun x => x * g) μ) A = μ A

Tactic:
rw [map_apply (measurable_mul_const g) hA]

Result:
no goals
-- Mathlib/Order/OrdContinuous.lean
theorem lt_iff (hf : LeftOrdContinuous f) (h : Injective f) {x y} : f x < f y ↔ x < y

Proof state:
α : Type u
β : Type v
inst✝¹ : SemilatticeSup α
inst✝ : SemilatticeSup β
f : α → β
hf : LeftOrdContinuous f
h : Injective f
x y : α
⊢ f x < f y ↔ x < y

Tactic:
simp only [lt_iff_le_not_le, hf.le_iff h]

Result:
no goals
-- Mathlib/Topology/PartialHomeomorph.lean
theorem transHomeomorph_transHomeomorph (e : PartialHomeomorph X Y) (f' : Y ≃ₜ Z) (f'' : Z ≃ₜ Z') :
    (e.transHomeomorph f').transHomeomorph f'' = e.transHomeomorph (f'.trans f'')

Proof state:
X : Type u_1
Y : Type u_3
Z : Type u_5
Z' : Type u_6
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace Z'
e : PartialHomeomorph X Y
f' : Y ≃ₜ Z
f'' : Z ≃ₜ Z'
⊢ (e.transHomeomorph f').transHomeomorph f'' = e.transHomeomorph (f'.trans f'')

Tactic:
simp only [transHomeomorph_eq_trans, trans_assoc, Homeomorph.trans_toPartialHomeomorph]

Result:
no goals
-- Mathlib/Analysis/Analytic/Basic.lean
theorem analyticWithinAt_insert {f : E → F} {s : Set E} {x y : E} :
    AnalyticWithinAt 𝕜 f (insert y s) x ↔ AnalyticWithinAt 𝕜 f s x

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
s : Set E
x y : E
⊢ AnalyticWithinAt 𝕜 f (insert y s) x ↔ AnalyticWithinAt 𝕜 f s x

Tactic:
simp [AnalyticWithinAt]

Result:
no goals
-- Mathlib/GroupTheory/Perm/Basic.lean
lemma BijOn.perm_pow : BijOn f s s → ∀ n : ℕ, BijOn (f ^ n) s s

Proof state:
α : Type u_1
f : Perm α
s : Set α
⊢ BijOn (⇑f) s s → ∀ (n : ℕ), BijOn (⇑(f ^ n)) s s

Tactic:
simp_rw [Equiv.Perm.coe_pow]

Result:
α : Type u_1
f : Perm α
s : Set α
⊢ BijOn (⇑f) s s → ∀ (n : ℕ), BijOn (⇑f)^[n] s s

Proof state:
α : Type u_1
f : Perm α
s : Set α
⊢ BijOn (⇑f) s s → ∀ (n : ℕ), BijOn (⇑f)^[n] s s

Tactic:
exact BijOn.iterate

Result:
no goals
-- Mathlib/Order/SuccPred/Relation.lean
theorem transGen_of_succ_of_reflexive (r : α → α → Prop) {n m : α} (hr : Reflexive r)
    (h1 : ∀ i ∈ Ico n m, r i (succ i)) (h2 : ∀ i ∈ Ico m n, r (succ i) i) : TransGen r n m

Proof state:
case inl
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
r : α → α → Prop
m : α
hr : Reflexive r
h1 : ∀ i ∈ Ico m m, r i (succ i)
h2 : ∀ i ∈ Ico m m, r (succ i) i
⊢ TransGen r m m

Tactic:
exact TransGen.single (hr m)

Result:
no goals

Proof state:
case inr
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
r : α → α → Prop
n m : α
hr : Reflexive r
h1 : ∀ i ∈ Ico n m, r i (succ i)
h2 : ∀ i ∈ Ico m n, r (succ i) i
hmn : m ≠ n
⊢ TransGen r n m

Tactic:
exact transGen_of_succ_of_ne r h1 h2 hmn.symm

Result:
no goals

Proof state:
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
r : α → α → Prop
n m : α
hr : Reflexive r
h1 : ∀ i ∈ Ico n m, r i (succ i)
h2 : ∀ i ∈ Ico m n, r (succ i) i
⊢ TransGen r n m

Tactic:
rcases eq_or_ne m n with (rfl | hmn)

Result:
case inl
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
r : α → α → Prop
m : α
hr : Reflexive r
h1 : ∀ i ∈ Ico m m, r i (succ i)
h2 : ∀ i ∈ Ico m m, r (succ i) i
⊢ TransGen r m m

case inr
α : Type u_1
inst✝² : LinearOrder α
inst✝¹ : SuccOrder α
inst✝ : IsSuccArchimedean α
r : α → α → Prop
n m : α
hr : Reflexive r
h1 : ∀ i ∈ Ico n m, r i (succ i)
h2 : ∀ i ∈ Ico m n, r (succ i) i
hmn : m ≠ n
⊢ TransGen r n m
-- Mathlib/NumberTheory/LSeries/HurwitzZetaEven.lean
/-- For `a = 0`, both kernels agree. -/
lemma evenKernel_eq_cosKernel_of_zero : evenKernel 0 = cosKernel 0

Proof state:
⊢ evenKernel 0 = cosKernel 0

Tactic:
ext1 x

Result:
case h
x : ℝ
⊢ evenKernel 0 x = cosKernel 0 x

Proof state:
case h
x : ℝ
⊢ evenKernel 0 x = cosKernel 0 x

Tactic:
simp [← QuotientAddGroup.mk_zero, ← ofReal_inj, evenKernel_def, cosKernel_def]

Result:
no goals