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

Proof state:
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
ho : o < Ordinal.type fun x1 x2 => x1 < x2
h : Set.range (sum_to C ho) = Set.range Subtype.val ∪ Set.range Subtype.val
⊢ Set.range (sum_to C ho) = GoodProducts (π C fun x => ord I x < o) ∪ MaxProducts C ho

Tactic:
rw [h]

Result:
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
ho : o < Ordinal.type fun x1 x2 => x1 < x2
h : Set.range (sum_to C ho) = Set.range Subtype.val ∪ Set.range Subtype.val
⊢ Set.range Subtype.val ∪ Set.range Subtype.val = GoodProducts (π C fun x => ord I x < o) ∪ MaxProducts C ho

Proof state:
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
ho : o < Ordinal.type fun x1 x2 => x1 < x2
h : Set.range (sum_to C ho) = Set.range Subtype.val ∪ Set.range Subtype.val
l : Products I
x✝ : l ∈ Set.range Subtype.val
m : ↑(GoodProducts (π C fun x => ord I x < o))
hm : ↑m = l
⊢ ↑m ∈ GoodProducts (π C fun x => ord I x < o)

Tactic:
exact m.prop

Result:
no goals

Proof state:
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
ho : o < Ordinal.type fun x1 x2 => x1 < x2
h : Set.range (sum_to C ho) = Set.range Subtype.val ∪ Set.range Subtype.val
l : Products I
x✝ : l ∈ Set.range Subtype.val
m : ↑(MaxProducts C ho)
hm : ↑m = l
⊢ l ∈ MaxProducts C ho

Tactic:
rw [← hm]

Result:
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
ho : o < Ordinal.type fun x1 x2 => x1 < x2
h : Set.range (sum_to C ho) = Set.range Subtype.val ∪ Set.range Subtype.val
l : Products I
x✝ : l ∈ Set.range Subtype.val
m : ↑(MaxProducts C ho)
hm : ↑m = l
⊢ ↑m ∈ MaxProducts C ho

Proof state:
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
ho : o < Ordinal.type fun x1 x2 => x1 < x2
h : Set.range (sum_to C ho) = Set.range Subtype.val ∪ Set.range Subtype.val
l : Products I
x✝ : l ∈ Set.range Subtype.val
m : ↑(GoodProducts (π C fun x => ord I x < o))
hm : ↑m = l
⊢ l ∈ GoodProducts (π C fun x => ord I x < o)

Tactic:
rw [← hm]

Result:
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
ho : o < Ordinal.type fun x1 x2 => x1 < x2
h : Set.range (sum_to C ho) = Set.range Subtype.val ∪ Set.range Subtype.val
l : Products I
x✝ : l ∈ Set.range Subtype.val
m : ↑(GoodProducts (π C fun x => ord I x < o))
hm : ↑m = l
⊢ ↑m ∈ GoodProducts (π C fun x => ord I x < o)

Proof state:
case e_a.h
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
ho : o < Ordinal.type fun x1 x2 => x1 < x2
h : Set.range (sum_to C ho) = Set.range Subtype.val ∪ Set.range Subtype.val
l : Products I
⊢ l ∈ Set.range Subtype.val ↔ l ∈ GoodProducts (π C fun x => ord I x < o)

Tactic:
exact ⟨fun ⟨m,hm⟩ ↦ by rw [← hm]; exact m.prop, fun hl ↦ ⟨⟨l,hl⟩, rfl⟩⟩

Result:
no goals

Proof state:
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
ho : o < Ordinal.type fun x1 x2 => x1 < x2
h : Set.range (sum_to C ho) = Set.range Subtype.val ∪ Set.range Subtype.val
⊢ Set.range Subtype.val ∪ Set.range Subtype.val = GoodProducts (π C fun x => ord I x < o) ∪ MaxProducts C ho

Tactic:
congr<;> ext l

Result:
case e_a.h
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
ho : o < Ordinal.type fun x1 x2 => x1 < x2
h : Set.range (sum_to C ho) = Set.range Subtype.val ∪ Set.range Subtype.val
l : Products I
⊢ l ∈ Set.range Subtype.val ↔ l ∈ GoodProducts (π C fun x => ord I x < o)

case e_a.h
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
ho : o < Ordinal.type fun x1 x2 => x1 < x2
h : Set.range (sum_to C ho) = Set.range Subtype.val ∪ Set.range Subtype.val
l : Products I
⊢ l ∈ Set.range Subtype.val ↔ l ∈ MaxProducts C ho

Proof state:
case e_a.h
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
ho : o < Ordinal.type fun x1 x2 => x1 < x2
h : Set.range (sum_to C ho) = Set.range Subtype.val ∪ Set.range Subtype.val
l : Products I
⊢ l ∈ Set.range Subtype.val ↔ l ∈ MaxProducts C ho

Tactic:
exact ⟨fun ⟨m,hm⟩ ↦ by rw [← hm]; exact m.prop, fun hl ↦ ⟨⟨l,hl⟩, rfl⟩⟩

Result:
no goals

Proof state:
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
ho : o < Ordinal.type fun x1 x2 => x1 < x2
h : Set.range (sum_to C ho) = Set.range Subtype.val ∪ Set.range Subtype.val
l : Products I
x✝ : l ∈ Set.range Subtype.val
m : ↑(MaxProducts C ho)
hm : ↑m = l
⊢ ↑m ∈ MaxProducts C ho

Tactic:
exact m.prop

Result:
no goals

Proof state:
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
ho : o < Ordinal.type fun x1 x2 => x1 < x2
⊢ Set.range (sum_to C ho) = GoodProducts (π C fun x => ord I x < o) ∪ MaxProducts C ho

Tactic:
have h : Set.range (sum_to C ho) = _ ∪ _ := Set.Sum.elim_range _ _

Result:
I : Type u
C : Set (I → Bool)
inst✝¹ : LinearOrder I
inst✝ : WellFoundedLT I
o : Ordinal.{u}
ho : o < Ordinal.type fun x1 x2 => x1 < x2
h : Set.range (sum_to C ho) = Set.range Subtype.val ∪ Set.range Subtype.val
⊢ Set.range (sum_to C ho) = GoodProducts (π C fun x => ord I x < o) ∪ MaxProducts C ho