-- Mathlib/CategoryTheory/Preadditive/HomOrthogonal.lean
theorem equiv_of_iso (o : HomOrthogonal s) {α β : Type} [Finite α] [Finite β] {f : α → ι}
    {g : β → ι} (i : (⨁ fun a => s (f a)) ≅ ⨁ fun b => s (g b)) :
    ∃ e : α ≃ β, ∀ a, g (e a) = f a

Proof state:
C : Type u
inst✝⁵ : Category.{v, u} C
ι : Type u_1
s : ι → C
inst✝⁴ : Preadditive C
inst✝³ : HasFiniteBiproducts C
inst✝² : ∀ (i : ι), InvariantBasisNumber (End (s i))
o : HomOrthogonal s
α β : Type
inst✝¹ : Finite α
inst✝ : Finite β
f : α → ι
g : β → ι
i : (⨁ fun a => s (f a)) ≅ ⨁ fun b => s (g b)
c : ι
val✝¹ : Fintype α
val✝ : Fintype β
⊢ o.matrixDecomposition i.hom c * o.matrixDecomposition i.inv c = 1

Tactic:
rw [← o.matrixDecomposition_comp]

Result:
C : Type u
inst✝⁵ : Category.{v, u} C
ι : Type u_1
s : ι → C
inst✝⁴ : Preadditive C
inst✝³ : HasFiniteBiproducts C
inst✝² : ∀ (i : ι), InvariantBasisNumber (End (s i))
o : HomOrthogonal s
α β : Type
inst✝¹ : Finite α
inst✝ : Finite β
f : α → ι
g : β → ι
i : (⨁ fun a => s (f a)) ≅ ⨁ fun b => s (g b)
c : ι
val✝¹ : Fintype α
val✝ : Fintype β
⊢ o.matrixDecomposition (i.inv ≫ i.hom) c = 1

Proof state:
C : Type u
inst✝⁵ : Category.{v, u} C
ι : Type u_1
s : ι → C
inst✝⁴ : Preadditive C
inst✝³ : HasFiniteBiproducts C
inst✝² : ∀ (i : ι), InvariantBasisNumber (End (s i))
o : HomOrthogonal s
α β : Type
inst✝¹ : Finite α
inst✝ : Finite β
f : α → ι
g : β → ι
i : (⨁ fun a => s (f a)) ≅ ⨁ fun b => s (g b)
⊢ ∃ e, ∀ (a : α), g (e a) = f a

Tactic:
refine ⟨Equiv.ofPreimageEquiv ?_, fun a => Equiv.ofPreimageEquiv_map _ _⟩

Result:
C : Type u
inst✝⁵ : Category.{v, u} C
ι : Type u_1
s : ι → C
inst✝⁴ : Preadditive C
inst✝³ : HasFiniteBiproducts C
inst✝² : ∀ (i : ι), InvariantBasisNumber (End (s i))
o : HomOrthogonal s
α β : Type
inst✝¹ : Finite α
inst✝ : Finite β
f : α → ι
g : β → ι
i : (⨁ fun a => s (f a)) ≅ ⨁ fun b => s (g b)
⊢ (c : ι) → ↑(f ⁻¹' {c}) ≃ ↑(g ⁻¹' {c})

Proof state:
case h.intro
C : Type u
inst✝⁵ : Category.{v, u} C
ι : Type u_1
s : ι → C
inst✝⁴ : Preadditive C
inst✝³ : HasFiniteBiproducts C
inst✝² : ∀ (i : ι), InvariantBasisNumber (End (s i))
o : HomOrthogonal s
α β : Type
inst✝¹ : Finite α
inst✝ : Finite β
f : α → ι
g : β → ι
i : (⨁ fun a => s (f a)) ≅ ⨁ fun b => s (g b)
c : ι
val✝ : Fintype α
⊢ Cardinal.mk ↑(f ⁻¹' {c}) = Cardinal.mk ↑(g ⁻¹' {c})

Tactic:
cases nonempty_fintype β

Result:
case h.intro.intro
C : Type u
inst✝⁵ : Category.{v, u} C
ι : Type u_1
s : ι → C
inst✝⁴ : Preadditive C
inst✝³ : HasFiniteBiproducts C
inst✝² : ∀ (i : ι), InvariantBasisNumber (End (s i))
o : HomOrthogonal s
α β : Type
inst✝¹ : Finite α
inst✝ : Finite β
f : α → ι
g : β → ι
i : (⨁ fun a => s (f a)) ≅ ⨁ fun b => s (g b)
c : ι
val✝¹ : Fintype α
val✝ : Fintype β
⊢ Cardinal.mk ↑(f ⁻¹' {c}) = Cardinal.mk ↑(g ⁻¹' {c})

Proof state:
C : Type u
inst✝⁵ : Category.{v, u} C
ι : Type u_1
s : ι → C
inst✝⁴ : Preadditive C
inst✝³ : HasFiniteBiproducts C
inst✝² : ∀ (i : ι), InvariantBasisNumber (End (s i))
o : HomOrthogonal s
α β : Type
inst✝¹ : Finite α
inst✝ : Finite β
f : α → ι
g : β → ι
i : (⨁ fun a => s (f a)) ≅ ⨁ fun b => s (g b)
c : ι
⊢ ↑(f ⁻¹' {c}) ≃ ↑(g ⁻¹' {c})

Tactic:
apply Nonempty.some

Result:
case h
C : Type u
inst✝⁵ : Category.{v, u} C
ι : Type u_1
s : ι → C
inst✝⁴ : Preadditive C
inst✝³ : HasFiniteBiproducts C
inst✝² : ∀ (i : ι), InvariantBasisNumber (End (s i))
o : HomOrthogonal s
α β : Type
inst✝¹ : Finite α
inst✝ : Finite β
f : α → ι
g : β → ι
i : (⨁ fun a => s (f a)) ≅ ⨁ fun b => s (g b)
c : ι
⊢ Nonempty (↑(f ⁻¹' {c}) ≃ ↑(g ⁻¹' {c}))

Proof state:
case h.intro.intro
C : Type u
inst✝⁵ : Category.{v, u} C
ι : Type u_1
s : ι → C
inst✝⁴ : Preadditive C
inst✝³ : HasFiniteBiproducts C
inst✝² : ∀ (i : ι), InvariantBasisNumber (End (s i))
o : HomOrthogonal s
α β : Type
inst✝¹ : Finite α
inst✝ : Finite β
f : α → ι
g : β → ι
i : (⨁ fun a => s (f a)) ≅ ⨁ fun b => s (g b)
c : ι
val✝¹ : Fintype α
val✝ : Fintype β
⊢ Fintype.card ↑(f ⁻¹' {c}) = Fintype.card ↑(g ⁻¹' {c})

Tactic:
exact
  Matrix.square_of_invertible (o.matrixDecomposition i.inv c) (o.matrixDecomposition i.hom c)
    (by
      rw [← o.matrixDecomposition_comp]
      simp)
    (by
      rw [← o.matrixDecomposition_comp]
      simp)

Result:
no goals

Proof state:
case h
C : Type u
inst✝⁵ : Category.{v, u} C
ι : Type u_1
s : ι → C
inst✝⁴ : Preadditive C
inst✝³ : HasFiniteBiproducts C
inst✝² : ∀ (i : ι), InvariantBasisNumber (End (s i))
o : HomOrthogonal s
α β : Type
inst✝¹ : Finite α
inst✝ : Finite β
f : α → ι
g : β → ι
i : (⨁ fun a => s (f a)) ≅ ⨁ fun b => s (g b)
c : ι
⊢ Cardinal.mk ↑(f ⁻¹' {c}) = Cardinal.mk ↑(g ⁻¹' {c})

Tactic:
cases nonempty_fintype α

Result:
case h.intro
C : Type u
inst✝⁵ : Category.{v, u} C
ι : Type u_1
s : ι → C
inst✝⁴ : Preadditive C
inst✝³ : HasFiniteBiproducts C
inst✝² : ∀ (i : ι), InvariantBasisNumber (End (s i))
o : HomOrthogonal s
α β : Type
inst✝¹ : Finite α
inst✝ : Finite β
f : α → ι
g : β → ι
i : (⨁ fun a => s (f a)) ≅ ⨁ fun b => s (g b)
c : ι
val✝ : Fintype α
⊢ Cardinal.mk ↑(f ⁻¹' {c}) = Cardinal.mk ↑(g ⁻¹' {c})

Proof state:
case h.intro.intro
C : Type u
inst✝⁵ : Category.{v, u} C
ι : Type u_1
s : ι → C
inst✝⁴ : Preadditive C
inst✝³ : HasFiniteBiproducts C
inst✝² : ∀ (i : ι), InvariantBasisNumber (End (s i))
o : HomOrthogonal s
α β : Type
inst✝¹ : Finite α
inst✝ : Finite β
f : α → ι
g : β → ι
i : (⨁ fun a => s (f a)) ≅ ⨁ fun b => s (g b)
c : ι
val✝¹ : Fintype α
val✝ : Fintype β
⊢ Cardinal.mk ↑(f ⁻¹' {c}) = Cardinal.mk ↑(g ⁻¹' {c})

Tactic:
simp only [Cardinal.mk_fintype, Nat.cast_inj]

Result:
case h.intro.intro
C : Type u
inst✝⁵ : Category.{v, u} C
ι : Type u_1
s : ι → C
inst✝⁴ : Preadditive C
inst✝³ : HasFiniteBiproducts C
inst✝² : ∀ (i : ι), InvariantBasisNumber (End (s i))
o : HomOrthogonal s
α β : Type
inst✝¹ : Finite α
inst✝ : Finite β
f : α → ι
g : β → ι
i : (⨁ fun a => s (f a)) ≅ ⨁ fun b => s (g b)
c : ι
val✝¹ : Fintype α
val✝ : Fintype β
⊢ Fintype.card ↑(f ⁻¹' {c}) = Fintype.card ↑(g ⁻¹' {c})

Proof state:
C : Type u
inst✝⁵ : Category.{v, u} C
ι : Type u_1
s : ι → C
inst✝⁴ : Preadditive C
inst✝³ : HasFiniteBiproducts C
inst✝² : ∀ (i : ι), InvariantBasisNumber (End (s i))
o : HomOrthogonal s
α β : Type
inst✝¹ : Finite α
inst✝ : Finite β
f : α → ι
g : β → ι
i : (⨁ fun a => s (f a)) ≅ ⨁ fun b => s (g b)
⊢ ∃ e, ∀ (a : α), g (e a) = f a

Tactic:
classical
refine ⟨Equiv.ofPreimageEquiv ?_, fun a => Equiv.ofPreimageEquiv_map _ _⟩
intro c
apply Nonempty.some
apply Cardinal.eq.1
cases nonempty_fintype α; cases nonempty_fintype β
simp only [Cardinal.mk_fintype, Nat.cast_inj]
exact
  Matrix.square_of_invertible (o.matrixDecomposition i.inv c) (o.matrixDecomposition i.hom c)
    (by
      rw [← o.matrixDecomposition_comp]
      simp)
    (by
      rw [← o.matrixDecomposition_comp]
      simp)

Result:
no goals

Proof state:
C : Type u
inst✝⁵ : Category.{v, u} C
ι : Type u_1
s : ι → C
inst✝⁴ : Preadditive C
inst✝³ : HasFiniteBiproducts C
inst✝² : ∀ (i : ι), InvariantBasisNumber (End (s i))
o : HomOrthogonal s
α β : Type
inst✝¹ : Finite α
inst✝ : Finite β
f : α → ι
g : β → ι
i : (⨁ fun a => s (f a)) ≅ ⨁ fun b => s (g b)
c : ι
val✝¹ : Fintype α
val✝ : Fintype β
⊢ o.matrixDecomposition (i.hom ≫ i.inv) c = 1

Tactic:
simp

Result:
no goals