-- Mathlib/ModelTheory/LanguageMap.lean
theorem Injective.isExpansionOn_default {ϕ : L →ᴸ L'}
    [∀ (n) (f : L'.Functions n), Decidable (f ∈ Set.range fun f : L.Functions n => ϕ.onFunction f)]
    [∀ (n) (r : L'.Relations n), Decidable (r ∈ Set.range fun r : L.Relations n => ϕ.onRelation r)]
    (h : ϕ.Injective) (M : Type*) [Inhabited M] [L.Structure M] :
    @IsExpansionOn L L' ϕ M _ (ϕ.defaultExpansion M)

Proof state:
L : Language
L' : Language
ϕ : L →ᴸ L'
inst✝³ : (n : ℕ) → (f : L'.Functions n) → Decidable (f ∈ Set.range fun f => ϕ.onFunction f)
inst✝² : (n : ℕ) → (r : L'.Relations n) → Decidable (r ∈ Set.range fun r => ϕ.onRelation r)
h : ϕ.Injective
M : Type u_1
inst✝¹ : Inhabited M
inst✝ : L.Structure M
this : L'.Structure M := ϕ.defaultExpansion M
⊢ ϕ.IsExpansionOn M

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

Result:
case refine_1
L : Language
L' : Language
ϕ : L →ᴸ L'
inst✝³ : (n : ℕ) → (f : L'.Functions n) → Decidable (f ∈ Set.range fun f => ϕ.onFunction f)
inst✝² : (n : ℕ) → (r : L'.Relations n) → Decidable (r ∈ Set.range fun r => ϕ.onRelation r)
h : ϕ.Injective
M : Type u_1
inst✝¹ : Inhabited M
inst✝ : 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

case refine_2
L : Language
L' : Language
ϕ : L →ᴸ L'
inst✝³ : (n : ℕ) → (f : L'.Functions n) → Decidable (f ∈ Set.range fun f => ϕ.onFunction f)
inst✝² : (n : ℕ) → (r : L'.Relations n) → Decidable (r ∈ Set.range fun r => ϕ.onRelation r)
h : ϕ.Injective
M : Type u_1
inst✝¹ : Inhabited M
inst✝ : 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

Proof state:
case refine_1
L : Language
L' : Language
ϕ : L →ᴸ L'
inst✝³ : (n : ℕ) → (f : L'.Functions n) → Decidable (f ∈ Set.range fun f => ϕ.onFunction f)
inst✝² : (n : ℕ) → (r : L'.Relations n) → Decidable (r ∈ Set.range fun r => ϕ.onRelation r)
h : ϕ.Injective
M : Type u_1
inst✝¹ : Inhabited M
inst✝ : L.Structure M
this : L'.Structure M := ϕ.defaultExpansion M
n : ℕ
f : L.Functions n
xs : Fin n → M
hf : ϕ.onFunction f ∈ Set.range fun f => ϕ.onFunction f
⊢ funMap (Exists.choose hf) xs = funMap f xs

Tactic:
rw [h.onFunction hf.choose_spec]

Result:
no goals

Proof state:
case refine_2
L : Language
L' : Language
ϕ : L →ᴸ L'
inst✝³ : (n : ℕ) → (f : L'.Functions n) → Decidable (f ∈ Set.range fun f => ϕ.onFunction f)
inst✝² : (n : ℕ) → (r : L'.Relations n) → Decidable (r ∈ Set.range fun r => ϕ.onRelation r)
h : ϕ.Injective
M : Type u_1
inst✝¹ : Inhabited M
inst✝ : L.Structure M
this : L'.Structure M := ϕ.defaultExpansion M
n : ℕ
r : L.Relations n
xs : Fin n → M
hr : ϕ.onRelation r ∈ Set.range fun r => ϕ.onRelation r
⊢ RelMap (Exists.choose hr) xs = RelMap r xs

Tactic:
rw [h.onRelation hr.choose_spec]

Result:
no goals

Proof state:
case refine_1
L : Language
L' : Language
ϕ : L →ᴸ L'
inst✝³ : (n : ℕ) → (f : L'.Functions n) → Decidable (f ∈ Set.range fun f => ϕ.onFunction f)
inst✝² : (n : ℕ) → (r : L'.Relations n) → Decidable (r ∈ Set.range fun r => ϕ.onRelation r)
h : ϕ.Injective
M : Type u_1
inst✝¹ : Inhabited M
inst✝ : L.Structure M
this : L'.Structure M := ϕ.defaultExpansion M
n : ℕ
f : L.Functions n
xs : Fin n → M
hf : ϕ.onFunction f ∈ Set.range fun f => ϕ.onFunction f
⊢ funMap (ϕ.onFunction f) xs = funMap f xs

Tactic:
refine (dif_pos hf).trans ?_

Result:
case refine_1
L : Language
L' : Language
ϕ : L →ᴸ L'
inst✝³ : (n : ℕ) → (f : L'.Functions n) → Decidable (f ∈ Set.range fun f => ϕ.onFunction f)
inst✝² : (n : ℕ) → (r : L'.Relations n) → Decidable (r ∈ Set.range fun r => ϕ.onRelation r)
h : ϕ.Injective
M : Type u_1
inst✝¹ : Inhabited M
inst✝ : L.Structure M
this : L'.Structure M := ϕ.defaultExpansion M
n : ℕ
f : L.Functions n
xs : Fin n → M
hf : ϕ.onFunction f ∈ Set.range fun f => ϕ.onFunction f
⊢ funMap (Exists.choose hf) xs = funMap f xs

Proof state:
L : Language
L' : Language
ϕ : L →ᴸ L'
inst✝³ : (n : ℕ) → (f : L'.Functions n) → Decidable (f ∈ Set.range fun f => ϕ.onFunction f)
inst✝² : (n : ℕ) → (r : L'.Relations n) → Decidable (r ∈ Set.range fun r => ϕ.onRelation r)
h : ϕ.Injective
M : Type u_1
inst✝¹ : Inhabited M
inst✝ : L.Structure M
⊢ ϕ.IsExpansionOn M

Tactic:
letI := ϕ.defaultExpansion M

Result:
L : Language
L' : Language
ϕ : L →ᴸ L'
inst✝³ : (n : ℕ) → (f : L'.Functions n) → Decidable (f ∈ Set.range fun f => ϕ.onFunction f)
inst✝² : (n : ℕ) → (r : L'.Relations n) → Decidable (r ∈ Set.range fun r => ϕ.onRelation r)
h : ϕ.Injective
M : Type u_1
inst✝¹ : Inhabited M
inst✝ : L.Structure M
this : L'.Structure M := ϕ.defaultExpansion M
⊢ ϕ.IsExpansionOn M

Proof state:
case refine_2
L : Language
L' : Language
ϕ : L →ᴸ L'
inst✝³ : (n : ℕ) → (f : L'.Functions n) → Decidable (f ∈ Set.range fun f => ϕ.onFunction f)
inst✝² : (n : ℕ) → (r : L'.Relations n) → Decidable (r ∈ Set.range fun r => ϕ.onRelation r)
h : ϕ.Injective
M : Type u_1
inst✝¹ : Inhabited M
inst✝ : 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

Tactic:
have hr : ϕ.onRelation r ∈ Set.range fun r : L.Relations n => ϕ.onRelation r := ⟨r, rfl⟩

Result:
case refine_2
L : Language
L' : Language
ϕ : L →ᴸ L'
inst✝³ : (n : ℕ) → (f : L'.Functions n) → Decidable (f ∈ Set.range fun f => ϕ.onFunction f)
inst✝² : (n : ℕ) → (r : L'.Relations n) → Decidable (r ∈ Set.range fun r => ϕ.onRelation r)
h : ϕ.Injective
M : Type u_1
inst✝¹ : Inhabited M
inst✝ : L.Structure M
this : L'.Structure M := ϕ.defaultExpansion M
n : ℕ
r : L.Relations n
xs : Fin n → M
hr : ϕ.onRelation r ∈ Set.range fun r => ϕ.onRelation r
⊢ RelMap (ϕ.onRelation r) xs = RelMap r xs

Proof state:
case refine_2
L : Language
L' : Language
ϕ : L →ᴸ L'
inst✝³ : (n : ℕ) → (f : L'.Functions n) → Decidable (f ∈ Set.range fun f => ϕ.onFunction f)
inst✝² : (n : ℕ) → (r : L'.Relations n) → Decidable (r ∈ Set.range fun r => ϕ.onRelation r)
h : ϕ.Injective
M : Type u_1
inst✝¹ : Inhabited M
inst✝ : L.Structure M
this : L'.Structure M := ϕ.defaultExpansion M
n : ℕ
r : L.Relations n
xs : Fin n → M
hr : ϕ.onRelation r ∈ Set.range fun r => ϕ.onRelation r
⊢ RelMap (ϕ.onRelation r) xs = RelMap r xs

Tactic:
refine (dif_pos hr).trans ?_

Result:
case refine_2
L : Language
L' : Language
ϕ : L →ᴸ L'
inst✝³ : (n : ℕ) → (f : L'.Functions n) → Decidable (f ∈ Set.range fun f => ϕ.onFunction f)
inst✝² : (n : ℕ) → (r : L'.Relations n) → Decidable (r ∈ Set.range fun r => ϕ.onRelation r)
h : ϕ.Injective
M : Type u_1
inst✝¹ : Inhabited M
inst✝ : L.Structure M
this : L'.Structure M := ϕ.defaultExpansion M
n : ℕ
r : L.Relations n
xs : Fin n → M
hr : ϕ.onRelation r ∈ Set.range fun r => ϕ.onRelation r
⊢ RelMap (Exists.choose hr) xs = RelMap r xs

Proof state:
case refine_1
L : Language
L' : Language
ϕ : L →ᴸ L'
inst✝³ : (n : ℕ) → (f : L'.Functions n) → Decidable (f ∈ Set.range fun f => ϕ.onFunction f)
inst✝² : (n : ℕ) → (r : L'.Relations n) → Decidable (r ∈ Set.range fun r => ϕ.onRelation r)
h : ϕ.Injective
M : Type u_1
inst✝¹ : Inhabited M
inst✝ : 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

Tactic:
have hf : ϕ.onFunction f ∈ Set.range fun f : L.Functions n => ϕ.onFunction f := ⟨f, rfl⟩

Result:
case refine_1
L : Language
L' : Language
ϕ : L →ᴸ L'
inst✝³ : (n : ℕ) → (f : L'.Functions n) → Decidable (f ∈ Set.range fun f => ϕ.onFunction f)
inst✝² : (n : ℕ) → (r : L'.Relations n) → Decidable (r ∈ Set.range fun r => ϕ.onRelation r)
h : ϕ.Injective
M : Type u_1
inst✝¹ : Inhabited M
inst✝ : L.Structure M
this : L'.Structure M := ϕ.defaultExpansion M
n : ℕ
f : L.Functions n
xs : Fin n → M
hf : ϕ.onFunction f ∈ Set.range fun f => ϕ.onFunction f
⊢ funMap (ϕ.onFunction f) xs = funMap f xs