harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/MeasureTheory/Measure/Map.lean
lemma map_apply₀ {f : α → β} (hf : AEMeasurable f μ) {s : Set β}
    (hs : NullMeasurableSet s (map f μ)) : μ.map f s = μ (f ⁻¹' s)

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
f : α → β
hf : AEMeasurable f μ
s : Set β
hs : NullMeasurableSet s ((liftLinear (OuterMeasure.map (AEMeasurable.mk f hf)) ⋯) μ)
⊢ ((liftLinear (OuterMeasure.map (AEMeasurable.mk f hf)) ⋯) μ) s = μ (f ⁻¹' s)

Tactic:
rw [liftLinear_apply₀ _ hs, measure_congr (hf.ae_eq_mk.preimage s)]

Result:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
f : α → β
hf : AEMeasurable f μ
s : Set β
hs : NullMeasurableSet s ((liftLinear (OuterMeasure.map (AEMeasurable.mk f hf)) ⋯) μ)
⊢ ((OuterMeasure.map (AEMeasurable.mk f hf)) μ.toOuterMeasure) s = μ (AEMeasurable.mk f hf ⁻¹' s)

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
f : α → β
hf : AEMeasurable f μ
s : Set β
hs : NullMeasurableSet s ((liftLinear (OuterMeasure.map (AEMeasurable.mk f hf)) ⋯) μ)
⊢ ((OuterMeasure.map (AEMeasurable.mk f hf)) μ.toOuterMeasure) s = μ (AEMeasurable.mk f hf ⁻¹' s)

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
f : α → β
hf : AEMeasurable f μ
s : Set β
hs : NullMeasurableSet s (map f μ)
⊢ (map f μ) s = μ (f ⁻¹' s)

Tactic:
rw [map, dif_pos hf, mapₗ, dif_pos hf.measurable_mk] at hs ⊢

Result:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
f : α → β
hf : AEMeasurable f μ
s : Set β
hs : NullMeasurableSet s ((liftLinear (OuterMeasure.map (AEMeasurable.mk f hf)) ⋯) μ)
⊢ ((liftLinear (OuterMeasure.map (AEMeasurable.mk f hf)) ⋯) μ) s = μ (f ⁻¹' s)
-- Mathlib/NumberTheory/NumberField/CanonicalEmbedding/Basic.lean
theorem iUnion_negAt_plusPart_ae :
    ⋃ s, negAt s '' (plusPart A) =ᵐ[volume] A

Proof state:
K : Type u_1
inst✝¹ : Field K
A : Set (mixedSpace K)
hA : ∀ (x : mixedSpace K), x ∈ A ↔ (fun w => |x.1 w|, x.2) ∈ A
inst✝ : NumberField K
⊢ volume (A ∩ ⋃ w, {x | x.1 w = 0}) = 0

Tactic:
exact measure_mono_null Set.inter_subset_right
  (measure_iUnion_null_iff.mpr fun _ ↦ volume_eq_zero _)

Result:
no goals

Proof state:
K : Type u_1
inst✝¹ : Field K
A : Set (mixedSpace K)
hA : ∀ (x : mixedSpace K), x ∈ A ↔ (fun w => |x.1 w|, x.2) ∈ A
inst✝ : NumberField K
⊢ ⋃ s, ⇑(negAt s) '' plusPart A =ᶠ[ae volume] A

Tactic:
nth_rewrite 2 [← iUnion_negAt_plusPart_union A hA]

Result:
K : Type u_1
inst✝¹ : Field K
A : Set (mixedSpace K)
hA : ∀ (x : mixedSpace K), x ∈ A ↔ (fun w => |x.1 w|, x.2) ∈ A
inst✝ : NumberField K
⊢ ⋃ s, ⇑(negAt s) '' plusPart A =ᶠ[ae volume] (⋃ s, ⇑(negAt s) '' plusPart A) ∪ A ∩ ⋃ w, {x | x.1 w = 0}

Proof state:
K : Type u_1
inst✝¹ : Field K
A : Set (mixedSpace K)
hA : ∀ (x : mixedSpace K), x ∈ A ↔ (fun w => |x.1 w|, x.2) ∈ A
inst✝ : NumberField K
⊢ ⋃ s, ⇑(negAt s) '' plusPart A =ᶠ[ae volume] (⋃ s, ⇑(negAt s) '' plusPart A) ∪ A ∩ ⋃ w, {x | x.1 w = 0}

Tactic:
refine (MeasureTheory.union_ae_eq_left_of_ae_eq_empty (ae_eq_empty.mpr ?_)).symm

Result:
K : Type u_1
inst✝¹ : Field K
A : Set (mixedSpace K)
hA : ∀ (x : mixedSpace K), x ∈ A ↔ (fun w => |x.1 w|, x.2) ∈ A
inst✝ : NumberField K
⊢ volume (A ∩ ⋃ w, {x | x.1 w = 0}) = 0
-- Mathlib/LinearAlgebra/LinearPMap.lean
theorem mem_graph (f : E →ₗ.[R] F) (x : domain f) : ((x : E), f x) ∈ f.graph

Proof state:
R : Type u_1
inst✝⁴ : Ring R
E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_3
inst✝¹ : AddCommGroup F
inst✝ : Module R F
f : E →ₗ.[R] F
x : ↥f.domain
⊢ (↑x, ↑f x) ∈ f.graph

Tactic:
simp

Result:
no goals
-- Mathlib/Geometry/Manifold/MFDeriv/SpecificFunctions.lean
theorem tangentMap_id : tangentMap I I (id : M → M) = id

Proof state:
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
H : Type u_3
inst✝² : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
⊢ tangentMap I I id = id

Tactic:
ext1 ⟨x, v⟩

Result:
case h.mk
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
H : Type u_3
inst✝² : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
x : M
v : TangentSpace I x
⊢ tangentMap I I id { proj := x, snd := v } = id { proj := x, snd := v }

Proof state:
case h.mk
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
H : Type u_3
inst✝² : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝¹ : TopologicalSpace M
inst✝ : ChartedSpace H M
x : M
v : TangentSpace I x
⊢ tangentMap I I id { proj := x, snd := v } = id { proj := x, snd := v }

Tactic:
simp [tangentMap]

Result:
no goals
-- Mathlib/Topology/NoetherianSpace.lean
theorem NoetherianSpace.isCompact [NoetherianSpace α] (s : Set α) : IsCompact s

Proof state:
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : NoetherianSpace α
s : Set α
ι✝ : Type u_1
U : ι✝ → Set α
hUo : ∀ (i : ι✝), IsOpen (U i)
hs : s ⊆ ⋃ i, U i
⊢ ∃ t, s ⊆ ⋃ i ∈ t, U i

Tactic:
rcases ((noetherianSpace_iff_opens α).mp ‹_› ⟨⋃ i, U i, isOpen_iUnion hUo⟩).elim_finite_subcover U
  hUo Set.Subset.rfl with ⟨t, ht⟩

Result:
case intro
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : NoetherianSpace α
s : Set α
ι✝ : Type u_1
U : ι✝ → Set α
hUo : ∀ (i : ι✝), IsOpen (U i)
hs : s ⊆ ⋃ i, U i
t : Finset ι✝
ht : ↑{ carrier := ⋃ i, U i, is_open' := ⋯ } ⊆ ⋃ i ∈ t, U i
⊢ ∃ t, s ⊆ ⋃ i ∈ t, U i

Proof state:
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : NoetherianSpace α
s : Set α
⊢ IsCompact s

Tactic:
refine isCompact_iff_finite_subcover.2 fun U hUo hs => ?_

Result:
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : NoetherianSpace α
s : Set α
ι✝ : Type u_1
U : ι✝ → Set α
hUo : ∀ (i : ι✝), IsOpen (U i)
hs : s ⊆ ⋃ i, U i
⊢ ∃ t, s ⊆ ⋃ i ∈ t, U i

Proof state:
case intro
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : NoetherianSpace α
s : Set α
ι✝ : Type u_1
U : ι✝ → Set α
hUo : ∀ (i : ι✝), IsOpen (U i)
hs : s ⊆ ⋃ i, U i
t : Finset ι✝
ht : ↑{ carrier := ⋃ i, U i, is_open' := ⋯ } ⊆ ⋃ i ∈ t, U i
⊢ ∃ t, s ⊆ ⋃ i ∈ t, U i

Tactic:
exact ⟨t, hs.trans ht⟩

Result:
no goals
-- Mathlib/Analysis/Calculus/LHopital.lean
theorem lhopital_zero_atBot_on_Iio (hdf : DifferentiableOn ℝ f (Iio a))
    (hg' : ∀ x ∈ Iio a, (deriv g) x ≠ 0) (hfbot : Tendsto f atBot (𝓝 0))
    (hgbot : Tendsto g atBot (𝓝 0)) (hdiv : Tendsto (fun x => (deriv f) x / (deriv g) x) atBot l) :
    Tendsto (fun x => f x / g x) atBot l

Proof state:
a : ℝ
l : Filter ℝ
f g : ℝ → ℝ
hdf : DifferentiableOn ℝ f (Iio a)
hg' : ∀ x ∈ Iio a, deriv g x ≠ 0
hfbot : Tendsto f atBot (𝓝 0)
hgbot : Tendsto g atBot (𝓝 0)
hdiv : Tendsto (fun x => deriv f x / deriv g x) atBot l
⊢ Tendsto (fun x => f x / g x) atBot l

Tactic:
have hdf : ∀ x ∈ Iio a, DifferentiableAt ℝ f x := fun x hx =>
  (hdf x hx).differentiableAt (Iio_mem_nhds hx)

Result:
a : ℝ
l : Filter ℝ
f g : ℝ → ℝ
hdf✝ : DifferentiableOn ℝ f (Iio a)
hg' : ∀ x ∈ Iio a, deriv g x ≠ 0
hfbot : Tendsto f atBot (𝓝 0)
hgbot : Tendsto g atBot (𝓝 0)
hdiv : Tendsto (fun x => deriv f x / deriv g x) atBot l
hdf : ∀ x ∈ Iio a, DifferentiableAt ℝ f x
⊢ Tendsto (fun x => f x / g x) atBot l

Proof state:
a : ℝ
l : Filter ℝ
f g : ℝ → ℝ
hdf✝ : DifferentiableOn ℝ f (Iio a)
hg' : ∀ x ∈ Iio a, deriv g x ≠ 0
hfbot : Tendsto f atBot (𝓝 0)
hgbot : Tendsto g atBot (𝓝 0)
hdiv : Tendsto (fun x => deriv f x / deriv g x) atBot l
hdf : ∀ x ∈ Iio a, DifferentiableAt ℝ f x
⊢ Tendsto (fun x => f x / g x) atBot l

Tactic:
have hdg : ∀ x ∈ Iio a, DifferentiableAt ℝ g x := fun x hx =>
  by_contradiction fun h => hg' x hx (deriv_zero_of_not_differentiableAt h)

Result:
a : ℝ
l : Filter ℝ
f g : ℝ → ℝ
hdf✝ : DifferentiableOn ℝ f (Iio a)
hg' : ∀ x ∈ Iio a, deriv g x ≠ 0
hfbot : Tendsto f atBot (𝓝 0)
hgbot : Tendsto g atBot (𝓝 0)
hdiv : Tendsto (fun x => deriv f x / deriv g x) atBot l
hdf : ∀ x ∈ Iio a, DifferentiableAt ℝ f x
hdg : ∀ x ∈ Iio a, DifferentiableAt ℝ g x
⊢ Tendsto (fun x => f x / g x) atBot l

Proof state:
a : ℝ
l : Filter ℝ
f g : ℝ → ℝ
hdf✝ : DifferentiableOn ℝ f (Iio a)
hg' : ∀ x ∈ Iio a, deriv g x ≠ 0
hfbot : Tendsto f atBot (𝓝 0)
hgbot : Tendsto g atBot (𝓝 0)
hdiv : Tendsto (fun x => deriv f x / deriv g x) atBot l
hdf : ∀ x ∈ Iio a, DifferentiableAt ℝ f x
hdg : ∀ x ∈ Iio a, DifferentiableAt ℝ g x
⊢ Tendsto (fun x => f x / g x) atBot l

Tactic:
exact HasDerivAt.lhopital_zero_atBot_on_Iio (fun x hx => (hdf x hx).hasDerivAt)
  (fun x hx => (hdg x hx).hasDerivAt) hg' hfbot hgbot hdiv

Result:
no goals
-- Mathlib/MeasureTheory/Integral/Average.lean
theorem measure_le_setLaverage_pos (hμ : μ s ≠ 0) (hμ₁ : μ s ≠ ∞)
    (hf : AEMeasurable f (μ.restrict s)) : 0 < μ {x ∈ s | f x ≤ ⨍⁻ a in s, f a ∂μ}

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ≥0∞
hμ : μ s ≠ 0
hμ₁ : μ s ≠ ⊤
hf : AEMeasurable f (μ.restrict s)
⊢ 0 < μ {x | x ∈ s ∧ f x ≤ ⨍⁻ (a : α) in s, f a ∂μ}

Tactic:
obtain h | h := eq_or_ne (∫⁻ a in s, f a ∂μ) ∞

Result:
case inl
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ≥0∞
hμ : μ s ≠ 0
hμ₁ : μ s ≠ ⊤
hf : AEMeasurable f (μ.restrict s)
h : ∫⁻ (a : α) in s, f a ∂μ = ⊤
⊢ 0 < μ {x | x ∈ s ∧ f x ≤ ⨍⁻ (a : α) in s, f a ∂μ}

case inr
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ≥0∞
hμ : μ s ≠ 0
hμ₁ : μ s ≠ ⊤
hf : AEMeasurable f (μ.restrict s)
h : ∫⁻ (a : α) in s, f a ∂μ ≠ ⊤
⊢ 0 < μ {x | x ∈ s ∧ f x ≤ ⨍⁻ (a : α) in s, f a ∂μ}
-- Mathlib/MeasureTheory/Measure/MeasureSpace.lean
theorem sum_add_sum_compl (s : Set ι) (μ : ι → Measure α) :
    ((sum fun i : s => μ i) + sum fun i : ↥sᶜ => μ i) = sum μ

Proof state:
α : Type u_1
ι : Type u_5
m0 : MeasurableSpace α
s : Set ι
μ : ι → Measure α
⊢ ((sum fun i => μ ↑i) + sum fun i => μ ↑i) = sum μ

Tactic:
ext1 t ht

Result:
case h
α : Type u_1
ι : Type u_5
m0 : MeasurableSpace α
s : Set ι
μ : ι → Measure α
t : Set α
ht : MeasurableSet t
⊢ ((sum fun i => μ ↑i) + sum fun i => μ ↑i) t = (sum μ) t

Proof state:
case h
α : Type u_1
ι : Type u_5
m0 : MeasurableSpace α
s : Set ι
μ : ι → Measure α
t : Set α
ht : MeasurableSet t
⊢ ∑' (i : ↑s), (μ ↑i) t + ∑' (i : ↑sᶜ), (μ ↑i) t = ∑' (i : ι), (μ i) t

Tactic:
exact tsum_add_tsum_compl (f := fun i => μ i t) ENNReal.summable ENNReal.summable

Result:
no goals

Proof state:
case h
α : Type u_1
ι : Type u_5
m0 : MeasurableSpace α
s : Set ι
μ : ι → Measure α
t : Set α
ht : MeasurableSet t
⊢ ((sum fun i => μ ↑i) + sum fun i => μ ↑i) t = (sum μ) t

Tactic:
simp only [add_apply, sum_apply _ ht]

Result:
case h
α : Type u_1
ι : Type u_5
m0 : MeasurableSpace α
s : Set ι
μ : ι → Measure α
t : Set α
ht : MeasurableSet t
⊢ ∑' (i : ↑s), (μ ↑i) t + ∑' (i : ↑sᶜ), (μ ↑i) t = ∑' (i : ι), (μ i) t
-- Mathlib/LinearAlgebra/AffineSpace/FiniteDimensional.lean
theorem collinear_empty : Collinear k (∅ : Set P)

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
⊢ Collinear k ∅

Tactic:
rw [collinear_iff_rank_le_one, vectorSpan_empty]

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
⊢ Module.rank k ↥⊥ ≤ 1

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
⊢ Module.rank k ↥⊥ ≤ 1

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Fintype/Prod.lean
theorem toFinset_prod (s : Set α) (t : Set β) [Fintype s] [Fintype t] [Fintype (s ×ˢ t)] :
    (s ×ˢ t).toFinset = s.toFinset ×ˢ t.toFinset

Proof state:
α : Type u_1
β : Type u_2
s : Set α
t : Set β
inst✝² : Fintype ↑s
inst✝¹ : Fintype ↑t
inst✝ : Fintype ↑(s ×ˢ t)
⊢ (s ×ˢ t).toFinset = s.toFinset ×ˢ t.toFinset

Tactic:
ext

Result:
case h
α : Type u_1
β : Type u_2
s : Set α
t : Set β
inst✝² : Fintype ↑s
inst✝¹ : Fintype ↑t
inst✝ : Fintype ↑(s ×ˢ t)
a✝ : α × β
⊢ a✝ ∈ (s ×ˢ t).toFinset ↔ a✝ ∈ s.toFinset ×ˢ t.toFinset

Proof state:
case h
α : Type u_1
β : Type u_2
s : Set α
t : Set β
inst✝² : Fintype ↑s
inst✝¹ : Fintype ↑t
inst✝ : Fintype ↑(s ×ˢ t)
a✝ : α × β
⊢ a✝ ∈ (s ×ˢ t).toFinset ↔ a✝ ∈ s.toFinset ×ˢ t.toFinset

Tactic:
simp

Result:
no goals
-- Mathlib/LinearAlgebra/BilinearForm/Properties.lean
theorem compLeft_injective (B : BilinForm R₁ M₁) (b : B.Nondegenerate) :
    Function.Injective B.compLeft := fun φ ψ h => by
  ext w
  refine eq_of_sub_eq_zero (b _ ?_)
  intro v
  rw [sub_left, ← compLeft_apply, ← compLeft_apply, ← h, sub_self]

Proof state:
case h
R₁ : Type u_3
M₁ : Type u_4
inst✝² : CommRing R₁
inst✝¹ : AddCommGroup M₁
inst✝ : Module R₁ M₁
B : BilinForm R₁ M₁
b : B.Nondegenerate
φ ψ : M₁ →ₗ[R₁] M₁
h : B.compLeft φ = B.compLeft ψ
w v : M₁
⊢ (B (φ w - ψ w)) v = 0

Tactic:
rw [sub_left, ← compLeft_apply, ← compLeft_apply, ← h, sub_self]

Result:
no goals

Proof state:
case h
R₁ : Type u_3
M₁ : Type u_4
inst✝² : CommRing R₁
inst✝¹ : AddCommGroup M₁
inst✝ : Module R₁ M₁
B : BilinForm R₁ M₁
b : B.Nondegenerate
φ ψ : M₁ →ₗ[R₁] M₁
h : B.compLeft φ = B.compLeft ψ
w : M₁
⊢ ∀ (n : M₁), (B (φ w - ψ w)) n = 0

Tactic:
intro v

Result:
case h
R₁ : Type u_3
M₁ : Type u_4
inst✝² : CommRing R₁
inst✝¹ : AddCommGroup M₁
inst✝ : Module R₁ M₁
B : BilinForm R₁ M₁
b : B.Nondegenerate
φ ψ : M₁ →ₗ[R₁] M₁
h : B.compLeft φ = B.compLeft ψ
w v : M₁
⊢ (B (φ w - ψ w)) v = 0

Proof state:
case h
R₁ : Type u_3
M₁ : Type u_4
inst✝² : CommRing R₁
inst✝¹ : AddCommGroup M₁
inst✝ : Module R₁ M₁
B : BilinForm R₁ M₁
b : B.Nondegenerate
φ ψ : M₁ →ₗ[R₁] M₁
h : B.compLeft φ = B.compLeft ψ
w : M₁
⊢ φ w = ψ w

Tactic:
refine eq_of_sub_eq_zero (b _ ?_)

Result:
case h
R₁ : Type u_3
M₁ : Type u_4
inst✝² : CommRing R₁
inst✝¹ : AddCommGroup M₁
inst✝ : Module R₁ M₁
B : BilinForm R₁ M₁
b : B.Nondegenerate
φ ψ : M₁ →ₗ[R₁] M₁
h : B.compLeft φ = B.compLeft ψ
w : M₁
⊢ ∀ (n : M₁), (B (φ w - ψ w)) n = 0

Proof state:
R₁ : Type u_3
M₁ : Type u_4
inst✝² : CommRing R₁
inst✝¹ : AddCommGroup M₁
inst✝ : Module R₁ M₁
B : BilinForm R₁ M₁
b : B.Nondegenerate
φ ψ : M₁ →ₗ[R₁] M₁
h : B.compLeft φ = B.compLeft ψ
⊢ φ = ψ

Tactic:
ext w

Result:
case h
R₁ : Type u_3
M₁ : Type u_4
inst✝² : CommRing R₁
inst✝¹ : AddCommGroup M₁
inst✝ : Module R₁ M₁
B : BilinForm R₁ M₁
b : B.Nondegenerate
φ ψ : M₁ →ₗ[R₁] M₁
h : B.compLeft φ = B.compLeft ψ
w : M₁
⊢ φ w = ψ w
-- Mathlib/RingTheory/MvPolynomial/MonomialOrder.lean
theorem degree_sub_le {f g : MvPolynomial σ R} :
    m.toSyn (m.degree (f - g)) ≤ m.toSyn (m.degree f) ⊔ m.toSyn (m.degree g)

Proof state:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
f g : MvPolynomial σ R
⊢ m.toSyn (m.degree (f - g)) ≤ m.toSyn (m.degree f) ⊔ m.toSyn (m.degree g)

Tactic:
rw [sub_eq_add_neg]

Result:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
f g : MvPolynomial σ R
⊢ m.toSyn (m.degree (f + -g)) ≤ m.toSyn (m.degree f) ⊔ m.toSyn (m.degree g)

Proof state:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
f g : MvPolynomial σ R
⊢ m.toSyn (m.degree f) ⊔ m.toSyn (m.degree (-g)) = m.toSyn (m.degree f) ⊔ m.toSyn (m.degree g)

Tactic:
rw [degree_neg]

Result:
no goals

Proof state:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
f g : MvPolynomial σ R
⊢ m.toSyn (m.degree (f + -g)) ≤ m.toSyn (m.degree f) ⊔ m.toSyn (m.degree g)

Tactic:
apply le_of_le_of_eq m.degree_add_le

Result:
σ : Type u_1
m : MonomialOrder σ
R : Type u_2
inst✝ : CommRing R
f g : MvPolynomial σ R
⊢ m.toSyn (m.degree f) ⊔ m.toSyn (m.degree (-g)) = m.toSyn (m.degree f) ⊔ m.toSyn (m.degree g)
-- Mathlib/GroupTheory/Perm/Cycle/Factors.lean
theorem IsCycle.forall_commute_iff [DecidableEq α] [Fintype α] (g z : Perm α) :
    (∀ c ∈ g.cycleFactorsFinset, Commute z c) ↔
      ∀ c ∈ g.cycleFactorsFinset,
      ∃ (hc : ∀ x : α, x ∈ c.support ↔ z x ∈ c.support),
        ofSubtype (subtypePerm z hc) ∈ Subgroup.zpowers c

Proof state:
case h.h
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z c : Perm α
hc : c ∈ g.cycleFactorsFinset
⊢ Commute z c ↔ ∃ (hc : ∀ (x : α), x ∈ c.support ↔ z x ∈ c.support), ofSubtype (z.subtypePerm hc) ∈ Subgroup.zpowers c

Tactic:
exact IsCycle.commute_iff (mem_cycleFactorsFinset_iff.mp hc).1

Result:
no goals

Proof state:
case h.h
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z c : Perm α
⊢ c ∈ g.cycleFactorsFinset →
    (Commute z c ↔
      ∃ (hc : ∀ (x : α), x ∈ c.support ↔ z x ∈ c.support), ofSubtype (z.subtypePerm hc) ∈ Subgroup.zpowers c)

Tactic:
intro hc

Result:
case h.h
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z c : Perm α
hc : c ∈ g.cycleFactorsFinset
⊢ Commute z c ↔ ∃ (hc : ∀ (x : α), x ∈ c.support ↔ z x ∈ c.support), ofSubtype (z.subtypePerm hc) ∈ Subgroup.zpowers c

Proof state:
case h
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z : Perm α
⊢ ∀ (a : Perm α),
    a ∈ g.cycleFactorsFinset → Commute z a ↔
      a ∈ g.cycleFactorsFinset →
        ∃ (hc : ∀ (x : α), x ∈ a.support ↔ z x ∈ a.support), ofSubtype (z.subtypePerm hc) ∈ Subgroup.zpowers a

Tactic:
intro c

Result:
case h
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z c : Perm α
⊢ c ∈ g.cycleFactorsFinset → Commute z c ↔
    c ∈ g.cycleFactorsFinset →
      ∃ (hc : ∀ (x : α), x ∈ c.support ↔ z x ∈ c.support), ofSubtype (z.subtypePerm hc) ∈ Subgroup.zpowers c

Proof state:
case h
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z c : Perm α
⊢ c ∈ g.cycleFactorsFinset → Commute z c ↔
    c ∈ g.cycleFactorsFinset →
      ∃ (hc : ∀ (x : α), x ∈ c.support ↔ z x ∈ c.support), ofSubtype (z.subtypePerm hc) ∈ Subgroup.zpowers c

Tactic:
apply imp_congr_right

Result:
case h.h
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z c : Perm α
⊢ c ∈ g.cycleFactorsFinset →
    (Commute z c ↔
      ∃ (hc : ∀ (x : α), x ∈ c.support ↔ z x ∈ c.support), ofSubtype (z.subtypePerm hc) ∈ Subgroup.zpowers c)

Proof state:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z : Perm α
⊢ (∀ c ∈ g.cycleFactorsFinset, Commute z c) ↔
    ∀ c ∈ g.cycleFactorsFinset,
      ∃ (hc : ∀ (x : α), x ∈ c.support ↔ z x ∈ c.support), ofSubtype (z.subtypePerm hc) ∈ Subgroup.zpowers c

Tactic:
apply forall_congr'

Result:
case h
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
g z : Perm α
⊢ ∀ (a : Perm α),
    a ∈ g.cycleFactorsFinset → Commute z a ↔
      a ∈ g.cycleFactorsFinset →
        ∃ (hc : ∀ (x : α), x ∈ a.support ↔ z x ∈ a.support), ofSubtype (z.subtypePerm hc) ∈ Subgroup.zpowers a
-- Mathlib/MeasureTheory/Integral/Lebesgue.lean
theorem lintegral_union {f : α → ℝ≥0∞} {A B : Set α} (hB : MeasurableSet B) (hAB : Disjoint A B) :
    ∫⁻ a in A ∪ B, f a ∂μ = ∫⁻ a in A, f a ∂μ + ∫⁻ a in B, f a ∂μ

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
A B : Set α
hB : MeasurableSet B
hAB : Disjoint A B
⊢ ∫⁻ (a : α) in A ∪ B, f a ∂μ = ∫⁻ (a : α) in A, f a ∂μ + ∫⁻ (a : α) in B, f a ∂μ

Tactic:
rw [restrict_union hAB hB, lintegral_add_measure]

Result:
no goals
-- Mathlib/Order/LiminfLimsup.lean
lemma isBoundedUnder_iff_eventually_bddAbove :
    f.IsBoundedUnder (· ≤ ·) u ↔ ∃ s, BddAbove (u '' s) ∧ ∀ᶠ x in f, x ∈ s

Proof state:
case mp
α : Type u_1
β : Type u_2
inst✝ : Preorder α
f : Filter β
u : β → α
⊢ IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f u → ∃ s, BddAbove (u '' s) ∧ ∀ᶠ (x : β) in f, x ∈ s

Tactic:
rintro ⟨b, hb⟩

Result:
case mp.intro
α : Type u_1
β : Type u_2
inst✝ : Preorder α
f : Filter β
u : β → α
b : α
hb : ∀ᶠ (x : α) in map u f, (fun x1 x2 => x1 ≤ x2) x b
⊢ ∃ s, BddAbove (u '' s) ∧ ∀ᶠ (x : β) in f, x ∈ s

Proof state:
case mpr
α : Type u_1
β : Type u_2
inst✝ : Preorder α
f : Filter β
u : β → α
⊢ (∃ s, BddAbove (u '' s) ∧ ∀ᶠ (x : β) in f, x ∈ s) → IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f u

Tactic:
rintro ⟨s, ⟨b, hb⟩, hs⟩

Result:
case mpr.intro.intro.intro
α : Type u_1
β : Type u_2
inst✝ : Preorder α
f : Filter β
u : β → α
s : Set β
hs : ∀ᶠ (x : β) in f, x ∈ s
b : α
hb : b ∈ upperBounds (u '' s)
⊢ IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f u

Proof state:
case mpr.intro.intro.intro
α : Type u_1
β : Type u_2
inst✝ : Preorder α
f : Filter β
u : β → α
s : Set β
hs : ∀ᶠ (x : β) in f, x ∈ s
b : α
hb : b ∈ upperBounds (u '' s)
⊢ IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f u

Tactic:
exact ⟨b, hs.mono <| by simpa [upperBounds] using hb⟩

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝ : Preorder α
f : Filter β
u : β → α
⊢ IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f u ↔ ∃ s, BddAbove (u '' s) ∧ ∀ᶠ (x : β) in f, x ∈ s

Tactic:
constructor

Result:
case mp
α : Type u_1
β : Type u_2
inst✝ : Preorder α
f : Filter β
u : β → α
⊢ IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f u → ∃ s, BddAbove (u '' s) ∧ ∀ᶠ (x : β) in f, x ∈ s

case mpr
α : Type u_1
β : Type u_2
inst✝ : Preorder α
f : Filter β
u : β → α
⊢ (∃ s, BddAbove (u '' s) ∧ ∀ᶠ (x : β) in f, x ∈ s) → IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f u

Proof state:
α : Type u_1
β : Type u_2
inst✝ : Preorder α
f : Filter β
u : β → α
b : α
hb : ∀ᶠ (x : α) in map u f, (fun x1 x2 => x1 ≤ x2) x b
⊢ b ∈ upperBounds (u '' {a | u a ≤ b})

Tactic:
rintro _ ⟨a, ha, rfl⟩

Result:
case intro.intro
α : Type u_1
β : Type u_2
inst✝ : Preorder α
f : Filter β
u : β → α
b : α
hb : ∀ᶠ (x : α) in map u f, (fun x1 x2 => x1 ≤ x2) x b
a : β
ha : a ∈ {a | u a ≤ b}
⊢ u a ≤ b

Proof state:
case intro.intro
α : Type u_1
β : Type u_2
inst✝ : Preorder α
f : Filter β
u : β → α
b : α
hb : ∀ᶠ (x : α) in map u f, (fun x1 x2 => x1 ≤ x2) x b
a : β
ha : a ∈ {a | u a ≤ b}
⊢ u a ≤ b

Tactic:
exact ha

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝ : Preorder α
f : Filter β
u : β → α
s : Set β
hs : ∀ᶠ (x : β) in f, x ∈ s
b : α
hb : b ∈ upperBounds (u '' s)
⊢ ∀ x ∈ s, u x ∈ {x | (fun x => (fun x1 x2 => x1 ≤ x2) x b) x}

Tactic:
simpa [upperBounds] using hb

Result:
no goals

Proof state:
case mp.intro
α : Type u_1
β : Type u_2
inst✝ : Preorder α
f : Filter β
u : β → α
b : α
hb : ∀ᶠ (x : α) in map u f, (fun x1 x2 => x1 ≤ x2) x b
⊢ ∃ s, BddAbove (u '' s) ∧ ∀ᶠ (x : β) in f, x ∈ s

Tactic:
exact ⟨{a | u a ≤ b}, ⟨b, by rintro _ ⟨a, ha, rfl⟩; exact ha⟩, hb⟩

Result:
no goals
-- Mathlib/Analysis/Calculus/IteratedDeriv/Lemmas.lean
theorem iteratedDeriv_const_mul {n : ℕ} {f : 𝕜 → 𝕜} (h : ContDiffAt 𝕜 n f x) (c : 𝕜) :
    iteratedDeriv n (fun z => c * f z) x = c * iteratedDeriv n f x

Proof state:
𝕜 : Type u_1
inst✝ : NontriviallyNormedField 𝕜
x : 𝕜
n : ℕ
f : 𝕜 → 𝕜
h : ContDiffAt 𝕜 (↑n) f x
c : 𝕜
⊢ iteratedDeriv n (fun z => c * f z) x = c * iteratedDeriv n f x

Tactic:
simpa only [iteratedDerivWithin_univ] using
  iteratedDerivWithin_const_mul (Set.mem_univ x) uniqueDiffOn_univ
    c (contDiffWithinAt_univ.mpr h)

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Basic.lean
theorem type_ne_zero_iff_nonempty [IsWellOrder α r] : type r ≠ 0 ↔ Nonempty α

Proof state:
α : Type u
r : α → α → Prop
inst✝ : IsWellOrder α r
⊢ type r ≠ 0 ↔ Nonempty α

Tactic:
simp

Result:
no goals