harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Probability/Moments/IntegrableExpMul.lean
lemma integrable_pow_mul_cexp_of_re_mem_interior_integrableExpSet
    (hz : z.re ∈ interior (integrableExpSet X μ)) (n : ℕ) :
    Integrable (fun ω ↦ X ω ^ n * cexp (z * X ω)) μ

Proof state:
case h.e'_6.h.h.e'_5
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
z : ℂ
hz : z.re ∈ interior (integrableExpSet X μ)
n : ℕ
x✝ : Ω
⊢ ↑(X x✝) ^ n = ↑(X x✝ ^ ↑n)

Tactic:
simp

Result:
no goals

Proof state:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
z : ℂ
hz : z.re ∈ interior (integrableExpSet X μ)
n : ℕ
⊢ Integrable (fun ω => ↑(X ω) ^ n * cexp (z * ↑(X ω))) μ

Tactic:
convert integrable_rpow_mul_cexp_of_re_mem_interior_integrableExpSet hz (Nat.cast_nonneg n)

Result:
case h.e'_6.h.h.e'_5
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
z : ℂ
hz : z.re ∈ interior (integrableExpSet X μ)
n : ℕ
x✝ : Ω
⊢ ↑(X x✝) ^ n = ↑(X x✝ ^ ↑n)
-- Mathlib/Algebra/Group/PNatPowAssoc.lean
theorem ppow_eq_pow [Monoid M] [Pow M ℕ+] [PNatPowAssoc M] (x : M) (n : ℕ+) :
    x ^ n = x ^ (n : ℕ)

Proof state:
case succ
M : Type u_1
inst✝² : Monoid M
inst✝¹ : Pow M ℕ+
inst✝ : PNatPowAssoc M
x : M
k : ℕ+
hk : x ^ k = x ^ ↑k
⊢ x ^ (k + 1) = x ^ ↑(k + 1)

Tactic:
rw [ppow_add, ppow_one, PNat.add_coe, pow_add, PNat.one_coe, pow_one, ← hk]

Result:
no goals

Proof state:
case one
M : Type u_1
inst✝² : Monoid M
inst✝¹ : Pow M ℕ+
inst✝ : PNatPowAssoc M
x : M
⊢ x ^ 1 = x ^ ↑1

Tactic:
rw [ppow_one, PNat.one_coe, pow_one]

Result:
no goals

Proof state:
M : Type u_1
inst✝² : Monoid M
inst✝¹ : Pow M ℕ+
inst✝ : PNatPowAssoc M
x : M
n : ℕ+
⊢ x ^ n = x ^ ↑n

Tactic:
induction n with
| one => rw [ppow_one, PNat.one_coe, pow_one]
| succ k hk => rw [ppow_add, ppow_one, PNat.add_coe, pow_add, PNat.one_coe, pow_one, ← hk]

Result:
no goals
-- Mathlib/Analysis/Calculus/MeanValue.lean
theorem _root_.IsOpen.eqOn_of_fderiv_eq (hs : IsOpen s) (hs' : IsPreconnected s)
    (hf : DifferentiableOn 𝕜 f s) (hg : DifferentiableOn 𝕜 g s)
    (hf' : ∀ x ∈ s, fderiv 𝕜 f x = fderiv 𝕜 g x) (hx : x ∈ s) (hfgx : f x = g x) :
    s.EqOn f g

Proof state:
case intro
E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
𝕜 : Type u_3
G : Type u_4
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : IsRCLikeNormedField 𝕜
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f g : E → G
s : Set E
x : E
hs : IsOpen s
hs' : IsPreconnected s
hf : DifferentiableOn 𝕜 f s
hg : DifferentiableOn 𝕜 g s
hf' : ∀ x ∈ s, fderiv 𝕜 f x = fderiv 𝕜 g x
hx : x ∈ s
hfgx : f x = g x
a : G
ha : EqOn f (fun x => g x + a) s
⊢ EqOn f g s

Tactic:
obtain rfl := self_eq_add_right.mp (hfgx.symm.trans (ha hx))

Result:
case intro
E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
𝕜 : Type u_3
G : Type u_4
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : IsRCLikeNormedField 𝕜
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f g : E → G
s : Set E
x : E
hs : IsOpen s
hs' : IsPreconnected s
hf : DifferentiableOn 𝕜 f s
hg : DifferentiableOn 𝕜 g s
hf' : ∀ x ∈ s, fderiv 𝕜 f x = fderiv 𝕜 g x
hx : x ∈ s
hfgx : f x = g x
ha : EqOn f (fun x => g x + 0) s
⊢ EqOn f g s

Proof state:
E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
𝕜 : Type u_3
G : Type u_4
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : IsRCLikeNormedField 𝕜
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f g : E → G
s : Set E
x : E
hs : IsOpen s
hs' : IsPreconnected s
hf : DifferentiableOn 𝕜 f s
hg : DifferentiableOn 𝕜 g s
hf' : ∀ x ∈ s, fderiv 𝕜 f x = fderiv 𝕜 g x
hx : x ∈ s
hfgx : f x = g x
⊢ EqOn f g s

Tactic:
obtain ⟨a, ha⟩ := hs.exists_eq_add_of_fderiv_eq hs' hf hg hf'

Result:
case intro
E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
𝕜 : Type u_3
G : Type u_4
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : IsRCLikeNormedField 𝕜
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f g : E → G
s : Set E
x : E
hs : IsOpen s
hs' : IsPreconnected s
hf : DifferentiableOn 𝕜 f s
hg : DifferentiableOn 𝕜 g s
hf' : ∀ x ∈ s, fderiv 𝕜 f x = fderiv 𝕜 g x
hx : x ∈ s
hfgx : f x = g x
a : G
ha : EqOn f (fun x => g x + a) s
⊢ EqOn f g s

Proof state:
case intro
E : Type u_1
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
𝕜 : Type u_3
G : Type u_4
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : IsRCLikeNormedField 𝕜
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f g : E → G
s : Set E
x : E
hs : IsOpen s
hs' : IsPreconnected s
hf : DifferentiableOn 𝕜 f s
hg : DifferentiableOn 𝕜 g s
hf' : ∀ x ∈ s, fderiv 𝕜 f x = fderiv 𝕜 g x
hx : x ∈ s
hfgx : f x = g x
ha : EqOn f (fun x => g x + 0) s
⊢ EqOn f g s

Tactic:
simpa using ha

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Lebesgue/EqHaar.lean
theorem map_linearMap_addHaar_eq_smul_addHaar {f : E →ₗ[ℝ] E} (hf : LinearMap.det f ≠ 0) :
    Measure.map f μ = ENNReal.ofReal |(LinearMap.det f)⁻¹| • μ

Proof state:
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
f : E →ₗ[ℝ] E
hf : LinearMap.det f ≠ 0
ι : Type := Fin (finrank ℝ E)
this✝ : FiniteDimensional ℝ (ι → ℝ)
this : finrank ℝ E = finrank ℝ (ι → ℝ)
e : E ≃ₗ[ℝ] ι → ℝ
g : (ι → ℝ) →ₗ[ℝ] ι → ℝ
hg : g = ↑e ∘ₗ f ∘ₗ ↑e.symm
⊢ LinearMap.det (↑e ∘ₗ f ∘ₗ ↑e.symm) = LinearMap.det f

Tactic:
exact LinearMap.det_conj f e

Result:
no goals

Proof state:
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
f : E →ₗ[ℝ] E
hf : LinearMap.det f ≠ 0
ι : Type := Fin (finrank ℝ E)
⊢ map (⇑f) μ = ENNReal.ofReal |(LinearMap.det f)⁻¹| • μ

Tactic:
haveI : FiniteDimensional ℝ (ι → ℝ) := by infer_instance

Result:
E : Type u_1
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : FiniteDimensional ℝ E
μ : Measure E
inst✝ : μ.IsAddHaarMeasure
f : E →ₗ[ℝ] E
hf : LinearMap.det f ≠ 0
ι : Type := Fin (finrank ℝ E)
this : FiniteDimensional ℝ (ι → ℝ)
⊢ map (⇑f) μ = ENNReal.ofReal |(LinearMap.det f)⁻¹| • μ
-- Mathlib/Algebra/Polynomial/Degree/Support.lean
theorem card_supp_le_succ_natDegree (p : R[X]) : #p.support ≤ p.natDegree + 1

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
⊢ #p.support ≤ p.natDegree + 1

Tactic:
rw [← Finset.card_range (p.natDegree + 1)]

Result:
R : Type u
inst✝ : Semiring R
p : R[X]
⊢ #p.support ≤ #(range (p.natDegree + 1))

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
⊢ #p.support ≤ #(range (p.natDegree + 1))

Tactic:
exact Finset.card_le_card supp_subset_range_natDegree_succ

Result:
no goals
-- Mathlib/AlgebraicGeometry/IdealSheaf.lean
lemma vanishingIdeal_support {I : IdealSheafData X} :
    vanishingIdeal I.support = I.radical

Proof state:
case ideal.h
X : Scheme
I : X.IdealSheafData
U : ↑X.affineOpens
⊢ (vanishingIdeal I.support).ideal U = I.radical.ideal U

Tactic:
dsimp

Result:
case ideal.h
X : Scheme
I : X.IdealSheafData
U : ↑X.affineOpens
⊢ PrimeSpectrum.vanishingIdeal (⇑(ConcreteCategory.hom (IsAffineOpen.fromSpec ⋯).base) ⁻¹' I.support) =
    (I.ideal U).radical

Proof state:
case ideal.h
X : Scheme
I : X.IdealSheafData
U : ↑X.affineOpens
⊢ PrimeSpectrum.vanishingIdeal (⇑(ConcreteCategory.hom (IsAffineOpen.fromSpec ⋯).base) ⁻¹' I.support) =
    PrimeSpectrum.vanishingIdeal (PrimeSpectrum.zeroLocus ↑(I.ideal U))

Tactic:
congr 1

Result:
case ideal.h.e_t
X : Scheme
I : X.IdealSheafData
U : ↑X.affineOpens
⊢ ⇑(ConcreteCategory.hom (IsAffineOpen.fromSpec ⋯).base) ⁻¹' I.support = PrimeSpectrum.zeroLocus ↑(I.ideal U)

Proof state:
case ideal.h
X : Scheme
I : X.IdealSheafData
U : ↑X.affineOpens
⊢ PrimeSpectrum.vanishingIdeal (⇑(ConcreteCategory.hom (IsAffineOpen.fromSpec ⋯).base) ⁻¹' I.support) =
    (I.ideal U).radical

Tactic:
rw [← vanishingIdeal_zeroLocus_eq_radical]

Result:
case ideal.h
X : Scheme
I : X.IdealSheafData
U : ↑X.affineOpens
⊢ PrimeSpectrum.vanishingIdeal (⇑(ConcreteCategory.hom (IsAffineOpen.fromSpec ⋯).base) ⁻¹' I.support) =
    PrimeSpectrum.vanishingIdeal (PrimeSpectrum.zeroLocus ↑(I.ideal U))

Proof state:
case ideal.h.e_t.a
X : Scheme
I : X.IdealSheafData
U : ↑X.affineOpens
⊢ ⇑(ConcreteCategory.hom (IsAffineOpen.fromSpec ⋯).base) ''
      (⇑(ConcreteCategory.hom (IsAffineOpen.fromSpec ⋯).base) ⁻¹' I.support) =
    ⇑(ConcreteCategory.hom (IsAffineOpen.fromSpec ⋯).base) '' PrimeSpectrum.zeroLocus ↑(I.ideal U)

Tactic:
rw [Set.image_preimage_eq_inter_range, IsAffineOpen.range_fromSpec,
  IsAffineOpen.fromSpec_image_zeroLocus, support_inter]

Result:
no goals

Proof state:
X : Scheme
I : X.IdealSheafData
⊢ vanishingIdeal I.support = I.radical

Tactic:
ext U : 2

Result:
case ideal.h
X : Scheme
I : X.IdealSheafData
U : ↑X.affineOpens
⊢ (vanishingIdeal I.support).ideal U = I.radical.ideal U

Proof state:
case ideal.h.e_t
X : Scheme
I : X.IdealSheafData
U : ↑X.affineOpens
⊢ ⇑(ConcreteCategory.hom (IsAffineOpen.fromSpec ⋯).base) ⁻¹' I.support = PrimeSpectrum.zeroLocus ↑(I.ideal U)

Tactic:
apply U.2.fromSpec.isOpenEmbedding.injective.image_injective

Result:
case ideal.h.e_t.a
X : Scheme
I : X.IdealSheafData
U : ↑X.affineOpens
⊢ ⇑(ConcreteCategory.hom (IsAffineOpen.fromSpec ⋯).base) ''
      (⇑(ConcreteCategory.hom (IsAffineOpen.fromSpec ⋯).base) ⁻¹' I.support) =
    ⇑(ConcreteCategory.hom (IsAffineOpen.fromSpec ⋯).base) '' PrimeSpectrum.zeroLocus ↑(I.ideal U)
-- Mathlib/Data/Holor.lean
theorem cprankMax_add [Monoid α] [AddMonoid α] :
    ∀ {m : ℕ} {n : ℕ} {x : Holor α ds} {y : Holor α ds},
      CPRankMax m x → CPRankMax n y → CPRankMax (m + n) (x + y)
  | 0, n, x, y, hx, hy => by
    match hx with
    | CPRankMax.zero => simp only [zero_add, hy]
  | m + 1, n, _, y, CPRankMax.succ _ x₁ x₂ hx₁ hx₂, hy => by
    simp only [add_comm, add_assoc]
    apply CPRankMax.succ
    · assumption
    · -- Porting note: Single line is added.
      simp only [Nat.add_eq, add_zero, add_comm n m]
      exact cprankMax_add hx₂ hy

Proof state:
case a
α : Type
ds : List ℕ
inst✝¹ : Monoid α
inst✝ : AddMonoid α
m n : ℕ
y x₁ x₂ : Holor α ds
hx₁ : x₁.CPRankMax1
hx₂ : CPRankMax m x₂
hy : CPRankMax n y
⊢ CPRankMax (m + n) (x₂ + y)

Tactic:
exact cprankMax_add hx₂ hy

Result:
no goals

Proof state:
α : Type
ds : List ℕ
inst✝¹ : Monoid α
inst✝ : AddMonoid α
m n : ℕ
y x₁ x₂ : Holor α ds
hx₁ : x₁.CPRankMax1
hx₂ : CPRankMax m x₂
hy : CPRankMax n y
⊢ CPRankMax (n + (m + 1)) (x₁ + (x₂ + y))

Tactic:
apply CPRankMax.succ

Result:
case a
α : Type
ds : List ℕ
inst✝¹ : Monoid α
inst✝ : AddMonoid α
m n : ℕ
y x₁ x₂ : Holor α ds
hx₁ : x₁.CPRankMax1
hx₂ : CPRankMax m x₂
hy : CPRankMax n y
⊢ x₁.CPRankMax1

case a
α : Type
ds : List ℕ
inst✝¹ : Monoid α
inst✝ : AddMonoid α
m n : ℕ
y x₁ x₂ : Holor α ds
hx₁ : x₁.CPRankMax1
hx₂ : CPRankMax m x₂
hy : CPRankMax n y
⊢ CPRankMax (n.add m) (x₂ + y)

Proof state:
α : Type
ds : List ℕ
inst✝¹ : Monoid α
inst✝ : AddMonoid α
n : ℕ
x y : Holor α ds
hx : CPRankMax 0 x
hy : CPRankMax n y
⊢ CPRankMax (0 + n) (0 + y)

Tactic:
simp only [zero_add, hy]

Result:
no goals

Proof state:
case a
α : Type
ds : List ℕ
inst✝¹ : Monoid α
inst✝ : AddMonoid α
m n : ℕ
y x₁ x₂ : Holor α ds
hx₁ : x₁.CPRankMax1
hx₂ : CPRankMax m x₂
hy : CPRankMax n y
⊢ CPRankMax (n.add m) (x₂ + y)

Tactic:
simp only [Nat.add_eq, add_zero, add_comm n m]

Result:
case a
α : Type
ds : List ℕ
inst✝¹ : Monoid α
inst✝ : AddMonoid α
m n : ℕ
y x₁ x₂ : Holor α ds
hx₁ : x₁.CPRankMax1
hx₂ : CPRankMax m x₂
hy : CPRankMax n y
⊢ CPRankMax (m + n) (x₂ + y)

Proof state:
α : Type
ds : List ℕ
inst✝¹ : Monoid α
inst✝ : AddMonoid α
n : ℕ
x y : Holor α ds
hx : CPRankMax 0 x
hy : CPRankMax n y
⊢ CPRankMax (0 + n) (x + y)

Tactic:
match hx with
| CPRankMax.zero => simp only [zero_add, hy]

Result:
no goals

Proof state:
α : Type
ds : List ℕ
inst✝¹ : Monoid α
inst✝ : AddMonoid α
m n : ℕ
y x₁ x₂ : Holor α ds
hx₁ : x₁.CPRankMax1
hx₂ : CPRankMax m x₂
hy : CPRankMax n y
⊢ CPRankMax (m + 1 + n) (x₁ + x₂ + y)

Tactic:
simp only [add_comm, add_assoc]

Result:
α : Type
ds : List ℕ
inst✝¹ : Monoid α
inst✝ : AddMonoid α
m n : ℕ
y x₁ x₂ : Holor α ds
hx₁ : x₁.CPRankMax1
hx₂ : CPRankMax m x₂
hy : CPRankMax n y
⊢ CPRankMax (n + (m + 1)) (x₁ + (x₂ + y))

Proof state:
case a
α : Type
ds : List ℕ
inst✝¹ : Monoid α
inst✝ : AddMonoid α
m n : ℕ
y x₁ x₂ : Holor α ds
hx₁ : x₁.CPRankMax1
hx₂ : CPRankMax m x₂
hy : CPRankMax n y
⊢ x₁.CPRankMax1

Tactic:
assumption

Result:
no goals
-- Mathlib/Topology/Algebra/Polynomial.lean
theorem eq_one_of_roots_le {p : F[X]} {f : F →+* K} {B : ℝ} (hB : B < 0) (h1 : p.Monic)
    (h2 : Splits f p) (h3 : ∀ z ∈ (map f p).roots, ‖z‖ ≤ B) : p = 1 :=
  h1.natDegree_eq_zero_iff_eq_one.mp (by
    contrapose! hB
    rw [← h1.natDegree_map f, natDegree_eq_card_roots' h2] at hB
    obtain ⟨z, hz⟩ := card_pos_iff_exists_mem.mp (zero_lt_iff.mpr hB)
    exact le_trans (norm_nonneg _) (h3 z hz))

Proof state:
F : Type u_3
K : Type u_4
inst✝¹ : CommRing F
inst✝ : NormedField K
p : F[X]
f : F →+* K
B : ℝ
h1 : p.Monic
h2 : Splits f p
h3 : ∀ z ∈ (map f p).roots, ‖z‖ ≤ B
hB : (map f p).roots.card ≠ 0
⊢ 0 ≤ B

Tactic:
obtain ⟨z, hz⟩ := card_pos_iff_exists_mem.mp (zero_lt_iff.mpr hB)

Result:
case intro
F : Type u_3
K : Type u_4
inst✝¹ : CommRing F
inst✝ : NormedField K
p : F[X]
f : F →+* K
B : ℝ
h1 : p.Monic
h2 : Splits f p
h3 : ∀ z ∈ (map f p).roots, ‖z‖ ≤ B
hB : (map f p).roots.card ≠ 0
z : K
hz : z ∈ (map f p).roots
⊢ 0 ≤ B

Proof state:
case intro
F : Type u_3
K : Type u_4
inst✝¹ : CommRing F
inst✝ : NormedField K
p : F[X]
f : F →+* K
B : ℝ
h1 : p.Monic
h2 : Splits f p
h3 : ∀ z ∈ (map f p).roots, ‖z‖ ≤ B
hB : (map f p).roots.card ≠ 0
z : K
hz : z ∈ (map f p).roots
⊢ 0 ≤ B

Tactic:
exact le_trans (norm_nonneg _) (h3 z hz)

Result:
no goals

Proof state:
F : Type u_3
K : Type u_4
inst✝¹ : CommRing F
inst✝ : NormedField K
p : F[X]
f : F →+* K
B : ℝ
h1 : p.Monic
h2 : Splits f p
h3 : ∀ z ∈ (map f p).roots, ‖z‖ ≤ B
hB : p.natDegree ≠ 0
⊢ 0 ≤ B

Tactic:
rw [← h1.natDegree_map f, natDegree_eq_card_roots' h2] at hB

Result:
F : Type u_3
K : Type u_4
inst✝¹ : CommRing F
inst✝ : NormedField K
p : F[X]
f : F →+* K
B : ℝ
h1 : p.Monic
h2 : Splits f p
h3 : ∀ z ∈ (map f p).roots, ‖z‖ ≤ B
hB : (map f p).roots.card ≠ 0
⊢ 0 ≤ B

Proof state:
F : Type u_3
K : Type u_4
inst✝¹ : CommRing F
inst✝ : NormedField K
p : F[X]
f : F →+* K
B : ℝ
hB : B < 0
h1 : p.Monic
h2 : Splits f p
h3 : ∀ z ∈ (map f p).roots, ‖z‖ ≤ B
⊢ p.natDegree = 0

Tactic:
contrapose! hB

Result:
F : Type u_3
K : Type u_4
inst✝¹ : CommRing F
inst✝ : NormedField K
p : F[X]
f : F →+* K
B : ℝ
h1 : p.Monic
h2 : Splits f p
h3 : ∀ z ∈ (map f p).roots, ‖z‖ ≤ B
hB : p.natDegree ≠ 0
⊢ 0 ≤ B
-- Mathlib/MeasureTheory/Measure/Stieltjes.lean
theorem borel_le_measurable : borel ℝ ≤ f.outer.caratheodory

Proof state:
f : StieltjesFunction
⊢ MeasurableSpace.generateFrom (range Ioi) ≤ f.outer.caratheodory

Tactic:
refine MeasurableSpace.generateFrom_le ?_

Result:
f : StieltjesFunction
⊢ ∀ t ∈ range Ioi, MeasurableSet t

Proof state:
f : StieltjesFunction
⊢ borel ℝ ≤ f.outer.caratheodory

Tactic:
rw [borel_eq_generateFrom_Ioi]

Result:
f : StieltjesFunction
⊢ MeasurableSpace.generateFrom (range Ioi) ≤ f.outer.caratheodory

Proof state:
f : StieltjesFunction
⊢ ∀ t ∈ range Ioi, MeasurableSet t

Tactic:
simp +contextual [f.measurableSet_Ioi]

Result:
no goals
-- Mathlib/Probability/Kernel/Disintegration/Integral.lean
lemma setLIntegral_condKernel_eq_measure_prod (a : α) {s : Set β} (hs : MeasurableSet s)
    {t : Set Ω} (ht : MeasurableSet t) :
    ∫⁻ b in s, Kernel.condKernel κ (a, b) t ∂(Kernel.fst κ a) = κ a (s ×ˢ t)

Proof state:
α : Type u_1
β : Type u_2
Ω : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst✝⁴ : MeasurableSpace Ω
inst✝³ : StandardBorelSpace Ω
inst✝² : Nonempty Ω
inst✝¹ : CountableOrCountablyGenerated α β
κ : Kernel α (β × Ω)
inst✝ : IsFiniteKernel κ
a : α
s : Set β
hs : MeasurableSet s
t : Set Ω
ht : MeasurableSet t
this : (κ a) (s ×ˢ t) = ((κ.fst ⊗ₖ κ.condKernel) a) (s ×ˢ t)
⊢ ∫⁻ (b : β) in s, (κ.condKernel (a, b)) t ∂κ.fst a = ∫⁻ (b : β), (κ.condKernel (a, b)) {c | (b, c) ∈ s ×ˢ t} ∂κ.fst a

Tactic:
classical
have : ∀ b, Kernel.condKernel κ (a, b) {c | (b, c) ∈ s ×ˢ t}
    = s.indicator (fun b ↦ Kernel.condKernel κ (a, b) t) b := by
  intro b
  by_cases hb : b ∈ s <;> simp [hb]
simp_rw [this]
rw [lintegral_indicator hs]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
Ω : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst✝⁴ : MeasurableSpace Ω
inst✝³ : StandardBorelSpace Ω
inst✝² : Nonempty Ω
inst✝¹ : CountableOrCountablyGenerated α β
κ : Kernel α (β × Ω)
inst✝ : IsFiniteKernel κ
a : α
s : Set β
hs : MeasurableSet s
t : Set Ω
ht : MeasurableSet t
⊢ ∫⁻ (b : β) in s, (κ.condKernel (a, b)) t ∂κ.fst a = (κ a) (s ×ˢ t)

Tactic:
have : κ a (s ×ˢ t) = (Kernel.fst κ ⊗ₖ Kernel.condKernel κ) a (s ×ˢ t) := by
  congr; exact (κ.disintegrate _).symm

Result:
α : Type u_1
β : Type u_2
Ω : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
inst✝⁴ : MeasurableSpace Ω
inst✝³ : StandardBorelSpace Ω
inst✝² : Nonempty Ω
inst✝¹ : CountableOrCountablyGenerated α β
κ : Kernel α (β × Ω)
inst✝ : IsFiniteKernel κ
a : α
s : Set β
hs : MeasurableSet s
t : Set Ω
ht : MeasurableSet t
this : (κ a) (s ×ˢ t) = ((κ.fst ⊗ₖ κ.condKernel) a) (s ×ˢ t)
⊢ ∫⁻ (b : β) in s, (κ.condKernel (a, b)) t ∂κ.fst a = (κ a) (s ×ˢ t)
-- Mathlib/Algebra/Lie/Weights/RootSystem.lean
lemma chainTopCoeff_add_chainBotCoeff :
    chainTopCoeff α β + chainBotCoeff α β = chainLength α β

Proof state:
K : Type u_1
L : Type u_2
inst✝⁷ : Field K
inst✝⁶ : CharZero K
inst✝⁵ : LieRing L
inst✝⁴ : LieAlgebra K L
inst✝³ : IsKilling K L
inst✝² : FiniteDimensional K L
H : LieSubalgebra K L
inst✝¹ : H.IsCartanSubalgebra
inst✝ : IsTriangularizable K (↥H) L
α β : Weight K (↥H) L
⊢ chainTopCoeff (⇑α) β + chainBotCoeff (⇑α) β = chainLength α β

Tactic:
rw [add_comm, chainBotCoeff_add_chainTopCoeff]

Result:
no goals
-- Mathlib/GroupTheory/GroupAction/Primitive.lean
theorem IsPreprimitive.of_isTrivialBlock_of_not_mem_fixedPoints {a : X} (ha : a ∉ fixedPoints G X)
    (H : ∀ ⦃B : Set X⦄, a ∈ B → IsBlock G B → IsTrivialBlock B) :
    IsPreprimitive G X :=
  have : IsPretransitive G X

Proof state:
case inr.intro.intro
G : Type u_1
X : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G X
a : X
ha : a ∉ fixedPoints G X
H : ∀ ⦃B : Set X⦄, a ∈ B → IsBlock G B → IsTrivialBlock B
this : IsPretransitive G X
B : Set X
hB : IsBlock G B
b : X
hb : b ∈ B
g : G
hg : g • b = a
⊢ IsTrivialBlock B

Tactic:
rw [← IsTrivialBlock.smul_iff g]

Result:
case inr.intro.intro
G : Type u_1
X : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G X
a : X
ha : a ∉ fixedPoints G X
H : ∀ ⦃B : Set X⦄, a ∈ B → IsBlock G B → IsTrivialBlock B
this : IsPretransitive G X
B : Set X
hB : IsBlock G B
b : X
hb : b ∈ B
g : G
hg : g • b = a
⊢ IsTrivialBlock (g • B)

Proof state:
case inr.intro
G : Type u_1
X : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G X
a : X
ha : a ∉ fixedPoints G X
H : ∀ ⦃B : Set X⦄, a ∈ B → IsBlock G B → IsTrivialBlock B
this : IsPretransitive G X
B : Set X
hB : IsBlock G B
b : X
hb : b ∈ B
⊢ IsTrivialBlock B

Tactic:
obtain ⟨g, hg⟩ := exists_smul_eq G b a

Result:
case inr.intro.intro
G : Type u_1
X : Type u_2
inst✝¹ : Group G
inst✝ : MulAction G X
a : X
ha : a ∉ fixedPoints G X
H : ∀ ⦃B : Set X⦄, a ∈ B → IsBlock G B → IsTrivialBlock B
this : IsPretransitive G X
B : Set X
hB : IsBlock G B
b : X
hb : b ∈ B
g : G
hg : g • b = a
⊢ IsTrivialBlock B
-- Mathlib/Data/Set/Image.lean
theorem preimage_congr {f g : α → β} {s : Set β} (h : ∀ x : α, f x = g x) : f ⁻¹' s = g ⁻¹' s

Proof state:
case h
α : Type u_1
β : Type u_2
f g : α → β
s : Set β
h : ∀ (x : α), f x = g x
x : α
⊢ x ∈ f ⁻¹' s ↔ x ∈ g ⁻¹' s

Tactic:
simp [h]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
f g : α → β
s : Set β
h : ∀ (x : α), f x = g x
⊢ f ⁻¹' s = g ⁻¹' s

Tactic:
congr with x

Result:
case h
α : Type u_1
β : Type u_2
f g : α → β
s : Set β
h : ∀ (x : α), f x = g x
x : α
⊢ x ∈ f ⁻¹' s ↔ x ∈ g ⁻¹' s
-- Mathlib/Algebra/AddTorsor/Basic.lean
theorem vsub_sub_vsub_cancel_left (p₁ p₂ p₃ : P) : p₃ -ᵥ p₂ - (p₃ -ᵥ p₁) = p₁ -ᵥ p₂

Proof state:
G : Type u_1
P : Type u_2
inst✝¹ : AddCommGroup G
inst✝ : AddTorsor G P
p₁ p₂ p₃ : P
⊢ p₃ -ᵥ p₂ - (p₃ -ᵥ p₁) = p₁ -ᵥ p₂

Tactic:
rw [sub_eq_add_neg, neg_vsub_eq_vsub_rev, add_comm, vsub_add_vsub_cancel]

Result:
no goals
-- Mathlib/NumberTheory/Bertrand.lean
theorem exists_prime_lt_and_le_two_mul_eventually (n : ℕ) (n_large : 512 ≤ n) :
    ∃ p : ℕ, p.Prime ∧ n < p ∧ p ≤ 2 * n

Proof state:
n : ℕ
n_large : 512 ≤ n
no_prime : ¬∃ p, Prime p ∧ n < p ∧ p ≤ 2 * n
H1 : n * (2 * n) ^ (2 * n).sqrt * 4 ^ (2 * n / 3) ≤ 4 ^ n
⊢ 4 ≤ 512

Tactic:
norm_num1

Result:
no goals

Proof state:
n : ℕ
n_large : 512 ≤ n
no_prime : ¬∃ p, Prime p ∧ n < p ∧ p ≤ 2 * n
H1 : n * (2 * n) ^ (2 * n).sqrt * 4 ^ (2 * n / 3) ≤ 4 ^ n
⊢ False

Tactic:
have H2 : 4 ^ n < n * n.centralBinom :=
  Nat.four_pow_lt_mul_centralBinom n (le_trans (by norm_num1) n_large)

Result:
n : ℕ
n_large : 512 ≤ n
no_prime : ¬∃ p, Prime p ∧ n < p ∧ p ≤ 2 * n
H1 : n * (2 * n) ^ (2 * n).sqrt * 4 ^ (2 * n / 3) ≤ 4 ^ n
H2 : 4 ^ n < n * n.centralBinom
⊢ False

Proof state:
n : ℕ
n_large : 512 ≤ n
no_prime : ¬∃ p, Prime p ∧ n < p ∧ p ≤ 2 * n
H1 : n * (2 * n) ^ (2 * n).sqrt * 4 ^ (2 * n / 3) ≤ 4 ^ n
H2 : 4 ^ n < n * n.centralBinom
H3 : n.centralBinom ≤ (2 * n) ^ (2 * n).sqrt * 4 ^ (2 * n / 3)
⊢ False

Tactic:
rw [mul_assoc] at H1

Result:
n : ℕ
n_large : 512 ≤ n
no_prime : ¬∃ p, Prime p ∧ n < p ∧ p ≤ 2 * n
H1 : n * ((2 * n) ^ (2 * n).sqrt * 4 ^ (2 * n / 3)) ≤ 4 ^ n
H2 : 4 ^ n < n * n.centralBinom
H3 : n.centralBinom ≤ (2 * n) ^ (2 * n).sqrt * 4 ^ (2 * n / 3)
⊢ False

Proof state:
n : ℕ
n_large : 512 ≤ n
no_prime : ¬∃ p, Prime p ∧ n < p ∧ p ≤ 2 * n
⊢ False

Tactic:
have H1 : n * (2 * n) ^ sqrt (2 * n) * 4 ^ (2 * n / 3) ≤ 4 ^ n := bertrand_main_inequality n_large

Result:
n : ℕ
n_large : 512 ≤ n
no_prime : ¬∃ p, Prime p ∧ n < p ∧ p ≤ 2 * n
H1 : n * (2 * n) ^ (2 * n).sqrt * 4 ^ (2 * n / 3) ≤ 4 ^ n
⊢ False

Proof state:
n : ℕ
n_large : 512 ≤ n
no_prime : ¬∃ p, Prime p ∧ n < p ∧ p ≤ 2 * n
H1 : n * (2 * n) ^ (2 * n).sqrt * 4 ^ (2 * n / 3) ≤ 4 ^ n
H2 : 4 ^ n < n * n.centralBinom
⊢ False

Tactic:
have H3 : n.centralBinom ≤ (2 * n) ^ sqrt (2 * n) * 4 ^ (2 * n / 3) :=
  centralBinom_le_of_no_bertrand_prime n (lt_of_lt_of_le (by norm_num1) n_large) no_prime

Result:
n : ℕ
n_large : 512 ≤ n
no_prime : ¬∃ p, Prime p ∧ n < p ∧ p ≤ 2 * n
H1 : n * (2 * n) ^ (2 * n).sqrt * 4 ^ (2 * n / 3) ≤ 4 ^ n
H2 : 4 ^ n < n * n.centralBinom
H3 : n.centralBinom ≤ (2 * n) ^ (2 * n).sqrt * 4 ^ (2 * n / 3)
⊢ False

Proof state:
n : ℕ
n_large : 512 ≤ n
⊢ ∃ p, Prime p ∧ n < p ∧ p ≤ 2 * n

Tactic:
by_contra no_prime

Result:
n : ℕ
n_large : 512 ≤ n
no_prime : ¬∃ p, Prime p ∧ n < p ∧ p ≤ 2 * n
⊢ False

Proof state:
n : ℕ
n_large : 512 ≤ n
no_prime : ¬∃ p, Prime p ∧ n < p ∧ p ≤ 2 * n
H1 : n * ((2 * n) ^ (2 * n).sqrt * 4 ^ (2 * n / 3)) ≤ 4 ^ n
H2 : 4 ^ n < n * n.centralBinom
H3 : n.centralBinom ≤ (2 * n) ^ (2 * n).sqrt * 4 ^ (2 * n / 3)
⊢ False

Tactic:
exact not_le.2 H2 ((mul_le_mul_left' H3 n).trans H1)

Result:
no goals

Proof state:
n : ℕ
n_large : 512 ≤ n
no_prime : ¬∃ p, Prime p ∧ n < p ∧ p ≤ 2 * n
H1 : n * (2 * n) ^ (2 * n).sqrt * 4 ^ (2 * n / 3) ≤ 4 ^ n
H2 : 4 ^ n < n * n.centralBinom
⊢ 2 < 512

Tactic:
norm_num1

Result:
no goals
-- Mathlib/Data/Matroid/Basic.lean
theorem Indep.subset_isBasis_of_subset (hI : M.Indep I) (hIX : I ⊆ X)
    (hX : X ⊆ M.E

Proof state:
α : Type u_1
M : Matroid α
I X : Set α
hI : M.Indep I
hIX : I ⊆ X
hX : autoParam (X ⊆ M.E) _auto✝
⊢ ∃ J, M.IsBasis J X ∧ I ⊆ J

Tactic:
obtain ⟨J, hJ, hJmax⟩ := M.maximality X hX I hI hIX

Result:
case intro.intro
α : Type u_1
M : Matroid α
I X : Set α
hI : M.Indep I
hIX : I ⊆ X
hX : autoParam (X ⊆ M.E) _auto✝
J : Set α
hJ : I ⊆ J
hJmax : Maximal (fun K => M.Indep K ∧ K ⊆ X) J
⊢ ∃ J, M.IsBasis J X ∧ I ⊆ J

Proof state:
case intro.intro
α : Type u_1
M : Matroid α
I X : Set α
hI : M.Indep I
hIX : I ⊆ X
hX : autoParam (X ⊆ M.E) _auto✝
J : Set α
hJ : I ⊆ J
hJmax : Maximal (fun K => M.Indep K ∧ K ⊆ X) J
⊢ ∃ J, M.IsBasis J X ∧ I ⊆ J

Tactic:
exact ⟨J, ⟨hJmax, hX⟩, hJ⟩

Result:
no goals