harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/MeasureTheory/Integral/Bochner.lean
theorem integral_smul [NormedSpace 𝕜 G] [SMulCommClass ℝ 𝕜 G] (c : 𝕜) (f : α → G) :
    ∫ a, c • f a ∂μ = c • ∫ a, f a ∂μ

Proof state:
case neg
α : Type u_1
𝕜 : Type u_4
inst✝⁴ : NontriviallyNormedField 𝕜
G : Type u_5
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedSpace 𝕜 G
inst✝ : SMulCommClass ℝ 𝕜 G
c : 𝕜
f : α → G
hG : ¬CompleteSpace G
⊢ ∫ (a : α), c • f a ∂μ = c • ∫ (a : α), f a ∂μ

Tactic:
simp [integral, hG]

Result:
no goals

Proof state:
case pos
α : Type u_1
𝕜 : Type u_4
inst✝⁴ : NontriviallyNormedField 𝕜
G : Type u_5
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedSpace 𝕜 G
inst✝ : SMulCommClass ℝ 𝕜 G
c : 𝕜
f : α → G
hG : CompleteSpace G
⊢ (if h : True then
      if hf : Integrable (fun a => c • f a) μ then L1.integralCLM (Integrable.toL1 (fun a => c • f a) hf) else 0
    else 0) =
    c •
      if h : True then
        if hf : Integrable (fun a => f a) μ then L1.integralCLM (Integrable.toL1 (fun a => f a) hf) else 0
      else 0

Tactic:
exact setToFun_smul (dominatedFinMeasAdditive_weightedSMul μ) weightedSMul_smul c f

Result:
no goals

Proof state:
case pos
α : Type u_1
𝕜 : Type u_4
inst✝⁴ : NontriviallyNormedField 𝕜
G : Type u_5
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedSpace 𝕜 G
inst✝ : SMulCommClass ℝ 𝕜 G
c : 𝕜
f : α → G
hG : CompleteSpace G
⊢ ∫ (a : α), c • f a ∂μ = c • ∫ (a : α), f a ∂μ

Tactic:
simp only [integral, hG, L1.integral]

Result:
case pos
α : Type u_1
𝕜 : Type u_4
inst✝⁴ : NontriviallyNormedField 𝕜
G : Type u_5
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedSpace 𝕜 G
inst✝ : SMulCommClass ℝ 𝕜 G
c : 𝕜
f : α → G
hG : CompleteSpace G
⊢ (if h : True then
      if hf : Integrable (fun a => c • f a) μ then L1.integralCLM (Integrable.toL1 (fun a => c • f a) hf) else 0
    else 0) =
    c •
      if h : True then
        if hf : Integrable (fun a => f a) μ then L1.integralCLM (Integrable.toL1 (fun a => f a) hf) else 0
      else 0

Proof state:
α : Type u_1
𝕜 : Type u_4
inst✝⁴ : NontriviallyNormedField 𝕜
G : Type u_5
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedSpace 𝕜 G
inst✝ : SMulCommClass ℝ 𝕜 G
c : 𝕜
f : α → G
⊢ ∫ (a : α), c • f a ∂μ = c • ∫ (a : α), f a ∂μ

Tactic:
by_cases hG : CompleteSpace G

Result:
case pos
α : Type u_1
𝕜 : Type u_4
inst✝⁴ : NontriviallyNormedField 𝕜
G : Type u_5
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedSpace 𝕜 G
inst✝ : SMulCommClass ℝ 𝕜 G
c : 𝕜
f : α → G
hG : CompleteSpace G
⊢ ∫ (a : α), c • f a ∂μ = c • ∫ (a : α), f a ∂μ

case neg
α : Type u_1
𝕜 : Type u_4
inst✝⁴ : NontriviallyNormedField 𝕜
G : Type u_5
inst✝³ : NormedAddCommGroup G
inst✝² : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
inst✝¹ : NormedSpace 𝕜 G
inst✝ : SMulCommClass ℝ 𝕜 G
c : 𝕜
f : α → G
hG : ¬CompleteSpace G
⊢ ∫ (a : α), c • f a ∂μ = c • ∫ (a : α), f a ∂μ
-- Mathlib/Algebra/Order/Antidiag/Nat.lean
lemma image_piFinTwoEquiv_finMulAntidiag {n : ℕ} :
    (finMulAntidiag 2 n).image (piFinTwoEquiv <| fun _ => ℕ) = divisorsAntidiagonal n

Proof state:
case h
n : ℕ
x : ℕ × ℕ
⊢ x ∈ image (⇑(piFinTwoEquiv fun x => ℕ)) (finMulAntidiag 2 n) ↔ x ∈ n.divisorsAntidiagonal

Tactic:
simp [(piFinTwoEquiv <| fun _ => ℕ).symm.surjective.exists]

Result:
no goals

Proof state:
n : ℕ
⊢ image (⇑(piFinTwoEquiv fun x => ℕ)) (finMulAntidiag 2 n) = n.divisorsAntidiagonal

Tactic:
ext x

Result:
case h
n : ℕ
x : ℕ × ℕ
⊢ x ∈ image (⇑(piFinTwoEquiv fun x => ℕ)) (finMulAntidiag 2 n) ↔ x ∈ n.divisorsAntidiagonal
-- Mathlib/Data/Int/ModEq.lean
theorem of_div (h : a / c ≡ b / c [ZMOD m / c]) (ha : c ∣ a) (ha : c ∣ b) (ha : c ∣ m) :
    a ≡ b [ZMOD m]

Proof state:
m a b c : ℤ
h : a / c ≡ b / c [ZMOD m / c]
ha✝¹ : c ∣ a
ha✝ : c ∣ b
ha : c ∣ m
⊢ a ≡ b [ZMOD m]

Tactic:
convert h.mul_left' <;> rwa [Int.mul_ediv_cancel']

Result:
no goals
-- Mathlib/Analysis/Normed/Affine/Isometry.lean
theorem linearIsometryEquiv_mk' (e : P₁ → P₂) (e' : V₁ ≃ₗᵢ[𝕜] V₂) (p h) :
    (mk' e e' p h).linearIsometryEquiv = e'

Proof state:
case h
𝕜 : Type u_1
V₁ : Type u_3
V₂ : Type u_5
P₁ : Type u_8
P₂ : Type u_11
inst✝⁸ : NormedField 𝕜
inst✝⁷ : SeminormedAddCommGroup V₁
inst✝⁶ : NormedSpace 𝕜 V₁
inst✝⁵ : PseudoMetricSpace P₁
inst✝⁴ : NormedAddTorsor V₁ P₁
inst✝³ : SeminormedAddCommGroup V₂
inst✝² : NormedSpace 𝕜 V₂
inst✝¹ : PseudoMetricSpace P₂
inst✝ : NormedAddTorsor V₂ P₂
e : P₁ → P₂
e' : V₁ ≃ₗᵢ[𝕜] V₂
p : P₁
h : ∀ (p' : P₁), e p' = e' (p' -ᵥ p) +ᵥ e p
x✝ : V₁
⊢ (mk' e e' p h).linearIsometryEquiv x✝ = e' x✝

Tactic:
rfl

Result:
no goals

Proof state:
𝕜 : Type u_1
V₁ : Type u_3
V₂ : Type u_5
P₁ : Type u_8
P₂ : Type u_11
inst✝⁸ : NormedField 𝕜
inst✝⁷ : SeminormedAddCommGroup V₁
inst✝⁶ : NormedSpace 𝕜 V₁
inst✝⁵ : PseudoMetricSpace P₁
inst✝⁴ : NormedAddTorsor V₁ P₁
inst✝³ : SeminormedAddCommGroup V₂
inst✝² : NormedSpace 𝕜 V₂
inst✝¹ : PseudoMetricSpace P₂
inst✝ : NormedAddTorsor V₂ P₂
e : P₁ → P₂
e' : V₁ ≃ₗᵢ[𝕜] V₂
p : P₁
h : ∀ (p' : P₁), e p' = e' (p' -ᵥ p) +ᵥ e p
⊢ (mk' e e' p h).linearIsometryEquiv = e'

Tactic:
ext

Result:
case h
𝕜 : Type u_1
V₁ : Type u_3
V₂ : Type u_5
P₁ : Type u_8
P₂ : Type u_11
inst✝⁸ : NormedField 𝕜
inst✝⁷ : SeminormedAddCommGroup V₁
inst✝⁶ : NormedSpace 𝕜 V₁
inst✝⁵ : PseudoMetricSpace P₁
inst✝⁴ : NormedAddTorsor V₁ P₁
inst✝³ : SeminormedAddCommGroup V₂
inst✝² : NormedSpace 𝕜 V₂
inst✝¹ : PseudoMetricSpace P₂
inst✝ : NormedAddTorsor V₂ P₂
e : P₁ → P₂
e' : V₁ ≃ₗᵢ[𝕜] V₂
p : P₁
h : ∀ (p' : P₁), e p' = e' (p' -ᵥ p) +ᵥ e p
x✝ : V₁
⊢ (mk' e e' p h).linearIsometryEquiv x✝ = e' x✝
-- Mathlib/Algebra/Algebra/NonUnitalSubalgebra.lean
theorem mem_iInf {ι : Sort*} {S : ι → NonUnitalSubalgebra R A} {x : A} :
    (x ∈ ⨅ i, S i) ↔ ∀ i, x ∈ S i

Proof state:
R : Type u
A : Type v
inst✝⁴ : CommSemiring R
inst✝³ : NonUnitalNonAssocSemiring A
inst✝² : Module R A
inst✝¹ : IsScalarTower R A A
inst✝ : SMulCommClass R A A
ι : Sort u_2
S : ι → NonUnitalSubalgebra R A
x : A
⊢ x ∈ ⨅ i, S i ↔ ∀ (i : ι), x ∈ S i

Tactic:
simp only [iInf, mem_sInf, Set.forall_mem_range]

Result:
no goals
-- Mathlib/CategoryTheory/Monoidal/Braided/Basic.lean
theorem braiding_tensor_right (X Y Z : C) :
    (β_ X (Y ⊗ Z)).hom  =
      (α_ X Y Z).inv ≫ (β_ X Y).hom ▷ Z ≫ (α_ Y X Z).hom ≫
        Y ◁ (β_ X Z).hom ≫ (α_ Y Z X).inv

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X Y Z : C
⊢ (β_ X (Y ⊗ Z)).hom = (α_ X Y Z).inv ≫ (β_ X Y).hom ▷ Z ≫ (α_ Y X Z).hom ≫ Y ◁ (β_ X Z).hom ≫ (α_ Y Z X).inv

Tactic:
apply (cancel_epi (α_ X Y Z).hom).1

Result:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X Y Z : C
⊢ (α_ X Y Z).hom ≫ (β_ X (Y ⊗ Z)).hom =
    (α_ X Y Z).hom ≫ (α_ X Y Z).inv ≫ (β_ X Y).hom ▷ Z ≫ (α_ Y X Z).hom ≫ Y ◁ (β_ X Z).hom ≫ (α_ Y Z X).inv

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X Y Z : C
⊢ (α_ X Y Z).hom ≫ (β_ X (Y ⊗ Z)).hom =
    (α_ X Y Z).hom ≫ (α_ X Y Z).inv ≫ (β_ X Y).hom ▷ Z ≫ (α_ Y X Z).hom ≫ Y ◁ (β_ X Z).hom ≫ (α_ Y Z X).inv

Tactic:
apply (cancel_mono (α_ Y Z X).hom).1

Result:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X Y Z : C
⊢ ((α_ X Y Z).hom ≫ (β_ X (Y ⊗ Z)).hom) ≫ (α_ Y Z X).hom =
    ((α_ X Y Z).hom ≫ (α_ X Y Z).inv ≫ (β_ X Y).hom ▷ Z ≫ (α_ Y X Z).hom ≫ Y ◁ (β_ X Z).hom ≫ (α_ Y Z X).inv) ≫
      (α_ Y Z X).hom

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
inst✝ : BraidedCategory C
X Y Z : C
⊢ ((α_ X Y Z).hom ≫ (β_ X (Y ⊗ Z)).hom) ≫ (α_ Y Z X).hom =
    ((α_ X Y Z).hom ≫ (α_ X Y Z).inv ≫ (β_ X Y).hom ▷ Z ≫ (α_ Y X Z).hom ≫ Y ◁ (β_ X Z).hom ≫ (α_ Y Z X).inv) ≫
      (α_ Y Z X).hom

Tactic:
simp [hexagon_forward]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lex.lean
theorem lex_irrefl {r : α → α → Prop} (irrefl : ∀ x, ¬r x x) (l : List α) : ¬Lex r l l

Proof state:
α : Type u_1
r : α → α → Prop
irrefl : ∀ (x : α), ¬r x x
a : α
l : List α
ih : ¬Lex r l l
x✝ : Lex r (a :: l) (a :: l)
h : r a a
⊢ False

Tactic:
exact irrefl _ h

Result:
no goals

Proof state:
α : Type u_1
r : α → α → Prop
irrefl : ∀ (x : α), ¬r x x
a : α
l : List α
ih : ¬Lex r l l
x✝ : Lex r (a :: l) (a :: l)
h : Lex r l l
⊢ False

Tactic:
exact ih h

Result:
no goals

Proof state:
case cons
α : Type u_1
r : α → α → Prop
irrefl : ∀ (x : α), ¬r x x
a : α
l : List α
ih : ¬Lex r l l
⊢ ¬Lex r (a :: l) (a :: l)

Tactic:
intro
| .rel h => exact irrefl _ h
| .cons h => exact ih h

Result:
no goals

Proof state:
α : Type u_1
r : α → α → Prop
irrefl : ∀ (x : α), ¬r x x
l : List α
⊢ ¬Lex r l l

Tactic:
induction l with
| nil => nofun
| cons a l ih => intro
  | .rel h => exact irrefl _ h
  | .cons h => exact ih h

Result:
no goals

Proof state:
case nil
α : Type u_1
r : α → α → Prop
irrefl : ∀ (x : α), ¬r x x
⊢ ¬Lex r [] []

Tactic:
nofun

Result:
no goals
-- Mathlib/Data/Set/Finite/Basic.lean
theorem Finite.surjOn_iff_bijOn_of_mapsTo (hs : s.Finite) (hm : MapsTo f s s) :
    SurjOn f s s ↔ BijOn f s s

Proof state:
α : Type u
s : Set α
f : α → α
hs : s.Finite
hm : MapsTo f s s
h : SurjOn f s s
this : Finite ↑s
⊢ InjOn f s

Tactic:
exact hm.restrict_inj.mp (Finite.injective_iff_surjective.mpr <| hm.restrict_surjective_iff.mpr h)

Result:
no goals

Proof state:
α : Type u
s : Set α
f : α → α
hs : s.Finite
hm : MapsTo f s s
⊢ SurjOn f s s ↔ BijOn f s s

Tactic:
refine ⟨fun h ↦ ⟨hm, ?_, h⟩, BijOn.surjOn⟩

Result:
α : Type u
s : Set α
f : α → α
hs : s.Finite
hm : MapsTo f s s
h : SurjOn f s s
⊢ InjOn f s

Proof state:
α : Type u
s : Set α
f : α → α
hs : s.Finite
hm : MapsTo f s s
h : SurjOn f s s
⊢ InjOn f s

Tactic:
have : Finite s := finite_coe_iff.mpr hs

Result:
α : Type u
s : Set α
f : α → α
hs : s.Finite
hm : MapsTo f s s
h : SurjOn f s s
this : Finite ↑s
⊢ InjOn f s
-- Mathlib/CategoryTheory/Limits/Shapes/Biproducts.lean
theorem biproduct.components_matrix (m : ⨁ f ⟶ ⨁ g) :
    (biproduct.matrix fun j k => biproduct.components m j k) = m

Proof state:
case w.w
J : Type
inst✝⁴ : Finite J
K : Type
inst✝³ : Finite K
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasFiniteBiproducts C
f : J → C
g : K → C
m : ⨁ f ⟶ ⨁ g
j✝¹ : K
j✝ : J
⊢ ι f j✝ ≫ (matrix fun j k => components m j k) ≫ π g j✝¹ = ι f j✝ ≫ m ≫ π g j✝¹

Tactic:
simp [biproduct.components]

Result:
no goals

Proof state:
J : Type
inst✝⁴ : Finite J
K : Type
inst✝³ : Finite K
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasFiniteBiproducts C
f : J → C
g : K → C
m : ⨁ f ⟶ ⨁ g
⊢ (matrix fun j k => components m j k) = m

Tactic:
ext

Result:
case w.w
J : Type
inst✝⁴ : Finite J
K : Type
inst✝³ : Finite K
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasFiniteBiproducts C
f : J → C
g : K → C
m : ⨁ f ⟶ ⨁ g
j✝¹ : K
j✝ : J
⊢ ι f j✝ ≫ (matrix fun j k => components m j k) ≫ π g j✝¹ = ι f j✝ ≫ m ≫ π g j✝¹
-- Mathlib/SetTheory/Ordinal/Exponential.lean
theorem log_le_self (b x : Ordinal) : log b x ≤ x

Proof state:
case inr.inl
b x : Ordinal.{u_1}
hx : x ≠ 0
hb : 1 < b
⊢ log b x ≤ x

Tactic:
exact (right_le_opow _ hb).trans (opow_log_le_self b hx)

Result:
no goals

Proof state:
case inr
b x : Ordinal.{u_1}
hx : x ≠ 0
⊢ log b x ≤ x

Tactic:
obtain hb | hb := lt_or_le 1 b

Result:
case inr.inl
b x : Ordinal.{u_1}
hx : x ≠ 0
hb : 1 < b
⊢ log b x ≤ x

case inr.inr
b x : Ordinal.{u_1}
hx : x ≠ 0
hb : b ≤ 1
⊢ log b x ≤ x

Proof state:
b x : Ordinal.{u_1}
⊢ log b x ≤ x

Tactic:
obtain rfl | hx := eq_or_ne x 0

Result:
case inl
b : Ordinal.{u_1}
⊢ log b 0 ≤ 0

case inr
b x : Ordinal.{u_1}
hx : x ≠ 0
⊢ log b x ≤ x

Proof state:
case inr.inr
b x : Ordinal.{u_1}
hx : x ≠ 0
hb : b ≤ 1
⊢ log b x ≤ x

Tactic:
simp_rw [log_of_left_le_one hb, Ordinal.zero_le]

Result:
no goals

Proof state:
case inl
b : Ordinal.{u_1}
⊢ log b 0 ≤ 0

Tactic:
rw [log_zero_right]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Log/Deriv.lean
lemma lt_log_one_add_of_pos {x : ℝ} (hx : 0 < x) : 2 * x / (x + 2) < log (1 + x)

Proof state:
x : ℝ
hx : 0 < x
⊢ 1 ≠ 0

Tactic:
positivity

Result:
no goals

Proof state:
x : ℝ
hx : 0 < x
⊢ 0 < 2 * (1 / (2 * ↑1 + 1)) * (x / (x + 2)) ^ (2 * 1 + 1)

Tactic:
positivity

Result:
no goals

Proof state:
case h.e'_3
x : ℝ
hx : 0 < x
⊢ 2 * x / (x + 2) = 2 * (1 / (2 * ↑0 + 1)) * (x / (x + 2)) ^ (2 * 0 + 1)

Tactic:
field_simp

Result:
no goals

Proof state:
x : ℝ
hx : 0 < x
j✝ : ℕ
a✝ : j✝ ≠ 0
⊢ 0 ≤ 2 * (1 / (2 * ↑j✝ + 1)) * (x / (x + 2)) ^ (2 * j✝ + 1)

Tactic:
positivity

Result:
no goals

Proof state:
x : ℝ
hx : 0 < x
⊢ ∀ (j : ℕ), j ≠ 0 → 0 ≤ 2 * (1 / (2 * ↑j + 1)) * (x / (x + 2)) ^ (2 * j + 1)

Tactic:
intros

Result:
x : ℝ
hx : 0 < x
j✝ : ℕ
a✝ : j✝ ≠ 0
⊢ 0 ≤ 2 * (1 / (2 * ↑j✝ + 1)) * (x / (x + 2)) ^ (2 * j✝ + 1)

Proof state:
x : ℝ
hx : 0 < x
⊢ 2 * x / (x + 2) < log (1 + x)

Tactic:
convert lt_hasSum (hasSum_log_one_add hx.le) 0 (by intros; positivity)
  1 (by positivity) (by positivity) using 1

Result:
case h.e'_3
x : ℝ
hx : 0 < x
⊢ 2 * x / (x + 2) = 2 * (1 / (2 * ↑0 + 1)) * (x / (x + 2)) ^ (2 * 0 + 1)
-- Mathlib/Topology/PartitionOfUnity.lean
theorem exists_finset_nhd (ρ : PartitionOfUnity ι X univ) (x₀ : X) :
    ∃ I : Finset ι, ∀ᶠ x in 𝓝 x₀, ∑ i ∈ I, ρ i x = 1 ∧ support (ρ · x) ⊆ I

Proof state:
case h
ι : Type u
X : Type v
inst✝ : TopologicalSpace X
ρ : PartitionOfUnity ι X
x₀ : X
I : Finset ι
H : (∀ᶠ (x : X) in 𝓝[univ] x₀, ∑ i ∈ I, (ρ i) x = 1) ∧ ∀ᶠ (x : X) in 𝓝 x₀, (support fun x_1 => (ρ x_1) x) ⊆ ↑I
⊢ ∀ᶠ (x : X) in 𝓝 x₀, ∑ i ∈ I, (ρ i) x = 1 ∧ (support fun x_1 => (ρ x_1) x) ⊆ ↑I

Tactic:
rwa [nhdsWithin_univ, ← eventually_and] at H

Result:
no goals

Proof state:
case intro
ι : Type u
X : Type v
inst✝ : TopologicalSpace X
ρ : PartitionOfUnity ι X
x₀ : X
I : Finset ι
H : (∀ᶠ (x : X) in 𝓝[univ] x₀, ∑ i ∈ I, (ρ i) x = 1) ∧ ∀ᶠ (x : X) in 𝓝 x₀, (support fun x_1 => (ρ x_1) x) ⊆ ↑I
⊢ ∃ I, ∀ᶠ (x : X) in 𝓝 x₀, ∑ i ∈ I, (ρ i) x = 1 ∧ (support fun x_1 => (ρ x_1) x) ⊆ ↑I

Tactic:
use I

Result:
case h
ι : Type u
X : Type v
inst✝ : TopologicalSpace X
ρ : PartitionOfUnity ι X
x₀ : X
I : Finset ι
H : (∀ᶠ (x : X) in 𝓝[univ] x₀, ∑ i ∈ I, (ρ i) x = 1) ∧ ∀ᶠ (x : X) in 𝓝 x₀, (support fun x_1 => (ρ x_1) x) ⊆ ↑I
⊢ ∀ᶠ (x : X) in 𝓝 x₀, ∑ i ∈ I, (ρ i) x = 1 ∧ (support fun x_1 => (ρ x_1) x) ⊆ ↑I

Proof state:
ι : Type u
X : Type v
inst✝ : TopologicalSpace X
ρ : PartitionOfUnity ι X
x₀ : X
⊢ ∃ I, ∀ᶠ (x : X) in 𝓝 x₀, ∑ i ∈ I, (ρ i) x = 1 ∧ (support fun x_1 => (ρ x_1) x) ⊆ ↑I

Tactic:
rcases ρ.exists_finset_nhd' x₀ with ⟨I, H⟩

Result:
case intro
ι : Type u
X : Type v
inst✝ : TopologicalSpace X
ρ : PartitionOfUnity ι X
x₀ : X
I : Finset ι
H : (∀ᶠ (x : X) in 𝓝[univ] x₀, ∑ i ∈ I, (ρ i) x = 1) ∧ ∀ᶠ (x : X) in 𝓝 x₀, (support fun x_1 => (ρ x_1) x) ⊆ ↑I
⊢ ∃ I, ∀ᶠ (x : X) in 𝓝 x₀, ∑ i ∈ I, (ρ i) x = 1 ∧ (support fun x_1 => (ρ x_1) x) ⊆ ↑I
-- Mathlib/Analysis/Normed/Group/Basic.lean
theorem nnnorm_multiset_prod_le (m : Multiset E) : ‖m.prod‖₊ ≤ (m.map fun x => ‖x‖₊).sum :=
  NNReal.coe_le_coe.1 <| by
    push_cast
    rw [Multiset.map_map]
    exact norm_multiset_prod_le _

Proof state:
E : Type u_5
inst✝ : SeminormedCommGroup E
m : Multiset E
⊢ ‖m.prod‖ ≤ (Multiset.map toReal (Multiset.map (fun x => ‖x‖₊) m)).sum

Tactic:
rw [Multiset.map_map]

Result:
E : Type u_5
inst✝ : SeminormedCommGroup E
m : Multiset E
⊢ ‖m.prod‖ ≤ (Multiset.map (toReal ∘ fun x => ‖x‖₊) m).sum

Proof state:
E : Type u_5
inst✝ : SeminormedCommGroup E
m : Multiset E
⊢ ‖m.prod‖ ≤ (Multiset.map (toReal ∘ fun x => ‖x‖₊) m).sum

Tactic:
exact norm_multiset_prod_le _

Result:
no goals

Proof state:
E : Type u_5
inst✝ : SeminormedCommGroup E
m : Multiset E
⊢ ↑‖m.prod‖₊ ≤ ↑(Multiset.map (fun x => ‖x‖₊) m).sum

Tactic:
push_cast

Result:
E : Type u_5
inst✝ : SeminormedCommGroup E
m : Multiset E
⊢ ‖m.prod‖ ≤ (Multiset.map toReal (Multiset.map (fun x => ‖x‖₊) m)).sum
-- Mathlib/Data/QPF/Multivariate/Constructions/Cofix.lean
theorem Cofix.dest_mk {α : TypeVec n} (x : F (α.append1 <| Cofix F α)) :
    Cofix.dest (Cofix.mk x) = x

Proof state:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
x : F (α ::: Cofix F α)
⊢ (mk x).dest = x

Tactic:
have : Cofix.mk ∘ Cofix.dest = @_root_.id (Cofix F α) := funext Cofix.mk_dest

Result:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
x : F (α ::: Cofix F α)
this : mk ∘ dest = _root_.id
⊢ (mk x).dest = x

Proof state:
n : ℕ
F : TypeVec.{u} (n + 1) → Type u
q : MvQPF F
α : TypeVec.{u} n
x : F (α ::: Cofix F α)
this : mk ∘ dest = _root_.id
⊢ (mk x).dest = x

Tactic:
rw [Cofix.mk, Cofix.dest_corec, ← comp_map, ← Cofix.mk, ← appendFun_comp, this, id_comp,
  appendFun_id_id, MvFunctor.id_map]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Find.lean
theorem map_findSome? (f : α → Option β) (g : β → γ) (l : List α) :
    (l.findSome? f).map g = l.findSome? (Option.map g ∘ f)

Proof state:
case cons
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → Option β
g : β → γ
head✝ : α
tail✝ : List α
tail_ih✝ : Option.map g (findSome? f tail✝) = findSome? (Option.map g ∘ f) tail✝
⊢ Option.map g
      (match f head✝ with
      | some b => some b
      | none => findSome? f tail✝) =
    match Option.map g (f head✝) with
    | some b => some b
    | none => findSome? (Option.map g ∘ f) tail✝

Tactic:
split <;> simp [*]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → Option β
g : β → γ
l : List α
⊢ Option.map g (findSome? f l) = findSome? (Option.map g ∘ f) l

Tactic:
induction l <;> simp [findSome?_cons]

Result:
case cons
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → Option β
g : β → γ
head✝ : α
tail✝ : List α
tail_ih✝ : Option.map g (findSome? f tail✝) = findSome? (Option.map g ∘ f) tail✝
⊢ Option.map g
      (match f head✝ with
      | some b => some b
      | none => findSome? f tail✝) =
    match Option.map g (f head✝) with
    | some b => some b
    | none => findSome? (Option.map g ∘ f) tail✝
-- Mathlib/RingTheory/Ideal/Quotient/Operations.lean
lemma comap_map_mk {I J : Ideal R} [I.IsTwoSided] (h : I ≤ J) :
    Ideal.comap (Ideal.Quotient.mk I) (Ideal.map (Ideal.Quotient.mk I) J) = J

Proof state:
case h
R : Type u
inst✝¹ : Ring R
I J : Ideal R
inst✝ : I.IsTwoSided
h : I ≤ J
x✝ : R
⊢ x✝ ∈ comap (Quotient.mk I) (map (Quotient.mk I) J) ↔ x✝ ∈ J

Tactic:
rw [← Ideal.mem_quotient_iff_mem h, Ideal.mem_comap]

Result:
no goals

Proof state:
R : Type u
inst✝¹ : Ring R
I J : Ideal R
inst✝ : I.IsTwoSided
h : I ≤ J
⊢ comap (Quotient.mk I) (map (Quotient.mk I) J) = J

Tactic:
ext

Result:
case h
R : Type u
inst✝¹ : Ring R
I J : Ideal R
inst✝ : I.IsTwoSided
h : I ≤ J
x✝ : R
⊢ x✝ ∈ comap (Quotient.mk I) (map (Quotient.mk I) J) ↔ x✝ ∈ J
-- Mathlib/Analysis/Calculus/FDeriv/Comp.lean
theorem fderivWithin_comp_of_eq {g : F → G} {t : Set F} {y : F}
    (hg : DifferentiableWithinAt 𝕜 g t y) (hf : DifferentiableWithinAt 𝕜 f s x) (h : MapsTo f s t)
    (hxs : UniqueDiffWithinAt 𝕜 s x) (hy : f x = y) :
    fderivWithin 𝕜 (g ∘ f) s x = (fderivWithin 𝕜 g t (f x)).comp (fderivWithin 𝕜 f s x)

Proof state:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : E → F
x : E
s : Set E
g : F → G
t : Set F
hf : DifferentiableWithinAt 𝕜 f s x
h : MapsTo f s t
hxs : UniqueDiffWithinAt 𝕜 s x
hg : DifferentiableWithinAt 𝕜 g t (f x)
⊢ fderivWithin 𝕜 (g ∘ f) s x = (fderivWithin 𝕜 g t (f x)).comp (fderivWithin 𝕜 f s x)

Tactic:
exact fderivWithin_comp _ hg hf h hxs

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : E → F
x : E
s : Set E
g : F → G
t : Set F
y : F
hg : DifferentiableWithinAt 𝕜 g t y
hf : DifferentiableWithinAt 𝕜 f s x
h : MapsTo f s t
hxs : UniqueDiffWithinAt 𝕜 s x
hy : f x = y
⊢ fderivWithin 𝕜 (g ∘ f) s x = (fderivWithin 𝕜 g t (f x)).comp (fderivWithin 𝕜 f s x)

Tactic:
subst hy

Result:
𝕜 : Type u_1
inst✝⁶ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
F : Type u_3
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
G : Type u_4
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : E → F
x : E
s : Set E
g : F → G
t : Set F
hf : DifferentiableWithinAt 𝕜 f s x
h : MapsTo f s t
hxs : UniqueDiffWithinAt 𝕜 s x
hg : DifferentiableWithinAt 𝕜 g t (f x)
⊢ fderivWithin 𝕜 (g ∘ f) s x = (fderivWithin 𝕜 g t (f x)).comp (fderivWithin 𝕜 f s x)
-- Mathlib/AlgebraicGeometry/ResidueField.lean
lemma descResidueField_stalkClosedPointTo_fromSpecResidueField
    (K : Type u) [Field K] (X : Scheme.{u}) (f : Spec (.of K) ⟶ X) :
    Spec.map (@descResidueField (CommRingCat.of K) _ X _ (Scheme.stalkClosedPointTo f)
        _) ≫
      X.fromSpecResidueField (f.base (closedPoint K)) = f

Proof state:
K : Type u
inst✝ : Field K
X : Scheme
f : Spec (CommRingCat.of K) ⟶ X
⊢ Spec.map (descResidueField (stalkClosedPointTo f)) ≫
      X.fromSpecResidueField ((ConcreteCategory.hom f.base) (closedPoint K)) =
    f

Tactic:
rw [X.descResidueField_fromSpecResidueField]

Result:
K : Type u
inst✝ : Field K
X : Scheme
f : Spec (CommRingCat.of K) ⟶ X
⊢ Spec.map (stalkClosedPointTo f) ≫ X.fromSpecStalk ((ConcreteCategory.hom f.base) (closedPoint ↑(CommRingCat.of K))) =
    f

Proof state:
K : Type u
inst✝ : Field K
X : Scheme
f : Spec (CommRingCat.of K) ⟶ X
⊢ Spec.map (stalkClosedPointTo f) ≫ X.fromSpecStalk ((ConcreteCategory.hom f.base) (closedPoint ↑(CommRingCat.of K))) =
    f

Tactic:
rw [Scheme.Spec_stalkClosedPointTo_fromSpecStalk]

Result:
no goals
-- Mathlib/CategoryTheory/Monoidal/End.lean
theorem η_naturality {X Y : C} (f : X ⟶ Y) [F.OplaxMonoidal]:
    (η F).app X ≫ (𝟙_ (C ⥤ C)).map f = (η F).app X ≫ f

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
M : Type u_1
inst✝² : Category.{u_2, u_1} M
inst✝¹ : MonoidalCategory M
F : M ⥤ C ⥤ C
X Y : C
f : X ⟶ Y
inst✝ : F.OplaxMonoidal
⊢ (η F).app X ≫ (𝟙_ (C ⥤ C)).map f = (η F).app X ≫ f

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Multiset/Replicate.lean
theorem le_count_iff_replicate_le {a : α} {s : Multiset α} {n : ℕ} :
    n ≤ count a s ↔ replicate n a ≤ s :=
  Quot.inductionOn s fun _l => by
    simp only [quot_mk_to_coe'', mem_coe, coe_count]
    exact le_count_iff_replicate_sublist.trans replicate_le_coe.symm

Proof state:
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Multiset α
n : ℕ
_l : List α
⊢ n ≤ List.count a _l ↔ replicate n a ≤ ↑_l

Tactic:
exact le_count_iff_replicate_sublist.trans replicate_le_coe.symm

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Multiset α
n : ℕ
_l : List α
⊢ n ≤ count a (Quot.mk (⇑(isSetoid α)) _l) ↔ replicate n a ≤ Quot.mk (⇑(isSetoid α)) _l

Tactic:
simp only [quot_mk_to_coe'', mem_coe, coe_count]

Result:
α : Type u_1
inst✝ : DecidableEq α
a : α
s : Multiset α
n : ℕ
_l : List α
⊢ n ≤ List.count a _l ↔ replicate n a ≤ ↑_l