harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/RingTheory/Ideal/Operations.lean
theorem span_singleton_pow (s : R) (n : ℕ) : span {s} ^ n = (span {s ^ n} : Ideal R)

Proof state:
case succ
R : Type u
inst✝ : CommSemiring R
s : R
n : ℕ
ih : span {s} ^ n = span {s ^ n}
⊢ span {s} ^ (n + 1) = span {s ^ (n + 1)}

Tactic:
simp only [pow_succ, ih, span_singleton_mul_span_singleton]

Result:
no goals

Proof state:
case zero
R : Type u
inst✝ : CommSemiring R
s : R
⊢ span {s} ^ 0 = span {s ^ 0}

Tactic:
simp [Set.singleton_one]

Result:
no goals

Proof state:
R : Type u
inst✝ : CommSemiring R
s : R
n : ℕ
⊢ span {s} ^ n = span {s ^ n}

Tactic:
induction' n with n ih

Result:
case zero
R : Type u
inst✝ : CommSemiring R
s : R
⊢ span {s} ^ 0 = span {s ^ 0}

case succ
R : Type u
inst✝ : CommSemiring R
s : R
n : ℕ
ih : span {s} ^ n = span {s ^ n}
⊢ span {s} ^ (n + 1) = span {s ^ (n + 1)}
-- Mathlib/Data/List/Enum.lean
theorem exists_mem_zipIdx' {l : List α} {p : α × ℕ → Prop} :
    (∃ x ∈ l.zipIdx, p x) ↔ ∃ (i : ℕ) (_ : i < length l), p (l[i], i) :=
  exists_mem_zipIdx.trans <| by simp

Proof state:
α : Type u_1
l : List α
p : α × ℕ → Prop
⊢ (∃ i x, p (l[i], 0 + i)) ↔ ∃ i x, p (l[i], i)

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Order/AddGroupWithTop.lean
@[simp] lemma neg_eq_top {a : α} : -a = ⊤ ↔ a = ⊤ where
  mp h

Proof state:
α : Type u_1
inst✝ : LinearOrderedAddCommGroupWithTop α
a : α
h : -a = ⊤
nh : a + -a = 0
⊢ False

Tactic:
rw [h, add_top] at nh

Result:
α : Type u_1
inst✝ : LinearOrderedAddCommGroupWithTop α
a : α
h : -a = ⊤
nh : ⊤ = 0
⊢ False

Proof state:
α : Type u_1
inst✝ : LinearOrderedAddCommGroupWithTop α
a : α
h : -a = ⊤
nh : ¬a = ⊤
⊢ False

Tactic:
replace nh := add_neg_cancel_of_ne_top nh

Result:
α : Type u_1
inst✝ : LinearOrderedAddCommGroupWithTop α
a : α
h : -a = ⊤
nh : a + -a = 0
⊢ False

Proof state:
α : Type u_1
inst✝ : LinearOrderedAddCommGroupWithTop α
a : α
h : a = ⊤
⊢ -a = ⊤

Tactic:
simp [h]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : LinearOrderedAddCommGroupWithTop α
a : α
h : -a = ⊤
⊢ a = ⊤

Tactic:
by_contra nh

Result:
α : Type u_1
inst✝ : LinearOrderedAddCommGroupWithTop α
a : α
h : -a = ⊤
nh : ¬a = ⊤
⊢ False

Proof state:
α : Type u_1
inst✝ : LinearOrderedAddCommGroupWithTop α
a : α
h : -a = ⊤
nh : ⊤ = 0
⊢ False

Tactic:
exact top_ne_zero nh

Result:
no goals
-- Mathlib/Algebra/Group/Pointwise/Set/Basic.lean
@[to_additive]
lemma mul_subset_range {s t : Set β} (hs : s ⊆ range m) (ht : t ⊆ range m) : s * t ⊆ range m

Proof state:
F : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : Mul α
inst✝² : Mul β
inst✝¹ : FunLike F α β
inst✝ : MulHomClass F α β
m : F
s t : Set β
hs : s ⊆ range ⇑m
ht : t ⊆ range ⇑m
⊢ s * t ⊆ range ⇑m

Tactic:
rintro _ ⟨a, ha, b, hb, rfl⟩

Result:
case intro.intro.intro.intro
F : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : Mul α
inst✝² : Mul β
inst✝¹ : FunLike F α β
inst✝ : MulHomClass F α β
m : F
s t : Set β
hs : s ⊆ range ⇑m
ht : t ⊆ range ⇑m
a : β
ha : a ∈ s
b : β
hb : b ∈ t
⊢ (fun x1 x2 => x1 * x2) a b ∈ range ⇑m

Proof state:
case intro.intro.intro.intro.intro.intro
F : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : Mul α
inst✝² : Mul β
inst✝¹ : FunLike F α β
inst✝ : MulHomClass F α β
m : F
s t : Set β
hs : s ⊆ range ⇑m
ht : t ⊆ range ⇑m
a : α
ha : m a ∈ s
b : α
hb : m b ∈ t
⊢ (fun x1 x2 => x1 * x2) (m a) (m b) ∈ range ⇑m

Tactic:
exact ⟨a * b, map_mul ..⟩

Result:
no goals

Proof state:
case intro.intro.intro.intro.intro
F : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : Mul α
inst✝² : Mul β
inst✝¹ : FunLike F α β
inst✝ : MulHomClass F α β
m : F
s t : Set β
hs : s ⊆ range ⇑m
ht : t ⊆ range ⇑m
b : β
hb : b ∈ t
a : α
ha : m a ∈ s
⊢ (fun x1 x2 => x1 * x2) (m a) b ∈ range ⇑m

Tactic:
obtain ⟨b, rfl⟩ := ht hb

Result:
case intro.intro.intro.intro.intro.intro
F : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : Mul α
inst✝² : Mul β
inst✝¹ : FunLike F α β
inst✝ : MulHomClass F α β
m : F
s t : Set β
hs : s ⊆ range ⇑m
ht : t ⊆ range ⇑m
a : α
ha : m a ∈ s
b : α
hb : m b ∈ t
⊢ (fun x1 x2 => x1 * x2) (m a) (m b) ∈ range ⇑m

Proof state:
case intro.intro.intro.intro
F : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : Mul α
inst✝² : Mul β
inst✝¹ : FunLike F α β
inst✝ : MulHomClass F α β
m : F
s t : Set β
hs : s ⊆ range ⇑m
ht : t ⊆ range ⇑m
a : β
ha : a ∈ s
b : β
hb : b ∈ t
⊢ (fun x1 x2 => x1 * x2) a b ∈ range ⇑m

Tactic:
obtain ⟨a, rfl⟩ := hs ha

Result:
case intro.intro.intro.intro.intro
F : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : Mul α
inst✝² : Mul β
inst✝¹ : FunLike F α β
inst✝ : MulHomClass F α β
m : F
s t : Set β
hs : s ⊆ range ⇑m
ht : t ⊆ range ⇑m
b : β
hb : b ∈ t
a : α
ha : m a ∈ s
⊢ (fun x1 x2 => x1 * x2) (m a) b ∈ range ⇑m
-- Mathlib/Analysis/InnerProductSpace/Basic.lean
theorem dist_div_norm_sq_smul {x y : F} (hx : x ≠ 0) (hy : y ≠ 0) (R : ℝ) :
    dist ((R / ‖x‖) ^ 2 • x) ((R / ‖y‖) ^ 2 • y) = R ^ 2 / (‖x‖ * ‖y‖) * dist x y :=
  calc
    dist ((R / ‖x‖) ^ 2 • x) ((R / ‖y‖) ^ 2 • y) =
        √(‖(R / ‖x‖) ^ 2 • x - (R / ‖y‖) ^ 2 • y‖ ^ 2)

Proof state:
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
x y : F
hx : x ≠ 0
hy : y ≠ 0
R : ℝ
⊢ ((R * R * ‖x‖ * (R * R * ‖x‖) * (‖y‖ * ‖y‖ * (‖x‖ * ‖x‖)) -
            ‖x‖ * ‖x‖ * (‖x‖ * ‖x‖) * (2 * (R * R * (R * R * ⟪x, y⟫_ℝ)))) *
          (‖y‖ * ‖y‖ * (‖y‖ * ‖y‖)) +
        R * R * ‖y‖ * (R * R * ‖y‖) * (‖x‖ * ‖x‖ * (‖x‖ * ‖x‖) * (‖y‖ * ‖y‖ * (‖x‖ * ‖x‖)))) *
      (‖x‖ * ‖y‖ * (‖x‖ * ‖y‖)) =
    R * R * (R * R) * (‖x‖ * ‖x‖ - 2 * ⟪x, y⟫_ℝ + ‖y‖ * ‖y‖) *
      (‖x‖ * ‖x‖ * (‖x‖ * ‖x‖) * (‖y‖ * ‖y‖ * (‖x‖ * ‖x‖)) * (‖y‖ * ‖y‖ * (‖y‖ * ‖y‖)))

Tactic:
ring

Result:
no goals

Proof state:
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
x y : F
hx : x ≠ 0
hy : y ≠ 0
R : ℝ
⊢ dist ((R / ‖x‖) ^ 2 • x) ((R / ‖y‖) ^ 2 • y) = √(‖(R / ‖x‖) ^ 2 • x - (R / ‖y‖) ^ 2 • y‖ ^ 2)

Tactic:
rw [dist_eq_norm, sqrt_sq (norm_nonneg _)]

Result:
no goals

Proof state:
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
x y : F
hx : x ≠ 0
hy : y ≠ 0
R : ℝ
⊢ ‖(R / ‖x‖) ^ 2 • x - (R / ‖y‖) ^ 2 • y‖ ^ 2 = (R ^ 2 / (‖x‖ * ‖y‖)) ^ 2 * ‖x - y‖ ^ 2

Tactic:
field_simp [sq, norm_sub_mul_self_real, norm_smul, real_inner_smul_left, inner_smul_right,
  Real.norm_of_nonneg (mul_self_nonneg _)]

Result:
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
x y : F
hx : x ≠ 0
hy : y ≠ 0
R : ℝ
⊢ ((R * R * ‖x‖ * (R * R * ‖x‖) * (‖y‖ * ‖y‖ * (‖x‖ * ‖x‖)) -
            ‖x‖ * ‖x‖ * (‖x‖ * ‖x‖) * (2 * (R * R * (R * R * ⟪x, y⟫_ℝ)))) *
          (‖y‖ * ‖y‖ * (‖y‖ * ‖y‖)) +
        R * R * ‖y‖ * (R * R * ‖y‖) * (‖x‖ * ‖x‖ * (‖x‖ * ‖x‖) * (‖y‖ * ‖y‖ * (‖x‖ * ‖x‖)))) *
      (‖x‖ * ‖y‖ * (‖x‖ * ‖y‖)) =
    R * R * (R * R) * (‖x‖ * ‖x‖ - 2 * ⟪x, y⟫_ℝ + ‖y‖ * ‖y‖) *
      (‖x‖ * ‖x‖ * (‖x‖ * ‖x‖) * (‖y‖ * ‖y‖ * (‖x‖ * ‖x‖)) * (‖y‖ * ‖y‖ * (‖y‖ * ‖y‖)))

Proof state:
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace ℝ F
x y : F
hx : x ≠ 0
hy : y ≠ 0
R : ℝ
⊢ √((R ^ 2 / (‖x‖ * ‖y‖)) ^ 2 * ‖x - y‖ ^ 2) = R ^ 2 / (‖x‖ * ‖y‖) * dist x y

Tactic:
rw [sqrt_mul, sqrt_sq, sqrt_sq, dist_eq_norm] <;> positivity

Result:
no goals
-- Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Order.lean
lemma nnnorm_mem_spectrum_of_nonneg [Nontrivial A] {a : A} (ha : 0 ≤ a

Proof state:
case h.e'_5
A : Type u_1
inst✝³ : CStarAlgebra A
inst✝² : PartialOrder A
inst✝¹ : StarOrderedRing A
inst✝ : Nontrivial A
a : A
ha : autoParam (0 ≤ a) _auto✝
this : IsSelfAdjoint a
⊢ ‖a‖₊ = (spectralRadius ℝ a).toNNReal

Tactic:
simp [this.spectrumRestricts.spectralRadius_eq, this.spectralRadius_eq_nnnorm]

Result:
no goals

Proof state:
A : Type u_1
inst✝³ : CStarAlgebra A
inst✝² : PartialOrder A
inst✝¹ : StarOrderedRing A
inst✝ : Nontrivial A
a : A
ha : autoParam (0 ≤ a) _auto✝
this : IsSelfAdjoint a
⊢ ‖a‖₊ ∈ spectrum ℝ≥0 a

Tactic:
convert NNReal.spectralRadius_mem_spectrum (a := a) ?_ (.nnreal_of_nonneg ha)

Result:
case h.e'_5
A : Type u_1
inst✝³ : CStarAlgebra A
inst✝² : PartialOrder A
inst✝¹ : StarOrderedRing A
inst✝ : Nontrivial A
a : A
ha : autoParam (0 ≤ a) _auto✝
this : IsSelfAdjoint a
⊢ ‖a‖₊ = (spectralRadius ℝ a).toNNReal

A : Type u_1
inst✝³ : CStarAlgebra A
inst✝² : PartialOrder A
inst✝¹ : StarOrderedRing A
inst✝ : Nontrivial A
a : A
ha : autoParam (0 ≤ a) _auto✝
this : IsSelfAdjoint a
⊢ (spectrum ℝ a).Nonempty

Proof state:
A : Type u_1
inst✝³ : CStarAlgebra A
inst✝² : PartialOrder A
inst✝¹ : StarOrderedRing A
inst✝ : Nontrivial A
a : A
ha : autoParam (0 ≤ a) _auto✝
⊢ ‖a‖₊ ∈ spectrum ℝ≥0 a

Tactic:
have : IsSelfAdjoint a := .of_nonneg ha

Result:
A : Type u_1
inst✝³ : CStarAlgebra A
inst✝² : PartialOrder A
inst✝¹ : StarOrderedRing A
inst✝ : Nontrivial A
a : A
ha : autoParam (0 ≤ a) _auto✝
this : IsSelfAdjoint a
⊢ ‖a‖₊ ∈ spectrum ℝ≥0 a

Proof state:
A : Type u_1
inst✝³ : CStarAlgebra A
inst✝² : PartialOrder A
inst✝¹ : StarOrderedRing A
inst✝ : Nontrivial A
a : A
ha : autoParam (0 ≤ a) _auto✝
this : IsSelfAdjoint a
⊢ (spectrum ℝ a).Nonempty

Tactic:
exact this.spectrumRestricts.image ▸ (spectrum.nonempty a).image _

Result:
no goals
-- Mathlib/RingTheory/Jacobson/Ring.lean
/--
If `f : R →+* S` is a ring homomorphism from a jacobson ring to a field,
then it is finite if and only if it is finite type.
-/
lemma RingHom.finite_iff_finiteType_of_isJacobsonRing
    {R S : Type*} [CommRing R] [IsJacobsonRing R] [Field S]
    {f : R →+* S} : f.Finite ↔ f.FiniteType :=
  ⟨RingHom.FiniteType.of_finite,
    by intro; algebraize [f]; exact finite_of_finite_type_of_isJacobsonRing R S⟩

Proof state:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : IsJacobsonRing R
inst✝ : Field S
f : R →+* S
⊢ f.FiniteType → f.Finite

Tactic:
intro

Result:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : IsJacobsonRing R
inst✝ : Field S
f : R →+* S
a✝ : f.FiniteType
⊢ f.Finite

Proof state:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : IsJacobsonRing R
inst✝ : Field S
f : R →+* S
a✝ : f.FiniteType
algInst✝ : Algebra R S := f.toAlgebra
algebraizeInst✝ : Algebra.FiniteType R S
⊢ f.Finite

Tactic:
exact finite_of_finite_type_of_isJacobsonRing R S

Result:
no goals

Proof state:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : IsJacobsonRing R
inst✝ : Field S
f : R →+* S
a✝ : f.FiniteType
⊢ f.Finite

Tactic:
algebraize [f]

Result:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : IsJacobsonRing R
inst✝ : Field S
f : R →+* S
a✝ : f.FiniteType
algInst✝ : Algebra R S := f.toAlgebra
algebraizeInst✝ : Algebra.FiniteType R S
⊢ f.Finite
-- Mathlib/Analysis/Analytic/Constructions.lean
lemma AnalyticAt.restrictScalars (hf : AnalyticAt 𝕜' f x) :
    AnalyticAt 𝕜 f x

Proof state:
𝕜 : Type u_2
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace 𝕜 F
𝕜' : Type u_9
inst✝⁵ : NontriviallyNormedField 𝕜'
inst✝⁴ : NormedAlgebra 𝕜 𝕜'
inst✝³ : NormedSpace 𝕜' E
inst✝² : IsScalarTower 𝕜 𝕜' E
inst✝¹ : NormedSpace 𝕜' F
inst✝ : IsScalarTower 𝕜 𝕜' F
f : E → F
x : E
hf : AnalyticAt 𝕜' f x
⊢ AnalyticAt 𝕜 f x

Tactic:
rcases hf with ⟨p, hp⟩

Result:
case intro
𝕜 : Type u_2
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace 𝕜 F
𝕜' : Type u_9
inst✝⁵ : NontriviallyNormedField 𝕜'
inst✝⁴ : NormedAlgebra 𝕜 𝕜'
inst✝³ : NormedSpace 𝕜' E
inst✝² : IsScalarTower 𝕜 𝕜' E
inst✝¹ : NormedSpace 𝕜' F
inst✝ : IsScalarTower 𝕜 𝕜' F
f : E → F
x : E
p : FormalMultilinearSeries 𝕜' E F
hp : HasFPowerSeriesAt f p x
⊢ AnalyticAt 𝕜 f x

Proof state:
case intro
𝕜 : Type u_2
inst✝¹⁰ : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace 𝕜 E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace 𝕜 F
𝕜' : Type u_9
inst✝⁵ : NontriviallyNormedField 𝕜'
inst✝⁴ : NormedAlgebra 𝕜 𝕜'
inst✝³ : NormedSpace 𝕜' E
inst✝² : IsScalarTower 𝕜 𝕜' E
inst✝¹ : NormedSpace 𝕜' F
inst✝ : IsScalarTower 𝕜 𝕜' F
f : E → F
x : E
p : FormalMultilinearSeries 𝕜' E F
hp : HasFPowerSeriesAt f p x
⊢ AnalyticAt 𝕜 f x

Tactic:
exact ⟨p.restrictScalars 𝕜, hp.restrictScalars⟩

Result:
no goals
-- Mathlib/RingTheory/Polynomial/Nilpotent.lean
@[simp] lemma isNilpotent_reflect_iff {P : R[X]} {N : ℕ} (hN : P.natDegree ≤ N) :
    IsNilpotent (reflect N P) ↔ IsNilpotent P

Proof state:
case refine_2.inr
R : Type u_1
inst✝ : CommRing R
P : R[X]
N : ℕ
hN : P.natDegree ≤ N
h : ∀ (i : ℕ), IsNilpotent (P.coeff i)
i : ℕ
hi : N < i
⊢ IsNilpotent ((reflect N P).coeff i)

Tactic:
simpa [revAt_eq_self_of_lt hi] using h i

Result:
no goals

Proof state:
case refine_1.inl
R : Type u_1
inst✝ : CommRing R
P : R[X]
N : ℕ
hN : P.natDegree ≤ N
h : ∀ (i : ℕ), IsNilpotent ((reflect N P).coeff i)
i : ℕ
hi : i ≤ N
⊢ IsNilpotent (P.coeff i)

Tactic:
simpa [tsub_tsub_cancel_of_le hi] using h (N - i)

Result:
no goals

Proof state:
R : Type u_1
inst✝ : CommRing R
P : R[X]
N : ℕ
hN : P.natDegree ≤ N
⊢ (∀ (i : ℕ), IsNilpotent ((reflect N P).coeff i)) ↔ ∀ (i : ℕ), IsNilpotent (P.coeff i)

Tactic:
refine ⟨fun h i ↦ ?_, fun h i ↦ ?_⟩ <;> rcases le_or_lt i N with hi | hi

Result:
case refine_1.inl
R : Type u_1
inst✝ : CommRing R
P : R[X]
N : ℕ
hN : P.natDegree ≤ N
h : ∀ (i : ℕ), IsNilpotent ((reflect N P).coeff i)
i : ℕ
hi : i ≤ N
⊢ IsNilpotent (P.coeff i)

case refine_1.inr
R : Type u_1
inst✝ : CommRing R
P : R[X]
N : ℕ
hN : P.natDegree ≤ N
h : ∀ (i : ℕ), IsNilpotent ((reflect N P).coeff i)
i : ℕ
hi : N < i
⊢ IsNilpotent (P.coeff i)

case refine_2.inl
R : Type u_1
inst✝ : CommRing R
P : R[X]
N : ℕ
hN : P.natDegree ≤ N
h : ∀ (i : ℕ), IsNilpotent (P.coeff i)
i : ℕ
hi : i ≤ N
⊢ IsNilpotent ((reflect N P).coeff i)

case refine_2.inr
R : Type u_1
inst✝ : CommRing R
P : R[X]
N : ℕ
hN : P.natDegree ≤ N
h : ∀ (i : ℕ), IsNilpotent (P.coeff i)
i : ℕ
hi : N < i
⊢ IsNilpotent ((reflect N P).coeff i)

Proof state:
case refine_1.inr
R : Type u_1
inst✝ : CommRing R
P : R[X]
N : ℕ
hN : P.natDegree ≤ N
h : ∀ (i : ℕ), IsNilpotent ((reflect N P).coeff i)
i : ℕ
hi : N < i
⊢ IsNilpotent (P.coeff i)

Tactic:
simp [coeff_eq_zero_of_natDegree_lt <| lt_of_le_of_lt hN hi]

Result:
no goals

Proof state:
R : Type u_1
inst✝ : CommRing R
P : R[X]
N : ℕ
hN : P.natDegree ≤ N
⊢ IsNilpotent (reflect N P) ↔ IsNilpotent P

Tactic:
simp only [Polynomial.isNilpotent_iff, coeff_reverse]

Result:
R : Type u_1
inst✝ : CommRing R
P : R[X]
N : ℕ
hN : P.natDegree ≤ N
⊢ (∀ (i : ℕ), IsNilpotent ((reflect N P).coeff i)) ↔ ∀ (i : ℕ), IsNilpotent (P.coeff i)

Proof state:
case refine_2.inl
R : Type u_1
inst✝ : CommRing R
P : R[X]
N : ℕ
hN : P.natDegree ≤ N
h : ∀ (i : ℕ), IsNilpotent (P.coeff i)
i : ℕ
hi : i ≤ N
⊢ IsNilpotent ((reflect N P).coeff i)

Tactic:
simpa [hi, revAt_le] using h (N - i)

Result:
no goals
-- Mathlib/Order/Filter/Ultrafilter/Basic.lean
theorem eq_pure_of_finite_mem (h : s.Finite) (h' : s ∈ f) : ∃ x ∈ s, f = pure x

Proof state:
case intro.intro
α : Type u
f : Ultrafilter α
s : Set α
h : s.Finite
h' : ⋃ x ∈ s, {x} ∈ f
a : α
has : a ∈ s
haf : {a} ∈ f
⊢ ∃ x ∈ s, f = pure x

Tactic:
exact ⟨a, has, eq_of_le (Filter.le_pure_iff.2 haf)⟩

Result:
no goals

Proof state:
α : Type u
f : Ultrafilter α
s : Set α
h : s.Finite
h' : s ∈ f
⊢ ∃ x ∈ s, f = pure x

Tactic:
rw [← biUnion_of_singleton s] at h'

Result:
α : Type u
f : Ultrafilter α
s : Set α
h : s.Finite
h' : ⋃ x ∈ s, {x} ∈ f
⊢ ∃ x ∈ s, f = pure x

Proof state:
α : Type u
f : Ultrafilter α
s : Set α
h : s.Finite
h' : ⋃ x ∈ s, {x} ∈ f
⊢ ∃ x ∈ s, f = pure x

Tactic:
rcases (Ultrafilter.finite_biUnion_mem_iff h).mp h' with ⟨a, has, haf⟩

Result:
case intro.intro
α : Type u
f : Ultrafilter α
s : Set α
h : s.Finite
h' : ⋃ x ∈ s, {x} ∈ f
a : α
has : a ∈ s
haf : {a} ∈ f
⊢ ∃ x ∈ s, f = pure x
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/String/Basic.lean
theorem utf8SetAux_of_gt (c' : Char) : ∀ (cs : List Char) {i p : Pos}, i > p → utf8SetAux c' cs i p = cs
  | [],    _, _, _ => rfl
  | c::cs, i, p, h => by
    rw [utf8SetAux, if_neg (mt (congrArg (·.1)) (Ne.symm <| Nat.ne_of_lt h)), utf8SetAux_of_gt c' cs]
    exact Nat.lt_of_lt_of_le h (Nat.le_add_right ..)

Proof state:
c' c : Char
cs : List Char
i p : Pos
h : i > p
⊢ i + c > p

Tactic:
exact Nat.lt_of_lt_of_le h (Nat.le_add_right ..)

Result:
no goals
-- Mathlib/LinearAlgebra/Ray.lean
theorem map_neg (f : M ≃ₗ[R] N) (v : Module.Ray R M) : map f (-v) = -map f v

Proof state:
case h
R : Type u_1
inst✝⁴ : StrictOrderedCommRing R
M : Type u_2
N : Type u_3
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
f : M ≃ₗ[R] N
g : M
hg : g ≠ 0
⊢ (map f) (-rayOfNeZero R g hg) = -(map f) (rayOfNeZero R g hg)

Tactic:
simp

Result:
no goals

Proof state:
R : Type u_1
inst✝⁴ : StrictOrderedCommRing R
M : Type u_2
N : Type u_3
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
f : M ≃ₗ[R] N
v : Ray R M
⊢ (map f) (-v) = -(map f) v

Tactic:
induction v using Module.Ray.ind with | h g hg => simp

Result:
no goals
-- Mathlib/GroupTheory/Sylow.lean
theorem subtype_injective {P Q : Sylow p G} {hP : P ≤ N} {hQ : Q ≤ N}
    (h : P.subtype hP = Q.subtype hQ) : P = Q

Proof state:
p : ℕ
G : Type u_1
inst✝ : Group G
N : Subgroup G
P Q : Sylow p G
hP : ↑P ≤ N
hQ : ↑Q ≤ N
h : ∀ (x : ↥N), x ∈ P.subtype hP ↔ x ∈ Q.subtype hQ
⊢ ∀ (x : G), x ∈ P ↔ x ∈ Q

Tactic:
exact fun g => ⟨fun hg => (h ⟨g, hP hg⟩).mp hg, fun hg => (h ⟨g, hQ hg⟩).mpr hg⟩

Result:
no goals

Proof state:
p : ℕ
G : Type u_1
inst✝ : Group G
N : Subgroup G
P Q : Sylow p G
hP : ↑P ≤ N
hQ : ↑Q ≤ N
h : P.subtype hP = Q.subtype hQ
⊢ P = Q

Tactic:
rw [SetLike.ext_iff] at h ⊢

Result:
p : ℕ
G : Type u_1
inst✝ : Group G
N : Subgroup G
P Q : Sylow p G
hP : ↑P ≤ N
hQ : ↑Q ≤ N
h : ∀ (x : ↥N), x ∈ P.subtype hP ↔ x ∈ Q.subtype hQ
⊢ ∀ (x : G), x ∈ P ↔ x ∈ Q
-- Mathlib/MeasureTheory/Integral/Lebesgue.lean
theorem lintegral_eq_nnreal {m : MeasurableSpace α} (f : α → ℝ≥0∞) (μ : Measure α) :
    ∫⁻ a, f a ∂μ =
      ⨆ (φ : α →ₛ ℝ≥0) (_ : ∀ x, ↑(φ x) ≤ f x), (φ.map ((↑) : ℝ≥0 → ℝ≥0∞)).lintegral μ

Proof state:
case h
α : Type u_1
m : MeasurableSpace α
f : α → ℝ≥0∞
μ : Measure α
φ : α →ₛ ℝ≥0∞
hφ : ⇑φ ≤ fun a => f a
h : ¬∀ᵐ (a : α) ∂μ, φ a ≠ ⊤
h_meas : μ (⇑φ ⁻¹' {⊤}) ≠ 0
b : ℝ≥0∞
hb : b < ⊤
n : ℕ
hn : b < ↑n * μ (⇑φ ⁻¹' {⊤})
⊢ b <
    ⨆ (_ : ∀ (x : α), ↑(((const α ↑n).restrict (⇑φ ⁻¹' {⊤})) x) ≤ f x),
      (SimpleFunc.map ofNNReal ((const α ↑n).restrict (⇑φ ⁻¹' {⊤}))).lintegral μ

Tactic:
simp only [lt_iSup_iff, exists_prop, coe_restrict, φ.measurableSet_preimage, coe_const,
  ENNReal.coe_indicator, map_coe_ennreal_restrict, SimpleFunc.map_const, ENNReal.coe_natCast,
  restrict_const_lintegral]

Result:
case h
α : Type u_1
m : MeasurableSpace α
f : α → ℝ≥0∞
μ : Measure α
φ : α →ₛ ℝ≥0∞
hφ : ⇑φ ≤ fun a => f a
h : ¬∀ᵐ (a : α) ∂μ, φ a ≠ ⊤
h_meas : μ (⇑φ ⁻¹' {⊤}) ≠ 0
b : ℝ≥0∞
hb : b < ⊤
n : ℕ
hn : b < ↑n * μ (⇑φ ⁻¹' {⊤})
⊢ (∀ (x : α), (⇑φ ⁻¹' {⊤}).indicator (fun x => ↑(Function.const α (↑n) x)) x ≤ f x) ∧ b < ↑n * μ (⇑φ ⁻¹' {⊤})

Proof state:
case h
α : Type u_1
m : MeasurableSpace α
f : α → ℝ≥0∞
μ : Measure α
φ : α →ₛ ℝ≥0∞
hφ : ⇑φ ≤ fun a => f a
h : ¬∀ᵐ (a : α) ∂μ, φ a ≠ ⊤
h_meas : μ (⇑φ ⁻¹' {⊤}) ≠ 0
b : ℝ≥0∞
hb : b < ⊤
n : ℕ
hn : b < ↑n * μ (⇑φ ⁻¹' {⊤})
x : α
hx : φ x = ⊤
⊢ ↑(Function.const α (↑n) x) ≤ φ x

Tactic:
simp only [hx, le_top]

Result:
no goals

Proof state:
case pos
α : Type u_1
m : MeasurableSpace α
f : α → ℝ≥0∞
μ : Measure α
φ : α →ₛ ℝ≥0∞
hφ : ⇑φ ≤ fun a => f a
ψ : α →ₛ ℝ≥0 := SimpleFunc.map ENNReal.toNNReal φ
h : ⇑(SimpleFunc.map ofNNReal ψ) =ᶠ[ae μ] ⇑φ
this : ∀ (x : α), ↑(ψ x) ≤ f x
⊢ φ.lintegral μ ≤ ⨆ φ, ⨆ (_ : ∀ (x : α), ↑(φ x) ≤ f x), (SimpleFunc.map ofNNReal φ).lintegral μ

Tactic:
exact le_iSup₂_of_le (φ.map ENNReal.toNNReal) this (ge_of_eq <| lintegral_congr h)

Result:
no goals
-- Mathlib/CategoryTheory/FintypeCat.lean
@[ext]
lemma hom_ext {X Y : FintypeCat} (f g : X ⟶ Y) (h : ∀ x, f x = g x) : f = g

Proof state:
case h
X Y : FintypeCat
f g : X ⟶ Y
h : ∀ (x : X.carrier), f x = g x
x✝ : X.carrier
⊢ f x✝ = g x✝

Tactic:
apply h

Result:
no goals

Proof state:
X Y : FintypeCat
f g : X ⟶ Y
h : ∀ (x : X.carrier), f x = g x
⊢ f = g

Tactic:
funext

Result:
case h
X Y : FintypeCat
f g : X ⟶ Y
h : ∀ (x : X.carrier), f x = g x
x✝ : X.carrier
⊢ f x✝ = g x✝
-- Mathlib/Logic/Encodable/Lattice.lean
theorem iSup_decode₂ [CompleteLattice α] (f : β → α) :
    ⨆ (i : ℕ) (b ∈ decode₂ β i), f b = (⨆ b, f b)

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : Encodable β
inst✝ : CompleteLattice α
f : β → α
⊢ ⨆ j, ⨆ i, ⨆ (_ : j ∈ decode₂ β i), f j = ⨆ b, f b

Tactic:
simp only [mem_decode₂, iSup_iSup_eq_right]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : Encodable β
inst✝ : CompleteLattice α
f : β → α
⊢ ⨆ i, ⨆ b ∈ decode₂ β i, f b = ⨆ b, f b

Tactic:
rw [iSup_comm]

Result:
α : Type u_1
β : Type u_2
inst✝¹ : Encodable β
inst✝ : CompleteLattice α
f : β → α
⊢ ⨆ j, ⨆ i, ⨆ (_ : j ∈ decode₂ β i), f j = ⨆ b, f b
-- Mathlib/Geometry/Manifold/Sheaf/Smooth.lean
@[simp, reassoc, elementwise] lemma smoothSheafCommRing.forgetStalk_hom_comp_evalHom
    (x : TopCat.of M) :
    (smoothSheafCommRing.forgetStalk IM I M R x).hom ≫ (smoothSheaf.evalHom IM I R x) =
      ⇑(smoothSheafCommRing.evalHom _ _ _ _ _)

Proof state:
𝕜 : Type u_1
inst✝¹² : NontriviallyNormedField 𝕜
EM : Type u_2
inst✝¹¹ : NormedAddCommGroup EM
inst✝¹⁰ : NormedSpace 𝕜 EM
HM : Type u_3
inst✝⁹ : TopologicalSpace HM
IM : ModelWithCorners 𝕜 EM HM
E : Type u_4
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
H : Type u_5
inst✝⁶ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u
inst✝⁵ : TopologicalSpace M
inst✝⁴ : ChartedSpace HM M
R : Type u
inst✝³ : TopologicalSpace R
inst✝² : ChartedSpace H R
inst✝¹ : CommRing R
inst✝ : ContMDiffRing I ∞ R
x : ↑(TopCat.of M)
⊢ smoothSheaf.evalHom IM I R x = (forgetStalk IM I M R x).inv ≫ ⇑(ConcreteCategory.hom (evalHom IM I M R x))

Tactic:
rw [← smoothSheafCommRing.forgetStalk_inv_comp_eval]

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝¹² : NontriviallyNormedField 𝕜
EM : Type u_2
inst✝¹¹ : NormedAddCommGroup EM
inst✝¹⁰ : NormedSpace 𝕜 EM
HM : Type u_3
inst✝⁹ : TopologicalSpace HM
IM : ModelWithCorners 𝕜 EM HM
E : Type u_4
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
H : Type u_5
inst✝⁶ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u
inst✝⁵ : TopologicalSpace M
inst✝⁴ : ChartedSpace HM M
R : Type u
inst✝³ : TopologicalSpace R
inst✝² : ChartedSpace H R
inst✝¹ : CommRing R
inst✝ : ContMDiffRing I ∞ R
x : ↑(TopCat.of M)
⊢ (forgetStalk IM I M R x).hom ≫ smoothSheaf.evalHom IM I R x = ⇑(ConcreteCategory.hom (evalHom IM I M R x))

Tactic:
simp_rw [← CategoryTheory.Iso.eq_inv_comp]

Result:
𝕜 : Type u_1
inst✝¹² : NontriviallyNormedField 𝕜
EM : Type u_2
inst✝¹¹ : NormedAddCommGroup EM
inst✝¹⁰ : NormedSpace 𝕜 EM
HM : Type u_3
inst✝⁹ : TopologicalSpace HM
IM : ModelWithCorners 𝕜 EM HM
E : Type u_4
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
H : Type u_5
inst✝⁶ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u
inst✝⁵ : TopologicalSpace M
inst✝⁴ : ChartedSpace HM M
R : Type u
inst✝³ : TopologicalSpace R
inst✝² : ChartedSpace H R
inst✝¹ : CommRing R
inst✝ : ContMDiffRing I ∞ R
x : ↑(TopCat.of M)
⊢ smoothSheaf.evalHom IM I R x = (forgetStalk IM I M R x).inv ≫ ⇑(ConcreteCategory.hom (evalHom IM I M R x))