-- Mathlib/LinearAlgebra/LinearPMap.lean
theorem le_of_le_graph {f g : E →ₗ.[R] F} (h : f.graph ≤ g.graph) : f ≤ g

Proof state:
case left
R : Type u_1
inst✝⁴ : Ring R
E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_3
inst✝¹ : AddCommGroup F
inst✝ : Module R F
f g : E →ₗ.[R] F
h : f.graph ≤ g.graph
x : E
hx : x ∈ f.domain
⊢ x ∈ g.domain

Tactic:
rw [mem_domain_iff] at hx ⊢

Result:
case left
R : Type u_1
inst✝⁴ : Ring R
E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_3
inst✝¹ : AddCommGroup F
inst✝ : Module R F
f g : E →ₗ.[R] F
h : f.graph ≤ g.graph
x : E
hx : ∃ y, (x, y) ∈ f.graph
⊢ ∃ y, (x, y) ∈ g.graph

Proof state:
case right.mk.mk
R : Type u_1
inst✝⁴ : Ring R
E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_3
inst✝¹ : AddCommGroup F
inst✝ : Module R F
f g : E →ₗ.[R] F
h : f.graph ≤ g.graph
x : E
hx : x ∈ f.domain
y : E
hy : y ∈ g.domain
hxy : ↑⟨x, hx⟩ = ↑⟨y, hy⟩
⊢ ↑f ⟨x, hx⟩ = ↑g ⟨y, hy⟩

Tactic:
rw [image_iff]

Result:
case right.mk.mk
R : Type u_1
inst✝⁴ : Ring R
E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_3
inst✝¹ : AddCommGroup F
inst✝ : Module R F
f g : E →ₗ.[R] F
h : f.graph ≤ g.graph
x : E
hx : x ∈ f.domain
y : E
hy : y ∈ g.domain
hxy : ↑⟨x, hx⟩ = ↑⟨y, hy⟩
⊢ (y, ↑f ⟨x, hx⟩) ∈ g.graph

Proof state:
case h
R : Type u_1
inst✝⁴ : Ring R
E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_3
inst✝¹ : AddCommGroup F
inst✝ : Module R F
f g : E →ₗ.[R] F
h : f.graph ≤ g.graph
x : E
y : F
hx : (x, y) ∈ f.graph
⊢ (x, y) ∈ g.graph

Tactic:
exact h hx

Result:
no goals

Proof state:
R : Type u_1
inst✝⁴ : Ring R
E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_3
inst✝¹ : AddCommGroup F
inst✝ : Module R F
f g : E →ₗ.[R] F
h : f.graph ≤ g.graph
⊢ f ≤ g

Tactic:
constructor

Result:
case left
R : Type u_1
inst✝⁴ : Ring R
E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_3
inst✝¹ : AddCommGroup F
inst✝ : Module R F
f g : E →ₗ.[R] F
h : f.graph ≤ g.graph
⊢ f.domain ≤ g.domain

case right
R : Type u_1
inst✝⁴ : Ring R
E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_3
inst✝¹ : AddCommGroup F
inst✝ : Module R F
f g : E →ₗ.[R] F
h : f.graph ≤ g.graph
⊢ ∀ ⦃x : ↥f.domain⦄ ⦃y : ↥g.domain⦄, ↑x = ↑y → ↑f x = ↑g y

Proof state:
case right.mk.mk
R : Type u_1
inst✝⁴ : Ring R
E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_3
inst✝¹ : AddCommGroup F
inst✝ : Module R F
f g : E →ₗ.[R] F
h : f.graph ≤ g.graph
x : E
hx : x ∈ f.domain
y : E
hy : y ∈ g.domain
hxy : ↑⟨x, hx⟩ = ↑⟨y, hy⟩
⊢ (y, ↑f ⟨x, hx⟩) ∈ f.graph

Tactic:
simp only [Submodule.coe_mk] at hxy

Result:
case right.mk.mk
R : Type u_1
inst✝⁴ : Ring R
E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_3
inst✝¹ : AddCommGroup F
inst✝ : Module R F
f g : E →ₗ.[R] F
h : f.graph ≤ g.graph
x : E
hx : x ∈ f.domain
y : E
hy : y ∈ g.domain
hxy : x = y
⊢ (y, ↑f ⟨x, hx⟩) ∈ f.graph

Proof state:
case right.mk.mk
R : Type u_1
inst✝⁴ : Ring R
E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_3
inst✝¹ : AddCommGroup F
inst✝ : Module R F
f g : E →ₗ.[R] F
h : f.graph ≤ g.graph
x : E
hx✝ : x ∈ f.domain
y : E
hx : y ∈ f.domain
hy : y ∈ g.domain
hxy : x = y
⊢ (y, ↑f ⟨x, hx✝⟩) ∈ f.graph

Tactic:
rw [← image_iff hx]

Result:
case right.mk.mk
R : Type u_1
inst✝⁴ : Ring R
E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_3
inst✝¹ : AddCommGroup F
inst✝ : Module R F
f g : E →ₗ.[R] F
h : f.graph ≤ g.graph
x : E
hx✝ : x ∈ f.domain
y : E
hx : y ∈ f.domain
hy : y ∈ g.domain
hxy : x = y
⊢ ↑f ⟨x, hx✝⟩ = ↑f ⟨y, hx⟩

Proof state:
case left
R : Type u_1
inst✝⁴ : Ring R
E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_3
inst✝¹ : AddCommGroup F
inst✝ : Module R F
f g : E →ₗ.[R] F
h : f.graph ≤ g.graph
x : E
hx : ∃ y, (x, y) ∈ f.graph
⊢ ∃ y, (x, y) ∈ g.graph

Tactic:
obtain ⟨y, hx⟩ := hx

Result:
case left.intro
R : Type u_1
inst✝⁴ : Ring R
E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_3
inst✝¹ : AddCommGroup F
inst✝ : Module R F
f g : E →ₗ.[R] F
h : f.graph ≤ g.graph
x : E
y : F
hx : (x, y) ∈ f.graph
⊢ ∃ y, (x, y) ∈ g.graph

Proof state:
case left
R : Type u_1
inst✝⁴ : Ring R
E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_3
inst✝¹ : AddCommGroup F
inst✝ : Module R F
f g : E →ₗ.[R] F
h : f.graph ≤ g.graph
⊢ f.domain ≤ g.domain

Tactic:
intro x hx

Result:
case left
R : Type u_1
inst✝⁴ : Ring R
E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_3
inst✝¹ : AddCommGroup F
inst✝ : Module R F
f g : E →ₗ.[R] F
h : f.graph ≤ g.graph
x : E
hx : x ∈ f.domain
⊢ x ∈ g.domain

Proof state:
case right.mk.mk
R : Type u_1
inst✝⁴ : Ring R
E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_3
inst✝¹ : AddCommGroup F
inst✝ : Module R F
f g : E →ₗ.[R] F
h : f.graph ≤ g.graph
x : E
hx : x ∈ f.domain
y : E
hy : y ∈ g.domain
hxy : ↑⟨x, hx⟩ = ↑⟨y, hy⟩
⊢ (y, ↑f ⟨x, hx⟩) ∈ g.graph

Tactic:
refine h ?_

Result:
case right.mk.mk
R : Type u_1
inst✝⁴ : Ring R
E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_3
inst✝¹ : AddCommGroup F
inst✝ : Module R F
f g : E →ₗ.[R] F
h : f.graph ≤ g.graph
x : E
hx : x ∈ f.domain
y : E
hy : y ∈ g.domain
hxy : ↑⟨x, hx⟩ = ↑⟨y, hy⟩
⊢ (y, ↑f ⟨x, hx⟩) ∈ f.graph

Proof state:
case right.mk.mk
R : Type u_1
inst✝⁴ : Ring R
E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_3
inst✝¹ : AddCommGroup F
inst✝ : Module R F
f g : E →ₗ.[R] F
h : f.graph ≤ g.graph
x : E
hx✝ : x ∈ f.domain
y : E
hx : y ∈ f.domain
hy : y ∈ g.domain
hxy : x = y
⊢ ↑f ⟨x, hx✝⟩ = ↑f ⟨y, hx⟩

Tactic:
simp [hxy]

Result:
no goals

Proof state:
case left.intro
R : Type u_1
inst✝⁴ : Ring R
E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_3
inst✝¹ : AddCommGroup F
inst✝ : Module R F
f g : E →ₗ.[R] F
h : f.graph ≤ g.graph
x : E
y : F
hx : (x, y) ∈ f.graph
⊢ ∃ y, (x, y) ∈ g.graph

Tactic:
use y

Result:
case h
R : Type u_1
inst✝⁴ : Ring R
E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_3
inst✝¹ : AddCommGroup F
inst✝ : Module R F
f g : E →ₗ.[R] F
h : f.graph ≤ g.graph
x : E
y : F
hx : (x, y) ∈ f.graph
⊢ (x, y) ∈ g.graph

Proof state:
case right.mk.mk
R : Type u_1
inst✝⁴ : Ring R
E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_3
inst✝¹ : AddCommGroup F
inst✝ : Module R F
f g : E →ₗ.[R] F
h : f.graph ≤ g.graph
x : E
hx : x ∈ f.domain
y : E
hy : y ∈ g.domain
hxy : x = y
⊢ (y, ↑f ⟨x, hx⟩) ∈ f.graph

Tactic:
rw [hxy] at hx

Result:
case right.mk.mk
R : Type u_1
inst✝⁴ : Ring R
E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_3
inst✝¹ : AddCommGroup F
inst✝ : Module R F
f g : E →ₗ.[R] F
h : f.graph ≤ g.graph
x : E
hx✝ : x ∈ f.domain
y : E
hx : y ∈ f.domain
hy : y ∈ g.domain
hxy : x = y
⊢ (y, ↑f ⟨x, hx✝⟩) ∈ f.graph

Proof state:
case right
R : Type u_1
inst✝⁴ : Ring R
E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_3
inst✝¹ : AddCommGroup F
inst✝ : Module R F
f g : E →ₗ.[R] F
h : f.graph ≤ g.graph
⊢ ∀ ⦃x : ↥f.domain⦄ ⦃y : ↥g.domain⦄, ↑x = ↑y → ↑f x = ↑g y

Tactic:
rintro ⟨x, hx⟩ ⟨y, hy⟩ hxy

Result:
case right.mk.mk
R : Type u_1
inst✝⁴ : Ring R
E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_3
inst✝¹ : AddCommGroup F
inst✝ : Module R F
f g : E →ₗ.[R] F
h : f.graph ≤ g.graph
x : E
hx : x ∈ f.domain
y : E
hy : y ∈ g.domain
hxy : ↑⟨x, hx⟩ = ↑⟨y, hy⟩
⊢ ↑f ⟨x, hx⟩ = ↑g ⟨y, hy⟩