awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.ModelTheory.LanguageMap (goal)
Goal:
L : Language
L' : Language
ϕ : L →ᴸ L'
inst :
  (n : ℕ) →
    (f : L'.Functions n) →
      Decidable (Membership.mem (γ := Set (L'.Functions n)) (Set.range fun (f : L.Functions n) ↦ ϕ.onFunction f) f)
inst_1 :
  (n : ℕ) →
    (r : L'.Relations n) →
      Decidable (Membership.mem (γ := Set (L'.Relations n)) (Set.range fun (r : L.Relations n) ↦ ϕ.onRelation r) r)
h : ϕ.Injective
M : Type u_1
inst_2 : Inhabited M
inst_3 : L.Structure M
this : L'.Structure M := ϕ.defaultExpansion M
⊢ ϕ.IsExpansionOn M
have refine_1 : ∀ {n : ℕ} (f : L.Functions n) (xs : Fin n → M), funMap (ϕ.onFunction f) xs = funMap f xs
Tactic: refine ⟨fun {n} f xs => ?_, fun {n} r xs => ?_⟩
-- Lean 4 proof step from Mathlib.ModelTheory.LanguageMap (goal)
Goal:
L : Language
L' : Language
ϕ : L →ᴸ L'
inst :
  (n : ℕ) →
    (f : L'.Functions n) →
      Decidable (Membership.mem (γ := Set (L'.Functions n)) (Set.range fun (f : L.Functions n) ↦ ϕ.onFunction f) f)
inst_1 :
  (n : ℕ) →
    (r : L'.Relations n) →
      Decidable (Membership.mem (γ := Set (L'.Relations n)) (Set.range fun (r : L.Relations n) ↦ ϕ.onRelation r) r)
h : ϕ.Injective
M : Type u_1
inst_2 : Inhabited M
inst_3 : L.Structure M
this : L'.Structure M := ϕ.defaultExpansion M
refine_1 : ∀ {n : ℕ} (f : L.Functions n) (xs : Fin n → M), funMap (ϕ.onFunction f) xs = funMap f xs
⊢ ϕ.IsExpansionOn M
have refine_2 : ∀ {n : ℕ} (r : L.Relations n) (xs : Fin n → M), RelMap (ϕ.onRelation r) xs = RelMap r xs
Tactic: refine ⟨fun {n} f xs => ?_, fun {n} r xs => ?_⟩
-- Lean 4 proof step from Mathlib.ModelTheory.LanguageMap (hypothesis)
Goal:
L : Language
L' : Language
ϕ : L →ᴸ L'
inst :
  (n : ℕ) →
    (f : L'.Functions n) →
      Decidable (Membership.mem (γ := Set (L'.Functions n)) (Set.range fun (f : L.Functions n) ↦ ϕ.onFunction f) f)
inst_1 :
  (n : ℕ) →
    (r : L'.Relations n) →
      Decidable (Membership.mem (γ := Set (L'.Relations n)) (Set.range fun (r : L.Relations n) ↦ ϕ.onRelation r) r)
h : ϕ.Injective
M : Type u_1
inst_2 : Inhabited M
inst_3 : L.Structure M
this : L'.Structure M := ϕ.defaultExpansion M
n : ℕ
f : L.Functions n
xs : Fin n → M
⊢ funMap (ϕ.onFunction f) xs = funMap f xs
have hf : Membership.mem (γ := Set (L'.Functions n)) (Set.range fun (f : L.Functions n) ↦ ϕ.onFunction f) (ϕ.onFunction f)
Tactic: have hf : ϕ.onFunction f ∈ Set.range fun f : L.Functions n => ϕ.onFunction f := ⟨f, rfl⟩
-- Lean 4 proof step from Mathlib.ModelTheory.LanguageMap (goal)
Goal:
L : Language
L' : Language
ϕ : L →ᴸ L'
inst :
  (n : ℕ) →
    (f : L'.Functions n) →
      Decidable (Membership.mem (γ := Set (L'.Functions n)) (Set.range fun (f : L.Functions n) ↦ ϕ.onFunction f) f)
inst_1 :
  (n : ℕ) →
    (r : L'.Relations n) →
      Decidable (Membership.mem (γ := Set (L'.Relations n)) (Set.range fun (r : L.Relations n) ↦ ϕ.onRelation r) r)
h : ϕ.Injective
M : Type u_1
inst_2 : Inhabited M
inst_3 : L.Structure M
this : L'.Structure M := ϕ.defaultExpansion M
n : ℕ
f : L.Functions n
xs : Fin n → M
hf : Membership.mem (γ := Set (L'.Functions n)) (Set.range fun (f : L.Functions n) ↦ ϕ.onFunction f) (ϕ.onFunction f)
⊢ funMap (ϕ.onFunction f) xs = funMap f xs
have refine_1 : funMap (Exists.choose (p := fun (y : L.Functions n) ↦ (fun (f : L.Functions n) ↦ ϕ.onFunction f) y = ϕ.onFunction f) hf)
    xs =
  funMap f xs
Tactic: refine (dif_pos hf).trans ?_
-- Lean 4 proof step from Mathlib.ModelTheory.LanguageMap (goal)
Goal:
L : Language
L' : Language
ϕ : L →ᴸ L'
inst :
  (n : ℕ) →
    (f : L'.Functions n) →
      Decidable (Membership.mem (γ := Set (L'.Functions n)) (Set.range fun (f : L.Functions n) ↦ ϕ.onFunction f) f)
inst_1 :
  (n : ℕ) →
    (r : L'.Relations n) →
      Decidable (Membership.mem (γ := Set (L'.Relations n)) (Set.range fun (r : L.Relations n) ↦ ϕ.onRelation r) r)
h : ϕ.Injective
M : Type u_1
inst_2 : Inhabited M
inst_3 : L.Structure M
this : L'.Structure M := ϕ.defaultExpansion M
n : ℕ
f : L.Functions n
xs : Fin n → M
hf : Membership.mem (γ := Set (L'.Functions n)) (Set.range fun (f : L.Functions n) ↦ ϕ.onFunction f) (ϕ.onFunction f)
⊢ funMap
      (Exists.choose (p := fun (y : L.Functions n) ↦ (fun (f : L.Functions n) ↦ ϕ.onFunction f) y = ϕ.onFunction f) hf)
      xs =
    funMap f xs
have refine_1 : funMap f xs = funMap f xs
Tactic: rw [h.onFunction hf.choose_spec]
-- Lean 4 proof step from Mathlib.ModelTheory.LanguageMap (hypothesis)
Goal:
L : Language
L' : Language
ϕ : L →ᴸ L'
inst :
  (n : ℕ) →
    (f : L'.Functions n) →
      Decidable (Membership.mem (γ := Set (L'.Functions n)) (Set.range fun (f : L.Functions n) ↦ ϕ.onFunction f) f)
inst_1 :
  (n : ℕ) →
    (r : L'.Relations n) →
      Decidable (Membership.mem (γ := Set (L'.Relations n)) (Set.range fun (r : L.Relations n) ↦ ϕ.onRelation r) r)
h : ϕ.Injective
M : Type u_1
inst_2 : Inhabited M
inst_3 : L.Structure M
this : L'.Structure M := ϕ.defaultExpansion M
n : ℕ
r : L.Relations n
xs : Fin n → M
⊢ RelMap (ϕ.onRelation r) xs = RelMap r xs
have hr : Membership.mem (γ := Set (L'.Relations n)) (Set.range fun (r : L.Relations n) ↦ ϕ.onRelation r) (ϕ.onRelation r)
Tactic: have hr : ϕ.onRelation r ∈ Set.range fun r : L.Relations n => ϕ.onRelation r := ⟨r, rfl⟩
-- Lean 4 proof step from Mathlib.ModelTheory.LanguageMap (goal)
Goal:
L : Language
L' : Language
ϕ : L →ᴸ L'
inst :
  (n : ℕ) →
    (f : L'.Functions n) →
      Decidable (Membership.mem (γ := Set (L'.Functions n)) (Set.range fun (f : L.Functions n) ↦ ϕ.onFunction f) f)
inst_1 :
  (n : ℕ) →
    (r : L'.Relations n) →
      Decidable (Membership.mem (γ := Set (L'.Relations n)) (Set.range fun (r : L.Relations n) ↦ ϕ.onRelation r) r)
h : ϕ.Injective
M : Type u_1
inst_2 : Inhabited M
inst_3 : L.Structure M
this : L'.Structure M := ϕ.defaultExpansion M
n : ℕ
r : L.Relations n
xs : Fin n → M
hr : Membership.mem (γ := Set (L'.Relations n)) (Set.range fun (r : L.Relations n) ↦ ϕ.onRelation r) (ϕ.onRelation r)
⊢ RelMap (ϕ.onRelation r) xs = RelMap r xs
have refine_2 : RelMap (Exists.choose (p := fun (y : L.Relations n) ↦ (fun (r : L.Relations n) ↦ ϕ.onRelation r) y = ϕ.onRelation r) hr)
    xs =
  RelMap r xs
Tactic: refine (dif_pos hr).trans ?_
-- Lean 4 proof step from Mathlib.ModelTheory.LanguageMap (goal)
Goal:
L : Language
L' : Language
ϕ : L →ᴸ L'
inst :
  (n : ℕ) →
    (f : L'.Functions n) →
      Decidable (Membership.mem (γ := Set (L'.Functions n)) (Set.range fun (f : L.Functions n) ↦ ϕ.onFunction f) f)
inst_1 :
  (n : ℕ) →
    (r : L'.Relations n) →
      Decidable (Membership.mem (γ := Set (L'.Relations n)) (Set.range fun (r : L.Relations n) ↦ ϕ.onRelation r) r)
h : ϕ.Injective
M : Type u_1
inst_2 : Inhabited M
inst_3 : L.Structure M
this : L'.Structure M := ϕ.defaultExpansion M
n : ℕ
r : L.Relations n
xs : Fin n → M
hr : Membership.mem (γ := Set (L'.Relations n)) (Set.range fun (r : L.Relations n) ↦ ϕ.onRelation r) (ϕ.onRelation r)
⊢ RelMap
      (Exists.choose (p := fun (y : L.Relations n) ↦ (fun (r : L.Relations n) ↦ ϕ.onRelation r) y = ϕ.onRelation r) hr)
      xs =
    RelMap r xs
have refine_2 : RelMap r xs = RelMap r xs
Tactic: rw [h.onRelation hr.choose_spec]
-- Lean 4 proof step from Mathlib.ModelTheory.LanguageMap (goal)
Goal:
L : Language
L' : Language
M : Type w
inst : L.Structure M
L'' : Language
e'_1 : L' ≃ᴸ L''
e_1 e : L ≃ᴸ L'
e' : L' ≃ᴸ L''
⊢ (e.invLHom.comp e'.invLHom).comp (e'.toLHom.comp e.toLHom) = LHom.id L
have rw : e.invLHom.comp (e'.invLHom.comp (e'.toLHom.comp e.toLHom)) = LHom.id L
Tactic: rw [LHom.comp_assoc, ← LHom.comp_assoc e'.invLHom, e'.left_inv, LHom.id_comp, e.left_inv]
-- Lean 4 proof step from Mathlib.ModelTheory.LanguageMap (goal)
Goal:
L : Language
L' : Language
M : Type w
inst : L.Structure M
L'' : Language
e'_1 : L' ≃ᴸ L''
e_1 e : L ≃ᴸ L'
e' : L' ≃ᴸ L''
rw : e.invLHom.comp (e'.invLHom.comp (e'.toLHom.comp e.toLHom)) = LHom.id L
⊢ (e.invLHom.comp e'.invLHom).comp (e'.toLHom.comp e.toLHom) = LHom.id L
have rw₁ : e.invLHom.comp ((e'.invLHom.comp e'.toLHom).comp e.toLHom) = LHom.id L
Tactic: rw [LHom.comp_assoc, ← LHom.comp_assoc e'.invLHom, e'.left_inv, LHom.id_comp, e.left_inv]
-- Lean 4 proof step from Mathlib.ModelTheory.LanguageMap (goal)
Goal:
L : Language
L' : Language
M : Type w
inst : L.Structure M
L'' : Language
e'_1 : L' ≃ᴸ L''
e_1 e : L ≃ᴸ L'
e' : L' ≃ᴸ L''
rw : e.invLHom.comp (e'.invLHom.comp (e'.toLHom.comp e.toLHom)) = LHom.id L
rw₁ : e.invLHom.comp ((e'.invLHom.comp e'.toLHom).comp e.toLHom) = LHom.id L
⊢ (e.invLHom.comp e'.invLHom).comp (e'.toLHom.comp e.toLHom) = LHom.id L
have rw₂ : e.invLHom.comp ((LHom.id L').comp e.toLHom) = LHom.id L
Tactic: rw [LHom.comp_assoc, ← LHom.comp_assoc e'.invLHom, e'.left_inv, LHom.id_comp, e.left_inv]
-- Lean 4 proof step from Mathlib.ModelTheory.LanguageMap (goal)
Goal:
L : Language
L' : Language
M : Type w
inst : L.Structure M
L'' : Language
e'_1 : L' ≃ᴸ L''
e_1 e : L ≃ᴸ L'
e' : L' ≃ᴸ L''
rw : e.invLHom.comp (e'.invLHom.comp (e'.toLHom.comp e.toLHom)) = LHom.id L
rw₁ : e.invLHom.comp ((e'.invLHom.comp e'.toLHom).comp e.toLHom) = LHom.id L
rw₂ : e.invLHom.comp ((LHom.id L').comp e.toLHom) = LHom.id L
⊢ (e.invLHom.comp e'.invLHom).comp (e'.toLHom.comp e.toLHom) = LHom.id L
have rw₃ : e.invLHom.comp e.toLHom = LHom.id L
Tactic: rw [LHom.comp_assoc, ← LHom.comp_assoc e'.invLHom, e'.left_inv, LHom.id_comp, e.left_inv]
-- Lean 4 proof step from Mathlib.ModelTheory.LanguageMap (goal)
Goal:
L : Language
L' : Language
M : Type w
inst : L.Structure M
L'' : Language
e'_1 : L' ≃ᴸ L''
e_1 e : L ≃ᴸ L'
e' : L' ≃ᴸ L''
rw : e.invLHom.comp (e'.invLHom.comp (e'.toLHom.comp e.toLHom)) = LHom.id L
rw₁ : e.invLHom.comp ((e'.invLHom.comp e'.toLHom).comp e.toLHom) = LHom.id L
rw₂ : e.invLHom.comp ((LHom.id L').comp e.toLHom) = LHom.id L
rw₃ : e.invLHom.comp e.toLHom = LHom.id L
⊢ (e.invLHom.comp e'.invLHom).comp (e'.toLHom.comp e.toLHom) = LHom.id L
have rw₄ : LHom.id L = LHom.id L
Tactic: rw [LHom.comp_assoc, ← LHom.comp_assoc e'.invLHom, e'.left_inv, LHom.id_comp, e.left_inv]
-- Lean 4 proof step from Mathlib.ModelTheory.LanguageMap (goal)
Goal:
L : Language
L' : Language
M : Type w
inst : L.Structure M
L'' : Language
e'_1 : L' ≃ᴸ L''
e_1 e : L ≃ᴸ L'
e' : L' ≃ᴸ L''
⊢ (e'.toLHom.comp e.toLHom).comp (e.invLHom.comp e'.invLHom) = LHom.id L''
have rw : e'.toLHom.comp (e.toLHom.comp (e.invLHom.comp e'.invLHom)) = LHom.id L''
Tactic: rw [LHom.comp_assoc, ← LHom.comp_assoc e.toLHom, e.right_inv, LHom.id_comp, e'.right_inv]
-- Lean 4 proof step from Mathlib.ModelTheory.LanguageMap (goal)
Goal:
L : Language
L' : Language
M : Type w
inst : L.Structure M
L'' : Language
e'_1 : L' ≃ᴸ L''
e_1 e : L ≃ᴸ L'
e' : L' ≃ᴸ L''
rw : e'.toLHom.comp (e.toLHom.comp (e.invLHom.comp e'.invLHom)) = LHom.id L''
⊢ (e'.toLHom.comp e.toLHom).comp (e.invLHom.comp e'.invLHom) = LHom.id L''
have rw₁ : e'.toLHom.comp ((e.toLHom.comp e.invLHom).comp e'.invLHom) = LHom.id L''
Tactic: rw [LHom.comp_assoc, ← LHom.comp_assoc e.toLHom, e.right_inv, LHom.id_comp, e'.right_inv]
-- Lean 4 proof step from Mathlib.ModelTheory.LanguageMap (goal)
Goal:
L : Language
L' : Language
M : Type w
inst : L.Structure M
L'' : Language
e'_1 : L' ≃ᴸ L''
e_1 e : L ≃ᴸ L'
e' : L' ≃ᴸ L''
rw : e'.toLHom.comp (e.toLHom.comp (e.invLHom.comp e'.invLHom)) = LHom.id L''
rw₁ : e'.toLHom.comp ((e.toLHom.comp e.invLHom).comp e'.invLHom) = LHom.id L''
⊢ (e'.toLHom.comp e.toLHom).comp (e.invLHom.comp e'.invLHom) = LHom.id L''
have rw₂ : e'.toLHom.comp ((LHom.id L').comp e'.invLHom) = LHom.id L''
Tactic: rw [LHom.comp_assoc, ← LHom.comp_assoc e.toLHom, e.right_inv, LHom.id_comp, e'.right_inv]
-- Lean 4 proof step from Mathlib.ModelTheory.LanguageMap (goal)
Goal:
L : Language
L' : Language
M : Type w
inst : L.Structure M
L'' : Language
e'_1 : L' ≃ᴸ L''
e_1 e : L ≃ᴸ L'
e' : L' ≃ᴸ L''
rw : e'.toLHom.comp (e.toLHom.comp (e.invLHom.comp e'.invLHom)) = LHom.id L''
rw₁ : e'.toLHom.comp ((e.toLHom.comp e.invLHom).comp e'.invLHom) = LHom.id L''
rw₂ : e'.toLHom.comp ((LHom.id L').comp e'.invLHom) = LHom.id L''
⊢ (e'.toLHom.comp e.toLHom).comp (e.invLHom.comp e'.invLHom) = LHom.id L''
have rw₃ : e'.toLHom.comp e'.invLHom = LHom.id L''
Tactic: rw [LHom.comp_assoc, ← LHom.comp_assoc e.toLHom, e.right_inv, LHom.id_comp, e'.right_inv]
-- Lean 4 proof step from Mathlib.ModelTheory.LanguageMap (goal)
Goal:
L : Language
L' : Language
M : Type w
inst : L.Structure M
L'' : Language
e'_1 : L' ≃ᴸ L''
e_1 e : L ≃ᴸ L'
e' : L' ≃ᴸ L''
rw : e'.toLHom.comp (e.toLHom.comp (e.invLHom.comp e'.invLHom)) = LHom.id L''
rw₁ : e'.toLHom.comp ((e.toLHom.comp e.invLHom).comp e'.invLHom) = LHom.id L''
rw₂ : e'.toLHom.comp ((LHom.id L').comp e'.invLHom) = LHom.id L''
rw₃ : e'.toLHom.comp e'.invLHom = LHom.id L''
⊢ (e'.toLHom.comp e.toLHom).comp (e.invLHom.comp e'.invLHom) = LHom.id L''
have rw₄ : LHom.id L'' = LHom.id L''
Tactic: rw [LHom.comp_assoc, ← LHom.comp_assoc e.toLHom, e.right_inv, LHom.id_comp, e'.right_inv]
-- Lean 4 proof step from Mathlib.ModelTheory.LanguageMap (goal)
Goal:
L : Language
α : Type w'
⊢ L[[α]].card = lift.{w', max u v} L.card + lift.{max u v, w'} #α
have rw : (Language.sum.{u, v, w', 0} L (constantsOn α)).card = lift.{w', max u v} L.card + lift.{max u v, w'} #α
Tactic: rw [withConstants, card_sum, card_constantsOn]
-- Lean 4 proof step from Mathlib.ModelTheory.LanguageMap (goal)
Goal:
L : Language
α : Type w'
rw : (Language.sum.{u, v, w', 0} L (constantsOn α)).card = lift.{w', max u v} L.card + lift.{max u v, w'} #α
⊢ L[[α]].card = lift.{w', max u v} L.card + lift.{max u v, w'} #α
have rw₁ : lift.{w', max u v} L.card + lift.{max u v, w'} (constantsOn α).card = lift.{w', max u v} L.card + lift.{max u v, w'} #α
Tactic: rw [withConstants, card_sum, card_constantsOn]
-- Lean 4 proof step from Mathlib.ModelTheory.LanguageMap (goal)
Goal:
L : Language
α : Type w'
rw : (Language.sum.{u, v, w', 0} L (constantsOn α)).card = lift.{w', max u v} L.card + lift.{max u v, w'} #α
rw₁ :
  lift.{w', max u v} L.card + lift.{max u v, w'} (constantsOn α).card =
    lift.{w', max u v} L.card + lift.{max u v, w'} #α
⊢ L[[α]].card = lift.{w', max u v} L.card + lift.{max u v, w'} #α
have rw₂ : lift.{w', max u v} L.card + lift.{max u v, w'} #α = lift.{w', max u v} L.card + lift.{max u v, w'} #α
Tactic: rw [withConstants, card_sum, card_constantsOn]
-- Lean 4 proof step from Mathlib.ModelTheory.LanguageMap (goal)
Goal:
L : Language
L' : Language
M : Type w
inst : L.Structure M
α : Type w'
ie : IsEmpty α
⊢ LHom.comp ((LHom.id L).sumElim (LHom.ofIsEmpty (constantsOn α) L)) (L.lhomWithConstants α) = LHom.id L
have rw : LHom.comp (L' := L[[α]]) ((LHom.id L).sumElim (LHom.ofIsEmpty (constantsOn α) L)) LHom.sumInl = LHom.id L
Tactic: rw [lhomWithConstants, LHom.sumElim_comp_inl]
-- Lean 4 proof step from Mathlib.ModelTheory.LanguageMap (goal)
Goal:
L : Language
L' : Language
M : Type w
inst : L.Structure M
α : Type w'
ie : IsEmpty α
rw : LHom.comp (L' := L[[α]]) ((LHom.id L).sumElim (LHom.ofIsEmpty (constantsOn α) L)) LHom.sumInl = LHom.id L
⊢ LHom.comp ((LHom.id L).sumElim (LHom.ofIsEmpty (constantsOn α) L)) (L.lhomWithConstants α) = LHom.id L
have rw₁ : LHom.id L = LHom.id L
Tactic: rw [lhomWithConstants, LHom.sumElim_comp_inl]
-- Lean 4 proof step from Mathlib.ModelTheory.LanguageMap (goal)
Goal:
L : Language
L' : Language
M : Type w
inst : L.Structure M
α : Type w'
ie : IsEmpty α
⊢ (L.lhomWithConstants α).comp ((LHom.id L).sumElim (LHom.ofIsEmpty (constantsOn α) L)) = LHom.id L[[α]]
have simp : Eq (α := L[[α]] →ᴸ L[[α]]) (LHom.sumElim LHom.sumInl (LHom.comp LHom.sumInl (LHom.ofIsEmpty (constantsOn α) L)))
  (LHom.id L[[α]])
Tactic: simp only [LHom.comp_sumElim, lhomWithConstants, LHom.comp_id]
-- Lean 4 proof step from Mathlib.ModelTheory.LanguageMap (goal)
Goal:
L : Language
α : Type w'
β : Type u_1
f : α → β
⊢ (L.lhomWithConstantsMap f).comp LHom.sumInl = L.lhomWithConstants β
have h_fun : ∀ (x : ℕ) (x_1 : L.Functions x),
  ((L.lhomWithConstantsMap f).comp LHom.sumInl).onFunction x_1 = (L.lhomWithConstants β).onFunction x_1
Tactic: ext
-- Lean 4 proof step from Mathlib.ModelTheory.LanguageMap (goal)
Goal:
L : Language
α : Type w'
β : Type u_1
f : α → β
h_fun :
  ∀ (x : ℕ) (x_1 : L.Functions x),
    ((L.lhomWithConstantsMap f).comp LHom.sumInl).onFunction x_1 = (L.lhomWithConstants β).onFunction x_1
⊢ (L.lhomWithConstantsMap f).comp LHom.sumInl = L.lhomWithConstants β
have h_rel : ∀ (x : ℕ) (x_1 : L.Relations x),
  ((L.lhomWithConstantsMap f).comp LHom.sumInl).onRelation x_1 = (L.lhomWithConstants β).onRelation x_1
Tactic: ext
-- Lean 4 proof step from Mathlib.ModelTheory.LanguageMap (goal)
Goal:
L : Language
M : Type w
inst : L.Structure M
α : Type u_1
inst_1 : Structure.{u_1, 0, w} (constantsOn α) M
a : α
x : Fin 0 → M
⊢ funMap (L := L[[α]]) (Sum.inr a) x = (↑(L.con a) : M)
have rw : Eq.{w + 1} (α := M) (funMap (L := L[[α]]) (n := 0) (Sum.inr a) default) (↑(L.con a) : M)
Tactic: rw [Unique.eq_default x]
-- Lean 4 proof step from Mathlib.ModelTheory.LanguageMap (goal)
Goal:
L : Language
L' : Language
M : Type w
inst : L.Structure M
α : Type u_1
inst_1 : Structure.{u_1, 0, w} (constantsOn α) M
A B : Set M
h : A ⊆ B
N : Type w'
inst_2 : L.Structure N
f : M ↪[L] N
⊢ M ↪[Language.withConstants.{u, v, w} L (↑A : Type w)] f.withConstants A
have refine_1 : ∀ {n : ℕ} (f_1 : (Language.withConstants.{u, v, w} L (↑A : Type w)).Functions n) (x : Fin n → M),
  f.toFun (funMap f_1 x) = funMap f_1 (f.toFun ∘ x)
Tactic: refine ⟨f.toEmbedding, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.ModelTheory.LanguageMap (goal)
Goal:
L : Language
L' : Language
M : Type w
inst : L.Structure M
α : Type u_1
inst_1 : Structure.{u_1, 0, w} (constantsOn α) M
A B : Set M
h : A ⊆ B
N : Type w'
inst_2 : L.Structure N
f : M ↪[L] N
refine_1 :
  ∀ {n : ℕ} (f_1 : (Language.withConstants.{u, v, w} L (↑A : Type w)).Functions n) (x : Fin n → M),
    f.toFun (funMap f_1 x) = funMap f_1 (f.toFun ∘ x)
⊢ M ↪[Language.withConstants.{u, v, w} L (↑A : Type w)] f.withConstants A
have refine_2 : ∀ {n : ℕ} (r : (Language.withConstants.{u, v, w} L (↑A : Type w)).Relations n) (x : Fin n → M),
  RelMap r (f.toFun ∘ x) ↔ RelMap r x
Tactic: refine ⟨f.toEmbedding, ?_, ?_⟩
-- Lean 4 proof step from Mathlib.ModelTheory.LanguageMap (goal)
Goal:
L : Language
L' : Language
M : Type w
inst : L.Structure M
α : Type u_1
inst_1 : Structure.{u_1, 0, w} (constantsOn α) M
A B : Set M
h : A ⊆ B
N : Type w'
inst_2 : L.Structure N
f : M ↪[L] N
n : ℕ
x : Fin n → M
c : (constantsOn (↑A : Type w)).Functions n
⊢ f.toFun (funMap (L := Language.withConstants.{u, v, w} L (↑A : Type w)) (Sum.inr c) x) =
    funMap (L := Language.withConstants.{u, v, w} L (↑A : Type w)) (Sum.inr c) (f.toFun ∘ x)
have refine_1 : ∀ (x : Fin 0 → M) (c : (constantsOn (↑A : Type w)).Functions 0),
  f.toFun (funMap (L := Language.withConstants.{u, v, w} L (↑A : Type w)) (Sum.inr c) x) =
    funMap (L := Language.withConstants.{u, v, w} L (↑A : Type w)) (Sum.inr c) (f.toFun ∘ x)
Tactic: cases n with
      | zero => rfl
      | succ n => exact isEmptyElim c
Cleared hypotheses: n, x, c
-- Lean 4 proof step from Mathlib.ModelTheory.LanguageMap (goal)
Goal:
L : Language
L' : Language
M : Type w
inst : L.Structure M
α : Type u_1
inst_1 : Structure.{u_1, 0, w} (constantsOn α) M
A B : Set M
h : A ⊆ B
N : Type w'
inst_2 : L.Structure N
f : M ↪[L] N
n : ℕ
x : Fin n → M
c : (constantsOn (↑A : Type w)).Functions n
refine_1 :
  ∀ (x : Fin 0 → M) (c : (constantsOn (↑A : Type w)).Functions 0),
    f.toFun (funMap (L := Language.withConstants.{u, v, w} L (↑A : Type w)) (Sum.inr c) x) =
      funMap (L := Language.withConstants.{u, v, w} L (↑A : Type w)) (Sum.inr c) (f.toFun ∘ x)
⊢ f.toFun (funMap (L := Language.withConstants.{u, v, w} L (↑A : Type w)) (Sum.inr c) x) =
    funMap (L := Language.withConstants.{u, v, w} L (↑A : Type w)) (Sum.inr c) (f.toFun ∘ x)
have refine_1₁ : ∀ (n : ℕ) (x : Fin (n + 1) → M) (c : (constantsOn (↑A : Type w)).Functions (n + 1)),
  f.toFun (funMap (L := Language.withConstants.{u, v, w} L (↑A : Type w)) (Sum.inr c) x) =
    funMap (L := Language.withConstants.{u, v, w} L (↑A : Type w)) (Sum.inr c) (f.toFun ∘ x)
Tactic: cases n with
      | zero => rfl
      | succ n => exact isEmptyElim c
Cleared hypotheses: n, x, c
-- Lean 4 proof step from Mathlib.ModelTheory.LanguageMap (goal)
Goal:
L : Language
L' : Language
M : Type w
inst : L.Structure M
α : Type u_1
inst_1 : Structure.{u_1, 0, w} (constantsOn α) M
A B : Set M
h : A ⊆ B
N : Type w'
inst_2 : L.Structure N
f : M ↪[L] N
n : ℕ
g : (Language.withConstants.{u, v, w} L (↑A : Type w)).Functions n
x : Fin n → M
⊢ f.toFun (funMap g x) = funMap g (f.toFun ∘ x)
have refine_1 : ∀ (g : L.Functions n),
  f.toFun (funMap (L := Language.withConstants.{u, v, w} L (↑A : Type w)) (Sum.inl g) x) =
    funMap (L := Language.withConstants.{u, v, w} L (↑A : Type w)) (Sum.inl g) (f.toFun ∘ x)
Tactic: cases g with
    | inl g => exact f.map_fun' g x
    | inr c =>
      cases n with
      | zero => rfl
      | succ n => exact isEmptyElim c
Cleared hypotheses: g
-- Lean 4 proof step from Mathlib.ModelTheory.LanguageMap (goal)
Goal:
L : Language
L' : Language
M : Type w
inst : L.Structure M
α : Type u_1
inst_1 : Structure.{u_1, 0, w} (constantsOn α) M
A B : Set M
h : A ⊆ B
N : Type w'
inst_2 : L.Structure N
f : M ↪[L] N
n : ℕ
g : (Language.withConstants.{u, v, w} L (↑A : Type w)).Functions n
x : Fin n → M
refine_1 :
  ∀ (g : L.Functions n),
    f.toFun (funMap (L := Language.withConstants.{u, v, w} L (↑A : Type w)) (Sum.inl g) x) =
      funMap (L := Language.withConstants.{u, v, w} L (↑A : Type w)) (Sum.inl g) (f.toFun ∘ x)
⊢ f.toFun (funMap g x) = funMap g (f.toFun ∘ x)
have refine_1₁ : ∀ (c : (constantsOn (↑A : Type w)).Functions n),
  f.toFun (funMap (L := Language.withConstants.{u, v, w} L (↑A : Type w)) (Sum.inr c) x) =
    funMap (L := Language.withConstants.{u, v, w} L (↑A : Type w)) (Sum.inr c) (f.toFun ∘ x)
Tactic: cases g with
    | inl g => exact f.map_fun' g x
    | inr c =>
      cases n with
      | zero => rfl
      | succ n => exact isEmptyElim c
Cleared hypotheses: g
-- Lean 4 proof step from Mathlib.ModelTheory.LanguageMap (goal)
Goal:
L : Language
L' : Language
M : Type w
inst : L.Structure M
α : Type u_1
inst_1 : Structure.{u_1, 0, w} (constantsOn α) M
A B : Set M
h : A ⊆ B
N : Type w'
inst_2 : L.Structure N
f : M ↪[L] N
n : ℕ
R : (Language.withConstants.{u, v, w} L (↑A : Type w)).Relations n
x : Fin n → M
⊢ RelMap R (f.toFun ∘ x) ↔ RelMap R x
have refine_2 : ∀ (R : L.Relations n),
  RelMap (L := Language.withConstants.{u, v, w} L (↑A : Type w)) (Sum.inl R) (f.toFun ∘ x) ↔
    RelMap (L := Language.withConstants.{u, v, w} L (↑A : Type w)) (Sum.inl R) x
Tactic: cases R with
    | inl R => exact f.map_rel' R x
    | inr r => exact isEmptyElim r
Cleared hypotheses: R
-- Lean 4 proof step from Mathlib.ModelTheory.LanguageMap (goal)
Goal:
L : Language
L' : Language
M : Type w
inst : L.Structure M
α : Type u_1
inst_1 : Structure.{u_1, 0, w} (constantsOn α) M
A B : Set M
h : A ⊆ B
N : Type w'
inst_2 : L.Structure N
f : M ↪[L] N
n : ℕ
R : (Language.withConstants.{u, v, w} L (↑A : Type w)).Relations n
x : Fin n → M
refine_2 :
  ∀ (R : L.Relations n),
    RelMap (L := Language.withConstants.{u, v, w} L (↑A : Type w)) (Sum.inl R) (f.toFun ∘ x) ↔
      RelMap (L := Language.withConstants.{u, v, w} L (↑A : Type w)) (Sum.inl R) x
⊢ RelMap R (f.toFun ∘ x) ↔ RelMap R x
have refine_2₁ : ∀ (r : Relations.{w, 0} (constantsOn (↑A : Type w)) n),
  RelMap (L := Language.withConstants.{u, v, w} L (↑A : Type w)) (Sum.inr r) (f.toFun ∘ x) ↔
    RelMap (L := Language.withConstants.{u, v, w} L (↑A : Type w)) (Sum.inr r) x
Tactic: cases R with
    | inl R => exact f.map_rel' R x
    | inr r => exact isEmptyElim r
Cleared hypotheses: R
-- Lean 4 proof step from Mathlib.ModelTheory.Order (hypothesis)
Goal:
L : Language
α : Type w
M : Type w'
n : ℕ
⊢ ∀ (a : Language.order.Symbols), a = default
have this : IsEmpty ((n : ℕ) × Language.order.Functions n)
Tactic: have : IsEmpty (Σ n, Language.order.Functions n) := isEmpty_sigma.2 inferInstance
-- Lean 4 proof step from Mathlib.ModelTheory.Order (goal)
Goal:
L : Language
α : Type w
M : Type w'
n : ℕ
this : IsEmpty ((n : ℕ) × Language.order.Functions n)
⊢ ∀ (a : Language.order.Symbols), a = default
have simp : ∀ (b : (l : ℕ) × Language.order.Relations l), b = default
Tactic: simp only [Symbols, Sum.forall, reduceCtorEq, Sum.inr.injEq, IsEmpty.forall_iff, true_and]