case calc_1
R : Type u
inst✝⁴ : CommRing R
R' : Type v
inst✝³ : CommRing R'
R'' : Type w
inst✝² : CommRing R''
inst✝¹ : Fintype 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
inst✝⁴ : CommRing R
R' : Type v
inst✝³ : CommRing R'
R'' : Type w
inst✝² : CommRing R''
inst✝¹ : Fintype R
inst✝ : DecidableEq R
⊢ ↑(Finset.card (Finset.filter IsUnit Finset.univ)) =
    ↑(Finset.card (Finset.map { toFun := Units.val, inj' := (_ : Function.Injective Units.val) } Finset.univ))
R : Type u
inst✝⁴ : CommRing R
R' : Type v
inst✝³ : CommRing R'
R'' : Type w
inst✝² : CommRing R''
inst✝¹ : Fintype R
inst✝ : DecidableEq R
⊢ ∑ a : R, ↑1 a = ↑(Fintype.card Rˣ)
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 _)
case calc_1.inl
R : Type u
inst✝⁴ : CommRing R
R' : Type v
inst✝³ : CommRing R'
R'' : Type w
inst✝² : CommRing R''
inst✝¹ : Fintype R
inst✝ : DecidableEq R
a : R
x✝ : a ∈ Finset.univ
h : IsUnit a
⊢ ↑1 a = 1

case calc_1.inr
R : Type u
inst✝⁴ : CommRing R
R' : Type v
inst✝³ : CommRing R'
R'' : Type w
inst✝² : CommRing R''
inst✝¹ : Fintype R
inst✝ : DecidableEq R
a : R
x✝ : a ∈ Finset.univ
h : ¬IsUnit a
⊢ ↑1 a = 0
case calc_1
R : Type u
inst✝⁴ : CommRing R
R' : Type v
inst✝³ : CommRing R'
R'' : Type w
inst✝² : CommRing R''
inst✝¹ : Fintype R
inst✝ : DecidableEq R
a : R
x✝ : a ∈ Finset.univ
⊢ ↑1 a = if IsUnit a then 1 else 0
split_ifs with h
no goals
case calc_1.inl
R : Type u
inst✝⁴ : CommRing R
R' : Type v
inst✝³ : CommRing R'
R'' : Type w
inst✝² : CommRing R''
inst✝¹ : Fintype R
inst✝ : DecidableEq R
a : R
x✝ : a ∈ Finset.univ
h : IsUnit a
⊢ ↑1 a = 1
exact one_apply_coe h.unit
no goals
case calc_1.inr
R : Type u
inst✝⁴ : CommRing R
R' : Type v
inst✝³ : CommRing R'
R'' : Type w
inst✝² : CommRing R''
inst✝¹ : Fintype R
inst✝ : DecidableEq R
a : R
x✝ : a ∈ Finset.univ
h : ¬IsUnit a
⊢ ↑1 a = 0
exact map_nonunit _ h
case calc_2.e_a.e_s
R : Type u
inst✝⁴ : CommRing R
R' : Type v
inst✝³ : CommRing R'
R'' : Type w
inst✝² : CommRing R''
inst✝¹ : Fintype R
inst✝ : DecidableEq R
⊢ Finset.filter IsUnit Finset.univ =
    Finset.map { toFun := Units.val, inj' := (_ : Function.Injective Units.val) } Finset.univ
case calc_2
R : Type u
inst✝⁴ : CommRing R
R' : Type v
inst✝³ : CommRing R'
R'' : Type w
inst✝² : CommRing R''
inst✝¹ : Fintype R
inst✝ : DecidableEq R
⊢ ↑(Finset.card (Finset.filter IsUnit Finset.univ)) =
    ↑(Finset.card (Finset.map { toFun := Units.val, inj' := (_ : Function.Injective Units.val) } Finset.univ))
congr
case calc_2.e_a.e_s.a
R : Type u
inst✝⁴ : CommRing R
R' : Type v
inst✝³ : CommRing R'
R'' : Type w
inst✝² : CommRing R''
inst✝¹ : Fintype R
inst✝ : DecidableEq R
a : R
⊢ a ∈ Finset.filter IsUnit Finset.univ ↔
    a ∈ Finset.map { toFun := Units.val, inj' := (_ : Function.Injective Units.val) } Finset.univ
case calc_2.e_a.e_s
R : Type u
inst✝⁴ : CommRing R
R' : Type v
inst✝³ : CommRing R'
R'' : Type w
inst✝² : CommRing R''
inst✝¹ : Fintype R
inst✝ : DecidableEq R
⊢ Finset.filter IsUnit Finset.univ =
    Finset.map { toFun := Units.val, inj' := (_ : Function.Injective Units.val) } Finset.univ
ext a
no goals
case calc_2.e_a.e_s.a
R : Type u
inst✝⁴ : CommRing R
R' : Type v
inst✝³ : CommRing R'
R'' : Type w
inst✝² : CommRing R''
inst✝¹ : Fintype R
inst✝ : DecidableEq R
a : R
⊢ a ∈ Finset.filter IsUnit Finset.univ ↔
    a ∈ Finset.map { toFun := Units.val, inj' := (_ : Function.Injective Units.val) } Finset.univ
simp only [Finset.mem_filter, Finset.mem_univ, true_and_iff, Finset.mem_map,
  Function.Embedding.coeFn_mk, exists_true_left, IsUnit]