awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
x y z : ℤ
h : PythagoreanTriple x y z
h_coprime : x.gcd y = 1
h_parity : x % 2 = 1
h_pos : 0 < z
m n : ℤ
ht2 : z = HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2 ∨ z = -(HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2)
ht3 : m.gcd n = 1
ht4 : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0
hm : m < 0
h_even : x = 2 * m * n ∧ y = HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2
h₁ : False
⊢ x = HPow.hPow (β := ℕ) (-m) 2 - HPow.hPow (β := ℕ) (-n) 2 ∧
    y = 2 * -m * -n ∧
      z = HPow.hPow (β := ℕ) (-m) 2 + HPow.hPow (β := ℕ) (-n) 2 ∧
        (-m).gcd (-n) = 1 ∧ (-m % 2 = 0 ∧ -n % 2 = 1 ∨ -m % 2 = 1 ∧ -n % 2 = 0) ∧ 0 ≤ -m

Tactic:
exfalso
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
x y z : ℤ
h : PythagoreanTriple x y z
h_coprime : x.gcd y = 1
h_parity : x % 2 = 1
h_pos : 0 < z
m n : ℤ
ht2 : z = HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2 ∨ z = -(HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2)
ht3 : m.gcd n = 1
ht4 : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0
hm : m < 0
h_even : x = 2 * m * n ∧ y = HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2
⊢ PythagoreanTriple (2 * m * n) y z

Tactic:
rcases h_even with ⟨rfl, -⟩

Premises used: rfl
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
x y z : ℤ
h : PythagoreanTriple x y z
h_coprime : x.gcd y = 1
h_parity : x % 2 = 1
h_pos : 0 < z
m n : ℤ
ht2 : z = HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2 ∨ z = -(HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2)
ht3 : m.gcd n = 1
ht4 : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0
hm : m < 0
h_even : x = 2 * m * n ∧ y = HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2
h₁ : PythagoreanTriple (2 * m * n) y z
⊢ (2 * m * n).gcd y = 1

Tactic:
rcases h_even with ⟨rfl, -⟩

Premises used: rfl
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
x y z : ℤ
h : PythagoreanTriple x y z
h_coprime : x.gcd y = 1
h_parity : x % 2 = 1
h_pos : 0 < z
m n : ℤ
ht2 : z = HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2 ∨ z = -(HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2)
ht3 : m.gcd n = 1
ht4 : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0
hm : m < 0
h_even : x = 2 * m * n ∧ y = HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2
h₁ : PythagoreanTriple (2 * m * n) y z
h_coprime₁ : (2 * m * n).gcd y = 1
⊢ 2 * m * n % 2 = 1

Tactic:
rcases h_even with ⟨rfl, -⟩

Premises used: rfl
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
y z : ℤ
h_pos : 0 < z
m n : ℤ
ht2 : z = HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2 ∨ z = -(HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2)
ht3 : m.gcd n = 1
ht4 : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0
hm : m < 0
h : PythagoreanTriple (2 * m * n) y z
h_coprime : (2 * m * n).gcd y = 1
h_parity : 2 * m * n % 2 = 1
⊢ Eq (α := ℤ) 0 1

Tactic:
rw [mul_assoc, Int.mul_emod_right] at h_parity

Premises used: mul_assoc, Int.mul_emod_right
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
y z : ℤ
h_pos : 0 < z
m n : ℤ
ht2 : z = HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2 ∨ z = -(HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2)
ht3 : m.gcd n = 1
ht4 : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0
hm : m < 0
h : PythagoreanTriple (2 * m * n) y z
h_coprime : (2 * m * n).gcd y = 1
h_parity : Eq (α := ℤ) 0 1
⊢ False

Tactic:
zero_ne_one h_parity

Premises used: zero_ne_one
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
y z : ℤ
h_pos : 0 < z
m n : ℤ
ht2 : z = HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2 ∨ z = -(HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2)
ht3 : m.gcd n = 1
ht4 : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0
hm : m < 0
h : PythagoreanTriple (2 * m * n) y z
h_coprime : (2 * m * n).gcd y = 1
h_parity : Eq (α := ℤ) 0 1
⊢ False

Tactic:
exact zero_ne_one h_parity

Premises used: zero_ne_one
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
x y z : ℤ
mp :
  PythagoreanTriple x y z →
    ∃ (k : ℤ) (m : ℤ) (n : ℤ),
      (x = k * (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2) ∧ y = k * (2 * m * n) ∨
          x = k * (2 * m * n) ∧ y = k * (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2)) ∧
        (z = k * (HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2) ∨
          z = -k * (HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2))
mpr :
  (∃ (k : ℤ) (m : ℤ) (n : ℤ),
      (x = k * (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2) ∧ y = k * (2 * m * n) ∨
          x = k * (2 * m * n) ∧ y = k * (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2)) ∧
        (z = k * (HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2) ∨
          z = -k * (HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2))) →
    PythagoreanTriple x y z
⊢ PythagoreanTriple x y z ↔
    ∃ (k : ℤ) (m : ℤ) (n : ℤ),
      (x = k * (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2) ∧ y = k * (2 * m * n) ∨
          x = k * (2 * m * n) ∧ y = k * (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2)) ∧
        (z = k * (HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2) ∨
          z = -k * (HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2))

Tactic:
constructor
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
x y z : ℤ
h : PythagoreanTriple x y z
mp :
  ∀ (k m n : ℤ)
    (H :
      (x = k * (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2) ∧ y = k * (2 * m * n) ∨
          x = k * (2 * m * n) ∧ y = k * (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2)) ∧
        m.gcd n = 1),
    ∃ (k : ℤ) (m : ℤ) (n : ℤ),
      (x = k * (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2) ∧ y = k * (2 * m * n) ∨
          x = k * (2 * m * n) ∧ y = k * (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2)) ∧
        (z = k * (HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2) ∨
          z = -k * (HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2))
⊢ ∃ (k : ℤ) (m : ℤ) (n : ℤ),
    (x = k * (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2) ∧ y = k * (2 * m * n) ∨
        x = k * (2 * m * n) ∧ y = k * (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2)) ∧
      (z = k * (HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2) ∨
        z = -k * (HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2))

Tactic:
obtain ⟨k, m, n, H⟩ := h.classified

Premises used: PythagoreanTriple.classified
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
x y z : ℤ
h : PythagoreanTriple x y z
k m n : ℤ
H :
  (x = k * (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2) ∧ y = k * (2 * m * n) ∨
      x = k * (2 * m * n) ∧ y = k * (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2)) ∧
    m.gcd n = 1
h₁ :
  (x = k * (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2) ∧ y = k * (2 * m * n) ∨
      x = k * (2 * m * n) ∧ y = k * (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2)) ∧
    (z = k * (HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2) ∨
      z = -k * (HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2))
⊢ ∃ (k : ℤ) (m : ℤ) (n : ℤ),
    (x = k * (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2) ∧ y = k * (2 * m * n) ∨
        x = k * (2 * m * n) ∧ y = k * (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2)) ∧
      (z = k * (HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2) ∨
        z = -k * (HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2))

Tactic:
use k, m, n
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
x y z : ℤ
h : PythagoreanTriple x y z
k m n : ℤ
H :
  (x = k * (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2) ∧ y = k * (2 * m * n) ∨
      x = k * (2 * m * n) ∧ y = k * (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2)) ∧
    m.gcd n = 1
h₁ :
  m.gcd n = 1 →
    ∀ (h : PythagoreanTriple (k * (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2)) (k * (2 * m * n)) z),
      (k * (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2) = k * (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2) ∧
            k * (2 * m * n) = k * (2 * m * n) ∨
          k * (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2) = k * (2 * m * n) ∧
            k * (2 * m * n) = k * (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2)) ∧
        (z = k * (HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2) ∨
          z = -k * (HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2))
h₂ :
  m.gcd n = 1 →
    ∀ (h : PythagoreanTriple (k * (2 * m * n)) (k * (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2)) z),
      (k * (2 * m * n) = k * (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2) ∧
            k * (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2) = k * (2 * m * n) ∨
          k * (2 * m * n) = k * (2 * m * n) ∧
            k * (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2) =
              k * (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2)) ∧
        (z = k * (HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2) ∨
          z = -k * (HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2))
⊢ (x = k * (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2) ∧ y = k * (2 * m * n) ∨
      x = k * (2 * m * n) ∧ y = k * (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2)) ∧
    (z = k * (HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2) ∨
      z = -k * (HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2))

Tactic:
rcases H with (⟨rfl, rfl⟩ | ⟨rfl, rfl⟩)

Premises used: rfl
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
z k m n : ℤ
right : m.gcd n = 1
h : PythagoreanTriple (k * (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2)) (k * (2 * m * n)) z
⊢ (k * (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2) = k * (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2) ∧
        k * (2 * m * n) = k * (2 * m * n) ∨
      k * (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2) = k * (2 * m * n) ∧
        k * (2 * m * n) = k * (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2)) ∧
    (z = k * (HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2) ∨
      z = -k * (HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2))

Tactic:
⟨Or.inl ⟨rfl, rfl⟩, ?_⟩

Premises used: And.intro, Or.inl, rfl
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
z k m n : ℤ
right : m.gcd n = 1
h : PythagoreanTriple (k * (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2)) (k * (2 * m * n)) z
h₁ :
  z = k * (HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2) ∨ z = -k * (HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2)
⊢ (k * (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2) = k * (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2) ∧
        k * (2 * m * n) = k * (2 * m * n) ∨
      k * (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2) = k * (2 * m * n) ∧
        k * (2 * m * n) = k * (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2)) ∧
    (z = k * (HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2) ∨
      z = -k * (HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2))

Tactic:
refine ⟨Or.inl ⟨rfl, rfl⟩, ?_⟩
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
z k m n : ℤ
right : m.gcd n = 1
h : PythagoreanTriple (k * (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2)) (k * (2 * m * n)) z
rw :
  k * (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2) * (k * (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2)) +
      k * (2 * m * n) * (k * (2 * m * n)) =
    HPow.hPow (β := ℕ) (k * (HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2)) 2
⊢ HPow.hPow (β := ℕ) z 2 = HPow.hPow (β := ℕ) (k * (HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2)) 2

Tactic:
rw [sq, ← h.eq]

Premises used: sq, PythagoreanTriple.eq
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
z k m n : ℤ
right : m.gcd n = 1
h : PythagoreanTriple (k * (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2)) (k * (2 * m * n)) z
⊢ k * (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2) * (k * (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2)) +
      k * (2 * m * n) * (k * (2 * m * n)) =
    HPow.hPow (β := ℕ) (k * (HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2)) 2

Tactic:
ring
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
z k m n : ℤ
right : m.gcd n = 1
h : PythagoreanTriple (k * (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2)) (k * (2 * m * n)) z
⊢ HPow.hPow (β := ℕ) z 2 = HPow.hPow (β := ℕ) (k * (HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2)) 2

Tactic:
have : z ^ 2 = (k * (m ^ 2 + n ^ 2)) ^ 2 := by
        rw [sq, ← h.eq]
        ring
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
z k m n : ℤ
right : m.gcd n = 1
h : PythagoreanTriple (k * (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2)) (k * (2 * m * n)) z
this : HPow.hPow (β := ℕ) z 2 = HPow.hPow (β := ℕ) (k * (HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2)) 2
⊢ z = k * (HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2) ∨ z = -k * (HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2)

Tactic:
simpa using eq_or_eq_neg_of_sq_eq_sq _ _ this

Premises used: eq_or_eq_neg_of_sq_eq_sq
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
z k m n : ℤ
right : m.gcd n = 1
h : PythagoreanTriple (k * (2 * m * n)) (k * (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2)) z
⊢ (k * (2 * m * n) = k * (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2) ∧
        k * (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2) = k * (2 * m * n) ∨
      k * (2 * m * n) = k * (2 * m * n) ∧
        k * (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2) = k * (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2)) ∧
    (z = k * (HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2) ∨
      z = -k * (HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2))

Tactic:
⟨Or.inr ⟨rfl, rfl⟩, ?_⟩

Premises used: And.intro, Or.inr, rfl
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
z k m n : ℤ
right : m.gcd n = 1
h : PythagoreanTriple (k * (2 * m * n)) (k * (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2)) z
h₁ :
  z = k * (HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2) ∨ z = -k * (HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2)
⊢ (k * (2 * m * n) = k * (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2) ∧
        k * (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2) = k * (2 * m * n) ∨
      k * (2 * m * n) = k * (2 * m * n) ∧
        k * (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2) = k * (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2)) ∧
    (z = k * (HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2) ∨
      z = -k * (HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2))

Tactic:
refine ⟨Or.inr ⟨rfl, rfl⟩, ?_⟩
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
z k m n : ℤ
right : m.gcd n = 1
h : PythagoreanTriple (k * (2 * m * n)) (k * (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2)) z
rw :
  k * (2 * m * n) * (k * (2 * m * n)) +
      k * (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2) * (k * (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2)) =
    HPow.hPow (β := ℕ) (k * (HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2)) 2
⊢ HPow.hPow (β := ℕ) z 2 = HPow.hPow (β := ℕ) (k * (HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2)) 2

Tactic:
rw [sq, ← h.eq]

Premises used: sq, PythagoreanTriple.eq
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
z k m n : ℤ
right : m.gcd n = 1
h : PythagoreanTriple (k * (2 * m * n)) (k * (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2)) z
⊢ k * (2 * m * n) * (k * (2 * m * n)) +
      k * (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2) * (k * (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2)) =
    HPow.hPow (β := ℕ) (k * (HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2)) 2

Tactic:
ring
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
z k m n : ℤ
right : m.gcd n = 1
h : PythagoreanTriple (k * (2 * m * n)) (k * (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2)) z
⊢ HPow.hPow (β := ℕ) z 2 = HPow.hPow (β := ℕ) (k * (HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2)) 2

Tactic:
have : z ^ 2 = (k * (m ^ 2 + n ^ 2)) ^ 2 := by
        rw [sq, ← h.eq]
        ring
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
z k m n : ℤ
right : m.gcd n = 1
h : PythagoreanTriple (k * (2 * m * n)) (k * (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2)) z
this : HPow.hPow (β := ℕ) z 2 = HPow.hPow (β := ℕ) (k * (HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2)) 2
⊢ z = k * (HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2) ∨ z = -k * (HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2)

Tactic:
simpa using eq_or_eq_neg_of_sq_eq_sq _ _ this

Premises used: eq_or_eq_neg_of_sq_eq_sq
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
k m n : ℤ
⊢ k * (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2) * (k * (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2)) +
      k * (2 * m * n) * (k * (2 * m * n)) =
    k * (HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2) * (k * (HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2))

Tactic:
ring
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
k m n : ℤ
⊢ k * (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2) * (k * (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2)) +
      k * (2 * m * n) * (k * (2 * m * n)) =
    -k * (HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2) * (-k * (HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2))

Tactic:
ring
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
k m n : ℤ
⊢ k * (2 * m * n) * (k * (2 * m * n)) +
      k * (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2) * (k * (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2)) =
    k * (HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2) * (k * (HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2))

Tactic:
ring
-- Module: Mathlib.NumberTheory.PythagoreanTriples
Goal:
k m n : ℤ
⊢ k * (2 * m * n) * (k * (2 * m * n)) +
      k * (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2) * (k * (HPow.hPow (β := ℕ) m 2 - HPow.hPow (β := ℕ) n 2)) =
    -k * (HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2) * (-k * (HPow.hPow (β := ℕ) m 2 + HPow.hPow (β := ℕ) n 2))

Tactic:
ring
-- Module: Mathlib.NumberTheory.RamificationInertia.Basic
Goal:
R : Type u
inst : CommRing R
S : Type v
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
K : Type u_1
inst_3 : Field K
inst_4 : Algebra R K
L : Type u_2
inst_5 : Field L
inst_6 : Algebra S L
inst_7 : IsFractionRing S L
inst_8 : IsDomain R
inst_9 : IsDomain S
inst_10 : Algebra K L
inst_11 : Module.Finite R S
inst_12 : Algebra R L
inst_13 : IsScalarTower R S L
inst_14 : IsScalarTower R K L
inst_15 : Algebra.IsAlgebraic R S
inst_16 : IsTorsionFree R K
hp : p ≠ ⊤
b : Set S
hb' : Eq (α := Submodule R S) (Submodule.span R b ⊔ Submodule.restrictScalars R (map (F := R →+* S) f p)) ⊤
rw :
  Function.Injective.{u + 1, u_2 + 1} (α := R) (β := L)
    (⇑(@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap K L) (algebraMap R K)) : (a : R) → L)
⊢ Function.Injective.{u + 1, u_2 + 1} (α := R) (β := L) (⇑(algebraMap R L) : (a : R) → L)

Tactic:
rw [IsScalarTower.algebraMap_eq R K L]

Premises used: IsScalarTower.algebraMap_eq
-- Module: Mathlib.NumberTheory.RamificationInertia.Basic
Goal:
R : Type u
inst : CommRing R
S : Type v
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
K : Type u_1
inst_3 : Field K
inst_4 : Algebra R K
L : Type u_2
inst_5 : Field L
inst_6 : Algebra S L
inst_7 : IsFractionRing S L
inst_8 : IsDomain R
inst_9 : IsDomain S
inst_10 : Algebra K L
inst_11 : Module.Finite R S
inst_12 : Algebra R L
inst_13 : IsScalarTower R S L
inst_14 : IsScalarTower R K L
inst_15 : Algebra.IsAlgebraic R S
inst_16 : IsTorsionFree R K
hp : p ≠ ⊤
b : Set S
hb' : Eq (α := Submodule R S) (Submodule.span R b ⊔ Submodule.restrictScalars R (map (F := R →+* S) f p)) ⊤
⊢ Function.Injective.{u + 1, u_2 + 1} (α := R) (β := L)
    (⇑(@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap K L) (algebraMap R K)) : (a : R) → L)

Tactic:
(algebraMap K L).injective.comp (FaithfulSMul.algebraMap_injective R K)

Premises used: Algebra.algebraMap, RingHom.injective, Function.Injective.comp, FaithfulSMul.algebraMap_injective
-- Module: Mathlib.NumberTheory.RamificationInertia.Basic
Goal:
R : Type u
inst : CommRing R
S : Type v
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
K : Type u_1
inst_3 : Field K
inst_4 : Algebra R K
L : Type u_2
inst_5 : Field L
inst_6 : Algebra S L
inst_7 : IsFractionRing S L
inst_8 : IsDomain R
inst_9 : IsDomain S
inst_10 : Algebra K L
inst_11 : Module.Finite R S
inst_12 : Algebra R L
inst_13 : IsScalarTower R S L
inst_14 : IsScalarTower R K L
inst_15 : Algebra.IsAlgebraic R S
inst_16 : IsTorsionFree R K
hp : p ≠ ⊤
b : Set S
hb' : Eq (α := Submodule R S) (Submodule.span R b ⊔ Submodule.restrictScalars R (map (F := R →+* S) f p)) ⊤
⊢ Function.Injective.{u + 1, u_2 + 1} (α := R) (β := L)
    (⇑(@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap K L) (algebraMap R K)) : (a : R) → L)

Tactic:
exact (algebraMap K L).injective.comp (FaithfulSMul.algebraMap_injective R K)

Premises used: Algebra.algebraMap, RingHom.injective, Function.Injective.comp, FaithfulSMul.algebraMap_injective
-- Module: Mathlib.NumberTheory.RamificationInertia.Basic
Goal:
R : Type u
inst : CommRing R
S : Type v
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
K : Type u_1
inst_3 : Field K
inst_4 : Algebra R K
L : Type u_2
inst_5 : Field L
inst_6 : Algebra S L
inst_7 : IsFractionRing S L
inst_8 : IsDomain R
inst_9 : IsDomain S
inst_10 : Algebra K L
inst_11 : Module.Finite R S
inst_12 : Algebra R L
inst_13 : IsScalarTower R S L
inst_14 : IsScalarTower R K L
inst_15 : Algebra.IsAlgebraic R S
inst_16 : IsTorsionFree R K
hp : p ≠ ⊤
b : Set S
hb' : Eq (α := Submodule R S) (Submodule.span R b ⊔ Submodule.restrictScalars R (map (F := R →+* S) f p)) ⊤
⊢ Function.Injective.{u + 1, u_2 + 1} (α := R) (β := L) (⇑(algebraMap R L) : (a : R) → L)

Tactic:
have hRL : Function.Injective (algebraMap R L) := by
    rw [IsScalarTower.algebraMap_eq R K L]
    exact (algebraMap K L).injective.comp (FaithfulSMul.algebraMap_injective R K)
-- Module: Mathlib.NumberTheory.RamificationInertia.Basic
Goal:
R : Type u
inst : CommRing R
S : Type v
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
K : Type u_1
inst_3 : Field K
inst_4 : Algebra R K
L : Type u_2
inst_5 : Field L
inst_6 : Algebra S L
inst_7 : IsFractionRing S L
inst_8 : IsDomain R
inst_9 : IsDomain S
inst_10 : Algebra K L
inst_11 : Module.Finite R S
inst_12 : Algebra R L
inst_13 : IsScalarTower R S L
inst_14 : IsScalarTower R K L
inst_15 : Algebra.IsAlgebraic R S
inst_16 : IsTorsionFree R K
hp : p ≠ ⊤
b : Set S
hb' : Eq (α := Submodule R S) (Submodule.span R b ⊔ Submodule.restrictScalars R (map (F := R →+* S) f p)) ⊤
hRL : Function.Injective.{u + 1, u_2 + 1} (α := R) (β := L) (⇑(algebraMap R L) : (a : R) → L)
M : Submodule R S := Submodule.span R b
obtain :
  ∀ (n : ℕ) (a : Fin n → S ⧸ M) (ha : Eq (α := Submodule R (S ⧸ M)) (Submodule.span R (Set.range a)) ⊤),
    Eq.{u_2 + 1} (α := Submodule K L) (Submodule.span K ((⇑(algebraMap S L) : (a : S) → L) '' b)) ⊤
⊢ Eq.{u_2 + 1} (α := Submodule K L) (Submodule.span K ((⇑(algebraMap S L) : (a : S) → L) '' b)) ⊤

Tactic:
obtain ⟨n, a, ha⟩ := @Module.Finite.exists_fin R (S ⧸ M) _ _ _ _

Premises used: Module.Finite.exists_fin
-- Module: Mathlib.NumberTheory.RamificationInertia.Basic
Goal:
R : Type u
inst : CommRing R
S : Type v
inst_1 : CommRing S
inst_2 : Algebra R S
p : Ideal R
K : Type u_1
inst_3 : Field K
inst_4 : Algebra R K
L : Type u_2
inst_5 : Field L
inst_6 : Algebra S L
inst_7 : IsFractionRing S L
inst_8 : IsDomain R
inst_9 : IsDomain S
inst_10 : Algebra K L
inst_11 : Module.Finite R S
inst_12 : Algebra R L
inst_13 : IsScalarTower R S L
inst_14 : IsScalarTower R K L
inst_15 : Algebra.IsAlgebraic R S
inst_16 : IsTorsionFree R K
hp : p ≠ ⊤
b : Set S
hb' : Eq (α := Submodule R S) (Submodule.span R b ⊔ Submodule.restrictScalars R (map (F := R →+* S) f p)) ⊤
hRL : Function.Injective.{u + 1, u_2 + 1} (α := R) (β := L) (⇑(algebraMap R L) : (a : R) → L)
M : Submodule R S := Submodule.span R b
n : ℕ
a : Fin n → S ⧸ M
ha : Eq (α := Submodule R (S ⧸ M)) (Submodule.span R (Set.range a)) ⊤
rw : HSMul.hSMul (β := Submodule R (S ⧸ M)) p ⊤ = HSMul.hSMul (β := Submodule R (S ⧸ M)) p (Submodule.map M.mkQ ⊤)
rw₁ : HSMul.hSMul (β := Submodule R (S ⧸ M)) p ⊤ = HSMul.hSMul (β := Submodule R (S ⧸ M)) p (LinearMap.range M.mkQ)
rw₂ rw₃ : HSMul.hSMul (β := Submodule R (S ⧸ M)) p ⊤ = HSMul.hSMul (β := Submodule R (S ⧸ M)) p ⊤
⊢ HSMul.hSMul (β := Submodule R (S ⧸ M)) p ⊤ = Submodule.map M.mkQ (HSMul.hSMul (β := Submodule R S) p ⊤)

Tactic:
rw [Submodule.map_smul'', Submodule.map_top, M.range_mkQ]

Premises used: Submodule.map_smul'', Submodule.map_top, Submodule.range_mkQ