case mp
C : Type u₁
inst✝¹ : Category C
D : Type u₂
inst✝ : Category D
P Q : C
S T : D
f : (P, S) ⟶ (Q, T)
⊢ IsIso f → IsIso f.fst ∧ IsIso f.snd

case mpr
C : Type u₁
inst✝¹ : Category C
D : Type u₂
inst✝ : Category D
P Q : C
S T : D
f : (P, S) ⟶ (Q, T)
⊢ IsIso f.fst ∧ IsIso f.snd → IsIso f
C : Type u₁
inst✝¹ : Category C
D : Type u₂
inst✝ : Category D
P Q : C
S T : D
f : (P, S) ⟶ (Q, T)
⊢ IsIso f ↔ IsIso f.fst ∧ IsIso f.snd
constructor
case mp.mk.intro.intro
C : Type u₁
inst✝¹ : Category C
D : Type u₂
inst✝ : Category D
P Q : C
S T : D
f : (P, S) ⟶ (Q, T)
g : (Q, T) ⟶ (P, S)
hfg : f ≫ g = 𝟙 (P, S)
hgf : g ≫ f = 𝟙 (Q, T)
⊢ IsIso f.fst ∧ IsIso f.snd
case mp
C : Type u₁
inst✝¹ : Category C
D : Type u₂
inst✝ : Category D
P Q : C
S T : D
f : (P, S) ⟶ (Q, T)
⊢ IsIso f → IsIso f.fst ∧ IsIso f.snd
rintro ⟨g, hfg, hgf⟩
case mp.mk.intro.intro
C : Type u₁
inst✝¹ : Category C
D : Type u₂
inst✝ : Category D
P Q : C
S T : D
f : (P, S) ⟶ (Q, T)
g : (Q, T) ⟶ (P, S)
hfg : f.fst ≫ g.fst = 𝟙 P ∧ f.snd ≫ g.snd = 𝟙 S
hgf : g.fst ≫ f.fst = 𝟙 Q ∧ g.snd ≫ f.snd = 𝟙 T
⊢ IsIso f.fst ∧ IsIso f.snd
case mp.mk.intro.intro
C : Type u₁
inst✝¹ : Category C
D : Type u₂
inst✝ : Category D
P Q : C
S T : D
f : (P, S) ⟶ (Q, T)
g : (Q, T) ⟶ (P, S)
hfg : f ≫ g = 𝟙 (P, S)
hgf : g ≫ f = 𝟙 (Q, T)
⊢ IsIso f.fst ∧ IsIso f.snd
simp at hfg hgf
case mp.mk.intro.intro.intro
C : Type u₁
inst✝¹ : Category C
D : Type u₂
inst✝ : Category D
P Q : C
S T : D
f : (P, S) ⟶ (Q, T)
g : (Q, T) ⟶ (P, S)
hgf : g.fst ≫ f.fst = 𝟙 Q ∧ g.snd ≫ f.snd = 𝟙 T
hfg₁ : f.fst ≫ g.fst = 𝟙 P
hfg₂ : f.snd ≫ g.snd = 𝟙 S
⊢ IsIso f.fst ∧ IsIso f.snd
case mp.mk.intro.intro
C : Type u₁
inst✝¹ : Category C
D : Type u₂
inst✝ : Category D
P Q : C
S T : D
f : (P, S) ⟶ (Q, T)
g : (Q, T) ⟶ (P, S)
hfg : f.fst ≫ g.fst = 𝟙 P ∧ f.snd ≫ g.snd = 𝟙 S
hgf : g.fst ≫ f.fst = 𝟙 Q ∧ g.snd ≫ f.snd = 𝟙 T
⊢ IsIso f.fst ∧ IsIso f.snd
rcases hfg with ⟨hfg₁, hfg₂⟩
case mp.mk.intro.intro.intro.intro
C : Type u₁
inst✝¹ : Category C
D : Type u₂
inst✝ : Category D
P Q : C
S T : D
f : (P, S) ⟶ (Q, T)
g : (Q, T) ⟶ (P, S)
hfg₁ : f.fst ≫ g.fst = 𝟙 P
hfg₂ : f.snd ≫ g.snd = 𝟙 S
hgf₁ : g.fst ≫ f.fst = 𝟙 Q
hgf₂ : g.snd ≫ f.snd = 𝟙 T
⊢ IsIso f.fst ∧ IsIso f.snd
case mp.mk.intro.intro.intro
C : Type u₁
inst✝¹ : Category C
D : Type u₂
inst✝ : Category D
P Q : C
S T : D
f : (P, S) ⟶ (Q, T)
g : (Q, T) ⟶ (P, S)
hgf : g.fst ≫ f.fst = 𝟙 Q ∧ g.snd ≫ f.snd = 𝟙 T
hfg₁ : f.fst ≫ g.fst = 𝟙 P
hfg₂ : f.snd ≫ g.snd = 𝟙 S
⊢ IsIso f.fst ∧ IsIso f.snd
rcases hgf with ⟨hgf₁, hgf₂⟩
no goals
case mp.mk.intro.intro.intro.intro
C : Type u₁
inst✝¹ : Category C
D : Type u₂
inst✝ : Category D
P Q : C
S T : D
f : (P, S) ⟶ (Q, T)
g : (Q, T) ⟶ (P, S)
hfg₁ : f.fst ≫ g.fst = 𝟙 P
hfg₂ : f.snd ≫ g.snd = 𝟙 S
hgf₁ : g.fst ≫ f.fst = 𝟙 Q
hgf₂ : g.snd ≫ f.snd = 𝟙 T
⊢ IsIso f.fst ∧ IsIso f.snd
exact ⟨⟨⟨g.1, hfg₁, hgf₁⟩⟩, ⟨⟨g.2, hfg₂, hgf₂⟩⟩⟩
case mpr.intro.mk.intro.intro.mk.intro.intro
C : Type u₁
inst✝¹ : Category C
D : Type u₂
inst✝ : Category D
P Q : C
S T : D
f : (P, S) ⟶ (Q, T)
g₁ : (Q, T).fst ⟶ (P, S).fst
hfg₁ : f.fst ≫ g₁ = 𝟙 (P, S).fst
hgf₁ : g₁ ≫ f.fst = 𝟙 (Q, T).fst
g₂ : (Q, T).snd ⟶ (P, S).snd
hfg₂ : f.snd ≫ g₂ = 𝟙 (P, S).snd
hgf₂ : g₂ ≫ f.snd = 𝟙 (Q, T).snd
⊢ IsIso f
case mpr
C : Type u₁
inst✝¹ : Category C
D : Type u₂
inst✝ : Category D
P Q : C
S T : D
f : (P, S) ⟶ (Q, T)
⊢ IsIso f.fst ∧ IsIso f.snd → IsIso f
rintro ⟨⟨g₁, hfg₁, hgf₁⟩, ⟨g₂, hfg₂, hgf₂⟩⟩
case mpr.intro.mk.intro.intro.mk.intro.intro
C : Type u₁
inst✝¹ : Category C
D : Type u₂
inst✝ : Category D
P Q : C
S T : D
f : (P, S) ⟶ (Q, T)
g₁ : (Q, T).fst ⟶ (P, S).fst
hfg₁ : f.fst ≫ g₁ = 𝟙 P
hgf₁ : g₁ ≫ f.fst = 𝟙 Q
g₂ : (Q, T).snd ⟶ (P, S).snd
hfg₂ : f.snd ≫ g₂ = 𝟙 S
hgf₂ : g₂ ≫ f.snd = 𝟙 T
⊢ IsIso f
case mpr.intro.mk.intro.intro.mk.intro.intro
C : Type u₁
inst✝¹ : Category C
D : Type u₂
inst✝ : Category D
P Q : C
S T : D
f : (P, S) ⟶ (Q, T)
g₁ : (Q, T).fst ⟶ (P, S).fst
hfg₁ : f.fst ≫ g₁ = 𝟙 (P, S).fst
hgf₁ : g₁ ≫ f.fst = 𝟙 (Q, T).fst
g₂ : (Q, T).snd ⟶ (P, S).snd
hfg₂ : f.snd ≫ g₂ = 𝟙 (P, S).snd
hgf₂ : g₂ ≫ f.snd = 𝟙 (Q, T).snd
⊢ IsIso f
dsimp at hfg₁ hgf₁ hfg₂ hgf₂
case mpr.intro.mk.intro.intro.mk.intro.intro.refine'_1
C : Type u₁
inst✝¹ : Category C
D : Type u₂
inst✝ : Category D
P Q : C
S T : D
f : (P, S) ⟶ (Q, T)
g₁ : (Q, T).fst ⟶ (P, S).fst
hfg₁ : f.fst ≫ g₁ = 𝟙 P
hgf₁ : g₁ ≫ f.fst = 𝟙 Q
g₂ : (Q, T).snd ⟶ (P, S).snd
hfg₂ : f.snd ≫ g₂ = 𝟙 S
hgf₂ : g₂ ≫ f.snd = 𝟙 T
⊢ f ≫ (g₁, g₂) = 𝟙 (P, S)

case mpr.intro.mk.intro.intro.mk.intro.intro.refine'_2
C : Type u₁
inst✝¹ : Category C
D : Type u₂
inst✝ : Category D
P Q : C
S T : D
f : (P, S) ⟶ (Q, T)
g₁ : (Q, T).fst ⟶ (P, S).fst
hfg₁ : f.fst ≫ g₁ = 𝟙 P
hgf₁ : g₁ ≫ f.fst = 𝟙 Q
g₂ : (Q, T).snd ⟶ (P, S).snd
hfg₂ : f.snd ≫ g₂ = 𝟙 S
hgf₂ : g₂ ≫ f.snd = 𝟙 T
⊢ (g₁, g₂) ≫ f = 𝟙 (Q, T)
case mpr.intro.mk.intro.intro.mk.intro.intro
C : Type u₁
inst✝¹ : Category C
D : Type u₂
inst✝ : Category D
P Q : C
S T : D
f : (P, S) ⟶ (Q, T)
g₁ : (Q, T).fst ⟶ (P, S).fst
hfg₁ : f.fst ≫ g₁ = 𝟙 P
hgf₁ : g₁ ≫ f.fst = 𝟙 Q
g₂ : (Q, T).snd ⟶ (P, S).snd
hfg₂ : f.snd ≫ g₂ = 𝟙 S
hgf₂ : g₂ ≫ f.snd = 𝟙 T
⊢ IsIso f
refine' ⟨⟨(g₁, g₂), _, _⟩⟩
no goals
case mpr.intro.mk.intro.intro.mk.intro.intro.refine'_1
C : Type u₁
inst✝¹ : Category C
D : Type u₂
inst✝ : Category D
P Q : C
S T : D
f : (P, S) ⟶ (Q, T)
g₁ : (Q, T).fst ⟶ (P, S).fst
hfg₁ : f.fst ≫ g₁ = 𝟙 P
hgf₁ : g₁ ≫ f.fst = 𝟙 Q
g₂ : (Q, T).snd ⟶ (P, S).snd
hfg₂ : f.snd ≫ g₂ = 𝟙 S
hgf₂ : g₂ ≫ f.snd = 𝟙 T
⊢ f ≫ (g₁, g₂) = 𝟙 (P, S)

case mpr.intro.mk.intro.intro.mk.intro.intro.refine'_2
C : Type u₁
inst✝¹ : Category C
D : Type u₂
inst✝ : Category D
P Q : C
S T : D
f : (P, S) ⟶ (Q, T)
g₁ : (Q, T).fst ⟶ (P, S).fst
hfg₁ : f.fst ≫ g₁ = 𝟙 P
hgf₁ : g₁ ≫ f.fst = 𝟙 Q
g₂ : (Q, T).snd ⟶ (P, S).snd
hfg₂ : f.snd ≫ g₂ = 𝟙 S
hgf₂ : g₂ ≫ f.snd = 𝟙 T
⊢ (g₁, g₂) ≫ f = 𝟙 (Q, T)
repeat { simp; constructor; assumption; assumption }