awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Idempotents (goal)
Goal:
R : Type u_1
e_1 : R
I : Type u_2
inst : Fintype I
e : I → R
inst_1 : Semiring R
he : CompleteOrthogonalIdempotents e
hc : ∀ (i : I), IsMulCentral (e i)
r : R
simp_rw simp_rw₁ : ∑ x : I, e x * r * e x = r
⊢ (fun (r : (i : I) → ⋯.Corner) ↦ (∑ i : I, (↑(r i) : R) : R))
      ((fun (r : R) (i : I) ↦
          Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Subsemigroup R) (Subsemigroup.corner (e i)) x)
            ((fun (x : R) ↦ e i * x * e i) r) ⋯)
        r) =
    r
have simp_rw₂ : ∑ x : I, r * e x * e x = r
Tactic: simp_rw [((hc _).comm _).eq, mul_assoc, (he.idem _).eq, ← Finset.mul_sum, he.complete, mul_one]
-- Lean 4 proof step from Mathlib.RingTheory.Idempotents (goal)
Goal:
R : Type u_1
e_1 : R
I : Type u_2
inst : Fintype I
e : I → R
inst_1 : Semiring R
he : CompleteOrthogonalIdempotents e
hc : ∀ (i : I), IsMulCentral (e i)
r : R
simp_rw simp_rw₁ : ∑ x : I, e x * r * e x = r
simp_rw₂ : ∑ x : I, r * e x * e x = r
⊢ (fun (r : (i : I) → ⋯.Corner) ↦ (∑ i : I, (↑(r i) : R) : R))
      ((fun (r : R) (i : I) ↦
          Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Subsemigroup R) (Subsemigroup.corner (e i)) x)
            ((fun (x : R) ↦ e i * x * e i) r) ⋯)
        r) =
    r
have simp_rw₃ : ∑ x : I, r * (e x * e x) = r
Tactic: simp_rw [((hc _).comm _).eq, mul_assoc, (he.idem _).eq, ← Finset.mul_sum, he.complete, mul_one]
-- Lean 4 proof step from Mathlib.RingTheory.Idempotents (goal)
Goal:
R : Type u_1
e_1 : R
I : Type u_2
inst : Fintype I
e : I → R
inst_1 : Semiring R
he : CompleteOrthogonalIdempotents e
hc : ∀ (i : I), IsMulCentral (e i)
r : R
simp_rw simp_rw₁ : ∑ x : I, e x * r * e x = r
simp_rw₂ : ∑ x : I, r * e x * e x = r
simp_rw₃ : ∑ x : I, r * (e x * e x) = r
⊢ (fun (r : (i : I) → ⋯.Corner) ↦ (∑ i : I, (↑(r i) : R) : R))
      ((fun (r : R) (i : I) ↦
          Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Subsemigroup R) (Subsemigroup.corner (e i)) x)
            ((fun (x : R) ↦ e i * x * e i) r) ⋯)
        r) =
    r
have simp_rw₄ : ∑ x : I, r * e x = r
Tactic: simp_rw [((hc _).comm _).eq, mul_assoc, (he.idem _).eq, ← Finset.mul_sum, he.complete, mul_one]
-- Lean 4 proof step from Mathlib.RingTheory.Idempotents (goal)
Goal:
R : Type u_1
e_1 : R
I : Type u_2
inst : Fintype I
e : I → R
inst_1 : Semiring R
he : CompleteOrthogonalIdempotents e
hc : ∀ (i : I), IsMulCentral (e i)
r : R
simp_rw simp_rw₁ : ∑ x : I, e x * r * e x = r
simp_rw₂ : ∑ x : I, r * e x * e x = r
simp_rw₃ : ∑ x : I, r * (e x * e x) = r
simp_rw₄ : ∑ x : I, r * e x = r
⊢ (fun (r : (i : I) → ⋯.Corner) ↦ (∑ i : I, (↑(r i) : R) : R))
      ((fun (r : R) (i : I) ↦
          Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Subsemigroup R) (Subsemigroup.corner (e i)) x)
            ((fun (x : R) ↦ e i * x * e i) r) ⋯)
        r) =
    r
have simp_rw₅ : r * ∑ i : I, e i = r
Tactic: simp_rw [((hc _).comm _).eq, mul_assoc, (he.idem _).eq, ← Finset.mul_sum, he.complete, mul_one]
-- Lean 4 proof step from Mathlib.RingTheory.Idempotents (goal)
Goal:
R : Type u_1
e_1 : R
I : Type u_2
inst : Fintype I
e : I → R
inst_1 : Semiring R
he : CompleteOrthogonalIdempotents e
hc : ∀ (i : I), IsMulCentral (e i)
r : R
simp_rw simp_rw₁ : ∑ x : I, e x * r * e x = r
simp_rw₂ : ∑ x : I, r * e x * e x = r
simp_rw₃ : ∑ x : I, r * (e x * e x) = r
simp_rw₄ : ∑ x : I, r * e x = r
simp_rw₅ : r * ∑ i : I, e i = r
⊢ (fun (r : (i : I) → ⋯.Corner) ↦ (∑ i : I, (↑(r i) : R) : R))
      ((fun (r : R) (i : I) ↦
          Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Subsemigroup R) (Subsemigroup.corner (e i)) x)
            ((fun (x : R) ↦ e i * x * e i) r) ⋯)
        r) =
    r
have simp_rw₆ : r * 1 = r
Tactic: simp_rw [((hc _).comm _).eq, mul_assoc, (he.idem _).eq, ← Finset.mul_sum, he.complete, mul_one]
-- Lean 4 proof step from Mathlib.RingTheory.Idempotents (goal)
Goal:
R : Type u_1
e_1 : R
I : Type u_2
inst : Fintype I
e : I → R
inst_1 : Semiring R
he : CompleteOrthogonalIdempotents e
hc : ∀ (i : I), IsMulCentral (e i)
r : (i : I) → ⋯.Corner
i : I
⊢ (↑((fun (r : R) (i : I) ↦
            Subtype.mk (p := fun (x : R) ↦ Membership.mem (γ := Subsemigroup R) (Subsemigroup.corner (e i)) x)
              ((fun (x : R) ↦ e i * x * e i) r) ⋯)
          ((fun (r : (i : I) → ⋯.Corner) ↦ (∑ i : I, (↑(r i) : R) : R)) r) i) :
      R) =
    (↑(r i) : R)
have simp_rw : ∑ i_1 : I, e i * (↑(r i_1) : R) * e i = (↑(r i) : R)
Tactic: simp_rw [Finset.mul_sum, Finset.sum_mul]
-- Lean 4 proof step from Mathlib.RingTheory.Idempotents (goal)
Goal:
R : Type u_1
e_1 : R
I : Type u_2
inst : Fintype I
e : I → R
inst_1 : Semiring R
he : CompleteOrthogonalIdempotents e
hc : ∀ (i : I), IsMulCentral (e i)
r : (i : I) → ⋯.Corner
i : I
⊢ ∑ i_1 : I, e i * (↑(r i_1) : R) * e i = (↑(r i) : R)
have rw : e i * (↑(r i) : R) * e i = (↑(r i) : R)
Tactic: rw [Finset.sum_eq_single i _ (by simp at ·)]
-- Lean 4 proof step from Mathlib.RingTheory.Idempotents (goal)
Goal:
R : Type u_1
e_1 : R
I : Type u_2
inst : Fintype I
e : I → R
inst_1 : Semiring R
he : CompleteOrthogonalIdempotents e
hc : ∀ (i : I), IsMulCentral (e i)
r : (i : I) → ⋯.Corner
i : I
rw : e i * (↑(r i) : R) * e i = (↑(r i) : R)
⊢ ∑ i_1 : I, e i * (↑(r i_1) : R) * e i = (↑(r i) : R)
have rw₁ : ∀ (b : I), Membership.mem (γ := Finset I) Finset.univ b → b ≠ i → e i * (↑(r b) : R) * e i = 0
Tactic: rw [Finset.sum_eq_single i _ (by simp at ·)]
-- Lean 4 proof step from Mathlib.RingTheory.Idempotents (goal)
Goal:
R : Type u_1
e_1 : R
I : Type u_2
inst : Fintype I
e : I → R
inst_1 : Semiring R
he : CompleteOrthogonalIdempotents e
hc : ∀ (i : I), IsMulCentral (e i)
r : (i : I) → ⋯.Corner
i : I
⊢ e i * (↑(r i) : R) * e i = (↑(r i) : R)
have have : ∀ (r' : R) (eq : (fun (x : R) ↦ e i * x * e i) r' = (↑(r i) : R)), e i * (↑(r i) : R) * e i = (↑(r i) : R)
Tactic: have ⟨r', eq⟩ := (r i).2
-- Lean 4 proof step from Mathlib.RingTheory.Idempotents (goal)
Goal:
R : Type u_1
e_1 : R
I : Type u_2
inst : Fintype I
e : I → R
inst_1 : Semiring R
he : CompleteOrthogonalIdempotents e
hc : ∀ (i : I), IsMulCentral (e i)
r : (i : I) → ⋯.Corner
i : I
r' : R
eq : (fun (x : R) ↦ e i * x * e i) r' = (↑(r i) : R)
⊢ e i * (↑(r i) : R) * e i = (↑(r i) : R)
have rw : e i * (fun (x : R) ↦ e i * x * e i) r' * e i = (fun (x : R) ↦ e i * x * e i) r'
Tactic: rw [← eq]
-- Lean 4 proof step from Mathlib.RingTheory.Idempotents (goal)
Goal:
R : Type u_1
e_1 : R
I : Type u_2
inst : Fintype I
e : I → R
inst_1 : Semiring R
he : CompleteOrthogonalIdempotents e
hc : ∀ (i : I), IsMulCentral (e i)
r : (i : I) → ⋯.Corner
i : I
r' : R
eq : (fun (x : R) ↦ e i * x * e i) r' = (↑(r i) : R)
simp_rw simp_rw₁ : e i * (e i * r' * e i) * e i = e i * r' * e i
⊢ e i * (fun (x : R) ↦ e i * x * e i) r' * e i = (fun (x : R) ↦ e i * x * e i) r'
have simp_rw₂ : e i * e i * r' * e i * e i = e i * r' * e i
Tactic: simp_rw [← mul_assoc, (he.idem i).eq, mul_assoc, (he.idem i).eq]
-- Lean 4 proof step from Mathlib.RingTheory.Idempotents (goal)
Goal:
R : Type u_1
e_1 : R
I : Type u_2
inst : Fintype I
e : I → R
inst_1 : Semiring R
he : CompleteOrthogonalIdempotents e
hc : ∀ (i : I), IsMulCentral (e i)
r : (i : I) → ⋯.Corner
i : I
r' : R
eq : (fun (x : R) ↦ e i * x * e i) r' = (↑(r i) : R)
simp_rw simp_rw₁ : e i * (e i * r' * e i) * e i = e i * r' * e i
simp_rw₂ : e i * e i * r' * e i * e i = e i * r' * e i
⊢ e i * (fun (x : R) ↦ e i * x * e i) r' * e i = (fun (x : R) ↦ e i * x * e i) r'
have simp_rw₃ : e i * r' * e i * e i = e i * r' * e i
Tactic: simp_rw [← mul_assoc, (he.idem i).eq, mul_assoc, (he.idem i).eq]
-- Lean 4 proof step from Mathlib.RingTheory.Idempotents (goal)
Goal:
R : Type u_1
e_1 : R
I : Type u_2
inst : Fintype I
e : I → R
inst_1 : Semiring R
he : CompleteOrthogonalIdempotents e
hc : ∀ (i : I), IsMulCentral (e i)
r : (i : I) → ⋯.Corner
i : I
r' : R
eq : (fun (x : R) ↦ e i * x * e i) r' = (↑(r i) : R)
simp_rw simp_rw₁ : e i * (e i * r' * e i) * e i = e i * r' * e i
simp_rw₂ : e i * e i * r' * e i * e i = e i * r' * e i
simp_rw₃ : e i * r' * e i * e i = e i * r' * e i
⊢ e i * (fun (x : R) ↦ e i * x * e i) r' * e i = (fun (x : R) ↦ e i * x * e i) r'
have simp_rw₄ : e i * (r' * (e i * e i)) = e i * (r' * e i)
Tactic: simp_rw [← mul_assoc, (he.idem i).eq, mul_assoc, (he.idem i).eq]
-- Lean 4 proof step from Mathlib.RingTheory.Idempotents (goal)
Goal:
R : Type u_1
e_1 : R
I : Type u_2
inst : Fintype I
e : I → R
inst_1 : Semiring R
he : CompleteOrthogonalIdempotents e
hc : ∀ (i : I), IsMulCentral (e i)
r : (i : I) → ⋯.Corner
i j : I
h : Membership.mem (γ := Finset I) Finset.univ j
ne : j ≠ i
⊢ e i * (↑(r j) : R) * e i = 0
have have : ∀ (r' : R) (eq : (fun (x : R) ↦ e j * x * e j) r' = (↑(r j) : R)), e i * (↑(r j) : R) * e i = 0
Tactic: have ⟨r', eq⟩ := (r j).2
-- Lean 4 proof step from Mathlib.RingTheory.Idempotents (goal)
Goal:
R : Type u_1
e_1 : R
I : Type u_2
inst : Fintype I
e : I → R
inst_1 : Semiring R
he : CompleteOrthogonalIdempotents e
hc : ∀ (i : I), IsMulCentral (e i)
r : (i : I) → ⋯.Corner
i j : I
h : Membership.mem (γ := Finset I) Finset.univ j
ne : j ≠ i
r' : R
eq : (fun (x : R) ↦ e j * x * e j) r' = (↑(r j) : R)
⊢ e i * (↑(r j) : R) * e i = 0
have rw : e i * (fun (x : R) ↦ e j * x * e j) r' * e i = 0
Tactic: rw [← eq]
-- Lean 4 proof step from Mathlib.RingTheory.Idempotents (goal)
Goal:
R : Type u_1
e_1 : R
I : Type u_2
inst : Fintype I
e : I → R
inst_1 : Semiring R
he : CompleteOrthogonalIdempotents e
hc : ∀ (i : I), IsMulCentral (e i)
r : (i : I) → ⋯.Corner
i j : I
h : Membership.mem (γ := Finset I) Finset.univ j
ne : j ≠ i
r' : R
eq : (fun (x : R) ↦ e j * x * e j) r' = (↑(r j) : R)
simp_rw simp_rw₁ : e i * (e j * r' * e j) * e i = 0
⊢ e i * (fun (x : R) ↦ e j * x * e j) r' * e i = 0
have simp_rw₂ : e i * e j * r' * e j * e i = 0
Tactic: simp_rw [← mul_assoc, he.ortho ne.symm, zero_mul]
-- Lean 4 proof step from Mathlib.RingTheory.Idempotents (goal)
Goal:
R : Type u_1
e_1 : R
I : Type u_2
inst : Fintype I
e : I → R
inst_1 : Semiring R
he : CompleteOrthogonalIdempotents e
hc : ∀ (i : I), IsMulCentral (e i)
r : (i : I) → ⋯.Corner
i j : I
h : Membership.mem (γ := Finset I) Finset.univ j
ne : j ≠ i
r' : R
eq : (fun (x : R) ↦ e j * x * e j) r' = (↑(r j) : R)
simp_rw simp_rw₁ : e i * (e j * r' * e j) * e i = 0
simp_rw₂ : e i * e j * r' * e j * e i = 0
⊢ e i * (fun (x : R) ↦ e j * x * e j) r' * e i = 0
have simp_rw₃ : 0 * r' * e j * e i = 0
Tactic: simp_rw [← mul_assoc, he.ortho ne.symm, zero_mul]
-- Lean 4 proof step from Mathlib.RingTheory.Idempotents (goal)
Goal:
R : Type u_1
e_1 : R
I : Type u_2
inst : Fintype I
e : I → R
inst_1 : Semiring R
he : CompleteOrthogonalIdempotents e
hc : ∀ (i : I), IsMulCentral (e i)
r₁ r₂ : R
i : I
⊢ e i * (r₁ * r₂) * e i = e i * (r₁ * e i * r₂) * e i
have simp_rw : e i * (r₁ * r₂) * e i = e i * (e i * r₁ * r₂) * e i
Tactic: simp_rw [← ((hc i).comm r₁).eq, ← mul_assoc, (he.idem i).eq]
-- Lean 4 proof step from Mathlib.RingTheory.Idempotents (goal)
Goal:
R : Type u_1
e_1 : R
I : Type u_2
inst : Fintype I
e : I → R
inst_1 : Semiring R
he : CompleteOrthogonalIdempotents e
hc : ∀ (i : I), IsMulCentral (e i)
r₁ r₂ : R
i : I
simp_rw : e i * (r₁ * r₂) * e i = e i * (e i * r₁ * r₂) * e i
⊢ e i * (r₁ * r₂) * e i = e i * (r₁ * e i * r₂) * e i
have simp_rw₁ : e i * r₁ * r₂ * e i = e i * e i * r₁ * r₂ * e i
Tactic: simp_rw [← ((hc i).comm r₁).eq, ← mul_assoc, (he.idem i).eq]
-- Lean 4 proof step from Mathlib.RingTheory.Idempotents (goal)
Goal:
R : Type u_1
e_1 : R
I : Type u_2
inst : Fintype I
e : I → R
inst_1 : Semiring R
he : CompleteOrthogonalIdempotents e
hc : ∀ (i : I), IsMulCentral (e i)
r₁ r₂ : R
i : I
| r₁ * e i * r₂
have rw : r₁ * (e i * e i) * r₂
Tactic: rw [← (he.idem i).eq]
-- Lean 4 proof step from Mathlib.RingTheory.Idempotents (goal)
Goal:
R : Type u_1
e_1 : R
I : Type u_2
inst : Fintype I
e : I → R
inst_1 : Semiring R
he : CompleteOrthogonalIdempotents e
hc : ∀ (i : I), IsMulCentral (e i)
r₁ r₂ : R
i : I
⊢ e i * (r₁ * e i * r₂) * e i = e i * r₁ * e i * (e i * r₂ * e i)
have conv : e i * (r₁ * (e i * e i) * r₂) * e i = e i * r₁ * e i * (e i * r₂ * e i)
Tactic: conv in (r₁ * _ * r₂) => rw [← (he.idem i).eq]
-- Lean 4 proof step from Mathlib.RingTheory.Int.Basic (goal)
Goal:
a b : ℤ
⊢ IsCoprime a b ↔ a.natAbs.Coprime b.natAbs
have rw : a.gcd b = 1 ↔ a.natAbs.Coprime b.natAbs
Tactic: rw [isCoprime_iff_gcd_eq_one, Nat.coprime_iff_gcd_eq_one, gcd_eq_natAbs]
-- Lean 4 proof step from Mathlib.RingTheory.Int.Basic (goal)
Goal:
a b : ℤ
rw : a.gcd b = 1 ↔ a.natAbs.Coprime b.natAbs
⊢ IsCoprime a b ↔ a.natAbs.Coprime b.natAbs
have rw₁ : a.gcd b = 1 ↔ a.natAbs.gcd b.natAbs = 1
Tactic: rw [isCoprime_iff_gcd_eq_one, Nat.coprime_iff_gcd_eq_one, gcd_eq_natAbs]
-- Lean 4 proof step from Mathlib.RingTheory.Int.Basic (goal)
Goal:
a b : ℤ
rw : a.gcd b = 1 ↔ a.natAbs.Coprime b.natAbs
rw₁ : a.gcd b = 1 ↔ a.natAbs.gcd b.natAbs = 1
⊢ IsCoprime a b ↔ a.natAbs.Coprime b.natAbs
have rw₂ : a.natAbs.gcd b.natAbs = 1 ↔ a.natAbs.gcd b.natAbs = 1
Tactic: rw [isCoprime_iff_gcd_eq_one, Nat.coprime_iff_gcd_eq_one, gcd_eq_natAbs]
-- Lean 4 proof step from Mathlib.RingTheory.Int.Basic (goal)
Goal:
a b c : ℤ
h : a.gcd b = 1
heq : a * b = HPow.hPow (β := ℕ) c 2
⊢ IsUnit (@GCDMonoid.gcd _ CommSemiring.toCommMonoidWithZero _ a b)
have rw : IsUnit (M := ℤ) 1
Tactic: rw [← coe_gcd, h, Int.ofNat_one]
-- Lean 4 proof step from Mathlib.RingTheory.Int.Basic (hypothesis)
Goal:
a b c : ℤ
h : a.gcd b = 1
heq : a * b = HPow.hPow (β := ℕ) c 2
⊢ ∃ (a0 : ℤ), a = HPow.hPow (β := ℕ) a0 2 ∨ a = -HPow.hPow (β := ℕ) a0 2
have h' : IsUnit (@GCDMonoid.gcd _ CommSemiring.toCommMonoidWithZero _ a b)
Tactic: have h' : IsUnit (GCDMonoid.gcd a b) := by
    rw [← coe_gcd, h, Int.ofNat_one]
    exact isUnit_one
-- Lean 4 proof step from Mathlib.RingTheory.Int.Basic (goal)
Goal:
a b c : ℤ
h : a.gcd b = 1
heq : a * b = HPow.hPow (β := ℕ) c 2
h' : IsUnit (@GCDMonoid.gcd _ CommSemiring.toCommMonoidWithZero _ a b)
⊢ ∃ (a0 : ℤ), a = HPow.hPow (β := ℕ) a0 2 ∨ a = -HPow.hPow (β := ℕ) a0 2
have obtain : ∀ (d : ℤ) (u : ℤˣ) (hu : HPow.hPow (β := ℕ) d 2 * (↑u : ℤ) = a),
  ∃ (a0 : ℤ), a = HPow.hPow (β := ℕ) a0 2 ∨ a = -HPow.hPow (β := ℕ) a0 2
Tactic: obtain ⟨d, ⟨u, hu⟩⟩ := exists_associated_pow_of_mul_eq_pow h' heq
-- Lean 4 proof step from Mathlib.RingTheory.Int.Basic (goal)
Goal:
a b c : ℤ
h : a.gcd b = 1
heq : a * b = HPow.hPow (β := ℕ) c 2
h' : IsUnit (@GCDMonoid.gcd _ CommSemiring.toCommMonoidWithZero _ a b)
d : ℤ
u : ℤˣ
hu : HPow.hPow (β := ℕ) d 2 * (↑u : ℤ) = a
⊢ ∃ (a0 : ℤ), a = HPow.hPow (β := ℕ) a0 2 ∨ a = -HPow.hPow (β := ℕ) a0 2
have h₁ : a = HPow.hPow (β := ℕ) d 2 ∨ a = -HPow.hPow (β := ℕ) d 2
Tactic: use d
-- Lean 4 proof step from Mathlib.RingTheory.Int.Basic (goal)
Goal:
a b c : ℤ
h : a.gcd b = 1
heq : a * b = HPow.hPow (β := ℕ) c 2
h' : IsUnit (@GCDMonoid.gcd _ CommSemiring.toCommMonoidWithZero _ a b)
d : ℤ
u : ℤˣ
hu : HPow.hPow (β := ℕ) d 2 * (↑u : ℤ) = a
⊢ a = HPow.hPow (β := ℕ) d 2 ∨ a = -HPow.hPow (β := ℕ) d 2
have h₁ : HPow.hPow (β := ℕ) d 2 * (↑u : ℤ) = HPow.hPow (β := ℕ) d 2 ∨ HPow.hPow (β := ℕ) d 2 * (↑u : ℤ) = -HPow.hPow (β := ℕ) d 2
Tactic: rw [← hu]
-- Lean 4 proof step from Mathlib.RingTheory.Int.Basic (goal)
Goal:
a b c : ℤ
h : a.gcd b = 1
heq : a * b = HPow.hPow (β := ℕ) c 2
h' : IsUnit (@GCDMonoid.gcd _ CommSemiring.toCommMonoidWithZero _ a b)
d : ℤ
u : ℤˣ
hu : HPow.hPow (β := ℕ) d 2 * (↑u : ℤ) = a
⊢ HPow.hPow (β := ℕ) d 2 * (↑u : ℤ) = HPow.hPow (β := ℕ) d 2 ∨
    HPow.hPow (β := ℕ) d 2 * (↑u : ℤ) = -HPow.hPow (β := ℕ) d 2
have h₁ : ∀ (hu' : u = 1),
  HPow.hPow (β := ℕ) d 2 * (↑u : ℤ) = HPow.hPow (β := ℕ) d 2 ∨
    HPow.hPow (β := ℕ) d 2 * (↑u : ℤ) = -HPow.hPow (β := ℕ) d 2
Tactic: rcases Int.units_eq_one_or u with hu' | hu'
-- Lean 4 proof step from Mathlib.RingTheory.Int.Basic (goal)
Goal:
a b c : ℤ
h : a.gcd b = 1
heq : a * b = HPow.hPow (β := ℕ) c 2
h' : IsUnit (@GCDMonoid.gcd _ CommSemiring.toCommMonoidWithZero _ a b)
d : ℤ
u : ℤˣ
hu : HPow.hPow (β := ℕ) d 2 * (↑u : ℤ) = a
h₁ :
  ∀ (hu' : u = 1),
    HPow.hPow (β := ℕ) d 2 * (↑u : ℤ) = HPow.hPow (β := ℕ) d 2 ∨
      HPow.hPow (β := ℕ) d 2 * (↑u : ℤ) = -HPow.hPow (β := ℕ) d 2
⊢ HPow.hPow (β := ℕ) d 2 * (↑u : ℤ) = HPow.hPow (β := ℕ) d 2 ∨
    HPow.hPow (β := ℕ) d 2 * (↑u : ℤ) = -HPow.hPow (β := ℕ) d 2
have h₂ : ∀ (hu' : u = -1),
  HPow.hPow (β := ℕ) d 2 * (↑u : ℤ) = HPow.hPow (β := ℕ) d 2 ∨
    HPow.hPow (β := ℕ) d 2 * (↑u : ℤ) = -HPow.hPow (β := ℕ) d 2
Tactic: rcases Int.units_eq_one_or u with hu' | hu'
-- Lean 4 proof step from Mathlib.RingTheory.Int.Basic (goal)
Goal:
a b c : ℤ
h : a.gcd b = 1
heq : a * b = HPow.hPow (β := ℕ) c 2
h' : IsUnit (@GCDMonoid.gcd _ CommSemiring.toCommMonoidWithZero _ a b)
d : ℤ
u : ℤˣ
hu : HPow.hPow (β := ℕ) d 2 * (↑u : ℤ) = a
hu' : u = 1
⊢ HPow.hPow (β := ℕ) d 2 * (↑u : ℤ) = HPow.hPow (β := ℕ) d 2 ∨
    HPow.hPow (β := ℕ) d 2 * (↑u : ℤ) = -HPow.hPow (β := ℕ) d 2
have h₁ : HPow.hPow (β := ℕ) d 2 * (↑1 : ℤ) = HPow.hPow (β := ℕ) d 2 ∨ HPow.hPow (β := ℕ) d 2 * (↑1 : ℤ) = -HPow.hPow (β := ℕ) d 2
Tactic: rw [hu']
-- Lean 4 proof step from Mathlib.RingTheory.Int.Basic (goal)
Goal:
a b c : ℤ
h : a.gcd b = 1
heq : a * b = HPow.hPow (β := ℕ) c 2
h' : IsUnit (@GCDMonoid.gcd _ CommSemiring.toCommMonoidWithZero _ a b)
d : ℤ
u : ℤˣ
hu : HPow.hPow (β := ℕ) d 2 * (↑u : ℤ) = a
hu' : u = -1
⊢ HPow.hPow (β := ℕ) d 2 * (↑u : ℤ) = HPow.hPow (β := ℕ) d 2 ∨
    HPow.hPow (β := ℕ) d 2 * (↑u : ℤ) = -HPow.hPow (β := ℕ) d 2
have h₁ : HPow.hPow (β := ℕ) d 2 * (↑(-1) : ℤ) = HPow.hPow (β := ℕ) d 2 ∨
  HPow.hPow (β := ℕ) d 2 * (↑(-1) : ℤ) = -HPow.hPow (β := ℕ) d 2
Tactic: rw [hu']
-- Lean 4 proof step from Mathlib.RingTheory.Int.Basic (goal)
Goal:
a b : ℤ
⊢ (EuclideanDomain.gcd a b).natAbs = a.gcd b
have a₁ : (EuclideanDomain.gcd a b).natAbs ∣ a.gcd b
Tactic: apply Nat.dvd_antisymm
-- Lean 4 proof step from Mathlib.RingTheory.Int.Basic (goal)
Goal:
a b : ℤ
a₁ : (EuclideanDomain.gcd a b).natAbs ∣ a.gcd b
⊢ (EuclideanDomain.gcd a b).natAbs = a.gcd b
have a₂ : a.gcd b ∣ (EuclideanDomain.gcd a b).natAbs
Tactic: apply Nat.dvd_antisymm
-- Lean 4 proof step from Mathlib.RingTheory.Int.Basic (goal)
Goal:
a b : ℤ
⊢ (EuclideanDomain.gcd a b).natAbs ∣ a.gcd b
have a₁ : Dvd.dvd (α := ℤ) (↑(EuclideanDomain.gcd a b).natAbs : ℤ) (↑(a.gcd b) : ℤ)
Tactic: rw [← Int.natCast_dvd_natCast]
-- Lean 4 proof step from Mathlib.RingTheory.Int.Basic (goal)
Goal:
a b : ℤ
⊢ a.gcd b ∣ (EuclideanDomain.gcd a b).natAbs
have a₁ : Dvd.dvd (α := ℤ) (↑(a.gcd b) : ℤ) (↑(EuclideanDomain.gcd a b).natAbs : ℤ)
Tactic: rw [← Int.natCast_dvd_natCast]
-- Lean 4 proof step from Mathlib.RingTheory.Int.Basic (goal)
Goal:
a b : ℤ
⊢ Dvd.dvd (α := ℤ) (↑(EuclideanDomain.gcd a b).natAbs : ℤ) (↑(a.gcd b) : ℤ)
have a₁ : EuclideanDomain.gcd a b ∣ (↑(a.gcd b) : ℤ)
Tactic: rw [Int.natAbs_dvd]
-- Lean 4 proof step from Mathlib.RingTheory.Int.Basic (goal)
Goal:
a b : ℤ
⊢ Dvd.dvd (α := ℤ) (↑(a.gcd b) : ℤ) (↑(EuclideanDomain.gcd a b).natAbs : ℤ)
have a₁ : (↑(a.gcd b) : ℤ) ∣ EuclideanDomain.gcd a b
Tactic: rw [Int.dvd_natAbs]
-- Lean 4 proof step from Mathlib.RingTheory.Int.Basic (goal)
Goal:
m n : ℤ
p : ℕ
hp : Nat.Prime p
h : (↑p : ℤ) ∣ m * n
⊢ p ∣ m.natAbs ∨ p ∣ n.natAbs
have rwa : p ∣ m.natAbs * n.natAbs
Tactic: rwa [← hp.dvd_mul, ← Int.natAbs_mul, ← Int.natCast_dvd]
-- Lean 4 proof step from Mathlib.RingTheory.Int.Basic (goal)
Goal:
m n : ℤ
p : ℕ
hp : Nat.Prime p
h : (↑p : ℤ) ∣ m * n
rwa : p ∣ m.natAbs * n.natAbs
⊢ p ∣ m.natAbs ∨ p ∣ n.natAbs
have rwa₁ : p ∣ (m * n).natAbs
Tactic: rwa [← hp.dvd_mul, ← Int.natAbs_mul, ← Int.natCast_dvd]
-- Lean 4 proof step from Mathlib.RingTheory.Int.Basic (goal)
Goal:
m n : ℤ
p : ℕ
hp : Nat.Prime p
h : (↑p : ℤ) ∣ m * n
⊢ (↑p : ℤ) ∣ m ∨ (↑p : ℤ) ∣ n
have rw : p ∣ m.natAbs ∨ p ∣ n.natAbs
Tactic: rw [Int.natCast_dvd, Int.natCast_dvd]
-- Lean 4 proof step from Mathlib.RingTheory.Int.Basic (hypothesis)
Goal:
n : ℤ
k p : ℕ
hp : Nat.Prime p
h : (↑p : ℤ) ∣ n ^ k
⊢ p ∣ n.natAbs
have h₁ : p ∣ n.natAbs ^ k
Tactic: rw [Int.natCast_dvd, Int.natAbs_pow] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.Int.Basic (goal)
Goal:
n : ℤ
k p : ℕ
hp : Nat.Prime p
h : (↑p : ℤ) ∣ n ^ k
⊢ (↑p : ℤ) ∣ n
have rw : p ∣ n.natAbs
Tactic: rw [Int.natCast_dvd]
-- Lean 4 proof step from Mathlib.RingTheory.Int.Basic (goal)
Goal:
m : ℤ
p : ℕ
hp : Nat.Prime p
h : (↑p : ℤ) ∣ 2 * HPow.hPow (β := ℕ) m 2
⊢ p = 2 ∨ p ∣ m.natAbs
have inl : ∀ (hp2 : p ∣ Int.natAbs 2), p = 2 ∨ p ∣ m.natAbs
Tactic: rcases Int.Prime.dvd_mul hp h with hp2 | hpp
-- Lean 4 proof step from Mathlib.RingTheory.Int.Basic (goal)
Goal:
m : ℤ
p : ℕ
hp : Nat.Prime p
h : (↑p : ℤ) ∣ 2 * HPow.hPow (β := ℕ) m 2
inl : ∀ (hp2 : p ∣ Int.natAbs 2), p = 2 ∨ p ∣ m.natAbs
⊢ p = 2 ∨ p ∣ m.natAbs
have inr : ∀ (hpp : p ∣ (HPow.hPow (β := ℕ) m 2).natAbs), p = 2 ∨ p ∣ m.natAbs
Tactic: rcases Int.Prime.dvd_mul hp h with hp2 | hpp
-- Lean 4 proof step from Mathlib.RingTheory.Int.Basic (goal)
Goal:
m : ℤ
p : ℕ
hp : Nat.Prime p
h : (↑p : ℤ) ∣ 2 * HPow.hPow (β := ℕ) m 2
hp2 : p ∣ Int.natAbs 2
⊢ p = 2 ∨ p ∣ m.natAbs
have inl : p = 2
Tactic: apply Or.intro_left
-- Lean 4 proof step from Mathlib.RingTheory.Int.Basic (goal)
Goal:
m : ℤ
p : ℕ
hp : Nat.Prime p
h : (↑p : ℤ) ∣ 2 * HPow.hPow (β := ℕ) m 2
hpp : p ∣ (HPow.hPow (β := ℕ) m 2).natAbs
⊢ p = 2 ∨ p ∣ m.natAbs
have inr : p ∣ m.natAbs
Tactic: apply Or.intro_right
-- Lean 4 proof step from Mathlib.RingTheory.Int.Basic (hypothesis)
Goal:
m : ℤ
p : ℕ
hp : Nat.Prime p
h : (↑p : ℤ) ∣ 2 * HPow.hPow (β := ℕ) m 2
hpp : p ∣ (HPow.hPow (β := ℕ) m 2).natAbs
⊢ p ∣ m.natAbs
have hpp₁ : p ∣ m.natAbs * m.natAbs
Tactic: rw [sq, Int.natAbs_mul] at hpp
Cleared hypotheses: hpp
-- Lean 4 proof step from Mathlib.RingTheory.Int.Basic (goal)
Goal:
n : ℤ
hn : n.natAbs ≠ 1
⊢ ∃ (p : ℤ), Prime p ∧ p ∣ n
have obtain : ∀ (p : ℕ) (pp : Nat.Prime p) (pd : p ∣ n.natAbs), ∃ (p : ℤ), Prime p ∧ p ∣ n
Tactic: obtain ⟨p, pp, pd⟩ := Nat.exists_prime_and_dvd hn
-- Lean 4 proof step from Mathlib.RingTheory.Int.Basic (goal)
Goal:
a : ℤ
⊢ Eq (α := Ideal ℤ) (Ideal.span {(↑a.natAbs : ℤ)}) (Ideal.span {a})
have rw : Associated (↑a.natAbs : ℤ) a
Tactic: rw [Ideal.span_singleton_eq_span_singleton]
-- Lean 4 proof step from Mathlib.RingTheory.Int.Basic (goal)
Goal:
a b c : ℤ
hab : IsCoprime a b
k : ℕ
hk : Odd k
h : a * b = c ^ k
⊢ ∃ (d : ℤ), a = d ^ k
have obtain : ∀ (d : ℤ) (hd : Associated (d ^ k) a), ∃ (d : ℤ), a = d ^ k
Tactic: obtain ⟨d, hd⟩ := exists_associated_pow_of_mul_eq_pow' hab h
-- Lean 4 proof step from Mathlib.RingTheory.Int.Basic (hypothesis)
Goal:
a b c : ℤ
hab : IsCoprime a b
k : ℕ
hk : Odd k
h : a * b = c ^ k
d : ℤ
hd : Associated (d ^ k) a
⊢ ∃ (d : ℤ), a = d ^ k
have hd₁ : Associated a (d ^ k)
Tactic: replace hd := hd.symm
Cleared hypotheses: hd
-- Lean 4 proof step from Mathlib.RingTheory.Int.Basic (hypothesis)
Goal:
a b c : ℤ
hab : IsCoprime a b
k : ℕ
hk : Odd k
h : a * b = c ^ k
d : ℤ
hd : Associated a (d ^ k)
⊢ ∃ (d : ℤ), a = d ^ k
have hd₁ : a = d ^ k ∨ a = (-d) ^ k
Tactic: rw [associated_iff_natAbs, natAbs_eq_natAbs_iff, ← hk.neg_pow] at hd
Cleared hypotheses: hd
-- Lean 4 proof step from Mathlib.RingTheory.Int.Basic (goal)
Goal:
a b c : ℤ
hab : IsCoprime a b
k : ℕ
hk : Odd k
h : a * b = c ^ k
d : ℤ
hd : a = d ^ k ∨ a = (-d) ^ k
⊢ ∃ (d : ℤ), a = d ^ k
have inl : ∀ (hab : IsCoprime (d ^ k) b) (h : d ^ k * b = c ^ k), ∃ (d_1 : ℤ), d ^ k = d_1 ^ k
Tactic: obtain rfl | rfl := hd
Cleared hypotheses: a, hab, h, hd
-- Lean 4 proof step from Mathlib.RingTheory.Int.Basic (goal)
Goal:
a b c : ℤ
hab : IsCoprime a b
k : ℕ
hk : Odd k
h : a * b = c ^ k
d : ℤ
hd : a = d ^ k ∨ a = (-d) ^ k
inl : ∀ (hab : IsCoprime (d ^ k) b) (h : d ^ k * b = c ^ k), ∃ (d_1 : ℤ), d ^ k = d_1 ^ k
⊢ ∃ (d : ℤ), a = d ^ k
have inr : ∀ (hab : IsCoprime ((-d) ^ k) b) (h : (-d) ^ k * b = c ^ k), ∃ (d_1 : ℤ), (-d) ^ k = d_1 ^ k
Tactic: obtain rfl | rfl := hd
Cleared hypotheses: a, hab, h, hd
-- Lean 4 proof step from Mathlib.RingTheory.Int.Basic (goal)
Goal:
a b c : ℤ
hab : IsCoprime a b
k : ℕ
hk : Odd k
h : a * b = c ^ k
⊢ b * a = c ^ k
have rwa : ∀ (h : b * a = c ^ k), b * a = c ^ k
Tactic: rwa [mul_comm] at h
Cleared hypotheses: h