harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem getValueCast!_insertEntryIfNew [BEq α] [LawfulBEq α] {l : List ((a : α) × β a)} {k a : α}
    {v : β k} [Inhabited (β a)] : getValueCast! a (insertEntryIfNew k v l) =
      if h : k == a ∧ containsKey k l = false then cast (congrArg β (eq_of_beq h.1)) v
      else getValueCast! a l

Proof state:
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : LawfulBEq α
l : List ((a : α) × β a)
k a : α
v : β k
inst✝ : Inhabited (β a)
⊢ getValueCast! a (insertEntryIfNew k v l) =
    if h : (k == a) = true ∧ containsKey k l = false then cast ⋯ v else getValueCast! a l

Tactic:
simp [getValueCast!_eq_getValueCast?, getValueCast?_insertEntryIfNew, apply_dite Option.get!]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/BinaryEntropy.lean
@[simp] lemma binEntropy_zero : binEntropy 0 = 0

Proof state:
⊢ binEntropy 0 = 0

Tactic:
simp [binEntropy]

Result:
no goals
-- Mathlib/Algebra/BigOperators/Finprod.lean
theorem finprod_eq_mulIndicator_apply (s : Set α) (f : α → M) (a : α) :
    ∏ᶠ _ : a ∈ s, f a = mulIndicator s f a

Proof state:
α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
s : Set α
f : α → M
a : α
⊢ ∏ᶠ (_ : a ∈ s), f a = s.mulIndicator f a

Tactic:
convert finprod_eq_if (M := M) (p := a ∈ s) (x := f a)

Result:
no goals

Proof state:
α : Type u_1
M : Type u_5
inst✝ : CommMonoid M
s : Set α
f : α → M
a : α
⊢ ∏ᶠ (_ : a ∈ s), f a = s.mulIndicator f a

Tactic:
classical convert finprod_eq_if (M := M) (p := a ∈ s) (x := f a)

Result:
no goals
-- Mathlib/Analysis/Convex/Function.lean
theorem LinearMap.concaveOn (f : E →ₗ[𝕜] β) {s : Set E} (hs : Convex 𝕜 s) : ConcaveOn 𝕜 s f :=
  ⟨hs, fun _ _ _ _ _ _ _ _ _ => by rw [f.map_add, f.map_smul, f.map_smul]⟩

Proof state:
𝕜 : Type u_1
E : Type u_2
β : Type u_5
inst✝⁴ : OrderedSemiring 𝕜
inst✝³ : AddCommMonoid E
inst✝² : OrderedAddCommMonoid β
inst✝¹ : Module 𝕜 E
inst✝ : Module 𝕜 β
f : E →ₗ[𝕜] β
s : Set E
hs : Convex 𝕜 s
x✝⁸ : E
x✝⁷ : x✝⁸ ∈ s
x✝⁶ : E
x✝⁵ : x✝⁶ ∈ s
x✝⁴ x✝³ : 𝕜
x✝² : 0 ≤ x✝⁴
x✝¹ : 0 ≤ x✝³
x✝ : x✝⁴ + x✝³ = 1
⊢ x✝⁴ • f x✝⁸ + x✝³ • f x✝⁶ ≤ f (x✝⁴ • x✝⁸ + x✝³ • x✝⁶)

Tactic:
rw [f.map_add, f.map_smul, f.map_smul]

Result:
no goals
-- Mathlib/Analysis/Normed/Group/Pointwise.lean
theorem singleton_div_closedBall : {x} / closedBall y δ = closedBall (x / y) δ

Proof state:
E : Type u_1
inst✝ : SeminormedCommGroup E
δ : ℝ
x y : E
⊢ {x} / closedBall y δ = closedBall (x / y) δ

Tactic:
simp_rw [div_eq_mul_inv, inv_closedBall, singleton_mul_closedBall]

Result:
no goals
-- Mathlib/LinearAlgebra/Orientation.lean
theorem eq_or_eq_neg [FiniteDimensional R M] (x₁ x₂ : Orientation R M ι)
    (h : Fintype.card ι = finrank R M) : x₁ = x₂ ∨ x₁ = -x₂

Proof state:
R : Type u_1
inst✝⁴ : LinearOrderedField R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
ι : Type u_3
inst✝¹ : Fintype ι
inst✝ : FiniteDimensional R M
x₁ x₂ : Orientation R M ι
h : Fintype.card ι = finrank R M
⊢ x₁ = x₂ ∨ x₁ = -x₂

Tactic:
have e := (finBasis R M).reindex (Fintype.equivFinOfCardEq h).symm

Result:
R : Type u_1
inst✝⁴ : LinearOrderedField R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
ι : Type u_3
inst✝¹ : Fintype ι
inst✝ : FiniteDimensional R M
x₁ x₂ : Orientation R M ι
h : Fintype.card ι = finrank R M
e : Basis ι R M
⊢ x₁ = x₂ ∨ x₁ = -x₂

Proof state:
R : Type u_1
inst✝⁴ : LinearOrderedField R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
ι : Type u_3
inst✝¹ : Fintype ι
inst✝ : FiniteDimensional R M
x₁ x₂ : Orientation R M ι
h : Fintype.card ι = finrank R M
e : Basis ι R M
this : DecidableEq ι := Classical.decEq ι
⊢ x₁ = x₂ ∨ x₁ = -x₂

Tactic:
have orientation_neg_neg :
    ∀ f : Basis ι R M, - -Basis.orientation f = Basis.orientation f := by simp

Result:
R : Type u_1
inst✝⁴ : LinearOrderedField R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
ι : Type u_3
inst✝¹ : Fintype ι
inst✝ : FiniteDimensional R M
x₁ x₂ : Orientation R M ι
h : Fintype.card ι = finrank R M
e : Basis ι R M
this : DecidableEq ι := Classical.decEq ι
orientation_neg_neg : ∀ (f : Basis ι R M), - -f.orientation = f.orientation
⊢ x₁ = x₂ ∨ x₁ = -x₂

Proof state:
R : Type u_1
inst✝⁴ : LinearOrderedField R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
ι : Type u_3
inst✝¹ : Fintype ι
inst✝ : FiniteDimensional R M
x₁ x₂ : Orientation R M ι
h : Fintype.card ι = finrank R M
e : Basis ι R M
this : DecidableEq ι := Classical.decEq ι
orientation_neg_neg : ∀ (f : Basis ι R M), - -f.orientation = f.orientation
⊢ x₁ = x₂ ∨ x₁ = -x₂

Tactic:
rcases e.orientation_eq_or_eq_neg x₁ with (h₁ | h₁) <;>
  rcases e.orientation_eq_or_eq_neg x₂ with (h₂ | h₂) <;> simp [h₁, h₂, orientation_neg_neg]

Result:
no goals

Proof state:
R : Type u_1
inst✝⁴ : LinearOrderedField R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
ι : Type u_3
inst✝¹ : Fintype ι
inst✝ : FiniteDimensional R M
x₁ x₂ : Orientation R M ι
h : Fintype.card ι = finrank R M
e : Basis ι R M
⊢ x₁ = x₂ ∨ x₁ = -x₂

Tactic:
letI := Classical.decEq ι

Result:
R : Type u_1
inst✝⁴ : LinearOrderedField R
M : Type u_2
inst✝³ : AddCommGroup M
inst✝² : Module R M
ι : Type u_3
inst✝¹ : Fintype ι
inst✝ : FiniteDimensional R M
x₁ x₂ : Orientation R M ι
h : Fintype.card ι = finrank R M
e : Basis ι R M
this : DecidableEq ι := Classical.decEq ι
⊢ x₁ = x₂ ∨ x₁ = -x₂
-- Mathlib/SetTheory/Cardinal/ENat.lean
@[simp] lemma ofENat_le_one {m : ℕ∞} : ofENat m ≤ 1 ↔ m ≤ 1

Proof state:
m : ℕ∞
⊢ ↑m ≤ 1 ↔ m ≤ 1

Tactic:
norm_cast

Result:
no goals
-- Mathlib/RingTheory/Ideal/Over.lean
theorem under_under : (𝔓.under B).under A  = 𝔓.under A

Proof state:
A : Type u_2
inst✝⁶ : CommSemiring A
B : Type u_3
inst✝⁵ : CommSemiring B
C : Type u_4
inst✝⁴ : Semiring C
inst✝³ : Algebra A B
inst✝² : Algebra B C
inst✝¹ : Algebra A C
inst✝ : IsScalarTower A B C
𝔓 : Ideal C
⊢ under A (under B 𝔓) = under A 𝔓

Tactic:
simp_rw [comap_comap, ← IsScalarTower.algebraMap_eq]

Result:
no goals
-- Mathlib/Order/Interval/Finset/SuccPred.lean
lemma Ioo_pred_left_eq_Ioc (a b : α) : Ioo (pred a) b = Ico a b := coe_injective <| by simp

Proof state:
α : Type u_1
inst✝³ : LinearOrder α
inst✝² : LocallyFiniteOrder α
inst✝¹ : PredOrder α
inst✝ : NoMinOrder α
a b : α
⊢ ↑(Ioo (pred a) b) = ↑(Ico a b)

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Angle.lean
theorem toReal_coe_eq_self_add_two_pi_iff {θ : ℝ} :
    (θ : Angle).toReal = θ + 2 * π ↔ θ ∈ Set.Ioc (-3 * π) (-π)

Proof state:
θ : ℝ
⊢ (↑θ).toReal = θ + 2 * π ↔ θ ∈ Set.Ioc (-3 * π) (-π)

Tactic:
convert @toReal_coe_eq_self_sub_two_mul_int_mul_pi_iff θ (-1) using 2 <;> norm_num

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/PropLemmas.lean
theorem ite_iff_ite (p : Prop) {h h' : Decidable p} (x y : Prop) :
    (@ite _ p h x y ↔ @ite _ p h' x y) ↔ True

Proof state:
p : Prop
h h' : Decidable p
x y : Prop
⊢ ((if p then x else y) ↔ if p then x else y) ↔ True

Tactic:
rw [iff_true]

Result:
p : Prop
h h' : Decidable p
x y : Prop
⊢ (if p then x else y) ↔ if p then x else y

Proof state:
p : Prop
h h' : Decidable p
x y : Prop
⊢ (if p then x else y) = if p then x else y

Tactic:
congr

Result:
no goals

Proof state:
p : Prop
h h' : Decidable p
x y : Prop
⊢ (if p then x else y) ↔ if p then x else y

Tactic:
suffices @ite _ p h x y = @ite _ p h' x y by simp [this]

Result:
p : Prop
h h' : Decidable p
x y : Prop
⊢ (if p then x else y) = if p then x else y

Proof state:
p : Prop
h h' : Decidable p
x y : Prop
this : (if p then x else y) = if p then x else y
⊢ (if p then x else y) ↔ if p then x else y

Tactic:
simp [this]

Result:
no goals
-- Mathlib/Topology/Algebra/Module/StrongTopology.lean
theorem isUniformEmbedding_restrictScalars :
    IsUniformEmbedding (restrictScalars 𝕜' : (E →L[𝕜] F) → (E →L[𝕜'] F))

Proof state:
case h.e'_4.h.e'_4.h.e'_2.h.a
𝕜 : Type u_1
inst✝¹⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹³ : AddCommGroup E
inst✝¹² : TopologicalSpace E
inst✝¹¹ : Module 𝕜 E
inst✝¹⁰ : ContinuousSMul 𝕜 E
F : Type u_3
inst✝⁹ : AddCommGroup F
inst✝⁸ : UniformSpace F
inst✝⁷ : UniformAddGroup F
inst✝⁶ : Module 𝕜 F
𝕜' : Type u_4
inst✝⁵ : NontriviallyNormedField 𝕜'
inst✝⁴ : NormedAlgebra 𝕜' 𝕜
inst✝³ : Module 𝕜' E
inst✝² : IsScalarTower 𝕜' 𝕜 E
inst✝¹ : Module 𝕜' F
inst✝ : IsScalarTower 𝕜' 𝕜 F
s : Set E
⊢ IsVonNBounded 𝕜' s ↔ IsVonNBounded 𝕜 s

Tactic:
exact ⟨fun h ↦ h.extend_scalars _, fun h ↦ h.restrict_scalars _⟩

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝¹⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹³ : AddCommGroup E
inst✝¹² : TopologicalSpace E
inst✝¹¹ : Module 𝕜 E
inst✝¹⁰ : ContinuousSMul 𝕜 E
F : Type u_3
inst✝⁹ : AddCommGroup F
inst✝⁸ : UniformSpace F
inst✝⁷ : UniformAddGroup F
inst✝⁶ : Module 𝕜 F
𝕜' : Type u_4
inst✝⁵ : NontriviallyNormedField 𝕜'
inst✝⁴ : NormedAlgebra 𝕜' 𝕜
inst✝³ : Module 𝕜' E
inst✝² : IsScalarTower 𝕜' 𝕜 E
inst✝¹ : Module 𝕜' F
inst✝ : IsScalarTower 𝕜' 𝕜 F
⊢ IsUniformEmbedding ((fun f => (UniformOnFun.ofFun {s | IsVonNBounded 𝕜' s}) ⇑f) ∘ restrictScalars 𝕜')

Tactic:
convert isUniformEmbedding_toUniformOnFun using 4 with s

Result:
case h.e'_4.h.e'_4.h.e'_2.h.a
𝕜 : Type u_1
inst✝¹⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹³ : AddCommGroup E
inst✝¹² : TopologicalSpace E
inst✝¹¹ : Module 𝕜 E
inst✝¹⁰ : ContinuousSMul 𝕜 E
F : Type u_3
inst✝⁹ : AddCommGroup F
inst✝⁸ : UniformSpace F
inst✝⁷ : UniformAddGroup F
inst✝⁶ : Module 𝕜 F
𝕜' : Type u_4
inst✝⁵ : NontriviallyNormedField 𝕜'
inst✝⁴ : NormedAlgebra 𝕜' 𝕜
inst✝³ : Module 𝕜' E
inst✝² : IsScalarTower 𝕜' 𝕜 E
inst✝¹ : Module 𝕜' F
inst✝ : IsScalarTower 𝕜' 𝕜 F
s : Set E
⊢ IsVonNBounded 𝕜' s ↔ IsVonNBounded 𝕜 s

Proof state:
𝕜 : Type u_1
inst✝¹⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹³ : AddCommGroup E
inst✝¹² : TopologicalSpace E
inst✝¹¹ : Module 𝕜 E
inst✝¹⁰ : ContinuousSMul 𝕜 E
F : Type u_3
inst✝⁹ : AddCommGroup F
inst✝⁸ : UniformSpace F
inst✝⁷ : UniformAddGroup F
inst✝⁶ : Module 𝕜 F
𝕜' : Type u_4
inst✝⁵ : NontriviallyNormedField 𝕜'
inst✝⁴ : NormedAlgebra 𝕜' 𝕜
inst✝³ : Module 𝕜' E
inst✝² : IsScalarTower 𝕜' 𝕜 E
inst✝¹ : Module 𝕜' F
inst✝ : IsScalarTower 𝕜' 𝕜 F
⊢ IsUniformEmbedding (restrictScalars 𝕜')

Tactic:
rw [← isUniformEmbedding_toUniformOnFun.of_comp_iff]

Result:
𝕜 : Type u_1
inst✝¹⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝¹³ : AddCommGroup E
inst✝¹² : TopologicalSpace E
inst✝¹¹ : Module 𝕜 E
inst✝¹⁰ : ContinuousSMul 𝕜 E
F : Type u_3
inst✝⁹ : AddCommGroup F
inst✝⁸ : UniformSpace F
inst✝⁷ : UniformAddGroup F
inst✝⁶ : Module 𝕜 F
𝕜' : Type u_4
inst✝⁵ : NontriviallyNormedField 𝕜'
inst✝⁴ : NormedAlgebra 𝕜' 𝕜
inst✝³ : Module 𝕜' E
inst✝² : IsScalarTower 𝕜' 𝕜 E
inst✝¹ : Module 𝕜' F
inst✝ : IsScalarTower 𝕜' 𝕜 F
⊢ IsUniformEmbedding ((fun f => (UniformOnFun.ofFun {s | IsVonNBounded 𝕜' s}) ⇑f) ∘ restrictScalars 𝕜')
-- Mathlib/Data/List/Rotate.lean
theorem isRotated_reverse_comm_iff : l.reverse ~r l' ↔ l ~r l'.reverse

Proof state:
case mpr
α : Type u
l l' : List α
⊢ l ~r l'.reverse → l.reverse ~r l'

Tactic:
intro h

Result:
case mpr
α : Type u
l l' : List α
h : l ~r l'.reverse
⊢ l.reverse ~r l'

Proof state:
case mpr
α : Type u
l l' : List α
h : l ~r l'.reverse
⊢ l.reverse ~r l'

Tactic:
simpa using h.reverse

Result:
no goals
-- Mathlib/Data/Finsupp/Weight.lean
lemma degree_eq_zero_iff {R : Type*} [OrderedAddCommMonoid R] [CanonicallyOrderedAdd R]
    (d : σ →₀ R) :
    degree d = 0 ↔ d = 0

Proof state:
σ : Type u_1
R : Type u_5
inst✝¹ : OrderedAddCommMonoid R
inst✝ : CanonicallyOrderedAdd R
d : σ →₀ R
⊢ d.degree = 0 ↔ d = 0

Tactic:
simp only [degree, Finset.sum_eq_zero_iff, mem_support_iff, ne_eq, _root_.not_imp_self,
  DFunLike.ext_iff, coe_zero, Pi.zero_apply]

Result:
no goals
-- Mathlib/Order/WellQuasiOrder.lean
theorem wellQuasiOrderedLE_iff_wellFoundedLT : WellQuasiOrderedLE α ↔ WellFoundedLT α

Proof state:
α : Type u_1
inst✝ : LinearOrder α
⊢ WellFoundedLT α → ∀ (s : Set α), IsAntichain (fun x1 x2 => x1 ≤ x2) s → s.Finite

Tactic:
exact fun _ s hs ↦ hs.subsingleton.finite

Result:
no goals

Proof state:
α : Type u_1
inst✝ : LinearOrder α
⊢ WellQuasiOrderedLE α ↔ WellFoundedLT α

Tactic:
rw [wellQuasiOrderedLE_iff, and_iff_left_iff_imp]

Result:
α : Type u_1
inst✝ : LinearOrder α
⊢ WellFoundedLT α → ∀ (s : Set α), IsAntichain (fun x1 x2 => x1 ≤ x2) s → s.Finite
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem toList_filter (p : α → Bool) (l : Array α) :
    (l.filter p).toList = l.toList.filter p

Proof state:
α : Type u_1
p : α → Bool
l : Array α
⊢ (filter p l).toList = List.filter p l.toList

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Homology/HomotopyCategory/Pretriangulated.lean
lemma rotate_distinguished_triangle (T : Triangle (HomotopyCategory C (ComplexShape.up ℤ))) :
    T ∈ distinguishedTriangles C ↔ T.rotate ∈ distinguishedTriangles C

Proof state:
case mpr
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasBinaryBiproducts C
T : Triangle (HomotopyCategory C (ComplexShape.up ℤ))
hT : T.rotate ∈ distinguishedTriangles C
⊢ T ∈ distinguishedTriangles C

Tactic:
exact isomorphic_distinguished _ (invRotate_distinguished_triangle' T.rotate hT) _
  ((triangleRotation _).unitIso.app T)

Result:
no goals

Proof state:
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasBinaryBiproducts C
T : Triangle (HomotopyCategory C (ComplexShape.up ℤ))
⊢ T ∈ distinguishedTriangles C ↔ T.rotate ∈ distinguishedTriangles C

Tactic:
constructor

Result:
case mp
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasBinaryBiproducts C
T : Triangle (HomotopyCategory C (ComplexShape.up ℤ))
⊢ T ∈ distinguishedTriangles C → T.rotate ∈ distinguishedTriangles C

case mpr
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasBinaryBiproducts C
T : Triangle (HomotopyCategory C (ComplexShape.up ℤ))
⊢ T.rotate ∈ distinguishedTriangles C → T ∈ distinguishedTriangles C

Proof state:
case mp
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasBinaryBiproducts C
T : Triangle (HomotopyCategory C (ComplexShape.up ℤ))
⊢ T ∈ distinguishedTriangles C → T.rotate ∈ distinguishedTriangles C

Tactic:
exact rotate_distinguished_triangle' T

Result:
no goals

Proof state:
case mpr
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasBinaryBiproducts C
T : Triangle (HomotopyCategory C (ComplexShape.up ℤ))
⊢ T.rotate ∈ distinguishedTriangles C → T ∈ distinguishedTriangles C

Tactic:
intro hT

Result:
case mpr
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasBinaryBiproducts C
T : Triangle (HomotopyCategory C (ComplexShape.up ℤ))
hT : T.rotate ∈ distinguishedTriangles C
⊢ T ∈ distinguishedTriangles C
-- Mathlib/MeasureTheory/Measure/Map.lean
@[simp] lemma map_eq_zero_iff (hf : AEMeasurable f μ) : μ.map f = 0 ↔ μ = 0

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
f : α → β
hf : AEMeasurable f μ
⊢ map f μ = 0 ↔ μ = 0

Tactic:
simp_rw [← measure_univ_eq_zero, map_apply_of_aemeasurable hf .univ, preimage_univ]

Result:
no goals
-- Mathlib/Data/Set/Image.lean
theorem preimage_singleton_false (p : α → Prop) : p ⁻¹' {False} = {a | ¬p a}

Proof state:
α : Type u_1
p : α → Prop
⊢ p ⁻¹' {False} = {a | ¬p a}

Tactic:
ext

Result:
case h
α : Type u_1
p : α → Prop
x✝ : α
⊢ x✝ ∈ p ⁻¹' {False} ↔ x✝ ∈ {a | ¬p a}

Proof state:
case h
α : Type u_1
p : α → Prop
x✝ : α
⊢ x✝ ∈ p ⁻¹' {False} ↔ x✝ ∈ {a | ¬p a}

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Grind/Offset.lean
theorem Nat.unsat_lo_lo (u v k₁ k₂ : Nat) : isLt 0 (k₁+k₂) = true → u + k₁ ≤ v → v + k₂ ≤ u → False

Proof state:
u v k₁ k₂ : Nat
⊢ isLt 0 (k₁ + k₂) = true → u + k₁ ≤ v → v + k₂ ≤ u → False

Tactic:
simp [isLt]

Result:
u v k₁ k₂ : Nat
⊢ 0 < k₁ + k₂ → u + k₁ ≤ v → u < v + k₂

Proof state:
u v k₁ k₂ : Nat
⊢ 0 < k₁ + k₂ → u + k₁ ≤ v → u < v + k₂

Tactic:
omega

Result:
no goals
-- Mathlib/Analysis/Convex/Gauge.lean
theorem gauge_zero : gauge s 0 = 0

Proof state:
case pos
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : Set E
h : 0 ∈ s
⊢ sInf {r | r ∈ Ioi 0 ∧ r⁻¹ • 0 ∈ s} = 0

Tactic:
simp only [smul_zero, sep_true, h, csInf_Ioi]

Result:
no goals

Proof state:
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : Set E
⊢ gauge s 0 = 0

Tactic:
rw [gauge_def']

Result:
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : Set E
⊢ sInf {r | r ∈ Ioi 0 ∧ r⁻¹ • 0 ∈ s} = 0

Proof state:
case neg
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : Set E
h : 0 ∉ s
⊢ sInf {r | r ∈ Ioi 0 ∧ r⁻¹ • 0 ∈ s} = 0

Tactic:
simp only [smul_zero, sep_false, h, Real.sInf_empty]

Result:
no goals

Proof state:
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : Set E
⊢ sInf {r | r ∈ Ioi 0 ∧ r⁻¹ • 0 ∈ s} = 0

Tactic:
by_cases h : (0 : E) ∈ s

Result:
case pos
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : Set E
h : 0 ∈ s
⊢ sInf {r | r ∈ Ioi 0 ∧ r⁻¹ • 0 ∈ s} = 0

case neg
E : Type u_2
inst✝¹ : AddCommGroup E
inst✝ : Module ℝ E
s : Set E
h : 0 ∉ s
⊢ sInf {r | r ∈ Ioi 0 ∧ r⁻¹ • 0 ∈ s} = 0
-- Mathlib/MeasureTheory/Function/L1Space/Integrable.lean
/-- If `f` is `ℝ`-valued and integrable, then for any `c > 0` the set `{x | f x ≥ c}` has finite
measure. -/
lemma Integrable.measure_ge_lt_top {f : α → ℝ} (hf : Integrable f μ) {ε : ℝ} (ε_pos : 0 < ε) :
    μ {a : α | ε ≤ f a} < ∞

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
ε : ℝ
ε_pos : 0 < ε
⊢ μ {a | ε ≤ f a} < ⊤

Tactic:
refine lt_of_le_of_lt (measure_mono ?_) (hf.measure_norm_ge_lt_top ε_pos)

Result:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
ε : ℝ
ε_pos : 0 < ε
⊢ {a | ε ≤ f a} ⊆ {x | ε ≤ ‖f x‖}

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
ε : ℝ
ε_pos : 0 < ε
x : α
hx : x ∈ {a | ε ≤ f a}
⊢ x ∈ {x | ε ≤ ‖f x‖}

Tactic:
simp only [Real.norm_eq_abs, Set.mem_setOf_eq] at hx ⊢

Result:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
ε : ℝ
ε_pos : 0 < ε
x : α
hx : ε ≤ f x
⊢ ε ≤ |f x|

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
ε : ℝ
ε_pos : 0 < ε
⊢ {a | ε ≤ f a} ⊆ {x | ε ≤ ‖f x‖}

Tactic:
intro x hx

Result:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
ε : ℝ
ε_pos : 0 < ε
x : α
hx : x ∈ {a | ε ≤ f a}
⊢ x ∈ {x | ε ≤ ‖f x‖}

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
ε : ℝ
ε_pos : 0 < ε
x : α
hx : ε ≤ f x
⊢ ε ≤ |f x|

Tactic:
exact hx.trans (le_abs_self _)

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian.lean
lemma negY_smul (P : Fin 3 → R) (u : R) : W'.negY (u • P) = u ^ 3 * W'.negY P

Proof state:
R : Type r
inst✝ : CommRing R
W' : Jacobian R
P : Fin 3 → R
u : R
⊢ -(u ^ 3 * P y) - W'.a₁ * (u ^ 2 * P x) * (u * P z) - W'.a₃ * (u * P z) ^ 3 =
    u ^ 3 * (-P y - W'.a₁ * P x * P z - W'.a₃ * P z ^ 3)

Tactic:
ring1

Result:
no goals

Proof state:
R : Type r
inst✝ : CommRing R
W' : Jacobian R
P : Fin 3 → R
u : R
⊢ W'.negY (u • P) = u ^ 3 * W'.negY P

Tactic:
simp only [negY, smul_fin3_ext]

Result:
R : Type r
inst✝ : CommRing R
W' : Jacobian R
P : Fin 3 → R
u : R
⊢ -(u ^ 3 * P y) - W'.a₁ * (u ^ 2 * P x) * (u * P z) - W'.a₃ * (u * P z) ^ 3 =
    u ^ 3 * (-P y - W'.a₁ * P x * P z - W'.a₃ * P z ^ 3)
-- Mathlib/Data/Finset/NoncommProd.lean
theorem noncommFold_cons (s : Multiset α) (a : α) (h h') (x : α) :
    noncommFold op (a ::ₘ s) h x = op a (noncommFold op s h' x)

Proof state:
case h
α : Type u_3
op : α → α → α
assoc : Std.Associative op
a x : α
a✝ : List α
h : {x | x ∈ a ::ₘ ⟦a✝⟧}.Pairwise fun x y => op x y = op y x
h' : {x | x ∈ ⟦a✝⟧}.Pairwise fun x y => op x y = op y x
⊢ noncommFold op (a ::ₘ ⟦a✝⟧) h x = op a (noncommFold op ⟦a✝⟧ h' x)

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_3
op : α → α → α
assoc : Std.Associative op
s : Multiset α
a : α
h : {x | x ∈ a ::ₘ s}.Pairwise fun x y => op x y = op y x
h' : {x | x ∈ s}.Pairwise fun x y => op x y = op y x
x : α
⊢ noncommFold op (a ::ₘ s) h x = op a (noncommFold op s h' x)

Tactic:
induction s using Quotient.inductionOn

Result:
case h
α : Type u_3
op : α → α → α
assoc : Std.Associative op
a x : α
a✝ : List α
h : {x | x ∈ a ::ₘ ⟦a✝⟧}.Pairwise fun x y => op x y = op y x
h' : {x | x ∈ ⟦a✝⟧}.Pairwise fun x y => op x y = op y x
⊢ noncommFold op (a ::ₘ ⟦a✝⟧) h x = op a (noncommFold op ⟦a✝⟧ h' x)
-- Mathlib/Geometry/Euclidean/PerpBisector.lean
theorem mem_perpBisector_iff_inner_eq_inner :
    c ∈ perpBisector p₁ p₂ ↔ ⟪c -ᵥ p₁, p₂ -ᵥ p₁⟫ = ⟪c -ᵥ p₂, p₁ -ᵥ p₂⟫

Proof state:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
c p₁ p₂ : P
⊢ inner (c -ᵥ p₁ + (c -ᵥ p₂)) (p₂ -ᵥ p₁) = 0 ↔ 2⁻¹ * inner (c -ᵥ p₁ + (c -ᵥ p₂)) (p₂ -ᵥ p₁) = 0

Tactic:
simp

Result:
no goals

Proof state:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
c p₁ p₂ : P
⊢ c ∈ perpBisector p₁ p₂ ↔ inner (c -ᵥ p₁) (p₂ -ᵥ p₁) = inner (c -ᵥ p₂) (p₁ -ᵥ p₂)

Tactic:
rw [Iff.comm, mem_perpBisector_iff_inner_eq_zero, ← add_neg_eq_zero, ← inner_neg_right,
  neg_vsub_eq_vsub_rev, ← inner_add_left, vsub_midpoint, invOf_eq_inv, ← smul_add,
  real_inner_smul_left]

Result:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
c p₁ p₂ : P
⊢ inner (c -ᵥ p₁ + (c -ᵥ p₂)) (p₂ -ᵥ p₁) = 0 ↔ 2⁻¹ * inner (c -ᵥ p₁ + (c -ᵥ p₂)) (p₂ -ᵥ p₁) = 0
-- Mathlib/Topology/Instances/ENNReal/Lemmas.lean
theorem lt_top_of_tsum_ne_top {a : α → ℝ≥0∞} (tsum_ne_top : ∑' i, a i ≠ ∞) (j : α) :
    a j < ∞

Proof state:
α : Type u_1
a : α → ℝ≥0∞
j : α
h : ⊤ ≤ a j
⊢ ∑' (i : α), a i = ⊤

Tactic:
exact ENNReal.tsum_eq_top_of_eq_top ⟨j, top_unique h⟩

Result:
no goals

Proof state:
α : Type u_1
a : α → ℝ≥0∞
tsum_ne_top : ∑' (i : α), a i ≠ ⊤
j : α
⊢ a j < ⊤

Tactic:
contrapose! tsum_ne_top with h

Result:
α : Type u_1
a : α → ℝ≥0∞
j : α
h : ⊤ ≤ a j
⊢ ∑' (i : α), a i = ⊤
-- Mathlib/Analysis/SpecialFunctions/Pow/NNReal.lean
theorem eq_rpow_inv_iff {x y : ℝ≥0} {z : ℝ} (hz : z ≠ 0) : x = y ^ z⁻¹ ↔ x ^ z = y

Proof state:
x y : ℝ≥0
z : ℝ
hz : z ≠ 0
⊢ x = y ^ z⁻¹ ↔ x ^ z = y

Tactic:
rw [← rpow_eq_rpow_iff hz, ← one_div, rpow_self_rpow_inv hz]

Result:
no goals
-- Mathlib/Analysis/Calculus/LogDeriv.lean
theorem logDeriv_mul {f g : 𝕜 → 𝕜'} (x : 𝕜) (hf : f x ≠ 0) (hg : g x ≠ 0)
    (hdf : DifferentiableAt 𝕜 f x) (hdg : DifferentiableAt 𝕜 g x) :
      logDeriv (fun z => f z * g z) x = logDeriv f x + logDeriv g x

Proof state:
𝕜 : Type u_1
𝕜' : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
f g : 𝕜 → 𝕜'
x : 𝕜
hf : f x ≠ 0
hg : g x ≠ 0
hdf : DifferentiableAt 𝕜 f x
hdg : DifferentiableAt 𝕜 g x
⊢ (deriv f x * g x + f x * deriv g x) / (f x * g x) = deriv f x / f x + deriv g x / g x

Tactic:
field_simp [mul_comm]

Result:
no goals

Proof state:
𝕜 : Type u_1
𝕜' : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
f g : 𝕜 → 𝕜'
x : 𝕜
hf : f x ≠ 0
hg : g x ≠ 0
hdf : DifferentiableAt 𝕜 f x
hdg : DifferentiableAt 𝕜 g x
⊢ logDeriv (fun z => f z * g z) x = logDeriv f x + logDeriv g x

Tactic:
simp only [logDeriv_apply, deriv_mul hdf hdg]

Result:
𝕜 : Type u_1
𝕜' : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NontriviallyNormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
f g : 𝕜 → 𝕜'
x : 𝕜
hf : f x ≠ 0
hg : g x ≠ 0
hdf : DifferentiableAt 𝕜 f x
hdg : DifferentiableAt 𝕜 g x
⊢ (deriv f x * g x + f x * deriv g x) / (f x * g x) = deriv f x / f x + deriv g x / g x
-- Mathlib/Algebra/Module/LinearMap/Polynomial.lean
lemma toMvPolynomial_eval_eq_apply (M : Matrix m n R) (i : m) (c : n → R) :
    eval c (M.toMvPolynomial i) = (M *ᵥ c) i

Proof state:
m : Type u_1
n : Type u_2
R : Type u_4
inst✝¹ : Fintype n
inst✝ : CommSemiring R
M : Matrix m n R
i : m
c : n → R
⊢ (eval c) (M.toMvPolynomial i) = (M *ᵥ c) i

Tactic:
simp only [toMvPolynomial, map_sum, eval_monomial, pow_zero, Finsupp.prod_single_index, pow_one,
  mulVec, dotProduct]

Result:
no goals