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

Tactic:
constructor
-- Module: Mathlib.Algebra.Exact
Goal:
M₁ : Type u_8
M₂ : Type u_9
M₃ : Type u_10
N₁ : Type u_11
N₂ : Type u_12
N₃ : Type u_13
inst : CommMonoid M₁
inst_1 : CommMonoid M₂
inst_2 : CommMonoid M₃
inst_3 : CommMonoid N₁
inst_4 : CommMonoid N₂
inst_5 : CommMonoid N₃
f : M₁ →* M₂
g : M₂ →* M₃
f' : N₁ →* N₂
g' : N₂ →* N₃
τ₁ : M₁ →* N₁
τ₂ : M₂ →* N₂
τ₃ : M₃ →* N₃
h₁ : Surjective.{u_8 + 1, u_11 + 1} (α := M₁) (β := N₁) (⇑τ₁ : (a : M₁) → N₁)
h₂ : Bijective.{u_9 + 1, u_12 + 1} (α := M₂) (β := N₂) (⇑τ₂ : (a : M₂) → N₂)
h₃ : Injective.{u_10 + 1, u_13 + 1} (α := M₃) (β := N₃) (⇑τ₃ : (a : M₃) → N₃)
comm₁₂ :
  ∀ (x : M₁),
    Eq.{u_12 + 1} (α := N₂) ((f' : (a : N₁) → N₂) ((τ₁ : (a : M₁) → N₁) x : N₁) : N₂)
      ((τ₂ : (a : M₂) → N₂) ((f : (a : M₁) → M₂) x : M₂) : N₂)
comm₂₃ :
  ∀ (x : M₂),
    Eq.{u_13 + 1} (α := N₃) ((g' : (a : N₂) → N₃) ((τ₂ : (a : M₂) → N₂) x : N₂) : N₃)
      ((τ₃ : (a : M₃) → N₃) ((g : (a : M₂) → M₃) x : M₃) : N₃)
h : MulExact.{u_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₃)
⊢ Eq.{u_13 + 1} (α := N₃) ((τ₃ : (a : M₃) → N₃) ((g : (a : M₂) → M₃) x₂ : M₃) : N₃) ((τ₃ : (a : M₃) → N₃) 1 : N₃)

Tactic:
simpa only [map_one, comm₂₃] using hx₂

Premises used: map_one
-- Module: Mathlib.Algebra.Exact
Goal:
M₁ : Type u_8
M₂ : Type u_9
M₃ : Type u_10
N₁ : Type u_11
N₂ : Type u_12
N₃ : Type u_13
inst : CommMonoid M₁
inst_1 : CommMonoid M₂
inst_2 : CommMonoid M₃
inst_3 : CommMonoid N₁
inst_4 : CommMonoid N₂
inst_5 : CommMonoid N₃
f : M₁ →* M₂
g : M₂ →* M₃
f' : N₁ →* N₂
g' : N₂ →* N₃
τ₁ : M₁ →* N₁
τ₂ : M₂ →* N₂
τ₃ : M₃ →* N₃
h₁ : Surjective.{u_8 + 1, u_11 + 1} (α := M₁) (β := N₁) (⇑τ₁ : (a : M₁) → N₁)
h₂ : Bijective.{u_9 + 1, u_12 + 1} (α := M₂) (β := N₂) (⇑τ₂ : (a : M₂) → N₂)
h₃ : Injective.{u_10 + 1, u_13 + 1} (α := M₃) (β := N₃) (⇑τ₃ : (a : M₃) → N₃)
comm₁₂ :
  ∀ (x : M₁),
    Eq.{u_12 + 1} (α := N₂) ((f' : (a : N₁) → N₂) ((τ₁ : (a : M₁) → N₁) x : N₁) : N₂)
      ((τ₂ : (a : M₂) → N₂) ((f : (a : M₁) → M₂) x : M₂) : N₂)
comm₂₃ :
  ∀ (x : M₂),
    Eq.{u_13 + 1} (α := N₃) ((g' : (a : N₂) → N₃) ((τ₂ : (a : M₂) → N₂) x : N₂) : N₃)
      ((τ₃ : (a : M₃) → N₃) ((g : (a : M₂) → M₃) x : M₃) : N₃)
h : MulExact.{u_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₃)
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₂)
⊢ 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₂)

Tactic:
obtain ⟨x₁, rfl⟩ := (h x₂).1 (h₃ (by simpa only [map_one, comm₂₃] using hx₂))

Premises used: Iff.mp, rfl
-- Module: Mathlib.Algebra.Exact
Goal:
M₁ : Type u_8
M₂ : Type u_9
M₃ : Type u_10
N₁ : Type u_11
N₂ : Type u_12
N₃ : Type u_13
inst : CommMonoid M₁
inst_1 : CommMonoid M₂
inst_2 : CommMonoid M₃
inst_3 : CommMonoid N₁
inst_4 : CommMonoid N₂
inst_5 : CommMonoid N₃
f : M₁ →* M₂
g : M₂ →* M₃
f' : N₁ →* N₂
g' : N₂ →* N₃
τ₁ : M₁ →* N₁
τ₂ : M₂ →* N₂
τ₃ : M₃ →* N₃
h₁ : Surjective.{u_8 + 1, u_11 + 1} (α := M₁) (β := N₁) (⇑τ₁ : (a : M₁) → N₁)
h₂ : Bijective.{u_9 + 1, u_12 + 1} (α := M₂) (β := N₂) (⇑τ₂ : (a : M₂) → N₂)
h₃ : Injective.{u_10 + 1, u_13 + 1} (α := M₃) (β := N₃) (⇑τ₃ : (a : M₃) → N₃)
comm₁₂ :
  ∀ (x : M₁),
    Eq.{u_12 + 1} (α := N₂) ((f' : (a : N₁) → N₂) ((τ₁ : (a : M₁) → N₁) x : N₁) : N₂)
      ((τ₂ : (a : M₂) → N₂) ((f : (a : M₁) → M₂) x : M₂) : N₂)
comm₂₃ :
  ∀ (x : M₂),
    Eq.{u_13 + 1} (α := N₃) ((g' : (a : N₂) → N₃) ((τ₂ : (a : M₂) → N₂) x : N₂) : N₃)
      ((τ₃ : (a : M₃) → N₃) ((g : (a : M₂) → M₃) x : M₃) : N₃)
h : MulExact.{u_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₂) ((f : (a : M₁) → M₂) x₁ : M₂) : N₂) : N₃) (1 : N₃)
⊢ 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₂)

Tactic:
simp only [comm₁₂]
-- Module: Mathlib.Algebra.Exact
Goal:
M₁ : Type u_8
M₂ : Type u_9
M₃ : Type u_10
N₁ : Type u_11
N₂ : Type u_12
N₃ : Type u_13
inst : CommMonoid M₁
inst_1 : CommMonoid M₂
inst_2 : CommMonoid M₃
inst_3 : CommMonoid N₁
inst_4 : CommMonoid N₂
inst_5 : CommMonoid N₃
f : M₁ →* M₂
g : M₂ →* M₃
f' : N₁ →* N₂
g' : N₂ →* N₃
τ₁ : M₁ →* N₁
τ₂ : M₂ →* N₂
τ₃ : M₃ →* N₃
h₁ : Surjective.{u_8 + 1, u_11 + 1} (α := M₁) (β := N₁) (⇑τ₁ : (a : M₁) → N₁)
h₂ : Bijective.{u_9 + 1, u_12 + 1} (α := M₂) (β := N₂) (⇑τ₂ : (a : M₂) → N₂)
h₃ : Injective.{u_10 + 1, u_13 + 1} (α := M₃) (β := N₃) (⇑τ₃ : (a : M₃) → N₃)
comm₁₂ :
  ∀ (x : M₁),
    Eq.{u_12 + 1} (α := N₂) ((f' : (a : N₁) → N₂) ((τ₁ : (a : M₁) → N₁) x : N₁) : N₂)
      ((τ₂ : (a : M₂) → N₂) ((f : (a : M₁) → M₂) x : M₂) : N₂)
comm₂₃ :
  ∀ (x : M₂),
    Eq.{u_13 + 1} (α := N₃) ((g' : (a : N₂) → N₃) ((τ₂ : (a : M₂) → N₂) x : N₂) : N₃)
      ((τ₃ : (a : M₃) → N₃) ((g : (a : M₂) → M₃) x : M₃) : N₃)
h : MulExact.{u_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₂) ((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:
exact ⟨τ₁ x₁, by simp only [comm₁₂]⟩
-- Module: Mathlib.Algebra.Exact
Goal:
M₁ : Type u_8
M₂ : Type u_9
M₃ : Type u_10
N₁ : Type u_11
N₂ : Type u_12
N₃ : Type u_13
inst : CommMonoid M₁
inst_1 : CommMonoid M₂
inst_2 : CommMonoid M₃
inst_3 : CommMonoid N₁
inst_4 : CommMonoid N₂
inst_5 : CommMonoid N₃
f : M₁ →* M₂
g : M₂ →* M₃
f' : N₁ →* N₂
g' : N₂ →* N₃
τ₁ : M₁ →* N₁
τ₂ : M₂ →* N₂
τ₃ : M₃ →* N₃
h₁ : Surjective.{u_8 + 1, u_11 + 1} (α := M₁) (β := N₁) (⇑τ₁ : (a : M₁) → N₁)
h₂ : Bijective.{u_9 + 1, u_12 + 1} (α := M₂) (β := N₂) (⇑τ₂ : (a : M₂) → N₂)
h₃ : Injective.{u_10 + 1, u_13 + 1} (α := M₃) (β := N₃) (⇑τ₃ : (a : M₃) → N₃)
comm₁₂ :
  ∀ (x : M₁),
    Eq.{u_12 + 1} (α := N₂) ((f' : (a : N₁) → N₂) ((τ₁ : (a : M₁) → N₁) x : N₁) : N₂)
      ((τ₂ : (a : M₂) → N₂) ((f : (a : M₁) → M₂) x : M₂) : N₂)
comm₂₃ :
  ∀ (x : M₂),
    Eq.{u_13 + 1} (α := N₃) ((g' : (a : N₂) → N₃) ((τ₂ : (a : M₂) → N₂) x : N₂) : N₃)
      ((τ₃ : (a : M₃) → N₃) ((g : (a : M₂) → M₃) x : M₃) : N₃)
h : MulExact.{u_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₂)
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₃)
⊢ Eq.{u_13 + 1} (α := N₃) ((g' : (a : N₂) → N₃) ((τ₂ : (a : M₂) → N₂) x₂ : N₂) : N₃) (1 : N₃)

Tactic:
obtain ⟨x₁, rfl⟩ := h₁ y₁

Premises used: rfl
-- Module: Mathlib.Algebra.Exact
Goal:
M₁ : Type u_8
M₂ : Type u_9
M₃ : Type u_10
N₁ : Type u_11
N₂ : Type u_12
N₃ : Type u_13
inst : CommMonoid M₁
inst_1 : CommMonoid M₂
inst_2 : CommMonoid M₃
inst_3 : CommMonoid N₁
inst_4 : CommMonoid N₂
inst_5 : CommMonoid N₃
f : M₁ →* M₂
g : M₂ →* M₃
f' : N₁ →* N₂
g' : N₂ →* N₃
τ₁ : M₁ →* N₁
τ₂ : M₂ →* N₂
τ₃ : M₃ →* N₃
h₁ : Surjective.{u_8 + 1, u_11 + 1} (α := M₁) (β := N₁) (⇑τ₁ : (a : M₁) → N₁)
h₂ : Bijective.{u_9 + 1, u_12 + 1} (α := M₂) (β := N₂) (⇑τ₂ : (a : M₂) → N₂)
h₃ : Injective.{u_10 + 1, u_13 + 1} (α := M₃) (β := N₃) (⇑τ₃ : (a : M₃) → N₃)
comm₁₂ :
  ∀ (x : M₁),
    Eq.{u_12 + 1} (α := N₂) ((f' : (a : N₁) → N₂) ((τ₁ : (a : M₁) → N₁) x : N₁) : N₂)
      ((τ₂ : (a : M₂) → N₂) ((f : (a : M₁) → M₂) x : M₂) : N₂)
comm₂₃ :
  ∀ (x : M₂),
    Eq.{u_13 + 1} (α := N₃) ((g' : (a : N₂) → N₃) ((τ₂ : (a : M₂) → N₂) x : N₂) : N₃)
      ((τ₃ : (a : M₃) → N₃) ((g : (a : M₂) → M₃) x : M₃) : N₃)
h : MulExact.{u_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₂)
rw : Membership.mem (γ := Set M₂) (Set.range.{u_9, u_8 + 1} (ι := M₁) (⇑f : (a : M₁) → M₂)) x₂
⊢ Eq.{u_13 + 1} (α := N₃) ((g' : (a : N₂) → N₃) ((τ₂ : (a : M₂) → N₂) x₂ : N₂) : N₃) (1 : N₃)

Tactic:
rw [comm₂₃, (h x₂).2 _, map_one]

Premises used: Iff.mpr, map_one
-- Module: Mathlib.Algebra.Exact
Goal:
M₁ : Type u_8
M₂ : Type u_9
M₃ : Type u_10
N₁ : Type u_11
N₂ : Type u_12
N₃ : Type u_13
inst : CommMonoid M₁
inst_1 : CommMonoid M₂
inst_2 : CommMonoid M₃
inst_3 : CommMonoid N₁
inst_4 : CommMonoid N₂
inst_5 : CommMonoid N₃
f : M₁ →* M₂
g : M₂ →* M₃
f' : N₁ →* N₂
g' : N₂ →* N₃
τ₁ : M₁ →* N₁
τ₂ : M₂ →* N₂
τ₃ : M₃ →* N₃
h₁ : Surjective.{u_8 + 1, u_11 + 1} (α := M₁) (β := N₁) (⇑τ₁ : (a : M₁) → N₁)
h₂ : Bijective.{u_9 + 1, u_12 + 1} (α := M₂) (β := N₂) (⇑τ₂ : (a : M₂) → N₂)
h₃ : Injective.{u_10 + 1, u_13 + 1} (α := M₃) (β := N₃) (⇑τ₃ : (a : M₃) → N₃)
comm₁₂ :
  ∀ (x : M₁),
    Eq.{u_12 + 1} (α := N₂) ((f' : (a : N₁) → N₂) ((τ₁ : (a : M₁) → N₁) x : N₁) : N₂)
      ((τ₂ : (a : M₂) → N₂) ((f : (a : M₁) → M₂) x : M₂) : N₂)
comm₂₃ :
  ∀ (x : M₂),
    Eq.{u_13 + 1} (α := N₃) ((g' : (a : N₂) → N₃) ((τ₂ : (a : M₂) → N₂) x : N₂) : N₃)
      ((τ₃ : (a : M₃) → N₃) ((g : (a : M₂) → M₃) x : M₃) : N₃)
h : MulExact.{u_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_12 + 1} (α := N₂) ((τ₂ : (a : M₂) → N₂) ((f : (a : M₁) → M₂) x₁ : M₂) : N₂) ((τ₂ : (a : M₂) → N₂) x₂ : N₂)

Tactic:
simpa only [comm₁₂] using hy₁
-- Module: Mathlib.Algebra.Exact
Goal:
M₁ : Type u_8
M₂ : Type u_9
M₃ : Type u_10
N₁ : Type u_11
N₂ : Type u_12
N₃ : Type u_13
inst : CommMonoid M₁
inst_1 : CommMonoid M₂
inst_2 : CommMonoid M₃
inst_3 : CommMonoid N₁
inst_4 : CommMonoid N₂
inst_5 : CommMonoid N₃
f : M₁ →* M₂
g : M₂ →* M₃
f' : N₁ →* N₂
g' : N₂ →* N₃
τ₁ : M₁ →* N₁
τ₂ : M₂ →* N₂
τ₃ : M₃ →* N₃
h₁ : Surjective.{u_8 + 1, u_11 + 1} (α := M₁) (β := N₁) (⇑τ₁ : (a : M₁) → N₁)
h₂ : Bijective.{u_9 + 1, u_12 + 1} (α := M₂) (β := N₂) (⇑τ₂ : (a : M₂) → N₂)
h₃ : Injective.{u_10 + 1, u_13 + 1} (α := M₃) (β := N₃) (⇑τ₃ : (a : M₃) → N₃)
comm₁₂ :
  ∀ (x : M₁),
    Eq.{u_12 + 1} (α := N₂) ((f' : (a : N₁) → N₂) ((τ₁ : (a : M₁) → N₁) x : N₁) : N₂)
      ((τ₂ : (a : M₂) → N₂) ((f : (a : M₁) → M₂) x : M₂) : N₂)
comm₂₃ :
  ∀ (x : M₂),
    Eq.{u_13 + 1} (α := N₃) ((g' : (a : N₂) → N₃) ((τ₂ : (a : M₂) → N₂) x : N₂) : N₃)
      ((τ₃ : (a : M₃) → N₃) ((g : (a : M₂) → M₃) x : M₃) : N₃)
h : MulExact.{u_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₂)
⊢ Membership.mem (γ := Set M₂) (Set.range.{u_9, u_8 + 1} (ι := M₁) (⇑f : (a : M₁) → M₂)) x₂

Tactic:
exact ⟨x₁, h₂.1 (by simpa only [comm₁₂] using hy₁)⟩
-- Module: Mathlib.Algebra.Exact
Goal:
M₁ : Type u_8
M₂ : Type u_9
M₃ : Type u_10
N₁ : Type u_11
N₂ : Type u_12
N₃ : Type u_13
inst : CommMonoid M₁
inst_1 : CommMonoid M₂
inst_2 : CommMonoid M₃
inst_3 : CommMonoid N₁
inst_4 : CommMonoid N₂
inst_5 : CommMonoid N₃
f : M₁ →* M₂
g : M₂ →* M₃
f' : N₁ →* N₂
g' : N₂ →* N₃
τ₁ : M₁ →* N₁
τ₂ : M₂ →* N₂
τ₃ : M₃ →* N₃
h₁ : Surjective.{u_8 + 1, u_11 + 1} (α := M₁) (β := N₁) (⇑τ₁ : (a : M₁) → N₁)
h₂ : Bijective.{u_9 + 1, u_12 + 1} (α := M₂) (β := N₂) (⇑τ₂ : (a : M₂) → N₂)
h₃ : Injective.{u_10 + 1, u_13 + 1} (α := M₃) (β := N₃) (⇑τ₃ : (a : M₃) → N₃)
comm₁₂ :
  ∀ (x : M₁),
    Eq.{u_12 + 1} (α := N₂) ((f' : (a : N₁) → N₂) ((τ₁ : (a : M₁) → N₁) x : N₁) : N₂)
      ((τ₂ : (a : M₂) → N₂) ((f : (a : M₁) → M₂) x : M₂) : N₂)
comm₂₃ :
  ∀ (x : M₂),
    Eq.{u_13 + 1} (α := N₃) ((g' : (a : N₂) → N₃) ((τ₂ : (a : M₂) → N₂) x : N₂) : N₃)
      ((τ₃ : (a : M₃) → N₃) ((g : (a : M₂) → M₃) x : M₃) : N₃)
h : MulExact.{u_11, u_12, u_13} (M := N₁) (N := N₂) (P := N₃) (⇑f' : (a : N₁) → N₂) (⇑g' : (a : N₂) → N₃)
x₂ : M₂
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₂
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₃)
⊢ 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
-- Module: Mathlib.Algebra.Exact
Goal:
M₁ : Type u_8
M₂ : Type u_9
M₃ : Type u_10
N₁ : Type u_11
N₂ : Type u_12
N₃ : Type u_13
inst : CommMonoid M₁
inst_1 : CommMonoid M₂
inst_2 : CommMonoid M₃
inst_3 : CommMonoid N₁
inst_4 : CommMonoid N₂
inst_5 : CommMonoid N₃
f : M₁ →* M₂
g : M₂ →* M₃
f' : N₁ →* N₂
g' : N₂ →* N₃
τ₁ : M₁ →* N₁
τ₂ : M₂ →* N₂
τ₃ : M₃ →* N₃
h₁ : Surjective.{u_8 + 1, u_11 + 1} (α := M₁) (β := N₁) (⇑τ₁ : (a : M₁) → N₁)
h₂ : Bijective.{u_9 + 1, u_12 + 1} (α := M₂) (β := N₂) (⇑τ₂ : (a : M₂) → N₂)
h₃ : Injective.{u_10 + 1, u_13 + 1} (α := M₃) (β := N₃) (⇑τ₃ : (a : M₃) → N₃)
comm₁₂ :
  ∀ (x : M₁),
    Eq.{u_12 + 1} (α := N₂) ((f' : (a : N₁) → N₂) ((τ₁ : (a : M₁) → N₁) x : N₁) : N₂)
      ((τ₂ : (a : M₂) → N₂) ((f : (a : M₁) → M₂) x : M₂) : N₂)
comm₂₃ :
  ∀ (x : M₂),
    Eq.{u_13 + 1} (α := N₃) ((g' : (a : N₂) → N₃) ((τ₂ : (a : M₂) → N₂) x : N₂) : N₃)
      ((τ₃ : (a : M₃) → N₃) ((g : (a : M₂) → M₃) x : M₃) : N₃)
h : MulExact.{u_11, u_12, u_13} (M := N₁) (N := N₂) (P := N₃) (⇑f' : (a : N₁) → N₂) (⇑g' : (a : N₂) → N₃)
x₂ : M₂
hx₂ : Eq.{u_10 + 1} (α := M₃) ((g : (a : M₂) → M₃) x₂ : M₃) (1 : M₃)
⊢ Eq.{u_13 + 1} (α := N₃) ((g' : (a : N₂) → N₃) ((τ₂ : (a : M₂) → N₂) x₂ : N₂) : N₃) (1 : N₃)

Tactic:
simp only [comm₂₃, hx₂, map_one]

Premises used: map_one
-- Module: Mathlib.Algebra.Exact
Goal:
M₁ : Type u_8
M₂ : Type u_9
M₃ : Type u_10
N₁ : Type u_11
N₂ : Type u_12
N₃ : Type u_13
inst : CommMonoid M₁
inst_1 : CommMonoid M₂
inst_2 : CommMonoid M₃
inst_3 : CommMonoid N₁
inst_4 : CommMonoid N₂
inst_5 : CommMonoid N₃
f : M₁ →* M₂
g : M₂ →* M₃
f' : N₁ →* N₂
g' : N₂ →* N₃
τ₁ : M₁ →* N₁
τ₂ : M₂ →* N₂
τ₃ : M₃ →* N₃
h₁ : Surjective.{u_8 + 1, u_11 + 1} (α := M₁) (β := N₁) (⇑τ₁ : (a : M₁) → N₁)
h₂ : Bijective.{u_9 + 1, u_12 + 1} (α := M₂) (β := N₂) (⇑τ₂ : (a : M₂) → N₂)
h₃ : Injective.{u_10 + 1, u_13 + 1} (α := M₃) (β := N₃) (⇑τ₃ : (a : M₃) → N₃)
comm₁₂ :
  ∀ (x : M₁),
    Eq.{u_12 + 1} (α := N₂) ((f' : (a : N₁) → N₂) ((τ₁ : (a : M₁) → N₁) x : N₁) : N₂)
      ((τ₂ : (a : M₂) → N₂) ((f : (a : M₁) → M₂) x : M₂) : N₂)
comm₂₃ :
  ∀ (x : M₂),
    Eq.{u_13 + 1} (α := N₃) ((g' : (a : N₂) → N₃) ((τ₂ : (a : M₂) → N₂) x : N₂) : N₃)
      ((τ₃ : (a : M₃) → N₃) ((g : (a : M₂) → M₃) x : M₃) : N₃)
h : MulExact.{u_11, u_12, u_13} (M := N₁) (N := N₂) (P := N₃) (⇑f' : (a : N₁) → N₂) (⇑g' : (a : N₂) → N₃)
x₂ : M₂
hx₂ : Eq.{u_10 + 1} (α := M₃) ((g : (a : M₂) → M₃) x₂ : M₃) (1 : M₃)
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₂
⊢ 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])

Premises used: Iff.mp, DFunLike.coe
-- Module: Mathlib.Algebra.Exact
Goal:
M₁ : Type u_8
M₂ : Type u_9
M₃ : Type u_10
N₁ : Type u_11
N₂ : Type u_12
N₃ : Type u_13
inst : CommMonoid M₁
inst_1 : CommMonoid M₂
inst_2 : CommMonoid M₃
inst_3 : CommMonoid N₁
inst_4 : CommMonoid N₂
inst_5 : CommMonoid N₃
f : M₁ →* M₂
g : M₂ →* M₃
f' : N₁ →* N₂
g' : N₂ →* N₃
τ₁ : M₁ →* N₁
τ₂ : M₂ →* N₂
τ₃ : M₃ →* N₃
h₁ : Surjective.{u_8 + 1, u_11 + 1} (α := M₁) (β := N₁) (⇑τ₁ : (a : M₁) → N₁)
h₂ : Bijective.{u_9 + 1, u_12 + 1} (α := M₂) (β := N₂) (⇑τ₂ : (a : M₂) → N₂)
h₃ : Injective.{u_10 + 1, u_13 + 1} (α := M₃) (β := N₃) (⇑τ₃ : (a : M₃) → N₃)
comm₁₂ :
  ∀ (x : M₁),
    Eq.{u_12 + 1} (α := N₂) ((f' : (a : N₁) → N₂) ((τ₁ : (a : M₁) → N₁) x : N₁) : N₂)
      ((τ₂ : (a : M₂) → N₂) ((f : (a : M₁) → M₂) x : M₂) : N₂)
comm₂₃ :
  ∀ (x : M₂),
    Eq.{u_13 + 1} (α := N₃) ((g' : (a : N₂) → N₃) ((τ₂ : (a : M₂) → N₂) x : N₂) : N₃)
      ((τ₃ : (a : M₃) → N₃) ((g : (a : M₂) → M₃) x : M₃) : N₃)
h : MulExact.{u_11, u_12, u_13} (M := N₁) (N := N₂) (P := N₃) (⇑f' : (a : N₁) → N₂) (⇑g' : (a : N₂) → N₃)
x₂ : M₂
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₂)
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₂
⊢ Membership.mem (γ := Set M₂) (Set.range.{u_9, u_8 + 1} (ι := M₁) (⇑f : (a : M₁) → M₂)) x₂

Tactic:
obtain ⟨x₁, rfl⟩ := h₁ y₁

Premises used: rfl
-- Module: Mathlib.Algebra.Exact
Goal:
M₁ : Type u_8
M₂ : Type u_9
M₃ : Type u_10
N₁ : Type u_11
N₂ : Type u_12
N₃ : Type u_13
inst : CommMonoid M₁
inst_1 : CommMonoid M₂
inst_2 : CommMonoid M₃
inst_3 : CommMonoid N₁
inst_4 : CommMonoid N₂
inst_5 : CommMonoid N₃
f : M₁ →* M₂
g : M₂ →* M₃
f' : N₁ →* N₂
g' : N₂ →* N₃
τ₁ : M₁ →* N₁
τ₂ : M₂ →* N₂
τ₃ : M₃ →* N₃
h₁ : Surjective.{u_8 + 1, u_11 + 1} (α := M₁) (β := N₁) (⇑τ₁ : (a : M₁) → N₁)
h₂ : Bijective.{u_9 + 1, u_12 + 1} (α := M₂) (β := N₂) (⇑τ₂ : (a : M₂) → N₂)
h₃ : Injective.{u_10 + 1, u_13 + 1} (α := M₃) (β := N₃) (⇑τ₃ : (a : M₃) → N₃)
comm₁₂ :
  ∀ (x : M₁),
    Eq.{u_12 + 1} (α := N₂) ((f' : (a : N₁) → N₂) ((τ₁ : (a : M₁) → N₁) x : N₁) : N₂)
      ((τ₂ : (a : M₂) → N₂) ((f : (a : M₁) → M₂) x : M₂) : N₂)
comm₂₃ :
  ∀ (x : M₂),
    Eq.{u_13 + 1} (α := N₃) ((g' : (a : N₂) → N₃) ((τ₂ : (a : M₂) → N₂) x : N₂) : N₃)
      ((τ₃ : (a : M₃) → N₃) ((g : (a : M₂) → M₃) x : M₃) : N₃)
h : MulExact.{u_11, u_12, u_13} (M := N₁) (N := N₂) (P := N₃) (⇑f' : (a : N₁) → N₂) (⇑g' : (a : N₂) → N₃)
x₂ : M₂
hx₂ : Eq.{u_10 + 1} (α := M₃) ((g : (a : M₂) → M₃) x₂ : M₃) (1 : 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_12 + 1} (α := N₂) ((τ₂ : (a : M₂) → N₂) ((f : (a : M₁) → M₂) x₁ : M₂) : N₂) ((τ₂ : (a : M₂) → N₂) x₂ : N₂)

Tactic:
simpa only [comm₁₂] using hy₁
-- Module: Mathlib.Algebra.Exact
Goal:
M₁ : Type u_8
M₂ : Type u_9
M₃ : Type u_10
N₁ : Type u_11
N₂ : Type u_12
N₃ : Type u_13
inst : CommMonoid M₁
inst_1 : CommMonoid M₂
inst_2 : CommMonoid M₃
inst_3 : CommMonoid N₁
inst_4 : CommMonoid N₂
inst_5 : CommMonoid N₃
f : M₁ →* M₂
g : M₂ →* M₃
f' : N₁ →* N₂
g' : N₂ →* N₃
τ₁ : M₁ →* N₁
τ₂ : M₂ →* N₂
τ₃ : M₃ →* N₃
h₁ : Surjective.{u_8 + 1, u_11 + 1} (α := M₁) (β := N₁) (⇑τ₁ : (a : M₁) → N₁)
h₂ : Bijective.{u_9 + 1, u_12 + 1} (α := M₂) (β := N₂) (⇑τ₂ : (a : M₂) → N₂)
h₃ : Injective.{u_10 + 1, u_13 + 1} (α := M₃) (β := N₃) (⇑τ₃ : (a : M₃) → N₃)
comm₁₂ :
  ∀ (x : M₁),
    Eq.{u_12 + 1} (α := N₂) ((f' : (a : N₁) → N₂) ((τ₁ : (a : M₁) → N₁) x : N₁) : N₂)
      ((τ₂ : (a : M₂) → N₂) ((f : (a : M₁) → M₂) x : M₂) : N₂)
comm₂₃ :
  ∀ (x : M₂),
    Eq.{u_13 + 1} (α := N₃) ((g' : (a : N₂) → N₃) ((τ₂ : (a : M₂) → N₂) x : N₂) : N₃)
      ((τ₃ : (a : M₃) → N₃) ((g : (a : M₂) → M₃) x : M₃) : N₃)
h : MulExact.{u_11, u_12, u_13} (M := N₁) (N := N₂) (P := N₃) (⇑f' : (a : N₁) → N₂) (⇑g' : (a : N₂) → N₃)
x₂ : M₂
hx₂ : Eq.{u_10 + 1} (α := M₃) ((g : (a : M₂) → M₃) x₂ : M₃) (1 : M₃)
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:
exact ⟨x₁, h₂.1 (by simpa only [comm₁₂] using hy₁)⟩
-- Module: Mathlib.Algebra.Exact
Goal:
M₁ : Type u_8
M₂ : Type u_9
M₃ : Type u_10
N₁ : Type u_11
N₂ : Type u_12
N₃ : Type u_13
inst : CommMonoid M₁
inst_1 : CommMonoid M₂
inst_2 : CommMonoid M₃
inst_3 : CommMonoid N₁
inst_4 : CommMonoid N₂
inst_5 : CommMonoid N₃
f : M₁ →* M₂
g : M₂ →* M₃
f' : N₁ →* N₂
g' : N₂ →* N₃
τ₁ : M₁ →* N₁
τ₂ : M₂ →* N₂
τ₃ : M₃ →* N₃
h₁ : Surjective.{u_8 + 1, u_11 + 1} (α := M₁) (β := N₁) (⇑τ₁ : (a : M₁) → N₁)
h₂ : Bijective.{u_9 + 1, u_12 + 1} (α := M₂) (β := N₂) (⇑τ₂ : (a : M₂) → N₂)
h₃ : Injective.{u_10 + 1, u_13 + 1} (α := M₃) (β := N₃) (⇑τ₃ : (a : M₃) → N₃)
comm₁₂ :
  ∀ (x : M₁),
    Eq.{u_12 + 1} (α := N₂) ((f' : (a : N₁) → N₂) ((τ₁ : (a : M₁) → N₁) x : N₁) : N₂)
      ((τ₂ : (a : M₂) → N₂) ((f : (a : M₁) → M₂) x : M₂) : N₂)
comm₂₃ :
  ∀ (x : M₂),
    Eq.{u_13 + 1} (α := N₃) ((g' : (a : N₂) → N₃) ((τ₂ : (a : M₂) → N₂) x : N₂) : N₃)
      ((τ₃ : (a : M₃) → N₃) ((g : (a : M₂) → M₃) x : M₃) : N₃)
h : MulExact.{u_11, u_12, u_13} (M := N₁) (N := N₂) (P := N₃) (⇑f' : (a : N₁) → N₂) (⇑g' : (a : N₂) → N₃)
x₁ : M₁
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₃)
⊢ Eq.{u_10 + 1} (α := M₃) ((g : (a : M₂) → M₃) ((f : (a : M₁) → M₂) x₁ : M₂) : M₃) (1 : M₃)

Tactic:
apply h₃