awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.Divisors (goal)
Goal:
α : Type u_1
inst : CommMonoid α
n : ℕ
f : ℕ → α
pos : ∀ (hn : n = 0), ∏ d ∈ n.divisors, f (n / d) = n.divisors.prod f
⊢ ∏ d ∈ n.divisors, f (n / d) = n.divisors.prod f
have neg : ∀ (hn : ¬n = 0), ∏ d ∈ n.divisors, f (n / d) = n.divisors.prod f
Tactic: by_cases hn : n = 0
-- Lean 4 proof step from Mathlib.NumberTheory.Divisors (goal)
Goal:
α : Type u_1
inst : CommMonoid α
n : ℕ
f : ℕ → α
hn : ¬n = 0
⊢ ∏ d ∈ n.divisors, f (n / d) = n.divisors.prod f
have neg : ∏ x ∈ image (HDiv.hDiv n) n.divisors, f x = n.divisors.prod f
Tactic: rw [← prod_image]
-- Lean 4 proof step from Mathlib.NumberTheory.Divisors (goal)
Goal:
α : Type u_1
inst : CommMonoid α
n : ℕ
f : ℕ → α
hn : ¬n = 0
neg : ∏ x ∈ image (HDiv.hDiv n) n.divisors, f x = n.divisors.prod f
⊢ ∏ d ∈ n.divisors, f (n / d) = n.divisors.prod f
have neg₁ : Set.InjOn (HDiv.hDiv n) (↑n.divisors : Set ℕ)
Tactic: rw [← prod_image]
-- Lean 4 proof step from Mathlib.NumberTheory.Divisors (goal)
Goal:
α : Type u_1
inst : CommMonoid α
n : ℕ
f : ℕ → α
hn : ¬n = 0
x : ℕ
hx : x ∈ (↑n.divisors : Set ℕ)
y : ℕ
hy : y ∈ (↑n.divisors : Set ℕ)
h : n / x = n / y
⊢ x = y
have neg : ∀ (hx : x ∣ n ∧ n ≠ 0) ⦃y : ℕ⦄ (hy : y ∣ n ∧ n ≠ 0) (h : n / x = n / y), x = y
Tactic: rw [mem_coe, mem_divisors] at hx hy
Cleared hypotheses: hx, y, hy, h
-- Lean 4 proof step from Mathlib.NumberTheory.Divisors (goal)
Goal:
a b : ℕ
hab : a.Coprime b
⊢ Disjoint (filter IsPrimePow a.divisors) (filter IsPrimePow b.divisors)
have simp : ∀ ⦃a_1 : ℕ⦄, a_1 ∣ a → a ≠ 0 → IsPrimePow a_1 → a_1 ∣ b → b ≠ 0 → ¬IsPrimePow a_1
Tactic: simp only [Finset.disjoint_left, Finset.mem_filter, and_imp, Nat.mem_divisors, not_and]
-- Lean 4 proof step from Mathlib.NumberTheory.Divisors (goal)
Goal:
n N : ℕ
n_ne_zero : n ≠ 0
hn : n ≤ N
⊢ n.divisorsAntidiagonal = {x ∈ Ioc 0 N ×ˢ Ioc 0 N | x.1 * x.2 = n}
have h : ∀ (n1 n2 : ℕ), (n1, n2) ∈ n.divisorsAntidiagonal ↔ (n1, n2) ∈ {x ∈ Ioc 0 N ×ˢ Ioc 0 N | x.1 * x.2 = n}
Tactic: ext ⟨n1, n2⟩
-- Lean 4 proof step from Mathlib.NumberTheory.Divisors (goal)
Goal:
n N : ℕ
n_ne_zero : n ≠ 0
hn : n ≤ N
n1 n2 : ℕ
⊢ (n1, n2) ∈ n.divisorsAntidiagonal ↔ (n1, n2) ∈ {x ∈ Ioc 0 N ×ˢ Ioc 0 N | x.1 * x.2 = n}
have h : (n1, n2).1 * (n1, n2).2 = n ∧ n ≠ 0 ↔ (n1, n2) ∈ {x ∈ Ioc 0 N ×ˢ Ioc 0 N | x.1 * x.2 = n}
Tactic: rw [Nat.mem_divisorsAntidiagonal]
-- Lean 4 proof step from Mathlib.NumberTheory.Divisors (goal)
Goal:
n N : ℕ
n_ne_zero : n ≠ 0
hn : n ≤ N
n1 n2 : ℕ
⊢ (n1, n2).1 * (n1, n2).2 = n ∧ n ≠ 0 ↔ (n1, n2) ∈ {x ∈ Ioc 0 N ×ˢ Ioc 0 N | x.1 * x.2 = n}
have h : n1 * n2 = n ∧ ¬n = 0 ↔ ((0 < n1 ∧ n1 ≤ N) ∧ 0 < n2 ∧ n2 ≤ N) ∧ n1 * n2 = n
Tactic: simp only [ne_eq, Finset.mem_filter, Finset.mem_product, Finset.mem_Ioc]
-- Lean 4 proof step from Mathlib.NumberTheory.Divisors (goal)
Goal:
n N : ℕ
n_ne_zero : n ≠ 0
hn : n ≤ N
n1 n2 : ℕ
⊢ n1 * n2 = n ∧ ¬n = 0 ↔ ((0 < n1 ∧ n1 ≤ N) ∧ 0 < n2 ∧ n2 ≤ N) ∧ n1 * n2 = n
have h : n1 * n2 = n ∧ ¬n = 0 → ((0 < n1 ∧ n1 ≤ N) ∧ 0 < n2 ∧ n2 ≤ N) ∧ n1 * n2 = n
Tactic: constructor
-- Lean 4 proof step from Mathlib.NumberTheory.Divisors (goal)
Goal:
n N : ℕ
n_ne_zero : n ≠ 0
hn : n ≤ N
n1 n2 : ℕ
h : n1 * n2 = n ∧ ¬n = 0 → ((0 < n1 ∧ n1 ≤ N) ∧ 0 < n2 ∧ n2 ≤ N) ∧ n1 * n2 = n
⊢ n1 * n2 = n ∧ ¬n = 0 ↔ ((0 < n1 ∧ n1 ≤ N) ∧ 0 < n2 ∧ n2 ≤ N) ∧ n1 * n2 = n
have h₁ : ((0 < n1 ∧ n1 ≤ N) ∧ 0 < n2 ∧ n2 ≤ N) ∧ n1 * n2 = n → n1 * n2 = n ∧ ¬n = 0
Tactic: constructor
-- Lean 4 proof step from Mathlib.NumberTheory.Divisors (goal)
Goal:
n N n1 n2 : ℕ
hn2 : ¬n1 * n2 = 0
n_ne_zero : n1 * n2 ≠ 0
hn : n1 * n2 ≤ N
⊢ ((0 < n1 ∧ n1 ≤ N) ∧ 0 < n2 ∧ n2 ≤ N) ∧ n1 * n2 = n1 * n2
have h : ((0 < n1 ∧ n1 ≤ n1 * n2) ∧ 0 < n2 ∧ n2 ≤ n1 * n2) ∧ n1 * n2 = n1 * n2
Tactic: grw [← hn]
-- Lean 4 proof step from Mathlib.NumberTheory.Divisors (goal)
Goal:
n N n1 n2 : ℕ
hn2 : ¬n1 * n2 = 0
n_ne_zero : n1 * n2 ≠ 0
hn : n1 * n2 ≤ N
⊢ ((0 < n1 ∧ n1 ≤ n1 * n2) ∧ 0 < n2 ∧ n2 ≤ n1 * n2) ∧ n1 * n2 = n1 * n2
have h : (0 < n1 ∧ 1 ≤ n2) ∧ 0 < n2 ∧ 1 ≤ n1
Tactic: simp (disch := lia) only [le_mul_iff_one_le_right, le_mul_iff_one_le_left, and_true]
-- Lean 4 proof step from Mathlib.NumberTheory.Divisors (goal)
Goal:
q : ℕ
hq : 1 < q
k_1 : ℕ
k : ℕ × ℕ
hk :
  k ∈
    map
      ({ toFun := fun (k : ℕ) ↦ q ^ k, inj' := ⋯ : ℕ ↪ ℕ }.prodMap { toFun := fun (k : ℕ) ↦ q ^ k, inj' := ⋯ : ℕ ↪ ℕ })
      (@antidiagonal _ instAddMonoid _ k_1)
⊢ k ∈ (q ^ k_1).divisorsAntidiagonal
have obtain : ∀ (i : ℕ × ℕ) (hi : i ∈ @antidiagonal _ instAddMonoid _ k_1)
  (hk :
    Membership.mem (α := ℕ × ℕ)
      (map
        ({ toFun := fun (k : ℕ) ↦ q ^ k, inj' := sorry : ℕ ↪ ℕ }.prodMap
          { toFun := fun (k : ℕ) ↦ q ^ k, inj' := sorry : ℕ ↪ ℕ })
        (@antidiagonal _ instAddMonoid _ k_1))
      (({ toFun := fun (k : ℕ) ↦ q ^ k, inj' := sorry : ℕ ↪ ℕ }.prodMap
              { toFun := fun (k : ℕ) ↦ q ^ k, inj' := sorry : ℕ ↪ ℕ } :
            (a : ℕ × ℕ) → ℕ × ℕ)
          i :
        ℕ × ℕ)),
  Membership.mem (α := ℕ × ℕ) (q ^ k_1).divisorsAntidiagonal
    (({ toFun := fun (k : ℕ) ↦ q ^ k, inj' := sorry : ℕ ↪ ℕ }.prodMap { toFun := fun (k : ℕ) ↦ q ^ k, inj' := sorry : ℕ ↪ ℕ } :
          (a : ℕ × ℕ) → ℕ × ℕ)
        i :
      ℕ × ℕ)
Tactic: obtain ⟨i, hi, rfl⟩ := Finset.mem_map.mp hk
Cleared hypotheses: k, hk
-- Lean 4 proof step from Mathlib.NumberTheory.Divisors (goal)
Goal:
⊢ divisors 0 = ∅
have h : ∀ (a : ℤ), a ∈ divisors 0 ↔ Membership.mem (γ := Finset ℤ) ∅ a
Tactic: ext
-- Lean 4 proof step from Mathlib.NumberTheory.Divisors (goal)
Goal:
z : ℤ
⊢ z.divisors = ∅ ↔ z = 0
have contrapose! : z.divisors.Nonempty ↔ z ≠ 0
Tactic: contrapose!
-- Lean 4 proof step from Mathlib.NumberTheory.Divisors (goal)
Goal:
z : ℤ
⊢ (-z).divisors = z.divisors
have h : ∀ (a : ℤ), a ∈ (-z).divisors ↔ a ∈ z.divisors
Tactic: ext
-- Lean 4 proof step from Mathlib.NumberTheory.Divisors (goal)
Goal:
xy : ℤ × ℤ
z : ℤ
⊢ xy ∈ z.divisorsAntidiag ↔ xy.1 * xy.2 = z ∧ z ≠ 0
have ofNat : ∀ (a a_1 a_2 : ℕ),
  (ofNat a_1, ofNat a_2) ∈ (ofNat a).divisorsAntidiag ↔
    (ofNat a_1, ofNat a_2).1 * (ofNat a_1, ofNat a_2).2 = ofNat a ∧ ofNat a ≠ 0
Tactic: rcases z, xy with ⟨_ | _, ⟨_ | _, _ | _⟩⟩
Cleared hypotheses: xy, z
-- Lean 4 proof step from Mathlib.NumberTheory.Divisors (goal)
Goal:
xy : ℤ × ℤ
z : ℤ
ofNat :
  ∀ (a a_1 a_2 : ℕ),
    (Int.ofNat a_1, Int.ofNat a_2) ∈ (Int.ofNat a).divisorsAntidiag ↔
      (Int.ofNat a_1, Int.ofNat a_2).1 * (Int.ofNat a_1, Int.ofNat a_2).2 = Int.ofNat a ∧ Int.ofNat a ≠ 0
⊢ xy ∈ z.divisorsAntidiag ↔ xy.1 * xy.2 = z ∧ z ≠ 0
have ofNat₁ : ∀ (a a_1 a_2 : ℕ),
  (Int.ofNat a_1, -[a_2+1]) ∈ (Int.ofNat a).divisorsAntidiag ↔
    (Int.ofNat a_1, -[a_2+1]).1 * (Int.ofNat a_1, -[a_2+1]).2 = Int.ofNat a ∧ Int.ofNat a ≠ 0
Tactic: rcases z, xy with ⟨_ | _, ⟨_ | _, _ | _⟩⟩
Cleared hypotheses: xy, z
-- Lean 4 proof step from Mathlib.NumberTheory.Divisors (goal)
Goal:
xy : ℤ × ℤ
z : ℤ
ofNat :
  ∀ (a a_1 a_2 : ℕ),
    (Int.ofNat a_1, Int.ofNat a_2) ∈ (Int.ofNat a).divisorsAntidiag ↔
      (Int.ofNat a_1, Int.ofNat a_2).1 * (Int.ofNat a_1, Int.ofNat a_2).2 = Int.ofNat a ∧ Int.ofNat a ≠ 0
ofNat₁ :
  ∀ (a a_1 a_2 : ℕ),
    (Int.ofNat a_1, -[a_2+1]) ∈ (Int.ofNat a).divisorsAntidiag ↔
      (Int.ofNat a_1, -[a_2+1]).1 * (Int.ofNat a_1, -[a_2+1]).2 = Int.ofNat a ∧ Int.ofNat a ≠ 0
⊢ xy ∈ z.divisorsAntidiag ↔ xy.1 * xy.2 = z ∧ z ≠ 0
have ofNat₂ : ∀ (a a_1 a_2 : ℕ),
  (-[a_1+1], Int.ofNat a_2) ∈ (Int.ofNat a).divisorsAntidiag ↔
    (-[a_1+1], Int.ofNat a_2).1 * (-[a_1+1], Int.ofNat a_2).2 = Int.ofNat a ∧ Int.ofNat a ≠ 0
Tactic: rcases z, xy with ⟨_ | _, ⟨_ | _, _ | _⟩⟩
Cleared hypotheses: xy, z
-- Lean 4 proof step from Mathlib.NumberTheory.Divisors (goal)
Goal:
xy : ℤ × ℤ
z : ℤ
ofNat :
  ∀ (a a_1 a_2 : ℕ),
    (Int.ofNat a_1, Int.ofNat a_2) ∈ (Int.ofNat a).divisorsAntidiag ↔
      (Int.ofNat a_1, Int.ofNat a_2).1 * (Int.ofNat a_1, Int.ofNat a_2).2 = Int.ofNat a ∧ Int.ofNat a ≠ 0
ofNat₁ :
  ∀ (a a_1 a_2 : ℕ),
    (Int.ofNat a_1, -[a_2+1]) ∈ (Int.ofNat a).divisorsAntidiag ↔
      (Int.ofNat a_1, -[a_2+1]).1 * (Int.ofNat a_1, -[a_2+1]).2 = Int.ofNat a ∧ Int.ofNat a ≠ 0
ofNat₂ :
  ∀ (a a_1 a_2 : ℕ),
    (-[a_1+1], Int.ofNat a_2) ∈ (Int.ofNat a).divisorsAntidiag ↔
      (-[a_1+1], Int.ofNat a_2).1 * (-[a_1+1], Int.ofNat a_2).2 = Int.ofNat a ∧ Int.ofNat a ≠ 0
⊢ xy ∈ z.divisorsAntidiag ↔ xy.1 * xy.2 = z ∧ z ≠ 0
have rcases : ∀ (a a_1 a_2 : ℕ),
  (-[a_1+1], -[a_2+1]) ∈ (Int.ofNat a).divisorsAntidiag ↔
    (-[a_1+1], -[a_2+1]).1 * (-[a_1+1], -[a_2+1]).2 = Int.ofNat a ∧ Int.ofNat a ≠ 0
Tactic: rcases z, xy with ⟨_ | _, ⟨_ | _, _ | _⟩⟩
Cleared hypotheses: xy, z
-- Lean 4 proof step from Mathlib.NumberTheory.Divisors (goal)
Goal:
xy : ℤ × ℤ
z : ℤ
ofNat :
  ∀ (a a_1 a_2 : ℕ),
    (Int.ofNat a_1, Int.ofNat a_2) ∈ (Int.ofNat a).divisorsAntidiag ↔
      (Int.ofNat a_1, Int.ofNat a_2).1 * (Int.ofNat a_1, Int.ofNat a_2).2 = Int.ofNat a ∧ Int.ofNat a ≠ 0
ofNat₁ :
  ∀ (a a_1 a_2 : ℕ),
    (Int.ofNat a_1, -[a_2+1]) ∈ (Int.ofNat a).divisorsAntidiag ↔
      (Int.ofNat a_1, -[a_2+1]).1 * (Int.ofNat a_1, -[a_2+1]).2 = Int.ofNat a ∧ Int.ofNat a ≠ 0
ofNat₂ :
  ∀ (a a_1 a_2 : ℕ),
    (-[a_1+1], Int.ofNat a_2) ∈ (Int.ofNat a).divisorsAntidiag ↔
      (-[a_1+1], Int.ofNat a_2).1 * (-[a_1+1], Int.ofNat a_2).2 = Int.ofNat a ∧ Int.ofNat a ≠ 0
rcases :
  ∀ (a a_1 a_2 : ℕ),
    (-[a_1+1], -[a_2+1]) ∈ (Int.ofNat a).divisorsAntidiag ↔
      (-[a_1+1], -[a_2+1]).1 * (-[a_1+1], -[a_2+1]).2 = Int.ofNat a ∧ Int.ofNat a ≠ 0
⊢ xy ∈ z.divisorsAntidiag ↔ xy.1 * xy.2 = z ∧ z ≠ 0
have negSucc : ∀ (a a_1 a_2 : ℕ),
  (Int.ofNat a_1, Int.ofNat a_2) ∈ -[a+1].divisorsAntidiag ↔
    (Int.ofNat a_1, Int.ofNat a_2).1 * (Int.ofNat a_1, Int.ofNat a_2).2 = -[a+1] ∧ -[a+1] ≠ 0
Tactic: rcases z, xy with ⟨_ | _, ⟨_ | _, _ | _⟩⟩
Cleared hypotheses: xy, z
-- Lean 4 proof step from Mathlib.NumberTheory.Divisors (goal)
Goal:
xy : ℤ × ℤ
z : ℤ
ofNat :
  ∀ (a a_1 a_2 : ℕ),
    (Int.ofNat a_1, Int.ofNat a_2) ∈ (Int.ofNat a).divisorsAntidiag ↔
      (Int.ofNat a_1, Int.ofNat a_2).1 * (Int.ofNat a_1, Int.ofNat a_2).2 = Int.ofNat a ∧ Int.ofNat a ≠ 0
ofNat₁ :
  ∀ (a a_1 a_2 : ℕ),
    (Int.ofNat a_1, -[a_2+1]) ∈ (Int.ofNat a).divisorsAntidiag ↔
      (Int.ofNat a_1, -[a_2+1]).1 * (Int.ofNat a_1, -[a_2+1]).2 = Int.ofNat a ∧ Int.ofNat a ≠ 0
ofNat₂ :
  ∀ (a a_1 a_2 : ℕ),
    (-[a_1+1], Int.ofNat a_2) ∈ (Int.ofNat a).divisorsAntidiag ↔
      (-[a_1+1], Int.ofNat a_2).1 * (-[a_1+1], Int.ofNat a_2).2 = Int.ofNat a ∧ Int.ofNat a ≠ 0
rcases :
  ∀ (a a_1 a_2 : ℕ),
    (-[a_1+1], -[a_2+1]) ∈ (Int.ofNat a).divisorsAntidiag ↔
      (-[a_1+1], -[a_2+1]).1 * (-[a_1+1], -[a_2+1]).2 = Int.ofNat a ∧ Int.ofNat a ≠ 0
negSucc :
  ∀ (a a_1 a_2 : ℕ),
    (Int.ofNat a_1, Int.ofNat a_2) ∈ -[a+1].divisorsAntidiag ↔
      (Int.ofNat a_1, Int.ofNat a_2).1 * (Int.ofNat a_1, Int.ofNat a_2).2 = -[a+1] ∧ -[a+1] ≠ 0
⊢ xy ∈ z.divisorsAntidiag ↔ xy.1 * xy.2 = z ∧ z ≠ 0
have negSucc₁ : ∀ (a a_1 a_2 : ℕ),
  (Int.ofNat a_1, -[a_2+1]) ∈ -[a+1].divisorsAntidiag ↔
    (Int.ofNat a_1, -[a_2+1]).1 * (Int.ofNat a_1, -[a_2+1]).2 = -[a+1] ∧ -[a+1] ≠ 0
Tactic: rcases z, xy with ⟨_ | _, ⟨_ | _, _ | _⟩⟩
Cleared hypotheses: xy, z
-- Lean 4 proof step from Mathlib.NumberTheory.Divisors (goal)
Goal:
xy : ℤ × ℤ
z : ℤ
ofNat :
  ∀ (a a_1 a_2 : ℕ),
    (Int.ofNat a_1, Int.ofNat a_2) ∈ (Int.ofNat a).divisorsAntidiag ↔
      (Int.ofNat a_1, Int.ofNat a_2).1 * (Int.ofNat a_1, Int.ofNat a_2).2 = Int.ofNat a ∧ Int.ofNat a ≠ 0
ofNat₁ :
  ∀ (a a_1 a_2 : ℕ),
    (Int.ofNat a_1, -[a_2+1]) ∈ (Int.ofNat a).divisorsAntidiag ↔
      (Int.ofNat a_1, -[a_2+1]).1 * (Int.ofNat a_1, -[a_2+1]).2 = Int.ofNat a ∧ Int.ofNat a ≠ 0
ofNat₂ :
  ∀ (a a_1 a_2 : ℕ),
    (-[a_1+1], Int.ofNat a_2) ∈ (Int.ofNat a).divisorsAntidiag ↔
      (-[a_1+1], Int.ofNat a_2).1 * (-[a_1+1], Int.ofNat a_2).2 = Int.ofNat a ∧ Int.ofNat a ≠ 0
rcases :
  ∀ (a a_1 a_2 : ℕ),
    (-[a_1+1], -[a_2+1]) ∈ (Int.ofNat a).divisorsAntidiag ↔
      (-[a_1+1], -[a_2+1]).1 * (-[a_1+1], -[a_2+1]).2 = Int.ofNat a ∧ Int.ofNat a ≠ 0
negSucc :
  ∀ (a a_1 a_2 : ℕ),
    (Int.ofNat a_1, Int.ofNat a_2) ∈ -[a+1].divisorsAntidiag ↔
      (Int.ofNat a_1, Int.ofNat a_2).1 * (Int.ofNat a_1, Int.ofNat a_2).2 = -[a+1] ∧ -[a+1] ≠ 0
negSucc₁ :
  ∀ (a a_1 a_2 : ℕ),
    (Int.ofNat a_1, -[a_2+1]) ∈ -[a+1].divisorsAntidiag ↔
      (Int.ofNat a_1, -[a_2+1]).1 * (Int.ofNat a_1, -[a_2+1]).2 = -[a+1] ∧ -[a+1] ≠ 0
⊢ xy ∈ z.divisorsAntidiag ↔ xy.1 * xy.2 = z ∧ z ≠ 0
have negSucc₂ : ∀ (a a_1 a_2 : ℕ),
  (-[a_1+1], Int.ofNat a_2) ∈ -[a+1].divisorsAntidiag ↔
    (-[a_1+1], Int.ofNat a_2).1 * (-[a_1+1], Int.ofNat a_2).2 = -[a+1] ∧ -[a+1] ≠ 0
Tactic: rcases z, xy with ⟨_ | _, ⟨_ | _, _ | _⟩⟩
Cleared hypotheses: xy, z
-- Lean 4 proof step from Mathlib.NumberTheory.Divisors (goal)
Goal:
xy : ℤ × ℤ
z : ℤ
ofNat :
  ∀ (a a_1 a_2 : ℕ),
    (Int.ofNat a_1, Int.ofNat a_2) ∈ (Int.ofNat a).divisorsAntidiag ↔
      (Int.ofNat a_1, Int.ofNat a_2).1 * (Int.ofNat a_1, Int.ofNat a_2).2 = Int.ofNat a ∧ Int.ofNat a ≠ 0
ofNat₁ :
  ∀ (a a_1 a_2 : ℕ),
    (Int.ofNat a_1, -[a_2+1]) ∈ (Int.ofNat a).divisorsAntidiag ↔
      (Int.ofNat a_1, -[a_2+1]).1 * (Int.ofNat a_1, -[a_2+1]).2 = Int.ofNat a ∧ Int.ofNat a ≠ 0
ofNat₂ :
  ∀ (a a_1 a_2 : ℕ),
    (-[a_1+1], Int.ofNat a_2) ∈ (Int.ofNat a).divisorsAntidiag ↔
      (-[a_1+1], Int.ofNat a_2).1 * (-[a_1+1], Int.ofNat a_2).2 = Int.ofNat a ∧ Int.ofNat a ≠ 0
rcases :
  ∀ (a a_1 a_2 : ℕ),
    (-[a_1+1], -[a_2+1]) ∈ (Int.ofNat a).divisorsAntidiag ↔
      (-[a_1+1], -[a_2+1]).1 * (-[a_1+1], -[a_2+1]).2 = Int.ofNat a ∧ Int.ofNat a ≠ 0
negSucc :
  ∀ (a a_1 a_2 : ℕ),
    (Int.ofNat a_1, Int.ofNat a_2) ∈ -[a+1].divisorsAntidiag ↔
      (Int.ofNat a_1, Int.ofNat a_2).1 * (Int.ofNat a_1, Int.ofNat a_2).2 = -[a+1] ∧ -[a+1] ≠ 0
negSucc₁ :
  ∀ (a a_1 a_2 : ℕ),
    (Int.ofNat a_1, -[a_2+1]) ∈ -[a+1].divisorsAntidiag ↔
      (Int.ofNat a_1, -[a_2+1]).1 * (Int.ofNat a_1, -[a_2+1]).2 = -[a+1] ∧ -[a+1] ≠ 0
negSucc₂ :
  ∀ (a a_1 a_2 : ℕ),
    (-[a_1+1], Int.ofNat a_2) ∈ -[a+1].divisorsAntidiag ↔
      (-[a_1+1], Int.ofNat a_2).1 * (-[a_1+1], Int.ofNat a_2).2 = -[a+1] ∧ -[a+1] ≠ 0
⊢ xy ∈ z.divisorsAntidiag ↔ xy.1 * xy.2 = z ∧ z ≠ 0
have negSucc₃ : ∀ (a a_1 a_2 : ℕ),
  (-[a_1+1], -[a_2+1]) ∈ -[a+1].divisorsAntidiag ↔ (-[a_1+1], -[a_2+1]).1 * (-[a_1+1], -[a_2+1]).2 = -[a+1] ∧ -[a+1] ≠ 0
Tactic: rcases z, xy with ⟨_ | _, ⟨_ | _, _ | _⟩⟩
Cleared hypotheses: xy, z
-- Lean 4 proof step from Mathlib.NumberTheory.Divisors (goal)
Goal:
a a_1 a_2 : ℕ
⊢ (-[a_1+1], -[a_2+1]) ∈ (ofNat a).divisorsAntidiag ↔
    (-[a_1+1], -[a_2+1]).1 * (-[a_1+1], -[a_2+1]).2 = ofNat a ∧ ofNat a ≠ 0
have simp : ¬a = 0 → ((a_1 + 1) * (a_2 + 1) = a ↔ -[a_1+1] * -[a_2+1] = (↑a : ℤ))
Tactic: simp [divisorsAntidiag]
-- Lean 4 proof step from Mathlib.NumberTheory.Divisors (goal)
Goal:
a a_1 a_2 : ℕ
⊢ (ofNat a_1, ofNat a_2) ∈ (ofNat a).divisorsAntidiag ↔
    (ofNat a_1, ofNat a_2).1 * (ofNat a_1, ofNat a_2).2 = ofNat a ∧ ofNat a ≠ 0
have ofNat : a_1 * a_2 = a ∧ ¬a = 0 ∨ (0 = a ∧ ¬a = 0) ∧ a_1 = 0 ∧ a_2 = 0 ↔
  HMul.hMul (α := ℤ) (↑a_1 : ℤ) (↑a_2 : ℤ) = (↑a : ℤ) ∧ ¬a = 0
Tactic: simp [divisorsAntidiag]
-- Lean 4 proof step from Mathlib.NumberTheory.Divisors (goal)
Goal:
a a_1 a_2 : ℕ
⊢ (ofNat a_1, -[a_2+1]) ∈ (ofNat a).divisorsAntidiag ↔
    (ofNat a_1, -[a_2+1]).1 * (ofNat a_1, -[a_2+1]).2 = ofNat a ∧ ofNat a ≠ 0
have ofNat : (0 = a ∧ ¬a = 0) ∧ a_1 = 0 ↔ (↑a_1 : ℤ) * -[a_2+1] = (↑a : ℤ) ∧ ¬a = 0
Tactic: simp [divisorsAntidiag]
-- Lean 4 proof step from Mathlib.NumberTheory.Divisors (goal)
Goal:
a a_1 a_2 : ℕ
⊢ (-[a_1+1], ofNat a_2) ∈ (ofNat a).divisorsAntidiag ↔
    (-[a_1+1], ofNat a_2).1 * (-[a_1+1], ofNat a_2).2 = ofNat a ∧ ofNat a ≠ 0
have ofNat : (0 = a ∧ ¬a = 0) ∧ a_2 = 0 ↔ -[a_1+1] * (↑a_2 : ℤ) = (↑a : ℤ) ∧ ¬a = 0
Tactic: simp [divisorsAntidiag]
-- Lean 4 proof step from Mathlib.NumberTheory.Divisors (goal)
Goal:
a a_1 a_2 : ℕ
⊢ (ofNat a_1, ofNat a_2) ∈ -[a+1].divisorsAntidiag ↔
    (ofNat a_1, ofNat a_2).1 * (ofNat a_1, ofNat a_2).2 = -[a+1] ∧ -[a+1] ≠ 0
have negSucc : ¬HMul.hMul (α := ℤ) (↑a_1 : ℤ) (↑a_2 : ℤ) = -[a+1]
Tactic: simp [divisorsAntidiag]
-- Lean 4 proof step from Mathlib.NumberTheory.Divisors (goal)
Goal:
a a_1 a_2 : ℕ
⊢ (ofNat a_1, -[a_2+1]) ∈ -[a+1].divisorsAntidiag ↔
    (ofNat a_1, -[a_2+1]).1 * (ofNat a_1, -[a_2+1]).2 = -[a+1] ∧ -[a+1] ≠ 0
have negSucc : a_1 * (a_2 + 1) = a + 1 ↔ (↑a_1 : ℤ) * -[a_2+1] = -[a+1]
Tactic: simp [divisorsAntidiag]
-- Lean 4 proof step from Mathlib.NumberTheory.Divisors (goal)
Goal:
a a_1 a_2 : ℕ
⊢ (-[a_1+1], ofNat a_2) ∈ -[a+1].divisorsAntidiag ↔
    (-[a_1+1], ofNat a_2).1 * (-[a_1+1], ofNat a_2).2 = -[a+1] ∧ -[a+1] ≠ 0
have negSucc : (a_1 + 1) * a_2 = a + 1 ↔ -[a_1+1] * (↑a_2 : ℤ) = -[a+1]
Tactic: simp [divisorsAntidiag]
-- Lean 4 proof step from Mathlib.NumberTheory.Divisors (goal)
Goal:
a a_1 a_2 : ℕ
⊢ (-[a_1+1], -[a_2+1]) ∈ -[a+1].divisorsAntidiag ↔ (-[a_1+1], -[a_2+1]).1 * (-[a_1+1], -[a_2+1]).2 = -[a+1] ∧ -[a+1] ≠ 0
have negSucc : ¬-[a_1+1] * -[a_2+1] = -[a+1]
Tactic: simp [divisorsAntidiag]
-- Lean 4 proof step from Mathlib.NumberTheory.Divisors (goal)
Goal:
z : ℤ
⊢ image Prod.fst z.divisorsAntidiag = z.divisors
have h : ∀ (a : ℤ), a ∈ image Prod.fst z.divisorsAntidiag ↔ a ∈ z.divisors
Tactic: ext
-- Lean 4 proof step from Mathlib.NumberTheory.Divisors (goal)
Goal:
z : ℤ
⊢ image Prod.snd z.divisorsAntidiag = z.divisors
have h : ∀ (a : ℤ), a ∈ image Prod.snd z.divisorsAntidiag ↔ a ∈ z.divisors
Tactic: ext
-- Lean 4 proof step from Mathlib.NumberTheory.Divisors (goal)
Goal:
z : ℤ
⊢ map (Equiv.prodComm ℤ ℤ).toEmbedding z.divisorsAntidiag = z.divisorsAntidiag
have h : ∀ (a : ℤ × ℤ), a ∈ map (Equiv.prodComm ℤ ℤ).toEmbedding z.divisorsAntidiag ↔ a ∈ z.divisorsAntidiag
Tactic: ext
-- Lean 4 proof step from Mathlib.NumberTheory.Divisors (goal)
Goal:
z : ℤ
⊢ map (Equiv.toEmbedding (Equiv.neg (ℤ × ℤ))) z.divisorsAntidiag = z.divisorsAntidiag
have h : ∀ (a : ℤ × ℤ), a ∈ map (Equiv.toEmbedding (Equiv.neg (ℤ × ℤ))) z.divisorsAntidiag ↔ a ∈ z.divisorsAntidiag
Tactic: ext
-- Lean 4 proof step from Mathlib.NumberTheory.Divisors (goal)
Goal:
z : ℤ
⊢ (-z).divisorsAntidiag = map ((Function.Embedding.refl ℤ).prodMap (Equiv.toEmbedding (Equiv.neg ℤ))) z.divisorsAntidiag
have h : ∀ (a : ℤ × ℤ),
  a ∈ (-z).divisorsAntidiag ↔
    a ∈ map ((Function.Embedding.refl ℤ).prodMap (Equiv.toEmbedding (Equiv.neg ℤ))) z.divisorsAntidiag
Tactic: ext
-- Lean 4 proof step from Mathlib.NumberTheory.Divisors (goal)
Goal:
n : ℕ
⊢ divisorsAntidiag (-(↑n : ℤ)) =
    disjUnion (map (Function.Embedding.prodMap Nat.castEmbedding negNatCast) n.divisorsAntidiagonal)
      (map (negNatCast.prodMap Nat.castEmbedding) n.divisorsAntidiagonal) ⋯
have zero : divisorsAntidiag (-(↑0 : ℤ)) =
  disjUnion (map (Function.Embedding.prodMap Nat.castEmbedding negNatCast) (Nat.divisorsAntidiagonal 0))
    (map (negNatCast.prodMap Nat.castEmbedding) (Nat.divisorsAntidiagonal 0)) sorry
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.NumberTheory.Divisors (goal)
Goal:
n : ℕ
zero :
  divisorsAntidiag (-(↑0 : ℤ)) =
    disjUnion (map (Function.Embedding.prodMap Nat.castEmbedding negNatCast) (Nat.divisorsAntidiagonal 0))
      (map (negNatCast.prodMap Nat.castEmbedding) (Nat.divisorsAntidiagonal 0)) ⋯
⊢ divisorsAntidiag (-(↑n : ℤ)) =
    disjUnion (map (Function.Embedding.prodMap Nat.castEmbedding negNatCast) n.divisorsAntidiagonal)
      (map (negNatCast.prodMap Nat.castEmbedding) n.divisorsAntidiagonal) ⋯
have succ : ∀ (n : ℕ),
  divisorsAntidiag (-(↑(n + 1) : ℤ)) =
    disjUnion (map (Function.Embedding.prodMap Nat.castEmbedding negNatCast) (n + 1).divisorsAntidiagonal)
      (map (negNatCast.prodMap Nat.castEmbedding) (n + 1).divisorsAntidiagonal) sorry
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.NumberTheory.Divisors (goal)
Goal:
a b : ℤ
⊢ Membership.mem (γ := Set ℤ) {1, 2, 3} (a * b) ↔
    Membership.mem (γ := Set (ℤ × ℤ))
      {(1, 1), (-1, -1), (1, 2), (2, 1), (-1, -2), (-2, -1), (1, 3), (3, 1), (-1, -3), (-3, -1)} (a, b)
have simp : (a, b) ∈ divisorsAntidiag 1 ∨ (a, b) ∈ divisorsAntidiag 2 ∨ (a, b) ∈ divisorsAntidiag 3 ↔
  (a, b) = (1, 1) ∨
    (a, b) = (-1, -1) ∨
      (a, b) = (1, 2) ∨
        (a, b) = (2, 1) ∨
          (a, b) = (-1, -2) ∨
            (a, b) = (-2, -1) ∨ (a, b) = (1, 3) ∨ (a, b) = (3, 1) ∨ (a, b) = (-1, -3) ∨ (a, b) = (-3, -1)
Tactic: simp only [← Int.prodMk_mem_divisorsAntidiag, Set.mem_insert_iff, Set.mem_singleton_iff, ne_eq,
    one_ne_zero, not_false_eq_true, OfNat.ofNat_ne_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.Divisors (goal)
Goal:
a b : ℤ
h₀ : a = 0 ↔ b = 0
⊢ Membership.mem (γ := Set ℤ) {0, 1, 2, 3, 4} (a * b) ↔
    Membership.mem (γ := Set (ℤ × ℤ))
      {(0, 0), (1, 1), (-1, -1), (1, 2), (2, 1), (-1, -2), (-2, -1), (1, 3), (3, 1), (-1, -3), (-3, -1), (4, 1), (1, 4),
        (-4, -1), (-1, -4), (2, 2), (-2, -2)}
      (a, b)
have simp : a * b = 0 ∨
    (a, b) ∈ divisorsAntidiag 1 ∨
      (a, b) ∈ divisorsAntidiag 2 ∨ (a, b) ∈ divisorsAntidiag 3 ∨ (a, b) ∈ divisorsAntidiag 4 ↔
  (a, b) = (0, 0) ∨
    (a, b) = (1, 1) ∨
      (a, b) = (-1, -1) ∨
        (a, b) = (1, 2) ∨
          (a, b) = (2, 1) ∨
            (a, b) = (-1, -2) ∨
              (a, b) = (-2, -1) ∨
                (a, b) = (1, 3) ∨
                  (a, b) = (3, 1) ∨
                    (a, b) = (-1, -3) ∨
                      (a, b) = (-3, -1) ∨
                        (a, b) = (4, 1) ∨
                          (a, b) = (1, 4) ∨ (a, b) = (-4, -1) ∨ (a, b) = (-1, -4) ∨ (a, b) = (2, 2) ∨ (a, b) = (-2, -2)
Tactic: simp only [← Int.prodMk_mem_divisorsAntidiag, Set.mem_insert_iff, Set.mem_singleton_iff, ne_eq,
    one_ne_zero, not_false_eq_true, OfNat.ofNat_ne_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.EllipticDivisibilitySequence (goal)
Goal:
x x_1 x_2 : ℤ
⊢ id (x + x_1) * id (x - x_1) * HPow.hPow (β := ℕ) (id x_2) 2 =
    id (x + x_2) * id (x - x_2) * HPow.hPow (β := ℕ) (id x_1) 2 -
      id (x_1 + x_2) * id (x_1 - x_2) * HPow.hPow (β := ℕ) (id x) 2
have simp_rw : (x + x_1) * (x - x_1) * HPow.hPow (β := ℕ) x_2 2 =
  (x + x_2) * (x - x_2) * HPow.hPow (β := ℕ) x_1 2 - (x_1 + x_2) * (x_1 - x_2) * HPow.hPow (β := ℕ) x 2
Tactic: simp_rw [id_eq]
-- Lean 4 proof step from Mathlib.NumberTheory.EllipticDivisibilitySequence (goal)
Goal:
R : Type u
inst : CommRing R
W : ℤ → R
h : IsEllSequence W
x : R
m n r : ℤ
⊢ (x • W) (m + n) * (x • W) (m - n) * HPow.hPow (β := ℕ) ((x • W) r) 2 +
        HPow.hPow (β := ℕ) x 4 *
          (W (m + r) * W (m - r) * HPow.hPow (β := ℕ) (W n) 2 - W (n + r) * W (n - r) * HPow.hPow (β := ℕ) (W m) 2) -
      ((x • W) (m + r) * (x • W) (m - r) * HPow.hPow (β := ℕ) ((x • W) n) 2 -
          (x • W) (n + r) * (x • W) (n - r) * HPow.hPow (β := ℕ) ((x • W) m) 2 +
        HPow.hPow (β := ℕ) x 4 * (W (m + n) * W (m - n) * HPow.hPow (β := ℕ) (W r) 2)) =
    0
have a : x * W (m + n) * (x * W (m - n)) * HPow.hPow (β := ℕ) (x * W r) 2 +
      HPow.hPow (β := ℕ) x 4 *
        (W (m + r) * W (m - r) * HPow.hPow (β := ℕ) (W n) 2 - W (n + r) * W (n - r) * HPow.hPow (β := ℕ) (W m) 2) -
    (x * W (m + r) * (x * W (m - r)) * HPow.hPow (β := ℕ) (x * W n) 2 -
        x * W (n + r) * (x * W (n - r)) * HPow.hPow (β := ℕ) (x * W m) 2 +
      HPow.hPow (β := ℕ) x 4 * (W (m + n) * W (m - n) * HPow.hPow (β := ℕ) (W r) 2)) =
  0
Tactic: simp_rw [Pi.smul_apply, smul_eq_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.EllipticDivisibilitySequence (goal)
Goal:
R : Type u
inst : CommRing R
W : ℤ → R
h : IsEllSequence W
x : R
m n r : ℤ
⊢ (x • W) (m + n) * (x • W) (m - n) * HPow.hPow (β := ℕ) ((x • W) r) 2 =
    (x • W) (m + r) * (x • W) (m - r) * HPow.hPow (β := ℕ) ((x • W) n) 2 -
      (x • W) (n + r) * (x • W) (n - r) * HPow.hPow (β := ℕ) ((x • W) m) 2
have a : (x • W) (m + n) * (x • W) (m - n) * HPow.hPow (β := ℕ) ((x • W) r) 2 +
      HPow.hPow (β := ℕ) x 4 *
        (W (m + r) * W (m - r) * HPow.hPow (β := ℕ) (W n) 2 - W (n + r) * W (n - r) * HPow.hPow (β := ℕ) (W m) 2) -
    ((x • W) (m + r) * (x • W) (m - r) * HPow.hPow (β := ℕ) ((x • W) n) 2 -
        (x • W) (n + r) * (x • W) (n - r) * HPow.hPow (β := ℕ) ((x • W) m) 2 +
      HPow.hPow (β := ℕ) x 4 * (W (m + n) * W (m - n) * HPow.hPow (β := ℕ) (W r) 2)) =
  0
Tactic: linear_combination (norm := (simp_rw [Pi.smul_apply, smul_eq_mul]; ring1)) x ^ 4 * h m n r
-- Lean 4 proof step from Mathlib.NumberTheory.EllipticDivisibilitySequence (goal)
Goal:
R : Type u
inst : CommRing R
b c d : R
n : ℕ
m : ℕ := n / 2
hn : ¬Even n
⊢ m + 5 < n + 5
have bc : m < n
Tactic: gcongr