harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Topology/TietzeExtension.lean
theorem tietze_extension_step (f : X →ᵇ ℝ) (e : C(X, Y)) (he : IsClosedEmbedding e) :
    ∃ g : Y →ᵇ ℝ, ‖g‖ ≤ ‖f‖ / 3 ∧ dist (g.compContinuous e) f ≤ 2 / 3 * ‖f‖

Proof state:
case inr.intro.intro.intro.refine_1
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : NormalSpace Y
f : X →ᵇ ℝ
e : C(X, Y)
he : IsClosedEmbedding ⇑e
h3 : 0 < 3
h23 : 0 < 2 / 3
hf : 0 < ‖f‖
hf3 : -‖f‖ / 3 < ‖f‖ / 3
hc₁ : IsClosed (⇑e '' (⇑f ⁻¹' Iic (-‖f‖ / 3)))
hc₂ : IsClosed (⇑e '' (⇑f ⁻¹' Ici (‖f‖ / 3)))
hd : Disjoint (⇑e '' (⇑f ⁻¹' Iic (-‖f‖ / 3))) (⇑e '' (⇑f ⁻¹' Ici (‖f‖ / 3)))
g : Y →ᵇ ℝ
hg₁ : EqOn (⇑g) (Function.const Y (-‖f‖ / 3)) (⇑e '' (⇑f ⁻¹' Iic (-‖f‖ / 3)))
hg₂ : EqOn (⇑g) (Function.const Y (‖f‖ / 3)) (⇑e '' (⇑f ⁻¹' Ici (‖f‖ / 3)))
hgf : ∀ (x : Y), g x ∈ Icc (-‖f‖ / 3) (‖f‖ / 3)
⊢ ‖g‖ ≤ ‖f‖ / 3

Tactic:
refine (norm_le <| div_nonneg hf.le h3.le).mpr fun y => ?_

Result:
case inr.intro.intro.intro.refine_1
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : NormalSpace Y
f : X →ᵇ ℝ
e : C(X, Y)
he : IsClosedEmbedding ⇑e
h3 : 0 < 3
h23 : 0 < 2 / 3
hf : 0 < ‖f‖
hf3 : -‖f‖ / 3 < ‖f‖ / 3
hc₁ : IsClosed (⇑e '' (⇑f ⁻¹' Iic (-‖f‖ / 3)))
hc₂ : IsClosed (⇑e '' (⇑f ⁻¹' Ici (‖f‖ / 3)))
hd : Disjoint (⇑e '' (⇑f ⁻¹' Iic (-‖f‖ / 3))) (⇑e '' (⇑f ⁻¹' Ici (‖f‖ / 3)))
g : Y →ᵇ ℝ
hg₁ : EqOn (⇑g) (Function.const Y (-‖f‖ / 3)) (⇑e '' (⇑f ⁻¹' Iic (-‖f‖ / 3)))
hg₂ : EqOn (⇑g) (Function.const Y (‖f‖ / 3)) (⇑e '' (⇑f ⁻¹' Ici (‖f‖ / 3)))
hgf : ∀ (x : Y), g x ∈ Icc (-‖f‖ / 3) (‖f‖ / 3)
y : Y
⊢ ‖g y‖ ≤ ‖f‖ / 3
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Nat/TakeDrop.lean
theorem take_take : ∀ (n m) (l : List α), take n (take m l) = take (min n m) l
  | n, 0, l => by rw [Nat.min_zero, take_zero, take_nil]
  | 0, m, l => by rw [Nat.zero_min, take_zero, take_zero]
  | succ n, succ m, nil => by simp only [take_nil]
  | succ n, succ m, a :: l => by
    simp only [take, succ_min_succ, take_take n m l]

Proof state:
α : Type u_1
n m : Nat
a : α
l : List α
⊢ take n.succ (take m.succ (a :: l)) = take (min n.succ m.succ) (a :: l)

Tactic:
simp only [take, succ_min_succ, take_take n m l]

Result:
no goals

Proof state:
α : Type u_1
n : Nat
l : List α
⊢ take n (take 0 l) = take (min n 0) l

Tactic:
rw [Nat.min_zero, take_zero, take_nil]

Result:
no goals

Proof state:
α : Type u_1
n m : Nat
⊢ take n.succ (take m.succ []) = take (min n.succ m.succ) []

Tactic:
simp only [take_nil]

Result:
no goals

Proof state:
α : Type u_1
m : Nat
l : List α
⊢ take 0 (take m l) = take (min 0 m) l

Tactic:
rw [Nat.zero_min, take_zero, take_zero]

Result:
no goals
-- Mathlib/Control/Traversable/Basic.lean
theorem preserves_map' {α β} (x : α → β) : @η _ ∘ Functor.map x = Functor.map x ∘ @η _

Proof state:
F : Type u → Type v
inst✝³ : Applicative F
G : Type u → Type w
inst✝² : Applicative G
η : ApplicativeTransformation F G
inst✝¹ : LawfulApplicative F
inst✝ : LawfulApplicative G
α β : Type u
x : α → β
⊢ (fun {α} => η.app α) ∘ Functor.map x = Functor.map x ∘ fun {α} => η.app α

Tactic:
ext y

Result:
case h
F : Type u → Type v
inst✝³ : Applicative F
G : Type u → Type w
inst✝² : Applicative G
η : ApplicativeTransformation F G
inst✝¹ : LawfulApplicative F
inst✝ : LawfulApplicative G
α β : Type u
x : α → β
y : F α
⊢ ((fun {α} => η.app α) ∘ Functor.map x) y = (Functor.map x ∘ fun {α} => η.app α) y

Proof state:
case h
F : Type u → Type v
inst✝³ : Applicative F
G : Type u → Type w
inst✝² : Applicative G
η : ApplicativeTransformation F G
inst✝¹ : LawfulApplicative F
inst✝ : LawfulApplicative G
α β : Type u
x : α → β
y : F α
⊢ ((fun {α} => η.app α) ∘ Functor.map x) y = (Functor.map x ∘ fun {α} => η.app α) y

Tactic:
exact preserves_map η x y

Result:
no goals
-- Mathlib/Algebra/Homology/HomotopyCategory/HomComplexShift.lean
@[simp]
lemma rightShift_zero (a n' : ℤ) (hn' : n' + a = n) :
    (0 : Cochain K L n).rightShift a n' hn' = 0

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
n a n' : ℤ
hn' : n' + a = n
⊢ (rightShiftAddEquiv K L n a n' hn') 0 = 0

Tactic:
apply _root_.map_zero

Result:
no goals

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
n a n' : ℤ
hn' : n' + a = n
⊢ rightShift 0 a n' hn' = 0

Tactic:
change rightShiftAddEquiv K L n a n' hn' 0 = 0

Result:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
K L : CochainComplex C ℤ
n a n' : ℤ
hn' : n' + a = n
⊢ (rightShiftAddEquiv K L n a n' hn') 0 = 0
-- Mathlib/Combinatorics/SimpleGraph/Matching.lean
lemma IsCycles.reachable_deleteEdges [Finite V] (hadj : G.Adj v w)
    (hcyc : G.IsCycles) : (G.deleteEdges {s(v, w)}).Reachable v w

Proof state:
V : Type u_1
G : SimpleGraph V
v w : V
inst✝ : Finite V
hadj : G.Adj v w
hcyc : G.IsCycles
⊢ fromEdgeSet {s(v, w)} = (G.subgraphOfAdj hadj).spanningCoe

Tactic:
exact (Subgraph.spanningCoe_subgraphOfAdj hadj).symm

Result:
no goals

Proof state:
V : Type u_1
G : SimpleGraph V
v w : V
inst✝ : Finite V
hadj : G.Adj v w
hcyc : G.IsCycles
⊢ fromEdgeSet {s(v, w)} = hadj.toWalk.toSubgraph.spanningCoe

Tactic:
simp only [Walk.toSubgraph, singletonSubgraph_le_iff, subgraphOfAdj_verts, Set.mem_insert_iff,
  Set.mem_singleton_iff, or_true, sup_of_le_left]

Result:
V : Type u_1
G : SimpleGraph V
v w : V
inst✝ : Finite V
hadj : G.Adj v w
hcyc : G.IsCycles
⊢ fromEdgeSet {s(v, w)} = (G.subgraphOfAdj hadj).spanningCoe

Proof state:
V : Type u_1
G : SimpleGraph V
v w : V
inst✝ : Finite V
hadj : G.Adj v w
hcyc : G.IsCycles
this : fromEdgeSet {s(v, w)} = hadj.toWalk.toSubgraph.spanningCoe
⊢ G.deleteEdges {s(v, w)} = G \ fromEdgeSet {s(v, w)}

Tactic:
rfl

Result:
no goals

Proof state:
V : Type u_1
G : SimpleGraph V
v w : V
inst✝ : Finite V
hadj : G.Adj v w
hcyc : G.IsCycles
this : fromEdgeSet {s(v, w)} = hadj.toWalk.toSubgraph.spanningCoe
⊢ (G \ fromEdgeSet {s(v, w)}).Reachable v w

Tactic:
exact this ▸ (hcyc.reachable_sdiff_toSubgraph_spanningCoe hadj.toWalk
  (Walk.IsPath.of_adj hadj)).symm

Result:
no goals

Proof state:
V : Type u_1
G : SimpleGraph V
v w : V
inst✝ : Finite V
hadj : G.Adj v w
hcyc : G.IsCycles
⊢ (G.deleteEdges {s(v, w)}).Reachable v w

Tactic:
have : fromEdgeSet {s(v, w)} = hadj.toWalk.toSubgraph.spanningCoe := by
  simp only [Walk.toSubgraph, singletonSubgraph_le_iff, subgraphOfAdj_verts, Set.mem_insert_iff,
    Set.mem_singleton_iff, or_true, sup_of_le_left]
  exact (Subgraph.spanningCoe_subgraphOfAdj hadj).symm

Result:
V : Type u_1
G : SimpleGraph V
v w : V
inst✝ : Finite V
hadj : G.Adj v w
hcyc : G.IsCycles
this : fromEdgeSet {s(v, w)} = hadj.toWalk.toSubgraph.spanningCoe
⊢ (G.deleteEdges {s(v, w)}).Reachable v w

Proof state:
V : Type u_1
G : SimpleGraph V
v w : V
inst✝ : Finite V
hadj : G.Adj v w
hcyc : G.IsCycles
this : fromEdgeSet {s(v, w)} = hadj.toWalk.toSubgraph.spanningCoe
⊢ (G.deleteEdges {s(v, w)}).Reachable v w

Tactic:
rw [show G.deleteEdges {s(v, w)} = G \ fromEdgeSet {s(v, w)} from by rfl]

Result:
V : Type u_1
G : SimpleGraph V
v w : V
inst✝ : Finite V
hadj : G.Adj v w
hcyc : G.IsCycles
this : fromEdgeSet {s(v, w)} = hadj.toWalk.toSubgraph.spanningCoe
⊢ (G \ fromEdgeSet {s(v, w)}).Reachable v w
-- Mathlib/MeasureTheory/Measure/NullMeasurable.lean
lemma measure_of_measure_compl_eq_zero (hs : μ sᶜ = 0) : μ s = μ Set.univ

Proof state:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : μ sᶜ = 0
⊢ μ s = μ univ

Tactic:
simpa [hs] using measure_add_measure_compl₀ <| .of_compl <| .of_null hs

Result:
no goals
-- Mathlib/CategoryTheory/Preadditive/Biproducts.lean
theorem Biprod.inr_ofComponents :
    biprod.inr ≫ Biprod.ofComponents f₁₁ f₁₂ f₂₁ f₂₂ = f₂₁ ≫ biprod.inl + f₂₂ ≫ biprod.inr

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : Preadditive C
inst✝ : HasBinaryBiproducts C
X₁ X₂ Y₁ Y₂ : C
f₁₁ : X₁ ⟶ Y₁
f₁₂ : X₁ ⟶ Y₂
f₂₁ : X₂ ⟶ Y₁
f₂₂ : X₂ ⟶ Y₂
⊢ biprod.inr ≫ ofComponents f₁₁ f₁₂ f₂₁ f₂₂ = f₂₁ ≫ biprod.inl + f₂₂ ≫ biprod.inr

Tactic:
simp [Biprod.ofComponents]

Result:
no goals
-- Mathlib/Order/Filter/Extr.lean
theorem IsExtrFilter.congr {α β : Type*} [Preorder β] {f g : α → β} {a : α} {l : Filter α}
    (h : IsExtrFilter f l a) (heq : f =ᶠ[l] g) (hfga : f a = g a) : IsExtrFilter g l a

Proof state:
α : Type u_1
β : Type u_2
inst✝ : Preorder β
f g : α → β
a : α
l : Filter α
h : IsMinFilter f l a ∨ IsMaxFilter f l a
heq : f =ᶠ[l] g
hfga : f a = g a
⊢ IsMinFilter g l a ∨ IsMaxFilter g l a

Tactic:
rwa [← heq.isMaxFilter_iff hfga, ← heq.isMinFilter_iff hfga]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝ : Preorder β
f g : α → β
a : α
l : Filter α
h : IsExtrFilter f l a
heq : f =ᶠ[l] g
hfga : f a = g a
⊢ IsExtrFilter g l a

Tactic:
rw [IsExtrFilter] at *

Result:
α : Type u_1
β : Type u_2
inst✝ : Preorder β
f g : α → β
a : α
l : Filter α
h : IsMinFilter f l a ∨ IsMaxFilter f l a
heq : f =ᶠ[l] g
hfga : f a = g a
⊢ IsMinFilter g l a ∨ IsMaxFilter g l a
-- Mathlib/ModelTheory/Ultraproducts.lean
theorem sentence_realize (φ : L.Sentence) :
    (u : Filter α).Product M ⊨ φ ↔ ∀ᶠ a : α in u, M a ⊨ φ

Proof state:
α : Type u_1
M : α → Type u_2
u : Ultrafilter α
L : Language
inst✝¹ : (a : α) → L.Structure (M a)
inst✝ : ∀ (a : α), Nonempty (M a)
φ : L.Sentence
⊢ Formula.Realize φ default = Formula.Realize φ fun i => Quotient.mk' fun a => default i

Tactic:
exact congr rfl (Subsingleton.elim _ _)

Result:
no goals

Proof state:
α : Type u_1
M : α → Type u_2
u : Ultrafilter α
L : Language
inst✝¹ : (a : α) → L.Structure (M a)
inst✝ : ∀ (a : α), Nonempty (M a)
φ : L.Sentence
⊢ (↑u).Product M ⊨ φ ↔ ∀ᶠ (a : α) in ↑u, M a ⊨ φ

Tactic:
simp_rw [Sentence.Realize]

Result:
α : Type u_1
M : α → Type u_2
u : Ultrafilter α
L : Language
inst✝¹ : (a : α) → L.Structure (M a)
inst✝ : ∀ (a : α), Nonempty (M a)
φ : L.Sentence
⊢ Formula.Realize φ default ↔ ∀ᶠ (a : α) in ↑u, Formula.Realize φ default

Proof state:
α : Type u_1
M : α → Type u_2
u : Ultrafilter α
L : Language
inst✝¹ : (a : α) → L.Structure (M a)
inst✝ : ∀ (a : α), Nonempty (M a)
φ : L.Sentence
⊢ Formula.Realize φ default ↔ ∀ᶠ (a : α) in ↑u, Formula.Realize φ default

Tactic:
rw [← realize_formula_cast φ, iff_eq_eq]

Result:
α : Type u_1
M : α → Type u_2
u : Ultrafilter α
L : Language
inst✝¹ : (a : α) → L.Structure (M a)
inst✝ : ∀ (a : α), Nonempty (M a)
φ : L.Sentence
⊢ Formula.Realize φ default = Formula.Realize φ fun i => Quotient.mk' fun a => default i
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Erase.lean
theorem eraseP_map (f : β → α) : ∀ (l : List β), (map f l).eraseP p = map f (l.eraseP (p ∘ f))
  | [] => rfl
  | b::l => by by_cases h : p (f b) <;> simp [h, eraseP_map f l, eraseP_cons_of_pos]

Proof state:
β : Type u_1
α : Type u_2
p : α → Bool
f : β → α
b : β
l : List β
⊢ eraseP p (map f (b :: l)) = map f (eraseP (p ∘ f) (b :: l))

Tactic:
by_cases h : p (f b) <;> simp [h, eraseP_map f l, eraseP_cons_of_pos]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/TakeDrop.lean
theorem take_append_getLast? (l : List α) :
    (l.take (l.length - 1)) ++ l.getLast?.toList = l

Proof state:
α : Type u_1
l : List α
⊢ take (l.length - 1) l ++ l.getLast?.toList = l

Tactic:
match l with
| [] => simp
| x :: xs =>
  simpa using take_append_getLast (x :: xs) (by simp)

Result:
no goals

Proof state:
α : Type u_1
l : List α
x : α
xs : List α
⊢ x :: xs ≠ []

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
l : List α
⊢ take ([].length - 1) [] ++ [].getLast?.toList = []

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
l : List α
x : α
xs : List α
⊢ take ((x :: xs).length - 1) (x :: xs) ++ (x :: xs).getLast?.toList = x :: xs

Tactic:
simpa using take_append_getLast (x :: xs) (by simp)

Result:
no goals
-- Mathlib/Algebra/Homology/Embedding/Basic.lean
lemma not_mem_range_embeddingUpIntGE_iff (n : ℤ) :
    (∀ (i : ℕ), (embeddingUpIntGE p).f i ≠ n) ↔ n < p

Proof state:
p n : ℤ
⊢ (∀ (i : ℕ), (embeddingUpIntGE p).f i ≠ n) ↔ n < p

Tactic:
constructor

Result:
case mp
p n : ℤ
⊢ (∀ (i : ℕ), (embeddingUpIntGE p).f i ≠ n) → n < p

case mpr
p n : ℤ
⊢ n < p → ∀ (i : ℕ), (embeddingUpIntGE p).f i ≠ n

Proof state:
case mp
p n : ℤ
⊢ (∀ (i : ℕ), (embeddingUpIntGE p).f i ≠ n) → n < p

Tactic:
intro h

Result:
case mp
p n : ℤ
h : ∀ (i : ℕ), (embeddingUpIntGE p).f i ≠ n
⊢ n < p

Proof state:
p n : ℤ
h : ∀ (i : ℕ), (embeddingUpIntGE p).f i ≠ n
this : ¬n < p
⊢ (embeddingUpIntGE p).f (n - p).natAbs = n

Tactic:
simp

Result:
p n : ℤ
h : ∀ (i : ℕ), (embeddingUpIntGE p).f i ≠ n
this : ¬n < p
⊢ p + ↑(n - p).natAbs = n

Proof state:
case mp
p n : ℤ
h : ∀ (i : ℕ), (embeddingUpIntGE p).f i ≠ n
this : ¬n < p
⊢ False

Tactic:
exact h (n - p).natAbs (by simp; omega)

Result:
no goals

Proof state:
case mpr
p n : ℤ
a✝ : n < p
i✝ : ℕ
⊢ (embeddingUpIntGE p).f i✝ ≠ n

Tactic:
dsimp

Result:
case mpr
p n : ℤ
a✝ : n < p
i✝ : ℕ
⊢ ¬p + ↑i✝ = n

Proof state:
case mpr
p n : ℤ
a✝ : n < p
i✝ : ℕ
⊢ ¬p + ↑i✝ = n

Tactic:
omega

Result:
no goals

Proof state:
case mp
p n : ℤ
h : ∀ (i : ℕ), (embeddingUpIntGE p).f i ≠ n
⊢ n < p

Tactic:
by_contra!

Result:
case mp
p n : ℤ
h : ∀ (i : ℕ), (embeddingUpIntGE p).f i ≠ n
this : ¬n < p
⊢ False

Proof state:
case mpr
p n : ℤ
⊢ n < p → ∀ (i : ℕ), (embeddingUpIntGE p).f i ≠ n

Tactic:
intros

Result:
case mpr
p n : ℤ
a✝ : n < p
i✝ : ℕ
⊢ (embeddingUpIntGE p).f i✝ ≠ n

Proof state:
p n : ℤ
h : ∀ (i : ℕ), (embeddingUpIntGE p).f i ≠ n
this : ¬n < p
⊢ p + ↑(n - p).natAbs = n

Tactic:
omega

Result:
no goals
-- Mathlib/MeasureTheory/Decomposition/Lebesgue.lean
theorem eq_singularPart {s : Measure α} {f : α → ℝ≥0∞} (hf : Measurable f) (hs : s ⟂ₘ ν)
    (hadd : μ = s + ν.withDensity f) : s = μ.singularPart ν

Proof state:
α : Type u_1
m : MeasurableSpace α
μ ν s : Measure α
f : α → ℝ≥0∞
hf : Measurable f
hadd : μ.singularPart ν + ν.withDensity (μ.rnDeriv ν) = s + ν.withDensity f
this : μ.HaveLebesgueDecomposition ν
hmeas : Measurable (μ.rnDeriv ν)
hadd' : μ = μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)
S : Set α
hS₁ : MeasurableSet S
hS₂ : s S = 0
hS₃ : ν Sᶜ = 0
T : Set α
hT₁ : MeasurableSet T
hT₂ : (μ.singularPart ν) T = 0
hT₃ : ν Tᶜ = 0
hνinter : ν (S ∩ T)ᶜ = 0
heq : s.restrict (S ∩ T)ᶜ = (μ.singularPart ν).restrict (S ∩ T)ᶜ
heq' : ∀ (A : Set α), MeasurableSet A → s A = (s.restrict (S ∩ T)ᶜ) A
A : Set α
hA : MeasurableSet A
⊢ (μ.singularPart ν) (A ∩ (S ∩ T)) ≤ 0

Tactic:
exact hT₂ ▸ measure_mono (inter_subset_right.trans inter_subset_right)

Result:
no goals

Proof state:
case intro.intro.intro.intro.intro.intro.intro.intro.h
α : Type u_1
m : MeasurableSpace α
μ ν s : Measure α
f : α → ℝ≥0∞
hf : Measurable f
hadd : μ.singularPart ν + ν.withDensity (μ.rnDeriv ν) = s + ν.withDensity f
this : μ.HaveLebesgueDecomposition ν
hmeas : Measurable (μ.rnDeriv ν)
hadd' : μ = μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)
S : Set α
hS₁ : MeasurableSet S
hS₂ : s S = 0
hS₃ : ν Sᶜ = 0
T : Set α
hT₁ : MeasurableSet T
hT₂ : (μ.singularPart ν) T = 0
hT₃ : ν Tᶜ = 0
hνinter : ν (S ∩ T)ᶜ = 0
heq : s.restrict (S ∩ T)ᶜ = (μ.singularPart ν).restrict (S ∩ T)ᶜ
heq' : ∀ (A : Set α), MeasurableSet A → s A = (s.restrict (S ∩ T)ᶜ) A
A : Set α
hA : MeasurableSet A
⊢ s A = (μ.singularPart ν) A

Tactic:
have hμinter : μ.singularPart ν (A ∩ (S ∩ T)) = 0 := by
  rw [← nonpos_iff_eq_zero]
  exact hT₂ ▸ measure_mono (inter_subset_right.trans inter_subset_right)

Result:
case intro.intro.intro.intro.intro.intro.intro.intro.h
α : Type u_1
m : MeasurableSpace α
μ ν s : Measure α
f : α → ℝ≥0∞
hf : Measurable f
hadd : μ.singularPart ν + ν.withDensity (μ.rnDeriv ν) = s + ν.withDensity f
this : μ.HaveLebesgueDecomposition ν
hmeas : Measurable (μ.rnDeriv ν)
hadd' : μ = μ.singularPart ν + ν.withDensity (μ.rnDeriv ν)
S : Set α
hS₁ : MeasurableSet S
hS₂ : s S = 0
hS₃ : ν Sᶜ = 0
T : Set α
hT₁ : MeasurableSet T
hT₂ : (μ.singularPart ν) T = 0
hT₃ : ν Tᶜ = 0
hνinter : ν (S ∩ T)ᶜ = 0
heq : s.restrict (S ∩ T)ᶜ = (μ.singularPart ν).restrict (S ∩ T)ᶜ
heq' : ∀ (A : Set α), MeasurableSet A → s A = (s.restrict (S ∩ T)ᶜ) A
A : Set α
hA : MeasurableSet A
hμinter : (μ.singularPart ν) (A ∩ (S ∩ T)) = 0
⊢ s A = (μ.singularPart ν) A
-- Mathlib/Order/Filter/Finite.lean
theorem iInf_principal_finite {ι : Type w} {s : Set ι} (hs : s.Finite) (f : ι → Set α) :
    ⨅ i ∈ s, 𝓟 (f i) = 𝓟 (⋂ i ∈ s, f i)

Proof state:
α : Type u
ι : Type w
s : Set ι
hs : s.Finite
f : ι → Set α
⊢ ⨅ i ∈ s, 𝓟 (f i) = 𝓟 (⋂ i ∈ s, f i)

Tactic:
lift s to Finset ι using hs

Result:
case intro
α : Type u
ι : Type w
f : ι → Set α
s : Finset ι
⊢ ⨅ i ∈ ↑s, 𝓟 (f i) = 𝓟 (⋂ i ∈ ↑s, f i)

Proof state:
case intro
α : Type u
ι : Type w
f : ι → Set α
s : Finset ι
⊢ ⨅ i ∈ ↑s, 𝓟 (f i) = 𝓟 (⋂ i ∈ ↑s, f i)

Tactic:
exact mod_cast iInf_principal_finset s f

Result:
no goals
-- Mathlib/Analysis/Analytic/Basic.lean
theorem radius_neg (p : FormalMultilinearSeries 𝕜 E F) : (-p).radius = p.radius

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
⊢ (-p).radius = p.radius

Tactic:
simp only [radius, neg_apply, norm_neg]

Result:
no goals
-- Mathlib/Analysis/Convex/Strong.lean
lemma UniformConcaveOn.mono (hψφ : ψ ≤ φ) (hf : UniformConcaveOn s φ f) : UniformConcaveOn s ψ f :=
  ⟨hf.1, fun x hx y hy a b ha hb hab ↦ (hf.2 hx hy ha hb hab).trans' <| by gcongr; apply hψφ⟩

Proof state:
case bc.h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
φ ψ : ℝ → ℝ
s : Set E
f : E → ℝ
hψφ : ψ ≤ φ
hf : UniformConcaveOn s φ f
x : E
hx : x ∈ s
y : E
hy : y ∈ s
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ ψ ‖x - y‖ ≤ φ ‖x - y‖

Tactic:
apply hψφ

Result:
no goals

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
φ ψ : ℝ → ℝ
s : Set E
f : E → ℝ
hψφ : ψ ≤ φ
hf : UniformConcaveOn s φ f
x : E
hx : x ∈ s
y : E
hy : y ∈ s
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ a • f x + b • f y + a * b * ψ ‖x - y‖ ≤ a • f x + b • f y + a * b * φ ‖x - y‖

Tactic:
gcongr

Result:
case bc.h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
φ ψ : ℝ → ℝ
s : Set E
f : E → ℝ
hψφ : ψ ≤ φ
hf : UniformConcaveOn s φ f
x : E
hx : x ∈ s
y : E
hy : y ∈ s
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
⊢ ψ ‖x - y‖ ≤ φ ‖x - y‖
-- Mathlib/CategoryTheory/MorphismProperty/Retract.lean
lemma isStableUnderRetracts_iff_retracts_le (P : MorphismProperty C) :
    P.IsStableUnderRetracts ↔ P.retracts ≤ P

Proof state:
case mpr
C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
⊢ P.retracts ≤ P → ∀ {X Y Z W : C} {f : X ⟶ Y} {g : Z ⟶ W}, RetractArrow f g → P g → P f

Tactic:
intro h₁ _ _ _ _ _ _ h₂ h₃

Result:
case mpr
C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
h₁ : P.retracts ≤ P
X✝ Y✝ Z✝ W✝ : C
f✝ : X✝ ⟶ Y✝
g✝ : Z✝ ⟶ W✝
h₂ : RetractArrow f✝ g✝
h₃ : P g✝
⊢ P f✝

Proof state:
case mp
C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
⊢ (∀ {X Y Z W : C} {f : X ⟶ Y} {g : Z ⟶ W}, RetractArrow f g → P g → P f) → P.retracts ≤ P

Tactic:
intro h₁ X Y f ⟨_, _, _, h₂, h₃⟩

Result:
case mp
C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
h₁ : ∀ {X Y Z W : C} {f : X ⟶ Y} {g : Z ⟶ W}, RetractArrow f g → P g → P f
X Y : C
f : X ⟶ Y
w✝² w✝¹ : C
w✝ : w✝² ⟶ w✝¹
h₂ : RetractArrow f w✝
h₃ : P w✝
⊢ P f

Proof state:
C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
⊢ P.IsStableUnderRetracts ↔ P.retracts ≤ P

Tactic:
rw [isStableUnderRetracts_iff]

Result:
C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
⊢ (∀ {X Y Z W : C} {f : X ⟶ Y} {g : Z ⟶ W}, RetractArrow f g → P g → P f) ↔ P.retracts ≤ P

Proof state:
case mp
C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
h₁ : ∀ {X Y Z W : C} {f : X ⟶ Y} {g : Z ⟶ W}, RetractArrow f g → P g → P f
X Y : C
f : X ⟶ Y
w✝² w✝¹ : C
w✝ : w✝² ⟶ w✝¹
h₂ : RetractArrow f w✝
h₃ : P w✝
⊢ P f

Tactic:
exact h₁ h₂ h₃

Result:
no goals

Proof state:
C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
⊢ (∀ {X Y Z W : C} {f : X ⟶ Y} {g : Z ⟶ W}, RetractArrow f g → P g → P f) ↔ P.retracts ≤ P

Tactic:
constructor

Result:
case mp
C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
⊢ (∀ {X Y Z W : C} {f : X ⟶ Y} {g : Z ⟶ W}, RetractArrow f g → P g → P f) → P.retracts ≤ P

case mpr
C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
⊢ P.retracts ≤ P → ∀ {X Y Z W : C} {f : X ⟶ Y} {g : Z ⟶ W}, RetractArrow f g → P g → P f

Proof state:
case mpr
C : Type u
inst✝ : Category.{v, u} C
P : MorphismProperty C
h₁ : P.retracts ≤ P
X✝ Y✝ Z✝ W✝ : C
f✝ : X✝ ⟶ Y✝
g✝ : Z✝ ⟶ W✝
h₂ : RetractArrow f✝ g✝
h₃ : P g✝
⊢ P f✝

Tactic:
exact h₁ _ ⟨_, _, _, h₂, h₃⟩

Result:
no goals
-- Mathlib/Algebra/PresentedMonoid/Basic.lean
theorem closure_range_of (rels : FreeMonoid α → FreeMonoid α → Prop) :
    Submonoid.closure (Set.range (PresentedMonoid.of rels)) = ⊤

Proof state:
case h.of
α : Type u_2
rels : FreeMonoid α → FreeMonoid α → Prop
x : α
⊢ (mk rels) (FreeMonoid.of x) ∈ closure (range (of rels))

Tactic:
exact subset_closure (Exists.intro x rfl)

Result:
no goals

Proof state:
α : Type u_2
rels : FreeMonoid α → FreeMonoid α → Prop
x : PresentedMonoid rels
⊢ x ∈ closure (range (of rels))

Tactic:
induction' x with a

Result:
case h
α : Type u_2
rels : FreeMonoid α → FreeMonoid α → Prop
a : FreeMonoid α
⊢ (mk rels) a ∈ closure (range (of rels))

Proof state:
α : Type u_2
rels : FreeMonoid α → FreeMonoid α → Prop
⊢ ∀ (x : PresentedMonoid rels), x ∈ closure (range (of rels))

Tactic:
intro x

Result:
α : Type u_2
rels : FreeMonoid α → FreeMonoid α → Prop
x : PresentedMonoid rels
⊢ x ∈ closure (range (of rels))

Proof state:
α : Type u_2
rels : FreeMonoid α → FreeMonoid α → Prop
⊢ closure (range (of rels)) = ⊤

Tactic:
rw [Submonoid.eq_top_iff']

Result:
α : Type u_2
rels : FreeMonoid α → FreeMonoid α → Prop
⊢ ∀ (x : PresentedMonoid rels), x ∈ closure (range (of rels))

Proof state:
case h.of
α : Type u_2
rels : FreeMonoid α → FreeMonoid α → Prop
x✝ : α
⊢ (mk rels) (FreeMonoid.of x✝) ∈ closure (range (of rels))

Tactic:
rename_i x

Result:
case h.of
α : Type u_2
rels : FreeMonoid α → FreeMonoid α → Prop
x : α
⊢ (mk rels) (FreeMonoid.of x) ∈ closure (range (of rels))

Proof state:
case h.mul
α : Type u_2
rels : FreeMonoid α → FreeMonoid α → Prop
x✝ y✝ : FreeMonoid α
a✝¹ : (mk rels) x✝ ∈ closure (range (of rels))
a✝ : (mk rels) y✝ ∈ closure (range (of rels))
⊢ (mk rels) (x✝ * y✝) ∈ closure (range (of rels))

Tactic:
rename_i x y hx hy

Result:
case h.mul
α : Type u_2
rels : FreeMonoid α → FreeMonoid α → Prop
x y : FreeMonoid α
hx : (mk rels) x ∈ closure (range (of rels))
hy : (mk rels) y ∈ closure (range (of rels))
⊢ (mk rels) (x * y) ∈ closure (range (of rels))

Proof state:
case h.mul
α : Type u_2
rels : FreeMonoid α → FreeMonoid α → Prop
x y : FreeMonoid α
hx : (mk rels) x ∈ closure (range (of rels))
hy : (mk rels) y ∈ closure (range (of rels))
⊢ (mk rels) (x * y) ∈ closure (range (of rels))

Tactic:
exact Submonoid.mul_mem _ hx hy

Result:
no goals

Proof state:
case h.one
α : Type u_2
rels : FreeMonoid α → FreeMonoid α → Prop
⊢ (mk rels) 1 ∈ closure (range (of rels))

Tactic:
exact Submonoid.one_mem _

Result:
no goals

Proof state:
case h
α : Type u_2
rels : FreeMonoid α → FreeMonoid α → Prop
a : FreeMonoid α
⊢ (mk rels) a ∈ closure (range (of rels))

Tactic:
induction a

Result:
case h.one
α : Type u_2
rels : FreeMonoid α → FreeMonoid α → Prop
⊢ (mk rels) 1 ∈ closure (range (of rels))

case h.of
α : Type u_2
rels : FreeMonoid α → FreeMonoid α → Prop
x✝ : α
⊢ (mk rels) (FreeMonoid.of x✝) ∈ closure (range (of rels))

case h.mul
α : Type u_2
rels : FreeMonoid α → FreeMonoid α → Prop
x✝ y✝ : FreeMonoid α
a✝¹ : (mk rels) x✝ ∈ closure (range (of rels))
a✝ : (mk rels) y✝ ∈ closure (range (of rels))
⊢ (mk rels) (x✝ * y✝) ∈ closure (range (of rels))