harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Probability/Distributions/Uniform.lean
theorem pdf_eq_zero_of_measure_eq_zero_or_top {X : Ω → E} {s : Set E}
    (hu : IsUniform X s ℙ μ) (hμs : μ s = 0 ∨ μ s = ∞) : pdf X ℙ μ =ᵐ[μ] 0

Proof state:
case inr
E : Type u_1
inst✝ : MeasurableSpace E
μ : Measure E
Ω : Type u_2
x✝ : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → E
s : Set E
H : μ s = ⊤
hu : Measure.map X ℙ = 0
⊢ pdf X ℙ μ =ᶠ[ae μ] 0

Tactic:
simp [pdf, hu]

Result:
no goals

Proof state:
E : Type u_1
inst✝ : MeasurableSpace E
μ : Measure E
Ω : Type u_2
x✝ : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → E
s : Set E
hu : IsUniform X s ℙ μ
hμs : μ s = 0 ∨ μ s = ⊤
⊢ pdf X ℙ μ =ᶠ[ae μ] 0

Tactic:
rcases hμs with H|H

Result:
case inl
E : Type u_1
inst✝ : MeasurableSpace E
μ : Measure E
Ω : Type u_2
x✝ : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → E
s : Set E
hu : IsUniform X s ℙ μ
H : μ s = 0
⊢ pdf X ℙ μ =ᶠ[ae μ] 0

case inr
E : Type u_1
inst✝ : MeasurableSpace E
μ : Measure E
Ω : Type u_2
x✝ : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → E
s : Set E
hu : IsUniform X s ℙ μ
H : μ s = ⊤
⊢ pdf X ℙ μ =ᶠ[ae μ] 0

Proof state:
case inl
E : Type u_1
inst✝ : MeasurableSpace E
μ : Measure E
Ω : Type u_2
x✝ : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → E
s : Set E
hu : IsUniform X s ℙ μ
H : μ s = 0
⊢ pdf X ℙ μ =ᶠ[ae μ] 0

Tactic:
simp only [IsUniform, ProbabilityTheory.cond, H, ENNReal.inv_zero, restrict_eq_zero.mpr H,
smul_zero] at hu

Result:
case inl
E : Type u_1
inst✝ : MeasurableSpace E
μ : Measure E
Ω : Type u_2
x✝ : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → E
s : Set E
H : μ s = 0
hu : Measure.map X ℙ = 0
⊢ pdf X ℙ μ =ᶠ[ae μ] 0

Proof state:
case inr
E : Type u_1
inst✝ : MeasurableSpace E
μ : Measure E
Ω : Type u_2
x✝ : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → E
s : Set E
hu : IsUniform X s ℙ μ
H : μ s = ⊤
⊢ pdf X ℙ μ =ᶠ[ae μ] 0

Tactic:
simp only [IsUniform, ProbabilityTheory.cond, H, ENNReal.inv_top, zero_smul] at hu

Result:
case inr
E : Type u_1
inst✝ : MeasurableSpace E
μ : Measure E
Ω : Type u_2
x✝ : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → E
s : Set E
H : μ s = ⊤
hu : Measure.map X ℙ = 0
⊢ pdf X ℙ μ =ᶠ[ae μ] 0

Proof state:
case inl
E : Type u_1
inst✝ : MeasurableSpace E
μ : Measure E
Ω : Type u_2
x✝ : MeasurableSpace Ω
ℙ : Measure Ω
X : Ω → E
s : Set E
H : μ s = 0
hu : Measure.map X ℙ = 0
⊢ pdf X ℙ μ =ᶠ[ae μ] 0

Tactic:
simp [pdf, hu]

Result:
no goals
-- Mathlib/RingTheory/Ideal/Norm/AbsNorm.lean
theorem Ideal.mul_add_mem_pow_succ_inj (P : Ideal S) {i : ℕ} (a d d' e e' : S) (a_mem : a ∈ P ^ i)
    (e_mem : e ∈ P ^ (i + 1)) (e'_mem : e' ∈ P ^ (i + 1)) (h : d - d' ∈ P) :
    a * d + e - (a * d' + e') ∈ P ^ (i + 1)

Proof state:
S : Type u_1
inst✝ : CommRing S
P : Ideal S
i : ℕ
a d d' e e' : S
a_mem : a ∈ P ^ i
e_mem : e ∈ P ^ (i + 1)
e'_mem : e' ∈ P ^ (i + 1)
h : d - d' ∈ P
⊢ a * d + e - (a * d' + e') ∈ P ^ (i + 1)

Tactic:
have : a * d - a * d' ∈ P ^ (i + 1) := by
  simp only [← mul_sub]
  exact Ideal.mul_mem_mul a_mem h

Result:
S : Type u_1
inst✝ : CommRing S
P : Ideal S
i : ℕ
a d d' e e' : S
a_mem : a ∈ P ^ i
e_mem : e ∈ P ^ (i + 1)
e'_mem : e' ∈ P ^ (i + 1)
h : d - d' ∈ P
this : a * d - a * d' ∈ P ^ (i + 1)
⊢ a * d + e - (a * d' + e') ∈ P ^ (i + 1)

Proof state:
S : Type u_1
inst✝ : CommRing S
P : Ideal S
i : ℕ
a d d' e e' : S
a_mem : a ∈ P ^ i
e_mem : e ∈ P ^ (i + 1)
e'_mem : e' ∈ P ^ (i + 1)
h : d - d' ∈ P
⊢ a * d - a * d' ∈ P ^ (i + 1)

Tactic:
simp only [← mul_sub]

Result:
S : Type u_1
inst✝ : CommRing S
P : Ideal S
i : ℕ
a d d' e e' : S
a_mem : a ∈ P ^ i
e_mem : e ∈ P ^ (i + 1)
e'_mem : e' ∈ P ^ (i + 1)
h : d - d' ∈ P
⊢ a * (d - d') ∈ P ^ (i + 1)

Proof state:
S : Type u_1
inst✝ : CommRing S
P : Ideal S
i : ℕ
a d d' e e' : S
a_mem : a ∈ P ^ i
e_mem : e ∈ P ^ (i + 1)
e'_mem : e' ∈ P ^ (i + 1)
h : d - d' ∈ P
⊢ a * (d - d') ∈ P ^ (i + 1)

Tactic:
exact Ideal.mul_mem_mul a_mem h

Result:
no goals

Proof state:
case h.e'_5
S : Type u_1
inst✝ : CommRing S
P : Ideal S
i : ℕ
a d d' e e' : S
a_mem : a ∈ P ^ i
e_mem : e ∈ P ^ (i + 1)
e'_mem : e' ∈ P ^ (i + 1)
h : d - d' ∈ P
this : a * d - a * d' ∈ P ^ (i + 1)
⊢ a * d + e - (a * d' + e') = a * d - a * d' + (e - e')

Tactic:
ring

Result:
no goals

Proof state:
S : Type u_1
inst✝ : CommRing S
P : Ideal S
i : ℕ
a d d' e e' : S
a_mem : a ∈ P ^ i
e_mem : e ∈ P ^ (i + 1)
e'_mem : e' ∈ P ^ (i + 1)
h : d - d' ∈ P
this : a * d - a * d' ∈ P ^ (i + 1)
⊢ a * d + e - (a * d' + e') ∈ P ^ (i + 1)

Tactic:
convert Ideal.add_mem _ this (Ideal.sub_mem _ e_mem e'_mem) using 1

Result:
case h.e'_5
S : Type u_1
inst✝ : CommRing S
P : Ideal S
i : ℕ
a d d' e e' : S
a_mem : a ∈ P ^ i
e_mem : e ∈ P ^ (i + 1)
e'_mem : e' ∈ P ^ (i + 1)
h : d - d' ∈ P
this : a * d - a * d' ∈ P ^ (i + 1)
⊢ a * d + e - (a * d' + e') = a * d - a * d' + (e - e')
-- Mathlib/Analysis/RCLike/Basic.lean
lemma norm_nnqsmul (q : ℚ≥0) (x : E) : ‖q • x‖ = q • ‖x‖

Proof state:
K : Type u_1
E : Type u_2
inst✝³ : RCLike K
inst✝² : NormedField E
inst✝¹ : CharZero E
inst✝ : NormedSpace K E
q : ℚ≥0
x : E
⊢ ‖q • x‖ = q • ‖x‖

Tactic:
simpa [NNRat.cast_smul_eq_nnqsmul] using norm_smul (q : K) x

Result:
no goals
-- Mathlib/Algebra/EuclideanDomain/Basic.lean
theorem gcd_eq_zero_iff {a b : R} : gcd a b = 0 ↔ a = 0 ∧ b = 0 :=
  ⟨fun h => by simpa [h] using gcd_dvd a b, by
    rintro ⟨rfl, rfl⟩
    exact gcd_zero_right _⟩

Proof state:
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
a b : R
h : gcd a b = 0
⊢ a = 0 ∧ b = 0

Tactic:
simpa [h] using gcd_dvd a b

Result:
no goals

Proof state:
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
a b : R
⊢ a = 0 ∧ b = 0 → gcd a b = 0

Tactic:
rintro ⟨rfl, rfl⟩

Result:
case intro
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
⊢ gcd 0 0 = 0

Proof state:
case intro
R : Type u
inst✝¹ : EuclideanDomain R
inst✝ : DecidableEq R
⊢ gcd 0 0 = 0

Tactic:
exact gcd_zero_right _

Result:
no goals
-- Mathlib/MeasureTheory/Function/LpSeminorm/ChebyshevMarkov.lean
theorem mul_meas_ge_le_pow_eLpNorm' (hp_ne_zero : p ≠ 0) (hp_ne_top : p ≠ ∞)
    (hf : AEStronglyMeasurable f μ) (ε : ℝ≥0∞) :
    ε ^ p.toReal * μ { x | ε ≤ ‖f x‖₊ } ≤ eLpNorm f p μ ^ p.toReal

Proof state:
case h.e'_3.h.e'_6.h.e'_6.h.e'_2.h.a
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
f : α → E
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ⊤
hf : AEStronglyMeasurable f μ
ε : ℝ≥0∞
x : α
⊢ ε ≤ ↑‖f x‖₊ ↔ ε ^ p.toReal ≤ ↑‖f x‖₊ ^ p.toReal

Tactic:
rw [ENNReal.rpow_le_rpow_iff (ENNReal.toReal_pos hp_ne_zero hp_ne_top)]

Result:
no goals

Proof state:
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
f : α → E
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ⊤
hf : AEStronglyMeasurable f μ
ε : ℝ≥0∞
⊢ ε ^ p.toReal * μ {x | ε ≤ ↑‖f x‖₊} ≤ eLpNorm f p μ ^ p.toReal

Tactic:
convert mul_meas_ge_le_pow_eLpNorm μ hp_ne_zero hp_ne_top hf (ε ^ p.toReal) using 4

Result:
case h.e'_3.h.e'_6.h.e'_6.h.e'_2
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
f : α → E
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ⊤
hf : AEStronglyMeasurable f μ
ε : ℝ≥0∞
⊢ (fun x => ε ≤ ↑‖f x‖₊) = fun x => ε ^ p.toReal ≤ ↑‖f x‖₊ ^ p.toReal

Proof state:
case h.e'_3.h.e'_6.h.e'_6.h.e'_2
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
f : α → E
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ⊤
hf : AEStronglyMeasurable f μ
ε : ℝ≥0∞
⊢ (fun x => ε ≤ ↑‖f x‖₊) = fun x => ε ^ p.toReal ≤ ↑‖f x‖₊ ^ p.toReal

Tactic:
ext x

Result:
case h.e'_3.h.e'_6.h.e'_6.h.e'_2.h.a
α : Type u_1
E : Type u_2
m0 : MeasurableSpace α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
f : α → E
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ⊤
hf : AEStronglyMeasurable f μ
ε : ℝ≥0∞
x : α
⊢ ε ≤ ↑‖f x‖₊ ↔ ε ^ p.toReal ≤ ↑‖f x‖₊ ^ p.toReal
-- Mathlib/RingTheory/DiscreteValuationRing/TFAE.lean
theorem tfae_of_isNoetherianRing_of_isLocalRing_of_isDomain
    [IsNoetherianRing R] [IsLocalRing R] [IsDomain R] :
    List.TFAE
      [IsPrincipalIdealRing R, ValuationRing R, IsDedekindDomain R,
        IsIntegrallyClosed R ∧ ∀ P : Ideal R, P ≠ ⊥ → P.IsPrime → P = maximalIdeal R,
        (maximalIdeal R).IsPrincipal,
        finrank (ResidueField R) (CotangentSpace R) ≤ 1,
        ∀ I ≠ ⊥, ∃ n : ℕ, I = maximalIdeal R ^ n]

Proof state:
case pos
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsNoetherianRing R
inst✝¹ : IsLocalRing R
inst✝ : IsDomain R
tfae_1_to_2 : IsPrincipalIdealRing R → ValuationRing R
tfae_2_to_1 : ValuationRing R → IsPrincipalIdealRing R
tfae_1_to_4 : IsPrincipalIdealRing R → IsIntegrallyClosed R ∧ ∀ (P : Ideal R), P ≠ ⊥ → P.IsPrime → P = maximalIdeal R
tfae_4_to_3 : (IsIntegrallyClosed R ∧ ∀ (P : Ideal R), P ≠ ⊥ → P.IsPrime → P = maximalIdeal R) → IsDedekindDomain R
tfae_3_to_5 : IsDedekindDomain R → Submodule.IsPrincipal (maximalIdeal R)
tfae_6_iff_5 : finrank (ResidueField R) (CotangentSpace R) ≤ 1 ↔ Submodule.IsPrincipal (maximalIdeal R)
tfae_5_to_7 : Submodule.IsPrincipal (maximalIdeal R) → ∀ (I : Ideal R), I ≠ ⊥ → ∃ n, I = maximalIdeal R ^ n
H : ∀ (I : Ideal R), I ≠ ⊥ → ∃ n, I = maximalIdeal R ^ n
I J : Ideal R
hI : I = ⊥
⊢ I ≤ J ∨ J ≤ I

Tactic:
subst hI

Result:
case pos
R : Type u_1
inst✝³ : CommRing R
inst✝² : IsNoetherianRing R
inst✝¹ : IsLocalRing R
inst✝ : IsDomain R
tfae_1_to_2 : IsPrincipalIdealRing R → ValuationRing R
tfae_2_to_1 : ValuationRing R → IsPrincipalIdealRing R
tfae_1_to_4 : IsPrincipalIdealRing R → IsIntegrallyClosed R ∧ ∀ (P : Ideal R), P ≠ ⊥ → P.IsPrime → P = maximalIdeal R
tfae_4_to_3 : (IsIntegrallyClosed R ∧ ∀ (P : Ideal R), P ≠ ⊥ → P.IsPrime → P = maximalIdeal R) → IsDedekindDomain R
tfae_3_to_5 : IsDedekindDomain R → Submodule.IsPrincipal (maximalIdeal R)
tfae_6_iff_5 : finrank (ResidueField R) (CotangentSpace R) ≤ 1 ↔ Submodule.IsPrincipal (maximalIdeal R)
tfae_5_to_7 : Submodule.IsPrincipal (maximalIdeal R) → ∀ (I : Ideal R), I ≠ ⊥ → ∃ n, I = maximalIdeal R ^ n
H : ∀ (I : Ideal R), I ≠ ⊥ → ∃ n, I = maximalIdeal R ^ n
J : Ideal R
⊢ ⊥ ≤ J ∨ J ≤ ⊥
-- Mathlib/Data/Fin/Basic.lean
theorem succ_one_eq_two' [NeZero n] : Fin.succ (1 : Fin (n + 1)) = 2

Proof state:
case zero
inst✝ : NeZero 0
⊢ succ 1 = 2

Tactic:
exact (NeZero.ne 0 rfl).elim

Result:
no goals

Proof state:
case succ
n✝ : ℕ
inst✝ : NeZero (n✝ + 1)
⊢ succ 1 = 2

Tactic:
rfl

Result:
no goals

Proof state:
n : ℕ
inst✝ : NeZero n
⊢ succ 1 = 2

Tactic:
cases n

Result:
case zero
inst✝ : NeZero 0
⊢ succ 1 = 2

case succ
n✝ : ℕ
inst✝ : NeZero (n✝ + 1)
⊢ succ 1 = 2
-- Mathlib/AlgebraicGeometry/EllipticCurve/Projective.lean
lemma Y_ne_negY_of_Y_ne [NoZeroDivisors R] {P Q : Fin 3 → R} (hP : W'.Equation P)
    (hQ : W'.Equation Q) (hPz : P z ≠ 0) (hQz : Q z ≠ 0) (hx : P x * Q z = Q x * P z)
    (hy : P y * Q z ≠ Q y * P z) : P y ≠ W'.negY P

Proof state:
R : Type r
inst✝¹ : CommRing R
W' : Projective R
inst✝ : NoZeroDivisors R
P Q : Fin 3 → R
hP : W'.Equation P
hQ : W'.Equation Q
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z = Q x * P z
hy : P y * Q z ≠ Q y * P z
⊢ P y ≠ W'.negY P

Tactic:
have hy' : P y * Q z - W'.negY Q * P z = 0 := sub_eq_zero.mpr <| Y_eq_of_Y_ne hP hQ hPz hQz hx hy

Result:
R : Type r
inst✝¹ : CommRing R
W' : Projective R
inst✝ : NoZeroDivisors R
P Q : Fin 3 → R
hP : W'.Equation P
hQ : W'.Equation Q
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z = Q x * P z
hy : P y * Q z ≠ Q y * P z
hy' : P y * Q z - W'.negY Q * P z = 0
⊢ P y ≠ W'.negY P

Proof state:
R : Type r
inst✝¹ : CommRing R
W' : Projective R
inst✝ : NoZeroDivisors R
P Q : Fin 3 → R
hP : W'.Equation P
hQ : W'.Equation Q
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z = Q x * P z
hy' : P y * Q z - W'.negY Q * P z = 0
hy : P y = W'.negY P
⊢ P y * Q z = Q y * P z

Tactic:
linear_combination (norm := ring1) Y_sub_Y_add_Y_sub_negY hx + Q z * hy - hy'

Result:
no goals

Proof state:
R : Type r
inst✝¹ : CommRing R
W' : Projective R
inst✝ : NoZeroDivisors R
P Q : Fin 3 → R
hP : W'.Equation P
hQ : W'.Equation Q
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z = Q x * P z
hy : P y * Q z ≠ Q y * P z
hy' : P y * Q z - W'.negY Q * P z = 0
⊢ P y ≠ W'.negY P

Tactic:
contrapose! hy

Result:
R : Type r
inst✝¹ : CommRing R
W' : Projective R
inst✝ : NoZeroDivisors R
P Q : Fin 3 → R
hP : W'.Equation P
hQ : W'.Equation Q
hPz : P z ≠ 0
hQz : Q z ≠ 0
hx : P x * Q z = Q x * P z
hy' : P y * Q z - W'.negY Q * P z = 0
hy : P y = W'.negY P
⊢ P y * Q z = Q y * P z
-- Mathlib/Analysis/SpecialFunctions/Exp.lean
theorem exp_bound_sq (x z : ℂ) (hz : ‖z‖ ≤ 1) :
    ‖exp (x + z) - exp x - z • exp x‖ ≤ ‖exp x‖ * ‖z‖ ^ 2 :=
  calc
    ‖exp (x + z) - exp x - z * exp x‖ = ‖exp x * (exp z - 1 - z)‖

Proof state:
x z : ℂ
hz : ‖z‖ ≤ 1
⊢ ‖cexp (x + z) - cexp x - z * cexp x‖ = ‖cexp x * (cexp z - 1 - z)‖

Tactic:
congr

Result:
case e_a
x z : ℂ
hz : ‖z‖ ≤ 1
⊢ cexp (x + z) - cexp x - z * cexp x = cexp x * (cexp z - 1 - z)

Proof state:
case e_a
x z : ℂ
hz : ‖z‖ ≤ 1
⊢ cexp (x + z) - cexp x - z * cexp x = cexp x * (cexp z - 1 - z)

Tactic:
rw [exp_add]

Result:
case e_a
x z : ℂ
hz : ‖z‖ ≤ 1
⊢ cexp x * cexp z - cexp x - z * cexp x = cexp x * (cexp z - 1 - z)

Proof state:
case e_a
x z : ℂ
hz : ‖z‖ ≤ 1
⊢ cexp x * cexp z - cexp x - z * cexp x = cexp x * (cexp z - 1 - z)

Tactic:
ring

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem getValue_cons_of_beq [BEq α] {l : List ((_ : α) × β)} {k a : α} {v : β} (h : k == a) :
    getValue a (⟨k, v⟩ :: l) (containsKey_cons_of_beq (k := k) (v := v) h) = v

Proof state:
α : Type u
β : Type v
inst✝ : BEq α
l : List ((_ : α) × β)
k a : α
v : β
h : (k == a) = true
⊢ getValue a (⟨k, v⟩ :: l) ⋯ = v

Tactic:
simp [getValue, getValue?_cons_of_true h]

Result:
no goals
-- Mathlib/MeasureTheory/Function/ConditionalExpectation/CondexpL2.lean
theorem condExpL2_const_inner (hm : m ≤ m0) (f : Lp E 2 μ) (c : E) :
    condExpL2 𝕜 𝕜 hm (((Lp.memLp f).const_inner c).toLp fun a => ⟪c, f a⟫) =ᵐ[μ]
    fun a => ⟪c, (condExpL2 E 𝕜 hm f : α → E) a⟫

Proof state:
case refine_1
α : Type u_1
E : Type u_2
𝕜 : Type u_7
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : ↥(Lp E 2 μ)
c : E
h_mem_Lp : MemLp (fun a => inner c (↑↑↑((condExpL2 E 𝕜 hm) f) a)) 2 μ
h_eq :
  ↑↑(MemLp.toLp (fun a => inner c (↑↑↑((condExpL2 E 𝕜 hm) f) a)) h_mem_Lp) =ᶠ[ae μ] fun a =>
    inner c (↑↑↑((condExpL2 E 𝕜 hm) f) a)
s : Set α
a✝ : MeasurableSet s
hμs : μ s < ⊤
⊢ Integrable (fun a => inner c (↑↑↑((condExpL2 E 𝕜 hm) f) a)) (μ.restrict s)

Tactic:
exact (integrableOn_condExpL2_of_measure_ne_top hm hμs.ne _).const_inner _

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem getElem_setWidth (m : Nat) (x : BitVec n) (i : Nat) (h : i < m) :
    (setWidth m x)[i] = x.getLsbD i

Proof state:
case isFalse
n m : Nat
x : BitVec n
i : Nat
h : i < m
h✝ : ¬n ≤ m
⊢ (BitVec.ofNat m x.toNat)[i] = x.getLsbD i

Tactic:
simp [getElem_eq_testBit_toNat, getLsbD]

Result:
case isFalse
n m : Nat
x : BitVec n
i : Nat
h : i < m
h✝ : ¬n ≤ m
⊢ x.toNat.testBit i = true → i < m

Proof state:
n m : Nat
x : BitVec n
i : Nat
h : i < m
⊢ (if h : n ≤ m then setWidth' h x else BitVec.ofNat m x.toNat)[i] = x.getLsbD i

Tactic:
split

Result:
case isTrue
n m : Nat
x : BitVec n
i : Nat
h : i < m
h✝ : n ≤ m
⊢ (setWidth' h✝ x)[i] = x.getLsbD i

case isFalse
n m : Nat
x : BitVec n
i : Nat
h : i < m
h✝ : ¬n ≤ m
⊢ (BitVec.ofNat m x.toNat)[i] = x.getLsbD i

Proof state:
case isTrue
n m : Nat
x : BitVec n
i : Nat
h : i < m
h✝ : n ≤ m
⊢ (setWidth' h✝ x)[i] = x.getLsbD i

Tactic:
rw [getElem_setWidth']

Result:
no goals

Proof state:
n m : Nat
x : BitVec n
i : Nat
h : i < m
⊢ (setWidth m x)[i] = x.getLsbD i

Tactic:
rw [setWidth]

Result:
n m : Nat
x : BitVec n
i : Nat
h : i < m
⊢ (if h : n ≤ m then setWidth' h x else BitVec.ofNat m x.toNat)[i] = x.getLsbD i

Proof state:
case isFalse
n m : Nat
x : BitVec n
i : Nat
h : i < m
h✝ : ¬n ≤ m
⊢ x.toNat.testBit i = true → i < m

Tactic:
omega

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Bounds.lean
theorem sin_lt (h : 0 < x) : sin x < x

Proof state:
case inr
x : ℝ
h : 0 < x
h' : x ≤ 1
hx : |x| = x
this : sin x - (x - x ^ 3 / 6) ≤ |x| ^ 4 * (5 / 96)
⊢ sin x < x

Tactic:
rw [sub_le_iff_le_add', hx] at this

Result:
case inr
x : ℝ
h : 0 < x
h' : x ≤ 1
hx : |x| = x
this : sin x ≤ x - x ^ 3 / 6 + x ^ 4 * (5 / 96)
⊢ sin x < x

Proof state:
x : ℝ
h : 0 < x
h' : x ≤ 1
hx : |x| = x
⊢ |x| ≤ 1

Tactic:
rwa [hx]

Result:
no goals

Proof state:
case inr
x : ℝ
h : 0 < x
h' : x ≤ 1
hx : |x| = x
this : sin x ≤ x - x ^ 3 / 6 + x ^ 4 * (5 / 96)
⊢ 3 ≤ 4

Tactic:
norm_num

Result:
no goals

Proof state:
case inr
x : ℝ
h : 0 < x
h' : x ≤ 1
⊢ sin x < x

Tactic:
have hx : |x| = x := abs_of_nonneg h.le

Result:
case inr
x : ℝ
h : 0 < x
h' : x ≤ 1
hx : |x| = x
⊢ sin x < x

Proof state:
case inr
x : ℝ
h : 0 < x
h' : x ≤ 1
hx : |x| = x
this : sin x ≤ x - x ^ 3 / 6 + x ^ 4 * (5 / 96)
⊢ x - x ^ 3 / 6 + x ^ 4 * (5 / 96) < x

Tactic:
rw [sub_add, sub_lt_self_iff, sub_pos, div_eq_mul_inv (x ^ 3)]

Result:
case inr
x : ℝ
h : 0 < x
h' : x ≤ 1
hx : |x| = x
this : sin x ≤ x - x ^ 3 / 6 + x ^ 4 * (5 / 96)
⊢ x ^ 4 * (5 / 96) < x ^ 3 * 6⁻¹

Proof state:
case inr
x : ℝ
h : 0 < x
h' : x ≤ 1
hx : |x| = x
this : sin x ≤ x - x ^ 3 / 6 + x ^ 4 * (5 / 96)
⊢ x ^ 4 ≤ x ^ 3

Tactic:
apply pow_le_pow_of_le_one h.le h'

Result:
case inr
x : ℝ
h : 0 < x
h' : x ≤ 1
hx : |x| = x
this : sin x ≤ x - x ^ 3 / 6 + x ^ 4 * (5 / 96)
⊢ 3 ≤ 4

Proof state:
case inl
x : ℝ
h : 0 < x
h' : 1 < x
⊢ sin x < x

Tactic:
exact (sin_le_one x).trans_lt h'

Result:
no goals

Proof state:
case inr
x : ℝ
h : 0 < x
h' : x ≤ 1
hx : |x| = x
this : sin x ≤ x - x ^ 3 / 6 + x ^ 4 * (5 / 96)
⊢ sin x < x

Tactic:
apply this.trans_lt

Result:
case inr
x : ℝ
h : 0 < x
h' : x ≤ 1
hx : |x| = x
this : sin x ≤ x - x ^ 3 / 6 + x ^ 4 * (5 / 96)
⊢ x - x ^ 3 / 6 + x ^ 4 * (5 / 96) < x

Proof state:
x : ℝ
h : 0 < x
⊢ sin x < x

Tactic:
rcases lt_or_le 1 x with h' | h'

Result:
case inl
x : ℝ
h : 0 < x
h' : 1 < x
⊢ sin x < x

case inr
x : ℝ
h : 0 < x
h' : x ≤ 1
⊢ sin x < x

Proof state:
x : ℝ
h : 0 < x
h' : x ≤ 1
hx : |x| = x
this : sin x ≤ x - x ^ 3 / 6 + x ^ 4 * (5 / 96)
⊢ 0 ≤ 5 / 96

Tactic:
norm_num

Result:
no goals

Proof state:
x : ℝ
h : 0 < x
h' : x ≤ 1
hx : |x| = x
this : sin x ≤ x - x ^ 3 / 6 + x ^ 4 * (5 / 96)
⊢ 5 / 96 < 6⁻¹

Tactic:
norm_num

Result:
no goals

Proof state:
case inr
x : ℝ
h : 0 < x
h' : x ≤ 1
hx : |x| = x
⊢ sin x < x

Tactic:
have := le_of_abs_le (sin_bound <| show |x| ≤ 1 by rwa [hx])

Result:
case inr
x : ℝ
h : 0 < x
h' : x ≤ 1
hx : |x| = x
this : sin x - (x - x ^ 3 / 6) ≤ |x| ^ 4 * (5 / 96)
⊢ sin x < x

Proof state:
case inr
x : ℝ
h : 0 < x
h' : x ≤ 1
hx : |x| = x
this : sin x ≤ x - x ^ 3 / 6 + x ^ 4 * (5 / 96)
⊢ x ^ 4 * (5 / 96) < x ^ 3 * 6⁻¹

Tactic:
refine mul_lt_mul' ?_ (by norm_num) (by norm_num) (pow_pos h 3)

Result:
case inr
x : ℝ
h : 0 < x
h' : x ≤ 1
hx : |x| = x
this : sin x ≤ x - x ^ 3 / 6 + x ^ 4 * (5 / 96)
⊢ x ^ 4 ≤ x ^ 3
-- Mathlib/LinearAlgebra/PiTensorProduct.lean
theorem span_tprod_eq_top :
    Submodule.span R (Set.range (tprod R)) = (⊤ : Submodule R (⨂[R] i, s i)) :=
  Submodule.eq_top_iff'.mpr fun t ↦ t.induction_on
    (fun _ _ ↦ Submodule.smul_mem _ _
      (Submodule.subset_span (by simp only [Set.mem_range, exists_apply_eq_apply])))
    (fun _ _ hx hy ↦ Submodule.add_mem _ hx hy)

Proof state:
ι : Type u_1
R : Type u_4
inst✝² : CommSemiring R
s : ι → Type u_7
inst✝¹ : (i : ι) → AddCommMonoid (s i)
inst✝ : (i : ι) → Module R (s i)
t : ⨂[R] (i : ι), s i
x✝¹ : R
x✝ : (i : ι) → s i
⊢ (tprod R) x✝ ∈ Set.range ⇑(tprod R)

Tactic:
simp only [Set.mem_range, exists_apply_eq_apply]

Result:
no goals
-- Mathlib/GroupTheory/Nilpotent.lean
theorem Subgroup.nilpotencyClass_le (H : Subgroup G) [hG : IsNilpotent G] :
    Group.nilpotencyClass H ≤ Group.nilpotencyClass G

Proof state:
G : Type u_1
inst✝ : Group G
H : Subgroup G
hG : IsNilpotent G
⊢ Nat.find ⋯ ≤ Nat.find ⋯

Tactic:
apply Nat.find_mono

Result:
case h
G : Type u_1
inst✝ : Group G
H : Subgroup G
hG : IsNilpotent G
⊢ ∀ (n : ℕ), lowerCentralSeries G n = ⊥ → lowerCentralSeries (↥H) n = ⊥

Proof state:
case h
G : Type u_1
inst✝ : Group G
H : Subgroup G
hG✝ : IsNilpotent G
n : ℕ
hG : lowerCentralSeries G n = ⊥
this : ∀ ⦃x : G⦄ (x_1 : ↥H), x_1 ∈ lowerCentralSeries (↥H) n ∧ H.subtype x_1 = x → x ∈ ⊥
⊢ lowerCentralSeries (↥H) n = ⊥

Tactic:
exact eq_bot_iff.mpr fun x hx => Subtype.ext (this x ⟨hx, rfl⟩)

Result:
no goals

Proof state:
G : Type u_1
inst✝ : Group G
H : Subgroup G
hG : IsNilpotent G
⊢ Nat.find ⋯ ≤ Nat.find ⋯

Tactic:
classical apply Nat.find_mono

Result:
case h
G : Type u_1
inst✝ : Group G
H : Subgroup G
hG : IsNilpotent G
⊢ ∀ (n : ℕ), lowerCentralSeries G n = ⊥ → lowerCentralSeries (↥H) n = ⊥

Proof state:
G : Type u_1
inst✝ : Group G
H : Subgroup G
hG : IsNilpotent G
⊢ nilpotencyClass ↥H ≤ nilpotencyClass G

Tactic:
repeat rw [← lowerCentralSeries_length_eq_nilpotencyClass]

Result:
G : Type u_1
inst✝ : Group G
H : Subgroup G
hG : IsNilpotent G
⊢ Nat.find ⋯ ≤ Nat.find ⋯

Proof state:
case h
G : Type u_1
inst✝ : Group G
H : Subgroup G
hG✝ : IsNilpotent G
n : ℕ
hG : lowerCentralSeries G n = ⊥
⊢ lowerCentralSeries (↥H) n = ⊥

Tactic:
have := lowerCentralSeries_map_subtype_le H n

Result:
case h
G : Type u_1
inst✝ : Group G
H : Subgroup G
hG✝ : IsNilpotent G
n : ℕ
hG : lowerCentralSeries G n = ⊥
this : map H.subtype (lowerCentralSeries (↥H) n) ≤ lowerCentralSeries G n
⊢ lowerCentralSeries (↥H) n = ⊥

Proof state:
case h
G : Type u_1
inst✝ : Group G
H : Subgroup G
hG : IsNilpotent G
⊢ ∀ (n : ℕ), lowerCentralSeries G n = ⊥ → lowerCentralSeries (↥H) n = ⊥

Tactic:
intro n hG

Result:
case h
G : Type u_1
inst✝ : Group G
H : Subgroup G
hG✝ : IsNilpotent G
n : ℕ
hG : lowerCentralSeries G n = ⊥
⊢ lowerCentralSeries (↥H) n = ⊥

Proof state:
G : Type u_1
inst✝ : Group G
H : Subgroup G
hG : IsNilpotent G
⊢ Nat.find ⋯ ≤ nilpotencyClass G

Tactic:
rw [← lowerCentralSeries_length_eq_nilpotencyClass]

Result:
G : Type u_1
inst✝ : Group G
H : Subgroup G
hG : IsNilpotent G
⊢ Nat.find ⋯ ≤ Nat.find ⋯

Proof state:
case h
G : Type u_1
inst✝ : Group G
H : Subgroup G
hG✝ : IsNilpotent G
n : ℕ
hG : lowerCentralSeries G n = ⊥
this : map H.subtype (lowerCentralSeries (↥H) n) ≤ lowerCentralSeries G n
⊢ lowerCentralSeries (↥H) n = ⊥

Tactic:
simp only [hG, SetLike.le_def, mem_map, forall_apply_eq_imp_iff₂, exists_imp] at this

Result:
case h
G : Type u_1
inst✝ : Group G
H : Subgroup G
hG✝ : IsNilpotent G
n : ℕ
hG : lowerCentralSeries G n = ⊥
this : ∀ ⦃x : G⦄ (x_1 : ↥H), x_1 ∈ lowerCentralSeries (↥H) n ∧ H.subtype x_1 = x → x ∈ ⊥
⊢ lowerCentralSeries (↥H) n = ⊥
-- Mathlib/MeasureTheory/Function/AEEqFun.lean
theorem compMeasurable_eq_mk (g : β → γ) (hg : Measurable g) (f : α →ₘ[μ] β) :
    compMeasurable g hg f =
    mk (g ∘ f) (hg.comp_aemeasurable f.aemeasurable).aestronglyMeasurable

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝⁹ : MeasurableSpace α
μ : Measure α
inst✝⁸ : TopologicalSpace β
inst✝⁷ : TopologicalSpace γ
inst✝⁶ : MeasurableSpace β
inst✝⁵ : PseudoMetrizableSpace β
inst✝⁴ : BorelSpace β
inst✝³ : MeasurableSpace γ
inst✝² : PseudoMetrizableSpace γ
inst✝¹ : OpensMeasurableSpace γ
inst✝ : SecondCountableTopology γ
g : β → γ
hg : Measurable g
f : α →ₘ[μ] β
⊢ compMeasurable g hg f = mk (g ∘ ↑f) ⋯

Tactic:
rw [← compMeasurable_mk g hg f f.aestronglyMeasurable, mk_coeFn]

Result:
no goals