harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/CStarAlgebra/Basic.lean
theorem IsSelfAdjoint.nnnorm_pow_two_pow [NormedRing E] [StarRing E] [CStarRing E] {x : E}
    (hx : IsSelfAdjoint x) (n : ℕ) : ‖x ^ 2 ^ n‖₊ = ‖x‖₊ ^ 2 ^ n

Proof state:
case zero
E : Type u_2
inst✝² : NormedRing E
inst✝¹ : StarRing E
inst✝ : CStarRing E
x : E
hx : IsSelfAdjoint x
⊢ ‖x ^ 2 ^ 0‖₊ = ‖x‖₊ ^ 2 ^ 0

Tactic:
simp only [pow_zero, pow_one]

Result:
no goals

Proof state:
E : Type u_2
inst✝² : NormedRing E
inst✝¹ : StarRing E
inst✝ : CStarRing E
x : E
hx : IsSelfAdjoint x
n : ℕ
⊢ ‖x ^ 2 ^ n‖₊ = ‖x‖₊ ^ 2 ^ n

Tactic:
induction' n with k hk

Result:
case zero
E : Type u_2
inst✝² : NormedRing E
inst✝¹ : StarRing E
inst✝ : CStarRing E
x : E
hx : IsSelfAdjoint x
⊢ ‖x ^ 2 ^ 0‖₊ = ‖x‖₊ ^ 2 ^ 0

case succ
E : Type u_2
inst✝² : NormedRing E
inst✝¹ : StarRing E
inst✝ : CStarRing E
x : E
hx : IsSelfAdjoint x
k : ℕ
hk : ‖x ^ 2 ^ k‖₊ = ‖x‖₊ ^ 2 ^ k
⊢ ‖x ^ 2 ^ (k + 1)‖₊ = ‖x‖₊ ^ 2 ^ (k + 1)

Proof state:
case succ
E : Type u_2
inst✝² : NormedRing E
inst✝¹ : StarRing E
inst✝ : CStarRing E
x : E
hx : IsSelfAdjoint x
k : ℕ
hk : ‖x ^ 2 ^ k‖₊ = ‖x‖₊ ^ 2 ^ k
⊢ ‖x ^ 2 ^ (k + 1)‖₊ = ‖x‖₊ ^ 2 ^ (k + 1)

Tactic:
rw [pow_succ', pow_mul', sq]

Result:
case succ
E : Type u_2
inst✝² : NormedRing E
inst✝¹ : StarRing E
inst✝ : CStarRing E
x : E
hx : IsSelfAdjoint x
k : ℕ
hk : ‖x ^ 2 ^ k‖₊ = ‖x‖₊ ^ 2 ^ k
⊢ ‖x ^ 2 ^ k * x ^ 2 ^ k‖₊ = ‖x‖₊ ^ (2 * 2 ^ k)

Proof state:
case succ
E : Type u_2
inst✝² : NormedRing E
inst✝¹ : StarRing E
inst✝ : CStarRing E
x : E
hx : IsSelfAdjoint x
k : ℕ
hk : ‖x ^ 2 ^ k‖₊ = ‖x‖₊ ^ 2 ^ k
⊢ ‖x ^ 2 ^ k * x ^ 2 ^ k‖₊ = ‖x‖₊ ^ (2 * 2 ^ k)

Tactic:
nth_rw 1 [← selfAdjoint.mem_iff.mp hx]

Result:
case succ
E : Type u_2
inst✝² : NormedRing E
inst✝¹ : StarRing E
inst✝ : CStarRing E
x : E
hx : IsSelfAdjoint x
k : ℕ
hk : ‖x ^ 2 ^ k‖₊ = ‖x‖₊ ^ 2 ^ k
⊢ ‖x⋆ ^ 2 ^ k * x ^ 2 ^ k‖₊ = ‖x‖₊ ^ (2 * 2 ^ k)

Proof state:
case succ
E : Type u_2
inst✝² : NormedRing E
inst✝¹ : StarRing E
inst✝ : CStarRing E
x : E
hx : IsSelfAdjoint x
k : ℕ
hk : ‖x ^ 2 ^ k‖₊ = ‖x‖₊ ^ 2 ^ k
⊢ ‖x⋆ ^ 2 ^ k * x ^ 2 ^ k‖₊ = ‖x‖₊ ^ (2 * 2 ^ k)

Tactic:
rw [← star_pow, CStarRing.nnnorm_star_mul_self, ← sq, hk, pow_mul']

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Zip.lean
theorem reverse_zipWith (h : l.size = l'.size) :
    (zipWith f l l').reverse = zipWith f l.reverse l'.reverse

Proof state:
case mk
α✝² : Type u_1
α✝¹ : Type u_2
α✝ : Type u_3
f : α✝² → α✝¹ → α✝
l' : Array α✝¹
toList✝ : List α✝²
h : { toList := toList✝ }.size = l'.size
⊢ (zipWith f { toList := toList✝ } l').reverse = zipWith f { toList := toList✝ }.reverse l'.reverse

Tactic:
cases l'

Result:
case mk.mk
α✝² : Type u_1
α✝¹ : Type u_2
α✝ : Type u_3
f : α✝² → α✝¹ → α✝
toList✝¹ : List α✝²
toList✝ : List α✝¹
h : { toList := toList✝¹ }.size = { toList := toList✝ }.size
⊢ (zipWith f { toList := toList✝¹ } { toList := toList✝ }).reverse =
    zipWith f { toList := toList✝¹ }.reverse { toList := toList✝ }.reverse

Proof state:
α✝² : Type u_1
α✝¹ : Type u_2
α✝ : Type u_3
f : α✝² → α✝¹ → α✝
toList✝¹ : List α✝²
toList✝ : List α✝¹
h : { toList := toList✝¹ }.size = { toList := toList✝ }.size
⊢ List.length ?m.25122 = List.length ?m.25123

Tactic:
simpa using h

Result:
no goals

Proof state:
α✝² : Type u_1
α✝¹ : Type u_2
α✝ : Type u_3
f : α✝² → α✝¹ → α✝
l : Array α✝²
l' : Array α✝¹
h : l.size = l'.size
⊢ (zipWith f l l').reverse = zipWith f l.reverse l'.reverse

Tactic:
cases l

Result:
case mk
α✝² : Type u_1
α✝¹ : Type u_2
α✝ : Type u_3
f : α✝² → α✝¹ → α✝
l' : Array α✝¹
toList✝ : List α✝²
h : { toList := toList✝ }.size = l'.size
⊢ (zipWith f { toList := toList✝ } l').reverse = zipWith f { toList := toList✝ }.reverse l'.reverse

Proof state:
case mk.mk
α✝² : Type u_1
α✝¹ : Type u_2
α✝ : Type u_3
f : α✝² → α✝¹ → α✝
toList✝¹ : List α✝²
toList✝ : List α✝¹
h : { toList := toList✝¹ }.size = { toList := toList✝ }.size
⊢ (zipWith f { toList := toList✝¹ } { toList := toList✝ }).reverse =
    zipWith f { toList := toList✝¹ }.reverse { toList := toList✝ }.reverse

Tactic:
simp [List.reverse_zipWith (by simpa using h)]

Result:
no goals
-- Mathlib/RingTheory/GradedAlgebra/Homogeneous/Submodule.lean
theorem HomogeneousSubmodule.toSubmodule_injective :
    Function.Injective
      (HomogeneousSubmodule.toSubmodule : HomogeneousSubmodule 𝒜 ℳ → Submodule A M) :=
  fun ⟨x, hx⟩ ⟨y, hy⟩ ↦ fun (h : x = y) ↦ by simp [h]

Proof state:
ιA : Type u_1
ιM : Type u_2
σA : Type u_3
σM : Type u_4
A : Type u_5
M : Type u_6
inst✝¹³ : Semiring A
inst✝¹² : AddCommMonoid M
inst✝¹¹ : Module A M
𝒜 : ιA → σA
ℳ : ιM → σM
inst✝¹⁰ : DecidableEq ιA
inst✝⁹ : AddMonoid ιA
inst✝⁸ : SetLike σA A
inst✝⁷ : AddSubmonoidClass σA A
inst✝⁶ : GradedRing 𝒜
inst✝⁵ : DecidableEq ιM
inst✝⁴ : SetLike σM M
inst✝³ : AddSubmonoidClass σM M
inst✝² : Decomposition ℳ
inst✝¹ : VAdd ιA ιM
inst✝ : GradedSMul 𝒜 ℳ
x✝¹ x✝ : HomogeneousSubmodule 𝒜 ℳ
x : Submodule A M
hx : x.IsHomogeneous ℳ
y : Submodule A M
hy : y.IsHomogeneous ℳ
h : x = y
⊢ { toSubmodule := x, is_homogeneous' := hx } = { toSubmodule := y, is_homogeneous' := hy }

Tactic:
simp [h]

Result:
no goals
-- Mathlib/Analysis/Normed/Lp/ProdLp.lean
theorem prod_nnnorm_eq_sup (f : WithLp ∞ (α × β)) : ‖f‖₊ = ‖f.fst‖₊ ⊔  ‖f.snd‖₊

Proof state:
α : Type u_2
β : Type u_3
inst✝¹ : SeminormedAddCommGroup α
inst✝ : SeminormedAddCommGroup β
f : WithLp ⊤ (α × β)
⊢ ‖f‖₊ = ‖f.1‖₊ ⊔ ‖f.2‖₊

Tactic:
ext

Result:
case a
α : Type u_2
β : Type u_3
inst✝¹ : SeminormedAddCommGroup α
inst✝ : SeminormedAddCommGroup β
f : WithLp ⊤ (α × β)
⊢ ↑‖f‖₊ = ↑(‖f.1‖₊ ⊔ ‖f.2‖₊)

Proof state:
case a
α : Type u_2
β : Type u_3
inst✝¹ : SeminormedAddCommGroup α
inst✝ : SeminormedAddCommGroup β
f : WithLp ⊤ (α × β)
⊢ ↑‖f‖₊ = ↑(‖f.1‖₊ ⊔ ‖f.2‖₊)

Tactic:
norm_cast

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Sort/Lemmas.lean
theorem length_merge (s : α → α → Bool) (l r) :
    (merge l r s).length = l.length + r.length

Proof state:
case isFalse
α : Type u_1
s : α → α → Bool
l✝ r✝ : List α
a : α
l : List α
b : α
r : List α
h✝ : ¬s a b = true
⊢ (b :: (a :: l).merge r s).length = (a :: l).length + (b :: r).length

Tactic:
simp_arith [length_merge s (a::l) r]

Result:
no goals

Proof state:
case isTrue
α : Type u_1
s : α → α → Bool
l✝ r✝ : List α
a : α
l : List α
b : α
r : List α
h✝ : s a b = true
⊢ (a :: l.merge (b :: r) s).length = (a :: l).length + (b :: r).length

Tactic:
simp_arith [length_merge s l (b::r)]

Result:
no goals

Proof state:
α : Type u_1
s : α → α → Bool
l r✝ r : List α
⊢ ([].merge r s).length = [].length + r.length

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
s : α → α → Bool
l✝ r✝ : List α
a : α
l : List α
b : α
r : List α
⊢ ((a :: l).merge (b :: r) s).length = (a :: l).length + (b :: r).length

Tactic:
rw [cons_merge_cons]

Result:
α : Type u_1
s : α → α → Bool
l✝ r✝ : List α
a : α
l : List α
b : α
r : List α
⊢ (if s a b = true then a :: l.merge (b :: r) s else b :: (a :: l).merge r s).length = (a :: l).length + (b :: r).length

Proof state:
α : Type u_1
s : α → α → Bool
l✝ r l : List α
⊢ (l.merge [] s).length = l.length + [].length

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
s : α → α → Bool
l✝ r✝ : List α
a : α
l : List α
b : α
r : List α
⊢ (if s a b = true then a :: l.merge (b :: r) s else b :: (a :: l).merge r s).length = (a :: l).length + (b :: r).length

Tactic:
split

Result:
case isTrue
α : Type u_1
s : α → α → Bool
l✝ r✝ : List α
a : α
l : List α
b : α
r : List α
h✝ : s a b = true
⊢ (a :: l.merge (b :: r) s).length = (a :: l).length + (b :: r).length

case isFalse
α : Type u_1
s : α → α → Bool
l✝ r✝ : List α
a : α
l : List α
b : α
r : List α
h✝ : ¬s a b = true
⊢ (b :: (a :: l).merge r s).length = (a :: l).length + (b :: r).length
-- Mathlib/RingTheory/Polynomial/Eisenstein/Basic.lean
theorem scaleRoots.isWeaklyEisensteinAt (p : R[X]) {x : R} {P : Ideal R} (hP : x ∈ P) :
    (scaleRoots p x).IsWeaklyEisensteinAt P

Proof state:
R : Type u
inst✝ : CommRing R
p : R[X]
x : R
P : Ideal R
hP : x ∈ P
n✝ : ℕ
i : n✝ < (p.scaleRoots x).natDegree
⊢ (p.scaleRoots x).coeff n✝ ∈ P

Tactic:
rw [coeff_scaleRoots]

Result:
R : Type u
inst✝ : CommRing R
p : R[X]
x : R
P : Ideal R
hP : x ∈ P
n✝ : ℕ
i : n✝ < (p.scaleRoots x).natDegree
⊢ p.coeff n✝ * x ^ (p.natDegree - n✝) ∈ P

Proof state:
R : Type u
inst✝ : CommRing R
p : R[X]
x : R
P : Ideal R
hP : x ∈ P
n✝ : ℕ
i : n✝ < (p.scaleRoots x).natDegree
⊢ p.coeff n✝ * x ^ (p.natDegree - n✝) ∈ P

Tactic:
rw [natDegree_scaleRoots, ← tsub_pos_iff_lt] at i

Result:
R : Type u
inst✝ : CommRing R
p : R[X]
x : R
P : Ideal R
hP : x ∈ P
n✝ : ℕ
i : 0 < p.natDegree - n✝
⊢ p.coeff n✝ * x ^ (p.natDegree - n✝) ∈ P

Proof state:
R : Type u
inst✝ : CommRing R
p : R[X]
x : R
P : Ideal R
hP : x ∈ P
n✝ : ℕ
i : 0 < p.natDegree - n✝
⊢ p.coeff n✝ * x ^ (p.natDegree - n✝) ∈ P

Tactic:
exact Ideal.mul_mem_left _ _ (Ideal.pow_mem_of_mem P hP _ i)

Result:
no goals

Proof state:
R : Type u
inst✝ : CommRing R
p : R[X]
x : R
P : Ideal R
hP : x ∈ P
⊢ (p.scaleRoots x).IsWeaklyEisensteinAt P

Tactic:
refine ⟨fun i => ?_⟩

Result:
R : Type u
inst✝ : CommRing R
p : R[X]
x : R
P : Ideal R
hP : x ∈ P
n✝ : ℕ
i : n✝ < (p.scaleRoots x).natDegree
⊢ (p.scaleRoots x).coeff n✝ ∈ P
-- Mathlib/Analysis/SpecialFunctions/Exp.lean
theorem tendsto_pow_mul_exp_neg_atTop_nhds_zero (n : ℕ) :
    Tendsto (fun x => x ^ n * exp (-x)) atTop (𝓝 0) :=
  (tendsto_inv_atTop_zero.comp (tendsto_exp_div_pow_atTop n)).congr fun x => by
    rw [comp_apply, inv_eq_one_div, div_div_eq_mul_div, one_mul, div_eq_mul_inv, exp_neg]

Proof state:
n : ℕ
x : ℝ
⊢ ((fun r => r⁻¹) ∘ fun x => rexp x / x ^ n) x = x ^ n * rexp (-x)

Tactic:
rw [comp_apply, inv_eq_one_div, div_div_eq_mul_div, one_mul, div_eq_mul_inv, exp_neg]

Result:
no goals
-- Mathlib/Data/Fintype/Basic.lean
theorem Fin.univ_image_getElem' [DecidableEq β] (l : List α) (f : α → β) :
    Finset.univ.image (fun i : Fin l.length => f <| l[(i : Nat)]) = (l.map f).toFinset

Proof state:
α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
l : List α
f : α → β
⊢ image (fun i => f l[↑i]) univ = (List.map f l).toFinset

Tactic:
simp only [univ_image_def, List.ofFn_getElem_eq_map]

Result:
no goals
-- Mathlib/Topology/PartialHomeomorph.lean
theorem partialHomeomorphSubtypeCoe_target : (s.partialHomeomorphSubtypeCoe hs).target = s

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
s : Opens X
hs : Nonempty ↥s
⊢ {x | x ∈ s.carrier} = ↑s

Tactic:
rfl

Result:
no goals

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
s : Opens X
hs : Nonempty ↥s
⊢ (s.partialHomeomorphSubtypeCoe hs).target = ↑s

Tactic:
simp only [partialHomeomorphSubtypeCoe, Subtype.range_coe_subtype, mfld_simps]

Result:
X : Type u_1
inst✝ : TopologicalSpace X
s : Opens X
hs : Nonempty ↥s
⊢ {x | x ∈ s.carrier} = ↑s
-- Mathlib/NumberTheory/ADEInequality.lean
theorem admissible_of_one_lt_sumInv {p q r : ℕ+} (H : 1 < sumInv {p, q, r}) :
    Admissible {p, q, r}

Proof state:
p q r : ℕ+
H : 1 < sumInv {p, q, r}
S : List ℕ+ := sort (fun x1 x2 => x1 ≤ x2) {p, q, r}
hS : List.Sorted (fun x1 x2 => x1 ≤ x2) S
hpqr : {p, q, r} = ↑S
⊢ (∃ q_1 r_1, A' q_1 r_1 = {p, q, r}) ∨
    (∃ r_1, D' r_1 = {p, q, r}) ∨ E' 3 = {p, q, r} ∨ E' 4 = {p, q, r} ∨ E' 5 = {p, q, r}

Tactic:
rw [hpqr]

Result:
p q r : ℕ+
H : 1 < sumInv {p, q, r}
S : List ℕ+ := sort (fun x1 x2 => x1 ≤ x2) {p, q, r}
hS : List.Sorted (fun x1 x2 => x1 ≤ x2) S
hpqr : {p, q, r} = ↑S
⊢ (∃ q r, A' q r = ↑S) ∨ (∃ r, D' r = ↑S) ∨ E' 3 = ↑S ∨ E' 4 = ↑S ∨ E' 5 = ↑S

Proof state:
p q r : ℕ+
S : List ℕ+ := sort (fun x1 x2 => x1 ≤ x2) {p, q, r}
H : 1 < sumInv ↑S
hS : List.Sorted (fun x1 x2 => x1 ≤ x2) S
hpqr : {p, q, r} = ↑S
⊢ S.length = 3

Tactic:
simp only [S, insert_eq_cons, length_sort, card_cons, card_singleton]

Result:
no goals

Proof state:
p q r : ℕ+
H : 1 < sumInv {p, q, r}
S : List ℕ+ := sort (fun x1 x2 => x1 ≤ x2) {p, q, r}
hS : List.Sorted (fun x1 x2 => x1 ≤ x2) S
hpqr : {p, q, r} = ↑S
⊢ (∃ q r, A' q r = ↑S) ∨ (∃ r, D' r = ↑S) ∨ E' 3 = ↑S ∨ E' 4 = ↑S ∨ E' 5 = ↑S

Tactic:
rw [hpqr] at H

Result:
p q r : ℕ+
S : List ℕ+ := sort (fun x1 x2 => x1 ≤ x2) {p, q, r}
H : 1 < sumInv ↑S
hS : List.Sorted (fun x1 x2 => x1 ≤ x2) S
hpqr : {p, q, r} = ↑S
⊢ (∃ q r, A' q r = ↑S) ∨ (∃ r, D' r = ↑S) ∨ E' 3 = ↑S ∨ E' 4 = ↑S ∨ E' 5 = ↑S

Proof state:
p q r : ℕ+
H : 1 < sumInv {p, q, r}
S : List ℕ+ := sort (fun x1 x2 => x1 ≤ x2) {p, q, r}
hS : List.Sorted (fun x1 x2 => x1 ≤ x2) S
⊢ (∃ q_1 r_1, A' q_1 r_1 = {p, q, r}) ∨
    (∃ r_1, D' r_1 = {p, q, r}) ∨ E' 3 = {p, q, r} ∨ E' 4 = {p, q, r} ∨ E' 5 = {p, q, r}

Tactic:
have hpqr : ({p, q, r} : Multiset ℕ+) = S := (sort_eq LE.le {p, q, r}).symm

Result:
p q r : ℕ+
H : 1 < sumInv {p, q, r}
S : List ℕ+ := sort (fun x1 x2 => x1 ≤ x2) {p, q, r}
hS : List.Sorted (fun x1 x2 => x1 ≤ x2) S
hpqr : {p, q, r} = ↑S
⊢ (∃ q_1 r_1, A' q_1 r_1 = {p, q, r}) ∨
    (∃ r_1, D' r_1 = {p, q, r}) ∨ E' 3 = {p, q, r} ∨ E' 4 = {p, q, r} ∨ E' 5 = {p, q, r}

Proof state:
p q r : ℕ+
S : List ℕ+ := sort (fun x1 x2 => x1 ≤ x2) {p, q, r}
H : 1 < sumInv ↑S
hS : List.Sorted (fun x1 x2 => x1 ≤ x2) S
hpqr : {p, q, r} = ↑S
⊢ (∃ q r, A' q r = ↑S) ∨ (∃ r, D' r = ↑S) ∨ E' 3 = ↑S ∨ E' 4 = ↑S ∨ E' 5 = ↑S

Tactic:
apply admissible_of_one_lt_sumInv_aux hS _ H

Result:
p q r : ℕ+
S : List ℕ+ := sort (fun x1 x2 => x1 ≤ x2) {p, q, r}
H : 1 < sumInv ↑S
hS : List.Sorted (fun x1 x2 => x1 ≤ x2) S
hpqr : {p, q, r} = ↑S
⊢ S.length = 3

Proof state:
p q r : ℕ+
H : 1 < sumInv {p, q, r}
⊢ Admissible {p, q, r}

Tactic:
simp only [Admissible]

Result:
p q r : ℕ+
H : 1 < sumInv {p, q, r}
⊢ (∃ q_1 r_1, A' q_1 r_1 = {p, q, r}) ∨
    (∃ r_1, D' r_1 = {p, q, r}) ∨ E' 3 = {p, q, r} ∨ E' 4 = {p, q, r} ∨ E' 5 = {p, q, r}
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem insertMany_list_singleton (h : m.WF)
    {k : α} {v : β} :
    insertMany m [⟨k, v⟩] = m.insert k v

Proof state:
α : Type u
inst✝¹ : BEq α
inst✝ : Hashable α
β : Type v
m : Raw α fun x => β
h : m.WF
k : α
v : β
⊢ (Raw₀.Const.insertMany ⟨m, ⋯⟩ [(k, v)]).val.val = (Raw₀.insert ⟨m, ⋯⟩ k v).val

Tactic:
rw [Raw₀.Const.insertMany_list_singleton]

Result:
no goals

Proof state:
α : Type u
inst✝¹ : BEq α
inst✝ : Hashable α
β : Type v
m : Raw α fun x => β
h : m.WF
k : α
v : β
⊢ insertMany m [(k, v)] = m.insert k v

Tactic:
simp_to_raw

Result:
α : Type u
inst✝¹ : BEq α
inst✝ : Hashable α
β : Type v
m : Raw α fun x => β
h : m.WF
k : α
v : β
⊢ (Raw₀.Const.insertMany ⟨m, ⋯⟩ [(k, v)]).val.val = (Raw₀.insert ⟨m, ⋯⟩ k v).val
-- Mathlib/Topology/Bornology/Basic.lean
theorem isBounded_union : IsBounded (s ∪ t) ↔ IsBounded s ∧ IsBounded t

Proof state:
α : Type u_2
x✝ : Bornology α
s t : Set α
⊢ IsBounded (s ∪ t) ↔ IsBounded s ∧ IsBounded t

Tactic:
simp only [← isCobounded_compl_iff, compl_union, isCobounded_inter]

Result:
no goals
-- Mathlib/Probability/Martingale/Upcrossing.lean
theorem Submartingale.sum_sub_upcrossingStrat_mul [IsFiniteMeasure μ] (hf : Submartingale f ℱ μ)
    (a b : ℝ) (N : ℕ) : Submartingale (fun n : ℕ =>
      ∑ k ∈ Finset.range n, (1 - upcrossingStrat a b f N k) * (f (k + 1) - f k)) ℱ μ

Proof state:
case refine_1
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
f : ℕ → Ω → ℝ
ℱ : Filtration ℕ m0
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
a b : ℝ
N : ℕ
⊢ ∀ (n : ℕ) (ω : Ω), (1 - upcrossingStrat a b f N n) ω ≤ 1

Tactic:
exact fun n ω => sub_le_self _ upcrossingStrat_nonneg

Result:
no goals

Proof state:
case refine_2
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
f : ℕ → Ω → ℝ
ℱ : Filtration ℕ m0
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
a b : ℝ
N : ℕ
⊢ ∀ (n : ℕ) (ω : Ω), 0 ≤ (1 - upcrossingStrat a b f N n) ω

Tactic:
intro n ω

Result:
case refine_2
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
f : ℕ → Ω → ℝ
ℱ : Filtration ℕ m0
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
a b : ℝ
N n : ℕ
ω : Ω
⊢ 0 ≤ (1 - upcrossingStrat a b f N n) ω

Proof state:
case refine_2
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
f : ℕ → Ω → ℝ
ℱ : Filtration ℕ m0
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
a b : ℝ
N n : ℕ
ω : Ω
⊢ 0 ≤ (1 - upcrossingStrat a b f N n) ω

Tactic:
simp [upcrossingStrat_le_one]

Result:
no goals

Proof state:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
f : ℕ → Ω → ℝ
ℱ : Filtration ℕ m0
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
a b : ℝ
N : ℕ
⊢ Submartingale (fun n => ∑ k ∈ Finset.range n, (1 - upcrossingStrat a b f N k) * (f (k + 1) - f k)) ℱ μ

Tactic:
refine hf.sum_mul_sub (fun n => (adapted_const ℱ 1 n).sub (hf.adapted.upcrossingStrat_adapted n))
  (?_ : ∀ n ω, (1 - upcrossingStrat a b f N n) ω ≤ 1) ?_

Result:
case refine_1
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
f : ℕ → Ω → ℝ
ℱ : Filtration ℕ m0
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
a b : ℝ
N : ℕ
⊢ ∀ (n : ℕ) (ω : Ω), (1 - upcrossingStrat a b f N n) ω ≤ 1

case refine_2
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
f : ℕ → Ω → ℝ
ℱ : Filtration ℕ m0
inst✝ : IsFiniteMeasure μ
hf : Submartingale f ℱ μ
a b : ℝ
N : ℕ
⊢ ∀ (n : ℕ) (ω : Ω), 0 ≤ (1 - upcrossingStrat a b f N n) ω
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Bool.lean
theorem bne_self_left  : ∀(a b : Bool), (a != (a != b)) = b

Proof state:
⊢ ∀ (a b : Bool), (a != (a != b)) = b

Tactic:
decide

Result:
no goals
-- Mathlib/Data/Sym/Basic.lean
theorem map_map {α β γ : Type*} {n : ℕ} (g : β → γ) (f : α → β) (s : Sym α n) :
    Sym.map g (Sym.map f s) = Sym.map (g ∘ f) s :=
  Subtype.ext <| by dsimp only [Sym.map]; simp

Proof state:
α : Type u_3
β : Type u_4
γ : Type u_5
n : ℕ
g : β → γ
f : α → β
s : Sym α n
⊢ Multiset.map g (Multiset.map f ↑s) = Multiset.map (g ∘ f) ↑s

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_3
β : Type u_4
γ : Type u_5
n : ℕ
g : β → γ
f : α → β
s : Sym α n
⊢ ↑(map g (map f s)) = ↑(map (g ∘ f) s)

Tactic:
dsimp only [Sym.map]

Result:
α : Type u_3
β : Type u_4
γ : Type u_5
n : ℕ
g : β → γ
f : α → β
s : Sym α n
⊢ Multiset.map g (Multiset.map f ↑s) = Multiset.map (g ∘ f) ↑s
-- Mathlib/AlgebraicGeometry/EllipticCurve/Group.lean
lemma toClass_injective : Function.Injective <| @toClass _ _ W

Proof state:
F : Type u
inst✝ : Field F
W : Affine F
⊢ Function.Injective ⇑toClass

Tactic:
rintro (_ | h) _ hP

Result:
case zero
F : Type u
inst✝ : Field F
W : Affine F
a₂✝ : W.Point
hP : toClass zero = toClass a₂✝
⊢ zero = a₂✝

case some
F : Type u
inst✝ : Field F
W : Affine F
x✝ y✝ : F
h : W.Nonsingular x✝ y✝
a₂✝ : W.Point
hP : toClass (some h) = toClass a₂✝
⊢ some h = a₂✝

Proof state:
case zero
F : Type u
inst✝ : Field F
W : Affine F
a₂✝ : W.Point
hP : toClass zero = toClass a₂✝
⊢ toClass (-zero) + toClass zero = 0

Tactic:
exact zero_add 0

Result:
no goals

Proof state:
case some
F : Type u
inst✝ : Field F
W : Affine F
x✝ y✝ : F
h : W.Nonsingular x✝ y✝
a₂✝ : W.Point
hP : toClass (some h) = toClass a₂✝
⊢ some h = a₂✝

Tactic:
rw [← neg_inj, ← add_eq_zero, ← toClass_eq_zero, map_add, ← hP]

Result:
case some
F : Type u
inst✝ : Field F
W : Affine F
x✝ y✝ : F
h : W.Nonsingular x✝ y✝
a₂✝ : W.Point
hP : toClass (some h) = toClass a₂✝
⊢ toClass (-some h) + toClass (some h) = 0

Proof state:
case some
F : Type u
inst✝ : Field F
W : Affine F
x✝ y✝ : F
h : W.Nonsingular x✝ y✝
a₂✝ : W.Point
hP : toClass (some h) = toClass a₂✝
⊢ toClass (-some h) + toClass (some h) = 0

Tactic:
exact CoordinateRing.mk_XYIdeal'_mul_mk_XYIdeal'_of_Yeq h

Result:
no goals

Proof state:
case zero
F : Type u
inst✝ : Field F
W : Affine F
a₂✝ : W.Point
hP : toClass zero = toClass a₂✝
⊢ zero = a₂✝

case some
F : Type u
inst✝ : Field F
W : Affine F
x✝ y✝ : F
h : W.Nonsingular x✝ y✝
a₂✝ : W.Point
hP : toClass (some h) = toClass a₂✝
⊢ some h = a₂✝

Tactic:
all_goals rw [← neg_inj, ← add_eq_zero, ← toClass_eq_zero, map_add, ← hP]

Result:
case zero
F : Type u
inst✝ : Field F
W : Affine F
a₂✝ : W.Point
hP : toClass zero = toClass a₂✝
⊢ toClass (-zero) + toClass zero = 0

case some
F : Type u
inst✝ : Field F
W : Affine F
x✝ y✝ : F
h : W.Nonsingular x✝ y✝
a₂✝ : W.Point
hP : toClass (some h) = toClass a₂✝
⊢ toClass (-some h) + toClass (some h) = 0
-- Mathlib/Topology/Algebra/InfiniteSum/Group.lean
theorem hasProd_ite_div_hasProd [DecidableEq β] (hf : HasProd f a) (b : β) :
    HasProd (fun n ↦ ite (n = b) 1 (f n)) (a / f b)

Proof state:
case h.e'_5
α : Type u_1
β : Type u_2
inst✝³ : CommGroup α
inst✝² : TopologicalSpace α
inst✝¹ : IsTopologicalGroup α
f : β → α
a : α
inst✝ : DecidableEq β
hf : HasProd f a
b : β
⊢ (fun n => if n = b then 1 else f n) = update f b 1

Tactic:
ext n

Result:
case h.e'_5.h
α : Type u_1
β : Type u_2
inst✝³ : CommGroup α
inst✝² : TopologicalSpace α
inst✝¹ : IsTopologicalGroup α
f : β → α
a : α
inst✝ : DecidableEq β
hf : HasProd f a
b n : β
⊢ (if n = b then 1 else f n) = update f b 1 n

Proof state:
case h.e'_6
α : Type u_1
β : Type u_2
inst✝³ : CommGroup α
inst✝² : TopologicalSpace α
inst✝¹ : IsTopologicalGroup α
f : β → α
a : α
inst✝ : DecidableEq β
hf : HasProd f a
b : β
⊢ a / f b = 1 / f b * a

Tactic:
rw [div_mul_eq_mul_div, one_mul]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
inst✝³ : CommGroup α
inst✝² : TopologicalSpace α
inst✝¹ : IsTopologicalGroup α
f : β → α
a : α
inst✝ : DecidableEq β
hf : HasProd f a
b : β
⊢ HasProd (fun n => if n = b then 1 else f n) (a / f b)

Tactic:
convert hf.update b 1 using 1

Result:
case h.e'_5
α : Type u_1
β : Type u_2
inst✝³ : CommGroup α
inst✝² : TopologicalSpace α
inst✝¹ : IsTopologicalGroup α
f : β → α
a : α
inst✝ : DecidableEq β
hf : HasProd f a
b : β
⊢ (fun n => if n = b then 1 else f n) = update f b 1

case h.e'_6
α : Type u_1
β : Type u_2
inst✝³ : CommGroup α
inst✝² : TopologicalSpace α
inst✝¹ : IsTopologicalGroup α
f : β → α
a : α
inst✝ : DecidableEq β
hf : HasProd f a
b : β
⊢ a / f b = 1 / f b * a

Proof state:
case h.e'_5.h
α : Type u_1
β : Type u_2
inst✝³ : CommGroup α
inst✝² : TopologicalSpace α
inst✝¹ : IsTopologicalGroup α
f : β → α
a : α
inst✝ : DecidableEq β
hf : HasProd f a
b n : β
⊢ (if n = b then 1 else f n) = update f b 1 n

Tactic:
rw [Function.update_apply]

Result:
no goals
-- Mathlib/RingTheory/Regular/RegularSequence.lean
lemma nil [Nontrivial M] : IsRegular M ([] : List R) where
  toIsWeaklyRegular := IsWeaklyRegular.nil R M
  top_ne_smul h

Proof state:
R : Type u_1
M : Type u_3
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Nontrivial M
h : ⊤ = Ideal.ofList [] • ⊤
⊢ False

Tactic:
rw [Ideal.ofList_nil, bot_smul, eq_comm, subsingleton_iff_bot_eq_top] at h

Result:
R : Type u_1
M : Type u_3
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Nontrivial M
h : Subsingleton (Submodule R M)
⊢ False

Proof state:
R : Type u_1
M : Type u_3
inst✝³ : CommRing R
inst✝² : AddCommGroup M
inst✝¹ : Module R M
inst✝ : Nontrivial M
h : Subsingleton (Submodule R M)
⊢ False

Tactic:
exact not_subsingleton M ((Submodule.subsingleton_iff _).mp h)

Result:
no goals
-- Mathlib/CategoryTheory/Iso.lean
theorem isIso_of_hom_comp_eq_id (g : X ⟶ Y) [IsIso g] {f : Y ⟶ X} (h : g ≫ f = 𝟙 X) : IsIso f

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
g : X ⟶ Y
inst✝ : IsIso g
f : Y ⟶ X
h : g ≫ f = 𝟙 X
⊢ IsIso f

Tactic:
rw [(hom_comp_eq_id _).mp h]

Result:
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
g : X ⟶ Y
inst✝ : IsIso g
f : Y ⟶ X
h : g ≫ f = 𝟙 X
⊢ IsIso (inv g)

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
g : X ⟶ Y
inst✝ : IsIso g
f : Y ⟶ X
h : g ≫ f = 𝟙 X
⊢ IsIso (inv g)

Tactic:
infer_instance

Result:
no goals
-- Mathlib/Topology/AlexandrovDiscrete.lean
lemma alexandrovDiscrete_coinduced {β : Type*} {f : α → β} :
    @AlexandrovDiscrete β (coinduced f ‹_›) :=
  @AlexandrovDiscrete.mk β (coinduced f ‹_›) fun S hS ↦ by
    rw [isOpen_coinduced, preimage_sInter]; exact isOpen_iInter₂ hS

Proof state:
α : Type u_3
inst✝¹ : TopologicalSpace α
inst✝ : AlexandrovDiscrete α
β : Type u_5
f : α → β
S : Set (Set β)
hS : ∀ s ∈ S, IsOpen s
⊢ IsOpen (⋂₀ S)

Tactic:
rw [isOpen_coinduced, preimage_sInter]

Result:
α : Type u_3
inst✝¹ : TopologicalSpace α
inst✝ : AlexandrovDiscrete α
β : Type u_5
f : α → β
S : Set (Set β)
hS : ∀ s ∈ S, IsOpen s
⊢ IsOpen (⋂ t ∈ S, f ⁻¹' t)

Proof state:
α : Type u_3
inst✝¹ : TopologicalSpace α
inst✝ : AlexandrovDiscrete α
β : Type u_5
f : α → β
S : Set (Set β)
hS : ∀ s ∈ S, IsOpen s
⊢ IsOpen (⋂ t ∈ S, f ⁻¹' t)

Tactic:
exact isOpen_iInter₂ hS

Result:
no goals