n : ℕ
e : ↑{m | m < n ∧ coprime n m} ≃ { x // x ∈ filter (coprime n) (range n) } :=
  { toFun := fun m => { val := ↑m, property := (_ : ↑m ∈ filter (coprime n) (range n)) },
    invFun := fun m => { val := ↑m, property := (_ : ↑m < n ∧ coprime n ↑m) },
    left_inv :=
      (_ :
        ∀ (m : ↑{m | m < n ∧ coprime n m}),
          { val := ↑m,
              property :=
                (_ :
                  ↑((fun m => { val := ↑m, property := (_ : ↑m ∈ filter (coprime n) (range n)) }) m) < n ∧
                    coprime n ↑((fun m => { val := ↑m, property := (_ : ↑m ∈ filter (coprime n) (range n)) }) m)) } =
            m),
    right_inv :=
      (_ :
        ∀ (m : { x // x ∈ filter (coprime n) (range n) }),
          { val := ↑m,
              property :=
                (_ :
                  ↑((fun m => { val := ↑m, property := (_ : ↑m < n ∧ coprime n ↑m) }) m) ∈
                    filter (coprime n) (range n)) } =
            m) }
⊢ φ n = Nat.card ↑{m | m < n ∧ coprime n m}
n : ℕ
⊢ φ n = Nat.card ↑{m | m < n ∧ coprime n m}
let e : { m | m < n ∧ n.coprime m } ≃ Finset.filter n.coprime (Finset.range n) :=
  { toFun := fun m => ⟨m, by simpa only [Finset.mem_filter, Finset.mem_range] using m.property⟩
    invFun := fun m => ⟨m, by simpa only [Finset.mem_filter, Finset.mem_range] using m.property⟩
    left_inv := fun m => by simp only [Subtype.coe_mk, Subtype.coe_eta]
    right_inv := fun m => by simp only [Subtype.coe_mk, Subtype.coe_eta] }
no goals
n : ℕ
e : ↑{m | m < n ∧ coprime n m} ≃ { x // x ∈ filter (coprime n) (range n) } :=
  { toFun := fun m => { val := ↑m, property := (_ : ↑m ∈ filter (coprime n) (range n)) },
    invFun := fun m => { val := ↑m, property := (_ : ↑m < n ∧ coprime n ↑m) },
    left_inv :=
      (_ :
        ∀ (m : ↑{m | m < n ∧ coprime n m}),
          { val := ↑m,
              property :=
                (_ :
                  ↑((fun m => { val := ↑m, property := (_ : ↑m ∈ filter (coprime n) (range n)) }) m) < n ∧
                    coprime n ↑((fun m => { val := ↑m, property := (_ : ↑m ∈ filter (coprime n) (range n)) }) m)) } =
            m),
    right_inv :=
      (_ :
        ∀ (m : { x // x ∈ filter (coprime n) (range n) }),
          { val := ↑m,
              property :=
                (_ :
                  ↑((fun m => { val := ↑m, property := (_ : ↑m < n ∧ coprime n ↑m) }) m) ∈
                    filter (coprime n) (range n)) } =
            m) }
⊢ φ n = Nat.card ↑{m | m < n ∧ coprime n m}
rw [totient_eq_card_coprime, card_congr e, card_eq_fintype_card, Fintype.card_coe]
no goals
n : ℕ
m : ↑{m | m < n ∧ coprime n m}
⊢ ↑m ∈ filter (coprime n) (range n)
simpa only [Finset.mem_filter, Finset.mem_range] using m.property
no goals
n : ℕ
m : { x // x ∈ filter (coprime n) (range n) }
⊢ ↑m ∈ {m | m < n ∧ coprime n m}
simpa only [Finset.mem_filter, Finset.mem_range] using m.property
no goals
n : ℕ
m : ↑{m | m < n ∧ coprime n m}
⊢ (fun m => { val := ↑m, property := (_ : ↑m < n ∧ coprime n ↑m) })
      ((fun m => { val := ↑m, property := (_ : ↑m ∈ filter (coprime n) (range n)) }) m) =
    m
simp only [Subtype.coe_mk, Subtype.coe_eta]
no goals
n : ℕ
m : { x // x ∈ filter (coprime n) (range n) }
⊢ (fun m => { val := ↑m, property := (_ : ↑m ∈ filter (coprime n) (range n)) })
      ((fun m => { val := ↑m, property := (_ : ↑m < n ∧ coprime n ↑m) }) m) =
    m
simp only [Subtype.coe_mk, Subtype.coe_eta]