Theorem: dvd_iff_nat_dvd (meetings/ex6.lean)

State before:
a b : ℕplus
⊢ R3 a b ↔ ↑a ∣ ↑b
Tactic:
constructor
State after:
case mp
a b : ℕplus
⊢ R3 a b → ↑a ∣ ↑b

case mpr
a b : ℕplus
⊢ ↑a ∣ ↑b → R3 a b

State before:
case mp
a b : ℕplus
⊢ R3 a b → ↑a ∣ ↑b
Tactic:
intro hdvd
State after:
case mp
a b : ℕplus
hdvd : R3 a b
⊢ ↑a ∣ ↑b

State before:
case mp
a b : ℕplus
hdvd : R3 a b
⊢ ↑a ∣ ↑b
Tactic:
rcases hdvd with ⟨c, hc⟩
State after:
case mp.intro
a b c : ℕplus
hc : b = a * c
⊢ ↑a ∣ ↑b

State before:
case mp.intro
a b c : ℕplus
hc : b = a * c
⊢ ↑a ∣ ↑b
Tactic:
use c.val
State after:
case h
a b c : ℕplus
hc : b = a * c
⊢ ↑b = ↑a * ↑c

State before:
case h
a b c : ℕplus
hc : b = a * c
⊢ ↑b = ↑a * ↑c
Tactic:
rw [ℕplus.mul_def] at hc
State after:
case h
a b c : ℕplus
hc : b = { val := ↑a * ↑c, property := (_ : ↑a * ↑c ≠ 0) }
⊢ ↑b = ↑a * ↑c

State before:
case h
a b c : ℕplus
hc : b = { val := ↑a * ↑c, property := (_ : ↑a * ↑c ≠ 0) }
⊢ ↑b = ↑a * ↑c
Tactic:
apply_fun Subtype.val at hc
State after:
case h
a b c : ℕplus
hc : ↑b = ↑{ val := ↑a * ↑c, property := (_ : ↑a * ↑c ≠ 0) }
⊢ ↑b = ↑a * ↑c

State before:
case h
a b c : ℕplus
hc : ↑b = ↑{ val := ↑a * ↑c, property := (_ : ↑a * ↑c ≠ 0) }
⊢ ↑b = ↑a * ↑c
Tactic:
exact hc
State after:
no goals

State before:
case mpr
a b : ℕplus
⊢ ↑a ∣ ↑b → R3 a b
Tactic:
intro hdvd
State after:
case mpr
a b : ℕplus
hdvd : ↑a ∣ ↑b
⊢ R3 a b

State before:
case mpr
a b : ℕplus
hdvd : ↑a ∣ ↑b
⊢ R3 a b
Tactic:
rcases hdvd with ⟨c, hc⟩
State after:
case mpr.intro
a b : ℕplus
c : ℕ
hc : ↑b = ↑a * c
⊢ R3 a b

State before:
case mpr.intro
a b : ℕplus
c : ℕ
hc : ↑b = ↑a * c
⊢ R3 a b
Tactic:
have hb := b.property
State after:
case mpr.intro
a b : ℕplus
c : ℕ
hc : ↑b = ↑a * c
hb : ↑b ≠ 0
⊢ R3 a b

State before:
case mpr.intro
a b : ℕplus
c : ℕ
hc : ↑b = ↑a * c
hb : ↑b ≠ 0
⊢ R3 a b
Tactic:
rw [hc, mul_ne_zero_iff] at hb
State after:
case mpr.intro
a b : ℕplus
c : ℕ
hc : ↑b = ↑a * c
hb : ↑a ≠ 0 ∧ c ≠ 0
⊢ R3 a b

State before:
case mpr.intro
a b : ℕplus
c : ℕ
hc : ↑b = ↑a * c
hb : ↑a ≠ 0 ∧ c ≠ 0
⊢ R3 a b
Tactic:
let lc : ℕplus := ⟨c, hb.2⟩
State after:
case mpr.intro
a b : ℕplus
c : ℕ
hc : ↑b = ↑a * c
hb : ↑a ≠ 0 ∧ c ≠ 0
lc : ℕplus := { val := c, property := (_ : c ≠ 0) }
⊢ R3 a b

State before:
case mpr.intro
a b : ℕplus
c : ℕ
hc : ↑b = ↑a * c
hb : ↑a ≠ 0 ∧ c ≠ 0
lc : ℕplus := { val := c, property := (_ : c ≠ 0) }
⊢ R3 a b
Tactic:
use lc
State after:
case h
a b : ℕplus
c : ℕ
hc : ↑b = ↑a * c
hb : ↑a ≠ 0 ∧ c ≠ 0
lc : ℕplus := { val := c, property := (_ : c ≠ 0) }
⊢ b = a * lc

State before:
case h
a b : ℕplus
c : ℕ
hc : ↑b = ↑a * c
hb : ↑a ≠ 0 ∧ c ≠ 0
lc : ℕplus := { val := c, property := (_ : c ≠ 0) }
⊢ b = a * lc
Tactic:
rw [Subtype.ext_iff]
State after:
case h
a b : ℕplus
c : ℕ
hc : ↑b = ↑a * c
hb : ↑a ≠ 0 ∧ c ≠ 0
lc : ℕplus := { val := c, property := (_ : c ≠ 0) }
⊢ ↑b = ↑(a * lc)

State before:
case h
a b : ℕplus
c : ℕ
hc : ↑b = ↑a * c
hb : ↑a ≠ 0 ∧ c ≠ 0
lc : ℕplus := { val := c, property := (_ : c ≠ 0) }
⊢ ↑b = ↑(a * lc)
Tactic:
exact hc
State after:
no goals