harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem getLast_append_right {l : List α} (h : l' ≠ []) :
    (l ++ l').getLast (fun h => by simp_all) = l'.getLast h

Proof state:
α : Type u_1
l' l : List α
h : l' ≠ []
⊢ (l ++ l').getLast ⋯ = l'.getLast h

Tactic:
rw [getLast_append, dif_neg (by simp_all)]

Result:
no goals

Proof state:
α : Type ?u.315451
l' l : List α
h✝ : l' ≠ []
h : l ++ l' = []
⊢ False

Tactic:
simp_all

Result:
no goals

Proof state:
α : Type u_1
l' l : List α
h : l' ≠ []
⊢ ¬l'.isEmpty = true

Tactic:
simp_all

Result:
no goals
-- Mathlib/Data/Set/Finite/Basic.lean
theorem Infinite.exists_subset_card_eq {s : Set α} (hs : s.Infinite) (n : ℕ) :
    ∃ t : Finset α, ↑t ⊆ s ∧ t.card = n :=
  ⟨((Finset.range n).map (hs.natEmbedding _)).map (Embedding.subtype _), by simp⟩

Proof state:
α : Type u
s : Set α
hs : s.Infinite
n : ℕ
⊢ ↑(Finset.map (Embedding.subtype fun x => x ∈ s) (Finset.map (natEmbedding s hs) (Finset.range n))) ⊆ s ∧
    (Finset.map (Embedding.subtype fun x => x ∈ s) (Finset.map (natEmbedding s hs) (Finset.range n))).card = n

Tactic:
simp

Result:
no goals
-- Mathlib/Data/NNReal/Defs.lean
@[simp]
lemma one_lt_toNNReal {r : ℝ} : 1 < r.toNNReal ↔ 1 < r

Proof state:
r : ℝ
⊢ 1 < r.toNNReal ↔ 1 < r

Tactic:
simpa only [not_le] using toNNReal_le_one.not

Result:
no goals
-- Mathlib/Data/Seq/WSeq.lean
theorem destruct_dropn : ∀ (s : WSeq α) (n), destruct (drop s n) = destruct s >>= drop.aux n
  | _, 0 => (bind_pure' _).symm
  | s, n + 1 => by
    rw [← dropn_tail, destruct_dropn _ n, destruct_tail, LawfulMonad.bind_assoc]
    rfl

Proof state:
α : Type u
s : WSeq α
n : ℕ
⊢ (s.drop (n + 1)).destruct = s.destruct >>= drop.aux (n + 1)

Tactic:
rw [← dropn_tail, destruct_dropn _ n, destruct_tail, LawfulMonad.bind_assoc]

Result:
α : Type u
s : WSeq α
n : ℕ
⊢ (s.destruct >>= fun x => tail.aux x >>= drop.aux n) = s.destruct >>= drop.aux (n + 1)

Proof state:
α : Type u
s : WSeq α
n : ℕ
⊢ (s.destruct >>= fun x => tail.aux x >>= drop.aux n) = s.destruct >>= drop.aux (n + 1)

Tactic:
rfl

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/Symmetric.lean
theorem IsSymmetric.conj_inner_sym {T : E →ₗ[𝕜] E} (hT : IsSymmetric T) (x y : E) :
    conj ⟪T x, y⟫ = ⟪T y, x⟫

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : E →ₗ[𝕜] E
hT : T.IsSymmetric
x y : E
⊢ (starRingEnd 𝕜) (inner (T x) y) = inner (T y) x

Tactic:
rw [hT x y, inner_conj_symm]

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/VariableChange.lean
@[simp]
lemma variableChange_c₆ : (W.variableChange C).c₆ = C.u⁻¹ ^ 6 * W.c₆

Proof state:
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
C : VariableChange R
⊢ -(↑C.u⁻¹ ^ 2 * (W.b₂ + 12 * C.r)) ^ 3 +
        36 * (↑C.u⁻¹ ^ 2 * (W.b₂ + 12 * C.r)) * (↑C.u⁻¹ ^ 4 * (W.b₄ + C.r * W.b₂ + 6 * C.r ^ 2)) -
      216 * (↑C.u⁻¹ ^ 6 * (W.b₆ + 2 * C.r * W.b₄ + C.r ^ 2 * W.b₂ + 4 * C.r ^ 3)) =
    ↑C.u⁻¹ ^ 6 * (-W.b₂ ^ 3 + 36 * W.b₂ * W.b₄ - 216 * W.b₆)

Tactic:
ring1

Result:
no goals

Proof state:
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
C : VariableChange R
⊢ (W.variableChange C).c₆ = ↑C.u⁻¹ ^ 6 * W.c₆

Tactic:
simp only [c₆, variableChange_b₂, variableChange_b₄, variableChange_b₆]

Result:
R : Type u
inst✝ : CommRing R
W : WeierstrassCurve R
C : VariableChange R
⊢ -(↑C.u⁻¹ ^ 2 * (W.b₂ + 12 * C.r)) ^ 3 +
        36 * (↑C.u⁻¹ ^ 2 * (W.b₂ + 12 * C.r)) * (↑C.u⁻¹ ^ 4 * (W.b₄ + C.r * W.b₂ + 6 * C.r ^ 2)) -
      216 * (↑C.u⁻¹ ^ 6 * (W.b₆ + 2 * C.r * W.b₄ + C.r ^ 2 * W.b₂ + 4 * C.r ^ 3)) =
    ↑C.u⁻¹ ^ 6 * (-W.b₂ ^ 3 + 36 * W.b₂ * W.b₄ - 216 * W.b₆)
-- Mathlib/Order/PartialSups.lean
theorem iSup_le_iSup_of_partialSups_le_partialSups {f g : ι → α}
    (h : partialSups f ≤ partialSups g) : ⨆ i, f i ≤ ⨆ i, g i

Proof state:
α : Type u_1
ι : Type u_2
inst✝² : Preorder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : CompleteLattice α
f g : ι → α
h : partialSups f ≤ partialSups g
⊢ ⨆ i, f i ≤ ⨆ i, g i

Tactic:
rw [← iSup_partialSups_eq f, ← iSup_partialSups_eq g]

Result:
α : Type u_1
ι : Type u_2
inst✝² : Preorder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : CompleteLattice α
f g : ι → α
h : partialSups f ≤ partialSups g
⊢ ⨆ i, (partialSups f) i ≤ ⨆ i, (partialSups g) i

Proof state:
α : Type u_1
ι : Type u_2
inst✝² : Preorder ι
inst✝¹ : LocallyFiniteOrderBot ι
inst✝ : CompleteLattice α
f g : ι → α
h : partialSups f ≤ partialSups g
⊢ ⨆ i, (partialSups f) i ≤ ⨆ i, (partialSups g) i

Tactic:
exact iSup_mono h

Result:
no goals
-- Mathlib/Data/Part.lean
theorem append_mem_append [Append α] (a b : Part α) (ma mb : α) (ha : ma ∈ a) (hb : mb ∈ b) :
    ma ++ mb ∈ a ++ b

Proof state:
α : Type u_1
inst✝ : Append α
a b : Part α
ma mb : α
ha : ma ∈ a
hb : mb ∈ b
⊢ ∃ a_1 ∈ a, ∃ a ∈ b, a_1 ++ a = ma ++ mb

Tactic:
aesop

Result:
no goals

Proof state:
α : Type u_1
inst✝ : Append α
a b : Part α
ma mb : α
ha : ma ∈ a
hb : mb ∈ b
⊢ ma ++ mb ∈ a ++ b

Tactic:
simp [append_def]

Result:
α : Type u_1
inst✝ : Append α
a b : Part α
ma mb : α
ha : ma ∈ a
hb : mb ∈ b
⊢ ∃ a_1 ∈ a, ∃ a ∈ b, a_1 ++ a = ma ++ mb
-- Mathlib/Geometry/Euclidean/Angle/Unoriented/Basic.lean
theorem angle_eq_pi_iff {x y : V} : angle x y = π ↔ x ≠ 0 ∧ ∃ r : ℝ, r < 0 ∧ y = r • x

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
⊢ angle x y = π ↔ x ≠ 0 ∧ ∃ r < 0, y = r • x

Tactic:
rw [angle, ← real_inner_div_norm_mul_norm_eq_neg_one_iff, Real.arccos_eq_pi, LE.le.le_iff_eq]

Result:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
⊢ -1 ≤ inner x y / (‖x‖ * ‖y‖)

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
⊢ -1 ≤ inner x y / (‖x‖ * ‖y‖)

Tactic:
exact (abs_le.mp (abs_real_inner_div_norm_mul_norm_le_one x y)).1

Result:
no goals
-- Mathlib/Probability/Kernel/Basic.lean
theorem setLIntegral_restrict (κ : Kernel α β) (hs : MeasurableSet s) (a : α) (f : β → ℝ≥0∞)
    (t : Set β) : ∫⁻ b in t, f b ∂κ.restrict hs a = ∫⁻ b in t ∩ s, f b ∂κ a

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
s : Set β
κ : Kernel α β
hs : MeasurableSet s
a : α
f : β → ℝ≥0∞
t : Set β
⊢ ∫⁻ (b : β) in t, f b ∂(κ.restrict hs) a = ∫⁻ (b : β) in t ∩ s, f b ∂κ a

Tactic:
rw [restrict_apply, Measure.restrict_restrict' hs]

Result:
no goals
-- Mathlib/Algebra/Polynomial/UnitTrinomial.lean
theorem trinomial_natTrailingDegree (hkm : k < m) (hmn : m < n) (hu : u ≠ 0) :
    (trinomial k m n u v w).natTrailingDegree = k

Proof state:
case inr.inl
R : Type u_1
inst✝ : Semiring R
k n : ℕ
u v w : R
hu : u ≠ 0
i : ℕ
hkm : k < i
hmn : i < n
⊢ ↑k ≤ ↑i

Tactic:
exact WithTop.coe_le_coe.mpr hkm.le

Result:
no goals

Proof state:
case inr.inr
R : Type u_1
inst✝ : Semiring R
k m : ℕ
u v w : R
hkm : k < m
hu : u ≠ 0
i : ℕ
hmn : m < i
⊢ ↑k ≤ ↑i

Tactic:
exact WithTop.coe_le_coe.mpr (hkm.trans hmn).le

Result:
no goals

Proof state:
R : Type u_1
inst✝ : Semiring R
k m n : ℕ
u v w : R
hkm : k < m
hmn : m < n
hu : u ≠ 0
i : ℕ
h : i = k ∨ i = m ∨ i = n
⊢ ↑k ≤ ↑i

Tactic:
rcases h with (rfl | rfl | rfl)

Result:
case inl
R : Type u_1
inst✝ : Semiring R
m n : ℕ
u v w : R
hmn : m < n
hu : u ≠ 0
i : ℕ
hkm : i < m
⊢ ↑i ≤ ↑i

case inr.inl
R : Type u_1
inst✝ : Semiring R
k n : ℕ
u v w : R
hu : u ≠ 0
i : ℕ
hkm : k < i
hmn : i < n
⊢ ↑k ≤ ↑i

case inr.inr
R : Type u_1
inst✝ : Semiring R
k m : ℕ
u v w : R
hkm : k < m
hu : u ≠ 0
i : ℕ
hmn : m < i
⊢ ↑k ≤ ↑i

Proof state:
R : Type u_1
inst✝ : Semiring R
k m n : ℕ
u v w : R
hkm : k < m
hmn : m < n
hu : u ≠ 0
⊢ (trinomial k m n u v w).natTrailingDegree = k

Tactic:
refine
  natTrailingDegree_eq_of_trailingDegree_eq_some
    ((Finset.le_inf fun i h => ?_).antisymm <|
        trailingDegree_le_of_ne_zero <| by rwa [trinomial_trailing_coeff' hkm hmn]).symm

Result:
R : Type u_1
inst✝ : Semiring R
k m n : ℕ
u v w : R
hkm : k < m
hmn : m < n
hu : u ≠ 0
i : ℕ
h : i ∈ (trinomial k m n u v w).support
⊢ ↑k ≤ ↑i

Proof state:
R : Type u_1
inst✝ : Semiring R
k m n : ℕ
u v w : R
hkm : k < m
hmn : m < n
hu : u ≠ 0
i : ℕ
h : i ∈ {k, m, n}
⊢ ↑k ≤ ↑i

Tactic:
rw [mem_insert, mem_insert, mem_singleton] at h

Result:
R : Type u_1
inst✝ : Semiring R
k m n : ℕ
u v w : R
hkm : k < m
hmn : m < n
hu : u ≠ 0
i : ℕ
h : i = k ∨ i = m ∨ i = n
⊢ ↑k ≤ ↑i

Proof state:
R : Type u_1
inst✝ : Semiring R
k m n : ℕ
u v w : R
hkm : k < m
hmn : m < n
hu : u ≠ 0
⊢ (trinomial k m n u v w).coeff k ≠ 0

Tactic:
rwa [trinomial_trailing_coeff' hkm hmn]

Result:
no goals

Proof state:
R : Type u_1
inst✝ : Semiring R
k m n : ℕ
u v w : R
hkm : k < m
hmn : m < n
hu : u ≠ 0
i : ℕ
h : i ∈ (trinomial k m n u v w).support
⊢ ↑k ≤ ↑i

Tactic:
replace h := support_trinomial' k m n u v w h

Result:
R : Type u_1
inst✝ : Semiring R
k m n : ℕ
u v w : R
hkm : k < m
hmn : m < n
hu : u ≠ 0
i : ℕ
h : i ∈ {k, m, n}
⊢ ↑k ≤ ↑i

Proof state:
case inl
R : Type u_1
inst✝ : Semiring R
m n : ℕ
u v w : R
hmn : m < n
hu : u ≠ 0
i : ℕ
hkm : i < m
⊢ ↑i ≤ ↑i

Tactic:
exact le_rfl

Result:
no goals
-- Mathlib/CategoryTheory/Adjunction/Reflective.lean
lemma Functor.essImage.counit_isIso [Coreflective j] {A : D} (h : j.essImage A) :
    IsIso ((coreflectorAdjunction j).counit.app A)

Proof state:
C : Type u₁
D : Type u₂
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Category.{v₂, u₂} D
j : C ⥤ D
inst✝ : Coreflective j
A : D
h : j.essImage A
⊢ IsIso ((coreflectorAdjunction j).counit.app A)

Tactic:
rwa [isIso_counit_app_iff_mem_essImage]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/WithDensity.lean
theorem withDensity_apply' [SFinite μ] (f : α → ℝ≥0∞) (s : Set α) :
    μ.withDensity f s = ∫⁻ a in s, f a ∂μ

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : SFinite μ
f : α → ℝ≥0∞
s : Set α
t : Set α := toMeasurable μ s
⊢ ∫⁻ (a : α) in t, f a ∂μ = ∫⁻ (a : α) in s, f a ∂μ

Tactic:
congr 1

Result:
case e_μ
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : SFinite μ
f : α → ℝ≥0∞
s : Set α
t : Set α := toMeasurable μ s
⊢ μ.restrict t = μ.restrict s

Proof state:
case e_μ
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : SFinite μ
f : α → ℝ≥0∞
s : Set α
t : Set α := toMeasurable μ s
⊢ μ.restrict t = μ.restrict s

Tactic:
exact restrict_toMeasurable_of_sFinite s

Result:
no goals

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : SFinite μ
f : α → ℝ≥0∞
s : Set α
t : Set α := toMeasurable μ s
⊢ (μ.withDensity f) s ≤ ∫⁻ (a : α) in s, f a ∂μ

Tactic:
calc
μ.withDensity f s ≤ μ.withDensity f t := measure_mono (subset_toMeasurable μ s)
_ = ∫⁻ a in t, f a ∂μ := withDensity_apply f (measurableSet_toMeasurable μ s)
_ = ∫⁻ a in s, f a ∂μ := by congr 1; exact restrict_toMeasurable_of_sFinite s

Result:
no goals

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : SFinite μ
f : α → ℝ≥0∞
s : Set α
⊢ (μ.withDensity f) s ≤ ∫⁻ (a : α) in s, f a ∂μ

Tactic:
let t := toMeasurable μ s

Result:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : SFinite μ
f : α → ℝ≥0∞
s : Set α
t : Set α := toMeasurable μ s
⊢ (μ.withDensity f) s ≤ ∫⁻ (a : α) in s, f a ∂μ

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : SFinite μ
f : α → ℝ≥0∞
s : Set α
⊢ (μ.withDensity f) s = ∫⁻ (a : α) in s, f a ∂μ

Tactic:
apply le_antisymm ?_ (withDensity_apply_le f s)

Result:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : SFinite μ
f : α → ℝ≥0∞
s : Set α
⊢ (μ.withDensity f) s ≤ ∫⁻ (a : α) in s, f a ∂μ
-- Mathlib/SetTheory/Cardinal/Cofinality.lean
theorem isRegular_aleph0 : IsRegular ℵ₀ :=
  ⟨le_rfl, by simp⟩

Proof state:
⊢ ℵ₀ ≤ ℵ₀.ord.cof

Tactic:
simp

Result:
no goals
-- Mathlib/CategoryTheory/Monoidal/Bimod.lean
theorem inv_hom_id : inv P ≫ hom P = 𝟙 _

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : HasCoequalizers C
R S : Mon_ C
P : Bimod R S
⊢ ((ρ_ P.X).inv ≫ P.X ◁ S.one ≫ coequalizer.π (P.actRight ▷ S.X) ((α_ P.X S.X S.X).hom ≫ P.X ◁ S.mul)) ≫
      coequalizer.desc P.actRight ⋯ =
    𝟙 P.X

Tactic:
slice_lhs 3 4 => rw [coequalizer.π_desc]

Result:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : HasCoequalizers C
R S : Mon_ C
P : Bimod R S
⊢ (ρ_ P.X).inv ≫ P.X ◁ S.one ≫ P.actRight = 𝟙 P.X

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : HasCoequalizers C
R S : Mon_ C
P : Bimod R S
⊢ (ρ_ P.X).inv ≫ P.X ◁ S.one ≫ P.actRight = 𝟙 P.X

Tactic:
rw [actRight_one, Iso.inv_hom_id]

Result:
no goals

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : HasCoequalizers C
R S : Mon_ C
P : Bimod R S
⊢ inv P ≫ hom P = 𝟙 P.X

Tactic:
dsimp [hom, inv]

Result:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
inst✝ : HasCoequalizers C
R S : Mon_ C
P : Bimod R S
⊢ ((ρ_ P.X).inv ≫ P.X ◁ S.one ≫ coequalizer.π (P.actRight ▷ S.X) ((α_ P.X S.X S.X).hom ≫ P.X ◁ S.mul)) ≫
      coequalizer.desc P.actRight ⋯ =
    𝟙 P.X
-- Mathlib/Data/Set/Finite/Basic.lean
theorem infinite_of_finite_compl [Infinite α] {s : Set α} (hs : sᶜ.Finite) : s.Infinite := fun h =>
  Set.infinite_univ (α := α) (by simpa using hs.union h)

Proof state:
α : Type u
inst✝ : Infinite α
s : Set α
hs : sᶜ.Finite
h : s.Finite
⊢ univ.Finite

Tactic:
simpa using hs.union h

Result:
no goals
-- Mathlib/CategoryTheory/Subobject/Basic.lean
theorem ofLEMk_comp_ofMkLE {B A : C} (X : Subobject B) (f : A ⟶ B) [Mono f] (Y : Subobject B)
    (h₁ : X ≤ mk f) (h₂ : mk f ≤ Y) : ofLEMk X f h₁ ≫ ofMkLE f Y h₂ = ofLE X Y (h₁.trans h₂)

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
B A : C
X : Subobject B
f : A ⟶ B
inst✝ : Mono f
Y : Subobject B
h₁ : X ≤ mk f
h₂ : mk f ≤ Y
⊢ X.ofLEMk f h₁ ≫ ofMkLE f Y h₂ = X.ofLE Y ⋯

Tactic:
simp only [ofMkLE, ofLEMk, ofLE, ← Functor.map_comp underlying, assoc, Iso.hom_inv_id_assoc]

Result:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
B A : C
X : Subobject B
f : A ⟶ B
inst✝ : Mono f
Y : Subobject B
h₁ : X ≤ mk f
h₂ : mk f ≤ Y
⊢ underlying.map (h₁.hom ≫ h₂.hom) = underlying.map ⋯.hom

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
B A : C
X : Subobject B
f : A ⟶ B
inst✝ : Mono f
Y : Subobject B
h₁ : X ≤ mk f
h₂ : mk f ≤ Y
⊢ underlying.map (h₁.hom ≫ h₂.hom) = underlying.map ⋯.hom

Tactic:
congr 1

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem foldl_flatten (f : β → α → β) (b : β) (L : List (List α)) :
    (flatten L).foldl f b = L.foldl (fun b l => l.foldl f b) b

Proof state:
β : Type u_1
α : Type u_2
f : β → α → β
b : β
L : List (List α)
⊢ foldl f b L.flatten = foldl (fun b l => foldl f b l) b L

Tactic:
induction L generalizing b <;> simp_all

Result:
no goals
-- Mathlib/Topology/MetricSpace/PiNat.lean
theorem dist_comm (x y : ∀ n, E n) : dist x y = dist y x

Proof state:
E : ℕ → Type u_1
x y : (n : ℕ) → E n
⊢ dist x y = dist y x

Tactic:
classical
simp [dist, @eq_comm _ x y, firstDiff_comm]

Result:
no goals

Proof state:
E : ℕ → Type u_1
x y : (n : ℕ) → E n
⊢ dist x y = dist y x

Tactic:
simp [dist, @eq_comm _ x y, firstDiff_comm]

Result:
no goals
-- Mathlib/InformationTheory/KullbackLeibler/Basic.lean
@[simp]
lemma klDiv_of_not_integrable (h : ¬ Integrable (llr μ ν) μ) : klDiv μ ν = ∞

Proof state:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
h : ¬Integrable (llr μ ν) μ
⊢ klDiv μ ν = ⊤

Tactic:
rw [klDiv_def]

Result:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
h : ¬Integrable (llr μ ν) μ
⊢ (if μ ≪ ν ∧ Integrable (llr μ ν) μ then ENNReal.ofReal (∫ (x : α), llr μ ν x ∂μ + (ν univ).toReal - (μ univ).toReal)
    else ⊤) =
    ⊤

Proof state:
α : Type u_1
mα : MeasurableSpace α
μ ν : Measure α
h : ¬Integrable (llr μ ν) μ
⊢ (if μ ≪ ν ∧ Integrable (llr μ ν) μ then ENNReal.ofReal (∫ (x : α), llr μ ν x ∂μ + (ν univ).toReal - (μ univ).toReal)
    else ⊤) =
    ⊤

Tactic:
exact if_neg (not_and_of_not_right _ h)

Result:
no goals
-- Mathlib/CategoryTheory/MorphismProperty/Limits.lean
@[simp]
lemma pushouts_le_iff {P Q : MorphismProperty C} [Q.IsStableUnderCobaseChange] :
    P.pushouts ≤ Q ↔ P ≤ Q

Proof state:
case mpr
C : Type u
inst✝¹ : Category.{v, u} C
P Q : MorphismProperty C
inst✝ : Q.IsStableUnderCobaseChange
⊢ P ≤ Q → P.pushouts ≤ Q

Tactic:
intro h

Result:
case mpr
C : Type u
inst✝¹ : Category.{v, u} C
P Q : MorphismProperty C
inst✝ : Q.IsStableUnderCobaseChange
h : P ≤ Q
⊢ P.pushouts ≤ Q

Proof state:
case mpr
C : Type u
inst✝¹ : Category.{v, u} C
P Q : MorphismProperty C
inst✝ : Q.IsStableUnderCobaseChange
h : P ≤ Q
⊢ P.pushouts ≤ Q

Tactic:
exact le_trans (pushouts_monotone h) pushouts_le

Result:
no goals

Proof state:
case mp
C : Type u
inst✝¹ : Category.{v, u} C
P Q : MorphismProperty C
inst✝ : Q.IsStableUnderCobaseChange
⊢ P.pushouts ≤ Q → P ≤ Q

Tactic:
exact le_trans P.le_pushouts

Result:
no goals

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
P Q : MorphismProperty C
inst✝ : Q.IsStableUnderCobaseChange
⊢ P.pushouts ≤ Q ↔ P ≤ Q

Tactic:
constructor

Result:
case mp
C : Type u
inst✝¹ : Category.{v, u} C
P Q : MorphismProperty C
inst✝ : Q.IsStableUnderCobaseChange
⊢ P.pushouts ≤ Q → P ≤ Q

case mpr
C : Type u
inst✝¹ : Category.{v, u} C
P Q : MorphismProperty C
inst✝ : Q.IsStableUnderCobaseChange
⊢ P ≤ Q → P.pushouts ≤ Q
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/Normalize/BitVec.lean
theorem BitVec.le_ult (x y : BitVec w) : (x ≤ y) ↔ ((!y.ult x) = true)

Proof state:
w : Nat
x y : BitVec w
⊢ x ≤ y ↔ x.ule y = true

Tactic:
simp [BitVec.le_def, BitVec.ule]

Result:
no goals

Proof state:
w : Nat
x y : BitVec w
this : x ≤ y ↔ x.ule y = true
⊢ x ≤ y ↔ (!y.ult x) = true

Tactic:
rw [this, BitVec.ule_eq_not_ult]

Result:
no goals

Proof state:
w : Nat
x y : BitVec w
⊢ x ≤ y ↔ (!y.ult x) = true

Tactic:
have : x ≤ y ↔ (x.ule y = true) := by
  simp [BitVec.le_def, BitVec.ule]

Result:
w : Nat
x y : BitVec w
this : x ≤ y ↔ x.ule y = true
⊢ x ≤ y ↔ (!y.ult x) = true
-- Mathlib/Analysis/BoxIntegral/Box/Basic.lean
theorem diam_Icc_le_of_distortion_le (I : Box ι) (i : ι) {c : ℝ≥0} (h : I.distortion ≤ c) :
    diam (Box.Icc I) ≤ c * (I.upper i - I.lower i) :=
  have : (0 : ℝ) ≤ c * (I.upper i - I.lower i) :=
    mul_nonneg c.coe_nonneg (sub_nonneg.2 <| I.lower_le_upper _)
  diam_le_of_forall_dist_le this fun x hx y hy ↦
    calc
      dist x y ≤ dist I.lower I.upper := Real.dist_le_of_mem_pi_Icc hx hy
      _ ≤ I.distortion * (I.upper i - I.lower i) := I.dist_le_distortion_mul i
      _ ≤ c * (I.upper i - I.lower i)

Proof state:
case a0
ι : Type u_1
inst✝ : Fintype ι
I : Box ι
i : ι
c : ℝ≥0
h : I.distortion ≤ c
this : 0 ≤ ↑c * (I.upper i - I.lower i)
x : ι → ℝ
hx : x ∈ Box.Icc I
y : ι → ℝ
hy : y ∈ Box.Icc I
⊢ 0 ≤ I.upper i - I.lower i

Tactic:
exact sub_nonneg.2 (I.lower_le_upper i)

Result:
no goals

Proof state:
ι : Type u_1
inst✝ : Fintype ι
I : Box ι
i : ι
c : ℝ≥0
h : I.distortion ≤ c
this : 0 ≤ ↑c * (I.upper i - I.lower i)
x : ι → ℝ
hx : x ∈ Box.Icc I
y : ι → ℝ
hy : y ∈ Box.Icc I
⊢ ↑I.distortion * (I.upper i - I.lower i) ≤ ↑c * (I.upper i - I.lower i)

Tactic:
gcongr

Result:
case a0
ι : Type u_1
inst✝ : Fintype ι
I : Box ι
i : ι
c : ℝ≥0
h : I.distortion ≤ c
this : 0 ≤ ↑c * (I.upper i - I.lower i)
x : ι → ℝ
hx : x ∈ Box.Icc I
y : ι → ℝ
hy : y ∈ Box.Icc I
⊢ 0 ≤ I.upper i - I.lower i
-- Mathlib/Algebra/BigOperators/Group/Finset/Basic.lean
theorem prod_apply_ite_of_false {p : α → Prop} {hp : DecidablePred p} (f g : α → γ) (k : γ → β)
    (h : ∀ x ∈ s, ¬p x) : (∏ x ∈ s, k (if p x then f x else g x)) = ∏ x ∈ s, k (g x)

Proof state:
α : Type u_3
β : Type u_4
γ : Type u_5
s : Finset α
inst✝ : CommMonoid β
p : α → Prop
hp : DecidablePred p
f g : α → γ
k : γ → β
h : ∀ x ∈ s, ¬p x
⊢ ∏ x ∈ s, k (if p x then f x else g x) = ∏ x ∈ s, k (g x)

Tactic:
simp_rw [apply_ite k]

Result:
α : Type u_3
β : Type u_4
γ : Type u_5
s : Finset α
inst✝ : CommMonoid β
p : α → Prop
hp : DecidablePred p
f g : α → γ
k : γ → β
h : ∀ x ∈ s, ¬p x
⊢ (∏ x ∈ s, if p x then k (f x) else k (g x)) = ∏ x ∈ s, k (g x)

Proof state:
α : Type u_3
β : Type u_4
γ : Type u_5
s : Finset α
inst✝ : CommMonoid β
p : α → Prop
hp : DecidablePred p
f g : α → γ
k : γ → β
h : ∀ x ∈ s, ¬p x
⊢ (∏ x ∈ s, if p x then k (f x) else k (g x)) = ∏ x ∈ s, k (g x)

Tactic:
exact prod_ite_of_false h _ _

Result:
no goals
-- Mathlib/Analysis/Normed/Operator/LinearIsometry.lean
theorem range_eq_univ (e : E ≃ₛₗᵢ[σ₁₂] E₂) : Set.range e = Set.univ

Proof state:
R : Type u_1
R₂ : Type u_2
E : Type u_5
E₂ : Type u_6
inst✝⁷ : Semiring R
inst✝⁶ : Semiring R₂
σ₁₂ : R →+* R₂
σ₂₁ : R₂ →+* R
inst✝⁵ : RingHomInvPair σ₁₂ σ₂₁
inst✝⁴ : RingHomInvPair σ₂₁ σ₁₂
inst✝³ : SeminormedAddCommGroup E
inst✝² : SeminormedAddCommGroup E₂
inst✝¹ : Module R E
inst✝ : Module R₂ E₂
e : E ≃ₛₗᵢ[σ₁₂] E₂
⊢ range ⇑e.toIsometryEquiv = univ

Tactic:
exact IsometryEquiv.range_eq_univ _

Result:
no goals

Proof state:
R : Type u_1
R₂ : Type u_2
E : Type u_5
E₂ : Type u_6
inst✝⁷ : Semiring R
inst✝⁶ : Semiring R₂
σ₁₂ : R →+* R₂
σ₂₁ : R₂ →+* R
inst✝⁵ : RingHomInvPair σ₁₂ σ₂₁
inst✝⁴ : RingHomInvPair σ₂₁ σ₁₂
inst✝³ : SeminormedAddCommGroup E
inst✝² : SeminormedAddCommGroup E₂
inst✝¹ : Module R E
inst✝ : Module R₂ E₂
e : E ≃ₛₗᵢ[σ₁₂] E₂
⊢ range ⇑e = univ

Tactic:
rw [← coe_toIsometryEquiv]

Result:
R : Type u_1
R₂ : Type u_2
E : Type u_5
E₂ : Type u_6
inst✝⁷ : Semiring R
inst✝⁶ : Semiring R₂
σ₁₂ : R →+* R₂
σ₂₁ : R₂ →+* R
inst✝⁵ : RingHomInvPair σ₁₂ σ₂₁
inst✝⁴ : RingHomInvPair σ₂₁ σ₁₂
inst✝³ : SeminormedAddCommGroup E
inst✝² : SeminormedAddCommGroup E₂
inst✝¹ : Module R E
inst✝ : Module R₂ E₂
e : E ≃ₛₗᵢ[σ₁₂] E₂
⊢ range ⇑e.toIsometryEquiv = univ
-- Mathlib/Algebra/ContinuedFractions/Computation/TerminatesIffRat.lean
theorem of_terminates_iff_of_rat_terminates {v : K} {q : ℚ} (v_eq_q : v = (q : K)) :
    (of v).Terminates ↔ (of q).Terminates

Proof state:
K : Type u_1
inst✝¹ : LinearOrderedField K
inst✝ : FloorRing K
v : K
q : ℚ
v_eq_q : v = ↑q
⊢ (of v).Terminates ↔ (of q).Terminates

Tactic:
constructor <;> intro h <;> obtain ⟨n, h⟩ := h <;> use n <;>
  simp only [Stream'.Seq.TerminatedAt, (coe_of_s_get?_rat_eq v_eq_q n).symm] at h ⊢ <;>
  cases h' : (of q).s.get? n <;>
  simp only [h'] at h <;>
  trivial

Result:
no goals
-- Mathlib/Topology/ContinuousMap/Units.lean
theorem spectrum_eq_range [CompleteSpace 𝕜] (f : C(X, 𝕜)) : spectrum 𝕜 f = Set.range f

Proof state:
X : Type u_1
𝕜 : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : NormedField 𝕜
inst✝ : CompleteSpace 𝕜
f : C(X, 𝕜)
⊢ ⇑(RingHom.id 𝕜) ⁻¹' Set.range ⇑f = Set.range ⇑f

Tactic:
exact Set.preimage_id

Result:
no goals

Proof state:
X : Type u_1
𝕜 : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : NormedField 𝕜
inst✝ : CompleteSpace 𝕜
f : C(X, 𝕜)
⊢ spectrum 𝕜 f = Set.range ⇑f

Tactic:
rw [spectrum_eq_preimage_range, Algebra.id.map_eq_id]

Result:
X : Type u_1
𝕜 : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : NormedField 𝕜
inst✝ : CompleteSpace 𝕜
f : C(X, 𝕜)
⊢ ⇑(RingHom.id 𝕜) ⁻¹' Set.range ⇑f = Set.range ⇑f
-- Mathlib/GroupTheory/Abelianization.lean
theorem commutator_eq_closure : commutator G = Subgroup.closure (commutatorSet G)

Proof state:
G : Type u
inst✝ : Group G
⊢ commutator G = Subgroup.closure (commutatorSet G)

Tactic:
simp [commutator, Subgroup.commutator_def, commutatorSet]

Result:
no goals
-- Mathlib/Topology/Constructions.lean
theorem set_pi_mem_nhds_iff {I : Set ι} (hI : I.Finite) {s : ∀ i, Set (π i)} (a : ∀ i, π i) :
    I.pi s ∈ 𝓝 a ↔ ∀ i : ι, i ∈ I → s i ∈ 𝓝 (a i)

Proof state:
ι : Type u_5
π : ι → Type u_6
T : (i : ι) → TopologicalSpace (π i)
I : Set ι
hI : I.Finite
s : (i : ι) → Set (π i)
a : (i : ι) → π i
⊢ I.pi s ∈ 𝓝 a ↔ ∀ i ∈ I, s i ∈ 𝓝 (a i)

Tactic:
rw [nhds_pi, pi_mem_pi_iff hI]

Result:
no goals
-- Mathlib/Data/Vector/Defs.lean
lemma toList_getElem (v : Vector α n) (i : ℕ) {hi : i < v.toList.length} :
    v.toList[i] = v[i]'(by simp_all) := rfl

Proof state:
α : Type u_1
β : Type u_2
σ : Type u_3
φ : Type u_4
n : ℕ
p : α → Prop
v : Vector α n
i : ℕ
hi : i < v.toList.length
⊢ i < n

Tactic:
simp_all

Result:
no goals