-- Mathlib/Topology/Category/Profinite/Nobeling.lean
theorem swapTrue_mem_C1 (f : π (C1 C ho) (ord I · < o)) :
    SwapTrue o f.val ∈ C1 C ho

Proof state:
case h.e'_5
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
g : I → Bool
hg : g ∈ C1 C ho
⊢ SwapTrue o ↑⟨Proj (fun x => ord I x < o) g, ⋯⟩ = g

Tactic:
dsimp (config := { unfoldPartialApp := true }) [SwapTrue]

Result:
case h.e'_5
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
g : I → Bool
hg : g ∈ C1 C ho
⊢ (fun i => if ord I i = o then true else Proj (fun x => ord I x < o) g i) = g

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
g : I → Bool
hg : g ∈ C1 C ho
i : I
h : ord I i = o
⊢ true = g i

Tactic:
rw [ord_term ho] at h

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
g : I → Bool
hg : g ∈ C1 C ho
i : I
h : term I ho = i
⊢ true = g i

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
g : I → Bool
hg : g ∈ C1 C ho
i : I
h : term I ho = i
⊢ true = g i

Tactic:
simpa only [← h] using hg.2.symm

Result:
no goals

Proof state:
case h.e'_5.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
g : I → Bool
hg : g ∈ C1 C ho
i : I
⊢ (if ord I i = o then true else Proj (fun x => ord I x < o) g i) = g i

Tactic:
split_ifs with h

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
g : I → Bool
hg : g ∈ C1 C ho
i : I
h : ord I i = o
⊢ true = g i

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
g : I → Bool
hg : g ∈ C1 C ho
i : I
h : ¬ord I i = o
⊢ Proj (fun x => ord I x < o) g i = g i

Proof state:
case neg
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
g : I → Bool
hg : g ∈ C1 C ho
i : I
h : ¬ord I i = o
hsC : g i = true → ord I i < Order.succ o
⊢ o ≤ ord I i → ¬g i = true

Tactic:
intro h'

Result:
case neg
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
g : I → Bool
hg : g ∈ C1 C ho
i : I
h : ¬ord I i = o
hsC : g i = true → ord I i < Order.succ o
h' : o ≤ ord I i
⊢ ¬g i = true

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
g : I → Bool
hg : g ∈ C1 C ho
i : I
h : ¬ord I i = o
⊢ Proj (fun x => ord I x < o) g i = g i

Tactic:
simp only [Proj, ite_eq_left_iff, not_lt, @eq_comm _ false, ← Bool.not_eq_true]

Result:
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
g : I → Bool
hg : g ∈ C1 C ho
i : I
h : ¬ord I i = o
⊢ o ≤ ord I i → ¬g i = true

Proof state:
case mk.intro.intro
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
g : I → Bool
hg : g ∈ C1 C ho
⊢ SwapTrue o ↑⟨Proj (fun x => ord I x < o) g, ⋯⟩ ∈ C1 C ho

Tactic:
convert hg

Result:
case h.e'_5
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
g : I → Bool
hg : g ∈ C1 C ho
⊢ SwapTrue o ↑⟨Proj (fun x => ord I x < o) g, ⋯⟩ = g

Proof state:
case neg
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
g : I → Bool
hg : g ∈ C1 C ho
i : I
h : ¬ord I i = o
h' : o ≤ ord I i
hsC : g i = true
⊢ g i = true ∧ Order.succ o ≤ ord I i

Tactic:
exact ⟨hsC, Order.succ_le_of_lt (h'.lt_of_ne' h)⟩

Result:
no goals

Proof state:
case neg
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
g : I → Bool
hg : g ∈ C1 C ho
i : I
h : ¬ord I i = o
hsC : g i = true → ord I i < Order.succ o
h' : o ≤ ord I i
⊢ ¬g i = true

Tactic:
contrapose! hsC

Result:
case neg
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
g : I → Bool
hg : g ∈ C1 C ho
i : I
h : ¬ord I i = o
h' : o ≤ ord I i
hsC : g i = true
⊢ g i = true ∧ Order.succ o ≤ ord I i

Proof state:
case h.e'_5
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
g : I → Bool
hg : g ∈ C1 C ho
⊢ (fun i => if ord I i = o then true else Proj (fun x => ord I x < o) g i) = g

Tactic:
ext i

Result:
case h.e'_5.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
g : I → Bool
hg : g ∈ C1 C ho
i : I
⊢ (if ord I i = o then true else Proj (fun x => ord I x < o) g i) = g i

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
g : I → Bool
hg : g ∈ C1 C ho
i : I
h : ¬ord I i = o
⊢ o ≤ ord I i → ¬g i = true

Tactic:
specialize hsC g hg.1 i

Result:
case neg
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
g : I → Bool
hg : g ∈ C1 C ho
i : I
h : ¬ord I i = o
hsC : g i = true → ord I i < Order.succ o
⊢ o ≤ ord I i → ¬g i = true

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
f : ↑(π (C1 C ho) fun x => ord I x < o)
⊢ SwapTrue o ↑f ∈ C1 C ho

Tactic:
obtain ⟨f, g, hg, rfl⟩ := f

Result:
case mk.intro.intro
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
g : I → Bool
hg : g ∈ C1 C ho
⊢ SwapTrue o ↑⟨Proj (fun x => ord I x < o) g, ⋯⟩ ∈ C1 C ho