awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.Divisors
Goal:
h : ∀ (a : ℤ), a ∈ divisors 0 ↔ Membership.mem (γ := Finset ℤ) ∅ a
⊢ divisors 0 = ∅

Tactic:
ext
-- Module: Mathlib.NumberTheory.Divisors
Goal:
a : ℤ
⊢ a ∈ divisors 0 ↔ Membership.mem (γ := Finset ℤ) ∅ a

Tactic:
simp
-- Module: Mathlib.NumberTheory.Divisors
Goal:
z_1 : ℤ
h : z_1.divisors.Nonempty
hx : z_1 = 0
z : ℤ
hz : z ∈ z_1.divisors
⊢ False

Tactic:
simp [hx] at hz
-- Module: Mathlib.NumberTheory.Divisors
Goal:
z : ℤ
contrapose! : z.divisors.Nonempty ↔ z ≠ 0
⊢ z.divisors = ∅ ↔ z = 0

Tactic:
contrapose!
-- Module: Mathlib.NumberTheory.Divisors
Goal:
z : ℤ
⊢ z.divisors.Nonempty ↔ z ≠ 0

Tactic:
nonempty_divisors

Premises used: Int.nonempty_divisors
-- Module: Mathlib.NumberTheory.Divisors
Goal:
z : ℤ
⊢ z.divisors.Nonempty ↔ z ≠ 0

Tactic:
exact nonempty_divisors

Premises used: Int.nonempty_divisors
-- Module: Mathlib.NumberTheory.Divisors
Goal:
⊢ divisors 1 = {1, -1}

Tactic:
rfl

Premises used: Int.divisors, Multiset.add, List.map, Finset.disjUnion, List.append, Multiset.ofList, Multiset.ndinsert, Int.neg, rfl, Int.negOfNat, ite
-- Module: Mathlib.NumberTheory.Divisors
Goal:
z : ℤ
hz : z ≠ 0
⊢ z ∈ z.divisors

Tactic:
mem_divisors.mpr ⟨dvd_rfl, hz⟩

Premises used: Iff.mpr, Int.mem_divisors, And.intro, dvd_rfl
-- Module: Mathlib.NumberTheory.Divisors
Goal:
z : ℤ
h : ∀ (a : ℤ), a ∈ (-z).divisors ↔ a ∈ z.divisors
⊢ (-z).divisors = z.divisors

Tactic:
ext
-- Module: Mathlib.NumberTheory.Divisors
Goal:
z a : ℤ
⊢ a ∈ (-z).divisors ↔ a ∈ z.divisors

Tactic:
simp
-- Module: Mathlib.NumberTheory.Divisors
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
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
⊢ xy ∈ z.divisorsAntidiag ↔ xy.1 * xy.2 = z ∧ z ≠ 0

Tactic:
rcases z, xy with ⟨_ | _, ⟨_ | _, _ | _⟩⟩
-- Module: Mathlib.NumberTheory.Divisors
Goal:
a a_1 a_2 : ℕ
simp : ¬a = 0 → ((a_1 + 1) * (a_2 + 1) = a ↔ -[a_1+1] * -[a_2+1] = (↑a : ℤ))
⊢ (-[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

Tactic:
simp [divisorsAntidiag]

Premises used: Int.divisorsAntidiag
-- Module: Mathlib.NumberTheory.Divisors
Goal:
a a_1 a_2 : ℕ
⊢ ¬a = 0 → ((a_1 + 1) * (a_2 + 1) = a ↔ -[a_1+1] * -[a_2+1] = (↑a : ℤ))

Tactic:
grind [Nat.cast_inj]

Premises used: Nat.cast_inj
-- Module: Mathlib.NumberTheory.Divisors
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

Tactic:
case ofNat.negSucc.negSucc =>
    simp [divisorsAntidiag]
    grind [Nat.cast_inj]

Premises used: Int.divisorsAntidiag, Nat.cast_inj
-- Module: Mathlib.NumberTheory.Divisors
Goal:
a a_1 a_2 : ℕ
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
⊢ (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

Tactic:
simp [divisorsAntidiag]

Premises used: Int.divisorsAntidiag
-- Module: Mathlib.NumberTheory.Divisors
Goal:
a a_1 a_2 : ℕ
⊢ 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:
grind
-- Module: Mathlib.NumberTheory.Divisors
Goal:
a a_1 a_2 : ℕ
ofNat : (0 = a ∧ ¬a = 0) ∧ a_1 = 0 ↔ (↑a_1 : ℤ) * -[a_2+1] = (↑a : ℤ) ∧ ¬a = 0
⊢ (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:
simp [divisorsAntidiag]

Premises used: Int.divisorsAntidiag
-- Module: Mathlib.NumberTheory.Divisors
Goal:
a a_1 a_2 : ℕ
⊢ (0 = a ∧ ¬a = 0) ∧ a_1 = 0 ↔ (↑a_1 : ℤ) * -[a_2+1] = (↑a : ℤ) ∧ ¬a = 0

Tactic:
grind
-- Module: Mathlib.NumberTheory.Divisors
Goal:
a a_1 a_2 : ℕ
ofNat : (0 = a ∧ ¬a = 0) ∧ a_2 = 0 ↔ -[a_1+1] * (↑a_2 : ℤ) = (↑a : ℤ) ∧ ¬a = 0
⊢ (-[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:
simp [divisorsAntidiag]

Premises used: Int.divisorsAntidiag
-- Module: Mathlib.NumberTheory.Divisors
Goal:
a a_1 a_2 : ℕ
⊢ (0 = a ∧ ¬a = 0) ∧ a_2 = 0 ↔ -[a_1+1] * (↑a_2 : ℤ) = (↑a : ℤ) ∧ ¬a = 0

Tactic:
grind
-- Module: Mathlib.NumberTheory.Divisors
Goal:
a a_1 a_2 : ℕ
negSucc : ¬HMul.hMul (α := ℤ) (↑a_1 : ℤ) (↑a_2 : ℤ) = -[a+1]
⊢ (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

Tactic:
simp [divisorsAntidiag]

Premises used: Int.divisorsAntidiag
-- Module: Mathlib.NumberTheory.Divisors
Goal:
a a_1 a_2 : ℕ
⊢ ¬HMul.hMul (α := ℤ) (↑a_1 : ℤ) (↑a_2 : ℤ) = -[a+1]

Tactic:
grind
-- Module: Mathlib.NumberTheory.Divisors
Goal:
a a_1 a_2 : ℕ
negSucc : a_1 * (a_2 + 1) = a + 1 ↔ (↑a_1 : ℤ) * -[a_2+1] = -[a+1]
⊢ (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

Tactic:
simp [divisorsAntidiag]

Premises used: Int.divisorsAntidiag
-- Module: Mathlib.NumberTheory.Divisors
Goal:
a a_1 a_2 : ℕ
⊢ a_1 * (a_2 + 1) = a + 1 ↔ (↑a_1 : ℤ) * -[a_2+1] = -[a+1]

Tactic:
grind
-- Module: Mathlib.NumberTheory.Divisors
Goal:
a a_1 a_2 : ℕ
negSucc : (a_1 + 1) * a_2 = a + 1 ↔ -[a_1+1] * (↑a_2 : ℤ) = -[a+1]
⊢ (-[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

Tactic:
simp [divisorsAntidiag]

Premises used: Int.divisorsAntidiag
-- Module: Mathlib.NumberTheory.Divisors
Goal:
a a_1 a_2 : ℕ
⊢ (a_1 + 1) * a_2 = a + 1 ↔ -[a_1+1] * (↑a_2 : ℤ) = -[a+1]

Tactic:
grind
-- Module: Mathlib.NumberTheory.Divisors
Goal:
a a_1 a_2 : ℕ
negSucc : ¬-[a_1+1] * -[a_2+1] = -[a+1]
⊢ (-[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:
simp [divisorsAntidiag]

Premises used: Int.divisorsAntidiag
-- Module: Mathlib.NumberTheory.Divisors
Goal:
a a_1 a_2 : ℕ
⊢ ¬-[a_1+1] * -[a_2+1] = -[a+1]

Tactic:
grind
-- Module: Mathlib.NumberTheory.Divisors
Goal:
z : ℤ
h : ∀ (a : ℤ), a ∈ image Prod.fst z.divisorsAntidiag ↔ a ∈ z.divisors
⊢ image Prod.fst z.divisorsAntidiag = z.divisors

Tactic:
ext
-- Module: Mathlib.NumberTheory.Divisors
Goal:
z a : ℤ
⊢ a ∈ image Prod.fst z.divisorsAntidiag ↔ a ∈ z.divisors

Tactic:
simp [Eq.comm, dvd_def]

Premises used: dvd_def, Eq.comm
-- Module: Mathlib.NumberTheory.Divisors
Goal:
z : ℤ
h : ∀ (a : ℤ), a ∈ image Prod.snd z.divisorsAntidiag ↔ a ∈ z.divisors
⊢ image Prod.snd z.divisorsAntidiag = z.divisors

Tactic:
ext
-- Module: Mathlib.NumberTheory.Divisors
Goal:
z a : ℤ
⊢ a ∈ image Prod.snd z.divisorsAntidiag ↔ a ∈ z.divisors

Tactic:
simp [Eq.comm, mul_comm, dvd_def]

Premises used: dvd_def, Eq.comm, mul_comm
-- Module: Mathlib.NumberTheory.Divisors
Goal:
⊢ divisorsAntidiag 0 = ∅

Tactic:
rfl

Premises used: Int.divisorsAntidiag, List.map, Multiset.zero, Finset.empty, Finset.disjUnion, List.append, rfl
-- Module: Mathlib.NumberTheory.Divisors
Goal:
⊢ divisorsAntidiag 1 = {(1, 1), (-1, -1)}

Tactic:
rfl

Premises used: Multiset.add, Int.divisorsAntidiag, List.map, Prod.map, Finset.disjUnion, List.append, Multiset.ofList, Multiset.ndinsert, Int.neg, rfl, Int.negOfNat, ite
-- Module: Mathlib.NumberTheory.Divisors
Goal:
⊢ divisorsAntidiag 2 = {(1, 2), (2, 1), (-1, -2), (-2, -1)}

Tactic:
rfl

Premises used: Multiset.add, Int.divisorsAntidiag, List.map, Prod.map, Finset.disjUnion, List.append, Multiset.ofList, Multiset.ndinsert, Int.neg, rfl, Int.negOfNat, ite
-- Module: Mathlib.NumberTheory.Divisors
Goal:
⊢ divisorsAntidiag 3 = {(1, 3), (3, 1), (-1, -3), (-3, -1)}

Tactic:
rfl

Premises used: Multiset.add, Int.divisorsAntidiag, List.map, Prod.map, Finset.disjUnion, List.append, Multiset.ofList, Multiset.ndinsert, Int.neg, rfl, Int.negOfNat, ite
-- Module: Mathlib.NumberTheory.Divisors
Goal:
⊢ divisorsAntidiag 4 = {(1, 4), (2, 2), (4, 1), (-1, -4), (-2, -2), (-4, -1)}

Tactic:
rfl

Premises used: Multiset.add, Int.divisorsAntidiag, List.map, Prod.map, Finset.disjUnion, List.append, Multiset.ofList, Multiset.ndinsert, Int.neg, rfl, Int.negOfNat, ite
-- Module: Mathlib.NumberTheory.Divisors
Goal:
x y z : ℤ
hz : z ≠ 0
⊢ (x, y) ∈ z.divisorsAntidiag ↔ x * y = z

Tactic:
simp [hz]
-- Module: Mathlib.NumberTheory.Divisors
Goal:
xy : ℤ × ℤ
z : ℤ
⊢ xy.swap ∈ z.divisorsAntidiag ↔ xy ∈ z.divisorsAntidiag

Tactic:
simp [mul_comm]

Premises used: mul_comm
-- Module: Mathlib.NumberTheory.Divisors
Goal:
xy : ℤ × ℤ
z : ℤ
⊢ -xy ∈ z.divisorsAntidiag ↔ xy ∈ z.divisorsAntidiag

Tactic:
simp
-- Module: Mathlib.NumberTheory.Divisors
Goal:
z : ℤ
h : ∀ (a : ℤ × ℤ), a ∈ map (Equiv.prodComm ℤ ℤ).toEmbedding z.divisorsAntidiag ↔ a ∈ z.divisorsAntidiag
⊢ map (Equiv.prodComm ℤ ℤ).toEmbedding z.divisorsAntidiag = z.divisorsAntidiag

Tactic:
ext
-- Module: Mathlib.NumberTheory.Divisors
Goal:
z : ℤ
a : ℤ × ℤ
⊢ a ∈ map (Equiv.prodComm ℤ ℤ).toEmbedding z.divisorsAntidiag ↔ a ∈ z.divisorsAntidiag

Tactic:
simp [mem_divisorsAntidiag]

Premises used: Int.mem_divisorsAntidiag
-- Module: Mathlib.NumberTheory.Divisors
Goal:
z : ℤ
h : ∀ (a : ℤ × ℤ), a ∈ map (Equiv.toEmbedding (Equiv.neg (ℤ × ℤ))) z.divisorsAntidiag ↔ a ∈ z.divisorsAntidiag
⊢ map (Equiv.toEmbedding (Equiv.neg (ℤ × ℤ))) z.divisorsAntidiag = z.divisorsAntidiag

Tactic:
ext
-- Module: Mathlib.NumberTheory.Divisors
Goal:
z : ℤ
a : ℤ × ℤ
⊢ a ∈ map (Equiv.toEmbedding (Equiv.neg (ℤ × ℤ))) z.divisorsAntidiag ↔ a ∈ z.divisorsAntidiag

Tactic:
simp [mem_divisorsAntidiag, mul_comm]

Premises used: Int.mem_divisorsAntidiag, mul_comm
-- Module: Mathlib.NumberTheory.Divisors
Goal:
z : ℤ
h :
  ∀ (a : ℤ × ℤ),
    a ∈ (-z).divisorsAntidiag ↔
      a ∈ map ((Function.Embedding.refl ℤ).prodMap (Equiv.toEmbedding (Equiv.neg ℤ))) z.divisorsAntidiag
⊢ (-z).divisorsAntidiag = map ((Function.Embedding.refl ℤ).prodMap (Equiv.toEmbedding (Equiv.neg ℤ))) z.divisorsAntidiag

Tactic:
ext
-- Module: Mathlib.NumberTheory.Divisors
Goal:
z : ℤ
a : ℤ × ℤ
⊢ a ∈ (-z).divisorsAntidiag ↔
    a ∈ map ((Function.Embedding.refl ℤ).prodMap (Equiv.toEmbedding (Equiv.neg ℤ))) z.divisorsAntidiag

Tactic:
simp [mem_divisorsAntidiag, Prod.ext_iff, neg_eq_iff_eq_neg]

Premises used: Int.mem_divisorsAntidiag, Prod.ext_iff, neg_eq_iff_eq_neg
-- Module: Mathlib.NumberTheory.Divisors
Goal:
xy : ℤ × ℤ
x y z : ℤ
n : ℕ
⊢ Disjoint (map (Function.Embedding.prodMap Nat.castEmbedding Nat.castEmbedding) n.divisorsAntidiagonal)
    (map (negNatCast.prodMap negNatCast) n.divisorsAntidiagonal)

Tactic:
simp +contextual [disjoint_left, eq_comm]

Premises used: eq_comm, Finset.disjoint_left
-- Module: Mathlib.NumberTheory.Divisors
Goal:
n : ℕ
⊢ divisorsAntidiag (↑n : ℤ) =
    disjUnion (map (Function.Embedding.prodMap Nat.castEmbedding Nat.castEmbedding) n.divisorsAntidiagonal)
      (map (negNatCast.prodMap negNatCast) n.divisorsAntidiagonal) ⋯

Tactic:
rfl

Premises used: Int.divisorsAntidiag, rfl
-- Module: Mathlib.NumberTheory.Divisors
Goal:
xy : ℤ × ℤ
x y z : ℤ
n : ℕ
⊢ Disjoint (map (Function.Embedding.prodMap Nat.castEmbedding negNatCast) n.divisorsAntidiagonal)
    (map (negNatCast.prodMap Nat.castEmbedding) n.divisorsAntidiagonal)

Tactic:
simp +contextual [disjoint_left, eq_comm]

Premises used: eq_comm, Finset.disjoint_left
-- Module: Mathlib.NumberTheory.Divisors
Goal:
n : ℕ
zero :
  divisorsAntidiag (-(↑0 : ℤ)) =
    disjUnion (map (Function.Embedding.prodMap Nat.castEmbedding negNatCast) (Nat.divisorsAntidiagonal 0))
      (map (negNatCast.prodMap Nat.castEmbedding) (Nat.divisorsAntidiagonal 0)) ⋯
succ :
  ∀ (n : ℕ),
    divisorsAntidiag (-(↑(n + 1) : ℤ)) =
      disjUnion (map (Function.Embedding.prodMap Nat.castEmbedding negNatCast) (n + 1).divisorsAntidiagonal)
        (map (negNatCast.prodMap Nat.castEmbedding) (n + 1).divisorsAntidiagonal) ⋯
⊢ divisorsAntidiag (-(↑n : ℤ)) =
    disjUnion (map (Function.Embedding.prodMap Nat.castEmbedding negNatCast) n.divisorsAntidiagonal)
      (map (negNatCast.prodMap Nat.castEmbedding) n.divisorsAntidiagonal) ⋯

Tactic:
cases n
-- Module: Mathlib.NumberTheory.Divisors
Goal:
⊢ divisorsAntidiag (-(↑0 : ℤ)) =
    disjUnion (map (Function.Embedding.prodMap Nat.castEmbedding negNatCast) (Nat.divisorsAntidiagonal 0))
      (map (negNatCast.prodMap Nat.castEmbedding) (Nat.divisorsAntidiagonal 0)) ⋯

Tactic:
rfl
-- Module: Mathlib.NumberTheory.Divisors
Goal:
n : ℕ
⊢ divisorsAntidiag (-(↑(n + 1) : ℤ)) =
    disjUnion (map (Function.Embedding.prodMap Nat.castEmbedding negNatCast) (n + 1).divisorsAntidiagonal)
      (map (negNatCast.prodMap Nat.castEmbedding) (n + 1).divisorsAntidiagonal) ⋯

Tactic:
rfl
-- Module: Mathlib.NumberTheory.Divisors
Goal:
n : ℕ
⊢ divisorsAntidiag (OfNat.ofNat n) =
    disjUnion (map (Function.Embedding.prodMap Nat.castEmbedding Nat.castEmbedding) n.divisorsAntidiagonal)
      (map (negNatCast.prodMap negNatCast) n.divisorsAntidiagonal) ⋯

Tactic:
rfl

Premises used: Int.divisorsAntidiag, rfl
-- Module: Mathlib.NumberTheory.Divisors
Goal:
a b : ℤ
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)
⊢ 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)

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]

Premises used: OfNat.ofNat_ne_zero, Int.prodMk_mem_divisorsAntidiag, ne_eq, Set.mem_singleton_iff, Set.mem_insert_iff, one_ne_zero, not_false_eq_true
-- Module: Mathlib.NumberTheory.Divisors
Goal:
a b : ℤ
⊢ (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:
aesop
-- Module: Mathlib.NumberTheory.Divisors
Goal:
a b : ℤ
h₀ : a = 0 ↔ b = 0
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)
⊢ 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)

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]

Premises used: OfNat.ofNat_ne_zero, Int.prodMk_mem_divisorsAntidiag, ne_eq, Set.mem_singleton_iff, Set.mem_insert_iff, one_ne_zero, not_false_eq_true
-- Module: Mathlib.NumberTheory.Divisors
Goal:
a b : ℤ
h₀ : a = 0 ↔ b = 0
⊢ 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:
aesop
-- Module: Mathlib.NumberTheory.EllipticDivisibilitySequence
Goal:
x x_1 x_2 : ℤ
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
⊢ 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

Tactic:
simp_rw [id_eq]

Premises used: id_eq
-- Module: Mathlib.NumberTheory.EllipticDivisibilitySequence
Goal:
x x_1 x_2 : ℤ
⊢ (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:
ring1
-- Module: Mathlib.NumberTheory.EllipticDivisibilitySequence
Goal:
⊢ IsDivSequence id

Tactic:
fun _ _ => Int.ofNat_dvd.mpr

Premises used: Iff.mpr, Int.ofNat_dvd, IsDivSequence
-- Module: Mathlib.NumberTheory.EllipticDivisibilitySequence
Goal:
⊢ IsEllDivSequence id

Tactic:
⟨isEllSequence_id, isDivSequence_id⟩

Premises used: isEllSequence_id, isDivSequence_id, IsEllDivSequence, And.intro
-- Module: Mathlib.NumberTheory.EllipticDivisibilitySequence
Goal:
R : Type u
inst : CommRing R
W : ℤ → R
h : IsEllSequence W
x : R
m n r : ℤ
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
⊢ (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]

Premises used: smul_eq_mul, Pi.smul_apply
-- Module: Mathlib.NumberTheory.EllipticDivisibilitySequence
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

Tactic:
ring1
-- Module: Mathlib.NumberTheory.EllipticDivisibilitySequence
Goal:
R : Type u
inst : CommRing R
W : ℤ → R
h : IsEllSequence W
x : R
m n r : ℤ
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
⊢ (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

Tactic:
linear_combination (norm := (simp_rw [Pi.smul_apply, smul_eq_mul]; ring1)) x ^ 4 * h m n r

Premises used: smul_eq_mul, Pi.smul_apply
-- Module: Mathlib.NumberTheory.EllipticDivisibilitySequence
Goal:
R : Type u
inst : CommRing R
W : ℤ → R
h : IsDivSequence W
x : R
⊢ IsDivSequence (x • W)

Tactic:
fun m n r => mul_dvd_mul_left x <| h m n r

Premises used: mul_dvd_mul_left, IsDivSequence
-- Module: Mathlib.NumberTheory.EllipticDivisibilitySequence
Goal:
R : Type u
inst : CommRing R
W : ℤ → R
h : IsEllDivSequence W
x : R
⊢ IsEllDivSequence (x • W)

Tactic:
⟨h.left.smul x, h.right.smul x⟩

Premises used: IsDivSequence.smul, IsEllDivSequence, And.right, And.left, And.intro, IsEllSequence.smul
-- Module: Mathlib.NumberTheory.EllipticDivisibilitySequence
Goal:
R : Type u
inst : CommRing R
b c d : R
n : ℕ
m : ℕ := n / 2
hn : ¬Even n
bc : m < n
⊢ m + 5 < n + 5

Tactic:
gcongr
-- Module: Mathlib.NumberTheory.EllipticDivisibilitySequence
Goal:
R : Type u
inst : CommRing R
b c d : R
n : ℕ
m : ℕ := n / 2
hn : ¬Even n
⊢ m < n

Tactic:
Nat.div_lt_self (Nat.not_even_iff_odd.mp hn).pos one_lt_two

Premises used: Odd.pos, Nat.div_lt_self, Nat.not_even_iff_odd, Iff.mp, one_lt_two
-- Module: Mathlib.NumberTheory.EllipticDivisibilitySequence
Goal:
R : Type u
inst : CommRing R
b c d : R
n : ℕ
m : ℕ := n / 2
hn : ¬Even n
⊢ m < n

Tactic:
exact Nat.div_lt_self (Nat.not_even_iff_odd.mp hn).pos one_lt_two

Premises used: Odd.pos, Nat.div_lt_self, Nat.not_even_iff_odd, Iff.mp, one_lt_two
-- Module: Mathlib.NumberTheory.EllipticDivisibilitySequence
Goal:
R : Type u
inst : CommRing R
b c d : R
rw rw₁ : Eq.{u + 1} (α := R) 0 0
⊢ preNormEDS' b c d 0 = 0

Tactic:
rw [preNormEDS']

Premises used: preNormEDS'
-- Module: Mathlib.NumberTheory.EllipticDivisibilitySequence
Goal:
R : Type u
inst : CommRing R
b c d : R
rw rw₁ : Eq.{u + 1} (α := R) 1 1
⊢ preNormEDS' b c d 1 = 1

Tactic:
rw [preNormEDS']

Premises used: preNormEDS'
-- Module: Mathlib.NumberTheory.EllipticDivisibilitySequence
Goal:
R : Type u
inst : CommRing R
b c d : R
rw rw₁ : Eq.{u + 1} (α := R) 1 1
⊢ preNormEDS' b c d 2 = 1

Tactic:
rw [preNormEDS']

Premises used: preNormEDS'
-- Module: Mathlib.NumberTheory.EllipticDivisibilitySequence
Goal:
R : Type u
inst : CommRing R
b c d : R
rw rw₁ : c = c
⊢ preNormEDS' b c d 3 = c

Tactic:
rw [preNormEDS']

Premises used: preNormEDS'
-- Module: Mathlib.NumberTheory.EllipticDivisibilitySequence
Goal:
R : Type u
inst : CommRing R
b c d : R
rw rw₁ : d = d
⊢ preNormEDS' b c d 4 = d

Tactic:
rw [preNormEDS']

Premises used: preNormEDS'
-- Module: Mathlib.NumberTheory.EllipticDivisibilitySequence
Goal:
R : Type u
inst : CommRing R
b c d : R
m : ℕ
⊢ 2 * (m + 3) = 2 * m + 1 + 5

Tactic:
rfl