harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Topology/TietzeExtension.lean
theorem exists_extension_forall_exists_le_ge_of_isClosedEmbedding [Nonempty X] (f : X →ᵇ ℝ)
    {e : X → Y} (he : IsClosedEmbedding e) :
    ∃ g : Y →ᵇ ℝ, (∀ y, ∃ x₁ x₂, g y ∈ Icc (f x₁) (f x₂)) ∧ g ∘ e = f

Proof state:
case refine_1.intro
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : NormalSpace Y
inst✝ : Nonempty X
f : X →ᵇ ℝ
e : X → Y
he : IsClosedEmbedding e
inhabited_h : Inhabited X
a : ℝ
ha : IsGLB (range ⇑f) a
g : Y →ᵇ ℝ
hgf : ⇑g ∘ e = ⇑f
xl : Y → X
hxl : ∀ (y : Y), f (xl y) ≤ g y
x : X
hb : IsLUB (range ⇑f) (g (e x))
hmem : ∀ (x_1 : X), f x_1 ∈ Icc a (g (e x))
hle : a ≤ g (e x)
hlt : a < g (e x)
c : ℝ := (a + g (e x)) / 2
hac : a < c
hcb : c < g (e x)
hsub : c - a = g (e x) - c
hgb : ∀ (y : Y), g y ≤ g (e x)
hb' : ¬∃ x_1, f x_1 = g (e x)
⊢ False

Tactic:
exact hb' ⟨x, (congr_fun hgf x).symm⟩

Result:
no goals

Proof state:
case intro.intro
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : NormalSpace Y
inst✝ : Nonempty X
f : X →ᵇ ℝ
e : X → Y
he : IsClosedEmbedding e
inhabited_h : Inhabited X
a : ℝ
ha : IsGLB (range ⇑f) a
b : ℝ
hb : IsLUB (range ⇑f) b
hmem : ∀ (x : X), f x ∈ Icc a b
⊢ ∃ g, (∀ (y : Y), ∃ x₁ x₂, g y ∈ Icc (f x₁) (f x₂)) ∧ ⇑g ∘ e = ⇑f

Tactic:
have hle : a ≤ b := (hmem default).1.trans (hmem default).2

Result:
case intro.intro
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : NormalSpace Y
inst✝ : Nonempty X
f : X →ᵇ ℝ
e : X → Y
he : IsClosedEmbedding e
inhabited_h : Inhabited X
a : ℝ
ha : IsGLB (range ⇑f) a
b : ℝ
hb : IsLUB (range ⇑f) b
hmem : ∀ (x : X), f x ∈ Icc a b
hle : a ≤ b
⊢ ∃ g, (∀ (y : Y), ∃ x₁ x₂, g y ∈ Icc (f x₁) (f x₂)) ∧ ⇑g ∘ e = ⇑f
-- Mathlib/CategoryTheory/Functor/Flat.lean
theorem representablyFlat_op_iff : RepresentablyFlat F.op ↔ RepresentablyCoflat F

Proof state:
case refine_2
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
x✝¹ : RepresentablyCoflat F
x✝ : Dᵒᵖ
X : D
⊢ IsFiltered (CostructuredArrow F X)ᵒᵖᵒᵖ

Tactic:
apply IsFiltered.of_equivalence (opOpEquivalence _)

Result:
no goals

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
⊢ RepresentablyFlat F.op ↔ RepresentablyCoflat F

Tactic:
refine ⟨fun _ => ⟨fun X => ?_⟩, fun _ => ⟨fun ⟨X⟩ => ?_⟩⟩

Result:
case refine_1
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
x✝ : RepresentablyFlat F.op
X : D
⊢ IsFiltered (CostructuredArrow F X)

case refine_2
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
x✝¹ : RepresentablyCoflat F
x✝ : Dᵒᵖ
X : D
⊢ IsCofiltered (StructuredArrow (op X) F.op)

Proof state:
case refine_1
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
x✝ : RepresentablyFlat F.op
X : D
⊢ IsFiltered (CostructuredArrow F X)

Tactic:
suffices IsCofiltered (CostructuredArrow F X)ᵒᵖ from isFiltered_of_isCofiltered_op _

Result:
case refine_1
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
x✝ : RepresentablyFlat F.op
X : D
⊢ IsCofiltered (CostructuredArrow F X)ᵒᵖ

Proof state:
case refine_1
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
x✝ : RepresentablyFlat F.op
X : D
⊢ IsCofiltered (CostructuredArrow F X)ᵒᵖ

Tactic:
apply IsCofiltered.of_equivalence (costructuredArrowOpEquivalence _ _).symm

Result:
no goals

Proof state:
case refine_2
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
x✝¹ : RepresentablyCoflat F
x✝ : Dᵒᵖ
X : D
⊢ IsFiltered (StructuredArrow (op X) F.op)ᵒᵖ

Tactic:
suffices IsFiltered (CostructuredArrow F X)ᵒᵖᵒᵖ from
  IsFiltered.of_equivalence (costructuredArrowOpEquivalence _ _).op

Result:
case refine_2
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
x✝¹ : RepresentablyCoflat F
x✝ : Dᵒᵖ
X : D
⊢ IsFiltered (CostructuredArrow F X)ᵒᵖᵒᵖ

Proof state:
case refine_2
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
x✝¹ : RepresentablyCoflat F
x✝ : Dᵒᵖ
X : D
⊢ IsCofiltered (StructuredArrow (op X) F.op)

Tactic:
suffices IsFiltered (StructuredArrow (op X) F.op)ᵒᵖ from isCofiltered_of_isFiltered_op _

Result:
case refine_2
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
x✝¹ : RepresentablyCoflat F
x✝ : Dᵒᵖ
X : D
⊢ IsFiltered (StructuredArrow (op X) F.op)ᵒᵖ
-- Mathlib/Data/Nat/Factorization/Basic.lean
theorem Ico_filter_pow_dvd_eq {n p b : ℕ} (pp : p.Prime) (hn : n ≠ 0) (hb : n ≤ p ^ b) :
    {i ∈ Ico 1 n | p ^ i ∣ n} = {i ∈ Icc 1 b | p ^ i ∣ n}

Proof state:
case h
n p b : ℕ
pp : Prime p
hn : n ≠ 0
hb : n ≤ p ^ b
x : ℕ
h1 : p ^ x ∣ n
⊢ x < n ↔ x ≤ b

Tactic:
exact iff_of_true (lt_of_pow_dvd_right hn pp.two_le h1) <|
  (Nat.pow_le_pow_iff_right pp.one_lt).1 <| (le_of_dvd hn.bot_lt h1).trans hb

Result:
no goals

Proof state:
n p b : ℕ
pp : Prime p
hn : n ≠ 0
hb : n ≤ p ^ b
⊢ Finset.filter (fun i => p ^ i ∣ n) (Ico 1 n) = Finset.filter (fun i => p ^ i ∣ n) (Icc 1 b)

Tactic:
ext x

Result:
case h
n p b : ℕ
pp : Prime p
hn : n ≠ 0
hb : n ≤ p ^ b
x : ℕ
⊢ x ∈ Finset.filter (fun i => p ^ i ∣ n) (Ico 1 n) ↔ x ∈ Finset.filter (fun i => p ^ i ∣ n) (Icc 1 b)

Proof state:
case h
n p b : ℕ
pp : Prime p
hn : n ≠ 0
hb : n ≤ p ^ b
x : ℕ
⊢ x ∈ Finset.filter (fun i => p ^ i ∣ n) (Ico 1 n) ↔ x ∈ Finset.filter (fun i => p ^ i ∣ n) (Icc 1 b)

Tactic:
simp only [Finset.mem_filter, mem_Ico, mem_Icc, and_congr_left_iff, and_congr_right_iff]

Result:
case h
n p b : ℕ
pp : Prime p
hn : n ≠ 0
hb : n ≤ p ^ b
x : ℕ
⊢ p ^ x ∣ n → 1 ≤ x → (x < n ↔ x ≤ b)

Proof state:
case h
n p b : ℕ
pp : Prime p
hn : n ≠ 0
hb : n ≤ p ^ b
x : ℕ
⊢ p ^ x ∣ n → 1 ≤ x → (x < n ↔ x ≤ b)

Tactic:
rintro h1 -

Result:
case h
n p b : ℕ
pp : Prime p
hn : n ≠ 0
hb : n ≤ p ^ b
x : ℕ
h1 : p ^ x ∣ n
⊢ x < n ↔ x ≤ b
-- Mathlib/LinearAlgebra/Matrix/PosDef.lean
theorem transpose {M : Matrix n n R} (hM : M.PosDef) : Mᵀ.PosDef

Proof state:
n : Type u_2
R : Type u_3
inst✝³ : Fintype n
inst✝² : CommRing R
inst✝¹ : PartialOrder R
inst✝ : StarRing R
M : Matrix n n R
hM : M.PosDef
x : n → R
hx : x ≠ 0
⊢ 0 < star x ⬝ᵥ Mᵀ *ᵥ x

Tactic:
convert hM.2 (star x) (star_ne_zero.2 hx) using 1

Result:
case h.e'_4
n : Type u_2
R : Type u_3
inst✝³ : Fintype n
inst✝² : CommRing R
inst✝¹ : PartialOrder R
inst✝ : StarRing R
M : Matrix n n R
hM : M.PosDef
x : n → R
hx : x ≠ 0
⊢ star x ⬝ᵥ Mᵀ *ᵥ x = star (star x) ⬝ᵥ M *ᵥ star x

Proof state:
n : Type u_2
R : Type u_3
inst✝³ : Fintype n
inst✝² : CommRing R
inst✝¹ : PartialOrder R
inst✝ : StarRing R
M : Matrix n n R
hM : M.PosDef
⊢ Mᵀ.PosDef

Tactic:
refine ⟨IsHermitian.transpose hM.1, fun x hx => ?_⟩

Result:
n : Type u_2
R : Type u_3
inst✝³ : Fintype n
inst✝² : CommRing R
inst✝¹ : PartialOrder R
inst✝ : StarRing R
M : Matrix n n R
hM : M.PosDef
x : n → R
hx : x ≠ 0
⊢ 0 < star x ⬝ᵥ Mᵀ *ᵥ x

Proof state:
case h.e'_4
n : Type u_2
R : Type u_3
inst✝³ : Fintype n
inst✝² : CommRing R
inst✝¹ : PartialOrder R
inst✝ : StarRing R
M : Matrix n n R
hM : M.PosDef
x : n → R
hx : x ≠ 0
⊢ star x ⬝ᵥ Mᵀ *ᵥ x = star (star x) ⬝ᵥ M *ᵥ star x

Tactic:
rw [mulVec_transpose, dotProduct_mulVec, star_star, dotProduct_comm]

Result:
no goals
-- Mathlib/RingTheory/WittVector/Truncated.lean
theorem out_truncateFun (x : 𝕎 R) : (truncateFun n x).out = init n x

Proof state:
case h
p n : ℕ
R : Type u_1
inst✝ : CommRing R
x : 𝕎 R
i : ℕ
⊢ (if h : i < n then TruncatedWittVector.coeff ⟨i, h⟩ (truncateFun n x) else 0) = if i < n then x.coeff i else 0

Tactic:
split_ifs with hi

Result:
case pos
p n : ℕ
R : Type u_1
inst✝ : CommRing R
x : 𝕎 R
i : ℕ
hi : i < n
⊢ TruncatedWittVector.coeff ⟨i, hi⟩ (truncateFun n x) = x.coeff i

case neg
p n : ℕ
R : Type u_1
inst✝ : CommRing R
x : 𝕎 R
i : ℕ
hi : ¬i < n
⊢ 0 = 0

Proof state:
case pos
p n : ℕ
R : Type u_1
inst✝ : CommRing R
x : 𝕎 R
i : ℕ
hi : i < n
⊢ TruncatedWittVector.coeff ⟨i, hi⟩ (truncateFun n x) = x.coeff i

Tactic:
rw [coeff_truncateFun, Fin.val_mk]

Result:
no goals

Proof state:
p n : ℕ
R : Type u_1
inst✝ : CommRing R
x : 𝕎 R
⊢ (truncateFun n x).out = init n x

Tactic:
ext i

Result:
case h
p n : ℕ
R : Type u_1
inst✝ : CommRing R
x : 𝕎 R
i : ℕ
⊢ (truncateFun n x).out.coeff i = (init n x).coeff i

Proof state:
case neg
p n : ℕ
R : Type u_1
inst✝ : CommRing R
x : 𝕎 R
i : ℕ
hi : ¬i < n
⊢ 0 = 0

Tactic:
rfl

Result:
no goals

Proof state:
case pos
p n : ℕ
R : Type u_1
inst✝ : CommRing R
x : 𝕎 R
i : ℕ
hi : i < n
⊢ TruncatedWittVector.coeff ⟨i, hi⟩ (truncateFun n x) = x.coeff i

case neg
p n : ℕ
R : Type u_1
inst✝ : CommRing R
x : 𝕎 R
i : ℕ
hi : ¬i < n
⊢ 0 = 0

Tactic:
swap

Result:
case neg
p n : ℕ
R : Type u_1
inst✝ : CommRing R
x : 𝕎 R
i : ℕ
hi : ¬i < n
⊢ 0 = 0

case pos
p n : ℕ
R : Type u_1
inst✝ : CommRing R
x : 𝕎 R
i : ℕ
hi : i < n
⊢ TruncatedWittVector.coeff ⟨i, hi⟩ (truncateFun n x) = x.coeff i

Proof state:
case h
p n : ℕ
R : Type u_1
inst✝ : CommRing R
x : 𝕎 R
i : ℕ
⊢ (truncateFun n x).out.coeff i = (init n x).coeff i

Tactic:
dsimp [TruncatedWittVector.out, init, select, coeff_mk]

Result:
case h
p n : ℕ
R : Type u_1
inst✝ : CommRing R
x : 𝕎 R
i : ℕ
⊢ (if h : i < n then TruncatedWittVector.coeff ⟨i, h⟩ (truncateFun n x) else 0) = if i < n then x.coeff i else 0
-- Mathlib/RingTheory/Multiplicity.lean
theorem emultiplicity_pow_self {p : α} (h0 : p ≠ 0) (hu : ¬IsUnit p) (n : ℕ) :
    emultiplicity p (p ^ n) = n

Proof state:
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
p : α
h0 : p ≠ 0
hu : ¬IsUnit p
n : ℕ
⊢ emultiplicity p (p ^ n) = ↑n

Tactic:
apply emultiplicity_eq_of_dvd_of_not_dvd

Result:
case hk
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
p : α
h0 : p ≠ 0
hu : ¬IsUnit p
n : ℕ
⊢ p ^ n ∣ p ^ n

case hsucc
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
p : α
h0 : p ≠ 0
hu : ¬IsUnit p
n : ℕ
⊢ ¬p ^ (n + 1) ∣ p ^ n

Proof state:
case hk
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
p : α
h0 : p ≠ 0
hu : ¬IsUnit p
n : ℕ
⊢ p ^ n ∣ p ^ n

Tactic:
rfl

Result:
no goals

Proof state:
case hsucc
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
p : α
h0 : p ≠ 0
hu : ¬IsUnit p
n : ℕ
⊢ ¬p ^ (n + 1) ∣ p ^ n

Tactic:
rw [pow_dvd_pow_iff h0 hu]

Result:
case hsucc
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
p : α
h0 : p ≠ 0
hu : ¬IsUnit p
n : ℕ
⊢ ¬n + 1 ≤ n

Proof state:
case hsucc
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
p : α
h0 : p ≠ 0
hu : ¬IsUnit p
n : ℕ
⊢ ¬n + 1 ≤ n

Tactic:
apply Nat.not_succ_le_self

Result:
no goals
-- Mathlib/Topology/UniformSpace/Equicontinuity.lean
theorem equicontinuousWithinAt_iff_continuousWithinAt {F : ι → X → α} {S : Set X} {x₀ : X} :
    EquicontinuousWithinAt F S x₀ ↔
    ContinuousWithinAt (ofFun ∘ Function.swap F : X → ι →ᵤ α) S x₀

Proof state:
ι : Type u_1
X : Type u_3
α : Type u_6
tX : TopologicalSpace X
uα : UniformSpace α
F : ι → X → α
S : Set X
x₀ : X
⊢ EquicontinuousWithinAt F S x₀ ↔
    ∀ i ∈ 𝓤 α, ∀ᶠ (x : X) in 𝓝[S] x₀, (⇑ofFun ∘ swap F) x ∈ {g | ((⇑ofFun ∘ swap F) x₀, g) ∈ UniformFun.gen ι α i}

Tactic:
rfl

Result:
no goals

Proof state:
ι : Type u_1
X : Type u_3
α : Type u_6
tX : TopologicalSpace X
uα : UniformSpace α
F : ι → X → α
S : Set X
x₀ : X
⊢ EquicontinuousWithinAt F S x₀ ↔ ContinuousWithinAt (⇑ofFun ∘ swap F) S x₀

Tactic:
rw [ContinuousWithinAt, (UniformFun.hasBasis_nhds ι α _).tendsto_right_iff]

Result:
ι : Type u_1
X : Type u_3
α : Type u_6
tX : TopologicalSpace X
uα : UniformSpace α
F : ι → X → α
S : Set X
x₀ : X
⊢ EquicontinuousWithinAt F S x₀ ↔
    ∀ i ∈ 𝓤 α, ∀ᶠ (x : X) in 𝓝[S] x₀, (⇑ofFun ∘ swap F) x ∈ {g | ((⇑ofFun ∘ swap F) x₀, g) ∈ UniformFun.gen ι α i}
-- Mathlib/Analysis/Calculus/FDeriv/Equiv.lean
theorem ContinuousLinearEquiv.uniqueDiffOn_preimage_iff (e : F ≃L[𝕜] E) :
    UniqueDiffOn 𝕜 (e ⁻¹' s) ↔ UniqueDiffOn 𝕜 s

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
s : Set E
e : F ≃L[𝕜] E
⊢ UniqueDiffOn 𝕜 (⇑e ⁻¹' s) ↔ UniqueDiffOn 𝕜 s

Tactic:
rw [← e.image_symm_eq_preimage, e.symm.uniqueDiffOn_image_iff]

Result:
no goals
-- Mathlib/RingTheory/PowerSeries/Trunc.lean
@[simp]
lemma trunc_C_mul (n : ℕ) (r : R) (f : R⟦X⟧) : trunc n (C R r * f) = .C r * trunc n f

Proof state:
case a
R : Type u_1
inst✝ : Semiring R
n : ℕ
r : R
f : R⟦X⟧
i : ℕ
⊢ (trunc n ((C R) r * f)).coeff i = (Polynomial.C r * trunc n f).coeff i

Tactic:
simp [coeff_trunc]

Result:
no goals

Proof state:
R : Type u_1
inst✝ : Semiring R
n : ℕ
r : R
f : R⟦X⟧
⊢ trunc n ((C R) r * f) = Polynomial.C r * trunc n f

Tactic:
ext i

Result:
case a
R : Type u_1
inst✝ : Semiring R
n : ℕ
r : R
f : R⟦X⟧
i : ℕ
⊢ (trunc n ((C R) r * f)).coeff i = (Polynomial.C r * trunc n f).coeff i
-- Mathlib/Data/Matroid/Dual.lean
theorem coindep_iff_exists (hX : X ⊆ M.E

Proof state:
α : Type u_1
M : Matroid α
X : Set α
hX : autoParam (X ⊆ M.E) _auto✝
⊢ M.Coindep X ↔ ∃ B, M.IsBase B ∧ B ⊆ M.E \ X

Tactic:
rw [coindep_iff_exists', and_iff_left hX]

Result:
no goals
-- Mathlib/Data/Ordmap/Ordset.lean
theorem balanceL_eq_balance' {l x r} (hl : Balanced l) (hr : Balanced r) (sl : Sized l)
    (sr : Sized r)
    (H :
      (∃ l', Raised l' (size l) ∧ BalancedSz l' (size r)) ∨
        ∃ r', Raised (size r) r' ∧ BalancedSz (size l) r') :
    @balanceL α l x r = balance' l x r

Proof state:
case H1
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
hl : l.Balanced
hr : r.Balanced
sl : l.Sized
sr : r.Sized
H : (∃ l', Raised l' l.size ∧ BalancedSz l' r.size) ∨ ∃ r', Raised r.size r' ∧ BalancedSz l.size r'
⊢ l.size = 0 → r.size ≤ 1

Tactic:
intro l0

Result:
case H1
α : Type u_1
l : Ordnode α
x : α
r : Ordnode α
hl : l.Balanced
hr : r.Balanced
sl : l.Sized
sr : r.Sized
H : (∃ l', Raised l' l.size ∧ BalancedSz l' r.size) ∨ ∃ r', Raised r.size r' ∧ BalancedSz l.size r'
l0 : l.size = 0
⊢ r.size ≤ 1
-- Mathlib/LinearAlgebra/Vandermonde.lean
theorem vandermonde_succ {n : ℕ} (v : Fin n.succ → R) :
    vandermonde v = .of
      Fin.cons (fun (j : Fin n.succ) => v 0 ^ (j : ℕ)) fun i =>
        Fin.cons 1 fun j => v i.succ * vandermonde (Fin.tail v) i j

Proof state:
R : Type u_1
inst✝ : CommRing R
n : ℕ
v : Fin n.succ → R
⊢ vandermonde v = of Fin.cons (fun j => v 0 ^ ↑j) fun i => Fin.cons 1 fun j => v i.succ * vandermonde (Fin.tail v) i j

Tactic:
conv_lhs => rw [← Fin.cons_self_tail v, vandermonde_cons]

Result:
R : Type u_1
inst✝ : CommRing R
n : ℕ
v : Fin n.succ → R
⊢ (Fin.cons (fun j => v 0 ^ ↑j) fun i => Fin.cons 1 fun j => Fin.tail v i * vandermonde (Fin.tail v) i j) =
    of Fin.cons (fun j => v 0 ^ ↑j) fun i => Fin.cons 1 fun j => v i.succ * vandermonde (Fin.tail v) i j

Proof state:
R : Type u_1
inst✝ : CommRing R
n : ℕ
v : Fin n.succ → R
⊢ (Fin.cons (fun j => v 0 ^ ↑j) fun i => Fin.cons 1 fun j => Fin.tail v i * vandermonde (Fin.tail v) i j) =
    of Fin.cons (fun j => v 0 ^ ↑j) fun i => Fin.cons 1 fun j => v i.succ * vandermonde (Fin.tail v) i j

Tactic:
rfl

Result:
no goals
-- Mathlib/Analysis/Calculus/MeanValue.lean
/-- Let `f` be a function continuous on a convex (or, equivalently, connected) subset `D`
of the real line. If `f` is differentiable on the interior of `D` and `f'` is nonpositive, then
`f` is an antitone function on `D`. -/
lemma antitoneOn_of_hasDerivWithinAt_nonpos {D : Set ℝ} (hD : Convex ℝ D) {f f' : ℝ → ℝ}
    (hf : ContinuousOn f D) (hf' : ∀ x ∈ interior D, HasDerivWithinAt f (f' x) (interior D) x)
    (hf'₀ : ∀ x ∈ interior D, f' x ≤ 0) : AntitoneOn f D :=
  antitoneOn_of_deriv_nonpos hD hf (fun _ hx ↦ (hf' _ hx).differentiableWithinAt) fun x hx ↦ by
    rw [deriv_eqOn isOpen_interior hf' hx]; exact hf'₀ _ hx

Proof state:
D : Set ℝ
hD : Convex ℝ D
f f' : ℝ → ℝ
hf : ContinuousOn f D
hf' : ∀ x ∈ interior D, HasDerivWithinAt f (f' x) (interior D) x
hf'₀ : ∀ x ∈ interior D, f' x ≤ 0
x : ℝ
hx : x ∈ interior D
⊢ deriv f x ≤ 0

Tactic:
rw [deriv_eqOn isOpen_interior hf' hx]

Result:
D : Set ℝ
hD : Convex ℝ D
f f' : ℝ → ℝ
hf : ContinuousOn f D
hf' : ∀ x ∈ interior D, HasDerivWithinAt f (f' x) (interior D) x
hf'₀ : ∀ x ∈ interior D, f' x ≤ 0
x : ℝ
hx : x ∈ interior D
⊢ f' x ≤ 0

Proof state:
D : Set ℝ
hD : Convex ℝ D
f f' : ℝ → ℝ
hf : ContinuousOn f D
hf' : ∀ x ∈ interior D, HasDerivWithinAt f (f' x) (interior D) x
hf'₀ : ∀ x ∈ interior D, f' x ≤ 0
x : ℝ
hx : x ∈ interior D
⊢ f' x ≤ 0

Tactic:
exact hf'₀ _ hx

Result:
no goals
-- Mathlib/Data/Set/Image.lean
theorem range_subtype_map {p : α → Prop} {q : β → Prop} (f : α → β) (h : ∀ x, p x → q (f x)) :
    range (Subtype.map f h) = (↑) ⁻¹' (f '' { x | p x })

Proof state:
α : Type u_1
β : Type u_2
p : α → Prop
q : β → Prop
f : α → β
h : ∀ (x : α), p x → q (f x)
⊢ range (Subtype.map f h) = Subtype.val ⁻¹' (f '' {x | p x})

Tactic:
ext ⟨x, hx⟩

Result:
case h.mk
α : Type u_1
β : Type u_2
p : α → Prop
q : β → Prop
f : α → β
h : ∀ (x : α), p x → q (f x)
x : β
hx : q x
⊢ ⟨x, hx⟩ ∈ range (Subtype.map f h) ↔ ⟨x, hx⟩ ∈ Subtype.val ⁻¹' (f '' {x | p x})

Proof state:
case h.mk
α : Type u_1
β : Type u_2
p : α → Prop
q : β → Prop
f : α → β
h : ∀ (x : α), p x → q (f x)
x : β
hx : q x
⊢ ⟨x, hx⟩ ∈ range (Subtype.map f h) ↔ ⟨x, hx⟩ ∈ Subtype.val ⁻¹' (f '' {x | p x})

Tactic:
simp_rw [mem_preimage, mem_range, mem_image, Subtype.exists, Subtype.map]

Result:
case h.mk
α : Type u_1
β : Type u_2
p : α → Prop
q : β → Prop
f : α → β
h : ∀ (x : α), p x → q (f x)
x : β
hx : q x
⊢ (∃ a, ∃ (h_1 : p a), ⟨f a, ⋯⟩ = ⟨x, hx⟩) ↔ ∃ x_1 ∈ {x | p x}, f x_1 = x

Proof state:
case h.mk
α : Type u_1
β : Type u_2
p : α → Prop
q : β → Prop
f : α → β
h : ∀ (x : α), p x → q (f x)
x : β
hx : q x
⊢ (∃ a, ∃ (h_1 : p a), ⟨f a, ⋯⟩ = ⟨x, hx⟩) ↔ ∃ x_1 ∈ {x | p x}, f x_1 = x

Tactic:
simp only [Subtype.mk.injEq, exists_prop, mem_setOf_eq]

Result:
no goals
-- Mathlib/LinearAlgebra/AffineSpace/AffineSubspace/Defs.lean
theorem vadd_mem_iff_mem_of_mem_direction {s : AffineSubspace k P} {v : V} (hv : v ∈ s.direction)
    {p : P} : v +ᵥ p ∈ s ↔ p ∈ s

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
v : V
hv : v ∈ s.direction
p : P
⊢ v +ᵥ p ∈ s ↔ p ∈ s

Tactic:
refine ⟨fun h => ?_, fun h => vadd_mem_of_mem_direction hv h⟩

Result:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
v : V
hv : v ∈ s.direction
p : P
h : v +ᵥ p ∈ s
⊢ p ∈ s

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
v : V
hv : v ∈ s.direction
p : P
h : v +ᵥ p ∈ s
⊢ p ∈ s

Tactic:
convert vadd_mem_of_mem_direction (Submodule.neg_mem _ hv) h

Result:
case h.e'_5
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
v : V
hv : v ∈ s.direction
p : P
h : v +ᵥ p ∈ s
⊢ p = -v +ᵥ v +ᵥ p

Proof state:
case h.e'_5
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
inst✝ : AffineSpace V P
s : AffineSubspace k P
v : V
hv : v ∈ s.direction
p : P
h : v +ᵥ p ∈ s
⊢ p = -v +ᵥ v +ᵥ p

Tactic:
simp

Result:
no goals
-- Mathlib/Probability/Martingale/Upcrossing.lean
theorem Adapted.upcrossingStrat_adapted (hf : Adapted ℱ f) :
    Adapted ℱ (upcrossingStrat a b f N)

Proof state:
Ω : Type u_1
m0 : MeasurableSpace Ω
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ℱ : Filtration ℕ m0
hf : Adapted ℱ f
⊢ Adapted ℱ (upcrossingStrat a b f N)

Tactic:
intro n

Result:
Ω : Type u_1
m0 : MeasurableSpace Ω
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ℱ : Filtration ℕ m0
hf : Adapted ℱ f
n : ℕ
⊢ StronglyMeasurable (upcrossingStrat a b f N n)

Proof state:
Ω : Type u_1
m0 : MeasurableSpace Ω
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ℱ : Filtration ℕ m0
hf : Adapted ℱ f
n : ℕ
⊢ StronglyMeasurable (upcrossingStrat a b f N n)

Tactic:
change StronglyMeasurable[ℱ n] fun ω =>
  ∑ k ∈ Finset.range N, ({n | lowerCrossingTime a b f N k ω ≤ n} ∩
    {n | n < upperCrossingTime a b f N (k + 1) ω}).indicator 1 n

Result:
Ω : Type u_1
m0 : MeasurableSpace Ω
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ℱ : Filtration ℕ m0
hf : Adapted ℱ f
n : ℕ
⊢ StronglyMeasurable fun ω =>
    ∑ k ∈ Finset.range N,
      ({n | lowerCrossingTime a b f N k ω ≤ n} ∩ {n | n < upperCrossingTime a b f N (k + 1) ω}).indicator 1 n

Proof state:
Ω : Type u_1
m0 : MeasurableSpace Ω
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ℱ : Filtration ℕ m0
hf : Adapted ℱ f
n : ℕ
⊢ StronglyMeasurable fun ω =>
    ∑ k ∈ Finset.range N,
      ({n | lowerCrossingTime a b f N k ω ≤ n} ∩ {n | n < upperCrossingTime a b f N (k + 1) ω}).indicator 1 n

Tactic:
refine Finset.stronglyMeasurable_sum _ fun i _ =>
  stronglyMeasurable_const.indicator ((hf.isStoppingTime_lowerCrossingTime n).inter ?_)

Result:
Ω : Type u_1
m0 : MeasurableSpace Ω
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ℱ : Filtration ℕ m0
hf : Adapted ℱ f
n i : ℕ
x✝ : i ∈ Finset.range N
⊢ MeasurableSet fun ω => {n | n < upperCrossingTime a b f N (i + 1) ω} n

Proof state:
Ω : Type u_1
m0 : MeasurableSpace Ω
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ℱ : Filtration ℕ m0
hf : Adapted ℱ f
n i : ℕ
x✝ : i ∈ Finset.range N
⊢ MeasurableSet fun ω => {n | n < upperCrossingTime a b f N (i + 1) ω} n

Tactic:
simp_rw [← not_le]

Result:
Ω : Type u_1
m0 : MeasurableSpace Ω
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ℱ : Filtration ℕ m0
hf : Adapted ℱ f
n i : ℕ
x✝ : i ∈ Finset.range N
⊢ MeasurableSet fun ω => {n | ¬upperCrossingTime a b f N (i + 1) ω ≤ n} n

Proof state:
Ω : Type u_1
m0 : MeasurableSpace Ω
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ℱ : Filtration ℕ m0
hf : Adapted ℱ f
n i : ℕ
x✝ : i ∈ Finset.range N
⊢ MeasurableSet fun ω => {n | ¬upperCrossingTime a b f N (i + 1) ω ≤ n} n

Tactic:
exact (hf.isStoppingTime_upperCrossingTime n).compl

Result:
no goals