harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Attach.lean
theorem toArray_unattach {p : α → Prop} {l : Vector { x // p x } n} :
    l.unattach.toArray = l.toArray.unattach

Proof state:
α : Type u_1
n : Nat
p : α → Prop
l : Vector { x // p x } n
⊢ l.unattach.toArray = l.unattach

Tactic:
simp [unattach]

Result:
no goals
-- Mathlib/Order/Filter/Basic.lean
theorem frequently_or_distrib {f : Filter α} {p q : α → Prop} :
    (∃ᶠ x in f, p x ∨ q x) ↔ (∃ᶠ x in f, p x) ∨ ∃ᶠ x in f, q x

Proof state:
α : Type u
f : Filter α
p q : α → Prop
⊢ (∃ᶠ (x : α) in f, p x ∨ q x) ↔ (∃ᶠ (x : α) in f, p x) ∨ ∃ᶠ (x : α) in f, q x

Tactic:
simp only [Filter.Frequently, ← not_and_or, not_or, eventually_and]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem getKey_modifyKey_self [EquivBEq α] [Inhabited α] {k : α} {f : β → β}
    (l : List ((_ : α) × β)) (hl : DistinctKeys l) (h : containsKey k (modifyKey k f l)) :
    getKey k (modifyKey k f l) h = k

Proof state:
α : Type u
β : Type v
inst✝² : BEq α
inst✝¹ : EquivBEq α
inst✝ : Inhabited α
k : α
f : β → β
l : List ((_ : α) × β)
hl : DistinctKeys l
h : containsKey k (modifyKey k f l) = true
⊢ getKey k (modifyKey k f l) h = k

Tactic:
simp [getKey_modifyKey, hl]

Result:
no goals
-- Mathlib/CategoryTheory/Monoidal/Braided/Basic.lean
theorem hexagon_forward_inv (X Y Z : C) :
    (α_ Y Z X).inv ≫ (β_ X (Y ⊗ Z)).inv ≫ (α_ X Y Z).inv =
      Y ◁ (β_ X Z).inv ≫ (α_ Y X Z).inv ≫ (β_ X Y).inv ▷ Z

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X Y Z : C
⊢ (α_ Y Z X).inv ≫ (β_ X (Y ⊗ Z)).inv ≫ (α_ X Y Z).inv = Y ◁ (β_ X Z).inv ≫ (α_ Y X Z).inv ≫ (β_ X Y).inv ▷ Z

Tactic:
simp

Result:
no goals
-- Mathlib/AlgebraicTopology/DoldKan/PInfty.lean
theorem PInfty_idem : (PInfty : K[X] ⟶ _) ≫ PInfty = PInfty

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
⊢ PInfty ≫ PInfty = PInfty

Tactic:
ext n

Result:
case h
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n : ℕ
⊢ (PInfty ≫ PInfty).f n = PInfty.f n

Proof state:
case h
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n : ℕ
⊢ (PInfty ≫ PInfty).f n = PInfty.f n

Tactic:
exact PInfty_f_idem n

Result:
no goals
-- Mathlib/Algebra/Module/LinearMap/End.lean
theorem iterate_succ (n : ℕ) : f' ^ (n + 1) = comp (f' ^ n) f'

Proof state:
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f' : M →ₗ[R] M
n : ℕ
⊢ f' ^ (n + 1) = (f' ^ n) ∘ₗ f'

Tactic:
rw [pow_succ, mul_eq_comp]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/Lemmas.lean
theorem mul_zero (a : Int) : a * 0 = 0

Proof state:
a : Int
⊢ a * 0 = 0

Tactic:
cases a <;> rfl

Result:
no goals
-- Mathlib/Combinatorics/Additive/DoublingConst.lean
lemma cast_addConst (A B : Finset G') : (σ[A, B] : 𝕜) = #(A + B) / #A

Proof state:
G' : Type u_2
inst✝³ : AddGroup G'
inst✝² : DecidableEq G'
𝕜 : Type u_3
inst✝¹ : Semifield 𝕜
inst✝ : CharZero 𝕜
A B : Finset G'
⊢ ↑σ[A, B] = ↑(#(A + B)) / ↑(#A)

Tactic:
simp [addConst]

Result:
no goals
-- Mathlib/CategoryTheory/Simple.lean
theorem id_nonzero (X : C) [Simple.{v} X] : 𝟙 X ≠ 0 :=
  (Simple.mono_isIso_iff_nonzero (𝟙 X)).mp (by infer_instance)

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
X : C
inst✝ : Simple X
⊢ IsIso (𝟙 X)

Tactic:
infer_instance

Result:
no goals
-- Mathlib/Data/String/Lemmas.lean
lemma length_eq_list_length (l : List Char) : (String.mk l).length = l.length

Proof state:
l : List Char
⊢ { data := l }.length = l.length

Tactic:
simp only [String.length]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem leftpad_prefix (n : Nat) (a : α) (l : List α) :
    replicate (n - length l) a <+: leftpad n a l

Proof state:
α : Type u_1
n : Nat
a : α
l : List α
⊢ replicate (n - l.length) a <+: leftpad n a l

Tactic:
simp only [IsPrefix, leftpad]

Result:
α : Type u_1
n : Nat
a : α
l : List α
⊢ ∃ t, replicate (n - l.length) a ++ t = replicate (n - l.length) a ++ l

Proof state:
α : Type u_1
n : Nat
a : α
l : List α
⊢ ∃ t, replicate (n - l.length) a ++ t = replicate (n - l.length) a ++ l

Tactic:
exact Exists.intro l rfl

Result:
no goals
-- Mathlib/Algebra/Homology/HomotopyCategory/HomComplex.lean
@[simp]
lemma comp_assoc_of_third_is_zero_cochain {n₁ n₂ n₁₂ : ℤ}
    (z₁ : Cochain F G n₁) (z₂ : Cochain G K n₂) (z₃ : Cochain K L 0) (h₁₂ : n₁ + n₂ = n₁₂) :
    (z₁.comp z₂ h₁₂).comp z₃ (add_zero n₁₂) = z₁.comp (z₂.comp z₃ (add_zero n₂)) h₁₂ :=
  comp_assoc _ _ _ _ _ (by omega)

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
F G K L : CochainComplex C ℤ
n₁ n₂ n₁₂ : ℤ
z₁ : Cochain F G n₁
z₂ : Cochain G K n₂
z₃ : Cochain K L 0
h₁₂ : n₁ + n₂ = n₁₂
⊢ n₁ + n₂ + 0 = n₁₂

Tactic:
omega

Result:
no goals
-- Mathlib/Data/Set/Finite/Lemmas.lean
theorem exists_min_image [LinearOrder β] (s : Set α) (f : α → β) (h1 : s.Finite) :
    s.Nonempty → ∃ a ∈ s, ∀ b ∈ s, f a ≤ f b
  | ⟨x, hx⟩ => by
    simpa only [exists_prop, Finite.mem_toFinset] using
      h1.toFinset.exists_min_image f ⟨x, h1.mem_toFinset.2 hx⟩

Proof state:
α : Type u
β : Type v
inst✝ : LinearOrder β
s : Set α
f : α → β
h1 : s.Finite
x : α
hx : x ∈ s
⊢ ∃ a ∈ s, ∀ b ∈ s, f a ≤ f b

Tactic:
simpa only [exists_prop, Finite.mem_toFinset] using
  h1.toFinset.exists_min_image f ⟨x, h1.mem_toFinset.2 hx⟩

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/Lemmas.lean
theorem eq_neg_of_eq_neg {a b : Int} (h : a = -b) : b = -a

Proof state:
a b : Int
h : a = -b
⊢ b = -a

Tactic:
rw [h, Int.neg_neg]

Result:
no goals
-- Mathlib/Algebra/Group/Units/Hom.lean
theorem isLocalHom_of_leftInverse [FunLike G S R] [MonoidHomClass G S R]
    {f : F} (g : G) (hfg : Function.LeftInverse g f) : IsLocalHom f where
  map_nonunit a ha

Proof state:
G : Type u_1
R : Type u_2
S : Type u_3
F : Type u_5
inst✝⁵ : Monoid R
inst✝⁴ : Monoid S
inst✝³ : FunLike F R S
inst✝² : MonoidHomClass F R S
inst✝¹ : FunLike G S R
inst✝ : MonoidHomClass G S R
f : F
g : G
hfg : LeftInverse ⇑g ⇑f
a : R
ha : IsUnit (f a)
⊢ IsUnit a

Tactic:
rwa [isUnit_map_of_leftInverse g hfg] at ha

Result:
no goals
-- Mathlib/MeasureTheory/Group/Integral.lean
theorem integral_eq_zero_of_mul_left_eq_neg [IsMulLeftInvariant μ] (hf' : ∀ x, f (g * x) = -f x) :
    ∫ x, f x ∂μ = 0

Proof state:
G : Type u_4
E : Type u_5
inst✝⁵ : MeasurableSpace G
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
μ : Measure G
f : G → E
g : G
inst✝² : Group G
inst✝¹ : MeasurableMul G
inst✝ : μ.IsMulLeftInvariant
hf' : ∀ (x : G), f (g * x) = -f x
⊢ ∫ (x : G), f x ∂μ = 0

Tactic:
simp_rw [← self_eq_neg ℝ E, ← integral_neg, ← hf', integral_mul_left_eq_self]

Result:
no goals
-- Mathlib/Algebra/Quaternion.lean
lemma comm (r : R) (x : ℍ[R, c₁, c₂, c₃]) : r * x = x * r

Proof state:
R : Type u_3
c₁ c₂ c₃ : R
inst✝ : CommRing R
r : R
x : ℍ[R,c₁,c₂,c₃]
⊢ ↑r * x = x * ↑r

Tactic:
ext <;> simp [mul_comm]

Result:
no goals
-- Mathlib/Analysis/Convex/Function.lean
theorem StrictConvexOn.add (hf : StrictConvexOn 𝕜 s f) (hg : StrictConvexOn 𝕜 s g) :
    StrictConvexOn 𝕜 s (f + g) :=
  ⟨hf.1, fun x hx y hy hxy a b ha hb hab =>
    calc
      f (a • x + b • y) + g (a • x + b • y) < a • f x + b • f y + (a • g x + b • g y) :=
        add_lt_add (hf.2 hx hy hxy ha hb hab) (hg.2 hx hy hxy ha hb hab)
      _ = a • (f x + g x) + b • (f y + g y)

Proof state:
𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : OrderedCancelAddCommMonoid β
inst✝¹ : SMul 𝕜 E
inst✝ : DistribMulAction 𝕜 β
s : Set E
f g : E → β
hf : StrictConvexOn 𝕜 s f
hg : StrictConvexOn 𝕜 s g
x : E
hx : x ∈ s
y : E
hy : y ∈ s
hxy : x ≠ y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ a • f x + b • f y + (a • g x + b • g y) = a • (f x + g x) + b • (f y + g y)

Tactic:
rw [smul_add, smul_add, add_add_add_comm]

Result:
no goals
-- Mathlib/Order/LatticeIntervals.lean
protected lemma disjoint_iff [SemilatticeInf α] [OrderBot α] {x y : Iic a} :
    Disjoint x y ↔ Disjoint (x : α) (y : α)

Proof state:
α : Type u_1
a : α
inst✝¹ : SemilatticeInf α
inst✝ : OrderBot α
x y : ↑(Iic a)
⊢ Disjoint x y ↔ Disjoint ↑x ↑y

Tactic:
simp [_root_.disjoint_iff, Subtype.ext_iff]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Zip.lean
theorem zip_map_right (f : β → γ) (l₁ : Vector α n) (l₂ : Vector β n) :
    zip l₁ (l₂.map f) = (zip l₁ l₂).map (Prod.map id f)

Proof state:
β : Type u_1
γ : Type u_2
α : Type u_3
n : Nat
f : β → γ
l₁ : Vector α n
l₂ : Vector β n
⊢ l₁.zip (map f l₂) = map (Prod.map id f) (l₁.zip l₂)

Tactic:
rw [← zip_map, map_id]

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Basic.lean
theorem mk_ord_toType (c : Cardinal) : #c.ord.toType = c

Proof state:
c : Cardinal.{u_1}
⊢ #c.ord.toType = c

Tactic:
simp

Result:
no goals
-- Mathlib/CategoryTheory/Triangulated/HomologicalFunctor.lean
lemma IsHomological.mk' [F.PreservesZeroMorphisms]
    (hF : ∀ (T : Pretriangulated.Triangle C) (hT : T ∈ distTriang C),
      ∃ (T' : Pretriangulated.Triangle C) (e : T ≅ T'),
      ((shortComplexOfDistTriangle T' (isomorphic_distinguished _ hT _ e.symm)).map F).Exact) :
    F.IsHomological where
  exact T hT

Proof state:
case intro.intro
C : Type u_1
A : Type u_3
inst✝⁸ : Category.{u_4, u_1} C
inst✝⁷ : HasShift C ℤ
inst✝⁶ : Category.{u_5, u_3} A
F : C ⥤ A
inst✝⁵ : HasZeroObject C
inst✝⁴ : Preadditive C
inst✝³ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝² : Pretriangulated C
inst✝¹ : Abelian A
inst✝ : F.PreservesZeroMorphisms
hF : ∀ (T : Triangle C) (hT : T ∈ distinguishedTriangles), ∃ T' e, ((shortComplexOfDistTriangle T' ⋯).map F).Exact
T : Triangle C
hT : T ∈ distinguishedTriangles
T' : Triangle C
e : T ≅ T'
h' : ((shortComplexOfDistTriangle T' ⋯).map F).Exact
⊢ ((shortComplexOfDistTriangle T hT).map F).Exact

Tactic:
exact (ShortComplex.exact_iff_of_iso
  (F.mapShortComplex.mapIso ((shortComplexOfDistTriangleIsoOfIso e hT)))).2 h'

Result:
no goals

Proof state:
C : Type u_1
A : Type u_3
inst✝⁸ : Category.{u_4, u_1} C
inst✝⁷ : HasShift C ℤ
inst✝⁶ : Category.{u_5, u_3} A
F : C ⥤ A
inst✝⁵ : HasZeroObject C
inst✝⁴ : Preadditive C
inst✝³ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝² : Pretriangulated C
inst✝¹ : Abelian A
inst✝ : F.PreservesZeroMorphisms
hF : ∀ (T : Triangle C) (hT : T ∈ distinguishedTriangles), ∃ T' e, ((shortComplexOfDistTriangle T' ⋯).map F).Exact
T : Triangle C
hT : T ∈ distinguishedTriangles
⊢ ((shortComplexOfDistTriangle T hT).map F).Exact

Tactic:
obtain ⟨T', e, h'⟩ := hF T hT

Result:
case intro.intro
C : Type u_1
A : Type u_3
inst✝⁸ : Category.{u_4, u_1} C
inst✝⁷ : HasShift C ℤ
inst✝⁶ : Category.{u_5, u_3} A
F : C ⥤ A
inst✝⁵ : HasZeroObject C
inst✝⁴ : Preadditive C
inst✝³ : ∀ (n : ℤ), (shiftFunctor C n).Additive
inst✝² : Pretriangulated C
inst✝¹ : Abelian A
inst✝ : F.PreservesZeroMorphisms
hF : ∀ (T : Triangle C) (hT : T ∈ distinguishedTriangles), ∃ T' e, ((shortComplexOfDistTriangle T' ⋯).map F).Exact
T : Triangle C
hT : T ∈ distinguishedTriangles
T' : Triangle C
e : T ≅ T'
h' : ((shortComplexOfDistTriangle T' ⋯).map F).Exact
⊢ ((shortComplexOfDistTriangle T hT).map F).Exact
-- Mathlib/Topology/Basic.lean
theorem subset_interior_iff_nhds {V : Set X} : s ⊆ interior V ↔ ∀ x ∈ s, V ∈ 𝓝 x

Proof state:
X : Type u
s : Set X
inst✝ : TopologicalSpace X
V : Set X
⊢ s ⊆ interior V ↔ ∀ x ∈ s, V ∈ 𝓝 x

Tactic:
simp_rw [subset_def, mem_interior_iff_mem_nhds]

Result:
no goals
-- Mathlib/RingTheory/PrincipalIdealDomain.lean
theorem eq_bot_iff_generator_eq_zero (S : Submodule R M) [S.IsPrincipal] :
    S = ⊥ ↔ generator S = 0

Proof state:
R : Type u
M : Type v
inst✝³ : AddCommMonoid M
inst✝² : Semiring R
inst✝¹ : Module R M
S : Submodule R M
inst✝ : S.IsPrincipal
⊢ S = ⊥ ↔ generator S = 0

Tactic:
rw [← @span_singleton_eq_bot R M, span_singleton_generator]

Result:
no goals
-- Mathlib/Data/Set/Card.lean
theorem encard_eq_top_iff : s.encard = ⊤ ↔ s.Infinite

Proof state:
α : Type u_1
s : Set α
⊢ s.encard = ⊤ ↔ s.Infinite

Tactic:
rw [← not_iff_not, ← Ne, ← lt_top_iff_ne_top, encard_lt_top_iff, not_infinite]

Result:
no goals
-- Mathlib/Dynamics/Circle/RotationNumber/TranslationNumber.lean
theorem le_translationNumber_of_add_int_le {x : ℝ} {m : ℤ} (h : x + m ≤ f x) : ↑m ≤ τ f :=
  ge_of_tendsto' (f.tendsto_translation_number' x) fun n =>
    (le_div_iff₀ (n.cast_add_one_pos : (0 : ℝ) < _)).mpr <| le_sub_iff_add_le'.2 <| by
      simp only [coe_pow, mul_comm (m : ℝ), ← Nat.cast_add_one, f.le_iterate_of_add_int_le_map h]

Proof state:
f : CircleDeg1Lift
x : ℝ
m : ℤ
h : x + ↑m ≤ f x
n : ℕ
⊢ x + ↑m * (↑n + 1) ≤ (f ^ (n + 1)) x

Tactic:
simp only [coe_pow, mul_comm (m : ℝ), ← Nat.cast_add_one, f.le_iterate_of_add_int_le_map h]

Result:
no goals
-- Mathlib/RingTheory/DedekindDomain/Ideal.lean
theorem mul_inv_cancel_iff {I : FractionalIdeal R₁⁰ K} : I * I⁻¹ = 1 ↔ ∃ J, I * J = 1 :=
  ⟨fun h => ⟨I⁻¹, h⟩, fun ⟨J, hJ⟩ => by rwa [← right_inverse_eq K I J hJ]⟩

Proof state:
K : Type u_3
inst✝⁴ : Field K
R₁ : Type u_4
inst✝³ : CommRing R₁
inst✝² : IsDomain R₁
inst✝¹ : Algebra R₁ K
inst✝ : IsFractionRing R₁ K
I : FractionalIdeal R₁⁰ K
x✝ : ∃ J, I * J = 1
J : FractionalIdeal R₁⁰ K
hJ : I * J = 1
⊢ I * I⁻¹ = 1

Tactic:
rwa [← right_inverse_eq K I J hJ]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Laurent.lean
theorem _root_.Polynomial.toLaurent_C_mul_T (n : ℕ) (r : R) :
    (toLaurent (Polynomial.monomial n r) : R[T;T⁻¹]) = C r * T n :=
  show Finsupp.mapDomain (↑) (monomial n r).toFinsupp = (C r * T n : R[T;T⁻¹]) by
    rw [toFinsupp_monomial, Finsupp.mapDomain_single, single_eq_C_mul_T]

Proof state:
R : Type u_1
inst✝ : Semiring R
n : ℕ
r : R
⊢ Finsupp.mapDomain Nat.cast ((monomial n) r).toFinsupp = C r * T ↑n

Tactic:
rw [toFinsupp_monomial, Finsupp.mapDomain_single, single_eq_C_mul_T]

Result:
no goals
-- Mathlib/Topology/Exterior.lean
@[simp] lemma exterior_exterior (s : Set X) : exterior (exterior s) = exterior s

Proof state:
X : Type u_2
inst✝ : TopologicalSpace X
s : Set X
⊢ exterior (exterior s) = exterior s

Tactic:
simp only [exterior_eq_exterior_iff_nhdsSet, nhdsSet_exterior]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/MapIdx.lean
theorem toList_mapIdx (f : Nat → α → β) (as : Array α) :
    (as.mapIdx f).toList = as.toList.mapIdx (fun i a => f i a)

Proof state:
α : Type u_1
β : Type u_2
f : Nat → α → β
as : Array α
⊢ (mapIdx f as).toList = List.mapIdx (fun i a => f i a) as.toList

Tactic:
apply List.ext_getElem <;> simp

Result:
no goals
-- Mathlib/CategoryTheory/FiberedCategory/Fibered.lean
protected lemma IsPreFibered.exists_isCartesian (p : 𝒳 ⥤ 𝒮) [p.IsPreFibered] {a : 𝒳} {R S : 𝒮}
    (ha : p.obj a = S) (f : R ⟶ S) : ∃ (b : 𝒳) (φ : b ⟶ a), IsCartesian p f φ

Proof state:
𝒮 : Type u₁
𝒳 : Type u₂
inst✝² : Category.{v₁, u₁} 𝒮
inst✝¹ : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
inst✝ : p.IsPreFibered
a : 𝒳
R : 𝒮
f : R ⟶ p.obj a
⊢ ∃ b φ, p.IsCartesian f φ

Tactic:
exact IsPreFibered.exists_isCartesian' f

Result:
no goals

Proof state:
𝒮 : Type u₁
𝒳 : Type u₂
inst✝² : Category.{v₁, u₁} 𝒮
inst✝¹ : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
inst✝ : p.IsPreFibered
a : 𝒳
R S : 𝒮
ha : p.obj a = S
f : R ⟶ S
⊢ ∃ b φ, p.IsCartesian f φ

Tactic:
subst ha

Result:
𝒮 : Type u₁
𝒳 : Type u₂
inst✝² : Category.{v₁, u₁} 𝒮
inst✝¹ : Category.{v₂, u₂} 𝒳
p : 𝒳 ⥤ 𝒮
inst✝ : p.IsPreFibered
a : 𝒳
R : 𝒮
f : R ⟶ p.obj a
⊢ ∃ b φ, p.IsCartesian f φ
-- Mathlib/Analysis/Calculus/FDeriv/Measurable.lean
theorem measurable_deriv_with_param [LocallyCompactSpace 𝕜] [MeasurableSpace 𝕜]
    [OpensMeasurableSpace 𝕜] [MeasurableSpace F]
    [BorelSpace F] {f : α → 𝕜 → F} (hf : Continuous f.uncurry) :
    Measurable (fun (p : α × 𝕜) ↦ deriv (f p.1) p.2)

Proof state:
𝕜 : Type u_1
inst✝¹¹ : NontriviallyNormedField 𝕜
F : Type u_3
inst✝¹⁰ : NormedAddCommGroup F
inst✝⁹ : NormedSpace 𝕜 F
α : Type u_4
inst✝⁸ : TopologicalSpace α
inst✝⁷ : MeasurableSpace α
inst✝⁶ : OpensMeasurableSpace α
inst✝⁵ : CompleteSpace F
inst✝⁴ : LocallyCompactSpace 𝕜
inst✝³ : MeasurableSpace 𝕜
inst✝² : OpensMeasurableSpace 𝕜
inst✝¹ : MeasurableSpace F
inst✝ : BorelSpace F
f : α → 𝕜 → F
hf : Continuous (Function.uncurry f)
⊢ Measurable fun p => deriv (f p.1) p.2

Tactic:
simpa only [fderiv_deriv] using measurable_fderiv_apply_const_with_param 𝕜 hf 1

Result:
no goals
-- Mathlib/Data/List/Intervals.lean
theorem length (n m : ℕ) : length (Ico n m) = m - n

Proof state:
n m : ℕ
⊢ (Ico n m).length = m - n

Tactic:
dsimp [Ico]

Result:
n m : ℕ
⊢ (range' n (m - n)).length = m - n

Proof state:
n m : ℕ
⊢ (range' n (m - n)).length = m - n

Tactic:
simp [length_range']

Result:
no goals
-- Mathlib/LinearAlgebra/Semisimple.lean
@[simp]
lemma isSemisimple_id [IsSemisimpleModule R M] : IsSemisimple (LinearMap.id : Module.End R M)

Proof state:
R : Type u_1
M : Type u_2
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : IsSemisimpleModule R M
⊢ IsSemisimple LinearMap.id

Tactic:
simpa [isSemisimple_iff] using exists_isCompl

Result:
no goals
-- Mathlib/Analysis/Normed/Lp/ProdLp.lean
theorem prod_edist_eq_of_L1 (x y : WithLp 1 (α × β)) :
    edist x y = edist x.fst y.fst + edist x.snd y.snd

Proof state:
α : Type u_2
β : Type u_3
inst✝¹ : SeminormedAddCommGroup α
inst✝ : SeminormedAddCommGroup β
x y : WithLp 1 (α × β)
⊢ edist x y = edist x.1 y.1 + edist x.2 y.2

Tactic:
simp [prod_edist_eq_add]

Result:
no goals
-- Mathlib/RingTheory/Spectrum/Prime/Topology.lean
theorem maximalSpectrumToPiLocalization_surjective_of_discreteTopology :
    Function.Surjective (MaximalSpectrum.toPiLocalization R)

Proof state:
R : Type u
inst✝¹ : CommSemiring R
inst✝ : DiscreteTopology (PrimeSpectrum R)
⊢ Function.Surjective ⇑(MaximalSpectrum.toPiLocalization R)

Tactic:
rw [← piLocalizationToMaximal_comp_toPiLocalization]

Result:
R : Type u
inst✝¹ : CommSemiring R
inst✝ : DiscreteTopology (PrimeSpectrum R)
⊢ Function.Surjective ⇑((piLocalizationToMaximal R).comp (toPiLocalization R))

Proof state:
R : Type u
inst✝¹ : CommSemiring R
inst✝ : DiscreteTopology (PrimeSpectrum R)
⊢ Function.Surjective ⇑((piLocalizationToMaximal R).comp (toPiLocalization R))

Tactic:
exact (piLocalizationToMaximal_surjective R).comp
  (toPiLocalization_surjective_of_discreteTopology R)

Result:
no goals
-- Mathlib/Data/Matroid/Dual.lean
theorem coindep_iff_exists' : M.Coindep X ↔ (∃ B, M.IsBase B ∧ B ⊆ M.E \ X) ∧ X ⊆ M.E

Proof state:
α : Type u_1
M : Matroid α
X : Set α
⊢ M.Coindep X ↔ (∃ B, M.IsBase B ∧ B ⊆ M.E \ X) ∧ X ⊆ M.E

Tactic:
simp_rw [Coindep, dual_indep_iff_exists', and_comm (a := _ ⊆ _), and_congr_left_iff, subset_diff]

Result:
α : Type u_1
M : Matroid α
X : Set α
⊢ X ⊆ M.E → ((∃ B, M.IsBase B ∧ Disjoint X B) ↔ ∃ B, M.IsBase B ∧ B ⊆ M.E ∧ Disjoint B X)

Proof state:
α : Type u_1
M : Matroid α
X : Set α
⊢ X ⊆ M.E → ((∃ B, M.IsBase B ∧ Disjoint X B) ↔ ∃ B, M.IsBase B ∧ B ⊆ M.E ∧ Disjoint B X)

Tactic:
exact fun _ ↦ ⟨fun ⟨B, hB, hXB⟩ ↦ ⟨B, hB, hB.subset_ground, hXB.symm⟩,
  fun ⟨B, hB, _, hBX⟩ ↦ ⟨B, hB, hBX.symm⟩⟩

Result:
no goals
-- Mathlib/Data/Real/EReal.lean
lemma div_mul_cancel (h₁ : b ≠ ⊥) (h₂ : b ≠ ⊤) (h₃ : b ≠ 0) : a / b * b = a

Proof state:
a b : EReal
h₁ : b ≠ ⊥
h₂ : b ≠ ⊤
h₃ : b ≠ 0
⊢ a / b * b = a

Tactic:
rw [mul_comm (a / b) b, ← mul_div_left_comm a b b, div_self h₁ h₂ h₃, mul_one]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Option/Lemmas.lean
theorem not_isSome_iff_eq_none : ¬o.isSome ↔ o = none

Proof state:
α✝ : Type u_1
o : Option α✝
⊢ ¬o.isSome = true ↔ o = none

Tactic:
cases o <;> simp

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Arctan.lean
theorem two_mul_arctan_inv_3_add_arctan_inv_7 : 2 * arctan 3⁻¹ + arctan 7⁻¹ = π / 4

Proof state:
⊢ 2 * arctan 3⁻¹ + arctan 7⁻¹ = π / 4

Tactic:
rw [two_mul_arctan, arctan_add] <;> norm_num

Result:
no goals
-- Mathlib/Tactic/NormNum/Basic.lean
theorem isNat_natAbs_neg : {n : ℤ} → {a : ℕ} → IsInt n (.negOfNat a) → IsNat n.natAbs a
  | _, _, ⟨rfl⟩ => ⟨by simp⟩

Proof state:
a✝ : ℕ
⊢ (↑(Int.negOfNat a✝)).natAbs = ↑a✝

Tactic:
simp

Result:
no goals
-- Mathlib/Data/List/OfFn.lean
theorem ofFn_fin_append {m n} (a : Fin m → α) (b : Fin n → α) :
    List.ofFn (Fin.append a b) = List.ofFn a ++ List.ofFn b

Proof state:
α : Type u
m n : ℕ
a : Fin m → α
b : Fin n → α
⊢ ofFn (Fin.append a b) = ofFn a ++ ofFn b

Tactic:
simp_rw [ofFn_add, Fin.append_left, Fin.append_right]

Result:
no goals
-- Mathlib/RingTheory/MvPowerSeries/Basic.lean
theorem coeff_C_mul (n : σ →₀ ℕ) (φ : MvPowerSeries σ R) (a : R) :
    coeff R n (C σ R a * φ) = a * coeff R n φ

Proof state:
σ : Type u_1
R : Type u_2
inst✝ : Semiring R
n : σ →₀ ℕ
φ : MvPowerSeries σ R
a : R
⊢ (coeff R n) ((C σ R) a * φ) = a * (coeff R n) φ

Tactic:
simpa using coeff_add_monomial_mul 0 n φ a

Result:
no goals
-- Mathlib/NumberTheory/LSeries/Basic.lean
lemma term_nonneg {a : ℕ → ℂ} {n : ℕ} (h : 0 ≤ a n) (x : ℝ) : 0 ≤ term a x n

Proof state:
case pos
a : ℕ → ℂ
n : ℕ
h : 0 ≤ a n
x : ℝ
hn : n = 0
⊢ 0 ≤ 0

case neg
a : ℕ → ℂ
n : ℕ
h : 0 ≤ a n
x : ℝ
hn : ¬n = 0
⊢ 0 ≤ a n / ↑n ^ ↑x

Tactic:
exacts [le_rfl, mul_nonneg h (inv_natCast_cpow_ofReal_pos hn x).le]

Result:
no goals

Proof state:
a : ℕ → ℂ
n : ℕ
h : 0 ≤ a n
x : ℝ
⊢ 0 ≤ term a (↑x) n

Tactic:
rw [term_def]

Result:
a : ℕ → ℂ
n : ℕ
h : 0 ≤ a n
x : ℝ
⊢ 0 ≤ if n = 0 then 0 else a n / ↑n ^ ↑x

Proof state:
a : ℕ → ℂ
n : ℕ
h : 0 ≤ a n
x : ℝ
⊢ 0 ≤ if n = 0 then 0 else a n / ↑n ^ ↑x

Tactic:
split_ifs with hn

Result:
case pos
a : ℕ → ℂ
n : ℕ
h : 0 ≤ a n
x : ℝ
hn : n = 0
⊢ 0 ≤ 0

case neg
a : ℕ → ℂ
n : ℕ
h : 0 ≤ a n
x : ℝ
hn : ¬n = 0
⊢ 0 ≤ a n / ↑n ^ ↑x
-- Mathlib/SetTheory/Ordinal/Arithmetic.lean
theorem mod_one (a : Ordinal) : a % 1 = 0

Proof state:
a : Ordinal.{u_4}
⊢ a % 1 = 0

Tactic:
simp only [mod_def, div_one, one_mul, sub_self]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Degree/Definitions.lean
theorem degree_lt_iff_coeff_zero (f : R[X]) (n : ℕ) :
    degree f < n ↔ ∀ m : ℕ, n ≤ m → coeff f m = 0

Proof state:
R : Type u
inst✝ : Semiring R
f : R[X]
n : ℕ
⊢ f.degree < ↑n ↔ ∀ (m : ℕ), n ≤ m → f.coeff m = 0

Tactic:
simp only [degree, Finset.sup_lt_iff (WithBot.bot_lt_coe n), mem_support_iff,
  WithBot.coe_lt_coe, ← @not_le ℕ, max_eq_sup_coe, Nat.cast_withBot, Ne, not_imp_not]

Result:
no goals
-- Mathlib/Algebra/Group/Hom/Defs.lean
theorem MulHom.cancel_left [Mul M] [Mul N] [Mul P] {g : N →ₙ* P} {f₁ f₂ : M →ₙ* N}
    (hg : Function.Injective g) : g.comp f₁ = g.comp f₂ ↔ f₁ = f₂ :=
  ⟨fun h => MulHom.ext fun x => hg <| by rw [← MulHom.comp_apply, h, MulHom.comp_apply],
    fun h => h ▸ rfl⟩

Proof state:
M : Type u_4
N : Type u_5
P : Type u_6
inst✝² : Mul M
inst✝¹ : Mul N
inst✝ : Mul P
g : N →ₙ* P
f₁ f₂ : M →ₙ* N
hg : Injective ⇑g
h : g.comp f₁ = g.comp f₂
x : M
⊢ g (f₁ x) = g (f₂ x)

Tactic:
rw [← MulHom.comp_apply, h, MulHom.comp_apply]

Result:
no goals
-- Mathlib/Topology/UniformSpace/Defs.lean
theorem isOpen_iff_ball_subset {s : Set α} : IsOpen s ↔ ∀ x ∈ s, ∃ V ∈ 𝓤 α, ball x V ⊆ s

Proof state:
α : Type ua
inst✝ : UniformSpace α
s : Set α
⊢ IsOpen s ↔ ∀ x ∈ s, ∃ V ∈ 𝓤 α, ball x V ⊆ s

Tactic:
simp_rw [isOpen_iff_mem_nhds, nhds_eq_comap_uniformity, mem_comap, ball]

Result:
no goals
-- Mathlib/Analysis/Normed/Algebra/Spectrum.lean
lemma nnreal_iff [Module ℝ A] [IsScalarTower ℝ A A] [SMulCommClass ℝ A A] {a : A} :
    QuasispectrumRestricts a ContinuousMap.realToNNReal ↔ ∀ x ∈ σₙ ℝ a, 0 ≤ x

Proof state:
A : Type u_3
inst✝³ : NonUnitalRing A
inst✝² : Module ℝ A
inst✝¹ : IsScalarTower ℝ A A
inst✝ : SMulCommClass ℝ A A
a : A
⊢ QuasispectrumRestricts a ⇑ContinuousMap.realToNNReal ↔ ∀ x ∈ σₙ ℝ a, 0 ≤ x

Tactic:
rw [quasispectrumRestricts_iff_spectrumRestricts_inr,
  Unitization.quasispectrum_eq_spectrum_inr' _ ℝ, SpectrumRestricts.nnreal_iff]

Result:
no goals