harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/MeasureTheory/Function/LpSeminorm/TriangleInequality.lean
theorem eLpNorm_sub_le' (hf : AEStronglyMeasurable f μ) (hg : AEStronglyMeasurable g μ)
    (p : ℝ≥0∞) : eLpNorm (f - g) p μ ≤ LpAddConst p * (eLpNorm f p μ + eLpNorm g p μ)

Proof state:
α : Type u_1
E : Type u_2
m : MeasurableSpace α
inst✝ : NormedAddCommGroup E
μ : Measure α
f g : α → E
hf : AEStronglyMeasurable f μ
hg : AEStronglyMeasurable g μ
p : ℝ≥0∞
⊢ eLpNorm (f - g) p μ ≤ LpAddConst p * (eLpNorm f p μ + eLpNorm g p μ)

Tactic:
simpa only [sub_eq_add_neg, eLpNorm_neg] using eLpNorm_add_le' hf hg.neg p

Result:
no goals
-- Mathlib/Analysis/Convex/Function.lean
theorem ConvexOn.le_left_of_right_le (hf : ConvexOn 𝕜 s f) {x y z : E} (hx : x ∈ s) (hy : y ∈ s)
    (hz : z ∈ openSegment 𝕜 x y) (hyz : f y ≤ f z) : f z ≤ f x

Proof state:
𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst✝⁵ : OrderedSemiring 𝕜
inst✝⁴ : AddCommMonoid E
inst✝³ : LinearOrderedCancelAddCommMonoid β
inst✝² : SMul 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : OrderedSMul 𝕜 β
s : Set E
f : E → β
hf : ConvexOn 𝕜 s f
x y z : E
hx : x ∈ s
hy : y ∈ s
hz : z ∈ openSegment 𝕜 x y
hyz : f y ≤ f z
⊢ f z ≤ f x

Tactic:
obtain ⟨a, b, ha, hb, hab, rfl⟩ := hz

Result:
case intro.intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst✝⁵ : OrderedSemiring 𝕜
inst✝⁴ : AddCommMonoid E
inst✝³ : LinearOrderedCancelAddCommMonoid β
inst✝² : SMul 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : OrderedSMul 𝕜 β
s : Set E
f : E → β
hf : ConvexOn 𝕜 s f
x y : E
hx : x ∈ s
hy : y ∈ s
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
hyz : f y ≤ f (a • x + b • y)
⊢ f (a • x + b • y) ≤ f x

Proof state:
case intro.intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst✝⁵ : OrderedSemiring 𝕜
inst✝⁴ : AddCommMonoid E
inst✝³ : LinearOrderedCancelAddCommMonoid β
inst✝² : SMul 𝕜 E
inst✝¹ : Module 𝕜 β
inst✝ : OrderedSMul 𝕜 β
s : Set E
f : E → β
hf : ConvexOn 𝕜 s f
x y : E
hx : x ∈ s
hy : y ∈ s
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
hyz : f y ≤ f (a • x + b • y)
⊢ f (a • x + b • y) ≤ f x

Tactic:
exact hf.le_left_of_right_le' hx hy ha hb.le hab hyz

Result:
no goals
-- Mathlib/Data/Real/EReal.lean
theorem add_lt_add_of_lt_of_le' {x y z t : EReal} (h : x < y) (h' : z ≤ t) (hbot : t ≠ ⊥)
    (htop : t = ⊤ → z = ⊤ → x = ⊥) : x + z < y + t

Proof state:
case inl.inl
x y : EReal
h : x < y
h' : ⊤ ≤ ⊤
hbot : ⊤ ≠ ⊥
htop : ⊤ = ⊤ → ⊤ = ⊤ → x = ⊥
⊢ x + ⊤ < y + ⊤

Tactic:
obtain rfl := htop rfl rfl

Result:
case inl.inl
y : EReal
h' : ⊤ ≤ ⊤
hbot : ⊤ ≠ ⊥
h : ⊥ < y
htop : ⊤ = ⊤ → ⊤ = ⊤ → ⊥ = ⊥
⊢ ⊥ + ⊤ < y + ⊤

Proof state:
case inl.inl
y : EReal
h' : ⊤ ≤ ⊤
hbot : ⊤ ≠ ⊥
h : ⊥ < y
htop : ⊤ = ⊤ → ⊤ = ⊤ → ⊥ = ⊥
⊢ ⊥ + ⊤ < y + ⊤

Tactic:
simpa

Result:
no goals

Proof state:
x y z t : EReal
h : x < y
h' : z ≤ t
hbot : t ≠ ⊥
htop : t = ⊤ → z = ⊤ → x = ⊥
⊢ x + z < y + t

Tactic:
rcases h'.eq_or_lt with (rfl | hlt)

Result:
case inl
x y z : EReal
h : x < y
h' : z ≤ z
hbot : z ≠ ⊥
htop : z = ⊤ → z = ⊤ → x = ⊥
⊢ x + z < y + z

case inr
x y z t : EReal
h : x < y
h' : z ≤ t
hbot : t ≠ ⊥
htop : t = ⊤ → z = ⊤ → x = ⊥
hlt : z < t
⊢ x + z < y + t

Proof state:
case inr
x y z t : EReal
h : x < y
h' : z ≤ t
hbot : t ≠ ⊥
htop : t = ⊤ → z = ⊤ → x = ⊥
hlt : z < t
⊢ x + z < y + t

Tactic:
exact add_lt_add h hlt

Result:
no goals

Proof state:
case inl.inr
x y z : EReal
h : x < y
h' : z ≤ z
hbot : z ≠ ⊥
htop : z = ⊤ → z = ⊤ → x = ⊥
hz : z ≠ ⊤
⊢ x + z < y + z

Tactic:
lift z to ℝ using ⟨hz, hbot⟩

Result:
case inl.inr.intro
x y : EReal
h : x < y
z : ℝ
h' : ↑z ≤ ↑z
hbot : ↑z ≠ ⊥
htop : ↑z = ⊤ → ↑z = ⊤ → x = ⊥
hz : ↑z ≠ ⊤
⊢ x + ↑z < y + ↑z

Proof state:
case inl
x y z : EReal
h : x < y
h' : z ≤ z
hbot : z ≠ ⊥
htop : z = ⊤ → z = ⊤ → x = ⊥
⊢ x + z < y + z

Tactic:
rcases eq_or_ne z ⊤ with (rfl | hz)

Result:
case inl.inl
x y : EReal
h : x < y
h' : ⊤ ≤ ⊤
hbot : ⊤ ≠ ⊥
htop : ⊤ = ⊤ → ⊤ = ⊤ → x = ⊥
⊢ x + ⊤ < y + ⊤

case inl.inr
x y z : EReal
h : x < y
h' : z ≤ z
hbot : z ≠ ⊥
htop : z = ⊤ → z = ⊤ → x = ⊥
hz : z ≠ ⊤
⊢ x + z < y + z

Proof state:
case inl.inr.intro
x y : EReal
h : x < y
z : ℝ
h' : ↑z ≤ ↑z
hbot : ↑z ≠ ⊥
htop : ↑z = ⊤ → ↑z = ⊤ → x = ⊥
hz : ↑z ≠ ⊤
⊢ x + ↑z < y + ↑z

Tactic:
exact add_lt_add_right_coe h z

Result:
no goals
-- Mathlib/CategoryTheory/Quotient.lean
lemma compClosure_iff_self [h : Congruence r] {X Y : C} (f g : X ⟶ Y) :
    CompClosure r f g ↔ r f g

Proof state:
case mp
C : Type u_1
inst✝ : Category.{u_2, u_1} C
r : HomRel C
h : Congruence r
X Y : C
f g : X ⟶ Y
hfg : CompClosure r f g
⊢ r f g

Tactic:
induction' hfg with m m' hm

Result:
case mp.intro
C : Type u_1
inst✝ : Category.{u_2, u_1} C
r : HomRel C
h : Congruence r
X Y : C
f g : X ⟶ Y
m m' : C
hm : X ⟶ m
m₁✝ m₂✝ : m ⟶ m'
g✝ : m' ⟶ Y
h✝ : r m₁✝ m₂✝
⊢ r (hm ≫ m₁✝ ≫ g✝) (hm ≫ m₂✝ ≫ g✝)

Proof state:
C : Type u_1
inst✝ : Category.{u_2, u_1} C
r : HomRel C
h : Congruence r
X Y : C
f g : X ⟶ Y
m m' : C
hm : X ⟶ m
m₁✝ m₂✝ : m ⟶ m'
g✝ : m' ⟶ Y
h✝ : r m₁✝ m₂✝
⊢ r m₁✝ m₂✝

Tactic:
assumption

Result:
no goals

Proof state:
C : Type u_1
inst✝ : Category.{u_2, u_1} C
r : HomRel C
h : Congruence r
X Y : C
f g : X ⟶ Y
⊢ CompClosure r f g ↔ r f g

Tactic:
constructor

Result:
case mp
C : Type u_1
inst✝ : Category.{u_2, u_1} C
r : HomRel C
h : Congruence r
X Y : C
f g : X ⟶ Y
⊢ CompClosure r f g → r f g

case mpr
C : Type u_1
inst✝ : Category.{u_2, u_1} C
r : HomRel C
h : Congruence r
X Y : C
f g : X ⟶ Y
⊢ r f g → CompClosure r f g

Proof state:
case mp
C : Type u_1
inst✝ : Category.{u_2, u_1} C
r : HomRel C
h : Congruence r
X Y : C
f g : X ⟶ Y
⊢ CompClosure r f g → r f g

Tactic:
intro hfg

Result:
case mp
C : Type u_1
inst✝ : Category.{u_2, u_1} C
r : HomRel C
h : Congruence r
X Y : C
f g : X ⟶ Y
hfg : CompClosure r f g
⊢ r f g

Proof state:
case mp.intro
C : Type u_1
inst✝ : Category.{u_2, u_1} C
r : HomRel C
h : Congruence r
X Y : C
f g : X ⟶ Y
m m' : C
hm : X ⟶ m
m₁✝ m₂✝ : m ⟶ m'
g✝ : m' ⟶ Y
h✝ : r m₁✝ m₂✝
⊢ r (hm ≫ m₁✝ ≫ g✝) (hm ≫ m₂✝ ≫ g✝)

Tactic:
exact Congruence.compLeft _ (Congruence.compRight _ (by assumption))

Result:
no goals

Proof state:
case mpr
C : Type u_1
inst✝ : Category.{u_2, u_1} C
r : HomRel C
h : Congruence r
X Y : C
f g : X ⟶ Y
⊢ r f g → CompClosure r f g

Tactic:
exact CompClosure.of _ _ _

Result:
no goals
-- Mathlib/Order/UpperLower/Basic.lean
theorem bddAbove_lowerClosure : BddAbove (lowerClosure s : Set α) ↔ BddAbove s

Proof state:
α : Type u_1
inst✝ : Preorder α
s : Set α
⊢ BddAbove ↑(lowerClosure s) ↔ BddAbove s

Tactic:
simp_rw [BddAbove, upperBounds_lowerClosure]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Sat/AIG/CachedLemmas.lean
theorem mkConstCached_miss_aig (aig : AIG α) (hcache : aig.cache.get? (.const val) = none) :
    (aig.mkConstCached val).aig.decls = aig.decls.push (.const val)

Proof state:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
val : Bool
aig : AIG α
hcache : aig.cache.get? (Decl.const val) = none
⊢ (match aig.cache.get? (Decl.const val) with
        | some hit =>
          { aig := { decls := aig.decls, cache := aig.cache, invariant := ⋯ }, ref := { gate := hit.idx, hgate := ⋯ } }
        | none =>
          {
            aig :=
              { decls := aig.decls.push (Decl.const val), cache := Cache.insert aig.decls aig.cache (Decl.const val),
                invariant := ⋯ },
            ref := { gate := aig.decls.size, hgate := ⋯ } }).aig.decls =
    aig.decls.push (Decl.const val)

Tactic:
split <;> simp_all

Result:
no goals

Proof state:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
val : Bool
aig : AIG α
hcache : aig.cache.get? (Decl.const val) = none
⊢ (aig.mkConstCached val).aig.decls = aig.decls.push (Decl.const val)

Tactic:
simp only [mkConstCached]

Result:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
val : Bool
aig : AIG α
hcache : aig.cache.get? (Decl.const val) = none
⊢ (match aig.cache.get? (Decl.const val) with
        | some hit =>
          { aig := { decls := aig.decls, cache := aig.cache, invariant := ⋯ }, ref := { gate := hit.idx, hgate := ⋯ } }
        | none =>
          {
            aig :=
              { decls := aig.decls.push (Decl.const val), cache := Cache.insert aig.decls aig.cache (Decl.const val),
                invariant := ⋯ },
            ref := { gate := aig.decls.size, hgate := ⋯ } }).aig.decls =
    aig.decls.push (Decl.const val)
-- Mathlib/Data/Nat/Bits.lean
theorem bit_add' : ∀ (b : Bool) (n m : ℕ), bit b (n + m) = bit b n + bit false m
  | true,  _, _ => by dsimp [bit]; omega
  | false, _, _ => by dsimp [bit]; omega

Proof state:
x✝¹ x✝ : ℕ
⊢ 2 * (x✝¹ + x✝) = 2 * x✝¹ + 2 * x✝

Tactic:
omega

Result:
no goals

Proof state:
x✝¹ x✝ : ℕ
⊢ 2 * (x✝¹ + x✝) + 1 = 2 * x✝¹ + 1 + 2 * x✝

Tactic:
omega

Result:
no goals

Proof state:
x✝¹ x✝ : ℕ
⊢ bit false (x✝¹ + x✝) = bit false x✝¹ + bit false x✝

Tactic:
dsimp [bit]

Result:
x✝¹ x✝ : ℕ
⊢ 2 * (x✝¹ + x✝) = 2 * x✝¹ + 2 * x✝

Proof state:
x✝¹ x✝ : ℕ
⊢ bit true (x✝¹ + x✝) = bit true x✝¹ + bit false x✝

Tactic:
dsimp [bit]

Result:
x✝¹ x✝ : ℕ
⊢ 2 * (x✝¹ + x✝) + 1 = 2 * x✝¹ + 1 + 2 * x✝
-- Mathlib/Data/Real/EReal.lean
lemma sub_nonpos {x y : EReal} : x - y ≤ 0 ↔ x ≤ y

Proof state:
x y : EReal
⊢ x - y ≤ 0 ↔ x ≤ y

Tactic:
cases x <;> cases y <;> simp [← EReal.coe_sub]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem mem_iff_getElem? {a} {l : Vector α n} : a ∈ l ↔ ∃ i : Nat, l[i]? = some a

Proof state:
α : Type u_1
n : Nat
a : α
l : Vector α n
⊢ a ∈ l ↔ ∃ i, l[i]? = some a

Tactic:
simp [getElem?_eq_some_iff, mem_iff_getElem]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Lemmas.lean
theorem one_lt_two_pow (h : n ≠ 0) : 1 < 2 ^ n :=
  match n, h with
  | n+1, _ => by
    rw [Nat.pow_succ', ← Nat.one_mul 1]
    exact Nat.mul_lt_mul_of_lt_of_le' (by decide) (Nat.two_pow_pos n) (by decide)

Proof state:
n✝ : Nat
h : n✝ ≠ 0
n : Nat
x✝ : n + 1 ≠ 0
⊢ 1 < 2 ^ (n + 1)

Tactic:
rw [Nat.pow_succ', ← Nat.one_mul 1]

Result:
n✝ : Nat
h : n✝ ≠ 0
n : Nat
x✝ : n + 1 ≠ 0
⊢ 1 * 1 < 2 * 2 ^ n

Proof state:
n✝ : Nat
h : n✝ ≠ 0
n : Nat
x✝ : n + 1 ≠ 0
⊢ 1 * 1 < 2 * 2 ^ n

Tactic:
exact Nat.mul_lt_mul_of_lt_of_le' (by decide) (Nat.two_pow_pos n) (by decide)

Result:
no goals

Proof state:
n✝ : Nat
h : n✝ ≠ 0
n : Nat
x✝ : n + 1 ≠ 0
⊢ 1 < 2

Tactic:
decide

Result:
no goals

Proof state:
n✝ : Nat
h : n✝ ≠ 0
n : Nat
x✝ : n + 1 ≠ 0
⊢ 0 < 1

Tactic:
decide

Result:
no goals
-- Mathlib/CategoryTheory/Galois/Prorepresentability.lean
lemma autGaloisSystem_map_surjective ⦃A B : PointedGaloisObject F⦄ (f : A ⟶ B) :
    Function.Surjective ((autGaloisSystem F).map f)

Proof state:
C : Type u₁
inst✝¹ : Category.{u₂, u₁} C
inst✝ : GaloisCategory C
F : C ⥤ FintypeCat
A B : PointedGaloisObject F
f : A ⟶ B
φ : Aut B.obj
⊢ ∃ a, (ConcreteCategory.hom ((autGaloisSystem F).map f)) a = φ

Tactic:
obtain ⟨ψ, hψ⟩ := autMap_surjective_of_isGalois f.val φ

Result:
case intro
C : Type u₁
inst✝¹ : Category.{u₂, u₁} C
inst✝ : GaloisCategory C
F : C ⥤ FintypeCat
A B : PointedGaloisObject F
f : A ⟶ B
φ : Aut B.obj
ψ : Aut A.obj
hψ : autMap f.val ψ = φ
⊢ ∃ a, (ConcreteCategory.hom ((autGaloisSystem F).map f)) a = φ

Proof state:
case intro
C : Type u₁
inst✝¹ : Category.{u₂, u₁} C
inst✝ : GaloisCategory C
F : C ⥤ FintypeCat
A B : PointedGaloisObject F
f : A ⟶ B
φ : Aut B.obj
ψ : Aut A.obj
hψ : autMap f.val ψ = φ
⊢ ∃ a, (ConcreteCategory.hom ((autGaloisSystem F).map f)) a = φ

Tactic:
use ψ

Result:
case h
C : Type u₁
inst✝¹ : Category.{u₂, u₁} C
inst✝ : GaloisCategory C
F : C ⥤ FintypeCat
A B : PointedGaloisObject F
f : A ⟶ B
φ : Aut B.obj
ψ : Aut A.obj
hψ : autMap f.val ψ = φ
⊢ (ConcreteCategory.hom ((autGaloisSystem F).map f)) ψ = φ

Proof state:
C : Type u₁
inst✝¹ : Category.{u₂, u₁} C
inst✝ : GaloisCategory C
F : C ⥤ FintypeCat
A B : PointedGaloisObject F
f : A ⟶ B
⊢ Function.Surjective ⇑(ConcreteCategory.hom ((autGaloisSystem F).map f))

Tactic:
intro (φ : Aut B.obj)

Result:
C : Type u₁
inst✝¹ : Category.{u₂, u₁} C
inst✝ : GaloisCategory C
F : C ⥤ FintypeCat
A B : PointedGaloisObject F
f : A ⟶ B
φ : Aut B.obj
⊢ ∃ a, (ConcreteCategory.hom ((autGaloisSystem F).map f)) a = φ

Proof state:
case h
C : Type u₁
inst✝¹ : Category.{u₂, u₁} C
inst✝ : GaloisCategory C
F : C ⥤ FintypeCat
A B : PointedGaloisObject F
f : A ⟶ B
φ : Aut B.obj
ψ : Aut A.obj
hψ : autMap f.val ψ = φ
⊢ (ConcreteCategory.hom (Grp.ofHom (autMapHom f.val))) ψ = φ

Tactic:
exact hψ

Result:
no goals

Proof state:
case h
C : Type u₁
inst✝¹ : Category.{u₂, u₁} C
inst✝ : GaloisCategory C
F : C ⥤ FintypeCat
A B : PointedGaloisObject F
f : A ⟶ B
φ : Aut B.obj
ψ : Aut A.obj
hψ : autMap f.val ψ = φ
⊢ (ConcreteCategory.hom ((autGaloisSystem F).map f)) ψ = φ

Tactic:
simp only [autGaloisSystem_map]

Result:
case h
C : Type u₁
inst✝¹ : Category.{u₂, u₁} C
inst✝ : GaloisCategory C
F : C ⥤ FintypeCat
A B : PointedGaloisObject F
f : A ⟶ B
φ : Aut B.obj
ψ : Aut A.obj
hψ : autMap f.val ψ = φ
⊢ (ConcreteCategory.hom (Grp.ofHom (autMapHom f.val))) ψ = φ
-- Mathlib/Topology/Order/LowerUpperTopology.lean
theorem continuous_toLower [TopologicalSpace α] [ClosedIciTopology α] :
    Continuous (toLower : α → WithLower α) :=
  continuous_generateFrom_iff.mpr <| by rintro _ ⟨a, rfl⟩; exact isClosed_Ici.isOpen_compl

Proof state:
α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : ClosedIciTopology α
⊢ ∀ s ∈ {s | ∃ a, (Ici a)ᶜ = s}, IsOpen (⇑toLower ⁻¹' s)

Tactic:
rintro _ ⟨a, rfl⟩

Result:
case intro
α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : ClosedIciTopology α
a : WithLower α
⊢ IsOpen (⇑toLower ⁻¹' (Ici a)ᶜ)

Proof state:
case intro
α : Type u_1
inst✝² : Preorder α
inst✝¹ : TopologicalSpace α
inst✝ : ClosedIciTopology α
a : WithLower α
⊢ IsOpen (⇑toLower ⁻¹' (Ici a)ᶜ)

Tactic:
exact isClosed_Ici.isOpen_compl

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Basic.lean
theorem not_isSuccLimit_of_lt_aleph0 {c : Cardinal} (h : c < ℵ₀) : ¬ IsSuccLimit c

Proof state:
c : Cardinal.{u_1}
h : c < ℵ₀
⊢ ¬IsSuccLimit c

Tactic:
obtain ⟨n, rfl⟩ := lt_aleph0.1 h

Result:
case intro
n : ℕ
h : ↑n < ℵ₀
⊢ ¬IsSuccLimit ↑n

Proof state:
case intro
n : ℕ
h : ↑n < ℵ₀
⊢ ¬IsSuccLimit ↑n

Tactic:
exact not_isSuccLimit_natCast n

Result:
no goals
-- Mathlib/Algebra/Group/Subgroup/Basic.lean
theorem characteristic_iff_map_le : H.Characteristic ↔ ∀ ϕ : G ≃* G, H.map ϕ.toMonoidHom ≤ H

Proof state:
G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ H.Characteristic ↔ ∀ (ϕ : G ≃* G), map ϕ.toMonoidHom H ≤ H

Tactic:
simp_rw [map_equiv_eq_comap_symm']

Result:
G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ H.Characteristic ↔ ∀ (ϕ : G ≃* G), comap ϕ.symm.toMonoidHom H ≤ H

Proof state:
G : Type u_1
inst✝ : Group G
H : Subgroup G
⊢ H.Characteristic ↔ ∀ (ϕ : G ≃* G), comap ϕ.symm.toMonoidHom H ≤ H

Tactic:
exact characteristic_iff_comap_le.trans ⟨fun h ϕ => h ϕ.symm, fun h ϕ => h ϕ.symm⟩

Result:
no goals
-- Mathlib/MeasureTheory/Function/SimpleFuncDenseLp.lean
theorem Integrable.induction (P : (α → E) → Prop)
    (h_ind : ∀ (c : E) ⦃s⦄, MeasurableSet s → μ s < ∞ → P (s.indicator fun _ => c))
    (h_add :
      ∀ ⦃f g : α → E⦄,
        Disjoint (support f) (support g) → Integrable f μ → Integrable g μ → P f → P g → P (f + g))
    (h_closed : IsClosed { f : α →₁[μ] E | P f })
    (h_ae : ∀ ⦃f g⦄, f =ᵐ[μ] g → Integrable f μ → P f → P g) :
    ∀ ⦃f : α → E⦄, Integrable f μ → P f

Proof state:
α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
μ : Measure α
P : (α → E) → Prop
h_ind : ∀ (c : E) ⦃s : Set α⦄, MeasurableSet s → μ s < ⊤ → P (s.indicator fun x => c)
h_add : ∀ ⦃f g : α → E⦄, Disjoint (support f) (support g) → Integrable f μ → Integrable g μ → P f → P g → P (f + g)
h_closed : IsClosed {f | P ↑↑f}
h_ae : ∀ ⦃f g : α → E⦄, f =ᶠ[ae μ] g → Integrable f μ → P f → P g
⊢ ∀ ⦃f : α → E⦄, Integrable f μ → P f

Tactic:
simp only [← memLp_one_iff_integrable] at *

Result:
α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
μ : Measure α
P : (α → E) → Prop
h_ind : ∀ (c : E) ⦃s : Set α⦄, MeasurableSet s → μ s < ⊤ → P (s.indicator fun x => c)
h_closed : IsClosed {f | P ↑↑f}
h_add : ∀ ⦃f g : α → E⦄, Disjoint (support f) (support g) → MemLp f 1 μ → MemLp g 1 μ → P f → P g → P (f + g)
h_ae : ∀ ⦃f g : α → E⦄, f =ᶠ[ae μ] g → MemLp f 1 μ → P f → P g
⊢ ∀ ⦃f : α → E⦄, MemLp f 1 μ → P f

Proof state:
α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
μ : Measure α
P : (α → E) → Prop
h_ind : ∀ (c : E) ⦃s : Set α⦄, MeasurableSet s → μ s < ⊤ → P (s.indicator fun x => c)
h_closed : IsClosed {f | P ↑↑f}
h_add : ∀ ⦃f g : α → E⦄, Disjoint (support f) (support g) → MemLp f 1 μ → MemLp g 1 μ → P f → P g → P (f + g)
h_ae : ∀ ⦃f g : α → E⦄, f =ᶠ[ae μ] g → MemLp f 1 μ → P f → P g
⊢ ∀ ⦃f : α → E⦄, MemLp f 1 μ → P f

Tactic:
exact MemLp.induction one_ne_top (P := P) h_ind h_add h_closed h_ae

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem setWidth_cast {x : BitVec w} {h : w = v} : (x.cast h).setWidth k = x.setWidth k

Proof state:
case pred
w v k : Nat
x : BitVec w
h : w = v
⊢ ∀ (i : Nat), i < k → (setWidth k (BitVec.cast h x)).getLsbD i = (setWidth k x).getLsbD i

Tactic:
simp

Result:
no goals

Proof state:
w v k : Nat
x : BitVec w
h : w = v
⊢ setWidth k (BitVec.cast h x) = setWidth k x

Tactic:
apply eq_of_getLsbD_eq

Result:
case pred
w v k : Nat
x : BitVec w
h : w = v
⊢ ∀ (i : Nat), i < k → (setWidth k (BitVec.cast h x)).getLsbD i = (setWidth k x).getLsbD i
-- Mathlib/AlgebraicGeometry/Morphisms/QuasiSeparated.lean
theorem quasiSeparatedSpace_of_quasiSeparated {X Y : Scheme} (f : X ⟶ Y)
    [hY : QuasiSeparatedSpace Y] [QuasiSeparated f] : QuasiSeparatedSpace X

Proof state:
X Y : Scheme
f : X ⟶ Y
hY : QuasiSeparated (terminal.from Y)
inst✝ : QuasiSeparated f
⊢ QuasiSeparated (f ≫ terminal.from Y)

Tactic:
infer_instance

Result:
no goals

Proof state:
X Y : Scheme
f : X ⟶ Y
hY : QuasiSeparated (terminal.from Y)
inst✝ : QuasiSeparated f
⊢ QuasiSeparated (terminal.from X)

Tactic:
rw [← terminalIsTerminal.hom_ext (f ≫ terminal.from Y) (terminal.from X)]

Result:
X Y : Scheme
f : X ⟶ Y
hY : QuasiSeparated (terminal.from Y)
inst✝ : QuasiSeparated f
⊢ QuasiSeparated (f ≫ terminal.from Y)

Proof state:
X Y : Scheme
f : X ⟶ Y
hY : QuasiSeparatedSpace ↑↑Y.toPresheafedSpace
inst✝ : QuasiSeparated f
⊢ QuasiSeparatedSpace ↑↑X.toPresheafedSpace

Tactic:
rw [quasiSeparatedSpace_iff_quasiSeparated] at hY ⊢

Result:
X Y : Scheme
f : X ⟶ Y
hY : QuasiSeparated (terminal.from Y)
inst✝ : QuasiSeparated f
⊢ QuasiSeparated (terminal.from X)
-- Mathlib/MeasureTheory/Function/LpSpace/Basic.lean
theorem Lp.norm_const' (hp_zero : p ≠ 0) (hp_top : p ≠ ∞) :
    ‖Lp.const p μ c‖ = ‖c‖ * (μ Set.univ).toReal ^ (1 / p.toReal)

Proof state:
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝¹ : NormedAddCommGroup E
inst✝ : IsFiniteMeasure μ
c : E
hp_zero : p ≠ 0
hp_top : p ≠ ⊤
⊢ (‖c‖ₑ * μ Set.univ ^ (1 / p.toReal)).toReal = ‖c‖ * (μ Set.univ).toReal ^ (1 / p.toReal)

Tactic:
rw [ENNReal.toReal_mul, toReal_enorm, ← ENNReal.toReal_rpow]

Result:
no goals

Proof state:
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝¹ : NormedAddCommGroup E
inst✝ : IsFiniteMeasure μ
c : E
hp_zero : p ≠ 0
hp_top : p ≠ ⊤
⊢ ‖(Lp.const p μ) c‖ = ‖c‖ * (μ Set.univ).toReal ^ (1 / p.toReal)

Tactic:
rw [← MemLp.toLp_const, Lp.norm_toLp, eLpNorm_const'] <;> try assumption

Result:
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝¹ : NormedAddCommGroup E
inst✝ : IsFiniteMeasure μ
c : E
hp_zero : p ≠ 0
hp_top : p ≠ ⊤
⊢ (‖c‖ₑ * μ Set.univ ^ (1 / p.toReal)).toReal = ‖c‖ * (μ Set.univ).toReal ^ (1 / p.toReal)

Proof state:
case h_top
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝¹ : NormedAddCommGroup E
inst✝ : IsFiniteMeasure μ
c : E
hp_zero : p ≠ 0
hp_top : p ≠ ⊤
⊢ p ≠ ⊤

Tactic:
assumption

Result:
no goals
-- Mathlib/AlgebraicGeometry/OpenImmersion.lean
theorem image_basicOpen {U : X.Opens} (r : Γ(X, U)) :
    f ''ᵁ X.basicOpen r = Y.basicOpen ((f.appIso U).inv r)

Proof state:
X Y : Scheme
f : X ⟶ Y
H : IsOpenImmersion f
U : X.Opens
r : ↑Γ(X, U)
e :
  f ⁻¹ᵁ Y.basicOpen ((ConcreteCategory.hom (Hom.appIso f U).inv) r) =
    X.basicOpen ((ConcreteCategory.hom (Hom.app f (f ''ᵁ U))) ((ConcreteCategory.hom (Hom.appIso f U).inv) r))
⊢ f ''ᵁ X.basicOpen r = Y.basicOpen ((ConcreteCategory.hom (Hom.appIso f U).inv) r)

Tactic:
rw [Scheme.Hom.appIso_inv_app_apply, Scheme.basicOpen_res, inf_eq_right.mpr _] at e

Result:
X Y : Scheme
f : X ⟶ Y
H : IsOpenImmersion f
U : X.Opens
r : ↑Γ(X, U)
e : f ⁻¹ᵁ Y.basicOpen ((ConcreteCategory.hom (Hom.appIso f U).inv) r) = X.basicOpen r
⊢ f ''ᵁ X.basicOpen r = Y.basicOpen ((ConcreteCategory.hom (Hom.appIso f U).inv) r)

X Y : Scheme
f : X ⟶ Y
H : IsOpenImmersion f
U : X.Opens
r : ↑Γ(X, U)
e : f ⁻¹ᵁ Y.basicOpen ((ConcreteCategory.hom (Hom.appIso f U).inv) r) = f ⁻¹ᵁ f ''ᵁ U ⊓ X.basicOpen r
⊢ X.basicOpen r ≤ f ⁻¹ᵁ f ''ᵁ U

Proof state:
X Y : Scheme
f : X ⟶ Y
H : IsOpenImmersion f
U : X.Opens
r : ↑Γ(X, U)
e : f ⁻¹ᵁ Y.basicOpen ((ConcreteCategory.hom (Hom.appIso f U).inv) r) = X.basicOpen r
⊢ f ''ᵁ X.basicOpen r = Y.basicOpen ((ConcreteCategory.hom (Hom.appIso f U).inv) r)

Tactic:
rw [← e, f.image_preimage_eq_opensRange_inter, inf_eq_right]

Result:
X Y : Scheme
f : X ⟶ Y
H : IsOpenImmersion f
U : X.Opens
r : ↑Γ(X, U)
e : f ⁻¹ᵁ Y.basicOpen ((ConcreteCategory.hom (Hom.appIso f U).inv) r) = X.basicOpen r
⊢ Y.basicOpen ((ConcreteCategory.hom (Hom.appIso f U).inv) r) ≤ Hom.opensRange f

Proof state:
X Y : Scheme
f : X ⟶ Y
H : IsOpenImmersion f
U : X.Opens
r : ↑Γ(X, U)
⊢ f ''ᵁ X.basicOpen r = Y.basicOpen ((ConcreteCategory.hom (Hom.appIso f U).inv) r)

Tactic:
have e := Scheme.preimage_basicOpen f ((f.appIso U).inv r)

Result:
X Y : Scheme
f : X ⟶ Y
H : IsOpenImmersion f
U : X.Opens
r : ↑Γ(X, U)
e :
  f ⁻¹ᵁ Y.basicOpen ((ConcreteCategory.hom (Hom.appIso f U).inv) r) =
    X.basicOpen ((ConcreteCategory.hom (Hom.app f (f ''ᵁ U))) ((ConcreteCategory.hom (Hom.appIso f U).inv) r))
⊢ f ''ᵁ X.basicOpen r = Y.basicOpen ((ConcreteCategory.hom (Hom.appIso f U).inv) r)

Proof state:
X Y : Scheme
f : X ⟶ Y
H : IsOpenImmersion f
U : X.Opens
r : ↑Γ(X, U)
e : f ⁻¹ᵁ Y.basicOpen ((ConcreteCategory.hom (Hom.appIso f U).inv) r) = f ⁻¹ᵁ f ''ᵁ U ⊓ X.basicOpen r
⊢ X.basicOpen r ≤ f ⁻¹ᵁ f ''ᵁ U

Tactic:
exact (X.basicOpen_le r).trans (f.preimage_image_eq _).ge

Result:
no goals

Proof state:
X Y : Scheme
f : X ⟶ Y
H : IsOpenImmersion f
U : X.Opens
r : ↑Γ(X, U)
e : f ⁻¹ᵁ Y.basicOpen ((ConcreteCategory.hom (Hom.appIso f U).inv) r) = X.basicOpen r
⊢ Y.basicOpen ((ConcreteCategory.hom (Hom.appIso f U).inv) r) ≤ Hom.opensRange f

Tactic:
refine Set.Subset.trans (Scheme.basicOpen_le _ _) (Set.image_subset_range _ _)

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/MapIdx.lean
theorem mapFinIdx_push {l : Array α} {a : α} {f : (i : Nat) → α → (h : i < (l.push a).size) → β} :
    mapFinIdx (l.push a) f =
      (mapFinIdx l (fun i a h => f i a (by simp; omega))).push (f l.size a (by simp))

Proof state:
α : Type ?u.56159
β : Type ?u.56188
l : Array α
a✝ : α
f : (i : Nat) → α → i < (l.push a✝).size → β
i : Nat
a : α
h : i < l.size
⊢ i < (l.push a✝).size

Tactic:
simp

Result:
α : Type ?u.56159
β : Type ?u.56188
l : Array α
a✝ : α
f : (i : Nat) → α → i < (l.push a✝).size → β
i : Nat
a : α
h : i < l.size
⊢ i < l.size + 1

Proof state:
α : Type ?u.56159
β : Type ?u.56188
l : Array α
a✝ : α
f : (i : Nat) → α → i < (l.push a✝).size → β
i : Nat
a : α
h : i < l.size
⊢ i < l.size + 1

Tactic:
omega

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
l : Array α
a : α
f : (i : Nat) → α → i < (l.push a).size → β
⊢ (l.push a).mapFinIdx f = (l.mapFinIdx fun i a_1 h => f i a_1 ⋯).push (f l.size a ⋯)

Tactic:
simp [← append_singleton, mapFinIdx_append]

Result:
no goals

Proof state:
α : Type ?u.56159
β : Type ?u.56188
l : Array α
a : α
f : (i : Nat) → α → i < (l.push a).size → β
⊢ l.size < (l.push a).size

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Num/Lemmas.lean
theorem add_succ : ∀ m n : Num, m + succ n = succ (m + n)
  | 0, n => by simp [zero_add]
  | pos p, 0 => show pos (p + 1) = succ (pos p + 0) by rw [PosNum.add_one, add_zero, succ, succ']
  | pos _, pos _ => congr_arg pos (PosNum.add_succ _ _)

Proof state:
p : PosNum
⊢ pos (p + 1) = (pos p + 0).succ

Tactic:
rw [PosNum.add_one, add_zero, succ, succ']

Result:
no goals

Proof state:
n : Num
⊢ 0 + n.succ = (0 + n).succ

Tactic:
simp [zero_add]

Result:
no goals