awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.Martingale.Upcrossing (goal)
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
hab : a < b
pos :
  ∀ (hN : N = 0),
    upcrossingsBefore a b f N ω =
      ∑ i ∈ Finset.Ico 1 (N + 1), Set.indicator {n : ℕ | upperCrossingTime a b f N n ω < N} 1 i
⊢ upcrossingsBefore a b f N ω =
    ∑ i ∈ Finset.Ico 1 (N + 1), Set.indicator {n : ℕ | upperCrossingTime a b f N n ω < N} 1 i
have neg : ∀ (hN : ¬N = 0),
  upcrossingsBefore a b f N ω =
    ∑ i ∈ Finset.Ico 1 (N + 1), Set.indicator {n : ℕ | upperCrossingTime a b f N n ω < N} 1 i
Tactic: by_cases hN : N = 0
-- Lean 4 proof step from Mathlib.Probability.Martingale.Upcrossing (goal)
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
hab : a < b
hN : ¬N = 0
⊢ upcrossingsBefore a b f N ω =
    ∑ i ∈ Finset.Ico 1 (N + 1), Set.indicator {n : ℕ | upperCrossingTime a b f N n ω < N} 1 i
have neg : upcrossingsBefore a b f N ω =
  HAdd.hAdd (α := ℕ)
    (∑ i ∈ Finset.Ico (Nat.succ 0) (upcrossingsBefore a b f N ω).succ,
      Set.indicator {n : ℕ | upperCrossingTime a b f N n ω < N} 1 i)
    (∑ i ∈ Finset.Ico (upcrossingsBefore a b f N ω).succ N.succ,
      Set.indicator {n : ℕ | upperCrossingTime a b f N n ω < N} 1 i)
Tactic: rw [← Finset.sum_Ico_consecutive _ (Nat.succ_le_succ zero_le')
    (Nat.succ_le_succ (upcrossingsBefore_le f ω hab))]
-- Lean 4 proof step from Mathlib.Probability.Martingale.Upcrossing (hypothesis)
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
hab : a < b
hN : ¬N = 0
k : ℕ
hk : k ∈ Finset.Ico 1 (upcrossingsBefore a b f N ω + 1)
⊢ Eq (α := ℕ) (Set.indicator {n : ℕ | upperCrossingTime a b f N n ω < N} 1 k) 1
have hk₁ : 1 ≤ k ∧ k < upcrossingsBefore a b f N ω + 1
Tactic: rw [Finset.mem_Ico] at hk
Cleared hypotheses: hk
-- Lean 4 proof step from Mathlib.Probability.Martingale.Upcrossing (goal)
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
hab : a < b
hN : ¬N = 0
k : ℕ
hk : 1 ≤ k ∧ k < upcrossingsBefore a b f N ω + 1
⊢ Eq (α := ℕ) (Set.indicator {n : ℕ | upperCrossingTime a b f N n ω < N} 1 k) 1
have rw : Eq (α := ℕ) (1 k) 1
Tactic: rw [Set.indicator_of_mem]
-- Lean 4 proof step from Mathlib.Probability.Martingale.Upcrossing (goal)
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
hab : a < b
hN : ¬N = 0
k : ℕ
hk : 1 ≤ k ∧ k < upcrossingsBefore a b f N ω + 1
rw : Eq (α := ℕ) (1 k) 1
⊢ Eq (α := ℕ) (Set.indicator {n : ℕ | upperCrossingTime a b f N n ω < N} 1 k) 1
have h : Membership.mem (γ := Set ℕ) {n : ℕ | upperCrossingTime a b f N n ω < N} k
Tactic: rw [Set.indicator_of_mem]
-- Lean 4 proof step from Mathlib.Probability.Martingale.Upcrossing (hypothesis)
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
hab : a < b
hN : ¬N = 0
⊢ upcrossingsBefore a b f N ω =
    HAdd.hAdd (α := ℕ)
      (∑ i ∈ Finset.Ico (Nat.succ 0) (upcrossingsBefore a b f N ω).succ,
        Set.indicator {n : ℕ | upperCrossingTime a b f N n ω < N} 1 i)
      (∑ i ∈ Finset.Ico (upcrossingsBefore a b f N ω).succ N.succ,
        Set.indicator {n : ℕ | upperCrossingTime a b f N n ω < N} 1 i)
have h₁ : ∀ k ∈ Finset.Ico 1 (upcrossingsBefore a b f N ω + 1),
  Eq (α := ℕ) (Set.indicator {n : ℕ | upperCrossingTime a b f N n ω < N} 1 k) 1
Tactic: have h₁ : ∀ k ∈ Finset.Ico 1 (upcrossingsBefore a b f N ω + 1),
      {n : ℕ | upperCrossingTime a b f N n ω < N}.indicator 1 k = 1 := by
    rintro k hk
    rw [Finset.mem_Ico] at hk
    rw [Set.indicator_of_mem]
    · rfl
    · exact upperCrossingTime_lt_of_le_upcrossingsBefore (zero_lt_iff.2 hN) hab
        (Nat.lt_succ_iff.1 hk.2)
-- Lean 4 proof step from Mathlib.Probability.Martingale.Upcrossing (hypothesis)
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
hab : a < b
hN : ¬N = 0
h₁ :
  ∀ k ∈ Finset.Ico 1 (upcrossingsBefore a b f N ω + 1),
    Eq (α := ℕ) (Set.indicator {n : ℕ | upperCrossingTime a b f N n ω < N} 1 k) 1
k : ℕ
hk : k ∈ Finset.Ico (upcrossingsBefore a b f N ω + 1) (N + 1)
⊢ Eq (α := ℕ) (Set.indicator {n : ℕ | upperCrossingTime a b f N n ω < N} 1 k) 0
have hk₁ : upcrossingsBefore a b f N ω < k ∧ k < N + 1
Tactic: rw [Finset.mem_Ico, Nat.succ_le_iff] at hk
Cleared hypotheses: hk
-- Lean 4 proof step from Mathlib.Probability.Martingale.Upcrossing (goal)
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
hab : a < b
hN : ¬N = 0
h₁ :
  ∀ k ∈ Finset.Ico 1 (upcrossingsBefore a b f N ω + 1),
    Eq (α := ℕ) (Set.indicator {n : ℕ | upperCrossingTime a b f N n ω < N} 1 k) 1
k : ℕ
hk : upcrossingsBefore a b f N ω < k ∧ k < N + 1
⊢ Eq (α := ℕ) (Set.indicator {n : ℕ | upperCrossingTime a b f N n ω < N} 1 k) 0
have h : k ∉ {n : ℕ | upperCrossingTime a b f N n ω < N}
Tactic: rw [Set.indicator_of_notMem]
-- Lean 4 proof step from Mathlib.Probability.Martingale.Upcrossing (goal)
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
hab : a < b
hN : ¬N = 0
h₁ :
  ∀ k ∈ Finset.Ico 1 (upcrossingsBefore a b f N ω + 1),
    Eq (α := ℕ) (Set.indicator {n : ℕ | upperCrossingTime a b f N n ω < N} 1 k) 1
k : ℕ
hk : upcrossingsBefore a b f N ω < k ∧ k < N + 1
⊢ k ∉ {n : ℕ | upperCrossingTime a b f N n ω < N}
have h : N ≤ upperCrossingTime a b f N k ω
Tactic: simp only [Set.mem_setOf_eq, not_lt]
-- Lean 4 proof step from Mathlib.Probability.Martingale.Upcrossing (hypothesis)
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
hab : a < b
hN : ¬N = 0
h₁ :
  ∀ k ∈ Finset.Ico 1 (upcrossingsBefore a b f N ω + 1),
    Eq (α := ℕ) (Set.indicator {n : ℕ | upperCrossingTime a b f N n ω < N} 1 k) 1
⊢ upcrossingsBefore a b f N ω =
    HAdd.hAdd (α := ℕ)
      (∑ i ∈ Finset.Ico (Nat.succ 0) (upcrossingsBefore a b f N ω).succ,
        Set.indicator {n : ℕ | upperCrossingTime a b f N n ω < N} 1 i)
      (∑ i ∈ Finset.Ico (upcrossingsBefore a b f N ω).succ N.succ,
        Set.indicator {n : ℕ | upperCrossingTime a b f N n ω < N} 1 i)
have h₂ : ∀ k ∈ Finset.Ico (upcrossingsBefore a b f N ω + 1) (N + 1),
  Eq (α := ℕ) (Set.indicator {n : ℕ | upperCrossingTime a b f N n ω < N} 1 k) 0
Tactic: have h₂ : ∀ k ∈ Finset.Ico (upcrossingsBefore a b f N ω + 1) (N + 1),
      {n : ℕ | upperCrossingTime a b f N n ω < N}.indicator 1 k = 0 := by
    rintro k hk
    rw [Finset.mem_Ico, Nat.succ_le_iff] at hk
    rw [Set.indicator_of_notMem]
    simp only [Set.mem_setOf_eq, not_lt]
    exact (upperCrossingTime_eq_of_upcrossingsBefore_lt hab hk.1).symm.le
-- Lean 4 proof step from Mathlib.Probability.Martingale.Upcrossing (goal)
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
hab : a < b
hN : ¬N = 0
h₁ :
  ∀ k ∈ Finset.Ico 1 (upcrossingsBefore a b f N ω + 1),
    Eq (α := ℕ) (Set.indicator {n : ℕ | upperCrossingTime a b f N n ω < N} 1 k) 1
h₂ :
  ∀ k ∈ Finset.Ico (upcrossingsBefore a b f N ω + 1) (N + 1),
    Eq (α := ℕ) (Set.indicator {n : ℕ | upperCrossingTime a b f N n ω < N} 1 k) 0
⊢ upcrossingsBefore a b f N ω =
    HAdd.hAdd (α := ℕ)
      (∑ i ∈ Finset.Ico (Nat.succ 0) (upcrossingsBefore a b f N ω).succ,
        Set.indicator {n : ℕ | upperCrossingTime a b f N n ω < N} 1 i)
      (∑ i ∈ Finset.Ico (upcrossingsBefore a b f N ω).succ N.succ,
        Set.indicator {n : ℕ | upperCrossingTime a b f N n ω < N} 1 i)
have neg : upcrossingsBefore a b f N ω =
  HAdd.hAdd (α := ℕ) (∑ x ∈ Finset.Ico 1 (upcrossingsBefore a b f N ω + 1), 1)
    (∑ i ∈ Finset.Ico (upcrossingsBefore a b f N ω).succ N.succ,
      Set.indicator {n : ℕ | upperCrossingTime a b f N n ω < N} 1 i)
Tactic: rw [Finset.sum_congr rfl h₁, Finset.sum_congr rfl h₂, Finset.sum_const, Finset.sum_const,
    smul_eq_mul, mul_one, smul_eq_mul, mul_zero, Nat.card_Ico, Nat.add_succ_sub_one,
    add_zero, add_zero]
-- Lean 4 proof step from Mathlib.Probability.Martingale.Upcrossing (goal)
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
hab : a < b
hN : ¬N = 0
h₁ :
  ∀ k ∈ Finset.Ico 1 (upcrossingsBefore a b f N ω + 1),
    Eq (α := ℕ) (Set.indicator {n : ℕ | upperCrossingTime a b f N n ω < N} 1 k) 1
h₂ :
  ∀ k ∈ Finset.Ico (upcrossingsBefore a b f N ω + 1) (N + 1),
    Eq (α := ℕ) (Set.indicator {n : ℕ | upperCrossingTime a b f N n ω < N} 1 k) 0
neg :
  upcrossingsBefore a b f N ω =
    HAdd.hAdd (α := ℕ) (∑ x ∈ Finset.Ico 1 (upcrossingsBefore a b f N ω + 1), 1)
      (∑ i ∈ Finset.Ico (upcrossingsBefore a b f N ω).succ N.succ,
        Set.indicator {n : ℕ | upperCrossingTime a b f N n ω < N} 1 i)
⊢ upcrossingsBefore a b f N ω =
    HAdd.hAdd (α := ℕ)
      (∑ i ∈ Finset.Ico (Nat.succ 0) (upcrossingsBefore a b f N ω).succ,
        Set.indicator {n : ℕ | upperCrossingTime a b f N n ω < N} 1 i)
      (∑ i ∈ Finset.Ico (upcrossingsBefore a b f N ω).succ N.succ,
        Set.indicator {n : ℕ | upperCrossingTime a b f N n ω < N} 1 i)
have neg₁ : upcrossingsBefore a b f N ω =
  HAdd.hAdd (α := ℕ) (∑ x ∈ Finset.Ico 1 (upcrossingsBefore a b f N ω + 1), 1)
    (∑ x ∈ Finset.Ico (upcrossingsBefore a b f N ω + 1) (N + 1), 0)
Tactic: rw [Finset.sum_congr rfl h₁, Finset.sum_congr rfl h₂, Finset.sum_const, Finset.sum_const,
    smul_eq_mul, mul_one, smul_eq_mul, mul_zero, Nat.card_Ico, Nat.add_succ_sub_one,
    add_zero, add_zero]
-- Lean 4 proof step from Mathlib.Probability.Martingale.Upcrossing (goal)
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
hab : a < b
hN : ¬N = 0
h₁ :
  ∀ k ∈ Finset.Ico 1 (upcrossingsBefore a b f N ω + 1),
    Eq (α := ℕ) (Set.indicator {n : ℕ | upperCrossingTime a b f N n ω < N} 1 k) 1
h₂ :
  ∀ k ∈ Finset.Ico (upcrossingsBefore a b f N ω + 1) (N + 1),
    Eq (α := ℕ) (Set.indicator {n : ℕ | upperCrossingTime a b f N n ω < N} 1 k) 0
neg :
  upcrossingsBefore a b f N ω =
    HAdd.hAdd (α := ℕ) (∑ x ∈ Finset.Ico 1 (upcrossingsBefore a b f N ω + 1), 1)
      (∑ i ∈ Finset.Ico (upcrossingsBefore a b f N ω).succ N.succ,
        Set.indicator {n : ℕ | upperCrossingTime a b f N n ω < N} 1 i)
neg₁ :
  upcrossingsBefore a b f N ω =
    HAdd.hAdd (α := ℕ) (∑ x ∈ Finset.Ico 1 (upcrossingsBefore a b f N ω + 1), 1)
      (∑ x ∈ Finset.Ico (upcrossingsBefore a b f N ω + 1) (N + 1), 0)
⊢ upcrossingsBefore a b f N ω =
    HAdd.hAdd (α := ℕ)
      (∑ i ∈ Finset.Ico (Nat.succ 0) (upcrossingsBefore a b f N ω).succ,
        Set.indicator {n : ℕ | upperCrossingTime a b f N n ω < N} 1 i)
      (∑ i ∈ Finset.Ico (upcrossingsBefore a b f N ω).succ N.succ,
        Set.indicator {n : ℕ | upperCrossingTime a b f N n ω < N} 1 i)
have neg₂ : upcrossingsBefore a b f N ω =
  HSMul.hSMul (β := ℕ) (Finset.Ico 1 (upcrossingsBefore a b f N ω + 1)).card 1 +
    ∑ x ∈ Finset.Ico (upcrossingsBefore a b f N ω + 1) (N + 1), 0
Tactic: rw [Finset.sum_congr rfl h₁, Finset.sum_congr rfl h₂, Finset.sum_const, Finset.sum_const,
    smul_eq_mul, mul_one, smul_eq_mul, mul_zero, Nat.card_Ico, Nat.add_succ_sub_one,
    add_zero, add_zero]
-- Lean 4 proof step from Mathlib.Probability.Martingale.Upcrossing (goal)
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
hab : a < b
hN : ¬N = 0
h₁ :
  ∀ k ∈ Finset.Ico 1 (upcrossingsBefore a b f N ω + 1),
    Eq (α := ℕ) (Set.indicator {n : ℕ | upperCrossingTime a b f N n ω < N} 1 k) 1
h₂ :
  ∀ k ∈ Finset.Ico (upcrossingsBefore a b f N ω + 1) (N + 1),
    Eq (α := ℕ) (Set.indicator {n : ℕ | upperCrossingTime a b f N n ω < N} 1 k) 0
neg :
  upcrossingsBefore a b f N ω =
    HAdd.hAdd (α := ℕ) (∑ x ∈ Finset.Ico 1 (upcrossingsBefore a b f N ω + 1), 1)
      (∑ i ∈ Finset.Ico (upcrossingsBefore a b f N ω).succ N.succ,
        Set.indicator {n : ℕ | upperCrossingTime a b f N n ω < N} 1 i)
neg₁ :
  upcrossingsBefore a b f N ω =
    HAdd.hAdd (α := ℕ) (∑ x ∈ Finset.Ico 1 (upcrossingsBefore a b f N ω + 1), 1)
      (∑ x ∈ Finset.Ico (upcrossingsBefore a b f N ω + 1) (N + 1), 0)
neg₂ :
  upcrossingsBefore a b f N ω =
    HSMul.hSMul (β := ℕ) (Finset.Ico 1 (upcrossingsBefore a b f N ω + 1)).card 1 +
      ∑ x ∈ Finset.Ico (upcrossingsBefore a b f N ω + 1) (N + 1), 0
⊢ upcrossingsBefore a b f N ω =
    HAdd.hAdd (α := ℕ)
      (∑ i ∈ Finset.Ico (Nat.succ 0) (upcrossingsBefore a b f N ω).succ,
        Set.indicator {n : ℕ | upperCrossingTime a b f N n ω < N} 1 i)
      (∑ i ∈ Finset.Ico (upcrossingsBefore a b f N ω).succ N.succ,
        Set.indicator {n : ℕ | upperCrossingTime a b f N n ω < N} 1 i)
have neg₃ : upcrossingsBefore a b f N ω =
  HSMul.hSMul (β := ℕ) (Finset.Ico 1 (upcrossingsBefore a b f N ω + 1)).card 1 +
    HSMul.hSMul (β := ℕ) (Finset.Ico (upcrossingsBefore a b f N ω + 1) (N + 1)).card 0
Tactic: rw [Finset.sum_congr rfl h₁, Finset.sum_congr rfl h₂, Finset.sum_const, Finset.sum_const,
    smul_eq_mul, mul_one, smul_eq_mul, mul_zero, Nat.card_Ico, Nat.add_succ_sub_one,
    add_zero, add_zero]
-- Lean 4 proof step from Mathlib.Probability.Martingale.Upcrossing (goal)
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
hab : a < b
hN : ¬N = 0
h₁ :
  ∀ k ∈ Finset.Ico 1 (upcrossingsBefore a b f N ω + 1),
    Eq (α := ℕ) (Set.indicator {n : ℕ | upperCrossingTime a b f N n ω < N} 1 k) 1
h₂ :
  ∀ k ∈ Finset.Ico (upcrossingsBefore a b f N ω + 1) (N + 1),
    Eq (α := ℕ) (Set.indicator {n : ℕ | upperCrossingTime a b f N n ω < N} 1 k) 0
neg :
  upcrossingsBefore a b f N ω =
    HAdd.hAdd (α := ℕ) (∑ x ∈ Finset.Ico 1 (upcrossingsBefore a b f N ω + 1), 1)
      (∑ i ∈ Finset.Ico (upcrossingsBefore a b f N ω).succ N.succ,
        Set.indicator {n : ℕ | upperCrossingTime a b f N n ω < N} 1 i)
neg₁ :
  upcrossingsBefore a b f N ω =
    HAdd.hAdd (α := ℕ) (∑ x ∈ Finset.Ico 1 (upcrossingsBefore a b f N ω + 1), 1)
      (∑ x ∈ Finset.Ico (upcrossingsBefore a b f N ω + 1) (N + 1), 0)
neg₂ :
  upcrossingsBefore a b f N ω =
    HSMul.hSMul (β := ℕ) (Finset.Ico 1 (upcrossingsBefore a b f N ω + 1)).card 1 +
      ∑ x ∈ Finset.Ico (upcrossingsBefore a b f N ω + 1) (N + 1), 0
neg₃ :
  upcrossingsBefore a b f N ω =
    HSMul.hSMul (β := ℕ) (Finset.Ico 1 (upcrossingsBefore a b f N ω + 1)).card 1 +
      HSMul.hSMul (β := ℕ) (Finset.Ico (upcrossingsBefore a b f N ω + 1) (N + 1)).card 0
⊢ upcrossingsBefore a b f N ω =
    HAdd.hAdd (α := ℕ)
      (∑ i ∈ Finset.Ico (Nat.succ 0) (upcrossingsBefore a b f N ω).succ,
        Set.indicator {n : ℕ | upperCrossingTime a b f N n ω < N} 1 i)
      (∑ i ∈ Finset.Ico (upcrossingsBefore a b f N ω).succ N.succ,
        Set.indicator {n : ℕ | upperCrossingTime a b f N n ω < N} 1 i)
have neg₄ : upcrossingsBefore a b f N ω =
  (Finset.Ico 1 (upcrossingsBefore a b f N ω + 1)).card * 1 +
    HSMul.hSMul (β := ℕ) (Finset.Ico (upcrossingsBefore a b f N ω + 1) (N + 1)).card 0
Tactic: rw [Finset.sum_congr rfl h₁, Finset.sum_congr rfl h₂, Finset.sum_const, Finset.sum_const,
    smul_eq_mul, mul_one, smul_eq_mul, mul_zero, Nat.card_Ico, Nat.add_succ_sub_one,
    add_zero, add_zero]
-- Lean 4 proof step from Mathlib.Probability.Martingale.Upcrossing (goal)
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
hab : a < b
hN : ¬N = 0
h₁ :
  ∀ k ∈ Finset.Ico 1 (upcrossingsBefore a b f N ω + 1),
    Eq (α := ℕ) (Set.indicator {n : ℕ | upperCrossingTime a b f N n ω < N} 1 k) 1
h₂ :
  ∀ k ∈ Finset.Ico (upcrossingsBefore a b f N ω + 1) (N + 1),
    Eq (α := ℕ) (Set.indicator {n : ℕ | upperCrossingTime a b f N n ω < N} 1 k) 0
neg :
  upcrossingsBefore a b f N ω =
    HAdd.hAdd (α := ℕ) (∑ x ∈ Finset.Ico 1 (upcrossingsBefore a b f N ω + 1), 1)
      (∑ i ∈ Finset.Ico (upcrossingsBefore a b f N ω).succ N.succ,
        Set.indicator {n : ℕ | upperCrossingTime a b f N n ω < N} 1 i)
neg₁ :
  upcrossingsBefore a b f N ω =
    HAdd.hAdd (α := ℕ) (∑ x ∈ Finset.Ico 1 (upcrossingsBefore a b f N ω + 1), 1)
      (∑ x ∈ Finset.Ico (upcrossingsBefore a b f N ω + 1) (N + 1), 0)
neg₂ :
  upcrossingsBefore a b f N ω =
    HSMul.hSMul (β := ℕ) (Finset.Ico 1 (upcrossingsBefore a b f N ω + 1)).card 1 +
      ∑ x ∈ Finset.Ico (upcrossingsBefore a b f N ω + 1) (N + 1), 0
neg₃ :
  upcrossingsBefore a b f N ω =
    HSMul.hSMul (β := ℕ) (Finset.Ico 1 (upcrossingsBefore a b f N ω + 1)).card 1 +
      HSMul.hSMul (β := ℕ) (Finset.Ico (upcrossingsBefore a b f N ω + 1) (N + 1)).card 0
neg₄ :
  upcrossingsBefore a b f N ω =
    (Finset.Ico 1 (upcrossingsBefore a b f N ω + 1)).card * 1 +
      HSMul.hSMul (β := ℕ) (Finset.Ico (upcrossingsBefore a b f N ω + 1) (N + 1)).card 0
⊢ upcrossingsBefore a b f N ω =
    HAdd.hAdd (α := ℕ)
      (∑ i ∈ Finset.Ico (Nat.succ 0) (upcrossingsBefore a b f N ω).succ,
        Set.indicator {n : ℕ | upperCrossingTime a b f N n ω < N} 1 i)
      (∑ i ∈ Finset.Ico (upcrossingsBefore a b f N ω).succ N.succ,
        Set.indicator {n : ℕ | upperCrossingTime a b f N n ω < N} 1 i)
have neg₅ : upcrossingsBefore a b f N ω =
  (Finset.Ico 1 (upcrossingsBefore a b f N ω + 1)).card +
    HSMul.hSMul (β := ℕ) (Finset.Ico (upcrossingsBefore a b f N ω + 1) (N + 1)).card 0
Tactic: rw [Finset.sum_congr rfl h₁, Finset.sum_congr rfl h₂, Finset.sum_const, Finset.sum_const,
    smul_eq_mul, mul_one, smul_eq_mul, mul_zero, Nat.card_Ico, Nat.add_succ_sub_one,
    add_zero, add_zero]
-- Lean 4 proof step from Mathlib.Probability.Martingale.Upcrossing (goal)
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
hab : a < b
hN : ¬N = 0
h₁ :
  ∀ k ∈ Finset.Ico 1 (upcrossingsBefore a b f N ω + 1),
    Eq (α := ℕ) (Set.indicator {n : ℕ | upperCrossingTime a b f N n ω < N} 1 k) 1
h₂ :
  ∀ k ∈ Finset.Ico (upcrossingsBefore a b f N ω + 1) (N + 1),
    Eq (α := ℕ) (Set.indicator {n : ℕ | upperCrossingTime a b f N n ω < N} 1 k) 0
neg :
  upcrossingsBefore a b f N ω =
    HAdd.hAdd (α := ℕ) (∑ x ∈ Finset.Ico 1 (upcrossingsBefore a b f N ω + 1), 1)
      (∑ i ∈ Finset.Ico (upcrossingsBefore a b f N ω).succ N.succ,
        Set.indicator {n : ℕ | upperCrossingTime a b f N n ω < N} 1 i)
neg₁ :
  upcrossingsBefore a b f N ω =
    HAdd.hAdd (α := ℕ) (∑ x ∈ Finset.Ico 1 (upcrossingsBefore a b f N ω + 1), 1)
      (∑ x ∈ Finset.Ico (upcrossingsBefore a b f N ω + 1) (N + 1), 0)
neg₂ :
  upcrossingsBefore a b f N ω =
    HSMul.hSMul (β := ℕ) (Finset.Ico 1 (upcrossingsBefore a b f N ω + 1)).card 1 +
      ∑ x ∈ Finset.Ico (upcrossingsBefore a b f N ω + 1) (N + 1), 0
neg₃ :
  upcrossingsBefore a b f N ω =
    HSMul.hSMul (β := ℕ) (Finset.Ico 1 (upcrossingsBefore a b f N ω + 1)).card 1 +
      HSMul.hSMul (β := ℕ) (Finset.Ico (upcrossingsBefore a b f N ω + 1) (N + 1)).card 0
neg₄ :
  upcrossingsBefore a b f N ω =
    (Finset.Ico 1 (upcrossingsBefore a b f N ω + 1)).card * 1 +
      HSMul.hSMul (β := ℕ) (Finset.Ico (upcrossingsBefore a b f N ω + 1) (N + 1)).card 0
neg₅ :
  upcrossingsBefore a b f N ω =
    (Finset.Ico 1 (upcrossingsBefore a b f N ω + 1)).card +
      HSMul.hSMul (β := ℕ) (Finset.Ico (upcrossingsBefore a b f N ω + 1) (N + 1)).card 0
⊢ upcrossingsBefore a b f N ω =
    HAdd.hAdd (α := ℕ)
      (∑ i ∈ Finset.Ico (Nat.succ 0) (upcrossingsBefore a b f N ω).succ,
        Set.indicator {n : ℕ | upperCrossingTime a b f N n ω < N} 1 i)
      (∑ i ∈ Finset.Ico (upcrossingsBefore a b f N ω).succ N.succ,
        Set.indicator {n : ℕ | upperCrossingTime a b f N n ω < N} 1 i)
have neg₆ : upcrossingsBefore a b f N ω =
  (Finset.Ico 1 (upcrossingsBefore a b f N ω + 1)).card +
    (Finset.Ico (upcrossingsBefore a b f N ω + 1) (N + 1)).card * 0
Tactic: rw [Finset.sum_congr rfl h₁, Finset.sum_congr rfl h₂, Finset.sum_const, Finset.sum_const,
    smul_eq_mul, mul_one, smul_eq_mul, mul_zero, Nat.card_Ico, Nat.add_succ_sub_one,
    add_zero, add_zero]
-- Lean 4 proof step from Mathlib.Probability.Martingale.Upcrossing (goal)
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
hab : a < b
hN : ¬N = 0
h₁ :
  ∀ k ∈ Finset.Ico 1 (upcrossingsBefore a b f N ω + 1),
    Eq (α := ℕ) (Set.indicator {n : ℕ | upperCrossingTime a b f N n ω < N} 1 k) 1
h₂ :
  ∀ k ∈ Finset.Ico (upcrossingsBefore a b f N ω + 1) (N + 1),
    Eq (α := ℕ) (Set.indicator {n : ℕ | upperCrossingTime a b f N n ω < N} 1 k) 0
neg :
  upcrossingsBefore a b f N ω =
    HAdd.hAdd (α := ℕ) (∑ x ∈ Finset.Ico 1 (upcrossingsBefore a b f N ω + 1), 1)
      (∑ i ∈ Finset.Ico (upcrossingsBefore a b f N ω).succ N.succ,
        Set.indicator {n : ℕ | upperCrossingTime a b f N n ω < N} 1 i)
neg₁ :
  upcrossingsBefore a b f N ω =
    HAdd.hAdd (α := ℕ) (∑ x ∈ Finset.Ico 1 (upcrossingsBefore a b f N ω + 1), 1)
      (∑ x ∈ Finset.Ico (upcrossingsBefore a b f N ω + 1) (N + 1), 0)
neg₂ :
  upcrossingsBefore a b f N ω =
    HSMul.hSMul (β := ℕ) (Finset.Ico 1 (upcrossingsBefore a b f N ω + 1)).card 1 +
      ∑ x ∈ Finset.Ico (upcrossingsBefore a b f N ω + 1) (N + 1), 0
neg₃ :
  upcrossingsBefore a b f N ω =
    HSMul.hSMul (β := ℕ) (Finset.Ico 1 (upcrossingsBefore a b f N ω + 1)).card 1 +
      HSMul.hSMul (β := ℕ) (Finset.Ico (upcrossingsBefore a b f N ω + 1) (N + 1)).card 0
neg₄ :
  upcrossingsBefore a b f N ω =
    (Finset.Ico 1 (upcrossingsBefore a b f N ω + 1)).card * 1 +
      HSMul.hSMul (β := ℕ) (Finset.Ico (upcrossingsBefore a b f N ω + 1) (N + 1)).card 0
neg₅ :
  upcrossingsBefore a b f N ω =
    (Finset.Ico 1 (upcrossingsBefore a b f N ω + 1)).card +
      HSMul.hSMul (β := ℕ) (Finset.Ico (upcrossingsBefore a b f N ω + 1) (N + 1)).card 0
neg₆ :
  upcrossingsBefore a b f N ω =
    (Finset.Ico 1 (upcrossingsBefore a b f N ω + 1)).card +
      (Finset.Ico (upcrossingsBefore a b f N ω + 1) (N + 1)).card * 0
⊢ upcrossingsBefore a b f N ω =
    HAdd.hAdd (α := ℕ)
      (∑ i ∈ Finset.Ico (Nat.succ 0) (upcrossingsBefore a b f N ω).succ,
        Set.indicator {n : ℕ | upperCrossingTime a b f N n ω < N} 1 i)
      (∑ i ∈ Finset.Ico (upcrossingsBefore a b f N ω).succ N.succ,
        Set.indicator {n : ℕ | upperCrossingTime a b f N n ω < N} 1 i)
have neg₇ : upcrossingsBefore a b f N ω = (Finset.Ico 1 (upcrossingsBefore a b f N ω + 1)).card + 0
Tactic: rw [Finset.sum_congr rfl h₁, Finset.sum_congr rfl h₂, Finset.sum_const, Finset.sum_const,
    smul_eq_mul, mul_one, smul_eq_mul, mul_zero, Nat.card_Ico, Nat.add_succ_sub_one,
    add_zero, add_zero]
-- Lean 4 proof step from Mathlib.Probability.Martingale.Upcrossing (goal)
Goal:
Ω : Type u_1
a b : ℝ
f : ℕ → Ω → ℝ
N : ℕ
ω : Ω
hab : a < b
hN : ¬N = 0
h₁ :
  ∀ k ∈ Finset.Ico 1 (upcrossingsBefore a b f N ω + 1),
    Eq (α := ℕ) (Set.indicator {n : ℕ | upperCrossingTime a b f N n ω < N} 1 k) 1
h₂ :
  ∀ k ∈ Finset.Ico (upcrossingsBefore a b f N ω + 1) (N + 1),
    Eq (α := ℕ) (Set.indicator {n : ℕ | upperCrossingTime a b f N n ω < N} 1 k) 0
neg :
  upcrossingsBefore a b f N ω =
    HAdd.hAdd (α := ℕ) (∑ x ∈ Finset.Ico 1 (upcrossingsBefore a b f N ω + 1), 1)
      (∑ i ∈ Finset.Ico (upcrossingsBefore a b f N ω).succ N.succ,
        Set.indicator {n : ℕ | upperCrossingTime a b f N n ω < N} 1 i)
neg₁ :
  upcrossingsBefore a b f N ω =
    HAdd.hAdd (α := ℕ) (∑ x ∈ Finset.Ico 1 (upcrossingsBefore a b f N ω + 1), 1)
      (∑ x ∈ Finset.Ico (upcrossingsBefore a b f N ω + 1) (N + 1), 0)
neg₂ :
  upcrossingsBefore a b f N ω =
    HSMul.hSMul (β := ℕ) (Finset.Ico 1 (upcrossingsBefore a b f N ω + 1)).card 1 +
      ∑ x ∈ Finset.Ico (upcrossingsBefore a b f N ω + 1) (N + 1), 0
neg₃ :
  upcrossingsBefore a b f N ω =
    HSMul.hSMul (β := ℕ) (Finset.Ico 1 (upcrossingsBefore a b f N ω + 1)).card 1 +
      HSMul.hSMul (β := ℕ) (Finset.Ico (upcrossingsBefore a b f N ω + 1) (N + 1)).card 0
neg₄ :
  upcrossingsBefore a b f N ω =
    (Finset.Ico 1 (upcrossingsBefore a b f N ω + 1)).card * 1 +
      HSMul.hSMul (β := ℕ) (Finset.Ico (upcrossingsBefore a b f N ω + 1) (N + 1)).card 0
neg₅ :
  upcrossingsBefore a b f N ω =
    (Finset.Ico 1 (upcrossingsBefore a b f N ω + 1)).card +
      HSMul.hSMul (β := ℕ) (Finset.Ico (upcrossingsBefore a b f N ω + 1) (N + 1)).card 0
neg₆ :
  upcrossingsBefore a b f N ω =
    (Finset.Ico 1 (upcrossingsBefore a b f N ω + 1)).card +
      (Finset.Ico (upcrossingsBefore a b f N ω + 1) (N + 1)).card * 0
neg₇ : upcrossingsBefore a b f N ω = (Finset.Ico 1 (upcrossingsBefore a b f N ω + 1)).card + 0
⊢ upcrossingsBefore a b f N ω =
    HAdd.hAdd (α := ℕ)
      (∑ i ∈ Finset.Ico (Nat.succ 0) (upcrossingsBefore a b f N ω).succ,
        Set.indicator {n : ℕ | upperCrossingTime a b f N n ω < N} 1 i)
      (∑ i ∈ Finset.Ico (upcrossingsBefore a b f N ω).succ N.succ,
        Set.indicator {n : ℕ | upperCrossingTime a b f N n ω < N} 1 i)
have neg₈ : upcrossingsBefore a b f N ω = upcrossingsBefore a b f N ω + 1 - 1 + 0
Tactic: rw [Finset.sum_congr rfl h₁, Finset.sum_congr rfl h₂, Finset.sum_const, Finset.sum_const,
    smul_eq_mul, mul_one, smul_eq_mul, mul_zero, Nat.card_Ico, Nat.add_succ_sub_one,
    add_zero, add_zero]