awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Logic.Relator
Goal:
⊢ LiftFun (γ := Prop → Prop) (δ := Prop → Prop) (fun (x1 x2 : Prop) ↦ x1 ↔ x2)
    ((fun (x1 x2 : Prop) ↦ x1 ↔ x2) ⇒ fun (x1 x2 : Prop) ↦ x1 ↔ x2) (fun (x1 x2 : Prop) ↦ x1 ↔ x2) fun (x1 x2 : Prop) ↦
    x1 ↔ x2

Tactic:
fun _ _ h₁ _ _ h₂ => iff_congr h₁ h₂

Premises used: iff_congr, Relator.LiftFun
-- Module: Mathlib.Logic.Relator
Goal:
α : Type u_1
β : Type u_2
r : α → β → Prop
hr : BiUnique r
⊢ LiftFun (γ := α → Prop) (δ := β → Prop) r (r ⇒ fun (x1 x2 : Prop) ↦ x1 ↔ x2) (fun (x1 x2 : α) ↦ x1 = x2)
    fun (x1 x2 : β) ↦ x1 = x2

Tactic:
fun _ _ h₁ _ _ h₂ => ⟨fun h => hr.right h₁ <| h.symm ▸ h₂, fun h => hr.left h₁ <| h.symm ▸ h₂⟩

Premises used: Eq.rec, And.right, And.left, Iff.intro, Eq.symm, Relator.LiftFun
-- Module: Mathlib.Logic.Relator
Goal:
α : Type u_1
r₁₁ : α → α → Prop
hr : ∀ (a : α), r₁₁ a a
⊢ LeftTotal r₁₁

Tactic:
fun a ↦ ⟨a, hr _⟩

Premises used: Relator.LeftTotal, Exists.intro
-- Module: Mathlib.Logic.Relator
Goal:
α : Type u_1
β : Type u_2
r₁₂ : α → β → Prop
r₂₁ : β → α → Prop
hr : ∀ (a : α) (b : β), r₁₂ a b → r₂₁ b a
⊢ LeftTotal r₁₂ → RightTotal r₂₁

Tactic:
fun h a ↦ (h a).imp (fun _ ↦ hr _ _)

Premises used: Exists.imp, Relator.RightTotal
-- Module: Mathlib.Logic.Relator
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
r₁₂ : α → β → Prop
r₂₃ : β → γ → Prop
r₁₃ : α → γ → Prop
hr : ∀ (a : α) (b : β) (c : γ), r₁₂ a b → r₂₃ b c → r₁₃ a c
⊢ LeftTotal r₁₂ → LeftTotal r₂₃ → LeftTotal r₁₃

Tactic:
fun h₁ h₂ a ↦ let ⟨b, hab⟩ := h₁ a; let ⟨c, hbc⟩ := h₂ b; ⟨c, hr _ _ _ hab hbc⟩

Premises used: Relator.LeftTotal, Exists, _private.0.Relator.LeftTotal.trans.match_1, Exists.intro
-- Module: Mathlib.Logic.Relator
Goal:
α : Type u_1
r₁₁ : α → α → Prop
hr : ∀ (a : α), r₁₁ a a
⊢ RightTotal r₁₁

Tactic:
LeftTotal.refl hr

Premises used: Relator.RightTotal, Relator.LeftTotal.refl
-- Module: Mathlib.Logic.Relator
Goal:
α : Type u_1
β : Type u_2
r₁₂ : α → β → Prop
r₂₁ : β → α → Prop
hr : ∀ (a : α) (b : β), r₁₂ a b → r₂₁ b a
⊢ RightTotal r₁₂ → LeftTotal r₂₁

Tactic:
LeftTotal.symm (fun _ _ ↦ hr _ _)

Premises used: Relator.LeftTotal, Relator.LeftTotal.symm, Relator.RightTotal
-- Module: Mathlib.Logic.Relator
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
r₁₂ : α → β → Prop
r₂₃ : β → γ → Prop
r₁₃ : α → γ → Prop
hr : ∀ (a : α) (b : β) (c : γ), r₁₂ a b → r₂₃ b c → r₁₃ a c
⊢ RightTotal r₁₂ → RightTotal r₂₃ → RightTotal r₁₃

Tactic:
swap <| LeftTotal.trans (fun _ _ _ ↦ swap <| hr _ _ _)

Premises used: Function.swap, Relator.LeftTotal.trans
-- Module: Mathlib.Logic.Relator
Goal:
α : Type u_1
r₁₁ : α → α → Prop
hr : ∀ (a : α), r₁₁ a a
⊢ BiTotal r₁₁

Tactic:
⟨LeftTotal.refl hr, RightTotal.refl hr⟩

Premises used: Relator.RightTotal.refl, And.intro, Relator.BiTotal, Relator.LeftTotal.refl
-- Module: Mathlib.Logic.Relator
Goal:
α : Type u_1
β : Type u_2
r₁₂ : α → β → Prop
r₂₁ : β → α → Prop
hr : ∀ (a : α) (b : β), r₁₂ a b → r₂₁ b a
⊢ BiTotal r₁₂ → BiTotal r₂₁

Tactic:
fun h ↦ ⟨h.2.symm hr, h.1.symm hr⟩

Premises used: Relator.RightTotal.symm, And.right, And.left, And.intro, Relator.LeftTotal.symm, Relator.BiTotal
-- Module: Mathlib.Logic.Relator
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
r₁₂ : α → β → Prop
r₂₃ : β → γ → Prop
r₁₃ : α → γ → Prop
hr : ∀ (a : α) (b : β) (c : γ), r₁₂ a b → r₂₃ b c → r₁₃ a c
⊢ BiTotal r₁₂ → BiTotal r₂₃ → BiTotal r₁₃

Tactic:
fun h₁ h₂ ↦ ⟨h₁.1.trans hr h₂.1, h₁.2.trans hr h₂.2⟩

Premises used: Relator.LeftTotal.trans, And.right, And.left, And.intro, Relator.RightTotal.trans, Relator.BiTotal
-- Module: Mathlib.Logic.Small.Basic
Goal:
α : Type v
inst : Small.{w, v} α
P : α → Prop
⊢ Small.{w, v} { x : α // P x }

Tactic:
small_map (equivShrink α).subtypeEquivOfSubtype'

Premises used: Equiv.subtypeEquivOfSubtype', small_map, equivShrink
-- Module: Mathlib.Logic.Small.Basic
Goal:
α : Type v
β : Type w
inst : Small.{u, w} β
f : α → β
hf : Function.Injective f
⊢ Small.{u, v} α

Tactic:
small_map (Equiv.ofInjective f hf)

Premises used: Equiv.ofInjective, small_map
-- Module: Mathlib.Logic.Small.Basic
Goal:
α : Type v
β : Type w
inst : Small.{u, v} α
f : α → β
hf : Function.Surjective f
⊢ Small.{u, w} β

Tactic:
small_of_injective (Function.injective_surjInv hf)

Premises used: small_of_injective, Function.injective_surjInv
-- Module: Mathlib.Logic.Small.Basic
Goal:
α : Type v
inst : Subsingleton α
inl : IsEmpty α → Small.{w, v} α
inr : Nonempty α → Small.{w, v} α
⊢ Small.{w, v} α

Tactic:
rcases isEmpty_or_nonempty α with ⟨⟩

Premises used: isEmpty_or_nonempty
-- Module: Mathlib.Logic.Small.Basic
Goal:
α : Type v
inst : Subsingleton α
h : IsEmpty α
⊢ Small.{w, v} α

Tactic:
apply small_map (Equiv.equivPEmpty α)

Premises used: small_map, Equiv.equivPEmpty
-- Module: Mathlib.Logic.Small.Basic
Goal:
α : Type v
inst : Subsingleton α
h : Nonempty α
⊢ Small.{w, v} α

Tactic:
apply small_map Equiv.punitOfNonemptyOfSubsingleton

Premises used: Equiv.punitOfNonemptyOfSubsingleton, small_map
-- Module: Mathlib.Logic.Small.Basic
Goal:
α : Type v
β : Type w
γ : Type v'
inst : Small.{u, v} α
f : α → γ
g : β → γ
hg : Function.Injective g
h : ∀ (b : β), ∃ (a : α), f a = g b
pos : ∀ (hβ : Nonempty β), Small.{u, w} β
neg : ∀ (hβ : ¬Nonempty β), Small.{u, w} β
⊢ Small.{u, w} β

Tactic:
by_cases hβ : Nonempty β

Premises used: Nonempty
-- Module: Mathlib.Logic.Small.Basic
Goal:
α : Type v
β : Type w
γ : Type v'
inst : Small.{u, v} α
f : α → γ
g : β → γ
hg : Function.Injective g
h : ∀ (b : β), ∃ (a : α), f a = g b
hβ : Nonempty β
⊢ Small.{u, w} β

Tactic:
small_of_surjective (f := Function.invFun g ∘ f) (fun b => ?_)

Premises used: small_of_surjective
-- Module: Mathlib.Logic.Small.Basic
Goal:
α : Type v
β : Type w
γ : Type v'
inst : Small.{u, v} α
f : α → γ
g : β → γ
hg : Function.Injective g
h : ∀ (b : β), ∃ (a : α), f a = g b
hβ : Nonempty β
pos : ∀ (b : β), ∃ (a : α), (Function.invFun g ∘ f) a = b
⊢ Small.{u, w} β

Tactic:
refine small_of_surjective (f := Function.invFun g ∘ f) (fun b => ?_)

Premises used: small_of_surjective
-- Module: Mathlib.Logic.Small.Basic
Goal:
α : Type v
β : Type w
γ : Type v'
inst : Small.{u, v} α
f : α → γ
g : β → γ
hg : Function.Injective g
h : ∀ (b : β), ∃ (a : α), f a = g b
hβ : Nonempty β
b : β
pos : ∀ (a : α) (ha : f a = g b), ∃ (a : α), (Function.invFun g ∘ f) a = b
⊢ ∃ (a : α), (Function.invFun g ∘ f) a = b

Tactic:
obtain ⟨a, ha⟩ := h b
-- Module: Mathlib.Logic.Small.Basic
Goal:
α : Type v
β : Type w
γ : Type v'
inst : Small.{u, v} α
f : α → γ
g : β → γ
hg : Function.Injective g
h : ∀ (b : β), ∃ (a : α), f a = g b
hβ : Nonempty β
b : β
a : α
ha : f a = g b
rw : Function.invFun g (f a) = b
rw₁ : Function.invFun g (g b) = b
rw₂ rw₃ : b = b
⊢ (Function.invFun g ∘ f) a = b

Tactic:
rw [Function.comp_apply, ha, Function.leftInverse_invFun hg]

Premises used: Function.leftInverse_invFun, Function.comp_apply
-- Module: Mathlib.Logic.Small.Basic
Goal:
α : Type v
β : Type w
γ : Type v'
inst : Small.{u, v} α
f : α → γ
g : β → γ
hg : Function.Injective g
h : ∀ (b : β), ∃ (a : α), f a = g b
hβ : Nonempty β
b : β
a : α
ha : f a = g b
⊢ ∃ (a : α), (Function.invFun g ∘ f) a = b

Tactic:
exact ⟨a, by rw [Function.comp_apply, ha, Function.leftInverse_invFun hg]⟩
-- Module: Mathlib.Logic.Small.Basic
Goal:
α : Type v
β : Type w
γ : Type v'
inst : Small.{u, v} α
f : α → γ
g : β → γ
hg : Function.Injective g
h : ∀ (b : β), ∃ (a : α), f a = g b
hβ : ¬Nonempty β
⊢ IsEmpty β

Tactic:
simp only [not_nonempty_iff] at hβ

Premises used: not_nonempty_iff
-- Module: Mathlib.Logic.Small.Basic
Goal:
α : Type v
β : Type w
γ : Type v'
inst : Small.{u, v} α
f : α → γ
g : β → γ
hg : Function.Injective g
h : ∀ (b : β), ∃ (a : α), f a = g b
hβ : IsEmpty β
⊢ Small.{u, w} β

Tactic:
infer_instance
-- Module: Mathlib.Logic.Small.Basic
Goal:
α : Type u_2
β : α → Type u_1
inst : Small.{w, u_2} α
inst_1 : ∀ (a : α), Small.{w, u_1} (β a)
a : α
⊢ Equiv.{u_1 + 1, w + 1} (β a)
    (Shrink.{w, u_1}
      (β
        ((Equiv.symm (equivShrink α) : (a : Shrink.{w, u_2} α) → α)
          ((equivShrink α : (a : α) → Shrink.{w, u_2} α) a : Shrink.{w, u_2} α))))

Tactic:
simpa using equivShrink (β a)

Premises used: equivShrink
-- Module: Mathlib.Logic.Small.Basic
Goal:
α : Type u_1
β : Type u_2
inst : Small.{w, u_1} α
inst_1 : Small.{w, u_2} β
⊢ Small.{w, max u_2 u_1} (α × β)

Tactic:
⟨⟨Shrink α × Shrink β, ⟨Equiv.prodCongr (equivShrink α) (equivShrink β)⟩⟩⟩

Premises used: Small.mk, Nonempty.intro, Exists.intro, Shrink, Prod, Equiv.prodCongr, equivShrink
-- Module: Mathlib.Logic.Small.Basic
Goal:
α : Type u_1
β : Type u_2
inst : Small.{w, u_1} α
inst_1 : Small.{w, u_2} β
⊢ Small.{w, max u_2 u_1} (α ⊕ β)

Tactic:
⟨⟨Shrink α ⊕ Shrink β, ⟨Equiv.sumCongr (equivShrink α) (equivShrink β)⟩⟩⟩

Premises used: Sum, Small.mk, Nonempty.intro, Equiv.sumCongr, Exists.intro, Shrink, equivShrink
-- Module: Mathlib.Logic.Small.Basic
Goal:
α : Type u_1
inst : Small.{w, u_1} α
⊢ Small.{w, u_1} (Set α)

Tactic:
⟨⟨Set (Shrink α), ⟨Equiv.Set.congr (equivShrink α)⟩⟩⟩

Premises used: Equiv.Set.congr, Small.mk, Nonempty.intro, Exists.intro, Shrink, equivShrink, Set
-- Module: Mathlib.Logic.Small.Basic
Goal:
α : Type u
inst : Small.{v, u} α
r : α → α → Prop
⊢ Small.{v, u} (Quot r)

Tactic:
small_of_surjective Quot.mk_surjective

Premises used: small_of_surjective, Quot.mk_surjective
-- Module: Mathlib.Logic.Small.Basic
Goal:
α : Type u
inst : Small.{v, u} α
s : Setoid α
⊢ Small.{v, u} (Quotient s)

Tactic:
small_of_surjective Quotient.mk_surjective

Premises used: small_of_surjective, Quotient.mk_surjective
-- Module: Mathlib.Logic.Small.Defs
Goal:
α : Type v
S : Type w
e : α ≃ S
⊢ Small.{w, v} α

Tactic:
⟨⟨S, ⟨e⟩⟩⟩

Premises used: Small.mk, Nonempty.intro, Exists.intro
-- Module: Mathlib.Logic.Small.Defs
Goal:
α : Type v
inst : Small.{w, v} α
x y : Shrink.{w, v} α
w :
  Eq.{v + 1} (α := α) ((Equiv.symm (equivShrink α) : (a : Shrink.{w, v} α) → α) x : α)
    ((Equiv.symm (equivShrink α) : (a : Shrink.{w, v} α) → α) y : α)
⊢ x = y

Tactic:
simpa using w
-- Module: Mathlib.Logic.Small.Defs
Goal:
α : Type u_1
inst : Small.{w, u_1} α
F : Shrink.{w, u_1} α → Sort v
f : (a : α) → F ((equivShrink α : (a : α) → Shrink.{w, u_1} α) a)
a : α
simp :
  HEq (α :=
    F
      ((equivShrink α : (a : α) → Shrink.{w, u_1} α)
        ((Equiv.symm (equivShrink α) : (a : Shrink.{w, u_1} α) → α)
          ((equivShrink α : (a : α) → Shrink.{w, u_1} α) a : Shrink.{w, u_1} α))))
    (f
      ((Equiv.symm (equivShrink α) : (a : Shrink.{w, u_1} α) → α)
        ((equivShrink α : (a : α) → Shrink.{w, u_1} α) a : Shrink.{w, u_1} α)))
    (f a)
⊢ Shrink.rec (F := F) f ((equivShrink α : (a : α) → Shrink.{w, u_1} α) a) = f a

Tactic:
simp only [Shrink.rec, eqRec_eq_cast, cast_eq_iff_heq]

Premises used: eqRec_eq_cast, cast_eq_iff_heq, Shrink.rec
-- Module: Mathlib.Logic.Small.Defs
Goal:
α : Type u_1
inst : Small.{w, u_1} α
F : Shrink.{w, u_1} α → Sort v
f : (a : α) → F ((equivShrink α : (a : α) → Shrink.{w, u_1} α) a)
a : α
rw rw₁ : f a ≍ f a
⊢ HEq (α :=
    F
      ((equivShrink α : (a : α) → Shrink.{w, u_1} α)
        ((Equiv.symm (equivShrink α) : (a : Shrink.{w, u_1} α) → α)
          ((equivShrink α : (a : α) → Shrink.{w, u_1} α) a : Shrink.{w, u_1} α))))
    (f
      ((Equiv.symm (equivShrink α) : (a : Shrink.{w, u_1} α) → α)
        ((equivShrink α : (a : α) → Shrink.{w, u_1} α) a : Shrink.{w, u_1} α)))
    (f a)

Tactic:
rw [Equiv.symm_apply_apply]

Premises used: Equiv.symm_apply_apply
-- Module: Mathlib.Logic.Small.Defs
Goal:
α : Type v
⊢ Small.{v, v} α

Tactic:
Small.mk' <| Equiv.refl α

Premises used: Small.mk', Equiv.refl
-- Module: Mathlib.Logic.Small.Defs
Goal:
α : Type u_1
β : Type u_2
hβ : Small.{w, u_2} β
e : α ≃ β
⊢ Small.{w, u_1} α

Tactic:
let ⟨_, ⟨f⟩⟩ := hβ.equiv_small
  Small.mk' (e.trans f)

Premises used: Equiv.trans, Small.mk', Small.equiv_small, _private.0.small_map.match_1, Small
-- Module: Mathlib.Logic.Small.Defs
Goal:
α : Type u
hα : Small.{v, u} α
⊢ Small.{max v w, u} α

Tactic:
let ⟨⟨_, ⟨f⟩⟩⟩ := hα
  Small.mk' <| f.trans (Equiv.ulift.{w}).symm

Premises used: Equiv.trans, Small.mk', Equiv.ulift, Equiv.symm, _private.0.small_lift.match_1, Small
-- Module: Mathlib.Logic.Small.Defs
Goal:
α : Type v
⊢ Small.{max w v, v} α

Tactic:
small_lift.{v, w} α

Premises used: small_lift
-- Module: Mathlib.Logic.Small.Defs
Goal:
α : Type
⊢ Small.{w, 0} α

Tactic:
small_max α

Premises used: small_max
-- Module: Mathlib.Logic.Small.Defs
Goal:
α : Type v
⊢ Small.{v + 1, v} α

Tactic:
small_lift.{v, v + 1} α

Premises used: small_lift
-- Module: Mathlib.Logic.Small.Defs
Goal:
α : Type u
inst : Small.{v, u} α
⊢ Small.{v, max w u} (ULift.{w, u} α)

Tactic:
small_map Equiv.ulift

Premises used: Equiv.ulift, small_map
-- Module: Mathlib.Logic.Small.Defs
Goal:
α : Type u
inst : Small.{v, u} α
⊢ Small.{v, u + 1} (PLift α)

Tactic:
small_map Equiv.plift

Premises used: Equiv.plift, small_map
-- Module: Mathlib.Logic.Small.Defs
Goal:
⊢ Small.{max (u + 1) v, u + 1} (Type u)

Tactic:
small_max.{max (u + 1) v} _

Premises used: small_max
-- Module: Mathlib.Logic.Small.Defs
Goal:
α : Type u
inst : Small.{v, u} α
inst_1 : Nontrivial α
⊢ Nontrivial.{v} (Shrink.{v, u} α)

Tactic:
(equivShrink α).symm.nontrivial

Premises used: Equiv.nontrivial, Equiv.symm, equivShrink
-- Module: Mathlib.Logic.Small.Defs
Goal:
α : Type u_1
β : Type u_2
e : α ≃ β
⊢ Small.{w, u_1} α ↔ Small.{w, u_2} β

Tactic:
⟨fun h => @small_map _ _ h e.symm, fun h => @small_map _ _ h e⟩

Premises used: Iff.intro, small_map, Equiv.symm
-- Module: Mathlib.Logic.Small.Defs
Goal:
α : Type u_2
β : α → Type u_1
inst : Small.{w, u_2} α
inst_1 : ∀ (a : α), Small.{w, u_1} (β a)
a : α
⊢ Equiv.{u_1 + 1, w + 1} (β a)
    (Shrink.{w, u_1}
      (β
        ((Equiv.symm (equivShrink α) : (a : Shrink.{w, u_2} α) → α)
          ((equivShrink α : (a : α) → Shrink.{w, u_2} α) a : Shrink.{w, u_2} α))))

Tactic:
simpa using equivShrink (β a)

Premises used: equivShrink
-- Module: Mathlib.Logic.Small.Defs
Goal:
S : Type u
e_1 : Type (max u v) ≃ S
a b : Set ((α : S) × (e_1.symm : (a : S) → Type (max u v)) α)
e :
  Eq (α := (α : S) × (e_1.symm : (a : S) → Type (max u v)) α)
    (Sigma.mk (β := fun (α : S) ↦ (e_1.symm : (a : S) → Type (max u v)) α)
        ((e_1 : (a : Type (max u v)) → S) (Set ((α : S) × (e_1.symm : (a : S) → Type (max u v)) α))) (cast ⋯ a) :
      (α : S) × (e_1.symm : (a : S) → Type (max u v)) α)
    (Sigma.mk (β := fun (α : S) ↦ (e_1.symm : (a : S) → Type (max u v)) α)
        ((e_1 : (a : Type (max u v)) → S) (Set ((α : S) × (e_1.symm : (a : S) → Type (max u v)) α))) (cast ⋯ b) :
      (α : S) × (e_1.symm : (a : S) → Type (max u v)) α)
⊢ Eq.{u + 1} (α := S) ((e_1 : (a : Type (max u v)) → S) (Set ((α : S) × (e_1.symm : (a : S) → Type (max u v)) α)) : S)
    ((e_1 : (a : Type (max u v)) → S) (Set ((α : S) × (e_1.symm : (a : S) → Type (max u v)) α)) : S)

Tactic:
injection e with h₁ h₂
-- Module: Mathlib.Logic.Small.Defs
Goal:
S : Type u
e_1 : Type (max u v) ≃ S
a b : Set ((α : S) × (e_1.symm : (a : S) → Type (max u v)) α)
e :
  Eq (α := (α : S) × (e_1.symm : (a : S) → Type (max u v)) α)
    (Sigma.mk (β := fun (α : S) ↦ (e_1.symm : (a : S) → Type (max u v)) α)
        ((e_1 : (a : Type (max u v)) → S) (Set ((α : S) × (e_1.symm : (a : S) → Type (max u v)) α))) (cast ⋯ a) :
      (α : S) × (e_1.symm : (a : S) → Type (max u v)) α)
    (Sigma.mk (β := fun (α : S) ↦ (e_1.symm : (a : S) → Type (max u v)) α)
        ((e_1 : (a : Type (max u v)) → S) (Set ((α : S) × (e_1.symm : (a : S) → Type (max u v)) α))) (cast ⋯ b) :
      (α : S) × (e_1.symm : (a : S) → Type (max u v)) α)
h₁ :
  Eq.{u + 1} (α := S) ((e_1 : (a : Type (max u v)) → S) (Set ((α : S) × (e_1.symm : (a : S) → Type (max u v)) α)) : S)
    ((e_1 : (a : Type (max u v)) → S) (Set ((α : S) × (e_1.symm : (a : S) → Type (max u v)) α)) : S)
⊢ cast ⋯ a = cast ⋯ b

Tactic:
injection e with h₁ h₂
-- Module: Mathlib.Logic.Small.Defs
Goal:
S : Type u
e : Type (max u v) ≃ S
a b : Set ((α : S) × (e.symm : (a : S) → Type (max u v)) α)
h₁ :
  Eq.{u + 1} (α := S) ((e : (a : Type (max u v)) → S) (Set ((α : S) × (e.symm : (a : S) → Type (max u v)) α)) : S)
    ((e : (a : Type (max u v)) → S) (Set ((α : S) × (e.symm : (a : S) → Type (max u v)) α)) : S)
h₂ : cast ⋯ a = cast ⋯ b
⊢ a = b

Tactic:
simpa using h₂
-- Module: Mathlib.Logic.Small.List
Goal:
α : Type v
n : ℕ
inst : Small.{u, v} α
⊢ Small.{u, v} (List.Vector α n)

Tactic:
small_of_injective (Equiv.vectorEquivFin α n).injective

Premises used: Equiv.vectorEquivFin, small_of_injective, Equiv.injective
-- Module: Mathlib.Logic.Small.List
Goal:
α : Type v
inst : Small.{u, v} α
e : (n : ℕ) × List.Vector α n ≃ List α := Equiv.sigmaFiberEquiv List.length
⊢ Small.{u, v} (List α)

Tactic:
small_of_surjective e.surjective

Premises used: small_of_surjective, Equiv.surjective
-- Module: Mathlib.Logic.Small.List
Goal:
α : Type v
inst : Small.{u, v} α
e : (n : ℕ) × List.Vector α n ≃ List α := Equiv.sigmaFiberEquiv List.length
⊢ Small.{u, v} (List α)

Tactic:
exact small_of_surjective e.surjective

Premises used: small_of_surjective, Equiv.surjective
-- Module: Mathlib.Logic.Small.Set
Goal:
α : Type u1
s t : Set α
hts : t ⊆ s
inst : Small.{u, u1} (↑s : Type u1)
⊢ Small.{u, u1} (↑t : Type u1)

Tactic:
small_of_injective (Set.inclusion_injective hts)

Premises used: small_of_injective, Set.inclusion_injective
-- Module: Mathlib.Logic.Small.Set
Goal:
α : Type u1
β : Type u2
γ : Type u3
ι : Type u4
s : Set α
inst : Small.{u, u1} (↑s : Type u1)
⊢ Small.{u, u1} (↑(𝒫 s) : Type u1)

Tactic:
small_map (Equiv.Set.powerset s)

Premises used: Equiv.Set.powerset, small_map
-- Module: Mathlib.Logic.Small.Set
Goal:
α : Type u1
β : Type u2
γ : Type u3
ι : Type u4
s : Set α
t : Set β
inst : Small.{u, u1} (↑s : Type u1)
inst_1 : Small.{u, u2} (↑t : Type u2)
⊢ Small.{u, max u1 u2} (↑(s ×ˢ t) : Type (max u1 u2))

Tactic:
small_of_injective (Equiv.Set.prod s t).injective

Premises used: small_of_injective, Equiv.Set.prod, Equiv.injective
-- Module: Mathlib.Logic.Small.Set
Goal:
α : Type u1
β_1 : Type u2
γ : Type u3
ι : Type u4
β : α → Type u2
s : (a : α) → Set (β a)
inst : Small.{u, u1} α
inst_1 : ∀ (a : α), Small.{u, u2} (↑(s a) : Type u2)
⊢ Small.{u, max u1 u2} (↑(Set.pi (α := β) Set.univ s) : Type (max u1 u2))

Tactic:
small_of_injective (Equiv.Set.univPi s).injective

Premises used: Equiv.Set.univPi, small_of_injective, Equiv.injective
-- Module: Mathlib.Logic.Small.Set
Goal:
α : Type u1
β : Type u2
γ : Type u3
ι : Type u4
f : α → β
inst : Small.{u, u1} α
⊢ Small.{u, u2} (↑(Set.range f) : Type u2)

Tactic:
small_of_surjective Set.rangeFactorization_surjective

Premises used: small_of_surjective, Set.rangeFactorization_surjective
-- Module: Mathlib.Logic.Small.Set
Goal:
α : Type u1
β : Type u2
γ : Type u3
ι : Type u4
f : α → β
s : Set α
inst : Small.{u, u1} (↑s : Type u1)
⊢ Small.{u, u2} (↑(f '' s) : Type u2)

Tactic:
small_of_surjective Set.imageFactorization_surjective

Premises used: small_of_surjective, Set.imageFactorization_surjective
-- Module: Mathlib.Logic.Small.Set
Goal:
α : Type u1
β : Type u2
γ : Type u3
ι : Type u4
f : α → β → γ
s : Set α
t : Set β
inst : Small.{u, u1} (↑s : Type u1)
inst_1 : Small.{u, u2} (↑t : Type u2)
rw : Small.{u, u3} (↑(Function.uncurry f '' s ×ˢ t) : Type u3)
⊢ Small.{u, u3} (↑(Set.image2 f s t) : Type u3)

Tactic:
rw [← Set.image_uncurry_prod]

Premises used: Set.image_uncurry_prod
-- Module: Mathlib.Logic.Small.Set
Goal:
α : Type u1
β : Type u2
γ : Type u3
ι : Type u4
f : α → β → γ
s : Set α
t : Set β
inst : Small.{u, u1} (↑s : Type u1)
inst_1 : Small.{u, u2} (↑t : Type u2)
⊢ Small.{u, u3} (↑(Function.uncurry f '' s ×ˢ t) : Type u3)

Tactic:
infer_instance
-- Module: Mathlib.Logic.Small.Set
Goal:
α : Type u1
⊢ Small.{u, u1} (↑Set.univ : Type u1) ↔ Small.{u, u1} α

Tactic:
small_congr <| Equiv.Set.univ α

Premises used: small_congr, Equiv.Set.univ
-- Module: Mathlib.Logic.Small.Set
Goal:
α : Type u1
β : Type u2
γ : Type u3
ι : Type u4
h : Small.{u, u1} α
⊢ Small.{u, u1} (↑Set.univ : Type u1)

Tactic:
small_univ_iff.2 h

Premises used: Iff.mpr, small_univ_iff
-- Module: Mathlib.Logic.Small.Set
Goal:
α : Type u1
β : Type u2
γ : Type u3
ι : Type u4
s t : Set α
inst : Small.{u, u1} (↑s : Type u1)
inst_1 : Small.{u, u1} (↑t : Type u1)
rw :
  Small.{u, u1}
    (↑(Set.range (ι := { x : α // x ∈ s } ⊕ { x : α // x ∈ t })
          (Sum.elim (Subtype.val (p := fun (x : α) ↦ x ∈ s)) (Subtype.val (p := fun (x : α) ↦ x ∈ t)))) :
      Type u1)
⊢ Small.{u, u1} (↑(s ∪ t) : Type u1)

Tactic:
rw [← Subtype.range_val (s := s), ← Subtype.range_val (s := t), ← Set.Sum.elim_range]

Premises used: Set.Sum.elim_range, Subtype.range_val
-- Module: Mathlib.Logic.Small.Set
Goal:
α : Type u1
β : Type u2
γ : Type u3
ι : Type u4
s t : Set α
inst : Small.{u, u1} (↑s : Type u1)
inst_1 : Small.{u, u1} (↑t : Type u1)
⊢ Small.{u, u1}
    (↑(Set.range (ι := { x : α // x ∈ s } ⊕ { x : α // x ∈ t })
          (Sum.elim (Subtype.val (p := fun (x : α) ↦ x ∈ s)) (Subtype.val (p := fun (x : α) ↦ x ∈ t)))) :
      Type u1)

Tactic:
infer_instance
-- Module: Mathlib.Logic.Small.Set
Goal:
α : Type u1
β : Type u2
γ : Type u3
ι : Type u4
inst : Small.{u, u4} ι
s : ι → Set α
inst_1 : ∀ (i : ι), Small.{u, u1} (↑(s i) : Type u1)
⊢ Small.{u, u1} (↑(⋃ (i : ι), s i) : Type u1)

Tactic:
small_of_surjective <| Set.sigmaToiUnion_surjective _

Premises used: small_of_surjective, Set.sigmaToiUnion_surjective
-- Module: Mathlib.Logic.Small.Set
Goal:
α : Type u1
β : Type u2
γ : Type u3
ι : Type u4
s : Set (Set α)
inst : Small.{u, u1} (↑s : Type u1)
inst_1 : ∀ (t : (↑s : Type u1)), Small.{u, u1} (↑(↑t : Set α) : Type u1)
⊢ Small.{u, u1} (↑(⋃₀ s) : Type u1)

Tactic:
Set.sUnion_eq_iUnion ▸ small_iUnion _

Premises used: Set.sUnion_eq_iUnion, Eq.rec, small_iUnion, Eq.symm
-- Module: Mathlib.Logic.Small.Set
Goal:
α : Type u1
β : Type u2
γ : Type u3
ι : Type u4
s : Set ι
inst : Small.{u, u4} (↑s : Type u4)
f : (i : ι) → i ∈ s → Set α
inst_1 : ∀ (i : ι) (hi : i ∈ s), Small.{u, u1} (↑(f i hi) : Type u1)
⊢ Small.{u, u1} (↑(⋃ (i : ι), ⋃ (hi : i ∈ s), f i hi) : Type u1)

Tactic:
Set.biUnion_eq_iUnion s f ▸ small_iUnion _

Premises used: Eq.rec, small_iUnion, Set.biUnion_eq_iUnion, Eq.symm
-- Module: Mathlib.Logic.Small.Set
Goal:
α : Type u1
β : Type u2
γ : Type u3
ι : Type u4
x : α
s : Set α
inst : Small.{u, u1} (↑s : Type u1)
⊢ Small.{u, u1} (↑(insert x s) : Type u1)

Tactic:
Set.insert_eq x s ▸ small_union.{u} {x} s

Premises used: small_union, Set.insert_eq, Eq.rec, Singleton.singleton, Eq.symm
-- Module: Mathlib.Logic.Small.Set
Goal:
α : Type u1
β : Type u2
γ : Type u3
ι : Type u4
s t : Set α
inst : Small.{u, u1} (↑s : Type u1)
⊢ Small.{u, u1} (↑(s \ t) : Type u1)

Tactic:
small_subset (Set.diff_subset)

Premises used: Set.diff_subset, small_subset
-- Module: Mathlib.Logic.Small.Set
Goal:
α : Type u1
β : Type u2
γ : Type u3
ι : Type u4
s : Set α
P : α → Prop
inst : Small.{u, u1} (↑s : Type u1)
⊢ Small.{u, u1} (↑{x : α | x ∈ s ∧ P x} : Type u1)

Tactic:
small_subset (Set.sep_subset s P)

Premises used: small_subset, Set.sep_subset
-- Module: Mathlib.Logic.Small.Set
Goal:
α : Type u1
β : Type u2
γ : Type u3
ι : Type u4
s t : Set α
inst : Small.{u, u1} (↑s : Type u1)
⊢ Small.{u, u1} (↑(s ∩ t) : Type u1)

Tactic:
small_subset Set.inter_subset_left

Premises used: Set.inter_subset_left, small_subset
-- Module: Mathlib.Logic.Small.Set
Goal:
α : Type u1
β : Type u2
γ : Type u3
ι : Type u4
s t : Set α
inst : Small.{u, u1} (↑t : Type u1)
⊢ Small.{u, u1} (↑(s ∩ t) : Type u1)

Tactic:
small_subset Set.inter_subset_right

Premises used: small_subset, Set.inter_subset_right
-- Module: Mathlib.Logic.Small.Set
Goal:
α : Type u1
ι : Type u4
s : ι → Set α
i : ι
inst : Small.{u, u1} (↑(s i) : Type u1)
⊢ Small.{u, u1} (↑(⋂ (i : ι), s i) : Type u1)

Tactic:
small_subset (Set.iInter_subset s i)

Premises used: small_subset, Set.iInter_subset
-- Module: Mathlib.Logic.Small.Set
Goal:
α : Type u1
β : Type u2
γ : Type u3
ι : Type u4
inst : Nonempty ι
s : ι → Set α
inst_1 : ∀ (i : ι), Small.{u, u1} (↑(s i) : Type u1)
⊢ Small.{u, u1} (↑(⋂ (i : ι), s i) : Type u1)

Tactic:
let ⟨i⟩ : Nonempty ι := inferInstance
  small_iInter s i

Premises used: Set.iInter, inferInstance, Set.Elem, small_iInter, _private.0.small_iInter'.match_1, Small
-- Module: Mathlib.Logic.Small.Set
Goal:
α : Type u1
s : Set (Set α)
t : Set α
ht : t ∈ s
inst : Small.{u, u1} (↑t : Type u1)
⊢ Small.{u, u1} (↑(⋂₀ s) : Type u1)

Tactic:
Set.sInter_eq_iInter ▸ small_iInter _ ⟨t, ht⟩

Premises used: Set.sInter_eq_iInter, Eq.rec, Subtype.mk, Eq.symm, small_iInter