awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.MahlerMeasure (hypothesis)
Goal:
p : ℤ[X]
h : (map (castRingHom ℂ) p).mahlerMeasure = 1
this : ‖(map (castRingHom ℂ) p).leadingCoeff‖ = 1
⊢ |p.leadingCoeff| = 1
have this₁ : norm (E := ℂ) (↑p.leadingCoeff : ℂ) = 1
Tactic: rw [leadingCoeff_map_of_injective (castRingHom ℂ).injective_int, eq_intCast] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.NumberTheory.MahlerMeasure (goal)
Goal:
p : ℤ[X]
h : (map (castRingHom ℂ) p).mahlerMeasure = 1
this : norm (E := ℂ) (↑p.leadingCoeff : ℂ) = 1
⊢ |p.leadingCoeff| = 1
have norm_cast : ∀ (this : |p.leadingCoeff| = 1), |p.leadingCoeff| = 1
Tactic: norm_cast at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.NumberTheory.MahlerMeasure (hypothesis)
Goal:
p : ℤ[X]
h : (map (castRingHom ℂ) p).mahlerMeasure = 1
z : ℂ
hz : z ∈ p.aroots ℂ
⊢ IsIntegral ℤ z
have this : p.leadingCoeff = 1 ∨ p.leadingCoeff = -1
Tactic: have : p.leadingCoeff = 1 ∨ p.leadingCoeff = -1 := abs_eq_abs.mp <|
    abs_leadingCoeff_eq_one_of_mahlerMeasure_eq_one h
-- Lean 4 proof step from Mathlib.NumberTheory.MahlerMeasure (hypothesis)
Goal:
p : ℤ[X]
h : (map (castRingHom ℂ) p).mahlerMeasure = 1
z : ℂ
hz : z ∈ p.aroots ℂ
this : p.leadingCoeff = 1 ∨ p.leadingCoeff = -1
⊢ IsIntegral ℤ z
have this₁ : (HMul.hMul (α := ℤ[X]) ((C : (a : ℤ) → ℤ[X]) (1 / p.leadingCoeff) : ℤ[X]) p).Monic
Tactic: have : (C (1 / p.leadingCoeff) * p).Monic := by aesop (add safe (by simp [Monic.def]))
-- Lean 4 proof step from Mathlib.NumberTheory.MahlerMeasure (goal)
Goal:
p : ℤ[X]
h : (map (castRingHom ℂ) p).mahlerMeasure = 1
z : ℂ
hz : z ∈ p.aroots ℂ
⊢ ‖z‖ ≤ 1
have max : LE.le (α := ℝ) (prod (Multiset.map (fun (a : ℂ) ↦ max 1 ‖a‖) (map (castRingHom ℂ) p).roots)) 1
Tactic: calc
  ‖z‖ ≤ max 1 ‖z‖ := le_max_right 1 ‖z‖
  _   ≤ ((p.map (castRingHom ℂ)).roots.map (fun a ↦ max 1 ‖a‖)).prod :=
        mem_le_prod_of_one_le (fun a ↦ le_max_left 1 ‖a‖) hz
  _   ≤ 1 := by grind [prod_max_one_norm_roots_le_mahlerMeasure_of_one_le_leadingCoeff,
        norm_leadingCoeff_eq_one_of_mahlerMeasure_eq_one]
-- Lean 4 proof step from Mathlib.NumberTheory.MahlerMeasure (goal)
Goal:
p : ℤ[X]
h : (map (castRingHom ℂ) p).mahlerMeasure = 1
z : ℂ
hz₀ : z ≠ 0
hz : z ∈ p.aroots ℂ
K : IntermediateField ℚ ℂ := ℚ⟮z⟯
this_1 : NumberField ↥K := ⋯
y : ↥K := Subtype.mk (p := fun (x : ℂ) ↦ x ∈ K) z ⋯
this : ∃ (n : ℕ) (_ : 0 < n), y ^ n = 1
⊢ ∃ (n : ℕ), 0 < n ∧ z ^ n = 1
have obtain : ∀ (n : ℕ) (hn₀ : 0 < n) (hn₁ : y ^ n = 1), ∃ (n : ℕ), 0 < n ∧ z ^ n = 1
Tactic: obtain ⟨n, hn₀, hn₁⟩ := this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.NumberTheory.MahlerMeasure (goal)
Goal:
p : ℤ[X]
h : (map (castRingHom ℂ) p).mahlerMeasure = 1
z : ℂ
hz₀ : z ≠ 0
hz : z ∈ p.aroots ℂ
K : IntermediateField ℚ ℂ := ℚ⟮z⟯
this : NumberField ↥K := ⋯
y : ↥K := Subtype.mk (p := fun (x : ℂ) ↦ x ∈ K) z ⋯
⊢ ∃ (n : ℕ), 0 < n ∧ z ^ n = 1
have suffices : ∃ (n : ℕ) (_ : 0 < n), y ^ n = 1
Tactic: suffices ∃ (n : ℕ) (_ : 0 < n), y ^ n = 1 by
    obtain ⟨n, hn₀, hn₁⟩ := this
    exact ⟨n, hn₀, congrArg (algebraMap K ℂ) hn₁⟩
-- Lean 4 proof step from Mathlib.NumberTheory.MahlerMeasure (goal)
Goal:
p : ℤ[X]
h : (map (castRingHom ℂ) p).mahlerMeasure = 1
z : ℂ
hz₀ : z ≠ 0
hz : z ∈ p.aroots ℂ
K : IntermediateField ℚ ℂ := ℚ⟮z⟯
this : NumberField ↥K := ⋯
y : ↥K := Subtype.mk (p := fun (x : ℂ) ↦ x ∈ K) z ⋯
⊢ ∃ (n : ℕ) (_ : 0 < n), y ^ n = 1
have refine : ∀ (φ : ↥K →+* ℂ), Membership.mem (α := ℂ) (p.aroots ℂ) ((φ : (a : ↥K) → ℂ) y : ℂ)
Tactic: refine NumberField.Embeddings.pow_eq_one_of_norm_le_one (x := y) K ℂ (Subtype.coe_ne_coe.mp hz₀)
    (coe_isIntegral_iff.mp <| isIntegral_of_mahlerMeasure_eq_one h hz)
    fun φ ↦ norm_root_le_one_of_mahlerMeasure_eq_one h ?_
-- Lean 4 proof step from Mathlib.NumberTheory.MahlerMeasure (goal)
Goal:
p : ℤ[X]
h : (map (castRingHom ℂ) p).mahlerMeasure = 1
z : ℂ
hz₀ : z ≠ 0
hz : z ∈ p.aroots ℂ
K : IntermediateField ℚ ℂ := ℚ⟮z⟯
this : NumberField ↥K := ⋯
y : ↥K := Subtype.mk (p := fun (x : ℂ) ↦ x ∈ K) z ⋯
φ : ↥K →+* ℂ
⊢ Membership.mem (α := ℂ) (p.aroots ℂ) ((φ : (a : ↥K) → ℂ) y : ℂ)
have rw : ∀ (hz : p ≠ 0 ∧ Eq (α := ℂ) ((aeval z : (a : ℤ[X]) → ℂ) p : ℂ) (0 : ℂ)),
  let K : IntermediateField ℚ ℂ := ℚ⟮z⟯;
  let y : ↥K := Subtype.mk (p := fun (x : ℂ) ↦ x ∈ K) z sorry;
  ∀ (φ : ↥K →+* ℂ), p ≠ 0 ∧ Eq (α := ℂ) (((aeval ((φ : (a : ↥K) → ℂ) y) : ℤ[X] →ₐ[ℤ] ℂ) : (a : ℤ[X]) → ℂ) p : ℂ) (0 : ℂ)
Tactic: rw [mem_aroots] at hz ⊢
Cleared hypotheses: K, this, y, φ
-- Lean 4 proof step from Mathlib.NumberTheory.MahlerMeasure (goal)
Goal:
p : ℤ[X]
h : (map (castRingHom ℂ) p).mahlerMeasure = 1
z : ℂ
hz₀ : z ≠ 0
hz_1 : z ∈ p.aroots ℂ
hz : p ≠ 0 ∧ Eq (α := ℂ) ((aeval z : (a : ℤ[X]) → ℂ) p : ℂ) (0 : ℂ)
K : IntermediateField ℚ ℂ := ℚ⟮z⟯
this : NumberField ↥K := ⋯
y : ↥K := Subtype.mk (p := fun (x : ℂ) ↦ x ∈ K) z ⋯
φ : ↥K →+* ℂ
⊢ p ≠ 0 ∧ Eq (α := ℂ) (((aeval ((φ : (a : ↥K) → ℂ) y) : ℤ[X] →ₐ[ℤ] ℂ) : (a : ℤ[X]) → ℂ) p : ℂ) (0 : ℂ)
have refine : Eq (α := ℂ) (((aeval ((φ : (a : ↥K) → ℂ) y) : ℤ[X] →ₐ[ℤ] ℂ) : (a : ℤ[X]) → ℂ) p : ℂ) (0 : ℂ)
Tactic: refine ⟨hz.1, ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.MahlerMeasure (goal)
Goal:
p : ℤ[X]
h : (map (castRingHom ℂ) p).mahlerMeasure = 1
z : ℂ
hz₀ : z ≠ 0
hz_1 : z ∈ p.aroots ℂ
hz : p ≠ 0 ∧ Eq (α := ℂ) ((aeval z : (a : ℤ[X]) → ℂ) p : ℂ) (0 : ℂ)
K : IntermediateField ℚ ℂ := ℚ⟮z⟯
this : NumberField ↥K := ⋯
y : ↥K := Subtype.mk (p := fun (x : ℂ) ↦ x ∈ K) z ⋯
φ : ↥K →+* ℂ
ψ : ↥K →+* ℂ
| (((aeval ((ψ : (a : ↥K) → ℂ) y) : ℤ[X] →ₐ[ℤ] ℂ) : (a : ℤ[X]) → ℂ) p : ℂ)
have rw : (((aeval ((ψ : (a : ↥K) → ℂ) y) : ℤ[X] →ₐ[ℤ] ℂ) : (a : ℤ[X]) → ℂ) (map (RingHom.id ℤ) p) : ℂ)
Tactic: rw [← map_id (p := p)]
-- Lean 4 proof step from Mathlib.NumberTheory.MahlerMeasure (goal)
Goal:
p : ℤ[X]
h : (map (castRingHom ℂ) p).mahlerMeasure = 1
z : ℂ
hz₀ : z ≠ 0
hz_1 : z ∈ p.aroots ℂ
hz : p ≠ 0 ∧ Eq (α := ℂ) ((aeval z : (a : ℤ[X]) → ℂ) p : ℂ) (0 : ℂ)
K : IntermediateField ℚ ℂ := ℚ⟮z⟯
this : NumberField ↥K := ⋯
y : ↥K := Subtype.mk (p := fun (x : ℂ) ↦ x ∈ K) z ⋯
φ : ↥K →+* ℂ
ψ : ↥K →+* ℂ
⊢ Eq (α := ℂ) ((ψ : (a : ↥K) → ℂ) ((aeval y : (a : ℤ[X]) → ↥K) p : ↥K) : ℂ)
    (((aeval ((ψ : (a : ↥K) → ℂ) y) : ℤ[X] →ₐ[ℤ] ℂ) : (a : ℤ[X]) → ℂ) p : ℂ)
have conv_rhs : Eq (α := ℂ) ((ψ : (a : ↥K) → ℂ) ((aeval y : (a : ℤ[X]) → ↥K) p : ↥K) : ℂ)
  (((aeval ((ψ : (a : ↥K) → ℂ) y) : ℤ[X] →ₐ[ℤ] ℂ) : (a : ℤ[X]) → ℂ) (map (RingHom.id ℤ) p) : ℂ)
Tactic: conv_rhs => rw [← map_id (p := p)]
-- Lean 4 proof step from Mathlib.NumberTheory.MahlerMeasure (goal)
Goal:
p : ℤ[X]
h : (map (castRingHom ℂ) p).mahlerMeasure = 1
z : ℂ
hz₀ : z ≠ 0
hz_1 : z ∈ p.aroots ℂ
hz : p ≠ 0 ∧ Eq (α := ℂ) ((aeval z : (a : ℤ[X]) → ℂ) p : ℂ) (0 : ℂ)
K : IntermediateField ℚ ℂ := ℚ⟮z⟯
this : NumberField ↥K := ⋯
y : ↥K := Subtype.mk (p := fun (x : ℂ) ↦ x ∈ K) z ⋯
φ : ↥K →+* ℂ
ψ : ↥K →+* ℂ
⊢ RingHom.comp (algebraMap ℤ ℂ) (RingHom.id ℤ) = ψ.comp (algebraMap ℤ ↥K)
have a : ∀ (x : ℤ),
  Eq (α := ℂ) ((RingHom.comp (algebraMap ℤ ℂ) (RingHom.id ℤ) : (a : ℤ) → ℂ) x : ℂ)
    ((ψ.comp (algebraMap ℤ ↥K) : (a : ℤ) → ℂ) x : ℂ)
Tactic: ext
-- Lean 4 proof step from Mathlib.NumberTheory.MahlerMeasure (hypothesis)
Goal:
p : ℤ[X]
h : (map (castRingHom ℂ) p).mahlerMeasure = 1
z : ℂ
hz₀ : z ≠ 0
hz_1 : z ∈ p.aroots ℂ
hz : p ≠ 0 ∧ Eq (α := ℂ) ((aeval z : (a : ℤ[X]) → ℂ) p : ℂ) (0 : ℂ)
K : IntermediateField ℚ ℂ := ℚ⟮z⟯
this : NumberField ↥K := ⋯
y : ↥K := Subtype.mk (p := fun (x : ℂ) ↦ x ∈ K) z ⋯
φ : ↥K →+* ℂ
⊢ Eq (α := ℂ) (((aeval ((φ : (a : ↥K) → ℂ) y) : ℤ[X] →ₐ[ℤ] ℂ) : (a : ℤ[X]) → ℂ) p : ℂ) (0 : ℂ)
have H : ∀ (ψ : ↥K →+* ℂ),
  Eq (α := ℂ) ((ψ : (a : ↥K) → ℂ) ((aeval y : (a : ℤ[X]) → ↥K) p : ↥K) : ℂ)
    (((aeval ((ψ : (a : ↥K) → ℂ) y) : ℤ[X] →ₐ[ℤ] ℂ) : (a : ℤ[X]) → ℂ) p : ℂ)
Tactic: have H (ψ : K →+* ℂ) : ψ ((aeval y) p) = (aeval (ψ y)) p := by
    conv_rhs => rw [← map_id (p := p)]
    exact p.map_aeval_eq_aeval_map (by ext; simp) y
-- Lean 4 proof step from Mathlib.NumberTheory.MahlerMeasure (goal)
Goal:
p : ℤ[X]
h : (map (castRingHom ℂ) p).mahlerMeasure = 1
z : ℂ
hz₀ : z ≠ 0
hz_1 : z ∈ p.aroots ℂ
hz : p ≠ 0 ∧ Eq (α := ℂ) ((aeval z : (a : ℤ[X]) → ℂ) p : ℂ) (0 : ℂ)
K : IntermediateField ℚ ℂ := ℚ⟮z⟯
this : NumberField ↥K := ⋯
y : ↥K := Subtype.mk (p := fun (x : ℂ) ↦ x ∈ K) z ⋯
φ : ↥K →+* ℂ
H :
  ∀ (ψ : ↥K →+* ℂ),
    Eq (α := ℂ) ((ψ : (a : ↥K) → ℂ) ((aeval y : (a : ℤ[X]) → ↥K) p : ↥K) : ℂ)
      (((aeval ((ψ : (a : ↥K) → ℂ) y) : ℤ[X] →ₐ[ℤ] ℂ) : (a : ℤ[X]) → ℂ) p : ℂ)
⊢ Eq (α := ℂ) (((aeval ((φ : (a : ↥K) → ℂ) y) : ℤ[X] →ₐ[ℤ] ℂ) : (a : ℤ[X]) → ℂ) p : ℂ) (0 : ℂ)
have rw : Eq (α := ℂ) (((aeval ((algebraMap ↥K ℂ : (a : ↥K) → ℂ) y) : ℤ[X] →ₐ[ℤ] ℂ) : (a : ℤ[X]) → ℂ) p : ℂ) (0 : ℂ)
Tactic: rw [← H, map_eq_zero_iff _ φ.injective,
    ← map_eq_zero_iff _ (FaithfulSMul.algebraMap_injective ↥K ℂ), H]
-- Lean 4 proof step from Mathlib.NumberTheory.MahlerMeasure (goal)
Goal:
p : ℤ[X]
h : (map (castRingHom ℂ) p).mahlerMeasure = 1
z : ℂ
hz₀ : z ≠ 0
hz : z ∈ p.aroots ℂ
⊢ ∃ (n : ℕ), 0 < n ∧ IsPrimitiveRoot z n
have obtain : ∀ (w : ℕ), 0 < w → ∀ (hz_pow : z ^ w = 1), ∃ (n : ℕ), 0 < n ∧ IsPrimitiveRoot z n
Tactic: obtain ⟨_, _, hz_pow⟩ := pow_eq_one_of_mahlerMeasure_eq_one h hz₀ hz
-- Lean 4 proof step from Mathlib.NumberTheory.MahlerMeasure (hypothesis)
Goal:
p : ℤ[X]
h : (map (castRingHom ℂ) p).mahlerMeasure = 1
hX : ¬X ∣ p
hpdeg : p.degree ≠ 0
⊢ ∃ (n : ℕ), 0 < n ∧ cyclotomic n ℤ ∣ p
have hpdegC : (map (castRingHom ℂ) p).degree ≠ 0
Tactic: have hpdegC : (p.map (castRingHom ℂ)).degree ≠ 0 := by
    rwa [p.degree_map_eq_of_injective (castRingHom ℂ).injective_int]
-- Lean 4 proof step from Mathlib.NumberTheory.MahlerMeasure (goal)
Goal:
p : ℤ[X]
h : (map (castRingHom ℂ) p).mahlerMeasure = 1
hX : ¬X ∣ p
hpdeg : p.degree ≠ 0
hpdegC : (map (castRingHom ℂ) p).degree ≠ 0
⊢ ∃ (n : ℕ), 0 < n ∧ cyclotomic n ℤ ∣ p
have obtain : ∀ (z : ℂ), eval z (map (castRingHom ℂ) p) = 0 → ∃ (n : ℕ), 0 < n ∧ cyclotomic n ℤ ∣ p
Tactic: obtain ⟨z, _⟩ := Splits.exists_eval_eq_zero (IsAlgClosed.splits <| p.map (castRingHom ℂ))
    hpdegC
-- Lean 4 proof step from Mathlib.NumberTheory.MahlerMeasure (goal)
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
have contrapose : ∀ (hX : z = 0), X ∣ p
Tactic: contrapose hX
Cleared hypotheses: hX
-- Lean 4 proof step from Mathlib.NumberTheory.MahlerMeasure (hypothesis)
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
⊢ ∃ (n : ℕ), 0 < n ∧ cyclotomic n ℤ ∣ p
have hz₀ : z ≠ 0
Tactic: have hz₀ : z ≠ 0 := by
    contrapose hX
    simp_all [X_dvd_iff, coeff_zero_eq_aeval_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.MahlerMeasure (hypothesis)
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
⊢ ∃ (n : ℕ), 0 < n ∧ cyclotomic n ℤ ∣ p
have h_z_root : z ∈ p.aroots ℂ
Tactic: have h_z_root : z ∈ p.aroots ℂ := by aesop
-- Lean 4 proof step from Mathlib.NumberTheory.MahlerMeasure (goal)
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 ℂ
⊢ ∃ (n : ℕ), 0 < n ∧ cyclotomic n ℤ ∣ p
have obtain : ∀ (m : ℕ) (h_m_pos : 0 < m) (h_prim : IsPrimitiveRoot z m), ∃ (n : ℕ), 0 < n ∧ cyclotomic n ℤ ∣ p
Tactic: obtain ⟨m, h_m_pos, h_prim⟩ := isPrimitiveRoot_of_mahlerMeasure_eq_one h hz₀ h_z_root
-- Lean 4 proof step from Mathlib.NumberTheory.MahlerMeasure (goal)
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
⊢ ∃ (n : ℕ), 0 < n ∧ cyclotomic n ℤ ∣ p
have right : cyclotomic m ℤ ∣ p
Tactic: use m, h_m_pos
-- Lean 4 proof step from Mathlib.NumberTheory.MahlerMeasure (goal)
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
⊢ cyclotomic m ℤ ∣ p
have right : minpoly ℤ z ∣ p
Tactic: rw [cyclotomic_eq_minpoly h_prim h_m_pos]
-- Lean 4 proof step from Mathlib.NumberTheory.MahlerMeasure (goal)
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
⊢ minpoly ℤ z ∣ p
have right : Eq (α := ℂ) ((aeval z : (a : ℤ[X]) → ℂ) p : ℂ) (0 : ℂ)
Tactic: apply minpoly.isIntegrallyClosed_dvd <| isIntegral_of_mahlerMeasure_eq_one h h_z_root
-- Lean 4 proof step from Mathlib.NumberTheory.MaricaSchoenheim (goal)
Goal:
n : ℕ
f : ℕ → ℕ
hf' : ∀ k < n, Squarefree (f k)
hn : n ≠ 0
hf : StrictMonoOn f (Set.Iio n)
⊢ ∃ i < n, ∃ j < n, (f i).gcd (f j) * n ≤ f i
have by_contra! : ∀ (this : ∀ (i : ℕ) (_ : i < n) (j : ℕ) (_ : j < n), f i < (f i).gcd (f j) * n), False
Tactic: by_contra!
-- Lean 4 proof step from Mathlib.NumberTheory.MaricaSchoenheim (hypothesis)
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)
⊢ False
have hf'' : ∀ 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 _ _
-- Lean 4 proof step from Mathlib.NumberTheory.MaricaSchoenheim (goal)
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
have refine : n < n
Tactic: refine lt_irrefl n ?_
-- Lean 4 proof step from Mathlib.NumberTheory.MaricaSchoenheim (goal)
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) = n - 1
have rw : n - 0 - 1 = n - 1
Tactic: rw [card_Ioo, tsub_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.MaricaSchoenheim (goal)
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
⊢ #(Ioo 0 n) = n - 1
have rw₁ : n - 1 = n - 1
Tactic: rw [card_Ioo, tsub_zero]
-- Lean 4 proof step from Mathlib.NumberTheory.MaricaSchoenheim (goal)
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 < n
have calc_1 : 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
-- Lean 4 proof step from Mathlib.NumberTheory.MaricaSchoenheim (goal)
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 = #𝒜
⊢ n < n
have calc_2 : Set.MapsTo (fun (s : Finset ℕ) ↦ ∏ p ∈ s, p) (↑(𝒜 \\ 𝒜) : Set (Finset ℕ)) (↑(Ioo 0 n) : Set ℕ)
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
-- Lean 4 proof step from Mathlib.NumberTheory.MaricaSchoenheim (goal)
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 ℕ)
⊢ n < n
have calc_3 : Set.InjOn (β := ℕ) (fun (s : Finset ℕ) ↦ ∏ p ∈ s, p) (↑(𝒜 \\ 𝒜) : Set (Finset ℕ))
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
-- Lean 4 proof step from Mathlib.NumberTheory.MaricaSchoenheim (goal)
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 = #𝒜
have calc_1 : Set.InjOn (β := Finset ℕ) (fun (n : ℕ) ↦ (f n).primeFactors) (↑(Iio n) : Set ℕ)
Tactic: rw [Finset.card_image_of_injOn, card_Iio]
-- Lean 4 proof step from Mathlib.NumberTheory.MaricaSchoenheim (goal)
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.MapsTo (fun (s : Finset ℕ) ↦ ∏ p ∈ s, p) (↑(𝒜 \\ 𝒜) : Set (Finset ℕ)) (↑(Ioo 0 n) : Set ℕ)
have 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
Tactic: simp only [𝒜, forall_mem_diffs, forall_mem_image, mem_Ioo, mem_Iio, Set.MapsTo, mem_coe]
-- Lean 4 proof step from Mathlib.NumberTheory.MaricaSchoenheim (goal)
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
⊢ LT.lt (α := ℕ) 0 (∏ p ∈ (f i).primeFactors \ (f j).primeFactors, p) ∧
    ∏ p ∈ (f i).primeFactors \ (f j).primeFactors, p < n
have calc_2 : 0 < f i / (f i).gcd (f j) ∧ f i / (f i).gcd (f j) < n
Tactic: rw [← primeFactors_div_gcd (hf' _ hi) (hf' _ hj).ne_zero,
      prod_primeFactors_of_squarefree <| hf'' _ hi _]
-- Lean 4 proof step from Mathlib.NumberTheory.MaricaSchoenheim (goal)
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 (β := ℕ) (fun (s : Finset ℕ) ↦ ∏ p ∈ s, p) (↑(𝒜 \\ 𝒜) : Set (Finset ℕ))
have 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
Tactic: simp only [𝒜, Set.InjOn, mem_coe, forall_mem_diffs, forall_mem_image, mem_Iio]
-- Lean 4 proof step from Mathlib.NumberTheory.MaricaSchoenheim (goal)
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
⊢ 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
have 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
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 _)]
-- Lean 4 proof step from Mathlib.NumberTheory.MaricaSchoenheim (goal)
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)
⊢ (f a / (f a).gcd (f b)).primeFactors = (f c / (f c).gcd (f d)).primeFactors
have calc_3 : (f c / (f c).gcd (f d)).primeFactors = (f c / (f c).gcd (f d)).primeFactors
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
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
have h : A.det = b₀ * cd 0 + a * cd 1
Tactic: convert! gcd_eqn
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (goal)
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 = b₀ * cd 0 + a * cd 1
have h : A 0 0 * A 1 1 - A 0 1 * A 1 0 = b₀ * cd 0 + a * cd 1
Tactic: rw [det_fin_two]
-- Lean 4 proof step from Mathlib.NumberTheory.Modular (hypothesis)
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]
⊢ Membership.mem (γ := Set (Fin 2 → R)) ((fun (g : SL(2, R)) ↦ (↑g : Matrix (Fin 2) (Fin 2) R) 1) '' Set.univ) cd
have det_A_1 : 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)]