-- Mathlib/Algebra/Colimit/Module.lean
lemma lift_injective [IsDirected ι (· ≤ ·)]
    (injective : ∀ i, Function.Injective <| g i) :
    Function.Injective (lift R ι G f g Hg)

Proof state:
case inl
R : Type u_1
inst✝⁷ : Semiring R
ι : Type u_2
inst✝⁶ : Preorder ι
G : ι → Type u_3
inst✝⁵ : DecidableEq ι
inst✝⁴ : (i : ι) → AddCommMonoid (G i)
inst✝³ : (i : ι) → Module R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
P : Type u_4
inst✝² : AddCommMonoid P
inst✝¹ : Module R P
g : (i : ι) → G i →ₗ[R] P
Hg : ∀ (i j : ι) (hij : i ≤ j) (x : G i), (g j) ((f i j hij) x) = (g i) x
inst✝ : IsDirected ι fun x1 x2 => x1 ≤ x2
injective : ∀ (i : ι), Function.Injective ⇑(g i)
h✝ : IsEmpty ι
⊢ Function.Injective ⇑(lift R ι G f g Hg)

Tactic:
apply Function.injective_of_subsingleton

Result:
no goals

Proof state:
case inr
R : Type u_1
inst✝⁷ : Semiring R
ι : Type u_2
inst✝⁶ : Preorder ι
G : ι → Type u_3
inst✝⁵ : DecidableEq ι
inst✝⁴ : (i : ι) → AddCommMonoid (G i)
inst✝³ : (i : ι) → Module R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
P : Type u_4
inst✝² : AddCommMonoid P
inst✝¹ : Module R P
g : (i : ι) → G i →ₗ[R] P
Hg : ∀ (i j : ι) (hij : i ≤ j) (x : G i), (g j) ((f i j hij) x) = (g i) x
inst✝ : IsDirected ι fun x1 x2 => x1 ≤ x2
injective : ∀ (i : ι), Function.Injective ⇑(g i)
h✝ : Nonempty ι
z w : DirectLimit G f
eq : (lift R ι G f g Hg) z = (lift R ι G f g Hg) w
⊢ z = w

Tactic:
obtain ⟨i, x, y, rfl, rfl⟩ := exists_of₂ z w

Result:
case inr.intro.intro.intro.intro
R : Type u_1
inst✝⁷ : Semiring R
ι : Type u_2
inst✝⁶ : Preorder ι
G : ι → Type u_3
inst✝⁵ : DecidableEq ι
inst✝⁴ : (i : ι) → AddCommMonoid (G i)
inst✝³ : (i : ι) → Module R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
P : Type u_4
inst✝² : AddCommMonoid P
inst✝¹ : Module R P
g : (i : ι) → G i →ₗ[R] P
Hg : ∀ (i j : ι) (hij : i ≤ j) (x : G i), (g j) ((f i j hij) x) = (g i) x
inst✝ : IsDirected ι fun x1 x2 => x1 ≤ x2
injective : ∀ (i : ι), Function.Injective ⇑(g i)
h✝ : Nonempty ι
i : ι
x y : G i
eq : (lift R ι G f g Hg) ((of R ι G f i) x) = (lift R ι G f g Hg) ((of R ι G f i) y)
⊢ (of R ι G f i) x = (of R ι G f i) y

Proof state:
case inr
R : Type u_1
inst✝⁷ : Semiring R
ι : Type u_2
inst✝⁶ : Preorder ι
G : ι → Type u_3
inst✝⁵ : DecidableEq ι
inst✝⁴ : (i : ι) → AddCommMonoid (G i)
inst✝³ : (i : ι) → Module R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
P : Type u_4
inst✝² : AddCommMonoid P
inst✝¹ : Module R P
g : (i : ι) → G i →ₗ[R] P
Hg : ∀ (i j : ι) (hij : i ≤ j) (x : G i), (g j) ((f i j hij) x) = (g i) x
inst✝ : IsDirected ι fun x1 x2 => x1 ≤ x2
injective : ∀ (i : ι), Function.Injective ⇑(g i)
h✝ : Nonempty ι
⊢ Function.Injective ⇑(lift R ι G f g Hg)

Tactic:
intros z w eq

Result:
case inr
R : Type u_1
inst✝⁷ : Semiring R
ι : Type u_2
inst✝⁶ : Preorder ι
G : ι → Type u_3
inst✝⁵ : DecidableEq ι
inst✝⁴ : (i : ι) → AddCommMonoid (G i)
inst✝³ : (i : ι) → Module R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
P : Type u_4
inst✝² : AddCommMonoid P
inst✝¹ : Module R P
g : (i : ι) → G i →ₗ[R] P
Hg : ∀ (i j : ι) (hij : i ≤ j) (x : G i), (g j) ((f i j hij) x) = (g i) x
inst✝ : IsDirected ι fun x1 x2 => x1 ≤ x2
injective : ∀ (i : ι), Function.Injective ⇑(g i)
h✝ : Nonempty ι
z w : DirectLimit G f
eq : (lift R ι G f g Hg) z = (lift R ι G f g Hg) w
⊢ z = w

Proof state:
case inr.intro.intro.intro.intro
R : Type u_1
inst✝⁷ : Semiring R
ι : Type u_2
inst✝⁶ : Preorder ι
G : ι → Type u_3
inst✝⁵ : DecidableEq ι
inst✝⁴ : (i : ι) → AddCommMonoid (G i)
inst✝³ : (i : ι) → Module R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
P : Type u_4
inst✝² : AddCommMonoid P
inst✝¹ : Module R P
g : (i : ι) → G i →ₗ[R] P
Hg : ∀ (i j : ι) (hij : i ≤ j) (x : G i), (g j) ((f i j hij) x) = (g i) x
inst✝ : IsDirected ι fun x1 x2 => x1 ≤ x2
injective : ∀ (i : ι), Function.Injective ⇑(g i)
h✝ : Nonempty ι
i : ι
x y : G i
eq : (g i) x = (g i) y
⊢ (of R ι G f i) x = (of R ι G f i) y

Tactic:
rw [injective _ eq]

Result:
no goals

Proof state:
case inr.intro.intro.intro.intro
R : Type u_1
inst✝⁷ : Semiring R
ι : Type u_2
inst✝⁶ : Preorder ι
G : ι → Type u_3
inst✝⁵ : DecidableEq ι
inst✝⁴ : (i : ι) → AddCommMonoid (G i)
inst✝³ : (i : ι) → Module R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
P : Type u_4
inst✝² : AddCommMonoid P
inst✝¹ : Module R P
g : (i : ι) → G i →ₗ[R] P
Hg : ∀ (i j : ι) (hij : i ≤ j) (x : G i), (g j) ((f i j hij) x) = (g i) x
inst✝ : IsDirected ι fun x1 x2 => x1 ≤ x2
injective : ∀ (i : ι), Function.Injective ⇑(g i)
h✝ : Nonempty ι
i : ι
x y : G i
eq : (lift R ι G f g Hg) ((of R ι G f i) x) = (lift R ι G f g Hg) ((of R ι G f i) y)
⊢ (of R ι G f i) x = (of R ι G f i) y

Tactic:
simp_rw [lift_of] at eq

Result:
case inr.intro.intro.intro.intro
R : Type u_1
inst✝⁷ : Semiring R
ι : Type u_2
inst✝⁶ : Preorder ι
G : ι → Type u_3
inst✝⁵ : DecidableEq ι
inst✝⁴ : (i : ι) → AddCommMonoid (G i)
inst✝³ : (i : ι) → Module R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
P : Type u_4
inst✝² : AddCommMonoid P
inst✝¹ : Module R P
g : (i : ι) → G i →ₗ[R] P
Hg : ∀ (i j : ι) (hij : i ≤ j) (x : G i), (g j) ((f i j hij) x) = (g i) x
inst✝ : IsDirected ι fun x1 x2 => x1 ≤ x2
injective : ∀ (i : ι), Function.Injective ⇑(g i)
h✝ : Nonempty ι
i : ι
x y : G i
eq : (g i) x = (g i) y
⊢ (of R ι G f i) x = (of R ι G f i) y

Proof state:
R : Type u_1
inst✝⁷ : Semiring R
ι : Type u_2
inst✝⁶ : Preorder ι
G : ι → Type u_3
inst✝⁵ : DecidableEq ι
inst✝⁴ : (i : ι) → AddCommMonoid (G i)
inst✝³ : (i : ι) → Module R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
P : Type u_4
inst✝² : AddCommMonoid P
inst✝¹ : Module R P
g : (i : ι) → G i →ₗ[R] P
Hg : ∀ (i j : ι) (hij : i ≤ j) (x : G i), (g j) ((f i j hij) x) = (g i) x
inst✝ : IsDirected ι fun x1 x2 => x1 ≤ x2
injective : ∀ (i : ι), Function.Injective ⇑(g i)
⊢ Function.Injective ⇑(lift R ι G f g Hg)

Tactic:
cases isEmpty_or_nonempty ι

Result:
case inl
R : Type u_1
inst✝⁷ : Semiring R
ι : Type u_2
inst✝⁶ : Preorder ι
G : ι → Type u_3
inst✝⁵ : DecidableEq ι
inst✝⁴ : (i : ι) → AddCommMonoid (G i)
inst✝³ : (i : ι) → Module R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
P : Type u_4
inst✝² : AddCommMonoid P
inst✝¹ : Module R P
g : (i : ι) → G i →ₗ[R] P
Hg : ∀ (i j : ι) (hij : i ≤ j) (x : G i), (g j) ((f i j hij) x) = (g i) x
inst✝ : IsDirected ι fun x1 x2 => x1 ≤ x2
injective : ∀ (i : ι), Function.Injective ⇑(g i)
h✝ : IsEmpty ι
⊢ Function.Injective ⇑(lift R ι G f g Hg)

case inr
R : Type u_1
inst✝⁷ : Semiring R
ι : Type u_2
inst✝⁶ : Preorder ι
G : ι → Type u_3
inst✝⁵ : DecidableEq ι
inst✝⁴ : (i : ι) → AddCommMonoid (G i)
inst✝³ : (i : ι) → Module R (G i)
f : (i j : ι) → i ≤ j → G i →ₗ[R] G j
P : Type u_4
inst✝² : AddCommMonoid P
inst✝¹ : Module R P
g : (i : ι) → G i →ₗ[R] P
Hg : ∀ (i j : ι) (hij : i ≤ j) (x : G i), (g j) ((f i j hij) x) = (g i) x
inst✝ : IsDirected ι fun x1 x2 => x1 ≤ x2
injective : ∀ (i : ι), Function.Injective ⇑(g i)
h✝ : Nonempty ι
⊢ Function.Injective ⇑(lift R ι G f g Hg)