harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/Calculus/ContDiff/Defs.lean
theorem ContDiff.ftaylorSeries (hf : ContDiff 𝕜 n f) :
    HasFTaylorSeriesUpTo n f (ftaylorSeries 𝕜 f)

Proof state:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
n : WithTop ℕ∞
hf : ContDiffOn 𝕜 n f univ
⊢ HasFTaylorSeriesUpToOn n f (ftaylorSeriesWithin 𝕜 f univ) univ

Tactic:
exact ContDiffOn.ftaylorSeriesWithin hf uniqueDiffOn_univ

Result:
no goals

Proof state:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
n : WithTop ℕ∞
hf : ContDiff 𝕜 n f
⊢ HasFTaylorSeriesUpTo n f (_root_.ftaylorSeries 𝕜 f)

Tactic:
simp only [← contDiffOn_univ, ← hasFTaylorSeriesUpToOn_univ_iff, ← ftaylorSeriesWithin_univ]
  at hf ⊢

Result:
𝕜 : Type u
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
n : WithTop ℕ∞
hf : ContDiffOn 𝕜 n f univ
⊢ HasFTaylorSeriesUpToOn n f (ftaylorSeriesWithin 𝕜 f univ) univ
-- Mathlib/Analysis/RCLike/Basic.lean
theorem nonpos_iff : z ≤ 0 ↔ re z ≤ 0 ∧ im z = 0

Proof state:
K : Type u_1
inst✝ : RCLike K
z : K
⊢ z ≤ 0 ↔ re z ≤ 0 ∧ im z = 0

Tactic:
simpa only [map_zero] using le_iff_re_im (z := z) (w := 0)

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Dirac.lean
theorem sum_smul_dirac [Countable α] [MeasurableSingletonClass α] (μ : Measure α) :
    (sum fun a => μ {a} • dirac a) = μ

Proof state:
α : Type u_1
inst✝² : MeasurableSpace α
inst✝¹ : Countable α
inst✝ : MeasurableSingletonClass α
μ : Measure α
⊢ (sum fun a => μ {a} • dirac a) = μ

Tactic:
simpa using (map_eq_sum μ id measurable_id).symm

Result:
no goals
-- Mathlib/CategoryTheory/Subobject/FactorThru.lean
theorem factorThru_comp_arrow {X Y : C} {P : Subobject Y} (f : X ⟶ P) (h) :
    P.factorThru (f ≫ P.arrow) h = f

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
P : Subobject Y
f : X ⟶ underlying.obj P
h : P.Factors (f ≫ P.arrow)
⊢ P.factorThru (f ≫ P.arrow) h = f

Tactic:
ext

Result:
case h
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
P : Subobject Y
f : X ⟶ underlying.obj P
h : P.Factors (f ≫ P.arrow)
⊢ P.factorThru (f ≫ P.arrow) h ≫ P.arrow = f ≫ P.arrow

Proof state:
case h
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
P : Subobject Y
f : X ⟶ underlying.obj P
h : P.Factors (f ≫ P.arrow)
⊢ P.factorThru (f ≫ P.arrow) h ≫ P.arrow = f ≫ P.arrow

Tactic:
simp

Result:
no goals
-- Mathlib/RingTheory/Polynomial/Hermite/Basic.lean
theorem coeff_hermite_succ_zero (n : ℕ) : coeff (hermite (n + 1)) 0 = -coeff (hermite n) 1

Proof state:
n : ℕ
⊢ (hermite (n + 1)).coeff 0 = -(hermite n).coeff 1

Tactic:
simp [coeff_derivative]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Exp.lean
theorem range_exp : range exp = Set.Ioi 0

Proof state:
⊢ Set.range rexp = Set.Ioi 0

Tactic:
rw [← coe_comp_expOrderIso, range_comp, expOrderIso.range_eq, image_univ, Subtype.range_coe]

Result:
no goals
-- Mathlib/Data/List/TakeDrop.lean
@[simp] lemma take_eq_left_iff {x y : List α} {n : ℕ} :
    (x ++ y).take n = x.take n ↔ y = [] ∨ n ≤ x.length

Proof state:
α : Type u
x y : List α
n : ℕ
⊢ take n (x ++ y) = take n x ↔ y = [] ∨ n ≤ x.length

Tactic:
simp [take_append_eq_append_take, Nat.sub_eq_zero_iff_le, Or.comm]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/Raw.lean
theorem getKey!_val [BEq α] [Hashable α] [Inhabited α] {m : Raw₀ α β} {a : α} :
    m.val.getKey! a = m.getKey! a

Proof state:
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : Inhabited α
m : Raw₀ α β
a : α
⊢ m.val.getKey! a = m.getKey! a

Tactic:
simp [Raw.getKey!, m.2]

Result:
no goals
-- Mathlib/Topology/Maps/Basic.lean
lemma tendsto_nhds_iff {f : ι → Y} {l : Filter ι} {y : Y} (hg : IsInducing g) :
    Tendsto f l (𝓝 y) ↔ Tendsto (g ∘ f) l (𝓝 (g y))

Proof state:
Y : Type u_2
Z : Type u_3
ι : Type u_4
g : Y → Z
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
f : ι → Y
l : Filter ι
y : Y
hg : IsInducing g
⊢ Tendsto f l (𝓝 y) ↔ Tendsto (g ∘ f) l (𝓝 (g y))

Tactic:
rw [hg.nhds_eq_comap, tendsto_comap_iff]

Result:
no goals
-- Mathlib/Algebra/Order/GroupWithZero/Unbundled.lean
lemma pow_right_mono₀ (h : 1 ≤ a) : Monotone (a ^ ·) :=
  monotone_nat_of_le_succ fun n => by
    rw [pow_succ']; exact le_mul_of_one_le_left (pow_nonneg (zero_le_one.trans h) _) h

Proof state:
M₀ : Type u_1
inst✝⁴ : MonoidWithZero M₀
inst✝³ : Preorder M₀
a : M₀
inst✝² : ZeroLEOneClass M₀
inst✝¹ : PosMulMono M₀
inst✝ : MulPosMono M₀
h : 1 ≤ a
n : ℕ
⊢ a ^ n ≤ a * a ^ n

Tactic:
exact le_mul_of_one_le_left (pow_nonneg (zero_le_one.trans h) _) h

Result:
no goals

Proof state:
M₀ : Type u_1
inst✝⁴ : MonoidWithZero M₀
inst✝³ : Preorder M₀
a : M₀
inst✝² : ZeroLEOneClass M₀
inst✝¹ : PosMulMono M₀
inst✝ : MulPosMono M₀
h : 1 ≤ a
n : ℕ
⊢ a ^ n ≤ a ^ (n + 1)

Tactic:
rw [pow_succ']

Result:
M₀ : Type u_1
inst✝⁴ : MonoidWithZero M₀
inst✝³ : Preorder M₀
a : M₀
inst✝² : ZeroLEOneClass M₀
inst✝¹ : PosMulMono M₀
inst✝ : MulPosMono M₀
h : 1 ≤ a
n : ℕ
⊢ a ^ n ≤ a * a ^ n
-- Mathlib/.lake/packages/lean4/src/lean/Init/SimpLemmas.lean
theorem Bool.not_eq_true (b : Bool) : (¬(b = true)) = (b = false)

Proof state:
b : Bool
⊢ (¬b = true) = (b = false)

Tactic:
cases b <;> decide

Result:
no goals
-- Mathlib/Topology/Separation/Regular.lean
theorem Topology.IsInducing.regularSpace [TopologicalSpace Y] {f : Y → X}
    (hf : IsInducing f) : RegularSpace Y :=
  .of_hasBasis
    (fun b => by rw [hf.nhds_eq_comap b]; exact (closed_nhds_basis _).comap _)
    fun b s hs => by exact hs.2.preimage hf.continuous

Proof state:
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : RegularSpace X
inst✝ : TopologicalSpace Y
f : Y → X
hf : IsInducing f
b : Y
⊢ (comap f (𝓝 (f b))).HasBasis (?m.14497 b) (?m.14498 b)

Tactic:
exact (closed_nhds_basis _).comap _

Result:
no goals

Proof state:
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : RegularSpace X
inst✝ : TopologicalSpace Y
f : Y → X
hf : IsInducing f
b : Y
s : Set X
hs : s ∈ 𝓝 (f b) ∧ IsClosed s
⊢ IsClosed (f ⁻¹' id s)

Tactic:
exact hs.2.preimage hf.continuous

Result:
no goals

Proof state:
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : RegularSpace X
inst✝ : TopologicalSpace Y
f : Y → X
hf : IsInducing f
b : Y
⊢ (𝓝 b).HasBasis (?m.14497 b) (?m.14498 b)

Tactic:
rw [hf.nhds_eq_comap b]

Result:
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : RegularSpace X
inst✝ : TopologicalSpace Y
f : Y → X
hf : IsInducing f
b : Y
⊢ (comap f (𝓝 (f b))).HasBasis (?m.14497 b) (?m.14498 b)
-- Mathlib/Algebra/Order/Round.lean
theorem round_one : round (1 : α) = 1

Proof state:
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
⊢ round 1 = 1

Tactic:
simp [round]

Result:
no goals
-- Mathlib/Order/ConditionallyCompleteLattice/Indexed.lean
theorem ciSup_of_empty [IsEmpty ι] (f : ι → α) : ⨆ i, f i = ⊥

Proof state:
α : Type u_1
ι : Sort u_4
inst✝¹ : ConditionallyCompleteLinearOrderBot α
inst✝ : IsEmpty ι
f : ι → α
⊢ ⨆ i, f i = ⊥

Tactic:
rw [iSup_of_empty', csSup_empty]

Result:
no goals
-- Mathlib/Order/Defs/LinearOrder.lean
lemma max_lt (h₁ : a < c) (h₂ : b < c) : max a b < c

Proof state:
α : Type u_1
inst✝ : LinearOrder α
a b c : α
h₁ : a < c
h₂ : b < c
⊢ max a b < c

Tactic:
cases le_total a b <;> simp [max_eq_left, max_eq_right, *]

Result:
no goals
-- Mathlib/ModelTheory/Substructures.lean
theorem range_eq_top {f : M →[L] N} : range f = ⊤ ↔ Function.Surjective f

Proof state:
L : Language
M : Type w
N : Type u_1
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f : M →[L] N
⊢ f.range = ⊤ ↔ Function.Surjective ⇑f

Tactic:
rw [SetLike.ext'_iff, range_coe, coe_top, Set.range_eq_univ]

Result:
no goals
-- Mathlib/NumberTheory/Padics/PadicNumbers.lean
@[simp]
lemma valuation_mul {x y : ℚ_[p]} (hx : x ≠ 0) (hy : y ≠ 0) :
    (x * y).valuation = x.valuation + y.valuation

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℚ_[p]
hx : x ≠ 0
hy : y ≠ 0
h_norm : ‖x * y‖ = ‖x‖ * ‖y‖
hp_ne_one : ↑p ≠ 1
⊢ (x * y).valuation = x.valuation + y.valuation

Tactic:
have hp_pos : (0 : ℝ) < p := mod_cast NeZero.pos _

Result:
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℚ_[p]
hx : x ≠ 0
hy : y ≠ 0
h_norm : ‖x * y‖ = ‖x‖ * ‖y‖
hp_ne_one : ↑p ≠ 1
hp_pos : 0 < ↑p
⊢ (x * y).valuation = x.valuation + y.valuation

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℚ_[p]
hx : x ≠ 0
hy : y ≠ 0
⊢ (x * y).valuation = x.valuation + y.valuation

Tactic:
have h_norm : ‖x * y‖ = ‖x‖ * ‖y‖ := norm_mul x y

Result:
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℚ_[p]
hx : x ≠ 0
hy : y ≠ 0
h_norm : ‖x * y‖ = ‖x‖ * ‖y‖
⊢ (x * y).valuation = x.valuation + y.valuation

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℚ_[p]
hx : x ≠ 0
hy : y ≠ 0
h_norm : ‖x * y‖ = ‖x‖ * ‖y‖
⊢ (x * y).valuation = x.valuation + y.valuation

Tactic:
have hp_ne_one : (p : ℝ) ≠ 1 := mod_cast (Fact.out : p.Prime).ne_one

Result:
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℚ_[p]
hx : x ≠ 0
hy : y ≠ 0
h_norm : ‖x * y‖ = ‖x‖ * ‖y‖
hp_ne_one : ↑p ≠ 1
⊢ (x * y).valuation = x.valuation + y.valuation

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
x y : ℚ_[p]
hx : x ≠ 0
hy : y ≠ 0
h_norm : ‖x * y‖ = ‖x‖ * ‖y‖
hp_ne_one : ↑p ≠ 1
hp_pos : 0 < ↑p
⊢ (x * y).valuation = x.valuation + y.valuation

Tactic:
rwa [norm_eq_zpow_neg_valuation hx, norm_eq_zpow_neg_valuation hy,
  norm_eq_zpow_neg_valuation (mul_ne_zero hx hy), ← zpow_add₀ hp_pos.ne',
  zpow_right_inj₀ hp_pos hp_ne_one, ← neg_add, neg_inj] at h_norm

Result:
no goals
-- Mathlib/Analysis/Complex/Basic.lean
/-- The slit plane includes the open unit ball of radius `1` around `1`. -/
lemma mem_slitPlane_of_norm_lt_one {z : ℂ} (hz : ‖z‖ < 1) : 1 + z ∈ slitPlane :=
  ball_one_subset_slitPlane <| by simpa

Proof state:
z : ℂ
hz : ‖z‖ < 1
⊢ 1 + z ∈ Metric.ball 1 1

Tactic:
simpa

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Sublist.lean
theorem Sublist.filterMap (f : α → Option β) (s : l₁ <+ l₂) :
    filterMap f l₁ <+ filterMap f l₂

Proof state:
α : Type u_1
β : Type u_2
l₁ l₂ : List α
f : α → Option β
s : l₁ <+ l₂
⊢ filterMap f l₁ <+ filterMap f l₂

Tactic:
induction s <;> simp [filterMap_cons] <;> split <;> simp [*, cons, cons₂]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Range.lean
theorem zipIdx_map (l : Array α) (k : Nat) (f : α → β) :
    zipIdx (l.map f) k = (zipIdx l k).map (Prod.map f id)

Proof state:
case mk
α : Type u_1
β : Type u_2
k : Nat
f : α → β
toList✝ : List α
⊢ (map f { toList := toList✝ }).zipIdx k = map (Prod.map f id) ({ toList := toList✝ }.zipIdx k)

Tactic:
simp [List.zipIdx_map]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
l : Array α
k : Nat
f : α → β
⊢ (map f l).zipIdx k = map (Prod.map f id) (l.zipIdx k)

Tactic:
cases l

Result:
case mk
α : Type u_1
β : Type u_2
k : Nat
f : α → β
toList✝ : List α
⊢ (map f { toList := toList✝ }).zipIdx k = map (Prod.map f id) ({ toList := toList✝ }.zipIdx k)
-- Mathlib/Combinatorics/Quiver/Basic.lean
lemma heq_of_homOfEq_ext {X Y X' Y' : V} (hX : X = X') (hY : Y = Y') {f : X ⟶ Y} {f' : X' ⟶ Y'}
    (e : Quiver.homOfEq f hX hY = f') : HEq f f'

Proof state:
V : Type u_1
inst✝ : Quiver V
X Y : V
f f' : X ⟶ Y
e : homOfEq f ⋯ ⋯ = f'
⊢ HEq f f'

Tactic:
rw [Quiver.homOfEq_rfl] at e

Result:
V : Type u_1
inst✝ : Quiver V
X Y : V
f f' : X ⟶ Y
e : f = f'
⊢ HEq f f'

Proof state:
V : Type u_1
inst✝ : Quiver V
X Y X' Y' : V
hX : X = X'
hY : Y = Y'
f : X ⟶ Y
f' : X' ⟶ Y'
e : homOfEq f hX hY = f'
⊢ HEq f f'

Tactic:
subst hX hY

Result:
V : Type u_1
inst✝ : Quiver V
X Y : V
f f' : X ⟶ Y
e : homOfEq f ⋯ ⋯ = f'
⊢ HEq f f'

Proof state:
V : Type u_1
inst✝ : Quiver V
X Y : V
f f' : X ⟶ Y
e : f = f'
⊢ HEq f f'

Tactic:
rw [e]

Result:
no goals
-- Mathlib/Data/Set/Finite/Basic.lean
theorem infinite_union {s t : Set α} : (s ∪ t).Infinite ↔ s.Infinite ∨ t.Infinite

Proof state:
α : Type u
s t : Set α
⊢ (s ∪ t).Infinite ↔ s.Infinite ∨ t.Infinite

Tactic:
simp only [Set.Infinite, finite_union, not_and_or]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Reverse.lean
theorem revAt_zero (N : ℕ) : revAt N 0 = N

Proof state:
N : ℕ
⊢ (revAt N) 0 = N

Tactic:
simp

Result:
no goals
-- Mathlib/Topology/Maps/Basic.lean
lemma of_comp_iff (hg : IsClosedEmbedding g) : IsClosedEmbedding (g ∘ f) ↔ IsClosedEmbedding f

Proof state:
X : Type u_1
Y : Type u_2
Z : Type u_3
f : X → Y
g : Y → Z
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
hg : IsClosedEmbedding g
⊢ IsClosedEmbedding (g ∘ f) ↔ IsClosedEmbedding f

Tactic:
simp_rw [isClosedEmbedding_iff, hg.isEmbedding.of_comp_iff, Set.range_comp,
  ← hg.isClosed_iff_image_isClosed]

Result:
no goals
-- Mathlib/AlgebraicGeometry/ProjectiveSpectrum/Scheme.lean
theorem isPrime_carrier : Ideal.IsPrime (carrier x)

Proof state:
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
f : A
x : ↑(Proj.restrict ⋯).toTopCat
⊢ (carrier x).IsPrime

Tactic:
refine Ideal.IsPrime.comap _ (hK := ?_)

Result:
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
f : A
x : ↑(Proj.restrict ⋯).toTopCat
⊢ (Ideal.map (algebraMap A (Away f)) (↑x).asHomogeneousIdeal.toIdeal).IsPrime

Proof state:
R : Type u_1
A : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
f : A
x : ↑(Proj.restrict ⋯).toTopCat
⊢ (Ideal.map (algebraMap A (Away f)) (↑x).asHomogeneousIdeal.toIdeal).IsPrime

Tactic:
exact IsLocalization.isPrime_of_isPrime_disjoint
  (Submonoid.powers f) _ _ inferInstance
  ((disjoint_powers_iff_not_mem _ (Ideal.IsPrime.isRadical inferInstance)).mpr x.2)

Result:
no goals
-- Mathlib/Data/Multiset/FinsetOps.lean
theorem Subset.ndunion_eq_right {s t : Multiset α} (h : s ⊆ t) : s.ndunion t = t

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
h : s ⊆ t
⊢ s.ndunion t = t

Tactic:
induction s, t using Quot.induction_on₂

Result:
case h
α : Type u_1
inst✝ : DecidableEq α
a✝ b✝ : List α
h : Quot.mk (⇑(isSetoid α)) a✝ ⊆ Quot.mk (⇑(isSetoid α)) b✝
⊢ ndunion (Quot.mk (⇑(isSetoid α)) a✝) (Quot.mk (⇑(isSetoid α)) b✝) = Quot.mk (⇑(isSetoid α)) b✝

Proof state:
case h
α : Type u_1
inst✝ : DecidableEq α
a✝ b✝ : List α
h : Quot.mk (⇑(isSetoid α)) a✝ ⊆ Quot.mk (⇑(isSetoid α)) b✝
⊢ ndunion (Quot.mk (⇑(isSetoid α)) a✝) (Quot.mk (⇑(isSetoid α)) b✝) = Quot.mk (⇑(isSetoid α)) b✝

Tactic:
exact congr_arg ((↑) : List α → Multiset α) <| List.Subset.union_eq_right h

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/Rayleigh.lean
theorem eq_smul_self_of_isLocalExtrOn (hT : IsSelfAdjoint T) {x₀ : E}
    (hextr : IsLocalExtrOn T.reApplyInnerSelf (sphere (0 : E) ‖x₀‖) x₀) :
    T x₀ = (↑(T.rayleighQuotient x₀) : 𝕜) • x₀

Proof state:
𝕜 : Type u_1
inst✝³ : RCLike 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
T : E →L[𝕜] E
hT : IsSelfAdjoint T
x₀ : E
hextr : IsLocalExtrOn T.reApplyInnerSelf (sphere 0 ‖x₀‖) x₀
this : InnerProductSpace ℝ E := InnerProductSpace.rclikeToReal 𝕜 E
hSA : ↑⋯.toSelfAdjoint ∈ selfAdjoint (E →L[ℝ] E) :=
  Subtype.prop (LinearMap.IsSymmetric.restrictScalars (isSymmetric hT)).toSelfAdjoint
⊢ T x₀ = ↑(T.rayleighQuotient x₀) • x₀

Tactic:
exact hSA.eq_smul_self_of_isLocalExtrOn_real hextr

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝³ : RCLike 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
T : E →L[𝕜] E
hT : IsSelfAdjoint T
x₀ : E
hextr : IsLocalExtrOn T.reApplyInnerSelf (sphere 0 ‖x₀‖) x₀
this : InnerProductSpace ℝ E := InnerProductSpace.rclikeToReal 𝕜 E
⊢ T x₀ = ↑(T.rayleighQuotient x₀) • x₀

Tactic:
let hSA := hT.isSymmetric.restrictScalars.toSelfAdjoint.prop

Result:
𝕜 : Type u_1
inst✝³ : RCLike 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
T : E →L[𝕜] E
hT : IsSelfAdjoint T
x₀ : E
hextr : IsLocalExtrOn T.reApplyInnerSelf (sphere 0 ‖x₀‖) x₀
this : InnerProductSpace ℝ E := InnerProductSpace.rclikeToReal 𝕜 E
hSA : ↑⋯.toSelfAdjoint ∈ selfAdjoint (E →L[ℝ] E) :=
  Subtype.prop (LinearMap.IsSymmetric.restrictScalars (isSymmetric hT)).toSelfAdjoint
⊢ T x₀ = ↑(T.rayleighQuotient x₀) • x₀

Proof state:
𝕜 : Type u_1
inst✝³ : RCLike 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
T : E →L[𝕜] E
hT : IsSelfAdjoint T
x₀ : E
hextr : IsLocalExtrOn T.reApplyInnerSelf (sphere 0 ‖x₀‖) x₀
⊢ T x₀ = ↑(T.rayleighQuotient x₀) • x₀

Tactic:
letI := InnerProductSpace.rclikeToReal 𝕜 E

Result:
𝕜 : Type u_1
inst✝³ : RCLike 𝕜
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
T : E →L[𝕜] E
hT : IsSelfAdjoint T
x₀ : E
hextr : IsLocalExtrOn T.reApplyInnerSelf (sphere 0 ‖x₀‖) x₀
this : InnerProductSpace ℝ E := InnerProductSpace.rclikeToReal 𝕜 E
⊢ T x₀ = ↑(T.rayleighQuotient x₀) • x₀
-- Mathlib/Analysis/SpecialFunctions/Pow/Real.lean
theorem rpow_le_one_of_one_le_of_nonpos {x z : ℝ} (hx : 1 ≤ x) (hz : z ≤ 0) : x ^ z ≤ 1

Proof state:
case h.e'_4
x z : ℝ
hx : 1 ≤ x
hz : z ≤ 0
⊢ 1 = x ^ 0

Tactic:
exact (rpow_zero x).symm

Result:
no goals

Proof state:
x z : ℝ
hx : 1 ≤ x
hz : z ≤ 0
⊢ x ^ z ≤ 1

Tactic:
convert rpow_le_rpow_of_exponent_le hx hz

Result:
case h.e'_4
x z : ℝ
hx : 1 ≤ x
hz : z ≤ 0
⊢ 1 = x ^ 0
-- Mathlib/.lake/packages/batteries/Batteries/Data/Array/Monadic.lean
theorem toList_filterM [Monad m] [LawfulMonad m] (a : Array α) (p : α → m Bool) :
    toList <$> a.filterM p = a.toList.filterM p

Proof state:
m : Type → Type u_1
α : Type
inst✝¹ : Monad m
inst✝ : LawfulMonad m
a : Array α
p : α → m Bool
⊢ toList <$> filterM p a = List.filterM p a.toList

Tactic:
rw [List.filterM_toArray]

Result:
m : Type → Type u_1
α : Type
inst✝¹ : Monad m
inst✝ : LawfulMonad m
a : Array α
p : α → m Bool
⊢ toList <$> List.toArray <$> List.filterM p a.toList = List.filterM p a.toList

Proof state:
m : Type → Type u_1
α : Type
inst✝¹ : Monad m
inst✝ : LawfulMonad m
a : Array α
p : α → m Bool
⊢ toList <$> List.toArray <$> List.filterM p a.toList = List.filterM p a.toList

Tactic:
simp only [Functor.map_map, id_map']

Result:
no goals
-- Mathlib/Data/Finset/Image.lean
theorem finsetCongr_trans (e : α ≃ β) (e' : β ≃ γ) :
    e.finsetCongr.trans e'.finsetCongr = (e.trans e').finsetCongr

Proof state:
case H.h
α : Type u_1
β : Type u_2
γ : Type u_3
e : α ≃ β
e' : β ≃ γ
x✝ : Finset α
a✝ : γ
⊢ a✝ ∈ (e.finsetCongr.trans e'.finsetCongr) x✝ ↔ a✝ ∈ (e.trans e').finsetCongr x✝

Tactic:
simp [-Finset.mem_map, -Equiv.trans_toEmbedding]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
e : α ≃ β
e' : β ≃ γ
⊢ e.finsetCongr.trans e'.finsetCongr = (e.trans e').finsetCongr

Tactic:
ext

Result:
case H.h
α : Type u_1
β : Type u_2
γ : Type u_3
e : α ≃ β
e' : β ≃ γ
x✝ : Finset α
a✝ : γ
⊢ a✝ ∈ (e.finsetCongr.trans e'.finsetCongr) x✝ ↔ a✝ ∈ (e.trans e').finsetCongr x✝
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem get?_set_eq (a : Array α) (i : Nat) (v : α) (h : i < a.size) :
    (a.set i v)[i]? = v

Proof state:
α : Type u_1
a : Array α
i : Nat
v : α
h : i < a.size
⊢ (a.set i v h)[i]? = some v

Tactic:
simp [getElem?_pos, h]

Result:
no goals
-- Mathlib/Probability/Distributions/Gaussian.lean
@[simp]
lemma gaussianPDF_zero_var (μ : ℝ) : gaussianPDF μ 0 = 0

Proof state:
μ : ℝ
⊢ gaussianPDF μ 0 = 0

Tactic:
ext

Result:
case h
μ x✝ : ℝ
⊢ gaussianPDF μ 0 x✝ = 0 x✝

Proof state:
case h
μ x✝ : ℝ
⊢ gaussianPDF μ 0 x✝ = 0 x✝

Tactic:
simp [gaussianPDF]

Result:
no goals
-- Mathlib/Analysis/Calculus/FDeriv/Mul.lean
theorem hasFDerivAt_list_prod_attach' {l : List ι} {x : {i // i ∈ l} → 𝔸} :
    HasFDerivAt (𝕜 := 𝕜) (fun x ↦ (l.attach.map x).prod)
      (∑ i : Fin l.length, ((l.attach.take i).map x).prod •
        smulRight (proj l.attach[i.cast List.length_attach.symm])
          ((l.attach.drop (.succ i)).map x).prod) x

Proof state:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
ι : Type u_5
𝔸 : Type u_6
inst✝¹ : NormedRing 𝔸
inst✝ : NormedAlgebra 𝕜 𝔸
l : List ι
x : { i // i ∈ l } → 𝔸
⊢ HasFDerivAt (fun x => (List.map x l.attach).prod)
    (∑ i : Fin l.length,
      (List.map x (List.take (↑i) l.attach)).prod •
        (proj l.attach[Fin.cast ⋯ i]).smulRight (List.map x (List.drop (↑i).succ l.attach)).prod)
    x

Tactic:
exact hasStrictFDerivAt_list_prod_attach'.hasFDerivAt

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
ι : Type u_5
𝔸 : Type u_6
inst✝¹ : NormedRing 𝔸
inst✝ : NormedAlgebra 𝕜 𝔸
l : List ι
x : { i // i ∈ l } → 𝔸
⊢ HasFDerivAt (fun x => (List.map x l.attach).prod)
    (∑ i : Fin l.length,
      (List.map x (List.take (↑i) l.attach)).prod •
        (proj l.attach[Fin.cast ⋯ i]).smulRight (List.map x (List.drop (↑i).succ l.attach)).prod)
    x

Tactic:
classical exact hasStrictFDerivAt_list_prod_attach'.hasFDerivAt

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Attach.lean
theorem mem_pmap_of_mem {p : α → Prop} {f : ∀ a, p a → β} {l H} {a} (h : a ∈ l) :
    f a (H a h) ∈ pmap f l H

Proof state:
α : Type u_1
β : Type u_2
p : α → Prop
f : (a : α) → p a → β
l : List α
H : ∀ (a : α), a ∈ l → p a
a : α
h : a ∈ l
⊢ ∃ a_1 h_1, f a_1 ⋯ = f a ⋯

Tactic:
exact ⟨a, h, rfl⟩

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
p : α → Prop
f : (a : α) → p a → β
l : List α
H : ∀ (a : α), a ∈ l → p a
a : α
h : a ∈ l
⊢ f a ⋯ ∈ pmap f l H

Tactic:
rw [mem_pmap]

Result:
α : Type u_1
β : Type u_2
p : α → Prop
f : (a : α) → p a → β
l : List α
H : ∀ (a : α), a ∈ l → p a
a : α
h : a ∈ l
⊢ ∃ a_1 h_1, f a_1 ⋯ = f a ⋯
-- Mathlib/Data/Set/Finite/Basic.lean
lemma Infinite.exists_not_mem_finite (hs : s.Infinite) (ht : t.Finite) : ∃ a, a ∈ s ∧ a ∉ t

Proof state:
α : Type u
s t : Set α
hs : s.Infinite
ht : t.Finite
⊢ ∃ a ∈ s, a ∉ t

Tactic:
by_contra! h

Result:
α : Type u
s t : Set α
hs : s.Infinite
ht : t.Finite
h : ∀ a ∈ s, a ∈ t
⊢ False

Proof state:
α : Type u
s t : Set α
hs : s.Infinite
ht : t.Finite
h : ∀ a ∈ s, a ∈ t
⊢ False

Tactic:
exact hs <| ht.subset h

Result:
no goals
-- Mathlib/Algebra/Polynomial/Degree/SmallDegree.lean
theorem leadingCoeff_linear (ha : a ≠ 0) : leadingCoeff (C a * X + C b) = a

Proof state:
R : Type u
a b : R
inst✝ : Semiring R
ha : a ≠ 0
⊢ (C a * X + C b).leadingCoeff = a

Tactic:
rw [add_comm, leadingCoeff_add_of_degree_lt (degree_C_lt_degree_C_mul_X ha),
  leadingCoeff_C_mul_X]

Result:
no goals
-- Mathlib/Algebra/MonoidAlgebra/Support.lean
theorem mem_span_support (f : MonoidAlgebra k G) :
    f ∈ Submodule.span k (of k G '' (f.support : Set G))

Proof state:
k : Type u₁
G : Type u₂
inst✝¹ : Semiring k
inst✝ : MulOneClass G
f : MonoidAlgebra k G
⊢ f ∈ Submodule.span k (⇑(of k G) '' ↑f.support)

Tactic:
erw [of, MonoidHom.coe_mk, ← supported_eq_span_single, Finsupp.mem_supported]

Result:
no goals
-- Mathlib/Data/Num/Lemmas.lean
theorem one_sub' (a : PosNum) : sub' 1 a = (pred' a).toZNumNeg

Proof state:
a : PosNum
⊢ sub' 1 a = a.pred'.toZNumNeg

Tactic:
cases a <;> rfl

Result:
no goals
-- Mathlib/Analysis/Complex/UpperHalfPlane/Metric.lean
theorem le_dist_coe (z w : ℍ) : w.im * (1 - Real.exp (-dist z w)) ≤ dist (z : ℂ) w :=
  calc
    w.im * (1 - Real.exp (-dist z w)) =
        dist (z : ℂ) (w.center (dist z w)) - dist (w : ℂ) (w.center (dist z w))

Proof state:
z w : ℍ
⊢ w.im * (1 - (Real.cosh (dist z w) - Real.sinh (dist z w))) =
    w.im * Real.sinh (dist z w) - w.im * (Real.cosh (dist z w) - 1)

Tactic:
ring

Result:
no goals

Proof state:
z w : ℍ
⊢ w.im * (1 - rexp (-dist z w)) = dist ↑z ↑(w.center (dist z w)) - dist ↑w ↑(w.center (dist z w))

Tactic:
rw [dist_center_dist, dist_self_center, ← Real.cosh_sub_sinh]

Result:
z w : ℍ
⊢ w.im * (1 - (Real.cosh (dist z w) - Real.sinh (dist z w))) =
    w.im * Real.sinh (dist z w) - w.im * (Real.cosh (dist z w) - 1)