harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Probability/Moments/ComplexMGF.lean
lemma hasDerivAt_iteratedDeriv_complexMGF (hz : z.re ∈ interior (integrableExpSet X μ)) (n : ℕ) :
    HasDerivAt (iteratedDeriv n (complexMGF X μ)) μ[fun ω ↦ X ω ^ (n + 1) * cexp (z * X ω)] z

Proof state:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
n : ℕ
hn :
  ∀ {z : ℂ},
    z.re ∈ interior (integrableExpSet X μ) →
      HasDerivAt (iteratedDeriv n (complexMGF X μ)) (∫ (x : Ω), (fun ω => ↑(X ω) ^ (n + 1) * cexp (z * ↑(X ω))) x ∂μ) z
z : ℂ
hz : z.re ∈ interior (integrableExpSet X μ)
⊢ IsOpen fun y => interior (integrableExpSet X μ) y.re

Tactic:
exact isOpen_interior.preimage Complex.continuous_re

Result:
no goals

Proof state:
case zero
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
z : ℂ
hz : z.re ∈ interior (integrableExpSet X μ)
⊢ HasDerivAt (iteratedDeriv 0 (complexMGF X μ)) (∫ (x : Ω), (fun ω => ↑(X ω) ^ (0 + 1) * cexp (z * ↑(X ω))) x ∂μ) z

Tactic:
simp [hasDerivAt_complexMGF hz]

Result:
no goals
-- Mathlib/Algebra/BigOperators/Pi.lean
lemma Pi.single_induction [AddCommMonoid M] (p : (ι → M) → Prop) (f : ι → M)
    (zero : p 0) (add : ∀ f g, p f → p g → p (f + g))
    (single : ∀ i m, p (Pi.single i m)) : p f

Proof state:
ι : Type u_1
inst✝² : Finite ι
inst✝¹ : DecidableEq ι
M : Type u_4
inst✝ : AddCommMonoid M
p : (ι → M) → Prop
f : ι → M
zero : p 0
add : ∀ (f g : ι → M), p f → p g → p (f + g)
single : ∀ (i : ι) (m : M), p (Pi.single i m)
val✝ : Fintype ι
⊢ ∀ x ∈ Finset.univ, p (Pi.single x (f x))

Tactic:
simp [single]

Result:
no goals

Proof state:
ι : Type u_1
inst✝² : Finite ι
inst✝¹ : DecidableEq ι
M : Type u_4
inst✝ : AddCommMonoid M
p : (ι → M) → Prop
f : ι → M
zero : p 0
add : ∀ (f g : ι → M), p f → p g → p (f + g)
single : ∀ (i : ι) (m : M), p (Pi.single i m)
⊢ p f

Tactic:
cases nonempty_fintype ι

Result:
case intro
ι : Type u_1
inst✝² : Finite ι
inst✝¹ : DecidableEq ι
M : Type u_4
inst✝ : AddCommMonoid M
p : (ι → M) → Prop
f : ι → M
zero : p 0
add : ∀ (f g : ι → M), p f → p g → p (f + g)
single : ∀ (i : ι) (m : M), p (Pi.single i m)
val✝ : Fintype ι
⊢ p f

Proof state:
case intro
ι : Type u_1
inst✝² : Finite ι
inst✝¹ : DecidableEq ι
M : Type u_4
inst✝ : AddCommMonoid M
p : (ι → M) → Prop
f : ι → M
zero : p 0
add : ∀ (f g : ι → M), p f → p g → p (f + g)
single : ∀ (i : ι) (m : M), p (Pi.single i m)
val✝ : Fintype ι
⊢ p (∑ i : ι, Pi.single i (f i))

Tactic:
exact Finset.sum_induction _ _ add zero (by simp [single])

Result:
no goals

Proof state:
case intro
ι : Type u_1
inst✝² : Finite ι
inst✝¹ : DecidableEq ι
M : Type u_4
inst✝ : AddCommMonoid M
p : (ι → M) → Prop
f : ι → M
zero : p 0
add : ∀ (f g : ι → M), p f → p g → p (f + g)
single : ∀ (i : ι) (m : M), p (Pi.single i m)
val✝ : Fintype ι
⊢ p f

Tactic:
rw [← Finset.univ_sum_single f]

Result:
case intro
ι : Type u_1
inst✝² : Finite ι
inst✝¹ : DecidableEq ι
M : Type u_4
inst✝ : AddCommMonoid M
p : (ι → M) → Prop
f : ι → M
zero : p 0
add : ∀ (f g : ι → M), p f → p g → p (f + g)
single : ∀ (i : ι) (m : M), p (Pi.single i m)
val✝ : Fintype ι
⊢ p (∑ i : ι, Pi.single i (f i))
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem getKey_alter [LawfulBEq α] [Inhabited α] {k k' : α} {f : Option (β k) → Option (β k)}
    (h : m.WF) {hc : k' ∈ m.alter k f} :
    (m.alter k f).getKey k' hc =
      if heq : k == k' then
        k
      else
        haveI h' : k' ∈ m := mem_alter_of_beq_eq_false h (Bool.not_eq_true _ ▸ heq) |>.mp hc
        m.getKey k' h'

Proof state:
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
m : Raw α β
inst✝¹ : LawfulBEq α
inst✝ : Inhabited α
k k' : α
f : Option (β k) → Option (β k)
h : m.WF
hc✝ : k' ∈ m.alter k f
hc : (m.alter k f).contains k' = true
⊢ (m.alter k f).getKey k' hc✝ = if heq : (k == k') = true then k else m.getKey k' ⋯

Tactic:
revert hc

Result:
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
m : Raw α β
inst✝¹ : LawfulBEq α
inst✝ : Inhabited α
k k' : α
f : Option (β k) → Option (β k)
h : m.WF
hc : k' ∈ m.alter k f
⊢ (m.alter k f).contains k' = true → (m.alter k f).getKey k' hc = if heq : (k == k') = true then k else m.getKey k' ⋯

Proof state:
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
m : Raw α β
inst✝¹ : LawfulBEq α
inst✝ : Inhabited α
k k' : α
f : Option (β k) → Option (β k)
h : m.WF
hc : k' ∈ m.alter k f
⊢ (m.alter k f).getKey k' hc = if heq : (k == k') = true then k else m.getKey k' ⋯

Tactic:
simp only [mem_iff_contains] at hc

Result:
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
m : Raw α β
inst✝¹ : LawfulBEq α
inst✝ : Inhabited α
k k' : α
f : Option (β k) → Option (β k)
h : m.WF
hc✝ : k' ∈ m.alter k f
hc : (m.alter k f).contains k' = true
⊢ (m.alter k f).getKey k' hc✝ = if heq : (k == k') = true then k else m.getKey k' ⋯

Proof state:
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
m : Raw α β
inst✝¹ : LawfulBEq α
inst✝ : Inhabited α
k k' : α
f : Option (β k) → Option (β k)
h : m.WF
hc : k' ∈ m.alter k f
⊢ (m.alter k f).contains k' = true → (m.alter k f).getKey k' hc = if heq : (k == k') = true then k else m.getKey k' ⋯

Tactic:
simp_to_raw using Raw₀.getKey_alter

Result:
no goals
-- Mathlib/Algebra/Order/Round.lean
theorem abs_sub_round (x : α) : |x - round x| ≤ 1 / 2

Proof state:
α : Type u_2
inst✝¹ : LinearOrderedField α
inst✝ : FloorRing α
x : α
⊢ x - ↑⌊x + 1 / 2⌋ ≤ 1 / 2 ∧ ↑⌊x + 1 / 2⌋ - x ≤ 1 / 2

Tactic:
have := floor_le (x + 1 / 2)

Result:
α : Type u_2
inst✝¹ : LinearOrderedField α
inst✝ : FloorRing α
x : α
this : ↑⌊x + 1 / 2⌋ ≤ x + 1 / 2
⊢ x - ↑⌊x + 1 / 2⌋ ≤ 1 / 2 ∧ ↑⌊x + 1 / 2⌋ - x ≤ 1 / 2

Proof state:
α : Type u_2
inst✝¹ : LinearOrderedField α
inst✝ : FloorRing α
x : α
⊢ |x - ↑(round x)| ≤ 1 / 2

Tactic:
rw [round_eq, abs_sub_le_iff]

Result:
α : Type u_2
inst✝¹ : LinearOrderedField α
inst✝ : FloorRing α
x : α
⊢ x - ↑⌊x + 1 / 2⌋ ≤ 1 / 2 ∧ ↑⌊x + 1 / 2⌋ - x ≤ 1 / 2

Proof state:
α : Type u_2
inst✝¹ : LinearOrderedField α
inst✝ : FloorRing α
x : α
this : ↑⌊x + 1 / 2⌋ ≤ x + 1 / 2
⊢ x - ↑⌊x + 1 / 2⌋ ≤ 1 / 2 ∧ ↑⌊x + 1 / 2⌋ - x ≤ 1 / 2

Tactic:
have := lt_floor_add_one (x + 1 / 2)

Result:
α : Type u_2
inst✝¹ : LinearOrderedField α
inst✝ : FloorRing α
x : α
this✝ : ↑⌊x + 1 / 2⌋ ≤ x + 1 / 2
this : x + 1 / 2 < ↑⌊x + 1 / 2⌋ + 1
⊢ x - ↑⌊x + 1 / 2⌋ ≤ 1 / 2 ∧ ↑⌊x + 1 / 2⌋ - x ≤ 1 / 2

Proof state:
α : Type u_2
inst✝¹ : LinearOrderedField α
inst✝ : FloorRing α
x : α
this✝ : ↑⌊x + 1 / 2⌋ ≤ x + 1 / 2
this : x + 1 / 2 < ↑⌊x + 1 / 2⌋ + 1
⊢ x - ↑⌊x + 1 / 2⌋ ≤ 1 / 2 ∧ ↑⌊x + 1 / 2⌋ - x ≤ 1 / 2

Tactic:
constructor <;> linarith

Result:
no goals
-- Mathlib/Probability/Kernel/Composition/MapComap.lean
theorem sum_map_seq (κ : Kernel α β) [IsSFiniteKernel κ] (f : β → γ) :
    (Kernel.sum fun n => map (seq κ n) f) = map κ f

Proof state:
case pos
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
f : β → γ
hf : Measurable f
⊢ (Kernel.sum fun n => (κ.seq n).map f) = κ.map f

Tactic:
ext a s hs

Result:
case pos.h.h
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
f : β → γ
hf : Measurable f
a : α
s : Set γ
hs : MeasurableSet s
⊢ ((Kernel.sum fun n => (κ.seq n).map f) a) s = ((κ.map f) a) s

Proof state:
case pos.h.h
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
f : β → γ
hf : Measurable f
a : α
s : Set γ
hs : MeasurableSet s
⊢ ((Kernel.sum fun n => (κ.seq n).map f) a) s = ((κ.map f) a) s

Tactic:
rw [Kernel.sum_apply, map_apply' κ hf a hs, Measure.sum_apply _ hs, ← measure_sum_seq κ,
  Measure.sum_apply _ (hf hs)]

Result:
case pos.h.h
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
f : β → γ
hf : Measurable f
a : α
s : Set γ
hs : MeasurableSet s
⊢ ∑' (i : ℕ), (((κ.seq i).map f) a) s = ∑' (i : ℕ), ((κ.seq i) a) (f ⁻¹' s)

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
f : β → γ
⊢ (Kernel.sum fun n => (κ.seq n).map f) = κ.map f

Tactic:
by_cases hf : Measurable f

Result:
case pos
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
f : β → γ
hf : Measurable f
⊢ (Kernel.sum fun n => (κ.seq n).map f) = κ.map f

case neg
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
f : β → γ
hf : ¬Measurable f
⊢ (Kernel.sum fun n => (κ.seq n).map f) = κ.map f

Proof state:
case neg
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
f : β → γ
hf : ¬Measurable f
⊢ (Kernel.sum fun n => (κ.seq n).map f) = κ.map f

Tactic:
simp [map_of_not_measurable _ hf]

Result:
no goals

Proof state:
case pos.h.h
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
f : β → γ
hf : Measurable f
a : α
s : Set γ
hs : MeasurableSet s
⊢ ∑' (i : ℕ), (((κ.seq i).map f) a) s = ∑' (i : ℕ), ((κ.seq i) a) (f ⁻¹' s)

Tactic:
simp_rw [map_apply' _ hf _ hs]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Complex/Circle.lean
lemma exp_eq_exp {x y : ℝ} : exp x = exp y ↔ ∃ m : ℤ, x = y + m * (2 * π)

Proof state:
x y : ℝ
n : ℤ
⊢ ↑x * I = ↑y * I + ↑n * (2 * ↑π * I) ↔ x = y + ↑n * (2 * π)

Tactic:
rw [← mul_assoc, ← add_mul, mul_left_inj' I_ne_zero]

Result:
x y : ℝ
n : ℤ
⊢ ↑x = ↑y + ↑n * (2 * ↑π) ↔ x = y + ↑n * (2 * π)

Proof state:
x y : ℝ
n : ℤ
⊢ ↑x = ↑y + ↑n * (2 * ↑π) ↔ x = y + ↑n * (2 * π)

Tactic:
norm_cast

Result:
no goals

Proof state:
x y : ℝ
⊢ exp x = exp y ↔ ∃ m, x = y + ↑m * (2 * π)

Tactic:
rw [Subtype.ext_iff, coe_exp, coe_exp, exp_eq_exp_iff_exists_int]

Result:
x y : ℝ
⊢ (∃ n, ↑x * I = ↑y * I + ↑n * (2 * ↑π * I)) ↔ ∃ m, x = y + ↑m * (2 * π)

Proof state:
x y : ℝ
⊢ (∃ n, ↑x * I = ↑y * I + ↑n * (2 * ↑π * I)) ↔ ∃ m, x = y + ↑m * (2 * π)

Tactic:
refine exists_congr fun n => ?_

Result:
x y : ℝ
n : ℤ
⊢ ↑x * I = ↑y * I + ↑n * (2 * ↑π * I) ↔ x = y + ↑n * (2 * π)
-- Mathlib/Algebra/Order/Group/Basic.lean
@[to_additive zsmul_right_injective
"See also `smul_right_injective`. TODO: provide a `NoZeroSMulDivisors` instance. We can't do
that here because importing that definition would create import cycles."]
lemma zpow_left_injective (hn : n ≠ 0) : Injective ((· ^ n) : α → α)

Proof state:
case inr
α : Type u_1
inst✝ : LinearOrderedCommGroup α
n : ℤ
hn✝ : n ≠ 0
hn : 0 < n
⊢ Injective fun x => x ^ n

Tactic:
exact (zpow_left_strictMono _ hn).injective

Result:
no goals

Proof state:
α : Type u_1
inst✝ : LinearOrderedCommGroup α
n : ℤ
hn : n ≠ 0
⊢ Injective fun x => x ^ n

Tactic:
obtain hn | hn := hn.lt_or_lt

Result:
case inl
α : Type u_1
inst✝ : LinearOrderedCommGroup α
n : ℤ
hn✝ : n ≠ 0
hn : n < 0
⊢ Injective fun x => x ^ n

case inr
α : Type u_1
inst✝ : LinearOrderedCommGroup α
n : ℤ
hn✝ : n ≠ 0
hn : 0 < n
⊢ Injective fun x => x ^ n

Proof state:
case inl
α : Type u_1
inst✝ : LinearOrderedCommGroup α
n : ℤ
hn✝ : n ≠ 0
hn : n < 0
a b : α
hab : a ^ n = b ^ n
⊢ a ^ (-n) = b ^ (-n)

Tactic:
rw [zpow_neg, zpow_neg, hab]

Result:
no goals

Proof state:
case inl
α : Type u_1
inst✝ : LinearOrderedCommGroup α
n : ℤ
hn✝ : n ≠ 0
hn : n < 0
⊢ Injective fun x => x ^ n

Tactic:
refine fun a b (hab : a ^ n = b ^ n) ↦
  (zpow_left_strictMono _ <| Int.neg_pos_of_neg hn).injective ?_

Result:
case inl
α : Type u_1
inst✝ : LinearOrderedCommGroup α
n : ℤ
hn✝ : n ≠ 0
hn : n < 0
a b : α
hab : a ^ n = b ^ n
⊢ a ^ (-n) = b ^ (-n)
-- Mathlib/Data/Nat/Choose/Multinomial.lean
theorem multinomial_congr {f g : α → ℕ} (h : ∀ a ∈ s, f a = g a) :
    multinomial s f = multinomial s g

Proof state:
case e_a
α : Type u_1
s : Finset α
f g : α → ℕ
h : ∀ a ∈ s, f a = g a
⊢ (∑ i ∈ s, f i)! = (∑ i ∈ s, g i)!

Tactic:
rw [Finset.sum_congr rfl h]

Result:
no goals

Proof state:
case e_a
α : Type u_1
s : Finset α
f g : α → ℕ
h : ∀ a ∈ s, f a = g a
⊢ ∏ i ∈ s, (f i)! = ∏ i ∈ s, (g i)!

Tactic:
exact Finset.prod_congr rfl fun a ha => by rw [h a ha]

Result:
no goals

Proof state:
α : Type u_1
s : Finset α
f g : α → ℕ
h : ∀ a ∈ s, f a = g a
⊢ multinomial s f = multinomial s g

Tactic:
simp only [multinomial]

Result:
α : Type u_1
s : Finset α
f g : α → ℕ
h : ∀ a ∈ s, f a = g a
⊢ (∑ i ∈ s, f i)! / ∏ i ∈ s, (f i)! = (∑ i ∈ s, g i)! / ∏ i ∈ s, (g i)!

Proof state:
α : Type u_1
s : Finset α
f g : α → ℕ
h : ∀ a ∈ s, f a = g a
a : α
ha : a ∈ s
⊢ (f a)! = (g a)!

Tactic:
rw [h a ha]

Result:
no goals

Proof state:
α : Type u_1
s : Finset α
f g : α → ℕ
h : ∀ a ∈ s, f a = g a
⊢ (∑ i ∈ s, f i)! / ∏ i ∈ s, (f i)! = (∑ i ∈ s, g i)! / ∏ i ∈ s, (g i)!

Tactic:
congr 1

Result:
case e_a
α : Type u_1
s : Finset α
f g : α → ℕ
h : ∀ a ∈ s, f a = g a
⊢ (∑ i ∈ s, f i)! = (∑ i ∈ s, g i)!

case e_a
α : Type u_1
s : Finset α
f g : α → ℕ
h : ∀ a ∈ s, f a = g a
⊢ ∏ i ∈ s, (f i)! = ∏ i ∈ s, (g i)!
-- Mathlib/CategoryTheory/EqToHom.lean
theorem eqToHom_iso_hom_naturality {f g : β → C} (z : ∀ b, f b ≅ g b) {j j' : β} (w : j = j') :
    (z j).hom ≫ eqToHom (by simp [w]) = eqToHom (by simp [w]) ≫ (z j').hom

Proof state:
case refl
C : Type u₁
inst✝ : Category.{v₁, u₁} C
β : Sort u_1
f g : β → C
z : (b : β) → f b ≅ g b
j : β
⊢ (z j).hom ≫ eqToHom ⋯ = eqToHom ⋯ ≫ (z j).hom

Tactic:
simp

Result:
no goals

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
β : Sort u_1
f g : β → C
z : (b : β) → f b ≅ g b
j j' : β
w : j = j'
⊢ f j = f j'

Tactic:
simp [w]

Result:
no goals

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
β : Sort u_1
f g : β → C
z : (b : β) → f b ≅ g b
j j' : β
w : j = j'
⊢ g j = g j'

Tactic:
simp [w]

Result:
no goals

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
β : Sort u_1
f g : β → C
z : (b : β) → f b ≅ g b
j j' : β
w : j = j'
⊢ (z j).hom ≫ eqToHom ⋯ = eqToHom ⋯ ≫ (z j').hom

Tactic:
cases w

Result:
case refl
C : Type u₁
inst✝ : Category.{v₁, u₁} C
β : Sort u_1
f g : β → C
z : (b : β) → f b ≅ g b
j : β
⊢ (z j).hom ≫ eqToHom ⋯ = eqToHom ⋯ ≫ (z j).hom
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Count.lean
theorem countP_eq_size_filter' : countP p = size ∘ filter p

Proof state:
α : Type u_1
p : α → Bool
⊢ countP p = size ∘ fun as => filter p as

Tactic:
funext l

Result:
case h
α : Type u_1
p : α → Bool
l : Array α
⊢ countP p l = (size ∘ fun as => filter p as) l

Proof state:
case h
α : Type u_1
p : α → Bool
l : Array α
⊢ countP p l = (size ∘ fun as => filter p as) l

Tactic:
apply countP_eq_size_filter

Result:
no goals
-- Mathlib/Analysis/Convex/Independent.lean
theorem Subsingleton.convexIndependent [Subsingleton ι] (p : ι → E) : ConvexIndependent 𝕜 p

Proof state:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝³ : OrderedSemiring 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : Subsingleton ι
p : ι → E
s : Set ι
x : ι
hx : p x ∈ (convexHull 𝕜) (p '' s)
this : s.Nonempty
⊢ x ∈ s

Tactic:
rwa [Subsingleton.mem_iff_nonempty]

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝³ : OrderedSemiring 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : Subsingleton ι
p : ι → E
s : Set ι
x : ι
hx : p x ∈ (convexHull 𝕜) (p '' s)
this : ((convexHull 𝕜) (p '' s)).Nonempty
⊢ x ∈ s

Tactic:
rw [convexHull_nonempty_iff, Set.image_nonempty] at this

Result:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝³ : OrderedSemiring 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : Subsingleton ι
p : ι → E
s : Set ι
x : ι
hx : p x ∈ (convexHull 𝕜) (p '' s)
this : s.Nonempty
⊢ x ∈ s

Proof state:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝³ : OrderedSemiring 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : Subsingleton ι
p : ι → E
⊢ ConvexIndependent 𝕜 p

Tactic:
intro s x hx

Result:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝³ : OrderedSemiring 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : Subsingleton ι
p : ι → E
s : Set ι
x : ι
hx : p x ∈ (convexHull 𝕜) (p '' s)
⊢ x ∈ s

Proof state:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝³ : OrderedSemiring 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : Subsingleton ι
p : ι → E
s : Set ι
x : ι
hx : p x ∈ (convexHull 𝕜) (p '' s)
⊢ x ∈ s

Tactic:
have : (convexHull 𝕜 (p '' s)).Nonempty := ⟨p x, hx⟩

Result:
𝕜 : Type u_1
E : Type u_2
ι : Type u_3
inst✝³ : OrderedSemiring 𝕜
inst✝² : AddCommGroup E
inst✝¹ : Module 𝕜 E
inst✝ : Subsingleton ι
p : ι → E
s : Set ι
x : ι
hx : p x ∈ (convexHull 𝕜) (p '' s)
this : ((convexHull 𝕜) (p '' s)).Nonempty
⊢ x ∈ s
-- Mathlib/Analysis/Normed/Module/Basic.lean
protected lemma NormedSpace.cobounded_neBot : NeBot (cobounded E)

Proof state:
𝕜 : Type u_1
E : Type u_3
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : Nontrivial E
⊢ (cobounded E).NeBot

Tactic:
rw [neBot_iff, Ne, cobounded_eq_bot_iff, ← isBounded_univ]

Result:
𝕜 : Type u_1
E : Type u_3
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : Nontrivial E
⊢ ¬Bornology.IsBounded univ

Proof state:
𝕜 : Type u_1
E : Type u_3
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace 𝕜 E
inst✝ : Nontrivial E
⊢ ¬Bornology.IsBounded univ

Tactic:
exact NormedSpace.unbounded_univ 𝕜 E

Result:
no goals
-- Mathlib/Order/SuccPred/Basic.lean
theorem pred_le_pred_iff_of_not_isMin (ha : ¬IsMin a) (hb : ¬IsMin b) :
    pred a ≤ pred b ↔ a ≤ b

Proof state:
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : PredOrder α
a b : α
ha : ¬IsMin a
hb : ¬IsMin b
⊢ pred a ≤ pred b ↔ a ≤ b

Tactic:
rw [le_pred_iff_of_not_isMin hb, pred_lt_iff_of_not_isMin ha]

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Aleph.lean
theorem isLimit_omega (o : Ordinal) : Ordinal.IsLimit (ω_ o)

Proof state:
o : Ordinal.{u_1}
⊢ (ℵ_ o).ord.IsLimit

Tactic:
exact isLimit_ord (aleph0_le_aleph _)

Result:
no goals

Proof state:
o : Ordinal.{u_1}
⊢ (ω_ o).IsLimit

Tactic:
rw [← ord_aleph]

Result:
o : Ordinal.{u_1}
⊢ (ℵ_ o).ord.IsLimit
-- Mathlib/MeasureTheory/Integral/IntervalIntegral.lean
theorem integral_smul_const [CompleteSpace E]
    {𝕜 : Type*} [RCLike 𝕜] [NormedSpace 𝕜 E] (f : ℝ → 𝕜) (c : E) :
    ∫ x in a..b, f x • c ∂μ = (∫ x in a..b, f x ∂μ) • c

Proof state:
E : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
a b : ℝ
μ : Measure ℝ
inst✝² : CompleteSpace E
𝕜 : Type u_6
inst✝¹ : RCLike 𝕜
inst✝ : NormedSpace 𝕜 E
f : ℝ → 𝕜
c : E
⊢ ∫ (x : ℝ) in a..b, f x • c ∂μ = (∫ (x : ℝ) in a..b, f x ∂μ) • c

Tactic:
simp only [intervalIntegral_eq_integral_uIoc, integral_smul_const, smul_assoc]

Result:
no goals
-- Mathlib/Order/JordanHolder.lean
theorem length_eq_zero_of_head_eq_head_of_last_eq_last_of_length_eq_zero
    {s₁ s₂ : CompositionSeries X} (hb : s₁.head = s₂.head)
    (ht : s₁.last = s₂.last) (hs₁ : s₁.length = 0) : s₂.length = 0

Proof state:
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s₁ s₂ : CompositionSeries X
hb : head s₁ = head s₂
ht : last s₁ = last s₂
hs₁ : s₁.length = 0
this : Fin.last s₂.length = 0
⊢ s₂.length = 0

Tactic:
simpa [Fin.ext_iff]

Result:
no goals

Proof state:
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s₁ s₂ : CompositionSeries X
hb : head s₁ = head s₂
ht : last s₁ = last s₂
hs₁ : s₁.length = 0
⊢ s₂.length = 0

Tactic:
have : Fin.last s₂.length = (0 : Fin s₂.length.succ) :=
  s₂.injective (hb.symm.trans ((congr_arg s₁ (Fin.ext (by simp [hs₁]))).trans ht)).symm

Result:
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s₁ s₂ : CompositionSeries X
hb : head s₁ = head s₂
ht : last s₁ = last s₂
hs₁ : s₁.length = 0
this : Fin.last s₂.length = 0
⊢ s₂.length = 0

Proof state:
X : Type u
inst✝¹ : Lattice X
inst✝ : JordanHolderLattice X
s₁ s₂ : CompositionSeries X
hb : head s₁ = head s₂
ht : last s₁ = last s₂
hs₁ : s₁.length = 0
⊢ ↑0 = ↑(Fin.last s₁.length)

Tactic:
simp [hs₁]

Result:
no goals
-- Mathlib/Topology/Order/Priestley.lean
theorem exists_isClopen_upper_or_lower_of_ne (h : x ≠ y) :
    ∃ U : Set α, IsClopen U ∧ (IsUpperSet U ∨ IsLowerSet U) ∧ x ∈ U ∧ y ∉ U

Proof state:
case inr
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : PartialOrder α
inst✝ : PriestleySpace α
x y : α
h✝ : x ≠ y
h : ¬y ≤ x
⊢ ∃ U, IsClopen U ∧ (IsUpperSet U ∨ IsLowerSet U) ∧ x ∈ U ∧ y ∉ U

Tactic:
obtain ⟨U, hU, hU', hy, hx⟩ := exists_isClopen_lower_of_not_le h

Result:
case inr.intro.intro.intro.intro
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : PartialOrder α
inst✝ : PriestleySpace α
x y : α
h✝ : x ≠ y
h : ¬y ≤ x
U : Set α
hU : IsClopen U
hU' : IsLowerSet U
hy : y ∉ U
hx : x ∈ U
⊢ ∃ U, IsClopen U ∧ (IsUpperSet U ∨ IsLowerSet U) ∧ x ∈ U ∧ y ∉ U

Proof state:
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : PartialOrder α
inst✝ : PriestleySpace α
x y : α
h : x ≠ y
⊢ ∃ U, IsClopen U ∧ (IsUpperSet U ∨ IsLowerSet U) ∧ x ∈ U ∧ y ∉ U

Tactic:
obtain h | h := h.not_le_or_not_le

Result:
case inl
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : PartialOrder α
inst✝ : PriestleySpace α
x y : α
h✝ : x ≠ y
h : ¬x ≤ y
⊢ ∃ U, IsClopen U ∧ (IsUpperSet U ∨ IsLowerSet U) ∧ x ∈ U ∧ y ∉ U

case inr
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : PartialOrder α
inst✝ : PriestleySpace α
x y : α
h✝ : x ≠ y
h : ¬y ≤ x
⊢ ∃ U, IsClopen U ∧ (IsUpperSet U ∨ IsLowerSet U) ∧ x ∈ U ∧ y ∉ U

Proof state:
case inl
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : PartialOrder α
inst✝ : PriestleySpace α
x y : α
h✝ : x ≠ y
h : ¬x ≤ y
⊢ ∃ U, IsClopen U ∧ (IsUpperSet U ∨ IsLowerSet U) ∧ x ∈ U ∧ y ∉ U

Tactic:
exact (exists_isClopen_upper_of_not_le h).imp fun _ ↦ And.imp_right <| And.imp_left Or.inl

Result:
no goals

Proof state:
case inr.intro.intro.intro.intro
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : PartialOrder α
inst✝ : PriestleySpace α
x y : α
h✝ : x ≠ y
h : ¬y ≤ x
U : Set α
hU : IsClopen U
hU' : IsLowerSet U
hy : y ∉ U
hx : x ∈ U
⊢ ∃ U, IsClopen U ∧ (IsUpperSet U ∨ IsLowerSet U) ∧ x ∈ U ∧ y ∉ U

Tactic:
exact ⟨U, hU, Or.inr hU', hx, hy⟩

Result:
no goals
-- Mathlib/MeasureTheory/Measure/MeasureSpaceDef.lean
theorem measure_eq_extend (hs : MeasurableSet s) :
    μ s = extend (fun t (_ht : MeasurableSet t) => μ t) s

Proof state:
case h
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
⊢ MeasurableSet s

Tactic:
exact hs

Result:
no goals

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
⊢ μ s = extend (fun t _ht => μ t) s

Tactic:
rw [extend_eq]

Result:
case h
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
⊢ MeasurableSet s
-- Mathlib/Order/ConditionallyCompleteLattice/Basic.lean
theorem WithTop.coe_sSup' [SupSet α] {s : Set α} (hs : BddAbove s) :
    ↑(sSup s) = (sSup ((fun (a : α) ↦ ↑a) '' s) : WithTop α)

Proof state:
case h
α : Type u_1
inst✝¹ : Preorder α
inst✝ : SupSet α
s : Set α
hs : BddAbove s
⊢ Injective fun a => ↑a

Tactic:
exact Option.some_injective _

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : Preorder α
inst✝ : SupSet α
s : Set α
hs : BddAbove s
⊢ ↑(sSup s) = sSup ((fun a => ↑a) '' s)

Tactic:
change _ = ite _ _ _

Result:
α : Type u_1
inst✝¹ : Preorder α
inst✝ : SupSet α
s : Set α
hs : BddAbove s
⊢ ↑(sSup s) =
    if ⊤ ∈ (fun a => ↑a) '' s then ⊤
    else
      if BddAbove ((fun a => ↑a) ⁻¹' ((fun a => ↑a) '' s)) then ↑(sSup ((fun a => ↑a) ⁻¹' ((fun a => ↑a) '' s))) else ⊤

Proof state:
α : Type u_1
inst✝¹ : Preorder α
inst✝ : SupSet α
s : Set α
hs : BddAbove s
⊢ ↑(sSup s) =
    if ⊤ ∈ (fun a => ↑a) '' s then ⊤
    else
      if BddAbove ((fun a => ↑a) ⁻¹' ((fun a => ↑a) '' s)) then ↑(sSup ((fun a => ↑a) ⁻¹' ((fun a => ↑a) '' s))) else ⊤

Tactic:
rw [if_neg, preimage_image_eq, if_pos hs]

Result:
case h
α : Type u_1
inst✝¹ : Preorder α
inst✝ : SupSet α
s : Set α
hs : BddAbove s
⊢ Injective fun a => ↑a

case hnc
α : Type u_1
inst✝¹ : Preorder α
inst✝ : SupSet α
s : Set α
hs : BddAbove s
⊢ ⊤ ∉ (fun a => ↑a) '' s

Proof state:
case hnc
α : Type u_1
inst✝¹ : Preorder α
inst✝ : SupSet α
s : Set α
hs : BddAbove s
⊢ ⊤ ∉ (fun a => ↑a) '' s

Tactic:
rintro ⟨x, _, ⟨⟩⟩

Result:
no goals