harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Probability/UniformOn.lean
theorem uniformOn_union (hs : s.Finite) (htu : Disjoint t u) :
    uniformOn s (t ∪ u) = uniformOn s t + uniformOn s u

Proof state:
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s t u : Set Ω
hs : s.Finite
htu : Disjoint t u
⊢ (uniformOn s) (t ∪ u) = (uniformOn s) t + (uniformOn s) u

Tactic:
rw [uniformOn, cond_apply hs.measurableSet, cond_apply hs.measurableSet,
  cond_apply hs.measurableSet, Set.inter_union_distrib_left, measure_union, mul_add]

Result:
case hd
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s t u : Set Ω
hs : s.Finite
htu : Disjoint t u
⊢ Disjoint (s ∩ t) (s ∩ u)

case h
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s t u : Set Ω
hs : s.Finite
htu : Disjoint t u
⊢ MeasurableSet (s ∩ u)

Proof state:
case hd
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s t u : Set Ω
hs : s.Finite
htu : Disjoint t u
⊢ Disjoint (s ∩ t) (s ∩ u)

case h
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s t u : Set Ω
hs : s.Finite
htu : Disjoint t u
⊢ MeasurableSet (s ∩ u)

Tactic:
exacts [htu.mono inf_le_right inf_le_right, (hs.inter_of_left _).measurableSet]

Result:
no goals
-- Mathlib/CategoryTheory/Comma/Presheaf/Basic.lean
/-- "Functoriality" of `MakesOverArrow η s` in `η`. -/
lemma map₁ {F G : Cᵒᵖ ⥤ Type v} {η : F ⟶ A} {μ : G ⟶ A} {ε : F ⟶ G}
    (hε : ε ≫ μ = η) {X : C} {s : yoneda.obj X ⟶ A} {u : F.obj (op X)}
    (h : MakesOverArrow η s u) : MakesOverArrow μ s (ε.app _ u) :=
  ⟨by rw [← elementwise_of% NatTrans.comp_app ε μ, hε, h.app]⟩

Proof state:
C : Type u
inst✝ : Category.{v, u} C
A F G : Cᵒᵖ ⥤ Type v
η : F ⟶ A
μ : G ⟶ A
ε : F ⟶ G
hε : ε ≫ μ = η
X : C
s : yoneda.obj X ⟶ A
u : F.obj (op X)
h : MakesOverArrow η s u
⊢ μ.app (op X) (ε.app (op X) u) = yonedaEquiv s

Tactic:
rw [← elementwise_of% NatTrans.comp_app ε μ, hε, h.app]

Result:
no goals
-- Mathlib/RingTheory/GradedAlgebra/HomogeneousLocalization.lean
lemma val_awayMap_mk (n a i hi) : (awayMap 𝒜 hg hx (mk ⟨n, a, ⟨f ^ i, hi⟩, ⟨i, rfl⟩⟩)).val =
    Localization.mk (a * g ^ i) ⟨x ^ i, (Submonoid.mem_powers_iff _ _).mpr ⟨i, rfl⟩⟩

Proof state:
ι : Type u_1
R : Type u_2
A : Type u_3
inst✝⁵ : CommRing R
inst✝⁴ : CommRing A
inst✝³ : Algebra R A
𝒜 : ι → Submodule R A
inst✝² : AddCommMonoid ι
inst✝¹ : DecidableEq ι
inst✝ : GradedAlgebra 𝒜
e : ι
f g : A
hg : g ∈ 𝒜 e
x : A
hx : x = f * g
n : ι
a : ↥(𝒜 n)
i : ℕ
hi : f ^ i ∈ 𝒜 n
⊢ val ((awayMap 𝒜 hg hx) (mk { deg := n, num := a, den := ⟨f ^ i, hi⟩, den_mem := ⋯ })) =
    Localization.mk (↑a * g ^ i) ⟨x ^ i, ⋯⟩

Tactic:
rw [val_awayMap_eq_aux, awayMapAux_mk 𝒜 (hx := hx)]

Result:
no goals
-- Mathlib/Analysis/MeanInequalities.lean
theorem rpow_sum_le_const_mul_sum_rpow_of_nonneg (hp : 1 ≤ p) (hf : ∀ i ∈ s, 0 ≤ f i) :
    (∑ i ∈ s, f i) ^ p ≤ (#s : ℝ) ^ (p - 1) * ∑ i ∈ s, f i ^ p

Proof state:
ι : Type u
s : Finset ι
f : ι → ℝ
p : ℝ
hp : 1 ≤ p
hf : ∀ i ∈ s, 0 ≤ f i
⊢ (∑ i ∈ s, f i) ^ p ≤ ↑(#s) ^ (p - 1) * ∑ i ∈ s, f i ^ p

Tactic:
convert rpow_sum_le_const_mul_sum_rpow s f hp using 2 <;> apply sum_congr rfl <;> intro i hi <;>
  simp only [abs_of_nonneg, hf i hi]

Result:
no goals
-- Mathlib/Logic/Equiv/Basic.lean
theorem comp_swap_eq_update (i j : α) (f : α → β) :
    f ∘ Equiv.swap i j = update (update f j (f i)) i (f j)

Proof state:
α : Sort u_1
β : Sort u_4
inst✝ : DecidableEq α
i j : α
f : α → β
⊢ f ∘ ⇑(swap i j) = update (update f j (f i)) i (f j)

Tactic:
rw [swap_eq_update, comp_update, comp_update, comp_id]

Result:
no goals
-- Mathlib/Algebra/Order/SuccPred.lean
theorem le_sub_one_iff_of_not_isMin (hy : ¬ IsMin y) : x ≤ y - 1 ↔ x < y

Proof state:
α : Type u_1
x y : α
inst✝³ : Preorder α
inst✝² : Sub α
inst✝¹ : One α
inst✝ : PredSubOrder α
hy : ¬IsMin y
⊢ x ≤ y - 1 ↔ x < y

Tactic:
rw [← pred_eq_sub_one, le_pred_iff_of_not_isMin hy]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Coeff.lean
theorem coeff_X_pow_mul' (p : R[X]) (n d : ℕ) :
    (X ^ n * p).coeff d = ite (n ≤ d) (p.coeff (d - n)) 0

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
n d : ℕ
⊢ (X ^ n * p).coeff d = if n ≤ d then p.coeff (d - n) else 0

Tactic:
rw [(commute_X_pow p n).eq, coeff_mul_X_pow']

Result:
no goals
-- Mathlib/CategoryTheory/Sites/Subcanonical.lean
/-- See also `yonedaEquiv_naturality'` for a more general version. -/
lemma yonedaEquiv_naturality {X Y : C} {F : Sheaf J (Type v)} (f : J.yoneda.obj X ⟶ F)
    (g : Y ⟶ X) : F.val.map g.op (J.yonedaEquiv f) = J.yonedaEquiv (J.yoneda.map g ≫ f)

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
inst✝ : J.Subcanonical
X Y : C
F : Sheaf J (Type v)
f : J.yoneda.obj X ⟶ F
g : Y ⟶ X
⊢ F.val.map g.op (J.yonedaEquiv f) = J.yonedaEquiv (J.yoneda.map g ≫ f)

Tactic:
simp [yonedaEquiv, CategoryTheory.yonedaEquiv_naturality]

Result:
C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
inst✝ : J.Subcanonical
X Y : C
F : Sheaf J (Type v)
f : J.yoneda.obj X ⟶ F
g : Y ⟶ X
⊢ CategoryTheory.yoneda.map g ≫ (fullyFaithfulSheafToPresheaf J (Type v)).homEquiv f =
    (fullyFaithfulSheafToPresheaf J (Type v)).homEquiv (J.yoneda.map g ≫ f)

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
inst✝ : J.Subcanonical
X Y : C
F : Sheaf J (Type v)
f : J.yoneda.obj X ⟶ F
g : Y ⟶ X
⊢ CategoryTheory.yoneda.map g ≫ (fullyFaithfulSheafToPresheaf J (Type v)).homEquiv f =
    (fullyFaithfulSheafToPresheaf J (Type v)).homEquiv (J.yoneda.map g ≫ f)

Tactic:
rfl

Result:
no goals
-- Mathlib/Topology/Category/UniformSpace.lean
theorem extension_comp_coe {X : UniformSpaceCat} {Y : CpltSepUniformSpace}
    (f : toUniformSpace (CpltSepUniformSpace.of (Completion X)) ⟶ toUniformSpace Y) :
    extensionHom (completionHom X ≫ f) = f

Proof state:
case h.a.h
X : UniformSpaceCat
Y : CpltSepUniformSpace
f : (CpltSepUniformSpace.of (Completion X.carrier)).toUniformSpace ⟶ Y.toUniformSpace
x : (completionFunctor.obj X).α
⊢ ↑(ConcreteCategory.hom (extensionHom (X.completionHom ≫ f))) x = ↑(ConcreteCategory.hom f) x

Tactic:
exact congr_fun (Completion.extension_comp_coe f.hom.property) x

Result:
no goals

Proof state:
X : UniformSpaceCat
Y : CpltSepUniformSpace
f : (CpltSepUniformSpace.of (Completion X.carrier)).toUniformSpace ⟶ Y.toUniformSpace
⊢ extensionHom (X.completionHom ≫ f) = f

Tactic:
ext x

Result:
case h.a.h
X : UniformSpaceCat
Y : CpltSepUniformSpace
f : (CpltSepUniformSpace.of (Completion X.carrier)).toUniformSpace ⟶ Y.toUniformSpace
x : (completionFunctor.obj X).α
⊢ ↑(ConcreteCategory.hom (extensionHom (X.completionHom ≫ f))) x = ↑(ConcreteCategory.hom f) x
-- Mathlib/ModelTheory/Equivalence.lean
theorem iff_all_liftAt : φ ⇔[T] (φ.liftAt 1 n).all :=
  fun M v xs => by
  rw [realize_iff, realize_all_liftAt_one_self]

Proof state:
L : Language
T : L.Theory
α : Type w
n : ℕ
φ : L.BoundedFormula α n
M : T.ModelType
v : α → ↑M
xs : Fin n → ↑M
⊢ (φ ⇔ ∀'liftAt 1 n φ).Realize v xs

Tactic:
rw [realize_iff, realize_all_liftAt_one_self]

Result:
no goals
-- Mathlib/Analysis/Matrix.lean
theorem nnnorm_lt_iff {r : ℝ≥0} (hr : 0 < r) {A : Matrix m n α} :
    ‖A‖₊ < r ↔ ∀ i j, ‖A i j‖₊ < r

Proof state:
m : Type u_3
n : Type u_4
α : Type u_5
inst✝² : Fintype m
inst✝¹ : Fintype n
inst✝ : SeminormedAddCommGroup α
r : ℝ≥0
hr : 0 < r
A : Matrix m n α
⊢ ‖A‖₊ < r ↔ ∀ (i : m) (j : n), ‖A i j‖₊ < r

Tactic:
simp_rw [nnnorm_def, pi_nnnorm_lt_iff hr]

Result:
no goals
-- Mathlib/Algebra/AddConstMap/Basic.lean
theorem map_add_int' [AddGroupWithOne G] [AddGroup H] [AddConstMapClass F G H 1 b]
    (f : F) (x : G) (n : ℤ) : f (x + n) = f x + n • b

Proof state:
F : Type u_1
G : Type u_2
H : Type u_3
inst✝³ : FunLike F G H
b : H
inst✝² : AddGroupWithOne G
inst✝¹ : AddGroup H
inst✝ : AddConstMapClass F G H 1 b
f : F
x : G
n : ℤ
⊢ f (x + ↑n) = f x + n • b

Tactic:
rw [← map_add_zsmul f x n, zsmul_one]

Result:
no goals
-- Mathlib/Data/Multiset/Bind.lean
theorem singleton_bind : bind {a} f = f a

Proof state:
α : Type u_1
β : Type v
a : α
f : α → Multiset β
⊢ {a}.bind f = f a

Tactic:
simp [bind]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Bool.lean
theorem not_and : ∀ (x y : Bool), (!(x && y)) = (!x || !y)

Proof state:
⊢ ∀ (x y : Bool), (!(x && y)) = (!x || !y)

Tactic:
decide

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem getKeyD_ofList_of_mem [EquivBEq α] [LawfulHashable α]
    {l : List (α × β)}
    {k k' fallback : α} (k_beq : k == k')
    (distinct : l.Pairwise (fun a b => (a.1 == b.1) = false))
    (mem : k ∈ l.map Prod.fst) :
    (ofList l).getKeyD k' fallback = k

Proof state:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
β : Type v
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
l : List (α × β)
k k' fallback : α
k_beq : (k == k') = true
distinct : List.Pairwise (fun a b => (a.fst == b.fst) = false) l
mem : k ∈ List.map Prod.fst l
⊢ (ofList l).getKeyD k' fallback = k

Tactic:
simp_to_raw using Raw₀.Const.getKeyD_insertMany_empty_list_of_mem

Result:
no goals
-- Mathlib/Topology/Algebra/Category/ProfiniteGrp/Limits.lean
theorem toLimit_surjective (P : ProfiniteGrp.{u}) : Function.Surjective (toLimit P)

Proof state:
P : ProfiniteGrp.{u}
⊢ Function.Surjective ⇑(Hom.hom P.toLimit)

Tactic:
have : IsClosed (Set.range P.toLimit) :=
  P.toLimit.hom.continuous_toFun.isClosedMap.isClosed_range

Result:
P : ProfiniteGrp.{u}
this : IsClosed (Set.range ⇑(Hom.hom P.toLimit))
⊢ Function.Surjective ⇑(Hom.hom P.toLimit)

Proof state:
P : ProfiniteGrp.{u}
this : IsClosed (Set.range ⇑(Hom.hom P.toLimit))
⊢ Function.Surjective ⇑(Hom.hom P.toLimit)

Tactic:
rw [← Set.range_eq_univ, ← closure_eq_iff_isClosed.mpr this,
  Dense.closure_eq (denseRange_toLimit P)]

Result:
no goals
-- Mathlib/Geometry/Manifold/Algebra/LieGroup.lean
theorem ContMDiff.div {f g : M → G} (hf : ContMDiff I' I n f) (hg : ContMDiff I' I n g) :
    ContMDiff I' I n fun x => f x / g 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
n : WithTop ℕ∞
G : Type u_4
inst✝⁸ : TopologicalSpace G
inst✝⁷ : ChartedSpace H G
inst✝⁶ : Group G
E' : Type u_5
inst✝⁵ : NormedAddCommGroup E'
inst✝⁴ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝³ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M : Type u_7
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H' M
inst✝ : LieGroup I n G
f g : M → G
hf : ContMDiff I' I n f
hg : ContMDiff I' I n g
⊢ ContMDiff I' I n fun x => f x / g x

Tactic:
simp_rw [div_eq_mul_inv]

Result:
𝕜 : 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
n : WithTop ℕ∞
G : Type u_4
inst✝⁸ : TopologicalSpace G
inst✝⁷ : ChartedSpace H G
inst✝⁶ : Group G
E' : Type u_5
inst✝⁵ : NormedAddCommGroup E'
inst✝⁴ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝³ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M : Type u_7
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H' M
inst✝ : LieGroup I n G
f g : M → G
hf : ContMDiff I' I n f
hg : ContMDiff I' I n g
⊢ ContMDiff I' I n fun x => f x * (g 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
n : WithTop ℕ∞
G : Type u_4
inst✝⁸ : TopologicalSpace G
inst✝⁷ : ChartedSpace H G
inst✝⁶ : Group G
E' : Type u_5
inst✝⁵ : NormedAddCommGroup E'
inst✝⁴ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝³ : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M : Type u_7
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H' M
inst✝ : LieGroup I n G
f g : M → G
hf : ContMDiff I' I n f
hg : ContMDiff I' I n g
⊢ ContMDiff I' I n fun x => f x * (g x)⁻¹

Tactic:
exact hf.mul hg.inv

Result:
no goals
-- Mathlib/RingTheory/Valuation/ValExtension.lean
theorem val_smul (r : vR.integer) (a : vA.integer) : ↑(r • a : vA.integer) = (r : R) • (a : A)

Proof state:
R : Type u_1
A : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : Ring A
inst✝³ : Algebra R A
ΓR : Type u_6
ΓA : Type u_7
inst✝² : LinearOrderedCommGroupWithZero ΓR
inst✝¹ : LinearOrderedCommGroupWithZero ΓA
vR : Valuation R ΓR
vA : Valuation A ΓA
inst✝ : IsValExtension vR vA
r : ↥vR.integer
a : ↥vA.integer
⊢ ↑(r • a) = ↑r • ↑a

Tactic:
rfl

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/Deriv.lean
theorem contDiffAt_rpow_of_ne (p : ℝ × ℝ) (hp : p.1 ≠ 0) {n : WithTop ℕ∞} :
    ContDiffAt ℝ n (fun p : ℝ × ℝ => p.1 ^ p.2) p

Proof state:
case inl
p : ℝ × ℝ
hp : p.1 ≠ 0
n : WithTop ℕ∞
hneg : p.1 < 0
⊢ ContDiffAt ℝ n (fun p => p.1 ^ p.2) p

case inr
p : ℝ × ℝ
hp : p.1 ≠ 0
n : WithTop ℕ∞
hpos : 0 < p.1
⊢ ContDiffAt ℝ n (fun p => p.1 ^ p.2) p

Tactic:
exacts
  [(((contDiffAt_fst.log hneg.ne).mul contDiffAt_snd).exp.mul
        (contDiffAt_snd.mul contDiffAt_const).cos).congr_of_eventuallyEq
    ((continuousAt_fst.eventually (gt_mem_nhds hneg)).mono fun p hp => rpow_def_of_neg hp _),
  ((contDiffAt_fst.log hpos.ne').mul contDiffAt_snd).exp.congr_of_eventuallyEq
    ((continuousAt_fst.eventually (lt_mem_nhds hpos)).mono fun p hp => rpow_def_of_pos hp _)]

Result:
no goals

Proof state:
p : ℝ × ℝ
hp : p.1 ≠ 0
n : WithTop ℕ∞
⊢ ContDiffAt ℝ n (fun p => p.1 ^ p.2) p

Tactic:
rcases hp.lt_or_lt with hneg | hpos

Result:
case inl
p : ℝ × ℝ
hp : p.1 ≠ 0
n : WithTop ℕ∞
hneg : p.1 < 0
⊢ ContDiffAt ℝ n (fun p => p.1 ^ p.2) p

case inr
p : ℝ × ℝ
hp : p.1 ≠ 0
n : WithTop ℕ∞
hpos : 0 < p.1
⊢ ContDiffAt ℝ n (fun p => p.1 ^ p.2) p
-- Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Unital.lean
lemma cfc_apply_of_not_predicate {f : R → R} (a : A) (ha : ¬ p a) :
    cfc f a = 0

Proof state:
R : Type u_1
A : Type u_2
p : A → Prop
inst✝⁸ : CommSemiring R
inst✝⁷ : StarRing R
inst✝⁶ : MetricSpace R
inst✝⁵ : IsTopologicalSemiring R
inst✝⁴ : ContinuousStar R
inst✝³ : TopologicalSpace A
inst✝² : Ring A
inst✝¹ : StarRing A
inst✝ : Algebra R A
instCFC : ContinuousFunctionalCalculus R p
f : R → R
a : A
ha : ¬p a
⊢ cfc f a = 0

Tactic:
rw [cfc_def, dif_neg (not_and_of_not_left _ ha)]

Result:
no goals
-- Mathlib/Logic/Function/Basic.lean
theorem not_injective_iff : ¬ Injective f ↔ ∃ a b, f a = f b ∧ a ≠ b

Proof state:
α : Sort u_1
β : Sort u_2
f : α → β
⊢ ¬Injective f ↔ ∃ a b, f a = f b ∧ a ≠ b

Tactic:
simp only [Injective, not_forall, exists_prop]

Result:
no goals
-- Mathlib/CategoryTheory/ObjectProperty/Shift.lean
lemma shift_shift (a b c : A) (h : a + b = c) [P.IsClosedUnderIsomorphisms] :
    (P.shift b).shift a = P.shift c

Proof state:
case h.a
C : Type u_1
inst✝³ : Category.{u_3, u_1} C
P : ObjectProperty C
A : Type u_2
inst✝² : AddMonoid A
inst✝¹ : HasShift C A
a b c : A
h : a + b = c
inst✝ : P.IsClosedUnderIsomorphisms
X : C
⊢ (P.shift b).shift a X ↔ P.shift c X

Tactic:
exact P.prop_iff_of_iso ((shiftFunctorAdd' C a b c h).symm.app X)

Result:
no goals

Proof state:
C : Type u_1
inst✝³ : Category.{u_3, u_1} C
P : ObjectProperty C
A : Type u_2
inst✝² : AddMonoid A
inst✝¹ : HasShift C A
a b c : A
h : a + b = c
inst✝ : P.IsClosedUnderIsomorphisms
⊢ (P.shift b).shift a = P.shift c

Tactic:
ext X

Result:
case h.a
C : Type u_1
inst✝³ : Category.{u_3, u_1} C
P : ObjectProperty C
A : Type u_2
inst✝² : AddMonoid A
inst✝¹ : HasShift C A
a b c : A
h : a + b = c
inst✝ : P.IsClosedUnderIsomorphisms
X : C
⊢ (P.shift b).shift a X ↔ P.shift c X
-- Mathlib/MeasureTheory/Integral/IntervalIntegral.lean
theorem integral_comp_mul_add (hc : c ≠ 0) (d) :
    (∫ x in a..b, f (c * x + d)) = c⁻¹ • ∫ x in c * a + d..c * b + d, f x

Proof state:
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a b c : ℝ
f : ℝ → E
hc : c ≠ 0
d : ℝ
⊢ ∫ (x : ℝ) in a..b, f (c * x + d) = c⁻¹ • ∫ (x : ℝ) in c * a + d..c * b + d, f x

Tactic:
rw [← integral_comp_add_right, ← integral_comp_mul_left _ hc]

Result:
no goals
-- Mathlib/Topology/ContinuousMap/Compact.lean
@[simp] lemma nnnorm_smul_const {R β : Type*} [NormedAddCommGroup β] [NormedDivisionRing R]
    [Module R β] [BoundedSMul R β] (f : C(α, R)) (b : β) :
    ‖f • const α b‖₊ = ‖f‖₊ * ‖b‖₊

Proof state:
α : Type u_1
inst✝⁵ : TopologicalSpace α
inst✝⁴ : CompactSpace α
R : Type u_4
β : Type u_5
inst✝³ : NormedAddCommGroup β
inst✝² : NormedDivisionRing R
inst✝¹ : Module R β
inst✝ : BoundedSMul R β
f : C(α, R)
b : β
⊢ ‖f • const α b‖₊ = ‖f‖₊ * ‖b‖₊

Tactic:
simp only [nnnorm_eq_iSup_nnnorm, smul_apply', const_apply, nnnorm_smul, iSup_mul]

Result:
no goals
-- Mathlib/GroupTheory/GroupExtension/Defs.lean
theorem rightHom_inl (n : N) : S.rightHom (S.inl n) = 1

Proof state:
N : Type u_1
E : Type u_2
G : Type u_3
inst✝² : Group N
inst✝¹ : Group E
inst✝ : Group G
S : GroupExtension N E G
n : N
⊢ ∃ x, S.inl x = S.inl n

Tactic:
exact exists_apply_eq_apply S.inl n

Result:
no goals

Proof state:
N : Type u_1
E : Type u_2
G : Type u_3
inst✝² : Group N
inst✝¹ : Group E
inst✝ : Group G
S : GroupExtension N E G
n : N
⊢ S.rightHom (S.inl n) = 1

Tactic:
rw [← MonoidHom.mem_ker, ← S.range_inl_eq_ker_rightHom, MonoidHom.mem_range]

Result:
N : Type u_1
E : Type u_2
G : Type u_3
inst✝² : Group N
inst✝¹ : Group E
inst✝ : Group G
S : GroupExtension N E G
n : N
⊢ ∃ x, S.inl x = S.inl n
-- Mathlib/Algebra/Group/Submonoid/Membership.lean
theorem exists_list_of_mem_closure {s : Set M} {x : M} (hx : x ∈ closure s) :
    ∃ l : List M, (∀ y ∈ l, y ∈ s) ∧ l.prod = x

Proof state:
M : Type u_1
inst✝ : Monoid M
s : Set M
x : M
hx : x ∈ closure s
⊢ ∃ l, (∀ y ∈ l, y ∈ s) ∧ l.prod = x

Tactic:
rwa [← SetLike.mem_coe, closure_eq_image_prod, Set.mem_image] at hx

Result:
no goals
-- Mathlib/MeasureTheory/Integral/SetIntegral.lean
theorem setIntegral_withDensity_eq_setIntegral_smul₀ {f : X → ℝ≥0} {s : Set X}
    (hf : AEMeasurable f (μ.restrict s)) (g : X → E) (hs : MeasurableSet s) :
    ∫ x in s, g x ∂μ.withDensity (fun x => f x) = ∫ x in s, f x • g x ∂μ

Proof state:
X : Type u_1
E : Type u_3
inst✝² : MeasurableSpace X
μ : Measure X
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : X → ℝ≥0
s : Set X
hf : AEMeasurable f (μ.restrict s)
g : X → E
hs : MeasurableSet s
⊢ (∫ (x : X) in s, g x ∂μ.withDensity fun x => ↑(f x)) = ∫ (x : X) in s, f x • g x ∂μ

Tactic:
rw [restrict_withDensity hs, integral_withDensity_eq_integral_smul₀ hf]

Result:
no goals
-- Mathlib/Algebra/BigOperators/Finsupp.lean
theorem prod_add_index' [AddZeroClass M] [CommMonoid N] {f g : α →₀ M} {h : α → M → N}
    (h_zero : ∀ a, h a 0 = 1) (h_add : ∀ a b₁ b₂, h a (b₁ + b₂) = h a b₁ * h a b₂) :
    (f + g).prod h = f.prod h * g.prod h

Proof state:
α : Type u_1
M : Type u_8
N : Type u_10
inst✝¹ : AddZeroClass M
inst✝ : CommMonoid N
f g : α →₀ M
h : α → M → N
h_zero : ∀ (a : α), h a 0 = 1
h_add : ∀ (a : α) (b₁ b₂ : M), h a (b₁ + b₂) = h a b₁ * h a b₂
⊢ (f + g).prod h = f.prod h * g.prod h

Tactic:
exact prod_add_index (fun a _ => h_zero a) fun a _ => h_add a

Result:
no goals

Proof state:
α : Type u_1
M : Type u_8
N : Type u_10
inst✝¹ : AddZeroClass M
inst✝ : CommMonoid N
f g : α →₀ M
h : α → M → N
h_zero : ∀ (a : α), h a 0 = 1
h_add : ∀ (a : α) (b₁ b₂ : M), h a (b₁ + b₂) = h a b₁ * h a b₂
⊢ (f + g).prod h = f.prod h * g.prod h

Tactic:
classical exact prod_add_index (fun a _ => h_zero a) fun a _ => h_add a

Result:
no goals
-- Mathlib/Order/SuccPred/Limit.lean
lemma _root_.IsGLB.isPredLimit_of_not_mem {s : Set α} (hs : IsGLB s a) (hs' : s.Nonempty)
    (ha : a ∉ s) : IsPredLimit a

Proof state:
α : Type u_1
a : α
inst✝ : LinearOrder α
s : Set α
hs : IsGLB s a
hs' : s.Nonempty
ha : a ∉ s
⊢ IsPredLimit a

Tactic:
simpa using (IsGLB.dual hs).isSuccLimit_of_not_mem hs' ha

Result:
no goals
-- Mathlib/Analysis/Convex/Cone/Proper.lean
theorem pointed_zero : ((0 : ProperCone 𝕜 E) : ConvexCone 𝕜 E).Pointed

Proof state:
𝕜 : Type u_1
inst✝⁴ : OrderedSemiring 𝕜
E : Type u_2
inst✝³ : AddCommMonoid E
inst✝² : TopologicalSpace E
inst✝¹ : T1Space E
inst✝ : Module 𝕜 E
⊢ (↑↑0).Pointed

Tactic:
simp [ConvexCone.pointed_zero]

Result:
no goals
-- Mathlib/RingTheory/IsAdjoinRoot.lean
theorem basis_one (h : IsAdjoinRootMonic S f) (hdeg : 1 < natDegree f) :
    h.basis ⟨1, hdeg⟩ = h.root

Proof state:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
f : R[X]
inst✝ : Algebra R S
h : IsAdjoinRootMonic S f
hdeg : 1 < f.natDegree
⊢ h.basis ⟨1, hdeg⟩ = h.root

Tactic:
rw [h.basis_apply, Fin.val_mk, pow_one]

Result:
no goals
-- Mathlib/FieldTheory/KrullTopology.lean
@[simp] lemma IntermediateField.fixingSubgroup_top (K L : Type*) [Field K] [Field L] [Algebra K L] :
    IntermediateField.fixingSubgroup (⊤ : IntermediateField K L) = ⊥

Proof state:
case h
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
x✝ : L ≃ₐ[K] L
⊢ x✝ ∈ ⊤.fixingSubgroup ↔ x✝ ∈ ⊥

Tactic:
simp [mem_fixingSubgroup_iff, DFunLike.ext_iff]

Result:
no goals

Proof state:
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
⊢ ⊤.fixingSubgroup = ⊥

Tactic:
ext

Result:
case h
K : Type u_1
L : Type u_2
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
x✝ : L ≃ₐ[K] L
⊢ x✝ ∈ ⊤.fixingSubgroup ↔ x✝ ∈ ⊥
-- Mathlib/Topology/Constructions.lean
theorem continuous_sigma_map {f₁ : ι → κ} {f₂ : ∀ i, σ i → τ (f₁ i)} :
    Continuous (Sigma.map f₁ f₂) ↔ ∀ i, Continuous (f₂ i) :=
  continuous_sigma_iff.trans <| by
    simp only [Sigma.map, IsEmbedding.sigmaMk.continuous_iff, comp_def]

Proof state:
ι : Type u_5
κ : Type u_6
σ : ι → Type u_7
τ : κ → Type u_8
inst✝¹ : (i : ι) → TopologicalSpace (σ i)
inst✝ : (k : κ) → TopologicalSpace (τ k)
f₁ : ι → κ
f₂ : (i : ι) → σ i → τ (f₁ i)
⊢ (∀ (i : ι), Continuous fun a => Sigma.map f₁ f₂ ⟨i, a⟩) ↔ ∀ (i : ι), Continuous (f₂ i)

Tactic:
simp only [Sigma.map, IsEmbedding.sigmaMk.continuous_iff, comp_def]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Option/Attach.lean
theorem toList_attach (o : Option α) :
    o.attach.toList = o.toList.attach.map fun ⟨x, h⟩ => ⟨x, by simpa using h⟩

Proof state:
α : Type u_1
o : Option α
⊢ o.attach.toList =
    List.map
      (fun x =>
        match x with
        | ⟨x, h⟩ => ⟨x, ⋯⟩)
      o.toList.attach

Tactic:
cases o <;> simp

Result:
no goals

Proof state:
α : Type ?u.7680
o : Option α
x✝ : { x // x ∈ o.toList }
x : α
h : x ∈ o.toList
⊢ x ∈ o

Tactic:
simpa using h

Result:
no goals
-- Mathlib/Topology/Sets/OpenCover.lean
lemma iUnion_inter (hu : IsOpenCover u) (s : Set X) :
    ⋃ i, s ∩ u i = s

Proof state:
ι : Type u_1
X : Type u_3
inst✝ : TopologicalSpace X
u : ι → Opens X
hu : IsOpenCover u
s : Set X
⊢ ⋃ i, s ∩ ↑(u i) = s

Tactic:
simp [← inter_iUnion, hu.iSup_set_eq_univ]

Result:
no goals
-- Mathlib/LinearAlgebra/AffineSpace/AffineSubspace/Defs.lean
theorem directionOfNonempty_eq_direction {s : AffineSubspace k P} (h : (s : Set P).Nonempty) :
    directionOfNonempty h = s.direction

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
h : (↑s).Nonempty
⊢ directionOfNonempty h ≤ s.direction

Tactic:
rw [← SetLike.coe_subset_coe, directionOfNonempty, direction, Submodule.coe_set_mk,
  AddSubmonoid.coe_set_mk]

Result:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
h : (↑s).Nonempty
⊢ ↑{ carrier := ↑s -ᵥ ↑s, add_mem' := ⋯ } ⊆ ↑(vectorSpan k ↑s)

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
h : (↑s).Nonempty
⊢ ↑{ carrier := ↑s -ᵥ ↑s, add_mem' := ⋯ } ⊆ ↑(vectorSpan k ↑s)

Tactic:
exact vsub_set_subset_vectorSpan k _

Result:
no goals

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
h : (↑s).Nonempty
⊢ directionOfNonempty h = s.direction

Tactic:
refine le_antisymm ?_ (Submodule.span_le.2 Set.Subset.rfl)

Result:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
h : (↑s).Nonempty
⊢ directionOfNonempty h ≤ s.direction