refactor(combinatorics/configuration): Implicit arguments for `nondeg…

…enerate.eq_or_eq` (#10885)

The arguments `p₁`, `p₂`, `l₁`, `l₂` can be implicit, since they can be inferred from `p₁ ∈ l₁`, `p₂ ∈ l₁`, `p₁ ∈ l₂`, `p₂ ∈ l₂`.

src/combinatorics/configuration.lean

@@ -45,7 +45,7 @@ instance : has_mem (dual L) (dual P) :=
 class nondegenerate : Prop :=
 (exists_point : ∀ l : L, ∃ p, p ∉ l)
 (exists_line : ∀ p, ∃ l : L, p ∉ l)
-(eq_or_eq : ∀ p₁ p₂ : P, ∀ l₁ l₂ : L, p₁ ∈ l₁ → p₂ ∈ l₁ → p₁ ∈ l₂ → p₂ ∈ l₂ → p₁ = p₂ ∨ l₁ = l₂)
+(eq_or_eq : ∀ {p₁ p₂ : P} {l₁ l₂ : L}, p₁ ∈ l₁ → p₂ ∈ l₁ → p₁ ∈ l₂ → p₂ ∈ l₂ → p₁ = p₂ ∨ l₁ = l₂)
 
 /-- A nondegenerate configuration in which every pair of lines has an intersection point. -/
 class has_points extends nondegenerate P L : Type u :=
@@ -74,8 +74,8 @@ instance [has_lines P L] : has_points (dual L) (dual P) :=
 
 lemma has_points.exists_unique_point [has_points P L] (l₁ l₂ : L) (hl : l₁ ≠ l₂) :
   ∃! p, p ∈ l₁ ∧ p ∈ l₂ :=
-⟨mk_point l₁ l₂, mk_point_ax l₁ l₂, λ p hp, (eq_or_eq p (mk_point l₁ l₂) l₁ l₂
-  hp.1 (mk_point_ax l₁ l₂).1 hp.2 (mk_point_ax l₁ l₂).2).resolve_right hl⟩
+⟨mk_point l₁ l₂, mk_point_ax l₁ l₂,
+  λ p hp, (eq_or_eq hp.1 (mk_point_ax l₁ l₂).1 hp.2 (mk_point_ax l₁ l₂).2).resolve_right hl⟩
 
 lemma has_lines.exists_unique_line [has_lines P L] (p₁ p₂ : P) (hp : p₁ ≠ p₂) :
   ∃! l : L, p₁ ∈ l ∧ p₂ ∈ l :=