harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/CategoryTheory/Closed/Monoidal.lean
@[reassoc]
lemma curry_pre_app (f : B ⟶ A) {X Y : C} (g : A ⊗ Y ⟶ X) :
    curry g ≫ (pre f).app X = curry (f ▷ _ ≫ g) := uncurry_injective (by
  rw [uncurry_curry, uncurry_eq, MonoidalCategory.whiskerLeft_comp, assoc,
    id_tensor_pre_app_comp_ev, whisker_exchange_assoc, whiskerLeft_curry_ihom_ev_app])

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : MonoidalCategory C
A B : C
inst✝¹ : Closed A
inst✝ : Closed B
f : B ⟶ A
X Y : C
g : A ⊗ Y ⟶ X
⊢ uncurry (curry g ≫ (pre f).app X) = uncurry (curry (f ▷ Y ≫ g))

Tactic:
rw [uncurry_curry, uncurry_eq, MonoidalCategory.whiskerLeft_comp, assoc,
  id_tensor_pre_app_comp_ev, whisker_exchange_assoc, whiskerLeft_curry_ihom_ev_app]

Result:
no goals
-- Mathlib/CategoryTheory/Abelian/Exact.lean
theorem preservesEpimorphisms_of_map_exact : L.PreservesEpimorphisms where
  preserves f hf

Proof state:
A : Type u₁
B : Type u₂
inst✝⁴ : Category.{v₁, u₁} A
inst✝³ : Category.{v₂, u₂} B
inst✝² : Abelian A
inst✝¹ : Abelian B
L : A ⥤ B
inst✝ : L.PreservesZeroMorphisms
hL : ∀ (S : ShortComplex A), S.Exact → (S.map L).Exact
X✝ Y✝ : A
f : X✝ ⟶ Y✝
hf : Epi f
⊢ Epi (L.map f)

Tactic:
apply ((Abelian.tfae_epi (L.map f) (L.obj 0)).out 2 0).mp

Result:
A : Type u₁
B : Type u₂
inst✝⁴ : Category.{v₁, u₁} A
inst✝³ : Category.{v₂, u₂} B
inst✝² : Abelian A
inst✝¹ : Abelian B
L : A ⥤ B
inst✝ : L.PreservesZeroMorphisms
hL : ∀ (S : ShortComplex A), S.Exact → (S.map L).Exact
X✝ Y✝ : A
f : X✝ ⟶ Y✝
hf : Epi f
⊢ (ShortComplex.mk (L.map f) 0 ⋯).Exact

Proof state:
A : Type u₁
B : Type u₂
inst✝⁴ : Category.{v₁, u₁} A
inst✝³ : Category.{v₂, u₂} B
inst✝² : Abelian A
inst✝¹ : Abelian B
L : A ⥤ B
inst✝ : L.PreservesZeroMorphisms
hL : ∀ (S : ShortComplex A), S.Exact → (S.map L).Exact
X✝ Y✝ : A
f : X✝ ⟶ Y✝
hf : Epi f
⊢ (ShortComplex.mk (L.map f) 0 ⋯).Exact

Tactic:
refine ShortComplex.exact_of_iso ?_ (hL _ (((tfae_epi f 0).out 0 2).mp hf))

Result:
A : Type u₁
B : Type u₂
inst✝⁴ : Category.{v₁, u₁} A
inst✝³ : Category.{v₂, u₂} B
inst✝² : Abelian A
inst✝¹ : Abelian B
L : A ⥤ B
inst✝ : L.PreservesZeroMorphisms
hL : ∀ (S : ShortComplex A), S.Exact → (S.map L).Exact
X✝ Y✝ : A
f : X✝ ⟶ Y✝
hf : Epi f
⊢ (ShortComplex.mk f 0 ⋯).map L ≅ ShortComplex.mk (L.map f) 0 ⋯

Proof state:
A : Type u₁
B : Type u₂
inst✝⁴ : Category.{v₁, u₁} A
inst✝³ : Category.{v₂, u₂} B
inst✝² : Abelian A
inst✝¹ : Abelian B
L : A ⥤ B
inst✝ : L.PreservesZeroMorphisms
hL : ∀ (S : ShortComplex A), S.Exact → (S.map L).Exact
X✝ Y✝ : A
f : X✝ ⟶ Y✝
hf : Epi f
⊢ (ShortComplex.mk f 0 ⋯).map L ≅ ShortComplex.mk (L.map f) 0 ⋯

Tactic:
exact ShortComplex.isoMk (Iso.refl _) (Iso.refl _) (Iso.refl _)

Result:
no goals
-- Mathlib/Data/Nat/Factorial/Basic.lean
theorem descFactorial_self : ∀ n : ℕ, n.descFactorial n = n !
  | 0 => by rw [descFactorial_zero, factorial_zero]
  | succ n => by rw [succ_descFactorial_succ, descFactorial_self n, factorial_succ]

Proof state:
⊢ descFactorial 0 0 = 0!

Tactic:
rw [descFactorial_zero, factorial_zero]

Result:
no goals

Proof state:
n : ℕ
⊢ n.succ.descFactorial n.succ = n.succ !

Tactic:
rw [succ_descFactorial_succ, descFactorial_self n, factorial_succ]

Result:
no goals
-- Mathlib/Analysis/Normed/Lp/PiLp.lean
theorem edist_eq_of_L1 (x y : PiLp 1 β) : edist x y = ∑ i, edist (x i) (y i)

Proof state:
ι : Type u_2
β : ι → Type u_4
inst✝¹ : Fintype ι
inst✝ : (i : ι) → SeminormedAddCommGroup (β i)
x y : PiLp 1 β
⊢ edist x y = ∑ i : ι, edist (x i) (y i)

Tactic:
simp [PiLp.edist_eq_sum]

Result:
no goals
-- Mathlib/NumberTheory/EllipticDivisibilitySequence.lean
lemma map_preNormEDS (n : ℤ) : f (preNormEDS b c d n) = preNormEDS (f b) (f c) (f d) n

Proof state:
R : Type u
inst✝¹ : CommRing R
b c d : R
S : Type v
inst✝ : CommRing S
f : R →+* S
n : ℤ
⊢ f (preNormEDS b c d n) = preNormEDS (f b) (f c) (f d) n

Tactic:
rw [preNormEDS, map_mul, map_intCast, map_preNormEDS', preNormEDS]

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Projective.lean
lemma polynomialY_eq : W'.polynomialY =
    C 2 * X 1 * X 2 + C W'.a₁ * X 0 * X 2 + C W'.a₃ * X 2 ^ 2

Proof state:
R : Type r
inst✝ : CommRing R
W' : Projective R
⊢ W'.polynomialY = C 2 * X y * X z + C W'.a₁ * X x * X z + C W'.a₃ * X z ^ 2

Tactic:
rw [polynomialY, polynomial]

Result:
R : Type r
inst✝ : CommRing R
W' : Projective R
⊢ (pderiv y)
      (X y ^ 2 * X z + C W'.a₁ * X x * X y * X z + C W'.a₃ * X y * X z ^ 2 -
        (X x ^ 3 + C W'.a₂ * X x ^ 2 * X z + C W'.a₄ * X x * X z ^ 2 + C W'.a₆ * X z ^ 3)) =
    C 2 * X y * X z + C W'.a₁ * X x * X z + C W'.a₃ * X z ^ 2

Proof state:
R : Type r
inst✝ : CommRing R
W' : Projective R
⊢ (pderiv y)
      (X y ^ 2 * X z + C W'.a₁ * X x * X y * X z + C W'.a₃ * X y * X z ^ 2 -
        (X x ^ 3 + C W'.a₂ * X x ^ 2 * X z + C W'.a₄ * X x * X z ^ 2 + C W'.a₆ * X z ^ 3)) =
    C 2 * X y * X z + C W'.a₁ * X x * X z + C W'.a₃ * X z ^ 2

Tactic:
pderiv_simp

Result:
R : Type r
inst✝ : CommRing R
W' : Projective R
⊢ ↑2 * X y ^ (2 - 1) * 1 * X z + X y ^ 2 * 0 +
          (((0 * X x + C W'.a₁ * 0) * X y + C W'.a₁ * X x * 1) * X z + C W'.a₁ * X x * X y * 0) +
        ((0 * X y + C W'.a₃ * 1) * X z ^ 2 + C W'.a₃ * X y * (↑2 * X z ^ (2 - 1) * 0)) -
      (↑3 * X x ^ (3 - 1) * 0 + ((0 * X x ^ 2 + C W'.a₂ * (↑2 * X x ^ (2 - 1) * 0)) * X z + C W'.a₂ * X x ^ 2 * 0) +
          ((0 * X x + C W'.a₄ * 0) * X z ^ 2 + C W'.a₄ * X x * (↑2 * X z ^ (2 - 1) * 0)) +
        (0 * X z ^ 3 + C W'.a₆ * (↑3 * X z ^ (3 - 1) * 0))) =
    2 * X y * X z + C W'.a₁ * X x * X z + C W'.a₃ * X z ^ 2

Proof state:
R : Type r
inst✝ : CommRing R
W' : Projective R
⊢ ↑2 * X y ^ (2 - 1) * 1 * X z + X y ^ 2 * 0 +
          (((0 * X x + C W'.a₁ * 0) * X y + C W'.a₁ * X x * 1) * X z + C W'.a₁ * X x * X y * 0) +
        ((0 * X y + C W'.a₃ * 1) * X z ^ 2 + C W'.a₃ * X y * (↑2 * X z ^ (2 - 1) * 0)) -
      (↑3 * X x ^ (3 - 1) * 0 + ((0 * X x ^ 2 + C W'.a₂ * (↑2 * X x ^ (2 - 1) * 0)) * X z + C W'.a₂ * X x ^ 2 * 0) +
          ((0 * X x + C W'.a₄ * 0) * X z ^ 2 + C W'.a₄ * X x * (↑2 * X z ^ (2 - 1) * 0)) +
        (0 * X z ^ 3 + C W'.a₆ * (↑3 * X z ^ (3 - 1) * 0))) =
    2 * X y * X z + C W'.a₁ * X x * X z + C W'.a₃ * X z ^ 2

Tactic:
ring1

Result:
no goals
-- Mathlib/Data/Matrix/Mul.lean
theorem dotProduct_mulVec [Fintype n] [Fintype m] [NonUnitalSemiring R] (v : m → R)
    (A : Matrix m n R) (w : n → R) : v ⬝ᵥ A *ᵥ w = v ᵥ* A ⬝ᵥ w

Proof state:
m : Type u_2
n : Type u_3
R : Type u_7
inst✝² : Fintype n
inst✝¹ : Fintype m
inst✝ : NonUnitalSemiring R
v : m → R
A : Matrix m n R
w : n → R
⊢ v ⬝ᵥ A *ᵥ w = v ᵥ* A ⬝ᵥ w

Tactic:
simp only [dotProduct, vecMul, mulVec, Finset.mul_sum, Finset.sum_mul, mul_assoc]

Result:
m : Type u_2
n : Type u_3
R : Type u_7
inst✝² : Fintype n
inst✝¹ : Fintype m
inst✝ : NonUnitalSemiring R
v : m → R
A : Matrix m n R
w : n → R
⊢ ∑ x : m, ∑ i : n, v x * (A x i * w i) = ∑ x : n, ∑ x_1 : m, v x_1 * (A x_1 x * w x)

Proof state:
m : Type u_2
n : Type u_3
R : Type u_7
inst✝² : Fintype n
inst✝¹ : Fintype m
inst✝ : NonUnitalSemiring R
v : m → R
A : Matrix m n R
w : n → R
⊢ ∑ x : m, ∑ i : n, v x * (A x i * w i) = ∑ x : n, ∑ x_1 : m, v x_1 * (A x_1 x * w x)

Tactic:
exact Finset.sum_comm

Result:
no goals
-- Mathlib/Topology/Basic.lean
theorem dense_compl_singleton_iff_not_open :
    Dense ({x}ᶜ : Set X) ↔ ¬IsOpen ({x} : Set X)

Proof state:
case mp
X : Type u
x : X
inst✝ : TopologicalSpace X
⊢ Dense {x}ᶜ → ¬IsOpen {x}

Tactic:
intro hd ho

Result:
case mp
X : Type u
x : X
inst✝ : TopologicalSpace X
hd : Dense {x}ᶜ
ho : IsOpen {x}
⊢ False

Proof state:
case mpr
X : Type u
x : X
inst✝ : TopologicalSpace X
ho : ¬IsOpen {x}
U : Set X
hU : IsOpen U
hne : U.Nonempty
hUx : U ⊆ {x}
⊢ False

Tactic:
obtain rfl : U = {x} := eq_singleton_iff_nonempty_unique_mem.2 ⟨hne, hUx⟩

Result:
case mpr
X : Type u
x : X
inst✝ : TopologicalSpace X
ho : ¬IsOpen {x}
hU : IsOpen {x}
hne : {x}.Nonempty
hUx : {x} ⊆ {x}
⊢ False

Proof state:
case mpr
X : Type u
x : X
inst✝ : TopologicalSpace X
⊢ ¬IsOpen {x} → Dense {x}ᶜ

Tactic:
refine fun ho => dense_iff_inter_open.2 fun U hU hne => inter_compl_nonempty_iff.2 fun hUx => ?_

Result:
case mpr
X : Type u
x : X
inst✝ : TopologicalSpace X
ho : ¬IsOpen {x}
U : Set X
hU : IsOpen U
hne : U.Nonempty
hUx : U ⊆ {x}
⊢ False

Proof state:
case mp
X : Type u
x : X
inst✝ : TopologicalSpace X
hd : Dense {x}ᶜ
ho : IsOpen {x}
⊢ False

Tactic:
exact (hd.inter_open_nonempty _ ho (singleton_nonempty _)).ne_empty (inter_compl_self _)

Result:
no goals

Proof state:
case mpr
X : Type u
x : X
inst✝ : TopologicalSpace X
ho : ¬IsOpen {x}
hU : IsOpen {x}
hne : {x}.Nonempty
hUx : {x} ⊆ {x}
⊢ False

Tactic:
exact ho hU

Result:
no goals

Proof state:
X : Type u
x : X
inst✝ : TopologicalSpace X
⊢ Dense {x}ᶜ ↔ ¬IsOpen {x}

Tactic:
constructor

Result:
case mp
X : Type u
x : X
inst✝ : TopologicalSpace X
⊢ Dense {x}ᶜ → ¬IsOpen {x}

case mpr
X : Type u
x : X
inst✝ : TopologicalSpace X
⊢ ¬IsOpen {x} → Dense {x}ᶜ
-- Mathlib/MeasureTheory/Measure/NullMeasurable.lean
theorem measure_inter_add_diff₀ (s : Set α) (ht : NullMeasurableSet t μ) :
    μ (s ∩ t) + μ (s \ t) = μ s

Proof state:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
t s : Set α
ht : NullMeasurableSet t μ
⊢ μ (s ∩ t) + μ (s \ t) = μ s

Tactic:
refine le_antisymm ?_ (measure_le_inter_add_diff _ _ _)

Result:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
t s : Set α
ht : NullMeasurableSet t μ
⊢ μ (s ∩ t) + μ (s \ t) ≤ μ s

Proof state:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
t s : Set α
ht : NullMeasurableSet t μ
⊢ μ (s ∩ t) + μ (s \ t) ≤ μ s

Tactic:
rcases exists_measurable_superset μ s with ⟨s', hsub, hs'm, hs'⟩

Result:
case intro.intro.intro
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
t s : Set α
ht : NullMeasurableSet t μ
s' : Set α
hsub : s ⊆ s'
hs'm : MeasurableSet s'
hs' : μ s' = μ s
⊢ μ (s ∩ t) + μ (s \ t) ≤ μ s

Proof state:
case intro.intro.intro
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
t s : Set α
ht : NullMeasurableSet t μ
s' : Set α
hsub : s ⊆ s'
hs' : μ s' = μ s
hs'm : NullMeasurableSet s' μ
⊢ μ (s ∩ t) + μ (s \ t) ≤ μ s

Tactic:
calc
  μ (s ∩ t) + μ (s \ t) ≤ μ (s' ∩ t) + μ (s' \ t) := by gcongr
  _ = μ (s' ∩ t ∪ s' \ t) :=
    (measure_union₀_aux (hs'm.inter ht) (hs'm.diff ht) <|
        (@disjoint_inf_sdiff _ s' t _).aedisjoint).symm
  _ = μ s' := congr_arg μ (inter_union_diff _ _)
  _ = μ s := hs'

Result:
no goals

Proof state:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
t s : Set α
ht : NullMeasurableSet t μ
s' : Set α
hsub : s ⊆ s'
hs' : μ s' = μ s
hs'm : NullMeasurableSet s' μ
⊢ μ (s ∩ t) + μ (s \ t) ≤ μ (s' ∩ t) + μ (s' \ t)

Tactic:
gcongr

Result:
no goals

Proof state:
case intro.intro.intro
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
t s : Set α
ht : NullMeasurableSet t μ
s' : Set α
hsub : s ⊆ s'
hs'm : MeasurableSet s'
hs' : μ s' = μ s
⊢ μ (s ∩ t) + μ (s \ t) ≤ μ s

Tactic:
replace hs'm : NullMeasurableSet s' μ := hs'm.nullMeasurableSet

Result:
case intro.intro.intro
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
t s : Set α
ht : NullMeasurableSet t μ
s' : Set α
hsub : s ⊆ s'
hs' : μ s' = μ s
hs'm : NullMeasurableSet s' μ
⊢ μ (s ∩ t) + μ (s \ t) ≤ μ s
-- Mathlib/Data/Finsupp/Basic.lean
theorem mapDomain_injective {f : α → β} (hf : Function.Injective f) :
    Function.Injective (mapDomain f : (α →₀ M) → β →₀ M)

Proof state:
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : AddCommMonoid M
f : α → β
hf : Injective f
v₁ v₂ : α →₀ M
eq : mapDomain f v₁ = mapDomain f v₂
a : α
⊢ (mapDomain f v₁) (f a) = (mapDomain f v₂) (f a)

Tactic:
rw [eq]

Result:
no goals

Proof state:
case h
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : AddCommMonoid M
f : α → β
hf : Injective f
v₁ v₂ : α →₀ M
eq : mapDomain f v₁ = mapDomain f v₂
a : α
this : (mapDomain f v₁) (f a) = (mapDomain f v₂) (f a)
⊢ v₁ a = v₂ a

Tactic:
rwa [mapDomain_apply hf, mapDomain_apply hf] at this

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : AddCommMonoid M
f : α → β
hf : Injective f
v₁ v₂ : α →₀ M
eq : mapDomain f v₁ = mapDomain f v₂
⊢ v₁ = v₂

Tactic:
ext a

Result:
case h
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : AddCommMonoid M
f : α → β
hf : Injective f
v₁ v₂ : α →₀ M
eq : mapDomain f v₁ = mapDomain f v₂
a : α
⊢ v₁ a = v₂ a

Proof state:
case h
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : AddCommMonoid M
f : α → β
hf : Injective f
v₁ v₂ : α →₀ M
eq : mapDomain f v₁ = mapDomain f v₂
a : α
⊢ v₁ a = v₂ a

Tactic:
have : mapDomain f v₁ (f a) = mapDomain f v₂ (f a) := by rw [eq]

Result:
case h
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : AddCommMonoid M
f : α → β
hf : Injective f
v₁ v₂ : α →₀ M
eq : mapDomain f v₁ = mapDomain f v₂
a : α
this : (mapDomain f v₁) (f a) = (mapDomain f v₂) (f a)
⊢ v₁ a = v₂ a

Proof state:
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : AddCommMonoid M
f : α → β
hf : Injective f
⊢ Injective (mapDomain f)

Tactic:
intro v₁ v₂ eq

Result:
α : Type u_1
β : Type u_2
M : Type u_5
inst✝ : AddCommMonoid M
f : α → β
hf : Injective f
v₁ v₂ : α →₀ M
eq : mapDomain f v₁ = mapDomain f v₂
⊢ v₁ = v₂
-- Mathlib/MeasureTheory/VectorMeasure/WithDensity.lean
theorem withDensityᵥ_neg : μ.withDensityᵥ (-f) = -μ.withDensityᵥ f

Proof state:
case neg.hnc
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → E
hf : ¬Integrable f μ
⊢ ¬Integrable (-f) μ

Tactic:
rwa [integrable_neg_iff]

Result:
no goals

Proof state:
case pos.h
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → E
hf : Integrable f μ
i : Set α
hi : MeasurableSet i
⊢ ∫ (x : α) in i, (-f) x ∂μ = ∫ (a : α) in i, -f a ∂μ

Tactic:
simp only [Pi.neg_apply]

Result:
no goals

Proof state:
case neg
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → E
hf : ¬Integrable f μ
⊢ μ.withDensityᵥ (-f) = -μ.withDensityᵥ f

Tactic:
rw [withDensityᵥ, withDensityᵥ, dif_neg hf, dif_neg, neg_zero]

Result:
case neg.hnc
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → E
hf : ¬Integrable f μ
⊢ ¬Integrable (-f) μ

Proof state:
case pos
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → E
hf : Integrable f μ
⊢ μ.withDensityᵥ (-f) = -μ.withDensityᵥ f

Tactic:
ext1 i hi

Result:
case pos.h
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → E
hf : Integrable f μ
i : Set α
hi : MeasurableSet i
⊢ ↑(μ.withDensityᵥ (-f)) i = ↑(-μ.withDensityᵥ f) i

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → E
⊢ μ.withDensityᵥ (-f) = -μ.withDensityᵥ f

Tactic:
by_cases hf : Integrable f μ

Result:
case pos
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → E
hf : Integrable f μ
⊢ μ.withDensityᵥ (-f) = -μ.withDensityᵥ f

case neg
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → E
hf : ¬Integrable f μ
⊢ μ.withDensityᵥ (-f) = -μ.withDensityᵥ f

Proof state:
case pos.h
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → E
hf : Integrable f μ
i : Set α
hi : MeasurableSet i
⊢ ↑(μ.withDensityᵥ (-f)) i = ↑(-μ.withDensityᵥ f) i

Tactic:
rw [VectorMeasure.neg_apply, withDensityᵥ_apply hf hi, ← integral_neg,
  withDensityᵥ_apply hf.neg hi]

Result:
case pos.h
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → E
hf : Integrable f μ
i : Set α
hi : MeasurableSet i
⊢ ∫ (x : α) in i, (-f) x ∂μ = ∫ (a : α) in i, -f a ∂μ
-- Mathlib/MeasureTheory/Integral/Average.lean
theorem exists_not_mem_null_laverage_le (hμ : μ ≠ 0) (hint : ∫⁻ a : α, f a ∂μ ≠ ∞) (hN : μ N = 0) :
    ∃ x, x ∉ N ∧ ⨍⁻ a, f a ∂μ ≤ f x

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
N : Set α
f : α → ℝ≥0∞
hμ : μ ≠ 0
hint : ∫⁻ (a : α), f a ∂μ ≠ ⊤
hN : μ N = 0
this : 0 < μ ({x | ⨍⁻ (a : α), f a ∂μ ≤ f x} \ N)
⊢ ∃ x ∉ N, ⨍⁻ (a : α), f a ∂μ ≤ f x

Tactic:
obtain ⟨x, hx, hxN⟩ := nonempty_of_measure_ne_zero this.ne'

Result:
case intro.intro
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
N : Set α
f : α → ℝ≥0∞
hμ : μ ≠ 0
hint : ∫⁻ (a : α), f a ∂μ ≠ ⊤
hN : μ N = 0
this : 0 < μ ({x | ⨍⁻ (a : α), f a ∂μ ≤ f x} \ N)
x : α
hx : x ∈ {x | ⨍⁻ (a : α), f a ∂μ ≤ f x}
hxN : x ∉ N
⊢ ∃ x ∉ N, ⨍⁻ (a : α), f a ∂μ ≤ f x

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
N : Set α
f : α → ℝ≥0∞
hμ : μ ≠ 0
hint : ∫⁻ (a : α), f a ∂μ ≠ ⊤
hN : μ N = 0
⊢ ∃ x ∉ N, ⨍⁻ (a : α), f a ∂μ ≤ f x

Tactic:
have := measure_laverage_le_pos hμ hint

Result:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
N : Set α
f : α → ℝ≥0∞
hμ : μ ≠ 0
hint : ∫⁻ (a : α), f a ∂μ ≠ ⊤
hN : μ N = 0
this : 0 < μ {x | ⨍⁻ (a : α), f a ∂μ ≤ f x}
⊢ ∃ x ∉ N, ⨍⁻ (a : α), f a ∂μ ≤ f x

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
N : Set α
f : α → ℝ≥0∞
hμ : μ ≠ 0
hint : ∫⁻ (a : α), f a ∂μ ≠ ⊤
hN : μ N = 0
this : 0 < μ {x | ⨍⁻ (a : α), f a ∂μ ≤ f x}
⊢ ∃ x ∉ N, ⨍⁻ (a : α), f a ∂μ ≤ f x

Tactic:
rw [← measure_diff_null hN] at this

Result:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
N : Set α
f : α → ℝ≥0∞
hμ : μ ≠ 0
hint : ∫⁻ (a : α), f a ∂μ ≠ ⊤
hN : μ N = 0
this : 0 < μ ({x | ⨍⁻ (a : α), f a ∂μ ≤ f x} \ N)
⊢ ∃ x ∉ N, ⨍⁻ (a : α), f a ∂μ ≤ f x

Proof state:
case intro.intro
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
N : Set α
f : α → ℝ≥0∞
hμ : μ ≠ 0
hint : ∫⁻ (a : α), f a ∂μ ≠ ⊤
hN : μ N = 0
this : 0 < μ ({x | ⨍⁻ (a : α), f a ∂μ ≤ f x} \ N)
x : α
hx : x ∈ {x | ⨍⁻ (a : α), f a ∂μ ≤ f x}
hxN : x ∉ N
⊢ ∃ x ∉ N, ⨍⁻ (a : α), f a ∂μ ≤ f x

Tactic:
exact ⟨x, hxN, hx⟩

Result:
no goals
-- Mathlib/Geometry/Euclidean/Angle/Unoriented/Basic.lean
theorem angle_self_neg_of_nonzero {x : V} (hx : x ≠ 0) : angle x (-x) = π

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x : V
hx : x ≠ 0
⊢ angle x (-x) = π

Tactic:
rw [angle_neg_right, angle_self hx, sub_zero]

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Arithmetic.lean
theorem isLimit_add_iff {a b} : IsLimit (a + b) ↔ IsLimit b ∨ b = 0 ∧ IsLimit a

Proof state:
case neg.h
a b : Ordinal.{u_4}
h : (a + b).IsLimit
h' : ¬b = 0
⊢ a < a + b

Tactic:
suffices a + 0 < a + b by simpa only [add_zero] using this

Result:
case neg.h
a b : Ordinal.{u_4}
h : (a + b).IsLimit
h' : ¬b = 0
⊢ a + 0 < a + b

Proof state:
case pos
a b : Ordinal.{u_4}
h : (a + b).IsLimit
h' : b = 0
⊢ b.IsLimit ∨ b = 0 ∧ a.IsLimit

Tactic:
rw [h', add_zero] at h

Result:
case pos
a b : Ordinal.{u_4}
h : a.IsLimit
h' : b = 0
⊢ b.IsLimit ∨ b = 0 ∧ a.IsLimit

Proof state:
a b : Ordinal.{u_4}
h : (a + b).IsLimit
h' : ¬b = 0
this : a + 0 < a + b
⊢ a < a + b

Tactic:
simpa only [add_zero] using this

Result:
no goals

Proof state:
a b : Ordinal.{u_4}
⊢ (a + b).IsLimit ↔ b.IsLimit ∨ b = 0 ∧ a.IsLimit

Tactic:
constructor <;> intro h

Result:
case mp
a b : Ordinal.{u_4}
h : (a + b).IsLimit
⊢ b.IsLimit ∨ b = 0 ∧ a.IsLimit

case mpr
a b : Ordinal.{u_4}
h : b.IsLimit ∨ b = 0 ∧ a.IsLimit
⊢ (a + b).IsLimit

Proof state:
case mpr.inl
a b : Ordinal.{u_4}
h : b.IsLimit
⊢ (a + b).IsLimit

Tactic:
exact isLimit_add a h

Result:
no goals

Proof state:
case pos.h
a b : Ordinal.{u_4}
h : a.IsLimit
h' : b = 0
⊢ b = 0 ∧ a.IsLimit

Tactic:
exact ⟨h', h⟩

Result:
no goals

Proof state:
case neg
a b : Ordinal.{u_4}
h : (a + b).IsLimit
h' : ¬b = 0
⊢ b.IsLimit ∨ b = 0 ∧ a.IsLimit

Tactic:
left

Result:
case neg.h
a b : Ordinal.{u_4}
h : (a + b).IsLimit
h' : ¬b = 0
⊢ b.IsLimit

Proof state:
case neg.h
a b : Ordinal.{u_4}
h : (a + b).IsLimit
h' : ¬b = 0
⊢ (a + b - a).IsLimit

Tactic:
apply isLimit_sub h

Result:
case neg.h
a b : Ordinal.{u_4}
h : (a + b).IsLimit
h' : ¬b = 0
⊢ a < a + b

Proof state:
case mpr
a b : Ordinal.{u_4}
h : b.IsLimit ∨ b = 0 ∧ a.IsLimit
⊢ (a + b).IsLimit

Tactic:
rcases h with (h | ⟨rfl, h⟩)

Result:
case mpr.inl
a b : Ordinal.{u_4}
h : b.IsLimit
⊢ (a + b).IsLimit

case mpr.inr.intro
a : Ordinal.{u_4}
h : a.IsLimit
⊢ (a + 0).IsLimit

Proof state:
case neg.h
a b : Ordinal.{u_4}
h : (a + b).IsLimit
h' : ¬b = 0
⊢ a + 0 < a + b

Tactic:
rwa [add_lt_add_iff_left, Ordinal.pos_iff_ne_zero]

Result:
no goals

Proof state:
case neg.h
a b : Ordinal.{u_4}
h : (a + b).IsLimit
h' : ¬b = 0
⊢ b.IsLimit

Tactic:
rw [← add_sub_cancel a b]

Result:
case neg.h
a b : Ordinal.{u_4}
h : (a + b).IsLimit
h' : ¬b = 0
⊢ (a + b - a).IsLimit

Proof state:
case mpr.inr.intro
a : Ordinal.{u_4}
h : a.IsLimit
⊢ (a + 0).IsLimit

Tactic:
simpa only [add_zero]

Result:
no goals

Proof state:
case mp
a b : Ordinal.{u_4}
h : (a + b).IsLimit
⊢ b.IsLimit ∨ b = 0 ∧ a.IsLimit

Tactic:
by_cases h' : b = 0

Result:
case pos
a b : Ordinal.{u_4}
h : (a + b).IsLimit
h' : b = 0
⊢ b.IsLimit ∨ b = 0 ∧ a.IsLimit

case neg
a b : Ordinal.{u_4}
h : (a + b).IsLimit
h' : ¬b = 0
⊢ b.IsLimit ∨ b = 0 ∧ a.IsLimit

Proof state:
case pos
a b : Ordinal.{u_4}
h : a.IsLimit
h' : b = 0
⊢ b.IsLimit ∨ b = 0 ∧ a.IsLimit

Tactic:
right

Result:
case pos.h
a b : Ordinal.{u_4}
h : a.IsLimit
h' : b = 0
⊢ b = 0 ∧ a.IsLimit
-- Mathlib/Dynamics/TopologicalEntropy/CoverEntropy.lean
lemma coverMincard_zero (T : X → X) {F : Set X} (h : F.Nonempty) (U : Set (X × X)) :
    coverMincard T F U 0 = 1

Proof state:
case intro
X : Type u_1
T : X → X
F : Set X
U : Set (X × X)
x : X
h✝ : x ∈ F
this : IsDynCoverOf T F U 0 ↑{x}
⊢ coverMincard T F U 0 ≤ 1

Tactic:
apply this.coverMincard_le_card.trans_eq

Result:
case intro
X : Type u_1
T : X → X
F : Set X
U : Set (X × X)
x : X
h✝ : x ∈ F
this : IsDynCoverOf T F U 0 ↑{x}
⊢ ↑{x}.card = 1

Proof state:
case intro
X : Type u_1
T : X → X
F : Set X
U : Set (X × X)
x : X
h✝ : x ∈ F
⊢ coverMincard T F U 0 ≤ 1

Tactic:
have := isDynCoverOf_zero T F U (singleton_nonempty x)

Result:
case intro
X : Type u_1
T : X → X
F : Set X
U : Set (X × X)
x : X
h✝ : x ∈ F
this : IsDynCoverOf T F U 0 {x}
⊢ coverMincard T F U 0 ≤ 1

Proof state:
case intro
X : Type u_1
T : X → X
F : Set X
U : Set (X × X)
x : X
h✝ : x ∈ F
this : IsDynCoverOf T F U 0 ↑{x}
⊢ ↑{x}.card = 1

Tactic:
rw [Finset.card_singleton, Nat.cast_one]

Result:
no goals

Proof state:
case intro
X : Type u_1
T : X → X
F : Set X
U : Set (X × X)
x : X
h✝ : x ∈ F
this : IsDynCoverOf T F U 0 {x}
⊢ coverMincard T F U 0 ≤ 1

Tactic:
rw [← Finset.coe_singleton] at this

Result:
case intro
X : Type u_1
T : X → X
F : Set X
U : Set (X × X)
x : X
h✝ : x ∈ F
this : IsDynCoverOf T F U 0 ↑{x}
⊢ coverMincard T F U 0 ≤ 1

Proof state:
X : Type u_1
T : X → X
F : Set X
h : F.Nonempty
U : Set (X × X)
⊢ coverMincard T F U 0 ≤ 1

Tactic:
rcases h with ⟨x, _⟩

Result:
case intro
X : Type u_1
T : X → X
F : Set X
U : Set (X × X)
x : X
h✝ : x ∈ F
⊢ coverMincard T F U 0 ≤ 1

Proof state:
X : Type u_1
T : X → X
F : Set X
h : F.Nonempty
U : Set (X × X)
⊢ coverMincard T F U 0 = 1

Tactic:
apply le_antisymm _ ((one_le_coverMincard_iff T F U 0).2 h)

Result:
X : Type u_1
T : X → X
F : Set X
h : F.Nonempty
U : Set (X × X)
⊢ coverMincard T F U 0 ≤ 1