case inl
b : ℕ
h : 0 ∣ b
⊢ φ 0 ∣ φ b

case inr
a b : ℕ
h : a ∣ b
ha0 : a ≠ 0
⊢ φ a ∣ φ b
a b : ℕ
h : a ∣ b
⊢ φ a ∣ φ b
rcases eq_or_ne a 0 with (rfl | ha0)
case inr.inl
a : ℕ
ha0 : a ≠ 0
h : a ∣ 0
⊢ φ a ∣ φ 0

case inr.inr
a b : ℕ
h : a ∣ b
ha0 : a ≠ 0
hb0 : b ≠ 0
⊢ φ a ∣ φ b
case inr
a b : ℕ
h : a ∣ b
ha0 : a ≠ 0
⊢ φ a ∣ φ b
rcases eq_or_ne b 0 with (rfl | hb0)
case inr.inr
a b : ℕ
h : a ∣ b
ha0 : a ≠ 0
hb0 : b ≠ 0
hab' : (factorization a).support ⊆ (factorization b).support
⊢ φ a ∣ φ b
case inr.inr
a b : ℕ
h : a ∣ b
ha0 : a ≠ 0
hb0 : b ≠ 0
⊢ φ a ∣ φ b
have hab' : a.factorization.support ⊆ b.factorization.support := by
  intro p
  simp only [support_factorization, List.mem_toFinset]
  apply factors_subset_of_dvd h hb0
case inr.inr
a b : ℕ
h : a ∣ b
ha0 : a ≠ 0
hb0 : b ≠ 0
hab' : (factorization a).support ⊆ (factorization b).support
⊢ (Finsupp.prod (factorization a) fun p k => p ^ (k - 1) * (p - 1)) ∣
    Finsupp.prod (factorization b) fun p k => p ^ (k - 1) * (p - 1)
case inr.inr
a b : ℕ
h : a ∣ b
ha0 : a ≠ 0
hb0 : b ≠ 0
hab' : (factorization a).support ⊆ (factorization b).support
⊢ φ a ∣ φ b
rw [totient_eq_prod_factorization ha0, totient_eq_prod_factorization hb0]
case inr.inr
a b : ℕ
h : a ∣ b
ha0 : a ≠ 0
hb0 : b ≠ 0
hab' : (factorization a).support ⊆ (factorization b).support
p : ℕ
x✝ : p ∈ (factorization a).support
⊢ p ^ (↑(factorization a) p - 1) ∣ p ^ (↑(factorization b) p - 1)
case inr.inr
a b : ℕ
h : a ∣ b
ha0 : a ≠ 0
hb0 : b ≠ 0
hab' : (factorization a).support ⊆ (factorization b).support
⊢ (Finsupp.prod (factorization a) fun p k => p ^ (k - 1) * (p - 1)) ∣
    Finsupp.prod (factorization b) fun p k => p ^ (k - 1) * (p - 1)
refine' Finsupp.prod_dvd_prod_of_subset_of_dvd hab' fun p _ => mul_dvd_mul _ dvd_rfl
no goals
case inr.inr
a b : ℕ
h : a ∣ b
ha0 : a ≠ 0
hb0 : b ≠ 0
hab' : (factorization a).support ⊆ (factorization b).support
p : ℕ
x✝ : p ∈ (factorization a).support
⊢ p ^ (↑(factorization a) p - 1) ∣ p ^ (↑(factorization b) p - 1)
exact pow_dvd_pow p (tsub_le_tsub_right ((factorization_le_iff_dvd ha0 hb0).2 h p) 1)
no goals
case inl
b : ℕ
h : 0 ∣ b
⊢ φ 0 ∣ φ b
simp [zero_dvd_iff.1 h]
no goals
case inr.inl
a : ℕ
ha0 : a ≠ 0
h : a ∣ 0
⊢ φ a ∣ φ 0
simp
a b : ℕ
h : a ∣ b
ha0 : a ≠ 0
hb0 : b ≠ 0
p : ℕ
⊢ p ∈ (factorization a).support → p ∈ (factorization b).support
a b : ℕ
h : a ∣ b
ha0 : a ≠ 0
hb0 : b ≠ 0
⊢ (factorization a).support ⊆ (factorization b).support
intro p
a b : ℕ
h : a ∣ b
ha0 : a ≠ 0
hb0 : b ≠ 0
p : ℕ
⊢ p ∈ factors a → p ∈ factors b
a b : ℕ
h : a ∣ b
ha0 : a ≠ 0
hb0 : b ≠ 0
p : ℕ
⊢ p ∈ (factorization a).support → p ∈ (factorization b).support
simp only [support_factorization, List.mem_toFinset]
no goals
a b : ℕ
h : a ∣ b
ha0 : a ≠ 0
hb0 : b ≠ 0
p : ℕ
⊢ p ∈ factors a → p ∈ factors b
apply factors_subset_of_dvd h hb0