harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/MeasureTheory/Measure/MeasureSpace.lean
theorem union_ae_eq_left_iff_ae_subset : (s ∪ t : Set α) =ᵐ[μ] s ↔ t ≤ᵐ[μ] s

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s t : Set α
h : μ (t \ s) = 0
⊢ s ∪ t ≤ᶠ[ae μ] s

Tactic:
rwa [ae_le_set, union_diff_left]

Result:
no goals

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s t : Set α
⊢ s ∪ t =ᶠ[ae μ] s ↔ μ (t \ s) = 0

Tactic:
refine
  ⟨fun h => by simpa only [union_diff_left] using (ae_eq_set.mp h).1, fun h =>
    eventuallyLE_antisymm_iff.mpr
      ⟨by rwa [ae_le_set, union_diff_left],
        HasSubset.Subset.eventuallyLE subset_union_left⟩⟩

Result:
no goals

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s t : Set α
h : s ∪ t =ᶠ[ae μ] s
⊢ μ (t \ s) = 0

Tactic:
simpa only [union_diff_left] using (ae_eq_set.mp h).1

Result:
no goals

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s t : Set α
⊢ s ∪ t =ᶠ[ae μ] s ↔ t ≤ᶠ[ae μ] s

Tactic:
rw [ae_le_set]

Result:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s t : Set α
⊢ s ∪ t =ᶠ[ae μ] s ↔ μ (t \ s) = 0
-- Mathlib/Data/ENNReal/Basic.lean
theorem coe_nnreal_eq (r : ℝ≥0) : (r : ℝ≥0∞) = ENNReal.ofReal r

Proof state:
r : ℝ≥0
⊢ ↑r = ENNReal.ofReal ↑r

Tactic:
rw [ENNReal.ofReal, Real.toNNReal_coe]

Result:
no goals
-- Mathlib/Analysis/LocallyConvex/AbsConvex.lean
theorem mem_absConvexHull_iff : x ∈ absConvexHull 𝕜 s ↔ ∀ t, s ⊆ t → AbsConvex 𝕜 t → x ∈ t

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝³ : SeminormedRing 𝕜
inst✝² : SMul 𝕜 E
inst✝¹ : SMul ℝ E
inst✝ : AddCommMonoid E
s : Set E
x : E
⊢ x ∈ (absConvexHull 𝕜) s ↔ ∀ (t : Set E), s ⊆ t → AbsConvex 𝕜 t → x ∈ t

Tactic:
simp_rw [absConvexHull_eq_iInter, mem_iInter]

Result:
no goals
-- Mathlib/Algebra/Ring/Parity.lean
@[simp] lemma not_even_iff_odd : ¬Even n ↔ Odd n

Proof state:
n : ℕ
⊢ ¬Even n ↔ Odd n

Tactic:
rw [not_even_iff, odd_iff]

Result:
no goals
-- Mathlib/Topology/LocalAtTarget.lean
theorem isOpen_iff_coe_preimage :
    IsOpen s ↔ ∀ i, IsOpen ((↑) ⁻¹' s : Set (U i))

Proof state:
β : Type u_2
inst✝ : TopologicalSpace β
ι : Type u_3
U : ι → Opens β
s : Set β
hU : IsOpenCover U
⊢ IsOpen s ↔ ∀ (i : ι), IsOpen (Subtype.val ⁻¹' s)

Tactic:
simp [hU.isOpen_iff_inter (s := s), (U _).2.isOpenEmbedding_subtypeVal.isOpen_iff_image_isOpen,
  image_preimage_eq_inter_range]

Result:
no goals
-- Mathlib/AlgebraicGeometry/PullbackCarrier.lean
lemma residueFieldCongr_inv_residueFieldMap_ofPoint (t : ↑(pullback f g)) :
    ((S.residueFieldCongr (Triplet.ofPoint t).hx).inv ≫ f.residueFieldMap (Triplet.ofPoint t).x) ≫
      (pullback.fst f g).residueFieldMap t = ((S.residueFieldCongr (Triplet.ofPoint t).hy).inv ≫
          g.residueFieldMap (Triplet.ofPoint t).y) ≫ (pullback.snd f g).residueFieldMap t

Proof state:
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
t : ↑↑(pullback f g).toPresheafedSpace
⊢ ((residueFieldCongr ⋯).inv ≫ Hom.residueFieldMap f (Triplet.ofPoint t).x) ≫ Hom.residueFieldMap (pullback.fst f g) t =
    ((residueFieldCongr ⋯).inv ≫ Hom.residueFieldMap g (Triplet.ofPoint t).y) ≫ Hom.residueFieldMap (pullback.snd f g) t

Tactic:
simp [← residueFieldMap_comp, Scheme.Hom.residueFieldMap_congr pullback.condition]

Result:
no goals
-- Mathlib/GroupTheory/GroupAction/Hom.lean
theorem id_apply (x : A) : DistribMulActionHom.id M x = x

Proof state:
M : Type u_1
inst✝² : Monoid M
A : Type u_4
inst✝¹ : AddMonoid A
inst✝ : DistribMulAction M A
x : A
⊢ (DistribMulActionHom.id M) x = x

Tactic:
rfl

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Find.lean
theorem find?_some {xs : Array α} (h : find? p xs = some a) : p a

Proof state:
α : Type u_1
p : α → Bool
a : α
xs : Array α
h : find? p xs = some a
⊢ p a = true

Tactic:
cases xs

Result:
case mk
α : Type u_1
p : α → Bool
a : α
toList✝ : List α
h : find? p { toList := toList✝ } = some a
⊢ p a = true

Proof state:
case mk
α : Type u_1
p : α → Bool
a : α
toList✝ : List α
h : List.find? p toList✝ = some a
⊢ p a = true

Tactic:
exact List.find?_some h

Result:
no goals

Proof state:
case mk
α : Type u_1
p : α → Bool
a : α
toList✝ : List α
h : find? p { toList := toList✝ } = some a
⊢ p a = true

Tactic:
simp at h

Result:
case mk
α : Type u_1
p : α → Bool
a : α
toList✝ : List α
h : List.find? p toList✝ = some a
⊢ p a = true
-- Mathlib/LinearAlgebra/Matrix/SesquilinearForm.lean
theorem LinearMap.mul_toMatrix' (B : (n → R) →ₗ[R] (m → R) →ₗ[R] R) (M : Matrix n' n R) :
    M * toMatrix₂' R B = toMatrix₂' R (B.comp <| toLin' Mᵀ)

Proof state:
n : Type u_11
m : Type u_12
n' : Type u_13
R : Type u_16
inst✝⁶ : CommSemiring R
inst✝⁵ : Fintype n
inst✝⁴ : Fintype m
inst✝³ : DecidableEq n
inst✝² : DecidableEq m
inst✝¹ : Fintype n'
inst✝ : DecidableEq n'
B : (n → R) →ₗ[R] (m → R) →ₗ[R] R
M : Matrix n' n R
⊢ M * (toMatrix₂' R) B = (toMatrix₂' R) (B ∘ₗ toLin' Mᵀ)

Tactic:
simp only [B.toMatrix₂'_comp, transpose_transpose, toMatrix'_toLin']

Result:
no goals
-- Mathlib/Data/Set/Pairwise/Basic.lean
theorem pairwise_subtype_iff_pairwise_set (s : Set α) (r : α → α → Prop) :
    (Pairwise fun (x : s) (y : s) => r x y) ↔ s.Pairwise r

Proof state:
α : Type u_1
s : Set α
r : α → α → Prop
⊢ (Pairwise fun x y => r ↑x ↑y) ↔ s.Pairwise r

Tactic:
simp only [Pairwise, Set.Pairwise, SetCoe.forall, Ne, Subtype.ext_iff, Subtype.coe_mk]

Result:
no goals
-- Mathlib/Analysis/Calculus/MeanValue.lean
theorem norm_image_sub_le_of_norm_hasDerivWithin_le {C : ℝ}
    (hf : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x) (bound : ∀ x ∈ s, ‖f' x‖ ≤ C) (hs : Convex ℝ s)
    (xs : x ∈ s) (ys : y ∈ s) : ‖f y - f x‖ ≤ C * ‖y - x‖ :=
  Convex.norm_image_sub_le_of_norm_hasFDerivWithin_le (fun x hx => (hf x hx).hasFDerivWithinAt)
    (fun x hx => le_trans (by simp) (bound x hx)) hs xs ys

Proof state:
𝕜 : Type u_3
G : Type u_4
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f f' : 𝕜 → G
s : Set 𝕜
x✝ y : 𝕜
C : ℝ
hf : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x
bound : ∀ x ∈ s, ‖f' x‖ ≤ C
hs : Convex ℝ s
xs : x✝ ∈ s
ys : y ∈ s
x : 𝕜
hx : x ∈ s
⊢ ‖smulRight 1 (f' x)‖ ≤ ‖f' x‖

Tactic:
simp

Result:
no goals
-- Mathlib/MeasureTheory/Function/L1Space/Integrable.lean
theorem memLp_one_iff_integrable {f : α → β} : MemLp f 1 μ ↔ Integrable f μ

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup β
f : α → β
⊢ MemLp f 1 μ ↔ Integrable f μ

Tactic:
simp_rw [Integrable, hasFiniteIntegral_iff_enorm, MemLp, eLpNorm_one_eq_lintegral_enorm]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem getElem?_len_le (a : Array α) {i : Nat} (h : a.size ≤ i) : a[i]? = none

Proof state:
α : Type u_1
a : Array α
i : Nat
h : a.size ≤ i
⊢ a[i]? = none

Tactic:
simp [getElem?_eq_none, h]

Result:
no goals
-- Mathlib/Algebra/BigOperators/Group/Multiset/Basic.lean
theorem prod_map_prod_map (m : Multiset β') (n : Multiset γ) {f : β' → γ → α} :
    prod (m.map fun a => prod <| n.map fun b => f a b) =
      prod (n.map fun b => prod <| m.map fun a => f a b) :=
  Multiset.induction_on m (by simp) fun a m ih => by simp [ih]

Proof state:
α : Type u_3
β' : Type u_5
γ : Type u_6
inst✝ : CommMonoid α
m✝ : Multiset β'
n : Multiset γ
f : β' → γ → α
a : β'
m : Multiset β'
ih : (map (fun a => (map (fun b => f a b) n).prod) m).prod = (map (fun b => (map (fun a => f a b) m).prod) n).prod
⊢ (map (fun a => (map (fun b => f a b) n).prod) (a ::ₘ m)).prod =
    (map (fun b => (map (fun a => f a b) (a ::ₘ m)).prod) n).prod

Tactic:
simp [ih]

Result:
no goals

Proof state:
α : Type u_3
β' : Type u_5
γ : Type u_6
inst✝ : CommMonoid α
m : Multiset β'
n : Multiset γ
f : β' → γ → α
⊢ (map (fun a => (map (fun b => f a b) n).prod) 0).prod = (map (fun b => (map (fun a => f a b) 0).prod) n).prod

Tactic:
simp

Result:
no goals
-- Mathlib/SetTheory/Game/PGame.lean
theorem lf_def {x y : PGame} :
    x ⧏ y ↔
      (∃ i, (∀ i', x.moveLeft i' ⧏ y.moveLeft i) ∧ ∀ j, x ⧏ (y.moveLeft i).moveRight j) ∨
        ∃ j, (∀ i, (x.moveRight j).moveLeft i ⧏ y) ∧ ∀ j', x.moveRight j ⧏ y.moveRight j'

Proof state:
x y : PGame
⊢ ((∃ i, x ≤ y.moveLeft i) ∨ ∃ j, x.moveRight j ≤ y) ↔
    (∃ i,
        (∀ (i' : x.LeftMoves), x.moveLeft i' ⧏ y.moveLeft i) ∧
          ∀ (j : (y.moveLeft i).RightMoves), x ⧏ (y.moveLeft i).moveRight j) ∨
      ∃ j,
        (∀ (i : (x.moveRight j).LeftMoves), (x.moveRight j).moveLeft i ⧏ y) ∧
          ∀ (j' : y.RightMoves), x.moveRight j ⧏ y.moveRight j'

Tactic:
conv =>
  lhs
  simp only [le_iff_forall_lf]

Result:
no goals

Proof state:
x y : PGame
⊢ x ⧏ y ↔
    (∃ i,
        (∀ (i' : x.LeftMoves), x.moveLeft i' ⧏ y.moveLeft i) ∧
          ∀ (j : (y.moveLeft i).RightMoves), x ⧏ (y.moveLeft i).moveRight j) ∨
      ∃ j,
        (∀ (i : (x.moveRight j).LeftMoves), (x.moveRight j).moveLeft i ⧏ y) ∧
          ∀ (j' : y.RightMoves), x.moveRight j ⧏ y.moveRight j'

Tactic:
rw [lf_iff_exists_le]

Result:
x y : PGame
⊢ ((∃ i, x ≤ y.moveLeft i) ∨ ∃ j, x.moveRight j ≤ y) ↔
    (∃ i,
        (∀ (i' : x.LeftMoves), x.moveLeft i' ⧏ y.moveLeft i) ∧
          ∀ (j : (y.moveLeft i).RightMoves), x ⧏ (y.moveLeft i).moveRight j) ∨
      ∃ j,
        (∀ (i : (x.moveRight j).LeftMoves), (x.moveRight j).moveLeft i ⧏ y) ∧
          ∀ (j' : y.RightMoves), x.moveRight j ⧏ y.moveRight j'
-- Mathlib/GroupTheory/Perm/Cycle/Type.lean
theorem one_eq : vectorsProdEqOne G 1 = {Vector.nil.cons 1}

Proof state:
G : Type u_2
inst✝ : Group G
⊢ ∀ (x : List.Vector G 1), x.head = 1 → x = 1 ::ᵥ Vector.nil

Tactic:
exact fun v hv => v.cons_head_tail.symm.trans (congr_arg₂ Vector.cons hv v.tail.eq_nil)

Result:
no goals

Proof state:
G : Type u_2
inst✝ : Group G
⊢ vectorsProdEqOne G 1 = {1 ::ᵥ Vector.nil}

Tactic:
simp_rw [Set.eq_singleton_iff_unique_mem, mem_iff, List.Vector.toList_singleton,
  List.prod_singleton, List.Vector.head_cons, true_and]

Result:
G : Type u_2
inst✝ : Group G
⊢ ∀ (x : List.Vector G 1), x.head = 1 → x = 1 ::ᵥ Vector.nil
-- Mathlib/RingTheory/PowerSeries/WellKnown.lean
theorem map_cos : map f (cos A) = cos A'

Proof state:
case h
A : Type u_1
A' : Type u_2
inst✝³ : Ring A
inst✝² : Ring A'
inst✝¹ : Algebra ℚ A
inst✝ : Algebra ℚ A'
f : A →+* A'
n✝ : ℕ
⊢ (coeff A' n✝) ((map f) (cos A)) = (coeff A' n✝) (cos A')

Tactic:
simp [cos, apply_ite f]

Result:
no goals

Proof state:
A : Type u_1
A' : Type u_2
inst✝³ : Ring A
inst✝² : Ring A'
inst✝¹ : Algebra ℚ A
inst✝ : Algebra ℚ A'
f : A →+* A'
⊢ (map f) (cos A) = cos A'

Tactic:
ext

Result:
case h
A : Type u_1
A' : Type u_2
inst✝³ : Ring A
inst✝² : Ring A'
inst✝¹ : Algebra ℚ A
inst✝ : Algebra ℚ A'
f : A →+* A'
n✝ : ℕ
⊢ (coeff A' n✝) ((map f) (cos A)) = (coeff A' n✝) (cos A')
-- Mathlib/RingTheory/Spectrum/Prime/Topology.lean
lemma vanishingIdeal_range_comap :
    vanishingIdeal (Set.range (comap f)) = (RingHom.ker f).radical

Proof state:
case h
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
x : R
⊢ (∀ (a : PrimeSpectrum S), f x ∈ a.asIdeal) ↔ ∀ (p : Submodule S S), Ideal.IsPrime p → f x ∈ p

Tactic:
exact ⟨fun H I hI ↦ H ⟨I, hI⟩, fun H I ↦ H I.1 I.2⟩

Result:
no goals

Proof state:
case h
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
x : R
⊢ x ∈ vanishingIdeal (Set.range ⇑(comap f)) ↔ x ∈ Ideal.comap f (sInf {J | ⊥ ≤ J ∧ J.IsPrime})

Tactic:
simp only [mem_vanishingIdeal, Set.mem_range, forall_exists_index, forall_apply_eq_imp_iff,
  comap_asIdeal, Ideal.mem_comap, bot_le, true_and, Submodule.mem_sInf, Set.mem_setOf_eq]

Result:
case h
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
x : R
⊢ (∀ (a : PrimeSpectrum S), f x ∈ a.asIdeal) ↔ ∀ (p : Submodule S S), Ideal.IsPrime p → f x ∈ p

Proof state:
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
⊢ vanishingIdeal (Set.range ⇑(comap f)) = (RingHom.ker f).radical

Tactic:
ext x

Result:
case h
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
x : R
⊢ x ∈ vanishingIdeal (Set.range ⇑(comap f)) ↔ x ∈ (RingHom.ker f).radical

Proof state:
case h
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
x : R
⊢ x ∈ vanishingIdeal (Set.range ⇑(comap f)) ↔ x ∈ (RingHom.ker f).radical

Tactic:
rw [RingHom.ker_eq_comap_bot, ← Ideal.comap_radical, Ideal.radical_eq_sInf]

Result:
case h
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
x : R
⊢ x ∈ vanishingIdeal (Set.range ⇑(comap f)) ↔ x ∈ Ideal.comap f (sInf {J | ⊥ ≤ J ∧ J.IsPrime})
-- Mathlib/GroupTheory/Coxeter/Basic.lean
theorem toMonoidHom_apply_symm_apply (a : PresentedGroup (M.relationsSet)) :
    (MulEquiv.toMonoidHom cs.mulEquiv : W →* PresentedGroup (M.relationsSet))
    ((MulEquiv.symm cs.mulEquiv) a) = a := calc
  _ = cs.mulEquiv ((MulEquiv.symm cs.mulEquiv) a)

Proof state:
B : Type u_1
W : Type u_3
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
a : PresentedGroup M.relationsSet
⊢ cs.mulEquiv (cs.mulEquiv.symm a) = a

Tactic:
rw [MulEquiv.apply_symm_apply]

Result:
no goals

Proof state:
B : Type u_1
W : Type u_3
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
a : PresentedGroup M.relationsSet
⊢ cs.mulEquiv.toMonoidHom (cs.mulEquiv.symm a) = cs.mulEquiv (cs.mulEquiv.symm a)

Tactic:
rfl

Result:
no goals
-- Mathlib/FieldTheory/SeparableDegree.lean
theorem natSepDegree_eq_zero (h : f.natDegree = 0) : f.natSepDegree = 0

Proof state:
F : Type u
inst✝ : Field F
f : F[X]
h : f.natDegree = 0
⊢ f.natSepDegree = 0

Tactic:
linarith only [natSepDegree_le_natDegree f, h]

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/Spectrum.lean
theorem inner_product_apply_eigenvector {μ : 𝕜} {v : E} {T : E →ₗ[𝕜] E}
    (h : v ∈ Module.End.eigenspace T μ) : ⟪v, T v⟫ = μ * (‖v‖ : 𝕜) ^ 2

Proof state:
𝕜 : Type u_1
inst✝² : RCLike 𝕜
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
μ : 𝕜
v : E
T : E →ₗ[𝕜] E
h : v ∈ eigenspace T μ
⊢ inner v (T v) = μ * ↑‖v‖ ^ 2

Tactic:
simp only [mem_eigenspace_iff.mp h, inner_smul_right, inner_self_eq_norm_sq_to_K]

Result:
no goals
-- Mathlib/LinearAlgebra/AffineSpace/FiniteDimensional.lean
theorem Coplanar.finiteDimensional_vectorSpan {s : Set P} (h : Coplanar k s) :
    FiniteDimensional k (vectorSpan k s)

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
h : Coplanar k s
⊢ FiniteDimensional k ↥(vectorSpan k s)

Tactic:
refine IsNoetherian.iff_fg.1 (IsNoetherian.iff_rank_lt_aleph0.2 (lt_of_le_of_lt h ?_))

Result:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
h : Coplanar k s
⊢ 2 < Cardinal.aleph0

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : DivisionRing k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : Set P
h : Coplanar k s
⊢ 2 < Cardinal.aleph0

Tactic:
exact Cardinal.lt_aleph0.2 ⟨2, rfl⟩

Result:
no goals
-- Mathlib/Probability/Moments/IntegrableExpMul.lean
/-- If `ω ↦ exp (t * X ω)` is integrable at `t` and `-t`, then `ω ↦ exp (t * |X ω|)` is
integrable. -/
lemma integrable_exp_mul_abs (ht_int_pos : Integrable (fun ω ↦ exp (t * X ω)) μ)
    (ht_int_neg : Integrable (fun ω ↦ exp (- t * X ω)) μ) :
    Integrable (fun ω ↦ exp (t * |X ω|)) μ

Proof state:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
ht_int_pos : Integrable (fun ω => rexp (t * X ω)) μ
ht_int_neg : Integrable (fun ω => rexp (-t * X ω)) μ
⊢ Integrable (fun ω => rexp (t * |X ω|)) μ

Tactic:
have h := integrable_exp_mul_abs_add (t := t) (μ := μ) (X := X) (v := 0) ?_ ?_

Result:
case refine_3
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
ht_int_pos : Integrable (fun ω => rexp (t * X ω)) μ
ht_int_neg : Integrable (fun ω => rexp (-t * X ω)) μ
h : Integrable (fun ω => rexp (t * |X ω| + 0 * X ω)) μ
⊢ Integrable (fun ω => rexp (t * |X ω|)) μ

case refine_1
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
ht_int_pos : Integrable (fun ω => rexp (t * X ω)) μ
ht_int_neg : Integrable (fun ω => rexp (-t * X ω)) μ
⊢ Integrable (fun ω => rexp ((0 + t) * X ω)) μ

case refine_2
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
ht_int_pos : Integrable (fun ω => rexp (t * X ω)) μ
ht_int_neg : Integrable (fun ω => rexp (-t * X ω)) μ
⊢ Integrable (fun ω => rexp ((0 - t) * X ω)) μ

Proof state:
case refine_3
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
ht_int_pos : Integrable (fun ω => rexp (t * X ω)) μ
ht_int_neg : Integrable (fun ω => rexp (-t * X ω)) μ
h : Integrable (fun ω => rexp (t * |X ω| + 0 * X ω)) μ
⊢ Integrable (fun ω => rexp (t * |X ω|)) μ

Tactic:
simpa using h

Result:
no goals

Proof state:
case refine_1
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
ht_int_pos : Integrable (fun ω => rexp (t * X ω)) μ
ht_int_neg : Integrable (fun ω => rexp (-t * X ω)) μ
⊢ Integrable (fun ω => rexp ((0 + t) * X ω)) μ

Tactic:
simpa using ht_int_pos

Result:
no goals

Proof state:
case refine_2
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
t : ℝ
ht_int_pos : Integrable (fun ω => rexp (t * X ω)) μ
ht_int_neg : Integrable (fun ω => rexp (-t * X ω)) μ
⊢ Integrable (fun ω => rexp ((0 - t) * X ω)) μ

Tactic:
simpa using ht_int_neg

Result:
no goals
-- Mathlib/Topology/LocallyClosed.lean
lemma coborder_eq_union_frontier_compl :
    coborder s = s ∪ (frontier s)ᶜ

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
⊢ coborder s = s ∪ (frontier s)ᶜ

Tactic:
rw [coborder, compl_eq_comm, compl_union, compl_compl, ← diff_eq_compl_inter,
  ← union_diff_right, union_comm, ← closure_eq_self_union_frontier]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Degree/SmallDegree.lean
theorem eq_X_add_C_of_degree_eq_one (h : degree p = 1) :
    p = C p.leadingCoeff * X + C (p.coeff 0) :=
  (eq_X_add_C_of_degree_le_one h.le).trans
    (by rw [← Nat.cast_one] at h; rw [leadingCoeff, natDegree_eq_of_degree_eq_some h])

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
h : p.degree = 1
⊢ C (p.coeff 1) * X + C (p.coeff 0) = C p.leadingCoeff * X + C (p.coeff 0)

Tactic:
rw [← Nat.cast_one] at h

Result:
R : Type u
inst✝ : Semiring R
p : R[X]
h : p.degree = ↑1
⊢ C (p.coeff 1) * X + C (p.coeff 0) = C p.leadingCoeff * X + C (p.coeff 0)

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
h : p.degree = ↑1
⊢ C (p.coeff 1) * X + C (p.coeff 0) = C p.leadingCoeff * X + C (p.coeff 0)

Tactic:
rw [leadingCoeff, natDegree_eq_of_degree_eq_some h]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Div/Basic.lean
theorem div_self (H : 0 < n) : n / n = 1

Proof state:
n : Nat
H : 0 < n
t : (0 + n) / n = 0 / n + 1 := add_div_right 0 H
⊢ n / n = 1

Tactic:
rwa [Nat.zero_add, Nat.zero_div] at t

Result:
no goals

Proof state:
n : Nat
H : 0 < n
⊢ n / n = 1

Tactic:
let t := add_div_right 0 H

Result:
n : Nat
H : 0 < n
t : (0 + n) / n = 0 / n + 1 := add_div_right 0 H
⊢ n / n = 1
-- Mathlib/MeasureTheory/Integral/BochnerL1.lean
theorem integral_eq (f : α →₁[μ] E) : integral f = integralCLM f

Proof state:
α : Type u_1
E : Type u_2
inst✝² : NormedAddCommGroup E
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedSpace ℝ E
inst✝ : CompleteSpace E
f : ↥(Lp E 1 μ)
⊢ integral f = integralCLM f

Tactic:
simp only [integral]

Result:
no goals
-- Mathlib/Analysis/NormedSpace/OperatorNorm/Basic.lean
theorem le_of_opNorm_le_of_le {x} {a b : ℝ} (hf : ‖f‖ ≤ a) (hx : ‖x‖ ≤ b) :
    ‖f x‖ ≤ a * b :=
  (f.le_opNorm x).trans <| by gcongr; exact (opNorm_nonneg f).trans hf

Proof state:
case b0
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst✝⁶ : SeminormedAddCommGroup E
inst✝⁵ : SeminormedAddCommGroup F
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NontriviallyNormedField 𝕜₂
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝ : RingHomIsometric σ₁₂
f : E →SL[σ₁₂] F
x : E
a b : ℝ
hf : ‖f‖ ≤ a
hx : ‖x‖ ≤ b
⊢ 0 ≤ a

Tactic:
exact (opNorm_nonneg f).trans hf

Result:
no goals

Proof state:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst✝⁶ : SeminormedAddCommGroup E
inst✝⁵ : SeminormedAddCommGroup F
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NontriviallyNormedField 𝕜₂
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝ : RingHomIsometric σ₁₂
f : E →SL[σ₁₂] F
x : E
a b : ℝ
hf : ‖f‖ ≤ a
hx : ‖x‖ ≤ b
⊢ ‖f‖ * ‖x‖ ≤ a * b

Tactic:
gcongr

Result:
case b0
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst✝⁶ : SeminormedAddCommGroup E
inst✝⁵ : SeminormedAddCommGroup F
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NontriviallyNormedField 𝕜₂
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝ : RingHomIsometric σ₁₂
f : E →SL[σ₁₂] F
x : E
a b : ℝ
hf : ‖f‖ ≤ a
hx : ‖x‖ ≤ b
⊢ 0 ≤ a
-- Mathlib/Order/Filter/Bases.lean
theorem ofSets_filter_eq_generate (s : Set (Set α)) :
    (FilterBasis.ofSets s).filter = generate s

Proof state:
α : Type u_1
s : Set (Set α)
⊢ (FilterBasis.ofSets s).filter = generate s

Tactic:
rw [← (FilterBasis.ofSets s).generate, FilterBasis.ofSets_sets, ← generate_eq_generate_inter]

Result:
no goals
-- Mathlib/Data/Nat/GCD/Basic.lean
theorem gcd_self_add_right (m n : ℕ) : gcd m (m + n) = gcd m n

Proof state:
m n : ℕ
⊢ m.gcd (m + n) = m.gcd n

Tactic:
rw [add_comm, gcd_add_self_right]

Result:
no goals
-- Mathlib/Order/Sublattice.lean
@[simp, norm_cast] lemma coe_eq_univ : L = (univ : Set α) ↔ L = ⊤

Proof state:
α : Type u_2
inst✝ : Lattice α
L : Sublattice α
⊢ ↑L = univ ↔ L = ⊤

Tactic:
rw [← coe_top, coe_inj]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem toArray_eq : List.toArray a = v ↔ a = v.toList

Proof state:
α✝ : Type u_1
a : List α✝
v : Array α✝
⊢ a.toArray = v ↔ a = v.toList

Tactic:
cases v

Result:
case mk
α✝ : Type u_1
a toList✝ : List α✝
⊢ a.toArray = { toList := toList✝ } ↔ a = { toList := toList✝ }.toList

Proof state:
case mk
α✝ : Type u_1
a toList✝ : List α✝
⊢ a.toArray = { toList := toList✝ } ↔ a = { toList := toList✝ }.toList

Tactic:
simp

Result:
no goals
-- Mathlib/RepresentationTheory/GroupCohomology/Functoriality.lean
theorem H0Map_id_eq_invariantsFunctor_map {A B : Rep k G} (f : A ⟶ B) :
    H0Map (MonoidHom.id G) f = (invariantsFunctor k G).map f

Proof state:
k G : Type u
inst✝¹ : CommRing k
inst✝ : Group G
A B : Rep k G
f : A ⟶ B
⊢ H0Map (MonoidHom.id G) f = (invariantsFunctor k G).map f

Tactic:
rfl

Result:
no goals
-- Mathlib/Combinatorics/Enumerative/Composition.lean
theorem boundary_last : c.boundary (Fin.last c.length) = Fin.last n

Proof state:
n : ℕ
c : Composition n
⊢ c.boundary (Fin.last c.length) = Fin.last n

Tactic:
simp [boundary, Fin.ext_iff]

Result:
no goals
-- Mathlib/Analysis/Analytic/OfScalars.lean
theorem ofScalars_norm_eq_mul :
    ‖ofScalars E c n‖ = ‖c n‖ * ‖ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 n E‖

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : SeminormedRing E
inst✝ : NormedAlgebra 𝕜 E
c : ℕ → 𝕜
n : ℕ
⊢ ‖ofScalars E c n‖ = ‖c n‖ * ‖ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 n E‖

Tactic:
rw [ofScalars, norm_smul]

Result:
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : SeminormedRing E
inst✝ : NormedAlgebra 𝕜 E
c : ℕ → 𝕜
n : ℕ
⊢ ‖c n • ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 n E‖ = ‖c n‖ * ‖ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 n E‖
-- Mathlib/Order/Bounds/Image.lean
lemma StrictAnti.map_isLeast (hf : StrictAnti f) : IsLeast (f '' s) (f a) ↔ IsGreatest s a

Proof state:
α : Type u
β : Type v
inst✝¹ : LinearOrder α
inst✝ : Preorder β
f : α → β
a : α
s : Set α
hf : StrictAnti f
⊢ IsLeast (f '' s) (f a) ↔ IsGreatest s a

Tactic:
simp [IsLeast, IsGreatest, hf.injective.eq_iff, hf.mem_lowerBounds_image]

Result:
no goals