harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/CategoryTheory/Monoidal/Rigid/Basic.lean
theorem rightAdjointMate_comp {X Y Z : C} [HasRightDual X] [HasRightDual Y] {f : X ⟶ Y}
    {g : Xᘁ ⟶ Z} :
    fᘁ ≫ g =
      (ρ_ (Yᘁ)).inv ≫
        _ ◁ η_ X (Xᘁ) ≫ _ ◁ (f ⊗ g) ≫ (α_ (Yᘁ) Y Z).inv ≫ ε_ Y (Yᘁ) ▷ _ ≫ (λ_ Z).hom :=
  calc
    _ = 𝟙 _ ⊗≫ (Yᘁ : C) ◁ η_ X Xᘁ ≫ Yᘁ ◁ f ▷ Xᘁ ⊗≫ (ε_ Y Yᘁ ▷ Xᘁ ≫ 𝟙_ C ◁ g) ⊗≫ 𝟙 _

Proof state:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
X Y Z : C
inst✝¹ : HasRightDual X
inst✝ : HasRightDual Y
f : X ⟶ Y
g : Xᘁ ⟶ Z
⊢ fᘁ ≫ g = 𝟙 Yᘁ ⊗≫ Yᘁ ◁ η_ X Xᘁ ≫ Yᘁ ◁ f ▷ Xᘁ ⊗≫ (ε_ Y Yᘁ ▷ Xᘁ ≫ 𝟙_ C ◁ g) ⊗≫ 𝟙 Z

Tactic:
dsimp only [rightAdjointMate]

Result:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
X Y Z : C
inst✝¹ : HasRightDual X
inst✝ : HasRightDual Y
f : X ⟶ Y
g : Xᘁ ⟶ Z
⊢ ((ρ_ Yᘁ).inv ≫ Yᘁ ◁ η_ X Xᘁ ≫ Yᘁ ◁ f ▷ Xᘁ ≫ (α_ Yᘁ Y Xᘁ).inv ≫ ε_ Y Yᘁ ▷ Xᘁ ≫ (λ_ Xᘁ).hom) ≫ g =
    𝟙 Yᘁ ⊗≫ Yᘁ ◁ η_ X Xᘁ ≫ Yᘁ ◁ f ▷ Xᘁ ⊗≫ (ε_ Y Yᘁ ▷ Xᘁ ≫ 𝟙_ C ◁ g) ⊗≫ 𝟙 Z

Proof state:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
X Y Z : C
inst✝¹ : HasRightDual X
inst✝ : HasRightDual Y
f : X ⟶ Y
g : Xᘁ ⟶ Z
⊢ 𝟙 Yᘁ ⊗≫ Yᘁ ◁ η_ X Xᘁ ≫ Yᘁ ◁ f ▷ Xᘁ ⊗≫ (ε_ Y Yᘁ ▷ Xᘁ ≫ 𝟙_ C ◁ g) ⊗≫ 𝟙 Z =
    (ρ_ Yᘁ).inv ≫ Yᘁ ◁ η_ X Xᘁ ≫ Yᘁ ◁ (f ⊗ g) ≫ (α_ Yᘁ Y Z).inv ≫ ε_ Y Yᘁ ▷ Z ≫ (λ_ Z).hom

Tactic:
rw [← whisker_exchange, tensorHom_def]

Result:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
X Y Z : C
inst✝¹ : HasRightDual X
inst✝ : HasRightDual Y
f : X ⟶ Y
g : Xᘁ ⟶ Z
⊢ 𝟙 Yᘁ ⊗≫ Yᘁ ◁ η_ X Xᘁ ≫ Yᘁ ◁ f ▷ Xᘁ ⊗≫ ((Yᘁ ⊗ Y) ◁ g ≫ ε_ Y Yᘁ ▷ Z) ⊗≫ 𝟙 Z =
    (ρ_ Yᘁ).inv ≫ Yᘁ ◁ η_ X Xᘁ ≫ Yᘁ ◁ (f ▷ Xᘁ ≫ Y ◁ g) ≫ (α_ Yᘁ Y Z).inv ≫ ε_ Y Yᘁ ▷ Z ≫ (λ_ Z).hom

Proof state:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
X Y Z : C
inst✝¹ : HasRightDual X
inst✝ : HasRightDual Y
f : X ⟶ Y
g : Xᘁ ⟶ Z
⊢ 𝟙 Yᘁ ⊗≫ Yᘁ ◁ η_ X Xᘁ ≫ Yᘁ ◁ f ▷ Xᘁ ⊗≫ ((Yᘁ ⊗ Y) ◁ g ≫ ε_ Y Yᘁ ▷ Z) ⊗≫ 𝟙 Z =
    (ρ_ Yᘁ).inv ≫ Yᘁ ◁ η_ X Xᘁ ≫ Yᘁ ◁ (f ▷ Xᘁ ≫ Y ◁ g) ≫ (α_ Yᘁ Y Z).inv ≫ ε_ Y Yᘁ ▷ Z ≫ (λ_ Z).hom

Tactic:
monoidal

Result:
no goals

Proof state:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
X Y Z : C
inst✝¹ : HasRightDual X
inst✝ : HasRightDual Y
f : X ⟶ Y
g : Xᘁ ⟶ Z
⊢ ((ρ_ Yᘁ).inv ≫ Yᘁ ◁ η_ X Xᘁ ≫ Yᘁ ◁ f ▷ Xᘁ ≫ (α_ Yᘁ Y Xᘁ).inv ≫ ε_ Y Yᘁ ▷ Xᘁ ≫ (λ_ Xᘁ).hom) ≫ g =
    𝟙 Yᘁ ⊗≫ Yᘁ ◁ η_ X Xᘁ ≫ Yᘁ ◁ f ▷ Xᘁ ⊗≫ (ε_ Y Yᘁ ▷ Xᘁ ≫ 𝟙_ C ◁ g) ⊗≫ 𝟙 Z

Tactic:
monoidal

Result:
no goals
-- Mathlib/NumberTheory/LSeries/Dirichlet.lean
/-- The L-series of the arithmetic function `ζ` does not vanish on the right half-plane
`re s > 1`. -/
lemma LSeries_zeta_ne_zero_of_one_lt_re {s : ℂ} (hs : 1 < s.re) : L ↗ζ s ≠ 0 :=
  fun h ↦ by simpa [h, -zeta_apply] using LSeries_zeta_mul_Lseries_moebius hs

Proof state:
s : ℂ
hs : 1 < s.re
h : L (fun n => ↑(ζ n)) s = 0
⊢ False

Tactic:
simpa [h, -zeta_apply] using LSeries_zeta_mul_Lseries_moebius hs

Result:
no goals
-- Mathlib/CategoryTheory/Localization/Predicate.lean
theorem liftNatTrans_id (F : C ⥤ E) (F' : D ⥤ E) [h : Lifting L W F F'] :
    liftNatTrans L W F F F' F' (𝟙 F) = 𝟙 F' :=
  natTrans_ext L W fun X => by
    simp only [liftNatTrans_app, NatTrans.id_app, id_comp, Iso.hom_inv_id_app]
    rfl

Proof state:
C : Type u_1
D : Type u_2
inst✝³ : Category.{u_4, u_1} C
inst✝² : Category.{u_6, u_2} D
L : C ⥤ D
W : MorphismProperty C
E : Type u_3
inst✝¹ : Category.{u_5, u_3} E
inst✝ : L.IsLocalization W
F : C ⥤ E
F' : D ⥤ E
h : Lifting L W F F'
X : C
⊢ (liftNatTrans L W F F F' F' (𝟙 F)).app (L.obj X) = (𝟙 F').app (L.obj X)

Tactic:
simp only [liftNatTrans_app, NatTrans.id_app, id_comp, Iso.hom_inv_id_app]

Result:
C : Type u_1
D : Type u_2
inst✝³ : Category.{u_4, u_1} C
inst✝² : Category.{u_6, u_2} D
L : C ⥤ D
W : MorphismProperty C
E : Type u_3
inst✝¹ : Category.{u_5, u_3} E
inst✝ : L.IsLocalization W
F : C ⥤ E
F' : D ⥤ E
h : Lifting L W F F'
X : C
⊢ 𝟙 ((L ⋙ F').obj X) = 𝟙 (F'.obj (L.obj X))

Proof state:
C : Type u_1
D : Type u_2
inst✝³ : Category.{u_4, u_1} C
inst✝² : Category.{u_6, u_2} D
L : C ⥤ D
W : MorphismProperty C
E : Type u_3
inst✝¹ : Category.{u_5, u_3} E
inst✝ : L.IsLocalization W
F : C ⥤ E
F' : D ⥤ E
h : Lifting L W F F'
X : C
⊢ 𝟙 ((L ⋙ F').obj X) = 𝟙 (F'.obj (L.obj X))

Tactic:
rfl

Result:
no goals
-- Mathlib/Topology/List.lean
theorem tendsto_prod [Monoid α] [ContinuousMul α] {l : List α} :
    Tendsto List.prod (𝓝 l) (𝓝 l.prod)

Proof state:
case cons
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : Monoid α
inst✝ : ContinuousMul α
x : α
l : List α
ih : Tendsto prod (𝓝 l) (𝓝 l.prod)
⊢ Tendsto prod (𝓝 (x :: l)) (𝓝 (x :: l).prod)

Tactic:
simp_rw [tendsto_cons_iff, prod_cons]

Result:
case cons
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : Monoid α
inst✝ : ContinuousMul α
x : α
l : List α
ih : Tendsto prod (𝓝 l) (𝓝 l.prod)
⊢ Tendsto (fun p => p.1 * p.2.prod) (𝓝 x ×ˢ 𝓝 l) (𝓝 (x * l.prod))

Proof state:
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : Monoid α
inst✝ : ContinuousMul α
l : List α
⊢ Tendsto prod (𝓝 l) (𝓝 l.prod)

Tactic:
induction l with
| nil => simp +contextual [nhds_nil, mem_of_mem_nhds, tendsto_pure_left]
| cons x l ih =>
  simp_rw [tendsto_cons_iff, prod_cons]
  have := continuous_iff_continuousAt.mp continuous_mul (x, l.prod)
  rw [ContinuousAt, nhds_prod_eq] at this
  exact this.comp (tendsto_id.prod_map ih)

Result:
no goals

Proof state:
case cons
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : Monoid α
inst✝ : ContinuousMul α
x : α
l : List α
ih : Tendsto prod (𝓝 l) (𝓝 l.prod)
this : Tendsto (fun p => p.1 * p.2) (𝓝 x ×ˢ 𝓝 l.prod) (𝓝 ((x, l.prod).1 * (x, l.prod).2))
⊢ Tendsto (fun p => p.1 * p.2.prod) (𝓝 x ×ˢ 𝓝 l) (𝓝 (x * l.prod))

Tactic:
exact this.comp (tendsto_id.prod_map ih)

Result:
no goals

Proof state:
case cons
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : Monoid α
inst✝ : ContinuousMul α
x : α
l : List α
ih : Tendsto prod (𝓝 l) (𝓝 l.prod)
this : ContinuousAt (fun p => p.1 * p.2) (x, l.prod)
⊢ Tendsto (fun p => p.1 * p.2.prod) (𝓝 x ×ˢ 𝓝 l) (𝓝 (x * l.prod))

Tactic:
rw [ContinuousAt, nhds_prod_eq] at this

Result:
case cons
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : Monoid α
inst✝ : ContinuousMul α
x : α
l : List α
ih : Tendsto prod (𝓝 l) (𝓝 l.prod)
this : Tendsto (fun p => p.1 * p.2) (𝓝 x ×ˢ 𝓝 l.prod) (𝓝 ((x, l.prod).1 * (x, l.prod).2))
⊢ Tendsto (fun p => p.1 * p.2.prod) (𝓝 x ×ˢ 𝓝 l) (𝓝 (x * l.prod))

Proof state:
case cons
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : Monoid α
inst✝ : ContinuousMul α
x : α
l : List α
ih : Tendsto prod (𝓝 l) (𝓝 l.prod)
⊢ Tendsto (fun p => p.1 * p.2.prod) (𝓝 x ×ˢ 𝓝 l) (𝓝 (x * l.prod))

Tactic:
have := continuous_iff_continuousAt.mp continuous_mul (x, l.prod)

Result:
case cons
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : Monoid α
inst✝ : ContinuousMul α
x : α
l : List α
ih : Tendsto prod (𝓝 l) (𝓝 l.prod)
this : ContinuousAt (fun p => p.1 * p.2) (x, l.prod)
⊢ Tendsto (fun p => p.1 * p.2.prod) (𝓝 x ×ˢ 𝓝 l) (𝓝 (x * l.prod))

Proof state:
case nil
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : Monoid α
inst✝ : ContinuousMul α
⊢ Tendsto prod (𝓝 []) (𝓝 [].prod)

Tactic:
simp +contextual [nhds_nil, mem_of_mem_nhds, tendsto_pure_left]

Result:
no goals
-- Mathlib/CategoryTheory/Iso.lean
theorem inv_inv [IsIso f] : inv (inv f) = f

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst✝ : IsIso f
⊢ inv (inv f) = f

Tactic:
apply inv_eq_of_hom_inv_id

Result:
case hom_inv_id
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst✝ : IsIso f
⊢ inv f ≫ f = 𝟙 Y

Proof state:
case hom_inv_id
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst✝ : IsIso f
⊢ inv f ≫ f = 𝟙 Y

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/Analytic/Basic.lean
theorem partialSum_continuous (p : FormalMultilinearSeries 𝕜 E F) (n : ℕ) :
    Continuous (p.partialSum n)

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝¹⁰ : Semiring 𝕜
inst✝⁹ : AddCommMonoid E
inst✝⁸ : AddCommMonoid F
inst✝⁷ : Module 𝕜 E
inst✝⁶ : Module 𝕜 F
inst✝⁵ : TopologicalSpace E
inst✝⁴ : TopologicalSpace F
inst✝³ : ContinuousAdd E
inst✝² : ContinuousAdd F
inst✝¹ : ContinuousConstSMul 𝕜 E
inst✝ : ContinuousConstSMul 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
n : ℕ
⊢ Continuous (p.partialSum n)

Tactic:
unfold partialSum

Result:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝¹⁰ : Semiring 𝕜
inst✝⁹ : AddCommMonoid E
inst✝⁸ : AddCommMonoid F
inst✝⁷ : Module 𝕜 E
inst✝⁶ : Module 𝕜 F
inst✝⁵ : TopologicalSpace E
inst✝⁴ : TopologicalSpace F
inst✝³ : ContinuousAdd E
inst✝² : ContinuousAdd F
inst✝¹ : ContinuousConstSMul 𝕜 E
inst✝ : ContinuousConstSMul 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
n : ℕ
⊢ Continuous fun x => ∑ k ∈ Finset.range n, (p k) fun x_1 => x

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝¹⁰ : Semiring 𝕜
inst✝⁹ : AddCommMonoid E
inst✝⁸ : AddCommMonoid F
inst✝⁷ : Module 𝕜 E
inst✝⁶ : Module 𝕜 F
inst✝⁵ : TopologicalSpace E
inst✝⁴ : TopologicalSpace F
inst✝³ : ContinuousAdd E
inst✝² : ContinuousAdd F
inst✝¹ : ContinuousConstSMul 𝕜 E
inst✝ : ContinuousConstSMul 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
n : ℕ
⊢ Continuous fun x => ∑ k ∈ Finset.range n, (p k) fun x_1 => x

Tactic:
continuity

Result:
no goals
-- Mathlib/Data/Finset/Lattice/Basic.lean
@[simp] lemma right_eq_union : s = t ∪ s ↔ t ⊆ s

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
⊢ s = t ∪ s ↔ t ⊆ s

Tactic:
rw [eq_comm, union_eq_right]

Result:
no goals
-- Mathlib/MeasureTheory/Function/AEEqOfLIntegral.lean
theorem ae_eq_of_forall_setLIntegral_eq_of_sigmaFinite₀ [SigmaFinite μ]
    {f g : α → ℝ≥0∞} (hf : AEMeasurable f μ) (hg : AEMeasurable g μ)
    (h : ∀ s, MeasurableSet s → μ s < ∞ → ∫⁻ x in s, f x ∂μ = ∫⁻ x in s, g x ∂μ) : f =ᵐ[μ] g

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
h : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∫⁻ (x : α) in s, f x ∂μ = ∫⁻ (x : α) in s, g x ∂μ
A : f ≤ᶠ[ae μ] g
B : g ≤ᶠ[ae μ] f
⊢ f =ᶠ[ae μ] g

Tactic:
filter_upwards [A, B] with x using le_antisymm

Result:
no goals

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
h : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∫⁻ (x : α) in s, f x ∂μ = ∫⁻ (x : α) in s, g x ∂μ
A : f ≤ᶠ[ae μ] g
⊢ f =ᶠ[ae μ] g

Tactic:
have B : g ≤ᵐ[μ] f :=
  ae_le_of_forall_setLIntegral_le_of_sigmaFinite₀ hg fun s hs h's => ge_of_eq (h s hs h's)

Result:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
h : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∫⁻ (x : α) in s, f x ∂μ = ∫⁻ (x : α) in s, g x ∂μ
A : f ≤ᶠ[ae μ] g
B : g ≤ᶠ[ae μ] f
⊢ f =ᶠ[ae μ] g

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
h : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∫⁻ (x : α) in s, f x ∂μ = ∫⁻ (x : α) in s, g x ∂μ
⊢ f =ᶠ[ae μ] g

Tactic:
have A : f ≤ᵐ[μ] g :=
  ae_le_of_forall_setLIntegral_le_of_sigmaFinite₀ hf fun s hs h's => le_of_eq (h s hs h's)

Result:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : SigmaFinite μ
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
h : ∀ (s : Set α), MeasurableSet s → μ s < ⊤ → ∫⁻ (x : α) in s, f x ∂μ = ∫⁻ (x : α) in s, g x ∂μ
A : f ≤ᶠ[ae μ] g
⊢ f =ᶠ[ae μ] g
-- Mathlib/Algebra/Order/ToIntervalMod.lean
theorem toIocDiv_sub_eq_toIocDiv_add' (a b c : α) :
    toIocDiv hp (a - c) b = toIocDiv hp a (b + c)

Proof state:
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
hα : Archimedean α
p : α
hp : 0 < p
a b c : α
⊢ toIocDiv hp (a - c) b = toIocDiv hp a (b + c)

Tactic:
rw [← sub_neg_eq_add, toIocDiv_sub_eq_toIocDiv_add, sub_eq_add_neg]

Result:
no goals
-- Mathlib/Analysis/Convex/Between.lean
theorem sbtw_one_zero_iff {x : R} : Sbtw R 1 x 0 ↔ x ∈ Set.Ioo (0 : R) 1

Proof state:
R : Type u_1
inst✝ : OrderedRing R
x : R
⊢ Sbtw R 1 x 0 ↔ x ∈ Set.Ioo 0 1

Tactic:
rw [sbtw_comm, sbtw_zero_one_iff]

Result:
no goals
-- Mathlib/Topology/Basic.lean
theorem tendsto_atTop_nhds [Nonempty α] [SemilatticeSup α] {f : α → X} :
    Tendsto f atTop (𝓝 x) ↔ ∀ U : Set X, x ∈ U → IsOpen U → ∃ N, ∀ n, N ≤ n → f n ∈ U :=
  (atTop_basis.tendsto_iff (nhds_basis_opens x)).trans <| by
    simp only [and_imp, exists_prop, true_and, mem_Ici]

Proof state:
X : Type u
α : Type u_1
x : X
inst✝² : TopologicalSpace X
inst✝¹ : Nonempty α
inst✝ : SemilatticeSup α
f : α → X
⊢ (∀ (ib : Set X), x ∈ ib ∧ IsOpen ib → ∃ ia, True ∧ ∀ x ∈ Ici ia, f x ∈ ib) ↔
    ∀ (U : Set X), x ∈ U → IsOpen U → ∃ N, ∀ (n : α), N ≤ n → f n ∈ U

Tactic:
simp only [and_imp, exists_prop, true_and, mem_Ici]

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/RBMap/Lemmas.lean
theorem Ordered.lt_upperBound? [@TransCmp α cmp] [IsStrictCut cmp cut] (ht : Ordered cmp t)
    (H : t.upperBound? cut = some x) (hy : y ∈ t) : cmp y x = .lt ↔ cut y = .gt

Proof state:
α : Type u_1
cmp : α → α → Ordering
cut : α → Ordering
t : RBNode α
x y : α
inst✝¹ : TransCmp cmp
inst✝ : IsStrictCut cmp cut
ht : Ordered cmp t
H : upperBound? cut t = some x
hy : y ∈ t
⊢ cmp y x = Ordering.lt ↔ cut y = Ordering.gt

Tactic:
rw [← reverse_reverse t, upperBound?_reverse] at H

Result:
α : Type u_1
cmp : α → α → Ordering
cut : α → Ordering
t : RBNode α
x y : α
inst✝¹ : TransCmp cmp
inst✝ : IsStrictCut cmp cut
ht : Ordered cmp t
H : lowerBound? (fun x => (cut x).swap) t.reverse = some x
hy : y ∈ t
⊢ cmp y x = Ordering.lt ↔ cut y = Ordering.gt

Proof state:
α : Type u_1
cmp : α → α → Ordering
cut : α → Ordering
t : RBNode α
x y : α
inst✝¹ : TransCmp cmp
inst✝ : IsStrictCut cmp cut
ht : Ordered cmp t
H : lowerBound? (fun x => (cut x).swap) t.reverse = some x
hy : y ∈ t
⊢ cmp y x = Ordering.lt ↔ cut y = Ordering.gt

Tactic:
rw [← Ordering.swap_inj (o₂ := .gt)]

Result:
α : Type u_1
cmp : α → α → Ordering
cut : α → Ordering
t : RBNode α
x y : α
inst✝¹ : TransCmp cmp
inst✝ : IsStrictCut cmp cut
ht : Ordered cmp t
H : lowerBound? (fun x => (cut x).swap) t.reverse = some x
hy : y ∈ t
⊢ cmp y x = Ordering.lt ↔ (cut y).swap = Ordering.gt.swap

Proof state:
α : Type u_1
cmp : α → α → Ordering
cut : α → Ordering
t : RBNode α
x y : α
inst✝¹ : TransCmp cmp
inst✝ : IsStrictCut cmp cut
ht : Ordered cmp t
H : lowerBound? (fun x => (cut x).swap) t.reverse = some x
⊢ y ∈ t → (cmp y x = Ordering.lt ↔ (cut y).swap = Ordering.gt.swap)

Tactic:
simpa [-Ordering.swap_inj] using ht.reverse.lowerBound?_lt H

Result:
no goals

Proof state:
α : Type u_1
cmp : α → α → Ordering
cut : α → Ordering
t : RBNode α
x y : α
inst✝¹ : TransCmp cmp
inst✝ : IsStrictCut cmp cut
ht : Ordered cmp t
H : lowerBound? (fun x => (cut x).swap) t.reverse = some x
hy : y ∈ t
⊢ cmp y x = Ordering.lt ↔ (cut y).swap = Ordering.gt.swap

Tactic:
revert hy

Result:
α : Type u_1
cmp : α → α → Ordering
cut : α → Ordering
t : RBNode α
x y : α
inst✝¹ : TransCmp cmp
inst✝ : IsStrictCut cmp cut
ht : Ordered cmp t
H : lowerBound? (fun x => (cut x).swap) t.reverse = some x
⊢ y ∈ t → (cmp y x = Ordering.lt ↔ (cut y).swap = Ordering.gt.swap)
-- Mathlib/MeasureTheory/Integral/IntegrableOn.lean
theorem integrableAtFilter_atBot_iff [Preorder α] [IsDirected α fun (x1 x2 : α) => x1 ≥ x2]
    [Nonempty α] :
    IntegrableAtFilter f atBot μ ↔ ∃ a, IntegrableOn f (Iic a) μ

Proof state:
α : Type u_1
E : Type u_4
inst✝⁴ : MeasurableSpace α
inst✝³ : NormedAddCommGroup E
f : α → E
μ : Measure α
inst✝² : Preorder α
inst✝¹ : IsDirected α fun x1 x2 => x1 ≥ x2
inst✝ : Nonempty α
⊢ IntegrableAtFilter f atBot μ ↔ ∃ a, IntegrableOn f (Iic a) μ

Tactic:
refine ⟨fun ⟨s, hs, hi⟩ ↦ ?_, fun ⟨a, ha⟩ ↦ ⟨Iic a, Iic_mem_atBot a, ha⟩⟩

Result:
α : Type u_1
E : Type u_4
inst✝⁴ : MeasurableSpace α
inst✝³ : NormedAddCommGroup E
f : α → E
μ : Measure α
inst✝² : Preorder α
inst✝¹ : IsDirected α fun x1 x2 => x1 ≥ x2
inst✝ : Nonempty α
x✝ : IntegrableAtFilter f atBot μ
s : Set α
hs : s ∈ atBot
hi : IntegrableOn f s μ
⊢ ∃ a, IntegrableOn f (Iic a) μ

Proof state:
α : Type u_1
E : Type u_4
inst✝⁴ : MeasurableSpace α
inst✝³ : NormedAddCommGroup E
f : α → E
μ : Measure α
inst✝² : Preorder α
inst✝¹ : IsDirected α fun x1 x2 => x1 ≥ x2
inst✝ : Nonempty α
x✝ : IntegrableAtFilter f atBot μ
s : Set α
hs : s ∈ atBot
hi : IntegrableOn f s μ
⊢ ∃ a, IntegrableOn f (Iic a) μ

Tactic:
obtain ⟨t, ht⟩ := mem_atBot_sets.mp hs

Result:
case intro
α : Type u_1
E : Type u_4
inst✝⁴ : MeasurableSpace α
inst✝³ : NormedAddCommGroup E
f : α → E
μ : Measure α
inst✝² : Preorder α
inst✝¹ : IsDirected α fun x1 x2 => x1 ≥ x2
inst✝ : Nonempty α
x✝ : IntegrableAtFilter f atBot μ
s : Set α
hs : s ∈ atBot
hi : IntegrableOn f s μ
t : α
ht : ∀ b ≤ t, b ∈ s
⊢ ∃ a, IntegrableOn f (Iic a) μ

Proof state:
case intro
α : Type u_1
E : Type u_4
inst✝⁴ : MeasurableSpace α
inst✝³ : NormedAddCommGroup E
f : α → E
μ : Measure α
inst✝² : Preorder α
inst✝¹ : IsDirected α fun x1 x2 => x1 ≥ x2
inst✝ : Nonempty α
x✝ : IntegrableAtFilter f atBot μ
s : Set α
hs : s ∈ atBot
hi : IntegrableOn f s μ
t : α
ht : ∀ b ≤ t, b ∈ s
⊢ ∃ a, IntegrableOn f (Iic a) μ

Tactic:
exact ⟨t, hi.mono_set fun _ hx ↦ ht _ hx⟩

Result:
no goals
-- Mathlib/MeasureTheory/Integral/Lebesgue.lean
theorem lintegral_indicator {s : Set α} (hs : MeasurableSet s) (f : α → ℝ≥0∞) :
    ∫⁻ a, s.indicator f a ∂μ = ∫⁻ a in s, f a ∂μ

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
f : α → ℝ≥0∞
φ : α →ₛ ℝ≥0∞
hφ : ⇑φ ≤ fun a => f a
⊢ ∃ i', ((↑⟨φ, hφ⟩).restrict s).lintegral μ ≤ (↑i').lintegral μ

Tactic:
refine ⟨⟨φ.restrict s, fun x => ?_⟩, le_rfl⟩

Result:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
f : α → ℝ≥0∞
φ : α →ₛ ℝ≥0∞
hφ : ⇑φ ≤ fun a => f a
x : α
⊢ (φ.restrict s) x ≤ (fun a => s.indicator f a) x

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
f : α → ℝ≥0∞
⊢ ∫⁻ (a : α) in s, f a ∂μ ≤ ∫⁻ (a : α), s.indicator f a ∂μ

Tactic:
simp only [lintegral, ← restrict_lintegral_eq_lintegral_restrict _ hs, iSup_subtype']

Result:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
f : α → ℝ≥0∞
⊢ ⨆ x, ((↑x).restrict s).lintegral μ ≤ ⨆ x, (↑x).lintegral μ

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
f : α → ℝ≥0∞
φ : α →ₛ ℝ≥0∞
hφ : ⇑φ ≤ fun a => f a
x : α
⊢ (φ.restrict s) x ≤ (fun a => s.indicator f a) x

Tactic:
simp [hφ x, hs, indicator_le_indicator]

Result:
no goals

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
f : α → ℝ≥0∞
⊢ ⨆ x, ((↑x).restrict s).lintegral μ ≤ ⨆ x, (↑x).lintegral μ

Tactic:
refine iSup_mono' (Subtype.forall.2 fun φ hφ => ?_)

Result:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
f : α → ℝ≥0∞
φ : α →ₛ ℝ≥0∞
hφ : ⇑φ ≤ fun a => f a
⊢ ∃ i', ((↑⟨φ, hφ⟩).restrict s).lintegral μ ≤ (↑i').lintegral μ

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

Tactic:
apply le_antisymm (lintegral_indicator_le f s)

Result:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
f : α → ℝ≥0∞
⊢ ∫⁻ (a : α) in s, f a ∂μ ≤ ∫⁻ (a : α), s.indicator f a ∂μ
-- Mathlib/Analysis/Convex/Side.lean
theorem sSameSide_iff_exists_left {s : AffineSubspace R P} {x y p₁ : P} (h : p₁ ∈ s) :
    s.SSameSide x y ↔ x ∉ s ∧ y ∉ s ∧ ∃ p₂ ∈ s, SameRay R (x -ᵥ p₁) (y -ᵥ p₂)

Proof state:
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
s : AffineSubspace R P
x y p₁ : P
h : p₁ ∈ s
hx : x ∉ s
⊢ y ∉ s ∧ (x ∈ s ∨ ∃ p₂ ∈ s, SameRay R (x -ᵥ p₁) (y -ᵥ p₂)) ↔ y ∉ s ∧ ∃ p₂ ∈ s, SameRay R (x -ᵥ p₁) (y -ᵥ p₂)

Tactic:
rw [or_iff_right hx]

Result:
no goals

Proof state:
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
s : AffineSubspace R P
x y p₁ : P
h : p₁ ∈ s
⊢ x ∉ s → (y ∉ s ∧ (x ∈ s ∨ ∃ p₂ ∈ s, SameRay R (x -ᵥ p₁) (y -ᵥ p₂)) ↔ y ∉ s ∧ ∃ p₂ ∈ s, SameRay R (x -ᵥ p₁) (y -ᵥ p₂))

Tactic:
intro hx

Result:
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
s : AffineSubspace R P
x y p₁ : P
h : p₁ ∈ s
hx : x ∉ s
⊢ y ∉ s ∧ (x ∈ s ∨ ∃ p₂ ∈ s, SameRay R (x -ᵥ p₁) (y -ᵥ p₂)) ↔ y ∉ s ∧ ∃ p₂ ∈ s, SameRay R (x -ᵥ p₁) (y -ᵥ p₂)

Proof state:
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
s : AffineSubspace R P
x y p₁ : P
h : p₁ ∈ s
⊢ s.SSameSide x y ↔ x ∉ s ∧ y ∉ s ∧ ∃ p₂ ∈ s, SameRay R (x -ᵥ p₁) (y -ᵥ p₂)

Tactic:
rw [SSameSide, and_comm, wSameSide_iff_exists_left h, and_assoc, and_congr_right_iff]

Result:
R : Type u_1
V : Type u_2
P : Type u_4
inst✝³ : LinearOrderedField R
inst✝² : AddCommGroup V
inst✝¹ : Module R V
inst✝ : AddTorsor V P
s : AffineSubspace R P
x y p₁ : P
h : p₁ ∈ s
⊢ x ∉ s → (y ∉ s ∧ (x ∈ s ∨ ∃ p₂ ∈ s, SameRay R (x -ᵥ p₁) (y -ᵥ p₂)) ↔ y ∉ s ∧ ∃ p₂ ∈ s, SameRay R (x -ᵥ p₁) (y -ᵥ p₂))
-- Mathlib/Analysis/Calculus/MeanValue.lean
theorem not_differentiableWithinAt_of_deriv_tendsto_atBot_Ioi (f : ℝ → ℝ) {a : ℝ}
    (hf : Tendsto (deriv f) (𝓝[>] a) atBot) : ¬ DifferentiableWithinAt ℝ f (Ioi a) a

Proof state:
f : ℝ → ℝ
a : ℝ
hf : Tendsto (deriv f) (𝓝[>] a) atBot
h : DifferentiableWithinAt ℝ f (Ioi a) a
hf' : Tendsto (deriv (-f)) (𝓝[>] a) atTop
⊢ False

Tactic:
exact not_differentiableWithinAt_of_deriv_tendsto_atTop_Ioi (-f) hf' h.neg

Result:
no goals

Proof state:
f : ℝ → ℝ
a : ℝ
hf : Tendsto (deriv f) (𝓝[>] a) atBot
h : DifferentiableWithinAt ℝ f (Ioi a) a
⊢ False

Tactic:
have hf' : Tendsto (deriv (-f)) (𝓝[>] a) atTop := by
  rw [Pi.neg_def, deriv.neg']
  exact tendsto_neg_atBot_atTop.comp hf

Result:
f : ℝ → ℝ
a : ℝ
hf : Tendsto (deriv f) (𝓝[>] a) atBot
h : DifferentiableWithinAt ℝ f (Ioi a) a
hf' : Tendsto (deriv (-f)) (𝓝[>] a) atTop
⊢ False

Proof state:
f : ℝ → ℝ
a : ℝ
hf : Tendsto (deriv f) (𝓝[>] a) atBot
h : DifferentiableWithinAt ℝ f (Ioi a) a
⊢ Tendsto (deriv (-f)) (𝓝[>] a) atTop

Tactic:
rw [Pi.neg_def, deriv.neg']

Result:
f : ℝ → ℝ
a : ℝ
hf : Tendsto (deriv f) (𝓝[>] a) atBot
h : DifferentiableWithinAt ℝ f (Ioi a) a
⊢ Tendsto (fun x => -deriv f x) (𝓝[>] a) atTop

Proof state:
f : ℝ → ℝ
a : ℝ
hf : Tendsto (deriv f) (𝓝[>] a) atBot
⊢ ¬DifferentiableWithinAt ℝ f (Ioi a) a

Tactic:
intro h

Result:
f : ℝ → ℝ
a : ℝ
hf : Tendsto (deriv f) (𝓝[>] a) atBot
h : DifferentiableWithinAt ℝ f (Ioi a) a
⊢ False

Proof state:
f : ℝ → ℝ
a : ℝ
hf : Tendsto (deriv f) (𝓝[>] a) atBot
h : DifferentiableWithinAt ℝ f (Ioi a) a
⊢ Tendsto (fun x => -deriv f x) (𝓝[>] a) atTop

Tactic:
exact tendsto_neg_atBot_atTop.comp hf

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Integrals.lean
theorem integral_one_div_one_add_sq :
    (∫ x : ℝ in a..b, ↑1 / (↑1 + x ^ 2)) = arctan b - arctan a

Proof state:
a b : ℝ
⊢ ∫ (x : ℝ) in a..b, 1 / (1 + x ^ 2) = arctan b - arctan a

Tactic:
refine integral_deriv_eq_sub' _ Real.deriv_arctan (fun _ _ => differentiableAt_arctan _)
  (continuous_const.div ?_ fun x => ?_).continuousOn

Result:
case refine_1
a b : ℝ
⊢ Continuous fun x => 1 + x ^ 2

case refine_2
a b x : ℝ
⊢ 1 + x ^ 2 ≠ 0

Proof state:
case refine_1
a b : ℝ
⊢ Continuous fun x => 1 + x ^ 2

Tactic:
fun_prop

Result:
no goals

Proof state:
case refine_2
a b x : ℝ
⊢ 1 + x ^ 2 ≠ 0

Tactic:
nlinarith

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/Real.lean
theorem lt_rpow_iff_log_lt (hx : 0 < x) (hy : 0 < y) : x < y ^ z ↔ log x < z * log y

Proof state:
x y z : ℝ
hx : 0 < x
hy : 0 < y
⊢ x < y ^ z ↔ log x < z * log y

Tactic:
rw [← log_lt_log_iff hx (rpow_pos_of_pos hy z), log_rpow hy]

Result:
no goals
-- Mathlib/Probability/ProbabilityMassFunction/Monad.lean
theorem mem_support_bind_iff (b : β) :
    b ∈ (p.bind f).support ↔ ∃ a ∈ p.support, b ∈ (f a).support

Proof state:
α : Type u_1
β : Type u_2
p : PMF α
f : α → PMF β
b : β
⊢ b ∈ (p.bind f).support ↔ ∃ a ∈ p.support, b ∈ (f a).support

Tactic:
simp only [support_bind, Set.mem_iUnion, Set.mem_setOf_eq, exists_prop]

Result:
no goals