harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Topology/Order/LawsonTopology.lean
/-- A lower set is Lawson closed if and only if it is closed under sups of directed sets -/
lemma lawsonClosed_iff_dirSupClosed_of_isLowerSet (s : Set α) (h : IsLowerSet s) :
    IsClosed[L] s ↔ DirSupClosed s

Proof state:
α : Type u_1
inst✝² : Preorder α
L S : TopologicalSpace α
inst✝¹ : IsLawson α
inst✝ : IsScott α univ
s : Set α
h : IsLowerSet s
⊢ IsClosed s ↔ DirSupClosed s

Tactic:
rw [lawsonClosed_iff_scottClosed_of_isLowerSet L S _ h,
  @IsScott.isClosed_iff_isLowerSet_and_dirSupClosed]

Result:
α : Type u_1
inst✝² : Preorder α
L S : TopologicalSpace α
inst✝¹ : IsLawson α
inst✝ : IsScott α univ
s : Set α
h : IsLowerSet s
⊢ IsLowerSet s ∧ DirSupClosed s ↔ DirSupClosed s

Proof state:
α : Type u_1
inst✝² : Preorder α
L S : TopologicalSpace α
inst✝¹ : IsLawson α
inst✝ : IsScott α univ
s : Set α
h : IsLowerSet s
⊢ IsLowerSet s ∧ DirSupClosed s ↔ DirSupClosed s

Tactic:
aesop

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem getEntry?_append [BEq α] {l l' : List ((a : α) × β a)} {a : α} :
    getEntry? a (l ++ l') = (getEntry? a l).or (getEntry? a l')

Proof state:
α : Type u
β : α → Type v
inst✝ : BEq α
l' : List ((a : α) × β a)
a k' : α
v' : β k'
t : List ((a : α) × β a)
ih : getEntry? a (t ++ l') = (getEntry? a t).or (getEntry? a l')
⊢ getEntry? a (⟨k', v'⟩ :: t ++ l') = (getEntry? a (⟨k', v'⟩ :: t)).or (getEntry? a l')

Tactic:
cases h : k' == a <;> simp_all [getEntry?_cons]

Result:
no goals

Proof state:
case cons
α : Type u
β : α → Type v
inst✝ : BEq α
l' : List ((a : α) × β a)
a k✝ : α
v✝ : β k✝
tail✝ : List ((a : α) × β a)
a✝ : getEntry? a (tail✝ ++ l') = (getEntry? a tail✝).or (getEntry? a l')
⊢ getEntry? a (⟨k✝, v✝⟩ :: tail✝ ++ l') = (getEntry? a (⟨k✝, v✝⟩ :: tail✝)).or (getEntry? a l')

Tactic:
next k' v' t ih => cases h : k' == a <;> simp_all [getEntry?_cons]

Result:
no goals

Proof state:
α : Type u
β : α → Type v
inst✝ : BEq α
l l' : List ((a : α) × β a)
a : α
⊢ getEntry? a (l ++ l') = (getEntry? a l).or (getEntry? a l')

Tactic:
induction l using assoc_induction

Result:
case nil
α : Type u
β : α → Type v
inst✝ : BEq α
l' : List ((a : α) × β a)
a : α
⊢ getEntry? a ([] ++ l') = (getEntry? a []).or (getEntry? a l')

case cons
α : Type u
β : α → Type v
inst✝ : BEq α
l' : List ((a : α) × β a)
a k✝ : α
v✝ : β k✝
tail✝ : List ((a : α) × β a)
a✝ : getEntry? a (tail✝ ++ l') = (getEntry? a tail✝).or (getEntry? a l')
⊢ getEntry? a (⟨k✝, v✝⟩ :: tail✝ ++ l') = (getEntry? a (⟨k✝, v✝⟩ :: tail✝)).or (getEntry? a l')

Proof state:
case nil
α : Type u
β : α → Type v
inst✝ : BEq α
l' : List ((a : α) × β a)
a : α
⊢ getEntry? a ([] ++ l') = (getEntry? a []).or (getEntry? a l')

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Matrix/PEquiv.lean
theorem transpose_toMatrix_toPEquiv_apply
    [DecidableEq m] [DecidableEq n] [Zero α] [One α] (f : m ≃ n) (j) :
    f.toPEquiv.toMatrixᵀ j = Pi.single (f.symm j) (1 : α)

Proof state:
case h
m : Type u_3
n : Type u_4
α : Type u_5
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : Zero α
inst✝ : One α
f : m ≃ n
j : n
x✝ : m
⊢ f.toPEquiv.toMatrixᵀ j x✝ = Pi.single (f.symm j) 1 x✝

Tactic:
simp [toMatrix_apply, Pi.single_apply, eq_comm, ← Equiv.apply_eq_iff_eq_symm_apply]

Result:
no goals

Proof state:
m : Type u_3
n : Type u_4
α : Type u_5
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : Zero α
inst✝ : One α
f : m ≃ n
j : n
⊢ f.toPEquiv.toMatrixᵀ j = Pi.single (f.symm j) 1

Tactic:
ext

Result:
case h
m : Type u_3
n : Type u_4
α : Type u_5
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : Zero α
inst✝ : One α
f : m ≃ n
j : n
x✝ : m
⊢ f.toPEquiv.toMatrixᵀ j x✝ = Pi.single (f.symm j) 1 x✝
-- Mathlib/Topology/Separation/CompletelyRegular.lean
lemma separatesPoints_continuous_of_t35Space_Icc [T35Space X] :
    SeparatesPoints (Continuous : Set (X → I))

Proof state:
X : Type u
inst✝² : TopologicalSpace X
inst✝¹ : T1Space X
inst✝ : T35Space X
x y : X
x_ne_y : x ≠ y
f : X → ↑I
f_cont : Continuous f
f_zero : f x = 0
f_one : EqOn f 1 {y}
⊢ f x ≠ f y

Tactic:
aesop

Result:
no goals

Proof state:
X : Type u
inst✝² : TopologicalSpace X
inst✝¹ : T1Space X
inst✝ : T35Space X
x y : X
x_ne_y : x ≠ y
⊢ ∃ f ∈ Continuous, f x ≠ f y

Tactic:
obtain ⟨f, f_cont, f_zero, f_one⟩ :=
  CompletelyRegularSpace.completely_regular x {y} isClosed_singleton x_ne_y

Result:
case intro.intro.intro
X : Type u
inst✝² : TopologicalSpace X
inst✝¹ : T1Space X
inst✝ : T35Space X
x y : X
x_ne_y : x ≠ y
f : X → ↑I
f_cont : Continuous f
f_zero : f x = 0
f_one : EqOn f 1 {y}
⊢ ∃ f ∈ Continuous, f x ≠ f y

Proof state:
case intro.intro.intro
X : Type u
inst✝² : TopologicalSpace X
inst✝¹ : T1Space X
inst✝ : T35Space X
x y : X
x_ne_y : x ≠ y
f : X → ↑I
f_cont : Continuous f
f_zero : f x = 0
f_one : EqOn f 1 {y}
⊢ ∃ f ∈ Continuous, f x ≠ f y

Tactic:
exact ⟨f, f_cont, by aesop⟩

Result:
no goals

Proof state:
X : Type u
inst✝² : TopologicalSpace X
inst✝¹ : T1Space X
inst✝ : T35Space X
⊢ SeparatesPoints Continuous

Tactic:
intro x y x_ne_y

Result:
X : Type u
inst✝² : TopologicalSpace X
inst✝¹ : T1Space X
inst✝ : T35Space X
x y : X
x_ne_y : x ≠ y
⊢ ∃ f ∈ Continuous, f x ≠ f y
-- Mathlib/LinearAlgebra/RootSystem/CartanMatrix.lean
@[simp]
lemma cartanMatrixIn_apply_same [FaithfulSMul S R] (i : b.support) :
    b.cartanMatrixIn S i i = 2 :=
  FaithfulSMul.algebraMap_injective S R <| by simp [cartanMatrixIn_def, map_ofNat]

Proof state:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁸ : CommRing R
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
inst✝⁵ : AddCommGroup N
inst✝⁴ : Module R N
S : Type u_5
inst✝³ : CommRing S
inst✝² : Algebra S R
P : RootPairing ι R M N
inst✝¹ : P.IsValuedIn S
b : P.Base
inst✝ : FaithfulSMul S R
i : ↑b.support
⊢ (algebraMap S R) (cartanMatrixIn S b i i) = (algebraMap S R) 2

Tactic:
simp [cartanMatrixIn_def, map_ofNat]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem toFin_and (x y : BitVec v) :
    BitVec.toFin (x &&& y) = BitVec.toFin x &&& BitVec.toFin y

Proof state:
v : Nat
x y : BitVec v
⊢ (x &&& y).toFin = x.toFin &&& y.toFin

Tactic:
apply Fin.eq_of_val_eq

Result:
case a
v : Nat
x y : BitVec v
⊢ ↑(x &&& y).toFin = ↑(x.toFin &&& y.toFin)

Proof state:
case a
v : Nat
x y : BitVec v
⊢ ↑(x &&& y).toFin = ↑(x.toFin &&& y.toFin)

Tactic:
exact (Nat.mod_eq_of_lt <| Nat.and_lt_two_pow _ y.isLt).symm

Result:
no goals
-- Mathlib/MeasureTheory/Constructions/BorelSpace/Real.lean
theorem measure_ext_Ioo_rat {μ ν : Measure ℝ} [IsLocallyFiniteMeasure μ]
    (h : ∀ a b : ℚ, μ (Ioo a b) = ν (Ioo a b)) : μ = ν :=
  (finiteSpanningSetsInIooRat μ).ext borel_eq_generateFrom_Ioo_rat isPiSystem_Ioo_rat <| by
    simp only [mem_iUnion, mem_singleton_iff]
    rintro _ ⟨a, b, -, rfl⟩
    apply h

Proof state:
μ ν : Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
h : ∀ (a b : ℚ), μ (Ioo ↑a ↑b) = ν (Ioo ↑a ↑b)
⊢ ∀ (s : Set ℝ), (∃ i i_1, ∃ (_ : i < i_1), s = Ioo ↑i ↑i_1) → μ s = ν s

Tactic:
rintro _ ⟨a, b, -, rfl⟩

Result:
case intro.intro.intro
μ ν : Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
h : ∀ (a b : ℚ), μ (Ioo ↑a ↑b) = ν (Ioo ↑a ↑b)
a b : ℚ
⊢ μ (Ioo ↑a ↑b) = ν (Ioo ↑a ↑b)

Proof state:
μ ν : Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
h : ∀ (a b : ℚ), μ (Ioo ↑a ↑b) = ν (Ioo ↑a ↑b)
⊢ ∀ s ∈ ⋃ a, ⋃ b, ⋃ (_ : a < b), {Ioo ↑a ↑b}, μ s = ν s

Tactic:
simp only [mem_iUnion, mem_singleton_iff]

Result:
μ ν : Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
h : ∀ (a b : ℚ), μ (Ioo ↑a ↑b) = ν (Ioo ↑a ↑b)
⊢ ∀ (s : Set ℝ), (∃ i i_1, ∃ (_ : i < i_1), s = Ioo ↑i ↑i_1) → μ s = ν s

Proof state:
case intro.intro.intro
μ ν : Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
h : ∀ (a b : ℚ), μ (Ioo ↑a ↑b) = ν (Ioo ↑a ↑b)
a b : ℚ
⊢ μ (Ioo ↑a ↑b) = ν (Ioo ↑a ↑b)

Tactic:
apply h

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem get!_insertMany_list_of_mem [LawfulBEq α] (h : m.WF)
    {l : List ((a : α) × β a)} {k k' : α} (k_beq : k == k') {v : β k} [Inhabited (β k')]
    (distinct : l.Pairwise (fun a b => (a.1 == b.1) = false))
    (mem : ⟨k, v⟩ ∈ l) :
    (m.insertMany l).get! k' = cast (by congr; apply LawfulBEq.eq_of_beq k_beq) v

Proof state:
case e_a
α : Type u
β : α → Type v
m : Raw α β
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : LawfulBEq α
h : m.WF
l : List ((a : α) × β a)
k k' : α
k_beq : (k == k') = true
v : β k
inst✝ : Inhabited (β k')
distinct : List.Pairwise (fun a b => (a.fst == b.fst) = false) l
mem : ⟨k, v⟩ ∈ l
⊢ k = k'

Tactic:
apply LawfulBEq.eq_of_beq k_beq

Result:
no goals

Proof state:
α : Type u
β : α → Type v
m : Raw α β
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : LawfulBEq α
h : m.WF
l : List ((a : α) × β a)
k k' : α
k_beq : (k == k') = true
v : β k
inst✝ : Inhabited (β k')
distinct : List.Pairwise (fun a b => (a.fst == b.fst) = false) l
mem : ⟨k, v⟩ ∈ l
⊢ (m.insertMany l).get! k' = cast ⋯ v

Tactic:
simp_to_raw using Raw₀.get!_insertMany_list_of_mem

Result:
no goals

Proof state:
α : Type u
β : α → Type v
m : Raw α β
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : LawfulBEq α
h : m.WF
l : List ((a : α) × β a)
k k' : α
k_beq : (k == k') = true
v : β k
inst✝ : Inhabited (β k')
distinct : List.Pairwise (fun a b => (a.fst == b.fst) = false) l
mem : ⟨k, v⟩ ∈ l
⊢ β k = β k'

Tactic:
congr

Result:
case e_a
α : Type u
β : α → Type v
m : Raw α β
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : LawfulBEq α
h : m.WF
l : List ((a : α) × β a)
k k' : α
k_beq : (k == k') = true
v : β k
inst✝ : Inhabited (β k')
distinct : List.Pairwise (fun a b => (a.fst == b.fst) = false) l
mem : ⟨k, v⟩ ∈ l
⊢ k = k'
-- Mathlib/CategoryTheory/Sites/Sieves.lean
theorem arrows_ext : ∀ {R S : Sieve X}, R.arrows = S.arrows → R = S

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
⊢ ∀ {R S : Sieve X}, R.arrows = S.arrows → R = S

Tactic:
rintro ⟨_, _⟩ ⟨_, _⟩ rfl

Result:
case mk.mk
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
arrows✝ : Presieve X
downward_closed✝¹ : ∀ {Y Z : C} {f : Y ⟶ X}, arrows✝ f → ∀ (g : Z ⟶ Y), arrows✝ (g ≫ f)
downward_closed✝ :
  ∀ {Y Z : C} {f : Y ⟶ X},
    { arrows := arrows✝, downward_closed := downward_closed✝¹ }.arrows f →
      ∀ (g : Z ⟶ Y), { arrows := arrows✝, downward_closed := downward_closed✝¹ }.arrows (g ≫ f)
⊢ { arrows := arrows✝, downward_closed := downward_closed✝¹ } =
    { arrows := { arrows := arrows✝, downward_closed := downward_closed✝¹ }.arrows,
      downward_closed := downward_closed✝ }

Proof state:
case mk.mk
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
arrows✝ : Presieve X
downward_closed✝¹ : ∀ {Y Z : C} {f : Y ⟶ X}, arrows✝ f → ∀ (g : Z ⟶ Y), arrows✝ (g ≫ f)
downward_closed✝ :
  ∀ {Y Z : C} {f : Y ⟶ X},
    { arrows := arrows✝, downward_closed := downward_closed✝¹ }.arrows f →
      ∀ (g : Z ⟶ Y), { arrows := arrows✝, downward_closed := downward_closed✝¹ }.arrows (g ≫ f)
⊢ { arrows := arrows✝, downward_closed := downward_closed✝¹ } =
    { arrows := { arrows := arrows✝, downward_closed := downward_closed✝¹ }.arrows,
      downward_closed := downward_closed✝ }

Tactic:
rfl

Result:
no goals
-- Mathlib/RingTheory/Spectrum/Prime/Topology.lean
theorem comap_id : comap (RingHom.id R) = ContinuousMap.id _

Proof state:
case h.asIdeal.h
R : Type u
inst✝ : CommSemiring R
a✝ : PrimeSpectrum R
x✝ : R
⊢ x✝ ∈ ((comap (RingHom.id R)) a✝).asIdeal ↔ x✝ ∈ ((ContinuousMap.id (PrimeSpectrum R)) a✝).asIdeal

Tactic:
rfl

Result:
no goals

Proof state:
R : Type u
inst✝ : CommSemiring R
⊢ comap (RingHom.id R) = ContinuousMap.id (PrimeSpectrum R)

Tactic:
ext

Result:
case h.asIdeal.h
R : Type u
inst✝ : CommSemiring R
a✝ : PrimeSpectrum R
x✝ : R
⊢ x✝ ∈ ((comap (RingHom.id R)) a✝).asIdeal ↔ x✝ ∈ ((ContinuousMap.id (PrimeSpectrum R)) a✝).asIdeal
-- Mathlib/Analysis/Complex/Basic.lean
theorem restrictScalars_one_smulRight (x : ℂ) :
    ContinuousLinearMap.restrictScalars ℝ ((1 : ℂ →L[ℂ] ℂ).smulRight x : ℂ →L[ℂ] ℂ) =
    x • (1 : ℂ →L[ℝ] ℂ)

Proof state:
x : ℂ
⊢ restrictScalars ℝ (smulRight 1 x) = x • 1

Tactic:
ext1 z

Result:
case h
x z : ℂ
⊢ (restrictScalars ℝ (smulRight 1 x)) z = (x • 1) z

Proof state:
case h
x z : ℂ
⊢ z * x = x * z

Tactic:
apply mul_comm

Result:
no goals

Proof state:
case h
x z : ℂ
⊢ (restrictScalars ℝ (smulRight 1 x)) z = (x • 1) z

Tactic:
dsimp

Result:
case h
x z : ℂ
⊢ z * x = x * z
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem toNat_setWidth' {m n : Nat} (p : m ≤ n) (x : BitVec m) :
    (setWidth' p x).toNat = x.toNat

Proof state:
m n : Nat
p : m ≤ n
x : BitVec m
⊢ (setWidth' p x).toNat = x.toNat

Tactic:
simp [setWidth']

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Basic.lean
theorem sub_self : ∀ (n : Nat), n - n = 0
  | 0        => by rw [Nat.sub_zero]
  | (succ n) => by rw [succ_sub_succ, Nat.sub_self n]

Proof state:
⊢ 0 - 0 = 0

Tactic:
rw [Nat.sub_zero]

Result:
no goals

Proof state:
n : Nat
⊢ n.succ - n.succ = 0

Tactic:
rw [succ_sub_succ, Nat.sub_self n]

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

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

Tactic:
simp_to_model [modify] using List.getValueCastD_modifyKey

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Nat/Modify.lean
theorem length_modifyHead {f : α → α} {l : List α} : (l.modifyHead f).length = l.length

Proof state:
α : Type u_1
f : α → α
l : List α
⊢ (modifyHead f l).length = l.length

Tactic:
cases l <;> simp [modifyHead]

Result:
no goals
-- Mathlib/Logic/Equiv/Fin.lean
theorem finSuccEquiv'_ne_last_apply {i j : Fin (n + 1)} (hi : i ≠ Fin.last n) (hj : j ≠ i) :
    finSuccEquiv' i j = (i.castLT (Fin.val_lt_last hi)).predAbove j

Proof state:
n : ℕ
i j : Fin (n + 1)
hi : i ≠ Fin.last n
hj : j ≠ i
⊢ (finSuccEquiv' i) j = some ((i.castLT ⋯).predAbove j)

Tactic:
rcases Fin.exists_succAbove_eq hj with ⟨j, rfl⟩

Result:
case intro
n : ℕ
i : Fin (n + 1)
hi : i ≠ Fin.last n
j : Fin n
hj : i.succAbove j ≠ i
⊢ (finSuccEquiv' i) (i.succAbove j) = some ((i.castLT ⋯).predAbove (i.succAbove j))

Proof state:
case intro
n : ℕ
i : Fin (n + 1)
hi : i ≠ Fin.last n
j : Fin n
hj : i.succAbove j ≠ i
⊢ (finSuccEquiv' i) (i.succAbove j) = some ((i.castLT ⋯).predAbove (i.succAbove j))

Tactic:
rcases Fin.exists_castSucc_eq.2 hi with ⟨i, rfl⟩

Result:
case intro.intro
n : ℕ
j i : Fin n
hi : i.castSucc ≠ Fin.last n
hj : i.castSucc.succAbove j ≠ i.castSucc
⊢ (finSuccEquiv' i.castSucc) (i.castSucc.succAbove j) = some ((i.castSucc.castLT ⋯).predAbove (i.castSucc.succAbove j))

Proof state:
case intro.intro
n : ℕ
j i : Fin n
hi : i.castSucc ≠ Fin.last n
hj : i.castSucc.succAbove j ≠ i.castSucc
⊢ (finSuccEquiv' i.castSucc) (i.castSucc.succAbove j) = some ((i.castSucc.castLT ⋯).predAbove (i.castSucc.succAbove j))

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Order/BigOperators/Expect.lean
lemma expect_nonneg (hf : ∀ i ∈ s, 0 ≤ f i) : 0 ≤ 𝔼 i ∈ s, f i :=
  smul_nonneg (by positivity) <| sum_nonneg hf

Proof state:
ι : Type u_1
α : Type u_2
inst✝² : OrderedAddCommMonoid α
inst✝¹ : Module ℚ≥0 α
s : Finset ι
f : ι → α
inst✝ : PosSMulMono ℚ≥0 α
hf : ∀ i ∈ s, 0 ≤ f i
⊢ 0 ≤ (↑(#s))⁻¹

Tactic:
positivity

Result:
no goals
-- Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean
theorem eLpNorm_lt_top_iff_lintegral_rpow_enorm_lt_top {f : α → ε} (hp_ne_zero : p ≠ 0)
    (hp_ne_top : p ≠ ∞) : eLpNorm f p μ < ∞ ↔ ∫⁻ a, (‖f a‖ₑ) ^ p.toReal ∂μ < ∞ :=
  ⟨lintegral_rpow_enorm_lt_top_of_eLpNorm_lt_top hp_ne_zero hp_ne_top, by
    intro h
    have hp' := ENNReal.toReal_pos hp_ne_zero hp_ne_top
    have : 0 < 1 / p.toReal := div_pos zero_lt_one hp'
    simpa [eLpNorm_eq_lintegral_rpow_enorm hp_ne_zero hp_ne_top] using
      ENNReal.rpow_lt_top_of_nonneg (le_of_lt this) (ne_of_lt h)⟩

Proof state:
α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : ENorm ε
f : α → ε
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ⊤
h : ∫⁻ (a : α), ‖f a‖ₑ ^ p.toReal ∂μ < ⊤
hp' : 0 < p.toReal
⊢ eLpNorm f p μ < ⊤

Tactic:
have : 0 < 1 / p.toReal := div_pos zero_lt_one hp'

Result:
α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : ENorm ε
f : α → ε
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ⊤
h : ∫⁻ (a : α), ‖f a‖ₑ ^ p.toReal ∂μ < ⊤
hp' : 0 < p.toReal
this : 0 < 1 / p.toReal
⊢ eLpNorm f p μ < ⊤

Proof state:
α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : ENorm ε
f : α → ε
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ⊤
⊢ ∫⁻ (a : α), ‖f a‖ₑ ^ p.toReal ∂μ < ⊤ → eLpNorm f p μ < ⊤

Tactic:
intro h

Result:
α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : ENorm ε
f : α → ε
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ⊤
h : ∫⁻ (a : α), ‖f a‖ₑ ^ p.toReal ∂μ < ⊤
⊢ eLpNorm f p μ < ⊤

Proof state:
α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : ENorm ε
f : α → ε
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ⊤
h : ∫⁻ (a : α), ‖f a‖ₑ ^ p.toReal ∂μ < ⊤
hp' : 0 < p.toReal
this : 0 < 1 / p.toReal
⊢ eLpNorm f p μ < ⊤

Tactic:
simpa [eLpNorm_eq_lintegral_rpow_enorm hp_ne_zero hp_ne_top] using
  ENNReal.rpow_lt_top_of_nonneg (le_of_lt this) (ne_of_lt h)

Result:
no goals

Proof state:
α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : ENorm ε
f : α → ε
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ⊤
h : ∫⁻ (a : α), ‖f a‖ₑ ^ p.toReal ∂μ < ⊤
⊢ eLpNorm f p μ < ⊤

Tactic:
have hp' := ENNReal.toReal_pos hp_ne_zero hp_ne_top

Result:
α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : ENorm ε
f : α → ε
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ⊤
h : ∫⁻ (a : α), ‖f a‖ₑ ^ p.toReal ∂μ < ⊤
hp' : 0 < p.toReal
⊢ eLpNorm f p μ < ⊤
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem isEmpty_erase [EquivBEq α] [LawfulHashable α] (h : m.WF) {k : α} :
    (m.erase k).isEmpty = (m.isEmpty || (m.size == 1 && m.contains k))

Proof state:
α : Type u
β : α → Type v
m : Raw α β
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.WF
k : α
⊢ (m.erase k).isEmpty = (m.isEmpty || m.size == 1 && m.contains k)

Tactic:
simp_to_raw using Raw₀.isEmpty_erase

Result:
no goals
-- Mathlib/Analysis/Normed/Affine/ContinuousAffineMap.lean
theorem decomp (f : V →ᴬ[R] W) : (f : V → W) = f.contLinear + Function.const V (f 0)

Proof state:
case mk
R : Type u_2
V : Type u_3
W : Type u_4
inst✝⁴ : NormedAddCommGroup V
inst✝³ : NormedAddCommGroup W
inst✝² : NormedField R
inst✝¹ : NormedSpace R V
inst✝ : NormedSpace R W
f : V →ᵃ[R] W
h : Continuous f.toFun
⊢ ⇑{ toAffineMap := f, cont := h } =
    ⇑{ toAffineMap := f, cont := h }.contLinear + Function.const V ({ toAffineMap := f, cont := h } 0)

Tactic:
rw [coe_mk_const_linear_eq_linear, coe_mk, f.decomp, Pi.add_apply, LinearMap.map_zero, zero_add,
  ← Function.const_def]

Result:
no goals

Proof state:
R : Type u_2
V : Type u_3
W : Type u_4
inst✝⁴ : NormedAddCommGroup V
inst✝³ : NormedAddCommGroup W
inst✝² : NormedField R
inst✝¹ : NormedSpace R V
inst✝ : NormedSpace R W
f : V →ᴬ[R] W
⊢ ⇑f = ⇑f.contLinear + Function.const V (f 0)

Tactic:
rcases f with ⟨f, h⟩

Result:
case mk
R : Type u_2
V : Type u_3
W : Type u_4
inst✝⁴ : NormedAddCommGroup V
inst✝³ : NormedAddCommGroup W
inst✝² : NormedField R
inst✝¹ : NormedSpace R V
inst✝ : NormedSpace R W
f : V →ᵃ[R] W
h : Continuous f.toFun
⊢ ⇑{ toAffineMap := f, cont := h } =
    ⇑{ toAffineMap := f, cont := h }.contLinear + Function.const V ({ toAffineMap := f, cont := h } 0)
-- Mathlib/Data/Set/Lattice.lean
theorem union_iInter₂ (s : Set α) (t : ∀ i, κ i → Set α) :
    (s ∪ ⋂ (i) (j), t i j) = ⋂ (i) (j), s ∪ t i j

Proof state:
α : Type u_1
ι : Sort u_5
κ : ι → Sort u_8
s : Set α
t : (i : ι) → κ i → Set α
⊢ s ∪ ⋂ i, ⋂ j, t i j = ⋂ i, ⋂ j, s ∪ t i j

Tactic:
simp_rw [union_iInter]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/Order.lean
theorem eq_succ_of_zero_lt {a : Int} (h : 0 < a) : ∃ n : Nat, a = n.succ :=
  let ⟨n, (h : ↑(1 + n) = a)⟩ := le.dest h
  ⟨n, by rw [Nat.add_comm] at h; exact h.symm⟩

Proof state:
a : Int
h✝ : 0 < a
n : Nat
h : ↑(n + 1) = a
⊢ a = ↑n.succ

Tactic:
exact h.symm

Result:
no goals

Proof state:
a : Int
h✝ : 0 < a
n : Nat
h : ↑(1 + n) = a
⊢ a = ↑n.succ

Tactic:
rw [Nat.add_comm] at h

Result:
a : Int
h✝ : 0 < a
n : Nat
h : ↑(n + 1) = a
⊢ a = ↑n.succ
-- Mathlib/Analysis/Calculus/VectorField.lean
/-- The Lie bracket commutes with taking pullbacks. This requires the function to have symmetric
second derivative. Version in a complete space. One could also give a version avoiding
completeness but requiring that `f` is a local diffeo. -/
lemma pullback_lieBracket_of_isSymmSndFDerivAt {f : E → F} {V W : F → F} {x : E}
    (hf : IsSymmSndFDerivAt 𝕜 f x) (h'f : ContDiffAt 𝕜 2 f x)
    (hV : DifferentiableAt 𝕜 V (f x)) (hW : DifferentiableAt 𝕜 W (f x)) :
    pullback 𝕜 f (lieBracket 𝕜 V W) x = lieBracket 𝕜 (pullback 𝕜 f V) (pullback 𝕜 f W) 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
inst✝ : CompleteSpace E
f : E → F
V W : F → F
x : E
h'f : ContDiffAt 𝕜 2 f x
hf : IsSymmSndFDerivWithinAt 𝕜 f univ x
hV : DifferentiableWithinAt 𝕜 V univ (f x)
hW : DifferentiableWithinAt 𝕜 W univ (f x)
⊢ pullbackWithin 𝕜 f (lieBracketWithin 𝕜 V W univ) univ x =
    lieBracketWithin 𝕜 (pullbackWithin 𝕜 f V univ) (pullbackWithin 𝕜 f W univ) univ x

Tactic:
exact pullbackWithin_lieBracketWithin_of_isSymmSndFDerivWithinAt hf h'f hV hW uniqueDiffOn_univ
  (mem_univ _) (mapsTo_univ _ _)

Result:
no goals

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
inst✝ : CompleteSpace E
f : E → F
V W : F → F
x : E
hf : IsSymmSndFDerivAt 𝕜 f x
h'f : ContDiffAt 𝕜 2 f x
hV : DifferentiableAt 𝕜 V (f x)
hW : DifferentiableAt 𝕜 W (f x)
⊢ pullback 𝕜 f (lieBracket 𝕜 V W) x = lieBracket 𝕜 (pullback 𝕜 f V) (pullback 𝕜 f W) x

Tactic:
simp only [← lieBracketWithin_univ, ← pullbackWithin_univ, ← isSymmSndFDerivWithinAt_univ,
  ← differentiableWithinAt_univ] at hf h'f hV hW ⊢

Result:
𝕜 : 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
inst✝ : CompleteSpace E
f : E → F
V W : F → F
x : E
h'f : ContDiffAt 𝕜 2 f x
hf : IsSymmSndFDerivWithinAt 𝕜 f univ x
hV : DifferentiableWithinAt 𝕜 V univ (f x)
hW : DifferentiableWithinAt 𝕜 W univ (f x)
⊢ pullbackWithin 𝕜 f (lieBracketWithin 𝕜 V W univ) univ x =
    lieBracketWithin 𝕜 (pullbackWithin 𝕜 f V univ) (pullbackWithin 𝕜 f W univ) univ x
-- Mathlib/Data/Ordmap/Ordset.lean
theorem dual_rotateR (l : Ordnode α) (x : α) (r : Ordnode α) :
    dual (rotateR l x r) = rotateL (dual r) x (dual l)

Proof state:
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
⊢ (l.rotateR x r).dual = r.dual.rotateL x l.dual

Tactic:
rw [← dual_dual (rotateL _ _ _), dual_rotateL, dual_dual, dual_dual]

Result:
no goals