awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.SetTheory.Cardinal.Defs
Goal:
a b : Cardinal.{u}
⊢ lift.{v, u} (a ^ b) = lift.{v, u} a ^ lift.{v, u} b

Tactic:
inductionOn₂ a b fun _ _ =>
    mk_congr <| Equiv.ulift.trans (Equiv.ulift.arrowCongr Equiv.ulift).symm

Premises used: Cardinal.inductionOn₂
-- Module: Mathlib.SetTheory.Cardinal.Defs
Goal:
a : Cardinal.{u_1}
⊢ HPow.hPow (β := Cardinal.{u_1}) a 0 = 1

Tactic:
inductionOn a fun _ => mk_eq_one _

Premises used: Cardinal.inductionOn
-- Module: Mathlib.SetTheory.Cardinal.Defs
Goal:
a : Cardinal.{u}
⊢ HPow.hPow (β := Cardinal.{u}) a 1 = a

Tactic:
inductionOn a fun α => mk_congr (Equiv.funUnique (ULift.{u} (Fin 1)) α)

Premises used: Cardinal.inductionOn
-- Module: Mathlib.SetTheory.Cardinal.Defs
Goal:
a b c : Cardinal.{u_1}
⊢ a ^ (b + c) = a ^ b * a ^ c

Tactic:
inductionOn₃ a b c fun α β γ => mk_congr <| Equiv.sumArrowEquivProdArrow β γ α

Premises used: Cardinal.inductionOn₃
-- Module: Mathlib.SetTheory.Cardinal.Defs
Goal:
a : Cardinal.{u_1}
⊢ HPow.hPow (α := Cardinal.{u_1}) 1 a = 1

Tactic:
inductionOn a fun _ => mk_eq_one _

Premises used: Cardinal.inductionOn
-- Module: Mathlib.SetTheory.Cardinal.Defs
Goal:
a : Cardinal.{u_1}
⊢ a ≠ 0 → HPow.hPow (α := Cardinal.{u_1}) 0 a = 0

Tactic:
inductionOn a fun _ heq =>
    mk_eq_zero_iff.2 <|
      isEmpty_pi.2 <|
        let ⟨a⟩ := mk_ne_zero_iff.1 heq
        ⟨a, inferInstance⟩

Premises used: Cardinal.inductionOn
-- Module: Mathlib.SetTheory.Cardinal.Defs
Goal:
a b : Cardinal.{u_1}
⊢ a ≠ 0 → a ^ b ≠ 0

Tactic:
inductionOn₂ a b fun _ _ h =>
    let ⟨a⟩ := mk_ne_zero_iff.1 h
    mk_ne_zero_iff.2 ⟨fun _ => a⟩

Premises used: Cardinal.inductionOn₂
-- Module: Mathlib.SetTheory.Cardinal.Defs
Goal:
a b c : Cardinal.{u_1}
⊢ (a * b) ^ c = a ^ c * b ^ c

Tactic:
inductionOn₃ a b c fun _ _ γ => mk_congr <| Equiv.arrowProdEquivProdArrow γ _ _

Premises used: Cardinal.inductionOn₃
-- Module: Mathlib.SetTheory.Cardinal.Defs
Goal:
⊢ lift.{u_2, u_1} 1 = 1

Tactic:
mk_eq_one _

Premises used: Quotient.map, Cardinal.lift, Cardinal.map, Quot.map, Cardinal.mk_eq_one
-- Module: Mathlib.SetTheory.Cardinal.Defs
Goal:
a b : Cardinal.{u}
⊢ lift.{v, u} (a + b) = lift.{v, u} a + lift.{v, u} b

Tactic:
inductionOn₂ a b fun _ _ =>
    mk_congr <| Equiv.ulift.trans (Equiv.sumCongr Equiv.ulift Equiv.ulift).symm

Premises used: Cardinal.inductionOn₂
-- Module: Mathlib.SetTheory.Cardinal.Defs
Goal:
ι : Type u_2
f : ι → Type u_1
⊢ #((i : ι) × f i) = sum.{u_2, u_1} fun (i : ι) ↦ #(f i)

Tactic:
mk_congr <| Equiv.sigmaCongrRight fun _ => outMkEquiv.symm

Premises used: Cardinal.outMkEquiv, Equiv.symm, Equiv.sigmaCongrRight, Cardinal.mk_congr, Cardinal.sum
-- Module: Mathlib.SetTheory.Cardinal.Defs
Goal:
ι : Type v
ι' : Type v'
f : ι → Type w
g : ι' → Type w'
e : ι ≃ ι'
h : ∀ (i : ι), lift.{w', w} #(f i) = lift.{w, w'} #(g ((e : (a : ι) → ι') i))
⊢ lift.{max v' w', max w v} #((i : ι) × f i) = lift.{max v w, max w' v'} #((i : ι') × g i)

Tactic:
Cardinal.lift_mk_eq'.2 ⟨.sigmaCongr e fun i ↦ Classical.choice <| Cardinal.lift_mk_eq'.1 (h i)⟩

Premises used: Iff.mpr, Equiv.sigmaCongr, Classical.choice, Cardinal.lift_mk_eq', Nonempty.intro, Iff.mp
-- Module: Mathlib.SetTheory.Cardinal.Defs
Goal:
ι ι' : Type u
f : ι → Type v
g : ι' → Type v
e : ι ≃ ι'
h : ∀ (i : ι), #(f i) = #(g ((e : (a : ι) → ι') i))
⊢ #((i : ι) × f i) = #((i : ι') × g i)

Tactic:
mk_congr <| Equiv.sigmaCongr e fun i ↦ Classical.choice <| Cardinal.eq.mp (h i)

Premises used: Equiv.sigmaCongr, Classical.choice, Cardinal.eq, Iff.mp, Cardinal.mk_congr
-- Module: Mathlib.SetTheory.Cardinal.Defs
Goal:
ι : Type u
ι' : Type v
f : ι → Type (max w u v)
g : ι' → Type (max w u v)
e : ι ≃ ι'
h : ∀ (i : ι), #(f i) = #(g ((e : (a : ι) → ι') i))
⊢ #((i : ι) × f i) = #((i : ι') × g i)

Tactic:
mk_congr <| Equiv.sigmaCongr e fun i ↦ Classical.choice <| Cardinal.eq.mp (h i)

Premises used: Equiv.sigmaCongr, Classical.choice, Cardinal.eq, Iff.mp, Cardinal.mk_congr
-- Module: Mathlib.SetTheory.Cardinal.Defs
Goal:
ι : Type u
f g : ι → Type v
h : ∀ (i : ι), #(f i) = #(g i)
⊢ #((i : ι) × f i) = #((i : ι) × g i)

Tactic:
mk_sigma_congr (Equiv.refl ι) h

Premises used: Equiv.refl, Cardinal.mk_sigma_congr
-- Module: Mathlib.SetTheory.Cardinal.Defs
Goal:
ι : Type u
f g : ι → Type v
h : ∀ (i : ι), #(f i) = #(g i)
⊢ #((i : ι) ×' f i) = #((i : ι) ×' g i)

Tactic:
mk_congr <| .psigmaCongrRight fun i => Classical.choice <| Cardinal.eq.mp (h i)

Premises used: Equiv.psigmaCongrRight, Classical.choice, Cardinal.eq, Iff.mp, Cardinal.mk_congr
-- Module: Mathlib.SetTheory.Cardinal.Defs
Goal:
ι : Prop
f g : ι → Type v
h : ∀ (i : ι), #(f i) = #(g i)
⊢ #((i : ι) ×' f i) = #((i : ι) ×' g i)

Tactic:
mk_congr <| .psigmaCongrRight fun i => Classical.choice <| Cardinal.eq.mp (h i)

Premises used: Equiv.psigmaCongrRight, Classical.choice, Cardinal.eq, Iff.mp, Cardinal.mk_congr
-- Module: Mathlib.SetTheory.Cardinal.Defs
Goal:
ι : Type u_3
α : Type u_1
f : ι → Type u_2
⊢ #(Sigma f → α) = #((i : ι) → f i → α)

Tactic:
mk_congr <| Equiv.piCurry fun _ _ ↦ α

Premises used: Equiv.piCurry, Cardinal.mk_congr
-- Module: Mathlib.SetTheory.Cardinal.Defs
Goal:
ι : Type u
a : Cardinal.{v}
⊢ (sum.{u, v} fun (x : ι) ↦ a) = lift.{v, u} #ι * lift.{u, v} a

Tactic:
inductionOn a fun α =>
    mk_congr <|
      calc
        (Σ _ : ι, Quotient.out #α) ≃ ι × Quotient.out #α := Equiv.sigmaEquivProd _ _
        _ ≃ ULift ι × ULift α := Equiv.ulift.symm.prodCongr (outMkEquiv.trans Equiv.ulift.symm)

Premises used: Cardinal.inductionOn
-- Module: Mathlib.SetTheory.Cardinal.Defs
Goal:
ι : Type u
a : Cardinal.{u}
⊢ (sum fun (x : ι) ↦ a) = #ι * a

Tactic:
simp
-- Module: Mathlib.SetTheory.Cardinal.Defs
Goal:
ι : Type u
f : ι → Cardinal.{v}
a : ι
rw :
  lift.{max v w, v} #(Quotient.out (f a)) =
    lift.{v, max v w} #(Quotient.out (s := isEquivalent) ((fun (i : ι) ↦ lift.{w, v} (f i)) a))
rw₁ :
  lift.{max v w, v} (f a) = lift.{v, max v w} #(Quotient.out (s := isEquivalent) ((fun (i : ι) ↦ lift.{w, v} (f i)) a))
rw₂ : lift.{max v w, v} (f a) = lift.{v, max v w} ((fun (i : ι) ↦ lift.{w, v} (f i)) a)
rw₃ rw₄ : lift.{max v w, v} (f a) = lift.{max w v, v} (f a)
⊢ Nonempty (Quotient.out (f a) ≃ Quotient.out (s := isEquivalent) ((fun (i : ι) ↦ lift.{w, v} (f i)) a))

Tactic:
rw [← lift_mk_eq.{_, _, v}, mk_out, mk_out, lift_lift]

Premises used: Cardinal.lift_lift, Cardinal.mk_out
-- Module: Mathlib.SetTheory.Cardinal.Defs
Goal:
f : ℕ → Cardinal.{u}
⊢ sum f = f 0 + sum fun (i : ℕ) ↦ f (i + 1)

Tactic:
(Equiv.sigmaNatSucc fun i => Quotient.out (f i)).cardinal_eq.trans ?_

Premises used: Quotient.out, Equiv.sigmaNatSucc, Eq.trans, Equiv.cardinal_eq, Cardinal.sum
-- Module: Mathlib.SetTheory.Cardinal.Defs
Goal:
f : ℕ → Cardinal.{u}
refine : #(Quotient.out (f 0) ⊕ (n : ℕ) × Quotient.out (f (n + 1))) = f 0 + sum fun (i : ℕ) ↦ f (i + 1)
⊢ sum f = f 0 + sum fun (i : ℕ) ↦ f (i + 1)

Tactic:
refine (Equiv.sigmaNatSucc fun i => Quotient.out (f i)).cardinal_eq.trans ?_

Premises used: Quotient.out, Equiv.sigmaNatSucc, Eq.trans, Equiv.cardinal_eq
-- Module: Mathlib.SetTheory.Cardinal.Defs
Goal:
f : ℕ → Cardinal.{u}
⊢ #(Quotient.out (f 0) ⊕ (n : ℕ) × Quotient.out (f (n + 1))) = f 0 + sum fun (i : ℕ) ↦ f (i + 1)

Tactic:
simp only [mk_sum, mk_out, lift_id, mk_sigma]

Premises used: Cardinal.mk_out, Cardinal.mk_sigma, Cardinal.mk_sum, Cardinal.lift_id
-- Module: Mathlib.SetTheory.Cardinal.Defs
Goal:
ι : Type u
α : ι → Type v
⊢ #((i : ι) → α i) = prod.{u, v} fun (i : ι) ↦ #(α i)

Tactic:
mk_congr <| Equiv.piCongrRight fun _ => outMkEquiv.symm

Premises used: Cardinal.outMkEquiv, Equiv.piCongrRight, Cardinal.prod, Equiv.symm, Cardinal.mk_congr
-- Module: Mathlib.SetTheory.Cardinal.Defs
Goal:
ι : Type v
ι' : Type v'
f : ι → Type w
g : ι' → Type w'
e : ι ≃ ι'
h : ∀ (i : ι), lift.{w', w} #(f i) = lift.{w, w'} #(g ((e : (a : ι) → ι') i))
⊢ lift.{max v' w', max v w} #((i : ι) → f i) = lift.{max v w, max v' w'} #((i : ι') → g i)

Tactic:
Cardinal.lift_mk_eq'.2 ⟨.piCongr e fun i ↦ Classical.choice <| Cardinal.lift_mk_eq'.1 (h i)⟩

Premises used: Iff.mpr, Classical.choice, Cardinal.lift_mk_eq', Nonempty.intro, Iff.mp, Equiv.piCongr
-- Module: Mathlib.SetTheory.Cardinal.Defs
Goal:
ι ι' : Type u
f : ι → Type v
g : ι' → Type v
e : ι ≃ ι'
h : ∀ (i : ι), #(f i) = #(g ((e : (a : ι) → ι') i))
⊢ #((i : ι) → f i) = #((i : ι') → g i)

Tactic:
mk_congr <| Equiv.piCongr e fun i ↦ Classical.choice <| Cardinal.eq.mp (h i)

Premises used: Classical.choice, Cardinal.eq, Iff.mp, Equiv.piCongr, Cardinal.mk_congr
-- Module: Mathlib.SetTheory.Cardinal.Defs
Goal:
ι ι' : Prop
f : ι → Type v
g : ι' → Type v
e : ι ↔ ι'
h : ∀ (i : ι), #(f i) = #(g ⋯)
⊢ #((i : ι) → f i) = #((i : ι') → g i)

Tactic:
mk_congr <| Equiv.piCongr (.ofIff e) fun i ↦ Classical.choice <| Cardinal.eq.mp (h i)

Premises used: Classical.choice, Cardinal.eq, Iff.mp, Equiv.piCongr, Equiv.ofIff, Cardinal.mk_congr
-- Module: Mathlib.SetTheory.Cardinal.Defs
Goal:
ι : Type u
ι' : Type v
f : ι → Type (max w u v)
g : ι' → Type (max w u v)
e : ι ≃ ι'
h : ∀ (i : ι), #(f i) = #(g ((e : (a : ι) → ι') i))
⊢ #((i : ι) → f i) = #((i : ι') → g i)

Tactic:
mk_congr <| Equiv.piCongr e fun i ↦ Classical.choice <| Cardinal.eq.mp (h i)

Premises used: Classical.choice, Cardinal.eq, Iff.mp, Equiv.piCongr, Cardinal.mk_congr
-- Module: Mathlib.SetTheory.Cardinal.Defs
Goal:
ι : Type u
f g : ι → Type v
h : ∀ (i : ι), #(f i) = #(g i)
⊢ #((i : ι) → f i) = #((i : ι) → g i)

Tactic:
mk_pi_congr (Equiv.refl ι) h

Premises used: Cardinal.mk_pi_congr, Equiv.refl
-- Module: Mathlib.SetTheory.Cardinal.Defs
Goal:
ι : Prop
f g : ι → Type v
h : ∀ (i : ι), #(f i) = #(g i)
⊢ #((i : ι) → f i) = #((i : ι) → g i)

Tactic:
mk_pi_congr_prop Iff.rfl h

Premises used: Iff.rfl, Cardinal.mk_pi_congr_prop
-- Module: Mathlib.SetTheory.Cardinal.Defs
Goal:
ι : Type u
a : Cardinal.{v}
⊢ (prod.{u, v} fun (x : ι) ↦ a) = lift.{u, v} a ^ lift.{v, u} #ι

Tactic:
inductionOn a fun _ =>
    mk_congr <| Equiv.piCongr Equiv.ulift.symm fun _ => outMkEquiv.trans Equiv.ulift.symm

Premises used: Cardinal.inductionOn
-- Module: Mathlib.SetTheory.Cardinal.Defs
Goal:
ι : Type u
a : Cardinal.{u}
⊢ (prod fun (x : ι) ↦ a) = a ^ #ι

Tactic:
inductionOn a fun _ => (mk_pi _).symm

Premises used: Cardinal.inductionOn
-- Module: Mathlib.SetTheory.Cardinal.Defs
Goal:
ι : Type u_1
f : ι → Cardinal.{u}
⊢ ∀ (i : ι), True

Tactic:
fun _ => trivial

Premises used: trivial
-- Module: Mathlib.SetTheory.Cardinal.Defs
Goal:
ι : Type u_1
f : ι → Cardinal.{u}
lift :
  ∀ (f : (i : ι) → Type u),
    (prod.{u_1, u} fun (i : ι) ↦ #(f i)) = 0 ↔
      ∃ (i : ι), Eq.{u + 2} (α := Cardinal.{u}) ((fun (i : ι) ↦ mk.{u} (f i)) i) 0
⊢ prod f = 0 ↔ ∃ (i : ι), f i = 0

Tactic:
lift f to ι → Type u using fun _ => trivial

Premises used: trivial
-- Module: Mathlib.SetTheory.Cardinal.Defs
Goal:
ι : Type u_1
f : (i : ι) → Type u
⊢ (prod.{u_1, u} fun (i : ι) ↦ #(f i)) = 0 ↔
    ∃ (i : ι), Eq.{u + 2} (α := Cardinal.{u}) ((fun (i : ι) ↦ mk.{u} (f i)) i) 0

Tactic:
simp only [mk_eq_zero_iff, ← mk_pi, isEmpty_pi]

Premises used: Cardinal.mk_pi, Cardinal.mk_eq_zero_iff, isEmpty_pi
-- Module: Mathlib.SetTheory.Cardinal.Defs
Goal:
ι : Type u_1
f : ι → Cardinal.{u_2}
⊢ prod f ≠ 0 ↔ ∀ (i : ι), f i ≠ 0

Tactic:
simp [prod_eq_zero]

Premises used: Cardinal.prod_eq_zero
-- Module: Mathlib.SetTheory.Cardinal.Defs
Goal:
ι : Type u
α : Type v
f : ι → Type v
mk : ((i : ι) × Quotient.out #(f i) → ULift.{u, v} α) ≃ ((i : ι) → Quotient.out #(f i → α))
⊢ #((i : ι) × Quotient.out #(f i) → ULift.{u, v} α) = #((i : ι) → Quotient.out #(f i → α))

Tactic:
apply mk_congr

Premises used: Cardinal.mk_congr
-- Module: Mathlib.SetTheory.Cardinal.Defs
Goal:
ι : Type u
α : Type v
f : ι → Type v
mk : ((a : ι) → (b : Quotient.out #(f a)) → ULift.{u, v} α) ≃ ((i : ι) → Quotient.out #(f i → α))
⊢ ((i : ι) × Quotient.out #(f i) → ULift.{u, v} α) ≃ ((i : ι) → Quotient.out #(f i → α))

Tactic:
refine (Equiv.piCurry fun _ _ => ULift α).trans ?_

Premises used: Equiv.trans, ULift, Equiv.piCurry
-- Module: Mathlib.SetTheory.Cardinal.Defs
Goal:
ι : Type u
α : Type v
f : ι → Type v
mk : (b : ι) → ((b : Quotient.out #(f b)) → ULift.{u, v} α) ≃ Quotient.out #(f b → α)
⊢ ((a : ι) → (b : Quotient.out #(f a)) → ULift.{u, v} α) ≃ ((i : ι) → Quotient.out #(f i → α))

Tactic:
refine Equiv.piCongrRight fun b => ?_

Premises used: Equiv.piCongrRight
-- Module: Mathlib.SetTheory.Cardinal.Defs
Goal:
ι : Type u
α : Type v
f : ι → Type v
b : ι
mk : (f b → α) ≃ Quotient.out #(f b → α)
⊢ ((b : Quotient.out #(f b)) → ULift.{u, v} α) ≃ Quotient.out #(f b → α)

Tactic:
refine (Equiv.arrowCongr outMkEquiv Equiv.ulift).trans ?_

Premises used: Equiv.trans, Equiv.arrowCongr, Equiv.ulift, Cardinal.outMkEquiv
-- Module: Mathlib.SetTheory.Cardinal.Defs
Goal:
ι : Type u
α : Type v
f : ι → Type v
b : ι
⊢ (f b → α) ≃ Quotient.out #(f b → α)

Tactic:
exact outMkEquiv.symm

Premises used: Cardinal.outMkEquiv, Equiv.symm
-- Module: Mathlib.SetTheory.Cardinal.Defs
Goal:
ι : Type u
f : ι → Cardinal.{v}
α : Type v
mk :
  ∀ (f : ι → Type v),
    (lift.{u, v} #α ^ sum.{u, v} fun (i : ι) ↦ #(f i)) =
      prod.{u, v} fun (i : ι) ↦ HPow.hPow (β := Cardinal.{v}) (#α) ((fun (i : ι) ↦ Cardinal.mk.{v} (f i)) i)
⊢ lift.{u, v} #α ^ sum f = prod.{u, v} fun (i : ι) ↦ #α ^ f i

Tactic:
induction f using induction_on_pi with | _ f =>
  simp_rw [← mk_uLift, prod, sum, power_def]
  apply mk_congr
  refine (Equiv.piCurry fun _ _ => ULift α).trans ?_
  refine Equiv.piCongrRight fun b => ?_
  refine (Equiv.arrowCongr outMkEquiv Equiv.ulift).trans ?_
  exact outMkEquiv.symm

Premises used: Cardinal.induction_on_pi, Equiv.trans, ULift, Equiv.arrowCongr, Equiv.ulift, Equiv.piCurry, Cardinal.outMkEquiv, Cardinal.mk_uLift, Equiv.piCongrRight, Cardinal.prod, Equiv.symm, Cardinal.power_def, Cardinal.mk_congr, Cardinal.sum
-- Module: Mathlib.SetTheory.Cardinal.Defs
Goal:
ι : Type u
a : Cardinal.{v}
f : ι → Cardinal.{v}
mk : ∀ (α : Type v), lift.{u, v} #α ^ sum f = prod.{u, v} fun (i : ι) ↦ #α ^ f i
⊢ lift.{u, v} a ^ sum f = prod.{u, v} fun (i : ι) ↦ a ^ f i

Tactic:
induction a using Cardinal.inductionOn with | _ α =>
  induction f using induction_on_pi with | _ f =>
  simp_rw [← mk_uLift, prod, sum, power_def]
  apply mk_congr
  refine (Equiv.piCurry fun _ _ => ULift α).trans ?_
  refine Equiv.piCongrRight fun b => ?_
  refine (Equiv.arrowCongr outMkEquiv Equiv.ulift).trans ?_
  exact outMkEquiv.symm

Premises used: Cardinal.induction_on_pi, Equiv.trans, Equiv.arrowCongr, Equiv.ulift, Cardinal.outMkEquiv, Cardinal.mk_uLift, Equiv.piCongrRight, Cardinal.prod, Equiv.symm, Cardinal.power_def, Cardinal.mk_congr, Cardinal.sum
-- Module: Mathlib.SetTheory.Cardinal.Defs
Goal:
ι : Type u
a : Cardinal.{max u v}
f : ι → Cardinal.{max u v}
⊢ a ^ sum f = prod fun (i : ι) ↦ a ^ f i

Tactic:
simpa [← lift_umax] using lift_power_sum a f

Premises used: Cardinal.lift_power_sum, Cardinal.lift_umax
-- Module: Mathlib.SetTheory.Cardinal.Defs
Goal:
ι : Type u
c : ι → Cardinal.{v}
⊢ ∀ (i : ι), True

Tactic:
fun _ => trivial

Premises used: trivial
-- Module: Mathlib.SetTheory.Cardinal.Defs
Goal:
ι : Type u
c : ι → Cardinal.{v}
lift :
  ∀ (c : (i : ι) → Type v),
    Cardinal.lift.{w, max v u} (prod.{u, v} fun (i : ι) ↦ #(c i)) =
      prod fun (i : ι) ↦ Cardinal.lift.{w, v} ((fun (i : ι) ↦ mk.{v} (c i)) i)
⊢ Cardinal.lift.{w, max v u} (prod c) = prod fun (i : ι) ↦ Cardinal.lift.{w, v} (c i)

Tactic:
lift c to ι → Type v using fun _ => trivial

Premises used: trivial
-- Module: Mathlib.SetTheory.Cardinal.Defs
Goal:
ι : Type u
c : (i : ι) → Type v
simp : #(ULift ((i : ι) → c i)) = #((i : ι) → ULift.{w, v} (c i))
⊢ lift.{w, max v u} (prod.{u, v} fun (i : ι) ↦ #(c i)) = prod fun (i : ι) ↦ lift.{w, v} ((fun (i : ι) ↦ mk.{v} (c i)) i)

Tactic:
simp only [← mk_pi, ← mk_uLift]

Premises used: Cardinal.mk_pi, Cardinal.mk_uLift
-- Module: Mathlib.SetTheory.Cardinal.Defs
Goal:
ι : Type u
c : (i : ι) → Type v
⊢ #(ULift ((i : ι) → c i)) = #((i : ι) → ULift.{w, v} (c i))

Tactic:
mk_congr (Equiv.ulift.trans <| Equiv.piCongrRight fun i => Equiv.ulift.symm)

Premises used: Equiv.trans, Equiv.ulift, Equiv.piCongrRight, Equiv.symm, Cardinal.mk_congr
-- Module: Mathlib.SetTheory.Cardinal.Defs
Goal:
ι : Type u
c : (i : ι) → Type v
⊢ #(ULift ((i : ι) → c i)) = #((i : ι) → ULift.{w, v} (c i))

Tactic:
exact mk_congr (Equiv.ulift.trans <| Equiv.piCongrRight fun i => Equiv.ulift.symm)

Premises used: Equiv.trans, Equiv.ulift, Equiv.piCongrRight, Equiv.symm, Cardinal.mk_congr
-- Module: Mathlib.SetTheory.Cardinal.Defs
Goal:
⊢ #ℕ = ℵ₀

Tactic:
(lift_id _).symm

Premises used: Cardinal.aleph0, Eq.symm, Cardinal.lift_id
-- Module: Mathlib.SetTheory.Cardinal.Defs
Goal:
⊢ ℵ₀ ≠ 0

Tactic:
mk_ne_zero _

Premises used: Quotient.map, Cardinal.lift, Cardinal.aleph0, Cardinal.map, Quot.map, Cardinal.mk_ne_zero
-- Module: Mathlib.SetTheory.Cardinal.Defs
Goal:
⊢ lift.{u_1, u_2} ℵ₀ = ℵ₀

Tactic:
lift_lift _

Premises used: Cardinal.lift_lift, Cardinal.aleph0
-- Module: Mathlib.SetTheory.Cardinal.Defs
Goal:
n : ℕ
⊢ lift.{u_1, 0} #(Fin n) = (↑n : Cardinal.{u_1})

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.SetTheory.Cardinal.Defs
Goal:
⊢ #Empty = 0

Tactic:
mk_eq_zero _

Premises used: Cardinal.mk_eq_zero
-- Module: Mathlib.SetTheory.Cardinal.Defs
Goal:
⊢ #PEmpty = 0

Tactic:
mk_eq_zero _

Premises used: Cardinal.mk_eq_zero
-- Module: Mathlib.SetTheory.Cardinal.Defs
Goal:
⊢ #PUnit = 1

Tactic:
mk_eq_one PUnit

Premises used: PUnit, Cardinal.mk_eq_one
-- Module: Mathlib.SetTheory.Cardinal.Defs
Goal:
⊢ #Unit = 1

Tactic:
mk_punit

Premises used: Cardinal.mk_punit
-- Module: Mathlib.SetTheory.Cardinal.Defs
Goal:
⊢ #(PLift True) = 1

Tactic:
mk_eq_one _

Premises used: Cardinal.mk_eq_one
-- Module: Mathlib.SetTheory.Cardinal.Defs
Goal:
⊢ #(PLift False) = 0

Tactic:
mk_eq_zero _

Premises used: Cardinal.mk_eq_zero
-- Module: Mathlib.SetTheory.Cardinal.Defs
Goal:
α β : Type u
p : β → Prop
e : α ≃ β
⊢ #{ a : α // p ((e : (a : α) → β) a) } = #{ b : β // p b }

Tactic:
mk_congr (Equiv.subtypeEquivOfSubtype e)

Premises used: Cardinal.mk_congr, Equiv.subtypeEquivOfSubtype
-- Module: Mathlib.SetTheory.Cardinal.Divisibility
Goal:
⊢ IsUnit.{u + 1} (M := Cardinal.{u}) 1

Tactic:
isUnit_one

Premises used: isUnit_one
-- Module: Mathlib.SetTheory.Cardinal.Divisibility
Goal:
⊢ IsUnit.{u + 1} (M := Cardinal.{u}) 1

Tactic:
exact isUnit_one

Premises used: isUnit_one
-- Module: Mathlib.SetTheory.Cardinal.Divisibility
Goal:
a : Cardinal.{u}
h : ∀ (h : IsUnit a), a = 1
⊢ IsUnit a ↔ a = 1

Tactic:
refine
    ⟨fun h => ?_, by
      rintro rfl
      exact isUnit_one⟩
-- Module: Mathlib.SetTheory.Cardinal.Divisibility
Goal:
a : Cardinal.{u}
h : IsUnit a
inl : ∀ (h : IsUnit.{u + 1} (M := Cardinal.{u}) 0), Eq.{u + 2} (α := Cardinal.{u}) 0 1
inr : ∀ (ha : a ≠ 0), a = 1
⊢ a = 1

Tactic:
rcases eq_or_ne a 0 with (rfl | ha)

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.SetTheory.Cardinal.Divisibility
Goal:
h : IsUnit.{u + 1} (M := Cardinal.{u}) 0
⊢ Eq.{u + 2} (α := Cardinal.{u}) 0 1

Tactic:
(not_isUnit_zero h).elim

Premises used: False.elim, not_isUnit_zero
-- Module: Mathlib.SetTheory.Cardinal.Divisibility
Goal:
h : IsUnit.{u + 1} (M := Cardinal.{u}) 0
⊢ Eq.{u + 2} (α := Cardinal.{u}) 0 1

Tactic:
exact (not_isUnit_zero h).elim

Premises used: False.elim, not_isUnit_zero
-- Module: Mathlib.SetTheory.Cardinal.Divisibility
Goal:
a : Cardinal.{u}
h : IsUnit a
ha : a ≠ 0
⊢ ∀ (y : Cardinal.{u}), a ∣ y

Tactic:
rw [isUnit_iff_forall_dvd] at h

Premises used: isUnit_iff_forall_dvd
-- Module: Mathlib.SetTheory.Cardinal.Divisibility
Goal:
a : Cardinal.{u}
h : IsUnit a
ha : a ≠ 0
h₁ : ∀ (y : Cardinal.{u}), a ∣ y
⊢ a ≠ 0

Tactic:
rw [isUnit_iff_forall_dvd] at h

Premises used: isUnit_iff_forall_dvd
-- Module: Mathlib.SetTheory.Cardinal.Divisibility
Goal:
a : Cardinal.{u}
h : ∀ (y : Cardinal.{u}), a ∣ y
ha : a ≠ 0
inr : ∀ (t : Cardinal.{u}) (ht : 1 = a * t), a = 1
⊢ a = 1

Tactic:
obtain ⟨t, ht⟩ := h 1

Premises used: OfNat.ofNat
-- Module: Mathlib.SetTheory.Cardinal.Divisibility
Goal:
a : Cardinal.{u}
h : ∀ (y : Cardinal.{u}), a ∣ y
ha : a ≠ 0
t : Cardinal.{u}
ht : 1 = a * t
inr : ∀ (ht : a = 1 ∧ t = 1), a = 1
inr₁ : ∀ (ht : a * t = 1), 1 ≤ a
inr₂ : ∀ (ht : a * t = 1), 1 ≤ t
⊢ a = 1

Tactic:
rw [eq_comm, mul_eq_one_iff_of_one_le] at ht

Premises used: mul_eq_one_iff_of_one_le, eq_comm
-- Module: Mathlib.SetTheory.Cardinal.Divisibility
Goal:
a : Cardinal.{u}
h : ∀ (y : Cardinal.{u}), a ∣ y
ha : a ≠ 0
t : Cardinal.{u}
ht : a = 1 ∧ t = 1
⊢ a = 1

Tactic:
ht.1

Premises used: And.left
-- Module: Mathlib.SetTheory.Cardinal.Divisibility
Goal:
a : Cardinal.{u}
h : ∀ (y : Cardinal.{u}), a ∣ y
ha : a ≠ 0
t : Cardinal.{u}
ht : a = 1 ∧ t = 1
⊢ a = 1

Tactic:
exact ht.1

Premises used: And.left
-- Module: Mathlib.SetTheory.Cardinal.Divisibility
Goal:
a : Cardinal.{u}
h : ∀ (y : Cardinal.{u}), a ∣ y
ha : a ≠ 0
t : Cardinal.{u}
ht : a * t = 1
⊢ 1 ≤ a

Tactic:
Cardinal.one_le_iff_ne_zero.mpr ha

Premises used: Iff.mpr, Cardinal.one_le_iff_ne_zero
-- Module: Mathlib.SetTheory.Cardinal.Divisibility
Goal:
a : Cardinal.{u}
h : ∀ (y : Cardinal.{u}), a ∣ y
ha : a ≠ 0
t : Cardinal.{u}
ht : a * t = 1
⊢ 1 ≤ a

Tactic:
exact Cardinal.one_le_iff_ne_zero.mpr ha

Premises used: Iff.mpr, Cardinal.one_le_iff_ne_zero
-- Module: Mathlib.SetTheory.Cardinal.Divisibility
Goal:
a : Cardinal.{u}
h : ∀ (y : Cardinal.{u}), a ∣ y
ha : a ≠ 0
t : Cardinal.{u}
ht : a * t = 1
inr : t ≠ 0
⊢ 1 ≤ t

Tactic:
apply Cardinal.one_le_iff_ne_zero.mpr

Premises used: Iff.mpr, Cardinal.one_le_iff_ne_zero
-- Module: Mathlib.SetTheory.Cardinal.Divisibility
Goal:
a : Cardinal.{u}
h_1 : ∀ (y : Cardinal.{u}), a ∣ y
ha : a ≠ 0
t : Cardinal.{u}
ht : a * t = 1
h : t = 0
⊢ Eq.{u + 2} (α := Cardinal.{u}) 0 1

Tactic:
rw [h, mul_zero] at ht

Premises used: MulZeroClass.mul_zero
-- Module: Mathlib.SetTheory.Cardinal.Divisibility
Goal:
a : Cardinal.{u}
h_1 : ∀ (y : Cardinal.{u}), a ∣ y
ha : a ≠ 0
t : Cardinal.{u}
ht : a * t = 1
h : t = 0
ht₁ : Eq.{u + 2} (α := Cardinal.{u}) 0 1
⊢ t = 0

Tactic:
rw [h, mul_zero] at ht

Premises used: MulZeroClass.mul_zero
-- Module: Mathlib.SetTheory.Cardinal.Divisibility
Goal:
a : Cardinal.{u}
h_1 : ∀ (y : Cardinal.{u}), a ∣ y
ha : a ≠ 0
t : Cardinal.{u}
ht : Eq.{u + 2} (α := Cardinal.{u}) 0 1
h : t = 0
⊢ False

Tactic:
zero_ne_one ht

Premises used: zero_ne_one
-- Module: Mathlib.SetTheory.Cardinal.Divisibility
Goal:
a : Cardinal.{u}
h_1 : ∀ (y : Cardinal.{u}), a ∣ y
ha : a ≠ 0
t : Cardinal.{u}
ht : Eq.{u + 2} (α := Cardinal.{u}) 0 1
h : t = 0
⊢ False

Tactic:
exact zero_ne_one ht

Premises used: zero_ne_one
-- Module: Mathlib.SetTheory.Cardinal.Divisibility
Goal:
a b : Cardinal.{u_1}
hb : b ≠ 0
hdiv : a ∣ b
obtain : ∀ (b : Cardinal.{u_1}) (hb : a * b ≠ 0), a ≤ a * b
⊢ a ≤ b

Tactic:
obtain ⟨b, rfl⟩ := hdiv

Premises used: rfl
-- Module: Mathlib.SetTheory.Cardinal.Divisibility
Goal:
a b : Cardinal.{u_1}
hb : a * b ≠ 0
h : b ≠ 0
⊢ a ≤ a * b

Tactic:
apply le_mul_right

Premises used: Cardinal.le_mul_right
-- Module: Mathlib.SetTheory.Cardinal.Divisibility
Goal:
a b : Cardinal.{u_1}
hb : a * b ≠ 0
⊢ b ≠ 0

Tactic:
simp_all
-- Module: Mathlib.SetTheory.Cardinal.Divisibility
Goal:
a b : Cardinal.{u}
ha : a ≠ 0
h : a ≤ b
hb : ℵ₀ ≤ b
⊢ a ∣ b

Tactic:
⟨b, (mul_eq_right hb h ha).symm⟩

Premises used: Cardinal.mul_eq_right, Exists.intro, Eq.symm
-- Module: Mathlib.SetTheory.Cardinal.Divisibility
Goal:
a : Cardinal.{u}
ha : ℵ₀ ≤ a
⊢ Prime a

Tactic:
⟨(aleph0_pos.trans_le ha).ne', ?_, fun b c hbc => ?_⟩

Premises used: Prime, LT.lt.ne', LT.lt.trans_le, And.intro, Cardinal.aleph0_pos
-- Module: Mathlib.SetTheory.Cardinal.Divisibility
Goal:
a : Cardinal.{u}
ha : ℵ₀ ≤ a
refine_1 : ¬IsUnit a
refine_2 : ∀ (b c : Cardinal.{u}) (hbc : a ∣ b * c), a ∣ b ∨ a ∣ c
⊢ Prime a

Tactic:
refine ⟨(aleph0_pos.trans_le ha).ne', ?_, fun b c hbc => ?_⟩
-- Module: Mathlib.SetTheory.Cardinal.Divisibility
Goal:
a : Cardinal.{u}
ha : ℵ₀ ≤ a
refine_1 : ¬a = 1
⊢ ¬IsUnit a

Tactic:
rw [isUnit_iff]

Premises used: Cardinal.isUnit_iff
-- Module: Mathlib.SetTheory.Cardinal.Divisibility
Goal:
a : Cardinal.{u}
ha : ℵ₀ ≤ a
⊢ ¬a = 1

Tactic:
(one_lt_aleph0.trans_le ha).ne'

Premises used: Cardinal.one_lt_aleph0, LT.lt.ne', LT.lt.trans_le
-- Module: Mathlib.SetTheory.Cardinal.Divisibility
Goal:
a : Cardinal.{u}
ha : ℵ₀ ≤ a
⊢ ¬a = 1

Tactic:
exact (one_lt_aleph0.trans_le ha).ne'

Premises used: Cardinal.one_lt_aleph0, LT.lt.ne', LT.lt.trans_le