awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Order (hypothesis)
Goal:
a : Cardinal.{u}
h : ¬Acc (fun (x1 x2 : Cardinal.{u}) ↦ x1 < x2) a
ι : Type (max 0 (u + 1)) := { c : Cardinal.{u} // ¬Acc (fun (x1 x2 : Cardinal.{u}) ↦ x1 < x2) c }
f : ι → Cardinal.{u} := Subtype.val (p := fun (c : Cardinal.{u}) ↦ ¬Acc (fun (x1 x2 : Cardinal.{u}) ↦ x1 < x2) c)
hι : Nonempty ι
c : Cardinal.{u}
hc : ¬Acc (fun (x1 x2 : Cardinal.{u}) ↦ x1 < x2) c
h_1 :
  (j : ι) →
    Quotient.out (f (Subtype.mk (p := fun (c : Cardinal.{u}) ↦ ¬Acc (fun (x1 x2 : Cardinal.{u}) ↦ x1 < x2) c) c hc)) ↪
      Quotient.out (f j)
j : Cardinal.{u}
h' : j < c
hj : ¬Acc (fun (x1 x2 : Cardinal.{u}) ↦ x1 < x2) j
⊢ c ≤ j
have this : #(Quotient.out (f (Subtype.mk (p := fun (c : Cardinal.{u}) ↦ ¬Acc (fun (x1 x2 : Cardinal.{u}) ↦ x1 < x2) c) c hc))) ≤
  #(Quotient.out (f (Subtype.mk (p := fun (c : Cardinal.{u}) ↦ ¬Acc (fun (x1 x2 : Cardinal.{u}) ↦ x1 < x2) c) j hj)))
Tactic: have : #_ ≤ #_ := ⟨h_1 ⟨j, hj⟩⟩
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Order (goal)
Goal:
a b : Cardinal.{u_1}
h : a < b
⊢ a + 1 ≤ b
have mk : ∀ (α β : Type u_1) (h : #α < #β), #α + 1 ≤ #β
Tactic: induction a, b using Cardinal.inductionOn₂ with | mk α β
Cleared hypotheses: a, b, h
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Order (goal)
Goal:
α β : Type u_1
h : #α < #β
⊢ #α + 1 ≤ #β
have mk : ∀ (f : α ↪ β), #α + 1 ≤ #β
Tactic: obtain ⟨f⟩ := h.le
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Order (hypothesis)
Goal:
α β : Type u_1
h : #α < #β
f : α ↪ β
⊢ #α + 1 ≤ #β
have hf : ¬Surjective (α := α) (β := β) (⇑f : (a : α) → β)
Tactic: have hf : ¬Surjective f := fun hn ↦ h.not_ge (mk_le_of_surjective hn)
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Order (hypothesis)
Goal:
α β : Type u_1
h : #α < #β
f : α ↪ β
hf : ¬Surjective (α := α) (β := β) (⇑f : (a : α) → β)
⊢ #α + 1 ≤ #β
have hf₁ : ∃ (x : β), ¬∃ (a : α), (f : (a : α) → β) a = x
Tactic: rw [Surjective, not_forall] at hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Order (goal)
Goal:
α β : Type u_1
h : #α < #β
f : α ↪ β
hf : ∃ (x : β), ¬∃ (a : α), (f : (a : α) → β) a = x
⊢ #α + 1 ≤ #β
have mk : ∀ (b : β) (hb : ¬∃ (a : α), (f : (a : α) → β) a = b), #α + 1 ≤ #β
Tactic: obtain ⟨b, hb⟩ := hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Order (goal)
Goal:
α β : Type u_1
h : #α < #β
f : α ↪ β
b : β
hb : ¬∃ (a : α), (f : (a : α) → β) a = b
⊢ #α + 1 ≤ #β
have mk : #(Option α) ≤ #β
Tactic: rw [← mk_option]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Order (goal)
Goal:
a : Cardinal.{u}
⊢ lift.{v, u} (succ a) = succ (lift.{v, u} a)
have apply : lift.{v, u} (succ a) ≤ succ (lift.{v, u} a)
Tactic: apply (succ_le_of_lt <| lift_lt.2 <| lt_succ a).antisymm'
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Order (goal)
Goal:
a : Cardinal.{u}
⊢ lift.{v, u} (succ a) ≤ succ (lift.{v, u} a)
have by_contra! : ∀ (h : succ (lift.{v, u} a) < lift.{v, u} (succ a)), False
Tactic: by_contra! h
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Order (goal)
Goal:
a : Cardinal.{u}
h : succ (lift.{v, u} a) < lift.{v, u} (succ a)
⊢ False
have rcases : ∀ (b : Cardinal.{u}) (h : b < succ a) (hb : lift.{v, u} b = succ (lift.{v, u} a)), False
Tactic: rcases lt_lift_iff.1 h with ⟨b, h, hb⟩
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Order (hypothesis)
Goal:
a : Cardinal.{u}
h_1 : succ (lift.{v, u} a) < lift.{v, u} (succ a)
b : Cardinal.{u}
h : b < succ a
hb : lift.{v, u} b = succ (lift.{v, u} a)
⊢ False
have h₁ : succ (lift.{v, u} a) ≤ lift.{v, u} a
Tactic: rw [lt_succ_iff, ← lift_le, hb] at h
Cleared hypotheses: h, hb
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Order (goal)
Goal:
c : Cardinal.{u_1}
hc : c.IsStrongLimit
⊢ IsSuccLimit c
have rw : c ≠ 0 ∧ IsSuccPrelimit c
Tactic: rw [Cardinal.isSuccLimit_iff]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Order (goal)
Goal:
ι : Type u
f : ι → Cardinal.{v}
i : ι
⊢ lift.{u, v} (f i) ≤ sum f
have rw : lift.{u, v} ⟦Quotient.out (f i)⟧ ≤ sum f
Tactic: rw [← Quotient.out_eq (f i)]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Order (hypothesis)
Goal:
ι : Type u_1
f g : ι → Cardinal.{u_2}
⊢ sum (f + g) = sum f + sum g
have this : #((i : ι) × ((Quotient.out ∘ f) i ⊕ (Quotient.out ∘ g) i)) =
  #((i : ι) × (Quotient.out ∘ f) i ⊕ (i : ι) × (Quotient.out ∘ g) i)
Tactic: have := mk_congr (Equiv.sigmaSumDistrib (Quotient.out ∘ f) (Quotient.out ∘ g))
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Order (hypothesis)
Goal:
ι : Type u_1
f g : ι → Cardinal.{u_2}
this :
  #((i : ι) × ((Quotient.out ∘ f) i ⊕ (Quotient.out ∘ g) i)) =
    #((i : ι) × (Quotient.out ∘ f) i ⊕ (i : ι) × (Quotient.out ∘ g) i)
⊢ sum (f + g) = sum f + sum g
have 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
Tactic: simp only [comp_apply, mk_sigma, mk_sum, mk_out, lift_id] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Order (hypothesis)
Goal:
ι : Type u_1
f g : ι → Cardinal.{u_2}
H : ∀ (i : ι), f i ≤ g i
i : ι
⊢ Nonempty.{u_2 + 1} (Quotient.out (f i) ↪ Quotient.out (g ((Embedding.refl ι : (a : ι) → ι) i)))
have this : f i ≤ g i
Tactic: have := H i
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Order (goal)
Goal:
ι : Type u_1
f g : ι → Cardinal.{u_2}
H : ∀ (i : ι), f i ≤ g i
i : ι
this : f i ≤ g i
⊢ Nonempty.{u_2 + 1} (Quotient.out (f i) ↪ Quotient.out (g ((Embedding.refl ι : (a : ι) → ι) i)))
have 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)))
Tactic: rwa [← Quot.out_eq (f i), ← Quot.out_eq (g i)] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Order (goal)
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)))
⊢ Nonempty.{u_2 + 1} (Quotient.out (f i) ↪ Quotient.out (g ((Embedding.refl ι : (a : ι) → ι) i)))
have 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)))
Tactic: rwa [← Quot.out_eq (f i), ← Quot.out_eq (g i)] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Order (goal)
Goal:
α : Type u
β : Type v
c : Cardinal.{max u v}
f : α → β
hf : ∀ (b : β), lift.{v, u} #(↑(f ⁻¹' {b}) : Type u) ≤ c
b : β
⊢ (↑(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)
have 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)
Tactic: rw [Equiv.image_eq_preimage_symm]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Order (goal)
Goal:
α : Type u
β : Type v
c : Cardinal.{max u v}
f : α → β
hf : ∀ (b : β), lift.{v, u} #(↑(f ⁻¹' {b}) : Type u) ≤ c
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)
have simp : { x : α // f (ULift.down.{v, u} ((Equiv.symm Equiv.ulift : (a : α) → ULift.{v, u} α) x)) = b } ≃ { x : α // f x = b }
Tactic: simp only [preimage, mem_singleton_iff, ULift.up_inj, mem_setOf_eq, coe_setOf]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Order (goal)
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 < g x
have rw : Cardinal.sum g < HPow.hPow (α := Cardinal.{u}) 2 (Cardinal.sum g)
Tactic: rw [hx]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Order (goal)
Goal:
ι : Type u
f : ι → Cardinal.{v}
ω : Cardinal.{v}
hω : ¬IsSuccPrelimit ω
h : ⨆ (i : ι), f i = ω
⊢ ∃ (i : ι), f i = ω
have subst : ∀ (hω : ¬IsSuccPrelimit.{v + 1} (α := Cardinal.{v}) (⨆ (i : ι), f i)), ∃ (i : ι), f i = ⨆ (i : ι), f i
Tactic: subst h
Cleared hypotheses: ω, hω, h
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Order (goal)
Goal:
ι : Type u
hι : Nonempty ι
f : ι → Cardinal.{v}
hf : BddAbove (Set.range f)
c : Cardinal.{v}
hc : ¬IsSuccLimit c
h : ⨆ (i : ι), f i = c
⊢ ∃ (i : ι), f i = c
have subst : ∀ (hc : ¬IsSuccLimit.{v + 1} (α := Cardinal.{v}) (⨆ (i : ι), f i)), ∃ (i : ι), f i = ⨆ (i : ι), f i
Tactic: subst h
Cleared hypotheses: c, hc, h
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Order (goal)
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)
⊢ Inhabited ((i : ι) → Quotient.out (g i))
have refine : ∀ (i : ι), #(Quotient.out (g i)) ≠ 0
Tactic: refine ⟨fun i => Classical.choice <| mk_ne_zero_iff.1 ?_⟩
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Order (goal)
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 : ι
⊢ #(Quotient.out (g i)) ≠ 0
have rw : g i ≠ 0
Tactic: rw [mk_out]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Order (goal)
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)
⊢ False
have have : ∀ (this : Inhabited ((i : ι) → Quotient.out (g i))), 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
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Order (hypothesis)
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))
⊢ False
have sG : Surjective G
Tactic: have sG : Surjective G := invFun_surjective F.2
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Order (goal)
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 : ι
⊢ ∃ (b : Quotient.out (g i)), ∀ (a : Quotient.out (f i)), G (Sigma.mk (β := fun (i : ι) ↦ Quotient.out (f i)) i a) i ≠ b
have 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
Tactic: simp only [not_exists.symm, not_forall.symm]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Order (goal)
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
have 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
Tactic: refine fun h => (H i).not_ge ?_
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Order (goal)
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
⊢ g i ≤ f i
have rw : #(Quotient.out (g i)) ≤ #(Quotient.out (f i))
Tactic: rw [← mk_out (f i), ← mk_out (g i)]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Order (goal)
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
⊢ False
have 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
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⟩
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Order (goal)
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
⊢ False
have let : ∀ (i : ι) (a : Quotient.out (f i)) (h : G (Sigma.mk (β := fun (i : ι) ↦ Quotient.out (f i)) i a) = C), False
Tactic: let ⟨⟨i, a⟩, h⟩ := sG C
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Order (hypothesis)
Goal:
ι : Type u_1
f g : ι → Cardinal.{u_2}
H : ∀ (i : ι), f i ≤ g i
i : ι
⊢ Nonempty.{u_2 + 1} (Quotient.out (f i) ↪ Quotient.out (g i))
have this : f i ≤ g i
Tactic: have := H i
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Order (goal)
Goal:
ι : Type u_1
f g : ι → Cardinal.{u_2}
H : ∀ (i : ι), f i ≤ g i
i : ι
this : f i ≤ g i
⊢ Nonempty.{u_2 + 1} (Quotient.out (f i) ↪ Quotient.out (g i))
have rwa : ∀ (this : #(Quotient.out (f i)) ≤ 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
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Order (goal)
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))
⊢ Nonempty.{u_2 + 1} (Quotient.out (f i) ↪ Quotient.out (g i))
have rwa₁ : ∀ (this : #(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
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Order (goal)
Goal:
n : ℕ
⊢ lift.{u, v} (↑n : Cardinal.{v}) = (↑n : Cardinal.{max v u})
have zero : lift.{u, v} (↑0 : Cardinal.{v}) = (↑0 : Cardinal.{max v u})
Tactic: induction n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Order (goal)
Goal:
n : ℕ
zero : lift.{u, v} (↑0 : Cardinal.{v}) = (↑0 : Cardinal.{max v u})
⊢ lift.{u, v} (↑n : Cardinal.{v}) = (↑n : Cardinal.{max v u})
have 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})
Tactic: induction n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Order (goal)
Goal:
n : ℕ
a : Cardinal.{u}
⊢ (↑n : Cardinal.{max u v}) = lift.{v, u} a ↔ (↑n : Cardinal.{u}) = a
have rw : lift.{v, u} (↑n : Cardinal.{u}) = lift.{v, u} a ↔ (↑n : Cardinal.{u}) = a
Tactic: rw [← lift_natCast.{v, u} n, lift_inj]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Order (goal)
Goal:
n : ℕ
a : Cardinal.{u}
rw : lift.{v, u} (↑n : Cardinal.{u}) = lift.{v, u} a ↔ (↑n : Cardinal.{u}) = a
⊢ (↑n : Cardinal.{max u v}) = lift.{v, u} a ↔ (↑n : Cardinal.{u}) = a
have rw₁ : (↑n : Cardinal.{u}) = a ↔ (↑n : Cardinal.{u}) = a
Tactic: rw [← lift_natCast.{v, u} n, lift_inj]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Order (goal)
Goal:
a : Cardinal.{u}
n : ℕ
⊢ lift.{v, u} a ≤ (↑n : Cardinal.{max u v}) ↔ a ≤ (↑n : Cardinal.{u})
have rw : lift.{v, u} a ≤ lift.{v, u} (↑n : Cardinal.{u}) ↔ a ≤ (↑n : Cardinal.{u})
Tactic: rw [← lift_natCast.{v, u}, lift_le]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Order (goal)
Goal:
a : Cardinal.{u}
n : ℕ
rw : lift.{v, u} a ≤ lift.{v, u} (↑n : Cardinal.{u}) ↔ a ≤ (↑n : Cardinal.{u})
⊢ lift.{v, u} a ≤ (↑n : Cardinal.{max u v}) ↔ a ≤ (↑n : Cardinal.{u})
have rw₁ : a ≤ (↑n : Cardinal.{u}) ↔ a ≤ (↑n : Cardinal.{u})
Tactic: rw [← lift_natCast.{v, u}, lift_le]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Order (goal)
Goal:
n : ℕ
a : Cardinal.{u}
⊢ (↑n : Cardinal.{max u v}) ≤ lift.{v, u} a ↔ (↑n : Cardinal.{u}) ≤ a
have rw : lift.{v, u} (↑n : Cardinal.{u}) ≤ lift.{v, u} a ↔ (↑n : Cardinal.{u}) ≤ a
Tactic: rw [← lift_natCast.{v, u}, lift_le]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Order (goal)
Goal:
n : ℕ
a : Cardinal.{u}
rw : lift.{v, u} (↑n : Cardinal.{u}) ≤ lift.{v, u} a ↔ (↑n : Cardinal.{u}) ≤ a
⊢ (↑n : Cardinal.{max u v}) ≤ lift.{v, u} a ↔ (↑n : Cardinal.{u}) ≤ a
have rw₁ : (↑n : Cardinal.{u}) ≤ a ↔ (↑n : Cardinal.{u}) ≤ a
Tactic: rw [← lift_natCast.{v, u}, lift_le]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Order (goal)
Goal:
a : Cardinal.{u}
n : ℕ
⊢ lift.{v, u} a < (↑n : Cardinal.{max u v}) ↔ a < (↑n : Cardinal.{u})
have rw : lift.{v, u} a < lift.{v, u} (↑n : Cardinal.{u}) ↔ a < (↑n : Cardinal.{u})
Tactic: rw [← lift_natCast.{v, u}, lift_lt]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Order (goal)
Goal:
a : Cardinal.{u}
n : ℕ
rw : lift.{v, u} a < lift.{v, u} (↑n : Cardinal.{u}) ↔ a < (↑n : Cardinal.{u})
⊢ lift.{v, u} a < (↑n : Cardinal.{max u v}) ↔ a < (↑n : Cardinal.{u})
have rw₁ : a < (↑n : Cardinal.{u}) ↔ a < (↑n : Cardinal.{u})
Tactic: rw [← lift_natCast.{v, u}, lift_lt]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Order (goal)
Goal:
n : ℕ
a : Cardinal.{u}
⊢ (↑n : Cardinal.{max u v}) < lift.{v, u} a ↔ (↑n : Cardinal.{u}) < a
have rw : lift.{v, u} (↑n : Cardinal.{u}) < lift.{v, u} a ↔ (↑n : Cardinal.{u}) < a
Tactic: rw [← lift_natCast.{v, u}, lift_lt]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Order (goal)
Goal:
n : ℕ
a : Cardinal.{u}
rw : lift.{v, u} (↑n : Cardinal.{u}) < lift.{v, u} a ↔ (↑n : Cardinal.{u}) < a
⊢ (↑n : Cardinal.{max u v}) < lift.{v, u} a ↔ (↑n : Cardinal.{u}) < a
have rw₁ : (↑n : Cardinal.{u}) < a ↔ (↑n : Cardinal.{u}) < a
Tactic: rw [← lift_natCast.{v, u}, lift_lt]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Order (goal)
Goal:
α β : Type u
⊢ CharZero Cardinal.{u_1}
have refine : ∀ (a b : ℕ) (h : Eq.{u_1 + 2} (α := Cardinal.{u_1}) (↑a : Cardinal.{u_1}) (↑b : Cardinal.{u_1})), a = b
Tactic: refine ⟨fun a b h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Order (goal)
Goal:
α β : Type u
a b : ℕ
h : Eq.{u_1 + 2} (α := Cardinal.{u_1}) (↑a : Cardinal.{u_1}) (↑b : Cardinal.{u_1})
⊢ a = b
have rwa : ∀ (h : lift.{u_1, 0} #(Fin a) = (↑b : Cardinal.{u_1})), a = b
Tactic: rwa [← lift_mk_fin, ← lift_mk_fin, lift_inj, Cardinal.eq, ← Fintype.card_eq,
    Fintype.card_fin, Fintype.card_fin] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Order (goal)
Goal:
α β : Type u
a b : ℕ
h : Eq.{u_1 + 2} (α := Cardinal.{u_1}) (↑a : Cardinal.{u_1}) (↑b : Cardinal.{u_1})
rwa : ∀ (h : lift.{u_1, 0} #(Fin a) = (↑b : Cardinal.{u_1})), a = b
⊢ a = b
have rwa₁ : ∀ (h : lift.{u_1, 0} #(Fin a) = lift.{u_1, 0} #(Fin b)), a = b
Tactic: rwa [← lift_mk_fin, ← lift_mk_fin, lift_inj, Cardinal.eq, ← Fintype.card_eq,
    Fintype.card_fin, Fintype.card_fin] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Order (goal)
Goal:
α β : Type u
a b : ℕ
h : Eq.{u_1 + 2} (α := Cardinal.{u_1}) (↑a : Cardinal.{u_1}) (↑b : Cardinal.{u_1})
rwa : ∀ (h : lift.{u_1, 0} #(Fin a) = (↑b : Cardinal.{u_1})), a = b
rwa₁ : ∀ (h : lift.{u_1, 0} #(Fin a) = lift.{u_1, 0} #(Fin b)), a = b
⊢ a = b
have rwa₂ : ∀ (h : #(Fin a) = #(Fin b)), a = b
Tactic: rwa [← lift_mk_fin, ← lift_mk_fin, lift_inj, Cardinal.eq, ← Fintype.card_eq,
    Fintype.card_fin, Fintype.card_fin] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Order (goal)
Goal:
α β : Type u
a b : ℕ
h : Eq.{u_1 + 2} (α := Cardinal.{u_1}) (↑a : Cardinal.{u_1}) (↑b : Cardinal.{u_1})
rwa : ∀ (h : lift.{u_1, 0} #(Fin a) = (↑b : Cardinal.{u_1})), a = b
rwa₁ : ∀ (h : lift.{u_1, 0} #(Fin a) = lift.{u_1, 0} #(Fin b)), a = b
rwa₂ : ∀ (h : #(Fin a) = #(Fin b)), a = b
⊢ a = b
have rwa₃ : ∀ (h : Nonempty (Fin a ≃ Fin b)), a = b
Tactic: rwa [← lift_mk_fin, ← lift_mk_fin, lift_inj, Cardinal.eq, ← Fintype.card_eq,
    Fintype.card_fin, Fintype.card_fin] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Order (goal)
Goal:
α β : Type u
a b : ℕ
h : Eq.{u_1 + 2} (α := Cardinal.{u_1}) (↑a : Cardinal.{u_1}) (↑b : Cardinal.{u_1})
rwa : ∀ (h : lift.{u_1, 0} #(Fin a) = (↑b : Cardinal.{u_1})), a = b
rwa₁ : ∀ (h : lift.{u_1, 0} #(Fin a) = lift.{u_1, 0} #(Fin b)), a = b
rwa₂ : ∀ (h : #(Fin a) = #(Fin b)), a = b
rwa₃ : ∀ (h : Nonempty (Fin a ≃ Fin b)), a = b
⊢ a = b
have rwa₄ : ∀ (h : Fintype.card (Fin a) = Fintype.card (Fin b)), a = b
Tactic: rwa [← lift_mk_fin, ← lift_mk_fin, lift_inj, Cardinal.eq, ← Fintype.card_eq,
    Fintype.card_fin, Fintype.card_fin] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Order (goal)
Goal:
α β : Type u
a b : ℕ
h : Eq.{u_1 + 2} (α := Cardinal.{u_1}) (↑a : Cardinal.{u_1}) (↑b : Cardinal.{u_1})
rwa : ∀ (h : lift.{u_1, 0} #(Fin a) = (↑b : Cardinal.{u_1})), a = b
rwa₁ : ∀ (h : lift.{u_1, 0} #(Fin a) = lift.{u_1, 0} #(Fin b)), a = b
rwa₂ : ∀ (h : #(Fin a) = #(Fin b)), a = b
rwa₃ : ∀ (h : Nonempty (Fin a ≃ Fin b)), a = b
rwa₄ : ∀ (h : Fintype.card (Fin a) = Fintype.card (Fin b)), a = b
⊢ a = b
have rwa₅ : ∀ (h : a = Fintype.card (Fin b)), a = b
Tactic: rwa [← lift_mk_fin, ← lift_mk_fin, lift_inj, Cardinal.eq, ← Fintype.card_eq,
    Fintype.card_fin, Fintype.card_fin] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Order (goal)
Goal:
α β : Type u
a b : ℕ
h : Eq.{u_1 + 2} (α := Cardinal.{u_1}) (↑a : Cardinal.{u_1}) (↑b : Cardinal.{u_1})
rwa : ∀ (h : lift.{u_1, 0} #(Fin a) = (↑b : Cardinal.{u_1})), a = b
rwa₁ : ∀ (h : lift.{u_1, 0} #(Fin a) = lift.{u_1, 0} #(Fin b)), a = b
rwa₂ : ∀ (h : #(Fin a) = #(Fin b)), a = b
rwa₃ : ∀ (h : Nonempty (Fin a ≃ Fin b)), a = b
rwa₄ : ∀ (h : Fintype.card (Fin a) = Fintype.card (Fin b)), a = b
rwa₅ : ∀ (h : a = Fintype.card (Fin b)), a = b
⊢ a = b
have rwa₆ : ∀ (h : a = b), a = b
Tactic: rwa [← lift_mk_fin, ← lift_mk_fin, lift_inj, Cardinal.eq, ← Fintype.card_eq,
    Fintype.card_fin, Fintype.card_fin] at h
Cleared hypotheses: h