harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/MeanInequalities.lean
theorem inner_le_Lp_mul_Lp_of_norm_le_one (f g : ι → ℝ≥0) {p q : ℝ}
    (hpq : p.IsConjExponent q) (hf : ∑ i ∈ s, f i ^ p ≤ 1) (hg : ∑ i ∈ s, g i ^ q ≤ 1) :
    ∑ i ∈ s, f i * g i ≤ 1

Proof state:
ι : Type u
s : Finset ι
f g : ι → ℝ≥0
p q : ℝ
hpq : p.IsConjExponent q
hf : ∑ i ∈ s, f i ^ p ≤ 1
hg : ∑ i ∈ s, g i ^ q ≤ 1
hp : 0 < p.toNNReal
hq : 0 < q.toNNReal
⊢ ∑ i ∈ s, (f i ^ p / p.toNNReal + g i ^ q / q.toNNReal) =
    (∑ i ∈ s, f i ^ p) / p.toNNReal + (∑ i ∈ s, g i ^ q) / q.toNNReal

Tactic:
rw [sum_add_distrib, sum_div, sum_div]

Result:
no goals

Proof state:
ι : Type u
s : Finset ι
f g : ι → ℝ≥0
p q : ℝ
hpq : p.IsConjExponent q
hf : ∑ i ∈ s, f i ^ p ≤ 1
hg : ∑ i ∈ s, g i ^ q ≤ 1
hp : 0 < p.toNNReal
hq : 0 < q.toNNReal
⊢ (∑ i ∈ s, f i ^ p) / p.toNNReal + (∑ i ∈ s, g i ^ q) / q.toNNReal ≤ 1 / p.toNNReal + 1 / q.toNNReal

Tactic:
refine add_le_add ?_ ?_ <;> rwa [div_le_iff₀, div_mul_cancel₀] <;> positivity

Result:
no goals

Proof state:
ι : Type u
s : Finset ι
f g : ι → ℝ≥0
p q : ℝ
hpq : p.IsConjExponent q
hf : ∑ i ∈ s, f i ^ p ≤ 1
hg : ∑ i ∈ s, g i ^ q ≤ 1
hp : 0 < p.toNNReal
⊢ ∑ i ∈ s, f i * g i ≤ 1

Tactic:
have hq : 0 < q.toNNReal := zero_lt_one.trans hpq.toNNReal.symm.one_lt

Result:
ι : Type u
s : Finset ι
f g : ι → ℝ≥0
p q : ℝ
hpq : p.IsConjExponent q
hf : ∑ i ∈ s, f i ^ p ≤ 1
hg : ∑ i ∈ s, g i ^ q ≤ 1
hp : 0 < p.toNNReal
hq : 0 < q.toNNReal
⊢ ∑ i ∈ s, f i * g i ≤ 1

Proof state:
ι : Type u
s : Finset ι
f g : ι → ℝ≥0
p q : ℝ
hpq : p.IsConjExponent q
hf : ∑ i ∈ s, f i ^ p ≤ 1
hg : ∑ i ∈ s, g i ^ q ≤ 1
hp : 0 < p.toNNReal
hq : 0 < q.toNNReal
⊢ 1 / p.toNNReal + 1 / q.toNNReal = 1

Tactic:
simp_rw [one_div, hpq.toNNReal.inv_add_inv_conj]

Result:
no goals

Proof state:
ι : Type u
s : Finset ι
f g : ι → ℝ≥0
p q : ℝ
hpq : p.IsConjExponent q
hf : ∑ i ∈ s, f i ^ p ≤ 1
hg : ∑ i ∈ s, g i ^ q ≤ 1
hp : 0 < p.toNNReal
hq : 0 < q.toNNReal
⊢ ∑ i ∈ s, f i * g i ≤ 1

Tactic:
calc
  ∑ i ∈ s, f i * g i ≤ ∑ i ∈ s, (f i ^ p / Real.toNNReal p + g i ^ q / Real.toNNReal q) :=
    Finset.sum_le_sum fun i _ => young_inequality_real (f i) (g i) hpq
  _ = (∑ i ∈ s, f i ^ p) / Real.toNNReal p + (∑ i ∈ s, g i ^ q) / Real.toNNReal q := by
    rw [sum_add_distrib, sum_div, sum_div]
  _ ≤ 1 / Real.toNNReal p + 1 / Real.toNNReal q := by
    refine add_le_add ?_ ?_ <;> rwa [div_le_iff₀, div_mul_cancel₀] <;> positivity
  _ = 1 := by simp_rw [one_div, hpq.toNNReal.inv_add_inv_conj]

Result:
no goals

Proof state:
ι : Type u
s : Finset ι
f g : ι → ℝ≥0
p q : ℝ
hpq : p.IsConjExponent q
hf : ∑ i ∈ s, f i ^ p ≤ 1
hg : ∑ i ∈ s, g i ^ q ≤ 1
⊢ ∑ i ∈ s, f i * g i ≤ 1

Tactic:
have hp : 0 < p.toNNReal := zero_lt_one.trans hpq.toNNReal.one_lt

Result:
ι : Type u
s : Finset ι
f g : ι → ℝ≥0
p q : ℝ
hpq : p.IsConjExponent q
hf : ∑ i ∈ s, f i ^ p ≤ 1
hg : ∑ i ∈ s, g i ^ q ≤ 1
hp : 0 < p.toNNReal
⊢ ∑ i ∈ s, f i * g i ≤ 1
-- Mathlib/MeasureTheory/Group/Prod.lean
theorem measure_inv_null : μ s⁻¹ = 0 ↔ μ s = 0

Proof state:
G : Type u_1
inst✝⁵ : MeasurableSpace G
inst✝⁴ : Group G
inst✝³ : MeasurableMul₂ G
μ : Measure G
inst✝² : SFinite μ
s : Set G
inst✝¹ : MeasurableInv G
inst✝ : μ.IsMulLeftInvariant
hs : μ s⁻¹ = 0
⊢ μ s⁻¹⁻¹ = 0

Tactic:
exact (quasiMeasurePreserving_inv μ).preimage_null hs

Result:
no goals

Proof state:
G : Type u_1
inst✝⁵ : MeasurableSpace G
inst✝⁴ : Group G
inst✝³ : MeasurableMul₂ G
μ : Measure G
inst✝² : SFinite μ
s : Set G
inst✝¹ : MeasurableInv G
inst✝ : μ.IsMulLeftInvariant
hs : μ s⁻¹ = 0
⊢ μ s = 0

Tactic:
rw [← inv_inv s]

Result:
G : Type u_1
inst✝⁵ : MeasurableSpace G
inst✝⁴ : Group G
inst✝³ : MeasurableMul₂ G
μ : Measure G
inst✝² : SFinite μ
s : Set G
inst✝¹ : MeasurableInv G
inst✝ : μ.IsMulLeftInvariant
hs : μ s⁻¹ = 0
⊢ μ s⁻¹⁻¹ = 0

Proof state:
G : Type u_1
inst✝⁵ : MeasurableSpace G
inst✝⁴ : Group G
inst✝³ : MeasurableMul₂ G
μ : Measure G
inst✝² : SFinite μ
s : Set G
inst✝¹ : MeasurableInv G
inst✝ : μ.IsMulLeftInvariant
⊢ μ s⁻¹ = 0 ↔ μ s = 0

Tactic:
refine ⟨fun hs => ?_, (quasiMeasurePreserving_inv μ).preimage_null⟩

Result:
G : Type u_1
inst✝⁵ : MeasurableSpace G
inst✝⁴ : Group G
inst✝³ : MeasurableMul₂ G
μ : Measure G
inst✝² : SFinite μ
s : Set G
inst✝¹ : MeasurableInv G
inst✝ : μ.IsMulLeftInvariant
hs : μ s⁻¹ = 0
⊢ μ s = 0
-- Mathlib/Topology/MetricSpace/Pseudo/Basic.lean
/-- The preimage of a separable set by an inducing map is separable. -/
protected lemma IsInducing.isSeparable_preimage {f : β → α} [TopologicalSpace β]
    (hf : IsInducing f) {s : Set α} (hs : IsSeparable s) : IsSeparable (f ⁻¹' s)

Proof state:
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
f : β → α
inst✝ : TopologicalSpace β
hf : IsInducing f
s : Set α
hs : IsSeparable s
this : SeparableSpace ↑s
⊢ IsSeparable (f ⁻¹' s)

Tactic:
have : SecondCountableTopology s := UniformSpace.secondCountable_of_separable _

Result:
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
f : β → α
inst✝ : TopologicalSpace β
hf : IsInducing f
s : Set α
hs : IsSeparable s
this✝ : SeparableSpace ↑s
this : SecondCountableTopology ↑s
⊢ IsSeparable (f ⁻¹' s)

Proof state:
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
f : β → α
inst✝ : TopologicalSpace β
hf : IsInducing f
s : Set α
hs : IsSeparable s
⊢ IsSeparable (f ⁻¹' s)

Tactic:
have : SeparableSpace s := hs.separableSpace

Result:
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
f : β → α
inst✝ : TopologicalSpace β
hf : IsInducing f
s : Set α
hs : IsSeparable s
this : SeparableSpace ↑s
⊢ IsSeparable (f ⁻¹' s)

Proof state:
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
f : β → α
inst✝ : TopologicalSpace β
hf : IsInducing f
s : Set α
hs : IsSeparable s
this✝ : SeparableSpace ↑s
this : SecondCountableTopology ↑s
⊢ IsSeparable (f ⁻¹' s)

Tactic:
have : IsInducing ((mapsTo_preimage f s).restrict _ _ _) :=
  (hf.comp IsInducing.subtypeVal).codRestrict _

Result:
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
f : β → α
inst✝ : TopologicalSpace β
hf : IsInducing f
s : Set α
hs : IsSeparable s
this✝¹ : SeparableSpace ↑s
this✝ : SecondCountableTopology ↑s
this : IsInducing (MapsTo.restrict f (f ⁻¹' s) s ⋯)
⊢ IsSeparable (f ⁻¹' s)

Proof state:
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
f : β → α
inst✝ : TopologicalSpace β
hf : IsInducing f
s : Set α
hs : IsSeparable s
this✝¹ : SeparableSpace ↑s
this✝ : SecondCountableTopology ↑s
this : IsInducing (MapsTo.restrict f (f ⁻¹' s) s ⋯)
⊢ IsSeparable (f ⁻¹' s)

Tactic:
have := this.secondCountableTopology

Result:
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
f : β → α
inst✝ : TopologicalSpace β
hf : IsInducing f
s : Set α
hs : IsSeparable s
this✝² : SeparableSpace ↑s
this✝¹ : SecondCountableTopology ↑s
this✝ : IsInducing (MapsTo.restrict f (f ⁻¹' s) s ⋯)
this : SecondCountableTopology ↑(f ⁻¹' s)
⊢ IsSeparable (f ⁻¹' s)

Proof state:
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
f : β → α
inst✝ : TopologicalSpace β
hf : IsInducing f
s : Set α
hs : IsSeparable s
this✝² : SeparableSpace ↑s
this✝¹ : SecondCountableTopology ↑s
this✝ : IsInducing (MapsTo.restrict f (f ⁻¹' s) s ⋯)
this : SecondCountableTopology ↑(f ⁻¹' s)
⊢ IsSeparable (f ⁻¹' s)

Tactic:
exact .of_subtype _

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Arithmetic.lean
theorem lt_mul_of_limit {a b c : Ordinal} (h : IsLimit c) : a < b * c ↔ ∃ c' < c, a < b * c'

Proof state:
a b c : Ordinal.{u_4}
h : c.IsLimit
⊢ a < b * c ↔ ∃ c' < c, a < b * c'

Tactic:
simpa only [not_forall₂, not_le, bex_def] using not_congr (@mul_le_of_limit b c a h)

Result:
no goals
-- Mathlib/Analysis/Calculus/FDeriv/Analytic.lean
theorem HasFPowerSeriesWithinOnBall.fderivWithin [CompleteSpace F]
    (h : HasFPowerSeriesWithinOnBall f p s x r) (hu : UniqueDiffOn 𝕜 (insert x s)) :
    HasFPowerSeriesWithinOnBall (fderivWithin 𝕜 f (insert x s)) p.derivSeries s x r

Proof state:
case refine_1
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0∞
f : E → F
x : E
s : Set E
inst✝ : CompleteSpace F
h : HasFPowerSeriesWithinOnBall f p s x r
hu : UniqueDiffOn 𝕜 (insert x s)
⊢ HasFPowerSeriesWithinOnBall (fun z => (continuousMultilinearCurryFin1 𝕜 E F) (p.changeOrigin (z - x) 1)) p.derivSeries
    s x r

Tactic:
refine continuousMultilinearCurryFin1 𝕜 E F
  |>.toContinuousLinearEquiv.toContinuousLinearMap.comp_hasFPowerSeriesWithinOnBall ?_

Result:
case refine_1
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0∞
f : E → F
x : E
s : Set E
inst✝ : CompleteSpace F
h : HasFPowerSeriesWithinOnBall f p s x r
hu : UniqueDiffOn 𝕜 (insert x s)
⊢ HasFPowerSeriesWithinOnBall (fun z => p.changeOrigin (z - x) 1) (p.changeOriginSeries 1) s x r
-- Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Order.lean
lemma CStarAlgebra.star_mul_le_algebraMap_norm_sq {a : A} :
    star a * a ≤ algebraMap ℝ A (‖a‖ ^ 2)

Proof state:
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
⊢ star a * a ≤ (algebraMap ℝ A) (‖a‖ ^ 2)

Tactic:
have : star a * a ≤ algebraMap ℝ A ‖star a * a‖ := IsSelfAdjoint.le_algebraMap_norm_self

Result:
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
this : star a * a ≤ (algebraMap ℝ A) ‖star a * a‖
⊢ star a * a ≤ (algebraMap ℝ A) (‖a‖ ^ 2)

Proof state:
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
this : star a * a ≤ (algebraMap ℝ A) ‖star a * a‖
⊢ star a * a ≤ (algebraMap ℝ A) (‖a‖ ^ 2)

Tactic:
rwa [CStarRing.norm_star_mul_self, ← pow_two] at this

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Integrals.lean
theorem integral_sin : ∫ x in a..b, sin x = cos a - cos b

Proof state:
case hdiff
a b : ℝ
⊢ ∀ x ∈ [[a, b]], DifferentiableAt ℝ (fun x => -cos x) x

Tactic:
simp only [differentiableAt_neg_iff, differentiableAt_cos, implies_true]

Result:
no goals

Proof state:
case hcont
a b : ℝ
⊢ ContinuousOn sin [[a, b]]

Tactic:
exact continuousOn_sin

Result:
no goals

Proof state:
case hderiv
a b : ℝ
⊢ (deriv fun x => -cos x) = sin

Tactic:
norm_num

Result:
no goals

Proof state:
a b : ℝ
⊢ -cos b - -cos a = cos a - cos b

Tactic:
ring

Result:
no goals

Proof state:
a b : ℝ
⊢ ∫ (x : ℝ) in a..b, sin x = cos a - cos b

Tactic:
rw [integral_deriv_eq_sub' fun x => -cos x]

Result:
a b : ℝ
⊢ -cos b - -cos a = cos a - cos b

case hderiv
a b : ℝ
⊢ (deriv fun x => -cos x) = sin

case hdiff
a b : ℝ
⊢ ∀ x ∈ [[a, b]], DifferentiableAt ℝ (fun x => -cos x) x

case hcont
a b : ℝ
⊢ ContinuousOn sin [[a, b]]
-- Mathlib/Probability/Martingale/Basic.lean
theorem sub (hf : Martingale f ℱ μ) (hg : Martingale g ℱ μ) : Martingale (f - g) ℱ μ

Proof state:
Ω : Type u_1
E : Type u_2
ι : Type u_3
inst✝³ : Preorder ι
m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f g : ι → Ω → E
ℱ : Filtration ι m0
hf : Martingale f ℱ μ
hg : Martingale g ℱ μ
⊢ Martingale (f - g) ℱ μ

Tactic:
rw [sub_eq_add_neg]

Result:
Ω : Type u_1
E : Type u_2
ι : Type u_3
inst✝³ : Preorder ι
m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f g : ι → Ω → E
ℱ : Filtration ι m0
hf : Martingale f ℱ μ
hg : Martingale g ℱ μ
⊢ Martingale (f + -g) ℱ μ

Proof state:
Ω : Type u_1
E : Type u_2
ι : Type u_3
inst✝³ : Preorder ι
m0 : MeasurableSpace Ω
μ : Measure Ω
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f g : ι → Ω → E
ℱ : Filtration ι m0
hf : Martingale f ℱ μ
hg : Martingale g ℱ μ
⊢ Martingale (f + -g) ℱ μ

Tactic:
exact hf.add hg.neg

Result:
no goals
-- Mathlib/Analysis/Complex/CauchyIntegral.lean
theorem analyticOn_iff_differentiableOn {f : ℂ → E} {s : Set ℂ} (o : IsOpen s) :
    AnalyticOn ℂ f s ↔ DifferentiableOn ℂ f s

Proof state:
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
s : Set ℂ
o : IsOpen s
⊢ AnalyticOn ℂ f s ↔ DifferentiableOn ℂ f s

Tactic:
rw [o.analyticOn_iff_analyticOnNhd]

Result:
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
s : Set ℂ
o : IsOpen s
⊢ AnalyticOnNhd ℂ f s ↔ DifferentiableOn ℂ f s

Proof state:
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
s : Set ℂ
o : IsOpen s
⊢ AnalyticOnNhd ℂ f s ↔ DifferentiableOn ℂ f s

Tactic:
exact analyticOnNhd_iff_differentiableOn o

Result:
no goals
-- Mathlib/Data/List/DropRight.lean
@[simp]
lemma rdrop_append_length {l₁ l₂ : List α} :
    List.rdrop (l₁ ++ l₂) (List.length l₂) = l₁

Proof state:
α : Type u_1
l₁ l₂ : List α
⊢ (l₁ ++ l₂).rdrop l₂.length = l₁

Tactic:
rw [rdrop_eq_reverse_drop_reverse, ← length_reverse l₂,
    reverse_append, drop_left, reverse_reverse]

Result:
no goals
-- Mathlib/Order/BooleanAlgebra.lean
theorem sup_inf_inf_sdiff : x ⊓ y ⊓ z ⊔ y \ z = x ⊓ y ⊔ y \ z :=
  calc
    x ⊓ y ⊓ z ⊔ y \ z = x ⊓ (y ⊓ z) ⊔ y \ z

Proof state:
α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ x ⊓ y ⊓ z ⊔ y \ z = x ⊓ (y ⊓ z) ⊔ y \ z

Tactic:
rw [inf_assoc]

Result:
no goals

Proof state:
α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ (x ⊔ y \ z) ⊓ y = x ⊓ y ⊔ y \ z

Tactic:
rw [inf_sup_right, inf_sdiff_left]

Result:
no goals

Proof state:
α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
⊢ x ⊓ (y ⊓ z) ⊔ y \ z = (x ⊔ y \ z) ⊓ y

Tactic:
rw [sup_inf_right, sup_inf_sdiff]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Subgraph.lean
theorem deleteEdges_le_of_le {s s' : Set (Sym2 V)} (h : s ⊆ s') :
    G'.deleteEdges s' ≤ G'.deleteEdges s

Proof state:
V : Type u
G : SimpleGraph V
G' : G.Subgraph
s s' : Set (Sym2 V)
h : s ⊆ s'
⊢ G'.deleteEdges s' ≤ G'.deleteEdges s

Tactic:
constructor <;> simp +contextual only [deleteEdges_verts, deleteEdges_adj,
  true_and, and_imp, subset_rfl]

Result:
case right
V : Type u
G : SimpleGraph V
G' : G.Subgraph
s s' : Set (Sym2 V)
h : s ⊆ s'
⊢ ∀ ⦃v w : V⦄, G'.Adj v w → s(v, w) ∉ s' → s(v, w) ∉ s

Proof state:
case right
V : Type u
G : SimpleGraph V
G' : G.Subgraph
s s' : Set (Sym2 V)
h : s ⊆ s'
⊢ ∀ ⦃v w : V⦄, G'.Adj v w → s(v, w) ∉ s' → s(v, w) ∉ s

Tactic:
exact fun _ _ _ hs' hs ↦ hs' (h hs)

Result:
no goals
-- Mathlib/MeasureTheory/Integral/FundThmCalculus.lean
theorem integral_hasFDerivWithinAt_of_tendsto_ae (hf : IntervalIntegrable f volume a b)
    {s t : Set ℝ} [FTCFilter a (𝓝[s] a) la] [FTCFilter b (𝓝[t] b) lb]
    (hmeas_a : StronglyMeasurableAtFilter f la) (hmeas_b : StronglyMeasurableAtFilter f lb)
    (ha : Tendsto f (la ⊓ ae volume) (𝓝 ca)) (hb : Tendsto f (lb ⊓ ae volume) (𝓝 cb)) :
    HasFDerivWithinAt (fun p : ℝ × ℝ => ∫ x in p.1..p.2, f x)
      ((snd ℝ ℝ ℝ).smulRight cb - (fst ℝ ℝ ℝ).smulRight ca) (s ×ˢ t) (a, b)

Proof state:
case refine_1
E : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : CompleteSpace E
f : ℝ → E
ca cb : E
la lb : Filter ℝ
a b : ℝ
hf : IntervalIntegrable f volume a b
s t : Set ℝ
inst✝¹ : FTCFilter a (𝓝[s] a) la
inst✝ : FTCFilter b (𝓝[t] b) lb
hmeas_a : StronglyMeasurableAtFilter f la volume
hmeas_b : StronglyMeasurableAtFilter f lb volume
ha : Tendsto f (la ⊓ ae volume) (𝓝 ca)
hb : Tendsto f (lb ⊓ ae volume) (𝓝 cb)
this :
  (fun t =>
      ((∫ (x : ℝ) in t.1 ..t.2, f x) - ∫ (x : ℝ) in a..b, f x) - ((t.2 - b) • cb - (t.1 - a) • ca)) =o[𝓝[s] a ×ˢ 𝓝[t] b]
    fun t => ‖t.1 - a‖ + ‖t.2 - b‖
⊢ ∀ (x : ℝ × ℝ),
    ((∫ (x : ℝ) in x.1 ..x.2, f x) - ∫ (x : ℝ) in a..b, f x) - ((x.2 - b) • cb - (x.1 - a) • ca) =
      ((∫ (x : ℝ) in x.1 ..x.2, f x) - ∫ (x : ℝ) in (a, b).1 ..(a, b).2, f x) -
        ((snd ℝ ℝ ℝ).smulRight cb - (fst ℝ ℝ ℝ).smulRight ca) (x - (a, b))

Tactic:
intro x

Result:
case refine_1
E : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : CompleteSpace E
f : ℝ → E
ca cb : E
la lb : Filter ℝ
a b : ℝ
hf : IntervalIntegrable f volume a b
s t : Set ℝ
inst✝¹ : FTCFilter a (𝓝[s] a) la
inst✝ : FTCFilter b (𝓝[t] b) lb
hmeas_a : StronglyMeasurableAtFilter f la volume
hmeas_b : StronglyMeasurableAtFilter f lb volume
ha : Tendsto f (la ⊓ ae volume) (𝓝 ca)
hb : Tendsto f (lb ⊓ ae volume) (𝓝 cb)
this :
  (fun t =>
      ((∫ (x : ℝ) in t.1 ..t.2, f x) - ∫ (x : ℝ) in a..b, f x) - ((t.2 - b) • cb - (t.1 - a) • ca)) =o[𝓝[s] a ×ˢ 𝓝[t] b]
    fun t => ‖t.1 - a‖ + ‖t.2 - b‖
x : ℝ × ℝ
⊢ ((∫ (x : ℝ) in x.1 ..x.2, f x) - ∫ (x : ℝ) in a..b, f x) - ((x.2 - b) • cb - (x.1 - a) • ca) =
    ((∫ (x : ℝ) in x.1 ..x.2, f x) - ∫ (x : ℝ) in (a, b).1 ..(a, b).2, f x) -
      ((snd ℝ ℝ ℝ).smulRight cb - (fst ℝ ℝ ℝ).smulRight ca) (x - (a, b))
-- Mathlib/LinearAlgebra/QuadraticForm/Basic.lean
/-- A version of `QuadraticMap.associated_isSymm` for general targets
(using `flip` because `IsSymm` does not apply here). -/
lemma associated_flip : (associatedHom S Q).flip = associatedHom S Q

Proof state:
S : Type u_1
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
inst✝⁴ : CommSemiring S
inst✝³ : Algebra S R
inst✝² : Module S N
inst✝¹ : IsScalarTower S R N
inst✝ : Invertible 2
Q : QuadraticMap R M N
⊢ LinearMap.flip ((associatedHom S) Q) = (associatedHom S) Q

Tactic:
ext

Result:
case h.h
S : Type u_1
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
inst✝⁴ : CommSemiring S
inst✝³ : Algebra S R
inst✝² : Module S N
inst✝¹ : IsScalarTower S R N
inst✝ : Invertible 2
Q : QuadraticMap R M N
x✝¹ x✝ : M
⊢ ((LinearMap.flip ((associatedHom S) Q)) x✝¹) x✝ = (((associatedHom S) Q) x✝¹) x✝

Proof state:
case h.h
S : Type u_1
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
inst✝⁴ : CommSemiring S
inst✝³ : Algebra S R
inst✝² : Module S N
inst✝¹ : IsScalarTower S R N
inst✝ : Invertible 2
Q : QuadraticMap R M N
x✝¹ x✝ : M
⊢ ((LinearMap.flip ((associatedHom S) Q)) x✝¹) x✝ = (((associatedHom S) Q) x✝¹) x✝

Tactic:
simp only [LinearMap.flip_apply, associated_apply, add_comm, sub_eq_add_neg, add_left_comm,
  add_assoc]

Result:
no goals
-- Mathlib/Analysis/Convex/Deriv.lean
/-- If `f` is convex on `S` and differentiable on `S`, then its derivative within `S` is monotone
on `S`. -/
lemma strictMonoOn_derivWithin (hfc : StrictConvexOn ℝ S f) (hfd : DifferentiableOn ℝ f S) :
    StrictMonoOn (derivWithin f S) S

Proof state:
S : Set ℝ
f : ℝ → ℝ
hfc : StrictConvexOn ℝ S f
hfd : DifferentiableOn ℝ f S
⊢ StrictMonoOn (derivWithin f S) S

Tactic:
intro x hx y hy hxy

Result:
S : Set ℝ
f : ℝ → ℝ
hfc : StrictConvexOn ℝ S f
hfd : DifferentiableOn ℝ f S
x : ℝ
hx : x ∈ S
y : ℝ
hy : y ∈ S
hxy : x < y
⊢ derivWithin f S x < derivWithin f S y

Proof state:
S : Set ℝ
f : ℝ → ℝ
hfc : StrictConvexOn ℝ S f
hfd : DifferentiableOn ℝ f S
x : ℝ
hx : x ∈ S
y : ℝ
hy : y ∈ S
hxy : x < y
⊢ derivWithin f S x < derivWithin f S y

Tactic:
exact (hfc.derivWithin_lt_slope hx hy hxy (hfd x hx)).trans
  (hfc.slope_lt_derivWithin hx hy hxy (hfd y hy))

Result:
no goals
-- Mathlib/RingTheory/SurjectiveOnStalks.lean
lemma SurjectiveOnStalks.of_comp (hg : SurjectiveOnStalks (g.comp f)) :
    SurjectiveOnStalks g

Proof state:
R : Type u_1
inst✝² : CommRing R
S : Type u_2
inst✝¹ : CommRing S
T : Type u_3
inst✝ : CommRing T
g : S →+* T
f : R →+* S
hg : (g.comp f).SurjectiveOnStalks
I : Ideal T
hI : I.IsPrime
this :
  Function.Surjective
    (⇑(Localization.localRingHom (Ideal.comap g I) I g ⋯) ∘
      ⇑(Localization.localRingHom (Ideal.comap (g.comp f) I) (Ideal.comap g I) f ⋯))
⊢ Function.Surjective ⇑(Localization.localRingHom (Ideal.comap g I) I g ⋯)

Tactic:
exact this.of_comp

Result:
no goals

Proof state:
R : Type u_1
inst✝² : CommRing R
S : Type u_2
inst✝¹ : CommRing S
T : Type u_3
inst✝ : CommRing T
g : S →+* T
f : R →+* S
hg : (g.comp f).SurjectiveOnStalks
I : Ideal T
hI : I.IsPrime
this : Function.Surjective ⇑(Localization.localRingHom (Ideal.comap (g.comp f) I) I (g.comp f) ⋯)
⊢ Function.Surjective ⇑(Localization.localRingHom (Ideal.comap g I) I g ⋯)

Tactic:
rw [Localization.localRingHom_comp (I.comap (g.comp f)) (I.comap g) _ _ rfl _ rfl,
  RingHom.coe_comp] at this

Result:
R : Type u_1
inst✝² : CommRing R
S : Type u_2
inst✝¹ : CommRing S
T : Type u_3
inst✝ : CommRing T
g : S →+* T
f : R →+* S
hg : (g.comp f).SurjectiveOnStalks
I : Ideal T
hI : I.IsPrime
this :
  Function.Surjective
    (⇑(Localization.localRingHom (Ideal.comap g I) I g ⋯) ∘
      ⇑(Localization.localRingHom (Ideal.comap (g.comp f) I) (Ideal.comap g I) f ⋯))
⊢ Function.Surjective ⇑(Localization.localRingHom (Ideal.comap g I) I g ⋯)

Proof state:
R : Type u_1
inst✝² : CommRing R
S : Type u_2
inst✝¹ : CommRing S
T : Type u_3
inst✝ : CommRing T
g : S →+* T
f : R →+* S
hg : (g.comp f).SurjectiveOnStalks
⊢ g.SurjectiveOnStalks

Tactic:
intros I hI

Result:
R : Type u_1
inst✝² : CommRing R
S : Type u_2
inst✝¹ : CommRing S
T : Type u_3
inst✝ : CommRing T
g : S →+* T
f : R →+* S
hg : (g.comp f).SurjectiveOnStalks
I : Ideal T
hI : I.IsPrime
⊢ Function.Surjective ⇑(Localization.localRingHom (Ideal.comap g I) I g ⋯)

Proof state:
R : Type u_1
inst✝² : CommRing R
S : Type u_2
inst✝¹ : CommRing S
T : Type u_3
inst✝ : CommRing T
g : S →+* T
f : R →+* S
hg : (g.comp f).SurjectiveOnStalks
I : Ideal T
hI : I.IsPrime
⊢ Function.Surjective ⇑(Localization.localRingHom (Ideal.comap g I) I g ⋯)

Tactic:
have := hg I hI

Result:
R : Type u_1
inst✝² : CommRing R
S : Type u_2
inst✝¹ : CommRing S
T : Type u_3
inst✝ : CommRing T
g : S →+* T
f : R →+* S
hg : (g.comp f).SurjectiveOnStalks
I : Ideal T
hI : I.IsPrime
this : Function.Surjective ⇑(Localization.localRingHom (Ideal.comap (g.comp f) I) I (g.comp f) ⋯)
⊢ Function.Surjective ⇑(Localization.localRingHom (Ideal.comap g I) I g ⋯)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem add_sub_cancel (x y : BitVec w) : x + y - y = x

Proof state:
case a
w : Nat
x y : BitVec w
y_toNat_le : y.toNat ≤ 2 ^ w
⊢ (x + y - y).toNat = x.toNat

Tactic:
rw [toNat_sub, toNat_add, Nat.add_comm, Nat.mod_add_mod, Nat.add_assoc, ← Nat.add_sub_assoc y_toNat_le,
    Nat.add_sub_cancel_left, Nat.add_mod_right, toNat_mod_cancel]

Result:
no goals

Proof state:
w : Nat
x y : BitVec w
⊢ x + y - y = x

Tactic:
apply eq_of_toNat_eq

Result:
case a
w : Nat
x y : BitVec w
⊢ (x + y - y).toNat = x.toNat

Proof state:
case a
w : Nat
x y : BitVec w
⊢ (x + y - y).toNat = x.toNat

Tactic:
have y_toNat_le := Nat.le_of_lt y.isLt

Result:
case a
w : Nat
x y : BitVec w
y_toNat_le : y.toNat ≤ 2 ^ w
⊢ (x + y - y).toNat = x.toNat
-- Mathlib/SetTheory/Cardinal/Basic.lean
theorem exists_finset_le_card (α : Type*) (n : ℕ) (h : n ≤ #α) :
    ∃ s : Finset α, n ≤ s.card

Proof state:
case inr
α : Type u_1
n : ℕ
h : ↑n ≤ #α
hα : Infinite α
⊢ ∃ s, n ≤ s.card

Tactic:
obtain ⟨s, hs⟩ := Infinite.exists_subset_card_eq α n

Result:
case inr.intro
α : Type u_1
n : ℕ
h : ↑n ≤ #α
hα : Infinite α
s : Finset α
hs : s.card = n
⊢ ∃ s, n ≤ s.card

Proof state:
α : Type u_1
n : ℕ
h : ↑n ≤ #α
⊢ ∃ s, n ≤ s.card

Tactic:
obtain hα|hα := finite_or_infinite α

Result:
case inl
α : Type u_1
n : ℕ
h : ↑n ≤ #α
hα : Finite α
⊢ ∃ s, n ≤ s.card

case inr
α : Type u_1
n : ℕ
h : ↑n ≤ #α
hα : Infinite α
⊢ ∃ s, n ≤ s.card

Proof state:
case inr.intro
α : Type u_1
n : ℕ
h : ↑n ≤ #α
hα : Infinite α
s : Finset α
hs : s.card = n
⊢ ∃ s, n ≤ s.card

Tactic:
exact ⟨s, hs.ge⟩

Result:
no goals

Proof state:
case inl
α : Type u_1
n : ℕ
h : ↑n ≤ #α
hα✝ : Finite α
hα : Fintype α := Fintype.ofFinite α
⊢ ∃ s, n ≤ s.card

Tactic:
use Finset.univ

Result:
case h
α : Type u_1
n : ℕ
h : ↑n ≤ #α
hα✝ : Finite α
hα : Fintype α := Fintype.ofFinite α
⊢ n ≤ Finset.univ.card

Proof state:
case h
α : Type u_1
n : ℕ
h : ↑n ≤ #α
hα✝ : Finite α
hα : Fintype α := Fintype.ofFinite α
⊢ n ≤ Finset.univ.card

Tactic:
simpa only [mk_fintype, Nat.cast_le] using h

Result:
no goals

Proof state:
case inl
α : Type u_1
n : ℕ
h : ↑n ≤ #α
hα : Finite α
⊢ ∃ s, n ≤ s.card

Tactic:
let hα := Fintype.ofFinite α

Result:
case inl
α : Type u_1
n : ℕ
h : ↑n ≤ #α
hα✝ : Finite α
hα : Fintype α := Fintype.ofFinite α
⊢ ∃ s, n ≤ s.card