harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Probability/Kernel/RadonNikodym.lean
lemma withDensity_rnDeriv_mutuallySingularSetSlice (κ η : Kernel α γ) [IsFiniteKernel κ]
    [IsFiniteKernel η] (a : α) :
    withDensity η (rnDeriv κ η) a (mutuallySingularSetSlice κ η a) = 0

Proof state:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel η
a : α
⊢ ((η.withDensity (κ.rnDeriv η)) a) (κ.mutuallySingularSetSlice η a) = 0

Tactic:
rw [Kernel.withDensity_apply']

Result:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel η
a : α
⊢ ∫⁻ (b : γ) in κ.mutuallySingularSetSlice η a, κ.rnDeriv η a b ∂η a = 0

case hf
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel η
a : α
⊢ Measurable (Function.uncurry (κ.rnDeriv η))

Proof state:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel η
a : α
⊢ ∫⁻ (b : γ) in κ.mutuallySingularSetSlice η a, κ.rnDeriv η a b ∂η a = 0

Tactic:
exact setLIntegral_measure_zero _ _ (measure_mutuallySingularSetSlice κ η a)

Result:
no goals

Proof state:
case hf
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
inst✝¹ : IsFiniteKernel κ
inst✝ : IsFiniteKernel η
a : α
⊢ Measurable (Function.uncurry (κ.rnDeriv η))

Tactic:
exact measurable_rnDeriv κ η

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/OfFn.lean
theorem back_ofFn {n} [NeZero n](f : Fin n → α) :
    (ofFn f).back = f ⟨n - 1, by have := NeZero.ne n; omega⟩

Proof state:
α : Type u_1
n : Nat
inst✝ : NeZero n
f : Fin n → α
⊢ (ofFn f).back = f ⟨n - 1, ⋯⟩

Tactic:
simp [back]

Result:
no goals

Proof state:
α : Type ?u.2100
n : Nat
inst✝ : NeZero n
f : Fin n → α
this : n ≠ 0
⊢ n - 1 < n

Tactic:
omega

Result:
no goals

Proof state:
α : Type ?u.2100
n : Nat
inst✝ : NeZero n
f : Fin n → α
⊢ n - 1 < n

Tactic:
have := NeZero.ne n

Result:
α : Type ?u.2100
n : Nat
inst✝ : NeZero n
f : Fin n → α
this : n ≠ 0
⊢ n - 1 < n
-- Mathlib/Data/PFun.lean
theorem preimage_univ : f.preimage Set.univ = f.Dom

Proof state:
α : Type u_1
β : Type u_2
f : α →. β
⊢ f.preimage Set.univ = f.Dom

Tactic:
ext

Result:
case h
α : Type u_1
β : Type u_2
f : α →. β
x✝ : α
⊢ x✝ ∈ f.preimage Set.univ ↔ x✝ ∈ f.Dom

Proof state:
case h
α : Type u_1
β : Type u_2
f : α →. β
x✝ : α
⊢ x✝ ∈ f.preimage Set.univ ↔ x✝ ∈ f.Dom

Tactic:
simp [mem_preimage, mem_dom]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Attach.lean
theorem pmap_eq_self {l : List α} {p : α → Prop} {hp : ∀ (a : α), a ∈ l → p a}
    {f : (a : α) → p a → α} : l.pmap f hp = l ↔ ∀ a (h : a ∈ l), f a (hp a h) = a

Proof state:
α : Type u_1
l : List α
p : α → Prop
hp : ∀ (a : α), a ∈ l → p a
f : (a : α) → p a → α
⊢ map (fun x => f x.val ⋯) l.attach = map Subtype.val l.attach ↔ ∀ (a : α) (h : a ∈ l), f a ⋯ = a

Tactic:
rw [map_inj_left]

Result:
α : Type u_1
l : List α
p : α → Prop
hp : ∀ (a : α), a ∈ l → p a
f : (a : α) → p a → α
⊢ (∀ (a : { x // x ∈ l }), a ∈ l.attach → f a.val ⋯ = a.val) ↔ ∀ (a : α) (h : a ∈ l), f a ⋯ = a

Proof state:
α : Type u_1
l : List α
p : α → Prop
hp : ∀ (a : α), a ∈ l → p a
f : (a : α) → p a → α
⊢ (∀ (a : { x // x ∈ l }), a ∈ l.attach → f a.val ⋯ = a.val) ↔ ∀ (a : α) (h : a ∈ l), f a ⋯ = a

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
l : List α
p : α → Prop
hp : ∀ (a : α), a ∈ l → p a
f : (a : α) → p a → α
⊢ map (fun x => f x.val ⋯) l.attach = l ↔ ∀ (a : α) (h : a ∈ l), f a ⋯ = a

Tactic:
conv => lhs; rhs; rw [← attach_map_subtype_val l]

Result:
α : Type u_1
l : List α
p : α → Prop
hp : ∀ (a : α), a ∈ l → p a
f : (a : α) → p a → α
⊢ map (fun x => f x.val ⋯) l.attach = map Subtype.val l.attach ↔ ∀ (a : α) (h : a ∈ l), f a ⋯ = a

Proof state:
α : Type u_1
l : List α
p : α → Prop
hp : ∀ (a : α), a ∈ l → p a
f : (a : α) → p a → α
⊢ pmap f l hp = l ↔ ∀ (a : α) (h : a ∈ l), f a ⋯ = a

Tactic:
rw [pmap_eq_map_attach]

Result:
α : Type u_1
l : List α
p : α → Prop
hp : ∀ (a : α), a ∈ l → p a
f : (a : α) → p a → α
⊢ map (fun x => f x.val ⋯) l.attach = l ↔ ∀ (a : α) (h : a ∈ l), f a ⋯ = a
-- Mathlib/Analysis/SpecialFunctions/ImproperIntegrals.lean
theorem not_integrableOn_Ioi_cpow (s : ℂ) :
    ¬ IntegrableOn (fun x : ℝ ↦ (x : ℂ) ^ s) (Ioi (0 : ℝ))

Proof state:
s : ℂ
h : IntegrableOn (fun x => ↑x ^ s) (Ioi 0) volume
⊢ False

Tactic:
rcases le_or_lt s.re (-1) with hs|hs

Result:
case inl
s : ℂ
h : IntegrableOn (fun x => ↑x ^ s) (Ioi 0) volume
hs : s.re ≤ -1
⊢ False

case inr
s : ℂ
h : IntegrableOn (fun x => ↑x ^ s) (Ioi 0) volume
hs : -1 < s.re
⊢ False

Proof state:
s : ℂ
⊢ ¬IntegrableOn (fun x => ↑x ^ s) (Ioi 0) volume

Tactic:
intro h

Result:
s : ℂ
h : IntegrableOn (fun x => ↑x ^ s) (Ioi 0) volume
⊢ False

Proof state:
case inl
s : ℂ
h : IntegrableOn (fun x => ↑x ^ s) (Ioi 0) volume
hs : s.re ≤ -1
this : IntegrableOn (fun x => ↑x ^ s) (Ioo 0 1) volume
⊢ False

Tactic:
rw [integrableOn_Ioo_cpow_iff zero_lt_one] at this

Result:
case inl
s : ℂ
h : IntegrableOn (fun x => ↑x ^ s) (Ioi 0) volume
hs : s.re ≤ -1
this : -1 < s.re
⊢ False

Proof state:
case inr
s : ℂ
h : IntegrableOn (fun x => ↑x ^ s) (Ioi 0) volume
hs : -1 < s.re
this : IntegrableOn (fun x => ↑x ^ s) (Ioi 1) volume
⊢ False

Tactic:
rw [integrableOn_Ioi_cpow_iff zero_lt_one] at this

Result:
case inr
s : ℂ
h : IntegrableOn (fun x => ↑x ^ s) (Ioi 0) volume
hs : -1 < s.re
this : s.re < -1
⊢ False

Proof state:
case inl
s : ℂ
h : IntegrableOn (fun x => ↑x ^ s) (Ioi 0) volume
hs : s.re ≤ -1
this : -1 < s.re
⊢ False

Tactic:
exact hs.not_lt this

Result:
no goals

Proof state:
case inr
s : ℂ
h : IntegrableOn (fun x => ↑x ^ s) (Ioi 0) volume
hs : -1 < s.re
this : s.re < -1
⊢ False

Tactic:
exact hs.not_lt this

Result:
no goals

Proof state:
case inl
s : ℂ
h : IntegrableOn (fun x => ↑x ^ s) (Ioi 0) volume
hs : s.re ≤ -1
⊢ False

Tactic:
have : IntegrableOn (fun x : ℝ ↦ (x : ℂ) ^ s) (Ioo (0 : ℝ) 1) :=
  h.mono Ioo_subset_Ioi_self le_rfl

Result:
case inl
s : ℂ
h : IntegrableOn (fun x => ↑x ^ s) (Ioi 0) volume
hs : s.re ≤ -1
this : IntegrableOn (fun x => ↑x ^ s) (Ioo 0 1) volume
⊢ False

Proof state:
case inr
s : ℂ
h : IntegrableOn (fun x => ↑x ^ s) (Ioi 0) volume
hs : -1 < s.re
⊢ False

Tactic:
have : IntegrableOn (fun x : ℝ ↦ (x : ℂ) ^ s) (Ioi 1) :=
  h.mono (Ioi_subset_Ioi zero_le_one) le_rfl

Result:
case inr
s : ℂ
h : IntegrableOn (fun x => ↑x ^ s) (Ioi 0) volume
hs : -1 < s.re
this : IntegrableOn (fun x => ↑x ^ s) (Ioi 1) volume
⊢ False
-- Mathlib/Topology/Algebra/UniformGroup/Defs.lean
theorem Filter.HasBasis.uniformity_of_nhds_one_inv_mul_swapped {ι} {p : ι → Prop} {U : ι → Set α}
    (h : (𝓝 (1 : α)).HasBasis p U) :
    (𝓤 α).HasBasis p fun i => { x : α × α | x.2⁻¹ * x.1 ∈ U i }

Proof state:
α : Type u_1
inst✝² : UniformSpace α
inst✝¹ : Group α
inst✝ : UniformGroup α
ι : Sort u_3
p : ι → Prop
U : ι → Set α
h : (𝓝 1).HasBasis p U
⊢ (Filter.comap (fun x => x.2⁻¹ * x.1) (𝓝 1)).HasBasis p fun i => {x | x.2⁻¹ * x.1 ∈ U i}

Tactic:
exact h.comap _

Result:
no goals

Proof state:
α : Type u_1
inst✝² : UniformSpace α
inst✝¹ : Group α
inst✝ : UniformGroup α
ι : Sort u_3
p : ι → Prop
U : ι → Set α
h : (𝓝 1).HasBasis p U
⊢ (𝓤 α).HasBasis p fun i => {x | x.2⁻¹ * x.1 ∈ U i}

Tactic:
rw [uniformity_eq_comap_inv_mul_nhds_one_swapped]

Result:
α : Type u_1
inst✝² : UniformSpace α
inst✝¹ : Group α
inst✝ : UniformGroup α
ι : Sort u_3
p : ι → Prop
U : ι → Set α
h : (𝓝 1).HasBasis p U
⊢ (Filter.comap (fun x => x.2⁻¹ * x.1) (𝓝 1)).HasBasis p fun i => {x | x.2⁻¹ * x.1 ∈ U i}
-- Mathlib/RingTheory/Localization/Away/Basic.lean
theorem existsUnique_algebraMap_eq_of_span_eq_top (s : Set R) (span_eq : Ideal.span s = ⊤)
    (f : Π a : s, Away a.1) (h : ∀ a b : s,
      Away.awayToAwayRight (P := Away (a * b : R)) a.1 b (f a) = Away.awayToAwayLeft b.1 a (f b)) :
    ∃! r : R, ∀ a : s, algebraMap R _ r = f a

Proof state:
case inr
R : Type u_1
inst✝ : CommSemiring R
s : Set R
f : (a : ↑s) → Away ↑a
h : ∀ (a b : ↑s), (Away.awayToAwayRight ↑a ↑b) (f a) = (Away.awayToAwayLeft ↑b ↑a) (f b)
mem✝ : 1 ∈ Ideal.span s
this :
  ∀ (s : Set R) (f : (a : ↑s) → Away ↑a),
    (∀ (a b : ↑s), (Away.awayToAwayRight ↑a ↑b) (f a) = (Away.awayToAwayLeft ↑b ↑a) (f b)) →
      1 ∈ Ideal.span s → (∃ t, ↑t = s) → ∃! r, ∀ (a : ↑s), (algebraMap R (Away ↑a)) r = f a
finset_eq : ¬∃ t, ↑t = s
t : Finset R
hts : ↑t ⊆ s
mem : 1 ∈ Submodule.span R ↑t
⊢ ∃! r, ∀ (a : ↑s), (algebraMap R (Away ↑a)) r = f a

Tactic:
have ⟨r, eq, uniq⟩ := this t (fun a ↦ f ⟨a, hts a.2⟩)
  (fun a b ↦ h ⟨a, hts a.2⟩ ⟨b, hts b.2⟩) mem ⟨_, rfl⟩

Result:
case inr
R : Type u_1
inst✝ : CommSemiring R
s : Set R
f : (a : ↑s) → Away ↑a
h : ∀ (a b : ↑s), (Away.awayToAwayRight ↑a ↑b) (f a) = (Away.awayToAwayLeft ↑b ↑a) (f b)
mem✝ : 1 ∈ Ideal.span s
this :
  ∀ (s : Set R) (f : (a : ↑s) → Away ↑a),
    (∀ (a b : ↑s), (Away.awayToAwayRight ↑a ↑b) (f a) = (Away.awayToAwayLeft ↑b ↑a) (f b)) →
      1 ∈ Ideal.span s → (∃ t, ↑t = s) → ∃! r, ∀ (a : ↑s), (algebraMap R (Away ↑a)) r = f a
finset_eq : ¬∃ t, ↑t = s
t : Finset R
hts : ↑t ⊆ s
mem : 1 ∈ Submodule.span R ↑t
r : R
eq : (fun r => ∀ (a : ↑↑t), (algebraMap R (Away ↑a)) r = f ⟨↑a, ⋯⟩) r
uniq : ∀ (y : R), (fun r => ∀ (a : ↑↑t), (algebraMap R (Away ↑a)) r = f ⟨↑a, ⋯⟩) y → y = r
⊢ ∃! r, ∀ (a : ↑s), (algebraMap R (Away ↑a)) r = f a
-- Mathlib/Computability/MyhillNerode.lean
theorem accepts_toDFA : L.toDFA.accepts = L

Proof state:
case h
α : Type u
L : Language α
x : List α
⊢ x ∈ L.toDFA.accepts ↔ x ∈ L

Tactic:
rw [DFA.mem_accepts]

Result:
case h
α : Type u
L : Language α
x : List α
⊢ L.toDFA.eval x ∈ L.toDFA.accept ↔ x ∈ L

Proof state:
α : Type u
L : Language α
x : List α
this : ↑(L.toDFA.eval x) = L.leftQuotient x
⊢ L.toDFA.eval x ∈ L.toDFA.accept ↔ x ∈ L

Tactic:
simp [this]

Result:
no goals

Proof state:
case h
α : Type u
L : Language α
x : List α
⊢ L.toDFA.eval x ∈ L.toDFA.accept ↔ x ∈ L

Tactic:
suffices L.toDFA.eval x = L.leftQuotient x by simp [this]

Result:
case h
α : Type u
L : Language α
x : List α
⊢ ↑(L.toDFA.eval x) = L.leftQuotient x

Proof state:
case h
α : Type u
L : Language α
x : List α
⊢ ↑(L.toDFA.eval x) = L.leftQuotient x

Tactic:
induction x using List.reverseRecOn with
| nil => simp
| append_singleton x a ih => simp [ih, leftQuotient_append]

Result:
no goals

Proof state:
case h.append_singleton
α : Type u
L : Language α
x : List α
a : α
ih : ↑(L.toDFA.eval x) = L.leftQuotient x
⊢ ↑(L.toDFA.eval (x ++ [a])) = L.leftQuotient (x ++ [a])

Tactic:
simp [ih, leftQuotient_append]

Result:
no goals

Proof state:
case h.nil
α : Type u
L : Language α
⊢ ↑(L.toDFA.eval []) = L.leftQuotient []

Tactic:
simp

Result:
no goals

Proof state:
α : Type u
L : Language α
⊢ L.toDFA.accepts = L

Tactic:
ext x

Result:
case h
α : Type u
L : Language α
x : List α
⊢ x ∈ L.toDFA.accepts ↔ x ∈ L
-- Mathlib/GroupTheory/Perm/Sign.lean
theorem prod_prodExtendRight {α : Type*} [DecidableEq α] (σ : α → Perm β) {l : List α}
    (hl : l.Nodup) (mem_l : ∀ a, a ∈ l) :
    (l.map fun a => prodExtendRight a (σ a)).prod = prodCongrRight σ

Proof state:
case H.mk.cons.inl.intro
β : Type v
α : Type u_1
inst✝ : DecidableEq α
σ : α → Perm β
a : α
b : β
a' : α
l : List α
ih :
  l.Nodup →
    a ∈ l ∧ (List.map (fun a => prodExtendRight a (σ a)) l).prod (a, b) = (a, (σ a) b) ∨
      a ∉ l ∧ (List.map (fun a => prodExtendRight a (σ a)) l).prod (a, b) = (a, b)
hl : (a' :: l).Nodup
mem_l : a ∈ l
prod_eq : (List.map (fun a => prodExtendRight a (σ a)) l).prod (a, b) = (a, (σ a) b)
⊢ a ∈ a' :: l ∧ (prodExtendRight a' (σ a')) (a, (σ a) b) = (a, (σ a) b) ∨
    a ∉ a' :: l ∧ (prodExtendRight a' (σ a')) (a, (σ a) b) = (a, b)

Tactic:
refine Or.inl ⟨List.mem_cons_of_mem _ mem_l, ?_⟩

Result:
case H.mk.cons.inl.intro
β : Type v
α : Type u_1
inst✝ : DecidableEq α
σ : α → Perm β
a : α
b : β
a' : α
l : List α
ih :
  l.Nodup →
    a ∈ l ∧ (List.map (fun a => prodExtendRight a (σ a)) l).prod (a, b) = (a, (σ a) b) ∨
      a ∉ l ∧ (List.map (fun a => prodExtendRight a (σ a)) l).prod (a, b) = (a, b)
hl : (a' :: l).Nodup
mem_l : a ∈ l
prod_eq : (List.map (fun a => prodExtendRight a (σ a)) l).prod (a, b) = (a, (σ a) b)
⊢ (prodExtendRight a' (σ a')) (a, (σ a) b) = (a, (σ a) b)

Proof state:
case neg
β : Type v
α : Type u_1
inst✝ : DecidableEq α
σ : α → Perm β
a : α
b : β
a' : α
l : List α
ih :
  l.Nodup →
    a ∈ l ∧ (List.map (fun a => prodExtendRight a (σ a)) l).prod (a, b) = (a, (σ a) b) ∨
      a ∉ l ∧ (List.map (fun a => prodExtendRight a (σ a)) l).prod (a, b) = (a, b)
hl : (a' :: l).Nodup
not_mem_l : a ∉ l
prod_eq : (List.map (fun a => prodExtendRight a (σ a)) l).prod (a, b) = (a, b)
ha' : ¬a = a'
⊢ (prodExtendRight a' (σ a')) (a, b) = (a, b)

Tactic:
rw [prodExtendRight_apply_ne _ ha']

Result:
no goals
-- Mathlib/Analysis/Complex/Liouville.lean
theorem norm_deriv_le_of_forall_mem_sphere_norm_le {c : ℂ} {R C : ℝ} {f : ℂ → F} (hR : 0 < R)
    (hd : DiffContOnCl ℂ f (ball c R)) (hC : ∀ z ∈ sphere c R, ‖f z‖ ≤ C) :
    ‖deriv f c‖ ≤ C / R

Proof state:
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
c : ℂ
R C : ℝ
f : ℂ → F
hR : 0 < R
hd : DiffContOnCl ℂ f (ball c R)
hC : ∀ z ∈ sphere c R, ‖f z‖ ≤ C
e : F →L[ℂ] F̂ := UniformSpace.Completion.toComplL
this : HasDerivAt (⇑e ∘ f) (e (deriv f c)) c
⊢ ‖deriv f c‖ = ‖e (deriv f c)‖

Tactic:
exact (UniformSpace.Completion.norm_coe _).symm

Result:
no goals

Proof state:
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
c : ℂ
R C : ℝ
f : ℂ → F
hR : 0 < R
hd : DiffContOnCl ℂ f (ball c R)
hC : ∀ z ∈ sphere c R, ‖f z‖ ≤ C
e : F →L[ℂ] F̂ := UniformSpace.Completion.toComplL
this : HasDerivAt (⇑e ∘ f) (e (deriv f c)) c
⊢ ‖deriv f c‖ = ‖deriv (⇑e ∘ f) c‖

Tactic:
rw [this.deriv]

Result:
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
c : ℂ
R C : ℝ
f : ℂ → F
hR : 0 < R
hd : DiffContOnCl ℂ f (ball c R)
hC : ∀ z ∈ sphere c R, ‖f z‖ ≤ C
e : F →L[ℂ] F̂ := UniformSpace.Completion.toComplL
this : HasDerivAt (⇑e ∘ f) (e (deriv f c)) c
⊢ ‖deriv f c‖ = ‖e (deriv f c)‖

Proof state:
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
c : ℂ
R C : ℝ
f : ℂ → F
hR : 0 < R
hd : DiffContOnCl ℂ f (ball c R)
hC : ∀ z ∈ sphere c R, ‖f z‖ ≤ C
e : F →L[ℂ] F̂ := UniformSpace.Completion.toComplL
⊢ ‖deriv f c‖ ≤ C / R

Tactic:
have : HasDerivAt (e ∘ f) (e (deriv f c)) c :=
  e.hasFDerivAt.comp_hasDerivAt c
    (hd.differentiableAt isOpen_ball <| mem_ball_self hR).hasDerivAt

Result:
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
c : ℂ
R C : ℝ
f : ℂ → F
hR : 0 < R
hd : DiffContOnCl ℂ f (ball c R)
hC : ∀ z ∈ sphere c R, ‖f z‖ ≤ C
e : F →L[ℂ] F̂ := UniformSpace.Completion.toComplL
this : HasDerivAt (⇑e ∘ f) (e (deriv f c)) c
⊢ ‖deriv f c‖ ≤ C / R

Proof state:
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
c : ℂ
R C : ℝ
f : ℂ → F
hR : 0 < R
hd : DiffContOnCl ℂ f (ball c R)
hC : ∀ z ∈ sphere c R, ‖f z‖ ≤ C
⊢ ‖deriv f c‖ ≤ C / R

Tactic:
set e : F →L[ℂ] F̂ := UniformSpace.Completion.toComplL

Result:
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
c : ℂ
R C : ℝ
f : ℂ → F
hR : 0 < R
hd : DiffContOnCl ℂ f (ball c R)
hC : ∀ z ∈ sphere c R, ‖f z‖ ≤ C
e : F →L[ℂ] F̂ := UniformSpace.Completion.toComplL
⊢ ‖deriv f c‖ ≤ C / R

Proof state:
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℂ F
c : ℂ
R C : ℝ
f : ℂ → F
hR : 0 < R
hd : DiffContOnCl ℂ f (ball c R)
hC : ∀ z ∈ sphere c R, ‖f z‖ ≤ C
e : F →L[ℂ] F̂ := UniformSpace.Completion.toComplL
this : HasDerivAt (⇑e ∘ f) (e (deriv f c)) c
⊢ ‖deriv f c‖ ≤ C / R

Tactic:
calc
  ‖deriv f c‖ = ‖deriv (e ∘ f) c‖ := by
    rw [this.deriv]
    exact (UniformSpace.Completion.norm_coe _).symm
  _ ≤ C / R :=
    norm_deriv_le_aux hR (e.differentiable.comp_diffContOnCl hd) fun z hz =>
      (UniformSpace.Completion.norm_coe _).trans_le (hC z hz)

Result:
no goals
-- Mathlib/Analysis/Convex/TotallyBounded.lean
theorem totallyBounded_convexHull (hs : TotallyBounded s) :
    TotallyBounded (convexHull ℝ s)

Proof state:
case intro.intro.intro.intro.intro.intro.intro.intro.intro
E : Type u_1
s : Set E
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
inst✝² : UniformSpace E
inst✝¹ : UniformAddGroup E
lcs : LocallyConvexSpace ℝ E
inst✝ : ContinuousSMul ℝ E
hs : TotallyBounded s
U : Set E
hU : U ∈ nhds 0
W : Set E
hW₁ : W ∈ nhds 0
hW₂ : ∀ v ∈ W, ∀ w ∈ W, v + w ∈ U
V : Set E
hV₁ : V ∈ nhds 0
hV₂ : Convex ℝ V
hV₃ : V ⊆ W
t : Set E
htf : t.Finite
hts : s ⊆ ⋃ y ∈ t, y +ᵥ V
t' : Set E
htf' : t'.Finite
hts' : (convexHull ℝ) t ⊆ ⋃ y ∈ t', y +ᵥ V
⊢ ∃ t, t.Finite ∧ (convexHull ℝ) s ⊆ ⋃ y ∈ t, y +ᵥ U

Tactic:
use t', htf'

Result:
case right
E : Type u_1
s : Set E
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
inst✝² : UniformSpace E
inst✝¹ : UniformAddGroup E
lcs : LocallyConvexSpace ℝ E
inst✝ : ContinuousSMul ℝ E
hs : TotallyBounded s
U : Set E
hU : U ∈ nhds 0
W : Set E
hW₁ : W ∈ nhds 0
hW₂ : ∀ v ∈ W, ∀ w ∈ W, v + w ∈ U
V : Set E
hV₁ : V ∈ nhds 0
hV₂ : Convex ℝ V
hV₃ : V ⊆ W
t : Set E
htf : t.Finite
hts : s ⊆ ⋃ y ∈ t, y +ᵥ V
t' : Set E
htf' : t'.Finite
hts' : (convexHull ℝ) t ⊆ ⋃ y ∈ t', y +ᵥ V
⊢ (convexHull ℝ) s ⊆ ⋃ y ∈ t', y +ᵥ U

Proof state:
E : Type u_1
s : Set E
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
inst✝² : UniformSpace E
inst✝¹ : UniformAddGroup E
lcs : LocallyConvexSpace ℝ E
inst✝ : ContinuousSMul ℝ E
hs : TotallyBounded s
⊢ ∀ U ∈ nhds 0, ∃ t, t.Finite ∧ (convexHull ℝ) s ⊆ ⋃ y ∈ t, y +ᵥ U

Tactic:
intro U hU

Result:
E : Type u_1
s : Set E
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
inst✝² : UniformSpace E
inst✝¹ : UniformAddGroup E
lcs : LocallyConvexSpace ℝ E
inst✝ : ContinuousSMul ℝ E
hs : TotallyBounded s
U : Set E
hU : U ∈ nhds 0
⊢ ∃ t, t.Finite ∧ (convexHull ℝ) s ⊆ ⋃ y ∈ t, y +ᵥ U

Proof state:
E : Type u_1
s : Set E
inst✝⁴ : AddCommGroup E
inst✝³ : Module ℝ E
inst✝² : UniformSpace E
inst✝¹ : UniformAddGroup E
lcs : LocallyConvexSpace ℝ E
inst✝ : ContinuousSMul ℝ E
hs : TotallyBounded s
U : Set E
hU : U ∈ nhds 0
W : Set E
hW₁ : W ∈ nhds 0
hW₂ : ∀ v ∈ W, ∀ w ∈ W, v + w ∈ U
V : Set E
hV₁ : V ∈ nhds 0
hV₂ : Convex ℝ V
hV₃ : V ⊆ W
t : Set E
htf : t.Finite
t' : Set E
htf' : t'.Finite
hts : s ⊆ t + V
hts' : (convexHull ℝ) t ⊆ t' + V
⊢ (convexHull ℝ) t + (convexHull ℝ) V = (convexHull ℝ) t + V

Tactic:
rw [hV₂.convexHull_eq]

Result:
no goals
-- Mathlib/Data/Multiset/Bind.lean
theorem bind_map_comm (m : Multiset α) (n : Multiset β) {f : α → β → γ} :
    ((bind m) fun a => n.map fun b => f a b) = (bind n) fun b => m.map fun a => f a b :=
  Multiset.induction_on m (by simp) (by simp +contextual)

Proof state:
α : Type u_1
β : Type v
γ : Type u_2
m : Multiset α
n : Multiset β
f : α → β → γ
⊢ ∀ (a : α) (s : Multiset α),
    ((s.bind fun a => map (fun b => f a b) n) = n.bind fun b => map (fun a => f a b) s) →
      ((a ::ₘ s).bind fun a => map (fun b => f a b) n) = n.bind fun b => map (fun a => f a b) (a ::ₘ s)

Tactic:
simp +contextual

Result:
no goals

Proof state:
α : Type u_1
β : Type v
γ : Type u_2
m : Multiset α
n : Multiset β
f : α → β → γ
⊢ (bind 0 fun a => map (fun b => f a b) n) = n.bind fun b => map (fun a => f a b) 0

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Ord.lean
theorem isEq_swap {o : Ordering} : o.swap.isEq = o.isEq

Proof state:
o : Ordering
⊢ o.swap.isEq = o.isEq

Tactic:
cases o <;> simp

Result:
no goals
-- Mathlib/AlgebraicGeometry/ValuativeCriterion.lean
@[stacks 01KE]
lemma specializingMap (H : ValuativeCriterion.Existence f) :
    SpecializingMap f.base

Proof state:
X Y : Scheme
f : X ⟶ Y
H : Existence f
x' : ↑↑X.toPresheafedSpace
y : ↑↑Y.toPresheafedSpace
h : flip (fun x1 x2 => x1 ⤳ x2) y ((ConcreteCategory.hom f.base) x')
stalk_y_to_residue_x' : Y.presheaf.stalk y ⟶ X.residueField x' :=
  Y.presheaf.stalkSpecializes h ≫ Scheme.Hom.stalkMap f x' ≫ X.residue x'
A : ValuationSubring ↑(X.residueField x')
hA : ∀ (x : ↑(Y.presheaf.stalk y)), (CommRingCat.Hom.hom stalk_y_to_residue_x') x ∈ A.toSubring
hA_local : IsLocalHom ((CommRingCat.Hom.hom stalk_y_to_residue_x').codRestrict A.toSubring hA)
stalk_y_to_A : Y.presheaf.stalk y ⟶ CommRingCat.of ↥A :=
  CommRingCat.ofHom ((CommRingCat.Hom.hom stalk_y_to_residue_x').codRestrict A hA)
⊢ Spec.map ((Y.presheaf.stalkSpecializes h ≫ Scheme.Hom.stalkMap f x') ≫ X.residue x') ≫ Y.fromSpecStalk y =
    Spec.map (stalk_y_to_A ≫ CommRingCat.ofHom (algebraMap ↥A ↑(X.residueField x'))) ≫ Y.fromSpecStalk y

Tactic:
rfl

Result:
no goals
-- Mathlib/Algebra/Group/Basic.lean
theorem eq_mul_inv_of_mul_eq (h : a * c = b) : a = b * c⁻¹

Proof state:
G : Type u_3
inst✝ : Group G
a b c : G
h : a * c = b
⊢ a = b * c⁻¹

Tactic:
simp [h.symm]

Result:
no goals
-- Mathlib/Data/Part.lean
theorem some_mod_some [Mod α] (a b : α) : some a % some b = some (a % b)

Proof state:
α : Type u_1
inst✝ : Mod α
a b : α
⊢ some a % some b = some (a % b)

Tactic:
simp [mod_def]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Sublist.lean
theorem reverse_subset {l₁ l₂ : List α} : reverse l₁ ⊆ l₂ ↔ l₁ ⊆ l₂

Proof state:
α : Type u_1
l₁ l₂ : List α
⊢ l₁.reverse ⊆ l₂ ↔ l₁ ⊆ l₂

Tactic:
simp [subset_def]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/Cooper.lean
theorem resolve_left_dvd₁ (a c d p x : Int) (h₁ : p ≤ a * x) :
    a ∣ resolve_left a c d p x + p

Proof state:
a c d p x : Int
h₁ : p ≤ a * x
k' : Nat
w : a * x = p + ↑k'
⊢ ↑k' + p = a * x

Tactic:
rw [w, Int.add_comm]

Result:
no goals

Proof state:
case mk
a c d p x : Int
h₁ : p ≤ a * x
k' : Nat
w : a * x = p + ↑k'
⊢ a ∣ ↑(⟨k', w⟩.val % a.lcm (a * d / ↑((a * d).gcd c))) + p

Tactic:
exact Int.ofNat_emod _ _ ▸ dvd_emod_add_of_dvd_add (x := k') ⟨x, by rw [w, Int.add_comm]⟩ dvd_lcm_left

Result:
no goals

Proof state:
a c d p x : Int
h₁ : p ≤ a * x
⊢ a ∣ resolve_left a c d p x + p

Tactic:
simp only [h₁, resolve_left_eq, resolve_left']

Result:
a c d p x : Int
h₁ : p ≤ a * x
⊢ a ∣ ↑((add_of_le h₁).val % a.lcm (a * d / ↑((a * d).gcd c))) + p

Proof state:
a c d p x : Int
h₁ : p ≤ a * x
⊢ a ∣ ↑((add_of_le h₁).val % a.lcm (a * d / ↑((a * d).gcd c))) + p

Tactic:
obtain ⟨k', w⟩ := add_of_le h₁

Result:
case mk
a c d p x : Int
h₁ : p ≤ a * x
k' : Nat
w : a * x = p + ↑k'
⊢ a ∣ ↑(⟨k', w⟩.val % a.lcm (a * d / ↑((a * d).gcd c))) + p
-- Mathlib/AlgebraicTopology/SimplexCategory/Basic.lean
theorem eq_of_one_to_two (f : ⦋1⦌ ⟶ ⦋2⦌) :
    (∃ i, f = (δ (n := 1) i)) ∨ ∃ a, f = SimplexCategory.const _ _ a

Proof state:
f : ⦋1⦌ ⟶ ⦋2⦌
this : (Hom.toOrderHom f) 0 ≤ (Hom.toOrderHom f) 1
e0 : (Hom.toOrderHom f) 0 = 0
e1 : (Hom.toOrderHom f) 1 = 1
⊢ (∃ i, f = δ i) ∨ ∃ a, f = ⦋1⦌.const ⦋2⦌ a

Tactic:
refine .inl ⟨2, ?_⟩

Result:
f : ⦋1⦌ ⟶ ⦋2⦌
this : (Hom.toOrderHom f) 0 ≤ (Hom.toOrderHom f) 1
e0 : (Hom.toOrderHom f) 0 = 0
e1 : (Hom.toOrderHom f) 1 = 1
⊢ f = δ 2