harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Topology/MetricSpace/Pseudo/Pi.lean
lemma dist_pi_le_iff {f g : ∀ b, π b} {r : ℝ} (hr : 0 ≤ r) :
    dist f g ≤ r ↔ ∀ b, dist (f b) (g b) ≤ r

Proof state:
β : Type u_2
π : β → Type u_3
inst✝¹ : Fintype β
inst✝ : (b : β) → PseudoMetricSpace (π b)
f g : (b : β) → π b
r : ℝ
hr : 0 ≤ r
⊢ dist f g ≤ r ↔ ∀ (b : β), dist (f b) (g b) ≤ r

Tactic:
lift r to ℝ≥0 using hr

Result:
case intro
β : Type u_2
π : β → Type u_3
inst✝¹ : Fintype β
inst✝ : (b : β) → PseudoMetricSpace (π b)
f g : (b : β) → π b
r : ℝ≥0
⊢ dist f g ≤ ↑r ↔ ∀ (b : β), dist (f b) (g b) ≤ ↑r

Proof state:
case intro
β : Type u_2
π : β → Type u_3
inst✝¹ : Fintype β
inst✝ : (b : β) → PseudoMetricSpace (π b)
f g : (b : β) → π b
r : ℝ≥0
⊢ dist f g ≤ ↑r ↔ ∀ (b : β), dist (f b) (g b) ≤ ↑r

Tactic:
exact nndist_pi_le_iff

Result:
no goals
-- Mathlib/Topology/Algebra/NonUnitalStarAlgebra.lean
theorem le_of_mem {x : A} {s : NonUnitalStarSubalgebra R A} (hs : IsClosed (s : Set A))
    (hx : x ∈ s) : elemental R x ≤ s :=
  topologicalClosure_minimal _ (adjoin_le <| by simpa using hx) hs

Proof state:
R : Type u_1
A : Type u_2
inst✝¹¹ : CommSemiring R
inst✝¹⁰ : StarRing R
inst✝⁹ : NonUnitalSemiring A
inst✝⁸ : StarRing A
inst✝⁷ : Module R A
inst✝⁶ : IsScalarTower R A A
inst✝⁵ : SMulCommClass R A A
inst✝⁴ : StarModule R A
inst✝³ : TopologicalSpace A
inst✝² : IsTopologicalSemiring A
inst✝¹ : ContinuousConstSMul R A
inst✝ : ContinuousStar A
x : A
s : NonUnitalStarSubalgebra R A
hs : IsClosed ↑s
hx : x ∈ s
⊢ {x} ⊆ ↑s

Tactic:
simpa using hx

Result:
no goals
-- Mathlib/Order/Interval/Set/ProjIcc.lean
theorem projIcc_of_le_left (hx : x ≤ a) : projIcc a b h x = ⟨a, left_mem_Icc.2 h⟩

Proof state:
α : Type u_1
inst✝ : LinearOrder α
a b : α
h : a ≤ b
x : α
hx : x ≤ a
⊢ projIcc a b h x = ⟨a, ⋯⟩

Tactic:
simp [projIcc, hx, hx.trans h]

Result:
no goals
-- Mathlib/Topology/UniformSpace/Separation.lean
theorem t0Space_iff_uniformity' :
    T0Space α ↔ Pairwise fun x y ↦ ∃ r ∈ 𝓤 α, (x, y) ∉ r

Proof state:
α : Type u
inst✝ : UniformSpace α
⊢ T0Space α ↔ Pairwise fun x y => ∃ r ∈ 𝓤 α, (x, y) ∉ r

Tactic:
simp [t0Space_iff_not_inseparable, inseparable_iff_ker_uniformity]

Result:
no goals
-- Mathlib/Probability/ConditionalProbability.lean
theorem cond_inter_self (hms : MeasurableSet s) (t : Set Ω) (μ : Measure Ω) :
    μ[s ∩ t|s] = μ[t|s]

Proof state:
Ω : Type u_1
m : MeasurableSpace Ω
s : Set Ω
hms : MeasurableSet s
t : Set Ω
μ : Measure Ω
⊢ μ[s ∩ t | s] = μ[t | s]

Tactic:
rw [cond_apply hms, ← Set.inter_assoc, Set.inter_self, ← cond_apply hms]

Result:
no goals
-- Mathlib/Algebra/Order/Group/Unbundled/Basic.lean
theorem lt_div_iff_mul_lt' : b < c / a ↔ a * b < c

Proof state:
α : Type u
inst✝² : CommGroup α
inst✝¹ : LT α
inst✝ : MulLeftStrictMono α
a b c : α
⊢ b < c / a ↔ a * b < c

Tactic:
rw [lt_div_iff_mul_lt, mul_comm]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem replicate_succ' : replicate (n + 1) a = replicate n a ++ [a]

Proof state:
n : Nat
α✝ : Type u_1
a : α✝
⊢ replicate (n + 1) a = replicate n a ++ [a]

Tactic:
induction n <;> simp_all [replicate_succ, ← cons_append]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/MeanInequalities.lean
theorem lintegral_rpow_funMulInvSnorm_eq_one {p : ℝ} (hp0_lt : 0 < p) {f : α → ℝ≥0∞}
    (hf_nonzero : (∫⁻ a, f a ^ p ∂μ) ≠ 0) (hf_top : (∫⁻ a, f a ^ p ∂μ) ≠ ⊤) :
    ∫⁻ c, funMulInvSnorm f p μ c ^ p ∂μ = 1

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
p : ℝ
hp0_lt : 0 < p
f : α → ℝ≥0∞
hf_nonzero : ∫⁻ (a : α), f a ^ p ∂μ ≠ 0
hf_top : ∫⁻ (a : α), f a ^ p ∂μ ≠ ⊤
⊢ ∫⁻ (c : α), f c ^ p * (∫⁻ (c : α), f c ^ p ∂μ)⁻¹ ∂μ = 1

Tactic:
rw [lintegral_mul_const', ENNReal.mul_inv_cancel hf_nonzero hf_top]

Result:
case hr
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
p : ℝ
hp0_lt : 0 < p
f : α → ℝ≥0∞
hf_nonzero : ∫⁻ (a : α), f a ^ p ∂μ ≠ 0
hf_top : ∫⁻ (a : α), f a ^ p ∂μ ≠ ⊤
⊢ (∫⁻ (c : α), f c ^ p ∂μ)⁻¹ ≠ ⊤

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
p : ℝ
hp0_lt : 0 < p
f : α → ℝ≥0∞
hf_nonzero : ∫⁻ (a : α), f a ^ p ∂μ ≠ 0
hf_top : ∫⁻ (a : α), f a ^ p ∂μ ≠ ⊤
⊢ ∫⁻ (c : α), funMulInvSnorm f p μ c ^ p ∂μ = 1

Tactic:
simp_rw [funMulInvSnorm_rpow hp0_lt]

Result:
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
p : ℝ
hp0_lt : 0 < p
f : α → ℝ≥0∞
hf_nonzero : ∫⁻ (a : α), f a ^ p ∂μ ≠ 0
hf_top : ∫⁻ (a : α), f a ^ p ∂μ ≠ ⊤
⊢ ∫⁻ (c : α), f c ^ p * (∫⁻ (c : α), f c ^ p ∂μ)⁻¹ ∂μ = 1

Proof state:
case hr
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
p : ℝ
hp0_lt : 0 < p
f : α → ℝ≥0∞
hf_nonzero : ∫⁻ (a : α), f a ^ p ∂μ ≠ 0
hf_top : ∫⁻ (a : α), f a ^ p ∂μ ≠ ⊤
⊢ (∫⁻ (c : α), f c ^ p ∂μ)⁻¹ ≠ ⊤

Tactic:
rwa [inv_ne_top]

Result:
no goals
-- Mathlib/Topology/Algebra/Module/FiniteDimension.lean
theorem toLinearEquiv_toContinuousLinearEquiv_symm (e : E ≃ₗ[𝕜] F) :
    e.toContinuousLinearEquiv.symm.toLinearEquiv = e.symm

Proof state:
𝕜 : Type u
hnorm : NontriviallyNormedField 𝕜
E : Type v
inst✝¹³ : AddCommGroup E
inst✝¹² : Module 𝕜 E
inst✝¹¹ : TopologicalSpace E
inst✝¹⁰ : IsTopologicalAddGroup E
inst✝⁹ : ContinuousSMul 𝕜 E
F : Type w
inst✝⁸ : AddCommGroup F
inst✝⁷ : Module 𝕜 F
inst✝⁶ : TopologicalSpace F
inst✝⁵ : IsTopologicalAddGroup F
inst✝⁴ : ContinuousSMul 𝕜 F
inst✝³ : CompleteSpace 𝕜
inst✝² : T2Space E
inst✝¹ : T2Space F
inst✝ : FiniteDimensional 𝕜 E
e : E ≃ₗ[𝕜] F
⊢ e.toContinuousLinearEquiv.symm.toLinearEquiv = e.symm

Tactic:
ext x

Result:
case h
𝕜 : Type u
hnorm : NontriviallyNormedField 𝕜
E : Type v
inst✝¹³ : AddCommGroup E
inst✝¹² : Module 𝕜 E
inst✝¹¹ : TopologicalSpace E
inst✝¹⁰ : IsTopologicalAddGroup E
inst✝⁹ : ContinuousSMul 𝕜 E
F : Type w
inst✝⁸ : AddCommGroup F
inst✝⁷ : Module 𝕜 F
inst✝⁶ : TopologicalSpace F
inst✝⁵ : IsTopologicalAddGroup F
inst✝⁴ : ContinuousSMul 𝕜 F
inst✝³ : CompleteSpace 𝕜
inst✝² : T2Space E
inst✝¹ : T2Space F
inst✝ : FiniteDimensional 𝕜 E
e : E ≃ₗ[𝕜] F
x : F
⊢ e.toContinuousLinearEquiv.symm.toLinearEquiv x = e.symm x

Proof state:
case h
𝕜 : Type u
hnorm : NontriviallyNormedField 𝕜
E : Type v
inst✝¹³ : AddCommGroup E
inst✝¹² : Module 𝕜 E
inst✝¹¹ : TopologicalSpace E
inst✝¹⁰ : IsTopologicalAddGroup E
inst✝⁹ : ContinuousSMul 𝕜 E
F : Type w
inst✝⁸ : AddCommGroup F
inst✝⁷ : Module 𝕜 F
inst✝⁶ : TopologicalSpace F
inst✝⁵ : IsTopologicalAddGroup F
inst✝⁴ : ContinuousSMul 𝕜 F
inst✝³ : CompleteSpace 𝕜
inst✝² : T2Space E
inst✝¹ : T2Space F
inst✝ : FiniteDimensional 𝕜 E
e : E ≃ₗ[𝕜] F
x : F
⊢ e.toContinuousLinearEquiv.symm.toLinearEquiv x = e.symm x

Tactic:
rfl

Result:
no goals
-- Mathlib/Order/Lattice.lean
theorem map_sup [SemilatticeSup β] {f : α → β} (hf : Monotone f) (x y : α) :
    f (x ⊔ y) = f x ⊔ f y :=
  (IsTotal.total x y).elim (fun h : x ≤ y => by simp only [h, hf h, sup_of_le_right]) fun h => by
    simp only [h, hf h, sup_of_le_left]

Proof state:
α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : SemilatticeSup β
f : α → β
hf : Monotone f
x y : α
h : y ≤ x
⊢ f (x ⊔ y) = f x ⊔ f y

Tactic:
simp only [h, hf h, sup_of_le_left]

Result:
no goals

Proof state:
α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : SemilatticeSup β
f : α → β
hf : Monotone f
x y : α
h : x ≤ y
⊢ f (x ⊔ y) = f x ⊔ f y

Tactic:
simp only [h, hf h, sup_of_le_right]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem contains_alter_self [EquivBEq α] [LawfulHashable α] {k : α} {f : Option β → Option β}
    (h : m.WF) : (Const.alter m k f).contains k = (f (Const.get? m k)).isSome

Proof state:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
β : Type v
m : Raw α fun x => β
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
k : α
f : Option β → Option β
h : m.WF
⊢ (alter m k f).contains k = (f (get? m k)).isSome

Tactic:
simp only [contains_alter h, BEq.refl, reduceIte]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/Pullback/CommSq.lean
/-- The following diagram is a pullback
```
X --f--> Z
|        |
id       id
v        v
X --f--> Z
```
-/
lemma id_vert (f : X ⟶ Z) : IsPushout f (𝟙 X) (𝟙 Z) f :=
  of_vert_isIso ⟨by simp only [Category.id_comp, Category.comp_id]⟩

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
Z X : C
f : X ⟶ Z
⊢ f ≫ 𝟙 Z = 𝟙 X ≫ f

Tactic:
simp only [Category.id_comp, Category.comp_id]

Result:
no goals
-- Mathlib/Order/Filter/Prod.lean
theorem prod_iInf_left [Nonempty ι] {f : ι → Filter α} {g : Filter β} :
    (⨅ i, f i) ×ˢ g = ⨅ i, f i ×ˢ g

Proof state:
α : Type u_1
β : Type u_2
ι : Sort u_5
inst✝ : Nonempty ι
f : ι → Filter α
g : Filter β
⊢ (⨅ i, f i) ×ˢ g = ⨅ i, f i ×ˢ g

Tactic:
simp only [prod_eq_inf, comap_iInf, iInf_inf]

Result:
no goals
-- Mathlib/FieldTheory/SeparableDegree.lean
theorem finSepDegree_adjoin_simple_eq_finrank_iff (α : E) (halg : IsAlgebraic F α) :
    finSepDegree F F⟮α⟯ = finrank F F⟮α⟯ ↔ IsSeparable F α

Proof state:
F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
α : E
halg : IsAlgebraic F α
⊢ finSepDegree F ↥F⟮α⟯ = finrank F ↥F⟮α⟯ ↔ IsSeparable F α

Tactic:
rw [finSepDegree_adjoin_simple_eq_natSepDegree F E halg, adjoin.finrank halg.isIntegral,
  natSepDegree_eq_natDegree_iff _ (minpoly.ne_zero halg.isIntegral), IsSeparable]

Result:
no goals
-- Mathlib/Logic/Basic.lean
lemma exists_or_forall_not (P : α → Prop) : (∃ a, P a) ∨ ∀ a, ¬ P a

Proof state:
α : Sort u_1
P : α → Prop
⊢ (∃ a, P a) ∨ ¬∃ x, P x

Tactic:
exact em _

Result:
no goals

Proof state:
α : Sort u_1
P : α → Prop
⊢ (∃ a, P a) ∨ ∀ (a : α), ¬P a

Tactic:
rw [← not_exists]

Result:
α : Sort u_1
P : α → Prop
⊢ (∃ a, P a) ∨ ¬∃ x, P x
-- Mathlib/Algebra/Star/Conjneg.lean
@[simp] lemma conjneg_sub (f g : G → R) : conjneg (f - g) = conjneg f - conjneg g

Proof state:
G : Type u_2
R : Type u_3
inst✝² : AddGroup G
inst✝¹ : CommRing R
inst✝ : StarRing R
f g : G → R
⊢ conjneg (f - g) = conjneg f - conjneg g

Tactic:
ext

Result:
case h
G : Type u_2
R : Type u_3
inst✝² : AddGroup G
inst✝¹ : CommRing R
inst✝ : StarRing R
f g : G → R
x✝ : G
⊢ conjneg (f - g) x✝ = (conjneg f - conjneg g) x✝

Proof state:
case h
G : Type u_2
R : Type u_3
inst✝² : AddGroup G
inst✝¹ : CommRing R
inst✝ : StarRing R
f g : G → R
x✝ : G
⊢ conjneg (f - g) x✝ = (conjneg f - conjneg g) x✝

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Fin/Lemmas.lean
theorem lt_succ {a : Fin n} : a.castSucc < a.succ

Proof state:
n : Nat
a : Fin n
⊢ a.castSucc < a.succ

Tactic:
rw [castSucc, lt_def, coe_castAdd, val_succ]

Result:
n : Nat
a : Fin n
⊢ ↑a < ↑a + 1

Proof state:
n : Nat
a : Fin n
⊢ ↑a < ↑a + 1

Tactic:
exact Nat.lt_succ_self a.val

Result:
no goals
-- Mathlib/Analysis/Fourier/Inversion.lean
theorem Continuous.fourier_inversion_inv (h : Continuous f)
    (hf : Integrable f) (h'f : Integrable (𝓕 f)) :
    𝓕 (𝓕⁻ f) = f

Proof state:
V : Type u_1
E : Type u_2
inst✝⁷ : NormedAddCommGroup V
inst✝⁶ : InnerProductSpace ℝ V
inst✝⁵ : MeasurableSpace V
inst✝⁴ : BorelSpace V
inst✝³ : FiniteDimensional ℝ V
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
f : V → E
inst✝ : CompleteSpace E
h : Continuous f
hf : Integrable f volume
h'f : Integrable (𝓕 f) volume
⊢ 𝓕 (𝓕⁻ f) = f

Tactic:
ext v

Result:
case h
V : Type u_1
E : Type u_2
inst✝⁷ : NormedAddCommGroup V
inst✝⁶ : InnerProductSpace ℝ V
inst✝⁵ : MeasurableSpace V
inst✝⁴ : BorelSpace V
inst✝³ : FiniteDimensional ℝ V
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
f : V → E
inst✝ : CompleteSpace E
h : Continuous f
hf : Integrable f volume
h'f : Integrable (𝓕 f) volume
v : V
⊢ 𝓕 (𝓕⁻ f) v = f v

Proof state:
case h
V : Type u_1
E : Type u_2
inst✝⁷ : NormedAddCommGroup V
inst✝⁶ : InnerProductSpace ℝ V
inst✝⁵ : MeasurableSpace V
inst✝⁴ : BorelSpace V
inst✝³ : FiniteDimensional ℝ V
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
f : V → E
inst✝ : CompleteSpace E
h : Continuous f
hf : Integrable f volume
h'f : Integrable (𝓕 f) volume
v : V
⊢ 𝓕 (𝓕⁻ f) v = f v

Tactic:
exact hf.fourier_inversion_inv h'f h.continuousAt

Result:
no goals
-- Mathlib/Analysis/Asymptotics/Defs.lean
theorem isBigOWith_zero (hc : 0 ≤ c) : IsBigOWith c l (fun _x => (0 : E')) g' :=
  IsBigOWith.of_bound <| univ_mem' fun x => by simpa using mul_nonneg hc (norm_nonneg <| g' x)

Proof state:
α : Type u_1
E' : Type u_6
F' : Type u_7
inst✝¹ : SeminormedAddCommGroup E'
inst✝ : SeminormedAddCommGroup F'
c : ℝ
g' : α → F'
l : Filter α
hc : 0 ≤ c
x : α
⊢ x ∈ {x | (fun x => ‖0‖ ≤ c * ‖g' x‖) x}

Tactic:
simpa using mul_nonneg hc (norm_nonneg <| g' x)

Result:
no goals
-- Mathlib/Data/Set/Image.lean
theorem compl_compl_image [BooleanAlgebra α] (S : Set α) :
    HasCompl.compl '' (HasCompl.compl '' S) = S

Proof state:
α : Type u_1
inst✝ : BooleanAlgebra α
S : Set α
⊢ compl '' (compl '' S) = S

Tactic:
rw [← image_comp, compl_comp_compl, image_id]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/Lemmas.lean
theorem neg_add_cancel_left (a b : Int) : -a + (a + b) = b

Proof state:
a b : Int
⊢ -a + (a + b) = b

Tactic:
rw [← Int.add_assoc, Int.add_left_neg, Int.zero_add]

Result:
no goals
-- Mathlib/Topology/ContinuousOn.lean
theorem nhdsWithin_insert (a : α) (s : Set α) : 𝓝[insert a s] a = pure a ⊔ 𝓝[s] a

Proof state:
α : Type u_1
inst✝ : TopologicalSpace α
a : α
s : Set α
⊢ 𝓝[insert a s] a = pure a ⊔ 𝓝[s] a

Tactic:
rw [← singleton_union, nhdsWithin_union, nhdsWithin_singleton]

Result:
no goals
-- Mathlib/Topology/Compactification/OnePoint.lean
theorem isOpen_iff_of_mem (h : ∞ ∈ s) :
    IsOpen s ↔ IsClosed ((↑) ⁻¹' s : Set X)ᶜ ∧ IsCompact ((↑) ⁻¹' s : Set X)ᶜ

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
s : Set (OnePoint X)
h : ∞ ∈ s
⊢ IsOpen s ↔ IsClosed (some ⁻¹' s)ᶜ ∧ IsCompact (some ⁻¹' s)ᶜ

Tactic:
simp only [isOpen_iff_of_mem' h, isClosed_compl_iff, and_comm]

Result:
no goals
-- Mathlib/CategoryTheory/Preadditive/Biproducts.lean
theorem HasBiproduct.of_hasProduct (f : J → C) [HasProduct f] : HasBiproduct f

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
J : Type
inst✝¹ : Finite J
f : J → C
inst✝ : HasProduct f
⊢ HasBiproduct f

Tactic:
cases nonempty_fintype J

Result:
case intro
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
J : Type
inst✝¹ : Finite J
f : J → C
inst✝ : HasProduct f
val✝ : Fintype J
⊢ HasBiproduct f

Proof state:
case intro
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
J : Type
inst✝¹ : Finite J
f : J → C
inst✝ : HasProduct f
val✝ : Fintype J
⊢ HasBiproduct f

Tactic:
exact HasBiproduct.mk
  { bicone := _
    isBilimit := biconeIsBilimitOfLimitConeOfIsLimit (limit.isLimit _) }

Result:
no goals
-- Mathlib/Algebra/Order/ToIntervalMod.lean
theorem toIocDiv_add_right (a b : α) : toIocDiv hp a (b + p) = toIocDiv hp a b + 1

Proof state:
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
⊢ toIocDiv hp a (b + p) = toIocDiv hp a b + 1

Tactic:
simpa only [one_zsmul] using toIocDiv_add_zsmul hp a b 1

Result:
no goals
-- Mathlib/Data/ENNReal/Operations.lean
theorem ofReal_sum_of_nonneg {s : Finset α} {f : α → ℝ} (hf : ∀ i, i ∈ s → 0 ≤ f i) :
    ENNReal.ofReal (∑ i ∈ s, f i) = ∑ i ∈ s, ENNReal.ofReal (f i)

Proof state:
α : Type u_1
s : Finset α
f : α → ℝ
hf : ∀ i ∈ s, 0 ≤ f i
⊢ (∑ i ∈ s, f i).toNNReal = ∑ a ∈ s, (f a).toNNReal

Tactic:
exact Real.toNNReal_sum_of_nonneg hf

Result:
no goals

Proof state:
α : Type u_1
s : Finset α
f : α → ℝ
hf : ∀ i ∈ s, 0 ≤ f i
⊢ ENNReal.ofReal (∑ i ∈ s, f i) = ∑ i ∈ s, ENNReal.ofReal (f i)

Tactic:
simp_rw [ENNReal.ofReal, ← coe_finset_sum, coe_inj]

Result:
α : Type u_1
s : Finset α
f : α → ℝ
hf : ∀ i ∈ s, 0 ≤ f i
⊢ (∑ i ∈ s, f i).toNNReal = ∑ a ∈ s, (f a).toNNReal
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem foldr_eq_foldrM (f : α → β → β) (b) (l : List α) :
    l.foldr f b = l.foldrM (m := Id) f b

Proof state:
α : Type u_1
β : Type u_2
f : α → β → β
b : β
l : List α
⊢ foldr f b l = foldrM f b l

Tactic:
induction l <;> simp [*, foldr]

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/List/Lemmas.lean
theorem get_range {n} (i) (H : i < (range n).length) : get (range n) ⟨i, H⟩ = i

Proof state:
n i : Nat
H : i < (range n).length
⊢ (range n).get ⟨i, H⟩ = i

Tactic:
simp

Result:
no goals
-- Mathlib/Order/Iterate.lean
theorem iterate_pos_eq_iff_map_eq (h : Commute f g) (hf : Monotone f) (hg : StrictMono g) {x n}
    (hn : 0 < n) : f^[n] x = g^[n] x ↔ f x = g x

Proof state:
α : Type u_1
inst✝ : LinearOrder α
f g : α → α
h : Commute f g
hf : Monotone f
hg : StrictMono g
x : α
n : ℕ
hn : 0 < n
⊢ f^[n] x = g^[n] x ↔ f x = g x

Tactic:
simp only [le_antisymm_iff, h.iterate_pos_le_iff_map_le hf hg hn,
  h.symm.iterate_pos_le_iff_map_le' hg hf hn]

Result:
no goals
-- Mathlib/Algebra/Order/Sub/Defs.lean
theorem add_tsub_cancel_right (hb : AddLECancellable b) : a + b - b = a :=
  hb.tsub_eq_of_eq_add <| by rw [add_comm]

Proof state:
α : Type u_1
inst✝³ : PartialOrder α
inst✝² : AddCommSemigroup α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b : α
hb : AddLECancellable b
⊢ a + b = a + b

Tactic:
rw [add_comm]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Attach.lean
theorem attachWith_map {l : List α} (f : α → β) {P : β → Prop} {H : ∀ (b : β), b ∈ l.map f → P b} :
    (l.map f).attachWith P H = (l.attachWith (P ∘ f) (fun _ h => H _ (mem_map_of_mem f h))).map
      fun ⟨x, h⟩ => ⟨f x, h⟩

Proof state:
α : Type u_1
β : Type u_2
l : List α
f : α → β
P : β → Prop
H : ∀ (b : β), b ∈ map f l → P b
⊢ (map f l).attachWith P H =
    map
      (fun x =>
        match x with
        | ⟨x, h⟩ => ⟨f x, h⟩)
      (l.attachWith (P ∘ f) ⋯)

Tactic:
induction l <;> simp [*]

Result:
no goals
-- Mathlib/GroupTheory/OrderOfElement.lean
theorem orderOf_dvd_sub_iff_zpow_eq_zpow {a b : ℤ} : (orderOf x : ℤ) ∣ a - b ↔ x ^ a = x ^ b

Proof state:
G : Type u_1
inst✝ : Group G
x : G
a b : ℤ
⊢ ↑(orderOf x) ∣ a - b ↔ x ^ a = x ^ b

Tactic:
rw [orderOf_dvd_iff_zpow_eq_one, zpow_sub, mul_inv_eq_one]

Result:
no goals
-- Mathlib/Data/Ordmap/Ordset.lean
theorem foldr_cons_eq_toList : ∀ (t : Ordnode α) (r : List α), t.foldr List.cons r = toList t ++ r
  | nil, _ => rfl
  | node _ l x r, r' => by
    rw [foldr, foldr_cons_eq_toList l, foldr_cons_eq_toList r, ← List.cons_append,
        ← List.append_assoc, ← foldr_cons_eq_toList l]; rfl

Proof state:
α : Type u_1
size✝ : ℕ
l : Ordnode α
x : α
r : Ordnode α
r' : List α
⊢ foldr List.cons (node size✝ l x r) r' = (node size✝ l x r).toList ++ r'

Tactic:
rw [foldr, foldr_cons_eq_toList l, foldr_cons_eq_toList r, ← List.cons_append,
    ← List.append_assoc, ← foldr_cons_eq_toList l]

Result:
α : Type u_1
size✝ : ℕ
l : Ordnode α
x : α
r : Ordnode α
r' : List α
⊢ foldr List.cons l (x :: r.toList) ++ r' = (node size✝ l x r).toList ++ r'

Proof state:
α : Type u_1
size✝ : ℕ
l : Ordnode α
x : α
r : Ordnode α
r' : List α
⊢ foldr List.cons l (x :: r.toList) ++ r' = (node size✝ l x r).toList ++ r'

Tactic:
rfl

Result:
no goals
-- Mathlib/Data/Set/Basic.lean
theorem not_subset : ¬s ⊆ t ↔ ∃ a ∈ s, a ∉ t

Proof state:
α : Type u
s t : Set α
⊢ ¬s ⊆ t ↔ ∃ a ∈ s, a ∉ t

Tactic:
simp only [subset_def, not_forall, exists_prop]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/IsLimit.lean
theorem lift_comp_conePointUniqueUpToIso_inv {r s t : Cone F} (P : IsLimit s) (Q : IsLimit t) :
    Q.lift r ≫ (conePointUniqueUpToIso P Q).inv = P.lift r :=
  P.uniq _ _ (by simp)

Proof state:
J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
C : Type u₃
inst✝ : Category.{v₃, u₃} C
F : J ⥤ C
r s t : Cone F
P : IsLimit s
Q : IsLimit t
⊢ ∀ (j : J), (Q.lift r ≫ (P.conePointUniqueUpToIso Q).inv) ≫ s.π.app j = r.π.app j

Tactic:
simp

Result:
no goals
-- Mathlib/MeasureTheory/Measure/RegularityCompacts.lean
theorem innerRegularWRT_isCompact_closure_of_univ [TopologicalSpace α]
    (hμ : ∀ ε, 0 < ε → ∃ K, IsCompact (closure K) ∧ μ (Kᶜ) < ε) :
    μ.InnerRegularWRT (IsCompact ∘ closure) IsClosed

Proof state:
α : Type u_1
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : TopologicalSpace α
hμ : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ K, IsCompact (closure K) ∧ μ Kᶜ < ε
⊢ μ.InnerRegularWRT (IsCompact ∘ closure) IsClosed

Tactic:
refine innerRegularWRT_of_exists_compl_lt (fun s t hs ht ↦ ?_) hμ

Result:
α : Type u_1
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : TopologicalSpace α
hμ : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ K, IsCompact (closure K) ∧ μ Kᶜ < ε
s t : Set α
hs : (IsCompact ∘ closure) s
ht : IsClosed t
⊢ (IsCompact ∘ closure) (s ∩ t)

Proof state:
α : Type u_1
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : TopologicalSpace α
hμ : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ K, IsCompact (closure K) ∧ μ Kᶜ < ε
s t : Set α
hs : (IsCompact ∘ closure) s
ht : IsClosed t
this : IsCompact (closure s ∩ t)
⊢ closure (s ∩ t) ⊆ closure s ∩ t

Tactic:
refine (closure_inter_subset_inter_closure _ _).trans_eq ?_

Result:
α : Type u_1
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : TopologicalSpace α
hμ : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ K, IsCompact (closure K) ∧ μ Kᶜ < ε
s t : Set α
hs : (IsCompact ∘ closure) s
ht : IsClosed t
this : IsCompact (closure s ∩ t)
⊢ closure s ∩ closure t = closure s ∩ t

Proof state:
α : Type u_1
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : TopologicalSpace α
hμ : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ K, IsCompact (closure K) ∧ μ Kᶜ < ε
s t : Set α
hs : (IsCompact ∘ closure) s
ht : IsClosed t
this : IsCompact (closure s ∩ t)
⊢ closure s ∩ closure t = closure s ∩ t

Tactic:
rw [IsClosed.closure_eq ht]

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : TopologicalSpace α
hμ : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ K, IsCompact (closure K) ∧ μ Kᶜ < ε
s t : Set α
hs : (IsCompact ∘ closure) s
ht : IsClosed t
this : IsCompact (closure s ∩ t)
⊢ (IsCompact ∘ closure) (s ∩ t)

Tactic:
refine this.of_isClosed_subset isClosed_closure ?_

Result:
α : Type u_1
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : TopologicalSpace α
hμ : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ K, IsCompact (closure K) ∧ μ Kᶜ < ε
s t : Set α
hs : (IsCompact ∘ closure) s
ht : IsClosed t
this : IsCompact (closure s ∩ t)
⊢ closure (s ∩ t) ⊆ closure s ∩ t

Proof state:
α : Type u_1
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : TopologicalSpace α
hμ : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ K, IsCompact (closure K) ∧ μ Kᶜ < ε
s t : Set α
hs : (IsCompact ∘ closure) s
ht : IsClosed t
⊢ (IsCompact ∘ closure) (s ∩ t)

Tactic:
have : IsCompact (closure s ∩ t) := hs.inter_right ht

Result:
α : Type u_1
inst✝¹ : MeasurableSpace α
μ : Measure α
inst✝ : TopologicalSpace α
hμ : ∀ (ε : ℝ≥0∞), 0 < ε → ∃ K, IsCompact (closure K) ∧ μ Kᶜ < ε
s t : Set α
hs : (IsCompact ∘ closure) s
ht : IsClosed t
this : IsCompact (closure s ∩ t)
⊢ (IsCompact ∘ closure) (s ∩ t)
-- Mathlib/Algebra/Polynomial/Degree/Operations.lean
theorem degree_add_eq_left_of_degree_lt (h : degree q < degree p) : degree (p + q) = degree p :=
  le_antisymm (max_eq_left_of_lt h ▸ degree_add_le _ _) <|
    degree_le_degree <| by
      rw [coeff_add, coeff_natDegree_eq_zero_of_degree_lt h, add_zero]
      exact mt leadingCoeff_eq_zero.1 (ne_zero_of_degree_gt h)

Proof state:
R : Type u
inst✝ : Semiring R
p q : R[X]
h : q.degree < p.degree
⊢ p.coeff p.natDegree ≠ 0

Tactic:
exact mt leadingCoeff_eq_zero.1 (ne_zero_of_degree_gt h)

Result:
no goals

Proof state:
R : Type u
inst✝ : Semiring R
p q : R[X]
h : q.degree < p.degree
⊢ (p + q).coeff p.natDegree ≠ 0

Tactic:
rw [coeff_add, coeff_natDegree_eq_zero_of_degree_lt h, add_zero]

Result:
R : Type u
inst✝ : Semiring R
p q : R[X]
h : q.degree < p.degree
⊢ p.coeff p.natDegree ≠ 0
-- Mathlib/Computability/PostTuringMachine.lean
theorem fun_respects {σ₁ σ₂ f₁ f₂} {tr : σ₁ → σ₂} :
    (Respects f₁ f₂ fun a b ↦ tr a = b) ↔ ∀ ⦃a₁⦄, FRespects f₂ tr (tr a₁) (f₁ a₁) :=
  forall_congr' fun a₁ ↦ by
    cases f₁ a₁ <;> simp only [FRespects, Respects, exists_eq_left', forall_eq']

Proof state:
σ₁ : Type u_1
σ₂ : Type u_2
f₁ : σ₁ → Option σ₁
f₂ : σ₂ → Option σ₂
tr : σ₁ → σ₂
a₁ : σ₁
⊢ (∀ ⦃a₂ : σ₂⦄,
      (fun a b => tr a = b) a₁ a₂ →
        match f₁ a₁ with
        | some b₁ => ∃ b₂, (fun a b => tr a = b) b₁ b₂ ∧ Reaches₁ f₂ a₂ b₂
        | none => f₂ a₂ = none) ↔
    FRespects f₂ tr (tr a₁) (f₁ a₁)

Tactic:
cases f₁ a₁ <;> simp only [FRespects, Respects, exists_eq_left', forall_eq']

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Bootstrap.lean
theorem foldr_eq_foldr_toList
    (f : α → β → β) (init : β) (arr : Array α) :
    arr.foldr f init = arr.toList.foldr f init

Proof state:
α : Type u_1
β : Type u_2
f : α → β → β
init : β
arr : Array α
⊢ foldr f init arr = List.foldr f init arr.toList

Tactic:
simp

Result:
no goals