Theorem: Imo1989P5.modulus_of_product (Compfiles/Imo1989P5.lean)

State before:
a b : ℕ
xs : List ℕ
h : a ≡ b [MOD xs.prod]
x : ℕ
hx : x ∈ xs
⊢ a ≡ b [MOD x]
Tactic:
induction xs with
| nil => aesop
| cons y ys ih =>
  rw [List.prod_cons] at h
  cases hx with
  | head => exact Nat.ModEq.of_mul_right _ h
  | tail w hw =>
    exact ih (Nat.ModEq.of_mul_left _ h) hw
State after:
no goals

State before:
case nil
a b x : ℕ
h : a ≡ b [MOD [].prod]
hx : x ∈ []
⊢ a ≡ b [MOD x]
Tactic:
aesop
State after:
no goals

State before:
case cons
a b x y : ℕ
ys : List ℕ
ih : a ≡ b [MOD ys.prod] → x ∈ ys → a ≡ b [MOD x]
h : a ≡ b [MOD (y :: ys).prod]
hx : x ∈ y :: ys
⊢ a ≡ b [MOD x]
Tactic:
rw [List.prod_cons] at h
State after:
case cons
a b x y : ℕ
ys : List ℕ
ih : a ≡ b [MOD ys.prod] → x ∈ ys → a ≡ b [MOD x]
h : a ≡ b [MOD y * ys.prod]
hx : x ∈ y :: ys
⊢ a ≡ b [MOD x]

State before:
case cons
a b x y : ℕ
ys : List ℕ
ih : a ≡ b [MOD ys.prod] → x ∈ ys → a ≡ b [MOD x]
h : a ≡ b [MOD y * ys.prod]
hx : x ∈ y :: ys
⊢ a ≡ b [MOD x]
Tactic:
cases hx with
| head => exact Nat.ModEq.of_mul_right _ h
| tail w hw =>
  exact ih (Nat.ModEq.of_mul_left _ h) hw
State after:
no goals

State before:
case cons.head
a b x : ℕ
ys : List ℕ
ih : a ≡ b [MOD ys.prod] → x ∈ ys → a ≡ b [MOD x]
h : a ≡ b [MOD x * ys.prod]
⊢ a ≡ b [MOD x]
Tactic:
exact Nat.ModEq.of_mul_right _ h
State after:
no goals

State before:
case cons.tail
a b x y : ℕ
ys : List ℕ
ih : a ≡ b [MOD ys.prod] → x ∈ ys → a ≡ b [MOD x]
h : a ≡ b [MOD y * ys.prod]
hw : List.Mem x ys
⊢ a ≡ b [MOD x]
Tactic:
exact ih (Nat.ModEq.of_mul_left _ h) hw
State after:
no goals