diff --git a/RiddleProofs/MontyHall/MeasureTheory.lean b/RiddleProofs/MontyHall/MeasureTheory.lean
index 6a18528..4c9a295 100644
--- a/RiddleProofs/MontyHall/MeasureTheory.lean
+++ b/RiddleProofs/MontyHall/MeasureTheory.lean
@@ -3,8 +3,7 @@ import Mathlib.Probability.Kernel.Posterior
 
 /-! Written by Matteo Cipollina
 
-This file contains generic measure theory, probability theory, and general Bayesian methods.
-This includes all probability theory infrastructure that could be reused for other problems.
+This file contains generic measure theory and probability theory.
 -/
 
 set_option linter.unusedVariables false
@@ -124,7 +123,9 @@ lemma comp_apply {Ω 𝓧 : Type*} [Fintype Ω]
   congr with ω
   exact CommMonoid.mul_comm ((κ ω) s) (μ {ω})
 
+/- Constructing a kernel from an arbitrary function requires measurability. A direct proof of measurability is much easier when the domain is countable. A measurable countable space with measurable singletons turns any function `f: α -> β` into a measurable function. -/
 lemma Kernel.ofFunOfCountable_apply [MeasurableSpace α] [MeasurableSpace β] [Countable α]
+    /- `MeasurableSingletonClass is required when you need to evaluate kernel at a point. -/
     [MeasurableSingletonClass α] (f : α → Measure β) (a : α) :
     Kernel.ofFunOfCountable f a = f a := rfl
 
@@ -144,6 +145,7 @@ lemma sum_univ_of_three {α β : Type*} [Fintype α] [DecidableEq α]
   simp [Finset.sum_insert h₁, Finset.sum_insert h₂, Finset.sum_singleton,
         add_comm, add_left_comm]
 
+
 end Finset
 
-end ProbabilityTheory
\ No newline at end of file
+end ProbabilityTheory
diff --git a/RiddleProofs/MontyHall/Solution.lean b/RiddleProofs/MontyHall/Solution.lean
index a63666c..764cc91 100644
--- a/RiddleProofs/MontyHall/Solution.lean
+++ b/RiddleProofs/MontyHall/Solution.lean
@@ -15,9 +15,11 @@ open scoped ENNReal
 
 /-! ## Monty Hall Specific Definitions -/
 
+variable {p h c d : Door}
+
 instance : StandardBorelSpace Door := inferInstance
 
-/- Prior: uniform on three doors (as a measure). -/
+/-- Prior: uniform distribution on three doors (as a measure). -/
 noncomputable def prior : Measure CarLocation :=
   (PMF.uniformOfFintype CarLocation).toMeasure
 
@@ -33,88 +35,92 @@ instance subtype_ne_nonempty (p : Door) : Nonempty { d : Door // d ≠ p } :=
   | .middle => ⟨⟨.left,   by decide⟩⟩
   | .right  => ⟨⟨.left,   by decide⟩⟩
 
-/-- likelihood kernel: if the car is at `p`, host picks uniformly among the two doors ≠ `p`. -/
+/-- Definition of a kernel representing conditional distributions of host actions given car locations.
+
+A kernel κ : α → Measure β assigns a measure on β for any a ∈ α.
+In the context of probability theory, a is the value of a random variable X and κ(a) represents the conditional probability distribution of some random variable Y given X = a. -/
 noncomputable def likelihood (p : Door) : Kernel CarLocation HostAction :=
   Kernel.ofFunOfCountable fun c =>
     if  c = p then
-      -- host chooses uniformly on the two doors not equal to p
-      -- Map the measure from the subtype to Door
-      Measure.map (fun x : { d // d ≠ p } => x.val)
+      -- Host chooses uniformly among the two doors not equal to p
+      -- Map the measure from the subtype to HostAction
+      let f : { d // d ≠ p } → Door := λ x : { d // d ≠ p } => x.val -- push-forward function
+      Measure.map f -- Computes push-forward of measure on codomain `HostAction`
         ((PMF.uniformOfFintype { d // d ≠ p }).toMeasure)
+        -- `Measure.map` works by defining the inverse map (f₊μ)(A) = μ(f⁻¹(A))
+        -- Remark: `f` is not necessarily surjective, but should be measurable
     else
-      -- if car ≠ p, host must open the unique other door
-      (PMF.pure (other_door p c)).toMeasure
+      -- If c ≠ p, host must open the unique other door
+      (PMF.pure (remaining_door p c)).toMeasure
+      -- `PMF.pure` creates a PMF that assigns probability 1 to the singleton set `{remaining_door p c}`
 
+/-- The kernel `likelihood` must yield an actual probability measure for every `p` door and sum to one. This requirement is captured by the `IsMarkovKernel` type class. -/
 instance (p : Door) : IsMarkovKernel (likelihood p) :=
+-- For any car location, we prove that `likelihood p c` is a probability measure over `HostAction`.
 ⟨fun c => by
-  by_cases hc : c = p
+  -- Consider each possible car location.
+  by_cases p_eq_c : c = p
   · -- uniform case: push-forward of a uniform PMF on the subtype
-    simp only [likelihood, hc, ProbabilityTheory.Kernel.ofFunOfCountable_apply]
+    show IsProbabilityMeasure ((likelihood p) c)
+    simp only [likelihood, p_eq_c, ProbabilityTheory.Kernel.ofFunOfCountable_apply]
+    -- We evaluate the kernel at `likelihood p c` with `ofFunOfCountable_apply`.
     haveI : IsProbabilityMeasure ((PMF.uniformOfFintype { d // d ≠ p }).toMeasure) :=
-      PMF.toMeasure.isProbabilityMeasure _
+      PMF.toMeasure.isProbabilityMeasure _ -- We can leave out `(PMF.uniformOfFintype { d // d ≠ p })`.
     exact
+      -- If you push-forward a probability measure, it remains a probability measure.
       MeasureTheory.isProbabilityMeasure_map
+        /- Required condition: the push-forward function `f` is measurable.
+        A slightly more general version of measurability is "almost everywhere measurable" (`aemeasurable`). -/
         measurable_subtype_coe.aemeasurable
   · -- deterministic case: `pure` PMF is a probability measure
-    simp only [likelihood, hc, ProbabilityTheory.Kernel.ofFunOfCountable_apply]
+    show IsProbabilityMeasure ((likelihood p) c)
+    simp only [likelihood, p_eq_c, ProbabilityTheory.Kernel.ofFunOfCountable_apply]
+    -- We evaluate the kernel at `likelihood p c` with `ofFunOfCountable_apply`.
     exact PMF.toMeasure.isProbabilityMeasure _
 ⟩
 
-/- Posterior kernel using Bayesian inference -/
-noncomputable def postK (p : Door) : Kernel HostAction CarLocation :=
-  (likelihood p)†prior
 
-section MontyHallBayes
+/-- The † operator computes an application of the `posterior` operator on kernel `likelihood p` with respect to prior distribution of cars in `prior`.
 
-lemma other_door_involutive {p h : Door} (h_ne_p : h ≠ p) :
-    other_door p (other_door p h) = h := by
-  cases p <;> cases h <;> simp [other_door]
+It works by applying a generalized version of Bayes' theorem that reduces to the more familiar discrete form of Bayes' theorem:
 
-open scoped BigOperators
+P(Car=X | Host=Y) = P(Host=Y | Car=X) × P(Car=X) / P(Host=Y)
 
+Where the marginal probability is computed as:
 
-lemma Door.card_eq_three : Fintype.card Door = 3 := by
-  decide
+P(Host=Y) = Σ_X P(Host=Y | Car=X) × P(Car=X)
 
-lemma Fintype.card_subtype_ne_of_three (p : Door) : Fintype.card { d : Door // d ≠ p } = 2 := by
-  rw [Fintype.card_subtype_compl, Door.card_eq_three]
-  simp
+-/
+noncomputable def postK (p : Door) : Kernel HostAction CarLocation :=
+  (likelihood p)†prior
 
-namespace MontyHallBayes
 
-variable {p h : Door} (h_ne_p : h ≠ p)
 
-/-- The third door, different from `p` and `h`. -/
-private noncomputable def o (p h : Door) : Door :=
-  other_door p h
+lemma Fintype.card_subtype_ne_of_three (p : Door) : Fintype.card { d : Door // d ≠ p } = 2 := by
+  rw [Fintype.card_subtype_compl, Door.card_eq_three]
+  simp
 
-private lemma o_ne_p (p h : Door) (h_ne_p : h ≠ p) : o p h ≠ p :=
-  -- we use `h_ne_p.symm : p ≠ h` so that `other_door_is_other` matches its arguments
+private lemma remaining_ne_p (p h : Door) (h_ne_p : h ≠ p) : remaining_door p h ≠ p :=
+  -- Use `h_ne_p.symm : p ≠ h` so that `other_door_is_other` matches its arguments
   (other_door_is_other (h_ne_p.symm)).1
 
-private lemma o_ne_h (p h : Door) (h_ne_p : h ≠ p) : o p h ≠ h :=
-  -- same trick
+private lemma remaining_ne_h (p h : Door) (h_ne_p : h ≠ p) : remaining_door p h ≠ h :=
+
   (other_door_is_other (h_ne_p.symm)).2
 
 private lemma other_door_of_ne {p h x : Door} (hp : p ≠ h) (hx_ne_p : x ≠ p) (hx_ne_h : x ≠ h) :
-    x = other_door p h := by
+    x = remaining_door p h := by
   revert p h x hp hx_ne_p hx_ne_h; decide
 
-variable {p h : Door} (h_ne_p : h ≠ p)
-
-namespace Measure
-
-open scoped ENNReal
-
 /--
 Probability that the push-forward of the uniform measure on the subtype
 `{d // d ≠ p}` assigns to the singleton `{h}`.
 Since the subtype has exactly two elements, this value is `1 / 2`. -/
 lemma map_uniform_subtype_singleton {p h : Door} (h_ne_p : h ≠ p) :
     (Measure.map (fun x : { d // d ≠ p } => (x : Door))
+        -- This lemma is only used when `p = c` and the host has to choose uniformly between the two remaining doors.
         ((PMF.uniformOfFintype { d // d ≠ p }).toMeasure)) {h}
       = (1 : ℝ≥0∞) / 2 := by
-  classical
   have h_map :
       (Measure.map (fun x : { d // d ≠ p } => (x : Door))
           ((PMF.uniformOfFintype { d // d ≠ p }).toMeasure)) {h}
@@ -144,33 +150,32 @@ lemma map_uniform_subtype_singleton {p h : Door} (h_ne_p : h ≠ p) :
       Fintype.card_unique, ENNReal.natCast_sub, Nat.cast_one, one_div, inv_inj, MeasurableSet.singleton]
   simp [h_map, h_pre, h_val]
 
-end Measure
 
-variable {p h : Door} (h_ne_p : h ≠ p)
 
 /-- If the car is behind door `p`, the host chooses uniformly among the two
 remaining doors, so the probability that he opens `h ≠ p` is `1 / 2`. -/
-lemma likelihood_at_p (h_ne_p : h ≠ p) :
+lemma likelihood_at_when_part_pick_car (h_ne_p : h ≠ p) :
     (likelihood p) p {h} = (1 : ℝ≥0∞) / 2 := by
   classical
   simpa [likelihood, ProbabilityTheory.Kernel.ofFunOfCountable_apply]
-        using Measure.map_uniform_subtype_singleton (p := p) (h := h) h_ne_p
+        using map_uniform_subtype_singleton (p := p) (h := h) h_ne_p
 
 /-- If the car is behind door `h`, the host cannot open `h`. -/
-lemma likelihood_at_h (h_ne_p : h ≠ p) :
+lemma likelihood_h_when_car_at_h (h_ne_p : h ≠ p) :
     (likelihood p) h {h} = 0 := by
-  have h_ne : other_door p h ≠ h := (other_door_is_other h_ne_p.symm).2
-  rw [likelihood, ProbabilityTheory.Kernel.ofFunOfCountable_apply]
+  have h_ne : remaining_door p h ≠ h := (other_door_is_other h_ne_p.symm).2
+  rw [likelihood, ProbabilityTheory.Kernel.ofFunOfCountable_apply] -- Evaluate simple kernel.
   simp only [h_ne_p]
-  simp [PMF.pure_apply,]
+  simp [PMF.pure_apply,] -- Apply a PMF defined on a singleton set.
   exact id (Ne.symm h_ne)
 
-/-- If the car is behind the third door `o p h`, the host must open `h`. -/
-lemma likelihood_at_o (h_ne_p : h ≠ p) :
-    (likelihood p) (o p h) {h} = 1 := by
-  have c_ne_p : o p h ≠ p := o_ne_p p h h_ne_p
-  have h_forced : other_door p (o p h) = h := by
-    rw [o, other_door_involutive h_ne_p]
+
+/-- If the car is behind the third door `remaining_door p h`, the host must open `h`. -/
+lemma likelihood_at_h_when_part_not_pick_car (h_ne_p : h ≠ p) :
+    (likelihood p) (remaining_door p h) {h} = 1 := by
+  have c_ne_p : remaining_door p h ≠ p := remaining_ne_p p h h_ne_p
+  have h_forced : remaining_door p (remaining_door p h) = h := by
+    rw [other_door_involutive h_ne_p]
   rw [likelihood,ProbabilityTheory.Kernel.ofFunOfCountable_apply]
   simp only [c_ne_p]
   rw [h_forced]
@@ -182,24 +187,24 @@ lemma likelihood_at_o (h_ne_p : h ≠ p) :
 open MeasureTheory ProbabilityTheory
 
 
-/-- The universe of doors consists of exactly the three doors `{p, h, o p h}`. -/
+/-- The universe of doors consists of exactly the three doors `{p, h, remaining_door p h}`. -/
 lemma door_univ_eq_three (h_ne_p : h ≠ p) :
-    (Finset.univ : Finset Door) = {p, h, o p h} := by
+    (Finset.univ : Finset Door) = {p, h, remaining_door p h} := by
   ext x; simp; by_cases hxp : x = p; · left; assumption
   right; by_cases hxh : x = h; · left; assumption
   right; exact (other_door_of_ne h_ne_p.symm hxp hxh)
 
-/-- The three doors `p`, `h`, and `o p h` are pairwise distinct. -/
+/-- The three doors `p`, `h`, and `remaining_door p h` are pairwise distinct. -/
 lemma doors_pairwise_distinct (h_ne_p : h ≠ p) :
-    p ≠ h ∧ p ≠ o p h ∧ h ≠ o p h := by
+    p ≠ h ∧ p ≠ remaining_door p h ∧ h ≠ remaining_door p h := by
   constructor
   · exact h_ne_p.symm
   · constructor
-    · exact (o_ne_p p h h_ne_p).symm
-    · exact (o_ne_h p h h_ne_p).symm
+    · exact (remaining_ne_p p h h_ne_p).symm
+    · exact (remaining_ne_h p h h_ne_p).symm
 
-/-- Each door has prior probability 1/3 under the uniform distribution. -/
-lemma prior_uniform (d : Door) : prior {d} = 1 / 3 := by
+/-- Without host evidence, every door is equally likely to have car for participant. -/
+lemma eval_uniform_prior (d : Door) : prior {d} = 1 / 3 := by
   rw [prior]
   rw [PMF.toMeasure_apply_singleton (PMF.uniformOfFintype CarLocation) d]
   rw [PMF.uniformOfFintype_apply]
@@ -207,46 +212,71 @@ lemma prior_uniform (d : Door) : prior {d} = 1 / 3 := by
 
 
 
-/-- The marginal probability of the host opening door `h`. -/
+
+
+/-
+First, it is important to understand the concept of the composition of a kernel with a measure.
+
+Given:
+- μ : Measure α (a measure on space α)
+- κ : Kernel α β (a kernel from α to β)
+
+The composition κ ∘ₘ μ : Measure β is defined as:
+(κ ∘ₘ μ)(B) = ∫_{a ∈ α} κ(a)(B) dμ(a)
+where κ(a)(B) is the measure that κ(a) assigns to set B ⊆ β
+
+In our Monty Hall context:
+- α = CarLocation (the space/type)
+- a ranges over specific car locations (door1, door2, door3)
+- μ = prior (uniform measure on car locations)
+- κ = likelihood p (kernel giving host behavior for each car location)
+
+Integrate over all possible car locations, weighted by the prior probability of each location.
+
+-/
+
+
+/-- What is the probability that the host will open door `h`? -/
 lemma marginal_prob_h (h_ne_p : h ≠ p) :
     ((likelihood p) ∘ₘ prior) {h} = (1 : ℝ≥0∞) / 2 := by
-  classical
+  -- We first apply a general measure-theoretic version of the law of total probability `comp_apply`. In a discrete probability space this becomes:
+  -- Σ_car P(host opens h | car location) × P(car location)
   rw [ProbabilityTheory.comp_apply _ _ (by simp)]
   have h_cover := door_univ_eq_three h_ne_p
   have h_doors_distinct := doors_pairwise_distinct h_ne_p
   rw [ProbabilityTheory.Finset.sum_univ_of_three _ h_doors_distinct.1 h_doors_distinct.2.1
         h_doors_distinct.2.2 h_cover]
-  rw [likelihood_at_p h_ne_p, likelihood_at_h h_ne_p, likelihood_at_o h_ne_p]
-  rw [prior_uniform p, prior_uniform h, prior_uniform (o p h)]
+  show
+    prior {p} * ((likelihood p) p) {h} +
+    prior {h} * ((likelihood p) h) {h} +
+    prior {remaining_door p h} * ((likelihood p) (remaining_door p h)) {h}
+       = 1 / 2
+  -- Rewrite each term in the sum:
+  -- Case 1: Car at picked door → 1/3 × 1/2
+  rw [likelihood_at_when_part_pick_car h_ne_p, eval_uniform_prior p]
+  -- Case 2: Car at host door → 1/3 × 0
+  rw [likelihood_h_when_car_at_h h_ne_p, eval_uniform_prior h]
+  -- Case 3: Car at remaining door → 1/3 × 1
+  rw [likelihood_at_h_when_part_not_pick_car h_ne_p, eval_uniform_prior (remaining_door p h)]
   eq_as_reals
 
-/- The probability of winning by switching doors. -/
+/-- The probability of winning by switching doors. -/
 theorem switch_wins_prob_bayes (p h : Door) (h_ne_p : h ≠ p) :
-    (postK p h) {other_door p h} = (2 : ℝ≥0∞) / 3 := by
-  classical
-  set o : Door := other_door p h with ho
+    (postK p h) {remaining_door p h} = (2 : ℝ≥0∞) / 3 := by
+  set o : Door := remaining_door p h with ho
   -- The denominator in Bayes’ formula is non-zero
   have hpos : ((likelihood p) ∘ₘ prior) {h} ≠ 0 := by
     rw [marginal_prob_h h_ne_p]
-    norm_num
-  -- Bayes’ rule specialised to singletons
-  have post_eq :
-      (postK p h) {o} =
-        (prior {o} * (likelihood p) o {h}) /
-          ((likelihood p) ∘ₘ prior) {h} := by
-    rw [postK]
-    exact posterior_apply_singleton (likelihood p) prior h o hpos
-  -- The prior is uniform
-  have prior_o : prior {o} = (1 : ℝ≥0∞) / 3 := by
-    simpa using prior_uniform o
-  have h_post : (postK p h) {o} = (2 : ℝ≥0∞) / 3 := by
-    have lik_o : (likelihood p) o {h} = 1 := by
-      simpa [ho] using likelihood_at_o (p := p) (h := h) h_ne_p
-    have : (prior {o} * (likelihood p) o {h}) /
-        ((likelihood p) ∘ₘ prior) {h} = (2 : ℝ≥0∞) / 3 := by
-      simp [prior_o, lik_o, marginal_prob_h h_ne_p,
-            div_eq_mul_inv, mul_comm]
-    simpa [post_eq] using this
-  simpa [ho] using h_post
-
-end MontyHallBayes
+    eq_as_reals
+  calc (postK p h) {remaining_door p h}
+    = (postK p h) {o} := by rw [ho]
+    _ = (prior {o} * (likelihood p) o {h}) / ((likelihood p) ∘ₘ prior) {h} := by
+      rw [postK]
+      -- Bayes’ rule specialised to singletons
+      exact posterior_apply_singleton (likelihood p) prior h o hpos
+    _ = ((1 : ℝ≥0∞) / 3 * (likelihood p) o {h}) / ((1 : ℝ≥0∞) / 2) := by
+      rw [eval_uniform_prior, marginal_prob_h h_ne_p]
+    _ = ((1 : ℝ≥0∞) / 3 * 1) / ((1 : ℝ≥0∞) / 2) := by
+      rw [likelihood_at_h_when_part_not_pick_car h_ne_p]
+    _ = (2 : ℝ≥0∞) / 3 := by
+      eq_as_reals
diff --git a/RiddleProofs/MontyHall/Statement.lean b/RiddleProofs/MontyHall/Statement.lean
index c1e5c3f..1ae93b3 100644
--- a/RiddleProofs/MontyHall/Statement.lean
+++ b/RiddleProofs/MontyHall/Statement.lean
@@ -51,7 +51,7 @@ instance : Nonempty Door := ⟨.left⟩
 
 
 @[simp]
-def other_door (d₁ d₂ : Door) : Door :=
+def remaining_door (d₁ d₂ : Door) : Door :=
   if d₁ = d₂ then d₁ else
   match d₁, d₂ with
   | .left,  .middle => .right
@@ -63,8 +63,16 @@ def other_door (d₁ d₂ : Door) : Door :=
   | _, _ => d₁
 
 lemma other_door_is_other {d₁ d₂ : Door} (h : d₁ ≠ d₂) :
-    other_door d₁ d₂ ≠ d₁ ∧ other_door d₁ d₂ ≠ d₂ := by
+    remaining_door d₁ d₂ ≠ d₁ ∧ remaining_door d₁ d₂ ≠ d₂ := by
   revert d₁ d₂ h; decide
 
 abbrev CarLocation := Door
 abbrev HostAction := Door
+
+
+lemma other_door_involutive {p h : Door} (h_ne_p : h ≠ p) :
+    remaining_door p (remaining_door p h) = h := by
+  cases p <;> cases h <;> simp [remaining_door]
+
+lemma Door.card_eq_three : Fintype.card Door = 3 := by
+  decide