Implicit vs explicit variables

Stream: general

[Quinn Culver]

In the code below, provided in this answer, by @Junyan Xu, the explicit/implicit status of P and L changes a few times. I think I understand why P is (made) implicit for collinear but L is (kept) explicit, and vice-versa for concurrent. But I don't understand why they're both implicit for the two perspective definitions and then both explicit for is_desarguesian. Here's the code

import combinatorics.configuration
open configuration.projective_plane

universe u

variables (P L : Type u) [has_mem P L] [configuration.projective_plane P L]

structure triangle :=
(p₀ p₁ p₂ : P)
(l₀ l₁ l₂ : L)
(i₀₁ : p₀ ∈ l₁)
(i₀₂ : p₀ ∈ l₂)
(i₁₀ : p₁ ∈ l₀)
(i₁₂ : p₁ ∈ l₂)
(i₂₀ : p₂ ∈ l₀)
(i₂₁ : p₂ ∈ l₁)

variables {P}
def collinear (p₀ p₁ p₂ : P) : Prop := ∃ l : L, p₀ ∈ l ∧ p₁ ∈ l ∧ p₂ ∈ l

variables (P) {L}
def concurrent (l₀ l₁ l₂ : L) : Prop := ∃ p : P, p ∈ l₀ ∧ p ∈ l₁ ∧ p ∈ l₂

variables {P}
def centrally_perspective (T₁ T₂ : triangle P L) : Prop :=
∃ p : P, collinear L p T₁.p₀ T₂.p₀ ∧ collinear L p T₁.p₁ T₂.p₁ ∧ collinear L p T₁.p₂ T₂.p₂

def axially_perspective (T₁ T₂ : triangle P L) : Prop :=
∃ l : L, concurrent P l T₁.l₀ T₂.l₀ ∧ concurrent P l T₁.l₁ T₂.l₁ ∧ concurrent P l T₁.l₂ T₂.l₂

variables (P L)
def is_desarguesian : Prop :=
∀ T₁ T₂ : triangle P L, centrally_perspective T₁ T₂ ↔ axially_perspective T₁ T₂

[Junyan Xu]

Because P and L can be inferred from the type of T₁ or T₂ (which is triangle P L) in the two perspective definitions, you just write axially_perspective T₁ T₂ and Lean will fill in the P L arguments. But Lean can neither infer P from L or vice versa (that's why it may be preferable to make a structure that bundles P and L), and there are no other arguments in is_desarguesian, so you need both explicit.