awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Idempotents
Goal:
R : Type u_1
e : R
inst : Semigroup R
a b : R
simp_rw simp_rw₁ : e * (a * e * e * b) * e = e * a * e * (e * b * e)
⊢ (fun (x : R) ↦ e * x * e) (a * e * e * b) =
    HMul.hMul (α := R) ((fun (x : R) ↦ e * x * e) a) ((fun (x : R) ↦ e * x * e) b)

Tactic:
simp_rw [mul_assoc]

Premises used: mul_assoc
-- Module: Mathlib.RingTheory.Idempotents
Goal:
R : Type u_1
e : R
inst : Semigroup R
a b : R
⊢ Membership.mem (γ := Set R) (Set.range fun (x : R) ↦ e * x * e)
    (HMul.hMul (α := R) ((fun (x : R) ↦ e * x * e) a) ((fun (x : R) ↦ e * x * e) b))

Tactic:
exact ⟨a * e * e * b, by simp_rw [mul_assoc]⟩
-- Module: Mathlib.RingTheory.Idempotents
Goal:
R : Type u_1
e : R
inst : Semigroup R
idem : IsIdempotentElem e
r : R
simp_rw simp_rw₁ : e * (e * r * e) = e * r * e ∧ e * r * e * e = e * r * e
simp_rw₂ : e * e * r * e = e * r * e ∧ e * r * e * e = e * r * e
simp_rw₃ : True ∧ e * r * e * e = e * r * e
simp_rw₄ : True ∧ e * (r * (e * e)) = e * (r * e)
simp_rw₅ : True ∧ True
⊢ e * (fun (x : R) ↦ e * x * e) r = (fun (x : R) ↦ e * x * e) r ∧
    (fun (x : R) ↦ e * x * e) r * e = (fun (x : R) ↦ e * x * e) r

Tactic:
simp_rw [← mul_assoc, idem.eq, mul_assoc, idem.eq, true_and]

Premises used: mul_assoc, IsIdempotentElem.eq, true_and
-- Module: Mathlib.RingTheory.Idempotents
Goal:
R : Type u_1
e : R
inst : Semigroup R
idem : IsIdempotentElem e
hc : IsMulCentral e
r : R
rw : e * r = r → r * e = r
⊢ Membership.mem (γ := Subsemigroup R) (corner e) r ↔ e * r = r

Tactic:
rw [mem_corner_iff idem, and_iff_left_of_imp]

Premises used: and_iff_left_of_imp, Subsemigroup.mem_corner_iff
-- Module: Mathlib.RingTheory.Idempotents
Goal:
R : Type u_1
e : R
inst : Semigroup R
idem : IsIdempotentElem e
hc : IsMulCentral e
r : R
h rwa rwa₁ rwa₂ rwa₃ : e * r = r
⊢ r * e = r

Tactic:
rwa [← hc.comm]

Premises used: IsMulCentral.comm
-- Module: Mathlib.RingTheory.Idempotents
Goal:
R : Type u_1
e : R
inst : Semigroup R
idem : IsIdempotentElem e
hc : IsMulCentral e
r : R
rw : e * r = r ↔ r * e = r
rw₁ rw₂ : r * e = r ↔ r * e = r
⊢ Membership.mem (γ := Subsemigroup R) (corner e) r ↔ r * e = r

Tactic:
rw [mem_corner_iff_mul_left idem hc, hc.comm]

Premises used: IsMulCentral.comm, Subsemigroup.mem_corner_iff_mul_left
-- Module: Mathlib.RingTheory.Idempotents
Goal:
R : Type u_1
e : R
inst : Semigroup R
idem : IsIdempotentElem e
hc : IsMulCentral e
r : R
simp_rw :
  Membership.mem (γ := Subsemigroup R) { carrier := Set.range fun (x : R) ↦ e * x * e, mul_mem' := ⋯ } r ↔
    Membership.mem (γ := Set R) (Set.range fun (x : R) ↦ e * x) r
simp_rw₁ :
  Membership.mem (γ := Set R) (Set.range fun (x : R) ↦ e * x * e) r ↔
    Membership.mem (γ := Set R) (Set.range fun (x : R) ↦ e * x) r
simp_rw₂ : (∃ (y : R), e * y * e = r) ↔ ∃ (y : R), e * y = r
simp_rw₃ : (∃ (y : R), e * (e * y) = r) ↔ ∃ (y : R), e * y = r
simp_rw₄ : (∃ (y : R), e * e * y = r) ↔ ∃ (y : R), e * y = r
⊢ Membership.mem (γ := Subsemigroup R) (corner e) r ↔ Membership.mem (γ := Set R) (Set.range fun (x : R) ↦ e * x) r

Tactic:
simp_rw [corner, mem_mk, Set.mem_range, ← (hc.comm _).eq, ← mul_assoc, idem.eq]

Premises used: Set.mem_range, mul_assoc, Subsemigroup.mem_mk, IsMulCentral.comm, IsIdempotentElem.eq, Subsemigroup.corner, Commute.eq
-- Module: Mathlib.RingTheory.Idempotents
Goal:
R : Type u_1
e : R
inst : Semigroup R
idem : IsIdempotentElem e
hc : IsMulCentral e
r : R
simp_rw :
  Membership.mem (γ := Set R) (Set.range fun (x : R) ↦ e * x) r ↔
    Membership.mem (γ := Set R) (Set.range fun (x : R) ↦ x * e) r
⊢ Membership.mem (γ := Subsemigroup R) (corner e) r ↔ Membership.mem (γ := Set R) (Set.range fun (x : R) ↦ x * e) r

Tactic:
simp_rw [mem_corner_iff_mem_range_mul_left idem hc, (hc.comm _).eq]

Premises used: IsMulCentral.comm, Commute.eq, Subsemigroup.mem_corner_iff_mem_range_mul_left
-- Module: Mathlib.RingTheory.Idempotents
Goal:
R : Type u_1
e : R
inst : NonUnitalSemiring R
a b : R
simp_rw simp_rw₁ : e * (a + b) * e = e * a * e + e * b * e
simp_rw₂ : (e * a + e * b) * e = e * a * e + e * b * e
⊢ (fun (x : R) ↦ e * x * e) (a + b) = HAdd.hAdd (α := R) ((fun (x : R) ↦ e * x * e) a) ((fun (x : R) ↦ e * x * e) b)

Tactic:
simp_rw [mul_add, add_mul]

Premises used: add_mul, mul_add
-- Module: Mathlib.RingTheory.Idempotents
Goal:
R : Type u_1
e : R
inst : NonUnitalSemiring R
a b : R
⊢ HAdd.hAdd (α := R) ((fun (x : R) ↦ e * x * e) a) ((fun (x : R) ↦ e * x * e) b) ∈
    Subsemigroup.carrier (Subsemigroup.corner e)

Tactic:
exact ⟨a + b, by simp_rw [mul_add, add_mul]⟩
-- Module: Mathlib.RingTheory.Idempotents
Goal:
R : Type u_1
e : R
inst : NonUnitalSemiring R
simp_rw simp_rw₁ : e * 0 * e = 0
simp_rw₂ : 0 * e = 0
⊢ Eq.{u_1 + 1} (α := R) ((fun (x : R) ↦ e * x * e) 0) 0

Tactic:
simp_rw [mul_zero, zero_mul]

Premises used: MulZeroClass.zero_mul, MulZeroClass.mul_zero
-- Module: Mathlib.RingTheory.Idempotents
Goal:
R : Type u_1
e : R
inst : NonUnitalRing R
a : R
simp_rw simp_rw₁ : e * -a * e = -(e * a * e)
simp_rw₂ : -(e * a) * e = -(e * a * e)
⊢ Eq.{u_1 + 1} (α := R) ((fun (x : R) ↦ e * x * e) (-a)) (-(fun (x : R) ↦ e * x * e) a)

Tactic:
simp_rw [mul_neg, neg_mul]

Premises used: neg_mul, mul_neg
-- Module: Mathlib.RingTheory.Idempotents
Goal:
R : Type u_1
e : R
inst : NonUnitalRing R
a : R
⊢ -(fun (x : R) ↦ e * x * e) a ∈
    AddSubsemigroup.carrier
      (AddSubmonoid.toAddSubsemigroup (NonUnitalSubsemiring.toAddSubmonoid (NonUnitalSubsemiring.corner e)))

Tactic:
exact ⟨-a, by simp_rw [mul_neg, neg_mul]⟩
-- Module: Mathlib.RingTheory.Idempotents
Goal:
R : Type u_1
e : R
inst : NonUnitalSemiring R
idem : IsIdempotentElem e
simp_rw simp_rw₁ : e * e * e = e
⊢ (fun (x : R) ↦ e * x * e) e = e

Tactic:
simp_rw [idem.eq]

Premises used: IsIdempotentElem.eq
-- Module: Mathlib.RingTheory.Idempotents
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
simp_rw₆ : r * 1 = 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

Tactic:
simp_rw [((hc _).comm _).eq, mul_assoc, (he.idem _).eq, ← Finset.mul_sum, he.complete, mul_one]

Premises used: Finset.mul_sum, CompleteOrthogonalIdempotents.toOrthogonalIdempotents, mul_assoc, OrthogonalIdempotents.idem, IsMulCentral.comm, CompleteOrthogonalIdempotents.complete, IsIdempotentElem.eq, mul_one, Commute.eq
-- Module: Mathlib.RingTheory.Idempotents
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
simp_rw : ∑ i_1 : I, e i * (↑(r i_1) : R) * e i = (↑(r i) : 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) ⋯)
          ((fun (r : (i : I) → ⋯.Corner) ↦ (∑ i : I, (↑(r i) : R) : R)) r) i) :
      R) =
    (↑(r i) : R)

Tactic:
simp_rw [Finset.mul_sum, Finset.sum_mul]

Premises used: Finset.mul_sum, Finset.sum_mul
-- Module: Mathlib.RingTheory.Idempotents
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)
rw₁ : ∀ (b : I), Membership.mem (γ := Finset I) Finset.univ b → b ≠ i → e i * (↑(r b) : R) * e i = 0
⊢ ∑ i_1 : I, e i * (↑(r i_1) : R) * e i = (↑(r i) : R)

Tactic:
rw [Finset.sum_eq_single i _ (by simp at ·)]

Premises used: Finset.sum_eq_single
-- Module: Mathlib.RingTheory.Idempotents
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
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)
⊢ e i * (↑(r i) : R) * e i = (↑(r i) : R)

Tactic:
have ⟨r', eq⟩ := (r i).2
-- Module: Mathlib.RingTheory.Idempotents
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)
rw : e i * (fun (x : R) ↦ e i * x * e i) r' * e i = (fun (x : R) ↦ e i * x * e i) r'
⊢ e i * (↑(r i) : R) * e i = (↑(r i) : R)

Tactic:
rw [← eq]
-- Module: Mathlib.RingTheory.Idempotents
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
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'

Tactic:
simp_rw [← mul_assoc, (he.idem i).eq, mul_assoc, (he.idem i).eq]

Premises used: CompleteOrthogonalIdempotents.toOrthogonalIdempotents, mul_assoc, OrthogonalIdempotents.idem, IsIdempotentElem.eq
-- Module: Mathlib.RingTheory.Idempotents
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
_ : Membership.mem (γ := Finset I) Finset.univ j → j ≠ i → e i * (↑(r j) : R) * e i = 0
⊢ Membership.mem (γ := Finset I) Finset.univ j → j ≠ i → e i * (↑(r j) : R) * e i = 0

Tactic:
_
-- Module: Mathlib.RingTheory.Idempotents
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
have : ∀ (r' : R) (eq : (fun (x : R) ↦ e j * x * e j) r' = (↑(r j) : R)), e i * (↑(r j) : R) * e i = 0
⊢ e i * (↑(r j) : R) * e i = 0

Tactic:
have ⟨r', eq⟩ := (r j).2
-- Module: Mathlib.RingTheory.Idempotents
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)
rw : e i * (fun (x : R) ↦ e j * x * e j) r' * e i = 0
⊢ e i * (↑(r j) : R) * e i = 0

Tactic:
rw [← eq]
-- Module: Mathlib.RingTheory.Idempotents
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
simp_rw₃ : 0 * r' * e j * e i = 0
⊢ e i * (fun (x : R) ↦ e j * x * e j) r' * e i = 0

Tactic:
simp_rw [← mul_assoc, he.ortho ne.symm, zero_mul]

Premises used: CompleteOrthogonalIdempotents.toOrthogonalIdempotents, MulZeroClass.zero_mul, mul_assoc, Ne.symm, OrthogonalIdempotents.ortho
-- Module: Mathlib.RingTheory.Idempotents
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
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

Tactic:
simp_rw [← ((hc i).comm r₁).eq, ← mul_assoc, (he.idem i).eq]

Premises used: CompleteOrthogonalIdempotents.toOrthogonalIdempotents, mul_assoc, OrthogonalIdempotents.idem, IsMulCentral.comm, IsIdempotentElem.eq, Commute.eq
-- Module: Mathlib.RingTheory.Idempotents
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
rw : r₁ * (e i * e i) * r₂
| r₁ * e i * r₂

Tactic:
rw [← (he.idem i).eq]

Premises used: CompleteOrthogonalIdempotents.toOrthogonalIdempotents, OrthogonalIdempotents.idem, IsIdempotentElem.eq
-- Module: Mathlib.RingTheory.Idempotents
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
conv : e i * (r₁ * (e i * e i) * r₂) * e i = e i * r₁ * e i * (e i * r₂ * e i)
⊢ e i * (r₁ * 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]

Premises used: HMul.hMul, CompleteOrthogonalIdempotents.toOrthogonalIdempotents, OrthogonalIdempotents.idem, IsIdempotentElem.eq
-- Module: Mathlib.RingTheory.Idempotents
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 * e i) * r₂) * e i = e i * r₁ * e i * (e i * r₂ * e i)

Tactic:
simp_rw [mul_assoc]

Premises used: mul_assoc
-- Module: Mathlib.RingTheory.Idempotents
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
⊢ (↑(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) =
    (↑(HAdd.hAdd (α := (i : I) → ⋯.Corner) (β := (i : I) → ⋯.Corner)
          (fun (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 (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₂) ⋯)
          i) :
      R)

Tactic:
simpa [mul_add] using add_mul ..

Premises used: add_mul, mul_add
-- Module: Mathlib.RingTheory.Int.Basic
Goal:
a b : ℤ
rw : a.gcd b = 1 ↔ a.natAbs.Coprime b.natAbs
rw₁ : a.gcd b = 1 ↔ a.natAbs.gcd b.natAbs = 1
rw₂ rw₃ : a.natAbs.gcd b.natAbs = 1 ↔ a.natAbs.gcd b.natAbs = 1
⊢ IsCoprime a b ↔ a.natAbs.Coprime b.natAbs

Tactic:
rw [isCoprime_iff_gcd_eq_one, Nat.coprime_iff_gcd_eq_one, gcd_eq_natAbs]

Premises used: Int.isCoprime_iff_gcd_eq_one, Int.gcd_eq_natAbs, Nat.coprime_iff_gcd_eq_one
-- Module: Mathlib.RingTheory.Int.Basic
Goal:
a : ℤ
m n : ℕ
⊢ a.gcd (HMul.hMul (α := ℤ) (↑m : ℤ) (↑n : ℤ)) ≠ 1 ↔ a.gcd (↑m : ℤ) ≠ 1 ∨ a.gcd (↑n : ℤ) ≠ 1

Tactic:
simp only [← isCoprime_iff_gcd_eq_one, ← not_and_or, not_iff_not, IsCoprime.mul_right_iff]

Premises used: not_iff_not, Int.isCoprime_iff_gcd_eq_one, IsCoprime.mul_right_iff, not_and_or
-- Module: Mathlib.RingTheory.Int.Basic
Goal:
a b c : ℤ
h : a.gcd b = 1
heq : a * b = HPow.hPow (β := ℕ) c 2
rw : IsUnit (M := ℤ) 1
⊢ IsUnit (@GCDMonoid.gcd _ CommSemiring.toCommMonoidWithZero _ a b)

Tactic:
rw [← coe_gcd, h, Int.ofNat_one]

Premises used: Int.coe_gcd, Int.ofNat_one
-- Module: Mathlib.RingTheory.Int.Basic
Goal:
a b c : ℤ
h : a.gcd b = 1
heq : a * b = HPow.hPow (β := ℕ) c 2
⊢ IsUnit (M := ℤ) 1

Tactic:
isUnit_one

Premises used: isUnit_one
-- Module: Mathlib.RingTheory.Int.Basic
Goal:
a b c : ℤ
h : a.gcd b = 1
heq : a * b = HPow.hPow (β := ℕ) c 2
⊢ IsUnit (M := ℤ) 1

Tactic:
exact isUnit_one

Premises used: isUnit_one
-- Module: Mathlib.RingTheory.Int.Basic
Goal:
a b c : ℤ
h : a.gcd b = 1
heq : a * b = HPow.hPow (β := ℕ) c 2
⊢ 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
-- Module: Mathlib.RingTheory.Int.Basic
Goal:
a b c : ℤ
h : a.gcd b = 1
heq : a * b = HPow.hPow (β := ℕ) c 2
h' : IsUnit (@GCDMonoid.gcd _ CommSemiring.toCommMonoidWithZero _ a b)
obtain :
  ∀ (d : ℤ) (u : ℤˣ) (hu : HPow.hPow (β := ℕ) d 2 * (↑u : ℤ) = a),
    ∃ (a0 : ℤ), a = HPow.hPow (β := ℕ) a0 2 ∨ a = -HPow.hPow (β := ℕ) a0 2
⊢ ∃ (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

Premises used: exists_associated_pow_of_mul_eq_pow
-- Module: Mathlib.RingTheory.Int.Basic
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₁ : a = HPow.hPow (β := ℕ) d 2 ∨ a = -HPow.hPow (β := ℕ) d 2
⊢ ∃ (a0 : ℤ), a = HPow.hPow (β := ℕ) a0 2 ∨ a = -HPow.hPow (β := ℕ) a0 2

Tactic:
use d
-- Module: Mathlib.RingTheory.Int.Basic
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₁ :
  HPow.hPow (β := ℕ) d 2 * (↑u : ℤ) = HPow.hPow (β := ℕ) d 2 ∨
    HPow.hPow (β := ℕ) d 2 * (↑u : ℤ) = -HPow.hPow (β := ℕ) d 2
⊢ a = HPow.hPow (β := ℕ) d 2 ∨ a = -HPow.hPow (β := ℕ) d 2

Tactic:
rw [← hu]
-- Module: Mathlib.RingTheory.Int.Basic
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
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

Tactic:
rcases Int.units_eq_one_or u with hu' | hu'

Premises used: Int.units_eq_one_or
-- Module: Mathlib.RingTheory.Int.Basic
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
h₁ :
  HPow.hPow (β := ℕ) d 2 * (↑1 : ℤ) = HPow.hPow (β := ℕ) d 2 ∨
    HPow.hPow (β := ℕ) d 2 * (↑1 : ℤ) = -HPow.hPow (β := ℕ) d 2
⊢ HPow.hPow (β := ℕ) d 2 * (↑u : ℤ) = HPow.hPow (β := ℕ) d 2 ∨
    HPow.hPow (β := ℕ) d 2 * (↑u : ℤ) = -HPow.hPow (β := ℕ) d 2

Tactic:
rw [hu']
-- Module: Mathlib.RingTheory.Int.Basic
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 * (↑1 : ℤ) = HPow.hPow (β := ℕ) d 2 ∨
    HPow.hPow (β := ℕ) d 2 * (↑1 : ℤ) = -HPow.hPow (β := ℕ) d 2

Tactic:
simp
-- Module: Mathlib.RingTheory.Int.Basic
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
h₁ :
  HPow.hPow (β := ℕ) d 2 * (↑(-1) : ℤ) = HPow.hPow (β := ℕ) d 2 ∨
    HPow.hPow (β := ℕ) d 2 * (↑(-1) : ℤ) = -HPow.hPow (β := ℕ) d 2
⊢ HPow.hPow (β := ℕ) d 2 * (↑u : ℤ) = HPow.hPow (β := ℕ) d 2 ∨
    HPow.hPow (β := ℕ) d 2 * (↑u : ℤ) = -HPow.hPow (β := ℕ) d 2

Tactic:
rw [hu']
-- Module: Mathlib.RingTheory.Int.Basic
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 * (↑(-1) : ℤ) = HPow.hPow (β := ℕ) d 2 ∨
    HPow.hPow (β := ℕ) d 2 * (↑(-1) : ℤ) = -HPow.hPow (β := ℕ) d 2

Tactic:
simp
-- Module: Mathlib.RingTheory.Int.Basic
Goal:
a b c : ℤ
h : IsCoprime a b
heq : a * b = HPow.hPow (β := ℕ) c 2
⊢ ∃ (a0 : ℤ), a = HPow.hPow (β := ℕ) a0 2 ∨ a = -HPow.hPow (β := ℕ) a0 2

Tactic:
sq_of_gcd_eq_one (isCoprime_iff_gcd_eq_one.mp h) heq

Premises used: Int.isCoprime_iff_gcd_eq_one, Int.sq_of_gcd_eq_one, Iff.mp
-- Module: Mathlib.RingTheory.Int.Basic
Goal:
a b : ℤ
a₁ : (EuclideanDomain.gcd a b).natAbs ∣ a.gcd b
a₂ : a.gcd b ∣ (EuclideanDomain.gcd a b).natAbs
⊢ (EuclideanDomain.gcd a b).natAbs = a.gcd b

Tactic:
apply Nat.dvd_antisymm

Premises used: Nat.dvd_antisymm
-- Module: Mathlib.RingTheory.Int.Basic
Goal:
a b : ℤ
a₁ : Dvd.dvd (α := ℤ) (↑(EuclideanDomain.gcd a b).natAbs : ℤ) (↑(a.gcd b) : ℤ)
⊢ (EuclideanDomain.gcd a b).natAbs ∣ a.gcd b

Tactic:
rw [← Int.natCast_dvd_natCast]

Premises used: Int.natCast_dvd_natCast
-- Module: Mathlib.RingTheory.Int.Basic
Goal:
a b : ℤ
a₁ : Dvd.dvd (α := ℤ) (↑(a.gcd b) : ℤ) (↑(EuclideanDomain.gcd a b).natAbs : ℤ)
⊢ a.gcd b ∣ (EuclideanDomain.gcd a b).natAbs

Tactic:
rw [← Int.natCast_dvd_natCast]

Premises used: Int.natCast_dvd_natCast
-- Module: Mathlib.RingTheory.Int.Basic
Goal:
a b : ℤ
a₁ : EuclideanDomain.gcd a b ∣ (↑(a.gcd b) : ℤ)
⊢ Dvd.dvd (α := ℤ) (↑(EuclideanDomain.gcd a b).natAbs : ℤ) (↑(a.gcd b) : ℤ)

Tactic:
rw [Int.natAbs_dvd]

Premises used: Int.natAbs_dvd
-- Module: Mathlib.RingTheory.Int.Basic
Goal:
a b : ℤ
⊢ EuclideanDomain.gcd a b ∣ (↑(a.gcd b) : ℤ)

Tactic:
Int.dvd_coe_gcd (EuclideanDomain.gcd_dvd_left _ _) (EuclideanDomain.gcd_dvd_right _ _)

Premises used: Int.dvd_coe_gcd, EuclideanDomain.gcd_dvd_right, EuclideanDomain.gcd_dvd_left
-- Module: Mathlib.RingTheory.Int.Basic
Goal:
a b : ℤ
⊢ EuclideanDomain.gcd a b ∣ (↑(a.gcd b) : ℤ)

Tactic:
exact Int.dvd_coe_gcd (EuclideanDomain.gcd_dvd_left _ _) (EuclideanDomain.gcd_dvd_right _ _)

Premises used: Int.dvd_coe_gcd, EuclideanDomain.gcd_dvd_right, EuclideanDomain.gcd_dvd_left
-- Module: Mathlib.RingTheory.Int.Basic
Goal:
a b : ℤ
a₁ : (↑(a.gcd b) : ℤ) ∣ EuclideanDomain.gcd a b
⊢ Dvd.dvd (α := ℤ) (↑(a.gcd b) : ℤ) (↑(EuclideanDomain.gcd a b).natAbs : ℤ)

Tactic:
rw [Int.dvd_natAbs]

Premises used: Int.dvd_natAbs
-- Module: Mathlib.RingTheory.Int.Basic
Goal:
a b : ℤ
⊢ (↑(a.gcd b) : ℤ) ∣ EuclideanDomain.gcd a b

Tactic:
EuclideanDomain.dvd_gcd (Int.gcd_dvd_left ..) (Int.gcd_dvd_right ..)

Premises used: Int.gcd_dvd_left, EuclideanDomain.dvd_gcd, Int.gcd_dvd_right
-- Module: Mathlib.RingTheory.Int.Basic
Goal:
a b : ℤ
⊢ (↑(a.gcd b) : ℤ) ∣ EuclideanDomain.gcd a b

Tactic:
exact EuclideanDomain.dvd_gcd (Int.gcd_dvd_left ..) (Int.gcd_dvd_right ..)

Premises used: Int.gcd_dvd_left, EuclideanDomain.dvd_gcd, Int.gcd_dvd_right
-- Module: Mathlib.RingTheory.Int.Basic
Goal:
m n : ℤ
p : ℕ
hp : Nat.Prime p
h : (↑p : ℤ) ∣ m * n
rwa : p ∣ m.natAbs * n.natAbs
rwa₁ : p ∣ (m * n).natAbs
rwa₂ rwa₃ rwa₄ rwa₅ : (↑p : ℤ) ∣ m * n
⊢ p ∣ m.natAbs ∨ p ∣ n.natAbs

Tactic:
rwa [← hp.dvd_mul, ← Int.natAbs_mul, ← Int.natCast_dvd]

Premises used: Int.natAbs_mul, Nat.Prime.dvd_mul, Int.natCast_dvd
-- Module: Mathlib.RingTheory.Int.Basic
Goal:
m n : ℤ
p : ℕ
hp : Nat.Prime p
h : (↑p : ℤ) ∣ m * n
rw : p ∣ m.natAbs ∨ p ∣ n.natAbs
⊢ (↑p : ℤ) ∣ m ∨ (↑p : ℤ) ∣ n

Tactic:
rw [Int.natCast_dvd, Int.natCast_dvd]

Premises used: Int.natCast_dvd
-- Module: Mathlib.RingTheory.Int.Basic
Goal:
m n : ℤ
p : ℕ
hp : Nat.Prime p
h : (↑p : ℤ) ∣ m * n
⊢ p ∣ m.natAbs ∨ p ∣ n.natAbs

Tactic:
Int.Prime.dvd_mul hp h

Premises used: Int.Prime.dvd_mul
-- Module: Mathlib.RingTheory.Int.Basic
Goal:
m n : ℤ
p : ℕ
hp : Nat.Prime p
h : (↑p : ℤ) ∣ m * n
⊢ p ∣ m.natAbs ∨ p ∣ n.natAbs

Tactic:
exact Int.Prime.dvd_mul hp h

Premises used: Int.Prime.dvd_mul
-- Module: Mathlib.RingTheory.Int.Basic
Goal:
n : ℤ
k p : ℕ
hp : Nat.Prime p
h : (↑p : ℤ) ∣ n ^ k
⊢ p ∣ n.natAbs ^ k

Tactic:
rw [Int.natCast_dvd, Int.natAbs_pow] at h

Premises used: Int.natAbs_pow, Int.natCast_dvd
-- Module: Mathlib.RingTheory.Int.Basic
Goal:
n : ℤ
k p : ℕ
hp : Nat.Prime p
h : p ∣ n.natAbs ^ k
⊢ p ∣ n.natAbs

Tactic:
hp.dvd_of_dvd_pow h

Premises used: Nat.Prime.dvd_of_dvd_pow
-- Module: Mathlib.RingTheory.Int.Basic
Goal:
n : ℤ
k p : ℕ
hp : Nat.Prime p
h : p ∣ n.natAbs ^ k
⊢ p ∣ n.natAbs

Tactic:
exact hp.dvd_of_dvd_pow h

Premises used: Nat.Prime.dvd_of_dvd_pow