harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/Finset/Sum.lean
@[simp] lemma toLeft_insert_inr : (insert (inr b) u).toLeft = u.toLeft

Proof state:
α : Type u_1
β : Type u_2
b : β
u : Finset (α ⊕ β)
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
⊢ (insert (inr b) u).toLeft = u.toLeft

Tactic:
ext y

Result:
case h
α : Type u_1
β : Type u_2
b : β
u : Finset (α ⊕ β)
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
y : α
⊢ y ∈ (insert (inr b) u).toLeft ↔ y ∈ u.toLeft

Proof state:
case h
α : Type u_1
β : Type u_2
b : β
u : Finset (α ⊕ β)
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
y : α
⊢ y ∈ (insert (inr b) u).toLeft ↔ y ∈ u.toLeft

Tactic:
simp

Result:
no goals
-- Mathlib/Order/Interval/Set/Basic.lean
theorem Ico_insert_right (h : a ≤ b) : insert b (Ico a b) = Icc a b

Proof state:
α : Type u_1
inst✝ : PartialOrder α
a b : α
h : a ≤ b
⊢ insert b (Ico a b) = Icc a b

Tactic:
rw [insert_eq, union_comm, Ico_union_right h]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem toFin_or (x y : BitVec v) :
    BitVec.toFin (x ||| y) = BitVec.toFin x ||| BitVec.toFin y

Proof state:
v : Nat
x y : BitVec v
⊢ (x ||| y).toFin = x.toFin ||| y.toFin

Tactic:
apply Fin.eq_of_val_eq

Result:
case a
v : Nat
x y : BitVec v
⊢ ↑(x ||| y).toFin = ↑(x.toFin ||| y.toFin)

Proof state:
case a
v : Nat
x y : BitVec v
⊢ ↑(x ||| y).toFin = ↑(x.toFin ||| y.toFin)

Tactic:
exact (Nat.mod_eq_of_lt <| Nat.or_lt_two_pow x.isLt y.isLt).symm

Result:
no goals
-- Mathlib/Algebra/Polynomial/Expand.lean
theorem isCoprime_expand {f g : R[X]} {p : ℕ} (hp : p ≠ 0) :
    IsCoprime (expand R p f) (expand R p g) ↔ IsCoprime f g :=
  ⟨fun ⟨a, b, eq⟩ ↦ ⟨contract p a, contract p b, by
    simp_rw [← contract_mul_expand hp, ← contract_add hp, eq, ← C_1, contract_C]⟩, (·.map _)⟩

Proof state:
R : Type u
inst✝ : CommSemiring R
f g : R[X]
p : ℕ
hp : p ≠ 0
x✝ : IsCoprime ((expand R p) f) ((expand R p) g)
a b : R[X]
eq : a * (expand R p) f + b * (expand R p) g = 1
⊢ contract p a * f + contract p b * g = 1

Tactic:
simp_rw [← contract_mul_expand hp, ← contract_add hp, eq, ← C_1, contract_C]

Result:
no goals
-- Mathlib/LinearAlgebra/Finsupp/LinearCombination.lean
theorem linearCombination_fin_zero (f : Fin 0 → M) : linearCombination R f = 0

Proof state:
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f : Fin 0 → M
⊢ linearCombination R f = 0

Tactic:
ext i

Result:
case h.h
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f : Fin 0 → M
i : Fin 0
⊢ (linearCombination R f ∘ₗ lsingle i) 1 = (0 ∘ₗ lsingle i) 1

Proof state:
case h.h
M : Type u_2
R : Type u_5
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f : Fin 0 → M
i : Fin 0
⊢ (linearCombination R f ∘ₗ lsingle i) 1 = (0 ∘ₗ lsingle i) 1

Tactic:
apply finZeroElim i

Result:
no goals
-- Mathlib/Data/Complex/Trigonometric.lean
theorem sin_three_mul : sin (3 * x) = 3 * sin x - 4 * sin x ^ 3

Proof state:
x : ℝ
⊢ ↑(sin (3 * x)) = ↑(3 * sin x - 4 * sin x ^ 3)

Tactic:
simp [sin_three_mul]

Result:
no goals

Proof state:
x : ℝ
⊢ sin (3 * x) = 3 * sin x - 4 * sin x ^ 3

Tactic:
rw [← ofReal_inj]

Result:
x : ℝ
⊢ ↑(sin (3 * x)) = ↑(3 * sin x - 4 * sin x ^ 3)
-- Mathlib/LinearAlgebra/Lagrange.lean
theorem degree_interpolate_lt (hvs : Set.InjOn v s) : (interpolate s v r).degree < #s

Proof state:
case inl
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
v r : ι → F
hvs : Set.InjOn v ↑∅
⊢ ⊥ < ↑0

Tactic:
exact WithBot.bot_lt_coe _

Result:
no goals

Proof state:
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
v r : ι → F
hvs : Set.InjOn v ↑s
⊢ ((interpolate s v) r).degree < ↑(#s)

Tactic:
rcases eq_empty_or_nonempty s with (rfl | h)

Result:
case inl
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
v r : ι → F
hvs : Set.InjOn v ↑∅
⊢ ((interpolate ∅ v) r).degree < ↑(#∅)

case inr
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
v r : ι → F
hvs : Set.InjOn v ↑s
h : s.Nonempty
⊢ ((interpolate s v) r).degree < ↑(#s)

Proof state:
case inl
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
v r : ι → F
hvs : Set.InjOn v ↑∅
⊢ ((interpolate ∅ v) r).degree < ↑(#∅)

Tactic:
rw [interpolate_empty, degree_zero, card_empty]

Result:
case inl
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
v r : ι → F
hvs : Set.InjOn v ↑∅
⊢ ⊥ < ↑0

Proof state:
case inr
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
v r : ι → F
hvs : Set.InjOn v ↑s
h : s.Nonempty
⊢ ((interpolate s v) r).degree < ↑(#s)

Tactic:
refine lt_of_le_of_lt (degree_interpolate_le _ hvs) ?_

Result:
case inr
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
v r : ι → F
hvs : Set.InjOn v ↑s
h : s.Nonempty
⊢ ↑(#s - 1) < ↑(#s)

Proof state:
case inr
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
v r : ι → F
hvs : Set.InjOn v ↑s
h : s.Nonempty
⊢ #s - 1 < #s

Tactic:
exact Nat.sub_lt (Nonempty.card_pos h) zero_lt_one

Result:
no goals

Proof state:
case inr
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
v r : ι → F
hvs : Set.InjOn v ↑s
h : s.Nonempty
⊢ ↑(#s - 1) < ↑(#s)

Tactic:
rw [Nat.cast_withBot, WithBot.coe_lt_coe]

Result:
case inr
F : Type u_1
inst✝¹ : Field F
ι : Type u_2
inst✝ : DecidableEq ι
s : Finset ι
v r : ι → F
hvs : Set.InjOn v ↑s
h : s.Nonempty
⊢ #s - 1 < #s
-- Mathlib/RingTheory/SimpleModule/Basic.lean
theorem isSimpleModule_self_iff_isUnit :
    IsSimpleModule R R ↔ Nontrivial R ∧ ∀ x : R, x ≠ 0 → IsUnit x :=
  isSimpleModule_iff_toSpanSingleton_surjective.trans <| and_congr_right fun _ ↦ by
    refine ⟨fun h x hx ↦ ?_, fun h x hx ↦ (h x hx).unit.mulRight_bijective.surjective⟩
    obtain ⟨y, hyx : y * x = 1⟩ := h x hx 1
    have hy : y ≠ 0 := left_ne_zero_of_mul (hyx.symm ▸ one_ne_zero)
    obtain ⟨z, hzy : z * y = 1⟩ := h y hy 1
    exact ⟨⟨x, y, left_inv_eq_right_inv hzy hyx ▸ hzy, hyx⟩, rfl⟩

Proof state:
case intro
R : Type u_2
inst✝ : Ring R
x✝ : Nontrivial R
h : ∀ (x : R), x ≠ 0 → Function.Surjective ⇑(LinearMap.toSpanSingleton R R x)
x : R
hx : x ≠ 0
y : R
hyx : y * x = 1
⊢ IsUnit x

Tactic:
have hy : y ≠ 0 := left_ne_zero_of_mul (hyx.symm ▸ one_ne_zero)

Result:
case intro
R : Type u_2
inst✝ : Ring R
x✝ : Nontrivial R
h : ∀ (x : R), x ≠ 0 → Function.Surjective ⇑(LinearMap.toSpanSingleton R R x)
x : R
hx : x ≠ 0
y : R
hyx : y * x = 1
hy : y ≠ 0
⊢ IsUnit x

Proof state:
case intro
R : Type u_2
inst✝ : Ring R
x✝ : Nontrivial R
h : ∀ (x : R), x ≠ 0 → Function.Surjective ⇑(LinearMap.toSpanSingleton R R x)
x : R
hx : x ≠ 0
y : R
hyx : y * x = 1
hy : y ≠ 0
⊢ IsUnit x

Tactic:
obtain ⟨z, hzy : z * y = 1⟩ := h y hy 1

Result:
case intro.intro
R : Type u_2
inst✝ : Ring R
x✝ : Nontrivial R
h : ∀ (x : R), x ≠ 0 → Function.Surjective ⇑(LinearMap.toSpanSingleton R R x)
x : R
hx : x ≠ 0
y : R
hyx : y * x = 1
hy : y ≠ 0
z : R
hzy : z * y = 1
⊢ IsUnit x

Proof state:
case intro.intro
R : Type u_2
inst✝ : Ring R
x✝ : Nontrivial R
h : ∀ (x : R), x ≠ 0 → Function.Surjective ⇑(LinearMap.toSpanSingleton R R x)
x : R
hx : x ≠ 0
y : R
hyx : y * x = 1
hy : y ≠ 0
z : R
hzy : z * y = 1
⊢ IsUnit x

Tactic:
exact ⟨⟨x, y, left_inv_eq_right_inv hzy hyx ▸ hzy, hyx⟩, rfl⟩

Result:
no goals

Proof state:
R : Type u_2
inst✝ : Ring R
x✝ : Nontrivial R
h : ∀ (x : R), x ≠ 0 → Function.Surjective ⇑(LinearMap.toSpanSingleton R R x)
x : R
hx : x ≠ 0
⊢ IsUnit x

Tactic:
obtain ⟨y, hyx : y * x = 1⟩ := h x hx 1

Result:
case intro
R : Type u_2
inst✝ : Ring R
x✝ : Nontrivial R
h : ∀ (x : R), x ≠ 0 → Function.Surjective ⇑(LinearMap.toSpanSingleton R R x)
x : R
hx : x ≠ 0
y : R
hyx : y * x = 1
⊢ IsUnit x

Proof state:
R : Type u_2
inst✝ : Ring R
x✝ : Nontrivial R
⊢ (∀ (x : R), x ≠ 0 → Function.Surjective ⇑(LinearMap.toSpanSingleton R R x)) ↔ ∀ (x : R), x ≠ 0 → IsUnit x

Tactic:
refine ⟨fun h x hx ↦ ?_, fun h x hx ↦ (h x hx).unit.mulRight_bijective.surjective⟩

Result:
R : Type u_2
inst✝ : Ring R
x✝ : Nontrivial R
h : ∀ (x : R), x ≠ 0 → Function.Surjective ⇑(LinearMap.toSpanSingleton R R x)
x : R
hx : x ≠ 0
⊢ IsUnit x
-- Mathlib/LinearAlgebra/SesquilinearForm.lean
@[simp]
lemma _root_.LinearEquiv.isAdjointPair_symm_iff {f : M ≃ M} :
    LinearMap.IsAdjointPair B B f f.symm ↔ B.IsOrthogonal f :=
  ⟨fun hf x y ↦ by simpa using hf x (f y), fun hf x y ↦ by simpa using hf x (f.symm y)⟩

Proof state:
R : Type u_20
M : Type u_21
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
B : LinearMap.BilinForm R M
f : M ≃ M
hf : IsAdjointPair B B ⇑f ⇑f.symm
x y : M
⊢ (B (f x)) (f y) = (B x) y

Tactic:
simpa using hf x (f y)

Result:
no goals

Proof state:
R : Type u_20
M : Type u_21
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
B : LinearMap.BilinForm R M
f : M ≃ M
hf : IsOrthogonal B ⇑f
x y : M
⊢ (B (f x)) y = (B x) (f.symm y)

Tactic:
simpa using hf x (f.symm y)

Result:
no goals
-- Mathlib/MeasureTheory/Integral/Bochner.lean
theorem integral_undef {f : α → G} (h : ¬Integrable f μ) : ∫ a, f a ∂μ = 0

Proof state:
case neg
α : Type u_1
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
f : α → G
h : ¬Integrable f μ
hG : ¬CompleteSpace G
⊢ ∫ (a : α), f a ∂μ = 0

Tactic:
simp [integral, hG]

Result:
no goals

Proof state:
case pos
α : Type u_1
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
f : α → G
h : ¬Integrable f μ
hG : CompleteSpace G
⊢ ∫ (a : α), f a ∂μ = 0

Tactic:
simp [integral, hG, h]

Result:
no goals

Proof state:
α : Type u_1
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
f : α → G
h : ¬Integrable f μ
⊢ ∫ (a : α), f a ∂μ = 0

Tactic:
by_cases hG : CompleteSpace G

Result:
case pos
α : Type u_1
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
f : α → G
h : ¬Integrable f μ
hG : CompleteSpace G
⊢ ∫ (a : α), f a ∂μ = 0

case neg
α : Type u_1
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
f : α → G
h : ¬Integrable f μ
hG : ¬CompleteSpace G
⊢ ∫ (a : α), f a ∂μ = 0
-- Mathlib/Topology/ContinuousMap/Bounded/Basic.lean
theorem arzela_ascoli₂ (s : Set β) (hs : IsCompact s) (A : Set (α →ᵇ β)) (closed : IsClosed A)
    (in_s : ∀ (f : α →ᵇ β) (x : α), f ∈ A → f x ∈ s) (H : Equicontinuous ((↑) : A → α → β)) :
    IsCompact A

Proof state:
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : CompactSpace α
inst✝ : PseudoMetricSpace β
s : Set β
hs : IsCompact s
A : Set (α →ᵇ β)
closed : IsClosed A
in_s : ∀ (f : α →ᵇ β) (x : α), f ∈ A → f x ∈ s
H : Equicontinuous fun x => ⇑↑x
M : LipschitzWith 1 Subtype.val
F : (α →ᵇ ↑s) → α →ᵇ β := comp Subtype.val M
⊢ IsCompact A

Tactic:
refine IsCompact.of_isClosed_subset ((?_ : IsCompact (F ⁻¹' A)).image (continuous_comp M)) closed
    fun f hf => ?_

Result:
case refine_1
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : CompactSpace α
inst✝ : PseudoMetricSpace β
s : Set β
hs : IsCompact s
A : Set (α →ᵇ β)
closed : IsClosed A
in_s : ∀ (f : α →ᵇ β) (x : α), f ∈ A → f x ∈ s
H : Equicontinuous fun x => ⇑↑x
M : LipschitzWith 1 Subtype.val
F : (α →ᵇ ↑s) → α →ᵇ β := comp Subtype.val M
⊢ IsCompact (F ⁻¹' A)

case refine_2
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : CompactSpace α
inst✝ : PseudoMetricSpace β
s : Set β
hs : IsCompact s
A : Set (α →ᵇ β)
closed : IsClosed A
in_s : ∀ (f : α →ᵇ β) (x : α), f ∈ A → f x ∈ s
H : Equicontinuous fun x => ⇑↑x
M : LipschitzWith 1 Subtype.val
F : (α →ᵇ ↑s) → α →ᵇ β := comp Subtype.val M
f : α →ᵇ β
hf : f ∈ A
⊢ f ∈ comp Subtype.val M '' (F ⁻¹' A)

Proof state:
case refine_1
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : CompactSpace α
inst✝ : PseudoMetricSpace β
s : Set β
hs : IsCompact s
A : Set (α →ᵇ β)
closed : IsClosed A
in_s : ∀ (f : α →ᵇ β) (x : α), f ∈ A → f x ∈ s
H : Equicontinuous fun x => ⇑↑x
M : LipschitzWith 1 Subtype.val
F : (α →ᵇ ↑s) → α →ᵇ β := comp Subtype.val M
this : CompactSpace ↑s
⊢ IsCompact (F ⁻¹' A)

Tactic:
refine arzela_ascoli₁ _ (continuous_iff_isClosed.1 (continuous_comp M) _ closed) ?_

Result:
case refine_1
α : Type u
β : Type v
inst✝² : TopologicalSpace α
inst✝¹ : CompactSpace α
inst✝ : PseudoMetricSpace β
s : Set β
hs : IsCompact s
A : Set (α →ᵇ β)
closed : IsClosed A
in_s : ∀ (f : α →ᵇ β) (x : α), f ∈ A → f x ∈ s
H : Equicontinuous fun x => ⇑↑x
M : LipschitzWith 1 Subtype.val
F : (α →ᵇ ↑s) → α →ᵇ β := comp Subtype.val M
this : CompactSpace ↑s
⊢ Equicontinuous fun x => ⇑↑x
-- Mathlib/Data/Finsupp/BigOperators.lean
theorem List.support_sum_subset [AddMonoid M] (l : List (ι →₀ M)) :
    l.sum.support ⊆ l.foldr (Finsupp.support · ⊔ ·) ∅

Proof state:
ι : Type u_1
M : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : AddMonoid M
l : List (ι →₀ M)
⊢ l.sum.support ⊆ foldr (fun x1 x2 => x1.support ⊔ x2) ∅ l

Tactic:
induction' l with hd tl IH

Result:
case nil
ι : Type u_1
M : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : AddMonoid M
⊢ [].sum.support ⊆ foldr (fun x1 x2 => x1.support ⊔ x2) ∅ []

case cons
ι : Type u_1
M : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : AddMonoid M
hd : ι →₀ M
tl : List (ι →₀ M)
IH : tl.sum.support ⊆ foldr (fun x1 x2 => x1.support ⊔ x2) ∅ tl
⊢ (hd :: tl).sum.support ⊆ foldr (fun x1 x2 => x1.support ⊔ x2) ∅ (hd :: tl)

Proof state:
case cons
ι : Type u_1
M : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : AddMonoid M
hd : ι →₀ M
tl : List (ι →₀ M)
IH : tl.sum.support ⊆ foldr (fun x1 x2 => x1.support ⊔ x2) ∅ tl
⊢ hd.support ⊆ hd.support

Tactic:
rfl

Result:
no goals

Proof state:
case nil
ι : Type u_1
M : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : AddMonoid M
⊢ [].sum.support ⊆ foldr (fun x1 x2 => x1.support ⊔ x2) ∅ []

Tactic:
simp

Result:
no goals

Proof state:
case cons
ι : Type u_1
M : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : AddMonoid M
hd : ι →₀ M
tl : List (ι →₀ M)
IH : tl.sum.support ⊆ foldr (fun x1 x2 => x1.support ⊔ x2) ∅ tl
⊢ (hd + tl.sum).support ⊆ foldr (fun x1 x2 => x1.support ⊔ x2) ∅ (hd :: tl)

Tactic:
refine Finsupp.support_add.trans (Finset.union_subset_union ?_ IH)

Result:
case cons
ι : Type u_1
M : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : AddMonoid M
hd : ι →₀ M
tl : List (ι →₀ M)
IH : tl.sum.support ⊆ foldr (fun x1 x2 => x1.support ⊔ x2) ∅ tl
⊢ hd.support ⊆ hd.support

Proof state:
case cons
ι : Type u_1
M : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : AddMonoid M
hd : ι →₀ M
tl : List (ι →₀ M)
IH : tl.sum.support ⊆ foldr (fun x1 x2 => x1.support ⊔ x2) ∅ tl
⊢ (hd :: tl).sum.support ⊆ foldr (fun x1 x2 => x1.support ⊔ x2) ∅ (hd :: tl)

Tactic:
simp only [List.sum_cons, Finset.union_comm]

Result:
case cons
ι : Type u_1
M : Type u_2
inst✝¹ : DecidableEq ι
inst✝ : AddMonoid M
hd : ι →₀ M
tl : List (ι →₀ M)
IH : tl.sum.support ⊆ foldr (fun x1 x2 => x1.support ⊔ x2) ∅ tl
⊢ (hd + tl.sum).support ⊆ foldr (fun x1 x2 => x1.support ⊔ x2) ∅ (hd :: tl)
-- Mathlib/Probability/Kernel/Composition/CompProd.lean
lemma compProd_sum_right {ι : Type*} [Countable ι]
    {κ : Kernel α β} {η : ι → Kernel (α × β) γ} [∀ i, IsSFiniteKernel (η i)] :
    κ ⊗ₖ Kernel.sum η = Kernel.sum (fun i ↦ κ ⊗ₖ (η i))

Proof state:
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
ι : Type u_4
inst✝¹ : Countable ι
κ : Kernel α β
η : ι → Kernel (α × β) γ
inst✝ : ∀ (i : ι), IsSFiniteKernel (η i)
hκ : IsSFiniteKernel κ
⊢ κ ⊗ₖ Kernel.sum η = Kernel.sum fun i => κ ⊗ₖ η i

Tactic:
ext a s hs

Result:
case pos.h.h
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
ι : Type u_4
inst✝¹ : Countable ι
κ : Kernel α β
η : ι → Kernel (α × β) γ
inst✝ : ∀ (i : ι), IsSFiniteKernel (η i)
hκ : IsSFiniteKernel κ
a : α
s : Set (β × γ)
hs : MeasurableSet s
⊢ ((κ ⊗ₖ Kernel.sum η) a) s = ((Kernel.sum fun i => κ ⊗ₖ η i) a) s
-- Mathlib/Data/Set/Function.lean
theorem surjOn_iff_exists_bijOn_subset : SurjOn f s t ↔ ∃ s' ⊆ s, BijOn f s' t

Proof state:
case mp.inr
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
ht : t.Nonempty
⊢ SurjOn f s t → ∃ s' ⊆ s, BijOn f s' t

Tactic:
intro h

Result:
case mp.inr
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
ht : t.Nonempty
h : SurjOn f s t
⊢ ∃ s' ⊆ s, BijOn f s' t

Proof state:
case mpr
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
⊢ (∃ s' ⊆ s, BijOn f s' t) → SurjOn f s t

Tactic:
rintro ⟨s', hs', hfs'⟩

Result:
case mpr.intro.intro
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
s' : Set α
hs' : s' ⊆ s
hfs' : BijOn f s' t
⊢ SurjOn f s t

Proof state:
case mp.inr
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
ht : t.Nonempty
h : SurjOn f s t
this : Nonempty α
⊢ ∃ s' ⊆ s, BijOn f s' t

Tactic:
exact ⟨_, h.mapsTo_invFunOn.image_subset, h.bijOn_subset⟩

Result:
no goals

Proof state:
case mpr.intro.intro
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
s' : Set α
hs' : s' ⊆ s
hfs' : BijOn f s' t
⊢ SurjOn f s t

Tactic:
exact hfs'.surjOn.mono hs' (Subset.refl _)

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
⊢ SurjOn f s t ↔ ∃ s' ⊆ s, BijOn f s' t

Tactic:
constructor

Result:
case mp
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
⊢ SurjOn f s t → ∃ s' ⊆ s, BijOn f s' t

case mpr
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
⊢ (∃ s' ⊆ s, BijOn f s' t) → SurjOn f s t

Proof state:
case mp.inl
α : Type u_1
β : Type u_2
s : Set α
f : α → β
⊢ SurjOn f s ∅ → ∃ s' ⊆ s, BijOn f s' ∅

Tactic:
exact fun _ => ⟨∅, empty_subset _, bijOn_empty f⟩

Result:
no goals

Proof state:
case mp.inr
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
ht : t.Nonempty
h : SurjOn f s t
⊢ ∃ s' ⊆ s, BijOn f s' t

Tactic:
haveI : Nonempty α := ⟨Classical.choose (h.comap_nonempty ht)⟩

Result:
case mp.inr
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
ht : t.Nonempty
h : SurjOn f s t
this : Nonempty α
⊢ ∃ s' ⊆ s, BijOn f s' t

Proof state:
case mp
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
⊢ SurjOn f s t → ∃ s' ⊆ s, BijOn f s' t

Tactic:
rcases eq_empty_or_nonempty t with (rfl | ht)

Result:
case mp.inl
α : Type u_1
β : Type u_2
s : Set α
f : α → β
⊢ SurjOn f s ∅ → ∃ s' ⊆ s, BijOn f s' ∅

case mp.inr
α : Type u_1
β : Type u_2
s : Set α
t : Set β
f : α → β
ht : t.Nonempty
⊢ SurjOn f s t → ∃ s' ⊆ s, BijOn f s' t
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Basic.lean
theorem le_of_sub_le_sub_right : ∀ {n m k : Nat}, k ≤ m → n - k ≤ m - k → n ≤ m
  | 0, _, _, _, _ => Nat.zero_le ..
  | _+1, _, 0, _, h₁ => h₁
  | _+1, _+1, _+1, h₀, h₁ => by
    simp only [Nat.succ_sub_succ] at h₁
    exact succ_le_succ <| Nat.le_of_sub_le_sub_right (le_of_succ_le_succ h₀) h₁

Proof state:
n✝² n✝¹ n✝ : Nat
h₀ : n✝ + 1 ≤ n✝¹ + 1
h₁ : n✝² + 1 - (n✝ + 1) ≤ n✝¹ + 1 - (n✝ + 1)
⊢ n✝² + 1 ≤ n✝¹ + 1

Tactic:
simp only [Nat.succ_sub_succ] at h₁

Result:
n✝² n✝¹ n✝ : Nat
h₀ : n✝ + 1 ≤ n✝¹ + 1
h₁ : n✝² - n✝ ≤ n✝¹ - n✝
⊢ n✝² + 1 ≤ n✝¹ + 1

Proof state:
n✝² n✝¹ n✝ : Nat
h₀ : n✝ + 1 ≤ n✝¹ + 1
h₁ : n✝² - n✝ ≤ n✝¹ - n✝
⊢ n✝² + 1 ≤ n✝¹ + 1

Tactic:
exact succ_le_succ <| Nat.le_of_sub_le_sub_right (le_of_succ_le_succ h₀) h₁

Result:
no goals
-- Mathlib/RingTheory/IntegralClosure/IsIntegral/Basic.lean
theorem RingHom.isIntegralElem_map {x : R} : f.IsIntegralElem (f x) :=
  ⟨X - C x, monic_X_sub_C _, by simp⟩

Proof state:
R : Type u_1
S : Type u_2
inst✝¹ : CommRing R
inst✝ : Ring S
f : R →+* S
x : R
⊢ eval₂ f (f x) (X - C x) = 0

Tactic:
simp

Result:
no goals
-- Mathlib/Topology/Maps/Proper/UniversallyClosed.lean
theorem isProperMap_iff_universally_closed {X : Type u} {Y : Type v} [TopologicalSpace X]
    [TopologicalSpace Y] {f : X → Y} :
    IsProperMap f ↔ Continuous f ∧ ∀ (Z : Type u) [TopologicalSpace Z],
      IsClosedMap (Prod.map f id : X × Z → Y × Z)

Proof state:
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
⊢ IsProperMap f ↔ Continuous f ∧ ∀ (Z : Type u) [inst : TopologicalSpace Z], IsClosedMap (Prod.map f id)

Tactic:
constructor <;> intro H

Result:
case mp
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
H : IsProperMap f
⊢ Continuous f ∧ ∀ (Z : Type u) [inst : TopologicalSpace Z], IsClosedMap (Prod.map f id)

case mpr
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
H : Continuous f ∧ ∀ (Z : Type u) [inst : TopologicalSpace Z], IsClosedMap (Prod.map f id)
⊢ IsProperMap f

Proof state:
case mpr
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
H : Continuous f ∧ ∀ (Z : Type u) [inst : TopologicalSpace Z], IsClosedMap (Prod.map f id)
⊢ Continuous f ∧ IsClosedMap (Prod.map f id)

Tactic:
exact ⟨H.1, H.2 _⟩

Result:
no goals

Proof state:
case mpr
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
H : Continuous f ∧ ∀ (Z : Type u) [inst : TopologicalSpace Z], IsClosedMap (Prod.map f id)
⊢ IsProperMap f

Tactic:
rw [isProperMap_iff_isClosedMap_ultrafilter]

Result:
case mpr
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
H : Continuous f ∧ ∀ (Z : Type u) [inst : TopologicalSpace Z], IsClosedMap (Prod.map f id)
⊢ Continuous f ∧ IsClosedMap (Prod.map f id)

Proof state:
case mp
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
H : IsProperMap f
⊢ Continuous f ∧ ∀ (Z : Type u) [inst : TopologicalSpace Z], IsClosedMap (Prod.map f id)

Tactic:
exact ⟨H.continuous, fun Z ↦ H.universally_closed _⟩

Result:
no goals
-- Mathlib/MeasureTheory/Integral/Bochner.lean
theorem integral_neg (f : α → G) : ∫ a, -f a ∂μ = -∫ a, f a ∂μ

Proof state:
case pos
α : Type u_1
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
f : α → G
hG : CompleteSpace G
⊢ ∫ (a : α), -f a ∂μ = -∫ (a : α), f a ∂μ

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

Result:
case pos
α : Type u_1
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
f : α → G
hG : CompleteSpace G
⊢ (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) =
    -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
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
f : α → G
⊢ ∫ (a : α), -f a ∂μ = -∫ (a : α), f a ∂μ

Tactic:
by_cases hG : CompleteSpace G

Result:
case pos
α : Type u_1
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
f : α → G
hG : CompleteSpace G
⊢ ∫ (a : α), -f a ∂μ = -∫ (a : α), f a ∂μ

case neg
α : Type u_1
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
f : α → G
hG : ¬CompleteSpace G
⊢ ∫ (a : α), -f a ∂μ = -∫ (a : α), f a ∂μ

Proof state:
case neg
α : Type u_1
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
f : α → G
hG : ¬CompleteSpace G
⊢ ∫ (a : α), -f a ∂μ = -∫ (a : α), f a ∂μ

Tactic:
simp [integral, hG]

Result:
no goals

Proof state:
case pos
α : Type u_1
G : Type u_5
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
f : α → G
hG : CompleteSpace G
⊢ (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) =
    -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_neg (dominatedFinMeasAdditive_weightedSMul μ) f

Result:
no goals