harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/MeasureTheory/VectorMeasure/Basic.lean
theorem neg_le_neg {i : Set α} (hi : MeasurableSet i) (h : v ≤[i] w) : -w ≤[i] -v

Proof state:
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : OrderedAddCommGroup M
inst✝ : IsTopologicalAddGroup M
v w : VectorMeasure α M
i : Set α
hi : MeasurableSet i
h : v ≤[i] w
⊢ -w ≤[i] -v

Tactic:
intro j hj₁

Result:
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : OrderedAddCommGroup M
inst✝ : IsTopologicalAddGroup M
v w : VectorMeasure α M
i : Set α
hi : MeasurableSet i
h : v ≤[i] w
j : Set α
hj₁ : MeasurableSet j
⊢ ↑((-w).restrict i) j ≤ ↑((-v).restrict i) j

Proof state:
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : OrderedAddCommGroup M
inst✝ : IsTopologicalAddGroup M
v w : VectorMeasure α M
i : Set α
hi : MeasurableSet i
h : v ≤[i] w
j : Set α
hj₁ : MeasurableSet j
⊢ ↑v (j ∩ i) ≤ ↑w (j ∩ i)

Tactic:
rw [← restrict_apply _ hi hj₁, ← restrict_apply _ hi hj₁]

Result:
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : OrderedAddCommGroup M
inst✝ : IsTopologicalAddGroup M
v w : VectorMeasure α M
i : Set α
hi : MeasurableSet i
h : v ≤[i] w
j : Set α
hj₁ : MeasurableSet j
⊢ ↑(v.restrict i) j ≤ ↑(w.restrict i) j

Proof state:
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : OrderedAddCommGroup M
inst✝ : IsTopologicalAddGroup M
v w : VectorMeasure α M
i : Set α
hi : MeasurableSet i
h : v ≤[i] w
j : Set α
hj₁ : MeasurableSet j
⊢ -↑w (j ∩ i) ≤ -↑v (j ∩ i)

Tactic:
refine neg_le_neg ?_

Result:
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : OrderedAddCommGroup M
inst✝ : IsTopologicalAddGroup M
v w : VectorMeasure α M
i : Set α
hi : MeasurableSet i
h : v ≤[i] w
j : Set α
hj₁ : MeasurableSet j
⊢ ↑v (j ∩ i) ≤ ↑w (j ∩ i)

Proof state:
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : OrderedAddCommGroup M
inst✝ : IsTopologicalAddGroup M
v w : VectorMeasure α M
i : Set α
hi : MeasurableSet i
h : v ≤[i] w
j : Set α
hj₁ : MeasurableSet j
⊢ ↑(v.restrict i) j ≤ ↑(w.restrict i) j

Tactic:
exact h j hj₁

Result:
no goals

Proof state:
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : OrderedAddCommGroup M
inst✝ : IsTopologicalAddGroup M
v w : VectorMeasure α M
i : Set α
hi : MeasurableSet i
h : v ≤[i] w
j : Set α
hj₁ : MeasurableSet j
⊢ ↑((-w).restrict i) j ≤ ↑((-v).restrict i) j

Tactic:
rw [restrict_apply _ hi hj₁, restrict_apply _ hi hj₁, neg_apply, neg_apply]

Result:
α : Type u_1
m : MeasurableSpace α
M : Type u_3
inst✝² : TopologicalSpace M
inst✝¹ : OrderedAddCommGroup M
inst✝ : IsTopologicalAddGroup M
v w : VectorMeasure α M
i : Set α
hi : MeasurableSet i
h : v ≤[i] w
j : Set α
hj₁ : MeasurableSet j
⊢ -↑w (j ∩ i) ≤ -↑v (j ∩ i)
-- Mathlib/GroupTheory/Congruence/Hom.lean
theorem lift_comp_mk' (H : c ≤ ker f) : (c.lift f H).comp c.mk' = f

Proof state:
M : Type u_1
P : Type u_3
inst✝¹ : MulOneClass M
inst✝ : MulOneClass P
c : Con M
f : M →* P
H : c ≤ ker f
⊢ (c.lift f H).comp c.mk' = f

Tactic:
ext

Result:
case h
M : Type u_1
P : Type u_3
inst✝¹ : MulOneClass M
inst✝ : MulOneClass P
c : Con M
f : M →* P
H : c ≤ ker f
x✝ : M
⊢ ((c.lift f H).comp c.mk') x✝ = f x✝

Proof state:
case h
M : Type u_1
P : Type u_3
inst✝¹ : MulOneClass M
inst✝ : MulOneClass P
c : Con M
f : M →* P
H : c ≤ ker f
x✝ : M
⊢ ((c.lift f H).comp c.mk') x✝ = f x✝

Tactic:
rfl

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Preserves/Shapes/Kernels.lean
@[reassoc (attr := simp)]
lemma map_condition : G.map f ≫ G.map c.π = 0

Proof state:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
inst✝³ : HasZeroMorphisms C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
inst✝¹ : HasZeroMorphisms D
X Y : C
f : X ⟶ Y
c : CokernelCofork f
G : C ⥤ D
inst✝ : G.PreservesZeroMorphisms
⊢ G.map f ≫ G.map (Cofork.π c) = 0

Tactic:
rw [← G.map_comp, c.condition, G.map_zero]

Result:
no goals
-- Mathlib/LinearAlgebra/Dual.lean
theorem linearCombination_dualBasis (f : ι →₀ R) (i : ι) :
    Finsupp.linearCombination R b.dualBasis f (b i) = f i

Proof state:
case intro
R : Type uR
M : Type uM
ι : Type uι
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : DecidableEq ι
b : Basis ι R M
inst✝ : Finite ι
f : ι →₀ R
i : ι
val✝ : Fintype ι
⊢ ∑ d : ι, (f d • b.dualBasis d) (b i) = f i

Tactic:
simp_rw [LinearMap.smul_apply, smul_eq_mul, dualBasis_apply_self, mul_boole,
Finset.sum_ite_eq, if_pos (Finset.mem_univ i)]

Result:
no goals

Proof state:
case intro.h
R : Type uR
M : Type uM
ι : Type uι
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : DecidableEq ι
b : Basis ι R M
inst✝ : Finite ι
f : ι →₀ R
i : ι
val✝ : Fintype ι
i✝ : ι
⊢ 0 • b.dualBasis i✝ = 0

Tactic:
rw [zero_smul]

Result:
no goals

Proof state:
case intro.h
R : Type uR
M : Type uM
ι : Type uι
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : DecidableEq ι
b : Basis ι R M
inst✝ : Finite ι
f : ι →₀ R
i : ι
val✝ : Fintype ι
⊢ ∀ (i : ι), 0 • b.dualBasis i = 0

Tactic:
intro

Result:
case intro.h
R : Type uR
M : Type uM
ι : Type uι
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : DecidableEq ι
b : Basis ι R M
inst✝ : Finite ι
f : ι →₀ R
i : ι
val✝ : Fintype ι
i✝ : ι
⊢ 0 • b.dualBasis i✝ = 0

Proof state:
case intro
R : Type uR
M : Type uM
ι : Type uι
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : DecidableEq ι
b : Basis ι R M
inst✝ : Finite ι
f : ι →₀ R
i : ι
val✝ : Fintype ι
⊢ ((Finsupp.linearCombination R ⇑b.dualBasis) f) (b i) = f i

Tactic:
rw [Finsupp.linearCombination_apply, Finsupp.sum_fintype, LinearMap.sum_apply]

Result:
case intro
R : Type uR
M : Type uM
ι : Type uι
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : DecidableEq ι
b : Basis ι R M
inst✝ : Finite ι
f : ι →₀ R
i : ι
val✝ : Fintype ι
⊢ ∑ d : ι, (f d • b.dualBasis d) (b i) = f i

case intro.h
R : Type uR
M : Type uM
ι : Type uι
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : DecidableEq ι
b : Basis ι R M
inst✝ : Finite ι
f : ι →₀ R
i : ι
val✝ : Fintype ι
⊢ ∀ (i : ι), 0 • b.dualBasis i = 0

Proof state:
R : Type uR
M : Type uM
ι : Type uι
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : DecidableEq ι
b : Basis ι R M
inst✝ : Finite ι
f : ι →₀ R
i : ι
⊢ ((Finsupp.linearCombination R ⇑b.dualBasis) f) (b i) = f i

Tactic:
cases nonempty_fintype ι

Result:
case intro
R : Type uR
M : Type uM
ι : Type uι
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
inst✝¹ : DecidableEq ι
b : Basis ι R M
inst✝ : Finite ι
f : ι →₀ R
i : ι
val✝ : Fintype ι
⊢ ((Finsupp.linearCombination R ⇑b.dualBasis) f) (b i) = f i
-- Mathlib/Data/List/DropRight.lean
theorem rtake_nil : rtake ([] : List α) n = []

Proof state:
α : Type u_1
n : ℕ
⊢ [].rtake n = []

Tactic:
simp [rtake]

Result:
no goals
-- Mathlib/GroupTheory/GroupAction/Primitive.lean
theorem isCoatom_stabilizer_iff_preprimitive [IsPretransitive G X] [Nontrivial X] (a : X) :
    IsCoatom (stabilizer G a) ↔ IsPreprimitive G X

Proof state:
G : Type u_3
inst✝³ : Group G
X : Type u_4
inst✝² : MulAction G X
inst✝¹ : IsPretransitive G X
inst✝ : Nontrivial X
a : X
⊢ IsCoatom ⊥ ↔ IsCoatom ⊥

Tactic:
rw [← OrderIso.isCoatom_iff (block_stabilizerOrderIso G a), OrderIso.map_bot]

Result:
no goals

Proof state:
G : Type u_3
inst✝³ : Group G
X : Type u_4
inst✝² : MulAction G X
inst✝¹ : IsPretransitive G X
inst✝ : Nontrivial X
a : X
⊢ IsCoatom (stabilizer G a) ↔ IsPreprimitive G X

Tactic:
rw [← isSimpleOrder_blockMem_iff_isPreprimitive G a, ← Set.isSimpleOrder_Ici_iff_isCoatom]

Result:
G : Type u_3
inst✝³ : Group G
X : Type u_4
inst✝² : MulAction G X
inst✝¹ : IsPretransitive G X
inst✝ : Nontrivial X
a : X
⊢ IsSimpleOrder ↑(Set.Ici (stabilizer G a)) ↔ IsSimpleOrder (BlockMem G a)

Proof state:
G : Type u_3
inst✝³ : Group G
X : Type u_4
inst✝² : MulAction G X
inst✝¹ : IsPretransitive G X
inst✝ : Nontrivial X
a : X
⊢ IsSimpleOrder ↑(Set.Ici (stabilizer G a)) ↔ IsSimpleOrder (BlockMem G a)

Tactic:
simp only [isSimpleOrder_iff_isCoatom_bot]

Result:
G : Type u_3
inst✝³ : Group G
X : Type u_4
inst✝² : MulAction G X
inst✝¹ : IsPretransitive G X
inst✝ : Nontrivial X
a : X
⊢ IsCoatom ⊥ ↔ IsCoatom ⊥
-- Mathlib/.lake/packages/batteries/Batteries/Data/HashMap/WF.lean
theorem expand_WF [BEq α] [Hashable α] {buckets : Buckets α β} (H : buckets.WF) :
    (expand sz buckets).buckets.WF :=
  go _ H.1 H.2 ⟨.mk' _, fun _ _ _ _ => by simp_all [Buckets.mk, List.mem_replicate]⟩
where
  go (i) {source : Array (AssocList α β)}
      (hs₁ : ∀ [LawfulHashable α] [PartialEquivBEq α], ∀ bucket ∈ source.toList,
        bucket.toList.Pairwise fun a b => ¬(a.1 == b.1))
      (hs₂ : ∀ (j : Nat) (h : j < source.size),
        source[j].All fun k _ => ((hash k).toUSize % USize.ofNat source.size).toNat = j)
      {target : Buckets α β} (ht : target.WF ∧ ∀ bucket ∈ target.1.toList,
        bucket.All fun k _ => ((hash k).toUSize % USize.ofNat source.size).toNat < i) :
      (expand.go i source target).WF

Proof state:
case refine_3.refine_1
α : Type u_1
β : Type u_2
sz : Nat
inst✝¹ : BEq α
inst✝ : Hashable α
buckets : Buckets α β
H✝ : buckets.WF
i : Nat
source : Array (AssocList α β)
hs₁ :
  ∀ [inst : LawfulHashable α] [inst : PartialEquivBEq α] (bucket : AssocList α β),
    bucket ∈ source.toList → List.Pairwise (fun a b => ¬(a.fst == b.fst) = true) bucket.toList
hs₂ :
  ∀ (j : Nat) (h : j < source.size),
    AssocList.All (fun k x => ((hash k).toUSize % USize.ofNat source.size).toNat = j) source[j]
target : Buckets α β
ht :
  target.WF ∧
    ∀ (bucket : AssocList α β),
      bucket ∈ target.val.toList →
        AssocList.All (fun k x => ((hash k).toUSize % USize.ofNat source.size).toNat < i) bucket
H : i < source.size
rank : α → Nat := fun k => ((hash k).toUSize % USize.ofNat source.size).toNat
⊢ ∀ [inst : PartialEquivBEq α] [inst : LawfulHashable α],
    List.Pairwise (fun a b => ¬(a.fst == b.fst) = true) source[i].toList

Tactic:
exact hs₁ _ (Array.getElem_mem_toList ..)

Result:
no goals
-- Mathlib/Algebra/Order/CauSeq/Completion.lean
theorem cau_seq_zero_ne_one : ¬(0 : CauSeq _ abv) ≈ 1 := fun h =>
  have : LimZero (1 - 0 : CauSeq _ abv) := Setoid.symm h
  have : LimZero (1 : CauSeq _ abv)

Proof state:
α : Type u_1
inst✝² : LinearOrderedField α
β : Type u_2
inst✝¹ : DivisionRing β
abv : β → α
inst✝ : IsAbsoluteValue abv
h : 0 ≈ 1
this : (1 - 0).LimZero
⊢ LimZero 1

Tactic:
simpa

Result:
no goals

Proof state:
α : Type u_1
inst✝² : LinearOrderedField α
β : Type u_2
inst✝¹ : DivisionRing β
abv : β → α
inst✝ : IsAbsoluteValue abv
h : 0 ≈ 1
this✝ : (1 - 0).LimZero
this : LimZero 1
⊢ False

Tactic:
apply one_ne_zero <| const_limZero.1 this

Result:
no goals
-- Mathlib/Data/Vector/Basic.lean
theorem head_pmap {p : α → Prop} (f : (a : α) → p a → β) (v : Vector α (n + 1))
    (hp : ∀ x ∈ v.toList, p x) :
    (v.pmap f hp).head = f v.head (hp _ <| by
      rw [← cons_head_tail v, toList_cons, head_cons, List.mem_cons]; exact .inl rfl)

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
φ : Type u_5
m n : ℕ
p : α → Prop
f : (a : α) → p a → β
v : Vector α (n + 1)
hp : ∀ x ∈ v.toList, p x
⊢ v.head ∈ v.toList

Tactic:
rw [← cons_head_tail v, toList_cons, head_cons, List.mem_cons]

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
φ : Type u_5
m n : ℕ
p : α → Prop
f : (a : α) → p a → β
v : Vector α (n + 1)
hp : ∀ x ∈ v.toList, p x
⊢ v.head = v.head ∨ v.head ∈ v.tail.toList

Proof state:
case intro.intro
α : Type u_1
β : Type u_2
n : ℕ
p : α → Prop
f : (a : α) → p a → β
v : Vector α (n + 1)
hp : ∀ x ∈ v.toList, p x
a : α
v' : Vector α n
h : v = a ::ᵥ v'
⊢ (pmap f v hp).head = f v.head ⋯

Tactic:
simp_rw [h, pmap_cons, head_cons]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
n : ℕ
p : α → Prop
f : (a : α) → p a → β
v : Vector α (n + 1)
hp : ∀ x ∈ v.toList, p x
⊢ (pmap f v hp).head = f v.head ⋯

Tactic:
obtain ⟨a, v', h⟩ := Vector.exists_eq_cons v

Result:
case intro.intro
α : Type u_1
β : Type u_2
n : ℕ
p : α → Prop
f : (a : α) → p a → β
v : Vector α (n + 1)
hp : ∀ x ∈ v.toList, p x
a : α
v' : Vector α n
h : v = a ::ᵥ v'
⊢ (pmap f v hp).head = f v.head ⋯

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
σ : Type u_4
φ : Type u_5
m n : ℕ
p : α → Prop
f : (a : α) → p a → β
v : Vector α (n + 1)
hp : ∀ x ∈ v.toList, p x
⊢ v.head = v.head ∨ v.head ∈ v.tail.toList

Tactic:
exact .inl rfl

Result:
no goals
-- Mathlib/Algebra/Algebra/Operations.lean
theorem toSubMulAction_one : (1 : Submodule R A).toSubMulAction = 1 :=
  SetLike.ext fun _ ↦ by rw [one_eq_span, SubMulAction.mem_one]; exact mem_span_singleton

Proof state:
R : Type u
inst✝² : Semiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Module R A
x✝ : A
⊢ x✝ ∈ (span R {1}).toSubMulAction ↔ ∃ r, r • 1 = x✝

Tactic:
exact mem_span_singleton

Result:
no goals

Proof state:
R : Type u
inst✝² : Semiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Module R A
x✝ : A
⊢ x✝ ∈ toSubMulAction 1 ↔ x✝ ∈ 1

Tactic:
rw [one_eq_span, SubMulAction.mem_one]

Result:
R : Type u
inst✝² : Semiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Module R A
x✝ : A
⊢ x✝ ∈ (span R {1}).toSubMulAction ↔ ∃ r, r • 1 = x✝
-- Mathlib/Topology/ContinuousOn.lean
theorem continuousWithinAt_inter' (h : t ∈ 𝓝[s] x) :
    ContinuousWithinAt f (s ∩ t) x ↔ ContinuousWithinAt f s x

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s t : Set α
x : α
h : t ∈ 𝓝[s] x
⊢ ContinuousWithinAt f (s ∩ t) x ↔ ContinuousWithinAt f s x

Tactic:
simp [ContinuousWithinAt, nhdsWithin_restrict'' s h]

Result:
no goals
-- Mathlib/Probability/Moments/MGFAnalytic.lean
/-- For `t ∈ interior (integrableExpSet X μ)`, the n-th derivative of `mgf X μ` at `t` is
`μ[X ^ n * exp (t * X)]`. -/
lemma iteratedDeriv_mgf (ht : t ∈ interior (integrableExpSet X μ)) (n : ℕ) :
    iteratedDeriv n (mgf X μ) t = μ[fun ω ↦ X ω ^ n * exp (t * X ω)]

Proof state:
case zero
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
ht : t ∈ interior (integrableExpSet X μ)
⊢ iteratedDeriv 0 (mgf X μ) t = ∫ (x : Ω), (fun ω => X ω ^ 0 * rexp (t * X ω)) x ∂μ

Tactic:
simp [mgf]

Result:
no goals

Proof state:
case succ
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
n : ℕ
hn :
  ∀ {t : ℝ},
    t ∈ interior (integrableExpSet X μ) →
      iteratedDeriv n (mgf X μ) t = ∫ (x : Ω), (fun ω => X ω ^ n * rexp (t * X ω)) x ∂μ
t : ℝ
ht : t ∈ interior (integrableExpSet X μ)
⊢ deriv (iteratedDeriv n (mgf X μ)) t = ∫ (x : Ω), (fun ω => X ω ^ (n + 1) * rexp (t * X ω)) x ∂μ

Tactic:
exact (hasDerivAt_iteratedDeriv_mgf ht n).deriv

Result:
no goals

Proof state:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
ht : t ∈ interior (integrableExpSet X μ)
n : ℕ
⊢ iteratedDeriv n (mgf X μ) t = ∫ (x : Ω), (fun ω => X ω ^ n * rexp (t * X ω)) x ∂μ

Tactic:
induction n generalizing t with
| zero => simp [mgf]
| succ n hn =>
  rw [iteratedDeriv_succ]
  exact (hasDerivAt_iteratedDeriv_mgf ht n).deriv

Result:
no goals

Proof state:
case succ
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
n : ℕ
hn :
  ∀ {t : ℝ},
    t ∈ interior (integrableExpSet X μ) →
      iteratedDeriv n (mgf X μ) t = ∫ (x : Ω), (fun ω => X ω ^ n * rexp (t * X ω)) x ∂μ
t : ℝ
ht : t ∈ interior (integrableExpSet X μ)
⊢ iteratedDeriv (n + 1) (mgf X μ) t = ∫ (x : Ω), (fun ω => X ω ^ (n + 1) * rexp (t * X ω)) x ∂μ

Tactic:
rw [iteratedDeriv_succ]

Result:
case succ
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
n : ℕ
hn :
  ∀ {t : ℝ},
    t ∈ interior (integrableExpSet X μ) →
      iteratedDeriv n (mgf X μ) t = ∫ (x : Ω), (fun ω => X ω ^ n * rexp (t * X ω)) x ∂μ
t : ℝ
ht : t ∈ interior (integrableExpSet X μ)
⊢ deriv (iteratedDeriv n (mgf X μ)) t = ∫ (x : Ω), (fun ω => X ω ^ (n + 1) * rexp (t * X ω)) x ∂μ
-- Mathlib/Algebra/Polynomial/Inductions.lean
theorem natDegree_divX_eq_natDegree_tsub_one : p.divX.natDegree = p.natDegree - 1

Proof state:
case φ_k
R : Type u
inst✝ : Semiring R
p f : R[X]
⊢ f.natDegree < 1 → divX_hom f = 0

Tactic:
simpa [divX_hom, divX_eq_zero_iff] using eq_C_of_natDegree_eq_zero

Result:
no goals

Proof state:
case neg
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
c : R
c0 : c ≠ 0
n0 : ¬n = 0
⊢ (C c * X ^ (n - 1)).natDegree = n - 1

Tactic:
exact natDegree_C_mul_X_pow (n - 1) c c0

Result:
no goals

Proof state:
case φ_mon
R : Type u
inst✝ : Semiring R
p : R[X]
⊢ ∀ (n : ℕ) (c : R), c ≠ 0 → (divX_hom ((monomial n) c)).natDegree = n - 1

Tactic:
intros n c c0

Result:
case φ_mon
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
c : R
c0 : c ≠ 0
⊢ (divX_hom ((monomial n) c)).natDegree = n - 1

Proof state:
case φ_mon
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
c : R
c0 : c ≠ 0
⊢ (divX_hom ((monomial n) c)).natDegree = n - 1

Tactic:
rw [← C_mul_X_pow_eq_monomial, divX_hom_toFun, divX_C_mul, divX_X_pow]

Result:
case φ_mon
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
c : R
c0 : c ≠ 0
⊢ (C c * if n = 0 then 0 else X ^ (n - 1)).natDegree = n - 1

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
⊢ p.divX.natDegree = p.natDegree - 1

Tactic:
apply map_natDegree_eq_sub (φ := divX_hom)

Result:
case φ_k
R : Type u
inst✝ : Semiring R
p : R[X]
⊢ ∀ (f : R[X]), f.natDegree < 1 → divX_hom f = 0

case φ_mon
R : Type u
inst✝ : Semiring R
p : R[X]
⊢ ∀ (n : ℕ) (c : R), c ≠ 0 → (divX_hom ((monomial n) c)).natDegree = n - 1

Proof state:
case φ_k
R : Type u
inst✝ : Semiring R
p : R[X]
⊢ ∀ (f : R[X]), f.natDegree < 1 → divX_hom f = 0

Tactic:
intro f

Result:
case φ_k
R : Type u
inst✝ : Semiring R
p f : R[X]
⊢ f.natDegree < 1 → divX_hom f = 0

Proof state:
case pos
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
c : R
c0 : c ≠ 0
n0 : n = 0
⊢ (C c * 0).natDegree = n - 1

Tactic:
simp [n0]

Result:
no goals

Proof state:
case φ_mon
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
c : R
c0 : c ≠ 0
⊢ (C c * if n = 0 then 0 else X ^ (n - 1)).natDegree = n - 1

Tactic:
split_ifs with n0

Result:
case pos
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
c : R
c0 : c ≠ 0
n0 : n = 0
⊢ (C c * 0).natDegree = n - 1

case neg
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
c : R
c0 : c ≠ 0
n0 : ¬n = 0
⊢ (C c * X ^ (n - 1)).natDegree = n - 1
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem empty_beq_iff [BEq α] {xs : Array α} : (#[] == xs) = xs.isEmpty

Proof state:
case mk
α : Type u_1
inst✝ : BEq α
toList✝ : List α
⊢ (#[] == { toList := toList✝ }) = { toList := toList✝ }.isEmpty

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
inst✝ : BEq α
xs : Array α
⊢ (#[] == xs) = xs.isEmpty

Tactic:
cases xs

Result:
case mk
α : Type u_1
inst✝ : BEq α
toList✝ : List α
⊢ (#[] == { toList := toList✝ }) = { toList := toList✝ }.isEmpty
-- Mathlib/Data/Finset/Sort.lean
theorem sorted_zero_eq_min'_aux (s : Finset α) (h : 0 < (s.sort (· ≤ ·)).length) (H : s.Nonempty) :
    (s.sort (· ≤ ·)).get ⟨0, h⟩ = s.min' H

Proof state:
case a.intro
α : Type u_1
inst✝ : LinearOrder α
s : Finset α
h : 0 < (sort (fun x1 x2 => x1 ≤ x2) s).length
H : s.Nonempty
l : List α := sort (fun x1 x2 => x1 ≤ x2) s
this : s.min' H ∈ l
i : Fin l.length
hi : l.get i = s.min' H
⊢ (sort (fun x1 x2 => x1 ≤ x2) s).get ⟨0, h⟩ ≤ s.min' H

Tactic:
rw [← hi]

Result:
case a.intro
α : Type u_1
inst✝ : LinearOrder α
s : Finset α
h : 0 < (sort (fun x1 x2 => x1 ≤ x2) s).length
H : s.Nonempty
l : List α := sort (fun x1 x2 => x1 ≤ x2) s
this : s.min' H ∈ l
i : Fin l.length
hi : l.get i = s.min' H
⊢ (sort (fun x1 x2 => x1 ≤ x2) s).get ⟨0, h⟩ ≤ l.get i

Proof state:
case a
α : Type u_1
inst✝ : LinearOrder α
s : Finset α
h : 0 < (sort (fun x1 x2 => x1 ≤ x2) s).length
H : s.Nonempty
l : List α := sort (fun x1 x2 => x1 ≤ x2) s
this : s.min' H ∈ l
⊢ (sort (fun x1 x2 => x1 ≤ x2) s).get ⟨0, h⟩ ≤ s.min' H

Tactic:
obtain ⟨i, hi⟩ : ∃ i, l.get i = s.min' H := List.mem_iff_get.1 this

Result:
case a.intro
α : Type u_1
inst✝ : LinearOrder α
s : Finset α
h : 0 < (sort (fun x1 x2 => x1 ≤ x2) s).length
H : s.Nonempty
l : List α := sort (fun x1 x2 => x1 ≤ x2) s
this : s.min' H ∈ l
i : Fin l.length
hi : l.get i = s.min' H
⊢ (sort (fun x1 x2 => x1 ≤ x2) s).get ⟨0, h⟩ ≤ s.min' H

Proof state:
α : Type u_1
inst✝ : LinearOrder α
s : Finset α
h : 0 < (sort (fun x1 x2 => x1 ≤ x2) s).length
H : s.Nonempty
l : List α := sort (fun x1 x2 => x1 ≤ x2) s
⊢ (sort (fun x1 x2 => x1 ≤ x2) s).get ⟨0, h⟩ = s.min' H

Tactic:
apply le_antisymm

Result:
case a
α : Type u_1
inst✝ : LinearOrder α
s : Finset α
h : 0 < (sort (fun x1 x2 => x1 ≤ x2) s).length
H : s.Nonempty
l : List α := sort (fun x1 x2 => x1 ≤ x2) s
⊢ (sort (fun x1 x2 => x1 ≤ x2) s).get ⟨0, h⟩ ≤ s.min' H

case a
α : Type u_1
inst✝ : LinearOrder α
s : Finset α
h : 0 < (sort (fun x1 x2 => x1 ≤ x2) s).length
H : s.Nonempty
l : List α := sort (fun x1 x2 => x1 ≤ x2) s
⊢ s.min' H ≤ (sort (fun x1 x2 => x1 ≤ x2) s).get ⟨0, h⟩

Proof state:
case a
α : Type u_1
inst✝ : LinearOrder α
s : Finset α
h : 0 < (sort (fun x1 x2 => x1 ≤ x2) s).length
H : s.Nonempty
l : List α := sort (fun x1 x2 => x1 ≤ x2) s
this : l.get ⟨0, h⟩ ∈ s
⊢ s.min' H ≤ (sort (fun x1 x2 => x1 ≤ x2) s).get ⟨0, h⟩

Tactic:
exact s.min'_le _ this

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem getKey_insertManyIfNewUnit_list_mem_of_contains [EquivBEq α] [LawfulHashable α]
    (h : m.1.WF) {l : List α} {k : α} (contains : m.contains k) {h'} :
    getKey (insertManyIfNewUnit m l).1 k h' = getKey m k contains

Proof state:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
m : Raw₀ α fun x => Unit
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.val.WF
l : List α
k : α
contains : m.contains k = true
h' : (insertManyIfNewUnit m l).val.contains k = true
⊢ (insertManyIfNewUnit m l).val.getKey k h' = m.getKey k contains

Tactic:
simp_to_model [Const.insertManyIfNewUnit] using List.getKey_insertListIfNewUnit_of_contains

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Restrict.lean
theorem exists_mem_of_measure_ne_zero_of_ae (hs : μ s ≠ 0) {p : α → Prop}
    (hp : ∀ᵐ x ∂μ.restrict s, p x) : ∃ x, x ∈ s ∧ p x

Proof state:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : μ s ≠ 0
p : α → Prop
hp : ∀ᵐ (x : α) ∂μ.restrict s, p x
⊢ ∃ x ∈ s, p x

Tactic:
rw [← μ.restrict_apply_self, ← frequently_ae_mem_iff] at hs

Result:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : ∃ᵐ (a : α) ∂μ.restrict s, a ∈ s
p : α → Prop
hp : ∀ᵐ (x : α) ∂μ.restrict s, p x
⊢ ∃ x ∈ s, p x

Proof state:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : ∃ᵐ (a : α) ∂μ.restrict s, a ∈ s
p : α → Prop
hp : ∀ᵐ (x : α) ∂μ.restrict s, p x
⊢ ∃ x ∈ s, p x

Tactic:
exact (hs.and_eventually hp).exists

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Erase.lean
theorem erase_append_left [LawfulBEq α] {l₁ : Array α} (l₂) (h : a ∈ l₁) :
    (l₁ ++ l₂).erase a = l₁.erase a ++ l₂

Proof state:
case mk
α : Type u_1
inst✝¹ : BEq α
a : α
inst✝ : LawfulBEq α
l₂ : Array α
l₁ : List α
h : a ∈ { toList := l₁ }
⊢ ({ toList := l₁ } ++ l₂).erase a = { toList := l₁ }.erase a ++ l₂

Tactic:
rcases l₂ with ⟨l₂⟩

Result:
case mk.mk
α : Type u_1
inst✝¹ : BEq α
a : α
inst✝ : LawfulBEq α
l₁ : List α
h : a ∈ { toList := l₁ }
l₂ : List α
⊢ ({ toList := l₁ } ++ { toList := l₂ }).erase a = { toList := l₁ }.erase a ++ { toList := l₂ }

Proof state:
α : Type u_1
inst✝¹ : BEq α
a : α
inst✝ : LawfulBEq α
l₁ : List α
h : a ∈ { toList := l₁ }
l₂ : List α
⊢ a ∈ l₁

Tactic:
simpa using h

Result:
no goals

Proof state:
case mk.mk
α : Type u_1
inst✝¹ : BEq α
a : α
inst✝ : LawfulBEq α
l₁ : List α
h : a ∈ { toList := l₁ }
l₂ : List α
⊢ ({ toList := l₁ } ++ { toList := l₂ }).erase a = { toList := l₁ }.erase a ++ { toList := l₂ }

Tactic:
simpa using List.erase_append_left l₂ (by simpa using h)

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : BEq α
a : α
inst✝ : LawfulBEq α
l₁ l₂ : Array α
h : a ∈ l₁
⊢ (l₁ ++ l₂).erase a = l₁.erase a ++ l₂

Tactic:
rcases l₁ with ⟨l₁⟩

Result:
case mk
α : Type u_1
inst✝¹ : BEq α
a : α
inst✝ : LawfulBEq α
l₂ : Array α
l₁ : List α
h : a ∈ { toList := l₁ }
⊢ ({ toList := l₁ } ++ l₂).erase a = { toList := l₁ }.erase a ++ l₂