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

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

Tactic:
refine ⟨mk x (.mk (by simp [x]) (by simp [x]) (fun _ ↦ (hg _).moveRight _) ),
  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 PEmpty.{u + 1} ((i : Shrink.{u, u_1} ι) × (g ((equivShrink ι).symm i)).RightMoves) PEmpty.elim fun x =>
    (g ((equivShrink ι).symm x.fst)).moveRight x.snd
i : ι
⊢ mk x ⋯ ≤ mk (g 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
⊢ BddBelow (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
⊢ BddBelow (Set.range fun i => mk (g i) ⋯)

Proof state:
case h
ι : Type u_1
inst✝ : Small.{u, u_1} ι
f : ι → Subtype Numeric
g : ι → PGame := Subtype.val ∘ f
⊢ BddBelow (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
⊢ BddBelow (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
⊢ BddBelow (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
⊢ BddBelow (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
⊢ BddBelow (Set.range fun i => mk (g i) ⋯)

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

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

Tactic:
simpa [x] using fun j ↦ @lf_moveRight 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 PEmpty.{u + 1} ((i : Shrink.{u, u_1} ι) × (g ((equivShrink ι).symm i)).RightMoves) PEmpty.elim fun x =>
    (g ((equivShrink ι).symm x.fst)).moveRight x.snd
i : ι
⊢ mk x ⋯ ≤ mk (g i) ⋯

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 PEmpty.{u + 1} ((i : Shrink.{u, u_1} ι) × (g ((equivShrink ι).symm i)).RightMoves) PEmpty.elim fun x =>
    (g ((equivShrink ι).symm x.fst)).moveRight x.snd
i : ι
⊢ (∀ (i_1 : x.LeftMoves), x.moveLeft i_1 ⧏ g ((equivShrink ι).symm ((equivShrink ι) i))) ∧
    ∀ (j : (g ((equivShrink ι).symm ((equivShrink ι) i))).RightMoves),
      x ⧏ (g ((equivShrink ι).symm ((equivShrink ι) i))).moveRight j

Proof state:
ι : Type u_1
inst✝ : Small.{u, u_1} ι
f : ι → Surreal
⊢ BddBelow (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
⊢ BddBelow (Set.range fun i => ⟦f i⟧)

Proof state:
case h
ι : Type u_1
inst✝ : Small.{u, u_1} ι
f : ι → Subtype Numeric
g : ι → PGame
hg : ∀ (i : ι), (g i).Numeric
⊢ BddBelow (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
⊢ BddBelow (Set.range fun i => mk (g i) ⋯)