harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/List/Permutation.lean
theorem getElem_permutations'Aux (s : List α) (x : α) (n : ℕ)
    (hn : n < length (permutations'Aux x s)) :
    (permutations'Aux x s)[n] = s.insertIdx n x

Proof state:
case cons.succ
α : Type u_1
x y : α
s : List α
IH : ∀ (n : ℕ) (hn : n < (permutations'Aux x s).length), (permutations'Aux x s)[n] = insertIdx n x s
n✝ : ℕ
hn : n✝ + 1 < (permutations'Aux x (y :: s)).length
⊢ (permutations'Aux x (y :: s))[n✝ + 1] = insertIdx (n✝ + 1) x (y :: s)

Tactic:
simpa [get] using IH _ _

Result:
no goals

Proof state:
α : Type u_1
s : List α
x : α
n : ℕ
hn : n < (permutations'Aux x s).length
⊢ (permutations'Aux x s)[n] = insertIdx n x s

Tactic:
induction' s with y s IH generalizing n

Result:
case nil
α : Type u_1
x : α
n : ℕ
hn : n < (permutations'Aux x []).length
⊢ (permutations'Aux x [])[n] = insertIdx n x []

case cons
α : Type u_1
x y : α
s : List α
IH : ∀ (n : ℕ) (hn : n < (permutations'Aux x s).length), (permutations'Aux x s)[n] = insertIdx n x s
n : ℕ
hn : n < (permutations'Aux x (y :: s)).length
⊢ (permutations'Aux x (y :: s))[n] = insertIdx n x (y :: s)

Proof state:
case nil
α : Type u_1
x : α
n : ℕ
hn : n < (permutations'Aux x []).length
⊢ (permutations'Aux x [])[n] = insertIdx n x []

Tactic:
simp only [permutations'Aux, length, Nat.zero_add, lt_one_iff] at hn

Result:
case nil
α : Type u_1
x : α
n : ℕ
hn✝ : n < (permutations'Aux x []).length
hn : n = 0
⊢ (permutations'Aux x [])[n] = insertIdx n x []

Proof state:
case nil
α : Type u_1
x : α
n : ℕ
hn✝ : n < (permutations'Aux x []).length
hn : n = 0
⊢ (permutations'Aux x [])[n] = insertIdx n x []

Tactic:
simp [hn]

Result:
no goals

Proof state:
case cons
α : Type u_1
x y : α
s : List α
IH : ∀ (n : ℕ) (hn : n < (permutations'Aux x s).length), (permutations'Aux x s)[n] = insertIdx n x s
n : ℕ
hn : n < (permutations'Aux x (y :: s)).length
⊢ (permutations'Aux x (y :: s))[n] = insertIdx n x (y :: s)

Tactic:
cases n

Result:
case cons.zero
α : Type u_1
x y : α
s : List α
IH : ∀ (n : ℕ) (hn : n < (permutations'Aux x s).length), (permutations'Aux x s)[n] = insertIdx n x s
hn : 0 < (permutations'Aux x (y :: s)).length
⊢ (permutations'Aux x (y :: s))[0] = insertIdx 0 x (y :: s)

case cons.succ
α : Type u_1
x y : α
s : List α
IH : ∀ (n : ℕ) (hn : n < (permutations'Aux x s).length), (permutations'Aux x s)[n] = insertIdx n x s
n✝ : ℕ
hn : n✝ + 1 < (permutations'Aux x (y :: s)).length
⊢ (permutations'Aux x (y :: s))[n✝ + 1] = insertIdx (n✝ + 1) x (y :: s)

Proof state:
case cons.zero
α : Type u_1
x y : α
s : List α
IH : ∀ (n : ℕ) (hn : n < (permutations'Aux x s).length), (permutations'Aux x s)[n] = insertIdx n x s
hn : 0 < (permutations'Aux x (y :: s)).length
⊢ (permutations'Aux x (y :: s))[0] = insertIdx 0 x (y :: s)

Tactic:
simp [get]

Result:
no goals
-- Mathlib/RingTheory/Spectrum/Prime/Topology.lean
theorem zeroLocus_vanishingIdeal_eq_closure (t : Set (PrimeSpectrum R)) :
    zeroLocus (vanishingIdeal t : Set R) = closure t

Proof state:
case intro
R : Type u
inst✝ : CommSemiring R
t : Set (PrimeSpectrum R)
I : Set R
hI : closure t = zeroLocus I
⊢ t ⊆ closure t ∧ t ⊆ zeroLocus ↑(vanishingIdeal t)

Tactic:
exact ⟨subset_closure, subset_zeroLocus_vanishingIdeal t⟩

Result:
no goals

Proof state:
R : Type u
inst✝ : CommSemiring R
t : Set (PrimeSpectrum R)
⊢ zeroLocus ↑(vanishingIdeal t) = closure t

Tactic:
rcases isClosed_iff_zeroLocus (closure t) |>.mp isClosed_closure with ⟨I, hI⟩

Result:
case intro
R : Type u
inst✝ : CommSemiring R
t : Set (PrimeSpectrum R)
I : Set R
hI : closure t = zeroLocus I
⊢ zeroLocus ↑(vanishingIdeal t) = closure t

Proof state:
case intro
R : Type u
inst✝ : CommSemiring R
t : Set (PrimeSpectrum R)
I : Set R
hI : closure t = zeroLocus I
⊢ zeroLocus ↑(vanishingIdeal t) = closure t

Tactic:
rw [subset_antisymm_iff, (isClosed_zeroLocus _).closure_subset_iff, hI,
    subset_zeroLocus_iff_subset_vanishingIdeal, (gc R).u_l_u_eq_u,
    ← subset_zeroLocus_iff_subset_vanishingIdeal, ← hI]

Result:
case intro
R : Type u
inst✝ : CommSemiring R
t : Set (PrimeSpectrum R)
I : Set R
hI : closure t = zeroLocus I
⊢ t ⊆ closure t ∧ t ⊆ zeroLocus ↑(vanishingIdeal t)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Nat/Range.lean
theorem mk_mem_enumFrom_iff_le_and_getElem?_sub {n i : Nat} {x : α} {l : List α} :
    (i, x) ∈ enumFrom n l ↔ n ≤ i ∧ l[i - n]? = x

Proof state:
α : Type u_1
n i : Nat
x : α
l : List α
⊢ (i, x) ∈ enumFrom n l ↔ n ≤ i ∧ l[i - n]? = some x

Tactic:
if h : n ≤ i then
  rcases Nat.exists_eq_add_of_le h with ⟨i, rfl⟩
  simp [mk_add_mem_enumFrom_iff_getElem?, Nat.add_sub_cancel_left]
else
  have : ∀ k, n + k ≠ i := by rintro k rfl; simp at h
  simp [h, mem_iff_get?, this]

Result:
no goals

Proof state:
α : Type u_1
n : Nat
x : α
l : List α
k : Nat
h : ¬n ≤ n + k
⊢ False

Tactic:
simp at h

Result:
no goals

Proof state:
α : Type u_1
n i : Nat
x : α
l : List α
h : ¬n ≤ i
⊢ ∀ (k : Nat), n + k ≠ i

Tactic:
rintro k rfl

Result:
α : Type u_1
n : Nat
x : α
l : List α
k : Nat
h : ¬n ≤ n + k
⊢ False

Proof state:
α : Type u_1
n i : Nat
x : α
l : List α
h : ¬n ≤ i
⊢ (i, x) ∈ enumFrom n l ↔ n ≤ i ∧ l[i - n]? = some x

Tactic:
have : ∀ k, n + k ≠ i := by rintro k rfl; simp at h

Result:
α : Type u_1
n i : Nat
x : α
l : List α
h : ¬n ≤ i
this : ∀ (k : Nat), n + k ≠ i
⊢ (i, x) ∈ enumFrom n l ↔ n ≤ i ∧ l[i - n]? = some x

Proof state:
α : Type u_1
n i : Nat
x : α
l : List α
h : ¬n ≤ i
this : ∀ (k : Nat), n + k ≠ i
⊢ (i, x) ∈ enumFrom n l ↔ n ≤ i ∧ l[i - n]? = some x

Tactic:
simp [h, mem_iff_get?, this]

Result:
no goals

Proof state:
α : Type u_1
n i : Nat
x : α
l : List α
h : n ≤ i
⊢ (i, x) ∈ enumFrom n l ↔ n ≤ i ∧ l[i - n]? = some x

Tactic:
rcases Nat.exists_eq_add_of_le h with ⟨i, rfl⟩

Result:
case intro
α : Type u_1
n : Nat
x : α
l : List α
i : Nat
h : n ≤ n + i
⊢ (n + i, x) ∈ enumFrom n l ↔ n ≤ n + i ∧ l[n + i - n]? = some x

Proof state:
case intro
α : Type u_1
n : Nat
x : α
l : List α
i : Nat
h : n ≤ n + i
⊢ (n + i, x) ∈ enumFrom n l ↔ n ≤ n + i ∧ l[n + i - n]? = some x

Tactic:
simp [mk_add_mem_enumFrom_iff_getElem?, Nat.add_sub_cancel_left]

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Affine.lean
lemma baseChange_negAddY : (W'.baseChange B).toAffine.negAddY (f x₁) (f x₂) (f y₁) (f ℓ) =
    f ((W'.baseChange A).toAffine.negAddY x₁ x₂ y₁ ℓ)

Proof state:
R : Type r
S : Type s
A : Type u
B : Type v
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : CommRing A
inst✝⁷ : CommRing B
W' : Affine R
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra R A
inst✝⁴ : Algebra S A
inst✝³ : IsScalarTower R S A
inst✝² : Algebra R B
inst✝¹ : Algebra S B
inst✝ : IsScalarTower R S B
f : A →ₐ[S] B
x₁ y₁ x₂ ℓ : A
⊢ (baseChange W' B).toAffine.negAddY (f x₁) (f x₂) (f y₁) (f ℓ) = f ((baseChange W' A).toAffine.negAddY x₁ x₂ y₁ ℓ)

Tactic:
rw [← RingHom.coe_coe, ← map_negAddY, map_baseChange]

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Arithmetic.lean
theorem lsub_empty {ι} [h : IsEmpty ι] (f : ι → Ordinal) : lsub f = 0

Proof state:
ι : Type u_4
h : IsEmpty ι
f : ι → Ordinal.{max u_5 u_4}
⊢ ∀ (i : ι), f i < 0

Tactic:
exact h.elim

Result:
no goals

Proof state:
ι : Type u_4
h : IsEmpty ι
f : ι → Ordinal.{max u_5 u_4}
⊢ lsub f = 0

Tactic:
rw [← Ordinal.le_zero, lsub_le_iff]

Result:
ι : Type u_4
h : IsEmpty ι
f : ι → Ordinal.{max u_5 u_4}
⊢ ∀ (i : ι), f i < 0
-- Mathlib/Probability/Kernel/Composition/IntegralCompProd.lean
theorem integral_comp : ∀ {f : γ → E} (_ : Integrable f ((η ∘ₖ κ) a)),
    ∫ z, f z ∂(η ∘ₖ κ) a = ∫ x, ∫ y, f y ∂η x ∂κ a

Proof state:
case pos.h_ind
α : Type u_1
β : Type u_2
γ : Type u_3
E : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : NormedAddCommGroup E
a : α
κ : Kernel α β
η : Kernel β γ
inst✝ : NormedSpace ℝ E
f✝ : γ → E
hE : CompleteSpace E
⊢ ∀ (c : E) ⦃s : Set γ⦄,
    MeasurableSet s →
      ((η ∘ₖ κ) a) s < ⊤ →
        ∫ (z : γ), s.indicator (fun x => c) z ∂(η ∘ₖ κ) a = ∫ (x : β), ∫ (y : γ), s.indicator (fun x => c) y ∂η x ∂κ a

Tactic:
intro c s hs ms

Result:
case pos.h_ind
α : Type u_1
β : Type u_2
γ : Type u_3
E : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : NormedAddCommGroup E
a : α
κ : Kernel α β
η : Kernel β γ
inst✝ : NormedSpace ℝ E
f✝ : γ → E
hE : CompleteSpace E
c : E
s : Set γ
hs : MeasurableSet s
ms : ((η ∘ₖ κ) a) s < ⊤
⊢ ∫ (z : γ), s.indicator (fun x => c) z ∂(η ∘ₖ κ) a = ∫ (x : β), ∫ (y : γ), s.indicator (fun x => c) y ∂η x ∂κ a

Proof state:
case pos.h_ind.e_a.hf
α : Type u_1
β : Type u_2
γ : Type u_3
E : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : NormedAddCommGroup E
a : α
κ : Kernel α β
η : Kernel β γ
inst✝ : NormedSpace ℝ E
f✝ : γ → E
hE : CompleteSpace E
c : E
s : Set γ
hs : MeasurableSet s
ms : ((η ∘ₖ κ) a) s < ⊤
⊢ ∀ᵐ (x : β) ∂κ a, (η x) s < ⊤

Tactic:
exact ae_lt_top_of_comp_ne_top a ms.ne

Result:
no goals

Proof state:
case pos.h_closed
α : Type u_1
β : Type u_2
γ : Type u_3
E : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝¹ : NormedAddCommGroup E
a : α
κ : Kernel α β
η : Kernel β γ
inst✝ : NormedSpace ℝ E
f✝ : γ → E
hE : CompleteSpace E
⊢ IsClosed {f | ∫ (z : γ), ↑↑f z ∂(η ∘ₖ κ) a = ∫ (x : β), ∫ (y : γ), ↑↑f y ∂η x ∂κ a}

Tactic:
exact isClosed_eq continuous_integral Kernel.continuous_integral_integral_comp

Result:
no goals
-- Mathlib/Topology/Homeomorph.lean
theorem continuous_symm_of_equiv_compact_to_t2 [CompactSpace X] [T2Space Y] {f : X ≃ Y}
    (hf : Continuous f) : Continuous f.symm

Proof state:
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : CompactSpace X
inst✝ : T2Space Y
f : X ≃ Y
hf : Continuous ⇑f
⊢ Continuous ⇑f.symm

Tactic:
rw [continuous_iff_isClosed]

Result:
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : CompactSpace X
inst✝ : T2Space Y
f : X ≃ Y
hf : Continuous ⇑f
⊢ ∀ (s : Set X), IsClosed s → IsClosed (⇑f.symm ⁻¹' s)

Proof state:
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : CompactSpace X
inst✝ : T2Space Y
f : X ≃ Y
hf : Continuous ⇑f
C : Set X
hC : IsClosed C
⊢ IsClosed (⇑f.symm ⁻¹' C)

Tactic:
have hC' : IsClosed (f '' C) := (hC.isCompact.image hf).isClosed

Result:
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : CompactSpace X
inst✝ : T2Space Y
f : X ≃ Y
hf : Continuous ⇑f
C : Set X
hC : IsClosed C
hC' : IsClosed (⇑f '' C)
⊢ IsClosed (⇑f.symm ⁻¹' C)

Proof state:
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : CompactSpace X
inst✝ : T2Space Y
f : X ≃ Y
hf : Continuous ⇑f
⊢ ∀ (s : Set X), IsClosed s → IsClosed (⇑f.symm ⁻¹' s)

Tactic:
intro C hC

Result:
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : CompactSpace X
inst✝ : T2Space Y
f : X ≃ Y
hf : Continuous ⇑f
C : Set X
hC : IsClosed C
⊢ IsClosed (⇑f.symm ⁻¹' C)

Proof state:
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : CompactSpace X
inst✝ : T2Space Y
f : X ≃ Y
hf : Continuous ⇑f
C : Set X
hC : IsClosed C
hC' : IsClosed (⇑f '' C)
⊢ IsClosed (⇑f.symm ⁻¹' C)

Tactic:
rwa [Equiv.image_eq_preimage] at hC'

Result:
no goals
-- Mathlib/LinearAlgebra/Dual.lean
theorem linearEquiv_dual_iff_finiteDimensional [Field K] [AddCommGroup V] [Module K V] :
    Nonempty (V ≃ₗ[K] Dual K V) ↔ FiniteDimensional K V

Proof state:
K : Type uK
V : Type uV
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
x✝ : Nonempty (V ≃ₗ[K] Dual K V)
e : V ≃ₗ[K] Dual K V
this : ℵ₀ ≤ Module.rank K V
⊢ False

Tactic:
apply (lift_rank_lt_rank_dual this).ne

Result:
K : Type uK
V : Type uV
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
x✝ : Nonempty (V ≃ₗ[K] Dual K V)
e : V ≃ₗ[K] Dual K V
this : ℵ₀ ≤ Module.rank K V
⊢ lift.{uK, uV} (Module.rank K V) = Module.rank K (V →ₗ[K] K)

Proof state:
K : Type uK
V : Type uV
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
x✝ : Nonempty (V ≃ₗ[K] Dual K V)
e : V ≃ₗ[K] Dual K V
this : ℵ₀ ≤ Module.rank K V
⊢ lift.{uK, uV} (Module.rank K V) = Module.rank K (V →ₗ[K] K)

Tactic:
have := e.lift_rank_eq

Result:
K : Type uK
V : Type uV
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
x✝ : Nonempty (V ≃ₗ[K] Dual K V)
e : V ≃ₗ[K] Dual K V
this✝ : ℵ₀ ≤ Module.rank K V
this : lift.{max uK uV, uV} (Module.rank K V) = lift.{uV, max uK uV} (Module.rank K (Dual K V))
⊢ lift.{uK, uV} (Module.rank K V) = Module.rank K (V →ₗ[K] K)

Proof state:
K : Type uK
V : Type uV
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
⊢ Nonempty (V ≃ₗ[K] Dual K V) ↔ FiniteDimensional K V

Tactic:
refine ⟨fun ⟨e⟩ ↦ ?_, fun h ↦ ⟨(Module.Free.chooseBasis K V).toDualEquiv⟩⟩

Result:
K : Type uK
V : Type uV
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
x✝ : Nonempty (V ≃ₗ[K] Dual K V)
e : V ≃ₗ[K] Dual K V
⊢ FiniteDimensional K V

Proof state:
K : Type uK
V : Type uV
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
x✝ : Nonempty (V ≃ₗ[K] Dual K V)
e : V ≃ₗ[K] Dual K V
⊢ Module.rank K V < ℵ₀

Tactic:
by_contra!

Result:
K : Type uK
V : Type uV
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
x✝ : Nonempty (V ≃ₗ[K] Dual K V)
e : V ≃ₗ[K] Dual K V
this : ℵ₀ ≤ Module.rank K V
⊢ False

Proof state:
K : Type uK
V : Type uV
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
x✝ : Nonempty (V ≃ₗ[K] Dual K V)
e : V ≃ₗ[K] Dual K V
this✝ : ℵ₀ ≤ Module.rank K V
this : lift.{max uK uV, uV} (Module.rank K V) = lift.{uV, max uK uV} (Module.rank K (Dual K V))
⊢ lift.{uK, uV} (Module.rank K V) = Module.rank K (V →ₗ[K] K)

Tactic:
rwa [lift_umax.{uV,uK}, lift_id'.{uV,uK}] at this

Result:
no goals

Proof state:
K : Type uK
V : Type uV
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
x✝ : Nonempty (V ≃ₗ[K] Dual K V)
e : V ≃ₗ[K] Dual K V
⊢ FiniteDimensional K V

Tactic:
rw [FiniteDimensional, ← Module.rank_lt_aleph0_iff]

Result:
K : Type uK
V : Type uV
inst✝² : Field K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
x✝ : Nonempty (V ≃ₗ[K] Dual K V)
e : V ≃ₗ[K] Dual K V
⊢ Module.rank K V < ℵ₀
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem getElem_push (a : Array α) (x : α) (i : Nat) (h : i < (a.push x).size) :
    (a.push x)[i] = if h : i < a.size then a[i] else x

Proof state:
case neg
α : Type u_1
a : Array α
x : α
i : Nat
h✝ : i < (a.push x).size
h' : ¬i < a.size
h : i < a.size + 1
⊢ (a.push x)[i] = if h : i < a.size then a[i] else x

Tactic:
simp [getElem_push_lt, Nat.le_antisymm (Nat.le_of_lt_succ h) (Nat.ge_of_not_lt h')]

Result:
no goals

Proof state:
case pos
α : Type u_1
a : Array α
x : α
i : Nat
h : i < (a.push x).size
h' : i < a.size
⊢ (a.push x)[i] = if h : i < a.size then a[i] else x

Tactic:
simp [getElem_push_lt, h']

Result:
no goals

Proof state:
α : Type u_1
a : Array α
x : α
i : Nat
h : i < (a.push x).size
⊢ (a.push x)[i] = if h : i < a.size then a[i] else x

Tactic:
by_cases h' : i < a.size

Result:
case pos
α : Type u_1
a : Array α
x : α
i : Nat
h : i < (a.push x).size
h' : i < a.size
⊢ (a.push x)[i] = if h : i < a.size then a[i] else x

case neg
α : Type u_1
a : Array α
x : α
i : Nat
h : i < (a.push x).size
h' : ¬i < a.size
⊢ (a.push x)[i] = if h : i < a.size then a[i] else x

Proof state:
case neg
α : Type u_1
a : Array α
x : α
i : Nat
h : i < (a.push x).size
h' : ¬i < a.size
⊢ (a.push x)[i] = if h : i < a.size then a[i] else x

Tactic:
simp at h

Result:
case neg
α : Type u_1
a : Array α
x : α
i : Nat
h✝ : i < (a.push x).size
h' : ¬i < a.size
h : i < a.size + 1
⊢ (a.push x)[i] = if h : i < a.size then a[i] else x
-- Mathlib/Algebra/Polynomial/SumIteratedDerivative.lean
theorem aeval_iterate_derivative_self (p : R[X]) (q : ℕ) (r : A) {p' : A[X]}
    (hp : p.map (algebraMap R A) = (X - C r) ^ q * p') :
    aeval r (derivative^[q] p) = q ! • p'.eval r

Proof state:
R : Type u_1
inst✝² : CommSemiring R
A : Type u_3
inst✝¹ : CommRing A
inst✝ : Algebra R A
p : R[X]
q : ℕ
r : A
p' : A[X]
hp : map (algebraMap R A) p = (X - C r) ^ q * p'
x : ℕ
h : 1 ≤ x
h' : x ≤ q
⊢ 1 ≤ q - (q - x)

Tactic:
rwa [tsub_tsub_cancel_of_le h']

Result:
no goals

Proof state:
R : Type u_1
inst✝² : CommSemiring R
A : Type u_3
inst✝¹ : CommRing A
inst✝ : Algebra R A
p : R[X]
q : ℕ
r : A
p' : A[X]
hp : map (algebraMap R A) p = (X - C r) ^ q * p'
h : ∀ (x : ℕ), 1 ≤ x → x ≤ q → (X - C r) ^ (q - (q - x)) = (X - C r) ^ 1 * (X - C r) ^ (q - (q - x) - 1)
⊢ eval r
      (∑ x ∈ range q.succ, (q.choose x * q.descFactorial (q - x)) • (X - C r) ^ (q - (q - x)) * (⇑derivative)^[x] p') =
    q ! • eval r p'

Tactic:
rw [sum_range_succ', Nat.choose_zero_right, one_mul, tsub_zero, Nat.descFactorial_self, tsub_self,
  pow_zero, smul_mul_assoc, one_mul, Function.iterate_zero_apply, eval_add, eval_smul]

Result:
R : Type u_1
inst✝² : CommSemiring R
A : Type u_3
inst✝¹ : CommRing A
inst✝ : Algebra R A
p : R[X]
q : ℕ
r : A
p' : A[X]
hp : map (algebraMap R A) p = (X - C r) ^ q * p'
h : ∀ (x : ℕ), 1 ≤ x → x ≤ q → (X - C r) ^ (q - (q - x)) = (X - C r) ^ 1 * (X - C r) ^ (q - (q - x) - 1)
⊢ eval r
        (∑ k ∈ range q,
          (q.choose (k + 1) * q.descFactorial (q - (k + 1))) • (X - C r) ^ (q - (q - (k + 1))) *
            (⇑derivative)^[k + 1] p') +
      q ! • eval r p' =
    q ! • eval r p'
-- Mathlib/Topology/Compactness/Compact.lean
theorem isCompact_of_finite_subfamily_closed
    (h : ∀ {ι : Type u} (t : ι → Set X), (∀ i, IsClosed (t i)) → (s ∩ ⋂ i, t i) = ∅ →
      ∃ u : Finset ι, (s ∩ ⋂ i ∈ u, t i) = ∅) :
    IsCompact s :=
  isCompact_of_finite_subcover fun U hUo hsU => by
    rw [← disjoint_compl_right_iff_subset, compl_iUnion, disjoint_iff] at hsU
    rcases h (fun i => (U i)ᶜ) (fun i => (hUo _).isClosed_compl) hsU with ⟨t, ht⟩
    refine ⟨t, ?_⟩
    rwa [← disjoint_compl_right_iff_subset, compl_iUnion₂, disjoint_iff]

Proof state:
X : Type u
inst✝ : TopologicalSpace X
s : Set X
h : ∀ {ι : Type u} (t : ι → Set X), (∀ (i : ι), IsClosed (t i)) → s ∩ ⋂ i, t i = ∅ → ∃ u, s ∩ ⋂ i ∈ u, t i = ∅
ι✝ : Type u
U : ι✝ → Set X
hUo : ∀ (i : ι✝), IsOpen (U i)
hsU : s ⊆ ⋃ i, U i
⊢ ∃ t, s ⊆ ⋃ i ∈ t, U i

Tactic:
rw [← disjoint_compl_right_iff_subset, compl_iUnion, disjoint_iff] at hsU

Result:
X : Type u
inst✝ : TopologicalSpace X
s : Set X
h : ∀ {ι : Type u} (t : ι → Set X), (∀ (i : ι), IsClosed (t i)) → s ∩ ⋂ i, t i = ∅ → ∃ u, s ∩ ⋂ i ∈ u, t i = ∅
ι✝ : Type u
U : ι✝ → Set X
hUo : ∀ (i : ι✝), IsOpen (U i)
hsU : s ⊓ ⋂ i, (U i)ᶜ = ⊥
⊢ ∃ t, s ⊆ ⋃ i ∈ t, U i

Proof state:
X : Type u
inst✝ : TopologicalSpace X
s : Set X
h : ∀ {ι : Type u} (t : ι → Set X), (∀ (i : ι), IsClosed (t i)) → s ∩ ⋂ i, t i = ∅ → ∃ u, s ∩ ⋂ i ∈ u, t i = ∅
ι✝ : Type u
U : ι✝ → Set X
hUo : ∀ (i : ι✝), IsOpen (U i)
hsU : s ⊓ ⋂ i, (U i)ᶜ = ⊥
⊢ ∃ t, s ⊆ ⋃ i ∈ t, U i

Tactic:
rcases h (fun i => (U i)ᶜ) (fun i => (hUo _).isClosed_compl) hsU with ⟨t, ht⟩

Result:
case intro
X : Type u
inst✝ : TopologicalSpace X
s : Set X
h : ∀ {ι : Type u} (t : ι → Set X), (∀ (i : ι), IsClosed (t i)) → s ∩ ⋂ i, t i = ∅ → ∃ u, s ∩ ⋂ i ∈ u, t i = ∅
ι✝ : Type u
U : ι✝ → Set X
hUo : ∀ (i : ι✝), IsOpen (U i)
hsU : s ⊓ ⋂ i, (U i)ᶜ = ⊥
t : Finset ι✝
ht : s ∩ ⋂ i ∈ t, (U i)ᶜ = ∅
⊢ ∃ t, s ⊆ ⋃ i ∈ t, U i

Proof state:
case intro
X : Type u
inst✝ : TopologicalSpace X
s : Set X
h : ∀ {ι : Type u} (t : ι → Set X), (∀ (i : ι), IsClosed (t i)) → s ∩ ⋂ i, t i = ∅ → ∃ u, s ∩ ⋂ i ∈ u, t i = ∅
ι✝ : Type u
U : ι✝ → Set X
hUo : ∀ (i : ι✝), IsOpen (U i)
hsU : s ⊓ ⋂ i, (U i)ᶜ = ⊥
t : Finset ι✝
ht : s ∩ ⋂ i ∈ t, (U i)ᶜ = ∅
⊢ ∃ t, s ⊆ ⋃ i ∈ t, U i

Tactic:
refine ⟨t, ?_⟩

Result:
case intro
X : Type u
inst✝ : TopologicalSpace X
s : Set X
h : ∀ {ι : Type u} (t : ι → Set X), (∀ (i : ι), IsClosed (t i)) → s ∩ ⋂ i, t i = ∅ → ∃ u, s ∩ ⋂ i ∈ u, t i = ∅
ι✝ : Type u
U : ι✝ → Set X
hUo : ∀ (i : ι✝), IsOpen (U i)
hsU : s ⊓ ⋂ i, (U i)ᶜ = ⊥
t : Finset ι✝
ht : s ∩ ⋂ i ∈ t, (U i)ᶜ = ∅
⊢ s ⊆ ⋃ i ∈ t, U i

Proof state:
case intro
X : Type u
inst✝ : TopologicalSpace X
s : Set X
h : ∀ {ι : Type u} (t : ι → Set X), (∀ (i : ι), IsClosed (t i)) → s ∩ ⋂ i, t i = ∅ → ∃ u, s ∩ ⋂ i ∈ u, t i = ∅
ι✝ : Type u
U : ι✝ → Set X
hUo : ∀ (i : ι✝), IsOpen (U i)
hsU : s ⊓ ⋂ i, (U i)ᶜ = ⊥
t : Finset ι✝
ht : s ∩ ⋂ i ∈ t, (U i)ᶜ = ∅
⊢ s ⊆ ⋃ i ∈ t, U i

Tactic:
rwa [← disjoint_compl_right_iff_subset, compl_iUnion₂, disjoint_iff]

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/RBMap/WF.lean
theorem Balanced.del {t : RBNode α} (h : t.Balanced c n) :
    (t.del cut).DelProp t.isBlack n

Proof state:
case black
α : Type u_1
c : RBColor
n✝ : Nat
cut : α → Ordering
t a : RBNode α
c₁✝ : RBColor
n : Nat
b : RBNode α
c₂✝ : RBColor
v✝ : α
ha : a.Balanced c₁✝ n
hb : b.Balanced c₂✝ n
iha : DelProp a.isBlack (del cut a) n
ihb : DelProp b.isBlack (del cut b) n
⊢ RedRed True (del cut (node black a v✝ b)) n

Tactic:
unfold del

Result:
case black
α : Type u_1
c : RBColor
n✝ : Nat
cut : α → Ordering
t a : RBNode α
c₁✝ : RBColor
n : Nat
b : RBNode α
c₂✝ : RBColor
v✝ : α
ha : a.Balanced c₁✝ n
hb : b.Balanced c₂✝ n
iha : DelProp a.isBlack (del cut a) n
ihb : DelProp b.isBlack (del cut b) n
⊢ RedRed True
    (match cut v✝ with
    | Ordering.lt =>
      match a.isBlack with
      | black => (del cut a).balLeft v✝ b
      | red => node red (del cut a) v✝ b
    | Ordering.gt =>
      match b.isBlack with
      | black => a.balRight v✝ (del cut b)
      | red => node red a v✝ (del cut b)
    | Ordering.eq => a.append b)
    n

Proof state:
case nil
α : Type u_1
c : RBColor
n : Nat
cut : α → Ordering
t : RBNode α
⊢ DelProp nil.isBlack (del cut nil) 0

Tactic:
exact ⟨_, .nil⟩

Result:
no goals

Proof state:
case red.h_1
α : Type u_1
c : RBColor
n✝ : Nat
cut : α → Ordering
t a : RBNode α
n : Nat
b : RBNode α
v✝ : α
ha : a.Balanced black n
hb : b.Balanced black n
iha : DelProp a.isBlack (del cut a) n
ihb : DelProp b.isBlack (del cut b) n
x✝ : Ordering
heq✝ : cut v✝ = Ordering.lt
⊢ DelProp (node red a v✝ b).isBlack
    (match a.isBlack with
    | black => (del cut a).balLeft v✝ b
    | red => node red (del cut a) v✝ b)
    n

Tactic:
exact match a, n, iha with
| .nil, _, _ => ⟨_, .red ha hb⟩
| .node black .., _, ⟨n, rfl, ha⟩ => (hb.balLeft ha).of_false nofun

Result:
no goals
-- Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean
theorem eLpNorm_le_of_ae_bound {f : α → F} {C : ℝ} (hfC : ∀ᵐ x ∂μ, ‖f x‖ ≤ C) :
    eLpNorm f p μ ≤ μ Set.univ ^ p.toReal⁻¹ * ENNReal.ofReal C

Proof state:
α : Type u_1
F : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup F
f : α → F
C : ℝ
hfC : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ C
⊢ eLpNorm f p μ ≤ μ Set.univ ^ p.toReal⁻¹ * ENNReal.ofReal C

Tactic:
rw [← mul_comm]

Result:
α : Type u_1
F : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup F
f : α → F
C : ℝ
hfC : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ C
⊢ eLpNorm f p μ ≤ ENNReal.ofReal C * μ Set.univ ^ p.toReal⁻¹

Proof state:
α : Type u_1
F : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup F
f : α → F
C : ℝ
hfC : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ C
⊢ eLpNorm f p μ ≤ ENNReal.ofReal C * μ Set.univ ^ p.toReal⁻¹

Tactic:
exact eLpNorm_le_of_ae_nnnorm_bound (hfC.mono fun x hx => hx.trans C.le_coe_toNNReal)

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Basic.lean
theorem zero_sub (n : Nat) : 0 - n = 0

Proof state:
case succ
n : Nat
ih : 0 - n = 0
⊢ 0 - (n + 1) = 0

Tactic:
simp only [ih, Nat.sub_succ]

Result:
case succ
n : Nat
ih : 0 - n = 0
⊢ pred 0 = 0

Proof state:
case zero

⊢ 0 - 0 = 0

Tactic:
rfl

Result:
no goals

Proof state:
n : Nat
⊢ 0 - n = 0

Tactic:
induction n with
| zero => rfl
| succ n ih => simp only [ih, Nat.sub_succ]; decide

Result:
no goals

Proof state:
case succ
n : Nat
ih : 0 - n = 0
⊢ pred 0 = 0

Tactic:
decide

Result:
no goals
-- Mathlib/Algebra/Polynomial/Roots.lean
theorem roots_monomial (ha : a ≠ 0) (n : ℕ) : (monomial n a).roots = n • ({0} : Multiset R)

Proof state:
R : Type u
a : R
inst✝¹ : CommRing R
inst✝ : IsDomain R
ha : a ≠ 0
n : ℕ
⊢ ((monomial n) a).roots = n • {0}

Tactic:
rw [← C_mul_X_pow_eq_monomial, roots_C_mul_X_pow ha]

Result:
no goals