harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Unitary.lean
lemma unitary_iff_isStarNormal_and_spectrum_subset_unitary {u : A} :
    u ∈ unitary A ↔ IsStarNormal u ∧ spectrum ℂ u ⊆ unitary ℂ

Proof state:
A : Type u_1
inst✝⁴ : TopologicalSpace A
inst✝³ : Ring A
inst✝² : StarRing A
inst✝¹ : Algebra ℂ A
inst✝ : ContinuousFunctionalCalculus ℂ IsStarNormal
u : A
hu : IsStarNormal u
⊢ (∀ x ∈ spectrum ℂ u, star (id x) * id x = 1) ↔ ∀ x ∈ spectrum ℂ u, x ∈ ↑(unitary ℂ)

Tactic:
simp only [id_eq, RCLike.star_def, SetLike.mem_coe, unitary.mem_iff_star_mul_self]

Result:
no goals

Proof state:
A : Type u_1
inst✝⁴ : TopologicalSpace A
inst✝³ : Ring A
inst✝² : StarRing A
inst✝¹ : Algebra ℂ A
inst✝ : ContinuousFunctionalCalculus ℂ IsStarNormal
u : A
hu : IsStarNormal u
⊢ u ∈ unitary A ↔ spectrum ℂ u ⊆ ↑(unitary ℂ)

Tactic:
nth_rw 1 [← cfc_id ℂ u]

Result:
A : Type u_1
inst✝⁴ : TopologicalSpace A
inst✝³ : Ring A
inst✝² : StarRing A
inst✝¹ : Algebra ℂ A
inst✝ : ContinuousFunctionalCalculus ℂ IsStarNormal
u : A
hu : IsStarNormal u
⊢ cfc id u ∈ unitary A ↔ spectrum ℂ u ⊆ ↑(unitary ℂ)

Proof state:
A : Type u_1
inst✝⁴ : TopologicalSpace A
inst✝³ : Ring A
inst✝² : StarRing A
inst✝¹ : Algebra ℂ A
inst✝ : ContinuousFunctionalCalculus ℂ IsStarNormal
u : A
⊢ IsStarNormal u ∧ u ∈ unitary A ↔ IsStarNormal u ∧ spectrum ℂ u ⊆ ↑(unitary ℂ)

Tactic:
refine and_congr_right fun hu ↦ ?_

Result:
A : Type u_1
inst✝⁴ : TopologicalSpace A
inst✝³ : Ring A
inst✝² : StarRing A
inst✝¹ : Algebra ℂ A
inst✝ : ContinuousFunctionalCalculus ℂ IsStarNormal
u : A
hu : IsStarNormal u
⊢ u ∈ unitary A ↔ spectrum ℂ u ⊆ ↑(unitary ℂ)

Proof state:
A : Type u_1
inst✝⁴ : TopologicalSpace A
inst✝³ : Ring A
inst✝² : StarRing A
inst✝¹ : Algebra ℂ A
inst✝ : ContinuousFunctionalCalculus ℂ IsStarNormal
u : A
⊢ u ∈ unitary A ↔ IsStarNormal u ∧ spectrum ℂ u ⊆ ↑(unitary ℂ)

Tactic:
rw [← and_iff_right_of_imp isStarNormal_of_mem_unitary]

Result:
A : Type u_1
inst✝⁴ : TopologicalSpace A
inst✝³ : Ring A
inst✝² : StarRing A
inst✝¹ : Algebra ℂ A
inst✝ : ContinuousFunctionalCalculus ℂ IsStarNormal
u : A
⊢ IsStarNormal u ∧ u ∈ unitary A ↔ IsStarNormal u ∧ spectrum ℂ u ⊆ ↑(unitary ℂ)

Proof state:
A : Type u_1
inst✝⁴ : TopologicalSpace A
inst✝³ : Ring A
inst✝² : StarRing A
inst✝¹ : Algebra ℂ A
inst✝ : ContinuousFunctionalCalculus ℂ IsStarNormal
u : A
hu : IsStarNormal u
⊢ cfc id u ∈ unitary A ↔ spectrum ℂ u ⊆ ↑(unitary ℂ)

Tactic:
rw [cfc_unitary_iff id u, Set.subset_def]

Result:
A : Type u_1
inst✝⁴ : TopologicalSpace A
inst✝³ : Ring A
inst✝² : StarRing A
inst✝¹ : Algebra ℂ A
inst✝ : ContinuousFunctionalCalculus ℂ IsStarNormal
u : A
hu : IsStarNormal u
⊢ (∀ x ∈ spectrum ℂ u, star (id x) * id x = 1) ↔ ∀ x ∈ spectrum ℂ u, x ∈ ↑(unitary ℂ)
-- Mathlib/Algebra/Homology/HomologicalComplex.lean
theorem d_comp_d (C : HomologicalComplex V c) (i j k : ι) : C.d i j ≫ C.d j k = 0

Proof state:
case pos
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
C : HomologicalComplex V c
i j k : ι
hij : c.Rel i j
hjk : c.Rel j k
⊢ C.d i j ≫ C.d j k = 0

Tactic:
exact C.d_comp_d' i j k hij hjk

Result:
no goals

Proof state:
case neg
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
C : HomologicalComplex V c
i j k : ι
hij : ¬c.Rel i j
⊢ C.d i j ≫ C.d j k = 0

Tactic:
rw [C.shape i j hij, zero_comp]

Result:
no goals

Proof state:
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
C : HomologicalComplex V c
i j k : ι
⊢ C.d i j ≫ C.d j k = 0

Tactic:
by_cases hij : c.Rel i j

Result:
case pos
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
C : HomologicalComplex V c
i j k : ι
hij : c.Rel i j
⊢ C.d i j ≫ C.d j k = 0

case neg
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
C : HomologicalComplex V c
i j k : ι
hij : ¬c.Rel i j
⊢ C.d i j ≫ C.d j k = 0

Proof state:
case pos
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
C : HomologicalComplex V c
i j k : ι
hij : c.Rel i j
⊢ C.d i j ≫ C.d j k = 0

Tactic:
by_cases hjk : c.Rel j k

Result:
case pos
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
C : HomologicalComplex V c
i j k : ι
hij : c.Rel i j
hjk : c.Rel j k
⊢ C.d i j ≫ C.d j k = 0

case neg
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
C : HomologicalComplex V c
i j k : ι
hij : c.Rel i j
hjk : ¬c.Rel j k
⊢ C.d i j ≫ C.d j k = 0

Proof state:
case neg
ι : Type u_1
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
c : ComplexShape ι
C : HomologicalComplex V c
i j k : ι
hij : c.Rel i j
hjk : ¬c.Rel j k
⊢ C.d i j ≫ C.d j k = 0

Tactic:
rw [C.shape j k hjk, comp_zero]

Result:
no goals
-- Mathlib/Order/Partition/Equipartition.lean
theorem bot_isEquipartition : (⊥ : Finpartition s).IsEquipartition :=
  Set.equitableOn_iff_exists_eq_eq_add_one.2 ⟨1, by simp⟩

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
⊢ ∀ a ∈ ↑⊥.parts, #a = 1 ∨ #a = 1 + 1

Tactic:
simp

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Clique.lean
@[simp] lemma isNClique_empty : G.IsNClique n ∅ ↔ n = 0

Proof state:
α : Type u_1
G : SimpleGraph α
n : ℕ
⊢ G.IsNClique n ∅ ↔ n = 0

Tactic:
simp [isNClique_iff, eq_comm]

Result:
no goals
-- Mathlib/GroupTheory/Perm/Support.lean
theorem disjoint_inv_left_iff : Disjoint f⁻¹ g ↔ Disjoint f g

Proof state:
α : Type u_1
f g : Perm α
h : f⁻¹.Disjoint g
⊢ f.Disjoint g

Tactic:
convert h.inv_left

Result:
no goals

Proof state:
α : Type u_1
f g : Perm α
⊢ f⁻¹.Disjoint g ↔ f.Disjoint g

Tactic:
refine ⟨fun h => ?_, Disjoint.inv_left⟩

Result:
α : Type u_1
f g : Perm α
h : f⁻¹.Disjoint g
⊢ f.Disjoint g
-- Mathlib/Data/Set/Pairwise/Basic.lean
lemma exists_lt_mem_inter_of_not_pairwise_disjoint [LinearOrder ι]
    {f : ι → Set α} (h : ¬ Pairwise (Disjoint on f)) :
    ∃ i j : ι, i < j ∧ ∃ x, x ∈ f i ∩ f j

Proof state:
case intro.intro.intro.intro
α : Type u_1
ι : Type u_4
inst✝ : LinearOrder ι
f : ι → Set α
h✝ : ¬univ.Pairwise (Disjoint on f)
i : ι
_hi : i ∈ univ
j : ι
_hj : j ∈ univ
h : i < j ∧ ∃ x, x ∈ f i ∩ f j
⊢ ∃ i j, i < j ∧ ∃ x, x ∈ f i ∩ f j

Tactic:
exact ⟨i, j, h⟩

Result:
no goals

Proof state:
α : Type u_1
ι : Type u_4
inst✝ : LinearOrder ι
f : ι → Set α
h : ¬Pairwise (Disjoint on f)
⊢ ∃ i j, i < j ∧ ∃ x, x ∈ f i ∩ f j

Tactic:
rw [← pairwise_univ] at h

Result:
α : Type u_1
ι : Type u_4
inst✝ : LinearOrder ι
f : ι → Set α
h : ¬univ.Pairwise (Disjoint on f)
⊢ ∃ i j, i < j ∧ ∃ x, x ∈ f i ∩ f j

Proof state:
α : Type u_1
ι : Type u_4
inst✝ : LinearOrder ι
f : ι → Set α
h : ¬univ.Pairwise (Disjoint on f)
⊢ ∃ i j, i < j ∧ ∃ x, x ∈ f i ∩ f j

Tactic:
obtain ⟨i, _hi, j, _hj, h⟩ := exists_lt_mem_inter_of_not_pairwiseDisjoint h

Result:
case intro.intro.intro.intro
α : Type u_1
ι : Type u_4
inst✝ : LinearOrder ι
f : ι → Set α
h✝ : ¬univ.Pairwise (Disjoint on f)
i : ι
_hi : i ∈ univ
j : ι
_hj : j ∈ univ
h : i < j ∧ ∃ x, x ∈ f i ∩ f j
⊢ ∃ i j, i < j ∧ ∃ x, x ∈ f i ∩ f j
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/MinMax.lean
theorem max?_eq_none_iff {xs : List α} [Max α] : xs.max? = none ↔ xs = []

Proof state:
α : Type u_1
xs : List α
inst✝ : Max α
⊢ xs.max? = none ↔ xs = []

Tactic:
cases xs <;> simp [max?]

Result:
no goals
-- Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean
theorem _root_.Continuous.memLp_top_of_hasCompactSupport
    {X : Type*} [TopologicalSpace X] [MeasurableSpace X] [OpensMeasurableSpace X]
    {f : X → E} (hf : Continuous f) (h'f : HasCompactSupport f) (μ : Measure X) : MemLp f ⊤ μ

Proof state:
E : Type u_3
inst✝³ : NormedAddCommGroup E
X : Type u_6
inst✝² : TopologicalSpace X
inst✝¹ : MeasurableSpace X
inst✝ : OpensMeasurableSpace X
f : X → E
hf : Continuous f
h'f : HasCompactSupport f
μ : Measure X
⊢ MemLp f ⊤ μ

Tactic:
borelize E

Result:
E : Type u_3
inst✝³ : NormedAddCommGroup E
X : Type u_6
inst✝² : TopologicalSpace X
inst✝¹ : MeasurableSpace X
inst✝ : OpensMeasurableSpace X
f : X → E
hf : Continuous f
h'f : HasCompactSupport f
μ : Measure X
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
⊢ MemLp f ⊤ μ

Proof state:
E : Type u_3
inst✝³ : NormedAddCommGroup E
X : Type u_6
inst✝² : TopologicalSpace X
inst✝¹ : MeasurableSpace X
inst✝ : OpensMeasurableSpace X
f : X → E
hf : Continuous f
h'f : HasCompactSupport f
μ : Measure X
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
⊢ MemLp f ⊤ μ

Tactic:
rcases hf.bounded_above_of_compact_support h'f with ⟨C, hC⟩

Result:
case intro
E : Type u_3
inst✝³ : NormedAddCommGroup E
X : Type u_6
inst✝² : TopologicalSpace X
inst✝¹ : MeasurableSpace X
inst✝ : OpensMeasurableSpace X
f : X → E
hf : Continuous f
h'f : HasCompactSupport f
μ : Measure X
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
C : ℝ
hC : ∀ (x : X), ‖f x‖ ≤ C
⊢ MemLp f ⊤ μ

Proof state:
case intro
E : Type u_3
inst✝³ : NormedAddCommGroup E
X : Type u_6
inst✝² : TopologicalSpace X
inst✝¹ : MeasurableSpace X
inst✝ : OpensMeasurableSpace X
f : X → E
hf : Continuous f
h'f : HasCompactSupport f
μ : Measure X
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
C : ℝ
hC : ∀ (x : X), ‖f x‖ ≤ C
⊢ MemLp f ⊤ μ

Tactic:
apply memLp_top_of_bound ?_ C (Filter.Eventually.of_forall hC)

Result:
E : Type u_3
inst✝³ : NormedAddCommGroup E
X : Type u_6
inst✝² : TopologicalSpace X
inst✝¹ : MeasurableSpace X
inst✝ : OpensMeasurableSpace X
f : X → E
hf : Continuous f
h'f : HasCompactSupport f
μ : Measure X
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
C : ℝ
hC : ∀ (x : X), ‖f x‖ ≤ C
⊢ AEStronglyMeasurable f μ

Proof state:
E : Type u_3
inst✝³ : NormedAddCommGroup E
X : Type u_6
inst✝² : TopologicalSpace X
inst✝¹ : MeasurableSpace X
inst✝ : OpensMeasurableSpace X
f : X → E
hf : Continuous f
h'f : HasCompactSupport f
μ : Measure X
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
C : ℝ
hC : ∀ (x : X), ‖f x‖ ≤ C
⊢ AEStronglyMeasurable f μ

Tactic:
exact (hf.stronglyMeasurable_of_hasCompactSupport h'f).aestronglyMeasurable

Result:
no goals
-- Mathlib/GroupTheory/Coset/Basic.lean
theorem normal_of_eq_cosets (h : ∀ g : α, g • (s : Set α) = op g • s) : s.Normal :=
  ⟨fun a ha g =>
    show g * a * g⁻¹ ∈ (s : Set α) by rw [← mem_rightCoset_iff, ← h]; exact mem_leftCoset g ha⟩

Proof state:
α : Type u_1
inst✝ : Group α
s : Subgroup α
h : ∀ (g : α), g • ↑s = op g • ↑s
a : α
ha : a ∈ s
g : α
⊢ g * a ∈ g • ↑s

Tactic:
exact mem_leftCoset g ha

Result:
no goals

Proof state:
α : Type u_1
inst✝ : Group α
s : Subgroup α
h : ∀ (g : α), g • ↑s = op g • ↑s
a : α
ha : a ∈ s
g : α
⊢ g * a * g⁻¹ ∈ ↑s

Tactic:
rw [← mem_rightCoset_iff, ← h]

Result:
α : Type u_1
inst✝ : Group α
s : Subgroup α
h : ∀ (g : α), g • ↑s = op g • ↑s
a : α
ha : a ∈ s
g : α
⊢ g * a ∈ g • ↑s
-- Mathlib/CategoryTheory/Preadditive/LeftExact.lean
/-- A functor between preadditive categories preserves all coequalizers if it preserves all kernels.
-/
lemma preservesCoequalizers_of_preservesCokernels
    [∀ {X Y} (f : X ⟶ Y), PreservesColimit (parallelPair f 0) F] :
    PreservesColimitsOfShape WalkingParallelPair F where
  preservesColimit {K}

Proof state:
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : Preadditive C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : Preadditive D
F : C ⥤ D
inst✝² : F.PreservesZeroMorphisms
inst✝¹ : HasBinaryBiproducts C
inst✝ : ∀ {X Y : C} (f : X ⟶ Y), PreservesColimit (parallelPair f 0) F
K : WalkingParallelPair ⥤ C
⊢ PreservesColimit K F

Tactic:
letI := preservesCoequalizer_of_preservesCokernels F (K.map Limits.WalkingParallelPairHom.left)
    (K.map Limits.WalkingParallelPairHom.right)

Result:
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : Preadditive C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : Preadditive D
F : C ⥤ D
inst✝² : F.PreservesZeroMorphisms
inst✝¹ : HasBinaryBiproducts C
inst✝ : ∀ {X Y : C} (f : X ⟶ Y), PreservesColimit (parallelPair f 0) F
K : WalkingParallelPair ⥤ C
this : PreservesColimit (parallelPair (K.map WalkingParallelPairHom.left) (K.map WalkingParallelPairHom.right)) F :=
  preservesCoequalizer_of_preservesCokernels F (K.map WalkingParallelPairHom.left) (K.map WalkingParallelPairHom.right)
⊢ PreservesColimit K F

Proof state:
C : Type u₁
inst✝⁶ : Category.{v₁, u₁} C
inst✝⁵ : Preadditive C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : Preadditive D
F : C ⥤ D
inst✝² : F.PreservesZeroMorphisms
inst✝¹ : HasBinaryBiproducts C
inst✝ : ∀ {X Y : C} (f : X ⟶ Y), PreservesColimit (parallelPair f 0) F
K : WalkingParallelPair ⥤ C
this : PreservesColimit (parallelPair (K.map WalkingParallelPairHom.left) (K.map WalkingParallelPairHom.right)) F :=
  preservesCoequalizer_of_preservesCokernels F (K.map WalkingParallelPairHom.left) (K.map WalkingParallelPairHom.right)
⊢ PreservesColimit K F

Tactic:
apply preservesColimit_of_iso_diagram F (diagramIsoParallelPair K).symm

Result:
no goals
-- Mathlib/MeasureTheory/Function/LpSeminorm/CompareExp.lean
theorem eLpNorm_le_eLpNorm_top_mul_eLpNorm (p : ℝ≥0∞) (f : α → E) {g : α → F}
    (hg : AEStronglyMeasurable g μ) (b : E → F → G) (c : ℝ≥0)
    (h : ∀ᵐ x ∂μ, ‖b (f x) (g x)‖₊ ≤ c * ‖f x‖₊ * ‖g x‖₊) :
    eLpNorm (fun x => b (f x) (g x)) p μ ≤ c * eLpNorm f ∞ μ * eLpNorm g p μ

Proof state:
case bc.inr.inr.intro
α : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
m : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
μ : Measure α
p : ℝ≥0∞
f : α → E
g : α → F
hg : AEStronglyMeasurable g μ
b : E → F → G
c : ℝ≥0
h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ c * ‖f x‖₊ * ‖g x‖₊
hp : 0 < p.toReal
hp₁ : 0 < p
hp₂ : p < ⊤
⊢ ∫⁻ (x : α), (‖f x‖ₑ * ‖g x‖ₑ) ^ p.toReal ∂μ ≤ ∫⁻ (a : α), (essSup (fun x => ‖f x‖ₑ) μ * ‖g a‖ₑ) ^ p.toReal ∂μ

Tactic:
apply lintegral_mono_ae

Result:
case bc.inr.inr.intro.h
α : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
m : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
μ : Measure α
p : ℝ≥0∞
f : α → E
g : α → F
hg : AEStronglyMeasurable g μ
b : E → F → G
c : ℝ≥0
h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ c * ‖f x‖₊ * ‖g x‖₊
hp : 0 < p.toReal
hp₁ : 0 < p
hp₂ : p < ⊤
⊢ ∀ᵐ (a : α) ∂μ, (‖f a‖ₑ * ‖g a‖ₑ) ^ p.toReal ≤ (essSup (fun x => ‖f x‖ₑ) μ * ‖g a‖ₑ) ^ p.toReal

Proof state:
case h.bc
α : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
m : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
μ : Measure α
p : ℝ≥0∞
f : α → E
g : α → F
hg : AEStronglyMeasurable g μ
b : E → F → G
c : ℝ≥0
h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ c * ‖f x‖₊ * ‖g x‖₊
hp : 0 < p.toReal
hp₁ : 0 < p
hp₂ : p < ⊤
x : α
hb : ‖b (f x) (g x)‖₊ ≤ c * ‖f x‖₊ * ‖g x‖₊
hf : ‖f x‖ₑ ≤ eLpNormEssSup f μ
⊢ ‖f x‖ₑ ≤ essSup (fun x => ‖f x‖ₑ) μ

Tactic:
exact hf

Result:
no goals

Proof state:
case bc.inr.inl
α : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
m : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
μ : Measure α
f : α → E
g : α → F
hg : AEStronglyMeasurable g μ
b : E → F → G
c : ℝ≥0
h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ c * ‖f x‖₊ * ‖g x‖₊
⊢ eLpNorm (fun i => ‖f i‖ * ‖g i‖) ⊤ μ ≤ eLpNorm (fun x => ‖f x‖) ⊤ μ * eLpNorm (fun x => ‖g x‖) ⊤ μ

Tactic:
simp_rw [eLpNorm_exponent_top, eLpNormEssSup_eq_essSup_enorm, enorm_mul, enorm_norm]

Result:
case bc.inr.inl
α : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
m : MeasurableSpace α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
μ : Measure α
f : α → E
g : α → F
hg : AEStronglyMeasurable g μ
b : E → F → G
c : ℝ≥0
h : ∀ᵐ (x : α) ∂μ, ‖b (f x) (g x)‖₊ ≤ c * ‖f x‖₊ * ‖g x‖₊
⊢ essSup (fun x => ‖f x‖ₑ * ‖g x‖ₑ) μ ≤ essSup (fun x => ‖f x‖ₑ) μ * essSup (fun x => ‖g x‖ₑ) μ
-- Mathlib/Algebra/Group/PNatPowAssoc.lean
theorem ppow_mul_comm (m n : ℕ+) (x : M) :
    x ^ m * x ^ n = x ^ n * x ^ m

Proof state:
M : Type u_1
inst✝² : Mul M
inst✝¹ : Pow M ℕ+
inst✝ : PNatPowAssoc M
m n : ℕ+
x : M
⊢ x ^ m * x ^ n = x ^ n * x ^ m

Tactic:
simp only [← ppow_add, add_comm]

Result:
no goals
-- Mathlib/MeasureTheory/Function/ConvergenceInMeasure.lean
theorem TendstoInMeasure.aemeasurable {u : Filter ι} [NeBot u] [IsCountablyGenerated u]
    {f : ι → α → E} {g : α → E} (hf : ∀ n, AEMeasurable (f n) μ)
    (h_tendsto : TendstoInMeasure μ f u g) : AEMeasurable g μ

Proof state:
case intro.intro
α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst✝⁴ : MeasurableSpace E
inst✝³ : NormedAddCommGroup E
inst✝² : BorelSpace E
u : Filter ι
inst✝¹ : u.NeBot
inst✝ : u.IsCountablyGenerated
f : ι → α → E
g : α → E
hf : ∀ (n : ι), AEMeasurable (f n) μ
h_tendsto : TendstoInMeasure μ f u g
ns : ℕ → ι
hns : ∀ᵐ (x : α) ∂μ, Tendsto (fun i => f (ns i) x) atTop (𝓝 (g x))
⊢ AEMeasurable g μ

Tactic:
exact aemeasurable_of_tendsto_metrizable_ae atTop (fun n => hf (ns n)) hns

Result:
no goals

Proof state:
α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst✝⁴ : MeasurableSpace E
inst✝³ : NormedAddCommGroup E
inst✝² : BorelSpace E
u : Filter ι
inst✝¹ : u.NeBot
inst✝ : u.IsCountablyGenerated
f : ι → α → E
g : α → E
hf : ∀ (n : ι), AEMeasurable (f n) μ
h_tendsto : TendstoInMeasure μ f u g
⊢ AEMeasurable g μ

Tactic:
obtain ⟨ns, -, hns⟩ := h_tendsto.exists_seq_tendsto_ae'

Result:
case intro.intro
α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst✝⁴ : MeasurableSpace E
inst✝³ : NormedAddCommGroup E
inst✝² : BorelSpace E
u : Filter ι
inst✝¹ : u.NeBot
inst✝ : u.IsCountablyGenerated
f : ι → α → E
g : α → E
hf : ∀ (n : ι), AEMeasurable (f n) μ
h_tendsto : TendstoInMeasure μ f u g
ns : ℕ → ι
hns : ∀ᵐ (x : α) ∂μ, Tendsto (fun i => f (ns i) x) atTop (𝓝 (g x))
⊢ AEMeasurable g μ
-- Mathlib/Order/Filter/Germ/Basic.lean
theorem map_id : map id = (id : Germ l β → Germ l β)

Proof state:
case h.mk
α : Type u_1
β : Type u_2
l : Filter α
x✝ : l.Germ β
f : α → β
⊢ map id (Quot.mk (⇑(l.germSetoid β)) f) = id (Quot.mk (⇑(l.germSetoid β)) f)

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
l : Filter α
⊢ map id = id

Tactic:
ext ⟨f⟩

Result:
case h.mk
α : Type u_1
β : Type u_2
l : Filter α
x✝ : l.Germ β
f : α → β
⊢ map id (Quot.mk (⇑(l.germSetoid β)) f) = id (Quot.mk (⇑(l.germSetoid β)) f)
-- Mathlib/Order/Filter/CountablyGenerated.lean
theorem countable_biInf_eq_iInf_seq' [CompleteLattice α] {B : Set ι} (Bcbl : B.Countable)
    (f : ι → α) {i₀ : ι} (h : f i₀ = ⊤) : ∃ x : ℕ → ι, ⨅ t ∈ B, f t = ⨅ i, f (x i)

Proof state:
α : Type u_1
ι : Type u_4
inst✝ : CompleteLattice α
B : Set ι
Bcbl : B.Countable
f : ι → α
i₀ : ι
h : f i₀ = ⊤
⊢ ∃ x, ⨅ t ∈ B, f t = ⨅ i, f (x i)

Tactic:
rcases B.eq_empty_or_nonempty with hB | Bnonempty

Result:
case inl
α : Type u_1
ι : Type u_4
inst✝ : CompleteLattice α
B : Set ι
Bcbl : B.Countable
f : ι → α
i₀ : ι
h : f i₀ = ⊤
hB : B = ∅
⊢ ∃ x, ⨅ t ∈ B, f t = ⨅ i, f (x i)

case inr
α : Type u_1
ι : Type u_4
inst✝ : CompleteLattice α
B : Set ι
Bcbl : B.Countable
f : ι → α
i₀ : ι
h : f i₀ = ⊤
Bnonempty : B.Nonempty
⊢ ∃ x, ⨅ t ∈ B, f t = ⨅ i, f (x i)

Proof state:
case inr
α : Type u_1
ι : Type u_4
inst✝ : CompleteLattice α
B : Set ι
Bcbl : B.Countable
f : ι → α
i₀ : ι
h : f i₀ = ⊤
Bnonempty : B.Nonempty
⊢ ∃ x, ⨅ t ∈ B, f t = ⨅ i, f (x i)

Tactic:
exact countable_biInf_eq_iInf_seq Bcbl Bnonempty f

Result:
no goals

Proof state:
case inl
α : Type u_1
ι : Type u_4
inst✝ : CompleteLattice α
B : Set ι
Bcbl : B.Countable
f : ι → α
i₀ : ι
h : f i₀ = ⊤
hB : B = ∅
⊢ ∃ x, ⨅ t ∈ B, f t = ⨅ i, f (x i)

Tactic:
rw [hB, iInf_emptyset]

Result:
case inl
α : Type u_1
ι : Type u_4
inst✝ : CompleteLattice α
B : Set ι
Bcbl : B.Countable
f : ι → α
i₀ : ι
h : f i₀ = ⊤
hB : B = ∅
⊢ ∃ x, ⊤ = ⨅ i, f (x i)

Proof state:
case h
α : Type u_1
ι : Type u_4
inst✝ : CompleteLattice α
B : Set ι
Bcbl : B.Countable
f : ι → α
i₀ : ι
h : f i₀ = ⊤
hB : B = ∅
⊢ ⊤ = ⨅ i, f ((fun x => i₀) i)

Tactic:
simp [h]

Result:
no goals

Proof state:
case inl
α : Type u_1
ι : Type u_4
inst✝ : CompleteLattice α
B : Set ι
Bcbl : B.Countable
f : ι → α
i₀ : ι
h : f i₀ = ⊤
hB : B = ∅
⊢ ∃ x, ⊤ = ⨅ i, f (x i)

Tactic:
use fun _ => i₀

Result:
case h
α : Type u_1
ι : Type u_4
inst✝ : CompleteLattice α
B : Set ι
Bcbl : B.Countable
f : ι → α
i₀ : ι
h : f i₀ = ⊤
hB : B = ∅
⊢ ⊤ = ⨅ i, f ((fun x => i₀) i)
-- Mathlib/LinearAlgebra/LinearIndependent/Basic.lean
theorem linearIndependent_finset_map_embedding_subtype (s : Set M)
    (li : LinearIndependent R ((↑) : s → M)) (t : Finset s) :
    LinearIndependent R ((↑) : Finset.map (Embedding.subtype s) t → M) :=
  li.comp (fun _ ↦ ⟨_, _⟩) <| by intro; aesop

Proof state:
R : Type u_2
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
li : LinearIndependent R Subtype.val
t : Finset ↑s
⊢ Injective fun x => ⟨x.1, ⋯⟩

Tactic:
intro

Result:
R : Type u_2
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
li : LinearIndependent R Subtype.val
t : Finset ↑s
a₁✝ : { x // x ∈ Finset.map (Embedding.subtype s) t }
⊢ ∀ ⦃a₂ : { x // x ∈ Finset.map (Embedding.subtype s) t }⦄, (fun x => ⟨x.1, ⋯⟩) a₁✝ = (fun x => ⟨x.1, ⋯⟩) a₂ → a₁✝ = a₂

Proof state:
R : Type u_2
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : Set M
li : LinearIndependent R Subtype.val
t : Finset ↑s
a₁✝ : { x // x ∈ Finset.map (Embedding.subtype s) t }
⊢ ∀ ⦃a₂ : { x // x ∈ Finset.map (Embedding.subtype s) t }⦄, (fun x => ⟨x.1, ⋯⟩) a₁✝ = (fun x => ⟨x.1, ⋯⟩) a₂ → a₁✝ = a₂

Tactic:
aesop

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Basic.lean
theorem sin_eq_zero_iff_cos_eq {x : ℝ} : sin x = 0 ↔ cos x = 1 ∨ cos x = -1

Proof state:
x : ℝ
⊢ sin x = 0 ↔ cos x = 1 ∨ cos x = -1

Tactic:
rw [← mul_self_eq_one_iff, ← sin_sq_add_cos_sq x, sq, sq, ← sub_eq_iff_eq_add, sub_self]

Result:
x : ℝ
⊢ sin x = 0 ↔ 0 = sin x * sin x

Proof state:
x : ℝ
⊢ sin x = 0 ↔ 0 = sin x * sin x

Tactic:
exact ⟨fun h => by rw [h, mul_zero], eq_zero_of_mul_self_eq_zero ∘ Eq.symm⟩

Result:
no goals

Proof state:
x : ℝ
h : sin x = 0
⊢ 0 = sin x * sin x

Tactic:
rw [h, mul_zero]

Result:
no goals
-- Mathlib/Algebra/GroupWithZero/Indicator.lean
lemma inter_indicator_mul (f g : ι → M₀) (i : ι) :
    (s ∩ t).indicator (fun j ↦ f j * g j) i = s.indicator f i * t.indicator g i

Proof state:
ι : Type u_1
M₀ : Type u_4
inst✝ : MulZeroClass M₀
s t : Set ι
f g : ι → M₀
i : ι
⊢ (s ∩ t).indicator (fun j => f j * g j) i = s.indicator f i * t.indicator g i

Tactic:
rw [← Set.indicator_indicator]

Result:
ι : Type u_1
M₀ : Type u_4
inst✝ : MulZeroClass M₀
s t : Set ι
f g : ι → M₀
i : ι
⊢ s.indicator (t.indicator fun j => f j * g j) i = s.indicator f i * t.indicator g i

Proof state:
ι : Type u_1
M₀ : Type u_4
inst✝ : MulZeroClass M₀
s t : Set ι
f g : ι → M₀
i : ι
⊢ (if i ∈ s then if i ∈ t then f i * g i else 0 else 0) = (if i ∈ s then f i else 0) * if i ∈ t then g i else 0

Tactic:
split_ifs <;> simp

Result:
no goals

Proof state:
ι : Type u_1
M₀ : Type u_4
inst✝ : MulZeroClass M₀
s t : Set ι
f g : ι → M₀
i : ι
⊢ s.indicator (t.indicator fun j => f j * g j) i = s.indicator f i * t.indicator g i

Tactic:
simp_rw [indicator]

Result:
ι : Type u_1
M₀ : Type u_4
inst✝ : MulZeroClass M₀
s t : Set ι
f g : ι → M₀
i : ι
⊢ (if i ∈ s then if i ∈ t then f i * g i else 0 else 0) = (if i ∈ s then f i else 0) * if i ∈ t then g i else 0
-- Mathlib/CategoryTheory/Monoidal/Grp_.lean
theorem lift_comp_inv_right {A : C} {B : Grp_ C} (f : A ⟶ B.X) :
    lift f (f ≫ B.inv) ≫ B.mul = toUnit _ ≫ B.one

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : ChosenFiniteProducts C
A : C
B : Grp_ C
f : A ⟶ B.X
this : f ≫ lift (𝟙 B.X) B.inv ≫ B.mul = f ≫ toUnit B.X ≫ B.one
⊢ lift f (f ≫ B.inv) ≫ B.mul = toUnit A ≫ B.one

Tactic:
rwa [comp_lift_assoc, comp_id, reassoc_of% toUnit_unique (f ≫ toUnit B.X) (toUnit A)] at this

Result:
no goals

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : ChosenFiniteProducts C
A : C
B : Grp_ C
f : A ⟶ B.X
⊢ lift f (f ≫ B.inv) ≫ B.mul = toUnit A ≫ B.one

Tactic:
have := f ≫= B.right_inv

Result:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : ChosenFiniteProducts C
A : C
B : Grp_ C
f : A ⟶ B.X
this : f ≫ lift (𝟙 B.X) B.inv ≫ B.mul = f ≫ toUnit B.X ≫ B.one
⊢ lift f (f ≫ B.inv) ≫ B.mul = toUnit A ≫ B.one