harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/CategoryTheory/Functor/EpiMono.lean
theorem strongEpi_map_of_strongEpi (adj : F ⊣ F') (f : A ⟶ B) [F'.PreservesMonomorphisms]
    [F.PreservesEpimorphisms] [StrongEpi f] : StrongEpi (F.map f) :=
  ⟨inferInstance, fun X Y Z => by
    intro
    rw [adj.hasLiftingProperty_iff]
    infer_instance⟩

Proof state:
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{u_3, u_1} C
inst✝³ : Category.{u_4, u_2} D
F : C ⥤ D
F' : D ⥤ C
A B : C
adj : F ⊣ F'
f : A ⟶ B
inst✝² : F'.PreservesMonomorphisms
inst✝¹ : F.PreservesEpimorphisms
inst✝ : StrongEpi f
X Y : D
Z : X ⟶ Y
⊢ ∀ [inst : Mono Z], HasLiftingProperty (F.map f) Z

Tactic:
intro

Result:
C : Type u_1
D : Type u_2
inst✝⁵ : Category.{u_3, u_1} C
inst✝⁴ : Category.{u_4, u_2} D
F : C ⥤ D
F' : D ⥤ C
A B : C
adj : F ⊣ F'
f : A ⟶ B
inst✝³ : F'.PreservesMonomorphisms
inst✝² : F.PreservesEpimorphisms
inst✝¹ : StrongEpi f
X Y : D
Z : X ⟶ Y
inst✝ : Mono Z
⊢ HasLiftingProperty (F.map f) Z

Proof state:
C : Type u_1
D : Type u_2
inst✝⁵ : Category.{u_3, u_1} C
inst✝⁴ : Category.{u_4, u_2} D
F : C ⥤ D
F' : D ⥤ C
A B : C
adj : F ⊣ F'
f : A ⟶ B
inst✝³ : F'.PreservesMonomorphisms
inst✝² : F.PreservesEpimorphisms
inst✝¹ : StrongEpi f
X Y : D
Z : X ⟶ Y
inst✝ : Mono Z
⊢ HasLiftingProperty f (F'.map Z)

Tactic:
infer_instance

Result:
no goals

Proof state:
C : Type u_1
D : Type u_2
inst✝⁵ : Category.{u_3, u_1} C
inst✝⁴ : Category.{u_4, u_2} D
F : C ⥤ D
F' : D ⥤ C
A B : C
adj : F ⊣ F'
f : A ⟶ B
inst✝³ : F'.PreservesMonomorphisms
inst✝² : F.PreservesEpimorphisms
inst✝¹ : StrongEpi f
X Y : D
Z : X ⟶ Y
inst✝ : Mono Z
⊢ HasLiftingProperty (F.map f) Z

Tactic:
rw [adj.hasLiftingProperty_iff]

Result:
C : Type u_1
D : Type u_2
inst✝⁵ : Category.{u_3, u_1} C
inst✝⁴ : Category.{u_4, u_2} D
F : C ⥤ D
F' : D ⥤ C
A B : C
adj : F ⊣ F'
f : A ⟶ B
inst✝³ : F'.PreservesMonomorphisms
inst✝² : F.PreservesEpimorphisms
inst✝¹ : StrongEpi f
X Y : D
Z : X ⟶ Y
inst✝ : Mono Z
⊢ HasLiftingProperty f (F'.map Z)
-- Mathlib/Topology/MetricSpace/HolderNorm.lean
@[simp]
lemma nnHolderNorm_const (r : ℝ≥0) (c : Y) : nnHolderNorm r (Function.const X c) = 0

Proof state:
X : Type u_1
Y : Type u_2
inst✝¹ : PseudoEMetricSpace X
inst✝ : PseudoEMetricSpace Y
r : ℝ≥0
c : Y
⊢ nnHolderNorm r (Function.const X c) = 0

Tactic:
refine le_antisymm (ENNReal.coe_le_coe.1 <|
  le_trans coe_nnHolderNorm_le_eHolderNorm ?_) (zero_le _)

Result:
X : Type u_1
Y : Type u_2
inst✝¹ : PseudoEMetricSpace X
inst✝ : PseudoEMetricSpace Y
r : ℝ≥0
c : Y
⊢ eHolderNorm r (Function.const X c) ≤ ↑0

Proof state:
X : Type u_1
Y : Type u_2
inst✝¹ : PseudoEMetricSpace X
inst✝ : PseudoEMetricSpace Y
r : ℝ≥0
c : Y
⊢ eHolderNorm r (Function.const X c) ≤ ↑0

Tactic:
rw [eHolderNorm_const, ENNReal.coe_zero]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/PosPart.lean
@[aesop norm apply (rule_sets := [CStarAlgebra])]
lemma negPart_nonneg (a : A) :
    0 ≤ a⁻ :=
  cfcₙ_nonneg (fun x _ ↦ by positivity)

Proof state:
A : Type u_1
inst✝⁸ : NonUnitalRing A
inst✝⁷ : Module ℝ A
inst✝⁶ : SMulCommClass ℝ A A
inst✝⁵ : IsScalarTower ℝ A A
inst✝⁴ : StarRing A
inst✝³ : TopologicalSpace A
inst✝² : NonUnitalContinuousFunctionalCalculus ℝ IsSelfAdjoint
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
a : A
x : ℝ
x✝ : x ∈ quasispectrum ℝ a
⊢ 0 ≤ x⁻

Tactic:
positivity

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian.lean
lemma toAffine_of_singular {P : Fin 3 → F} (hP : ¬W.Nonsingular P) : toAffine W P = 0

Proof state:
F : Type u
inst✝ : Field F
W : Jacobian F
P : Fin 3 → F
hP : ¬W.Nonsingular P
⊢ toAffine W P = 0

Tactic:
rw [toAffine, dif_neg <| not_and_of_not_left _ hP]

Result:
no goals
-- Mathlib/MeasureTheory/Function/AEEqFun.lean
theorem coeFn_comp₂Measurable (g : β → γ → δ) (hg : Measurable (uncurry g)) (f₁ : α →ₘ[μ] β)
    (f₂ : α →ₘ[μ] γ) : comp₂Measurable g hg f₁ f₂ =ᵐ[μ] fun a => g (f₁ a) (f₂ a)

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹⁴ : MeasurableSpace α
μ : Measure α
inst✝¹³ : TopologicalSpace δ
inst✝¹² : TopologicalSpace β
inst✝¹¹ : TopologicalSpace γ
inst✝¹⁰ : MeasurableSpace β
inst✝⁹ : PseudoMetrizableSpace β
inst✝⁸ : BorelSpace β
inst✝⁷ : MeasurableSpace γ
inst✝⁶ : PseudoMetrizableSpace γ
inst✝⁵ : BorelSpace γ
inst✝⁴ : SecondCountableTopologyEither β γ
inst✝³ : MeasurableSpace δ
inst✝² : PseudoMetrizableSpace δ
inst✝¹ : OpensMeasurableSpace δ
inst✝ : SecondCountableTopology δ
g : β → γ → δ
hg : Measurable (uncurry g)
f₁ : α →ₘ[μ] β
f₂ : α →ₘ[μ] γ
⊢ ↑(comp₂Measurable g hg f₁ f₂) =ᶠ[ae μ] fun a => g (↑f₁ a) (↑f₂ a)

Tactic:
rw [comp₂Measurable_eq_mk]

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹⁴ : MeasurableSpace α
μ : Measure α
inst✝¹³ : TopologicalSpace δ
inst✝¹² : TopologicalSpace β
inst✝¹¹ : TopologicalSpace γ
inst✝¹⁰ : MeasurableSpace β
inst✝⁹ : PseudoMetrizableSpace β
inst✝⁸ : BorelSpace β
inst✝⁷ : MeasurableSpace γ
inst✝⁶ : PseudoMetrizableSpace γ
inst✝⁵ : BorelSpace γ
inst✝⁴ : SecondCountableTopologyEither β γ
inst✝³ : MeasurableSpace δ
inst✝² : PseudoMetrizableSpace δ
inst✝¹ : OpensMeasurableSpace δ
inst✝ : SecondCountableTopology δ
g : β → γ → δ
hg : Measurable (uncurry g)
f₁ : α →ₘ[μ] β
f₂ : α →ₘ[μ] γ
⊢ ↑(mk (fun a => g (↑f₁ a) (↑f₂ a)) ⋯) =ᶠ[ae μ] fun a => g (↑f₁ a) (↑f₂ a)

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
inst✝¹⁴ : MeasurableSpace α
μ : Measure α
inst✝¹³ : TopologicalSpace δ
inst✝¹² : TopologicalSpace β
inst✝¹¹ : TopologicalSpace γ
inst✝¹⁰ : MeasurableSpace β
inst✝⁹ : PseudoMetrizableSpace β
inst✝⁸ : BorelSpace β
inst✝⁷ : MeasurableSpace γ
inst✝⁶ : PseudoMetrizableSpace γ
inst✝⁵ : BorelSpace γ
inst✝⁴ : SecondCountableTopologyEither β γ
inst✝³ : MeasurableSpace δ
inst✝² : PseudoMetrizableSpace δ
inst✝¹ : OpensMeasurableSpace δ
inst✝ : SecondCountableTopology δ
g : β → γ → δ
hg : Measurable (uncurry g)
f₁ : α →ₘ[μ] β
f₂ : α →ₘ[μ] γ
⊢ ↑(mk (fun a => g (↑f₁ a) (↑f₂ a)) ⋯) =ᶠ[ae μ] fun a => g (↑f₁ a) (↑f₂ a)

Tactic:
apply coeFn_mk

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Log/ENNRealLog.lean
theorem log_of_nnreal {x : ℝ≥0} (h : x ≠ 0) :
    log (x : ℝ≥0∞) = Real.log x

Proof state:
x : ℝ≥0
h : x ≠ 0
⊢ (↑x).log = ↑(Real.log ↑x)

Tactic:
simp [log, h]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/SetToL1.lean
theorem setToFun_add (hT : DominatedFinMeasAdditive μ T C) (hf : Integrable f μ)
    (hg : Integrable g μ) : setToFun μ T hT (f + g) = setToFun μ T hT f + setToFun μ T hT g

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 : Set α → E →L[ℝ] F
C : ℝ
f g : α → E
hT : DominatedFinMeasAdditive μ T C
hf : Integrable f μ
hg : Integrable g μ
⊢ setToFun μ T hT (f + g) = setToFun μ T hT f + setToFun μ T hT g

Tactic:
rw [setToFun_eq hT (hf.add hg), setToFun_eq hT hf, setToFun_eq hT hg, Integrable.toL1_add,
  (L1.setToL1 hT).map_add]

Result:
no goals
-- Mathlib/RingTheory/LocalProperties/Basic.lean
theorem Ideal.mem_of_localization_maximal {r : R} {J : Ideal R}
    (h : ∀ (P : Ideal R) (_ : P.IsMaximal),
      algebraMap R _ r ∈ Ideal.map (algebraMap R (Localization.AtPrime P)) J) :
    r ∈ J :=
  Submodule.mem_of_localization_maximal _ _ _ _ fun P hP ↦ by
    apply (localized'_eq_map (Localization.AtPrime P) P.primeCompl J).symm ▸ h P hP

Proof state:
R : Type u_1
inst✝ : CommSemiring R
r : R
J : Ideal R
h :
  ∀ (P : Ideal R) (x : P.IsMaximal),
    (algebraMap R (Localization.AtPrime P)) r ∈ map (algebraMap R (Localization.AtPrime P)) J
P : Ideal R
hP : P.IsMaximal
⊢ (?m.170946 P) r ∈ Submodule.localized₀ P.primeCompl (?m.170946 P) J

Tactic:
apply (localized'_eq_map (Localization.AtPrime P) P.primeCompl J).symm ▸ h P hP

Result:
no goals
-- Mathlib/CategoryTheory/Monoidal/Category.lean
theorem whiskerLeft_hom_inv' (X : C) {Y Z : C} (f : Y ⟶ Z) [IsIso f] :
    X ◁ f ≫ X ◁ inv f = 𝟙 (X ⊗ Y)

Proof state:
C : Type u
𝒞 : Category.{v, u} C
inst✝¹ : MonoidalCategory C
X Y Z : C
f : Y ⟶ Z
inst✝ : IsIso f
⊢ X ◁ f ≫ X ◁ inv f = 𝟙 (X ⊗ Y)

Tactic:
rw [← whiskerLeft_comp, IsIso.hom_inv_id, whiskerLeft_id]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem contains_push [BEq α] {l : Array α} {a : α} {b : α} :
    (l.push a).contains b = (l.contains b || b == a)

Proof state:
α : Type u_1
inst✝ : BEq α
l : Array α
a b : α
⊢ (l.push a).contains b = (l.contains b || b == a)

Tactic:
simp [contains]

Result:
no goals
-- Mathlib/GroupTheory/OreLocalization/Basic.lean
theorem smul_one_smul (r : R) (x : X[S⁻¹]) : (r • 1 : M) • x = r • x

Proof state:
case c
R : Type u_1
M : Type u_3
X : Type u_4
inst✝⁶ : Monoid M
S : Submonoid M
inst✝⁵ : OreSet S
inst✝⁴ : MulAction M X
inst✝³ : SMul R X
inst✝² : SMul R M
inst✝¹ : IsScalarTower R M M
inst✝ : IsScalarTower R M X
r : R
r' : X
s : ↥S
⊢ (r • 1) • (r' /ₒ s) = r • (r' /ₒ s)

Tactic:
simp only [smul_oreDiv, smul_eq_mul, mul_one]

Result:
no goals

Proof state:
R : Type u_1
M : Type u_3
X : Type u_4
inst✝⁶ : Monoid M
S : Submonoid M
inst✝⁵ : OreSet S
inst✝⁴ : MulAction M X
inst✝³ : SMul R X
inst✝² : SMul R M
inst✝¹ : IsScalarTower R M M
inst✝ : IsScalarTower R M X
r : R
x : OreLocalization S X
⊢ (r • 1) • x = r • x

Tactic:
induction' x using OreLocalization.ind with r' s

Result:
case c
R : Type u_1
M : Type u_3
X : Type u_4
inst✝⁶ : Monoid M
S : Submonoid M
inst✝⁵ : OreSet S
inst✝⁴ : MulAction M X
inst✝³ : SMul R X
inst✝² : SMul R M
inst✝¹ : IsScalarTower R M M
inst✝ : IsScalarTower R M X
r : R
r' : X
s : ↥S
⊢ (r • 1) • (r' /ₒ s) = r • (r' /ₒ s)
-- Mathlib/RingTheory/DualNumber.lean
@[simp]
lemma isNilpotent_inl_iff (r : R) : IsNilpotent (.inl r : TrivSqZeroExt R M) ↔ IsNilpotent r

Proof state:
R : Type u_1
M : Type u_2
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : SMulCommClass R Rᵐᵒᵖ M
r : R
⊢ IsNilpotent (inl r) ↔ IsNilpotent r

Tactic:
rw [isNilpotent_iff_isNilpotent_fst, fst_inl]

Result:
no goals
-- Mathlib/Data/Nat/GCD/Basic.lean
theorem coprime_add_mul_left_left (m n k : ℕ) : Coprime (m + n * k) n ↔ Coprime m n

Proof state:
m n k : ℕ
⊢ (m + n * k).Coprime n ↔ m.Coprime n

Tactic:
rw [Coprime, Coprime, gcd_add_mul_left_left]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem any_beq' [BEq α] [PartialEquivBEq α] {l : List α} :
    (l.any fun x => x == a) = l.contains a

Proof state:
α : Type u_1
a : α
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
l : List α
⊢ (l.any fun x => x == a) = l.contains a

Tactic:
simp only [BEq.comm, any_beq]

Result:
no goals
-- Mathlib/AlgebraicGeometry/GammaSpecAdjunction.lean
theorem toΓSpec_continuous : Continuous X.toΓSpecFun

Proof state:
X : LocallyRingedSpace
⊢ ∀ s ∈ Set.range fun r => ↑(basicOpen r), IsOpen (X.toΓSpecFun ⁻¹' s)

Tactic:
rintro _ ⟨r, rfl⟩

Result:
case intro
X : LocallyRingedSpace
r : ↑(Γ.obj (op X))
⊢ IsOpen (X.toΓSpecFun ⁻¹' (fun r => ↑(basicOpen r)) r)

Proof state:
X : LocallyRingedSpace
⊢ Continuous X.toΓSpecFun

Tactic:
rw [isTopologicalBasis_basic_opens.continuous_iff]

Result:
X : LocallyRingedSpace
⊢ ∀ s ∈ Set.range fun r => ↑(basicOpen r), IsOpen (X.toΓSpecFun ⁻¹' s)

Proof state:
case intro
X : LocallyRingedSpace
r : ↑(Γ.obj (op X))
⊢ IsOpen ↑(X.toRingedSpace.basicOpen r)

Tactic:
exact (X.toRingedSpace.basicOpen r).2

Result:
no goals

Proof state:
case intro
X : LocallyRingedSpace
r : ↑(Γ.obj (op X))
⊢ IsOpen (X.toΓSpecFun ⁻¹' (fun r => ↑(basicOpen r)) r)

Tactic:
rw [X.toΓSpec_preimage_basicOpen_eq r]

Result:
case intro
X : LocallyRingedSpace
r : ↑(Γ.obj (op X))
⊢ IsOpen ↑(X.toRingedSpace.basicOpen r)
-- Mathlib/NumberTheory/DirichletCharacter/Basic.lean
lemma changeLevel_self_toUnitHom : (changeLevel (dvd_refl n) χ).toUnitHom = χ.toUnitHom

Proof state:
R : Type u_1
inst✝ : CommMonoidWithZero R
n : ℕ
χ : DirichletCharacter R n
⊢ toUnitHom ((changeLevel ⋯) χ) = toUnitHom χ

Tactic:
rw [changeLevel_self]

Result:
no goals
-- Mathlib/Data/Real/Pi/Bounds.lean
theorem pi_lt_d2 : π < 3.15

Proof state:
⊢ π < 3.15

Tactic:
pi_upper_bound [41 / 29, 109 / 59, 865 / 441, 412 / 207]

Result:
no goals
-- Mathlib/Data/Seq/Seq.lean
theorem ofList_append (l l' : List α) : ofList (l ++ l') = append (ofList l) (ofList l')

Proof state:
α : Type u
l l' : List α
⊢ ↑(l ++ l') = (↑l).append ↑l'

Tactic:
induction l <;> simp [*]

Result:
no goals
-- Mathlib/Algebra/Module/PointwisePi.lean
theorem smul_pi_subset [∀ i, SMul K (R i)] (r : K) (s : Set ι) (t : ∀ i, Set (R i)) :
    r • pi s t ⊆ pi s (r • t)

Proof state:
K : Type u_1
ι : Type u_2
R : ι → Type u_3
inst✝ : (i : ι) → SMul K (R i)
r : K
s : Set ι
t : (i : ι) → Set (R i)
⊢ r • s.pi t ⊆ s.pi (r • t)

Tactic:
rintro x ⟨y, h, rfl⟩ i hi

Result:
case intro.intro
K : Type u_1
ι : Type u_2
R : ι → Type u_3
inst✝ : (i : ι) → SMul K (R i)
r : K
s : Set ι
t : (i : ι) → Set (R i)
y : (i : ι) → R i
h : y ∈ s.pi t
i : ι
hi : i ∈ s
⊢ (fun x => r • x) y i ∈ (r • t) i

Proof state:
case intro.intro
K : Type u_1
ι : Type u_2
R : ι → Type u_3
inst✝ : (i : ι) → SMul K (R i)
r : K
s : Set ι
t : (i : ι) → Set (R i)
y : (i : ι) → R i
h : y ∈ s.pi t
i : ι
hi : i ∈ s
⊢ (fun x => r • x) y i ∈ (r • t) i

Tactic:
exact smul_mem_smul_set (h i hi)

Result:
no goals
-- Mathlib/Data/Nat/Choose/Sum.lean
theorem sum_antidiagonal_choose_succ_mul (f : ℕ → ℕ → R) (n : ℕ) :
    (∑ ij ∈ antidiagonal (n + 1), ((n + 1).choose ij.1 : R) * f ij.1 ij.2) =
      (∑ ij ∈ antidiagonal n, (n.choose ij.1 : R) * f ij.1 (ij.2 + 1)) +
        ∑ ij ∈ antidiagonal n, (n.choose ij.2 : R) * f (ij.1 + 1) ij.2

Proof state:
R : Type u_1
inst✝ : NonAssocSemiring R
f : ℕ → ℕ → R
n : ℕ
⊢ ∑ ij ∈ antidiagonal (n + 1), ↑((n + 1).choose ij.1) * f ij.1 ij.2 =
    ∑ ij ∈ antidiagonal n, ↑(n.choose ij.1) * f ij.1 (ij.2 + 1) +
      ∑ ij ∈ antidiagonal n, ↑(n.choose ij.2) * f (ij.1 + 1) ij.2

Tactic:
simpa only [nsmul_eq_mul] using sum_antidiagonal_choose_succ_nsmul f n

Result:
no goals
-- Mathlib/Order/UpperLower/Basic.lean
@[simp] lemma IsLowerSet.disjoint_upperClosure_left (ht : IsLowerSet t) :
    Disjoint ↑(upperClosure s) t ↔ Disjoint s t

Proof state:
α : Type u_1
inst✝ : Preorder α
s t : Set α
ht : IsLowerSet t
⊢ Disjoint s t → Disjoint (↑(upperClosure s)) t

Tactic:
simp only [disjoint_left, SetLike.mem_coe, mem_upperClosure, forall_exists_index, and_imp]

Result:
α : Type u_1
inst✝ : Preorder α
s t : Set α
ht : IsLowerSet t
⊢ (∀ ⦃a : α⦄, a ∈ s → a ∉ t) → ∀ ⦃a : α⦄, ∀ x ∈ s, x ≤ a → a ∉ t

Proof state:
α : Type u_1
inst✝ : Preorder α
s t : Set α
ht : IsLowerSet t
⊢ Disjoint (↑(upperClosure s)) t ↔ Disjoint s t

Tactic:
refine ⟨Disjoint.mono_left subset_upperClosure, ?_⟩

Result:
α : Type u_1
inst✝ : Preorder α
s t : Set α
ht : IsLowerSet t
⊢ Disjoint s t → Disjoint (↑(upperClosure s)) t

Proof state:
α : Type u_1
inst✝ : Preorder α
s t : Set α
ht : IsLowerSet t
⊢ (∀ ⦃a : α⦄, a ∈ s → a ∉ t) → ∀ ⦃a : α⦄, ∀ x ∈ s, x ≤ a → a ∉ t

Tactic:
exact fun h a b hb hba ha ↦ h hb <| ht hba ha

Result:
no goals
-- Mathlib/Data/Rat/Cast/Order.lean
@[norm_cast] lemma cast_lt_zero : (q : K) < 0 ↔ q < 0

Proof state:
K : Type u_5
inst✝ : LinearOrderedSemifield K
q : ℚ≥0
⊢ ↑q < 0 ↔ q < 0

Tactic:
norm_cast

Result:
no goals
-- Mathlib/Analysis/Normed/Group/Uniform.lean
@[to_additive]
lemma LipschitzOnWith.div (hf : LipschitzOnWith Kf f s) (hg : LipschitzOnWith Kg g s) :
    LipschitzOnWith (Kf + Kg) (fun x ↦ f x / g x) s

Proof state:
α : Type u_4
E : Type u_5
inst✝¹ : SeminormedCommGroup E
inst✝ : PseudoEMetricSpace α
Kf Kg : ℝ≥0
f g : α → E
s : Set α
hf : LipschitzOnWith Kf f s
hg : LipschitzOnWith Kg g s
⊢ LipschitzOnWith (Kf + Kg) (fun x => f x / g x) s

Tactic:
simpa only [div_eq_mul_inv] using hf.mul hg.inv

Result:
no goals
-- Mathlib/Analysis/ConstantSpeed.lean
theorem unique_unit_speed {φ : ℝ → ℝ} (φm : MonotoneOn φ s) (hfφ : HasUnitSpeedOn (f ∘ φ) s)
    (hf : HasUnitSpeedOn f (φ '' s)) ⦃x : ℝ⦄ (xs : x ∈ s) : EqOn φ (fun y => y - x + φ x) s

Proof state:
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : ℝ → E
s : Set ℝ
φ : ℝ → ℝ
φm : MonotoneOn φ s
hfφ : HasUnitSpeedOn (f ∘ φ) s
hf : HasUnitSpeedOn f (φ '' s)
x : ℝ
xs : x ∈ s
⊢ EqOn φ (fun y => y - x + φ x) s

Tactic:
dsimp only [HasUnitSpeedOn] at hf hfφ

Result:
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : ℝ → E
s : Set ℝ
φ : ℝ → ℝ
φm : MonotoneOn φ s
hfφ : HasConstantSpeedOnWith (f ∘ φ) s 1
hf : HasConstantSpeedOnWith f (φ '' s) 1
x : ℝ
xs : x ∈ s
⊢ EqOn φ (fun y => y - x + φ x) s

Proof state:
case h.e'_4.h.h.e'_5
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : ℝ → E
s : Set ℝ
φ : ℝ → ℝ
φm : MonotoneOn φ s
hfφ : HasConstantSpeedOnWith (f ∘ φ) s 1
hf : HasConstantSpeedOnWith f (φ '' s) 1
x : ℝ
xs : x ∈ s
x✝ : ℝ
⊢ x✝ - x = ↑1 / ↑1 * (x✝ - x)

Tactic:
norm_num

Result:
no goals

Proof state:
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : ℝ → E
s : Set ℝ
φ : ℝ → ℝ
φm : MonotoneOn φ s
hfφ : HasConstantSpeedOnWith (f ∘ φ) s 1
hf : HasConstantSpeedOnWith f (φ '' s) 1
x : ℝ
xs : x ∈ s
⊢ EqOn φ (fun y => y - x + φ x) s

Tactic:
convert HasConstantSpeedOnWith.ratio one_ne_zero φm hfφ hf xs using 3

Result:
case h.e'_4.h.h.e'_5
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : ℝ → E
s : Set ℝ
φ : ℝ → ℝ
φm : MonotoneOn φ s
hfφ : HasConstantSpeedOnWith (f ∘ φ) s 1
hf : HasConstantSpeedOnWith f (φ '' s) 1
x : ℝ
xs : x ∈ s
x✝ : ℝ
⊢ x✝ - x = ↑1 / ↑1 * (x✝ - x)
-- Mathlib/Analysis/Calculus/FDeriv/WithLp.lean
theorem differentiableOn_piLp :
    DifferentiableOn 𝕜 f t ↔ ∀ i, DifferentiableOn 𝕜 (fun x => f x i) t

Proof state:
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
H : Type u_4
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : (i : ι) → NormedAddCommGroup (E i)
inst✝³ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝² : NormedSpace 𝕜 H
inst✝¹ : Fintype ι
p : ENNReal
inst✝ : Fact (1 ≤ p)
f : H → PiLp p E
t : Set H
⊢ (∀ (i : ι), DifferentiableOn 𝕜 (fun x => (⇑(PiLp.continuousLinearEquiv p 𝕜 E) ∘ f) x i) t) ↔
    ∀ (i : ι), DifferentiableOn 𝕜 (fun x => f x i) t

Tactic:
rfl

Result:
no goals

Proof state:
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
H : Type u_4
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : (i : ι) → NormedAddCommGroup (E i)
inst✝³ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝² : NormedSpace 𝕜 H
inst✝¹ : Fintype ι
p : ENNReal
inst✝ : Fact (1 ≤ p)
f : H → PiLp p E
t : Set H
⊢ DifferentiableOn 𝕜 f t ↔ ∀ (i : ι), DifferentiableOn 𝕜 (fun x => f x i) t

Tactic:
rw [← (PiLp.continuousLinearEquiv p 𝕜 E).comp_differentiableOn_iff, differentiableOn_pi]

Result:
𝕜 : Type u_1
ι : Type u_2
E : ι → Type u_3
H : Type u_4
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup H
inst✝⁴ : (i : ι) → NormedAddCommGroup (E i)
inst✝³ : (i : ι) → NormedSpace 𝕜 (E i)
inst✝² : NormedSpace 𝕜 H
inst✝¹ : Fintype ι
p : ENNReal
inst✝ : Fact (1 ≤ p)
f : H → PiLp p E
t : Set H
⊢ (∀ (i : ι), DifferentiableOn 𝕜 (fun x => (⇑(PiLp.continuousLinearEquiv p 𝕜 E) ∘ f) x i) t) ↔
    ∀ (i : ι), DifferentiableOn 𝕜 (fun x => f x i) t
-- Mathlib/Probability/Distributions/Exponential.lean
lemma exponentialPDF_eq (r x : ℝ) :
    exponentialPDF r x = ENNReal.ofReal (if 0 ≤ x then r * exp (-(r * x)) else 0)

Proof state:
r x : ℝ
⊢ ENNReal.ofReal (if 0 ≤ x then r ^ 1 / Gamma 1 * x ^ (1 - 1) * rexp (-(r * x)) else 0) =
    ENNReal.ofReal (if 0 ≤ x then r * rexp (-(r * x)) else 0)

Tactic:
simp only [rpow_one, Gamma_one, div_one, sub_self, rpow_zero, mul_one]

Result:
no goals

Proof state:
r x : ℝ
⊢ exponentialPDF r x = ENNReal.ofReal (if 0 ≤ x then r * rexp (-(r * x)) else 0)

Tactic:
rw [exponentialPDF, exponentialPDFReal, gammaPDFReal]

Result:
r x : ℝ
⊢ ENNReal.ofReal (if 0 ≤ x then r ^ 1 / Gamma 1 * x ^ (1 - 1) * rexp (-(r * x)) else 0) =
    ENNReal.ofReal (if 0 ≤ x then r * rexp (-(r * x)) else 0)
-- Mathlib/RingTheory/MvPolynomial/Basic.lean
theorem mem_restrictDegree_iff_sup [DecidableEq σ] (p : MvPolynomial σ R) (n : ℕ) :
    p ∈ restrictDegree σ R n ↔ ∀ i, p.degrees.count i ≤ n

Proof state:
σ : Type u
R : Type v
inst✝¹ : CommSemiring R
inst✝ : DecidableEq σ
p : MvPolynomial σ R
n : ℕ
⊢ (∀ s ∈ p.support, ∀ (i : σ), s i ≤ n) ↔ ∀ (i : σ), ∀ b ∈ p.support, b i ≤ n

Tactic:
exact ⟨fun h n s hs => h s hs n, fun h s hs n => h n s hs⟩

Result:
no goals

Proof state:
σ : Type u
R : Type v
inst✝¹ : CommSemiring R
inst✝ : DecidableEq σ
p : MvPolynomial σ R
n : ℕ
⊢ p ∈ restrictDegree σ R n ↔ ∀ (i : σ), Multiset.count i p.degrees ≤ n

Tactic:
simp only [mem_restrictDegree, degrees_def, Multiset.count_finset_sup, Finsupp.count_toMultiset,
  Finset.sup_le_iff]

Result:
σ : Type u
R : Type v
inst✝¹ : CommSemiring R
inst✝ : DecidableEq σ
p : MvPolynomial σ R
n : ℕ
⊢ (∀ s ∈ p.support, ∀ (i : σ), s i ≤ n) ↔ ∀ (i : σ), ∀ b ∈ p.support, b i ≤ n
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/DivModLemmas.lean
theorem zero_dvd {n : Int} : 0 ∣ n ↔ n = 0 :=
  Iff.intro (fun ⟨k, e⟩ => by rw [e, Int.zero_mul])
            (fun h => h.symm ▸ Int.dvd_refl _)

Proof state:
n : Int
x✝ : 0 ∣ n
k : Int
e : n = 0 * k
⊢ n = 0

Tactic:
rw [e, Int.zero_mul]

Result:
no goals
-- Mathlib/Order/CompleteBooleanAlgebra.lean
theorem iSup_inf_eq (f : ι → α) (a : α) : (⨆ i, f i) ⊓ a = ⨆ i, f i ⊓ a

Proof state:
α : Type u
ι : Sort w
inst✝ : Frame α
f : ι → α
a : α
⊢ (⨆ i, f i) ⊓ a = ⨆ i, f i ⊓ a

Tactic:
rw [iSup, sSup_inf_eq, iSup_range]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Hausdorff.lean
theorem trim_pre [MeasurableSpace X] [OpensMeasurableSpace X] (m : Set X → ℝ≥0∞)
    (hcl : ∀ s, m (closure s) = m s) (r : ℝ≥0∞) : (pre m r).trim = pre m r

Proof state:
X : Type u_2
inst✝² : EMetricSpace X
inst✝¹ : MeasurableSpace X
inst✝ : OpensMeasurableSpace X
m : Set X → ℝ≥0∞
hcl : ∀ (s : Set X), m (closure s) = m s
r : ℝ≥0∞
s : Set X
hs : diam s ≤ r
⊢ (pre m r).trim s ≤ m s

Tactic:
rw [trim_eq_iInf]

Result:
X : Type u_2
inst✝² : EMetricSpace X
inst✝¹ : MeasurableSpace X
inst✝ : OpensMeasurableSpace X
m : Set X → ℝ≥0∞
hcl : ∀ (s : Set X), m (closure s) = m s
r : ℝ≥0∞
s : Set X
hs : diam s ≤ r
⊢ ⨅ t, ⨅ (_ : s ⊆ t), ⨅ (_ : MeasurableSet t), (pre m r) t ≤ m s

Proof state:
X : Type u_2
inst✝² : EMetricSpace X
inst✝¹ : MeasurableSpace X
inst✝ : OpensMeasurableSpace X
m : Set X → ℝ≥0∞
hcl : ∀ (s : Set X), m (closure s) = m s
r : ℝ≥0∞
⊢ (pre m r).trim = pre m r

Tactic:
refine le_antisymm (le_pre.2 fun s hs => ?_) (le_trim _)

Result:
X : Type u_2
inst✝² : EMetricSpace X
inst✝¹ : MeasurableSpace X
inst✝ : OpensMeasurableSpace X
m : Set X → ℝ≥0∞
hcl : ∀ (s : Set X), m (closure s) = m s
r : ℝ≥0∞
s : Set X
hs : diam s ≤ r
⊢ (pre m r).trim s ≤ m s

Proof state:
X : Type u_2
inst✝² : EMetricSpace X
inst✝¹ : MeasurableSpace X
inst✝ : OpensMeasurableSpace X
m : Set X → ℝ≥0∞
hcl : ∀ (s : Set X), m (closure s) = m s
r : ℝ≥0∞
s : Set X
hs : diam s ≤ r
⊢ diam (closure s) ≤ r

Tactic:
rwa [diam_closure]

Result:
no goals

Proof state:
X : Type u_2
inst✝² : EMetricSpace X
inst✝¹ : MeasurableSpace X
inst✝ : OpensMeasurableSpace X
m : Set X → ℝ≥0∞
hcl : ∀ (s : Set X), m (closure s) = m s
r : ℝ≥0∞
s : Set X
hs : diam s ≤ r
⊢ ⨅ t, ⨅ (_ : s ⊆ t), ⨅ (_ : MeasurableSet t), (pre m r) t ≤ m s

Tactic:
refine iInf_le_of_le (closure s) <| iInf_le_of_le subset_closure <|
  iInf_le_of_le measurableSet_closure ((pre_le ?_).trans_eq (hcl _))

Result:
X : Type u_2
inst✝² : EMetricSpace X
inst✝¹ : MeasurableSpace X
inst✝ : OpensMeasurableSpace X
m : Set X → ℝ≥0∞
hcl : ∀ (s : Set X), m (closure s) = m s
r : ℝ≥0∞
s : Set X
hs : diam s ≤ r
⊢ diam (closure s) ≤ r