harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Topology/MetricSpace/Thickening.lean
theorem closure_eq_iInter_thickening' (E : Set α) (s : Set ℝ) (hs₀ : s ⊆ Ioi 0)
    (hs : ∀ ε, 0 < ε → (s ∩ Ioc 0 ε).Nonempty) : closure E = ⋂ δ ∈ s, thickening δ E

Proof state:
α : Type u
inst✝ : PseudoEMetricSpace α
E : Set α
s : Set ℝ
hs₀ : s ⊆ Ioi 0
hs : ∀ (ε : ℝ), 0 < ε → (s ∩ Ioc 0 ε).Nonempty
⊢ cthickening 0 E = ⋂ δ ∈ s, thickening δ E

Tactic:
apply cthickening_eq_iInter_thickening' le_rfl _ hs₀ hs

Result:
no goals

Proof state:
α : Type u
inst✝ : PseudoEMetricSpace α
E : Set α
s : Set ℝ
hs₀ : s ⊆ Ioi 0
hs : ∀ (ε : ℝ), 0 < ε → (s ∩ Ioc 0 ε).Nonempty
⊢ closure E = ⋂ δ ∈ s, thickening δ E

Tactic:
rw [← cthickening_zero]

Result:
α : Type u
inst✝ : PseudoEMetricSpace α
E : Set α
s : Set ℝ
hs₀ : s ⊆ Ioi 0
hs : ∀ (ε : ℝ), 0 < ε → (s ∩ Ioc 0 ε).Nonempty
⊢ cthickening 0 E = ⋂ δ ∈ s, thickening δ E
-- Mathlib/GroupTheory/QuotientGroup/Basic.lean
theorem le_comap_mk' (N : Subgroup G) [N.Normal] (H : Subgroup (G ⧸ N)) :
    N ≤ Subgroup.comap (QuotientGroup.mk' N) H

Proof state:
G : Type u
inst✝¹ : Group G
N : Subgroup G
inst✝ : N.Normal
H : Subgroup (G ⧸ N)
⊢ N ≤ Subgroup.comap (mk' N) H

Tactic:
simpa using Subgroup.comap_mono (f := mk' N) bot_le

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem filter_flatMap (l : List α) (g : α → List β) (f : β → Bool) :
    (l.flatMap g).filter f = l.flatMap fun a => (g a).filter f

Proof state:
α : Type u_1
β : Type u_2
l : List α
g : α → List β
f : β → Bool
⊢ filter f (flatMap g l) = flatMap (fun a => filter f (g a)) l

Tactic:
induction l <;> simp [*]

Result:
no goals
-- Mathlib/RingTheory/TensorProduct/Basic.lean
theorem lmul''_eq_lid_comp_mapOfCompatibleSMul :
    lmul'' R = (TensorProduct.lid S S).toAlgHom.comp (mapOfCompatibleSMul' _ _ _ _)

Proof state:
R : Type uR
S : Type uS
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
⊢ lmul'' R = (↑(TensorProduct.lid S S)).comp (mapOfCompatibleSMul' S R S S)

Tactic:
ext

Result:
case hb.H
R : Type uR
S : Type uS
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
x✝ : S
⊢ ((AlgHom.restrictScalars R (lmul'' R)).comp includeRight) x✝ =
    ((AlgHom.restrictScalars R ((↑(TensorProduct.lid S S)).comp (mapOfCompatibleSMul' S R S S))).comp includeRight) x✝

Proof state:
case hb.H
R : Type uR
S : Type uS
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
inst✝ : Algebra R S
x✝ : S
⊢ ((AlgHom.restrictScalars R (lmul'' R)).comp includeRight) x✝ =
    ((AlgHom.restrictScalars R ((↑(TensorProduct.lid S S)).comp (mapOfCompatibleSMul' S R S S))).comp includeRight) x✝

Tactic:
rfl

Result:
no goals
-- Mathlib/RingTheory/Polynomial/Quotient.lean
lemma modByMonic_eq_zero_iff_quotient_eq_zero (p q : R[X]) (hq : q.Monic) :
    p %ₘ q = 0 ↔ (p : R[X] ⧸ Ideal.span {q}) = 0

Proof state:
R : Type u_1
inst✝ : CommRing R
p q : R[X]
hq : q.Monic
⊢ p %ₘ q = 0 ↔ (Ideal.Quotient.mk (Ideal.span {q})) p = 0

Tactic:
rw [modByMonic_eq_zero_iff_dvd hq, Ideal.Quotient.eq_zero_iff_dvd]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/IntegrableOn.lean
theorem integrableOn_finite_iUnion [Finite β] {t : β → Set α} :
    IntegrableOn f (⋃ i, t i) μ ↔ ∀ i, IntegrableOn f (t i) μ

Proof state:
α : Type u_1
β : Type u_2
E : Type u_4
inst✝² : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
f : α → E
μ : Measure α
inst✝ : Finite β
t : β → Set α
⊢ IntegrableOn f (⋃ i, t i) μ ↔ ∀ (i : β), IntegrableOn f (t i) μ

Tactic:
cases nonempty_fintype β

Result:
case intro
α : Type u_1
β : Type u_2
E : Type u_4
inst✝² : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
f : α → E
μ : Measure α
inst✝ : Finite β
t : β → Set α
val✝ : Fintype β
⊢ IntegrableOn f (⋃ i, t i) μ ↔ ∀ (i : β), IntegrableOn f (t i) μ

Proof state:
case intro
α : Type u_1
β : Type u_2
E : Type u_4
inst✝² : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
f : α → E
μ : Measure α
inst✝ : Finite β
t : β → Set α
val✝ : Fintype β
⊢ IntegrableOn f (⋃ i, t i) μ ↔ ∀ (i : β), IntegrableOn f (t i) μ

Tactic:
simpa using @integrableOn_finset_iUnion _ _ _ _ _ f μ Finset.univ t

Result:
no goals
-- Mathlib/Geometry/Euclidean/Angle/Oriented/RightAngle.lean
theorem tan_oangle_sub_right_of_oangle_eq_pi_div_two {x y : V} (h : o.oangle x y = ↑(π / 2)) :
    Real.Angle.tan (o.oangle y (y - x)) = ‖x‖ / ‖y‖

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : o.oangle x y = ↑(π / 2)
⊢ (o.oangle y (y - x)).tan = ‖x‖ / ‖y‖

Tactic:
have hs : (o.oangle y (y - x)).sign = 1 := by
  rw [oangle_sign_sub_right_swap, h, Real.Angle.sign_coe_pi_div_two]

Result:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : o.oangle x y = ↑(π / 2)
hs : (o.oangle y (y - x)).sign = 1
⊢ (o.oangle y (y - x)).tan = ‖x‖ / ‖y‖

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : o.oangle x y = ↑(π / 2)
⊢ (o.oangle y (y - x)).sign = 1

Tactic:
rw [oangle_sign_sub_right_swap, h, Real.Angle.sign_coe_pi_div_two]

Result:
no goals

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
hd2 : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
h : o.oangle x y = ↑(π / 2)
hs : (o.oangle y (y - x)).sign = 1
⊢ (o.oangle y (y - x)).tan = ‖x‖ / ‖y‖

Tactic:
rw [o.oangle_eq_angle_of_sign_eq_one hs, Real.Angle.tan_coe,
  InnerProductGeometry.tan_angle_sub_of_inner_eq_zero
    (o.inner_rev_eq_zero_of_oangle_eq_pi_div_two h)]

Result:
no goals
-- Mathlib/MeasureTheory/Function/AEEqFun.lean
theorem inf_le_left (f g : α →ₘ[μ] β) : f ⊓ g ≤ f

Proof state:
α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : TopologicalSpace β
inst✝¹ : SemilatticeInf β
inst✝ : ContinuousInf β
f g : α →ₘ[μ] β
⊢ ↑(f ⊓ g) ≤ᶠ[ae μ] ↑f

Tactic:
filter_upwards [coeFn_inf f g] with _ ha

Result:
case h
α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : TopologicalSpace β
inst✝¹ : SemilatticeInf β
inst✝ : ContinuousInf β
f g : α →ₘ[μ] β
a✝ : α
ha : ↑(f ⊓ g) a✝ = ↑f a✝ ⊓ ↑g a✝
⊢ ↑(f ⊓ g) a✝ ≤ ↑f a✝

Proof state:
case h
α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : TopologicalSpace β
inst✝¹ : SemilatticeInf β
inst✝ : ContinuousInf β
f g : α →ₘ[μ] β
a✝ : α
ha : ↑(f ⊓ g) a✝ = ↑f a✝ ⊓ ↑g a✝
⊢ ↑f a✝ ⊓ ↑g a✝ ≤ ↑f a✝

Tactic:
exact inf_le_left

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : TopologicalSpace β
inst✝¹ : SemilatticeInf β
inst✝ : ContinuousInf β
f g : α →ₘ[μ] β
⊢ f ⊓ g ≤ f

Tactic:
rw [← coeFn_le]

Result:
α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : TopologicalSpace β
inst✝¹ : SemilatticeInf β
inst✝ : ContinuousInf β
f g : α →ₘ[μ] β
⊢ ↑(f ⊓ g) ≤ᶠ[ae μ] ↑f

Proof state:
case h
α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : TopologicalSpace β
inst✝¹ : SemilatticeInf β
inst✝ : ContinuousInf β
f g : α →ₘ[μ] β
a✝ : α
ha : ↑(f ⊓ g) a✝ = ↑f a✝ ⊓ ↑g a✝
⊢ ↑(f ⊓ g) a✝ ≤ ↑f a✝

Tactic:
rw [ha]

Result:
case h
α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
μ : Measure α
inst✝² : TopologicalSpace β
inst✝¹ : SemilatticeInf β
inst✝ : ContinuousInf β
f g : α →ₘ[μ] β
a✝ : α
ha : ↑(f ⊓ g) a✝ = ↑f a✝ ⊓ ↑g a✝
⊢ ↑f a✝ ⊓ ↑g a✝ ≤ ↑f a✝
-- Mathlib/Analysis/SpecialFunctions/Pow/Real.lean
theorem rpow_sub_one {x : ℝ} (hx : x ≠ 0) (y : ℝ) : x ^ (y - 1) = x ^ y / x

Proof state:
x : ℝ
hx : x ≠ 0
y : ℝ
⊢ x ^ (y - 1) = x ^ y / x

Tactic:
simpa using rpow_sub_natCast hx y 1

Result:
no goals
-- Mathlib/Probability/Variance.lean
theorem variance_zero (μ : Measure Ω) : variance 0 μ = 0

Proof state:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
⊢ Var[0; μ] = 0

Tactic:
simp only [variance, evariance_zero, ENNReal.zero_toReal]

Result:
no goals
-- Mathlib/Topology/MetricSpace/HolderNorm.lean
@[simp] lemma eHolderNorm_lt_top : eHolderNorm r f < ∞ ↔ MemHolder r f

Proof state:
X : Type u_1
Y : Type u_2
inst✝¹ : PseudoEMetricSpace X
inst✝ : PseudoEMetricSpace Y
r : ℝ≥0
f : X → Y
⊢ eHolderNorm r f < ⊤ ↔ MemHolder r f

Tactic:
refine ⟨fun h => ?_,
  fun hf => let ⟨C, hC⟩ := hf; iInf_lt_top.2 ⟨C, iInf_lt_top.2 ⟨hC, coe_lt_top⟩⟩⟩

Result:
X : Type u_1
Y : Type u_2
inst✝¹ : PseudoEMetricSpace X
inst✝ : PseudoEMetricSpace Y
r : ℝ≥0
f : X → Y
h : eHolderNorm r f < ⊤
⊢ MemHolder r f

Proof state:
X : Type u_1
Y : Type u_2
inst✝¹ : PseudoEMetricSpace X
inst✝ : PseudoEMetricSpace Y
r : ℝ≥0
f : X → Y
h : ∃ i, ∃ (_ : HolderWith i r f), ↑i < ⊤
⊢ MemHolder r f

Tactic:
let ⟨C, hC, _⟩ := h

Result:
X : Type u_1
Y : Type u_2
inst✝¹ : PseudoEMetricSpace X
inst✝ : PseudoEMetricSpace Y
r : ℝ≥0
f : X → Y
h : ∃ i, ∃ (_ : HolderWith i r f), ↑i < ⊤
C : ℝ≥0
hC : HolderWith C r f
h✝ : ↑C < ⊤
⊢ MemHolder r f

Proof state:
X : Type u_1
Y : Type u_2
inst✝¹ : PseudoEMetricSpace X
inst✝ : PseudoEMetricSpace Y
r : ℝ≥0
f : X → Y
h : ∃ i, ∃ (_ : HolderWith i r f), ↑i < ⊤
C : ℝ≥0
hC : HolderWith C r f
h✝ : ↑C < ⊤
⊢ MemHolder r f

Tactic:
exact ⟨C, hC⟩

Result:
no goals

Proof state:
X : Type u_1
Y : Type u_2
inst✝¹ : PseudoEMetricSpace X
inst✝ : PseudoEMetricSpace Y
r : ℝ≥0
f : X → Y
h : eHolderNorm r f < ⊤
⊢ MemHolder r f

Tactic:
simp_rw [eHolderNorm, iInf_lt_top] at h

Result:
X : Type u_1
Y : Type u_2
inst✝¹ : PseudoEMetricSpace X
inst✝ : PseudoEMetricSpace Y
r : ℝ≥0
f : X → Y
h : ∃ i, ∃ (_ : HolderWith i r f), ↑i < ⊤
⊢ MemHolder r f
-- Mathlib/CategoryTheory/Bicategory/Functor/Prelax.lean
@[simp]
lemma map₂_inv {f g : a ⟶ b} (η : f ⟶ g) [IsIso η] : F.map₂ (inv η) = inv (F.map₂ η)

Proof state:
B : Type u₁
inst✝² : Bicategory B
C : Type u₂
inst✝¹ : Bicategory C
F : PrelaxFunctor B C
a b : B
f g : a ⟶ b
η : f ⟶ g
inst✝ : IsIso η
⊢ F.map₂ (inv η) = inv (F.map₂ η)

Tactic:
apply IsIso.eq_inv_of_hom_inv_id

Result:
case hom_inv_id
B : Type u₁
inst✝² : Bicategory B
C : Type u₂
inst✝¹ : Bicategory C
F : PrelaxFunctor B C
a b : B
f g : a ⟶ b
η : f ⟶ g
inst✝ : IsIso η
⊢ F.map₂ η ≫ F.map₂ (inv η) = 𝟙 (F.map f)

Proof state:
case hom_inv_id
B : Type u₁
inst✝² : Bicategory B
C : Type u₂
inst✝¹ : Bicategory C
F : PrelaxFunctor B C
a b : B
f g : a ⟶ b
η : f ⟶ g
inst✝ : IsIso η
⊢ F.map₂ η ≫ F.map₂ (inv η) = 𝟙 (F.map f)

Tactic:
simp [← F.map₂_comp η (inv η)]

Result:
no goals
-- Mathlib/Order/Interval/Set/Basic.lean
theorem Icc_union_Icc (h₁ : min a b < max c d) (h₂ : min c d < max a b) :
    Icc a b ∪ Icc c d = Icc (min a c) (max b d)

Proof state:
case inl.inr
α : Type u_1
inst✝ : LinearOrder α
a b c d : α
hab : a ≤ b
hcd : d < c
h₁ : a < c
h₂ : d < b
⊢ Icc a b ∪ Icc c d = Icc (a ⊓ c) (b ⊔ d)

case inr.inl
α : Type u_1
inst✝ : LinearOrder α
a b c d : α
hab : b < a
hcd : c ≤ d
h₁ : b < d
h₂ : c < a
⊢ Icc a b ∪ Icc c d = Icc (a ⊓ c) (b ⊔ d)

case inr.inr
α : Type u_1
inst✝ : LinearOrder α
a b c d : α
hab : b < a
hcd : d < c
h₁ : b < c
h₂ : d < a
⊢ Icc a b ∪ Icc c d = Icc (a ⊓ c) (b ⊔ d)

Tactic:
all_goals simp [*, min_eq_left_of_lt, max_eq_left_of_lt, min_eq_right_of_lt, max_eq_right_of_lt]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : LinearOrder α
a b c d : α
h₁ : a ⊓ b < c ⊔ d
h₂ : c ⊓ d < a ⊔ b
⊢ Icc a b ∪ Icc c d = Icc (a ⊓ c) (b ⊔ d)

Tactic:
rcases le_or_lt a b with hab | hab <;> rcases le_or_lt c d with hcd | hcd <;>
  simp only [min_eq_left, min_eq_right, max_eq_left, max_eq_right, min_eq_left_of_lt,
    min_eq_right_of_lt, max_eq_left_of_lt, max_eq_right_of_lt, hab, hcd] at h₁ h₂

Result:
case inl.inl
α : Type u_1
inst✝ : LinearOrder α
a b c d : α
hab : a ≤ b
hcd : c ≤ d
h₁ : a < d
h₂ : c < b
⊢ Icc a b ∪ Icc c d = Icc (a ⊓ c) (b ⊔ d)

case inl.inr
α : Type u_1
inst✝ : LinearOrder α
a b c d : α
hab : a ≤ b
hcd : d < c
h₁ : a < c
h₂ : d < b
⊢ Icc a b ∪ Icc c d = Icc (a ⊓ c) (b ⊔ d)

case inr.inl
α : Type u_1
inst✝ : LinearOrder α
a b c d : α
hab : b < a
hcd : c ≤ d
h₁ : b < d
h₂ : c < a
⊢ Icc a b ∪ Icc c d = Icc (a ⊓ c) (b ⊔ d)

case inr.inr
α : Type u_1
inst✝ : LinearOrder α
a b c d : α
hab : b < a
hcd : d < c
h₁ : b < c
h₂ : d < a
⊢ Icc a b ∪ Icc c d = Icc (a ⊓ c) (b ⊔ d)

Proof state:
case inr.inr
α : Type u_1
inst✝ : LinearOrder α
a b c d : α
hab : b < a
hcd : d < c
h₁ : b < c
h₂ : d < a
⊢ Icc a b ∪ Icc c d = Icc (a ⊓ c) (b ⊔ d)

Tactic:
simp [*, min_eq_left_of_lt, max_eq_left_of_lt, min_eq_right_of_lt, max_eq_right_of_lt]

Result:
no goals

Proof state:
case inl.inl
α : Type u_1
inst✝ : LinearOrder α
a b c d : α
hab : a ≤ b
hcd : c ≤ d
h₁ : a < d
h₂ : c < b
⊢ Icc a b ∪ Icc c d = Icc (a ⊓ c) (b ⊔ d)

Tactic:
exact Icc_union_Icc' h₂.le h₁.le

Result:
no goals
-- Mathlib/Probability/Moments/Basic.lean
theorem mgf_neg : mgf (-X) μ t = mgf X μ (-t)

Proof state:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
⊢ mgf (-X) μ t = mgf X μ (-t)

Tactic:
simp_rw [mgf, Pi.neg_apply, mul_neg, neg_mul]

Result:
no goals
-- Mathlib/FieldTheory/Minpoly/Field.lean
theorem zero : minpoly A (0 : B) = X

Proof state:
A : Type u_1
B : Type u_2
inst✝³ : Field A
inst✝² : Ring B
inst✝¹ : Algebra A B
inst✝ : Nontrivial B
⊢ minpoly A 0 = X

Tactic:
simpa only [add_zero, C_0, sub_eq_add_neg, neg_zero, RingHom.map_zero] using eq_X_sub_C B (0 : A)

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem contains_insertMany_empty_list [EquivBEq α] [LawfulHashable α]
    {l : List ((a : α) × β a)} {k : α} :
    (insertMany empty l).1.contains k = (l.map Sigma.fst).contains k

Proof state:
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
l : List ((a : α) × β a)
k : α
⊢ (empty.insertMany l).val.contains k = (List.map Sigma.fst l).contains k

Tactic:
simp [contains_insertMany_list _ Raw.WF.empty₀]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/MeasureSpace.lean
theorem tsum_meas_le_meas_iUnion_of_disjoint₀ {ι : Type*} {_ : MeasurableSpace α} (μ : Measure α)
    {As : ι → Set α} (As_mble : ∀ i : ι, NullMeasurableSet (As i) μ)
    (As_disj : Pairwise (AEDisjoint μ on As)) : (∑' i, μ (As i)) ≤ μ (⋃ i, As i)

Proof state:
α : Type u_1
ι : Type u_8
x✝ : MeasurableSpace α
μ : Measure α
As : ι → Set α
As_mble : ∀ (i : ι), NullMeasurableSet (As i) μ
As_disj : Pairwise (AEDisjoint μ on As)
⊢ ∑' (i : ι), μ (As i) ≤ μ (⋃ i, As i)

Tactic:
rw [ENNReal.tsum_eq_iSup_sum, iSup_le_iff]

Result:
α : Type u_1
ι : Type u_8
x✝ : MeasurableSpace α
μ : Measure α
As : ι → Set α
As_mble : ∀ (i : ι), NullMeasurableSet (As i) μ
As_disj : Pairwise (AEDisjoint μ on As)
⊢ ∀ (i : Finset ι), ∑ a ∈ i, μ (As a) ≤ μ (⋃ i, As i)

Proof state:
α : Type u_1
ι : Type u_8
x✝ : MeasurableSpace α
μ : Measure α
As : ι → Set α
As_mble : ∀ (i : ι), NullMeasurableSet (As i) μ
As_disj : Pairwise (AEDisjoint μ on As)
s : Finset ι
⊢ ∑ a ∈ s, μ (As a) ≤ μ (⋃ i, As i)

Tactic:
simp only [← measure_biUnion_finset₀ (fun _i _hi _j _hj hij => As_disj hij) fun i _ => As_mble i]

Result:
α : Type u_1
ι : Type u_8
x✝ : MeasurableSpace α
μ : Measure α
As : ι → Set α
As_mble : ∀ (i : ι), NullMeasurableSet (As i) μ
As_disj : Pairwise (AEDisjoint μ on As)
s : Finset ι
⊢ μ (⋃ b ∈ s, As b) ≤ μ (⋃ i, As i)

Proof state:
case h.h
α : Type u_1
ι : Type u_8
x✝ : MeasurableSpace α
μ : Measure α
As : ι → Set α
As_mble : ∀ (i : ι), NullMeasurableSet (As i) μ
As_disj : Pairwise (AEDisjoint μ on As)
s : Finset ι
i✝ : ι
⊢ ⋃ (_ : i✝ ∈ s), As i✝ ⊆ As i✝

Tactic:
exact iUnion_subset fun _ ↦ Subset.rfl

Result:
no goals

Proof state:
α : Type u_1
ι : Type u_8
x✝ : MeasurableSpace α
μ : Measure α
As : ι → Set α
As_mble : ∀ (i : ι), NullMeasurableSet (As i) μ
As_disj : Pairwise (AEDisjoint μ on As)
s : Finset ι
⊢ μ (⋃ b ∈ s, As b) ≤ μ (⋃ i, As i)

Tactic:
gcongr

Result:
case h.h
α : Type u_1
ι : Type u_8
x✝ : MeasurableSpace α
μ : Measure α
As : ι → Set α
As_mble : ∀ (i : ι), NullMeasurableSet (As i) μ
As_disj : Pairwise (AEDisjoint μ on As)
s : Finset ι
i✝ : ι
⊢ ⋃ (_ : i✝ ∈ s), As i✝ ⊆ As i✝

Proof state:
α : Type u_1
ι : Type u_8
x✝ : MeasurableSpace α
μ : Measure α
As : ι → Set α
As_mble : ∀ (i : ι), NullMeasurableSet (As i) μ
As_disj : Pairwise (AEDisjoint μ on As)
⊢ ∀ (i : Finset ι), ∑ a ∈ i, μ (As a) ≤ μ (⋃ i, As i)

Tactic:
intro s

Result:
α : Type u_1
ι : Type u_8
x✝ : MeasurableSpace α
μ : Measure α
As : ι → Set α
As_mble : ∀ (i : ι), NullMeasurableSet (As i) μ
As_disj : Pairwise (AEDisjoint μ on As)
s : Finset ι
⊢ ∑ a ∈ s, μ (As a) ≤ μ (⋃ i, As i)
-- Mathlib/Order/OmegaCompletePartialOrder.lean
theorem ωSup_iterate_le_fixedPoint (h : x ≤ f x) {a : α}
    (h_a : a ∈ fixedPoints f) (h_x_le_a : x ≤ a) :
    ωSup (iterateChain f x h) ≤ a

Proof state:
α : Type u_2
inst✝ : OmegaCompletePartialOrder α
f : α →𝒄 α
x : α
h : x ≤ f x
a : α
h_a : IsFixedPt (⇑f) a
h_x_le_a : x ≤ a
⊢ ωSup (iterateChain (↑f) x h) ≤ a

Tactic:
obtain h_a := Eq.le h_a

Result:
α : Type u_2
inst✝ : OmegaCompletePartialOrder α
f : α →𝒄 α
x : α
h : x ≤ f x
a : α
h_a✝ : IsFixedPt (⇑f) a
h_x_le_a : x ≤ a
h_a : f a ≤ a
⊢ ωSup (iterateChain (↑f) x h) ≤ a

Proof state:
α : Type u_2
inst✝ : OmegaCompletePartialOrder α
f : α →𝒄 α
x : α
h : x ≤ f x
a : α
h_a : a ∈ fixedPoints ⇑f
h_x_le_a : x ≤ a
⊢ ωSup (iterateChain (↑f) x h) ≤ a

Tactic:
rw [mem_fixedPoints] at h_a

Result:
α : Type u_2
inst✝ : OmegaCompletePartialOrder α
f : α →𝒄 α
x : α
h : x ≤ f x
a : α
h_a : IsFixedPt (⇑f) a
h_x_le_a : x ≤ a
⊢ ωSup (iterateChain (↑f) x h) ≤ a

Proof state:
α : Type u_2
inst✝ : OmegaCompletePartialOrder α
f : α →𝒄 α
x : α
h : x ≤ f x
a : α
h_a✝ : IsFixedPt (⇑f) a
h_x_le_a : x ≤ a
h_a : f a ≤ a
⊢ ωSup (iterateChain (↑f) x h) ≤ a

Tactic:
exact ωSup_iterate_le_prefixedPoint f x h h_a h_x_le_a

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Attach.lean
theorem countP_attachWith {p : α → Prop} (l : Vector α n) (H : ∀ a ∈ l, p a) (q : α → Bool) :
    (l.attachWith p H).countP (fun a : {x // p x} => q a) = l.countP q

Proof state:
case mk
α : Type u_1
n : Nat
p : α → Prop
q : α → Bool
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
H : ∀ (a : α), a ∈ { toArray := toArray✝, size_toArray := size_toArray✝ } → p a
⊢ countP (fun a => q a.val) ({ toArray := toArray✝, size_toArray := size_toArray✝ }.attachWith p H) =
    countP q { toArray := toArray✝, size_toArray := size_toArray✝ }

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
n : Nat
p : α → Prop
l : Vector α n
H : ∀ (a : α), a ∈ l → p a
q : α → Bool
⊢ countP (fun a => q a.val) (l.attachWith p H) = countP q l

Tactic:
cases l

Result:
case mk
α : Type u_1
n : Nat
p : α → Prop
q : α → Bool
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
H : ∀ (a : α), a ∈ { toArray := toArray✝, size_toArray := size_toArray✝ } → p a
⊢ countP (fun a => q a.val) ({ toArray := toArray✝, size_toArray := size_toArray✝ }.attachWith p H) =
    countP q { toArray := toArray✝, size_toArray := size_toArray✝ }
-- Mathlib/Topology/MetricSpace/Pseudo/Defs.lean
theorem closedBall_eq_singleton_of_subsingleton [Subsingleton α] (h : 0 ≤ ε) :
    closedBall x ε = {x}

Proof state:
case h
α : Type u
inst✝¹ : PseudoMetricSpace α
x : α
ε : ℝ
inst✝ : Subsingleton α
h : 0 ≤ ε
x' : α
⊢ x' ∈ closedBall x ε ↔ x' ∈ {x}

Tactic:
simpa [Subsingleton.allEq x x']

Result:
no goals

Proof state:
α : Type u
inst✝¹ : PseudoMetricSpace α
x : α
ε : ℝ
inst✝ : Subsingleton α
h : 0 ≤ ε
⊢ closedBall x ε = {x}

Tactic:
ext x'

Result:
case h
α : Type u
inst✝¹ : PseudoMetricSpace α
x : α
ε : ℝ
inst✝ : Subsingleton α
h : 0 ≤ ε
x' : α
⊢ x' ∈ closedBall x ε ↔ x' ∈ {x}
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Basic.lean
theorem surjOn_sin : SurjOn sin (Icc (-(π / 2)) (π / 2)) (Icc (-1) 1)

Proof state:
⊢ SurjOn sin (Icc (-(π / 2)) (π / 2)) (Icc (-1) 1)

Tactic:
simpa only [sin_neg, sin_pi_div_two] using
  intermediate_value_Icc (neg_le_self pi_div_two_pos.le) continuous_sin.continuousOn

Result:
no goals
-- Mathlib/Topology/EMetricSpace/Defs.lean
theorem tendsto_nhdsWithin_nhds {a b} :
    Tendsto f (𝓝[s] a) (𝓝 b) ↔
      ∀ ε > 0, ∃ δ > 0, ∀ {x : α}, x ∈ s → edist x a < δ → edist (f x) b < ε

Proof state:
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
s : Set α
inst✝ : PseudoEMetricSpace β
f : α → β
a : α
b : β
⊢ Tendsto f (𝓝[s] a) (𝓝 b) ↔ ∀ ε > 0, ∃ δ > 0, ∀ {x : α}, x ∈ s → edist x a < δ → edist (f x) b < ε

Tactic:
rw [← nhdsWithin_univ b, tendsto_nhdsWithin_nhdsWithin]

Result:
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
s : Set α
inst✝ : PseudoEMetricSpace β
f : α → β
a : α
b : β
⊢ (∀ ε > 0, ∃ δ > 0, ∀ ⦃x : α⦄, x ∈ s → edist x a < δ → f x ∈ univ ∧ edist (f x) b < ε) ↔
    ∀ ε > 0, ∃ δ > 0, ∀ {x : α}, x ∈ s → edist x a < δ → edist (f x) b < ε

Proof state:
α : Type u
β : Type v
inst✝¹ : PseudoEMetricSpace α
s : Set α
inst✝ : PseudoEMetricSpace β
f : α → β
a : α
b : β
⊢ (∀ ε > 0, ∃ δ > 0, ∀ ⦃x : α⦄, x ∈ s → edist x a < δ → f x ∈ univ ∧ edist (f x) b < ε) ↔
    ∀ ε > 0, ∃ δ > 0, ∀ {x : α}, x ∈ s → edist x a < δ → edist (f x) b < ε

Tactic:
simp only [mem_univ, true_and]

Result:
no goals
-- Mathlib/MeasureTheory/Function/L1Space/AEEqFun.lean
theorem ofReal_norm_eq_lintegral (f : α →₁[μ] β) : ENNReal.ofReal ‖f‖ = ∫⁻ x, ‖f x‖ₑ ∂μ

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f : ↥(Lp β 1 μ)
⊢ ENNReal.ofReal ‖f‖ = ∫⁻ (x : α), ‖↑↑f x‖ₑ ∂μ

Tactic:
rw [norm_def, ENNReal.ofReal_toReal]

Result:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f : ↥(Lp β 1 μ)
⊢ ∫⁻ (a : α), ‖↑↑f a‖ₑ ∂μ ≠ ⊤

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f : ↥(Lp β 1 μ)
⊢ ∫⁻ (a : α), ‖↑↑f a‖ₑ ∂μ ≠ ⊤

Tactic:
exact ne_of_lt (hasFiniteIntegral_coeFn f)

Result:
no goals
-- Mathlib/Data/Matroid/Closure.lean
lemma Indep.insert_dep_iff (hI : M.Indep I) : M.Dep (insert e I) ↔ e ∈ M.closure I \ I

Proof state:
α : Type u_2
M : Matroid α
e : α
I : Set α
hI : M.Indep I
heI : e ∈ I
⊢ ¬M.Dep (insert e I)

Tactic:
rw [insert_eq_of_mem heI]

Result:
α : Type u_2
M : Matroid α
e : α
I : Set α
hI : M.Indep I
heI : e ∈ I
⊢ ¬M.Dep I

Proof state:
α : Type u_2
M : Matroid α
e : α
I : Set α
hI : M.Indep I
heI : e ∈ I
⊢ ¬M.Dep I

Tactic:
exact hI.not_dep

Result:
no goals

Proof state:
α : Type u_2
M : Matroid α
e : α
I : Set α
hI : M.Indep I
⊢ e ∈ I → ¬M.Dep (insert e I)

Tactic:
intro heI

Result:
α : Type u_2
M : Matroid α
e : α
I : Set α
hI : M.Indep I
heI : e ∈ I
⊢ ¬M.Dep (insert e I)

Proof state:
α : Type u_2
M : Matroid α
e : α
I : Set α
hI : M.Indep I
⊢ M.Dep (insert e I) ↔ e ∈ M.closure I \ I

Tactic:
rw [mem_diff, hI.mem_closure_iff, or_and_right, and_not_self_iff, or_false,
  iff_self_and, imp_not_comm]

Result:
α : Type u_2
M : Matroid α
e : α
I : Set α
hI : M.Indep I
⊢ e ∈ I → ¬M.Dep (insert e I)
-- Mathlib/Analysis/SpecialFunctions/Pow/NNReal.lean
theorem rpow_mul (x : ℝ≥0∞) (y z : ℝ) : x ^ (y * z) = (x ^ y) ^ z

Proof state:
y z : ℝ
x : ℝ≥0
h : ¬x = 0
⊢ x ^ y ≠ 0

Tactic:
simp [h]

Result:
no goals

Proof state:
case neg
y z : ℝ
x : ℝ≥0
h : ¬x = 0
this : x ^ y ≠ 0
⊢ ↑x ^ (y * z) = (↑x ^ y) ^ z

Tactic:
simp [← coe_rpow_of_ne_zero, h, this, NNReal.rpow_mul]

Result:
no goals

Proof state:
case pos
y z : ℝ
x : ℝ≥0
h : x = 0
⊢ ↑x ^ (y * z) = (↑x ^ y) ^ z

Tactic:
rcases lt_trichotomy y 0 with (Hy | Hy | Hy) <;>
    rcases lt_trichotomy z 0 with (Hz | Hz | Hz) <;>
  simp [h, Hy, Hz, zero_rpow_of_neg, zero_rpow_of_pos, top_rpow_of_neg, top_rpow_of_pos,
    mul_pos_of_neg_of_neg, mul_neg_of_neg_of_pos, mul_neg_of_pos_of_neg]

Result:
no goals

Proof state:
case coe
y z : ℝ
x : ℝ≥0
⊢ ↑x ^ (y * z) = (↑x ^ y) ^ z

Tactic:
by_cases h : x = 0

Result:
case pos
y z : ℝ
x : ℝ≥0
h : x = 0
⊢ ↑x ^ (y * z) = (↑x ^ y) ^ z

case neg
y z : ℝ
x : ℝ≥0
h : ¬x = 0
⊢ ↑x ^ (y * z) = (↑x ^ y) ^ z

Proof state:
case top
y z : ℝ
⊢ ⊤ ^ (y * z) = (⊤ ^ y) ^ z

Tactic:
rcases lt_trichotomy y 0 with (Hy | Hy | Hy) <;>
    rcases lt_trichotomy z 0 with (Hz | Hz | Hz) <;>
  simp [Hy, Hz, zero_rpow_of_neg, zero_rpow_of_pos, top_rpow_of_neg, top_rpow_of_pos,
    mul_pos_of_neg_of_neg, mul_neg_of_neg_of_pos, mul_neg_of_pos_of_neg]

Result:
no goals

Proof state:
case neg
y z : ℝ
x : ℝ≥0
h : ¬x = 0
⊢ ↑x ^ (y * z) = (↑x ^ y) ^ z

Tactic:
have : x ^ y ≠ 0 := by simp [h]

Result:
case neg
y z : ℝ
x : ℝ≥0
h : ¬x = 0
this : x ^ y ≠ 0
⊢ ↑x ^ (y * z) = (↑x ^ y) ^ z