# Etiqueta: IH.symmetric

## Pruebas de length (xs ++ ys) = length xs + length ys

En Lean están definidas las funciones

``` length : list α → nat (++) : list α → list α → list α```

tales que

• (length xs) es la longitud de xs. Por ejemplo,
` length [2,3,5,3] = 4`
• (xs ++ ys) es la lista obtenida concatenando xs e ys. Por ejemplo.
` [1,2] ++ [2,3,5,3] = [1,2,2,3,5,3]`

Dichas funciones están caracterizadas por los siguientes lemas:

``` length_nil : length [] = 0 length_cons : length (x :: xs) = length xs + 1 nil_append : [] ++ ys = ys cons_append : (x :: xs) ++ y = x :: (xs ++ ys)```

Demostrar que

` length (xs ++ ys) = length xs + length ys`

Para ello, completar la siguiente teoría de Lean:

```import tactic open list   variable {α : Type} variable (x : α) variables (xs ys zs : list α)   lemma length_nil : length ([] : list α) = 0 := rfl   example : length (xs ++ ys) = length xs + length ys := sorry```
Soluciones con Lean
```import tactic open list   variable {α : Type} variable (x : α) variables (xs ys zs : list α)   lemma length_nil : length ([] : list α) = 0 := rfl   -- 1ª demostración example : length (xs ++ ys) = length xs + length ys := begin induction xs with a as HI, { rw nil_append, rw length_nil, rw zero_add, }, { rw cons_append, rw length_cons, rw HI, rw length_cons, rw add_assoc, rw add_comm (length ys), rw add_assoc, }, end   -- 2ª demostración example : length (xs ++ ys) = length xs + length ys := begin induction xs with a as HI, { rw nil_append, rw length_nil, rw zero_add, }, { rw cons_append, rw length_cons, rw HI, rw length_cons, -- library_search, exact add_right_comm (length as) (length ys) 1 }, end   -- 3ª demostración example : length (xs ++ ys) = length xs + length ys := begin induction xs with a as HI, { rw nil_append, rw length_nil, rw zero_add, }, { rw cons_append, rw length_cons, rw HI, rw length_cons, -- by hint, linarith, }, end   -- 4ª demostración example : length (xs ++ ys) = length xs + length ys := begin induction xs with a as HI, { simp, }, { simp [HI], linarith, }, end   -- 5ª demostración example : length (xs ++ ys) = length xs + length ys := begin induction xs with a as HI, { simp, }, { finish [HI],}, end   -- 6ª demostración example : length (xs ++ ys) = length xs + length ys := by induction xs ; finish [*]   -- 7ª demostración example : length (xs ++ ys) = length xs + length ys := begin induction xs with a as HI, { calc length ([] ++ ys) = length ys : congr_arg length (nil_append ys) ... = 0 + length ys : (zero_add (length ys)).symm ... = length [] + length ys : congr_arg2 (+) length_nil.symm rfl, }, { calc length ((a :: as) ++ ys) = length (a :: (as ++ ys)) : congr_arg length (cons_append a as ys) ... = length (as ++ ys) + 1 : length_cons a (as ++ ys) ... = (length as + length ys) + 1 : congr_arg2 (+) HI rfl ... = (length as + 1) + length ys : add_right_comm (length as) (length ys) 1 ... = length (a :: as) + length ys : congr_arg2 (+) (length_cons a as).symm rfl, }, end   -- 8ª demostración example : length (xs ++ ys) = length xs + length ys := begin induction xs with a as HI, { calc length ([] ++ ys) = length ys : by rw nil_append ... = 0 + length ys : (zero_add (length ys)).symm ... = length [] + length ys : by rw length_nil }, { calc length ((a :: as) ++ ys) = length (a :: (as ++ ys)) : by rw cons_append ... = length (as ++ ys) + 1 : by rw length_cons ... = (length as + length ys) + 1 : by rw HI ... = (length as + 1) + length ys : add_right_comm (length as) (length ys) 1 ... = length (a :: as) + length ys : by rw length_cons, }, end   -- 9ª demostración example : length (xs ++ ys) = length xs + length ys := list.rec_on xs ( show length ([] ++ ys) = length [] + length ys, from calc length ([] ++ ys) = length ys : by rw nil_append ... = 0 + length ys : by exact (zero_add (length ys)).symm ... = length [] + length ys : by rw length_nil ) ( assume a as, assume HI : length (as ++ ys) = length as + length ys, show length ((a :: as) ++ ys) = length (a :: as) + length ys, from calc length ((a :: as) ++ ys) = length (a :: (as ++ ys)) : by rw cons_append ... = length (as ++ ys) + 1 : by rw length_cons ... = (length as + length ys) + 1 : by rw HI ... = (length as + 1) + length ys : by exact add_right_comm (length as) (length ys) 1 ... = length (a :: as) + length ys : by rw length_cons)   -- 10ª demostración example : length (xs ++ ys) = length xs + length ys := list.rec_on xs ( by simp) ( λ a as HI, by simp [HI, add_right_comm])   -- 11ª demostración lemma longitud_conc_1 : ∀ xs, length (xs ++ ys) = length xs + length ys | [] := by calc length ([] ++ ys) = length ys : by rw nil_append ... = 0 + length ys : by rw zero_add ... = length [] + length ys : by rw length_nil | (a :: as) := by calc length ((a :: as) ++ ys) = length (a :: (as ++ ys)) : by rw cons_append ... = length (as ++ ys) + 1 : by rw length_cons ... = (length as + length ys) + 1 : by rw longitud_conc_1 ... = (length as + 1) + length ys : by exact add_right_comm (length as) (length ys) 1 ... = length (a :: as) + length ys : by rw length_cons   -- 12ª demostración lemma longitud_conc_2 : ∀ xs, length (xs ++ ys) = length xs + length ys | [] := by simp | (a :: as) := by simp [longitud_conc_2 as, add_right_comm]   -- 13ª demostración example : length (xs ++ ys) = length xs + length ys := -- by library_search length_append xs ys   -- 14ª demostración example : length (xs ++ ys) = length xs + length ys := by simp```

Se puede interactuar con la prueba anterior en esta sesión con Lean.

En los comentarios se pueden escribir otras soluciones, escribiendo el código entre una línea con <pre lang="lean"> y otra con </pre>

Soluciones con Isabelle/HOL
```theory "Pruebas_de_length(xs_++_ys)_Ig_length_xs+length_ys" imports Main begin   (* 1ª demostración *) lemma "length (xs @ ys) = length xs + length ys" proof (induct xs) have "length ([] @ ys) = length ys" by (simp only: append_Nil) also have "… = 0 + length ys" by (rule add_0 [symmetric]) also have "… = length [] + length ys" by (simp only: list.size(3)) finally show "length ([] @ ys) = length [] + length ys" by this next fix x xs assume HI : "length (xs @ ys) = length xs + length ys" have "length ((x # xs) @ ys) = length (x # (xs @ ys))" by (simp only: append_Cons) also have "… = length (xs @ ys) + 1" by (simp only: list.size(4)) also have "… = (length xs + length ys) + 1" by (simp only: HI) also have "… = (length xs + 1) + length ys" by (simp only: add.assoc add.commute) also have "… = length (x # xs) + length ys" by (simp only: list.size(4)) then show "length ((x # xs) @ ys) = length (x # xs) + length ys" by simp qed   (* 2ª demostración *) lemma "length (xs @ ys) = length xs + length ys" proof (induct xs) show "length ([] @ ys) = length [] + length ys" by simp next fix x xs assume "length (xs @ ys) = length xs + length ys" then show "length ((x # xs) @ ys) = length (x # xs) + length ys" by simp qed   (* 3ª demostración *) lemma "length (xs @ ys) = length xs + length ys" proof (induct xs) case Nil then show ?case by simp next case (Cons a xs) then show ?case by simp qed   (* 4ª demostración *) lemma "length (xs @ ys) = length xs + length ys" by (induct xs) simp_all   (* 5ª demostración *) lemma "length (xs @ ys) = length xs + length ys" by (fact length_append)   end```

En los comentarios se pueden escribir otras soluciones, escribiendo el código entre una línea con <pre lang="isar"> y otra con </pre>

## Asociatividad de la concatenación de listas

En Lean la operación de concatenación de listas se representa por (++) y está caracterizada por los siguientes lemas

``` nil_append : [] ++ ys = ys cons_append : (x :: xs) ++ y = x :: (xs ++ ys)```

Demostrar que la concatenación es asociativa; es decir,

` xs ++ (ys ++ zs) = (xs ++ ys) ++ zs`

Para ello, completar la siguiente teoría de Lean:

```import data.list.basic import tactic open list   variable {α : Type} variable (x : α) variables (xs ys zs : list α)   example : xs ++ (ys ++ zs) = (xs ++ ys) ++ zs := sorry```
Soluciones con Lean
```import data.list.basic import tactic open list   variable {α : Type} variable (x : α) variables (xs ys zs : list α)   -- 1ª demostración example : xs ++ (ys ++ zs) = (xs ++ ys) ++ zs := begin induction xs with a as HI, { calc [] ++ (ys ++ zs) = ys ++ zs : append.equations._eqn_1 (ys ++ zs) ... = ([] ++ ys) ++ zs : congr_arg2 (++) (append.equations._eqn_1 ys) rfl, }, { calc (a :: as) ++ (ys ++ zs) = a :: (as ++ (ys ++ zs)) : append.equations._eqn_2 a as (ys ++ zs) ... = a :: ((as ++ ys) ++ zs) : congr_arg2 (::) rfl HI ... = (a :: (as ++ ys)) ++ zs : (append.equations._eqn_2 a (as ++ ys) zs).symm ... = ((a :: as) ++ ys) ++ zs : congr_arg2 (++) (append.equations._eqn_2 a as ys).symm rfl, }, end   -- 2ª demostración example : xs ++ (ys ++ zs) = (xs ++ ys) ++ zs := begin induction xs with a as HI, { calc [] ++ (ys ++ zs) = ys ++ zs : nil_append (ys ++ zs) ... = ([] ++ ys) ++ zs : congr_arg2 (++) (nil_append ys) rfl, }, { calc (a :: as) ++ (ys ++ zs) = a :: (as ++ (ys ++ zs)) : cons_append a as (ys ++ zs) ... = a :: ((as ++ ys) ++ zs) : congr_arg2 (::) rfl HI ... = (a :: (as ++ ys)) ++ zs : (cons_append a (as ++ ys) zs).symm ... = ((a :: as) ++ ys) ++ zs : congr_arg2 (++) (cons_append a as ys).symm rfl, }, end   -- 3ª demostración example : xs ++ (ys ++ zs) = (xs ++ ys) ++ zs := begin induction xs with a as HI, { calc [] ++ (ys ++ zs) = ys ++ zs : by rw nil_append ... = ([] ++ ys) ++ zs : by rw nil_append, }, { calc (a :: as) ++ (ys ++ zs) = a :: (as ++ (ys ++ zs)) : by rw cons_append ... = a :: ((as ++ ys) ++ zs) : by rw HI ... = (a :: (as ++ ys)) ++ zs : by rw cons_append ... = ((a :: as) ++ ys) ++ zs : by rw ← cons_append, }, end   -- 4ª demostración example : xs ++ (ys ++ zs) = (xs ++ ys) ++ zs := begin induction xs with a as HI, { calc [] ++ (ys ++ zs) = ys ++ zs : rfl ... = ([] ++ ys) ++ zs : rfl, }, { calc (a :: as) ++ (ys ++ zs) = a :: (as ++ (ys ++ zs)) : rfl ... = a :: ((as ++ ys) ++ zs) : by rw HI ... = (a :: (as ++ ys)) ++ zs : rfl ... = ((a :: as) ++ ys) ++ zs : rfl, }, end   -- 5ª demostración example : xs ++ (ys ++ zs) = (xs ++ ys) ++ zs := begin induction xs with a as HI, { calc [] ++ (ys ++ zs) = ys ++ zs : by simp ... = ([] ++ ys) ++ zs : by simp, }, { calc (a :: as) ++ (ys ++ zs) = a :: (as ++ (ys ++ zs)) : by simp ... = a :: ((as ++ ys) ++ zs) : congr_arg (cons a) HI ... = (a :: (as ++ ys)) ++ zs : by simp ... = ((a :: as) ++ ys) ++ zs : by simp, }, end   -- 6ª demostración example : xs ++ (ys ++ zs) = (xs ++ ys) ++ zs := begin induction xs with a as HI, { by simp, }, { by exact (cons_inj a).mpr HI, }, end   -- 7ª demostración example : xs ++ (ys ++ zs) = (xs ++ ys) ++ zs := begin induction xs with a as HI, { rw nil_append, rw nil_append, }, { rw cons_append, rw HI, rw cons_append, rw cons_append, }, end   -- 8ª demostración example : xs ++ (ys ++ zs) = (xs ++ ys) ++ zs := list.rec_on xs ( show [] ++ (ys ++ zs) = ([] ++ ys) ++ zs, from calc [] ++ (ys ++ zs) = ys ++ zs : by rw nil_append ... = ([] ++ ys) ++ zs : by rw nil_append ) ( assume a as, assume HI : as ++ (ys ++ zs) = (as ++ ys) ++ zs, show (a :: as) ++ (ys ++ zs) = ((a :: as) ++ ys) ++ zs, from calc (a :: as) ++ (ys ++ zs) = a :: (as ++ (ys ++ zs)) : by rw cons_append ... = a :: ((as ++ ys) ++ zs) : by rw HI ... = (a :: (as ++ ys)) ++ zs : by rw cons_append ... = ((a :: as) ++ ys) ++ zs : by rw ← cons_append)   -- 9ª demostración example : xs ++ (ys ++ zs) = (xs ++ ys) ++ zs := list.rec_on xs (by simp) (by simp [*])   -- 10ª demostración lemma conc_asoc_1 : ∀ xs, xs ++ (ys ++ zs) = (xs ++ ys) ++ zs | [] := by calc [] ++ (ys ++ zs) = ys ++ zs : by rw nil_append ... = ([] ++ ys) ++ zs : by rw nil_append | (a :: as) := by calc (a :: as) ++ (ys ++ zs) = a :: (as ++ (ys ++ zs)) : by rw cons_append ... = a :: ((as ++ ys) ++ zs) : by rw conc_asoc_1 ... = (a :: (as ++ ys)) ++ zs : by rw cons_append ... = ((a :: as) ++ ys) ++ zs : by rw ← cons_append   -- 11ª demostración example : (xs ++ ys) ++ zs = xs ++ (ys ++ zs) := -- by library_search append_assoc xs ys zs   -- 12ª demostración example : (xs ++ ys) ++ zs = xs ++ (ys ++ zs) := by induction xs ; simp [*]   -- 13ª demostración example : (xs ++ ys) ++ zs = xs ++ (ys ++ zs) := by simp```

Se puede interactuar con la prueba anterior en esta sesión con Lean.

En los comentarios se pueden escribir otras soluciones, escribiendo el código entre una línea con <pre lang="lean"> y otra con </pre>

Soluciones con Isabelle/HOL
```theory Asociatividad_de_la_concatenacion_de_listas imports Main begin   (* 1ª demostración *) lemma "xs @ (ys @ zs) = (xs @ ys) @ zs" proof (induct xs) have "[] @ (ys @ zs) = ys @ zs" by (simp only: append_Nil) also have "… = ([] @ ys) @ zs" by (simp only: append_Nil) finally show "[] @ (ys @ zs) = ([] @ ys) @ zs" by this next fix x xs assume HI : "xs @ (ys @ zs) = (xs @ ys) @ zs" have "(x # xs) @ (ys @ zs) = x # (xs @ (ys @ zs))" by (simp only: append_Cons) also have "… = x # ((xs @ ys) @ zs)" by (simp only: HI) also have "… = (x # (xs @ ys)) @ zs" by (simp only: append_Cons) also have "… = ((x # xs) @ ys) @ zs" by (simp only: append_Cons) finally show "(x # xs) @ (ys @ zs) = ((x # xs) @ ys) @ zs" by this qed   (* 2ª demostración *) lemma "xs @ (ys @ zs) = (xs @ ys) @ zs" proof (induct xs) have "[] @ (ys @ zs) = ys @ zs" by simp also have "… = ([] @ ys) @ zs" by simp finally show "[] @ (ys @ zs) = ([] @ ys) @ zs" . next fix x xs assume HI : "xs @ (ys @ zs) = (xs @ ys) @ zs" have "(x # xs) @ (ys @ zs) = x # (xs @ (ys @ zs))" by simp also have "… = x # ((xs @ ys) @ zs)" by simp also have "… = (x # (xs @ ys)) @ zs" by simp also have "… = ((x # xs) @ ys) @ zs" by simp finally show "(x # xs) @ (ys @ zs) = ((x # xs) @ ys) @ zs" . qed   (* 3ª demostración *) lemma "xs @ (ys @ zs) = (xs @ ys) @ zs" proof (induct xs) show "[] @ (ys @ zs) = ([] @ ys) @ zs" by simp next fix x xs assume "xs @ (ys @ zs) = (xs @ ys) @ zs" then show "(x # xs) @ (ys @ zs) = ((x # xs) @ ys) @ zs" by simp qed   (* 4ª demostración *) lemma "xs @ (ys @ zs) = (xs @ ys) @ zs" proof (induct xs) case Nil then show ?case by simp next case (Cons a xs) then show ?case by simp qed   (* 5ª demostración *) lemma "xs @ (ys @ zs) = (xs @ ys) @ zs" by (rule append_assoc [symmetric])   (* 6ª demostración *) lemma "xs @ (ys @ zs) = (xs @ ys) @ zs" by (induct xs) simp_all   (* 7ª demostración *) lemma "xs @ (ys @ zs) = (xs @ ys) @ zs" by simp   end```

En los comentarios se pueden escribir otras soluciones, escribiendo el código entre una línea con <pre lang="isar"> y otra con </pre>

## Las familias de conjuntos definen relaciones simétricas

Cada familia de conjuntos P define una relación de forma que dos elementos están relacionados si algún conjunto de P contiene a ambos elementos. Se puede definir en Lean por

``` def relacion (P : set (set X)) (x y : X) := ∃ A ∈ P, x ∈ A ∧ y ∈ A```

Demostrar que si P es una familia de subconjunt❙os de X, entonces la relación definida por P es simétrica.

Para ello, completar la siguiente teoría de Lean:

```import tactic   variable {X : Type} variable (P : set (set X))   def relacion (P : set (set X)) (x y : X) := ∃ A ∈ P, x ∈ A ∧ y ∈ A   example : symmetric (relacion P) := sorry```
Soluciones con Lean
```import tactic   variable {X : Type} variable (P : set (set X))   def relacion (P : set (set X)) (x y : X) := ∃ A ∈ P, x ∈ A ∧ y ∈ A   -- 1ª demostración example : symmetric (relacion P) := begin unfold symmetric, intros x y hxy, unfold relacion at *, rcases hxy with ⟨B, hBP, ⟨hxB, hyB⟩⟩, use B, repeat { split }, { exact hBP, }, { exact hyB, }, { exact hxB, }, end   -- 2ª demostración example : symmetric (relacion P) := begin intros x y hxy, rcases hxy with ⟨B, hBP, ⟨hxB, hyB⟩⟩, use B, repeat { split } ; assumption, end   -- 3ª demostración example : symmetric (relacion P) := begin intros x y hxy, rcases hxy with ⟨B, hBP, ⟨hxB, hyB⟩⟩, use [B, ⟨hBP, hyB, hxB⟩], end```

Se puede interactuar con la prueba anterior en esta sesión con Lean.

En los comentarios se pueden escribir otras soluciones, escribiendo el código entre una línea con <pre lang="lean"> y otra con </pre>

Soluciones con Isabelle/HOL
```theory Las_familias_de_conjuntos_definen_relaciones_simetricas imports Main begin   definition relacion :: "('a set) set ⇒ 'a ⇒ 'a ⇒ bool" where "relacion P x y ⟷ (∃A∈P. x ∈ A ∧ y ∈ A)"   (* 1ª demostración *) lemma "symp (relacion P)" proof (rule sympI) fix x y assume "relacion P x y" then have "∃A∈P. x ∈ A ∧ y ∈ A" by (unfold relacion_def) then have "∃A∈P. y ∈ A ∧ x ∈ A" proof (rule bexE) fix A assume hA1 : "A ∈ P" and hA2 : "x ∈ A ∧ y ∈ A" have "y ∈ A ∧ x ∈ A" using hA2 by (simp only: conj_commute) then show "∃A∈P. y ∈ A ∧ x ∈ A" using hA1 by (rule bexI) qed then show "relacion P y x" by (unfold relacion_def) qed   (* 2ª demostración *) lemma "symp (relacion P)" proof (rule sympI) fix x y assume "relacion P x y" then obtain A where "A ∈ P ∧ x ∈ A ∧ y ∈ A" using relacion_def by metis then show "relacion P y x" using relacion_def by metis qed   (* 3ª demostración *) lemma "symp (relacion P)" using relacion_def by (metis sympI)   end```

En los comentarios se pueden escribir otras soluciones, escribiendo el código entre una línea con <pre lang="isar"> y otra con </pre>

## La composición por la izquierda con una inyectiva es una operación inyectiva

Sean f₁ y f₂ funciones de X en Y y g una función de X en Y. Demostrar que si g es inyectiva y g ∘ f₁ = g ∘ f₂, entonces f₁ = f₂.

Para ello, completar la siguiente teoría de Lean:

```import tactic   variables {X Y Z : Type*} variables {f₁ f₂ : X → Y} variable {g : Y → Z}   example (hg : function.injective g) (hgf : g ∘ f₁ = g ∘ f₂) : f₁ = f₂ := sorry```
Soluciones con Lean
```import tactic   variables {X Y Z : Type*} variables {f₁ f₂ : X → Y} variable {g : Y → Z}   -- 1ª demostración example (hg : function.injective g) (hgf : g ∘ f₁ = g ∘ f₂) : f₁ = f₂ := begin funext, apply hg, calc g (f₁ x) = (g ∘ f₁) x : rfl ... = (g ∘ f₂) x : congr_fun hgf x ... = g (f₂ x) : rfl, end   -- 2ª demostración example (hg : function.injective g) (hgf : g ∘ f₁ = g ∘ f₂) : f₁ = f₂ := begin funext, apply hg, exact congr_fun hgf x, end   -- 3ª demostración example (hg : function.injective g) (hgf : g ∘ f₁ = g ∘ f₂) : f₁ = f₂ := begin refine funext (λ i, hg _), exact congr_fun hgf i, end   -- 4ª demostración example (hg : function.injective g) : function.injective ((∘) g : (X → Y) → (X → Z)) := λ f₁ f₂ hgf, funext (λ i, hg (congr_fun hgf i : _))   -- 5ª demostración example [hY : nonempty Y] (hg : injective g) (hgf : g ∘ f₁ = g ∘ f₂) : f₁ = f₂ := calc f₁ = id ∘ f₁ : (left_id f₁).symm ... = (inv_fun g ∘ g) ∘ f₁ : congr_arg2 (∘) (inv_fun_comp hg).symm rfl ... = inv_fun g ∘ (g ∘ f₁) : comp.assoc _ _ _ ... = inv_fun g ∘ (g ∘ f₂) : congr_arg2 (∘) rfl hgf ... = (inv_fun g ∘ g) ∘ f₂ : comp.assoc _ _ _ ... = id ∘ f₂ : congr_arg2 (∘) (inv_fun_comp hg) rfl ... = f₂ : left_id f₂   -- 6ª demostración example [hY : nonempty Y] (hg : injective g) (hgf : g ∘ f₁ = g ∘ f₂) : f₁ = f₂ := calc f₁ = id ∘ f₁ : by finish ... = (inv_fun g ∘ g) ∘ f₁ : by finish [inv_fun_comp] ... = inv_fun g ∘ (g ∘ f₁) : by refl ... = inv_fun g ∘ (g ∘ f₂) : by finish [hgf] ... = (inv_fun g ∘ g) ∘ f₂ : by refl ... = id ∘ f₂ : by finish [inv_fun_comp] ... = f₂ : by finish```

Se puede interactuar con la prueba anterior en esta sesión con Lean.

En los comentarios se pueden escribir otras soluciones, escribiendo el código entre una línea con <pre lang="lean"> y otra con </pre>

Soluciones con Isabelle/HOL
```theory La_composicion_por_la_izquierda_con_una_inyectiva_es_inyectiva imports Main begin   (* 1ª demostración *) lemma assumes "inj g" "g ∘ f1 = g ∘ f2" shows "f1 = f2" proof (rule ext) fix x have "(g ∘ f1) x = (g ∘ f2) x" using ‹g ∘ f1 = g ∘ f2› by (rule fun_cong) then have "g (f1 x) = g (f2 x)" by (simp only: o_apply) then show "f1 x = f2 x" using ‹inj g› by (simp only: injD) qed   (* 2ª demostración *) lemma assumes "inj g" "g ∘ f1 = g ∘ f2" shows "f1 = f2" proof fix x have "(g ∘ f1) x = (g ∘ f2) x" using ‹g ∘ f1 = g ∘ f2› by simp then have "g (f1 x) = g (f2 x)" by simp then show "f1 x = f2 x" using ‹inj g› by (simp only: injD) qed   (* 3ª demostración *) lemma assumes "inj g" "g ∘ f1 = g ∘ f2" shows "f1 = f2" using assms by (metis fun.inj_map_strong inj_eq)   (* 4ª demostración *) lemma assumes "inj g" "g ∘ f1 = g ∘ f2" shows "f1 = f2" proof - have "f1 = id ∘ f1" by (rule id_o [symmetric]) also have "… = (inv g ∘ g) ∘ f1" by (simp add: assms(1)) also have "… = inv g ∘ (g ∘ f1)" by (simp add: comp_assoc) also have "… = inv g ∘ (g ∘ f2)" using assms(2) by (rule arg_cong) also have "… = (inv g ∘ g) ∘ f2" by (simp add: comp_assoc) also have "… = id ∘ f2" by (simp add: assms(1)) also have "… = f2" by (rule id_o) finally show "f1 = f2" by this qed   (* 5ª demostración *) lemma assumes "inj g" "g ∘ f1 = g ∘ f2" shows "f1 = f2" proof - have "f1 = (inv g ∘ g) ∘ f1" by (simp add: assms(1)) also have "… = (inv g ∘ g) ∘ f2" using assms(2) by (simp add: comp_assoc) also have "… = f2" using assms(1) by simp finally show "f1 = f2" . qed   end```

En los comentarios se pueden escribir otras soluciones, escribiendo el código entre una línea con <pre lang="isar"> y otra con </pre>