-- Lean 4 proof step from Mathlib.Topology.Instances.AddCircle.DenseSubgroup (goal)
Goal:
a p : ℝ
rw :
  (DenseRange (X := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (AddSubgroup.zmultiples p)) fun (x : ℤ) ↦
      HSMul.hSMul (β := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (AddSubgroup.zmultiples p)) x
        (↑a : ℝ ⧸ AddSubgroup.zmultiples p)) ↔
    Dense (↑(AddSubgroup.closure {a, p}) : Set ℝ)
rw₁ :
  Dense (X := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (AddSubgroup.zmultiples p))
      (range fun (x : ℤ) ↦
        HSMul.hSMul (β := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (AddSubgroup.zmultiples p)) x
          (↑a : ℝ ⧸ AddSubgroup.zmultiples p)) ↔
    Dense (↑(AddSubgroup.closure {a, p}) : Set ℝ)
rw₂ :
  Dense (X := ℝ)
      (preimage (β := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (AddSubgroup.zmultiples p)) QuotientAddGroup.mk
        (range fun (x : ℤ) ↦
          HSMul.hSMul (β := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (AddSubgroup.zmultiples p)) x
            (↑a : ℝ ⧸ AddSubgroup.zmultiples p))) ↔
    Dense (↑(AddSubgroup.closure {a, p}) : Set ℝ)
rw₃ :
  Dense (X := ℝ)
      (preimage (β := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (AddSubgroup.zmultiples p))
        (⇑(QuotientAddGroup.mk' (AddSubgroup.zmultiples p)) : (a : ℝ) → ℝ ⧸ AddSubgroup.zmultiples p)
        (range fun (x : ℤ) ↦
          HSMul.hSMul (β := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (AddSubgroup.zmultiples p)) x
            ((QuotientAddGroup.mk' (AddSubgroup.zmultiples p) : (a : ℝ) → ℝ ⧸ AddSubgroup.zmultiples p) a :
              HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (AddSubgroup.zmultiples p)))) ↔
    Dense (↑(AddSubgroup.closure {a, p}) : Set ℝ)
rw₄ :
  Dense (X := ℝ)
      ((⇑(QuotientAddGroup.mk' (AddSubgroup.zmultiples p)) : (a : ℝ) → ℝ ⧸ AddSubgroup.zmultiples p) ⁻¹'
        (↑(AddSubgroup.zmultiples
                ((QuotientAddGroup.mk' (AddSubgroup.zmultiples p) : (a : ℝ) → ℝ ⧸ AddSubgroup.zmultiples p) a) :
              AddSubgroup (HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (AddSubgroup.zmultiples p))) :
          Set (ℝ ⧸ AddSubgroup.zmultiples p))) ↔
    Dense (↑(AddSubgroup.closure {a, p}) : Set ℝ)
rw₅ :
  Dense
      (↑(AddSubgroup.comap (N := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (AddSubgroup.zmultiples p))
            (QuotientAddGroup.mk' (AddSubgroup.zmultiples p))
            (AddSubgroup.zmultiples
              ((QuotientAddGroup.mk' (AddSubgroup.zmultiples p) : (a : ℝ) → ℝ ⧸ AddSubgroup.zmultiples p) a))) :
        Set ℝ) ↔
    Dense (↑(AddSubgroup.closure {a, p}) : Set ℝ)
rw₆ :
  Dense
      (↑(AddSubgroup.comap (N := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (AddSubgroup.zmultiples p))
            (QuotientAddGroup.mk' (AddSubgroup.zmultiples p))
            (AddSubgroup.map (QuotientAddGroup.mk' (AddSubgroup.zmultiples p)) (AddSubgroup.zmultiples a))) :
        Set ℝ) ↔
    Dense (↑(AddSubgroup.closure {a, p}) : Set ℝ)
⊢ (DenseRange (X := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (AddSubgroup.zmultiples p)) fun (x : ℤ) ↦
      HSMul.hSMul (β := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (AddSubgroup.zmultiples p)) x
        (↑a : ℝ ⧸ AddSubgroup.zmultiples p)) ↔
    Irrational (a / p)
have rw₇ : Dense
    (↑(AddSubgroup.zmultiples a ⊔
          AddMonoidHom.ker (M := HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (AddSubgroup.zmultiples p))
            (QuotientAddGroup.mk' (AddSubgroup.zmultiples p))) :
      Set ℝ) ↔
  Dense (↑(AddSubgroup.closure {a, p}) : Set ℝ)
Tactic: rw [← dense_addSubgroupClosure_pair_iff, DenseRange,
    ← QuotientAddGroup.dense_preimage_mk, ← QuotientAddGroup.coe_mk',
    ← AddSubgroup.coe_zmultiples, ← AddSubgroup.coe_comap, ← AddMonoidHom.map_zmultiples,
    AddSubgroup.comap_map_eq, QuotientAddGroup.ker_mk', AddSubgroup.zmultiples_eq_closure,
    AddSubgroup.zmultiples_eq_closure, ← AddSubgroup.closure_union, insert_eq]