awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Holor
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 : ℕ) ⋯)
⊢ (d :: ds).prod = (Finset.range d).card * ds.prod

Tactic:
simp [Finset.card_range]

Premises used: Finset.card_range
-- Module: Mathlib.Data.Holor
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 : ℕ) ⋯)
⊢ (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]
-- Module: Mathlib.Data.Holor
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 (α := α) ((Finset.range d).attach.card * ds.prod) (ds := [d] ++ ds)
    (∑ i ∈ (Finset.range d).attach, unitVec d (↑i : ℕ) ⊗ x.slice (↑i : ℕ) ⋯)

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
-- Module: Mathlib.Data.Holor
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 : ℕ) ⋯)
rwa rwa₁ rwa₂ rwa₃ :
  ∀
    (this :
      CPRankMax (α := α) ((Finset.range d).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 : ℕ) ⋯)
⊢ CPRankMax (α := α) ((Finset.range d).card * ds.prod) (ds := [d] ++ ds)
    (∑ i ∈ (Finset.range d).attach, unitVec d (↑i : ℕ) ⊗ x.slice (↑i : ℕ) ⋯)

Tactic:
rwa [Finset.card_attach] at this

Premises used: Finset.card_attach
-- Module: Mathlib.Data.Holor
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 : ℕ) ⋯)

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
-- Module: Mathlib.Data.Holor
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 : ℕ) ⋯)
rw :
  CPRankMax (α := α) (d :: ds).prod (ds := d :: ds)
    (∑ i ∈ (Finset.range d).attach, unitVec d (↑i : ℕ) ⊗ x.slice (↑i : ℕ) ⋯)
⊢ CPRankMax (d :: ds).prod x

Tactic:
rw [← sum_unitVec_mul_slice x]

Premises used: Holor.sum_unitVec_mul_slice
-- Module: Mathlib.Data.Holor
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 : ℕ) ⋯)
rw :
  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 : ℕ) ⋯)

Tactic:
rw [h_dds_prod]
-- Module: Mathlib.Data.Holor
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 (α := α) ((Finset.range d).card * ds.prod) (ds := d :: ds)
    (∑ i ∈ (Finset.range d).attach, unitVec d (↑i : ℕ) ⊗ x.slice (↑i : ℕ) ⋯)

Tactic:
h_cprankMax_sum

Premises used: List.append
-- Module: Mathlib.Data.Holor
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 (α := α) ((Finset.range d).card * ds.prod) (ds := d :: ds)
    (∑ i ∈ (Finset.range d).attach, unitVec d (↑i : ℕ) ⊗ x.slice (↑i : ℕ) ⋯)

Tactic:
exact h_cprankMax_sum
-- Module: Mathlib.Data.Holor
Goal:
α : Type
inst : Ring α
⊢ ∀ {ds : List ℕ} (x : Holor α ds), x.cprank ≤ ds.prod

Tactic:
fun {ds} x =>
  letI := Classical.decPred fun n : ℕ => CPRankMax n x
  Nat.find_min' ⟨ds.prod, show (fun n => CPRankMax n x) ds.prod from cprankMax_upper_bound x⟩
    (cprankMax_upper_bound x)

Premises used: Holor.cprankMax_upper_bound, Holor.cprank, Classical.decPred, Holor.CPRankMax, Nat.find_min', Exists.intro, List.prod
-- Module: Mathlib.Data.Int.AbsoluteValue
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)
inr : Eq (α := S) ((abv : (a : ℤ) → S) (↑(-1) : ℤ) : S) (1 : S)
⊢ Eq (α := S) ((abv : (a : ℤ) → S) (↑x : ℤ) : S) (1 : S)

Tactic:
rcases Int.units_eq_one_or x with (rfl | rfl)

Premises used: Int.units_eq_one_or, rfl
-- Module: Mathlib.Data.Int.AbsoluteValue
Goal:
S : Type u_2
inst : CommRing S
inst_1 : LinearOrder S
inst_2 : IsStrictOrderedRing S
abv : AbsoluteValue ℤ S
⊢ Eq (α := S) ((abv : (a : ℤ) → S) (↑1 : ℤ) : S) (1 : S)

Tactic:
simp
-- Module: Mathlib.Data.Int.AbsoluteValue
Goal:
S : Type u_2
inst : CommRing S
inst_1 : LinearOrder S
inst_2 : IsStrictOrderedRing S
abv : AbsoluteValue ℤ S
⊢ Eq (α := S) ((abv : (a : ℤ) → S) (↑(-1) : ℤ) : S) (1 : S)

Tactic:
simp
-- Module: Mathlib.Data.Int.AbsoluteValue
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)
inr : 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)

Tactic:
rcases Int.units_eq_one_or x with (rfl | rfl)

Premises used: Int.units_eq_one_or, rfl
-- Module: Mathlib.Data.Int.AbsoluteValue
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
⊢ Eq.{u_2 + 1} (α := S) ((abv : (a : R) → S) (↑(↑1 : ℤ) : R) : S) (1 : S)

Tactic:
simp
-- Module: Mathlib.Data.Int.AbsoluteValue
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
⊢ Eq.{u_2 + 1} (α := S) ((abv : (a : R) → S) (↑(↑(-1) : ℤ) : R) : S) (1 : S)

Tactic:
simp
-- Module: Mathlib.Data.Int.AbsoluteValue
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)
inr : 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)

Tactic:
rcases Int.units_eq_one_or x with (rfl | rfl)

Premises used: Int.units_eq_one_or, rfl
-- Module: Mathlib.Data.Int.AbsoluteValue
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
y : R
⊢ Eq.{u_2 + 1} (α := S) ((abv : (a : R) → S) (HSMul.hSMul (α := ℤˣ) 1 y) : S) ((abv : (a : R) → S) y : S)

Tactic:
simp
-- Module: Mathlib.Data.Int.AbsoluteValue
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
y : R
⊢ Eq.{u_2 + 1} (α := S) ((abv : (a : R) → S) (HSMul.hSMul (α := ℤˣ) (-1) y) : S) ((abv : (a : R) → S) y : S)

Tactic:
simp
-- Module: Mathlib.Data.Int.Associated
Goal:
a b : ℤ
⊢ a.natAbs = b.natAbs ↔ Associated a b

Tactic:
Int.natAbs_eq_natAbs_iff.trans ?_

Premises used: Int.natAbs_eq_natAbs_iff, Iff.trans
-- Module: Mathlib.Data.Int.Associated
Goal:
a b : ℤ
refine : a = b ∨ a = -b ↔ Associated a b
⊢ a.natAbs = b.natAbs ↔ Associated a b

Tactic:
refine Int.natAbs_eq_natAbs_iff.trans ?_

Premises used: Int.natAbs_eq_natAbs_iff, Iff.trans
-- Module: Mathlib.Data.Int.Associated
Goal:
a b : ℤ
mp : a = b ∨ a = -b → Associated a b
mpr : Associated a b → a = b ∨ a = -b
⊢ a = b ∨ a = -b ↔ Associated a b

Tactic:
constructor
-- Module: Mathlib.Data.Int.Associated
Goal:
a : ℤ
⊢ Associated a a

Tactic:
rfl
-- Module: Mathlib.Data.Int.Associated
Goal:
b : ℤ
⊢ -b * (↑(-1) : ℤ) = b

Tactic:
simp
-- Module: Mathlib.Data.Int.Associated
Goal:
b : ℤ
⊢ Associated (-b) b

Tactic:
exact ⟨-1, by simp⟩
-- Module: Mathlib.Data.Int.Associated
Goal:
a : ℤ
u : ℤˣ
mpr : a = a * (↑1 : ℤ) ∨ a = -(a * (↑1 : ℤ))
mpr₁ : a = a * (↑(-1) : ℤ) ∨ a = -(a * (↑(-1) : ℤ))
⊢ a = a * (↑u : ℤ) ∨ a = -(a * (↑u : ℤ))

Tactic:
obtain rfl | rfl := Int.units_eq_one_or u

Premises used: Int.units_eq_one_or, rfl
-- Module: Mathlib.Data.Int.Associated
Goal:
a : ℤ
⊢ a = a * (↑1 : ℤ)

Tactic:
simp
-- Module: Mathlib.Data.Int.Associated
Goal:
a : ℤ
⊢ a = a * (↑1 : ℤ) ∨ a = -(a * (↑1 : ℤ))

Tactic:
exact Or.inl (by simp)

Premises used: Or.inl
-- Module: Mathlib.Data.Int.Associated
Goal:
a : ℤ
⊢ a = -(a * (↑(-1) : ℤ))

Tactic:
simp
-- Module: Mathlib.Data.Int.Associated
Goal:
a : ℤ
⊢ a = a * (↑(-1) : ℤ) ∨ a = -(a * (↑(-1) : ℤ))

Tactic:
exact Or.inr (by simp)

Premises used: Or.inr
-- Module: Mathlib.Data.Int.Basic
Goal:
a b c d m n : ℤ
⊢ Nontrivial ℤ

Tactic:
⟨⟨0, 1, Int.zero_ne_one⟩⟩

Premises used: Int.zero_ne_one, Nontrivial.mk, Exists.intro, OfNat.ofNat
-- Module: Mathlib.Data.Int.Basic
Goal:
⊢ Function.Injective ofNat

Tactic:
@Int.ofNat.inj

Premises used: Int.ofNat.inj, Function.Injective
-- Module: Mathlib.Data.Int.Basic
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

Tactic:
m.strongRec (fun n hnm hmn ↦ (Int.not_lt.mpr hmn hnm).elim) (fun n _ ih hn ↦ ?_) n

Premises used: Int.strongRec
-- Module: Mathlib.Data.Int.Basic
Goal:
m n : ℤ
P : ℤ → Sort u_1
lt : (n : ℤ) → n < m → P n
ge : (n : ℤ) → n ≥ m → ((k : ℤ) → k < n → P k) → P n
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
⊢ ∀ (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
-- Module: Mathlib.Data.Int.Basic
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
rw :
  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
⊢ 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:
rw [Int.strongRec, dif_neg (Int.not_lt.mpr hn)]

Premises used: Iff.mpr, dif_neg, Int.not_lt
-- Module: Mathlib.Data.Int.Basic
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
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 ⋯ 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
⊢ 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

Tactic:
congr
-- Module: Mathlib.Data.Int.Basic
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
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 ⋯ 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
⊢ 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

Tactic:
revert ih
-- Module: Mathlib.Data.Int.Basic
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

Tactic:
n.inductionOn' m (fun _ ↦ ?_) (fun k hmk ih' ih ↦ ?_) (fun k hkm ih' _ ↦ ?_)

Premises used: Int.inductionOn'
-- Module: Mathlib.Data.Int.Basic
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
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 ⋯ 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 ⋯) l hl =
      Int.strongRec (motive := fun (x : ℤ) ↦ P x) lt ge l
⊢ 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

Tactic:
ext l hl
-- Module: Mathlib.Data.Int.Basic
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
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 ⋯ 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 ⋯) l hl =
      Int.strongRec (motive := fun (x : ℤ) ↦ P x) lt ge l
⊢ 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

Tactic:
ext l hl