harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/MeasureTheory/Integral/SetIntegral.lean
theorem continuous_integral_comp_L1 (L : E →L[𝕜] F) :
    Continuous fun φ : X →₁[μ] E => ∫ x : X, L (φ x) ∂μ

Proof state:
X : Type u_1
E : Type u_3
F : Type u_4
inst✝⁶ : MeasurableSpace X
μ : Measure X
𝕜 : Type u_5
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : NormedSpace ℝ F
L : E →L[𝕜] F
⊢ Continuous fun x => ∫ (x_1 : X), ↑↑(L.compLp x) x_1 ∂μ

Tactic:
exact continuous_integral.comp (L.compLpL 1 μ).continuous

Result:
no goals

Proof state:
X : Type u_1
E : Type u_3
F : Type u_4
inst✝⁶ : MeasurableSpace X
μ : Measure X
𝕜 : Type u_5
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : NormedSpace ℝ F
L : E →L[𝕜] F
⊢ Continuous fun φ => ∫ (x : X), L (↑↑φ x) ∂μ

Tactic:
rw [← funext L.integral_compLp]

Result:
X : Type u_1
E : Type u_3
F : Type u_4
inst✝⁶ : MeasurableSpace X
μ : Measure X
𝕜 : Type u_5
inst✝⁵ : RCLike 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : NormedSpace ℝ F
L : E →L[𝕜] F
⊢ Continuous fun x => ∫ (x_1 : X), ↑↑(L.compLp x) x_1 ∂μ
-- Mathlib/Algebra/Order/GroupWithZero/Unbundled.lean
@[simp] lemma inv_pos : 0 < a⁻¹ ↔ 0 < a :=
  suffices ∀ a : G₀, 0 < a → 0 < a⁻¹ from ⟨fun h ↦ inv_inv a ▸ this _ h, this a⟩
  fun a ha ↦ flip lt_of_mul_lt_mul_left ha.le <| by simp [ne_of_gt ha, zero_lt_one]

Proof state:
G₀ : Type u_2
inst✝³ : GroupWithZero G₀
inst✝² : PartialOrder G₀
inst✝¹ : ZeroLEOneClass G₀
inst✝ : PosMulReflectLT G₀
a✝ a : G₀
ha : 0 < a
⊢ a * 0 < a * a⁻¹

Tactic:
simp [ne_of_gt ha, zero_lt_one]

Result:
no goals
-- Mathlib/GroupTheory/Perm/Sign.lean
theorem sign_trans (f g : Perm α) : sign (f.trans g) = sign g * sign f

Proof state:
α : Type u
inst✝¹ : DecidableEq α
inst✝ : Fintype α
f g : Perm α
⊢ sign (Equiv.trans f g) = sign g * sign f

Tactic:
rw [← mul_def, sign_mul]

Result:
no goals
-- Mathlib/CategoryTheory/Preadditive/Biproducts.lean
theorem Biprod.ofComponents_comp {X₁ X₂ Y₁ Y₂ Z₁ Z₂ : C} (f₁₁ : X₁ ⟶ Y₁) (f₁₂ : X₁ ⟶ Y₂)
    (f₂₁ : X₂ ⟶ Y₁) (f₂₂ : X₂ ⟶ Y₂) (g₁₁ : Y₁ ⟶ Z₁) (g₁₂ : Y₁ ⟶ Z₂) (g₂₁ : Y₂ ⟶ Z₁)
    (g₂₂ : Y₂ ⟶ Z₂) :
    Biprod.ofComponents f₁₁ f₁₂ f₂₁ f₂₂ ≫ Biprod.ofComponents g₁₁ g₁₂ g₂₁ g₂₂ =
      Biprod.ofComponents (f₁₁ ≫ g₁₁ + f₁₂ ≫ g₂₁) (f₁₁ ≫ g₁₂ + f₁₂ ≫ g₂₂) (f₂₁ ≫ g₁₁ + f₂₂ ≫ g₂₁)
        (f₂₁ ≫ g₁₂ + f₂₂ ≫ g₂₂)

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : HasBinaryBiproducts C
X₁ X₂ Y₁ Y₂ Z₁ Z₂ : C
f₁₁ : X₁ ⟶ Y₁
f₁₂ : X₁ ⟶ Y₂
f₂₁ : X₂ ⟶ Y₁
f₂₂ : X₂ ⟶ Y₂
g₁₁ : Y₁ ⟶ Z₁
g₁₂ : Y₁ ⟶ Z₂
g₂₁ : Y₂ ⟶ Z₁
g₂₂ : Y₂ ⟶ Z₂
⊢ ofComponents f₁₁ f₁₂ f₂₁ f₂₂ ≫ ofComponents g₁₁ g₁₂ g₂₁ g₂₂ =
    ofComponents (f₁₁ ≫ g₁₁ + f₁₂ ≫ g₂₁) (f₁₁ ≫ g₁₂ + f₁₂ ≫ g₂₂) (f₂₁ ≫ g₁₁ + f₂₂ ≫ g₂₁) (f₂₁ ≫ g₁₂ + f₂₂ ≫ g₂₂)

Tactic:
dsimp [Biprod.ofComponents]

Result:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : HasBinaryBiproducts C
X₁ X₂ Y₁ Y₂ Z₁ Z₂ : C
f₁₁ : X₁ ⟶ Y₁
f₁₂ : X₁ ⟶ Y₂
f₂₁ : X₂ ⟶ Y₁
f₂₂ : X₂ ⟶ Y₂
g₁₁ : Y₁ ⟶ Z₁
g₁₂ : Y₁ ⟶ Z₂
g₂₁ : Y₂ ⟶ Z₁
g₂₂ : Y₂ ⟶ Z₂
⊢ (biprod.fst ≫ f₁₁ ≫ biprod.inl + biprod.fst ≫ f₁₂ ≫ biprod.inr + biprod.snd ≫ f₂₁ ≫ biprod.inl +
        biprod.snd ≫ f₂₂ ≫ biprod.inr) ≫
      (biprod.fst ≫ g₁₁ ≫ biprod.inl + biprod.fst ≫ g₁₂ ≫ biprod.inr + biprod.snd ≫ g₂₁ ≫ biprod.inl +
        biprod.snd ≫ g₂₂ ≫ biprod.inr) =
    biprod.fst ≫ (f₁₁ ≫ g₁₁ + f₁₂ ≫ g₂₁) ≫ biprod.inl + biprod.fst ≫ (f₁₁ ≫ g₁₂ + f₁₂ ≫ g₂₂) ≫ biprod.inr +
        biprod.snd ≫ (f₂₁ ≫ g₁₁ + f₂₂ ≫ g₂₁) ≫ biprod.inl +
      biprod.snd ≫ (f₂₁ ≫ g₁₂ + f₂₂ ≫ g₂₂) ≫ biprod.inr

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : HasBinaryBiproducts C
X₁ X₂ Y₁ Y₂ Z₁ Z₂ : C
f₁₁ : X₁ ⟶ Y₁
f₁₂ : X₁ ⟶ Y₂
f₂₁ : X₂ ⟶ Y₁
f₂₂ : X₂ ⟶ Y₂
g₁₁ : Y₁ ⟶ Z₁
g₁₂ : Y₁ ⟶ Z₂
g₂₁ : Y₂ ⟶ Z₁
g₂₂ : Y₂ ⟶ Z₂
⊢ (biprod.fst ≫ f₁₁ ≫ biprod.inl + biprod.fst ≫ f₁₂ ≫ biprod.inr + biprod.snd ≫ f₂₁ ≫ biprod.inl +
        biprod.snd ≫ f₂₂ ≫ biprod.inr) ≫
      (biprod.fst ≫ g₁₁ ≫ biprod.inl + biprod.fst ≫ g₁₂ ≫ biprod.inr + biprod.snd ≫ g₂₁ ≫ biprod.inl +
        biprod.snd ≫ g₂₂ ≫ biprod.inr) =
    biprod.fst ≫ (f₁₁ ≫ g₁₁ + f₁₂ ≫ g₂₁) ≫ biprod.inl + biprod.fst ≫ (f₁₁ ≫ g₁₂ + f₁₂ ≫ g₂₂) ≫ biprod.inr +
        biprod.snd ≫ (f₂₁ ≫ g₁₁ + f₂₂ ≫ g₂₁) ≫ biprod.inl +
      biprod.snd ≫ (f₂₁ ≫ g₁₂ + f₂₂ ≫ g₂₂) ≫ biprod.inr

Tactic:
ext <;>
  simp only [add_comp, comp_add, add_comp_assoc, add_zero, zero_add, biprod.inl_fst,
    biprod.inl_snd, biprod.inr_fst, biprod.inr_snd, biprod.inl_fst_assoc, biprod.inl_snd_assoc,
    biprod.inr_fst_assoc, biprod.inr_snd_assoc, comp_zero, zero_comp, Category.assoc]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Find.lean
theorem find?_flatMap_eq_none_iff {xs : List α} {f : α → List β} {p : β → Bool} :
    (xs.flatMap f).find? p = none ↔ ∀ x ∈ xs, ∀ y ∈ f x, !p y

Proof state:
α : Type u_1
β : Type u_2
xs : List α
f : α → List β
p : β → Bool
⊢ find? p (flatMap f xs) = none ↔ ∀ (x : α), x ∈ xs → ∀ (y : β), y ∈ f x → (!p y) = true

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Group/Invertible/Defs.lean
theorem invOf_mul_eq_iff_eq_mul_left : ⅟c * a = b ↔ a = c * b

Proof state:
α : Type u
inst✝¹ : Monoid α
a b c : α
inst✝ : Invertible c
⊢ ⅟c * a = b ↔ a = c * b

Tactic:
rw [← mul_right_inj_of_invertible (c := c), mul_invOf_cancel_left]

Result:
no goals
-- Mathlib/RingTheory/Flat/FaithfullyFlat/Basic.lean
/-- If `M` is a faithfully flat `R`-module and `N` is `R`-linearly isomorphic to `M`, then
`N` is faithfully flat. -/
lemma of_linearEquiv {N : Type*} [AddCommGroup N] [Module R N] [FaithfullyFlat R M]
    (e : N ≃ₗ[R] M) : FaithfullyFlat R N

Proof state:
R : Type u
M : Type v
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
N : Type u_1
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : FaithfullyFlat R M
e : N ≃ₗ[R] M
⊢ Flat R N ∧
    ∀ (N_1 : Type (max u u_1)) [inst : AddCommGroup N_1] [inst_1 : Module R N_1],
      Nontrivial N_1 → Nontrivial (N ⊗[R] N_1)

Tactic:
exact ⟨Flat.of_linearEquiv e,
  fun P _ _ hP ↦ (TensorProduct.congr e (LinearEquiv.refl R P)).toEquiv.nontrivial⟩

Result:
no goals

Proof state:
R : Type u
M : Type v
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
N : Type u_1
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : FaithfullyFlat R M
e : N ≃ₗ[R] M
⊢ FaithfullyFlat R N

Tactic:
rw [iff_flat_and_lTensor_faithful]

Result:
R : Type u
M : Type v
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
N : Type u_1
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : FaithfullyFlat R M
e : N ≃ₗ[R] M
⊢ Flat R N ∧
    ∀ (N_1 : Type (max u u_1)) [inst : AddCommGroup N_1] [inst_1 : Module R N_1],
      Nontrivial N_1 → Nontrivial (N ⊗[R] N_1)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem map_eq_iff : map f l = l' ↔ ∀ i : Nat, l'[i]? = l[i]?.map f

Proof state:
case mpr
α✝¹ : Type u_1
α✝ : Type u_2
f : α✝¹ → α✝
l : List α✝¹
l' : List α✝
⊢ (∀ (i : Nat), l'[i]? = Option.map f l[i]?) → map f l = l'

Tactic:
intro h

Result:
case mpr
α✝¹ : Type u_1
α✝ : Type u_2
f : α✝¹ → α✝
l : List α✝¹
l' : List α✝
h : ∀ (i : Nat), l'[i]? = Option.map f l[i]?
⊢ map f l = l'

Proof state:
case mp
α✝¹ : Type u_1
α✝ : Type u_2
f : α✝¹ → α✝
l : List α✝¹
i : Nat
⊢ (map f l)[i]? = Option.map f l[i]?

Tactic:
simp

Result:
no goals

Proof state:
case mpr.h
α✝¹ : Type u_1
α✝ : Type u_2
f : α✝¹ → α✝
l : List α✝¹
l' : List α✝
h : ∀ (i : Nat), l'[i]? = Option.map f l[i]?
i : Nat
⊢ (map f l)[i]? = l'[i]?

Tactic:
simp_all

Result:
no goals

Proof state:
case mp
α✝¹ : Type u_1
α✝ : Type u_2
f : α✝¹ → α✝
l : List α✝¹
l' : List α✝
⊢ map f l = l' → ∀ (i : Nat), l'[i]? = Option.map f l[i]?

Tactic:
rintro rfl i

Result:
case mp
α✝¹ : Type u_1
α✝ : Type u_2
f : α✝¹ → α✝
l : List α✝¹
i : Nat
⊢ (map f l)[i]? = Option.map f l[i]?

Proof state:
α✝¹ : Type u_1
α✝ : Type u_2
f : α✝¹ → α✝
l : List α✝¹
l' : List α✝
⊢ map f l = l' ↔ ∀ (i : Nat), l'[i]? = Option.map f l[i]?

Tactic:
constructor

Result:
case mp
α✝¹ : Type u_1
α✝ : Type u_2
f : α✝¹ → α✝
l : List α✝¹
l' : List α✝
⊢ map f l = l' → ∀ (i : Nat), l'[i]? = Option.map f l[i]?

case mpr
α✝¹ : Type u_1
α✝ : Type u_2
f : α✝¹ → α✝
l : List α✝¹
l' : List α✝
⊢ (∀ (i : Nat), l'[i]? = Option.map f l[i]?) → map f l = l'

Proof state:
case mpr
α✝¹ : Type u_1
α✝ : Type u_2
f : α✝¹ → α✝
l : List α✝¹
l' : List α✝
h : ∀ (i : Nat), l'[i]? = Option.map f l[i]?
⊢ map f l = l'

Tactic:
ext1 i

Result:
case mpr.h
α✝¹ : Type u_1
α✝ : Type u_2
f : α✝¹ → α✝
l : List α✝¹
l' : List α✝
h : ∀ (i : Nat), l'[i]? = Option.map f l[i]?
i : Nat
⊢ (map f l)[i]? = l'[i]?
-- Mathlib/Topology/UniformSpace/Compact.lean
theorem lebesgue_number_lemma_sUnion {S : Set (Set α)}
    (hK : IsCompact K) (hopen : ∀ s ∈ S, IsOpen s) (hcover : K ⊆ ⋃₀ S) :
    ∃ V ∈ 𝓤 α, ∀ x ∈ K, ∃ s ∈ S, ball x V ⊆ s

Proof state:
α : Type ua
inst✝ : UniformSpace α
K : Set α
S : Set (Set α)
hK : IsCompact K
hopen : ∀ s ∈ S, IsOpen s
hcover : K ⊆ ⋃ i, ↑i
⊢ ∃ V ∈ 𝓤 α, ∀ x ∈ K, ∃ s ∈ S, ball x V ⊆ s

Tactic:
simpa using lebesgue_number_lemma hK (by simpa) hcover

Result:
no goals

Proof state:
α : Type ua
inst✝ : UniformSpace α
K : Set α
S : Set (Set α)
hK : IsCompact K
hopen : ∀ s ∈ S, IsOpen s
hcover : K ⊆ ⋃₀ S
⊢ ∃ V ∈ 𝓤 α, ∀ x ∈ K, ∃ s ∈ S, ball x V ⊆ s

Tactic:
rw [sUnion_eq_iUnion] at hcover

Result:
α : Type ua
inst✝ : UniformSpace α
K : Set α
S : Set (Set α)
hK : IsCompact K
hopen : ∀ s ∈ S, IsOpen s
hcover : K ⊆ ⋃ i, ↑i
⊢ ∃ V ∈ 𝓤 α, ∀ x ∈ K, ∃ s ∈ S, ball x V ⊆ s

Proof state:
α : Type ua
inst✝ : UniformSpace α
K : Set α
S : Set (Set α)
hK : IsCompact K
hopen : ∀ s ∈ S, IsOpen s
hcover : K ⊆ ⋃ i, ↑i
⊢ ∀ (i : ↑S), IsOpen ↑i

Tactic:
simpa

Result:
no goals
-- Mathlib/RingTheory/IntegralClosure/IsIntegralClosure/Basic.lean
theorem RingHom.IsIntegral.quotient {I : Ideal S} (hf : f.IsIntegral) :
    (Ideal.quotientMap I f le_rfl).IsIntegral

Proof state:
case mk
R : Type u_1
S : Type u_4
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
I : Ideal S
hf : f.IsIntegral
x✝ : S ⧸ I
x : S
⊢ (Ideal.quotientMap I f ⋯).IsIntegralElem (Quot.mk (⇑(quotientRel I)) x)

Tactic:
obtain ⟨p, p_monic, hpx⟩ := hf x

Result:
case mk.intro.intro
R : Type u_1
S : Type u_4
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
I : Ideal S
hf : f.IsIntegral
x✝ : S ⧸ I
x : S
p : R[X]
p_monic : p.Monic
hpx : eval₂ f x p = 0
⊢ (Ideal.quotientMap I f ⋯).IsIntegralElem (Quot.mk (⇑(quotientRel I)) x)

Proof state:
case mk.intro.intro
R : Type u_1
S : Type u_4
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
I : Ideal S
hf : f.IsIntegral
x✝ : S ⧸ I
x : S
p : R[X]
p_monic : p.Monic
hpx : eval₂ f x p = 0
⊢ (Ideal.quotientMap I f ⋯).IsIntegralElem (Quot.mk (⇑(quotientRel I)) x)

Tactic:
refine ⟨p.map (Ideal.Quotient.mk _), p_monic.map _, ?_⟩

Result:
case mk.intro.intro
R : Type u_1
S : Type u_4
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
I : Ideal S
hf : f.IsIntegral
x✝ : S ⧸ I
x : S
p : R[X]
p_monic : p.Monic
hpx : eval₂ f x p = 0
⊢ eval₂ (Ideal.quotientMap I f ⋯) (Quot.mk (⇑(quotientRel I)) x)
      (Polynomial.map (Ideal.Quotient.mk (Ideal.comap f I)) p) =
    0

Proof state:
R : Type u_1
S : Type u_4
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
I : Ideal S
hf : f.IsIntegral
⊢ (Ideal.quotientMap I f ⋯).IsIntegral

Tactic:
rintro ⟨x⟩

Result:
case mk
R : Type u_1
S : Type u_4
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
I : Ideal S
hf : f.IsIntegral
x✝ : S ⧸ I
x : S
⊢ (Ideal.quotientMap I f ⋯).IsIntegralElem (Quot.mk (⇑(quotientRel I)) x)

Proof state:
case mk.intro.intro
R : Type u_1
S : Type u_4
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
I : Ideal S
hf : f.IsIntegral
x✝ : S ⧸ I
x : S
p : R[X]
p_monic : p.Monic
hpx : eval₂ f x p = 0
⊢ eval₂ (Ideal.quotientMap I f ⋯) (Quot.mk (⇑(quotientRel I)) x)
      (Polynomial.map (Ideal.Quotient.mk (Ideal.comap f I)) p) =
    0

Tactic:
simpa only [hom_eval₂, eval₂_map] using congr_arg (Ideal.Quotient.mk I) hpx

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem fill_true {w : Nat} : fill w true = allOnes w

Proof state:
w : Nat
⊢ fill w true = allOnes w

Tactic:
simp [fill_eq]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/TypesFiltered.lean
theorem rel_of_quot_rel (x y : Σ j, F.obj j) :
    Quot.Rel F x y → FilteredColimit.Rel.{v, u} F x y :=
  fun ⟨f, h⟩ => ⟨y.1, f, 𝟙 y.1, by rw [← h, FunctorToTypes.map_id_apply]⟩

Proof state:
J : Type v
inst✝ : Category.{w, v} J
F : J ⥤ Type u
x y : (j : J) × F.obj j
x✝ : Quot.Rel F x y
f : x.fst ⟶ y.fst
h : y.snd = F.map f x.snd
⊢ F.map f x.snd = F.map (𝟙 y.fst) y.snd

Tactic:
rw [← h, FunctorToTypes.map_id_apply]

Result:
no goals
-- Mathlib/MeasureTheory/Function/LocallyIntegrable.lean
theorem LocallyIntegrableOn.mono (hf : LocallyIntegrableOn f s μ) {g : X → F}
    (hg : AEStronglyMeasurable g μ) (h : ∀ᵐ x ∂μ, ‖g x‖ ≤ ‖f x‖) :
    LocallyIntegrableOn g s μ

Proof state:
X : Type u_1
E : Type u_3
F : Type u_4
inst✝³ : MeasurableSpace X
inst✝² : TopologicalSpace X
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedAddCommGroup F
f : X → E
μ : Measure X
s : Set X
hf : LocallyIntegrableOn f s μ
g : X → F
hg : AEStronglyMeasurable g μ
h : ∀ᵐ (x : X) ∂μ, ‖g x‖ ≤ ‖f x‖
⊢ LocallyIntegrableOn g s μ

Tactic:
intro x hx

Result:
X : Type u_1
E : Type u_3
F : Type u_4
inst✝³ : MeasurableSpace X
inst✝² : TopologicalSpace X
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedAddCommGroup F
f : X → E
μ : Measure X
s : Set X
hf : LocallyIntegrableOn f s μ
g : X → F
hg : AEStronglyMeasurable g μ
h : ∀ᵐ (x : X) ∂μ, ‖g x‖ ≤ ‖f x‖
x : X
hx : x ∈ s
⊢ IntegrableAtFilter g (𝓝[s] x) μ

Proof state:
case intro.intro
X : Type u_1
E : Type u_3
F : Type u_4
inst✝³ : MeasurableSpace X
inst✝² : TopologicalSpace X
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedAddCommGroup F
f : X → E
μ : Measure X
s : Set X
hf : LocallyIntegrableOn f s μ
g : X → F
hg : AEStronglyMeasurable g μ
h : ∀ᵐ (x : X) ∂μ, ‖g x‖ ≤ ‖f x‖
x : X
hx : x ∈ s
t : Set X
t_mem : t ∈ 𝓝[s] x
ht : IntegrableOn f t μ
⊢ IntegrableAtFilter g (𝓝[s] x) μ

Tactic:
exact ⟨t, t_mem, Integrable.mono ht hg.restrict (ae_restrict_of_ae h)⟩

Result:
no goals

Proof state:
X : Type u_1
E : Type u_3
F : Type u_4
inst✝³ : MeasurableSpace X
inst✝² : TopologicalSpace X
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedAddCommGroup F
f : X → E
μ : Measure X
s : Set X
hf : LocallyIntegrableOn f s μ
g : X → F
hg : AEStronglyMeasurable g μ
h : ∀ᵐ (x : X) ∂μ, ‖g x‖ ≤ ‖f x‖
x : X
hx : x ∈ s
⊢ IntegrableAtFilter g (𝓝[s] x) μ

Tactic:
rcases hf x hx with ⟨t, t_mem, ht⟩

Result:
case intro.intro
X : Type u_1
E : Type u_3
F : Type u_4
inst✝³ : MeasurableSpace X
inst✝² : TopologicalSpace X
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedAddCommGroup F
f : X → E
μ : Measure X
s : Set X
hf : LocallyIntegrableOn f s μ
g : X → F
hg : AEStronglyMeasurable g μ
h : ∀ᵐ (x : X) ∂μ, ‖g x‖ ≤ ‖f x‖
x : X
hx : x ∈ s
t : Set X
t_mem : t ∈ 𝓝[s] x
ht : IntegrableOn f t μ
⊢ IntegrableAtFilter g (𝓝[s] x) μ
-- Mathlib/AlgebraicTopology/SimplicialSet/Basic.lean
lemma δ_comp_σ_of_gt'_apply {n} {i : Fin (n + 3)} {j : Fin (n + 2)} (H : j.succ < i)
    (x : S _⦋n + 1⦌) : S.δ i (S.σ j x) =
      S.σ (j.castLT ((add_lt_add_iff_right 1).mp (lt_of_lt_of_le H i.is_le)))
        (S.δ (i.pred fun (hi : i = 0) => by simp only [Fin.not_lt_zero, hi] at H) x) :=
  congr_fun (S.δ_comp_σ_of_gt' H) x

Proof state:
S : SSet
n : ℕ
i : Fin (n + 3)
j : Fin (n + 2)
H : j.succ < i
x : S _⦋n + 1⦌
hi : i = 0
⊢ False

Tactic:
simp only [Fin.not_lt_zero, hi] at H

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

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

Tactic:
simp only [support_bindOnSupport, Set.mem_setOf_eq, Set.mem_iUnion]

Result:
no goals
-- Mathlib/Analysis/Convex/Strong.lean
@[simp] lemma uniformConcaveOn_zero : UniformConcaveOn s 0 f ↔ ConcaveOn ℝ s f

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
s : Set E
f : E → ℝ
⊢ UniformConcaveOn s 0 f ↔ ConcaveOn ℝ s f

Tactic:
simp [UniformConcaveOn, ConcaveOn]

Result:
no goals
-- Mathlib/Data/Matroid/Rank/Finite.lean
lemma IsRkFinite.isRkFinite_diff_iff (hX : M.IsRkFinite X) :
    M.IsRkFinite (Y \ X) ↔ M.IsRkFinite Y

Proof state:
α : Type u_1
M : Matroid α
X Y : Set α
hX : M.IsRkFinite X
⊢ M.IsRkFinite (Y \ X) ↔ M.IsRkFinite Y

Tactic:
rw [← hX.isRkFinite_union_iff, union_diff_self, hX.isRkFinite_union_iff]

Result:
no goals
-- Mathlib/Algebra/Tropical/BigOperators.lean
theorem Finset.untrop_sum [ConditionallyCompleteLinearOrder R] (s : Finset S)
    (f : S → Tropical (WithTop R)) : untrop (∑ i ∈ s, f i) = ⨅ i : s, untrop (f i)

Proof state:
R : Type u_1
S : Type u_2
inst✝ : ConditionallyCompleteLinearOrder R
s : Finset S
f : S → Tropical (WithTop R)
⊢ untrop (∑ i ∈ s, f i) = ⨅ i, untrop (f ↑i)

Tactic:
simpa [← _root_.untrop_sum] using (sum_attach _ _).symm

Result:
no goals
-- Mathlib/Order/Defs/Unbundled.lean
theorem trans_trichotomous_right [IsTrans α r] [IsTrichotomous α r] {a b c : α}
    (h₁ : r a b) (h₂ : ¬r c b) : r a c

Proof state:
case inr.inr
α : Type u_1
r : α → α → Prop
inst✝¹ : IsTrans α r
inst✝ : IsTrichotomous α r
a b c : α
h₁ : r a b
h₂ : ¬r c b
h₃ : r c b
⊢ r a c

Tactic:
exact absurd h₃ h₂

Result:
no goals

Proof state:
α : Type u_1
r : α → α → Prop
inst✝¹ : IsTrans α r
inst✝ : IsTrichotomous α r
a b c : α
h₁ : r a b
h₂ : ¬r c b
⊢ r a c

Tactic:
rcases trichotomous_of r b c with (h₃ | rfl | h₃)

Result:
case inl
α : Type u_1
r : α → α → Prop
inst✝¹ : IsTrans α r
inst✝ : IsTrichotomous α r
a b c : α
h₁ : r a b
h₂ : ¬r c b
h₃ : r b c
⊢ r a c

case inr.inl
α : Type u_1
r : α → α → Prop
inst✝¹ : IsTrans α r
inst✝ : IsTrichotomous α r
a b : α
h₁ : r a b
h₂ : ¬r b b
⊢ r a b

case inr.inr
α : Type u_1
r : α → α → Prop
inst✝¹ : IsTrans α r
inst✝ : IsTrichotomous α r
a b c : α
h₁ : r a b
h₂ : ¬r c b
h₃ : r c b
⊢ r a c

Proof state:
case inl
α : Type u_1
r : α → α → Prop
inst✝¹ : IsTrans α r
inst✝ : IsTrichotomous α r
a b c : α
h₁ : r a b
h₂ : ¬r c b
h₃ : r b c
⊢ r a c

Tactic:
exact _root_.trans h₁ h₃

Result:
no goals

Proof state:
case inr.inl
α : Type u_1
r : α → α → Prop
inst✝¹ : IsTrans α r
inst✝ : IsTrichotomous α r
a b : α
h₁ : r a b
h₂ : ¬r b b
⊢ r a b

Tactic:
exact h₁

Result:
no goals
-- Mathlib/Algebra/Polynomial/Eval/Defs.lean
theorem mul_X_comp : (p * X).comp r = p.comp r * r

Proof state:
case h_monomial
R : Type u
inst✝ : Semiring R
p r : R[X]
n : ℕ
b : R
⊢ ((monomial n) b * X).comp r = ((monomial n) b).comp r * r

Tactic:
simp only [pow_succ, mul_assoc, monomial_mul_X, monomial_comp]

Result:
no goals

Proof state:
R : Type u
inst✝ : Semiring R
p r : R[X]
⊢ (p * X).comp r = p.comp r * r

Tactic:
induction p using Polynomial.induction_on' with
| h_add p q hp hq =>
  simp only [hp, hq, add_mul, add_comp]
| h_monomial n b =>
  simp only [pow_succ, mul_assoc, monomial_mul_X, monomial_comp]

Result:
no goals

Proof state:
case h_add
R : Type u
inst✝ : Semiring R
p✝ r p q : R[X]
hp : (p * X).comp r = p.comp r * r
hq : (q * X).comp r = q.comp r * r
⊢ ((p + q) * X).comp r = (p + q).comp r * r

Tactic:
simp only [hp, hq, add_mul, add_comp]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Nat/Range.lean
theorem mem_iota {m n : Nat} : m ∈ iota n ↔ 0 < m ∧ m ≤ n

Proof state:
m n : Nat
⊢ m ∈ iota n ↔ 0 < m ∧ m ≤ n

Tactic:
simp [iota_eq_reverse_range', Nat.add_comm, Nat.lt_succ]

Result:
m n : Nat
⊢ m ≤ n → (1 ≤ m ↔ 0 < m)

Proof state:
m n : Nat
⊢ m ≤ n → (1 ≤ m ↔ 0 < m)

Tactic:
omega

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem twoPow_zero {w : Nat} : twoPow w 0 = 1#w

Proof state:
w : Nat
⊢ twoPow w 0 = 1#w

Tactic:
apply eq_of_toNat_eq

Result:
case a
w : Nat
⊢ (twoPow w 0).toNat = (1#w).toNat

Proof state:
case a
w : Nat
⊢ (twoPow w 0).toNat = (1#w).toNat

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Polynomial/Degree/Units.lean
@[simp] lemma natDegree_coe_units (u : R[X]ˣ) : natDegree (u : R[X]) = 0

Proof state:
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
u : R[X]ˣ
a✝ : Nontrivial R
⊢ (↑u).natDegree = 0

Tactic:
exact natDegree_eq_of_degree_eq_some (degree_coe_units u)

Result:
no goals

Proof state:
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
u : R[X]ˣ
⊢ (↑u).natDegree = 0

Tactic:
nontriviality R

Result:
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
u : R[X]ˣ
a✝ : Nontrivial R
⊢ (↑u).natDegree = 0
-- Mathlib/RingTheory/Ideal/MinimalPrime/Localization.lean
theorem Ideal.minimalPrimes_eq_comap :
    I.minimalPrimes = Ideal.comap (Ideal.Quotient.mk I) '' minimalPrimes (R ⧸ I)

Proof state:
R : Type u_1
inst✝ : CommRing R
I : Ideal R
⊢ I.minimalPrimes = comap (Quotient.mk I) '' minimalPrimes (R ⧸ I)

Tactic:
rw [minimalPrimes, ← Ideal.comap_minimalPrimes_eq_of_surjective Ideal.Quotient.mk_surjective,
  ← RingHom.ker_eq_comap_bot, Ideal.mk_ker]

Result:
no goals
-- Mathlib/Analysis/Convex/Mul.lean
lemma ConcaveOn.smul'' (hf : ConcaveOn 𝕜 s f) (hg : ConcaveOn 𝕜 s g) (hf₀ : ∀ ⦃x⦄, x ∈ s → f x ≤ 0)
    (hg₀ : ∀ ⦃x⦄, x ∈ s → g x ≤ 0) (hfg : MonovaryOn f g s) : ConvexOn 𝕜 s (f • g)

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁹ : LinearOrderedCommRing 𝕜
inst✝⁸ : LinearOrderedCommRing E
inst✝⁷ : LinearOrderedAddCommGroup F
inst✝⁶ : Module 𝕜 E
inst✝⁵ : Module 𝕜 F
inst✝⁴ : Module E F
inst✝³ : IsScalarTower 𝕜 E F
inst✝² : SMulCommClass 𝕜 E F
inst✝¹ : OrderedSMul 𝕜 F
inst✝ : OrderedSMul E F
s : Set 𝕜
f : 𝕜 → E
g : 𝕜 → F
hf : ConcaveOn 𝕜 s f
hg : ConcaveOn 𝕜 s g
hf₀ : ∀ ⦃x : 𝕜⦄, x ∈ s → f x ≤ 0
hg₀ : ∀ ⦃x : 𝕜⦄, x ∈ s → g x ≤ 0
hfg : MonovaryOn f g s
⊢ ConvexOn 𝕜 s (f • g)

Tactic:
rw [← neg_smul_neg]

Result:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁹ : LinearOrderedCommRing 𝕜
inst✝⁸ : LinearOrderedCommRing E
inst✝⁷ : LinearOrderedAddCommGroup F
inst✝⁶ : Module 𝕜 E
inst✝⁵ : Module 𝕜 F
inst✝⁴ : Module E F
inst✝³ : IsScalarTower 𝕜 E F
inst✝² : SMulCommClass 𝕜 E F
inst✝¹ : OrderedSMul 𝕜 F
inst✝ : OrderedSMul E F
s : Set 𝕜
f : 𝕜 → E
g : 𝕜 → F
hf : ConcaveOn 𝕜 s f
hg : ConcaveOn 𝕜 s g
hf₀ : ∀ ⦃x : 𝕜⦄, x ∈ s → f x ≤ 0
hg₀ : ∀ ⦃x : 𝕜⦄, x ∈ s → g x ≤ 0
hfg : MonovaryOn f g s
⊢ ConvexOn 𝕜 s (-f • -g)

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁹ : LinearOrderedCommRing 𝕜
inst✝⁸ : LinearOrderedCommRing E
inst✝⁷ : LinearOrderedAddCommGroup F
inst✝⁶ : Module 𝕜 E
inst✝⁵ : Module 𝕜 F
inst✝⁴ : Module E F
inst✝³ : IsScalarTower 𝕜 E F
inst✝² : SMulCommClass 𝕜 E F
inst✝¹ : OrderedSMul 𝕜 F
inst✝ : OrderedSMul E F
s : Set 𝕜
f : 𝕜 → E
g : 𝕜 → F
hf : ConcaveOn 𝕜 s f
hg : ConcaveOn 𝕜 s g
hf₀ : ∀ ⦃x : 𝕜⦄, x ∈ s → f x ≤ 0
hg₀ : ∀ ⦃x : 𝕜⦄, x ∈ s → g x ≤ 0
hfg : MonovaryOn f g s
⊢ ConvexOn 𝕜 s (-f • -g)

Tactic:
exact hf.neg.smul' hg.neg (fun x hx ↦ neg_nonneg.2 <| hf₀ hx) (fun x hx ↦ neg_nonneg.2 <| hg₀ hx)
  hfg.neg

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem and_any_distrib_right (l : List α) (p : α → Bool) (q : Bool) :
    (l.any p && q) = l.any fun a => p a && q

Proof state:
α : Type u_1
l : List α
p : α → Bool
q : Bool
⊢ (l.any p && q) = l.any fun a => p a && q

Tactic:
induction l with simp | cons _ _ ih => rw [Bool.and_or_distrib_right, ih]

Result:
no goals

Proof state:
case cons
α : Type u_1
p : α → Bool
q : Bool
head✝ : α
tail✝ : List α
ih : (tail✝.any p && q) = tail✝.any fun a => p a && q
⊢ ((p head✝ || tail✝.any p) && q) = (p head✝ && q || tail✝.any fun a => p a && q)

Tactic:
rw [Bool.and_or_distrib_right, ih]

Result:
no goals