awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Exact
Goal:
M₁ : Type u_8
M₂ : Type u_9
M₃ : Type u_10
N₁ : Type u_11
N₂ : Type u_12
N₃ : Type u_13
inst : CommMonoid M₁
inst_1 : CommMonoid M₂
inst_2 : CommMonoid M₃
inst_3 : CommMonoid N₁
inst_4 : CommMonoid N₂
inst_5 : CommMonoid N₃
f : M₁ →* M₂
g : M₂ →* M₃
f' : N₁ →* N₂
g' : N₂ →* N₃
τ₁ : M₁ →* N₁
τ₂ : M₂ →* N₂
τ₃ : M₃ →* N₃
h₁ : Surjective.{u_8 + 1, u_11 + 1} (α := M₁) (β := N₁) (⇑τ₁ : (a : M₁) → N₁)
h₂ : Bijective.{u_9 + 1, u_12 + 1} (α := M₂) (β := N₂) (⇑τ₂ : (a : M₂) → N₂)
h₃ : Injective.{u_10 + 1, u_13 + 1} (α := M₃) (β := N₃) (⇑τ₃ : (a : M₃) → N₃)
comm₁₂ :
  ∀ (x : M₁),
    Eq.{u_12 + 1} (α := N₂) ((f' : (a : N₁) → N₂) ((τ₁ : (a : M₁) → N₁) x : N₁) : N₂)
      ((τ₂ : (a : M₂) → N₂) ((f : (a : M₁) → M₂) x : M₂) : N₂)
comm₂₃ :
  ∀ (x : M₂),
    Eq.{u_13 + 1} (α := N₃) ((g' : (a : N₂) → N₃) ((τ₂ : (a : M₂) → N₂) x : N₂) : N₃)
      ((τ₃ : (a : M₃) → N₃) ((g : (a : M₂) → M₃) x : M₃) : N₃)
h : MulExact.{u_11, u_12, u_13} (M := N₁) (N := N₂) (P := N₃) (⇑f' : (a : N₁) → N₂) (⇑g' : (a : N₂) → N₃)
x₁ : M₁
⊢ Eq.{u_13 + 1} (α := N₃) ((τ₃ : (a : M₃) → N₃) ((g : (a : M₂) → M₃) ((f : (a : M₁) → M₂) x₁ : M₂) : M₃) : N₃)
    ((τ₃ : (a : M₃) → N₃) 1 : N₃)

Tactic:
simp only [← comm₁₂, ← comm₂₃, h.apply_apply_eq_one (τ₁ x₁), map_one]

Premises used: map_one, DFunLike.coe, Function.MulExact.apply_apply_eq_one
-- Module: Mathlib.Algebra.Exact
Goal:
M : Type u_2
N : Type u_4
P : Type u_6
inst : Group M
inst_1 : Group N
inst_2 : Group P
f : M →* N
g : N →* P
hfg : MulExact.{u_2, u_4, u_6} (M := M) (N := N) (P := P) (⇑f : (a : M) → N) (⇑g : (a : N) → P)
⊢ g.ker = f.range

Tactic:
SetLike.ext hfg

Premises used: SetLike.ext
-- Module: Mathlib.Algebra.Exact
Goal:
M : Type u_2
N : Type u_4
P : Type u_6
inst : Group M
inst_1 : Group N
inst_2 : Group P
f : M →* N
g : N →* P
h : MulExact.{u_2, u_4, u_6} (M := M) (N := N) (P := P) (⇑f : (a : M) → N) (⇑g : (a : N) → P)
⊢ g.comp f = 1

Tactic:
DFunLike.coe_injective h.comp_eq_one

Premises used: Function.MulExact.comp_eq_one, DFunLike.coe_injective
-- Module: Mathlib.Algebra.Exact
Goal:
X₁ : Type u_8
X₂ : Type u_9
X₃ : Type u_10
Y₁ : Type u_11
Y₂ : Type u_12
Y₃ : Type u_13
inst : CommMonoid X₁
inst_1 : CommMonoid X₂
inst_2 : CommMonoid X₃
inst_3 : CommMonoid Y₁
inst_4 : CommMonoid Y₂
inst_5 : CommMonoid Y₃
e₁ : X₁ ≃* Y₁
e₂ : X₂ ≃* Y₂
e₃ : X₃ ≃* Y₃
f₁₂ : X₁ →* X₂
f₂₃ : X₂ →* X₃
g₁₂ : Y₁ →* Y₂
g₂₃ : Y₂ →* Y₃
comm₁₂ : g₁₂.comp (↑e₁ : X₁ →* Y₁) = MonoidHom.comp (↑e₂ : X₂ →* Y₂) f₁₂
comm₂₃ : g₂₃.comp (↑e₂ : X₂ →* Y₂) = MonoidHom.comp (↑e₃ : X₃ →* Y₃) f₂₃
⊢ MulExact.{u_11, u_12, u_13} (M := Y₁) (N := Y₂) (P := Y₃) (⇑g₁₂ : (a : Y₁) → Y₂) (⇑g₂₃ : (a : Y₂) → Y₃) ↔
    MulExact.{u_8, u_9, u_10} (M := X₁) (N := X₂) (P := X₃) (⇑f₁₂ : (a : X₁) → X₂) (⇑f₂₃ : (a : X₂) → X₃)

Tactic:
(mulExact_iff_of_surjective_of_bijective_of_injective _ _ _ _ e₁ e₂ e₃ comm₁₂ comm₂₃
    e₁.surjective e₂.bijective e₃.injective).symm

Premises used: MonoidHom.mulExact_iff_of_surjective_of_bijective_of_injective, Iff.symm
-- Module: Mathlib.Algebra.Exact
Goal:
X₁ : Type u_8
X₂ : Type u_9
X₃ : Type u_10
Y₁ : Type u_11
Y₂ : Type u_12
Y₃ : Type u_13
inst : CommMonoid X₁
inst_1 : CommMonoid X₂
inst_2 : CommMonoid X₃
inst_3 : CommMonoid Y₁
inst_4 : CommMonoid Y₂
inst_5 : CommMonoid Y₃
e₁ : X₁ ≃* Y₁
e₂ : X₂ ≃* Y₂
e₃ : X₃ ≃* Y₃
f₁₂ : X₁ →* X₂
f₂₃ : X₂ →* X₃
g₁₂ : Y₁ →* Y₂
g₂₃ : Y₂ →* Y₃
comm₁₂ : g₁₂.comp (↑e₁ : X₁ →* Y₁) = MonoidHom.comp (↑e₂ : X₂ →* Y₂) f₁₂
comm₂₃ : g₂₃.comp (↑e₂ : X₂ →* Y₂) = MonoidHom.comp (↑e₃ : X₃ →* Y₃) f₂₃
H : MulExact.{u_8, u_9, u_10} (M := X₁) (N := X₂) (P := X₃) (⇑f₁₂ : (a : X₁) → X₂) (⇑f₂₃ : (a : X₂) → X₃)
⊢ MulExact.{u_11, u_12, u_13} (M := Y₁) (N := Y₂) (P := Y₃) (⇑g₁₂ : (a : Y₁) → Y₂) (⇑g₂₃ : (a : Y₂) → Y₃)

Tactic:
(iff_of_ladder_mulEquiv _ _ _ comm₁₂ comm₂₃).2 H

Premises used: Iff.mpr, Function.MulExact.iff_of_ladder_mulEquiv
-- Module: Mathlib.Algebra.Exact
Goal:
X₁ : Type u_8
X₂ : Type u_9
X₃ : Type u_10
Y₁ : Type u_11
Y₂ : Type u_12
Y₃ : Type u_13
inst : CommMonoid X₁
inst_1 : CommMonoid X₂
inst_2 : CommMonoid X₃
inst_3 : CommMonoid Y₁
inst_4 : CommMonoid Y₂
inst_5 : CommMonoid Y₃
e₁ : X₁ ≃* Y₁
e₂ : X₂ ≃* Y₂
e₃ : X₃ ≃* Y₃
f₁₂ : X₁ →* X₂
f₂₃ : X₂ →* X₃
g₁₂ : Y₁ →* Y₂
g₂₃ : Y₂ →* Y₃
comm₁₂ : g₁₂.comp (↑e₁ : X₁ →* Y₁) = MonoidHom.comp (↑e₂ : X₂ →* Y₂) f₁₂
comm₂₃ : g₂₃.comp (↑e₂ : X₂ →* Y₂) = MonoidHom.comp (↑e₃ : X₃ →* Y₃) f₂₃
H : MulExact.{u_11, u_12, u_13} (M := Y₁) (N := Y₂) (P := Y₃) (⇑g₁₂ : (a : Y₁) → Y₂) (⇑g₂₃ : (a : Y₂) → Y₃)
⊢ MulExact.{u_8, u_9, u_10} (M := X₁) (N := X₂) (P := X₃) (⇑f₁₂ : (a : X₁) → X₂) (⇑f₂₃ : (a : X₂) → X₃)

Tactic:
(iff_of_ladder_mulEquiv _ _ _ comm₁₂ comm₂₃).1 H

Premises used: Function.MulExact.iff_of_ladder_mulEquiv, Iff.mp
-- Module: Mathlib.Algebra.Exact
Goal:
M : Type u_2
N : Type u_4
P : Type u_6
inst : Group M
inst_1 : Group N
inst_2 : Group P
f : M →* N
g : N →* P
⊢ MulExact.{u_2, u_4, u_6} (M := M) (N := N) (P := P) (⇑f : (a : M) → N) (⇑g : (a : N) → P) ↔
    MulExact.{u_4, u_4, u_6} (M := ↥f.range) (N := N) (P := ↥g.range) (⇑f.range.subtype : (a : ↥f.range) → N)
      (⇑g.rangeRestrict : (a : N) → ↥g.range)

Tactic:
iff_rangeFactorization (one_mem g.range)

Premises used: MonoidHom.range, Function.MulExact.iff_rangeFactorization, Set.Mem, setOf, Set.range, Set.rangeFactorization, OneMemClass.one_mem
-- Module: Mathlib.Algebra.Exact
Goal:
R : Type u_1
M : Type u_2
N : Type u_4
P : Type u_6
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : AddCommMonoid P
inst_4 : Module R M
inst_5 : Module R N
inst_6 : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
⊢ Exact.{u_2, u_4, u_6} (M := M) (N := N) (P := P) (⇑f : (a : M) → N) (⇑g : (a : N) → P) ↔ g.ker = f.range

Tactic:
Iff.symm SetLike.ext_iff

Premises used: SetLike.ext_iff, Iff.symm
-- Module: Mathlib.Algebra.Exact
Goal:
R : Type u_1
M : Type u_2
N : Type u_4
P : Type u_6
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : AddCommMonoid P
inst_4 : Module R M
inst_5 : Module R N
inst_6 : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
h1 : g ∘ₗ f = 0
h2 : g.ker ≤ f.range
⊢ Exact.{u_2, u_4, u_6} (M := M) (N := N) (P := P) (⇑f : (a : M) → N) (⇑g : (a : N) → P)

Tactic:
Exact.of_comp_of_mem_range (congrArg DFunLike.coe h1) h2

Premises used: Function.Exact.of_comp_of_mem_range, congrArg, DFunLike.coe
-- Module: Mathlib.Algebra.Exact
Goal:
R : Type u_1
M : Type u_2
N : Type u_4
P : Type u_6
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : AddCommMonoid P
inst_4 : Module R M
inst_5 : Module R N
inst_6 : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
h1 : g ∘ₗ f = 0
h2 : ∀ (x : N), Eq.{u_6 + 1} (α := P) ((g : (a : N) → P) x : P) (0 : P) → x ∈ f.range
⊢ Exact.{u_2, u_4, u_6} (M := M) (N := N) (P := P) (⇑f : (a : M) → N) (⇑g : (a : N) → P)

Tactic:
exact_of_comp_eq_zero_of_ker_le_range h1 h2

Premises used: LinearMap.exact_of_comp_eq_zero_of_ker_le_range
-- Module: Mathlib.Algebra.Exact
Goal:
R : Type u_8
N : Type u_10
inst : Ring R
inst_1 : AddCommGroup N
inst_2 : Module R N
Q : Submodule R N
rw : Q.mkQ.ker = Q.subtype.range
rw₁ : Q = Q.subtype.range
rw₂ rw₃ : Q = Q
⊢ Exact (M := ↥Q) (N := N) (P := N ⧸ Q) (⇑Q.subtype : (a : ↥Q) → N) (⇑Q.mkQ : (a : N) → N ⧸ Q)

Tactic:
rw [exact_iff, Submodule.ker_mkQ, Submodule.range_subtype Q]

Premises used: Submodule.ker_mkQ, LinearMap.exact_iff, Submodule.range_subtype
-- Module: Mathlib.Algebra.Exact
Goal:
R : Type u_8
M : Type u_9
N : Type u_10
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Module R M
inst_4 : Module R N
f : M →ₗ[R] N
⊢ Exact.{u_9, u_10, u_10} (M := M) (N := N) (P := N ⧸ f.range) (⇑f : (a : M) → N) (⇑f.range.mkQ : (a : N) → N ⧸ f.range)

Tactic:
exact_iff.mpr <| Submodule.ker_mkQ _

Premises used: Iff.mpr, Submodule.ker_mkQ, LinearMap.exact_iff
-- Module: Mathlib.Algebra.Exact
Goal:
R : Type u_8
N : Type u_10
P : Type u_11
inst : Ring R
inst_1 : AddCommGroup N
inst_2 : AddCommGroup P
inst_3 : Module R N
inst_4 : Module R P
g : N →ₗ[R] P
⊢ Exact.{u_10, u_10, u_11} (M := ↥g.ker) (N := N) (P := P) (⇑g.ker.subtype : (a : ↥g.ker) → N) (⇑g : (a : N) → P)

Tactic:
exact_iff.mpr <| (Submodule.range_subtype _).symm

Premises used: Iff.mpr, LinearMap.exact_iff, Eq.symm, Submodule.range_subtype
-- Module: Mathlib.Algebra.Exact
Goal:
R : Type u_8
inst : Ring R
M : Type u_12
N : Type u_13
P : Type u_14
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : AddCommMonoid P
inst_4 : Module R N
inst_5 : Module R M
inst_6 : Module R P
f : M →ₗ[R] N
⊢ Exact.{u_14, u_12, u_13} (M := P) (N := M) (P := N) (⇑0 : (a : P) → M) (⇑f : (a : M) → N) ↔
    Injective.{u_12 + 1, u_13 + 1} (α := M) (β := N) (⇑f : (a : M) → N)

Tactic:
simp [← ker_eq_bot, exact_iff]

Premises used: LinearMap.ker_eq_bot, LinearMap.exact_iff
-- Module: Mathlib.Algebra.Exact
Goal:
R : Type u_1
inst : Semiring R
M : Type u_8
N : Type u_9
P : Type u_10
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : AddCommMonoid P
inst_4 : Module R N
inst_5 : Module R M
inst_6 : Module R P
f : M →ₗ[R] N
⊢ Exact.{u_8, u_9, u_10} (M := M) (N := N) (P := P) (⇑f : (a : M) → N) (⇑0 : (a : N) → P) ↔
    Surjective.{u_8 + 1, u_9 + 1} (α := M) (β := N) (⇑f : (a : M) → N)

Tactic:
simp [range_eq_top, exact_iff, eqComm]

Premises used: LinearMap.range_eq_top, LinearMap.exact_iff, eqComm
-- Module: Mathlib.Algebra.Exact
Goal:
R : Type u_1
M : Type u_2
N : Type u_4
N' : Type u_5
P : Type u_6
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : AddCommMonoid N'
inst_4 : AddCommMonoid P
inst_5 : Module R M
inst_6 : Module R N
inst_7 : Module R N'
inst_8 : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
e : N ≃ₗ[R] N'
simp_rw : Submodule.map (↑e : N →ₗ[R] N') g.ker = Submodule.map (↑e : N →ₗ[R] N') f.range ↔ g.ker = f.range
⊢ Exact.{u_2, u_5, u_6} (M := M) (N := N') (P := P) (⇑((↑e : N →ₗ[R] N') ∘ₗ f) : (a : M) → N')
      (⇑(g ∘ₗ (↑e.symm : N' →ₗ[R] N)) : (a : N') → P) ↔
    Exact.{u_2, u_4, u_6} (M := M) (N := N) (P := P) (⇑f : (a : M) → N) (⇑g : (a : N) → P)

Tactic:
simp_rw [LinearMap.exact_iff, LinearMap.ker_comp, ← Submodule.map_equiv_eq_comap_symm,
    LinearMap.range_comp]

Premises used: LinearMap.range_comp, LinearMap.ker_comp, Submodule.map_equiv_eq_comap_symm, LinearMap.exact_iff
-- Module: Mathlib.Algebra.Exact
Goal:
R : Type u_1
M : Type u_2
N : Type u_4
N' : Type u_5
P : Type u_6
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : AddCommMonoid N'
inst_4 : AddCommMonoid P
inst_5 : Module R M
inst_6 : Module R N
inst_7 : Module R N'
inst_8 : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
e : N ≃ₗ[R] N'
⊢ Submodule.map (↑e : N →ₗ[R] N') g.ker = Submodule.map (↑e : N →ₗ[R] N') f.range ↔ g.ker = f.range

Tactic:
(Submodule.map_injective_of_injective e.injective).eq_iff

Premises used: Function.Injective.eq_iff, LinearEquiv.injective, Submodule.map_injective_of_injective
-- Module: Mathlib.Algebra.Exact
Goal:
R : Type u_1
M : Type u_2
N : Type u_4
N' : Type u_5
P : Type u_6
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : AddCommMonoid N'
inst_4 : AddCommMonoid P
inst_5 : Module R M
inst_6 : Module R N
inst_7 : Module R N'
inst_8 : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
e : N ≃ₗ[R] N'
⊢ Submodule.map (↑e : N →ₗ[R] N') g.ker = Submodule.map (↑e : N →ₗ[R] N') f.range ↔ g.ker = f.range

Tactic:
exact (Submodule.map_injective_of_injective e.injective).eq_iff

Premises used: Function.Injective.eq_iff, LinearEquiv.injective, Submodule.map_injective_of_injective
-- Module: Mathlib.Algebra.Exact
Goal:
R : Type u_1
M : Type u_2
N : Type u_4
N' : Type u_5
P : Type u_6
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : AddCommMonoid N'
inst_4 : AddCommMonoid P
inst_5 : Module R M
inst_6 : Module R N
inst_7 : Module R N'
inst_8 : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
e : N' ≃ₗ[R] N
⊢ Exact.{u_2, u_5, u_6} (M := M) (N := N') (P := P) (⇑((↑e.symm : N →ₗ[R] N') ∘ₗ f) : (a : M) → N')
      (⇑(g ∘ₗ (↑e : N' →ₗ[R] N)) : (a : N') → P) ↔
    Exact.{u_2, u_4, u_6} (M := M) (N := N) (P := P) (⇑f : (a : M) → N) (⇑g : (a : N) → P)

Tactic:
LinearEquiv.conj_exact_iff_exact _ _ e.symm

Premises used: LinearEquiv.symm, LinearEquiv.conj_exact_iff_exact
-- Module: Mathlib.Algebra.Exact
Goal:
R : Type u_1
M : Type u_2
N : Type u_4
P : Type u_6
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : AddCommMonoid P
inst_4 : Module R M
inst_5 : Module R N
inst_6 : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
hfg : Exact.{u_2, u_4, u_6} (M := M) (N := N) (P := P) (⇑f : (a : M) → N) (⇑g : (a : N) → P)
⊢ g.ker = f.range

Tactic:
SetLike.ext hfg

Premises used: SetLike.ext
-- Module: Mathlib.Algebra.Exact
Goal:
R : Type u_1
M : Type u_2
N : Type u_4
P : Type u_6
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : AddCommMonoid 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)
⊢ g ∘ₗ f = 0

Tactic:
DFunLike.coe_injective h.comp_eq_zero

Premises used: Function.Exact.comp_eq_zero, DFunLike.coe_injective
-- Module: Mathlib.Algebra.Exact
Goal:
R : Type u_1
M : Type u_2
M' : Type u_3
N : Type u_4
P : Type u_6
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M'
inst_3 : AddCommMonoid N
inst_4 : AddCommMonoid P
inst_5 : Module R M
inst_6 : Module R M'
inst_7 : Module R N
inst_8 : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
p : M' →ₗ[R] M
h : Surjective.{u_3 + 1, u_2 + 1} (α := M') (β := M) (⇑p : (a : M') → M)
⊢ Exact.{u_3, u_4, u_6} (M := M') (N := N) (P := P) (⇑(f ∘ₗ p) : (a : M') → N) (⇑g : (a : N) → P) ↔
    Exact.{u_2, u_4, u_6} (M := M) (N := N) (P := P) (⇑f : (a : M) → N) (⇑g : (a : N) → P)

Tactic:
iff_of_eq <| forall_congr fun x =>
    congrArg (g x = 0 ↔ x ∈ ·) (h.range_comp f)

Premises used: congrArg, Membership.mem, Function.Surjective.range_comp, Iff, OfNat.ofNat, Eq, DFunLike.coe, iff_of_eq, forall_congr
-- Module: Mathlib.Algebra.Exact
Goal:
R : Type u_1
M : Type u_2
M' : Type u_3
N : Type u_4
P : Type u_6
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M'
inst_3 : AddCommMonoid N
inst_4 : AddCommMonoid P
inst_5 : Module R M
inst_6 : Module R M'
inst_7 : Module R N
inst_8 : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
e : M' ≃ₗ[R] M
⊢ Exact.{u_3, u_4, u_6} (M := M') (N := N) (P := P) (⇑(f ∘ₗ (↑e : M' →ₗ[R] M)) : (a : M') → N) (⇑g : (a : N) → P) ↔
    Exact.{u_2, u_4, u_6} (M := M) (N := N) (P := P) (⇑f : (a : M) → N) (⇑g : (a : N) → P)

Tactic:
e.surjective.comp_exact_iff_exact

Premises used: LinearEquiv.surjective, Function.Surjective.comp_exact_iff_exact
-- Module: Mathlib.Algebra.Exact
Goal:
R : Type u_1
M : Type u_2
N : Type u_4
P : Type u_6
P' : Type u_7
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : AddCommMonoid P
inst_4 : AddCommMonoid P'
inst_5 : Module R M
inst_6 : Module R N
inst_7 : Module R P
inst_8 : Module R P'
f : M →ₗ[R] N
g : N →ₗ[R] P
i : P →ₗ[R] P'
h : Injective.{u_6 + 1, u_7 + 1} (α := P) (β := P') (⇑i : (a : P) → P')
⊢ Exact.{u_2, u_4, u_7} (M := M) (N := N) (P := P') (⇑f : (a : M) → N) (⇑(i ∘ₗ g) : (a : N) → P') ↔
    Exact.{u_2, u_4, u_6} (M := M) (N := N) (P := P) (⇑f : (a : M) → N) (⇑g : (a : N) → P)

Tactic:
forall_congr' fun _ => iff_congr (map_eq_zero_iff _ h) Iff.rfl

Premises used: Function.Exact, iff_congr, Iff.rfl, map_eq_zero_iff, forall_congr'
-- Module: Mathlib.Algebra.Exact
Goal:
R : Type u_1
M : Type u_2
N : Type u_4
P : Type u_6
P' : Type u_7
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : AddCommMonoid P
inst_4 : AddCommMonoid P'
inst_5 : Module R M
inst_6 : Module R N
inst_7 : Module R P
inst_8 : Module R P'
f : M →ₗ[R] N
g : N →ₗ[R] P
e : P ≃ₗ[R] P'
⊢ Exact.{u_2, u_4, u_7} (M := M) (N := N) (P := P') (⇑f : (a : M) → N) (⇑((↑e : P →ₗ[R] P') ∘ₗ g) : (a : N) → P') ↔
    Exact.{u_2, u_4, u_6} (M := M) (N := N) (P := P) (⇑f : (a : M) → N) (⇑g : (a : N) → P)

Tactic:
e.injective.comp_exact_iff_exact

Premises used: LinearEquiv.injective, Function.Injective.comp_exact_iff_exact
-- Module: Mathlib.Algebra.Exact
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 : AddCommMonoid M
inst_2 : AddCommMonoid M'
inst_3 : AddCommMonoid N
inst_4 : AddCommMonoid N'
inst_5 : AddCommMonoid P
inst_6 : AddCommMonoid P'
inst_7 : Module R M
inst_8 : Module R M'
inst_9 : Module R N
inst_10 : Module R N'
inst_11 : Module R P
inst_12 : Module R P'
f₁₂ : M →ₗ[R] N
f₂₃ : N →ₗ[R] P
g₁₂ : M' →ₗ[R] N'
g₂₃ : N' →ₗ[R] P'
e₁ : M ≃ₗ[R] M'
e₂ : N ≃ₗ[R] N'
e₃ : P ≃ₗ[R] P'
h₁₂ : g₁₂ ∘ₗ (↑e₁ : M →ₗ[R] M') = (↑e₂ : N →ₗ[R] N') ∘ₗ f₁₂
h₂₃ : g₂₃ ∘ₗ (↑e₂ : N →ₗ[R] N') = (↑e₃ : P →ₗ[R] P') ∘ₗ f₂₃
⊢ Exact.{u_3, u_5, u_7} (M := M') (N := N') (P := P') (⇑g₁₂ : (a : M') → N') (⇑g₂₃ : (a : N') → P') ↔
    Exact.{u_2, u_4, u_6} (M := M) (N := N) (P := P) (⇑f₁₂ : (a : M) → N) (⇑f₂₃ : (a : N) → P)

Tactic:
iff_of_ladder_addEquiv e₁.toAddEquiv e₂.toAddEquiv e₃.toAddEquiv
    (f₁₂ := f₁₂) (f₂₃ := f₂₃) (g₁₂ := g₁₂) (g₂₃ := g₂₃)
    (congr_arg LinearMap.toAddMonoidHom h₁₂) (congr_arg LinearMap.toAddMonoidHom h₂₃)

Premises used: LinearMap.toAddMonoidHom, LinearEquiv.toAddEquiv, congr_arg, Function.Exact.iff_of_ladder_addEquiv
-- Module: Mathlib.Algebra.Exact
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 : AddCommMonoid M
inst_2 : AddCommMonoid M'
inst_3 : AddCommMonoid N
inst_4 : AddCommMonoid N'
inst_5 : AddCommMonoid P
inst_6 : AddCommMonoid P'
inst_7 : Module R M
inst_8 : Module R M'
inst_9 : Module R N
inst_10 : Module R N'
inst_11 : Module R P
inst_12 : Module R P'
f₁₂ : M →ₗ[R] N
f₂₃ : N →ₗ[R] P
g₁₂ : M' →ₗ[R] N'
g₂₃ : N' →ₗ[R] P'
e₁ : M ≃ₗ[R] M'
e₂ : N ≃ₗ[R] N'
e₃ : P ≃ₗ[R] P'
h₁₂ : g₁₂ ∘ₗ (↑e₁ : M →ₗ[R] M') = (↑e₂ : N →ₗ[R] N') ∘ₗ f₁₂
h₂₃ : g₂₃ ∘ₗ (↑e₂ : N →ₗ[R] N') = (↑e₃ : P →ₗ[R] P') ∘ₗ f₂₃
H rwa rwa₁ rwa₂ rwa₃ : Exact.{u_2, u_4, u_6} (M := M) (N := N) (P := P) (⇑f₁₂ : (a : M) → N) (⇑f₂₃ : (a : N) → P)
⊢ Exact.{u_3, u_5, u_7} (M := M') (N := N') (P := P') (⇑g₁₂ : (a : M') → N') (⇑g₂₃ : (a : N') → P')

Tactic:
rwa [iff_of_ladder_linearEquiv h₁₂ h₂₃]

Premises used: Function.Exact.iff_of_ladder_linearEquiv
-- Module: Mathlib.Algebra.Exact
Goal:
R : Type u_1
M : Type u_2
N : Type u_4
P : Type u_6
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : AddCommMonoid P
inst_4 : Module R M
inst_5 : Module R N
inst_6 : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
⊢ Exact.{u_2, u_4, u_6} (M := M) (N := N) (P := P) (⇑f : (a : M) → N) (⇑g : (a : N) → P) ↔
    Exact.{u_4, u_4, u_6} (M := ↥f.range) (N := N) (P := ↥g.range) (⇑f.range.subtype : (a : ↥f.range) → N)
      (⇑g.rangeRestrict : (a : N) → ↥g.range)

Tactic:
iff_rangeFactorization (zero_mem (LinearMap.range g))

Premises used: Set.Mem, setOf, LinearMap.range, Function.Exact.iff_rangeFactorization, ZeroMemClass.zero_mem, Set.range, Set.rangeFactorization
-- Module: Mathlib.Algebra.Exact
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)
refine_1 :
  ∀ (l : { l : P →ₗ[R] N // g ∘ₗ l = LinearMap.id }),
    Bijective (α := M × P) (β := N) (⇑(f ∘ₗ fst R M P + (↑l : P →ₗ[R] N) ∘ₗ snd R M P) : (a : M × P) → N)
refine_2 :
  ∀ (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)
refine_3 :
  ∀ (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
refine_4 :
  LeftInverse
    (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) ⋯)
    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) ⋯)) ⋯
refine_5 :
  RightInverse
    (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) ⋯)
    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) ⋯)) ⋯
⊢ { l : P →ₗ[R] N // g ∘ₗ l = 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) }

Tactic:
refine
  { toFun := fun l ↦ ⟨(LinearEquiv.ofBijective (f ∘ₗ fst R M P + l.1 ∘ₗ snd R M P) ?_).symm, ?_⟩
    invFun := fun e ↦ ⟨e.1.symm ∘ₗ inr R M P, ?_⟩
    left_inv := ?_
    right_inv := ?_ }
-- Module: Mathlib.Algebra.Exact
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 }
⊢ ∀ (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
-- Module: Mathlib.Algebra.Exact
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
⊢ ∀ (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
-- Module: Mathlib.Algebra.Exact
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)
refine_1₁ : Surjective (α := 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)

Tactic:
constructor