harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/CategoryTheory/Limits/ConcreteCategory/Basic.lean
theorem isColimit_exists_rep {D : Cocone F} (hD : IsColimit D) (x : ToType D.pt) :
    ∃ (j : J) (y : ToType (F.obj j)), D.ι.app j y = x

Proof state:
case intro
C : Type u
inst✝⁴ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type t
inst✝³ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝² : ConcreteCategory C FC
J : Type w
inst✝¹ : Category.{r, w} J
F : J ⥤ C
inst✝ : PreservesColimit F (forget C)
D : Cocone F
hD : IsColimit D
a : (j : J) × ToType (F.obj j)
⊢ ∃ j y, (ConcreteCategory.hom (D.ι.app j)) y = (fun a => (ConcreteCategory.hom (D.ι.app a.fst)) a.snd) a

Tactic:
exact ⟨a.1, a.2, rfl⟩

Result:
no goals

Proof state:
C : Type u
inst✝⁴ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type t
inst✝³ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝² : ConcreteCategory C FC
J : Type w
inst✝¹ : Category.{r, w} J
F : J ⥤ C
inst✝ : PreservesColimit F (forget C)
D : Cocone F
hD : IsColimit D
x : ToType D.pt
⊢ ∃ j y, (ConcreteCategory.hom (D.ι.app j)) y = x

Tactic:
obtain ⟨a, rfl⟩ := Concrete.from_union_surjective_of_isColimit F hD x

Result:
case intro
C : Type u
inst✝⁴ : Category.{v, u} C
FC : C → C → Type u_1
CC : C → Type t
inst✝³ : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)
inst✝² : ConcreteCategory C FC
J : Type w
inst✝¹ : Category.{r, w} J
F : J ⥤ C
inst✝ : PreservesColimit F (forget C)
D : Cocone F
hD : IsColimit D
a : (j : J) × ToType (F.obj j)
⊢ ∃ j y, (ConcreteCategory.hom (D.ι.app j)) y = (fun a => (ConcreteCategory.hom (D.ι.app a.fst)) a.snd) a
-- Mathlib/Logic/Equiv/Basic.lean
theorem swap_eq_refl_iff {x y : α} : swap x y = Equiv.refl _ ↔ x = y

Proof state:
α : Sort u_1
inst✝ : DecidableEq α
x y : α
h : swap x y = Equiv.refl α
⊢ (Equiv.refl α) x = (Equiv.refl α) y

Tactic:
rw [← h, swap_apply_left, h, refl_apply]

Result:
no goals

Proof state:
α : Sort u_1
inst✝ : DecidableEq α
x y : α
⊢ swap x y = Equiv.refl α ↔ x = y

Tactic:
refine ⟨fun h => (Equiv.refl _).injective ?_, fun h => h ▸ swap_self _⟩

Result:
α : Sort u_1
inst✝ : DecidableEq α
x y : α
h : swap x y = Equiv.refl α
⊢ (Equiv.refl α) x = (Equiv.refl α) y
-- Mathlib/Analysis/Calculus/TangentCone.lean
theorem uniqueDiffWithinAt_univ : UniqueDiffWithinAt 𝕜 univ x

Proof state:
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : TopologicalSpace E
x : E
⊢ UniqueDiffWithinAt 𝕜 univ x

Tactic:
rw [uniqueDiffWithinAt_iff, tangentCone_univ]

Result:
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : TopologicalSpace E
x : E
⊢ Dense ↑(Submodule.span 𝕜 univ) ∧ x ∈ closure univ

Proof state:
𝕜 : Type u_1
inst✝³ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : TopologicalSpace E
x : E
⊢ Dense ↑(Submodule.span 𝕜 univ) ∧ x ∈ closure univ

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/PiL2.lean
theorem coe_toBasis_repr_apply (b : OrthonormalBasis ι 𝕜 E) (x : E) (i : ι) :
    b.toBasis.repr x i = b.repr x i

Proof state:
ι : Type u_1
𝕜 : Type u_3
inst✝³ : RCLike 𝕜
E : Type u_4
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : Fintype ι
b : OrthonormalBasis ι 𝕜 E
x : E
i : ι
⊢ b.repr.toLinearEquiv x i = b.repr x i

Tactic:
erw [LinearIsometryEquiv.coe_toLinearEquiv]

Result:
no goals

Proof state:
ι : Type u_1
𝕜 : Type u_3
inst✝³ : RCLike 𝕜
E : Type u_4
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : Fintype ι
b : OrthonormalBasis ι 𝕜 E
x : E
i : ι
⊢ (b.toBasis.repr x) i = b.repr x i

Tactic:
rw [← Basis.equivFun_apply, OrthonormalBasis.coe_toBasis_repr]

Result:
ι : Type u_1
𝕜 : Type u_3
inst✝³ : RCLike 𝕜
E : Type u_4
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : Fintype ι
b : OrthonormalBasis ι 𝕜 E
x : E
i : ι
⊢ b.repr.toLinearEquiv x i = b.repr x i
-- Mathlib/Combinatorics/Schnirelmann.lean
/-- The Schnirelmann density is increasing with the set. -/
lemma schnirelmannDensity_le_of_subset {B : Set ℕ} [DecidablePred (· ∈ B)] (h : A ⊆ B) :
    schnirelmannDensity A ≤ schnirelmannDensity B :=
  ciInf_mono ⟨0, fun _ ⟨_, hx⟩ ↦ hx ▸ by positivity⟩ fun _ ↦ by
    gcongr; exact h

Proof state:
case hab.h.a.h
A : Set ℕ
inst✝¹ : DecidablePred fun x => x ∈ A
B : Set ℕ
inst✝ : DecidablePred fun x => x ∈ B
h : A ⊆ B
x✝ : { n // 0 < n }
⊢ (fun a => a ∈ A) ≤ fun a => a ∈ B

Tactic:
exact h

Result:
no goals

Proof state:
A : Set ℕ
inst✝¹ : DecidablePred fun x => x ∈ A
B : Set ℕ
inst✝ : DecidablePred fun x => x ∈ B
h : A ⊆ B
x✝ : { n // 0 < n }
⊢ ↑(#(filter (fun a => a ∈ A) (Ioc 0 ↑x✝))) / ↑↑x✝ ≤ ↑(#(filter (fun a => a ∈ B) (Ioc 0 ↑x✝))) / ↑↑x✝

Tactic:
gcongr

Result:
case hab.h.a.h
A : Set ℕ
inst✝¹ : DecidablePred fun x => x ∈ A
B : Set ℕ
inst✝ : DecidablePred fun x => x ∈ B
h : A ⊆ B
x✝ : { n // 0 < n }
⊢ (fun a => a ∈ A) ≤ fun a => a ∈ B

Proof state:
A : Set ℕ
inst✝¹ : DecidablePred fun x => x ∈ A
B : Set ℕ
inst✝ : DecidablePred fun x => x ∈ B
h : A ⊆ B
x✝¹ : ℝ
x✝ : x✝¹ ∈ Set.range fun n => ↑(#(filter (fun a => a ∈ A) (Ioc 0 ↑n))) / ↑↑n
w✝ : { n // 0 < n }
hx : (fun n => ↑(#(filter (fun a => a ∈ A) (Ioc 0 ↑n))) / ↑↑n) w✝ = x✝¹
⊢ 0 ≤ (fun n => ↑(#(filter (fun a => a ∈ A) (Ioc 0 ↑n))) / ↑↑n) w✝

Tactic:
positivity

Result:
no goals
-- Mathlib/Data/ENNReal/Inv.lean
/-- See `ENNReal.inv_mul_cancel_right'` for a stronger version. -/
protected lemma inv_mul_cancel_right (hb₀ : b ≠ 0) (hb : b ≠ ∞) : a * b⁻¹ * b = a :=
  ENNReal.inv_mul_cancel_right' (by simp [hb₀]) (by simp [hb])

Proof state:
a b : ℝ≥0∞
hb₀ : b ≠ 0
hb : b ≠ ⊤
⊢ b = 0 → a = 0

Tactic:
simp [hb₀]

Result:
no goals

Proof state:
a b : ℝ≥0∞
hb₀ : b ≠ 0
hb : b ≠ ⊤
⊢ b = ⊤ → a = 0

Tactic:
simp [hb]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Log/Basic.lean
lemma log_pos_of_isRat {n : ℤ} :
    (NormNum.IsRat e n d) → (decide ((1 : ℚ) < n / d)) → (0 < Real.log (e : ℝ))
  | ⟨inv, eq⟩, h => by
    rw [eq, invOf_eq_inv, ← div_eq_mul_inv]
    have : 1 < (n : ℝ) / d

Proof state:
e : ℝ
d : ℕ
n : ℤ
inv : Invertible ↑d
eq : e = ↑n * ⅟↑d
h : decide (1 < ↑n / ↑d) = true
⊢ 1 < ↑n / ↑d

Tactic:
exact_mod_cast of_decide_eq_true h

Result:
no goals

Proof state:
e : ℝ
d : ℕ
n : ℤ
inv : Invertible ↑d
eq : e = ↑n * ⅟↑d
h : decide (1 < ↑n / ↑d) = true
⊢ 0 < Real.log (↑n / ↑d)

Tactic:
have : 1 < (n : ℝ) / d := by exact_mod_cast of_decide_eq_true h

Result:
e : ℝ
d : ℕ
n : ℤ
inv : Invertible ↑d
eq : e = ↑n * ⅟↑d
h : decide (1 < ↑n / ↑d) = true
this : 1 < ↑n / ↑d
⊢ 0 < Real.log (↑n / ↑d)

Proof state:
e : ℝ
d : ℕ
n : ℤ
inv : Invertible ↑d
eq : e = ↑n * ⅟↑d
h : decide (1 < ↑n / ↑d) = true
⊢ 0 < Real.log e

Tactic:
rw [eq, invOf_eq_inv, ← div_eq_mul_inv]

Result:
e : ℝ
d : ℕ
n : ℤ
inv : Invertible ↑d
eq : e = ↑n * ⅟↑d
h : decide (1 < ↑n / ↑d) = true
⊢ 0 < Real.log (↑n / ↑d)

Proof state:
e : ℝ
d : ℕ
n : ℤ
inv : Invertible ↑d
eq : e = ↑n * ⅟↑d
h : decide (1 < ↑n / ↑d) = true
this : 1 < ↑n / ↑d
⊢ 0 < Real.log (↑n / ↑d)

Tactic:
exact Real.log_pos this

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Perm.lean
theorem Perm.append_right {l₁ l₂ : List α} (t₁ : List α) (p : l₁ ~ l₂) : l₁ ++ t₁ ~ l₂ ++ t₁

Proof state:
case nil
α : Type u_1
l₁ l₂ t₁ : List α
⊢ [] ++ t₁ ~ [] ++ t₁

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
l₁ l₂ t₁ : List α
p : l₁ ~ l₂
⊢ l₁ ++ t₁ ~ l₂ ++ t₁

Tactic:
induction p with
| nil => rfl
| cons _ _ ih => exact cons _ ih
| swap => exact swap ..
| trans _ _ ih₁ ih₂ => exact trans ih₁ ih₂

Result:
no goals

Proof state:
case trans
α : Type u_1
l₁ l₂ t₁ l₁✝ l₂✝ l₃✝ : List α
a✝¹ : l₁✝ ~ l₂✝
a✝ : l₂✝ ~ l₃✝
ih₁ : l₁✝ ++ t₁ ~ l₂✝ ++ t₁
ih₂ : l₂✝ ++ t₁ ~ l₃✝ ++ t₁
⊢ l₁✝ ++ t₁ ~ l₃✝ ++ t₁

Tactic:
exact trans ih₁ ih₂

Result:
no goals

Proof state:
case cons
α : Type u_1
l₁ l₂ t₁ : List α
x✝ : α
l₁✝ l₂✝ : List α
a✝ : l₁✝ ~ l₂✝
ih : l₁✝ ++ t₁ ~ l₂✝ ++ t₁
⊢ x✝ :: l₁✝ ++ t₁ ~ x✝ :: l₂✝ ++ t₁

Tactic:
exact cons _ ih

Result:
no goals

Proof state:
case swap
α : Type u_1
l₁ l₂ t₁ : List α
x✝ y✝ : α
l✝ : List α
⊢ y✝ :: x✝ :: l✝ ++ t₁ ~ x✝ :: y✝ :: l✝ ++ t₁

Tactic:
exact swap ..

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/ToLin.lean
theorem Matrix.toLinAlgEquiv_apply (M : Matrix n n R) (v : M₁) :
    Matrix.toLinAlgEquiv v₁ M v = ∑ j, (M *ᵥ v₁.repr v) j • v₁ j :=
  show v₁.equivFun.symm (Matrix.toLinAlgEquiv' M (v₁.repr v)) = _ by
    rw [Matrix.toLinAlgEquiv'_apply, v₁.equivFun_symm_apply]

Proof state:
R : Type u_1
inst✝⁴ : CommSemiring R
n : Type u_4
inst✝³ : Fintype n
inst✝² : DecidableEq n
M₁ : Type u_5
inst✝¹ : AddCommMonoid M₁
inst✝ : Module R M₁
v₁ : Basis n R M₁
M : Matrix n n R
v : M₁
⊢ v₁.equivFun.symm ((toLinAlgEquiv' M) ⇑(v₁.repr v)) = ∑ j : n, (M *ᵥ ⇑(v₁.repr v)) j • v₁ j

Tactic:
rw [Matrix.toLinAlgEquiv'_apply, v₁.equivFun_symm_apply]

Result:
no goals
-- Mathlib/Probability/IdentDistrib.lean
theorem lintegral_eq {f : α → ℝ≥0∞} {g : β → ℝ≥0∞} (h : IdentDistrib f g μ ν) :
    ∫⁻ x, f x ∂μ = ∫⁻ x, g x ∂ν

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
ν : Measure β
f : α → ℝ≥0∞
g : β → ℝ≥0∞
h : IdentDistrib f g μ ν
⊢ ∫⁻ (x : α), f x ∂μ = ∫⁻ (x : β), g x ∂ν

Tactic:
change ∫⁻ x, id (f x) ∂μ = ∫⁻ x, id (g x) ∂ν

Result:
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
ν : Measure β
f : α → ℝ≥0∞
g : β → ℝ≥0∞
h : IdentDistrib f g μ ν
⊢ ∫⁻ (x : α), id (f x) ∂μ = ∫⁻ (x : β), id (g x) ∂ν

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : MeasurableSpace β
μ : Measure α
ν : Measure β
f : α → ℝ≥0∞
g : β → ℝ≥0∞
h : IdentDistrib f g μ ν
⊢ ∫⁻ (x : α), id (f x) ∂μ = ∫⁻ (x : β), id (g x) ∂ν

Tactic:
rw [← lintegral_map' aemeasurable_id h.aemeasurable_fst, ←
  lintegral_map' aemeasurable_id h.aemeasurable_snd, h.map_eq]

Result:
no goals
-- Mathlib/SetTheory/ZFC/Basic.lean
lemma Definable₂.out_equiv (f : ZFSet.{u} → ZFSet.{u} → ZFSet.{u}) [Definable₂ f]
    {x₁ y₁ x₂ y₂ : PSet} (h₁ : x₁ ≈ y₁) (h₂ : x₂ ≈ y₂) :
    out f x₁ x₂ ≈ out f y₁ y₂ :=
  Definable.out_equiv _ (by simp [Fin.forall_fin_succ, h₁, h₂])

Proof state:
f : ZFSet.{u} → ZFSet.{u} → ZFSet.{u}
inst✝ : Definable₂ f
x₁ y₁ x₂ y₂ : PSet.{u}
h₁ : x₁ ≈ y₁
h₂ : x₂ ≈ y₂
⊢ ∀ (i : Fin (Nat.succ 0).succ), ![x₁, x₂] i ≈ ![y₁, y₂] i

Tactic:
simp [Fin.forall_fin_succ, h₁, h₂]

Result:
no goals
-- Mathlib/Algebra/Homology/Homotopy.lean
theorem dNext_zero_chainComplex (f : ∀ i j, P.X i ⟶ Q.X j) : dNext 0 f = 0

Proof state:
case a
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
P Q : ChainComplex V ℕ
f : (i j : ℕ) → P.X i ⟶ Q.X j
⊢ ¬1 = 0

Tactic:
decide

Result:
no goals

Proof state:
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
P Q : ChainComplex V ℕ
f : (i j : ℕ) → P.X i ⟶ Q.X j
⊢ P.d 0 ((ComplexShape.down ℕ).next 0) ≫ f ((ComplexShape.down ℕ).next 0) 0 = 0

Tactic:
rw [P.shape, zero_comp]

Result:
case a
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
P Q : ChainComplex V ℕ
f : (i j : ℕ) → P.X i ⟶ Q.X j
⊢ ¬(ComplexShape.down ℕ).Rel 0 ((ComplexShape.down ℕ).next 0)

Proof state:
case a
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
P Q : ChainComplex V ℕ
f : (i j : ℕ) → P.X i ⟶ Q.X j
⊢ ¬(ComplexShape.down ℕ).Rel 0 0

Tactic:
dsimp

Result:
case a
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
P Q : ChainComplex V ℕ
f : (i j : ℕ) → P.X i ⟶ Q.X j
⊢ ¬1 = 0

Proof state:
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
P Q : ChainComplex V ℕ
f : (i j : ℕ) → P.X i ⟶ Q.X j
⊢ (dNext 0) f = 0

Tactic:
dsimp [dNext]

Result:
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
P Q : ChainComplex V ℕ
f : (i j : ℕ) → P.X i ⟶ Q.X j
⊢ P.d 0 ((ComplexShape.down ℕ).next 0) ≫ f ((ComplexShape.down ℕ).next 0) 0 = 0

Proof state:
case a
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
P Q : ChainComplex V ℕ
f : (i j : ℕ) → P.X i ⟶ Q.X j
⊢ ¬(ComplexShape.down ℕ).Rel 0 ((ComplexShape.down ℕ).next 0)

Tactic:
rw [ChainComplex.next_nat_zero]

Result:
case a
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : Preadditive V
P Q : ChainComplex V ℕ
f : (i j : ℕ) → P.X i ⟶ Q.X j
⊢ ¬(ComplexShape.down ℕ).Rel 0 0
-- Mathlib/Data/Finsupp/Single.lean
theorem update_erase_eq_update (f : α →₀ M) (a : α) (b : M) :
    update (erase a f) a b = update f a b

Proof state:
α : Type u_1
M : Type u_5
inst✝ : Zero M
f : α →₀ M
a : α
b : M
⊢ (erase a f).update a b = f.update a b

Tactic:
rw [erase_eq_update_zero, update_idem]

Result:
no goals
-- Mathlib/AlgebraicGeometry/IdealSheaf.lean
lemma isClosed_support (I : IdealSheafData X) : IsClosed I.support

Proof state:
X : Scheme
I : X.IdealSheafData
U : ↑X.affineOpens
⊢ IsClosed (Subtype.val ⁻¹' I.support)

Tactic:
refine ⟨(X.zeroLocus (U := U.1) (I.ideal U))ᶜ, (X.zeroLocus_isClosed _).isOpen_compl, ?_⟩

Result:
X : Scheme
I : X.IdealSheafData
U : ↑X.affineOpens
⊢ Subtype.val ⁻¹' (X.zeroLocus ↑(I.ideal U))ᶜ = (Subtype.val ⁻¹' I.support)ᶜ

Proof state:
X : Scheme
I : X.IdealSheafData
U : ↑X.affineOpens
⊢ Subtype.val ⁻¹' X.zeroLocus ↑(I.ideal U) = Subtype.val ⁻¹' I.support

Tactic:
apply Subtype.val_injective.image_injective

Result:
case a
X : Scheme
I : X.IdealSheafData
U : ↑X.affineOpens
⊢ Subtype.val '' (Subtype.val ⁻¹' X.zeroLocus ↑(I.ideal U)) = Subtype.val '' (Subtype.val ⁻¹' I.support)

Proof state:
X : Scheme
I : X.IdealSheafData
U : ↑X.affineOpens
⊢ Subtype.val ⁻¹' (X.zeroLocus ↑(I.ideal U))ᶜ = (Subtype.val ⁻¹' I.support)ᶜ

Tactic:
simp only [Set.preimage_compl, compl_inj_iff]

Result:
X : Scheme
I : X.IdealSheafData
U : ↑X.affineOpens
⊢ Subtype.val ⁻¹' X.zeroLocus ↑(I.ideal U) = Subtype.val ⁻¹' I.support

Proof state:
X : Scheme
I : X.IdealSheafData
⊢ IsClosed I.support

Tactic:
rw [TopologicalSpace.IsOpenCover.isClosed_iff_coe_preimage (iSup_affineOpens_eq_top X)]

Result:
X : Scheme
I : X.IdealSheafData
⊢ ∀ (i : ↑X.affineOpens), IsClosed (Subtype.val ⁻¹' I.support)

Proof state:
case a
X : Scheme
I : X.IdealSheafData
U : ↑X.affineOpens
⊢ Subtype.val '' (Subtype.val ⁻¹' X.zeroLocus ↑(I.ideal U)) = Subtype.val '' (Subtype.val ⁻¹' I.support)

Tactic:
simp [Set.image_preimage_eq_inter_range, I.support_inter]

Result:
no goals

Proof state:
X : Scheme
I : X.IdealSheafData
⊢ ∀ (i : ↑X.affineOpens), IsClosed (Subtype.val ⁻¹' I.support)

Tactic:
intro U

Result:
X : Scheme
I : X.IdealSheafData
U : ↑X.affineOpens
⊢ IsClosed (Subtype.val ⁻¹' I.support)
-- Mathlib/Analysis/Calculus/IteratedDeriv/Defs.lean
theorem norm_iteratedFDeriv_eq_norm_iteratedDeriv :
    ‖iteratedFDeriv 𝕜 n f x‖ = ‖iteratedDeriv n f x‖

Proof state:
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
n : ℕ
f : 𝕜 → F
x : 𝕜
⊢ ‖iteratedFDeriv 𝕜 n f x‖ = ‖iteratedDeriv n f x‖

Tactic:
rw [iteratedDeriv_eq_equiv_comp, Function.comp_apply, LinearIsometryEquiv.norm_map]

Result:
no goals
-- Mathlib/Algebra/MvPolynomial/Supported.lean
theorem exists_restrict_to_vars (R : Type*) [CommRing R] {F : MvPolynomial σ ℤ}
    (hF : ↑F.vars ⊆ s) : ∃ f : (s → R) → R, ∀ x : σ → R, f (x ∘ (↑) : s → R) = aeval x F

Proof state:
case h
σ : Type u_1
s : Set σ
R : Type u_2
inst✝ : CommRing R
F : MvPolynomial σ ℤ
F' : MvPolynomial { x // x ∈ s } ℤ
hF' : (rename Subtype.val) F' = F
x : σ → R
⊢ (fun z => (aeval z) F') (x ∘ Subtype.val) = (aeval x) F

Tactic:
simp only [← hF', aeval_rename]

Result:
no goals

Proof state:
case h
σ : Type u_1
s : Set σ
R : Type u_2
inst✝ : CommRing R
F : MvPolynomial σ ℤ
F' : MvPolynomial { x // x ∈ s } ℤ
hF' : (rename Subtype.val) F' = F
⊢ ∀ (x : σ → R), (fun z => (aeval z) F') (x ∘ Subtype.val) = (aeval x) F

Tactic:
intro x

Result:
case h
σ : Type u_1
s : Set σ
R : Type u_2
inst✝ : CommRing R
F : MvPolynomial σ ℤ
F' : MvPolynomial { x // x ∈ s } ℤ
hF' : (rename Subtype.val) F' = F
x : σ → R
⊢ (fun z => (aeval z) F') (x ∘ Subtype.val) = (aeval x) F

Proof state:
σ : Type u_1
s : Set σ
R : Type u_2
inst✝ : CommRing R
F : MvPolynomial σ ℤ
hF : ↑F.vars ⊆ s
⊢ ∃ f, ∀ (x : σ → R), f (x ∘ Subtype.val) = (aeval x) F

Tactic:
rw [← mem_supported, supported_eq_range_rename, AlgHom.mem_range] at hF

Result:
σ : Type u_1
s : Set σ
R : Type u_2
inst✝ : CommRing R
F : MvPolynomial σ ℤ
hF : ∃ x, (rename Subtype.val) x = F
⊢ ∃ f, ∀ (x : σ → R), f (x ∘ Subtype.val) = (aeval x) F

Proof state:
case intro
σ : Type u_1
s : Set σ
R : Type u_2
inst✝ : CommRing R
F : MvPolynomial σ ℤ
F' : MvPolynomial { x // x ∈ s } ℤ
hF' : (rename Subtype.val) F' = F
⊢ ∃ f, ∀ (x : σ → R), f (x ∘ Subtype.val) = (aeval x) F

Tactic:
use fun z ↦ aeval z F'

Result:
case h
σ : Type u_1
s : Set σ
R : Type u_2
inst✝ : CommRing R
F : MvPolynomial σ ℤ
F' : MvPolynomial { x // x ∈ s } ℤ
hF' : (rename Subtype.val) F' = F
⊢ ∀ (x : σ → R), (fun z => (aeval z) F') (x ∘ Subtype.val) = (aeval x) F

Proof state:
σ : Type u_1
s : Set σ
R : Type u_2
inst✝ : CommRing R
F : MvPolynomial σ ℤ
hF : ∃ x, (rename Subtype.val) x = F
⊢ ∃ f, ∀ (x : σ → R), f (x ∘ Subtype.val) = (aeval x) F

Tactic:
obtain ⟨F', hF'⟩ := hF

Result:
case intro
σ : Type u_1
s : Set σ
R : Type u_2
inst✝ : CommRing R
F : MvPolynomial σ ℤ
F' : MvPolynomial { x // x ∈ s } ℤ
hF' : (rename Subtype.val) F' = F
⊢ ∃ f, ∀ (x : σ → R), f (x ∘ Subtype.val) = (aeval x) F
-- Mathlib/SetTheory/Nimber/Field.lean
theorem invAux_ne_zero (a : Nimber) : invAux a ≠ 0

Proof state:
a : Nimber
⊢ sInf a.invSetᶜ ≠ 0

Tactic:
exact fun h ↦ h ▸ csInf_mem (invSet_nonempty a) <| zero_mem_invSet a

Result:
no goals

Proof state:
a : Nimber
⊢ a.invAux ≠ 0

Tactic:
rw [invAux]

Result:
a : Nimber
⊢ sInf a.invSetᶜ ≠ 0
-- Mathlib/Topology/MetricSpace/Holder.lean
lemma smul {α} [NormedDivisionRing α] [Module α Y] [BoundedSMul α Y] (a : α)
    (hf : HolderWith C r f) : HolderWith (C * ‖a‖₊) r (a • f) := fun x₁ x₂ => by
  rw [Pi.smul_apply, coe_mul, Pi.smul_apply, edist_smul₀, mul_comm (C : ℝ≥0∞),
    ENNReal.smul_def, smul_eq_mul, mul_assoc]
  gcongr
  exact hf x₁ x₂

Proof state:
case bc
X : Type u_1
Y : Type u_2
inst✝⁴ : PseudoMetricSpace X
inst✝³ : SeminormedAddCommGroup Y
C r : ℝ≥0
f : X → Y
α : Type u_4
inst✝² : NormedDivisionRing α
inst✝¹ : Module α Y
inst✝ : BoundedSMul α Y
a : α
hf : HolderWith C r f
x₁ x₂ : X
⊢ edist (f x₁) (f x₂) ≤ ↑C * edist x₁ x₂ ^ ↑r

Tactic:
exact hf x₁ x₂

Result:
no goals

Proof state:
X : Type u_1
Y : Type u_2
inst✝⁴ : PseudoMetricSpace X
inst✝³ : SeminormedAddCommGroup Y
C r : ℝ≥0
f : X → Y
α : Type u_4
inst✝² : NormedDivisionRing α
inst✝¹ : Module α Y
inst✝ : BoundedSMul α Y
a : α
hf : HolderWith C r f
x₁ x₂ : X
⊢ ↑‖a‖₊ * edist (f x₁) (f x₂) ≤ ↑‖a‖₊ * (↑C * edist x₁ x₂ ^ ↑r)

Tactic:
gcongr

Result:
case bc
X : Type u_1
Y : Type u_2
inst✝⁴ : PseudoMetricSpace X
inst✝³ : SeminormedAddCommGroup Y
C r : ℝ≥0
f : X → Y
α : Type u_4
inst✝² : NormedDivisionRing α
inst✝¹ : Module α Y
inst✝ : BoundedSMul α Y
a : α
hf : HolderWith C r f
x₁ x₂ : X
⊢ edist (f x₁) (f x₂) ≤ ↑C * edist x₁ x₂ ^ ↑r

Proof state:
X : Type u_1
Y : Type u_2
inst✝⁴ : PseudoMetricSpace X
inst✝³ : SeminormedAddCommGroup Y
C r : ℝ≥0
f : X → Y
α : Type u_4
inst✝² : NormedDivisionRing α
inst✝¹ : Module α Y
inst✝ : BoundedSMul α Y
a : α
hf : HolderWith C r f
x₁ x₂ : X
⊢ edist ((a • f) x₁) ((a • f) x₂) ≤ ↑(C * ‖a‖₊) * edist x₁ x₂ ^ ↑r

Tactic:
rw [Pi.smul_apply, coe_mul, Pi.smul_apply, edist_smul₀, mul_comm (C : ℝ≥0∞),
  ENNReal.smul_def, smul_eq_mul, mul_assoc]

Result:
X : Type u_1
Y : Type u_2
inst✝⁴ : PseudoMetricSpace X
inst✝³ : SeminormedAddCommGroup Y
C r : ℝ≥0
f : X → Y
α : Type u_4
inst✝² : NormedDivisionRing α
inst✝¹ : Module α Y
inst✝ : BoundedSMul α Y
a : α
hf : HolderWith C r f
x₁ x₂ : X
⊢ ↑‖a‖₊ * edist (f x₁) (f x₂) ≤ ↑‖a‖₊ * (↑C * edist x₁ x₂ ^ ↑r)
-- Mathlib/Algebra/GroupWithZero/Basic.lean
lemma zero_zpow_eq_one₀ {n : ℤ} : (0 : G₀) ^ n = 1 ↔ n = 0

Proof state:
G₀ : Type u_2
inst✝ : GroupWithZero G₀
n : ℤ
⊢ 0 ^ n = 1 ↔ n = 0

Tactic:
rw [zero_zpow_eq, one_ne_zero.ite_eq_left_iff]

Result:
no goals
-- Mathlib/CategoryTheory/Abelian/Basic.lean
theorem imageIsoImage_inv :
    (imageIsoImage f).inv =
      kernel.lift _ (Limits.image.ι f) (by simp [← cancel_epi (factorThruImage f)])

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X Y : C
f : X ⟶ Y
⊢ (imageIsoImage f).inv = kernel.lift (cokernel.π f) (Limits.image.ι f) ⋯

Tactic:
ext

Result:
case w.h
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X Y : C
f : X ⟶ Y
⊢ (factorThruImage f ≫ (imageIsoImage f).inv) ≫ equalizer.ι (cokernel.π f) 0 =
    (factorThruImage f ≫ kernel.lift (cokernel.π f) (Limits.image.ι f) ⋯) ≫ equalizer.ι (cokernel.π f) 0

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X Y : C
f : X ⟶ Y
⊢ Limits.image.ι f ≫ cokernel.π f = 0

Tactic:
simp [← cancel_epi (factorThruImage f)]

Result:
no goals

Proof state:
case w.h
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X Y : C
f : X ⟶ Y
⊢ (factorThruImage f ≫ (imageIsoImage f).inv) ≫ equalizer.ι (cokernel.π f) 0 =
    (factorThruImage f ≫ kernel.lift (cokernel.π f) (Limits.image.ι f) ⋯) ≫ equalizer.ι (cokernel.π f) 0

Tactic:
rw [IsImage.isoExt_inv, image.isImage_lift, Limits.image.fac_lift,
  imageStrongEpiMonoFactorisation_e, Category.assoc, kernel.lift_ι, equalizer_as_kernel,
  kernel.lift_ι, Limits.image.fac]

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/Determinant/Basic.lean
theorem det_updateCol_smul (M : Matrix n n R) (j : n) (s : R) (u : n → R) :
    det (updateCol M j <| s • u) = s * det (updateCol M j u)

Proof state:
n : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
M : Matrix n n R
j : n
s : R
u : n → R
⊢ (M.updateCol j (s • u)).det = s * (M.updateCol j u).det

Tactic:
rw [← det_transpose, ← updateRow_transpose, det_updateRow_smul]

Result:
n : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
M : Matrix n n R
j : n
s : R
u : n → R
⊢ s * (Mᵀ.updateRow j u).det = s * (M.updateCol j u).det

Proof state:
n : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
M : Matrix n n R
j : n
s : R
u : n → R
⊢ s * (Mᵀ.updateRow j u).det = s * (M.updateCol j u).det

Tactic:
simp [updateRow_transpose, det_transpose]

Result:
no goals