awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Holor (goal)
Goal:
α : Type
ds : List ℕ
inst : NonUnitalNonAssocSemiring α
β : Type u_1
n : ℕ
s_1 : Finset β
f : β → Holor α ds
this : DecidableEq β := Classical.decEq β
x : β
s : Finset β
h_x_notin_s : x ∉ s
ih : (∀ x ∈ s, CPRankMax n (f x)) → CPRankMax (α := α) (s.card * n) (ds := ds) (∑ x ∈ s, f x)
h_cprank : ∀ x_1 ∈ insert x s, CPRankMax n (f x_1)
⊢ CPRankMax ((s.card + 1) * n) (f x + ∑ x ∈ s, f x)
have rw : CPRankMax (s.card * n + 1 * n) (f x + ∑ x ∈ s, f x)
Tactic: rw [Nat.right_distrib]
-- Lean 4 proof step from Mathlib.Data.Holor (goal)
Goal:
α : Type
ds : List ℕ
inst : NonUnitalNonAssocSemiring α
β : Type u_1
n : ℕ
s_1 : Finset β
f : β → Holor α ds
this : DecidableEq β := Classical.decEq β
x : β
s : Finset β
h_x_notin_s : x ∉ s
ih : (∀ x ∈ s, CPRankMax n (f x)) → CPRankMax (α := α) (s.card * n) (ds := ds) (∑ x ∈ s, f x)
h_cprank : ∀ x_1 ∈ insert x s, CPRankMax n (f x_1)
⊢ CPRankMax (s.card * n + 1 * n) (f x + ∑ x ∈ s, f x)
have simp : CPRankMax (n + s.card * n) (f x + ∑ x ∈ s, f x)
Tactic: simp only [Nat.one_mul, Nat.add_comm]
-- Lean 4 proof step from Mathlib.Data.Holor (hypothesis)
Goal:
α : Type
ds : List ℕ
inst : NonUnitalNonAssocSemiring α
β : Type u_1
n : ℕ
s_1 : Finset β
f : β → Holor α ds
this : DecidableEq β := Classical.decEq β
x : β
s : Finset β
h_x_notin_s : x ∉ s
ih : (∀ x ∈ s, CPRankMax n (f x)) → CPRankMax (α := α) (s.card * n) (ds := ds) (∑ x ∈ s, f x)
h_cprank : ∀ x_1 ∈ insert x s, CPRankMax n (f x_1)
⊢ CPRankMax (n + s.card * n) (f x + ∑ x ∈ s, f x)
have ih' : CPRankMax (α := α) (s.card * n) (ds := ds) (∑ x ∈ s, f x)
Tactic: have ih' : CPRankMax (Finset.card s * n) (∑ x ∈ s, f x) := by grind
-- Lean 4 proof step from Mathlib.Data.Holor (hypothesis)
Goal:
α : Type
inst : Semiring α
d : ℕ
ds : List ℕ
x : Holor α (d :: ds)
⊢ CPRankMax (d :: ds).prod x
have h_summands : ∀ (i : ↥(Finset.range d)), CPRankMax ds.prod (unitVec d (↑i : ℕ) ⊗ x.slice (↑i : ℕ) sorry)
Tactic: have h_summands :
      ∀ i : { x // x ∈ Finset.range d },
        CPRankMax ds.prod (unitVec d i.1 ⊗ slice x i.1 (mem_range.1 i.2)) :=
      fun i => cprankMax_mul _ _ _ (cprankMax_upper_bound (slice x i.1 (mem_range.1 i.2)))
-- Lean 4 proof step from Mathlib.Data.Holor (hypothesis)
Goal:
α : Type
inst : Semiring α
d : ℕ
ds : List ℕ
x : Holor α (d :: ds)
h_summands : ∀ (i : ↥(Finset.range d)), CPRankMax ds.prod (unitVec d (↑i : ℕ) ⊗ x.slice (↑i : ℕ) ⋯)
⊢ CPRankMax (d :: ds).prod x
have h_dds_prod : (d :: ds).prod = (Finset.range d).card * ds.prod
Tactic: have h_dds_prod : (List.cons d ds).prod = Finset.card (Finset.range d) * prod ds := by
      simp [Finset.card_range]
-- Lean 4 proof step from Mathlib.Data.Holor (hypothesis)
Goal:
α : Type
inst : Semiring α
d : ℕ
ds : List ℕ
x : Holor α (d :: ds)
h_summands : ∀ (i : ↥(Finset.range d)), CPRankMax ds.prod (unitVec d (↑i : ℕ) ⊗ x.slice (↑i : ℕ) ⋯)
h_dds_prod : (d :: ds).prod = (Finset.range d).card * ds.prod
⊢ CPRankMax (d :: ds).prod x
have this : CPRankMax (α := α) ((Finset.range d).attach.card * ds.prod) (ds := [d] ++ ds)
  (∑ i ∈ (Finset.range d).attach, unitVec d (↑i : ℕ) ⊗ x.slice (↑i : ℕ) sorry)
Tactic: have :
      CPRankMax (Finset.card (Finset.attach (Finset.range d)) * prod ds)
        (∑ i ∈ Finset.attach (Finset.range d),
          unitVec d i.val ⊗ slice x i.val (mem_range.1 i.2)) :=
      cprankMax_sum (Finset.range d).attach _ fun i _ => h_summands i
-- Lean 4 proof step from Mathlib.Data.Holor (goal)
Goal:
α : Type
inst : Semiring α
d : ℕ
ds : List ℕ
x : Holor α (d :: ds)
h_summands : ∀ (i : ↥(Finset.range d)), CPRankMax ds.prod (unitVec d (↑i : ℕ) ⊗ x.slice (↑i : ℕ) ⋯)
h_dds_prod : (d :: ds).prod = (Finset.range d).card * ds.prod
this :
  CPRankMax (α := α) ((Finset.range d).attach.card * ds.prod) (ds := [d] ++ ds)
    (∑ i ∈ (Finset.range d).attach, unitVec d (↑i : ℕ) ⊗ x.slice (↑i : ℕ) ⋯)
⊢ CPRankMax (α := α) ((Finset.range d).card * ds.prod) (ds := [d] ++ ds)
    (∑ i ∈ (Finset.range d).attach, unitVec d (↑i : ℕ) ⊗ x.slice (↑i : ℕ) ⋯)
have rwa : ∀
  (this :
    CPRankMax (α := α) ((Finset.range d).card * ds.prod) (ds := [d] ++ ds)
      (∑ i ∈ (Finset.range d).attach, unitVec d (↑i : ℕ) ⊗ x.slice (↑i : ℕ) sorry)),
  CPRankMax (α := α) ((Finset.range d).card * ds.prod) (ds := [d] ++ ds)
    (∑ i ∈ (Finset.range d).attach, unitVec d (↑i : ℕ) ⊗ x.slice (↑i : ℕ) sorry)
Tactic: rwa [Finset.card_attach] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Data.Holor (hypothesis)
Goal:
α : Type
inst : Semiring α
d : ℕ
ds : List ℕ
x : Holor α (d :: ds)
h_summands : ∀ (i : ↥(Finset.range d)), CPRankMax ds.prod (unitVec d (↑i : ℕ) ⊗ x.slice (↑i : ℕ) ⋯)
h_dds_prod : (d :: ds).prod = (Finset.range d).card * ds.prod
this :
  CPRankMax (α := α) ((Finset.range d).attach.card * ds.prod) (ds := [d] ++ ds)
    (∑ i ∈ (Finset.range d).attach, unitVec d (↑i : ℕ) ⊗ x.slice (↑i : ℕ) ⋯)
⊢ CPRankMax (d :: ds).prod x
have h_cprankMax_sum : CPRankMax (α := α) ((Finset.range d).card * ds.prod) (ds := [d] ++ ds)
  (∑ i ∈ (Finset.range d).attach, unitVec d (↑i : ℕ) ⊗ x.slice (↑i : ℕ) sorry)
Tactic: have h_cprankMax_sum :
      CPRankMax (Finset.card (Finset.range d) * prod ds)
        (∑ i ∈ Finset.attach (Finset.range d),
          unitVec d i.val ⊗ slice x i.val (mem_range.1 i.2)) := by rwa [Finset.card_attach] at this
-- Lean 4 proof step from Mathlib.Data.Holor (goal)
Goal:
α : Type
inst : Semiring α
d : ℕ
ds : List ℕ
x : Holor α (d :: ds)
h_summands : ∀ (i : ↥(Finset.range d)), CPRankMax ds.prod (unitVec d (↑i : ℕ) ⊗ x.slice (↑i : ℕ) ⋯)
h_dds_prod : (d :: ds).prod = (Finset.range d).card * ds.prod
this :
  CPRankMax (α := α) ((Finset.range d).attach.card * ds.prod) (ds := [d] ++ ds)
    (∑ i ∈ (Finset.range d).attach, unitVec d (↑i : ℕ) ⊗ x.slice (↑i : ℕ) ⋯)
h_cprankMax_sum :
  CPRankMax (α := α) ((Finset.range d).card * ds.prod) (ds := [d] ++ ds)
    (∑ i ∈ (Finset.range d).attach, unitVec d (↑i : ℕ) ⊗ x.slice (↑i : ℕ) ⋯)
⊢ CPRankMax (d :: ds).prod x
have rw : CPRankMax (α := α) (d :: ds).prod (ds := d :: ds)
  (∑ i ∈ (Finset.range d).attach, unitVec d (↑i : ℕ) ⊗ x.slice (↑i : ℕ) sorry)
Tactic: rw [← sum_unitVec_mul_slice x]
-- Lean 4 proof step from Mathlib.Data.Holor (goal)
Goal:
α : Type
inst : Semiring α
d : ℕ
ds : List ℕ
x : Holor α (d :: ds)
h_summands : ∀ (i : ↥(Finset.range d)), CPRankMax ds.prod (unitVec d (↑i : ℕ) ⊗ x.slice (↑i : ℕ) ⋯)
h_dds_prod : (d :: ds).prod = (Finset.range d).card * ds.prod
this :
  CPRankMax (α := α) ((Finset.range d).attach.card * ds.prod) (ds := [d] ++ ds)
    (∑ i ∈ (Finset.range d).attach, unitVec d (↑i : ℕ) ⊗ x.slice (↑i : ℕ) ⋯)
h_cprankMax_sum :
  CPRankMax (α := α) ((Finset.range d).card * ds.prod) (ds := [d] ++ ds)
    (∑ i ∈ (Finset.range d).attach, unitVec d (↑i : ℕ) ⊗ x.slice (↑i : ℕ) ⋯)
⊢ CPRankMax (α := α) (d :: ds).prod (ds := d :: ds)
    (∑ i ∈ (Finset.range d).attach, unitVec d (↑i : ℕ) ⊗ x.slice (↑i : ℕ) ⋯)
have rw : CPRankMax (α := α) ((Finset.range d).card * ds.prod) (ds := d :: ds)
  (∑ i ∈ (Finset.range d).attach, unitVec d (↑i : ℕ) ⊗ x.slice (↑i : ℕ) sorry)
Tactic: rw [h_dds_prod]
-- Lean 4 proof step from Mathlib.Data.Int.AbsoluteValue (goal)
Goal:
S : Type u_2
inst : CommRing S
inst_1 : LinearOrder S
inst_2 : IsStrictOrderedRing S
abv : AbsoluteValue ℤ S
x : ℤˣ
⊢ Eq (α := S) ((abv : (a : ℤ) → S) (↑x : ℤ) : S) (1 : S)
have inl : Eq (α := S) ((abv : (a : ℤ) → S) (↑1 : ℤ) : S) (1 : S)
Tactic: rcases Int.units_eq_one_or x with (rfl | rfl)
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Data.Int.AbsoluteValue (goal)
Goal:
S : Type u_2
inst : CommRing S
inst_1 : LinearOrder S
inst_2 : IsStrictOrderedRing S
abv : AbsoluteValue ℤ S
x : ℤˣ
inl : Eq (α := S) ((abv : (a : ℤ) → S) (↑1 : ℤ) : S) (1 : S)
⊢ Eq (α := S) ((abv : (a : ℤ) → S) (↑x : ℤ) : S) (1 : S)
have inr : Eq (α := S) ((abv : (a : ℤ) → S) (↑(-1) : ℤ) : S) (1 : S)
Tactic: rcases Int.units_eq_one_or x with (rfl | rfl)
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Data.Int.AbsoluteValue (goal)
Goal:
R : Type u_1
S : Type u_2
inst : Ring R
inst_1 : CommRing S
inst_2 : LinearOrder S
inst_3 : IsStrictOrderedRing S
inst_4 : Nontrivial R
abv : AbsoluteValue R S
x : ℤˣ
⊢ Eq.{u_2 + 1} (α := S) ((abv : (a : R) → S) (↑(↑x : ℤ) : R) : S) (1 : S)
have inl : Eq.{u_2 + 1} (α := S) ((abv : (a : R) → S) (↑(↑1 : ℤ) : R) : S) (1 : S)
Tactic: rcases Int.units_eq_one_or x with (rfl | rfl)
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Data.Int.AbsoluteValue (goal)
Goal:
R : Type u_1
S : Type u_2
inst : Ring R
inst_1 : CommRing S
inst_2 : LinearOrder S
inst_3 : IsStrictOrderedRing S
inst_4 : Nontrivial R
abv : AbsoluteValue R S
x : ℤˣ
inl : Eq.{u_2 + 1} (α := S) ((abv : (a : R) → S) (↑(↑1 : ℤ) : R) : S) (1 : S)
⊢ Eq.{u_2 + 1} (α := S) ((abv : (a : R) → S) (↑(↑x : ℤ) : R) : S) (1 : S)
have inr : Eq.{u_2 + 1} (α := S) ((abv : (a : R) → S) (↑(↑(-1) : ℤ) : R) : S) (1 : S)
Tactic: rcases Int.units_eq_one_or x with (rfl | rfl)
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Data.Int.AbsoluteValue (goal)
Goal:
R : Type u_1
S : Type u_2
inst : Ring R
inst_1 : CommRing S
inst_2 : LinearOrder S
inst_3 : IsStrictOrderedRing S
abv : AbsoluteValue R S
x : ℤˣ
y : R
⊢ Eq.{u_2 + 1} (α := S) ((abv : (a : R) → S) (x • y) : S) ((abv : (a : R) → S) y : S)
have inl : Eq.{u_2 + 1} (α := S) ((abv : (a : R) → S) (HSMul.hSMul (α := ℤˣ) 1 y) : S) ((abv : (a : R) → S) y : S)
Tactic: rcases Int.units_eq_one_or x with (rfl | rfl)
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Data.Int.AbsoluteValue (goal)
Goal:
R : Type u_1
S : Type u_2
inst : Ring R
inst_1 : CommRing S
inst_2 : LinearOrder S
inst_3 : IsStrictOrderedRing S
abv : AbsoluteValue R S
x : ℤˣ
y : R
inl : Eq.{u_2 + 1} (α := S) ((abv : (a : R) → S) (HSMul.hSMul (α := ℤˣ) 1 y) : S) ((abv : (a : R) → S) y : S)
⊢ Eq.{u_2 + 1} (α := S) ((abv : (a : R) → S) (x • y) : S) ((abv : (a : R) → S) y : S)
have inr : Eq.{u_2 + 1} (α := S) ((abv : (a : R) → S) (HSMul.hSMul (α := ℤˣ) (-1) y) : S) ((abv : (a : R) → S) y : S)
Tactic: rcases Int.units_eq_one_or x with (rfl | rfl)
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Data.Int.Associated (goal)
Goal:
a b : ℤ
⊢ a.natAbs = b.natAbs ↔ Associated a b
have refine : a = b ∨ a = -b ↔ Associated a b
Tactic: refine Int.natAbs_eq_natAbs_iff.trans ?_
-- Lean 4 proof step from Mathlib.Data.Int.Associated (goal)
Goal:
a b : ℤ
⊢ a = b ∨ a = -b ↔ Associated a b
have mp : a = b ∨ a = -b → Associated a b
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Int.Associated (goal)
Goal:
a b : ℤ
mp : a = b ∨ a = -b → Associated a b
⊢ a = b ∨ a = -b ↔ Associated a b
have mpr : Associated a b → a = b ∨ a = -b
Tactic: constructor
-- Lean 4 proof step from Mathlib.Data.Int.Associated (goal)
Goal:
a : ℤ
u : ℤˣ
⊢ a = a * (↑u : ℤ) ∨ a = -(a * (↑u : ℤ))
have mpr : a = a * (↑1 : ℤ) ∨ a = -(a * (↑1 : ℤ))
Tactic: obtain rfl | rfl := Int.units_eq_one_or u
Cleared hypotheses: u
-- Lean 4 proof step from Mathlib.Data.Int.Associated (goal)
Goal:
a : ℤ
u : ℤˣ
mpr : a = a * (↑1 : ℤ) ∨ a = -(a * (↑1 : ℤ))
⊢ a = a * (↑u : ℤ) ∨ a = -(a * (↑u : ℤ))
have mpr₁ : a = a * (↑(-1) : ℤ) ∨ a = -(a * (↑(-1) : ℤ))
Tactic: obtain rfl | rfl := Int.units_eq_one_or u
Cleared hypotheses: u
-- Lean 4 proof step from Mathlib.Data.Int.Basic (goal)
Goal:
m n : ℤ
P : ℤ → Sort u_1
lt : (n : ℤ) → n < m → P n
ge : (n : ℤ) → n ≥ m → ((k : ℤ) → k < n → P k) → P n
⊢ ∀ (hn : m ≤ n),
    Int.strongRec (motive := fun (x : ℤ) ↦ P x) lt ge n =
      ge n hn fun (k : ℤ) (x : k < n) ↦ Int.strongRec (motive := fun (x : ℤ) ↦ P x) lt ge k
have refine : ∀ (n : ℤ),
  n ≥ m →
    ∀
      (ih :
        ∀ (k : ℤ),
          k < n →
            ∀ (hn : m ≤ k),
              Int.strongRec (motive := fun (x : ℤ) ↦ P x) lt ge k =
                ge k hn fun (k_1 : ℤ) (x : k_1 < k) ↦ Int.strongRec (motive := fun (x : ℤ) ↦ P x) lt ge k_1)
      (hn : m ≤ n),
      Int.strongRec (motive := fun (x : ℤ) ↦ P x) lt ge n =
        ge n hn fun (k : ℤ) (x : k < n) ↦ Int.strongRec (motive := fun (x : ℤ) ↦ P x) lt ge k
Tactic: refine m.strongRec (fun n hnm hmn ↦ (Int.not_lt.mpr hmn hnm).elim) (fun n _ ih hn ↦ ?_) n
-- Lean 4 proof step from Mathlib.Data.Int.Basic (goal)
Goal:
m n_1 : ℤ
P : ℤ → Sort u_1
lt : (n : ℤ) → n < m → P n
ge : (n : ℤ) → n ≥ m → ((k : ℤ) → k < n → P k) → P n
n : ℤ
h : n ≥ m
ih :
  ∀ (k : ℤ),
    k < n →
      ∀ (hn : m ≤ k),
        Int.strongRec (motive := fun (x : ℤ) ↦ P x) lt ge k =
          ge k hn fun (k_1 : ℤ) (x : k_1 < k) ↦ Int.strongRec (motive := fun (x : ℤ) ↦ P x) lt ge k_1
hn : m ≤ n
⊢ Int.strongRec (motive := fun (x : ℤ) ↦ P x) lt ge n =
    ge n hn fun (k : ℤ) (x : k < n) ↦ Int.strongRec (motive := fun (x : ℤ) ↦ P x) lt ge k
have rw : ge n sorry
    (Int.inductionOn' (motive := fun (x : ℤ) ↦ (k : ℤ) → k < x → P k) n m lt
      (fun (_n : ℤ) (a : m ≤ _n) (ih : (k : ℤ) → k < _n → P k) (l : ℤ) (a_1 : l < _n + 1) ↦
        if hlm : l < m then lt l hlm else ge l sorry fun (k : ℤ) (x : k < l) ↦ ih k sorry)
      fun (n : ℤ) (x : n ≤ m) (hn : (k : ℤ) → k < n → P k) (l : ℤ) (x_1 : l < n - 1) ↦ hn l sorry) =
  ge n hn fun (k : ℤ) (x : k < n) ↦ Int.strongRec (motive := fun (x : ℤ) ↦ P x) lt ge k
Tactic: rw [Int.strongRec, dif_neg (Int.not_lt.mpr hn)]
-- Lean 4 proof step from Mathlib.Data.Int.Basic (goal)
Goal:
m n_1 : ℤ
P : ℤ → Sort u_1
lt : (n : ℤ) → n < m → P n
ge : (n : ℤ) → n ≥ m → ((k : ℤ) → k < n → P k) → P n
n : ℤ
h : n ≥ m
ih :
  ∀ (k : ℤ),
    k < n →
      ∀ (hn : m ≤ k),
        Int.strongRec (motive := fun (x : ℤ) ↦ P x) lt ge k =
          ge k hn fun (k_1 : ℤ) (x : k_1 < k) ↦ Int.strongRec (motive := fun (x : ℤ) ↦ P x) lt ge k_1
hn : m ≤ n
⊢ ge n ⋯
      (Int.inductionOn' (motive := fun (x : ℤ) ↦ (k : ℤ) → k < x → P k) n m lt
        (fun (_n : ℤ) (a : m ≤ _n) (ih : (k : ℤ) → k < _n → P k) (l : ℤ) (a_1 : l < _n + 1) ↦
          if hlm : l < m then lt l hlm else ge l ⋯ fun (k : ℤ) (x : k < l) ↦ ih k ⋯)
        fun (n : ℤ) (x : n ≤ m) (hn : (k : ℤ) → k < n → P k) (l : ℤ) (x_1 : l < n - 1) ↦ hn l ⋯) =
    ge n hn fun (k : ℤ) (x : k < n) ↦ Int.strongRec (motive := fun (x : ℤ) ↦ P x) lt ge k
have e_a : Eq.{u_1} (α := (k : ℤ) → k < n → P k)
  (Int.inductionOn' (motive := fun (x : ℤ) ↦ (k : ℤ) → k < x → P k) n m lt
      (fun (_n : ℤ) (a : m ≤ _n) (ih : (k : ℤ) → k < _n → P k) (l : ℤ) (a_1 : l < _n + 1) ↦
        if hlm : l < m then lt l hlm else ge l sorry fun (k : ℤ) (x : k < l) ↦ ih k sorry)
      fun (n : ℤ) (x : n ≤ m) (hn : (k : ℤ) → k < n → P k) (l : ℤ) (x_1 : l < n - 1) ↦ hn l sorry :
    (k : ℤ) → k < n → P k)
  fun (k : ℤ) (x : k < n) ↦ Int.strongRec (motive := fun (x : ℤ) ↦ P x) lt ge k
Tactic: congr
-- Lean 4 proof step from Mathlib.Data.Int.Basic (goal)
Goal:
m n_1 : ℤ
P : ℤ → Sort u_1
lt : (n : ℤ) → n < m → P n
ge : (n : ℤ) → n ≥ m → ((k : ℤ) → k < n → P k) → P n
n : ℤ
h : n ≥ m
ih :
  ∀ (k : ℤ),
    k < n →
      ∀ (hn : m ≤ k),
        Int.strongRec (motive := fun (x : ℤ) ↦ P x) lt ge k =
          ge k hn fun (k_1 : ℤ) (x : k_1 < k) ↦ Int.strongRec (motive := fun (x : ℤ) ↦ P x) lt ge k_1
hn : m ≤ n
⊢ Eq.{u_1} (α := (k : ℤ) → k < n → P k)
    (Int.inductionOn' (motive := fun (x : ℤ) ↦ (k : ℤ) → k < x → P k) n m lt
        (fun (_n : ℤ) (a : m ≤ _n) (ih : (k : ℤ) → k < _n → P k) (l : ℤ) (a_1 : l < _n + 1) ↦
          if hlm : l < m then lt l hlm else ge l ⋯ fun (k : ℤ) (x : k < l) ↦ ih k ⋯)
        fun (n : ℤ) (x : n ≤ m) (hn : (k : ℤ) → k < n → P k) (l : ℤ) (x_1 : l < n - 1) ↦ hn l ⋯ :
      (k : ℤ) → k < n → P k)
    fun (k : ℤ) (x : k < n) ↦ Int.strongRec (motive := fun (x : ℤ) ↦ P x) lt ge k
have e_a : ∀
  (ih :
    ∀ (k : ℤ),
      k < n →
        ∀ (hn : m ≤ k),
          Int.strongRec (motive := fun (x : ℤ) ↦ P x) lt ge k =
            ge k hn fun (k_1 : ℤ) (x : k_1 < k) ↦ Int.strongRec (motive := fun (x : ℤ) ↦ P x) lt ge k_1),
  Eq.{u_1} (α := (k : ℤ) → k < n → P k)
    (Int.inductionOn' (motive := fun (x : ℤ) ↦ (k : ℤ) → k < x → P k) n m lt
        (fun (_n : ℤ) (a : m ≤ _n) (ih : (k : ℤ) → k < _n → P k) (l : ℤ) (a_1 : l < _n + 1) ↦
          if hlm : l < m then lt l hlm else ge l sorry fun (k : ℤ) (x : k < l) ↦ ih k sorry)
        fun (n : ℤ) (x : n ≤ m) (hn : (k : ℤ) → k < n → P k) (l : ℤ) (x_1 : l < n - 1) ↦ hn l sorry :
      (k : ℤ) → k < n → P k)
    fun (k : ℤ) (x : k < n) ↦ Int.strongRec (motive := fun (x : ℤ) ↦ P x) lt ge k
Tactic: revert ih
Cleared hypotheses: ih
-- Lean 4 proof step from Mathlib.Data.Int.Basic (goal)
Goal:
m n_1 : ℤ
P : ℤ → Sort u_1
lt : (n : ℤ) → n < m → P n
ge : (n : ℤ) → n ≥ m → ((k : ℤ) → k < n → P k) → P n
n : ℤ
h : n ≥ m
hn : m ≤ n
⊢ ∀
    (ih :
      ∀ (k : ℤ),
        k < n →
          ∀ (hn : m ≤ k),
            Int.strongRec (motive := fun (x : ℤ) ↦ P x) lt ge k =
              ge k hn fun (k_1 : ℤ) (x : k_1 < k) ↦ Int.strongRec (motive := fun (x : ℤ) ↦ P x) lt ge k_1),
    Eq.{u_1} (α := (k : ℤ) → k < n → P k)
      (Int.inductionOn' (motive := fun (x : ℤ) ↦ (k : ℤ) → k < x → P k) n m lt
          (fun (_n : ℤ) (a : m ≤ _n) (ih : (k : ℤ) → k < _n → P k) (l : ℤ) (a_1 : l < _n + 1) ↦
            if hlm : l < m then lt l hlm else ge l ⋯ fun (k : ℤ) (x : k < l) ↦ ih k ⋯)
          fun (n : ℤ) (x : n ≤ m) (hn : (k : ℤ) → k < n → P k) (l : ℤ) (x_1 : l < n - 1) ↦ hn l ⋯ :
        (k : ℤ) → k < n → P k)
      fun (k : ℤ) (x : k < n) ↦ Int.strongRec (motive := fun (x : ℤ) ↦ P x) lt ge k
have e_a : (∀ (k : ℤ),
    k < m →
      ∀ (hn : m ≤ k),
        Int.strongRec (motive := fun (x : ℤ) ↦ P x) lt ge k =
          ge k hn fun (k_1 : ℤ) (x : k_1 < k) ↦ Int.strongRec (motive := fun (x : ℤ) ↦ P x) lt ge k_1) →
  Eq.{u_1} (α := (k : ℤ) → k < m → P k)
    (Int.inductionOn' (motive := fun (x : ℤ) ↦ (k : ℤ) → k < x → P k) m m lt
        (fun (_n : ℤ) (a : m ≤ _n) (ih : (k : ℤ) → k < _n → P k) (l : ℤ) (a_1 : l < _n + 1) ↦
          if hlm : l < m then lt l hlm else ge l sorry fun (k : ℤ) (x : k < l) ↦ ih k sorry)
        fun (n : ℤ) (x : n ≤ m) (hn : (k : ℤ) → k < n → P k) (l : ℤ) (x_1 : l < n - 1) ↦ hn l sorry :
      (k : ℤ) → k < m → P k)
    fun (k : ℤ) (x : k < m) ↦ Int.strongRec (motive := fun (x : ℤ) ↦ P x) lt ge k
Tactic: refine n.inductionOn' m (fun _ ↦ ?_) (fun k hmk ih' ih ↦ ?_) (fun k hkm ih' _ ↦ ?_)
-- Lean 4 proof step from Mathlib.Data.Int.Basic (goal)
Goal:
m n_1 : ℤ
P : ℤ → Sort u_1
lt : (n : ℤ) → n < m → P n
ge : (n : ℤ) → n ≥ m → ((k : ℤ) → k < n → P k) → P n
n : ℤ
h : n ≥ m
hn : m ≤ n
h_1 :
  ∀ (k : ℤ),
    k < m →
      ∀ (hn : m ≤ k),
        Int.strongRec (motive := fun (x : ℤ) ↦ P x) lt ge k =
          ge k hn fun (k_1 : ℤ) (x : k_1 < k) ↦ Int.strongRec (motive := fun (x : ℤ) ↦ P x) lt ge k_1
⊢ Eq.{u_1} (α := (k : ℤ) → k < m → P k)
    (Int.inductionOn' (motive := fun (x : ℤ) ↦ (k : ℤ) → k < x → P k) m m lt
        (fun (_n : ℤ) (a : m ≤ _n) (ih : (k : ℤ) → k < _n → P k) (l : ℤ) (a_1 : l < _n + 1) ↦
          if hlm : l < m then lt l hlm else ge l ⋯ fun (k : ℤ) (x : k < l) ↦ ih k ⋯)
        fun (n : ℤ) (x : n ≤ m) (hn : (k : ℤ) → k < n → P k) (l : ℤ) (x_1 : l < n - 1) ↦ hn l ⋯ :
      (k : ℤ) → k < m → P k)
    fun (k : ℤ) (x : k < m) ↦ Int.strongRec (motive := fun (x : ℤ) ↦ P x) lt ge k
have e_a : ∀ (l : ℤ) (hl : l < m),
  Int.inductionOn' (motive := fun (x : ℤ) ↦ (k : ℤ) → k < x → P k) m m lt
      (fun (_n : ℤ) (a : m ≤ _n) (ih : (k : ℤ) → k < _n → P k) (l : ℤ) (a_1 : l < _n + 1) ↦
        if hlm : l < m then lt l hlm else ge l sorry fun (k : ℤ) (x : k < l) ↦ ih k sorry)
      (fun (n : ℤ) (x : n ≤ m) (hn : (k : ℤ) → k < n → P k) (l : ℤ) (x_1 : l < n - 1) ↦ hn l sorry) l hl =
    Int.strongRec (motive := fun (x : ℤ) ↦ P x) lt ge l
Tactic: ext l hl
-- Lean 4 proof step from Mathlib.Data.Int.Basic (goal)
Goal:
m n_1 : ℤ
P : ℤ → Sort u_1
lt : (n : ℤ) → n < m → P n
ge : (n : ℤ) → n ≥ m → ((k : ℤ) → k < n → P k) → P n
n : ℤ
h : n ≥ m
hn : m ≤ n
k : ℤ
hmk : m ≤ k
ih' :
  ∀
    (ih :
      ∀ (k_1 : ℤ),
        k_1 < k →
          ∀ (hn : m ≤ k_1),
            Int.strongRec (motive := fun (x : ℤ) ↦ P x) lt ge k_1 =
              ge k_1 hn fun (k : ℤ) (x : k < k_1) ↦ Int.strongRec (motive := fun (x : ℤ) ↦ P x) lt ge k),
    Eq.{u_1} (α := (k_1 : ℤ) → k_1 < k → P k_1)
      (Int.inductionOn' (motive := fun (x : ℤ) ↦ (k : ℤ) → k < x → P k) k m lt
          (fun (_n : ℤ) (a : m ≤ _n) (ih : (k : ℤ) → k < _n → P k) (l : ℤ) (a_1 : l < _n + 1) ↦
            if hlm : l < m then lt l hlm else ge l ⋯ fun (k : ℤ) (x : k < l) ↦ ih k ⋯)
          fun (n : ℤ) (x : n ≤ m) (hn : (k : ℤ) → k < n → P k) (l : ℤ) (x_1 : l < n - 1) ↦ hn l ⋯ :
        (k_1 : ℤ) → k_1 < k → P k_1)
      fun (k_1 : ℤ) (x : k_1 < k) ↦ Int.strongRec (motive := fun (x : ℤ) ↦ P x) lt ge k_1
ih :
  ∀ (k_1 : ℤ),
    k_1 < k + 1 →
      ∀ (hn : m ≤ k_1),
        Int.strongRec (motive := fun (x : ℤ) ↦ P x) lt ge k_1 =
          ge k_1 hn fun (k : ℤ) (x : k < k_1) ↦ Int.strongRec (motive := fun (x : ℤ) ↦ P x) lt ge k
⊢ Eq.{u_1} (α := (k_1 : ℤ) → k_1 < k + 1 → P k_1)
    (Int.inductionOn' (motive := fun (x : ℤ) ↦ (k : ℤ) → k < x → P k) (k + 1) m lt
        (fun (_n : ℤ) (a : m ≤ _n) (ih : (k : ℤ) → k < _n → P k) (l : ℤ) (a_1 : l < _n + 1) ↦
          if hlm : l < m then lt l hlm else ge l ⋯ fun (k : ℤ) (x : k < l) ↦ ih k ⋯)
        fun (n : ℤ) (x : n ≤ m) (hn : (k : ℤ) → k < n → P k) (l : ℤ) (x_1 : l < n - 1) ↦ hn l ⋯ :
      (k_1 : ℤ) → k_1 < k + 1 → P k_1)
    fun (k_1 : ℤ) (x : k_1 < k + 1) ↦ Int.strongRec (motive := fun (x : ℤ) ↦ P x) lt ge k_1
have e_a : ∀ (l : ℤ) (hl : l < k + 1),
  Int.inductionOn' (motive := fun (x : ℤ) ↦ (k : ℤ) → k < x → P k) (k + 1) m lt
      (fun (_n : ℤ) (a : m ≤ _n) (ih : (k : ℤ) → k < _n → P k) (l : ℤ) (a_1 : l < _n + 1) ↦
        if hlm : l < m then lt l hlm else ge l sorry fun (k : ℤ) (x : k < l) ↦ ih k sorry)
      (fun (n : ℤ) (x : n ≤ m) (hn : (k : ℤ) → k < n → P k) (l : ℤ) (x_1 : l < n - 1) ↦ hn l sorry) l hl =
    Int.strongRec (motive := fun (x : ℤ) ↦ P x) lt ge l
Tactic: ext l hl
-- Lean 4 proof step from Mathlib.Data.Int.Basic (goal)
Goal:
m n_1 : ℤ
P : ℤ → Sort u_1
lt : (n : ℤ) → n < m → P n
ge : (n : ℤ) → n ≥ m → ((k : ℤ) → k < n → P k) → P n
n : ℤ
h : n ≥ m
hn : m ≤ n
k : ℤ
hkm : k ≤ m
ih' :
  ∀
    (ih :
      ∀ (k_1 : ℤ),
        k_1 < k →
          ∀ (hn : m ≤ k_1),
            Int.strongRec (motive := fun (x : ℤ) ↦ P x) lt ge k_1 =
              ge k_1 hn fun (k : ℤ) (x : k < k_1) ↦ Int.strongRec (motive := fun (x : ℤ) ↦ P x) lt ge k),
    Eq.{u_1} (α := (k_1 : ℤ) → k_1 < k → P k_1)
      (Int.inductionOn' (motive := fun (x : ℤ) ↦ (k : ℤ) → k < x → P k) k m lt
          (fun (_n : ℤ) (a : m ≤ _n) (ih : (k : ℤ) → k < _n → P k) (l : ℤ) (a_1 : l < _n + 1) ↦
            if hlm : l < m then lt l hlm else ge l ⋯ fun (k : ℤ) (x : k < l) ↦ ih k ⋯)
          fun (n : ℤ) (x : n ≤ m) (hn : (k : ℤ) → k < n → P k) (l : ℤ) (x_1 : l < n - 1) ↦ hn l ⋯ :
        (k_1 : ℤ) → k_1 < k → P k_1)
      fun (k_1 : ℤ) (x : k_1 < k) ↦ Int.strongRec (motive := fun (x : ℤ) ↦ P x) lt ge k_1
h_1 :
  ∀ (k_1 : ℤ),
    k_1 < k - 1 →
      ∀ (hn : m ≤ k_1),
        Int.strongRec (motive := fun (x : ℤ) ↦ P x) lt ge k_1 =
          ge k_1 hn fun (k : ℤ) (x : k < k_1) ↦ Int.strongRec (motive := fun (x : ℤ) ↦ P x) lt ge k
⊢ Eq.{u_1} (α := (k_1 : ℤ) → k_1 < k - 1 → P k_1)
    (Int.inductionOn' (motive := fun (x : ℤ) ↦ (k : ℤ) → k < x → P k) (k - 1) m lt
        (fun (_n : ℤ) (a : m ≤ _n) (ih : (k : ℤ) → k < _n → P k) (l : ℤ) (a_1 : l < _n + 1) ↦
          if hlm : l < m then lt l hlm else ge l ⋯ fun (k : ℤ) (x : k < l) ↦ ih k ⋯)
        fun (n : ℤ) (x : n ≤ m) (hn : (k : ℤ) → k < n → P k) (l : ℤ) (x_1 : l < n - 1) ↦ hn l ⋯ :
      (k_1 : ℤ) → k_1 < k - 1 → P k_1)
    fun (k_1 : ℤ) (x : k_1 < k - 1) ↦ Int.strongRec (motive := fun (x : ℤ) ↦ P x) lt ge k_1
have e_a : ∀ (l : ℤ) (hl : l < k - 1),
  Int.inductionOn' (motive := fun (x : ℤ) ↦ (k : ℤ) → k < x → P k) (k - 1) m lt
      (fun (_n : ℤ) (a : m ≤ _n) (ih : (k : ℤ) → k < _n → P k) (l : ℤ) (a_1 : l < _n + 1) ↦
        if hlm : l < m then lt l hlm else ge l sorry fun (k : ℤ) (x : k < l) ↦ ih k sorry)
      (fun (n : ℤ) (x : n ≤ m) (hn : (k : ℤ) → k < n → P k) (l : ℤ) (x_1 : l < n - 1) ↦ hn l sorry) l hl =
    Int.strongRec (motive := fun (x : ℤ) ↦ P x) lt ge l
Tactic: ext l hl