case mk.mk.mk.intro
α✝ β✝ : Type u
a✝ : Cardinal
α : Type u_1
b✝ : Cardinal
β : Type u_1
c✝ : Cardinal
γ : Type u_1
hα : Quot.mk Setoid.r α ≠ 0
e : β ↪ γ
⊢ Quot.mk Setoid.r α ^ Quot.mk Setoid.r β ≤ Quot.mk Setoid.r α ^ Quot.mk Setoid.r γ
α β : Type u
⊢ ∀ {a b c : Cardinal}, a ≠ 0 → b ≤ c → a ^ b ≤ a ^ c
rintro ⟨α⟩ ⟨β⟩ ⟨γ⟩ hα ⟨e⟩
case mk.mk.mk.intro
α✝ β✝ : Type u
a✝ : Cardinal
α : Type u_1
b✝ : Cardinal
β : Type u_1
c✝ : Cardinal
γ : Type u_1
hα : Quot.mk Setoid.r α ≠ 0
e : β ↪ γ
a : α
⊢ Quot.mk Setoid.r α ^ Quot.mk Setoid.r β ≤ Quot.mk Setoid.r α ^ Quot.mk Setoid.r γ
case mk.mk.mk.intro
α✝ β✝ : Type u
a✝ : Cardinal
α : Type u_1
b✝ : Cardinal
β : Type u_1
c✝ : Cardinal
γ : Type u_1
hα : Quot.mk Setoid.r α ≠ 0
e : β ↪ γ
⊢ Quot.mk Setoid.r α ^ Quot.mk Setoid.r β ≤ Quot.mk Setoid.r α ^ Quot.mk Setoid.r γ
let ⟨a⟩ := mk_ne_zero_iff.1 hα
no goals
case mk.mk.mk.intro
α✝ β✝ : Type u
a✝ : Cardinal
α : Type u_1
b✝ : Cardinal
β : Type u_1
c✝ : Cardinal
γ : Type u_1
hα : Quot.mk Setoid.r α ≠ 0
e : β ↪ γ
a : α
⊢ Quot.mk Setoid.r α ^ Quot.mk Setoid.r β ≤ Quot.mk Setoid.r α ^ Quot.mk Setoid.r γ
exact ⟨@Function.Embedding.arrowCongrLeft _ _ _ ⟨a⟩ e⟩