harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/Calculus/FDeriv/Equiv.lean
theorem comp_differentiableOn_iff {f : G → E} {s : Set G} :
    DifferentiableOn 𝕜 (iso ∘ f) s ↔ DifferentiableOn 𝕜 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
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
iso : E ≃L[𝕜] F
f : G → E
s : Set G
⊢ DifferentiableOn 𝕜 (⇑iso ∘ f) s ↔ DifferentiableOn 𝕜 f s

Tactic:
rw [DifferentiableOn, DifferentiableOn]

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
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
iso : E ≃L[𝕜] F
f : G → E
s : Set G
⊢ (∀ x ∈ s, DifferentiableWithinAt 𝕜 (⇑iso ∘ f) s x) ↔ ∀ x ∈ s, DifferentiableWithinAt 𝕜 f s x

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
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
iso : E ≃L[𝕜] F
f : G → E
s : Set G
⊢ (∀ x ∈ s, DifferentiableWithinAt 𝕜 (⇑iso ∘ f) s x) ↔ ∀ x ∈ s, DifferentiableWithinAt 𝕜 f s x

Tactic:
simp only [iso.comp_differentiableWithinAt_iff]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/DivModLemmas.lean
theorem lt_tdiv_add_one_mul_self (a : Int) {b : Int} (H : 0 < b) : a < (a.tdiv b + 1) * b

Proof state:
a b : Int
H : 0 < b
⊢ a < b * a.tdiv b + b

Tactic:
exact Int.lt_add_of_sub_left_lt <| Int.tmod_def .. ▸ tmod_lt_of_pos _ H

Result:
no goals

Proof state:
a b : Int
H : 0 < b
⊢ a < (a.tdiv b + 1) * b

Tactic:
rw [Int.add_mul, Int.one_mul, Int.mul_comm]

Result:
a b : Int
H : 0 < b
⊢ a < b * a.tdiv b + b
-- Mathlib/MeasureTheory/Function/L1Space/HasFiniteIntegral.lean
lemma lintegral_enorm_eq_lintegral_edist (f : α → β) :
    ∫⁻ a, ‖f a‖ₑ ∂μ = ∫⁻ a, edist (f a) 0 ∂μ

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f : α → β
⊢ ∫⁻ (a : α), ‖f a‖ₑ ∂μ = ∫⁻ (a : α), edist (f a) 0 ∂μ

Tactic:
simp only [edist_zero_eq_enorm]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Control/Lawful/Basic.lean
theorem LawfulMonad.map_pure' [Monad m] [LawfulMonad m] {a : α} :
    (f <$> pure a : m β) = pure (f a)

Proof state:
m : Type u_1 → Type u_2
α β : Type u_1
f : α → β
inst✝¹ : Monad m
inst✝ : LawfulMonad m
a : α
⊢ f <$> pure a = pure (f a)

Tactic:
simp only [map_pure]

Result:
no goals
-- Mathlib/Algebra/Order/Star/Basic.lean
theorem IsSelfAdjoint.mul_self_nonneg {a : R} (ha : IsSelfAdjoint a) : 0 ≤ a * a

Proof state:
R : Type u
inst✝³ : NonUnitalSemiring R
inst✝² : PartialOrder R
inst✝¹ : StarRing R
inst✝ : StarOrderedRing R
a : R
ha : IsSelfAdjoint a
⊢ 0 ≤ a * a

Tactic:
simpa [ha.star_eq] using star_mul_self_nonneg a

Result:
no goals
-- Mathlib/Analysis/NormedSpace/Pointwise.lean
theorem ball_sub_closedBall (hε : 0 < ε) (hδ : 0 ≤ δ) (a b : E) :
    ball a ε - closedBall b δ = ball (a - b) (ε + δ)

Proof state:
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
δ ε : ℝ
hε : 0 < ε
hδ : 0 ≤ δ
a b : E
⊢ Metric.ball a ε - Metric.closedBall b δ = Metric.ball (a - b) (ε + δ)

Tactic:
simp_rw [sub_eq_add_neg, neg_closedBall, ball_add_closedBall hε hδ]

Result:
no goals
-- Mathlib/Data/PFun.lean
theorem comp_assoc (f : γ →. δ) (g : β →. γ) (h : α →. β) : (f.comp g).comp h = f.comp (g.comp h) :=
  ext fun _ _ => by simp only [comp_apply, Part.bind_comp]

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
f : γ →. δ
g : β →. γ
h : α →. β
x✝¹ : α
x✝ : δ
⊢ x✝ ∈ (f.comp g).comp h x✝¹ ↔ x✝ ∈ f.comp (g.comp h) x✝¹

Tactic:
simp only [comp_apply, Part.bind_comp]

Result:
no goals
-- Mathlib/Geometry/Manifold/Complex.lean
theorem eqOn_of_isPreconnected_of_isMaxOn_norm [StrictConvexSpace ℝ F] {f : M → F} {U : Set M}
    {c : M} (hd : MDifferentiableOn I 𝓘(ℂ, F) f U) (hc : IsPreconnected U) (ho : IsOpen U)
    (hcU : c ∈ U) (hm : IsMaxOn (norm ∘ f) U c) : EqOn f (const M (f c)) U := fun x hx =>
  have H₁ : ‖f x‖ = ‖f c‖ := hd.norm_eqOn_of_isPreconnected_of_isMaxOn hc ho hcU hm hx
  -- TODO: Add `MDifferentiableOn.add` etc; does it mean importing `Manifold.Algebra.Monoid`?
  have hd' : MDifferentiableOn I 𝓘(ℂ, F) (f · + f c) U := fun x hx ↦
    ⟨(hd x hx).1.add continuousWithinAt_const, (hd x hx).2.add_const _⟩
  have H₂ : ‖f x + f c‖ = ‖f c + f c‖ :=
    hd'.norm_eqOn_of_isPreconnected_of_isMaxOn hc ho hcU hm.norm_add_self hx
  eq_of_norm_eq_of_norm_add_eq H₁ <| by simp only [H₂, SameRay.rfl.norm_add, H₁, Function.const]

Proof state:
E : Type u_1
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace ℂ E
F : Type u_2
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℂ F
H : Type u_3
inst✝⁵ : TopologicalSpace H
I : ModelWithCorners ℂ E H
inst✝⁴ : I.Boundaryless
M : Type u_4
inst✝³ : TopologicalSpace M
inst✝² : ChartedSpace H M
inst✝¹ : IsManifold I 1 M
inst✝ : StrictConvexSpace ℝ F
f : M → F
U : Set M
c : M
hd : MDifferentiableOn I 𝓘(ℂ, F) f U
hc : IsPreconnected U
ho : IsOpen U
hcU : c ∈ U
hm : IsMaxOn (norm ∘ f) U c
x : M
hx : x ∈ U
H₁ : ‖f x‖ = ‖f c‖
hd' : MDifferentiableOn I 𝓘(ℂ, F) (fun x => f x + f c) U
H₂ : ‖f x + f c‖ = ‖f c + f c‖
⊢ ‖f x + const M (f c) x‖ = ‖f x‖ + ‖const M (f c) x‖

Tactic:
simp only [H₂, SameRay.rfl.norm_add, H₁, Function.const]

Result:
no goals
-- Mathlib/Order/WithBot.lean
lemma lt_untop_iff (hy : y ≠ ⊤) : a < y.untop hy ↔ a < y

Proof state:
case intro
α : Type u_1
a : α
inst✝ : LT α
y : α
hy : ↑y ≠ ⊤
⊢ a < (↑y).untop hy ↔ ↑a < ↑y

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
a : α
inst✝ : LT α
y : WithTop α
hy : y ≠ ⊤
⊢ a < y.untop hy ↔ ↑a < y

Tactic:
lift y to α using id hy

Result:
case intro
α : Type u_1
a : α
inst✝ : LT α
y : α
hy : ↑y ≠ ⊤
⊢ a < (↑y).untop hy ↔ ↑a < ↑y
-- Mathlib/Algebra/BigOperators/Ring/Finset.lean
lemma natCast_card_filter (p) [DecidablePred p] (s : Finset ι) :
    (#{x ∈ s | p x} : α) = ∑ a ∈ s, if p a then (1 : α) else 0

Proof state:
ι : Type u_1
α : Type u_3
inst✝¹ : AddCommMonoidWithOne α
p : ι → Prop
inst✝ : DecidablePred p
s : Finset ι
⊢ ↑(#(filter (fun x => p x) s)) = ∑ a ∈ s, if p a then 1 else 0

Tactic:
rw [sum_ite, sum_const_zero, add_zero, sum_const, nsmul_one]

Result:
no goals
-- Mathlib/RingTheory/KrullDimension/Basic.lean
lemma Ring.KrullDimLE.mk₀ (H : ∀ I : Ideal R, I.IsPrime → I.IsMaximal) : Ring.KrullDimLE 0 R

Proof state:
R : Type u_1
inst✝ : CommSemiring R
H : ∀ (I : Ideal R), I.IsPrime → I.IsMaximal
⊢ KrullDimLE 0 R

Tactic:
rwa [Ring.krullDimLE_zero_iff]

Result:
no goals
-- Mathlib/Topology/Algebra/Group/Basic.lean
lemma Filter.tendsto_div_const_iff {G : Type*}
    [CommGroupWithZero G] [TopologicalSpace G] [ContinuousDiv G]
    {b : G} (hb : b ≠ 0) {c : G} {f : α → G} {l : Filter α} :
    Tendsto (f · / b) l (𝓝 (c / b)) ↔ Tendsto f l (𝓝 c)

Proof state:
α : Type u
G : Type u_1
inst✝² : CommGroupWithZero G
inst✝¹ : TopologicalSpace G
inst✝ : ContinuousDiv G
b : G
hb : b ≠ 0
c : G
f : α → G
l : Filter α
⊢ Tendsto (fun x => f x / b) l (𝓝 (c / b)) ↔ Tendsto f l (𝓝 c)

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ Filter.Tendsto.div_const' h b⟩

Result:
α : Type u
G : Type u_1
inst✝² : CommGroupWithZero G
inst✝¹ : TopologicalSpace G
inst✝ : ContinuousDiv G
b : G
hb : b ≠ 0
c : G
f : α → G
l : Filter α
h : Tendsto (fun x => f x / b) l (𝓝 (c / b))
⊢ Tendsto f l (𝓝 c)

Proof state:
α : Type u
G : Type u_1
inst✝² : CommGroupWithZero G
inst✝¹ : TopologicalSpace G
inst✝ : ContinuousDiv G
b : G
hb : b ≠ 0
c : G
f : α → G
l : Filter α
h : Tendsto (fun x => f x / b) l (𝓝 (c / b))
⊢ Tendsto f l (𝓝 c)

Tactic:
convert h.div_const' b⁻¹ with k <;> rw [div_div, mul_inv_cancel₀ hb, div_one]

Result:
no goals
-- Mathlib/RepresentationTheory/Basic.lean
theorem asAlgebraHom_single (g : G) (r : k) : asAlgebraHom ρ (Finsupp.single g r) = r • ρ g

Proof state:
k : Type u_1
G : Type u_2
V : Type u_3
inst✝³ : CommSemiring k
inst✝² : Monoid G
inst✝¹ : AddCommMonoid V
inst✝ : Module k V
ρ : Representation k G V
g : G
r : k
⊢ ρ.asAlgebraHom (Finsupp.single g r) = r • ρ g

Tactic:
simp only [asAlgebraHom_def, MonoidAlgebra.lift_single]

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Arithmetic.lean
theorem mk_embedding_eq_zero_iff_lt : #(α ↪ β) = 0 ↔ #β < #α

Proof state:
α β : Type u
⊢ #(α ↪ β) = 0 ↔ #β < #α

Tactic:
rw [mk_embedding_eq_zero_iff_lift_lt, lift_lt]

Result:
no goals
-- Mathlib/Topology/MetricSpace/Pseudo/Basic.lean
theorem Metric.inseparable_iff {x y : α} : Inseparable x y ↔ dist x y = 0

Proof state:
α : Type u
inst✝ : PseudoMetricSpace α
x y : α
⊢ Inseparable x y ↔ dist x y = 0

Tactic:
rw [Metric.inseparable_iff_nndist, dist_nndist, NNReal.coe_eq_zero]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Nat/Range.lean
theorem map_sub_range' (a s n : Nat) (h : a ≤ s) :
    map (· - a) (range' s n step) = range' (s - a) n step

Proof state:
case h
step a s n : Nat
h : a ≤ s
x : Nat
⊢ ((fun x => x - a) ∘ fun x => a + x) x = id x

Tactic:
apply Nat.add_sub_cancel_left

Result:
no goals

Proof state:
step a s n : Nat
h : a ≤ s
⊢ map (fun x => x - a) (range' s n step) = range' (s - a) n step

Tactic:
conv => lhs; rw [← Nat.add_sub_cancel' h]

Result:
step a s n : Nat
h : a ≤ s
⊢ map (fun x => x - a) (range' (a + (s - a)) n step) = range' (s - a) n step

Proof state:
step a s n : Nat
h : a ≤ s
⊢ map (fun x => x - a) (range' (a + (s - a)) n step) = range' (s - a) n step

Tactic:
rw [← map_add_range', map_map, (?_ : _∘_ = _), map_id]

Result:
step a s n : Nat
h : a ≤ s
⊢ ((fun x => x - a) ∘ fun x => a + x) = id

Proof state:
step a s n : Nat
h : a ≤ s
⊢ ((fun x => x - a) ∘ fun x => a + x) = id

Tactic:
funext x

Result:
case h
step a s n : Nat
h : a ≤ s
x : Nat
⊢ ((fun x => x - a) ∘ fun x => a + x) x = id x
-- Mathlib/Analysis/Normed/Group/HomCompletion.lean
theorem NormedAddGroupHom.norm_completion (f : NormedAddGroupHom G H) : ‖f.completion‖ = ‖f‖ :=
  le_antisymm (ofLipschitz_norm_le _ _) <| opNorm_le_bound _ (norm_nonneg _) fun x => by
    simpa using f.completion.le_opNorm x

Proof state:
G : Type u_1
inst✝¹ : SeminormedAddCommGroup G
H : Type u_2
inst✝ : SeminormedAddCommGroup H
f : NormedAddGroupHom G H
x : G
⊢ ‖f x‖ ≤ ‖f.completion‖ * ‖x‖

Tactic:
simpa using f.completion.le_opNorm x

Result:
no goals
-- Mathlib/Logic/Lemmas.lean
theorem iff_right_comm {a b c : Prop} : ((a ↔ b) ↔ c) ↔ ((a ↔ c) ↔ b)

Proof state:
a b c : Prop
⊢ ((a ↔ b) ↔ c) ↔ ((a ↔ c) ↔ b)

Tactic:
tauto

Result:
no goals
-- Mathlib/Analysis/Calculus/ContDiff/FTaylorSeries.lean
/-- The iterated derivative commutes with subtracting a constant. -/
lemma iteratedFDerivWithin_comp_sub' (n : ℕ) (a : E) :
    iteratedFDerivWithin 𝕜 n (fun z ↦ f (z - a)) s =
      fun x ↦ iteratedFDerivWithin 𝕜 n f (-a +ᵥ s) (x - a)

Proof state:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
f : E → F
n : ℕ
a : E
⊢ iteratedFDerivWithin 𝕜 n (fun z => f (z - a)) s = fun x => iteratedFDerivWithin 𝕜 n f (-a +ᵥ s) (x - a)

Tactic:
simpa [sub_eq_add_neg] using iteratedFDerivWithin_comp_add_right' n (-a)

Result:
no goals
-- Mathlib/Algebra/Order/Sub/Defs.lean
theorem tsub_add_eq_tsub_tsub_swap (a b c : α) : a - (b + c) = a - c - b

Proof state:
α : Type u_1
inst✝³ : PartialOrder α
inst✝² : AddCommSemigroup α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c : α
⊢ a - (c + b) = a - c - b

Tactic:
apply tsub_add_eq_tsub_tsub

Result:
no goals

Proof state:
α : Type u_1
inst✝³ : PartialOrder α
inst✝² : AddCommSemigroup α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c : α
⊢ a - (b + c) = a - c - b

Tactic:
rw [add_comm]

Result:
α : Type u_1
inst✝³ : PartialOrder α
inst✝² : AddCommSemigroup α
inst✝¹ : Sub α
inst✝ : OrderedSub α
a b c : α
⊢ a - (c + b) = a - c - b
-- Mathlib/Data/Set/NAry.lean
theorem image2_singleton_right : image2 f s {b} = (fun a => f a b) '' s :=
  ext fun x => by simp

Proof state:
α : Type u_1
β : Type u_3
γ : Type u_5
f : α → β → γ
s : Set α
b : β
x : γ
⊢ x ∈ image2 f s {b} ↔ x ∈ (fun a => f a b) '' s

Tactic:
simp

Result:
no goals
-- Mathlib/RingTheory/DedekindDomain/SelmerGroup.lean
theorem valuation_of_unit_mod_eq (n : ℕ) (x : Rˣ) :
    v.valuationOfNeZeroMod n (Units.map (algebraMap R K : R →* K) x : K/n) = 1

Proof state:
R : Type u
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
K : Type v
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
v : HeightOneSpectrum R
n : ℕ
x : Rˣ
⊢ (v.valuationOfNeZeroMod n) ↑((Units.map ↑(algebraMap R K)) x) = 1

Tactic:
erw [valuationOfNeZeroMod, MonoidHom.comp_apply, ← QuotientGroup.coe_mk',
  QuotientGroup.map_mk' (G := Kˣ) (N := MonoidHom.range (powMonoidHom n)),
  valuation_of_unit_eq, QuotientGroup.mk_one, map_one]

Result:
no goals
-- Mathlib/Algebra/Group/Submonoid/Defs.lean
@[to_additive (attr := simp)]
lemma mk_eq_one {a : M} {ha} : (⟨a, ha⟩ : S) = 1 ↔ a = 1

Proof state:
M : Type u_4
inst✝ : MulOneClass M
S : Submonoid M
a : M
ha : a ∈ S
⊢ ⟨a, ha⟩ = 1 ↔ a = 1

Tactic:
simp [← SetLike.coe_eq_coe]

Result:
no goals
-- Mathlib/Algebra/Group/Pointwise/Set/Basic.lean
theorem preimage_mul_left_one' : (a⁻¹ * ·) ⁻¹' 1 = {a}

Proof state:
α : Type u_2
inst✝ : Group α
a : α
⊢ (fun x => a⁻¹ * x) ⁻¹' 1 = {a}

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Seq/Seq.lean
theorem ofStream_append (l : List α) (s : Stream' α) :
    ofStream (l ++ₛ s) = append (ofList l) (ofStream s)

Proof state:
α : Type u
l : List α
s : Stream' α
⊢ ↑(l ++ₛ s) = (↑l).append ↑s

Tactic:
induction l <;> simp [*, Stream'.nil_append_stream, Stream'.cons_append_stream]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/WF.lean
theorem getKeyDₘ_eq_getKeyD [BEq α] [Hashable α] [EquivBEq α] [LawfulHashable α] {m : Raw₀ α β}
    (hm : Raw.WFImp m.1) {a fallback : α} :
    m.getKeyDₘ a fallback = List.getKeyD a (toListModel m.1.buckets) fallback

Proof state:
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
m : Raw₀ α β
hm : Raw.WFImp m.val
a fallback : α
⊢ m.getKeyDₘ a fallback = List.getKeyD a (toListModel m.val.buckets) fallback

Tactic:
rw [getKeyDₘ, getKey?ₘ_eq_getKey? hm, List.getKeyD_eq_getKey?]

Result:
no goals
-- Mathlib/Analysis/Calculus/Deriv/Mul.lean
theorem derivWithin_smul (hc : DifferentiableWithinAt 𝕜 c s x)
    (hf : DifferentiableWithinAt 𝕜 f s x) :
    derivWithin (fun y => c y • f y) s x = c x • derivWithin f s x + derivWithin c s x • f x

Proof state:
case inr
𝕜 : Type u
inst✝⁶ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
f : 𝕜 → F
x : 𝕜
s : Set 𝕜
𝕜' : Type u_2
inst✝³ : NontriviallyNormedField 𝕜'
inst✝² : NormedAlgebra 𝕜 𝕜'
inst✝¹ : NormedSpace 𝕜' F
inst✝ : IsScalarTower 𝕜 𝕜' F
c : 𝕜 → 𝕜'
hc : DifferentiableWithinAt 𝕜 c s x
hf : DifferentiableWithinAt 𝕜 f s x
hxs : 𝓝[s \ {x}] x = ⊥
⊢ derivWithin (fun y => c y • f y) s x = c x • derivWithin f s x + derivWithin c s x • f x

Tactic:
simp [derivWithin_zero_of_isolated hxs]

Result:
no goals

Proof state:
𝕜 : Type u
inst✝⁶ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
f : 𝕜 → F
x : 𝕜
s : Set 𝕜
𝕜' : Type u_2
inst✝³ : NontriviallyNormedField 𝕜'
inst✝² : NormedAlgebra 𝕜 𝕜'
inst✝¹ : NormedSpace 𝕜' F
inst✝ : IsScalarTower 𝕜 𝕜' F
c : 𝕜 → 𝕜'
hc : DifferentiableWithinAt 𝕜 c s x
hf : DifferentiableWithinAt 𝕜 f s x
⊢ derivWithin (fun y => c y • f y) s x = c x • derivWithin f s x + derivWithin c s x • f x

Tactic:
rcases uniqueDiffWithinAt_or_nhdsWithin_eq_bot s x with hxs | hxs

Result:
case inl
𝕜 : Type u
inst✝⁶ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
f : 𝕜 → F
x : 𝕜
s : Set 𝕜
𝕜' : Type u_2
inst✝³ : NontriviallyNormedField 𝕜'
inst✝² : NormedAlgebra 𝕜 𝕜'
inst✝¹ : NormedSpace 𝕜' F
inst✝ : IsScalarTower 𝕜 𝕜' F
c : 𝕜 → 𝕜'
hc : DifferentiableWithinAt 𝕜 c s x
hf : DifferentiableWithinAt 𝕜 f s x
hxs : UniqueDiffWithinAt 𝕜 s x
⊢ derivWithin (fun y => c y • f y) s x = c x • derivWithin f s x + derivWithin c s x • f x

case inr
𝕜 : Type u
inst✝⁶ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
f : 𝕜 → F
x : 𝕜
s : Set 𝕜
𝕜' : Type u_2
inst✝³ : NontriviallyNormedField 𝕜'
inst✝² : NormedAlgebra 𝕜 𝕜'
inst✝¹ : NormedSpace 𝕜' F
inst✝ : IsScalarTower 𝕜 𝕜' F
c : 𝕜 → 𝕜'
hc : DifferentiableWithinAt 𝕜 c s x
hf : DifferentiableWithinAt 𝕜 f s x
hxs : 𝓝[s \ {x}] x = ⊥
⊢ derivWithin (fun y => c y • f y) s x = c x • derivWithin f s x + derivWithin c s x • f x

Proof state:
case inl
𝕜 : Type u
inst✝⁶ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
f : 𝕜 → F
x : 𝕜
s : Set 𝕜
𝕜' : Type u_2
inst✝³ : NontriviallyNormedField 𝕜'
inst✝² : NormedAlgebra 𝕜 𝕜'
inst✝¹ : NormedSpace 𝕜' F
inst✝ : IsScalarTower 𝕜 𝕜' F
c : 𝕜 → 𝕜'
hc : DifferentiableWithinAt 𝕜 c s x
hf : DifferentiableWithinAt 𝕜 f s x
hxs : UniqueDiffWithinAt 𝕜 s x
⊢ derivWithin (fun y => c y • f y) s x = c x • derivWithin f s x + derivWithin c s x • f x

Tactic:
exact (hc.hasDerivWithinAt.smul hf.hasDerivWithinAt).derivWithin hxs

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Fold.lean
theorem foldRev_zero {α : Type u} (f : (i : Nat) → i < 0 → α → α) (init : α) :
    foldRev 0 f init = init

Proof state:
α : Type u
f : (i : Nat) → i < 0 → α → α
init : α
⊢ foldRev 0 f init = init

Tactic:
simp [foldRev]

Result:
no goals
-- Mathlib/Geometry/Euclidean/Angle/Oriented/Basic.lean
theorem oangle_smul_left_of_pos (x y : V) {r : ℝ} (hr : 0 < r) :
    o.oangle (r • x) y = o.oangle x y

Proof state:
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
r : ℝ
hr : 0 < r
⊢ o.oangle (r • x) y = o.oangle x y

Tactic:
simp [oangle, Complex.arg_real_mul _ hr]

Result:
no goals
-- Mathlib/Algebra/Group/Pointwise/Set/Basic.lean
theorem inv_mem_inv : a⁻¹ ∈ s⁻¹ ↔ a ∈ s

Proof state:
α : Type u_2
inst✝ : InvolutiveInv α
s : Set α
a : α
⊢ a⁻¹ ∈ s⁻¹ ↔ a ∈ s

Tactic:
simp only [mem_inv, inv_inv]

Result:
no goals
-- Mathlib/Algebra/Order/CauSeq/Basic.lean
theorem inf_limZero {f g : CauSeq α abs} (hf : LimZero f) (hg : LimZero g) : LimZero (f ⊓ g)
  | ε, ε0 =>
    (exists_forall_ge_and (hf _ ε0) (hg _ ε0)).imp fun _ H j ij => by
      let ⟨H₁, H₂⟩ := H _ ij
      rw [abs_lt] at H₁ H₂ ⊢
      exact ⟨lt_inf_iff.mpr ⟨H₁.1, H₂.1⟩, inf_lt_iff.mpr (Or.inl H₁.2)⟩

Proof state:
α : Type u_1
inst✝ : LinearOrderedField α
f g : CauSeq α abs
hf : f.LimZero
hg : g.LimZero
ε : α
ε0 : ε > 0
x✝ : ℕ
H : ∀ j ≥ x✝, |↑f j| < ε ∧ |↑g j| < ε
j : ℕ
ij : j ≥ x✝
H₁ : |↑f j| < ε
H₂ : |↑g j| < ε
⊢ |↑(f ⊓ g) j| < ε

Tactic:
rw [abs_lt] at H₁ H₂ ⊢

Result:
α : Type u_1
inst✝ : LinearOrderedField α
f g : CauSeq α abs
hf : f.LimZero
hg : g.LimZero
ε : α
ε0 : ε > 0
x✝ : ℕ
H : ∀ j ≥ x✝, |↑f j| < ε ∧ |↑g j| < ε
j : ℕ
ij : j ≥ x✝
H₁ : -ε < ↑f j ∧ ↑f j < ε
H₂ : -ε < ↑g j ∧ ↑g j < ε
⊢ -ε < ↑(f ⊓ g) j ∧ ↑(f ⊓ g) j < ε

Proof state:
α : Type u_1
inst✝ : LinearOrderedField α
f g : CauSeq α abs
hf : f.LimZero
hg : g.LimZero
ε : α
ε0 : ε > 0
x✝ : ℕ
H : ∀ j ≥ x✝, |↑f j| < ε ∧ |↑g j| < ε
j : ℕ
ij : j ≥ x✝
⊢ |↑(f ⊓ g) j| < ε

Tactic:
let ⟨H₁, H₂⟩ := H _ ij

Result:
α : Type u_1
inst✝ : LinearOrderedField α
f g : CauSeq α abs
hf : f.LimZero
hg : g.LimZero
ε : α
ε0 : ε > 0
x✝ : ℕ
H : ∀ j ≥ x✝, |↑f j| < ε ∧ |↑g j| < ε
j : ℕ
ij : j ≥ x✝
H₁ : |↑f j| < ε
H₂ : |↑g j| < ε
⊢ |↑(f ⊓ g) j| < ε

Proof state:
α : Type u_1
inst✝ : LinearOrderedField α
f g : CauSeq α abs
hf : f.LimZero
hg : g.LimZero
ε : α
ε0 : ε > 0
x✝ : ℕ
H : ∀ j ≥ x✝, |↑f j| < ε ∧ |↑g j| < ε
j : ℕ
ij : j ≥ x✝
H₁ : -ε < ↑f j ∧ ↑f j < ε
H₂ : -ε < ↑g j ∧ ↑g j < ε
⊢ -ε < ↑(f ⊓ g) j ∧ ↑(f ⊓ g) j < ε

Tactic:
exact ⟨lt_inf_iff.mpr ⟨H₁.1, H₂.1⟩, inf_lt_iff.mpr (Or.inl H₁.2)⟩

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Attach.lean
theorem getLast_attachWith {P : α → Prop} {xs : List α}
    {H : ∀ (a : α), a ∈ xs → P a} (h : xs.attachWith P H ≠ []) :
    (xs.attachWith P H).getLast h = ⟨xs.getLast (by simpa using h), H _ (getLast_mem _)⟩

Proof state:
α : Type ?u.82289
P : α → Prop
xs : List α
H : ∀ (a : α), a ∈ xs → P a
h : xs.attachWith P H ≠ []
⊢ xs ≠ []

Tactic:
simpa using h

Result:
no goals

Proof state:
α : Type u_1
P : α → Prop
xs : List α
H : ∀ (a : α), a ∈ xs → P a
h : xs.attachWith P H ≠ []
⊢ (xs.attachWith P H).getLast h = ⟨xs.getLast ⋯, ⋯⟩

Tactic:
simp only [getLast_eq_head_reverse, reverse_attachWith, head_attachWith, head_map]

Result:
no goals
-- Mathlib/AlgebraicTopology/SimplicialObject/Split.lean
theorem congr_F {S₁ S₂ : Split C} {Φ₁ Φ₂ : S₁ ⟶ S₂} (h : Φ₁ = Φ₂) : Φ₁.f = Φ₂.f

Proof state:
C : Type u_1
inst✝ : Category.{u_2, u_1} C
S₁ S₂ : Split C
Φ₁ Φ₂ : S₁ ⟶ S₂
h : Φ₁ = Φ₂
⊢ Φ₁.f = Φ₂.f

Tactic:
rw [h]

Result:
no goals
-- Mathlib/Analysis/Normed/Algebra/Spectrum.lean
lemma lt_nnreal_iff [Algebra ℝ A] {a : A}
    (ha : SpectrumRestricts a ContinuousMap.realToNNReal) {r : ℝ≥0} :
    (∀ x ∈ spectrum ℝ≥0 a, x < r) ↔ ∀ x ∈ spectrum ℝ a, x < r

Proof state:
A : Type u_3
inst✝¹ : Ring A
inst✝ : Algebra ℝ A
a : A
ha : SpectrumRestricts a ⇑ContinuousMap.realToNNReal
r : ℝ≥0
⊢ (∀ x ∈ spectrum ℝ≥0 a, x < r) ↔ ∀ x ∈ spectrum ℝ a, x < ↑r

Tactic:
simp [← ha.algebraMap_image]

Result:
no goals
-- Mathlib/Data/Matrix/Block.lean
theorem blockDiagonal_smul {R : Type*} [Monoid R] [AddMonoid α] [DistribMulAction R α] (x : R)
    (M : o → Matrix m n α) : blockDiagonal (x • M) = x • blockDiagonal M

Proof state:
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
inst✝³ : DecidableEq o
R : Type u_14
inst✝² : Monoid R
inst✝¹ : AddMonoid α
inst✝ : DistribMulAction R α
x : R
M : o → Matrix m n α
⊢ blockDiagonal (x • M) = x • blockDiagonal M

Tactic:
ext

Result:
case a
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
inst✝³ : DecidableEq o
R : Type u_14
inst✝² : Monoid R
inst✝¹ : AddMonoid α
inst✝ : DistribMulAction R α
x : R
M : o → Matrix m n α
i✝ : m × o
j✝ : n × o
⊢ blockDiagonal (x • M) i✝ j✝ = (x • blockDiagonal M) i✝ j✝

Proof state:
case a
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
inst✝³ : DecidableEq o
R : Type u_14
inst✝² : Monoid R
inst✝¹ : AddMonoid α
inst✝ : DistribMulAction R α
x : R
M : o → Matrix m n α
i✝ : m × o
j✝ : n × o
⊢ (if i✝.2 = j✝.2 then x • M i✝.2 i✝.1 j✝.1 else 0) = x • if i✝.2 = j✝.2 then M i✝.2 i✝.1 j✝.1 else 0

Tactic:
split_ifs <;> simp

Result:
no goals

Proof state:
case a
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
inst✝³ : DecidableEq o
R : Type u_14
inst✝² : Monoid R
inst✝¹ : AddMonoid α
inst✝ : DistribMulAction R α
x : R
M : o → Matrix m n α
i✝ : m × o
j✝ : n × o
⊢ blockDiagonal (x • M) i✝ j✝ = (x • blockDiagonal M) i✝ j✝

Tactic:
simp only [blockDiagonal_apply, Pi.smul_apply, smul_apply]

Result:
case a
m : Type u_2
n : Type u_3
o : Type u_4
α : Type u_12
inst✝³ : DecidableEq o
R : Type u_14
inst✝² : Monoid R
inst✝¹ : AddMonoid α
inst✝ : DistribMulAction R α
x : R
M : o → Matrix m n α
i✝ : m × o
j✝ : n × o
⊢ (if i✝.2 = j✝.2 then x • M i✝.2 i✝.1 j✝.1 else 0) = x • if i✝.2 = j✝.2 then M i✝.2 i✝.1 j✝.1 else 0
-- Mathlib/Data/Finsupp/SMul.lean
theorem smul_single_one [Semiring R] (a : α) (b : R) : b • single a (1 : R) = single a b

Proof state:
α : Type u_1
R : Type u_6
inst✝ : Semiring R
a : α
b : R
⊢ b • single a 1 = single a b

Tactic:
rw [smul_single, smul_eq_mul, mul_one]

Result:
no goals
-- Mathlib/Order/Cofinal.lean
theorem IsCofinal.of_not_bddAbove {s : Set α} (h : ¬ BddAbove s) : IsCofinal s

Proof state:
α : Type u_1
inst✝ : LinearOrder α
s : Set α
h : ¬BddAbove s
⊢ IsCofinal s

Tactic:
contrapose! h

Result:
α : Type u_1
inst✝ : LinearOrder α
s : Set α
h : ¬IsCofinal s
⊢ BddAbove s

Proof state:
α : Type u_1
inst✝ : LinearOrder α
s : Set α
h : ¬IsCofinal s
⊢ BddAbove s

Tactic:
exact .of_not_isCofinal h

Result:
no goals