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
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)
⊢ [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
have 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)
Tactic: tfae_have 1 → 3
  | ⟨hf, l, hl⟩ => ⟨_, (h.splitSurjectiveEquiv hf ⟨l, hl⟩).2⟩
-- Lean 4 proof step from Mathlib.Algebra.Exact (hypothesis)
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)
⊢ [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
have 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)
Tactic: tfae_have 2 → 3
  | ⟨hg, l, hl⟩ => ⟨_, (h.splitInjectiveEquiv hg ⟨l, hl⟩).2⟩
-- Lean 4 proof step from Mathlib.Algebra.Exact (hypothesis)
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)
e : N ≃ₗ[R] M × P
e₁ : f = (↑e.symm : M × P →ₗ[R] N) ∘ₗ inl R M P
e₂ : 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
have this : Injective.{u_2 + 1, u_4 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
Tactic: have : Function.Injective f := e₁ ▸ e.symm.injective.comp LinearMap.inl_injective
-- Lean 4 proof step from Mathlib.Algebra.Exact (hypothesis)
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)
⊢ [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
have 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
Tactic: tfae_have 3 → 1
  | ⟨e, e₁, e₂⟩ => by
    have : Function.Injective f := e₁ ▸ e.symm.injective.comp LinearMap.inl_injective
    exact ⟨this, ⟨_, ((h.splitSurjectiveEquiv this).symm ⟨e, e₁, e₂⟩).2⟩⟩
-- Lean 4 proof step from Mathlib.Algebra.Exact (hypothesis)
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
e : N ≃ₗ[R] M × P
e₁ : f = (↑e.symm : M × P →ₗ[R] N) ∘ₗ inl R M P
e₂ : 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
have this : Surjective.{u_4 + 1, u_6 + 1} (α := N) (β := P) (⇑g : (a : N) → P)
Tactic: have : Function.Surjective g := e₂ ▸ Prod.snd_surjective.comp e.surjective
-- Lean 4 proof step from Mathlib.Algebra.Exact (hypothesis)
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
⊢ [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
have 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
Tactic: tfae_have 3 → 2
  | ⟨e, e₁, e₂⟩ => by
    have : Function.Surjective g := e₂ ▸ Prod.snd_surjective.comp e.surjective
    exact ⟨this, ⟨_, ((h.splitInjectiveEquiv this).symm ⟨e, e₁, e₂⟩).2⟩⟩
-- Lean 4 proof step from Mathlib.Algebra.Exact (hypothesis)
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, ∃ (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
have 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)
Tactic: tfae_have 1 ↔ 3 := by
    simpa using (h.splitSurjectiveEquiv hf).nonempty_congr
-- Lean 4 proof step from Mathlib.Algebra.Exact (hypothesis)
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 : 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
have 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)
Tactic: tfae_have 2 ↔ 3 := by
    simpa using (h.splitInjectiveEquiv hg).nonempty_congr
-- Lean 4 proof step from Mathlib.Algebra.Exact (goal)
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
⊢ 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
have 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
Tactic: rw [exact_iff, ← (comap_injective_of_surjective (mkQ_surjective _)).eq_iff]
-- Lean 4 proof step from Mathlib.Algebra.Exact (goal)
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
⊢ comap q.mkQ (q.liftQ (r.mkQ ∘ₗ g) ⋯).ker = comap q.mkQ (p.liftQ (q.mkQ ∘ₗ f) ⋯).range ↔ g.range ⊓ r ≤ map g q
have rw : (q.liftQ (r.mkQ ∘ₗ g) sorry ∘ₗ q.mkQ).ker = comap q.mkQ (p.liftQ (q.mkQ ∘ₗ f) sorry).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]
-- Lean 4 proof step from Mathlib.Algebra.Exact (goal)
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
⊢ comap q.mkQ (q.liftQ (r.mkQ ∘ₗ g) ⋯).ker = comap q.mkQ (p.liftQ (q.mkQ ∘ₗ f) ⋯).range ↔ g.range ⊓ r ≤ map g q
have rw₁ : (q.liftQ (r.mkQ ∘ₗ g) sorry ∘ₗ q.mkQ).ker = comap q.mkQ (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]
-- Lean 4 proof step from Mathlib.Algebra.Exact (goal)
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
⊢ comap q.mkQ (q.liftQ (r.mkQ ∘ₗ g) ⋯).ker = comap q.mkQ (p.liftQ (q.mkQ ∘ₗ f) ⋯).range ↔ g.range ⊓ r ≤ map g q
have rw₂ : (r.mkQ ∘ₗ g).ker = comap q.mkQ (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]
-- Lean 4 proof step from Mathlib.Algebra.Exact (goal)
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
⊢ comap q.mkQ (q.liftQ (r.mkQ ∘ₗ g) ⋯).ker = comap q.mkQ (p.liftQ (q.mkQ ∘ₗ f) ⋯).range ↔ g.range ⊓ r ≤ map g q
have rw₃ : comap g r.mkQ.ker = comap q.mkQ (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]
-- Lean 4 proof step from Mathlib.Algebra.Exact (goal)
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
⊢ comap q.mkQ (q.liftQ (r.mkQ ∘ₗ g) ⋯).ker = comap q.mkQ (p.liftQ (q.mkQ ∘ₗ f) ⋯).range ↔ g.range ⊓ r ≤ map g q
have rw₄ : comap g r.mkQ.ker = comap q.mkQ (map 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]
-- Lean 4 proof step from Mathlib.Algebra.Exact (goal)
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
⊢ comap q.mkQ (q.liftQ (r.mkQ ∘ₗ g) ⋯).ker = comap q.mkQ (p.liftQ (q.mkQ ∘ₗ f) ⋯).range ↔ g.range ⊓ r ≤ map g q
have rw₅ : comap g r.mkQ.ker = f.range ⊔ q.mkQ.ker ↔ 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]
-- Lean 4 proof step from Mathlib.Algebra.Exact (goal)
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
⊢ comap q.mkQ (q.liftQ (r.mkQ ∘ₗ g) ⋯).ker = comap q.mkQ (p.liftQ (q.mkQ ∘ₗ f) ⋯).range ↔ g.range ⊓ r ≤ map g q
have rw₆ : comap g r = f.range ⊔ q.mkQ.ker ↔ 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]
-- Lean 4 proof step from Mathlib.Algebra.Exact (goal)
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
⊢ comap q.mkQ (q.liftQ (r.mkQ ∘ₗ g) ⋯).ker = comap q.mkQ (p.liftQ (q.mkQ ∘ₗ f) ⋯).range ↔ g.range ⊓ r ≤ map g q
have rw₇ : comap g r = f.range ⊔ q ↔ 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]
-- Lean 4 proof step from Mathlib.Algebra.Exact (goal)
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
⊢ comap q.mkQ (q.liftQ (r.mkQ ∘ₗ g) ⋯).ker = comap q.mkQ (p.liftQ (q.mkQ ∘ₗ f) ⋯).range ↔ g.range ⊓ r ≤ map g q
have rw₈ : comap g r = g.ker ⊔ q ↔ 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]