harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/Calculus/ContDiff/Basic.lean
theorem contDiffWithinAt_singleton : ContDiffWithinAt 𝕜 n f {x} x :=
  (contDiffWithinAt_const (c := f x)).congr (by simp) rfl

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
x : E
n : WithTop ℕ∞
⊢ ∀ y ∈ {x}, f y = f x

Tactic:
simp

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Arithmetic.lean
theorem zero_sub (a : Ordinal) : 0 - a = 0

Proof state:
a : Ordinal.{u_4}
⊢ 0 - a = 0

Tactic:
rw [← Ordinal.le_zero]

Result:
a : Ordinal.{u_4}
⊢ 0 - a ≤ 0

Proof state:
a : Ordinal.{u_4}
⊢ 0 - a ≤ 0

Tactic:
apply sub_le_self

Result:
no goals
-- Mathlib/Data/Matrix/Rank.lean
theorem rank_eq_finrank_span_row [Field R] [Finite m] (A : Matrix m n R) :
    A.rank = finrank R (Submodule.span R (Set.range A))

Proof state:
m : Type u_2
n : Type u_3
R : Type u_5
inst✝² : Fintype n
inst✝¹ : Field R
inst✝ : Finite m
A : Matrix m n R
⊢ A.rank = finrank R ↥(Submodule.span R (Set.range A))

Tactic:
cases nonempty_fintype m

Result:
case intro
m : Type u_2
n : Type u_3
R : Type u_5
inst✝² : Fintype n
inst✝¹ : Field R
inst✝ : Finite m
A : Matrix m n R
val✝ : Fintype m
⊢ A.rank = finrank R ↥(Submodule.span R (Set.range A))

Proof state:
case intro
m : Type u_2
n : Type u_3
R : Type u_5
inst✝² : Fintype n
inst✝¹ : Field R
inst✝ : Finite m
A : Matrix m n R
val✝ : Fintype m
⊢ A.rank = finrank R ↥(Submodule.span R (Set.range A))

Tactic:
rw [← rank_transpose, rank_eq_finrank_span_cols, transpose_transpose]

Result:
no goals
-- Mathlib/Logic/Equiv/Set.lean
theorem union_symm_apply_left {α} {s t : Set α} [DecidablePred fun x => x ∈ s] (H : Disjoint s t)
    (a : s) : (Equiv.Set.union H).symm (Sum.inl a) = ⟨a, by simp⟩ :=
  rfl

Proof state:
α✝ : Sort u
β : Sort v
γ : Sort w
α : Type ?u.16791
s t : Set α
inst✝ : DecidablePred fun x => x ∈ s
H : Disjoint s t
a : ↑s
⊢ ↑a ∈ s ∪ t

Tactic:
simp

Result:
no goals
-- Mathlib/Order/LiminfLimsup.lean
theorem cofinite.bliminf_set_eq : bliminf s cofinite p = { x | { n | p n ∧ x ∉ s n }.Finite }

Proof state:
α : Type u_1
ι : Type u_4
p : ι → Prop
s : ι → Set α
⊢ bliminf s cofinite p = {x | {n | p n ∧ x ∉ s n}.Finite}

Tactic:
rw [← compl_inj_iff]

Result:
α : Type u_1
ι : Type u_4
p : ι → Prop
s : ι → Set α
⊢ (bliminf s cofinite p)ᶜ = {x | {n | p n ∧ x ∉ s n}.Finite}ᶜ

Proof state:
α : Type u_1
ι : Type u_4
p : ι → Prop
s : ι → Set α
⊢ {x | {n | p n ∧ x ∈ (s n)ᶜ}.Infinite} = {x | {n | p n ∧ x ∉ s n}.Finite}ᶜ

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
ι : Type u_4
p : ι → Prop
s : ι → Set α
⊢ (bliminf s cofinite p)ᶜ = {x | {n | p n ∧ x ∉ s n}.Finite}ᶜ

Tactic:
simp only [bliminf_eq_iSup_biInf, compl_iInf, compl_iSup, ← blimsup_eq_iInf_biSup,
  cofinite.blimsup_set_eq]

Result:
α : Type u_1
ι : Type u_4
p : ι → Prop
s : ι → Set α
⊢ {x | {n | p n ∧ x ∈ (s n)ᶜ}.Infinite} = {x | {n | p n ∧ x ∉ s n}.Finite}ᶜ
-- Mathlib/Data/Matrix/Reflection.lean
theorem dotProductᵣ_eq [Mul α] [AddCommMonoid α] {m} (a b : Fin m → α) :
    dotProductᵣ a b = dotProduct a b

Proof state:
α : Type u_1
inst✝¹ : Mul α
inst✝ : AddCommMonoid α
m : ℕ
a b : Fin m → α
⊢ dotProductᵣ a b = a ⬝ᵥ b

Tactic:
simp_rw [dotProductᵣ, dotProduct, FinVec.sum_eq, FinVec.seq_eq, FinVec.map_eq,
    Function.comp_apply]

Result:
no goals
-- Mathlib/Topology/Algebra/Module/Basic.lean
theorem ContinuousSMul.of_nhds_zero [IsTopologicalRing R] [IsTopologicalAddGroup M]
    (hmul : Tendsto (fun p : R × M => p.1 • p.2) (𝓝 0 ×ˢ 𝓝 0) (𝓝 0))
    (hmulleft : ∀ m : M, Tendsto (fun a : R => a • m) (𝓝 0) (𝓝 0))
    (hmulright : ∀ a : R, Tendsto (fun m : M => a • m) (𝓝 0) (𝓝 0)) : ContinuousSMul R M where
  continuous_smul

Proof state:
R : Type u_1
M : Type u_2
inst✝⁶ : Ring R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : TopologicalSpace M
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsTopologicalRing R
inst✝ : IsTopologicalAddGroup M
hmul : Tendsto (fun p => p.1 • p.2) (𝓝 0 ×ˢ 𝓝 0) (𝓝 0)
hmulleft : ∀ (m : M), Tendsto (fun a => a • m) (𝓝 0) (𝓝 0)
hmulright : ∀ (a : R), Tendsto (fun m => a • m) (𝓝 0) (𝓝 0)
⊢ Continuous fun p => p.1 • p.2

Tactic:
rw [← nhds_prod_eq] at hmul

Result:
R : Type u_1
M : Type u_2
inst✝⁶ : Ring R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : TopologicalSpace M
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsTopologicalRing R
inst✝ : IsTopologicalAddGroup M
hmul : Tendsto (fun p => p.1 • p.2) (𝓝 (0, 0)) (𝓝 0)
hmulleft : ∀ (m : M), Tendsto (fun a => a • m) (𝓝 0) (𝓝 0)
hmulright : ∀ (a : R), Tendsto (fun m => a • m) (𝓝 0) (𝓝 0)
⊢ Continuous fun p => p.1 • p.2

Proof state:
R : Type u_1
M : Type u_2
inst✝⁶ : Ring R
inst✝⁵ : TopologicalSpace R
inst✝⁴ : TopologicalSpace M
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : IsTopologicalRing R
inst✝ : IsTopologicalAddGroup M
hmul : Tendsto (fun p => p.1 • p.2) (𝓝 (0, 0)) (𝓝 0)
hmulleft : ∀ (m : M), Tendsto (fun a => a • m) (𝓝 0) (𝓝 0)
hmulright : ∀ (a : R), Tendsto (fun m => a • m) (𝓝 0) (𝓝 0)
⊢ Continuous fun p => p.1 • p.2

Tactic:
refine continuous_of_continuousAt_zero₂ (AddMonoidHom.smul : R →+ M →+ M) ?_ ?_ ?_ <;>
  simpa [ContinuousAt]

Result:
no goals
-- Mathlib/MeasureTheory/MeasurableSpace/Defs.lean
theorem measurableSet_sSup {ms : Set (MeasurableSpace α)} {s : Set α} :
    MeasurableSet[sSup ms] s ↔
      GenerateMeasurable { s : Set α | ∃ m ∈ ms, MeasurableSet[m] s } s

Proof state:
α : Type u_1
ms : Set (MeasurableSpace α)
s : Set α
⊢ GenerateMeasurable (⋃₀ ((fun m => {t | MeasurableSet t}) '' ms)) s ↔
    GenerateMeasurable {s | ∃ m ∈ ms, MeasurableSet s} s

Tactic:
simp [← setOf_exists]

Result:
no goals

Proof state:
α : Type u_1
ms : Set (MeasurableSpace α)
s : Set α
⊢ MeasurableSet s ↔ GenerateMeasurable {s | ∃ m ∈ ms, MeasurableSet s} s

Tactic:
change GenerateMeasurable (⋃₀ _) _ ↔ _

Result:
α : Type u_1
ms : Set (MeasurableSpace α)
s : Set α
⊢ GenerateMeasurable (⋃₀ ((fun m => {t | MeasurableSet t}) '' ms)) s ↔
    GenerateMeasurable {s | ∃ m ∈ ms, MeasurableSet s} s
-- Mathlib/Order/Bounds/Basic.lean
theorem bddBelow_empty [Nonempty α] : BddBelow (∅ : Set α)

Proof state:
α : Type u
inst✝¹ : Preorder α
inst✝ : Nonempty α
⊢ BddBelow ∅

Tactic:
simp only [BddBelow, lowerBounds_empty, univ_nonempty]

Result:
no goals
-- Mathlib/Data/List/DropRight.lean
theorem rdrop_zero : rdrop l 0 = l

Proof state:
α : Type u_1
l : List α
⊢ l.rdrop 0 = l

Tactic:
simp [rdrop]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Fin/Fold.lean
theorem foldlM_loop_lt [Monad m] (f : α → Fin n → m α) (x) (h : i < n) :
    foldlM.loop n f x i = f x ⟨i, h⟩ >>= (foldlM.loop n f . (i+1))

Proof state:
m : Type u_1 → Type u_2
α : Type u_1
n i : Nat
inst✝ : Monad m
f : α → Fin n → m α
x : α
h : i < n
⊢ foldlM.loop n f x i = do
    let x ← f x ⟨i, h⟩
    foldlM.loop n f x (i + 1)

Tactic:
rw [foldlM.loop, dif_pos h]

Result:
no goals
-- Mathlib/Computability/Primrec.lean
theorem const (x : σ) : Primrec fun _ : α => x :=
  ((casesOn1 0 (.const (encode x).succ)).comp (@Primcodable.prim α _)).of_eq fun n => by
    cases @decode α _ n <;> rfl

Proof state:
α : Type u_1
σ : Type u_3
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
x : σ
n : ℕ
⊢ (Nat.casesOn (encode (decode n)) 0 fun x_1 => (encode x).succ) = encode (Option.map (fun x_1 => x) (decode n))

Tactic:
cases @decode α _ n <;> rfl

Result:
no goals
-- Mathlib/RingTheory/DedekindDomain/Factorization.lean
theorem count_coe_nonneg (J : Ideal R) : 0 ≤ count K v J

Proof state:
case pos
R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
J : Ideal R
hJ : J = 0
⊢ 0 ≤ count K v ↑J

Tactic:
simp only [hJ, Submodule.zero_eq_bot, coeIdeal_bot, count_zero, le_refl]

Result:
no goals

Proof state:
R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
J : Ideal R
⊢ 0 ≤ count K v ↑J

Tactic:
by_cases hJ : J = 0

Result:
case pos
R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
J : Ideal R
hJ : J = 0
⊢ 0 ≤ count K v ↑J

case neg
R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
J : Ideal R
hJ : ¬J = 0
⊢ 0 ≤ count K v ↑J

Proof state:
case neg
R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
J : Ideal R
hJ : ¬J = 0
⊢ 0 ≤ count K v ↑J

Tactic:
simp only [count_coe K v hJ, Nat.cast_nonneg]

Result:
no goals

Proof state:
case neg
R : Type u_1
inst✝⁴ : CommRing R
K : Type u_2
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : IsFractionRing R K
inst✝ : IsDedekindDomain R
v : HeightOneSpectrum R
J : Ideal R
hJ : ¬J = 0
⊢ 0 ≤ count K v ↑J

Tactic:
classical simp only [count_coe K v hJ, Nat.cast_nonneg]

Result:
no goals
-- Mathlib/CategoryTheory/Adjunction/Basic.lean
@[simp, reassoc]
lemma comp_counit_app (X : E) :
    (adj₁.comp adj₂).counit.app X = H.map (adj₁.counit.app (I.obj X)) ≫ adj₂.counit.app X

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
G : D ⥤ C
E : Type u₃
ℰ : Category.{v₃, u₃} E
H : D ⥤ E
I : E ⥤ D
adj₁ : F ⊣ G
adj₂ : H ⊣ I
X : E
⊢ (adj₁.comp adj₂).counit.app X = H.map (adj₁.counit.app (I.obj X)) ≫ adj₂.counit.app X

Tactic:
simp [Adjunction.comp]

Result:
no goals
-- Mathlib/Algebra/Lie/Free.lean
theorem Rel.addLeft (a : lib R X) {b c : lib R X} (h : Rel R X b c) : Rel R X (a + b) (a + c)

Proof state:
R : Type u
X : Type v
inst✝ : CommRing R
a b c : lib R X
h : Rel R X b c
⊢ Rel R X (a + b) (a + c)

Tactic:
rw [add_comm _ b, add_comm _ c]

Result:
R : Type u
X : Type v
inst✝ : CommRing R
a b c : lib R X
h : Rel R X b c
⊢ Rel R X (b + a) (c + a)

Proof state:
R : Type u
X : Type v
inst✝ : CommRing R
a b c : lib R X
h : Rel R X b c
⊢ Rel R X (b + a) (c + a)

Tactic:
exact h.add_right _

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Basic.lean
theorem sin_nonneg_of_mem_Icc {x : ℝ} (hx : x ∈ Icc 0 π) : 0 ≤ sin x

Proof state:
x : ℝ
hx : x ∈ closure (Ioo 0 π)
⊢ 0 ≤ sin x

Tactic:
exact
  closure_lt_subset_le continuous_const continuous_sin
    (closure_mono (fun y => sin_pos_of_mem_Ioo) hx)

Result:
no goals

Proof state:
x : ℝ
hx : x ∈ Icc 0 π
⊢ 0 ≤ sin x

Tactic:
rw [← closure_Ioo pi_ne_zero.symm] at hx

Result:
x : ℝ
hx : x ∈ closure (Ioo 0 π)
⊢ 0 ≤ sin x
-- Mathlib/Algebra/Algebra/Quasispectrum.lean
theorem of_rightInvOn (h₁ : Function.LeftInverse f (algebraMap R S))
    (h₂ : (spectrum S a).RightInvOn f (algebraMap R S)) : SpectrumRestricts a f where
  rightInvOn x hx

Proof state:
R : Type u_3
S : Type u_4
A : Type u_5
inst✝⁵ : Semifield R
inst✝⁴ : Semifield S
inst✝³ : Ring A
inst✝² : Algebra R S
inst✝¹ : Algebra R A
inst✝ : Algebra S A
a : A
f : S → R
h₁ : Function.LeftInverse f ⇑(algebraMap R S)
h₂ : Set.RightInvOn f (⇑(algebraMap R S)) (spectrum S a)
x : S
hx : x ∈ quasispectrum S a
⊢ (algebraMap R S) (f x) = x

Tactic:
obtain (rfl | hx) := mem_quasispectrum_iff.mp hx

Result:
case inl
R : Type u_3
S : Type u_4
A : Type u_5
inst✝⁵ : Semifield R
inst✝⁴ : Semifield S
inst✝³ : Ring A
inst✝² : Algebra R S
inst✝¹ : Algebra R A
inst✝ : Algebra S A
a : A
f : S → R
h₁ : Function.LeftInverse f ⇑(algebraMap R S)
h₂ : Set.RightInvOn f (⇑(algebraMap R S)) (spectrum S a)
hx : 0 ∈ quasispectrum S a
⊢ (algebraMap R S) (f 0) = 0

case inr
R : Type u_3
S : Type u_4
A : Type u_5
inst✝⁵ : Semifield R
inst✝⁴ : Semifield S
inst✝³ : Ring A
inst✝² : Algebra R S
inst✝¹ : Algebra R A
inst✝ : Algebra S A
a : A
f : S → R
h₁ : Function.LeftInverse f ⇑(algebraMap R S)
h₂ : Set.RightInvOn f (⇑(algebraMap R S)) (spectrum S a)
x : S
hx✝ : x ∈ quasispectrum S a
hx : x ∈ spectrum S a
⊢ (algebraMap R S) (f x) = x

Proof state:
case inr
R : Type u_3
S : Type u_4
A : Type u_5
inst✝⁵ : Semifield R
inst✝⁴ : Semifield S
inst✝³ : Ring A
inst✝² : Algebra R S
inst✝¹ : Algebra R A
inst✝ : Algebra S A
a : A
f : S → R
h₁ : Function.LeftInverse f ⇑(algebraMap R S)
h₂ : Set.RightInvOn f (⇑(algebraMap R S)) (spectrum S a)
x : S
hx✝ : x ∈ quasispectrum S a
hx : x ∈ spectrum S a
⊢ (algebraMap R S) (f x) = x

Tactic:
exact h₂ hx

Result:
no goals

Proof state:
case inl
R : Type u_3
S : Type u_4
A : Type u_5
inst✝⁵ : Semifield R
inst✝⁴ : Semifield S
inst✝³ : Ring A
inst✝² : Algebra R S
inst✝¹ : Algebra R A
inst✝ : Algebra S A
a : A
f : S → R
h₁ : Function.LeftInverse f ⇑(algebraMap R S)
h₂ : Set.RightInvOn f (⇑(algebraMap R S)) (spectrum S a)
hx : 0 ∈ quasispectrum S a
⊢ (algebraMap R S) (f 0) = 0

Tactic:
simpa using h₁ 0

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/SimpLemmas.lean
theorem Bool.not_eq_false (b : Bool) : (¬(b = false)) = (b = true)

Proof state:
b : Bool
⊢ (¬b = false) = (b = true)

Tactic:
cases b <;> decide

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Find.lean
theorem findFinIdx?_congr {p : α → Bool} {l₁ : Vector α n} {l₂ : Vector α n} (w : l₁ = l₂) :
    findFinIdx? p l₁ = findFinIdx? p l₂

Proof state:
α : Type u_1
n : Nat
p : α → Bool
l₁ l₂ : Vector α n
w : l₁ = l₂
⊢ findFinIdx? p l₁ = findFinIdx? p l₂

Tactic:
subst w

Result:
α : Type u_1
n : Nat
p : α → Bool
l₁ : Vector α n
⊢ findFinIdx? p l₁ = findFinIdx? p l₁

Proof state:
α : Type u_1
n : Nat
p : α → Bool
l₁ : Vector α n
⊢ findFinIdx? p l₁ = findFinIdx? p l₁

Tactic:
simp

Result:
no goals
-- Mathlib/RingTheory/Localization/Basic.lean
theorem algEquiv_symm_mk (x : R) (y : M) : (algEquiv M S).symm (mk' S x y) = mk x y

Proof state:
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type u_2
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
x : R
y : ↥M
⊢ (algEquiv M S).symm (mk' S x y) = mk x y

Tactic:
rw [mk_eq_mk', algEquiv_symm_mk']

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/PropLemmas.lean
theorem Decidable.not_exists_not {p : α → Prop} [∀ x, Decidable (p x)] :
    (¬∃ x, ¬p x) ↔ ∀ x, p x

Proof state:
α : Sort u_1
p : α → Prop
inst✝ : (x : α) → Decidable (p x)
⊢ (¬∃ x, ¬p x) ↔ ∀ (x : α), p x

Tactic:
simp only [not_exists, Decidable.not_not]

Result:
no goals
-- Mathlib/Topology/Sheaves/Stalks.lean
theorem stalk_hom_ext (F : X.Presheaf C) {x} {Y : C} {f₁ f₂ : F.stalk x ⟶ Y}
    (ih : ∀ (U : Opens X) (hxU : x ∈ U), F.germ U x hxU ≫ f₁ = F.germ U x hxU ≫ f₂) : f₁ = f₂ :=
  colimit.hom_ext fun U => by
    induction U using Opposite.rec with | op U => obtain ⟨U, hxU⟩ := U; exact ih U hxU

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X : TopCat
F : Presheaf C X
x : ↑X
Y : C
f₁ f₂ : F.stalk x ⟶ Y
ih : ∀ (U : Opens ↑X) (hxU : x ∈ U), F.germ U x hxU ≫ f₁ = F.germ U x hxU ≫ f₂
U : (OpenNhds x)ᵒᵖ
⊢ colimit.ι (((whiskeringLeft (OpenNhds x)ᵒᵖ (Opens ↑X)ᵒᵖ C).obj (OpenNhds.inclusion x).op).obj F) U ≫ f₁ =
    colimit.ι (((whiskeringLeft (OpenNhds x)ᵒᵖ (Opens ↑X)ᵒᵖ C).obj (OpenNhds.inclusion x).op).obj F) U ≫ f₂

Tactic:
induction U using Opposite.rec with | op U => obtain ⟨U, hxU⟩ := U; exact ih U hxU

Result:
no goals

Proof state:
case op
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X : TopCat
F : Presheaf C X
x : ↑X
Y : C
f₁ f₂ : F.stalk x ⟶ Y
ih : ∀ (U : Opens ↑X) (hxU : x ∈ U), F.germ U x hxU ≫ f₁ = F.germ U x hxU ≫ f₂
U : OpenNhds x
⊢ colimit.ι (((whiskeringLeft (OpenNhds x)ᵒᵖ (Opens ↑X)ᵒᵖ C).obj (OpenNhds.inclusion x).op).obj F) (op U) ≫ f₁ =
    colimit.ι (((whiskeringLeft (OpenNhds x)ᵒᵖ (Opens ↑X)ᵒᵖ C).obj (OpenNhds.inclusion x).op).obj F) (op U) ≫ f₂

Tactic:
obtain ⟨U, hxU⟩ := U

Result:
case op.mk
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X : TopCat
F : Presheaf C X
x : ↑X
Y : C
f₁ f₂ : F.stalk x ⟶ Y
ih : ∀ (U : Opens ↑X) (hxU : x ∈ U), F.germ U x hxU ≫ f₁ = F.germ U x hxU ≫ f₂
U : Opens ↑X
hxU : x ∈ U
⊢ colimit.ι (((whiskeringLeft (OpenNhds x)ᵒᵖ (Opens ↑X)ᵒᵖ C).obj (OpenNhds.inclusion x).op).obj F)
        (op { obj := U, property := hxU }) ≫
      f₁ =
    colimit.ι (((whiskeringLeft (OpenNhds x)ᵒᵖ (Opens ↑X)ᵒᵖ C).obj (OpenNhds.inclusion x).op).obj F)
        (op { obj := U, property := hxU }) ≫
      f₂

Proof state:
case op.mk
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : HasColimits C
X : TopCat
F : Presheaf C X
x : ↑X
Y : C
f₁ f₂ : F.stalk x ⟶ Y
ih : ∀ (U : Opens ↑X) (hxU : x ∈ U), F.germ U x hxU ≫ f₁ = F.germ U x hxU ≫ f₂
U : Opens ↑X
hxU : x ∈ U
⊢ colimit.ι (((whiskeringLeft (OpenNhds x)ᵒᵖ (Opens ↑X)ᵒᵖ C).obj (OpenNhds.inclusion x).op).obj F)
        (op { obj := U, property := hxU }) ≫
      f₁ =
    colimit.ι (((whiskeringLeft (OpenNhds x)ᵒᵖ (Opens ↑X)ᵒᵖ C).obj (OpenNhds.inclusion x).op).obj F)
        (op { obj := U, property := hxU }) ≫
      f₂

Tactic:
exact ih U hxU

Result:
no goals
-- Mathlib/Analysis/Normed/Algebra/Spectrum.lean
theorem algebraMap_eq_of_mem {a : A} {z : ℂ} (h : z ∈ σ a) : algebraMap ℂ A z = a

Proof state:
A : Type u_2
inst✝¹ : NormedRing A
inst✝ : NormedAlgebra ℂ A
hA : ∀ {a : A}, IsUnit a ↔ a ≠ 0
a : A
z : ℂ
h : z ∈ σ a
⊢ (algebraMap ℂ A) z = a

Tactic:
rwa [mem_iff, hA, Classical.not_not, sub_eq_zero] at h

Result:
no goals
-- Mathlib/Topology/Maps/Basic.lean
theorem of_nonempty (h : ∀ s, IsClosed s → s.Nonempty → IsClosed (f '' s)) :
    IsClosedMap f

Proof state:
case inl
X : Type u_1
Y : Type u_2
f : X → Y
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
h : ∀ (s : Set X), IsClosed s → s.Nonempty → IsClosed (f '' s)
s : Set X
hs : IsClosed s
h2s : s = ∅
⊢ IsClosed (f '' s)

Tactic:
simp_rw [h2s, image_empty, isClosed_empty]

Result:
no goals

Proof state:
X : Type u_1
Y : Type u_2
f : X → Y
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
h : ∀ (s : Set X), IsClosed s → s.Nonempty → IsClosed (f '' s)
s : Set X
hs : IsClosed s
⊢ IsClosed (f '' s)

Tactic:
rcases eq_empty_or_nonempty s with h2s | h2s

Result:
case inl
X : Type u_1
Y : Type u_2
f : X → Y
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
h : ∀ (s : Set X), IsClosed s → s.Nonempty → IsClosed (f '' s)
s : Set X
hs : IsClosed s
h2s : s = ∅
⊢ IsClosed (f '' s)

case inr
X : Type u_1
Y : Type u_2
f : X → Y
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
h : ∀ (s : Set X), IsClosed s → s.Nonempty → IsClosed (f '' s)
s : Set X
hs : IsClosed s
h2s : s.Nonempty
⊢ IsClosed (f '' s)

Proof state:
X : Type u_1
Y : Type u_2
f : X → Y
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
h : ∀ (s : Set X), IsClosed s → s.Nonempty → IsClosed (f '' s)
⊢ IsClosedMap f

Tactic:
intro s hs

Result:
X : Type u_1
Y : Type u_2
f : X → Y
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
h : ∀ (s : Set X), IsClosed s → s.Nonempty → IsClosed (f '' s)
s : Set X
hs : IsClosed s
⊢ IsClosed (f '' s)

Proof state:
case inr
X : Type u_1
Y : Type u_2
f : X → Y
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
h : ∀ (s : Set X), IsClosed s → s.Nonempty → IsClosed (f '' s)
s : Set X
hs : IsClosed s
h2s : s.Nonempty
⊢ IsClosed (f '' s)

Tactic:
exact h s hs h2s

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Complex/Log.lean
theorem tendsto_log_nhdsWithin_im_nonneg_of_re_neg_of_im_zero {z : ℂ} (hre : z.re < 0)
    (him : z.im = 0) : Tendsto log (𝓝[{ z : ℂ | 0 ≤ z.im }] z) (𝓝 <| Real.log ‖z‖ + π * I)

Proof state:
z : ℂ
hre : z.re < 0
him : z.im = 0
⊢ Tendsto log (𝓝[{z | 0 ≤ z.im}] z) (𝓝 (↑(Real.log ‖z‖) + ↑π * I))

Tactic:
simpa only [log, arg_eq_pi_iff.2 ⟨hre, him⟩] using
  (continuousWithinAt_log_of_re_neg_of_im_zero hre him).tendsto

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Lebesgue/Basic.lean
/-- The region between two a.e.-measurable functions on a null-measurable set is null-measurable. -/
lemma nullMeasurableSet_regionBetween (μ : Measure α)
    {f g : α → ℝ} (f_mble : AEMeasurable f μ) (g_mble : AEMeasurable g μ)
    {s : Set α} (s_mble : NullMeasurableSet s μ) :
    NullMeasurableSet {p : α × ℝ | p.1 ∈ s ∧ p.snd ∈ Ioo (f p.fst) (g p.fst)} (μ.prod volume)

Proof state:
case refine_2
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f g : α → ℝ
f_mble : AEMeasurable f μ
g_mble : AEMeasurable g μ
s : Set α
s_mble : NullMeasurableSet s μ
⊢ NullMeasurableSet (fun p => p.2 < g p.1) (μ.prod volume)

Tactic:
exact nullMeasurableSet_lt measurable_snd.aemeasurable (AEMeasurable.fst g_mble)

Result:
no goals

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f g : α → ℝ
f_mble : AEMeasurable f μ
g_mble : AEMeasurable g μ
s : Set α
s_mble : NullMeasurableSet s μ
⊢ NullMeasurableSet {p | p.1 ∈ s ∧ p.2 ∈ Ioo (f p.1) (g p.1)} (μ.prod volume)

Tactic:
refine NullMeasurableSet.inter
        (s_mble.preimage quasiMeasurePreserving_fst) (NullMeasurableSet.inter ?_ ?_)

Result:
case refine_1
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f g : α → ℝ
f_mble : AEMeasurable f μ
g_mble : AEMeasurable g μ
s : Set α
s_mble : NullMeasurableSet s μ
⊢ NullMeasurableSet (fun p => f p.1 < p.2) (μ.prod volume)

case refine_2
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f g : α → ℝ
f_mble : AEMeasurable f μ
g_mble : AEMeasurable g μ
s : Set α
s_mble : NullMeasurableSet s μ
⊢ NullMeasurableSet (fun p => p.2 < g p.1) (μ.prod volume)

Proof state:
case refine_1
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
f g : α → ℝ
f_mble : AEMeasurable f μ
g_mble : AEMeasurable g μ
s : Set α
s_mble : NullMeasurableSet s μ
⊢ NullMeasurableSet (fun p => f p.1 < p.2) (μ.prod volume)

Tactic:
exact nullMeasurableSet_lt (AEMeasurable.fst f_mble) measurable_snd.aemeasurable

Result:
no goals
-- Mathlib/Algebra/Group/Units/Basic.lean
theorem inv_eq_one_divp' (u : αˣ) : ((1 / u : αˣ) : α) = 1 /ₚ u

Proof state:
α : Type u
inst✝ : Monoid α
u : αˣ
⊢ ↑(1 / u) = 1 /ₚ u

Tactic:
rw [one_div, one_divp]

Result:
no goals