harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/RingTheory/PowerSeries/Basic.lean
theorem rescale_injective {a : R} (ha : a ≠ 0) : Function.Injective (rescale a)

Proof state:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
a : R
ha : a ≠ 0
p q : R⟦X⟧
n : ℕ
h : (coeff R n) p = (coeff R n) q ∨ a ^ n = 0
⊢ ¬a ^ n = 0

Tactic:
intro h'

Result:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
a : R
ha : a ≠ 0
p q : R⟦X⟧
n : ℕ
h : (coeff R n) p = (coeff R n) q ∨ a ^ n = 0
h' : a ^ n = 0
⊢ False

Proof state:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
a : R
ha : a ≠ 0
p q : R⟦X⟧
h : (rescale a) p = (rescale a) q
⊢ p = q

Tactic:
rw [PowerSeries.ext_iff] at *

Result:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
a : R
ha : a ≠ 0
p q : R⟦X⟧
h : ∀ (n : ℕ), (coeff R n) ((rescale a) p) = (coeff R n) ((rescale a) q)
⊢ ∀ (n : ℕ), (coeff R n) p = (coeff R n) q

Proof state:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
a : R
ha : a ≠ 0
p q : R⟦X⟧
h : ∀ (n : ℕ), (coeff R n) ((rescale a) p) = (coeff R n) ((rescale a) q)
⊢ ∀ (n : ℕ), (coeff R n) p = (coeff R n) q

Tactic:
intro n

Result:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
a : R
ha : a ≠ 0
p q : R⟦X⟧
h : ∀ (n : ℕ), (coeff R n) ((rescale a) p) = (coeff R n) ((rescale a) q)
n : ℕ
⊢ (coeff R n) p = (coeff R n) q

Proof state:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
a : R
ha : a ≠ 0
p q : R⟦X⟧
n : ℕ
h : (coeff R n) p = (coeff R n) q ∨ a ^ n = 0
h' : a ^ n = 0
⊢ False

Tactic:
exact ha (pow_eq_zero h')

Result:
no goals

Proof state:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
a : R
ha : a ≠ 0
p q : R⟦X⟧
n : ℕ
h : (coeff R n) ((rescale a) p) = (coeff R n) ((rescale a) q)
⊢ (coeff R n) p = (coeff R n) q

Tactic:
rw [coeff_rescale, coeff_rescale, mul_eq_mul_left_iff] at h

Result:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
a : R
ha : a ≠ 0
p q : R⟦X⟧
n : ℕ
h : (coeff R n) p = (coeff R n) q ∨ a ^ n = 0
⊢ (coeff R n) p = (coeff R n) q

Proof state:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
a : R
ha : a ≠ 0
p q : R⟦X⟧
h : ∀ (n : ℕ), (coeff R n) ((rescale a) p) = (coeff R n) ((rescale a) q)
n : ℕ
⊢ (coeff R n) p = (coeff R n) q

Tactic:
specialize h n

Result:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
a : R
ha : a ≠ 0
p q : R⟦X⟧
n : ℕ
h : (coeff R n) ((rescale a) p) = (coeff R n) ((rescale a) q)
⊢ (coeff R n) p = (coeff R n) q

Proof state:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
a : R
ha : a ≠ 0
p q : R⟦X⟧
n : ℕ
h : (coeff R n) p = (coeff R n) q ∨ a ^ n = 0
⊢ (coeff R n) p = (coeff R n) q

Tactic:
apply h.resolve_right

Result:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
a : R
ha : a ≠ 0
p q : R⟦X⟧
n : ℕ
h : (coeff R n) p = (coeff R n) q ∨ a ^ n = 0
⊢ ¬a ^ n = 0

Proof state:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
a : R
ha : a ≠ 0
⊢ Function.Injective ⇑(rescale a)

Tactic:
intro p q h

Result:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
a : R
ha : a ≠ 0
p q : R⟦X⟧
h : (rescale a) p = (rescale a) q
⊢ p = q
-- Mathlib/CategoryTheory/Triangulated/Pretriangulated.lean
/-- Obvious triangles `0 ⟶ X ⟶ X ⟶ 0⟦1⟧` are distinguished -/
lemma contractible_distinguished₁ (X : C) :
    Triangle.mk (0 : 0 ⟶ X) (𝟙 X) 0 ∈ distTriang C

Proof state:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), (shiftFunctor C n).Additive
hC : Pretriangulated C
X : C
⊢ (Triangle.mk 0 (𝟙 X) 0).mor₁ ≫ (Iso.refl (Triangle.mk 0 (𝟙 X) 0).obj₂).hom =
    (shiftFunctor C (-1)).mapZeroObject.symm.hom ≫ (contractibleTriangle X).invRotate.mor₁

Tactic:
simp

Result:
no goals

Proof state:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), (shiftFunctor C n).Additive
hC : Pretriangulated C
X : C
⊢ Triangle.mk 0 (𝟙 X) 0 ∈ distinguishedTriangles

Tactic:
refine isomorphic_distinguished _
  (inv_rot_of_distTriang _ (contractible_distinguished X)) _ ?_

Result:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), (shiftFunctor C n).Additive
hC : Pretriangulated C
X : C
⊢ Triangle.mk 0 (𝟙 X) 0 ≅ (contractibleTriangle X).invRotate

Proof state:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), (shiftFunctor C n).Additive
hC : Pretriangulated C
X : C
⊢ Triangle.mk 0 (𝟙 X) 0 ≅ (contractibleTriangle X).invRotate

Tactic:
exact Triangle.isoMk _ _ (Functor.mapZeroObject _).symm (Iso.refl _) (Iso.refl _)
  (by simp) (by simp) (by simp)

Result:
no goals

Proof state:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), (shiftFunctor C n).Additive
hC : Pretriangulated C
X : C
⊢ (Triangle.mk 0 (𝟙 X) 0).mor₂ ≫ (Iso.refl (Triangle.mk 0 (𝟙 X) 0).obj₃).hom =
    (Iso.refl (Triangle.mk 0 (𝟙 X) 0).obj₂).hom ≫ (contractibleTriangle X).invRotate.mor₂

Tactic:
simp

Result:
no goals

Proof state:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasZeroObject C
inst✝² : HasShift C ℤ
inst✝¹ : Preadditive C
inst✝ : ∀ (n : ℤ), (shiftFunctor C n).Additive
hC : Pretriangulated C
X : C
⊢ (Triangle.mk 0 (𝟙 X) 0).mor₃ ≫ (shiftFunctor C 1).map (shiftFunctor C (-1)).mapZeroObject.symm.hom =
    (Iso.refl (Triangle.mk 0 (𝟙 X) 0).obj₃).hom ≫ (contractibleTriangle X).invRotate.mor₃

Tactic:
simp

Result:
no goals
-- Mathlib/Order/Interval/Set/Basic.lean
theorem Icc_bot_top [PartialOrder α] [BoundedOrder α] : Icc (⊥ : α) ⊤ = univ

Proof state:
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : BoundedOrder α
⊢ Icc ⊥ ⊤ = univ

Tactic:
simp

Result:
no goals
-- Mathlib/GroupTheory/QuotientGroup/Defs.lean
theorem eq_iff_div_mem {N : Subgroup G} [nN : N.Normal] {x y : G} :
    (x : G ⧸ N) = y ↔ x / y ∈ N

Proof state:
G : Type u
inst✝ : Group G
N : Subgroup G
nN : N.Normal
x y : G
⊢ y⁻¹ * x ∈ N ↔ x / y ∈ N

Tactic:
rw [nN.mem_comm_iff, div_eq_mul_inv]

Result:
no goals

Proof state:
G : Type u
inst✝ : Group G
N : Subgroup G
nN : N.Normal
x y : G
⊢ ↑x = ↑y ↔ x / y ∈ N

Tactic:
refine eq_comm.trans (QuotientGroup.eq.trans ?_)

Result:
G : Type u
inst✝ : Group G
N : Subgroup G
nN : N.Normal
x y : G
⊢ y⁻¹ * x ∈ N ↔ x / y ∈ N
-- Mathlib/MeasureTheory/Function/AEEqOfIntegral.lean
/-- If an integrable function has zero integral on all compact sets in a sigma-compact space, then
it is zero almost everywhere. -/
lemma ae_eq_zero_of_forall_setIntegral_isCompact_eq_zero
    [SigmaCompactSpace β] [R1Space β] {μ : Measure β} {f : β → E} (hf : Integrable f μ)
    (h'f : ∀ (s : Set β), IsCompact s → ∫ x in s, f x ∂μ = 0) :
    f =ᵐ[μ] 0

Proof state:
E : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : CompleteSpace E
β : Type u_3
inst✝⁴ : TopologicalSpace β
inst✝³ : MeasurableSpace β
inst✝² : BorelSpace β
inst✝¹ : SigmaCompactSpace β
inst✝ : R1Space β
μ : Measure β
f : β → E
hf : Integrable f μ
h'f : ∀ (s : Set β), IsCompact s → ∫ (x : β) in s, f x ∂μ = 0
s : Set β
hs : IsClosed s
t : ℕ → Set β := fun n => closure (compactCovering β n) ∩ s
B : s = ⋃ n, t n
⊢ Tendsto (fun n => ∫ (x : β) in t n, f x ∂μ) atTop (𝓝 (∫ (x : β) in ⋃ n, t n, f x ∂μ))

Tactic:
apply tendsto_setIntegral_of_monotone

Result:
case hsm
E : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : CompleteSpace E
β : Type u_3
inst✝⁴ : TopologicalSpace β
inst✝³ : MeasurableSpace β
inst✝² : BorelSpace β
inst✝¹ : SigmaCompactSpace β
inst✝ : R1Space β
μ : Measure β
f : β → E
hf : Integrable f μ
h'f : ∀ (s : Set β), IsCompact s → ∫ (x : β) in s, f x ∂μ = 0
s : Set β
hs : IsClosed s
t : ℕ → Set β := fun n => closure (compactCovering β n) ∩ s
B : s = ⋃ n, t n
⊢ ∀ (i : ℕ), MeasurableSet (t i)

case h_mono
E : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : CompleteSpace E
β : Type u_3
inst✝⁴ : TopologicalSpace β
inst✝³ : MeasurableSpace β
inst✝² : BorelSpace β
inst✝¹ : SigmaCompactSpace β
inst✝ : R1Space β
μ : Measure β
f : β → E
hf : Integrable f μ
h'f : ∀ (s : Set β), IsCompact s → ∫ (x : β) in s, f x ∂μ = 0
s : Set β
hs : IsClosed s
t : ℕ → Set β := fun n => closure (compactCovering β n) ∩ s
B : s = ⋃ n, t n
⊢ Monotone t

case hfi
E : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : CompleteSpace E
β : Type u_3
inst✝⁴ : TopologicalSpace β
inst✝³ : MeasurableSpace β
inst✝² : BorelSpace β
inst✝¹ : SigmaCompactSpace β
inst✝ : R1Space β
μ : Measure β
f : β → E
hf : Integrable f μ
h'f : ∀ (s : Set β), IsCompact s → ∫ (x : β) in s, f x ∂μ = 0
s : Set β
hs : IsClosed s
t : ℕ → Set β := fun n => closure (compactCovering β n) ∩ s
B : s = ⋃ n, t n
⊢ IntegrableOn f (⋃ n, t n) μ

Proof state:
case hsm
E : Type u_2
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedSpace ℝ E
inst✝⁵ : CompleteSpace E
β : Type u_3
inst✝⁴ : TopologicalSpace β
inst✝³ : MeasurableSpace β
inst✝² : BorelSpace β
inst✝¹ : SigmaCompactSpace β
inst✝ : R1Space β
μ : Measure β
f : β → E
hf : Integrable f μ
h'f : ∀ (s : Set β), IsCompact s → ∫ (x : β) in s, f x ∂μ = 0
s : Set β
hs : IsClosed s
t : ℕ → Set β := fun n => closure (compactCovering β n) ∩ s
B : s = ⋃ n, t n
n : ℕ
⊢ MeasurableSet (t n)

Tactic:
exact (isClosed_closure.inter hs).measurableSet

Result:
no goals
-- Mathlib/CategoryTheory/Comma/Presheaf/Basic.lean
@[simp]
lemma map₁_map₂ {G : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v} (η : F ⟶ G) {Y : C} (f : X ⟶ Y)
    (p : YonedaCollection F Y) :
    YonedaCollection.map₂ G f (YonedaCollection.map₁ η p) =
      YonedaCollection.map₁ η (YonedaCollection.map₂ F f p)

Proof state:
case h'
C : Type u
inst✝ : Category.{v, u} C
A : Cᵒᵖ ⥤ Type v
F : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v
X : C
G : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v
η : F ⟶ G
Y : C
f : X ⟶ Y
p : YonedaCollection F Y
⊢ G.map (eqToHom ⋯) (map₁ η (map₂ F f p)).snd = (map₂ G f (map₁ η p)).snd

Tactic:
simp

Result:
no goals

Proof state:
C : Type u
inst✝ : Category.{v, u} C
A : Cᵒᵖ ⥤ Type v
F : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v
X : C
G : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v
η : F ⟶ G
Y : C
f : X ⟶ Y
p : YonedaCollection F Y
⊢ map₂ G f (map₁ η p) = map₁ η (map₂ F f p)

Tactic:
ext

Result:
case h.w.h.h
C : Type u
inst✝ : Category.{v, u} C
A : Cᵒᵖ ⥤ Type v
F : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v
X : C
G : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v
η : F ⟶ G
Y : C
f : X ⟶ Y
p : YonedaCollection F Y
x✝ : Cᵒᵖ
a✝ : (yoneda.obj X).obj x✝
⊢ (map₂ G f (map₁ η p)).fst.app x✝ a✝ = (map₁ η (map₂ F f p)).fst.app x✝ a✝

case h'
C : Type u
inst✝ : Category.{v, u} C
A : Cᵒᵖ ⥤ Type v
F : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v
X : C
G : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v
η : F ⟶ G
Y : C
f : X ⟶ Y
p : YonedaCollection F Y
⊢ G.map (eqToHom ⋯) (map₁ η (map₂ F f p)).snd = (map₂ G f (map₁ η p)).snd

Proof state:
case h.w.h.h
C : Type u
inst✝ : Category.{v, u} C
A : Cᵒᵖ ⥤ Type v
F : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v
X : C
G : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v
η : F ⟶ G
Y : C
f : X ⟶ Y
p : YonedaCollection F Y
x✝ : Cᵒᵖ
a✝ : (yoneda.obj X).obj x✝
⊢ (map₂ G f (map₁ η p)).fst.app x✝ a✝ = (map₁ η (map₂ F f p)).fst.app x✝ a✝

case h'
C : Type u
inst✝ : Category.{v, u} C
A : Cᵒᵖ ⥤ Type v
F : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v
X : C
G : (CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v
η : F ⟶ G
Y : C
f : X ⟶ Y
p : YonedaCollection F Y
⊢ G.map (eqToHom ⋯) (map₁ η (map₂ F f p)).snd = (map₂ G f (map₁ η p)).snd

Tactic:
all_goals simp

Result:
no goals
-- Mathlib/RingTheory/Spectrum/Prime/Topology.lean
@[stacks 00EC]
lemma basicOpen_eq_zeroLocus_of_isIdempotentElem
    (e : R) (he : IsIdempotentElem e) :
    basicOpen e = zeroLocus {1 - e}

Proof state:
case h.mp
R : Type u
inst✝ : CommRing R
e : R
he : IsIdempotentElem e
p : PrimeSpectrum R
⊢ e ∉ p.asIdeal → 1 - e ∈ p.asIdeal

Tactic:
refine (p.2.mem_or_mem_of_mul_eq_zero ?_).resolve_left

Result:
case h.mp
R : Type u
inst✝ : CommRing R
e : R
he : IsIdempotentElem e
p : PrimeSpectrum R
⊢ e * (1 - e) = 0

Proof state:
case h.mpr
R : Type u
inst✝ : CommRing R
e : R
he : IsIdempotentElem e
p : PrimeSpectrum R
⊢ 1 - e ∈ p.asIdeal → e ∉ p.asIdeal

Tactic:
refine fun h₁ h₂ ↦ p.2.1 ?_

Result:
case h.mpr
R : Type u
inst✝ : CommRing R
e : R
he : IsIdempotentElem e
p : PrimeSpectrum R
h₁ : 1 - e ∈ p.asIdeal
h₂ : e ∈ p.asIdeal
⊢ p.asIdeal = ⊤

Proof state:
case h.mpr
R : Type u
inst✝ : CommRing R
e : R
he : IsIdempotentElem e
p : PrimeSpectrum R
h₁ : 1 - e ∈ p.asIdeal
h₂ : e ∈ p.asIdeal
⊢ 1 - e + e ∈ p.asIdeal

Tactic:
exact add_mem h₁ h₂

Result:
no goals

Proof state:
case h.mp
R : Type u
inst✝ : CommRing R
e : R
he : IsIdempotentElem e
p : PrimeSpectrum R
⊢ e * (1 - e) = 0

Tactic:
rw [mul_sub, mul_one, he.eq, sub_self]

Result:
no goals

Proof state:
R : Type u
inst✝ : CommRing R
e : R
he : IsIdempotentElem e
p : PrimeSpectrum R
this : e ∉ p.asIdeal ↔ 1 - e ∈ p.asIdeal
⊢ p ∈ ↑(basicOpen e) ↔ p ∈ zeroLocus {1 - e}

Tactic:
simpa

Result:
no goals

Proof state:
R : Type u
inst✝ : CommRing R
e : R
he : IsIdempotentElem e
⊢ ↑(basicOpen e) = zeroLocus {1 - e}

Tactic:
ext p

Result:
case h
R : Type u
inst✝ : CommRing R
e : R
he : IsIdempotentElem e
p : PrimeSpectrum R
⊢ p ∈ ↑(basicOpen e) ↔ p ∈ zeroLocus {1 - e}

Proof state:
case h.mpr
R : Type u
inst✝ : CommRing R
e : R
he : IsIdempotentElem e
p : PrimeSpectrum R
h₁ : 1 - e ∈ p.asIdeal
h₂ : e ∈ p.asIdeal
⊢ p.asIdeal = ⊤

Tactic:
rw [Ideal.eq_top_iff_one, ← sub_add_cancel 1 e]

Result:
case h.mpr
R : Type u
inst✝ : CommRing R
e : R
he : IsIdempotentElem e
p : PrimeSpectrum R
h₁ : 1 - e ∈ p.asIdeal
h₂ : e ∈ p.asIdeal
⊢ 1 - e + e ∈ p.asIdeal

Proof state:
case h
R : Type u
inst✝ : CommRing R
e : R
he : IsIdempotentElem e
p : PrimeSpectrum R
⊢ e ∉ p.asIdeal ↔ 1 - e ∈ p.asIdeal

Tactic:
constructor

Result:
case h.mp
R : Type u
inst✝ : CommRing R
e : R
he : IsIdempotentElem e
p : PrimeSpectrum R
⊢ e ∉ p.asIdeal → 1 - e ∈ p.asIdeal

case h.mpr
R : Type u
inst✝ : CommRing R
e : R
he : IsIdempotentElem e
p : PrimeSpectrum R
⊢ 1 - e ∈ p.asIdeal → e ∉ p.asIdeal

Proof state:
case h
R : Type u
inst✝ : CommRing R
e : R
he : IsIdempotentElem e
p : PrimeSpectrum R
⊢ p ∈ ↑(basicOpen e) ↔ p ∈ zeroLocus {1 - e}

Tactic:
suffices e ∉ p.asIdeal ↔ 1 - e ∈ p.asIdeal by simpa

Result:
case h
R : Type u
inst✝ : CommRing R
e : R
he : IsIdempotentElem e
p : PrimeSpectrum R
⊢ e ∉ p.asIdeal ↔ 1 - e ∈ p.asIdeal
-- Mathlib/Analysis/MeanInequalities.lean
/-- **Weighted Hölder inequality**. -/
lemma inner_le_weight_mul_Lp_of_nonneg (s : Finset ι) {p : ℝ} (hp : 1 ≤ p) (w f : ι → ℝ)
    (hw : ∀ i, 0 ≤ w i) (hf : ∀ i, 0 ≤ f i) :
    ∑ i ∈ s, w i * f i ≤ (∑ i ∈ s, w i) ^ (1 - p⁻¹) * (∑ i ∈ s, w i * f i ^ p) ^ p⁻¹

Proof state:
case intro.intro
ι : Type u
s : Finset ι
p : ℝ
hp : 1 ≤ p
w f : ι → ℝ≥0
⊢ ∑ i ∈ s, (fun i => ↑(w i)) i * (fun i => ↑(f i)) i ≤
    (∑ i ∈ s, (fun i => ↑(w i)) i) ^ (1 - p⁻¹) * (∑ i ∈ s, (fun i => ↑(w i)) i * (fun i => ↑(f i)) i ^ p) ^ p⁻¹

Tactic:
beta_reduce at *

Result:
case intro.intro
ι : Type u
s : Finset ι
p : ℝ
hp : 1 ≤ p
w f : ι → ℝ≥0
⊢ ∑ i ∈ s, ↑(w i) * ↑(f i) ≤ (∑ i ∈ s, ↑(w i)) ^ (1 - p⁻¹) * (∑ i ∈ s, ↑(w i) * ↑(f i) ^ p) ^ p⁻¹

Proof state:
case intro.intro
ι : Type u
s : Finset ι
p : ℝ
hp : 1 ≤ p
w f : ι → ℝ≥0
⊢ ∑ i ∈ s, ↑(w i) * ↑(f i) ≤ (∑ i ∈ s, ↑(w i)) ^ (1 - p⁻¹) * (∑ i ∈ s, ↑(w i) * ↑(f i) ^ p) ^ p⁻¹

Tactic:
norm_cast at *

Result:
case intro.intro
ι : Type u
s : Finset ι
p : ℝ
w f : ι → ℝ≥0
hp : 1 ≤ p
⊢ ∑ i ∈ s, w i * f i ≤ (∑ i ∈ s, w i) ^ (1 - p⁻¹) * (∑ i ∈ s, w i * f i ^ p) ^ p⁻¹

Proof state:
case intro.intro
ι : Type u
s : Finset ι
p : ℝ
w f : ι → ℝ≥0
hp : 1 ≤ p
⊢ ∑ i ∈ s, w i * f i ≤ (∑ i ∈ s, w i) ^ (1 - p⁻¹) * (∑ i ∈ s, w i * f i ^ p) ^ p⁻¹

Tactic:
exact NNReal.inner_le_weight_mul_Lp _ hp _ _

Result:
no goals

Proof state:
ι : Type u
s : Finset ι
p : ℝ
hp : 1 ≤ p
w f : ι → ℝ
hw : ∀ (i : ι), 0 ≤ w i
hf : ∀ (i : ι), 0 ≤ f i
⊢ ∑ i ∈ s, w i * f i ≤ (∑ i ∈ s, w i) ^ (1 - p⁻¹) * (∑ i ∈ s, w i * f i ^ p) ^ p⁻¹

Tactic:
lift w to ι → ℝ≥0 using hw

Result:
case intro
ι : Type u
s : Finset ι
p : ℝ
hp : 1 ≤ p
f : ι → ℝ
hf : ∀ (i : ι), 0 ≤ f i
w : ι → ℝ≥0
⊢ ∑ i ∈ s, (fun i => ↑(w i)) i * f i ≤
    (∑ i ∈ s, (fun i => ↑(w i)) i) ^ (1 - p⁻¹) * (∑ i ∈ s, (fun i => ↑(w i)) i * f i ^ p) ^ p⁻¹

Proof state:
case intro
ι : Type u
s : Finset ι
p : ℝ
hp : 1 ≤ p
f : ι → ℝ
hf : ∀ (i : ι), 0 ≤ f i
w : ι → ℝ≥0
⊢ ∑ i ∈ s, (fun i => ↑(w i)) i * f i ≤
    (∑ i ∈ s, (fun i => ↑(w i)) i) ^ (1 - p⁻¹) * (∑ i ∈ s, (fun i => ↑(w i)) i * f i ^ p) ^ p⁻¹

Tactic:
lift f to ι → ℝ≥0 using hf

Result:
case intro.intro
ι : Type u
s : Finset ι
p : ℝ
hp : 1 ≤ p
w f : ι → ℝ≥0
⊢ ∑ i ∈ s, (fun i => ↑(w i)) i * (fun i => ↑(f i)) i ≤
    (∑ i ∈ s, (fun i => ↑(w i)) i) ^ (1 - p⁻¹) * (∑ i ∈ s, (fun i => ↑(w i)) i * (fun i => ↑(f i)) i ^ p) ^ p⁻¹
-- Mathlib/Order/Filter/AtTopBot/Archimedean.lean
theorem Filter.Eventually.ratCast_atTop [LinearOrderedField R] [Archimedean R] {p : R → Prop}
    (h : ∀ᶠ (x : R) in atTop, p x) : ∀ᶠ (n : ℚ) in atTop, p n

Proof state:
R : Type u_2
inst✝¹ : LinearOrderedField R
inst✝ : Archimedean R
p : R → Prop
h : ∀ᶠ (x : R) in atTop, p x
⊢ ∀ᶠ (n : ℚ) in Filter.comap Rat.cast atTop, p ↑n

Tactic:
exact h.comap _

Result:
no goals

Proof state:
R : Type u_2
inst✝¹ : LinearOrderedField R
inst✝ : Archimedean R
p : R → Prop
h : ∀ᶠ (x : R) in atTop, p x
⊢ ∀ᶠ (n : ℚ) in atTop, p ↑n

Tactic:
rw [← Rat.comap_cast_atTop (R := R)]

Result:
R : Type u_2
inst✝¹ : LinearOrderedField R
inst✝ : Archimedean R
p : R → Prop
h : ∀ᶠ (x : R) in atTop, p x
⊢ ∀ᶠ (n : ℚ) in Filter.comap Rat.cast atTop, p ↑n
-- Mathlib/Topology/Sets/OpenCover.lean
lemma of_sets {v : ι → Set X} (h_open : ∀ i, IsOpen (v i)) (h_iUnion : ⋃ i, v i = univ) :
    IsOpenCover (fun i ↦ ⟨v i, h_open i⟩)

Proof state:
ι : Type u_1
X : Type u_3
inst✝ : TopologicalSpace X
v : ι → Set X
h_open : ∀ (i : ι), IsOpen (v i)
h_iUnion : ⋃ i, v i = univ
⊢ IsOpenCover fun i => { carrier := v i, is_open' := ⋯ }

Tactic:
simp [IsOpenCover, h_iUnion]

Result:
no goals
-- Mathlib/RingTheory/Jacobson/Ring.lean
theorem isJacobsonRing_of_isIntegral [Algebra R S] [Algebra.IsIntegral R S] [IsJacobsonRing R] :
    IsJacobsonRing S

Proof state:
case neg
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : Algebra.IsIntegral R S
inst✝ : IsJacobsonRing R
P : Ideal S
hP : P.IsPrime
hP_top : ¬comap (algebraMap R S) P = ⊤
this : Nontrivial (R ⧸ comap (algebraMap R S) P)
⊢ ⊥.jacobson = ⊥

Tactic:
refine eq_bot_of_comap_eq_bot (R := R ⧸ comap (algebraMap R S) P) ?_

Result:
case neg
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : Algebra.IsIntegral R S
inst✝ : IsJacobsonRing R
P : Ideal S
hP : P.IsPrime
hP_top : ¬comap (algebraMap R S) P = ⊤
this : Nontrivial (R ⧸ comap (algebraMap R S) P)
⊢ comap (algebraMap (R ⧸ comap (algebraMap R S) P) (S ⧸ P)) ⊥.jacobson = ⊥

Proof state:
case neg
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : Algebra.IsIntegral R S
inst✝ : IsJacobsonRing R
P : Ideal S
hP : P.IsPrime
hP_top : ¬comap (algebraMap R S) P = ⊤
this : Nontrivial (R ⧸ comap (algebraMap R S) P)
⊢ P.jacobson = P

Tactic:
rw [jacobson_eq_iff_jacobson_quotient_eq_bot]

Result:
case neg
R : Type u_1
S : Type u_2
inst✝⁴ : CommRing R
inst✝³ : CommRing S
inst✝² : Algebra R S
inst✝¹ : Algebra.IsIntegral R S
inst✝ : IsJacobsonRing R
P : Ideal S
hP : P.IsPrime
hP_top : ¬comap (algebraMap R S) P = ⊤
this : Nontrivial (R ⧸ comap (algebraMap R S) P)
⊢ ⊥.jacobson = ⊥
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Div/Basic.lean
theorem mod_le (x y : Nat) : x % y ≤ x

Proof state:
x y : Nat
h₁ : x < y
⊢ x ≤ x

Tactic:
apply Nat.le_refl

Result:
no goals

Proof state:
x y : Nat
⊢ x % y ≤ x

Tactic:
match Nat.lt_or_ge x y with
| Or.inl h₁ => rw [mod_eq_of_lt h₁]; apply Nat.le_refl
| Or.inr h₁ => match eq_zero_or_pos y with
  | Or.inl h₂ => rw [h₂, Nat.mod_zero x]; apply Nat.le_refl
  | Or.inr h₂ => exact Nat.le_trans (Nat.le_of_lt (mod_lt _ h₂)) h₁

Result:
no goals

Proof state:
x y : Nat
h₁ : x ≥ y
h₂ : y > 0
⊢ x % y ≤ x

Tactic:
exact Nat.le_trans (Nat.le_of_lt (mod_lt _ h₂)) h₁

Result:
no goals

Proof state:
x y : Nat
h₁ : x < y
⊢ x % y ≤ x

Tactic:
rw [mod_eq_of_lt h₁]

Result:
x y : Nat
h₁ : x < y
⊢ x ≤ x

Proof state:
x y : Nat
h₁ : x ≥ y
⊢ x % y ≤ x

Tactic:
match eq_zero_or_pos y with
| Or.inl h₂ => rw [h₂, Nat.mod_zero x]; apply Nat.le_refl
| Or.inr h₂ => exact Nat.le_trans (Nat.le_of_lt (mod_lt _ h₂)) h₁

Result:
no goals

Proof state:
x y : Nat
h₁ : x ≥ y
h₂ : y = 0
⊢ x ≤ x

Tactic:
apply Nat.le_refl

Result:
no goals

Proof state:
x y : Nat
h₁ : x ≥ y
h₂ : y = 0
⊢ x % y ≤ x

Tactic:
rw [h₂, Nat.mod_zero x]

Result:
x y : Nat
h₁ : x ≥ y
h₂ : y = 0
⊢ x ≤ x
-- Mathlib/Data/Nat/Init.lean
lemma pow_mod (a b n : ℕ) : a ^ b % n = (a % n) ^ b % n

Proof state:
a b n : ℕ
⊢ a ^ b % n = (a % n) ^ b % n

Tactic:
induction b with
| zero => rfl
| succ b ih => simp [Nat.pow_succ, Nat.mul_mod, ih]

Result:
no goals

Proof state:
case zero
a n : ℕ
⊢ a ^ 0 % n = (a % n) ^ 0 % n

Tactic:
rfl

Result:
no goals

Proof state:
case succ
a n b : ℕ
ih : a ^ b % n = (a % n) ^ b % n
⊢ a ^ (b + 1) % n = (a % n) ^ (b + 1) % n

Tactic:
simp [Nat.pow_succ, Nat.mul_mod, ih]

Result:
no goals
-- Mathlib/Data/Multiset/Bind.lean
@[simp]
lemma dedup_bind_dedup [DecidableEq α] [DecidableEq β] (s : Multiset α) (f : α → Multiset β) :
    (s.dedup.bind f).dedup = (s.bind f).dedup

Proof state:
case a
α : Type u_1
β : Type v
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
s : Multiset α
f : α → Multiset β
x : β
⊢ x ∈ s.dedup.bind f ↔ x ∈ s.bind f

Tactic:
simp

Result:
no goals

Proof state:
case a
α : Type u_1
β : Type v
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
s : Multiset α
f : α → Multiset β
x : β
⊢ (if x ∈ s.dedup.bind f then 1 else 0) = if x ∈ s.bind f then 1 else 0

Tactic:
refine if_congr ?_ rfl rfl

Result:
case a
α : Type u_1
β : Type v
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
s : Multiset α
f : α → Multiset β
x : β
⊢ x ∈ s.dedup.bind f ↔ x ∈ s.bind f

Proof state:
case a
α : Type u_1
β : Type v
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
s : Multiset α
f : α → Multiset β
x : β
⊢ count x (s.dedup.bind f).dedup = count x (s.bind f).dedup

Tactic:
simp_rw [count_dedup]

Result:
case a
α : Type u_1
β : Type v
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
s : Multiset α
f : α → Multiset β
x : β
⊢ (if x ∈ s.dedup.bind f then 1 else 0) = if x ∈ s.bind f then 1 else 0

Proof state:
α : Type u_1
β : Type v
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
s : Multiset α
f : α → Multiset β
⊢ (s.dedup.bind f).dedup = (s.bind f).dedup

Tactic:
ext x

Result:
case a
α : Type u_1
β : Type v
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
s : Multiset α
f : α → Multiset β
x : β
⊢ count x (s.dedup.bind f).dedup = count x (s.bind f).dedup
-- Mathlib/LinearAlgebra/Matrix/Determinant/Basic.lean
theorem det_updateCol_add_smul_self (A : Matrix n n R) {i j : n} (hij : i ≠ j) (c : R) :
    det (updateCol A i fun k => A k i + c • A k j) = det A

Proof state:
n : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
A : Matrix n n R
i j : n
hij : i ≠ j
c : R
⊢ (Aᵀ.updateRow i fun k => A k i + c • A k j).det = Aᵀ.det

Tactic:
exact det_updateRow_add_smul_self Aᵀ hij c

Result:
no goals

Proof state:
n : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
A : Matrix n n R
i j : n
hij : i ≠ j
c : R
⊢ (A.updateCol i fun k => A k i + c • A k j).det = A.det

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

Result:
n : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
A : Matrix n n R
i j : n
hij : i ≠ j
c : R
⊢ (Aᵀ.updateRow i fun k => A k i + c • A k j).det = Aᵀ.det