Module: Mathlib.Algebra.Exact.Basic

Goal state before:
pp: case refine_5.fst
R✝ : Type u_1
M✝ : Type u_2
M' : Type u_3
N✝ : Type u_4
N' : Type u_5
P✝ : Type u_6
P' : Type u_7
inst✝¹³ : Semiring R✝
inst✝¹² : AddCommGroup M✝
inst✝¹¹ : AddCommGroup N✝
inst✝¹⁰ : AddCommGroup P✝
inst✝⁹ : Module R✝ M✝
inst✝⁸ : Module R✝ N✝
inst✝⁷ : Module R✝ P✝
f : M✝ →ₗ[R✝] N✝
g : N✝ →ₗ[R✝] P✝
R : Type ?u.42
M : Type ?u.44
N : Type ?u.46
P : Type ?u.48
inst✝⁶ : Semiring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : AddCommGroup P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
e : N ≃ₗ[R] M × P
hg : Surjective ⇑(snd R M P ∘ₗ ↑e)
h : Exact ⇑(↑e.symm ∘ₗ inl R M P) ⇑(snd R M P ∘ₗ ↑e)
x : N
⊢ (↑((fun l ↦ ⟨LinearEquiv.ofBijective ((↑l).prod (snd R M P ∘ₗ ↑e)) ⋯, ⋯⟩)
            ((fun e_1 ↦ ⟨fst R M P ∘ₗ ↑↑e_1, ⋯⟩) ⟨e, ⋯⟩))
        x).1 =
    (↑⟨e, ⋯⟩ x).1

pp: case refine_5.snd
R✝ : Type u_1
M✝ : Type u_2
M' : Type u_3
N✝ : Type u_4
N' : Type u_5
P✝ : Type u_6
P' : Type u_7
inst✝¹³ : Semiring R✝
inst✝¹² : AddCommGroup M✝
inst✝¹¹ : AddCommGroup N✝
inst✝¹⁰ : AddCommGroup P✝
inst✝⁹ : Module R✝ M✝
inst✝⁸ : Module R✝ N✝
inst✝⁷ : Module R✝ P✝
f : M✝ →ₗ[R✝] N✝
g : N✝ →ₗ[R✝] P✝
R : Type ?u.42
M : Type ?u.44
N : Type ?u.46
P : Type ?u.48
inst✝⁶ : Semiring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : AddCommGroup P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
e : N ≃ₗ[R] M × P
hg : Surjective ⇑(snd R M P ∘ₗ ↑e)
h : Exact ⇑(↑e.symm ∘ₗ inl R M P) ⇑(snd R M P ∘ₗ ↑e)
x : N
⊢ (↑((fun l ↦ ⟨LinearEquiv.ofBijective ((↑l).prod (snd R M P ∘ₗ ↑e)) ⋯, ⋯⟩)
            ((fun e_1 ↦ ⟨fst R M P ∘ₗ ↑↑e_1, ⋯⟩) ⟨e, ⋯⟩))
        x).2 =
    (↑⟨e, ⋯⟩ x).2

Tactic:
<;>

Goal state after:
case refine_5.fst
R✝ : Type u_1
M✝ : Type u_2
M' : Type u_3
N✝ : Type u_4
N' : Type u_5
P✝ : Type u_6
P' : Type u_7
inst✝¹³ : Semiring R✝
inst✝¹² : AddCommGroup M✝
inst✝¹¹ : AddCommGroup N✝
inst✝¹⁰ : AddCommGroup P✝
inst✝⁹ : Module R✝ M✝
inst✝⁸ : Module R✝ N✝
inst✝⁷ : Module R✝ P✝
f : M✝ →ₗ[R✝] N✝
g : N✝ →ₗ[R✝] P✝
R : Type ?u.42
M : Type ?u.44
N : Type ?u.46
P : Type ?u.48
inst✝⁶ : Semiring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : AddCommGroup P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
e : N ≃ₗ[R] M × P
hg : Surjective ⇑(snd R M P ∘ₗ ↑e)
h : Exact ⇑(↑e.symm ∘ₗ inl R M P) ⇑(snd R M P ∘ₗ ↑e)
x : N
⊢ (↑((fun l ↦ ⟨LinearEquiv.ofBijective ((↑l).prod (snd R M P ∘ₗ ↑e)) ⋯, ⋯⟩)
            ((fun e_1 ↦ ⟨fst R M P ∘ₗ ↑↑e_1, ⋯⟩) ⟨e, ⋯⟩))
        x).1 =
    (↑⟨e, ⋯⟩ x).1

case refine_5.snd
R✝ : Type u_1
M✝ : Type u_2
M' : Type u_3
N✝ : Type u_4
N' : Type u_5
P✝ : Type u_6
P' : Type u_7
inst✝¹³ : Semiring R✝
inst✝¹² : AddCommGroup M✝
inst✝¹¹ : AddCommGroup N✝
inst✝¹⁰ : AddCommGroup P✝
inst✝⁹ : Module R✝ M✝
inst✝⁸ : Module R✝ N✝
inst✝⁷ : Module R✝ P✝
f : M✝ →ₗ[R✝] N✝
g : N✝ →ₗ[R✝] P✝
R : Type ?u.42
M : Type ?u.44
N : Type ?u.46
P : Type ?u.48
inst✝⁶ : Semiring R
inst✝⁵ : AddCommGroup M
inst✝⁴ : AddCommGroup N
inst✝³ : AddCommGroup P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
e : N ≃ₗ[R] M × P
hg : Surjective ⇑(snd R M P ∘ₗ ↑e)
h : Exact ⇑(↑e.symm ∘ₗ inl R M P) ⇑(snd R M P ∘ₗ ↑e)
x : N
⊢ (↑((fun l ↦ ⟨LinearEquiv.ofBijective ((↑l).prod (snd R M P ∘ₗ ↑e)) ⋯, ⋯⟩)
            ((fun e_1 ↦ ⟨fst R M P ∘ₗ ↑↑e_1, ⋯⟩) ⟨e, ⋯⟩))
        x).2 =
    (↑⟨e, ⋯⟩ x).2