Add a lemma about equality of functions from a subsingleton type:

```lean
lemma funext_iff_of_subsingleton [Subsingleton α] {g : α → β} (x y : α) :
    f x = g y ↔ f = g := by
```

This isn't a `simp` lemma; it isn't entirely clear whether equality of functions or of particular values should necessarily be considered simpler, and making it a `simp` lemma introduces a `simpNF` linter failure for `eq_rec_inj`.

From AperiodicMonotilesLean.

Add a lemma about equality of functions from a subsingleton type:

```lean
lemma funext_iff_of_subsingleton [Subsingleton α] {g : α → β} (x y : α) :
    f x = g y ↔ f = g := by
```

This isn't a `simp` lemma; it isn't entirely clear whether equality of functions or of particular values should necessarily be considered simpler, and making it a `simp` lemma introduces a `simpNF` linter failure for `eq_rec_inj`.

From AperiodicMonotilesLean.

Add a lemma about equality of functions from a subsingleton type:

```lean
lemma funext_iff_of_subsingleton [Subsingleton α] {g : α → β} (x y : α) :
    f x = g y ↔ f = g := by
```

This isn't a `simp` lemma; it isn't entirely clear whether equality of functions or of particular values should necessarily be considered simpler, and making it a `simp` lemma introduces a `simpNF` linter failure for `eq_rec_inj`.

From AperiodicMonotilesLean.

Add a lemma about equality of functions from a subsingleton type:

```lean
lemma funext_iff_of_subsingleton [Subsingleton α] {g : α → β} (x y : α) :
    f x = g y ↔ f = g := by
```

This isn't a `simp` lemma; it isn't entirely clear whether equality of functions or of particular values should necessarily be considered simpler, and making it a `simp` lemma introduces a `simpNF` linter failure for `eq_rec_inj`.

From AperiodicMonotilesLean.

Add a lemma about equality of functions from a subsingleton type:

```lean
lemma funext_iff_of_subsingleton [Subsingleton α] {g : α → β} (x y : α) :
    f x = g y ↔ f = g := by
```

This isn't a `simp` lemma; it isn't entirely clear whether equality of functions or of particular values should necessarily be considered simpler, and making it a `simp` lemma introduces a `simpNF` linter failure for `eq_rec_inj`.

From AperiodicMonotilesLean.

Add a lemma about equality of functions from a subsingleton type:

```lean
lemma funext_iff_of_subsingleton [Subsingleton α] {g : α → β} (x y : α) :
    f x = g y ↔ f = g := by
```

This isn't a `simp` lemma; it isn't entirely clear whether equality of functions or of particular values should necessarily be considered simpler, and making it a `simp` lemma introduces a `simpNF` linter failure for `eq_rec_inj`.

From AperiodicMonotilesLean.