-- Mathlib/NumberTheory/MulChar/Basic.lean
theorem sum_one_eq_card_units [DecidableEq R] :
    (∑ a, (1 : MulChar R R') a) = Fintype.card Rˣ

Proof state:
R : Type u_1
inst✝³ : CommMonoid R
inst✝² : Fintype R
R' : Type u_2
inst✝¹ : CommRing R'
inst✝ : DecidableEq R
⊢ ∑ a : R, 1 a = ↑(Fintype.card Rˣ)

Tactic:
calc
  (∑ a, (1 : MulChar R R') a) = ∑ a : R, if IsUnit a then 1 else 0 :=
    Finset.sum_congr rfl fun a _ => ?_
  _ = ((Finset.univ : Finset R).filter IsUnit).card := Finset.sum_boole _ _
  _ = (Finset.univ.map ⟨((↑) : Rˣ → R), Units.ext⟩).card := ?_
  _ = Fintype.card Rˣ := congr_arg _ (Finset.card_map _)

Result:
case calc_1
R : Type u_1
inst✝³ : CommMonoid R
inst✝² : Fintype R
R' : Type u_2
inst✝¹ : CommRing R'
inst✝ : DecidableEq R
a : R
x✝ : a ∈ Finset.univ
⊢ 1 a = if IsUnit a then 1 else 0

case calc_2
R : Type u_1
inst✝³ : CommMonoid R
inst✝² : Fintype R
R' : Type u_2
inst✝¹ : CommRing R'
inst✝ : DecidableEq R
⊢ ↑(Finset.filter IsUnit Finset.univ).card = ↑(Finset.map { toFun := Units.val, inj' := ⋯ } Finset.univ).card

Proof state:
case calc_2.e_a.e_s
R : Type u_1
inst✝³ : CommMonoid R
inst✝² : Fintype R
R' : Type u_2
inst✝¹ : CommRing R'
inst✝ : DecidableEq R
⊢ Finset.filter IsUnit Finset.univ = Finset.map { toFun := Units.val, inj' := ⋯ } Finset.univ

Tactic:
ext a

Result:
case calc_2.e_a.e_s.h
R : Type u_1
inst✝³ : CommMonoid R
inst✝² : Fintype R
R' : Type u_2
inst✝¹ : CommRing R'
inst✝ : DecidableEq R
a : R
⊢ a ∈ Finset.filter IsUnit Finset.univ ↔ a ∈ Finset.map { toFun := Units.val, inj' := ⋯ } Finset.univ

Proof state:
case calc_1
R : Type u_1
inst✝³ : CommMonoid R
inst✝² : Fintype R
R' : Type u_2
inst✝¹ : CommRing R'
inst✝ : DecidableEq R
a : R
x✝ : a ∈ Finset.univ
⊢ 1 a = if IsUnit a then 1 else 0

Tactic:
split_ifs with h

Result:
case pos
R : Type u_1
inst✝³ : CommMonoid R
inst✝² : Fintype R
R' : Type u_2
inst✝¹ : CommRing R'
inst✝ : DecidableEq R
a : R
x✝ : a ∈ Finset.univ
h : IsUnit a
⊢ 1 a = 1

case neg
R : Type u_1
inst✝³ : CommMonoid R
inst✝² : Fintype R
R' : Type u_2
inst✝¹ : CommRing R'
inst✝ : DecidableEq R
a : R
x✝ : a ∈ Finset.univ
h : ¬IsUnit a
⊢ 1 a = 0

Proof state:
case pos
R : Type u_1
inst✝³ : CommMonoid R
inst✝² : Fintype R
R' : Type u_2
inst✝¹ : CommRing R'
inst✝ : DecidableEq R
a : R
x✝ : a ∈ Finset.univ
h : IsUnit a
⊢ 1 a = 1

Tactic:
exact one_apply_coe h.unit

Result:
no goals

Proof state:
case calc_2
R : Type u_1
inst✝³ : CommMonoid R
inst✝² : Fintype R
R' : Type u_2
inst✝¹ : CommRing R'
inst✝ : DecidableEq R
⊢ ↑(Finset.filter IsUnit Finset.univ).card = ↑(Finset.map { toFun := Units.val, inj' := ⋯ } Finset.univ).card

Tactic:
congr

Result:
case calc_2.e_a.e_s
R : Type u_1
inst✝³ : CommMonoid R
inst✝² : Fintype R
R' : Type u_2
inst✝¹ : CommRing R'
inst✝ : DecidableEq R
⊢ Finset.filter IsUnit Finset.univ = Finset.map { toFun := Units.val, inj' := ⋯ } Finset.univ

Proof state:
case neg
R : Type u_1
inst✝³ : CommMonoid R
inst✝² : Fintype R
R' : Type u_2
inst✝¹ : CommRing R'
inst✝ : DecidableEq R
a : R
x✝ : a ∈ Finset.univ
h : ¬IsUnit a
⊢ 1 a = 0

Tactic:
exact map_nonunit _ h

Result:
no goals

Proof state:
case calc_2.e_a.e_s.h
R : Type u_1
inst✝³ : CommMonoid R
inst✝² : Fintype R
R' : Type u_2
inst✝¹ : CommRing R'
inst✝ : DecidableEq R
a : R
⊢ a ∈ Finset.filter IsUnit Finset.univ ↔ a ∈ Finset.map { toFun := Units.val, inj' := ⋯ } Finset.univ

Tactic:
simp only [Finset.mem_filter, Finset.mem_univ, true_and, Finset.mem_map,
  Function.Embedding.coeFn_mk, exists_true_left, IsUnit]

Result:
no goals