C : Type u
inst✝⁵ : Category C
ι : Type u_1
s : ι → C
inst✝⁴ : Preadditive C
inst✝³ : HasFiniteBiproducts C
inst✝² : ∀ (i : ι), InvariantBasisNumber (End (s i))
o : HomOrthogonal s
α β : Type
inst✝¹ : Fintype α
inst✝ : Fintype β
f : α → ι
g : β → ι
i : (⨁ fun a => s (f a)) ≅ ⨁ fun b => s (g b)
⊢ (c : ι) → ↑((fun a => f a) ⁻¹' {c}) ≃ ↑(g ⁻¹' {c})
C : Type u
inst✝⁵ : Category C
ι : Type u_1
s : ι → C
inst✝⁴ : Preadditive C
inst✝³ : HasFiniteBiproducts C
inst✝² : ∀ (i : ι), InvariantBasisNumber (End (s i))
o : HomOrthogonal s
α β : Type
inst✝¹ : Fintype α
inst✝ : Fintype β
f : α → ι
g : β → ι
i : (⨁ fun a => s (f a)) ≅ ⨁ fun b => s (g b)
⊢ ∃ e, ∀ (a : α), g (↑e a) = f a
refine' ⟨Equiv.ofPreimageEquiv _, fun a => Equiv.ofPreimageEquiv_map _ _⟩
C : Type u
inst✝⁵ : Category C
ι : Type u_1
s : ι → C
inst✝⁴ : Preadditive C
inst✝³ : HasFiniteBiproducts C
inst✝² : ∀ (i : ι), InvariantBasisNumber (End (s i))
o : HomOrthogonal s
α β : Type
inst✝¹ : Fintype α
inst✝ : Fintype β
f : α → ι
g : β → ι
i : (⨁ fun a => s (f a)) ≅ ⨁ fun b => s (g b)
c : ι
⊢ ↑((fun a => f a) ⁻¹' {c}) ≃ ↑(g ⁻¹' {c})
C : Type u
inst✝⁵ : Category C
ι : Type u_1
s : ι → C
inst✝⁴ : Preadditive C
inst✝³ : HasFiniteBiproducts C
inst✝² : ∀ (i : ι), InvariantBasisNumber (End (s i))
o : HomOrthogonal s
α β : Type
inst✝¹ : Fintype α
inst✝ : Fintype β
f : α → ι
g : β → ι
i : (⨁ fun a => s (f a)) ≅ ⨁ fun b => s (g b)
⊢ (c : ι) → ↑((fun a => f a) ⁻¹' {c}) ≃ ↑(g ⁻¹' {c})
intro c
case h
C : Type u
inst✝⁵ : Category C
ι : Type u_1
s : ι → C
inst✝⁴ : Preadditive C
inst✝³ : HasFiniteBiproducts C
inst✝² : ∀ (i : ι), InvariantBasisNumber (End (s i))
o : HomOrthogonal s
α β : Type
inst✝¹ : Fintype α
inst✝ : Fintype β
f : α → ι
g : β → ι
i : (⨁ fun a => s (f a)) ≅ ⨁ fun b => s (g b)
c : ι
⊢ Nonempty (↑((fun a => f a) ⁻¹' {c}) ≃ ↑(g ⁻¹' {c}))
C : Type u
inst✝⁵ : Category C
ι : Type u_1
s : ι → C
inst✝⁴ : Preadditive C
inst✝³ : HasFiniteBiproducts C
inst✝² : ∀ (i : ι), InvariantBasisNumber (End (s i))
o : HomOrthogonal s
α β : Type
inst✝¹ : Fintype α
inst✝ : Fintype β
f : α → ι
g : β → ι
i : (⨁ fun a => s (f a)) ≅ ⨁ fun b => s (g b)
c : ι
⊢ ↑((fun a => f a) ⁻¹' {c}) ≃ ↑(g ⁻¹' {c})
apply Nonempty.some
case h
C : Type u
inst✝⁵ : Category C
ι : Type u_1
s : ι → C
inst✝⁴ : Preadditive C
inst✝³ : HasFiniteBiproducts C
inst✝² : ∀ (i : ι), InvariantBasisNumber (End (s i))
o : HomOrthogonal s
α β : Type
inst✝¹ : Fintype α
inst✝ : Fintype β
f : α → ι
g : β → ι
i : (⨁ fun a => s (f a)) ≅ ⨁ fun b => s (g b)
c : ι
⊢ Cardinal.mk ↑((fun a => f a) ⁻¹' {c}) = Cardinal.mk ↑(g ⁻¹' {c})
case h
C : Type u
inst✝⁵ : Category C
ι : Type u_1
s : ι → C
inst✝⁴ : Preadditive C
inst✝³ : HasFiniteBiproducts C
inst✝² : ∀ (i : ι), InvariantBasisNumber (End (s i))
o : HomOrthogonal s
α β : Type
inst✝¹ : Fintype α
inst✝ : Fintype β
f : α → ι
g : β → ι
i : (⨁ fun a => s (f a)) ≅ ⨁ fun b => s (g b)
c : ι
⊢ Nonempty (↑((fun a => f a) ⁻¹' {c}) ≃ ↑(g ⁻¹' {c}))
apply Cardinal.eq.1
case h
C : Type u
inst✝⁵ : Category C
ι : Type u_1
s : ι → C
inst✝⁴ : Preadditive C
inst✝³ : HasFiniteBiproducts C
inst✝² : ∀ (i : ι), InvariantBasisNumber (End (s i))
o : HomOrthogonal s
α β : Type
inst✝¹ : Fintype α
inst✝ : Fintype β
f : α → ι
g : β → ι
i : (⨁ fun a => s (f a)) ≅ ⨁ fun b => s (g b)
c : ι
⊢ Fintype.card ↑((fun a => f a) ⁻¹' {c}) = Fintype.card ↑(g ⁻¹' {c})
case h
C : Type u
inst✝⁵ : Category C
ι : Type u_1
s : ι → C
inst✝⁴ : Preadditive C
inst✝³ : HasFiniteBiproducts C
inst✝² : ∀ (i : ι), InvariantBasisNumber (End (s i))
o : HomOrthogonal s
α β : Type
inst✝¹ : Fintype α
inst✝ : Fintype β
f : α → ι
g : β → ι
i : (⨁ fun a => s (f a)) ≅ ⨁ fun b => s (g b)
c : ι
⊢ Cardinal.mk ↑((fun a => f a) ⁻¹' {c}) = Cardinal.mk ↑(g ⁻¹' {c})
simp only [Cardinal.mk_fintype, Nat.cast_inj]
no goals
case h
C : Type u
inst✝⁵ : Category C
ι : Type u_1
s : ι → C
inst✝⁴ : Preadditive C
inst✝³ : HasFiniteBiproducts C
inst✝² : ∀ (i : ι), InvariantBasisNumber (End (s i))
o : HomOrthogonal s
α β : Type
inst✝¹ : Fintype α
inst✝ : Fintype β
f : α → ι
g : β → ι
i : (⨁ fun a => s (f a)) ≅ ⨁ fun b => s (g b)
c : ι
⊢ Fintype.card ↑((fun a => f a) ⁻¹' {c}) = Fintype.card ↑(g ⁻¹' {c})
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)
C : Type u
inst✝⁵ : Category C
ι : Type u_1
s : ι → C
inst✝⁴ : Preadditive C
inst✝³ : HasFiniteBiproducts C
inst✝² : ∀ (i : ι), InvariantBasisNumber (End (s i))
o : HomOrthogonal s
α β : Type
inst✝¹ : Fintype α
inst✝ : Fintype β
f : α → ι
g : β → ι
i : (⨁ fun a => s (f a)) ≅ ⨁ fun b => s (g b)
c : ι
⊢ ↑(matrixDecomposition o) (i.hom ≫ i.inv) c = 1
C : Type u
inst✝⁵ : Category C
ι : Type u_1
s : ι → C
inst✝⁴ : Preadditive C
inst✝³ : HasFiniteBiproducts C
inst✝² : ∀ (i : ι), InvariantBasisNumber (End (s i))
o : HomOrthogonal s
α β : Type
inst✝¹ : Fintype α
inst✝ : Fintype β
f : α → ι
g : β → ι
i : (⨁ fun a => s (f a)) ≅ ⨁ fun b => s (g b)
c : ι
⊢ ↑(matrixDecomposition o) i.inv c ⬝ ↑(matrixDecomposition o) i.hom c = 1
rw [← o.matrixDecomposition_comp]
no goals
C : Type u
inst✝⁵ : Category C
ι : Type u_1
s : ι → C
inst✝⁴ : Preadditive C
inst✝³ : HasFiniteBiproducts C
inst✝² : ∀ (i : ι), InvariantBasisNumber (End (s i))
o : HomOrthogonal s
α β : Type
inst✝¹ : Fintype α
inst✝ : Fintype β
f : α → ι
g : β → ι
i : (⨁ fun a => s (f a)) ≅ ⨁ fun b => s (g b)
c : ι
⊢ ↑(matrixDecomposition o) (i.hom ≫ i.inv) c = 1
simp
C : Type u
inst✝⁵ : Category C
ι : Type u_1
s : ι → C
inst✝⁴ : Preadditive C
inst✝³ : HasFiniteBiproducts C
inst✝² : ∀ (i : ι), InvariantBasisNumber (End (s i))
o : HomOrthogonal s
α β : Type
inst✝¹ : Fintype α
inst✝ : Fintype β
f : α → ι
g : β → ι
i : (⨁ fun a => s (f a)) ≅ ⨁ fun b => s (g b)
c : ι
⊢ ↑(matrixDecomposition o) (i.inv ≫ i.hom) c = 1
C : Type u
inst✝⁵ : Category C
ι : Type u_1
s : ι → C
inst✝⁴ : Preadditive C
inst✝³ : HasFiniteBiproducts C
inst✝² : ∀ (i : ι), InvariantBasisNumber (End (s i))
o : HomOrthogonal s
α β : Type
inst✝¹ : Fintype α
inst✝ : Fintype β
f : α → ι
g : β → ι
i : (⨁ fun a => s (f a)) ≅ ⨁ fun b => s (g b)
c : ι
⊢ ↑(matrixDecomposition o) i.hom c ⬝ ↑(matrixDecomposition o) i.inv c = 1
rw [← o.matrixDecomposition_comp]
no goals
C : Type u
inst✝⁵ : Category C
ι : Type u_1
s : ι → C
inst✝⁴ : Preadditive C
inst✝³ : HasFiniteBiproducts C
inst✝² : ∀ (i : ι), InvariantBasisNumber (End (s i))
o : HomOrthogonal s
α β : Type
inst✝¹ : Fintype α
inst✝ : Fintype β
f : α → ι
g : β → ι
i : (⨁ fun a => s (f a)) ≅ ⨁ fun b => s (g b)
c : ι
⊢ ↑(matrixDecomposition o) (i.inv ≫ i.hom) c = 1
simp