harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Topology/Compactness/DeltaGeneratedSpace.lean
/-- `deltaGenerated` is idempotent as a function `TopologicalSpace X → TopologicalSpace X`. -/
lemma deltaGenerated_deltaGenerated_eq :
    @deltaGenerated X (deltaGenerated X) = deltaGenerated X

Proof state:
X : Type u_1
tX : TopologicalSpace X
⊢ deltaGenerated X = deltaGenerated X

Tactic:
ext u

Result:
case a.h.a
X : Type u_1
tX : TopologicalSpace X
u : Set X
⊢ IsOpen u ↔ IsOpen u

Proof state:
case a.h.a
X : Type u_1
tX : TopologicalSpace X
u : Set X
⊢ IsOpen u ↔ IsOpen u

Tactic:
simp_rw [isOpen_deltaGenerated_iff]

Result:
case a.h.a
X : Type u_1
tX : TopologicalSpace X
u : Set X
⊢ (∀ (n : ℕ) (p : C(Fin n → ℝ, X)), IsOpen (⇑p ⁻¹' u)) ↔ ∀ (n : ℕ) (p : C(Fin n → ℝ, X)), IsOpen (⇑p ⁻¹' u)

Proof state:
case a.h.a.refine_2
X : Type u_1
tX : TopologicalSpace X
u : Set X
n : ℕ
h : ∀ (p : C(Fin n → ℝ, X)), IsOpen (⇑p ⁻¹' u)
p : C(Fin n → ℝ, X)
⊢ Continuous ⇑p

Tactic:
exact continuous_euclidean_to_deltaGenerated.mp <| @ContinuousMap.continuous_toFun _ _ _ (_) p

Result:
no goals

Proof state:
case a.h.a
X : Type u_1
tX : TopologicalSpace X
u : Set X
n : ℕ
⊢ (∀ (p : C(Fin n → ℝ, X)), IsOpen (⇑p ⁻¹' u)) ↔ ∀ (p : C(Fin n → ℝ, X)), IsOpen (⇑p ⁻¹' u)

Tactic:
refine ⟨fun h p ↦ h <| @ContinuousMap.mk _ _ _ (_) p ?_, fun h p ↦ h ⟨p, ?_⟩⟩

Result:
case a.h.a.refine_1
X : Type u_1
tX : TopologicalSpace X
u : Set X
n : ℕ
h : ∀ (p : C(Fin n → ℝ, X)), IsOpen (⇑p ⁻¹' u)
p : C(Fin n → ℝ, X)
⊢ Continuous ⇑p

case a.h.a.refine_2
X : Type u_1
tX : TopologicalSpace X
u : Set X
n : ℕ
h : ∀ (p : C(Fin n → ℝ, X)), IsOpen (⇑p ⁻¹' u)
p : C(Fin n → ℝ, X)
⊢ Continuous ⇑p

Proof state:
case a.h.a.refine_1
X : Type u_1
tX : TopologicalSpace X
u : Set X
n : ℕ
h : ∀ (p : C(Fin n → ℝ, X)), IsOpen (⇑p ⁻¹' u)
p : C(Fin n → ℝ, X)
⊢ Continuous ⇑p

Tactic:
exact continuous_euclidean_to_deltaGenerated.mpr p.2

Result:
no goals

Proof state:
case a.h.a
X : Type u_1
tX : TopologicalSpace X
u : Set X
⊢ (∀ (n : ℕ) (p : C(Fin n → ℝ, X)), IsOpen (⇑p ⁻¹' u)) ↔ ∀ (n : ℕ) (p : C(Fin n → ℝ, X)), IsOpen (⇑p ⁻¹' u)

Tactic:
refine forall_congr' fun n ↦ ?_

Result:
case a.h.a
X : Type u_1
tX : TopologicalSpace X
u : Set X
n : ℕ
⊢ (∀ (p : C(Fin n → ℝ, X)), IsOpen (⇑p ⁻¹' u)) ↔ ∀ (p : C(Fin n → ℝ, X)), IsOpen (⇑p ⁻¹' u)
-- Mathlib/Analysis/Calculus/FDeriv/Mul.lean
theorem HasStrictFDerivAt.finset_prod [DecidableEq ι] {x : E}
    (hg : ∀ i ∈ u, HasStrictFDerivAt (g i) (g' i) x) :
    HasStrictFDerivAt (∏ i ∈ u, g i ·) (∑ i ∈ u, (∏ j ∈ u.erase i, g j x) • g' i) x

Proof state:
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
ι : Type u_5
𝔸' : Type u_7
inst✝² : NormedCommRing 𝔸'
inst✝¹ : NormedAlgebra 𝕜 𝔸'
u : Finset ι
g : ι → E → 𝔸'
g' : ι → E →L[𝕜] 𝔸'
inst✝ : DecidableEq ι
x : E
hg : ∀ i ∈ u, HasStrictFDerivAt (g i) (g' i) x
⊢ (∑ i ∈ u.attach, (∏ j ∈ u.attach.erase i, g (↑j) x) • proj i).comp (pi fun i => g' ↑i) =
    ∑ i ∈ u, (∏ j ∈ u.erase i, g j x) • g' i

Tactic:
ext

Result:
case h
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
ι : Type u_5
𝔸' : Type u_7
inst✝² : NormedCommRing 𝔸'
inst✝¹ : NormedAlgebra 𝕜 𝔸'
u : Finset ι
g : ι → E → 𝔸'
g' : ι → E →L[𝕜] 𝔸'
inst✝ : DecidableEq ι
x : E
hg : ∀ i ∈ u, HasStrictFDerivAt (g i) (g' i) x
x✝ : E
⊢ ((∑ i ∈ u.attach, (∏ j ∈ u.attach.erase i, g (↑j) x) • proj i).comp (pi fun i => g' ↑i)) x✝ =
    (∑ i ∈ u, (∏ j ∈ u.erase i, g j x) • g' i) x✝
-- Mathlib/Data/Finset/Max.lean
theorem toDual_max' {s : Finset α} (hs : s.Nonempty) :
    toDual (max' s hs) = min' (s.image toDual) (hs.image _)

Proof state:
α : Type u_2
inst✝ : LinearOrder α
s : Finset α
hs : s.Nonempty
⊢ s.inf (WithTop.some ∘ fun x => toDual x) = s.inf ((WithTop.some ∘ fun x => x) ∘ ⇑toDual)

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_2
inst✝ : LinearOrder α
s : Finset α
hs : s.Nonempty
⊢ ↑(toDual (s.max' hs)) = ↑((image (⇑toDual) s).min' ⋯)

Tactic:
simp only [max'_eq_sup', id_eq, toDual_sup', Function.comp_apply, coe_inf', min'_eq_inf',
  inf_image]

Result:
α : Type u_2
inst✝ : LinearOrder α
s : Finset α
hs : s.Nonempty
⊢ s.inf (WithTop.some ∘ fun x => toDual x) = s.inf ((WithTop.some ∘ fun x => x) ∘ ⇑toDual)

Proof state:
α : Type u_2
inst✝ : LinearOrder α
s : Finset α
hs : s.Nonempty
⊢ toDual (s.max' hs) = (image (⇑toDual) s).min' ⋯

Tactic:
rw [← WithTop.coe_eq_coe]

Result:
α : Type u_2
inst✝ : LinearOrder α
s : Finset α
hs : s.Nonempty
⊢ ↑(toDual (s.max' hs)) = ↑((image (⇑toDual) s).min' ⋯)
-- Mathlib/Data/List/Permutation.lean
theorem permutations_nil : permutations ([] : List α) = [[]]

Proof state:
α : Type u_1
⊢ [].permutations = [[]]

Tactic:
rw [permutations, permutationsAux_nil]

Result:
no goals
-- Mathlib/NumberTheory/ArithmeticFunction.lean
theorem cardDistinctFactors_eq_cardFactors_iff_squarefree {n : ℕ} (h0 : n ≠ 0) :
    ω n = Ω n ↔ Squarefree n

Proof state:
n : ℕ
h0 : n ≠ 0
⊢ n.primeFactorsList.dedup.length = Ω n ↔ n.primeFactorsList.Nodup

Tactic:
constructor <;> intro h

Result:
case mp
n : ℕ
h0 : n ≠ 0
h : n.primeFactorsList.dedup.length = Ω n
⊢ n.primeFactorsList.Nodup

case mpr
n : ℕ
h0 : n ≠ 0
h : n.primeFactorsList.Nodup
⊢ n.primeFactorsList.dedup.length = Ω n

Proof state:
case mp
n : ℕ
h0 : n ≠ 0
h : n.primeFactorsList.dedup.length = Ω n
⊢ n.primeFactorsList.dedup.Nodup

Tactic:
apply List.nodup_dedup

Result:
no goals

Proof state:
case mpr
n : ℕ
h0 : n ≠ 0
h : n.primeFactorsList.Nodup
⊢ n.primeFactorsList.dedup.length = Ω n

Tactic:
rw [h.dedup]

Result:
case mpr
n : ℕ
h0 : n ≠ 0
h : n.primeFactorsList.Nodup
⊢ n.primeFactorsList.length = Ω n

Proof state:
case mp
n : ℕ
h0 : n ≠ 0
h : n.primeFactorsList.dedup.length = Ω n
⊢ n.primeFactorsList.Nodup

Tactic:
rw [← n.primeFactorsList.dedup_sublist.eq_of_length h]

Result:
case mp
n : ℕ
h0 : n ≠ 0
h : n.primeFactorsList.dedup.length = Ω n
⊢ n.primeFactorsList.dedup.Nodup

Proof state:
n : ℕ
h0 : n ≠ 0
⊢ ω n = Ω n ↔ Squarefree n

Tactic:
rw [squarefree_iff_nodup_primeFactorsList h0, cardDistinctFactors_apply]

Result:
n : ℕ
h0 : n ≠ 0
⊢ n.primeFactorsList.dedup.length = Ω n ↔ n.primeFactorsList.Nodup

Proof state:
case mpr
n : ℕ
h0 : n ≠ 0
h : n.primeFactorsList.Nodup
⊢ n.primeFactorsList.length = Ω n

Tactic:
rfl

Result:
no goals
-- Mathlib/Algebra/RingQuot.lean
theorem one_quot : (⟨Quot.mk _ 1⟩ : RingQuot r) = 1 :=
  show _ = one r by rw [one_def]

Proof state:
R : Type uR
inst✝ : Semiring R
r : R → R → Prop
⊢ { toQuot := Quot.mk (Rel r) 1 } = RingQuot.one r

Tactic:
rw [one_def]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Typeclasses.lean
theorem Measure.smul_finite (μ : Measure α) [IsFiniteMeasure μ] {c : ℝ≥0∞} (hc : c ≠ ∞) :
    IsFiniteMeasure (c • μ)

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
c : ℝ≥0∞
hc : c ≠ ⊤
⊢ IsFiniteMeasure (c • μ)

Tactic:
lift c to ℝ≥0 using hc

Result:
case intro
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
c : ℝ≥0
⊢ IsFiniteMeasure (↑c • μ)

Proof state:
case intro
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
inst✝ : IsFiniteMeasure μ
c : ℝ≥0
⊢ IsFiniteMeasure (↑c • μ)

Tactic:
exact MeasureTheory.isFiniteMeasureSMulNNReal

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Basic.lean
theorem sq_cos_pi_div_six : cos (π / 6) ^ 2 = 3 / 4

Proof state:
⊢ cos (π / 6) ^ 2 = 3 / 4

Tactic:
rw [cos_pi_div_six, div_pow, sq_sqrt] <;> norm_num

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/PairingHeap.lean
theorem Heap.noSibling_tail? {s : Heap α} : s.tail? le = some s' →
    s'.NoSibling

Proof state:
α : Type u_1
le : α → α → Bool
s' s : Heap α
eq : Option.map (fun x => x.snd) (deleteMin le s) = some s'
⊢ s'.NoSibling

Tactic:
match eq₂ : s.deleteMin le, eq with
| some (a, tl), rfl => exact noSibling_deleteMin eq₂

Result:
no goals

Proof state:
α : Type u_1
le : α → α → Bool
s' s : Heap α
eq : Option.map (fun x => x.snd) (deleteMin le s) = some s'
a : α
tl : Heap α
eq₂ : deleteMin le s = some (a, tl)
⊢ ((fun x => x.snd) (a, tl)).NoSibling

Tactic:
exact noSibling_deleteMin eq₂

Result:
no goals

Proof state:
α : Type u_1
le : α → α → Bool
s' s : Heap α
⊢ tail? le s = some s' → s'.NoSibling

Tactic:
simp only [Heap.tail?]

Result:
α : Type u_1
le : α → α → Bool
s' s : Heap α
⊢ Option.map (fun x => x.snd) (deleteMin le s) = some s' → s'.NoSibling

Proof state:
α : Type u_1
le : α → α → Bool
s' s : Heap α
⊢ Option.map (fun x => x.snd) (deleteMin le s) = some s' → s'.NoSibling

Tactic:
intro eq

Result:
α : Type u_1
le : α → α → Bool
s' s : Heap α
eq : Option.map (fun x => x.snd) (deleteMin le s) = some s'
⊢ s'.NoSibling
-- Mathlib/SetTheory/Cardinal/Basic.lean
theorem lift_sInf (s : Set Cardinal) : lift.{u, v} (sInf s) = sInf (lift.{u, v} '' s)

Proof state:
case inl

⊢ lift.{u, v} (sInf ∅) = sInf (lift.{u, v} '' ∅)

Tactic:
simp

Result:
no goals

Proof state:
s : Set Cardinal.{v}
⊢ lift.{u, v} (sInf s) = sInf (lift.{u, v} '' s)

Tactic:
rcases eq_empty_or_nonempty s with (rfl | hs)

Result:
case inl

⊢ lift.{u, v} (sInf ∅) = sInf (lift.{u, v} '' ∅)

case inr
s : Set Cardinal.{v}
hs : s.Nonempty
⊢ lift.{u, v} (sInf s) = sInf (lift.{u, v} '' s)

Proof state:
case inr
s : Set Cardinal.{v}
hs : s.Nonempty
⊢ lift.{u, v} (sInf s) = sInf (lift.{u, v} '' s)

Tactic:
exact lift_monotone.map_csInf hs

Result:
no goals
-- Mathlib/Algebra/Order/GroupWithZero/Unbundled.lean
/-- See `le_mul_inv_iff₀` for a version with multiplication on the other side. -/
lemma le_mul_inv_iff₀' (hc : 0 < c) : a ≤ b * c⁻¹ ↔ c * a ≤ b

Proof state:
G₀ : Type u_2
inst✝⁴ : CommGroupWithZero G₀
inst✝³ : PartialOrder G₀
inst✝² : ZeroLEOneClass G₀
inst✝¹ : PosMulReflectLT G₀
inst✝ : PosMulMono G₀
a b c : G₀
hc : 0 < c
⊢ a ≤ b * c⁻¹ ↔ c * a ≤ b

Tactic:
have := posMulMono_iff_mulPosMono.1 ‹_›

Result:
G₀ : Type u_2
inst✝⁴ : CommGroupWithZero G₀
inst✝³ : PartialOrder G₀
inst✝² : ZeroLEOneClass G₀
inst✝¹ : PosMulReflectLT G₀
inst✝ : PosMulMono G₀
a b c : G₀
hc : 0 < c
this : MulPosMono G₀
⊢ a ≤ b * c⁻¹ ↔ c * a ≤ b

Proof state:
G₀ : Type u_2
inst✝⁴ : CommGroupWithZero G₀
inst✝³ : PartialOrder G₀
inst✝² : ZeroLEOneClass G₀
inst✝¹ : PosMulReflectLT G₀
inst✝ : PosMulMono G₀
a b c : G₀
hc : 0 < c
this : MulPosMono G₀
⊢ a ≤ b * c⁻¹ ↔ c * a ≤ b

Tactic:
rw [le_mul_inv_iff₀ hc, mul_comm]

Result:
no goals
-- Mathlib/Data/List/Rotate.lean
theorem get?_rotate {l : List α} {n m : ℕ} (hml : m < l.length) :
    (l.rotate n).get? m = l.get? ((m + n) % l.length)

Proof state:
α : Type u
l : List α
n m : ℕ
hml : m < l.length
⊢ (l.rotate n).get? m = l.get? ((m + n) % l.length)

Tactic:
simp only [get?_eq_getElem?, length_rotate, hml, getElem?_eq_getElem, getElem_rotate]

Result:
α : Type u
l : List α
n m : ℕ
hml : m < l.length
⊢ some l[(m + n) % l.length] = l[(m + n) % l.length]?

Proof state:
α : Type u
l : List α
n m : ℕ
hml : m < l.length
⊢ some l[(m + n) % l.length] = l[(m + n) % l.length]?

Tactic:
rw [← getElem?_eq_getElem]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem some_getElem_eq_getElem?_iff (a : Array α) (i : Nat) (h : i < a.size) :
    (some a[i] = a[i]?) ↔ True

Proof state:
α : Type u_1
a : Array α
i : Nat
h : i < a.size
⊢ some a[i] = a[i]? ↔ True

Tactic:
simp [h]

Result:
no goals
-- Mathlib/Topology/Separation/Regular.lean
theorem disjoint_nhdsSet_nhds : Disjoint (𝓝ˢ s) (𝓝 x) ↔ x ∉ closure s

Proof state:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : RegularSpace X
x : X
s : Set X
⊢ Disjoint (𝓝ˢ s) (𝓝 x) ↔ x ∉ closure s

Tactic:
have h := (regularSpace_TFAE X).out 0 2

Result:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : RegularSpace X
x : X
s : Set X
h : RegularSpace X ↔ ∀ (x : X) (s : Set X), Disjoint (𝓝ˢ s) (𝓝 x) ↔ x ∉ closure s
⊢ Disjoint (𝓝ˢ s) (𝓝 x) ↔ x ∉ closure s

Proof state:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : RegularSpace X
x : X
s : Set X
h : RegularSpace X ↔ ∀ (x : X) (s : Set X), Disjoint (𝓝ˢ s) (𝓝 x) ↔ x ∉ closure s
⊢ Disjoint (𝓝ˢ s) (𝓝 x) ↔ x ∉ closure s

Tactic:
exact h.mp ‹_› _ _

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/Block.lean
theorem blockTriangular_blockDiagonal [DecidableEq α] (d : α → Matrix m m R) :
    BlockTriangular (blockDiagonal d) Prod.snd

Proof state:
case mk.mk.a
α : Type u_1
m : Type u_3
R : Type v
inst✝² : Preorder α
inst✝¹ : Zero R
inst✝ : DecidableEq α
d : α → Matrix m m R
i : m
i' : α
j : m
j' : α
h : (j, j').2 < (i, i').2
⊢ ⟨j', j⟩.fst < ⟨i', i⟩.fst

Tactic:
exact h

Result:
no goals

Proof state:
α : Type u_1
m : Type u_3
R : Type v
inst✝² : Preorder α
inst✝¹ : Zero R
inst✝ : DecidableEq α
d : α → Matrix m m R
⊢ (blockDiagonal d).BlockTriangular Prod.snd

Tactic:
rintro ⟨i, i'⟩ ⟨j, j'⟩ h

Result:
case mk.mk
α : Type u_1
m : Type u_3
R : Type v
inst✝² : Preorder α
inst✝¹ : Zero R
inst✝ : DecidableEq α
d : α → Matrix m m R
i : m
i' : α
j : m
j' : α
h : (j, j').2 < (i, i').2
⊢ blockDiagonal d (i, i') (j, j') = 0

Proof state:
case mk.mk
α : Type u_1
m : Type u_3
R : Type v
inst✝² : Preorder α
inst✝¹ : Zero R
inst✝ : DecidableEq α
d : α → Matrix m m R
i : m
i' : α
j : m
j' : α
h : (j, j').2 < (i, i').2
⊢ blockDiagonal d (i, i') (j, j') = 0

Tactic:
rw [blockDiagonal'_eq_blockDiagonal, blockTriangular_blockDiagonal']

Result:
case mk.mk.a
α : Type u_1
m : Type u_3
R : Type v
inst✝² : Preorder α
inst✝¹ : Zero R
inst✝ : DecidableEq α
d : α → Matrix m m R
i : m
i' : α
j : m
j' : α
h : (j, j').2 < (i, i').2
⊢ ⟨j', j⟩.fst < ⟨i', i⟩.fst
-- Mathlib/Analysis/SpecialFunctions/Log/Basic.lean
theorem abs_log_mul_self_lt (x : ℝ) (h1 : 0 < x) (h2 : x ≤ 1) : |log x * x| < 1

Proof state:
x : ℝ
h1 : 0 < x
h2 : x ≤ 1
this : log (1 / x) ≤ 1 / x - 1
⊢ log (1 / x) < 1 / x

Tactic:
linarith

Result:
no goals

Proof state:
x : ℝ
h1 : 0 < x
h2 : x ≤ 1
this : -log x * x < 1
⊢ 0 ≤ -log x

Tactic:
rw [← log_inv]

Result:
x : ℝ
h1 : 0 < x
h2 : x ≤ 1
this : -log x * x < 1
⊢ 0 ≤ log x⁻¹

Proof state:
case hx
x : ℝ
h1 : 0 < x
h2 : x ≤ 1
this : -log x * x < 1
⊢ x ≤ 1

Tactic:
exact h2

Result:
no goals

Proof state:
x : ℝ
h1 : 0 < x
h2 : x ≤ 1
this : 0 < 1 / x
⊢ |log x * x| < 1

Tactic:
replace := log_le_sub_one_of_pos this

Result:
x : ℝ
h1 : 0 < x
h2 : x ≤ 1
this : log (1 / x) ≤ 1 / x - 1
⊢ |log x * x| < 1

Proof state:
x : ℝ
h1 : 0 < x
h2 : x ≤ 1
this : -log x * x < 1
aux : 0 ≤ -log x * x
⊢ |log x * x| < 1

Tactic:
rw [← abs_of_nonneg aux, neg_mul, abs_neg] at this

Result:
x : ℝ
h1 : 0 < x
h2 : x ≤ 1
this : |log x * x| < 1
aux : 0 ≤ -log x * x
⊢ |log x * x| < 1

Proof state:
x : ℝ
h1 : 0 < x
h2 : x ≤ 1
this : |log x * x| < 1
aux : 0 ≤ -log x * x
⊢ |log x * x| < 1

Tactic:
exact this

Result:
no goals

Proof state:
x : ℝ
h1 : 0 < x
h2 : x ≤ 1
⊢ |log x * x| < 1

Tactic:
have : 0 < 1 / x := by simpa only [one_div, inv_pos] using h1

Result:
x : ℝ
h1 : 0 < x
h2 : x ≤ 1
this : 0 < 1 / x
⊢ |log x * x| < 1

Proof state:
case hx
x : ℝ
h1 : 0 < x
h2 : x ≤ 1
this : -log x * x < 1
⊢ 1 ≤ x⁻¹

Tactic:
rw [← le_inv_comm₀ h1 zero_lt_one, inv_one]

Result:
case hx
x : ℝ
h1 : 0 < x
h2 : x ≤ 1
this : -log x * x < 1
⊢ x ≤ 1

Proof state:
x : ℝ
h1 : 0 < x
h2 : x ≤ 1
this : -log x * x < 1
⊢ 0 ≤ -log x * x

Tactic:
refine mul_nonneg ?_ h1.le

Result:
x : ℝ
h1 : 0 < x
h2 : x ≤ 1
this : -log x * x < 1
⊢ 0 ≤ -log x

Proof state:
x : ℝ
h1 : 0 < x
h2 : x ≤ 1
this : log (1 / x) ≤ 1 / x - 1
⊢ |log x * x| < 1

Tactic:
replace : log (1 / x) < 1 / x := by linarith

Result:
x : ℝ
h1 : 0 < x
h2 : x ≤ 1
this : log (1 / x) < 1 / x
⊢ |log x * x| < 1

Proof state:
x : ℝ
h1 : 0 < x
h2 : x ≤ 1
this : log (1 / x) < 1 / x
⊢ |log x * x| < 1

Tactic:
rw [log_div one_ne_zero h1.ne', log_one, zero_sub, lt_div_iff₀ h1] at this

Result:
x : ℝ
h1 : 0 < x
h2 : x ≤ 1
this : -log x * x < 1
⊢ |log x * x| < 1

Proof state:
x : ℝ
h1 : 0 < x
h2 : x ≤ 1
this : -log x * x < 1
⊢ 0 ≤ log x⁻¹

Tactic:
apply log_nonneg

Result:
case hx
x : ℝ
h1 : 0 < x
h2 : x ≤ 1
this : -log x * x < 1
⊢ 1 ≤ x⁻¹

Proof state:
x : ℝ
h1 : 0 < x
h2 : x ≤ 1
⊢ 0 < 1 / x

Tactic:
simpa only [one_div, inv_pos] using h1

Result:
no goals

Proof state:
x : ℝ
h1 : 0 < x
h2 : x ≤ 1
this : -log x * x < 1
⊢ |log x * x| < 1

Tactic:
have aux : 0 ≤ -log x * x := by
  refine mul_nonneg ?_ h1.le
  rw [← log_inv]
  apply log_nonneg
  rw [← le_inv_comm₀ h1 zero_lt_one, inv_one]
  exact h2

Result:
x : ℝ
h1 : 0 < x
h2 : x ≤ 1
this : -log x * x < 1
aux : 0 ≤ -log x * x
⊢ |log x * x| < 1
-- Mathlib/Analysis/Convex/Strict.lean
theorem strictConvex_iff_div :
    StrictConvex 𝕜 s ↔
      s.Pairwise fun x y =>
        ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → (a / (a + b)) • x + (b / (a + b)) • y ∈ interior s :=
  ⟨fun h x hx y hy hxy a b ha hb ↦ h hx hy hxy (by positivity) (by positivity) (by field_simp),
    fun h x hx y hy hxy a b ha hb hab ↦ by
    convert h hx hy hxy ha hb <;> rw [hab, div_one]⟩

Proof state:
𝕜 : Type u_1
E : Type u_3
inst✝³ : LinearOrderedField 𝕜
inst✝² : TopologicalSpace E
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
h : StrictConvex 𝕜 s
x : E
hx : x ∈ s
y : E
hy : y ∈ s
hxy : x ≠ y
a b : 𝕜
ha : 0 < a
hb : 0 < b
⊢ 0 < b / (a + b)

Tactic:
positivity

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_3
inst✝³ : LinearOrderedField 𝕜
inst✝² : TopologicalSpace E
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
h : StrictConvex 𝕜 s
x : E
hx : x ∈ s
y : E
hy : y ∈ s
hxy : x ≠ y
a b : 𝕜
ha : 0 < a
hb : 0 < b
⊢ a / (a + b) + b / (a + b) = 1

Tactic:
field_simp

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_3
inst✝³ : LinearOrderedField 𝕜
inst✝² : TopologicalSpace E
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
h : StrictConvex 𝕜 s
x : E
hx : x ∈ s
y : E
hy : y ∈ s
hxy : x ≠ y
a b : 𝕜
ha : 0 < a
hb : 0 < b
⊢ 0 < a / (a + b)

Tactic:
positivity

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_3
inst✝³ : LinearOrderedField 𝕜
inst✝² : TopologicalSpace E
inst✝¹ : AddCommGroup E
inst✝ : Module 𝕜 E
s : Set E
h : s.Pairwise fun x y => ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → (a / (a + b)) • x + (b / (a + b)) • y ∈ interior s
x : E
hx : x ∈ s
y : E
hy : y ∈ s
hxy : x ≠ y
a b : 𝕜
ha : 0 < a
hb : 0 < b
hab : a + b = 1
⊢ a • x + b • y ∈ interior s

Tactic:
convert h hx hy hxy ha hb <;> rw [hab, div_one]

Result:
no goals
-- Mathlib/Topology/Algebra/UniformGroup/Defs.lean
theorem UniformContinuous.zpow_const [UniformSpace β] {f : β → α} (hf : UniformContinuous f) :
    ∀ n : ℤ, UniformContinuous fun x => f x ^ n
  | (n : ℕ) => by
    simp_rw [zpow_natCast]
    exact hf.pow_const _
  | Int.negSucc n => by
    simp_rw [zpow_negSucc]
    exact (hf.pow_const _).inv

Proof state:
α : Type u_1
β : Type u_2
inst✝³ : UniformSpace α
inst✝² : Group α
inst✝¹ : UniformGroup α
inst✝ : UniformSpace β
f : β → α
hf : UniformContinuous f
n : ℕ
⊢ UniformContinuous fun x => f x ^ ↑n

Tactic:
simp_rw [zpow_natCast]

Result:
α : Type u_1
β : Type u_2
inst✝³ : UniformSpace α
inst✝² : Group α
inst✝¹ : UniformGroup α
inst✝ : UniformSpace β
f : β → α
hf : UniformContinuous f
n : ℕ
⊢ UniformContinuous fun x => f x ^ n

Proof state:
α : Type u_1
β : Type u_2
inst✝³ : UniformSpace α
inst✝² : Group α
inst✝¹ : UniformGroup α
inst✝ : UniformSpace β
f : β → α
hf : UniformContinuous f
n : ℕ
⊢ UniformContinuous fun x => (f x ^ (n + 1))⁻¹

Tactic:
exact (hf.pow_const _).inv

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝³ : UniformSpace α
inst✝² : Group α
inst✝¹ : UniformGroup α
inst✝ : UniformSpace β
f : β → α
hf : UniformContinuous f
n : ℕ
⊢ UniformContinuous fun x => f x ^ n

Tactic:
exact hf.pow_const _

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝³ : UniformSpace α
inst✝² : Group α
inst✝¹ : UniformGroup α
inst✝ : UniformSpace β
f : β → α
hf : UniformContinuous f
n : ℕ
⊢ UniformContinuous fun x => f x ^ Int.negSucc n

Tactic:
simp_rw [zpow_negSucc]

Result:
α : Type u_1
β : Type u_2
inst✝³ : UniformSpace α
inst✝² : Group α
inst✝¹ : UniformGroup α
inst✝ : UniformSpace β
f : β → α
hf : UniformContinuous f
n : ℕ
⊢ UniformContinuous fun x => (f x ^ (n + 1))⁻¹
-- Mathlib/Data/Nat/Sqrt.lean
lemma sqrt.lt_iter_succ_sq (n guess : ℕ) (hn : n < (guess + 1) * (guess + 1)) :
    n < (sqrt.iter n guess + 1) * (sqrt.iter n guess + 1)

Proof state:
case pos
n guess : ℕ
hn : n < (guess + 1) * (guess + 1)
m : ℕ := (guess + n / guess) / 2
h : (guess + n / guess) / 2 < guess
⊢ 4 * (guess * guess) * n < 4 * (guess * guess) * ((m + 1) * (m + 1))

Tactic:
apply Nat.lt_of_le_of_lt AM_GM

Result:
case pos
n guess : ℕ
hn : n < (guess + 1) * (guess + 1)
m : ℕ := (guess + n / guess) / 2
h : (guess + n / guess) / 2 < guess
⊢ (guess * guess + n) * (guess * guess + n) < 4 * (guess * guess) * ((m + 1) * (m + 1))

Proof state:
case neg
n guess : ℕ
hn : n < (guess + 1) * (guess + 1)
m : ℕ := (guess + n / guess) / 2
h : ¬(guess + n / guess) / 2 < guess
⊢ n < (guess + 1) * (guess + 1)

Tactic:
simpa only [dif_neg h] using hn

Result:
no goals

Proof state:
case pos
n guess : ℕ
hn : n < (guess + 1) * (guess + 1)
m : ℕ := (guess + n / guess) / 2
h : (guess + n / guess) / 2 < guess
⊢ n < (iter n ((guess + n / guess) / 2) + 1) * (iter n ((guess + n / guess) / 2) + 1)

Tactic:
suffices n < (m + 1) * (m + 1) by
  simpa only [dif_pos h] using sqrt.lt_iter_succ_sq n m this

Result:
case pos
n guess : ℕ
hn : n < (guess + 1) * (guess + 1)
m : ℕ := (guess + n / guess) / 2
h : (guess + n / guess) / 2 < guess
⊢ n < (m + 1) * (m + 1)

Proof state:
n guess : ℕ
hn : n < (guess + 1) * (guess + 1)
m : ℕ := (guess + n / guess) / 2
h : (guess + n / guess) / 2 < guess
⊢ 0 < 2

Tactic:
decide

Result:
no goals
-- Mathlib/Data/Finset/Pi.lean
theorem Pi.cons_injective {a : α} {b : δ a} {s : Finset α} (hs : a ∉ s) :
    Function.Injective (Pi.cons s a b) := fun e₁ e₂ eq =>
  @Multiset.Pi.cons_injective α _ δ a b s.1 hs _ _ <|
    funext fun e =>
      funext fun h =>
        have :
          Pi.cons s a b e₁ e (by simpa only [Multiset.mem_cons, mem_insert] using h) =
            Pi.cons s a b e₂ e (by simpa only [Multiset.mem_cons, mem_insert] using h)

Proof state:
α : Type u_1
δ : α → Sort v
inst✝ : DecidableEq α
a : α
b : δ a
s : Finset α
hs : a ∉ s
e₁ e₂ : (a : α) → a ∈ s → δ a
eq : cons s a b e₁ = cons s a b e₂
e : α
h : e ∈ a ::ₘ s.val
⊢ e ∈ insert a s

Tactic:
simpa only [Multiset.mem_cons, mem_insert] using h

Result:
no goals

Proof state:
α : Type u_1
δ : α → Sort v
inst✝ : DecidableEq α
a : α
b : δ a
s : Finset α
hs : a ∉ s
e₁ e₂ : (a : α) → a ∈ s → δ a
eq : cons s a b e₁ = cons s a b e₂
e : α
h : e ∈ a ::ₘ s.val
⊢ cons s a b e₁ e ⋯ = cons s a b e₂ e ⋯

Tactic:
rw [eq]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/Real.lean
lemma le_rpow_of_log_le (hy : 0 < y) (h : log x ≤ z * log y) : x ≤ y ^ z

Proof state:
x y z : ℝ
hy : 0 < y
h : log x ≤ z * log y
⊢ x ≤ y ^ z

Tactic:
obtain hx | hx := le_or_lt x 0

Result:
case inl
x y z : ℝ
hy : 0 < y
h : log x ≤ z * log y
hx : x ≤ 0
⊢ x ≤ y ^ z

case inr
x y z : ℝ
hy : 0 < y
h : log x ≤ z * log y
hx : 0 < x
⊢ x ≤ y ^ z

Proof state:
case inr
x y z : ℝ
hy : 0 < y
h : log x ≤ z * log y
hx : 0 < x
⊢ x ≤ y ^ z

Tactic:
exact (le_rpow_iff_log_le hx hy).2 h

Result:
no goals

Proof state:
case inl
x y z : ℝ
hy : 0 < y
h : log x ≤ z * log y
hx : x ≤ 0
⊢ x ≤ y ^ z

Tactic:
exact hx.trans (rpow_pos_of_pos hy _).le

Result:
no goals