awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.DirichletCharacter.Orthogonality (goal)
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
inst_1 : NeZero n
inst_2 : HasEnoughRootsOfUnity R (Monoid.exponent (ZMod n)ˣ)
inst_3 : IsDomain R
a : ZMod n
⊢ Eq.{u_1 + 1} (α := R) (∑ χ : DirichletCharacter R n, (χ : (a : ZMod n) → R) a) (if a = 1 then (↑n.totient : R) else 0)
have pos : ∀ (ha : a = 1), Eq.{u_1 + 1} (α := R) (∑ χ : DirichletCharacter R n, (χ : (a : ZMod n) → R) a) (↑n.totient : R)
Tactic: split_ifs with ha
-- Lean 4 proof step from Mathlib.NumberTheory.DirichletCharacter.Orthogonality (goal)
Goal:
R : Type u_1
inst : CommRing R
n : ℕ
inst_1 : NeZero n
inst_2 : HasEnoughRootsOfUnity R (Monoid.exponent (ZMod n)ˣ)
inst_3 : IsDomain R
a : ZMod n
pos : ∀ (ha : a = 1), Eq.{u_1 + 1} (α := R) (∑ χ : DirichletCharacter R n, (χ : (a : ZMod n) → R) a) (↑n.totient : R)
⊢ Eq.{u_1 + 1} (α := R) (∑ χ : DirichletCharacter R n, (χ : (a : ZMod n) → R) a) (if a = 1 then (↑n.totient : R) else 0)
have neg : ∀ (ha : ¬a = 1), Eq.{u_1 + 1} (α := R) (∑ χ : DirichletCharacter R n, (χ : (a : ZMod n) → R) a) 0
Tactic: split_ifs with ha
-- Lean 4 proof step from Mathlib.NumberTheory.Divisors (goal)
Goal:
n : ℕ
h : n ≠ 0
⊢ {d ∈ range n.succ | d ∣ n} = n.divisors
have h₁ : ∀ (a : ℕ), a ∈ {d ∈ range n.succ | d ∣ n} ↔ a ∈ n.divisors
Tactic: ext
-- Lean 4 proof step from Mathlib.NumberTheory.Divisors (goal)
Goal:
n : ℕ
h : n ≠ 0
a : ℕ
⊢ a ∈ {d ∈ range n.succ | d ∣ n} ↔ a ∈ n.divisors
have h₁ : a ∣ n → a < n.succ → 1 ≤ a
Tactic: simp only [divisors, mem_filter, mem_range, mem_Ico, and_congr_left_iff, iff_and_self]
-- Lean 4 proof step from Mathlib.NumberTheory.Divisors (goal)
Goal:
n : ℕ
h : n ≠ 0
⊢ {d ∈ range n | d ∣ n} = n.properDivisors
have h₁ : ∀ (a : ℕ), a ∈ {d ∈ range n | d ∣ n} ↔ a ∈ n.properDivisors
Tactic: ext
-- Lean 4 proof step from Mathlib.NumberTheory.Divisors (goal)
Goal:
n : ℕ
h : n ≠ 0
a : ℕ
⊢ a ∈ {d ∈ range n | d ∣ n} ↔ a ∈ n.properDivisors
have h₁ : a ∣ n → a < n → 1 ≤ a
Tactic: simp only [properDivisors, mem_filter, mem_range, mem_Ico, and_congr_left_iff, iff_and_self]
-- Lean 4 proof step from Mathlib.NumberTheory.Divisors (goal)
Goal:
n m : ℕ
⊢ n ∈ m.properDivisors ↔ n ∣ m ∧ n < m
have inl : n ∈ properDivisors 0 ↔ n ∣ 0 ∧ n < 0
Tactic: rcases eq_or_ne m 0 with (rfl | hm)
Cleared hypotheses: m
-- Lean 4 proof step from Mathlib.NumberTheory.Divisors (goal)
Goal:
n m : ℕ
inl : n ∈ properDivisors 0 ↔ n ∣ 0 ∧ n < 0
⊢ n ∈ m.properDivisors ↔ n ∣ m ∧ n < m
have inr : ∀ (hm : m ≠ 0), n ∈ m.properDivisors ↔ n ∣ m ∧ n < m
Tactic: rcases eq_or_ne m 0 with (rfl | hm)
-- Lean 4 proof step from Mathlib.NumberTheory.Divisors (goal)
Goal:
n : ℕ
h : n ≠ 0
⊢ insert n n.properDivisors = n.divisors
have rw : insert n n.properDivisors = {d ∈ Ico 1 (n + 1) | d ∣ n}
Tactic: rw [divisors, properDivisors,
    ← Finset.insert_Ico_right_eq_Ico_add_one (one_le_iff_ne_zero.2 h),
    Finset.filter_insert, if_pos (dvd_refl n)]
-- Lean 4 proof step from Mathlib.NumberTheory.Divisors (goal)
Goal:
n : ℕ
h : n ≠ 0
rw : insert n n.properDivisors = {d ∈ Ico 1 (n + 1) | d ∣ n}
⊢ insert n n.properDivisors = n.divisors
have rw₁ : insert n ({d ∈ Ico 1 n | d ∣ n}) = {d ∈ Ico 1 (n + 1) | d ∣ n}
Tactic: rw [divisors, properDivisors,
    ← Finset.insert_Ico_right_eq_Ico_add_one (one_le_iff_ne_zero.2 h),
    Finset.filter_insert, if_pos (dvd_refl n)]
-- Lean 4 proof step from Mathlib.NumberTheory.Divisors (goal)
Goal:
n : ℕ
h : n ≠ 0
rw : insert n n.properDivisors = {d ∈ Ico 1 (n + 1) | d ∣ n}
rw₁ : insert n ({d ∈ Ico 1 n | d ∣ n}) = {d ∈ Ico 1 (n + 1) | d ∣ n}
⊢ insert n n.properDivisors = n.divisors
have rw₂ : insert n ({d ∈ Ico 1 n | d ∣ n}) = {d ∈ insert n (Ico 1 n) | d ∣ n}
Tactic: rw [divisors, properDivisors,
    ← Finset.insert_Ico_right_eq_Ico_add_one (one_le_iff_ne_zero.2 h),
    Finset.filter_insert, if_pos (dvd_refl n)]
-- Lean 4 proof step from Mathlib.NumberTheory.Divisors (goal)
Goal:
n : ℕ
h : n ≠ 0
rw : insert n n.properDivisors = {d ∈ Ico 1 (n + 1) | d ∣ n}
rw₁ : insert n ({d ∈ Ico 1 n | d ∣ n}) = {d ∈ Ico 1 (n + 1) | d ∣ n}
rw₂ : insert n ({d ∈ Ico 1 n | d ∣ n}) = {d ∈ insert n (Ico 1 n) | d ∣ n}
⊢ insert n n.properDivisors = n.divisors
have rw₃ : insert n ({d ∈ Ico 1 n | d ∣ n}) = if n ∣ n then insert n ({d ∈ Ico 1 n | d ∣ n}) else {d ∈ Ico 1 n | d ∣ n}
Tactic: rw [divisors, properDivisors,
    ← Finset.insert_Ico_right_eq_Ico_add_one (one_le_iff_ne_zero.2 h),
    Finset.filter_insert, if_pos (dvd_refl n)]
-- Lean 4 proof step from Mathlib.NumberTheory.Divisors (goal)
Goal:
n : ℕ
h : n ≠ 0
rw : insert n n.properDivisors = {d ∈ Ico 1 (n + 1) | d ∣ n}
rw₁ : insert n ({d ∈ Ico 1 n | d ∣ n}) = {d ∈ Ico 1 (n + 1) | d ∣ n}
rw₂ : insert n ({d ∈ Ico 1 n | d ∣ n}) = {d ∈ insert n (Ico 1 n) | d ∣ n}
rw₃ : insert n ({d ∈ Ico 1 n | d ∣ n}) = if n ∣ n then insert n ({d ∈ Ico 1 n | d ∣ n}) else {d ∈ Ico 1 n | d ∣ n}
⊢ insert n n.properDivisors = n.divisors
have rw₄ : insert n ({d ∈ Ico 1 n | d ∣ n}) = insert n ({d ∈ Ico 1 n | d ∣ n})
Tactic: rw [divisors, properDivisors,
    ← Finset.insert_Ico_right_eq_Ico_add_one (one_le_iff_ne_zero.2 h),
    Finset.filter_insert, if_pos (dvd_refl n)]
-- Lean 4 proof step from Mathlib.NumberTheory.Divisors (goal)
Goal:
n : ℕ
h : n ≠ 0
⊢ cons n n.properDivisors ⋯ = n.divisors
have rw : insert n n.properDivisors = n.divisors
Tactic: rw [cons_eq_insert, insert_self_properDivisors h]
-- Lean 4 proof step from Mathlib.NumberTheory.Divisors (goal)
Goal:
n : ℕ
h : n ≠ 0
rw : insert n n.properDivisors = n.divisors
⊢ cons n n.properDivisors ⋯ = n.divisors
have rw₁ : n.divisors = n.divisors
Tactic: rw [cons_eq_insert, insert_self_properDivisors h]
-- Lean 4 proof step from Mathlib.NumberTheory.Divisors (goal)
Goal:
n m : ℕ
⊢ n ∈ m.divisors ↔ n ∣ m ∧ m ≠ 0
have inl : n ∈ divisors 0 ↔ n ∣ 0 ∧ Ne (α := ℕ) 0 0
Tactic: rcases eq_or_ne m 0 with (rfl | hm)
Cleared hypotheses: m
-- Lean 4 proof step from Mathlib.NumberTheory.Divisors (goal)
Goal:
n m : ℕ
inl : n ∈ divisors 0 ↔ n ∣ 0 ∧ Ne (α := ℕ) 0 0
⊢ n ∈ m.divisors ↔ n ∣ m ∧ m ≠ 0
have inr : ∀ (hm : m ≠ 0), n ∈ m.divisors ↔ n ∣ m ∧ m ≠ 0
Tactic: rcases eq_or_ne m 0 with (rfl | hm)
-- Lean 4 proof step from Mathlib.NumberTheory.Divisors (goal)
Goal:
n m : ℕ
hm : m ≠ 0
⊢ n ∈ m.divisors ↔ n ∣ m ∧ m ≠ 0
have inr : n ∣ m → n ≤ m
Tactic: simp only [hm, Ne, not_false_iff, and_true, ← filter_dvd_eq_divisors hm, mem_filter,
    mem_range, and_iff_right_iff_imp, Nat.lt_succ_iff]
-- Lean 4 proof step from Mathlib.NumberTheory.Divisors (goal)
Goal:
n : ℕ
x : ℕ × ℕ
⊢ x ∈ n.divisorsAntidiagonal ↔ x.1 * x.2 = n ∧ n ≠ 0
have obtain : ∀ (a b : ℕ), (a, b) ∈ n.divisorsAntidiagonal ↔ (a, b).1 * (a, b).2 = n ∧ n ≠ 0
Tactic: obtain ⟨a, b⟩ := x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.NumberTheory.Divisors (goal)
Goal:
n a b : ℕ
⊢ (a, b) ∈ n.divisorsAntidiagonal ↔ (a, b).1 * (a, b).2 = n ∧ n ≠ 0
have simp : a ∣ n ∧ (a ≠ 0 ∧ a ≤ n) ∧ n / a = b ↔ a * b = n ∧ n ≠ 0
Tactic: simp only [divisorsAntidiagonal, mul_div_eq_iff_dvd, mem_filterMap, mem_Icc, one_le_iff_ne_zero,
    Option.ite_none_right_eq_some, Option.some.injEq, Prod.ext_iff, and_left_comm, exists_eq_left]
-- Lean 4 proof step from Mathlib.NumberTheory.Divisors (goal)
Goal:
n a b : ℕ
⊢ a ∣ n ∧ (a ≠ 0 ∧ a ≤ n) ∧ n / a = b ↔ a * b = n ∧ n ≠ 0
have mp : a ∣ n ∧ (a ≠ 0 ∧ a ≤ n) ∧ n / a = b → a * b = n ∧ n ≠ 0
Tactic: constructor
-- Lean 4 proof step from Mathlib.NumberTheory.Divisors (goal)
Goal:
n a b : ℕ
mp : a ∣ n ∧ (a ≠ 0 ∧ a ≤ n) ∧ n / a = b → a * b = n ∧ n ≠ 0
⊢ a ∣ n ∧ (a ≠ 0 ∧ a ≤ n) ∧ n / a = b ↔ a * b = n ∧ n ≠ 0
have mpr : a * b = n ∧ n ≠ 0 → a ∣ n ∧ (a ≠ 0 ∧ a ≤ n) ∧ n / a = b
Tactic: constructor
-- Lean 4 proof step from Mathlib.NumberTheory.Divisors (goal)
Goal:
n a : ℕ
han : a ∣ n
ha : a ≠ 0
han' : a ≤ n
⊢ a * (n / a) = n ∧ n ≠ 0
have mp : ¬n = 0
Tactic: simp [Nat.mul_div_eq_iff_dvd, han]
-- Lean 4 proof step from Mathlib.NumberTheory.Divisors (hypothesis)
Goal:
a b : ℕ
hab : a * b ≠ 0
⊢ a ∣ a * b ∧ (a ≠ 0 ∧ a ≤ a * b) ∧ a * b / a = b
have hab₁ : a ≠ 0 ∧ b ≠ 0
Tactic: rw [mul_ne_zero_iff] at hab
Cleared hypotheses: hab
-- Lean 4 proof step from Mathlib.NumberTheory.Divisors (goal)
Goal:
n : ℕ
⊢ n.divisorsAntidiagonalList.toFinset = n.divisorsAntidiagonal
have rw : List.toFinset
    (List.filterMap
      (fun (x : ℕ) ↦
        have y := n / x;
        if x * y = n then some (x, y) else none)
      (List.range' 1 n)) =
  n.divisorsAntidiagonal
Tactic: rw [divisorsAntidiagonalList, divisorsAntidiagonal, List.toFinset_filterMap
    (f_inj := by simp_all), List.toFinset_range'_1_1]
-- Lean 4 proof step from Mathlib.NumberTheory.Divisors (goal)
Goal:
n : ℕ
rw :
  List.toFinset
      (List.filterMap
        (fun (x : ℕ) ↦
          have y := n / x;
          if x * y = n then some (x, y) else none)
        (List.range' 1 n)) =
    n.divisorsAntidiagonal
⊢ n.divisorsAntidiagonalList.toFinset = n.divisorsAntidiagonal
have rw₁ : List.toFinset
    (List.filterMap
      (fun (x : ℕ) ↦
        have y := n / x;
        if x * y = n then some (x, y) else none)
      (List.range' 1 n)) =
  filterMap
    (fun (x : ℕ) ↦
      have y := n / x;
      if x * y = n then some (x, y) else none)
    (Icc 1 n) sorry
Tactic: rw [divisorsAntidiagonalList, divisorsAntidiagonal, List.toFinset_filterMap
    (f_inj := by simp_all), List.toFinset_range'_1_1]
-- Lean 4 proof step from Mathlib.NumberTheory.Divisors (goal)
Goal:
n : ℕ
rw :
  List.toFinset
      (List.filterMap
        (fun (x : ℕ) ↦
          have y := n / x;
          if x * y = n then some (x, y) else none)
        (List.range' 1 n)) =
    n.divisorsAntidiagonal
rw₁ :
  List.toFinset
      (List.filterMap
        (fun (x : ℕ) ↦
          have y := n / x;
          if x * y = n then some (x, y) else none)
        (List.range' 1 n)) =
    filterMap
      (fun (x : ℕ) ↦
        have y := n / x;
        if x * y = n then some (x, y) else none)
      (Icc 1 n) ⋯
⊢ n.divisorsAntidiagonalList.toFinset = n.divisorsAntidiagonal
have rw₂ : filterMap
    (fun (x : ℕ) ↦
      have y := n / x;
      if x * y = n then some (x, y) else none)
    (List.range' 1 n).toFinset sorry =
  filterMap
    (fun (x : ℕ) ↦
      have y := n / x;
      if x * y = n then some (x, y) else none)
    (Icc 1 n) sorry
Tactic: rw [divisorsAntidiagonalList, divisorsAntidiagonal, List.toFinset_filterMap
    (f_inj := by simp_all), List.toFinset_range'_1_1]
-- Lean 4 proof step from Mathlib.NumberTheory.Divisors (goal)
Goal:
n : ℕ
rw :
  List.toFinset
      (List.filterMap
        (fun (x : ℕ) ↦
          have y := n / x;
          if x * y = n then some (x, y) else none)
        (List.range' 1 n)) =
    n.divisorsAntidiagonal
rw₁ :
  List.toFinset
      (List.filterMap
        (fun (x : ℕ) ↦
          have y := n / x;
          if x * y = n then some (x, y) else none)
        (List.range' 1 n)) =
    filterMap
      (fun (x : ℕ) ↦
        have y := n / x;
        if x * y = n then some (x, y) else none)
      (Icc 1 n) ⋯
rw₂ :
  filterMap
      (fun (x : ℕ) ↦
        have y := n / x;
        if x * y = n then some (x, y) else none)
      (List.range' 1 n).toFinset ⋯ =
    filterMap
      (fun (x : ℕ) ↦
        have y := n / x;
        if x * y = n then some (x, y) else none)
      (Icc 1 n) ⋯
⊢ n.divisorsAntidiagonalList.toFinset = n.divisorsAntidiagonal
have rw₃ : filterMap
    (fun (x : ℕ) ↦
      have y := n / x;
      if x * y = n then some (x, y) else none)
    (Icc 1 n) sorry =
  filterMap
    (fun (x : ℕ) ↦
      have y := n / x;
      if x * y = n then some (x, y) else none)
    (Icc 1 n) sorry
Tactic: rw [divisorsAntidiagonalList, divisorsAntidiagonal, List.toFinset_filterMap
    (f_inj := by simp_all), List.toFinset_range'_1_1]
-- Lean 4 proof step from Mathlib.NumberTheory.Divisors (goal)
Goal:
n : ℕ
⊢ List.Pairwise (fun (x1 x2 : ℕ × ℕ) ↦ x1.1 < x2.1) n.divisorsAntidiagonalList
have refine : ∀ (a b : ℕ) (c : a < b) (d : ℕ × ℕ)
  (h :
    (have y := n / a;
      if a * y = n then some (a, y) else none) =
      some d)
  (ha : ℕ × ℕ)
  (h' :
    (have y := n / b;
      if b * y = n then some (b, y) else none) =
      some ha),
  d.1 < ha.1
Tactic: refine (List.sortedLT_range' _ _ Nat.one_ne_zero).pairwise.filterMap _ fun a b c d h ha h' => ?_
-- Lean 4 proof step from Mathlib.NumberTheory.Divisors (goal)
Goal:
n a b : ℕ
c : a < b
d : ℕ × ℕ
h :
  (have y := n / a;
    if a * y = n then some (a, y) else none) =
    some d
ha : ℕ × ℕ
h' :
  (have y := n / b;
    if b * y = n then some (b, y) else none) =
    some ha
⊢ d.1 < ha.1
have rw : ∀ (h : a * (n / a) = n ∧ (a, n / a) = d) (ha : ℕ × ℕ) (h' : b * (n / b) = n ∧ (b, n / b) = ha), d.1 < ha.1
Tactic: rw [Option.ite_none_right_eq_some, Option.some.injEq] at h h'
Cleared hypotheses: h, ha, h'
-- Lean 4 proof step from Mathlib.NumberTheory.Divisors (goal)
Goal:
n : ℕ
⊢ List.Pairwise (fun (x1 x2 : ℕ × ℕ) ↦ x1.2 > x2.2) n.divisorsAntidiagonalList
have inl : List.Pairwise (fun (x1 x2 : ℕ × ℕ) ↦ x1.2 > x2.2) (divisorsAntidiagonalList 0)
Tactic: obtain rfl | hn := eq_or_ne n 0
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.NumberTheory.Divisors (goal)
Goal:
n : ℕ
inl : List.Pairwise (fun (x1 x2 : ℕ × ℕ) ↦ x1.2 > x2.2) (divisorsAntidiagonalList 0)
⊢ List.Pairwise (fun (x1 x2 : ℕ × ℕ) ↦ x1.2 > x2.2) n.divisorsAntidiagonalList
have inr : ∀ (hn : n ≠ 0), List.Pairwise (fun (x1 x2 : ℕ × ℕ) ↦ x1.2 > x2.2) n.divisorsAntidiagonalList
Tactic: obtain rfl | hn := eq_or_ne n 0
-- Lean 4 proof step from Mathlib.NumberTheory.Divisors (goal)
Goal:
n : ℕ
hn : n ≠ 0
⊢ List.Pairwise (fun (x1 x2 : ℕ × ℕ) ↦ x1.2 > x2.2) n.divisorsAntidiagonalList
have inr : ∀ (a a' : ℕ),
  a < a' →
    ∀ (b : ℕ × ℕ),
      (have y := n / a;
          if a * y = n then some (a, y) else none) =
          some b →
        ∀ (b' : ℕ × ℕ),
          (have y := n / a';
              if a' * y = n then some (a', y) else none) =
              some b' →
            b.2 > b'.2
Tactic: refine (List.sortedLT_range' _ _ Nat.one_ne_zero).pairwise.filterMap _ ?_
-- Lean 4 proof step from Mathlib.NumberTheory.Divisors (goal)
Goal:
n : ℕ
hn : n ≠ 0
⊢ ∀ (a a' : ℕ),
    a < a' →
      ∀ (b : ℕ × ℕ),
        (have y := n / a;
            if a * y = n then some (a, y) else none) =
            some b →
          ∀ (b' : ℕ × ℕ),
            (have y := n / a';
                if a' * y = n then some (a', y) else none) =
                some b' →
              b.2 > b'.2
have inr : ∀ (a a' : ℕ),
  a < a' →
    ∀ (a_2 b : ℕ),
      a * (n / a) = n → a = a_2 → n / a = b → ∀ (a b_1 : ℕ), a' * (n / a') = n → a' = a → n / a' = b_1 → b_1 < b
Tactic: simp only [Option.ite_none_right_eq_some, Option.some.injEq, gt_iff_lt,
    and_imp, Prod.forall, Prod.mk.injEq]
-- Lean 4 proof step from Mathlib.NumberTheory.Divisors (goal)
Goal:
n : ℕ
a : ℕ × ℕ
⊢ a ∈ n.divisorsAntidiagonalList ↔ a.1 * a.2 = n ∧ n ≠ 0
have rw : a ∈ n.divisorsAntidiagonalList.toFinset ↔ a.1 * a.2 = n ∧ n ≠ 0
Tactic: rw [← List.mem_toFinset, toFinset_divisorsAntidiagonalList, mem_divisorsAntidiagonal]
-- Lean 4 proof step from Mathlib.NumberTheory.Divisors (goal)
Goal:
n : ℕ
a : ℕ × ℕ
rw : a ∈ n.divisorsAntidiagonalList.toFinset ↔ a.1 * a.2 = n ∧ n ≠ 0
⊢ a ∈ n.divisorsAntidiagonalList ↔ a.1 * a.2 = n ∧ n ≠ 0
have rw₁ : a ∈ n.divisorsAntidiagonal ↔ a.1 * a.2 = n ∧ n ≠ 0
Tactic: rw [← List.mem_toFinset, toFinset_divisorsAntidiagonalList, mem_divisorsAntidiagonal]
-- Lean 4 proof step from Mathlib.NumberTheory.Divisors (goal)
Goal:
n : ℕ
a : ℕ × ℕ
rw : a ∈ n.divisorsAntidiagonalList.toFinset ↔ a.1 * a.2 = n ∧ n ≠ 0
rw₁ : a ∈ n.divisorsAntidiagonal ↔ a.1 * a.2 = n ∧ n ≠ 0
⊢ a ∈ n.divisorsAntidiagonalList ↔ a.1 * a.2 = n ∧ n ≠ 0
have rw₂ : a.1 * a.2 = n ∧ n ≠ 0 ↔ a.1 * a.2 = n ∧ n ≠ 0
Tactic: rw [← List.mem_toFinset, toFinset_divisorsAntidiagonalList, mem_divisorsAntidiagonal]
-- Lean 4 proof step from Mathlib.NumberTheory.Divisors (hypothesis)
Goal:
n : ℕ
⊢ n.divisorsAntidiagonalList.reverse = List.map Prod.swap n.divisorsAntidiagonalList
have this : Std.Asymm fun (x1 x2 : ℕ × ℕ) ↦ x1.2 < x2.2
Tactic: have : Std.Asymm (α := ℕ × ℕ) (·.snd < ·.snd) := ⟨fun _ _ ↦ lt_asymm⟩
-- Lean 4 proof step from Mathlib.NumberTheory.Divisors (goal)
Goal:
n : ℕ
this : Std.Asymm fun (x1 x2 : ℕ × ℕ) ↦ x1.2 < x2.2
⊢ n.divisorsAntidiagonalList.reverse = List.map Prod.swap n.divisorsAntidiagonalList
have refine : n.divisorsAntidiagonalList.reverse.Perm (List.map Prod.swap n.divisorsAntidiagonalList)
Tactic: refine List.Perm.eq_of_pairwise' pairwise_divisorsAntidiagonalList_snd.reverse
    (pairwise_divisorsAntidiagonalList_fst.map _ fun _ _ ↦ id) ?_
-- Lean 4 proof step from Mathlib.NumberTheory.Divisors (hypothesis)
Goal:
n : ℕ
p : ℕ × ℕ
hp : p ∈ n.divisorsAntidiagonal
⊢ p.1 ≠ 0 ∧ p.2 ≠ 0
have hp₁ : p.1 * p.2 = n
Tactic: obtain ⟨hp₁, hp₂⟩ := Nat.mem_divisorsAntidiagonal.mp hp
-- Lean 4 proof step from Mathlib.NumberTheory.Divisors (hypothesis)
Goal:
n : ℕ
p : ℕ × ℕ
hp : p ∈ n.divisorsAntidiagonal
hp₁ : p.1 * p.2 = n
⊢ p.1 ≠ 0 ∧ p.2 ≠ 0
have hp₂ : n ≠ 0
Tactic: obtain ⟨hp₁, hp₂⟩ := Nat.mem_divisorsAntidiagonal.mp hp
-- Lean 4 proof step from Mathlib.NumberTheory.Divisors (goal)
Goal:
n m : ℕ
⊢ n ∈ m.divisors → n ≤ m
have zero : n ∈ divisors 0 → n ≤ 0
Tactic: rcases m with - | m
Cleared hypotheses: m
-- Lean 4 proof step from Mathlib.NumberTheory.Divisors (goal)
Goal:
n m : ℕ
zero : n ∈ divisors 0 → n ≤ 0
⊢ n ∈ m.divisors → n ≤ m
have succ : ∀ (m : ℕ), n ∈ (m + 1).divisors → n ≤ m + 1
Tactic: rcases m with - | m
Cleared hypotheses: m
-- Lean 4 proof step from Mathlib.NumberTheory.Divisors (goal)
Goal:
n m : ℕ
⊢ n ∈ (m + 1).divisors → n ≤ m + 1
have succ : n ∣ m + 1 → n ≤ m + 1
Tactic: simp only [mem_divisors, Nat.succ_ne_zero m, and_true, Ne, not_false_iff]
-- Lean 4 proof step from Mathlib.NumberTheory.Divisors (goal)
Goal:
n : ℕ
⊢ #n.divisors ≤ #(Ico 1 (n + 1))
have a : n.divisors ⊆ Ico 1 (n + 1)
Tactic: apply card_le_card
-- Lean 4 proof step from Mathlib.NumberTheory.Divisors (goal)
Goal:
n : ℕ
⊢ #(Ico 1 (n + 1)) = n
have rw : n + 1 - 1 = n
Tactic: rw [card_Ico, add_tsub_cancel_right]
-- Lean 4 proof step from Mathlib.NumberTheory.Divisors (goal)
Goal:
n : ℕ
rw : n + 1 - 1 = n
⊢ #(Ico 1 (n + 1)) = n
have rw₁ : n = n
Tactic: rw [card_Ico, add_tsub_cancel_right]
-- Lean 4 proof step from Mathlib.NumberTheory.Divisors (goal)
Goal:
n m : ℕ
hn : n ≠ 0
hm : m ∣ n
⊢ {d ∈ n.divisors | d ∣ m} = m.divisors
have h : ∀ (k : ℕ), k ∈ {d ∈ n.divisors | d ∣ m} ↔ k ∈ m.divisors
Tactic: ext k
-- Lean 4 proof step from Mathlib.NumberTheory.Divisors (goal)
Goal:
n m : ℕ
hn : n ≠ 0
hm : m ∣ n
k : ℕ
⊢ k ∈ {d ∈ n.divisors | d ∣ m} ↔ k ∈ m.divisors
have h : (k ∣ n ∧ n ≠ 0) ∧ k ∣ m ↔ k ∣ m ∧ m ≠ 0
Tactic: simp_rw [mem_filter, mem_divisors]
-- 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:
⊢ properDivisors 0 = ∅
have h : ∀ (a : ℕ), a ∈ properDivisors 0 ↔ Membership.mem (γ := Finset ℕ) ∅ a
Tactic: ext
-- Lean 4 proof step from Mathlib.NumberTheory.Divisors (goal)
Goal:
n : ℕ
⊢ n.divisors = ∅ ↔ n = 0
have contrapose! : n.divisors.Nonempty ↔ n ≠ 0
Tactic: contrapose!
-- Lean 4 proof step from Mathlib.NumberTheory.Divisors (goal)
Goal:
⊢ divisors 1 = {1}
have h : ∀ (a : ℕ), a ∈ divisors 1 ↔ Membership.mem (γ := Finset ℕ) {1} a
Tactic: ext
-- Lean 4 proof step from Mathlib.NumberTheory.Divisors (goal)
Goal:
⊢ properDivisors 1 = ∅
have rw : Eq (α := Finset ℕ) ({d ∈ Ico 1 1 | d ∣ 1}) ∅
Tactic: rw [properDivisors, Ico_self, filter_empty]
-- Lean 4 proof step from Mathlib.NumberTheory.Divisors (goal)
Goal:
rw : Eq (α := Finset ℕ) ({d ∈ Ico 1 1 | d ∣ 1}) ∅
⊢ properDivisors 1 = ∅
have rw₁ : Eq (α := Finset ℕ) ({d ∈ ∅ | d ∣ 1}) ∅
Tactic: rw [properDivisors, Ico_self, filter_empty]
-- Lean 4 proof step from Mathlib.NumberTheory.Divisors (goal)
Goal:
rw : Eq (α := Finset ℕ) ({d ∈ Ico 1 1 | d ∣ 1}) ∅
rw₁ : Eq (α := Finset ℕ) ({d ∈ ∅ | d ∣ 1}) ∅
⊢ properDivisors 1 = ∅
have rw₂ : Eq (α := Finset ℕ) ∅ ∅
Tactic: rw [properDivisors, Ico_self, filter_empty]
-- Lean 4 proof step from Mathlib.NumberTheory.Divisors (goal)
Goal:
n m : ℕ
h : m ∈ n.divisors
⊢ 0 < m
have zero : ∀ (h : 0 ∈ n.divisors), LT.lt (α := ℕ) 0 0
Tactic: cases m
Cleared hypotheses: m, h
-- Lean 4 proof step from Mathlib.NumberTheory.Divisors (goal)
Goal:
n m : ℕ
h : m ∈ n.divisors
zero : ∀ (h : 0 ∈ n.divisors), LT.lt (α := ℕ) 0 0
⊢ 0 < m
have succ : ∀ (n_1 : ℕ) (h : n_1 + 1 ∈ n.divisors), 0 < n_1 + 1
Tactic: cases m
Cleared hypotheses: m, h
-- Lean 4 proof step from Mathlib.NumberTheory.Divisors (hypothesis)
Goal:
n : ℕ
h : 0 ∈ n.divisors
⊢ LT.lt (α := ℕ) 0 0
have h₁ : n = 0 ∧ n ≠ 0
Tactic: rw [mem_divisors, zero_dvd_iff (a := n)] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.NumberTheory.Divisors (goal)
Goal:
n : ℕ
⊢ 1 ∈ n.properDivisors ↔ 1 < n
have rw : 1 ∣ n ∧ 1 < n ↔ 1 < n
Tactic: rw [mem_properDivisors, and_iff_right (one_dvd _)]
-- Lean 4 proof step from Mathlib.NumberTheory.Divisors (goal)
Goal:
n : ℕ
rw : 1 ∣ n ∧ 1 < n ↔ 1 < n
⊢ 1 ∈ n.properDivisors ↔ 1 < n
have rw₁ : 1 < n ↔ 1 < n
Tactic: rw [mem_properDivisors, and_iff_right (one_dvd _)]
-- Lean 4 proof step from Mathlib.NumberTheory.Divisors (goal)
Goal:
n : ℕ
⊢ n.divisors.sup id = n
have refine : n ≤ n.divisors.sup id
Tactic: refine le_antisymm (Finset.sup_le fun _ ↦ divisor_le) ?_
-- Lean 4 proof step from Mathlib.NumberTheory.Divisors (goal)
Goal:
n : ℕ
⊢ n ≤ n.divisors.sup id
have inl : 0 ≤ (divisors 0).sup id
Tactic: rcases Decidable.eq_or_ne n 0 with rfl | hn
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.NumberTheory.Divisors (goal)
Goal:
n : ℕ
inl : 0 ≤ (divisors 0).sup id
⊢ n ≤ n.divisors.sup id
have inr : ∀ (hn : n ≠ 0), n ≤ n.divisors.sup id
Tactic: rcases Decidable.eq_or_ne n 0 with rfl | hn
-- Lean 4 proof step from Mathlib.NumberTheory.Divisors (hypothesis)
Goal:
m n : ℕ
h : m ∈ n.properDivisors
⊢ 1 < n / m
have h_dvd : m ∣ n
Tactic: obtain ⟨h_dvd, h_lt⟩ := mem_properDivisors.mp h
-- Lean 4 proof step from Mathlib.NumberTheory.Divisors (hypothesis)
Goal:
m n : ℕ
h : m ∈ n.properDivisors
h_dvd : m ∣ n
⊢ 1 < n / m
have h_lt : m < n
Tactic: obtain ⟨h_dvd, h_lt⟩ := mem_properDivisors.mp h
-- Lean 4 proof step from Mathlib.NumberTheory.Divisors (goal)
Goal:
m n : ℕ
h : m ∈ n.properDivisors
h_dvd : m ∣ n
h_lt : m < n
⊢ 1 < n / m
have rwa : m * 1 < n
Tactic: rwa [Nat.lt_div_iff_mul_lt' h_dvd, mul_one]
-- Lean 4 proof step from Mathlib.NumberTheory.Divisors (goal)
Goal:
m n : ℕ
hn : n ≠ 0
⊢ m ∈ n.properDivisors ↔ ∃ k > 1, n = m * k
have refine_1 : ∀ (h : m ∈ n.properDivisors), n = m * (n / m)
Tactic: refine ⟨fun h ↦ ⟨n / m, one_lt_div_of_mem_properDivisors h, ?_⟩, ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.Divisors (goal)
Goal:
m n : ℕ
hn : n ≠ 0
refine_1 : ∀ (h : m ∈ n.properDivisors), n = m * (n / m)
⊢ m ∈ n.properDivisors ↔ ∃ k > 1, n = m * k
have refine_2 : (∃ k > 1, n = m * k) → m ∈ n.properDivisors
Tactic: refine ⟨fun h ↦ ⟨n / m, one_lt_div_of_mem_properDivisors h, ?_⟩, ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.Divisors (hypothesis)
Goal:
m k : ℕ
hk : k > 1
hn : m * k ≠ 0
⊢ m ∈ (m * k).properDivisors
have hn₁ : m ≠ 0 ∧ k ≠ 0
Tactic: rw [mul_ne_zero_iff] at hn
Cleared hypotheses: hn
-- Lean 4 proof step from Mathlib.NumberTheory.Divisors (goal)
Goal:
n : ℕ
⊢ n.properDivisors = ∅ ↔ n ≤ 1
have contrapose! : n.properDivisors.Nonempty ↔ 1 < n
Tactic: contrapose!
-- Lean 4 proof step from Mathlib.NumberTheory.Divisors (goal)
Goal:
⊢ divisorsAntidiagonal 0 = ∅
have h : ∀ (a : ℕ × ℕ), a ∈ divisorsAntidiagonal 0 ↔ Membership.mem (γ := Finset (ℕ × ℕ)) ∅ a
Tactic: ext
-- Lean 4 proof step from Mathlib.NumberTheory.Divisors (goal)
Goal:
⊢ divisorsAntidiagonal 1 = {(1, 1)}
have h : ∀ (a : ℕ × ℕ), a ∈ divisorsAntidiagonal 1 ↔ Membership.mem (γ := Finset (ℕ × ℕ)) {(1, 1)} a
Tactic: ext
-- Lean 4 proof step from Mathlib.NumberTheory.Divisors (goal)
Goal:
n : ℕ
x : ℕ × ℕ
⊢ x.swap ∈ n.divisorsAntidiagonal ↔ x ∈ n.divisorsAntidiagonal
have rw : x.swap.1 * x.swap.2 = n ∧ n ≠ 0 ↔ x ∈ n.divisorsAntidiagonal
Tactic: rw [mem_divisorsAntidiagonal, mem_divisorsAntidiagonal, mul_comm, Prod.swap]
-- Lean 4 proof step from Mathlib.NumberTheory.Divisors (goal)
Goal:
n : ℕ
x : ℕ × ℕ
rw : x.swap.1 * x.swap.2 = n ∧ n ≠ 0 ↔ x ∈ n.divisorsAntidiagonal
⊢ x.swap ∈ n.divisorsAntidiagonal ↔ x ∈ n.divisorsAntidiagonal
have rw₁ : x.swap.1 * x.swap.2 = n ∧ n ≠ 0 ↔ x.1 * x.2 = n ∧ n ≠ 0
Tactic: rw [mem_divisorsAntidiagonal, mem_divisorsAntidiagonal, mul_comm, Prod.swap]