提交 #12

import Mathlib.Data.Real.Basic
section ProblemA

variable (P Q : Nat → Prop)
variable (R : Nat → Nat → Prop)

mutual
inductive A : Nat → Prop
| ca0 : ∀ n, P n → A n
| ca1 : ∀ n1, (∀ n2, R n1 n2 → B n2) → A n1

inductive B : Nat → Prop
| cb0 : ∀ n, Q n → B n
| cb1 : ∀ n1 n2, R n1 n2 → A n2 → B n1
end
open A B

-- #check A.rec
lemma neg_a :
  (∀ n, ¬ P n ∧ ¬ Q n) →
  (∀ n1, ∃ n2, R n1 n2) →
  (∀ n, A P Q R n → False) :=
by
  intro Hpq Hr

  have hc:= A.rec
          (motive_1 := fun a (_: A P Q R a) => False)
          (motive_2 := fun a (_: B P Q R a) => False)
  apply hc
  focus
    intro n Ha
    specialize Hpq n
    specialize Hr n
    rcases Hpq with ⟨Ha, Hb⟩
    apply Ha
    assumption

  focus
    intro n Hn1 Hn2
    specialize Hr n
    rcases Hr with ⟨r, Hr⟩
    specialize Hn2 r
    apply Hn2
    assumption

  focus
    intros n Hq
    specialize Hpq n
    rcases Hpq with ⟨Ha, Hb⟩
    apply Hb
    assumption

  focus
    intros n1 n2 Hr Ha Hf
    assumption
end ProblemA