awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : 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)
tfae_1_to_3 :
  ∀ (a : Injective.{u_2 + 1, u_4 + 1} (α := M) (β := N) (⇑f : (a : M) → N) ∧ ∃ (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)
tfae_2_to_3 :
  ∀ (a : Surjective.{u_4 + 1, u_6 + 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)
tfae_3_to_1 :
  ∀ (a : ∃ (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)),
    Injective.{u_2 + 1, u_4 + 1} (α := M) (β := N) (⇑f : (a : M) → N) ∧ ∃ (l : P →ₗ[R] N), g ∘ₗ l = LinearMap.id
tfae_3_to_2 :
  ∀ (a : ∃ (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)),
    Surjective.{u_4 + 1, u_6 + 1} (α := N) (β := P) (⇑g : (a : N) → P) ∧ ∃ (l : N →ₗ[R] M), l ∘ₗ f = LinearMap.id
⊢ [Injective.{u_2 + 1, u_4 + 1} (α := M) (β := N) (⇑f : (a : M) → N) ∧ ∃ (l : P →ₗ[R] N), g ∘ₗ l = LinearMap.id,
      Surjective.{u_4 + 1, u_6 + 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)].TFAE

Tactic:
tfae_finish
-- Module: Mathlib.Algebra.Exact
Goal:
R : Type u_8
M : Type u_9
N : Type u_10
P : Type u_11
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_9, u_10, u_11} (M := M) (N := N) (P := P) (⇑f : (a : M) → N) (⇑g : (a : N) → P)
hf : Injective.{u_9 + 1, u_10 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
hg : Surjective.{u_10 + 1, u_11 + 1} (α := N) (β := P) (⇑g : (a : N) → P)
⊢ ∃ (l : P →ₗ[R] N), g ∘ₗ l = LinearMap.id

Tactic:
1

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Algebra.Exact
Goal:
R : Type u_8
M : Type u_9
N : Type u_10
P : Type u_11
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_9, u_10, u_11} (M := M) (N := N) (P := P) (⇑f : (a : M) → N) (⇑g : (a : N) → P)
hf : Injective.{u_9 + 1, u_10 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
hg : Surjective.{u_10 + 1, u_11 + 1} (α := N) (β := P) (⇑g : (a : N) → 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)

Tactic:
3

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Algebra.Exact
Goal:
R : Type u_8
M : Type u_9
N : Type u_10
P : Type u_11
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_9, u_10, u_11} (M := M) (N := N) (P := P) (⇑f : (a : M) → N) (⇑g : (a : N) → P)
hf : Injective.{u_9 + 1, u_10 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
hg : Surjective.{u_10 + 1, u_11 + 1} (α := N) (β := P) (⇑g : (a : N) → 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:
1 ↔ 3

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Algebra.Exact
Goal:
R : Type u_8
M : Type u_9
N : Type u_10
P : Type u_11
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_9, u_10, u_11} (M := M) (N := N) (P := P) (⇑f : (a : M) → N) (⇑g : (a : N) → P)
hf : Injective.{u_9 + 1, u_10 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
hg : Surjective.{u_10 + 1, u_11 + 1} (α := N) (β := P) (⇑g : (a : N) → 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:
simpa using (h.splitSurjectiveEquiv hf).nonempty_congr

Premises used: Equiv.nonempty_congr, Function.Exact.splitSurjectiveEquiv
-- Module: Mathlib.Algebra.Exact
Goal:
R : Type u_8
M : Type u_9
N : Type u_10
P : Type u_11
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_9, u_10, u_11} (M := M) (N := N) (P := P) (⇑f : (a : M) → N) (⇑g : (a : N) → P)
hf : Injective.{u_9 + 1, u_10 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
hg : Surjective.{u_10 + 1, u_11 + 1} (α := N) (β := P) (⇑g : (a : N) → 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:
tfae_have 1 ↔ 3 := by
    simpa using (h.splitSurjectiveEquiv hf).nonempty_congr
-- Module: Mathlib.Algebra.Exact
Goal:
R : Type u_8
M : Type u_9
N : Type u_10
P : Type u_11
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_9, u_10, u_11} (M := M) (N := N) (P := P) (⇑f : (a : M) → N) (⇑g : (a : N) → P)
hf : Injective.{u_9 + 1, u_10 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
hg : Surjective.{u_10 + 1, u_11 + 1} (α := N) (β := P) (⇑g : (a : N) → P)
tfae_1_iff_3 :
  (∃ (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)
⊢ ∃ (l : N →ₗ[R] M), l ∘ₗ f = LinearMap.id

Tactic:
2

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Algebra.Exact
Goal:
R : Type u_8
M : Type u_9
N : Type u_10
P : Type u_11
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_9, u_10, u_11} (M := M) (N := N) (P := P) (⇑f : (a : M) → N) (⇑g : (a : N) → P)
hf : Injective.{u_9 + 1, u_10 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
hg : Surjective.{u_10 + 1, u_11 + 1} (α := N) (β := P) (⇑g : (a : N) → P)
tfae_1_iff_3 :
  (∃ (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)
⊢ ∃ (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:
3

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Algebra.Exact
Goal:
R : Type u_8
M : Type u_9
N : Type u_10
P : Type u_11
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_9, u_10, u_11} (M := M) (N := N) (P := P) (⇑f : (a : M) → N) (⇑g : (a : N) → P)
hf : Injective.{u_9 + 1, u_10 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
hg : Surjective.{u_10 + 1, u_11 + 1} (α := N) (β := P) (⇑g : (a : N) → P)
tfae_1_iff_3 :
  (∃ (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)
⊢ (∃ (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)

Tactic:
2 ↔ 3

Premises used: sorryAx, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous, OfNat.ofNat, Bool.false
-- Module: Mathlib.Algebra.Exact
Goal:
R : Type u_8
M : Type u_9
N : Type u_10
P : Type u_11
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_9, u_10, u_11} (M := M) (N := N) (P := P) (⇑f : (a : M) → N) (⇑g : (a : N) → P)
hf : Injective.{u_9 + 1, u_10 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
hg : Surjective.{u_10 + 1, u_11 + 1} (α := N) (β := P) (⇑g : (a : N) → P)
tfae_1_iff_3 :
  (∃ (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)
⊢ (∃ (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)

Tactic:
simpa using (h.splitInjectiveEquiv hg).nonempty_congr

Premises used: Equiv.nonempty_congr, Function.Exact.splitInjectiveEquiv
-- Module: Mathlib.Algebra.Exact
Goal:
R : Type u_8
M : Type u_9
N : Type u_10
P : Type u_11
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_9, u_10, u_11} (M := M) (N := N) (P := P) (⇑f : (a : M) → N) (⇑g : (a : N) → P)
hf : Injective.{u_9 + 1, u_10 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
hg : Surjective.{u_10 + 1, u_11 + 1} (α := N) (β := P) (⇑g : (a : N) → P)
tfae_1_iff_3 :
  (∃ (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)
⊢ (∃ (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)

Tactic:
tfae_have 2 ↔ 3 := by
    simpa using (h.splitInjectiveEquiv hg).nonempty_congr
-- Module: Mathlib.Algebra.Exact
Goal:
R : Type u_8
M : Type u_9
N : Type u_10
P : Type u_11
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_9, u_10, u_11} (M := M) (N := N) (P := P) (⇑f : (a : M) → N) (⇑g : (a : N) → P)
hf : Injective.{u_9 + 1, u_10 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
hg : Surjective.{u_10 + 1, u_11 + 1} (α := N) (β := P) (⇑g : (a : N) → P)
tfae_1_iff_3 :
  (∃ (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)
tfae_2_iff_3 :
  (∃ (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)
⊢ [∃ (l : P →ₗ[R] N), g ∘ₗ l = LinearMap.id, ∃ (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)].TFAE

Tactic:
tfae_finish
-- Module: Mathlib.Algebra.Exact
Goal:
R : Type u_1
M : Type u_2
N : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
x : M
y : N
⊢ Eq.{u_2 + 1} (α := M) ((LinearMap.fst R M N : (a : M × N) → M) (x, y) : M) (0 : M) ↔
    Membership.mem (γ := Set (M × N)) (Set.range (ι := N) (⇑(LinearMap.inr R M N) : (a : N) → M × N)) (x, y)

Tactic:
simp only [LinearMap.fst_apply, @eq_comm _ x, LinearMap.coe_inr, Set.mem_range, Prod.mk.injEq,
    exists_eq_right]

Premises used: Set.mem_range, LinearMap.coe_inr, exists_eq_right, eq_comm, LinearMap.fst_apply, Prod.mk.injEq
-- Module: Mathlib.Algebra.Exact
Goal:
R : Type u_1
M : Type u_2
N : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
x : M
y : N
⊢ Eq.{u_4 + 1} (α := N) ((LinearMap.snd R M N : (a : M × N) → N) (x, y) : N) (0 : N) ↔
    Membership.mem (γ := Set (M × N)) (Set.range (ι := M) (⇑(LinearMap.inl R M N) : (a : M) → M × N)) (x, y)

Tactic:
simp only [LinearMap.snd_apply, @eq_comm _ y, LinearMap.coe_inl, Set.mem_range, Prod.mk.injEq,
    exists_eq_left]

Premises used: Set.mem_range, exists_eq_left, eq_comm, LinearMap.coe_inl, Prod.mk.injEq, LinearMap.snd_apply
-- Module: Mathlib.Algebra.Exact
Goal:
R : Type u_1
M : Type u_2
N : Type u_4
P : Type u_6
inst : Ring 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
hfg : Exact.{u_2, u_4, u_6} (M := M) (N := N) (P := P) (⇑f : (a : M) → N) (⇑g : (a : N) → P)
p : Submodule R M
q : Submodule R N
r : Submodule R P
hpq : p ≤ comap f q
hqr : q ≤ comap g r
rw : comap q.mkQ (q.mapQ r g hqr).ker = comap q.mkQ (p.mapQ q f hpq).range ↔ g.range ⊓ r ≤ map g q
⊢ Exact.{u_2, u_4, u_6} (M := M ⧸ p) (N := N ⧸ q) (P := P ⧸ r) (⇑(p.mapQ q f hpq) : (a : M ⧸ p) → N ⧸ q)
      (⇑(q.mapQ r g hqr) : (a : N ⧸ q) → P ⧸ r) ↔
    g.range ⊓ r ≤ map g q

Tactic:
rw [exact_iff, ← (comap_injective_of_surjective (mkQ_surjective _)).eq_iff]

Premises used: Function.Injective.eq_iff, Submodule.comap_injective_of_surjective, Submodule.mkQ_surjective, LinearMap.exact_iff
-- Module: Mathlib.Algebra.Exact
Goal:
R : Type u_1
M : Type u_2
N : Type u_4
P : Type u_6
inst : Ring 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
hfg : Exact.{u_2, u_4, u_6} (M := M) (N := N) (P := P) (⇑f : (a : M) → N) (⇑g : (a : N) → P)
p : Submodule R M
q : Submodule R N
r : Submodule R P
hpq : p ≤ comap f q
hqr : q ≤ comap g r
rw : (q.liftQ (r.mkQ ∘ₗ g) ⋯ ∘ₗ q.mkQ).ker = comap q.mkQ (p.liftQ (q.mkQ ∘ₗ f) ⋯).range ↔ g.range ⊓ r ≤ map g q
rw₁ : (q.liftQ (r.mkQ ∘ₗ g) ⋯ ∘ₗ q.mkQ).ker = comap q.mkQ (q.mkQ ∘ₗ f).range ↔ g.range ⊓ r ≤ map g q
rw₂ : (r.mkQ ∘ₗ g).ker = comap q.mkQ (q.mkQ ∘ₗ f).range ↔ g.range ⊓ r ≤ map g q
rw₃ : comap g r.mkQ.ker = comap q.mkQ (q.mkQ ∘ₗ f).range ↔ g.range ⊓ r ≤ map g q
rw₄ : comap g r.mkQ.ker = comap q.mkQ (map q.mkQ f.range) ↔ g.range ⊓ r ≤ map g q
rw₅ : comap g r.mkQ.ker = f.range ⊔ q.mkQ.ker ↔ g.range ⊓ r ≤ map g q
rw₆ : comap g r = f.range ⊔ q.mkQ.ker ↔ g.range ⊓ r ≤ map g q
rw₇ : comap g r = f.range ⊔ q ↔ g.range ⊓ r ≤ map g q
rw₈ : comap g r = g.ker ⊔ q ↔ g.range ⊓ r ≤ map g q
rw₉ : comap g r = q ⊔ g.ker ↔ g.range ⊓ r ≤ map g q
rw₁₀ : comap g r ≤ q ⊔ g.ker ↔ g.range ⊓ r ≤ map g q
rw₁₁ : comap g r ≤ comap g (map g q) ↔ g.range ⊓ r ≤ map g q
rw₁₂ : map g (comap g r) ≤ map g q ↔ g.range ⊓ r ≤ map g q
rw₁₃ rw₁₄ : g.range ⊓ r ≤ map g q ↔ g.range ⊓ r ≤ map g q
⊢ comap q.mkQ (q.liftQ (r.mkQ ∘ₗ g) ⋯).ker = comap q.mkQ (p.liftQ (q.mkQ ∘ₗ f) ⋯).range ↔ g.range ⊓ r ≤ map g q

Tactic:
rw [← ker_comp, range_liftQ, liftQ_mkQ, ker_comp, range_comp, comap_map_eq,
    ker_mkQ, ker_mkQ, ← hfg.linearMap_ker_eq, sup_comm,
    ← (sup_le hqr (ker_le_comap g)).ge_iff_eq',
    ← comap_map_eq, ← map_le_iff_le_comap, map_comap_eq]

Premises used: Submodule.map_comap_eq, Function.Exact.linearMap_ker_eq, LinearMap.range_comp, LinearMap.ker_comp, LE.le.ge_iff_eq', sup_comm, sup_le, Submodule.ker_mkQ, Submodule.map_le_iff_le_comap, Submodule.liftQ_mkQ, LinearMap.ker_le_comap, Submodule.range_liftQ, Submodule.comap_map_eq
-- Module: Mathlib.Algebra.Exact
Goal:
R : Type u_1
inst : Ring R
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_1 : AddCommMonoid M₁
inst_2 : AddCommMonoid M₂
inst_3 : AddCommMonoid M₃
inst_4 : AddCommMonoid N₁
inst_5 : AddCommMonoid N₂
inst_6 : AddCommMonoid N₃
inst_7 : Module R M₁
inst_8 : Module R M₂
inst_9 : Module R M₃
inst_10 : Module R N₁
inst_11 : Module R N₂
inst_12 : Module R N₃
f : M₁ →ₗ[R] M₂
g : M₂ →ₗ[R] M₃
f' : N₁ →ₗ[R] N₂
g' : N₂ →ₗ[R] N₃
τ₁ : M₁ →ₗ[R] N₁
τ₂ : M₂ →ₗ[R] N₂
τ₃ : M₃ →ₗ[R] N₃
comm₁₂ : f' ∘ₗ τ₁ = τ₂ ∘ₗ f
comm₂₃ : g' ∘ₗ τ₂ = τ₃ ∘ₗ g
h₁ : Function.Surjective.{u_8 + 1, u_11 + 1} (α := M₁) (β := N₁) (⇑τ₁ : (a : M₁) → N₁)
h₂ : Function.Bijective.{u_9 + 1, u_12 + 1} (α := M₂) (β := N₂) (⇑τ₂ : (a : M₂) → N₂)
h₃ : Function.Injective.{u_10 + 1, u_13 + 1} (α := M₃) (β := N₃) (⇑τ₃ : (a : M₃) → N₃)
h :
  ∀ (x : M₁),
    Eq.{u_12 + 1} (α := N₂) ((f'.toAddMonoidHom.comp τ₁.toAddMonoidHom : (a : M₁) → N₂) x : N₂)
      ((τ₂.toAddMonoidHom.comp f.toAddMonoidHom : (a : M₁) → N₂) x : N₂)
⊢ f'.toAddMonoidHom.comp τ₁.toAddMonoidHom = τ₂.toAddMonoidHom.comp f.toAddMonoidHom

Tactic:
ext
-- Module: Mathlib.Algebra.Exact
Goal:
R : Type u_1
inst : Ring R
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_1 : AddCommMonoid M₁
inst_2 : AddCommMonoid M₂
inst_3 : AddCommMonoid M₃
inst_4 : AddCommMonoid N₁
inst_5 : AddCommMonoid N₂
inst_6 : AddCommMonoid N₃
inst_7 : Module R M₁
inst_8 : Module R M₂
inst_9 : Module R M₃
inst_10 : Module R N₁
inst_11 : Module R N₂
inst_12 : Module R N₃
f : M₁ →ₗ[R] M₂
g : M₂ →ₗ[R] M₃
f' : N₁ →ₗ[R] N₂
g' : N₂ →ₗ[R] N₃
τ₁ : M₁ →ₗ[R] N₁
τ₂ : M₂ →ₗ[R] N₂
τ₃ : M₃ →ₗ[R] N₃
comm₁₂ : f' ∘ₗ τ₁ = τ₂ ∘ₗ f
comm₂₃ : g' ∘ₗ τ₂ = τ₃ ∘ₗ g
h₁ : Function.Surjective.{u_8 + 1, u_11 + 1} (α := M₁) (β := N₁) (⇑τ₁ : (a : M₁) → N₁)
h₂ : Function.Bijective.{u_9 + 1, u_12 + 1} (α := M₂) (β := N₂) (⇑τ₂ : (a : M₂) → N₂)
h₃ : Function.Injective.{u_10 + 1, u_13 + 1} (α := M₃) (β := N₃) (⇑τ₃ : (a : M₃) → N₃)
x : M₁
⊢ Eq.{u_12 + 1} (α := N₂) ((f'.toAddMonoidHom.comp τ₁.toAddMonoidHom : (a : M₁) → N₂) x : N₂)
    ((τ₂.toAddMonoidHom.comp f.toAddMonoidHom : (a : M₁) → N₂) x : N₂)

Tactic:
apply DFunLike.congr_fun comm₁₂

Premises used: DFunLike.congr_fun
-- Module: Mathlib.Algebra.Exact
Goal:
R : Type u_1
inst : Ring R
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_1 : AddCommMonoid M₁
inst_2 : AddCommMonoid M₂
inst_3 : AddCommMonoid M₃
inst_4 : AddCommMonoid N₁
inst_5 : AddCommMonoid N₂
inst_6 : AddCommMonoid N₃
inst_7 : Module R M₁
inst_8 : Module R M₂
inst_9 : Module R M₃
inst_10 : Module R N₁
inst_11 : Module R N₂
inst_12 : Module R N₃
f : M₁ →ₗ[R] M₂
g : M₂ →ₗ[R] M₃
f' : N₁ →ₗ[R] N₂
g' : N₂ →ₗ[R] N₃
τ₁ : M₁ →ₗ[R] N₁
τ₂ : M₂ →ₗ[R] N₂
τ₃ : M₃ →ₗ[R] N₃
comm₁₂ : f' ∘ₗ τ₁ = τ₂ ∘ₗ f
comm₂₃ : g' ∘ₗ τ₂ = τ₃ ∘ₗ g
h₁ : Function.Surjective.{u_8 + 1, u_11 + 1} (α := M₁) (β := N₁) (⇑τ₁ : (a : M₁) → N₁)
h₂ : Function.Bijective.{u_9 + 1, u_12 + 1} (α := M₂) (β := N₂) (⇑τ₂ : (a : M₂) → N₂)
h₃ : Function.Injective.{u_10 + 1, u_13 + 1} (α := M₃) (β := N₃) (⇑τ₃ : (a : M₃) → N₃)
h :
  ∀ (x : M₂),
    Eq.{u_13 + 1} (α := N₃) ((g'.toAddMonoidHom.comp τ₂.toAddMonoidHom : (a : M₂) → N₃) x : N₃)
      ((τ₃.toAddMonoidHom.comp g.toAddMonoidHom : (a : M₂) → N₃) x : N₃)
⊢ g'.toAddMonoidHom.comp τ₂.toAddMonoidHom = τ₃.toAddMonoidHom.comp g.toAddMonoidHom

Tactic:
ext
-- Module: Mathlib.Algebra.Exact
Goal:
R : Type u_1
inst : Ring R
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_1 : AddCommMonoid M₁
inst_2 : AddCommMonoid M₂
inst_3 : AddCommMonoid M₃
inst_4 : AddCommMonoid N₁
inst_5 : AddCommMonoid N₂
inst_6 : AddCommMonoid N₃
inst_7 : Module R M₁
inst_8 : Module R M₂
inst_9 : Module R M₃
inst_10 : Module R N₁
inst_11 : Module R N₂
inst_12 : Module R N₃
f : M₁ →ₗ[R] M₂
g : M₂ →ₗ[R] M₃
f' : N₁ →ₗ[R] N₂
g' : N₂ →ₗ[R] N₃
τ₁ : M₁ →ₗ[R] N₁
τ₂ : M₂ →ₗ[R] N₂
τ₃ : M₃ →ₗ[R] N₃
comm₁₂ : f' ∘ₗ τ₁ = τ₂ ∘ₗ f
comm₂₃ : g' ∘ₗ τ₂ = τ₃ ∘ₗ g
h₁ : Function.Surjective.{u_8 + 1, u_11 + 1} (α := M₁) (β := N₁) (⇑τ₁ : (a : M₁) → N₁)
h₂ : Function.Bijective.{u_9 + 1, u_12 + 1} (α := M₂) (β := N₂) (⇑τ₂ : (a : M₂) → N₂)
h₃ : Function.Injective.{u_10 + 1, u_13 + 1} (α := M₃) (β := N₃) (⇑τ₃ : (a : M₃) → N₃)
x : M₂
⊢ Eq.{u_13 + 1} (α := N₃) ((g'.toAddMonoidHom.comp τ₂.toAddMonoidHom : (a : M₂) → N₃) x : N₃)
    ((τ₃.toAddMonoidHom.comp g.toAddMonoidHom : (a : M₂) → N₃) x : N₃)

Tactic:
apply DFunLike.congr_fun comm₂₃

Premises used: DFunLike.congr_fun
-- Module: Mathlib.Algebra.Exact
Goal:
R : Type u_1
M : Type u_2
N : Type u_4
P : Type u_6
inst : Ring 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 : f.range ≤ g.ker
hg : Function.Surjective.{u_4 + 1, u_6 + 1} (α := N) (β := P) (⇑g : (a : N) → P)
x₃ : P
obtain :
  ∀ (x₂ : N),
    ∃ (a : N ⧸ f.range),
      Eq.{u_6 + 1} (α := P) ((f.range.liftQ g h : (a : N ⧸ f.range) → P) a : P) ((g : (a : N) → P) x₂ : P)
⊢ ∃ (a : N ⧸ f.range), (f.range.liftQ g h : (a : N ⧸ f.range) → P) a = x₃

Tactic:
obtain ⟨x₂, rfl⟩ := hg x₃

Premises used: rfl
-- Module: Mathlib.Algebra.Exact
Goal:
R : Type u_1
M : Type u_2
N : Type u_4
P : Type u_6
inst : Ring 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 : f.range ≤ g.ker
hg : Function.Surjective.{u_4 + 1, u_6 + 1} (α := N) (β := P) (⇑g : (a : N) → P)
x₂ : N
⊢ ∃ (a : N ⧸ f.range),
    Eq.{u_6 + 1} (α := P) ((f.range.liftQ g h : (a : N ⧸ f.range) → P) a : P) ((g : (a : N) → P) x₂ : P)

Tactic:
⟨Submodule.Quotient.mk x₂, rfl⟩

Premises used: Submodule.Quotient.mk, Exists.intro, rfl
-- Module: Mathlib.Algebra.Exact
Goal:
R : Type u_1
M : Type u_2
N : Type u_4
P : Type u_6
inst : Ring 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 : f.range ≤ g.ker
hg : Function.Surjective.{u_4 + 1, u_6 + 1} (α := N) (β := P) (⇑g : (a : N) → P)
x₂ : N
⊢ ∃ (a : N ⧸ f.range),
    Eq.{u_6 + 1} (α := P) ((f.range.liftQ g h : (a : N ⧸ f.range) → P) a : P) ((g : (a : N) → P) x₂ : P)

Tactic:
exact ⟨Submodule.Quotient.mk x₂, rfl⟩
-- Module: Mathlib.Algebra.Exact
Goal:
R : Type u_1
M : Type u_2
N : Type u_4
P : Type u_6
inst : Ring 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 : f.range ≤ g.ker
simp :
  (∀ (x : N ⧸ f.range), Eq.{u_6 + 1} (α := P) ((f.range.liftQ g h : (a : N ⧸ f.range) → P) x : P) (0 : P) ↔ x = 0) ↔
    ∀ (x : N), Eq.{u_6 + 1} (α := P) ((g : (a : N) → P) x : P) (0 : P) ↔ ∃ (y : M), (f : (a : M) → N) y = x
⊢ (f.range.liftQ g h).ker = ⊥ ↔ g.ker = f.range

Tactic:
simp only [Submodule.ext_iff, mem_ker, Submodule.mem_bot, mem_range]

Premises used: Submodule.mem_bot, Submodule.ext_iff, LinearMap.mem_ker, LinearMap.mem_range
-- Module: Mathlib.Algebra.Exact
Goal:
R : Type u_1
M : Type u_2
N : Type u_4
P : Type u_6
inst : Ring 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 : f.range ≤ g.ker
mp :
  (∀ (x : N ⧸ f.range), Eq.{u_6 + 1} (α := P) ((f.range.liftQ g h : (a : N ⧸ f.range) → P) x : P) (0 : P) ↔ x = 0) →
    ∀ (x : N), Eq.{u_6 + 1} (α := P) ((g : (a : N) → P) x : P) (0 : P) ↔ ∃ (y : M), (f : (a : M) → N) y = x
mpr :
  (∀ (x : N), Eq.{u_6 + 1} (α := P) ((g : (a : N) → P) x : P) (0 : P) ↔ ∃ (y : M), (f : (a : M) → N) y = x) →
    ∀ (x : N ⧸ f.range), Eq.{u_6 + 1} (α := P) ((f.range.liftQ g h : (a : N ⧸ f.range) → P) x : P) (0 : P) ↔ x = 0
⊢ (∀ (x : N ⧸ f.range), Eq.{u_6 + 1} (α := P) ((f.range.liftQ g h : (a : N ⧸ f.range) → P) x : P) (0 : P) ↔ x = 0) ↔
    ∀ (x : N), Eq.{u_6 + 1} (α := P) ((g : (a : N) → P) x : P) (0 : P) ↔ ∃ (y : M), (f : (a : M) → N) y = x

Tactic:
constructor
-- Module: Mathlib.Algebra.Exact
Goal:
R : Type u_1
M : Type u_2
N : Type u_4
P : Type u_6
inst : Ring 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 : f.range ≤ g.ker
hfg : ∀ (x : N ⧸ f.range), Eq.{u_6 + 1} (α := P) ((f.range.liftQ g h : (a : N ⧸ f.range) → P) x : P) (0 : P) ↔ x = 0
x : N
⊢ Eq.{u_6 + 1} (α := P) ((g : (a : N) → P) x : P) (0 : P) ↔ ∃ (y : M), (f : (a : M) → N) y = x

Tactic:
simpa using hfg (Submodule.Quotient.mk x)

Premises used: Submodule.Quotient.mk