awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.HasCardinalLT (hypothesis)
Goal:
ι : Type u
α : ι → Type v
κ : Cardinal.{w}
inst : Fact κ.IsRegular
hι : HasCardinalLT ι κ
hα : ∀ (i : ι), HasCardinalLT.{w, v} (α i) κ
⊢ HasCardinalLT ((i : ι) × α i) κ
have this : Fact (Cardinal.lift.{max u v, w} κ).IsRegular
Tactic: have : Fact (Cardinal.lift.{max u v} κ).IsRegular := ⟨Cardinal.IsRegular.lift Fact.out⟩
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.HasCardinalLT (hypothesis)
Goal:
ι : Type u
α : ι → Type v
κ : Cardinal.{w}
inst : Fact κ.IsRegular
hι : HasCardinalLT ι κ
hα : ∀ (i : ι), HasCardinalLT.{w, v} (α i) κ
this : Fact (Cardinal.lift.{max u v, w} κ).IsRegular
⊢ HasCardinalLT ((i : ι) × α i) κ
have this₁ : HasCardinalLT ((i : ULift.{max v w, u} ι) × (fun (i : ULift.{max v w, u} ι) ↦ ULift.{max u w, v} (α i.down)) i)
  (Cardinal.lift.{max u v, w} κ)
Tactic: have := hasCardinalLT_sigma'
    (fun (i : ULift.{max v w} ι) ↦ ULift.{max u w} (α (ULift.down i)))
    (Cardinal.lift.{max u v} κ) (by simpa)
    (fun i ↦ by simpa using hα (ULift.down i))
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.HasCardinalLT (hypothesis)
Goal:
ι : Type u
α : ι → Type v
κ : Cardinal.{w}
inst : Fact κ.IsRegular
hι : HasCardinalLT ι κ
hα : ∀ (i : ι), HasCardinalLT.{w, v} (α i) κ
this_1 : Fact (Cardinal.lift.{max u v, w} κ).IsRegular
this :
  HasCardinalLT ((i : ULift.{max v w, u} ι) × (fun (i : ULift.{max v w, u} ι) ↦ ULift.{max u w, v} (α i.down)) i)
    (Cardinal.lift.{max u v, w} κ)
⊢ HasCardinalLT ((i : ι) × α i) κ
have this₁ : HasCardinalLT ((i : ULift.{max v w, u} ι) × (fun (i : ULift.{max v w, u} ι) ↦ ULift.{max u w, v} (α i.down)) i) κ
Tactic: rw [hasCardinalLT_lift_iff] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.HasCardinalLT (goal)
Goal:
ι : Type u_1
X : Type u_2
P : ι → X → Prop
κ : Cardinal.{u_3}
inst : Fact κ.IsRegular
hι : HasCardinalLT ι κ
hP : ∀ (i : ι), HasCardinalLT.{u_3, u_2} (Subtype (P i)) κ
x_1 : (i : ι) × Subtype (P i)
i : ι
x : X
hx : P i x
⊢ (⨆ (i : ι), P i) x
have simp : ∃ (i : ι), P i x
Tactic: simp only [iSup_apply, iSup_Prop_eq]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.HasCardinalLT (hypothesis)
Goal:
ι : Type u_1
X : Type u_2
P : ι → X → Prop
κ : Cardinal.{u_3}
inst : Fact κ.IsRegular
hι : HasCardinalLT ι κ
hP : ∀ (i : ι), HasCardinalLT.{u_3, u_2} (Subtype (P i)) κ
val : X
h : (⨆ (i : ι), P i) val
⊢ ∃ (a : (i : ι) × Subtype (P i)),
    (fun (x : (i : ι) × Subtype (P i)) ↦
          (match (motive := (i : ι) × Subtype (P i) → Subtype (α := X) (⨆ (i : ι), P i)) x with
            | ⟨i, ⟨x, hx⟩⟩ => Subtype.mk (p := ⨆ (i : ι), P i) x ⋯ :
            Subtype (α := X) (⨆ (i : ι), P i)))
        a =
      Subtype.mk (p := ⨆ (i : ι), P i) val h
have h₁ : ∃ (i : ι), P i val
Tactic: simp only [iSup_apply, iSup_Prop_eq] at h
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.HasCardinalLT (goal)
Goal:
ι : Type u_1
X : Type u_2
P : ι → X → Prop
κ : Cardinal.{u_3}
inst : Fact κ.IsRegular
hι : HasCardinalLT ι κ
hP : ∀ (i : ι), HasCardinalLT.{u_3, u_2} (Subtype (P i)) κ
val : X
h_1 : (⨆ (i : ι), P i) val
h : ∃ (i : ι), P i val
⊢ ∃ (a : (i : ι) × Subtype (P i)),
    (fun (x : (i : ι) × Subtype (P i)) ↦
          (match (motive := (i : ι) × Subtype (P i) → Subtype (α := X) (⨆ (i : ι), P i)) x with
            | ⟨i, ⟨x, hx⟩⟩ => Subtype.mk (p := ⨆ (i : ι), P i) x ⋯ :
            Subtype (α := X) (⨆ (i : ι), P i)))
        a =
      Subtype.mk (p := ⨆ (i : ι), P i) val h_1
have obtain : ∀ (i : ι) (hi : P i val),
  ∃ (a : (i : ι) × Subtype (P i)),
    (fun (x : (i : ι) × Subtype (P i)) ↦
          (match (motive := (i : ι) × Subtype (P i) → Subtype (α := X) (⨆ (i : ι), P i)) x with
            | ⟨i, ⟨x, hx⟩⟩ => Subtype.mk (p := ⨆ (i : ι), P i) x sorry :
            Subtype (α := X) (⨆ (i : ι), P i)))
        a =
      Subtype.mk (p := ⨆ (i : ι), P i) val h_1
Tactic: obtain ⟨i, hi⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.HasCardinalLT (goal)
Goal:
ι : Type u_1
X : Type u_2
S : ι → Set X
κ : Cardinal.{u_3}
inst : Fact κ.IsRegular
hι : HasCardinalLT ι κ
hS : ∀ (i : ι), HasCardinalLT.{u_3, u_2} (↑(S i) : Type u_2) κ
⊢ HasCardinalLT.{u_3, u_2} (↑(⋃ (i : ι), S i) : Type u_2) κ
have h : Eq.{u_2 + 1} (α := Set X) (⋃ (i : ι), S i) (setOf (⨆ (i : ι), S i))
Tactic: convert! show HasCardinalLT (setOf ((⨆ i, S i))) κ from hasCardinalLT_subtype_iSup S hι hS
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.HasCardinalLT (goal)
Goal:
T₁ T₂ : Type w
κ : Cardinal.{w}
hκ : Cardinal.aleph0 ≤ κ
h₁ : HasCardinalLT T₁ κ
h₂ : HasCardinalLT T₂ κ
⊢ HasCardinalLT (T₁ × T₂) κ
have rw : ∀ (h₁ : Cardinal.mk T₁ < κ) (h₂ : Cardinal.mk T₂ < κ), Cardinal.mk (T₁ × T₂) < κ
Tactic: rw [hasCardinalLT_iff_cardinal_mk_lt] at h₁ h₂ ⊢
Cleared hypotheses: h₁, h₂
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.HasCardinalLT (hypothesis)
Goal:
T₁ : Type u
T₂ : Type u'
κ : Cardinal.{w}
hκ : Cardinal.aleph0 ≤ κ
h₁ : HasCardinalLT T₁ κ
h₂ : HasCardinalLT T₂ κ
⊢ HasCardinalLT (T₁ × T₂) κ
have this : HasCardinalLT (ULift.{max u' w, u} T₁ × ULift.{max u w, u'} T₂) (Cardinal.lift.{max u u', w} κ)
Tactic: have := hasCardinalLT_prod' (T₁ := ULift.{max u' w} T₁) (T₂ := ULift.{max u w} T₂)
    (κ := Cardinal.lift.{max u u'} κ) (by simpa) (by simpa) (by simpa)
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.HasCardinalLT (hypothesis)
Goal:
T₁ : Type u
T₂ : Type u'
κ : Cardinal.{w}
hκ : Cardinal.aleph0 ≤ κ
h₁ : HasCardinalLT T₁ κ
h₂ : HasCardinalLT T₂ κ
this : HasCardinalLT (ULift.{max u' w, u} T₁ × ULift.{max u w, u'} T₂) (Cardinal.lift.{max u u', w} κ)
⊢ HasCardinalLT (T₁ × T₂) κ
have this₁ : HasCardinalLT (ULift.{max u' w, u} T₁ × ULift.{max u w, u'} T₂) κ
Tactic: simp only [hasCardinalLT_lift_iff] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.HasCardinalLT (goal)
Goal:
ι : Type v
X : ι → Type u
inst : Small.{w, v} ι
inst_1 : ∀ (i : ι), Small.{w, u} (X i)
⊢ ∃ (κ : Cardinal.{w}), κ.IsRegular ∧ ∀ (i : ι), HasCardinalLT.{w, u} (X i) κ
have obtain : ∀ (κ : Cardinal.{w}) (hκ : κ.IsRegular) (h : HasCardinalLT (Sigma X) κ),
  ∃ (κ : Cardinal.{w}), κ.IsRegular ∧ ∀ (i : ι), HasCardinalLT.{w, u} (X i) κ
Tactic: obtain ⟨κ, hκ, h⟩ := exists_regular_cardinal.{w} (Sigma X)
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.NatCount (goal)
Goal:
p : ℕ → Prop
inst : DecidablePred p
n : ℕ
⊢ (↑(count p n) : Cardinal.{0}) ≤ Cardinal.mk (↑{k : ℕ | p k} : Type)
have rw : Cardinal.mk { k : ℕ // k < n ∧ p k } ≤ Cardinal.mk (↑{k : ℕ | p k} : Type)
Tactic: rw [count_eq_card_fintype, ← Cardinal.mk_fintype]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.NatCount (goal)
Goal:
p : ℕ → Prop
inst : DecidablePred p
n : ℕ
⊢ (↑(count p n) : ℕ∞) ≤ Set.encard (α := ℕ) {k : ℕ | p k}
have simp : (↑(count p n) : Cardinal.{0}) ≤ Cardinal.mk { k : ℕ // p k }
Tactic: simp only [Set.encard, ENat.card, Set.coe_setOf, Cardinal.natCast_le_toENat]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.NatCount (goal)
Goal:
p : ℕ → Prop
inst : DecidablePred p
n : ℕ
h : Set.Finite (α := ℕ) {k : ℕ | p k}
⊢ count p n ≤ Set.ncard (α := ℕ) {k : ℕ | p k}
have rw : (↑(count p n) : ℕ∞) ≤ Set.encard (α := ℕ) {k : ℕ | p k}
Tactic: rw [Set.ncard_def, ← ENat.coe_le_coe, ENat.coe_toNat (by simpa)]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Order (goal)
Goal:
c c' : Cardinal.{u_1}
| c ≤ c'
have rw : Nonempty.{u_1 + 1} (Quotient.out c ↪ Quotient.out c')
Tactic: rw [← Cardinal.mk_out c, ← Cardinal.mk_out c', le_def]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Order (goal)
Goal:
c c' : Cardinal.{u_1}
⊢ c ≤ c' ↔ Nonempty.{u_1 + 1} (Quotient.out c ↪ Quotient.out c')
have conv_lhs : c ≤ c' ↔ Nonempty.{u_1 + 1} (Quotient.out c ↪ Quotient.out c')
Tactic: conv_lhs => rw [← Cardinal.mk_out c, ← Cardinal.mk_out c', le_def]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Order (goal)
Goal:
c c' : Cardinal.{u_1}
conv_lhs : c ≤ c' ↔ Nonempty.{u_1 + 1} (Quotient.out c ↪ Quotient.out c')
⊢ c ≤ c' ↔ Nonempty.{u_1 + 1} (Quotient.out c ↪ Quotient.out c')
have conv_lhs₁ : Nonempty.{u_1 + 1} (Quotient.out c ↪ Quotient.out c') ↔ Nonempty.{u_1 + 1} (Quotient.out c ↪ Quotient.out c')
Tactic: conv_lhs => rw [← Cardinal.mk_out c, ← Cardinal.mk_out c', le_def]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Order (goal)
Goal:
α β : Type u
⊢ InitialSeg (fun (x1 x2 : Cardinal.{u}) ↦ x1 < x2) fun (x1 x2 : Cardinal.{max u v}) ↦ x1 < x2
have refine_1 : ∀ (a b : Cardinal.{u}), lift.{v, u} a ≤ lift.{v, u} b ↔ a ≤ b
Tactic: refine ⟨(OrderEmbedding.ofMapLEIff lift ?_).ltEmbedding, ?_⟩
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Order (goal)
Goal:
α β : Type u
refine_1 : ∀ (a b : Cardinal.{u}), lift.{v, u} a ≤ lift.{v, u} b ↔ a ≤ b
⊢ InitialSeg (fun (x1 x2 : Cardinal.{u}) ↦ x1 < x2) fun (x1 x2 : Cardinal.{max u v}) ↦ x1 < x2
have refine_2 : ∀ (a : Cardinal.{u}),
  ∀
    b <
      (OrderEmbedding.ltEmbedding (OrderEmbedding.ofMapLEIff lift.{v, u} sorry) : (a : Cardinal.{u}) → Cardinal.{max u v})
        a,
    Membership.mem (γ := Set Cardinal.{max u v})
      (Set.range (ι := Cardinal.{u})
        (⇑(OrderEmbedding.ltEmbedding (OrderEmbedding.ofMapLEIff lift.{v, u} sorry)) :
          (a : Cardinal.{u}) → Cardinal.{max u v}))
      b
Tactic: refine ⟨(OrderEmbedding.ofMapLEIff lift ?_).ltEmbedding, ?_⟩
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Order (goal)
Goal:
α β : Type u
a b : Cardinal.{u}
⊢ lift.{v, u} a ≤ lift.{v, u} b ↔ a ≤ b
have refine_1 : ∀ (x x_1 : Type u), lift.{v, u} #x ≤ lift.{v, u} #x_1 ↔ #x ≤ #x_1
Tactic: refine inductionOn₂ a b fun _ _ ↦ ?_
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Order (goal)
Goal:
α β : Type u
a b : Cardinal.{u}
x x_1 : Type u
⊢ lift.{v, u} #x ≤ lift.{v, u} #x_1 ↔ #x ≤ #x_1
have refine_1 : lift.{max u v, u} #x ≤ lift.{max u v, u} #x_1 ↔ #x ≤ #x_1
Tactic: rw [← lift_umax, lift_mk_le.{v, u, u}, le_def]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Order (goal)
Goal:
α β : Type u
a b : Cardinal.{u}
x x_1 : Type u
refine_1 : lift.{max u v, u} #x ≤ lift.{max u v, u} #x_1 ↔ #x ≤ #x_1
⊢ lift.{v, u} #x ≤ lift.{v, u} #x_1 ↔ #x ≤ #x_1
have refine_1₁ : Nonempty.{u + 1} (x ↪ x_1) ↔ #x ≤ #x_1
Tactic: rw [← lift_umax, lift_mk_le.{v, u, u}, le_def]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Order (goal)
Goal:
α β : Type u
a b : Cardinal.{u}
x x_1 : Type u
refine_1 : lift.{max u v, u} #x ≤ lift.{max u v, u} #x_1 ↔ #x ≤ #x_1
refine_1₁ : Nonempty.{u + 1} (x ↪ x_1) ↔ #x ≤ #x_1
⊢ lift.{v, u} #x ≤ lift.{v, u} #x_1 ↔ #x ≤ #x_1
have refine_1₂ : Nonempty.{u + 1} (x ↪ x_1) ↔ Nonempty.{u + 1} (x ↪ x_1)
Tactic: rw [← lift_umax, lift_mk_le.{v, u, u}, le_def]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Order (goal)
Goal:
α β : Type u
a : Cardinal.{u}
b : Cardinal.{max u v}
⊢ b <
      (OrderEmbedding.ltEmbedding (OrderEmbedding.ofMapLEIff lift.{v, u} ⋯) : (a : Cardinal.{u}) → Cardinal.{max u v})
        a →
    Membership.mem (γ := Set Cardinal.{max u v})
      (Set.range (ι := Cardinal.{u})
        (⇑(OrderEmbedding.ltEmbedding (OrderEmbedding.ofMapLEIff lift.{v, u} ⋯)) :
          (a : Cardinal.{u}) → Cardinal.{max u v}))
      b
have refine_2 : ∀ (α : Type u) (β : Type (max u v))
  (h :
    #β <
      (OrderEmbedding.ltEmbedding (OrderEmbedding.ofMapLEIff lift.{v, u} sorry) : (a : Cardinal.{u}) → Cardinal.{max u v})
        #α),
  Membership.mem (γ := Set Cardinal.{max u v})
    (Set.range (ι := Cardinal.{u})
      (⇑(OrderEmbedding.ltEmbedding (OrderEmbedding.ofMapLEIff lift.{v, u} sorry)) :
        (a : Cardinal.{u}) → Cardinal.{max u v}))
    #β
Tactic: refine inductionOn₂ a b fun α β h ↦ ?_
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Order (goal)
Goal:
α_1 β_1 : Type u
a : Cardinal.{u}
b : Cardinal.{max u v}
α : Type u
β : Type (max u v)
h :
  #β <
    (OrderEmbedding.ltEmbedding (OrderEmbedding.ofMapLEIff lift.{v, u} ⋯) : (a : Cardinal.{u}) → Cardinal.{max u v}) #α
⊢ Membership.mem (γ := Set Cardinal.{max u v})
    (Set.range (ι := Cardinal.{u})
      (⇑(OrderEmbedding.ltEmbedding (OrderEmbedding.ofMapLEIff lift.{v, u} ⋯)) :
        (a : Cardinal.{u}) → Cardinal.{max u v}))
    #β
have refine_2 : ∀ (e : β ↪ ULift.{v, u} α),
  Membership.mem (γ := Set Cardinal.{max u v})
    (Set.range (ι := Cardinal.{u})
      (⇑(OrderEmbedding.ltEmbedding (OrderEmbedding.ofMapLEIff lift.{v, u} sorry)) :
        (a : Cardinal.{u}) → Cardinal.{max u v}))
    #β
Tactic: obtain ⟨e⟩ := h.le
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Order (goal)
Goal:
α_1 β_1 : Type u
a : Cardinal.{u}
b : Cardinal.{max u v}
α : Type u
β : Type (max u v)
h :
  #β <
    (OrderEmbedding.ltEmbedding (OrderEmbedding.ofMapLEIff lift.{v, u} ⋯) : (a : Cardinal.{u}) → Cardinal.{max u v}) #α
e : β ↪ ULift.{v, u} α
⊢ Membership.mem (γ := Set Cardinal.{max u v})
    (Set.range (ι := Cardinal.{u})
      (⇑(OrderEmbedding.ltEmbedding (OrderEmbedding.ofMapLEIff lift.{v, u} ⋯)) :
        (a : Cardinal.{u}) → Cardinal.{max u v}))
    #β
have refine_2 : ∀ (e : β ↪ α),
  Membership.mem (γ := Set Cardinal.{max u v})
    (Set.range (ι := Cardinal.{u})
      (⇑(OrderEmbedding.ltEmbedding (OrderEmbedding.ofMapLEIff lift.{v, u} sorry)) :
        (a : Cardinal.{u}) → Cardinal.{max u v}))
    #β
Tactic: replace e := e.congr (Equiv.refl β) Equiv.ulift
Cleared hypotheses: e
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Order (goal)
Goal:
α_1 β_1 : Type u
a : Cardinal.{u}
b : Cardinal.{max u v}
α : Type u
β : Type (max u v)
h :
  #β <
    (OrderEmbedding.ltEmbedding (OrderEmbedding.ofMapLEIff lift.{v, u} ⋯) : (a : Cardinal.{u}) → Cardinal.{max u v}) #α
e : β ↪ α
⊢ Membership.mem (γ := Set Cardinal.{max u v})
    (Set.range (ι := Cardinal.{u})
      (⇑(OrderEmbedding.ltEmbedding (OrderEmbedding.ofMapLEIff lift.{v, u} ⋯)) :
        (a : Cardinal.{u}) → Cardinal.{max u v}))
    #β
have refine_2 : β ≃ (↑(Set.range (ι := β) (⇑e : (a : β) → α)) : Type u)
Tactic: refine ⟨#(range e), mk_congr (Equiv.ulift.trans <| Equiv.symm ?_)⟩
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Order (goal)
Goal:
α_1 β_1 : Type u
a : Cardinal.{u}
b : Cardinal.{max u v}
α : Type u
β : Type (max u v)
h :
  #β <
    (OrderEmbedding.ltEmbedding (OrderEmbedding.ofMapLEIff lift.{v, u} ⋯) : (a : Cardinal.{u}) → Cardinal.{max u v}) #α
e : β ↪ α
⊢ β ≃ (↑(Set.range (ι := β) (⇑e : (a : β) → α)) : Type u)
have refine_2 : Surjective (α := β) (β := (↑(Set.range (ι := β) (⇑e : (a : β) → α)) : Type u))
  (⇑(Embedding.codRestrict (Set.range (ι := β) (⇑e : (a : β) → α)) e sorry) :
    (a : β) → (↑(Set.range (⇑e : (a : β) → α)) : Type u))
Tactic: apply (e.codRestrict _ mem_range_self).equivOfSurjective
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Order (goal)
Goal:
a : Cardinal.{u}
b : Cardinal.{v}
⊢ lift.{max v w, u} a = lift.{max u w, v} b ↔ lift.{v, u} a = lift.{u, v} b
have rw : lift.{w, max v u} (lift.{v, u} a) = lift.{max u w, v} b ↔ lift.{v, u} a = lift.{u, v} b
Tactic: rw [← lift_lift.{v, w, u}, ← lift_lift.{u, w, v}, lift_inj]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Order (goal)
Goal:
a : Cardinal.{u}
b : Cardinal.{v}
rw : lift.{w, max v u} (lift.{v, u} a) = lift.{max u w, v} b ↔ lift.{v, u} a = lift.{u, v} b
⊢ lift.{max v w, u} a = lift.{max u w, v} b ↔ lift.{v, u} a = lift.{u, v} b
have rw₁ : lift.{w, max v u} (lift.{v, u} a) = lift.{w, max u v} (lift.{u, v} b) ↔ lift.{v, u} a = lift.{u, v} b
Tactic: rw [← lift_lift.{v, w, u}, ← lift_lift.{u, w, v}, lift_inj]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Order (goal)
Goal:
a : Cardinal.{u}
b : Cardinal.{v}
rw : lift.{w, max v u} (lift.{v, u} a) = lift.{max u w, v} b ↔ lift.{v, u} a = lift.{u, v} b
rw₁ : lift.{w, max v u} (lift.{v, u} a) = lift.{w, max u v} (lift.{u, v} b) ↔ lift.{v, u} a = lift.{u, v} b
⊢ lift.{max v w, u} a = lift.{max u w, v} b ↔ lift.{v, u} a = lift.{u, v} b
have rw₂ : lift.{v, u} a = lift.{u, v} b ↔ lift.{v, u} a = lift.{u, v} b
Tactic: rw [← lift_lift.{v, w, u}, ← lift_lift.{u, w, v}, lift_inj]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Order (goal)
Goal:
n : ℕ
⊢ #(ULift.{u, 0} (Fin (n + 1))) = #(ULift.{u, 0} (Fin n)) + 1
have rw : #(ULift.{u, 0} (Fin (n + 1))) = #(Option (ULift.{u, 0} (Fin n)))
Tactic: rw [← mk_option]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Order (goal)
Goal:
α β : Type u
n : ℕ
c : Cardinal.{u}
⊢ HPow.hPow (β := Cardinal.{u}) c (↑(n + 1) : Cardinal.{u}) = HPow.hPow (β := Cardinal.{u}) c (↑n : Cardinal.{u}) * c
have rw : c ^ HAdd.hAdd (α := Cardinal.{u}) (↑n : Cardinal.{u}) 1 = HPow.hPow (β := Cardinal.{u}) c (↑n : Cardinal.{u}) * c
Tactic: rw [cast_succ, power_add, power_one]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Order (goal)
Goal:
α β : Type u
n : ℕ
c : Cardinal.{u}
rw : c ^ HAdd.hAdd (α := Cardinal.{u}) (↑n : Cardinal.{u}) 1 = HPow.hPow (β := Cardinal.{u}) c (↑n : Cardinal.{u}) * c
⊢ HPow.hPow (β := Cardinal.{u}) c (↑(n + 1) : Cardinal.{u}) = HPow.hPow (β := Cardinal.{u}) c (↑n : Cardinal.{u}) * c
have rw₁ : HPow.hPow (β := Cardinal.{u}) c (↑n : Cardinal.{u}) * HPow.hPow (β := Cardinal.{u}) c 1 =
  HPow.hPow (β := Cardinal.{u}) c (↑n : Cardinal.{u}) * c
Tactic: rw [cast_succ, power_add, power_one]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Order (goal)
Goal:
α β : Type u
n : ℕ
c : Cardinal.{u}
rw : c ^ HAdd.hAdd (α := Cardinal.{u}) (↑n : Cardinal.{u}) 1 = HPow.hPow (β := Cardinal.{u}) c (↑n : Cardinal.{u}) * c
rw₁ :
  HPow.hPow (β := Cardinal.{u}) c (↑n : Cardinal.{u}) * HPow.hPow (β := Cardinal.{u}) c 1 =
    HPow.hPow (β := Cardinal.{u}) c (↑n : Cardinal.{u}) * c
⊢ HPow.hPow (β := Cardinal.{u}) c (↑(n + 1) : Cardinal.{u}) = HPow.hPow (β := Cardinal.{u}) c (↑n : Cardinal.{u}) * c
have rw₂ : HPow.hPow (β := Cardinal.{u}) c (↑n : Cardinal.{u}) * c = HPow.hPow (β := Cardinal.{u}) c (↑n : Cardinal.{u}) * c
Tactic: rw [cast_succ, power_add, power_one]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Order (goal)
Goal:
a b c : Cardinal.{u_1}
⊢ a ^ (b * c) = (a ^ b) ^ c
have rw : a ^ (c * b) = (a ^ b) ^ c
Tactic: rw [mul_comm b c]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Order (goal)
Goal:
c : Cardinal.{u}
⊢ HPow.hPow (α := Cardinal.{u}) 0 c ≤ 1
have pos : ∀ (h : c = 0), HPow.hPow (α := Cardinal.{u}) 0 c ≤ 1
Tactic: by_cases h : c = 0
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Order (goal)
Goal:
c : Cardinal.{u}
pos : ∀ (h : c = 0), HPow.hPow (α := Cardinal.{u}) 0 c ≤ 1
⊢ HPow.hPow (α := Cardinal.{u}) 0 c ≤ 1
have neg : ∀ (h : ¬c = 0), HPow.hPow (α := Cardinal.{u}) 0 c ≤ 1
Tactic: by_cases h : c = 0
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Order (goal)
Goal:
c : Cardinal.{u}
h : c = 0
⊢ HPow.hPow (α := Cardinal.{u}) 0 c ≤ 1
have pos : HPow.hPow (α := Cardinal.{u}) (β := Cardinal.{u}) 0 0 ≤ 1
Tactic: rw [h, power_zero]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Order (goal)
Goal:
c : Cardinal.{u}
h : c = 0
pos : HPow.hPow (α := Cardinal.{u}) (β := Cardinal.{u}) 0 0 ≤ 1
⊢ HPow.hPow (α := Cardinal.{u}) 0 c ≤ 1
have pos₁ : LE.le.{u + 1} (α := Cardinal.{u}) 1 1
Tactic: rw [h, power_zero]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Order (goal)
Goal:
c : Cardinal.{u}
h : ¬c = 0
⊢ HPow.hPow (α := Cardinal.{u}) 0 c ≤ 1
have neg : LE.le.{u + 1} (α := Cardinal.{u}) 0 1
Tactic: rw [zero_power h]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Order (goal)
Goal:
a : Cardinal.{u_1}
α : Type u_1
b : Cardinal.{u_1}
β : Type u_1
c : Cardinal.{u_1}
γ : Type u_1
hα : Ne (α := Cardinal.{u_1}) (Quot.mk (⇑isEquivalent : Type u_1 → Type u_1 → Prop) α) 0
e : β ↪ γ
⊢ HPow.hPow (α := Cardinal.{u_1}) (β := Cardinal.{u_1}) (Quot.mk (⇑isEquivalent : Type u_1 → Type u_1 → Prop) α)
      (Quot.mk (⇑isEquivalent : Type u_1 → Type u_1 → Prop) β) ≤
    HPow.hPow (α := Cardinal.{u_1}) (β := Cardinal.{u_1}) (Quot.mk (⇑isEquivalent : Type u_1 → Type u_1 → Prop) α)
      (Quot.mk (⇑isEquivalent : Type u_1 → Type u_1 → Prop) γ)
have mk : ∀ (a : α),
  HPow.hPow (α := Cardinal.{u_1}) (β := Cardinal.{u_1}) (Quot.mk (⇑isEquivalent : Type u_1 → Type u_1 → Prop) α)
      (Quot.mk (⇑isEquivalent : Type u_1 → Type u_1 → Prop) β) ≤
    HPow.hPow (α := Cardinal.{u_1}) (β := Cardinal.{u_1}) (Quot.mk (⇑isEquivalent : Type u_1 → Type u_1 → Prop) α)
      (Quot.mk (⇑isEquivalent : Type u_1 → Type u_1 → Prop) γ)
Tactic: let ⟨a⟩ := mk_ne_zero_iff.1 hα
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Order (goal)
Goal:
a b : Cardinal.{u_1}
hb : 1 ≤ b
⊢ a ≤ a ^ b
have inl : 0 ≤ HPow.hPow (α := Cardinal.{u_1}) 0 b
Tactic: rcases eq_or_ne a 0 with (rfl | ha)
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Order (goal)
Goal:
a b : Cardinal.{u_1}
hb : 1 ≤ b
inl : 0 ≤ HPow.hPow (α := Cardinal.{u_1}) 0 b
⊢ a ≤ a ^ b
have inr : ∀ (ha : a ≠ 0), a ≤ a ^ b
Tactic: rcases eq_or_ne a 0 with (rfl | ha)
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Order (goal)
Goal:
a b : Cardinal.{u_1}
hb : 1 ≤ b
ha : a ≠ 0
⊢ a ≤ a ^ b
have h : a = HPow.hPow (β := Cardinal.{u_1}) a 1
Tactic: convert! power_le_power_left ha hb
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Order (goal)
Goal:
a : Cardinal.{u}
⊢ a < HPow.hPow (α := Cardinal.{u}) 2 a
have mk : ∀ (α : Type u), #α < HPow.hPow (α := Cardinal.{u}) 2 #α
Tactic: induction a using Cardinal.inductionOn with | _ α
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Order (goal)
Goal:
α : Type u
⊢ #α < HPow.hPow (α := Cardinal.{u}) 2 #α
have mk : #α < #(Set α)
Tactic: rw [← mk_set]
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Order (goal)
Goal:
α : Type u
⊢ #α < #(Set α)
have mk : ¬#(Set α) ≤ #α
Tactic: refine ⟨⟨⟨singleton, fun a b => singleton_eq_singleton_iff.1⟩⟩, ?_⟩
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Order (goal)
Goal:
a b c : Cardinal.{u_1}
h : b ≤ c
⊢ a ^ b ≤ max (a ^ c) 1
have pos : ∀ (ha : a = 0), a ^ b ≤ max (a ^ c) 1
Tactic: by_cases ha : a = 0
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Order (goal)
Goal:
a b c : Cardinal.{u_1}
h : b ≤ c
pos : ∀ (ha : a = 0), a ^ b ≤ max (a ^ c) 1
⊢ a ^ b ≤ max (a ^ c) 1
have neg : ∀ (ha : ¬a = 0), a ^ b ≤ max (a ^ c) 1
Tactic: by_cases ha : a = 0
-- 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)
⊢ False
have hι : Nonempty ι
Tactic: haveI hι : Nonempty ι := ⟨⟨_, h⟩⟩
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Order (goal)
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 ι
⊢ False
have obtain : ∀ (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)),
  False
Tactic: obtain ⟨⟨c : Cardinal, hc : ¬Acc (· < ·) c⟩, ⟨h_1 : ∀ j, (f ⟨c, hc⟩).out ↪ (f j).out⟩⟩ :=
        Embedding.min_injective fun i => (f i).out
-- Lean 4 proof step from Mathlib.SetTheory.Cardinal.Order (goal)
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)
⊢ False
have refine : ∀ (j : Cardinal.{u}) (h' : j < c) (hj : ¬Acc (fun (x1 x2 : Cardinal.{u}) ↦ x1 < x2) j), c ≤ j
Tactic: refine hc (Acc.intro _ fun j h' => by_contradiction fun hj => h'.2 ?_)