awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Exact (hypothesis)
Goal:
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_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : AddCommGroup P
inst_4 : Module R M
inst_5 : Module R N
inst_6 : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
h : Exact.{u_2, u_4, u_6} (M := M) (N := N) (P := P) (⇑f : (a : M) → N) (⇑g : (a : N) → P)
hf : Injective.{u_2 + 1, u_4 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
l : { l : P →ₗ[R] N // g ∘ₗ l = LinearMap.id }
h₁ : ∀ (x : P), (g : (a : N) → P) (((↑l : P →ₗ[R] N) : (a : P) → N) x : N) = x
⊢ Bijective (α := M × P) (β := N) (⇑(f ∘ₗ fst R M P + (↑l : P →ₗ[R] N) ∘ₗ snd R M P) : (a : M × P) → N)
have h₂ : ∀ (x : M), Eq.{u_6 + 1} (α := P) ((g : (a : N) → P) ((f : (a : M) → N) x : N) : P) (0 : P)
Tactic: have h₂ : ∀ x, g (f x) = 0 := congr_fun h.comp_eq_zero
-- Lean 4 proof step from Mathlib.Algebra.Exact (goal)
Goal:
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_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : AddCommGroup P
inst_4 : Module R M
inst_5 : Module R N
inst_6 : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
h : Exact.{u_2, u_4, u_6} (M := M) (N := N) (P := P) (⇑f : (a : M) → N) (⇑g : (a : N) → P)
hf : Injective.{u_2 + 1, u_4 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
l : { l : P →ₗ[R] N // g ∘ₗ l = LinearMap.id }
h₁ : ∀ (x : P), (g : (a : N) → P) (((↑l : P →ₗ[R] N) : (a : P) → N) x : N) = x
h₂ : ∀ (x : M), Eq.{u_6 + 1} (α := P) ((g : (a : N) → P) ((f : (a : M) → N) x : N) : P) (0 : P)
⊢ Bijective (α := M × P) (β := N) (⇑(f ∘ₗ fst R M P + (↑l : P →ₗ[R] N) ∘ₗ snd R M P) : (a : M × P) → N)
have refine_1 : Injective (α := M × P) (β := N) (⇑(f ∘ₗ fst R M P + (↑l : P →ₗ[R] N) ∘ₗ snd R M P) : (a : M × P) → N)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Exact (goal)
Goal:
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_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : AddCommGroup P
inst_4 : Module R M
inst_5 : Module R N
inst_6 : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
h : Exact.{u_2, u_4, u_6} (M := M) (N := N) (P := P) (⇑f : (a : M) → N) (⇑g : (a : N) → P)
hf : Injective.{u_2 + 1, u_4 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
l : { l : P →ₗ[R] N // g ∘ₗ l = LinearMap.id }
h₁ : ∀ (x : P), (g : (a : N) → P) (((↑l : P →ₗ[R] N) : (a : P) → N) x : N) = x
h₂ : ∀ (x : M), Eq.{u_6 + 1} (α := P) ((g : (a : N) → P) ((f : (a : M) → N) x : N) : P) (0 : P)
refine_1 : Injective (α := M × P) (β := N) (⇑(f ∘ₗ fst R M P + (↑l : P →ₗ[R] N) ∘ₗ snd R M P) : (a : M × P) → N)
⊢ Bijective (α := M × P) (β := N) (⇑(f ∘ₗ fst R M P + (↑l : P →ₗ[R] N) ∘ₗ snd R M P) : (a : M × P) → N)
have refine_1₁ : Surjective (α := M × P) (β := N) (⇑(f ∘ₗ fst R M P + (↑l : P →ₗ[R] N) ∘ₗ snd R M P) : (a : M × P) → N)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Exact (goal)
Goal:
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_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : AddCommGroup P
inst_4 : Module R M
inst_5 : Module R N
inst_6 : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
h : Exact.{u_2, u_4, u_6} (M := M) (N := N) (P := P) (⇑f : (a : M) → N) (⇑g : (a : N) → P)
hf : Injective.{u_2 + 1, u_4 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
l : { l : P →ₗ[R] N // g ∘ₗ l = LinearMap.id }
h₁ : ∀ (x : P), (g : (a : N) → P) (((↑l : P →ₗ[R] N) : (a : P) → N) x : N) = x
h₂ : ∀ (x : M), Eq.{u_6 + 1} (α := P) ((g : (a : N) → P) ((f : (a : M) → N) x : N) : P) (0 : P)
x y : M × P
e :
  HAdd.hAdd (α := N) (β := N) ((f : (a : M) → N) x.1 : N) (((↑l : P →ₗ[R] N) : (a : P) → N) x.2 : N) =
    HAdd.hAdd (α := N) (β := N) ((f : (a : M) → N) y.1 : N) (((↑l : P →ₗ[R] N) : (a : P) → N) y.2 : N)
this : x.2 = y.2
⊢ Eq.{u_4 + 1} (α := N) ((f : (a : M) → N) x.1 : N) ((f : (a : M) → N) y.1 : N)
have rwa : ∀
  (e :
    HAdd.hAdd (α := N) (β := N) ((f : (a : M) → N) x.1 : N) (((↑l : P →ₗ[R] N) : (a : P) → N) y.2 : N) =
      HAdd.hAdd (α := N) (β := N) ((f : (a : M) → N) y.1 : N) (((↑l : P →ₗ[R] N) : (a : P) → N) y.2 : N))
  (this : x.2 = y.2), Eq.{u_4 + 1} (α := N) ((f : (a : M) → N) x.1 : N) ((f : (a : M) → N) y.1 : N)
Tactic: rwa [this, add_left_inj] at e
Cleared hypotheses: e, this
-- Lean 4 proof step from Mathlib.Algebra.Exact (goal)
Goal:
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_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : AddCommGroup P
inst_4 : Module R M
inst_5 : Module R N
inst_6 : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
h : Exact.{u_2, u_4, u_6} (M := M) (N := N) (P := P) (⇑f : (a : M) → N) (⇑g : (a : N) → P)
hf : Injective.{u_2 + 1, u_4 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
l : { l : P →ₗ[R] N // g ∘ₗ l = LinearMap.id }
h₁ : ∀ (x : P), (g : (a : N) → P) (((↑l : P →ₗ[R] N) : (a : P) → N) x : N) = x
h₂ : ∀ (x : M), Eq.{u_6 + 1} (α := P) ((g : (a : N) → P) ((f : (a : M) → N) x : N) : P) (0 : P)
x y : M × P
e :
  HAdd.hAdd (α := N) (β := N) ((f : (a : M) → N) x.1 : N) (((↑l : P →ₗ[R] N) : (a : P) → N) x.2 : N) =
    HAdd.hAdd (α := N) (β := N) ((f : (a : M) → N) y.1 : N) (((↑l : P →ₗ[R] N) : (a : P) → N) y.2 : N)
this : x.2 = y.2
rwa :
  ∀
    (e :
      HAdd.hAdd (α := N) (β := N) ((f : (a : M) → N) x.1 : N) (((↑l : P →ₗ[R] N) : (a : P) → N) y.2 : N) =
        HAdd.hAdd (α := N) (β := N) ((f : (a : M) → N) y.1 : N) (((↑l : P →ₗ[R] N) : (a : P) → N) y.2 : N))
    (this : x.2 = y.2), Eq.{u_4 + 1} (α := N) ((f : (a : M) → N) x.1 : N) ((f : (a : M) → N) y.1 : N)
⊢ Eq.{u_4 + 1} (α := N) ((f : (a : M) → N) x.1 : N) ((f : (a : M) → N) y.1 : N)
have rwa₁ : ∀ (e : Eq.{u_4 + 1} (α := N) ((f : (a : M) → N) x.1 : N) ((f : (a : M) → N) y.1 : N)) (this : x.2 = y.2),
  Eq.{u_4 + 1} (α := N) ((f : (a : M) → N) x.1 : N) ((f : (a : M) → N) y.1 : N)
Tactic: rwa [this, add_left_inj] at e
Cleared hypotheses: e, this
-- Lean 4 proof step from Mathlib.Algebra.Exact (goal)
Goal:
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_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : AddCommGroup P
inst_4 : Module R M
inst_5 : Module R N
inst_6 : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
h : Exact.{u_2, u_4, u_6} (M := M) (N := N) (P := P) (⇑f : (a : M) → N) (⇑g : (a : N) → P)
hf : Injective.{u_2 + 1, u_4 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
l : { l : P →ₗ[R] N // g ∘ₗ l = LinearMap.id }
h₁ : ∀ (x : P), (g : (a : N) → P) (((↑l : P →ₗ[R] N) : (a : P) → N) x : N) = x
h₂ : ∀ (x : M), Eq.{u_6 + 1} (α := P) ((g : (a : N) → P) ((f : (a : M) → N) x : N) : P) (0 : P)
x y : M × P
e :
  HAdd.hAdd (α := N) (β := N) ((f : (a : M) → N) x.1 : N) (((↑l : P →ₗ[R] N) : (a : P) → N) x.2 : N) =
    HAdd.hAdd (α := N) (β := N) ((f : (a : M) → N) y.1 : N) (((↑l : P →ₗ[R] N) : (a : P) → N) y.2 : N)
⊢ x = y
have refine_1 : x.2 = y.2
Tactic: suffices x.2 = y.2 from Prod.ext (hf (by rwa [this, add_left_inj] at e)) this
-- Lean 4 proof step from Mathlib.Algebra.Exact (goal)
Goal:
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_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : AddCommGroup P
inst_4 : Module R M
inst_5 : Module R N
inst_6 : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
h : Exact.{u_2, u_4, u_6} (M := M) (N := N) (P := P) (⇑f : (a : M) → N) (⇑g : (a : N) → P)
hf : Injective.{u_2 + 1, u_4 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
l : { l : P →ₗ[R] N // g ∘ₗ l = LinearMap.id }
h₁ : ∀ (x : P), (g : (a : N) → P) (((↑l : P →ₗ[R] N) : (a : P) → N) x : N) = x
h₂ : ∀ (x : M), Eq.{u_6 + 1} (α := P) ((g : (a : N) → P) ((f : (a : M) → N) x : N) : P) (0 : P)
x : N
⊢ ∃ (a : M × P), (f ∘ₗ fst R M P + (↑l : P →ₗ[R] N) ∘ₗ snd R M P : (a : M × P) → N) a = x
have refine_1 : ∀ (y : M)
  (hy : (f : (a : M) → N) y = HSub.hSub (β := N) x (((↑l : P →ₗ[R] N) : (a : P) → N) ((g : (a : N) → P) x : P) : N)),
  ∃ (a : M × P), (f ∘ₗ fst R M P + (↑l : P →ₗ[R] N) ∘ₗ snd R M P : (a : M × P) → N) a = x
Tactic: obtain ⟨y, hy⟩ := (h (x - l.1 (g x))).mp (by simp [h₁, g.map_sub])
-- Lean 4 proof step from Mathlib.Algebra.Exact (hypothesis)
Goal:
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_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : AddCommGroup P
inst_4 : Module R M
inst_5 : Module R N
inst_6 : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
h : Exact.{u_2, u_4, u_6} (M := M) (N := N) (P := P) (⇑f : (a : M) → N) (⇑g : (a : N) → P)
hf : Injective.{u_2 + 1, u_4 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
l : { l : P →ₗ[R] N // g ∘ₗ l = LinearMap.id }
⊢ f =
      (↑(LinearEquiv.symm
              (LinearEquiv.symm (LinearEquiv.ofBijective (f ∘ₗ fst R M P + (↑l : P →ₗ[R] N) ∘ₗ snd R M P) ⋯))) :
          M × P →ₗ[R] N) ∘ₗ
        inl R M P ∧
    g =
      snd R M P ∘ₗ
        (↑(LinearEquiv.symm (LinearEquiv.ofBijective (f ∘ₗ fst R M P + (↑l : P →ₗ[R] N) ∘ₗ snd R M P) ⋯)) :
          N →ₗ[R] M × P)
have h₁ : ∀ (x : P), (g : (a : N) → P) (((↑l : P →ₗ[R] N) : (a : P) → N) x : N) = x
Tactic: have h₁ : ∀ x, g (l.1 x) = x := LinearMap.congr_fun l.2
-- Lean 4 proof step from Mathlib.Algebra.Exact (hypothesis)
Goal:
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_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : AddCommGroup P
inst_4 : Module R M
inst_5 : Module R N
inst_6 : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
h : Exact.{u_2, u_4, u_6} (M := M) (N := N) (P := P) (⇑f : (a : M) → N) (⇑g : (a : N) → P)
hf : Injective.{u_2 + 1, u_4 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
l : { l : P →ₗ[R] N // g ∘ₗ l = LinearMap.id }
h₁ : ∀ (x : P), (g : (a : N) → P) (((↑l : P →ₗ[R] N) : (a : P) → N) x : N) = x
⊢ f =
      (↑(LinearEquiv.symm
              (LinearEquiv.symm (LinearEquiv.ofBijective (f ∘ₗ fst R M P + (↑l : P →ₗ[R] N) ∘ₗ snd R M P) ⋯))) :
          M × P →ₗ[R] N) ∘ₗ
        inl R M P ∧
    g =
      snd R M P ∘ₗ
        (↑(LinearEquiv.symm (LinearEquiv.ofBijective (f ∘ₗ fst R M P + (↑l : P →ₗ[R] N) ∘ₗ snd R M P) ⋯)) :
          N →ₗ[R] M × P)
have h₂ : ∀ (x : M), Eq.{u_6 + 1} (α := P) ((g : (a : N) → P) ((f : (a : M) → N) x : N) : P) (0 : P)
Tactic: have h₂ : ∀ x, g (f x) = 0 := congr_fun h.comp_eq_zero
-- Lean 4 proof step from Mathlib.Algebra.Exact (goal)
Goal:
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_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : AddCommGroup P
inst_4 : Module R M
inst_5 : Module R N
inst_6 : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
h : Exact.{u_2, u_4, u_6} (M := M) (N := N) (P := P) (⇑f : (a : M) → N) (⇑g : (a : N) → P)
hf : Injective.{u_2 + 1, u_4 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
l : { l : P →ₗ[R] N // g ∘ₗ l = LinearMap.id }
h₁ : ∀ (x : P), (g : (a : N) → P) (((↑l : P →ₗ[R] N) : (a : P) → N) x : N) = x
h₂ : ∀ (x : M), Eq.{u_6 + 1} (α := P) ((g : (a : N) → P) ((f : (a : M) → N) x : N) : P) (0 : P)
⊢ f =
      (↑(LinearEquiv.symm
              (LinearEquiv.symm (LinearEquiv.ofBijective (f ∘ₗ fst R M P + (↑l : P →ₗ[R] N) ∘ₗ snd R M P) ⋯))) :
          M × P →ₗ[R] N) ∘ₗ
        inl R M P ∧
    g =
      snd R M P ∘ₗ
        (↑(LinearEquiv.symm (LinearEquiv.ofBijective (f ∘ₗ fst R M P + (↑l : P →ₗ[R] N) ∘ₗ snd R M P) ⋯)) :
          N →ₗ[R] M × P)
have refine_2 : f =
  (↑(LinearEquiv.symm (LinearEquiv.symm (LinearEquiv.ofBijective (f ∘ₗ fst R M P + (↑l : P →ₗ[R] N) ∘ₗ snd R M P) sorry))) :
      M × P →ₗ[R] N) ∘ₗ
    inl R M P
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Exact (goal)
Goal:
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_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : AddCommGroup P
inst_4 : Module R M
inst_5 : Module R N
inst_6 : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
h : Exact.{u_2, u_4, u_6} (M := M) (N := N) (P := P) (⇑f : (a : M) → N) (⇑g : (a : N) → P)
hf : Injective.{u_2 + 1, u_4 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
l : { l : P →ₗ[R] N // g ∘ₗ l = LinearMap.id }
h₁ : ∀ (x : P), (g : (a : N) → P) (((↑l : P →ₗ[R] N) : (a : P) → N) x : N) = x
h₂ : ∀ (x : M), Eq.{u_6 + 1} (α := P) ((g : (a : N) → P) ((f : (a : M) → N) x : N) : P) (0 : P)
refine_2 :
  f =
    (↑(LinearEquiv.symm
            (LinearEquiv.symm (LinearEquiv.ofBijective (f ∘ₗ fst R M P + (↑l : P →ₗ[R] N) ∘ₗ snd R M P) ⋯))) :
        M × P →ₗ[R] N) ∘ₗ
      inl R M P
⊢ f =
      (↑(LinearEquiv.symm
              (LinearEquiv.symm (LinearEquiv.ofBijective (f ∘ₗ fst R M P + (↑l : P →ₗ[R] N) ∘ₗ snd R M P) ⋯))) :
          M × P →ₗ[R] N) ∘ₗ
        inl R M P ∧
    g =
      snd R M P ∘ₗ
        (↑(LinearEquiv.symm (LinearEquiv.ofBijective (f ∘ₗ fst R M P + (↑l : P →ₗ[R] N) ∘ₗ snd R M P) ⋯)) :
          N →ₗ[R] M × P)
have refine_2₁ : g =
  snd R M P ∘ₗ
    (↑(LinearEquiv.symm (LinearEquiv.ofBijective (f ∘ₗ fst R M P + (↑l : P →ₗ[R] N) ∘ₗ snd R M P) sorry)) : N →ₗ[R] M × P)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Exact (goal)
Goal:
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_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : AddCommGroup P
inst_4 : Module R M
inst_5 : Module R N
inst_6 : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
h : Exact.{u_2, u_4, u_6} (M := M) (N := N) (P := P) (⇑f : (a : M) → N) (⇑g : (a : N) → P)
hf : Injective.{u_2 + 1, u_4 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
l : { l : P →ₗ[R] N // g ∘ₗ l = LinearMap.id }
h₁ : ∀ (x : P), (g : (a : N) → P) (((↑l : P →ₗ[R] N) : (a : P) → N) x : N) = x
h₂ : ∀ (x : M), Eq.{u_6 + 1} (α := P) ((g : (a : N) → P) ((f : (a : M) → N) x : N) : P) (0 : P)
⊢ f =
    (↑(LinearEquiv.symm
            (LinearEquiv.symm (LinearEquiv.ofBijective (f ∘ₗ fst R M P + (↑l : P →ₗ[R] N) ∘ₗ snd R M P) ⋯))) :
        M × P →ₗ[R] N) ∘ₗ
      inl R M P
have refine_2 : ∀ (x : M),
  Eq.{u_4 + 1} (α := N) ((f : (a : M) → N) x : N)
    (((↑(LinearEquiv.symm
                  (LinearEquiv.symm (LinearEquiv.ofBijective (f ∘ₗ fst R M P + (↑l : P →ₗ[R] N) ∘ₗ snd R M P) sorry))) :
              M × P →ₗ[R] N) ∘ₗ
            inl R M P :
          (a : M) → N)
        x :
      N)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Exact (goal)
Goal:
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_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : AddCommGroup P
inst_4 : Module R M
inst_5 : Module R N
inst_6 : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
h : Exact.{u_2, u_4, u_6} (M := M) (N := N) (P := P) (⇑f : (a : M) → N) (⇑g : (a : N) → P)
hf : Injective.{u_2 + 1, u_4 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
l : { l : P →ₗ[R] N // g ∘ₗ l = LinearMap.id }
h₁ : ∀ (x : P), (g : (a : N) → P) (((↑l : P →ₗ[R] N) : (a : P) → N) x : N) = x
h₂ : ∀ (x : M), Eq.{u_6 + 1} (α := P) ((g : (a : N) → P) ((f : (a : M) → N) x : N) : P) (0 : P)
⊢ g =
    snd R M P ∘ₗ
      (↑(LinearEquiv.symm (LinearEquiv.ofBijective (f ∘ₗ fst R M P + (↑l : P →ₗ[R] N) ∘ₗ snd R M P) ⋯)) : N →ₗ[R] M × P)
have refine_2 : g ∘ₗ (↑(LinearEquiv.ofBijective (f ∘ₗ fst R M P + (↑l : P →ₗ[R] N) ∘ₗ snd R M P) sorry) : M × P →ₗ[R] N) = snd R M P
Tactic: rw [LinearEquiv.eq_comp_toLinearMap_symm]
-- Lean 4 proof step from Mathlib.Algebra.Exact (goal)
Goal:
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_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : AddCommGroup P
inst_4 : Module R M
inst_5 : Module R N
inst_6 : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
h : Exact.{u_2, u_4, u_6} (M := M) (N := N) (P := P) (⇑f : (a : M) → N) (⇑g : (a : N) → P)
hf : Injective.{u_2 + 1, u_4 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
l : { l : P →ₗ[R] N // g ∘ₗ l = LinearMap.id }
h₁ : ∀ (x : P), (g : (a : N) → P) (((↑l : P →ₗ[R] N) : (a : P) → N) x : N) = x
h₂ : ∀ (x : M), Eq.{u_6 + 1} (α := P) ((g : (a : N) → P) ((f : (a : M) → N) x : N) : P) (0 : P)
⊢ g ∘ₗ (↑(LinearEquiv.ofBijective (f ∘ₗ fst R M P + (↑l : P →ₗ[R] N) ∘ₗ snd R M P) ⋯) : M × P →ₗ[R] N) = snd R M P
have refine_2 : ∀ (x : M),
  Eq.{u_6 + 1} (α := P)
    (((g ∘ₗ (↑(LinearEquiv.ofBijective (f ∘ₗ fst R M P + (↑l : P →ₗ[R] N) ∘ₗ snd R M P) sorry) : M × P →ₗ[R] N)) ∘ₗ
            inl R M P :
          (a : M) → P)
        x :
      P)
    ((snd R M P ∘ₗ inl R M P : (a : M) → P) x : P)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Exact (goal)
Goal:
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_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : AddCommGroup P
inst_4 : Module R M
inst_5 : Module R N
inst_6 : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
h : Exact.{u_2, u_4, u_6} (M := M) (N := N) (P := P) (⇑f : (a : M) → N) (⇑g : (a : N) → P)
hf : Injective.{u_2 + 1, u_4 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
l : { l : P →ₗ[R] N // g ∘ₗ l = LinearMap.id }
h₁ : ∀ (x : P), (g : (a : N) → P) (((↑l : P →ₗ[R] N) : (a : P) → N) x : N) = x
h₂ : ∀ (x : M), Eq.{u_6 + 1} (α := P) ((g : (a : N) → P) ((f : (a : M) → N) x : N) : P) (0 : P)
refine_2 :
  ∀ (x : M),
    Eq.{u_6 + 1} (α := P)
      (((g ∘ₗ (↑(LinearEquiv.ofBijective (f ∘ₗ fst R M P + (↑l : P →ₗ[R] N) ∘ₗ snd R M P) ⋯) : M × P →ₗ[R] N)) ∘ₗ
              inl R M P :
            (a : M) → P)
          x :
        P)
      ((snd R M P ∘ₗ inl R M P : (a : M) → P) x : P)
⊢ g ∘ₗ (↑(LinearEquiv.ofBijective (f ∘ₗ fst R M P + (↑l : P →ₗ[R] N) ∘ₗ snd R M P) ⋯) : M × P →ₗ[R] N) = snd R M P
have refine_2₁ : ∀ (x : P),
  Eq (α := P)
    (((g ∘ₗ (↑(LinearEquiv.ofBijective (f ∘ₗ fst R M P + (↑l : P →ₗ[R] N) ∘ₗ snd R M P) sorry) : M × P →ₗ[R] N)) ∘ₗ
            inr R M P :
          (a : P) → P)
        x :
      P)
    ((snd R M P ∘ₗ inr R M P : (a : P) → P) x : P)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Exact (goal)
Goal:
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_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : AddCommGroup P
inst_4 : Module R M
inst_5 : Module R N
inst_6 : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
h : Exact.{u_2, u_4, u_6} (M := M) (N := N) (P := P) (⇑f : (a : M) → N) (⇑g : (a : N) → P)
hf : Injective.{u_2 + 1, u_4 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
e : { e : N ≃ₗ[R] M × P // f = (↑e.symm : M × P →ₗ[R] N) ∘ₗ inl R M P ∧ g = snd R M P ∘ₗ (↑e : N →ₗ[R] M × P) }
⊢ g ∘ₗ (↑(↑e : N ≃ₗ[R] M × P).symm : M × P →ₗ[R] N) ∘ₗ inr R M P = LinearMap.id
have refine_3 : Eq (α := P →ₗ[R] P) (snd R M P ∘ₗ inr R M P) LinearMap.id
Tactic: rw [← LinearMap.comp_assoc, (LinearEquiv.eq_comp_toLinearMap_symm _ _).mp e.2.2]
-- Lean 4 proof step from Mathlib.Algebra.Exact (goal)
Goal:
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_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : AddCommGroup P
inst_4 : Module R M
inst_5 : Module R N
inst_6 : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
h : Exact.{u_2, u_4, u_6} (M := M) (N := N) (P := P) (⇑f : (a : M) → N) (⇑g : (a : N) → P)
hf : Injective.{u_2 + 1, u_4 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
x : { l : P →ₗ[R] N // g ∘ₗ l = LinearMap.id }
⊢ (fun
          (e :
            { e : N ≃ₗ[R] M × P //
              f = (↑e.symm : M × P →ₗ[R] N) ∘ₗ inl R M P ∧ g = snd R M P ∘ₗ (↑e : N →ₗ[R] M × P) }) ↦
        (Subtype.mk (p := fun (l : P →ₗ[R] N) ↦ g ∘ₗ l = LinearMap.id)
            ((↑(↑e : N ≃ₗ[R] M × P).symm : M × P →ₗ[R] N) ∘ₗ inr R M P) ⋯ :
          { l : P →ₗ[R] N // g ∘ₗ l = LinearMap.id }))
      ((fun (l : { l : P →ₗ[R] N // g ∘ₗ l = LinearMap.id }) ↦
          (Subtype.mk (p := fun (e : N ≃ₗ[R] M × P) ↦
              f = (↑e.symm : M × P →ₗ[R] N) ∘ₗ inl R M P ∧ g = snd R M P ∘ₗ (↑e : N →ₗ[R] M × P))
              (LinearEquiv.symm (LinearEquiv.ofBijective (f ∘ₗ fst R M P + (↑l : P →ₗ[R] N) ∘ₗ snd R M P) ⋯)) ⋯ :
            { e : N ≃ₗ[R] M × P //
              f = (↑e.symm : M × P →ₗ[R] N) ∘ₗ inl R M P ∧ g = snd R M P ∘ₗ (↑e : N →ₗ[R] M × P) }))
        x) =
    x
have refine_4 : ∀ (x_1 : P),
  Eq.{u_4 + 1} (α := N)
    (((↑((fun
                    (e :
                      { e : N ≃ₗ[R] M × P //
                        f = (↑e.symm : M × P →ₗ[R] N) ∘ₗ inl R M P ∧ g = snd R M P ∘ₗ (↑e : N →ₗ[R] M × P) }) ↦
                  (Subtype.mk (p := fun (l : P →ₗ[R] N) ↦ g ∘ₗ l = LinearMap.id)
                      ((↑(↑e : N ≃ₗ[R] M × P).symm : M × P →ₗ[R] N) ∘ₗ inr R M P) sorry :
                    { l : P →ₗ[R] N // g ∘ₗ l = LinearMap.id }))
                ((fun (l : { l : P →ₗ[R] N // g ∘ₗ l = LinearMap.id }) ↦
                    (Subtype.mk (p := fun (e : N ≃ₗ[R] M × P) ↦
                        f = (↑e.symm : M × P →ₗ[R] N) ∘ₗ inl R M P ∧ g = snd R M P ∘ₗ (↑e : N →ₗ[R] M × P))
                        (LinearEquiv.symm (LinearEquiv.ofBijective (f ∘ₗ fst R M P + (↑l : P →ₗ[R] N) ∘ₗ snd R M P) sorry))
                        sorry :
                      { e : N ≃ₗ[R] M × P //
                        f = (↑e.symm : M × P →ₗ[R] N) ∘ₗ inl R M P ∧ g = snd R M P ∘ₗ (↑e : N →ₗ[R] M × P) }))
                  x)) :
            P →ₗ[R] N) :
          (a : P) → N)
        x_1 :
      N)
    (((↑x : P →ₗ[R] N) : (a : P) → N) x_1 : N)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Exact (goal)
Goal:
R_1 : Type u_1
M_1 : Type u_2
M' : Type u_3
N_1 : Type u_4
N' : Type u_5
P_1 : Type u_6
P' : Type u_7
inst : Semiring R_1
inst_1 : AddCommGroup M_1
inst_2 : AddCommGroup N_1
inst_3 : AddCommGroup P_1
inst_4 : Module R_1 M_1
inst_5 : Module R_1 N_1
inst_6 : Module R_1 P_1
f_1 : M_1 →ₗ[R_1] N_1
g_1 : N_1 →ₗ[R_1] P_1
R : Type u_8
M : Type u_9
N : Type u_10
P : Type u_11
inst_7 : Semiring R
inst_8 : AddCommGroup M
inst_9 : AddCommGroup N
inst_10 : AddCommGroup P
inst_11 : Module R M
inst_12 : Module R N
inst_13 : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
h : Exact.{u_9, u_10, u_11} (M := M) (N := N) (P := P) (⇑f : (a : M) → N) (⇑g : (a : N) → P)
hg : Surjective.{u_10 + 1, u_11 + 1} (α := N) (β := P) (⇑g : (a : N) → P)
⊢ { l : N →ₗ[R] M // l ∘ₗ f = LinearMap.id } ≃
    { e : N ≃ₗ[R] M × P // f = (↑e.symm : M × P →ₗ[R] N) ∘ₗ inl R M P ∧ g = snd R M P ∘ₗ (↑e : N →ₗ[R] M × P) }
have refine_1 : ∀ (l : { l : N →ₗ[R] M // l ∘ₗ f = LinearMap.id }),
  Bijective (α := N) (β := M × P) (⇑((↑l : N →ₗ[R] M).prod g) : (a : N) → M × P)
Tactic: refine
  { toFun := fun l ↦ ⟨(LinearEquiv.ofBijective (l.1.prod g) ?_), ?_⟩
    invFun := fun e ↦ ⟨fst R M P ∘ₗ e.1, ?_⟩
    left_inv := ?_
    right_inv := ?_ }
-- Lean 4 proof step from Mathlib.Algebra.Exact (goal)
Goal:
R_1 : Type u_1
M_1 : Type u_2
M' : Type u_3
N_1 : Type u_4
N' : Type u_5
P_1 : Type u_6
P' : Type u_7
inst : Semiring R_1
inst_1 : AddCommGroup M_1
inst_2 : AddCommGroup N_1
inst_3 : AddCommGroup P_1
inst_4 : Module R_1 M_1
inst_5 : Module R_1 N_1
inst_6 : Module R_1 P_1
f_1 : M_1 →ₗ[R_1] N_1
g_1 : N_1 →ₗ[R_1] P_1
R : Type u_8
M : Type u_9
N : Type u_10
P : Type u_11
inst_7 : Semiring R
inst_8 : AddCommGroup M
inst_9 : AddCommGroup N
inst_10 : AddCommGroup P
inst_11 : Module R M
inst_12 : Module R N
inst_13 : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
h : Exact.{u_9, u_10, u_11} (M := M) (N := N) (P := P) (⇑f : (a : M) → N) (⇑g : (a : N) → P)
hg : Surjective.{u_10 + 1, u_11 + 1} (α := N) (β := P) (⇑g : (a : N) → P)
refine_1 :
  ∀ (l : { l : N →ₗ[R] M // l ∘ₗ f = LinearMap.id }),
    Bijective (α := N) (β := M × P) (⇑((↑l : N →ₗ[R] M).prod g) : (a : N) → M × P)
⊢ { l : N →ₗ[R] M // l ∘ₗ f = LinearMap.id } ≃
    { e : N ≃ₗ[R] M × P // f = (↑e.symm : M × P →ₗ[R] N) ∘ₗ inl R M P ∧ g = snd R M P ∘ₗ (↑e : N →ₗ[R] M × P) }
have refine_2 : ∀ (l : { l : N →ₗ[R] M // l ∘ₗ f = LinearMap.id }),
  f = (↑(LinearEquiv.symm (LinearEquiv.ofBijective ((↑l : N →ₗ[R] M).prod g) sorry)) : M × P →ₗ[R] N) ∘ₗ inl R M P ∧
    g = snd R M P ∘ₗ (↑(LinearEquiv.ofBijective ((↑l : N →ₗ[R] M).prod g) sorry) : N →ₗ[R] M × P)
Tactic: refine
  { toFun := fun l ↦ ⟨(LinearEquiv.ofBijective (l.1.prod g) ?_), ?_⟩
    invFun := fun e ↦ ⟨fst R M P ∘ₗ e.1, ?_⟩
    left_inv := ?_
    right_inv := ?_ }