-- Mathlib/Topology/Category/Profinite/Nobeling.lean
theorem union_succ : GoodProducts C = GoodProducts (π C (ord I · < o)) ∪ MaxProducts C ho

Proof state:
case h
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun x1 x2 => x1 < x2
l : Products I
⊢ Products.isGood C l ↔ Products.isGood (π C fun x => ord I x < o) l ∨ Products.isGood C l ∧ term I ho ∈ ↑l

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩

Result:
case h.refine_1
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun x1 x2 => x1 < x2
l : Products I
h : Products.isGood C l
⊢ Products.isGood (π C fun x => ord I x < o) l ∨ Products.isGood C l ∧ term I ho ∈ ↑l

case h.refine_2
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun x1 x2 => x1 < x2
l : Products I
h : Products.isGood (π C fun x => ord I x < o) l ∨ Products.isGood C l ∧ term I ho ∈ ↑l
⊢ Products.isGood C l

Proof state:
case neg.h
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun x1 x2 => x1 < x2
l : Products I
h : Products.isGood C l
hh : term I ho ∉ ↑l
he :
  Products.eval (π C fun x => ord I x < o) l ∈
    Submodule.span ℤ (Products.eval (π C fun x => ord I x < o) '' {m | m < l})
h' : ∀ i ∈ ↑l, ord I i < Order.succ o
⊢ Products.eval C l ∈ Submodule.span ℤ (Products.eval C '' {m | m < l})

Tactic:
simp only [Order.lt_succ_iff] at h'

Result:
case neg.h
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun x1 x2 => x1 < x2
l : Products I
h : Products.isGood C l
hh : term I ho ∉ ↑l
he :
  Products.eval (π C fun x => ord I x < o) l ∈
    Submodule.span ℤ (Products.eval (π C fun x => ord I x < o) '' {m | m < l})
h' : ∀ i ∈ ↑l, ord I i ≤ o
⊢ Products.eval C l ∈ Submodule.span ℤ (Products.eval C '' {m | m < l})

Proof state:
case h.refine_2
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun x1 x2 => x1 < x2
l : Products I
h : Products.isGood (π C fun x => ord I x < o) l ∨ Products.isGood C l ∧ term I ho ∈ ↑l
⊢ Products.isGood C l

Tactic:
refine h.elim (fun hh ↦ ?_) And.left

Result:
case h.refine_2
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun x1 x2 => x1 < x2
l : Products I
h : Products.isGood (π C fun x => ord I x < o) l ∨ Products.isGood C l ∧ term I ho ∈ ↑l
hh : Products.isGood (π C fun x => ord I x < o) l
⊢ Products.isGood C l

Proof state:
case neg.h
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun x1 x2 => x1 < x2
l : Products I
h : Products.isGood C l
hh : term I ho ∉ ↑l
he :
  Products.eval (π C fun x => ord I x < o) l ∈
    Submodule.span ℤ (Products.eval (π C fun x => ord I x < o) '' {m | m < l})
⊢ Products.eval C l ∈ Submodule.span ℤ (Products.eval C '' {m | m < l})

Tactic:
have h' := Products.prop_of_isGood_of_contained C _ h hsC

Result:
case neg.h
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun x1 x2 => x1 < x2
l : Products I
h : Products.isGood C l
hh : term I ho ∉ ↑l
he :
  Products.eval (π C fun x => ord I x < o) l ∈
    Submodule.span ℤ (Products.eval (π C fun x => ord I x < o) '' {m | m < l})
h' : ∀ i ∈ ↑l, ord I i < Order.succ o
⊢ Products.eval C l ∈ Submodule.span ℤ (Products.eval C '' {m | m < l})

Proof state:
case neg.h
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun x1 x2 => x1 < x2
l : Products I
h : Products.isGood C l
hh : term I ho ∉ ↑l
he :
  Products.eval (π C fun x => ord I x < o) l ∈
    Submodule.span ℤ (Products.eval (π C fun x => ord I x < o) '' {m | m < l})
h' : ∀ i ∈ ↑l, ord I i ≤ o
hh' : ∀ a ∈ ↑l, ord I a < o
⊢ Products.eval C l ∈ Submodule.span ℤ (Products.eval C '' {m | m < l})

Tactic:
rwa [Products.eval_πs_image C hh', ← Products.eval_πs C hh',
  Submodule.apply_mem_span_image_iff_mem_span (injective_πs _ _)]

Result:
no goals

Proof state:
case h.refine_1
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun x1 x2 => x1 < x2
l : Products I
h : Products.isGood C l
⊢ Products.isGood (π C fun x => ord I x < o) l ∨ Products.isGood C l ∧ term I ho ∈ ↑l

Tactic:
by_cases hh : term I ho ∈ l.val

Result:
case pos
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun x1 x2 => x1 < x2
l : Products I
h : Products.isGood C l
hh : term I ho ∈ ↑l
⊢ Products.isGood (π C fun x => ord I x < o) l ∨ Products.isGood C l ∧ term I ho ∈ ↑l

case neg
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun x1 x2 => x1 < x2
l : Products I
h : Products.isGood C l
hh : term I ho ∉ ↑l
⊢ Products.isGood (π C fun x => ord I x < o) l ∨ Products.isGood C l ∧ term I ho ∈ ↑l

Proof state:
case h.refine_2
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun x1 x2 => x1 < x2
l : Products I
h : Products.isGood (π C fun x => ord I x < o) l ∨ Products.isGood C l ∧ term I ho ∈ ↑l
hh : Products.isGood (π C fun x => ord I x < o) l
⊢ Products.isGood C l

Tactic:
have := Products.isGood_mono C (Order.lt_succ o).le hh

Result:
case h.refine_2
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun x1 x2 => x1 < x2
l : Products I
h : Products.isGood (π C fun x => ord I x < o) l ∨ Products.isGood C l ∧ term I ho ∈ ↑l
hh : Products.isGood (π C fun x => ord I x < o) l
this : Products.isGood (π C fun x => ord I x < Order.succ o) l
⊢ Products.isGood C l

Proof state:
case neg
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun x1 x2 => x1 < x2
l : Products I
h : Products.isGood C l
hh : term I ho ∉ ↑l
⊢ Products.isGood (π C fun x => ord I x < o) l ∨ Products.isGood C l ∧ term I ho ∈ ↑l

Tactic:
left

Result:
case neg.h
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun x1 x2 => x1 < x2
l : Products I
h : Products.isGood C l
hh : term I ho ∉ ↑l
⊢ Products.isGood (π C fun x => ord I x < o) l

Proof state:
case neg.h
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun x1 x2 => x1 < x2
l : Products I
h : Products.isGood C l
hh : term I ho ∉ ↑l
⊢ Products.isGood (π C fun x => ord I x < o) l

Tactic:
intro he

Result:
case neg.h
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
hsC : contained C (Order.succ o)
ho : o < Ordinal.type fun x1 x2 => x1 < x2
l : Products I
h : Products.isGood C l
hh : term I ho ∉ ↑l
he :
  Products.eval (π C fun x => ord I x < o) l ∈
    Submodule.span ℤ (Products.eval (π C fun x => ord I x < o) '' {m | m < l})
⊢ False