harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/CategoryTheory/EqToHom.lean
theorem congrArg_mpr_hom_right {X Y Z : C} (p : X ⟶ Y) (q : Z = Y) :
    (congrArg (fun W : C => X ⟶ W) q).mpr p = p ≫ eqToHom q.symm

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y Z : C
p : X ⟶ Y
q : Z = Y
⊢ ⋯.mpr p = p ≫ eqToHom ⋯

Tactic:
cases q

Result:
case refl
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
p : X ⟶ Y
⊢ ⋯.mpr p = p ≫ eqToHom ⋯

Proof state:
case refl
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y : C
p : X ⟶ Y
⊢ ⋯.mpr p = p ≫ eqToHom ⋯

Tactic:
simp

Result:
no goals
-- Mathlib/GroupTheory/SemidirectProduct.lean
theorem map_inr (g : G₁) : map fn fg h (inr g) = inr (fg g)

Proof state:
N₁ : Type u_4
G₁ : Type u_5
N₂ : Type u_6
G₂ : Type u_7
inst✝³ : Group N₁
inst✝² : Group G₁
inst✝¹ : Group N₂
inst✝ : Group G₂
φ₁ : G₁ →* MulAut N₁
φ₂ : G₂ →* MulAut N₂
fn : N₁ →* N₂
fg : G₁ →* G₂
h : ∀ (g : G₁), fn.comp (MulEquiv.toMonoidHom (φ₁ g)) = (MulEquiv.toMonoidHom (φ₂ (fg g))).comp fn
g : G₁
⊢ (map fn fg h) (inr g) = inr (fg g)

Tactic:
simp [map]

Result:
no goals
-- Mathlib/Algebra/Group/UniqueProds/Basic.lean
theorem to_mulOpposite (h : UniqueMul A B a0 b0) :
    UniqueMul (B.map ⟨_, op_injective⟩) (A.map ⟨_, op_injective⟩) (op b0) (op a0) :=
  of_mulOpposite (by simp_rw [map_map]; exact (mulHom_map_iff _ fun _ _ ↦ by rfl).mpr h)

Proof state:
G : Type u_1
inst✝ : Mul G
A B : Finset G
a0 b0 : G
h : UniqueMul A B a0 b0
x✝¹ x✝ : G
⊢ ({ toFun := op, inj' := ⋯ }.trans { toFun := op, inj' := ⋯ }) (x✝¹ * x✝) =
    ({ toFun := op, inj' := ⋯ }.trans { toFun := op, inj' := ⋯ }) x✝¹ *
      ({ toFun := op, inj' := ⋯ }.trans { toFun := op, inj' := ⋯ }) x✝

Tactic:
rfl

Result:
no goals

Proof state:
G : Type u_1
inst✝ : Mul G
A B : Finset G
a0 b0 : G
h : UniqueMul A B a0 b0
⊢ UniqueMul (map { toFun := op, inj' := ⋯ } (map { toFun := op, inj' := ⋯ } A))
    (map { toFun := op, inj' := ⋯ } (map { toFun := op, inj' := ⋯ } B)) (op (op a0)) (op (op b0))

Tactic:
simp_rw [map_map]

Result:
G : Type u_1
inst✝ : Mul G
A B : Finset G
a0 b0 : G
h : UniqueMul A B a0 b0
⊢ UniqueMul (map ({ toFun := op, inj' := ⋯ }.trans { toFun := op, inj' := ⋯ }) A)
    (map ({ toFun := op, inj' := ⋯ }.trans { toFun := op, inj' := ⋯ }) B) (op (op a0)) (op (op b0))

Proof state:
G : Type u_1
inst✝ : Mul G
A B : Finset G
a0 b0 : G
h : UniqueMul A B a0 b0
⊢ UniqueMul (map ({ toFun := op, inj' := ⋯ }.trans { toFun := op, inj' := ⋯ }) A)
    (map ({ toFun := op, inj' := ⋯ }.trans { toFun := op, inj' := ⋯ }) B) (op (op a0)) (op (op b0))

Tactic:
exact (mulHom_map_iff _ fun _ _ ↦ by rfl).mpr h

Result:
no goals
-- Mathlib/Algebra/Order/Monoid/Unbundled/Basic.lean
theorem mul_le_mul_iff_right [Mul α] [i : @Std.Commutative α (· * ·)]
    [MulLeftMono α] {a b c : α} (ha : MulLECancellable a) :
    b * a ≤ c * a ↔ b ≤ c

Proof state:
α : Type u_1
inst✝² : LE α
inst✝¹ : Mul α
i : Std.Commutative fun x1 x2 => x1 * x2
inst✝ : MulLeftMono α
a b c : α
ha : MulLECancellable a
⊢ b * a ≤ c * a ↔ b ≤ c

Tactic:
rw [i.comm b, i.comm c, ha.mul_le_mul_iff_left]

Result:
no goals
-- Mathlib/Order/Sublattice.lean
lemma pi_univ_bot [Nonempty κ] : (pi univ fun _ ↦ ⊥ : Sublattice (∀ i, π i)) = ⊥

Proof state:
κ : Type u_5
π : κ → Type u_6
inst✝¹ : (i : κ) → Lattice (π i)
inst✝ : Nonempty κ
⊢ (pi univ fun x => ⊥) = ⊥

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/SizeOfLemmas.lean
theorem UInt32.sizeOf (a : UInt32) : sizeOf a = a.toNat + 3

Proof state:
case mk
toBitVec✝ : BitVec 32
⊢ sizeOf { toBitVec := toBitVec✝ } = { toBitVec := toBitVec✝ }.toNat + 3

Tactic:
simp_arith [UInt32.toNat, BitVec.toNat]

Result:
no goals

Proof state:
a : UInt32
⊢ sizeOf a = a.toNat + 3

Tactic:
cases a

Result:
case mk
toBitVec✝ : BitVec 32
⊢ sizeOf { toBitVec := toBitVec✝ } = { toBitVec := toBitVec✝ }.toNat + 3
-- Mathlib/Data/Matroid/Circuit.lean
lemma empty_not_isCircuit (M : Matroid α) : ¬M.IsCircuit ∅ :=
  fun h ↦ by simpa using h.nonempty

Proof state:
α : Type u_1
M : Matroid α
h : M.IsCircuit ∅
⊢ False

Tactic:
simpa using h.nonempty

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/String/Lemmas.lean
theorem contains (c) : ∀ {s}, ValidFor l m r s → (s.contains c ↔ c ∈ m)
  | _, h => by simp [Substring.contains, h.any, String.contains]

Proof state:
l m r : List Char
c : Char
x✝ : Substring
h : ValidFor l m r x✝
⊢ x✝.contains c = true ↔ c ∈ m

Tactic:
simp [Substring.contains, h.any, String.contains]

Result:
no goals
-- Mathlib/Algebra/Ring/Identities.lean
theorem sum_eight_sq_mul_sum_eight_sq :
    (x₁ ^ 2 + x₂ ^ 2 + x₃ ^ 2 + x₄ ^ 2 + x₅ ^ 2 + x₆ ^ 2 + x₇ ^ 2 + x₈ ^ 2) *
      (y₁ ^ 2 + y₂ ^ 2 + y₃ ^ 2 + y₄ ^ 2 + y₅ ^ 2 + y₆ ^ 2 + y₇ ^ 2 + y₈ ^ 2) =
    (x₁ * y₁ - x₂ * y₂ - x₃ * y₃ - x₄ * y₄ - x₅ * y₅ - x₆ * y₆ - x₇ * y₇ - x₈ * y₈) ^ 2 +
      (x₁ * y₂ + x₂ * y₁ + x₃ * y₄ - x₄ * y₃ + x₅ * y₆ - x₆ * y₅ - x₇ * y₈ + x₈ * y₇) ^ 2 +
      (x₁ * y₃ - x₂ * y₄ + x₃ * y₁ + x₄ * y₂ + x₅ * y₇ + x₆ * y₈ - x₇ * y₅ - x₈ * y₆) ^ 2 +
      (x₁ * y₄ + x₂ * y₃ - x₃ * y₂ + x₄ * y₁ + x₅ * y₈ - x₆ * y₇ + x₇ * y₆ - x₈ * y₅) ^ 2 +
      (x₁ * y₅ - x₂ * y₆ - x₃ * y₇ - x₄ * y₈ + x₅ * y₁ + x₆ * y₂ + x₇ * y₃ + x₈ * y₄) ^ 2 +
      (x₁ * y₆ + x₂ * y₅ - x₃ * y₈ + x₄ * y₇ - x₅ * y₂ + x₆ * y₁ - x₇ * y₄ + x₈ * y₃) ^ 2 +
      (x₁ * y₇ + x₂ * y₈ + x₃ * y₅ - x₄ * y₆ - x₅ * y₃ + x₆ * y₄ + x₇ * y₁ - x₈ * y₂) ^ 2 +
      (x₁ * y₈ - x₂ * y₇ + x₃ * y₆ + x₄ * y₅ - x₅ * y₄ - x₆ * y₃ + x₇ * y₂ + x₈ * y₁) ^ 2

Proof state:
R : Type u_1
inst✝ : CommRing R
x₁ x₂ x₃ x₄ x₅ x₆ x₇ x₈ y₁ y₂ y₃ y₄ y₅ y₆ y₇ y₈ : R
⊢ (x₁ ^ 2 + x₂ ^ 2 + x₃ ^ 2 + x₄ ^ 2 + x₅ ^ 2 + x₆ ^ 2 + x₇ ^ 2 + x₈ ^ 2) *
      (y₁ ^ 2 + y₂ ^ 2 + y₃ ^ 2 + y₄ ^ 2 + y₅ ^ 2 + y₆ ^ 2 + y₇ ^ 2 + y₈ ^ 2) =
    (x₁ * y₁ - x₂ * y₂ - x₃ * y₃ - x₄ * y₄ - x₅ * y₅ - x₆ * y₆ - x₇ * y₇ - x₈ * y₈) ^ 2 +
                  (x₁ * y₂ + x₂ * y₁ + x₃ * y₄ - x₄ * y₃ + x₅ * y₆ - x₆ * y₅ - x₇ * y₈ + x₈ * y₇) ^ 2 +
                (x₁ * y₃ - x₂ * y₄ + x₃ * y₁ + x₄ * y₂ + x₅ * y₇ + x₆ * y₈ - x₇ * y₅ - x₈ * y₆) ^ 2 +
              (x₁ * y₄ + x₂ * y₃ - x₃ * y₂ + x₄ * y₁ + x₅ * y₈ - x₆ * y₇ + x₇ * y₆ - x₈ * y₅) ^ 2 +
            (x₁ * y₅ - x₂ * y₆ - x₃ * y₇ - x₄ * y₈ + x₅ * y₁ + x₆ * y₂ + x₇ * y₃ + x₈ * y₄) ^ 2 +
          (x₁ * y₆ + x₂ * y₅ - x₃ * y₈ + x₄ * y₇ - x₅ * y₂ + x₆ * y₁ - x₇ * y₄ + x₈ * y₃) ^ 2 +
        (x₁ * y₇ + x₂ * y₈ + x₃ * y₅ - x₄ * y₆ - x₅ * y₃ + x₆ * y₄ + x₇ * y₁ - x₈ * y₂) ^ 2 +
      (x₁ * y₈ - x₂ * y₇ + x₃ * y₆ + x₄ * y₅ - x₅ * y₄ - x₆ * y₃ + x₇ * y₂ + x₈ * y₁) ^ 2

Tactic:
ring

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Core.lean
theorem beq_false_of_ne [BEq α] [LawfulBEq α] {a b : α} (h : a ≠ b) : (a == b) = false :=
  have : ¬ (a == b) = true

Proof state:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a b : α
h : a ≠ b
h' : (a == b) = true
⊢ False

Tactic:
rw [eq_of_beq h'] at h

Result:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a b : α
h : b ≠ b
h' : (a == b) = true
⊢ False

Proof state:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a b : α
h : b ≠ b
h' : (a == b) = true
⊢ False

Tactic:
contradiction

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a b : α
h : a ≠ b
⊢ ¬(a == b) = true

Tactic:
intro h'

Result:
α : Type u_1
inst✝¹ : BEq α
inst✝ : LawfulBEq α
a b : α
h : a ≠ b
h' : (a == b) = true
⊢ False
-- Mathlib/Geometry/Manifold/VectorField.lean
lemma mpullback_add_apply :
    mpullback I I' f (V + V₁) x = mpullback I I' f V x + mpullback I I' f V₁ x

Proof state:
𝕜 : Type u_1
inst✝¹⁰ : NontriviallyNormedField 𝕜
H : Type u_2
inst✝⁹ : TopologicalSpace H
E : Type u_3
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁶ : TopologicalSpace M
inst✝⁵ : ChartedSpace H M
H' : Type u_5
inst✝⁴ : TopologicalSpace H'
E' : Type u_6
inst✝³ : NormedAddCommGroup E'
inst✝² : NormedSpace 𝕜 E'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
f : M → M'
x : M
V V₁ : (x : M') → TangentSpace I' x
⊢ mpullback I I' f (V + V₁) x = mpullback I I' f V x + mpullback I I' f V₁ x

Tactic:
simp [mpullback_apply]

Result:
no goals
-- Mathlib/CategoryTheory/Shift/CommShift.lean
@[simp, reassoc]
lemma map_shiftFunctorCompIsoId_inv_app [F.CommShift A] (X : C) (a b : A) (h : a + b = 0) :
    F.map ((shiftFunctorCompIsoId C a b h).inv.app X) =
      (shiftFunctorCompIsoId D a b h).inv.app (F.obj X) ≫
        ((F.commShiftIso a).inv.app X)⟦b⟧' ≫ (F.commShiftIso b).inv.app (X⟦a⟧)

Proof state:
C : Type u_1
D : Type u_2
inst✝⁵ : Category.{u_6, u_1} C
inst✝⁴ : Category.{u_7, u_2} D
F : C ⥤ D
A : Type u_4
inst✝³ : AddMonoid A
inst✝² : HasShift C A
inst✝¹ : HasShift D A
inst✝ : F.CommShift A
X : C
a b : A
h : a + b = 0
⊢ 𝟙 (F.obj ((shiftFunctor C a ⋙ shiftFunctor C b).obj X)) =
    ((F.commShiftIso b).hom.app ((shiftFunctor C a).obj X) ≫
        (shiftFunctor D b).map ((F.commShiftIso a).hom.app X) ≫ (shiftFunctorCompIsoId D a b h).hom.app (F.obj X)) ≫
      (shiftFunctorCompIsoId D a b h).inv.app (F.obj X) ≫
        (shiftFunctor D b).map ((F.commShiftIso a).inv.app X) ≫ (F.commShiftIso b).inv.app ((shiftFunctor C a).obj X)

Tactic:
simp only [comp_obj, id_obj, Category.assoc, Iso.hom_inv_id_app_assoc,
  ← Functor.map_comp_assoc, Iso.hom_inv_id_app, Functor.map_id, Category.id_comp]

Result:
no goals

Proof state:
C : Type u_1
D : Type u_2
inst✝⁵ : Category.{u_6, u_1} C
inst✝⁴ : Category.{u_7, u_2} D
F : C ⥤ D
A : Type u_4
inst✝³ : AddMonoid A
inst✝² : HasShift C A
inst✝¹ : HasShift D A
inst✝ : F.CommShift A
X : C
a b : A
h : a + b = 0
⊢ F.map ((shiftFunctorCompIsoId C a b h).inv.app X) =
    (shiftFunctorCompIsoId D a b h).inv.app (F.obj X) ≫
      (shiftFunctor D b).map ((F.commShiftIso a).inv.app X) ≫ (F.commShiftIso b).inv.app ((shiftFunctor C a).obj X)

Tactic:
rw [← cancel_epi (F.map ((shiftFunctorCompIsoId C a b h).hom.app X)), ← F.map_comp,
  Iso.hom_inv_id_app, F.map_id, map_shiftFunctorCompIsoId_hom_app]

Result:
C : Type u_1
D : Type u_2
inst✝⁵ : Category.{u_6, u_1} C
inst✝⁴ : Category.{u_7, u_2} D
F : C ⥤ D
A : Type u_4
inst✝³ : AddMonoid A
inst✝² : HasShift C A
inst✝¹ : HasShift D A
inst✝ : F.CommShift A
X : C
a b : A
h : a + b = 0
⊢ 𝟙 (F.obj ((shiftFunctor C a ⋙ shiftFunctor C b).obj X)) =
    ((F.commShiftIso b).hom.app ((shiftFunctor C a).obj X) ≫
        (shiftFunctor D b).map ((F.commShiftIso a).hom.app X) ≫ (shiftFunctorCompIsoId D a b h).hom.app (F.obj X)) ≫
      (shiftFunctorCompIsoId D a b h).inv.app (F.obj X) ≫
        (shiftFunctor D b).map ((F.commShiftIso a).inv.app X) ≫ (F.commShiftIso b).inv.app ((shiftFunctor C a).obj X)
-- Mathlib/Data/Set/Card.lean
theorem ncard_diff_add_ncard_of_subset (h : s ⊆ t) (ht : t.Finite

Proof state:
α : Type u_1
s t : Set α
h : s ⊆ t
ht : autoParam t.Finite _auto✝
⊢ ↑(t \ s).ncard + ↑s.ncard = ↑t.ncard

Tactic:
rw [ht.cast_ncard_eq, (ht.subset h).cast_ncard_eq, ht.diff.cast_ncard_eq,
  encard_diff_add_encard_of_subset h]

Result:
no goals

Proof state:
α : Type u_1
s t : Set α
h : s ⊆ t
ht : autoParam t.Finite _auto✝
⊢ (t \ s).ncard + s.ncard = t.ncard

Tactic:
to_encard_tac

Result:
α : Type u_1
s t : Set α
h : s ⊆ t
ht : autoParam t.Finite _auto✝
⊢ ↑(t \ s).ncard + ↑s.ncard = ↑t.ncard
-- Mathlib/RingTheory/Finiteness/Basic.lean
theorem fg_restrictScalars {R S M : Type*} [CommSemiring R] [Semiring S] [Algebra R S]
    [AddCommGroup M] [Module S M] [Module R M] [IsScalarTower R S M] (N : Submodule S M)
    (hfin : N.FG) (h : Function.Surjective (algebraMap R S)) :
    (Submodule.restrictScalars R N).FG

Proof state:
case intro
R : Type u_4
S : Type u_5
M : Type u_6
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring S
inst✝⁴ : Algebra R S
inst✝³ : AddCommGroup M
inst✝² : Module S M
inst✝¹ : Module R M
inst✝ : IsScalarTower R S M
h : Surjective ⇑(algebraMap R S)
X : Finset M
⊢ (restrictScalars R (span S ↑X)).FG

Tactic:
use X

Result:
case h
R : Type u_4
S : Type u_5
M : Type u_6
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring S
inst✝⁴ : Algebra R S
inst✝³ : AddCommGroup M
inst✝² : Module S M
inst✝¹ : Module R M
inst✝ : IsScalarTower R S M
h : Surjective ⇑(algebraMap R S)
X : Finset M
⊢ span R ↑X = restrictScalars R (span S ↑X)

Proof state:
R : Type u_4
S : Type u_5
M : Type u_6
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring S
inst✝⁴ : Algebra R S
inst✝³ : AddCommGroup M
inst✝² : Module S M
inst✝¹ : Module R M
inst✝ : IsScalarTower R S M
N : Submodule S M
hfin : N.FG
h : Surjective ⇑(algebraMap R S)
⊢ (restrictScalars R N).FG

Tactic:
obtain ⟨X, rfl⟩ := hfin

Result:
case intro
R : Type u_4
S : Type u_5
M : Type u_6
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring S
inst✝⁴ : Algebra R S
inst✝³ : AddCommGroup M
inst✝² : Module S M
inst✝¹ : Module R M
inst✝ : IsScalarTower R S M
h : Surjective ⇑(algebraMap R S)
X : Finset M
⊢ (restrictScalars R (span S ↑X)).FG

Proof state:
case h
R : Type u_4
S : Type u_5
M : Type u_6
inst✝⁶ : CommSemiring R
inst✝⁵ : Semiring S
inst✝⁴ : Algebra R S
inst✝³ : AddCommGroup M
inst✝² : Module S M
inst✝¹ : Module R M
inst✝ : IsScalarTower R S M
h : Surjective ⇑(algebraMap R S)
X : Finset M
⊢ span R ↑X = restrictScalars R (span S ↑X)

Tactic:
exact (Submodule.restrictScalars_span R S h (X : Set M)).symm

Result:
no goals
-- Mathlib/Algebra/Homology/TotalComplex.lean
@[reassoc (attr := simp)]
lemma ι_D₂ (i₁₂ i₁₂' : I₁₂) (i₁ : I₁) (i₂ : I₂)
    (h : ComplexShape.π c₁ c₂ c₁₂ ⟨i₁, i₂⟩ = i₁₂) :
    K.ιTotal c₁₂ i₁ i₂ i₁₂ h ≫ K.D₂ c₁₂ i₁₂ i₁₂' =
      K.d₂ c₁₂ i₁ i₂ i₁₂'

Proof state:
C : Type u_1
inst✝⁴ : Category.{u_5, u_1} C
inst✝³ : Preadditive C
I₁ : Type u_2
I₂ : Type u_3
I₁₂ : Type u_4
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K : HomologicalComplex₂ C c₁ c₂
c₁₂ : ComplexShape I₁₂
inst✝² : TotalComplexShape c₁ c₂ c₁₂
inst✝¹ : DecidableEq I₁₂
inst✝ : K.HasTotal c₁₂
i₁₂ i₁₂' : I₁₂
i₁ : I₁
i₂ : I₂
h : c₁.π c₂ c₁₂ (i₁, i₂) = i₁₂
⊢ K.ιTotal c₁₂ i₁ i₂ i₁₂ h ≫ K.D₂ c₁₂ i₁₂ i₁₂' = K.d₂ c₁₂ i₁ i₂ i₁₂'

Tactic:
apply totalAux.ιMapObj_D₂

Result:
no goals
-- Mathlib/Analysis/BoxIntegral/Partition/Filter.lean
theorem rCond_of_bRiemann_eq_false {ι} (l : IntegrationParams) (hl : l.bRiemann = false)
    {r : (ι → ℝ) → Ioi (0 : ℝ)} : l.RCond r

Proof state:
ι : Type u_2
l : IntegrationParams
hl : l.bRiemann = false
r : (ι → ℝ) → ↑(Set.Ioi 0)
⊢ l.RCond r

Tactic:
simp [RCond, hl]

Result:
no goals
-- Mathlib/Probability/Kernel/Disintegration/Density.lean
lemma eLpNorm_densityProcess_le (hκν : fst κ ≤ ν) (n : ℕ) (a : α) (s : Set β) :
    eLpNorm (fun x ↦ densityProcess κ ν n a x s) 1 (ν a) ≤ ν a univ

Proof state:
case refine_1
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
n : ℕ
a : α
s : Set β
x : γ
⊢ ‖κ.densityProcess ν n a x s‖ ≤ 1

Tactic:
simp only [Real.norm_eq_abs, abs_of_nonneg (densityProcess_nonneg κ ν n a x s),
  densityProcess_le_one hκν n a x s]

Result:
no goals

Proof state:
case refine_2
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
n : ℕ
a : α
s : Set β
⊢ (ν a) univ ^ (ENNReal.toReal 1)⁻¹ * ENNReal.ofReal 1 ≤ (ν a) univ

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
n : ℕ
a : α
s : Set β
⊢ eLpNorm (fun x => κ.densityProcess ν n a x s) 1 (ν a) ≤ (ν a) univ

Tactic:
refine (eLpNorm_le_of_ae_bound (C := 1) (ae_of_all _ (fun x ↦ ?_))).trans ?_

Result:
case refine_1
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
n : ℕ
a : α
s : Set β
x : γ
⊢ ‖κ.densityProcess ν n a x s‖ ≤ 1

case refine_2
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝ : CountablyGenerated γ
κ : Kernel α (γ × β)
ν : Kernel α γ
hκν : κ.fst ≤ ν
n : ℕ
a : α
s : Set β
⊢ (ν a) univ ^ (ENNReal.toReal 1)⁻¹ * ENNReal.ofReal 1 ≤ (ν a) univ
-- Mathlib/Topology/Sheaves/Skyscraper.lean
theorem SkyscraperPresheafFunctor.map'_comp {a b c : C} (f : a ⟶ b) (g : b ⟶ c) :
    SkyscraperPresheafFunctor.map' p₀ (f ≫ g) =
      SkyscraperPresheafFunctor.map' p₀ f ≫ SkyscraperPresheafFunctor.map' p₀ g

Proof state:
case w
X : TopCat
p₀ : ↑X
inst✝² : (U : Opens ↑X) → Decidable (p₀ ∈ U)
C : Type v
inst✝¹ : Category.{w, v} C
inst✝ : HasTerminal C
a b c : C
f : a ⟶ b
g : b ⟶ c
U : Opens ↑X
⊢ (if h : p₀ ∈ U then eqToHom ⋯ ≫ (f ≫ g) ≫ eqToHom ⋯
    else (⋯ ▸ terminalIsTerminal).from ((skyscraperPresheaf p₀ a).obj (op U))) =
    (map' p₀ f ≫ map' p₀ g).app (op U)

Tactic:
split_ifs with h <;> aesop_cat

Result:
no goals

Proof state:
X : TopCat
p₀ : ↑X
inst✝² : (U : Opens ↑X) → Decidable (p₀ ∈ U)
C : Type v
inst✝¹ : Category.{w, v} C
inst✝ : HasTerminal C
a b c : C
f : a ⟶ b
g : b ⟶ c
⊢ map' p₀ (f ≫ g) = map' p₀ f ≫ map' p₀ g

Tactic:
ext U

Result:
case w
X : TopCat
p₀ : ↑X
inst✝² : (U : Opens ↑X) → Decidable (p₀ ∈ U)
C : Type v
inst✝¹ : Category.{w, v} C
inst✝ : HasTerminal C
a b c : C
f : a ⟶ b
g : b ⟶ c
U : Opens ↑X
⊢ (map' p₀ (f ≫ g)).app (op U) = (map' p₀ f ≫ map' p₀ g).app (op U)

Proof state:
case w
X : TopCat
p₀ : ↑X
inst✝² : (U : Opens ↑X) → Decidable (p₀ ∈ U)
C : Type v
inst✝¹ : Category.{w, v} C
inst✝ : HasTerminal C
a b c : C
f : a ⟶ b
g : b ⟶ c
U : Opens ↑X
⊢ (map' p₀ (f ≫ g)).app (op U) = (map' p₀ f ≫ map' p₀ g).app (op U)

Tactic:
simp only [SkyscraperPresheafFunctor.map'_app, NatTrans.comp_app]

Result:
case w
X : TopCat
p₀ : ↑X
inst✝² : (U : Opens ↑X) → Decidable (p₀ ∈ U)
C : Type v
inst✝¹ : Category.{w, v} C
inst✝ : HasTerminal C
a b c : C
f : a ⟶ b
g : b ⟶ c
U : Opens ↑X
⊢ (if h : p₀ ∈ U then eqToHom ⋯ ≫ (f ≫ g) ≫ eqToHom ⋯
    else (⋯ ▸ terminalIsTerminal).from ((skyscraperPresheaf p₀ a).obj (op U))) =
    (map' p₀ f ≫ map' p₀ g).app (op U)
-- Mathlib/MeasureTheory/Integral/Prod.lean
theorem MeasureTheory.AEStronglyMeasurable.prod_mk_left {γ : Type*} [SFinite ν]
    [TopologicalSpace γ] {f : α × β → γ} (hf : AEStronglyMeasurable f (μ.prod ν)) :
    ∀ᵐ x ∂μ, AEStronglyMeasurable (fun y => f (x, y)) ν

Proof state:
case h
α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
μ : Measure α
ν : Measure β
γ : Type u_4
inst✝¹ : SFinite ν
inst✝ : TopologicalSpace γ
f : α × β → γ
hf : AEStronglyMeasurable f (μ.prod ν)
x : α
hx : ∀ᵐ (y : β) ∂ν, f (x, y) = AEStronglyMeasurable.mk f hf (x, y)
⊢ AEStronglyMeasurable (fun y => f (x, y)) ν

Tactic:
exact
  ⟨fun y => hf.mk f (x, y), hf.stronglyMeasurable_mk.comp_measurable measurable_prod_mk_left, hx⟩

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
μ : Measure α
ν : Measure β
γ : Type u_4
inst✝¹ : SFinite ν
inst✝ : TopologicalSpace γ
f : α × β → γ
hf : AEStronglyMeasurable f (μ.prod ν)
⊢ ∀ᵐ (x : α) ∂μ, AEStronglyMeasurable (fun y => f (x, y)) ν

Tactic:
filter_upwards [ae_ae_of_ae_prod hf.ae_eq_mk] with x hx

Result:
case h
α : Type u_1
β : Type u_2
inst✝³ : MeasurableSpace α
inst✝² : MeasurableSpace β
μ : Measure α
ν : Measure β
γ : Type u_4
inst✝¹ : SFinite ν
inst✝ : TopologicalSpace γ
f : α × β → γ
hf : AEStronglyMeasurable f (μ.prod ν)
x : α
hx : ∀ᵐ (y : β) ∂ν, f (x, y) = AEStronglyMeasurable.mk f hf (x, y)
⊢ AEStronglyMeasurable (fun y => f (x, y)) ν
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem getKey_insertList_of_contains_eq_false [BEq α] [EquivBEq α]
    {l toInsert : List ((a : α) × β a)} {k : α}
    (not_contains : (toInsert.map Sigma.fst).contains k = false)
    {h} :
    getKey k (insertList l toInsert) h =
      getKey k l (containsKey_of_containsKey_insertList h not_contains)

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : EquivBEq α
l toInsert : List ((a : α) × β a)
k : α
not_contains : (List.map Sigma.fst toInsert).contains k = false
h : containsKey k (insertList l toInsert) = true
⊢ getKey k (insertList l toInsert) h = getKey k l ⋯

Tactic:
rw [← Option.some_inj, ← getKey?_eq_some_getKey,
  getKey?_insertList_of_contains_eq_false not_contains, getKey?_eq_some_getKey]

Result:
no goals
-- Mathlib/Data/Vector/Basic.lean
theorem scanl_singleton (v : Vector α 1) : scanl f b v = b ::ᵥ f b v.head ::ᵥ nil

Proof state:
α : Type u_1
β : Type u_6
f : β → α → β
b : β
v : Vector α 1
⊢ scanl f b (v.head ::ᵥ v.tail) = b ::ᵥ f b (v.head ::ᵥ v.tail).head ::ᵥ nil

Tactic:
simp only [scanl_cons, scanl_nil, head_cons, singleton_tail]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_6
f : β → α → β
b : β
v : Vector α 1
⊢ scanl f b v = b ::ᵥ f b v.head ::ᵥ nil

Tactic:
rw [← cons_head_tail v]

Result:
α : Type u_1
β : Type u_6
f : β → α → β
b : β
v : Vector α 1
⊢ scanl f b (v.head ::ᵥ v.tail) = b ::ᵥ f b (v.head ::ᵥ v.tail).head ::ᵥ nil
-- Mathlib/CategoryTheory/Sites/LocallySurjective.lean
theorem isLocallySurjective_iff_whisker_forget {F G : Cᵒᵖ ⥤ A} (f : F ⟶ G) :
    IsLocallySurjective J f ↔ IsLocallySurjective J (whiskerRight f (forget A))

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝² : Category.{v', u'} A
FA : A → A → Type u_1
CA : A → Type w'
inst✝¹ : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)
inst✝ : ConcreteCategory A FA
F G : Cᵒᵖ ⥤ A
f : F ⟶ G
⊢ IsLocallySurjective J f ↔ IsLocallySurjective J (whiskerRight f (forget A))

Tactic:
simp only [isLocallySurjective_iff_range_sheafify_eq_top]

Result:
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝² : Category.{v', u'} A
FA : A → A → Type u_1
CA : A → Type w'
inst✝¹ : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)
inst✝ : ConcreteCategory A FA
F G : Cᵒᵖ ⥤ A
f : F ⟶ G
⊢ Subpresheaf.sheafify J (Subpresheaf.range (whiskerRight f (forget A))) = ⊤ ↔
    Subpresheaf.sheafify J (Subpresheaf.range (whiskerRight (whiskerRight f (forget A)) (forget (Type w')))) = ⊤

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝² : Category.{v', u'} A
FA : A → A → Type u_1
CA : A → Type w'
inst✝¹ : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)
inst✝ : ConcreteCategory A FA
F G : Cᵒᵖ ⥤ A
f : F ⟶ G
⊢ Subpresheaf.sheafify J (Subpresheaf.range (whiskerRight f (forget A))) = ⊤ ↔
    Subpresheaf.sheafify J (Subpresheaf.range (whiskerRight (whiskerRight f (forget A)) (forget (Type w')))) = ⊤

Tactic:
rfl

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem set_append_right {s t : Array α} {i : Nat} {x : α}
    (h' : i < (s ++ t).size) (h : s.size ≤ i) :
    (s ++ t).set i x = s ++ t.set (i - s.size) x (by simp at h'; omega)

Proof state:
α : Type ?u.251112
s t : Array α
i : Nat
x : α
h' : i < (s ++ t).size
h : s.size ≤ i
⊢ i - s.size < t.size

Tactic:
simp at h'

Result:
α : Type ?u.251112
s t : Array α
i : Nat
x : α
h : s.size ≤ i
h' : i < s.size + t.size
⊢ i - s.size < t.size

Proof state:
α : Type u_1
s t : Array α
i : Nat
x : α
h' : i < (s ++ t).size
h : s.size ≤ i
⊢ (s ++ t).set i x h' = s ++ t.set (i - s.size) x ⋯

Tactic:
rw [set_append, dif_neg (by omega)]

Result:
no goals

Proof state:
α : Type ?u.251112
s t : Array α
i : Nat
x : α
h : s.size ≤ i
h' : i < s.size + t.size
⊢ i - s.size < t.size

Tactic:
omega

Result:
no goals

Proof state:
α : Type u_1
s t : Array α
i : Nat
x : α
h' : i < (s ++ t).size
h : s.size ≤ i
⊢ ¬i < s.size

Tactic:
omega

Result:
no goals
-- Mathlib/CategoryTheory/Abelian/Pseudoelements.lean
theorem apply_eq_zero_of_comp_eq_zero {P Q R : C} (f : Q ⟶ R) (a : P ⟶ Q) : a ≫ f = 0 → f a = 0 :=
  fun h => by simp [over_coe_def, pseudoApply_mk', Over.coe_hom, h]

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
P Q R : C
f : Q ⟶ R
a : P ⟶ Q
h : a ≫ f = 0
⊢ pseudoApply f (Quot.mk (PseudoEqual Q) (Over.mk a)) = 0

Tactic:
simp [over_coe_def, pseudoApply_mk', Over.coe_hom, h]

Result:
no goals
-- Mathlib/Data/Fin/Parity.lean
lemma not_odd_iff_even_of_even {n : ℕ} [NeZero n] (hn : Even n) {k : Fin n} : ¬Odd k ↔ Even k

Proof state:
n : ℕ
inst✝ : NeZero n
hn : Even n
k : Fin n
⊢ ¬Odd ↑k ↔ Even ↑k

Tactic:
exact Nat.not_odd_iff_even

Result:
no goals

Proof state:
n : ℕ
inst✝ : NeZero n
hn : Even n
k : Fin n
⊢ ¬Odd k ↔ Even k

Tactic:
rw [even_iff_of_even hn, odd_iff_of_even hn]

Result:
n : ℕ
inst✝ : NeZero n
hn : Even n
k : Fin n
⊢ ¬Odd ↑k ↔ Even ↑k