harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/List/Sort.lean
theorem mem_orderedInsert {a b : α} {l : List α} :
    a ∈ orderedInsert r b l ↔ a = b ∨ a ∈ l :=
  match l with
  | [] => by simp [orderedInsert]
  | x :: xs => by
    rw [orderedInsert]
    split_ifs
    · simp [orderedInsert]
    · rw [mem_cons, mem_cons, mem_orderedInsert, or_left_comm]

Proof state:
α : Type u
r : α → α → Prop
inst✝ : DecidableRel r
a b : α
l : List α
x : α
xs : List α
⊢ (a ∈ if r b x then b :: x :: xs else x :: orderedInsert r b xs) ↔ a = b ∨ a ∈ x :: xs

Tactic:
split_ifs

Result:
case pos
α : Type u
r : α → α → Prop
inst✝ : DecidableRel r
a b : α
l : List α
x : α
xs : List α
h✝ : r b x
⊢ a ∈ b :: x :: xs ↔ a = b ∨ a ∈ x :: xs

case neg
α : Type u
r : α → α → Prop
inst✝ : DecidableRel r
a b : α
l : List α
x : α
xs : List α
h✝ : ¬r b x
⊢ a ∈ x :: orderedInsert r b xs ↔ a = b ∨ a ∈ x :: xs

Proof state:
α : Type u
r : α → α → Prop
inst✝ : DecidableRel r
a b : α
l : List α
⊢ a ∈ orderedInsert r b [] ↔ a = b ∨ a ∈ []

Tactic:
simp [orderedInsert]

Result:
no goals

Proof state:
α : Type u
r : α → α → Prop
inst✝ : DecidableRel r
a b : α
l : List α
x : α
xs : List α
⊢ a ∈ orderedInsert r b (x :: xs) ↔ a = b ∨ a ∈ x :: xs

Tactic:
rw [orderedInsert]

Result:
α : Type u
r : α → α → Prop
inst✝ : DecidableRel r
a b : α
l : List α
x : α
xs : List α
⊢ (a ∈ if r b x then b :: x :: xs else x :: orderedInsert r b xs) ↔ a = b ∨ a ∈ x :: xs

Proof state:
case pos
α : Type u
r : α → α → Prop
inst✝ : DecidableRel r
a b : α
l : List α
x : α
xs : List α
h✝ : r b x
⊢ a ∈ b :: x :: xs ↔ a = b ∨ a ∈ x :: xs

Tactic:
simp [orderedInsert]

Result:
no goals

Proof state:
case neg
α : Type u
r : α → α → Prop
inst✝ : DecidableRel r
a b : α
l : List α
x : α
xs : List α
h✝ : ¬r b x
⊢ a ∈ x :: orderedInsert r b xs ↔ a = b ∨ a ∈ x :: xs

Tactic:
rw [mem_cons, mem_cons, mem_orderedInsert, or_left_comm]

Result:
no goals
-- Mathlib/Data/Array/ExtractLemmas.lean
theorem extract_extract {s1 e2 e1 s2 : Nat} {a : Array α} (h : s1 + e2 ≤ e1) :
    (a.extract s1 e1).extract s2 e2 = a.extract (s1 + s2) (s1 + e2)

Proof state:
case h₂
α : Type u
s1 e2 e1 s2 : Nat
a : Array α
h : s1 + e2 ≤ e1
⊢ ∀ (i : Nat) (hi₁ : i < ((a.extract s1 e1).extract s2 e2).size) (hi₂ : i < (a.extract (s1 + s2) (s1 + e2)).size),
    ((a.extract s1 e1).extract s2 e2)[i] = (a.extract (s1 + s2) (s1 + e2))[i]

Tactic:
intro i h1 h2

Result:
case h₂
α : Type u
s1 e2 e1 s2 : Nat
a : Array α
h : s1 + e2 ≤ e1
i : Nat
h1 : i < ((a.extract s1 e1).extract s2 e2).size
h2 : i < (a.extract (s1 + s2) (s1 + e2)).size
⊢ ((a.extract s1 e1).extract s2 e2)[i] = (a.extract (s1 + s2) (s1 + e2))[i]

Proof state:
case h₁
α : Type u
s1 e2 e1 s2 : Nat
a : Array α
h : s1 + e2 ≤ e1
⊢ min e2 (min e1 a.size - s1) - s2 = min (s1 + e2) a.size - (s1 + s2)

Tactic:
omega

Result:
no goals

Proof state:
case h₁
α : Type u
s1 e2 e1 s2 : Nat
a : Array α
h : s1 + e2 ≤ e1
⊢ ((a.extract s1 e1).extract s2 e2).size = (a.extract (s1 + s2) (s1 + e2)).size

Tactic:
simp only [size_extract]

Result:
case h₁
α : Type u
s1 e2 e1 s2 : Nat
a : Array α
h : s1 + e2 ≤ e1
⊢ min e2 (min e1 a.size - s1) - s2 = min (s1 + e2) a.size - (s1 + s2)

Proof state:
case h₂
α : Type u
s1 e2 e1 s2 : Nat
a : Array α
h : s1 + e2 ≤ e1
i : Nat
h1 : i < ((a.extract s1 e1).extract s2 e2).size
h2 : i < (a.extract (s1 + s2) (s1 + e2)).size
⊢ ((a.extract s1 e1).extract s2 e2)[i] = (a.extract (s1 + s2) (s1 + e2))[i]

Tactic:
simp only [getElem_extract, Nat.add_assoc]

Result:
no goals

Proof state:
α : Type u
s1 e2 e1 s2 : Nat
a : Array α
h : s1 + e2 ≤ e1
⊢ (a.extract s1 e1).extract s2 e2 = a.extract (s1 + s2) (s1 + e2)

Tactic:
apply ext

Result:
case h₁
α : Type u
s1 e2 e1 s2 : Nat
a : Array α
h : s1 + e2 ≤ e1
⊢ ((a.extract s1 e1).extract s2 e2).size = (a.extract (s1 + s2) (s1 + e2)).size

case h₂
α : Type u
s1 e2 e1 s2 : Nat
a : Array α
h : s1 + e2 ≤ e1
⊢ ∀ (i : Nat) (hi₁ : i < ((a.extract s1 e1).extract s2 e2).size) (hi₂ : i < (a.extract (s1 + s2) (s1 + e2)).size),
    ((a.extract s1 e1).extract s2 e2)[i] = (a.extract (s1 + s2) (s1 + e2))[i]
-- Mathlib/Analysis/Convex/Strict.lean
theorem StrictConvex.inter {t : Set E} (hs : StrictConvex 𝕜 s) (ht : StrictConvex 𝕜 t) :
    StrictConvex 𝕜 (s ∩ t)

Proof state:
𝕜 : Type u_1
E : Type u_3
inst✝³ : OrderedSemiring 𝕜
inst✝² : TopologicalSpace E
inst✝¹ : AddCommMonoid E
inst✝ : SMul 𝕜 E
s t : Set E
hs : StrictConvex 𝕜 s
ht : StrictConvex 𝕜 t
⊢ StrictConvex 𝕜 (s ∩ t)

Tactic:
intro x hx y hy hxy a b ha hb hab

Result:
𝕜 : Type u_1
E : Type u_3
inst✝³ : OrderedSemiring 𝕜
inst✝² : TopologicalSpace E
inst✝¹ : AddCommMonoid E
inst✝ : SMul 𝕜 E
s t : Set E
hs : StrictConvex 𝕜 s
ht : StrictConvex 𝕜 t
x : E
hx : x ∈ s ∩ t
y : E
hy : y ∈ s ∩ t
hxy : x ≠ y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ a • x + b • y ∈ interior (s ∩ t)

Proof state:
𝕜 : Type u_1
E : Type u_3
inst✝³ : OrderedSemiring 𝕜
inst✝² : TopologicalSpace E
inst✝¹ : AddCommMonoid E
inst✝ : SMul 𝕜 E
s t : Set E
hs : StrictConvex 𝕜 s
ht : StrictConvex 𝕜 t
x : E
hx : x ∈ s ∩ t
y : E
hy : y ∈ s ∩ t
hxy : x ≠ y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ a • x + b • y ∈ interior (s ∩ t)

Tactic:
rw [interior_inter]

Result:
𝕜 : Type u_1
E : Type u_3
inst✝³ : OrderedSemiring 𝕜
inst✝² : TopologicalSpace E
inst✝¹ : AddCommMonoid E
inst✝ : SMul 𝕜 E
s t : Set E
hs : StrictConvex 𝕜 s
ht : StrictConvex 𝕜 t
x : E
hx : x ∈ s ∩ t
y : E
hy : y ∈ s ∩ t
hxy : x ≠ y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ a • x + b • y ∈ interior s ∩ interior t

Proof state:
𝕜 : Type u_1
E : Type u_3
inst✝³ : OrderedSemiring 𝕜
inst✝² : TopologicalSpace E
inst✝¹ : AddCommMonoid E
inst✝ : SMul 𝕜 E
s t : Set E
hs : StrictConvex 𝕜 s
ht : StrictConvex 𝕜 t
x : E
hx : x ∈ s ∩ t
y : E
hy : y ∈ s ∩ t
hxy : x ≠ y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ a • x + b • y ∈ interior s ∩ interior t

Tactic:
exact ⟨hs hx.1 hy.1 hxy ha hb hab, ht hx.2 hy.2 hxy ha hb hab⟩

Result:
no goals
-- Mathlib/Analysis/Calculus/IteratedDeriv/Lemmas.lean
theorem iteratedDeriv_const_smul {n : ℕ} {f : 𝕜 → F} (h : ContDiffAt 𝕜 n f x) (c : 𝕜) :
    iteratedDeriv n (c • f) x = c • iteratedDeriv n f x

Proof state:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
x : 𝕜
n : ℕ
f : 𝕜 → F
h : ContDiffAt 𝕜 (↑n) f x
c : 𝕜
⊢ iteratedDeriv n (c • f) x = c • iteratedDeriv n f x

Tactic:
simpa only [iteratedDerivWithin_univ] using
  iteratedDerivWithin_const_smul (Set.mem_univ x) uniqueDiffOn_univ
    c (contDiffWithinAt_univ.mpr h)

Result:
no goals
-- Mathlib/MeasureTheory/Integral/TorusIntegral.lean
theorem torusIntegral_radius_zero (hn : n ≠ 0) (f : ℂⁿ → E) (c : ℂⁿ) :
    (∯ x in T(c, 0), f x) = 0

Proof state:
n : ℕ
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
hn : n ≠ 0
f : (Fin n → ℂ) → E
c : Fin n → ℂ
⊢ (∯ (x : Fin n → ℂ) in T(c, 0), f x) = 0

Tactic:
simp only [torusIntegral, Pi.zero_apply, ofReal_zero, mul_zero, zero_mul, Fin.prod_const,
  zero_pow hn, zero_smul, integral_zero]

Result:
no goals
-- Mathlib/Order/SupIndep.lean
theorem iSupIndep.comp {ι ι' : Sort*} {t : ι → α} {f : ι' → ι} (ht : iSupIndep t)
    (hf : Injective f) : iSupIndep (t ∘ f) := fun i =>
  (ht (f i)).mono_right <| by
    refine (iSup_mono fun i => ?_).trans (iSup_comp_le _ f)
    exact iSup_const_mono hf.ne

Proof state:
α : Type u_1
inst✝ : CompleteLattice α
ι : Sort u_5
ι' : Sort u_6
t : ι → α
f : ι' → ι
ht : iSupIndep t
hf : Injective f
i✝ i : ι'
⊢ ⨆ (_ : i ≠ i✝), (t ∘ f) i ≤ ⨆ (_ : f i ≠ f i✝), t (f i)

Tactic:
exact iSup_const_mono hf.ne

Result:
no goals

Proof state:
α : Type u_1
inst✝ : CompleteLattice α
ι : Sort u_5
ι' : Sort u_6
t : ι → α
f : ι' → ι
ht : iSupIndep t
hf : Injective f
i : ι'
⊢ ⨆ j, ⨆ (_ : j ≠ i), (t ∘ f) j ≤ ⨆ j, ⨆ (_ : j ≠ f i), t j

Tactic:
refine (iSup_mono fun i => ?_).trans (iSup_comp_le _ f)

Result:
α : Type u_1
inst✝ : CompleteLattice α
ι : Sort u_5
ι' : Sort u_6
t : ι → α
f : ι' → ι
ht : iSupIndep t
hf : Injective f
i✝ i : ι'
⊢ ⨆ (_ : i ≠ i✝), (t ∘ f) i ≤ ⨆ (_ : f i ≠ f i✝), t (f i)
-- Mathlib/Analysis/Calculus/Deriv/Mul.lean
theorem HasStrictDerivAt.clm_apply (hc : HasStrictDerivAt c c' x) (hu : HasStrictDerivAt u u' x) :
    HasStrictDerivAt (fun y => (c y) (u y)) (c' (u x) + c x u') x

Proof state:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type v
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
x : 𝕜
G : Type u_2
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
c : 𝕜 → F →L[𝕜] G
c' : F →L[𝕜] G
u : 𝕜 → F
u' : F
hc : HasStrictDerivAt c c' x
hu : HasStrictDerivAt u u' x
this : HasStrictDerivAt (fun y => (c y) (u y)) (((c x).comp (smulRight 1 u') + (smulRight 1 c').flip (u x)) 1) x
⊢ HasStrictDerivAt (fun y => (c y) (u y)) (c' (u x) + (c x) u') x

Tactic:
rwa [add_apply, comp_apply, flip_apply, smulRight_apply, smulRight_apply, one_apply, one_smul,
  one_smul, add_comm] at this

Result:
no goals

Proof state:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type v
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
x : 𝕜
G : Type u_2
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
c : 𝕜 → F →L[𝕜] G
c' : F →L[𝕜] G
u : 𝕜 → F
u' : F
hc : HasStrictDerivAt c c' x
hu : HasStrictDerivAt u u' x
⊢ HasStrictDerivAt (fun y => (c y) (u y)) (c' (u x) + (c x) u') x

Tactic:
have := (hc.hasStrictFDerivAt.clm_apply hu.hasStrictFDerivAt).hasStrictDerivAt

Result:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
F : Type v
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
x : 𝕜
G : Type u_2
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
c : 𝕜 → F →L[𝕜] G
c' : F →L[𝕜] G
u : 𝕜 → F
u' : F
hc : HasStrictDerivAt c c' x
hu : HasStrictDerivAt u u' x
this : HasStrictDerivAt (fun y => (c y) (u y)) (((c x).comp (smulRight 1 u') + (smulRight 1 c').flip (u x)) 1) x
⊢ HasStrictDerivAt (fun y => (c y) (u y)) (c' (u x) + (c x) u') x
-- Mathlib/RingTheory/SimpleRing/Basic.lean
lemma one_mem_of_ne_zero_mem {A : Type*} [NonAssocRing A] [IsSimpleRing A] (I : TwoSidedIdeal A)
    {x : A} (hx : x ≠ 0) (hxI : x ∈ I) : (1 : A) ∈ I :=
  one_mem_of_ne_bot I (by rintro rfl; exact hx hxI)

Proof state:
A : Type u_2
inst✝¹ : NonAssocRing A
inst✝ : IsSimpleRing A
I : TwoSidedIdeal A
x : A
hx : x ≠ 0
hxI : x ∈ I
⊢ I ≠ ⊥

Tactic:
rintro rfl

Result:
A : Type u_2
inst✝¹ : NonAssocRing A
inst✝ : IsSimpleRing A
x : A
hx : x ≠ 0
hxI : x ∈ ⊥
⊢ False

Proof state:
A : Type u_2
inst✝¹ : NonAssocRing A
inst✝ : IsSimpleRing A
x : A
hx : x ≠ 0
hxI : x ∈ ⊥
⊢ False

Tactic:
exact hx hxI

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Walk.lean
lemma getVert_cons {u v w n} (p : G.Walk v w) (h : G.Adj u v) (hn : n ≠ 0) :
    (p.cons h).getVert n = p.getVert (n - 1)

Proof state:
V : Type u
G : SimpleGraph V
u v w : V
n : ℕ
p : G.Walk v w
h : G.Adj u v
hn : n ≠ 0
⊢ (cons h p).getVert n = p.getVert (n - 1)

Tactic:
obtain ⟨n, rfl⟩ := Nat.exists_eq_add_one_of_ne_zero hn

Result:
case intro
V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk v w
h : G.Adj u v
n : ℕ
hn : n + 1 ≠ 0
⊢ (cons h p).getVert (n + 1) = p.getVert (n + 1 - 1)

Proof state:
case intro
V : Type u
G : SimpleGraph V
u v w : V
p : G.Walk v w
h : G.Adj u v
n : ℕ
hn : n + 1 ≠ 0
⊢ (cons h p).getVert (n + 1) = p.getVert (n + 1 - 1)

Tactic:
rw [getVert_cons_succ, Nat.add_sub_cancel]

Result:
no goals
-- Mathlib/RingTheory/Polynomial/Content.lean
theorem dvd_content_iff_C_dvd {p : R[X]} {r : R} : r ∣ p.content ↔ C r ∣ p

Proof state:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
r : R
⊢ r ∣ p.content ↔ C r ∣ p

Tactic:
rw [C_dvd_iff_dvd_coeff]

Result:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
r : R
⊢ r ∣ p.content ↔ ∀ (i : ℕ), r ∣ p.coeff i

Proof state:
case mpr
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
r : R
h : ∀ (i : ℕ), r ∣ p.coeff i
⊢ r ∣ p.content

Tactic:
rw [content, Finset.dvd_gcd_iff]

Result:
case mpr
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
r : R
h : ∀ (i : ℕ), r ∣ p.coeff i
⊢ ∀ b ∈ p.support, r ∣ p.coeff b

Proof state:
case mp
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
r : R
h : r ∣ p.content
i : ℕ
⊢ r ∣ p.coeff i

Tactic:
apply h.trans (content_dvd_coeff _)

Result:
no goals

Proof state:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
r : R
⊢ r ∣ p.content ↔ ∀ (i : ℕ), r ∣ p.coeff i

Tactic:
constructor

Result:
case mp
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
r : R
⊢ r ∣ p.content → ∀ (i : ℕ), r ∣ p.coeff i

case mpr
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
r : R
⊢ (∀ (i : ℕ), r ∣ p.coeff i) → r ∣ p.content

Proof state:
case mp
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
r : R
⊢ r ∣ p.content → ∀ (i : ℕ), r ∣ p.coeff i

Tactic:
intro h i

Result:
case mp
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
r : R
h : r ∣ p.content
i : ℕ
⊢ r ∣ p.coeff i

Proof state:
case mpr
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
r : R
⊢ (∀ (i : ℕ), r ∣ p.coeff i) → r ∣ p.content

Tactic:
intro h

Result:
case mpr
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
r : R
h : ∀ (i : ℕ), r ∣ p.coeff i
⊢ r ∣ p.content

Proof state:
case mpr
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
r : R
h : ∀ (i : ℕ), r ∣ p.coeff i
⊢ ∀ b ∈ p.support, r ∣ p.coeff b

Tactic:
intro i _

Result:
case mpr
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
r : R
h : ∀ (i : ℕ), r ∣ p.coeff i
i : ℕ
a✝ : i ∈ p.support
⊢ r ∣ p.coeff i

Proof state:
case mpr
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : NormalizedGCDMonoid R
p : R[X]
r : R
h : ∀ (i : ℕ), r ∣ p.coeff i
i : ℕ
a✝ : i ∈ p.support
⊢ r ∣ p.coeff i

Tactic:
apply h i

Result:
no goals
-- Mathlib/Algebra/Polynomial/Roots.lean
theorem roots_map_of_injective_of_card_eq_natDegree [IsDomain A] [IsDomain B] {p : A[X]}
    {f : A →+* B} (hf : Function.Injective f) (hroots : Multiset.card p.roots = p.natDegree) :
    p.roots.map f = (p.map f).roots

Proof state:
A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : IsDomain A
inst✝ : IsDomain B
p : A[X]
f : A →+* B
hf : Function.Injective ⇑f
hroots : p.roots.card = p.natDegree
⊢ Multiset.map (⇑f) p.roots = (map f p).roots

Tactic:
apply Multiset.eq_of_le_of_card_le (map_roots_le_of_injective p hf)

Result:
A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : IsDomain A
inst✝ : IsDomain B
p : A[X]
f : A →+* B
hf : Function.Injective ⇑f
hroots : p.roots.card = p.natDegree
⊢ (map f p).roots.card ≤ (Multiset.map (⇑f) p.roots).card

Proof state:
A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : IsDomain A
inst✝ : IsDomain B
p : A[X]
f : A →+* B
hf : Function.Injective ⇑f
hroots : p.roots.card = p.natDegree
⊢ (map f p).roots.card ≤ (Multiset.map (⇑f) p.roots).card

Tactic:
simpa only [Multiset.card_map, hroots] using (card_roots' _).trans natDegree_map_le

Result:
no goals
-- Mathlib/CategoryTheory/Sites/Sheaf.lean
lemma Presheaf.IsSheaf.isSheafFor {P : Cᵒᵖ ⥤ Type w} (hP : Presheaf.IsSheaf J P)
    {X : C} (S : Sieve X) (hS : S ∈ J X) : Presieve.IsSheafFor P S.arrows

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
J : GrothendieckTopology C
P : Cᵒᵖ ⥤ Type w
hP : IsSheaf J P
X : C
S : Sieve X
hS : S ∈ J X
⊢ Presieve.IsSheafFor P S.arrows

Tactic:
rw [isSheaf_iff_isSheaf_of_type] at hP

Result:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
J : GrothendieckTopology C
P : Cᵒᵖ ⥤ Type w
hP : Presieve.IsSheaf J P
X : C
S : Sieve X
hS : S ∈ J X
⊢ Presieve.IsSheafFor P S.arrows

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
J : GrothendieckTopology C
P : Cᵒᵖ ⥤ Type w
hP : Presieve.IsSheaf J P
X : C
S : Sieve X
hS : S ∈ J X
⊢ Presieve.IsSheafFor P S.arrows

Tactic:
exact hP S hS

Result:
no goals
-- Mathlib/Algebra/CharP/Defs.lean
lemma spec : ∀ x : ℕ, (x : R) = 0 ↔ ringChar R ∣ x

Proof state:
R : Type u_1
inst✝ : NonAssocSemiring R
⊢ ∀ (x : ℕ), ↑x = 0 ↔ ringChar R ∣ x

Tactic:
letI : CharP R (ringChar R) := (Classical.choose_spec (CharP.existsUnique R)).1

Result:
R : Type u_1
inst✝ : NonAssocSemiring R
this : CharP R (ringChar R) := (Classical.choose_spec (CharP.existsUnique R)).left
⊢ ∀ (x : ℕ), ↑x = 0 ↔ ringChar R ∣ x

Proof state:
R : Type u_1
inst✝ : NonAssocSemiring R
this : CharP R (ringChar R) := (Classical.choose_spec (CharP.existsUnique R)).left
⊢ ∀ (x : ℕ), ↑x = 0 ↔ ringChar R ∣ x

Tactic:
exact CharP.cast_eq_zero_iff R (ringChar R)

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/Products.lean
@[simp]
lemma Sigma.map_id {f : α → C} [HasCoproduct f] : Sigma.map (fun a => 𝟙 (f a)) = 𝟙 (∐ f)

Proof state:
case h
α : Type w₂
C : Type u
inst✝¹ : Category.{v, u} C
f : α → C
inst✝ : HasCoproduct f
b✝ : α
⊢ (ι f b✝ ≫ map fun a => 𝟙 (f a)) = ι f b✝ ≫ 𝟙 (∐ f)

Tactic:
simp

Result:
no goals

Proof state:
α : Type w₂
C : Type u
inst✝¹ : Category.{v, u} C
f : α → C
inst✝ : HasCoproduct f
⊢ (map fun a => 𝟙 (f a)) = 𝟙 (∐ f)

Tactic:
ext

Result:
case h
α : Type w₂
C : Type u
inst✝¹ : Category.{v, u} C
f : α → C
inst✝ : HasCoproduct f
b✝ : α
⊢ (ι f b✝ ≫ map fun a => 𝟙 (f a)) = ι f b✝ ≫ 𝟙 (∐ f)
-- Mathlib/LinearAlgebra/LinearIndependent/Basic.lean
theorem LinearIndependent.map' (hv : LinearIndependent R v) (f : M →ₗ[R] M')
    (hf_inj : LinearMap.ker f = ⊥) : LinearIndependent R (f ∘ v) :=
  hv.map <| by simp_rw [hf_inj, disjoint_bot_right]

Proof state:
ι : Type u'
R : Type u_2
M : Type u_4
M' : Type u_5
v : ι → M
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup M'
inst✝¹ : Module R M
inst✝ : Module R M'
hv : LinearIndependent R v
f : M →ₗ[R] M'
hf_inj : LinearMap.ker f = ⊥
⊢ Disjoint (span R (range v)) (LinearMap.ker f)

Tactic:
simp_rw [hf_inj, disjoint_bot_right]

Result:
no goals
-- Mathlib/MeasureTheory/Decomposition/Exhaustion.lean
lemma restrict_compl_sigmaFiniteSetWRT [SFinite ν] (hμν : μ ≪ ν) :
    μ.restrict (μ.sigmaFiniteSetWRT ν)ᶜ = ∞ • ν.restrict (μ.sigmaFiniteSetWRT ν)ᶜ

Proof state:
case pos
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝ : SFinite ν
hμν : μ ≪ ν
s : Set α
a✝ : MeasurableSet s
hνs : ν (s ∩ (μ.sigmaFiniteSetWRT ν)ᶜ) = 0
⊢ μ (s ∩ (μ.sigmaFiniteSetWRT ν)ᶜ) = ⊤ * ν (s ∩ (μ.sigmaFiniteSetWRT ν)ᶜ)

Tactic:
rw [hνs, mul_zero]

Result:
case pos
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝ : SFinite ν
hμν : μ ≪ ν
s : Set α
a✝ : MeasurableSet s
hνs : ν (s ∩ (μ.sigmaFiniteSetWRT ν)ᶜ) = 0
⊢ μ (s ∩ (μ.sigmaFiniteSetWRT ν)ᶜ) = 0

Proof state:
case h
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝ : SFinite ν
hμν : μ ≪ ν
s : Set α
a✝ : MeasurableSet s
⊢ μ (s ∩ (μ.sigmaFiniteSetWRT ν)ᶜ) = ⊤ * ν (s ∩ (μ.sigmaFiniteSetWRT ν)ᶜ)

Tactic:
by_cases hνs : ν (s ∩ (μ.sigmaFiniteSetWRT ν)ᶜ) = 0

Result:
case pos
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝ : SFinite ν
hμν : μ ≪ ν
s : Set α
a✝ : MeasurableSet s
hνs : ν (s ∩ (μ.sigmaFiniteSetWRT ν)ᶜ) = 0
⊢ μ (s ∩ (μ.sigmaFiniteSetWRT ν)ᶜ) = ⊤ * ν (s ∩ (μ.sigmaFiniteSetWRT ν)ᶜ)

case neg
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝ : SFinite ν
hμν : μ ≪ ν
s : Set α
a✝ : MeasurableSet s
hνs : ¬ν (s ∩ (μ.sigmaFiniteSetWRT ν)ᶜ) = 0
⊢ μ (s ∩ (μ.sigmaFiniteSetWRT ν)ᶜ) = ⊤ * ν (s ∩ (μ.sigmaFiniteSetWRT ν)ᶜ)

Proof state:
case h
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝ : SFinite ν
hμν : μ ≪ ν
s : Set α
a✝ : MeasurableSet s
⊢ (μ.restrict (μ.sigmaFiniteSetWRT ν)ᶜ) s = (⊤ • ν.restrict (μ.sigmaFiniteSetWRT ν)ᶜ) s

Tactic:
rw [Measure.restrict_apply' measurableSet_sigmaFiniteSetWRT.compl,
  Measure.smul_apply, smul_eq_mul,
  Measure.restrict_apply' measurableSet_sigmaFiniteSetWRT.compl]

Result:
case h
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝ : SFinite ν
hμν : μ ≪ ν
s : Set α
a✝ : MeasurableSet s
⊢ μ (s ∩ (μ.sigmaFiniteSetWRT ν)ᶜ) = ⊤ * ν (s ∩ (μ.sigmaFiniteSetWRT ν)ᶜ)

Proof state:
case pos
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝ : SFinite ν
hμν : μ ≪ ν
s : Set α
a✝ : MeasurableSet s
hνs : ν (s ∩ (μ.sigmaFiniteSetWRT ν)ᶜ) = 0
⊢ μ (s ∩ (μ.sigmaFiniteSetWRT ν)ᶜ) = 0

Tactic:
exact hμν hνs

Result:
no goals

Proof state:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝ : SFinite ν
hμν : μ ≪ ν
⊢ μ.restrict (μ.sigmaFiniteSetWRT ν)ᶜ = ⊤ • ν.restrict (μ.sigmaFiniteSetWRT ν)ᶜ

Tactic:
ext s

Result:
case h
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝ : SFinite ν
hμν : μ ≪ ν
s : Set α
a✝ : MeasurableSet s
⊢ (μ.restrict (μ.sigmaFiniteSetWRT ν)ᶜ) s = (⊤ • ν.restrict (μ.sigmaFiniteSetWRT ν)ᶜ) s

Proof state:
case neg
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
inst✝ : SFinite ν
hμν : μ ≪ ν
s : Set α
a✝ : MeasurableSet s
hνs : ¬ν (s ∩ (μ.sigmaFiniteSetWRT ν)ᶜ) = 0
⊢ μ (s ∩ (μ.sigmaFiniteSetWRT ν)ᶜ) = ⊤ * ν (s ∩ (μ.sigmaFiniteSetWRT ν)ᶜ)

Tactic:
rw [ENNReal.top_mul hνs, measure_eq_top_of_subset_compl_sigmaFiniteSetWRT
  Set.inter_subset_right hνs]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Erase.lean
theorem size_eraseP_le (l : Array α) : (l.eraseP p).size ≤ l.size

Proof state:
α : Type u_1
p : α → Bool
l : Array α
⊢ (l.eraseP p).size ≤ l.size

Tactic:
rcases l with ⟨l⟩

Result:
case mk
α : Type u_1
p : α → Bool
l : List α
⊢ ({ toList := l }.eraseP p).size ≤ { toList := l }.size

Proof state:
case mk
α : Type u_1
p : α → Bool
l : List α
⊢ ({ toList := l }.eraseP p).size ≤ { toList := l }.size

Tactic:
simpa using List.length_eraseP_le l

Result:
no goals
-- Mathlib/Data/Rat/Defs.lean
protected lemma nonneg_total (a : ℚ) : 0 ≤ a ∨ 0 ≤ -a

Proof state:
a : ℚ
⊢ 0 ≤ a ∨ 0 ≤ -a

Tactic:
simp_rw [← num_nonneg, num_neg_eq_neg_num, Int.neg_nonneg]

Result:
a : ℚ
⊢ 0 ≤ a.num ∨ a.num ≤ 0

Proof state:
a : ℚ
⊢ 0 ≤ a.num ∨ a.num ≤ 0

Tactic:
exact Int.le_total _ _

Result:
no goals