awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.SetTheory.Cardinal.Order
Goal:
ι : Type u_1
f g : ι → Cardinal.{u_2}
this : (sum.{u_1, u_2} fun (i : ι) ↦ f i + g i) = (sum.{u_1, u_2} fun (i : ι) ↦ f i) + sum.{u_1, u_2} fun (i : ι) ↦ g i
⊢ sum (f + g) = sum f + sum g

Tactic:
exact this
-- Module: Mathlib.SetTheory.Cardinal.Order
Goal:
ι : Type u_1
f g : ι → Cardinal.{u_2}
⊢ (sum.{u_1, u_2} fun (i : ι) ↦ f i + g i) = sum f + sum g

Tactic:
sum_add_distrib f g

Premises used: Cardinal.sum_add_distrib
-- Module: Mathlib.SetTheory.Cardinal.Order
Goal:
ι : Type u_1
f g : ι → Cardinal.{u_2}
H : ∀ (i : ι), f i ≤ g i
i : ι
⊢ f i ≤ g i

Tactic:
have := H i
-- Module: Mathlib.SetTheory.Cardinal.Order
Goal:
ι : Type u_1
f g : ι → Cardinal.{u_2}
H : ∀ (i : ι), f i ≤ g i
i : ι
this : f i ≤ g i
rwa :
  ∀
    (this :
      Quot.mk (⇑isEquivalent : Type u_2 → Type u_2 → Prop)
          (Quot.out (r := (⇑isEquivalent : Type u_2 → Type u_2 → Prop)) (f i)) ≤
        g i),
    Nonempty.{u_2 + 1} (Quotient.out (f i) ↪ Quotient.out (g ((Embedding.refl ι : (a : ι) → ι) i)))
rwa₁ rwa₂ rwa₃ rwa₄ :
  ∀
    (this :
      LE.le (α := Cardinal.{u_2})
        (Quot.mk (⇑isEquivalent : Type u_2 → Type u_2 → Prop)
          (Quot.out (r := (⇑isEquivalent : Type u_2 → Type u_2 → Prop)) (f i)))
        (Quot.mk (⇑isEquivalent : Type u_2 → Type u_2 → Prop)
          (Quot.out (r := (⇑isEquivalent : Type u_2 → Type u_2 → Prop)) (g i)))),
    Nonempty.{u_2 + 1} (Quotient.out (f i) ↪ Quotient.out (g ((Embedding.refl ι : (a : ι) → ι) i)))
⊢ Nonempty.{u_2 + 1} (Quotient.out (f i) ↪ Quotient.out (g ((Embedding.refl ι : (a : ι) → ι) i)))

Tactic:
rwa [← Quot.out_eq (f i), ← Quot.out_eq (g i)] at this

Premises used: Quot.out_eq
-- Module: Mathlib.SetTheory.Cardinal.Order
Goal:
α β : Type u
c : Cardinal.{u}
f : α → β
hf : ∀ (b : β), #(↑(f ⁻¹' {b}) : Type u) ≤ c
⊢ #α ≤ #β * c

Tactic:
simpa only [← mk_congr (@Equiv.sigmaFiberEquiv α β f), mk_sigma, ← sum_const'] using
    sum_le_sum _ _ hf

Premises used: Equiv.sigmaFiberEquiv, Cardinal.sum_le_sum, Cardinal.sum_const', Cardinal.mk_sigma, Cardinal.mk_congr
-- Module: Mathlib.SetTheory.Cardinal.Order
Goal:
α : Type u
β : Type v
c : Cardinal.{max u v}
f : α → β
hf : ∀ (b : β), lift.{v, u} #(↑(f ⁻¹' {b}) : Type u) ≤ c
b : β
rw :
  (↑(preimage (β := ULift.{v, u} α) (⇑(Equiv.symm Equiv.ulift) : (a : α) → ULift.{v, u} α)
          (preimage (β := ULift.{u, v} β) (fun (x : ULift.{v, u} α) ↦ { down := f x.down })
            {{ down := b : ULift.{u, v} β }})) :
      Type u) ≃
    (↑(f ⁻¹' {b}) : Type u)
⊢ (↑(image (α := ULift.{v, u} α) (⇑Equiv.ulift : (a : ULift.{v, u} α) → α)
          (preimage (β := ULift.{u, v} β) (fun (x : ULift.{v, u} α) ↦ { down := f x.down })
            {{ down := b : ULift.{u, v} β }})) :
      Type u) ≃
    (↑(f ⁻¹' {b}) : Type u)

Tactic:
rw [Equiv.image_eq_preimage_symm]

Premises used: Equiv.image_eq_preimage_symm
-- Module: Mathlib.SetTheory.Cardinal.Order
Goal:
α : Type u
β : Type v
c : Cardinal.{max u v}
f : α → β
hf : ∀ (b : β), lift.{v, u} #(↑(f ⁻¹' {b}) : Type u) ≤ c
b : β
simp :
  { x : α // f (ULift.down.{v, u} ((Equiv.symm Equiv.ulift : (a : α) → ULift.{v, u} α) x)) = b } ≃ { x : α // f x = b }
⊢ (↑(preimage (β := ULift.{v, u} α) (⇑(Equiv.symm Equiv.ulift) : (a : α) → ULift.{v, u} α)
          (preimage (β := ULift.{u, v} β) (fun (x : ULift.{v, u} α) ↦ { down := f x.down })
            {{ down := b : ULift.{u, v} β }})) :
      Type u) ≃
    (↑(f ⁻¹' {b}) : Type u)

Tactic:
simp only [preimage, mem_singleton_iff, ULift.up_inj, mem_setOf_eq, coe_setOf]

Premises used: ULift.up_inj, Set.mem_setOf_eq, Set.mem_singleton_iff, Set.preimage, Set.coe_setOf
-- Module: Mathlib.SetTheory.Cardinal.Order
Goal:
α : Type u
β : Type v
c : Cardinal.{max u v}
f : α → β
hf : ∀ (b : β), lift.{v, u} #(↑(f ⁻¹' {b}) : Type u) ≤ c
b : β
⊢ { x : α // f (ULift.down.{v, u} ((Equiv.symm Equiv.ulift : (a : α) → ULift.{v, u} α) x)) = b } ≃ { x : α // f x = b }

Tactic:
exact Equiv.refl _

Premises used: Equiv.refl
-- Module: Mathlib.SetTheory.Cardinal.Order
Goal:
α : Type u
h : Nonempty.{u + 2} (Cardinal.{u} ↪ α)
f : Cardinal.{u} → α
hf : Injective f
g : α → Cardinal.{u} := invFun f
x : α
hx : g x = HPow.hPow (α := Cardinal.{u}) 2 (Cardinal.sum g)
this : g x ≤ Cardinal.sum g
rw : Cardinal.sum g < HPow.hPow (α := Cardinal.{u}) 2 (Cardinal.sum g)
⊢ Cardinal.sum g < g x

Tactic:
rw [hx]
-- Module: Mathlib.SetTheory.Cardinal.Order
Goal:
α : Type u
h : Nonempty.{u + 2} (Cardinal.{u} ↪ α)
f : Cardinal.{u} → α
hf : Injective f
g : α → Cardinal.{u} := invFun f
x : α
hx : g x = HPow.hPow (α := Cardinal.{u}) 2 (Cardinal.sum g)
this : g x ≤ Cardinal.sum g
⊢ Cardinal.sum g < HPow.hPow (α := Cardinal.{u}) 2 (Cardinal.sum g)

Tactic:
cantor _

Premises used: Cardinal.cantor
-- Module: Mathlib.SetTheory.Cardinal.Order
Goal:
α : Type u
h : Nonempty.{u + 2} (Cardinal.{u} ↪ α)
f : Cardinal.{u} → α
hf : Injective f
g : α → Cardinal.{u} := invFun f
x : α
hx : g x = HPow.hPow (α := Cardinal.{u}) 2 (Cardinal.sum g)
this : g x ≤ Cardinal.sum g
⊢ Cardinal.sum g < HPow.hPow (α := Cardinal.{u}) 2 (Cardinal.sum g)

Tactic:
exact cantor _

Premises used: Cardinal.cantor
-- Module: Mathlib.SetTheory.Cardinal.Order
Goal:
α β : Type u
⊢ IsWellOrder α WellOrderingRel

Tactic:
(RelEmbedding.preimage _ _).isWellOrder

Premises used: RelEmbedding.isWellOrder, RelEmbedding.preimage, WellOrderingRel
-- Module: Mathlib.SetTheory.Cardinal.Order
Goal:
α β : Type u
⊢ Nonempty.{max 1 (u + 1)} { r : α → α → Prop // IsWellOrder α r }

Tactic:
⟨⟨WellOrderingRel, inferInstance⟩⟩

Premises used: inferInstance, Nonempty.intro, Subtype.mk, WellOrderingRel
-- Module: Mathlib.SetTheory.Cardinal.Order
Goal:
α : Type u
⊢ WellFoundedGT α

Tactic:
simpa [isWellFounded_iff] using WellOrderingRel.isWellOrder.wf

Premises used: isWellFounded_iff, IsWellFounded.wf
-- Module: Mathlib.SetTheory.Cardinal.Order
Goal:
α : Type u
⊢ ∃ (x : LinearOrder α), WellFoundedGT α

Tactic:
exact ⟨linearOrderOfSTO (Function.swap WellOrderingRel),
    by simpa [isWellFounded_iff] using WellOrderingRel.isWellOrder.wf⟩
-- Module: Mathlib.SetTheory.Cardinal.Order
Goal:
α : Type u
⊢ ∃ (x : LinearOrder α), WellFoundedGT α

Tactic:
classical
  exact ⟨linearOrderOfSTO (Function.swap WellOrderingRel),
    by simpa [isWellFounded_iff] using WellOrderingRel.isWellOrder.wf⟩
-- Module: Mathlib.SetTheory.Cardinal.Order
Goal:
α : Type u
⊢ ∃ (x : LinearOrder α), WellFoundedLT α

Tactic:
⟨linearOrderOfSTO WellOrderingRel, WellOrderingRel.isWellOrder.toIsWellFounded⟩

Premises used: IsWellOrder.toIsWellFounded, Exists.intro, linearOrderOfSTO, WellOrderingRel
-- Module: Mathlib.SetTheory.Cardinal.Order
Goal:
α : Type u
⊢ ∃ (x : LinearOrder α), WellFoundedLT α

Tactic:
exact ⟨linearOrderOfSTO WellOrderingRel, WellOrderingRel.isWellOrder.toIsWellFounded⟩
-- Module: Mathlib.SetTheory.Cardinal.Order
Goal:
α : Type u
⊢ ∃ (x : LinearOrder α), WellFoundedLT α

Tactic:
classical
  exact ⟨linearOrderOfSTO WellOrderingRel, WellOrderingRel.isWellOrder.toIsWellFounded⟩
-- Module: Mathlib.SetTheory.Cardinal.Order
Goal:
ι : Type u
f : ι → Cardinal.{v}
ω : Cardinal.{v}
hω : ¬IsSuccPrelimit ω
h : ⨆ (i : ι), f i = ω
subst : ∀ (hω : ¬IsSuccPrelimit.{v + 1} (α := Cardinal.{v}) (⨆ (i : ι), f i)), ∃ (i : ι), f i = ⨆ (i : ι), f i
⊢ ∃ (i : ι), f i = ω

Tactic:
subst h
-- Module: Mathlib.SetTheory.Cardinal.Order
Goal:
ι : Type u
f : ι → Cardinal.{v}
hω : ¬IsSuccPrelimit.{v + 1} (α := Cardinal.{v}) (⨆ (i : ι), f i)
⊢ ∃ (i : ι), f i = ⨆ (i : ι), f i

Tactic:
exists_eq_ciSup_of_not_isSuccPrelimit' hω

Premises used: exists_eq_ciSup_of_not_isSuccPrelimit'
-- Module: Mathlib.SetTheory.Cardinal.Order
Goal:
ι : Type u
f : ι → Cardinal.{v}
hω : ¬IsSuccPrelimit.{v + 1} (α := Cardinal.{v}) (⨆ (i : ι), f i)
⊢ ∃ (i : ι), f i = ⨆ (i : ι), f i

Tactic:
exact exists_eq_ciSup_of_not_isSuccPrelimit' hω

Premises used: exists_eq_ciSup_of_not_isSuccPrelimit'
-- Module: Mathlib.SetTheory.Cardinal.Order
Goal:
ι : Type u
hι : Nonempty ι
f : ι → Cardinal.{v}
hf : BddAbove (Set.range f)
c : Cardinal.{v}
hc : ¬IsSuccLimit c
h : ⨆ (i : ι), f i = c
subst : ∀ (hc : ¬IsSuccLimit.{v + 1} (α := Cardinal.{v}) (⨆ (i : ι), f i)), ∃ (i : ι), f i = ⨆ (i : ι), f i
⊢ ∃ (i : ι), f i = c

Tactic:
subst h
-- Module: Mathlib.SetTheory.Cardinal.Order
Goal:
ι : Type u
hι : Nonempty ι
f : ι → Cardinal.{v}
hf : BddAbove (Set.range f)
hc : ¬IsSuccLimit.{v + 1} (α := Cardinal.{v}) (⨆ (i : ι), f i)
⊢ ∃ (i : ι), f i = ⨆ (i : ι), f i

Tactic:
exists_eq_ciSup_of_not_isSuccLimit hf hc

Premises used: exists_eq_ciSup_of_not_isSuccLimit
-- Module: Mathlib.SetTheory.Cardinal.Order
Goal:
ι : Type u
hι : Nonempty ι
f : ι → Cardinal.{v}
hf : BddAbove (Set.range f)
hc : ¬IsSuccLimit.{v + 1} (α := Cardinal.{v}) (⨆ (i : ι), f i)
⊢ ∃ (i : ι), f i = ⨆ (i : ι), f i

Tactic:
exact exists_eq_ciSup_of_not_isSuccLimit hf hc

Premises used: exists_eq_ciSup_of_not_isSuccLimit
-- Module: Mathlib.SetTheory.Cardinal.Order
Goal:
ι : Type u_1
f g : ι → Cardinal.{u_2}
H : ∀ (i : ι), f i < g i
h : prod g ≤ sum f
F : ((i : ι) → Quotient.out (g i)) ↪ (i : ι) × Quotient.out (f i)
refine : ∀ (i : ι), #(Quotient.out (g i)) ≠ 0
⊢ Inhabited ((i : ι) → Quotient.out (g i))

Tactic:
refine ⟨fun i => Classical.choice <| mk_ne_zero_iff.1 ?_⟩
-- Module: Mathlib.SetTheory.Cardinal.Order
Goal:
ι : Type u_1
f g : ι → Cardinal.{u_2}
H : ∀ (i : ι), f i < g i
h : prod g ≤ sum f
F : ((i : ι) → Quotient.out (g i)) ↪ (i : ι) × Quotient.out (f i)
i : ι
rw : g i ≠ 0
⊢ #(Quotient.out (g i)) ≠ 0

Tactic:
rw [mk_out]

Premises used: Cardinal.mk_out
-- Module: Mathlib.SetTheory.Cardinal.Order
Goal:
ι : Type u_1
f g : ι → Cardinal.{u_2}
H : ∀ (i : ι), f i < g i
h : prod g ≤ sum f
F : ((i : ι) → Quotient.out (g i)) ↪ (i : ι) × Quotient.out (f i)
i : ι
⊢ g i ≠ 0

Tactic:
(H i).ne_bot

Premises used: LT.lt.ne_bot
-- Module: Mathlib.SetTheory.Cardinal.Order
Goal:
ι : Type u_1
f g : ι → Cardinal.{u_2}
H : ∀ (i : ι), f i < g i
h : prod g ≤ sum f
F : ((i : ι) → Quotient.out (g i)) ↪ (i : ι) × Quotient.out (f i)
i : ι
⊢ g i ≠ 0

Tactic:
exact (H i).ne_bot

Premises used: LT.lt.ne_bot
-- Module: Mathlib.SetTheory.Cardinal.Order
Goal:
ι : Type u_1
f g : ι → Cardinal.{u_2}
H : ∀ (i : ι), f i < g i
h : prod g ≤ sum f
F : ((i : ι) → Quotient.out (g i)) ↪ (i : ι) × Quotient.out (f i)
have : ∀ (this : Inhabited ((i : ι) → Quotient.out (g i))), False
⊢ False

Tactic:
have : Inhabited (∀ i : ι, (g i).out) := by
      refine ⟨fun i => Classical.choice <| mk_ne_zero_iff.1 ?_⟩
      rw [mk_out]
      exact (H i).ne_bot
-- Module: Mathlib.SetTheory.Cardinal.Order
Goal:
ι : Type u_1
f g : ι → Cardinal.{u_2}
H : ∀ (i : ι), f i < g i
h : prod g ≤ sum f
F : ((i : ι) → Quotient.out (g i)) ↪ (i : ι) × Quotient.out (f i)
this : Inhabited ((i : ι) → Quotient.out (g i))
G : (i : ι) × Quotient.out (f i) → (i : ι) → Quotient.out (g i) :=
  invFun (⇑F : (a : (i : ι) → Quotient.out (g i)) → (i : ι) × Quotient.out (f i))
⊢ Surjective G

Tactic:
have sG : Surjective G := invFun_surjective F.2
-- Module: Mathlib.SetTheory.Cardinal.Order
Goal:
ι : Type u_1
f g : ι → Cardinal.{u_2}
H : ∀ (i : ι), f i < g i
h : prod g ≤ sum f
F : ((i : ι) → Quotient.out (g i)) ↪ (i : ι) × Quotient.out (f i)
this : Inhabited ((i : ι) → Quotient.out (g i))
G : (i : ι) × Quotient.out (f i) → (i : ι) → Quotient.out (g i) :=
  invFun (⇑F : (a : (i : ι) → Quotient.out (g i)) → (i : ι) × Quotient.out (f i))
sG : Surjective G
i : ι
simp :
  ¬∀ (x : Quotient.out (g i)),
      ∃ (x_1 : Quotient.out (f i)), G (Sigma.mk (β := fun (i : ι) ↦ Quotient.out (f i)) i x_1) i = x
⊢ ∃ (b : Quotient.out (g i)), ∀ (a : Quotient.out (f i)), G (Sigma.mk (β := fun (i : ι) ↦ Quotient.out (f i)) i a) i ≠ b

Tactic:
simp only [not_exists.symm, not_forall.symm]

Premises used: not_exists, Classical.not_forall, Iff.symm
-- Module: Mathlib.SetTheory.Cardinal.Order
Goal:
ι : Type u_1
f g : ι → Cardinal.{u_2}
H : ∀ (i : ι), f i < g i
h : prod g ≤ sum f
F : ((i : ι) → Quotient.out (g i)) ↪ (i : ι) × Quotient.out (f i)
this : Inhabited ((i : ι) → Quotient.out (g i))
G : (i : ι) × Quotient.out (f i) → (i : ι) → Quotient.out (g i) :=
  invFun (⇑F : (a : (i : ι) → Quotient.out (g i)) → (i : ι) × Quotient.out (f i))
sG : Surjective G
i : ι
⊢ ¬∀ (x : Quotient.out (g i)),
      ∃ (x_1 : Quotient.out (f i)), G (Sigma.mk (β := fun (i : ι) ↦ Quotient.out (f i)) i x_1) i = x

Tactic:
fun h => (H i).not_ge ?_

Premises used: LT.lt.not_ge, Not
-- Module: Mathlib.SetTheory.Cardinal.Order
Goal:
ι : Type u_1
f g : ι → Cardinal.{u_2}
H : ∀ (i : ι), f i < g i
h : prod g ≤ sum f
F : ((i : ι) → Quotient.out (g i)) ↪ (i : ι) × Quotient.out (f i)
this : Inhabited ((i : ι) → Quotient.out (g i))
G : (i : ι) × Quotient.out (f i) → (i : ι) → Quotient.out (g i) :=
  invFun (⇑F : (a : (i : ι) → Quotient.out (g i)) → (i : ι) × Quotient.out (f i))
sG : Surjective G
i : ι
refine :
  ∀
    (h :
      ∀ (x : Quotient.out (g i)),
        ∃ (x_1 : Quotient.out (f i)), G (Sigma.mk (β := fun (i : ι) ↦ Quotient.out (f i)) i x_1) i = x),
    g i ≤ f i
⊢ ¬∀ (x : Quotient.out (g i)),
      ∃ (x_1 : Quotient.out (f i)), G (Sigma.mk (β := fun (i : ι) ↦ Quotient.out (f i)) i x_1) i = x

Tactic:
refine fun h => (H i).not_ge ?_

Premises used: LT.lt.not_ge
-- Module: Mathlib.SetTheory.Cardinal.Order
Goal:
ι : Type u_1
f g : ι → Cardinal.{u_2}
H : ∀ (i : ι), f i < g i
h_1 : prod g ≤ sum f
F : ((i : ι) → Quotient.out (g i)) ↪ (i : ι) × Quotient.out (f i)
this : Inhabited ((i : ι) → Quotient.out (g i))
G : (i : ι) × Quotient.out (f i) → (i : ι) → Quotient.out (g i) :=
  invFun (⇑F : (a : (i : ι) → Quotient.out (g i)) → (i : ι) × Quotient.out (f i))
sG : Surjective G
i : ι
h :
  ∀ (x : Quotient.out (g i)),
    ∃ (x_1 : Quotient.out (f i)), G (Sigma.mk (β := fun (i : ι) ↦ Quotient.out (f i)) i x_1) i = x
rw : #(Quotient.out (g i)) ≤ #(Quotient.out (f i))
⊢ g i ≤ f i

Tactic:
rw [← mk_out (f i), ← mk_out (g i)]

Premises used: Cardinal.mk_out
-- Module: Mathlib.SetTheory.Cardinal.Order
Goal:
ι : Type u_1
f g : ι → Cardinal.{u_2}
H : ∀ (i : ι), f i < g i
h_1 : prod g ≤ sum f
F : ((i : ι) → Quotient.out (g i)) ↪ (i : ι) × Quotient.out (f i)
this : Inhabited ((i : ι) → Quotient.out (g i))
G : (i : ι) × Quotient.out (f i) → (i : ι) → Quotient.out (g i) :=
  invFun (⇑F : (a : (i : ι) → Quotient.out (g i)) → (i : ι) × Quotient.out (f i))
sG : Surjective G
i : ι
h :
  ∀ (x : Quotient.out (g i)),
    ∃ (x_1 : Quotient.out (f i)), G (Sigma.mk (β := fun (i : ι) ↦ Quotient.out (f i)) i x_1) i = x
⊢ #(Quotient.out (g i)) ≤ #(Quotient.out (f i))

Tactic:
⟨Embedding.ofSurjective _ h⟩

Premises used: Function.Embedding.ofSurjective, Nonempty.intro
-- Module: Mathlib.SetTheory.Cardinal.Order
Goal:
ι : Type u_1
f g : ι → Cardinal.{u_2}
H : ∀ (i : ι), f i < g i
h_1 : prod g ≤ sum f
F : ((i : ι) → Quotient.out (g i)) ↪ (i : ι) × Quotient.out (f i)
this : Inhabited ((i : ι) → Quotient.out (g i))
G : (i : ι) × Quotient.out (f i) → (i : ι) → Quotient.out (g i) :=
  invFun (⇑F : (a : (i : ι) → Quotient.out (g i)) → (i : ι) × Quotient.out (f i))
sG : Surjective G
i : ι
h :
  ∀ (x : Quotient.out (g i)),
    ∃ (x_1 : Quotient.out (f i)), G (Sigma.mk (β := fun (i : ι) ↦ Quotient.out (f i)) i x_1) i = x
⊢ #(Quotient.out (g i)) ≤ #(Quotient.out (f i))

Tactic:
exact ⟨Embedding.ofSurjective _ h⟩
-- Module: Mathlib.SetTheory.Cardinal.Order
Goal:
ι : Type u_1
f g : ι → Cardinal.{u_2}
H : ∀ (i : ι), f i < g i
h : prod g ≤ sum f
F : ((i : ι) → Quotient.out (g i)) ↪ (i : ι) × Quotient.out (f i)
this : Inhabited ((i : ι) → Quotient.out (g i))
G : (i : ι) × Quotient.out (f i) → (i : ι) → Quotient.out (g i) :=
  invFun (⇑F : (a : (i : ι) → Quotient.out (g i)) → (i : ι) × Quotient.out (f i))
sG : Surjective G
choose :
  ∀ (C : (i : ι) → Quotient.out (g i))
    (hc : ∀ (i : ι) (a : Quotient.out (f i)), G (Sigma.mk (β := fun (i : ι) ↦ Quotient.out (f i)) i a) i ≠ C i), False
⊢ False

Tactic:
choose C hc using
      show ∀ i, ∃ b, ∀ a, G ⟨i, a⟩ i ≠ b by
        intro i
        simp only [not_exists.symm, not_forall.symm]
        refine fun h => (H i).not_ge ?_
        rw [← mk_out (f i), ← mk_out (g i)]
        exact ⟨Embedding.ofSurjective _ h⟩
-- Module: Mathlib.SetTheory.Cardinal.Order
Goal:
ι : Type u_1
f g : ι → Cardinal.{u_2}
H : ∀ (i : ι), f i < g i
h : prod g ≤ sum f
F : ((i : ι) → Quotient.out (g i)) ↪ (i : ι) × Quotient.out (f i)
this : Inhabited ((i : ι) → Quotient.out (g i))
G : (i : ι) × Quotient.out (f i) → (i : ι) → Quotient.out (g i) :=
  invFun (⇑F : (a : (i : ι) → Quotient.out (g i)) → (i : ι) × Quotient.out (f i))
sG : Surjective G
C : (i : ι) → Quotient.out (g i)
hc : ∀ (i : ι) (a : Quotient.out (f i)), G (Sigma.mk (β := fun (i : ι) ↦ Quotient.out (f i)) i a) i ≠ C i
let : ∀ (i : ι) (a : Quotient.out (f i)) (h : G (Sigma.mk (β := fun (i : ι) ↦ Quotient.out (f i)) i a) = C), False
⊢ False

Tactic:
let ⟨⟨i, a⟩, h⟩ := sG C
-- Module: Mathlib.SetTheory.Cardinal.Order
Goal:
ι : Type u_1
f g : ι → Cardinal.{u_2}
H : ∀ (i : ι), f i < g i
h_1 : prod g ≤ sum f
F : ((i : ι) → Quotient.out (g i)) ↪ (i : ι) × Quotient.out (f i)
this : Inhabited ((i : ι) → Quotient.out (g i))
G : (i : ι) × Quotient.out (f i) → (i : ι) → Quotient.out (g i) :=
  invFun (⇑F : (a : (i : ι) → Quotient.out (g i)) → (i : ι) × Quotient.out (f i))
sG : Surjective G
C : (i : ι) → Quotient.out (g i)
hc : ∀ (i : ι) (a : Quotient.out (f i)), G (Sigma.mk (β := fun (i : ι) ↦ Quotient.out (f i)) i a) i ≠ C i
i : ι
a : Quotient.out (f i)
h : G (Sigma.mk (β := fun (i : ι) ↦ Quotient.out (f i)) i a) = C
⊢ False

Tactic:
hc i a (congr_fun h _)

Premises used: congr_fun
-- Module: Mathlib.SetTheory.Cardinal.Order
Goal:
ι : Type u_1
f g : ι → Cardinal.{u_2}
H : ∀ (i : ι), f i < g i
h_1 : prod g ≤ sum f
F : ((i : ι) → Quotient.out (g i)) ↪ (i : ι) × Quotient.out (f i)
this : Inhabited ((i : ι) → Quotient.out (g i))
G : (i : ι) × Quotient.out (f i) → (i : ι) → Quotient.out (g i) :=
  invFun (⇑F : (a : (i : ι) → Quotient.out (g i)) → (i : ι) × Quotient.out (f i))
sG : Surjective G
C : (i : ι) → Quotient.out (g i)
hc : ∀ (i : ι) (a : Quotient.out (f i)), G (Sigma.mk (β := fun (i : ι) ↦ Quotient.out (f i)) i a) i ≠ C i
i : ι
a : Quotient.out (f i)
h : G (Sigma.mk (β := fun (i : ι) ↦ Quotient.out (f i)) i a) = C
⊢ False

Tactic:
exact hc i a (congr_fun h _)

Premises used: congr_fun
-- Module: Mathlib.SetTheory.Cardinal.Order
Goal:
ι : Type u_1
f g : ι → Cardinal.{u_2}
H : ∀ (i : ι), f i ≤ g i
i : ι
this : f i ≤ g i
rwa : ∀ (this : #(Quotient.out (f i)) ≤ g i), Nonempty.{u_2 + 1} (Quotient.out (f i) ↪ Quotient.out (g i))
rwa₁ rwa₂ rwa₃ rwa₄ :
  ∀ (this : #(Quotient.out (f i)) ≤ #(Quotient.out (g i))), Nonempty.{u_2 + 1} (Quotient.out (f i) ↪ Quotient.out (g i))
⊢ Nonempty.{u_2 + 1} (Quotient.out (f i) ↪ Quotient.out (g i))

Tactic:
rwa [← mk_out (f i), ← mk_out (g i)] at this

Premises used: Cardinal.mk_out
-- Module: Mathlib.SetTheory.Cardinal.Order
Goal:
⊢ 0 < ℵ₀

Tactic:
pos_iff_ne_zero.2 aleph0_ne_zero

Premises used: Iff.mpr, pos_iff_ne_zero, Cardinal.aleph0_ne_zero
-- Module: Mathlib.SetTheory.Cardinal.Order
Goal:
c : Cardinal.{u}
⊢ ℵ₀ ≤ lift.{v, u} c ↔ ℵ₀ ≤ c

Tactic:
simpa using lift_le (a := ℵ₀)

Premises used: Cardinal.lift_le
-- Module: Mathlib.SetTheory.Cardinal.Order
Goal:
c : Cardinal.{u}
⊢ lift.{v, u} c ≤ ℵ₀ ↔ c ≤ ℵ₀

Tactic:
simpa using lift_le (b := ℵ₀)

Premises used: Cardinal.lift_le
-- Module: Mathlib.SetTheory.Cardinal.Order
Goal:
c : Cardinal.{u}
⊢ ℵ₀ < lift.{v, u} c ↔ ℵ₀ < c

Tactic:
simpa using lift_lt (a := ℵ₀)

Premises used: Cardinal.lift_lt
-- Module: Mathlib.SetTheory.Cardinal.Order
Goal:
c : Cardinal.{u}
⊢ lift.{v, u} c < ℵ₀ ↔ c < ℵ₀

Tactic:
simpa using lift_lt (b := ℵ₀)

Premises used: Cardinal.lift_lt
-- Module: Mathlib.SetTheory.Cardinal.Order
Goal:
c : Cardinal.{u}
⊢ ℵ₀ = lift.{v, u} c ↔ ℵ₀ = c

Tactic:
simpa using lift_inj (a := ℵ₀)

Premises used: Cardinal.lift_inj
-- Module: Mathlib.SetTheory.Cardinal.Order
Goal:
c : Cardinal.{u}
⊢ lift.{v, u} c = ℵ₀ ↔ c = ℵ₀

Tactic:
simp [eqComm]

Premises used: eqComm
-- Module: Mathlib.SetTheory.Cardinal.Order
Goal:
n : ℕ
⊢ #(Fin n) = (↑n : Cardinal.{0})

Tactic:
simp
-- Module: Mathlib.SetTheory.Cardinal.Order
Goal:
n : ℕ
zero : lift.{u, v} (↑0 : Cardinal.{v}) = (↑0 : Cardinal.{max v u})
succ :
  ∀ (n : ℕ),
    lift.{u, v} (↑n : Cardinal.{v}) = (↑n : Cardinal.{max v u}) →
      lift.{u, v} (↑(n + 1) : Cardinal.{v}) = (↑(n + 1) : Cardinal.{max v u})
⊢ lift.{u, v} (↑n : Cardinal.{v}) = (↑n : Cardinal.{max v u})

Tactic:
induction n
-- Module: Mathlib.SetTheory.Cardinal.Order
Goal:
⊢ lift.{u, v} (↑0 : Cardinal.{v}) = (↑0 : Cardinal.{max v u})

Tactic:
simp [*]
-- Module: Mathlib.SetTheory.Cardinal.Order
Goal:
n : ℕ
h : lift.{u, v} (↑n : Cardinal.{v}) = (↑n : Cardinal.{max v u})
⊢ lift.{u, v} (↑(n + 1) : Cardinal.{v}) = (↑(n + 1) : Cardinal.{max v u})

Tactic:
simp [*]
-- Module: Mathlib.SetTheory.Cardinal.Order
Goal:
n : ℕ
inst : n.AtLeastTwo
⊢ lift.{u, v} (OfNat.ofNat n) = OfNat.ofNat n

Tactic:
lift_natCast n

Premises used: Cardinal.lift_natCast
-- Module: Mathlib.SetTheory.Cardinal.Order
Goal:
a : Cardinal.{u}
n : ℕ
⊢ lift.{v, u} a = (↑n : Cardinal.{max u v}) ↔ a = (↑n : Cardinal.{u})

Tactic:
lift_injective.eq_iff' (lift_natCast n)

Premises used: Function.Injective.eq_iff', Cardinal.lift_natCast, Cardinal.lift_injective
-- Module: Mathlib.SetTheory.Cardinal.Order
Goal:
a : Cardinal.{u}
n : ℕ
inst : n.AtLeastTwo
⊢ lift.{v, u} a = OfNat.ofNat n ↔ a = OfNat.ofNat n

Tactic:
lift_eq_nat_iff

Premises used: Cardinal.lift_eq_nat_iff
-- Module: Mathlib.SetTheory.Cardinal.Order
Goal:
n : ℕ
a : Cardinal.{u}
rw : lift.{v, u} (↑n : Cardinal.{u}) = lift.{v, u} a ↔ (↑n : Cardinal.{u}) = a
rw₁ rw₂ : (↑n : Cardinal.{u}) = a ↔ (↑n : Cardinal.{u}) = a
⊢ (↑n : Cardinal.{max u v}) = lift.{v, u} a ↔ (↑n : Cardinal.{u}) = a

Tactic:
rw [← lift_natCast.{v, u} n, lift_inj]

Premises used: Cardinal.lift_inj
-- Module: Mathlib.SetTheory.Cardinal.Order
Goal:
a : Cardinal.{u}
⊢ 0 = lift.{v, u} a ↔ 0 = a

Tactic:
simp [eqComm]

Premises used: eqComm
-- Module: Mathlib.SetTheory.Cardinal.Order
Goal:
a : Cardinal.{u}
⊢ 1 = lift.{v, u} a ↔ 1 = a

Tactic:
simp [eqComm]

Premises used: eqComm
-- Module: Mathlib.SetTheory.Cardinal.Order
Goal:
a : Cardinal.{u}
n : ℕ
inst : n.AtLeastTwo
⊢ OfNat.ofNat n = lift.{v, u} a ↔ OfNat.ofNat n = a

Tactic:
nat_eq_lift_iff

Premises used: Cardinal.nat_eq_lift_iff
-- Module: Mathlib.SetTheory.Cardinal.Order
Goal:
a : Cardinal.{u}
n : ℕ
rw : lift.{v, u} a ≤ lift.{v, u} (↑n : Cardinal.{u}) ↔ a ≤ (↑n : Cardinal.{u})
rw₁ rw₂ : a ≤ (↑n : Cardinal.{u}) ↔ a ≤ (↑n : Cardinal.{u})
⊢ lift.{v, u} a ≤ (↑n : Cardinal.{max u v}) ↔ a ≤ (↑n : Cardinal.{u})

Tactic:
rw [← lift_natCast.{v, u}, lift_le]

Premises used: Cardinal.lift_le
-- Module: Mathlib.SetTheory.Cardinal.Order
Goal:
a : Cardinal.{u}
⊢ lift.{v, u} a ≤ 1 ↔ a ≤ 1

Tactic:
simpa using lift_le_nat_iff (n := 1)

Premises used: Cardinal.lift_le_nat_iff
-- Module: Mathlib.SetTheory.Cardinal.Order
Goal:
a : Cardinal.{u}
n : ℕ
inst : n.AtLeastTwo
⊢ lift.{v, u} a ≤ OfNat.ofNat n ↔ a ≤ OfNat.ofNat n

Tactic:
lift_le_nat_iff

Premises used: Cardinal.lift_le_nat_iff
-- Module: Mathlib.SetTheory.Cardinal.Order
Goal:
n : ℕ
a : Cardinal.{u}
rw : lift.{v, u} (↑n : Cardinal.{u}) ≤ lift.{v, u} a ↔ (↑n : Cardinal.{u}) ≤ a
rw₁ rw₂ : (↑n : Cardinal.{u}) ≤ a ↔ (↑n : Cardinal.{u}) ≤ a
⊢ (↑n : Cardinal.{max u v}) ≤ lift.{v, u} a ↔ (↑n : Cardinal.{u}) ≤ a

Tactic:
rw [← lift_natCast.{v, u}, lift_le]

Premises used: Cardinal.lift_le
-- Module: Mathlib.SetTheory.Cardinal.Order
Goal:
a : Cardinal.{u}
⊢ 1 ≤ lift.{v, u} a ↔ 1 ≤ a

Tactic:
simpa using nat_le_lift_iff (n := 1)

Premises used: Cardinal.nat_le_lift_iff
-- Module: Mathlib.SetTheory.Cardinal.Order
Goal:
a : Cardinal.{u}
n : ℕ
inst : n.AtLeastTwo
⊢ OfNat.ofNat n ≤ lift.{v, u} a ↔ OfNat.ofNat n ≤ a

Tactic:
nat_le_lift_iff

Premises used: Cardinal.nat_le_lift_iff
-- Module: Mathlib.SetTheory.Cardinal.Order
Goal:
a : Cardinal.{u}
n : ℕ
rw : lift.{v, u} a < lift.{v, u} (↑n : Cardinal.{u}) ↔ a < (↑n : Cardinal.{u})
rw₁ rw₂ : a < (↑n : Cardinal.{u}) ↔ a < (↑n : Cardinal.{u})
⊢ lift.{v, u} a < (↑n : Cardinal.{max u v}) ↔ a < (↑n : Cardinal.{u})

Tactic:
rw [← lift_natCast.{v, u}, lift_lt]

Premises used: Cardinal.lift_lt
-- Module: Mathlib.SetTheory.Cardinal.Order
Goal:
a : Cardinal.{u}
n : ℕ
inst : n.AtLeastTwo
⊢ lift.{v, u} a < OfNat.ofNat n ↔ a < OfNat.ofNat n

Tactic:
lift_lt_nat_iff

Premises used: Cardinal.lift_lt_nat_iff