harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/RingTheory/IntegralClosure/IsIntegralClosure/Basic.lean
theorem mk'_zero (h : IsIntegral R (0 : B) := isIntegral_zero) : mk' A 0 h = 0 :=
  algebraMap_injective A R B <| by rw [algebraMap_mk', RingHom.map_zero]

Proof state:
R : Type u_1
A : Type u_2
B : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : CommRing B
inst✝² : Algebra R B
inst✝¹ : Algebra A B
inst✝ : IsIntegralClosure A R B
h : optParam (IsIntegral R 0) ⋯
⊢ (algebraMap A B) (mk' A 0 h) = (algebraMap A B) 0

Tactic:
rw [algebraMap_mk', RingHom.map_zero]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem length_insert_of_mem {l : List α} (h : a ∈ l) :
    length (l.insert a) = length l

Proof state:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a : α
l : List α
h : a ∈ l
⊢ (List.insert a l).length = l.length

Tactic:
rw [insert_of_mem h]

Result:
no goals
-- Mathlib/CategoryTheory/Shift/Basic.lean
theorem shift_shiftFunctorCompIsoId_neg_add_cancel_inv_app (n : A) (X : C) :
    ((shiftFunctorCompIsoId C (-n) n (neg_add_cancel n)).inv.app X)⟦-n⟧' =
    (shiftFunctorCompIsoId C n (-n) (add_neg_cancel n)).inv.app (X⟦-n⟧)

Proof state:
C : Type u
A : Type u_1
inst✝² : Category.{v, u} C
inst✝¹ : AddGroup A
inst✝ : HasShift C A
n : A
X : C
⊢ (shiftFunctor C (-n)).map ((shiftFunctorCompIsoId C (-n) n ⋯).inv.app X) =
    (shiftFunctorCompIsoId C n (-n) ⋯).inv.app ((shiftFunctor C (-n)).obj X)

Tactic:
apply shift_shiftFunctorCompIsoId_inv_app

Result:
no goals
-- Mathlib/Data/Nat/Init.lean
lemma succ_succ_ne_one (n : ℕ) : n.succ.succ ≠ 1

Proof state:
n : ℕ
⊢ n.succ.succ ≠ 1

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem getElem_drop (a : Vector α n) (m : Nat) (hi : i < n - m) :
    (a.drop m)[i] = a[m + i]

Proof state:
α : Type u_1
n i : Nat
a : Vector α n
m : Nat
hi : i < n - m
⊢ (a.drop m)[i] = a[m + i]

Tactic:
cases a

Result:
case mk
α : Type u_1
n i m : Nat
hi : i < n - m
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
⊢ ({ toArray := toArray✝, size_toArray := size_toArray✝ }.drop m)[i] =
    { toArray := toArray✝, size_toArray := size_toArray✝ }[m + i]

Proof state:
case mk
α : Type u_1
n i m : Nat
hi : i < n - m
toArray✝ : Array α
size_toArray✝ : toArray✝.size = n
⊢ ({ toArray := toArray✝, size_toArray := size_toArray✝ }.drop m)[i] =
    { toArray := toArray✝, size_toArray := size_toArray✝ }[m + i]

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Sym/Basic.lean
theorem cons_of_coe_eq (a : α) (v : List.Vector α n) : a ::ₛ (↑v : Sym α n) = ↑(a ::ᵥ v) :=
  Subtype.ext <| by
    cases v
    rfl

Proof state:
case mk
α : Type u_1
n : ℕ
a : α
val✝ : List α
property✝ : val✝.length = n
⊢ ↑(a ::ₛ ofVector ⟨val✝, property✝⟩) = ↑(ofVector (a ::ᵥ ⟨val✝, property✝⟩))

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
n : ℕ
a : α
v : List.Vector α n
⊢ ↑(a ::ₛ ofVector v) = ↑(ofVector (a ::ᵥ v))

Tactic:
cases v

Result:
case mk
α : Type u_1
n : ℕ
a : α
val✝ : List α
property✝ : val✝.length = n
⊢ ↑(a ::ₛ ofVector ⟨val✝, property✝⟩) = ↑(ofVector (a ::ᵥ ⟨val✝, property✝⟩))
-- Mathlib/Analysis/LocallyConvex/WeakOperatorTopology.lean
lemma continuous_dual_apply (x : E) (y : F⋆) : Continuous fun (A : E →WOT[𝕜] F) => y (A x)

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁸ : NormedField 𝕜
inst✝⁷ : AddCommGroup E
inst✝⁶ : TopologicalSpace E
inst✝⁵ : Module 𝕜 E
inst✝⁴ : AddCommGroup F
inst✝³ : TopologicalSpace F
inst✝² : Module 𝕜 F
inst✝¹ : IsTopologicalAddGroup F
inst✝ : ContinuousConstSMul 𝕜 F
x : E
y : F →L[𝕜] 𝕜
⊢ Continuous fun A => y (A x)

Tactic:
refine (continuous_pi_iff.mp continuous_inducingFn) ⟨x, y⟩

Result:
no goals
-- Mathlib/Data/Matroid/Circuit.lean
lemma IsCircuit.isCocircuit (hC : M.IsCircuit C) : M✶.IsCocircuit C

Proof state:
α : Type u_1
M : Matroid α
C : Set α
hC : M.IsCircuit C
⊢ M✶.IsCocircuit C

Tactic:
rwa [isCocircuit_def, dual_dual]

Result:
no goals
-- Mathlib/Analysis/Normed/Group/Hom.lean
theorem lipschitz : LipschitzWith ⟨‖f‖, opNorm_nonneg f⟩ f :=
  LipschitzWith.of_dist_le_mul fun x y => by
    rw [dist_eq_norm, dist_eq_norm, ← map_sub]
    apply le_opNorm

Proof state:
V₁ : Type u_2
V₂ : Type u_3
inst✝¹ : SeminormedAddCommGroup V₁
inst✝ : SeminormedAddCommGroup V₂
f : NormedAddGroupHom V₁ V₂
x y : V₁
⊢ dist (f x) (f y) ≤ ↑⟨‖f‖, ⋯⟩ * dist x y

Tactic:
rw [dist_eq_norm, dist_eq_norm, ← map_sub]

Result:
V₁ : Type u_2
V₂ : Type u_3
inst✝¹ : SeminormedAddCommGroup V₁
inst✝ : SeminormedAddCommGroup V₂
f : NormedAddGroupHom V₁ V₂
x y : V₁
⊢ ‖f (x - y)‖ ≤ ↑⟨‖f‖, ⋯⟩ * ‖x - y‖

Proof state:
V₁ : Type u_2
V₂ : Type u_3
inst✝¹ : SeminormedAddCommGroup V₁
inst✝ : SeminormedAddCommGroup V₂
f : NormedAddGroupHom V₁ V₂
x y : V₁
⊢ ‖f (x - y)‖ ≤ ↑⟨‖f‖, ⋯⟩ * ‖x - y‖

Tactic:
apply le_opNorm

Result:
no goals
-- Mathlib/Probability/Kernel/Disintegration/CDFToKernel.lean
lemma integral_stieltjesOfMeasurableRat [IsFiniteKernel κ] (hf : IsRatCondKernelCDF f κ ν)
    (a : α) (x : ℝ) :
    ∫ b, stieltjesOfMeasurableRat f hf.measurable (a, b) x ∂(ν a)
      = (κ a (univ ×ˢ Iic x)).toReal

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
inst✝ : IsFiniteKernel κ
hf : IsRatCondKernelCDF f κ ν
a : α
x : ℝ
⊢ ∫ (b : β), ↑(stieltjesOfMeasurableRat f ⋯ (a, b)) x ∂ν a = ((κ a) (univ ×ˢ Iic x)).toReal

Tactic:
rw [← setIntegral_univ, setIntegral_stieltjesOfMeasurableRat hf _ _ MeasurableSet.univ]

Result:
no goals
-- Mathlib/Computability/Primrec.lean
theorem list_head? : Primrec (@List.head? α) :=
  (list_casesOn .id (const none) (option_some_iff.2 <| fst.comp snd).to₂).of_eq fun l => by
    cases l <;> rfl

Proof state:
α : Type u_1
inst✝ : Primcodable α
l : List α
⊢ (List.casesOn (id l) none fun b l_1 => some (l, b, l_1).2.1) = l.head?

Tactic:
cases l <;> rfl

Result:
no goals
-- Mathlib/Topology/Connected/PathConnected.lean
theorem isPathConnected_pathComponent : IsPathConnected (pathComponent x)

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
x : X
⊢ IsPathConnected (pathComponent x)

Tactic:
rw [← pathComponentIn_univ]

Result:
X : Type u_1
inst✝ : TopologicalSpace X
x : X
⊢ IsPathConnected (pathComponentIn x univ)

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
x : X
⊢ IsPathConnected (pathComponentIn x univ)

Tactic:
exact isPathConnected_pathComponentIn (mem_univ x)

Result:
no goals
-- Mathlib/Data/Matrix/PEquiv.lean
theorem single_mul_single_of_ne [Fintype n] [DecidableEq n] [DecidableEq k] [DecidableEq m]
    [Semiring α] {b₁ b₂ : n} (hb : b₁ ≠ b₂) (a : m) (c : k) :
    (single a b₁).toMatrix * (single b₂ c).toMatrix = (0 : Matrix _ _ α)

Proof state:
k : Type u_1
m : Type u_3
n : Type u_4
α : Type u_5
inst✝⁴ : Fintype n
inst✝³ : DecidableEq n
inst✝² : DecidableEq k
inst✝¹ : DecidableEq m
inst✝ : Semiring α
b₁ b₂ : n
hb : b₁ ≠ b₂
a : m
c : k
⊢ (single a b₁).toMatrix * (single b₂ c).toMatrix = 0

Tactic:
rw [← toMatrix_trans, single_trans_single_of_ne hb, toMatrix_bot]

Result:
no goals
-- Mathlib/Data/List/Rotate.lean
theorem isRotated_singleton_iff' {x : α} : [x] ~r l ↔ [x] = l

Proof state:
α : Type u
l : List α
x : α
⊢ [x] ~r l ↔ [x] = l

Tactic:
rw [isRotated_comm, isRotated_singleton_iff, eq_comm]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Angle.lean
theorem intCast_mul_eq_zsmul (x : ℝ) (n : ℤ) : ↑((n : ℝ) * x : ℝ) = n • (↑x : Angle)

Proof state:
x : ℝ
n : ℤ
⊢ ↑(↑n * x) = n • ↑x

Tactic:
simpa only [zsmul_eq_mul] using coeHom.map_zsmul x n

Result:
no goals
-- Mathlib/Control/Monad/Cont.lean
theorem monadLift_bind [Monad m] [LawfulMonad m] {α β} (x : m α) (f : α → m β) :
    (monadLift (x >>= f) : ContT r m β) = monadLift x >>= monadLift ∘ f

Proof state:
r : Type u
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α β : Type u
x : m α
f : α → m β
⊢ monadLift (x >>= f) = monadLift x >>= monadLift ∘ f

Tactic:
ext

Result:
case h
r : Type u
m : Type u → Type v
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α β : Type u
x : m α
f : α → m β
f✝ : β → m r
⊢ (monadLift (x >>= f)).run f✝ = (monadLift x >>= monadLift ∘ f).run f✝
-- Mathlib/Topology/MetricSpace/Isometry.lean
theorem preimage_ball (h : α ≃ᵢ β) (x : β) (r : ℝ) :
    h ⁻¹' Metric.ball x r = Metric.ball (h.symm x) r

Proof state:
α : Type u
β : Type v
inst✝¹ : PseudoMetricSpace α
inst✝ : PseudoMetricSpace β
h : α ≃ᵢ β
x : β
r : ℝ
⊢ ⇑h ⁻¹' Metric.ball x r = Metric.ball (h.symm x) r

Tactic:
rw [← h.isometry.preimage_ball (h.symm x) r, h.apply_symm_apply]

Result:
no goals
-- Mathlib/LinearAlgebra/AnnihilatingPolynomial.lean
theorem mem_iff_annIdealGenerator_dvd {p : 𝕜[X]} {a : A} :
    p ∈ annIdeal 𝕜 a ↔ annIdealGenerator 𝕜 a ∣ p

Proof state:
𝕜 : Type u_1
A : Type u_2
inst✝² : Field 𝕜
inst✝¹ : Ring A
inst✝ : Algebra 𝕜 A
p : 𝕜[X]
a : A
⊢ p ∈ annIdeal 𝕜 a ↔ annIdealGenerator 𝕜 a ∣ p

Tactic:
rw [← Ideal.mem_span_singleton, span_singleton_annIdealGenerator]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Log/Base.lean
theorem logb_neg_eq_logb (x : ℝ) : logb b (-x) = logb b x

Proof state:
b x : ℝ
⊢ logb b (-x) = logb b x

Tactic:
rw [← logb_abs x, ← logb_abs (-x), abs_neg]

Result:
no goals
-- Mathlib/CategoryTheory/Bicategory/Basic.lean
theorem pentagon_hom_hom_inv_hom_hom (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d) (i : d ⟶ e) :
    (α_ (f ≫ g) h i).hom ≫ (α_ f g (h ≫ i)).hom ≫ f ◁ (α_ g h i).inv =
      (α_ f g h).hom ▷ i ≫ (α_ f (g ≫ h) i).hom :=
  eq_of_inv_eq_inv (by simp)

Proof state:
B : Type u
inst✝ : Bicategory B
a b c d e : B
f : a ⟶ b
g : b ⟶ c
h : c ⟶ d
i : d ⟶ e
⊢ inv ((α_ (f ≫ g) h i).hom ≫ (α_ f g (h ≫ i)).hom ≫ f ◁ (α_ g h i).inv) =
    inv ((α_ f g h).hom ▷ i ≫ (α_ f (g ≫ h) i).hom)

Tactic:
simp

Result:
no goals
-- Mathlib/RingTheory/Multiplicity.lean
theorem multiplicity_eq_of_emultiplicity_eq_some {n : ℕ} (h : emultiplicity a b = n) :
    multiplicity a b = n

Proof state:
α : Type u_1
inst✝ : Monoid α
a b : α
n : ℕ
h : emultiplicity a b = ↑n
⊢ multiplicity a b = n

Tactic:
simp [multiplicity, h]

Result:
α : Type u_1
inst✝ : Monoid α
a b : α
n : ℕ
h : emultiplicity a b = ↑n
⊢ WithTop.untopD 1 ↑n = n

Proof state:
α : Type u_1
inst✝ : Monoid α
a b : α
n : ℕ
h : emultiplicity a b = ↑n
⊢ WithTop.untopD 1 ↑n = n

Tactic:
rfl

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

Proof state:
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulBEq α
m : Raw₀ α β
a : α
⊢ m.val.get? a = m.get? a

Tactic:
simp [Raw.get?, m.2]

Result:
no goals
-- Mathlib/Data/Matroid/Closure.lean
@[simp] lemma isFlat_closure : M.IsFlat (M.closure X)

Proof state:
α : Type u_2
M : Matroid α
X : Set α
⊢ M.IsFlat (M.closure X)

Tactic:
rw [closure, sInter_eq_iInter]

Result:
α : Type u_2
M : Matroid α
X : Set α
⊢ M.IsFlat (⋂ i, ↑i)
-- Mathlib/MeasureTheory/Function/SimpleFunc.lean
theorem restrict_preimage (f : α →ₛ β) {s : Set α} (hs : MeasurableSet s) {t : Set β}
    (ht : (0 : β) ∉ t) : restrict f s ⁻¹' t = s ∩ f ⁻¹' t

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : MeasurableSpace α
inst✝ : Zero β
f : α →ₛ β
s : Set α
hs : MeasurableSet s
t : Set β
ht : 0 ∉ t
⊢ ⇑(f.restrict s) ⁻¹' t = s ∩ ⇑f ⁻¹' t

Tactic:
simp [hs, indicator_preimage_of_not_mem _ _ ht, inter_comm]

Result:
no goals
-- Mathlib/Data/Real/Basic.lean
theorem ext_cauchy_iff : ∀ {x y : Real}, x = y ↔ x.cauchy = y.cauchy
  | ⟨a⟩, ⟨b⟩ => by rw [ofCauchy.injEq]

Proof state:
a b : Cauchy abs
⊢ { cauchy := a } = { cauchy := b } ↔ { cauchy := a }.cauchy = { cauchy := b }.cauchy

Tactic:
rw [ofCauchy.injEq]

Result:
no goals
-- Mathlib/Tactic/CategoryTheory/Bicategory/PureCoherence.lean
theorem naturality_associator
    {p : a ⟶ b} {f : b ⟶ c} {g : c ⟶ d} {h : d ⟶ e} {pf : a ⟶ c} {pfg : a ⟶ d} {pfgh : a ⟶ e}
    (η_f : p ≫ f ≅ pf) (η_g : pf ≫ g ≅ pfg) (η_h : pfg ≫ h ≅ pfgh) :
    p ◁ (α_ f g h) ≪≫ (normalizeIsoComp η_f (normalizeIsoComp η_g η_h)) =
    (normalizeIsoComp (normalizeIsoComp η_f η_g) η_h) :=
  Iso.ext (by simp)

Proof state:
B : Type u
inst✝ : Bicategory B
a b c d e : B
p : a ⟶ b
f : b ⟶ c
g : c ⟶ d
h : d ⟶ e
pf : a ⟶ c
pfg : a ⟶ d
pfgh : a ⟶ e
η_f : p ≫ f ≅ pf
η_g : pf ≫ g ≅ pfg
η_h : pfg ≫ h ≅ pfgh
⊢ (p ◁ α_ f g h ≪≫ normalizeIsoComp η_f (normalizeIsoComp η_g η_h)).hom =
    (normalizeIsoComp (normalizeIsoComp η_f η_g) η_h).hom

Tactic:
simp

Result:
no goals
-- Mathlib/Geometry/Euclidean/Inversion/Basic.lean
theorem inversion_mul (c : P) (a R : ℝ) (x : P) :
    inversion c (a * R) x = homothety c (a ^ 2) (inversion c R x)

Proof state:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
c : P
a R : ℝ
x : P
⊢ inversion c (a * R) x = (homothety c (a ^ 2)) (inversion c R x)

Tactic:
simp only [inversion_eq_lineMap, ← homothety_eq_lineMap, ← homothety_mul_apply, mul_div_assoc,
  mul_pow]

Result:
no goals
-- Mathlib/Algebra/Algebra/Operations.lean
theorem prod_span_singleton {ι : Type*} (s : Finset ι) (x : ι → A) :
    (∏ i ∈ s, span R ({x i} : Set A)) = span R {∏ i ∈ s, x i}

Proof state:
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
ι : Type u_1
s : Finset ι
x : ι → A
⊢ ∏ i ∈ s, span R {x i} = span R {∏ i ∈ s, x i}

Tactic:
rw [prod_span, Set.finset_prod_singleton]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem getMsbD_cons_succ : (cons a x).getMsbD (i + 1) = x.getMsbD i

Proof state:
a : Bool
w✝ : Nat
x : BitVec w✝
i : Nat
⊢ (cons a x).getMsbD (i + 1) = x.getMsbD i

Tactic:
simp [cons, Nat.le_add_left 1 i]

Result:
no goals
-- Mathlib/CategoryTheory/ComposableArrows.lean
@[simp]
lemma homMk₄_app_four :
    (homMk₄ app₀ app₁ app₂ app₃ app₄ w₀ w₁ w₂ w₃).app ⟨4, by valid⟩ = app₄ := rfl

Proof state:
C : Type u_1
inst✝ : Category.{?u.280369, u_1} C
n m : ℕ
F G : ComposableArrows C n
f g : ComposableArrows C 4
app₀ : f.obj' 0 ⋯ ⟶ g.obj' 0 ⋯
app₁ : f.obj' 1 ⋯ ⟶ g.obj' 1 ⋯
app₂ : f.obj' 2 ⋯ ⟶ g.obj' 2 ⋯
app₃ : f.obj' 3 ⋯ ⟶ g.obj' 3 ⋯
app₄ : f.obj' 4 ⋯ ⟶ g.obj' 4 ⋯
w₀ : f.map' 0 1 ⋯ ⋯ ≫ app₁ = app₀ ≫ g.map' 0 1 ⋯ ⋯
w₁ : f.map' 1 2 ⋯ ⋯ ≫ app₂ = app₁ ≫ g.map' 1 2 ⋯ ⋯
w₂ : f.map' 2 3 ⋯ ⋯ ≫ app₃ = app₂ ≫ g.map' 2 3 ⋯ ⋯
w₃ : f.map' 3 4 ⋯ ⋯ ≫ app₄ = app₃ ≫ g.map' 3 4 ⋯ ⋯
⊢ 4 < 4 + 1

Tactic:
valid

Result:
no goals
-- Mathlib/LinearAlgebra/Span/Defs.lean
theorem span_eq_iSup_of_singleton_spans (s : Set M) : span R s = ⨆ x ∈ s, R ∙ x

Proof state:
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
⊢ span R s = ⨆ x ∈ s, span R {x}

Tactic:
simp only [← span_iUnion, Set.biUnion_of_singleton s]

Result:
no goals
-- Mathlib/CategoryTheory/Functor/KanExtension/Adjunction.lean
@[reassoc (attr := simp)]
lemma leftKanExtensionUnit_leftKanExtensionObjIsoColimit_hom (X : C) :
    (L.leftKanExtensionUnit F).app X ≫ (L.leftKanExtensionObjIsoColimit F (L.obj X)).hom =
    colimit.ι (proj L (L.obj X) ⋙ F) (CostructuredArrow.mk (𝟙 _))

Proof state:
C : Type u_1
D : Type u_2
inst✝³ : Category.{u_5, u_1} C
inst✝² : Category.{u_6, u_2} D
L : C ⥤ D
H : Type u_3
inst✝¹ : Category.{u_4, u_3} H
F : C ⥤ H
inst✝ : L.HasPointwiseLeftKanExtension F
X : C
⊢ (L.leftKanExtensionUnit F).app X ≫ (L.leftKanExtensionObjIsoColimit F (L.obj X)).hom =
    colimit.ι (proj L (L.obj X) ⋙ F) (CostructuredArrow.mk (𝟙 (L.obj X)))

Tactic:
simpa using leftKanExtensionUnit_leftKanExtension_map_leftKanExtensionObjIsoColimit_hom L F
  (L.obj X) (CostructuredArrow.mk (𝟙 _))

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/NNReal.lean
@[simp] lemma rpow_rpow_inv {y : ℝ} (hy : y ≠ 0) (x : ℝ≥0∞) : (x ^ y) ^ y⁻¹ = x

Proof state:
y : ℝ
hy : y ≠ 0
x : ℝ≥0∞
⊢ (x ^ y) ^ y⁻¹ = x

Tactic:
rw [← rpow_mul, mul_inv_cancel₀ hy, rpow_one]

Result:
no goals
-- Mathlib/Order/Filter/Basic.lean
theorem mem_inf_principal' {f : Filter α} {s t : Set α} : s ∈ f ⊓ 𝓟 t ↔ tᶜ ∪ s ∈ f

Proof state:
α : Type u
f : Filter α
s t : Set α
⊢ s ∈ f ⊓ 𝓟 t ↔ tᶜ ∪ s ∈ f

Tactic:
simp only [← le_principal_iff, (isCompl_principal s).le_left_iff, disjoint_assoc, inf_principal,
  ← (isCompl_principal (t ∩ sᶜ)).le_right_iff, compl_inter, compl_compl]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/NullMeasurable.lean
lemma measure_preimage_snd_singleton_eq_sum [Fintype α] (μ : Measure (α × β)) (y : β) :
    μ (Prod.snd ⁻¹' {y}) = ∑ x, μ {(x, y)}

Proof state:
α : Type u_2
β : Type u_3
m0 : MeasurableSpace α
inst✝² : MeasurableSingletonClass α
mβ : MeasurableSpace β
inst✝¹ : MeasurableSingletonClass β
inst✝ : Fintype α
μ : Measure (α × β)
y : β
⊢ μ (Prod.snd ⁻¹' {y}) = ∑ x : α, μ {(x, y)}

Tactic:
rw [measure_preimage_snd_singleton_eq_tsum μ y, tsum_fintype]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Angle.lean
theorem neg_ne_self_iff {θ : Angle} : -θ ≠ θ ↔ θ ≠ 0 ∧ θ ≠ π

Proof state:
θ : Angle
⊢ -θ ≠ θ ↔ θ ≠ 0 ∧ θ ≠ ↑π

Tactic:
rw [← not_or, ← neg_eq_self_iff.not]

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/NonsingularInverse.lean
theorem conjTranspose_nonsing_inv [StarRing α] : A⁻¹ᴴ = Aᴴ⁻¹

Proof state:
n : Type u'
α : Type v
inst✝³ : Fintype n
inst✝² : DecidableEq n
inst✝¹ : CommRing α
A : Matrix n n α
inst✝ : StarRing α
⊢ A⁻¹ᴴ = Aᴴ⁻¹

Tactic:
rw [inv_def, inv_def, conjTranspose_smul, det_conjTranspose, adjugate_conjTranspose,
  Ring.inverse_star]

Result:
no goals
-- Mathlib/GroupTheory/NoncommPiCoprod.lean
@[to_additive]
lemma noncommPiCoprod_apply (h : (i : ι) → N i) :
    MonoidHom.noncommPiCoprod ϕ hcomm h = Finset.noncommProd Finset.univ (fun i ↦ ϕ i (h i))
      (Pairwise.set_pairwise (fun ⦃i j⦄ a ↦ hcomm a (h i) (h j)) _)

Proof state:
M : Type u_1
inst✝² : Monoid M
ι : Type u_2
inst✝¹ : Fintype ι
N : ι → Type u_3
inst✝ : (i : ι) → Monoid (N i)
ϕ : (i : ι) → N i →* M
hcomm : Pairwise fun i j => ∀ (x : N i) (y : N j), Commute ((ϕ i) x) ((ϕ j) y)
h : (i : ι) → N i
⊢ (noncommPiCoprod ϕ hcomm) h = Finset.univ.noncommProd (fun i => (ϕ i) (h i)) ⋯

Tactic:
dsimp only [MonoidHom.noncommPiCoprod, MonoidHom.coe_mk, OneHom.coe_mk]

Result:
no goals
-- Mathlib/RingTheory/PowerSeries/Basic.lean
theorem rescale_zero_apply : rescale 0 X = C R (constantCoeff R X)

Proof state:
R : Type u_1
inst✝ : CommSemiring R
⊢ (rescale 0) X = (C R) ((constantCoeff R) X)

Tactic:
simp

Result:
no goals
-- Mathlib/CategoryTheory/Preadditive/Transfer.lean
/-- The preadditive structure on `C` induced by a fully faithful functor `F : C ⥤ D` makes `F` an
additive functor. -/
lemma additive_ofFullyFaithful :
    letI : Preadditive C := Preadditive.ofFullyFaithful hF
    F.Additive :=
  letI : Preadditive C := Preadditive.ofFullyFaithful hF
  { map_add

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
inst✝ : Preadditive D
F : C ⥤ D
hF : F.FullyFaithful
this : Preadditive C := Preadditive.ofFullyFaithful hF
⊢ ∀ {X Y : C} {f g : X ⟶ Y}, F.map (f + g) = F.map f + F.map g

Tactic:
simp [Equiv.add_def]

Result:
no goals
-- Mathlib/RingTheory/MvPowerSeries/Basic.lean
theorem coeff_index_single_X [DecidableEq σ] (s t : σ) :
    coeff R (single t 1) (X s : MvPowerSeries σ R) = if t = s then 1 else 0

Proof state:
σ : Type u_1
R : Type u_2
inst✝¹ : Semiring R
inst✝ : DecidableEq σ
s t : σ
⊢ (coeff R (single t 1)) (X s) = if t = s then 1 else 0

Tactic:
simp only [coeff_X, single_left_inj (one_ne_zero : (1 : ℕ) ≠ 0)]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Complex/Arg.lean
@[simp]
lemma norm_mul_sin_arg (x : ℂ) : ‖x‖ * Real.sin (arg x) = x.im

Proof state:
x : ℂ
⊢ ‖x‖ * Real.sin x.arg = x.im

Tactic:
simpa [-norm_mul_cos_add_sin_mul_I] using congr_arg im (norm_mul_cos_add_sin_mul_I x)

Result:
no goals
-- Mathlib/Data/Set/Card.lean
theorem ncard_le_one_iff_subset_singleton [Nonempty α]
    (hs : s.Finite

Proof state:
α : Type u_1
s : Set α
inst✝ : Nonempty α
hs : autoParam s.Finite _auto✝
⊢ s.ncard ≤ 1 ↔ ∃ x, s ⊆ {x}

Tactic:
simp_rw [ncard_eq_toFinset_card _ hs, Finset.card_le_one_iff_subset_singleton,
  Finite.toFinset_subset, Finset.coe_singleton]

Result:
no goals
-- Mathlib/Analysis/Calculus/Deriv/Mul.lean
theorem HasDerivAt.smul_const (hc : HasDerivAt c c' x) (f : F) :
    HasDerivAt (fun y => c y • f) (c' • f) x

Proof state:
𝕜 : Type u
inst✝⁶ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
x : 𝕜
𝕜' : Type u_2
inst✝³ : NontriviallyNormedField 𝕜'
inst✝² : NormedAlgebra 𝕜 𝕜'
inst✝¹ : NormedSpace 𝕜' F
inst✝ : IsScalarTower 𝕜 𝕜' F
c : 𝕜 → 𝕜'
c' : 𝕜'
hc : HasDerivWithinAt c c' univ x
f : F
⊢ HasDerivWithinAt (fun y => c y • f) (c' • f) univ x

Tactic:
exact hc.smul_const f

Result:
no goals

Proof state:
𝕜 : Type u
inst✝⁶ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
x : 𝕜
𝕜' : Type u_2
inst✝³ : NontriviallyNormedField 𝕜'
inst✝² : NormedAlgebra 𝕜 𝕜'
inst✝¹ : NormedSpace 𝕜' F
inst✝ : IsScalarTower 𝕜 𝕜' F
c : 𝕜 → 𝕜'
c' : 𝕜'
hc : HasDerivAt c c' x
f : F
⊢ HasDerivAt (fun y => c y • f) (c' • f) x

Tactic:
rw [← hasDerivWithinAt_univ] at *

Result:
𝕜 : Type u
inst✝⁶ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
x : 𝕜
𝕜' : Type u_2
inst✝³ : NontriviallyNormedField 𝕜'
inst✝² : NormedAlgebra 𝕜 𝕜'
inst✝¹ : NormedSpace 𝕜' F
inst✝ : IsScalarTower 𝕜 𝕜' F
c : 𝕜 → 𝕜'
c' : 𝕜'
hc : HasDerivWithinAt c c' univ x
f : F
⊢ HasDerivWithinAt (fun y => c y • f) (c' • f) univ x
-- Mathlib/Analysis/Calculus/FDeriv/Equiv.lean
theorem comp_hasFDerivWithinAt_iff' {f : G → E} {s : Set G} {x : G} {f' : G →L[𝕜] F} :
    HasFDerivWithinAt (iso ∘ f) f' s x ↔
      HasFDerivWithinAt f ((iso.symm : F →L[𝕜] E).comp f') s x

Proof state:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
iso : E ≃L[𝕜] F
f : G → E
s : Set G
x : G
f' : G →L[𝕜] F
⊢ HasFDerivWithinAt (⇑iso ∘ f) f' s x ↔ HasFDerivWithinAt f ((↑iso.symm).comp f') s x

Tactic:
rw [← iso.comp_hasFDerivWithinAt_iff, ← ContinuousLinearMap.comp_assoc, iso.coe_comp_coe_symm,
  ContinuousLinearMap.id_comp]

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian.lean
lemma addXYZ_smul (P Q : Fin 3 → R) (u v : R) :
    W'.addXYZ (u • P) (v • Q) = (u * v) ^ 2 • W'.addXYZ P Q

Proof state:
R : Type r
inst✝ : CommRing R
W' : Jacobian R
P Q : Fin 3 → R
u v : R
⊢ W'.addXYZ (u • P) (v • Q) = (u * v) ^ 2 • W'.addXYZ P Q

Tactic:
rw [addXYZ, addX_smul, addY_smul, addZ_smul, smul_fin3, addXYZ_X, addXYZ_Y, addXYZ_Z]

Result:
no goals
-- Mathlib/Analysis/Convex/Strong.lean
lemma UniformConvexOn.sub (hf : UniformConvexOn s φ f) (hg : UniformConcaveOn s ψ g) :
    UniformConvexOn s (φ + ψ) (f - g)

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
φ ψ : ℝ → ℝ
s : Set E
f g : E → ℝ
hf : UniformConvexOn s φ f
hg : UniformConcaveOn s ψ g
⊢ UniformConvexOn s (φ + ψ) (f - g)

Tactic:
simpa using hf.add hg.neg

Result:
no goals
-- Mathlib/Algebra/MvPolynomial/Eval.lean
theorem comp_aeval {B : Type*} [CommSemiring B] [Algebra R B] (φ : S₁ →ₐ[R] B) :
    φ.comp (aeval f) = aeval fun i => φ (f i)

Proof state:
R : Type u
S₁ : Type v
σ : Type u_1
inst✝⁴ : CommSemiring R
inst✝³ : CommSemiring S₁
inst✝² : Algebra R S₁
f : σ → S₁
B : Type u_2
inst✝¹ : CommSemiring B
inst✝ : Algebra R B
φ : S₁ →ₐ[R] B
⊢ φ.comp (aeval f) = aeval fun i => φ (f i)

Tactic:
ext i

Result:
case hf
R : Type u
S₁ : Type v
σ : Type u_1
inst✝⁴ : CommSemiring R
inst✝³ : CommSemiring S₁
inst✝² : Algebra R S₁
f : σ → S₁
B : Type u_2
inst✝¹ : CommSemiring B
inst✝ : Algebra R B
φ : S₁ →ₐ[R] B
i : σ
⊢ (φ.comp (aeval f)) (X i) = (aeval fun i => φ (f i)) (X i)

Proof state:
case hf
R : Type u
S₁ : Type v
σ : Type u_1
inst✝⁴ : CommSemiring R
inst✝³ : CommSemiring S₁
inst✝² : Algebra R S₁
f : σ → S₁
B : Type u_2
inst✝¹ : CommSemiring B
inst✝ : Algebra R B
φ : S₁ →ₐ[R] B
i : σ
⊢ (φ.comp (aeval f)) (X i) = (aeval fun i => φ (f i)) (X i)

Tactic:
simp

Result:
no goals