case zero
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.16476
s t✝ : Set (α × α)
h : idRel ⊆ s
t : Set (α × α)
⊢ t ⊆ ((fun x x_1 => x ○ x_1) s^[Nat.zero]) t

case succ
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.16476
s t✝ : Set (α × α)
h : idRel ⊆ s
n : ℕ
ihn : ∀ {t : Set (α × α)}, t ⊆ ((fun x x_1 => x ○ x_1) s^[n]) t
t : Set (α × α)
⊢ t ⊆ ((fun x x_1 => x ○ x_1) s^[Nat.succ n]) t
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.16476
s t : Set (α × α)
h : idRel ⊆ s
n : ℕ
⊢ t ⊆ ((fun x x_1 => x ○ x_1) s^[n]) t
induction' n with n ihn generalizing t
no goals
case zero
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.16476
s t✝ : Set (α × α)
h : idRel ⊆ s
t : Set (α × α)
⊢ t ⊆ ((fun x x_1 => x ○ x_1) s^[Nat.zero]) t

case succ
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.16476
s t✝ : Set (α × α)
h : idRel ⊆ s
n : ℕ
ihn : ∀ {t : Set (α × α)}, t ⊆ ((fun x x_1 => x ○ x_1) s^[n]) t
t : Set (α × α)
⊢ t ⊆ ((fun x x_1 => x ○ x_1) s^[Nat.succ n]) t
exacts [Subset.rfl, (right_subset_compRel h).trans ihn]