-- 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
⊢ l ∈ GoodProducts C ↔ l ∈ GoodProducts (π C fun x => ord I x < o) ∪ MaxProducts C ho

Tactic:
simp only [GoodProducts, MaxProducts, Set.mem_union, Set.mem_setOf_eq]

Result:
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

Proof state:
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

Tactic:
exact Or.inr ⟨h, hh⟩

Result:
no goals

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
⊢ Products.eval C l ∈ Submodule.span ℤ (Products.eval C '' {m | m < l})

Tactic:
have hh' : ∀ a ∈ l.val, ord I a < o := by
  intro a ha
  refine (h' a ha).lt_of_ne ?_
  rw [ne_eq, ord_term ho a]
  rintro rfl
  contradiction

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
hh' : ∀ a ∈ ↑l, ord I a < 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
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

Tactic:
rwa [contained_eq_proj C (Order.succ o) hsC]

Result:
no goals

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})
⊢ False

Tactic:
apply 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})
⊢ Products.eval C l ∈ Submodule.span ℤ (Products.eval C '' {m | m < l})

Proof state:
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
a : I
ha : a ∈ ↑l
⊢ ord I a < o

Tactic:
refine (h' a ha).lt_of_ne ?_

Result:
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
a : I
ha : a ∈ ↑l
⊢ ord I a ≠ o

Proof state:
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
a : I
ha : a ∈ ↑l
⊢ ord I a ≠ o

Tactic:
rw [ne_eq, ord_term ho a]

Result:
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
a : I
ha : a ∈ ↑l
⊢ ¬term I ho = a

Proof state:
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
ha : term I ho ∈ ↑l
⊢ False

Tactic:
contradiction

Result:
no goals

Proof state:
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
a : I
ha : a ∈ ↑l
⊢ ¬term I ho = a

Tactic:
rintro rfl

Result:
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
ha : term I ho ∈ ↑l
⊢ False

Proof state:
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
⊢ ∀ a ∈ ↑l, ord I a < o

Tactic:
intro a ha

Result:
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
a : I
ha : a ∈ ↑l
⊢ ord I a < o