awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.ModelTheory.Encoding (goal)
Goal:
L : Language
α : Type u'
l_1 : List (L.Term α)
a : α
l : List (Sum.{u', u} α ((i : ℕ) × L.Functions i))
var : listDecode ([Sum.inl a] ++ l) = Language.var a :: listDecode l
var₁ : listDecode (Sum.inl a :: l) = Language.var a :: listDecode l
⊢ listDecode (listEncode (Language.var a) ++ l) = Language.var a :: listDecode l
have var₂ : Language.var a :: listDecode l = Language.var a :: listDecode l
Tactic: rw [listEncode, singleton_append, listDecode]
-- Lean 4 proof step from Mathlib.ModelTheory.Encoding (goal)
Goal:
L : Language
α : Type u'
l_1 : List (L.Term α)
n : ℕ
f : L.Functions n
ts : Fin n → L.Term α
ih :
  ∀ (a : Fin n) (l : List (Sum.{u', u} α ((i : ℕ) × L.Functions i))),
    listDecode ((ts a).listEncode ++ l) = ts a :: listDecode l
l : List (Sum.{u', u} α ((i : ℕ) × L.Functions i))
i : Fin n
l' : List (Fin n)
l'ih : listDecode (flatMap (fun (i : Fin n) ↦ (ts i).listEncode) l' ++ l) = List.map ts l' ++ listDecode l
⊢ listDecode (flatMap (fun (i : Fin n) ↦ (ts i).listEncode) (i :: l') ++ l) = List.map ts (i :: l') ++ listDecode l
have cons : listDecode ((ts i).listEncode ++ flatMap (fun (i : Fin n) ↦ (ts i).listEncode) l' ++ l) =
  List.map ts (i :: l') ++ listDecode l
Tactic: rw [flatMap_cons, List.append_assoc, ih, map_cons, l'ih, cons_append]
-- Lean 4 proof step from Mathlib.ModelTheory.Encoding (goal)
Goal:
L : Language
α : Type u'
l_1 : List (L.Term α)
n : ℕ
f : L.Functions n
ts : Fin n → L.Term α
ih :
  ∀ (a : Fin n) (l : List (Sum.{u', u} α ((i : ℕ) × L.Functions i))),
    listDecode ((ts a).listEncode ++ l) = ts a :: listDecode l
l : List (Sum.{u', u} α ((i : ℕ) × L.Functions i))
i : Fin n
l' : List (Fin n)
l'ih : listDecode (flatMap (fun (i : Fin n) ↦ (ts i).listEncode) l' ++ l) = List.map ts l' ++ listDecode l
cons :
  listDecode ((ts i).listEncode ++ flatMap (fun (i : Fin n) ↦ (ts i).listEncode) l' ++ l) =
    List.map ts (i :: l') ++ listDecode l
⊢ listDecode (flatMap (fun (i : Fin n) ↦ (ts i).listEncode) (i :: l') ++ l) = List.map ts (i :: l') ++ listDecode l
have cons₁ : listDecode ((ts i).listEncode ++ (flatMap (fun (i : Fin n) ↦ (ts i).listEncode) l' ++ l)) =
  List.map ts (i :: l') ++ listDecode l
Tactic: rw [flatMap_cons, List.append_assoc, ih, map_cons, l'ih, cons_append]
-- Lean 4 proof step from Mathlib.ModelTheory.Encoding (goal)
Goal:
L : Language
α : Type u'
l_1 : List (L.Term α)
n : ℕ
f : L.Functions n
ts : Fin n → L.Term α
ih :
  ∀ (a : Fin n) (l : List (Sum.{u', u} α ((i : ℕ) × L.Functions i))),
    listDecode ((ts a).listEncode ++ l) = ts a :: listDecode l
l : List (Sum.{u', u} α ((i : ℕ) × L.Functions i))
i : Fin n
l' : List (Fin n)
l'ih : listDecode (flatMap (fun (i : Fin n) ↦ (ts i).listEncode) l' ++ l) = List.map ts l' ++ listDecode l
cons :
  listDecode ((ts i).listEncode ++ flatMap (fun (i : Fin n) ↦ (ts i).listEncode) l' ++ l) =
    List.map ts (i :: l') ++ listDecode l
cons₁ :
  listDecode ((ts i).listEncode ++ (flatMap (fun (i : Fin n) ↦ (ts i).listEncode) l' ++ l)) =
    List.map ts (i :: l') ++ listDecode l
⊢ listDecode (flatMap (fun (i : Fin n) ↦ (ts i).listEncode) (i :: l') ++ l) = List.map ts (i :: l') ++ listDecode l
have cons₂ : ts i :: listDecode (flatMap (fun (i : Fin n) ↦ (ts i).listEncode) l' ++ l) = List.map ts (i :: l') ++ listDecode l
Tactic: rw [flatMap_cons, List.append_assoc, ih, map_cons, l'ih, cons_append]
-- Lean 4 proof step from Mathlib.ModelTheory.Encoding (goal)
Goal:
L : Language
α : Type u'
l_1 : List (L.Term α)
n : ℕ
f : L.Functions n
ts : Fin n → L.Term α
ih :
  ∀ (a : Fin n) (l : List (Sum.{u', u} α ((i : ℕ) × L.Functions i))),
    listDecode ((ts a).listEncode ++ l) = ts a :: listDecode l
l : List (Sum.{u', u} α ((i : ℕ) × L.Functions i))
i : Fin n
l' : List (Fin n)
l'ih : listDecode (flatMap (fun (i : Fin n) ↦ (ts i).listEncode) l' ++ l) = List.map ts l' ++ listDecode l
cons :
  listDecode ((ts i).listEncode ++ flatMap (fun (i : Fin n) ↦ (ts i).listEncode) l' ++ l) =
    List.map ts (i :: l') ++ listDecode l
cons₁ :
  listDecode ((ts i).listEncode ++ (flatMap (fun (i : Fin n) ↦ (ts i).listEncode) l' ++ l)) =
    List.map ts (i :: l') ++ listDecode l
cons₂ :
  ts i :: listDecode (flatMap (fun (i : Fin n) ↦ (ts i).listEncode) l' ++ l) = List.map ts (i :: l') ++ listDecode l
⊢ listDecode (flatMap (fun (i : Fin n) ↦ (ts i).listEncode) (i :: l') ++ l) = List.map ts (i :: l') ++ listDecode l
have cons₃ : ts i :: listDecode (flatMap (fun (i : Fin n) ↦ (ts i).listEncode) l' ++ l) = ts i :: List.map ts l' ++ listDecode l
Tactic: rw [flatMap_cons, List.append_assoc, ih, map_cons, l'ih, cons_append]
-- Lean 4 proof step from Mathlib.ModelTheory.Encoding (goal)
Goal:
L : Language
α : Type u'
l_1 : List (L.Term α)
n : ℕ
f : L.Functions n
ts : Fin n → L.Term α
ih :
  ∀ (a : Fin n) (l : List (Sum.{u', u} α ((i : ℕ) × L.Functions i))),
    listDecode ((ts a).listEncode ++ l) = ts a :: listDecode l
l : List (Sum.{u', u} α ((i : ℕ) × L.Functions i))
i : Fin n
l' : List (Fin n)
l'ih : listDecode (flatMap (fun (i : Fin n) ↦ (ts i).listEncode) l' ++ l) = List.map ts l' ++ listDecode l
cons :
  listDecode ((ts i).listEncode ++ flatMap (fun (i : Fin n) ↦ (ts i).listEncode) l' ++ l) =
    List.map ts (i :: l') ++ listDecode l
cons₁ :
  listDecode ((ts i).listEncode ++ (flatMap (fun (i : Fin n) ↦ (ts i).listEncode) l' ++ l)) =
    List.map ts (i :: l') ++ listDecode l
cons₂ :
  ts i :: listDecode (flatMap (fun (i : Fin n) ↦ (ts i).listEncode) l' ++ l) = List.map ts (i :: l') ++ listDecode l
cons₃ :
  ts i :: listDecode (flatMap (fun (i : Fin n) ↦ (ts i).listEncode) l' ++ l) = ts i :: List.map ts l' ++ listDecode l
⊢ listDecode (flatMap (fun (i : Fin n) ↦ (ts i).listEncode) (i :: l') ++ l) = List.map ts (i :: l') ++ listDecode l
have cons₄ : ts i :: (List.map ts l' ++ listDecode l) = ts i :: List.map ts l' ++ listDecode l
Tactic: rw [flatMap_cons, List.append_assoc, ih, map_cons, l'ih, cons_append]
-- Lean 4 proof step from Mathlib.ModelTheory.Encoding (goal)
Goal:
L : Language
α : Type u'
l_1 : List (L.Term α)
n : ℕ
f : L.Functions n
ts : Fin n → L.Term α
ih :
  ∀ (a : Fin n) (l : List (Sum.{u', u} α ((i : ℕ) × L.Functions i))),
    listDecode ((ts a).listEncode ++ l) = ts a :: listDecode l
l : List (Sum.{u', u} α ((i : ℕ) × L.Functions i))
i : Fin n
l' : List (Fin n)
l'ih : listDecode (flatMap (fun (i : Fin n) ↦ (ts i).listEncode) l' ++ l) = List.map ts l' ++ listDecode l
cons :
  listDecode ((ts i).listEncode ++ flatMap (fun (i : Fin n) ↦ (ts i).listEncode) l' ++ l) =
    List.map ts (i :: l') ++ listDecode l
cons₁ :
  listDecode ((ts i).listEncode ++ (flatMap (fun (i : Fin n) ↦ (ts i).listEncode) l' ++ l)) =
    List.map ts (i :: l') ++ listDecode l
cons₂ :
  ts i :: listDecode (flatMap (fun (i : Fin n) ↦ (ts i).listEncode) l' ++ l) = List.map ts (i :: l') ++ listDecode l
cons₃ :
  ts i :: listDecode (flatMap (fun (i : Fin n) ↦ (ts i).listEncode) l' ++ l) = ts i :: List.map ts l' ++ listDecode l
cons₄ : ts i :: (List.map ts l' ++ listDecode l) = ts i :: List.map ts l' ++ listDecode l
⊢ listDecode (flatMap (fun (i : Fin n) ↦ (ts i).listEncode) (i :: l') ++ l) = List.map ts (i :: l') ++ listDecode l
have cons₅ : ts i :: (List.map ts l' ++ listDecode l) = ts i :: (List.map ts l' ++ listDecode l)
Tactic: rw [flatMap_cons, List.append_assoc, ih, map_cons, l'ih, cons_append]
-- Lean 4 proof step from Mathlib.ModelTheory.Encoding (goal)
Goal:
L : Language
α : Type u'
l_1 : List (L.Term α)
n : ℕ
f : L.Functions n
ts : Fin n → L.Term α
ih :
  ∀ (a : Fin n) (l : List (Sum.{u', u} α ((i : ℕ) × L.Functions i))),
    listDecode ((ts a).listEncode ++ l) = ts a :: listDecode l
l : List (Sum.{u', u} α ((i : ℕ) × L.Functions i))
⊢ listDecode (flatMap (fun (i : Fin n) ↦ (ts i).listEncode) (finRange n) ++ l) =
    List.map ts (finRange n) ++ listDecode l
have induction : ∀ (x : List (Fin n)), listDecode (flatMap (fun (i : Fin n) ↦ (ts i).listEncode) x ++ l) = List.map ts x ++ listDecode l
Tactic: induction finRange n with
      | nil => rfl
      | cons i l' l'ih => rw [flatMap_cons, List.append_assoc, ih, map_cons, l'ih, cons_append]
-- Lean 4 proof step from Mathlib.ModelTheory.Encoding (hypothesis)
Goal:
L : Language
α : Type u'
l_1 : List (L.Term α)
n : ℕ
f : L.Functions n
ts : Fin n → L.Term α
ih :
  ∀ (a : Fin n) (l : List (Sum.{u', u} α ((i : ℕ) × L.Functions i))),
    listDecode ((ts a).listEncode ++ l) = ts a :: listDecode l
l : List (Sum.{u', u} α ((i : ℕ) × L.Functions i))
⊢ (if h : n ≤ (listDecode (flatMap (fun (i : Fin n) ↦ (ts i).listEncode) (finRange n) ++ l)).length then
      (func f fun (i : Fin n) ↦
          getElem (valid := fun (xs : List (L.Term α)) (i : Fin n) ↦ (↑i : ℕ) < xs.length)
            (listDecode (flatMap (fun (i : Fin n) ↦ (ts i).listEncode) (finRange n) ++ l)) i ⋯) ::
        drop n (listDecode (flatMap (fun (i : Fin n) ↦ (ts i).listEncode) (finRange n) ++ l))
    else []) =
    func f ts :: listDecode l
have h : listDecode (flatMap (fun (i : Fin n) ↦ (ts i).listEncode) (finRange n) ++ l) = List.map ts (finRange n) ++ listDecode l
Tactic: have h : listDecode (((finRange n).flatMap fun i : Fin n => (ts i).listEncode) ++ l) =
        (finRange n).map ts ++ listDecode l := by
      induction finRange n with
      | nil => rfl
      | cons i l' l'ih => rw [flatMap_cons, List.append_assoc, ih, map_cons, l'ih, cons_append]
-- Lean 4 proof step from Mathlib.ModelTheory.Encoding (goal)
Goal:
L : Language
α : Type u'
l_1 : List (L.Term α)
n : ℕ
f : L.Functions n
ts : Fin n → L.Term α
ih :
  ∀ (a : Fin n) (l : List (Sum.{u', u} α ((i : ℕ) × L.Functions i))),
    listDecode ((ts a).listEncode ++ l) = ts a :: listDecode l
l : List (Sum.{u', u} α ((i : ℕ) × L.Functions i))
h :
  listDecode (flatMap (fun (i : Fin n) ↦ (ts i).listEncode) (finRange n) ++ l) =
    List.map ts (finRange n) ++ listDecode l
⊢ (if h : n ≤ (listDecode (flatMap (fun (i : Fin n) ↦ (ts i).listEncode) (finRange n) ++ l)).length then
      (func f fun (i : Fin n) ↦
          getElem (valid := fun (xs : List (L.Term α)) (i : Fin n) ↦ (↑i : ℕ) < xs.length)
            (listDecode (flatMap (fun (i : Fin n) ↦ (ts i).listEncode) (finRange n) ++ l)) i ⋯) ::
        drop n (listDecode (flatMap (fun (i : Fin n) ↦ (ts i).listEncode) (finRange n) ++ l))
    else []) =
    func f ts :: listDecode l
have func : (fun (i : Fin n) ↦
      getElem (valid := fun (as : List (L.Term α)) (i : ℕ) ↦ i < as.length) (List.map ts (finRange n) ++ listDecode l)
        (↑i : ℕ) sorry) =
    ts ∧
  drop n (List.map ts (finRange n) ++ listDecode l) = listDecode l
Tactic: simp only [h, length_append, length_map, length_finRange, le_add_iff_nonneg_right,
      _root_.zero_le, ↓reduceDIte, getElem_fin, cons.injEq, func.injEq, heq_eq_eq, true_and]
-- Lean 4 proof step from Mathlib.ModelTheory.Encoding (goal)
Goal:
L : Language
α : Type u'
l_1 : List (L.Term α)
n : ℕ
f : L.Functions n
ts : Fin n → L.Term α
ih :
  ∀ (a : Fin n) (l : List (Sum.{u', u} α ((i : ℕ) × L.Functions i))),
    listDecode ((ts a).listEncode ++ l) = ts a :: listDecode l
l : List (Sum.{u', u} α ((i : ℕ) × L.Functions i))
h :
  listDecode (flatMap (fun (i : Fin n) ↦ (ts i).listEncode) (finRange n) ++ l) =
    List.map ts (finRange n) ++ listDecode l
⊢ (fun (i : Fin n) ↦
        getElem (valid := fun (as : List (L.Term α)) (i : ℕ) ↦ i < as.length) (List.map ts (finRange n) ++ listDecode l)
          (↑i : ℕ) ⋯) =
      ts ∧
    drop n (List.map ts (finRange n) ++ listDecode l) = listDecode l
have func : ∀ (i : Fin n),
  getElem (valid := fun (as : List (L.Term α)) (i : ℕ) ↦ i < as.length) (List.map ts (finRange n) ++ listDecode l)
      (↑i : ℕ) sorry =
    ts i
Tactic: refine ⟨funext (fun i => ?_), ?_⟩
-- Lean 4 proof step from Mathlib.ModelTheory.Encoding (goal)
Goal:
L : Language
α : Type u'
l_1 : List (L.Term α)
n : ℕ
f : L.Functions n
ts : Fin n → L.Term α
ih :
  ∀ (a : Fin n) (l : List (Sum.{u', u} α ((i : ℕ) × L.Functions i))),
    listDecode ((ts a).listEncode ++ l) = ts a :: listDecode l
l : List (Sum.{u', u} α ((i : ℕ) × L.Functions i))
h :
  listDecode (flatMap (fun (i : Fin n) ↦ (ts i).listEncode) (finRange n) ++ l) =
    List.map ts (finRange n) ++ listDecode l
func :
  ∀ (i : Fin n),
    getElem (valid := fun (as : List (L.Term α)) (i : ℕ) ↦ i < as.length) (List.map ts (finRange n) ++ listDecode l)
        (↑i : ℕ) ⋯ =
      ts i
⊢ (fun (i : Fin n) ↦
        getElem (valid := fun (as : List (L.Term α)) (i : ℕ) ↦ i < as.length) (List.map ts (finRange n) ++ listDecode l)
          (↑i : ℕ) ⋯) =
      ts ∧
    drop n (List.map ts (finRange n) ++ listDecode l) = listDecode l
have func₁ : drop n (List.map ts (finRange n) ++ listDecode l) = listDecode l
Tactic: refine ⟨funext (fun i => ?_), ?_⟩
-- Lean 4 proof step from Mathlib.ModelTheory.Encoding (goal)
Goal:
L : Language
α : Type u'
l_1 : List (L.Term α)
t : L.Term α
l : List (Sum.{u', u} α ((i : ℕ) × L.Functions i))
⊢ listDecode (t.listEncode ++ l) = t :: listDecode l
have var : ∀ (a : α) (l : List (Sum.{u', u} α ((i : ℕ) × L.Functions i))),
  listDecode (listEncode (var a) ++ l) = var a :: listDecode l
Tactic: induction t generalizing l with
  | var => rw [listEncode, singleton_append, listDecode]
  | @func n f ts ih =>
    rw [listEncode, cons_append, listDecode]
    have h : listDecode (((finRange n).flatMap fun i : Fin n => (ts i).listEncode) ++ l) =
        (finRange n).map ts ++ listDecode l := by
      induction finRange n with
      | nil => rfl
      | cons i l' l'ih => rw [flatMap_cons, List.append_assoc, ih, map_cons, l'ih, cons_append]
    simp only [h, length_append, length_map, length_finRange, le_add_iff_nonneg_right,
      _root_.zero_le, ↓reduceDIte, getElem_fin, cons.injEq, func.injEq, heq_eq_eq, true_and]
    refine ⟨funext (fun i => ?_), ?_⟩
    · simp only [length_map, length_finRange, is_lt, getElem_append_left, getElem_map,
      getElem_finRange, cast_mk, Fin.eta]
    · simp only [length_map, length_finRange, drop_left']
Cleared hypotheses: t, l
-- Lean 4 proof step from Mathlib.ModelTheory.Encoding (goal)
Goal:
L : Language
α : Type u'
l_1 : List (L.Term α)
t : L.Term α
l : List (Sum.{u', u} α ((i : ℕ) × L.Functions i))
var :
  ∀ (a : α) (l : List (Sum.{u', u} α ((i : ℕ) × L.Functions i))),
    listDecode (listEncode (Language.var a) ++ l) = Language.var a :: listDecode l
⊢ listDecode (t.listEncode ++ l) = t :: listDecode l
have func : ∀ {n : ℕ} (f : L.Functions n) (ts : Fin n → L.Term α)
  (ih :
    ∀ (a : Fin n) (l : List (Sum.{u', u} α ((i : ℕ) × L.Functions i))),
      listDecode ((ts a).listEncode ++ l) = ts a :: listDecode l)
  (l : List (Sum.{u', u} α ((i : ℕ) × L.Functions i))),
  listDecode ((func f ts).listEncode ++ l) = func f ts :: listDecode l
Tactic: induction t generalizing l with
  | var => rw [listEncode, singleton_append, listDecode]
  | @func n f ts ih =>
    rw [listEncode, cons_append, listDecode]
    have h : listDecode (((finRange n).flatMap fun i : Fin n => (ts i).listEncode) ++ l) =
        (finRange n).map ts ++ listDecode l := by
      induction finRange n with
      | nil => rfl
      | cons i l' l'ih => rw [flatMap_cons, List.append_assoc, ih, map_cons, l'ih, cons_append]
    simp only [h, length_append, length_map, length_finRange, le_add_iff_nonneg_right,
      _root_.zero_le, ↓reduceDIte, getElem_fin, cons.injEq, func.injEq, heq_eq_eq, true_and]
    refine ⟨funext (fun i => ?_), ?_⟩
    · simp only [length_map, length_finRange, is_lt, getElem_append_left, getElem_map,
      getElem_finRange, cast_mk, Fin.eta]
    · simp only [length_map, length_finRange, drop_left']
Cleared hypotheses: t, l
-- Lean 4 proof step from Mathlib.ModelTheory.Encoding (hypothesis)
Goal:
L : Language
α : Type u'
t : L.Term α
⊢ (Option.join do
      let a ← (listDecode t.listEncode).head?
      pure (some a)) =
    some t
have h : listDecode (flatMap listEncode [t]) = [t]
Tactic: have h := listDecode_encode_list [t]
-- Lean 4 proof step from Mathlib.ModelTheory.Encoding (hypothesis)
Goal:
L : Language
α : Type u'
t : L.Term α
h : listDecode (flatMap listEncode [t]) = [t]
⊢ (Option.join do
      let a ← (listDecode t.listEncode).head?
      pure (some a)) =
    some t
have h₁ : listDecode t.listEncode = [t]
Tactic: rw [flatMap_singleton] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.ModelTheory.Encoding (goal)
Goal:
L : Language
α : Type u'
⊢ #((n : ℕ) × Term.{u, v, u'} L (α ⊕ Fin n)) = max ℵ₀ #(Sum.{u', u} α ((i : ℕ) × L.Functions i))
have refine_1 : #((n : ℕ) × Term.{u, v, u'} L (α ⊕ Fin n)) ≤ max ℵ₀ #(Sum.{u', u} α ((i : ℕ) × L.Functions i))
Tactic: refine le_antisymm ?_ ?_
-- Lean 4 proof step from Mathlib.ModelTheory.Encoding (goal)
Goal:
L : Language
α : Type u'
refine_1 : #((n : ℕ) × Term.{u, v, u'} L (α ⊕ Fin n)) ≤ max ℵ₀ #(Sum.{u', u} α ((i : ℕ) × L.Functions i))
⊢ #((n : ℕ) × Term.{u, v, u'} L (α ⊕ Fin n)) = max ℵ₀ #(Sum.{u', u} α ((i : ℕ) × L.Functions i))
have refine_2 : max ℵ₀ #(Sum.{u', u} α ((i : ℕ) × L.Functions i)) ≤ #((n : ℕ) × Term.{u, v, u'} L (α ⊕ Fin n))
Tactic: refine le_antisymm ?_ ?_
-- Lean 4 proof step from Mathlib.ModelTheory.Encoding (goal)
Goal:
L : Language
α : Type u'
⊢ #((n : ℕ) × Term.{u, v, u'} L (α ⊕ Fin n)) ≤ max ℵ₀ #(Sum.{u', u} α ((i : ℕ) × L.Functions i))
have refine_1 : (Cardinal.sum fun (i : ℕ) ↦ #(Term.{u, v, u'} L (α ⊕ Fin i))) ≤ max ℵ₀ #(Sum.{u', u} α ((i : ℕ) × L.Functions i))
Tactic: rw [mk_sigma]
-- Lean 4 proof step from Mathlib.ModelTheory.Encoding (goal)
Goal:
L : Language
α : Type u'
⊢ (Cardinal.sum fun (i : ℕ) ↦ #(Term.{u, v, u'} L (α ⊕ Fin i))) ≤ max ℵ₀ #(Sum.{u', u} α ((i : ℕ) × L.Functions i))
have refine_1 : lift.{max u u', 0} #ℕ * ⨆ (i : ℕ), #(Term.{u, v, u'} L (α ⊕ Fin i)) ≤ max ℵ₀ #(Sum.{u', u} α ((i : ℕ) × L.Functions i))
Tactic: refine (sum_le_lift_mk_mul_iSup _).trans ?_
-- Lean 4 proof step from Mathlib.ModelTheory.Encoding (goal)
Goal:
L : Language
α : Type u'
⊢ lift.{max u u', 0} #ℕ * ⨆ (i : ℕ), #(Term.{u, v, u'} L (α ⊕ Fin i)) ≤
    max ℵ₀ #(Sum.{u', u} α ((i : ℕ) × L.Functions i))
have refine_1 : ℵ₀ ≤ max ℵ₀ #(Sum.{u', u} α ((i : ℕ) × L.Functions i)) ∧
  ∀ (i : ℕ), #(Term.{u, v, u'} L (α ⊕ Fin i)) ≤ max ℵ₀ #(Sum.{u', u} α ((i : ℕ) × L.Functions i))
Tactic: rw [mk_nat, lift_aleph0, mul_eq_max_of_aleph0_le_left le_rfl, max_le_iff,
      ciSup_le_iff' bddAbove_of_small]
-- Lean 4 proof step from Mathlib.ModelTheory.Encoding (goal)
Goal:
L : Language
α : Type u'
refine_1 :
  ℵ₀ ≤ max ℵ₀ #(Sum.{u', u} α ((i : ℕ) × L.Functions i)) ∧
    ∀ (i : ℕ), #(Term.{u, v, u'} L (α ⊕ Fin i)) ≤ max ℵ₀ #(Sum.{u', u} α ((i : ℕ) × L.Functions i))
⊢ lift.{max u u', 0} #ℕ * ⨆ (i : ℕ), #(Term.{u, v, u'} L (α ⊕ Fin i)) ≤
    max ℵ₀ #(Sum.{u', u} α ((i : ℕ) × L.Functions i))
have refine_1₁ : Ne (α := Cardinal.{max u u'}) (⨆ (i : ℕ), #(Term.{u, v, u'} L (α ⊕ Fin i))) 0
Tactic: rw [mk_nat, lift_aleph0, mul_eq_max_of_aleph0_le_left le_rfl, max_le_iff,
      ciSup_le_iff' bddAbove_of_small]
-- Lean 4 proof step from Mathlib.ModelTheory.Encoding (goal)
Goal:
L : Language
α : Type u'
⊢ ℵ₀ ≤ max ℵ₀ #(Sum.{u', u} α ((i : ℕ) × L.Functions i)) ∧
    ∀ (i : ℕ), #(Term.{u, v, u'} L (α ⊕ Fin i)) ≤ max ℵ₀ #(Sum.{u', u} α ((i : ℕ) × L.Functions i))
have refine_1 : ∀ (i : ℕ),
  max ℵ₀ #(Sum.{u', u} (α ⊕ Fin i) ((i : ℕ) × L.Functions i)) ≤ max ℵ₀ #(Sum.{u', u} α ((i : ℕ) × L.Functions i))
Tactic: refine ⟨le_max_left _ _, fun i => card_le.trans ?_⟩
-- Lean 4 proof step from Mathlib.ModelTheory.Encoding (goal)
Goal:
L : Language
α : Type u'
i : ℕ
⊢ max ℵ₀ #(Sum.{u', u} (α ⊕ Fin i) ((i : ℕ) × L.Functions i)) ≤ max ℵ₀ #(Sum.{u', u} α ((i : ℕ) × L.Functions i))
have refine_1 : #(Sum.{u', u} (α ⊕ Fin i) ((i : ℕ) × L.Functions i)) ≤ max ℵ₀ #(Sum.{u', u} α ((i : ℕ) × L.Functions i))
Tactic: refine max_le (le_max_left _ _) ?_
-- Lean 4 proof step from Mathlib.ModelTheory.Encoding (goal)
Goal:
L : Language
α : Type u'
i : ℕ
⊢ #(Sum.{u', u} (α ⊕ Fin i) ((i : ℕ) × L.Functions i)) ≤ max ℵ₀ #(Sum.{u', u} α ((i : ℕ) × L.Functions i))
have refine_1 : #(Sum.{u', u} (α ⊕ Fin i) ((i : ℕ) × L.Functions i)) ≤ ℵ₀ + #(Sum.{u', u} α ((i : ℕ) × L.Functions i))
Tactic: grw [← add_eq_max le_rfl, mk_sum, mk_sum, mk_sum, add_comm (Cardinal.lift #α), lift_add,
        add_assoc, lift_lift, lift_lift, mk_fin, lift_natCast, natCast_lt_aleph0]
-- Lean 4 proof step from Mathlib.ModelTheory.Encoding (goal)
Goal:
L : Language
α : Type u'
i : ℕ
refine_1 : #(Sum.{u', u} (α ⊕ Fin i) ((i : ℕ) × L.Functions i)) ≤ ℵ₀ + #(Sum.{u', u} α ((i : ℕ) × L.Functions i))
⊢ #(Sum.{u', u} (α ⊕ Fin i) ((i : ℕ) × L.Functions i)) ≤ max ℵ₀ #(Sum.{u', u} α ((i : ℕ) × L.Functions i))
have refine_1₁ : lift.{u, u'} #(α ⊕ Fin i) + lift.{u', u} #((i : ℕ) × L.Functions i) ≤ ℵ₀ + #(Sum.{u', u} α ((i : ℕ) × L.Functions i))
Tactic: grw [← add_eq_max le_rfl, mk_sum, mk_sum, mk_sum, add_comm (Cardinal.lift #α), lift_add,
        add_assoc, lift_lift, lift_lift, mk_fin, lift_natCast, natCast_lt_aleph0]
-- Lean 4 proof step from Mathlib.ModelTheory.Encoding (goal)
Goal:
L : Language
α : Type u'
i : ℕ
refine_1 : #(Sum.{u', u} (α ⊕ Fin i) ((i : ℕ) × L.Functions i)) ≤ ℵ₀ + #(Sum.{u', u} α ((i : ℕ) × L.Functions i))
refine_1₁ :
  lift.{u, u'} #(α ⊕ Fin i) + lift.{u', u} #((i : ℕ) × L.Functions i) ≤ ℵ₀ + #(Sum.{u', u} α ((i : ℕ) × L.Functions i))
⊢ #(Sum.{u', u} (α ⊕ Fin i) ((i : ℕ) × L.Functions i)) ≤ max ℵ₀ #(Sum.{u', u} α ((i : ℕ) × L.Functions i))
have refine_1₂ : lift.{u, u'} (lift.{0, u'} #α + lift.{u', 0} #(Fin i)) + lift.{u', u} #((i : ℕ) × L.Functions i) ≤
  ℵ₀ + #(Sum.{u', u} α ((i : ℕ) × L.Functions i))
Tactic: grw [← add_eq_max le_rfl, mk_sum, mk_sum, mk_sum, add_comm (Cardinal.lift #α), lift_add,
        add_assoc, lift_lift, lift_lift, mk_fin, lift_natCast, natCast_lt_aleph0]
-- Lean 4 proof step from Mathlib.ModelTheory.Encoding (goal)
Goal:
L : Language
α : Type u'
i : ℕ
refine_1 : #(Sum.{u', u} (α ⊕ Fin i) ((i : ℕ) × L.Functions i)) ≤ ℵ₀ + #(Sum.{u', u} α ((i : ℕ) × L.Functions i))
refine_1₁ :
  lift.{u, u'} #(α ⊕ Fin i) + lift.{u', u} #((i : ℕ) × L.Functions i) ≤ ℵ₀ + #(Sum.{u', u} α ((i : ℕ) × L.Functions i))
refine_1₂ :
  lift.{u, u'} (lift.{0, u'} #α + lift.{u', 0} #(Fin i)) + lift.{u', u} #((i : ℕ) × L.Functions i) ≤
    ℵ₀ + #(Sum.{u', u} α ((i : ℕ) × L.Functions i))
⊢ #(Sum.{u', u} (α ⊕ Fin i) ((i : ℕ) × L.Functions i)) ≤ max ℵ₀ #(Sum.{u', u} α ((i : ℕ) × L.Functions i))
have refine_1₃ : lift.{u, u'} (lift.{0, u'} #α + lift.{u', 0} #(Fin i)) + lift.{u', u} #((i : ℕ) × L.Functions i) ≤
  ℵ₀ + (lift.{u, u'} #α + lift.{u', u} #((i : ℕ) × L.Functions i))
Tactic: grw [← add_eq_max le_rfl, mk_sum, mk_sum, mk_sum, add_comm (Cardinal.lift #α), lift_add,
        add_assoc, lift_lift, lift_lift, mk_fin, lift_natCast, natCast_lt_aleph0]
-- Lean 4 proof step from Mathlib.ModelTheory.Encoding (goal)
Goal:
L : Language
α : Type u'
i : ℕ
refine_1 : #(Sum.{u', u} (α ⊕ Fin i) ((i : ℕ) × L.Functions i)) ≤ ℵ₀ + #(Sum.{u', u} α ((i : ℕ) × L.Functions i))
refine_1₁ :
  lift.{u, u'} #(α ⊕ Fin i) + lift.{u', u} #((i : ℕ) × L.Functions i) ≤ ℵ₀ + #(Sum.{u', u} α ((i : ℕ) × L.Functions i))
refine_1₂ :
  lift.{u, u'} (lift.{0, u'} #α + lift.{u', 0} #(Fin i)) + lift.{u', u} #((i : ℕ) × L.Functions i) ≤
    ℵ₀ + #(Sum.{u', u} α ((i : ℕ) × L.Functions i))
refine_1₃ :
  lift.{u, u'} (lift.{0, u'} #α + lift.{u', 0} #(Fin i)) + lift.{u', u} #((i : ℕ) × L.Functions i) ≤
    ℵ₀ + (lift.{u, u'} #α + lift.{u', u} #((i : ℕ) × L.Functions i))
⊢ #(Sum.{u', u} (α ⊕ Fin i) ((i : ℕ) × L.Functions i)) ≤ max ℵ₀ #(Sum.{u', u} α ((i : ℕ) × L.Functions i))
have refine_1₄ : lift.{u, u'} (lift.{u', 0} #(Fin i) + lift.{0, u'} #α) + lift.{u', u} #((i : ℕ) × L.Functions i) ≤
  ℵ₀ + (lift.{u, u'} #α + lift.{u', u} #((i : ℕ) × L.Functions i))
Tactic: grw [← add_eq_max le_rfl, mk_sum, mk_sum, mk_sum, add_comm (Cardinal.lift #α), lift_add,
        add_assoc, lift_lift, lift_lift, mk_fin, lift_natCast, natCast_lt_aleph0]