harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Topology/Order/DenselyOrdered.lean
theorem interior_Ico [NoMinOrder α] {a b : α} : interior (Ico a b) = Ioo a b

Proof state:
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : DenselyOrdered α
inst✝ : NoMinOrder α
a b : α
⊢ interior (Ico a b) = Ioo a b

Tactic:
rw [← Ici_inter_Iio, interior_inter, interior_Ici, interior_Iio, Ioi_inter_Iio]

Result:
no goals
-- Mathlib/Topology/Gluing.lean
theorem isOpen_iff (U : Set 𝖣.glued) : IsOpen U ↔ ∀ i, IsOpen (𝖣.ι i ⁻¹' U)

Proof state:
D : GlueData
U : Set ↑D.glued
⊢ IsOpen U ↔ ∀ (i : D.J), IsOpen (⇑(ConcreteCategory.hom (Multicoequalizer.π D.diagram i)) ⁻¹' U)

Tactic:
simp_rw [← Multicoequalizer.ι_sigmaπ 𝖣.diagram]

Result:
D : GlueData
U : Set ↑D.glued
⊢ IsOpen U ↔
    ∀ (i : D.J), IsOpen (⇑(ConcreteCategory.hom (Sigma.ι D.diagram.right i ≫ Multicoequalizer.sigmaπ D.diagram)) ⁻¹' U)

Proof state:
D : GlueData
U : Set ↑D.glued
⊢ IsOpen U ↔
    ∀ (i : D.J), IsOpen (⇑(ConcreteCategory.hom (Sigma.ι D.diagram.right i ≫ Multicoequalizer.sigmaπ D.diagram)) ⁻¹' U)

Tactic:
rw [← (homeoOfIso (Multicoequalizer.isoCoequalizer 𝖣.diagram).symm).isOpen_preimage]

Result:
D : GlueData
U : Set ↑D.glued
⊢ IsOpen (⇑(homeoOfIso (Multicoequalizer.isoCoequalizer D.diagram).symm) ⁻¹' U) ↔
    ∀ (i : D.J), IsOpen (⇑(ConcreteCategory.hom (Sigma.ι D.diagram.right i ≫ Multicoequalizer.sigmaπ D.diagram)) ⁻¹' U)

Proof state:
D : GlueData
U : Set ↑D.glued
⊢ IsOpen (⇑(homeoOfIso (Multicoequalizer.isoCoequalizer D.diagram).symm) ⁻¹' U) ↔
    ∀ (i : D.J), IsOpen (⇑(ConcreteCategory.hom (Sigma.ι D.diagram.right i ≫ Multicoequalizer.sigmaπ D.diagram)) ⁻¹' U)

Tactic:
rw [coequalizer_isOpen_iff, colimit_isOpen_iff.{u}]

Result:
D : GlueData
U : Set ↑D.glued
⊢ (∀ (j : Discrete (MultispanShape.prod D.J).R),
      IsOpen
        (⇑(ConcreteCategory.hom (colimit.ι (Discrete.functor D.diagram.right) j)) ⁻¹'
          (⇑(ConcreteCategory.hom (coequalizer.π D.diagram.fstSigmaMap D.diagram.sndSigmaMap)) ⁻¹'
            (⇑(homeoOfIso (Multicoequalizer.isoCoequalizer D.diagram).symm) ⁻¹' U)))) ↔
    ∀ (i : D.J), IsOpen (⇑(ConcreteCategory.hom (Sigma.ι D.diagram.right i ≫ Multicoequalizer.sigmaπ D.diagram)) ⁻¹' U)

Proof state:
D : GlueData
U : Set ↑D.glued
⊢ (∀ (j : Discrete (MultispanShape.prod D.J).R),
      IsOpen
        (⇑(ConcreteCategory.hom (colimit.ι (Discrete.functor D.diagram.right) j)) ⁻¹'
          (⇑(ConcreteCategory.hom (coequalizer.π D.diagram.fstSigmaMap D.diagram.sndSigmaMap)) ⁻¹'
            (⇑(homeoOfIso (Multicoequalizer.isoCoequalizer D.diagram).symm) ⁻¹' U)))) ↔
    ∀ (i : D.J), IsOpen (⇑(ConcreteCategory.hom (Sigma.ι D.diagram.right i ≫ Multicoequalizer.sigmaπ D.diagram)) ⁻¹' U)

Tactic:
tauto

Result:
no goals

Proof state:
D : GlueData
U : Set ↑D.glued
⊢ IsOpen U ↔ ∀ (i : D.J), IsOpen (⇑(ConcreteCategory.hom (D.ι i)) ⁻¹' U)

Tactic:
delta CategoryTheory.GlueData.ι

Result:
D : GlueData
U : Set ↑D.glued
⊢ IsOpen U ↔ ∀ (i : D.J), IsOpen (⇑(ConcreteCategory.hom (Multicoequalizer.π D.diagram i)) ⁻¹' U)
-- Mathlib/Data/Finsupp/Order.lean
lemma mapDomain_mono : Monotone (mapDomain f : (ι →₀ α) → (κ →₀ α))

Proof state:
ι : Type u_1
κ : Type u_2
α : Type u_3
inst✝ : OrderedAddCommMonoid α
f : ι → κ
g₁ g₂ : ι →₀ α
h : g₁ ≤ g₂
⊢ ∀ i ∈ g₁.support ∪ g₂.support, single (f i) 0 = 0

Tactic:
simp

Result:
no goals

Proof state:
ι : Type u_1
κ : Type u_2
α : Type u_3
inst✝ : OrderedAddCommMonoid α
f : ι → κ
⊢ Monotone (mapDomain f)

Tactic:
exact fun g₁ g₂ h ↦ sum_le_sum_index h (fun _ _ ↦ single_mono) (by simp)

Result:
no goals

Proof state:
ι : Type u_1
κ : Type u_2
α : Type u_3
inst✝ : OrderedAddCommMonoid α
f : ι → κ
⊢ Monotone (mapDomain f)

Tactic:
classical exact fun g₁ g₂ h ↦ sum_le_sum_index h (fun _ _ ↦ single_mono) (by simp)

Result:
no goals
-- Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean
@[simp] lemma MemLp.zero : MemLp (0 : α → E) p μ :=
  ⟨aestronglyMeasurable_zero, by rw [eLpNorm_zero]; exact ENNReal.coe_lt_top⟩

Proof state:
α : Type u_1
E : Type u_3
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
⊢ 0 < ⊤

Tactic:
exact ENNReal.coe_lt_top

Result:
no goals

Proof state:
α : Type u_1
E : Type u_3
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
⊢ eLpNorm 0 p μ < ⊤

Tactic:
rw [eLpNorm_zero]

Result:
α : Type u_1
E : Type u_3
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
⊢ 0 < ⊤
-- Mathlib/Combinatorics/SimpleGraph/Path.lean
theorem IsTrail.of_append_left {u v w : V} {p : G.Walk u v} {q : G.Walk v w}
    (h : (p.append q).IsTrail) : p.IsTrail

Proof state:
V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk u v
q : G.Walk v w
h : p.edges.Nodup ∧ q.edges.Nodup ∧ p.edges.Disjoint q.edges
⊢ p.IsTrail

Tactic:
exact ⟨h.1⟩

Result:
no goals

Proof state:
V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk u v
q : G.Walk v w
h : (p.append q).IsTrail
⊢ p.IsTrail

Tactic:
rw [isTrail_def, edges_append, List.nodup_append] at h

Result:
V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk u v
q : G.Walk v w
h : p.edges.Nodup ∧ q.edges.Nodup ∧ p.edges.Disjoint q.edges
⊢ p.IsTrail
-- Mathlib/RingTheory/Derivation/MapCoeffs.lean
theorem deriv_aeval_eq (x : R) (p : A[X]) :
    (aeval x p)′ = aeval x (mapCoeffs p) + aeval x (derivative p) * x′

Proof state:
case h.e'_3.h.e'_5
A : Type u_1
inst✝⁵ : CommRing A
inst✝⁴ : Differential A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Differential R
inst✝¹ : Algebra A R
inst✝ : DifferentialAlgebra A R
x : R
p : A[X]
⊢ (aeval x) (mapCoeffs p) =
    (PolynomialModule.eval x) ((PolynomialModule.map R (Algebra.linearMap A R)) (deriv.mapCoeffs p))

Tactic:
simp [mapCoeffs]

Result:
no goals

Proof state:
case convert_7
A : Type u_1
inst✝⁵ : CommRing A
inst✝⁴ : Differential A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Differential R
inst✝¹ : Algebra A R
inst✝ : DifferentialAlgebra A R
x : R
p : A[X]
⊢ ∀ (a : A), (Algebra.linearMap A R) a′ = ((algebraMap A R) a)′

Tactic:
simp [deriv_algebraMap]

Result:
no goals

Proof state:
A : Type u_1
inst✝⁵ : CommRing A
inst✝⁴ : Differential A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Differential R
inst✝¹ : Algebra A R
inst✝ : DifferentialAlgebra A R
x : R
p : A[X]
⊢ ((aeval x) p)′ = (aeval x) (mapCoeffs p) + (aeval x) (derivative p) * x′

Tactic:
convert Derivation.apply_aeval_eq' Differential.deriv _ (Algebra.linearMap A R) ..

Result:
case h.e'_3.h.e'_5
A : Type u_1
inst✝⁵ : CommRing A
inst✝⁴ : Differential A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Differential R
inst✝¹ : Algebra A R
inst✝ : DifferentialAlgebra A R
x : R
p : A[X]
⊢ (aeval x) (mapCoeffs p) =
    (PolynomialModule.eval x) ((PolynomialModule.map R (Algebra.linearMap A R)) (deriv.mapCoeffs p))

case convert_7
A : Type u_1
inst✝⁵ : CommRing A
inst✝⁴ : Differential A
R : Type u_2
inst✝³ : CommRing R
inst✝² : Differential R
inst✝¹ : Algebra A R
inst✝ : DifferentialAlgebra A R
x : R
p : A[X]
⊢ ∀ (a : A), (Algebra.linearMap A R) a′ = ((algebraMap A R) a)′
-- Mathlib/Analysis/Calculus/UniformLimitsDeriv.lean
theorem hasFDerivAt_of_tendsto_locally_uniformly_on' [NeBot l] {s : Set E} (hs : IsOpen s)
    (hf' : TendstoLocallyUniformlyOn (fderiv 𝕜 ∘ f) g' l s) (hf : ∀ n, DifferentiableOn 𝕜 (f n) s)
    (hfg : ∀ x ∈ s, Tendsto (fun n => f n x) l (𝓝 (g x))) (hx : x ∈ s) :
    HasFDerivAt g (g' x) x

Proof state:
ι : Type u_1
l : Filter ι
E : Type u_2
inst✝⁶ : NormedAddCommGroup E
𝕜 : Type u_3
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : IsRCLikeNormedField 𝕜
inst✝³ : NormedSpace 𝕜 E
G : Type u_4
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
f : ι → E → G
g : E → G
g' : E → E →L[𝕜] G
x : E
inst✝ : l.NeBot
s : Set E
hs : IsOpen s
hf' : TendstoLocallyUniformlyOn (fderiv 𝕜 ∘ f) g' l s
hf : ∀ (n : ι), DifferentiableOn 𝕜 (f n) s
hfg : ∀ x ∈ s, Tendsto (fun n => f n x) l (𝓝 (g x))
hx : x ∈ s
n : ι
z : E
hz : z ∈ s
⊢ HasFDerivAt (f n) ((fderiv 𝕜 ∘ f) n z) z

Tactic:
exact ((hf n z hz).differentiableAt (hs.mem_nhds hz)).hasFDerivAt

Result:
no goals

Proof state:
ι : Type u_1
l : Filter ι
E : Type u_2
inst✝⁶ : NormedAddCommGroup E
𝕜 : Type u_3
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : IsRCLikeNormedField 𝕜
inst✝³ : NormedSpace 𝕜 E
G : Type u_4
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
f : ι → E → G
g : E → G
g' : E → E →L[𝕜] G
x : E
inst✝ : l.NeBot
s : Set E
hs : IsOpen s
hf' : TendstoLocallyUniformlyOn (fderiv 𝕜 ∘ f) g' l s
hf : ∀ (n : ι), DifferentiableOn 𝕜 (f n) s
hfg : ∀ x ∈ s, Tendsto (fun n => f n x) l (𝓝 (g x))
hx : x ∈ s
⊢ HasFDerivAt g (g' x) x

Tactic:
refine hasFDerivAt_of_tendstoLocallyUniformlyOn hs hf' (fun n z hz => ?_) hfg hx

Result:
ι : Type u_1
l : Filter ι
E : Type u_2
inst✝⁶ : NormedAddCommGroup E
𝕜 : Type u_3
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : IsRCLikeNormedField 𝕜
inst✝³ : NormedSpace 𝕜 E
G : Type u_4
inst✝² : NormedAddCommGroup G
inst✝¹ : NormedSpace 𝕜 G
f : ι → E → G
g : E → G
g' : E → E →L[𝕜] G
x : E
inst✝ : l.NeBot
s : Set E
hs : IsOpen s
hf' : TendstoLocallyUniformlyOn (fderiv 𝕜 ∘ f) g' l s
hf : ∀ (n : ι), DifferentiableOn 𝕜 (f n) s
hfg : ∀ x ∈ s, Tendsto (fun n => f n x) l (𝓝 (g x))
hx : x ∈ s
n : ι
z : E
hz : z ∈ s
⊢ HasFDerivAt (f n) ((fderiv 𝕜 ∘ f) n z) z
-- Mathlib/SetTheory/Cardinal/Basic.lean
theorem sum_add_distrib {ι} (f g : ι → Cardinal) : sum (f + g) = sum f + sum g

Proof state:
ι : Type u_1
f g : ι → Cardinal.{u_2}
this :
  #((i : ι) × ((Quotient.out ∘ f) i ⊕ (Quotient.out ∘ g) i)) =
    #((i : ι) × (Quotient.out ∘ f) i ⊕ (i : ι) × (Quotient.out ∘ g) i)
⊢ sum (f + g) = sum f + sum g

Tactic:
simp only [comp_apply, mk_sigma, mk_sum, mk_out, lift_id] at this

Result:
ι : Type u_1
f g : ι → Cardinal.{u_2}
this : (sum fun i => f i + g i) = (sum fun i => f i) + sum fun i => g i
⊢ sum (f + g) = sum f + sum g

Proof state:
ι : Type u_1
f g : ι → Cardinal.{u_2}
⊢ sum (f + g) = sum f + sum g

Tactic:
have := mk_congr (Equiv.sigmaSumDistrib (Quotient.out ∘ f) (Quotient.out ∘ g))

Result:
ι : Type u_1
f g : ι → Cardinal.{u_2}
this :
  #((i : ι) × ((Quotient.out ∘ f) i ⊕ (Quotient.out ∘ g) i)) =
    #((i : ι) × (Quotient.out ∘ f) i ⊕ (i : ι) × (Quotient.out ∘ g) i)
⊢ sum (f + g) = sum f + sum g

Proof state:
ι : Type u_1
f g : ι → Cardinal.{u_2}
this : (sum fun i => f i + g i) = (sum fun i => f i) + sum fun i => g i
⊢ sum (f + g) = sum f + sum g

Tactic:
exact this

Result:
no goals
-- Mathlib/MeasureTheory/MeasurableSpace/CountablyGenerated.lean
lemma generateFrom_iUnion_countablePartition (α : Type*) [m : MeasurableSpace α]
    [CountablyGenerated α] :
    generateFrom (⋃ n, countablePartition α n) = m

Proof state:
α : Type u_3
m : MeasurableSpace α
inst✝ : CountablyGenerated α
⊢ generateFrom (⋃ n, countablePartition α n) = m

Tactic:
rw [countablePartition, generateFrom_iUnion_memPartition,
  range_enumerateCountable_of_mem _ empty_mem_countableGeneratingSet,
  generateFrom_countableGeneratingSet]

Result:
no goals
-- Mathlib/Topology/Category/Profinite/Nobeling.lean
theorem contained_proj (o : Ordinal) : contained (π C (ord I · < o)) o

Proof state:
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
x w✝ : I → Bool
left✝ : w✝ ∈ C
h : Proj (fun x => ord I x < o) w✝ = x
j : I
hj : x j = true
⊢ ord I j < o

Tactic:
aesop (add simp Proj)

Result:
no goals

Proof state:
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
⊢ contained (π C fun x => ord I x < o) o

Tactic:
intro x ⟨_, _, h⟩ j hj

Result:
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
x w✝ : I → Bool
left✝ : w✝ ∈ C
h : Proj (fun x => ord I x < o) w✝ = x
j : I
hj : x j = true
⊢ ord I j < o
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Lemmas.lean
theorem two_pow_pred_mod_two_pow (h : 0 < w) :
    2 ^ (w - 1) % 2 ^ w = 2 ^ (w - 1)

Proof state:
w : Nat
h : 0 < w
⊢ 1 < 2

Tactic:
omega

Result:
no goals

Proof state:
w : Nat
h : 0 < w
⊢ 2 ^ (w - 1) < 2 ^ w

Tactic:
apply Nat.pow_pred_lt_pow (by omega) h

Result:
no goals

Proof state:
w : Nat
h : 0 < w
⊢ 2 ^ (w - 1) % 2 ^ w = 2 ^ (w - 1)

Tactic:
rw [mod_eq_of_lt]

Result:
w : Nat
h : 0 < w
⊢ 2 ^ (w - 1) < 2 ^ w
-- Mathlib/Analysis/Complex/UpperHalfPlane/Metric.lean
theorem dist_le_iff_le_sinh :
    dist z w ≤ r ↔ dist (z : ℂ) w / (2 * √(z.im * w.im)) ≤ sinh (r / 2)

Proof state:
z w : ℍ
r : ℝ
⊢ dist z w ≤ r ↔ dist ↑z ↑w / (2 * √(z.im * w.im)) ≤ sinh (r / 2)

Tactic:
rw [← div_le_div_iff_of_pos_right (zero_lt_two' ℝ), ← sinh_le_sinh, sinh_half_dist]

Result:
no goals
-- Mathlib/Algebra/GeomSum.lean
theorem geom_sum_alternating_of_lt_neg_one [StrictOrderedRing α] (hx : x + 1 < 0) (hn : 1 < n) :
    if Even n then (∑ i ∈ range n, x ^ i) < 0 else 1 < ∑ i ∈ range n, x ^ i

Proof state:
case neg
α : Type u
n✝ : ℕ
x : α
inst✝ : StrictOrderedRing α
hx : x + 1 < 0
hx0 : x < 0
n : ℕ
hmn✝ : 2 ≤ n
ihn : 1 < ∑ i ∈ range n, x ^ i
hn' : ¬Even n
this : x * ∑ i ∈ range n, x ^ i + 1 < x * 1 + 1
⊢ x * ∑ i ∈ range n, x ^ i + 1 < 0

Tactic:
rw [mul_one] at this

Result:
case neg
α : Type u
n✝ : ℕ
x : α
inst✝ : StrictOrderedRing α
hx : x + 1 < 0
hx0 : x < 0
n : ℕ
hmn✝ : 2 ≤ n
ihn : 1 < ∑ i ∈ range n, x ^ i
hn' : ¬Even n
this : x * ∑ i ∈ range n, x ^ i + 1 < x + 1
⊢ x * ∑ i ∈ range n, x ^ i + 1 < 0

Proof state:
case neg
α : Type u
n✝ : ℕ
x : α
inst✝ : StrictOrderedRing α
hx : x + 1 < 0
hx0 : x < 0
n : ℕ
hmn✝ : 2 ≤ n
ihn : 1 < ∑ i ∈ range n, x ^ i
hn' : ¬Even n
⊢ x * ∑ i ∈ range n, x ^ i + 1 < 0

Tactic:
have := add_lt_add_right (mul_lt_mul_of_neg_left ihn hx0) 1

Result:
case neg
α : Type u
n✝ : ℕ
x : α
inst✝ : StrictOrderedRing α
hx : x + 1 < 0
hx0 : x < 0
n : ℕ
hmn✝ : 2 ≤ n
ihn : 1 < ∑ i ∈ range n, x ^ i
hn' : ¬Even n
this : x * ∑ i ∈ range n, x ^ i + 1 < x * 1 + 1
⊢ x * ∑ i ∈ range n, x ^ i + 1 < 0

Proof state:
case pos.hnc
α : Type u
n✝ : ℕ
x : α
inst✝ : StrictOrderedRing α
hx : x + 1 < 0
hx0 : x < 0
n : ℕ
hmn✝ : 2 ≤ n
ihn : ∑ i ∈ range n, x ^ i < 0
hn' : Even n
⊢ ¬¬Even n

Tactic:
exact not_not_intro hn'

Result:
no goals

Proof state:
case neg
α : Type u
n✝ : ℕ
x : α
inst✝ : StrictOrderedRing α
hx : x + 1 < 0
hx0 : x < 0
n : ℕ
hmn✝ : 2 ≤ n
ihn : 1 < ∑ i ∈ range n, x ^ i
hn' : ¬Even n
⊢ x * ∑ i ∈ range n, x ^ i + 1 < 0

case neg.hc
α : Type u
n✝ : ℕ
x : α
inst✝ : StrictOrderedRing α
hx : x + 1 < 0
hx0 : x < 0
n : ℕ
hmn✝ : 2 ≤ n
ihn : 1 < ∑ i ∈ range n, x ^ i
hn' : ¬Even n
⊢ ¬Even n

Tactic:
swap

Result:
case neg.hc
α : Type u
n✝ : ℕ
x : α
inst✝ : StrictOrderedRing α
hx : x + 1 < 0
hx0 : x < 0
n : ℕ
hmn✝ : 2 ≤ n
ihn : 1 < ∑ i ∈ range n, x ^ i
hn' : ¬Even n
⊢ ¬Even n

case neg
α : Type u
n✝ : ℕ
x : α
inst✝ : StrictOrderedRing α
hx : x + 1 < 0
hx0 : x < 0
n : ℕ
hmn✝ : 2 ≤ n
ihn : 1 < ∑ i ∈ range n, x ^ i
hn' : ¬Even n
⊢ x * ∑ i ∈ range n, x ^ i + 1 < 0
-- Mathlib/Probability/Moments/IntegrableExpMul.lean
lemma rpow_abs_le_mul_exp_abs (x : ℝ) {t p : ℝ} (hp : 0 ≤ p) (ht : t ≠ 0) :
    |x| ^ p ≤ (p / |t|) ^ p * exp (|t| * |x|)

Proof state:
case refine_2
x t p : ℝ
hp : 0 ≤ p
ht : t ≠ 0
⊢ (p / |t|) ^ p * (rexp (|t| * x) ⊔ rexp (-|t| * x)) = (p / |t|) ^ p * rexp (|t| * |x|)

Tactic:
congr

Result:
case refine_2.e_a
x t p : ℝ
hp : 0 ≤ p
ht : t ≠ 0
⊢ rexp (|t| * x) ⊔ rexp (-|t| * x) = rexp (|t| * |x|)

Proof state:
case refine_2.e_a.inl
x t p : ℝ
hp : 0 ≤ p
ht : t ≠ 0
hx : 0 ≤ x
⊢ 0 ≤ |t| * x

Tactic:
positivity

Result:
no goals

Proof state:
case refine_2.e_a.inl
x t p : ℝ
hp : 0 ≤ p
ht : t ≠ 0
hx : 0 ≤ x
⊢ rexp (|t| * x) ⊔ rexp (-|t| * x) = rexp (|t| * x)

Tactic:
simp only [neg_mul, sup_eq_left, exp_le_exp, neg_le_self_iff]

Result:
case refine_2.e_a.inl
x t p : ℝ
hp : 0 ≤ p
ht : t ≠ 0
hx : 0 ≤ x
⊢ 0 ≤ |t| * x

Proof state:
x t p : ℝ
hp : 0 ≤ p
ht : t ≠ 0
⊢ |x| ^ p ≤ (p / |t|) ^ p * rexp (|t| * |x|)

Tactic:
refine (rpow_abs_le_mul_max_exp_of_pos x hp (t := |t|) ?_).trans_eq ?_

Result:
case refine_1
x t p : ℝ
hp : 0 ≤ p
ht : t ≠ 0
⊢ 0 < |t|

case refine_2
x t p : ℝ
hp : 0 ≤ p
ht : t ≠ 0
⊢ (p / |t|) ^ p * (rexp (|t| * x) ⊔ rexp (-|t| * x)) = (p / |t|) ^ p * rexp (|t| * |x|)

Proof state:
case refine_2.e_a.inr
x t p : ℝ
hp : 0 ≤ p
ht : t ≠ 0
hx : x ≤ 0
⊢ rexp (|t| * x) ⊔ rexp (-|t| * x) = rexp (|t| * -x)

Tactic:
simp only [neg_mul, mul_neg, sup_eq_right, exp_le_exp, le_neg_self_iff]

Result:
case refine_2.e_a.inr
x t p : ℝ
hp : 0 ≤ p
ht : t ≠ 0
hx : x ≤ 0
⊢ |t| * x ≤ 0

Proof state:
case refine_2.e_a.inl
x t p : ℝ
hp : 0 ≤ p
ht : t ≠ 0
hx : 0 ≤ x
⊢ rexp (|t| * x) ⊔ rexp (-|t| * x) = rexp (|t| * |x|)

Tactic:
rw [abs_of_nonneg hx]

Result:
case refine_2.e_a.inl
x t p : ℝ
hp : 0 ≤ p
ht : t ≠ 0
hx : 0 ≤ x
⊢ rexp (|t| * x) ⊔ rexp (-|t| * x) = rexp (|t| * x)

Proof state:
case refine_2.e_a.inr
x t p : ℝ
hp : 0 ≤ p
ht : t ≠ 0
hx : x ≤ 0
⊢ |t| * x ≤ 0

Tactic:
exact mul_nonpos_of_nonneg_of_nonpos (abs_nonneg _) hx

Result:
no goals

Proof state:
case refine_2.e_a.inr
x t p : ℝ
hp : 0 ≤ p
ht : t ≠ 0
hx : x ≤ 0
⊢ rexp (|t| * x) ⊔ rexp (-|t| * x) = rexp (|t| * |x|)

Tactic:
rw [abs_of_nonpos hx]

Result:
case refine_2.e_a.inr
x t p : ℝ
hp : 0 ≤ p
ht : t ≠ 0
hx : x ≤ 0
⊢ rexp (|t| * x) ⊔ rexp (-|t| * x) = rexp (|t| * -x)

Proof state:
case refine_1
x t p : ℝ
hp : 0 ≤ p
ht : t ≠ 0
⊢ 0 < |t|

Tactic:
simp [ht]

Result:
no goals

Proof state:
case refine_2.e_a
x t p : ℝ
hp : 0 ≤ p
ht : t ≠ 0
⊢ rexp (|t| * x) ⊔ rexp (-|t| * x) = rexp (|t| * |x|)

Tactic:
rcases le_total 0 x with hx | hx

Result:
case refine_2.e_a.inl
x t p : ℝ
hp : 0 ≤ p
ht : t ≠ 0
hx : 0 ≤ x
⊢ rexp (|t| * x) ⊔ rexp (-|t| * x) = rexp (|t| * |x|)

case refine_2.e_a.inr
x t p : ℝ
hp : 0 ≤ p
ht : t ≠ 0
hx : x ≤ 0
⊢ rexp (|t| * x) ⊔ rexp (-|t| * x) = rexp (|t| * |x|)
-- Mathlib/FieldTheory/Finite/GaloisField.lean
theorem splits_zmod_X_pow_sub_X : Splits (RingHom.id (ZMod p)) (X ^ p - X)

Proof state:
p : ℕ
h_prime : Fact (Nat.Prime p)
hp : 1 < p
⊢ (X ^ p - X).roots = univ.val

Tactic:
convert FiniteField.roots_X_pow_card_sub_X (ZMod p)

Result:
case h.e'_2.h.e'_4.h.h.e'_5.h.e'_6
p : ℕ
h_prime : Fact (Nat.Prime p)
hp : 1 < p
e_2✝ : ZMod.commRing p = EuclideanDomain.toCommRing
⊢ p = Fintype.card (ZMod p)

Proof state:
p : ℕ
h_prime : Fact (Nat.Prime p)
⊢ Splits (RingHom.id (ZMod p)) (X ^ p - X)

Tactic:
have hp : 1 < p := h_prime.out.one_lt

Result:
p : ℕ
h_prime : Fact (Nat.Prime p)
hp : 1 < p
⊢ Splits (RingHom.id (ZMod p)) (X ^ p - X)

Proof state:
case succ
n✝ : ℕ
h_prime : Fact (Nat.Prime (n✝ + 1))
hp : 1 < n✝ + 1
h1 : (X ^ (n✝ + 1) - X).roots = univ.val
h2 : (X ^ (n✝ + 1) - X).natDegree = n✝ + 1
⊢ Splits (RingHom.id (ZMod (n✝ + 1))) (X ^ (n✝ + 1) - X)

Tactic:
rw [splits_iff_card_roots, h1, ← Finset.card_def, Finset.card_univ, h2, ZMod.card]

Result:
no goals

Proof state:
p : ℕ
h_prime : Fact (Nat.Prime p)
hp : 1 < p
⊢ Splits (RingHom.id (ZMod p)) (X ^ p - X)

Tactic:
have h1 : roots (X ^ p - X : (ZMod p)[X]) = Finset.univ.val := by
  convert FiniteField.roots_X_pow_card_sub_X (ZMod p)
  exact (ZMod.card p).symm

Result:
p : ℕ
h_prime : Fact (Nat.Prime p)
hp : 1 < p
h1 : (X ^ p - X).roots = univ.val
⊢ Splits (RingHom.id (ZMod p)) (X ^ p - X)

Proof state:
p : ℕ
h_prime : Fact (Nat.Prime p)
hp : 1 < p
h1 : (X ^ p - X).roots = univ.val
⊢ Splits (RingHom.id (ZMod p)) (X ^ p - X)

Tactic:
have h2 := FiniteField.X_pow_card_sub_X_natDegree_eq (ZMod p) hp

Result:
p : ℕ
h_prime : Fact (Nat.Prime p)
hp : 1 < p
h1 : (X ^ p - X).roots = univ.val
h2 : (X ^ p - X).natDegree = p
⊢ Splits (RingHom.id (ZMod p)) (X ^ p - X)

Proof state:
case zero
h_prime : Fact (Nat.Prime 0)
hp : 1 < 0
h1 : (X ^ 0 - X).roots = univ.val
h2 : (X ^ 0 - X).natDegree = 0
⊢ Splits (RingHom.id (ZMod 0)) (X ^ 0 - X)

case succ
n✝ : ℕ
h_prime : Fact (Nat.Prime (n✝ + 1))
hp : 1 < n✝ + 1
h1 : (X ^ (n✝ + 1) - X).roots = univ.val
h2 : (X ^ (n✝ + 1) - X).natDegree = n✝ + 1
⊢ Splits (RingHom.id (ZMod (n✝ + 1))) (X ^ (n✝ + 1) - X)

Tactic:
cases hp

Result:
case succ
n✝ : ℕ
h_prime : Fact (Nat.Prime (n✝ + 1))
hp : 1 < n✝ + 1
h1 : (X ^ (n✝ + 1) - X).roots = univ.val
h2 : (X ^ (n✝ + 1) - X).natDegree = n✝ + 1
⊢ Splits (RingHom.id (ZMod (n✝ + 1))) (X ^ (n✝ + 1) - X)

Proof state:
case h.e'_2.h.e'_4.h.h.e'_5.h.e'_6
p : ℕ
h_prime : Fact (Nat.Prime p)
hp : 1 < p
e_2✝ : ZMod.commRing p = EuclideanDomain.toCommRing
⊢ p = Fintype.card (ZMod p)

Tactic:
exact (ZMod.card p).symm

Result:
no goals

Proof state:
p : ℕ
h_prime : Fact (Nat.Prime p)
hp : 1 < p
h1 : (X ^ p - X).roots = univ.val
h2 : (X ^ p - X).natDegree = p
⊢ Splits (RingHom.id (ZMod p)) (X ^ p - X)

Tactic:
cases p

Result:
case zero
h_prime : Fact (Nat.Prime 0)
hp : 1 < 0
h1 : (X ^ 0 - X).roots = univ.val
h2 : (X ^ 0 - X).natDegree = 0
⊢ Splits (RingHom.id (ZMod 0)) (X ^ 0 - X)

case succ
n✝ : ℕ
h_prime : Fact (Nat.Prime (n✝ + 1))
hp : 1 < n✝ + 1
h1 : (X ^ (n✝ + 1) - X).roots = univ.val
h2 : (X ^ (n✝ + 1) - X).natDegree = n✝ + 1
⊢ Splits (RingHom.id (ZMod (n✝ + 1))) (X ^ (n✝ + 1) - X)
-- Mathlib/RingTheory/Localization/FractionRing.lean
theorem mk'_eq_zero_iff_eq_zero [Algebra R K] [IsFractionRing R K] {x : R} {y : nonZeroDivisors R} :
    mk' K x y = 0 ↔ x = 0

Proof state:
R : Type u_1
inst✝³ : CommRing R
K : Type u_5
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
x : R
y : ↥(nonZeroDivisors R)
⊢ mk' K x y = 0 ↔ x = 0

Tactic:
haveI := (algebraMap R K).domain_nontrivial

Result:
R : Type u_1
inst✝³ : CommRing R
K : Type u_5
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
x : R
y : ↥(nonZeroDivisors R)
this : Nontrivial R
⊢ mk' K x y = 0 ↔ x = 0

Proof state:
R : Type u_1
inst✝³ : CommRing R
K : Type u_5
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
x : R
y : ↥(nonZeroDivisors R)
this : Nontrivial R
⊢ mk' K x y = 0 ↔ x = 0

Tactic:
simp [nonZeroDivisors.ne_zero]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Regular.lean
/-- See also `IsCompact.measure_closure` for a version
that assumes the `σ`-algebra to be the Borel `σ`-algebra but makes no assumptions on `μ`. -/
lemma measure_closure_eq_of_isCompact [R1Space α] [OuterRegular μ]
    {k : Set α} (hk : IsCompact k) : μ (closure k) = μ k

Proof state:
α : Type u_1
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : TopologicalSpace α
inst✝¹ : R1Space α
inst✝ : μ.OuterRegular
k : Set α
hk : IsCompact k
u : Set α
ku : k ⊆ u
u_open : IsOpen u
⊢ μ (closure k) ≤ μ u

Tactic:
exact measure_mono (hk.closure_subset_of_isOpen u_open ku)

Result:
no goals

Proof state:
α : Type u_1
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : TopologicalSpace α
inst✝¹ : R1Space α
inst✝ : μ.OuterRegular
k : Set α
hk : IsCompact k
⊢ μ (closure k) ≤ μ k

Tactic:
simp only [measure_eq_iInf_isOpen k, le_iInf_iff]

Result:
α : Type u_1
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : TopologicalSpace α
inst✝¹ : R1Space α
inst✝ : μ.OuterRegular
k : Set α
hk : IsCompact k
⊢ ∀ (i : Set α), k ⊆ i → IsOpen i → μ (closure k) ≤ μ i

Proof state:
α : Type u_1
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : TopologicalSpace α
inst✝¹ : R1Space α
inst✝ : μ.OuterRegular
k : Set α
hk : IsCompact k
⊢ ∀ (i : Set α), k ⊆ i → IsOpen i → μ (closure k) ≤ μ i

Tactic:
intro u ku u_open

Result:
α : Type u_1
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : TopologicalSpace α
inst✝¹ : R1Space α
inst✝ : μ.OuterRegular
k : Set α
hk : IsCompact k
u : Set α
ku : k ⊆ u
u_open : IsOpen u
⊢ μ (closure k) ≤ μ u

Proof state:
α : Type u_1
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : TopologicalSpace α
inst✝¹ : R1Space α
inst✝ : μ.OuterRegular
k : Set α
hk : IsCompact k
⊢ μ (closure k) = μ k

Tactic:
apply le_antisymm ?_ (measure_mono subset_closure)

Result:
α : Type u_1
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : TopologicalSpace α
inst✝¹ : R1Space α
inst✝ : μ.OuterRegular
k : Set α
hk : IsCompact k
⊢ μ (closure k) ≤ μ k
-- Mathlib/MeasureTheory/Function/L1Space/HasFiniteIntegral.lean
theorem hasFiniteIntegral_iff_ofNNReal {f : α → ℝ≥0} :
    HasFiniteIntegral (fun x => (f x : ℝ)) μ ↔ (∫⁻ a, f a ∂μ) < ∞

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0
⊢ HasFiniteIntegral (fun x => ↑(f x)) μ ↔ ∫⁻ (a : α), ↑(f a) ∂μ < ⊤

Tactic:
simp [hasFiniteIntegral_iff_norm]

Result:
no goals