harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/BoxIntegral/Basic.lean
theorem sum_integral_congr (h : Integrable I l f vol) {π₁ π₂ : Prepartition I}
    (hU : π₁.iUnion = π₂.iUnion) :
    ∑ J ∈ π₁.boxes, integral J l f vol = ∑ J ∈ π₂.boxes, integral J l f vol

Proof state:
ι : Type u
E : Type v
F : Type w
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
I : Box ι
inst✝¹ : Fintype ι
l : IntegrationParams
f : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
inst✝ : CompleteSpace F
h : Integrable I l f vol
π₁ π₂ : Prepartition I
hU : π₁.iUnion = π₂.iUnion
⊢ Tendsto (integralSum f vol) (toFilteriUnion I π₁) (𝓝 (∑ J ∈ π₂.boxes, integral J l f vol))

Tactic:
rw [l.toFilteriUnion_congr _ hU]

Result:
ι : Type u
E : Type v
F : Type w
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
I : Box ι
inst✝¹ : Fintype ι
l : IntegrationParams
f : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
inst✝ : CompleteSpace F
h : Integrable I l f vol
π₁ π₂ : Prepartition I
hU : π₁.iUnion = π₂.iUnion
⊢ Tendsto (integralSum f vol) (toFilteriUnion I π₂) (𝓝 (∑ J ∈ π₂.boxes, integral J l f vol))

Proof state:
ι : Type u
E : Type v
F : Type w
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
I : Box ι
inst✝¹ : Fintype ι
l : IntegrationParams
f : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
inst✝ : CompleteSpace F
h : Integrable I l f vol
π₁ π₂ : Prepartition I
hU : π₁.iUnion = π₂.iUnion
⊢ Tendsto (integralSum f vol) (toFilteriUnion I π₂) (𝓝 (∑ J ∈ π₂.boxes, integral J l f vol))

Tactic:
exact h.tendsto_integralSum_sum_integral π₂

Result:
no goals

Proof state:
ι : Type u
E : Type v
F : Type w
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
I : Box ι
inst✝¹ : Fintype ι
l : IntegrationParams
f : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
inst✝ : CompleteSpace F
h : Integrable I l f vol
π₁ π₂ : Prepartition I
hU : π₁.iUnion = π₂.iUnion
⊢ ∑ J ∈ π₁.boxes, integral J l f vol = ∑ J ∈ π₂.boxes, integral J l f vol

Tactic:
refine tendsto_nhds_unique (h.tendsto_integralSum_sum_integral π₁) ?_

Result:
ι : Type u
E : Type v
F : Type w
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace ℝ F
I : Box ι
inst✝¹ : Fintype ι
l : IntegrationParams
f : (ι → ℝ) → E
vol : ι →ᵇᵃ[⊤] E →L[ℝ] F
inst✝ : CompleteSpace F
h : Integrable I l f vol
π₁ π₂ : Prepartition I
hU : π₁.iUnion = π₂.iUnion
⊢ Tendsto (integralSum f vol) (toFilteriUnion I π₁) (𝓝 (∑ J ∈ π₂.boxes, integral J l f vol))
-- Mathlib/Algebra/Polynomial/Degree/Definitions.lean
theorem natDegree_sub_le (p q : R[X]) : natDegree (p - q) ≤ max (natDegree p) (natDegree q)

Proof state:
R : Type u
inst✝ : Ring R
p q : R[X]
⊢ (p - q).natDegree ≤ p.natDegree ⊔ q.natDegree

Tactic:
simpa only [← natDegree_neg q] using natDegree_add_le p (-q)

Result:
no goals
-- Mathlib/MeasureTheory/Integral/Lebesgue.lean
theorem setLIntegral_measure_zero (s : Set α) (f : α → ℝ≥0∞) (hs' : μ s = 0) :
    ∫⁻ x in s, f x ∂μ = 0

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ≥0∞
hs' : μ s = 0
⊢ ∫⁻ (x : α) in s, f x ∂μ = 0

Tactic:
convert lintegral_zero_measure _

Result:
case h.e'_2.h.e'_3.h
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ≥0∞
hs' : μ s = 0
⊢ μ.restrict s = 0

Proof state:
case h.e'_2.h.e'_3.h
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ≥0∞
hs' : μ s = 0
⊢ μ.restrict s = 0

Tactic:
exact Measure.restrict_eq_zero.2 hs'

Result:
no goals
-- Mathlib/Algebra/Homology/ShortComplex/Exact.lean
lemma QuasiIso.exact_iff {S₁ S₂ : ShortComplex C} (φ : S₁ ⟶ S₂)
    [S₁.HasHomology] [S₂.HasHomology] [QuasiIso φ] : S₁.Exact ↔ S₂.Exact

Proof state:
C : Type u_1
inst✝⁴ : Category.{u_3, u_1} C
inst✝³ : Preadditive C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
inst✝² : S₁.HasHomology
inst✝¹ : S₂.HasHomology
inst✝ : QuasiIso φ
⊢ S₁.Exact ↔ S₂.Exact

Tactic:
simp only [exact_iff_isZero_homology]

Result:
C : Type u_1
inst✝⁴ : Category.{u_3, u_1} C
inst✝³ : Preadditive C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
inst✝² : S₁.HasHomology
inst✝¹ : S₂.HasHomology
inst✝ : QuasiIso φ
⊢ IsZero S₁.homology ↔ IsZero S₂.homology

Proof state:
C : Type u_1
inst✝⁴ : Category.{u_3, u_1} C
inst✝³ : Preadditive C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
inst✝² : S₁.HasHomology
inst✝¹ : S₂.HasHomology
inst✝ : QuasiIso φ
⊢ IsZero S₁.homology ↔ IsZero S₂.homology

Tactic:
exact Iso.isZero_iff (asIso (homologyMap φ))

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lex/Lemmas.lean
theorem le_empty [LT α] (l : Array α) : l ≤ #[] ↔ l = #[]

Proof state:
case mk
α : Type u_1
inst✝ : LT α
toList✝ : List α
⊢ { toList := toList✝ } ≤ #[] ↔ { toList := toList✝ } = #[]

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
inst✝ : LT α
l : Array α
⊢ l ≤ #[] ↔ l = #[]

Tactic:
cases l

Result:
case mk
α : Type u_1
inst✝ : LT α
toList✝ : List α
⊢ { toList := toList✝ } ≤ #[] ↔ { toList := toList✝ } = #[]
-- Mathlib/Algebra/Polynomial/Eval/Coeff.lean
theorem eval_zero_map (f : R →+* S) (p : R[X]) : (p.map f).eval 0 = f (p.eval 0)

Proof state:
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
p : R[X]
⊢ eval 0 (map f p) = f (eval 0 p)

Tactic:
simp [← coeff_zero_eq_eval_zero]

Result:
no goals
-- Mathlib/CategoryTheory/Dialectica/Monoidal.lean
theorem symmetry (X Y : Dial C) :
    (braiding X Y).hom ≫ (braiding Y X).hom = 𝟙 (tensorObj X Y)

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasFiniteProducts C
inst✝ : HasPullbacks C
X Y : Dial C
⊢ (X.braiding Y).hom ≫ (Y.braiding X).hom = 𝟙 (X.tensorObj Y)

Tactic:
aesop_cat

Result:
no goals
-- Mathlib/Logic/Equiv/Defs.lean
theorem equivCongr_refl {α β} :
    (Equiv.refl α).equivCongr (Equiv.refl β) = Equiv.refl (α ≃ β)

Proof state:
α : Sort u_1
β : Sort u_2
⊢ (Equiv.refl α).equivCongr (Equiv.refl β) = Equiv.refl (α ≃ β)

Tactic:
ext

Result:
case H.H
α : Sort u_1
β : Sort u_2
x✝¹ : α ≃ β
x✝ : α
⊢ (((Equiv.refl α).equivCongr (Equiv.refl β)) x✝¹) x✝ = ((Equiv.refl (α ≃ β)) x✝¹) x✝

Proof state:
case H.H
α : Sort u_1
β : Sort u_2
x✝¹ : α ≃ β
x✝ : α
⊢ (((Equiv.refl α).equivCongr (Equiv.refl β)) x✝¹) x✝ = ((Equiv.refl (α ≃ β)) x✝¹) x✝

Tactic:
rfl

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/InverseDeriv.lean
theorem hasDerivWithinAt_arcsin_Ici {x : ℝ} (h : x ≠ -1) :
    HasDerivWithinAt arcsin (1 / √(1 - x ^ 2)) (Ici x) x

Proof state:
case inr
x : ℝ
h : x ≠ -1
h' : x ≠ 1
⊢ HasDerivWithinAt arcsin (1 / √(1 - x ^ 2)) (Ici x) x

Tactic:
exact (hasDerivAt_arcsin h h').hasDerivWithinAt

Result:
no goals

Proof state:
case inl
h : 1 ≠ -1
⊢ HasDerivWithinAt arcsin (1 / √(1 - 1 ^ 2)) (Ici 1) 1

Tactic:
convert (hasDerivWithinAt_const (1 : ℝ) _ (π / 2)).congr _ _ <;>
  simp +contextual [arcsin_of_one_le]

Result:
no goals

Proof state:
x : ℝ
h : x ≠ -1
⊢ HasDerivWithinAt arcsin (1 / √(1 - x ^ 2)) (Ici x) x

Tactic:
rcases eq_or_ne x 1 with (rfl | h')

Result:
case inl
h : 1 ≠ -1
⊢ HasDerivWithinAt arcsin (1 / √(1 - 1 ^ 2)) (Ici 1) 1

case inr
x : ℝ
h : x ≠ -1
h' : x ≠ 1
⊢ HasDerivWithinAt arcsin (1 / √(1 - x ^ 2)) (Ici x) x
-- Mathlib/NumberTheory/Divisors.lean
theorem divisorsAntidiagonal_zero : divisorsAntidiagonal 0 = ∅

Proof state:
⊢ divisorsAntidiagonal 0 = ∅

Tactic:
ext

Result:
case h
a✝ : ℕ × ℕ
⊢ a✝ ∈ divisorsAntidiagonal 0 ↔ a✝ ∈ ∅

Proof state:
case h
a✝ : ℕ × ℕ
⊢ a✝ ∈ divisorsAntidiagonal 0 ↔ a✝ ∈ ∅

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/Adjoint.lean
theorem conj_adjoint {T : E →L[𝕜] E} (hT : IsSelfAdjoint T) (S : E →L[𝕜] F) :
    IsSelfAdjoint (S ∘L T ∘L ContinuousLinearMap.adjoint S)

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : InnerProductSpace 𝕜 F
inst✝¹ : CompleteSpace E
inst✝ : CompleteSpace F
T : E →L[𝕜] E
hT : adjoint T = T
S : E →L[𝕜] F
⊢ (S.comp T).comp (adjoint S) = S.comp (T.comp (adjoint S))

Tactic:
exact ContinuousLinearMap.comp_assoc _ _ _

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : InnerProductSpace 𝕜 F
inst✝¹ : CompleteSpace E
inst✝ : CompleteSpace F
T : E →L[𝕜] E
hT : IsSelfAdjoint T
S : E →L[𝕜] F
⊢ IsSelfAdjoint (S.comp (T.comp (adjoint S)))

Tactic:
rw [isSelfAdjoint_iff'] at hT ⊢

Result:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : InnerProductSpace 𝕜 F
inst✝¹ : CompleteSpace E
inst✝ : CompleteSpace F
T : E →L[𝕜] E
hT : adjoint T = T
S : E →L[𝕜] F
⊢ adjoint (S.comp (T.comp (adjoint S))) = S.comp (T.comp (adjoint S))

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : InnerProductSpace 𝕜 F
inst✝¹ : CompleteSpace E
inst✝ : CompleteSpace F
T : E →L[𝕜] E
hT : adjoint T = T
S : E →L[𝕜] F
⊢ adjoint (S.comp (T.comp (adjoint S))) = S.comp (T.comp (adjoint S))

Tactic:
simp only [hT, adjoint_comp, adjoint_adjoint]

Result:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : InnerProductSpace 𝕜 F
inst✝¹ : CompleteSpace E
inst✝ : CompleteSpace F
T : E →L[𝕜] E
hT : adjoint T = T
S : E →L[𝕜] F
⊢ (S.comp T).comp (adjoint S) = S.comp (T.comp (adjoint S))
-- Mathlib/Data/Set/Pairwise/Basic.lean
theorem pairwise_union :
    (s ∪ t).Pairwise r ↔
    s.Pairwise r ∧ t.Pairwise r ∧ ∀ a ∈ s, ∀ b ∈ t, a ≠ b → r a b ∧ r b a

Proof state:
α : Type u_1
r : α → α → Prop
s t : Set α
⊢ (((∀ x ∈ s, ∀ x_1 ∈ s, x ≠ x_1 → r x x_1) ∧ ∀ x ∈ t, ∀ x_1 ∈ s, x ≠ x_1 → r x x_1) ∧
      (∀ x ∈ s, ∀ x_1 ∈ t, x ≠ x_1 → r x x_1) ∧ ∀ x ∈ t, ∀ x_1 ∈ t, x ≠ x_1 → r x x_1) ↔
    (∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → x ≠ y → r x y) ∧
      (∀ ⦃x : α⦄, x ∈ t → ∀ ⦃y : α⦄, y ∈ t → x ≠ y → r x y) ∧
        (∀ x ∈ s, ∀ x_1 ∈ t, x ≠ x_1 → r x x_1) ∧ ∀ x ∈ s, ∀ x_2 ∈ t, x ≠ x_2 → r x_2 x

Tactic:
aesop

Result:
no goals

Proof state:
α : Type u_1
r : α → α → Prop
s t : Set α
⊢ (s ∪ t).Pairwise r ↔ s.Pairwise r ∧ t.Pairwise r ∧ ∀ a ∈ s, ∀ b ∈ t, a ≠ b → r a b ∧ r b a

Tactic:
simp only [Set.Pairwise, mem_union, or_imp, forall_and]

Result:
α : Type u_1
r : α → α → Prop
s t : Set α
⊢ (((∀ x ∈ s, ∀ x_1 ∈ s, x ≠ x_1 → r x x_1) ∧ ∀ x ∈ t, ∀ x_1 ∈ s, x ≠ x_1 → r x x_1) ∧
      (∀ x ∈ s, ∀ x_1 ∈ t, x ≠ x_1 → r x x_1) ∧ ∀ x ∈ t, ∀ x_1 ∈ t, x ≠ x_1 → r x x_1) ↔
    (∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → x ≠ y → r x y) ∧
      (∀ ⦃x : α⦄, x ∈ t → ∀ ⦃y : α⦄, y ∈ t → x ≠ y → r x y) ∧
        (∀ x ∈ s, ∀ x_1 ∈ t, x ≠ x_1 → r x x_1) ∧ ∀ x ∈ s, ∀ x_2 ∈ t, x ≠ x_2 → r x_2 x
-- Mathlib/Topology/Category/TopCat/Limits/Products.lean
theorem prodIsoProd_hom_snd (X Y : TopCat.{u}) :
    (prodIsoProd X Y).hom ≫ prodSnd = Limits.prod.snd

Proof state:
X Y : TopCat
⊢ (X.prodIsoProd Y).hom ≫ prodSnd = prod.snd

Tactic:
simp [← Iso.eq_inv_comp, prodIsoProd]

Result:
X Y : TopCat
⊢ prodSnd = (X.prodBinaryFan Y).snd

Proof state:
X Y : TopCat
⊢ prodSnd = (X.prodBinaryFan Y).snd

Tactic:
rfl

Result:
no goals
-- Mathlib/Topology/Maps/Basic.lean
lemma IsOpenEmbedding.isOpen_iff_image_isOpen (hf : IsOpenEmbedding f) {s : Set X} :
    IsOpen s ↔ IsOpen (f '' s) where
  mp := hf.isOpenMap s
  mpr h

Proof state:
X : Type u_1
Y : Type u_2
f : X → Y
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
hf : IsOpenEmbedding f
s : Set X
h : IsOpen (f '' s)
⊢ IsOpen s

Tactic:
convert ← h.preimage hf.isEmbedding.continuous

Result:
case h.e'_3
X : Type u_1
Y : Type u_2
f : X → Y
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
hf : IsOpenEmbedding f
s : Set X
h : IsOpen (f '' s)
⊢ f ⁻¹' (f '' s) = s

Proof state:
case h.e'_3
X : Type u_1
Y : Type u_2
f : X → Y
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
hf : IsOpenEmbedding f
s : Set X
h : IsOpen (f '' s)
⊢ f ⁻¹' (f '' s) = s

Tactic:
apply preimage_image_eq _ hf.injective

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/Trace.lean
theorem trace_col_mul_row {ι : Type*} [Unique ι] [NonUnitalNonAssocSemiring R] (a b : n → R) :
    trace (col ι a * row ι b) = dotProduct a b

Proof state:
n : Type u_3
R : Type u_6
inst✝² : Fintype n
ι : Type u_8
inst✝¹ : Unique ι
inst✝ : NonUnitalNonAssocSemiring R
a b : n → R
⊢ (col ι a * row ι b).trace = a ⬝ᵥ b

Tactic:
apply Finset.sum_congr rfl

Result:
n : Type u_3
R : Type u_6
inst✝² : Fintype n
ι : Type u_8
inst✝¹ : Unique ι
inst✝ : NonUnitalNonAssocSemiring R
a b : n → R
⊢ ∀ x ∈ Finset.univ, (col ι a * row ι b).diag x = a x * b x

Proof state:
n : Type u_3
R : Type u_6
inst✝² : Fintype n
ι : Type u_8
inst✝¹ : Unique ι
inst✝ : NonUnitalNonAssocSemiring R
a b : n → R
⊢ ∀ x ∈ Finset.univ, (col ι a * row ι b).diag x = a x * b x

Tactic:
simp [mul_apply]

Result:
no goals
-- Mathlib/Algebra/ModEq.lean
@[simp] lemma mul_modEq_mul_left (hc : c ≠ 0) : c * a ≡ c * b [PMOD p] ↔ a ≡ b [PMOD (p / c)]

Proof state:
α : Type u_1
inst✝ : Field α
a b c p : α
hc : c ≠ 0
⊢ c * a ≡ c * b [PMOD p] ↔ a ≡ b [PMOD p / c]

Tactic:
simp [mul_comm c, hc]

Result:
no goals
-- Mathlib/Analysis/Normed/Field/UnitBall.lean
theorem unitSphereToUnits_injective [NormedDivisionRing 𝕜] :
    Function.Injective (unitSphereToUnits 𝕜) := fun x y h =>
  Subtype.eq <| by convert congr_arg Units.val h

Proof state:
𝕜 : Type u_1
inst✝ : NormedDivisionRing 𝕜
x y : ↑(sphere 0 1)
h : (unitSphereToUnits 𝕜) x = (unitSphereToUnits 𝕜) y
⊢ ↑x = ↑y

Tactic:
convert congr_arg Units.val h

Result:
no goals
-- Mathlib/RingTheory/Polynomial/Pochhammer.lean
theorem descPochhammer_map (f : R →+* T) (n : ℕ) :
    (descPochhammer R n).map f = descPochhammer T n

Proof state:
case zero
R : Type u
inst✝¹ : Ring R
T : Type v
inst✝ : Ring T
f : R →+* T
⊢ map f (descPochhammer R 0) = descPochhammer T 0

Tactic:
simp

Result:
no goals

Proof state:
R : Type u
inst✝¹ : Ring R
T : Type v
inst✝ : Ring T
f : R →+* T
n : ℕ
⊢ map f (descPochhammer R n) = descPochhammer T n

Tactic:
induction n with
| zero => simp
| succ n ih => simp [ih, descPochhammer_succ_left, map_comp]

Result:
no goals

Proof state:
case succ
R : Type u
inst✝¹ : Ring R
T : Type v
inst✝ : Ring T
f : R →+* T
n : ℕ
ih : map f (descPochhammer R n) = descPochhammer T n
⊢ map f (descPochhammer R (n + 1)) = descPochhammer T (n + 1)

Tactic:
simp [ih, descPochhammer_succ_left, map_comp]

Result:
no goals
-- Mathlib/Analysis/Convex/Gauge.lean
theorem exists_lt_of_gauge_lt (absorbs : Absorbent ℝ s) (h : gauge s x < a) :
    ∃ b, 0 < b ∧ b < a ∧ x ∈ b • s

Proof state:
case intro.intro.intro
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : Set E
x : E
a : ℝ
absorbs : Absorbent ℝ s
h : gauge s x < a
b : ℝ
hba : b < a
hb : 0 < b
hx : x ∈ b • s
⊢ ∃ b, 0 < b ∧ b < a ∧ x ∈ b • s

Tactic:
exact ⟨b, hb, hba, hx⟩

Result:
no goals

Proof state:
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : Set E
x : E
a : ℝ
absorbs : Absorbent ℝ s
h : gauge s x < a
⊢ ∃ b, 0 < b ∧ b < a ∧ x ∈ b • s

Tactic:
obtain ⟨b, ⟨hb, hx⟩, hba⟩ := exists_lt_of_csInf_lt absorbs.gauge_set_nonempty h

Result:
case intro.intro.intro
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : Set E
x : E
a : ℝ
absorbs : Absorbent ℝ s
h : gauge s x < a
b : ℝ
hba : b < a
hb : 0 < b
hx : x ∈ b • s
⊢ ∃ b, 0 < b ∧ b < a ∧ x ∈ b • s
-- Mathlib/.lake/packages/lean4/src/lean/Init/Omega/IntList.lean
theorem dot_distrib_left (xs ys zs : IntList) : (xs + ys).dot zs = xs.dot zs + ys.dot zs

Proof state:
xs ys zs : IntList
⊢ (xs + ys).dot zs = xs.dot zs + ys.dot zs

Tactic:
simp [dot, mul_distrib_left, sum_add]

Result:
no goals
-- Mathlib/Order/Filter/AtTopBot/Archimedean.lean
theorem Tendsto.atTop_nsmul_const {f : α → ℕ} (hr : 0 < r) (hf : Tendsto f l atTop) :
    Tendsto (fun x => f x • r) l atTop

Proof state:
case intro
α : Type u_1
R : Type u_2
l : Filter α
r : R
inst✝¹ : LinearOrderedCancelAddCommMonoid R
inst✝ : Archimedean R
f : α → ℕ
hr : 0 < r
hf : Tendsto f l atTop
s : R
n : ℕ
hn : s ≤ n • r
⊢ ∀ᶠ (a : α) in l, s ≤ f a • r

Tactic:
exact (tendsto_atTop.mp hf n).mono fun a ha => hn.trans (nsmul_le_nsmul_left hr.le ha)

Result:
no goals

Proof state:
α : Type u_1
R : Type u_2
l : Filter α
r : R
inst✝¹ : LinearOrderedCancelAddCommMonoid R
inst✝ : Archimedean R
f : α → ℕ
hr : 0 < r
hf : Tendsto f l atTop
s : R
⊢ ∀ᶠ (a : α) in l, s ≤ f a • r

Tactic:
obtain ⟨n : ℕ, hn : s ≤ n • r⟩ := Archimedean.arch s hr

Result:
case intro
α : Type u_1
R : Type u_2
l : Filter α
r : R
inst✝¹ : LinearOrderedCancelAddCommMonoid R
inst✝ : Archimedean R
f : α → ℕ
hr : 0 < r
hf : Tendsto f l atTop
s : R
n : ℕ
hn : s ≤ n • r
⊢ ∀ᶠ (a : α) in l, s ≤ f a • r

Proof state:
α : Type u_1
R : Type u_2
l : Filter α
r : R
inst✝¹ : LinearOrderedCancelAddCommMonoid R
inst✝ : Archimedean R
f : α → ℕ
hr : 0 < r
hf : Tendsto f l atTop
⊢ Tendsto (fun x => f x • r) l atTop

Tactic:
refine tendsto_atTop.mpr fun s => ?_

Result:
α : Type u_1
R : Type u_2
l : Filter α
r : R
inst✝¹ : LinearOrderedCancelAddCommMonoid R
inst✝ : Archimedean R
f : α → ℕ
hr : 0 < r
hf : Tendsto f l atTop
s : R
⊢ ∀ᶠ (a : α) in l, s ≤ f a • r
-- Mathlib/Topology/MetricSpace/Equicontinuity.lean
theorem equicontinuousAt_of_continuity_modulus {ι : Type*} [TopologicalSpace β] {x₀ : β}
    (b : β → ℝ) (b_lim : Tendsto b (𝓝 x₀) (𝓝 0)) (F : ι → β → α)
    (H : ∀ᶠ x in 𝓝 x₀, ∀ i, dist (F i x₀) (F i x) ≤ b x) : EquicontinuousAt F x₀

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : PseudoMetricSpace α
ι : Type u_4
inst✝ : TopologicalSpace β
x₀ : β
b : β → ℝ
b_lim : Tendsto b (𝓝 x₀) (𝓝 0)
F : ι → β → α
H : ∀ᶠ (x : β) in 𝓝 x₀, ∀ (i : ι), dist (F i x₀) (F i x) ≤ b x
⊢ EquicontinuousAt F x₀

Tactic:
rw [Metric.equicontinuousAt_iff_right]

Result:
α : Type u_1
β : Type u_2
inst✝¹ : PseudoMetricSpace α
ι : Type u_4
inst✝ : TopologicalSpace β
x₀ : β
b : β → ℝ
b_lim : Tendsto b (𝓝 x₀) (𝓝 0)
F : ι → β → α
H : ∀ᶠ (x : β) in 𝓝 x₀, ∀ (i : ι), dist (F i x₀) (F i x) ≤ b x
⊢ ∀ ε > 0, ∀ᶠ (x : β) in 𝓝 x₀, ∀ (i : ι), dist (F i x₀) (F i x) < ε

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : PseudoMetricSpace α
ι : Type u_4
inst✝ : TopologicalSpace β
x₀ : β
b : β → ℝ
b_lim : Tendsto b (𝓝 x₀) (𝓝 0)
F : ι → β → α
H : ∀ᶠ (x : β) in 𝓝 x₀, ∀ (i : ι), dist (F i x₀) (F i x) ≤ b x
⊢ ∀ ε > 0, ∀ᶠ (x : β) in 𝓝 x₀, ∀ (i : ι), dist (F i x₀) (F i x) < ε

Tactic:
intro ε ε0

Result:
α : Type u_1
β : Type u_2
inst✝¹ : PseudoMetricSpace α
ι : Type u_4
inst✝ : TopologicalSpace β
x₀ : β
b : β → ℝ
b_lim : Tendsto b (𝓝 x₀) (𝓝 0)
F : ι → β → α
H : ∀ᶠ (x : β) in 𝓝 x₀, ∀ (i : ι), dist (F i x₀) (F i x) ≤ b x
ε : ℝ
ε0 : ε > 0
⊢ ∀ᶠ (x : β) in 𝓝 x₀, ∀ (i : ι), dist (F i x₀) (F i x) < ε

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : PseudoMetricSpace α
ι : Type u_4
inst✝ : TopologicalSpace β
x₀ : β
b : β → ℝ
b_lim : Tendsto b (𝓝 x₀) (𝓝 0)
F : ι → β → α
H : ∀ᶠ (x : β) in 𝓝 x₀, ∀ (i : ι), dist (F i x₀) (F i x) ≤ b x
ε : ℝ
ε0 : ε > 0
⊢ ∀ᶠ (x : β) in 𝓝 x₀, ∀ (i : ι), dist (F i x₀) (F i x) < ε

Tactic:
filter_upwards [Filter.mem_map.mp <| b_lim (Iio_mem_nhds ε0), H] using
  fun x hx₁ hx₂ i => (hx₂ i).trans_lt hx₁

Result:
no goals
-- Mathlib/Data/PFun.lean
theorem coe_comp (g : β → γ) (f : α → β) : ((g ∘ f : α → γ) : α →. γ) = (g : β →. γ).comp f :=
  ext fun _ _ => by simp only [coe_val, comp_apply, Function.comp, Part.bind_some]

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
g : β → γ
f : α → β
x✝¹ : α
x✝ : γ
⊢ x✝ ∈ ↑(g ∘ f) x✝¹ ↔ x✝ ∈ (↑g).comp (↑f) x✝¹

Tactic:
simp only [coe_val, comp_apply, Function.comp, Part.bind_some]

Result:
no goals
-- Mathlib/Algebra/Ring/Parity.lean
@[deprecated not_even_iff_odd (since := "2024-08-21")]
lemma odd_iff_not_even : Odd n ↔ ¬Even n

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

Tactic:
rw [not_even_iff, odd_iff]

Result:
no goals
-- Mathlib/Tactic/NormNum/BigOperators.lean
lemma List.range_succ_eq_map' {n nn n' : ℕ} (pn : NormNum.IsNat n nn) (pn' : nn = Nat.succ n') :
    List.range n = 0 :: List.map Nat.succ (List.range n')

Proof state:
n nn n' : ℕ
pn : NormNum.IsNat n nn
pn' : nn = n'.succ
⊢ List.range n = 0 :: List.map Nat.succ (List.range n')

Tactic:
rw [pn.out, Nat.cast_id, pn', List.range_succ_eq_map]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem mem_of_mem_erase [EquivBEq α] [LawfulHashable α] (h : m.WF) {k a : α} :
    a ∈ m.erase k → a ∈ m

Proof state:
α : Type u
β : α → Type v
m : Raw α β
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.WF
k a : α
⊢ a ∈ m.erase k → a ∈ m

Tactic:
simpa [mem_iff_contains] using contains_of_contains_erase h

Result:
no goals
-- Mathlib/LinearAlgebra/QuadraticForm/Basic.lean
theorem isOrtho_polarBilin {x y : M} : Q.polarBilin.IsOrtho x y ↔ IsOrtho Q x y

Proof state:
R : Type u_3
M : Type u_4
N : Type u_5
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : AddCommGroup N
inst✝ : Module R N
Q : QuadraticMap R M N
x y : M
⊢ LinearMap.IsOrtho Q.polarBilin x y ↔ Q.IsOrtho x y

Tactic:
simp_rw [isOrtho_def, LinearMap.isOrtho_def, polarBilin_apply_apply, polar, sub_sub, sub_eq_zero]

Result:
no goals
-- Mathlib/CategoryTheory/Abelian/Exact.lean
theorem exact_kernel {X Y : C} (f : X ⟶ Y) :
    (ShortComplex.mk (kernel.ι f) f (by simp)).Exact :=
  exact_of_f_is_kernel _ (kernelIsKernel f)

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Abelian C
S : ShortComplex C
X Y : C
f : X ⟶ Y
⊢ kernel.ι f ≫ f = 0

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Set/Insert.lean
theorem ssubset_iff_insert {s t : Set α} : s ⊂ t ↔ ∃ a ∉ s, insert a s ⊆ t

Proof state:
α : Type u
s t : Set α
⊢ s ⊂ t ↔ ∃ a ∉ s, insert a s ⊆ t

Tactic:
simp only [insert_subset_iff, exists_and_right, ssubset_def, not_subset]

Result:
α : Type u
s t : Set α
⊢ (s ⊆ t ∧ ∃ a ∈ t, a ∉ s) ↔ ∃ a ∉ s, a ∈ t ∧ s ⊆ t

Proof state:
α : Type u
s t : Set α
⊢ (s ⊆ t ∧ ∃ a ∈ t, a ∉ s) ↔ ∃ a ∉ s, a ∈ t ∧ s ⊆ t

Tactic:
aesop

Result:
no goals
-- Mathlib/NumberTheory/NumberField/Embeddings.lean
theorem mult_isComplex (w : {w : InfinitePlace K // IsComplex w}) :
    mult w.1 = 2

Proof state:
K : Type u_2
inst✝ : Field K
w : { w // w.IsComplex }
⊢ (↑w).mult = 2

Tactic:
rw [mult, if_neg (not_isReal_iff_isComplex.mpr w.prop)]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Restrict.lean
theorem volume_preimage_coe (hs : NullMeasurableSet s) (ht : MeasurableSet t) :
    volume (((↑) : s → α) ⁻¹' t) = volume (t ∩ s)

Proof state:
α : Type u_2
inst✝ : MeasureSpace α
s t : Set α
hs : NullMeasurableSet s volume
ht : MeasurableSet t
⊢ volume (Subtype.val ⁻¹' t) = volume (t ∩ s)

Tactic:
rw [volume_set_coe_def,
  comap_apply₀ _ _ Subtype.coe_injective
    (fun h => MeasurableSet.nullMeasurableSet_subtype_coe hs)
    (measurable_subtype_coe ht).nullMeasurableSet,
  image_preimage_eq_inter_range, Subtype.range_coe]

Result:
no goals
-- Mathlib/Topology/Order/IsLUB.lean
theorem exists_seq_tendsto_sSup {α : Type*} [ConditionallyCompleteLinearOrder α]
    [TopologicalSpace α] [OrderTopology α] [FirstCountableTopology α] {S : Set α} (hS : S.Nonempty)
    (hS' : BddAbove S) : ∃ u : ℕ → α, Monotone u ∧ Tendsto u atTop (𝓝 (sSup S)) ∧ ∀ n, u n ∈ S

Proof state:
case intro
α : Type u_3
inst✝³ : ConditionallyCompleteLinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : FirstCountableTopology α
S : Set α
hS : S.Nonempty
hS' : BddAbove S
u : ℕ → α
hu : Monotone u ∧ (∀ (n : ℕ), u n ≤ sSup S) ∧ Tendsto u atTop (𝓝 (sSup S)) ∧ ∀ (n : ℕ), u n ∈ S
⊢ ∃ u, Monotone u ∧ Tendsto u atTop (𝓝 (sSup S)) ∧ ∀ (n : ℕ), u n ∈ S

Tactic:
exact ⟨u, hu.1, hu.2.2⟩

Result:
no goals

Proof state:
α : Type u_3
inst✝³ : ConditionallyCompleteLinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : FirstCountableTopology α
S : Set α
hS : S.Nonempty
hS' : BddAbove S
⊢ ∃ u, Monotone u ∧ Tendsto u atTop (𝓝 (sSup S)) ∧ ∀ (n : ℕ), u n ∈ S

Tactic:
rcases (isLUB_csSup hS hS').exists_seq_monotone_tendsto hS with ⟨u, hu⟩

Result:
case intro
α : Type u_3
inst✝³ : ConditionallyCompleteLinearOrder α
inst✝² : TopologicalSpace α
inst✝¹ : OrderTopology α
inst✝ : FirstCountableTopology α
S : Set α
hS : S.Nonempty
hS' : BddAbove S
u : ℕ → α
hu : Monotone u ∧ (∀ (n : ℕ), u n ≤ sSup S) ∧ Tendsto u atTop (𝓝 (sSup S)) ∧ ∀ (n : ℕ), u n ∈ S
⊢ ∃ u, Monotone u ∧ Tendsto u atTop (𝓝 (sSup S)) ∧ ∀ (n : ℕ), u n ∈ S