awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
rw₈ : comap g r = g.ker ⊔ 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 = q ⊔ g.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
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
⊢ 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 ≤ q ⊔ g.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
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
⊢ 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 ≤ comap g (map g 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
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
⊢ 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₁₂ : map g (comap g r) ≤ map g 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
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
⊢ 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₁₃ : g.range ⊓ r ≤ map g 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
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₃)
⊢ f'.toAddMonoidHom.comp τ₁.toAddMonoidHom = τ₂.toAddMonoidHom.comp f.toAddMonoidHom
have 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₂)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Exact (goal)
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₃)
⊢ g'.toAddMonoidHom.comp τ₂.toAddMonoidHom = τ₃.toAddMonoidHom.comp g.toAddMonoidHom
have 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₃)
Tactic: ext
-- 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
h : f.range ≤ g.ker
hg : Function.Surjective.{u_4 + 1, u_6 + 1} (α := N) (β := P) (⇑g : (a : N) → P)
x₃ : P
⊢ ∃ (a : N ⧸ f.range), (f.range.liftQ g h : (a : N ⧸ f.range) → P) a = x₃
have 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)
Tactic: obtain ⟨x₂, rfl⟩ := hg x₃
Cleared hypotheses: x₃
-- 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
h : f.range ≤ g.ker
⊢ (f.range.liftQ g h).ker = ⊥ ↔ g.ker = f.range
have 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
Tactic: simp only [Submodule.ext_iff, mem_ker, Submodule.mem_bot, mem_range]
-- 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
h : f.range ≤ g.ker
⊢ (∀ (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
have 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
Tactic: constructor
-- 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
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
⊢ (∀ (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
have 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
Tactic: constructor
-- 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
h : f.range ≤ g.ker
hfg : ∀ (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
have mpr : ∀ (x : N),
  Eq.{u_6 + 1} (α := P) ((f.range.liftQ g h : (a : N ⧸ f.range) → P) (Submodule.Quotient.mk x) : P) (0 : P) ↔
    Eq (α := N ⧸ f.range) (Submodule.Quotient.mk x) 0
Tactic: obtain ⟨x, rfl⟩ := Submodule.Quotient.mk_surjective _ x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Algebra.Field.Basic (goal)
Goal:
K : Type u_1
inst : DivisionSemiring K
a b c : K
⊢ (a + b) / c = a / c + b / c
have simp_rw : (a + b) * c⁻¹ = a * c⁻¹ + b * c⁻¹
Tactic: simp_rw [div_eq_mul_inv, add_mul]
-- Lean 4 proof step from Mathlib.Algebra.Field.Basic (goal)
Goal:
K : Type u_1
inst : DivisionSemiring K
a b : K
h : b ≠ 0
⊢ (b + a) / b = 1 + a / b
have rw : (b + a) / b = b / b + a / b
Tactic: rw [← div_self h, add_div]
-- Lean 4 proof step from Mathlib.Algebra.Field.Basic (goal)
Goal:
K : Type u_1
inst : DivisionSemiring K
a b : K
h : b ≠ 0
rw : (b + a) / b = b / b + a / b
⊢ (b + a) / b = 1 + a / b
have rw₁ : b / b + a / b = b / b + a / b
Tactic: rw [← div_self h, add_div]
-- Lean 4 proof step from Mathlib.Algebra.Field.Basic (goal)
Goal:
K : Type u_1
inst : DivisionSemiring K
a b : K
h : b ≠ 0
⊢ (a + b) / b = a / b + 1
have rw : (a + b) / b = a / b + b / b
Tactic: rw [← div_self h, add_div]
-- Lean 4 proof step from Mathlib.Algebra.Field.Basic (goal)
Goal:
K : Type u_1
inst : DivisionSemiring K
a b : K
h : b ≠ 0
rw : (a + b) / b = a / b + b / b
⊢ (a + b) / b = a / b + 1
have rw₁ : a / b + b / b = a / b + b / b
Tactic: rw [← div_self h, add_div]
-- Lean 4 proof step from Mathlib.Algebra.Field.Basic (goal)
Goal:
K : Type u_1
inst : DivisionSemiring K
c a b : K
hc : c ≠ 0
⊢ (a + b / c) * c = a * c + b
have rw : a * c + b / c * c = a * c + b
Tactic: rw [right_distrib, div_mul_cancel₀ _ hc]
-- Lean 4 proof step from Mathlib.Algebra.Field.Basic (goal)
Goal:
K : Type u_1
inst : DivisionSemiring K
c a b : K
hc : c ≠ 0
rw : a * c + b / c * c = a * c + b
⊢ (a + b / c) * c = a * c + b
have rw₁ : a * c + b = a * c + b
Tactic: rw [right_distrib, div_mul_cancel₀ _ hc]
-- Lean 4 proof step from Mathlib.Algebra.Field.Basic (goal)
Goal:
K : Type u_1
inst : DivisionSemiring K
a b c : K
hc : c ≠ 0
⊢ b + a / c = (b * c + a) / c
have rw : b + a / c = b * c / c + a / c
Tactic: rw [add_div, mul_div_cancel_right₀ _ hc]
-- Lean 4 proof step from Mathlib.Algebra.Field.Basic (goal)
Goal:
K : Type u_1
inst : DivisionSemiring K
a b c : K
hc : c ≠ 0
rw : b + a / c = b * c / c + a / c
⊢ b + a / c = (b * c + a) / c
have rw₁ : b + a / c = b + a / c
Tactic: rw [add_div, mul_div_cancel_right₀ _ hc]
-- Lean 4 proof step from Mathlib.Algebra.Field.Basic (goal)
Goal:
K : Type u_1
inst : DivisionSemiring K
a b c : K
hc : c ≠ 0
⊢ a / c + b = (a + b * c) / c
have rwa : b + a / c = (a + b * c) / c
Tactic: rwa [add_comm, add_div', add_comm]
-- Lean 4 proof step from Mathlib.Algebra.Field.Basic (goal)
Goal:
K : Type u_1
inst : DivisionSemiring K
a b c : K
hc : c ≠ 0
rwa : b + a / c = (a + b * c) / c
⊢ a / c + b = (a + b * c) / c
have rwa₁ : (b * c + a) / c = (a + b * c) / c
Tactic: rwa [add_comm, add_div', add_comm]
-- Lean 4 proof step from Mathlib.Algebra.Field.Basic (goal)
Goal:
K : Type u_1
inst : DivisionSemiring K
a b c : K
hc : c ≠ 0
rwa : b + a / c = (a + b * c) / c
rwa₁ : (b * c + a) / c = (a + b * c) / c
hc₁ : c ≠ 0
⊢ a / c + b = (a + b * c) / c
have rwa₂ : (a + b * c) / c = (a + b * c) / c
Tactic: rwa [add_comm, add_div', add_comm]
-- Lean 4 proof step from Mathlib.Algebra.Field.Basic (goal)
Goal:
K : Type u_1
inst : DivisionSemiring K
a b c d : K
hbc : Commute b c
hbd : Commute b d
hb : b ≠ 0
hd : d ≠ 0
⊢ a / b + c / d = (a * d + b * c) / (b * d)
have rw : a / b + c / d = a * d / (b * d) + b * c / (b * d)
Tactic: rw [add_div, mul_div_mul_right _ b hd, hbc.eq, hbd.eq, mul_div_mul_right c d hb]
-- Lean 4 proof step from Mathlib.Algebra.Field.Basic (goal)
Goal:
K : Type u_1
inst : DivisionSemiring K
a b c d : K
hbc : Commute b c
hbd : Commute b d
hb : b ≠ 0
hd : d ≠ 0
rw : a / b + c / d = a * d / (b * d) + b * c / (b * d)
⊢ a / b + c / d = (a * d + b * c) / (b * d)
have rw₁ : a / b + c / d = a / b + b * c / (b * d)
Tactic: rw [add_div, mul_div_mul_right _ b hd, hbc.eq, hbd.eq, mul_div_mul_right c d hb]
-- Lean 4 proof step from Mathlib.Algebra.Field.Basic (goal)
Goal:
K : Type u_1
inst : DivisionSemiring K
a b c d : K
hbc : Commute b c
hbd : Commute b d
hb : b ≠ 0
hd : d ≠ 0
rw : a / b + c / d = a * d / (b * d) + b * c / (b * d)
rw₁ : a / b + c / d = a / b + b * c / (b * d)
⊢ a / b + c / d = (a * d + b * c) / (b * d)
have rw₂ : a / b + c / d = a / b + c * b / (b * d)
Tactic: rw [add_div, mul_div_mul_right _ b hd, hbc.eq, hbd.eq, mul_div_mul_right c d hb]
-- Lean 4 proof step from Mathlib.Algebra.Field.Basic (goal)
Goal:
K : Type u_1
inst : DivisionSemiring K
a b c d : K
hbc : Commute b c
hbd : Commute b d
hb : b ≠ 0
hd : d ≠ 0
rw : a / b + c / d = a * d / (b * d) + b * c / (b * d)
rw₁ : a / b + c / d = a / b + b * c / (b * d)
rw₂ : a / b + c / d = a / b + c * b / (b * d)
⊢ a / b + c / d = (a * d + b * c) / (b * d)
have rw₃ : a / b + c / d = a / b + c * b / (d * b)
Tactic: rw [add_div, mul_div_mul_right _ b hd, hbc.eq, hbd.eq, mul_div_mul_right c d hb]
-- Lean 4 proof step from Mathlib.Algebra.Field.Basic (goal)
Goal:
K : Type u_1
inst : DivisionSemiring K
a b c d : K
hbc : Commute b c
hbd : Commute b d
hb : b ≠ 0
hd : d ≠ 0
rw : a / b + c / d = a * d / (b * d) + b * c / (b * d)
rw₁ : a / b + c / d = a / b + b * c / (b * d)
rw₂ : a / b + c / d = a / b + c * b / (b * d)
rw₃ : a / b + c / d = a / b + c * b / (d * b)
⊢ a / b + c / d = (a * d + b * c) / (b * d)
have rw₄ : a / b + c / d = a / b + c / d
Tactic: rw [add_div, mul_div_mul_right _ b hd, hbc.eq, hbd.eq, mul_div_mul_right c d hb]
-- Lean 4 proof step from Mathlib.Algebra.Field.Basic (goal)
Goal:
K : Type u_1
inst : DivisionSemiring K
a b : K
hab : Commute a b
ha : a ≠ 0
hb : b ≠ 0
⊢ 1 / a + 1 / b = (a + b) / (a * b)
have rw : (1 * b + a * 1) / (a * b) = (a + b) / (a * b)
Tactic: rw [(Commute.one_right a).div_add_div hab ha hb, one_mul, mul_one, add_comm]
-- Lean 4 proof step from Mathlib.Algebra.Field.Basic (goal)
Goal:
K : Type u_1
inst : DivisionSemiring K
a b : K
hab : Commute a b
ha : a ≠ 0
hb : b ≠ 0
rw : (1 * b + a * 1) / (a * b) = (a + b) / (a * b)
⊢ 1 / a + 1 / b = (a + b) / (a * b)
have rw₁ : (b + a * 1) / (a * b) = (a + b) / (a * b)
Tactic: rw [(Commute.one_right a).div_add_div hab ha hb, one_mul, mul_one, add_comm]
-- Lean 4 proof step from Mathlib.Algebra.Field.Basic (goal)
Goal:
K : Type u_1
inst : DivisionSemiring K
a b : K
hab : Commute a b
ha : a ≠ 0
hb : b ≠ 0
rw : (1 * b + a * 1) / (a * b) = (a + b) / (a * b)
rw₁ : (b + a * 1) / (a * b) = (a + b) / (a * b)
⊢ 1 / a + 1 / b = (a + b) / (a * b)
have rw₂ : (b + a) / (a * b) = (a + b) / (a * b)
Tactic: rw [(Commute.one_right a).div_add_div hab ha hb, one_mul, mul_one, add_comm]
-- Lean 4 proof step from Mathlib.Algebra.Field.Basic (goal)
Goal:
K : Type u_1
inst : DivisionSemiring K
a b : K
hab : Commute a b
ha : a ≠ 0
hb : b ≠ 0
rw : (1 * b + a * 1) / (a * b) = (a + b) / (a * b)
rw₁ : (b + a * 1) / (a * b) = (a + b) / (a * b)
rw₂ : (b + a) / (a * b) = (a + b) / (a * b)
⊢ 1 / a + 1 / b = (a + b) / (a * b)
have rw₃ : (a + b) / (a * b) = (a + b) / (a * b)
Tactic: rw [(Commute.one_right a).div_add_div hab ha hb, one_mul, mul_one, add_comm]
-- Lean 4 proof step from Mathlib.Algebra.Field.Basic (goal)
Goal:
K : Type u_1
inst : DivisionSemiring K
a b : K
hab : Commute a b
ha : a ≠ 0
hb : b ≠ 0
⊢ a⁻¹ + b⁻¹ = (a + b) / (a * b)
have rw : 1 / a + b⁻¹ = (a + b) / (a * b)
Tactic: rw [inv_eq_one_div, inv_eq_one_div, hab.one_div_add_one_div ha hb]
-- Lean 4 proof step from Mathlib.Algebra.Field.Basic (goal)
Goal:
K : Type u_1
inst : DivisionSemiring K
a b : K
hab : Commute a b
ha : a ≠ 0
hb : b ≠ 0
rw : 1 / a + b⁻¹ = (a + b) / (a * b)
⊢ a⁻¹ + b⁻¹ = (a + b) / (a * b)
have rw₁ : 1 / a + 1 / b = (a + b) / (a * b)
Tactic: rw [inv_eq_one_div, inv_eq_one_div, hab.one_div_add_one_div ha hb]
-- Lean 4 proof step from Mathlib.Algebra.Field.Basic (goal)
Goal:
K : Type u_1
inst : DivisionSemiring K
a b : K
hab : Commute a b
ha : a ≠ 0
hb : b ≠ 0
rw : 1 / a + b⁻¹ = (a + b) / (a * b)
rw₁ : 1 / a + 1 / b = (a + b) / (a * b)
⊢ a⁻¹ + b⁻¹ = (a + b) / (a * b)
have rw₂ : (a + b) / (a * b) = (a + b) / (a * b)
Tactic: rw [inv_eq_one_div, inv_eq_one_div, hab.one_div_add_one_div ha hb]
-- Lean 4 proof step from Mathlib.Algebra.Field.Basic (goal)
Goal:
K : Type u_1
inst : DivisionSemiring K
inst_1 : NeZero.{u_1} (R := K) 2
a : K
⊢ (a + a) / 2 = a
have rw : a * 2 / 2 = a
Tactic: rw [← mul_two, mul_div_cancel_right₀ a two_ne_zero]
-- Lean 4 proof step from Mathlib.Algebra.Field.Basic (goal)
Goal:
K : Type u_1
inst : DivisionSemiring K
inst_1 : NeZero.{u_1} (R := K) 2
a : K
rw : a * 2 / 2 = a
⊢ (a + a) / 2 = a
have rw₁ : a = a
Tactic: rw [← mul_two, mul_div_cancel_right₀ a two_ne_zero]
-- Lean 4 proof step from Mathlib.Algebra.Field.Basic (goal)
Goal:
K : Type u_1
inst : DivisionSemiring K
inst_1 : NeZero.{u_1} (R := K) 2
a : K
⊢ a / 2 + a / 2 = a
have rw : (a + a) / 2 = a
Tactic: rw [← add_div, add_self_div_two]
-- Lean 4 proof step from Mathlib.Algebra.Field.Basic (goal)
Goal:
K : Type u_1
inst : DivisionSemiring K
inst_1 : NeZero.{u_1} (R := K) 2
a : K
rw : (a + a) / 2 = a
⊢ a / 2 + a / 2 = a
have rw₁ : a = a
Tactic: rw [← add_div, add_self_div_two]
-- Lean 4 proof step from Mathlib.Algebra.Field.Basic (goal)
Goal:
K : Type u_1
inst : DivisionRing K
a : K
h : a ≠ 0
⊢ a / -a = -1
have rw : -(a / a) = -1
Tactic: rw [div_neg_eq_neg_div, div_self h]
-- Lean 4 proof step from Mathlib.Algebra.Field.Basic (goal)
Goal:
K : Type u_1
inst : DivisionRing K
a : K
h : a ≠ 0
rw : -(a / a) = -1
⊢ a / -a = -1
have rw₁ : Eq.{u_1 + 1} (α := K) (-1) (-1)
Tactic: rw [div_neg_eq_neg_div, div_self h]
-- Lean 4 proof step from Mathlib.Algebra.Field.Basic (goal)
Goal:
K : Type u_1
inst : DivisionRing K
a : K
h : a ≠ 0
⊢ -a / a = -1
have rw : -(a / a) = -1
Tactic: rw [neg_div, div_self h]