harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/Distribution/SchwartzSpace.lean
lemma integrable_pow_neg_integrablePower
    (μ : Measure D) [h : μ.HasTemperateGrowth] :
    Integrable (fun x ↦ (1 + ‖x‖) ^ (- (μ.integrablePower : ℝ))) μ

Proof state:
D : Type u_3
inst✝¹ : NormedAddCommGroup D
inst✝ : MeasurableSpace D
μ : Measure D
h : μ.HasTemperateGrowth
⊢ Integrable (fun x => (1 + ‖x‖) ^ (-↑μ.integrablePower)) μ

Tactic:
simpa [Measure.integrablePower, h] using h.exists_integrable.choose_spec

Result:
no goals
-- Mathlib/Analysis/Normed/Field/Basic.lean
theorem punctured_nhds_neBot (x : α) : NeBot (𝓝[≠] x)

Proof state:
case intro.intro
α : Type u_2
inst✝ : NontriviallyNormedField α
x : α
ε : ℝ
ε0 : ε > 0
b : α
hb0 : 0 < ‖b‖
hbε : ‖b‖ < ε
⊢ ∃ b ∈ {x}ᶜ, dist x b < ε

Tactic:
refine ⟨x + b, mt (Set.mem_singleton_iff.trans add_right_eq_self).1 <| norm_pos_iff.1 hb0, ?_⟩

Result:
case intro.intro
α : Type u_2
inst✝ : NontriviallyNormedField α
x : α
ε : ℝ
ε0 : ε > 0
b : α
hb0 : 0 < ‖b‖
hbε : ‖b‖ < ε
⊢ dist x (x + b) < ε

Proof state:
α : Type u_2
inst✝ : NontriviallyNormedField α
x : α
⊢ (𝓝[≠] x).NeBot

Tactic:
rw [← mem_closure_iff_nhdsWithin_neBot, Metric.mem_closure_iff]

Result:
α : Type u_2
inst✝ : NontriviallyNormedField α
x : α
⊢ ∀ ε > 0, ∃ b ∈ {x}ᶜ, dist x b < ε

Proof state:
case intro.intro
α : Type u_2
inst✝ : NontriviallyNormedField α
x : α
ε : ℝ
ε0 : ε > 0
b : α
hb0 : 0 < ‖b‖
hbε : ‖b‖ < ε
⊢ dist x (x + b) < ε

Tactic:
rwa [dist_comm, dist_eq_norm, add_sub_cancel_left]

Result:
no goals

Proof state:
α : Type u_2
inst✝ : NontriviallyNormedField α
x : α
ε : ℝ
ε0 : ε > 0
⊢ ∃ b ∈ {x}ᶜ, dist x b < ε

Tactic:
rcases exists_norm_lt α ε0 with ⟨b, hb0, hbε⟩

Result:
case intro.intro
α : Type u_2
inst✝ : NontriviallyNormedField α
x : α
ε : ℝ
ε0 : ε > 0
b : α
hb0 : 0 < ‖b‖
hbε : ‖b‖ < ε
⊢ ∃ b ∈ {x}ᶜ, dist x b < ε

Proof state:
α : Type u_2
inst✝ : NontriviallyNormedField α
x : α
⊢ ∀ ε > 0, ∃ b ∈ {x}ᶜ, dist x b < ε

Tactic:
rintro ε ε0

Result:
α : Type u_2
inst✝ : NontriviallyNormedField α
x : α
ε : ℝ
ε0 : ε > 0
⊢ ∃ b ∈ {x}ᶜ, dist x b < ε
-- Mathlib/Data/Complex/Module.lean
lemma Complex.coe_realPart (z : ℂ) : (ℜ z : ℂ) = z.re := calc
  (ℜ z : ℂ) = (↑(ℜ (↑z.re + ↑z.im * I)))

Proof state:
z : ℂ
⊢ ↑(ℜ ↑z.re) + ↑(-ℑ ↑z.im) = ↑z.re

Tactic:
simp [conj_ofReal, ← two_mul]

Result:
no goals

Proof state:
z : ℂ
⊢ ↑(ℜ z) = ↑(ℜ (↑z.re + ↑z.im * I))

Tactic:
congrm (ℜ $((re_add_im z).symm))

Result:
no goals

Proof state:
z : ℂ
⊢ ↑(ℜ (↑z.re + ↑z.im * I)) = ↑z.re

Tactic:
rw [map_add, AddSubmonoid.coe_add, mul_comm, ← smul_eq_mul, realPart_I_smul]

Result:
z : ℂ
⊢ ↑(ℜ ↑z.re) + ↑(-ℑ ↑z.im) = ↑z.re
-- Mathlib/Algebra/Group/Commute/Defs.lean
theorem left_comm (h : Commute a b) (c) : a * (b * c) = b * (a * c)

Proof state:
S : Type u_3
inst✝ : Semigroup S
a b : S
h : Commute a b
c : S
⊢ a * (b * c) = b * (a * c)

Tactic:
simp only [← mul_assoc, h.eq]

Result:
no goals
-- Mathlib/Control/Functor/Multivariate.lean
theorem LiftR_def (x y : F α) :
    LiftR' R x y ↔
      ∃ u : F (Subtype_ R),
        (TypeVec.prod.fst ⊚ subtypeVal R) <$$> u = x ∧
          (TypeVec.prod.snd ⊚ subtypeVal R) <$$> u = y :=
  exists_iff_exists_of_mono _ _ _ (toSubtype'_of_subtype' R) (by
    simp only [map_map, comp_assoc, subtypeVal_toSubtype']
    simp (config := { unfoldPartialApp := true }) [comp])

Proof state:
n : ℕ
α : TypeVec.{u} n
F : TypeVec.{u} n → Type v
inst✝¹ : MvFunctor F
R : α ⊗ α ⟹ TypeVec.repeat n Prop
inst✝ : LawfulMvFunctor F
x y : F α
⊢ ∀ (u : F fun i => { p // (fun i x y => ofRepeat (R i (prod.mk i x y))) i p.1 p.2 }),
    (fun i t => (↑t).1) <$$> u = x ∧ (fun i t => (↑t).2) <$$> u = y ↔
      (prod.fst ⊚ subtypeVal R) <$$> toSubtype' R <$$> u = x ∧ (prod.snd ⊚ subtypeVal R) <$$> toSubtype' R <$$> u = y

Tactic:
simp only [map_map, comp_assoc, subtypeVal_toSubtype']

Result:
n : ℕ
α : TypeVec.{u} n
F : TypeVec.{u} n → Type v
inst✝¹ : MvFunctor F
R : α ⊗ α ⟹ TypeVec.repeat n Prop
inst✝ : LawfulMvFunctor F
x y : F α
⊢ ∀ (u : F fun i => { p // ofRepeat (R i (prod.mk i p.1 p.2)) }),
    (fun i t => (↑t).1) <$$> u = x ∧ (fun i t => (↑t).2) <$$> u = y ↔
      (prod.fst ⊚ fun i x => prod.mk i (↑x).1 (↑x).2) <$$> u = x ∧
        (prod.snd ⊚ fun i x => prod.mk i (↑x).1 (↑x).2) <$$> u = y

Proof state:
n : ℕ
α : TypeVec.{u} n
F : TypeVec.{u} n → Type v
inst✝¹ : MvFunctor F
R : α ⊗ α ⟹ TypeVec.repeat n Prop
inst✝ : LawfulMvFunctor F
x y : F α
⊢ ∀ (u : F fun i => { p // ofRepeat (R i (prod.mk i p.1 p.2)) }),
    (fun i t => (↑t).1) <$$> u = x ∧ (fun i t => (↑t).2) <$$> u = y ↔
      (prod.fst ⊚ fun i x => prod.mk i (↑x).1 (↑x).2) <$$> u = x ∧
        (prod.snd ⊚ fun i x => prod.mk i (↑x).1 (↑x).2) <$$> u = y

Tactic:
simp (config := { unfoldPartialApp := true }) [comp]

Result:
no goals
-- Mathlib/Data/Nat/PartENat.lean
theorem lt_add_iff_pos_right {x y : PartENat} (hx : x ≠ ⊤) : x < x + y ↔ 0 < y

Proof state:
x y : PartENat
hx : x ≠ ⊤
⊢ x < x + y ↔ x + 0 < x + y

Tactic:
rw [add_zero]

Result:
no goals

Proof state:
x y : PartENat
hx : x ≠ ⊤
⊢ x < x + y ↔ 0 < y

Tactic:
conv_rhs => rw [← PartENat.add_lt_add_iff_left hx]

Result:
x y : PartENat
hx : x ≠ ⊤
⊢ x < x + y ↔ x + 0 < x + y
-- Mathlib/Data/Set/Image.lean
theorem preimage_eq_univ_iff {f : α → β} {s} : f ⁻¹' s = univ ↔ range f ⊆ s

Proof state:
α : Type u_1
β : Type u_2
f : α → β
s : Set β
⊢ f ⁻¹' s = univ ↔ range f ⊆ s

Tactic:
rw [← univ_subset_iff, ← image_subset_iff, image_univ]

Result:
no goals
-- Mathlib/Data/Nat/Factorial/Basic.lean
lemma factorial_two_mul_le (n : ℕ) : (2 * n)! ≤ (2 * n) ^ n * n !

Proof state:
n : ℕ
⊢ (2 * n)! ≤ (2 * n) ^ n * n !

Tactic:
rw [Nat.two_mul, ← factorial_mul_ascFactorial, Nat.mul_comm]

Result:
n : ℕ
⊢ (n + 1).ascFactorial n * n ! ≤ (n + n) ^ n * n !

Proof state:
n : ℕ
⊢ (n + 1).ascFactorial n * n ! ≤ (n + n) ^ n * n !

Tactic:
exact Nat.mul_le_mul_right _ (ascFactorial_le_pow_add _ _)

Result:
no goals
-- Mathlib/Data/List/Basic.lean
theorem length_erase_add_one {a : α} {l : List α} (h : a ∈ l) :
    (l.erase a).length + 1 = l.length

Proof state:
α : Type u
inst✝ : DecidableEq α
a : α
l : List α
h : a ∈ l
⊢ (l.erase a).length + 1 = l.length

Tactic:
rw [erase_eq_eraseP, length_eraseP_add_one h (decide_eq_true rfl)]

Result:
no goals
-- Mathlib/Topology/Order/LeftRightNhds.lean
theorem mem_nhdsLE_iff_exists_Icc_subset [NoMinOrder α] [DenselyOrdered α] {a : α}
    {s : Set α} : s ∈ 𝓝[≤] a ↔ ∃ l, l < a ∧ Icc l a ⊆ s :=
  calc s ∈ 𝓝[≤] a ↔ ofDual ⁻¹' s ∈ 𝓝[≥] (toDual a) := Iff.rfl
  _ ↔ ∃ u : α, toDual a < toDual u ∧ Icc (toDual a) (toDual u) ⊆ ofDual ⁻¹' s :=
    mem_nhdsGE_iff_exists_Icc_subset
  _ ↔ ∃ l, l < a ∧ Icc l a ⊆ s

Proof state:
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : NoMinOrder α
inst✝ : DenselyOrdered α
a : α
s : Set α
⊢ (∃ u, toDual a < toDual u ∧ Icc (toDual a) (toDual u) ⊆ ⇑ofDual ⁻¹' s) ↔ ∃ l < a, Icc l a ⊆ s

Tactic:
simp only [dual_Icc]

Result:
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : NoMinOrder α
inst✝ : DenselyOrdered α
a : α
s : Set α
⊢ (∃ u, toDual a < toDual u ∧ ⇑ofDual ⁻¹' Icc u a ⊆ ⇑ofDual ⁻¹' s) ↔ ∃ l < a, Icc l a ⊆ s

Proof state:
α : Type u_1
inst✝⁴ : TopologicalSpace α
inst✝³ : LinearOrder α
inst✝² : OrderTopology α
inst✝¹ : NoMinOrder α
inst✝ : DenselyOrdered α
a : α
s : Set α
⊢ (∃ u, toDual a < toDual u ∧ ⇑ofDual ⁻¹' Icc u a ⊆ ⇑ofDual ⁻¹' s) ↔ ∃ l < a, Icc l a ⊆ s

Tactic:
rfl

Result:
no goals
-- Mathlib/Analysis/Calculus/FDeriv/Add.lean
theorem HasStrictFDerivAt.const_sub (hf : HasStrictFDerivAt f f' x) (c : F) :
    HasStrictFDerivAt (fun x => c - f x) (-f') 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
f : E → F
f' : E →L[𝕜] F
x : E
hf : HasStrictFDerivAt f f' x
c : F
⊢ HasStrictFDerivAt (fun x => c - f x) (-f') x

Tactic:
simpa only [sub_eq_add_neg] using hf.neg.const_add c

Result:
no goals
-- Mathlib/SetTheory/Cardinal/HasCardinalLT.lean
lemma of_injective (f : Y → X) (hf : Function.Injective f) :
    HasCardinalLT Y κ

Proof state:
X : Type u
κ : Cardinal.{v}
h : Cardinal.lift.{max v u', u} (Cardinal.mk X) < Cardinal.lift.{max u u', v} κ
Y : Type u'
f : Y → X
hf : Function.Injective f
⊢ Cardinal.lift.{max v u, u'} (Cardinal.mk Y) < Cardinal.lift.{max u' u, v} κ

Tactic:
exact lt_of_le_of_lt (Cardinal.mk_le_of_injective
  (Function.Injective.comp ULift.up_injective
    (Function.Injective.comp hf ULift.down_injective))) h

Result:
no goals

Proof state:
X : Type u
κ : Cardinal.{v}
h : Cardinal.lift.{v, u} (Cardinal.mk X) < Cardinal.lift.{u, v} κ
Y : Type u'
f : Y → X
hf : Function.Injective f
⊢ Cardinal.lift.{v, u'} (Cardinal.mk Y) < Cardinal.lift.{u', v} κ

Tactic:
rw [← Cardinal.lift_lt.{_, u}, Cardinal.lift_lift, Cardinal.lift_lift]

Result:
X : Type u
κ : Cardinal.{v}
h : Cardinal.lift.{v, u} (Cardinal.mk X) < Cardinal.lift.{u, v} κ
Y : Type u'
f : Y → X
hf : Function.Injective f
⊢ Cardinal.lift.{max v u, u'} (Cardinal.mk Y) < Cardinal.lift.{max u' u, v} κ

Proof state:
X : Type u
κ : Cardinal.{v}
h : Cardinal.lift.{v, u} (Cardinal.mk X) < Cardinal.lift.{u, v} κ
Y : Type u'
f : Y → X
hf : Function.Injective f
⊢ Cardinal.lift.{max v u, u'} (Cardinal.mk Y) < Cardinal.lift.{max u' u, v} κ

Tactic:
rw [← Cardinal.lift_lt.{_, u'}, Cardinal.lift_lift, Cardinal.lift_lift] at h

Result:
X : Type u
κ : Cardinal.{v}
h : Cardinal.lift.{max v u', u} (Cardinal.mk X) < Cardinal.lift.{max u u', v} κ
Y : Type u'
f : Y → X
hf : Function.Injective f
⊢ Cardinal.lift.{max v u, u'} (Cardinal.mk Y) < Cardinal.lift.{max u' u, v} κ

Proof state:
X : Type u
κ : Cardinal.{v}
h : HasCardinalLT X κ
Y : Type u'
f : Y → X
hf : Function.Injective f
⊢ HasCardinalLT Y κ

Tactic:
dsimp [HasCardinalLT] at h ⊢

Result:
X : Type u
κ : Cardinal.{v}
h : Cardinal.lift.{v, u} (Cardinal.mk X) < Cardinal.lift.{u, v} κ
Y : Type u'
f : Y → X
hf : Function.Injective f
⊢ Cardinal.lift.{v, u'} (Cardinal.mk Y) < Cardinal.lift.{u', v} κ
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem mapM_eq_mapM_toList [Monad m] [LawfulMonad m] (f : α → m β) (arr : Array α) :
    arr.mapM f = List.toArray <$> (arr.toList.mapM f)

Proof state:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → m β
arr : Array α
⊢ List.foldrM (fun a bs => bs.push <$> f a) #[] arr.toList.reverse =
    List.toArray <$> List.mapM f arr.toList.reverse.reverse

Tactic:
induction arr.toList.reverse with
| nil => simp
| cons a l ih => simp [ih]

Result:
no goals

Proof state:
case nil
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → m β
arr : Array α
⊢ List.foldrM (fun a bs => bs.push <$> f a) #[] [] = List.toArray <$> List.mapM f [].reverse

Tactic:
simp

Result:
no goals

Proof state:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → m β
arr : Array α
⊢ mapM f arr = List.toArray <$> List.mapM f arr.toList

Tactic:
rw [mapM_eq_foldlM, ← foldlM_toList, ← List.foldrM_reverse]

Result:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → m β
arr : Array α
⊢ List.foldrM (fun a bs => bs.push <$> f a) #[] arr.toList.reverse = List.toArray <$> List.mapM f arr.toList

Proof state:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → m β
arr : Array α
⊢ List.foldrM (fun a bs => bs.push <$> f a) #[] arr.toList.reverse = List.toArray <$> List.mapM f arr.toList

Tactic:
conv => rhs; rw [← List.reverse_reverse arr.toList]

Result:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → m β
arr : Array α
⊢ List.foldrM (fun a bs => bs.push <$> f a) #[] arr.toList.reverse =
    List.toArray <$> List.mapM f arr.toList.reverse.reverse

Proof state:
case cons
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f : α → m β
arr : Array α
a : α
l : List α
ih : List.foldrM (fun a bs => bs.push <$> f a) #[] l = List.toArray <$> List.mapM f l.reverse
⊢ List.foldrM (fun a bs => bs.push <$> f a) #[] (a :: l) = List.toArray <$> List.mapM f (a :: l).reverse

Tactic:
simp [ih]

Result:
no goals
-- Mathlib/Analysis/Normed/Operator/LinearIsometry.lean
theorem coe_injective : @Injective (E →ₛₗᵢ[σ₁₂] E₂) (E → E₂) (fun f => f)

Proof state:
R : Type u_1
R₂ : Type u_2
E : Type u_5
E₂ : Type u_6
inst✝⁵ : Semiring R
inst✝⁴ : Semiring R₂
σ₁₂ : R →+* R₂
inst✝³ : SeminormedAddCommGroup E
inst✝² : SeminormedAddCommGroup E₂
inst✝¹ : Module R E
inst✝ : Module R₂ E₂
⊢ Injective fun f => ⇑f

Tactic:
rintro ⟨_⟩ ⟨_⟩

Result:
case mk.mk
R : Type u_1
R₂ : Type u_2
E : Type u_5
E₂ : Type u_6
inst✝⁵ : Semiring R
inst✝⁴ : Semiring R₂
σ₁₂ : R →+* R₂
inst✝³ : SeminormedAddCommGroup E
inst✝² : SeminormedAddCommGroup E₂
inst✝¹ : Module R E
inst✝ : Module R₂ E₂
toLinearMap✝¹ : E →ₛₗ[σ₁₂] E₂
norm_map'✝¹ : ∀ (x : E), ‖toLinearMap✝¹ x‖ = ‖x‖
toLinearMap✝ : E →ₛₗ[σ₁₂] E₂
norm_map'✝ : ∀ (x : E), ‖toLinearMap✝ x‖ = ‖x‖
⊢ (fun f => ⇑f) { toLinearMap := toLinearMap✝¹, norm_map' := norm_map'✝¹ } =
      (fun f => ⇑f) { toLinearMap := toLinearMap✝, norm_map' := norm_map'✝ } →
    { toLinearMap := toLinearMap✝¹, norm_map' := norm_map'✝¹ } =
      { toLinearMap := toLinearMap✝, norm_map' := norm_map'✝ }

Proof state:
case mk.mk
R : Type u_1
R₂ : Type u_2
E : Type u_5
E₂ : Type u_6
inst✝⁵ : Semiring R
inst✝⁴ : Semiring R₂
σ₁₂ : R →+* R₂
inst✝³ : SeminormedAddCommGroup E
inst✝² : SeminormedAddCommGroup E₂
inst✝¹ : Module R E
inst✝ : Module R₂ E₂
toLinearMap✝¹ : E →ₛₗ[σ₁₂] E₂
norm_map'✝¹ : ∀ (x : E), ‖toLinearMap✝¹ x‖ = ‖x‖
toLinearMap✝ : E →ₛₗ[σ₁₂] E₂
norm_map'✝ : ∀ (x : E), ‖toLinearMap✝ x‖ = ‖x‖
⊢ (fun f => ⇑f) { toLinearMap := toLinearMap✝¹, norm_map' := norm_map'✝¹ } =
      (fun f => ⇑f) { toLinearMap := toLinearMap✝, norm_map' := norm_map'✝ } →
    { toLinearMap := toLinearMap✝¹, norm_map' := norm_map'✝¹ } =
      { toLinearMap := toLinearMap✝, norm_map' := norm_map'✝ }

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/Matrix.lean
theorem norm_unitOf (a : α) : ‖unitOf a‖₊ = 1

Proof state:
case pos
α : Type u_5
inst✝¹ : NormedDivisionRing α
inst✝ : NormedAlgebra ℝ α
a : α
h : a = 0
⊢ ‖1‖₊ = 1

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_5
inst✝¹ : NormedDivisionRing α
inst✝ : NormedAlgebra ℝ α
a : α
⊢ ‖Matrix.unitOf a‖₊ = 1

Tactic:
rw [unitOf]

Result:
α : Type u_5
inst✝¹ : NormedDivisionRing α
inst✝ : NormedAlgebra ℝ α
a : α
⊢ ‖if a = 0 then 1 else ‖a‖ • a⁻¹‖₊ = 1

Proof state:
case neg
α : Type u_5
inst✝¹ : NormedDivisionRing α
inst✝ : NormedAlgebra ℝ α
a : α
h : ¬a = 0
⊢ ‖‖a‖ • a⁻¹‖₊ = 1

Tactic:
rw [← nnnorm_eq_zero] at h

Result:
case neg
α : Type u_5
inst✝¹ : NormedDivisionRing α
inst✝ : NormedAlgebra ℝ α
a : α
h : ¬‖a‖₊ = 0
⊢ ‖‖a‖ • a⁻¹‖₊ = 1

Proof state:
case neg
α : Type u_5
inst✝¹ : NormedDivisionRing α
inst✝ : NormedAlgebra ℝ α
a : α
h : ¬‖a‖₊ = 0
⊢ ‖‖a‖ • a⁻¹‖₊ = 1

Tactic:
rw [nnnorm_smul, nnnorm_inv, nnnorm_norm, mul_inv_cancel₀ h]

Result:
no goals

Proof state:
α : Type u_5
inst✝¹ : NormedDivisionRing α
inst✝ : NormedAlgebra ℝ α
a : α
⊢ ‖if a = 0 then 1 else ‖a‖ • a⁻¹‖₊ = 1

Tactic:
split_ifs with h

Result:
case pos
α : Type u_5
inst✝¹ : NormedDivisionRing α
inst✝ : NormedAlgebra ℝ α
a : α
h : a = 0
⊢ ‖1‖₊ = 1

case neg
α : Type u_5
inst✝¹ : NormedDivisionRing α
inst✝ : NormedAlgebra ℝ α
a : α
h : ¬a = 0
⊢ ‖‖a‖ • a⁻¹‖₊ = 1
-- Mathlib/Data/Finset/Lattice/Fold.lean
theorem disjoint_sup_left : Disjoint (s.sup f) a ↔ ∀ ⦃i⦄, i ∈ s → Disjoint (f i) a

Proof state:
α : Type u_2
ι : Type u_5
inst✝¹ : DistribLattice α
inst✝ : OrderBot α
s : Finset ι
f : ι → α
a : α
⊢ Disjoint (s.sup f) a ↔ ∀ ⦃i : ι⦄, i ∈ s → Disjoint (f i) a

Tactic:
simp only [disjoint_iff, sup_inf_distrib_right, Finset.sup_eq_bot_iff]

Result:
no goals
-- Mathlib/RingTheory/MvPolynomial/WeightedHomogeneous.lean
theorem weightedHomogeneousComponent_of_isWeightedHomogeneous_same
    {m : M} {p : MvPolynomial σ R} (hp : IsWeightedHomogeneous w p m) :
    weightedHomogeneousComponent w m p = p

Proof state:
case pos
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
σ : Type u_3
inst✝ : AddCommMonoid M
w : σ → M
m : M
p : MvPolynomial σ R
hp : IsWeightedHomogeneous w p m
x : σ →₀ ℕ
zero_coeff : coeff x p = 0
⊢ (if (weight w) x = m then coeff x p else 0) = coeff x p

Tactic:
simp [zero_coeff]

Result:
no goals

Proof state:
case a
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
σ : Type u_3
inst✝ : AddCommMonoid M
w : σ → M
m : M
p : MvPolynomial σ R
hp : IsWeightedHomogeneous w p m
x : σ →₀ ℕ
⊢ coeff x ((weightedHomogeneousComponent w m) p) = coeff x p

Tactic:
rw [coeff_weightedHomogeneousComponent]

Result:
case a
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
σ : Type u_3
inst✝ : AddCommMonoid M
w : σ → M
m : M
p : MvPolynomial σ R
hp : IsWeightedHomogeneous w p m
x : σ →₀ ℕ
⊢ (if (weight w) x = m then coeff x p else 0) = coeff x p

Proof state:
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
σ : Type u_3
inst✝ : AddCommMonoid M
w : σ → M
m : M
p : MvPolynomial σ R
hp : IsWeightedHomogeneous w p m
⊢ (weightedHomogeneousComponent w m) p = p

Tactic:
ext x

Result:
case a
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
σ : Type u_3
inst✝ : AddCommMonoid M
w : σ → M
m : M
p : MvPolynomial σ R
hp : IsWeightedHomogeneous w p m
x : σ →₀ ℕ
⊢ coeff x ((weightedHomogeneousComponent w m) p) = coeff x p

Proof state:
case neg
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
σ : Type u_3
inst✝ : AddCommMonoid M
w : σ → M
m : M
p : MvPolynomial σ R
hp : IsWeightedHomogeneous w p m
x : σ →₀ ℕ
zero_coeff : ¬coeff x p = 0
⊢ (if (weight w) x = m then coeff x p else 0) = coeff x p

Tactic:
rw [hp zero_coeff, if_pos rfl]

Result:
no goals

Proof state:
case a
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
σ : Type u_3
inst✝ : AddCommMonoid M
w : σ → M
m : M
p : MvPolynomial σ R
hp : IsWeightedHomogeneous w p m
x : σ →₀ ℕ
⊢ (if (weight w) x = m then coeff x p else 0) = coeff x p

Tactic:
by_cases zero_coeff : coeff x p = 0

Result:
case pos
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
σ : Type u_3
inst✝ : AddCommMonoid M
w : σ → M
m : M
p : MvPolynomial σ R
hp : IsWeightedHomogeneous w p m
x : σ →₀ ℕ
zero_coeff : coeff x p = 0
⊢ (if (weight w) x = m then coeff x p else 0) = coeff x p

case neg
R : Type u_1
M : Type u_2
inst✝¹ : CommSemiring R
σ : Type u_3
inst✝ : AddCommMonoid M
w : σ → M
m : M
p : MvPolynomial σ R
hp : IsWeightedHomogeneous w p m
x : σ →₀ ℕ
zero_coeff : ¬coeff x p = 0
⊢ (if (weight w) x = m then coeff x p else 0) = coeff x p
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem setIfInBounds_append_left {s : Vector α n} {t : Vector α m} {i : Nat} {x : α} (h : i < n) :
    (s ++ t).setIfInBounds i x = s.setIfInBounds i x ++ t

Proof state:
α : Type u_1
n m : Nat
s : Vector α n
t : Vector α m
i : Nat
x : α
h : i < n
⊢ (s ++ t).setIfInBounds i x = s.setIfInBounds i x ++ t

Tactic:
simp [setIfInBounds_append, h]

Result:
no goals
-- Mathlib/NumberTheory/LSeries/ZMod.lean
/-- The L-function of an even function vanishes at negative even integers. -/
@[simp] lemma LFunction_neg_two_mul_nat_add_one (hΦ : Φ.Even) (n : ℕ) :
    LFunction Φ (-(2 * (n + 1))) = 0

Proof state:
N : ℕ
inst✝ : NeZero N
Φ : ZMod N → ℂ
hΦ : Function.Even Φ
n : ℕ
⊢ LFunction Φ (-(2 * (↑n + 1))) = 0

Tactic:
simp only [LFunction_def_even hΦ, hurwitzZetaEven_neg_two_mul_nat_add_one, mul_zero,
  sum_const_zero, ← neg_mul]

Result:
no goals
-- Mathlib/CategoryTheory/MorphismProperty/Limits.lean
lemma IsStableUnderColimitsOfShape.isomorphisms :
    (isomorphisms C).IsStableUnderColimitsOfShape J

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
J : Type u_1
inst✝ : Category.{u_2, u_1} J
F₁ F₂ : J ⥤ C
c₁ : Cocone F₁
c₂ : Cocone F₂
h₁ : IsColimit c₁
h₂ : IsColimit c₂
f : F₁ ⟶ F₂
x✝ : ∀ (j : J), IsIso (f.app j)
this : IsIso f
⊢ ∀ (j : J),
    c₁.ι.app j ≫ h₁.desc { pt := c₂.pt, ι := f ≫ c₂.ι } ≫ h₂.desc { pt := c₁.pt, ι := inv f ≫ c₁.ι } =
      c₁.ι.app j ≫ 𝟙 c₁.pt

Tactic:
simp

Result:
no goals

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
J : Type u_1
inst✝ : Category.{u_2, u_1} J
⊢ (MorphismProperty.isomorphisms C).IsStableUnderColimitsOfShape J

Tactic:
intro F₁ F₂ c₁ c₂ h₁ h₂ f (_ : ∀ j, IsIso (f.app j))

Result:
C : Type u
inst✝¹ : Category.{v, u} C
J : Type u_1
inst✝ : Category.{u_2, u_1} J
F₁ F₂ : J ⥤ C
c₁ : Cocone F₁
c₂ : Cocone F₂
h₁ : IsColimit c₁
h₂ : IsColimit c₂
f : F₁ ⟶ F₂
x✝ : ∀ (j : J), IsIso (f.app j)
⊢ MorphismProperty.isomorphisms C (h₁.desc { pt := c₂.pt, ι := f ≫ c₂.ι })

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
J : Type u_1
inst✝ : Category.{u_2, u_1} J
F₁ F₂ : J ⥤ C
c₁ : Cocone F₁
c₂ : Cocone F₂
h₁ : IsColimit c₁
h₂ : IsColimit c₂
f : F₁ ⟶ F₂
x✝ : ∀ (j : J), IsIso (f.app j)
⊢ MorphismProperty.isomorphisms C (h₁.desc { pt := c₂.pt, ι := f ≫ c₂.ι })

Tactic:
have := NatIso.isIso_of_isIso_app f

Result:
C : Type u
inst✝¹ : Category.{v, u} C
J : Type u_1
inst✝ : Category.{u_2, u_1} J
F₁ F₂ : J ⥤ C
c₁ : Cocone F₁
c₂ : Cocone F₂
h₁ : IsColimit c₁
h₂ : IsColimit c₂
f : F₁ ⟶ F₂
x✝ : ∀ (j : J), IsIso (f.app j)
this : IsIso f
⊢ MorphismProperty.isomorphisms C (h₁.desc { pt := c₂.pt, ι := f ≫ c₂.ι })

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
J : Type u_1
inst✝ : Category.{u_2, u_1} J
F₁ F₂ : J ⥤ C
c₁ : Cocone F₁
c₂ : Cocone F₂
h₁ : IsColimit c₁
h₂ : IsColimit c₂
f : F₁ ⟶ F₂
x✝ : ∀ (j : J), IsIso (f.app j)
this : IsIso f
⊢ ∀ (j : J),
    c₂.ι.app j ≫ h₂.desc { pt := c₁.pt, ι := inv f ≫ c₁.ι } ≫ h₁.desc { pt := c₂.pt, ι := f ≫ c₂.ι } =
      c₂.ι.app j ≫ 𝟙 { pt := c₂.pt, ι := f ≫ c₂.ι }.pt

Tactic:
simp

Result:
no goals

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
J : Type u_1
inst✝ : Category.{u_2, u_1} J
F₁ F₂ : J ⥤ C
c₁ : Cocone F₁
c₂ : Cocone F₂
h₁ : IsColimit c₁
h₂ : IsColimit c₂
f : F₁ ⟶ F₂
x✝ : ∀ (j : J), IsIso (f.app j)
this : IsIso f
⊢ MorphismProperty.isomorphisms C (h₁.desc { pt := c₂.pt, ι := f ≫ c₂.ι })

Tactic:
exact ⟨h₂.desc (Cocone.mk _ (inv f ≫ c₁.ι)),
  h₁.hom_ext (by simp), h₂.hom_ext (by simp)⟩

Result:
no goals