harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Topology/Algebra/InfiniteSum/Order.lean
theorem lt_hasProd [MulRightStrictMono α] (hf : HasProd f a) (i : ι)
    (hi : ∀ (j : ι), j ≠ i → 1 ≤ f j) (j : ι) (hij : j ≠ i) (hj : 1 < f j) :
    f i < a

Proof state:
ι : Type u_1
α : Type u_3
inst✝³ : OrderedCommMonoid α
inst✝² : TopologicalSpace α
inst✝¹ : OrderClosedTopology α
f : ι → α
a : α
inst✝ : MulRightStrictMono α
hf : HasProd f a
i : ι
hi : ∀ (j : ι), j ≠ i → 1 ≤ f j
j : ι
hij : j ≠ i
hj : 1 < f j
⊢ f j * f i = ∏ k ∈ {j, i}, f k

Tactic:
rw [Finset.prod_pair hij]

Result:
no goals

Proof state:
ι : Type u_1
α : Type u_3
inst✝³ : OrderedCommMonoid α
inst✝² : TopologicalSpace α
inst✝¹ : OrderClosedTopology α
f : ι → α
a : α
inst✝ : MulRightStrictMono α
hf : HasProd f a
i : ι
hi : ∀ (j : ι), j ≠ i → 1 ≤ f j
j : ι
hij : j ≠ i
hj : 1 < f j
⊢ f i < a

Tactic:
classical
calc
  f i < f j * f i := lt_mul_of_one_lt_left' (f i) hj
  _ = ∏ k ∈ {j, i}, f k := by rw [Finset.prod_pair hij]
  _ ≤ a := prod_le_hasProd _ (fun k hk ↦ hi k (hk ∘ mem_insert_of_mem ∘ mem_singleton.mpr)) hf

Result:
no goals

Proof state:
ι : Type u_1
α : Type u_3
inst✝³ : OrderedCommMonoid α
inst✝² : TopologicalSpace α
inst✝¹ : OrderClosedTopology α
f : ι → α
a : α
inst✝ : MulRightStrictMono α
hf : HasProd f a
i : ι
hi : ∀ (j : ι), j ≠ i → 1 ≤ f j
j : ι
hij : j ≠ i
hj : 1 < f j
⊢ f i < a

Tactic:
calc
  f i < f j * f i := lt_mul_of_one_lt_left' (f i) hj
  _ = ∏ k ∈ {j, i}, f k := by rw [Finset.prod_pair hij]
  _ ≤ a := prod_le_hasProd _ (fun k hk ↦ hi k (hk ∘ mem_insert_of_mem ∘ mem_singleton.mpr)) hf

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Sat/AIG/CachedGatesLemmas.lean
theorem denote_mkNotCached {aig : AIG α} {gate : Ref aig} :
    ⟦aig.mkNotCached gate, assign⟧
      =
    !⟦aig, ⟨gate.gate, gate.hgate⟩, assign⟧

Proof state:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
gate : aig.Ref
⊢ ⟦assign, aig.mkNotCached gate⟧ = !⟦assign, { aig := aig, ref := { gate := gate.gate, hgate := ⋯ } }⟧

Tactic:
rw [← not_as_aig]

Result:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
gate : aig.Ref
⊢ ⟦assign, aig.mkNotCached gate⟧ = (true && !⟦assign, { aig := aig, ref := { gate := gate.gate, hgate := ⋯ } }⟧)

Proof state:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
aig : AIG α
gate : aig.Ref
⊢ ⟦assign, aig.mkNotCached gate⟧ = (true && !⟦assign, { aig := aig, ref := { gate := gate.gate, hgate := ⋯ } }⟧)

Tactic:
simp [mkNotCached, LawfulOperator.denote_mem_prefix (f := mkConstCached) gate.hgate]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/MapIdx.lean
theorem mapFinIdx_eq_mkVector_iff {l : Vector α n} {f : (i : Nat) → α → (h : i < n) → β} {b : β} :
    l.mapFinIdx f = mkVector n b ↔ ∀ (i : Nat) (h : i < n), f i l[i] h = b

Proof state:
α : Type u_1
n : Nat
β : Type u_2
l : Vector α n
f : (i : Nat) → α → i < n → β
b : β
⊢ l.mapFinIdx f = mkVector n b ↔ ∀ (i : Nat) (h : i < n), f i l[i] h = b

Tactic:
rcases l with ⟨l, rfl⟩

Result:
case mk
α : Type u_1
β : Type u_2
b : β
l : Array α
f : (i : Nat) → α → i < l.size → β
⊢ { toArray := l, size_toArray := ⋯ }.mapFinIdx f = mkVector l.size b ↔
    ∀ (i : Nat) (h : i < l.size), f i { toArray := l, size_toArray := ⋯ }[i] h = b

Proof state:
case mk
α : Type u_1
β : Type u_2
b : β
l : Array α
f : (i : Nat) → α → i < l.size → β
⊢ { toArray := l, size_toArray := ⋯ }.mapFinIdx f = mkVector l.size b ↔
    ∀ (i : Nat) (h : i < l.size), f i { toArray := l, size_toArray := ⋯ }[i] h = b

Tactic:
simp [Array.mapFinIdx_eq_mkArray_iff]

Result:
no goals
-- Mathlib/CategoryTheory/Presentable/Basic.lean
lemma preservesColimitsOfShape_of_isCardinalAccessible_of_essentiallySmall
    [F.IsCardinalAccessible κ]
    (J : Type u₃) [Category.{v₃} J] [EssentiallySmall.{w} J] [IsCardinalFiltered J κ] :
    PreservesColimitsOfShape J F

Proof state:
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
F : C ⥤ D
κ : Cardinal.{w}
inst✝⁴ : Fact κ.IsRegular
inst✝³ : F.IsCardinalAccessible κ
J : Type u₃
inst✝² : Category.{v₃, u₃} J
inst✝¹ : EssentiallySmall.{w, v₃, u₃} J
inst✝ : IsCardinalFiltered J κ
this✝ : IsCardinalFiltered (SmallModel.{w, v₃, u₃} J) κ
this : PreservesColimitsOfShape (SmallModel.{w, v₃, u₃} J) F
⊢ PreservesColimitsOfShape J F

Tactic:
exact preservesColimitsOfShape_of_equiv (equivSmallModel.{w} J).symm F

Result:
no goals

Proof state:
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
F : C ⥤ D
κ : Cardinal.{w}
inst✝⁴ : Fact κ.IsRegular
inst✝³ : F.IsCardinalAccessible κ
J : Type u₃
inst✝² : Category.{v₃, u₃} J
inst✝¹ : EssentiallySmall.{w, v₃, u₃} J
inst✝ : IsCardinalFiltered J κ
⊢ PreservesColimitsOfShape J F

Tactic:
have := IsCardinalFiltered.of_equivalence κ (equivSmallModel.{w} J)

Result:
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
F : C ⥤ D
κ : Cardinal.{w}
inst✝⁴ : Fact κ.IsRegular
inst✝³ : F.IsCardinalAccessible κ
J : Type u₃
inst✝² : Category.{v₃, u₃} J
inst✝¹ : EssentiallySmall.{w, v₃, u₃} J
inst✝ : IsCardinalFiltered J κ
this : IsCardinalFiltered (SmallModel.{w, v₃, u₃} J) κ
⊢ PreservesColimitsOfShape J F

Proof state:
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
F : C ⥤ D
κ : Cardinal.{w}
inst✝⁴ : Fact κ.IsRegular
inst✝³ : F.IsCardinalAccessible κ
J : Type u₃
inst✝² : Category.{v₃, u₃} J
inst✝¹ : EssentiallySmall.{w, v₃, u₃} J
inst✝ : IsCardinalFiltered J κ
this : IsCardinalFiltered (SmallModel.{w, v₃, u₃} J) κ
⊢ PreservesColimitsOfShape J F

Tactic:
have := F.preservesColimitsOfShape_of_isCardinalAccessible κ (SmallModel.{w} J)

Result:
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁵ : Category.{v₂, u₂} D
F : C ⥤ D
κ : Cardinal.{w}
inst✝⁴ : Fact κ.IsRegular
inst✝³ : F.IsCardinalAccessible κ
J : Type u₃
inst✝² : Category.{v₃, u₃} J
inst✝¹ : EssentiallySmall.{w, v₃, u₃} J
inst✝ : IsCardinalFiltered J κ
this✝ : IsCardinalFiltered (SmallModel.{w, v₃, u₃} J) κ
this : PreservesColimitsOfShape (SmallModel.{w, v₃, u₃} J) F
⊢ PreservesColimitsOfShape J F
-- Mathlib/GroupTheory/Perm/Centralizer.lean
theorem ofPermHomFun_one (x : α) : (ofPermHomFun a 1) x = x

Proof state:
case inr.intro.intro.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
x : α
c : { x // x ∈ g.cycleFactorsFinset }
hc : x ∈ (↑c).support
m : ℤ
hm : (g ^ m) (a c) = x
⊢ a.ofPermHomFun 1 x = x

Tactic:
rw [ofPermHomFun_apply_of_cycleOf_mem a _ hc hm, OneMemClass.coe_one, coe_one, id_eq, hm]

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
x : α
⊢ a.ofPermHomFun 1 x = x

Tactic:
rcases mem_fixedPoints_or_exists_zpow_eq a x with (hx | ⟨c, hc, m, hm⟩)

Result:
case inl
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
x : α
hx : x ∈ Function.fixedPoints ⇑g
⊢ a.ofPermHomFun 1 x = x

case inr.intro.intro.intro
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
x : α
c : { x // x ∈ g.cycleFactorsFinset }
hc : x ∈ (↑c).support
m : ℤ
hm : (g ^ m) (a c) = x
⊢ a.ofPermHomFun 1 x = x

Proof state:
case inl
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g : Perm α
a : g.Basis
x : α
hx : x ∈ Function.fixedPoints ⇑g
⊢ a.ofPermHomFun 1 x = x

Tactic:
rw [ofPermHomFun_apply_of_mem_fixedPoints a _ hx]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem getMsbD_rotateRightAux_of_ge {x : BitVec w} {r : Nat} {i : Nat} (hi : i ≥ r) :
    (x.rotateRightAux r).getMsbD i = (decide (i < w) && x.getMsbD (i - r))

Proof state:
w : Nat
x : BitVec w
r i : Nat
hi : i ≥ r
⊢ ¬i < r

Tactic:
omega

Result:
no goals

Proof state:
w : Nat
x : BitVec w
r i : Nat
hi : i ≥ r
⊢ (x.rotateRightAux r).getMsbD i = (decide (i < w) && x.getMsbD (i - r))

Tactic:
simp [rotateRightAux, show ¬ i < r by omega, show i + (w - r) ≥ w by omega]

Result:
no goals

Proof state:
w : Nat
x : BitVec w
r i : Nat
hi : i ≥ r
⊢ i + (w - r) ≥ w

Tactic:
omega

Result:
no goals
-- Mathlib/Algebra/Polynomial/Basic.lean
theorem ofFinsupp_eq_zero {a} : (⟨a⟩ : R[X]) = 0 ↔ a = 0

Proof state:
R : Type u
inst✝ : Semiring R
a : R[ℕ]
⊢ { toFinsupp := a } = 0 ↔ a = 0

Tactic:
rw [← ofFinsupp_zero, ofFinsupp_inj]

Result:
no goals
-- Mathlib/Geometry/Manifold/IntegralCurve/Basic.lean
/-- If `γ` is an integral curve at each `t ∈ s`, it is an integral curve on `s`. -/
lemma IsIntegralCurveAt.isIntegralCurveOn (h : ∀ t ∈ s, IsIntegralCurveAt γ v t) :
    IsIntegralCurveOn γ v s

Proof state:
case intro.intro
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
H : Type u_2
inst✝² : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
γ : ℝ → M
v : (x : M) → TangentSpace I x
s✝ : Set ℝ
h✝ : ∀ t ∈ s✝, IsIntegralCurveAt γ v t
t : ℝ
ht : t ∈ s✝
s : Set ℝ
hs : s ∈ 𝓝 t
h : IsIntegralCurveOn γ v s
⊢ HasMFDerivAt 𝓘(ℝ, ℝ) I γ t (ContinuousLinearMap.smulRight 1 (v (γ t)))

Tactic:
exact h t (mem_of_mem_nhds hs)

Result:
no goals

Proof state:
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
H : Type u_2
inst✝² : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
γ : ℝ → M
v : (x : M) → TangentSpace I x
s : Set ℝ
h : ∀ t ∈ s, IsIntegralCurveAt γ v t
t : ℝ
ht : t ∈ s
⊢ HasMFDerivAt 𝓘(ℝ, ℝ) I γ t (ContinuousLinearMap.smulRight 1 (v (γ t)))

Tactic:
obtain ⟨s, hs, h⟩ := isIntegralCurveAt_iff.mp (h t ht)

Result:
case intro.intro
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
H : Type u_2
inst✝² : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
γ : ℝ → M
v : (x : M) → TangentSpace I x
s✝ : Set ℝ
h✝ : ∀ t ∈ s✝, IsIntegralCurveAt γ v t
t : ℝ
ht : t ∈ s✝
s : Set ℝ
hs : s ∈ 𝓝 t
h : IsIntegralCurveOn γ v s
⊢ HasMFDerivAt 𝓘(ℝ, ℝ) I γ t (ContinuousLinearMap.smulRight 1 (v (γ t)))

Proof state:
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
H : Type u_2
inst✝² : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
γ : ℝ → M
v : (x : M) → TangentSpace I x
s : Set ℝ
h : ∀ t ∈ s, IsIntegralCurveAt γ v t
⊢ IsIntegralCurveOn γ v s

Tactic:
intros t ht

Result:
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
H : Type u_2
inst✝² : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type u_3
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
γ : ℝ → M
v : (x : M) → TangentSpace I x
s : Set ℝ
h : ∀ t ∈ s, IsIntegralCurveAt γ v t
t : ℝ
ht : t ∈ s
⊢ HasMFDerivAt 𝓘(ℝ, ℝ) I γ t (ContinuousLinearMap.smulRight 1 (v (γ t)))
-- Mathlib/LinearAlgebra/Finsupp/LinearCombination.lean
theorem linearCombination_equivMapDomain (f : α ≃ α') (l : α →₀ R) :
    (linearCombination R v') (equivMapDomain f l) = (linearCombination R (v' ∘ f)) l

Proof state:
α : Type u_1
R : Type u_5
inst✝² : Semiring R
α' : Type u_7
M' : Type u_8
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
v' : α' → M'
f : α ≃ α'
l : α →₀ R
⊢ (linearCombination R v') (equivMapDomain f l) = (linearCombination R (v' ∘ ⇑f)) l

Tactic:
rw [equivMapDomain_eq_mapDomain, linearCombination_mapDomain]

Result:
no goals
-- Mathlib/RingTheory/Valuation/Quotient.lean
theorem self_le_supp_comap (J : Ideal R) (v : Valuation (R ⧸ J) Γ₀) :
    J ≤ (v.comap (Ideal.Quotient.mk J)).supp

Proof state:
R : Type u_1
Γ₀ : Type u_2
inst✝¹ : CommRing R
inst✝ : LinearOrderedCommMonoidWithZero Γ₀
J : Ideal R
v : Valuation (R ⧸ J) Γ₀
⊢ Ideal.map (Ideal.Quotient.mk J) J ≤ v.supp

Tactic:
simp

Result:
no goals

Proof state:
R : Type u_1
Γ₀ : Type u_2
inst✝¹ : CommRing R
inst✝ : LinearOrderedCommMonoidWithZero Γ₀
J : Ideal R
v : Valuation (R ⧸ J) Γ₀
⊢ J ≤ (comap (Ideal.Quotient.mk J) v).supp

Tactic:
rw [comap_supp, ← Ideal.map_le_iff_le_comap]

Result:
R : Type u_1
Γ₀ : Type u_2
inst✝¹ : CommRing R
inst✝ : LinearOrderedCommMonoidWithZero Γ₀
J : Ideal R
v : Valuation (R ⧸ J) Γ₀
⊢ Ideal.map (Ideal.Quotient.mk J) J ≤ v.supp
-- Mathlib/Data/Set/Image.lean
theorem range_comp (g : α → β) (f : ι → α) : range (g ∘ f) = g '' range f

Proof state:
α : Type u_1
β : Type u_2
ι : Sort u_4
g : α → β
f : ι → α
⊢ range (g ∘ f) = g '' range f

Tactic:
aesop

Result:
no goals
-- Mathlib/MeasureTheory/Function/LpSpace/Basic.lean
theorem const_smul_mem_Lp (c : 𝕜) (f : Lp E p μ) : c • (f : α →ₘ[μ] E) ∈ Lp E p μ

Proof state:
α : Type u_1
𝕜 : Type u_2
E : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedRing 𝕜
inst✝¹ : Module 𝕜 E
inst✝ : BoundedSMul 𝕜 E
c : 𝕜
f : ↥(Lp E p μ)
⊢ c • ↑f ∈ Lp E p μ

Tactic:
rw [mem_Lp_iff_eLpNorm_lt_top, eLpNorm_congr_ae (AEEqFun.coeFn_smul _ _)]

Result:
α : Type u_1
𝕜 : Type u_2
E : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedRing 𝕜
inst✝¹ : Module 𝕜 E
inst✝ : BoundedSMul 𝕜 E
c : 𝕜
f : ↥(Lp E p μ)
⊢ eLpNorm (c • ↑↑f) p μ < ⊤

Proof state:
α : Type u_1
𝕜 : Type u_2
E : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝³ : NormedAddCommGroup E
inst✝² : NormedRing 𝕜
inst✝¹ : Module 𝕜 E
inst✝ : BoundedSMul 𝕜 E
c : 𝕜
f : ↥(Lp E p μ)
⊢ eLpNorm (c • ↑↑f) p μ < ⊤

Tactic:
exact eLpNorm_const_smul_le.trans_lt <| ENNReal.mul_lt_top ENNReal.coe_lt_top f.prop

Result:
no goals
-- Mathlib/LinearAlgebra/AffineSpace/Basis.lean
theorem coord_apply_combination_of_not_mem (hi : i ∉ s) {w : ι → k} (hw : s.sum w = 1) :
    b.coord i (s.affineCombination k b w) = 0

Proof state:
ι : Type u_1
k : Type u_5
V : Type u_6
P : Type u_7
inst✝³ : AddCommGroup V
inst✝² : AffineSpace V P
inst✝¹ : Ring k
inst✝ : Module k V
b : AffineBasis ι k P
s : Finset ι
i : ι
hi : i ∉ s
w : ι → k
hw : s.sum w = 1
⊢ (b.coord i) ((Finset.affineCombination k s ⇑b) w) = 0

Tactic:
classical simp only [coord_apply, hi, Finset.affineCombination_eq_linear_combination, if_false,
    mul_boole, hw, Function.comp_apply, smul_eq_mul, s.sum_ite_eq,
    s.map_affineCombination b w hw]

Result:
no goals

Proof state:
ι : Type u_1
k : Type u_5
V : Type u_6
P : Type u_7
inst✝³ : AddCommGroup V
inst✝² : AffineSpace V P
inst✝¹ : Ring k
inst✝ : Module k V
b : AffineBasis ι k P
s : Finset ι
i : ι
hi : i ∉ s
w : ι → k
hw : s.sum w = 1
⊢ (b.coord i) ((Finset.affineCombination k s ⇑b) w) = 0

Tactic:
simp only [coord_apply, hi, Finset.affineCombination_eq_linear_combination, if_false,
mul_boole, hw, Function.comp_apply, smul_eq_mul, s.sum_ite_eq,
s.map_affineCombination b w hw]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/Deriv.lean
theorem hasStrictDerivAt_rpow_const_of_ne {x : ℝ} (hx : x ≠ 0) (p : ℝ) :
    HasStrictDerivAt (fun x => x ^ p) (p * x ^ (p - 1)) x

Proof state:
case h.e'_9
x : ℝ
hx✝ : x ≠ 0
p : ℝ
hx : x < 0
this :
  HasStrictDerivAt ((fun x => x.1 ^ x.2) ∘ fun x => (id x, p))
    ((((x, p).2 * (x, p).1 ^ ((x, p).2 - 1)) • ContinuousLinearMap.fst ℝ ℝ ℝ +
        ((x, p).1 ^ (x, p).2 * log (x, p).1 - rexp (log (x, p).1 * (x, p).2) * sin ((x, p).2 * π) * π) •
          ContinuousLinearMap.snd ℝ ℝ ℝ)
      (1, 0))
    x
⊢ p * x ^ (p - 1) =
    (((x, p).2 * (x, p).1 ^ ((x, p).2 - 1)) • ContinuousLinearMap.fst ℝ ℝ ℝ +
        ((x, p).1 ^ (x, p).2 * log (x, p).1 - rexp (log (x, p).1 * (x, p).2) * sin ((x, p).2 * π) * π) •
          ContinuousLinearMap.snd ℝ ℝ ℝ)
      (1, 0)

Tactic:
simp

Result:
no goals

Proof state:
case inl
x : ℝ
hx✝ : x ≠ 0
p : ℝ
hx : x < 0
⊢ HasStrictDerivAt (fun x => x ^ p) (p * x ^ (p - 1)) x

Tactic:
have := (hasStrictFDerivAt_rpow_of_neg (x, p) hx).comp_hasStrictDerivAt x
  ((hasStrictDerivAt_id x).prod (hasStrictDerivAt_const x p))

Result:
case inl
x : ℝ
hx✝ : x ≠ 0
p : ℝ
hx : x < 0
this :
  HasStrictDerivAt ((fun x => x.1 ^ x.2) ∘ fun x => (id x, p))
    ((((x, p).2 * (x, p).1 ^ ((x, p).2 - 1)) • ContinuousLinearMap.fst ℝ ℝ ℝ +
        ((x, p).1 ^ (x, p).2 * log (x, p).1 - rexp (log (x, p).1 * (x, p).2) * sin ((x, p).2 * π) * π) •
          ContinuousLinearMap.snd ℝ ℝ ℝ)
      (1, 0))
    x
⊢ HasStrictDerivAt (fun x => x ^ p) (p * x ^ (p - 1)) x

Proof state:
case inl
x : ℝ
hx✝ : x ≠ 0
p : ℝ
hx : x < 0
this :
  HasStrictDerivAt ((fun x => x.1 ^ x.2) ∘ fun x => (id x, p))
    ((((x, p).2 * (x, p).1 ^ ((x, p).2 - 1)) • ContinuousLinearMap.fst ℝ ℝ ℝ +
        ((x, p).1 ^ (x, p).2 * log (x, p).1 - rexp (log (x, p).1 * (x, p).2) * sin ((x, p).2 * π) * π) •
          ContinuousLinearMap.snd ℝ ℝ ℝ)
      (1, 0))
    x
⊢ HasStrictDerivAt (fun x => x ^ p) (p * x ^ (p - 1)) x

Tactic:
convert this using 1

Result:
case h.e'_9
x : ℝ
hx✝ : x ≠ 0
p : ℝ
hx : x < 0
this :
  HasStrictDerivAt ((fun x => x.1 ^ x.2) ∘ fun x => (id x, p))
    ((((x, p).2 * (x, p).1 ^ ((x, p).2 - 1)) • ContinuousLinearMap.fst ℝ ℝ ℝ +
        ((x, p).1 ^ (x, p).2 * log (x, p).1 - rexp (log (x, p).1 * (x, p).2) * sin ((x, p).2 * π) * π) •
          ContinuousLinearMap.snd ℝ ℝ ℝ)
      (1, 0))
    x
⊢ p * x ^ (p - 1) =
    (((x, p).2 * (x, p).1 ^ ((x, p).2 - 1)) • ContinuousLinearMap.fst ℝ ℝ ℝ +
        ((x, p).1 ^ (x, p).2 * log (x, p).1 - rexp (log (x, p).1 * (x, p).2) * sin ((x, p).2 * π) * π) •
          ContinuousLinearMap.snd ℝ ℝ ℝ)
      (1, 0)

Proof state:
x : ℝ
hx : x ≠ 0
p : ℝ
⊢ HasStrictDerivAt (fun x => x ^ p) (p * x ^ (p - 1)) x

Tactic:
rcases hx.lt_or_lt with hx | hx

Result:
case inl
x : ℝ
hx✝ : x ≠ 0
p : ℝ
hx : x < 0
⊢ HasStrictDerivAt (fun x => x ^ p) (p * x ^ (p - 1)) x

case inr
x : ℝ
hx✝ : x ≠ 0
p : ℝ
hx : 0 < x
⊢ HasStrictDerivAt (fun x => x ^ p) (p * x ^ (p - 1)) x

Proof state:
case inr
x : ℝ
hx✝ : x ≠ 0
p : ℝ
hx : 0 < x
⊢ HasStrictDerivAt (fun x => x ^ p) (p * x ^ (p - 1)) x

Tactic:
simpa using (hasStrictDerivAt_id x).rpow (hasStrictDerivAt_const x p) hx

Result:
no goals
-- Mathlib/Algebra/NoZeroSMulDivisors/Basic.lean
theorem Nat.noZeroSMulDivisors
    (R) (M) [Semiring R] [CharZero R] [AddCommMonoid M] [Module R M] [NoZeroSMulDivisors R M] :
    NoZeroSMulDivisors ℕ M where
  eq_zero_or_eq_zero_of_smul_eq_zero {c x}

Proof state:
R : Type u_3
M : Type u_4
inst✝⁴ : Semiring R
inst✝³ : CharZero R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
c : ℕ
x : M
⊢ c • x = 0 → c = 0 ∨ x = 0

Tactic:
rw [← Nat.cast_smul_eq_nsmul R, smul_eq_zero]

Result:
R : Type u_3
M : Type u_4
inst✝⁴ : Semiring R
inst✝³ : CharZero R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
c : ℕ
x : M
⊢ ↑c = 0 ∨ x = 0 → c = 0 ∨ x = 0

Proof state:
R : Type u_3
M : Type u_4
inst✝⁴ : Semiring R
inst✝³ : CharZero R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : NoZeroSMulDivisors R M
c : ℕ
x : M
⊢ ↑c = 0 ∨ x = 0 → c = 0 ∨ x = 0

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/PiL2.lean
theorem DirectSum.IsInternal.subordinateOrthonormalBasis_subordinate (a : Fin n)
    (hV' : OrthogonalFamily 𝕜 (fun i => V i) fun i => (V i).subtypeₗᵢ) :
    hV.subordinateOrthonormalBasis hn hV' a ∈ V (hV.subordinateOrthonormalBasisIndex hn a hV')

Proof state:
ι : Type u_1
𝕜 : Type u_3
inst✝⁵ : RCLike 𝕜
E : Type u_4
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : Fintype ι
inst✝¹ : FiniteDimensional 𝕜 E
n : ℕ
hn : finrank 𝕜 E = n
inst✝ : DecidableEq ι
V : ι → Submodule 𝕜 E
hV : IsInternal V
a : Fin n
hV' : OrthogonalFamily 𝕜 (fun i => ↥(V i)) fun i => (V i).subtypeₗᵢ
⊢ (subordinateOrthonormalBasis hn hV hV') a ∈ V (subordinateOrthonormalBasisIndex hn hV a hV')

Tactic:
simpa only [DirectSum.IsInternal.subordinateOrthonormalBasis, OrthonormalBasis.coe_reindex,
  DirectSum.IsInternal.subordinateOrthonormalBasisIndex] using
  hV.collectedOrthonormalBasis_mem hV' (fun i => stdOrthonormalBasis 𝕜 (V i))
    ((hV.sigmaOrthonormalBasisIndexEquiv hn hV').symm a)

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Principal.lean
theorem principal_mul_omega0 : Principal (· * ·) ω := fun a b ha hb =>
  match a, b, lt_omega0.1 ha, lt_omega0.1 hb with
  | _, _, ⟨m, rfl⟩, ⟨n, rfl⟩ => by
    dsimp only; rw [← natCast_mul]
    apply nat_lt_omega0

Proof state:
a b : Ordinal.{u_1}
m n : ℕ
ha : ↑m < ω
hb : ↑n < ω
⊢ ↑(m * n) < ω

Tactic:
apply nat_lt_omega0

Result:
no goals

Proof state:
a b : Ordinal.{u_1}
m n : ℕ
ha : ↑m < ω
hb : ↑n < ω
⊢ (fun x1 x2 => x1 * x2) ↑m ↑n < ω

Tactic:
dsimp only

Result:
a b : Ordinal.{u_1}
m n : ℕ
ha : ↑m < ω
hb : ↑n < ω
⊢ ↑m * ↑n < ω

Proof state:
a b : Ordinal.{u_1}
m n : ℕ
ha : ↑m < ω
hb : ↑n < ω
⊢ ↑m * ↑n < ω

Tactic:
rw [← natCast_mul]

Result:
a b : Ordinal.{u_1}
m n : ℕ
ha : ↑m < ω
hb : ↑n < ω
⊢ ↑(m * n) < ω
-- Mathlib/LinearAlgebra/Dimension/LinearMap.lean
theorem lift_rank_comp_le_right (g : V →ₗ[K] V') (f : V' →ₗ[K] V'') :
    Cardinal.lift.{v'} (rank (f.comp g)) ≤ Cardinal.lift.{v''} (rank g)

Proof state:
K : Type u
V : Type v
V' : Type v'
V'' : Type v''
inst✝⁶ : Ring K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
inst✝³ : AddCommGroup V'
inst✝² : Module K V'
inst✝¹ : AddCommGroup V''
inst✝ : Module K V''
g : V →ₗ[K] V'
f : V' →ₗ[K] V''
⊢ lift.{v', v''} (Module.rank K ↥(Submodule.map f (range g))) ≤ lift.{v'', v'} (Module.rank K ↥(range g))

Tactic:
exact lift_rank_map_le _ _

Result:
no goals

Proof state:
K : Type u
V : Type v
V' : Type v'
V'' : Type v''
inst✝⁶ : Ring K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
inst✝³ : AddCommGroup V'
inst✝² : Module K V'
inst✝¹ : AddCommGroup V''
inst✝ : Module K V''
g : V →ₗ[K] V'
f : V' →ₗ[K] V''
⊢ lift.{v', v''} (f ∘ₗ g).rank ≤ lift.{v'', v'} g.rank

Tactic:
rw [rank, rank, LinearMap.range_comp]

Result:
K : Type u
V : Type v
V' : Type v'
V'' : Type v''
inst✝⁶ : Ring K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
inst✝³ : AddCommGroup V'
inst✝² : Module K V'
inst✝¹ : AddCommGroup V''
inst✝ : Module K V''
g : V →ₗ[K] V'
f : V' →ₗ[K] V''
⊢ lift.{v', v''} (Module.rank K ↥(Submodule.map f (range g))) ≤ lift.{v'', v'} (Module.rank K ↥(range g))
-- Mathlib/SetTheory/ZFC/Basic.lean
theorem toSet_sInter {x : ZFSet.{u}} (h : x.Nonempty) : (⋂₀ x).toSet = ⋂₀ (toSet '' x.toSet)

Proof state:
x : ZFSet.{u}
h : x.Nonempty
⊢ (⋂₀ x).toSet = ⋂₀ (toSet '' x.toSet)

Tactic:
ext

Result:
case h
x : ZFSet.{u}
h : x.Nonempty
x✝ : ZFSet.{u}
⊢ x✝ ∈ (⋂₀ x).toSet ↔ x✝ ∈ ⋂₀ (toSet '' x.toSet)

Proof state:
case h
x : ZFSet.{u}
h : x.Nonempty
x✝ : ZFSet.{u}
⊢ x✝ ∈ (⋂₀ x).toSet ↔ x✝ ∈ ⋂₀ (toSet '' x.toSet)

Tactic:
simp [mem_sInter h]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/WithDensity.lean
theorem withDensity_indicator {s : Set α} (hs : MeasurableSet s) (f : α → ℝ≥0∞) :
    μ.withDensity (s.indicator f) = (μ.restrict s).withDensity f

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
f : α → ℝ≥0∞
⊢ μ.withDensity (s.indicator f) = (μ.restrict s).withDensity f

Tactic:
ext1 t ht

Result:
case h
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
f : α → ℝ≥0∞
t : Set α
ht : MeasurableSet t
⊢ (μ.withDensity (s.indicator f)) t = ((μ.restrict s).withDensity f) t

Proof state:
case h
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
f : α → ℝ≥0∞
t : Set α
ht : MeasurableSet t
⊢ (μ.withDensity (s.indicator f)) t = ((μ.restrict s).withDensity f) t

Tactic:
rw [withDensity_apply _ ht, lintegral_indicator hs, restrict_comm hs, ←
  withDensity_apply _ ht]

Result:
no goals
-- Mathlib/Analysis/Calculus/Deriv/Slope.lean
theorem isSeparable_range_deriv [SeparableSpace 𝕜] (f : 𝕜 → F) :
    IsSeparable (range (deriv f))

Proof state:
𝕜 : Type u
inst✝³ : NontriviallyNormedField 𝕜
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : SeparableSpace 𝕜
f : 𝕜 → F
⊢ IsSeparable (range (derivWithin f univ))

Tactic:
exact isSeparable_range_derivWithin _ _

Result:
no goals

Proof state:
𝕜 : Type u
inst✝³ : NontriviallyNormedField 𝕜
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : SeparableSpace 𝕜
f : 𝕜 → F
⊢ IsSeparable (range (deriv f))

Tactic:
rw [← derivWithin_univ]

Result:
𝕜 : Type u
inst✝³ : NontriviallyNormedField 𝕜
F : Type v
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : SeparableSpace 𝕜
f : 𝕜 → F
⊢ IsSeparable (range (derivWithin f univ))