Repetitive proofs...

a.lean

import Mathlib.Tactic

open Nat Finset

variable (A B X : Finset ℕ) {α : Type*} [LinearOrder α] {s : Finset α} {p : Finset α → Prop}

def multiples (a : ℕ) := X.filter (fun x ↦ a ∣ x)
def PredElement (a : ℕ) := ¬Even (multiples B a).card
instance : DecidablePred (PredElement X) := by intro ; exact Not.decidable
def Pred : Finset ℕ := X.filter $ PredElement B

/- Missing mathlib stuff -/
theorem min_not_mem (hm : ∀ a ∈ s, m < a) : m ∉ s := fun a ↦ (hm m a).false
theorem ind_min (s : Finset α) (hz : p ∅)
    (hi : ∀ m t (hm : ∀ a, a ∈ t → m < a), p t → p (cons m t <| min_not_mem hm)) :
    p s := by
  sorry

theorem A11 (hX : 0 ∉ X) (hA : A ⊆ X) : ∃ B, B ⊆ X ∧ Pred B X = A := by
  induction' X using ind_min with m X hm hind generalizing A
  · use ∅ ; simp [Pred, subset_empty.mp hA]
  · set A' := A.filter (fun x ↦ x ≠ m) with hA'
    let ⟨B', ⟨hB'₁, hB'₂⟩⟩ := hind A' (by sorry) (by sorry)
    /- We construct B as B' or B' ∪ {m} -/
    rw [Pred] at hB'₂
    by_cases hm₁ : m ∈ A <;> by_cases hm₂ : (PredElement B' m)
    · use B'
      constructor
      /- (1) -/
      · refine subset_trans hB'₁ $ subset_cons $ min_not_mem hm
      /- (2) -/
      · simp only [Pred, filter_cons, hm₂, ite_true, hB'₂, disjUnion_eq_union]
        nth_rewrite 2 [←filter_union_filter_neg_eq (fun x => x = m) A]
        congr
        simp only [filter_eq', hm₁, ite_true]
    save
    · use B' ∪ {m}
      constructor
      /- (3) = (1) + (3)' -/
      · apply union_subset
        · refine subset_trans hB'₁ $ subset_cons $ min_not_mem hm
        · rw [singleton_subset_iff]
          apply mem_cons_self
      · sorry
    · use B' ∪ {m}
      constructor
      /- (3) = (1) + (3)' -/
      · apply union_subset
        · refine subset_trans hB'₁ $ subset_cons $ min_not_mem hm
        · rw [singleton_subset_iff]
          apply mem_cons_self
      · sorry
    · use B'
      constructor
      /- (1) -/
      · refine subset_trans hB'₁ $ subset_cons $ min_not_mem hm
      /- (2) but with ite_true -> ite_false -/
      · simp only [Pred, filter_cons, hm₂, ite_false, hB'₂, disjUnion_eq_union]
        nth_rewrite 2 [←filter_union_filter_neg_eq (fun x => x = m) A]
        congr
        simp only [filter_eq', hm₁, ite_false]