harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/Calculus/LocalExtr/LineDeriv.lean
theorem IsExtrOn.lineDerivWithin_eq_zero (h : IsExtrOn f s a)
    (h' : ∀ᶠ t : ℝ in 𝓝 0, a + t • b ∈ s) : lineDerivWithin ℝ f s a b = 0

Proof state:
E : Type u_1
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
f : E → ℝ
s : Set E
a b : E
h : IsExtrOn f s a
h' : ∀ᶠ (t : ℝ) in 𝓝 0, a + t • b ∈ s
⊢ lineDerivWithin ℝ f s a b = 0

Tactic:
exact if hd : LineDifferentiableWithinAt ℝ f s a b then
  h.hasLineDerivWithinAt_eq_zero hd.hasLineDerivWithinAt h'
else
  lineDerivWithin_zero_of_not_lineDifferentiableWithinAt hd

Result:
no goals

Proof state:
E : Type u_1
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
f : E → ℝ
s : Set E
a b : E
h : IsExtrOn f s a
h' : ∀ᶠ (t : ℝ) in 𝓝 0, a + t • b ∈ s
⊢ lineDerivWithin ℝ f s a b = 0

Tactic:
classical
exact if hd : LineDifferentiableWithinAt ℝ f s a b then
  h.hasLineDerivWithinAt_eq_zero hd.hasLineDerivWithinAt h'
else
  lineDerivWithin_zero_of_not_lineDifferentiableWithinAt hd

Result:
no goals
-- Mathlib/Analysis/Calculus/InverseFunctionTheorem/ApproximatesLinearOn.lean
theorem approximatesLinearOn_iff_lipschitzOnWith {f : E → F} {f' : E →L[𝕜] F} {s : Set E}
    {c : ℝ≥0} : ApproximatesLinearOn f f' s c ↔ LipschitzOnWith c (f - ⇑f') s

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
f' : E →L[𝕜] F
s : Set E
c : ℝ≥0
this : ∀ (x y : E), f x - f y - f' (x - y) = (f - ⇑f') x - (f - ⇑f') y
⊢ ApproximatesLinearOn f f' s c ↔ LipschitzOnWith c (f - ⇑f') s

Tactic:
simp only [this, lipschitzOnWith_iff_norm_sub_le, ApproximatesLinearOn]

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
f' : E →L[𝕜] F
s : Set E
c : ℝ≥0
⊢ ApproximatesLinearOn f f' s c ↔ LipschitzOnWith c (f - ⇑f') s

Tactic:
have : ∀ x y, f x - f y - f' (x - y) = (f - f') x - (f - f') y := fun x y ↦ by
  simp only [map_sub, Pi.sub_apply]; abel

Result:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
f' : E →L[𝕜] F
s : Set E
c : ℝ≥0
this : ∀ (x y : E), f x - f y - f' (x - y) = (f - ⇑f') x - (f - ⇑f') y
⊢ ApproximatesLinearOn f f' s c ↔ LipschitzOnWith c (f - ⇑f') s

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
f' : E →L[𝕜] F
s : Set E
c : ℝ≥0
x y : E
⊢ f x - f y - (f' x - f' y) = f x - f' x - (f y - f' y)

Tactic:
abel

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
f' : E →L[𝕜] F
s : Set E
c : ℝ≥0
x y : E
⊢ f x - f y - f' (x - y) = (f - ⇑f') x - (f - ⇑f') y

Tactic:
simp only [map_sub, Pi.sub_apply]

Result:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
f' : E →L[𝕜] F
s : Set E
c : ℝ≥0
x y : E
⊢ f x - f y - (f' x - f' y) = f x - f' x - (f y - f' y)
-- Mathlib/RingTheory/Noetherian/Orzech.lean
theorem IsNoetherian.injective_of_surjective_of_injective (i f : N →ₗ[R] M)
    (hi : Injective i) (hf : Surjective f) : Injective f

Proof state:
R : Type u_1
M : Type u_2
N : Type w
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : IsNoetherian R M
i f : N →ₗ[R] M
hi : Injective ⇑i
hf : Surjective ⇑f
⊢ Injective ⇑f

Tactic:
haveI := isNoetherian_of_injective i hi

Result:
R : Type u_1
M : Type u_2
N : Type w
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : IsNoetherian R M
i f : N →ₗ[R] M
hi : Injective ⇑i
hf : Surjective ⇑f
this : IsNoetherian R N
⊢ Injective ⇑f

Proof state:
R : Type u_1
M : Type u_2
N : Type w
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : IsNoetherian R M
i f : N →ₗ[R] M
hi : Injective ⇑i
hf : Surjective ⇑f
this : IsNoetherian R N
⊢ Submodule.map f ⊥ ≤ Submodule.map i ⊥

Tactic:
simp

Result:
no goals

Proof state:
R : Type u_1
M : Type u_2
N : Type w
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : IsNoetherian R M
i f : N →ₗ[R] M
hi : Injective ⇑i
hf : Surjective ⇑f
this : IsNoetherian R N
⊢ Injective ⇑f

Tactic:
obtain ⟨n, H⟩ := monotone_stabilizes_iff_noetherian.2 ‹_›
  ⟨_, monotone_nat_of_le_succ <| f.iterateMapComap_le_succ i ⊥ (by simp)⟩

Result:
case intro
R : Type u_1
M : Type u_2
N : Type w
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : IsNoetherian R M
i f : N →ₗ[R] M
hi : Injective ⇑i
hf : Surjective ⇑f
this : IsNoetherian R N
n : ℕ
H :
  ∀ (m : ℕ),
    n ≤ m →
      { toFun := fun n => f.iterateMapComap i n ⊥, monotone' := ⋯ } n =
        { toFun := fun n => f.iterateMapComap i n ⊥, monotone' := ⋯ } m
⊢ Injective ⇑f

Proof state:
case intro
R : Type u_1
M : Type u_2
N : Type w
inst✝⁵ : Ring R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
inst✝ : IsNoetherian R M
i f : N →ₗ[R] M
hi : Injective ⇑i
hf : Surjective ⇑f
this : IsNoetherian R N
n : ℕ
H :
  ∀ (m : ℕ),
    n ≤ m →
      { toFun := fun n => f.iterateMapComap i n ⊥, monotone' := ⋯ } n =
        { toFun := fun n => f.iterateMapComap i n ⊥, monotone' := ⋯ } m
⊢ Injective ⇑f

Tactic:
exact LinearMap.ker_eq_bot.1 <| bot_unique <|
  f.ker_le_of_iterateMapComap_eq_succ i ⊥ n (H _ (Nat.le_succ _)) hf hi

Result:
no goals
-- Mathlib/Tactic/Push.lean
theorem not_nonempty_eq (s : Set β) : (¬ s.Nonempty) = (s = ∅)

Proof state:
β : Type u_2
s : Set β
A : ∀ (x : β), ¬x ∈ ∅
h : s = ∅
⊢ ∀ (x : β), ¬x ∈ s

Tactic:
rwa [h]

Result:
no goals

Proof state:
β : Type u_2
s : Set β
A : ∀ (x : β), ¬x ∈ ∅
⊢ (∀ (x : β), ¬x ∈ s) ↔ s = ∅

Tactic:
exact ⟨fun h ↦ Set.ext (fun x ↦ by simp only [h x, false_iff, A]), fun h ↦ by rwa [h]⟩

Result:
no goals

Proof state:
β : Type u_2
s : Set β
A : ∀ (x : β), ¬x ∈ ∅
h : ∀ (x : β), ¬x ∈ s
x : β
⊢ x ∈ s ↔ x ∈ ∅

Tactic:
simp only [h x, false_iff, A]

Result:
no goals

Proof state:
β : Type u_2
s : Set β
⊢ (¬s.Nonempty) = (s = ∅)

Tactic:
have A : ∀ (x : β), ¬(x ∈ (∅ : Set β)) := fun x ↦ id

Result:
β : Type u_2
s : Set β
A : ∀ (x : β), ¬x ∈ ∅
⊢ (¬s.Nonempty) = (s = ∅)

Proof state:
β : Type u_2
s : Set β
A : ∀ (x : β), ¬x ∈ ∅
⊢ (¬s.Nonempty) = (s = ∅)

Tactic:
simp only [Set.Nonempty, not_exists, eq_iff_iff]

Result:
β : Type u_2
s : Set β
A : ∀ (x : β), ¬x ∈ ∅
⊢ (∀ (x : β), ¬x ∈ s) ↔ s = ∅
-- Mathlib/.lake/packages/batteries/Batteries/Data/Vector/Monadic.lean
theorem mapIdxM_mk [Monad m] [LawfulMonad m] [MonadSatisfying m]
    (a : Array α) (h : a.size = n) (f : Nat → α → m β) :
    (Vector.mk a h).mapIdxM f =
      (fun ⟨a, h'⟩ => Vector.mk a (h'.trans h)) <$> satisfying (Array.size_mapIdxM a f)

Proof state:
m : Type u_1 → Type u_2
α : Type u_3
n : Nat
β : Type u_1
inst✝² : Monad m
inst✝¹ : LawfulMonad m
inst✝ : MonadSatisfying m
a : Array α
h : a.size = n
f : Nat → α → m β
⊢ mapIdxM f { toArray := a, size_toArray := h } =
    (fun x =>
        match x with
        | ⟨a_1, h'⟩ => { toArray := a_1, size_toArray := ⋯ }) <$>
      satisfying ⋯

Tactic:
rw [← LawfulMonad.map_inj_right Vector.toArray_inj.mp]

Result:
m : Type u_1 → Type u_2
α : Type u_3
n : Nat
β : Type u_1
inst✝² : Monad m
inst✝¹ : LawfulMonad m
inst✝ : MonadSatisfying m
a : Array α
h : a.size = n
f : Nat → α → m β
⊢ (fun {x} => x.toArray) <$> mapIdxM f { toArray := a, size_toArray := h } =
    (fun {x} => x.toArray) <$>
      (fun x =>
          match x with
          | ⟨a_1, h'⟩ => { toArray := a_1, size_toArray := ⋯ }) <$>
        satisfying ⋯

Proof state:
m : Type u_1 → Type u_2
α : Type u_3
n : Nat
β : Type u_1
inst✝² : Monad m
inst✝¹ : LawfulMonad m
inst✝ : MonadSatisfying m
a : Array α
h : a.size = n
f : Nat → α → m β
⊢ (fun {x} => x.toArray) <$> mapIdxM f { toArray := a, size_toArray := h } =
    (fun {x} => x.toArray) <$>
      (fun x =>
          match x with
          | ⟨a_1, h'⟩ => { toArray := a_1, size_toArray := ⋯ }) <$>
        satisfying ⋯

Tactic:
simp only [Functor.map_map, MonadSatisfying.val_eq, toArray_mapIdxM]

Result:
no goals
-- Mathlib/Analysis/Calculus/Deriv/Slope.lean
theorem HasDerivWithinAt.liminf_right_slope_norm_le (hf : HasDerivWithinAt f f' (Ici x) x)
    (hr : ‖f'‖ < r) : ∃ᶠ z in 𝓝[>] x, (z - x)⁻¹ * (‖f z‖ - ‖f x‖) < r

Proof state:
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
f' : E
x r : ℝ
hf : HasDerivWithinAt f f' (Ici x) x
hr : ‖f'‖ < r
⊢ ∃ᶠ (z : ℝ) in 𝓝[>] x, (z - x)⁻¹ * (‖f z‖ - ‖f x‖) < r

Tactic:
have := (hf.Ioi_of_Ici.limsup_slope_norm_le hr).frequently

Result:
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
f' : E
x r : ℝ
hf : HasDerivWithinAt f f' (Ici x) x
hr : ‖f'‖ < r
this : ∃ᶠ (x_1 : ℝ) in 𝓝[>] x, ‖x_1 - x‖⁻¹ * (‖f x_1‖ - ‖f x‖) < r
⊢ ∃ᶠ (z : ℝ) in 𝓝[>] x, (z - x)⁻¹ * (‖f z‖ - ‖f x‖) < r

Proof state:
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
f' : E
x r : ℝ
hf : HasDerivWithinAt f f' (Ici x) x
hr : ‖f'‖ < r
this : ∃ᶠ (x_1 : ℝ) in 𝓝[>] x, ‖x_1 - x‖⁻¹ * (‖f x_1‖ - ‖f x‖) < r
z : ℝ
hxz : x < z
hz : ‖z - x‖⁻¹ * (‖f z‖ - ‖f x‖) < r
⊢ (z - x)⁻¹ * (‖f z‖ - ‖f x‖) < r

Tactic:
rwa [Real.norm_eq_abs, abs_of_pos (sub_pos_of_lt hxz)] at hz

Result:
no goals

Proof state:
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
f' : E
x r : ℝ
hf : HasDerivWithinAt f f' (Ici x) x
hr : ‖f'‖ < r
this : ∃ᶠ (x_1 : ℝ) in 𝓝[>] x, ‖x_1 - x‖⁻¹ * (‖f x_1‖ - ‖f x‖) < r
⊢ ∃ᶠ (z : ℝ) in 𝓝[>] x, (z - x)⁻¹ * (‖f z‖ - ‖f x‖) < r

Tactic:
refine this.mp (Eventually.mono self_mem_nhdsWithin fun z hxz hz ↦ ?_)

Result:
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : ℝ → E
f' : E
x r : ℝ
hf : HasDerivWithinAt f f' (Ici x) x
hr : ‖f'‖ < r
this : ∃ᶠ (x_1 : ℝ) in 𝓝[>] x, ‖x_1 - x‖⁻¹ * (‖f x_1‖ - ‖f x‖) < r
z : ℝ
hxz : x < z
hz : ‖z - x‖⁻¹ * (‖f z‖ - ‖f x‖) < r
⊢ (z - x)⁻¹ * (‖f z‖ - ‖f x‖) < r
-- Mathlib/Order/CompleteLattice.lean
theorem iSup_option (f : Option β → α) : ⨆ o, f o = f none ⊔ ⨆ b, f (Option.some b) :=
  eq_of_forall_ge_iff fun c => by simp only [iSup_le_iff, sup_le_iff, Option.forall]

Proof state:
α : Type u_1
β : Type u_2
inst✝ : CompleteLattice α
f : Option β → α
c : α
⊢ ⨆ o, f o ≤ c ↔ f none ⊔ ⨆ b, f (some b) ≤ c

Tactic:
simp only [iSup_le_iff, sup_le_iff, Option.forall]

Result:
no goals
-- Mathlib/Data/Num/Lemmas.lean
theorem pred_to_nat : ∀ n : Num, (pred n : ℕ) = Nat.pred n
  | 0 => rfl
  | pos p => by rw [pred, PosNum.pred'_to_nat]; rfl

Proof state:
p : PosNum
⊢ (↑p).pred = (↑(pos p)).pred

Tactic:
rfl

Result:
no goals

Proof state:
p : PosNum
⊢ ↑(pos p).pred = (↑(pos p)).pred

Tactic:
rw [pred, PosNum.pred'_to_nat]

Result:
p : PosNum
⊢ (↑p).pred = (↑(pos p)).pred
-- Mathlib/Analysis/SpecialFunctions/Integrals.lean
theorem integral_cos_pow :
    (∫ x in a..b, cos x ^ (n + 2)) =
      (cos b ^ (n + 1) * sin b - cos a ^ (n + 1) * sin a) / (n + 2) +
        (n + 1) / (n + 2) * ∫ x in a..b, cos x ^ n

Proof state:
case h.e'_2
a b : ℝ
n : ℕ
⊢ (∫ (x : ℝ) in a..b, cos x ^ (n + 2)) * (↑n + 2) =
    (∫ (x : ℝ) in a..b, cos x ^ (n + 2)) + (↑n + 1) * ∫ (x : ℝ) in a..b, cos x ^ (n + 2)

Tactic:
ring

Result:
no goals

Proof state:
a b : ℝ
n : ℕ
⊢ ∫ (x : ℝ) in a..b, cos x ^ (n + 2) =
    (cos b ^ (n + 1) * sin b - cos a ^ (n + 1) * sin a) / (↑n + 2) + (↑n + 1) / (↑n + 2) * ∫ (x : ℝ) in a..b, cos x ^ n

Tactic:
field_simp

Result:
a b : ℝ
n : ℕ
⊢ (∫ (x : ℝ) in a..b, cos x ^ (n + 2)) * (↑n + 2) =
    cos b ^ (n + 1) * sin b - cos a ^ (n + 1) * sin a + (↑n + 1) * ∫ (x : ℝ) in a..b, cos x ^ n

Proof state:
a b : ℝ
n : ℕ
⊢ (∫ (x : ℝ) in a..b, cos x ^ (n + 2)) * (↑n + 2) =
    cos b ^ (n + 1) * sin b - cos a ^ (n + 1) * sin a + (↑n + 1) * ∫ (x : ℝ) in a..b, cos x ^ n

Tactic:
convert eq_sub_iff_add_eq.mp (integral_cos_pow_aux n) using 1

Result:
case h.e'_2
a b : ℝ
n : ℕ
⊢ (∫ (x : ℝ) in a..b, cos x ^ (n + 2)) * (↑n + 2) =
    (∫ (x : ℝ) in a..b, cos x ^ (n + 2)) + (↑n + 1) * ∫ (x : ℝ) in a..b, cos x ^ (n + 2)
-- Mathlib/Order/Filter/Basic.lean
theorem not_le : ¬f ≤ g ↔ ∃ s ∈ g, s ∉ f

Proof state:
α : Type u
f g : Filter α
⊢ ¬f ≤ g ↔ ∃ s ∈ g, s ∉ f

Tactic:
simp_rw [le_def, not_forall, exists_prop]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/EverywherePos.lean
/-- If two measures coincide locally, then a set which is everywhere positive for the former is
also everywhere positive for the latter. -/
lemma IsEverywherePos.of_forall_exists_nhds_eq (hs : IsEverywherePos μ s)
    (h : ∀ x ∈ s, ∃ t ∈ 𝓝 x, ∀ u ⊆ t, ν u = μ u) : IsEverywherePos ν s

Proof state:
case intro.intro
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : MeasurableSpace α
μ ν : Measure α
s : Set α
hs : μ.IsEverywherePos s
h : ∀ x ∈ s, ∃ t ∈ 𝓝 x, ∀ u ⊆ t, ν u = μ u
x : α
hx : x ∈ s
n : Set α
hn : n ∈ 𝓝[s] x
t : Set α
t_mem : t ∈ 𝓝 x
ht : ∀ u ⊆ t, ν u = μ u
⊢ 0 < ν (n ∩ t)

Tactic:
rw [ht (n ∩ t) inter_subset_right]

Result:
case intro.intro
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : MeasurableSpace α
μ ν : Measure α
s : Set α
hs : μ.IsEverywherePos s
h : ∀ x ∈ s, ∃ t ∈ 𝓝 x, ∀ u ⊆ t, ν u = μ u
x : α
hx : x ∈ s
n : Set α
hn : n ∈ 𝓝[s] x
t : Set α
t_mem : t ∈ 𝓝 x
ht : ∀ u ⊆ t, ν u = μ u
⊢ 0 < μ (n ∩ t)

Proof state:
case intro.intro
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : MeasurableSpace α
μ ν : Measure α
s : Set α
hs : μ.IsEverywherePos s
h : ∀ x ∈ s, ∃ t ∈ 𝓝 x, ∀ u ⊆ t, ν u = μ u
x : α
hx : x ∈ s
n : Set α
hn : n ∈ 𝓝[s] x
t : Set α
t_mem : t ∈ 𝓝 x
ht : ∀ u ⊆ t, ν u = μ u
⊢ 0 < ν n

Tactic:
refine lt_of_lt_of_le ?_ (measure_mono (inter_subset_left (t := t)))

Result:
case intro.intro
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : MeasurableSpace α
μ ν : Measure α
s : Set α
hs : μ.IsEverywherePos s
h : ∀ x ∈ s, ∃ t ∈ 𝓝 x, ∀ u ⊆ t, ν u = μ u
x : α
hx : x ∈ s
n : Set α
hn : n ∈ 𝓝[s] x
t : Set α
t_mem : t ∈ 𝓝 x
ht : ∀ u ⊆ t, ν u = μ u
⊢ 0 < ν (n ∩ t)

Proof state:
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : MeasurableSpace α
μ ν : Measure α
s : Set α
hs : μ.IsEverywherePos s
h : ∀ x ∈ s, ∃ t ∈ 𝓝 x, ∀ u ⊆ t, ν u = μ u
⊢ ν.IsEverywherePos s

Tactic:
intro x hx n hn

Result:
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : MeasurableSpace α
μ ν : Measure α
s : Set α
hs : μ.IsEverywherePos s
h : ∀ x ∈ s, ∃ t ∈ 𝓝 x, ∀ u ⊆ t, ν u = μ u
x : α
hx : x ∈ s
n : Set α
hn : n ∈ 𝓝[s] x
⊢ 0 < ν n

Proof state:
case intro.intro
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : MeasurableSpace α
μ ν : Measure α
s : Set α
hs : μ.IsEverywherePos s
h : ∀ x ∈ s, ∃ t ∈ 𝓝 x, ∀ u ⊆ t, ν u = μ u
x : α
hx : x ∈ s
n : Set α
hn : n ∈ 𝓝[s] x
t : Set α
t_mem : t ∈ 𝓝 x
ht : ∀ u ⊆ t, ν u = μ u
⊢ 0 < μ (n ∩ t)

Tactic:
exact hs x hx _ (inter_mem hn (mem_nhdsWithin_of_mem_nhds t_mem))

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : MeasurableSpace α
μ ν : Measure α
s : Set α
hs : μ.IsEverywherePos s
h : ∀ x ∈ s, ∃ t ∈ 𝓝 x, ∀ u ⊆ t, ν u = μ u
x : α
hx : x ∈ s
n : Set α
hn : n ∈ 𝓝[s] x
⊢ 0 < ν n

Tactic:
rcases h x hx with ⟨t, t_mem, ht⟩

Result:
case intro.intro
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : MeasurableSpace α
μ ν : Measure α
s : Set α
hs : μ.IsEverywherePos s
h : ∀ x ∈ s, ∃ t ∈ 𝓝 x, ∀ u ⊆ t, ν u = μ u
x : α
hx : x ∈ s
n : Set α
hn : n ∈ 𝓝[s] x
t : Set α
t_mem : t ∈ 𝓝 x
ht : ∀ u ⊆ t, ν u = μ u
⊢ 0 < ν n
-- Mathlib/Algebra/Order/Ring/Basic.lean
lemma Odd.pow_nonpos_iff (hn : Odd n) : a ^ n ≤ 0 ↔ a ≤ 0

Proof state:
R : Type u_3
inst✝¹ : LinearOrderedSemiring R
a : R
n : ℕ
inst✝ : ExistsAddOfLE R
hn : Odd n
⊢ a ^ n ≤ 0 ↔ a ≤ 0

Tactic:
rw [le_iff_lt_or_eq, le_iff_lt_or_eq, hn.pow_neg_iff, pow_eq_zero_iff]

Result:
R : Type u_3
inst✝¹ : LinearOrderedSemiring R
a : R
n : ℕ
inst✝ : ExistsAddOfLE R
hn : Odd n
⊢ n ≠ 0

Proof state:
R : Type u_3
inst✝¹ : LinearOrderedSemiring R
a : R
inst✝ : ExistsAddOfLE R
hn : Odd 0
⊢ False

Tactic:
simp [Odd, eq_comm (a := 0)] at hn

Result:
no goals

Proof state:
R : Type u_3
inst✝¹ : LinearOrderedSemiring R
a : R
n : ℕ
inst✝ : ExistsAddOfLE R
hn : Odd n
⊢ n ≠ 0

Tactic:
rintro rfl

Result:
R : Type u_3
inst✝¹ : LinearOrderedSemiring R
a : R
inst✝ : ExistsAddOfLE R
hn : Odd 0
⊢ False
-- Mathlib/Analysis/Calculus/ContDiff/Operations.lean
theorem ContDiffAt.prod_map' {f : E → F} {g : E' → F'} {p : E × E'} (hf : ContDiffAt 𝕜 n f p.1)
    (hg : ContDiffAt 𝕜 n g p.2) : ContDiffAt 𝕜 n (Prod.map f g) p

Proof state:
case mk
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type uF
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
n : WithTop ℕ∞
E' : Type u_3
inst✝³ : NormedAddCommGroup E'
inst✝² : NormedSpace 𝕜 E'
F' : Type u_4
inst✝¹ : NormedAddCommGroup F'
inst✝ : NormedSpace 𝕜 F'
f : E → F
g : E' → F'
fst✝ : E
snd✝ : E'
hf : ContDiffAt 𝕜 n f (fst✝, snd✝).1
hg : ContDiffAt 𝕜 n g (fst✝, snd✝).2
⊢ ContDiffAt 𝕜 n (Prod.map f g) (fst✝, snd✝)

Tactic:
exact ContDiffAt.prod_map hf hg

Result:
no goals

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
n : WithTop ℕ∞
E' : Type u_3
inst✝³ : NormedAddCommGroup E'
inst✝² : NormedSpace 𝕜 E'
F' : Type u_4
inst✝¹ : NormedAddCommGroup F'
inst✝ : NormedSpace 𝕜 F'
f : E → F
g : E' → F'
p : E × E'
hf : ContDiffAt 𝕜 n f p.1
hg : ContDiffAt 𝕜 n g p.2
⊢ ContDiffAt 𝕜 n (Prod.map f g) p

Tactic:
rcases p with ⟨⟩

Result:
case mk
𝕜 : Type u_1
inst✝⁸ : NontriviallyNormedField 𝕜
E : Type uE
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace 𝕜 E
F : Type uF
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
n : WithTop ℕ∞
E' : Type u_3
inst✝³ : NormedAddCommGroup E'
inst✝² : NormedSpace 𝕜 E'
F' : Type u_4
inst✝¹ : NormedAddCommGroup F'
inst✝ : NormedSpace 𝕜 F'
f : E → F
g : E' → F'
fst✝ : E
snd✝ : E'
hf : ContDiffAt 𝕜 n f (fst✝, snd✝).1
hg : ContDiffAt 𝕜 n g (fst✝, snd✝).2
⊢ ContDiffAt 𝕜 n (Prod.map f g) (fst✝, snd✝)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/String/Basic.lean
theorem prevn_zero (s : Substring) : ∀ n, s.prevn n 0 = 0
  | 0 => rfl
  | n+1 => by simp [prevn, prevn_zero s n]

Proof state:
s : Substring
n : Nat
⊢ s.prevn (n + 1) 0 = 0

Tactic:
simp [prevn, prevn_zero s n]

Result:
no goals
-- Mathlib/Order/BooleanAlgebra.lean
theorem inf_sdiff_distrib_right (a b c : α) : a \ b ⊓ c = (a ⊓ c) \ (b ⊓ c)

Proof state:
α : Type u
inst✝ : GeneralizedBooleanAlgebra α
a b c : α
⊢ a \ b ⊓ c = (a ⊓ c) \ (b ⊓ c)

Tactic:
simp_rw [inf_comm _ c, inf_sdiff_distrib_left]

Result:
no goals
-- Mathlib/CategoryTheory/Monoidal/Braided/Basic.lean
theorem braiding_tensorUnit_right (X : C) : (β_ X (𝟙_ C)).hom = (ρ_ X).hom ≫ (λ_ X).inv

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X : C
⊢ (β_ X (𝟙_ C)).hom = (ρ_ X).hom ≫ (λ_ X).inv

Tactic:
simp [← rightUnitor_inv_braiding]

Result:
no goals
-- Mathlib/Algebra/EuclideanDomain/Defs.lean
theorem div_add_mod' (m k : R) : m / k * k + m % k = m

Proof state:
R : Type u
inst✝ : EuclideanDomain R
m k : R
⊢ m / k * k + m % k = m

Tactic:
rw [mul_comm]

Result:
R : Type u
inst✝ : EuclideanDomain R
m k : R
⊢ k * (m / k) + m % k = m

Proof state:
R : Type u
inst✝ : EuclideanDomain R
m k : R
⊢ k * (m / k) + m % k = m

Tactic:
exact div_add_mod _ _

Result:
no goals
-- Mathlib/Analysis/Convex/Between.lean
theorem AffineEquiv.sbtw_map_iff {x y z : P} (f : P ≃ᵃ[R] P') :
    Sbtw R (f x) (f y) (f z) ↔ Sbtw R x y z

Proof state:
R : Type u_1
V : Type u_2
V' : Type u_3
P : Type u_4
P' : Type u_5
inst✝⁶ : OrderedRing R
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module R V
inst✝³ : AddTorsor V P
inst✝² : AddCommGroup V'
inst✝¹ : Module R V'
inst✝ : AddTorsor V' P'
x y z : P
f : P ≃ᵃ[R] P'
this : Function.Injective ⇑↑f
⊢ Sbtw R (f x) (f y) (f z) ↔ Sbtw R x y z

Tactic:
apply this.sbtw_map_iff

Result:
no goals

Proof state:
R : Type u_1
V : Type u_2
V' : Type u_3
P : Type u_4
P' : Type u_5
inst✝⁶ : OrderedRing R
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module R V
inst✝³ : AddTorsor V P
inst✝² : AddCommGroup V'
inst✝¹ : Module R V'
inst✝ : AddTorsor V' P'
x y z : P
f : P ≃ᵃ[R] P'
⊢ Sbtw R (f x) (f y) (f z) ↔ Sbtw R x y z

Tactic:
have : Function.Injective f.toAffineMap := f.injective

Result:
R : Type u_1
V : Type u_2
V' : Type u_3
P : Type u_4
P' : Type u_5
inst✝⁶ : OrderedRing R
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module R V
inst✝³ : AddTorsor V P
inst✝² : AddCommGroup V'
inst✝¹ : Module R V'
inst✝ : AddTorsor V' P'
x y z : P
f : P ≃ᵃ[R] P'
this : Function.Injective ⇑↑f
⊢ Sbtw R (f x) (f y) (f z) ↔ Sbtw R x y z
-- Mathlib/Data/DFinsupp/Order.lean
theorem single_tsub : single i (a - b) = single i a - single i b

Proof state:
case h.inl
ι : Type u_1
α : ι → Type u_2
inst✝⁵ : (i : ι) → AddCommMonoid (α i)
inst✝⁴ : (i : ι) → PartialOrder (α i)
inst✝³ : ∀ (i : ι), CanonicallyOrderedAdd (α i)
inst✝² : (i : ι) → Sub (α i)
inst✝¹ : ∀ (i : ι), OrderedSub (α i)
i : ι
a b : α i
inst✝ : DecidableEq ι
⊢ (single i (a - b)) i = (single i a - single i b) i

Tactic:
rw [tsub_apply, single_eq_same, single_eq_same, single_eq_same]

Result:
no goals

Proof state:
ι : Type u_1
α : ι → Type u_2
inst✝⁵ : (i : ι) → AddCommMonoid (α i)
inst✝⁴ : (i : ι) → PartialOrder (α i)
inst✝³ : ∀ (i : ι), CanonicallyOrderedAdd (α i)
inst✝² : (i : ι) → Sub (α i)
inst✝¹ : ∀ (i : ι), OrderedSub (α i)
i : ι
a b : α i
inst✝ : DecidableEq ι
⊢ single i (a - b) = single i a - single i b

Tactic:
ext j

Result:
case h
ι : Type u_1
α : ι → Type u_2
inst✝⁵ : (i : ι) → AddCommMonoid (α i)
inst✝⁴ : (i : ι) → PartialOrder (α i)
inst✝³ : ∀ (i : ι), CanonicallyOrderedAdd (α i)
inst✝² : (i : ι) → Sub (α i)
inst✝¹ : ∀ (i : ι), OrderedSub (α i)
i : ι
a b : α i
inst✝ : DecidableEq ι
j : ι
⊢ (single i (a - b)) j = (single i a - single i b) j

Proof state:
case h.inr
ι : Type u_1
α : ι → Type u_2
inst✝⁵ : (i : ι) → AddCommMonoid (α i)
inst✝⁴ : (i : ι) → PartialOrder (α i)
inst✝³ : ∀ (i : ι), CanonicallyOrderedAdd (α i)
inst✝² : (i : ι) → Sub (α i)
inst✝¹ : ∀ (i : ι), OrderedSub (α i)
i : ι
a b : α i
inst✝ : DecidableEq ι
j : ι
h : i ≠ j
⊢ (single i (a - b)) j = (single i a - single i b) j

Tactic:
rw [tsub_apply, single_eq_of_ne h, single_eq_of_ne h, single_eq_of_ne h, tsub_self]

Result:
no goals

Proof state:
case h
ι : Type u_1
α : ι → Type u_2
inst✝⁵ : (i : ι) → AddCommMonoid (α i)
inst✝⁴ : (i : ι) → PartialOrder (α i)
inst✝³ : ∀ (i : ι), CanonicallyOrderedAdd (α i)
inst✝² : (i : ι) → Sub (α i)
inst✝¹ : ∀ (i : ι), OrderedSub (α i)
i : ι
a b : α i
inst✝ : DecidableEq ι
j : ι
⊢ (single i (a - b)) j = (single i a - single i b) j

Tactic:
obtain rfl | h := eq_or_ne i j

Result:
case h.inl
ι : Type u_1
α : ι → Type u_2
inst✝⁵ : (i : ι) → AddCommMonoid (α i)
inst✝⁴ : (i : ι) → PartialOrder (α i)
inst✝³ : ∀ (i : ι), CanonicallyOrderedAdd (α i)
inst✝² : (i : ι) → Sub (α i)
inst✝¹ : ∀ (i : ι), OrderedSub (α i)
i : ι
a b : α i
inst✝ : DecidableEq ι
⊢ (single i (a - b)) i = (single i a - single i b) i

case h.inr
ι : Type u_1
α : ι → Type u_2
inst✝⁵ : (i : ι) → AddCommMonoid (α i)
inst✝⁴ : (i : ι) → PartialOrder (α i)
inst✝³ : ∀ (i : ι), CanonicallyOrderedAdd (α i)
inst✝² : (i : ι) → Sub (α i)
inst✝¹ : ∀ (i : ι), OrderedSub (α i)
i : ι
a b : α i
inst✝ : DecidableEq ι
j : ι
h : i ≠ j
⊢ (single i (a - b)) j = (single i a - single i b) j