awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.HomOrthogonal (goal)
Goal:
C : Type u
inst : Category.{v, u} C
ι : Type u_1
s : ι → C
inst_1 : Preadditive.{v, u} C
inst_2 : HasFiniteBiproducts.{v, u} C
o : HomOrthogonal.{v, u, u_1} s
α β γ : Type
inst_3 : Finite α
inst_4 : Fintype β
inst_5 : Finite γ
f : α → ι
g : β → ι
h : γ → ι
z : Quiver.Hom.{v, u} (V := C) (biproduct.{0, v, u} fun (a : α) ↦ s (f a)) (biproduct.{0, v, u} fun (b : β) ↦ s (g b))
w : Quiver.Hom.{v, u} (V := C) (biproduct.{0, v, u} fun (b : β) ↦ s (g b)) (biproduct.{0, v, u} fun (c : γ) ↦ s (h c))
c : γ
a : α
j_property_1 : a ∈ f ⁻¹' {h c}
j_property : f a = h c
b : β
nm : ¬g b = h c
⊢ eqToHom ⋯ ≫
      biproduct.ι.{0, v, u} (C := C) (fun (a : α) ↦ s (f a)) a ≫
        z ≫
          ((biproduct.π (fun (b : β) ↦ s (g b)) b ≫ biproduct.ι.{0, v, u} (C := C) (fun (b : β) ↦ s (g b)) b) ≫ w) ≫
            biproduct.π (fun (b : γ) ↦ s (h b)) c =
    0
have a₁ : Eq (α := End (s (h c)))
  (eqToHom sorry ≫
    biproduct.ι.{0, v, u} (C := C) (fun (a : α) ↦ s (f a)) a ≫
      z ≫
        biproduct.π (fun (b : β) ↦ s (g b)) b ≫
          biproduct.ι.{0, v, u} (C := C) (fun (b : β) ↦ s (g b)) b ≫ w ≫ biproduct.π (fun (b : γ) ↦ s (h b)) c)
  0
Tactic: simp only [Category.assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.HomOrthogonal (goal)
Goal:
C : Type u
inst : Category.{v, u} C
ι : Type u_1
s : ι → C
inst_1 : Preadditive.{v, u} C
inst_2 : HasFiniteBiproducts.{v, u} C
o : HomOrthogonal.{v, u, u_1} s
α β γ : Type
inst_3 : Finite α
inst_4 : Fintype β
inst_5 : Finite γ
f : α → ι
g : β → ι
h : γ → ι
z : Quiver.Hom.{v, u} (V := C) (biproduct.{0, v, u} fun (a : α) ↦ s (f a)) (biproduct.{0, v, u} fun (b : β) ↦ s (g b))
w : Quiver.Hom.{v, u} (V := C) (biproduct.{0, v, u} fun (b : β) ↦ s (g b)) (biproduct.{0, v, u} fun (c : γ) ↦ s (h c))
c : γ
a : α
j_property_1 : a ∈ f ⁻¹' {h c}
j_property : f a = h c
b : β
nm : ¬g b = h c
⊢ Eq (α := End (s (h c)))
    (eqToHom ⋯ ≫
      biproduct.ι.{0, v, u} (C := C) (fun (a : α) ↦ s (f a)) a ≫
        z ≫
          biproduct.π (fun (b : β) ↦ s (g b)) b ≫
            biproduct.ι.{0, v, u} (C := C) (fun (b : β) ↦ s (g b)) b ≫ w ≫ biproduct.π (fun (b : γ) ↦ s (h b)) c)
    0
have h₁ : Eq (α := s (f a) ⟶ s (h c))
  (biproduct.ι.{0, v, u} (C := C) (fun (a : α) ↦ s (f a)) a ≫
    z ≫
      biproduct.π (fun (b : β) ↦ s (g b)) b ≫
        biproduct.ι.{0, v, u} (C := C) (fun (b : β) ↦ s (g b)) b ≫ w ≫ biproduct.π (fun (b : γ) ↦ s (h b)) c)
  0
Tactic: convert! comp_zero
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.HomOrthogonal (goal)
Goal:
C : Type u
inst : Category.{v, u} C
ι : Type u_1
s : ι → C
inst_1 : Preadditive.{v, u} C
inst_2 : HasFiniteBiproducts.{v, u} C
o : HomOrthogonal.{v, u, u_1} s
α β γ : Type
inst_3 : Finite α
inst_4 : Fintype β
inst_5 : Finite γ
f : α → ι
g : β → ι
h : γ → ι
z : Quiver.Hom.{v, u} (V := C) (biproduct.{0, v, u} fun (a : α) ↦ s (f a)) (biproduct.{0, v, u} fun (b : β) ↦ s (g b))
w : Quiver.Hom.{v, u} (V := C) (biproduct.{0, v, u} fun (b : β) ↦ s (g b)) (biproduct.{0, v, u} fun (c : γ) ↦ s (h c))
c : γ
a : α
j_property_1 : a ∈ f ⁻¹' {h c}
j_property : f a = h c
b : β
nm : ¬g b = h c
⊢ Eq (α := s (f a) ⟶ s (h c))
    (biproduct.ι.{0, v, u} (C := C) (fun (a : α) ↦ s (f a)) a ≫
      z ≫
        biproduct.π (fun (b : β) ↦ s (g b)) b ≫
          biproduct.ι.{0, v, u} (C := C) (fun (b : β) ↦ s (g b)) b ≫ w ≫ biproduct.π (fun (b : γ) ↦ s (h b)) c)
    0
have h₁ : Eq (α := (biproduct.{0, v, u} fun (a : α) ↦ s (f a)) ⟶ s (h c))
  (z ≫
    biproduct.π (fun (b : β) ↦ s (g b)) b ≫
      biproduct.ι.{0, v, u} (C := C) (fun (b : β) ↦ s (g b)) b ≫ w ≫ biproduct.π (fun (b : γ) ↦ s (h b)) c)
  0
Tactic: convert! comp_zero
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.HomOrthogonal (goal)
Goal:
C : Type u
inst : Category.{v, u} C
ι : Type u_1
s : ι → C
inst_1 : Preadditive.{v, u} C
inst_2 : HasFiniteBiproducts.{v, u} C
o : HomOrthogonal.{v, u, u_1} s
α β γ : Type
inst_3 : Finite α
inst_4 : Fintype β
inst_5 : Finite γ
f : α → ι
g : β → ι
h : γ → ι
z : Quiver.Hom.{v, u} (V := C) (biproduct.{0, v, u} fun (a : α) ↦ s (f a)) (biproduct.{0, v, u} fun (b : β) ↦ s (g b))
w : Quiver.Hom.{v, u} (V := C) (biproduct.{0, v, u} fun (b : β) ↦ s (g b)) (biproduct.{0, v, u} fun (c : γ) ↦ s (h c))
c : γ
a : α
j_property_1 : a ∈ f ⁻¹' {h c}
j_property : f a = h c
b : β
nm : ¬g b = h c
⊢ Eq (α := (biproduct.{0, v, u} fun (a : α) ↦ s (f a)) ⟶ s (h c))
    (z ≫
      biproduct.π (fun (b : β) ↦ s (g b)) b ≫
        biproduct.ι.{0, v, u} (C := C) (fun (b : β) ↦ s (g b)) b ≫ w ≫ biproduct.π (fun (b : γ) ↦ s (h b)) c)
    0
have h₁ : Eq.{v + 1} (α := (biproduct.{0, v, u} fun (b : β) ↦ s (g b)) ⟶ s (h c))
  (biproduct.π (fun (b : β) ↦ s (g b)) b ≫
    biproduct.ι.{0, v, u} (C := C) (fun (b : β) ↦ s (g b)) b ≫ w ≫ biproduct.π (fun (b : γ) ↦ s (h b)) c)
  0
Tactic: convert! comp_zero
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.HomOrthogonal (goal)
Goal:
C : Type u
inst : Category.{v, u} C
ι : Type u_1
s : ι → C
inst_1 : Preadditive.{v, u} C
inst_2 : HasFiniteBiproducts.{v, u} C
o : HomOrthogonal.{v, u, u_1} s
α β γ : Type
inst_3 : Finite α
inst_4 : Fintype β
inst_5 : Finite γ
f : α → ι
g : β → ι
h : γ → ι
z : Quiver.Hom.{v, u} (V := C) (biproduct.{0, v, u} fun (a : α) ↦ s (f a)) (biproduct.{0, v, u} fun (b : β) ↦ s (g b))
w : Quiver.Hom.{v, u} (V := C) (biproduct.{0, v, u} fun (b : β) ↦ s (g b)) (biproduct.{0, v, u} fun (c : γ) ↦ s (h c))
c : γ
a : α
j_property_1 : a ∈ f ⁻¹' {h c}
j_property : f a = h c
b : β
nm : ¬g b = h c
⊢ Eq.{v + 1} (α := (biproduct.{0, v, u} fun (b : β) ↦ s (g b)) ⟶ s (h c))
    (biproduct.π (fun (b : β) ↦ s (g b)) b ≫
      biproduct.ι.{0, v, u} (C := C) (fun (b : β) ↦ s (g b)) b ≫ w ≫ biproduct.π (fun (b : γ) ↦ s (h b)) c)
    0
have h₁ : biproduct.ι.{0, v, u} (C := C) (fun (b : β) ↦ s (g b)) b ≫ w ≫ biproduct.π (fun (b : γ) ↦ s (h b)) c = 0
Tactic: convert! comp_zero
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.HomOrthogonal (goal)
Goal:
C : Type u
inst : Category.{v, u} C
ι : Type u_1
s : ι → C
inst_1 : Preadditive.{v, u} C
inst_2 : HasFiniteBiproducts.{v, u} C
R : Type u_2
inst_3 : Semiring R
inst_4 : Linear.{u_2, v, u} R C
o : HomOrthogonal.{v, u, u_1} s
α β : Type
inst_5 : Finite α
inst_6 : Finite β
f : α → ι
g : β → ι
w : R
z : Quiver.Hom.{v, u} (V := C) (biproduct.{0, v, u} fun (a : α) ↦ s (f a)) (biproduct.{0, v, u} fun (b : β) ↦ s (g b))
⊢ Equiv.toFun
      (AddEquiv.toEquiv
        (o.matrixDecompositionAddEquiv :
          Quiver.Hom.{v, u} (V := C) (biproduct.{0, v, u} fun (a : α) ↦ s (f a))
              (biproduct.{0, v, u} fun (b : β) ↦ s (g b)) ≃+
            ((i : ι) → Matrix (↑(g ⁻¹' {i}) : Type) (↑(f ⁻¹' {i}) : Type) (End (s i)))))
      (w • z) =
    HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) w : R)
      (Equiv.toFun
        (AddEquiv.toEquiv
          (o.matrixDecompositionAddEquiv :
            Quiver.Hom.{v, u} (V := C) (biproduct.{0, v, u} fun (a : α) ↦ s (f a))
                (biproduct.{0, v, u} fun (b : β) ↦ s (g b)) ≃+
              ((i : ι) → Matrix (↑(g ⁻¹' {i}) : Type) (↑(f ⁻¹' {i}) : Type) (End (s i)))))
        z)
have h : ∀ (x : ι) (i : (↑(g ⁻¹' {x}) : Type)) (j : (↑(f ⁻¹' {x}) : Type)),
  Equiv.toFun
      (AddEquiv.toEquiv
        (o.matrixDecompositionAddEquiv :
          Quiver.Hom.{v, u} (V := C) (biproduct.{0, v, u} fun (a : α) ↦ s (f a))
              (biproduct.{0, v, u} fun (b : β) ↦ s (g b)) ≃+
            ((i : ι) → Matrix (↑(g ⁻¹' {i}) : Type) (↑(f ⁻¹' {i}) : Type) (End (s i)))))
      (w • z) x i j =
    HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) w : R)
      (Equiv.toFun
        (AddEquiv.toEquiv
          (o.matrixDecompositionAddEquiv :
            Quiver.Hom.{v, u} (V := C) (biproduct.{0, v, u} fun (a : α) ↦ s (f a))
                (biproduct.{0, v, u} fun (b : β) ↦ s (g b)) ≃+
              ((i : ι) → Matrix (↑(g ⁻¹' {i}) : Type) (↑(f ⁻¹' {i}) : Type) (End (s i)))))
        z)
      x i j
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.HomOrthogonal (goal)
Goal:
C : Type u
inst : Category.{v, u} C
ι : Type u_1
s : ι → C
inst_1 : Preadditive.{v, u} C
inst_2 : HasFiniteBiproducts.{v, u} C
R : Type u_2
inst_3 : Semiring R
inst_4 : Linear.{u_2, v, u} R C
o : HomOrthogonal.{v, u, u_1} s
α β : Type
inst_5 : Finite α
inst_6 : Finite β
f : α → ι
g : β → ι
w : R
z : Quiver.Hom.{v, u} (V := C) (biproduct.{0, v, u} fun (a : α) ↦ s (f a)) (biproduct.{0, v, u} fun (b : β) ↦ s (g b))
x : ι
i : (↑(g ⁻¹' {x}) : Type)
j : (↑(f ⁻¹' {x}) : Type)
⊢ Equiv.toFun
      (AddEquiv.toEquiv
        (o.matrixDecompositionAddEquiv :
          Quiver.Hom.{v, u} (V := C) (biproduct.{0, v, u} fun (a : α) ↦ s (f a))
              (biproduct.{0, v, u} fun (b : β) ↦ s (g b)) ≃+
            ((i : ι) → Matrix (↑(g ⁻¹' {i}) : Type) (↑(f ⁻¹' {i}) : Type) (End (s i)))))
      (w • z) x i j =
    HSMul.hSMul (α := R) ((RingHom.id R : (a : R) → R) w : R)
      (Equiv.toFun
        (AddEquiv.toEquiv
          (o.matrixDecompositionAddEquiv :
            Quiver.Hom.{v, u} (V := C) (biproduct.{0, v, u} fun (a : α) ↦ s (f a))
                (biproduct.{0, v, u} fun (b : β) ↦ s (g b)) ≃+
              ((i : ι) → Matrix (↑(g ⁻¹' {i}) : Type) (↑(f ⁻¹' {i}) : Type) (End (s i)))))
        z)
      x i j
have h : eqToHom sorry ≫
    (biproduct.ι.{0, v, u} (C := C) (fun (a : α) ↦ s (f a)) (↑j : α) ≫
        (w • z) ≫ biproduct.π (fun (b : β) ↦ s (g b)) (↑i : β)) ≫
      eqToHom sorry =
  w •
    eqToHom sorry ≫
      (biproduct.ι.{0, v, u} (C := C) (fun (a : α) ↦ s (f a)) (↑j : α) ≫
          z ≫ biproduct.π (fun (b : β) ↦ s (g b)) (↑i : β)) ≫
        eqToHom sorry
Tactic: dsimp [biproduct.components]
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.HomOrthogonal (goal)
Goal:
C : Type u
inst : Category.{v, u} C
ι : Type u_1
s : ι → C
inst_1 : Preadditive.{v, u} C
inst_2 : HasFiniteBiproducts.{v, u} C
inst_3 : ∀ (i : ι), InvariantBasisNumber.{v} (End (s i))
o : HomOrthogonal.{v, u, u_1} s
α β : Type
inst_4 : Finite α
inst_5 : Finite β
f : α → ι
g : β → ι
i : Iso.{v, u} (C := C) (biproduct.{0, v, u} fun (a : α) ↦ s (f a)) (biproduct.{0, v, u} fun (b : β) ↦ s (g b))
⊢ ∃ (e : α ≃ β), ∀ (a : α), g ((e : (a : α) → β) a) = f a
have refine : (c : ι) → (↑(f ⁻¹' {c}) : Type) ≃ (↑(g ⁻¹' {c}) : Type)
Tactic: refine ⟨Equiv.ofPreimageEquiv ?_, fun a => Equiv.ofPreimageEquiv_map _ _⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.HomOrthogonal (goal)
Goal:
C : Type u
inst : Category.{v, u} C
ι : Type u_1
s : ι → C
inst_1 : Preadditive.{v, u} C
inst_2 : HasFiniteBiproducts.{v, u} C
inst_3 : ∀ (i : ι), InvariantBasisNumber.{v} (End (s i))
o : HomOrthogonal.{v, u, u_1} s
α β : Type
inst_4 : Finite α
inst_5 : Finite β
f : α → ι
g : β → ι
i : Iso.{v, u} (C := C) (biproduct.{0, v, u} fun (a : α) ↦ s (f a)) (biproduct.{0, v, u} fun (b : β) ↦ s (g b))
c : ι
⊢ (↑(f ⁻¹' {c}) : Type) ≃ (↑(g ⁻¹' {c}) : Type)
have h : Nonempty ((↑(f ⁻¹' {c}) : Type) ≃ (↑(g ⁻¹' {c}) : Type))
Tactic: apply Nonempty.some
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.HomOrthogonal (goal)
Goal:
C : Type u
inst : Category.{v, u} C
ι : Type u_1
s : ι → C
inst_1 : Preadditive.{v, u} C
inst_2 : HasFiniteBiproducts.{v, u} C
inst_3 : ∀ (i : ι), InvariantBasisNumber.{v} (End (s i))
o : HomOrthogonal.{v, u, u_1} s
α β : Type
inst_4 : Finite α
inst_5 : Finite β
f : α → ι
g : β → ι
i : Iso.{v, u} (C := C) (biproduct.{0, v, u} fun (a : α) ↦ s (f a)) (biproduct.{0, v, u} fun (b : β) ↦ s (g b))
c : ι
⊢ Nonempty ((↑(f ⁻¹' {c}) : Type) ≃ (↑(g ⁻¹' {c}) : Type))
have h : Cardinal.mk (↑(f ⁻¹' {c}) : Type) = Cardinal.mk (↑(g ⁻¹' {c}) : Type)
Tactic: apply Cardinal.eq.1
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.HomOrthogonal (goal)
Goal:
C : Type u
inst : Category.{v, u} C
ι : Type u_1
s : ι → C
inst_1 : Preadditive.{v, u} C
inst_2 : HasFiniteBiproducts.{v, u} C
inst_3 : ∀ (i : ι), InvariantBasisNumber.{v} (End (s i))
o : HomOrthogonal.{v, u, u_1} s
α β : Type
inst_4 : Finite α
inst_5 : Finite β
f : α → ι
g : β → ι
i : Iso.{v, u} (C := C) (biproduct.{0, v, u} fun (a : α) ↦ s (f a)) (biproduct.{0, v, u} fun (b : β) ↦ s (g b))
c : ι
⊢ Cardinal.mk (↑(f ⁻¹' {c}) : Type) = Cardinal.mk (↑(g ⁻¹' {c}) : Type)
have h : ∀ (val : Fintype α), Cardinal.mk (↑(f ⁻¹' {c}) : Type) = Cardinal.mk (↑(g ⁻¹' {c}) : Type)
Tactic: cases nonempty_fintype α
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.HomOrthogonal (goal)
Goal:
C : Type u
inst : Category.{v, u} C
ι : Type u_1
s : ι → C
inst_1 : Preadditive.{v, u} C
inst_2 : HasFiniteBiproducts.{v, u} C
inst_3 : ∀ (i : ι), InvariantBasisNumber.{v} (End (s i))
o : HomOrthogonal.{v, u, u_1} s
α β : Type
inst_4 : Finite α
inst_5 : Finite β
f : α → ι
g : β → ι
i : Iso.{v, u} (C := C) (biproduct.{0, v, u} fun (a : α) ↦ s (f a)) (biproduct.{0, v, u} fun (b : β) ↦ s (g b))
c : ι
val : Fintype α
⊢ Cardinal.mk (↑(f ⁻¹' {c}) : Type) = Cardinal.mk (↑(g ⁻¹' {c}) : Type)
have h : ∀ (val : Fintype β), Cardinal.mk (↑(f ⁻¹' {c}) : Type) = Cardinal.mk (↑(g ⁻¹' {c}) : Type)
Tactic: cases nonempty_fintype β
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.HomOrthogonal (goal)
Goal:
C : Type u
inst : Category.{v, u} C
ι : Type u_1
s : ι → C
inst_1 : Preadditive.{v, u} C
inst_2 : HasFiniteBiproducts.{v, u} C
inst_3 : ∀ (i : ι), InvariantBasisNumber.{v} (End (s i))
o : HomOrthogonal.{v, u, u_1} s
α β : Type
inst_4 : Finite α
inst_5 : Finite β
f : α → ι
g : β → ι
i : Iso.{v, u} (C := C) (biproduct.{0, v, u} fun (a : α) ↦ s (f a)) (biproduct.{0, v, u} fun (b : β) ↦ s (g b))
c : ι
val : Fintype α
val_1 : Fintype β
⊢ Cardinal.mk (↑(f ⁻¹' {c}) : Type) = Cardinal.mk (↑(g ⁻¹' {c}) : Type)
have h : Fintype.card (↑(f ⁻¹' {c}) : Type) = Fintype.card (↑(g ⁻¹' {c}) : Type)
Tactic: simp only [Cardinal.mk_fintype, Nat.cast_inj]
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.HomOrthogonal (goal)
Goal:
C : Type u
inst : Category.{v, u} C
ι : Type u_1
s : ι → C
inst_1 : Preadditive.{v, u} C
inst_2 : HasFiniteBiproducts.{v, u} C
inst_3 : ∀ (i : ι), InvariantBasisNumber.{v} (End (s i))
o : HomOrthogonal.{v, u, u_1} s
α β : Type
inst_4 : Finite α
inst_5 : Finite β
f : α → ι
g : β → ι
i : Iso.{v, u} (C := C) (biproduct.{0, v, u} fun (a : α) ↦ s (f a)) (biproduct.{0, v, u} fun (b : β) ↦ s (g b))
c : ι
val : Fintype α
val_1 : Fintype β
⊢ HMul.hMul (α := Matrix (↑(f ⁻¹' {c}) : Type) (↑(g ⁻¹' {c}) : Type) (End (s c))) (β :=
      Matrix (↑(g ⁻¹' {c}) : Type) (↑(f ⁻¹' {c}) : Type) (End (s c)))
      (((o.matrixDecomposition :
              Quiver.Hom.{v, u} (V := C) (biproduct.{0, v, u} fun (a : β) ↦ s (g a))
                  (biproduct.{0, v, u} fun (b : α) ↦ s (f b)) ≃
                ((i : ι) → Matrix (↑(f ⁻¹' {i}) : Type) (↑(g ⁻¹' {i}) : Type) (End (s i)))) :
            (a : (⨁ fun (a : β) ↦ s (g a)) ⟶ ⨁ fun (b : α) ↦ s (f b)) →
              (i : ι) → Matrix (↑(f ⁻¹' {i}) : Type) (↑(g ⁻¹' {i}) : Type) (End (s i)))
          i.inv c :
        Matrix (↑(f ⁻¹' {c}) : Type) (↑(g ⁻¹' {c}) : Type) (End (s c)))
      (((o.matrixDecomposition :
              Quiver.Hom.{v, u} (V := C) (biproduct.{0, v, u} fun (a : α) ↦ s (f a))
                  (biproduct.{0, v, u} fun (b : β) ↦ s (g b)) ≃
                ((i : ι) → Matrix (↑(g ⁻¹' {i}) : Type) (↑(f ⁻¹' {i}) : Type) (End (s i)))) :
            (a : (⨁ fun (a : α) ↦ s (f a)) ⟶ ⨁ fun (b : β) ↦ s (g b)) →
              (i : ι) → Matrix (↑(g ⁻¹' {i}) : Type) (↑(f ⁻¹' {i}) : Type) (End (s i)))
          i.hom c :
        Matrix (↑(g ⁻¹' {c}) : Type) (↑(f ⁻¹' {c}) : Type) (End (s c))) =
    1
have rw : Eq.{max 1 (v + 1)} (α := Matrix (↑(f ⁻¹' {c}) : Type) (↑(f ⁻¹' {c}) : Type) (End (s c)))
  (((o.matrixDecomposition :
          Quiver.Hom.{v, u} (V := C) (biproduct.{0, v, u} fun (a : α) ↦ s (f a))
              (biproduct.{0, v, u} fun (b : α) ↦ s (f b)) ≃
            ((i : ι) → Matrix (↑(f ⁻¹' {i}) : Type) (↑(f ⁻¹' {i}) : Type) (End (s i)))) :
        (a : (⨁ fun (a : α) ↦ s (f a)) ⟶ ⨁ fun (b : α) ↦ s (f b)) →
          (i : ι) → Matrix (↑(f ⁻¹' {i}) : Type) (↑(f ⁻¹' {i}) : Type) (End (s i)))
      (i.hom ≫ i.inv) c :
    Matrix (↑(f ⁻¹' {c}) : Type) (↑(f ⁻¹' {c}) : Type) (End (s c)))
  (1 : Matrix (↑(f ⁻¹' {c}) : Type) (↑(f ⁻¹' {c}) : Type) (End (s c)))
Tactic: rw [← o.matrixDecomposition_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.HomOrthogonal (goal)
Goal:
C : Type u
inst : Category.{v, u} C
ι : Type u_1
s : ι → C
inst_1 : Preadditive.{v, u} C
inst_2 : HasFiniteBiproducts.{v, u} C
inst_3 : ∀ (i : ι), InvariantBasisNumber.{v} (End (s i))
o : HomOrthogonal.{v, u, u_1} s
α β : Type
inst_4 : Finite α
inst_5 : Finite β
f : α → ι
g : β → ι
i : Iso.{v, u} (C := C) (biproduct.{0, v, u} fun (a : α) ↦ s (f a)) (biproduct.{0, v, u} fun (b : β) ↦ s (g b))
c : ι
val : Fintype α
val_1 : Fintype β
⊢ HMul.hMul (α := Matrix (↑(g ⁻¹' {c}) : Type) (↑(f ⁻¹' {c}) : Type) (End (s c))) (β :=
      Matrix (↑(f ⁻¹' {c}) : Type) (↑(g ⁻¹' {c}) : Type) (End (s c)))
      (((o.matrixDecomposition :
              Quiver.Hom.{v, u} (V := C) (biproduct.{0, v, u} fun (a : α) ↦ s (f a))
                  (biproduct.{0, v, u} fun (b : β) ↦ s (g b)) ≃
                ((i : ι) → Matrix (↑(g ⁻¹' {i}) : Type) (↑(f ⁻¹' {i}) : Type) (End (s i)))) :
            (a : (⨁ fun (a : α) ↦ s (f a)) ⟶ ⨁ fun (b : β) ↦ s (g b)) →
              (i : ι) → Matrix (↑(g ⁻¹' {i}) : Type) (↑(f ⁻¹' {i}) : Type) (End (s i)))
          i.hom c :
        Matrix (↑(g ⁻¹' {c}) : Type) (↑(f ⁻¹' {c}) : Type) (End (s c)))
      (((o.matrixDecomposition :
              Quiver.Hom.{v, u} (V := C) (biproduct.{0, v, u} fun (a : β) ↦ s (g a))
                  (biproduct.{0, v, u} fun (b : α) ↦ s (f b)) ≃
                ((i : ι) → Matrix (↑(f ⁻¹' {i}) : Type) (↑(g ⁻¹' {i}) : Type) (End (s i)))) :
            (a : (⨁ fun (a : β) ↦ s (g a)) ⟶ ⨁ fun (b : α) ↦ s (f b)) →
              (i : ι) → Matrix (↑(f ⁻¹' {i}) : Type) (↑(g ⁻¹' {i}) : Type) (End (s i)))
          i.inv c :
        Matrix (↑(f ⁻¹' {c}) : Type) (↑(g ⁻¹' {c}) : Type) (End (s c))) =
    1
have rw : Eq.{max 1 (v + 1)} (α := Matrix (↑(g ⁻¹' {c}) : Type) (↑(g ⁻¹' {c}) : Type) (End (s c)))
  (((o.matrixDecomposition :
          Quiver.Hom.{v, u} (V := C) (biproduct.{0, v, u} fun (a : β) ↦ s (g a))
              (biproduct.{0, v, u} fun (b : β) ↦ s (g b)) ≃
            ((i : ι) → Matrix (↑(g ⁻¹' {i}) : Type) (↑(g ⁻¹' {i}) : Type) (End (s i)))) :
        (a : (⨁ fun (a : β) ↦ s (g a)) ⟶ ⨁ fun (b : β) ↦ s (g b)) →
          (i : ι) → Matrix (↑(g ⁻¹' {i}) : Type) (↑(g ⁻¹' {i}) : Type) (End (s i)))
      (i.inv ≫ i.hom) c :
    Matrix (↑(g ⁻¹' {c}) : Type) (↑(g ⁻¹' {c}) : Type) (End (s c)))
  (1 : Matrix (↑(g ⁻¹' {c}) : Type) (↑(g ⁻¹' {c}) : Type) (End (s c)))
Tactic: rw [← o.matrixDecomposition_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.HomOrthogonal (goal)
Goal:
C : Type u
inst : Category.{v, u} C
ι : Type u_1
s : ι → C
inst_1 : Preadditive.{v, u} C
inst_2 : HasFiniteBiproducts.{v, u} C
inst_3 : ∀ (i : ι), InvariantBasisNumber.{v} (End (s i))
o : HomOrthogonal.{v, u, u_1} s
α β : Type
inst_4 : Finite α
inst_5 : Finite β
f : α → ι
g : β → ι
i : Iso.{v, u} (C := C) (biproduct.{0, v, u} fun (a : α) ↦ s (f a)) (biproduct.{0, v, u} fun (b : β) ↦ s (g b))
⊢ ∃ (e : α ≃ β), ∀ (a : α), g ((e : (a : α) → β) a) = f a
have refine : (c : ι) → (↑(f ⁻¹' {c}) : Type) ≃ (↑(g ⁻¹' {c}) : Type)
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)
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.HomOrthogonal (goal)
Goal:
C : Type u
inst : Category.{v, u} C
ι : Type u_1
s : ι → C
inst_1 : Preadditive.{v, u} C
inst_2 : HasFiniteBiproducts.{v, u} C
inst_3 : ∀ (i : ι), InvariantBasisNumber.{v} (End (s i))
o : HomOrthogonal.{v, u, u_1} s
α β : Type
inst_4 : Finite α
inst_5 : Finite β
f : α → ι
g : β → ι
i : Iso.{v, u} (C := C) (biproduct.{0, v, u} fun (a : α) ↦ s (f a)) (biproduct.{0, v, u} fun (b : β) ↦ s (g b))
refine refine₁ : (c : ι) → (↑(f ⁻¹' {c}) : Type) ≃ (↑(g ⁻¹' {c}) : Type)
⊢ ∃ (e : α ≃ β), ∀ (a : α), g ((e : (a : α) → β) a) = f a
have h : ∀ (c : ι), Nonempty ((↑(f ⁻¹' {c}) : Type) ≃ (↑(g ⁻¹' {c}) : Type))
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)
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.HomOrthogonal (goal)
Goal:
C : Type u
inst : Category.{v, u} C
ι : Type u_1
s : ι → C
inst_1 : Preadditive.{v, u} C
inst_2 : HasFiniteBiproducts.{v, u} C
inst_3 : ∀ (i : ι), InvariantBasisNumber.{v} (End (s i))
o : HomOrthogonal.{v, u, u_1} s
α β : Type
inst_4 : Finite α
inst_5 : Finite β
f : α → ι
g : β → ι
i : Iso.{v, u} (C := C) (biproduct.{0, v, u} fun (a : α) ↦ s (f a)) (biproduct.{0, v, u} fun (b : β) ↦ s (g b))
refine refine₁ : (c : ι) → (↑(f ⁻¹' {c}) : Type) ≃ (↑(g ⁻¹' {c}) : Type)
h : ∀ (c : ι), Nonempty ((↑(f ⁻¹' {c}) : Type) ≃ (↑(g ⁻¹' {c}) : Type))
⊢ ∃ (e : α ≃ β), ∀ (a : α), g ((e : (a : α) → β) a) = f a
have h₁ : ∀ (c : ι), Cardinal.mk (↑(f ⁻¹' {c}) : Type) = Cardinal.mk (↑(g ⁻¹' {c}) : Type)
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)
-- Lean 4 proof step from Mathlib.CategoryTheory.Preadditive.HomOrthogonal (goal)
Goal:
C : Type u
inst : Category.{v, u} C
ι : Type u_1
s : ι → C
inst_1 : Preadditive.{v, u} C
inst_2 : HasFiniteBiproducts.{v, u} C
inst_3 : ∀ (i : ι), InvariantBasisNumber.{v} (End (s i))
o : HomOrthogonal.{v, u, u_1} s
α β : Type
inst_4 : Finite α
inst_5 : Finite β
f : α → ι
g : β → ι
i : Iso.{v, u} (C := C) (biproduct.{0, v, u} fun (a : α) ↦ s (f a)) (biproduct.{0, v, u} fun (b : β) ↦ s (g b))
refine refine₁ : (c : ι) → (↑(f ⁻¹' {c}) : Type) ≃ (↑(g ⁻¹' {c}) : Type)
h : ∀ (c : ι), Nonempty ((↑(f ⁻¹' {c}) : Type) ≃ (↑(g ⁻¹' {c}) : Type))
h₁ : ∀ (c : ι), Cardinal.mk (↑(f ⁻¹' {c}) : Type) = Cardinal.mk (↑(g ⁻¹' {c}) : Type)
⊢ ∃ (e : α ≃ β), ∀ (a : α), g ((e : (a : α) → β) a) = f a
have h₂ : ∀ (c : ι) (val : Fintype α), Cardinal.mk (↑(f ⁻¹' {c}) : Type) = Cardinal.mk (↑(g ⁻¹' {c}) : Type)
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)