harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/GroupTheory/Perm/Support.lean
theorem support_prod_le (l : List (Perm α)) : l.prod.support ≤ (l.map support).foldr (· ⊔ ·) ⊥

Proof state:
case cons
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hd : Perm α
tl : List (Perm α)
hl : tl.prod.support ≤ List.foldr (fun x1 x2 => x1 ⊔ x2) ⊥ (List.map support tl)
⊢ hd.support ⊔ tl.prod.support ≤ hd.support ⊔ List.foldr (fun x1 x2 => x1 ⊔ x2) ⊥ (List.map support tl)

Tactic:
exact sup_le_sup le_rfl hl

Result:
no goals

Proof state:
case nil
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
⊢ [].prod.support ≤ List.foldr (fun x1 x2 => x1 ⊔ x2) ⊥ (List.map support [])

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
l : List (Perm α)
⊢ l.prod.support ≤ List.foldr (fun x1 x2 => x1 ⊔ x2) ⊥ (List.map support l)

Tactic:
induction' l with hd tl hl

Result:
case nil
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
⊢ [].prod.support ≤ List.foldr (fun x1 x2 => x1 ⊔ x2) ⊥ (List.map support [])

case cons
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hd : Perm α
tl : List (Perm α)
hl : tl.prod.support ≤ List.foldr (fun x1 x2 => x1 ⊔ x2) ⊥ (List.map support tl)
⊢ (hd :: tl).prod.support ≤ List.foldr (fun x1 x2 => x1 ⊔ x2) ⊥ (List.map support (hd :: tl))

Proof state:
case cons
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hd : Perm α
tl : List (Perm α)
hl : tl.prod.support ≤ List.foldr (fun x1 x2 => x1 ⊔ x2) ⊥ (List.map support tl)
⊢ (hd * tl.prod).support ≤ hd.support ⊔ List.foldr (fun x1 x2 => x1 ⊔ x2) ⊥ (List.map support tl)

Tactic:
refine (support_mul_le hd tl.prod).trans ?_

Result:
case cons
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hd : Perm α
tl : List (Perm α)
hl : tl.prod.support ≤ List.foldr (fun x1 x2 => x1 ⊔ x2) ⊥ (List.map support tl)
⊢ hd.support ⊔ tl.prod.support ≤ hd.support ⊔ List.foldr (fun x1 x2 => x1 ⊔ x2) ⊥ (List.map support tl)

Proof state:
case cons
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hd : Perm α
tl : List (Perm α)
hl : tl.prod.support ≤ List.foldr (fun x1 x2 => x1 ⊔ x2) ⊥ (List.map support tl)
⊢ (hd :: tl).prod.support ≤ List.foldr (fun x1 x2 => x1 ⊔ x2) ⊥ (List.map support (hd :: tl))

Tactic:
rw [List.prod_cons, List.map_cons, List.foldr_cons]

Result:
case cons
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
hd : Perm α
tl : List (Perm α)
hl : tl.prod.support ≤ List.foldr (fun x1 x2 => x1 ⊔ x2) ⊥ (List.map support tl)
⊢ (hd * tl.prod).support ≤ hd.support ⊔ List.foldr (fun x1 x2 => x1 ⊔ x2) ⊥ (List.map support tl)
-- Mathlib/LinearAlgebra/Matrix/Determinant/Basic.lean
theorem det_mul_row (v : n → R) (A : Matrix n n R) :
    det (of fun i j => v j * A i j) = (∏ i, v i) * det A :=
  calc
    det (of fun i j => v j * A i j) = det (A * diagonal v) :=
      congr_arg det <| by
        ext
        simp [mul_comm]
    _ = (∏ i, v i) * det A

Proof state:
n : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
v : n → R
A : Matrix n n R
⊢ (of fun i j => v j * A i j) = A * diagonal v

Tactic:
ext

Result:
case a
n : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
v : n → R
A : Matrix n n R
i✝ j✝ : n
⊢ of (fun i j => v j * A i j) i✝ j✝ = (A * diagonal v) i✝ j✝

Proof state:
case a
n : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
v : n → R
A : Matrix n n R
i✝ j✝ : n
⊢ of (fun i j => v j * A i j) i✝ j✝ = (A * diagonal v) i✝ j✝

Tactic:
simp [mul_comm]

Result:
no goals

Proof state:
n : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
v : n → R
A : Matrix n n R
⊢ (A * diagonal v).det = (∏ i : n, v i) * A.det

Tactic:
rw [det_mul, det_diagonal, mul_comm]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem getD_insert_self [LawfulBEq α] (h : m.1.WF) {a : α} {fallback b : β a} :
    (m.insert a b).getD a fallback = b

Proof state:
α : Type u
β : α → Type v
m : Raw₀ α β
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulBEq α
h : m.val.WF
a : α
fallback b : β a
⊢ (m.insert a b).getD a fallback = b

Tactic:
simp_to_model [insert] using List.getValueCastD_insertEntry_self

Result:
no goals
-- Mathlib/CategoryTheory/Enriched/HomCongr.lean
/-- `eHomCongr` respects composition of morphisms. Recall that for any
composable pair of arrows `f : X ⟶ Y` and `g : Y ⟶ Z` in `C`, the composite
`f ≫ g` in `C` defines a morphism `𝟙_ V ⟶ (X ⟶[V] Z)` in `V`. Composing with
the isomorphism `eHomCongr V α γ` yields a morphism in `V` that can be factored
through the enriched composition map as shown:
`𝟙_ V ⟶ 𝟙_ V ⊗ 𝟙_ V ⟶ (X₁ ⟶[V] Y₁) ⊗ (Y₁ ⟶[V] Z₁) ⟶ (X₁ ⟶[V] Z₁)`. -/
@[reassoc]
lemma eHomCongr_comp {X Y Z X₁ Y₁ Z₁ : C} (α : X ≅ X₁) (β : Y ≅ Y₁) (γ : Z ≅ Z₁)
    (f : X ⟶ Y) (g : Y ⟶ Z) :
    eHomEquiv V (f ≫ g) ≫ (eHomCongr V α γ).hom =
      (λ_ _).inv ≫ (eHomEquiv V f ≫ (eHomCongr V α β).hom) ▷ _ ≫
        _ ◁ (eHomEquiv V g ≫ (eHomCongr V β γ).hom) ≫ eComp V X₁ Y₁ Z₁

Proof state:
V : Type u'
inst✝³ : Category.{v', u'} V
inst✝² : MonoidalCategory V
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : EnrichedOrdinaryCategory V C
X Y Z X₁ Y₁ Z₁ : C
α : X ≅ X₁
β : Y ≅ Y₁
γ : Z ≅ Z₁
f : X ⟶ Y
g : Y ⟶ Z
⊢ (eHomEquiv V) (f ≫ g) ≫ (eHomCongr V α γ).hom =
    (λ_ (𝟙_ V)).inv ≫
      ((eHomEquiv V) f ≫ (eHomCongr V α β).hom) ▷ 𝟙_ V ≫
        EnrichedCategory.Hom X₁ Y₁ ◁ ((eHomEquiv V) g ≫ (eHomCongr V β γ).hom) ≫ eComp V X₁ Y₁ Z₁

Tactic:
simp only [eHomCongr, MonoidalCategory.whiskerRight_id, assoc,
  MonoidalCategory.whiskerLeft_comp]

Result:
V : Type u'
inst✝³ : Category.{v', u'} V
inst✝² : MonoidalCategory V
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : EnrichedOrdinaryCategory V C
X Y Z X₁ Y₁ Z₁ : C
α : X ≅ X₁
β : Y ≅ Y₁
γ : Z ≅ Z₁
f : X ⟶ Y
g : Y ⟶ Z
⊢ (eHomEquiv V) (f ≫ g) ≫ eHomWhiskerRight V α.inv Z ≫ eHomWhiskerLeft V X₁ γ.hom =
    (λ_ (𝟙_ V)).inv ≫
      (ρ_ (𝟙_ V)).hom ≫
        (eHomEquiv V) f ≫
          eHomWhiskerRight V α.inv Y ≫
            eHomWhiskerLeft V X₁ β.hom ≫
              (ρ_ (EnrichedCategory.Hom X₁ Y₁)).inv ≫
                EnrichedCategory.Hom X₁ Y₁ ◁ (eHomEquiv V) g ≫
                  EnrichedCategory.Hom X₁ Y₁ ◁ eHomWhiskerRight V β.inv Z ≫
                    EnrichedCategory.Hom X₁ Y₁ ◁ eHomWhiskerLeft V Y₁ γ.hom ≫ eComp V X₁ Y₁ Z₁

Proof state:
V : Type u'
inst✝³ : Category.{v', u'} V
inst✝² : MonoidalCategory V
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : EnrichedOrdinaryCategory V C
X Y Z X₁ Y₁ Z₁ : C
α : X ≅ X₁
β : Y ≅ Y₁
γ : Z ≅ Z₁
f : X ⟶ Y
g : Y ⟶ Z
⊢ (eHomEquiv V) (f ≫ g) ≫ eHomWhiskerRight V α.inv Z ≫ eHomWhiskerLeft V X₁ γ.hom =
    (λ_ (𝟙_ V)).inv ≫
      (ρ_ (𝟙_ V)).hom ≫
        (eHomEquiv V) f ≫
          eHomWhiskerRight V α.inv Y ≫
            eHomWhiskerLeft V X₁ β.hom ≫
              (ρ_ (EnrichedCategory.Hom X₁ Y₁)).inv ≫
                EnrichedCategory.Hom X₁ Y₁ ◁ (eHomEquiv V) g ≫
                  EnrichedCategory.Hom X₁ Y₁ ◁ eHomWhiskerRight V β.inv Z ≫
                    EnrichedCategory.Hom X₁ Y₁ ◁ eHomWhiskerLeft V Y₁ γ.hom ≫ eComp V X₁ Y₁ Z₁

Tactic:
rw [rightUnitor_inv_naturality_assoc, rightUnitor_inv_naturality_assoc,
  rightUnitor_inv_naturality_assoc, hom_inv_id_assoc, ← whisker_exchange_assoc,
  ← whisker_exchange_assoc, ← eComp_eHomWhiskerLeft, eHom_whisker_cancel_assoc,
  ← eComp_eHomWhiskerRight_assoc, ← tensorHom_def_assoc,
  ← eHomEquiv_comp_assoc]

Result:
no goals
-- Mathlib/Probability/Kernel/Disintegration/MeasurableStieltjes.lean
lemma monotone_defaultRatCDF : Monotone defaultRatCDF

Proof state:
x y : ℚ
hxy : x ≤ y
⊢ (if x < 0 then 0 else 1) ≤ if y < 0 then 0 else 1

Tactic:
split_ifs with h_1 h_2 h_2

Result:
case pos
x y : ℚ
hxy : x ≤ y
h_1 : x < 0
h_2 : y < 0
⊢ 0 ≤ 0

case neg
x y : ℚ
hxy : x ≤ y
h_1 : x < 0
h_2 : ¬y < 0
⊢ 0 ≤ 1

case pos
x y : ℚ
hxy : x ≤ y
h_1 : ¬x < 0
h_2 : y < 0
⊢ 1 ≤ 0

case neg
x y : ℚ
hxy : x ≤ y
h_1 : ¬x < 0
h_2 : ¬y < 0
⊢ 1 ≤ 1

Proof state:
case pos
x y : ℚ
hxy : x ≤ y
h_1 : x < 0
h_2 : y < 0
⊢ 0 ≤ 0

case neg
x y : ℚ
hxy : x ≤ y
h_1 : x < 0
h_2 : ¬y < 0
⊢ 0 ≤ 1

case pos
x y : ℚ
hxy : x ≤ y
h_1 : ¬x < 0
h_2 : y < 0
⊢ 1 ≤ 0

case neg
x y : ℚ
hxy : x ≤ y
h_1 : ¬x < 0
h_2 : ¬y < 0
⊢ 1 ≤ 1

Tactic:
exacts [le_rfl, zero_le_one, absurd (hxy.trans_lt h_2) h_1, le_rfl]

Result:
no goals

Proof state:
x y : ℚ
hxy : x ≤ y
⊢ (fun q => if q < 0 then 0 else 1) x ≤ (fun q => if q < 0 then 0 else 1) y

Tactic:
dsimp only

Result:
x y : ℚ
hxy : x ≤ y
⊢ (if x < 0 then 0 else 1) ≤ if y < 0 then 0 else 1

Proof state:
⊢ Monotone defaultRatCDF

Tactic:
unfold defaultRatCDF

Result:
⊢ Monotone fun q => if q < 0 then 0 else 1

Proof state:
⊢ Monotone fun q => if q < 0 then 0 else 1

Tactic:
intro x y hxy

Result:
x y : ℚ
hxy : x ≤ y
⊢ (fun q => if q < 0 then 0 else 1) x ≤ (fun q => if q < 0 then 0 else 1) y
-- Mathlib/Tactic/NormNum/LegendreSymbol.lean
theorem jacobiSymNat.zero_right (a : ℕ) : jacobiSymNat a 0 = 1

Proof state:
a : ℕ
⊢ jacobiSymNat a 0 = 1

Tactic:
rw [jacobiSymNat, jacobiSym.zero_right]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Control.lean
theorem findSomeM?_id (f : α → Option β) (as : List α) : findSomeM? (m := Id) f as = as.findSome? f

Proof state:
case cons.none
α : Type u_1
β : Type u_2
f : α → Option β
a : α
as : List α
ih : findSomeM? f as = findSome? f as
⊢ (do
      let __do_lift ← none
      match __do_lift with
        | some b => pure (some b)
        | none => findSome? f as) =
    match none with
    | some b => some b
    | none => findSome? f as

Tactic:
rfl

Result:
no goals

Proof state:
case cons
α : Type u_1
β : Type u_2
f : α → Option β
a : α
as : List α
ih : findSomeM? f as = findSome? f as
⊢ findSomeM? f (a :: as) = findSome? f (a :: as)

Tactic:
simp only [findSomeM?, findSome?]

Result:
case cons
α : Type u_1
β : Type u_2
f : α → Option β
a : α
as : List α
ih : findSomeM? f as = findSome? f as
⊢ (do
      let __do_lift ← f a
      match __do_lift with
        | some b => pure (some b)
        | none => findSomeM? f as) =
    match f a with
    | some b => some b
    | none => findSome? f as

Proof state:
case cons.none
α : Type u_1
β : Type u_2
f : α → Option β
a : α
as : List α
ih : findSomeM? f as = findSome? f as
⊢ (do
      let __do_lift ← none
      match __do_lift with
        | some b => pure (some b)
        | none => findSomeM? f as) =
    match none with
    | some b => some b
    | none => findSome? f as

Tactic:
rw [ih]

Result:
case cons.none
α : Type u_1
β : Type u_2
f : α → Option β
a : α
as : List α
ih : findSomeM? f as = findSome? f as
⊢ (do
      let __do_lift ← none
      match __do_lift with
        | some b => pure (some b)
        | none => findSome? f as) =
    match none with
    | some b => some b
    | none => findSome? f as

Proof state:
case nil
α : Type u_1
β : Type u_2
f : α → Option β
⊢ findSomeM? f [] = findSome? f []

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
f : α → Option β
as : List α
⊢ findSomeM? f as = findSome? f as

Tactic:
induction as with
| nil => rfl
| cons a as ih =>
  simp only [findSomeM?, findSome?]
  cases f a with
  | some b => rfl
  | none   => rw [ih]; rfl

Result:
no goals

Proof state:
case cons
α : Type u_1
β : Type u_2
f : α → Option β
a : α
as : List α
ih : findSomeM? f as = findSome? f as
⊢ (do
      let __do_lift ← f a
      match __do_lift with
        | some b => pure (some b)
        | none => findSomeM? f as) =
    match f a with
    | some b => some b
    | none => findSome? f as

Tactic:
cases f a with
| some b => rfl
| none   => rw [ih]; rfl

Result:
no goals

Proof state:
case cons.some
α : Type u_1
β : Type u_2
f : α → Option β
a : α
as : List α
ih : findSomeM? f as = findSome? f as
b : β
⊢ (do
      let __do_lift ← some b
      match __do_lift with
        | some b => pure (some b)
        | none => findSomeM? f as) =
    match some b with
    | some b => some b
    | none => findSome? f as

Tactic:
rfl

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/ZeroMorphisms.lean
theorem image.ι_zero' [HasEqualizers C] {X Y : C} {f : X ⟶ Y} (h : f = 0) [HasImage f] :
    image.ι f = 0

Proof state:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
inst✝² : HasZeroObject C
inst✝¹ : HasEqualizers C
X Y : C
f : X ⟶ Y
h : f = 0
inst✝ : HasImage f
⊢ ι f = 0

Tactic:
rw [image.eq_fac h]

Result:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
inst✝² : HasZeroObject C
inst✝¹ : HasEqualizers C
X Y : C
f : X ⟶ Y
h : f = 0
inst✝ : HasImage f
⊢ (eqToIso h).hom ≫ ι 0 = 0

Proof state:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroMorphisms C
inst✝² : HasZeroObject C
inst✝¹ : HasEqualizers C
X Y : C
f : X ⟶ Y
h : f = 0
inst✝ : HasImage f
⊢ (eqToIso h).hom ≫ ι 0 = 0

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/Complex.lean
theorem cpow_eq_zero_iff (x y : ℂ) : x ^ y = 0 ↔ x = 0 ∧ y ≠ 0

Proof state:
x y : ℂ
⊢ x ^ y = 0 ↔ x = 0 ∧ y ≠ 0

Tactic:
simp only [cpow_def]

Result:
x y : ℂ
⊢ (if x = 0 then if y = 0 then 1 else 0 else cexp (log x * y)) = 0 ↔ x = 0 ∧ y ≠ 0

Proof state:
x y : ℂ
⊢ (if x = 0 then if y = 0 then 1 else 0 else cexp (log x * y)) = 0 ↔ x = 0 ∧ y ≠ 0

Tactic:
split_ifs <;> simp [*, exp_ne_zero]

Result:
no goals
-- Mathlib/GroupTheory/Exponent.lean
theorem exponent_min (m : ℕ) (hpos : 0 < m) (hm : m < exponent G) : ∃ g : G, g ^ m ≠ 1

Proof state:
G : Type u
inst✝ : Monoid G
m : ℕ
hpos : 0 < m
hm : m < exponent G
⊢ ∃ g, g ^ m ≠ 1

Tactic:
by_contra! h

Result:
G : Type u
inst✝ : Monoid G
m : ℕ
hpos : 0 < m
hm : m < exponent G
h : ∀ (g : G), g ^ m = 1
⊢ False

Proof state:
G : Type u
inst✝ : Monoid G
m : ℕ
hpos : 0 < m
hm : m < exponent G
h : ∀ (g : G), g ^ m = 1
⊢ False

Tactic:
have hcon : exponent G ≤ m := exponent_min' m hpos h

Result:
G : Type u
inst✝ : Monoid G
m : ℕ
hpos : 0 < m
hm : m < exponent G
h : ∀ (g : G), g ^ m = 1
hcon : exponent G ≤ m
⊢ False

Proof state:
G : Type u
inst✝ : Monoid G
m : ℕ
hpos : 0 < m
hm : m < exponent G
h : ∀ (g : G), g ^ m = 1
hcon : exponent G ≤ m
⊢ False

Tactic:
omega

Result:
no goals
-- Mathlib/MeasureTheory/Integral/Lebesgue.lean
theorem lintegral_max {f g : α → ℝ≥0∞} (hf : Measurable f) (hg : Measurable g) :
    ∫⁻ x, max (f x) (g x) ∂μ =
      ∫⁻ x in { x | f x ≤ g x }, g x ∂μ + ∫⁻ x in { x | g x < f x }, f x ∂μ

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : Measurable f
hg : Measurable g
hm : MeasurableSet {x | f x ≤ g x}
⊢ ∫⁻ (x : α) in {x | f x ≤ g x}, f x ⊔ g x ∂μ + ∫⁻ (x : α) in {x | f x ≤ g x}ᶜ, f x ⊔ g x ∂μ =
    ∫⁻ (x : α) in {x | f x ≤ g x}, g x ∂μ + ∫⁻ (x : α) in {x | g x < f x}, f x ∂μ

Tactic:
simp only [← compl_setOf, ← not_le]

Result:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : Measurable f
hg : Measurable g
hm : MeasurableSet {x | f x ≤ g x}
⊢ ∫⁻ (x : α) in {x | f x ≤ g x}, f x ⊔ g x ∂μ + ∫⁻ (x : α) in {x | f x ≤ g x}ᶜ, f x ⊔ g x ∂μ =
    ∫⁻ (x : α) in {x | f x ≤ g x}, g x ∂μ + ∫⁻ (x : α) in {a | f a ≤ g a}ᶜ, f x ∂μ

Proof state:
case refine_1
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : Measurable f
hg : Measurable g
hm : MeasurableSet {x | f x ≤ g x}
⊢ ∀ᵐ (x : α) ∂μ, x ∈ {x | f x ≤ g x} → f x ⊔ g x = g x

case refine_2
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : Measurable f
hg : Measurable g
hm : MeasurableSet {x | f x ≤ g x}
⊢ ∀ᵐ (x : α) ∂μ, x ∈ {x | f x ≤ g x}ᶜ → f x ⊔ g x = f x

Tactic:
exacts [ae_of_all _ fun x => max_eq_right (a := f x) (b := g x),
  ae_of_all _ fun x (hx : ¬ f x ≤ g x) => max_eq_left (not_le.1 hx).le]

Result:
no goals

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : Measurable f
hg : Measurable g
⊢ ∫⁻ (x : α), f x ⊔ g x ∂μ = ∫⁻ (x : α) in {x | f x ≤ g x}, g x ∂μ + ∫⁻ (x : α) in {x | g x < f x}, f x ∂μ

Tactic:
have hm : MeasurableSet { x | f x ≤ g x } := measurableSet_le hf hg

Result:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : Measurable f
hg : Measurable g
hm : MeasurableSet {x | f x ≤ g x}
⊢ ∫⁻ (x : α), f x ⊔ g x ∂μ = ∫⁻ (x : α) in {x | f x ≤ g x}, g x ∂μ + ∫⁻ (x : α) in {x | g x < f x}, f x ∂μ

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : Measurable f
hg : Measurable g
hm : MeasurableSet {x | f x ≤ g x}
⊢ ∫⁻ (x : α), f x ⊔ g x ∂μ = ∫⁻ (x : α) in {x | f x ≤ g x}, g x ∂μ + ∫⁻ (x : α) in {x | g x < f x}, f x ∂μ

Tactic:
rw [← lintegral_add_compl (fun x => max (f x) (g x)) hm]

Result:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hf : Measurable f
hg : Measurable g
hm : MeasurableSet {x | f x ≤ g x}
⊢ ∫⁻ (x : α) in {x | f x ≤ g x}, f x ⊔ g x ∂μ + ∫⁻ (x : α) in {x | f x ≤ g x}ᶜ, f x ⊔ g x ∂μ =
    ∫⁻ (x : α) in {x | f x ≤ g x}, g x ∂μ + ∫⁻ (x : α) in {x | g x < f x}, f x ∂μ
-- Mathlib/Algebra/CharP/Defs.lean
lemma CharOne.subsingleton [CharP R 1] : Subsingleton R :=
  Subsingleton.intro <|
    suffices ∀ r : R, r = 0 from fun a b => show a = b by rw [this a, this b]
    fun r =>
    calc
      r = 1 * r

Proof state:
R : Type u_1
inst✝¹ : NonAssocSemiring R
inst✝ : CharP R 1
this : ∀ (r : R), r = 0
a b : R
⊢ a = b

Tactic:
rw [this a, this b]

Result:
no goals

Proof state:
R : Type u_1
inst✝¹ : NonAssocSemiring R
inst✝ : CharP R 1
r : R
⊢ ↑1 * r = 0 * r

Tactic:
rw [CharP.cast_eq_zero]

Result:
no goals

Proof state:
R : Type u_1
inst✝¹ : NonAssocSemiring R
inst✝ : CharP R 1
r : R
⊢ 0 * r = 0

Tactic:
rw [zero_mul]

Result:
no goals

Proof state:
R : Type u_1
inst✝¹ : NonAssocSemiring R
inst✝ : CharP R 1
r : R
⊢ 1 * r = ↑1 * r

Tactic:
rw [Nat.cast_one]

Result:
no goals

Proof state:
R : Type u_1
inst✝¹ : NonAssocSemiring R
inst✝ : CharP R 1
r : R
⊢ r = 1 * r

Tactic:
rw [one_mul]

Result:
no goals
-- Mathlib/Topology/Algebra/Order/Floor.lean
theorem tendsto_floor_left (n : ℤ) :
    Tendsto (fun x => floor x : α → α) (𝓝[<] n) (𝓝[≤] (n - 1)) :=
  ((tendsto_pure_pure _ _).comp (tendsto_floor_left_pure_sub_one n)).mono_right <| by
    rw [← @cast_one α, ← cast_sub]; exact pure_le_nhdsWithin le_rfl

Proof state:
α : Type u_1
inst✝³ : LinearOrderedRing α
inst✝² : FloorRing α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
n : ℤ
⊢ pure (IntCast.intCast (n - 1)) ≤ 𝓝[≤] ↑(n - 1)

Tactic:
exact pure_le_nhdsWithin le_rfl

Result:
no goals

Proof state:
α : Type u_1
inst✝³ : LinearOrderedRing α
inst✝² : FloorRing α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
n : ℤ
⊢ pure (IntCast.intCast (n - 1)) ≤ 𝓝[≤] (↑n - 1)

Tactic:
rw [← @cast_one α, ← cast_sub]

Result:
α : Type u_1
inst✝³ : LinearOrderedRing α
inst✝² : FloorRing α
inst✝¹ : TopologicalSpace α
inst✝ : OrderClosedTopology α
n : ℤ
⊢ pure (IntCast.intCast (n - 1)) ≤ 𝓝[≤] ↑(n - 1)
-- Mathlib/Data/Real/EReal.lean
theorem abs_mul (x y : EReal) : (x * y).abs = x.abs * y.abs

Proof state:
x y : EReal
⊢ (x * y).abs = x.abs * y.abs

Tactic:
induction x, y using induction₂_symm_neg with
| top_zero => simp only [zero_mul, mul_zero, abs_zero]
| top_top => rfl
| symm h => rwa [mul_comm, EReal.mul_comm]
| coe_coe => simp only [← coe_mul, abs_def, _root_.abs_mul, ENNReal.ofReal_mul (abs_nonneg _)]
| top_pos _ h =>
  rw [top_mul_coe_of_pos h, abs_top, ENNReal.top_mul]
  rw [Ne, abs_eq_zero_iff, coe_eq_zero]
  exact h.ne'
| neg_left h => rwa [neg_mul, EReal.abs_neg, EReal.abs_neg]

Result:
no goals

Proof state:
case neg_left
x✝ y✝ : EReal
h : (x✝ * y✝).abs = x✝.abs * y✝.abs
⊢ (-x✝ * y✝).abs = (-x✝).abs * y✝.abs

Tactic:
rwa [neg_mul, EReal.abs_neg, EReal.abs_neg]

Result:
no goals

Proof state:
case top_pos
x✝ : ℝ
h : 0 < x✝
⊢ (↑x✝).abs ≠ 0

Tactic:
rw [Ne, abs_eq_zero_iff, coe_eq_zero]

Result:
case top_pos
x✝ : ℝ
h : 0 < x✝
⊢ ¬x✝ = 0

Proof state:
case top_zero

⊢ (⊤ * 0).abs = ⊤.abs * EReal.abs 0

Tactic:
simp only [zero_mul, mul_zero, abs_zero]

Result:
no goals

Proof state:
case symm
x✝ y✝ : EReal
h : (x✝ * y✝).abs = x✝.abs * y✝.abs
⊢ (y✝ * x✝).abs = y✝.abs * x✝.abs

Tactic:
rwa [mul_comm, EReal.mul_comm]

Result:
no goals

Proof state:
case top_pos
x✝ : ℝ
h : 0 < x✝
⊢ (⊤ * ↑x✝).abs = ⊤.abs * (↑x✝).abs

Tactic:
rw [top_mul_coe_of_pos h, abs_top, ENNReal.top_mul]

Result:
case top_pos
x✝ : ℝ
h : 0 < x✝
⊢ (↑x✝).abs ≠ 0

Proof state:
case top_top

⊢ (⊤ * ⊤).abs = ⊤.abs * ⊤.abs

Tactic:
rfl

Result:
no goals

Proof state:
case coe_coe
x✝ y✝ : ℝ
⊢ (↑x✝ * ↑y✝).abs = (↑x✝).abs * (↑y✝).abs

Tactic:
simp only [← coe_mul, abs_def, _root_.abs_mul, ENNReal.ofReal_mul (abs_nonneg _)]

Result:
no goals

Proof state:
case top_pos
x✝ : ℝ
h : 0 < x✝
⊢ ¬x✝ = 0

Tactic:
exact h.ne'

Result:
no goals
-- Mathlib/MeasureTheory/Integral/CircleIntegral.lean
theorem integral_congr {f g : ℂ → E} {c : ℂ} {R : ℝ} (hR : 0 ≤ R) (h : EqOn f g (sphere c R)) :
    (∮ z in C(c, R), f z) = ∮ z in C(c, R), g z :=
  intervalIntegral.integral_congr fun θ _ => by simp only [h (circleMap_mem_sphere _ hR _)]

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f g : ℂ → E
c : ℂ
R : ℝ
hR : 0 ≤ R
h : EqOn f g (sphere c R)
θ : ℝ
x✝ : θ ∈ [[0, 2 * π]]
⊢ deriv (circleMap c R) θ • (fun z => f z) (circleMap c R θ) =
    deriv (circleMap c R) θ • (fun z => g z) (circleMap c R θ)

Tactic:
simp only [h (circleMap_mem_sphere _ hR _)]

Result:
no goals
-- Mathlib/Topology/UniformSpace/Basic.lean
theorem uniformity_prod_eq_prod [UniformSpace α] [UniformSpace β] :
    𝓤 (α × β) = map (fun p : (α × α) × β × β => ((p.1.1, p.2.1), (p.1.2, p.2.2))) (𝓤 α ×ˢ 𝓤 β)

Proof state:
α : Type ua
β : Type ub
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
⊢ 𝓤 (α × β) = map (fun p => ((p.1.1, p.2.1), p.1.2, p.2.2)) (𝓤 α ×ˢ 𝓤 β)

Tactic:
rw [map_swap4_eq_comap, uniformity_prod_eq_comap_prod]

Result:
no goals
-- Mathlib/MeasureTheory/Function/ConditionalExpectation/CondexpL2.lean
theorem condExpL2_ae_eq_zero_of_ae_eq_zero (hs : MeasurableSet[m] s) (hμs : μ s ≠ ∞) {f : Lp ℝ 2 μ}
    (hf : f =ᵐ[μ.restrict s] 0) : condExpL2 ℝ ℝ hm f =ᵐ[μ.restrict s] (0 : α → ℝ)

Proof state:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
hs : MeasurableSet s
hμs : μ s ≠ ⊤
f : ↥(Lp ℝ 2 μ)
hf : ↑↑f =ᶠ[ae (μ.restrict s)] 0
h_nnnorm_eq_zero : ∫⁻ (x : α) in s, ↑‖↑↑↑((condExpL2 ℝ ℝ hm) f) x‖₊ ∂μ = 0
⊢ Measurable fun x => ↑‖↑↑↑((condExpL2 ℝ ℝ hm) f) x‖₊

Tactic:
refine Measurable.coe_nnreal_ennreal (Measurable.nnnorm ?_)

Result:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
hs : MeasurableSet s
hμs : μ s ≠ ⊤
f : ↥(Lp ℝ 2 μ)
hf : ↑↑f =ᶠ[ae (μ.restrict s)] 0
h_nnnorm_eq_zero : ∫⁻ (x : α) in s, ↑‖↑↑↑((condExpL2 ℝ ℝ hm) f) x‖₊ ∂μ = 0
⊢ Measurable ↑↑↑((condExpL2 ℝ ℝ hm) f)