harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/CategoryTheory/Subpresheaf/Image.lean
@[simp]
lemma range_toRange : range (toRange p) = ⊤

Proof state:
case obj.h.h.mk
C : Type u
inst✝ : Category.{v, u} C
F F' : Cᵒᵖ ⥤ Type w
p : F' ⟶ F
i : Cᵒᵖ
x : F.obj i
hx : x ∈ (range p).obj i
⊢ ⟨x, hx⟩ ∈ (range (toRange p)).obj i ↔ ⟨x, hx⟩ ∈ ⊤.obj i

Tactic:
dsimp at hx ⊢

Result:
case obj.h.h.mk
C : Type u
inst✝ : Category.{v, u} C
F F' : Cᵒᵖ ⥤ Type w
p : F' ⟶ F
i : Cᵒᵖ
x : F.obj i
hx : x ∈ Set.range (p.app i)
⊢ ⟨x, hx⟩ ∈ Set.range ((toRange p).app i) ↔ ⟨x, hx⟩ ∈ Set.univ

Proof state:
case obj.h.h.mk
C : Type u
inst✝ : Category.{v, u} C
F F' : Cᵒᵖ ⥤ Type w
p : F' ⟶ F
i : Cᵒᵖ
x : F.obj i
hx : x ∈ Set.range (p.app i)
⊢ ⟨x, hx⟩ ∈ Set.range ((toRange p).app i) ↔ ⟨x, hx⟩ ∈ Set.univ

Tactic:
simp only [Set.mem_range, Set.mem_univ, iff_true]

Result:
case obj.h.h.mk
C : Type u
inst✝ : Category.{v, u} C
F F' : Cᵒᵖ ⥤ Type w
p : F' ⟶ F
i : Cᵒᵖ
x : F.obj i
hx : x ∈ Set.range (p.app i)
⊢ ∃ y, (toRange p).app i y = ⟨x, hx⟩

Proof state:
case obj.h.h.mk
C : Type u
inst✝ : Category.{v, u} C
F F' : Cᵒᵖ ⥤ Type w
p : F' ⟶ F
i : Cᵒᵖ
x : F.obj i
hx : x ∈ Set.range (p.app i)
⊢ ∃ y, (toRange p).app i y = ⟨x, hx⟩

Tactic:
simp only [Set.mem_range] at hx

Result:
case obj.h.h.mk
C : Type u
inst✝ : Category.{v, u} C
F F' : Cᵒᵖ ⥤ Type w
p : F' ⟶ F
i : Cᵒᵖ
x : F.obj i
hx✝ : x ∈ Set.range (p.app i)
hx : ∃ y, p.app i y = x
⊢ ∃ y, (toRange p).app i y = ⟨x, hx✝⟩

Proof state:
case obj.h.h.mk.intro
C : Type u
inst✝ : Category.{v, u} C
F F' : Cᵒᵖ ⥤ Type w
p : F' ⟶ F
i : Cᵒᵖ
y : F'.obj i
hx : p.app i y ∈ Set.range (p.app i)
⊢ ∃ y_1, (toRange p).app i y_1 = ⟨p.app i y, hx⟩

Tactic:
exact ⟨y, rfl⟩

Result:
no goals

Proof state:
case obj.h.h.mk
C : Type u
inst✝ : Category.{v, u} C
F F' : Cᵒᵖ ⥤ Type w
p : F' ⟶ F
i : Cᵒᵖ
x : F.obj i
hx✝ : x ∈ Set.range (p.app i)
hx : ∃ y, p.app i y = x
⊢ ∃ y, (toRange p).app i y = ⟨x, hx✝⟩

Tactic:
obtain ⟨y, rfl⟩ := hx

Result:
case obj.h.h.mk.intro
C : Type u
inst✝ : Category.{v, u} C
F F' : Cᵒᵖ ⥤ Type w
p : F' ⟶ F
i : Cᵒᵖ
y : F'.obj i
hx : p.app i y ∈ Set.range (p.app i)
⊢ ∃ y_1, (toRange p).app i y_1 = ⟨p.app i y, hx⟩

Proof state:
C : Type u
inst✝ : Category.{v, u} C
F F' : Cᵒᵖ ⥤ Type w
p : F' ⟶ F
⊢ range (toRange p) = ⊤

Tactic:
ext i ⟨x, hx⟩

Result:
case obj.h.h.mk
C : Type u
inst✝ : Category.{v, u} C
F F' : Cᵒᵖ ⥤ Type w
p : F' ⟶ F
i : Cᵒᵖ
x : F.obj i
hx : x ∈ (range p).obj i
⊢ ⟨x, hx⟩ ∈ (range (toRange p)).obj i ↔ ⟨x, hx⟩ ∈ ⊤.obj i
-- Mathlib/Algebra/Module/NatInt.lean
/-- `nsmul` is equal to any other module structure via a cast. -/
@[norm_cast]
lemma Nat.cast_smul_eq_nsmul (n : ℕ) (b : M) : (n : R) • b = n • b

Proof state:
case succ
R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : M
n : ℕ
ih : ↑n • b = n • b
⊢ ↑(n + 1) • b = (n + 1) • b

Tactic:
rw [Nat.cast_succ, add_smul, add_smul, one_smul, ih, one_smul]

Result:
no goals

Proof state:
R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
n : ℕ
b : M
⊢ ↑n • b = n • b

Tactic:
induction n with
| zero => rw [Nat.cast_zero, zero_smul, zero_smul]
| succ n ih => rw [Nat.cast_succ, add_smul, add_smul, one_smul, ih, one_smul]

Result:
no goals

Proof state:
case zero
R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
b : M
⊢ ↑0 • b = 0 • b

Tactic:
rw [Nat.cast_zero, zero_smul, zero_smul]

Result:
no goals
-- Mathlib/Data/Sym/Sym2.lean
theorem mem_iff' {a b c : α} : Sym2.Mem a s(b, c) ↔ a = b ∨ a = c :=
  { mp

Proof state:
case inr
α : Type u_1
a b : α
⊢ Sym2.Mem a s(a, b)

Tactic:
exact ⟨_, rfl⟩

Result:
no goals

Proof state:
case intro
α : Type u_1
a b c w✝ : α
h : s(b, c) = s(a, w✝)
⊢ a = b ∨ a = c

Tactic:
rw [eq_iff] at h

Result:
case intro
α : Type u_1
a b c w✝ : α
h : b = a ∧ c = w✝ ∨ b = w✝ ∧ c = a
⊢ a = b ∨ a = c

Proof state:
case intro
α : Type u_1
a b c w✝ : α
h : b = a ∧ c = w✝ ∨ b = w✝ ∧ c = a
⊢ a = b ∨ a = c

Tactic:
aesop

Result:
no goals

Proof state:
α : Type u_1
a b c : α
⊢ a = b ∨ a = c → Sym2.Mem a s(b, c)

Tactic:
rintro (rfl | rfl)

Result:
case inl
α : Type u_1
a c : α
⊢ Sym2.Mem a s(a, c)

case inr
α : Type u_1
a b : α
⊢ Sym2.Mem a s(b, a)

Proof state:
case inl
α : Type u_1
a c : α
⊢ Sym2.Mem a s(a, c)

Tactic:
exact ⟨_, rfl⟩

Result:
no goals

Proof state:
α : Type u_1
a b c : α
⊢ Sym2.Mem a s(b, c) → a = b ∨ a = c

Tactic:
rintro ⟨_, h⟩

Result:
case intro
α : Type u_1
a b c w✝ : α
h : s(b, c) = s(a, w✝)
⊢ a = b ∨ a = c

Proof state:
case inr
α : Type u_1
a b : α
⊢ Sym2.Mem a s(b, a)

Tactic:
rw [eq_swap]

Result:
case inr
α : Type u_1
a b : α
⊢ Sym2.Mem a s(a, b)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Zip.lean
theorem take_zipWith : (zipWith f l l').take n = zipWith f (l.take n) (l'.take n)

Proof state:
case mk
α✝² : Type u_1
α✝¹ : Type u_2
α✝ : Type u_3
f : α✝² → α✝¹ → α✝
n : Nat
l : Array α✝²
l' : Vector α✝¹ l.size
⊢ (zipWith f { toArray := l, size_toArray := ⋯ } l').take n =
    zipWith f ({ toArray := l, size_toArray := ⋯ }.take n) (l'.take n)

Tactic:
rcases l' with ⟨l', h⟩

Result:
case mk.mk
α✝² : Type u_1
α✝¹ : Type u_2
α✝ : Type u_3
f : α✝² → α✝¹ → α✝
n : Nat
l : Array α✝²
l' : Array α✝¹
h : l'.size = l.size
⊢ (zipWith f { toArray := l, size_toArray := ⋯ } { toArray := l', size_toArray := h }).take n =
    zipWith f ({ toArray := l, size_toArray := ⋯ }.take n) ({ toArray := l', size_toArray := h }.take n)

Proof state:
α✝² : Type u_1
α✝¹ : Type u_2
α✝ : Type u_3
f : α✝² → α✝¹ → α✝
n✝ : Nat
l : Vector α✝² n✝
l' : Vector α✝¹ n✝
n : Nat
⊢ (zipWith f l l').take n = zipWith f (l.take n) (l'.take n)

Tactic:
rcases l with ⟨l, rfl⟩

Result:
case mk
α✝² : Type u_1
α✝¹ : Type u_2
α✝ : Type u_3
f : α✝² → α✝¹ → α✝
n : Nat
l : Array α✝²
l' : Vector α✝¹ l.size
⊢ (zipWith f { toArray := l, size_toArray := ⋯ } l').take n =
    zipWith f ({ toArray := l, size_toArray := ⋯ }.take n) (l'.take n)

Proof state:
case mk.mk
α✝² : Type u_1
α✝¹ : Type u_2
α✝ : Type u_3
f : α✝² → α✝¹ → α✝
n : Nat
l : Array α✝²
l' : Array α✝¹
h : l'.size = l.size
⊢ (zipWith f { toArray := l, size_toArray := ⋯ } { toArray := l', size_toArray := h }).take n =
    zipWith f ({ toArray := l, size_toArray := ⋯ }.take n) ({ toArray := l', size_toArray := h }.take n)

Tactic:
simp [Array.take_zipWith]

Result:
no goals
-- Mathlib/Analysis/Calculus/ContDiff/FaaDiBruno.lean
lemma emb_zero [NeZero n] : c.emb (c.index 0) 0 = 0

Proof state:
n : ℕ
c : OrderedFinpartition n
inst✝ : NeZero n
⊢ c.emb (c.index 0) 0 = 0

Tactic:
apply le_antisymm _ (Fin.zero_le' _)

Result:
n : ℕ
c : OrderedFinpartition n
inst✝ : NeZero n
⊢ c.emb (c.index 0) 0 ≤ 0

Proof state:
n : ℕ
c : OrderedFinpartition n
inst✝ : NeZero n
⊢ c.emb (c.index 0) 0 ≤ 0

Tactic:
conv_rhs => rw [← c.emb_invEmbedding 0]

Result:
n : ℕ
c : OrderedFinpartition n
inst✝ : NeZero n
⊢ c.emb (c.index 0) 0 ≤ c.emb (c.index 0) (c.invEmbedding 0)

Proof state:
n : ℕ
c : OrderedFinpartition n
inst✝ : NeZero n
⊢ c.emb (c.index 0) 0 ≤ c.emb (c.index 0) (c.invEmbedding 0)

Tactic:
apply (c.emb_strictMono _).monotone (Fin.zero_le' _)

Result:
no goals
-- Mathlib/CategoryTheory/EqToHom.lean
theorem congr_inv_of_congr_hom (F G : C ⥤ D) {X Y : C} (e : X ≅ Y) (hX : F.obj X = G.obj X)
    (hY : F.obj Y = G.obj Y)
    (h₂ : F.map e.hom = eqToHom (by rw [hX]) ≫ G.map e.hom ≫ eqToHom (by rw [hY])) :
    F.map e.inv = eqToHom (by rw [hY]) ≫ G.map e.inv ≫ eqToHom (by rw [hX])

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : C ⥤ D
X Y : C
e : X ≅ Y
hX : F.obj X = G.obj X
hY : F.obj Y = G.obj Y
h₂ : F.map e.hom = eqToHom ⋯ ≫ G.map e.hom ≫ eqToHom ⋯
⊢ F.map e.inv = eqToHom ⋯ ≫ G.map e.inv ≫ eqToHom ⋯

Tactic:
simp only [← IsIso.Iso.inv_hom e, Functor.map_inv, h₂, IsIso.inv_comp, inv_eqToHom,
  Category.assoc]

Result:
no goals

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
β : Sort u_1
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : C ⥤ D
X Y : C
e : X ≅ Y
hX : F.obj X = G.obj X
hY : F.obj Y = G.obj Y
⊢ G.obj Y = F.obj Y

Tactic:
rw [hY]

Result:
no goals

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
β : Sort u_1
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : C ⥤ D
X Y : C
e : X ≅ Y
hX : F.obj X = G.obj X
hY : F.obj Y = G.obj Y
h₂ : F.map e.hom = eqToHom ⋯ ≫ G.map e.hom ≫ eqToHom ⋯
⊢ G.obj X = F.obj X

Tactic:
rw [hX]

Result:
no goals

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
β : Sort u_1
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : C ⥤ D
X Y : C
e : X ≅ Y
hX : F.obj X = G.obj X
hY : F.obj Y = G.obj Y
h₂ : F.map e.hom = eqToHom ⋯ ≫ G.map e.hom ≫ eqToHom ⋯
⊢ F.obj Y = G.obj Y

Tactic:
rw [hY]

Result:
no goals

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
β : Sort u_1
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G : C ⥤ D
X Y : C
e : X ≅ Y
hX : F.obj X = G.obj X
hY : F.obj Y = G.obj Y
⊢ F.obj X = G.obj X

Tactic:
rw [hX]

Result:
no goals
-- Mathlib/Analysis/MeanInequalities.lean
theorem inner_le_Lp_mul_Lp_of_norm_eq_zero (f g : ι → ℝ≥0) {p q : ℝ}
    (hpq : p.IsConjExponent q) (hf : ∑ i ∈ s, f i ^ p = 0) :
    ∑ i ∈ s, f i * g i ≤ (∑ i ∈ s, f i ^ p) ^ (1 / p) * (∑ i ∈ s, g i ^ q) ^ (1 / q)

Proof state:
case h
ι : Type u
s : Finset ι
f g : ι → ℝ≥0
p q : ℝ
hpq : p.IsConjExponent q
hf : ∑ i ∈ s, f i ^ p = 0
i : ι
his : i ∈ s
⊢ f i = 0

Tactic:
rw [sum_eq_zero_iff] at hf

Result:
case h
ι : Type u
s : Finset ι
f g : ι → ℝ≥0
p q : ℝ
hpq : p.IsConjExponent q
hf : ∀ x ∈ s, f x ^ p = 0
i : ι
his : i ∈ s
⊢ f i = 0

Proof state:
ι : Type u
s : Finset ι
f g : ι → ℝ≥0
p q : ℝ
hpq : p.IsConjExponent q
hf : ∑ i ∈ s, f i ^ p = 0
i : ι
his : i ∈ s
⊢ f i = 0 ∨ g i = 0

Tactic:
left

Result:
case h
ι : Type u
s : Finset ι
f g : ι → ℝ≥0
p q : ℝ
hpq : p.IsConjExponent q
hf : ∑ i ∈ s, f i ^ p = 0
i : ι
his : i ∈ s
⊢ f i = 0

Proof state:
ι : Type u
s : Finset ι
f g : ι → ℝ≥0
p q : ℝ
hpq : p.IsConjExponent q
hf : ∑ i ∈ s, f i ^ p = 0
⊢ ∑ i ∈ s, f i * g i ≤ (∑ i ∈ s, f i ^ p) ^ (1 / p) * (∑ i ∈ s, g i ^ q) ^ (1 / q)

Tactic:
simp only [hf, hpq.ne_zero, one_div, sum_eq_zero_iff, zero_rpow, zero_mul,
  inv_eq_zero, Ne, not_false_iff, le_zero_iff, mul_eq_zero]

Result:
ι : Type u
s : Finset ι
f g : ι → ℝ≥0
p q : ℝ
hpq : p.IsConjExponent q
hf : ∑ i ∈ s, f i ^ p = 0
⊢ ∀ x ∈ s, f x = 0 ∨ g x = 0

Proof state:
ι : Type u
s : Finset ι
f g : ι → ℝ≥0
p q : ℝ
hpq : p.IsConjExponent q
hf : ∑ i ∈ s, f i ^ p = 0
⊢ ∀ x ∈ s, f x = 0 ∨ g x = 0

Tactic:
intro i his

Result:
ι : Type u
s : Finset ι
f g : ι → ℝ≥0
p q : ℝ
hpq : p.IsConjExponent q
hf : ∑ i ∈ s, f i ^ p = 0
i : ι
his : i ∈ s
⊢ f i = 0 ∨ g i = 0

Proof state:
case h
ι : Type u
s : Finset ι
f g : ι → ℝ≥0
p q : ℝ
hpq : p.IsConjExponent q
hf : ∀ x ∈ s, f x ^ p = 0
i : ι
his : i ∈ s
⊢ f i = 0

Tactic:
exact (rpow_eq_zero_iff.mp (hf i his)).left

Result:
no goals
-- Mathlib/NumberTheory/ArithmeticFunction.lean
theorem pow_apply {k n : ℕ} : pow k n = if k = 0 ∧ n = 0 then 0 else n ^ k

Proof state:
k n : ℕ
⊢ (pow k) n = if k = 0 ∧ n = 0 then 0 else n ^ k

Tactic:
cases k <;> simp [pow]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem mem_of_getElem {l : Array α} {i : Nat} {h} {a : α} (e : l[i] = a) : a ∈ l

Proof state:
α : Type u_1
l : Array α
i : Nat
h : i < l.size
a : α
e : l[i] = a
⊢ a ∈ l

Tactic:
subst e

Result:
α : Type u_1
l : Array α
i : Nat
h : i < l.size
⊢ l[i] ∈ l

Proof state:
α : Type u_1
l : Array α
i : Nat
h : i < l.size
⊢ l[i] ∈ l

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Zip.lean
theorem map_prod_right_eq_zip {l : List α} (f : α → β) :
    (l.map fun x => (f x, x)) = (l.map f).zip l

Proof state:
α : Type u_1
β : Type u_2
l : List α
f : α → β
⊢ (map f l).zip (map (fun x => x) l) = (map f l).zip l

Tactic:
congr

Result:
case e_a
α : Type u_1
β : Type u_2
l : List α
f : α → β
⊢ map (fun x => x) l = l

Proof state:
α : Type u_1
β : Type u_2
l : List α
f : α → β
⊢ map (fun x => (f x, x)) l = (map f l).zip l

Tactic:
rw [← zip_map']

Result:
α : Type u_1
β : Type u_2
l : List α
f : α → β
⊢ (map f l).zip (map (fun x => x) l) = (map f l).zip l

Proof state:
case e_a
α : Type u_1
β : Type u_2
l : List α
f : α → β
⊢ map (fun x => x) l = l

Tactic:
simp

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/NormalForms.lean
theorem b₆_of_isCharNeTwoNF : W.b₆ = 4 * W.a₆

Proof state:
R : Type u_1
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : W.IsCharNeTwoNF
⊢ 0 ^ 2 + 4 * W.a₆ = 4 * W.a₆

Tactic:
ring1

Result:
no goals

Proof state:
R : Type u_1
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : W.IsCharNeTwoNF
⊢ W.b₆ = 4 * W.a₆

Tactic:
rw [b₆, a₃_of_isCharNeTwoNF]

Result:
R : Type u_1
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : W.IsCharNeTwoNF
⊢ 0 ^ 2 + 4 * W.a₆ = 4 * W.a₆
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem toNat_mod_cancel' {x : BitVec n} :
    (x.toNat : Int) % (((2 ^ n) : Nat) : Int) = x.toNat

Proof state:
n : Nat
x : BitVec n
⊢ ↑x.toNat % ↑(2 ^ n) = ↑x.toNat

Tactic:
rw_mod_cast [toNat_mod_cancel]

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/TwoDim.lean
theorem kahler_swap (x y : E) : o.kahler x y = conj (o.kahler y x)

Proof state:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
⊢ ↑(inner y x) + -(o.areaForm y) x • Complex.I = (starRingEnd ℂ) (↑(inner y x) + (o.areaForm y) x • Complex.I)

Tactic:
simp [Complex.conj_ofReal]

Result:
no goals

Proof state:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
⊢ (o.kahler x) y = (starRingEnd ℂ) ((o.kahler y) x)

Tactic:
simp only [kahler_apply_apply]

Result:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
⊢ ↑(inner x y) + (o.areaForm x) y • Complex.I = (starRingEnd ℂ) (↑(inner y x) + (o.areaForm y) x • Complex.I)

Proof state:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
⊢ ↑(inner x y) + (o.areaForm x) y • Complex.I = (starRingEnd ℂ) (↑(inner y x) + (o.areaForm y) x • Complex.I)

Tactic:
rw [real_inner_comm, areaForm_swap]

Result:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace ℝ E
inst✝ : Fact (finrank ℝ E = 2)
o : Orientation ℝ E (Fin 2)
x y : E
⊢ ↑(inner y x) + -(o.areaForm y) x • Complex.I = (starRingEnd ℂ) (↑(inner y x) + (o.areaForm y) x • Complex.I)
-- Mathlib/Data/Nat/Digits.lean
theorem nine_dvd_iff (n : ℕ) : 9 ∣ n ↔ 9 ∣ (digits 10 n).sum :=
  dvd_iff_dvd_digits_sum 9 10 (by norm_num) n

Proof state:
n : ℕ
⊢ 10 % 9 = 1

Tactic:
norm_num

Result:
no goals
-- Mathlib/Probability/Martingale/Basic.lean
theorem martingale_of_condExp_sub_eq_zero_nat [IsFiniteMeasure μ] {f : ℕ → Ω → ℝ}
    (hadp : Adapted 𝒢 f) (hint : ∀ i, Integrable (f i) μ)
    (hf : ∀ i, μ[f (i + 1) - f i|𝒢 i] =ᵐ[μ] 0) : Martingale f 𝒢 μ

Proof state:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
inst✝ : IsFiniteMeasure μ
f : ℕ → Ω → ℝ
hadp : Adapted 𝒢 f
hint : ∀ (i : ℕ), Integrable (f i) μ
hf : ∀ (i : ℕ), μ[f (i + 1) - f i|↑𝒢 i] =ᶠ[ae μ] 0
i : ℕ
⊢ 0 =ᶠ[ae μ] -μ[f (i + 1) - f i|↑𝒢 i]

Tactic:
filter_upwards [hf i] with x hx

Result:
case h
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
inst✝ : IsFiniteMeasure μ
f : ℕ → Ω → ℝ
hadp : Adapted 𝒢 f
hint : ∀ (i : ℕ), Integrable (f i) μ
hf : ∀ (i : ℕ), μ[f (i + 1) - f i|↑𝒢 i] =ᶠ[ae μ] 0
i : ℕ
x : Ω
hx : (μ[f (i + 1) - f i|↑𝒢 i]) x = 0 x
⊢ 0 x = (-μ[f (i + 1) - f i|↑𝒢 i]) x

Proof state:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
inst✝ : IsFiniteMeasure μ
f : ℕ → Ω → ℝ
hadp : Adapted 𝒢 f
hint : ∀ (i : ℕ), Integrable (f i) μ
hf : ∀ (i : ℕ), μ[f (i + 1) - f i|↑𝒢 i] =ᶠ[ae μ] 0
⊢ Martingale f 𝒢 μ

Tactic:
refine martingale_iff.2 ⟨supermartingale_of_condExp_sub_nonneg_nat hadp hint fun i => ?_,
  submartingale_of_condExp_sub_nonneg_nat hadp hint fun i => (hf i).symm.le⟩

Result:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
inst✝ : IsFiniteMeasure μ
f : ℕ → Ω → ℝ
hadp : Adapted 𝒢 f
hint : ∀ (i : ℕ), Integrable (f i) μ
hf : ∀ (i : ℕ), μ[f (i + 1) - f i|↑𝒢 i] =ᶠ[ae μ] 0
i : ℕ
⊢ 0 ≤ᶠ[ae μ] μ[f i - f (i + 1)|↑𝒢 i]

Proof state:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
inst✝ : IsFiniteMeasure μ
f : ℕ → Ω → ℝ
hadp : Adapted 𝒢 f
hint : ∀ (i : ℕ), Integrable (f i) μ
hf : ∀ (i : ℕ), μ[f (i + 1) - f i|↑𝒢 i] =ᶠ[ae μ] 0
i : ℕ
⊢ 0 ≤ᶠ[ae μ] μ[-(f (i + 1) - f i)|↑𝒢 i]

Tactic:
refine (EventuallyEq.trans ?_ (condExp_neg ..).symm).le

Result:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
inst✝ : IsFiniteMeasure μ
f : ℕ → Ω → ℝ
hadp : Adapted 𝒢 f
hint : ∀ (i : ℕ), Integrable (f i) μ
hf : ∀ (i : ℕ), μ[f (i + 1) - f i|↑𝒢 i] =ᶠ[ae μ] 0
i : ℕ
⊢ 0 =ᶠ[ae μ] -μ[f (i + 1) - f i|↑𝒢 i]

Proof state:
case h
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
inst✝ : IsFiniteMeasure μ
f : ℕ → Ω → ℝ
hadp : Adapted 𝒢 f
hint : ∀ (i : ℕ), Integrable (f i) μ
hf : ∀ (i : ℕ), μ[f (i + 1) - f i|↑𝒢 i] =ᶠ[ae μ] 0
i : ℕ
x : Ω
hx : (μ[f (i + 1) - f i|↑𝒢 i]) x = 0 x
⊢ 0 x = (-μ[f (i + 1) - f i|↑𝒢 i]) x

Tactic:
simpa only [Pi.zero_apply, Pi.neg_apply, zero_eq_neg]

Result:
no goals

Proof state:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
inst✝ : IsFiniteMeasure μ
f : ℕ → Ω → ℝ
hadp : Adapted 𝒢 f
hint : ∀ (i : ℕ), Integrable (f i) μ
hf : ∀ (i : ℕ), μ[f (i + 1) - f i|↑𝒢 i] =ᶠ[ae μ] 0
i : ℕ
⊢ 0 ≤ᶠ[ae μ] μ[f i - f (i + 1)|↑𝒢 i]

Tactic:
rw [← neg_sub]

Result:
Ω : Type u_1
m0 : MeasurableSpace Ω
μ : Measure Ω
𝒢 : Filtration ℕ m0
inst✝ : IsFiniteMeasure μ
f : ℕ → Ω → ℝ
hadp : Adapted 𝒢 f
hint : ∀ (i : ℕ), Integrable (f i) μ
hf : ∀ (i : ℕ), μ[f (i + 1) - f i|↑𝒢 i] =ᶠ[ae μ] 0
i : ℕ
⊢ 0 ≤ᶠ[ae μ] μ[-(f (i + 1) - f i)|↑𝒢 i]
-- Mathlib/Topology/Separation/Profinite.lean
theorem totallySeparatedSpace_of_t1_of_basis_clopen [T1Space X]
    (h : IsTopologicalBasis { s : Set X | IsClopen s }) : TotallySeparatedSpace X

Proof state:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
h : IsTopologicalBasis {s | IsClopen s}
⊢ TotallySeparatedSpace X

Tactic:
constructor

Result:
case isTotallySeparated_univ
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
h : IsTopologicalBasis {s | IsClopen s}
⊢ IsTotallySeparated univ

Proof state:
case isTotallySeparated_univ
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
h : IsTopologicalBasis {s | IsClopen s}
x y : X
hxy : x ≠ y
⊢ ∃ u v, IsOpen u ∧ IsOpen v ∧ x ∈ u ∧ y ∈ v ∧ univ ⊆ u ∪ v ∧ Disjoint u v

Tactic:
rcases h.mem_nhds_iff.mp (isOpen_ne.mem_nhds hxy) with ⟨U, hU, hxU, hyU⟩

Result:
case isTotallySeparated_univ.intro.intro.intro
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
h : IsTopologicalBasis {s | IsClopen s}
x y : X
hxy : x ≠ y
U : Set X
hU : U ∈ {s | IsClopen s}
hxU : x ∈ U
hyU : U ⊆ {y_1 | y_1 ≠ y}
⊢ ∃ u v, IsOpen u ∧ IsOpen v ∧ x ∈ u ∧ y ∈ v ∧ univ ⊆ u ∪ v ∧ Disjoint u v

Proof state:
case isTotallySeparated_univ
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
h : IsTopologicalBasis {s | IsClopen s}
⊢ IsTotallySeparated univ

Tactic:
rintro x - y - hxy

Result:
case isTotallySeparated_univ
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
h : IsTopologicalBasis {s | IsClopen s}
x y : X
hxy : x ≠ y
⊢ ∃ u v, IsOpen u ∧ IsOpen v ∧ x ∈ u ∧ y ∈ v ∧ univ ⊆ u ∪ v ∧ Disjoint u v

Proof state:
case isTotallySeparated_univ.intro.intro.intro
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T1Space X
h : IsTopologicalBasis {s | IsClopen s}
x y : X
hxy : x ≠ y
U : Set X
hU : U ∈ {s | IsClopen s}
hxU : x ∈ U
hyU : U ⊆ {y_1 | y_1 ≠ y}
⊢ ∃ u v, IsOpen u ∧ IsOpen v ∧ x ∈ u ∧ y ∈ v ∧ univ ⊆ u ∪ v ∧ Disjoint u v

Tactic:
exact ⟨U, Uᶜ, hU.isOpen, hU.compl.isOpen, hxU, fun h => hyU h rfl, (union_compl_self U).superset,
  disjoint_compl_right⟩

Result:
no goals
-- Mathlib/Geometry/Manifold/LocalInvariantProperties.lean
theorem liftProp_of_locally_liftPropOn (h : ∀ x, ∃ u, IsOpen u ∧ x ∈ u ∧ LiftPropOn P g u) :
    LiftProp P g

Proof state:
H : Type u_1
M : Type u_2
H' : Type u_3
M' : Type u_4
inst✝⁵ : TopologicalSpace H
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : TopologicalSpace H'
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
G : StructureGroupoid H
G' : StructureGroupoid H'
P : (H → H') → Set H → H → Prop
g : M → M'
hG : G.LocalInvariantProp G' P
h : ∀ (x : M), ∃ u, IsOpen u ∧ x ∈ u ∧ LiftPropOn P g u
x : M
x✝ : x ∈ univ
⊢ ∃ u, IsOpen u ∧ x ∈ u ∧ LiftPropOn P g (univ ∩ u)

Tactic:
simp [h x]

Result:
no goals

Proof state:
H : Type u_1
M : Type u_2
H' : Type u_3
M' : Type u_4
inst✝⁵ : TopologicalSpace H
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : TopologicalSpace H'
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
G : StructureGroupoid H
G' : StructureGroupoid H'
P : (H → H') → Set H → H → Prop
g : M → M'
hG : G.LocalInvariantProp G' P
h : ∀ (x : M), ∃ u, IsOpen u ∧ x ∈ u ∧ LiftPropOn P g u
⊢ LiftPropOn P g univ

Tactic:
refine hG.liftPropOn_of_locally_liftPropOn fun x _ ↦ ?_

Result:
H : Type u_1
M : Type u_2
H' : Type u_3
M' : Type u_4
inst✝⁵ : TopologicalSpace H
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : TopologicalSpace H'
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
G : StructureGroupoid H
G' : StructureGroupoid H'
P : (H → H') → Set H → H → Prop
g : M → M'
hG : G.LocalInvariantProp G' P
h : ∀ (x : M), ∃ u, IsOpen u ∧ x ∈ u ∧ LiftPropOn P g u
x : M
x✝ : x ∈ univ
⊢ ∃ u, IsOpen u ∧ x ∈ u ∧ LiftPropOn P g (univ ∩ u)

Proof state:
H : Type u_1
M : Type u_2
H' : Type u_3
M' : Type u_4
inst✝⁵ : TopologicalSpace H
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : TopologicalSpace H'
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
G : StructureGroupoid H
G' : StructureGroupoid H'
P : (H → H') → Set H → H → Prop
g : M → M'
hG : G.LocalInvariantProp G' P
h : ∀ (x : M), ∃ u, IsOpen u ∧ x ∈ u ∧ LiftPropOn P g u
⊢ LiftProp P g

Tactic:
rw [← liftPropOn_univ]

Result:
H : Type u_1
M : Type u_2
H' : Type u_3
M' : Type u_4
inst✝⁵ : TopologicalSpace H
inst✝⁴ : TopologicalSpace M
inst✝³ : ChartedSpace H M
inst✝² : TopologicalSpace H'
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
G : StructureGroupoid H
G' : StructureGroupoid H'
P : (H → H') → Set H → H → Prop
g : M → M'
hG : G.LocalInvariantProp G' P
h : ∀ (x : M), ∃ u, IsOpen u ∧ x ∈ u ∧ LiftPropOn P g u
⊢ LiftPropOn P g univ
-- Mathlib/Analysis/Calculus/LocalExtr/Basic.lean
theorem IsLocalMaxOn.fderivWithin_nonpos (h : IsLocalMaxOn f s a)
    (hy : y ∈ posTangentConeAt s a) : (fderivWithin ℝ f s a : E → ℝ) y ≤ 0

Proof state:
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℝ
s : Set E
a y : E
h : IsLocalMaxOn f s a
hy : y ∈ posTangentConeAt s a
⊢ (fderivWithin ℝ f s a) y ≤ 0

Tactic:
exact
  if hf : DifferentiableWithinAt ℝ f s a then h.hasFDerivWithinAt_nonpos hf.hasFDerivWithinAt hy
  else by rw [fderivWithin_zero_of_not_differentiableWithinAt hf]; rfl

Result:
no goals

Proof state:
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℝ
s : Set E
a y : E
h : IsLocalMaxOn f s a
hy : y ∈ posTangentConeAt s a
hf : ¬DifferentiableWithinAt ℝ f s a
⊢ 0 y ≤ 0

Tactic:
rfl

Result:
no goals

Proof state:
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℝ
s : Set E
a y : E
h : IsLocalMaxOn f s a
hy : y ∈ posTangentConeAt s a
hf : ¬DifferentiableWithinAt ℝ f s a
⊢ (fderivWithin ℝ f s a) y ≤ 0

Tactic:
rw [fderivWithin_zero_of_not_differentiableWithinAt hf]

Result:
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℝ
s : Set E
a y : E
h : IsLocalMaxOn f s a
hy : y ∈ posTangentConeAt s a
hf : ¬DifferentiableWithinAt ℝ f s a
⊢ 0 y ≤ 0

Proof state:
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : E → ℝ
s : Set E
a y : E
h : IsLocalMaxOn f s a
hy : y ∈ posTangentConeAt s a
⊢ (fderivWithin ℝ f s a) y ≤ 0

Tactic:
classical
exact
  if hf : DifferentiableWithinAt ℝ f s a then h.hasFDerivWithinAt_nonpos hf.hasFDerivWithinAt hy
  else by rw [fderivWithin_zero_of_not_differentiableWithinAt hf]; rfl

Result:
no goals