awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Exact (goal)
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_8, u_9, u_10} (M := M₁) (N := M₂) (P := M₃) (⇑f : (a : M₁) → M₂) (⇑g : (a : M₂) → M₃)
x₂ : M₂
hx₂ : Eq.{u_13 + 1} (α := N₃) ((g' : (a : N₂) → N₃) ((τ₂ : (a : M₂) → N₂) x₂ : N₂) : N₃) (1 : N₃)
⊢ Membership.mem.{u_12, u_12} (α := N₂) (γ := Set N₂) (Set.range.{u_12, u_11 + 1} (ι := N₁) (⇑f' : (a : N₁) → N₂))
    ((τ₂ : (a : M₂) → N₂) x₂ : N₂)
have mp : ∀ (x₁ : M₁)
  (hx₂ :
    Eq.{u_13 + 1} (α := N₃) ((g' : (a : N₂) → N₃) ((τ₂ : (a : M₂) → N₂) ((f : (a : M₁) → M₂) x₁ : M₂) : N₂) : N₃)
      (1 : N₃)),
  Membership.mem.{u_12, u_12} (α := N₂) (γ := Set N₂) (Set.range.{u_12, u_11 + 1} (ι := N₁) (⇑f' : (a : N₁) → N₂))
    ((τ₂ : (a : M₂) → N₂) ((f : (a : M₁) → M₂) x₁ : M₂) : N₂)
Tactic: obtain ⟨x₁, rfl⟩ := (h x₂).1 (h₃ (by simpa only [map_one, comm₂₃] using hx₂))
Cleared hypotheses: x₂, hx₂
-- Lean 4 proof step from Mathlib.Algebra.Exact (goal)
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_8, u_9, u_10} (M := M₁) (N := M₂) (P := M₃) (⇑f : (a : M₁) → M₂) (⇑g : (a : M₂) → M₃)
x₂ : M₂
y₁ : N₁
hy₁ : Eq.{u_12 + 1} (α := N₂) ((f' : (a : N₁) → N₂) y₁ : N₂) ((τ₂ : (a : M₂) → N₂) x₂ : N₂)
⊢ Eq.{u_13 + 1} (α := N₃) ((g' : (a : N₂) → N₃) ((τ₂ : (a : M₂) → N₂) x₂ : N₂) : N₃) (1 : N₃)
have mp : ∀ (x₁ : M₁)
  (hy₁ :
    Eq.{u_12 + 1} (α := N₂) ((f' : (a : N₁) → N₂) ((τ₁ : (a : M₁) → N₁) x₁ : N₁) : N₂) ((τ₂ : (a : M₂) → N₂) x₂ : N₂)),
  Eq.{u_13 + 1} (α := N₃) ((g' : (a : N₂) → N₃) ((τ₂ : (a : M₂) → N₂) x₂ : N₂) : N₃) (1 : N₃)
Tactic: obtain ⟨x₁, rfl⟩ := h₁ y₁
Cleared hypotheses: y₁, hy₁
-- Lean 4 proof step from Mathlib.Algebra.Exact (goal)
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_8, u_9, u_10} (M := M₁) (N := M₂) (P := M₃) (⇑f : (a : M₁) → M₂) (⇑g : (a : M₂) → M₃)
x₂ : M₂
x₁ : M₁
hy₁ : Eq.{u_12 + 1} (α := N₂) ((f' : (a : N₁) → N₂) ((τ₁ : (a : M₁) → N₁) x₁ : N₁) : N₂) ((τ₂ : (a : M₂) → N₂) x₂ : N₂)
⊢ Eq.{u_13 + 1} (α := N₃) ((g' : (a : N₂) → N₃) ((τ₂ : (a : M₂) → N₂) x₂ : N₂) : N₃) (1 : N₃)
have rw : Membership.mem (γ := Set M₂) (Set.range.{u_9, u_8 + 1} (ι := M₁) (⇑f : (a : M₁) → M₂)) x₂
Tactic: rw [comm₂₃, (h x₂).2 _, map_one]
-- Lean 4 proof step from Mathlib.Algebra.Exact (goal)
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_10 + 1} (α := M₃) ((g : (a : M₂) → M₃) x₂ : M₃) (1 : M₃) ↔
    Membership.mem (γ := Set M₂) (Set.range.{u_9, u_8 + 1} (ι := M₁) (⇑f : (a : M₁) → M₂)) x₂
have mpr : Eq.{u_10 + 1} (α := M₃) ((g : (a : M₂) → M₃) x₂ : M₃) (1 : M₃) →
  Membership.mem (γ := Set M₂) (Set.range.{u_9, u_8 + 1} (ι := M₁) (⇑f : (a : M₁) → M₂)) x₂
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Exact (goal)
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₂
mpr :
  Eq.{u_10 + 1} (α := M₃) ((g : (a : M₂) → M₃) x₂ : M₃) (1 : M₃) →
    Membership.mem (γ := Set M₂) (Set.range.{u_9, u_8 + 1} (ι := M₁) (⇑f : (a : M₁) → M₂)) x₂
⊢ Eq.{u_10 + 1} (α := M₃) ((g : (a : M₂) → M₃) x₂ : M₃) (1 : M₃) ↔
    Membership.mem (γ := Set M₂) (Set.range.{u_9, u_8 + 1} (ι := M₁) (⇑f : (a : M₁) → M₂)) x₂
have mpr₁ : Membership.mem (γ := Set M₂) (Set.range.{u_9, u_8 + 1} (ι := M₁) (⇑f : (a : M₁) → M₂)) x₂ →
  Eq.{u_10 + 1} (α := M₃) ((g : (a : M₂) → M₃) x₂ : M₃) (1 : M₃)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Exact (goal)
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₂
hx₂ : Eq.{u_10 + 1} (α := M₃) ((g : (a : M₂) → M₃) x₂ : M₃) (1 : M₃)
⊢ Membership.mem (γ := Set M₂) (Set.range.{u_9, u_8 + 1} (ι := M₁) (⇑f : (a : M₁) → M₂)) x₂
have mpr : ∀ (y₁ : N₁) (hy₁ : Eq.{u_12 + 1} (α := N₂) ((f' : (a : N₁) → N₂) y₁ : N₂) ((τ₂ : (a : M₂) → N₂) x₂ : N₂)),
  Membership.mem (γ := Set M₂) (Set.range.{u_9, u_8 + 1} (ι := M₁) (⇑f : (a : M₁) → M₂)) x₂
Tactic: obtain ⟨y₁, hy₁⟩ := (h (τ₂ x₂)).1 (by simp only [comm₂₃, hx₂, map_one])
-- Lean 4 proof step from Mathlib.Algebra.Exact (goal)
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₂
hx₂ : Eq.{u_10 + 1} (α := M₃) ((g : (a : M₂) → M₃) x₂ : M₃) (1 : M₃)
y₁ : N₁
hy₁ : Eq.{u_12 + 1} (α := N₂) ((f' : (a : N₁) → N₂) y₁ : N₂) ((τ₂ : (a : M₂) → N₂) x₂ : N₂)
⊢ Membership.mem (γ := Set M₂) (Set.range.{u_9, u_8 + 1} (ι := M₁) (⇑f : (a : M₁) → M₂)) x₂
have mpr : ∀ (x₁ : M₁)
  (hy₁ :
    Eq.{u_12 + 1} (α := N₂) ((f' : (a : N₁) → N₂) ((τ₁ : (a : M₁) → N₁) x₁ : N₁) : N₂) ((τ₂ : (a : M₂) → N₂) x₂ : N₂)),
  Membership.mem (γ := Set M₂) (Set.range.{u_9, u_8 + 1} (ι := M₁) (⇑f : (a : M₁) → M₂)) x₂
Tactic: obtain ⟨x₁, rfl⟩ := h₁ y₁
Cleared hypotheses: y₁, hy₁
-- Lean 4 proof step from Mathlib.Algebra.Exact (goal)
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_10 + 1} (α := M₃) ((g : (a : M₂) → M₃) ((f : (a : M₁) → M₂) x₁ : M₂) : M₃) (1 : M₃)
have mpr : 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: apply h₃
-- Lean 4 proof step from Mathlib.Algebra.Exact (goal)
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
⊢ Exact (M := ↥Q) (N := N) (P := N ⧸ Q) (⇑Q.subtype : (a : ↥Q) → N) (⇑Q.mkQ : (a : N) → N ⧸ Q)
have rw : Q.mkQ.ker = Q.subtype.range
Tactic: rw [exact_iff, Submodule.ker_mkQ, Submodule.range_subtype Q]
-- Lean 4 proof step from Mathlib.Algebra.Exact (goal)
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
⊢ Exact (M := ↥Q) (N := N) (P := N ⧸ Q) (⇑Q.subtype : (a : ↥Q) → N) (⇑Q.mkQ : (a : N) → N ⧸ Q)
have rw₁ : Q = Q.subtype.range
Tactic: rw [exact_iff, Submodule.ker_mkQ, Submodule.range_subtype Q]
-- Lean 4 proof step from Mathlib.Algebra.Exact (goal)
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
⊢ Exact (M := ↥Q) (N := N) (P := N ⧸ Q) (⇑Q.subtype : (a : ↥Q) → N) (⇑Q.mkQ : (a : N) → N ⧸ Q)
have rw₂ : Q = Q
Tactic: rw [exact_iff, Submodule.ker_mkQ, Submodule.range_subtype Q]
-- Lean 4 proof step from Mathlib.Algebra.Exact (goal)
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 : 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)
have simp_rw : Submodule.map (↑e : N →ₗ[R] N') g.ker = Submodule.map (↑e : N →ₗ[R] N') f.range ↔ g.ker = f.range
Tactic: simp_rw [LinearMap.exact_iff, LinearMap.ker_comp, ← Submodule.map_equiv_eq_comap_symm,
    LinearMap.range_comp]
-- Lean 4 proof step from Mathlib.Algebra.Exact (goal)
Goal:
R : Type u_1
M : Type u_2
M' : Type u_3
N : Type u_4
N' : Type u_5
P : Type u_6
P' : Type u_7
inst : Semiring R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : AddCommGroup P
inst_4 : Module R M
inst_5 : Module R N
inst_6 : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
h : Exact.{u_2, u_4, u_6} (M := M) (N := N) (P := P) (⇑f : (a : M) → N) (⇑g : (a : N) → P)
hf : Injective.{u_2 + 1, u_4 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
⊢ { l : 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) }
have 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)
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 := ?_ }
-- Lean 4 proof step from Mathlib.Algebra.Exact (goal)
Goal:
R : Type u_1
M : Type u_2
M' : Type u_3
N : Type u_4
N' : Type u_5
P : Type u_6
P' : Type u_7
inst : Semiring R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : AddCommGroup P
inst_4 : Module R M
inst_5 : Module R N
inst_6 : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
h : Exact.{u_2, u_4, u_6} (M := M) (N := N) (P := P) (⇑f : (a : M) → N) (⇑g : (a : N) → P)
hf : Injective.{u_2 + 1, u_4 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
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)
⊢ { 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) }
have 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) sorry))) :
          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) sorry)) :
          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 := ?_ }
-- Lean 4 proof step from Mathlib.Algebra.Exact (goal)
Goal:
R : Type u_1
M : Type u_2
M' : Type u_3
N : Type u_4
N' : Type u_5
P : Type u_6
P' : Type u_7
inst : Semiring R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : AddCommGroup P
inst_4 : Module R M
inst_5 : Module R N
inst_6 : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
h : Exact.{u_2, u_4, u_6} (M := M) (N := N) (P := P) (⇑f : (a : M) → N) (⇑g : (a : N) → P)
hf : Injective.{u_2 + 1, u_4 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
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)
⊢ { 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) }
have 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
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 := ?_ }
-- Lean 4 proof step from Mathlib.Algebra.Exact (goal)
Goal:
R : Type u_1
M : Type u_2
M' : Type u_3
N : Type u_4
N' : Type u_5
P : Type u_6
P' : Type u_7
inst : Semiring R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : AddCommGroup P
inst_4 : Module R M
inst_5 : Module R N
inst_6 : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
h : Exact.{u_2, u_4, u_6} (M := M) (N := N) (P := P) (⇑f : (a : M) → N) (⇑g : (a : N) → P)
hf : Injective.{u_2 + 1, u_4 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
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
⊢ { 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) }
have 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) sorry)
  fun (l : { l : P →ₗ[R] N // g ∘ₗ l = LinearMap.id }) ↦
  Subtype.mk (p := fun (e : N ≃ₗ[R] M × P) ↦
    f = (↑e.symm : M × P →ₗ[R] N) ∘ₗ inl R M P ∧ g = snd R M P ∘ₗ (↑e : N →ₗ[R] M × P))
    (LinearEquiv.symm (LinearEquiv.ofBijective (f ∘ₗ fst R M P + (↑l : P →ₗ[R] N) ∘ₗ snd R M P) sorry)) sorry
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 := ?_ }
-- Lean 4 proof step from Mathlib.Algebra.Exact (goal)
Goal:
R : Type u_1
M : Type u_2
M' : Type u_3
N : Type u_4
N' : Type u_5
P : Type u_6
P' : Type u_7
inst : Semiring R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : AddCommGroup P
inst_4 : Module R M
inst_5 : Module R N
inst_6 : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
h : Exact.{u_2, u_4, u_6} (M := M) (N := N) (P := P) (⇑f : (a : M) → N) (⇑g : (a : N) → P)
hf : Injective.{u_2 + 1, u_4 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
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) ⋯)) ⋯
⊢ { 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) }
have 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) sorry)
  fun (l : { l : P →ₗ[R] N // g ∘ₗ l = LinearMap.id }) ↦
  Subtype.mk (p := fun (e : N ≃ₗ[R] M × P) ↦
    f = (↑e.symm : M × P →ₗ[R] N) ∘ₗ inl R M P ∧ g = snd R M P ∘ₗ (↑e : N →ₗ[R] M × P))
    (LinearEquiv.symm (LinearEquiv.ofBijective (f ∘ₗ fst R M P + (↑l : P →ₗ[R] N) ∘ₗ snd R M P) sorry)) sorry
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 := ?_ }
-- Lean 4 proof step from Mathlib.Algebra.Exact (hypothesis)
Goal:
R : Type u_1
M : Type u_2
M' : Type u_3
N : Type u_4
N' : Type u_5
P : Type u_6
P' : Type u_7
inst : Semiring R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : AddCommGroup P
inst_4 : Module R M
inst_5 : Module R N
inst_6 : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
h : Exact.{u_2, u_4, u_6} (M := M) (N := N) (P := P) (⇑f : (a : M) → N) (⇑g : (a : N) → P)
hf : Injective.{u_2 + 1, u_4 + 1} (α := M) (β := N) (⇑f : (a : M) → N)
l : { l : P →ₗ[R] N // g ∘ₗ l = LinearMap.id }
⊢ Bijective (α := M × P) (β := N) (⇑(f ∘ₗ fst R M P + (↑l : P →ₗ[R] N) ∘ₗ snd R M P) : (a : M × P) → N)
have h₁ : ∀ (x : P), (g : (a : N) → P) (((↑l : P →ₗ[R] N) : (a : P) → N) x : N) = x
Tactic: have h₁ : ∀ x, g (l.1 x) = x := LinearMap.congr_fun l.2