-- Mathlib/SetTheory/Surreal/Basic.lean
/-- A small family of surreals is bounded above. -/
lemma bddAbove_range_of_small {ι : Type*} [Small.{u} ι] (f : ι → Surreal.{u}) :
    BddAbove (Set.range f)

Proof state:
case h
ι : Type u_1
inst✝ : Small.{u, u_1} ι
f : ι → Subtype Numeric
⊢ BddAbove (Set.range fun i => ⟦f i⟧)

Tactic:
let g : ι → PGame.{u} := Subtype.val ∘ f

Result:
case h
ι : Type u_1
inst✝ : Small.{u, u_1} ι
f : ι → Subtype Numeric
g : ι → PGame := Subtype.val ∘ f
⊢ BddAbove (Set.range fun i => ⟦f i⟧)

Proof state:
ι : Type u_1
inst✝ : Small.{u, u_1} ι
g : ι → PGame
hg : ∀ (i : ι), (g i).Numeric
x : PGame :=
  PGame.mk ((i : Shrink.{u, u_1} ι) × (g ((equivShrink ι).symm i)).LeftMoves) PEmpty.{u + 1}
    (fun x => (g ((equivShrink ι).symm x.fst)).moveLeft x.snd) PEmpty.elim
⊢ ∀ (j : x.RightMoves), (x.moveRight j).Numeric

Tactic:
simp [x]

Result:
no goals

Proof state:
case h
ι : Type u_1
inst✝ : Small.{u, u_1} ι
g : ι → PGame
hg : ∀ (i : ι), (g i).Numeric
x : PGame :=
  PGame.mk ((i : Shrink.{u, u_1} ι) × (g ((equivShrink ι).symm i)).LeftMoves) PEmpty.{u + 1}
    (fun x => (g ((equivShrink ι).symm x.fst)).moveLeft x.snd) PEmpty.elim
⊢ BddAbove (Set.range fun i => mk (g i) ⋯)

Tactic:
refine ⟨mk x (.mk (by simp [x]) (fun _ ↦ (hg _).moveLeft _) (by simp [x])),
  Set.forall_mem_range.2 fun i ↦ ?_⟩

Result:
case h
ι : Type u_1
inst✝ : Small.{u, u_1} ι
g : ι → PGame
hg : ∀ (i : ι), (g i).Numeric
x : PGame :=
  PGame.mk ((i : Shrink.{u, u_1} ι) × (g ((equivShrink ι).symm i)).LeftMoves) PEmpty.{u + 1}
    (fun x => (g ((equivShrink ι).symm x.fst)).moveLeft x.snd) PEmpty.elim
i : ι
⊢ mk (g i) ⋯ ≤ mk x ⋯

Proof state:
ι : Type u_1
inst✝ : Small.{u, u_1} ι
f : ι → Surreal
⊢ BddAbove (Set.range f)

Tactic:
induction' f using Quotient.induction_on_pi with f

Result:
case h
ι : Type u_1
inst✝ : Small.{u, u_1} ι
f : ι → Subtype Numeric
⊢ BddAbove (Set.range fun i => ⟦f i⟧)

Proof state:
case h
ι : Type u_1
inst✝ : Small.{u, u_1} ι
f : ι → Subtype Numeric
g : ι → PGame := Subtype.val ∘ f
hg : ∀ (i : ι), (g i).Numeric
⊢ BddAbove (Set.range fun i => ⟦f i⟧)

Tactic:
conv in (⟦f _⟧) =>
  change mk (g i) (hg i)

Result:
case h
ι : Type u_1
inst✝ : Small.{u, u_1} ι
f : ι → Subtype Numeric
g : ι → PGame := Subtype.val ∘ f
hg : ∀ (i : ι), (g i).Numeric
⊢ BddAbove (Set.range fun i => mk (g i) ⋯)

Proof state:
case h
ι : Type u_1
inst✝ : Small.{u, u_1} ι
f : ι → Subtype Numeric
g : ι → PGame
hg : ∀ (i : ι), (g i).Numeric
⊢ BddAbove (Set.range fun i => mk (g i) ⋯)

Tactic:
clear f

Result:
case h
ι : Type u_1
inst✝ : Small.{u, u_1} ι
g : ι → PGame
hg : ∀ (i : ι), (g i).Numeric
⊢ BddAbove (Set.range fun i => mk (g i) ⋯)

Proof state:
ι : Type u_1
inst✝ : Small.{u, u_1} ι
g : ι → PGame
hg : ∀ (i : ι), (g i).Numeric
x : PGame :=
  PGame.mk ((i : Shrink.{u, u_1} ι) × (g ((equivShrink ι).symm i)).LeftMoves) PEmpty.{u + 1}
    (fun x => (g ((equivShrink ι).symm x.fst)).moveLeft x.snd) PEmpty.elim
⊢ ∀ (i : x.LeftMoves) (j : x.RightMoves), x.moveLeft i < x.moveRight j

Tactic:
simp [x]

Result:
no goals

Proof state:
case h
ι : Type u_1
inst✝ : Small.{u, u_1} ι
f : ι → Subtype Numeric
g : ι → PGame := Subtype.val ∘ f
⊢ BddAbove (Set.range fun i => ⟦f i⟧)

Tactic:
have hg (i) : (g i).Numeric := Subtype.prop _

Result:
case h
ι : Type u_1
inst✝ : Small.{u, u_1} ι
f : ι → Subtype Numeric
g : ι → PGame := Subtype.val ∘ f
hg : ∀ (i : ι), (g i).Numeric
⊢ BddAbove (Set.range fun i => ⟦f i⟧)

Proof state:
case h
ι : Type u_1
inst✝ : Small.{u, u_1} ι
g : ι → PGame
hg : ∀ (i : ι), (g i).Numeric
x : PGame :=
  PGame.mk ((i : Shrink.{u, u_1} ι) × (g ((equivShrink ι).symm i)).LeftMoves) PEmpty.{u + 1}
    (fun x => (g ((equivShrink ι).symm x.fst)).moveLeft x.snd) PEmpty.elim
i : ι
⊢ (∀ (i_1 : (g ((equivShrink ι).symm ((equivShrink ι) i))).LeftMoves),
      (g ((equivShrink ι).symm ((equivShrink ι) i))).moveLeft i_1 ⧏ x) ∧
    ∀ (j : x.RightMoves), g ((equivShrink ι).symm ((equivShrink ι) i)) ⧏ x.moveRight j

Tactic:
simpa [x] using fun j ↦ @moveLeft_lf x ⟨equivShrink ι i, j⟩

Result:
no goals

Proof state:
case h
ι : Type u_1
inst✝ : Small.{u, u_1} ι
g : ι → PGame
hg : ∀ (i : ι), (g i).Numeric
x : PGame :=
  PGame.mk ((i : Shrink.{u, u_1} ι) × (g ((equivShrink ι).symm i)).LeftMoves) PEmpty.{u + 1}
    (fun x => (g ((equivShrink ι).symm x.fst)).moveLeft x.snd) PEmpty.elim
i : ι
⊢ mk (g i) ⋯ ≤ mk x ⋯

Tactic:
rw [mk_le_mk, ← (equivShrink ι).symm_apply_apply i, le_iff_forall_lf]

Result:
case h
ι : Type u_1
inst✝ : Small.{u, u_1} ι
g : ι → PGame
hg : ∀ (i : ι), (g i).Numeric
x : PGame :=
  PGame.mk ((i : Shrink.{u, u_1} ι) × (g ((equivShrink ι).symm i)).LeftMoves) PEmpty.{u + 1}
    (fun x => (g ((equivShrink ι).symm x.fst)).moveLeft x.snd) PEmpty.elim
i : ι
⊢ (∀ (i_1 : (g ((equivShrink ι).symm ((equivShrink ι) i))).LeftMoves),
      (g ((equivShrink ι).symm ((equivShrink ι) i))).moveLeft i_1 ⧏ x) ∧
    ∀ (j : x.RightMoves), g ((equivShrink ι).symm ((equivShrink ι) i)) ⧏ x.moveRight j

Proof state:
case h
ι : Type u_1
inst✝ : Small.{u, u_1} ι
f : ι → Subtype Numeric
g : ι → PGame := Subtype.val ∘ f
hg : ∀ (i : ι), (g i).Numeric
⊢ BddAbove (Set.range fun i => mk (g i) ⋯)

Tactic:
clear_value g

Result:
case h
ι : Type u_1
inst✝ : Small.{u, u_1} ι
f : ι → Subtype Numeric
g : ι → PGame
hg : ∀ (i : ι), (g i).Numeric
⊢ BddAbove (Set.range fun i => mk (g i) ⋯)

Proof state:
case h
ι : Type u_1
inst✝ : Small.{u, u_1} ι
g : ι → PGame
hg : ∀ (i : ι), (g i).Numeric
⊢ BddAbove (Set.range fun i => mk (g i) ⋯)

Tactic:
let x : PGame.{u} := ⟨Σ i, (g <| (equivShrink.{u} ι).symm i).LeftMoves, PEmpty,
  fun x ↦ moveLeft _ x.2, PEmpty.elim⟩

Result:
case h
ι : Type u_1
inst✝ : Small.{u, u_1} ι
g : ι → PGame
hg : ∀ (i : ι), (g i).Numeric
x : PGame :=
  PGame.mk ((i : Shrink.{u, u_1} ι) × (g ((equivShrink ι).symm i)).LeftMoves) PEmpty.{u + 1}
    (fun x => (g ((equivShrink ι).symm x.fst)).moveLeft x.snd) PEmpty.elim
⊢ BddAbove (Set.range fun i => mk (g i) ⋯)