awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.ModelTheory.LanguageMap
Goal:
L : Language
L' : Language
Ff : ⦃n : ℕ⦄ → L.Functions n → L'.Functions n
Fr : ⦃n : ℕ⦄ → L.Relations n → L'.Relations n
Gf : ⦃n : ℕ⦄ → L.Functions n → L'.Functions n
Gr : ⦃n : ℕ⦄ → L.Relations n → L'.Relations n
h_fun : { onFunction := Ff, onRelation := Fr : L →ᴸ L' }.onFunction = { onFunction := Gf, onRelation := Gr }.onFunction
h_rel : { onFunction := Ff, onRelation := Fr : L →ᴸ L' }.onRelation = { onFunction := Gf, onRelation := Gr }.onRelation
⊢ Ff = Gf ∧ Fr = Gr

Tactic:
exact And.intro h_fun h_rel

Premises used: And.intro
-- Module: Mathlib.ModelTheory.LanguageMap
Goal:
L : Language
L' : Language
F : L →ᴸ L'
mk :
  ∀ (onFunction : ⦃n : ℕ⦄ → L.Functions n → L'.Functions n) (onRelation : ⦃n : ℕ⦄ → L.Relations n → L'.Relations n),
    LHom.id L' ∘ᴸ { onFunction := onFunction, onRelation := onRelation : L →ᴸ L' } =
      { onFunction := onFunction, onRelation := onRelation }
⊢ LHom.id L' ∘ᴸ F = F

Tactic:
cases F
-- Module: Mathlib.ModelTheory.LanguageMap
Goal:
L : Language
L' : Language
onFunction : ⦃n : ℕ⦄ → L.Functions n → L'.Functions n
onRelation : ⦃n : ℕ⦄ → L.Relations n → L'.Relations n
⊢ LHom.id L' ∘ᴸ { onFunction := onFunction, onRelation := onRelation : L →ᴸ L' } =
    { onFunction := onFunction, onRelation := onRelation }

Tactic:
rfl
-- Module: Mathlib.ModelTheory.LanguageMap
Goal:
L : Language
L' : Language
F : L →ᴸ L'
mk :
  ∀ (onFunction : ⦃n : ℕ⦄ → L.Functions n → L'.Functions n) (onRelation : ⦃n : ℕ⦄ → L.Relations n → L'.Relations n),
    { onFunction := onFunction, onRelation := onRelation : L →ᴸ L' } ∘ᴸ LHom.id L =
      { onFunction := onFunction, onRelation := onRelation }
⊢ F ∘ᴸ LHom.id L = F

Tactic:
cases F
-- Module: Mathlib.ModelTheory.LanguageMap
Goal:
L : Language
L' : Language
onFunction : ⦃n : ℕ⦄ → L.Functions n → L'.Functions n
onRelation : ⦃n : ℕ⦄ → L.Relations n → L'.Relations n
⊢ { onFunction := onFunction, onRelation := onRelation : L →ᴸ L' } ∘ᴸ LHom.id L =
    { onFunction := onFunction, onRelation := onRelation }

Tactic:
rfl
-- Module: Mathlib.ModelTheory.LanguageMap
Goal:
L : Language
L' : Language
L'' : Language
L3 : Language
F : L'' →ᴸ L3
G : L' →ᴸ L''
H : L →ᴸ L'
⊢ F ∘ᴸ G ∘ᴸ H = F ∘ᴸ (G ∘ᴸ H)

Tactic:
rfl

Premises used: FirstOrder.Language.LHom.comp, rfl
-- Module: Mathlib.ModelTheory.LanguageMap
Goal:
L : Language
L' : Language
ϕ : L →ᴸ L'
L'' : Language
ψ : L'' →ᴸ L'
⊢ ϕ.sumElim ψ ∘ᴸ LHom.sumInl = ϕ

Tactic:
LHom.funext (funext fun _ => rfl) (funext fun _ => rfl)

Premises used: FirstOrder.Language.LHom.funext, funext, rfl
-- Module: Mathlib.ModelTheory.LanguageMap
Goal:
L : Language
L' : Language
ϕ : L →ᴸ L'
L'' : Language
ψ : L'' →ᴸ L'
⊢ ϕ.sumElim ψ ∘ᴸ LHom.sumInr = ψ

Tactic:
LHom.funext (funext fun _ => rfl) (funext fun _ => rfl)

Premises used: FirstOrder.Language.LHom.funext, funext, rfl
-- Module: Mathlib.ModelTheory.LanguageMap
Goal:
L : Language
L' : Language
⊢ Eq (α := L.sum L' →ᴸ L.sum L') (LHom.sumElim LHom.sumInl LHom.sumInr) (LHom.id (L.sum L'))

Tactic:
LHom.funext (funext fun _ => Sum.elim_inl_inr) (funext fun _ => Sum.elim_inl_inr)

Premises used: FirstOrder.Language.LHom.funext, funext, Sum.elim_inl_inr
-- Module: Mathlib.ModelTheory.LanguageMap
Goal:
L : Language
L' : Language
ϕ : L →ᴸ L'
L'' : Language
ψ : L'' →ᴸ L'
L3 : Language
θ : L' →ᴸ L3
⊢ θ ∘ᴸ ϕ.sumElim ψ = (θ ∘ᴸ ϕ).sumElim (θ ∘ᴸ ψ)

Tactic:
LHom.funext (funext fun _n => Sum.comp_elim _ _ _) (funext fun _n => Sum.comp_elim _ _ _)

Premises used: FirstOrder.Language.LHom.onRelation, FirstOrder.Language.LHom.funext, funext, FirstOrder.Language.LHom.onFunction, Sum.comp_elim
-- Module: Mathlib.ModelTheory.LanguageMap
Goal:
L : Language
L' : Language
ϕ : L →ᴸ L'
L₁ : Language
L₂ : Language
ψ : L₁ →ᴸ L₂
⊢ ϕ.sumMap ψ ∘ᴸ LHom.sumInl = LHom.sumInl ∘ᴸ ϕ

Tactic:
LHom.funext (funext fun _ => rfl) (funext fun _ => rfl)

Premises used: FirstOrder.Language.LHom.funext, funext, rfl
-- Module: Mathlib.ModelTheory.LanguageMap
Goal:
L : Language
L' : Language
ϕ : L →ᴸ L'
L₁ : Language
L₂ : Language
ψ : L₁ →ᴸ L₂
⊢ ϕ.sumMap ψ ∘ᴸ LHom.sumInr = LHom.sumInr ∘ᴸ ψ

Tactic:
LHom.funext (funext fun _ => rfl) (funext fun _ => rfl)

Premises used: FirstOrder.Language.LHom.funext, funext, rfl
-- Module: Mathlib.ModelTheory.LanguageMap
Goal:
L : Language
L' : Language
ϕ : L →ᴸ L'
M : Type u_1
inst : L.Structure M
inst_1 : L'.Structure M
inst_2 : ϕ.IsExpansionOn M
n : ℕ
f : L.Functions n
x : Fin n → M
⊢ funMap (ϕ.onFunction f) x = funMap f x

Tactic:
IsExpansionOn.map_onFunction f x

Premises used: FirstOrder.Language.LHom.IsExpansionOn.map_onFunction
-- Module: Mathlib.ModelTheory.LanguageMap
Goal:
L : Language
L' : Language
ϕ : L →ᴸ L'
M : Type u_1
inst : L.Structure M
inst_1 : L'.Structure M
inst_2 : ϕ.IsExpansionOn M
n : ℕ
R : L.Relations n
x : Fin n → M
⊢ RelMap (ϕ.onRelation R) x = RelMap R x

Tactic:
IsExpansionOn.map_onRelation R x

Premises used: FirstOrder.Language.LHom.IsExpansionOn.map_onRelation
-- Module: Mathlib.ModelTheory.LanguageMap
Goal:
L : Language
L' : Language
M_1 : Type w
inst : L.Structure M_1
ϕ : L →ᴸ L'
L'' : Language
M : Type u_1
inst_1 : L.Structure M
⊢ (LHom.id L).IsExpansionOn M

Tactic:
⟨fun _ _ => rfl, fun _ _ => rfl⟩

Premises used: FirstOrder.Language.LHom.IsExpansionOn.mk, rfl
-- Module: Mathlib.ModelTheory.LanguageMap
Goal:
L : Language
L' : Language
M_1 : Type w
inst : L.Structure M_1
ϕ : L →ᴸ L'
L''_1 : Language
L'' : Language
ψ : L'' →ᴸ L'
M : Type u_1
inst_1 : L.Structure M
inst_2 : L'.Structure M
inst_3 : L''.Structure M
inst_4 : ϕ.IsExpansionOn M
inst_5 : ψ.IsExpansionOn M
n : ℕ
f : (L.sum L'').Functions n
x : Fin n → M
⊢ ∀ (val : L.Functions n), funMap ((ϕ.sumElim ψ).onFunction (Sum.inl val)) x = funMap (L := L.sum L'') (Sum.inl val) x

Tactic:
simp
-- Module: Mathlib.ModelTheory.LanguageMap
Goal:
L : Language
L' : Language
M_1 : Type w
inst : L.Structure M_1
ϕ : L →ᴸ L'
L''_1 : Language
L'' : Language
ψ : L'' →ᴸ L'
M : Type u_1
inst_1 : L.Structure M
inst_2 : L'.Structure M
inst_3 : L''.Structure M
inst_4 : ϕ.IsExpansionOn M
inst_5 : ψ.IsExpansionOn M
n : ℕ
f : (L.sum L'').Functions n
x : Fin n → M
⊢ ∀ (val : L''.Functions n), funMap ((ϕ.sumElim ψ).onFunction (Sum.inr val)) x = funMap (L := L.sum L'') (Sum.inr val) x

Tactic:
simp
-- Module: Mathlib.ModelTheory.LanguageMap
Goal:
L : Language
L' : Language
M_1 : Type w
inst : L.Structure M_1
ϕ : L →ᴸ L'
L''_1 : Language
L'' : Language
ψ : L'' →ᴸ L'
M : Type u_1
inst_1 : L.Structure M
inst_2 : L'.Structure M
inst_3 : L''.Structure M
inst_4 : ϕ.IsExpansionOn M
inst_5 : ψ.IsExpansionOn M
n : ℕ
R : (L.sum L'').Relations n
x : Fin n → M
⊢ ∀ (val : L.Relations n), RelMap ((ϕ.sumElim ψ).onRelation (Sum.inl val)) x = RelMap (L := L.sum L'') (Sum.inl val) x

Tactic:
simp
-- Module: Mathlib.ModelTheory.LanguageMap
Goal:
L : Language
L' : Language
M_1 : Type w
inst : L.Structure M_1
ϕ : L →ᴸ L'
L''_1 : Language
L'' : Language
ψ : L'' →ᴸ L'
M : Type u_1
inst_1 : L.Structure M
inst_2 : L'.Structure M
inst_3 : L''.Structure M
inst_4 : ϕ.IsExpansionOn M
inst_5 : ψ.IsExpansionOn M
n : ℕ
R : (L.sum L'').Relations n
x : Fin n → M
⊢ ∀ (val : L''.Relations n), RelMap ((ϕ.sumElim ψ).onRelation (Sum.inr val)) x = RelMap (L := L.sum L'') (Sum.inr val) x

Tactic:
simp
-- Module: Mathlib.ModelTheory.LanguageMap
Goal:
L : Language
L' : Language
M_1 : Type w
inst : L.Structure M_1
ϕ : L →ᴸ L'
L'' : Language
L₁ : Language
L₂ : Language
ψ : L₁ →ᴸ L₂
M : Type u_1
inst_1 : L.Structure M
inst_2 : L'.Structure M
inst_3 : L₁.Structure M
inst_4 : L₂.Structure M
inst_5 : ϕ.IsExpansionOn M
inst_6 : ψ.IsExpansionOn M
n : ℕ
f : (L.sum L₁).Functions n
x : Fin n → M
⊢ ∀ (val : L.Functions n), funMap ((ϕ.sumMap ψ).onFunction (Sum.inl val)) x = funMap (L := L.sum L₁) (Sum.inl val) x

Tactic:
simp
-- Module: Mathlib.ModelTheory.LanguageMap
Goal:
L : Language
L' : Language
M_1 : Type w
inst : L.Structure M_1
ϕ : L →ᴸ L'
L'' : Language
L₁ : Language
L₂ : Language
ψ : L₁ →ᴸ L₂
M : Type u_1
inst_1 : L.Structure M
inst_2 : L'.Structure M
inst_3 : L₁.Structure M
inst_4 : L₂.Structure M
inst_5 : ϕ.IsExpansionOn M
inst_6 : ψ.IsExpansionOn M
n : ℕ
f : (L.sum L₁).Functions n
x : Fin n → M
⊢ ∀ (val : L₁.Functions n), funMap ((ϕ.sumMap ψ).onFunction (Sum.inr val)) x = funMap (L := L.sum L₁) (Sum.inr val) x

Tactic:
simp
-- Module: Mathlib.ModelTheory.LanguageMap
Goal:
L : Language
L' : Language
M_1 : Type w
inst : L.Structure M_1
ϕ : L →ᴸ L'
L'' : Language
L₁ : Language
L₂ : Language
ψ : L₁ →ᴸ L₂
M : Type u_1
inst_1 : L.Structure M
inst_2 : L'.Structure M
inst_3 : L₁.Structure M
inst_4 : L₂.Structure M
inst_5 : ϕ.IsExpansionOn M
inst_6 : ψ.IsExpansionOn M
n : ℕ
R : (L.sum L₁).Relations n
x : Fin n → M
⊢ ∀ (val : L.Relations n), RelMap ((ϕ.sumMap ψ).onRelation (Sum.inl val)) x = RelMap (L := L.sum L₁) (Sum.inl val) x

Tactic:
simp
-- Module: Mathlib.ModelTheory.LanguageMap
Goal:
L : Language
L' : Language
M_1 : Type w
inst : L.Structure M_1
ϕ : L →ᴸ L'
L'' : Language
L₁ : Language
L₂ : Language
ψ : L₁ →ᴸ L₂
M : Type u_1
inst_1 : L.Structure M
inst_2 : L'.Structure M
inst_3 : L₁.Structure M
inst_4 : L₂.Structure M
inst_5 : ϕ.IsExpansionOn M
inst_6 : ψ.IsExpansionOn M
n : ℕ
R : (L.sum L₁).Relations n
x : Fin n → M
⊢ ∀ (val : L₁.Relations n), RelMap ((ϕ.sumMap ψ).onRelation (Sum.inr val)) x = RelMap (L := L.sum L₁) (Sum.inr val) x

Tactic:
simp
-- Module: Mathlib.ModelTheory.LanguageMap
Goal:
L : Language
L' : Language
M_1 : Type w
inst : L.Structure M_1
ϕ : L →ᴸ L'
L'' : Language
M : Type u_1
inst_1 : L.Structure M
inst_2 : L'.Structure M
⊢ IsExpansionOn (L := L) (L' := L.sum L') LHom.sumInl M

Tactic:
⟨fun _f _ => rfl, fun _R _ => rfl⟩

Premises used: FirstOrder.Language.LHom.IsExpansionOn.mk, rfl
-- Module: Mathlib.ModelTheory.LanguageMap
Goal:
L : Language
L' : Language
M_1 : Type w
inst : L.Structure M_1
ϕ : L →ᴸ L'
L'' : Language
M : Type u_1
inst_1 : L.Structure M
inst_2 : L'.Structure M
⊢ IsExpansionOn (L := L') (L' := L.sum L') LHom.sumInr M

Tactic:
⟨fun _f _ => rfl, fun _R _ => rfl⟩

Premises used: FirstOrder.Language.LHom.IsExpansionOn.mk, rfl
-- Module: Mathlib.ModelTheory.LanguageMap
Goal:
L : Language
L' : Language
M : Type w
inst : L.Structure M
inst_1 : (L.sum L').Structure M
inst_2 : IsExpansionOn (L := L) (L' := L.sum L') LHom.sumInl M
n : ℕ
f : L.Functions n
x : Fin n → M
⊢ funMap (L := L.sum L') (Sum.inl f) x = funMap f x

Tactic:
(LHom.sumInl : L →ᴸ L.sum L').map_onFunction f x

Premises used: FirstOrder.Language.LHom.map_onFunction, FirstOrder.Language.LHom.sumInl
-- Module: Mathlib.ModelTheory.LanguageMap
Goal:
L : Language
L' : Language
M : Type w
inst : L.Structure M
inst_1 : (L'.sum L).Structure M
inst_2 : IsExpansionOn (L := L) (L' := L'.sum L) LHom.sumInr M
n : ℕ
f : L.Functions n
x : Fin n → M
⊢ funMap (L := L'.sum L) (Sum.inr f) x = funMap f x

Tactic:
(LHom.sumInr : L →ᴸ L'.sum L).map_onFunction f x

Premises used: FirstOrder.Language.LHom.sumInr, FirstOrder.Language.LHom.map_onFunction
-- Module: Mathlib.ModelTheory.LanguageMap
Goal:
L : Language
L' : Language
⊢ LHom.Injective (L := L) (L' := L.sum L') LHom.sumInl

Tactic:
⟨fun h => Sum.inl_injective h, fun h => Sum.inl_injective h⟩

Premises used: Sum.inl_injective, FirstOrder.Language.LHom.Injective.mk
-- Module: Mathlib.ModelTheory.LanguageMap
Goal:
L : Language
L' : Language
⊢ LHom.Injective (L := L') (L' := L.sum L') LHom.sumInr

Tactic:
⟨fun h => Sum.inr_injective h, fun h => Sum.inr_injective h⟩

Premises used: Sum.inr_injective, FirstOrder.Language.LHom.Injective.mk
-- Module: Mathlib.ModelTheory.LanguageMap
Goal:
L : Language
L' : Language
M_1 : Type w
inst : L.Structure M_1
ϕ_1 : L →ᴸ L'
L'' : Language
ϕ : L →ᴸ L'
M : Type u_1
inst_1 : L'.Structure M
⊢ ϕ.IsExpansionOn M

Tactic:
letI := ϕ.reduct M
  ⟨fun _f _ => rfl, fun _R _ => rfl⟩

Premises used: FirstOrder.Language.LHom.IsExpansionOn.mk, rfl
-- Module: Mathlib.ModelTheory.LanguageMap
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

Tactic:
⟨fun {n} f xs => ?_, fun {n} r xs => ?_⟩

Premises used: FirstOrder.Language.LHom.IsExpansionOn.mk
-- Module: Mathlib.ModelTheory.LanguageMap
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
refine_2 : ∀ {n : ℕ} (r : L.Relations n) (xs : Fin n → M), RelMap (ϕ.onRelation r) xs = RelMap r xs
⊢ ϕ.IsExpansionOn M

Tactic:
refine ⟨fun {n} f xs => ?_, fun {n} r xs => ?_⟩
-- Module: Mathlib.ModelTheory.LanguageMap
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
⊢ 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⟩
-- Module: Mathlib.ModelTheory.LanguageMap
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

Tactic:
(dif_pos hf).trans ?_

Premises used: dif_pos, Eq.trans
-- Module: Mathlib.ModelTheory.LanguageMap
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)
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
⊢ funMap (ϕ.onFunction f) xs = funMap f xs

Tactic:
refine (dif_pos hf).trans ?_

Premises used: dif_pos, Eq.trans
-- Module: Mathlib.ModelTheory.LanguageMap
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)
refine_1 refine_1₁ : funMap f xs = funMap f xs
⊢ 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:
rw [h.onFunction hf.choose_spec]

Premises used: FirstOrder.Language.LHom.Injective.onFunction, Exists.choose_spec
-- Module: Mathlib.ModelTheory.LanguageMap
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
⊢ 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⟩
-- Module: Mathlib.ModelTheory.LanguageMap
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

Tactic:
(dif_pos hr).trans ?_

Premises used: dif_pos, Eq.trans
-- Module: Mathlib.ModelTheory.LanguageMap
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)
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
⊢ RelMap (ϕ.onRelation r) xs = RelMap r xs

Tactic:
refine (dif_pos hr).trans ?_

Premises used: dif_pos, Eq.trans
-- Module: Mathlib.ModelTheory.LanguageMap
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)
refine_2 refine_2₁ : RelMap r xs = RelMap r xs
⊢ 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:
rw [h.onRelation hr.choose_spec]

Premises used: Exists.choose_spec, FirstOrder.Language.LHom.Injective.onRelation
-- Module: Mathlib.ModelTheory.LanguageMap
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
rw₄ rw₅ : LHom.id L = LHom.id L
⊢ (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]

Premises used: FirstOrder.Language.LHom.id_comp, FirstOrder.Language.LHom.comp_assoc, FirstOrder.Language.LEquiv.invLHom, FirstOrder.Language.LEquiv.left_inv
-- Module: Mathlib.ModelTheory.LanguageMap
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''
rw₄ rw₅ : LHom.id L'' = LHom.id L''
⊢ (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]

Premises used: FirstOrder.Language.LEquiv.right_inv, FirstOrder.Language.LHom.id_comp, FirstOrder.Language.LHom.comp_assoc, FirstOrder.Language.LEquiv.toLHom
-- Module: Mathlib.ModelTheory.LanguageMap
Goal:
α : Type u'
⊢ (constantsOn α).Constants = α

Tactic:
rfl

Premises used: FirstOrder.Language.constantsOnFunc, rfl
-- Module: Mathlib.ModelTheory.LanguageMap
Goal:
L : Language
L' : Language
M : Type w
inst : L.Structure M
α : Type u'
n : ℕ
⊢ IsEmpty.{u' + 1} ((constantsOn α).Functions (n + 1))

Tactic:
inferInstanceAs (IsEmpty PEmpty)

Premises used: _private.0.FirstOrder.Language.isEmpty_functions_constantsOn_succ._proof_1
-- Module: Mathlib.ModelTheory.LanguageMap
Goal:
L : Language
L' : Language
M : Type w
inst : L.Structure M
α : Type u'
_ie : IsEmpty α
⊢ IsRelational.{u', 0} (constantsOn α)

Tactic:
fun n => Nat.casesOn n _ie inferInstance

Premises used: Nat.casesOn
-- Module: Mathlib.ModelTheory.LanguageMap
Goal:
α : Type u'
⊢ (constantsOn α).card = #α

Tactic:
simp [card_eq_card_functions_add_card_relations, sum_nat_eq_add_sum_succ]

Premises used: FirstOrder.Language.card_eq_card_functions_add_card_relations, Cardinal.sum_nat_eq_add_sum_succ
-- Module: Mathlib.ModelTheory.LanguageMap
Goal:
M : Type w
α : Type u'
β : Type v'
f : α → β
fα : α → M
fβ : β → M
h : fβ ∘ f = fα
this_1 : Structure.{u', 0, w} (constantsOn α) M := constantsOn.structure fα
this : Structure.{v', 0, w} (constantsOn β) M := constantsOn.structure fβ
⊢ (LHom.constantsOnMap f).IsExpansionOn M

Tactic:
⟨fun {n} => Nat.casesOn n (fun F _x => (congr_fun h F :)) fun n F => isEmptyElim F, fun R =>
      isEmptyElim R⟩

Premises used: isEmptyElim, FirstOrder.Language.LHom.IsExpansionOn.mk, Nat.casesOn
-- Module: Mathlib.ModelTheory.LanguageMap
Goal:
M : Type w
α : Type u'
β : Type v'
f : α → β
fα : α → M
fβ : β → M
h : fβ ∘ f = fα
this_1 : Structure.{u', 0, w} (constantsOn α) M := constantsOn.structure fα
this : Structure.{v', 0, w} (constantsOn β) M := constantsOn.structure fβ
⊢ (LHom.constantsOnMap f).IsExpansionOn M

Tactic:
exact
    ⟨fun {n} => Nat.casesOn n (fun F _x => (congr_fun h F :)) fun n F => isEmptyElim F, fun R =>
      isEmptyElim R⟩