awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.MahlerMeasure
Goal:
p : ℤ[X]
h : (map (castRingHom ℂ) p).mahlerMeasure = 1
z : ℂ
hz₀ : z ≠ 0
hz : z ∈ p.aroots ℂ
w : ℕ
left : 0 < w
hz_pow : z ^ w = 1
⊢ ∃ (n : ℕ), 0 < n ∧ IsPrimitiveRoot z n

Tactic:
exact IsPrimitiveRoot.exists_pos hz_pow (by omega)

Premises used: IsPrimitiveRoot.exists_pos
-- Module: Mathlib.NumberTheory.MahlerMeasure
Goal:
p : ℤ[X]
h : (map (castRingHom ℂ) p).mahlerMeasure = 1
hX : ¬X ∣ p
hpdeg rwa rwa₁ rwa₂ rwa₃ : p.degree ≠ 0
⊢ (map (castRingHom ℂ) p).degree ≠ 0

Tactic:
rwa [p.degree_map_eq_of_injective (castRingHom ℂ).injective_int]

Premises used: Polynomial.degree_map_eq_of_injective, Int.castRingHom, Complex, RingHom.injective_int
-- Module: Mathlib.NumberTheory.MahlerMeasure
Goal:
p : ℤ[X]
h : (map (castRingHom ℂ) p).mahlerMeasure = 1
hX : ¬X ∣ p
hpdeg : p.degree ≠ 0
⊢ (map (castRingHom ℂ) p).degree ≠ 0

Tactic:
have hpdegC : (p.map (castRingHom ℂ)).degree ≠ 0 := by
    rwa [p.degree_map_eq_of_injective (castRingHom ℂ).injective_int]
-- Module: Mathlib.NumberTheory.MahlerMeasure
Goal:
p : ℤ[X]
h : (map (castRingHom ℂ) p).mahlerMeasure = 1
hX : ¬X ∣ p
hpdeg : p.degree ≠ 0
hpdegC : (map (castRingHom ℂ) p).degree ≠ 0
obtain : ∀ (z : ℂ), eval z (map (castRingHom ℂ) p) = 0 → ∃ (n : ℕ), 0 < n ∧ cyclotomic n ℤ ∣ p
⊢ ∃ (n : ℕ), 0 < n ∧ cyclotomic n ℤ ∣ p

Tactic:
obtain ⟨z, _⟩ := Splits.exists_eval_eq_zero (IsAlgClosed.splits <| p.map (castRingHom ℂ))
    hpdegC

Premises used: Int.castRingHom, IsAlgClosed.splits, Polynomial.Splits.exists_eval_eq_zero, Polynomial.map, Complex
-- Module: Mathlib.NumberTheory.MahlerMeasure
Goal:
p : ℤ[X]
h : (map (castRingHom ℂ) p).mahlerMeasure = 1
hX : ¬X ∣ p
hpdeg : p.degree ≠ 0
hpdegC : (map (castRingHom ℂ) p).degree ≠ 0
z : ℂ
h_1 : eval z (map (castRingHom ℂ) p) = 0
contrapose : ∀ (hX : z = 0), X ∣ p
⊢ z ≠ 0

Tactic:
contrapose hX
-- Module: Mathlib.NumberTheory.MahlerMeasure
Goal:
p : ℤ[X]
h : (map (castRingHom ℂ) p).mahlerMeasure = 1
hpdeg : p.degree ≠ 0
hpdegC : (map (castRingHom ℂ) p).degree ≠ 0
z : ℂ
h_1 : eval z (map (castRingHom ℂ) p) = 0
hX : z = 0
⊢ X ∣ p

Tactic:
simp_all [X_dvd_iff, coeff_zero_eq_aeval_zero]

Premises used: Polynomial.coeff_zero_eq_aeval_zero, Polynomial.X_dvd_iff
-- Module: Mathlib.NumberTheory.MahlerMeasure
Goal:
p : ℤ[X]
h : (map (castRingHom ℂ) p).mahlerMeasure = 1
hX : ¬X ∣ p
hpdeg : p.degree ≠ 0
hpdegC : (map (castRingHom ℂ) p).degree ≠ 0
z : ℂ
h_1 : eval z (map (castRingHom ℂ) p) = 0
⊢ z ≠ 0

Tactic:
have hz₀ : z ≠ 0 := by
    contrapose hX
    simp_all [X_dvd_iff, coeff_zero_eq_aeval_zero]
-- Module: Mathlib.NumberTheory.MahlerMeasure
Goal:
p : ℤ[X]
h : (map (castRingHom ℂ) p).mahlerMeasure = 1
hX : ¬X ∣ p
hpdeg : p.degree ≠ 0
hpdegC : (map (castRingHom ℂ) p).degree ≠ 0
z : ℂ
h_1 : eval z (map (castRingHom ℂ) p) = 0
hz₀ : z ≠ 0
⊢ z ∈ p.aroots ℂ

Tactic:
aesop
-- Module: Mathlib.NumberTheory.MahlerMeasure
Goal:
p : ℤ[X]
h : (map (castRingHom ℂ) p).mahlerMeasure = 1
hX : ¬X ∣ p
hpdeg : p.degree ≠ 0
hpdegC : (map (castRingHom ℂ) p).degree ≠ 0
z : ℂ
h_1 : eval z (map (castRingHom ℂ) p) = 0
hz₀ : z ≠ 0
⊢ z ∈ p.aroots ℂ

Tactic:
have h_z_root : z ∈ p.aroots ℂ := by aesop
-- Module: Mathlib.NumberTheory.MahlerMeasure
Goal:
p : ℤ[X]
h : (map (castRingHom ℂ) p).mahlerMeasure = 1
hX : ¬X ∣ p
hpdeg : p.degree ≠ 0
hpdegC : (map (castRingHom ℂ) p).degree ≠ 0
z : ℂ
h_1 : eval z (map (castRingHom ℂ) p) = 0
hz₀ : z ≠ 0
h_z_root : z ∈ p.aroots ℂ
obtain : ∀ (m : ℕ) (h_m_pos : 0 < m) (h_prim : IsPrimitiveRoot z m), ∃ (n : ℕ), 0 < n ∧ cyclotomic n ℤ ∣ p
⊢ ∃ (n : ℕ), 0 < n ∧ cyclotomic n ℤ ∣ p

Tactic:
obtain ⟨m, h_m_pos, h_prim⟩ := isPrimitiveRoot_of_mahlerMeasure_eq_one h hz₀ h_z_root

Premises used: Polynomial.isPrimitiveRoot_of_mahlerMeasure_eq_one
-- Module: Mathlib.NumberTheory.MahlerMeasure
Goal:
p : ℤ[X]
h : (map (castRingHom ℂ) p).mahlerMeasure = 1
hX : ¬X ∣ p
hpdeg : p.degree ≠ 0
hpdegC : (map (castRingHom ℂ) p).degree ≠ 0
z : ℂ
h_1 : eval z (map (castRingHom ℂ) p) = 0
hz₀ : z ≠ 0
h_z_root : z ∈ p.aroots ℂ
m : ℕ
h_m_pos : 0 < m
h_prim : IsPrimitiveRoot z m
right : cyclotomic m ℤ ∣ p
⊢ ∃ (n : ℕ), 0 < n ∧ cyclotomic n ℤ ∣ p

Tactic:
use m, h_m_pos
-- Module: Mathlib.NumberTheory.MahlerMeasure
Goal:
p : ℤ[X]
h : (map (castRingHom ℂ) p).mahlerMeasure = 1
hX : ¬X ∣ p
hpdeg : p.degree ≠ 0
hpdegC : (map (castRingHom ℂ) p).degree ≠ 0
z : ℂ
h_1 : eval z (map (castRingHom ℂ) p) = 0
hz₀ : z ≠ 0
h_z_root : z ∈ p.aroots ℂ
m : ℕ
h_m_pos : 0 < m
h_prim : IsPrimitiveRoot z m
right : minpoly ℤ z ∣ p
⊢ cyclotomic m ℤ ∣ p

Tactic:
rw [cyclotomic_eq_minpoly h_prim h_m_pos]

Premises used: Polynomial.cyclotomic_eq_minpoly
-- Module: Mathlib.NumberTheory.MahlerMeasure
Goal:
p : ℤ[X]
h : (map (castRingHom ℂ) p).mahlerMeasure = 1
hX : ¬X ∣ p
hpdeg : p.degree ≠ 0
hpdegC : (map (castRingHom ℂ) p).degree ≠ 0
z : ℂ
h_1 : eval z (map (castRingHom ℂ) p) = 0
hz₀ : z ≠ 0
h_z_root : z ∈ p.aroots ℂ
m : ℕ
h_m_pos : 0 < m
h_prim : IsPrimitiveRoot z m
right : Eq (α := ℂ) ((aeval z : (a : ℤ[X]) → ℂ) p : ℂ) (0 : ℂ)
⊢ minpoly ℤ z ∣ p

Tactic:
apply minpoly.isIntegrallyClosed_dvd <| isIntegral_of_mahlerMeasure_eq_one h h_z_root

Premises used: minpoly.isIntegrallyClosed_dvd, Polynomial.isIntegral_of_mahlerMeasure_eq_one
-- Module: Mathlib.NumberTheory.MahlerMeasure
Goal:
p : ℤ[X]
h : (map (castRingHom ℂ) p).mahlerMeasure = 1
hX : ¬X ∣ p
hpdeg : p.degree ≠ 0
hpdegC : (map (castRingHom ℂ) p).degree ≠ 0
z : ℂ
h_1 : eval z (map (castRingHom ℂ) p) = 0
hz₀ : z ≠ 0
h_z_root : z ∈ p.aroots ℂ
m : ℕ
h_m_pos : 0 < m
h_prim : IsPrimitiveRoot z m
⊢ Eq (α := ℂ) ((aeval z : (a : ℤ[X]) → ℂ) p : ℂ) (0 : ℂ)

Tactic:
(mem_aroots.mp h_z_root).2

Premises used: And.right, Iff.mp, Polynomial.mem_aroots
-- Module: Mathlib.NumberTheory.MahlerMeasure
Goal:
p : ℤ[X]
h : (map (castRingHom ℂ) p).mahlerMeasure = 1
hX : ¬X ∣ p
hpdeg : p.degree ≠ 0
hpdegC : (map (castRingHom ℂ) p).degree ≠ 0
z : ℂ
h_1 : eval z (map (castRingHom ℂ) p) = 0
hz₀ : z ≠ 0
h_z_root : z ∈ p.aroots ℂ
m : ℕ
h_m_pos : 0 < m
h_prim : IsPrimitiveRoot z m
⊢ Eq (α := ℂ) ((aeval z : (a : ℤ[X]) → ℂ) p : ℂ) (0 : ℂ)

Tactic:
exact (mem_aroots.mp h_z_root).2

Premises used: And.right, Iff.mp, Polynomial.mem_aroots
-- Module: Mathlib.NumberTheory.MaricaSchoenheim
Goal:
n : ℕ
f : ℕ → ℕ
hf' : ∀ k < n, Squarefree (f k)
hn : n ≠ 0
hf : StrictMonoOn f (Set.Iio n)
by_contra! : ∀ (this : ∀ (i : ℕ) (_ : i < n) (j : ℕ) (_ : j < n), f i < (f i).gcd (f j) * n), False
⊢ ∃ i < n, ∃ j < n, (f i).gcd (f j) * n ≤ f i

Tactic:
by_contra!
-- Module: Mathlib.NumberTheory.MaricaSchoenheim
Goal:
n : ℕ
f : ℕ → ℕ
hf' : ∀ k < n, Squarefree (f k)
hn : n ≠ 0
hf : StrictMonoOn f (Set.Iio n)
this : ∀ (i : ℕ) (_ : i < n) (j : ℕ) (_ : j < n), f i < (f i).gcd (f j) * n
𝒜 : Finset (Finset ℕ) := image (fun (n : ℕ) ↦ (f n).primeFactors) (Iio n)
⊢ ∀ i < n, ∀ (j : ℕ), Squarefree (f i / (f i).gcd (f j))

Tactic:
have hf'' : ∀ i < n, ∀ j, Squarefree (f i / (f i).gcd (f j)) :=
    fun i hi j ↦ (hf' _ hi).squarefree_of_dvd <| div_dvd_of_dvd <| gcd_dvd_left _ _
-- Module: Mathlib.NumberTheory.MaricaSchoenheim
Goal:
n : ℕ
f : ℕ → ℕ
hf' : ∀ k < n, Squarefree (f k)
hn : n ≠ 0
hf : StrictMonoOn f (Set.Iio n)
this : ∀ (i : ℕ) (_ : i < n) (j : ℕ) (_ : j < n), f i < (f i).gcd (f j) * n
𝒜 : Finset (Finset ℕ) := image (fun (n : ℕ) ↦ (f n).primeFactors) (Iio n)
hf'' : ∀ i < n, ∀ (j : ℕ), Squarefree (f i / (f i).gcd (f j))
⊢ False

Tactic:
lt_irrefl n ?_

Premises used: lt_irrefl
-- Module: Mathlib.NumberTheory.MaricaSchoenheim
Goal:
n : ℕ
f : ℕ → ℕ
hf' : ∀ k < n, Squarefree (f k)
hn : n ≠ 0
hf : StrictMonoOn f (Set.Iio n)
this : ∀ (i : ℕ) (_ : i < n) (j : ℕ) (_ : j < n), f i < (f i).gcd (f j) * n
𝒜 : Finset (Finset ℕ) := image (fun (n : ℕ) ↦ (f n).primeFactors) (Iio n)
hf'' : ∀ i < n, ∀ (j : ℕ), Squarefree (f i / (f i).gcd (f j))
refine : n < n
⊢ False

Tactic:
refine lt_irrefl n ?_

Premises used: lt_irrefl
-- Module: Mathlib.NumberTheory.MaricaSchoenheim
Goal:
n : ℕ
f : ℕ → ℕ
hf' : ∀ k < n, Squarefree (f k)
hn : n ≠ 0
hf : StrictMonoOn f (Set.Iio n)
this : ∀ (i : ℕ) (_ : i < n) (j : ℕ) (_ : j < n), f i < (f i).gcd (f j) * n
𝒜 : Finset (Finset ℕ) := image (fun (n : ℕ) ↦ (f n).primeFactors) (Iio n)
hf'' : ∀ i < n, ∀ (j : ℕ), Squarefree (f i / (f i).gcd (f j))
⊢ n = #𝒜

Tactic:
?_
-- Module: Mathlib.NumberTheory.MaricaSchoenheim
Goal:
n : ℕ
f : ℕ → ℕ
hf' : ∀ k < n, Squarefree (f k)
hn : n ≠ 0
hf : StrictMonoOn f (Set.Iio n)
this : ∀ (i : ℕ) (_ : i < n) (j : ℕ) (_ : j < n), f i < (f i).gcd (f j) * n
𝒜 : Finset (Finset ℕ) := image (fun (n : ℕ) ↦ (f n).primeFactors) (Iio n)
hf'' : ∀ i < n, ∀ (j : ℕ), Squarefree (f i / (f i).gcd (f j))
⊢ #𝒜 ≤ #(𝒜 \\ 𝒜)

Tactic:
𝒜.card_le_card_diffs

Premises used: Finset.card_le_card_diffs
-- Module: Mathlib.NumberTheory.MaricaSchoenheim
Goal:
n : ℕ
f : ℕ → ℕ
hf' : ∀ k < n, Squarefree (f k)
hn : n ≠ 0
hf : StrictMonoOn f (Set.Iio n)
this : ∀ (i : ℕ) (_ : i < n) (j : ℕ) (_ : j < n), f i < (f i).gcd (f j) * n
𝒜 : Finset (Finset ℕ) := image (fun (n : ℕ) ↦ (f n).primeFactors) (Iio n)
hf'' : ∀ i < n, ∀ (j : ℕ), Squarefree (f i / (f i).gcd (f j))
⊢ #(𝒜 \\ 𝒜) ≤ #(Ioo 0 n)

Tactic:
card_le_card_of_injOn (fun s ↦ ∏ p ∈ s, p) ?_ ?_

Premises used: Finset.card_le_card_of_injOn, Finset.prod
-- Module: Mathlib.NumberTheory.MaricaSchoenheim
Goal:
n : ℕ
f : ℕ → ℕ
hf' : ∀ k < n, Squarefree (f k)
hn : n ≠ 0
hf : StrictMonoOn f (Set.Iio n)
this : ∀ (i : ℕ) (_ : i < n) (j : ℕ) (_ : j < n), f i < (f i).gcd (f j) * n
𝒜 : Finset (Finset ℕ) := image (fun (n : ℕ) ↦ (f n).primeFactors) (Iio n)
hf'' : ∀ i < n, ∀ (j : ℕ), Squarefree (f i / (f i).gcd (f j))
rw : n - 0 - 1 = n - 1
rw₁ rw₂ : n - 1 = n - 1
⊢ #(Ioo 0 n) = n - 1

Tactic:
rw [card_Ioo, tsub_zero]

Premises used: Nat.card_Ioo, tsub_zero
-- Module: Mathlib.NumberTheory.MaricaSchoenheim
Goal:
n : ℕ
f : ℕ → ℕ
hf' : ∀ k < n, Squarefree (f k)
hn : n ≠ 0
hf : StrictMonoOn f (Set.Iio n)
this : ∀ (i : ℕ) (_ : i < n) (j : ℕ) (_ : j < n), f i < (f i).gcd (f j) * n
𝒜 : Finset (Finset ℕ) := image (fun (n : ℕ) ↦ (f n).primeFactors) (Iio n)
hf'' : ∀ i < n, ∀ (j : ℕ), Squarefree (f i / (f i).gcd (f j))
⊢ n - 1 < n

Tactic:
tsub_lt_self hn.bot_lt zero_lt_one

Premises used: zero_lt_one, tsub_lt_self, Ne.bot_lt
-- Module: Mathlib.NumberTheory.MaricaSchoenheim
Goal:
n : ℕ
f : ℕ → ℕ
hf' : ∀ k < n, Squarefree (f k)
hn : n ≠ 0
hf : StrictMonoOn f (Set.Iio n)
this : ∀ (i : ℕ) (_ : i < n) (j : ℕ) (_ : j < n), f i < (f i).gcd (f j) * n
𝒜 : Finset (Finset ℕ) := image (fun (n : ℕ) ↦ (f n).primeFactors) (Iio n)
hf'' : ∀ i < n, ∀ (j : ℕ), Squarefree (f i / (f i).gcd (f j))
calc_1 : n = #𝒜
calc_2 : Set.MapsTo (fun (s : Finset ℕ) ↦ ∏ p ∈ s, p) (↑(𝒜 \\ 𝒜) : Set (Finset ℕ)) (↑(Ioo 0 n) : Set ℕ)
calc_3 : Set.InjOn (β := ℕ) (fun (s : Finset ℕ) ↦ ∏ p ∈ s, p) (↑(𝒜 \\ 𝒜) : Set (Finset ℕ))
⊢ n < n

Tactic:
calc
    n = #𝒜 := ?_
    _ ≤ #(𝒜 \\ 𝒜) := 𝒜.card_le_card_diffs
    _ ≤ #(Ioo 0 n) := card_le_card_of_injOn (fun s ↦ ∏ p ∈ s, p) ?_ ?_
    _ = n - 1 := by rw [card_Ioo, tsub_zero]
    _ < n := tsub_lt_self hn.bot_lt zero_lt_one

Premises used: Finset.diffs, Finset.card_le_card_of_injOn, Finset.card_le_card_diffs, Finset.prod, zero_lt_one, OfNat.ofNat, Finset.Ioo, tsub_lt_self, Ne.bot_lt
-- Module: Mathlib.NumberTheory.MaricaSchoenheim
Goal:
n : ℕ
f : ℕ → ℕ
hf' : ∀ k < n, Squarefree (f k)
hn : n ≠ 0
hf : StrictMonoOn f (Set.Iio n)
this : ∀ (i : ℕ) (_ : i < n) (j : ℕ) (_ : j < n), f i < (f i).gcd (f j) * n
𝒜 : Finset (Finset ℕ) := image (fun (n : ℕ) ↦ (f n).primeFactors) (Iio n)
hf'' : ∀ i < n, ∀ (j : ℕ), Squarefree (f i / (f i).gcd (f j))
calc_1 : Set.InjOn (β := Finset ℕ) (fun (n : ℕ) ↦ (f n).primeFactors) (↑(Iio n) : Set ℕ)
⊢ n = #𝒜

Tactic:
rw [Finset.card_image_of_injOn, card_Iio]

Premises used: Finset.card_image_of_injOn, Nat.card_Iio
-- Module: Mathlib.NumberTheory.MaricaSchoenheim
Goal:
n : ℕ
f : ℕ → ℕ
hf' : ∀ k < n, Squarefree (f k)
hn : n ≠ 0
hf : StrictMonoOn f (Set.Iio n)
this : ∀ (i : ℕ) (_ : i < n) (j : ℕ) (_ : j < n), f i < (f i).gcd (f j) * n
𝒜 : Finset (Finset ℕ) := image (fun (n : ℕ) ↦ (f n).primeFactors) (Iio n)
hf'' : ∀ i < n, ∀ (j : ℕ), Squarefree (f i / (f i).gcd (f j))
⊢ Set.InjOn (β := Finset ℕ) (fun (n : ℕ) ↦ (f n).primeFactors) (↑(Iio n) : Set ℕ)

Tactic:
simpa using prod_primeFactors_invOn_squarefree.2.injOn.comp hf.injOn hf'

Premises used: StrictMonoOn.injOn, Set.InjOn.comp, And.right, Nat.prod_primeFactors_invOn_squarefree, Set.LeftInvOn.injOn
-- Module: Mathlib.NumberTheory.MaricaSchoenheim
Goal:
n : ℕ
f : ℕ → ℕ
hf' : ∀ k < n, Squarefree (f k)
hn : n ≠ 0
hf : StrictMonoOn f (Set.Iio n)
this : ∀ (i : ℕ) (_ : i < n) (j : ℕ) (_ : j < n), f i < (f i).gcd (f j) * n
𝒜 : Finset (Finset ℕ) := image (fun (n : ℕ) ↦ (f n).primeFactors) (Iio n)
hf'' : ∀ i < n, ∀ (j : ℕ), Squarefree (f i / (f i).gcd (f j))
calc_2 :
  ∀ ⦃x : ℕ⦄,
    x < n →
      ∀ ⦃x_1 : ℕ⦄,
        x_1 < n →
          LT.lt (α := ℕ) 0 (∏ p ∈ (f x).primeFactors \ (f x_1).primeFactors, p) ∧
            ∏ p ∈ (f x).primeFactors \ (f x_1).primeFactors, p < n
⊢ Set.MapsTo (fun (s : Finset ℕ) ↦ ∏ p ∈ s, p) (↑(𝒜 \\ 𝒜) : Set (Finset ℕ)) (↑(Ioo 0 n) : Set ℕ)

Tactic:
simp only [𝒜, forall_mem_diffs, forall_mem_image, mem_Ioo, mem_Iio, Set.MapsTo, mem_coe]

Premises used: Finset.forall_mem_image, Finset.mem_Ioo, Finset.forall_mem_diffs, Set.MapsTo, Finset.mem_Iio, Finset.mem_coe
-- Module: Mathlib.NumberTheory.MaricaSchoenheim
Goal:
n : ℕ
f : ℕ → ℕ
hf' : ∀ k < n, Squarefree (f k)
hn : n ≠ 0
hf : StrictMonoOn f (Set.Iio n)
this : ∀ (i : ℕ) (_ : i < n) (j : ℕ) (_ : j < n), f i < (f i).gcd (f j) * n
𝒜 : Finset (Finset ℕ) := image (fun (n : ℕ) ↦ (f n).primeFactors) (Iio n)
hf'' : ∀ i < n, ∀ (j : ℕ), Squarefree (f i / (f i).gcd (f j))
i : ℕ
hi : i < n
j : ℕ
hj : j < n
calc_2 : 0 < f i / (f i).gcd (f j) ∧ f i / (f i).gcd (f j) < n
⊢ LT.lt (α := ℕ) 0 (∏ p ∈ (f i).primeFactors \ (f j).primeFactors, p) ∧
    ∏ p ∈ (f i).primeFactors \ (f j).primeFactors, p < n

Tactic:
rw [← primeFactors_div_gcd (hf' _ hi) (hf' _ hj).ne_zero,
      prod_primeFactors_of_squarefree <| hf'' _ hi _]

Premises used: Nat.prod_primeFactors_of_squarefree, Nat.primeFactors_div_gcd, Squarefree.ne_zero
-- Module: Mathlib.NumberTheory.MaricaSchoenheim
Goal:
n : ℕ
f : ℕ → ℕ
hf' : ∀ k < n, Squarefree (f k)
hn : n ≠ 0
hf : StrictMonoOn f (Set.Iio n)
this : ∀ (i : ℕ) (_ : i < n) (j : ℕ) (_ : j < n), f i < (f i).gcd (f j) * n
𝒜 : Finset (Finset ℕ) := image (fun (n : ℕ) ↦ (f n).primeFactors) (Iio n)
hf'' : ∀ i < n, ∀ (j : ℕ), Squarefree (f i / (f i).gcd (f j))
i : ℕ
hi : i < n
j : ℕ
hj : j < n
⊢ 0 < f i / (f i).gcd (f j) ∧ f i / (f i).gcd (f j) < n

Tactic:
⟨Nat.div_pos (gcd_le_left _ (hf' _ hi).ne_zero.bot_lt) <|
      Nat.gcd_pos_of_pos_left _ (hf' _ hi).ne_zero.bot_lt, Nat.div_lt_of_lt_mul <| this _ hi _ hj⟩

Premises used: Nat.gcd_pos_of_pos_left, Nat.div_lt_of_lt_mul, Squarefree.ne_zero, And.intro, Nat.div_pos, Ne.bot_lt, Nat.gcd_le_left
-- Module: Mathlib.NumberTheory.MaricaSchoenheim
Goal:
n : ℕ
f : ℕ → ℕ
hf' : ∀ k < n, Squarefree (f k)
hn : n ≠ 0
hf : StrictMonoOn f (Set.Iio n)
this : ∀ (i : ℕ) (_ : i < n) (j : ℕ) (_ : j < n), f i < (f i).gcd (f j) * n
𝒜 : Finset (Finset ℕ) := image (fun (n : ℕ) ↦ (f n).primeFactors) (Iio n)
hf'' : ∀ i < n, ∀ (j : ℕ), Squarefree (f i / (f i).gcd (f j))
i : ℕ
hi : i < n
j : ℕ
hj : j < n
⊢ 0 < f i / (f i).gcd (f j) ∧ f i / (f i).gcd (f j) < n

Tactic:
exact ⟨Nat.div_pos (gcd_le_left _ (hf' _ hi).ne_zero.bot_lt) <|
      Nat.gcd_pos_of_pos_left _ (hf' _ hi).ne_zero.bot_lt, Nat.div_lt_of_lt_mul <| this _ hi _ hj⟩
-- Module: Mathlib.NumberTheory.MaricaSchoenheim
Goal:
n : ℕ
f : ℕ → ℕ
hf' : ∀ k < n, Squarefree (f k)
hn : n ≠ 0
hf : StrictMonoOn f (Set.Iio n)
this : ∀ (i : ℕ) (_ : i < n) (j : ℕ) (_ : j < n), f i < (f i).gcd (f j) * n
𝒜 : Finset (Finset ℕ) := image (fun (n : ℕ) ↦ (f n).primeFactors) (Iio n)
hf'' : ∀ i < n, ∀ (j : ℕ), Squarefree (f i / (f i).gcd (f j))
calc_3 :
  ∀ ⦃x : ℕ⦄,
    x < n →
      ∀ ⦃x_1 : ℕ⦄,
        x_1 < n →
          ∀ ⦃x_2 : ℕ⦄,
            x_2 < n →
              ∀ ⦃x_3 : ℕ⦄,
                x_3 < n →
                  Eq (α := ℕ) (∏ p ∈ (f x).primeFactors \ (f x_1).primeFactors, p)
                      (∏ p ∈ (f x_2).primeFactors \ (f x_3).primeFactors, p) →
                    (f x).primeFactors \ (f x_1).primeFactors = (f x_2).primeFactors \ (f x_3).primeFactors
⊢ Set.InjOn (β := ℕ) (fun (s : Finset ℕ) ↦ ∏ p ∈ s, p) (↑(𝒜 \\ 𝒜) : Set (Finset ℕ))

Tactic:
simp only [𝒜, Set.InjOn, mem_coe, forall_mem_diffs, forall_mem_image, mem_Iio]

Premises used: Finset.forall_mem_image, Finset.forall_mem_diffs, Finset.mem_Iio, Set.InjOn, Finset.mem_coe
-- Module: Mathlib.NumberTheory.MaricaSchoenheim
Goal:
n : ℕ
f : ℕ → ℕ
hf' : ∀ k < n, Squarefree (f k)
hn : n ≠ 0
hf : StrictMonoOn f (Set.Iio n)
this : ∀ (i : ℕ) (_ : i < n) (j : ℕ) (_ : j < n), f i < (f i).gcd (f j) * n
𝒜 : Finset (Finset ℕ) := image (fun (n : ℕ) ↦ (f n).primeFactors) (Iio n)
hf'' : ∀ i < n, ∀ (j : ℕ), Squarefree (f i / (f i).gcd (f j))
a : ℕ
ha : a < n
b : ℕ
hb : b < n
c : ℕ
hc : c < n
d : ℕ
hd : d < n
calc_3 :
  f a / (f a).gcd (f b) = f c / (f c).gcd (f d) →
    (f a / (f a).gcd (f b)).primeFactors = (f c / (f c).gcd (f d)).primeFactors
⊢ Eq (α := ℕ) (∏ p ∈ (f a).primeFactors \ (f b).primeFactors, p) (∏ p ∈ (f c).primeFactors \ (f d).primeFactors, p) →
    (f a).primeFactors \ (f b).primeFactors = (f c).primeFactors \ (f d).primeFactors

Tactic:
rw [← primeFactors_div_gcd (hf' _ ha) (hf' _ hb).ne_zero, ← primeFactors_div_gcd
      (hf' _ hc) (hf' _ hd).ne_zero, prod_primeFactors_of_squarefree (hf'' _ ha _),
      prod_primeFactors_of_squarefree (hf'' _ hc _)]

Premises used: Nat.prod_primeFactors_of_squarefree, Nat.primeFactors_div_gcd, Squarefree.ne_zero
-- Module: Mathlib.NumberTheory.MaricaSchoenheim
Goal:
n : ℕ
f : ℕ → ℕ
hf' : ∀ k < n, Squarefree (f k)
hn : n ≠ 0
hf : StrictMonoOn f (Set.Iio n)
this : ∀ (i : ℕ) (_ : i < n) (j : ℕ) (_ : j < n), f i < (f i).gcd (f j) * n
𝒜 : Finset (Finset ℕ) := image (fun (n : ℕ) ↦ (f n).primeFactors) (Iio n)
hf'' : ∀ i < n, ∀ (j : ℕ), Squarefree (f i / (f i).gcd (f j))
a : ℕ
ha : a < n
b : ℕ
hb : b < n
c : ℕ
hc : c < n
d : ℕ
hd : d < n
h : f a / (f a).gcd (f b) = f c / (f c).gcd (f d)
calc_3 calc_3₁ : (f c / (f c).gcd (f d)).primeFactors = (f c / (f c).gcd (f d)).primeFactors
⊢ (f a / (f a).gcd (f b)).primeFactors = (f c / (f c).gcd (f d)).primeFactors

Tactic:
rw [h]
-- Module: Mathlib.NumberTheory.Modular
Goal:
R : Type u_1
inst : CommRing R
g : SL(2, R)
⊢ IsCoprime ((↑g : Matrix (Fin 2) (Fin 2) R) 1 0) ((↑g : Matrix (Fin 2) (Fin 2) R) 1 1)

Tactic:
isCoprime_row g 1

Premises used: Matrix.SpecialLinearGroup.isCoprime_row, OfNat.ofNat
-- Module: Mathlib.NumberTheory.Modular
Goal:
R : Type u_1
inst : CommRing R
cd : Fin 2 → R
b₀ a : R
gcd_eqn : b₀ * cd 0 + a * cd 1 = 1
A : Matrix (Fin (Nat.succ 0).succ) (Fin (Nat.succ 0).succ) R :=
  (of :
      (a : Fin (Nat.succ 0).succ → Fin (Nat.succ 0).succ → R) →
        Matrix (Fin (Nat.succ 0).succ) (Fin (Nat.succ 0).succ) R)
    ![![a, -b₀], cd]
⊢ b₀ * cd 0 + a * cd 1 = 1

Tactic:
gcd_eqn
-- Module: Mathlib.NumberTheory.Modular
Goal:
R : Type u_1
inst : CommRing R
cd : Fin 2 → R
b₀ a : R
gcd_eqn : b₀ * cd 0 + a * cd 1 = 1
A : Matrix (Fin (Nat.succ 0).succ) (Fin (Nat.succ 0).succ) R :=
  (of :
      (a : Fin (Nat.succ 0).succ → Fin (Nat.succ 0).succ → R) →
        Matrix (Fin (Nat.succ 0).succ) (Fin (Nat.succ 0).succ) R)
    ![![a, -b₀], cd]
h : A.det = b₀ * cd 0 + a * cd 1
⊢ A.det = 1

Tactic:
convert! gcd_eqn
-- Module: Mathlib.NumberTheory.Modular
Goal:
R : Type u_1
inst : CommRing R
cd : Fin 2 → R
b₀ a : R
gcd_eqn : b₀ * cd 0 + a * cd 1 = 1
A : Matrix (Fin (Nat.succ 0).succ) (Fin (Nat.succ 0).succ) R :=
  (of :
      (a : Fin (Nat.succ 0).succ → Fin (Nat.succ 0).succ → R) →
        Matrix (Fin (Nat.succ 0).succ) (Fin (Nat.succ 0).succ) R)
    ![![a, -b₀], cd]
h : A 0 0 * A 1 1 - A 0 1 * A 1 0 = b₀ * cd 0 + a * cd 1
⊢ A.det = b₀ * cd 0 + a * cd 1

Tactic:
rw [det_fin_two]

Premises used: Matrix.det_fin_two
-- Module: Mathlib.NumberTheory.Modular
Goal:
R : Type u_1
inst : CommRing R
cd : Fin 2 → R
b₀ a : R
gcd_eqn : b₀ * cd 0 + a * cd 1 = 1
A : Matrix (Fin (Nat.succ 0).succ) (Fin (Nat.succ 0).succ) R :=
  (of :
      (a : Fin (Nat.succ 0).succ → Fin (Nat.succ 0).succ → R) →
        Matrix (Fin (Nat.succ 0).succ) (Fin (Nat.succ 0).succ) R)
    ![![a, -b₀], cd]
⊢ a * cd 1 + b₀ * cd 0 = b₀ * cd 0 + a * cd 1

Tactic:
ring
-- Module: Mathlib.NumberTheory.Modular
Goal:
R : Type u_1
inst : CommRing R
cd : Fin 2 → R
b₀ a : R
gcd_eqn : b₀ * cd 0 + a * cd 1 = 1
A : Matrix (Fin (Nat.succ 0).succ) (Fin (Nat.succ 0).succ) R :=
  (of :
      (a : Fin (Nat.succ 0).succ → Fin (Nat.succ 0).succ → R) →
        Matrix (Fin (Nat.succ 0).succ) (Fin (Nat.succ 0).succ) R)
    ![![a, -b₀], cd]
⊢ A.det = 1

Tactic:
have det_A_1 : det A = 1 := by
    convert! gcd_eqn
    rw [det_fin_two]
    simp [A, (by ring : a * cd 1 + b₀ * cd 0 = b₀ * cd 0 + a * cd 1)]
-- Module: Mathlib.NumberTheory.Modular
Goal:
R : Type u_1
inst : CommRing R
cd : Fin 2 → R
b₀ a : R
gcd_eqn : b₀ * cd 0 + a * cd 1 = 1
A : Matrix (Fin (Nat.succ 0).succ) (Fin (Nat.succ 0).succ) R :=
  (of :
      (a : Fin (Nat.succ 0).succ → Fin (Nat.succ 0).succ → R) →
        Matrix (Fin (Nat.succ 0).succ) (Fin (Nat.succ 0).succ) R)
    ![![a, -b₀], cd]
det_A_1 : A.det = 1
⊢ Membership.mem (γ := Set (Fin 2 → R)) ((fun (g : SL(2, R)) ↦ (↑g : Matrix (Fin 2) (Fin 2) R) 1) '' Set.univ) cd

Tactic:
⟨⟨A, det_A_1⟩, Set.mem_univ _, ?_⟩

Premises used: Set.Mem, setOf, Subtype.mk, And.intro, Exists.intro, Set.mem_univ, Set.image
-- Module: Mathlib.NumberTheory.Modular
Goal:
R : Type u_1
inst : CommRing R
cd : Fin 2 → R
b₀ a : R
gcd_eqn : b₀ * cd 0 + a * cd 1 = 1
A : Matrix (Fin (Nat.succ 0).succ) (Fin (Nat.succ 0).succ) R :=
  (of :
      (a : Fin (Nat.succ 0).succ → Fin (Nat.succ 0).succ → R) →
        Matrix (Fin (Nat.succ 0).succ) (Fin (Nat.succ 0).succ) R)
    ![![a, -b₀], cd]
det_A_1 : A.det = 1
refine :
  (fun (g : SL(2, R)) ↦ (↑g : Matrix (Fin 2) (Fin 2) R) 1)
      (Subtype.mk (p := fun (A : Matrix (Fin 2) (Fin 2) R) ↦ A.det = 1) A det_A_1) =
    cd
⊢ Membership.mem (γ := Set (Fin 2 → R)) ((fun (g : SL(2, R)) ↦ (↑g : Matrix (Fin 2) (Fin 2) R) 1) '' Set.univ) cd

Tactic:
refine ⟨⟨A, det_A_1⟩, Set.mem_univ _, ?_⟩
-- Module: Mathlib.NumberTheory.Modular
Goal:
R : Type u_1
inst : CommRing R
cd : Fin 2 → R
b₀ a : R
gcd_eqn : b₀ * cd 0 + a * cd 1 = 1
A : Matrix (Fin (Nat.succ 0).succ) (Fin (Nat.succ 0).succ) R :=
  (of :
      (a : Fin (Nat.succ 0).succ → Fin (Nat.succ 0).succ → R) →
        Matrix (Fin (Nat.succ 0).succ) (Fin (Nat.succ 0).succ) R)
    ![![a, -b₀], cd]
det_A_1 : A.det = 1
h :
  ∀ (x : Fin 2),
    (fun (g : SL(2, R)) ↦ (↑g : Matrix (Fin 2) (Fin 2) R) 1)
        (Subtype.mk (p := fun (A : Matrix (Fin 2) (Fin 2) R) ↦ A.det = 1) A det_A_1) x =
      cd x
⊢ (fun (g : SL(2, R)) ↦ (↑g : Matrix (Fin 2) (Fin 2) R) 1)
      (Subtype.mk (p := fun (A : Matrix (Fin 2) (Fin 2) R) ↦ A.det = 1) A det_A_1) =
    cd

Tactic:
ext
-- Module: Mathlib.NumberTheory.Modular
Goal:
R : Type u_1
inst : CommRing R
cd : Fin 2 → R
b₀ a : R
gcd_eqn : b₀ * cd 0 + a * cd 1 = 1
A : Matrix (Fin (Nat.succ 0).succ) (Fin (Nat.succ 0).succ) R :=
  (of :
      (a : Fin (Nat.succ 0).succ → Fin (Nat.succ 0).succ → R) →
        Matrix (Fin (Nat.succ 0).succ) (Fin (Nat.succ 0).succ) R)
    ![![a, -b₀], cd]
det_A_1 : A.det = 1
x : Fin 2
⊢ (fun (g : SL(2, R)) ↦ (↑g : Matrix (Fin 2) (Fin 2) R) 1)
      (Subtype.mk (p := fun (A : Matrix (Fin 2) (Fin 2) R) ↦ A.det = 1) A det_A_1) x =
    cd x

Tactic:
simp [A]
-- Module: Mathlib.NumberTheory.Modular
Goal:
z : ℍ
this : Module ℝ (Fin 2 → ℝ) := NormedSpace.toModule
π₀ : (Fin 2 → ℝ) →ₗ[ℝ] ℝ := LinearMap.proj (φ := fun (a : Fin 2) ↦ ℝ) 0
π₁ : (Fin 2 → ℝ) →ₗ[ℝ] ℝ := LinearMap.proj (φ := fun (a : Fin 2) ↦ ℝ) 1
f : (Fin 2 → ℝ) →ₗ[ℝ] ℂ := HAdd.hAdd (α := (Fin 2 → ℝ) →ₗ[ℝ] ℂ) (π₀.smulRight (↑z : ℂ)) (π₁.smulRight 1)
h : ∀ (x : Fin 2 → ℝ), (f : (a : Fin 2 → ℝ) → ℂ) x = (↑(x 0) : ℂ) * (↑z : ℂ) + (↑(x 1) : ℂ)
⊢ Eq (α := (a : Fin 2 → ℝ) → ℂ) (⇑f : (a : Fin 2 → ℝ) → ℂ) fun (p : Fin 2 → ℝ) ↦ (↑(p 0) : ℂ) * (↑z : ℂ) + (↑(p 1) : ℂ)

Tactic:
ext1