harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/CategoryTheory/Limits/Opposites.lean
@[reassoc (attr := simp)]
lemma limitLeftOpIsoUnopColimit_inv_comp_π (F : J ⥤ Cᵒᵖ) [HasColimit F] (j : Jᵒᵖ) :
    (limitLeftOpIsoUnopColimit F).inv ≫ limit.π F.leftOp j = (colimit.ι F j.unop).unop

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
J : Type u₂
inst✝¹ : Category.{v₂, u₂} J
F : J ⥤ Cᵒᵖ
inst✝ : HasColimit F
j : Jᵒᵖ
⊢ (limitLeftOpIsoUnopColimit F).inv ≫ limit.π F.leftOp j = (colimit.ι F (unop j)).unop

Tactic:
simp [limitLeftOpIsoUnopColimit]

Result:
no goals
-- Mathlib/Order/Interval/Set/OrderEmbedding.lean
theorem preimage_uIoc [LinearOrder β] (e : α ↪o β) (x y : α) :
    e ⁻¹' (uIoc (e x) (e y)) = uIoc x y

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LinearOrder β
e : α ↪o β
x y : α
⊢ ⇑e ⁻¹' Ι (e x) (e y) = Ι x y

Tactic:
cases le_total x y <;> simp [*]

Result:
no goals
-- Mathlib/Order/Interval/Set/Basic.lean
theorem right_mem_Icc : b ∈ Icc a b ↔ a ≤ b

Proof state:
α : Type u_1
inst✝ : Preorder α
a b : α
⊢ b ∈ Icc a b ↔ a ≤ b

Tactic:
simp [le_refl]

Result:
no goals
-- Mathlib/Combinatorics/Young/YoungDiagram.lean
theorem rowLen_eq_card (μ : YoungDiagram) {i : ℕ} : μ.rowLen i = (μ.row i).card

Proof state:
μ : YoungDiagram
i : ℕ
⊢ μ.rowLen i = (μ.row i).card

Tactic:
simp [row_eq_prod]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Bool.lean
theorem eq_true_imp_eq_false_iff :
    ∀ (a b : Bool), ((a = true → b = false) ↔ (b = true → a = false)) = True

Proof state:
⊢ ∀ (a b : Bool), (a = true → b = false ↔ b = true → a = false) = True

Tactic:
decide

Result:
no goals
-- Mathlib/Algebra/BigOperators/Finprod.lean
theorem finprod_mem_empty : (∏ᶠ i ∈ (∅ : Set α), f i) = 1

Proof state:
α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
f : α → M
⊢ ∏ᶠ (i : α) (_ : i ∈ ∅), f i = 1

Tactic:
simp

Result:
no goals
-- Mathlib/Computability/ContextFreeGrammar.lean
@[simp] lemma reverse_reverse (g : ContextFreeGrammar T) : g.reverse.reverse = g

Proof state:
T : Type u_1
g : ContextFreeGrammar T
⊢ g.reverse.reverse = g

Tactic:
simp [reverse, Finset.map_map]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem getValueCastD_insertEntryIfNew [BEq α] [LawfulBEq α] {l : List ((a : α) × β a)} {k a : α}
    {v : β k} {fallback : β a} : getValueCastD a (insertEntryIfNew k v l) fallback =
      if h : k == a ∧ containsKey k l = false then cast (congrArg β (eq_of_beq h.1)) v
      else getValueCastD a l fallback

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l : List ((a : α) × β a)
k a : α
v : β k
fallback : β a
⊢ getValueCastD a (insertEntryIfNew k v l) fallback =
    if h : (k == a) = true ∧ containsKey k l = false then cast ⋯ v else getValueCastD a l fallback

Tactic:
simp [getValueCastD_eq_getValueCast?, getValueCast?_insertEntryIfNew,
  apply_dite (fun x => Option.getD x fallback)]

Result:
no goals
-- Mathlib/RingTheory/IntegralClosure/IsIntegralClosure/Basic.lean
theorem RingHom.isIntegralElem.of_comp {x : T} (h : (g.comp f).IsIntegralElem x) :
    g.IsIntegralElem x :=
  let ⟨p, hp, hp'⟩ := h
  ⟨p.map f, hp.map f, by rwa [← eval₂_map] at hp'⟩

Proof state:
R : Type u_1
S : Type u_4
T : Type u_5
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CommRing T
f : R →+* S
g : S →+* T
x : T
h : (g.comp f).IsIntegralElem x
p : R[X]
hp : p.Monic
hp' : eval₂ (g.comp f) x p = 0
⊢ eval₂ g x (Polynomial.map f p) = 0

Tactic:
rwa [← eval₂_map] at hp'

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem swapAt!_mk (a : Array α) (h : a.size = n) (i x) : (Vector.mk a h).swapAt! i x =
    ((a.swapAt! i x).fst, Vector.mk (a.swapAt! i x).snd (by simp [h])) := rfl

Proof state:
α : Type ?u.17182
n : Nat
a : Array α
h : a.size = n
i : Nat
x : α
⊢ (a.swapAt! i x).snd.size = n

Tactic:
simp [h]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem getD_eq_getD_get? [EquivBEq α] [LawfulHashable α] (h : m.1.WF) {a : α} {fallback : β} :
    getD m a fallback = (get? m a).getD fallback

Proof state:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
β : Type v
m : Raw₀ α fun x => β
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.val.WF
a : α
fallback : β
⊢ getD m a fallback = (get? m a).getD fallback

Tactic:
simp_to_model using List.getValueD_eq_getValue?

Result:
no goals
-- Mathlib/Order/GaloisConnection/Basic.lean
theorem l_sSup {s : Set α} : l (sSup s) = ⨆ a ∈ s, l a

Proof state:
α : Type u
β : Type v
inst✝¹ : CompleteLattice α
inst✝ : CompleteLattice β
l : α → β
u : β → α
gc : GaloisConnection l u
s : Set α
⊢ l (sSup s) = ⨆ a ∈ s, l a

Tactic:
simp only [sSup_eq_iSup, gc.l_iSup]

Result:
no goals
-- Mathlib/Data/Nat/Factorization/Basic.lean
theorem ordProj_mul {a b : ℕ} (p : ℕ) (ha : a ≠ 0) (hb : b ≠ 0) :
    ordProj[p] (a * b) = ordProj[p] a * ordProj[p] b

Proof state:
a b p : ℕ
ha : a ≠ 0
hb : b ≠ 0
⊢ p ^ (a * b).factorization p = p ^ a.factorization p * p ^ b.factorization p

Tactic:
simp [factorization_mul ha hb, pow_add]

Result:
no goals
-- Mathlib/Probability/Kernel/Composition/MapComap.lean
@[simp]
lemma prodMkLeft_add (κ η : Kernel α β) :
    prodMkLeft γ (κ + η) = prodMkLeft γ κ + prodMkLeft γ η

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ η : Kernel α β
⊢ prodMkLeft γ (κ + η) = prodMkLeft γ κ + prodMkLeft γ η

Tactic:
ext

Result:
case h.h
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ η : Kernel α β
a✝¹ : γ × α
s✝ : Set β
a✝ : MeasurableSet s✝
⊢ ((prodMkLeft γ (κ + η)) a✝¹) s✝ = ((prodMkLeft γ κ + prodMkLeft γ η) a✝¹) s✝

Proof state:
case h.h
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ η : Kernel α β
a✝¹ : γ × α
s✝ : Set β
a✝ : MeasurableSet s✝
⊢ ((prodMkLeft γ (κ + η)) a✝¹) s✝ = ((prodMkLeft γ κ + prodMkLeft γ η) a✝¹) s✝

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Polynomial/Bivariate.lean
lemma evalEval_prod {ι : Type*} (s : Finset ι) (x y : R) (p : ι → R[X][Y]) :
    (∏ j ∈ s, p j).evalEval x y = ∏ j ∈ s, (p j).evalEval x y

Proof state:
R : Type u_1
inst✝ : CommSemiring R
ι : Type u_3
s : Finset ι
x y : R
p : ι → R[X][Y]
⊢ evalEval x y (∏ j ∈ s, p j) = ∏ j ∈ s, evalEval x y (p j)

Tactic:
simp only [evalEval, eval_prod]

Result:
no goals
-- Mathlib/Order/Hom/Lattice.lean
theorem cancel_left {g : BoundedLatticeHom β γ} {f₁ f₂ : BoundedLatticeHom α β} (hg : Injective g) :
    g.comp f₁ = g.comp f₂ ↔ f₁ = f₂ :=
  ⟨fun h => ext fun a => hg <| by rw [← comp_apply, h, comp_apply], congr_arg _⟩

Proof state:
α : Type u_3
β : Type u_4
γ : Type u_5
inst✝⁵ : Lattice α
inst✝⁴ : Lattice β
inst✝³ : Lattice γ
inst✝² : BoundedOrder α
inst✝¹ : BoundedOrder β
inst✝ : BoundedOrder γ
g : BoundedLatticeHom β γ
f₁ f₂ : BoundedLatticeHom α β
hg : Injective ⇑g
h : g.comp f₁ = g.comp f₂
a : α
⊢ g (f₁ a) = g (f₂ a)

Tactic:
rw [← comp_apply, h, comp_apply]

Result:
no goals
-- Mathlib/Analysis/Matrix.lean
theorem norm_lt_iff {r : ℝ} (hr : 0 < r) {A : Matrix m n α} : ‖A‖ < r ↔ ∀ i j, ‖A i j‖ < r

Proof state:
m : Type u_3
n : Type u_4
α : Type u_5
inst✝² : Fintype m
inst✝¹ : Fintype n
inst✝ : SeminormedAddCommGroup α
r : ℝ
hr : 0 < r
A : Matrix m n α
⊢ ‖A‖ < r ↔ ∀ (i : m) (j : n), ‖A i j‖ < r

Tactic:
simp_rw [norm_def, pi_norm_lt_iff hr]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem getKey!_insertManyIfNewUnit_list_of_contains_eq_false_of_contains_eq_false
    [EquivBEq α] [LawfulHashable α] [Inhabited α] (h : m.1.WF) {l : List α} {k : α} :
    m.contains k = false → l.contains k = false →
      getKey! (insertManyIfNewUnit m l).1 k = default

Proof state:
α : Type u
inst✝⁴ : BEq α
inst✝³ : Hashable α
m : Raw₀ α fun x => Unit
inst✝² : EquivBEq α
inst✝¹ : LawfulHashable α
inst✝ : Inhabited α
h : m.val.WF
l : List α
k : α
⊢ m.contains k = false → l.contains k = false → (insertManyIfNewUnit m l).val.getKey! k = default

Tactic:
simp_to_model [Const.insertManyIfNewUnit] using List.getKey!_insertListIfNewUnit_of_contains_eq_false_of_contains_eq_false

Result:
no goals
-- Mathlib/AlgebraicGeometry/ProjectiveSpectrum/Topology.lean
theorem gc_homogeneousIdeal :
    @GaloisConnection (HomogeneousIdeal 𝒜) (Set (ProjectiveSpectrum 𝒜))ᵒᵈ _ _
      (fun I => zeroLocus 𝒜 I) fun t => vanishingIdeal t :=
  fun I t => by
  simpa [show I.toIdeal ≤ (vanishingIdeal t).toIdeal ↔ I ≤ vanishingIdeal t from Iff.rfl] using
    subset_zeroLocus_iff_le_vanishingIdeal t I.toIdeal

Proof state:
R : Type u_1
A : Type u_2
inst✝³ : CommSemiring R
inst✝² : CommRing A
inst✝¹ : Algebra R A
𝒜 : ℕ → Submodule R A
inst✝ : GradedAlgebra 𝒜
I : HomogeneousIdeal 𝒜
t : (Set (ProjectiveSpectrum 𝒜))ᵒᵈ
⊢ (fun I => zeroLocus 𝒜 ↑I) I ≤ t ↔ I ≤ (fun t => vanishingIdeal t) t

Tactic:
simpa [show I.toIdeal ≤ (vanishingIdeal t).toIdeal ↔ I ≤ vanishingIdeal t from Iff.rfl] using
  subset_zeroLocus_iff_le_vanishingIdeal t I.toIdeal

Result:
no goals
-- Mathlib/Order/UpperLower/Basic.lean
lemma IsLowerSet.sdiff_of_isUpperSet (hs : IsLowerSet s) (ht : IsUpperSet t) : IsLowerSet (s \ t) :=
  hs.sdiff <| by aesop

Proof state:
α : Type u_1
inst✝ : LE α
s t : Set α
hs : IsLowerSet s
ht : IsUpperSet t
⊢ ∀ b ∈ s, ∀ c ∈ t, c ≤ b → b ∈ t

Tactic:
aesop

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/Real.lean
theorem rpow_intCast (x : ℝ) (n : ℤ) : x ^ (n : ℝ) = x ^ n

Proof state:
x : ℝ
n : ℤ
⊢ x ^ ↑n = x ^ n

Tactic:
simp only [rpow_def, ← Complex.ofReal_zpow, Complex.cpow_intCast, Complex.ofReal_intCast,
  Complex.ofReal_re]

Result:
no goals
-- Mathlib/MeasureTheory/Group/FundamentalDomain.lean
theorem mem_fundamentalInterior :
    x ∈ fundamentalInterior G s ↔ x ∈ s ∧ ∀ g : G, g ≠ 1 → x ∉ g • s

Proof state:
G : Type u_1
α : Type u_3
inst✝¹ : Group G
inst✝ : MulAction G α
s : Set α
x : α
⊢ x ∈ fundamentalInterior G s ↔ x ∈ s ∧ ∀ (g : G), g ≠ 1 → x ∉ g • s

Tactic:
simp [fundamentalInterior]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Eval/Defs.lean
@[simp]
lemma eval_ofNat (n : ℕ) [n.AtLeastTwo] (a : R) :
    (ofNat(n) : R[X]).eval a = ofNat(n)

Proof state:
R : Type u
inst✝¹ : Semiring R
n : ℕ
inst✝ : n.AtLeastTwo
a : R
⊢ eval a (OfNat.ofNat n) = OfNat.ofNat n

Tactic:
simp only [OfNat.ofNat, eval_natCast]

Result:
no goals
-- Mathlib/Algebra/Group/Basic.lean
theorem mul_inv_eq_iff_eq_mul : a * b⁻¹ = c ↔ a = c * b :=
  ⟨fun h ↦ by rw [← h, inv_mul_cancel_right], fun h ↦ by rw [h, mul_inv_cancel_right]⟩

Proof state:
G : Type u_3
inst✝ : Group G
a b c : G
h : a * b⁻¹ = c
⊢ a = c * b

Tactic:
rw [← h, inv_mul_cancel_right]

Result:
no goals

Proof state:
G : Type u_3
inst✝ : Group G
a b c : G
h : a = c * b
⊢ a * b⁻¹ = c

Tactic:
rw [h, mul_inv_cancel_right]

Result:
no goals
-- Mathlib/LinearAlgebra/TensorAlgebra/Basic.lean
theorem ι_comp_lift {A : Type*} [Semiring A] [Algebra R A] (f : M →ₗ[R] A) :
    (lift R f).toLinearMap.comp (ι R) = f

Proof state:
R : Type u_1
inst✝⁴ : CommSemiring R
M : Type u_2
inst✝³ : AddCommMonoid M
inst✝² : Module R M
A : Type u_3
inst✝¹ : Semiring A
inst✝ : Algebra R A
f : M →ₗ[R] A
⊢ ((lift R) f).toLinearMap ∘ₗ ι R = f

Tactic:
convert (lift R).symm_apply_apply f

Result:
no goals
-- Mathlib/NumberTheory/ModularForms/QExpansion.lean
theorem bounded_at_infty_comp_ofComplex [ModularFormClass F Γ k] :
    BoundedAtFilter I∞ (f ∘ ofComplex)

Proof state:
k : ℤ
F : Type u_1
inst✝¹ : FunLike F ℍ ℂ
Γ : Subgroup SL(2, ℤ)
f : F
inst✝ : ModularFormClass F Γ k
⊢ I∞.BoundedAtFilter (⇑f ∘ ↑ofComplex)

Tactic:
simpa only [SlashAction.slash_one, ModularForm.toSlashInvariantForm_coe]
  using (ModularFormClass.bdd_at_infty f 1).comp_tendsto tendsto_comap_im_ofComplex

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem get?_eq_some_getD [LawfulBEq α] (h : m.WF) {a : α} {fallback : β a} :
    a ∈ m → m.get? a = some (m.getD a fallback)

Proof state:
α : Type u
β : α → Type v
m : Raw α β
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulBEq α
h : m.WF
a : α
fallback : β a
⊢ a ∈ m → m.get? a = some (m.getD a fallback)

Tactic:
simpa [mem_iff_contains] using get?_eq_some_getD_of_contains h

Result:
no goals
-- Mathlib/Probability/Independence/Kernel.lean
theorem IndepSet.measure_inter_eq_mul {_m0 : MeasurableSpace Ω} (κ : Kernel α Ω) (μ : Measure α)
    (h : IndepSet s t κ μ) : ∀ᵐ a ∂μ, κ a (s ∩ t) = κ a s * κ a t :=
  Indep.indepSets h _ _ (by simp) (by simp)

Proof state:
α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
s t : Set Ω
_m0 : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
h : IndepSet s t κ μ
⊢ s ∈ {s}

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
Ω : Type u_2
_mα : MeasurableSpace α
s t : Set Ω
_m0 : MeasurableSpace Ω
κ : Kernel α Ω
μ : Measure α
h : IndepSet s t κ μ
⊢ t ∈ {t}

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Seq/WSeq.lean
theorem ofList_cons (a : α) (l) : ofList (a::l) = cons a (ofList l) :=
  show Seq.map some (Seq.ofList (a::l)) = Seq.cons (some a) (Seq.map some (Seq.ofList l)) by simp

Proof state:
α : Type u
a : α
l : List α
⊢ Seq.map some ↑(a :: l) = Seq.cons (some a) (Seq.map some ↑l)

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem get!_modify (h : m.1.WF) {k k' : α} [hi : Inhabited (β k')] {f : β k → β k} :
    (m.modify k f).get! k' =
      if heq : k == k' then
        m.get? k |>.map f |>.map (cast (congrArg β (eq_of_beq heq))) |>.get!
      else
        m.get! k'

Proof state:
α : Type u
β : α → Type v
m : Raw₀ α β
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulBEq α
h : m.val.WF
k k' : α
hi : Inhabited (β k')
f : β k → β k
⊢ (m.modify k f).get! k' =
    if heq : (k == k') = true then (Option.map (cast ⋯) (Option.map f (m.get? k))).get! else m.get! k'

Tactic:
simp_to_model [modify] using List.getValueCast!_modifyKey

Result:
no goals
-- Mathlib/Analysis/Normed/Lp/lpSpace.lean
theorem norm_eq_tsum_rpow (hp : 0 < p.toReal) (f : lp E p) :
    ‖f‖ = (∑' i, ‖f i‖ ^ p.toReal) ^ (1 / p.toReal)

Proof state:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
hp : 0 < p ∧ p < ⊤
f : ↥(lp E p)
⊢ (if hp : p = 0 then Eq.rec (motive := fun x x_1 => ↥(lp E x) → ℝ) (fun f => ↑⋯.toFinset.card) ⋯ f
    else if p = ⊤ then ⨆ i, ‖↑f i‖ else (∑' (i : α), ‖↑f i‖ ^ p.toReal) ^ (1 / p.toReal)) =
    (∑' (i : α), ‖↑f i‖ ^ p.toReal) ^ (1 / p.toReal)

Tactic:
rw [dif_neg hp.1.ne', if_neg hp.2.ne]

Result:
no goals

Proof state:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
hp : 0 < p.toReal
f : ↥(lp E p)
⊢ (if hp : p = 0 then Eq.rec (motive := fun x x_1 => ↥(lp E x) → ℝ) (fun f => ↑⋯.toFinset.card) ⋯ f
    else if p = ⊤ then ⨆ i, ‖↑f i‖ else (∑' (i : α), ‖↑f i‖ ^ p.toReal) ^ (1 / p.toReal)) =
    (∑' (i : α), ‖↑f i‖ ^ p.toReal) ^ (1 / p.toReal)

Tactic:
rw [ENNReal.toReal_pos_iff] at hp

Result:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
hp : 0 < p ∧ p < ⊤
f : ↥(lp E p)
⊢ (if hp : p = 0 then Eq.rec (motive := fun x x_1 => ↥(lp E x) → ℝ) (fun f => ↑⋯.toFinset.card) ⋯ f
    else if p = ⊤ then ⨆ i, ‖↑f i‖ else (∑' (i : α), ‖↑f i‖ ^ p.toReal) ^ (1 / p.toReal)) =
    (∑' (i : α), ‖↑f i‖ ^ p.toReal) ^ (1 / p.toReal)

Proof state:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
hp : 0 < p.toReal
f : ↥(lp E p)
⊢ ‖f‖ = (∑' (i : α), ‖↑f i‖ ^ p.toReal) ^ (1 / p.toReal)

Tactic:
dsimp [norm]

Result:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
hp : 0 < p.toReal
f : ↥(lp E p)
⊢ (if hp : p = 0 then Eq.rec (motive := fun x x_1 => ↥(lp E x) → ℝ) (fun f => ↑⋯.toFinset.card) ⋯ f
    else if p = ⊤ then ⨆ i, ‖↑f i‖ else (∑' (i : α), ‖↑f i‖ ^ p.toReal) ^ (1 / p.toReal)) =
    (∑' (i : α), ‖↑f i‖ ^ p.toReal) ^ (1 / p.toReal)
-- Mathlib/MeasureTheory/Function/LpSeminorm/Trim.lean
theorem essSup_trim (hm : m ≤ m0) {f : α → ℝ≥0∞} (hf : Measurable[m] f) :
    essSup f (μ.trim hm) = essSup f μ

Proof state:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : α → ℝ≥0∞
hf : Measurable f
⊢ limsup f (ae (μ.trim hm)) = limsup f (ae μ)

Tactic:
exact limsup_trim hm hf

Result:
no goals

Proof state:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : α → ℝ≥0∞
hf : Measurable f
⊢ essSup f (μ.trim hm) = essSup f μ

Tactic:
simp_rw [essSup]

Result:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
f : α → ℝ≥0∞
hf : Measurable f
⊢ limsup f (ae (μ.trim hm)) = limsup f (ae μ)
-- Mathlib/MeasureTheory/Decomposition/Lebesgue.lean
theorem rnDeriv_smul_left_of_ne_top' (ν μ : Measure α) [SigmaFinite ν] [SigmaFinite μ]
    {r : ℝ≥0∞} (hr : r ≠ ∞) :
    (r • ν).rnDeriv μ =ᵐ[μ] r • ν.rnDeriv μ

Proof state:
α : Type u_1
m : MeasurableSpace α
ν μ : Measure α
inst✝¹ : SigmaFinite ν
inst✝ : SigmaFinite μ
r : ℝ≥0∞
hr : r ≠ ⊤
h : (r.toNNReal • ν).rnDeriv μ =ᶠ[ae μ] r.toNNReal • ν.rnDeriv μ
⊢ (r • ν).rnDeriv μ =ᶠ[ae μ] r • ν.rnDeriv μ

Tactic:
simpa [ENNReal.smul_def, ENNReal.coe_toNNReal hr] using h

Result:
no goals

Proof state:
α : Type u_1
m : MeasurableSpace α
ν μ : Measure α
inst✝¹ : SigmaFinite ν
inst✝ : SigmaFinite μ
r : ℝ≥0∞
hr : r ≠ ⊤
⊢ (r • ν).rnDeriv μ =ᶠ[ae μ] r • ν.rnDeriv μ

Tactic:
have h : (r.toNNReal • ν).rnDeriv μ =ᵐ[μ] r.toNNReal • ν.rnDeriv μ :=
  rnDeriv_smul_left' ν μ r.toNNReal

Result:
α : Type u_1
m : MeasurableSpace α
ν μ : Measure α
inst✝¹ : SigmaFinite ν
inst✝ : SigmaFinite μ
r : ℝ≥0∞
hr : r ≠ ⊤
h : (r.toNNReal • ν).rnDeriv μ =ᶠ[ae μ] r.toNNReal • ν.rnDeriv μ
⊢ (r • ν).rnDeriv μ =ᶠ[ae μ] r • ν.rnDeriv μ
-- Mathlib/Dynamics/PeriodicPts/Defs.lean
theorem Commute.minimalPeriod_of_comp_dvd_lcm {g : α → α} (h : Commute f g) :
    minimalPeriod (f ∘ g) x ∣ Nat.lcm (minimalPeriod f x) (minimalPeriod g x)

Proof state:
α : Type u_1
f : α → α
x : α
g : α → α
h : Function.Commute f g
⊢ minimalPeriod (f ∘ g) x ∣ (minimalPeriod f x).lcm (minimalPeriod g x)

Tactic:
rw [← isPeriodicPt_iff_minimalPeriod_dvd]

Result:
α : Type u_1
f : α → α
x : α
g : α → α
h : Function.Commute f g
⊢ IsPeriodicPt (f ∘ g) ((minimalPeriod f x).lcm (minimalPeriod g x)) x

Proof state:
α : Type u_1
f : α → α
x : α
g : α → α
h : Function.Commute f g
⊢ IsPeriodicPt (f ∘ g) ((minimalPeriod f x).lcm (minimalPeriod g x)) x

Tactic:
exact (isPeriodicPt_minimalPeriod f x).comp_lcm h (isPeriodicPt_minimalPeriod g x)

Result:
no goals
-- Mathlib/Analysis/Calculus/Deriv/Basic.lean
theorem HasDerivAtFilter.isBigO_sub_rev (hf : HasDerivAtFilter f f' x L) (hf' : f' ≠ 0) :
    (fun x' => x' - x) =O[L] fun x' => f x' - f x :=
  suffices AntilipschitzWith ‖f'‖₊⁻¹ (smulRight (1 : 𝕜 →L[𝕜] 𝕜) f') from hf.isBigO_sub_rev this
  AddMonoidHomClass.antilipschitz_of_bound (smulRight (1 : 𝕜 →L[𝕜] 𝕜) f') fun x => by
    simp [norm_smul, ← div_eq_inv_mul, mul_div_cancel_right₀ _ (mt norm_eq_zero.1 hf')]

Proof state:
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
f' : F
x✝ : 𝕜
L : Filter 𝕜
hf : HasDerivAtFilter f f' x✝ L
hf' : f' ≠ 0
x : 𝕜
⊢ ‖x‖ ≤ ↑‖f'‖₊⁻¹ * ‖(smulRight 1 f') x‖

Tactic:
simp [norm_smul, ← div_eq_inv_mul, mul_div_cancel_right₀ _ (mt norm_eq_zero.1 hf')]

Result:
no goals
-- Mathlib/Algebra/Polynomial/HasseDeriv.lean
theorem hasseDeriv_zero' : hasseDeriv 0 f = f

Proof state:
R : Type u_1
inst✝ : Semiring R
f : R[X]
⊢ (hasseDeriv 0) f = f

Tactic:
simp only [hasseDeriv_apply, tsub_zero, Nat.choose_zero_right, Nat.cast_one, one_mul,
  sum_monomial_eq]

Result:
no goals
-- Mathlib/Order/Basic.lean
lemma eq_iff_not_lt_of_le (hab : a ≤ b) : a = b ↔ ¬ a < b

Proof state:
α : Type u_2
inst✝ : PartialOrder α
a b : α
hab : a ≤ b
⊢ a = b ↔ ¬a < b

Tactic:
simp [hab, lt_iff_le_and_ne]

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Exponential.lean
theorem log_of_not_one_lt_left {b : Ordinal} (h : ¬1 < b) (x : Ordinal) : log b x = 0

Proof state:
b : Ordinal.{u_1}
h : ¬1 < b
x : Ordinal.{u_1}
⊢ log b x = 0

Tactic:
simp only [log, if_neg h]

Result:
no goals
-- Mathlib/Analysis/Complex/CauchyIntegral.lean
theorem analyticOn_univ_iff_differentiable {f : ℂ → E} :
    AnalyticOn ℂ f univ ↔ Differentiable ℂ f

Proof state:
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
⊢ AnalyticOn ℂ f univ ↔ Differentiable ℂ f

Tactic:
rw [analyticOn_univ]

Result:
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
⊢ AnalyticOnNhd ℂ f univ ↔ Differentiable ℂ f

Proof state:
E : Type u
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
⊢ AnalyticOnNhd ℂ f univ ↔ Differentiable ℂ f

Tactic:
exact analyticOnNhd_univ_iff_differentiable

Result:
no goals
-- Mathlib/Data/List/Basic.lean
theorem map_foldl_erase [DecidableEq β] {f : α → β} (finj : Injective f) {l₁ l₂ : List α} :
    map f (foldl List.erase l₁ l₂) = foldl (fun l a => l.erase (f a)) (map f l₁) l₂

Proof state:
α : Type u
β : Type v
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
f : α → β
finj : Injective f
l₁ l₂ : List α
⊢ map f (foldl List.erase l₁ l₂) = foldl (fun l a => l.erase (f a)) (map f l₁) l₂

Tactic:
induction l₂ generalizing l₁ <;> [rfl; simp only [foldl_cons, map_erase finj, *]]

Result:
no goals
-- Mathlib/Analysis/Normed/MulAction.lean
theorem edist_smul₀ (s : α) (x y : β) : edist (s • x) (s • y) = ‖s‖₊ • edist x y

Proof state:
α : Type u_1
β : Type u_2
inst✝³ : NormedDivisionRing α
inst✝² : SeminormedAddCommGroup β
inst✝¹ : Module α β
inst✝ : BoundedSMul α β
s : α
x y : β
⊢ edist (s • x) (s • y) = ‖s‖₊ • edist x y

Tactic:
simp only [edist_nndist, nndist_smul₀, ENNReal.coe_mul, ENNReal.smul_def, smul_eq_mul]

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/Orientation.lean
theorem adjustToOrientation_apply_eq_or_eq_neg (i : ι) :
    e.adjustToOrientation x i = e i ∨ e.adjustToOrientation x i = -e i

Proof state:
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace ℝ E
ι : Type u_2
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
e : OrthonormalBasis ι ℝ E
x : Orientation ℝ E ι
inst✝ : Nonempty ι
i : ι
⊢ (e.adjustToOrientation x) i = e i ∨ (e.adjustToOrientation x) i = -e i

Tactic:
simpa [← e.toBasis_adjustToOrientation] using
  e.toBasis.adjustToOrientation_apply_eq_or_eq_neg x i

Result:
no goals
-- Mathlib/Geometry/Manifold/MFDeriv/Basic.lean
theorem mdifferentiableAt_iff_of_mem_source {x' : M} {y : M'} (hx : x' ∈ (chartAt H x).source)
    (hy : f x' ∈ (chartAt H' y).source) :
    MDifferentiableAt I I' f x' ↔
      ContinuousAt f x' ∧
        DifferentiableWithinAt 𝕜 (extChartAt I' y ∘ f ∘ (extChartAt I x).symm) (range I)
          (extChartAt I x x') :=
  (mdifferentiableWithinAt_iff_of_mem_source hx hy).trans <| by
    rw [continuousWithinAt_univ, preimage_univ, univ_inter]

Proof state:
𝕜 : Type u_1
inst✝¹² : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁹ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁸ : TopologicalSpace M
inst✝⁷ : ChartedSpace H M
E' : Type u_5
inst✝⁶ : NormedAddCommGroup E'
inst✝⁵ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝⁴ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝³ : TopologicalSpace M'
inst✝² : ChartedSpace H' M'
f : M → M'
x : M
inst✝¹ : IsManifold I 1 M
inst✝ : IsManifold I' 1 M'
x' : M
y : M'
hx : x' ∈ (chartAt H x).source
hy : f x' ∈ (chartAt H' y).source
⊢ ContinuousWithinAt f univ x' ∧
      DifferentiableWithinAt 𝕜 (↑(extChartAt I' y) ∘ f ∘ ↑(extChartAt I x).symm)
        (↑(extChartAt I x).symm ⁻¹' univ ∩ range ↑I) (↑(extChartAt I x) x') ↔
    ContinuousAt f x' ∧
      DifferentiableWithinAt 𝕜 (↑(extChartAt I' y) ∘ f ∘ ↑(extChartAt I x).symm) (range ↑I) (↑(extChartAt I x) x')

Tactic:
rw [continuousWithinAt_univ, preimage_univ, univ_inter]

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/NormalForms.lean
theorem b₄_of_isCharThreeJNeZeroNF : W.b₄ = 0

Proof state:
R : Type u_1
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : W.IsCharThreeJNeZeroNF
⊢ W.b₄ = 0

Tactic:
simp

Result:
no goals