Theorem: Usa2019P1.pnat_odd_mul (Compfiles/Usa2019P1.lean)

State before:
a b c : ℕ+
h : a * b = c * c
hc : Odd ↑c
⊢ Odd ↑a ∧ Odd ↑b
Tactic:
obtain ⟨a, ha⟩ := a
State after:
case mk
b c : ℕ+
hc : Odd ↑c
a : ℕ
ha : 0 < a
h : ⟨a, ha⟩ * b = c * c
⊢ Odd ↑⟨a, ha⟩ ∧ Odd ↑b

State before:
case mk
b c : ℕ+
hc : Odd ↑c
a : ℕ
ha : 0 < a
h : ⟨a, ha⟩ * b = c * c
⊢ Odd ↑⟨a, ha⟩ ∧ Odd ↑b
Tactic:
obtain ⟨b, hb⟩ := b
State after:
case mk.mk
c : ℕ+
hc : Odd ↑c
a : ℕ
ha : 0 < a
b : ℕ
hb : 0 < b
h : ⟨a, ha⟩ * ⟨b, hb⟩ = c * c
⊢ Odd ↑⟨a, ha⟩ ∧ Odd ↑⟨b, hb⟩

State before:
case mk.mk
c : ℕ+
hc : Odd ↑c
a : ℕ
ha : 0 < a
b : ℕ
hb : 0 < b
h : ⟨a, ha⟩ * ⟨b, hb⟩ = c * c
⊢ Odd ↑⟨a, ha⟩ ∧ Odd ↑⟨b, hb⟩
Tactic:
obtain ⟨c, hc⟩ := c
State after:
case mk.mk.mk
a : ℕ
ha : 0 < a
b : ℕ
hb : 0 < b
c : ℕ
hc✝ : 0 < c
hc : Odd ↑⟨c, hc✝⟩
h : ⟨a, ha⟩ * ⟨b, hb⟩ = ⟨c, hc✝⟩ * ⟨c, hc✝⟩
⊢ Odd ↑⟨a, ha⟩ ∧ Odd ↑⟨b, hb⟩

State before:
case mk.mk.mk
a : ℕ
ha : 0 < a
b : ℕ
hb : 0 < b
c : ℕ
hc✝ : 0 < c
hc : Odd ↑⟨c, hc✝⟩
h : ⟨a, ha⟩ * ⟨b, hb⟩ = ⟨c, hc✝⟩ * ⟨c, hc✝⟩
⊢ Odd ↑⟨a, ha⟩ ∧ Odd ↑⟨b, hb⟩
Tactic:
simp only [PNat.mk_coe]
State after:
case mk.mk.mk
a : ℕ
ha : 0 < a
b : ℕ
hb : 0 < b
c : ℕ
hc✝ : 0 < c
hc : Odd ↑⟨c, hc✝⟩
h : ⟨a, ha⟩ * ⟨b, hb⟩ = ⟨c, hc✝⟩ * ⟨c, hc✝⟩
⊢ Odd a ∧ Odd b

State before:
case mk.mk.mk
a : ℕ
ha : 0 < a
b : ℕ
hb : 0 < b
c : ℕ
hc✝ : 0 < c
hc : Odd ↑⟨c, hc✝⟩
h : ⟨a, ha⟩ * ⟨b, hb⟩ = ⟨c, hc✝⟩ * ⟨c, hc✝⟩
⊢ Odd a ∧ Odd b
Tactic:
rw [PNat.mk_coe] at hc
State after:
case mk.mk.mk
a : ℕ
ha : 0 < a
b : ℕ
hb : 0 < b
c : ℕ
hc✝ : 0 < c
hc : Odd c
h : ⟨a, ha⟩ * ⟨b, hb⟩ = ⟨c, hc✝⟩ * ⟨c, hc✝⟩
⊢ Odd a ∧ Odd b

State before:
case mk.mk.mk
a : ℕ
ha : 0 < a
b : ℕ
hb : 0 < b
c : ℕ
hc✝ : 0 < c
hc : Odd c
h : ⟨a, ha⟩ * ⟨b, hb⟩ = ⟨c, hc✝⟩ * ⟨c, hc✝⟩
⊢ Odd a ∧ Odd b
Tactic:
apply_fun (fun x ↦ x.val) at h
State after:
case mk.mk.mk
a : ℕ
ha : 0 < a
b : ℕ
hb : 0 < b
c : ℕ
hc✝ : 0 < c
hc : Odd c
h : ↑(⟨a, ha⟩ * ⟨b, hb⟩) = ↑(⟨c, hc✝⟩ * ⟨c, hc✝⟩)
⊢ Odd a ∧ Odd b

State before:
case mk.mk.mk
a : ℕ
ha : 0 < a
b : ℕ
hb : 0 < b
c : ℕ
hc✝ : 0 < c
hc : Odd c
h : ↑(⟨a, ha⟩ * ⟨b, hb⟩) = ↑(⟨c, hc✝⟩ * ⟨c, hc✝⟩)
⊢ Odd a ∧ Odd b
Tactic:
dsimp at h
State after:
case mk.mk.mk
a : ℕ
ha : 0 < a
b : ℕ
hb : 0 < b
c : ℕ
hc✝ : 0 < c
hc : Odd c
h : a * b = c * c
⊢ Odd a ∧ Odd b

State before:
case mk.mk.mk
a : ℕ
ha : 0 < a
b : ℕ
hb : 0 < b
c : ℕ
hc✝ : 0 < c
hc : Odd c
h : a * b = c * c
⊢ Odd a ∧ Odd b
Tactic:
have h1 : Odd (c * c) := Odd.mul hc hc
State after:
case mk.mk.mk
a : ℕ
ha : 0 < a
b : ℕ
hb : 0 < b
c : ℕ
hc✝ : 0 < c
hc : Odd c
h : a * b = c * c
h1 : Odd (c * c)
⊢ Odd a ∧ Odd b

State before:
case mk.mk.mk
a : ℕ
ha : 0 < a
b : ℕ
hb : 0 < b
c : ℕ
hc✝ : 0 < c
hc : Odd c
h : a * b = c * c
h1 : Odd (c * c)
⊢ Odd a ∧ Odd b
Tactic:
rw [←h] at h1
State after:
case mk.mk.mk
a : ℕ
ha : 0 < a
b : ℕ
hb : 0 < b
c : ℕ
hc✝ : 0 < c
hc : Odd c
h : a * b = c * c
h1 : Odd (a * b)
⊢ Odd a ∧ Odd b

State before:
case mk.mk.mk
a : ℕ
ha : 0 < a
b : ℕ
hb : 0 < b
c : ℕ
hc✝ : 0 < c
hc : Odd c
h : a * b = c * c
h1 : Odd (a * b)
⊢ Odd a ∧ Odd b
Tactic:
exact Nat.odd_mul.mp h1
State after:
no goals